proposition: Lemma tc2_get_next_aux_equiv n s s1 s2 l1 l2 l : valid_state s -> valid_pair (s1, s2) -> pstates_equiv (s1,s2) (l1,l2) -> incl l Movel -> get_next_aux n s s1 s2 l = tc2_get_next_aux n s l1 l2 l.
proof: Proof. intros Hg (Hg1, Hg2) (H1, H2); elim l; simpl; auto; clear l. intros a l Hrec Hi; rewrite Hrec; auto with datatypes. rewrite <- (fun x => tc2_get_number_equiv x s1 s2); auto. apply move_valid with s; auto. now apply Movel_move; auto with datatypes. now split; auto. now split; auto. apply incl_tran with (2 := Hi); auto with datatypes. Qed.
imports: PrimInt63 Cyclic63 List BasicRubik Max