proposition: Theorem make_listto1i l1 l2 c k ll : In k (to1it _ make_list l1 l2 ll c) -> In k ll \/(exists l3, exists l4, exists p, k = (l3++l1,l4++l2,p) /\ validtc4 (rev l3) /\ validto1 (rev l4) /\ valid63 p /\ to1i (rev l4) c (rev l3) p = true).
proof: Proof. revert ll; unfold to1it; case c. now intros ll HH; left; assumption. intros cc1 cc2 cc3 ll. set (ll1 := (tc4it _ make_list l1 (O3 :: l2) ll cc3)). set (ll2 := (tc4it _ make_list l1 (O2 :: l2) ll1 cc2)). set (ll3 := (tc4it _ make_list l1 (O1 :: l2) ll2 cc1)). intros H. case (make_listtc4i _ _ _ _ _ H); clear H; unfold ll3; intros H. - case (make_listtc4i _ _ _ _ _ H); clear H; unfold ll2; intros H. + case (make_listtc4i _ _ _ _ _ H); clear H; unfold ll1; intros H. now left; assumption. case H; intros l3 (p, (Hp1, (Hp2, (Hp3, Hp4)))). right; rewrite Hp1. exists l3; exists (O3 :: nil); exists p; split; [auto | split; auto]. split; [red; auto | split; auto]. + case H; intros l3 (p, (Hp1, (Hp2, (Hp3, Hp4)))). right; rewrite Hp1. exists l3; exists (O2 :: nil); exists p; split; [auto | split; auto]. split; [red; auto | split; auto]. - case H; intros l3 (p, (Hp1, (Hp2, (Hp3, Hp4)))). right; rewrite Hp1. exists l3; exists (O1 :: nil); exists p; split; [auto | split; auto]. split; [red; auto | split; auto]. Qed.
imports: PrimInt63 Cyclic63 List BasicRubik