We study operations on fixpoint equation systems (FES) over arbitrary complete lattices. We investigate under which conditions these operations, such as substituting variables by their definition, and swapping the ordering of equations, preserve the solution of a FES. We provide rigorous, computer-checked proofs. Along the way, we list a number of known and new identities and inequalities on extremal fixpoints in complete lattices.

翻译：我们研究任意完备格上不动点方程系统（FES）的运算。我们探究这些运算（例如用变量的定义替换变量，以及交换方程的次序）在何种条件下能保持 FES 的解。我们提供了严格的、可由计算机检验的证明。在此过程中，我们列举了完备格中关于极值不动点的若干已知及新的恒等式与不等式。