Alphabet

!plus:[a × a] ⟶ a
!times:[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
true:b

Variables

X:a
Y:a
U:a
V:a
W:a
P:a
X1:a
Y1:a
U1:a
V1:a
W1:a
P1:a
F2:c → c
Z2:c → c
U2:c
V2:d
I2:c → b
J2:c → b
X3:c
Y3:d
G3:c → b
V3:c
W3:d
J3:c → b
X4:c
Y4:d

Rules

!times(X, !plus(Y, U))⇒!plus(!times(X, Y), !times(X, U))
!times(!plus(W, P), V)⇒!plus(!times(V, W), !times(V, P))
!times(!times(X1, Y1), U1)⇒!times(X1, !times(Y1, U1))
!plus(!plus(V1, W1), P1)⇒!plus(V1, !plus(W1, P1))
map(F2, nil)⇒nil
map(Z2, cons(U2, V2))⇒cons(Z2 · U2, map(Z2, V2))
filter(I2, nil)⇒nil
filter(J2, cons(X3, Y3))⇒filter2(J2 · X3, J2, X3, Y3)
filter2(true, G3, V3, W3)⇒cons(V3, filter(G3, W3))
filter2(false, J3, X4, Y4)⇒filter(J3, Y4)