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 · (λ%Y:c.λ%X:a.F · %Y · %X) · nil · Y⇒Y
fold · (λ%U:c.λ%Z:a.G · %U · %Z) · (cons · V · W) · P⇒fold · (λ%W:c.λ%V:a.G · %W · %V) · W · (G · P · V)
sum · X1⇒fold · (λ%G:c.λ%F:a.add · %G · %F) · X1 · 0
fold · (λ%I:c.λ%H:a.mul · %I · %H) · Y1 · 1⇒prod · Y1