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