Ignore:
Timestamp:
Sep 21, 2011, 6:08:50 PM (8 years ago)
Author:
campbell
Message:

Sort out Clight semantics equivalence proof for new SmallstepExec?.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/CexecComplete.ma

    r1058 r1244  
    8181
    8282theorem the_initial_state:
    83   ∀p,s. initial_state p s → ∃ge. yields ? (make_initial_state p) 〈ge,s〉.
    84 #p #s cases p; #fns #main #globs #H
     83  ∀p,s. initial_state p s → yields ? (make_initial_state p) s.
     84#p #s cases p; #globs #fns #main #H
    8585inversion H;
    86 #b #f #ge #m #e1 #e2 #e3 #e4 #e5 %{ge}
    87 whd in ⊢ (??%?);
    88 >e1
     86#b #f #ge #m #e1 #e2 #e3 #e4 #e5
    8987whd in ⊢ (??%?);
    9088>e2
    9189whd in ⊢ (??%?);
     90change in e1:(??%?) with (make_global (mk_program ?? globs fns main))
     91>e1
    9292>e3
    9393whd in ⊢ (??%?);
Note: See TracChangeset for help on using the changeset viewer.