Alphabet

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

Variables

X:b
Y:b
U:b
V:b
W:b
P:b
X1:b
Y1:b
U1:b
V1:b
W1:b
P1:b
X2:b
Z2:d → d
G2:d → d
V2:d
W2:e
J2:d → c
F3:d → c
Y3:d
U3:e
H3:d → c
W3:d
P3:e
F4:d → c
Y4:d
U4:e

Rules

perfectp(0)⇒false
perfectp(s(X))⇒f(X, s(0), s(X), s(X))
f(0, U, 0, Y)⇒true
f(0, W, s(P), V)⇒false
f(s(Y1), 0, U1, X1)⇒f(Y1, X1, minus(U1, s(Y1)), X1)
f(s(W1), s(P1), X2, V1)⇒if(le(W1, P1), f(s(W1), minus(P1, W1), X2, V1), f(W1, V1, X2, V1))
map(Z2, nil)⇒nil
map(G2, cons(V2, W2))⇒cons(G2 · V2, map(G2, W2))
filter(J2, nil)⇒nil
filter(F3, cons(Y3, U3))⇒filter2(F3 · Y3, F3, Y3, U3)
filter2(true, H3, W3, P3)⇒cons(W3, filter(H3, P3))
filter2(false, F4, Y4, U4)⇒filter(F4, U4)