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的解。我们提供严谨的、计算机验证的证明。在此过程中，我们列举了关于完全格中极值不动点的一系列已知及新的恒等式与不等式。