MachineDecisionInput.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The machine-theoretic published input for the decision corollaries.

A. M. Turing, On computable numbers, with an application to the Entscheidungsproblem, Proc. London Math. Soc. (2) 42 (1936–1937), 230–265, Section 8, printed p.248: undecidability of ever printing a designated symbol. No fluid event, force compiler, or geometric conclusion is assumed.

def OAI.ForcedComputation.FiniteMachineHaltingUndecidable line 17
Source documentation
The standard halting undecidability specialization to finite one-tape machine tables. Correctness is required on every well-formed finite input.
```
def FiniteMachineHaltingUndecidable : Prop :=
…
```
def OAI.ForcedComputation.NoCompiledInputDecider line 23
Source documentation
No total algorithm on the finite source descriptions decides the given observation for all valid compiled inputs.
```
def NoCompiledInputDecider
    (event : (I : Alternating.MachineInput) → Alternating.ValidInput I → Prop) : Prop :=
…
```
Mentions: OAI.Alternating.MachineInput, OAI.Alternating.ValidInput
theorem OAI.ForcedComputation.noCompiledInputDecider_of_halting line 28