proposition: Lemma compile_cont_Kseq_inv: forall C c k pc s, compile_cont C (Kseq c k) pc -> exists pc', star (transition C) (pc, nil, s) (pc', nil, s) /\ code_at C pc' (compile_com c) /\ compile_cont C k (pc' + codelen(compile_com c)).
proof: Proof. intros. dependent induction H. - exists pc; split. apply star_refl. split; congruence. - edestruct IHcompile_cont as (pc'' & A & B). eauto. 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)