proposition: Lemma l11_ok: l11 = OTC2.
proof: Proof. native_cast_no_check (refl_equal OTC2). Time Qed. Lemma s11_correct: (s11, OTC2) = iter 12. Proof. apply trans_equal with (s11,l11). apply f_equal2 with (f := @pair _ _). now apply refl_equal. apply sym_equal. now exact l11_ok. exact s11_l11. Time Qed. Lemma reach11 s : reachable s -> nlreachable 11 s. Proof. revert s. assert (F1: forall n ss, (ss, OTC2) = iter (S n) -> forall s, reachable s -> nlreachable n s). intros n ss Hss s Hs; generalize Hss (iter_final (S n)); case iter. intros s1 s2; case s2; auto. now intros t1 t2 HH; discriminate HH. intros; apply F1 with s11. now exact s11_correct. exact H. Qed.
imports: PrimInt63 List BasicRubik Rubik63