Changeset 535 for Deliverables/D3.1/Csemantics/Smallstep.ma
 Timestamp:
 Feb 16, 2011, 4:25:02 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D3.1/Csemantics/Smallstep.ma
r487 r535 87 87 [ @(t'⧺t2) 88 88  // 89  <(Eapp_assoc …) //;89  <(Eapp_assoc …) <H2 @H5 90 90 ] 91 91 ] … … 104 104 star tr ge s1 t s3. 105 105 #tr #ge #s1 #t1 #s2 #t2 #s3 #t #H1 #H2 #H3 106 @(star_trans … H1 … (star_one … H2)) //;106 @(star_trans … H1 … (star_one … H2)) @H3 107 107 qed. 108 108 … … 124 124 ∀tr,ge,s1,t,s2. plus tr ge s1 t s2 > star tr ge s1 t s2. 125 125 #tr #ge #s1 #t #s2 #H elim H; #s1' #t1' #s2' #t2' #s3' #t3' #H1 #H2 #e1 126 @(star_step … H1 H2 …) //;126 @(star_step … H1 H2 …) @e1; 127 127 qed. 128 128 … … 216 216 forever tr ge s1 (t ⧻ T). 217 217 #tr #ge #s1 #t1 #s2 #H elim H; 218 [ #s' #T #H2 //;218 [ #s' #T #H2 @H2 219 219  #s1' #t1 #s0 #t0 #s2' #t2' #H1 #H2 #e1 #IH #T #H3 220 220 >e1 >(Eappinf_assoc …) … … 551 551 elim (IH ? B); #st3' *; #C #D 552 552 %{ st3'} % //; 553 @(star_trans ??? tA st2' ? tB ) //;554 elim A ; /2/; *; //;553 @(star_trans ??? tA st2' ? tB ?? C Ht) 554 elim A /2/ * // 555 555 ] qed. 556 556
Note: See TracChangeset
for help on using the changeset viewer.