proposition: Lemma candidate_list_correct l n : (forall i, (nsreachable n i -> In i l) /\ (In i l -> nlreachable n i)) -> (forall i, (nsreachable (S n) i -> In i (candidate_list l)) /\ (In i (candidate_list l) -> nlreachable (S n) i)).
proof: Proof. assert (F : forall l n i, (forall j, move j i -> nsreachable n j -> In j l) -> nsreachable (S n) i -> In i (candidate_list l)). - intros l1; elim l1; simpl; auto; clear l1. + intros n1 i1 H Hi1. case (move_nsreachable _ _ Hi1); intros j1 (Hj1, Hj2); auto. apply (H j1); auto. + intros s l1 Hrec n1 i1 Hi Hi1. case (move_nsreachable _ _ Hi1); intros j1 (Hj1, Hj2); auto. case (Hi _ Hj1 Hj2); intros HH. * rewrite <-HH in Hj1; unfold move in Hj1; clear HH; intuition. * do 9 match goal with |- context[?X = ?Y] => generalize (state_eq_correct X Y); case state_eq; auto; intros; right end. apply Hrec with n1; auto. intros j Hj3 Hj4. case (Hi _ Hj3 Hj4); auto. intros HH1; rewrite <- HH1 in Hj3. do 8 (case Hj3; intros HH2; contradict HH2; auto; clear Hj3; intros Hj3). - intros H i; split. + intros; apply F with n; auto. intros; case (H j); auto. + assert (H1: forall i, In i l -> nlreachable n i). intros i1; case (H i1); auto. generalize H1; elim l; simpl; auto; clear l H H1. * intros _ HH; case HH. * intros a l Hrec; intros H1. case (H1 a); auto; intros m (Hm, Hm1). intros [HH1 | [HH1 | [HH1 | [HH1 | [HH1 | [HH1 | [HH1 | [HH1 | [HH1 | HH1]]]]]]]]]; try (subst i; exists (S m); split; auto with arith; apply nreachS with (1 := Hm1); unfold move; auto; do 3 right; auto; do 3 right; auto). apply Hrec; auto. Qed.
imports: ZArith List