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/CexecSound.ma

    r1224 r1244  
    533533qed.
    534534
    535 lemma make_initial_state_sound : ∀p. P_res ? (λgs.globalenv Genv ?? (fst ??) p = OK ? (\fst gs) ∧ initial_state p (\snd gs)) (make_initial_state p).
     535lemma make_initial_state_sound : ∀p. P_res ? (initial_state p) (make_initial_state p).
    536536#p cases p; #fns #main #vars
    537537whd in ⊢ (???%);
    538 @bind_OK #ge #Ege
    539538@bind_OK #m #Em
    540539@opt_bind_OK #x cases x; #sp #b #esb
    541540@opt_bind_OK #f #ef
    542 whd; % [ whd in ⊢ (???(??%)) @Ege | @(initial_state_intro … Ege Em esb ef) ]
     541@(initial_state_intro … Em esb ef) @refl
    543542qed.
    544543
Note: See TracChangeset for help on using the changeset viewer.