NOT.4:5.3 - Keep a cancellation inside the condition that permits it

For real x, consider if x != 0 then x/x else 0. Only the selected branch is evaluated. Within the first branch, division is defined and the quotient is 1, so the expression can become if x != 0 then 1 else 0.

At x = 2 both expressions return 1; at x = 0 both return 0 without evaluating the quotient. More generally, the two branches cover all real inputs and give the same result in each. Replacing the whole expression by 1 would fail at zero. Replacing an unrelated occurrence of x/x outside that guarded branch would also need its own domain condition. The useful transformation follows the local assumption through its scope.