MAYBE

Problem:
 p(s(x)) -> x
 p(0()) -> 0()
 le(0(),y) -> true()
 le(s(x),0()) -> false()
 le(s(x),s(y)) -> le(x,y)
 average(x,y) -> if(le(x,0()),le(y,0()),le(y,s(0())),le(y,s(s(0()))),x,y)
 if(true(),b1,b2,b3,x,y) -> if2(b1,b2,b3,x,y)
 if(false(),b1,b2,b3,x,y) -> average(p(x),s(y))
 if2(true(),b2,b3,x,y) -> 0()
 if2(false(),b2,b3,x,y) -> if3(b2,b3,x,y)
 if3(true(),b3,x,y) -> 0()
 if3(false(),b3,x,y) -> if4(b3,x,y)
 if4(true(),x,y) -> s(0())
 if4(false(),x,y) -> average(s(x),p(p(y)))

Proof:
 DP Processor:
  DPs:
   le#(s(x),s(y)) -> le#(x,y)
   average#(x,y) -> le#(y,s(s(0())))
   average#(x,y) -> le#(y,s(0()))
   average#(x,y) -> le#(y,0())
   average#(x,y) -> le#(x,0())
   average#(x,y) -> if#(le(x,0()),le(y,0()),le(y,s(0())),le(y,s(s(0()))),x,y)
   if#(true(),b1,b2,b3,x,y) -> if2#(b1,b2,b3,x,y)
   if#(false(),b1,b2,b3,x,y) -> p#(x)
   if#(false(),b1,b2,b3,x,y) -> average#(p(x),s(y))
   if2#(false(),b2,b3,x,y) -> if3#(b2,b3,x,y)
   if3#(false(),b3,x,y) -> if4#(b3,x,y)
   if4#(false(),x,y) -> p#(y)
   if4#(false(),x,y) -> p#(p(y))
   if4#(false(),x,y) -> average#(s(x),p(p(y)))
  TRS:
   p(s(x)) -> x
   p(0()) -> 0()
   le(0(),y) -> true()
   le(s(x),0()) -> false()
   le(s(x),s(y)) -> le(x,y)
   average(x,y) -> if(le(x,0()),le(y,0()),le(y,s(0())),le(y,s(s(0()))),x,y)
   if(true(),b1,b2,b3,x,y) -> if2(b1,b2,b3,x,y)
   if(false(),b1,b2,b3,x,y) -> average(p(x),s(y))
   if2(true(),b2,b3,x,y) -> 0()
   if2(false(),b2,b3,x,y) -> if3(b2,b3,x,y)
   if3(true(),b3,x,y) -> 0()
   if3(false(),b3,x,y) -> if4(b3,x,y)
   if4(true(),x,y) -> s(0())
   if4(false(),x,y) -> average(s(x),p(p(y)))
  TDG Processor:
   DPs:
    le#(s(x),s(y)) -> le#(x,y)
    average#(x,y) -> le#(y,s(s(0())))
    average#(x,y) -> le#(y,s(0()))
    average#(x,y) -> le#(y,0())
    average#(x,y) -> le#(x,0())
    average#(x,y) -> if#(le(x,0()),le(y,0()),le(y,s(0())),le(y,s(s(0()))),x,y)
    if#(true(),b1,b2,b3,x,y) -> if2#(b1,b2,b3,x,y)
    if#(false(),b1,b2,b3,x,y) -> p#(x)
    if#(false(),b1,b2,b3,x,y) -> average#(p(x),s(y))
    if2#(false(),b2,b3,x,y) -> if3#(b2,b3,x,y)
    if3#(false(),b3,x,y) -> if4#(b3,x,y)
    if4#(false(),x,y) -> p#(y)
    if4#(false(),x,y) -> p#(p(y))
    if4#(false(),x,y) -> average#(s(x),p(p(y)))
   TRS:
    p(s(x)) -> x
    p(0()) -> 0()
    le(0(),y) -> true()
    le(s(x),0()) -> false()
    le(s(x),s(y)) -> le(x,y)
    average(x,y) -> if(le(x,0()),le(y,0()),le(y,s(0())),le(y,s(s(0()))),x,y)
    if(true(),b1,b2,b3,x,y) -> if2(b1,b2,b3,x,y)
    if(false(),b1,b2,b3,x,y) -> average(p(x),s(y))
    if2(true(),b2,b3,x,y) -> 0()
    if2(false(),b2,b3,x,y) -> if3(b2,b3,x,y)
    if3(true(),b3,x,y) -> 0()
    if3(false(),b3,x,y) -> if4(b3,x,y)
    if4(true(),x,y) -> s(0())
    if4(false(),x,y) -> average(s(x),p(p(y)))
   graph:
    if4#(false(),x,y) -> average#(s(x),p(p(y))) ->
    average#(x,y) -> if#(le(x,0()),le(y,0()),le(y,s(0())),le(y,s(s(0()))),x,y)
    if4#(false(),x,y) -> average#(s(x),p(p(y))) ->
    average#(x,y) -> le#(x,0())
    if4#(false(),x,y) -> average#(s(x),p(p(y))) ->
    average#(x,y) -> le#(y,0())
    if4#(false(),x,y) -> average#(s(x),p(p(y))) ->
    average#(x,y) -> le#(y,s(0()))
    if4#(false(),x,y) -> average#(s(x),p(p(y))) ->
    average#(x,y) -> le#(y,s(s(0())))
    if3#(false(),b3,x,y) -> if4#(b3,x,y) ->
    if4#(false(),x,y) -> average#(s(x),p(p(y)))
    if3#(false(),b3,x,y) -> if4#(b3,x,y) ->
    if4#(false(),x,y) -> p#(p(y))
    if3#(false(),b3,x,y) -> if4#(b3,x,y) ->
    if4#(false(),x,y) -> p#(y)
    if2#(false(),b2,b3,x,y) -> if3#(b2,b3,x,y) ->
    if3#(false(),b3,x,y) -> if4#(b3,x,y)
    if#(false(),b1,b2,b3,x,y) -> average#(p(x),s(y)) ->
    average#(x,y) -> if#(le(x,0()),le(y,0()),le(y,s(0())),le(y,s(s(0()))),x,y)
    if#(false(),b1,b2,b3,x,y) -> average#(p(x),s(y)) ->
    average#(x,y) -> le#(x,0())
    if#(false(),b1,b2,b3,x,y) -> average#(p(x),s(y)) ->
    average#(x,y) -> le#(y,0())
    if#(false(),b1,b2,b3,x,y) -> average#(p(x),s(y)) ->
    average#(x,y) -> le#(y,s(0()))
    if#(false(),b1,b2,b3,x,y) -> average#(p(x),s(y)) ->
    average#(x,y) -> le#(y,s(s(0())))
    if#(true(),b1,b2,b3,x,y) -> if2#(b1,b2,b3,x,y) ->
    if2#(false(),b2,b3,x,y) -> if3#(b2,b3,x,y)
    average#(x,y) -> if#(le(x,0()),le(y,0()),le(y,s(0())),le(y,s(s(0()))),x,y) ->
    if#(false(),b1,b2,b3,x,y) -> average#(p(x),s(y))
    average#(x,y) -> if#(le(x,0()),le(y,0()),le(y,s(0())),le(y,s(s(0()))),x,y) ->
    if#(false(),b1,b2,b3,x,y) -> p#(x)
    average#(x,y) -> if#(le(x,0()),le(y,0()),le(y,s(0())),le(y,s(s(0()))),x,y) ->
    if#(true(),b1,b2,b3,x,y) -> if2#(b1,b2,b3,x,y)
    average#(x,y) -> le#(y,0()) -> le#(s(x),s(y)) -> le#(x,y)
    average#(x,y) -> le#(y,s(0())) -> le#(s(x),s(y)) -> le#(x,y)
    average#(x,y) -> le#(y,s(s(0()))) -> le#(s(x),s(y)) -> le#(x,y)
    average#(x,y) -> le#(x,0()) -> le#(s(x),s(y)) -> le#(x,y)
    le#(s(x),s(y)) -> le#(x,y) -> le#(s(x),s(y)) -> le#(x,y)
   EDG Processor:
    DPs:
     le#(s(x),s(y)) -> le#(x,y)
     average#(x,y) -> le#(y,s(s(0())))
     average#(x,y) -> le#(y,s(0()))
     average#(x,y) -> le#(y,0())
     average#(x,y) -> le#(x,0())
     average#(x,y) -> if#(le(x,0()),le(y,0()),le(y,s(0())),le(y,s(s(0()))),x,y)
     if#(true(),b1,b2,b3,x,y) -> if2#(b1,b2,b3,x,y)
     if#(false(),b1,b2,b3,x,y) -> p#(x)
     if#(false(),b1,b2,b3,x,y) -> average#(p(x),s(y))
     if2#(false(),b2,b3,x,y) -> if3#(b2,b3,x,y)
     if3#(false(),b3,x,y) -> if4#(b3,x,y)
     if4#(false(),x,y) -> p#(y)
     if4#(false(),x,y) -> p#(p(y))
     if4#(false(),x,y) -> average#(s(x),p(p(y)))
    TRS:
     p(s(x)) -> x
     p(0()) -> 0()
     le(0(),y) -> true()
     le(s(x),0()) -> false()
     le(s(x),s(y)) -> le(x,y)
     average(x,y) -> if(le(x,0()),le(y,0()),le(y,s(0())),le(y,s(s(0()))),x,y)
     if(true(),b1,b2,b3,x,y) -> if2(b1,b2,b3,x,y)
     if(false(),b1,b2,b3,x,y) -> average(p(x),s(y))
     if2(true(),b2,b3,x,y) -> 0()
     if2(false(),b2,b3,x,y) -> if3(b2,b3,x,y)
     if3(true(),b3,x,y) -> 0()
     if3(false(),b3,x,y) -> if4(b3,x,y)
     if4(true(),x,y) -> s(0())
     if4(false(),x,y) -> average(s(x),p(p(y)))
    graph:
     if4#(false(),x,y) -> average#(s(x),p(p(y))) ->
     average#(x,y) -> le#(y,s(s(0())))
     if4#(false(),x,y) -> average#(s(x),p(p(y))) ->
     average#(x,y) -> le#(y,s(0()))
     if4#(false(),x,y) -> average#(s(x),p(p(y))) ->
     average#(x,y) -> le#(y,0())
     if4#(false(),x,y) -> average#(s(x),p(p(y))) ->
     average#(x,y) -> le#(x,0())
     if4#(false(),x,y) -> average#(s(x),p(p(y))) ->
     average#(x,y) -> if#(le(x,0()),le(y,0()),le(y,s(0())),le(y,s(s(0()))),x,y)
     if3#(false(),b3,x,y) -> if4#(b3,x,y) ->
     if4#(false(),x,y) -> p#(y)
     if3#(false(),b3,x,y) -> if4#(b3,x,y) ->
     if4#(false(),x,y) -> p#(p(y))
     if3#(false(),b3,x,y) -> if4#(b3,x,y) ->
     if4#(false(),x,y) -> average#(s(x),p(p(y)))
     if2#(false(),b2,b3,x,y) -> if3#(b2,b3,x,y) ->
     if3#(false(),b3,x,y) -> if4#(b3,x,y)
     if#(false(),b1,b2,b3,x,y) -> average#(p(x),s(y)) ->
     average#(x,y) -> le#(y,s(s(0())))
     if#(false(),b1,b2,b3,x,y) -> average#(p(x),s(y)) ->
     average#(x,y) -> le#(y,s(0()))
     if#(false(),b1,b2,b3,x,y) -> average#(p(x),s(y)) ->
     average#(x,y) -> le#(y,0())
     if#(false(),b1,b2,b3,x,y) -> average#(p(x),s(y)) ->
     average#(x,y) -> le#(x,0())
     if#(false(),b1,b2,b3,x,y) -> average#(p(x),s(y)) ->
     average#(x,y) -> if#(le(x,0()),le(y,0()),le(y,s(0())),le(y,s(s(0()))),x,y)
     if#(true(),b1,b2,b3,x,y) -> if2#(b1,b2,b3,x,y) ->
     if2#(false(),b2,b3,x,y) -> if3#(b2,b3,x,y)
     average#(x,y) -> if#(le(x,0()),le(y,0()),le(y,s(0())),le(y,s(s(0()))),x,y) ->
     if#(true(),b1,b2,b3,x,y) -> if2#(b1,b2,b3,x,y)
     average#(x,y) -> if#(le(x,0()),le(y,0()),le(y,s(0())),le(y,s(s(0()))),x,y) ->
     if#(false(),b1,b2,b3,x,y) -> p#(x)
     average#(x,y) -> if#(le(x,0()),le(y,0()),le(y,s(0())),le(y,s(s(0()))),x,y) ->
     if#(false(),b1,b2,b3,x,y) -> average#(p(x),s(y))
     average#(x,y) -> le#(y,s(0())) -> le#(s(x),s(y)) -> le#(x,y)
     average#(x,y) -> le#(y,s(s(0()))) -> le#(s(x),s(y)) -> le#(x,y)
     le#(s(x),s(y)) -> le#(x,y) -> le#(s(x),s(y)) -> le#(x,y)
    SCC Processor:
     #sccs: 2
     #rules: 7
     #arcs: 21/196
     DPs:
      if4#(false(),x,y) -> average#(s(x),p(p(y)))
      average#(x,y) -> if#(le(x,0()),le(y,0()),le(y,s(0())),le(y,s(s(0()))),x,y)
      if#(false(),b1,b2,b3,x,y) -> average#(p(x),s(y))
      if#(true(),b1,b2,b3,x,y) -> if2#(b1,b2,b3,x,y)
      if2#(false(),b2,b3,x,y) -> if3#(b2,b3,x,y)
      if3#(false(),b3,x,y) -> if4#(b3,x,y)
     TRS:
      p(s(x)) -> x
      p(0()) -> 0()
      le(0(),y) -> true()
      le(s(x),0()) -> false()
      le(s(x),s(y)) -> le(x,y)
      average(x,y) -> if(le(x,0()),le(y,0()),le(y,s(0())),le(y,s(s(0()))),x,y)
      if(true(),b1,b2,b3,x,y) -> if2(b1,b2,b3,x,y)
      if(false(),b1,b2,b3,x,y) -> average(p(x),s(y))
      if2(true(),b2,b3,x,y) -> 0()
      if2(false(),b2,b3,x,y) -> if3(b2,b3,x,y)
      if3(true(),b3,x,y) -> 0()
      if3(false(),b3,x,y) -> if4(b3,x,y)
      if4(true(),x,y) -> s(0())
      if4(false(),x,y) -> average(s(x),p(p(y)))
     Open
     
     DPs:
      le#(s(x),s(y)) -> le#(x,y)
     TRS:
      p(s(x)) -> x
      p(0()) -> 0()
      le(0(),y) -> true()
      le(s(x),0()) -> false()
      le(s(x),s(y)) -> le(x,y)
      average(x,y) -> if(le(x,0()),le(y,0()),le(y,s(0())),le(y,s(s(0()))),x,y)
      if(true(),b1,b2,b3,x,y) -> if2(b1,b2,b3,x,y)
      if(false(),b1,b2,b3,x,y) -> average(p(x),s(y))
      if2(true(),b2,b3,x,y) -> 0()
      if2(false(),b2,b3,x,y) -> if3(b2,b3,x,y)
      if3(true(),b3,x,y) -> 0()
      if3(false(),b3,x,y) -> if4(b3,x,y)
      if4(true(),x,y) -> s(0())
      if4(false(),x,y) -> average(s(x),p(p(y)))
     Matrix Interpretation Processor: dim=1
      
      interpretation:
       [le#](x0, x1) = 3x0,
       
       [if4](x0, x1, x2) = 1,
       
       [if3](x0, x1, x2, x3) = x1 + 1,
       
       [if2](x0, x1, x2, x3, x4) = x2 + 1,
       
       [if](x0, x1, x2, x3, x4, x5) = x1 + 4x2 + x3 + 1,
       
       [average](x0, x1) = 1,
       
       [false] = 0,
       
       [true] = 0,
       
       [le](x0, x1) = 0,
       
       [0] = 0,
       
       [p](x0) = x0 + 6,
       
       [s](x0) = x0 + 1
      orientation:
       le#(s(x),s(y)) = 3x + 3 >= 3x = le#(x,y)
       
       p(s(x)) = x + 7 >= x = x
       
       p(0()) = 6 >= 0 = 0()
       
       le(0(),y) = 0 >= 0 = true()
       
       le(s(x),0()) = 0 >= 0 = false()
       
       le(s(x),s(y)) = 0 >= 0 = le(x,y)
       
       average(x,y) = 1 >= 1 = if(le(x,0()),le(y,0()),le(y,s(0())),le(y,s(s(0()))),x,y)
       
       if(true(),b1,b2,b3,x,y) = b1 + 4b2 + b3 + 1 >= b3 + 1 = if2(b1,b2,b3,x,y)
       
       if(false(),b1,b2,b3,x,y) = b1 + 4b2 + b3 + 1 >= 1 = average(p(x),s(y))
       
       if2(true(),b2,b3,x,y) = b3 + 1 >= 0 = 0()
       
       if2(false(),b2,b3,x,y) = b3 + 1 >= b3 + 1 = if3(b2,b3,x,y)
       
       if3(true(),b3,x,y) = b3 + 1 >= 0 = 0()
       
       if3(false(),b3,x,y) = b3 + 1 >= 1 = if4(b3,x,y)
       
       if4(true(),x,y) = 1 >= 1 = s(0())
       
       if4(false(),x,y) = 1 >= 1 = average(s(x),p(p(y)))
      problem:
       DPs:
        
       TRS:
        p(s(x)) -> x
        p(0()) -> 0()
        le(0(),y) -> true()
        le(s(x),0()) -> false()
        le(s(x),s(y)) -> le(x,y)
        average(x,y) -> if(le(x,0()),le(y,0()),le(y,s(0())),le(y,s(s(0()))),x,y)
        if(true(),b1,b2,b3,x,y) -> if2(b1,b2,b3,x,y)
        if(false(),b1,b2,b3,x,y) -> average(p(x),s(y))
        if2(true(),b2,b3,x,y) -> 0()
        if2(false(),b2,b3,x,y) -> if3(b2,b3,x,y)
        if3(true(),b3,x,y) -> 0()
        if3(false(),b3,x,y) -> if4(b3,x,y)
        if4(true(),x,y) -> s(0())
        if4(false(),x,y) -> average(s(x),p(p(y)))
      Qed