Definition. The \textbf {fix} operator [dt-001Q]
Let \textbf {fix}(f) denote the least fixed point of the continuous function f, that is \bigsqcup _{n\in \mathbb {N}}f^{n}(\bot ), guaranteed to exist by Theorem [dt-001P].
Let \textbf {fix}(f) denote the least fixed point of the continuous function f, that is \bigsqcup _{n\in \mathbb {N}}f^{n}(\bot ), guaranteed to exist by Theorem [dt-001P].