proposition: Lemma fold_next2s_nreach n p ps : p = porder (S n) -> (forall s, In s (fst (fst ps)) <-> exists m, m <= n /\ nsreachable m s /\ is_odd (porder m)) /\ (forall s, In s (snd (fst ps)) <-> exists m, m <= n /\ nsreachable m s /\ porder m <> 1%positive) /\ (forall s, (nsreachable n s -> In s (snd ps)) /\ (In s (snd ps) -> nlreachable n s)) -> (forall s, In s (fst (fst (fold_left (next2s p) (snd ps) (fst ps,nil)))) <-> exists m, m <= S n /\ nsreachable m s /\ is_odd (porder m)) /\ (forall s, In s (snd (fst (fold_left (next2s p) (snd ps) (fst ps,nil)))) <-> exists m, m <= S n /\ nsreachable m s /\ porder m <> 1%positive) /\ (forall s, (nsreachable (S n) s -> In s (snd (fold_left (next2s p) (snd ps) (fst ps,nil)))) /\ (In s (snd (fold_left (next2s p) (snd ps) (fst ps,nil))) -> nlreachable (S n) s)).
proof: Proof. destruct ps as (ss1, ss2). unfold next2s. rewrite fold_left_comb with (f := fun (y: state) (y1: state -> state) => y1 y) (g := filter2s p). match goal with |- context[fold_right ?X ?Y ?Z] => change (fold_right X Y Z) with (candidate_list Z) end; fold filters. simpl fst; simpl snd. intros Hn (H1, (H2, H3)); generalize (filter2s_correct p (ss1, nil) (candidate_list ss2)); case (fold_left (filter2s p) (candidate_list ss2) (ss1, nil)). intros ss4 ss5; simpl; intros (H4, (H5, H6)). split; [idtac | split]. - intros s; apply iff_trans with (1:= H4 s). split. + generalize (in_states_correct s (fst ss1)); case in_states; intros He. * intros _; case (H1 s); intros HH _. case (HH He); intros m (Hm1, (Hm2, Hm3)). exists m; repeat (split; auto with arith). * intros [H7 | (H8, (H9, H10))]. -- case He; auto. -- assert (H11 := candidate_list_correct ss2 n). case (fun x => H11 x s); auto. intros _ H12; generalize (H12 H9); clear H11 H12; intros H11. case (nlreachable_bound _ _ H11); intros m (Hm, Hm1). apply Nat.le_lteq in Hm; destruct Hm as [Hm2|Hm2]. ++ case (porder_inv1 m); intros Hm3. ** case H8; rewrite H2; exists m; auto with arith. ** case He; rewrite H1; exists m; auto with arith. ++ subst; exists (S n); repeat (split; auto). + rewrite Hn; auto. intros (m, (Hm1, (Hm2, Hm3))). apply Nat.le_lteq in Hm1; destruct Hm1 as [Hm1|Hm1]. * left. rewrite H1; exists m; auto with arith. * subst; right; split; auto. -- rewrite H2. intros (m1, (Hm4, (Hm5, Hmm6))). contradict Hm4. rewrite (nsreachable_unique _ _ _ Hm5 Hm2); auto with arith. -- split; auto. assert (H11 := candidate_list_correct ss2 n). case (fun x => H11 x s); auto. - intros s; apply iff_trans with (1:= H5 s). split. + generalize (in_states_correct s (snd ss1)); case in_states; intros He. * intros _; case (H2 s); intros HH _. case (HH He); intros m (Hm1, (Hm2, Hm3)). exists m; repeat (split; auto with arith). * intros [H7 | (H8, (H9, H10))]. -- case He; auto. -- assert (H11 := candidate_list_correct ss2 n). case (fun x => H11 x s); auto. intros _ H12; generalize (H12 H9); clear H11 H12; intros H11. case (nlreachable_bound _ _ H11); intros m (Hm, Hm1). apply Nat.le_lteq in Hm; destruct Hm as [Hm2|Hm2]. ++ case (porder_inv1 m); intros Hm3. ** case He; rewrite H2; exists m; auto with arith. ** case H8; rewrite H1; exists m; auto with arith. ++ subst; exists (S n); repeat (split; auto). + rewrite Hn; auto. intros (m, (Hm1, (Hm2, Hm3))). apply Nat.le_lteq in Hm1; destruct Hm1 as [Hm1|Hm1]. * left. rewrite H2; exists m; auto with arith. * subst; right; split; auto. -- rewrite H1. intros (m1, (Hm4, (Hm5, Hmm6))). contradict Hm4; rewrite (nsreachable_unique _ _ _ Hm5 Hm2); auto with zarith. -- split; auto. assert (H11 := candidate_list_correct ss2 n). case (fun x => H11 x s); auto. - intros s; split; rewrite H6; intros Hg. + right; split; [idtac | split]; auto. * rewrite H1; intros (m, (Hm, (Hm1, _))). case Hg; intros _ HH; case (HH m); auto with arith. case Hm1; auto. * rewrite H2; intros (m, (Hm, (Hm1, _))). case Hg; intros _ HH; case (HH m); auto with arith. case Hm1; auto. * case (fun x => candidate_list_correct ss2 n x s); auto. + case Hg; [intros HH; case HH | intros (G1, (G2, G3))]. case (fun x => candidate_list_correct ss2 n x s); auto. Qed.
imports: ZArith List