YES
We show the termination of the TRS R:

  empty(nil()) -> true()
  empty(cons(x,y)) -> false()
  tail(nil()) -> nil()
  tail(cons(x,y)) -> y
  head(cons(x,y)) -> x
  zero(|0|()) -> true()
  zero(s(x)) -> false()
  p(|0|()) -> |0|()
  p(s(|0|())) -> |0|()
  p(s(s(x))) -> s(p(s(x)))
  intlist(x) -> if_intlist(empty(x),x)
  if_intlist(true(),x) -> nil()
  if_intlist(false(),x) -> cons(s(head(x)),intlist(tail(x)))
  int(x,y) -> if_int(zero(x),zero(y),x,y)
  if_int(true(),b,x,y) -> if1(b,x,y)
  if_int(false(),b,x,y) -> if2(b,x,y)
  if1(true(),x,y) -> cons(|0|(),nil())
  if1(false(),x,y) -> cons(|0|(),int(s(|0|()),y))
  if2(true(),x,y) -> nil()
  if2(false(),x,y) -> intlist(int(p(x),p(y)))


-- SCC decomposition.

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

p1: p#(s(s(x))) -> p#(s(x))
p2: intlist#(x) -> if_intlist#(empty(x),x)
p3: intlist#(x) -> empty#(x)
p4: if_intlist#(false(),x) -> head#(x)
p5: if_intlist#(false(),x) -> intlist#(tail(x))
p6: if_intlist#(false(),x) -> tail#(x)
p7: int#(x,y) -> if_int#(zero(x),zero(y),x,y)
p8: int#(x,y) -> zero#(x)
p9: int#(x,y) -> zero#(y)
p10: if_int#(true(),b,x,y) -> if1#(b,x,y)
p11: if_int#(false(),b,x,y) -> if2#(b,x,y)
p12: if1#(false(),x,y) -> int#(s(|0|()),y)
p13: if2#(false(),x,y) -> intlist#(int(p(x),p(y)))
p14: if2#(false(),x,y) -> int#(p(x),p(y))
p15: if2#(false(),x,y) -> p#(x)
p16: if2#(false(),x,y) -> p#(y)

and R consists of:

r1: empty(nil()) -> true()
r2: empty(cons(x,y)) -> false()
r3: tail(nil()) -> nil()
r4: tail(cons(x,y)) -> y
r5: head(cons(x,y)) -> x
r6: zero(|0|()) -> true()
r7: zero(s(x)) -> false()
r8: p(|0|()) -> |0|()
r9: p(s(|0|())) -> |0|()
r10: p(s(s(x))) -> s(p(s(x)))
r11: intlist(x) -> if_intlist(empty(x),x)
r12: if_intlist(true(),x) -> nil()
r13: if_intlist(false(),x) -> cons(s(head(x)),intlist(tail(x)))
r14: int(x,y) -> if_int(zero(x),zero(y),x,y)
r15: if_int(true(),b,x,y) -> if1(b,x,y)
r16: if_int(false(),b,x,y) -> if2(b,x,y)
r17: if1(true(),x,y) -> cons(|0|(),nil())
r18: if1(false(),x,y) -> cons(|0|(),int(s(|0|()),y))
r19: if2(true(),x,y) -> nil()
r20: if2(false(),x,y) -> intlist(int(p(x),p(y)))

The estimated dependency graph contains the following SCCs:

  {p7, p10, p11, p12, p14}
  {p1}
  {p2, p5}


-- Reduction pair.

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

p1: if_int#(false(),b,x,y) -> if2#(b,x,y)
p2: if2#(false(),x,y) -> int#(p(x),p(y))
p3: int#(x,y) -> if_int#(zero(x),zero(y),x,y)
p4: if_int#(true(),b,x,y) -> if1#(b,x,y)
p5: if1#(false(),x,y) -> int#(s(|0|()),y)

and R consists of:

r1: empty(nil()) -> true()
r2: empty(cons(x,y)) -> false()
r3: tail(nil()) -> nil()
r4: tail(cons(x,y)) -> y
r5: head(cons(x,y)) -> x
r6: zero(|0|()) -> true()
r7: zero(s(x)) -> false()
r8: p(|0|()) -> |0|()
r9: p(s(|0|())) -> |0|()
r10: p(s(s(x))) -> s(p(s(x)))
r11: intlist(x) -> if_intlist(empty(x),x)
r12: if_intlist(true(),x) -> nil()
r13: if_intlist(false(),x) -> cons(s(head(x)),intlist(tail(x)))
r14: int(x,y) -> if_int(zero(x),zero(y),x,y)
r15: if_int(true(),b,x,y) -> if1(b,x,y)
r16: if_int(false(),b,x,y) -> if2(b,x,y)
r17: if1(true(),x,y) -> cons(|0|(),nil())
r18: if1(false(),x,y) -> cons(|0|(),int(s(|0|()),y))
r19: if2(true(),x,y) -> nil()
r20: if2(false(),x,y) -> intlist(int(p(x),p(y)))

The set of usable rules consists of

  r2, r6, r7, r8, r9, r10

Take the reduction pair:

  generalized weighted path order (>=MG, >G)
  
    base order 1:
  
      trivial reduction triple (T x T, T x T, Φ)
  
    base order 2:
  
      lexicographic combination of reduction triples:
      
        1. marked-algebra reduction triple (>=A, >=A!, >A!):
        
          max/plus interpretation on natural numbers:
          
            if_int#_A(x1,x2,x3,x4) = max{1, x3 - 43, x4 - 44}
            false_A = 60
            if2#_A(x1,x2,x3) = max{1, x2 - 45, x3 - 45}
            int#_A(x1,x2) = max{1, x1 - 43, x2 - 44}
            p_A(x1) = max{0, x1 - 43}
            zero_A(x1) = max{38, x1 + 17}
            true_A = 18
            if1#_A(x1,x2,x3) = max{1, x2 - 44, x3 - 44}
            s_A(x1) = x1 + 43
            |0|_A = 0
            empty_A(x1) = max{614, x1 - 140}
            cons_A(x1,x2) = max{139, x1 - 415, x2 - 140}
            if_int#!_A(x1,x2,x3,x4) = max{20, x1 - 18, x2 + 1, x3 + 15, x4 + 19}
            false!_A = 49
            if2#!_A(x1,x2,x3) = max{41, x1 + 1, x2, x3 + 16}
            int#!_A(x1,x2) = max{40, x1 + 15, x2 + 19}
            p!_A(x1) = 51
            zero!_A(x1) = 53
            true!_A = 12
            if1#!_A(x1,x2,x3) = max{x1 - 1, x3 + 19}
            s!_A(x1) = 50
            |0|!_A = 13
            empty!_A(x1) = max{50, x1 - 140}
            cons!_A(x1,x2) = max{12, x2 - 178}
        
        2. marked-algebra reduction triple (>=A, >=A!, >A!):
        
          max/plus interpretation on natural numbers:
          
            if_int#_A(x1,x2,x3,x4) = max{22, x1 - 2, x4 - 4}
            false_A = 25
            if2#_A(x1,x2,x3) = max{23, x3 - 4}
            int#_A(x1,x2) = max{23, x1 - 7, x2 - 4}
            p_A(x1) = 27
            zero_A(x1) = 25
            true_A = 25
            if1#_A(x1,x2,x3) = max{23, x3 - 4}
            s_A(x1) = max{6, x1}
            |0|_A = 4
            empty_A(x1) = max{61, x1 - 6}
            cons_A(x1,x2) = max{5, x1 - 9, x2 - 6}
            if_int#!_A(x1,x2,x3,x4) = max{21, x1 - 24, x3 - 6}
            false!_A = 17
            if2#!_A(x1,x2,x3) = 20
            int#!_A(x1,x2) = max{21, x1 - 6}
            p!_A(x1) = 19
            zero!_A(x1) = x1 + 10
            true!_A = 22
            if1#!_A(x1,x2,x3) = 21
            s!_A(x1) = 18
            |0|!_A = 24
            empty!_A(x1) = max{38, x1 - 6}
            cons!_A(x1,x2) = max{22, x1 - 7, x2 - 12}
        
  
    partial status:
  
      pi(if_int#) = []
      pi(false) = []
      pi(if2#) = []
      pi(int#) = []
      pi(p) = [1]
      pi(zero) = [1]
      pi(true) = []
      pi(if1#) = []
      pi(s) = []
      pi(|0|) = []
      pi(empty) = []
      pi(cons) = []

The following rules are removed:

  p1, p2



-- SCC decomposition.

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

p1: int#(x,y) -> if_int#(zero(x),zero(y),x,y)
p2: if_int#(true(),b,x,y) -> if1#(b,x,y)
p3: if1#(false(),x,y) -> int#(s(|0|()),y)

and R consists of:

r1: empty(nil()) -> true()
r2: empty(cons(x,y)) -> false()
r3: tail(nil()) -> nil()
r4: tail(cons(x,y)) -> y
r5: head(cons(x,y)) -> x
r6: zero(|0|()) -> true()
r7: zero(s(x)) -> false()
r8: p(|0|()) -> |0|()
r9: p(s(|0|())) -> |0|()
r10: p(s(s(x))) -> s(p(s(x)))
r11: intlist(x) -> if_intlist(empty(x),x)
r12: if_intlist(true(),x) -> nil()
r13: if_intlist(false(),x) -> cons(s(head(x)),intlist(tail(x)))
r14: int(x,y) -> if_int(zero(x),zero(y),x,y)
r15: if_int(true(),b,x,y) -> if1(b,x,y)
r16: if_int(false(),b,x,y) -> if2(b,x,y)
r17: if1(true(),x,y) -> cons(|0|(),nil())
r18: if1(false(),x,y) -> cons(|0|(),int(s(|0|()),y))
r19: if2(true(),x,y) -> nil()
r20: if2(false(),x,y) -> intlist(int(p(x),p(y)))

The estimated dependency graph contains the following SCCs:

  {p1, p2, p3}


-- Reduction pair.

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

p1: int#(x,y) -> if_int#(zero(x),zero(y),x,y)
p2: if_int#(true(),b,x,y) -> if1#(b,x,y)
p3: if1#(false(),x,y) -> int#(s(|0|()),y)

and R consists of:

r1: empty(nil()) -> true()
r2: empty(cons(x,y)) -> false()
r3: tail(nil()) -> nil()
r4: tail(cons(x,y)) -> y
r5: head(cons(x,y)) -> x
r6: zero(|0|()) -> true()
r7: zero(s(x)) -> false()
r8: p(|0|()) -> |0|()
r9: p(s(|0|())) -> |0|()
r10: p(s(s(x))) -> s(p(s(x)))
r11: intlist(x) -> if_intlist(empty(x),x)
r12: if_intlist(true(),x) -> nil()
r13: if_intlist(false(),x) -> cons(s(head(x)),intlist(tail(x)))
r14: int(x,y) -> if_int(zero(x),zero(y),x,y)
r15: if_int(true(),b,x,y) -> if1(b,x,y)
r16: if_int(false(),b,x,y) -> if2(b,x,y)
r17: if1(true(),x,y) -> cons(|0|(),nil())
r18: if1(false(),x,y) -> cons(|0|(),int(s(|0|()),y))
r19: if2(true(),x,y) -> nil()
r20: if2(false(),x,y) -> intlist(int(p(x),p(y)))

The set of usable rules consists of

  r3, r6, r7

Take the reduction pair:

  generalized weighted path order (>=MG, >G)
  
    base order 1:
  
      trivial reduction triple (T x T, T x T, Φ)
  
    base order 2:
  
      lexicographic combination of reduction triples:
      
        1. marked-algebra reduction triple (>=A, >=A!, >A!):
        
          max/plus interpretation on natural numbers:
          
            int#_A(x1,x2) = max{0, x1 - 11, x2 - 15}
            if_int#_A(x1,x2,x3,x4) = max{0, x1 - 47, x2 - 38, x3 - 11, x4 - 15}
            zero_A(x1) = max{37, x1 - 3}
            true_A = 46
            if1#_A(x1,x2,x3) = max{0, x1 - 38, x2 - 15, x3 - 15}
            false_A = 1
            s_A(x1) = max{2, x1 - 52}
            |0|_A = 49
            tail_A(x1) = max{84, x1 - 6}
            nil_A = 5
            int#!_A(x1,x2) = x1 + 2
            if_int#!_A(x1,x2,x3,x4) = max{x1 - 38, x3 + 1}
            zero!_A(x1) = max{9, x1 - 111}
            true!_A = 8
            if1#!_A(x1,x2,x3) = 7
            false!_A = 3
            s!_A(x1) = max{5, x1 - 43}
            |0|!_A = 6
            tail!_A(x1) = max{5, x1 - 6}
            nil!_A = 4
        
        2. marked-algebra reduction triple (>=A, >=A!, >A!):
        
          max/plus interpretation on natural numbers:
          
            int#_A(x1,x2) = max{0, x1 - 2, x2 - 28}
            if_int#_A(x1,x2,x3,x4) = max{0, x1 - 36, x2 - 36, x3 - 2, x4 - 28}
            zero_A(x1) = max{35, x1 - 2}
            true_A = 3
            if1#_A(x1,x2,x3) = max{0, x1 - 36, x2 - 28, x3 - 28}
            false_A = 1
            s_A(x1) = max{1, x1 - 26}
            |0|_A = 1
            tail_A(x1) = max{15, x1 - 6}
            nil_A = 5
            int#!_A(x1,x2) = max{x1 + 4, x2 + 42}
            if_int#!_A(x1,x2,x3,x4) = max{38, x1 + 1, x2 - 36, x3 + 1}
            zero!_A(x1) = max{41, x1 - 75}
            true!_A = 40
            if1#!_A(x1,x2,x3) = 5
            false!_A = 38
            s!_A(x1) = max{43, x1 - 50}
            |0|!_A = 41
            tail!_A(x1) = max{37, x1 - 23}
            nil!_A = 46
        
  
    partial status:
  
      pi(int#) = []
      pi(if_int#) = []
      pi(zero) = []
      pi(true) = []
      pi(if1#) = []
      pi(false) = []
      pi(s) = []
      pi(|0|) = []
      pi(tail) = []
      pi(nil) = []

The following rules are removed:

  p1, p2, p3

Then no dependency pair remains.

-- Reduction pair.

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

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

and R consists of:

r1: empty(nil()) -> true()
r2: empty(cons(x,y)) -> false()
r3: tail(nil()) -> nil()
r4: tail(cons(x,y)) -> y
r5: head(cons(x,y)) -> x
r6: zero(|0|()) -> true()
r7: zero(s(x)) -> false()
r8: p(|0|()) -> |0|()
r9: p(s(|0|())) -> |0|()
r10: p(s(s(x))) -> s(p(s(x)))
r11: intlist(x) -> if_intlist(empty(x),x)
r12: if_intlist(true(),x) -> nil()
r13: if_intlist(false(),x) -> cons(s(head(x)),intlist(tail(x)))
r14: int(x,y) -> if_int(zero(x),zero(y),x,y)
r15: if_int(true(),b,x,y) -> if1(b,x,y)
r16: if_int(false(),b,x,y) -> if2(b,x,y)
r17: if1(true(),x,y) -> cons(|0|(),nil())
r18: if1(false(),x,y) -> cons(|0|(),int(s(|0|()),y))
r19: if2(true(),x,y) -> nil()
r20: if2(false(),x,y) -> intlist(int(p(x),p(y)))

The set of usable rules consists of

  r3, r7

Take the reduction pair:

  generalized weighted path order (>=MG, >G)
  
    base order 1:
  
      trivial reduction triple (T x T, T x T, Φ)
  
    base order 2:
  
      lexicographic combination of reduction triples:
      
        1. marked-algebra reduction triple (>=A, >=A!, >A!):
        
          max/plus interpretation on natural numbers:
          
            p#_A(x1) = 0
            s_A(x1) = max{25, x1 - 11}
            tail_A(x1) = max{20, x1 - 6}
            nil_A = 5
            zero_A(x1) = max{11, x1 - 26}
            false_A = 1
            p#!_A(x1) = max{1, x1 - 80}
            s!_A(x1) = max{13, x1 - 43}
            tail!_A(x1) = max{13, x1 - 9}
            nil!_A = 0
            zero!_A(x1) = max{13, x1 - 26}
            false!_A = 12
        
        2. marked-algebra reduction triple (>=A, >=A!, >A!):
        
          max/plus interpretation on natural numbers:
          
            p#_A(x1) = 0
            s_A(x1) = max{58, x1 - 90}
            tail_A(x1) = max{129, x1 - 125}
            nil_A = 3
            zero_A(x1) = max{45, x1 - 61}
            false_A = 8
            p#!_A(x1) = max{1, x1 - 372}
            s!_A(x1) = max{4, x1 - 313}
            tail!_A(x1) = max{0, x1 - 255}
            nil!_A = 1
            zero!_A(x1) = max{7, x1 - 61}
            false!_A = 3
        
  
    partial status:
  
      pi(p#) = [1]
      pi(s) = [1]
      pi(tail) = []
      pi(nil) = []
      pi(zero) = []
      pi(false) = []

The following rules are removed:

  p1

Then no dependency pair remains.

-- Reduction pair.

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

p1: intlist#(x) -> if_intlist#(empty(x),x)
p2: if_intlist#(false(),x) -> intlist#(tail(x))

and R consists of:

r1: empty(nil()) -> true()
r2: empty(cons(x,y)) -> false()
r3: tail(nil()) -> nil()
r4: tail(cons(x,y)) -> y
r5: head(cons(x,y)) -> x
r6: zero(|0|()) -> true()
r7: zero(s(x)) -> false()
r8: p(|0|()) -> |0|()
r9: p(s(|0|())) -> |0|()
r10: p(s(s(x))) -> s(p(s(x)))
r11: intlist(x) -> if_intlist(empty(x),x)
r12: if_intlist(true(),x) -> nil()
r13: if_intlist(false(),x) -> cons(s(head(x)),intlist(tail(x)))
r14: int(x,y) -> if_int(zero(x),zero(y),x,y)
r15: if_int(true(),b,x,y) -> if1(b,x,y)
r16: if_int(false(),b,x,y) -> if2(b,x,y)
r17: if1(true(),x,y) -> cons(|0|(),nil())
r18: if1(false(),x,y) -> cons(|0|(),int(s(|0|()),y))
r19: if2(true(),x,y) -> nil()
r20: if2(false(),x,y) -> intlist(int(p(x),p(y)))

The set of usable rules consists of

  r1, r2, r3, r4, r7, r8

Take the reduction pair:

  generalized weighted path order (>=MG, >G)
  
    base order 1:
  
      trivial reduction triple (T x T, T x T, Φ)
  
    base order 2:
  
      lexicographic combination of reduction triples:
      
        1. marked-algebra reduction triple (>=A, >=A!, >A!):
        
          max/plus interpretation on natural numbers:
          
            intlist#_A(x1) = max{0, x1 - 4}
            if_intlist#_A(x1,x2) = max{0, x1 - 10, x2 - 4}
            empty_A(x1) = max{0, x1 - 40}
            false_A = 8
            tail_A(x1) = max{3, x1 - 55}
            nil_A = 3
            true_A = 0
            cons_A(x1,x2) = max{x1 - 5, x2 + 57}
            zero_A(x1) = max{167, x1 - 2}
            s_A(x1) = max{1, x1 - 81}
            p_A(x1) = 80
            |0|_A = 1
            intlist#!_A(x1) = max{6, x1 + 1}
            if_intlist#!_A(x1,x2) = max{5, x1 - 1, x2 - 4}
            empty!_A(x1) = max{7, x1 - 5}
            false!_A = 12
            tail!_A(x1) = max{5, x1 - 4}
            nil!_A = 11
            true!_A = 10
            cons!_A(x1,x2) = max{12, x1 - 2}
            zero!_A(x1) = max{13, x1 - 2}
            s!_A(x1) = max{10, x1 - 163}
            p!_A(x1) = 10
            |0|!_A = 2
        
        2. marked-algebra reduction triple (>=A, >=A!, >A!):
        
          max/plus interpretation on natural numbers:
          
            intlist#_A(x1) = max{0, x1 - 14}
            if_intlist#_A(x1,x2) = max{0, x1 - 5, x2 - 14}
            empty_A(x1) = max{2, x1 - 9}
            false_A = 2
            tail_A(x1) = max{13, x1 - 6}
            nil_A = 5
            true_A = 0
            cons_A(x1,x2) = max{x1 - 13, x2 + 8}
            zero_A(x1) = max{81, x1 - 13}
            s_A(x1) = max{12, x1 - 84}
            p_A(x1) = max{64, x1 + 51}
            |0|_A = 0
            intlist#!_A(x1) = max{10, x1 + 2}
            if_intlist#!_A(x1,x2) = max{x1 + 14, x2 + 3}
            empty!_A(x1) = max{11, x1 - 83}
            false!_A = 9
            tail!_A(x1) = max{4, x1 - 22}
            nil!_A = 5
            true!_A = 12
            cons!_A(x1,x2) = max{7, x1 - 2}
            zero!_A(x1) = max{13, x1 - 109}
            s!_A(x1) = 7
            p!_A(x1) = 9
            |0|!_A = 8
        
  
    partial status:
  
      pi(intlist#) = []
      pi(if_intlist#) = []
      pi(empty) = [1]
      pi(false) = []
      pi(tail) = [1]
      pi(nil) = []
      pi(true) = []
      pi(cons) = [1, 2]
      pi(zero) = []
      pi(s) = []
      pi(p) = []
      pi(|0|) = []

The following rules are removed:

  p1, p2

Then no dependency pair remains.