proposition: Theorem compile_program_correct_diverging: forall c s, infseq step (c, Kstop, s) -> machine_diverges (compile_program c) s.
proof: Proof. intros. set (C := compile_program c). eapply (simulation_infseq _ _ _ _ _ _ (simulation_step C)). eauto. apply match_initial_configs. Qed.
imports: Coq(Arith ZArith Psatz Bool String List Program.Equality) CDF(Sequences IMP Simulation)