NOT.4:5.1 - Name a repeated construction without capturing another input

A reader wants to see and change the repeated construction in (x + 1) * (x + 1). The expression denotes ordinary integer arithmetic with a fixed input x. Introduce a local definition: let v = x + 1 in v * v. Here let gives v the value of its defining expression within the following body.

At x = 3 the original expression gives 4 * 4 = 16; the new one first obtains v = 4 and then the same result. For any integer x, substitution of v’s definition recovers the original expression, establishing the general equality under this interpretation. To change the repeated construction to x + 2, change the one definition. The new value at x = 3 is 25, and expansion shows both occurrences received that change.

Now use a larger expression u + (x + 1) * (x + 1) with external inputs u = 10 and x = 3. Introducing let u = x + 1 in u + u * u is wrong: it turns the external u into a local reference and produces 20 instead of 26. A fresh v gives let v = x + 1 in u + v * v, which produces 26. The repair changes the binding choice, not the arithmetic law.

The rule applies to the pure arithmetic interpretation supplied here. If each occurrence instead instructs a fresh observation, sharing their results changes the operation. For example, two sensor reads may return 4 and 5, whose product is 20; one read returning 4 reused twice gives 16. Retain two observations unless their consolidation is justified for the intended use.