t 
= t SUBX(f(t); UP(f(t))) = SUBX(f(t); f(t))
SUBX(t; SUBX(f(t); UP(f(t)))) = SUBX(t; SUBX(f(t); f(t)))
t,r,t',r':Term. t = t' & r = r' 
SUBX(t; r) = SUBX(t'; r')
| 1 | t = t | 1 step |
| 2 | SUBX(f(t); UP(f(t))) = SUBX(f(t); f(t)) | 4 steps |
About:
 |  |  |