(STRATEGY
    INNERMOST)

(VAR
    b l x y)
(DATATYPES
    A = µX.< cons(X, X), nil, 0, true, s(X), false >)
(SIGNATURES
    car :: [A] -> A
    cddr :: [A] -> A
    cadr :: [A] -> A
    isZero :: [A] -> A
    plus :: [A x A] -> A
    ifplus :: [A x A x A] -> A
    times :: [A x A] -> A
    iftimes :: [A x A x A] -> A
    p :: [A] -> A
    shorter :: [A x A] -> A
    prod :: [A] -> A
    if :: [A x A x A] -> A
    if2 :: [A x A] -> A)
(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))))