proposition: Theorem infinite_loop_aux : forall (s s':state)(i:inst), exec s i s' -> forall b, i = (WhileDo b Skip) -> evalB s b = Some true -> False.
proof: Proof. intros s s' i Hexec; elim Hexec; try (intros; discriminate). - intros s0 i0 e Heval b Heq; injection Heq; intros Heq1 Heq2; subst; rewrite Heval; intros; discriminate. - intros s0 s1 s2 i0 e Heval Hexeci0 _ Hexecw IHw b Heq; injection Heq; intros Heq1 Heq2 _; subst. apply (IHw b); trivial. inversion Hexeci0; subst; trivial. Qed.
imports: ZArith