Alphabet

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

Variables

F:c → a → c
Y:c
G:c → a → c
V:a
W:b
P:c
X1:b
Y1:b

Rules

fold(F, nil, Y)⇒Y
fold(G, cons(V, W), P)⇒fold(G, W, G · P · V)
sum(X1)⇒fold(add, X1, 0)
fold(mul, Y1, 1)⇒prod(Y1)