MAYBE
TRS:
 {                      p(s(x)) -> x,
                         p(0()) -> 0(),
                 le(s(x), s(y)) -> le(x, y),
                  le(s(x), 0()) -> false(),
                     le(0(), y) -> true(),
   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)),
                  average(x, y) -> if(le(x, 0()), le(y, 0()), le(y, s(0())), le(y, s(s(0()))), x, 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)))}
 DP:
  Strict:
   {               le#(s(x), s(y)) -> le#(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)),
                    average#(x, y) -> le#(x, 0()),
                    average#(x, y) -> le#(y, s(s(0()))),
                    average#(x, y) -> le#(y, s(0())),
                    average#(x, y) -> le#(y, 0()),
                    average#(x, y) -> if#(le(x, 0()), le(y, 0()), le(y, s(0())), le(y, s(s(0()))), x, 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)))}
  Weak:
  {                      p(s(x)) -> x,
                          p(0()) -> 0(),
                  le(s(x), s(y)) -> le(x, y),
                   le(s(x), 0()) -> false(),
                      le(0(), y) -> true(),
    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)),
                   average(x, y) -> if(le(x, 0()), le(y, 0()), le(y, s(0())), le(y, s(s(0()))), x, 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)))}
  EDG:
   {(average#(x, y) -> le#(y, 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))
    (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))
    (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#(x, 0()))
    (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) -> 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))))
    (if#(true(), b1, b2, b3, x, y) -> if2#(b1, b2, b3, x, y), if2#(false(), b2, b3, x, y) -> if3#(b2, b3, 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, 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) -> if#(le(x, 0()), le(y, 0()), le(y, s(0())), le(y, s(s(0()))), x, y))
    (average#(x, y) -> le#(y, s(s(0()))), le#(s(x), s(y)) -> le#(x, y))}
   SCCS:
    Scc:
     { 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)),
                      average#(x, y) -> if#(le(x, 0()), le(y, 0()), le(y, s(0())), le(y, s(s(0()))), x, 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) -> average#(s(x), p(p(y)))}
    Scc:
     {le#(s(x), s(y)) -> le#(x, y)}
    SCC:
     Strict:
      { 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)),
                       average#(x, y) -> if#(le(x, 0()), le(y, 0()), le(y, s(0())), le(y, s(s(0()))), x, 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) -> average#(s(x), p(p(y)))}
     Weak:
     {                      p(s(x)) -> x,
                             p(0()) -> 0(),
                     le(s(x), s(y)) -> le(x, y),
                      le(s(x), 0()) -> false(),
                         le(0(), y) -> true(),
       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)),
                      average(x, y) -> if(le(x, 0()), le(y, 0()), le(y, s(0())), le(y, s(s(0()))), x, 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)))}
     Fail
    SCC:
     Strict:
      {le#(s(x), s(y)) -> le#(x, y)}
     Weak:
     {                      p(s(x)) -> x,
                             p(0()) -> 0(),
                     le(s(x), s(y)) -> le(x, y),
                      le(s(x), 0()) -> false(),
                         le(0(), y) -> true(),
       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)),
                      average(x, y) -> if(le(x, 0()), le(y, 0()), le(y, s(0())), le(y, s(s(0()))), x, 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)))}
     SPSC:
      Simple Projection:
       pi(le#) = 1
      Strict:
       {}
      Qed