Turing
Sections
NuprlLIB
Doc
Def
(p) == 1of(2of(2of(2of(2of(p)))))
Thm*
p:PM{i}.
(p)
(p)
(P
(p)+P
(p))
(p)
(P
(p)+P
(p))
tm_delta_proto
(p) == 1of(2of(2of(2of(2of(p)))))
p:PM{i}. (p) 
(p)
(P
(p)+P
(p))
(p)(P(p)+P(p))
tm_delta_proto