Turing Sections NuprlLIB Doc

conf_st Def t.st == 1of(t)

Thm* M:PM{i}, t:Config(M). t.st (M)

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

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