An invariant is a property that holds in a system's initial state and is preserved by every legal transition/move; if a target state lacks that property, the target state is provably unreachable, and invariant proofs are structured as inductive proofs where the inductive hypothesis is the invariant itself, parameterized by the number of moves taken. Strong induction is a proof technique in mathematical logic/discrete mathematics generalizing ordinary induction: to prove P(n+1), one may assume P(0), P(1), ..., P(n) all hold (rather than only P(n)), which does not increase logical proving power but often simplifies proofs, particularly for recursive or divide-and-combine processes where results depend on multiple, variably-sized prior cases rather than a single preceding case.
An invariant is a property that holds in a system's initial state and is preserved by every legal transition/move; if a target state lacks that property, the target state is provably unreachable, and…