Previous Up Next
B.3 Subject reduction for the rewriting semantics (Theorem 1.2)


We first show a couple of properties relating typing and the set of declared labels.
Lemma 7  []   For any class C such that A |- C : z(r)BV,W, then dl(C) = dom(B).
The proof of this lemma is omitted because it is a straighforward induction on the depth of A |- C : z(r)BV,W.
Lemma 8  []   For any selective refinement clauses S such that A |- S :: BW Þ B'W', V', we have dom(B') \ dom(B) Í dl(S).

Proof: Selective refinement clauses can always be written as |i Î I Ki Þ K'i |> P. A proof of A |- S :: BW Þ B'W', V' can only end with rule Modifier in which the derivation of each premise ends with a rule Modifier-Clause. Hence, we have at least the judgments
  Ai |- Ki :: Bi (18)
  Bi Í B (19)
  Ai |- Ki' :: B'i (20)
  B' = Åi Î i B'i (21)
Hence,
  dom(B') \ dom(B) Í dom(B') \ (Èi Î I dom(Bi)) by (19)
    = (Èi Î I dom(B'i)) \ (Èi Î I dom(Bi)) by (21)
    = Èi Î I ( dom(B'i) \ (ÈjÎ I dom(Bj)))
    Í Èi Î I ( dom(B'i) \ dom(Bi))
    = Èi Î I (dl(K'i) \ dl(Ki))
    = dl(S)


We now show that filter rewriting |- ® preserves typing. We denote with B \ L the set of pairs l : t that belongs to B and such that l ÏL.
Lemma 9  [Filter rewriting]   If all the following conditions hold
C with S |-® C'      A |- C :: z(r)BW,V
A |- S :: B1W1 Þ B2W2,V2      dl(S) Ç dom(B1) = Ø      B Í B1      B2 | dom(B1) Í B1     
then A |- C' :: z(r)(B Å (B2 \ L))W',V' for some W' Í W È (W2 Ç dom(B Å (B2 \ L))), V' Í V È (V2 Ç ( dom(B1) \ L)), and L Í (dl(S) \ dl(C')) È ( dom(B1) \ dom(B)).

Proof: In this proof, we abbreviate dom(B) by ëBû, for sake of conciseness.

Basic cases.
Filter-Apply.
Let us assume that
  K1 & K |> P with K1 Þ K2 |> Q | S     
       |® K2 & K |> P & Q or dl(K1) \ dl(K2) (1)
  A |- K1 & K |> P :: z(r)BW, V (2)
  A |- K1 Þ K2 |> Q | S :: B1W1 Þ B2W2,V2 (3)
  ((dl(K2) \ dl(K1)) È dl(S)) Ç ëB1û = Ø (4)
  B Í B1 (5)
  B2 | ëB1û Í B1 (6)
The judgments (2) and (3) are respectively derived by
[Sub]
[Reaction]
[Synchronization]
A' |- K1 :: B1' (7)      A' |- K :: B0  (8)
A' |- K1 & K :: B1' Å B0  (9)
A + A' |- P (10)      ëA'û = fn(K1 & K) (11)
A |- K1 & K |> P :: z(r)(B1' Å B0)cl(K1 & K),Ø
A |- K1 & K |> P :: z(r)(B1' Å B0)W,V
and,
[Modifier]+[Sub]
A'' |- K1 :: B1' (12)
A'' |- K2 :: B2' (14)
A + A'' |- Q  (15)
     B1' Í B1 (13)
ëA''û = fn(K2) (16)
W2' = cls(B1W1, K1 Þ K2)
A |- K1 Þ K2 |> Q :: B1W1 Þ B2'W2',dl(K1) \ dl(K2)
    ···
A |- K1 Þ K2 |> Q | S :: B1W1 Þ B2W2,V2
where B = B1' Å B0 (17), cl(K1 & K) Í W (18), B2' Í B2 (19), W2' Í W2 and dl(K1) \ dl(K2) Í V2 (20).

From (7) and (12), A' and A'' coincide on fn(K1) because they assign the same types to fn(K1). Moreover, due to the scope rules of reaction rules and the selection operator, we can safely assume that ëA'û Ç ëA''û = fn(K1). Thus, by Lemma 2 applied to (8), and (14) we derive A'+A'' |- K :: B0 (21) and A'+A'' |- K2 :: B2' (22). Similarly, by lemma 2 applied to (10) and (15), we also derive A + A' + A'' |- P (23) and A + A' + A'' |- Q  (24).

Foremost we prove the linearity of K2 & K. Notice that dl(K2) = (dl(K2) \ dl(K1)) È (dl(K2) Ç dl(K1)) and both left and right hand-sides of the È have an empty intersection with dl(K). This follows from (4) and from the linearity of K1 & K.

By rule Synchronization with premises (22) and (21), we derive A' + A'' |- K2 & K :: B2' Å B0 (25). Also, combining the judgments (23) and (24) yields A + A' + A'' |- P & Q (26) using rule Parallel. By premises (11) and (16) we have ëA'û È ëA''û = fn(K) È fn(K1)È fn(K2). By (16) and (12), we have fn(K1) Í fn(K2). Hence ëA' + A''û = fn(K2 & K) (27). Therefore, by Reaction with premises (25), (26), and (27) we derive
A |- K2 & K |> P & Q :: z(r)(B2' Å B0)cl(K2 & K),Ø      (28).
By rule Abstract, we also deduce
A |- dl(K1) \ dl(K2) :: z(r)B1'' Ø,dl(K1) \ dl(K2)     (29)
where B1'' = B1' \ dl(K2) (30). Hence, Disjunction allows to derive:
A |- K2 & K |> P & Q or L' :: z(r)(B2' Å B0 Å B1'' )cl(K2 & K), dl(K1) \ dl(K2)      (31)
and by rule Sub:
A |- K2 & K |> P & Q or L' :: z(r)(B2' Å B0 Å B1'' )W', V'      (32)
where W' = W È cl(K2 & K) and V' = V È (dl(K1) \ dl(K2)).

Let L be (dl(S) \ (dl(K2) È dl(K) È dl(K1))) È ((ëB1û \ ëBû) \ dl(K2)), or equivalently, (dl(S) \ (ëB'2û È ëB0û È ëB'1û)) È ((ëB1û \ ëBû) \ ëB'2û) (33). Observe that L is choosen so as to satisfy the condition L Í (dl(S) \ dl(C')) È (ëB1û \ ëBû). To conclude, we verify that other constraints of the lemma are satisfied for the judgment (32). That is,
  1. B2' Å B0 Å B1'' = B Å (B2 \ L). By (6), (13), (17), (19) it is enough to check the set equality: ëB'2ûÈ ëB0û È ëB''1û = ëBû È (ëB2û \ L). Since both sides of (33) are restrictions outside of the set ëB'2û, we have L Ç ëB'2û Ì ëBû (34). Therefore,
    ëB2'û È ëB0û È ëB1''û
      = ëB2'û È ëB0û È (ëB1'û \ dl(K2)) by definition of B'1
      = ëB2'û È ëB0û È (ëB1'û \ ëB'2û)) by (16)
      = ëB2'û È ëB0û È ëB1'û
      = ëB2'û È ëBû by definition of B
      = ëBû È (ëB2û \ L) by (34)


  2. W' Í W È (W2 Ç (ëB Å (B2 \ L)û). Because W' = W È cl(K2 & K) and cl(K2 & K) Í W2 by (18), and cl(K2 & K) Í dl(K2 & K) = ëB'2û È ëB0û Í ëB Å (B2 \ L)û by the equality above.

  3. V' Í V È (V2 Ç (ëB1û \ L)). By definition, V' = V È (dl(K1) \ dl(K2)) and dl(K1) \ dl(K2) Í V2 by (20). It remains to prove that dl(K1) \ dl(K2)Í ëB1û \ L. Since dl(K1) \ dl(K2)Í ëB1û, it suffices to show that (dl(K1) \ dl(K2)) Ç L = Ø. Obviously, (dl(K1) \ dl(K2)) Ç (dl(S) \ dl(K2 & K & K1)) = Ø, whilst (dl(K1) \ dl(K2)) Ç ((ëB1û \ ëBû) \ dl(K2))= Ø, since dl(K1) = ëB'1û Í ëBû.
Filter-End.
Let us assume
  M |> P with 0 |® M |> P (1)
  A |- M |> P :: z(r)BW,V (2)
  A |- 0 :: B1W1 Þ B2W2,V2 (3)
  dl(0) Ç ëB1û = Ø (4)
  B Í B1 (5)
Since in (3) ëB2û must be the empty set, we conclude from (2) by choosing L = ëB1û \ ëBû, W' = W, and V' = V.

Filter-Abstract.
Let us assume
  L' with S |® L'
  A |- L' :: z(r)BW,V (1)
  A |- S :: B1W1 Þ B2W2, V2
  dl(S) Ç ëB1û = Ø (2)
  B Í B1 (3)
  B2 | ëB1û Í B1 (4)
A derivation of (1) must contain an instance of rule Abstract, hence A |- L' :: z(r)BØ,V and ëBû = V = L' (5). Let L be (dl(S) \ L') È (ëB1û \ ëBû). We show that (1) satisfies the lemma:
  1. B Å (B2 \ L) =B. Since by (4) B2 is compatible with B1 and with B by (3), it suffices to show that ëB2û \ L Í ëBû. By (5), it follows that L is equal to (dl(S) È ëB1û) \ ëBû (6). Hence:
    ëB2û \ L = ((ëB2û | ëB1û) È (ëB2û \ ëB1û)) \ L
      Í (ëB1û È dl(S)) \ L by (4) and Lemma 8
      = (ëB1û È dl(S)) \ ((ëB1û È dl(S)) \ ëBû)
      = (ëB1û È dl(S)) Ç ëBû


  2. W Í W È (W2 Ç (ëB Å B2û \ L)). Obvious.

  3. V Í V È (V2 Ç (ëB1û \ L)). Obvious.
Inductive cases.
Filter-Next.
Let us assume
  M |> P with K1 Þ K2 |> Q | S |® C' (1)
  dl(K1) ¬ Ídl(M) (2)
  A |- M |> P :: z(r)BW,V (3)
  A |- K1 Þ K2 |> Q | S :: B1W1 Þ B2W2, V2 (4)
  ((dl(K2) \ dl(K1)) È dl(S)) Ç ëB1û = Ø (5)
  B Í B1 (6)
  B2 | ëB1û Í B1 (7)
The selection clauses S are of the form |iÎ IKi' Þ K''i |> Qi. A derivation of (4) must contain an instance of Modifier, with premises:
  A |- K1 Þ K2 |> Q :: B1W1 Þ B2'W2', V2' (8)
  (A |- Ki' Þ Ki'' |> Qi :: B1W1 Þ Bi''Wi'', Vi'')i Î I
where
  B2'' = Åi Î I B''i  
  B2 = B2' Å B2'' (9)
  W2'' = ÈiÎ I Wi''  
  W2 = W2' È W2'' (10)
  V2'' = Èi Î I Vi''  
  V2 = V2' È V2'' (11)
 
Hence, by rule Modifier, we derive
A |- S :: B1W1 Þ B2''W2'', V2''     (12)
A derivation of (1) must end with an instance of rule Filter-Next, hence M |> P with S |® C' (13). By induction hypothesis applied to (13), (3), (5), (12), (6), and (7) there must exist some L', W', and V' such that
  A |- C' :: z(r)(B Å (B''2 \ L'))W', V' (14)
  L' Í (dl(S) \ dl(C')) È (ëB1û \ ëBû) (15)
  W' Í W È (W''2 Ç (ëB Å (B''2 \ L')û)) (16)
  V' Í V È (V''2 Ç (ëB1û \ L')) (17)
Let us prove that A |- C' :: z(r)(B Å (B2 \ L))W', V' (18), for L = L' È ëB'2û \ (ëB1û È ëB''2û) and check that L, W', V' satisfy the conditions of the lemma. We first prove that L Í (((dl(K2) \ dl(K1)) È dl(S)) \ dl(C')) È (ëB1û \ ëBû) (19). By Lemma 8 applied to (8), we have ëB2'û\ ëB1û Í dl(K2) \ dl(K1) (20). Notice that dl(C') = ëBû È ëB''2 \ L'û by Lemma 7 and (14), hence dl(C') Í ëBû È ëB''2û (21). Thus, we have:
  L = L' È ëB'2û \ (ëB1û È ëB''2û)
  = L' È (ëB'2û \ ëB1û) \ ëB''2û  
  Í L' È (dl(K2) \ dl(K1)) \ ëB''2û by (20)
  = L' È (dl(K2) \ dl(K1)) \ (ëBû È ëB''2û) by (5)
  Í L' È (dl(K2) \ dl(K1)) \ dl(C') by (21)
  = (dl(S) \ dl(C')) È (ëB1û \ ëBû) È (dl(K2) \ dl(K1)) \ dl(C') by (15)
  = ((dl(K2) \ dl(K1)) È dl(S)) \ dl(C') È ëB1û \ ëBû
To conclude, we check the following properties:
  1. B Å (B2 \ L) =B Å (B''2 \ L'). Since by (7) B2 and B1 agree, and so do B''2 and B by (6) and (9), it suffices to check the equality of their domains. By
    ëBû È (ëB2û \ L)   = ëBû È (ëB2û \ (L' È ëB'2û \ (ëB1û È ëB''2û)))
    = ëBû È (ëB2û \ (ëB'2û \ (ëB1û È ëB''2û))) \ L'
    = ëBû È ((B'2 Å B''2) \ (ëB'2û \ (ëB1û È ëB''2û))) \ L'
    = ëBû È ((ëB'2û \ (ëB'2û \ (ëB1û È ëB''2û))) È
      (ëB'2û \ (ëB'2û \ (ëB1û È ëB''2û))) ) \ L'
    = ëBû È ((ëB1û È ëB''2û) | ëB'2û È B''2) \ L'
    =
    ëBû È
     
    (ëB1û | ëB'2û) \ L'
    Í B
    		È
     
    (ëB''2û | ëB'2û) \ L'
    Í B''2 \ L'
    		È (ëB''2û \ L')
    = ëBû È (ëB''2û \ L')


  2. W' Í W È (W2 Ç ëB Å (B2 \ L)û). This follows from (16), W2'' Í W2 (by (10)), and B Å (B2 \ L) =B Å (B''2 \ L').

  3. V' Í V È (V2 Ç (ëB1û \ L)). This follows from (17), V2 Í V2' (by (11)) and L' Í L (by definition of L').
Filter-Or.
Let us assume that:
  C1 or C2 with S |-® C' (1)
  A |- C1 or C2 :: z(r)BW,V (2)
  A |- S :: B1 Þ B2W2,V2 (3)
  dl(S) Ç ëB1û = Ø (4)
  B Í B1 (5)
  B2 | ëB1û Í B1 (6)
A derivation of (2) must end with an instance of rule Disjunction, followed by a sequence of rules Sub. Hence B is of the form B'1 Å B'2 (7) and:
  A |- C1 :: z(r)B'1W'1, V'1 (8)
  A |- C2 :: z(r)B'2W'2, V'2 (9)
  W'1 È W'2 Í W (10)
  (V'1 \ (ëB'2û \ V'2)) È (V'2 \ (ëB'1û \ V'1)) Í V (11)
The condition (4) implies that dl(S) Ç ëBiû = Ø for i Î {1,2} (12). The reduction (1) implies that C' is of the form C'1 or C'2 such that Ci with S |® C'i for i Î {1,2} (13). By induction hypothesis applied to (13), (8) and (9), (3), (12), (5), and (6), it follows that there exist some Li, W''i, and V''i such that
  A |- C'i :: z(r)(B'i Å (B2 \ Li))W''i, V''i (14)
  Li Í (dl(S) \ dl(C'i)) È (ëB1û \ ëB'iû) (15)
  W''i Í W'i È (W2 Ç ëB'i Å (B2 \ Liû)) (16)
  V''i Í V'i È (V2 Ç (ëB1û \ Li)) (17)
for i Î {1,2}. By rule Disjunction applied to the two cases of (14) and since B'1, B'2 and B''2 are compatible by (6), (5) and by the definition of B'1 and B'2, we have:
A |- C'1 or C'2 :: z(r)(B'1 Å B'2 Å (B2 \ L1) Å (B2 \ L2)W', V'     (18)
where
  W' = W''1 È W''2
  V' = V''1 \ (ëB'2 Å (B2 \ L2)û \ V''2) È V''2 \ (ëB'1 Å (B2 \ L1)û \ V''1)
Let L be L1 Ç L2. Then
  L = L1 Ç L2
  Í ((dl(S) \ dl(C1)) È (ëB1û \ ëB'1û)) Ç ((dl(S) \ dl(C2)) È (ëB1û \ ëB'2û)) by (15)
  Í (dl(S) \ dl(C1)) Ç (dl(S) \ dl(C2)) È (ëB1û \ ëB'1û) Ç (ëB1û \ ëB'2û) by distributivity
  = (dl(S) \ (dl(C1) È dl(C2))) È (ëB1û \ (ëB'1û È ëB'2û))
  = (dl(S) \ dl(C)) È (ëB1û \ ëBû) (19)

To conclude, we prove that (18) satisfies the constraints of the lemma. Indeed, we have:
  1. B Å (B2 \ L) = B'1 Å B'2 Å (B2 \ L1) Å (B2 \ L2). Since B = B'1 Å B'2 and B2 \ L = B2 \ L1 Å B2 \ L2.

  2. W' Í W È (W2 Ç ëB Å (B2 \ L)û). Since W' = W''1 È W''2, it suffices to show that W''i Í W È (W2 Ç ëB Å (B2 \ L)û), for i Î {1,2}. This follows by (16), (10) and because B'i Å (B2 \ Li) Í B Å (B2 \ L) (by previous item).

  3. V' Í V È (V2 Ç (ëB1û \ L)). It suffices to show that both
    V''1 \ (ëB'2 Å (B2 \ L2)û \ V''2) Í V È (V2 Ç (ëB1û \ L))
    and
    V''2 \ (ëB'1 Å (B2 \ L1)û \ V''1) Í V È (V2 Ç (ëB1û \ L))
    Each of these two containments follows by (17), which establishes a stronger relation between a superset of the left hand side and two subsets of the two right hand sides.





Theorem 3  [Process Reduction]   Process rewriting |- ® preserves typing.

We show that class reduction |-x® and process reduction |- ® preserve typing, simultaneously.

That is, we prove that
  1. if A + x : [r] , x.(B | F) |- C:: z(r)BW,V and C |-x® C' then A + x : [r] , x.(B | F) |- C':: z(r)BW,V;

  2. if A |- P and P |-® P' then A |- P'.
Proof: We reason by induction on the depth of the proofs of C |-x® C' and P |-® P'. We write Ax for A + x : [r] , x.(B | F).

Basic cases for class reduction.
Self.
Let self(z)  C |-x® C {z ¬ x} and let Ax |- self(z)  C :: z(r)BW,V. A derivation of this judgment must end with an instance of Self-Binding, followed by a sequence of Sub rules. Hence,
Ax + z : [r] , z.(B | F) |- C :: z(r)B W',V'
with W' Í W and V' Í V. Then, by Lemma 5, we have:
Ax |- C {z ¬ x} :: z(r)B W',V'
We conclude Ax |- C {z ¬ x} :: z(r)BW,V by rule Sub.

Or-Pat.
Let J1 or J2 |> P |-x® J1 |> P or J2 |> P and let Ax |- J1 or J2 |> P :: z(r)BW, V (1). The derivation of this judgment must end with the following derivation followed by a sequence of Sub rules:
[Reaction]
[Alternative]
A' |- J1 :: B1      A' |- J2 :: B2     
A' |- J1 or J2 :: B
Ax + A' |- P      dom(A') = fn(J1 or J2) (2)
Ax |- J1 or J2 |> P :: z(r)Bcl(J1) È cl(J2), Ø
where B is B1 Å B2 and cl(J1) È cl(J2) Í W. Since fn(J1 or J2) = fn(J1) = fn(J2), we have:
[Disjunction]
A' |- Ji :: Bi      Ax+ A' |- P      dom(A') = fn(Ji)
Ax |- Ji |> P :: z(r)Bicl(Ji), Ø
 i = 1, 2
Ax |- J1 |> P or J2 |> P :: z(r)Bcl(J1) È cl(J2), Ø
The we conclude Ax |- J1 |> P or J2 |> P :: z(r)BW, V by rule Sub.

Abstract-Cut.
Let C or L |-x® C or L' and Ax |- C or L :: z(r)BW,V and L' = L \ dl(C), with L ¹ L'. Therefore L' Í L (1). The derivation of the judgment Ax |- C or L :: z(r)BW,V must end with the following derivation followed by a sequence of Sub rules:
[Disjunction]
[Abstract]
dom(B2) = L
Ax |- L :: z(r)B2Ø, L
     Ax|- C :: z(r)B1W1,V1
L'' = L \ ( dom(B1) \ V1) (2)
Ax |- C or L :: z(r)(B1 Å B2)W1, V1 È L''
where B = B1 Å B2, W1 Í W (3) and V1 È L'' Í V (4).

We first observe that B1 Å B2 = B1 Å (B2 | L'). Therefore we can derive:
[Disjunction]
[Abstract]
dom(B2 | L') = L'
Ax |- L' :: z(r)(B2 | L')Ø, L'
     Ax|- C :: z(r)B1W1,V1
L''' = L' \ ( dom(B1) \ V1) (5)
Ax |- C or L' :: z(r)(B1 Å B2)W1, V1 È L'''
By (2), (5) and (1), we derive V1 È L''' Í V1 È L''. Hence, by (3), (4) and rule Sub, we obtain Ax |- C or L' :: z(r)(B1 Å B2)W, V.

Class-Abstract.
Let C or Ø |-x® C and Ax |- C or Ø :: z(r)BW,V. The derivation of this judgment must end with rule Disjunction followed by a sequence of Sub rules:
[Disjunction]
Ax |- C :: z(r)BW', V'      Ax|- Ø :: z(r)ØØ, Ø
Ax |- C or Ø :: z(r)BW',V'
where W' Í W and V' Í V. Then, by rule Sub applied to Ax |- C :: z(r)BW',V', we obtain Ax |- C :: z(r)BW,V.

Basic cases for processes.
Class-Var.
Let us assume A |- class c = self(z)  C in P (1) and class c = C in P |-® P {x ¬ C}. The final part of the derivation of (1) must have the form
Class
A |- C :: z(r)BW,V (2)
A + c : " Gen (r, B, A). z(r)BW,V |- P (3)
A |- class c = C in P
By Lemma 6 applied to (2) and (3), we derive A |- P {c ¬ C}.

Inductive cases for classes.
Class-Context.
Let Ax |- E {C} :: z(r)BW,V and E {C} |-x® E {C'}. By inductive hypothesis, if Ax |- C :: z(r)B'W', V' then Ax |- C' :: z(r)B'W',V', since C |-x® C'. The judgment Ax |- E {C'} :: z(r)BV follows by induction on the structure of E {·}. The details are omitted.

Match.
Let us assume that A |- match C with S end : z(r)BW, V (1) and match C with S end ¾® C' (2). We must prove that A |- C' : z(r)BW, V (3)

A derivation of (1) must end with an instance of rule Refinement followed by a sequence of Sub. Hence, B is of the form B1 Å B2 (4) and
  A |- C :: z(r)B1W1, V1 (5)
  A |- S :: B1W1 Þ B2W2, V2 (6)
  dl(S) Ç dom(B1) = Ø (7)
  W1 È W2 Í W (8)
  V1 È V2 Í V (9)
The derivation of (2) must contain a rule Match with the premises:
  C with S ¾® C' (10)
  dl(S) Í dl(C') (11)
From (4) it follows that B2 | dom(B1) Í dom(B2) (12). Lemma 9 applied to (10), (5), (6), (7), and (12) implies that
  A |- C' :: z(r)(B1 Å (B2 \ L))W',V' (13)
  L Í (dl(S) \ dl(C')) È ( dom(B1) \ dom(B1)) (14)
  W' Í W1 È (W2 Ç dom(B1 Å (B2 \ L))) (15)
  V' Í V1 È (V2 Ç ( dom(B1) \ L)) (16)
The property (11) combined with (14) imply that L is empty. Therefore W' Í W1 È W2 and V' Í V1 È V2. Hence (3) follows by (13), (8), (9) and rule Sub.

Inductive cases for processes.
Class-Red.
Let A |- obj x = C init P in Q (1) and obj x = C init P in Q |- ® obj x = C' init P in P', under the assumption that C |-x® C' (2).

A derivation of (1) has the shape
[Object]
[Self-Binding]
A + x : [r], x :(B | F) |- C :: z(r)BW,Ø (3)
A |- self(x)  C :: z(r)BW,Ø
r = B | M      X= Gen (r, B, A) \ ctv(B|W)
A + x : " X. [r], x : " X. (B | F) |- P      A + x : " X. [r] |- Q
A |- obj x = C init P in Q
By induction hypothesis applied to (2) and (3), we obtain the judgment A + x : [r], x :(B | F) |- C' :: z(r)BW,Ø, which we can substitute in the previous derivation, thus concluding A |- obj x = C' init P in Q.


Previous Up Next