proposition: Lemma tc2aif s l1 l2 l3 l4 p1 p2 : validtc2 l1 -> validtc2 l2 -> validto5 l3 -> valid63 p1 -> validto5 l4 -> valid63 p2 -> tc2i l1 l3 p1 s = false -> (l1 <> l2 \/ l3 <> l4 \/ p1 <> p2) -> tc2i l2 l4 p2 (tc2a l1 l3 p1 s) = tc2i l2 l4 p2 s.
proof: Proof. intros Hl1 Hl2 Hl3 Hl4 Hp1 Hp2. case (validtc2_inv _ Hl1); clear Hl1; case (validtc2_inv _ Hl2); clear Hl2. assert (Hpp1: (Zpos p1 <= 63)%Z); auto. assert (Hpp2: (Zpos p2 <= 63)%Z); auto. intros c1 [l5 [H1 [[H2 | H2] Hp]]]; rewrite H1; rewrite H2; clear H1 H2; intros q1 [l6 [H1 [[H2 | H2] Hq]]]; rewrite H1; rewrite H2; clear H1 H2; case s; unfold tc2i, tc2a; auto; intros; rewrite to5aif; auto; repeat match goal with H : _ \/ _ |- _ => case H; clear H; intros H1 end; auto; right; left; intros HH; case H1; subst; auto. Qed.
imports: PrimInt63 Cyclic63 List BasicRubik