Changeset 2254 for src/Cminor
- Timestamp:
- Jul 24, 2012, 7:40:23 PM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/Cminor/semantics.ma
r2251 r2254 169 169 // 170 170 try @(π2 Inv) 171 try @(π2 (π1 Inv)) 172 [ % [ @(π2 Inv) | @kInv ] 171 try @(π1 (π2 Inv)) 172 try @(π2 (π2 Inv)) 173 [ % [ @(π2 (π2 Inv)) | @kInv ] 173 174 | % [ @(π2 Inv) | @kInv ] 174 175 ] qed. … … 180 181 try (try #a try #b try #c try #d try #e try #f try #g try #h try #i try #j try #m % * (* *) ) 181 182 [ #s1 #s2 #IH1 #IH2 #k #f #en #Inv #kInv whd in ⊢ (??%? → ?(???%)); 182 lapply (IH1 (Kseq s2 k) f en (π 2 (π1 Inv)) (conj ?? (π2 Inv) kInv))183 lapply (IH1 (Kseq s2 k) f en (π1 (π2 Inv)) (conj ?? (π2 (π2 Inv)) kInv)) 183 184 cases (find_label l s1 (Kseq s2 k) f en ??) 184 185 [ #H1 whd in ⊢ (??%? → ?); 185 lapply (IH2 k f en (π2 Inv) kInv) cases (find_label l s2 k f en ??)186 lapply (IH2 k f en (π2 (π2 Inv)) kInv) cases (find_label l s2 k f en ??) 186 187 [ #H2 #_ % #H cases (Exists_append … H) 187 188 [ #H' cases (H1 (refl ??)) /2/ … … 193 194 ] 194 195 | #sz #sg #e #s1 #s2 #IH1 #IH2 #k #f #en #Inv #kInv whd in ⊢ (??%? → ?(???%)); 195 lapply (IH1 k f en (π 2 (π1Inv)) kInv)196 lapply (IH1 k f en (π1 (π2 Inv)) kInv) 196 197 cases (find_label l s1 k f en ??) 197 198 [ #H1 whd in ⊢ (??%? → ?); 198 lapply (IH2 k f en (π2 Inv) kInv) cases (find_label l s2 k f en ??)199 lapply (IH2 k f en (π2 (π2 Inv)) kInv) cases (find_label l s2 k f en ??) 199 200 [ #H2 #_ % #H cases (Exists_append … H) 200 201 [ #H' cases (H1 (refl ??)) /2/ … … 382 383 try @kInv 383 384 try @(π1 (π1 Inv)) 384 try (@cont_inv_update @kInv) 385 try @(π2 (π1 (π1 Inv))) 385 try (@cont_inv_update @kInv) 386 try @(π2 (π1 (π1 Inv))) 386 387 try @(π1 (π1 (π1 Inv))) 387 try @(π1 Inv)388 388 try @(π2 Inv) 389 try @(π1 (π2 Inv)) 389 390 [ @fInv 390 391 | @(π2 Inv') 391 392 | @(π1 Inv') 392 | cases b [ @(π2 (π1 Inv)) | @(π2 Inv) ] 393 | % [ @(π2 Inv) | @kInv ] 393 | cases b [ @(π1 (π2 Inv)) | @(π2 (π2 Inv)) ] 394 | % [ @(π2 (π2 Inv)) | @kInv ] 395 | @(π1 (π1 (π1 (π1 Inv)))) 396 | @(π2 (π1 (π1 (π1 Inv)))) 397 | /3/ 394 398 | @stmt_inv_update @fInv 395 | 7,8: 399 | /3/ 400 | /3/ 401 | 12,13: 396 402 @(stmt_P_mp … (f_inv f)) 397 403 #s * #V #L #R % … … 406 412 | @I 407 413 | @cont_inv_update @Inv 414 | /3/ 408 415 | @stmt_inv_update @fInv 409 416 | @Inv 417 | /3/ 410 418 | @fInv 411 419 ] qed.
Note: See TracChangeset
for help on using the changeset viewer.