Ignore:
Timestamp:
Nov 19, 2011, 12:38:20 AM (9 years ago)
Author:
sacerdot
Message:

Ported to syntax of Matita 0.99.1.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Cminor/semantics.ma

    r1369 r1516  
    185185#l #s elim s
    186186try (try #a try #b try #c try #d try #e try #f try #g try #h try #i try #j try #m % * (* *) )
    187 [ #s1 #s2 #IH1 #IH2 #k #f #en #Inv #kInv whd in ⊢ (??%? → ?(???%))
     187[ #s1 #s2 #IH1 #IH2 #k #f #en #Inv #kInv whd in ⊢ (??%? → ?(???%));
    188188  lapply (IH1 (Kseq s2 k) f en (π2 (π1 Inv)) (conj ?? (π2 Inv) kInv))
    189189  cases (find_label l s1 (Kseq s2 k) f en ??)
    190   [ #H1 whd in ⊢ (??%? → ?)
     190  [ #H1 whd in ⊢ (??%? → ?);
    191191    lapply (IH2 k f en (π2 Inv) kInv) cases (find_label l s2 k f en ??)
    192192    [ #H2 #_ % #H cases (Exists_append … H)
     
    198198  | #sk #_ #E whd in E:(??%?); destruct
    199199  ]
    200 | #sz #sg #e #s1 #s2 #IH1 #IH2 #k #f #en #Inv #kInv whd in ⊢ (??%? → ?(???%))
     200| #sz #sg #e #s1 #s2 #IH1 #IH2 #k #f #en #Inv #kInv whd in ⊢ (??%? → ?(???%));
    201201  lapply (IH1 k f en (π2 (π1 Inv)) kInv)
    202202  cases (find_label l s1 k f en ??)
    203   [ #H1 whd in ⊢ (??%? → ?)
     203  [ #H1 whd in ⊢ (??%? → ?);
    204204    lapply (IH2 k f en (π2 Inv) kInv) cases (find_label l s2 k f en ??)
    205205    [ #H2 #_ % #H cases (Exists_append … H)
     
    214214| #s1 #IH #k #f #en #Inv #kInv @IH
    215215| #E whd in i:(??%?); cases (identifier_eq Label l a) in i;
    216   whd in ⊢ (? → ??%? → ?) [ #_ #E2 destruct | *; #H cases (H (sym_eq … E)) ]
     216  whd in ⊢ (? → ??%? → ?); [ #_ #E2 destruct | *; #H cases (H (sym_eq … E)) ]
    217217| whd in i:(??%?); cases (identifier_eq Label l a) in i;
    218   whd in ⊢ (? → ??%? → ?) [ #_ #E2 destruct | #NE #E cases (c d e f ?? E) #H @H ]
     218  whd in ⊢ (? → ??%? → ?); [ #_ #E2 destruct | #NE #E cases (c d e f ?? E) #H @H ]
    219219| #cl #s1 #IH #k #f #en #Inv #kInv @IH
    220220] qed.
Note: See TracChangeset for help on using the changeset viewer.