proposition: Lemma diverges_seq_inv: forall s c1 c2, diverges s (c1 ;; c2) -> diverges s c1 \/ exists s', terminates s c1 s' /\ diverges s' c2.
proof: Proof. intros. destruct (terminates_or_diverges c1 s) as [D | (s' & T)]. - auto. - right; exists s'; split; auto. eapply diverges_steps_inv. eauto. eapply star_trans. apply red_seq_steps; eauto. apply star_one; constructor. Qed.
imports: Coq(Arith ZArith Psatz Bool String List) CDF(Sequences IMP Compil) Coq(Classical Description)