proposition: Lemma simulation_red_cont: forall C1 C1', red C1 C1' -> forall C2, match_conf C2 C1 -> exists C2', (plus step C2 C2' \/ (star step C2 C2' /\ rmeasure C1' < rmeasure C1))%nat /\ match_conf C2' C1'.
proof: Proof. intros C1 C1' R C2 MC. inversion MC; subst. destruct C1' as (c' & s'). assert (A: red_apply_cont_cases k c s c' s') by (apply invert_red_apply_cont; auto). clear MC R. inversion A; subst; clear A. - cut (exists C2', plus step (c, k, s) C2' /\ match_conf C2' (apply_cont k c2, s')). intros (C2' & A & B). exists C2'; auto. revert k. dependent induction H; intros. + econstructor; split. apply plus_one; constructor. constructor; auto. + econstructor; split. eapply plus_left. constructor. eapply star_one. constructor. constructor; auto. + edestruct IHred as (((cx & kx) & sx) & A & B); eauto. econstructor; split. eapply plus_left. constructor. apply plus_star. eexact A. exact B. + econstructor; split. apply plus_one; constructor. constructor; auto. + econstructor; split. apply plus_one; apply step_while_done; auto. constructor; auto. + econstructor; split. apply plus_one; apply step_while_loop; auto. constructor; auto. - econstructor; split. left; apply plus_one; constructor. constructor; auto. - econstructor; split. left; apply plus_one; constructor. constructor; auto. Qed.
imports: Coq(Arith ZArith Psatz Bool String List Program.Equality) CDF(Sequences Simulation)