YES
Time: 0.002034
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}
  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))}
   SCCS (2):
    Scc:
     {+#(x, s y) -> +#(x, y)}
    Scc:
     {g# s x -> g# x}
    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}
     SPSC:
      Simple Projection:
       pi(+#) = 1
      Strict:
       {}
      Qed
    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}
     SPSC:
      Simple Projection:
       pi(g#) = 0
      Strict:
       {}
      Qed