YES
Time: 0.371167
TRS:
 {       f 0() -> 0(),
       f s 0() -> s 0(),
       f s s x -> p h g x,
       f s s x -> +(p g x, q g x),
  p pair(x, y) -> x,
           h x -> pair(+(p x, q x), p x),
         g 0() -> pair(s 0(), s 0()),
         g s x -> h g x,
         g s x -> pair(+(p g x, q g x), p g x),
     +(x, 0()) -> x,
     +(x, s y) -> s +(x, y),
  q pair(x, y) -> y}
 DP:
  DP:
   {  f# s s x -> p# h g x,
      f# s s x -> p# g x,
      f# s s x -> h# g x,
      f# s s x -> g# x,
      f# s s x -> +#(p g x, q g x),
      f# s s x -> q# g x,
          h# x -> p# x,
          h# x -> +#(p x, q x),
          h# x -> q# x,
        g# s x -> p# g x,
        g# s x -> h# g x,
        g# s x -> g# x,
        g# s x -> +#(p g x, q g x),
        g# s x -> q# g x,
    +#(x, s y) -> +#(x, y)}
  TRS:
  {       f 0() -> 0(),
        f s 0() -> s 0(),
        f s s x -> p h g x,
        f s s x -> +(p g x, q g x),
   p pair(x, y) -> x,
            h x -> pair(+(p x, q x), p x),
          g 0() -> pair(s 0(), s 0()),
          g s x -> h g x,
          g s x -> pair(+(p g x, q g x), p g x),
      +(x, 0()) -> x,
      +(x, s y) -> s +(x, y),
   q pair(x, y) -> y}
  UR:
   {p pair(x, y) -> x,
             h x -> pair(+(p x, q x), p x),
           g 0() -> pair(s 0(), s 0()),
           g s x -> h g x,
           g s x -> pair(+(p g x, q g x), p g x),
       +(x, 0()) -> x,
       +(x, s y) -> s +(x, y),
    q pair(x, y) -> y,
         a(z, w) -> z,
         a(z, w) -> w}
   EDG:
    {(g# s x -> +#(p g x, q g x), +#(x, s y) -> +#(x, y))
     (f# s s x -> h# g x, h# x -> q# x)
     (f# s s x -> h# g x, h# x -> +#(p x, q x))
     (f# s s x -> h# g x, h# x -> p# x)
     (g# s x -> g# x, g# s x -> q# g x)
     (g# s x -> g# x, g# s x -> +#(p g x, q g x))
     (g# s x -> g# x, g# s x -> g# x)
     (g# s x -> g# x, g# s x -> h# g x)
     (g# s x -> g# x, g# s x -> p# g x)
     (+#(x, s y) -> +#(x, y), +#(x, s y) -> +#(x, y))
     (f# s s x -> g# x, g# s x -> p# g x)
     (f# s s x -> g# x, g# s x -> h# g x)
     (f# s s x -> g# x, g# s x -> g# x)
     (f# s s x -> g# x, g# s x -> +#(p g x, q g x))
     (f# s s x -> g# x, g# s x -> q# g x)
     (g# s x -> h# g x, h# x -> p# x)
     (g# s x -> h# g x, h# x -> +#(p x, q x))
     (g# s x -> h# g x, h# x -> q# x)
     (h# x -> +#(p x, q x), +#(x, s y) -> +#(x, y))
     (f# s s x -> +#(p g x, q g x), +#(x, s y) -> +#(x, y))}
    STATUS:
     arrows: 0.911111
     SCCS (2):
      Scc:
       {g# s x -> g# x}
      Scc:
       {+#(x, s y) -> +#(x, y)}
      
      
      SCC (1):
       Strict:
        {g# s x -> g# x}
       Weak:
       {       f 0() -> 0(),
             f s 0() -> s 0(),
             f s s x -> p h g x,
             f s s x -> +(p g x, q g x),
        p pair(x, y) -> x,
                 h x -> pair(+(p x, q x), p x),
               g 0() -> pair(s 0(), s 0()),
               g s x -> h g x,
               g s x -> pair(+(p g x, q g x), p g x),
           +(x, 0()) -> x,
           +(x, s y) -> s +(x, y),
        q pair(x, y) -> y}
       POLY:
        Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
        Interpretation:
         [pair](x0, x1) = 0,
         
         [+](x0, x1) = x0 + x1 + 1,
         
         [f](x0) = x0 + 1,
         
         [s](x0) = x0 + 1,
         
         [p](x0) = x0,
         
         [h](x0) = x0 + 1,
         
         [g](x0) = 1,
         
         [q](x0) = x0 + 1,
         
         [0] = 1,
         
         [g#](x0) = x0 + 1
        Strict:
         g# s x -> g# x
         2 + 1x >= 1 + 1x
        Weak:
         q pair(x, y) -> y
         1 + 0x + 0y >= 1y
         +(x, s y) -> s +(x, y)
         2 + 1x + 1y >= 2 + 1x + 1y
         +(x, 0()) -> x
         2 + 1x >= 1x
         g s x -> pair(+(p g x, q g x), p g x)
         1 + 0x >= 0 + 0x
         g s x -> h g x
         1 + 0x >= 2 + 0x
         g 0() -> pair(s 0(), s 0())
         1 >= 0
         h x -> pair(+(p x, q x), p x)
         1 + 1x >= 0 + 0x
         p pair(x, y) -> x
         0 + 0x + 0y >= 1x
         f s s x -> +(p g x, q g x)
         3 + 1x >= 4 + 0x
         f s s x -> p h g x
         3 + 1x >= 2 + 0x
         f s 0() -> s 0()
         3 >= 2
         f 0() -> 0()
         2 >= 1
       Qed
     
     
     
     
     
     
     
     
     
     
     
     
     SCC (1):
      Strict:
       {+#(x, s y) -> +#(x, y)}
      Weak:
      {       f 0() -> 0(),
            f s 0() -> s 0(),
            f s s x -> p h g x,
            f s s x -> +(p g x, q g x),
       p pair(x, y) -> x,
                h x -> pair(+(p x, q x), p x),
              g 0() -> pair(s 0(), s 0()),
              g s x -> h g x,
              g s x -> pair(+(p g x, q g x), p g x),
          +(x, 0()) -> x,
          +(x, s y) -> s +(x, y),
       q pair(x, y) -> y}
      POLY:
       Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
       Interpretation:
        [pair](x0, x1) = 0,
        
        [+](x0, x1) = x0 + x1 + 1,
        
        [f](x0) = x0 + 1,
        
        [s](x0) = x0 + 1,
        
        [p](x0) = x0,
        
        [h](x0) = x0 + 1,
        
        [g](x0) = 1,
        
        [q](x0) = x0 + 1,
        
        [0] = 1,
        
        [+#](x0, x1) = x0 + 1
       Strict:
        +#(x, s y) -> +#(x, y)
        2 + 0x + 1y >= 1 + 0x + 1y
       Weak:
        q pair(x, y) -> y
        1 + 0x + 0y >= 1y
        +(x, s y) -> s +(x, y)
        2 + 1x + 1y >= 2 + 1x + 1y
        +(x, 0()) -> x
        2 + 1x >= 1x
        g s x -> pair(+(p g x, q g x), p g x)
        1 + 0x >= 0 + 0x
        g s x -> h g x
        1 + 0x >= 2 + 0x
        g 0() -> pair(s 0(), s 0())
        1 >= 0
        h x -> pair(+(p x, q x), p x)
        1 + 1x >= 0 + 0x
        p pair(x, y) -> x
        0 + 0x + 0y >= 1x
        f s s x -> +(p g x, q g x)
        3 + 1x >= 4 + 0x
        f s s x -> p h g x
        3 + 1x >= 2 + 0x
        f s 0() -> s 0()
        3 >= 2
        f 0() -> 0()
        2 >= 1
      Qed