"Translation"

X1(f) = x1 f
X2(f) = x2 f
X3(f) = x3 f

P1(f) = -i hbar d(f,x1)
P2(f) = -i hbar d(f,x2)
P3(f) = -i hbar d(f,x3)

L1(f) = X2(P3(f)) - X3(P2(f))
L2(f) = X3(P1(f)) - X1(P3(f))
L3(f) = X1(P2(f)) - X2(P1(f))

K1(f) = P1(f) / hbar
K2(f) = P2(f) / hbar
K3(f) = P3(f) / hbar

U(f) = f - i epsilon K3(f) - 1/2 epsilon^2 K3(K3(f))
V(f) = f + i epsilon K3(f) - 1/2 epsilon^2 K3(K3(f)) -- inverse of U

psi = Psi(x1,x2,x3)

T = V(U(psi))
T = eval(T, epsilon^4, 0)
check(T == psi)

"Verify (1)"

T1 = V(X1(U(psi)))
T1 = eval(T1, epsilon^4, 0, epsilon^3, 0)
check(T1 == X1(psi))

T2 = V(X2(U(psi)))
T2 = eval(T2, epsilon^4, 0, epsilon^3, 0)
check(T2 == X2(psi))

T3 = V(X3(U(psi)))
T3 = eval(T3, epsilon^4, 0, epsilon^3, 0)
check(T3 == X3(psi) + epsilon psi)

"ok"

"Verify (2)"

T1 = V(P1(U(psi)))
T1 = eval(T1, epsilon^4, 0, epsilon^3, 0)
check(T1 == P1(psi))

T2 = V(P2(U(psi)))
T2 = eval(T2, epsilon^4, 0, epsilon^3, 0)
check(T2 == P2(psi))

T3 = V(P3(U(psi)))
T3 = eval(T3, epsilon^4, 0, epsilon^3, 0)
check(T3 == P3(psi))

"ok"

"Verify (3)"

T1 = V(L1(U(psi)))
T1 = eval(T1, epsilon^4, 0, epsilon^3, 0)
check(T1 == L1(psi) - epsilon P2(psi))

T2 = V(L2(U(psi)))
T2 = eval(T2, epsilon^4, 0, epsilon^3, 0)
check(T2 == L2(psi) + epsilon P1(psi))

T3 = V(L3(U(psi)))
T3 = eval(T3, epsilon^4, 0, epsilon^3, 0)
check(T3 == L3(psi))

"ok"

"Verify (4)"

H(f) = (P1(P1(f)) + P2(P2(f)) + P3(P3(f))) / (2 m)

T = V(H(U(psi)))
T = eval(T, epsilon^4, 0, epsilon^3, 0)
check(T == H(psi))

"ok"