proposition: Theorem make_list63i l1 l2 c k ll : In k (int63it _ make_list l1 l2 ll c) -> In k ll \/ exists p, (Zpos p <= 63)%Z /\ k = (l1,l2,p) /\ int63i c p = true.
proof: Proof. rewrite int63it_naive; unfold naive_int63it; generalize l1 l2 c k ll; clear l1 l2 c k ll. assert(F: forall m p l1 l2 c k ll, (Z_of_nat m + Zpos p = 63)%Z -> In k (naive_int63it_aux _ make_list m p c l1 l2 ll) -> In k ll \/ exists p1 : positive, (Zpos p <= Zpos p1 <= 63)%Z /\ k = (l1,l2,p1) /\ int63i c p1 = true). - intros m; elim m; clear m. + intros p l1 l2 c k ll1 H. rewrite naive_aux0. case_eq (int63i c p); intros Heq Hf; auto. case (in_app_or _ _ _ Hf); auto. simpl In; intros [H2 | H2]; try (case H2; fail); auto. right; exists p; auto with zarith. + intros m Hrec p l1 l2 c k ll H. rewrite naive_auxS. assert (F1: (Z_of_nat m + (Zpos (Pos.succ p)) = 63)%Z). rewrite <- H. now rewrite inj_S; rewrite Zpos_succ_morphism; auto with zarith. case_eq (int63i c p); intros H1. intros HH; case (Hrec _ _ _ _ _ _ F1 HH). intros HH1; case (in_app_or _ _ _ HH1); auto. simpl In; intros HH2; case HH2; intros HH3; auto. now right; exists p; split; auto with zarith. now case HH3; auto. intros [p1 [Hk1 [Hk2 Hk3]]]. right; exists p1; split; auto with zarith. intros HH; case (Hrec _ _ _ _ _ _ F1 HH); auto. intros [p1 [Hk1 [Hk2 Hk3]]]. right; exists p1; split; auto with zarith. - intros l1 l2 c k ll H. case (F 62%nat 1%positive l1 l2 c k ll). + reflexivity. + exact H. + intros HH; left; exact HH. + intros [p [Hp1 [Hp2 Hp3]]]; right; exists p; split. now case Hp1; intros _ HH1; exact HH1. split; assumption. Qed.
imports: PrimInt63 Cyclic63 List BasicRubik