MAYBE
MAYBE
TRS:
 {
                   sum(xs) -> sum2(xs, 0()),
            generate(x, y) -> gen(x, y, 0()),
               times(x, y) -> sum(generate(x, y)),
              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))),
                ge(x, 0()) -> true(),
             ge(0(), s(y)) -> false(),
            ge(s(x), s(y)) -> ge(x, y),
               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),
              isNil(nil()) -> true(),
        isNil(cons(x, xs)) -> false(),
               isZero(0()) -> true(),
            isZero(s(0())) -> false(),
           isZero(s(s(x))) -> isZero(s(x)),
               head(nil()) -> error(),
         head(cons(x, xs)) -> x,
     ifsum2(true(), xs, y) -> sum2(tail(xs), y),
    ifsum2(false(), xs, y) -> sum2(cons(p(head(xs)), tail(xs)), s(y)),
               tail(nil()) -> nil(),
         tail(cons(x, xs)) -> xs,
                    p(0()) -> s(s(0())),
                 p(s(0())) -> 0(),
                p(s(s(x))) -> s(p(s(x))),
                       a() -> c(),
                       a() -> d()
 }
 DUP: We consider a duplicating system.
  Trs:
   {
                     sum(xs) -> sum2(xs, 0()),
              generate(x, y) -> gen(x, y, 0()),
                 times(x, y) -> sum(generate(x, y)),
                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))),
                  ge(x, 0()) -> true(),
               ge(0(), s(y)) -> false(),
              ge(s(x), s(y)) -> ge(x, y),
                 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),
                isNil(nil()) -> true(),
          isNil(cons(x, xs)) -> false(),
                 isZero(0()) -> true(),
              isZero(s(0())) -> false(),
             isZero(s(s(x))) -> isZero(s(x)),
                 head(nil()) -> error(),
           head(cons(x, xs)) -> x,
       ifsum2(true(), xs, y) -> sum2(tail(xs), y),
      ifsum2(false(), xs, y) -> sum2(cons(p(head(xs)), tail(xs)), s(y)),
                 tail(nil()) -> nil(),
           tail(cons(x, xs)) -> xs,
                      p(0()) -> s(s(0())),
                   p(s(0())) -> 0(),
                  p(s(s(x))) -> s(p(s(x))),
                         a() -> c(),
                         a() -> d()
   }
  Fail