YES
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:
  Strict:
   {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)}
  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}
  EDG:
   {(g#(s(x)) -> +#(p(g(x)), q(g(x))), +#(x, s(y)) -> +#(x, y))
    (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)))
    (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))
    (+#(x, s(y)) -> +#(x, y), +#(x, s(y)) -> +#(x, y))
    (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))
    (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)))
    (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:
    Scc:
     {+#(x, s(y)) -> +#(x, y)}
    Scc:
     {g#(s(x)) -> g#(x)}
    SCC:
     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:
     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