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:

  max/plus interpretations on natural numbers:
  
    rev#_A(x1) = max{2, x1 - 1}
    cons_A(x1,x2) = x2 + 4
    rev2#_A(x1,x2) = max{0, x2 - 1}
    rev2_A(x1,x2) = x2
    rev_A(x1) = max{3, x1}
    rev1_A(x1,x2) = max{x1, x2 - 1}
    nil_A = 3

The next rules are strictly ordered:

  p1, p2

We remove them from the problem.

-- SCC decomposition.

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

p1: 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 estimated dependency graph contains the following SCCs:

  (no SCCs)

-- 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:

  max/plus interpretations on natural numbers:
  
    last#_A(x1,x2) = max{x1 + 2, x2 + 2}
    if#_A(x1,x2,x3) = max{x1 + 1, x2 + 2, x3 + 2}
    empty_A(x1) = max{1, x1}
    false_A = 2
    head_A(x1) = max{0, x1 - 1}
    tail_A(x1) = max{0, x1 - 1}
    nil_A = 0
    true_A = 1
    cons_A(x1,x2) = max{x1 + 2, x2 + 2}

The next rules are strictly ordered:

  p2

We remove them from the problem.

-- SCC decomposition.

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

p1: last#(x,l) -> if#(empty(l),x,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:

  (no SCCs)