proposition: Theorem compile_program_correct_terminating_2: forall c s s', star step (c, Kstop, s) (SKIP, Kstop, s') -> machine_terminates (compile_program c) s s'.
proof: Proof. intros. set (C := compile_program c). edestruct (simulation_star _ _ _ _ _ _ (simulation_step C)) as (ms & A & B). eauto. apply match_initial_configs. inversion B; subst. edestruct compile_cont_Kstop_inv as (pc' & D & E). eauto. exists pc'; split; auto. eapply star_trans. eauto. cbn in D; autorewrite with code in D. eauto. Qed.
imports: Coq(Arith ZArith Psatz Bool String List Program.Equality) CDF(Sequences IMP Simulation)