YES We show the termination of the TRS R: a__zeros() -> cons(|0|(),zeros()) a__U11(tt(),L) -> s(a__length(mark(L))) a__and(tt(),X) -> mark(X) a__isNat(|0|()) -> tt() a__isNat(length(V1)) -> a__isNatList(V1) a__isNat(s(V1)) -> a__isNat(V1) a__isNatIList(V) -> a__isNatList(V) a__isNatIList(zeros()) -> tt() a__isNatIList(cons(V1,V2)) -> a__and(a__isNat(V1),isNatIList(V2)) a__isNatList(nil()) -> tt() a__isNatList(cons(V1,V2)) -> a__and(a__isNat(V1),isNatList(V2)) a__length(nil()) -> |0|() a__length(cons(N,L)) -> a__U11(a__and(a__isNatList(L),isNat(N)),L) mark(zeros()) -> a__zeros() mark(U11(X1,X2)) -> a__U11(mark(X1),X2) mark(length(X)) -> a__length(mark(X)) mark(and(X1,X2)) -> a__and(mark(X1),X2) mark(isNat(X)) -> a__isNat(X) mark(isNatList(X)) -> a__isNatList(X) mark(isNatIList(X)) -> a__isNatIList(X) mark(cons(X1,X2)) -> cons(mark(X1),X2) mark(|0|()) -> |0|() mark(tt()) -> tt() mark(s(X)) -> s(mark(X)) mark(nil()) -> nil() a__zeros() -> zeros() a__U11(X1,X2) -> U11(X1,X2) a__length(X) -> length(X) a__and(X1,X2) -> and(X1,X2) a__isNat(X) -> isNat(X) a__isNatList(X) -> isNatList(X) a__isNatIList(X) -> isNatIList(X) -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: a__U11#(tt(),L) -> a__length#(mark(L)) p2: a__U11#(tt(),L) -> mark#(L) p3: a__and#(tt(),X) -> mark#(X) p4: a__isNat#(length(V1)) -> a__isNatList#(V1) p5: a__isNat#(s(V1)) -> a__isNat#(V1) p6: a__isNatIList#(V) -> a__isNatList#(V) p7: a__isNatIList#(cons(V1,V2)) -> a__and#(a__isNat(V1),isNatIList(V2)) p8: a__isNatIList#(cons(V1,V2)) -> a__isNat#(V1) p9: a__isNatList#(cons(V1,V2)) -> a__and#(a__isNat(V1),isNatList(V2)) p10: a__isNatList#(cons(V1,V2)) -> a__isNat#(V1) p11: a__length#(cons(N,L)) -> a__U11#(a__and(a__isNatList(L),isNat(N)),L) p12: a__length#(cons(N,L)) -> a__and#(a__isNatList(L),isNat(N)) p13: a__length#(cons(N,L)) -> a__isNatList#(L) p14: mark#(zeros()) -> a__zeros#() p15: mark#(U11(X1,X2)) -> a__U11#(mark(X1),X2) p16: mark#(U11(X1,X2)) -> mark#(X1) p17: mark#(length(X)) -> a__length#(mark(X)) p18: mark#(length(X)) -> mark#(X) p19: mark#(and(X1,X2)) -> a__and#(mark(X1),X2) p20: mark#(and(X1,X2)) -> mark#(X1) p21: mark#(isNat(X)) -> a__isNat#(X) p22: mark#(isNatList(X)) -> a__isNatList#(X) p23: mark#(isNatIList(X)) -> a__isNatIList#(X) p24: mark#(cons(X1,X2)) -> mark#(X1) p25: mark#(s(X)) -> mark#(X) and R consists of: r1: a__zeros() -> cons(|0|(),zeros()) r2: a__U11(tt(),L) -> s(a__length(mark(L))) r3: a__and(tt(),X) -> mark(X) r4: a__isNat(|0|()) -> tt() r5: a__isNat(length(V1)) -> a__isNatList(V1) r6: a__isNat(s(V1)) -> a__isNat(V1) r7: a__isNatIList(V) -> a__isNatList(V) r8: a__isNatIList(zeros()) -> tt() r9: a__isNatIList(cons(V1,V2)) -> a__and(a__isNat(V1),isNatIList(V2)) r10: a__isNatList(nil()) -> tt() r11: a__isNatList(cons(V1,V2)) -> a__and(a__isNat(V1),isNatList(V2)) r12: a__length(nil()) -> |0|() r13: a__length(cons(N,L)) -> a__U11(a__and(a__isNatList(L),isNat(N)),L) r14: mark(zeros()) -> a__zeros() r15: mark(U11(X1,X2)) -> a__U11(mark(X1),X2) r16: mark(length(X)) -> a__length(mark(X)) r17: mark(and(X1,X2)) -> a__and(mark(X1),X2) r18: mark(isNat(X)) -> a__isNat(X) r19: mark(isNatList(X)) -> a__isNatList(X) r20: mark(isNatIList(X)) -> a__isNatIList(X) r21: mark(cons(X1,X2)) -> cons(mark(X1),X2) r22: mark(|0|()) -> |0|() r23: mark(tt()) -> tt() r24: mark(s(X)) -> s(mark(X)) r25: mark(nil()) -> nil() r26: a__zeros() -> zeros() r27: a__U11(X1,X2) -> U11(X1,X2) r28: a__length(X) -> length(X) r29: a__and(X1,X2) -> and(X1,X2) r30: a__isNat(X) -> isNat(X) r31: a__isNatList(X) -> isNatList(X) r32: a__isNatIList(X) -> isNatIList(X) The estimated dependency graph contains the following SCCs: {p1, p2, p3, p4, p5, p6, p7, p8, p9, p10, p11, p12, p13, p15, p16, p17, p18, p19, p20, p21, p22, p23, p24, p25} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: a__U11#(tt(),L) -> a__length#(mark(L)) p2: a__length#(cons(N,L)) -> a__isNatList#(L) p3: a__isNatList#(cons(V1,V2)) -> a__isNat#(V1) p4: a__isNat#(s(V1)) -> a__isNat#(V1) p5: a__isNat#(length(V1)) -> a__isNatList#(V1) p6: a__isNatList#(cons(V1,V2)) -> a__and#(a__isNat(V1),isNatList(V2)) p7: a__and#(tt(),X) -> mark#(X) p8: mark#(s(X)) -> mark#(X) p9: mark#(cons(X1,X2)) -> mark#(X1) p10: mark#(isNatIList(X)) -> a__isNatIList#(X) p11: a__isNatIList#(cons(V1,V2)) -> a__isNat#(V1) p12: a__isNatIList#(cons(V1,V2)) -> a__and#(a__isNat(V1),isNatIList(V2)) p13: a__isNatIList#(V) -> a__isNatList#(V) p14: mark#(isNatList(X)) -> a__isNatList#(X) p15: mark#(isNat(X)) -> a__isNat#(X) p16: mark#(and(X1,X2)) -> mark#(X1) p17: mark#(and(X1,X2)) -> a__and#(mark(X1),X2) p18: mark#(length(X)) -> mark#(X) p19: mark#(length(X)) -> a__length#(mark(X)) p20: a__length#(cons(N,L)) -> a__and#(a__isNatList(L),isNat(N)) p21: a__length#(cons(N,L)) -> a__U11#(a__and(a__isNatList(L),isNat(N)),L) p22: a__U11#(tt(),L) -> mark#(L) p23: mark#(U11(X1,X2)) -> mark#(X1) p24: mark#(U11(X1,X2)) -> a__U11#(mark(X1),X2) and R consists of: r1: a__zeros() -> cons(|0|(),zeros()) r2: a__U11(tt(),L) -> s(a__length(mark(L))) r3: a__and(tt(),X) -> mark(X) r4: a__isNat(|0|()) -> tt() r5: a__isNat(length(V1)) -> a__isNatList(V1) r6: a__isNat(s(V1)) -> a__isNat(V1) r7: a__isNatIList(V) -> a__isNatList(V) r8: a__isNatIList(zeros()) -> tt() r9: a__isNatIList(cons(V1,V2)) -> a__and(a__isNat(V1),isNatIList(V2)) r10: a__isNatList(nil()) -> tt() r11: a__isNatList(cons(V1,V2)) -> a__and(a__isNat(V1),isNatList(V2)) r12: a__length(nil()) -> |0|() r13: a__length(cons(N,L)) -> a__U11(a__and(a__isNatList(L),isNat(N)),L) r14: mark(zeros()) -> a__zeros() r15: mark(U11(X1,X2)) -> a__U11(mark(X1),X2) r16: mark(length(X)) -> a__length(mark(X)) r17: mark(and(X1,X2)) -> a__and(mark(X1),X2) r18: mark(isNat(X)) -> a__isNat(X) r19: mark(isNatList(X)) -> a__isNatList(X) r20: mark(isNatIList(X)) -> a__isNatIList(X) r21: mark(cons(X1,X2)) -> cons(mark(X1),X2) r22: mark(|0|()) -> |0|() r23: mark(tt()) -> tt() r24: mark(s(X)) -> s(mark(X)) r25: mark(nil()) -> nil() r26: a__zeros() -> zeros() r27: a__U11(X1,X2) -> U11(X1,X2) r28: a__length(X) -> length(X) r29: a__and(X1,X2) -> and(X1,X2) r30: a__isNat(X) -> isNat(X) r31: a__isNatList(X) -> isNatList(X) r32: a__isNatIList(X) -> isNatIList(X) The set of usable rules consists of r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r12, r13, r14, r15, r16, r17, r18, r19, r20, r21, r22, r23, r24, r25, r26, r27, r28, r29, r30, r31, r32 Take the reduction pair: lexicographic combination of reduction pairs: 1. matrix interpretations: carrier: N^2 order: lexicographic order interpretations: a__U11#_A(x1,x2) = x1 + x2 + (0,26) tt_A() = (19,19) a__length#_A(x1) = x1 + (0,22) mark_A(x1) = x1 + (19,20) cons_A(x1,x2) = ((1,0),(1,0)) x1 + ((1,0),(1,1)) x2 + (19,17) a__isNatList#_A(x1) = ((0,0),(1,0)) x1 + (18,40) a__isNat#_A(x1) = ((0,0),(1,0)) x1 + (18,37) s_A(x1) = x1 + (0,1) length_A(x1) = x1 + (4,7) a__and#_A(x1,x2) = x2 + (18,37) a__isNat_A(x1) = ((0,0),(1,0)) x1 + (19,20) isNatList_A(x1) = ((0,0),(1,0)) x1 + (0,5) mark#_A(x1) = x1 + (18,36) isNatIList_A(x1) = ((1,0),(1,1)) x1 + (2,1) a__isNatIList#_A(x1) = ((1,0),(1,1)) x1 + (19,0) isNat_A(x1) = ((0,0),(1,0)) x1 + (0,1) and_A(x1,x2) = x1 + x2 + (0,2) a__isNatList_A(x1) = ((0,0),(1,0)) x1 + (19,9) a__and_A(x1,x2) = x1 + x2 + (0,2) U11_A(x1,x2) = x1 + x2 + (4,10) a__zeros_A() = (20,36) |0|_A() = (0,9) zeros_A() = (1,17) a__U11_A(x1,x2) = x1 + x2 + (4,10) a__length_A(x1) = x1 + (4,7) a__isNatIList_A(x1) = ((1,0),(1,1)) x1 + (20,2) nil_A() = (11,1) 2. lexicographic path order with precedence: precedence: |0| > a__isNatIList# > a__length# > a__U11# > and > a__and > mark# > mark > a__length > isNat > a__isNat > a__isNatList > isNatList > a__isNatList# > a__isNatIList > tt > s > a__zeros > zeros > a__and# > cons > a__isNat# > nil > a__U11 > U11 > isNatIList > length argument filter: pi(a__U11#) = [2] pi(tt) = [] pi(a__length#) = [1] pi(mark) = [1] pi(cons) = [2] pi(a__isNatList#) = [] pi(a__isNat#) = [] pi(s) = [] pi(length) = [] pi(a__and#) = [] pi(a__isNat) = [] pi(isNatList) = [] pi(mark#) = [] pi(isNatIList) = 1 pi(a__isNatIList#) = [1] pi(isNat) = [] pi(and) = 2 pi(a__isNatList) = [] pi(a__and) = 2 pi(U11) = 1 pi(a__zeros) = [] pi(|0|) = [] pi(zeros) = [] pi(a__U11) = 1 pi(a__length) = [] pi(a__isNatIList) = [1] pi(nil) = [] The next rules are strictly ordered: p1, p2, p3, p5, p6, p7, p8, p9, p10, p11, p12, p13, p14, p15, p16, p17, p18, p19, p20, p21, p22, p23, p24 We remove them from the problem. -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: a__isNat#(s(V1)) -> a__isNat#(V1) and R consists of: r1: a__zeros() -> cons(|0|(),zeros()) r2: a__U11(tt(),L) -> s(a__length(mark(L))) r3: a__and(tt(),X) -> mark(X) r4: a__isNat(|0|()) -> tt() r5: a__isNat(length(V1)) -> a__isNatList(V1) r6: a__isNat(s(V1)) -> a__isNat(V1) r7: a__isNatIList(V) -> a__isNatList(V) r8: a__isNatIList(zeros()) -> tt() r9: a__isNatIList(cons(V1,V2)) -> a__and(a__isNat(V1),isNatIList(V2)) r10: a__isNatList(nil()) -> tt() r11: a__isNatList(cons(V1,V2)) -> a__and(a__isNat(V1),isNatList(V2)) r12: a__length(nil()) -> |0|() r13: a__length(cons(N,L)) -> a__U11(a__and(a__isNatList(L),isNat(N)),L) r14: mark(zeros()) -> a__zeros() r15: mark(U11(X1,X2)) -> a__U11(mark(X1),X2) r16: mark(length(X)) -> a__length(mark(X)) r17: mark(and(X1,X2)) -> a__and(mark(X1),X2) r18: mark(isNat(X)) -> a__isNat(X) r19: mark(isNatList(X)) -> a__isNatList(X) r20: mark(isNatIList(X)) -> a__isNatIList(X) r21: mark(cons(X1,X2)) -> cons(mark(X1),X2) r22: mark(|0|()) -> |0|() r23: mark(tt()) -> tt() r24: mark(s(X)) -> s(mark(X)) r25: mark(nil()) -> nil() r26: a__zeros() -> zeros() r27: a__U11(X1,X2) -> U11(X1,X2) r28: a__length(X) -> length(X) r29: a__and(X1,X2) -> and(X1,X2) r30: a__isNat(X) -> isNat(X) r31: a__isNatList(X) -> isNatList(X) r32: a__isNatIList(X) -> isNatIList(X) The estimated dependency graph contains the following SCCs: {p1} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: a__isNat#(s(V1)) -> a__isNat#(V1) and R consists of: r1: a__zeros() -> cons(|0|(),zeros()) r2: a__U11(tt(),L) -> s(a__length(mark(L))) r3: a__and(tt(),X) -> mark(X) r4: a__isNat(|0|()) -> tt() r5: a__isNat(length(V1)) -> a__isNatList(V1) r6: a__isNat(s(V1)) -> a__isNat(V1) r7: a__isNatIList(V) -> a__isNatList(V) r8: a__isNatIList(zeros()) -> tt() r9: a__isNatIList(cons(V1,V2)) -> a__and(a__isNat(V1),isNatIList(V2)) r10: a__isNatList(nil()) -> tt() r11: a__isNatList(cons(V1,V2)) -> a__and(a__isNat(V1),isNatList(V2)) r12: a__length(nil()) -> |0|() r13: a__length(cons(N,L)) -> a__U11(a__and(a__isNatList(L),isNat(N)),L) r14: mark(zeros()) -> a__zeros() r15: mark(U11(X1,X2)) -> a__U11(mark(X1),X2) r16: mark(length(X)) -> a__length(mark(X)) r17: mark(and(X1,X2)) -> a__and(mark(X1),X2) r18: mark(isNat(X)) -> a__isNat(X) r19: mark(isNatList(X)) -> a__isNatList(X) r20: mark(isNatIList(X)) -> a__isNatIList(X) r21: mark(cons(X1,X2)) -> cons(mark(X1),X2) r22: mark(|0|()) -> |0|() r23: mark(tt()) -> tt() r24: mark(s(X)) -> s(mark(X)) r25: mark(nil()) -> nil() r26: a__zeros() -> zeros() r27: a__U11(X1,X2) -> U11(X1,X2) r28: a__length(X) -> length(X) r29: a__and(X1,X2) -> and(X1,X2) r30: a__isNat(X) -> isNat(X) r31: a__isNatList(X) -> isNatList(X) r32: a__isNatIList(X) -> isNatIList(X) The set of usable rules consists of (no rules) Take the monotone reduction pair: lexicographic combination of reduction pairs: 1. matrix interpretations: carrier: N^2 order: lexicographic order interpretations: a__isNat#_A(x1) = ((1,0),(1,1)) x1 s_A(x1) = ((1,0),(1,1)) x1 + (1,1) 2. lexicographic path order with precedence: precedence: s > a__isNat# argument filter: pi(a__isNat#) = 1 pi(s) = [1] The next rules are strictly ordered: p1 r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r12, r13, r14, r15, r16, r17, r18, r19, r20, r21, r22, r23, r24, r25, r26, r27, r28, r29, r30, r31, r32 We remove them from the problem. Then no dependency pair remains.