FiniteMachineHaltingDischarge.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Discharge of the finite-table undecidability input, using the fixed universal interpreter and Mathlib's proved halting theorem.