Changeset 1244 for src/Clight/CexecSound.ma
 Timestamp:
 Sep 21, 2011, 6:08:50 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/Clight/CexecSound.ma
r1224 r1244 533 533 qed. 534 534 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).535 lemma make_initial_state_sound : ∀p. P_res ? (initial_state p) (make_initial_state p). 536 536 #p cases p; #fns #main #vars 537 537 whd in ⊢ (???%); 538 @bind_OK #ge #Ege539 538 @bind_OK #m #Em 540 539 @opt_bind_OK #x cases x; #sp #b #esb 541 540 @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 543 542 qed. 544 543
Note: See TracChangeset
for help on using the changeset viewer.