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