ElisTarskiPf
B
Sections
NuprlLIB
Doc
Def
f(t) == SUBX(q(t); SUBX(X; Q(X)))
is mentioned by
Thm*
t:Term. s(t) reps t/(f(t)/q(f(t)))
[s2]
Thm*
t:Term. s(t) = SUBX(q(t); SUBX(q(f(t)); Q(q(f(t)))))
[s1]
Def
s(t) == f(t)/q(f(t))
[s]
ElisTarskiPf
B
Sections
NuprlLIB
Doc
t:Term. s(t) reps t/(f(t)/q(f(t)))t:Term. s(t) = SUBX(q(t); SUBX(q(f(t)); Q(q(f(t)))))t:Term. s(t) reps t/(f(t)/q(f(t)))t:Term. s(t) = SUBX(q(t); SUBX(q(f(t)); Q(q(f(t)))))