(STRATEGY
    INNERMOST)

(VAR
    b x xs y z)
(DATATYPES
    A = µX.< 0, true, nil, false, cons(X, X), s(X), error, c, d >)
(SIGNATURES
    times :: [A x A] -> A
    generate :: [A x A] -> A
    gen :: [A x A x A] -> A
    if :: [A x A x A x A] -> A
    sum :: [A] -> A
    sum2 :: [A x A] -> A
    ifsum :: [A x A x A x A] -> A
    ifsum2 :: [A x A x A] -> A
    isNil :: [A] -> A
    tail :: [A] -> A
    head :: [A] -> A
    isZero :: [A] -> A
    p :: [A] -> A
    ge :: [A x A] -> A
    a :: [] -> A)
(RULES
    times(x,y) -> sum(generate(x,y))
    generate(x,y) -> gen(x,y,0())
    gen(x,y,z) -> if(ge(z,x),x,y,z)
    if(true(),x,y,z) -> nil()
    if(false(),x,y,z) -> cons(y
                             ,gen(x,y,s(z)))
    sum(xs) -> sum2(xs,0())
    sum2(xs,y) -> ifsum(isNil(xs)
                       ,isZero(head(xs))
                       ,xs
                       ,y)
    ifsum(true(),b,xs,y) -> y
    ifsum(false(),b,xs,y) ->
      ifsum2(b,xs,y)
    ifsum2(true(),xs,y) ->
      sum2(tail(xs),y)
    ifsum2(false(),xs,y) ->
      sum2(cons(p(head(xs)),tail(xs))
          ,s(y))
    isNil(nil()) -> true()
    isNil(cons(x,xs)) -> false()
    tail(nil()) -> nil()
    tail(cons(x,xs)) -> xs
    head(cons(x,xs)) -> x
    head(nil()) -> error()
    isZero(0()) -> true()
    isZero(s(0())) -> false()
    isZero(s(s(x))) -> isZero(s(x))
    p(0()) -> s(s(0()))
    p(s(0())) -> 0()
    p(s(s(x))) -> s(p(s(x)))
    ge(x,0()) -> true()
    ge(0(),s(y)) -> false()
    ge(s(x),s(y)) -> ge(x,y)
    a() -> c()
    a() -> d())