proposition: Theorem compile_program_correct_terminating: forall s c s', cexec s c s' -> machine_terminates (compile_program c) s s'.
proof: Proof. intros. set (C := compile_program c). assert (CODEAT: code_at C 0 (compile_com c ++ Ihalt :: nil)). { replace C with (nil ++ compile_program c ++ nil). apply code_at_intro. auto. rewrite app_nil_r; auto. } unfold machine_terminates. exists (0 + codelen (compile_com c)); split. - apply compile_com_correct_terminating. auto. eauto with code. - eauto with code. Qed.
imports: Coq(Arith ZArith Psatz Bool String List Program.Equality) CDF(Sequences IMP Simulation)