q(t) reps t SUBX(q(f(t)); Q(q(f(t)))) reps f(t)/q(f(t))
SUBX(q(t); SUBX(q(f(t)); Q(q(f(t))))) reps t/(f(t)/q(f(t)))
t,r,t',r':Term. t reps t' & r reps r' 
SUBX(t; r) reps t'/r'
| 1 | q(t) reps t | 1 step |
| 2 | SUBX(q(f(t)); Q(q(f(t)))) reps f(t)/q(f(t)) | 4 steps |
About:
 |  |  |