YES We show the termination of the TRS R: U11(tt(),V1,V2) -> U12(isNatKind(activate(V1)),activate(V1),activate(V2)) U12(tt(),V1,V2) -> U13(isNatKind(activate(V2)),activate(V1),activate(V2)) U13(tt(),V1,V2) -> U14(isNatKind(activate(V2)),activate(V1),activate(V2)) U14(tt(),V1,V2) -> U15(isNat(activate(V1)),activate(V2)) U15(tt(),V2) -> U16(isNat(activate(V2))) U16(tt()) -> tt() U21(tt(),V1) -> U22(isNatKind(activate(V1)),activate(V1)) U22(tt(),V1) -> U23(isNat(activate(V1))) U23(tt()) -> tt() U31(tt(),V2) -> U32(isNatKind(activate(V2))) U32(tt()) -> tt() U41(tt()) -> tt() U51(tt(),N) -> U52(isNatKind(activate(N)),activate(N)) U52(tt(),N) -> activate(N) U61(tt(),M,N) -> U62(isNatKind(activate(M)),activate(M),activate(N)) U62(tt(),M,N) -> U63(isNat(activate(N)),activate(M),activate(N)) U63(tt(),M,N) -> U64(isNatKind(activate(N)),activate(M),activate(N)) U64(tt(),M,N) -> s(plus(activate(N),activate(M))) isNat(n__0()) -> tt() isNat(n__plus(V1,V2)) -> U11(isNatKind(activate(V1)),activate(V1),activate(V2)) isNat(n__s(V1)) -> U21(isNatKind(activate(V1)),activate(V1)) isNatKind(n__0()) -> tt() isNatKind(n__plus(V1,V2)) -> U31(isNatKind(activate(V1)),activate(V2)) isNatKind(n__s(V1)) -> U41(isNatKind(activate(V1))) plus(N,|0|()) -> U51(isNat(N),N) plus(N,s(M)) -> U61(isNat(M),M,N) |0|() -> n__0() plus(X1,X2) -> n__plus(X1,X2) s(X) -> n__s(X) activate(n__0()) -> |0|() activate(n__plus(X1,X2)) -> plus(activate(X1),activate(X2)) activate(n__s(X)) -> s(activate(X)) activate(X) -> X -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: U11#(tt(),V1,V2) -> U12#(isNatKind(activate(V1)),activate(V1),activate(V2)) p2: U11#(tt(),V1,V2) -> isNatKind#(activate(V1)) p3: U11#(tt(),V1,V2) -> activate#(V1) p4: U11#(tt(),V1,V2) -> activate#(V2) p5: U12#(tt(),V1,V2) -> U13#(isNatKind(activate(V2)),activate(V1),activate(V2)) p6: U12#(tt(),V1,V2) -> isNatKind#(activate(V2)) p7: U12#(tt(),V1,V2) -> activate#(V2) p8: U12#(tt(),V1,V2) -> activate#(V1) p9: U13#(tt(),V1,V2) -> U14#(isNatKind(activate(V2)),activate(V1),activate(V2)) p10: U13#(tt(),V1,V2) -> isNatKind#(activate(V2)) p11: U13#(tt(),V1,V2) -> activate#(V2) p12: U13#(tt(),V1,V2) -> activate#(V1) p13: U14#(tt(),V1,V2) -> U15#(isNat(activate(V1)),activate(V2)) p14: U14#(tt(),V1,V2) -> isNat#(activate(V1)) p15: U14#(tt(),V1,V2) -> activate#(V1) p16: U14#(tt(),V1,V2) -> activate#(V2) p17: U15#(tt(),V2) -> U16#(isNat(activate(V2))) p18: U15#(tt(),V2) -> isNat#(activate(V2)) p19: U15#(tt(),V2) -> activate#(V2) p20: U21#(tt(),V1) -> U22#(isNatKind(activate(V1)),activate(V1)) p21: U21#(tt(),V1) -> isNatKind#(activate(V1)) p22: U21#(tt(),V1) -> activate#(V1) p23: U22#(tt(),V1) -> U23#(isNat(activate(V1))) p24: U22#(tt(),V1) -> isNat#(activate(V1)) p25: U22#(tt(),V1) -> activate#(V1) p26: U31#(tt(),V2) -> U32#(isNatKind(activate(V2))) p27: U31#(tt(),V2) -> isNatKind#(activate(V2)) p28: U31#(tt(),V2) -> activate#(V2) p29: U51#(tt(),N) -> U52#(isNatKind(activate(N)),activate(N)) p30: U51#(tt(),N) -> isNatKind#(activate(N)) p31: U51#(tt(),N) -> activate#(N) p32: U52#(tt(),N) -> activate#(N) p33: U61#(tt(),M,N) -> U62#(isNatKind(activate(M)),activate(M),activate(N)) p34: U61#(tt(),M,N) -> isNatKind#(activate(M)) p35: U61#(tt(),M,N) -> activate#(M) p36: U61#(tt(),M,N) -> activate#(N) p37: U62#(tt(),M,N) -> U63#(isNat(activate(N)),activate(M),activate(N)) p38: U62#(tt(),M,N) -> isNat#(activate(N)) p39: U62#(tt(),M,N) -> activate#(N) p40: U62#(tt(),M,N) -> activate#(M) p41: U63#(tt(),M,N) -> U64#(isNatKind(activate(N)),activate(M),activate(N)) p42: U63#(tt(),M,N) -> isNatKind#(activate(N)) p43: U63#(tt(),M,N) -> activate#(N) p44: U63#(tt(),M,N) -> activate#(M) p45: U64#(tt(),M,N) -> s#(plus(activate(N),activate(M))) p46: U64#(tt(),M,N) -> plus#(activate(N),activate(M)) p47: U64#(tt(),M,N) -> activate#(N) p48: U64#(tt(),M,N) -> activate#(M) p49: isNat#(n__plus(V1,V2)) -> U11#(isNatKind(activate(V1)),activate(V1),activate(V2)) p50: isNat#(n__plus(V1,V2)) -> isNatKind#(activate(V1)) p51: isNat#(n__plus(V1,V2)) -> activate#(V1) p52: isNat#(n__plus(V1,V2)) -> activate#(V2) p53: isNat#(n__s(V1)) -> U21#(isNatKind(activate(V1)),activate(V1)) p54: isNat#(n__s(V1)) -> isNatKind#(activate(V1)) p55: isNat#(n__s(V1)) -> activate#(V1) p56: isNatKind#(n__plus(V1,V2)) -> U31#(isNatKind(activate(V1)),activate(V2)) p57: isNatKind#(n__plus(V1,V2)) -> isNatKind#(activate(V1)) p58: isNatKind#(n__plus(V1,V2)) -> activate#(V1) p59: isNatKind#(n__plus(V1,V2)) -> activate#(V2) p60: isNatKind#(n__s(V1)) -> U41#(isNatKind(activate(V1))) p61: isNatKind#(n__s(V1)) -> isNatKind#(activate(V1)) p62: isNatKind#(n__s(V1)) -> activate#(V1) p63: plus#(N,|0|()) -> U51#(isNat(N),N) p64: plus#(N,|0|()) -> isNat#(N) p65: plus#(N,s(M)) -> U61#(isNat(M),M,N) p66: plus#(N,s(M)) -> isNat#(M) p67: activate#(n__0()) -> |0|#() p68: activate#(n__plus(X1,X2)) -> plus#(activate(X1),activate(X2)) p69: activate#(n__plus(X1,X2)) -> activate#(X1) p70: activate#(n__plus(X1,X2)) -> activate#(X2) p71: activate#(n__s(X)) -> s#(activate(X)) p72: activate#(n__s(X)) -> activate#(X) and R consists of: r1: U11(tt(),V1,V2) -> U12(isNatKind(activate(V1)),activate(V1),activate(V2)) r2: U12(tt(),V1,V2) -> U13(isNatKind(activate(V2)),activate(V1),activate(V2)) r3: U13(tt(),V1,V2) -> U14(isNatKind(activate(V2)),activate(V1),activate(V2)) r4: U14(tt(),V1,V2) -> U15(isNat(activate(V1)),activate(V2)) r5: U15(tt(),V2) -> U16(isNat(activate(V2))) r6: U16(tt()) -> tt() r7: U21(tt(),V1) -> U22(isNatKind(activate(V1)),activate(V1)) r8: U22(tt(),V1) -> U23(isNat(activate(V1))) r9: U23(tt()) -> tt() r10: U31(tt(),V2) -> U32(isNatKind(activate(V2))) r11: U32(tt()) -> tt() r12: U41(tt()) -> tt() r13: U51(tt(),N) -> U52(isNatKind(activate(N)),activate(N)) r14: U52(tt(),N) -> activate(N) r15: U61(tt(),M,N) -> U62(isNatKind(activate(M)),activate(M),activate(N)) r16: U62(tt(),M,N) -> U63(isNat(activate(N)),activate(M),activate(N)) r17: U63(tt(),M,N) -> U64(isNatKind(activate(N)),activate(M),activate(N)) r18: U64(tt(),M,N) -> s(plus(activate(N),activate(M))) r19: isNat(n__0()) -> tt() r20: isNat(n__plus(V1,V2)) -> U11(isNatKind(activate(V1)),activate(V1),activate(V2)) r21: isNat(n__s(V1)) -> U21(isNatKind(activate(V1)),activate(V1)) r22: isNatKind(n__0()) -> tt() r23: isNatKind(n__plus(V1,V2)) -> U31(isNatKind(activate(V1)),activate(V2)) r24: isNatKind(n__s(V1)) -> U41(isNatKind(activate(V1))) r25: plus(N,|0|()) -> U51(isNat(N),N) r26: plus(N,s(M)) -> U61(isNat(M),M,N) r27: |0|() -> n__0() r28: plus(X1,X2) -> n__plus(X1,X2) r29: s(X) -> n__s(X) r30: activate(n__0()) -> |0|() r31: activate(n__plus(X1,X2)) -> plus(activate(X1),activate(X2)) r32: activate(n__s(X)) -> s(activate(X)) r33: activate(X) -> 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, p18, p19, p20, p21, p22, p24, p25, p27, p28, p29, p30, p31, p32, p33, p34, p35, p36, p37, p38, p39, p40, p41, p42, p43, p44, p46, p47, p48, p49, p50, p51, p52, p53, p54, p55, p56, p57, p58, p59, p61, p62, p63, p64, p65, p66, p68, p69, p70, p72} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: U11#(tt(),V1,V2) -> U12#(isNatKind(activate(V1)),activate(V1),activate(V2)) p2: U12#(tt(),V1,V2) -> activate#(V1) p3: activate#(n__s(X)) -> activate#(X) p4: activate#(n__plus(X1,X2)) -> activate#(X2) p5: activate#(n__plus(X1,X2)) -> activate#(X1) p6: activate#(n__plus(X1,X2)) -> plus#(activate(X1),activate(X2)) p7: plus#(N,s(M)) -> isNat#(M) p8: isNat#(n__s(V1)) -> activate#(V1) p9: isNat#(n__s(V1)) -> isNatKind#(activate(V1)) p10: isNatKind#(n__s(V1)) -> activate#(V1) p11: isNatKind#(n__s(V1)) -> isNatKind#(activate(V1)) p12: isNatKind#(n__plus(V1,V2)) -> activate#(V2) p13: isNatKind#(n__plus(V1,V2)) -> activate#(V1) p14: isNatKind#(n__plus(V1,V2)) -> isNatKind#(activate(V1)) p15: isNatKind#(n__plus(V1,V2)) -> U31#(isNatKind(activate(V1)),activate(V2)) p16: U31#(tt(),V2) -> activate#(V2) p17: U31#(tt(),V2) -> isNatKind#(activate(V2)) p18: isNat#(n__s(V1)) -> U21#(isNatKind(activate(V1)),activate(V1)) p19: U21#(tt(),V1) -> activate#(V1) p20: U21#(tt(),V1) -> isNatKind#(activate(V1)) p21: U21#(tt(),V1) -> U22#(isNatKind(activate(V1)),activate(V1)) p22: U22#(tt(),V1) -> activate#(V1) p23: U22#(tt(),V1) -> isNat#(activate(V1)) p24: isNat#(n__plus(V1,V2)) -> activate#(V2) p25: isNat#(n__plus(V1,V2)) -> activate#(V1) p26: isNat#(n__plus(V1,V2)) -> isNatKind#(activate(V1)) p27: isNat#(n__plus(V1,V2)) -> U11#(isNatKind(activate(V1)),activate(V1),activate(V2)) p28: U11#(tt(),V1,V2) -> activate#(V2) p29: U11#(tt(),V1,V2) -> activate#(V1) p30: U11#(tt(),V1,V2) -> isNatKind#(activate(V1)) p31: plus#(N,s(M)) -> U61#(isNat(M),M,N) p32: U61#(tt(),M,N) -> activate#(N) p33: U61#(tt(),M,N) -> activate#(M) p34: U61#(tt(),M,N) -> isNatKind#(activate(M)) p35: U61#(tt(),M,N) -> U62#(isNatKind(activate(M)),activate(M),activate(N)) p36: U62#(tt(),M,N) -> activate#(M) p37: U62#(tt(),M,N) -> activate#(N) p38: U62#(tt(),M,N) -> isNat#(activate(N)) p39: U62#(tt(),M,N) -> U63#(isNat(activate(N)),activate(M),activate(N)) p40: U63#(tt(),M,N) -> activate#(M) p41: U63#(tt(),M,N) -> activate#(N) p42: U63#(tt(),M,N) -> isNatKind#(activate(N)) p43: U63#(tt(),M,N) -> U64#(isNatKind(activate(N)),activate(M),activate(N)) p44: U64#(tt(),M,N) -> activate#(M) p45: U64#(tt(),M,N) -> activate#(N) p46: U64#(tt(),M,N) -> plus#(activate(N),activate(M)) p47: plus#(N,|0|()) -> isNat#(N) p48: plus#(N,|0|()) -> U51#(isNat(N),N) p49: U51#(tt(),N) -> activate#(N) p50: U51#(tt(),N) -> isNatKind#(activate(N)) p51: U51#(tt(),N) -> U52#(isNatKind(activate(N)),activate(N)) p52: U52#(tt(),N) -> activate#(N) p53: U12#(tt(),V1,V2) -> activate#(V2) p54: U12#(tt(),V1,V2) -> isNatKind#(activate(V2)) p55: U12#(tt(),V1,V2) -> U13#(isNatKind(activate(V2)),activate(V1),activate(V2)) p56: U13#(tt(),V1,V2) -> activate#(V1) p57: U13#(tt(),V1,V2) -> activate#(V2) p58: U13#(tt(),V1,V2) -> isNatKind#(activate(V2)) p59: U13#(tt(),V1,V2) -> U14#(isNatKind(activate(V2)),activate(V1),activate(V2)) p60: U14#(tt(),V1,V2) -> activate#(V2) p61: U14#(tt(),V1,V2) -> activate#(V1) p62: U14#(tt(),V1,V2) -> isNat#(activate(V1)) p63: U14#(tt(),V1,V2) -> U15#(isNat(activate(V1)),activate(V2)) p64: U15#(tt(),V2) -> activate#(V2) p65: U15#(tt(),V2) -> isNat#(activate(V2)) and R consists of: r1: U11(tt(),V1,V2) -> U12(isNatKind(activate(V1)),activate(V1),activate(V2)) r2: U12(tt(),V1,V2) -> U13(isNatKind(activate(V2)),activate(V1),activate(V2)) r3: U13(tt(),V1,V2) -> U14(isNatKind(activate(V2)),activate(V1),activate(V2)) r4: U14(tt(),V1,V2) -> U15(isNat(activate(V1)),activate(V2)) r5: U15(tt(),V2) -> U16(isNat(activate(V2))) r6: U16(tt()) -> tt() r7: U21(tt(),V1) -> U22(isNatKind(activate(V1)),activate(V1)) r8: U22(tt(),V1) -> U23(isNat(activate(V1))) r9: U23(tt()) -> tt() r10: U31(tt(),V2) -> U32(isNatKind(activate(V2))) r11: U32(tt()) -> tt() r12: U41(tt()) -> tt() r13: U51(tt(),N) -> U52(isNatKind(activate(N)),activate(N)) r14: U52(tt(),N) -> activate(N) r15: U61(tt(),M,N) -> U62(isNatKind(activate(M)),activate(M),activate(N)) r16: U62(tt(),M,N) -> U63(isNat(activate(N)),activate(M),activate(N)) r17: U63(tt(),M,N) -> U64(isNatKind(activate(N)),activate(M),activate(N)) r18: U64(tt(),M,N) -> s(plus(activate(N),activate(M))) r19: isNat(n__0()) -> tt() r20: isNat(n__plus(V1,V2)) -> U11(isNatKind(activate(V1)),activate(V1),activate(V2)) r21: isNat(n__s(V1)) -> U21(isNatKind(activate(V1)),activate(V1)) r22: isNatKind(n__0()) -> tt() r23: isNatKind(n__plus(V1,V2)) -> U31(isNatKind(activate(V1)),activate(V2)) r24: isNatKind(n__s(V1)) -> U41(isNatKind(activate(V1))) r25: plus(N,|0|()) -> U51(isNat(N),N) r26: plus(N,s(M)) -> U61(isNat(M),M,N) r27: |0|() -> n__0() r28: plus(X1,X2) -> n__plus(X1,X2) r29: s(X) -> n__s(X) r30: activate(n__0()) -> |0|() r31: activate(n__plus(X1,X2)) -> plus(activate(X1),activate(X2)) r32: activate(n__s(X)) -> s(activate(X)) r33: activate(X) -> 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 Take the reduction pair: weighted path order base order: matrix interpretations: carrier: N^1 order: lexicographic order interpretations: U11#_A(x1,x2,x3) = x2 + x3 + 16 tt_A() = 20 U12#_A(x1,x2,x3) = x2 + x3 + 15 isNatKind_A(x1) = x1 + 17 activate_A(x1) = x1 activate#_A(x1) = x1 n__s_A(x1) = x1 + 10 n__plus_A(x1,x2) = x1 + x2 + 23 plus#_A(x1,x2) = x1 + x2 + 14 s_A(x1) = x1 + 10 isNat#_A(x1) = x1 + 11 isNatKind#_A(x1) = x1 + 10 U31#_A(x1,x2) = x2 + 11 U21#_A(x1,x2) = x2 + 16 U22#_A(x1,x2) = x2 + 12 U61#_A(x1,x2,x3) = x2 + x3 + 20 isNat_A(x1) = x1 + 14 U62#_A(x1,x2,x3) = x2 + x3 + 19 U63#_A(x1,x2,x3) = x2 + x3 + 16 U64#_A(x1,x2,x3) = x2 + x3 + 15 |0|_A() = 21 U51#_A(x1,x2) = x2 + 22 U52#_A(x1,x2) = x2 + 1 U13#_A(x1,x2,x3) = x2 + x3 + 14 U14#_A(x1,x2,x3) = x2 + x3 + 13 U15#_A(x1,x2) = x2 + 12 U16_A(x1) = x1 + 7 U15_A(x1,x2) = x1 + x2 + 2 U64_A(x1,x2,x3) = x2 + x3 + 33 plus_A(x1,x2) = x1 + x2 + 23 U14_A(x1,x2,x3) = x2 + x3 + 17 U63_A(x1,x2,x3) = x2 + x3 + 33 U13_A(x1,x2,x3) = x2 + x3 + 18 U23_A(x1) = 21 U52_A(x1,x2) = x2 + 1 U62_A(x1,x2,x3) = x2 + x3 + 33 U12_A(x1,x2,x3) = x2 + x3 + 19 U22_A(x1,x2) = 22 U32_A(x1) = 21 U51_A(x1,x2) = x2 + 18 U61_A(x1,x2,x3) = x2 + x3 + 33 U11_A(x1,x2,x3) = x2 + x3 + 20 U21_A(x1,x2) = 23 U31_A(x1,x2) = 22 U41_A(x1) = x1 + 1 n__0_A() = 21 precedence: isNatKind = isNatKind# = U31# > plus# = isNat = U63# = U64# = U51# = U52# = U52 > U22# > U61# > U12 = U11 = U41 > U23 = U22 > U21 > U14 = U13 > U16 = U15 > U51 > U32 > |0| = U31 = n__0 > tt > n__plus = plus = U62 = U61 > activate > U15# > isNat# > U21# > U62# > activate# > U11# = U12# = U13# = U14# > n__s = s = U64 = U63 partial status: pi(U11#) = [] pi(tt) = [] pi(U12#) = [] pi(isNatKind) = [] pi(activate) = [1] pi(activate#) = [1] pi(n__s) = [] pi(n__plus) = [] pi(plus#) = [] pi(s) = [] pi(isNat#) = [] pi(isNatKind#) = [] pi(U31#) = [] pi(U21#) = [] pi(U22#) = [2] pi(U61#) = [] pi(isNat) = [1] pi(U62#) = [] pi(U63#) = [] pi(U64#) = [] pi(|0|) = [] pi(U51#) = [] pi(U52#) = [] pi(U13#) = [] pi(U14#) = [] pi(U15#) = [] pi(U16) = [] pi(U15) = [] pi(U64) = [] pi(plus) = [] pi(U14) = [] pi(U63) = [3] pi(U13) = [] pi(U23) = [] pi(U52) = [] pi(U62) = [] pi(U12) = [] pi(U22) = [] pi(U32) = [] pi(U51) = [] pi(U61) = [] pi(U11) = [2, 3] pi(U21) = [] pi(U31) = [] pi(U41) = [] pi(n__0) = [] The next rules are strictly ordered: p53 We remove them from the problem. -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: U11#(tt(),V1,V2) -> U12#(isNatKind(activate(V1)),activate(V1),activate(V2)) p2: U12#(tt(),V1,V2) -> activate#(V1) p3: activate#(n__s(X)) -> activate#(X) p4: activate#(n__plus(X1,X2)) -> activate#(X2) p5: activate#(n__plus(X1,X2)) -> activate#(X1) p6: activate#(n__plus(X1,X2)) -> plus#(activate(X1),activate(X2)) p7: plus#(N,s(M)) -> isNat#(M) p8: isNat#(n__s(V1)) -> activate#(V1) p9: isNat#(n__s(V1)) -> isNatKind#(activate(V1)) p10: isNatKind#(n__s(V1)) -> activate#(V1) p11: isNatKind#(n__s(V1)) -> isNatKind#(activate(V1)) p12: isNatKind#(n__plus(V1,V2)) -> activate#(V2) p13: isNatKind#(n__plus(V1,V2)) -> activate#(V1) p14: isNatKind#(n__plus(V1,V2)) -> isNatKind#(activate(V1)) p15: isNatKind#(n__plus(V1,V2)) -> U31#(isNatKind(activate(V1)),activate(V2)) p16: U31#(tt(),V2) -> activate#(V2) p17: U31#(tt(),V2) -> isNatKind#(activate(V2)) p18: isNat#(n__s(V1)) -> U21#(isNatKind(activate(V1)),activate(V1)) p19: U21#(tt(),V1) -> activate#(V1) p20: U21#(tt(),V1) -> isNatKind#(activate(V1)) p21: U21#(tt(),V1) -> U22#(isNatKind(activate(V1)),activate(V1)) p22: U22#(tt(),V1) -> activate#(V1) p23: U22#(tt(),V1) -> isNat#(activate(V1)) p24: isNat#(n__plus(V1,V2)) -> activate#(V2) p25: isNat#(n__plus(V1,V2)) -> activate#(V1) p26: isNat#(n__plus(V1,V2)) -> isNatKind#(activate(V1)) p27: isNat#(n__plus(V1,V2)) -> U11#(isNatKind(activate(V1)),activate(V1),activate(V2)) p28: U11#(tt(),V1,V2) -> activate#(V2) p29: U11#(tt(),V1,V2) -> activate#(V1) p30: U11#(tt(),V1,V2) -> isNatKind#(activate(V1)) p31: plus#(N,s(M)) -> U61#(isNat(M),M,N) p32: U61#(tt(),M,N) -> activate#(N) p33: U61#(tt(),M,N) -> activate#(M) p34: U61#(tt(),M,N) -> isNatKind#(activate(M)) p35: U61#(tt(),M,N) -> U62#(isNatKind(activate(M)),activate(M),activate(N)) p36: U62#(tt(),M,N) -> activate#(M) p37: U62#(tt(),M,N) -> activate#(N) p38: U62#(tt(),M,N) -> isNat#(activate(N)) p39: U62#(tt(),M,N) -> U63#(isNat(activate(N)),activate(M),activate(N)) p40: U63#(tt(),M,N) -> activate#(M) p41: U63#(tt(),M,N) -> activate#(N) p42: U63#(tt(),M,N) -> isNatKind#(activate(N)) p43: U63#(tt(),M,N) -> U64#(isNatKind(activate(N)),activate(M),activate(N)) p44: U64#(tt(),M,N) -> activate#(M) p45: U64#(tt(),M,N) -> activate#(N) p46: U64#(tt(),M,N) -> plus#(activate(N),activate(M)) p47: plus#(N,|0|()) -> isNat#(N) p48: plus#(N,|0|()) -> U51#(isNat(N),N) p49: U51#(tt(),N) -> activate#(N) p50: U51#(tt(),N) -> isNatKind#(activate(N)) p51: U51#(tt(),N) -> U52#(isNatKind(activate(N)),activate(N)) p52: U52#(tt(),N) -> activate#(N) p53: U12#(tt(),V1,V2) -> isNatKind#(activate(V2)) p54: U12#(tt(),V1,V2) -> U13#(isNatKind(activate(V2)),activate(V1),activate(V2)) p55: U13#(tt(),V1,V2) -> activate#(V1) p56: U13#(tt(),V1,V2) -> activate#(V2) p57: U13#(tt(),V1,V2) -> isNatKind#(activate(V2)) p58: U13#(tt(),V1,V2) -> U14#(isNatKind(activate(V2)),activate(V1),activate(V2)) p59: U14#(tt(),V1,V2) -> activate#(V2) p60: U14#(tt(),V1,V2) -> activate#(V1) p61: U14#(tt(),V1,V2) -> isNat#(activate(V1)) p62: U14#(tt(),V1,V2) -> U15#(isNat(activate(V1)),activate(V2)) p63: U15#(tt(),V2) -> activate#(V2) p64: U15#(tt(),V2) -> isNat#(activate(V2)) and R consists of: r1: U11(tt(),V1,V2) -> U12(isNatKind(activate(V1)),activate(V1),activate(V2)) r2: U12(tt(),V1,V2) -> U13(isNatKind(activate(V2)),activate(V1),activate(V2)) r3: U13(tt(),V1,V2) -> U14(isNatKind(activate(V2)),activate(V1),activate(V2)) r4: U14(tt(),V1,V2) -> U15(isNat(activate(V1)),activate(V2)) r5: U15(tt(),V2) -> U16(isNat(activate(V2))) r6: U16(tt()) -> tt() r7: U21(tt(),V1) -> U22(isNatKind(activate(V1)),activate(V1)) r8: U22(tt(),V1) -> U23(isNat(activate(V1))) r9: U23(tt()) -> tt() r10: U31(tt(),V2) -> U32(isNatKind(activate(V2))) r11: U32(tt()) -> tt() r12: U41(tt()) -> tt() r13: U51(tt(),N) -> U52(isNatKind(activate(N)),activate(N)) r14: U52(tt(),N) -> activate(N) r15: U61(tt(),M,N) -> U62(isNatKind(activate(M)),activate(M),activate(N)) r16: U62(tt(),M,N) -> U63(isNat(activate(N)),activate(M),activate(N)) r17: U63(tt(),M,N) -> U64(isNatKind(activate(N)),activate(M),activate(N)) r18: U64(tt(),M,N) -> s(plus(activate(N),activate(M))) r19: isNat(n__0()) -> tt() r20: isNat(n__plus(V1,V2)) -> U11(isNatKind(activate(V1)),activate(V1),activate(V2)) r21: isNat(n__s(V1)) -> U21(isNatKind(activate(V1)),activate(V1)) r22: isNatKind(n__0()) -> tt() r23: isNatKind(n__plus(V1,V2)) -> U31(isNatKind(activate(V1)),activate(V2)) r24: isNatKind(n__s(V1)) -> U41(isNatKind(activate(V1))) r25: plus(N,|0|()) -> U51(isNat(N),N) r26: plus(N,s(M)) -> U61(isNat(M),M,N) r27: |0|() -> n__0() r28: plus(X1,X2) -> n__plus(X1,X2) r29: s(X) -> n__s(X) r30: activate(n__0()) -> |0|() r31: activate(n__plus(X1,X2)) -> plus(activate(X1),activate(X2)) r32: activate(n__s(X)) -> s(activate(X)) r33: activate(X) -> 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, p30, p31, p32, p33, p34, p35, p36, p37, p38, p39, p40, p41, p42, p43, p44, p45, p46, p47, p48, p49, p50, p51, p52, p53, p54, p55, p56, p57, p58, p59, p60, p61, p62, p63, p64} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: U11#(tt(),V1,V2) -> U12#(isNatKind(activate(V1)),activate(V1),activate(V2)) p2: U12#(tt(),V1,V2) -> U13#(isNatKind(activate(V2)),activate(V1),activate(V2)) p3: U13#(tt(),V1,V2) -> U14#(isNatKind(activate(V2)),activate(V1),activate(V2)) p4: U14#(tt(),V1,V2) -> U15#(isNat(activate(V1)),activate(V2)) p5: U15#(tt(),V2) -> isNat#(activate(V2)) p6: isNat#(n__plus(V1,V2)) -> U11#(isNatKind(activate(V1)),activate(V1),activate(V2)) p7: U11#(tt(),V1,V2) -> isNatKind#(activate(V1)) p8: isNatKind#(n__plus(V1,V2)) -> U31#(isNatKind(activate(V1)),activate(V2)) p9: U31#(tt(),V2) -> isNatKind#(activate(V2)) p10: isNatKind#(n__plus(V1,V2)) -> isNatKind#(activate(V1)) p11: isNatKind#(n__plus(V1,V2)) -> activate#(V1) p12: activate#(n__plus(X1,X2)) -> plus#(activate(X1),activate(X2)) p13: plus#(N,|0|()) -> U51#(isNat(N),N) p14: U51#(tt(),N) -> U52#(isNatKind(activate(N)),activate(N)) p15: U52#(tt(),N) -> activate#(N) p16: activate#(n__plus(X1,X2)) -> activate#(X1) p17: activate#(n__plus(X1,X2)) -> activate#(X2) p18: activate#(n__s(X)) -> activate#(X) p19: U51#(tt(),N) -> isNatKind#(activate(N)) p20: isNatKind#(n__plus(V1,V2)) -> activate#(V2) p21: isNatKind#(n__s(V1)) -> isNatKind#(activate(V1)) p22: isNatKind#(n__s(V1)) -> activate#(V1) p23: U51#(tt(),N) -> activate#(N) p24: plus#(N,|0|()) -> isNat#(N) p25: isNat#(n__plus(V1,V2)) -> isNatKind#(activate(V1)) p26: isNat#(n__plus(V1,V2)) -> activate#(V1) p27: isNat#(n__plus(V1,V2)) -> activate#(V2) p28: isNat#(n__s(V1)) -> U21#(isNatKind(activate(V1)),activate(V1)) p29: U21#(tt(),V1) -> U22#(isNatKind(activate(V1)),activate(V1)) p30: U22#(tt(),V1) -> isNat#(activate(V1)) p31: isNat#(n__s(V1)) -> isNatKind#(activate(V1)) p32: isNat#(n__s(V1)) -> activate#(V1) p33: U22#(tt(),V1) -> activate#(V1) p34: U21#(tt(),V1) -> isNatKind#(activate(V1)) p35: U21#(tt(),V1) -> activate#(V1) p36: plus#(N,s(M)) -> U61#(isNat(M),M,N) p37: U61#(tt(),M,N) -> U62#(isNatKind(activate(M)),activate(M),activate(N)) p38: U62#(tt(),M,N) -> U63#(isNat(activate(N)),activate(M),activate(N)) p39: U63#(tt(),M,N) -> U64#(isNatKind(activate(N)),activate(M),activate(N)) p40: U64#(tt(),M,N) -> plus#(activate(N),activate(M)) p41: plus#(N,s(M)) -> isNat#(M) p42: U64#(tt(),M,N) -> activate#(N) p43: U64#(tt(),M,N) -> activate#(M) p44: U63#(tt(),M,N) -> isNatKind#(activate(N)) p45: U63#(tt(),M,N) -> activate#(N) p46: U63#(tt(),M,N) -> activate#(M) p47: U62#(tt(),M,N) -> isNat#(activate(N)) p48: U62#(tt(),M,N) -> activate#(N) p49: U62#(tt(),M,N) -> activate#(M) p50: U61#(tt(),M,N) -> isNatKind#(activate(M)) p51: U61#(tt(),M,N) -> activate#(M) p52: U61#(tt(),M,N) -> activate#(N) p53: U31#(tt(),V2) -> activate#(V2) p54: U11#(tt(),V1,V2) -> activate#(V1) p55: U11#(tt(),V1,V2) -> activate#(V2) p56: U15#(tt(),V2) -> activate#(V2) p57: U14#(tt(),V1,V2) -> isNat#(activate(V1)) p58: U14#(tt(),V1,V2) -> activate#(V1) p59: U14#(tt(),V1,V2) -> activate#(V2) p60: U13#(tt(),V1,V2) -> isNatKind#(activate(V2)) p61: U13#(tt(),V1,V2) -> activate#(V2) p62: U13#(tt(),V1,V2) -> activate#(V1) p63: U12#(tt(),V1,V2) -> isNatKind#(activate(V2)) p64: U12#(tt(),V1,V2) -> activate#(V1) and R consists of: r1: U11(tt(),V1,V2) -> U12(isNatKind(activate(V1)),activate(V1),activate(V2)) r2: U12(tt(),V1,V2) -> U13(isNatKind(activate(V2)),activate(V1),activate(V2)) r3: U13(tt(),V1,V2) -> U14(isNatKind(activate(V2)),activate(V1),activate(V2)) r4: U14(tt(),V1,V2) -> U15(isNat(activate(V1)),activate(V2)) r5: U15(tt(),V2) -> U16(isNat(activate(V2))) r6: U16(tt()) -> tt() r7: U21(tt(),V1) -> U22(isNatKind(activate(V1)),activate(V1)) r8: U22(tt(),V1) -> U23(isNat(activate(V1))) r9: U23(tt()) -> tt() r10: U31(tt(),V2) -> U32(isNatKind(activate(V2))) r11: U32(tt()) -> tt() r12: U41(tt()) -> tt() r13: U51(tt(),N) -> U52(isNatKind(activate(N)),activate(N)) r14: U52(tt(),N) -> activate(N) r15: U61(tt(),M,N) -> U62(isNatKind(activate(M)),activate(M),activate(N)) r16: U62(tt(),M,N) -> U63(isNat(activate(N)),activate(M),activate(N)) r17: U63(tt(),M,N) -> U64(isNatKind(activate(N)),activate(M),activate(N)) r18: U64(tt(),M,N) -> s(plus(activate(N),activate(M))) r19: isNat(n__0()) -> tt() r20: isNat(n__plus(V1,V2)) -> U11(isNatKind(activate(V1)),activate(V1),activate(V2)) r21: isNat(n__s(V1)) -> U21(isNatKind(activate(V1)),activate(V1)) r22: isNatKind(n__0()) -> tt() r23: isNatKind(n__plus(V1,V2)) -> U31(isNatKind(activate(V1)),activate(V2)) r24: isNatKind(n__s(V1)) -> U41(isNatKind(activate(V1))) r25: plus(N,|0|()) -> U51(isNat(N),N) r26: plus(N,s(M)) -> U61(isNat(M),M,N) r27: |0|() -> n__0() r28: plus(X1,X2) -> n__plus(X1,X2) r29: s(X) -> n__s(X) r30: activate(n__0()) -> |0|() r31: activate(n__plus(X1,X2)) -> plus(activate(X1),activate(X2)) r32: activate(n__s(X)) -> s(activate(X)) r33: activate(X) -> 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 Take the reduction pair: weighted path order base order: matrix interpretations: carrier: N^1 order: lexicographic order interpretations: U11#_A(x1,x2,x3) = x2 + x3 + 19 tt_A() = 14 U12#_A(x1,x2,x3) = x2 + x3 + 19 isNatKind_A(x1) = 20 activate_A(x1) = x1 U13#_A(x1,x2,x3) = x2 + x3 + 19 U14#_A(x1,x2,x3) = x2 + x3 + 19 U15#_A(x1,x2) = x2 + 19 isNat_A(x1) = x1 + 10 isNat#_A(x1) = x1 + 19 n__plus_A(x1,x2) = x1 + x2 isNatKind#_A(x1) = x1 + 17 U31#_A(x1,x2) = x2 + 17 activate#_A(x1) = x1 + 14 plus#_A(x1,x2) = x1 + x2 + 14 |0|_A() = 5 U51#_A(x1,x2) = x2 + 18 U52#_A(x1,x2) = x2 + 18 n__s_A(x1) = x1 + 9 U21#_A(x1,x2) = x2 + 28 U22#_A(x1,x2) = x2 + 28 s_A(x1) = x1 + 9 U61#_A(x1,x2,x3) = x2 + x3 + 22 U62#_A(x1,x2,x3) = x2 + x3 + 21 U63#_A(x1,x2,x3) = x2 + x3 + 20 U64#_A(x1,x2,x3) = x1 + x2 + x3 U16_A(x1) = x1 + 3 U15_A(x1,x2) = x1 + x2 U64_A(x1,x2,x3) = x2 + x3 + 9 plus_A(x1,x2) = x1 + x2 U14_A(x1,x2,x3) = x2 + x3 + 10 U63_A(x1,x2,x3) = x2 + x3 + 9 U13_A(x1,x2,x3) = x2 + x3 + 10 U23_A(x1) = 15 U52_A(x1,x2) = x2 + 4 U62_A(x1,x2,x3) = x2 + x3 + 9 U12_A(x1,x2,x3) = x2 + x3 + 10 U22_A(x1,x2) = 16 U32_A(x1) = 15 U51_A(x1,x2) = x2 + 5 U61_A(x1,x2,x3) = x2 + x3 + 9 U11_A(x1,x2,x3) = x2 + x3 + 10 U21_A(x1,x2) = 18 U31_A(x1,x2) = 20 U41_A(x1) = 15 n__0_A() = 5 precedence: U11# = tt = U12# = isNatKind = activate = U13# = U14# = U15# = isNat = isNat# = n__plus = isNatKind# = U31# = activate# = plus# = |0| = U51# = U52# = n__s = U21# = U22# = s = U61# = U62# = U63# = U64# = U16 = U15 = U64 = plus = U14 = U63 = U13 = U23 = U52 = U62 = U12 = U22 = U32 = U51 = U61 = U11 = U21 = U31 = U41 = n__0 partial status: pi(U11#) = [] pi(tt) = [] pi(U12#) = [] pi(isNatKind) = [] pi(activate) = [] pi(U13#) = [] pi(U14#) = [] pi(U15#) = [] pi(isNat) = [] pi(isNat#) = [] pi(n__plus) = [] pi(isNatKind#) = [] pi(U31#) = [] pi(activate#) = [] pi(plus#) = [] pi(|0|) = [] pi(U51#) = [] pi(U52#) = [] pi(n__s) = [] pi(U21#) = [] pi(U22#) = [] pi(s) = [] pi(U61#) = [] pi(U62#) = [] pi(U63#) = [] pi(U64#) = [] pi(U16) = [] pi(U15) = [] pi(U64) = [] pi(plus) = [] pi(U14) = [] pi(U63) = [] pi(U13) = [] pi(U23) = [] pi(U52) = [] pi(U62) = [] pi(U12) = [] pi(U22) = [] pi(U32) = [] pi(U51) = [] pi(U61) = [] pi(U11) = [] pi(U21) = [] pi(U31) = [] pi(U41) = [] pi(n__0) = [] The next rules are strictly ordered: p18 We remove them from the problem. -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: U11#(tt(),V1,V2) -> U12#(isNatKind(activate(V1)),activate(V1),activate(V2)) p2: U12#(tt(),V1,V2) -> U13#(isNatKind(activate(V2)),activate(V1),activate(V2)) p3: U13#(tt(),V1,V2) -> U14#(isNatKind(activate(V2)),activate(V1),activate(V2)) p4: U14#(tt(),V1,V2) -> U15#(isNat(activate(V1)),activate(V2)) p5: U15#(tt(),V2) -> isNat#(activate(V2)) p6: isNat#(n__plus(V1,V2)) -> U11#(isNatKind(activate(V1)),activate(V1),activate(V2)) p7: U11#(tt(),V1,V2) -> isNatKind#(activate(V1)) p8: isNatKind#(n__plus(V1,V2)) -> U31#(isNatKind(activate(V1)),activate(V2)) p9: U31#(tt(),V2) -> isNatKind#(activate(V2)) p10: isNatKind#(n__plus(V1,V2)) -> isNatKind#(activate(V1)) p11: isNatKind#(n__plus(V1,V2)) -> activate#(V1) p12: activate#(n__plus(X1,X2)) -> plus#(activate(X1),activate(X2)) p13: plus#(N,|0|()) -> U51#(isNat(N),N) p14: U51#(tt(),N) -> U52#(isNatKind(activate(N)),activate(N)) p15: U52#(tt(),N) -> activate#(N) p16: activate#(n__plus(X1,X2)) -> activate#(X1) p17: activate#(n__plus(X1,X2)) -> activate#(X2) p18: U51#(tt(),N) -> isNatKind#(activate(N)) p19: isNatKind#(n__plus(V1,V2)) -> activate#(V2) p20: isNatKind#(n__s(V1)) -> isNatKind#(activate(V1)) p21: isNatKind#(n__s(V1)) -> activate#(V1) p22: U51#(tt(),N) -> activate#(N) p23: plus#(N,|0|()) -> isNat#(N) p24: isNat#(n__plus(V1,V2)) -> isNatKind#(activate(V1)) p25: isNat#(n__plus(V1,V2)) -> activate#(V1) p26: isNat#(n__plus(V1,V2)) -> activate#(V2) p27: isNat#(n__s(V1)) -> U21#(isNatKind(activate(V1)),activate(V1)) p28: U21#(tt(),V1) -> U22#(isNatKind(activate(V1)),activate(V1)) p29: U22#(tt(),V1) -> isNat#(activate(V1)) p30: isNat#(n__s(V1)) -> isNatKind#(activate(V1)) p31: isNat#(n__s(V1)) -> activate#(V1) p32: U22#(tt(),V1) -> activate#(V1) p33: U21#(tt(),V1) -> isNatKind#(activate(V1)) p34: U21#(tt(),V1) -> activate#(V1) p35: plus#(N,s(M)) -> U61#(isNat(M),M,N) p36: U61#(tt(),M,N) -> U62#(isNatKind(activate(M)),activate(M),activate(N)) p37: U62#(tt(),M,N) -> U63#(isNat(activate(N)),activate(M),activate(N)) p38: U63#(tt(),M,N) -> U64#(isNatKind(activate(N)),activate(M),activate(N)) p39: U64#(tt(),M,N) -> plus#(activate(N),activate(M)) p40: plus#(N,s(M)) -> isNat#(M) p41: U64#(tt(),M,N) -> activate#(N) p42: U64#(tt(),M,N) -> activate#(M) p43: U63#(tt(),M,N) -> isNatKind#(activate(N)) p44: U63#(tt(),M,N) -> activate#(N) p45: U63#(tt(),M,N) -> activate#(M) p46: U62#(tt(),M,N) -> isNat#(activate(N)) p47: U62#(tt(),M,N) -> activate#(N) p48: U62#(tt(),M,N) -> activate#(M) p49: U61#(tt(),M,N) -> isNatKind#(activate(M)) p50: U61#(tt(),M,N) -> activate#(M) p51: U61#(tt(),M,N) -> activate#(N) p52: U31#(tt(),V2) -> activate#(V2) p53: U11#(tt(),V1,V2) -> activate#(V1) p54: U11#(tt(),V1,V2) -> activate#(V2) p55: U15#(tt(),V2) -> activate#(V2) p56: U14#(tt(),V1,V2) -> isNat#(activate(V1)) p57: U14#(tt(),V1,V2) -> activate#(V1) p58: U14#(tt(),V1,V2) -> activate#(V2) p59: U13#(tt(),V1,V2) -> isNatKind#(activate(V2)) p60: U13#(tt(),V1,V2) -> activate#(V2) p61: U13#(tt(),V1,V2) -> activate#(V1) p62: U12#(tt(),V1,V2) -> isNatKind#(activate(V2)) p63: U12#(tt(),V1,V2) -> activate#(V1) and R consists of: r1: U11(tt(),V1,V2) -> U12(isNatKind(activate(V1)),activate(V1),activate(V2)) r2: U12(tt(),V1,V2) -> U13(isNatKind(activate(V2)),activate(V1),activate(V2)) r3: U13(tt(),V1,V2) -> U14(isNatKind(activate(V2)),activate(V1),activate(V2)) r4: U14(tt(),V1,V2) -> U15(isNat(activate(V1)),activate(V2)) r5: U15(tt(),V2) -> U16(isNat(activate(V2))) r6: U16(tt()) -> tt() r7: U21(tt(),V1) -> U22(isNatKind(activate(V1)),activate(V1)) r8: U22(tt(),V1) -> U23(isNat(activate(V1))) r9: U23(tt()) -> tt() r10: U31(tt(),V2) -> U32(isNatKind(activate(V2))) r11: U32(tt()) -> tt() r12: U41(tt()) -> tt() r13: U51(tt(),N) -> U52(isNatKind(activate(N)),activate(N)) r14: U52(tt(),N) -> activate(N) r15: U61(tt(),M,N) -> U62(isNatKind(activate(M)),activate(M),activate(N)) r16: U62(tt(),M,N) -> U63(isNat(activate(N)),activate(M),activate(N)) r17: U63(tt(),M,N) -> U64(isNatKind(activate(N)),activate(M),activate(N)) r18: U64(tt(),M,N) -> s(plus(activate(N),activate(M))) r19: isNat(n__0()) -> tt() r20: isNat(n__plus(V1,V2)) -> U11(isNatKind(activate(V1)),activate(V1),activate(V2)) r21: isNat(n__s(V1)) -> U21(isNatKind(activate(V1)),activate(V1)) r22: isNatKind(n__0()) -> tt() r23: isNatKind(n__plus(V1,V2)) -> U31(isNatKind(activate(V1)),activate(V2)) r24: isNatKind(n__s(V1)) -> U41(isNatKind(activate(V1))) r25: plus(N,|0|()) -> U51(isNat(N),N) r26: plus(N,s(M)) -> U61(isNat(M),M,N) r27: |0|() -> n__0() r28: plus(X1,X2) -> n__plus(X1,X2) r29: s(X) -> n__s(X) r30: activate(n__0()) -> |0|() r31: activate(n__plus(X1,X2)) -> plus(activate(X1),activate(X2)) r32: activate(n__s(X)) -> s(activate(X)) r33: activate(X) -> 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, p30, p31, p32, p33, p34, p35, p36, p37, p38, p39, p40, p41, p42, p43, p44, p45, p46, p47, p48, p49, p50, p51, p52, p53, p54, p55, p56, p57, p58, p59, p60, p61, p62, p63} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: U11#(tt(),V1,V2) -> U12#(isNatKind(activate(V1)),activate(V1),activate(V2)) p2: U12#(tt(),V1,V2) -> activate#(V1) p3: activate#(n__plus(X1,X2)) -> activate#(X2) p4: activate#(n__plus(X1,X2)) -> activate#(X1) p5: activate#(n__plus(X1,X2)) -> plus#(activate(X1),activate(X2)) p6: plus#(N,s(M)) -> isNat#(M) p7: isNat#(n__s(V1)) -> activate#(V1) p8: isNat#(n__s(V1)) -> isNatKind#(activate(V1)) p9: isNatKind#(n__s(V1)) -> activate#(V1) p10: isNatKind#(n__s(V1)) -> isNatKind#(activate(V1)) p11: isNatKind#(n__plus(V1,V2)) -> activate#(V2) p12: isNatKind#(n__plus(V1,V2)) -> activate#(V1) p13: isNatKind#(n__plus(V1,V2)) -> isNatKind#(activate(V1)) p14: isNatKind#(n__plus(V1,V2)) -> U31#(isNatKind(activate(V1)),activate(V2)) p15: U31#(tt(),V2) -> activate#(V2) p16: U31#(tt(),V2) -> isNatKind#(activate(V2)) p17: isNat#(n__s(V1)) -> U21#(isNatKind(activate(V1)),activate(V1)) p18: U21#(tt(),V1) -> activate#(V1) p19: U21#(tt(),V1) -> isNatKind#(activate(V1)) p20: U21#(tt(),V1) -> U22#(isNatKind(activate(V1)),activate(V1)) p21: U22#(tt(),V1) -> activate#(V1) p22: U22#(tt(),V1) -> isNat#(activate(V1)) p23: isNat#(n__plus(V1,V2)) -> activate#(V2) p24: isNat#(n__plus(V1,V2)) -> activate#(V1) p25: isNat#(n__plus(V1,V2)) -> isNatKind#(activate(V1)) p26: isNat#(n__plus(V1,V2)) -> U11#(isNatKind(activate(V1)),activate(V1),activate(V2)) p27: U11#(tt(),V1,V2) -> activate#(V2) p28: U11#(tt(),V1,V2) -> activate#(V1) p29: U11#(tt(),V1,V2) -> isNatKind#(activate(V1)) p30: plus#(N,s(M)) -> U61#(isNat(M),M,N) p31: U61#(tt(),M,N) -> activate#(N) p32: U61#(tt(),M,N) -> activate#(M) p33: U61#(tt(),M,N) -> isNatKind#(activate(M)) p34: U61#(tt(),M,N) -> U62#(isNatKind(activate(M)),activate(M),activate(N)) p35: U62#(tt(),M,N) -> activate#(M) p36: U62#(tt(),M,N) -> activate#(N) p37: U62#(tt(),M,N) -> isNat#(activate(N)) p38: U62#(tt(),M,N) -> U63#(isNat(activate(N)),activate(M),activate(N)) p39: U63#(tt(),M,N) -> activate#(M) p40: U63#(tt(),M,N) -> activate#(N) p41: U63#(tt(),M,N) -> isNatKind#(activate(N)) p42: U63#(tt(),M,N) -> U64#(isNatKind(activate(N)),activate(M),activate(N)) p43: U64#(tt(),M,N) -> activate#(M) p44: U64#(tt(),M,N) -> activate#(N) p45: U64#(tt(),M,N) -> plus#(activate(N),activate(M)) p46: plus#(N,|0|()) -> isNat#(N) p47: plus#(N,|0|()) -> U51#(isNat(N),N) p48: U51#(tt(),N) -> activate#(N) p49: U51#(tt(),N) -> isNatKind#(activate(N)) p50: U51#(tt(),N) -> U52#(isNatKind(activate(N)),activate(N)) p51: U52#(tt(),N) -> activate#(N) p52: U12#(tt(),V1,V2) -> isNatKind#(activate(V2)) p53: U12#(tt(),V1,V2) -> U13#(isNatKind(activate(V2)),activate(V1),activate(V2)) p54: U13#(tt(),V1,V2) -> activate#(V1) p55: U13#(tt(),V1,V2) -> activate#(V2) p56: U13#(tt(),V1,V2) -> isNatKind#(activate(V2)) p57: U13#(tt(),V1,V2) -> U14#(isNatKind(activate(V2)),activate(V1),activate(V2)) p58: U14#(tt(),V1,V2) -> activate#(V2) p59: U14#(tt(),V1,V2) -> activate#(V1) p60: U14#(tt(),V1,V2) -> isNat#(activate(V1)) p61: U14#(tt(),V1,V2) -> U15#(isNat(activate(V1)),activate(V2)) p62: U15#(tt(),V2) -> activate#(V2) p63: U15#(tt(),V2) -> isNat#(activate(V2)) and R consists of: r1: U11(tt(),V1,V2) -> U12(isNatKind(activate(V1)),activate(V1),activate(V2)) r2: U12(tt(),V1,V2) -> U13(isNatKind(activate(V2)),activate(V1),activate(V2)) r3: U13(tt(),V1,V2) -> U14(isNatKind(activate(V2)),activate(V1),activate(V2)) r4: U14(tt(),V1,V2) -> U15(isNat(activate(V1)),activate(V2)) r5: U15(tt(),V2) -> U16(isNat(activate(V2))) r6: U16(tt()) -> tt() r7: U21(tt(),V1) -> U22(isNatKind(activate(V1)),activate(V1)) r8: U22(tt(),V1) -> U23(isNat(activate(V1))) r9: U23(tt()) -> tt() r10: U31(tt(),V2) -> U32(isNatKind(activate(V2))) r11: U32(tt()) -> tt() r12: U41(tt()) -> tt() r13: U51(tt(),N) -> U52(isNatKind(activate(N)),activate(N)) r14: U52(tt(),N) -> activate(N) r15: U61(tt(),M,N) -> U62(isNatKind(activate(M)),activate(M),activate(N)) r16: U62(tt(),M,N) -> U63(isNat(activate(N)),activate(M),activate(N)) r17: U63(tt(),M,N) -> U64(isNatKind(activate(N)),activate(M),activate(N)) r18: U64(tt(),M,N) -> s(plus(activate(N),activate(M))) r19: isNat(n__0()) -> tt() r20: isNat(n__plus(V1,V2)) -> U11(isNatKind(activate(V1)),activate(V1),activate(V2)) r21: isNat(n__s(V1)) -> U21(isNatKind(activate(V1)),activate(V1)) r22: isNatKind(n__0()) -> tt() r23: isNatKind(n__plus(V1,V2)) -> U31(isNatKind(activate(V1)),activate(V2)) r24: isNatKind(n__s(V1)) -> U41(isNatKind(activate(V1))) r25: plus(N,|0|()) -> U51(isNat(N),N) r26: plus(N,s(M)) -> U61(isNat(M),M,N) r27: |0|() -> n__0() r28: plus(X1,X2) -> n__plus(X1,X2) r29: s(X) -> n__s(X) r30: activate(n__0()) -> |0|() r31: activate(n__plus(X1,X2)) -> plus(activate(X1),activate(X2)) r32: activate(n__s(X)) -> s(activate(X)) r33: activate(X) -> 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 Take the reduction pair: weighted path order base order: matrix interpretations: carrier: N^1 order: lexicographic order interpretations: U11#_A(x1,x2,x3) = x2 + x3 + 17 tt_A() = 1 U12#_A(x1,x2,x3) = x1 + x2 + x3 + 12 isNatKind_A(x1) = 1 activate_A(x1) = x1 activate#_A(x1) = x1 + 6 n__plus_A(x1,x2) = x1 + x2 + 9 plus#_A(x1,x2) = x1 + x2 + 8 s_A(x1) = x1 isNat#_A(x1) = x1 + 8 n__s_A(x1) = x1 isNatKind#_A(x1) = x1 + 7 U31#_A(x1,x2) = x2 + 7 U21#_A(x1,x2) = x2 + 8 U22#_A(x1,x2) = x2 + 8 U61#_A(x1,x2,x3) = x2 + x3 + 8 isNat_A(x1) = 6 U62#_A(x1,x2,x3) = x2 + x3 + 8 U63#_A(x1,x2,x3) = x2 + x3 + 8 U64#_A(x1,x2,x3) = x1 + x2 + x3 + 7 |0|_A() = 0 U51#_A(x1,x2) = x2 + 8 U52#_A(x1,x2) = x2 + 7 U13#_A(x1,x2,x3) = x1 + x2 + x3 + 12 U14#_A(x1,x2,x3) = x1 + x2 + x3 + 12 U15#_A(x1,x2) = x1 + x2 + 7 U16_A(x1) = 2 U15_A(x1,x2) = 2 U64_A(x1,x2,x3) = x1 + x2 + x3 + 8 plus_A(x1,x2) = x1 + x2 + 9 U14_A(x1,x2,x3) = 3 U63_A(x1,x2,x3) = x2 + x3 + 9 U13_A(x1,x2,x3) = x1 + 3 U23_A(x1) = 2 U52_A(x1,x2) = x2 + 2 U62_A(x1,x2,x3) = x2 + x3 + 9 U12_A(x1,x2,x3) = 5 U22_A(x1,x2) = 3 U32_A(x1) = x1 U51_A(x1,x2) = x1 + x2 + 2 U61_A(x1,x2,x3) = x2 + x3 + 9 U11_A(x1,x2,x3) = 6 U21_A(x1,x2) = 4 U31_A(x1,x2) = 1 U41_A(x1) = 1 n__0_A() = 0 precedence: U11# = tt = U12# = isNatKind = activate = activate# = n__plus = plus# = s = isNat# = n__s = isNatKind# = U31# = U21# = U22# = U61# = isNat = U62# = U63# = U64# = |0| = U51# = U52# = U13# = U14# = U15# = U16 = U15 = U64 = plus = U14 = U63 = U13 = U23 = U52 = U62 = U12 = U22 = U32 = U51 = U61 = U11 = U21 = U31 = U41 = n__0 partial status: pi(U11#) = [] pi(tt) = [] pi(U12#) = [] pi(isNatKind) = [] pi(activate) = [] pi(activate#) = [] pi(n__plus) = [] pi(plus#) = [] pi(s) = [] pi(isNat#) = [] pi(n__s) = [] pi(isNatKind#) = [] pi(U31#) = [] pi(U21#) = [] pi(U22#) = [] pi(U61#) = [] pi(isNat) = [] pi(U62#) = [] pi(U63#) = [] pi(U64#) = [] pi(|0|) = [] pi(U51#) = [] pi(U52#) = [] pi(U13#) = [] pi(U14#) = [] pi(U15#) = [] pi(U16) = [] pi(U15) = [] pi(U64) = [] pi(plus) = [] pi(U14) = [] pi(U63) = [] pi(U13) = [] pi(U23) = [] pi(U52) = [] pi(U62) = [] pi(U12) = [] pi(U22) = [] pi(U32) = [] pi(U51) = [] pi(U61) = [] pi(U11) = [] pi(U21) = [] pi(U31) = [] pi(U41) = [] pi(n__0) = [] The next rules are strictly ordered: p3 We remove them from the problem. -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: U11#(tt(),V1,V2) -> U12#(isNatKind(activate(V1)),activate(V1),activate(V2)) p2: U12#(tt(),V1,V2) -> activate#(V1) p3: activate#(n__plus(X1,X2)) -> activate#(X1) p4: activate#(n__plus(X1,X2)) -> plus#(activate(X1),activate(X2)) p5: plus#(N,s(M)) -> isNat#(M) p6: isNat#(n__s(V1)) -> activate#(V1) p7: isNat#(n__s(V1)) -> isNatKind#(activate(V1)) p8: isNatKind#(n__s(V1)) -> activate#(V1) p9: isNatKind#(n__s(V1)) -> isNatKind#(activate(V1)) p10: isNatKind#(n__plus(V1,V2)) -> activate#(V2) p11: isNatKind#(n__plus(V1,V2)) -> activate#(V1) p12: isNatKind#(n__plus(V1,V2)) -> isNatKind#(activate(V1)) p13: isNatKind#(n__plus(V1,V2)) -> U31#(isNatKind(activate(V1)),activate(V2)) p14: U31#(tt(),V2) -> activate#(V2) p15: U31#(tt(),V2) -> isNatKind#(activate(V2)) p16: isNat#(n__s(V1)) -> U21#(isNatKind(activate(V1)),activate(V1)) p17: U21#(tt(),V1) -> activate#(V1) p18: U21#(tt(),V1) -> isNatKind#(activate(V1)) p19: U21#(tt(),V1) -> U22#(isNatKind(activate(V1)),activate(V1)) p20: U22#(tt(),V1) -> activate#(V1) p21: U22#(tt(),V1) -> isNat#(activate(V1)) p22: isNat#(n__plus(V1,V2)) -> activate#(V2) p23: isNat#(n__plus(V1,V2)) -> activate#(V1) p24: isNat#(n__plus(V1,V2)) -> isNatKind#(activate(V1)) p25: isNat#(n__plus(V1,V2)) -> U11#(isNatKind(activate(V1)),activate(V1),activate(V2)) p26: U11#(tt(),V1,V2) -> activate#(V2) p27: U11#(tt(),V1,V2) -> activate#(V1) p28: U11#(tt(),V1,V2) -> isNatKind#(activate(V1)) p29: plus#(N,s(M)) -> U61#(isNat(M),M,N) p30: U61#(tt(),M,N) -> activate#(N) p31: U61#(tt(),M,N) -> activate#(M) p32: U61#(tt(),M,N) -> isNatKind#(activate(M)) p33: U61#(tt(),M,N) -> U62#(isNatKind(activate(M)),activate(M),activate(N)) p34: U62#(tt(),M,N) -> activate#(M) p35: U62#(tt(),M,N) -> activate#(N) p36: U62#(tt(),M,N) -> isNat#(activate(N)) p37: U62#(tt(),M,N) -> U63#(isNat(activate(N)),activate(M),activate(N)) p38: U63#(tt(),M,N) -> activate#(M) p39: U63#(tt(),M,N) -> activate#(N) p40: U63#(tt(),M,N) -> isNatKind#(activate(N)) p41: U63#(tt(),M,N) -> U64#(isNatKind(activate(N)),activate(M),activate(N)) p42: U64#(tt(),M,N) -> activate#(M) p43: U64#(tt(),M,N) -> activate#(N) p44: U64#(tt(),M,N) -> plus#(activate(N),activate(M)) p45: plus#(N,|0|()) -> isNat#(N) p46: plus#(N,|0|()) -> U51#(isNat(N),N) p47: U51#(tt(),N) -> activate#(N) p48: U51#(tt(),N) -> isNatKind#(activate(N)) p49: U51#(tt(),N) -> U52#(isNatKind(activate(N)),activate(N)) p50: U52#(tt(),N) -> activate#(N) p51: U12#(tt(),V1,V2) -> isNatKind#(activate(V2)) p52: U12#(tt(),V1,V2) -> U13#(isNatKind(activate(V2)),activate(V1),activate(V2)) p53: U13#(tt(),V1,V2) -> activate#(V1) p54: U13#(tt(),V1,V2) -> activate#(V2) p55: U13#(tt(),V1,V2) -> isNatKind#(activate(V2)) p56: U13#(tt(),V1,V2) -> U14#(isNatKind(activate(V2)),activate(V1),activate(V2)) p57: U14#(tt(),V1,V2) -> activate#(V2) p58: U14#(tt(),V1,V2) -> activate#(V1) p59: U14#(tt(),V1,V2) -> isNat#(activate(V1)) p60: U14#(tt(),V1,V2) -> U15#(isNat(activate(V1)),activate(V2)) p61: U15#(tt(),V2) -> activate#(V2) p62: U15#(tt(),V2) -> isNat#(activate(V2)) and R consists of: r1: U11(tt(),V1,V2) -> U12(isNatKind(activate(V1)),activate(V1),activate(V2)) r2: U12(tt(),V1,V2) -> U13(isNatKind(activate(V2)),activate(V1),activate(V2)) r3: U13(tt(),V1,V2) -> U14(isNatKind(activate(V2)),activate(V1),activate(V2)) r4: U14(tt(),V1,V2) -> U15(isNat(activate(V1)),activate(V2)) r5: U15(tt(),V2) -> U16(isNat(activate(V2))) r6: U16(tt()) -> tt() r7: U21(tt(),V1) -> U22(isNatKind(activate(V1)),activate(V1)) r8: U22(tt(),V1) -> U23(isNat(activate(V1))) r9: U23(tt()) -> tt() r10: U31(tt(),V2) -> U32(isNatKind(activate(V2))) r11: U32(tt()) -> tt() r12: U41(tt()) -> tt() r13: U51(tt(),N) -> U52(isNatKind(activate(N)),activate(N)) r14: U52(tt(),N) -> activate(N) r15: U61(tt(),M,N) -> U62(isNatKind(activate(M)),activate(M),activate(N)) r16: U62(tt(),M,N) -> U63(isNat(activate(N)),activate(M),activate(N)) r17: U63(tt(),M,N) -> U64(isNatKind(activate(N)),activate(M),activate(N)) r18: U64(tt(),M,N) -> s(plus(activate(N),activate(M))) r19: isNat(n__0()) -> tt() r20: isNat(n__plus(V1,V2)) -> U11(isNatKind(activate(V1)),activate(V1),activate(V2)) r21: isNat(n__s(V1)) -> U21(isNatKind(activate(V1)),activate(V1)) r22: isNatKind(n__0()) -> tt() r23: isNatKind(n__plus(V1,V2)) -> U31(isNatKind(activate(V1)),activate(V2)) r24: isNatKind(n__s(V1)) -> U41(isNatKind(activate(V1))) r25: plus(N,|0|()) -> U51(isNat(N),N) r26: plus(N,s(M)) -> U61(isNat(M),M,N) r27: |0|() -> n__0() r28: plus(X1,X2) -> n__plus(X1,X2) r29: s(X) -> n__s(X) r30: activate(n__0()) -> |0|() r31: activate(n__plus(X1,X2)) -> plus(activate(X1),activate(X2)) r32: activate(n__s(X)) -> s(activate(X)) r33: activate(X) -> 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, p30, p31, p32, p33, p34, p35, p36, p37, p38, p39, p40, p41, p42, p43, p44, p45, p46, p47, p48, p49, p50, p51, p52, p53, p54, p55, p56, p57, p58, p59, p60, p61, p62} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: U11#(tt(),V1,V2) -> U12#(isNatKind(activate(V1)),activate(V1),activate(V2)) p2: U12#(tt(),V1,V2) -> U13#(isNatKind(activate(V2)),activate(V1),activate(V2)) p3: U13#(tt(),V1,V2) -> U14#(isNatKind(activate(V2)),activate(V1),activate(V2)) p4: U14#(tt(),V1,V2) -> U15#(isNat(activate(V1)),activate(V2)) p5: U15#(tt(),V2) -> isNat#(activate(V2)) p6: isNat#(n__plus(V1,V2)) -> U11#(isNatKind(activate(V1)),activate(V1),activate(V2)) p7: U11#(tt(),V1,V2) -> isNatKind#(activate(V1)) p8: isNatKind#(n__plus(V1,V2)) -> U31#(isNatKind(activate(V1)),activate(V2)) p9: U31#(tt(),V2) -> isNatKind#(activate(V2)) p10: isNatKind#(n__plus(V1,V2)) -> isNatKind#(activate(V1)) p11: isNatKind#(n__plus(V1,V2)) -> activate#(V1) p12: activate#(n__plus(X1,X2)) -> plus#(activate(X1),activate(X2)) p13: plus#(N,|0|()) -> U51#(isNat(N),N) p14: U51#(tt(),N) -> U52#(isNatKind(activate(N)),activate(N)) p15: U52#(tt(),N) -> activate#(N) p16: activate#(n__plus(X1,X2)) -> activate#(X1) p17: U51#(tt(),N) -> isNatKind#(activate(N)) p18: isNatKind#(n__plus(V1,V2)) -> activate#(V2) p19: isNatKind#(n__s(V1)) -> isNatKind#(activate(V1)) p20: isNatKind#(n__s(V1)) -> activate#(V1) p21: U51#(tt(),N) -> activate#(N) p22: plus#(N,|0|()) -> isNat#(N) p23: isNat#(n__plus(V1,V2)) -> isNatKind#(activate(V1)) p24: isNat#(n__plus(V1,V2)) -> activate#(V1) p25: isNat#(n__plus(V1,V2)) -> activate#(V2) p26: isNat#(n__s(V1)) -> U21#(isNatKind(activate(V1)),activate(V1)) p27: U21#(tt(),V1) -> U22#(isNatKind(activate(V1)),activate(V1)) p28: U22#(tt(),V1) -> isNat#(activate(V1)) p29: isNat#(n__s(V1)) -> isNatKind#(activate(V1)) p30: isNat#(n__s(V1)) -> activate#(V1) p31: U22#(tt(),V1) -> activate#(V1) p32: U21#(tt(),V1) -> isNatKind#(activate(V1)) p33: U21#(tt(),V1) -> activate#(V1) p34: plus#(N,s(M)) -> U61#(isNat(M),M,N) p35: U61#(tt(),M,N) -> U62#(isNatKind(activate(M)),activate(M),activate(N)) p36: U62#(tt(),M,N) -> U63#(isNat(activate(N)),activate(M),activate(N)) p37: U63#(tt(),M,N) -> U64#(isNatKind(activate(N)),activate(M),activate(N)) p38: U64#(tt(),M,N) -> plus#(activate(N),activate(M)) p39: plus#(N,s(M)) -> isNat#(M) p40: U64#(tt(),M,N) -> activate#(N) p41: U64#(tt(),M,N) -> activate#(M) p42: U63#(tt(),M,N) -> isNatKind#(activate(N)) p43: U63#(tt(),M,N) -> activate#(N) p44: U63#(tt(),M,N) -> activate#(M) p45: U62#(tt(),M,N) -> isNat#(activate(N)) p46: U62#(tt(),M,N) -> activate#(N) p47: U62#(tt(),M,N) -> activate#(M) p48: U61#(tt(),M,N) -> isNatKind#(activate(M)) p49: U61#(tt(),M,N) -> activate#(M) p50: U61#(tt(),M,N) -> activate#(N) p51: U31#(tt(),V2) -> activate#(V2) p52: U11#(tt(),V1,V2) -> activate#(V1) p53: U11#(tt(),V1,V2) -> activate#(V2) p54: U15#(tt(),V2) -> activate#(V2) p55: U14#(tt(),V1,V2) -> isNat#(activate(V1)) p56: U14#(tt(),V1,V2) -> activate#(V1) p57: U14#(tt(),V1,V2) -> activate#(V2) p58: U13#(tt(),V1,V2) -> isNatKind#(activate(V2)) p59: U13#(tt(),V1,V2) -> activate#(V2) p60: U13#(tt(),V1,V2) -> activate#(V1) p61: U12#(tt(),V1,V2) -> isNatKind#(activate(V2)) p62: U12#(tt(),V1,V2) -> activate#(V1) and R consists of: r1: U11(tt(),V1,V2) -> U12(isNatKind(activate(V1)),activate(V1),activate(V2)) r2: U12(tt(),V1,V2) -> U13(isNatKind(activate(V2)),activate(V1),activate(V2)) r3: U13(tt(),V1,V2) -> U14(isNatKind(activate(V2)),activate(V1),activate(V2)) r4: U14(tt(),V1,V2) -> U15(isNat(activate(V1)),activate(V2)) r5: U15(tt(),V2) -> U16(isNat(activate(V2))) r6: U16(tt()) -> tt() r7: U21(tt(),V1) -> U22(isNatKind(activate(V1)),activate(V1)) r8: U22(tt(),V1) -> U23(isNat(activate(V1))) r9: U23(tt()) -> tt() r10: U31(tt(),V2) -> U32(isNatKind(activate(V2))) r11: U32(tt()) -> tt() r12: U41(tt()) -> tt() r13: U51(tt(),N) -> U52(isNatKind(activate(N)),activate(N)) r14: U52(tt(),N) -> activate(N) r15: U61(tt(),M,N) -> U62(isNatKind(activate(M)),activate(M),activate(N)) r16: U62(tt(),M,N) -> U63(isNat(activate(N)),activate(M),activate(N)) r17: U63(tt(),M,N) -> U64(isNatKind(activate(N)),activate(M),activate(N)) r18: U64(tt(),M,N) -> s(plus(activate(N),activate(M))) r19: isNat(n__0()) -> tt() r20: isNat(n__plus(V1,V2)) -> U11(isNatKind(activate(V1)),activate(V1),activate(V2)) r21: isNat(n__s(V1)) -> U21(isNatKind(activate(V1)),activate(V1)) r22: isNatKind(n__0()) -> tt() r23: isNatKind(n__plus(V1,V2)) -> U31(isNatKind(activate(V1)),activate(V2)) r24: isNatKind(n__s(V1)) -> U41(isNatKind(activate(V1))) r25: plus(N,|0|()) -> U51(isNat(N),N) r26: plus(N,s(M)) -> U61(isNat(M),M,N) r27: |0|() -> n__0() r28: plus(X1,X2) -> n__plus(X1,X2) r29: s(X) -> n__s(X) r30: activate(n__0()) -> |0|() r31: activate(n__plus(X1,X2)) -> plus(activate(X1),activate(X2)) r32: activate(n__s(X)) -> s(activate(X)) r33: activate(X) -> 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 Take the reduction pair: weighted path order base order: matrix interpretations: carrier: N^1 order: lexicographic order interpretations: U11#_A(x1,x2,x3) = x2 + x3 + 5 tt_A() = 1 U12#_A(x1,x2,x3) = x2 + x3 + 5 isNatKind_A(x1) = 4 activate_A(x1) = x1 U13#_A(x1,x2,x3) = x2 + x3 + 5 U14#_A(x1,x2,x3) = x2 + x3 + 5 U15#_A(x1,x2) = x2 + 5 isNat_A(x1) = 8 isNat#_A(x1) = x1 + 5 n__plus_A(x1,x2) = x1 + x2 isNatKind#_A(x1) = x1 + 5 U31#_A(x1,x2) = x2 + 5 activate#_A(x1) = x1 + 5 plus#_A(x1,x2) = x1 + x2 + 5 |0|_A() = 0 U51#_A(x1,x2) = x2 + 5 U52#_A(x1,x2) = x2 + 5 n__s_A(x1) = x1 + 12 U21#_A(x1,x2) = x2 + 13 U22#_A(x1,x2) = x2 + 6 s_A(x1) = x1 + 12 U61#_A(x1,x2,x3) = x2 + x3 + 16 U62#_A(x1,x2,x3) = x2 + x3 + 15 U63#_A(x1,x2,x3) = x1 + x2 + x3 + 6 U64#_A(x1,x2,x3) = x2 + x3 + 6 U16_A(x1) = 2 U15_A(x1,x2) = 3 U64_A(x1,x2,x3) = x2 + x3 + 12 plus_A(x1,x2) = x1 + x2 U14_A(x1,x2,x3) = 4 U63_A(x1,x2,x3) = x2 + x3 + 12 U13_A(x1,x2,x3) = 5 U23_A(x1) = 2 U52_A(x1,x2) = x2 U62_A(x1,x2,x3) = x2 + x3 + 12 U12_A(x1,x2,x3) = 6 U22_A(x1,x2) = 6 U32_A(x1) = 2 U51_A(x1,x2) = x2 U61_A(x1,x2,x3) = x2 + x3 + 12 U11_A(x1,x2,x3) = 7 U21_A(x1,x2) = 7 U31_A(x1,x2) = 3 U41_A(x1) = x1 n__0_A() = 0 precedence: U11# = tt = U12# = isNatKind = activate = U13# = U14# = U15# = isNat = isNat# = n__plus = isNatKind# = U31# = activate# = plus# = |0| = U51# = U52# = n__s = U21# = U22# = s = U61# = U62# = U63# = U64# = U16 = U15 = U64 = plus = U14 = U63 = U13 = U23 = U52 = U62 = U12 = U22 = U32 = U51 = U61 = U11 = U21 = U31 = U41 = n__0 partial status: pi(U11#) = [] pi(tt) = [] pi(U12#) = [] pi(isNatKind) = [] pi(activate) = [] pi(U13#) = [] pi(U14#) = [] pi(U15#) = [] pi(isNat) = [] pi(isNat#) = [] pi(n__plus) = [] pi(isNatKind#) = [] pi(U31#) = [] pi(activate#) = [] pi(plus#) = [] pi(|0|) = [] pi(U51#) = [] pi(U52#) = [] pi(n__s) = [] pi(U21#) = [] pi(U22#) = [] pi(s) = [] pi(U61#) = [] pi(U62#) = [] pi(U63#) = [] pi(U64#) = [] pi(U16) = [] pi(U15) = [] pi(U64) = [] pi(plus) = [] pi(U14) = [] pi(U63) = [] pi(U13) = [] pi(U23) = [] pi(U52) = [] pi(U62) = [] pi(U12) = [] pi(U22) = [] pi(U32) = [] pi(U51) = [] pi(U61) = [] pi(U11) = [] pi(U21) = [] pi(U31) = [] pi(U41) = [] pi(n__0) = [] The next rules are strictly ordered: p33 We remove them from the problem. -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: U11#(tt(),V1,V2) -> U12#(isNatKind(activate(V1)),activate(V1),activate(V2)) p2: U12#(tt(),V1,V2) -> U13#(isNatKind(activate(V2)),activate(V1),activate(V2)) p3: U13#(tt(),V1,V2) -> U14#(isNatKind(activate(V2)),activate(V1),activate(V2)) p4: U14#(tt(),V1,V2) -> U15#(isNat(activate(V1)),activate(V2)) p5: U15#(tt(),V2) -> isNat#(activate(V2)) p6: isNat#(n__plus(V1,V2)) -> U11#(isNatKind(activate(V1)),activate(V1),activate(V2)) p7: U11#(tt(),V1,V2) -> isNatKind#(activate(V1)) p8: isNatKind#(n__plus(V1,V2)) -> U31#(isNatKind(activate(V1)),activate(V2)) p9: U31#(tt(),V2) -> isNatKind#(activate(V2)) p10: isNatKind#(n__plus(V1,V2)) -> isNatKind#(activate(V1)) p11: isNatKind#(n__plus(V1,V2)) -> activate#(V1) p12: activate#(n__plus(X1,X2)) -> plus#(activate(X1),activate(X2)) p13: plus#(N,|0|()) -> U51#(isNat(N),N) p14: U51#(tt(),N) -> U52#(isNatKind(activate(N)),activate(N)) p15: U52#(tt(),N) -> activate#(N) p16: activate#(n__plus(X1,X2)) -> activate#(X1) p17: U51#(tt(),N) -> isNatKind#(activate(N)) p18: isNatKind#(n__plus(V1,V2)) -> activate#(V2) p19: isNatKind#(n__s(V1)) -> isNatKind#(activate(V1)) p20: isNatKind#(n__s(V1)) -> activate#(V1) p21: U51#(tt(),N) -> activate#(N) p22: plus#(N,|0|()) -> isNat#(N) p23: isNat#(n__plus(V1,V2)) -> isNatKind#(activate(V1)) p24: isNat#(n__plus(V1,V2)) -> activate#(V1) p25: isNat#(n__plus(V1,V2)) -> activate#(V2) p26: isNat#(n__s(V1)) -> U21#(isNatKind(activate(V1)),activate(V1)) p27: U21#(tt(),V1) -> U22#(isNatKind(activate(V1)),activate(V1)) p28: U22#(tt(),V1) -> isNat#(activate(V1)) p29: isNat#(n__s(V1)) -> isNatKind#(activate(V1)) p30: isNat#(n__s(V1)) -> activate#(V1) p31: U22#(tt(),V1) -> activate#(V1) p32: U21#(tt(),V1) -> isNatKind#(activate(V1)) p33: plus#(N,s(M)) -> U61#(isNat(M),M,N) p34: U61#(tt(),M,N) -> U62#(isNatKind(activate(M)),activate(M),activate(N)) p35: U62#(tt(),M,N) -> U63#(isNat(activate(N)),activate(M),activate(N)) p36: U63#(tt(),M,N) -> U64#(isNatKind(activate(N)),activate(M),activate(N)) p37: U64#(tt(),M,N) -> plus#(activate(N),activate(M)) p38: plus#(N,s(M)) -> isNat#(M) p39: U64#(tt(),M,N) -> activate#(N) p40: U64#(tt(),M,N) -> activate#(M) p41: U63#(tt(),M,N) -> isNatKind#(activate(N)) p42: U63#(tt(),M,N) -> activate#(N) p43: U63#(tt(),M,N) -> activate#(M) p44: U62#(tt(),M,N) -> isNat#(activate(N)) p45: U62#(tt(),M,N) -> activate#(N) p46: U62#(tt(),M,N) -> activate#(M) p47: U61#(tt(),M,N) -> isNatKind#(activate(M)) p48: U61#(tt(),M,N) -> activate#(M) p49: U61#(tt(),M,N) -> activate#(N) p50: U31#(tt(),V2) -> activate#(V2) p51: U11#(tt(),V1,V2) -> activate#(V1) p52: U11#(tt(),V1,V2) -> activate#(V2) p53: U15#(tt(),V2) -> activate#(V2) p54: U14#(tt(),V1,V2) -> isNat#(activate(V1)) p55: U14#(tt(),V1,V2) -> activate#(V1) p56: U14#(tt(),V1,V2) -> activate#(V2) p57: U13#(tt(),V1,V2) -> isNatKind#(activate(V2)) p58: U13#(tt(),V1,V2) -> activate#(V2) p59: U13#(tt(),V1,V2) -> activate#(V1) p60: U12#(tt(),V1,V2) -> isNatKind#(activate(V2)) p61: U12#(tt(),V1,V2) -> activate#(V1) and R consists of: r1: U11(tt(),V1,V2) -> U12(isNatKind(activate(V1)),activate(V1),activate(V2)) r2: U12(tt(),V1,V2) -> U13(isNatKind(activate(V2)),activate(V1),activate(V2)) r3: U13(tt(),V1,V2) -> U14(isNatKind(activate(V2)),activate(V1),activate(V2)) r4: U14(tt(),V1,V2) -> U15(isNat(activate(V1)),activate(V2)) r5: U15(tt(),V2) -> U16(isNat(activate(V2))) r6: U16(tt()) -> tt() r7: U21(tt(),V1) -> U22(isNatKind(activate(V1)),activate(V1)) r8: U22(tt(),V1) -> U23(isNat(activate(V1))) r9: U23(tt()) -> tt() r10: U31(tt(),V2) -> U32(isNatKind(activate(V2))) r11: U32(tt()) -> tt() r12: U41(tt()) -> tt() r13: U51(tt(),N) -> U52(isNatKind(activate(N)),activate(N)) r14: U52(tt(),N) -> activate(N) r15: U61(tt(),M,N) -> U62(isNatKind(activate(M)),activate(M),activate(N)) r16: U62(tt(),M,N) -> U63(isNat(activate(N)),activate(M),activate(N)) r17: U63(tt(),M,N) -> U64(isNatKind(activate(N)),activate(M),activate(N)) r18: U64(tt(),M,N) -> s(plus(activate(N),activate(M))) r19: isNat(n__0()) -> tt() r20: isNat(n__plus(V1,V2)) -> U11(isNatKind(activate(V1)),activate(V1),activate(V2)) r21: isNat(n__s(V1)) -> U21(isNatKind(activate(V1)),activate(V1)) r22: isNatKind(n__0()) -> tt() r23: isNatKind(n__plus(V1,V2)) -> U31(isNatKind(activate(V1)),activate(V2)) r24: isNatKind(n__s(V1)) -> U41(isNatKind(activate(V1))) r25: plus(N,|0|()) -> U51(isNat(N),N) r26: plus(N,s(M)) -> U61(isNat(M),M,N) r27: |0|() -> n__0() r28: plus(X1,X2) -> n__plus(X1,X2) r29: s(X) -> n__s(X) r30: activate(n__0()) -> |0|() r31: activate(n__plus(X1,X2)) -> plus(activate(X1),activate(X2)) r32: activate(n__s(X)) -> s(activate(X)) r33: activate(X) -> 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, p30, p31, p32, p33, p34, p35, p36, p37, p38, p39, p40, p41, p42, p43, p44, p45, p46, p47, p48, p49, p50, p51, p52, p53, p54, p55, p56, p57, p58, p59, p60, p61} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: U11#(tt(),V1,V2) -> U12#(isNatKind(activate(V1)),activate(V1),activate(V2)) p2: U12#(tt(),V1,V2) -> activate#(V1) p3: activate#(n__plus(X1,X2)) -> activate#(X1) p4: activate#(n__plus(X1,X2)) -> plus#(activate(X1),activate(X2)) p5: plus#(N,s(M)) -> isNat#(M) p6: isNat#(n__s(V1)) -> activate#(V1) p7: isNat#(n__s(V1)) -> isNatKind#(activate(V1)) p8: isNatKind#(n__s(V1)) -> activate#(V1) p9: isNatKind#(n__s(V1)) -> isNatKind#(activate(V1)) p10: isNatKind#(n__plus(V1,V2)) -> activate#(V2) p11: isNatKind#(n__plus(V1,V2)) -> activate#(V1) p12: isNatKind#(n__plus(V1,V2)) -> isNatKind#(activate(V1)) p13: isNatKind#(n__plus(V1,V2)) -> U31#(isNatKind(activate(V1)),activate(V2)) p14: U31#(tt(),V2) -> activate#(V2) p15: U31#(tt(),V2) -> isNatKind#(activate(V2)) p16: isNat#(n__s(V1)) -> U21#(isNatKind(activate(V1)),activate(V1)) p17: U21#(tt(),V1) -> isNatKind#(activate(V1)) p18: U21#(tt(),V1) -> U22#(isNatKind(activate(V1)),activate(V1)) p19: U22#(tt(),V1) -> activate#(V1) p20: U22#(tt(),V1) -> isNat#(activate(V1)) p21: isNat#(n__plus(V1,V2)) -> activate#(V2) p22: isNat#(n__plus(V1,V2)) -> activate#(V1) p23: isNat#(n__plus(V1,V2)) -> isNatKind#(activate(V1)) p24: isNat#(n__plus(V1,V2)) -> U11#(isNatKind(activate(V1)),activate(V1),activate(V2)) p25: U11#(tt(),V1,V2) -> activate#(V2) p26: U11#(tt(),V1,V2) -> activate#(V1) p27: U11#(tt(),V1,V2) -> isNatKind#(activate(V1)) p28: plus#(N,s(M)) -> U61#(isNat(M),M,N) p29: U61#(tt(),M,N) -> activate#(N) p30: U61#(tt(),M,N) -> activate#(M) p31: U61#(tt(),M,N) -> isNatKind#(activate(M)) p32: U61#(tt(),M,N) -> U62#(isNatKind(activate(M)),activate(M),activate(N)) p33: U62#(tt(),M,N) -> activate#(M) p34: U62#(tt(),M,N) -> activate#(N) p35: U62#(tt(),M,N) -> isNat#(activate(N)) p36: U62#(tt(),M,N) -> U63#(isNat(activate(N)),activate(M),activate(N)) p37: U63#(tt(),M,N) -> activate#(M) p38: U63#(tt(),M,N) -> activate#(N) p39: U63#(tt(),M,N) -> isNatKind#(activate(N)) p40: U63#(tt(),M,N) -> U64#(isNatKind(activate(N)),activate(M),activate(N)) p41: U64#(tt(),M,N) -> activate#(M) p42: U64#(tt(),M,N) -> activate#(N) p43: U64#(tt(),M,N) -> plus#(activate(N),activate(M)) p44: plus#(N,|0|()) -> isNat#(N) p45: plus#(N,|0|()) -> U51#(isNat(N),N) p46: U51#(tt(),N) -> activate#(N) p47: U51#(tt(),N) -> isNatKind#(activate(N)) p48: U51#(tt(),N) -> U52#(isNatKind(activate(N)),activate(N)) p49: U52#(tt(),N) -> activate#(N) p50: U12#(tt(),V1,V2) -> isNatKind#(activate(V2)) p51: U12#(tt(),V1,V2) -> U13#(isNatKind(activate(V2)),activate(V1),activate(V2)) p52: U13#(tt(),V1,V2) -> activate#(V1) p53: U13#(tt(),V1,V2) -> activate#(V2) p54: U13#(tt(),V1,V2) -> isNatKind#(activate(V2)) p55: U13#(tt(),V1,V2) -> U14#(isNatKind(activate(V2)),activate(V1),activate(V2)) p56: U14#(tt(),V1,V2) -> activate#(V2) p57: U14#(tt(),V1,V2) -> activate#(V1) p58: U14#(tt(),V1,V2) -> isNat#(activate(V1)) p59: U14#(tt(),V1,V2) -> U15#(isNat(activate(V1)),activate(V2)) p60: U15#(tt(),V2) -> activate#(V2) p61: U15#(tt(),V2) -> isNat#(activate(V2)) and R consists of: r1: U11(tt(),V1,V2) -> U12(isNatKind(activate(V1)),activate(V1),activate(V2)) r2: U12(tt(),V1,V2) -> U13(isNatKind(activate(V2)),activate(V1),activate(V2)) r3: U13(tt(),V1,V2) -> U14(isNatKind(activate(V2)),activate(V1),activate(V2)) r4: U14(tt(),V1,V2) -> U15(isNat(activate(V1)),activate(V2)) r5: U15(tt(),V2) -> U16(isNat(activate(V2))) r6: U16(tt()) -> tt() r7: U21(tt(),V1) -> U22(isNatKind(activate(V1)),activate(V1)) r8: U22(tt(),V1) -> U23(isNat(activate(V1))) r9: U23(tt()) -> tt() r10: U31(tt(),V2) -> U32(isNatKind(activate(V2))) r11: U32(tt()) -> tt() r12: U41(tt()) -> tt() r13: U51(tt(),N) -> U52(isNatKind(activate(N)),activate(N)) r14: U52(tt(),N) -> activate(N) r15: U61(tt(),M,N) -> U62(isNatKind(activate(M)),activate(M),activate(N)) r16: U62(tt(),M,N) -> U63(isNat(activate(N)),activate(M),activate(N)) r17: U63(tt(),M,N) -> U64(isNatKind(activate(N)),activate(M),activate(N)) r18: U64(tt(),M,N) -> s(plus(activate(N),activate(M))) r19: isNat(n__0()) -> tt() r20: isNat(n__plus(V1,V2)) -> U11(isNatKind(activate(V1)),activate(V1),activate(V2)) r21: isNat(n__s(V1)) -> U21(isNatKind(activate(V1)),activate(V1)) r22: isNatKind(n__0()) -> tt() r23: isNatKind(n__plus(V1,V2)) -> U31(isNatKind(activate(V1)),activate(V2)) r24: isNatKind(n__s(V1)) -> U41(isNatKind(activate(V1))) r25: plus(N,|0|()) -> U51(isNat(N),N) r26: plus(N,s(M)) -> U61(isNat(M),M,N) r27: |0|() -> n__0() r28: plus(X1,X2) -> n__plus(X1,X2) r29: s(X) -> n__s(X) r30: activate(n__0()) -> |0|() r31: activate(n__plus(X1,X2)) -> plus(activate(X1),activate(X2)) r32: activate(n__s(X)) -> s(activate(X)) r33: activate(X) -> 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 Take the reduction pair: weighted path order base order: matrix interpretations: carrier: N^1 order: lexicographic order interpretations: U11#_A(x1,x2,x3) = x2 + x3 + 4 tt_A() = 0 U12#_A(x1,x2,x3) = x2 + x3 + 4 isNatKind_A(x1) = x1 activate_A(x1) = x1 activate#_A(x1) = x1 + 4 n__plus_A(x1,x2) = x1 + x2 + 3 plus#_A(x1,x2) = x1 + x2 s_A(x1) = x1 + 7 isNat#_A(x1) = x1 + 1 n__s_A(x1) = x1 + 7 isNatKind#_A(x1) = x1 + 2 U31#_A(x1,x2) = x2 + 5 U21#_A(x1,x2) = x2 + 6 U22#_A(x1,x2) = x2 + 5 U61#_A(x1,x2,x3) = x2 + x3 + 6 isNat_A(x1) = x1 + 11 U62#_A(x1,x2,x3) = x2 + x3 + 6 U63#_A(x1,x2,x3) = x2 + x3 + 5 U64#_A(x1,x2,x3) = x2 + x3 + 5 |0|_A() = 5 U51#_A(x1,x2) = x2 + 5 U52#_A(x1,x2) = x2 + 5 U13#_A(x1,x2,x3) = x2 + x3 + 4 U14#_A(x1,x2,x3) = x2 + x3 + 4 U15#_A(x1,x2) = x2 + 4 U16_A(x1) = 1 U15_A(x1,x2) = 2 U64_A(x1,x2,x3) = x2 + x3 + 10 plus_A(x1,x2) = x1 + x2 + 3 U14_A(x1,x2,x3) = 3 U63_A(x1,x2,x3) = x2 + x3 + 10 U13_A(x1,x2,x3) = 4 U23_A(x1) = 1 U52_A(x1,x2) = x2 + 1 U62_A(x1,x2,x3) = x2 + x3 + 10 U12_A(x1,x2,x3) = 5 U22_A(x1,x2) = 2 U32_A(x1) = 1 U51_A(x1,x2) = x2 + 6 U61_A(x1,x2,x3) = x2 + x3 + 10 U11_A(x1,x2,x3) = 6 U21_A(x1,x2) = 8 U31_A(x1,x2) = 2 U41_A(x1) = 0 n__0_A() = 5 precedence: isNatKind = U41 > U16 > U14 > U15 > isNat = U51 = U21 > U22 > n__plus = plus = U23 = U62 = U61 > tt = U32 > U64 = U63 > U11# = U12# = activate = activate# = plus# = s = isNat# = isNatKind# = U31# = U21# = U22# = U61# = U62# = U63# = U64# = U51# = U52# = U13# = U14# = U15# > |0| > n__0 > U13 = U52 > U31 > n__s > U12 = U11 partial status: pi(U11#) = [] pi(tt) = [] pi(U12#) = [] pi(isNatKind) = [1] pi(activate) = [1] pi(activate#) = [] pi(n__plus) = [] pi(plus#) = [] pi(s) = [] pi(isNat#) = [] pi(n__s) = [] pi(isNatKind#) = [] pi(U31#) = [] pi(U21#) = [] pi(U22#) = [] pi(U61#) = [] pi(isNat) = [] pi(U62#) = [] pi(U63#) = [] pi(U64#) = [] pi(|0|) = [] pi(U51#) = [] pi(U52#) = [] pi(U13#) = [] pi(U14#) = [] pi(U15#) = [] pi(U16) = [] pi(U15) = [] pi(U64) = [] pi(plus) = [] pi(U14) = [] pi(U63) = [] pi(U13) = [] pi(U23) = [] pi(U52) = [2] pi(U62) = [] pi(U12) = [] pi(U22) = [] pi(U32) = [] pi(U51) = [2] pi(U61) = [] pi(U11) = [] pi(U21) = [] pi(U31) = [] pi(U41) = [] pi(n__0) = [] The next rules are strictly ordered: p9 We remove them from the problem. -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: U11#(tt(),V1,V2) -> U12#(isNatKind(activate(V1)),activate(V1),activate(V2)) p2: U12#(tt(),V1,V2) -> activate#(V1) p3: activate#(n__plus(X1,X2)) -> activate#(X1) p4: activate#(n__plus(X1,X2)) -> plus#(activate(X1),activate(X2)) p5: plus#(N,s(M)) -> isNat#(M) p6: isNat#(n__s(V1)) -> activate#(V1) p7: isNat#(n__s(V1)) -> isNatKind#(activate(V1)) p8: isNatKind#(n__s(V1)) -> activate#(V1) p9: isNatKind#(n__plus(V1,V2)) -> activate#(V2) p10: isNatKind#(n__plus(V1,V2)) -> activate#(V1) p11: isNatKind#(n__plus(V1,V2)) -> isNatKind#(activate(V1)) p12: isNatKind#(n__plus(V1,V2)) -> U31#(isNatKind(activate(V1)),activate(V2)) p13: U31#(tt(),V2) -> activate#(V2) p14: U31#(tt(),V2) -> isNatKind#(activate(V2)) p15: isNat#(n__s(V1)) -> U21#(isNatKind(activate(V1)),activate(V1)) p16: U21#(tt(),V1) -> isNatKind#(activate(V1)) p17: U21#(tt(),V1) -> U22#(isNatKind(activate(V1)),activate(V1)) p18: U22#(tt(),V1) -> activate#(V1) p19: U22#(tt(),V1) -> isNat#(activate(V1)) p20: isNat#(n__plus(V1,V2)) -> activate#(V2) p21: isNat#(n__plus(V1,V2)) -> activate#(V1) p22: isNat#(n__plus(V1,V2)) -> isNatKind#(activate(V1)) p23: isNat#(n__plus(V1,V2)) -> U11#(isNatKind(activate(V1)),activate(V1),activate(V2)) p24: U11#(tt(),V1,V2) -> activate#(V2) p25: U11#(tt(),V1,V2) -> activate#(V1) p26: U11#(tt(),V1,V2) -> isNatKind#(activate(V1)) p27: plus#(N,s(M)) -> U61#(isNat(M),M,N) p28: U61#(tt(),M,N) -> activate#(N) p29: U61#(tt(),M,N) -> activate#(M) p30: U61#(tt(),M,N) -> isNatKind#(activate(M)) p31: U61#(tt(),M,N) -> U62#(isNatKind(activate(M)),activate(M),activate(N)) p32: U62#(tt(),M,N) -> activate#(M) p33: U62#(tt(),M,N) -> activate#(N) p34: U62#(tt(),M,N) -> isNat#(activate(N)) p35: U62#(tt(),M,N) -> U63#(isNat(activate(N)),activate(M),activate(N)) p36: U63#(tt(),M,N) -> activate#(M) p37: U63#(tt(),M,N) -> activate#(N) p38: U63#(tt(),M,N) -> isNatKind#(activate(N)) p39: U63#(tt(),M,N) -> U64#(isNatKind(activate(N)),activate(M),activate(N)) p40: U64#(tt(),M,N) -> activate#(M) p41: U64#(tt(),M,N) -> activate#(N) p42: U64#(tt(),M,N) -> plus#(activate(N),activate(M)) p43: plus#(N,|0|()) -> isNat#(N) p44: plus#(N,|0|()) -> U51#(isNat(N),N) p45: U51#(tt(),N) -> activate#(N) p46: U51#(tt(),N) -> isNatKind#(activate(N)) p47: U51#(tt(),N) -> U52#(isNatKind(activate(N)),activate(N)) p48: U52#(tt(),N) -> activate#(N) p49: U12#(tt(),V1,V2) -> isNatKind#(activate(V2)) p50: U12#(tt(),V1,V2) -> U13#(isNatKind(activate(V2)),activate(V1),activate(V2)) p51: U13#(tt(),V1,V2) -> activate#(V1) p52: U13#(tt(),V1,V2) -> activate#(V2) p53: U13#(tt(),V1,V2) -> isNatKind#(activate(V2)) p54: U13#(tt(),V1,V2) -> U14#(isNatKind(activate(V2)),activate(V1),activate(V2)) p55: U14#(tt(),V1,V2) -> activate#(V2) p56: U14#(tt(),V1,V2) -> activate#(V1) p57: U14#(tt(),V1,V2) -> isNat#(activate(V1)) p58: U14#(tt(),V1,V2) -> U15#(isNat(activate(V1)),activate(V2)) p59: U15#(tt(),V2) -> activate#(V2) p60: U15#(tt(),V2) -> isNat#(activate(V2)) and R consists of: r1: U11(tt(),V1,V2) -> U12(isNatKind(activate(V1)),activate(V1),activate(V2)) r2: U12(tt(),V1,V2) -> U13(isNatKind(activate(V2)),activate(V1),activate(V2)) r3: U13(tt(),V1,V2) -> U14(isNatKind(activate(V2)),activate(V1),activate(V2)) r4: U14(tt(),V1,V2) -> U15(isNat(activate(V1)),activate(V2)) r5: U15(tt(),V2) -> U16(isNat(activate(V2))) r6: U16(tt()) -> tt() r7: U21(tt(),V1) -> U22(isNatKind(activate(V1)),activate(V1)) r8: U22(tt(),V1) -> U23(isNat(activate(V1))) r9: U23(tt()) -> tt() r10: U31(tt(),V2) -> U32(isNatKind(activate(V2))) r11: U32(tt()) -> tt() r12: U41(tt()) -> tt() r13: U51(tt(),N) -> U52(isNatKind(activate(N)),activate(N)) r14: U52(tt(),N) -> activate(N) r15: U61(tt(),M,N) -> U62(isNatKind(activate(M)),activate(M),activate(N)) r16: U62(tt(),M,N) -> U63(isNat(activate(N)),activate(M),activate(N)) r17: U63(tt(),M,N) -> U64(isNatKind(activate(N)),activate(M),activate(N)) r18: U64(tt(),M,N) -> s(plus(activate(N),activate(M))) r19: isNat(n__0()) -> tt() r20: isNat(n__plus(V1,V2)) -> U11(isNatKind(activate(V1)),activate(V1),activate(V2)) r21: isNat(n__s(V1)) -> U21(isNatKind(activate(V1)),activate(V1)) r22: isNatKind(n__0()) -> tt() r23: isNatKind(n__plus(V1,V2)) -> U31(isNatKind(activate(V1)),activate(V2)) r24: isNatKind(n__s(V1)) -> U41(isNatKind(activate(V1))) r25: plus(N,|0|()) -> U51(isNat(N),N) r26: plus(N,s(M)) -> U61(isNat(M),M,N) r27: |0|() -> n__0() r28: plus(X1,X2) -> n__plus(X1,X2) r29: s(X) -> n__s(X) r30: activate(n__0()) -> |0|() r31: activate(n__plus(X1,X2)) -> plus(activate(X1),activate(X2)) r32: activate(n__s(X)) -> s(activate(X)) r33: activate(X) -> 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, p30, p31, p32, p33, p34, p35, p36, p37, p38, p39, p40, p41, p42, p43, p44, p45, p46, p47, p48, p49, p50, p51, p52, p53, p54, p55, p56, p57, p58, p59, p60} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: U11#(tt(),V1,V2) -> U12#(isNatKind(activate(V1)),activate(V1),activate(V2)) p2: U12#(tt(),V1,V2) -> U13#(isNatKind(activate(V2)),activate(V1),activate(V2)) p3: U13#(tt(),V1,V2) -> U14#(isNatKind(activate(V2)),activate(V1),activate(V2)) p4: U14#(tt(),V1,V2) -> U15#(isNat(activate(V1)),activate(V2)) p5: U15#(tt(),V2) -> isNat#(activate(V2)) p6: isNat#(n__plus(V1,V2)) -> U11#(isNatKind(activate(V1)),activate(V1),activate(V2)) p7: U11#(tt(),V1,V2) -> isNatKind#(activate(V1)) p8: isNatKind#(n__plus(V1,V2)) -> U31#(isNatKind(activate(V1)),activate(V2)) p9: U31#(tt(),V2) -> isNatKind#(activate(V2)) p10: isNatKind#(n__plus(V1,V2)) -> isNatKind#(activate(V1)) p11: isNatKind#(n__plus(V1,V2)) -> activate#(V1) p12: activate#(n__plus(X1,X2)) -> plus#(activate(X1),activate(X2)) p13: plus#(N,|0|()) -> U51#(isNat(N),N) p14: U51#(tt(),N) -> U52#(isNatKind(activate(N)),activate(N)) p15: U52#(tt(),N) -> activate#(N) p16: activate#(n__plus(X1,X2)) -> activate#(X1) p17: U51#(tt(),N) -> isNatKind#(activate(N)) p18: isNatKind#(n__plus(V1,V2)) -> activate#(V2) p19: isNatKind#(n__s(V1)) -> activate#(V1) p20: U51#(tt(),N) -> activate#(N) p21: plus#(N,|0|()) -> isNat#(N) p22: isNat#(n__plus(V1,V2)) -> isNatKind#(activate(V1)) p23: isNat#(n__plus(V1,V2)) -> activate#(V1) p24: isNat#(n__plus(V1,V2)) -> activate#(V2) p25: isNat#(n__s(V1)) -> U21#(isNatKind(activate(V1)),activate(V1)) p26: U21#(tt(),V1) -> U22#(isNatKind(activate(V1)),activate(V1)) p27: U22#(tt(),V1) -> isNat#(activate(V1)) p28: isNat#(n__s(V1)) -> isNatKind#(activate(V1)) p29: isNat#(n__s(V1)) -> activate#(V1) p30: U22#(tt(),V1) -> activate#(V1) p31: U21#(tt(),V1) -> isNatKind#(activate(V1)) p32: plus#(N,s(M)) -> U61#(isNat(M),M,N) p33: U61#(tt(),M,N) -> U62#(isNatKind(activate(M)),activate(M),activate(N)) p34: U62#(tt(),M,N) -> U63#(isNat(activate(N)),activate(M),activate(N)) p35: U63#(tt(),M,N) -> U64#(isNatKind(activate(N)),activate(M),activate(N)) p36: U64#(tt(),M,N) -> plus#(activate(N),activate(M)) p37: plus#(N,s(M)) -> isNat#(M) p38: U64#(tt(),M,N) -> activate#(N) p39: U64#(tt(),M,N) -> activate#(M) p40: U63#(tt(),M,N) -> isNatKind#(activate(N)) p41: U63#(tt(),M,N) -> activate#(N) p42: U63#(tt(),M,N) -> activate#(M) p43: U62#(tt(),M,N) -> isNat#(activate(N)) p44: U62#(tt(),M,N) -> activate#(N) p45: U62#(tt(),M,N) -> activate#(M) p46: U61#(tt(),M,N) -> isNatKind#(activate(M)) p47: U61#(tt(),M,N) -> activate#(M) p48: U61#(tt(),M,N) -> activate#(N) p49: U31#(tt(),V2) -> activate#(V2) p50: U11#(tt(),V1,V2) -> activate#(V1) p51: U11#(tt(),V1,V2) -> activate#(V2) p52: U15#(tt(),V2) -> activate#(V2) p53: U14#(tt(),V1,V2) -> isNat#(activate(V1)) p54: U14#(tt(),V1,V2) -> activate#(V1) p55: U14#(tt(),V1,V2) -> activate#(V2) p56: U13#(tt(),V1,V2) -> isNatKind#(activate(V2)) p57: U13#(tt(),V1,V2) -> activate#(V2) p58: U13#(tt(),V1,V2) -> activate#(V1) p59: U12#(tt(),V1,V2) -> isNatKind#(activate(V2)) p60: U12#(tt(),V1,V2) -> activate#(V1) and R consists of: r1: U11(tt(),V1,V2) -> U12(isNatKind(activate(V1)),activate(V1),activate(V2)) r2: U12(tt(),V1,V2) -> U13(isNatKind(activate(V2)),activate(V1),activate(V2)) r3: U13(tt(),V1,V2) -> U14(isNatKind(activate(V2)),activate(V1),activate(V2)) r4: U14(tt(),V1,V2) -> U15(isNat(activate(V1)),activate(V2)) r5: U15(tt(),V2) -> U16(isNat(activate(V2))) r6: U16(tt()) -> tt() r7: U21(tt(),V1) -> U22(isNatKind(activate(V1)),activate(V1)) r8: U22(tt(),V1) -> U23(isNat(activate(V1))) r9: U23(tt()) -> tt() r10: U31(tt(),V2) -> U32(isNatKind(activate(V2))) r11: U32(tt()) -> tt() r12: U41(tt()) -> tt() r13: U51(tt(),N) -> U52(isNatKind(activate(N)),activate(N)) r14: U52(tt(),N) -> activate(N) r15: U61(tt(),M,N) -> U62(isNatKind(activate(M)),activate(M),activate(N)) r16: U62(tt(),M,N) -> U63(isNat(activate(N)),activate(M),activate(N)) r17: U63(tt(),M,N) -> U64(isNatKind(activate(N)),activate(M),activate(N)) r18: U64(tt(),M,N) -> s(plus(activate(N),activate(M))) r19: isNat(n__0()) -> tt() r20: isNat(n__plus(V1,V2)) -> U11(isNatKind(activate(V1)),activate(V1),activate(V2)) r21: isNat(n__s(V1)) -> U21(isNatKind(activate(V1)),activate(V1)) r22: isNatKind(n__0()) -> tt() r23: isNatKind(n__plus(V1,V2)) -> U31(isNatKind(activate(V1)),activate(V2)) r24: isNatKind(n__s(V1)) -> U41(isNatKind(activate(V1))) r25: plus(N,|0|()) -> U51(isNat(N),N) r26: plus(N,s(M)) -> U61(isNat(M),M,N) r27: |0|() -> n__0() r28: plus(X1,X2) -> n__plus(X1,X2) r29: s(X) -> n__s(X) r30: activate(n__0()) -> |0|() r31: activate(n__plus(X1,X2)) -> plus(activate(X1),activate(X2)) r32: activate(n__s(X)) -> s(activate(X)) r33: activate(X) -> 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 Take the reduction pair: weighted path order base order: matrix interpretations: carrier: N^1 order: lexicographic order interpretations: U11#_A(x1,x2,x3) = x2 + x3 + 12 tt_A() = 8 U12#_A(x1,x2,x3) = x2 + x3 + 12 isNatKind_A(x1) = x1 activate_A(x1) = x1 U13#_A(x1,x2,x3) = x2 + x3 + 12 U14#_A(x1,x2,x3) = x2 + x3 + 12 U15#_A(x1,x2) = x2 + 12 isNat_A(x1) = x1 + 7 isNat#_A(x1) = x1 + 12 n__plus_A(x1,x2) = x1 + x2 isNatKind#_A(x1) = x1 + 12 U31#_A(x1,x2) = x1 + x2 + 4 activate#_A(x1) = x1 + 12 plus#_A(x1,x2) = x1 + x2 + 1 |0|_A() = 11 U51#_A(x1,x2) = x2 + 12 U52#_A(x1,x2) = x2 + 12 n__s_A(x1) = x1 + 17 U21#_A(x1,x2) = x2 + 14 U22#_A(x1,x2) = x2 + 13 s_A(x1) = x1 + 17 U61#_A(x1,x2,x3) = x2 + x3 + 16 U62#_A(x1,x2,x3) = x2 + x3 + 15 U63#_A(x1,x2,x3) = x2 + x3 + 14 U64#_A(x1,x2,x3) = x2 + x3 + 13 U16_A(x1) = 9 U15_A(x1,x2) = 10 U64_A(x1,x2,x3) = x2 + x3 + 17 plus_A(x1,x2) = x1 + x2 U14_A(x1,x2,x3) = x1 + 3 U63_A(x1,x2,x3) = x2 + x3 + 17 U13_A(x1,x2,x3) = x3 + 4 U23_A(x1) = 9 U52_A(x1,x2) = x2 + 9 U62_A(x1,x2,x3) = x2 + x3 + 17 U12_A(x1,x2,x3) = x3 + 5 U22_A(x1,x2) = 10 U32_A(x1) = x1 + 1 U51_A(x1,x2) = x2 + 10 U61_A(x1,x2,x3) = x2 + x3 + 17 U11_A(x1,x2,x3) = x3 + 6 U21_A(x1,x2) = 18 U31_A(x1,x2) = x1 + x2 U41_A(x1) = 9 n__0_A() = 11 precedence: isNatKind > isNat > U21 > U31 > U11# = U12# = U13# = U14# = U15# = isNat# = n__plus = isNatKind# = U31# = activate# = plus# = U51# = U52# = U21# = U22# = plus = U52 = U51 > U61# = U62# = U63# = U64# > |0| = U32 = U41 = n__0 > U11 > U23 = U22 > tt = activate = U16 = U15 = U14 = U13 = U12 > U61 > U62 > n__s = s = U64 = U63 partial status: pi(U11#) = [] pi(tt) = [] pi(U12#) = [] pi(isNatKind) = [] pi(activate) = [1] pi(U13#) = [] pi(U14#) = [] pi(U15#) = [] pi(isNat) = [1] pi(isNat#) = [] pi(n__plus) = [] pi(isNatKind#) = [] pi(U31#) = [] pi(activate#) = [] pi(plus#) = [] pi(|0|) = [] pi(U51#) = [] pi(U52#) = [] pi(n__s) = [] pi(U21#) = [] pi(U22#) = [] pi(s) = [] pi(U61#) = [2] pi(U62#) = [] pi(U63#) = [] pi(U64#) = [] pi(U16) = [] pi(U15) = [] pi(U64) = [] pi(plus) = [] pi(U14) = [] pi(U63) = [] pi(U13) = [] pi(U23) = [] pi(U52) = [] pi(U62) = [] pi(U12) = [] pi(U22) = [] pi(U32) = [] pi(U51) = [] pi(U61) = [] pi(U11) = [] pi(U21) = [] pi(U31) = [] pi(U41) = [] pi(n__0) = [] The next rules are strictly ordered: p12 We remove them from the problem. -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: U11#(tt(),V1,V2) -> U12#(isNatKind(activate(V1)),activate(V1),activate(V2)) p2: U12#(tt(),V1,V2) -> U13#(isNatKind(activate(V2)),activate(V1),activate(V2)) p3: U13#(tt(),V1,V2) -> U14#(isNatKind(activate(V2)),activate(V1),activate(V2)) p4: U14#(tt(),V1,V2) -> U15#(isNat(activate(V1)),activate(V2)) p5: U15#(tt(),V2) -> isNat#(activate(V2)) p6: isNat#(n__plus(V1,V2)) -> U11#(isNatKind(activate(V1)),activate(V1),activate(V2)) p7: U11#(tt(),V1,V2) -> isNatKind#(activate(V1)) p8: isNatKind#(n__plus(V1,V2)) -> U31#(isNatKind(activate(V1)),activate(V2)) p9: U31#(tt(),V2) -> isNatKind#(activate(V2)) p10: isNatKind#(n__plus(V1,V2)) -> isNatKind#(activate(V1)) p11: isNatKind#(n__plus(V1,V2)) -> activate#(V1) p12: plus#(N,|0|()) -> U51#(isNat(N),N) p13: U51#(tt(),N) -> U52#(isNatKind(activate(N)),activate(N)) p14: U52#(tt(),N) -> activate#(N) p15: activate#(n__plus(X1,X2)) -> activate#(X1) p16: U51#(tt(),N) -> isNatKind#(activate(N)) p17: isNatKind#(n__plus(V1,V2)) -> activate#(V2) p18: isNatKind#(n__s(V1)) -> activate#(V1) p19: U51#(tt(),N) -> activate#(N) p20: plus#(N,|0|()) -> isNat#(N) p21: isNat#(n__plus(V1,V2)) -> isNatKind#(activate(V1)) p22: isNat#(n__plus(V1,V2)) -> activate#(V1) p23: isNat#(n__plus(V1,V2)) -> activate#(V2) p24: isNat#(n__s(V1)) -> U21#(isNatKind(activate(V1)),activate(V1)) p25: U21#(tt(),V1) -> U22#(isNatKind(activate(V1)),activate(V1)) p26: U22#(tt(),V1) -> isNat#(activate(V1)) p27: isNat#(n__s(V1)) -> isNatKind#(activate(V1)) p28: isNat#(n__s(V1)) -> activate#(V1) p29: U22#(tt(),V1) -> activate#(V1) p30: U21#(tt(),V1) -> isNatKind#(activate(V1)) p31: plus#(N,s(M)) -> U61#(isNat(M),M,N) p32: U61#(tt(),M,N) -> U62#(isNatKind(activate(M)),activate(M),activate(N)) p33: U62#(tt(),M,N) -> U63#(isNat(activate(N)),activate(M),activate(N)) p34: U63#(tt(),M,N) -> U64#(isNatKind(activate(N)),activate(M),activate(N)) p35: U64#(tt(),M,N) -> plus#(activate(N),activate(M)) p36: plus#(N,s(M)) -> isNat#(M) p37: U64#(tt(),M,N) -> activate#(N) p38: U64#(tt(),M,N) -> activate#(M) p39: U63#(tt(),M,N) -> isNatKind#(activate(N)) p40: U63#(tt(),M,N) -> activate#(N) p41: U63#(tt(),M,N) -> activate#(M) p42: U62#(tt(),M,N) -> isNat#(activate(N)) p43: U62#(tt(),M,N) -> activate#(N) p44: U62#(tt(),M,N) -> activate#(M) p45: U61#(tt(),M,N) -> isNatKind#(activate(M)) p46: U61#(tt(),M,N) -> activate#(M) p47: U61#(tt(),M,N) -> activate#(N) p48: U31#(tt(),V2) -> activate#(V2) p49: U11#(tt(),V1,V2) -> activate#(V1) p50: U11#(tt(),V1,V2) -> activate#(V2) p51: U15#(tt(),V2) -> activate#(V2) p52: U14#(tt(),V1,V2) -> isNat#(activate(V1)) p53: U14#(tt(),V1,V2) -> activate#(V1) p54: U14#(tt(),V1,V2) -> activate#(V2) p55: U13#(tt(),V1,V2) -> isNatKind#(activate(V2)) p56: U13#(tt(),V1,V2) -> activate#(V2) p57: U13#(tt(),V1,V2) -> activate#(V1) p58: U12#(tt(),V1,V2) -> isNatKind#(activate(V2)) p59: U12#(tt(),V1,V2) -> activate#(V1) and R consists of: r1: U11(tt(),V1,V2) -> U12(isNatKind(activate(V1)),activate(V1),activate(V2)) r2: U12(tt(),V1,V2) -> U13(isNatKind(activate(V2)),activate(V1),activate(V2)) r3: U13(tt(),V1,V2) -> U14(isNatKind(activate(V2)),activate(V1),activate(V2)) r4: U14(tt(),V1,V2) -> U15(isNat(activate(V1)),activate(V2)) r5: U15(tt(),V2) -> U16(isNat(activate(V2))) r6: U16(tt()) -> tt() r7: U21(tt(),V1) -> U22(isNatKind(activate(V1)),activate(V1)) r8: U22(tt(),V1) -> U23(isNat(activate(V1))) r9: U23(tt()) -> tt() r10: U31(tt(),V2) -> U32(isNatKind(activate(V2))) r11: U32(tt()) -> tt() r12: U41(tt()) -> tt() r13: U51(tt(),N) -> U52(isNatKind(activate(N)),activate(N)) r14: U52(tt(),N) -> activate(N) r15: U61(tt(),M,N) -> U62(isNatKind(activate(M)),activate(M),activate(N)) r16: U62(tt(),M,N) -> U63(isNat(activate(N)),activate(M),activate(N)) r17: U63(tt(),M,N) -> U64(isNatKind(activate(N)),activate(M),activate(N)) r18: U64(tt(),M,N) -> s(plus(activate(N),activate(M))) r19: isNat(n__0()) -> tt() r20: isNat(n__plus(V1,V2)) -> U11(isNatKind(activate(V1)),activate(V1),activate(V2)) r21: isNat(n__s(V1)) -> U21(isNatKind(activate(V1)),activate(V1)) r22: isNatKind(n__0()) -> tt() r23: isNatKind(n__plus(V1,V2)) -> U31(isNatKind(activate(V1)),activate(V2)) r24: isNatKind(n__s(V1)) -> U41(isNatKind(activate(V1))) r25: plus(N,|0|()) -> U51(isNat(N),N) r26: plus(N,s(M)) -> U61(isNat(M),M,N) r27: |0|() -> n__0() r28: plus(X1,X2) -> n__plus(X1,X2) r29: s(X) -> n__s(X) r30: activate(n__0()) -> |0|() r31: activate(n__plus(X1,X2)) -> plus(activate(X1),activate(X2)) r32: activate(n__s(X)) -> s(activate(X)) r33: activate(X) -> X The estimated dependency graph contains the following SCCs: {p31, p32, p33, p34, p35} {p1, p2, p3, p4, p5, p6, p24, p25, p26, p52} {p8, p9, p10} {p15} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: U64#(tt(),M,N) -> plus#(activate(N),activate(M)) p2: plus#(N,s(M)) -> U61#(isNat(M),M,N) p3: U61#(tt(),M,N) -> U62#(isNatKind(activate(M)),activate(M),activate(N)) p4: U62#(tt(),M,N) -> U63#(isNat(activate(N)),activate(M),activate(N)) p5: U63#(tt(),M,N) -> U64#(isNatKind(activate(N)),activate(M),activate(N)) and R consists of: r1: U11(tt(),V1,V2) -> U12(isNatKind(activate(V1)),activate(V1),activate(V2)) r2: U12(tt(),V1,V2) -> U13(isNatKind(activate(V2)),activate(V1),activate(V2)) r3: U13(tt(),V1,V2) -> U14(isNatKind(activate(V2)),activate(V1),activate(V2)) r4: U14(tt(),V1,V2) -> U15(isNat(activate(V1)),activate(V2)) r5: U15(tt(),V2) -> U16(isNat(activate(V2))) r6: U16(tt()) -> tt() r7: U21(tt(),V1) -> U22(isNatKind(activate(V1)),activate(V1)) r8: U22(tt(),V1) -> U23(isNat(activate(V1))) r9: U23(tt()) -> tt() r10: U31(tt(),V2) -> U32(isNatKind(activate(V2))) r11: U32(tt()) -> tt() r12: U41(tt()) -> tt() r13: U51(tt(),N) -> U52(isNatKind(activate(N)),activate(N)) r14: U52(tt(),N) -> activate(N) r15: U61(tt(),M,N) -> U62(isNatKind(activate(M)),activate(M),activate(N)) r16: U62(tt(),M,N) -> U63(isNat(activate(N)),activate(M),activate(N)) r17: U63(tt(),M,N) -> U64(isNatKind(activate(N)),activate(M),activate(N)) r18: U64(tt(),M,N) -> s(plus(activate(N),activate(M))) r19: isNat(n__0()) -> tt() r20: isNat(n__plus(V1,V2)) -> U11(isNatKind(activate(V1)),activate(V1),activate(V2)) r21: isNat(n__s(V1)) -> U21(isNatKind(activate(V1)),activate(V1)) r22: isNatKind(n__0()) -> tt() r23: isNatKind(n__plus(V1,V2)) -> U31(isNatKind(activate(V1)),activate(V2)) r24: isNatKind(n__s(V1)) -> U41(isNatKind(activate(V1))) r25: plus(N,|0|()) -> U51(isNat(N),N) r26: plus(N,s(M)) -> U61(isNat(M),M,N) r27: |0|() -> n__0() r28: plus(X1,X2) -> n__plus(X1,X2) r29: s(X) -> n__s(X) r30: activate(n__0()) -> |0|() r31: activate(n__plus(X1,X2)) -> plus(activate(X1),activate(X2)) r32: activate(n__s(X)) -> s(activate(X)) r33: activate(X) -> 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 Take the reduction pair: weighted path order base order: matrix interpretations: carrier: N^1 order: lexicographic order interpretations: U64#_A(x1,x2,x3) = x2 + 1 tt_A() = 5 plus#_A(x1,x2) = x2 activate_A(x1) = x1 s_A(x1) = x1 + 9 U61#_A(x1,x2,x3) = x2 + 4 isNat_A(x1) = x1 + 4 U62#_A(x1,x2,x3) = x2 + 3 isNatKind_A(x1) = x1 + 4 U63#_A(x1,x2,x3) = x2 + 2 U16_A(x1) = 6 U15_A(x1,x2) = 7 U64_A(x1,x2,x3) = x2 + x3 + 21 plus_A(x1,x2) = x1 + x2 + 12 U14_A(x1,x2,x3) = 8 U63_A(x1,x2,x3) = x2 + x3 + 21 U13_A(x1,x2,x3) = 9 U23_A(x1) = 6 U52_A(x1,x2) = x2 + 6 U62_A(x1,x2,x3) = x2 + x3 + 21 U12_A(x1,x2,x3) = 10 U22_A(x1,x2) = 7 U32_A(x1) = 6 U51_A(x1,x2) = x2 + 7 U61_A(x1,x2,x3) = x2 + x3 + 21 U11_A(x1,x2,x3) = 11 U21_A(x1,x2) = 8 U31_A(x1,x2) = 7 U41_A(x1) = 6 |0|_A() = 3 n__0_A() = 3 n__plus_A(x1,x2) = x1 + x2 + 12 n__s_A(x1) = x1 + 9 precedence: U61# > tt = activate = isNat = U62# = isNatKind = plus = U52 = U51 = U31 = U41 > U23 > U64# = plus# = U63# > U32 = U61 > U14 = U13 = U12 = U11 > U16 = U15 = U63 = U62 > |0| > U64 = n__0 > n__plus > U21 > s = n__s > U22 partial status: pi(U64#) = [] pi(tt) = [] pi(plus#) = [] pi(activate) = [1] pi(s) = [1] pi(U61#) = [] pi(isNat) = [] pi(U62#) = [] pi(isNatKind) = [] pi(U63#) = [] pi(U16) = [] pi(U15) = [] pi(U64) = [] pi(plus) = [] pi(U14) = [] pi(U63) = [] pi(U13) = [] pi(U23) = [] pi(U52) = [] pi(U62) = [] pi(U12) = [] pi(U22) = [] pi(U32) = [] pi(U51) = [] pi(U61) = [2, 3] pi(U11) = [] pi(U21) = [] pi(U31) = [] pi(U41) = [] pi(|0|) = [] pi(n__0) = [] pi(n__plus) = [1, 2] pi(n__s) = [] 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: U64#(tt(),M,N) -> plus#(activate(N),activate(M)) p2: U61#(tt(),M,N) -> U62#(isNatKind(activate(M)),activate(M),activate(N)) p3: U62#(tt(),M,N) -> U63#(isNat(activate(N)),activate(M),activate(N)) p4: U63#(tt(),M,N) -> U64#(isNatKind(activate(N)),activate(M),activate(N)) and R consists of: r1: U11(tt(),V1,V2) -> U12(isNatKind(activate(V1)),activate(V1),activate(V2)) r2: U12(tt(),V1,V2) -> U13(isNatKind(activate(V2)),activate(V1),activate(V2)) r3: U13(tt(),V1,V2) -> U14(isNatKind(activate(V2)),activate(V1),activate(V2)) r4: U14(tt(),V1,V2) -> U15(isNat(activate(V1)),activate(V2)) r5: U15(tt(),V2) -> U16(isNat(activate(V2))) r6: U16(tt()) -> tt() r7: U21(tt(),V1) -> U22(isNatKind(activate(V1)),activate(V1)) r8: U22(tt(),V1) -> U23(isNat(activate(V1))) r9: U23(tt()) -> tt() r10: U31(tt(),V2) -> U32(isNatKind(activate(V2))) r11: U32(tt()) -> tt() r12: U41(tt()) -> tt() r13: U51(tt(),N) -> U52(isNatKind(activate(N)),activate(N)) r14: U52(tt(),N) -> activate(N) r15: U61(tt(),M,N) -> U62(isNatKind(activate(M)),activate(M),activate(N)) r16: U62(tt(),M,N) -> U63(isNat(activate(N)),activate(M),activate(N)) r17: U63(tt(),M,N) -> U64(isNatKind(activate(N)),activate(M),activate(N)) r18: U64(tt(),M,N) -> s(plus(activate(N),activate(M))) r19: isNat(n__0()) -> tt() r20: isNat(n__plus(V1,V2)) -> U11(isNatKind(activate(V1)),activate(V1),activate(V2)) r21: isNat(n__s(V1)) -> U21(isNatKind(activate(V1)),activate(V1)) r22: isNatKind(n__0()) -> tt() r23: isNatKind(n__plus(V1,V2)) -> U31(isNatKind(activate(V1)),activate(V2)) r24: isNatKind(n__s(V1)) -> U41(isNatKind(activate(V1))) r25: plus(N,|0|()) -> U51(isNat(N),N) r26: plus(N,s(M)) -> U61(isNat(M),M,N) r27: |0|() -> n__0() r28: plus(X1,X2) -> n__plus(X1,X2) r29: s(X) -> n__s(X) r30: activate(n__0()) -> |0|() r31: activate(n__plus(X1,X2)) -> plus(activate(X1),activate(X2)) r32: activate(n__s(X)) -> s(activate(X)) r33: activate(X) -> 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: U11#(tt(),V1,V2) -> U12#(isNatKind(activate(V1)),activate(V1),activate(V2)) p2: U12#(tt(),V1,V2) -> U13#(isNatKind(activate(V2)),activate(V1),activate(V2)) p3: U13#(tt(),V1,V2) -> U14#(isNatKind(activate(V2)),activate(V1),activate(V2)) p4: U14#(tt(),V1,V2) -> isNat#(activate(V1)) p5: isNat#(n__s(V1)) -> U21#(isNatKind(activate(V1)),activate(V1)) p6: U21#(tt(),V1) -> U22#(isNatKind(activate(V1)),activate(V1)) p7: U22#(tt(),V1) -> isNat#(activate(V1)) p8: isNat#(n__plus(V1,V2)) -> U11#(isNatKind(activate(V1)),activate(V1),activate(V2)) p9: U14#(tt(),V1,V2) -> U15#(isNat(activate(V1)),activate(V2)) p10: U15#(tt(),V2) -> isNat#(activate(V2)) and R consists of: r1: U11(tt(),V1,V2) -> U12(isNatKind(activate(V1)),activate(V1),activate(V2)) r2: U12(tt(),V1,V2) -> U13(isNatKind(activate(V2)),activate(V1),activate(V2)) r3: U13(tt(),V1,V2) -> U14(isNatKind(activate(V2)),activate(V1),activate(V2)) r4: U14(tt(),V1,V2) -> U15(isNat(activate(V1)),activate(V2)) r5: U15(tt(),V2) -> U16(isNat(activate(V2))) r6: U16(tt()) -> tt() r7: U21(tt(),V1) -> U22(isNatKind(activate(V1)),activate(V1)) r8: U22(tt(),V1) -> U23(isNat(activate(V1))) r9: U23(tt()) -> tt() r10: U31(tt(),V2) -> U32(isNatKind(activate(V2))) r11: U32(tt()) -> tt() r12: U41(tt()) -> tt() r13: U51(tt(),N) -> U52(isNatKind(activate(N)),activate(N)) r14: U52(tt(),N) -> activate(N) r15: U61(tt(),M,N) -> U62(isNatKind(activate(M)),activate(M),activate(N)) r16: U62(tt(),M,N) -> U63(isNat(activate(N)),activate(M),activate(N)) r17: U63(tt(),M,N) -> U64(isNatKind(activate(N)),activate(M),activate(N)) r18: U64(tt(),M,N) -> s(plus(activate(N),activate(M))) r19: isNat(n__0()) -> tt() r20: isNat(n__plus(V1,V2)) -> U11(isNatKind(activate(V1)),activate(V1),activate(V2)) r21: isNat(n__s(V1)) -> U21(isNatKind(activate(V1)),activate(V1)) r22: isNatKind(n__0()) -> tt() r23: isNatKind(n__plus(V1,V2)) -> U31(isNatKind(activate(V1)),activate(V2)) r24: isNatKind(n__s(V1)) -> U41(isNatKind(activate(V1))) r25: plus(N,|0|()) -> U51(isNat(N),N) r26: plus(N,s(M)) -> U61(isNat(M),M,N) r27: |0|() -> n__0() r28: plus(X1,X2) -> n__plus(X1,X2) r29: s(X) -> n__s(X) r30: activate(n__0()) -> |0|() r31: activate(n__plus(X1,X2)) -> plus(activate(X1),activate(X2)) r32: activate(n__s(X)) -> s(activate(X)) r33: activate(X) -> 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 Take the reduction pair: weighted path order base order: matrix interpretations: carrier: N^1 order: lexicographic order interpretations: U11#_A(x1,x2,x3) = x1 + x2 + x3 + 16 tt_A() = 13 U12#_A(x1,x2,x3) = x2 + x3 + 28 isNatKind_A(x1) = 15 activate_A(x1) = x1 U13#_A(x1,x2,x3) = x1 + x2 + x3 + 12 U14#_A(x1,x2,x3) = x1 + x2 + x3 + 9 isNat#_A(x1) = x1 + 20 n__s_A(x1) = x1 U21#_A(x1,x2) = x2 + 20 U22#_A(x1,x2) = x2 + 20 n__plus_A(x1,x2) = x1 + x2 + 12 U15#_A(x1,x2) = x2 + 21 isNat_A(x1) = 21 U16_A(x1) = 13 U15_A(x1,x2) = x1 U64_A(x1,x2,x3) = x2 + x3 + 12 s_A(x1) = x1 plus_A(x1,x2) = x1 + x2 + 12 U14_A(x1,x2,x3) = 21 U63_A(x1,x2,x3) = x2 + x3 + 12 U13_A(x1,x2,x3) = 21 U23_A(x1) = 14 U52_A(x1,x2) = x2 + 20 U62_A(x1,x2,x3) = x2 + x3 + 12 U12_A(x1,x2,x3) = 21 U22_A(x1,x2) = x1 + 2 U32_A(x1) = 13 U51_A(x1,x2) = x2 + 21 U61_A(x1,x2,x3) = x2 + x3 + 12 U11_A(x1,x2,x3) = 21 U21_A(x1,x2) = x1 + 5 U31_A(x1,x2) = 14 U41_A(x1) = 13 |0|_A() = 22 n__0_A() = 22 precedence: U32 = U31 > isNat > U12 = U11 > U23 > U13 > |0| = n__0 > U14 > tt = isNatKind = U16 = U15 = U41 > n__plus = plus = U61 > U51 > U62 > U63 > U12# = U13# = U14# = U15# > isNat# = U21# = U22# = U22 = U21 > U11# = activate = n__s = U64 = s = U52 partial status: pi(U11#) = [] pi(tt) = [] pi(U12#) = [3] pi(isNatKind) = [] pi(activate) = [1] pi(U13#) = [] pi(U14#) = [3] pi(isNat#) = [] pi(n__s) = [] pi(U21#) = [] pi(U22#) = [] pi(n__plus) = [] pi(U15#) = [] pi(isNat) = [] pi(U16) = [] pi(U15) = [] pi(U64) = [] pi(s) = [] pi(plus) = [] pi(U14) = [] pi(U63) = [2, 3] pi(U13) = [] pi(U23) = [] pi(U52) = [] pi(U62) = [] pi(U12) = [] pi(U22) = [] pi(U32) = [] pi(U51) = [2] pi(U61) = [] pi(U11) = [] pi(U21) = [1] pi(U31) = [] pi(U41) = [] pi(|0|) = [] pi(n__0) = [] The next rules are strictly ordered: p9 We remove them from the problem. -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: U11#(tt(),V1,V2) -> U12#(isNatKind(activate(V1)),activate(V1),activate(V2)) p2: U12#(tt(),V1,V2) -> U13#(isNatKind(activate(V2)),activate(V1),activate(V2)) p3: U13#(tt(),V1,V2) -> U14#(isNatKind(activate(V2)),activate(V1),activate(V2)) p4: U14#(tt(),V1,V2) -> isNat#(activate(V1)) p5: isNat#(n__s(V1)) -> U21#(isNatKind(activate(V1)),activate(V1)) p6: U21#(tt(),V1) -> U22#(isNatKind(activate(V1)),activate(V1)) p7: U22#(tt(),V1) -> isNat#(activate(V1)) p8: isNat#(n__plus(V1,V2)) -> U11#(isNatKind(activate(V1)),activate(V1),activate(V2)) p9: U15#(tt(),V2) -> isNat#(activate(V2)) and R consists of: r1: U11(tt(),V1,V2) -> U12(isNatKind(activate(V1)),activate(V1),activate(V2)) r2: U12(tt(),V1,V2) -> U13(isNatKind(activate(V2)),activate(V1),activate(V2)) r3: U13(tt(),V1,V2) -> U14(isNatKind(activate(V2)),activate(V1),activate(V2)) r4: U14(tt(),V1,V2) -> U15(isNat(activate(V1)),activate(V2)) r5: U15(tt(),V2) -> U16(isNat(activate(V2))) r6: U16(tt()) -> tt() r7: U21(tt(),V1) -> U22(isNatKind(activate(V1)),activate(V1)) r8: U22(tt(),V1) -> U23(isNat(activate(V1))) r9: U23(tt()) -> tt() r10: U31(tt(),V2) -> U32(isNatKind(activate(V2))) r11: U32(tt()) -> tt() r12: U41(tt()) -> tt() r13: U51(tt(),N) -> U52(isNatKind(activate(N)),activate(N)) r14: U52(tt(),N) -> activate(N) r15: U61(tt(),M,N) -> U62(isNatKind(activate(M)),activate(M),activate(N)) r16: U62(tt(),M,N) -> U63(isNat(activate(N)),activate(M),activate(N)) r17: U63(tt(),M,N) -> U64(isNatKind(activate(N)),activate(M),activate(N)) r18: U64(tt(),M,N) -> s(plus(activate(N),activate(M))) r19: isNat(n__0()) -> tt() r20: isNat(n__plus(V1,V2)) -> U11(isNatKind(activate(V1)),activate(V1),activate(V2)) r21: isNat(n__s(V1)) -> U21(isNatKind(activate(V1)),activate(V1)) r22: isNatKind(n__0()) -> tt() r23: isNatKind(n__plus(V1,V2)) -> U31(isNatKind(activate(V1)),activate(V2)) r24: isNatKind(n__s(V1)) -> U41(isNatKind(activate(V1))) r25: plus(N,|0|()) -> U51(isNat(N),N) r26: plus(N,s(M)) -> U61(isNat(M),M,N) r27: |0|() -> n__0() r28: plus(X1,X2) -> n__plus(X1,X2) r29: s(X) -> n__s(X) r30: activate(n__0()) -> |0|() r31: activate(n__plus(X1,X2)) -> plus(activate(X1),activate(X2)) r32: activate(n__s(X)) -> s(activate(X)) r33: activate(X) -> X The estimated dependency graph contains the following SCCs: {p1, p2, p3, p4, p5, p6, p7, p8} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: U11#(tt(),V1,V2) -> U12#(isNatKind(activate(V1)),activate(V1),activate(V2)) p2: U12#(tt(),V1,V2) -> U13#(isNatKind(activate(V2)),activate(V1),activate(V2)) p3: U13#(tt(),V1,V2) -> U14#(isNatKind(activate(V2)),activate(V1),activate(V2)) p4: U14#(tt(),V1,V2) -> isNat#(activate(V1)) p5: isNat#(n__plus(V1,V2)) -> U11#(isNatKind(activate(V1)),activate(V1),activate(V2)) p6: isNat#(n__s(V1)) -> U21#(isNatKind(activate(V1)),activate(V1)) p7: U21#(tt(),V1) -> U22#(isNatKind(activate(V1)),activate(V1)) p8: U22#(tt(),V1) -> isNat#(activate(V1)) and R consists of: r1: U11(tt(),V1,V2) -> U12(isNatKind(activate(V1)),activate(V1),activate(V2)) r2: U12(tt(),V1,V2) -> U13(isNatKind(activate(V2)),activate(V1),activate(V2)) r3: U13(tt(),V1,V2) -> U14(isNatKind(activate(V2)),activate(V1),activate(V2)) r4: U14(tt(),V1,V2) -> U15(isNat(activate(V1)),activate(V2)) r5: U15(tt(),V2) -> U16(isNat(activate(V2))) r6: U16(tt()) -> tt() r7: U21(tt(),V1) -> U22(isNatKind(activate(V1)),activate(V1)) r8: U22(tt(),V1) -> U23(isNat(activate(V1))) r9: U23(tt()) -> tt() r10: U31(tt(),V2) -> U32(isNatKind(activate(V2))) r11: U32(tt()) -> tt() r12: U41(tt()) -> tt() r13: U51(tt(),N) -> U52(isNatKind(activate(N)),activate(N)) r14: U52(tt(),N) -> activate(N) r15: U61(tt(),M,N) -> U62(isNatKind(activate(M)),activate(M),activate(N)) r16: U62(tt(),M,N) -> U63(isNat(activate(N)),activate(M),activate(N)) r17: U63(tt(),M,N) -> U64(isNatKind(activate(N)),activate(M),activate(N)) r18: U64(tt(),M,N) -> s(plus(activate(N),activate(M))) r19: isNat(n__0()) -> tt() r20: isNat(n__plus(V1,V2)) -> U11(isNatKind(activate(V1)),activate(V1),activate(V2)) r21: isNat(n__s(V1)) -> U21(isNatKind(activate(V1)),activate(V1)) r22: isNatKind(n__0()) -> tt() r23: isNatKind(n__plus(V1,V2)) -> U31(isNatKind(activate(V1)),activate(V2)) r24: isNatKind(n__s(V1)) -> U41(isNatKind(activate(V1))) r25: plus(N,|0|()) -> U51(isNat(N),N) r26: plus(N,s(M)) -> U61(isNat(M),M,N) r27: |0|() -> n__0() r28: plus(X1,X2) -> n__plus(X1,X2) r29: s(X) -> n__s(X) r30: activate(n__0()) -> |0|() r31: activate(n__plus(X1,X2)) -> plus(activate(X1),activate(X2)) r32: activate(n__s(X)) -> s(activate(X)) r33: activate(X) -> 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 Take the reduction pair: weighted path order base order: matrix interpretations: carrier: N^1 order: lexicographic order interpretations: U11#_A(x1,x2,x3) = x2 + 6 tt_A() = 1 U12#_A(x1,x2,x3) = x2 + 5 isNatKind_A(x1) = 1 activate_A(x1) = x1 U13#_A(x1,x2,x3) = x2 + 4 U14#_A(x1,x2,x3) = x2 + 3 isNat#_A(x1) = x1 + 2 n__plus_A(x1,x2) = x1 + x2 + 8 n__s_A(x1) = x1 + 3 U21#_A(x1,x2) = x2 + 4 U22#_A(x1,x2) = x2 + 3 U16_A(x1) = 2 U15_A(x1,x2) = 3 isNat_A(x1) = x1 U14_A(x1,x2,x3) = x1 + 3 U13_A(x1,x2,x3) = x1 + x3 + 4 U23_A(x1) = 1 U64_A(x1,x2,x3) = x2 + x3 + 11 s_A(x1) = x1 + 3 plus_A(x1,x2) = x1 + x2 + 8 U12_A(x1,x2,x3) = x1 + x3 + 5 U22_A(x1,x2) = x1 U63_A(x1,x2,x3) = x2 + x3 + 11 U11_A(x1,x2,x3) = x1 + x2 + x3 + 6 U21_A(x1,x2) = x1 U52_A(x1,x2) = x2 + 2 U62_A(x1,x2,x3) = x2 + x3 + 11 U32_A(x1) = x1 U51_A(x1,x2) = x2 + 3 U61_A(x1,x2,x3) = x2 + x3 + 11 n__0_A() = 2 U31_A(x1,x2) = 1 U41_A(x1) = 1 |0|_A() = 2 precedence: U21 = U51 > isNat > n__plus = plus = U62 = U61 > activate > U22 > U63 > |0| > U64 > U22# > U12# = s > n__s > U11# = isNatKind = isNat# = U21# > U14# > n__0 = U31 > U32 > U15 = U14 = U13 = U12 = U11 > U41 > U13# > U16 > tt = U23 > U52 partial status: pi(U11#) = [] pi(tt) = [] pi(U12#) = [] pi(isNatKind) = [] pi(activate) = [1] pi(U13#) = [] pi(U14#) = [] pi(isNat#) = [1] pi(n__plus) = [] pi(n__s) = [] pi(U21#) = [] pi(U22#) = [] pi(U16) = [] pi(U15) = [] pi(isNat) = [1] pi(U14) = [] pi(U13) = [] pi(U23) = [] pi(U64) = [] pi(s) = [] pi(plus) = [] pi(U12) = [] pi(U22) = [1] pi(U63) = [] pi(U11) = [1, 3] pi(U21) = [] pi(U52) = [] pi(U62) = [] pi(U32) = [] pi(U51) = [] pi(U61) = [] pi(n__0) = [] pi(U31) = [] pi(U41) = [] pi(|0|) = [] The next rules are strictly ordered: p7 We remove them from the problem. -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: U11#(tt(),V1,V2) -> U12#(isNatKind(activate(V1)),activate(V1),activate(V2)) p2: U12#(tt(),V1,V2) -> U13#(isNatKind(activate(V2)),activate(V1),activate(V2)) p3: U13#(tt(),V1,V2) -> U14#(isNatKind(activate(V2)),activate(V1),activate(V2)) p4: U14#(tt(),V1,V2) -> isNat#(activate(V1)) p5: isNat#(n__plus(V1,V2)) -> U11#(isNatKind(activate(V1)),activate(V1),activate(V2)) p6: isNat#(n__s(V1)) -> U21#(isNatKind(activate(V1)),activate(V1)) p7: U22#(tt(),V1) -> isNat#(activate(V1)) and R consists of: r1: U11(tt(),V1,V2) -> U12(isNatKind(activate(V1)),activate(V1),activate(V2)) r2: U12(tt(),V1,V2) -> U13(isNatKind(activate(V2)),activate(V1),activate(V2)) r3: U13(tt(),V1,V2) -> U14(isNatKind(activate(V2)),activate(V1),activate(V2)) r4: U14(tt(),V1,V2) -> U15(isNat(activate(V1)),activate(V2)) r5: U15(tt(),V2) -> U16(isNat(activate(V2))) r6: U16(tt()) -> tt() r7: U21(tt(),V1) -> U22(isNatKind(activate(V1)),activate(V1)) r8: U22(tt(),V1) -> U23(isNat(activate(V1))) r9: U23(tt()) -> tt() r10: U31(tt(),V2) -> U32(isNatKind(activate(V2))) r11: U32(tt()) -> tt() r12: U41(tt()) -> tt() r13: U51(tt(),N) -> U52(isNatKind(activate(N)),activate(N)) r14: U52(tt(),N) -> activate(N) r15: U61(tt(),M,N) -> U62(isNatKind(activate(M)),activate(M),activate(N)) r16: U62(tt(),M,N) -> U63(isNat(activate(N)),activate(M),activate(N)) r17: U63(tt(),M,N) -> U64(isNatKind(activate(N)),activate(M),activate(N)) r18: U64(tt(),M,N) -> s(plus(activate(N),activate(M))) r19: isNat(n__0()) -> tt() r20: isNat(n__plus(V1,V2)) -> U11(isNatKind(activate(V1)),activate(V1),activate(V2)) r21: isNat(n__s(V1)) -> U21(isNatKind(activate(V1)),activate(V1)) r22: isNatKind(n__0()) -> tt() r23: isNatKind(n__plus(V1,V2)) -> U31(isNatKind(activate(V1)),activate(V2)) r24: isNatKind(n__s(V1)) -> U41(isNatKind(activate(V1))) r25: plus(N,|0|()) -> U51(isNat(N),N) r26: plus(N,s(M)) -> U61(isNat(M),M,N) r27: |0|() -> n__0() r28: plus(X1,X2) -> n__plus(X1,X2) r29: s(X) -> n__s(X) r30: activate(n__0()) -> |0|() r31: activate(n__plus(X1,X2)) -> plus(activate(X1),activate(X2)) r32: activate(n__s(X)) -> s(activate(X)) r33: activate(X) -> X The estimated dependency graph contains the following SCCs: {p1, p2, p3, p4, p5} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: U11#(tt(),V1,V2) -> U12#(isNatKind(activate(V1)),activate(V1),activate(V2)) p2: U12#(tt(),V1,V2) -> U13#(isNatKind(activate(V2)),activate(V1),activate(V2)) p3: U13#(tt(),V1,V2) -> U14#(isNatKind(activate(V2)),activate(V1),activate(V2)) p4: U14#(tt(),V1,V2) -> isNat#(activate(V1)) p5: isNat#(n__plus(V1,V2)) -> U11#(isNatKind(activate(V1)),activate(V1),activate(V2)) and R consists of: r1: U11(tt(),V1,V2) -> U12(isNatKind(activate(V1)),activate(V1),activate(V2)) r2: U12(tt(),V1,V2) -> U13(isNatKind(activate(V2)),activate(V1),activate(V2)) r3: U13(tt(),V1,V2) -> U14(isNatKind(activate(V2)),activate(V1),activate(V2)) r4: U14(tt(),V1,V2) -> U15(isNat(activate(V1)),activate(V2)) r5: U15(tt(),V2) -> U16(isNat(activate(V2))) r6: U16(tt()) -> tt() r7: U21(tt(),V1) -> U22(isNatKind(activate(V1)),activate(V1)) r8: U22(tt(),V1) -> U23(isNat(activate(V1))) r9: U23(tt()) -> tt() r10: U31(tt(),V2) -> U32(isNatKind(activate(V2))) r11: U32(tt()) -> tt() r12: U41(tt()) -> tt() r13: U51(tt(),N) -> U52(isNatKind(activate(N)),activate(N)) r14: U52(tt(),N) -> activate(N) r15: U61(tt(),M,N) -> U62(isNatKind(activate(M)),activate(M),activate(N)) r16: U62(tt(),M,N) -> U63(isNat(activate(N)),activate(M),activate(N)) r17: U63(tt(),M,N) -> U64(isNatKind(activate(N)),activate(M),activate(N)) r18: U64(tt(),M,N) -> s(plus(activate(N),activate(M))) r19: isNat(n__0()) -> tt() r20: isNat(n__plus(V1,V2)) -> U11(isNatKind(activate(V1)),activate(V1),activate(V2)) r21: isNat(n__s(V1)) -> U21(isNatKind(activate(V1)),activate(V1)) r22: isNatKind(n__0()) -> tt() r23: isNatKind(n__plus(V1,V2)) -> U31(isNatKind(activate(V1)),activate(V2)) r24: isNatKind(n__s(V1)) -> U41(isNatKind(activate(V1))) r25: plus(N,|0|()) -> U51(isNat(N),N) r26: plus(N,s(M)) -> U61(isNat(M),M,N) r27: |0|() -> n__0() r28: plus(X1,X2) -> n__plus(X1,X2) r29: s(X) -> n__s(X) r30: activate(n__0()) -> |0|() r31: activate(n__plus(X1,X2)) -> plus(activate(X1),activate(X2)) r32: activate(n__s(X)) -> s(activate(X)) r33: activate(X) -> 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 Take the reduction pair: weighted path order base order: matrix interpretations: carrier: N^1 order: lexicographic order interpretations: U11#_A(x1,x2,x3) = x2 + 53 tt_A() = 5 U12#_A(x1,x2,x3) = x2 + 40 isNatKind_A(x1) = x1 + 7 activate_A(x1) = x1 + 12 U13#_A(x1,x2,x3) = x2 + 27 U14#_A(x1,x2,x3) = x2 + 14 isNat#_A(x1) = x1 + 1 n__plus_A(x1,x2) = x1 + 66 U16_A(x1) = 6 U15_A(x1,x2) = 7 isNat_A(x1) = x1 + 67 U14_A(x1,x2,x3) = 8 U13_A(x1,x2,x3) = 9 U23_A(x1) = 6 U64_A(x1,x2,x3) = 2 s_A(x1) = 1 plus_A(x1,x2) = x1 + 66 U12_A(x1,x2,x3) = 10 U22_A(x1,x2) = 7 U63_A(x1,x2,x3) = 3 U11_A(x1,x2,x3) = x1 + 6 U21_A(x1,x2) = 8 U52_A(x1,x2) = x2 + 13 U62_A(x1,x2,x3) = 4 U32_A(x1) = 6 U51_A(x1,x2) = x2 + 26 U61_A(x1,x2,x3) = 66 n__0_A() = 6 n__s_A(x1) = 0 U31_A(x1,x2) = 67 U41_A(x1) = 6 |0|_A() = 7 precedence: U12 = U11 > U13 > tt = activate = U15 = U14 = U23 = U52 = U51 > isNatKind > n__plus = plus > U14# > U21 > U11# = U12# = isNat# = U16 = s = U61 > U13# > isNat = U22 = U62 > U32 = n__0 = n__s = U31 = U41 = |0| > U64 = U63 partial status: pi(U11#) = [] pi(tt) = [] pi(U12#) = [] pi(isNatKind) = [] pi(activate) = [] pi(U13#) = [] pi(U14#) = [] pi(isNat#) = [1] pi(n__plus) = [] pi(U16) = [] pi(U15) = [] pi(isNat) = [1] pi(U14) = [] pi(U13) = [] pi(U23) = [] pi(U64) = [] pi(s) = [] pi(plus) = [] pi(U12) = [] pi(U22) = [] pi(U63) = [] pi(U11) = [1] pi(U21) = [] pi(U52) = [] pi(U62) = [] pi(U32) = [] pi(U51) = [2] pi(U61) = [] pi(n__0) = [] pi(n__s) = [] pi(U31) = [] pi(U41) = [] pi(|0|) = [] The next rules are strictly ordered: p5 We remove them from the problem. -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: U11#(tt(),V1,V2) -> U12#(isNatKind(activate(V1)),activate(V1),activate(V2)) p2: U12#(tt(),V1,V2) -> U13#(isNatKind(activate(V2)),activate(V1),activate(V2)) p3: U13#(tt(),V1,V2) -> U14#(isNatKind(activate(V2)),activate(V1),activate(V2)) p4: U14#(tt(),V1,V2) -> isNat#(activate(V1)) and R consists of: r1: U11(tt(),V1,V2) -> U12(isNatKind(activate(V1)),activate(V1),activate(V2)) r2: U12(tt(),V1,V2) -> U13(isNatKind(activate(V2)),activate(V1),activate(V2)) r3: U13(tt(),V1,V2) -> U14(isNatKind(activate(V2)),activate(V1),activate(V2)) r4: U14(tt(),V1,V2) -> U15(isNat(activate(V1)),activate(V2)) r5: U15(tt(),V2) -> U16(isNat(activate(V2))) r6: U16(tt()) -> tt() r7: U21(tt(),V1) -> U22(isNatKind(activate(V1)),activate(V1)) r8: U22(tt(),V1) -> U23(isNat(activate(V1))) r9: U23(tt()) -> tt() r10: U31(tt(),V2) -> U32(isNatKind(activate(V2))) r11: U32(tt()) -> tt() r12: U41(tt()) -> tt() r13: U51(tt(),N) -> U52(isNatKind(activate(N)),activate(N)) r14: U52(tt(),N) -> activate(N) r15: U61(tt(),M,N) -> U62(isNatKind(activate(M)),activate(M),activate(N)) r16: U62(tt(),M,N) -> U63(isNat(activate(N)),activate(M),activate(N)) r17: U63(tt(),M,N) -> U64(isNatKind(activate(N)),activate(M),activate(N)) r18: U64(tt(),M,N) -> s(plus(activate(N),activate(M))) r19: isNat(n__0()) -> tt() r20: isNat(n__plus(V1,V2)) -> U11(isNatKind(activate(V1)),activate(V1),activate(V2)) r21: isNat(n__s(V1)) -> U21(isNatKind(activate(V1)),activate(V1)) r22: isNatKind(n__0()) -> tt() r23: isNatKind(n__plus(V1,V2)) -> U31(isNatKind(activate(V1)),activate(V2)) r24: isNatKind(n__s(V1)) -> U41(isNatKind(activate(V1))) r25: plus(N,|0|()) -> U51(isNat(N),N) r26: plus(N,s(M)) -> U61(isNat(M),M,N) r27: |0|() -> n__0() r28: plus(X1,X2) -> n__plus(X1,X2) r29: s(X) -> n__s(X) r30: activate(n__0()) -> |0|() r31: activate(n__plus(X1,X2)) -> plus(activate(X1),activate(X2)) r32: activate(n__s(X)) -> s(activate(X)) r33: activate(X) -> 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: isNatKind#(n__plus(V1,V2)) -> U31#(isNatKind(activate(V1)),activate(V2)) p2: U31#(tt(),V2) -> isNatKind#(activate(V2)) p3: isNatKind#(n__plus(V1,V2)) -> isNatKind#(activate(V1)) and R consists of: r1: U11(tt(),V1,V2) -> U12(isNatKind(activate(V1)),activate(V1),activate(V2)) r2: U12(tt(),V1,V2) -> U13(isNatKind(activate(V2)),activate(V1),activate(V2)) r3: U13(tt(),V1,V2) -> U14(isNatKind(activate(V2)),activate(V1),activate(V2)) r4: U14(tt(),V1,V2) -> U15(isNat(activate(V1)),activate(V2)) r5: U15(tt(),V2) -> U16(isNat(activate(V2))) r6: U16(tt()) -> tt() r7: U21(tt(),V1) -> U22(isNatKind(activate(V1)),activate(V1)) r8: U22(tt(),V1) -> U23(isNat(activate(V1))) r9: U23(tt()) -> tt() r10: U31(tt(),V2) -> U32(isNatKind(activate(V2))) r11: U32(tt()) -> tt() r12: U41(tt()) -> tt() r13: U51(tt(),N) -> U52(isNatKind(activate(N)),activate(N)) r14: U52(tt(),N) -> activate(N) r15: U61(tt(),M,N) -> U62(isNatKind(activate(M)),activate(M),activate(N)) r16: U62(tt(),M,N) -> U63(isNat(activate(N)),activate(M),activate(N)) r17: U63(tt(),M,N) -> U64(isNatKind(activate(N)),activate(M),activate(N)) r18: U64(tt(),M,N) -> s(plus(activate(N),activate(M))) r19: isNat(n__0()) -> tt() r20: isNat(n__plus(V1,V2)) -> U11(isNatKind(activate(V1)),activate(V1),activate(V2)) r21: isNat(n__s(V1)) -> U21(isNatKind(activate(V1)),activate(V1)) r22: isNatKind(n__0()) -> tt() r23: isNatKind(n__plus(V1,V2)) -> U31(isNatKind(activate(V1)),activate(V2)) r24: isNatKind(n__s(V1)) -> U41(isNatKind(activate(V1))) r25: plus(N,|0|()) -> U51(isNat(N),N) r26: plus(N,s(M)) -> U61(isNat(M),M,N) r27: |0|() -> n__0() r28: plus(X1,X2) -> n__plus(X1,X2) r29: s(X) -> n__s(X) r30: activate(n__0()) -> |0|() r31: activate(n__plus(X1,X2)) -> plus(activate(X1),activate(X2)) r32: activate(n__s(X)) -> s(activate(X)) r33: activate(X) -> 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 Take the reduction pair: weighted path order base order: matrix interpretations: carrier: N^1 order: lexicographic order interpretations: isNatKind#_A(x1) = x1 + 11 n__plus_A(x1,x2) = x1 + x2 U31#_A(x1,x2) = x1 + x2 isNatKind_A(x1) = x1 activate_A(x1) = x1 tt_A() = 12 U16_A(x1) = 13 U15_A(x1,x2) = 14 isNat_A(x1) = 19 U14_A(x1,x2,x3) = 15 U13_A(x1,x2,x3) = 16 U23_A(x1) = 13 U64_A(x1,x2,x3) = x1 + 13 s_A(x1) = 24 plus_A(x1,x2) = x1 + x2 U12_A(x1,x2,x3) = 17 U22_A(x1,x2) = 14 U63_A(x1,x2,x3) = x1 + x3 + 2 U11_A(x1,x2,x3) = 18 U21_A(x1,x2) = 15 U52_A(x1,x2) = x2 + 10 U62_A(x1,x2,x3) = x3 + 22 U32_A(x1) = 12 U51_A(x1,x2) = x2 + 11 U61_A(x1,x2,x3) = x3 + 23 n__0_A() = 12 n__s_A(x1) = 24 U31_A(x1,x2) = x1 U41_A(x1) = 23 |0|_A() = 12 precedence: n__plus = activate = plus = U12 = U11 > isNat = U52 > U14 = U13 > U16 = U15 > n__0 = |0| > U23 = U22 = U61 > U64 = U63 = U62 > isNatKind# = U31# = s = n__s > U41 > isNatKind = U21 = U31 > tt = U32 = U51 partial status: pi(isNatKind#) = [1] pi(n__plus) = [] pi(U31#) = [] pi(isNatKind) = [] pi(activate) = [] pi(tt) = [] pi(U16) = [] pi(U15) = [] pi(isNat) = [] pi(U14) = [] pi(U13) = [] pi(U23) = [] pi(U64) = [] pi(s) = [] pi(plus) = [] pi(U12) = [] pi(U22) = [] pi(U63) = [] pi(U11) = [] pi(U21) = [] pi(U52) = [] pi(U62) = [] pi(U32) = [] pi(U51) = [2] pi(U61) = [] pi(n__0) = [] pi(n__s) = [] pi(U31) = [] pi(U41) = [] pi(|0|) = [] 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: isNatKind#(n__plus(V1,V2)) -> U31#(isNatKind(activate(V1)),activate(V2)) p2: isNatKind#(n__plus(V1,V2)) -> isNatKind#(activate(V1)) and R consists of: r1: U11(tt(),V1,V2) -> U12(isNatKind(activate(V1)),activate(V1),activate(V2)) r2: U12(tt(),V1,V2) -> U13(isNatKind(activate(V2)),activate(V1),activate(V2)) r3: U13(tt(),V1,V2) -> U14(isNatKind(activate(V2)),activate(V1),activate(V2)) r4: U14(tt(),V1,V2) -> U15(isNat(activate(V1)),activate(V2)) r5: U15(tt(),V2) -> U16(isNat(activate(V2))) r6: U16(tt()) -> tt() r7: U21(tt(),V1) -> U22(isNatKind(activate(V1)),activate(V1)) r8: U22(tt(),V1) -> U23(isNat(activate(V1))) r9: U23(tt()) -> tt() r10: U31(tt(),V2) -> U32(isNatKind(activate(V2))) r11: U32(tt()) -> tt() r12: U41(tt()) -> tt() r13: U51(tt(),N) -> U52(isNatKind(activate(N)),activate(N)) r14: U52(tt(),N) -> activate(N) r15: U61(tt(),M,N) -> U62(isNatKind(activate(M)),activate(M),activate(N)) r16: U62(tt(),M,N) -> U63(isNat(activate(N)),activate(M),activate(N)) r17: U63(tt(),M,N) -> U64(isNatKind(activate(N)),activate(M),activate(N)) r18: U64(tt(),M,N) -> s(plus(activate(N),activate(M))) r19: isNat(n__0()) -> tt() r20: isNat(n__plus(V1,V2)) -> U11(isNatKind(activate(V1)),activate(V1),activate(V2)) r21: isNat(n__s(V1)) -> U21(isNatKind(activate(V1)),activate(V1)) r22: isNatKind(n__0()) -> tt() r23: isNatKind(n__plus(V1,V2)) -> U31(isNatKind(activate(V1)),activate(V2)) r24: isNatKind(n__s(V1)) -> U41(isNatKind(activate(V1))) r25: plus(N,|0|()) -> U51(isNat(N),N) r26: plus(N,s(M)) -> U61(isNat(M),M,N) r27: |0|() -> n__0() r28: plus(X1,X2) -> n__plus(X1,X2) r29: s(X) -> n__s(X) r30: activate(n__0()) -> |0|() r31: activate(n__plus(X1,X2)) -> plus(activate(X1),activate(X2)) r32: activate(n__s(X)) -> s(activate(X)) r33: activate(X) -> X The estimated dependency graph contains the following SCCs: {p2} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: isNatKind#(n__plus(V1,V2)) -> isNatKind#(activate(V1)) and R consists of: r1: U11(tt(),V1,V2) -> U12(isNatKind(activate(V1)),activate(V1),activate(V2)) r2: U12(tt(),V1,V2) -> U13(isNatKind(activate(V2)),activate(V1),activate(V2)) r3: U13(tt(),V1,V2) -> U14(isNatKind(activate(V2)),activate(V1),activate(V2)) r4: U14(tt(),V1,V2) -> U15(isNat(activate(V1)),activate(V2)) r5: U15(tt(),V2) -> U16(isNat(activate(V2))) r6: U16(tt()) -> tt() r7: U21(tt(),V1) -> U22(isNatKind(activate(V1)),activate(V1)) r8: U22(tt(),V1) -> U23(isNat(activate(V1))) r9: U23(tt()) -> tt() r10: U31(tt(),V2) -> U32(isNatKind(activate(V2))) r11: U32(tt()) -> tt() r12: U41(tt()) -> tt() r13: U51(tt(),N) -> U52(isNatKind(activate(N)),activate(N)) r14: U52(tt(),N) -> activate(N) r15: U61(tt(),M,N) -> U62(isNatKind(activate(M)),activate(M),activate(N)) r16: U62(tt(),M,N) -> U63(isNat(activate(N)),activate(M),activate(N)) r17: U63(tt(),M,N) -> U64(isNatKind(activate(N)),activate(M),activate(N)) r18: U64(tt(),M,N) -> s(plus(activate(N),activate(M))) r19: isNat(n__0()) -> tt() r20: isNat(n__plus(V1,V2)) -> U11(isNatKind(activate(V1)),activate(V1),activate(V2)) r21: isNat(n__s(V1)) -> U21(isNatKind(activate(V1)),activate(V1)) r22: isNatKind(n__0()) -> tt() r23: isNatKind(n__plus(V1,V2)) -> U31(isNatKind(activate(V1)),activate(V2)) r24: isNatKind(n__s(V1)) -> U41(isNatKind(activate(V1))) r25: plus(N,|0|()) -> U51(isNat(N),N) r26: plus(N,s(M)) -> U61(isNat(M),M,N) r27: |0|() -> n__0() r28: plus(X1,X2) -> n__plus(X1,X2) r29: s(X) -> n__s(X) r30: activate(n__0()) -> |0|() r31: activate(n__plus(X1,X2)) -> plus(activate(X1),activate(X2)) r32: activate(n__s(X)) -> s(activate(X)) r33: activate(X) -> 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 Take the reduction pair: weighted path order base order: matrix interpretations: carrier: N^1 order: lexicographic order interpretations: isNatKind#_A(x1) = x1 n__plus_A(x1,x2) = x1 + 35 activate_A(x1) = x1 + 6 U16_A(x1) = 1 tt_A() = 0 U15_A(x1,x2) = 2 isNat_A(x1) = x1 + 36 U14_A(x1,x2,x3) = x2 + 7 U13_A(x1,x2,x3) = x2 + 14 isNatKind_A(x1) = 3 U23_A(x1) = 1 U32_A(x1) = 1 U64_A(x1,x2,x3) = x1 + 12 s_A(x1) = 11 plus_A(x1,x2) = x1 + 35 U12_A(x1,x2,x3) = x2 + 21 U22_A(x1,x2) = 2 U31_A(x1,x2) = 2 U41_A(x1) = 1 U63_A(x1,x2,x3) = 16 U11_A(x1,x2,x3) = x2 + 28 U21_A(x1,x2) = 4 U52_A(x1,x2) = x2 + 7 U62_A(x1,x2,x3) = 17 n__0_A() = 1 n__s_A(x1) = 5 U51_A(x1,x2) = x2 + 14 U61_A(x1,x2,x3) = 18 |0|_A() = 2 precedence: U12 = U11 = U51 > U64 = U63 = U62 > activate > plus > s > tt > U15 = U14 = U13 = U52 > U23 = U22 = U21 > isNat > U16 = isNatKind = U32 = U31 = U41 = n__s > isNatKind# = n__0 = |0| > n__plus = U61 partial status: pi(isNatKind#) = [1] pi(n__plus) = [] pi(activate) = [1] pi(U16) = [] pi(tt) = [] pi(U15) = [] pi(isNat) = [1] pi(U14) = [] pi(U13) = [] pi(isNatKind) = [] pi(U23) = [] pi(U32) = [] pi(U64) = [] pi(s) = [] pi(plus) = [] pi(U12) = [] pi(U22) = [] pi(U31) = [] pi(U41) = [] pi(U63) = [] pi(U11) = [2] pi(U21) = [] pi(U52) = [2] pi(U62) = [] pi(n__0) = [] pi(n__s) = [] pi(U51) = [2] pi(U61) = [] pi(|0|) = [] The next rules are strictly ordered: p1 We remove them from the problem. Then no dependency pair remains. -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: activate#(n__plus(X1,X2)) -> activate#(X1) and R consists of: r1: U11(tt(),V1,V2) -> U12(isNatKind(activate(V1)),activate(V1),activate(V2)) r2: U12(tt(),V1,V2) -> U13(isNatKind(activate(V2)),activate(V1),activate(V2)) r3: U13(tt(),V1,V2) -> U14(isNatKind(activate(V2)),activate(V1),activate(V2)) r4: U14(tt(),V1,V2) -> U15(isNat(activate(V1)),activate(V2)) r5: U15(tt(),V2) -> U16(isNat(activate(V2))) r6: U16(tt()) -> tt() r7: U21(tt(),V1) -> U22(isNatKind(activate(V1)),activate(V1)) r8: U22(tt(),V1) -> U23(isNat(activate(V1))) r9: U23(tt()) -> tt() r10: U31(tt(),V2) -> U32(isNatKind(activate(V2))) r11: U32(tt()) -> tt() r12: U41(tt()) -> tt() r13: U51(tt(),N) -> U52(isNatKind(activate(N)),activate(N)) r14: U52(tt(),N) -> activate(N) r15: U61(tt(),M,N) -> U62(isNatKind(activate(M)),activate(M),activate(N)) r16: U62(tt(),M,N) -> U63(isNat(activate(N)),activate(M),activate(N)) r17: U63(tt(),M,N) -> U64(isNatKind(activate(N)),activate(M),activate(N)) r18: U64(tt(),M,N) -> s(plus(activate(N),activate(M))) r19: isNat(n__0()) -> tt() r20: isNat(n__plus(V1,V2)) -> U11(isNatKind(activate(V1)),activate(V1),activate(V2)) r21: isNat(n__s(V1)) -> U21(isNatKind(activate(V1)),activate(V1)) r22: isNatKind(n__0()) -> tt() r23: isNatKind(n__plus(V1,V2)) -> U31(isNatKind(activate(V1)),activate(V2)) r24: isNatKind(n__s(V1)) -> U41(isNatKind(activate(V1))) r25: plus(N,|0|()) -> U51(isNat(N),N) r26: plus(N,s(M)) -> U61(isNat(M),M,N) r27: |0|() -> n__0() r28: plus(X1,X2) -> n__plus(X1,X2) r29: s(X) -> n__s(X) r30: activate(n__0()) -> |0|() r31: activate(n__plus(X1,X2)) -> plus(activate(X1),activate(X2)) r32: activate(n__s(X)) -> s(activate(X)) r33: activate(X) -> X The set of usable rules consists of (no rules) Take the reduction pair: weighted path order base order: matrix interpretations: carrier: N^1 order: lexicographic order interpretations: activate#_A(x1) = x1 n__plus_A(x1,x2) = x1 + x2 + 1 precedence: activate# = n__plus partial status: pi(activate#) = [] pi(n__plus) = [2] The next rules are strictly ordered: p1 We remove them from the problem. Then no dependency pair remains.