proposition: Lemma iters_final n : match iters n with | (_, nil) => forall s, reachable s -> nlreachable (pred n) s | _ => True end.
proof: Proof. generalize (iters_correct n). case iters; intros s1 s2. case s2; auto; simpl. case n; simpl; clear n. - intros (H1, H2). case (H2 init_state); intros HH; case HH. split. + apply nreach0. + intros m Hm; contradict Hm; auto with arith. - intros n (H1, H2) s Hs. elim Hs. + exists 0; split; auto with arith. now constructor. + intros s3 HH1 HH2. case (nlreachable_bound (S n) (rright s3)). * case HH2; intros m (Hm, Hm1). exists (S m); split; auto with arith. apply nreachS with s3; auto; unfold move; auto. * intros m (Hm, Hm1). apply Nat.le_lteq in Hm; destruct Hm as [Hm2|Hm2]. -- exists m; split; auto with arith. case Hm1; auto. -- subst m; case (H2 (rright s3)); intros HH _; case (HH Hm1). + intros s3 HH1 HH2. case (nlreachable_bound (S n) (rback s3)). * case HH2; intros m (Hm, Hm1). exists (S m); split; auto with arith. apply nreachS with s3; auto; unfold move; auto. * intros m (Hm, Hm1). apply Nat.le_lteq in Hm; destruct Hm as [Hm2|Hm2]. -- exists m; split; auto with arith. case Hm1; auto. -- subst m; case (H2 (rback s3)); intros HH _; case (HH Hm1). + intros s3 HH1 HH2. case (nlreachable_bound (S n) (rdown s3)). * case HH2; intros m (Hm, Hm1). exists (S m); split; auto with arith. apply nreachS with s3; auto; unfold move; do 3 right; auto. * intros m (Hm, Hm1). apply Nat.le_lteq in Hm; destruct Hm as [Hm2|Hm2]. exists m; split; auto with arith. case Hm1; auto. subst m; case (H2 (rdown s3)); intros HH _; case (HH Hm1). Qed.
imports: ZArith List