Alphabet

0:a
ack:[a × a] ⟶ a
cons:[c × d] ⟶ d
false:b
filter:[c → b × d] ⟶ d
filter2:[b × c → b × c × d] ⟶ d
map:[c → c × d] ⟶ d
nil:d
succ:[a] ⟶ a
true:b

Variables

X:a
Y:a
U:a
V:a
W:a
J:c → c
F1:c → c
Y1:c
U1:d
H1:c → b
I1:c → b
P1:c
X2:d
Z2:c → b
U2:c
V2:d
I2:c → b
P2:c
X3:d

Rules

ack(0, X)⇒succ(X)
ack(succ(Y), U)⇒ack(Y, succ(0))
ack(succ(V), succ(W))⇒ack(V, ack(succ(V), W))
map(J, nil)⇒nil
map(F1, cons(Y1, U1))⇒cons(F1 · Y1, map(F1, U1))
filter(H1, nil)⇒nil
filter(I1, cons(P1, X2))⇒filter2(I1 · P1, I1, P1, X2)
filter2(true, Z2, U2, V2)⇒cons(U2, filter(Z2, V2))
filter2(false, I2, P2, X3)⇒filter(I2, X3)