Library / Mathematical Thinking DPF
Jump to passage
In this reading

Link to current text

Published source confirmed at last check

Source changed 2026-10-03 11:52:20 UTC · snapshot created 2026-10-03 11:53:41 UTC · last check 2026-10-03 12:25:14 UTC

MATH.11:4.4 - Prove the consequence for a sequence

Let a=x0 → x1 → … → xm be any finite allowed sequence. Preservation gives:

I(xm)=I(xm-1)=...=I(x0)=I(a).

Equivalently, use induction on the number of steps: the zero-step state has value I(a), and one more preserving step keeps that value.

Now use the relation. If I(b)≠I(a), no finite allowed sequence reaches b. If an invariant equation determines an output quantity from other known quantities, derive that output under the equation’s conditions. When several invariants are retained, every component must agree.

For a set of initial states, compare the target’s invariant value with the values of I on that set.