Changeset 365 for C-semantics/CexecIOcomplete.ma
- Timestamp:
- Dec 2, 2010, 4:40:54 PM (10 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
C-semantics/CexecIOcomplete.ma
r253 r365 485 485 ##] nqed. 486 486 487 nlemma wrong_sound: ∀ge,tr,s,s',e. 488 execution_goes_wrong tr s e s' → 489 exec_inf_aux ge (Value ??? 〈E0, s〉) = e_step E0 s e → 490 star (mk_transrel … step) ge s tr s' ∧ 491 nostep (mk_transrel … step) ge s' ∧ 492 (¬∃r. final_state s' r). 493 #ge tr0 s0 s0' e0 WRONG; ncases WRONG; 494 #tr s s' e ESTEPS EXEC; 495 ncases (several_steps … ESTEPS EXEC); 496 #STAR EXEC'; @; 497 ##[ @; ##[ napply STAR; 498 ##| #badtr bads; @; #badSTEP; 499 nlapply (step_complete … badSTEP); 500 nlapply (exec_e_step … EXEC'); 501 ncases (exec_step ge s'); 502 ##[ #o k; nrewrite > (execution_cases (exec_inf_aux …)); #E; nwhd in E:(??%?); 503 ndestruct 504 ##| #x; ncases x; #trx stx; nrewrite > (exec_inf_aux_unfold …); 505 nwhd in ⊢ (??%? → ?); ncases (is_final_state stx); 506 #FINAL E; nwhd in E:(??%?); ndestruct 507 ##| #E H; nwhd in H; napply H 508 ##] 509 ##] 510 ##| @; #FINAL; 511 nrewrite > (exec_inf_aux_unfold …) in EXEC'; 512 nwhd in ⊢ (??%? → ?); 513 ncases (is_final_state s'); #FINAL'; 514 ##[ nwhd in ⊢ (??%? → ?); #E; ndestruct; 515 ##| napply False_ind; napply (absurd … FINAL FINAL'); 516 ##] 517 ##] nqed.
Note: See TracChangeset
for help on using the changeset viewer.