proposition: Lemma cexecinf_to_diverges: forall s c, cexecinf s c -> diverges s c.
proof: Proof. intros. set (X := fun cs => cexecinf (snd cs) (fst cs)). red. apply (infseq_coinduction_principle X). - intros (c1 & s1) D. destruct (cexecinf_productive _ _ D) as (c2 & s2 & P & D'). exists (c2, s2); auto. - auto. Qed.
imports: Coq(Arith ZArith Psatz Bool String List) CDF(Sequences IMP Compil) Coq(Classical Description)