YES

We show the termination of the TRS R:

  f(|0|()) -> |0|()
  f(s(|0|())) -> s(|0|())
  f(s(s(x))) -> p(h(g(x)))
  g(|0|()) -> pair(s(|0|()),s(|0|()))
  g(s(x)) -> h(g(x))
  h(x) -> pair(+(p(x),q(x)),p(x))
  p(pair(x,y)) -> x
  q(pair(x,y)) -> y
  +(x,|0|()) -> x
  +(x,s(y)) -> s(+(x,y))
  f(s(s(x))) -> +(p(g(x)),q(g(x)))
  g(s(x)) -> pair(+(p(g(x)),q(g(x))),p(g(x)))

-- SCC decomposition.

Consider the dependency pair problem (P, R), where P consists of

p1: f#(s(s(x))) -> p#(h(g(x)))
p2: f#(s(s(x))) -> h#(g(x))
p3: f#(s(s(x))) -> g#(x)
p4: g#(s(x)) -> h#(g(x))
p5: g#(s(x)) -> g#(x)
p6: h#(x) -> +#(p(x),q(x))
p7: h#(x) -> p#(x)
p8: h#(x) -> q#(x)
p9: +#(x,s(y)) -> +#(x,y)
p10: f#(s(s(x))) -> +#(p(g(x)),q(g(x)))
p11: f#(s(s(x))) -> p#(g(x))
p12: f#(s(s(x))) -> g#(x)
p13: f#(s(s(x))) -> q#(g(x))
p14: g#(s(x)) -> +#(p(g(x)),q(g(x)))
p15: g#(s(x)) -> p#(g(x))
p16: g#(s(x)) -> g#(x)
p17: g#(s(x)) -> q#(g(x))

and R consists of:

r1: f(|0|()) -> |0|()
r2: f(s(|0|())) -> s(|0|())
r3: f(s(s(x))) -> p(h(g(x)))
r4: g(|0|()) -> pair(s(|0|()),s(|0|()))
r5: g(s(x)) -> h(g(x))
r6: h(x) -> pair(+(p(x),q(x)),p(x))
r7: p(pair(x,y)) -> x
r8: q(pair(x,y)) -> y
r9: +(x,|0|()) -> x
r10: +(x,s(y)) -> s(+(x,y))
r11: f(s(s(x))) -> +(p(g(x)),q(g(x)))
r12: g(s(x)) -> pair(+(p(g(x)),q(g(x))),p(g(x)))

The estimated dependency graph contains the following SCCs:

  {p5, p16}
  {p9}


-- Reduction pair.

Consider the dependency pair problem (P, R), where P consists of

p1: g#(s(x)) -> g#(x)

and R consists of:

r1: f(|0|()) -> |0|()
r2: f(s(|0|())) -> s(|0|())
r3: f(s(s(x))) -> p(h(g(x)))
r4: g(|0|()) -> pair(s(|0|()),s(|0|()))
r5: g(s(x)) -> h(g(x))
r6: h(x) -> pair(+(p(x),q(x)),p(x))
r7: p(pair(x,y)) -> x
r8: q(pair(x,y)) -> y
r9: +(x,|0|()) -> x
r10: +(x,s(y)) -> s(+(x,y))
r11: f(s(s(x))) -> +(p(g(x)),q(g(x)))
r12: g(s(x)) -> pair(+(p(g(x)),q(g(x))),p(g(x)))

The set of usable rules consists of

  (no rules)

Take the monotone reduction pair:

  lexicographic combination of reduction pairs:
  
    1. lexicographic path order with precedence:
    
      precedence:
      
        g# > s
      
      argument filter:
    
        pi(g#) = 1
        pi(s) = [1]
    
    2. matrix interpretations:
    
      carrier: N^1
      order: standard order
      interpretations:
        g#_A(x1) = x1
        s_A(x1) = x1 + 1
    

The next rules are strictly ordered:

  p1
  r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r12

We remove them from the problem.  Then no dependency pair remains.

-- Reduction pair.

Consider the dependency pair problem (P, R), where P consists of

p1: +#(x,s(y)) -> +#(x,y)

and R consists of:

r1: f(|0|()) -> |0|()
r2: f(s(|0|())) -> s(|0|())
r3: f(s(s(x))) -> p(h(g(x)))
r4: g(|0|()) -> pair(s(|0|()),s(|0|()))
r5: g(s(x)) -> h(g(x))
r6: h(x) -> pair(+(p(x),q(x)),p(x))
r7: p(pair(x,y)) -> x
r8: q(pair(x,y)) -> y
r9: +(x,|0|()) -> x
r10: +(x,s(y)) -> s(+(x,y))
r11: f(s(s(x))) -> +(p(g(x)),q(g(x)))
r12: g(s(x)) -> pair(+(p(g(x)),q(g(x))),p(g(x)))

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  lexicographic combination of reduction pairs:
  
    1. lexicographic path order with precedence:
    
      precedence:
      
        s > +#
      
      argument filter:
    
        pi(+#) = 2
        pi(s) = [1]
    
    2. matrix interpretations:
    
      carrier: N^1
      order: standard order
      interpretations:
        +#_A(x1,x2) = x2
        s_A(x1) = x1 + 1
    

The next rules are strictly ordered:

  p1

We remove them from the problem.  Then no dependency pair remains.