ElisTarskiPf
A
Sections
NuprlLIB
Doc
Rank
Theorem
Name
2
Thm*
t:Term. s(t) = SUBX(
t; SUBX(
f(t); UP(
f(t))))
[s1]
cites
1
Thm*
t:Term. closed(t)
[up_term_closed]
ElisTarskiPf
A
Sections
NuprlLIB
Doc
t:Term. s(t) = SUBX(
t; SUBX(f(t); UP(f(t))))t:Term. closed(t)t:Term. s(t) = SUBX(t; SUBX(f(t); UP(f(t))))t:Term. closed(t)