···1414And the second definition above results in the failure of this equation that removes redundant checks:
1515##{\mathsf{ite}(b,x,x) = x}
1616}
1717-\li{ The power domain construction (TODO) does not generalise to complete lattices, so semantics for non-deterministic programs are difficult in this setting. }
1717+\li{ The [powerdomain construction](dt-0061) does not generalise to complete lattices, so semantics for [non-deterministic](dt-005U) programs are difficult in this setting. }
1818}}