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的解。我们提供了严格且经计算机验证的证明。在此过程中，我们列举了完备格上极值不动点的一些已知和新的恒等式及不等式。