MAYBE
TRS:
 { cond1(true(), x, y) -> 0(),
  cond1(false(), x, y) -> cond2(gt(x, y), x, y),
       equal(0(), 0()) -> true(),
      equal(0(), s(y)) -> false(),
      equal(s(x), 0()) -> false(),
     equal(s(x), s(y)) -> equal(x, y),
            diff(x, y) -> cond1(equal(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)}
 DP:
  Strict:
   {cond1#(false(), x, y) -> cond2#(gt(x, y), x, y),
    cond1#(false(), x, y) -> gt#(x, y),
       equal#(s(x), s(y)) -> equal#(x, y),
              diff#(x, y) -> cond1#(equal(x, y), x, y),
              diff#(x, y) -> equal#(x, y),
     cond2#(true(), x, y) -> diff#(x, s(y)),
    cond2#(false(), x, y) -> diff#(s(x), y),
          gt#(s(u), s(v)) -> gt#(u, v)}
  Weak:
  { cond1(true(), x, y) -> 0(),
   cond1(false(), x, y) -> cond2(gt(x, y), x, y),
        equal(0(), 0()) -> true(),
       equal(0(), s(y)) -> false(),
       equal(s(x), 0()) -> false(),
      equal(s(x), s(y)) -> equal(x, y),
             diff(x, y) -> cond1(equal(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)}
  EDG:
   {(diff#(x, y) -> cond1#(equal(x, y), x, y), cond1#(false(), x, y) -> gt#(x, y))
    (diff#(x, y) -> cond1#(equal(x, y), x, y), cond1#(false(), x, y) -> cond2#(gt(x, y), x, y))
    (cond2#(false(), x, y) -> diff#(s(x), y), diff#(x, y) -> equal#(x, y))
    (cond2#(false(), x, y) -> diff#(s(x), y), diff#(x, y) -> cond1#(equal(x, y), x, y))
    (cond1#(false(), x, y) -> gt#(x, y), gt#(s(u), s(v)) -> gt#(u, v))
    (diff#(x, y) -> equal#(x, y), equal#(s(x), s(y)) -> equal#(x, y))
    (equal#(s(x), s(y)) -> equal#(x, y), equal#(s(x), s(y)) -> equal#(x, y))
    (cond2#(true(), x, y) -> diff#(x, s(y)), diff#(x, y) -> cond1#(equal(x, y), x, y))
    (cond2#(true(), x, y) -> diff#(x, s(y)), diff#(x, y) -> equal#(x, y))
    (gt#(s(u), s(v)) -> gt#(u, v), gt#(s(u), s(v)) -> gt#(u, v))
    (cond1#(false(), x, y) -> cond2#(gt(x, y), x, y), cond2#(true(), x, y) -> diff#(x, s(y)))
    (cond1#(false(), x, y) -> cond2#(gt(x, y), x, y), cond2#(false(), x, y) -> diff#(s(x), y))}
   SCCS:
    Scc:
     {gt#(s(u), s(v)) -> gt#(u, v)}
    Scc:
     {equal#(s(x), s(y)) -> equal#(x, y)}
    Scc:
     {cond1#(false(), x, y) -> cond2#(gt(x, y), x, y),
                diff#(x, y) -> cond1#(equal(x, y), x, y),
       cond2#(true(), x, y) -> diff#(x, s(y)),
      cond2#(false(), x, y) -> diff#(s(x), y)}
    SCC:
     Strict:
      {gt#(s(u), s(v)) -> gt#(u, v)}
     Weak:
     { cond1(true(), x, y) -> 0(),
      cond1(false(), x, y) -> cond2(gt(x, y), x, y),
           equal(0(), 0()) -> true(),
          equal(0(), s(y)) -> false(),
          equal(s(x), 0()) -> false(),
         equal(s(x), s(y)) -> equal(x, y),
                diff(x, y) -> cond1(equal(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)}
     SPSC:
      Simple Projection:
       pi(gt#) = 0
      Strict:
       {}
      Qed
    SCC:
     Strict:
      {equal#(s(x), s(y)) -> equal#(x, y)}
     Weak:
     { cond1(true(), x, y) -> 0(),
      cond1(false(), x, y) -> cond2(gt(x, y), x, y),
           equal(0(), 0()) -> true(),
          equal(0(), s(y)) -> false(),
          equal(s(x), 0()) -> false(),
         equal(s(x), s(y)) -> equal(x, y),
                diff(x, y) -> cond1(equal(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)}
     SPSC:
      Simple Projection:
       pi(equal#) = 0
      Strict:
       {}
      Qed
    SCC:
     Strict:
      {cond1#(false(), x, y) -> cond2#(gt(x, y), x, y),
                 diff#(x, y) -> cond1#(equal(x, y), x, y),
        cond2#(true(), x, y) -> diff#(x, s(y)),
       cond2#(false(), x, y) -> diff#(s(x), y)}
     Weak:
     { cond1(true(), x, y) -> 0(),
      cond1(false(), x, y) -> cond2(gt(x, y), x, y),
           equal(0(), 0()) -> true(),
          equal(0(), s(y)) -> false(),
          equal(s(x), 0()) -> false(),
         equal(s(x), s(y)) -> equal(x, y),
                diff(x, y) -> cond1(equal(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)}
     Fail