proposition: Lemma iters_correct n : (forall s, In s (fst (iters n)) <-> nlreachable n s) /\ (forall s, (nsreachable n s -> In s (snd (iters n))) /\ (In s (snd (iters n)) -> nlreachable n s)).
proof: Proof. unfold iters. pattern n at 2 3 6. replace n with (n + 0); auto with arith. apply iters_aux_nreach; simpl. assert (F1: forall s, nlreachable 0 s -> init_state = s). - intros s (m, Hm); generalize Hm; case m; clear m Hm. + intros (_, HH); inversion HH; auto. + intros n1 (Hn1, _); contradict Hn1; auto with arith. - split; intros s; split; auto. + intros [H1 | H1]. * now subst s; exists 0; split; auto; constructor. * now case H1. + intros H1; left; apply F1. now exists 0; split; auto; case H1; auto. + intros [H1 | H1]. * now subst s; exists 0; split; auto; constructor. * now case H1. Qed.
imports: ZArith List