Alphabet

0:a
cons:[a × c] ⟶ c
false:b
filter:[a → b] ⟶ c → c
filtersub:[b × a → b × c] ⟶ c
neq:[a] ⟶ a → b
nil:c
nonzero:c → c
s:[a] ⟶ a
true:b

Variables

X:a
Y:a
U:a
V:a
I:a → b
J:a → b
X1:a
Y1:c
G1:a → b
V1:a
W1:c
J1:a → b
X2:a
Y2:c

Rules

neq(0) · 0⇒false
neq(0) · s(X)⇒true
neq(s(Y)) · 0⇒true
neq(s(U)) · s(V)⇒neq(U) · V
filter(I) · nil⇒nil
filter(J) · cons(X1, Y1)⇒filtersub(J · X1, J, cons(X1, Y1))
filtersub(true, G1, cons(V1, W1))⇒cons(V1, filter(G1) · W1)
filtersub(false, J1, cons(X2, Y2))⇒filter(J1) · Y2
nonzero⇒filter(neq(0))