proposition: Lemma compile_cont_Kstop_inv: forall C pc s, compile_cont C Kstop pc -> exists pc', star (transition C) (pc, nil, s) (pc', nil, s) /\ instr_at C pc' = Some Ihalt.
proof: Proof. intros. dependent induction H. - exists pc; split. apply star_refl. auto. - destruct IHcompile_cont as (pc'' & A & B); auto. exists pc''; split; auto. eapply star_step; eauto. eapply trans_branch; eauto. Qed.
imports: Coq(Arith ZArith Psatz Bool String List Program.Equality) CDF(Sequences IMP Simulation)