Changeset 190 for C-semantics
- Timestamp:
- Oct 18, 2010, 11:36:10 AM (10 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
C-semantics/Mem.ma
r156 r190 1026 1026 ncases (in_bounds m1 chunk' psp' b' ofs'); 1027 1027 ##[#Hvalid1;nrewrite > (in_bounds_true m2 chunk' psp' b' ofs' ? (Some ? ?) ??); 1028 ##[nwhd in ⊢ (???%); napply eq_f;napply eq_f;1028 ##[nwhd in ⊢ (???%); napply (eq_f … (Some val));napply (eq_f … (load_result chunk')); 1029 1029 nrewrite > Heq;nwhd in ⊢ (??(???(? (? % ?)))?); 1030 1030 nwhd in ⊢ (??(???(? %))?); … … 1086 1086 napply (store_valid_access_1 … STORE);// 1087 1087 ##|#H3;ncases H3; 1088 #x;#Hx;nrewrite > Hx;napply eq_f;1088 #x;#Hx;nrewrite > Hx;napply (eq_f … (Some val)); 1089 1089 napply (load_store_overlap … STORE … Hx);//;##] 1090 1090 nqed. … … 1123 1123 napply 1124 1124 (store_valid_access_1 … STORE);// 1125 ##|*;#x;#Hx;nrewrite > Hx;napply eq_f;1125 ##|*;#x;#Hx;nrewrite > Hx;napply (eq_f … (Some val)); 1126 1126 napply (load_store_mismatch … STORE … Hsize);//;##] 1127 1127 nqed. … … 1207 1207 ##| nrewrite < H1 in ⊢ (% → ?);#Hx'; 1208 1208 nrewrite < H1 in Hx;#Hx;nrewrite > Hx; 1209 napply eq_f;napply (load_store_overlap … STORE … Hx');/2/;1209 napply (eq_f … (Some val));napply (load_store_overlap … STORE … Hx');/2/; 1210 1210 ##] 1211 1211 ##|#H1;#H2;#H3; … … 1214 1214 nrewrite > H1; nelim (store_valid_access_3 … STORE); // 1215 1215 ##| nrewrite < H1 in Hx ⊢ %; nrewrite < H2; #Hx Hx'; 1216 nrewrite > Hx;napply eq_f;1216 nrewrite > Hx;napply (eq_f … (Some val)); 1217 1217 napply (load_store_mismatch … STORE … Hx');/2/ 1218 1218 ##] … … 1517 1517 ##| nrewrite > (class_alloc_same … ALLOC); // 1518 1518 ##] 1519 ##| *; #v;#LOAD; nrewrite > LOAD; napply eq_f;1519 ##| *; #v;#LOAD; nrewrite > LOAD; napply (eq_f … (Some val)); 1520 1520 napply (load_alloc_same … ALLOC … LOAD); 1521 1521 ##] nqed.
Note: See TracChangeset
for help on using the changeset viewer.