Alphabet

!dot:[a × a] ⟶ a
1:a
cons:[c × d] ⟶ d
false:b
filter:[c → b × d] ⟶ d
filter2:[b × c → b × c × d] ⟶ d
i:[a] ⟶ a
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
H1:c → c
I1:c → c
P1:c
X2:d
Z2:c → b
G2:c → b
V2:c
W2:d
J2:c → b
X3:c
Y3:d
G3:c → b
V3:c
W3:d

Rules

!dot(1, X)⇒X
!dot(Y, 1)⇒Y
!dot(i(U), U)⇒1
!dot(V, i(V))⇒1
!dot(i(W), !dot(W, P))⇒P
!dot(X1, !dot(i(X1), Y1))⇒Y1
i(1)⇒1
i(i(U1))⇒U1
map(H1, nil)⇒nil
map(I1, cons(P1, X2))⇒cons(I1 · P1, map(I1, X2))
filter(Z2, nil)⇒nil
filter(G2, cons(V2, W2))⇒filter2(G2 · V2, G2, V2, W2)
filter2(true, J2, X3, Y3)⇒cons(X3, filter(J2, Y3))
filter2(false, G3, V3, W3)⇒filter(G3, W3)