Changeset 891 for src/common
 Timestamp:
 Jun 7, 2011, 4:53:53 PM (9 years ago)
 Location:
 src/common
 Files:

 3 edited
Legend:
 Unmodified
 Added
 Removed

src/common/Mem.ma
r790 r891 66 66 ∀A: Type[0]. ∀x: block. ∀v: A. ∀f: block > A. 67 67 update_block … x v f x = v. 68 #A * * #ix #v #f whd in ⊢ (??%?) ;69 > (eqZb_z_z …) //;68 #A * * #ix #v #f whd in ⊢ (??%?) 69 >eq_block_b_b // 70 70 qed. 71 71 
src/common/Smallstep.ma
r700 r891 133 133 #tr #ge #s1 #t1 #s2 #t2 #s3 #t3 #Hstar #Hstep #e1 inversion Hstar; 134 134 [ #s2' #e2 #e3 #e4 destruct; @plus_one //; 135  #s1' #t1' #s1'' #t1'' #s2' #t2' #H1 #H2 #e2 #foo #e3 #e4 #e5 destruct;136 > (Eapp_assoc …)@(plus_left … H1)135  #s1' #t1' #s1'' #t1'' #s2' #t2' #H1 #H2 #e2 #foo #e3 #e4 #e5 136 >e1 >e4 >e2 >Eapp_assoc destruct @(plus_left … H1) 137 137 [ 2: @(star_right … H2 Hstep) //; 138 138  skip; 
src/common/Values.ma
r797 r891 64 64  @H2 % #E destruct elim H3 /2/ 65 65 ] qed. 66 67 lemma eq_block_b_b : ∀b. eq_block b b = true. 68 * * #z whd in ⊢ (??%?) >eqZb_z_z @refl 69 qed. 66 70 67 71 (* Characterise the memory regions which the pointer representations can … … 1225 1229 lemma sign_ext_lessdef: 1226 1230 ∀n,v1,v2. Val_lessdef v1 v2 → Val_lessdef (sign_ext n v1) (sign_ext n v2). 1227 #n #v1 #v2 #H inversion H ;//;#v #e1 #e2 <e1 in H >e2 //;1231 #n #v1 #v2 #H inversion H // #v #e1 #e2 whd in ⊢ (?%?) // 1228 1232 qed. 1229 1233 (*
Note: See TracChangeset
for help on using the changeset viewer.