(0) Obligation:
Q restricted rewrite system:
The TRS R consists of the following rules:
car(cons(x, l)) → x
cddr(nil) → nil
cddr(cons(x, nil)) → nil
cddr(cons(x, cons(y, l))) → l
cadr(cons(x, cons(y, l))) → y
isZero(0) → true
isZero(s(x)) → false
plus(x, y) → ifplus(isZero(x), x, y)
ifplus(true, x, y) → y
ifplus(false, x, y) → s(plus(p(x), y))
times(x, y) → iftimes(isZero(x), x, y)
iftimes(true, x, y) → 0
iftimes(false, x, y) → plus(y, times(p(x), y))
p(s(x)) → x
p(0) → 0
shorter(nil, y) → true
shorter(cons(x, l), 0) → false
shorter(cons(x, l), s(y)) → shorter(l, y)
prod(l) → if(shorter(l, 0), shorter(l, s(0)), l)
if(true, b, l) → s(0)
if(false, b, l) → if2(b, l)
if2(true, l) → car(l)
if2(false, l) → prod(cons(times(car(l), cadr(l)), cddr(l)))
Q is empty.