proposition: Theorem make_listtc6i l1 l2 c k ll : In k (tc6it _ make_list l1 l2 ll c) -> In k ll \/(exists l3, exists p, k = (l3 ++ l1,l2,p) /\ validtc6 (rev l3) /\ valid63 p /\ tc6i (rev l3) c p = true).
proof: Proof. revert ll; unfold tc6it; case c. now intros ll HH; left; assumption. intros cc1 cc2 cc3 cc4 cc5 cc6 ll. set (ll1 := (int63it _ make_list (C6 :: l1) l2 ll cc6)). set (ll2 := (int63it _ make_list (C5 :: l1) l2 ll1 cc5)). set (ll3 := (int63it _ make_list (C4 :: l1) l2 ll2 cc4)). set (ll4 := (int63it _ make_list (C3 :: l1) l2 ll3 cc3)). set (ll5 := (int63it _ make_list (C2 :: l1) l2 ll4 cc2)). intros H. case (make_list63i _ _ _ _ _ H); clear H; unfold ll5; intros H. - case (make_list63i _ _ _ _ _ H); clear H; unfold ll4; intros H. + case (make_list63i _ _ _ _ _ H); clear H; unfold ll3; intros H. * case (make_list63i _ _ _ _ _ H); clear H; unfold ll2; intros H. -- case (make_list63i _ _ _ _ _ H); clear H; unfold ll1; intros H. ++ case (make_list63i _ _ _ _ _ H); clear H; intros H. ** left; assumption. ** case H; intros p (Hp1, (Hp2, Hp3)). right; rewrite Hp2. exists (C6 :: nil); exists p; split. now reflexivity. split. now unfold validtc6, valid63, rev, app; auto. now split; auto with zarith. ++ case H; intros p (Hp1, (Hp2, Hp3)). right; rewrite Hp2. exists (C5 :: nil); exists p; split. now reflexivity. split. now unfold validtc6, valid63, rev, app; auto. split; auto. -- case H; intros p (Hp1, (Hp2, Hp3)). right; rewrite Hp2. exists (C4 :: nil); exists p; split. now reflexivity. split. now unfold validtc6, valid63, rev, app; auto. split; auto. * case H; intros p (Hp1, (Hp2, Hp3)). right; rewrite Hp2. exists (C3 :: nil); exists p; split. now reflexivity. split. now unfold validtc6, valid63, rev, app; auto. split; auto. + case H; intros p (Hp1, (Hp2, Hp3)). right; rewrite Hp2. exists (C2 :: nil); exists p; split. now reflexivity. split. unfold validtc6, valid63, rev, app; simpl; auto with arith. split; auto. - case H; intros p (Hp1, (Hp2, Hp3)). right; rewrite Hp2. exists (C1 :: nil); exists p; split. now reflexivity. split. now unfold validtc6, valid63, rev, app; auto with arith. split; auto. Qed.
imports: PrimInt63 Cyclic63 List BasicRubik