let normal_form ({ litterals = sa; array = ar } as c) = let vars = Variable.Set.elements (SAtom.variables_proc sa) in if !size_proc <> 0 && List.length vars > !size_proc then cube_false else let sigma = Variable.build_subst vars Variable.procs in if Variable.is_subst_identity sigma then c else let new_vars = List.map snd sigma in let new_ar = ArrayAtom.apply_subst sigma ar in let new_sa = ArrayAtom.to_satom new_ar in { vars = new_vars; litterals = new_sa; array = new_ar; }