YES We show the termination of the TRS R: ap(ap(map(),f),xs) -> ap(ap(ap(if(),ap(isEmpty(),xs)),f),xs) ap(ap(ap(if(),true()),f),xs) -> nil() ap(ap(ap(if(),false()),f),xs) -> ap(ap(cons(),ap(f,ap(last(),xs))),ap(ap(map(),f),ap(dropLast(),xs))) ap(isEmpty(),nil()) -> true() ap(isEmpty(),ap(ap(cons(),x),xs)) -> false() ap(last(),ap(ap(cons(),x),nil())) -> x ap(last(),ap(ap(cons(),x),ap(ap(cons(),y),ys))) -> ap(last(),ap(ap(cons(),y),ys)) ap(dropLast(),nil()) -> nil() ap(dropLast(),ap(ap(cons(),x),nil())) -> nil() ap(dropLast(),ap(ap(cons(),x),ap(ap(cons(),y),ys))) -> ap(ap(cons(),x),ap(dropLast(),ap(ap(cons(),y),ys))) Instead we prove termination of the uncurried system: ap(cons_0(),y) -> cons_1(y) ap(cons_1(x1),y) -> cons_2(x1,y) ap(dropLast_0(),y) -> dropLast_1(y) ap(if_0(),y) -> if_1(y) ap(if_1(x1),y) -> if_2(x1,y) ap(if_2(x1,x2),y) -> if_3(x1,x2,y) ap(isEmpty_0(),y) -> isEmpty_1(y) ap(last_0(),y) -> last_1(y) ap(map_0(),y) -> map_1(y) ap(map_1(x1),y) -> map_2(x1,y) map_2(f,xs) -> if_3(isEmpty_1(xs),f,xs) if_3(true_0(),f,xs) -> nil_0() if_3(false_0(),f,xs) -> cons_2(ap(f,last_1(xs)),map_2(f,dropLast_1(xs))) isEmpty_1(nil_0()) -> true_0() isEmpty_1(cons_2(x,xs)) -> false_0() last_1(cons_2(x,nil_0())) -> x last_1(cons_2(x,cons_2(y,ys))) -> last_1(cons_2(y,ys)) dropLast_1(nil_0()) -> nil_0() dropLast_1(cons_2(x,nil_0())) -> nil_0() dropLast_1(cons_2(x,cons_2(y,ys))) -> cons_2(x,dropLast_1(cons_2(y,ys))) -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: ap#(dropLast_0(),y) -> dropLast_1#(y) p2: ap#(if_2(x1,x2),y) -> if_3#(x1,x2,y) p3: ap#(isEmpty_0(),y) -> isEmpty_1#(y) p4: ap#(last_0(),y) -> last_1#(y) p5: ap#(map_1(x1),y) -> map_2#(x1,y) p6: map_2#(f,xs) -> if_3#(isEmpty_1(xs),f,xs) p7: map_2#(f,xs) -> isEmpty_1#(xs) p8: if_3#(false_0(),f,xs) -> ap#(f,last_1(xs)) p9: if_3#(false_0(),f,xs) -> last_1#(xs) p10: if_3#(false_0(),f,xs) -> map_2#(f,dropLast_1(xs)) p11: if_3#(false_0(),f,xs) -> dropLast_1#(xs) p12: last_1#(cons_2(x,cons_2(y,ys))) -> last_1#(cons_2(y,ys)) p13: dropLast_1#(cons_2(x,cons_2(y,ys))) -> dropLast_1#(cons_2(y,ys)) and R consists of: r1: ap(cons_0(),y) -> cons_1(y) r2: ap(cons_1(x1),y) -> cons_2(x1,y) r3: ap(dropLast_0(),y) -> dropLast_1(y) r4: ap(if_0(),y) -> if_1(y) r5: ap(if_1(x1),y) -> if_2(x1,y) r6: ap(if_2(x1,x2),y) -> if_3(x1,x2,y) r7: ap(isEmpty_0(),y) -> isEmpty_1(y) r8: ap(last_0(),y) -> last_1(y) r9: ap(map_0(),y) -> map_1(y) r10: ap(map_1(x1),y) -> map_2(x1,y) r11: map_2(f,xs) -> if_3(isEmpty_1(xs),f,xs) r12: if_3(true_0(),f,xs) -> nil_0() r13: if_3(false_0(),f,xs) -> cons_2(ap(f,last_1(xs)),map_2(f,dropLast_1(xs))) r14: isEmpty_1(nil_0()) -> true_0() r15: isEmpty_1(cons_2(x,xs)) -> false_0() r16: last_1(cons_2(x,nil_0())) -> x r17: last_1(cons_2(x,cons_2(y,ys))) -> last_1(cons_2(y,ys)) r18: dropLast_1(nil_0()) -> nil_0() r19: dropLast_1(cons_2(x,nil_0())) -> nil_0() r20: dropLast_1(cons_2(x,cons_2(y,ys))) -> cons_2(x,dropLast_1(cons_2(y,ys))) The estimated dependency graph contains the following SCCs: {p2, p5, p6, p8, p10} {p13} {p12} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: if_3#(false_0(),f,xs) -> ap#(f,last_1(xs)) p2: ap#(map_1(x1),y) -> map_2#(x1,y) p3: map_2#(f,xs) -> if_3#(isEmpty_1(xs),f,xs) p4: if_3#(false_0(),f,xs) -> map_2#(f,dropLast_1(xs)) p5: ap#(if_2(x1,x2),y) -> if_3#(x1,x2,y) and R consists of: r1: ap(cons_0(),y) -> cons_1(y) r2: ap(cons_1(x1),y) -> cons_2(x1,y) r3: ap(dropLast_0(),y) -> dropLast_1(y) r4: ap(if_0(),y) -> if_1(y) r5: ap(if_1(x1),y) -> if_2(x1,y) r6: ap(if_2(x1,x2),y) -> if_3(x1,x2,y) r7: ap(isEmpty_0(),y) -> isEmpty_1(y) r8: ap(last_0(),y) -> last_1(y) r9: ap(map_0(),y) -> map_1(y) r10: ap(map_1(x1),y) -> map_2(x1,y) r11: map_2(f,xs) -> if_3(isEmpty_1(xs),f,xs) r12: if_3(true_0(),f,xs) -> nil_0() r13: if_3(false_0(),f,xs) -> cons_2(ap(f,last_1(xs)),map_2(f,dropLast_1(xs))) r14: isEmpty_1(nil_0()) -> true_0() r15: isEmpty_1(cons_2(x,xs)) -> false_0() r16: last_1(cons_2(x,nil_0())) -> x r17: last_1(cons_2(x,cons_2(y,ys))) -> last_1(cons_2(y,ys)) r18: dropLast_1(nil_0()) -> nil_0() r19: dropLast_1(cons_2(x,nil_0())) -> nil_0() r20: dropLast_1(cons_2(x,cons_2(y,ys))) -> cons_2(x,dropLast_1(cons_2(y,ys))) The set of usable rules consists of r14, r15, r16, r17, r18, r19, r20 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_3#_A(x1,x2,x3) = max{0, x1 - 38, x2 - 19, x3 - 4} false_0_A = 36 ap#_A(x1,x2) = max{0, x1 - 19, x2 - 2} last_1_A(x1) = max{1, x1 - 22} map_1_A(x1) = x1 + 15 map_2#_A(x1,x2) = max{0, x1 - 19, x2 - 4} isEmpty_1_A(x1) = max{36, x1 - 31} dropLast_1_A(x1) = max{3, x1} if_2_A(x1,x2) = max{x1 - 10, x2 + 18} nil_0_A = 4 true_0_A = 23 cons_2_A(x1,x2) = max{x1 + 22, x2 + 30} if_3#!_A(x1,x2,x3) = max{12, x1 - 37, x2 + 10, x3 + 9} false_0!_A = 1 ap#!_A(x1,x2) = max{11, x1 + 9, x2 + 10} last_1!_A(x1) = max{19, x1 - 66} map_1!_A(x1) = max{7, x1 - 1} map_2#!_A(x1,x2) = max{12, x1 + 10, x2 + 9} isEmpty_1!_A(x1) = 8 dropLast_1!_A(x1) = max{13, x1 - 29} if_2!_A(x1,x2) = max{17, x1 - 37} nil_0!_A = 6 true_0!_A = 7 cons_2!_A(x1,x2) = max{16, x1 - 45, x2 - 5} 2. marked-algebra reduction triple (>=A, >=A!, >A!): matrix interpretation with standard point-wise order: carrier: N^1 order: standard order interpretations: if_3#_A(x1,x2,x3) = x2 + x3 + 3 false_0_A() = 1 ap#_A(x1,x2) = x1 + x2 last_1_A(x1) = x1 + 3 map_1_A(x1) = x1 + 3 map_2#_A(x1,x2) = x1 + x2 + 3 isEmpty_1_A(x1) = 3 dropLast_1_A(x1) = x1 if_2_A(x1,x2) = x1 + x2 + 5 nil_0_A() = 8 true_0_A() = 1 cons_2_A(x1,x2) = x1 + x2 + 5 if_3#!_A(x1,x2,x3) = 13 false_0!_A() = 2 ap#!_A(x1,x2) = x1 + 11 last_1!_A(x1) = 1 map_1!_A(x1) = 10 map_2#!_A(x1,x2) = 13 isEmpty_1!_A(x1) = 12 dropLast_1!_A(x1) = 9 if_2!_A(x1,x2) = 9 nil_0!_A() = 1 true_0!_A() = 0 cons_2!_A(x1,x2) = x1 + x2 + 3 partial status: pi(if_3#) = [] pi(false_0) = [] pi(ap#) = [] pi(last_1) = [1] pi(map_1) = [] pi(map_2#) = [] pi(isEmpty_1) = [1] pi(dropLast_1) = [1] pi(if_2) = [1, 2] pi(nil_0) = [] pi(true_0) = [] pi(cons_2) = [1, 2] The following rules are removed: p1, p2, p5 -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: map_2#(f,xs) -> if_3#(isEmpty_1(xs),f,xs) p2: if_3#(false_0(),f,xs) -> map_2#(f,dropLast_1(xs)) and R consists of: r1: ap(cons_0(),y) -> cons_1(y) r2: ap(cons_1(x1),y) -> cons_2(x1,y) r3: ap(dropLast_0(),y) -> dropLast_1(y) r4: ap(if_0(),y) -> if_1(y) r5: ap(if_1(x1),y) -> if_2(x1,y) r6: ap(if_2(x1,x2),y) -> if_3(x1,x2,y) r7: ap(isEmpty_0(),y) -> isEmpty_1(y) r8: ap(last_0(),y) -> last_1(y) r9: ap(map_0(),y) -> map_1(y) r10: ap(map_1(x1),y) -> map_2(x1,y) r11: map_2(f,xs) -> if_3(isEmpty_1(xs),f,xs) r12: if_3(true_0(),f,xs) -> nil_0() r13: if_3(false_0(),f,xs) -> cons_2(ap(f,last_1(xs)),map_2(f,dropLast_1(xs))) r14: isEmpty_1(nil_0()) -> true_0() r15: isEmpty_1(cons_2(x,xs)) -> false_0() r16: last_1(cons_2(x,nil_0())) -> x r17: last_1(cons_2(x,cons_2(y,ys))) -> last_1(cons_2(y,ys)) r18: dropLast_1(nil_0()) -> nil_0() r19: dropLast_1(cons_2(x,nil_0())) -> nil_0() r20: dropLast_1(cons_2(x,cons_2(y,ys))) -> cons_2(x,dropLast_1(cons_2(y,ys))) The estimated dependency graph contains the following SCCs: {p1, p2} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: map_2#(f,xs) -> if_3#(isEmpty_1(xs),f,xs) p2: if_3#(false_0(),f,xs) -> map_2#(f,dropLast_1(xs)) and R consists of: r1: ap(cons_0(),y) -> cons_1(y) r2: ap(cons_1(x1),y) -> cons_2(x1,y) r3: ap(dropLast_0(),y) -> dropLast_1(y) r4: ap(if_0(),y) -> if_1(y) r5: ap(if_1(x1),y) -> if_2(x1,y) r6: ap(if_2(x1,x2),y) -> if_3(x1,x2,y) r7: ap(isEmpty_0(),y) -> isEmpty_1(y) r8: ap(last_0(),y) -> last_1(y) r9: ap(map_0(),y) -> map_1(y) r10: ap(map_1(x1),y) -> map_2(x1,y) r11: map_2(f,xs) -> if_3(isEmpty_1(xs),f,xs) r12: if_3(true_0(),f,xs) -> nil_0() r13: if_3(false_0(),f,xs) -> cons_2(ap(f,last_1(xs)),map_2(f,dropLast_1(xs))) r14: isEmpty_1(nil_0()) -> true_0() r15: isEmpty_1(cons_2(x,xs)) -> false_0() r16: last_1(cons_2(x,nil_0())) -> x r17: last_1(cons_2(x,cons_2(y,ys))) -> last_1(cons_2(y,ys)) r18: dropLast_1(nil_0()) -> nil_0() r19: dropLast_1(cons_2(x,nil_0())) -> nil_0() r20: dropLast_1(cons_2(x,cons_2(y,ys))) -> cons_2(x,dropLast_1(cons_2(y,ys))) The set of usable rules consists of r12, r14, r15, r18, r19, r20 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: map_2#_A(x1,x2) = max{1, x1 - 1} if_3#_A(x1,x2,x3) = max{1, x2 - 1} isEmpty_1_A(x1) = max{7, x1 + 1} false_0_A = 15 dropLast_1_A(x1) = max{0, x1 - 19} if_3_A(x1,x2,x3) = max{2, x1 - 16, x2 - 21, x3 - 1} true_0_A = 2 nil_0_A = 0 cons_2_A(x1,x2) = x2 + 19 map_2#!_A(x1,x2) = x2 + 6 if_3#!_A(x1,x2,x3) = max{3, x1 - 8, x3} isEmpty_1!_A(x1) = max{7, x1 + 1} false_0!_A = 5 dropLast_1!_A(x1) = 8 if_3!_A(x1,x2,x3) = max{9, x1 - 3, x2 - 79} true_0!_A = 2 nil_0!_A = 1 cons_2!_A(x1,x2) = 8 2. marked-algebra reduction triple (>=A, >=A!, >A!): matrix interpretation with standard point-wise order: carrier: N^1 order: standard order interpretations: map_2#_A(x1,x2) = 0 if_3#_A(x1,x2,x3) = 0 isEmpty_1_A(x1) = x1 + 3 false_0_A() = 1 dropLast_1_A(x1) = x1 if_3_A(x1,x2,x3) = 7 true_0_A() = 4 nil_0_A() = 1 cons_2_A(x1,x2) = x1 + x2 + 7 map_2#!_A(x1,x2) = 2 if_3#!_A(x1,x2,x3) = x3 + 3 isEmpty_1!_A(x1) = x1 + 1 false_0!_A() = 4 dropLast_1!_A(x1) = 5 if_3!_A(x1,x2,x3) = x2 + x3 + 7 true_0!_A() = 1 nil_0!_A() = 0 cons_2!_A(x1,x2) = x1 + 6 partial status: pi(map_2#) = [] pi(if_3#) = [] pi(isEmpty_1) = [1] pi(false_0) = [] pi(dropLast_1) = [1] pi(if_3) = [1, 2, 3] pi(true_0) = [] pi(nil_0) = [] pi(cons_2) = [1] The following rules are removed: p1, p2 Then no dependency pair remains. -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: dropLast_1#(cons_2(x,cons_2(y,ys))) -> dropLast_1#(cons_2(y,ys)) and R consists of: r1: ap(cons_0(),y) -> cons_1(y) r2: ap(cons_1(x1),y) -> cons_2(x1,y) r3: ap(dropLast_0(),y) -> dropLast_1(y) r4: ap(if_0(),y) -> if_1(y) r5: ap(if_1(x1),y) -> if_2(x1,y) r6: ap(if_2(x1,x2),y) -> if_3(x1,x2,y) r7: ap(isEmpty_0(),y) -> isEmpty_1(y) r8: ap(last_0(),y) -> last_1(y) r9: ap(map_0(),y) -> map_1(y) r10: ap(map_1(x1),y) -> map_2(x1,y) r11: map_2(f,xs) -> if_3(isEmpty_1(xs),f,xs) r12: if_3(true_0(),f,xs) -> nil_0() r13: if_3(false_0(),f,xs) -> cons_2(ap(f,last_1(xs)),map_2(f,dropLast_1(xs))) r14: isEmpty_1(nil_0()) -> true_0() r15: isEmpty_1(cons_2(x,xs)) -> false_0() r16: last_1(cons_2(x,nil_0())) -> x r17: last_1(cons_2(x,cons_2(y,ys))) -> last_1(cons_2(y,ys)) r18: dropLast_1(nil_0()) -> nil_0() r19: dropLast_1(cons_2(x,nil_0())) -> nil_0() r20: dropLast_1(cons_2(x,cons_2(y,ys))) -> cons_2(x,dropLast_1(cons_2(y,ys))) The set of usable rules consists of r18 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: dropLast_1#_A(x1) = 0 cons_2_A(x1,x2) = max{79, x1 - 9, x2 - 39} dropLast_1_A(x1) = max{38, x1 - 90} nil_0_A = 0 dropLast_1#!_A(x1) = x1 + 87 cons_2!_A(x1,x2) = x2 + 88 dropLast_1!_A(x1) = x1 + 9 nil_0!_A = 8 2. marked-algebra reduction triple (>=A, >=A!, >A!): matrix interpretation with standard point-wise order: carrier: N^1 order: standard order interpretations: dropLast_1#_A(x1) = x1 cons_2_A(x1,x2) = x1 + x2 + 5 dropLast_1_A(x1) = x1 + 3 nil_0_A() = 8 dropLast_1#!_A(x1) = 12 cons_2!_A(x1,x2) = 13 dropLast_1!_A(x1) = x1 + 1 nil_0!_A() = 10 partial status: pi(dropLast_1#) = [1] pi(cons_2) = [2] pi(dropLast_1) = [1] pi(nil_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: last_1#(cons_2(x,cons_2(y,ys))) -> last_1#(cons_2(y,ys)) and R consists of: r1: ap(cons_0(),y) -> cons_1(y) r2: ap(cons_1(x1),y) -> cons_2(x1,y) r3: ap(dropLast_0(),y) -> dropLast_1(y) r4: ap(if_0(),y) -> if_1(y) r5: ap(if_1(x1),y) -> if_2(x1,y) r6: ap(if_2(x1,x2),y) -> if_3(x1,x2,y) r7: ap(isEmpty_0(),y) -> isEmpty_1(y) r8: ap(last_0(),y) -> last_1(y) r9: ap(map_0(),y) -> map_1(y) r10: ap(map_1(x1),y) -> map_2(x1,y) r11: map_2(f,xs) -> if_3(isEmpty_1(xs),f,xs) r12: if_3(true_0(),f,xs) -> nil_0() r13: if_3(false_0(),f,xs) -> cons_2(ap(f,last_1(xs)),map_2(f,dropLast_1(xs))) r14: isEmpty_1(nil_0()) -> true_0() r15: isEmpty_1(cons_2(x,xs)) -> false_0() r16: last_1(cons_2(x,nil_0())) -> x r17: last_1(cons_2(x,cons_2(y,ys))) -> last_1(cons_2(y,ys)) r18: dropLast_1(nil_0()) -> nil_0() r19: dropLast_1(cons_2(x,nil_0())) -> nil_0() r20: dropLast_1(cons_2(x,cons_2(y,ys))) -> cons_2(x,dropLast_1(cons_2(y,ys))) The set of usable rules consists of r18 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_1#_A(x1) = 0 cons_2_A(x1,x2) = max{0, x1 - 9, x2 - 8} dropLast_1_A(x1) = max{7, x1 - 37} nil_0_A = 0 last_1#!_A(x1) = x1 + 23 cons_2!_A(x1,x2) = x2 + 33 dropLast_1!_A(x1) = 39 nil_0!_A = 32 2. marked-algebra reduction triple (>=A, >=A!, >A!): matrix interpretation with standard point-wise order: carrier: N^1 order: standard order interpretations: last_1#_A(x1) = x1 cons_2_A(x1,x2) = x1 + x2 + 5 dropLast_1_A(x1) = x1 + 6 nil_0_A() = 9 last_1#!_A(x1) = 3 cons_2!_A(x1,x2) = x2 + 2 dropLast_1!_A(x1) = 6 nil_0!_A() = 7 partial status: pi(last_1#) = [1] pi(cons_2) = [2] pi(dropLast_1) = [] pi(nil_0) = [] The following rules are removed: p1 Then no dependency pair remains.