fact: Definition next (s : tc2 * tc2) lc lo n := let s1 := decode_state lc lo n in fold_left (fun (s : tc2 * tc2) f => let (states, nstates) := s in let (u, n) := encode_state (f s1) in let (lc , lo) := u in if tc2i lc lo n states then s else let states1 := tc2a lc lo n states in let nstates1 := tc2a lc lo n nstates in (states1, nstates1)) movel s.
imports: PrimInt63 Cyclic63 List BasicRubik