proposition: Lemma iter_aux_equiv n ps ll : valid_pair ps -> pstates_equiv ps ll -> pstates_equiv (iters_aux n ps) (iter_aux n ll).
proof: Proof. revert ps ll; elim n; simpl; clear n; auto. intros n Hrec (ss1, ss2) (ll1, ll2) Hg He. case (fold_next_equiv ss1 ss2 nil ll1 ll2 OTC2); auto with datatypes. - intros s HH; inversion HH. - intros s HH; inversion HH. - intros s; simpl; split; auto. - case (fold_nexts_valid (ss1, ss2) nil); simpl; auto. intros s HH; inversion HH. match goal with |- context[fold_left ?X ?Y ?Z] => set (u := fold_left X Y Z) end. match goal with |- context[fold_left ?X ?Y ?Z] => change (fold_left X Y Z) with u; case u end. intros ss3 ss4. match goal with |- context[tc2it _ ?X ?Y ?Z] => case (tc2it _ X Y Z) end. simpl; intros ll3 ll4 Hg3 Hg4 He3 He4. apply Hrec; auto; split; auto. Qed.
imports: PrimInt63 Cyclic63 List BasicRubik Max