proposition: Lemma s11_all : tc2all s11 = true.
proof: Proof. native_cast_no_check (refl_equal true). Time Qed. Lemma valid11 s : valid_state s -> reachable s. Proof. revert s. assert (F1: forall n ss, (ss, OTC2) = iter n -> tc2all ss = true -> forall s, valid_state s -> reachable s). intros n ss Hss Hc s Hs. apply nlreachable_reachable with n; auto. apply (iter_true_reachable n s Hs). rewrite <- Hss; simpl fst. generalize (encode_valid _ Hs); case (encode_state s). intros (l1,l2) p (Hp1, (Hp2, Hp3)). now apply checktc2_all; auto. intros s Hs. exact (F1 12%nat s11 s11_correct s11_all s Hs). Qed.
imports: PrimInt63 List BasicRubik Rubik63