Changeset 250 for C-semantics/CexecIOcomplete.ma
- Timestamp:
- Nov 22, 2010, 2:40:22 PM (10 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
C-semantics/CexecIOcomplete.ma
r239 r250 61 61 62 62 ntheorem the_initial_state: 63 ∀p,s. initial_state p s → yieldsIO ?? (make_initial_state p) s.63 ∀p,s. initial_state p s → yieldsIObare ? (make_initial_state p) s. 64 64 #p s; ncases p; #fns main globs H; 65 napply remove_io_sig;66 65 ninversion H; 67 66 #b f e1 e2 e3; 67 nwhd in ⊢ (??%?); 68 68 nrewrite > e1; 69 69 nwhd in ⊢ (??%?); … … 84 84 85 85 nlemma cast_complete: ∀m,v,ty,ty',v'. 86 cast m v ty ty' v' → yields ?? (exec_cast m v ty ty') v'.86 cast m v ty ty' v' → yieldsbare ? (exec_cast m v ty ty') v'. 87 87 #m v ty ty' v' H; 88 88 nelim H; … … 91 91 ##| #m i sz sz' sg; napply refl; 92 92 ##| #m f sz sz'; napply refl; 93 ##| #m sp sp' ty ty' b ofs H1 H2 H3; napply remove_res_sig;93 ##| #m sp sp' ty ty' b ofs H1 H2 H3; 94 94 nelim H1; ##[ #sp1 ty1 ##| #sp1 ty1 n1 ##| #tys1 ty1; nletin sp1 ≝ Code ##] 95 95 nwhd in ⊢ (??%?);
Note: See TracChangeset
for help on using the changeset viewer.