z,x2,x3:T List. ||v||||z|| (v @ x2) = (z @ x3) (z':T List. z = (v @ z') & x2 = (z' @ x3))

x2,x3:T List. ||v||+1||v1|| [u / (v @ x2)] = (v1 @ x3) (z':T List. v1 = [u / (v @ z')] & x2 = (z' @ x3))

||v||+1||v1||+1

z':T List. v1 = (v @ z') & x2 = (z' @ x3)

z':T List. [u1 / v1] = [u / (v @ z')] & x2 = (z' @ x3)

1

14. z': T List 15. v1 = (v @ z') 16. x2 = (z' @ x3) z'@0:T List. [u1 / v1] = [u / (v @ z'@0)] & (z' @ x3) = (z'@0 @ x3)

1 step

About: