proposition: Lemma terminates_not_diverges: forall s c s', terminates s c s' -> diverges s c -> False.
proof: Proof. intros. assert (D: diverges s' SKIP). { eapply diverges_steps_inv; eauto. } apply infseq_inv in D. destruct D as (b & R & I). inversion R. Qed.
imports: Coq(Arith ZArith Psatz Bool String List) CDF(Sequences IMP Compil) Coq(Classical Description)