proposition: Lemma simulation_infseq_productive: forall N c1 c2, measure c1 < N -> infseq step1 c1 -> inv c1 c2 -> exists c1', exists c2', plus step2 c2 c2' /\ infseq step1 c1' /\ inv c1' c2'.
proof: Proof. induction N; intros c1 c2 MEAS INF1 INV. - lia. - destruct (infseq_inv INF1) as (c1' & STEP1 & INF1'). destruct (simulation _ _ STEP1 _ INV) as (c2' & P & INV'). destruct P as [STEPS2 | [STEPS2 MEAS']]. + exists c1'; exists c2'; auto. + inversion STEPS2; subst; clear STEPS2. * eapply IHN; eauto. lia. * exists c1'; exists c2'; split. eapply plus_left; eauto. auto. Qed.
imports: Coq(Psatz) CDF(Sequences)