YES We show the termination of the TRS R: app(app(mapt(),f),app(leaf(),x)) -> app(leaf(),app(f,x)) app(app(mapt(),f),app(node(),xs)) -> app(node(),app(app(maptlist(),f),xs)) app(app(maptlist(),f),nil()) -> nil() app(app(maptlist(),f),app(app(cons(),x),xs)) -> app(app(cons(),app(app(mapt(),f),x)),app(app(maptlist(),f),xs)) Instead we prove termination of the uncurried system: app(cons_0(),y) -> cons_1(y) app(cons_1(x1),y) -> cons_2(x1,y) app(leaf_0(),y) -> leaf_1(y) app(mapt_0(),y) -> mapt_1(y) app(mapt_1(x1),y) -> mapt_2(x1,y) app(maptlist_0(),y) -> maptlist_1(y) app(maptlist_1(x1),y) -> maptlist_2(x1,y) app(node_0(),y) -> node_1(y) mapt_2(f,leaf_1(x)) -> leaf_1(app(f,x)) mapt_2(f,node_1(xs)) -> node_1(maptlist_2(f,xs)) maptlist_2(f,nil_0()) -> nil_0() maptlist_2(f,cons_2(x,xs)) -> cons_2(mapt_2(f,x),maptlist_2(f,xs)) -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: app#(mapt_1(x1),y) -> mapt_2#(x1,y) p2: app#(maptlist_1(x1),y) -> maptlist_2#(x1,y) p3: mapt_2#(f,leaf_1(x)) -> app#(f,x) p4: mapt_2#(f,node_1(xs)) -> maptlist_2#(f,xs) p5: maptlist_2#(f,cons_2(x,xs)) -> mapt_2#(f,x) p6: maptlist_2#(f,cons_2(x,xs)) -> maptlist_2#(f,xs) and R consists of: r1: app(cons_0(),y) -> cons_1(y) r2: app(cons_1(x1),y) -> cons_2(x1,y) r3: app(leaf_0(),y) -> leaf_1(y) r4: app(mapt_0(),y) -> mapt_1(y) r5: app(mapt_1(x1),y) -> mapt_2(x1,y) r6: app(maptlist_0(),y) -> maptlist_1(y) r7: app(maptlist_1(x1),y) -> maptlist_2(x1,y) r8: app(node_0(),y) -> node_1(y) r9: mapt_2(f,leaf_1(x)) -> leaf_1(app(f,x)) r10: mapt_2(f,node_1(xs)) -> node_1(maptlist_2(f,xs)) r11: maptlist_2(f,nil_0()) -> nil_0() r12: maptlist_2(f,cons_2(x,xs)) -> cons_2(mapt_2(f,x),maptlist_2(f,xs)) The estimated dependency graph contains the following SCCs: {p1, p2, p3, p4, p5, p6} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: app#(mapt_1(x1),y) -> mapt_2#(x1,y) p2: mapt_2#(f,node_1(xs)) -> maptlist_2#(f,xs) p3: maptlist_2#(f,cons_2(x,xs)) -> maptlist_2#(f,xs) p4: maptlist_2#(f,cons_2(x,xs)) -> mapt_2#(f,x) p5: mapt_2#(f,leaf_1(x)) -> app#(f,x) p6: app#(maptlist_1(x1),y) -> maptlist_2#(x1,y) and R consists of: r1: app(cons_0(),y) -> cons_1(y) r2: app(cons_1(x1),y) -> cons_2(x1,y) r3: app(leaf_0(),y) -> leaf_1(y) r4: app(mapt_0(),y) -> mapt_1(y) r5: app(mapt_1(x1),y) -> mapt_2(x1,y) r6: app(maptlist_0(),y) -> maptlist_1(y) r7: app(maptlist_1(x1),y) -> maptlist_2(x1,y) r8: app(node_0(),y) -> node_1(y) r9: mapt_2(f,leaf_1(x)) -> leaf_1(app(f,x)) r10: mapt_2(f,node_1(xs)) -> node_1(maptlist_2(f,xs)) r11: maptlist_2(f,nil_0()) -> nil_0() r12: maptlist_2(f,cons_2(x,xs)) -> cons_2(mapt_2(f,x),maptlist_2(f,xs)) The set of usable rules consists of r2, r3, r8 Take the reduction pair: generalized weighted path order (>=MG, >MG) base order 1: max/plus interpretation on natural numbers: app#_A(x1,x2) = max{0, x1 - 3} mapt_1_A(x1) = x1 + 3 mapt_2#_A(x1,x2) = x1 node_1_A(x1) = max{4, x1 - 13} maptlist_2#_A(x1,x2) = x1 cons_2_A(x1,x2) = max{1, x1 - 15, x2 - 30} leaf_1_A(x1) = max{2, x1 - 13} maptlist_1_A(x1) = x1 + 4 app_A(x1,x2) = max{5, x1 - 8, x2 - 11} cons_1_A(x1) = max{6, x1 - 1} leaf_0_A = 9 node_0_A = 7 base order 2: precedence: app > mapt_1 = leaf_1 = maptlist_1 > app# = mapt_2# = maptlist_2# = cons_2 = leaf_0 > node_1 = cons_1 > node_0 partial status: pi(app#) = [] pi(mapt_1) = [] pi(mapt_2#) = [] pi(node_1) = [] pi(maptlist_2#) = [] pi(cons_2) = [] pi(leaf_1) = [] pi(maptlist_1) = [] pi(app) = [] pi(cons_1) = [] pi(leaf_0) = [] pi(node_0) = [] The following rules are removed: p6 -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: app#(mapt_1(x1),y) -> mapt_2#(x1,y) p2: mapt_2#(f,node_1(xs)) -> maptlist_2#(f,xs) p3: maptlist_2#(f,cons_2(x,xs)) -> maptlist_2#(f,xs) p4: maptlist_2#(f,cons_2(x,xs)) -> mapt_2#(f,x) p5: mapt_2#(f,leaf_1(x)) -> app#(f,x) and R consists of: r1: app(cons_0(),y) -> cons_1(y) r2: app(cons_1(x1),y) -> cons_2(x1,y) r3: app(leaf_0(),y) -> leaf_1(y) r4: app(mapt_0(),y) -> mapt_1(y) r5: app(mapt_1(x1),y) -> mapt_2(x1,y) r6: app(maptlist_0(),y) -> maptlist_1(y) r7: app(maptlist_1(x1),y) -> maptlist_2(x1,y) r8: app(node_0(),y) -> node_1(y) r9: mapt_2(f,leaf_1(x)) -> leaf_1(app(f,x)) r10: mapt_2(f,node_1(xs)) -> node_1(maptlist_2(f,xs)) r11: maptlist_2(f,nil_0()) -> nil_0() r12: maptlist_2(f,cons_2(x,xs)) -> cons_2(mapt_2(f,x),maptlist_2(f,xs)) The estimated dependency graph contains the following SCCs: {p1, p2, p3, p4, p5} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: app#(mapt_1(x1),y) -> mapt_2#(x1,y) p2: mapt_2#(f,leaf_1(x)) -> app#(f,x) p3: mapt_2#(f,node_1(xs)) -> maptlist_2#(f,xs) p4: maptlist_2#(f,cons_2(x,xs)) -> mapt_2#(f,x) p5: maptlist_2#(f,cons_2(x,xs)) -> maptlist_2#(f,xs) and R consists of: r1: app(cons_0(),y) -> cons_1(y) r2: app(cons_1(x1),y) -> cons_2(x1,y) r3: app(leaf_0(),y) -> leaf_1(y) r4: app(mapt_0(),y) -> mapt_1(y) r5: app(mapt_1(x1),y) -> mapt_2(x1,y) r6: app(maptlist_0(),y) -> maptlist_1(y) r7: app(maptlist_1(x1),y) -> maptlist_2(x1,y) r8: app(node_0(),y) -> node_1(y) r9: mapt_2(f,leaf_1(x)) -> leaf_1(app(f,x)) r10: mapt_2(f,node_1(xs)) -> node_1(maptlist_2(f,xs)) r11: maptlist_2(f,nil_0()) -> nil_0() r12: maptlist_2(f,cons_2(x,xs)) -> cons_2(mapt_2(f,x),maptlist_2(f,xs)) The set of usable rules consists of r1, r2, r3, r6, r8 Take the reduction pair: generalized weighted path order (>=MG, >MG) base order 1: max/plus interpretation on natural numbers: app#_A(x1,x2) = max{3, x1 - 6} mapt_1_A(x1) = max{25, x1 + 5} mapt_2#_A(x1,x2) = max{4, x1 - 2} leaf_1_A(x1) = max{2, x1 - 21} node_1_A(x1) = max{3, x1 - 18} maptlist_2#_A(x1,x2) = max{4, x1 - 2} cons_2_A(x1,x2) = max{3, x1 - 29, x2 - 29} app_A(x1,x2) = max{24, x1 - 26, x2 - 1} cons_0_A = 1 cons_1_A(x1) = max{2, x1 - 2} leaf_0_A = 1 maptlist_0_A = 23 maptlist_1_A(x1) = max{24, x1 - 1} node_0_A = 2 base order 2: precedence: mapt_2# = maptlist_2# > app# = node_1 > node_0 > mapt_1 > app > leaf_1 = cons_2 = maptlist_1 > cons_1 = leaf_0 = maptlist_0 > cons_0 partial status: pi(app#) = [] pi(mapt_1) = [1] pi(mapt_2#) = [] pi(leaf_1) = [] pi(node_1) = [] pi(maptlist_2#) = [] pi(cons_2) = [] pi(app) = [] pi(cons_0) = [] pi(cons_1) = [] pi(leaf_0) = [] pi(maptlist_0) = [] pi(maptlist_1) = [] pi(node_0) = [] The following rules are removed: p1 -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: mapt_2#(f,leaf_1(x)) -> app#(f,x) p2: mapt_2#(f,node_1(xs)) -> maptlist_2#(f,xs) p3: maptlist_2#(f,cons_2(x,xs)) -> mapt_2#(f,x) p4: maptlist_2#(f,cons_2(x,xs)) -> maptlist_2#(f,xs) and R consists of: r1: app(cons_0(),y) -> cons_1(y) r2: app(cons_1(x1),y) -> cons_2(x1,y) r3: app(leaf_0(),y) -> leaf_1(y) r4: app(mapt_0(),y) -> mapt_1(y) r5: app(mapt_1(x1),y) -> mapt_2(x1,y) r6: app(maptlist_0(),y) -> maptlist_1(y) r7: app(maptlist_1(x1),y) -> maptlist_2(x1,y) r8: app(node_0(),y) -> node_1(y) r9: mapt_2(f,leaf_1(x)) -> leaf_1(app(f,x)) r10: mapt_2(f,node_1(xs)) -> node_1(maptlist_2(f,xs)) r11: maptlist_2(f,nil_0()) -> nil_0() r12: maptlist_2(f,cons_2(x,xs)) -> cons_2(mapt_2(f,x),maptlist_2(f,xs)) The estimated dependency graph contains the following SCCs: {p2, p3, p4} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: mapt_2#(f,node_1(xs)) -> maptlist_2#(f,xs) p2: maptlist_2#(f,cons_2(x,xs)) -> maptlist_2#(f,xs) p3: maptlist_2#(f,cons_2(x,xs)) -> mapt_2#(f,x) and R consists of: r1: app(cons_0(),y) -> cons_1(y) r2: app(cons_1(x1),y) -> cons_2(x1,y) r3: app(leaf_0(),y) -> leaf_1(y) r4: app(mapt_0(),y) -> mapt_1(y) r5: app(mapt_1(x1),y) -> mapt_2(x1,y) r6: app(maptlist_0(),y) -> maptlist_1(y) r7: app(maptlist_1(x1),y) -> maptlist_2(x1,y) r8: app(node_0(),y) -> node_1(y) r9: mapt_2(f,leaf_1(x)) -> leaf_1(app(f,x)) r10: mapt_2(f,node_1(xs)) -> node_1(maptlist_2(f,xs)) r11: maptlist_2(f,nil_0()) -> nil_0() r12: maptlist_2(f,cons_2(x,xs)) -> cons_2(mapt_2(f,x),maptlist_2(f,xs)) The set of usable rules consists of r1, r2, r3, r4, r6, r8 Take the reduction pair: generalized weighted path order (>=MG, >MG) base order 1: max/plus interpretation on natural numbers: mapt_2#_A(x1,x2) = x2 + 8 node_1_A(x1) = max{3, x1 - 5} maptlist_2#_A(x1,x2) = max{2, x2 - 6} cons_2_A(x1,x2) = max{x1 + 23, x2 + 5} app_A(x1,x2) = max{x1 - 14, x2 + 38} cons_0_A = 8 cons_1_A(x1) = x1 + 37 leaf_0_A = 13 leaf_1_A(x1) = max{12, x1 - 39} mapt_0_A = 9 mapt_1_A(x1) = max{10, x1 - 39} maptlist_0_A = 2 maptlist_1_A(x1) = max{3, x1 - 1} node_0_A = 2 base order 2: precedence: cons_0 > node_1 > node_0 > app > cons_2 = leaf_1 = mapt_1 = maptlist_1 > maptlist_2# = cons_1 = leaf_0 = mapt_0 = maptlist_0 > mapt_2# partial status: pi(mapt_2#) = [2] pi(node_1) = [] pi(maptlist_2#) = [] pi(cons_2) = [2] pi(app) = [] pi(cons_0) = [] pi(cons_1) = [] pi(leaf_0) = [] pi(leaf_1) = [] pi(mapt_0) = [] pi(mapt_1) = [] pi(maptlist_0) = [] pi(maptlist_1) = [] pi(node_0) = [] The following rules are removed: p2 -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: mapt_2#(f,node_1(xs)) -> maptlist_2#(f,xs) p2: maptlist_2#(f,cons_2(x,xs)) -> mapt_2#(f,x) and R consists of: r1: app(cons_0(),y) -> cons_1(y) r2: app(cons_1(x1),y) -> cons_2(x1,y) r3: app(leaf_0(),y) -> leaf_1(y) r4: app(mapt_0(),y) -> mapt_1(y) r5: app(mapt_1(x1),y) -> mapt_2(x1,y) r6: app(maptlist_0(),y) -> maptlist_1(y) r7: app(maptlist_1(x1),y) -> maptlist_2(x1,y) r8: app(node_0(),y) -> node_1(y) r9: mapt_2(f,leaf_1(x)) -> leaf_1(app(f,x)) r10: mapt_2(f,node_1(xs)) -> node_1(maptlist_2(f,xs)) r11: maptlist_2(f,nil_0()) -> nil_0() r12: maptlist_2(f,cons_2(x,xs)) -> cons_2(mapt_2(f,x),maptlist_2(f,xs)) The estimated dependency graph contains the following SCCs: {p1, p2} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: mapt_2#(f,node_1(xs)) -> maptlist_2#(f,xs) p2: maptlist_2#(f,cons_2(x,xs)) -> mapt_2#(f,x) and R consists of: r1: app(cons_0(),y) -> cons_1(y) r2: app(cons_1(x1),y) -> cons_2(x1,y) r3: app(leaf_0(),y) -> leaf_1(y) r4: app(mapt_0(),y) -> mapt_1(y) r5: app(mapt_1(x1),y) -> mapt_2(x1,y) r6: app(maptlist_0(),y) -> maptlist_1(y) r7: app(maptlist_1(x1),y) -> maptlist_2(x1,y) r8: app(node_0(),y) -> node_1(y) r9: mapt_2(f,leaf_1(x)) -> leaf_1(app(f,x)) r10: mapt_2(f,node_1(xs)) -> node_1(maptlist_2(f,xs)) r11: maptlist_2(f,nil_0()) -> nil_0() r12: maptlist_2(f,cons_2(x,xs)) -> cons_2(mapt_2(f,x),maptlist_2(f,xs)) The set of usable rules consists of r1, r2, r3, r4, r6 Take the reduction pair: generalized weighted path order (>=MG, >MG) base order 1: max/plus interpretation on natural numbers: mapt_2#_A(x1,x2) = x2 + 2 node_1_A(x1) = x1 + 16 maptlist_2#_A(x1,x2) = x2 + 15 cons_2_A(x1,x2) = max{7, x1 - 12, x2 - 19} app_A(x1,x2) = max{10, x1 - 9, x2 - 1} cons_0_A = 7 cons_1_A(x1) = max{8, x1 - 2} leaf_0_A = 8 leaf_1_A(x1) = max{9, x1 - 11} mapt_0_A = 8 mapt_1_A(x1) = max{7, x1 - 2} maptlist_0_A = 6 maptlist_1_A(x1) = max{7, x1 - 2} base order 2: precedence: node_1 > mapt_2# = maptlist_2# = app = mapt_0 > cons_2 = cons_0 = leaf_1 = mapt_1 = maptlist_1 > cons_1 = leaf_0 = maptlist_0 partial status: pi(mapt_2#) = [2] pi(node_1) = [1] pi(maptlist_2#) = [] pi(cons_2) = [] pi(app) = [] pi(cons_0) = [] pi(cons_1) = [] pi(leaf_0) = [] pi(leaf_1) = [] pi(mapt_0) = [] pi(mapt_1) = [] pi(maptlist_0) = [] pi(maptlist_1) = [] The following rules are removed: p2 -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: mapt_2#(f,node_1(xs)) -> maptlist_2#(f,xs) and R consists of: r1: app(cons_0(),y) -> cons_1(y) r2: app(cons_1(x1),y) -> cons_2(x1,y) r3: app(leaf_0(),y) -> leaf_1(y) r4: app(mapt_0(),y) -> mapt_1(y) r5: app(mapt_1(x1),y) -> mapt_2(x1,y) r6: app(maptlist_0(),y) -> maptlist_1(y) r7: app(maptlist_1(x1),y) -> maptlist_2(x1,y) r8: app(node_0(),y) -> node_1(y) r9: mapt_2(f,leaf_1(x)) -> leaf_1(app(f,x)) r10: mapt_2(f,node_1(xs)) -> node_1(maptlist_2(f,xs)) r11: maptlist_2(f,nil_0()) -> nil_0() r12: maptlist_2(f,cons_2(x,xs)) -> cons_2(mapt_2(f,x),maptlist_2(f,xs)) The estimated dependency graph contains the following SCCs: (no SCCs)