Alphabet

!plus:[a × a] ⟶ a
!times:[a × a] ⟶ a
0:a
cons:[c × d] ⟶ d
fact:[a] ⟶ a
false:b
filter:[c → b × d] ⟶ d
filter2:[b × c → b × c × d] ⟶ d
map:[c → c × d] ⟶ d
nil:d
p:[a] ⟶ a
s:[a] ⟶ a
true:b

Variables

X:a
Y:a
U:a
V:a
W:a
P:a
X1:a
Y1:a
G1:c → c
H1:c → c
W1:c
P1:d
F2:c → b
Z2:c → b
U2:c
V2:d
I2:c → b
P2:c
X3:d
Z3:c → b
U3:c
V3:d

Rules

p(s(X))⇒X
fact(0)⇒s(0)
fact(s(Y))⇒!times(s(Y), fact(p(s(Y))))
!times(0, U)⇒0
!times(s(V), W)⇒!plus(!times(V, W), W)
!plus(P, 0)⇒P
!plus(X1, s(Y1))⇒s(!plus(X1, Y1))
map(G1, nil)⇒nil
map(H1, cons(W1, P1))⇒cons(H1 · W1, map(H1, P1))
filter(F2, nil)⇒nil
filter(Z2, cons(U2, V2))⇒filter2(Z2 · U2, Z2, U2, V2)
filter2(true, I2, P2, X3)⇒cons(P2, filter(I2, X3))
filter2(false, Z3, U3, V3)⇒filter(Z3, V3)