proposition: Lemma diverges_loop_inv: forall s b c, diverges s (WHILE b c) -> beval b s = true /\ (diverges s c \/ exists s', terminates s c s' /\ diverges s' (WHILE b c)).
proof: Proof. intros. apply infseq_inv in H. destruct H as ((c1 & s1) & R1 & INF1). inversion R1; subst. - elim (terminates_not_diverges s1 SKIP s1); auto. apply star_refl. - split; auto. destruct (terminates_or_diverges c s1) as [D | (s2 & T)]. + auto. + right; exists s2; 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)