Turing Sections NuprlLIB Doc

Def P(p) == 1of(2of(2of(p)))

Thm* p:PM{i}. (p) (p)(P(p)+P(p))(p)(P(p)+P(p)) tm_delta_proto

Thm* p:PM{i}. _(p) Void+P(p) blank_proto_pi