Thms Turing Sections NuprlLIB Doc

tm_blank Def _(p) == 1of(2of(2of(2of(p))))

Thm* p:PM{i}. _(p) G(p)

tm_gamma Def G(p) == P(p)+P(p)

Thm* M:PM{i}. G(M) Type

proto_machine Def PM{i} == q:Type proto_sigma:Type proto_pi:Type(Void+proto_pi)(q(proto_sigma+proto_pi)q(proto_sigma+proto_pi))qqq

Thm* PM{i} Type{i'}

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

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

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

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

pi2 Def 2of(t) == t.2

Thm* B:(AType), p:a:AB(a). 2of(p) B(1of(p))

pi1 Def 1of(t) == t.1

Thm* B:(AType), p:a:AB(a). 1of(p) A