proposition: Lemma iter2s_aux_nreach n p m ps : p = porder (S m) -> (forall s, In s (fst (fst ps)) <-> exists m1, m1 <= m /\ nsreachable m1 s /\ is_odd (porder m1)) /\ (forall s, In s (snd (fst ps)) <-> exists m1, m1 <= m /\ nsreachable m1 s /\ porder m1 <> 1%positive) /\ (forall s, (nsreachable m s -> In s (snd ps)) /\ (In s (snd ps) -> nlreachable m s)) -> (forall s, In s (fst (fst (iter2s_aux n p ps))) <-> exists m1, m1 <= n + m /\ nsreachable m1 s /\ is_odd (porder m1)) /\ (forall s, In s (snd (fst (iter2s_aux n p ps))) <-> exists m1, m1 <= n + m /\ nsreachable m1 s /\ porder m1 <> 1%positive) /\ (forall s, (nsreachable (n + m) s -> In s (snd (iter2s_aux n p ps))) /\ (In s (snd (iter2s_aux n p ps)) -> nlreachable (n + m) s)).
proof: Proof. revert p m ps; elim n; auto; clear n. intros n Hrec p m (ss1, ss2); simpl fst; simpl snd. rewrite plus_Snm_nSm. intros H1 (H2, (H3, H4)); apply (Hrec (pos_up p) (S m)). rewrite H1; repeat rewrite porderS; auto. apply (fold_next2s_nreach m p (ss1, ss2)); auto. Qed.
imports: ZArith List