YES We show the termination of the TRS R: a__U11(tt(),V1,V2) -> a__U12(a__isNat(V1),V2) a__U12(tt(),V2) -> a__U13(a__isNat(V2)) a__U13(tt()) -> tt() a__U21(tt(),V1) -> a__U22(a__isNat(V1)) a__U22(tt()) -> tt() a__U31(tt(),N) -> mark(N) a__U41(tt(),M,N) -> s(a__plus(mark(N),mark(M))) a__and(tt(),X) -> mark(X) a__isNat(|0|()) -> tt() a__isNat(plus(V1,V2)) -> a__U11(a__and(a__isNatKind(V1),isNatKind(V2)),V1,V2) a__isNat(s(V1)) -> a__U21(a__isNatKind(V1),V1) a__isNatKind(|0|()) -> tt() a__isNatKind(plus(V1,V2)) -> a__and(a__isNatKind(V1),isNatKind(V2)) a__isNatKind(s(V1)) -> a__isNatKind(V1) a__plus(N,|0|()) -> a__U31(a__and(a__isNat(N),isNatKind(N)),N) a__plus(N,s(M)) -> a__U41(a__and(a__and(a__isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N) mark(U11(X1,X2,X3)) -> a__U11(mark(X1),X2,X3) mark(U12(X1,X2)) -> a__U12(mark(X1),X2) mark(isNat(X)) -> a__isNat(X) mark(U13(X)) -> a__U13(mark(X)) mark(U21(X1,X2)) -> a__U21(mark(X1),X2) mark(U22(X)) -> a__U22(mark(X)) mark(U31(X1,X2)) -> a__U31(mark(X1),X2) mark(U41(X1,X2,X3)) -> a__U41(mark(X1),X2,X3) mark(plus(X1,X2)) -> a__plus(mark(X1),mark(X2)) mark(and(X1,X2)) -> a__and(mark(X1),X2) mark(isNatKind(X)) -> a__isNatKind(X) mark(tt()) -> tt() mark(s(X)) -> s(mark(X)) mark(|0|()) -> |0|() a__U11(X1,X2,X3) -> U11(X1,X2,X3) a__U12(X1,X2) -> U12(X1,X2) a__isNat(X) -> isNat(X) a__U13(X) -> U13(X) a__U21(X1,X2) -> U21(X1,X2) a__U22(X) -> U22(X) a__U31(X1,X2) -> U31(X1,X2) a__U41(X1,X2,X3) -> U41(X1,X2,X3) a__plus(X1,X2) -> plus(X1,X2) a__and(X1,X2) -> and(X1,X2) a__isNatKind(X) -> isNatKind(X) -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: a__U11#(tt(),V1,V2) -> a__U12#(a__isNat(V1),V2) p2: a__U11#(tt(),V1,V2) -> a__isNat#(V1) p3: a__U12#(tt(),V2) -> a__U13#(a__isNat(V2)) p4: a__U12#(tt(),V2) -> a__isNat#(V2) p5: a__U21#(tt(),V1) -> a__U22#(a__isNat(V1)) p6: a__U21#(tt(),V1) -> a__isNat#(V1) p7: a__U31#(tt(),N) -> mark#(N) p8: a__U41#(tt(),M,N) -> a__plus#(mark(N),mark(M)) p9: a__U41#(tt(),M,N) -> mark#(N) p10: a__U41#(tt(),M,N) -> mark#(M) p11: a__and#(tt(),X) -> mark#(X) p12: a__isNat#(plus(V1,V2)) -> a__U11#(a__and(a__isNatKind(V1),isNatKind(V2)),V1,V2) p13: a__isNat#(plus(V1,V2)) -> a__and#(a__isNatKind(V1),isNatKind(V2)) p14: a__isNat#(plus(V1,V2)) -> a__isNatKind#(V1) p15: a__isNat#(s(V1)) -> a__U21#(a__isNatKind(V1),V1) p16: a__isNat#(s(V1)) -> a__isNatKind#(V1) p17: a__isNatKind#(plus(V1,V2)) -> a__and#(a__isNatKind(V1),isNatKind(V2)) p18: a__isNatKind#(plus(V1,V2)) -> a__isNatKind#(V1) p19: a__isNatKind#(s(V1)) -> a__isNatKind#(V1) p20: a__plus#(N,|0|()) -> a__U31#(a__and(a__isNat(N),isNatKind(N)),N) p21: a__plus#(N,|0|()) -> a__and#(a__isNat(N),isNatKind(N)) p22: a__plus#(N,|0|()) -> a__isNat#(N) p23: a__plus#(N,s(M)) -> a__U41#(a__and(a__and(a__isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N) p24: a__plus#(N,s(M)) -> a__and#(a__and(a__isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))) p25: a__plus#(N,s(M)) -> a__and#(a__isNat(M),isNatKind(M)) p26: a__plus#(N,s(M)) -> a__isNat#(M) p27: mark#(U11(X1,X2,X3)) -> a__U11#(mark(X1),X2,X3) p28: mark#(U11(X1,X2,X3)) -> mark#(X1) p29: mark#(U12(X1,X2)) -> a__U12#(mark(X1),X2) p30: mark#(U12(X1,X2)) -> mark#(X1) p31: mark#(isNat(X)) -> a__isNat#(X) p32: mark#(U13(X)) -> a__U13#(mark(X)) p33: mark#(U13(X)) -> mark#(X) p34: mark#(U21(X1,X2)) -> a__U21#(mark(X1),X2) p35: mark#(U21(X1,X2)) -> mark#(X1) p36: mark#(U22(X)) -> a__U22#(mark(X)) p37: mark#(U22(X)) -> mark#(X) p38: mark#(U31(X1,X2)) -> a__U31#(mark(X1),X2) p39: mark#(U31(X1,X2)) -> mark#(X1) p40: mark#(U41(X1,X2,X3)) -> a__U41#(mark(X1),X2,X3) p41: mark#(U41(X1,X2,X3)) -> mark#(X1) p42: mark#(plus(X1,X2)) -> a__plus#(mark(X1),mark(X2)) p43: mark#(plus(X1,X2)) -> mark#(X1) p44: mark#(plus(X1,X2)) -> mark#(X2) p45: mark#(and(X1,X2)) -> a__and#(mark(X1),X2) p46: mark#(and(X1,X2)) -> mark#(X1) p47: mark#(isNatKind(X)) -> a__isNatKind#(X) p48: mark#(s(X)) -> mark#(X) and R consists of: r1: a__U11(tt(),V1,V2) -> a__U12(a__isNat(V1),V2) r2: a__U12(tt(),V2) -> a__U13(a__isNat(V2)) r3: a__U13(tt()) -> tt() r4: a__U21(tt(),V1) -> a__U22(a__isNat(V1)) r5: a__U22(tt()) -> tt() r6: a__U31(tt(),N) -> mark(N) r7: a__U41(tt(),M,N) -> s(a__plus(mark(N),mark(M))) r8: a__and(tt(),X) -> mark(X) r9: a__isNat(|0|()) -> tt() r10: a__isNat(plus(V1,V2)) -> a__U11(a__and(a__isNatKind(V1),isNatKind(V2)),V1,V2) r11: a__isNat(s(V1)) -> a__U21(a__isNatKind(V1),V1) r12: a__isNatKind(|0|()) -> tt() r13: a__isNatKind(plus(V1,V2)) -> a__and(a__isNatKind(V1),isNatKind(V2)) r14: a__isNatKind(s(V1)) -> a__isNatKind(V1) r15: a__plus(N,|0|()) -> a__U31(a__and(a__isNat(N),isNatKind(N)),N) r16: a__plus(N,s(M)) -> a__U41(a__and(a__and(a__isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N) r17: mark(U11(X1,X2,X3)) -> a__U11(mark(X1),X2,X3) r18: mark(U12(X1,X2)) -> a__U12(mark(X1),X2) r19: mark(isNat(X)) -> a__isNat(X) r20: mark(U13(X)) -> a__U13(mark(X)) r21: mark(U21(X1,X2)) -> a__U21(mark(X1),X2) r22: mark(U22(X)) -> a__U22(mark(X)) r23: mark(U31(X1,X2)) -> a__U31(mark(X1),X2) r24: mark(U41(X1,X2,X3)) -> a__U41(mark(X1),X2,X3) r25: mark(plus(X1,X2)) -> a__plus(mark(X1),mark(X2)) r26: mark(and(X1,X2)) -> a__and(mark(X1),X2) r27: mark(isNatKind(X)) -> a__isNatKind(X) r28: mark(tt()) -> tt() r29: mark(s(X)) -> s(mark(X)) r30: mark(|0|()) -> |0|() r31: a__U11(X1,X2,X3) -> U11(X1,X2,X3) r32: a__U12(X1,X2) -> U12(X1,X2) r33: a__isNat(X) -> isNat(X) r34: a__U13(X) -> U13(X) r35: a__U21(X1,X2) -> U21(X1,X2) r36: a__U22(X) -> U22(X) r37: a__U31(X1,X2) -> U31(X1,X2) r38: a__U41(X1,X2,X3) -> U41(X1,X2,X3) r39: a__plus(X1,X2) -> plus(X1,X2) r40: a__and(X1,X2) -> and(X1,X2) r41: a__isNatKind(X) -> isNatKind(X) The estimated dependency graph contains the following SCCs: {p1, p2, p4, p6, p7, p8, p9, p10, p11, p12, p13, p14, p15, p16, p17, p18, p19, p20, p21, p22, p23, p24, p25, p26, p27, p28, p29, p30, p31, p33, p34, p35, p37, p38, p39, p40, p41, p42, p43, p44, p45, p46, p47, p48} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: a__U11#(tt(),V1,V2) -> a__U12#(a__isNat(V1),V2) p2: a__U12#(tt(),V2) -> a__isNat#(V2) p3: a__isNat#(s(V1)) -> a__isNatKind#(V1) p4: a__isNatKind#(s(V1)) -> a__isNatKind#(V1) p5: a__isNatKind#(plus(V1,V2)) -> a__isNatKind#(V1) p6: a__isNatKind#(plus(V1,V2)) -> a__and#(a__isNatKind(V1),isNatKind(V2)) p7: a__and#(tt(),X) -> mark#(X) p8: mark#(s(X)) -> mark#(X) p9: mark#(isNatKind(X)) -> a__isNatKind#(X) p10: mark#(and(X1,X2)) -> mark#(X1) p11: mark#(and(X1,X2)) -> a__and#(mark(X1),X2) p12: mark#(plus(X1,X2)) -> mark#(X2) p13: mark#(plus(X1,X2)) -> mark#(X1) p14: mark#(plus(X1,X2)) -> a__plus#(mark(X1),mark(X2)) p15: a__plus#(N,s(M)) -> a__isNat#(M) p16: a__isNat#(s(V1)) -> a__U21#(a__isNatKind(V1),V1) p17: a__U21#(tt(),V1) -> a__isNat#(V1) p18: a__isNat#(plus(V1,V2)) -> a__isNatKind#(V1) p19: a__isNat#(plus(V1,V2)) -> a__and#(a__isNatKind(V1),isNatKind(V2)) p20: a__isNat#(plus(V1,V2)) -> a__U11#(a__and(a__isNatKind(V1),isNatKind(V2)),V1,V2) p21: a__U11#(tt(),V1,V2) -> a__isNat#(V1) p22: a__plus#(N,s(M)) -> a__and#(a__isNat(M),isNatKind(M)) p23: a__plus#(N,s(M)) -> a__and#(a__and(a__isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))) p24: a__plus#(N,s(M)) -> a__U41#(a__and(a__and(a__isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N) p25: a__U41#(tt(),M,N) -> mark#(M) p26: mark#(U41(X1,X2,X3)) -> mark#(X1) p27: mark#(U41(X1,X2,X3)) -> a__U41#(mark(X1),X2,X3) p28: a__U41#(tt(),M,N) -> mark#(N) p29: mark#(U31(X1,X2)) -> mark#(X1) p30: mark#(U31(X1,X2)) -> a__U31#(mark(X1),X2) p31: a__U31#(tt(),N) -> mark#(N) p32: mark#(U22(X)) -> mark#(X) p33: mark#(U21(X1,X2)) -> mark#(X1) p34: mark#(U21(X1,X2)) -> a__U21#(mark(X1),X2) p35: mark#(U13(X)) -> mark#(X) p36: mark#(isNat(X)) -> a__isNat#(X) p37: mark#(U12(X1,X2)) -> mark#(X1) p38: mark#(U12(X1,X2)) -> a__U12#(mark(X1),X2) p39: mark#(U11(X1,X2,X3)) -> mark#(X1) p40: mark#(U11(X1,X2,X3)) -> a__U11#(mark(X1),X2,X3) p41: a__U41#(tt(),M,N) -> a__plus#(mark(N),mark(M)) p42: a__plus#(N,|0|()) -> a__isNat#(N) p43: a__plus#(N,|0|()) -> a__and#(a__isNat(N),isNatKind(N)) p44: a__plus#(N,|0|()) -> a__U31#(a__and(a__isNat(N),isNatKind(N)),N) and R consists of: r1: a__U11(tt(),V1,V2) -> a__U12(a__isNat(V1),V2) r2: a__U12(tt(),V2) -> a__U13(a__isNat(V2)) r3: a__U13(tt()) -> tt() r4: a__U21(tt(),V1) -> a__U22(a__isNat(V1)) r5: a__U22(tt()) -> tt() r6: a__U31(tt(),N) -> mark(N) r7: a__U41(tt(),M,N) -> s(a__plus(mark(N),mark(M))) r8: a__and(tt(),X) -> mark(X) r9: a__isNat(|0|()) -> tt() r10: a__isNat(plus(V1,V2)) -> a__U11(a__and(a__isNatKind(V1),isNatKind(V2)),V1,V2) r11: a__isNat(s(V1)) -> a__U21(a__isNatKind(V1),V1) r12: a__isNatKind(|0|()) -> tt() r13: a__isNatKind(plus(V1,V2)) -> a__and(a__isNatKind(V1),isNatKind(V2)) r14: a__isNatKind(s(V1)) -> a__isNatKind(V1) r15: a__plus(N,|0|()) -> a__U31(a__and(a__isNat(N),isNatKind(N)),N) r16: a__plus(N,s(M)) -> a__U41(a__and(a__and(a__isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N) r17: mark(U11(X1,X2,X3)) -> a__U11(mark(X1),X2,X3) r18: mark(U12(X1,X2)) -> a__U12(mark(X1),X2) r19: mark(isNat(X)) -> a__isNat(X) r20: mark(U13(X)) -> a__U13(mark(X)) r21: mark(U21(X1,X2)) -> a__U21(mark(X1),X2) r22: mark(U22(X)) -> a__U22(mark(X)) r23: mark(U31(X1,X2)) -> a__U31(mark(X1),X2) r24: mark(U41(X1,X2,X3)) -> a__U41(mark(X1),X2,X3) r25: mark(plus(X1,X2)) -> a__plus(mark(X1),mark(X2)) r26: mark(and(X1,X2)) -> a__and(mark(X1),X2) r27: mark(isNatKind(X)) -> a__isNatKind(X) r28: mark(tt()) -> tt() r29: mark(s(X)) -> s(mark(X)) r30: mark(|0|()) -> |0|() r31: a__U11(X1,X2,X3) -> U11(X1,X2,X3) r32: a__U12(X1,X2) -> U12(X1,X2) r33: a__isNat(X) -> isNat(X) r34: a__U13(X) -> U13(X) r35: a__U21(X1,X2) -> U21(X1,X2) r36: a__U22(X) -> U22(X) r37: a__U31(X1,X2) -> U31(X1,X2) r38: a__U41(X1,X2,X3) -> U41(X1,X2,X3) r39: a__plus(X1,X2) -> plus(X1,X2) r40: a__and(X1,X2) -> and(X1,X2) r41: a__isNatKind(X) -> isNatKind(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, r33, r34, r35, r36, r37, r38, r39, r40, r41 Take the reduction pair: lexicographic combination of reduction pairs: 1. weighted path order base order: matrix interpretations: carrier: N^2 order: lexicographic order interpretations: a__U11#_A(x1,x2,x3) = (8,6) tt_A() = (0,0) a__U12#_A(x1,x2) = (8,6) a__isNat_A(x1) = ((0,0),(1,0)) x1 a__isNat#_A(x1) = (8,6) s_A(x1) = ((1,0),(0,0)) x1 + (0,2) a__isNatKind#_A(x1) = (8,6) plus_A(x1,x2) = ((1,0),(1,0)) x1 + x2 + (7,12) a__and#_A(x1,x2) = ((0,0),(1,0)) x2 + (8,6) a__isNatKind_A(x1) = ((0,0),(1,0)) x1 + (0,5) isNatKind_A(x1) = ((0,0),(1,0)) x1 + (0,1) mark#_A(x1) = ((0,0),(1,0)) x1 + (8,6) and_A(x1,x2) = ((1,0),(0,0)) x1 + x2 + (0,2) mark_A(x1) = x1 + (0,7) a__plus#_A(x1,x2) = ((0,0),(1,0)) x1 + ((0,0),(1,0)) x2 + (8,12) a__U21#_A(x1,x2) = (8,6) a__and_A(x1,x2) = ((1,0),(0,0)) x1 + x2 + (0,7) isNat_A(x1) = ((0,0),(1,0)) x1 a__U41#_A(x1,x2,x3) = ((0,0),(1,0)) x2 + ((0,0),(1,0)) x3 + (8,12) U41_A(x1,x2,x3) = ((1,0),(1,1)) x1 + ((1,0),(0,0)) x2 + ((1,0),(0,0)) x3 + (7,3) U31_A(x1,x2) = ((1,0),(0,0)) x1 + ((1,0),(1,0)) x2 + (10,1) a__U31#_A(x1,x2) = ((0,0),(1,0)) x2 + (8,7) U22_A(x1) = ((1,0),(0,0)) x1 U21_A(x1,x2) = ((1,0),(0,0)) x1 + ((0,0),(1,0)) x2 U13_A(x1) = ((1,0),(0,0)) x1 U12_A(x1,x2) = ((1,0),(0,0)) x1 U11_A(x1,x2,x3) = ((1,0),(0,0)) x1 |0|_A() = (9,6) a__U11_A(x1,x2,x3) = ((1,0),(0,0)) x1 a__U12_A(x1,x2) = ((1,0),(0,0)) x1 a__U13_A(x1) = ((1,0),(0,0)) x1 a__U21_A(x1,x2) = ((1,0),(0,0)) x1 + ((0,0),(1,0)) x2 a__U22_A(x1) = ((1,0),(0,0)) x1 a__U31_A(x1,x2) = ((1,0),(0,0)) x1 + ((1,0),(1,0)) x2 + (10,1) a__U41_A(x1,x2,x3) = ((1,0),(1,1)) x1 + ((1,0),(0,0)) x2 + ((1,0),(0,0)) x3 + (7,3) a__plus_A(x1,x2) = ((1,0),(1,0)) x1 + x2 + (7,12) precedence: a__plus# = a__U41# > a__U31# > a__U11# = a__U12# = a__isNat# = a__isNatKind# = a__and# = mark# = a__U21# = |0| > a__isNatKind > isNatKind > a__and > and > s = mark = a__U11 = a__plus > a__isNat > isNat > plus > U21 = a__U21 > U22 = a__U22 > U41 = U31 = U12 = a__U12 = a__U31 = a__U41 > a__U13 > tt > U13 = U11 partial status: pi(a__U11#) = [] pi(tt) = [] pi(a__U12#) = [] pi(a__isNat) = [] pi(a__isNat#) = [] pi(s) = [] pi(a__isNatKind#) = [] pi(plus) = [2] pi(a__and#) = [] pi(a__isNatKind) = [] pi(isNatKind) = [] pi(mark#) = [] pi(and) = [2] pi(mark) = [1] pi(a__plus#) = [] pi(a__U21#) = [] pi(a__and) = [] pi(isNat) = [] pi(a__U41#) = [] pi(U41) = [] pi(U31) = [] pi(a__U31#) = [] pi(U22) = [] pi(U21) = [] pi(U13) = [] pi(U12) = [] pi(U11) = [] pi(|0|) = [] pi(a__U11) = [] pi(a__U12) = [] pi(a__U13) = [] pi(a__U21) = [] pi(a__U22) = [] pi(a__U31) = [] pi(a__U41) = [1] pi(a__plus) = [] 2. weighted path order base order: matrix interpretations: carrier: N^2 order: lexicographic order interpretations: a__U11#_A(x1,x2,x3) = (4,16) tt_A() = (9,3) a__U12#_A(x1,x2) = (4,16) a__isNat_A(x1) = (17,0) a__isNat#_A(x1) = (4,16) s_A(x1) = (6,2) a__isNatKind#_A(x1) = (4,16) plus_A(x1,x2) = (8,15) a__and#_A(x1,x2) = (4,16) a__isNatKind_A(x1) = (8,14) isNatKind_A(x1) = (1,0) mark#_A(x1) = (4,16) and_A(x1,x2) = (8,1) mark_A(x1) = ((1,0),(1,1)) x1 + (8,5) a__plus#_A(x1,x2) = (5,17) a__U21#_A(x1,x2) = (4,16) a__and_A(x1,x2) = (8,14) isNat_A(x1) = (17,0) a__U41#_A(x1,x2,x3) = (5,17) U41_A(x1,x2,x3) = (1,4) U31_A(x1,x2) = (16,28) a__U31#_A(x1,x2) = (5,1) U22_A(x1) = (2,1) U21_A(x1,x2) = (3,4) U13_A(x1) = (2,6) U12_A(x1,x2) = (5,17) U11_A(x1,x2,x3) = (10,0) |0|_A() = (17,1) a__U11_A(x1,x2,x3) = (17,0) a__U12_A(x1,x2) = (11,28) a__U13_A(x1) = (10,7) a__U21_A(x1,x2) = (10,5) a__U22_A(x1) = (9,4) a__U31_A(x1,x2) = (16,28) a__U41_A(x1,x2,x3) = (7,3) a__plus_A(x1,x2) = (16,28) precedence: U22 > U21 = a__U21 > a__plus# = a__U41# > a__U11# = a__U12# = a__isNat# = a__isNatKind# = a__and# = mark# = a__U21# = a__U31# > a__isNatKind = mark = a__and = U31 = |0| = a__U13 = a__U31 = a__plus > a__U22 > tt = a__isNat = a__U11 > a__U12 > U41 = U12 > and = isNat = U13 = U11 > s = plus = isNatKind = a__U41 partial status: pi(a__U11#) = [] pi(tt) = [] pi(a__U12#) = [] pi(a__isNat) = [] pi(a__isNat#) = [] pi(s) = [] pi(a__isNatKind#) = [] pi(plus) = [] pi(a__and#) = [] pi(a__isNatKind) = [] pi(isNatKind) = [] pi(mark#) = [] pi(and) = [] pi(mark) = [1] pi(a__plus#) = [] pi(a__U21#) = [] pi(a__and) = [] pi(isNat) = [] pi(a__U41#) = [] pi(U41) = [] pi(U31) = [] pi(a__U31#) = [] pi(U22) = [] pi(U21) = [] pi(U13) = [] pi(U12) = [] pi(U11) = [] pi(|0|) = [] pi(a__U11) = [] pi(a__U12) = [] pi(a__U13) = [] pi(a__U21) = [] pi(a__U22) = [] pi(a__U31) = [] pi(a__U41) = [] pi(a__plus) = [] The next rules are strictly ordered: p14, p27, p28, p30, p31, p44 We remove them from the problem. -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: a__U11#(tt(),V1,V2) -> a__U12#(a__isNat(V1),V2) p2: a__U12#(tt(),V2) -> a__isNat#(V2) p3: a__isNat#(s(V1)) -> a__isNatKind#(V1) p4: a__isNatKind#(s(V1)) -> a__isNatKind#(V1) p5: a__isNatKind#(plus(V1,V2)) -> a__isNatKind#(V1) p6: a__isNatKind#(plus(V1,V2)) -> a__and#(a__isNatKind(V1),isNatKind(V2)) p7: a__and#(tt(),X) -> mark#(X) p8: mark#(s(X)) -> mark#(X) p9: mark#(isNatKind(X)) -> a__isNatKind#(X) p10: mark#(and(X1,X2)) -> mark#(X1) p11: mark#(and(X1,X2)) -> a__and#(mark(X1),X2) p12: mark#(plus(X1,X2)) -> mark#(X2) p13: mark#(plus(X1,X2)) -> mark#(X1) p14: a__plus#(N,s(M)) -> a__isNat#(M) p15: a__isNat#(s(V1)) -> a__U21#(a__isNatKind(V1),V1) p16: a__U21#(tt(),V1) -> a__isNat#(V1) p17: a__isNat#(plus(V1,V2)) -> a__isNatKind#(V1) p18: a__isNat#(plus(V1,V2)) -> a__and#(a__isNatKind(V1),isNatKind(V2)) p19: a__isNat#(plus(V1,V2)) -> a__U11#(a__and(a__isNatKind(V1),isNatKind(V2)),V1,V2) p20: a__U11#(tt(),V1,V2) -> a__isNat#(V1) p21: a__plus#(N,s(M)) -> a__and#(a__isNat(M),isNatKind(M)) p22: a__plus#(N,s(M)) -> a__and#(a__and(a__isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))) p23: a__plus#(N,s(M)) -> a__U41#(a__and(a__and(a__isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N) p24: a__U41#(tt(),M,N) -> mark#(M) p25: mark#(U41(X1,X2,X3)) -> mark#(X1) p26: mark#(U31(X1,X2)) -> mark#(X1) p27: mark#(U22(X)) -> mark#(X) p28: mark#(U21(X1,X2)) -> mark#(X1) p29: mark#(U21(X1,X2)) -> a__U21#(mark(X1),X2) p30: mark#(U13(X)) -> mark#(X) p31: mark#(isNat(X)) -> a__isNat#(X) p32: mark#(U12(X1,X2)) -> mark#(X1) p33: mark#(U12(X1,X2)) -> a__U12#(mark(X1),X2) p34: mark#(U11(X1,X2,X3)) -> mark#(X1) p35: mark#(U11(X1,X2,X3)) -> a__U11#(mark(X1),X2,X3) p36: a__U41#(tt(),M,N) -> a__plus#(mark(N),mark(M)) p37: a__plus#(N,|0|()) -> a__isNat#(N) p38: a__plus#(N,|0|()) -> a__and#(a__isNat(N),isNatKind(N)) and R consists of: r1: a__U11(tt(),V1,V2) -> a__U12(a__isNat(V1),V2) r2: a__U12(tt(),V2) -> a__U13(a__isNat(V2)) r3: a__U13(tt()) -> tt() r4: a__U21(tt(),V1) -> a__U22(a__isNat(V1)) r5: a__U22(tt()) -> tt() r6: a__U31(tt(),N) -> mark(N) r7: a__U41(tt(),M,N) -> s(a__plus(mark(N),mark(M))) r8: a__and(tt(),X) -> mark(X) r9: a__isNat(|0|()) -> tt() r10: a__isNat(plus(V1,V2)) -> a__U11(a__and(a__isNatKind(V1),isNatKind(V2)),V1,V2) r11: a__isNat(s(V1)) -> a__U21(a__isNatKind(V1),V1) r12: a__isNatKind(|0|()) -> tt() r13: a__isNatKind(plus(V1,V2)) -> a__and(a__isNatKind(V1),isNatKind(V2)) r14: a__isNatKind(s(V1)) -> a__isNatKind(V1) r15: a__plus(N,|0|()) -> a__U31(a__and(a__isNat(N),isNatKind(N)),N) r16: a__plus(N,s(M)) -> a__U41(a__and(a__and(a__isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N) r17: mark(U11(X1,X2,X3)) -> a__U11(mark(X1),X2,X3) r18: mark(U12(X1,X2)) -> a__U12(mark(X1),X2) r19: mark(isNat(X)) -> a__isNat(X) r20: mark(U13(X)) -> a__U13(mark(X)) r21: mark(U21(X1,X2)) -> a__U21(mark(X1),X2) r22: mark(U22(X)) -> a__U22(mark(X)) r23: mark(U31(X1,X2)) -> a__U31(mark(X1),X2) r24: mark(U41(X1,X2,X3)) -> a__U41(mark(X1),X2,X3) r25: mark(plus(X1,X2)) -> a__plus(mark(X1),mark(X2)) r26: mark(and(X1,X2)) -> a__and(mark(X1),X2) r27: mark(isNatKind(X)) -> a__isNatKind(X) r28: mark(tt()) -> tt() r29: mark(s(X)) -> s(mark(X)) r30: mark(|0|()) -> |0|() r31: a__U11(X1,X2,X3) -> U11(X1,X2,X3) r32: a__U12(X1,X2) -> U12(X1,X2) r33: a__isNat(X) -> isNat(X) r34: a__U13(X) -> U13(X) r35: a__U21(X1,X2) -> U21(X1,X2) r36: a__U22(X) -> U22(X) r37: a__U31(X1,X2) -> U31(X1,X2) r38: a__U41(X1,X2,X3) -> U41(X1,X2,X3) r39: a__plus(X1,X2) -> plus(X1,X2) r40: a__and(X1,X2) -> and(X1,X2) r41: a__isNatKind(X) -> isNatKind(X) The estimated dependency graph contains the following SCCs: {p23, p36} {p1, p2, p3, p4, p5, p6, p7, p8, p9, p10, p11, p12, p13, p15, p16, p17, p18, p19, p20, p25, p26, p27, p28, p29, p30, p31, p32, p33, p34, p35} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: a__plus#(N,s(M)) -> a__U41#(a__and(a__and(a__isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N) p2: a__U41#(tt(),M,N) -> a__plus#(mark(N),mark(M)) and R consists of: r1: a__U11(tt(),V1,V2) -> a__U12(a__isNat(V1),V2) r2: a__U12(tt(),V2) -> a__U13(a__isNat(V2)) r3: a__U13(tt()) -> tt() r4: a__U21(tt(),V1) -> a__U22(a__isNat(V1)) r5: a__U22(tt()) -> tt() r6: a__U31(tt(),N) -> mark(N) r7: a__U41(tt(),M,N) -> s(a__plus(mark(N),mark(M))) r8: a__and(tt(),X) -> mark(X) r9: a__isNat(|0|()) -> tt() r10: a__isNat(plus(V1,V2)) -> a__U11(a__and(a__isNatKind(V1),isNatKind(V2)),V1,V2) r11: a__isNat(s(V1)) -> a__U21(a__isNatKind(V1),V1) r12: a__isNatKind(|0|()) -> tt() r13: a__isNatKind(plus(V1,V2)) -> a__and(a__isNatKind(V1),isNatKind(V2)) r14: a__isNatKind(s(V1)) -> a__isNatKind(V1) r15: a__plus(N,|0|()) -> a__U31(a__and(a__isNat(N),isNatKind(N)),N) r16: a__plus(N,s(M)) -> a__U41(a__and(a__and(a__isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N) r17: mark(U11(X1,X2,X3)) -> a__U11(mark(X1),X2,X3) r18: mark(U12(X1,X2)) -> a__U12(mark(X1),X2) r19: mark(isNat(X)) -> a__isNat(X) r20: mark(U13(X)) -> a__U13(mark(X)) r21: mark(U21(X1,X2)) -> a__U21(mark(X1),X2) r22: mark(U22(X)) -> a__U22(mark(X)) r23: mark(U31(X1,X2)) -> a__U31(mark(X1),X2) r24: mark(U41(X1,X2,X3)) -> a__U41(mark(X1),X2,X3) r25: mark(plus(X1,X2)) -> a__plus(mark(X1),mark(X2)) r26: mark(and(X1,X2)) -> a__and(mark(X1),X2) r27: mark(isNatKind(X)) -> a__isNatKind(X) r28: mark(tt()) -> tt() r29: mark(s(X)) -> s(mark(X)) r30: mark(|0|()) -> |0|() r31: a__U11(X1,X2,X3) -> U11(X1,X2,X3) r32: a__U12(X1,X2) -> U12(X1,X2) r33: a__isNat(X) -> isNat(X) r34: a__U13(X) -> U13(X) r35: a__U21(X1,X2) -> U21(X1,X2) r36: a__U22(X) -> U22(X) r37: a__U31(X1,X2) -> U31(X1,X2) r38: a__U41(X1,X2,X3) -> U41(X1,X2,X3) r39: a__plus(X1,X2) -> plus(X1,X2) r40: a__and(X1,X2) -> and(X1,X2) r41: a__isNatKind(X) -> isNatKind(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, r33, r34, r35, r36, r37, r38, r39, r40, r41 Take the reduction pair: lexicographic combination of reduction pairs: 1. weighted path order base order: matrix interpretations: carrier: N^2 order: lexicographic order interpretations: a__plus#_A(x1,x2) = x1 + ((1,0),(1,1)) x2 + (1,11) s_A(x1) = ((1,0),(0,0)) x1 + (6,13) a__U41#_A(x1,x2,x3) = ((1,0),(0,0)) x2 + x3 + (5,24) a__and_A(x1,x2) = x1 + ((1,0),(0,0)) x2 + (2,3) a__isNat_A(x1) = x1 + (8,26) isNatKind_A(x1) = ((1,0),(0,0)) x1 + (5,2) and_A(x1,x2) = x1 + ((1,0),(0,0)) x2 + (2,2) isNat_A(x1) = x1 + (8,12) tt_A() = (2,2) mark_A(x1) = ((1,0),(1,1)) x1 + (0,6) a__U11_A(x1,x2,x3) = ((1,0),(0,0)) x1 + (6,18) a__U12_A(x1,x2) = (3,9) a__U13_A(x1) = (2,8) a__U21_A(x1,x2) = ((0,0),(1,0)) x1 + (4,7) a__U22_A(x1) = (3,8) a__U31_A(x1,x2) = ((1,0),(0,0)) x2 + (1,2) a__U41_A(x1,x2,x3) = ((1,0),(0,0)) x2 + x3 + (16,14) a__plus_A(x1,x2) = x1 + ((1,0),(0,0)) x2 + (10,18) a__isNatKind_A(x1) = ((1,0),(0,0)) x1 + (5,13) |0|_A() = (7,1) plus_A(x1,x2) = x1 + ((1,0),(0,0)) x2 + (10,17) U11_A(x1,x2,x3) = ((1,0),(0,0)) x1 + (6,7) U12_A(x1,x2) = (3,1) U13_A(x1) = (2,7) U21_A(x1,x2) = ((0,0),(1,0)) x1 + (4,1) U22_A(x1) = (3,7) U31_A(x1,x2) = ((1,0),(0,0)) x2 + (1,1) U41_A(x1,x2,x3) = ((1,0),(0,0)) x2 + x3 + (16,1) precedence: mark = a__U21 > a__U41# > a__isNatKind > isNatKind > a__isNat > a__and > a__plus > a__U41 > s > a__plus# > a__U11 > a__U12 > a__U13 > a__U31 > a__U22 = U12 > plus > U11 > U13 = U21 > and = tt = U22 > isNat = |0| = U31 = U41 partial status: pi(a__plus#) = [1, 2] pi(s) = [] pi(a__U41#) = [3] pi(a__and) = [] pi(a__isNat) = [1] pi(isNatKind) = [] pi(and) = [] pi(isNat) = [] pi(tt) = [] pi(mark) = [] pi(a__U11) = [] pi(a__U12) = [] pi(a__U13) = [] pi(a__U21) = [] pi(a__U22) = [] pi(a__U31) = [] pi(a__U41) = [3] pi(a__plus) = [] pi(a__isNatKind) = [] pi(|0|) = [] pi(plus) = [1] pi(U11) = [] pi(U12) = [] pi(U13) = [] pi(U21) = [] pi(U22) = [] pi(U31) = [] pi(U41) = [] 2. weighted path order base order: matrix interpretations: carrier: N^2 order: lexicographic order interpretations: a__plus#_A(x1,x2) = ((1,0),(0,0)) x1 + ((1,0),(1,1)) x2 s_A(x1) = (5,7) a__U41#_A(x1,x2,x3) = x3 + (1,13) a__and_A(x1,x2) = (0,6) a__isNat_A(x1) = (4,5) isNatKind_A(x1) = (0,0) and_A(x1,x2) = (0,1) isNat_A(x1) = (0,0) tt_A() = (0,0) mark_A(x1) = (0,0) a__U11_A(x1,x2,x3) = (3,4) a__U12_A(x1,x2) = (2,3) a__U13_A(x1) = (1,2) a__U21_A(x1,x2) = (0,0) a__U22_A(x1) = (0,0) a__U31_A(x1,x2) = (1,1) a__U41_A(x1,x2,x3) = (0,0) a__plus_A(x1,x2) = (5,2) a__isNatKind_A(x1) = (0,0) |0|_A() = (0,0) plus_A(x1,x2) = (0,0) U11_A(x1,x2,x3) = (0,0) U12_A(x1,x2) = (1,4) U13_A(x1) = (0,1) U21_A(x1,x2) = (0,0) U22_A(x1) = (0,0) U31_A(x1,x2) = (0,0) U41_A(x1,x2,x3) = (0,0) precedence: U31 > a__and > mark > a__isNat = a__U41 = a__plus > isNat > |0| > and > a__U22 > U22 > a__U11 = a__U12 > s = a__U21 = a__isNatKind = U13 > a__plus# = a__U41# = isNatKind = tt = a__U13 = a__U31 = plus = U11 = U12 = U21 = U41 partial status: pi(a__plus#) = [] pi(s) = [] pi(a__U41#) = [3] pi(a__and) = [] pi(a__isNat) = [] pi(isNatKind) = [] pi(and) = [] pi(isNat) = [] pi(tt) = [] pi(mark) = [] pi(a__U11) = [] pi(a__U12) = [] pi(a__U13) = [] pi(a__U21) = [] pi(a__U22) = [] pi(a__U31) = [] pi(a__U41) = [] pi(a__plus) = [] pi(a__isNatKind) = [] pi(|0|) = [] pi(plus) = [] pi(U11) = [] pi(U12) = [] pi(U13) = [] pi(U21) = [] pi(U22) = [] pi(U31) = [] pi(U41) = [] 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: a__U41#(tt(),M,N) -> a__plus#(mark(N),mark(M)) and R consists of: r1: a__U11(tt(),V1,V2) -> a__U12(a__isNat(V1),V2) r2: a__U12(tt(),V2) -> a__U13(a__isNat(V2)) r3: a__U13(tt()) -> tt() r4: a__U21(tt(),V1) -> a__U22(a__isNat(V1)) r5: a__U22(tt()) -> tt() r6: a__U31(tt(),N) -> mark(N) r7: a__U41(tt(),M,N) -> s(a__plus(mark(N),mark(M))) r8: a__and(tt(),X) -> mark(X) r9: a__isNat(|0|()) -> tt() r10: a__isNat(plus(V1,V2)) -> a__U11(a__and(a__isNatKind(V1),isNatKind(V2)),V1,V2) r11: a__isNat(s(V1)) -> a__U21(a__isNatKind(V1),V1) r12: a__isNatKind(|0|()) -> tt() r13: a__isNatKind(plus(V1,V2)) -> a__and(a__isNatKind(V1),isNatKind(V2)) r14: a__isNatKind(s(V1)) -> a__isNatKind(V1) r15: a__plus(N,|0|()) -> a__U31(a__and(a__isNat(N),isNatKind(N)),N) r16: a__plus(N,s(M)) -> a__U41(a__and(a__and(a__isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N) r17: mark(U11(X1,X2,X3)) -> a__U11(mark(X1),X2,X3) r18: mark(U12(X1,X2)) -> a__U12(mark(X1),X2) r19: mark(isNat(X)) -> a__isNat(X) r20: mark(U13(X)) -> a__U13(mark(X)) r21: mark(U21(X1,X2)) -> a__U21(mark(X1),X2) r22: mark(U22(X)) -> a__U22(mark(X)) r23: mark(U31(X1,X2)) -> a__U31(mark(X1),X2) r24: mark(U41(X1,X2,X3)) -> a__U41(mark(X1),X2,X3) r25: mark(plus(X1,X2)) -> a__plus(mark(X1),mark(X2)) r26: mark(and(X1,X2)) -> a__and(mark(X1),X2) r27: mark(isNatKind(X)) -> a__isNatKind(X) r28: mark(tt()) -> tt() r29: mark(s(X)) -> s(mark(X)) r30: mark(|0|()) -> |0|() r31: a__U11(X1,X2,X3) -> U11(X1,X2,X3) r32: a__U12(X1,X2) -> U12(X1,X2) r33: a__isNat(X) -> isNat(X) r34: a__U13(X) -> U13(X) r35: a__U21(X1,X2) -> U21(X1,X2) r36: a__U22(X) -> U22(X) r37: a__U31(X1,X2) -> U31(X1,X2) r38: a__U41(X1,X2,X3) -> U41(X1,X2,X3) r39: a__plus(X1,X2) -> plus(X1,X2) r40: a__and(X1,X2) -> and(X1,X2) r41: a__isNatKind(X) -> isNatKind(X) The estimated dependency graph contains the following SCCs: (no SCCs) -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: a__U11#(tt(),V1,V2) -> a__U12#(a__isNat(V1),V2) p2: a__U12#(tt(),V2) -> a__isNat#(V2) p3: a__isNat#(plus(V1,V2)) -> a__U11#(a__and(a__isNatKind(V1),isNatKind(V2)),V1,V2) p4: a__U11#(tt(),V1,V2) -> a__isNat#(V1) p5: a__isNat#(plus(V1,V2)) -> a__and#(a__isNatKind(V1),isNatKind(V2)) p6: a__and#(tt(),X) -> mark#(X) p7: mark#(U11(X1,X2,X3)) -> a__U11#(mark(X1),X2,X3) p8: mark#(U11(X1,X2,X3)) -> mark#(X1) p9: mark#(U12(X1,X2)) -> a__U12#(mark(X1),X2) p10: mark#(U12(X1,X2)) -> mark#(X1) p11: mark#(isNat(X)) -> a__isNat#(X) p12: a__isNat#(plus(V1,V2)) -> a__isNatKind#(V1) p13: a__isNatKind#(plus(V1,V2)) -> a__and#(a__isNatKind(V1),isNatKind(V2)) p14: a__isNatKind#(plus(V1,V2)) -> a__isNatKind#(V1) p15: a__isNatKind#(s(V1)) -> a__isNatKind#(V1) p16: a__isNat#(s(V1)) -> a__U21#(a__isNatKind(V1),V1) p17: a__U21#(tt(),V1) -> a__isNat#(V1) p18: a__isNat#(s(V1)) -> a__isNatKind#(V1) p19: mark#(U13(X)) -> mark#(X) p20: mark#(U21(X1,X2)) -> a__U21#(mark(X1),X2) p21: mark#(U21(X1,X2)) -> mark#(X1) p22: mark#(U22(X)) -> mark#(X) p23: mark#(U31(X1,X2)) -> mark#(X1) p24: mark#(U41(X1,X2,X3)) -> mark#(X1) p25: mark#(plus(X1,X2)) -> mark#(X1) p26: mark#(plus(X1,X2)) -> mark#(X2) p27: mark#(and(X1,X2)) -> a__and#(mark(X1),X2) p28: mark#(and(X1,X2)) -> mark#(X1) p29: mark#(isNatKind(X)) -> a__isNatKind#(X) p30: mark#(s(X)) -> mark#(X) and R consists of: r1: a__U11(tt(),V1,V2) -> a__U12(a__isNat(V1),V2) r2: a__U12(tt(),V2) -> a__U13(a__isNat(V2)) r3: a__U13(tt()) -> tt() r4: a__U21(tt(),V1) -> a__U22(a__isNat(V1)) r5: a__U22(tt()) -> tt() r6: a__U31(tt(),N) -> mark(N) r7: a__U41(tt(),M,N) -> s(a__plus(mark(N),mark(M))) r8: a__and(tt(),X) -> mark(X) r9: a__isNat(|0|()) -> tt() r10: a__isNat(plus(V1,V2)) -> a__U11(a__and(a__isNatKind(V1),isNatKind(V2)),V1,V2) r11: a__isNat(s(V1)) -> a__U21(a__isNatKind(V1),V1) r12: a__isNatKind(|0|()) -> tt() r13: a__isNatKind(plus(V1,V2)) -> a__and(a__isNatKind(V1),isNatKind(V2)) r14: a__isNatKind(s(V1)) -> a__isNatKind(V1) r15: a__plus(N,|0|()) -> a__U31(a__and(a__isNat(N),isNatKind(N)),N) r16: a__plus(N,s(M)) -> a__U41(a__and(a__and(a__isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N) r17: mark(U11(X1,X2,X3)) -> a__U11(mark(X1),X2,X3) r18: mark(U12(X1,X2)) -> a__U12(mark(X1),X2) r19: mark(isNat(X)) -> a__isNat(X) r20: mark(U13(X)) -> a__U13(mark(X)) r21: mark(U21(X1,X2)) -> a__U21(mark(X1),X2) r22: mark(U22(X)) -> a__U22(mark(X)) r23: mark(U31(X1,X2)) -> a__U31(mark(X1),X2) r24: mark(U41(X1,X2,X3)) -> a__U41(mark(X1),X2,X3) r25: mark(plus(X1,X2)) -> a__plus(mark(X1),mark(X2)) r26: mark(and(X1,X2)) -> a__and(mark(X1),X2) r27: mark(isNatKind(X)) -> a__isNatKind(X) r28: mark(tt()) -> tt() r29: mark(s(X)) -> s(mark(X)) r30: mark(|0|()) -> |0|() r31: a__U11(X1,X2,X3) -> U11(X1,X2,X3) r32: a__U12(X1,X2) -> U12(X1,X2) r33: a__isNat(X) -> isNat(X) r34: a__U13(X) -> U13(X) r35: a__U21(X1,X2) -> U21(X1,X2) r36: a__U22(X) -> U22(X) r37: a__U31(X1,X2) -> U31(X1,X2) r38: a__U41(X1,X2,X3) -> U41(X1,X2,X3) r39: a__plus(X1,X2) -> plus(X1,X2) r40: a__and(X1,X2) -> and(X1,X2) r41: a__isNatKind(X) -> isNatKind(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, r33, r34, r35, r36, r37, r38, r39, r40, r41 Take the reduction pair: lexicographic combination of reduction pairs: 1. weighted path order base order: matrix interpretations: carrier: N^2 order: lexicographic order interpretations: a__U11#_A(x1,x2,x3) = (0,0) tt_A() = (0,1) a__U12#_A(x1,x2) = (0,0) a__isNat_A(x1) = (0,8) a__isNat#_A(x1) = (0,0) plus_A(x1,x2) = ((1,0),(1,1)) x1 + ((1,0),(1,0)) x2 + (9,4) a__and_A(x1,x2) = ((1,0),(0,0)) x1 + ((1,0),(1,1)) x2 + (0,8) a__isNatKind_A(x1) = ((0,0),(1,0)) x1 + (0,1) isNatKind_A(x1) = ((0,0),(1,0)) x1 + (0,1) a__and#_A(x1,x2) = ((0,0),(1,0)) x2 mark#_A(x1) = ((0,0),(1,0)) x1 U11_A(x1,x2,x3) = ((1,0),(0,0)) x1 mark_A(x1) = x1 + (0,6) U12_A(x1,x2) = ((1,0),(0,0)) x1 + (0,1) isNat_A(x1) = (0,3) a__isNatKind#_A(x1) = (0,0) s_A(x1) = ((1,0),(0,0)) x1 + (0,2) a__U21#_A(x1,x2) = (0,0) U13_A(x1) = ((1,0),(0,0)) x1 U21_A(x1,x2) = ((1,0),(1,0)) x1 + (0,1) U22_A(x1) = ((1,0),(0,0)) x1 U31_A(x1,x2) = ((1,0),(0,0)) x1 + x2 + (1,2) U41_A(x1,x2,x3) = ((1,0),(0,0)) x1 + ((1,0),(1,0)) x2 + x3 + (9,2) and_A(x1,x2) = ((1,0),(0,0)) x1 + ((1,0),(1,1)) x2 + (0,8) a__U11_A(x1,x2,x3) = ((1,0),(0,0)) x1 + (0,5) a__U12_A(x1,x2) = ((1,0),(0,0)) x1 + (0,4) a__U13_A(x1) = ((1,0),(0,0)) x1 + (0,1) a__U21_A(x1,x2) = ((1,0),(1,0)) x1 + (0,7) a__U22_A(x1) = ((1,0),(0,0)) x1 + (0,6) a__U31_A(x1,x2) = ((1,0),(0,0)) x1 + x2 + (1,3) a__U41_A(x1,x2,x3) = ((1,0),(0,0)) x1 + ((1,0),(1,0)) x2 + x3 + (9,3) a__plus_A(x1,x2) = ((1,0),(1,1)) x1 + ((1,0),(1,0)) x2 + (9,4) |0|_A() = (0,2) precedence: a__isNatKind = isNatKind > a__isNat = a__and = mark = and > a__U11 > a__U12 > U12 > a__U21 > U11 = isNat = U21 = a__U13 > a__U31 > U13 = a__plus > a__U22 = a__U41 > U41 > tt = plus > U31 = |0| > a__U11# = a__U12# = a__isNat# = a__and# = mark# = a__isNatKind# = s = a__U21# = U22 partial status: pi(a__U11#) = [] pi(tt) = [] pi(a__U12#) = [] pi(a__isNat) = [] pi(a__isNat#) = [] pi(plus) = [1] pi(a__and) = [2] pi(a__isNatKind) = [] pi(isNatKind) = [] pi(a__and#) = [] pi(mark#) = [] pi(U11) = [] pi(mark) = [1] pi(U12) = [] pi(isNat) = [] pi(a__isNatKind#) = [] pi(s) = [] pi(a__U21#) = [] pi(U13) = [] pi(U21) = [] pi(U22) = [] pi(U31) = [] pi(U41) = [] pi(and) = [2] pi(a__U11) = [] pi(a__U12) = [] pi(a__U13) = [] pi(a__U21) = [] pi(a__U22) = [] pi(a__U31) = [2] pi(a__U41) = [] pi(a__plus) = [] pi(|0|) = [] 2. weighted path order base order: matrix interpretations: carrier: N^2 order: lexicographic order interpretations: a__U11#_A(x1,x2,x3) = (3,1) tt_A() = (1,4) a__U12#_A(x1,x2) = (3,1) a__isNat_A(x1) = (5,3) a__isNat#_A(x1) = (3,1) plus_A(x1,x2) = (7,1) a__and_A(x1,x2) = (8,8) a__isNatKind_A(x1) = (9,0) isNatKind_A(x1) = (4,4) a__and#_A(x1,x2) = (3,1) mark#_A(x1) = (3,1) U11_A(x1,x2,x3) = (0,8) mark_A(x1) = (6,7) U12_A(x1,x2) = (1,2) isNat_A(x1) = (4,2) a__isNatKind#_A(x1) = (3,1) s_A(x1) = (0,1) a__U21#_A(x1,x2) = (3,1) U13_A(x1) = (2,1) U21_A(x1,x2) = (3,8) U22_A(x1) = (6,0) U31_A(x1,x2) = (4,5) U41_A(x1,x2,x3) = (1,8) and_A(x1,x2) = (3,0) a__U11_A(x1,x2,x3) = (4,6) a__U12_A(x1,x2) = (3,5) a__U13_A(x1) = (2,7) a__U21_A(x1,x2) = (4,2) a__U22_A(x1) = (6,1) a__U31_A(x1,x2) = (5,6) a__U41_A(x1,x2,x3) = (5,9) a__plus_A(x1,x2) = (9,10) |0|_A() = (0,0) precedence: |0| > a__U31 > a__isNatKind > a__and > mark > tt > s > U21 > a__U11 > a__isNat = a__U41 = a__plus > isNat > a__U12 > U41 > a__U21 > a__U11# = a__U12# = a__isNat# = plus = isNatKind = a__and# = mark# = U12 = a__isNatKind# = a__U21# = a__U13 = a__U22 > U13 > U22 = U31 > U11 = and partial status: pi(a__U11#) = [] pi(tt) = [] pi(a__U12#) = [] pi(a__isNat) = [] pi(a__isNat#) = [] pi(plus) = [] pi(a__and) = [] pi(a__isNatKind) = [] pi(isNatKind) = [] pi(a__and#) = [] pi(mark#) = [] pi(U11) = [] pi(mark) = [] pi(U12) = [] pi(isNat) = [] pi(a__isNatKind#) = [] pi(s) = [] pi(a__U21#) = [] pi(U13) = [] pi(U21) = [] pi(U22) = [] pi(U31) = [] pi(U41) = [] pi(and) = [] pi(a__U11) = [] pi(a__U12) = [] pi(a__U13) = [] pi(a__U21) = [] pi(a__U22) = [] pi(a__U31) = [] pi(a__U41) = [] pi(a__plus) = [] pi(|0|) = [] The next rules are strictly ordered: p23 We remove them from the problem. -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: a__U11#(tt(),V1,V2) -> a__U12#(a__isNat(V1),V2) p2: a__U12#(tt(),V2) -> a__isNat#(V2) p3: a__isNat#(plus(V1,V2)) -> a__U11#(a__and(a__isNatKind(V1),isNatKind(V2)),V1,V2) p4: a__U11#(tt(),V1,V2) -> a__isNat#(V1) p5: a__isNat#(plus(V1,V2)) -> a__and#(a__isNatKind(V1),isNatKind(V2)) p6: a__and#(tt(),X) -> mark#(X) p7: mark#(U11(X1,X2,X3)) -> a__U11#(mark(X1),X2,X3) p8: mark#(U11(X1,X2,X3)) -> mark#(X1) p9: mark#(U12(X1,X2)) -> a__U12#(mark(X1),X2) p10: mark#(U12(X1,X2)) -> mark#(X1) p11: mark#(isNat(X)) -> a__isNat#(X) p12: a__isNat#(plus(V1,V2)) -> a__isNatKind#(V1) p13: a__isNatKind#(plus(V1,V2)) -> a__and#(a__isNatKind(V1),isNatKind(V2)) p14: a__isNatKind#(plus(V1,V2)) -> a__isNatKind#(V1) p15: a__isNatKind#(s(V1)) -> a__isNatKind#(V1) p16: a__isNat#(s(V1)) -> a__U21#(a__isNatKind(V1),V1) p17: a__U21#(tt(),V1) -> a__isNat#(V1) p18: a__isNat#(s(V1)) -> a__isNatKind#(V1) p19: mark#(U13(X)) -> mark#(X) p20: mark#(U21(X1,X2)) -> a__U21#(mark(X1),X2) p21: mark#(U21(X1,X2)) -> mark#(X1) p22: mark#(U22(X)) -> mark#(X) p23: mark#(U41(X1,X2,X3)) -> mark#(X1) p24: mark#(plus(X1,X2)) -> mark#(X1) p25: mark#(plus(X1,X2)) -> mark#(X2) p26: mark#(and(X1,X2)) -> a__and#(mark(X1),X2) p27: mark#(and(X1,X2)) -> mark#(X1) p28: mark#(isNatKind(X)) -> a__isNatKind#(X) p29: mark#(s(X)) -> mark#(X) and R consists of: r1: a__U11(tt(),V1,V2) -> a__U12(a__isNat(V1),V2) r2: a__U12(tt(),V2) -> a__U13(a__isNat(V2)) r3: a__U13(tt()) -> tt() r4: a__U21(tt(),V1) -> a__U22(a__isNat(V1)) r5: a__U22(tt()) -> tt() r6: a__U31(tt(),N) -> mark(N) r7: a__U41(tt(),M,N) -> s(a__plus(mark(N),mark(M))) r8: a__and(tt(),X) -> mark(X) r9: a__isNat(|0|()) -> tt() r10: a__isNat(plus(V1,V2)) -> a__U11(a__and(a__isNatKind(V1),isNatKind(V2)),V1,V2) r11: a__isNat(s(V1)) -> a__U21(a__isNatKind(V1),V1) r12: a__isNatKind(|0|()) -> tt() r13: a__isNatKind(plus(V1,V2)) -> a__and(a__isNatKind(V1),isNatKind(V2)) r14: a__isNatKind(s(V1)) -> a__isNatKind(V1) r15: a__plus(N,|0|()) -> a__U31(a__and(a__isNat(N),isNatKind(N)),N) r16: a__plus(N,s(M)) -> a__U41(a__and(a__and(a__isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N) r17: mark(U11(X1,X2,X3)) -> a__U11(mark(X1),X2,X3) r18: mark(U12(X1,X2)) -> a__U12(mark(X1),X2) r19: mark(isNat(X)) -> a__isNat(X) r20: mark(U13(X)) -> a__U13(mark(X)) r21: mark(U21(X1,X2)) -> a__U21(mark(X1),X2) r22: mark(U22(X)) -> a__U22(mark(X)) r23: mark(U31(X1,X2)) -> a__U31(mark(X1),X2) r24: mark(U41(X1,X2,X3)) -> a__U41(mark(X1),X2,X3) r25: mark(plus(X1,X2)) -> a__plus(mark(X1),mark(X2)) r26: mark(and(X1,X2)) -> a__and(mark(X1),X2) r27: mark(isNatKind(X)) -> a__isNatKind(X) r28: mark(tt()) -> tt() r29: mark(s(X)) -> s(mark(X)) r30: mark(|0|()) -> |0|() r31: a__U11(X1,X2,X3) -> U11(X1,X2,X3) r32: a__U12(X1,X2) -> U12(X1,X2) r33: a__isNat(X) -> isNat(X) r34: a__U13(X) -> U13(X) r35: a__U21(X1,X2) -> U21(X1,X2) r36: a__U22(X) -> U22(X) r37: a__U31(X1,X2) -> U31(X1,X2) r38: a__U41(X1,X2,X3) -> U41(X1,X2,X3) r39: a__plus(X1,X2) -> plus(X1,X2) r40: a__and(X1,X2) -> and(X1,X2) r41: a__isNatKind(X) -> isNatKind(X) The estimated dependency graph contains the following SCCs: {p1, p2, p3, p4, p5, p6, p7, p8, p9, p10, p11, p12, p13, p14, p15, p16, p17, p18, p19, p20, p21, p22, p23, p24, p25, p26, p27, p28, p29} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: a__U11#(tt(),V1,V2) -> a__U12#(a__isNat(V1),V2) p2: a__U12#(tt(),V2) -> a__isNat#(V2) p3: a__isNat#(s(V1)) -> a__isNatKind#(V1) p4: a__isNatKind#(s(V1)) -> a__isNatKind#(V1) p5: a__isNatKind#(plus(V1,V2)) -> a__isNatKind#(V1) p6: a__isNatKind#(plus(V1,V2)) -> a__and#(a__isNatKind(V1),isNatKind(V2)) p7: a__and#(tt(),X) -> mark#(X) p8: mark#(s(X)) -> mark#(X) p9: mark#(isNatKind(X)) -> a__isNatKind#(X) p10: mark#(and(X1,X2)) -> mark#(X1) p11: mark#(and(X1,X2)) -> a__and#(mark(X1),X2) p12: mark#(plus(X1,X2)) -> mark#(X2) p13: mark#(plus(X1,X2)) -> mark#(X1) p14: mark#(U41(X1,X2,X3)) -> mark#(X1) p15: mark#(U22(X)) -> mark#(X) p16: mark#(U21(X1,X2)) -> mark#(X1) p17: mark#(U21(X1,X2)) -> a__U21#(mark(X1),X2) p18: a__U21#(tt(),V1) -> a__isNat#(V1) p19: a__isNat#(s(V1)) -> a__U21#(a__isNatKind(V1),V1) p20: a__isNat#(plus(V1,V2)) -> a__isNatKind#(V1) p21: a__isNat#(plus(V1,V2)) -> a__and#(a__isNatKind(V1),isNatKind(V2)) p22: a__isNat#(plus(V1,V2)) -> a__U11#(a__and(a__isNatKind(V1),isNatKind(V2)),V1,V2) p23: a__U11#(tt(),V1,V2) -> a__isNat#(V1) p24: mark#(U13(X)) -> mark#(X) p25: mark#(isNat(X)) -> a__isNat#(X) p26: mark#(U12(X1,X2)) -> mark#(X1) p27: mark#(U12(X1,X2)) -> a__U12#(mark(X1),X2) p28: mark#(U11(X1,X2,X3)) -> mark#(X1) p29: mark#(U11(X1,X2,X3)) -> a__U11#(mark(X1),X2,X3) and R consists of: r1: a__U11(tt(),V1,V2) -> a__U12(a__isNat(V1),V2) r2: a__U12(tt(),V2) -> a__U13(a__isNat(V2)) r3: a__U13(tt()) -> tt() r4: a__U21(tt(),V1) -> a__U22(a__isNat(V1)) r5: a__U22(tt()) -> tt() r6: a__U31(tt(),N) -> mark(N) r7: a__U41(tt(),M,N) -> s(a__plus(mark(N),mark(M))) r8: a__and(tt(),X) -> mark(X) r9: a__isNat(|0|()) -> tt() r10: a__isNat(plus(V1,V2)) -> a__U11(a__and(a__isNatKind(V1),isNatKind(V2)),V1,V2) r11: a__isNat(s(V1)) -> a__U21(a__isNatKind(V1),V1) r12: a__isNatKind(|0|()) -> tt() r13: a__isNatKind(plus(V1,V2)) -> a__and(a__isNatKind(V1),isNatKind(V2)) r14: a__isNatKind(s(V1)) -> a__isNatKind(V1) r15: a__plus(N,|0|()) -> a__U31(a__and(a__isNat(N),isNatKind(N)),N) r16: a__plus(N,s(M)) -> a__U41(a__and(a__and(a__isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N) r17: mark(U11(X1,X2,X3)) -> a__U11(mark(X1),X2,X3) r18: mark(U12(X1,X2)) -> a__U12(mark(X1),X2) r19: mark(isNat(X)) -> a__isNat(X) r20: mark(U13(X)) -> a__U13(mark(X)) r21: mark(U21(X1,X2)) -> a__U21(mark(X1),X2) r22: mark(U22(X)) -> a__U22(mark(X)) r23: mark(U31(X1,X2)) -> a__U31(mark(X1),X2) r24: mark(U41(X1,X2,X3)) -> a__U41(mark(X1),X2,X3) r25: mark(plus(X1,X2)) -> a__plus(mark(X1),mark(X2)) r26: mark(and(X1,X2)) -> a__and(mark(X1),X2) r27: mark(isNatKind(X)) -> a__isNatKind(X) r28: mark(tt()) -> tt() r29: mark(s(X)) -> s(mark(X)) r30: mark(|0|()) -> |0|() r31: a__U11(X1,X2,X3) -> U11(X1,X2,X3) r32: a__U12(X1,X2) -> U12(X1,X2) r33: a__isNat(X) -> isNat(X) r34: a__U13(X) -> U13(X) r35: a__U21(X1,X2) -> U21(X1,X2) r36: a__U22(X) -> U22(X) r37: a__U31(X1,X2) -> U31(X1,X2) r38: a__U41(X1,X2,X3) -> U41(X1,X2,X3) r39: a__plus(X1,X2) -> plus(X1,X2) r40: a__and(X1,X2) -> and(X1,X2) r41: a__isNatKind(X) -> isNatKind(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, r33, r34, r35, r36, r37, r38, r39, r40, r41 Take the reduction pair: lexicographic combination of reduction pairs: 1. weighted path order base order: matrix interpretations: carrier: N^2 order: lexicographic order interpretations: a__U11#_A(x1,x2,x3) = (17,2) tt_A() = (0,15) a__U12#_A(x1,x2) = (17,2) a__isNat_A(x1) = ((0,0),(1,0)) x1 + (0,14) a__isNat#_A(x1) = (17,2) s_A(x1) = ((1,0),(0,0)) x1 + (8,21) a__isNatKind#_A(x1) = (17,2) plus_A(x1,x2) = ((1,0),(0,0)) x1 + ((1,0),(1,1)) x2 + (8,5) a__and#_A(x1,x2) = ((0,0),(1,0)) x2 + (17,2) a__isNatKind_A(x1) = ((0,0),(1,0)) x1 + (0,13) isNatKind_A(x1) = ((0,0),(1,0)) x1 + (0,3) mark#_A(x1) = ((0,0),(1,0)) x1 + (17,2) and_A(x1,x2) = ((1,0),(0,0)) x1 + ((1,0),(1,1)) x2 + (0,15) mark_A(x1) = x1 + (0,16) U41_A(x1,x2,x3) = ((1,0),(0,0)) x1 + ((1,0),(1,0)) x2 + ((1,0),(0,0)) x3 + (16,5) U22_A(x1) = ((1,0),(0,0)) x1 + (0,1) U21_A(x1,x2) = ((1,0),(0,0)) x1 + (0,7) a__U21#_A(x1,x2) = (17,2) a__and_A(x1,x2) = ((1,0),(0,0)) x1 + ((1,0),(1,1)) x2 + (0,17) U13_A(x1) = ((1,0),(1,1)) x1 isNat_A(x1) = ((0,0),(1,0)) x1 + (0,14) U12_A(x1,x2) = ((1,0),(0,0)) x1 + ((0,0),(1,0)) x2 + (0,1) U11_A(x1,x2,x3) = ((1,0),(1,0)) x1 + ((0,0),(1,0)) x2 + ((0,0),(1,0)) x3 + (0,13) a__U11_A(x1,x2,x3) = ((1,0),(1,0)) x1 + ((0,0),(1,0)) x2 + ((0,0),(1,0)) x3 + (0,14) a__U12_A(x1,x2) = ((1,0),(0,0)) x1 + ((0,0),(1,0)) x2 + (0,14) a__U13_A(x1) = ((1,0),(1,1)) x1 a__U21_A(x1,x2) = ((1,0),(0,0)) x1 + (0,22) a__U22_A(x1) = ((1,0),(0,0)) x1 + (0,17) a__U31_A(x1,x2) = ((0,0),(1,0)) x1 + ((1,0),(0,0)) x2 + (1,16) a__U41_A(x1,x2,x3) = ((1,0),(0,0)) x1 + ((1,0),(1,0)) x2 + ((1,0),(0,0)) x3 + (16,21) a__plus_A(x1,x2) = ((1,0),(0,0)) x1 + ((1,0),(1,1)) x2 + (8,5) |0|_A() = (2,4) U31_A(x1,x2) = ((0,0),(1,0)) x1 + ((1,0),(0,0)) x2 + (1,1) precedence: a__isNat = isNat = U11 = a__U11 > |0| > a__U11# = tt = a__U12# = a__isNat# = s = a__isNatKind# = plus = a__and# = a__isNatKind = isNatKind = mark# = mark = U22 = U21 = a__U21# = U13 = U12 = a__U12 = a__U13 = a__U21 = a__U22 = a__U31 = a__U41 = a__plus = U31 > U41 = a__and > and partial status: pi(a__U11#) = [] pi(tt) = [] pi(a__U12#) = [] pi(a__isNat) = [] pi(a__isNat#) = [] pi(s) = [] pi(a__isNatKind#) = [] pi(plus) = [2] pi(a__and#) = [] pi(a__isNatKind) = [] pi(isNatKind) = [] pi(mark#) = [] pi(and) = [2] pi(mark) = [1] pi(U41) = [] pi(U22) = [] pi(U21) = [] pi(a__U21#) = [] pi(a__and) = [2] pi(U13) = [] pi(isNat) = [] pi(U12) = [] pi(U11) = [] pi(a__U11) = [] pi(a__U12) = [] pi(a__U13) = [] pi(a__U21) = [] pi(a__U22) = [] pi(a__U31) = [] pi(a__U41) = [] pi(a__plus) = [2] pi(|0|) = [] pi(U31) = [] 2. weighted path order base order: matrix interpretations: carrier: N^2 order: lexicographic order interpretations: a__U11#_A(x1,x2,x3) = (11,2) tt_A() = (12,3) a__U12#_A(x1,x2) = (11,2) a__isNat_A(x1) = (0,0) a__isNat#_A(x1) = (11,2) s_A(x1) = (26,11) a__isNatKind#_A(x1) = (11,2) plus_A(x1,x2) = x2 + (12,1) a__and#_A(x1,x2) = (11,2) a__isNatKind_A(x1) = (13,20) isNatKind_A(x1) = (3,4) mark#_A(x1) = (11,2) and_A(x1,x2) = ((1,0),(1,1)) x2 + (12,3) mark_A(x1) = ((1,0),(1,1)) x1 + (10,13) U41_A(x1,x2,x3) = (17,12) U22_A(x1) = (3,1) U21_A(x1,x2) = (0,0) a__U21#_A(x1,x2) = (11,2) a__and_A(x1,x2) = ((1,0),(0,0)) x2 + (10,14) U13_A(x1) = (12,1) isNat_A(x1) = (0,0) U12_A(x1,x2) = (11,2) U11_A(x1,x2,x3) = (12,1) a__U11_A(x1,x2,x3) = (0,0) a__U12_A(x1,x2) = (14,5) a__U13_A(x1) = (13,4) a__U21_A(x1,x2) = (0,0) a__U22_A(x1) = (13,4) a__U31_A(x1,x2) = (2,16) a__U41_A(x1,x2,x3) = (26,11) a__plus_A(x1,x2) = x2 + (12,12) |0|_A() = (4,3) U31_A(x1,x2) = (1,0) precedence: U41 > and > U13 > a__U12 > a__U11# = tt = a__U12# = a__isNat# = a__isNatKind# = a__and# = a__isNatKind = mark# = mark = a__U21# = U12 = a__U13 = a__plus > a__U31 > U22 > isNatKind > s = plus = a__and = a__U41 > a__isNat = |0| > isNat > a__U21 > U21 > a__U11 > U11 > a__U22 = U31 partial status: pi(a__U11#) = [] pi(tt) = [] pi(a__U12#) = [] pi(a__isNat) = [] pi(a__isNat#) = [] pi(s) = [] pi(a__isNatKind#) = [] pi(plus) = [2] pi(a__and#) = [] pi(a__isNatKind) = [] pi(isNatKind) = [] pi(mark#) = [] pi(and) = [2] pi(mark) = [1] pi(U41) = [] pi(U22) = [] pi(U21) = [] pi(a__U21#) = [] pi(a__and) = [] pi(U13) = [] pi(isNat) = [] pi(U12) = [] pi(U11) = [] pi(a__U11) = [] pi(a__U12) = [] pi(a__U13) = [] pi(a__U21) = [] pi(a__U22) = [] pi(a__U31) = [] pi(a__U41) = [] pi(a__plus) = [2] pi(|0|) = [] pi(U31) = [] The next rules are strictly ordered: p13 We remove them from the problem. -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: a__U11#(tt(),V1,V2) -> a__U12#(a__isNat(V1),V2) p2: a__U12#(tt(),V2) -> a__isNat#(V2) p3: a__isNat#(s(V1)) -> a__isNatKind#(V1) p4: a__isNatKind#(s(V1)) -> a__isNatKind#(V1) p5: a__isNatKind#(plus(V1,V2)) -> a__isNatKind#(V1) p6: a__isNatKind#(plus(V1,V2)) -> a__and#(a__isNatKind(V1),isNatKind(V2)) p7: a__and#(tt(),X) -> mark#(X) p8: mark#(s(X)) -> mark#(X) p9: mark#(isNatKind(X)) -> a__isNatKind#(X) p10: mark#(and(X1,X2)) -> mark#(X1) p11: mark#(and(X1,X2)) -> a__and#(mark(X1),X2) p12: mark#(plus(X1,X2)) -> mark#(X2) p13: mark#(U41(X1,X2,X3)) -> mark#(X1) p14: mark#(U22(X)) -> mark#(X) p15: mark#(U21(X1,X2)) -> mark#(X1) p16: mark#(U21(X1,X2)) -> a__U21#(mark(X1),X2) p17: a__U21#(tt(),V1) -> a__isNat#(V1) p18: a__isNat#(s(V1)) -> a__U21#(a__isNatKind(V1),V1) p19: a__isNat#(plus(V1,V2)) -> a__isNatKind#(V1) p20: a__isNat#(plus(V1,V2)) -> a__and#(a__isNatKind(V1),isNatKind(V2)) p21: a__isNat#(plus(V1,V2)) -> a__U11#(a__and(a__isNatKind(V1),isNatKind(V2)),V1,V2) p22: a__U11#(tt(),V1,V2) -> a__isNat#(V1) p23: mark#(U13(X)) -> mark#(X) p24: mark#(isNat(X)) -> a__isNat#(X) p25: mark#(U12(X1,X2)) -> mark#(X1) p26: mark#(U12(X1,X2)) -> a__U12#(mark(X1),X2) p27: mark#(U11(X1,X2,X3)) -> mark#(X1) p28: mark#(U11(X1,X2,X3)) -> a__U11#(mark(X1),X2,X3) and R consists of: r1: a__U11(tt(),V1,V2) -> a__U12(a__isNat(V1),V2) r2: a__U12(tt(),V2) -> a__U13(a__isNat(V2)) r3: a__U13(tt()) -> tt() r4: a__U21(tt(),V1) -> a__U22(a__isNat(V1)) r5: a__U22(tt()) -> tt() r6: a__U31(tt(),N) -> mark(N) r7: a__U41(tt(),M,N) -> s(a__plus(mark(N),mark(M))) r8: a__and(tt(),X) -> mark(X) r9: a__isNat(|0|()) -> tt() r10: a__isNat(plus(V1,V2)) -> a__U11(a__and(a__isNatKind(V1),isNatKind(V2)),V1,V2) r11: a__isNat(s(V1)) -> a__U21(a__isNatKind(V1),V1) r12: a__isNatKind(|0|()) -> tt() r13: a__isNatKind(plus(V1,V2)) -> a__and(a__isNatKind(V1),isNatKind(V2)) r14: a__isNatKind(s(V1)) -> a__isNatKind(V1) r15: a__plus(N,|0|()) -> a__U31(a__and(a__isNat(N),isNatKind(N)),N) r16: a__plus(N,s(M)) -> a__U41(a__and(a__and(a__isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N) r17: mark(U11(X1,X2,X3)) -> a__U11(mark(X1),X2,X3) r18: mark(U12(X1,X2)) -> a__U12(mark(X1),X2) r19: mark(isNat(X)) -> a__isNat(X) r20: mark(U13(X)) -> a__U13(mark(X)) r21: mark(U21(X1,X2)) -> a__U21(mark(X1),X2) r22: mark(U22(X)) -> a__U22(mark(X)) r23: mark(U31(X1,X2)) -> a__U31(mark(X1),X2) r24: mark(U41(X1,X2,X3)) -> a__U41(mark(X1),X2,X3) r25: mark(plus(X1,X2)) -> a__plus(mark(X1),mark(X2)) r26: mark(and(X1,X2)) -> a__and(mark(X1),X2) r27: mark(isNatKind(X)) -> a__isNatKind(X) r28: mark(tt()) -> tt() r29: mark(s(X)) -> s(mark(X)) r30: mark(|0|()) -> |0|() r31: a__U11(X1,X2,X3) -> U11(X1,X2,X3) r32: a__U12(X1,X2) -> U12(X1,X2) r33: a__isNat(X) -> isNat(X) r34: a__U13(X) -> U13(X) r35: a__U21(X1,X2) -> U21(X1,X2) r36: a__U22(X) -> U22(X) r37: a__U31(X1,X2) -> U31(X1,X2) r38: a__U41(X1,X2,X3) -> U41(X1,X2,X3) r39: a__plus(X1,X2) -> plus(X1,X2) r40: a__and(X1,X2) -> and(X1,X2) r41: a__isNatKind(X) -> isNatKind(X) The estimated dependency graph contains the following SCCs: {p1, p2, p3, p4, p5, p6, p7, p8, p9, p10, p11, p12, p13, p14, p15, p16, p17, p18, p19, p20, p21, p22, p23, p24, p25, p26, p27, p28} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: a__U11#(tt(),V1,V2) -> a__U12#(a__isNat(V1),V2) p2: a__U12#(tt(),V2) -> a__isNat#(V2) p3: a__isNat#(plus(V1,V2)) -> a__U11#(a__and(a__isNatKind(V1),isNatKind(V2)),V1,V2) p4: a__U11#(tt(),V1,V2) -> a__isNat#(V1) p5: a__isNat#(plus(V1,V2)) -> a__and#(a__isNatKind(V1),isNatKind(V2)) p6: a__and#(tt(),X) -> mark#(X) p7: mark#(U11(X1,X2,X3)) -> a__U11#(mark(X1),X2,X3) p8: mark#(U11(X1,X2,X3)) -> mark#(X1) p9: mark#(U12(X1,X2)) -> a__U12#(mark(X1),X2) p10: mark#(U12(X1,X2)) -> mark#(X1) p11: mark#(isNat(X)) -> a__isNat#(X) p12: a__isNat#(plus(V1,V2)) -> a__isNatKind#(V1) p13: a__isNatKind#(plus(V1,V2)) -> a__and#(a__isNatKind(V1),isNatKind(V2)) p14: a__isNatKind#(plus(V1,V2)) -> a__isNatKind#(V1) p15: a__isNatKind#(s(V1)) -> a__isNatKind#(V1) p16: a__isNat#(s(V1)) -> a__U21#(a__isNatKind(V1),V1) p17: a__U21#(tt(),V1) -> a__isNat#(V1) p18: a__isNat#(s(V1)) -> a__isNatKind#(V1) p19: mark#(U13(X)) -> mark#(X) p20: mark#(U21(X1,X2)) -> a__U21#(mark(X1),X2) p21: mark#(U21(X1,X2)) -> mark#(X1) p22: mark#(U22(X)) -> mark#(X) p23: mark#(U41(X1,X2,X3)) -> mark#(X1) p24: mark#(plus(X1,X2)) -> mark#(X2) p25: mark#(and(X1,X2)) -> a__and#(mark(X1),X2) p26: mark#(and(X1,X2)) -> mark#(X1) p27: mark#(isNatKind(X)) -> a__isNatKind#(X) p28: mark#(s(X)) -> mark#(X) and R consists of: r1: a__U11(tt(),V1,V2) -> a__U12(a__isNat(V1),V2) r2: a__U12(tt(),V2) -> a__U13(a__isNat(V2)) r3: a__U13(tt()) -> tt() r4: a__U21(tt(),V1) -> a__U22(a__isNat(V1)) r5: a__U22(tt()) -> tt() r6: a__U31(tt(),N) -> mark(N) r7: a__U41(tt(),M,N) -> s(a__plus(mark(N),mark(M))) r8: a__and(tt(),X) -> mark(X) r9: a__isNat(|0|()) -> tt() r10: a__isNat(plus(V1,V2)) -> a__U11(a__and(a__isNatKind(V1),isNatKind(V2)),V1,V2) r11: a__isNat(s(V1)) -> a__U21(a__isNatKind(V1),V1) r12: a__isNatKind(|0|()) -> tt() r13: a__isNatKind(plus(V1,V2)) -> a__and(a__isNatKind(V1),isNatKind(V2)) r14: a__isNatKind(s(V1)) -> a__isNatKind(V1) r15: a__plus(N,|0|()) -> a__U31(a__and(a__isNat(N),isNatKind(N)),N) r16: a__plus(N,s(M)) -> a__U41(a__and(a__and(a__isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N) r17: mark(U11(X1,X2,X3)) -> a__U11(mark(X1),X2,X3) r18: mark(U12(X1,X2)) -> a__U12(mark(X1),X2) r19: mark(isNat(X)) -> a__isNat(X) r20: mark(U13(X)) -> a__U13(mark(X)) r21: mark(U21(X1,X2)) -> a__U21(mark(X1),X2) r22: mark(U22(X)) -> a__U22(mark(X)) r23: mark(U31(X1,X2)) -> a__U31(mark(X1),X2) r24: mark(U41(X1,X2,X3)) -> a__U41(mark(X1),X2,X3) r25: mark(plus(X1,X2)) -> a__plus(mark(X1),mark(X2)) r26: mark(and(X1,X2)) -> a__and(mark(X1),X2) r27: mark(isNatKind(X)) -> a__isNatKind(X) r28: mark(tt()) -> tt() r29: mark(s(X)) -> s(mark(X)) r30: mark(|0|()) -> |0|() r31: a__U11(X1,X2,X3) -> U11(X1,X2,X3) r32: a__U12(X1,X2) -> U12(X1,X2) r33: a__isNat(X) -> isNat(X) r34: a__U13(X) -> U13(X) r35: a__U21(X1,X2) -> U21(X1,X2) r36: a__U22(X) -> U22(X) r37: a__U31(X1,X2) -> U31(X1,X2) r38: a__U41(X1,X2,X3) -> U41(X1,X2,X3) r39: a__plus(X1,X2) -> plus(X1,X2) r40: a__and(X1,X2) -> and(X1,X2) r41: a__isNatKind(X) -> isNatKind(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, r33, r34, r35, r36, r37, r38, r39, r40, r41 Take the reduction pair: lexicographic combination of reduction pairs: 1. weighted path order base order: matrix interpretations: carrier: N^2 order: lexicographic order interpretations: a__U11#_A(x1,x2,x3) = (20,15) tt_A() = (0,11) a__U12#_A(x1,x2) = (20,15) a__isNat_A(x1) = ((0,0),(1,0)) x1 + (0,18) a__isNat#_A(x1) = (20,15) plus_A(x1,x2) = ((1,0),(1,1)) x1 + ((1,0),(1,1)) x2 + (19,1) a__and_A(x1,x2) = ((1,0),(0,0)) x1 + ((1,0),(1,1)) x2 + (0,18) a__isNatKind_A(x1) = ((0,0),(1,0)) x1 + (0,14) isNatKind_A(x1) = ((0,0),(1,0)) x1 + (0,14) a__and#_A(x1,x2) = ((0,0),(1,0)) x2 + (20,15) mark#_A(x1) = ((0,0),(1,0)) x1 + (20,15) U11_A(x1,x2,x3) = ((1,0),(0,0)) x1 + (0,16) mark_A(x1) = ((1,0),(1,1)) x1 + (0,10) U12_A(x1,x2) = ((1,0),(0,0)) x1 + (0,16) isNat_A(x1) = ((0,0),(1,0)) x1 + (0,18) a__isNatKind#_A(x1) = (20,15) s_A(x1) = ((1,0),(0,0)) x1 + (21,0) a__U21#_A(x1,x2) = (20,15) U13_A(x1) = ((1,0),(0,0)) x1 + (0,2) U21_A(x1,x2) = ((1,0),(0,0)) x1 + ((0,0),(1,0)) x2 + (0,19) U22_A(x1) = x1 U41_A(x1,x2,x3) = ((1,0),(1,0)) x1 + ((1,0),(1,0)) x2 + ((1,0),(1,1)) x3 + (40,16) and_A(x1,x2) = ((1,0),(0,0)) x1 + x2 + (0,16) a__U11_A(x1,x2,x3) = ((1,0),(0,0)) x1 + (0,17) a__U12_A(x1,x2) = ((1,0),(0,0)) x1 + (0,16) a__U13_A(x1) = ((1,0),(0,0)) x1 + (0,11) a__U21_A(x1,x2) = ((1,0),(0,0)) x1 + ((0,0),(1,0)) x2 + (0,19) a__U22_A(x1) = x1 a__U31_A(x1,x2) = x2 + (1,14) a__U41_A(x1,x2,x3) = ((1,0),(1,0)) x1 + ((1,0),(1,0)) x2 + ((1,0),(1,1)) x3 + (40,30) a__plus_A(x1,x2) = ((1,0),(1,1)) x1 + ((1,0),(1,1)) x2 + (19,10) |0|_A() = (4,0) U31_A(x1,x2) = x2 + (1,4) precedence: a__isNatKind = isNatKind > a__and = a__U31 = |0| = U31 > a__U11# = tt = a__U12# = a__isNat = a__isNat# = plus = a__and# = mark# = U11 = mark = U12 = isNat = a__isNatKind# = a__U21# = U13 = U21 = U41 = and = a__U11 = a__U12 = a__U13 = a__U21 = a__U41 = a__plus > a__U22 > s = U22 partial status: pi(a__U11#) = [] pi(tt) = [] pi(a__U12#) = [] pi(a__isNat) = [] pi(a__isNat#) = [] pi(plus) = [1] pi(a__and) = [2] pi(a__isNatKind) = [] pi(isNatKind) = [] pi(a__and#) = [] pi(mark#) = [] pi(U11) = [] pi(mark) = [1] pi(U12) = [] pi(isNat) = [] pi(a__isNatKind#) = [] pi(s) = [] pi(a__U21#) = [] pi(U13) = [] pi(U21) = [] pi(U22) = [1] pi(U41) = [3] pi(and) = [2] pi(a__U11) = [] pi(a__U12) = [] pi(a__U13) = [] pi(a__U21) = [] pi(a__U22) = [1] pi(a__U31) = [2] pi(a__U41) = [3] pi(a__plus) = [1, 2] pi(|0|) = [] pi(U31) = [2] 2. weighted path order base order: matrix interpretations: carrier: N^2 order: lexicographic order interpretations: a__U11#_A(x1,x2,x3) = (13,8) tt_A() = (0,0) a__U12#_A(x1,x2) = (13,8) a__isNat_A(x1) = (24,5) a__isNat#_A(x1) = (13,8) plus_A(x1,x2) = ((1,0),(1,1)) x1 + (22,3) a__and_A(x1,x2) = ((1,0),(0,0)) x2 + (11,0) a__isNatKind_A(x1) = (11,4) isNatKind_A(x1) = (0,4) a__and#_A(x1,x2) = (13,8) mark#_A(x1) = (13,8) U11_A(x1,x2,x3) = (14,9) mark_A(x1) = ((1,0),(1,1)) x1 + (12,7) U12_A(x1,x2) = (0,2) isNat_A(x1) = (24,5) a__isNatKind#_A(x1) = (13,8) s_A(x1) = (11,6) a__U21#_A(x1,x2) = (13,8) U13_A(x1) = (9,1) U21_A(x1,x2) = (24,5) U22_A(x1) = ((0,0),(1,0)) x1 + (4,1) U41_A(x1,x2,x3) = ((1,0),(0,0)) x3 + (13,0) and_A(x1,x2) = ((1,0),(0,0)) x2 + (11,0) a__U11_A(x1,x2,x3) = (23,4) a__U12_A(x1,x2) = (11,3) a__U13_A(x1) = (10,2) a__U21_A(x1,x2) = (24,5) a__U22_A(x1) = ((0,0),(1,0)) x1 + (16,0) a__U31_A(x1,x2) = ((1,0),(1,1)) x2 + (13,11) a__U41_A(x1,x2,x3) = x3 + (13,0) a__plus_A(x1,x2) = ((1,0),(1,1)) x1 + (22,12) |0|_A() = (13,12) U31_A(x1,x2) = ((1,0),(0,0)) x2 + (2,1) precedence: |0| > plus = a__U31 = a__plus > a__U22 > a__U11# = a__U12# = a__isNat = a__isNat# = a__and# = mark# = isNat = a__isNatKind# = a__U21# = a__U11 = a__U21 > U31 > tt = a__and = a__isNatKind = U11 = mark = a__U12 > a__U13 > U13 > a__U41 > isNatKind = s = U22 > U21 > U41 > U12 > and partial status: pi(a__U11#) = [] pi(tt) = [] pi(a__U12#) = [] pi(a__isNat) = [] pi(a__isNat#) = [] pi(plus) = [] pi(a__and) = [] pi(a__isNatKind) = [] pi(isNatKind) = [] pi(a__and#) = [] pi(mark#) = [] pi(U11) = [] pi(mark) = [1] pi(U12) = [] pi(isNat) = [] pi(a__isNatKind#) = [] pi(s) = [] pi(a__U21#) = [] pi(U13) = [] pi(U21) = [] pi(U22) = [] pi(U41) = [] pi(and) = [] pi(a__U11) = [] pi(a__U12) = [] pi(a__U13) = [] pi(a__U21) = [] pi(a__U22) = [] pi(a__U31) = [] pi(a__U41) = [3] pi(a__plus) = [1] pi(|0|) = [] pi(U31) = [] The next rules are strictly ordered: p23 We remove them from the problem. -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: a__U11#(tt(),V1,V2) -> a__U12#(a__isNat(V1),V2) p2: a__U12#(tt(),V2) -> a__isNat#(V2) p3: a__isNat#(plus(V1,V2)) -> a__U11#(a__and(a__isNatKind(V1),isNatKind(V2)),V1,V2) p4: a__U11#(tt(),V1,V2) -> a__isNat#(V1) p5: a__isNat#(plus(V1,V2)) -> a__and#(a__isNatKind(V1),isNatKind(V2)) p6: a__and#(tt(),X) -> mark#(X) p7: mark#(U11(X1,X2,X3)) -> a__U11#(mark(X1),X2,X3) p8: mark#(U11(X1,X2,X3)) -> mark#(X1) p9: mark#(U12(X1,X2)) -> a__U12#(mark(X1),X2) p10: mark#(U12(X1,X2)) -> mark#(X1) p11: mark#(isNat(X)) -> a__isNat#(X) p12: a__isNat#(plus(V1,V2)) -> a__isNatKind#(V1) p13: a__isNatKind#(plus(V1,V2)) -> a__and#(a__isNatKind(V1),isNatKind(V2)) p14: a__isNatKind#(plus(V1,V2)) -> a__isNatKind#(V1) p15: a__isNatKind#(s(V1)) -> a__isNatKind#(V1) p16: a__isNat#(s(V1)) -> a__U21#(a__isNatKind(V1),V1) p17: a__U21#(tt(),V1) -> a__isNat#(V1) p18: a__isNat#(s(V1)) -> a__isNatKind#(V1) p19: mark#(U13(X)) -> mark#(X) p20: mark#(U21(X1,X2)) -> a__U21#(mark(X1),X2) p21: mark#(U21(X1,X2)) -> mark#(X1) p22: mark#(U22(X)) -> mark#(X) p23: mark#(plus(X1,X2)) -> mark#(X2) p24: mark#(and(X1,X2)) -> a__and#(mark(X1),X2) p25: mark#(and(X1,X2)) -> mark#(X1) p26: mark#(isNatKind(X)) -> a__isNatKind#(X) p27: mark#(s(X)) -> mark#(X) and R consists of: r1: a__U11(tt(),V1,V2) -> a__U12(a__isNat(V1),V2) r2: a__U12(tt(),V2) -> a__U13(a__isNat(V2)) r3: a__U13(tt()) -> tt() r4: a__U21(tt(),V1) -> a__U22(a__isNat(V1)) r5: a__U22(tt()) -> tt() r6: a__U31(tt(),N) -> mark(N) r7: a__U41(tt(),M,N) -> s(a__plus(mark(N),mark(M))) r8: a__and(tt(),X) -> mark(X) r9: a__isNat(|0|()) -> tt() r10: a__isNat(plus(V1,V2)) -> a__U11(a__and(a__isNatKind(V1),isNatKind(V2)),V1,V2) r11: a__isNat(s(V1)) -> a__U21(a__isNatKind(V1),V1) r12: a__isNatKind(|0|()) -> tt() r13: a__isNatKind(plus(V1,V2)) -> a__and(a__isNatKind(V1),isNatKind(V2)) r14: a__isNatKind(s(V1)) -> a__isNatKind(V1) r15: a__plus(N,|0|()) -> a__U31(a__and(a__isNat(N),isNatKind(N)),N) r16: a__plus(N,s(M)) -> a__U41(a__and(a__and(a__isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N) r17: mark(U11(X1,X2,X3)) -> a__U11(mark(X1),X2,X3) r18: mark(U12(X1,X2)) -> a__U12(mark(X1),X2) r19: mark(isNat(X)) -> a__isNat(X) r20: mark(U13(X)) -> a__U13(mark(X)) r21: mark(U21(X1,X2)) -> a__U21(mark(X1),X2) r22: mark(U22(X)) -> a__U22(mark(X)) r23: mark(U31(X1,X2)) -> a__U31(mark(X1),X2) r24: mark(U41(X1,X2,X3)) -> a__U41(mark(X1),X2,X3) r25: mark(plus(X1,X2)) -> a__plus(mark(X1),mark(X2)) r26: mark(and(X1,X2)) -> a__and(mark(X1),X2) r27: mark(isNatKind(X)) -> a__isNatKind(X) r28: mark(tt()) -> tt() r29: mark(s(X)) -> s(mark(X)) r30: mark(|0|()) -> |0|() r31: a__U11(X1,X2,X3) -> U11(X1,X2,X3) r32: a__U12(X1,X2) -> U12(X1,X2) r33: a__isNat(X) -> isNat(X) r34: a__U13(X) -> U13(X) r35: a__U21(X1,X2) -> U21(X1,X2) r36: a__U22(X) -> U22(X) r37: a__U31(X1,X2) -> U31(X1,X2) r38: a__U41(X1,X2,X3) -> U41(X1,X2,X3) r39: a__plus(X1,X2) -> plus(X1,X2) r40: a__and(X1,X2) -> and(X1,X2) r41: a__isNatKind(X) -> isNatKind(X) The estimated dependency graph contains the following SCCs: {p1, p2, p3, p4, p5, p6, p7, p8, p9, p10, p11, p12, p13, p14, p15, p16, p17, p18, p19, p20, p21, p22, p23, p24, p25, p26, p27} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: a__U11#(tt(),V1,V2) -> a__U12#(a__isNat(V1),V2) p2: a__U12#(tt(),V2) -> a__isNat#(V2) p3: a__isNat#(s(V1)) -> a__isNatKind#(V1) p4: a__isNatKind#(s(V1)) -> a__isNatKind#(V1) p5: a__isNatKind#(plus(V1,V2)) -> a__isNatKind#(V1) p6: a__isNatKind#(plus(V1,V2)) -> a__and#(a__isNatKind(V1),isNatKind(V2)) p7: a__and#(tt(),X) -> mark#(X) p8: mark#(s(X)) -> mark#(X) p9: mark#(isNatKind(X)) -> a__isNatKind#(X) p10: mark#(and(X1,X2)) -> mark#(X1) p11: mark#(and(X1,X2)) -> a__and#(mark(X1),X2) p12: mark#(plus(X1,X2)) -> mark#(X2) p13: mark#(U22(X)) -> mark#(X) p14: mark#(U21(X1,X2)) -> mark#(X1) p15: mark#(U21(X1,X2)) -> a__U21#(mark(X1),X2) p16: a__U21#(tt(),V1) -> a__isNat#(V1) p17: a__isNat#(s(V1)) -> a__U21#(a__isNatKind(V1),V1) p18: a__isNat#(plus(V1,V2)) -> a__isNatKind#(V1) p19: a__isNat#(plus(V1,V2)) -> a__and#(a__isNatKind(V1),isNatKind(V2)) p20: a__isNat#(plus(V1,V2)) -> a__U11#(a__and(a__isNatKind(V1),isNatKind(V2)),V1,V2) p21: a__U11#(tt(),V1,V2) -> a__isNat#(V1) p22: mark#(U13(X)) -> mark#(X) p23: mark#(isNat(X)) -> a__isNat#(X) p24: mark#(U12(X1,X2)) -> mark#(X1) p25: mark#(U12(X1,X2)) -> a__U12#(mark(X1),X2) p26: mark#(U11(X1,X2,X3)) -> mark#(X1) p27: mark#(U11(X1,X2,X3)) -> a__U11#(mark(X1),X2,X3) and R consists of: r1: a__U11(tt(),V1,V2) -> a__U12(a__isNat(V1),V2) r2: a__U12(tt(),V2) -> a__U13(a__isNat(V2)) r3: a__U13(tt()) -> tt() r4: a__U21(tt(),V1) -> a__U22(a__isNat(V1)) r5: a__U22(tt()) -> tt() r6: a__U31(tt(),N) -> mark(N) r7: a__U41(tt(),M,N) -> s(a__plus(mark(N),mark(M))) r8: a__and(tt(),X) -> mark(X) r9: a__isNat(|0|()) -> tt() r10: a__isNat(plus(V1,V2)) -> a__U11(a__and(a__isNatKind(V1),isNatKind(V2)),V1,V2) r11: a__isNat(s(V1)) -> a__U21(a__isNatKind(V1),V1) r12: a__isNatKind(|0|()) -> tt() r13: a__isNatKind(plus(V1,V2)) -> a__and(a__isNatKind(V1),isNatKind(V2)) r14: a__isNatKind(s(V1)) -> a__isNatKind(V1) r15: a__plus(N,|0|()) -> a__U31(a__and(a__isNat(N),isNatKind(N)),N) r16: a__plus(N,s(M)) -> a__U41(a__and(a__and(a__isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N) r17: mark(U11(X1,X2,X3)) -> a__U11(mark(X1),X2,X3) r18: mark(U12(X1,X2)) -> a__U12(mark(X1),X2) r19: mark(isNat(X)) -> a__isNat(X) r20: mark(U13(X)) -> a__U13(mark(X)) r21: mark(U21(X1,X2)) -> a__U21(mark(X1),X2) r22: mark(U22(X)) -> a__U22(mark(X)) r23: mark(U31(X1,X2)) -> a__U31(mark(X1),X2) r24: mark(U41(X1,X2,X3)) -> a__U41(mark(X1),X2,X3) r25: mark(plus(X1,X2)) -> a__plus(mark(X1),mark(X2)) r26: mark(and(X1,X2)) -> a__and(mark(X1),X2) r27: mark(isNatKind(X)) -> a__isNatKind(X) r28: mark(tt()) -> tt() r29: mark(s(X)) -> s(mark(X)) r30: mark(|0|()) -> |0|() r31: a__U11(X1,X2,X3) -> U11(X1,X2,X3) r32: a__U12(X1,X2) -> U12(X1,X2) r33: a__isNat(X) -> isNat(X) r34: a__U13(X) -> U13(X) r35: a__U21(X1,X2) -> U21(X1,X2) r36: a__U22(X) -> U22(X) r37: a__U31(X1,X2) -> U31(X1,X2) r38: a__U41(X1,X2,X3) -> U41(X1,X2,X3) r39: a__plus(X1,X2) -> plus(X1,X2) r40: a__and(X1,X2) -> and(X1,X2) r41: a__isNatKind(X) -> isNatKind(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, r33, r34, r35, r36, r37, r38, r39, r40, r41 Take the reduction pair: lexicographic combination of reduction pairs: 1. weighted path order base order: matrix interpretations: carrier: N^2 order: lexicographic order interpretations: a__U11#_A(x1,x2,x3) = ((1,0),(1,1)) x2 + ((1,0),(0,0)) x3 + (7,41) tt_A() = (0,16) a__U12#_A(x1,x2) = x1 + ((1,0),(1,1)) x2 + (3,1) a__isNat_A(x1) = ((1,0),(1,1)) x1 + (3,23) a__isNat#_A(x1) = x1 + (2,12) s_A(x1) = ((1,0),(0,0)) x1 + (46,0) a__isNatKind#_A(x1) = ((0,0),(1,0)) x1 + (47,54) plus_A(x1,x2) = ((1,0),(1,1)) x1 + x2 + (57,40) a__and#_A(x1,x2) = ((1,0),(1,1)) x2 + (47,3) a__isNatKind_A(x1) = ((0,0),(1,0)) x1 + (0,68) isNatKind_A(x1) = ((0,0),(1,0)) x1 + (0,53) mark#_A(x1) = ((1,0),(1,1)) x1 + (47,2) and_A(x1,x2) = x1 + x2 + (0,4) mark_A(x1) = ((1,0),(1,1)) x1 + (0,15) U22_A(x1) = x1 + (1,1) U21_A(x1,x2) = ((1,0),(1,1)) x1 + ((1,0),(1,1)) x2 + (11,1) a__U21#_A(x1,x2) = ((0,0),(1,0)) x1 + ((1,0),(1,1)) x2 + (12,13) a__and_A(x1,x2) = x1 + ((1,0),(1,1)) x2 + (0,4) U13_A(x1) = x1 + (48,2) isNat_A(x1) = ((1,0),(1,1)) x1 + (3,6) U12_A(x1,x2) = x1 + ((1,0),(1,1)) x2 + (52,3) U11_A(x1,x2,x3) = ((1,0),(1,0)) x1 + ((1,0),(1,1)) x2 + ((1,0),(0,0)) x3 + (59,41) a__U11_A(x1,x2,x3) = ((1,0),(1,0)) x1 + ((1,0),(1,1)) x2 + ((1,0),(0,0)) x3 + (59,79) a__U12_A(x1,x2) = x1 + ((1,0),(1,1)) x2 + (52,55) a__U13_A(x1) = x1 + (48,49) a__U21_A(x1,x2) = ((1,0),(1,1)) x1 + ((1,0),(1,1)) x2 + (11,10) a__U22_A(x1) = x1 + (1,2) a__U31_A(x1,x2) = ((1,0),(1,1)) x2 + (1,17) a__U41_A(x1,x2,x3) = ((1,0),(0,0)) x2 + x3 + (103,0) a__plus_A(x1,x2) = ((1,0),(1,1)) x1 + x2 + (57,81) |0|_A() = (4,1) U31_A(x1,x2) = ((1,0),(1,1)) x2 + (1,16) U41_A(x1,x2,x3) = ((1,0),(0,0)) x2 + x3 + (103,0) precedence: a__U31 > a__isNatKind = mark = a__plus > a__isNat > plus > a__U11# = a__U12# = a__isNat# = a__isNatKind# = isNatKind = mark# = a__and > a__and# = and > a__U21# > s = a__U41 > a__U11 > a__U12 > a__U13 > a__U21 > a__U22 > tt = U12 > U22 = U13 > U21 = U11 = U41 > |0| > isNat = U31 partial status: pi(a__U11#) = [] pi(tt) = [] pi(a__U12#) = [1, 2] pi(a__isNat) = [1] pi(a__isNat#) = [] pi(s) = [] pi(a__isNatKind#) = [] pi(plus) = [2] pi(a__and#) = [] pi(a__isNatKind) = [] pi(isNatKind) = [] pi(mark#) = [1] pi(and) = [1] pi(mark) = [1] pi(U22) = [1] pi(U21) = [1, 2] pi(a__U21#) = [] pi(a__and) = [1] pi(U13) = [] pi(isNat) = [] pi(U12) = [1, 2] pi(U11) = [] pi(a__U11) = [] pi(a__U12) = [1, 2] pi(a__U13) = [1] pi(a__U21) = [1, 2] pi(a__U22) = [] pi(a__U31) = [] pi(a__U41) = [3] pi(a__plus) = [1, 2] pi(|0|) = [] pi(U31) = [] pi(U41) = [] 2. weighted path order base order: matrix interpretations: carrier: N^2 order: lexicographic order interpretations: a__U11#_A(x1,x2,x3) = (12,24) tt_A() = (13,1) a__U12#_A(x1,x2) = ((0,0),(1,0)) x1 + x2 + (12,12) a__isNat_A(x1) = ((0,0),(1,0)) x1 + (16,43) a__isNat#_A(x1) = (12,24) s_A(x1) = (17,0) a__isNatKind#_A(x1) = (12,24) plus_A(x1,x2) = ((1,0),(1,1)) x2 + (23,67) a__and#_A(x1,x2) = (12,24) a__isNatKind_A(x1) = (1,4) isNatKind_A(x1) = (0,3) mark#_A(x1) = x1 + (12,21) and_A(x1,x2) = ((1,0),(1,1)) x1 + (0,3) mark_A(x1) = ((0,0),(1,0)) x1 + (22,47) U22_A(x1) = ((1,0),(0,0)) x1 + (13,0) U21_A(x1,x2) = ((1,0),(1,1)) x1 + (13,27) a__U21#_A(x1,x2) = (12,1) a__and_A(x1,x2) = ((1,0),(0,0)) x1 + (0,66) U13_A(x1) = (3,1) isNat_A(x1) = (1,3) U12_A(x1,x2) = x1 + x2 + (0,22) U11_A(x1,x2,x3) = (11,25) a__U11_A(x1,x2,x3) = (15,26) a__U12_A(x1,x2) = ((0,0),(1,0)) x2 + (21,46) a__U13_A(x1) = x1 + (4,2) a__U21_A(x1,x2) = ((1,0),(1,1)) x1 + (14,28) a__U22_A(x1) = (23,2) a__U31_A(x1,x2) = (20,3) a__U41_A(x1,x2,x3) = (18,46) a__plus_A(x1,x2) = (21,71) |0|_A() = (23,2) U31_A(x1,x2) = (1,1) U41_A(x1,x2,x3) = (1,1) precedence: a__U21# > plus > a__U11# = a__U12# = a__isNat# = a__isNatKind# = a__and# = mark# > U31 > a__isNat = a__U12 > U41 > a__plus > a__U31 = |0| > and = mark = U21 = a__and = a__U11 > tt = U13 = a__U13 > U11 > a__isNatKind > isNat > a__U41 > U22 = U12 = a__U21 = a__U22 > s = isNatKind partial status: pi(a__U11#) = [] pi(tt) = [] pi(a__U12#) = [2] pi(a__isNat) = [] pi(a__isNat#) = [] pi(s) = [] pi(a__isNatKind#) = [] pi(plus) = [2] pi(a__and#) = [] pi(a__isNatKind) = [] pi(isNatKind) = [] pi(mark#) = [1] pi(and) = [1] pi(mark) = [] pi(U22) = [] pi(U21) = [1] pi(a__U21#) = [] pi(a__and) = [] pi(U13) = [] pi(isNat) = [] pi(U12) = [1, 2] pi(U11) = [] pi(a__U11) = [] pi(a__U12) = [] pi(a__U13) = [1] pi(a__U21) = [1] pi(a__U22) = [] pi(a__U31) = [] pi(a__U41) = [] pi(a__plus) = [] pi(|0|) = [] pi(U31) = [] pi(U41) = [] The next rules are strictly ordered: p1, p7, p8, p10, p12, p13, p14, p16, p22, p24, p26, p27 We remove them from the problem. -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: a__U12#(tt(),V2) -> a__isNat#(V2) p2: a__isNat#(s(V1)) -> a__isNatKind#(V1) p3: a__isNatKind#(s(V1)) -> a__isNatKind#(V1) p4: a__isNatKind#(plus(V1,V2)) -> a__isNatKind#(V1) p5: a__isNatKind#(plus(V1,V2)) -> a__and#(a__isNatKind(V1),isNatKind(V2)) p6: mark#(isNatKind(X)) -> a__isNatKind#(X) p7: mark#(and(X1,X2)) -> a__and#(mark(X1),X2) p8: mark#(U21(X1,X2)) -> a__U21#(mark(X1),X2) p9: a__isNat#(s(V1)) -> a__U21#(a__isNatKind(V1),V1) p10: a__isNat#(plus(V1,V2)) -> a__isNatKind#(V1) p11: a__isNat#(plus(V1,V2)) -> a__and#(a__isNatKind(V1),isNatKind(V2)) p12: a__isNat#(plus(V1,V2)) -> a__U11#(a__and(a__isNatKind(V1),isNatKind(V2)),V1,V2) p13: a__U11#(tt(),V1,V2) -> a__isNat#(V1) p14: mark#(isNat(X)) -> a__isNat#(X) p15: mark#(U12(X1,X2)) -> a__U12#(mark(X1),X2) and R consists of: r1: a__U11(tt(),V1,V2) -> a__U12(a__isNat(V1),V2) r2: a__U12(tt(),V2) -> a__U13(a__isNat(V2)) r3: a__U13(tt()) -> tt() r4: a__U21(tt(),V1) -> a__U22(a__isNat(V1)) r5: a__U22(tt()) -> tt() r6: a__U31(tt(),N) -> mark(N) r7: a__U41(tt(),M,N) -> s(a__plus(mark(N),mark(M))) r8: a__and(tt(),X) -> mark(X) r9: a__isNat(|0|()) -> tt() r10: a__isNat(plus(V1,V2)) -> a__U11(a__and(a__isNatKind(V1),isNatKind(V2)),V1,V2) r11: a__isNat(s(V1)) -> a__U21(a__isNatKind(V1),V1) r12: a__isNatKind(|0|()) -> tt() r13: a__isNatKind(plus(V1,V2)) -> a__and(a__isNatKind(V1),isNatKind(V2)) r14: a__isNatKind(s(V1)) -> a__isNatKind(V1) r15: a__plus(N,|0|()) -> a__U31(a__and(a__isNat(N),isNatKind(N)),N) r16: a__plus(N,s(M)) -> a__U41(a__and(a__and(a__isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N) r17: mark(U11(X1,X2,X3)) -> a__U11(mark(X1),X2,X3) r18: mark(U12(X1,X2)) -> a__U12(mark(X1),X2) r19: mark(isNat(X)) -> a__isNat(X) r20: mark(U13(X)) -> a__U13(mark(X)) r21: mark(U21(X1,X2)) -> a__U21(mark(X1),X2) r22: mark(U22(X)) -> a__U22(mark(X)) r23: mark(U31(X1,X2)) -> a__U31(mark(X1),X2) r24: mark(U41(X1,X2,X3)) -> a__U41(mark(X1),X2,X3) r25: mark(plus(X1,X2)) -> a__plus(mark(X1),mark(X2)) r26: mark(and(X1,X2)) -> a__and(mark(X1),X2) r27: mark(isNatKind(X)) -> a__isNatKind(X) r28: mark(tt()) -> tt() r29: mark(s(X)) -> s(mark(X)) r30: mark(|0|()) -> |0|() r31: a__U11(X1,X2,X3) -> U11(X1,X2,X3) r32: a__U12(X1,X2) -> U12(X1,X2) r33: a__isNat(X) -> isNat(X) r34: a__U13(X) -> U13(X) r35: a__U21(X1,X2) -> U21(X1,X2) r36: a__U22(X) -> U22(X) r37: a__U31(X1,X2) -> U31(X1,X2) r38: a__U41(X1,X2,X3) -> U41(X1,X2,X3) r39: a__plus(X1,X2) -> plus(X1,X2) r40: a__and(X1,X2) -> and(X1,X2) r41: a__isNatKind(X) -> isNatKind(X) The estimated dependency graph contains the following SCCs: {p12, p13} {p3, p4} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: a__U11#(tt(),V1,V2) -> a__isNat#(V1) p2: a__isNat#(plus(V1,V2)) -> a__U11#(a__and(a__isNatKind(V1),isNatKind(V2)),V1,V2) and R consists of: r1: a__U11(tt(),V1,V2) -> a__U12(a__isNat(V1),V2) r2: a__U12(tt(),V2) -> a__U13(a__isNat(V2)) r3: a__U13(tt()) -> tt() r4: a__U21(tt(),V1) -> a__U22(a__isNat(V1)) r5: a__U22(tt()) -> tt() r6: a__U31(tt(),N) -> mark(N) r7: a__U41(tt(),M,N) -> s(a__plus(mark(N),mark(M))) r8: a__and(tt(),X) -> mark(X) r9: a__isNat(|0|()) -> tt() r10: a__isNat(plus(V1,V2)) -> a__U11(a__and(a__isNatKind(V1),isNatKind(V2)),V1,V2) r11: a__isNat(s(V1)) -> a__U21(a__isNatKind(V1),V1) r12: a__isNatKind(|0|()) -> tt() r13: a__isNatKind(plus(V1,V2)) -> a__and(a__isNatKind(V1),isNatKind(V2)) r14: a__isNatKind(s(V1)) -> a__isNatKind(V1) r15: a__plus(N,|0|()) -> a__U31(a__and(a__isNat(N),isNatKind(N)),N) r16: a__plus(N,s(M)) -> a__U41(a__and(a__and(a__isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N) r17: mark(U11(X1,X2,X3)) -> a__U11(mark(X1),X2,X3) r18: mark(U12(X1,X2)) -> a__U12(mark(X1),X2) r19: mark(isNat(X)) -> a__isNat(X) r20: mark(U13(X)) -> a__U13(mark(X)) r21: mark(U21(X1,X2)) -> a__U21(mark(X1),X2) r22: mark(U22(X)) -> a__U22(mark(X)) r23: mark(U31(X1,X2)) -> a__U31(mark(X1),X2) r24: mark(U41(X1,X2,X3)) -> a__U41(mark(X1),X2,X3) r25: mark(plus(X1,X2)) -> a__plus(mark(X1),mark(X2)) r26: mark(and(X1,X2)) -> a__and(mark(X1),X2) r27: mark(isNatKind(X)) -> a__isNatKind(X) r28: mark(tt()) -> tt() r29: mark(s(X)) -> s(mark(X)) r30: mark(|0|()) -> |0|() r31: a__U11(X1,X2,X3) -> U11(X1,X2,X3) r32: a__U12(X1,X2) -> U12(X1,X2) r33: a__isNat(X) -> isNat(X) r34: a__U13(X) -> U13(X) r35: a__U21(X1,X2) -> U21(X1,X2) r36: a__U22(X) -> U22(X) r37: a__U31(X1,X2) -> U31(X1,X2) r38: a__U41(X1,X2,X3) -> U41(X1,X2,X3) r39: a__plus(X1,X2) -> plus(X1,X2) r40: a__and(X1,X2) -> and(X1,X2) r41: a__isNatKind(X) -> isNatKind(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, r33, r34, r35, r36, r37, r38, r39, r40, r41 Take the reduction pair: lexicographic combination of reduction pairs: 1. weighted path order base order: matrix interpretations: carrier: N^2 order: lexicographic order interpretations: a__U11#_A(x1,x2,x3) = ((1,0),(1,1)) x2 + ((1,0),(0,0)) x3 + (42,10) tt_A() = (36,3) a__isNat#_A(x1) = ((1,0),(1,1)) x1 + (40,9) plus_A(x1,x2) = x1 + ((1,0),(1,1)) x2 + (43,0) a__and_A(x1,x2) = x2 + (3,18) a__isNatKind_A(x1) = ((1,0),(1,1)) x1 + (28,52) isNatKind_A(x1) = ((1,0),(1,1)) x1 + (28,15) a__U11_A(x1,x2,x3) = ((1,0),(0,0)) x1 + x2 + (0,16) a__U12_A(x1,x2) = ((1,0),(0,0)) x1 + (2,4) a__isNat_A(x1) = x1 + (6,17) a__U13_A(x1) = (37,2) a__U21_A(x1,x2) = ((1,0),(0,0)) x2 + (9,35) a__U22_A(x1) = x1 + (2,2) a__U31_A(x1,x2) = ((1,0),(1,1)) x2 + (31,35) mark_A(x1) = ((1,0),(1,1)) x1 + (0,15) a__U41_A(x1,x2,x3) = ((1,0),(0,0)) x2 + ((1,0),(0,0)) x3 + (78,35) s_A(x1) = ((1,0),(0,0)) x1 + (35,34) a__plus_A(x1,x2) = x1 + ((1,0),(1,1)) x2 + (43,4) |0|_A() = (30,0) and_A(x1,x2) = x2 + (3,0) isNat_A(x1) = x1 + (6,0) U11_A(x1,x2,x3) = ((1,0),(0,0)) x1 + x2 + (0,16) U12_A(x1,x2) = ((1,0),(0,0)) x1 + (2,3) U13_A(x1) = (37,1) U21_A(x1,x2) = ((1,0),(0,0)) x2 + (9,16) U22_A(x1) = x1 + (2,1) U31_A(x1,x2) = x2 + (31,0) U41_A(x1,x2,x3) = ((1,0),(0,0)) x2 + ((1,0),(0,0)) x3 + (78,16) precedence: U22 > a__and = a__isNatKind = isNatKind = a__U31 = mark = a__U41 = |0| = and = U31 = U41 > a__isNat > a__U11 = U11 > a__U12 = a__U21 = U12 > a__U11# = tt = a__isNat# = plus = a__U13 = a__U22 = s = a__plus = isNat = U21 > U13 partial status: pi(a__U11#) = [] pi(tt) = [] pi(a__isNat#) = [] pi(plus) = [] pi(a__and) = [] pi(a__isNatKind) = [1] pi(isNatKind) = [] pi(a__U11) = [2] pi(a__U12) = [] pi(a__isNat) = [] pi(a__U13) = [] pi(a__U21) = [] pi(a__U22) = [] pi(a__U31) = [2] pi(mark) = [1] pi(a__U41) = [] pi(s) = [] pi(a__plus) = [] pi(|0|) = [] pi(and) = [] pi(isNat) = [1] pi(U11) = [] pi(U12) = [] pi(U13) = [] pi(U21) = [] pi(U22) = [1] pi(U31) = [] pi(U41) = [] 2. weighted path order base order: matrix interpretations: carrier: N^2 order: lexicographic order interpretations: a__U11#_A(x1,x2,x3) = (8,18) tt_A() = (4,14) a__isNat#_A(x1) = (3,17) plus_A(x1,x2) = (7,1) a__and_A(x1,x2) = (2,16) a__isNatKind_A(x1) = ((1,0),(1,1)) x1 + (4,4) isNatKind_A(x1) = (1,13) a__U11_A(x1,x2,x3) = ((0,0),(1,0)) x2 + (6,18) a__U12_A(x1,x2) = (5,17) a__isNat_A(x1) = (8,3) a__U13_A(x1) = (4,16) a__U21_A(x1,x2) = (7,2) a__U22_A(x1) = (5,1) a__U31_A(x1,x2) = (2,5) mark_A(x1) = (9,15) a__U41_A(x1,x2,x3) = (7,13) s_A(x1) = (0,0) a__plus_A(x1,x2) = (8,0) |0|_A() = (5,4) and_A(x1,x2) = (1,0) isNat_A(x1) = ((0,0),(1,0)) x1 + (0,1) U11_A(x1,x2,x3) = (0,1) U12_A(x1,x2) = (6,1) U13_A(x1) = (0,1) U21_A(x1,x2) = (0,1) U22_A(x1) = (6,16) U31_A(x1,x2) = (1,0) U41_A(x1,x2,x3) = (6,14) precedence: U41 > mark > a__U21 > a__U11# > isNatKind > a__plus > a__U41 > U21 = U31 > a__isNat# > a__U31 > tt = a__U11 = a__isNat = |0| > U11 > a__isNatKind > plus = a__and = and > s = isNat > a__U22 > a__U12 = a__U13 = U12 = U13 = U22 partial status: pi(a__U11#) = [] pi(tt) = [] pi(a__isNat#) = [] pi(plus) = [] pi(a__and) = [] pi(a__isNatKind) = [1] pi(isNatKind) = [] pi(a__U11) = [] pi(a__U12) = [] pi(a__isNat) = [] pi(a__U13) = [] pi(a__U21) = [] pi(a__U22) = [] pi(a__U31) = [] pi(mark) = [] pi(a__U41) = [] pi(s) = [] pi(a__plus) = [] pi(|0|) = [] pi(and) = [] pi(isNat) = [] pi(U11) = [] pi(U12) = [] pi(U13) = [] pi(U21) = [] pi(U22) = [] pi(U31) = [] pi(U41) = [] The next rules are strictly ordered: p1, p2 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: a__isNatKind#(s(V1)) -> a__isNatKind#(V1) p2: a__isNatKind#(plus(V1,V2)) -> a__isNatKind#(V1) and R consists of: r1: a__U11(tt(),V1,V2) -> a__U12(a__isNat(V1),V2) r2: a__U12(tt(),V2) -> a__U13(a__isNat(V2)) r3: a__U13(tt()) -> tt() r4: a__U21(tt(),V1) -> a__U22(a__isNat(V1)) r5: a__U22(tt()) -> tt() r6: a__U31(tt(),N) -> mark(N) r7: a__U41(tt(),M,N) -> s(a__plus(mark(N),mark(M))) r8: a__and(tt(),X) -> mark(X) r9: a__isNat(|0|()) -> tt() r10: a__isNat(plus(V1,V2)) -> a__U11(a__and(a__isNatKind(V1),isNatKind(V2)),V1,V2) r11: a__isNat(s(V1)) -> a__U21(a__isNatKind(V1),V1) r12: a__isNatKind(|0|()) -> tt() r13: a__isNatKind(plus(V1,V2)) -> a__and(a__isNatKind(V1),isNatKind(V2)) r14: a__isNatKind(s(V1)) -> a__isNatKind(V1) r15: a__plus(N,|0|()) -> a__U31(a__and(a__isNat(N),isNatKind(N)),N) r16: a__plus(N,s(M)) -> a__U41(a__and(a__and(a__isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N) r17: mark(U11(X1,X2,X3)) -> a__U11(mark(X1),X2,X3) r18: mark(U12(X1,X2)) -> a__U12(mark(X1),X2) r19: mark(isNat(X)) -> a__isNat(X) r20: mark(U13(X)) -> a__U13(mark(X)) r21: mark(U21(X1,X2)) -> a__U21(mark(X1),X2) r22: mark(U22(X)) -> a__U22(mark(X)) r23: mark(U31(X1,X2)) -> a__U31(mark(X1),X2) r24: mark(U41(X1,X2,X3)) -> a__U41(mark(X1),X2,X3) r25: mark(plus(X1,X2)) -> a__plus(mark(X1),mark(X2)) r26: mark(and(X1,X2)) -> a__and(mark(X1),X2) r27: mark(isNatKind(X)) -> a__isNatKind(X) r28: mark(tt()) -> tt() r29: mark(s(X)) -> s(mark(X)) r30: mark(|0|()) -> |0|() r31: a__U11(X1,X2,X3) -> U11(X1,X2,X3) r32: a__U12(X1,X2) -> U12(X1,X2) r33: a__isNat(X) -> isNat(X) r34: a__U13(X) -> U13(X) r35: a__U21(X1,X2) -> U21(X1,X2) r36: a__U22(X) -> U22(X) r37: a__U31(X1,X2) -> U31(X1,X2) r38: a__U41(X1,X2,X3) -> U41(X1,X2,X3) r39: a__plus(X1,X2) -> plus(X1,X2) r40: a__and(X1,X2) -> and(X1,X2) r41: a__isNatKind(X) -> isNatKind(X) The set of usable rules consists of (no rules) Take the reduction pair: lexicographic combination of reduction pairs: 1. weighted path order base order: matrix interpretations: carrier: N^2 order: lexicographic order interpretations: a__isNatKind#_A(x1) = x1 + (2,2) s_A(x1) = x1 + (1,3) plus_A(x1,x2) = ((1,0),(1,0)) x1 + x2 + (3,1) precedence: a__isNatKind# = s = plus partial status: pi(a__isNatKind#) = [1] pi(s) = [1] pi(plus) = [2] 2. weighted path order base order: matrix interpretations: carrier: N^2 order: lexicographic order interpretations: a__isNatKind#_A(x1) = x1 s_A(x1) = x1 + (1,1) plus_A(x1,x2) = x2 + (1,1) precedence: plus > s > a__isNatKind# partial status: pi(a__isNatKind#) = [] pi(s) = [] pi(plus) = [] The next rules are strictly ordered: p2 We remove them from the problem. -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: a__isNatKind#(s(V1)) -> a__isNatKind#(V1) and R consists of: r1: a__U11(tt(),V1,V2) -> a__U12(a__isNat(V1),V2) r2: a__U12(tt(),V2) -> a__U13(a__isNat(V2)) r3: a__U13(tt()) -> tt() r4: a__U21(tt(),V1) -> a__U22(a__isNat(V1)) r5: a__U22(tt()) -> tt() r6: a__U31(tt(),N) -> mark(N) r7: a__U41(tt(),M,N) -> s(a__plus(mark(N),mark(M))) r8: a__and(tt(),X) -> mark(X) r9: a__isNat(|0|()) -> tt() r10: a__isNat(plus(V1,V2)) -> a__U11(a__and(a__isNatKind(V1),isNatKind(V2)),V1,V2) r11: a__isNat(s(V1)) -> a__U21(a__isNatKind(V1),V1) r12: a__isNatKind(|0|()) -> tt() r13: a__isNatKind(plus(V1,V2)) -> a__and(a__isNatKind(V1),isNatKind(V2)) r14: a__isNatKind(s(V1)) -> a__isNatKind(V1) r15: a__plus(N,|0|()) -> a__U31(a__and(a__isNat(N),isNatKind(N)),N) r16: a__plus(N,s(M)) -> a__U41(a__and(a__and(a__isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N) r17: mark(U11(X1,X2,X3)) -> a__U11(mark(X1),X2,X3) r18: mark(U12(X1,X2)) -> a__U12(mark(X1),X2) r19: mark(isNat(X)) -> a__isNat(X) r20: mark(U13(X)) -> a__U13(mark(X)) r21: mark(U21(X1,X2)) -> a__U21(mark(X1),X2) r22: mark(U22(X)) -> a__U22(mark(X)) r23: mark(U31(X1,X2)) -> a__U31(mark(X1),X2) r24: mark(U41(X1,X2,X3)) -> a__U41(mark(X1),X2,X3) r25: mark(plus(X1,X2)) -> a__plus(mark(X1),mark(X2)) r26: mark(and(X1,X2)) -> a__and(mark(X1),X2) r27: mark(isNatKind(X)) -> a__isNatKind(X) r28: mark(tt()) -> tt() r29: mark(s(X)) -> s(mark(X)) r30: mark(|0|()) -> |0|() r31: a__U11(X1,X2,X3) -> U11(X1,X2,X3) r32: a__U12(X1,X2) -> U12(X1,X2) r33: a__isNat(X) -> isNat(X) r34: a__U13(X) -> U13(X) r35: a__U21(X1,X2) -> U21(X1,X2) r36: a__U22(X) -> U22(X) r37: a__U31(X1,X2) -> U31(X1,X2) r38: a__U41(X1,X2,X3) -> U41(X1,X2,X3) r39: a__plus(X1,X2) -> plus(X1,X2) r40: a__and(X1,X2) -> and(X1,X2) r41: a__isNatKind(X) -> isNatKind(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__isNatKind#(s(V1)) -> a__isNatKind#(V1) and R consists of: r1: a__U11(tt(),V1,V2) -> a__U12(a__isNat(V1),V2) r2: a__U12(tt(),V2) -> a__U13(a__isNat(V2)) r3: a__U13(tt()) -> tt() r4: a__U21(tt(),V1) -> a__U22(a__isNat(V1)) r5: a__U22(tt()) -> tt() r6: a__U31(tt(),N) -> mark(N) r7: a__U41(tt(),M,N) -> s(a__plus(mark(N),mark(M))) r8: a__and(tt(),X) -> mark(X) r9: a__isNat(|0|()) -> tt() r10: a__isNat(plus(V1,V2)) -> a__U11(a__and(a__isNatKind(V1),isNatKind(V2)),V1,V2) r11: a__isNat(s(V1)) -> a__U21(a__isNatKind(V1),V1) r12: a__isNatKind(|0|()) -> tt() r13: a__isNatKind(plus(V1,V2)) -> a__and(a__isNatKind(V1),isNatKind(V2)) r14: a__isNatKind(s(V1)) -> a__isNatKind(V1) r15: a__plus(N,|0|()) -> a__U31(a__and(a__isNat(N),isNatKind(N)),N) r16: a__plus(N,s(M)) -> a__U41(a__and(a__and(a__isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N) r17: mark(U11(X1,X2,X3)) -> a__U11(mark(X1),X2,X3) r18: mark(U12(X1,X2)) -> a__U12(mark(X1),X2) r19: mark(isNat(X)) -> a__isNat(X) r20: mark(U13(X)) -> a__U13(mark(X)) r21: mark(U21(X1,X2)) -> a__U21(mark(X1),X2) r22: mark(U22(X)) -> a__U22(mark(X)) r23: mark(U31(X1,X2)) -> a__U31(mark(X1),X2) r24: mark(U41(X1,X2,X3)) -> a__U41(mark(X1),X2,X3) r25: mark(plus(X1,X2)) -> a__plus(mark(X1),mark(X2)) r26: mark(and(X1,X2)) -> a__and(mark(X1),X2) r27: mark(isNatKind(X)) -> a__isNatKind(X) r28: mark(tt()) -> tt() r29: mark(s(X)) -> s(mark(X)) r30: mark(|0|()) -> |0|() r31: a__U11(X1,X2,X3) -> U11(X1,X2,X3) r32: a__U12(X1,X2) -> U12(X1,X2) r33: a__isNat(X) -> isNat(X) r34: a__U13(X) -> U13(X) r35: a__U21(X1,X2) -> U21(X1,X2) r36: a__U22(X) -> U22(X) r37: a__U31(X1,X2) -> U31(X1,X2) r38: a__U41(X1,X2,X3) -> U41(X1,X2,X3) r39: a__plus(X1,X2) -> plus(X1,X2) r40: a__and(X1,X2) -> and(X1,X2) r41: a__isNatKind(X) -> isNatKind(X) The set of usable rules consists of (no rules) Take the reduction pair: lexicographic combination of reduction pairs: 1. weighted path order base order: matrix interpretations: carrier: N^2 order: lexicographic order interpretations: a__isNatKind#_A(x1) = ((1,0),(1,1)) x1 + (2,2) s_A(x1) = ((1,0),(0,0)) x1 + (1,1) precedence: a__isNatKind# = s partial status: pi(a__isNatKind#) = [] pi(s) = [] 2. weighted path order base order: matrix interpretations: carrier: N^2 order: lexicographic order interpretations: a__isNatKind#_A(x1) = ((1,0),(0,0)) x1 s_A(x1) = (1,1) precedence: s > a__isNatKind# partial status: pi(a__isNatKind#) = [] pi(s) = [] The next rules are strictly ordered: p1 We remove them from the problem. Then no dependency pair remains.