TRS:
 {          diff(x, y) -> cond1(equal(x, y), x, y),
   cond1(true(), x, y) -> 0(),
  cond1(false(), x, y) -> cond2(gt(x, y), x, y),
   cond2(true(), x, y) -> s(diff(x, s(y))),
  cond2(false(), x, y) -> s(diff(s(x), y)),
            gt(0(), v) -> false(),
         gt(s(u), 0()) -> true(),
        gt(s(u), s(v)) -> gt(u, v),
       equal(0(), 0()) -> true(),
      equal(s(x), 0()) -> false(),
      equal(0(), s(y)) -> false(),
     equal(s(x), s(y)) -> equal(x, y)}
 Fail