proposition: Lemma terminates_or_diverges: forall c s, diverges s c \/ exists s', terminates s c s'.
proof: Proof. intros. destruct (classic (all_seq_inf red (c, s))). - left. apply infseq_if_all_seq_inf; auto. - apply not_all_ex_not in H. destruct H as ((c' & s') & H). apply imply_to_and in H. destruct H as [STAR H]. destruct (red_progress c' s') as [E | (c'' & s'' & RED)]. subst c'. right; exists s'; auto. elim H; exists (c'', s''); auto. Qed.
imports: Coq(Arith ZArith Psatz Bool String List) CDF(Sequences IMP Compil) Coq(Classical Description)