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.