Validating a finite Mathlib machine's input

A DFA scans the binary input without changing it. Accepted inputs are rewound and passed to the source machine. Rejected inputs halt at the first blank, so their complete right-of-head output is empty.

inductive Complexity.MathlibTM0.BinaryMachine.GuardState (σ Q : Type) : Type

Control for input validation, rewinding, and source execution.

• scan {σ Q : Type} : σ → GuardState σ Q

  Scan the input using a DFA state.

• rewind {σ Q : Type} : GuardState σ Q

  Return to the blank preceding the input.

• run {σ Q : Type} : Q → GuardState σ Q

  Execute a source state.

@[instance_reducible]

instance Complexity.MathlibTM0.BinaryMachine.instFintypeGuardState {σ✝ Q✝ : Type} [Fintype σ✝] [Fintype Q✝] : Fintype (GuardState σ✝ Q✝)

Equations

• Complexity.MathlibTM0.BinaryMachine.instFintypeGuardState = Fintype.ofEquiv (σ✝ ⊕ Unit ⊕ Q✝) (Complexity.MathlibTM0.BinaryMachine.GuardState.proxyTypeEquiv σ✝ Q✝)

@[reducible, inline]

noncomputable abbrev Complexity.MathlibTM0.BinaryMachine.guarded (M : BinaryMachine) {σ : Type} [Fintype σ] (D : DFA Bool σ) : BinaryMachine

A DFA check followed by the original machine on accepted inputs.

Equations

• One or more equations did not get rendered due to their size.