YES We show the termination of the TRS R: g(A()) -> A() g(B()) -> A() g(B()) -> B() g(C()) -> A() g(C()) -> B() g(C()) -> C() foldB(t,|0|()) -> t foldB(t,s(n)) -> f(foldB(t,n),B()) foldC(t,|0|()) -> t foldC(t,s(n)) -> f(foldC(t,n),C()) f(t,x) -> |f'|(t,g(x)) |f'|(triple(a,b,c),C()) -> triple(a,b,s(c)) |f'|(triple(a,b,c),B()) -> f(triple(a,b,c),A()) |f'|(triple(a,b,c),A()) -> |f''|(foldB(triple(s(a),|0|(),c),b)) |f''|(triple(a,b,c)) -> foldC(triple(a,b,|0|()),c) -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: foldB#(t,s(n)) -> f#(foldB(t,n),B()) p2: foldB#(t,s(n)) -> foldB#(t,n) p3: foldC#(t,s(n)) -> f#(foldC(t,n),C()) p4: foldC#(t,s(n)) -> foldC#(t,n) p5: f#(t,x) -> |f'|#(t,g(x)) p6: f#(t,x) -> g#(x) p7: |f'|#(triple(a,b,c),B()) -> f#(triple(a,b,c),A()) p8: |f'|#(triple(a,b,c),A()) -> |f''|#(foldB(triple(s(a),|0|(),c),b)) p9: |f'|#(triple(a,b,c),A()) -> foldB#(triple(s(a),|0|(),c),b) p10: |f''|#(triple(a,b,c)) -> foldC#(triple(a,b,|0|()),c) and R consists of: r1: g(A()) -> A() r2: g(B()) -> A() r3: g(B()) -> B() r4: g(C()) -> A() r5: g(C()) -> B() r6: g(C()) -> C() r7: foldB(t,|0|()) -> t r8: foldB(t,s(n)) -> f(foldB(t,n),B()) r9: foldC(t,|0|()) -> t r10: foldC(t,s(n)) -> f(foldC(t,n),C()) r11: f(t,x) -> |f'|(t,g(x)) r12: |f'|(triple(a,b,c),C()) -> triple(a,b,s(c)) r13: |f'|(triple(a,b,c),B()) -> f(triple(a,b,c),A()) r14: |f'|(triple(a,b,c),A()) -> |f''|(foldB(triple(s(a),|0|(),c),b)) r15: |f''|(triple(a,b,c)) -> foldC(triple(a,b,|0|()),c) The estimated dependency graph contains the following SCCs: {p1, p2, p3, p4, p5, p7, p8, p9, p10} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: foldB#(t,s(n)) -> f#(foldB(t,n),B()) p2: f#(t,x) -> |f'|#(t,g(x)) p3: |f'|#(triple(a,b,c),A()) -> foldB#(triple(s(a),|0|(),c),b) p4: foldB#(t,s(n)) -> foldB#(t,n) p5: |f'|#(triple(a,b,c),A()) -> |f''|#(foldB(triple(s(a),|0|(),c),b)) p6: |f''|#(triple(a,b,c)) -> foldC#(triple(a,b,|0|()),c) p7: foldC#(t,s(n)) -> foldC#(t,n) p8: foldC#(t,s(n)) -> f#(foldC(t,n),C()) p9: |f'|#(triple(a,b,c),B()) -> f#(triple(a,b,c),A()) and R consists of: r1: g(A()) -> A() r2: g(B()) -> A() r3: g(B()) -> B() r4: g(C()) -> A() r5: g(C()) -> B() r6: g(C()) -> C() r7: foldB(t,|0|()) -> t r8: foldB(t,s(n)) -> f(foldB(t,n),B()) r9: foldC(t,|0|()) -> t r10: foldC(t,s(n)) -> f(foldC(t,n),C()) r11: f(t,x) -> |f'|(t,g(x)) r12: |f'|(triple(a,b,c),C()) -> triple(a,b,s(c)) r13: |f'|(triple(a,b,c),B()) -> f(triple(a,b,c),A()) r14: |f'|(triple(a,b,c),A()) -> |f''|(foldB(triple(s(a),|0|(),c),b)) r15: |f''|(triple(a,b,c)) -> foldC(triple(a,b,|0|()),c) The set of usable rules consists of r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r12, r13, r14, r15 Take the reduction pair: weighted path order base order: matrix interpretations: carrier: N^2 order: lexicographic order interpretations: foldB#_A(x1,x2) = x1 + ((1,0),(0,0)) x2 + (8,19) s_A(x1) = ((1,0),(1,1)) x1 + (12,18) f#_A(x1,x2) = ((1,0),(0,0)) x1 + ((1,0),(0,0)) x2 + (3,4) foldB_A(x1,x2) = ((1,0),(1,0)) x1 + ((1,0),(0,0)) x2 + (1,20) B_A() = (11,3) |f'|#_A(x1,x2) = ((1,0),(0,0)) x1 + ((1,0),(1,0)) x2 + (1,2) g_A(x1) = ((1,0),(0,0)) x1 + (1,5) triple_A(x1,x2,x3) = ((1,0),(0,0)) x2 + ((1,0),(0,0)) x3 + (1,2) A_A() = (8,6) |0|_A() = (0,9) |f''|#_A(x1) = ((1,0),(0,0)) x1 + (7,8) foldC#_A(x1,x2) = x1 + ((1,0),(0,0)) x2 + (3,5) foldC_A(x1,x2) = x1 + ((1,0),(0,0)) x2 + (1,17) C_A() = (10,1) |f''|_A(x1) = ((1,0),(0,0)) x1 + (2,10) |f'|_A(x1,x2) = ((1,0),(0,0)) x1 + ((0,0),(1,0)) x2 + (12,4) f_A(x1,x2) = ((1,0),(0,0)) x1 + ((0,0),(1,0)) x2 + (12,6) precedence: s = foldB = B = g > C > A > foldC = |f''| = |f'| = f > |0| > |f''|# > foldB# = f# = |f'|# = triple = foldC# partial status: pi(foldB#) = [] pi(s) = [] pi(f#) = [] pi(foldB) = [] pi(B) = [] pi(|f'|#) = [] pi(g) = [] pi(triple) = [] pi(A) = [] pi(|0|) = [] pi(|f''|#) = [] pi(foldC#) = [] pi(foldC) = [] pi(C) = [] pi(|f''|) = [] pi(|f'|) = [] pi(f) = [] The next rules are strictly ordered: p6 We remove them from the problem. -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: foldB#(t,s(n)) -> f#(foldB(t,n),B()) p2: f#(t,x) -> |f'|#(t,g(x)) p3: |f'|#(triple(a,b,c),A()) -> foldB#(triple(s(a),|0|(),c),b) p4: foldB#(t,s(n)) -> foldB#(t,n) p5: |f'|#(triple(a,b,c),A()) -> |f''|#(foldB(triple(s(a),|0|(),c),b)) p6: foldC#(t,s(n)) -> foldC#(t,n) p7: foldC#(t,s(n)) -> f#(foldC(t,n),C()) p8: |f'|#(triple(a,b,c),B()) -> f#(triple(a,b,c),A()) and R consists of: r1: g(A()) -> A() r2: g(B()) -> A() r3: g(B()) -> B() r4: g(C()) -> A() r5: g(C()) -> B() r6: g(C()) -> C() r7: foldB(t,|0|()) -> t r8: foldB(t,s(n)) -> f(foldB(t,n),B()) r9: foldC(t,|0|()) -> t r10: foldC(t,s(n)) -> f(foldC(t,n),C()) r11: f(t,x) -> |f'|(t,g(x)) r12: |f'|(triple(a,b,c),C()) -> triple(a,b,s(c)) r13: |f'|(triple(a,b,c),B()) -> f(triple(a,b,c),A()) r14: |f'|(triple(a,b,c),A()) -> |f''|(foldB(triple(s(a),|0|(),c),b)) r15: |f''|(triple(a,b,c)) -> foldC(triple(a,b,|0|()),c) The estimated dependency graph contains the following SCCs: {p6} {p1, p2, p3, p4, p8} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: foldC#(t,s(n)) -> foldC#(t,n) and R consists of: r1: g(A()) -> A() r2: g(B()) -> A() r3: g(B()) -> B() r4: g(C()) -> A() r5: g(C()) -> B() r6: g(C()) -> C() r7: foldB(t,|0|()) -> t r8: foldB(t,s(n)) -> f(foldB(t,n),B()) r9: foldC(t,|0|()) -> t r10: foldC(t,s(n)) -> f(foldC(t,n),C()) r11: f(t,x) -> |f'|(t,g(x)) r12: |f'|(triple(a,b,c),C()) -> triple(a,b,s(c)) r13: |f'|(triple(a,b,c),B()) -> f(triple(a,b,c),A()) r14: |f'|(triple(a,b,c),A()) -> |f''|(foldB(triple(s(a),|0|(),c),b)) r15: |f''|(triple(a,b,c)) -> foldC(triple(a,b,|0|()),c) The set of usable rules consists of (no rules) Take the reduction pair: weighted path order base order: matrix interpretations: carrier: N^2 order: lexicographic order interpretations: foldC#_A(x1,x2) = ((1,0),(1,0)) x2 + (1,2) s_A(x1) = ((1,0),(0,0)) x1 + (2,1) precedence: s > foldC# partial status: pi(foldC#) = [] pi(s) = [] The next rules are strictly ordered: p1 We remove them from the problem. Then no dependency pair remains. -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: foldB#(t,s(n)) -> f#(foldB(t,n),B()) p2: f#(t,x) -> |f'|#(t,g(x)) p3: |f'|#(triple(a,b,c),B()) -> f#(triple(a,b,c),A()) p4: |f'|#(triple(a,b,c),A()) -> foldB#(triple(s(a),|0|(),c),b) p5: foldB#(t,s(n)) -> foldB#(t,n) and R consists of: r1: g(A()) -> A() r2: g(B()) -> A() r3: g(B()) -> B() r4: g(C()) -> A() r5: g(C()) -> B() r6: g(C()) -> C() r7: foldB(t,|0|()) -> t r8: foldB(t,s(n)) -> f(foldB(t,n),B()) r9: foldC(t,|0|()) -> t r10: foldC(t,s(n)) -> f(foldC(t,n),C()) r11: f(t,x) -> |f'|(t,g(x)) r12: |f'|(triple(a,b,c),C()) -> triple(a,b,s(c)) r13: |f'|(triple(a,b,c),B()) -> f(triple(a,b,c),A()) r14: |f'|(triple(a,b,c),A()) -> |f''|(foldB(triple(s(a),|0|(),c),b)) r15: |f''|(triple(a,b,c)) -> foldC(triple(a,b,|0|()),c) The set of usable rules consists of r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r12, r13, r14, r15 Take the reduction pair: weighted path order base order: matrix interpretations: carrier: N^2 order: lexicographic order interpretations: foldB#_A(x1,x2) = ((1,0),(0,0)) x1 + ((1,0),(0,0)) x2 + (15,0) s_A(x1) = ((1,0),(1,0)) x1 + (14,13) f#_A(x1,x2) = ((1,0),(0,0)) x1 + ((1,0),(0,0)) x2 + (7,4) foldB_A(x1,x2) = ((1,0),(1,1)) x1 + ((1,0),(0,0)) x2 + (4,14) B_A() = (17,11) |f'|#_A(x1,x2) = ((1,0),(0,0)) x1 + ((1,0),(0,0)) x2 + (4,2) g_A(x1) = x1 + (2,1) triple_A(x1,x2,x3) = ((1,0),(0,0)) x2 + ((1,0),(0,0)) x3 + (0,3) A_A() = (12,1) |0|_A() = (0,6) foldC_A(x1,x2) = ((1,0),(1,1)) x1 + ((1,0),(1,0)) x2 + (1,1) f_A(x1,x2) = ((1,0),(0,0)) x1 + (14,10) C_A() = (16,12) |f''|_A(x1) = ((1,0),(1,0)) x1 + (9,5) |f'|_A(x1,x2) = ((1,0),(0,0)) x1 + (14,10) precedence: f# = foldB = B = |f'|# = g = |0| = foldC = f = C = |f''| = |f'| > foldB# = s = triple = A partial status: pi(foldB#) = [] pi(s) = [] pi(f#) = [] pi(foldB) = [] pi(B) = [] pi(|f'|#) = [] pi(g) = [] pi(triple) = [] pi(A) = [] pi(|0|) = [] pi(foldC) = [] pi(f) = [] pi(C) = [] pi(|f''|) = [] pi(|f'|) = [] The next rules are strictly ordered: p5 We remove them from the problem. -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: foldB#(t,s(n)) -> f#(foldB(t,n),B()) p2: f#(t,x) -> |f'|#(t,g(x)) p3: |f'|#(triple(a,b,c),B()) -> f#(triple(a,b,c),A()) p4: |f'|#(triple(a,b,c),A()) -> foldB#(triple(s(a),|0|(),c),b) and R consists of: r1: g(A()) -> A() r2: g(B()) -> A() r3: g(B()) -> B() r4: g(C()) -> A() r5: g(C()) -> B() r6: g(C()) -> C() r7: foldB(t,|0|()) -> t r8: foldB(t,s(n)) -> f(foldB(t,n),B()) r9: foldC(t,|0|()) -> t r10: foldC(t,s(n)) -> f(foldC(t,n),C()) r11: f(t,x) -> |f'|(t,g(x)) r12: |f'|(triple(a,b,c),C()) -> triple(a,b,s(c)) r13: |f'|(triple(a,b,c),B()) -> f(triple(a,b,c),A()) r14: |f'|(triple(a,b,c),A()) -> |f''|(foldB(triple(s(a),|0|(),c),b)) r15: |f''|(triple(a,b,c)) -> foldC(triple(a,b,|0|()),c) The estimated dependency graph contains the following SCCs: {p1, p2, p3, p4} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: foldB#(t,s(n)) -> f#(foldB(t,n),B()) p2: f#(t,x) -> |f'|#(t,g(x)) p3: |f'|#(triple(a,b,c),A()) -> foldB#(triple(s(a),|0|(),c),b) p4: |f'|#(triple(a,b,c),B()) -> f#(triple(a,b,c),A()) and R consists of: r1: g(A()) -> A() r2: g(B()) -> A() r3: g(B()) -> B() r4: g(C()) -> A() r5: g(C()) -> B() r6: g(C()) -> C() r7: foldB(t,|0|()) -> t r8: foldB(t,s(n)) -> f(foldB(t,n),B()) r9: foldC(t,|0|()) -> t r10: foldC(t,s(n)) -> f(foldC(t,n),C()) r11: f(t,x) -> |f'|(t,g(x)) r12: |f'|(triple(a,b,c),C()) -> triple(a,b,s(c)) r13: |f'|(triple(a,b,c),B()) -> f(triple(a,b,c),A()) r14: |f'|(triple(a,b,c),A()) -> |f''|(foldB(triple(s(a),|0|(),c),b)) r15: |f''|(triple(a,b,c)) -> foldC(triple(a,b,|0|()),c) The set of usable rules consists of r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r12, r13, r14, r15 Take the reduction pair: weighted path order base order: matrix interpretations: carrier: N^2 order: lexicographic order interpretations: foldB#_A(x1,x2) = ((1,0),(1,1)) x1 + ((1,0),(0,0)) x2 + (0,27) s_A(x1) = ((1,0),(0,0)) x1 + (18,1) f#_A(x1,x2) = ((1,0),(1,1)) x1 + x2 + (4,23) foldB_A(x1,x2) = x1 + ((1,0),(1,0)) x2 + (1,2) B_A() = (12,21) |f'|#_A(x1,x2) = x1 + ((1,0),(1,0)) x2 + (1,22) g_A(x1) = ((1,0),(0,0)) x1 + (2,22) triple_A(x1,x2,x3) = ((1,0),(1,0)) x2 + ((1,0),(0,0)) x3 + (2,8) A_A() = (8,10) |0|_A() = (1,0) foldC_A(x1,x2) = x1 + ((1,0),(1,0)) x2 + (1,2) f_A(x1,x2) = x1 + ((0,0),(1,0)) x2 + (18,4) C_A() = (11,2) |f''|_A(x1) = ((1,0),(1,0)) x1 + (3,9) |f'|_A(x1,x2) = x1 + ((0,0),(1,0)) x2 + (18,1) precedence: s = foldB = foldC = f = C > foldB# > |f''| = |f'| > f# = B = |f'|# = g = A = |0| > triple partial status: pi(foldB#) = [1] pi(s) = [] pi(f#) = [1] pi(foldB) = [] pi(B) = [] pi(|f'|#) = [1] pi(g) = [] pi(triple) = [] pi(A) = [] pi(|0|) = [] pi(foldC) = [] pi(f) = [] pi(C) = [] pi(|f''|) = [] pi(|f'|) = [] The next rules are strictly ordered: p4 We remove them from the problem. -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: foldB#(t,s(n)) -> f#(foldB(t,n),B()) p2: f#(t,x) -> |f'|#(t,g(x)) p3: |f'|#(triple(a,b,c),A()) -> foldB#(triple(s(a),|0|(),c),b) and R consists of: r1: g(A()) -> A() r2: g(B()) -> A() r3: g(B()) -> B() r4: g(C()) -> A() r5: g(C()) -> B() r6: g(C()) -> C() r7: foldB(t,|0|()) -> t r8: foldB(t,s(n)) -> f(foldB(t,n),B()) r9: foldC(t,|0|()) -> t r10: foldC(t,s(n)) -> f(foldC(t,n),C()) r11: f(t,x) -> |f'|(t,g(x)) r12: |f'|(triple(a,b,c),C()) -> triple(a,b,s(c)) r13: |f'|(triple(a,b,c),B()) -> f(triple(a,b,c),A()) r14: |f'|(triple(a,b,c),A()) -> |f''|(foldB(triple(s(a),|0|(),c),b)) r15: |f''|(triple(a,b,c)) -> foldC(triple(a,b,|0|()),c) 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: foldB#(t,s(n)) -> f#(foldB(t,n),B()) p2: f#(t,x) -> |f'|#(t,g(x)) p3: |f'|#(triple(a,b,c),A()) -> foldB#(triple(s(a),|0|(),c),b) and R consists of: r1: g(A()) -> A() r2: g(B()) -> A() r3: g(B()) -> B() r4: g(C()) -> A() r5: g(C()) -> B() r6: g(C()) -> C() r7: foldB(t,|0|()) -> t r8: foldB(t,s(n)) -> f(foldB(t,n),B()) r9: foldC(t,|0|()) -> t r10: foldC(t,s(n)) -> f(foldC(t,n),C()) r11: f(t,x) -> |f'|(t,g(x)) r12: |f'|(triple(a,b,c),C()) -> triple(a,b,s(c)) r13: |f'|(triple(a,b,c),B()) -> f(triple(a,b,c),A()) r14: |f'|(triple(a,b,c),A()) -> |f''|(foldB(triple(s(a),|0|(),c),b)) r15: |f''|(triple(a,b,c)) -> foldC(triple(a,b,|0|()),c) The set of usable rules consists of r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r12, r13, r14, r15 Take the reduction pair: weighted path order base order: matrix interpretations: carrier: N^2 order: lexicographic order interpretations: foldB#_A(x1,x2) = ((1,0),(0,0)) x1 + ((1,0),(0,0)) x2 + (6,1) s_A(x1) = ((1,0),(1,0)) x1 + (28,1) f#_A(x1,x2) = ((1,0),(0,0)) x1 + (26,3) foldB_A(x1,x2) = ((1,0),(0,0)) x1 + ((1,0),(0,0)) x2 + (3,63) B_A() = (33,31) |f'|#_A(x1,x2) = ((1,0),(0,0)) x1 + (15,2) g_A(x1) = ((1,0),(0,0)) x1 + (27,35) triple_A(x1,x2,x3) = ((1,0),(0,0)) x2 + ((1,0),(0,0)) x3 + (7,33) A_A() = (1,32) |0|_A() = (8,0) foldC_A(x1,x2) = x1 + ((1,0),(1,1)) x2 + (7,35) f_A(x1,x2) = ((1,0),(0,0)) x1 + ((0,0),(1,0)) x2 + (28,29) C_A() = (34,34) |f''|_A(x1) = ((1,0),(1,0)) x1 + (16,62) |f'|_A(x1,x2) = ((1,0),(0,0)) x1 + ((0,0),(1,0)) x2 + (28,1) precedence: foldB# = s = f# = foldB = B = |f'|# = g = triple = A = |0| = foldC = f = C = |f''| = |f'| partial status: pi(foldB#) = [] pi(s) = [] pi(f#) = [] pi(foldB) = [] pi(B) = [] pi(|f'|#) = [] pi(g) = [] pi(triple) = [] pi(A) = [] pi(|0|) = [] pi(foldC) = [] pi(f) = [] pi(C) = [] pi(|f''|) = [] pi(|f'|) = [] The next rules are strictly ordered: p1 We remove them from the problem. -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: f#(t,x) -> |f'|#(t,g(x)) p2: |f'|#(triple(a,b,c),A()) -> foldB#(triple(s(a),|0|(),c),b) and R consists of: r1: g(A()) -> A() r2: g(B()) -> A() r3: g(B()) -> B() r4: g(C()) -> A() r5: g(C()) -> B() r6: g(C()) -> C() r7: foldB(t,|0|()) -> t r8: foldB(t,s(n)) -> f(foldB(t,n),B()) r9: foldC(t,|0|()) -> t r10: foldC(t,s(n)) -> f(foldC(t,n),C()) r11: f(t,x) -> |f'|(t,g(x)) r12: |f'|(triple(a,b,c),C()) -> triple(a,b,s(c)) r13: |f'|(triple(a,b,c),B()) -> f(triple(a,b,c),A()) r14: |f'|(triple(a,b,c),A()) -> |f''|(foldB(triple(s(a),|0|(),c),b)) r15: |f''|(triple(a,b,c)) -> foldC(triple(a,b,|0|()),c) The estimated dependency graph contains the following SCCs: (no SCCs)