proposition: Lemma cexecinf_productive: forall c s, cexecinf s c -> exists c' s', plus red (c, s) (c', s') /\ cexecinf s' c'.
proof: Proof. induction c; intros s EXEC; inversion EXEC; subst. - destruct (IHc1 _ H1) as (c' & s' & R & E). exists (c' ;; c2), s'; split. apply red_seq_steps_plus; auto. apply cexecinf_seq_1; auto. - exists c2, s'; split. eapply plus_right. apply red_seq_steps. apply cexec_to_reds; eauto. constructor. auto. - do 2 econstructor; split. apply plus_one. constructor. auto. - do 2 econstructor; split. apply plus_one. apply red_while_loop; auto. apply cexecinf_seq_1; auto. - do 2 econstructor; split. eapply plus_right. eapply star_step. apply red_while_loop; auto. apply red_seq_steps. apply cexec_to_reds; eauto. constructor. auto. Qed.
imports: Coq(Arith ZArith Psatz Bool String List) CDF(Sequences IMP Compil) Coq(Classical Description)