Changeset 1244 for src/Clight/CexecComplete.ma
- Timestamp:
- Sep 21, 2011, 6:08:50 PM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/Clight/CexecComplete.ma
r1058 r1244 81 81 82 82 theorem 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#H83 ∀p,s. initial_state p s → yields ? (make_initial_state p) s. 84 #p #s cases p; #globs #fns #main #H 85 85 inversion 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 89 87 whd in ⊢ (??%?); 90 88 >e2 91 89 whd in ⊢ (??%?); 90 change in e1:(??%?) with (make_global (mk_program ?? globs fns main)) 91 >e1 92 92 >e3 93 93 whd in ⊢ (??%?);
Note: See TracChangeset
for help on using the changeset viewer.