Alphabet

0:c
add:a → c → c
cons:[a × b] ⟶ b
fold:[a → c → c × c] ⟶ b → c
mul:a → c → c
nil:b
plus:[c × c] ⟶ c
prod:b → c
s:[c] ⟶ c
sum:b → c
times:[c × c] ⟶ c

Variables

F:a → c → c
Y:c
G:a → c → c
V:c
W:a
P:b
X1:c
Y1:c
U1:c
V1:c
W1:c
P1:c

Rules

fold(F, Y) · nil⇒Y
fold(G, V) · cons(W, P)⇒G · W · (fold(G, V) · P)
plus(0, X1)⇒X1
plus(s(Y1), U1)⇒s(plus(Y1, U1))
times(0, V1)⇒0
times(s(W1), P1)⇒plus(times(W1, P1), P1)
sum⇒fold(add, 0)
prod⇒fold(mul, s(0))