MAYBE

Problem:
 prod(xs) -> prodIter(xs,s(0()))
 prodIter(xs,x) -> ifProd(isempty(xs),xs,x)
 ifProd(true(),xs,x) -> x
 ifProd(false(),xs,x) -> prodIter(tail(xs),times(x,head(xs)))
 plus(0(),y) -> y
 plus(s(x),y) -> s(plus(x,y))
 times(x,y) -> timesIter(x,y,0(),0())
 timesIter(x,y,z,u) -> ifTimes(ge(u,x),x,y,z,u)
 ifTimes(true(),x,y,z,u) -> z
 ifTimes(false(),x,y,z,u) -> timesIter(x,y,plus(y,z),s(u))
 isempty(nil()) -> true()
 isempty(cons(x,xs)) -> false()
 head(nil()) -> error()
 head(cons(x,xs)) -> x
 tail(nil()) -> nil()
 tail(cons(x,xs)) -> xs
 ge(x,0()) -> true()
 ge(0(),s(y)) -> false()
 ge(s(x),s(y)) -> ge(x,y)
 a() -> b()
 a() -> c()

Proof:
 DP Processor:
  DPs:
   prod#(xs) -> prodIter#(xs,s(0()))
   prodIter#(xs,x) -> isempty#(xs)
   prodIter#(xs,x) -> ifProd#(isempty(xs),xs,x)
   ifProd#(false(),xs,x) -> head#(xs)
   ifProd#(false(),xs,x) -> times#(x,head(xs))
   ifProd#(false(),xs,x) -> tail#(xs)
   ifProd#(false(),xs,x) -> prodIter#(tail(xs),times(x,head(xs)))
   plus#(s(x),y) -> plus#(x,y)
   times#(x,y) -> timesIter#(x,y,0(),0())
   timesIter#(x,y,z,u) -> ge#(u,x)
   timesIter#(x,y,z,u) -> ifTimes#(ge(u,x),x,y,z,u)
   ifTimes#(false(),x,y,z,u) -> plus#(y,z)
   ifTimes#(false(),x,y,z,u) -> timesIter#(x,y,plus(y,z),s(u))
   ge#(s(x),s(y)) -> ge#(x,y)
  TRS:
   prod(xs) -> prodIter(xs,s(0()))
   prodIter(xs,x) -> ifProd(isempty(xs),xs,x)
   ifProd(true(),xs,x) -> x
   ifProd(false(),xs,x) -> prodIter(tail(xs),times(x,head(xs)))
   plus(0(),y) -> y
   plus(s(x),y) -> s(plus(x,y))
   times(x,y) -> timesIter(x,y,0(),0())
   timesIter(x,y,z,u) -> ifTimes(ge(u,x),x,y,z,u)
   ifTimes(true(),x,y,z,u) -> z
   ifTimes(false(),x,y,z,u) -> timesIter(x,y,plus(y,z),s(u))
   isempty(nil()) -> true()
   isempty(cons(x,xs)) -> false()
   head(nil()) -> error()
   head(cons(x,xs)) -> x
   tail(nil()) -> nil()
   tail(cons(x,xs)) -> xs
   ge(x,0()) -> true()
   ge(0(),s(y)) -> false()
   ge(s(x),s(y)) -> ge(x,y)
   a() -> b()
   a() -> c()
  TDG Processor:
   DPs:
    prod#(xs) -> prodIter#(xs,s(0()))
    prodIter#(xs,x) -> isempty#(xs)
    prodIter#(xs,x) -> ifProd#(isempty(xs),xs,x)
    ifProd#(false(),xs,x) -> head#(xs)
    ifProd#(false(),xs,x) -> times#(x,head(xs))
    ifProd#(false(),xs,x) -> tail#(xs)
    ifProd#(false(),xs,x) -> prodIter#(tail(xs),times(x,head(xs)))
    plus#(s(x),y) -> plus#(x,y)
    times#(x,y) -> timesIter#(x,y,0(),0())
    timesIter#(x,y,z,u) -> ge#(u,x)
    timesIter#(x,y,z,u) -> ifTimes#(ge(u,x),x,y,z,u)
    ifTimes#(false(),x,y,z,u) -> plus#(y,z)
    ifTimes#(false(),x,y,z,u) -> timesIter#(x,y,plus(y,z),s(u))
    ge#(s(x),s(y)) -> ge#(x,y)
   TRS:
    prod(xs) -> prodIter(xs,s(0()))
    prodIter(xs,x) -> ifProd(isempty(xs),xs,x)
    ifProd(true(),xs,x) -> x
    ifProd(false(),xs,x) -> prodIter(tail(xs),times(x,head(xs)))
    plus(0(),y) -> y
    plus(s(x),y) -> s(plus(x,y))
    times(x,y) -> timesIter(x,y,0(),0())
    timesIter(x,y,z,u) -> ifTimes(ge(u,x),x,y,z,u)
    ifTimes(true(),x,y,z,u) -> z
    ifTimes(false(),x,y,z,u) -> timesIter(x,y,plus(y,z),s(u))
    isempty(nil()) -> true()
    isempty(cons(x,xs)) -> false()
    head(nil()) -> error()
    head(cons(x,xs)) -> x
    tail(nil()) -> nil()
    tail(cons(x,xs)) -> xs
    ge(x,0()) -> true()
    ge(0(),s(y)) -> false()
    ge(s(x),s(y)) -> ge(x,y)
    a() -> b()
    a() -> c()
   graph:
    ifTimes#(false(),x,y,z,u) -> timesIter#(x,y,plus(y,z),s(u)) ->
    timesIter#(x,y,z,u) -> ifTimes#(ge(u,x),x,y,z,u)
    ifTimes#(false(),x,y,z,u) -> timesIter#(x,y,plus(y,z),s(u)) ->
    timesIter#(x,y,z,u) -> ge#(u,x)
    ifTimes#(false(),x,y,z,u) -> plus#(y,z) ->
    plus#(s(x),y) -> plus#(x,y)
    ge#(s(x),s(y)) -> ge#(x,y) ->
    ge#(s(x),s(y)) -> ge#(x,y)
    timesIter#(x,y,z,u) -> ifTimes#(ge(u,x),x,y,z,u) ->
    ifTimes#(false(),x,y,z,u) -> timesIter#(x,y,plus(y,z),s(u))
    timesIter#(x,y,z,u) -> ifTimes#(ge(u,x),x,y,z,u) ->
    ifTimes#(false(),x,y,z,u) -> plus#(y,z)
    timesIter#(x,y,z,u) -> ge#(u,x) -> ge#(s(x),s(y)) -> ge#(x,y)
    plus#(s(x),y) -> plus#(x,y) ->
    plus#(s(x),y) -> plus#(x,y)
    times#(x,y) -> timesIter#(x,y,0(),0()) ->
    timesIter#(x,y,z,u) -> ifTimes#(ge(u,x),x,y,z,u)
    times#(x,y) -> timesIter#(x,y,0(),0()) ->
    timesIter#(x,y,z,u) -> ge#(u,x)
    ifProd#(false(),xs,x) -> times#(x,head(xs)) ->
    times#(x,y) -> timesIter#(x,y,0(),0())
    ifProd#(false(),xs,x) -> prodIter#(tail(xs),times(x,head(xs))) ->
    prodIter#(xs,x) -> ifProd#(isempty(xs),xs,x)
    ifProd#(false(),xs,x) -> prodIter#(tail(xs),times(x,head(xs))) ->
    prodIter#(xs,x) -> isempty#(xs)
    prodIter#(xs,x) -> ifProd#(isempty(xs),xs,x) ->
    ifProd#(false(),xs,x) -> prodIter#(tail(xs),times(x,head(xs)))
    prodIter#(xs,x) -> ifProd#(isempty(xs),xs,x) ->
    ifProd#(false(),xs,x) -> tail#(xs)
    prodIter#(xs,x) -> ifProd#(isempty(xs),xs,x) ->
    ifProd#(false(),xs,x) -> times#(x,head(xs))
    prodIter#(xs,x) -> ifProd#(isempty(xs),xs,x) ->
    ifProd#(false(),xs,x) -> head#(xs)
    prod#(xs) -> prodIter#(xs,s(0())) ->
    prodIter#(xs,x) -> ifProd#(isempty(xs),xs,x)
    prod#(xs) -> prodIter#(xs,s(0())) -> prodIter#(xs,x) -> isempty#(xs)
   SCC Processor:
    #sccs: 4
    #rules: 6
    #arcs: 19/196
    DPs:
     ifProd#(false(),xs,x) -> prodIter#(tail(xs),times(x,head(xs)))
     prodIter#(xs,x) -> ifProd#(isempty(xs),xs,x)
    TRS:
     prod(xs) -> prodIter(xs,s(0()))
     prodIter(xs,x) -> ifProd(isempty(xs),xs,x)
     ifProd(true(),xs,x) -> x
     ifProd(false(),xs,x) -> prodIter(tail(xs),times(x,head(xs)))
     plus(0(),y) -> y
     plus(s(x),y) -> s(plus(x,y))
     times(x,y) -> timesIter(x,y,0(),0())
     timesIter(x,y,z,u) -> ifTimes(ge(u,x),x,y,z,u)
     ifTimes(true(),x,y,z,u) -> z
     ifTimes(false(),x,y,z,u) -> timesIter(x,y,plus(y,z),s(u))
     isempty(nil()) -> true()
     isempty(cons(x,xs)) -> false()
     head(nil()) -> error()
     head(cons(x,xs)) -> x
     tail(nil()) -> nil()
     tail(cons(x,xs)) -> xs
     ge(x,0()) -> true()
     ge(0(),s(y)) -> false()
     ge(s(x),s(y)) -> ge(x,y)
     a() -> b()
     a() -> c()
    Matrix Interpretation Processor: dim=1
     
     interpretation:
      [ifProd#](x0, x1, x2) = 2x0 + x1,
      
      [prodIter#](x0, x1) = 2x0 + 2,
      
      [c] = 1/2,
      
      [b] = 0,
      
      [a] = 1/2,
      
      [error] = 0,
      
      [cons](x0, x1) = 2x0 + 2x1 + 2,
      
      [nil] = 0,
      
      [ifTimes](x0, x1, x2, x3, x4) = 2x3,
      
      [ge](x0, x1) = 1,
      
      [timesIter](x0, x1, x2, x3) = 2x2,
      
      [plus](x0, x1) = x1,
      
      [times](x0, x1) = 0,
      
      [head](x0) = 2x0 + 2,
      
      [tail](x0) = 1/2x0,
      
      [false] = 1,
      
      [true] = 0,
      
      [ifProd](x0, x1, x2) = 5/2x2,
      
      [isempty](x0) = 1/2x0,
      
      [prodIter](x0, x1) = 3x1,
      
      [s](x0) = 0,
      
      [0] = 0,
      
      [prod](x0) = 1/2
     orientation:
      ifProd#(false(),xs,x) = xs + 2 >= xs + 2 = prodIter#(tail(xs),times(x,head(xs)))
      
      prodIter#(xs,x) = 2xs + 2 >= 2xs = ifProd#(isempty(xs),xs,x)
      
      prod(xs) = 1/2 >= 0 = prodIter(xs,s(0()))
      
      prodIter(xs,x) = 3x >= 5/2x = ifProd(isempty(xs),xs,x)
      
      ifProd(true(),xs,x) = 5/2x >= x = x
      
      ifProd(false(),xs,x) = 5/2x >= 0 = prodIter(tail(xs),times(x,head(xs)))
      
      plus(0(),y) = y >= y = y
      
      plus(s(x),y) = y >= 0 = s(plus(x,y))
      
      times(x,y) = 0 >= 0 = timesIter(x,y,0(),0())
      
      timesIter(x,y,z,u) = 2z >= 2z = ifTimes(ge(u,x),x,y,z,u)
      
      ifTimes(true(),x,y,z,u) = 2z >= z = z
      
      ifTimes(false(),x,y,z,u) = 2z >= 2z = timesIter(x,y,plus(y,z),s(u))
      
      isempty(nil()) = 0 >= 0 = true()
      
      isempty(cons(x,xs)) = x + xs + 1 >= 1 = false()
      
      head(nil()) = 2 >= 0 = error()
      
      head(cons(x,xs)) = 4x + 4xs + 6 >= x = x
      
      tail(nil()) = 0 >= 0 = nil()
      
      tail(cons(x,xs)) = x + xs + 1 >= xs = xs
      
      ge(x,0()) = 1 >= 0 = true()
      
      ge(0(),s(y)) = 1 >= 1 = false()
      
      ge(s(x),s(y)) = 1 >= 1 = ge(x,y)
      
      a() = 1/2 >= 0 = b()
      
      a() = 1/2 >= 1/2 = c()
     problem:
      DPs:
       ifProd#(false(),xs,x) -> prodIter#(tail(xs),times(x,head(xs)))
      TRS:
       prod(xs) -> prodIter(xs,s(0()))
       prodIter(xs,x) -> ifProd(isempty(xs),xs,x)
       ifProd(true(),xs,x) -> x
       ifProd(false(),xs,x) -> prodIter(tail(xs),times(x,head(xs)))
       plus(0(),y) -> y
       plus(s(x),y) -> s(plus(x,y))
       times(x,y) -> timesIter(x,y,0(),0())
       timesIter(x,y,z,u) -> ifTimes(ge(u,x),x,y,z,u)
       ifTimes(true(),x,y,z,u) -> z
       ifTimes(false(),x,y,z,u) -> timesIter(x,y,plus(y,z),s(u))
       isempty(nil()) -> true()
       isempty(cons(x,xs)) -> false()
       head(nil()) -> error()
       head(cons(x,xs)) -> x
       tail(nil()) -> nil()
       tail(cons(x,xs)) -> xs
       ge(x,0()) -> true()
       ge(0(),s(y)) -> false()
       ge(s(x),s(y)) -> ge(x,y)
       a() -> b()
       a() -> c()
     SCC Processor:
      #sccs: 0
      #rules: 0
      #arcs: 2/1
      
    
    DPs:
     ifTimes#(false(),x,y,z,u) -> timesIter#(x,y,plus(y,z),s(u))
     timesIter#(x,y,z,u) -> ifTimes#(ge(u,x),x,y,z,u)
    TRS:
     prod(xs) -> prodIter(xs,s(0()))
     prodIter(xs,x) -> ifProd(isempty(xs),xs,x)
     ifProd(true(),xs,x) -> x
     ifProd(false(),xs,x) -> prodIter(tail(xs),times(x,head(xs)))
     plus(0(),y) -> y
     plus(s(x),y) -> s(plus(x,y))
     times(x,y) -> timesIter(x,y,0(),0())
     timesIter(x,y,z,u) -> ifTimes(ge(u,x),x,y,z,u)
     ifTimes(true(),x,y,z,u) -> z
     ifTimes(false(),x,y,z,u) -> timesIter(x,y,plus(y,z),s(u))
     isempty(nil()) -> true()
     isempty(cons(x,xs)) -> false()
     head(nil()) -> error()
     head(cons(x,xs)) -> x
     tail(nil()) -> nil()
     tail(cons(x,xs)) -> xs
     ge(x,0()) -> true()
     ge(0(),s(y)) -> false()
     ge(s(x),s(y)) -> ge(x,y)
     a() -> b()
     a() -> c()
    Open
    
    DPs:
     plus#(s(x),y) -> plus#(x,y)
    TRS:
     prod(xs) -> prodIter(xs,s(0()))
     prodIter(xs,x) -> ifProd(isempty(xs),xs,x)
     ifProd(true(),xs,x) -> x
     ifProd(false(),xs,x) -> prodIter(tail(xs),times(x,head(xs)))
     plus(0(),y) -> y
     plus(s(x),y) -> s(plus(x,y))
     times(x,y) -> timesIter(x,y,0(),0())
     timesIter(x,y,z,u) -> ifTimes(ge(u,x),x,y,z,u)
     ifTimes(true(),x,y,z,u) -> z
     ifTimes(false(),x,y,z,u) -> timesIter(x,y,plus(y,z),s(u))
     isempty(nil()) -> true()
     isempty(cons(x,xs)) -> false()
     head(nil()) -> error()
     head(cons(x,xs)) -> x
     tail(nil()) -> nil()
     tail(cons(x,xs)) -> xs
     ge(x,0()) -> true()
     ge(0(),s(y)) -> false()
     ge(s(x),s(y)) -> ge(x,y)
     a() -> b()
     a() -> c()
    Subterm Criterion Processor:
     simple projection:
      pi(plus#) = 0
     problem:
      DPs:
       
      TRS:
       prod(xs) -> prodIter(xs,s(0()))
       prodIter(xs,x) -> ifProd(isempty(xs),xs,x)
       ifProd(true(),xs,x) -> x
       ifProd(false(),xs,x) -> prodIter(tail(xs),times(x,head(xs)))
       plus(0(),y) -> y
       plus(s(x),y) -> s(plus(x,y))
       times(x,y) -> timesIter(x,y,0(),0())
       timesIter(x,y,z,u) -> ifTimes(ge(u,x),x,y,z,u)
       ifTimes(true(),x,y,z,u) -> z
       ifTimes(false(),x,y,z,u) -> timesIter(x,y,plus(y,z),s(u))
       isempty(nil()) -> true()
       isempty(cons(x,xs)) -> false()
       head(nil()) -> error()
       head(cons(x,xs)) -> x
       tail(nil()) -> nil()
       tail(cons(x,xs)) -> xs
       ge(x,0()) -> true()
       ge(0(),s(y)) -> false()
       ge(s(x),s(y)) -> ge(x,y)
       a() -> b()
       a() -> c()
     Qed
    
    DPs:
     ge#(s(x),s(y)) -> ge#(x,y)
    TRS:
     prod(xs) -> prodIter(xs,s(0()))
     prodIter(xs,x) -> ifProd(isempty(xs),xs,x)
     ifProd(true(),xs,x) -> x
     ifProd(false(),xs,x) -> prodIter(tail(xs),times(x,head(xs)))
     plus(0(),y) -> y
     plus(s(x),y) -> s(plus(x,y))
     times(x,y) -> timesIter(x,y,0(),0())
     timesIter(x,y,z,u) -> ifTimes(ge(u,x),x,y,z,u)
     ifTimes(true(),x,y,z,u) -> z
     ifTimes(false(),x,y,z,u) -> timesIter(x,y,plus(y,z),s(u))
     isempty(nil()) -> true()
     isempty(cons(x,xs)) -> false()
     head(nil()) -> error()
     head(cons(x,xs)) -> x
     tail(nil()) -> nil()
     tail(cons(x,xs)) -> xs
     ge(x,0()) -> true()
     ge(0(),s(y)) -> false()
     ge(s(x),s(y)) -> ge(x,y)
     a() -> b()
     a() -> c()
    Subterm Criterion Processor:
     simple projection:
      pi(ge#) = 1
     problem:
      DPs:
       
      TRS:
       prod(xs) -> prodIter(xs,s(0()))
       prodIter(xs,x) -> ifProd(isempty(xs),xs,x)
       ifProd(true(),xs,x) -> x
       ifProd(false(),xs,x) -> prodIter(tail(xs),times(x,head(xs)))
       plus(0(),y) -> y
       plus(s(x),y) -> s(plus(x,y))
       times(x,y) -> timesIter(x,y,0(),0())
       timesIter(x,y,z,u) -> ifTimes(ge(u,x),x,y,z,u)
       ifTimes(true(),x,y,z,u) -> z
       ifTimes(false(),x,y,z,u) -> timesIter(x,y,plus(y,z),s(u))
       isempty(nil()) -> true()
       isempty(cons(x,xs)) -> false()
       head(nil()) -> error()
       head(cons(x,xs)) -> x
       tail(nil()) -> nil()
       tail(cons(x,xs)) -> xs
       ge(x,0()) -> true()
       ge(0(),s(y)) -> false()
       ge(s(x),s(y)) -> ge(x,y)
       a() -> b()
       a() -> c()
     Qed