proposition: Lemma compile_cont_Kwhile_inv: forall C b c k pc s, compile_cont C (Kwhile b c k) pc -> exists pc', plus (transition C) (pc, nil, s) (pc', nil, s) /\ code_at C pc' (compile_com (WHILE b c)) /\ compile_cont C k (pc' + codelen(compile_com (WHILE b c))).
proof: Proof. intros. dependent induction H. - exists (pc + 1 + d); split. apply plus_one. eapply trans_branch; eauto. split; congruence. - edestruct IHcompile_cont as (pc'' & A & B & D). eauto. exists pc''; split; auto. eapply plus_left. eapply trans_branch; eauto. apply plus_star; auto. Qed.
imports: Coq(Arith ZArith Psatz Bool String List Program.Equality) CDF(Sequences IMP Simulation)