YES
Time: 0.092204
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)}
  UR:
   {  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),
            a(z, w) -> z,
            a(z, w) -> w}
   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))}
    STATUS:
     arrows: 0.693878
     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:
         g s x -> minus(s x, f g x)
         2 + 1x >= 1 + 1x
         g 0() -> 0()
         2 >= 1
         f s x -> minus(s x, g f x)
         2 + 1x >= 1 + 1x
         f 0() -> s 0()
         2 >= 2
         minus(s x, s y) -> minus(x, y)
         1 + 1x + 0y >= 0 + 1x + 0y
         minus(x, 0()) -> x
         0 + 1x >= 1x
       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:
           g s x -> minus(s x, f g x)
           1 + 1x >= 1 + 1x
           g 0() -> 0()
           1 >= 1
           f s x -> minus(s x, g f x)
           2 + 1x >= 1 + 1x
           f 0() -> s 0()
           2 >= 2
           minus(s x, s y) -> minus(x, y)
           1 + 1x + 0y >= 0 + 1x + 0y
           minus(x, 0()) -> x
           0 + 1x >= 1x
         SCCS (0):
          
          
     
     
     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)}
      POLY:
       Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
       Interpretation:
        [minus](x0, x1) = x0 + 1,
        
        [s](x0) = x0 + 1,
        
        [f](x0) = 0,
        
        [g](x0) = 0,
        
        [0] = 1,
        
        [minus#](x0, x1) = x0
       Strict:
        minus#(s x, s y) -> minus#(x, y)
        1 + 0x + 1y >= 0 + 0x + 1y
       Weak:
        g s x -> minus(s x, f g x)
        0 + 0x >= 1 + 0x
        g 0() -> 0()
        0 >= 1
        f s x -> minus(s x, g f x)
        0 + 0x >= 1 + 0x
        f 0() -> s 0()
        0 >= 2
        minus(s x, s y) -> minus(x, y)
        2 + 0x + 1y >= 1 + 0x + 1y
        minus(x, 0()) -> x
        2 + 0x >= 1x
      Qed