proposition: Lemma tc5aif s l1 l2 p1 p2 : validtc5 l1 -> validtc5 l2 -> valid63 p1 -> valid63 p2 -> tc5i l1 s p1 = false -> (l1 <> l2 \/ p1 <> p2) -> tc5i l2 (tc5a l1 s p1) p2 = tc5i l2 s p2.
proof: Proof. intros Hl1 Hl2 Hp1 Hp2; case (validtc5_inv _ Hl1); clear Hl1; case (validtc5_inv _ Hl2); clear Hl2. assert (Hpp1: (Zpos p1 <= 63)%Z); auto. assert (Hpp2: (Zpos p2 <= 63)%Z); auto. intros c1 [l3 [H1 [[H2 | [H2 | [H2 | [H2 | H2]]]] Hp]]]; rewrite H1; rewrite H2; clear H1 H2; intros q1 [l4 [H1 [[H2 | [H2 | [H2 | [H2 | H2]]]] Hq]]]; rewrite H1; rewrite H2; clear H1 H2; case s; unfold tc5i, tc5a; auto; intros; rewrite tc6aif; auto; try (match goal with H : _ \/ _ |- _ => case H end; auto; intros HH; left; intros HH1; case HH; rewrite HH1; auto). Qed.
imports: PrimInt63 Cyclic63 List BasicRubik