(VAR b l x y )
(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)))
        
)