proposition: Lemma diverges_to_cexecinf: forall s c, diverges s c -> cexecinf s c.
proof: Proof. cofix CIH; intros s c D. destruct c. - eelim terminates_not_diverges; eauto. apply star_refl. - eelim terminates_not_diverges; eauto. apply star_one. constructor. - destruct (diverges_seq_inv _ _ _ D) as [D1 | (s' & T1 & D2)]. + apply cexecinf_seq_1; auto. + apply cexecinf_seq_2 with s'; auto using reds_to_cexec. - apply infseq_inv in D. destruct D as ((c' & s') & R & D). inversion R; subst. apply cexecinf_ifthenelse; auto. - destruct (diverges_loop_inv _ _ _ D) as (B & [D1 | (s' & T1 & D2)]). + apply cexecinf_while_1; auto. + apply cexecinf_while_2 with s'; auto using reds_to_cexec. Qed.
imports: Coq(Arith ZArith Psatz Bool String List) CDF(Sequences IMP Compil) Coq(Classical Description)