proposition: Lemma tc6aif: forall s l1 l2 p1 p2, validtc6 l1 -> validtc6 l2 -> valid63 p1 -> valid63 p2 -> tc6i l1 s p1 = false -> (l1 <> l2 \/ p1 <> p2) -> tc6i l2 (tc6a l1 s p1) p2 = tc6i l2 s p2.
proof: Proof. intros s l1 l2 p1 p2 Hl1 Hl2 Hp1 Hp2; case (validtc6_inv _ Hl1); clear Hl1; case (validtc6_inv _ Hl2); clear Hl2. assert (Hpp1: (Zpos p1 <= 63)%Z); auto. assert (Hpp2: (Zpos p2 <= 63)%Z); auto. intros c1 [H1 [H2 | [H2 | [H2 | [H2 | [H2 | H2]]]]]]; rewrite H1; rewrite H2; clear H1 H2; intros c2 [H1 [H2 | [H2 | [H2 | [H2 | [H2 | H2]]]]]]; rewrite H1; rewrite H2; clear H1 H2; case s; unfold tc6i, tc6a; try (intros; apply int63_0; auto with zarith); ((intros i1 i2 i3 i4 i5 i6 H1 [HH | HH]) || (intros _ [HH | HH])); try match goal with H : ?X <> ?X |- _ => case H; trivial end; rewrite ?int63aif; auto with zarith; apply int63_0; auto. Qed.
imports: PrimInt63 Cyclic63 List BasicRubik