Alphabet

0:b
cons:[c × d] ⟶ d
false:a
filter:[c → a × d] ⟶ d
filter2:[a × c → a × c × d] ⟶ d
if:[a × b × b] ⟶ b
le:[b × b] ⟶ a
map:[c → c × d] ⟶ d
minus:[b × b] ⟶ b
nil:d
p:[b] ⟶ b
s:[b] ⟶ b
true:a

Variables

X:b
Y:b
U:b
V:b
W:b
P:b
X1:b
Y1:b
U1:b
V1:b
W1:b
J1:c → c
F2:c → c
Y2:c
U2:d
H2:c → a
I2:c → a
P2:c
X3:d
Z3:c → a
U3:c
V3:d
I3:c → a
P3:c
X4:d

Rules

p(0)⇒0
p(s(X))⇒X
le(0, Y)⇒true
le(s(U), 0)⇒false
le(s(V), s(W))⇒le(V, W)
minus(P, X1)⇒if(le(P, X1), P, X1)
if(true, Y1, U1)⇒0
if(false, V1, W1)⇒s(minus(p(V1), W1))
map(J1, nil)⇒nil
map(F2, cons(Y2, U2))⇒cons(F2 · Y2, map(F2, U2))
filter(H2, nil)⇒nil
filter(I2, cons(P2, X3))⇒filter2(I2 · P2, I2, P2, X3)
filter2(true, Z3, U3, V3)⇒cons(U3, filter(Z3, V3))
filter2(false, I3, P3, X4)⇒filter(I3, X4)