Changeset 1510 for src/common
- Timestamp:
- Nov 16, 2011, 4:38:41 PM (8 years ago)
- Location:
- src/common
- Files:
-
- 2 edited
Legend:
- Unmodified
- Added
- Removed
-
src/common/Smallstep.ma
r891 r1510 132 132 plus tr ge s1 t s3. 133 133 #tr #ge #s1 #t1 #s2 #t2 #s3 #t3 #Hstar #Hstep #e1 inversion Hstar; 134 [ #s2' #e2 #e3 #e4 destruct; @plus_one //;135 | #s1' #t1' #s1'' #t1'' #s2' #t2' #H1 #H2 #e2 #foo #e3 #e4 #e5 134 [ #s2' #e2 #e3 #e4 #e5s destruct; @plus_one //; 135 | #s1' #t1' #s1'' #t1'' #s2' #t2' #H1 #H2 #e2 #foo #e3 #e4 #e5 #e6 136 136 >e1 >e4 >e2 >Eapp_assoc destruct @(plus_left … H1) 137 137 [ 2: @(star_right … H2 Hstep) //; … … 140 140 ] 141 141 ] 142 qed. 142 qed. 143 143 (* 144 144 Lemma plus_left': -
src/common/Values.ma
r1369 r1510 1098 1098 ∀chunk,v1,v2. 1099 1099 Val_lessdef v1 v2 → Val_lessdef (load_result chunk v1) (load_result chunk v2). 1100 #chunk #v1 #v2 #H inversion H; //; #v #e1 #e2 cases chunk1101 [ 8: #r ] whd in ⊢ (?%?); //; 1100 #chunk #v1 #v2 #H inversion H; //; #v #e1 #e2 #e3 cases chunk 1101 [ 8: #r ] whd in ⊢ (?%?); //; 1102 1102 qed. 1103 1103
Note: See TracChangeset
for help on using the changeset viewer.