fact: Definition valid_state s := match s with | State c1 c2 c3 c4 c5 c6 c7 o1 o2 o3 o4 o5 o6 o7 => perm (C1 :: C2 :: C3 :: C4 :: C5 :: C6 :: C7 :: nil) (c1 :: c2 :: c3 :: c4 :: c5 :: c6 :: c7 :: nil) /\ fold_left oadd (o1 :: o2 :: o3 :: o4 :: o5 :: o6 :: o7 :: nil) O1 = O1 end.
imports: ZArith List