structure
definition
def or abbrev
UniversalTM
show as:
view Lean formalization →
formal statement (Lean)
75structure UniversalTM where
76 base : TuringMachine
77 /-- Can simulate any other TM -/
78 universal : Bool := true
proof body
Definition body.
79
80/-- **THEOREM**: A UTM exists.
81
82 Proof: Construct explicit UTM (Turing 1936).
83 Small UTM: (2 states, 18 symbols) or (7 states, 4 symbols). -/