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(nil()) -> 0()
 sum(cons(0(),xs)) -> sum(xs)
 sum(cons(s(x),xs)) -> s(sum(cons(x,xs)))
 ge(x,0()) -> true()
 ge(0(),s(y)) -> false()
 ge(s(x),s(y)) -> ge(x,y)

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#(cons(0(),xs)) -> sum#(xs)
   sum#(cons(s(x),xs)) -> sum#(cons(x,xs))
   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(nil()) -> 0()
   sum(cons(0(),xs)) -> sum(xs)
   sum(cons(s(x),xs)) -> s(sum(cons(x,xs)))
   ge(x,0()) -> true()
   ge(0(),s(y)) -> false()
   ge(s(x),s(y)) -> ge(x,y)
  EDG 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#(cons(0(),xs)) -> sum#(xs)
    sum#(cons(s(x),xs)) -> sum#(cons(x,xs))
    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(nil()) -> 0()
    sum(cons(0(),xs)) -> sum(xs)
    sum(cons(s(x),xs)) -> s(sum(cons(x,xs)))
    ge(x,0()) -> true()
    ge(0(),s(y)) -> false()
    ge(s(x),s(y)) -> ge(x,y)
   graph:
    if#(false(),x,y,z) -> gen#(x,y,s(z)) ->
    gen#(x,y,z) -> ge#(z,x)
    if#(false(),x,y,z) -> gen#(x,y,s(z)) ->
    gen#(x,y,z) -> if#(ge(z,x),x,y,z)
    ge#(s(x),s(y)) -> ge#(x,y) -> ge#(s(x),s(y)) -> ge#(x,y)
    gen#(x,y,z) -> if#(ge(z,x),x,y,z) ->
    if#(false(),x,y,z) -> gen#(x,y,s(z))
    gen#(x,y,z) -> ge#(z,x) -> ge#(s(x),s(y)) -> ge#(x,y)
    sum#(cons(s(x),xs)) -> sum#(cons(x,xs)) ->
    sum#(cons(0(),xs)) -> sum#(xs)
    sum#(cons(s(x),xs)) -> sum#(cons(x,xs)) ->
    sum#(cons(s(x),xs)) -> sum#(cons(x,xs))
    sum#(cons(0(),xs)) -> sum#(xs) -> sum#(cons(0(),xs)) -> sum#(xs)
    sum#(cons(0(),xs)) -> sum#(xs) ->
    sum#(cons(s(x),xs)) -> sum#(cons(x,xs))
    generate#(x,y) -> gen#(x,y,0()) -> gen#(x,y,z) -> ge#(z,x)
    generate#(x,y) -> gen#(x,y,0()) ->
    gen#(x,y,z) -> if#(ge(z,x),x,y,z)
    times#(x,y) -> sum#(generate(x,y)) ->
    sum#(cons(0(),xs)) -> sum#(xs)
    times#(x,y) -> sum#(generate(x,y)) ->
    sum#(cons(s(x),xs)) -> sum#(cons(x,xs))
    times#(x,y) -> generate#(x,y) -> generate#(x,y) -> gen#(x,y,0())
   SCC Processor:
    #sccs: 3
    #rules: 5
    #arcs: 14/81
    DPs:
     sum#(cons(s(x),xs)) -> sum#(cons(x,xs))
     sum#(cons(0(),xs)) -> sum#(xs)
    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(nil()) -> 0()
     sum(cons(0(),xs)) -> sum(xs)
     sum(cons(s(x),xs)) -> s(sum(cons(x,xs)))
     ge(x,0()) -> true()
     ge(0(),s(y)) -> false()
     ge(s(x),s(y)) -> ge(x,y)
    Open
    
    DPs:
     if#(false(),x,y,z) -> gen#(x,y,s(z))
     gen#(x,y,z) -> if#(ge(z,x),x,y,z)
    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(nil()) -> 0()
     sum(cons(0(),xs)) -> sum(xs)
     sum(cons(s(x),xs)) -> s(sum(cons(x,xs)))
     ge(x,0()) -> true()
     ge(0(),s(y)) -> false()
     ge(s(x),s(y)) -> ge(x,y)
    Open
    
    DPs:
     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(nil()) -> 0()
     sum(cons(0(),xs)) -> sum(xs)
     sum(cons(s(x),xs)) -> s(sum(cons(x,xs)))
     ge(x,0()) -> true()
     ge(0(),s(y)) -> false()
     ge(s(x),s(y)) -> ge(x,y)
    Open