proposition: Theorem make_listtc6ir l p c l1 l2 ll : validtc6 (rev l) -> valid63 p -> tc6i (rev l) c p = true -> In (l ++ l1,l2,p) (tc6it _ make_list l1 l2 ll c).
proof: Proof. assert (H : exists f, f = tc6it). now exists tc6it; auto. case H; intros f Hf; rewrite <- Hf. case c. now unfold tc6i; intros _ _ HH; discriminate. intros cc1 cc2 cc3 cc4 cc5 cc6 HH Hp. case (validtc6_inv _ HH); clear HH. intros p1 (HH, HH1). rewrite <- (rev_involutive l). rewrite HH; simpl rev; clear HH. case HH1; [intros HH2 | intros [HH2 | [HH2 | [HH2 | [HH2 | HH2]]]]]; rewrite HH2; clear HH1 HH2; simpl; intros HH; rewrite Hf; unfold tc6it. - apply make_list63ir; auto. - apply make_list63irI; apply make_list63ir; auto. - do 2 (apply make_list63irI); apply make_list63ir; auto. - do 3 (apply make_list63irI); apply make_list63ir; auto. - do 4 (apply make_list63irI); apply make_list63ir; auto. - do 5 (apply make_list63irI); apply make_list63ir; auto. Qed.
imports: PrimInt63 Cyclic63 List BasicRubik