proposition: Lemma get_next_init n s1 s2 : (s1, s2) = fst (iter2s n) -> get_next init_state s1 s2 = None.
proof: Proof. generalize (iter2s_correct n) (fun n1 s => get_number_correct n n1 s s1 s2); case iter2s. intros (s3, s4) ss; simpl; intros (H1, (H2, H3)) Hn HH. injection HH; intros; subst s3 s4; clear HH. unfold get_next. replace (get_number init_state s1 s2) with 1%positive. - simpl pos_down. generalize (get_next_aux_correct 3 init_state s1 s2 Movel); case get_next_aux; auto. intros a (Ha, Ha1). generalize Ha1; unfold get_number. generalize (in_states_correct (m2f a init_state) s1); case in_states; intros G1. rewrite H1 in G1. case G1; intros k (Hk, (Hk1,Hk2)). generalize (in_states_correct (m2f a init_state) s2); case in_states; intros G2; auto. + rewrite H2 in G2. case G2; intros k1 (Hk3, (Hk4,Hk5)). case (porder_move init_state (m2f a init_state) 0 k); auto. * split; try apply nreach0; intros m Hm; contradict Hm; auto with arith. * apply Movel_move; auto. * intros HH; subst k. case (porder_move init_state (m2f a init_state) 0 k1); auto. -- split; try apply nreach0; intros m Hm; contradict Hm; auto with arith. -- apply Movel_move; auto. -- intros HH; subst k1. case Hk5; simpl; auto. -- intros HH; case HH; clear HH; intros HH; try discriminate; subst k1. absurd (0 = 1); auto with arith. apply nsreachable_unique with (1 := Hk1); auto. * intros HH; case HH; clear HH; intros HH; try discriminate; subst k. case Hk2; simpl; auto. + intros; discriminate. + case in_states; intros; discriminate. - unfold get_number. generalize (in_states_correct init_state s1); case in_states; intros G1. + generalize (in_states_correct init_state s2); case in_states; intros G2; auto. rewrite H2 in G2. case G2; intros k (Hk, (Hk1,Hk2)). assert (k = 0); subst. apply nsreachable_unique with init_state; auto. split; try apply nreach0; intros m Hm; contradict Hm; auto with arith. case Hk2; auto. + case G1; rewrite H1; exists 0; repeat (split; auto with arith); try constructor. intros m Hm; contradict Hm; auto with arith. Qed.
imports: ZArith List