YES
We show the termination of the TRS R:

  rev(nil()) -> nil()
  rev(cons(x,l)) -> cons(rev1(x,l),rev2(x,l))
  rev1(|0|(),nil()) -> |0|()
  rev1(s(x),nil()) -> s(x)
  rev1(x,cons(y,l)) -> rev1(y,l)
  rev2(x,nil()) -> nil()
  rev2(x,cons(y,l)) -> rev(cons(x,rev2(y,l)))


-- SCC decomposition.

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

p1: rev#(cons(x,l)) -> rev1#(x,l)
p2: rev#(cons(x,l)) -> rev2#(x,l)
p3: rev1#(x,cons(y,l)) -> rev1#(y,l)
p4: rev2#(x,cons(y,l)) -> rev#(cons(x,rev2(y,l)))
p5: rev2#(x,cons(y,l)) -> rev2#(y,l)

and R consists of:

r1: rev(nil()) -> nil()
r2: rev(cons(x,l)) -> cons(rev1(x,l),rev2(x,l))
r3: rev1(|0|(),nil()) -> |0|()
r4: rev1(s(x),nil()) -> s(x)
r5: rev1(x,cons(y,l)) -> rev1(y,l)
r6: rev2(x,nil()) -> nil()
r7: rev2(x,cons(y,l)) -> rev(cons(x,rev2(y,l)))

The estimated dependency graph contains the following SCCs:

  {p2, p4, p5}
  {p3}


-- Reduction pair.

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

p1: rev2#(x,cons(y,l)) -> rev#(cons(x,rev2(y,l)))
p2: rev#(cons(x,l)) -> rev2#(x,l)
p3: rev2#(x,cons(y,l)) -> rev2#(y,l)

and R consists of:

r1: rev(nil()) -> nil()
r2: rev(cons(x,l)) -> cons(rev1(x,l),rev2(x,l))
r3: rev1(|0|(),nil()) -> |0|()
r4: rev1(s(x),nil()) -> s(x)
r5: rev1(x,cons(y,l)) -> rev1(y,l)
r6: rev2(x,nil()) -> nil()
r7: rev2(x,cons(y,l)) -> rev(cons(x,rev2(y,l)))

The set of usable rules consists of

  r1, r2, r6, r7

Take the reduction pair:

  generalized weighted path order (>=MG, >MG)
  
    base order 1:
  
      max/plus interpretation on natural numbers:
      
        rev2#_A(x1,x2) = max{7, x2 + 6}
        cons_A(x1,x2) = x2 + 16
        rev#_A(x1) = max{6, x1 - 6}
        rev2_A(x1,x2) = x2
        rev_A(x1) = max{3, x1}
        nil_A = 2
        rev1_A(x1,x2) = max{1, x2 - 8}
  
    base order 2:
  
      precedence:
      
        rev2 > cons = rev > rev2# = nil > rev# > rev1
      
  
    partial status:
  
      pi(rev2#) = []
      pi(cons) = []
      pi(rev#) = []
      pi(rev2) = [2]
      pi(rev) = []
      pi(nil) = []
      pi(rev1) = []

The following rules are removed:

  p1



-- SCC decomposition.

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

p1: rev#(cons(x,l)) -> rev2#(x,l)
p2: rev2#(x,cons(y,l)) -> rev2#(y,l)

and R consists of:

r1: rev(nil()) -> nil()
r2: rev(cons(x,l)) -> cons(rev1(x,l),rev2(x,l))
r3: rev1(|0|(),nil()) -> |0|()
r4: rev1(s(x),nil()) -> s(x)
r5: rev1(x,cons(y,l)) -> rev1(y,l)
r6: rev2(x,nil()) -> nil()
r7: rev2(x,cons(y,l)) -> rev(cons(x,rev2(y,l)))

The estimated dependency graph contains the following SCCs:

  {p2}


-- Reduction pair.

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

p1: rev2#(x,cons(y,l)) -> rev2#(y,l)

and R consists of:

r1: rev(nil()) -> nil()
r2: rev(cons(x,l)) -> cons(rev1(x,l),rev2(x,l))
r3: rev1(|0|(),nil()) -> |0|()
r4: rev1(s(x),nil()) -> s(x)
r5: rev1(x,cons(y,l)) -> rev1(y,l)
r6: rev2(x,nil()) -> nil()
r7: rev2(x,cons(y,l)) -> rev(cons(x,rev2(y,l)))

The set of usable rules consists of

  r1, r3

Take the reduction pair:

  generalized weighted path order (>=MG, >MG)
  
    base order 1:
  
      max/plus interpretation on natural numbers:
      
        rev2#_A(x1,x2) = max{3, x2 - 3}
        cons_A(x1,x2) = max{7, x1 - 4, x2 + 2}
        rev_A(x1) = max{9, x1 - 9}
        nil_A = 5
        rev1_A(x1,x2) = max{3, x1 - 14, x2 - 10}
        |0|_A = 0
  
    base order 2:
  
      precedence:
      
        rev > cons > rev2# = rev1 > nil > |0|
      
  
    partial status:
  
      pi(rev2#) = []
      pi(cons) = [2]
      pi(rev) = []
      pi(nil) = []
      pi(rev1) = []
      pi(|0|) = []

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: rev1#(x,cons(y,l)) -> rev1#(y,l)

and R consists of:

r1: rev(nil()) -> nil()
r2: rev(cons(x,l)) -> cons(rev1(x,l),rev2(x,l))
r3: rev1(|0|(),nil()) -> |0|()
r4: rev1(s(x),nil()) -> s(x)
r5: rev1(x,cons(y,l)) -> rev1(y,l)
r6: rev2(x,nil()) -> nil()
r7: rev2(x,cons(y,l)) -> rev(cons(x,rev2(y,l)))

The set of usable rules consists of

  r1, r3

Take the reduction pair:

  generalized weighted path order (>=MG, >MG)
  
    base order 1:
  
      max/plus interpretation on natural numbers:
      
        rev1#_A(x1,x2) = max{4, x2 - 4}
        cons_A(x1,x2) = max{9, x1 - 5, x2 + 3}
        rev_A(x1) = max{7, x1 - 12}
        nil_A = 6
        rev1_A(x1,x2) = max{4, x1 - 18, x2 - 13}
        |0|_A = 0
  
    base order 2:
  
      precedence:
      
        rev > cons > rev1# = nil = rev1 > |0|
      
  
    partial status:
  
      pi(rev1#) = []
      pi(cons) = [2]
      pi(rev) = []
      pi(nil) = []
      pi(rev1) = []
      pi(|0|) = []

The following rules are removed:

  p1

Then no dependency pair remains.