Changeset 2254 for src/Cminor/semantics.ma
 Timestamp:
 Jul 24, 2012, 7:40:23 PM (8 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.