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
X2:b
Y2:b

Rules

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