MAYBE

Problem:
 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()

Proof:
 DP Processor:
  DPs:
   times#(x,y) -> generate#(x,y)
   times#(x,y) -> sum#(generate(x,y))
   generate#(x,y) -> gen#(x,y,0())
   gen#(x,y,z) -> ge#(z,x)
   gen#(x,y,z) -> if#(ge(z,x),x,y,z)
   if#(false(),x,y,z) -> gen#(x,y,s(z))
   sum#(xs) -> sum2#(xs,0())
   sum2#(xs,y) -> head#(xs)
   sum2#(xs,y) -> isZero#(head(xs))
   sum2#(xs,y) -> isNil#(xs)
   sum2#(xs,y) -> ifsum#(isNil(xs),isZero(head(xs)),xs,y)
   ifsum#(false(),b,xs,y) -> ifsum2#(b,xs,y)
   ifsum2#(true(),xs,y) -> tail#(xs)
   ifsum2#(true(),xs,y) -> sum2#(tail(xs),y)
   ifsum2#(false(),xs,y) -> tail#(xs)
   ifsum2#(false(),xs,y) -> head#(xs)
   ifsum2#(false(),xs,y) -> p#(head(xs))
   ifsum2#(false(),xs,y) -> sum2#(cons(p(head(xs)),tail(xs)),s(y))
   isZero#(s(s(x))) -> isZero#(s(x))
   p#(s(s(x))) -> p#(s(x))
   ge#(s(x),s(y)) -> ge#(x,y)
  TRS:
   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()
  Usable Rule Processor:
   DPs:
    times#(x,y) -> generate#(x,y)
    times#(x,y) -> sum#(generate(x,y))
    generate#(x,y) -> gen#(x,y,0())
    gen#(x,y,z) -> ge#(z,x)
    gen#(x,y,z) -> if#(ge(z,x),x,y,z)
    if#(false(),x,y,z) -> gen#(x,y,s(z))
    sum#(xs) -> sum2#(xs,0())
    sum2#(xs,y) -> head#(xs)
    sum2#(xs,y) -> isZero#(head(xs))
    sum2#(xs,y) -> isNil#(xs)
    sum2#(xs,y) -> ifsum#(isNil(xs),isZero(head(xs)),xs,y)
    ifsum#(false(),b,xs,y) -> ifsum2#(b,xs,y)
    ifsum2#(true(),xs,y) -> tail#(xs)
    ifsum2#(true(),xs,y) -> sum2#(tail(xs),y)
    ifsum2#(false(),xs,y) -> tail#(xs)
    ifsum2#(false(),xs,y) -> head#(xs)
    ifsum2#(false(),xs,y) -> p#(head(xs))
    ifsum2#(false(),xs,y) -> sum2#(cons(p(head(xs)),tail(xs)),s(y))
    isZero#(s(s(x))) -> isZero#(s(x))
    p#(s(s(x))) -> p#(s(x))
    ge#(s(x),s(y)) -> ge#(x,y)
   TRS:
    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)))
    ge(x,0()) -> true()
    ge(0(),s(y)) -> false()
    ge(s(x),s(y)) -> ge(x,y)
    head(cons(x,xs)) -> x
    head(nil()) -> error()
    isZero(0()) -> true()
    isZero(s(0())) -> false()
    isZero(s(s(x))) -> isZero(s(x))
    isNil(nil()) -> true()
    isNil(cons(x,xs)) -> false()
    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)))
   Open