YES

We show the termination of the TRS R:

  empty(nil()) -> true()
  empty(cons(x,l)) -> false()
  head(cons(x,l)) -> x
  tail(nil()) -> nil()
  tail(cons(x,l)) -> l
  rev(nil()) -> nil()
  rev(cons(x,l)) -> cons(rev1(x,l),rev2(x,l))
  last(x,l) -> if(empty(l),x,l)
  if(true(),x,l) -> x
  if(false(),x,l) -> last(head(l),tail(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)) -> rev2#(x,l)
p2: last#(x,l) -> if#(empty(l),x,l)
p3: last#(x,l) -> empty#(l)
p4: if#(false(),x,l) -> last#(head(l),tail(l))
p5: if#(false(),x,l) -> head#(l)
p6: if#(false(),x,l) -> tail#(l)
p7: rev2#(x,cons(y,l)) -> rev#(cons(x,rev2(y,l)))
p8: rev2#(x,cons(y,l)) -> rev2#(y,l)

and R consists of:

r1: empty(nil()) -> true()
r2: empty(cons(x,l)) -> false()
r3: head(cons(x,l)) -> x
r4: tail(nil()) -> nil()
r5: tail(cons(x,l)) -> l
r6: rev(nil()) -> nil()
r7: rev(cons(x,l)) -> cons(rev1(x,l),rev2(x,l))
r8: last(x,l) -> if(empty(l),x,l)
r9: if(true(),x,l) -> x
r10: if(false(),x,l) -> last(head(l),tail(l))
r11: rev2(x,nil()) -> nil()
r12: rev2(x,cons(y,l)) -> rev(cons(x,rev2(y,l)))

The estimated dependency graph contains the following SCCs:

  {p1, p7, p8}
  {p2, p4}


-- Reduction pair.

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

and R consists of:

r1: empty(nil()) -> true()
r2: empty(cons(x,l)) -> false()
r3: head(cons(x,l)) -> x
r4: tail(nil()) -> nil()
r5: tail(cons(x,l)) -> l
r6: rev(nil()) -> nil()
r7: rev(cons(x,l)) -> cons(rev1(x,l),rev2(x,l))
r8: last(x,l) -> if(empty(l),x,l)
r9: if(true(),x,l) -> x
r10: if(false(),x,l) -> last(head(l),tail(l))
r11: rev2(x,nil()) -> nil()
r12: rev2(x,cons(y,l)) -> rev(cons(x,rev2(y,l)))

The set of usable rules consists of

  r7, r11, r12

Take the reduction pair:

  lexicographic combination of reduction pairs:
  
    1. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          rev#_A(x1) = max{4, x1}
          cons_A(x1,x2) = x2 + 4
          rev2#_A(x1,x2) = x2 + 4
          rev2_A(x1,x2) = x2
          rev_A(x1) = max{1, x1}
          rev1_A(x1,x2) = max{x1 - 1, x2}
          nil_A = 0
    
      precedence:
      
        rev1 > nil > rev2 = rev > cons > rev2# > rev#
      
      partial status:
    
        pi(rev#) = [1]
        pi(cons) = []
        pi(rev2#) = []
        pi(rev2) = [2]
        pi(rev) = []
        pi(rev1) = [2]
        pi(nil) = []
    
    2. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          rev#_A(x1) = 5
          cons_A(x1,x2) = 11
          rev2#_A(x1,x2) = 5
          rev2_A(x1,x2) = 22
          rev_A(x1) = 22
          rev1_A(x1,x2) = max{23, x2 - 1}
          nil_A = 23
    
      precedence:
      
        rev# = rev1 = nil > rev2 > rev > cons = rev2#
      
      partial status:
    
        pi(rev#) = []
        pi(cons) = []
        pi(rev2#) = []
        pi(rev2) = []
        pi(rev) = []
        pi(rev1) = []
        pi(nil) = []
    

The next rules are strictly ordered:

  p3

We remove them from the problem.

-- 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: empty(nil()) -> true()
r2: empty(cons(x,l)) -> false()
r3: head(cons(x,l)) -> x
r4: tail(nil()) -> nil()
r5: tail(cons(x,l)) -> l
r6: rev(nil()) -> nil()
r7: rev(cons(x,l)) -> cons(rev1(x,l),rev2(x,l))
r8: last(x,l) -> if(empty(l),x,l)
r9: if(true(),x,l) -> x
r10: if(false(),x,l) -> last(head(l),tail(l))
r11: rev2(x,nil()) -> nil()
r12: 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: empty(nil()) -> true()
r2: empty(cons(x,l)) -> false()
r3: head(cons(x,l)) -> x
r4: tail(nil()) -> nil()
r5: tail(cons(x,l)) -> l
r6: rev(nil()) -> nil()
r7: rev(cons(x,l)) -> cons(rev1(x,l),rev2(x,l))
r8: last(x,l) -> if(empty(l),x,l)
r9: if(true(),x,l) -> x
r10: if(false(),x,l) -> last(head(l),tail(l))
r11: rev2(x,nil()) -> nil()
r12: rev2(x,cons(y,l)) -> rev(cons(x,rev2(y,l)))

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  lexicographic combination of reduction pairs:
  
    1. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          rev2#_A(x1,x2) = max{x1 + 2, x2 + 2}
          cons_A(x1,x2) = max{x1 + 2, x2 + 2}
    
      precedence:
      
        cons > rev2#
      
      partial status:
    
        pi(rev2#) = [1, 2]
        pi(cons) = [2]
    
    2. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          rev2#_A(x1,x2) = max{3, x1 - 1, x2 + 2}
          cons_A(x1,x2) = x2 + 1
    
      precedence:
      
        rev2# = cons
      
      partial status:
    
        pi(rev2#) = []
        pi(cons) = [2]
    

The next rules are strictly ordered:

  p1

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: last#(x,l) -> if#(empty(l),x,l)
p2: if#(false(),x,l) -> last#(head(l),tail(l))

and R consists of:

r1: empty(nil()) -> true()
r2: empty(cons(x,l)) -> false()
r3: head(cons(x,l)) -> x
r4: tail(nil()) -> nil()
r5: tail(cons(x,l)) -> l
r6: rev(nil()) -> nil()
r7: rev(cons(x,l)) -> cons(rev1(x,l),rev2(x,l))
r8: last(x,l) -> if(empty(l),x,l)
r9: if(true(),x,l) -> x
r10: if(false(),x,l) -> last(head(l),tail(l))
r11: rev2(x,nil()) -> nil()
r12: rev2(x,cons(y,l)) -> rev(cons(x,rev2(y,l)))

The set of usable rules consists of

  r1, r2, r3, r4, r5

Take the reduction pair:

  lexicographic combination of reduction pairs:
  
    1. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          last#_A(x1,x2) = max{x1 + 6, x2 + 9}
          if#_A(x1,x2,x3) = max{9, x1 + 2, x2 + 6, x3 + 8}
          empty_A(x1) = max{3, x1 + 2}
          false_A = 12
          head_A(x1) = max{7, x1 + 1}
          tail_A(x1) = max{4, x1 - 2}
          nil_A = 3
          true_A = 4
          cons_A(x1,x2) = max{x1 + 13, x2 + 13}
    
      precedence:
      
        last# = empty = false > if# = head = tail > nil = true = cons
      
      partial status:
    
        pi(last#) = [1, 2]
        pi(if#) = [1, 3]
        pi(empty) = [1]
        pi(false) = []
        pi(head) = []
        pi(tail) = []
        pi(nil) = []
        pi(true) = []
        pi(cons) = [1, 2]
    
    2. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          last#_A(x1,x2) = max{12, x1 - 1, x2 + 9}
          if#_A(x1,x2,x3) = max{x1 + 6, x3 + 2}
          empty_A(x1) = x1 + 2
          false_A = 6
          head_A(x1) = 13
          tail_A(x1) = 3
          nil_A = 4
          true_A = 5
          cons_A(x1,x2) = max{x1 + 7, x2 + 7}
    
      precedence:
      
        last# = if# = empty = false = head = tail = nil = true = cons
      
      partial status:
    
        pi(last#) = []
        pi(if#) = [3]
        pi(empty) = []
        pi(false) = []
        pi(head) = []
        pi(tail) = []
        pi(nil) = []
        pi(true) = []
        pi(cons) = [2]
    

The next rules are strictly ordered:

  p1, p2

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