(9steps total) PrintForm Definitions Lemmas ElisTarskiPf B Sections NuprlLIB Doc

At: s1 1 2 1
1. t: Term
2. s(t) = f(t)[q(f(t))/X]
s(t) = SUBX(q(t); SUBX(q(f(t)); Q(q(f(t)))))
By: ComputeWithTaggedTerm (s(t) = [ 0: f(t) ][q(f(t))/X]) 2
Generated subgoal:

12. s(t) = SUBX(q(t); SUBX(X; Q(X)))[q(f(t))/X]
s(t) = SUBX(q(t); SUBX(q(f(t)); Q(q(f(t)))))		4 steps

About:
equal

(9steps total) PrintForm Definitions Lemmas ElisTarskiPf B Sections NuprlLIB Doc