Theorems · Inductive type · logic and foundations

Turing.TM2.Cfg

{K : Type u_1} → (K → Type u_2) → Type u_3 → Type u_4 → Type (max (max (max u_1 u_2) u_3) u_4)

A configuration in the TM2 model is a label (or none for the halt state), the state of local variables, and the stacks. (Note that the stacks are not ListBlanks, they have a definite size.)

Defined in

Mathlib.Computability.TuringMachine.StackTuringMachine

Cited by

22 results in Mathlib

Foundations

Depth 0 from the axioms · uses no axioms