fact: Definition decode_state lc lo n := match lc, lo with | p6 :: p5 :: p4 :: p2 :: nil, o1 :: o2 :: o3 :: o4 :: o5 :: nil => let (pp, p7) := cube3_decode n in let (o6, p3) := pp in let o7 := oinv (oadd o1 (oadd o2 (oadd o3 (oadd o4 (oadd o5 o6))))) in match decode_memo (p7 :: p6 :: p5 :: p4 :: p3 :: p2 :: C1 :: nil) with i7 :: i6 :: i5 :: i4 :: i3 :: i2 :: i1 :: nil => State i7 i6 i5 i4 i3 i2 i1 o1 o2 o3 o4 o5 o6 o7 | _ => init_state end | _, _ => init_state end.
imports: PrimInt63 Cyclic63 List BasicRubik