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 r6, r7, r11, r12 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: rev#_A(x1) = max{6, x1 - 1} cons_A(x1,x2) = max{7, x1 + 2, x2} rev2#_A(x1,x2) = max{4, x1 + 1, x2 - 1} rev2_A(x1,x2) = max{6, x1 + 2, x2} rev_A(x1) = max{5, x1} nil_A = 9 rev1_A(x1,x2) = 0 rev#!_A(x1) = max{1, x1 - 2} cons!_A(x1,x2) = x1 + 3 rev2#!_A(x1,x2) = max{2, x1, x2 - 2} rev2!_A(x1,x2) = max{3, x2 - 8} rev!_A(x1) = 3 nil!_A = 2 rev1!_A(x1,x2) = 2 2. marked-algebra reduction triple (>=A, >=A!, >A!): max/plus interpretation on natural numbers: rev#_A(x1) = 1 cons_A(x1,x2) = max{64, x2 + 44} rev2#_A(x1,x2) = 1 rev2_A(x1,x2) = max{13, x2} rev_A(x1) = max{56, x1} nil_A = 13 rev1_A(x1,x2) = max{1, x2 - 2} rev#!_A(x1) = max{19, x1 - 23} cons!_A(x1,x2) = max{18, x1 + 2, x2 + 3} rev2#!_A(x1,x2) = max{20, x2 - 2} rev2!_A(x1,x2) = max{61, x2 + 17} rev!_A(x1) = max{17, x1 - 28} nil!_A = 62 rev1!_A(x1,x2) = max{37, x1 - 1, x2 + 17} partial status: pi(rev#) = [] pi(cons) = [] pi(rev2#) = [] pi(rev2) = [] pi(rev) = [] pi(nil) = [] pi(rev1) = [] 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: 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, r4, r5 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: last#_A(x1,x2) = max{1, x2 - 16} if#_A(x1,x2,x3) = max{1, x1 - 86, x3 - 16} empty_A(x1) = max{71, x1 + 59} false_A = 84 head_A(x1) = max{3, x1 - 1} tail_A(x1) = max{15, x1 - 12} nil_A = 11 true_A = 71 cons_A(x1,x2) = max{x1 - 58, x2 + 25} last#!_A(x1,x2) = max{7, x2 - 16} if#!_A(x1,x2,x3) = max{5, x1 - 76, x3 - 16} empty!_A(x1) = 7 false!_A = 53 head!_A(x1) = max{1, x1 - 7} tail!_A(x1) = max{4, x1 - 12} nil!_A = 3 true!_A = 6 cons!_A(x1,x2) = x2 + 53 2. marked-algebra reduction triple (>=A, >=A!, >A!): max/plus interpretation on natural numbers: last#_A(x1,x2) = 1 if#_A(x1,x2,x3) = max{1, x1 - 21} empty_A(x1) = 20 false_A = 20 head_A(x1) = max{2, x1 - 1} tail_A(x1) = x1 + 16 nil_A = 6 true_A = 1 cons_A(x1,x2) = max{4, x1 - 16, x2 - 16} last#!_A(x1,x2) = 5 if#!_A(x1,x2,x3) = max{5, x1 - 16} empty!_A(x1) = 2 false!_A = 8 head!_A(x1) = max{7, x1 - 8} tail!_A(x1) = max{6, x1 - 7} nil!_A = 2 true!_A = 1 cons!_A(x1,x2) = max{25, x1 + 1, x2 - 37} partial status: pi(last#) = [] pi(if#) = [] pi(empty) = [1] pi(false) = [] pi(head) = [] pi(tail) = [1] pi(nil) = [] pi(true) = [] pi(cons) = [2] The following rules are removed: p2 -- 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)