YES We show the termination of the TRS R: ap(ap(ff(),x),x) -> ap(ap(x,ap(ff(),x)),ap(ap(cons(),x),nil())) 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(ff_0(),y) -> ff_1(y) ap(ff_1(x1),y) -> ff_2(x1,y) ff_2(x,x) -> ap(ap(x,ff_1(x)),cons_2(x,nil_0())) -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: ap#(ff_1(x1),y) -> ff_2#(x1,y) p2: ff_2#(x,x) -> ap#(ap(x,ff_1(x)),cons_2(x,nil_0())) p3: ff_2#(x,x) -> ap#(x,ff_1(x)) and R consists of: r1: ap(cons_0(),y) -> cons_1(y) r2: ap(cons_1(x1),y) -> cons_2(x1,y) r3: ap(ff_0(),y) -> ff_1(y) r4: ap(ff_1(x1),y) -> ff_2(x1,y) r5: ff_2(x,x) -> ap(ap(x,ff_1(x)),cons_2(x,nil_0())) The estimated dependency graph contains the following SCCs: {p1, p2, p3} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: ap#(ff_1(x1),y) -> ff_2#(x1,y) p2: ff_2#(x,x) -> ap#(x,ff_1(x)) p3: ff_2#(x,x) -> ap#(ap(x,ff_1(x)),cons_2(x,nil_0())) and R consists of: r1: ap(cons_0(),y) -> cons_1(y) r2: ap(cons_1(x1),y) -> cons_2(x1,y) r3: ap(ff_0(),y) -> ff_1(y) r4: ap(ff_1(x1),y) -> ff_2(x1,y) r5: ff_2(x,x) -> ap(ap(x,ff_1(x)),cons_2(x,nil_0())) The set of usable rules consists of r1, r2, r3, r4, r5 Take the reduction pair: generalized weighted path order (>=MG, >G) base order 1: max/plus interpretation on natural numbers: ap#_A(x1,x2) = max{x1 + 47, x2 + 47} ff_1_A(x1) = max{13, x1 - 18} ff_2#_A(x1,x2) = max{60, x1 + 14, x2 + 47} ap_A(x1,x2) = max{3, x1 - 8, x2 - 14} cons_2_A(x1,x2) = max{1, x2 - 49} nil_0_A = 1 cons_0_A = 11 cons_1_A(x1) = max{2, x1 - 15} ff_0_A = 22 ff_2_A(x1,x2) = max{4, x2 - 15} base order 2: marked-algebra reduction triple (>=A, >=A!, >A!): max/plus interpretation on natural numbers: ap#_A(x1,x2) = 1 ff_1_A(x1) = max{11, x1 + 9} ff_2#_A(x1,x2) = 1 ap_A(x1,x2) = max{23, x2 + 10} cons_2_A(x1,x2) = max{13, x2 + 10} nil_0_A = 2 cons_0_A = 23 cons_1_A(x1) = max{23, x1 + 10} ff_0_A = 4 ff_2_A(x1,x2) = 23 ap#!_A(x1,x2) = max{1, x1 - 4} ff_1!_A(x1) = x1 + 6 ff_2#!_A(x1,x2) = max{6, x1 - 3} ap!_A(x1,x2) = max{3, x1 - 5} cons_2!_A(x1,x2) = max{4, x1 - 7} nil_0!_A = 1 cons_0!_A = 1 cons_1!_A(x1) = max{18, x1 - 8} ff_0!_A = 1 ff_2!_A(x1,x2) = max{7, x2 - 6} partial status: pi(ap#) = [] pi(ff_1) = [] pi(ff_2#) = [] pi(ap) = [] pi(cons_2) = [] pi(nil_0) = [] pi(cons_0) = [] pi(cons_1) = [] pi(ff_0) = [] pi(ff_2) = [] The following rules are removed: p1, p2, p3 Then no dependency pair remains.