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 (no rules) 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: app#_A(x1,x2) = max{0, x1 - 27, x2 - 1} mapt_1_A(x1) = max{26, x1 + 18} mapt_2#_A(x1,x2) = max{0, x1 - 27, x2 - 21} node_1_A(x1) = x1 + 19 maptlist_2#_A(x1,x2) = max{0, x1 - 27, x2 - 8} cons_2_A(x1,x2) = max{7, x1 - 7, x2 + 1} leaf_1_A(x1) = x1 + 20 maptlist_1_A(x1) = max{24, x1} app#!_A(x1,x2) = max{8, x1 - 27, x2 - 31} mapt_1!_A(x1) = max{2, x1 - 28} mapt_2#!_A(x1,x2) = max{8, x1 - 27, x2 - 51} node_1!_A(x1) = max{7, x1 - 32} maptlist_2#!_A(x1,x2) = max{8, x1 - 27, x2 - 32} cons_2!_A(x1,x2) = max{0, x1 - 52, x2 - 45} leaf_1!_A(x1) = max{5, x1 - 1} maptlist_1!_A(x1) = max{2, x1 - 68} 2. marked-algebra reduction triple (>=A, >=A!, >A!): max/plus interpretation on natural numbers: app#_A(x1,x2) = max{0, x1 - 11, x2 - 8} mapt_1_A(x1) = max{2, x1 + 1} mapt_2#_A(x1,x2) = max{0, x1 - 11, x2 - 24} node_1_A(x1) = x1 + 23 maptlist_2#_A(x1,x2) = max{0, x1 - 11, x2 - 8} cons_2_A(x1,x2) = max{3, x1 - 3, x2 + 1} leaf_1_A(x1) = x1 + 16 maptlist_1_A(x1) = x1 + 10 app#!_A(x1,x2) = max{4, x1 - 3, x2 - 2} mapt_1!_A(x1) = max{2, x1 - 40} mapt_2#!_A(x1,x2) = max{4, x1 - 2, x2 - 17} node_1!_A(x1) = max{5, x1 - 33} maptlist_2#!_A(x1,x2) = max{6, x1 - 2, x2 - 4} cons_2!_A(x1,x2) = max{3, x1 - 29, x2 - 32} leaf_1!_A(x1) = max{0, x1 - 41} maptlist_1!_A(x1) = max{7, x1 - 1} partial status: pi(app#) = [1] pi(mapt_1) = [1] pi(mapt_2#) = [1] pi(node_1) = [1] pi(maptlist_2#) = [1] pi(cons_2) = [2] pi(leaf_1) = [1] pi(maptlist_1) = [1] 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 (no rules) 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: app#_A(x1,x2) = max{0, x1 - 10, x2 - 14} mapt_1_A(x1) = x1 + 9 mapt_2#_A(x1,x2) = max{0, x1 - 1, x2 - 14} leaf_1_A(x1) = x1 + 11 node_1_A(x1) = max{13, x1 + 5} maptlist_2#_A(x1,x2) = max{0, x1 - 1, x2 - 9} cons_2_A(x1,x2) = max{3, x1 - 3, x2} app#!_A(x1,x2) = max{5, x1 - 3, x2 - 1} mapt_1!_A(x1) = max{0, x1 - 1} mapt_2#!_A(x1,x2) = max{5, x1 - 3, x2 - 12} leaf_1!_A(x1) = max{1, x1 - 15} node_1!_A(x1) = max{4, x1 - 8} maptlist_2#!_A(x1,x2) = max{5, x1 - 3, x2 - 8} cons_2!_A(x1,x2) = max{0, x1 - 13} 2. marked-algebra reduction triple (>=A, >=A!, >A!): max/plus interpretation on natural numbers: app#_A(x1,x2) = max{0, x1 - 11, x2 - 6} mapt_1_A(x1) = x1 + 10 mapt_2#_A(x1,x2) = max{0, x1 - 1, x2 - 25} leaf_1_A(x1) = max{20, x1 + 19} node_1_A(x1) = max{20, x1 + 19} maptlist_2#_A(x1,x2) = max{0, x1 - 1, x2 - 6} cons_2_A(x1,x2) = max{x1 - 7, x2 + 5} app#!_A(x1,x2) = max{2, x1 - 11, x2 - 3} mapt_1!_A(x1) = max{0, x1 - 18} mapt_2#!_A(x1,x2) = max{x1 + 8, x2 - 21} leaf_1!_A(x1) = max{1, x1 - 4} node_1!_A(x1) = max{7, x1 - 7} maptlist_2#!_A(x1,x2) = max{x1 + 8, x2 - 8} cons_2!_A(x1,x2) = max{4, x1 - 8, x2 - 20} partial status: pi(app#) = [] pi(mapt_1) = [1] pi(mapt_2#) = [] pi(leaf_1) = [1] pi(node_1) = [1] pi(maptlist_2#) = [] pi(cons_2) = [1] The following rules are removed: p1, 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) p3: 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} -- 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 (no rules) 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: mapt_2#_A(x1,x2) = max{0, x1 - 1, x2 - 35} node_1_A(x1) = max{19, x1 + 18} maptlist_2#_A(x1,x2) = max{0, x1 - 1, x2 - 17} cons_2_A(x1,x2) = max{16, x1 - 3, x2 + 10} mapt_2#!_A(x1,x2) = max{3, x1 - 1, x2 - 20} node_1!_A(x1) = max{8, x1 - 3} maptlist_2#!_A(x1,x2) = max{3, x1 - 1, x2 - 17} cons_2!_A(x1,x2) = max{4, x1 - 6, x2 - 3} 2. marked-algebra reduction triple (>=A, >=A!, >A!): max/plus interpretation on natural numbers: mapt_2#_A(x1,x2) = max{0, x1 - 1, x2 - 20} node_1_A(x1) = max{12, x1 + 7} maptlist_2#_A(x1,x2) = max{0, x1 - 1, x2 - 15} cons_2_A(x1,x2) = max{14, x1 - 5, x2 + 11} mapt_2#!_A(x1,x2) = max{1, x1 - 1, x2 - 22} node_1!_A(x1) = max{0, x1 - 26} maptlist_2#!_A(x1,x2) = max{1, x1 - 1, x2 - 15} cons_2!_A(x1,x2) = max{0, x1 - 14, x2 - 26} partial status: pi(mapt_2#) = [2] pi(node_1) = [1] pi(maptlist_2#) = [2] pi(cons_2) = [1, 2] The following rules are removed: p2, p3 -- 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)