Nuprl - Some Definitions

tm_r	`Def p.r == 2of(2of(2of(2of(2of(2of(2of(p)))))))` `Thm* p:PM{i}. p.r (p)`
tm_t	`Def p.t == 1of(2of(2of(2of(2of(2of(2of(p)))))))` `Thm* p:PM{i}. p.t (p)`
tm_s	`Def p.s == 1of(2of(2of(2of(2of(2of(p))))))` `Thm* p:PM{i}. p.s (p)`
tm_delta	`Def (p) == 1of(2of(2of(2of(2of(p)))))` `Thm* p:PM{i}. (p) (p)G(p)(p)G(p)`
tm_blank	`Def _(p) == 1of(2of(2of(2of(p))))` `Thm* p:PM{i}. _(p) G(p)`
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`
tm_q	`Def (p) == 1of(p)` `Thm* p:PM{i}. (p) 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'}`
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`