proposition: Theorem make_listto5i l1 l2 c k ll : In k (to5it _ make_list l1 l2 ll c) -> In k ll \/(exists l3, exists l4, exists p, k = (l3++l1,l4++l2,p) /\ validtc4 (rev l3) /\ validto5 (rev l4) /\ valid63 p /\ to5i (rev l4) c (rev l3) p = true).
proof: Proof. unfold to5it; case c. intros HH; left; assumption. intros cc1 cc2 cc3. set (ll1 := (to4it _ make_list l1 (O3 :: l2) ll cc3)). set (ll2 := (to4it _ make_list l1 (O2 :: l2) ll1 cc2)). set (ll3 := (to4it _ make_list l1 (O1 :: l2) ll2 cc1)). intros H. case (make_listto4i _ _ _ _ _ H); clear H; unfold ll3; intros H. - case (make_listto4i _ _ _ _ _ H); clear H; unfold ll2; intros H. + case (make_listto4i _ _ _ _ _ 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; exists (l4 ++ (O3 :: nil)); exists p; split; [rewrite app_ass | split]; auto; rewrite rev_unit. split; [red; auto | split; auto]. simpl; red in Hp3; rewrite Hp3; auto. + case H; intros l3 (l4, (p, (Hp1, (Hp2, (Hp3, (Hp4, Hp5)))))). right; rewrite Hp1. exists l3; exists (l4 ++ (O2 :: nil)); exists p; split; [rewrite app_ass | split]; auto; rewrite rev_unit. split; [red; auto | split; auto]. simpl; red in Hp3; rewrite Hp3; auto. - case H; intros l3 (l4, (p, (Hp1, (Hp2, (Hp3, (Hp4, Hp5)))))). right; rewrite Hp1. exists l3; exists (l4 ++ (O1 :: nil)); exists p; split; [rewrite app_ass | split]; auto; rewrite rev_unit. split; [red; auto | split; auto]. simpl; red in Hp3; rewrite Hp3; auto. Qed.
imports: PrimInt63 Cyclic63 List BasicRubik