proposition: Lemma iter2s_correct n : (forall s, In s (fst (fst (iter2s n))) <-> exists m1, m1 <= n /\ nsreachable m1 s /\ is_odd (porder m1)) /\ (forall s, In s (snd (fst (iter2s n))) <-> exists m1, m1 <= n /\ nsreachable m1 s /\ porder m1 <> 1%positive) /\ (forall s, (nsreachable n s -> In s (snd (iter2s n))) /\ (In s (snd (iter2s n)) -> nlreachable n s)).
proof: Proof. unfold iters. pattern n at 2 4 5 8. replace n with (n + 0); auto with arith. unfold iter2s; apply iter2s_aux_nreach; simpl; auto. assert (F1: forall s, nsreachable 0 s -> init_state = s). - intros s (H1, H2); inversion H1; auto. - split. + intros s; split; auto. intros [H1 | H1]. * subst; exists 0; repeat split; auto; try constructor. now intros m Hm; contradict Hm; auto with arith. * case H1; auto. * intros (m1, (Hm1, (Hm2, _))); left. apply F1; generalize Hm1 Hm2; case m1; simpl; auto. intros n1 Hn1; contradict Hn1; auto with arith. + split. * intros s; split; auto. intros HH; case HH. intros (m1, (Hm1, (Hm2, Hm3))). generalize Hm1 Hm3; case m1; simpl; auto. intros n1 Hn1; contradict Hn1; auto with arith. * intros s; split; auto. intros [HH | HH]; subst; try (case HH; fail). exists 0; split; auto; constructor. Qed.
imports: ZArith List