Progress of well-formed inductive-counting instructions

The controller checks a decreasing progress measure. This file proves that the check succeeds in the intended loop ranges. The check is not an additional graph or reachability oracle.

Main results

• Cslib.InductiveCounting.rank_instruction_lt: legitimate instructions decrease the measure.

References

• M. Sipser, Introduction to the Theory of Computation, Section 8.6

theorem Cslib.InductiveCounting.rank_instruction_lt {N width source : ℕ} {edge : ℕ → ℕ → Bool} {bad : ℕ → Bool} {s : State} (hi : Invariant N edge bad source s) (hh : halted s = false) (choice : Bool) : rank N width (instruction N width source s (answer edge bad s) choice) < rank N width s