MAYBE
MAYBE
TRS:
 {
  f(true(), x, y, z) -> f(gt(x, plus(y, z)), x, y, s(z)),
  f(true(), x, y, z) -> f(gt(x, plus(y, z)), x, s(y), z),
      gt(s(u), s(v)) -> gt(u, v),
       gt(s(u), 0()) -> true(),
          gt(0(), v) -> false(),
       plus(n, s(m)) -> s(plus(n, m)),
        plus(n, 0()) -> n
 }
 DUP: We consider a duplicating system.
  Trs:
   {
    f(true(), x, y, z) -> f(gt(x, plus(y, z)), x, y, s(z)),
    f(true(), x, y, z) -> f(gt(x, plus(y, z)), x, s(y), z),
        gt(s(u), s(v)) -> gt(u, v),
         gt(s(u), 0()) -> true(),
            gt(0(), v) -> false(),
         plus(n, s(m)) -> s(plus(n, m)),
          plus(n, 0()) -> n
   }
  Fail