YES
Time: 0.013246
TRS:
 {  minus(x, 0()) -> x,
  minus(s x, s y) -> minus(x, y),
            f 0() -> s 0(),
            f s x -> minus(s x, g f x),
            g 0() -> 0(),
            g s x -> minus(s x, f g x)}
 DP:
  DP:
   {minus#(s x, s y) -> minus#(x, y),
              f# s x -> minus#(s x, g f x),
              f# s x -> f# x,
              f# s x -> g# f x,
              g# s x -> minus#(s x, f g x),
              g# s x -> f# g x,
              g# s x -> g# x}
  TRS:
  {  minus(x, 0()) -> x,
   minus(s x, s y) -> minus(x, y),
             f 0() -> s 0(),
             f s x -> minus(s x, g f x),
             g 0() -> 0(),
             g s x -> minus(s x, f g x)}
  EDG:
   {(g# s x -> minus#(s x, f g x), minus#(s x, s y) -> minus#(x, y))
    (g# s x -> g# x, g# s x -> g# x)
    (g# s x -> g# x, g# s x -> f# g x)
    (g# s x -> g# x, g# s x -> minus#(s x, f g x))
    (f# s x -> g# f x, g# s x -> g# x)
    (f# s x -> g# f x, g# s x -> f# g x)
    (f# s x -> g# f x, g# s x -> minus#(s x, f g x))
    (g# s x -> f# g x, f# s x -> minus#(s x, g f x))
    (g# s x -> f# g x, f# s x -> f# x)
    (g# s x -> f# g x, f# s x -> g# f x)
    (minus#(s x, s y) -> minus#(x, y), minus#(s x, s y) -> minus#(x, y))
    (f# s x -> f# x, f# s x -> minus#(s x, g f x))
    (f# s x -> f# x, f# s x -> f# x)
    (f# s x -> f# x, f# s x -> g# f x)
    (f# s x -> minus#(s x, g f x), minus#(s x, s y) -> minus#(x, y))}
   SCCS (2):
    Scc:
     {f# s x -> f# x,
      f# s x -> g# f x,
      g# s x -> f# g x,
      g# s x -> g# x}
    Scc:
     {minus#(s x, s y) -> minus#(x, y)}
    SCC (4):
     Strict:
      {f# s x -> f# x,
       f# s x -> g# f x,
       g# s x -> f# g x,
       g# s x -> g# x}
     Weak:
     {  minus(x, 0()) -> x,
      minus(s x, s y) -> minus(x, y),
                f 0() -> s 0(),
                f s x -> minus(s x, g f x),
                g 0() -> 0(),
                g s x -> minus(s x, f g x)}
     POLY:
      Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
      Interpretation:
       [minus](x0, x1) = x0,
       
       [s](x0) = x0 + 1,
       
       [f](x0) = x0 + 1,
       
       [g](x0) = x0 + 1,
       
       [0] = 1,
       
       [f#](x0) = x0 + 1,
       
       [g#](x0) = x0 + 1
      Strict:
       g# s x -> g# x
       2 + 1x >= 1 + 1x
       g# s x -> f# g x
       2 + 1x >= 2 + 1x
       f# s x -> g# f x
       2 + 1x >= 2 + 1x
       f# s x -> f# x
       2 + 1x >= 1 + 1x
      Weak:
       
     EDG:
      {(g# s x -> f# g x, f# s x -> g# f x)
       (f# s x -> g# f x, g# s x -> f# g x)}
      SCCS (1):
       Scc:
        {f# s x -> g# f x,
         g# s x -> f# g x}
       SCC (2):
        Strict:
         {f# s x -> g# f x,
          g# s x -> f# g x}
        Weak:
        {  minus(x, 0()) -> x,
         minus(s x, s y) -> minus(x, y),
                   f 0() -> s 0(),
                   f s x -> minus(s x, g f x),
                   g 0() -> 0(),
                   g s x -> minus(s x, f g x)}
        POLY:
         Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
         Interpretation:
          [minus](x0, x1) = x0,
          
          [s](x0) = x0 + 1,
          
          [f](x0) = x0 + 1,
          
          [g](x0) = x0,
          
          [0] = 1,
          
          [f#](x0) = x0 + 1,
          
          [g#](x0) = x0 + 1
         Strict:
          g# s x -> f# g x
          2 + 1x >= 1 + 1x
          f# s x -> g# f x
          2 + 1x >= 2 + 1x
         Weak:
          
        EDG:
         {}
         SCCS (0):
          
          Qed
   SCC (1):
    Strict:
     {minus#(s x, s y) -> minus#(x, y)}
    Weak:
    {  minus(x, 0()) -> x,
     minus(s x, s y) -> minus(x, y),
               f 0() -> s 0(),
               f s x -> minus(s x, g f x),
               g 0() -> 0(),
               g s x -> minus(s x, f g x)}
    SPSC:
     Simple Projection:
      pi(minus#) = 1
     Strict:
      {}
     Qed