proposition: Lemma iter_true_reachable n : (forall s, valid_state s -> tc2i3 (encode_state s) (fst (iter n)) = true -> nlreachable n s).
proof: Proof. generalize (iter_equiv n) (iters_correct n) (iters_valid n). case (iters n); case (iter n); intros s1 s2 l1 l2; simpl. intros (H1, _) (H2, _) (Hg1, Hg2) s Hg Hs. rewrite <- H2. rewrite <- (in_states_equiv l1 s1 s) in Hs; auto. generalize (in_states_correct s l1); rewrite Hs; auto. Qed.
imports: PrimInt63 Cyclic63 List BasicRubik Max