proposition: Theorem make_listtc2i c k ll : In k (tc2it _ make_list ll c) -> In k ll \/(exists l3, exists l4, exists p, k = (l3,l4,p) /\ validtc2 (rev l3) /\ validto5 (rev l4) /\ valid63 p /\ tc2i (rev l3) (rev l4) p c = true).
proof: Proof. unfold tc2it; case c. now intros HH; left; assumption. intros cc1 cc2. set (ll1 := (to5it _ make_list (C2 :: nil) nil ll cc2)). set (ll2 := (to5it _ make_list (C1 :: nil) nil ll1 cc1)). intros H. case (make_listto5i _ _ _ _ _ H); clear H; unfold ll2; intros H. - case (make_listto5i _ _ _ _ _ H); clear H; unfold ll1; intros H. now left; assumption. case H; intros l3 (l4, (p, (Hp1, (Hp2, (Hp3, (Hp4, Hp5)))))). right; rewrite Hp1. exists (l3 ++ (C2 :: nil)); exists l4; exists p; split. now rewrite <- app_nil_end; reflexivity. split. rewrite rev_unit; unfold validtc2, valid63; auto. split; [idtac | split]; auto. rewrite rev_unit; unfold tc2i; exact Hp5. - case H; intros l3 (l4, (p, (Hp1, (Hp2, (Hp3, (Hp4, Hp5)))))). right; rewrite Hp1. exists (l3 ++ (C1 :: nil)); exists l4; exists p; split. rewrite <- app_nil_end; reflexivity. split. rewrite rev_unit; unfold validtc2, valid63; auto. split; [idtac | split]; auto. rewrite rev_unit; unfold tc2i; exact Hp5. Qed.
imports: PrimInt63 Cyclic63 List BasicRubik