proposition: Lemma iter2_aux_equiv n p ps ll : valid_triple ps -> tstates_equiv ps ll -> tstates_equiv (iter2s_aux n p ps) (iter2_aux n p ll).
proof: Proof. revert p ps ll. elim n; simpl; clear n; auto. intros n Hrec p (ss1, ss2) (ll1, ll2) Hg He. case (fold_next2_equiv p ss1 ss2 nil ll1 ll2 OTC2); auto with datatypes. now intros s HH; inversion HH. now intros s HH; inversion HH. now intros s; simpl; split; auto. case (fold_next2s_valid p (ss1, ss2) nil); simpl; auto. now intros s HH; inversion HH. match goal with |- context[fold_left ?X ?Y ?Z] => case (fold_left X Y Z) 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