MAYBE

Problem:
 gt(0(),y) -> false()
 gt(s(x),0()) -> true()
 gt(s(x),s(y)) -> gt(x,y)
 plus(0(),y) -> y
 plus(s(x),y) -> s(plus(x,y))
 double(0()) -> 0()
 double(s(x)) -> s(s(double(x)))
 average(x,y) -> aver(plus(x,y),0())
 aver(sum,z) -> if(gt(sum,double(z)),sum,z)
 if(true(),sum,z) -> aver(sum,s(z))
 if(false(),sum,z) -> z

Proof:
 DP Processor:
  DPs:
   gt#(s(x),s(y)) -> gt#(x,y)
   plus#(s(x),y) -> plus#(x,y)
   double#(s(x)) -> double#(x)
   average#(x,y) -> plus#(x,y)
   average#(x,y) -> aver#(plus(x,y),0())
   aver#(sum,z) -> double#(z)
   aver#(sum,z) -> gt#(sum,double(z))
   aver#(sum,z) -> if#(gt(sum,double(z)),sum,z)
   if#(true(),sum,z) -> aver#(sum,s(z))
  TRS:
   gt(0(),y) -> false()
   gt(s(x),0()) -> true()
   gt(s(x),s(y)) -> gt(x,y)
   plus(0(),y) -> y
   plus(s(x),y) -> s(plus(x,y))
   double(0()) -> 0()
   double(s(x)) -> s(s(double(x)))
   average(x,y) -> aver(plus(x,y),0())
   aver(sum,z) -> if(gt(sum,double(z)),sum,z)
   if(true(),sum,z) -> aver(sum,s(z))
   if(false(),sum,z) -> z
  TDG Processor:
   DPs:
    gt#(s(x),s(y)) -> gt#(x,y)
    plus#(s(x),y) -> plus#(x,y)
    double#(s(x)) -> double#(x)
    average#(x,y) -> plus#(x,y)
    average#(x,y) -> aver#(plus(x,y),0())
    aver#(sum,z) -> double#(z)
    aver#(sum,z) -> gt#(sum,double(z))
    aver#(sum,z) -> if#(gt(sum,double(z)),sum,z)
    if#(true(),sum,z) -> aver#(sum,s(z))
   TRS:
    gt(0(),y) -> false()
    gt(s(x),0()) -> true()
    gt(s(x),s(y)) -> gt(x,y)
    plus(0(),y) -> y
    plus(s(x),y) -> s(plus(x,y))
    double(0()) -> 0()
    double(s(x)) -> s(s(double(x)))
    average(x,y) -> aver(plus(x,y),0())
    aver(sum,z) -> if(gt(sum,double(z)),sum,z)
    if(true(),sum,z) -> aver(sum,s(z))
    if(false(),sum,z) -> z
   graph:
    if#(true(),sum,z) -> aver#(sum,s(z)) ->
    aver#(sum,z) -> if#(gt(sum,double(z)),sum,z)
    if#(true(),sum,z) -> aver#(sum,s(z)) ->
    aver#(sum,z) -> gt#(sum,double(z))
    if#(true(),sum,z) -> aver#(sum,s(z)) ->
    aver#(sum,z) -> double#(z)
    aver#(sum,z) -> if#(gt(sum,double(z)),sum,z) ->
    if#(true(),sum,z) -> aver#(sum,s(z))
    aver#(sum,z) -> double#(z) -> double#(s(x)) -> double#(x)
    aver#(sum,z) -> gt#(sum,double(z)) ->
    gt#(s(x),s(y)) -> gt#(x,y)
    average#(x,y) -> aver#(plus(x,y),0()) ->
    aver#(sum,z) -> if#(gt(sum,double(z)),sum,z)
    average#(x,y) -> aver#(plus(x,y),0()) ->
    aver#(sum,z) -> gt#(sum,double(z))
    average#(x,y) -> aver#(plus(x,y),0()) -> aver#(sum,z) -> double#(z)
    average#(x,y) -> plus#(x,y) -> plus#(s(x),y) -> plus#(x,y)
    double#(s(x)) -> double#(x) -> double#(s(x)) -> double#(x)
    plus#(s(x),y) -> plus#(x,y) -> plus#(s(x),y) -> plus#(x,y)
    gt#(s(x),s(y)) -> gt#(x,y) -> gt#(s(x),s(y)) -> gt#(x,y)
   SCC Processor:
    #sccs: 4
    #rules: 5
    #arcs: 13/81
    DPs:
     plus#(s(x),y) -> plus#(x,y)
    TRS:
     gt(0(),y) -> false()
     gt(s(x),0()) -> true()
     gt(s(x),s(y)) -> gt(x,y)
     plus(0(),y) -> y
     plus(s(x),y) -> s(plus(x,y))
     double(0()) -> 0()
     double(s(x)) -> s(s(double(x)))
     average(x,y) -> aver(plus(x,y),0())
     aver(sum,z) -> if(gt(sum,double(z)),sum,z)
     if(true(),sum,z) -> aver(sum,s(z))
     if(false(),sum,z) -> z
    Subterm Criterion Processor:
     simple projection:
      pi(plus#) = 0
     problem:
      DPs:
       
      TRS:
       gt(0(),y) -> false()
       gt(s(x),0()) -> true()
       gt(s(x),s(y)) -> gt(x,y)
       plus(0(),y) -> y
       plus(s(x),y) -> s(plus(x,y))
       double(0()) -> 0()
       double(s(x)) -> s(s(double(x)))
       average(x,y) -> aver(plus(x,y),0())
       aver(sum,z) -> if(gt(sum,double(z)),sum,z)
       if(true(),sum,z) -> aver(sum,s(z))
       if(false(),sum,z) -> z
     Qed
    
    DPs:
     if#(true(),sum,z) -> aver#(sum,s(z))
     aver#(sum,z) -> if#(gt(sum,double(z)),sum,z)
    TRS:
     gt(0(),y) -> false()
     gt(s(x),0()) -> true()
     gt(s(x),s(y)) -> gt(x,y)
     plus(0(),y) -> y
     plus(s(x),y) -> s(plus(x,y))
     double(0()) -> 0()
     double(s(x)) -> s(s(double(x)))
     average(x,y) -> aver(plus(x,y),0())
     aver(sum,z) -> if(gt(sum,double(z)),sum,z)
     if(true(),sum,z) -> aver(sum,s(z))
     if(false(),sum,z) -> z
    Open
    
    DPs:
     gt#(s(x),s(y)) -> gt#(x,y)
    TRS:
     gt(0(),y) -> false()
     gt(s(x),0()) -> true()
     gt(s(x),s(y)) -> gt(x,y)
     plus(0(),y) -> y
     plus(s(x),y) -> s(plus(x,y))
     double(0()) -> 0()
     double(s(x)) -> s(s(double(x)))
     average(x,y) -> aver(plus(x,y),0())
     aver(sum,z) -> if(gt(sum,double(z)),sum,z)
     if(true(),sum,z) -> aver(sum,s(z))
     if(false(),sum,z) -> z
    Subterm Criterion Processor:
     simple projection:
      pi(gt#) = 1
     problem:
      DPs:
       
      TRS:
       gt(0(),y) -> false()
       gt(s(x),0()) -> true()
       gt(s(x),s(y)) -> gt(x,y)
       plus(0(),y) -> y
       plus(s(x),y) -> s(plus(x,y))
       double(0()) -> 0()
       double(s(x)) -> s(s(double(x)))
       average(x,y) -> aver(plus(x,y),0())
       aver(sum,z) -> if(gt(sum,double(z)),sum,z)
       if(true(),sum,z) -> aver(sum,s(z))
       if(false(),sum,z) -> z
     Qed
    
    DPs:
     double#(s(x)) -> double#(x)
    TRS:
     gt(0(),y) -> false()
     gt(s(x),0()) -> true()
     gt(s(x),s(y)) -> gt(x,y)
     plus(0(),y) -> y
     plus(s(x),y) -> s(plus(x,y))
     double(0()) -> 0()
     double(s(x)) -> s(s(double(x)))
     average(x,y) -> aver(plus(x,y),0())
     aver(sum,z) -> if(gt(sum,double(z)),sum,z)
     if(true(),sum,z) -> aver(sum,s(z))
     if(false(),sum,z) -> z
    Subterm Criterion Processor:
     simple projection:
      pi(double#) = 0
     problem:
      DPs:
       
      TRS:
       gt(0(),y) -> false()
       gt(s(x),0()) -> true()
       gt(s(x),s(y)) -> gt(x,y)
       plus(0(),y) -> y
       plus(s(x),y) -> s(plus(x,y))
       double(0()) -> 0()
       double(s(x)) -> s(s(double(x)))
       average(x,y) -> aver(plus(x,y),0())
       aver(sum,z) -> if(gt(sum,double(z)),sum,z)
       if(true(),sum,z) -> aver(sum,s(z))
       if(false(),sum,z) -> z
     Qed