proposition: Lemma tc2_solve_init n s s1 s2 : (s1, s2) = fst (iter2 n) -> nlreachable n s -> fold_left (fun s a => m2f a s) (tc2_solve n s s1 s2) s = init_state.
proof: Proof. intros H1 H2. rewrite <- (tc2_solve_equiv n s (fst (fst (iter2s n))) (snd (fst (iter2s n))) s1 s2). - apply solve_init; auto. case (fst (iter2s n)); auto. - case (nlreachable_bound _ _ H2); clear H2; intros m (H2, H3). apply nreachable_valid with m; case H3; auto. - generalize (iter2s_valid n). intros (HH1, HH2); auto. - rewrite H1; case (iter2_equiv n); intros HH (HH1, _); split; auto. Qed.
imports: PrimInt63 Cyclic63 List BasicRubik Max