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