MAYBE
TRS:
 {           le(0(), y) -> true(),
          le(s(x), 0()) -> false(),
         le(s(x), s(y)) -> le(x, y),
             pred(s(x)) -> x,
          minus(x, 0()) -> x,
         minus(x, s(y)) -> pred(minus(x, y)),
            gcd(0(), y) -> y,
         gcd(s(x), 0()) -> s(x),
        gcd(s(x), s(y)) -> if_gcd(le(y, x), s(x), s(y)),
   if_gcd(true(), x, y) -> gcd(minus(x, y), y),
  if_gcd(false(), x, y) -> gcd(minus(y, x), x)}
 DP:
  Strict:
   {       le#(s(x), s(y)) -> le#(x, y),
           minus#(x, s(y)) -> pred#(minus(x, y)),
           minus#(x, s(y)) -> minus#(x, y),
          gcd#(s(x), s(y)) -> le#(y, x),
          gcd#(s(x), s(y)) -> if_gcd#(le(y, x), s(x), s(y)),
     if_gcd#(true(), x, y) -> minus#(x, y),
     if_gcd#(true(), x, y) -> gcd#(minus(x, y), y),
    if_gcd#(false(), x, y) -> minus#(y, x),
    if_gcd#(false(), x, y) -> gcd#(minus(y, x), x)}
  Weak:
  {           le(0(), y) -> true(),
           le(s(x), 0()) -> false(),
          le(s(x), s(y)) -> le(x, y),
              pred(s(x)) -> x,
           minus(x, 0()) -> x,
          minus(x, s(y)) -> pred(minus(x, y)),
             gcd(0(), y) -> y,
          gcd(s(x), 0()) -> s(x),
         gcd(s(x), s(y)) -> if_gcd(le(y, x), s(x), s(y)),
    if_gcd(true(), x, y) -> gcd(minus(x, y), y),
   if_gcd(false(), x, y) -> gcd(minus(y, x), x)}
  EDG:
   {(gcd#(s(x), s(y)) -> le#(y, x), le#(s(x), s(y)) -> le#(x, y))
    (if_gcd#(false(), x, y) -> minus#(y, x), minus#(x, s(y)) -> minus#(x, y))
    (if_gcd#(false(), x, y) -> minus#(y, x), minus#(x, s(y)) -> pred#(minus(x, y)))
    (minus#(x, s(y)) -> minus#(x, y), minus#(x, s(y)) -> minus#(x, y))
    (minus#(x, s(y)) -> minus#(x, y), minus#(x, s(y)) -> pred#(minus(x, y)))
    (gcd#(s(x), s(y)) -> if_gcd#(le(y, x), s(x), s(y)), if_gcd#(true(), x, y) -> minus#(x, y))
    (gcd#(s(x), s(y)) -> if_gcd#(le(y, x), s(x), s(y)), if_gcd#(true(), x, y) -> gcd#(minus(x, y), y))
    (gcd#(s(x), s(y)) -> if_gcd#(le(y, x), s(x), s(y)), if_gcd#(false(), x, y) -> minus#(y, x))
    (gcd#(s(x), s(y)) -> if_gcd#(le(y, x), s(x), s(y)), if_gcd#(false(), x, y) -> gcd#(minus(y, x), x))
    (if_gcd#(true(), x, y) -> minus#(x, y), minus#(x, s(y)) -> pred#(minus(x, y)))
    (if_gcd#(true(), x, y) -> minus#(x, y), minus#(x, s(y)) -> minus#(x, y))
    (le#(s(x), s(y)) -> le#(x, y), le#(s(x), s(y)) -> le#(x, y))
    (if_gcd#(true(), x, y) -> gcd#(minus(x, y), y), gcd#(s(x), s(y)) -> le#(y, x))
    (if_gcd#(true(), x, y) -> gcd#(minus(x, y), y), gcd#(s(x), s(y)) -> if_gcd#(le(y, x), s(x), s(y)))
    (if_gcd#(false(), x, y) -> gcd#(minus(y, x), x), gcd#(s(x), s(y)) -> le#(y, x))
    (if_gcd#(false(), x, y) -> gcd#(minus(y, x), x), gcd#(s(x), s(y)) -> if_gcd#(le(y, x), s(x), s(y)))}
   SCCS:
    Scc:
     {      gcd#(s(x), s(y)) -> if_gcd#(le(y, x), s(x), s(y)),
       if_gcd#(true(), x, y) -> gcd#(minus(x, y), y),
      if_gcd#(false(), x, y) -> gcd#(minus(y, x), x)}
    Scc:
     {minus#(x, s(y)) -> minus#(x, y)}
    Scc:
     {le#(s(x), s(y)) -> le#(x, y)}
    SCC:
     Strict:
      {      gcd#(s(x), s(y)) -> if_gcd#(le(y, x), s(x), s(y)),
        if_gcd#(true(), x, y) -> gcd#(minus(x, y), y),
       if_gcd#(false(), x, y) -> gcd#(minus(y, x), x)}
     Weak:
     {           le(0(), y) -> true(),
              le(s(x), 0()) -> false(),
             le(s(x), s(y)) -> le(x, y),
                 pred(s(x)) -> x,
              minus(x, 0()) -> x,
             minus(x, s(y)) -> pred(minus(x, y)),
                gcd(0(), y) -> y,
             gcd(s(x), 0()) -> s(x),
            gcd(s(x), s(y)) -> if_gcd(le(y, x), s(x), s(y)),
       if_gcd(true(), x, y) -> gcd(minus(x, y), y),
      if_gcd(false(), x, y) -> gcd(minus(y, x), x)}
     Fail
    SCC:
     Strict:
      {minus#(x, s(y)) -> minus#(x, y)}
     Weak:
     {           le(0(), y) -> true(),
              le(s(x), 0()) -> false(),
             le(s(x), s(y)) -> le(x, y),
                 pred(s(x)) -> x,
              minus(x, 0()) -> x,
             minus(x, s(y)) -> pred(minus(x, y)),
                gcd(0(), y) -> y,
             gcd(s(x), 0()) -> s(x),
            gcd(s(x), s(y)) -> if_gcd(le(y, x), s(x), s(y)),
       if_gcd(true(), x, y) -> gcd(minus(x, y), y),
      if_gcd(false(), x, y) -> gcd(minus(y, x), x)}
     SPSC:
      Simple Projection:
       pi(minus#) = 1
      Strict:
       {}
      Qed
    SCC:
     Strict:
      {le#(s(x), s(y)) -> le#(x, y)}
     Weak:
     {           le(0(), y) -> true(),
              le(s(x), 0()) -> false(),
             le(s(x), s(y)) -> le(x, y),
                 pred(s(x)) -> x,
              minus(x, 0()) -> x,
             minus(x, s(y)) -> pred(minus(x, y)),
                gcd(0(), y) -> y,
             gcd(s(x), 0()) -> s(x),
            gcd(s(x), s(y)) -> if_gcd(le(y, x), s(x), s(y)),
       if_gcd(true(), x, y) -> gcd(minus(x, y), y),
      if_gcd(false(), x, y) -> gcd(minus(y, x), x)}
     SPSC:
      Simple Projection:
       pi(le#) = 0
      Strict:
       {}
      Qed