proposition: Lemma iter2_equiv n : tstates_equiv (iter2s n) (iter2 n).
proof: Proof. unfold iter2s, iter2. assert (F: tc2it _ make_list nil s0 = (map (fun x => rev3 (encode_state x)) (init_state :: nil))). now apply refl_equal. apply iter2_aux_equiv; simpl; auto. split; [split | idtac]. now intros s [H | H]; try (case H; fail); subst; apply valid_state_init. now intros s HH; case HH. now intros s [H | H]; try (case H; fail); subst; apply valid_state_init. split; [split | idtac]; simpl fst; try rewrite F; auto. split; simpl. now intros s; split; auto. unfold states_equiv. intros s; rewrite F. split; auto. Qed.
imports: PrimInt63 Cyclic63 List BasicRubik Max