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(X1,X2) activate(n__s(X)) -> s(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#(X1,X2) p69: activate#(n__s(X)) -> s#(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(X1,X2) r32: activate(n__s(X)) -> s(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} -- 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)) -> plus#(X1,X2) p4: plus#(N,s(M)) -> isNat#(M) p5: isNat#(n__s(V1)) -> activate#(V1) p6: isNat#(n__s(V1)) -> isNatKind#(activate(V1)) p7: isNatKind#(n__s(V1)) -> activate#(V1) p8: isNatKind#(n__s(V1)) -> isNatKind#(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) -> 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) -> activate#(V2) 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(X1,X2) r32: activate(n__s(X)) -> s(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^2 order: lexicographic order interpretations: U11#_A(x1,x2,x3) = ((1,0),(0,0)) x2 + ((1,0),(0,0)) x3 + (44,122) tt_A() = (51,50) U12#_A(x1,x2,x3) = ((1,0),(0,0)) x2 + ((1,0),(1,1)) x3 + (43,123) isNatKind_A(x1) = ((0,0),(1,0)) x1 + (51,86) activate_A(x1) = x1 + (0,68) activate#_A(x1) = ((1,0),(1,1)) x1 + (28,122) n__plus_A(x1,x2) = ((1,0),(1,0)) x1 + ((1,0),(0,0)) x2 + (25,22) plus#_A(x1,x2) = ((1,0),(0,0)) x1 + x2 + (52,56) s_A(x1) = ((1,0),(0,0)) x1 + (31,18) isNat#_A(x1) = ((1,0),(1,1)) x1 + (20,74) n__s_A(x1) = ((1,0),(0,0)) x1 + (31,17) isNatKind#_A(x1) = ((1,0),(0,0)) x1 + (26,73) U31#_A(x1,x2) = ((1,0),(0,0)) x2 + (29,21) U21#_A(x1,x2) = ((1,0),(0,0)) x2 + (30,74) U22#_A(x1,x2) = ((1,0),(0,0)) x2 + (29,67) U61#_A(x1,x2,x3) = ((1,0),(1,1)) x2 + ((1,0),(0,0)) x3 + (56,73) isNat_A(x1) = ((1,0),(0,0)) x1 + (39,71) U62#_A(x1,x2,x3) = ((1,0),(0,0)) x2 + ((1,0),(0,0)) x3 + (55,72) U63#_A(x1,x2,x3) = ((0,0),(1,0)) x1 + ((1,0),(0,0)) x2 + ((1,0),(0,0)) x3 + (54,34) U64#_A(x1,x2,x3) = ((1,0),(1,1)) x2 + ((1,0),(1,1)) x3 + (53,125) |0|_A() = (13,67) U51#_A(x1,x2) = ((1,0),(0,0)) x2 + (53,122) U52#_A(x1,x2) = ((1,0),(1,1)) x2 + (52,123) U13#_A(x1,x2,x3) = ((1,0),(0,0)) x2 + ((1,0),(0,0)) x3 + (42,69) U14#_A(x1,x2,x3) = ((1,0),(1,1)) x2 + ((1,0),(1,1)) x3 + (41,143) U15#_A(x1,x2) = ((1,0),(0,0)) x1 + x2 + (1,69) U16_A(x1) = (52,62) U15_A(x1,x2) = ((1,0),(0,0)) x1 + (13,63) U64_A(x1,x2,x3) = ((1,0),(0,0)) x1 + ((1,0),(0,0)) x2 + ((1,0),(1,0)) x3 + (5,69) plus_A(x1,x2) = ((1,0),(1,0)) x1 + ((1,0),(0,0)) x2 + (25,89) U14_A(x1,x2,x3) = ((1,0),(0,0)) x1 + ((1,0),(0,0)) x2 + (2,64) U63_A(x1,x2,x3) = ((1,0),(0,0)) x2 + ((1,0),(1,0)) x3 + (56,87) U13_A(x1,x2,x3) = ((1,0),(0,0)) x1 + ((1,0),(0,0)) x2 + (3,65) U23_A(x1) = ((0,0),(1,0)) x1 + (52,12) U52_A(x1,x2) = ((1,0),(1,1)) x2 + (1,69) U62_A(x1,x2,x3) = ((1,0),(0,0)) x1 + ((1,0),(0,0)) x2 + ((1,0),(1,0)) x3 + (5,88) U12_A(x1,x2,x3) = ((1,0),(0,0)) x1 + ((1,0),(0,0)) x2 + (4,66) U22_A(x1,x2) = ((0,0),(1,0)) x1 + ((0,0),(1,0)) x2 + (53,19) U32_A(x1) = ((1,0),(1,0)) x1 U51_A(x1,x2) = ((0,0),(1,0)) x1 + ((1,0),(1,1)) x2 + (2,87) U61_A(x1,x2,x3) = ((1,0),(0,0)) x2 + ((1,0),(1,0)) x3 + (56,88) U11_A(x1,x2,x3) = ((1,0),(0,0)) x1 + ((1,0),(0,0)) x2 + (5,67) U21_A(x1,x2) = (54,69) U31_A(x1,x2) = ((0,0),(1,0)) x1 + (51,18) U41_A(x1) = (51,51) n__0_A() = (13,0) precedence: n__plus = U64# = U12 = U11 > U22# > isNatKind = U22 = U32 = U21 = U31 > activate = s = n__s = U64 = plus > U11# = U12# = activate# = plus# = isNat# = isNatKind# = U31# = U21# = U61# = isNat = U51# = U52# = U13# = U14# = U15# > U13 > U15 = U14 > U62# > tt = U16 = U41 > U63 > U63# > U61 > U62 > U51 > |0| > n__0 > U23 > U52 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: p2 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: activate#(n__plus(X1,X2)) -> plus#(X1,X2) p3: plus#(N,s(M)) -> isNat#(M) p4: isNat#(n__s(V1)) -> activate#(V1) p5: isNat#(n__s(V1)) -> isNatKind#(activate(V1)) p6: isNatKind#(n__s(V1)) -> activate#(V1) p7: isNatKind#(n__s(V1)) -> isNatKind#(activate(V1)) p8: isNatKind#(n__plus(V1,V2)) -> activate#(V2) p9: isNatKind#(n__plus(V1,V2)) -> activate#(V1) p10: isNatKind#(n__plus(V1,V2)) -> isNatKind#(activate(V1)) p11: isNatKind#(n__plus(V1,V2)) -> U31#(isNatKind(activate(V1)),activate(V2)) p12: U31#(tt(),V2) -> activate#(V2) p13: U31#(tt(),V2) -> isNatKind#(activate(V2)) p14: isNat#(n__s(V1)) -> U21#(isNatKind(activate(V1)),activate(V1)) p15: U21#(tt(),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) -> activate#(V2) 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(X1,X2) r32: activate(n__s(X)) -> s(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) -> 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#(X1,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: U51#(tt(),N) -> isNatKind#(activate(N)) p17: isNatKind#(n__plus(V1,V2)) -> activate#(V2) p18: isNatKind#(n__s(V1)) -> isNatKind#(activate(V1)) 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: U21#(tt(),V1) -> 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#(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(X1,X2) r32: activate(n__s(X)) -> s(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^2 order: lexicographic order interpretations: U11#_A(x1,x2,x3) = ((1,0),(1,1)) x2 + ((1,0),(1,1)) x3 + (106,42) tt_A() = (105,33) U12#_A(x1,x2,x3) = ((0,0),(1,0)) x1 + x2 + ((1,0),(1,1)) x3 + (106,1) isNatKind_A(x1) = ((1,0),(1,0)) x1 + (16,20) activate_A(x1) = x1 + (0,12) U13#_A(x1,x2,x3) = x2 + ((1,0),(1,0)) x3 + (106,93) U14#_A(x1,x2,x3) = x2 + ((1,0),(1,0)) x3 + (106,80) U15#_A(x1,x2) = ((1,0),(0,0)) x1 + ((1,0),(1,1)) x2 + (2,108) isNat_A(x1) = ((1,0),(1,0)) x1 + (95,19) isNat#_A(x1) = x1 + (106,67) n__plus_A(x1,x2) = ((1,0),(1,1)) x1 + ((1,0),(1,1)) x2 isNatKind#_A(x1) = ((1,0),(0,0)) x1 + (92,96) U31#_A(x1,x2) = x1 + ((1,0),(0,0)) x2 + (1,75) activate#_A(x1) = ((1,0),(0,0)) x1 + (91,107) plus#_A(x1,x2) = ((1,0),(0,0)) x1 + x2 + (90,108) |0|_A() = (94,1) U51#_A(x1,x2) = ((0,0),(1,0)) x1 + ((1,0),(1,0)) x2 + (93,15) U52#_A(x1,x2) = ((1,0),(0,0)) x2 + (92,108) n__s_A(x1) = ((1,0),(1,0)) x1 + (90,31) U21#_A(x1,x2) = ((1,0),(1,0)) x2 + (107,97) U22#_A(x1,x2) = ((1,0),(1,1)) x2 + (106,108) s_A(x1) = ((1,0),(1,0)) x1 + (90,32) U61#_A(x1,x2,x3) = x2 + x3 + (108,141) U62#_A(x1,x2,x3) = x2 + x3 + (107,118) U63#_A(x1,x2,x3) = x2 + x3 + (106,95) U64#_A(x1,x2,x3) = ((1,0),(0,0)) x2 + ((1,0),(0,0)) x3 + (92,121) U16_A(x1) = (106,34) U15_A(x1,x2) = (107,35) U64_A(x1,x2,x3) = ((1,0),(1,0)) x2 + ((1,0),(1,0)) x3 + (90,34) plus_A(x1,x2) = ((1,0),(1,1)) x1 + ((1,0),(1,1)) x2 + (0,11) U14_A(x1,x2,x3) = ((1,0),(0,0)) x1 + (3,36) U63_A(x1,x2,x3) = ((1,0),(1,0)) x2 + ((1,0),(1,0)) x3 + (90,35) U13_A(x1,x2,x3) = ((1,0),(0,0)) x3 + (95,37) U23_A(x1) = (106,32) U52_A(x1,x2) = ((1,0),(0,0)) x2 + (93,1) U62_A(x1,x2,x3) = ((1,0),(1,0)) x2 + ((1,0),(1,0)) x3 + (90,36) U12_A(x1,x2,x3) = ((0,0),(1,0)) x1 + ((1,0),(0,0)) x3 + (95,1) U22_A(x1,x2) = ((0,0),(1,0)) x1 + ((0,0),(1,0)) x2 + (107,1) U32_A(x1) = ((1,0),(1,0)) x1 + (0,2) U51_A(x1,x2) = x2 + (93,2) U61_A(x1,x2,x3) = ((0,0),(1,0)) x1 + ((1,0),(1,0)) x2 + ((1,0),(1,0)) x3 + (90,1) U11_A(x1,x2,x3) = ((0,0),(1,0)) x2 + ((1,0),(1,0)) x3 + (95,18) U21_A(x1,x2) = x1 + ((0,0),(1,0)) x2 + (3,90) U31_A(x1,x2) = ((1,0),(1,0)) x2 + (16,19) U41_A(x1) = ((0,0),(1,0)) x1 + (105,95) n__0_A() = (94,1) precedence: U51 > U12 > U11 > U52 > isNat > U13 > |0| = n__0 > activate > U62 > U63 > isNatKind > U21 > U11# = U12# = U13# = U14# = U15# = isNat# = isNatKind# = U31# = plus# = U51# = U21# = U22# = U61# = U62# = U63# = U64# > U52# = plus > activate# > U15 = U14 > s = U64 > U61 > n__s > n__plus > U22 > U32 = U31 > tt = U16 = U23 = U41 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) = [1] pi(U31) = [] pi(U41) = [] pi(n__0) = [] The next rules are strictly ordered: p11 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: activate#(n__plus(X1,X2)) -> plus#(X1,X2) 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: U51#(tt(),N) -> isNatKind#(activate(N)) p16: isNatKind#(n__plus(V1,V2)) -> activate#(V2) p17: isNatKind#(n__s(V1)) -> isNatKind#(activate(V1)) 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: U21#(tt(),V1) -> 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#(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(X1,X2) r32: activate(n__s(X)) -> s(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) -> activate#(V2) p3: activate#(n__plus(X1,X2)) -> plus#(X1,X2) p4: plus#(N,s(M)) -> isNat#(M) p5: isNat#(n__s(V1)) -> activate#(V1) p6: isNat#(n__s(V1)) -> isNatKind#(activate(V1)) p7: isNatKind#(n__s(V1)) -> activate#(V1) p8: isNatKind#(n__s(V1)) -> isNatKind#(activate(V1)) p9: isNatKind#(n__plus(V1,V2)) -> activate#(V2) p10: isNatKind#(n__plus(V1,V2)) -> isNatKind#(activate(V1)) p11: isNatKind#(n__plus(V1,V2)) -> U31#(isNatKind(activate(V1)),activate(V2)) p12: U31#(tt(),V2) -> activate#(V2) p13: U31#(tt(),V2) -> isNatKind#(activate(V2)) p14: isNat#(n__s(V1)) -> U21#(isNatKind(activate(V1)),activate(V1)) p15: U21#(tt(),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(X1,X2) r32: activate(n__s(X)) -> s(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^2 order: lexicographic order interpretations: U11#_A(x1,x2,x3) = x2 + x3 + (86,27) tt_A() = (7,22) U12#_A(x1,x2,x3) = x2 + ((1,0),(0,0)) x3 + (85,7) isNatKind_A(x1) = ((0,0),(1,0)) x1 + (80,9) activate_A(x1) = x1 + (0,26) activate#_A(x1) = ((1,0),(1,1)) x1 + (8,23) n__plus_A(x1,x2) = ((1,0),(0,0)) x1 + ((1,0),(1,1)) x2 + (79,35) plus#_A(x1,x2) = ((1,0),(0,0)) x1 + ((1,0),(0,0)) x2 + (70,138) s_A(x1) = x1 + (149,33) isNat#_A(x1) = ((1,0),(0,0)) x1 + (8,80) n__s_A(x1) = x1 + (149,8) isNatKind#_A(x1) = ((1,0),(1,1)) x1 + (6,115) U31#_A(x1,x2) = ((1,0),(1,1)) x1 + ((1,0),(1,1)) x2 + (4,113) U21#_A(x1,x2) = ((1,0),(1,0)) x1 + ((1,0),(0,0)) x2 + (76,1) U22#_A(x1,x2) = ((1,0),(0,0)) x1 + ((1,0),(0,0)) x2 + (2,8) U61#_A(x1,x2,x3) = ((1,0),(1,1)) x2 + ((1,0),(1,0)) x3 + (218,32) isNat_A(x1) = ((0,0),(1,0)) x1 + (11,0) U62#_A(x1,x2,x3) = ((1,0),(0,0)) x1 + ((1,0),(1,0)) x2 + ((1,0),(0,0)) x3 + (67,141) U63#_A(x1,x2,x3) = ((1,0),(0,0)) x1 + ((1,0),(1,0)) x2 + ((1,0),(0,0)) x3 + (63,140) U64#_A(x1,x2,x3) = ((1,0),(1,0)) x2 + ((1,0),(0,0)) x3 + (70,139) |0|_A() = (12,2) U51#_A(x1,x2) = ((1,0),(1,1)) x2 + (81,142) U52#_A(x1,x2) = ((0,0),(1,0)) x1 + ((1,0),(0,0)) x2 + (9,17) U13#_A(x1,x2,x3) = ((1,0),(0,0)) x2 + ((1,0),(1,0)) x3 + (84,8) U14#_A(x1,x2,x3) = ((1,0),(1,1)) x1 + ((1,0),(0,0)) x2 + x3 + (3,52) U15#_A(x1,x2) = x2 + (9,1) U16_A(x1) = (8,23) U15_A(x1,x2) = (9,24) U64_A(x1,x2,x3) = ((1,0),(1,1)) x2 + ((1,0),(0,0)) x3 + (228,95) plus_A(x1,x2) = ((1,0),(0,0)) x1 + ((1,0),(1,1)) x2 + (79,36) U14_A(x1,x2,x3) = (9,25) U63_A(x1,x2,x3) = ((0,0),(1,0)) x1 + ((1,0),(1,1)) x2 + ((1,0),(0,0)) x3 + (228,115) U13_A(x1,x2,x3) = (9,27) U23_A(x1) = ((0,0),(1,0)) x1 + (8,16) U52_A(x1,x2) = ((0,0),(1,0)) x1 + ((1,0),(1,0)) x2 + (8,20) U62_A(x1,x2,x3) = ((1,0),(1,1)) x2 + ((1,0),(0,0)) x3 + (228,153) U12_A(x1,x2,x3) = ((0,0),(1,0)) x2 + ((0,0),(1,0)) x3 + (9,28) U22_A(x1,x2) = ((0,0),(1,0)) x2 + (10,28) U32_A(x1) = (80,23) U51_A(x1,x2) = x2 + (81,8) U61_A(x1,x2,x3) = ((0,0),(1,0)) x1 + ((1,0),(1,1)) x2 + ((1,0),(0,0)) x3 + (228,207) U11_A(x1,x2,x3) = (10,36) U21_A(x1,x2) = ((0,0),(1,0)) x2 + (10,29) U31_A(x1,x2) = ((0,0),(1,0)) x2 + (80,24) U41_A(x1) = (80,23) n__0_A() = (12,1) precedence: U31# > plus > U11# = U12# = isNat# = U21# = U22# = U13# = U14# = U15# > n__plus = plus# = isNatKind# = U61# = U63# = U64# = U51# > isNatKind > activate# = U62# = U52# > U22 = U21 > U23 > tt = isNat = U63 = U62 = U32 = U61 = U31 = U41 > U64 > n__0 > activate = s = |0| > U51 > n__s > U11 > U52 > U12 > U15 = U14 = U13 > U16 partial status: pi(U11#) = [] pi(tt) = [] pi(U12#) = [] pi(isNatKind) = [] pi(activate) = [1] pi(activate#) = [1] pi(n__plus) = [] pi(plus#) = [] pi(s) = [] pi(isNat#) = [] pi(n__s) = [1] 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: p47 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#(V2) p3: activate#(n__plus(X1,X2)) -> plus#(X1,X2) p4: plus#(N,s(M)) -> isNat#(M) p5: isNat#(n__s(V1)) -> activate#(V1) p6: isNat#(n__s(V1)) -> isNatKind#(activate(V1)) p7: isNatKind#(n__s(V1)) -> activate#(V1) p8: isNatKind#(n__s(V1)) -> isNatKind#(activate(V1)) p9: isNatKind#(n__plus(V1,V2)) -> activate#(V2) p10: isNatKind#(n__plus(V1,V2)) -> isNatKind#(activate(V1)) p11: isNatKind#(n__plus(V1,V2)) -> U31#(isNatKind(activate(V1)),activate(V2)) p12: U31#(tt(),V2) -> activate#(V2) p13: U31#(tt(),V2) -> isNatKind#(activate(V2)) p14: isNat#(n__s(V1)) -> U21#(isNatKind(activate(V1)),activate(V1)) p15: U21#(tt(),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: U52#(tt(),N) -> activate#(N) p48: U12#(tt(),V1,V2) -> isNatKind#(activate(V2)) p49: U12#(tt(),V1,V2) -> U13#(isNatKind(activate(V2)),activate(V1),activate(V2)) p50: U13#(tt(),V1,V2) -> activate#(V1) p51: U13#(tt(),V1,V2) -> activate#(V2) p52: U13#(tt(),V1,V2) -> isNatKind#(activate(V2)) p53: U13#(tt(),V1,V2) -> U14#(isNatKind(activate(V2)),activate(V1),activate(V2)) p54: U14#(tt(),V1,V2) -> activate#(V2) p55: U14#(tt(),V1,V2) -> activate#(V1) p56: U14#(tt(),V1,V2) -> isNat#(activate(V1)) p57: U14#(tt(),V1,V2) -> U15#(isNat(activate(V1)),activate(V2)) p58: U15#(tt(),V2) -> activate#(V2) p59: 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(X1,X2) r32: activate(n__s(X)) -> s(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, p48, p49, p50, p51, p52, p53, p54, p55, p56, p57, p58, p59} -- 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#(V2) p12: activate#(n__plus(X1,X2)) -> plus#(X1,X2) p13: plus#(N,|0|()) -> U51#(isNat(N),N) p14: U51#(tt(),N) -> isNatKind#(activate(N)) p15: isNatKind#(n__s(V1)) -> isNatKind#(activate(V1)) p16: isNatKind#(n__s(V1)) -> activate#(V1) p17: U51#(tt(),N) -> activate#(N) p18: plus#(N,|0|()) -> isNat#(N) p19: isNat#(n__plus(V1,V2)) -> isNatKind#(activate(V1)) p20: isNat#(n__plus(V1,V2)) -> activate#(V1) p21: isNat#(n__plus(V1,V2)) -> activate#(V2) p22: isNat#(n__s(V1)) -> U21#(isNatKind(activate(V1)),activate(V1)) p23: U21#(tt(),V1) -> U22#(isNatKind(activate(V1)),activate(V1)) p24: U22#(tt(),V1) -> isNat#(activate(V1)) p25: isNat#(n__s(V1)) -> isNatKind#(activate(V1)) p26: isNat#(n__s(V1)) -> activate#(V1) p27: U22#(tt(),V1) -> activate#(V1) p28: U21#(tt(),V1) -> isNatKind#(activate(V1)) p29: U21#(tt(),V1) -> activate#(V1) p30: plus#(N,s(M)) -> U61#(isNat(M),M,N) p31: U61#(tt(),M,N) -> U62#(isNatKind(activate(M)),activate(M),activate(N)) p32: U62#(tt(),M,N) -> U63#(isNat(activate(N)),activate(M),activate(N)) p33: U63#(tt(),M,N) -> U64#(isNatKind(activate(N)),activate(M),activate(N)) p34: U64#(tt(),M,N) -> plus#(activate(N),activate(M)) p35: plus#(N,s(M)) -> isNat#(M) p36: U64#(tt(),M,N) -> activate#(N) p37: U64#(tt(),M,N) -> activate#(M) p38: U63#(tt(),M,N) -> isNatKind#(activate(N)) p39: U63#(tt(),M,N) -> activate#(N) p40: U63#(tt(),M,N) -> activate#(M) p41: U62#(tt(),M,N) -> isNat#(activate(N)) p42: U62#(tt(),M,N) -> activate#(N) p43: U62#(tt(),M,N) -> activate#(M) p44: U61#(tt(),M,N) -> isNatKind#(activate(M)) p45: U61#(tt(),M,N) -> activate#(M) p46: U61#(tt(),M,N) -> activate#(N) p47: U31#(tt(),V2) -> activate#(V2) p48: U11#(tt(),V1,V2) -> activate#(V1) p49: U11#(tt(),V1,V2) -> activate#(V2) p50: U15#(tt(),V2) -> activate#(V2) p51: U14#(tt(),V1,V2) -> isNat#(activate(V1)) p52: U14#(tt(),V1,V2) -> activate#(V1) p53: U14#(tt(),V1,V2) -> activate#(V2) p54: U13#(tt(),V1,V2) -> isNatKind#(activate(V2)) p55: U13#(tt(),V1,V2) -> activate#(V2) p56: U13#(tt(),V1,V2) -> activate#(V1) p57: U12#(tt(),V1,V2) -> isNatKind#(activate(V2)) p58: U12#(tt(),V1,V2) -> 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(X1,X2) r32: activate(n__s(X)) -> s(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^2 order: lexicographic order interpretations: U11#_A(x1,x2,x3) = ((1,0),(0,0)) x2 + ((1,0),(1,1)) x3 + (31,81) tt_A() = (22,1) U12#_A(x1,x2,x3) = ((1,0),(0,0)) x2 + x3 + (30,1) isNatKind_A(x1) = ((1,0),(0,0)) x1 + (10,82) activate_A(x1) = ((1,0),(1,1)) x1 + (0,21) U13#_A(x1,x2,x3) = ((0,0),(1,0)) x1 + x2 + ((1,0),(0,0)) x3 + (29,59) U14#_A(x1,x2,x3) = ((1,0),(0,0)) x2 + ((1,0),(0,0)) x3 + (28,2) U15#_A(x1,x2) = ((1,0),(0,0)) x2 + (23,3) isNat_A(x1) = x1 + (27,99) isNat#_A(x1) = ((1,0),(1,0)) x1 + (20,78) n__plus_A(x1,x2) = x1 + ((1,0),(1,1)) x2 + (12,112) isNatKind#_A(x1) = ((1,0),(1,1)) x1 + (0,59) U31#_A(x1,x2) = x1 + ((1,0),(1,1)) x2 + (1,79) activate#_A(x1) = ((1,0),(1,1)) x1 + (12,4) plus#_A(x1,x2) = ((1,0),(1,1)) x1 + x2 + (11,38) |0|_A() = (13,19) U51#_A(x1,x2) = ((1,0),(1,1)) x2 + (14,22) n__s_A(x1) = ((1,0),(1,0)) x1 + (14,5) U21#_A(x1,x2) = ((1,0),(1,1)) x2 + (24,80) U22#_A(x1,x2) = ((1,0),(1,0)) x2 + (23,79) s_A(x1) = ((1,0),(1,0)) x1 + (14,6) U61#_A(x1,x2,x3) = ((1,0),(1,0)) x2 + ((1,0),(1,1)) x3 + (25,43) U62#_A(x1,x2,x3) = ((1,0),(1,1)) x2 + ((1,0),(0,0)) x3 + (21,22) U63#_A(x1,x2,x3) = ((1,0),(1,1)) x2 + ((1,0),(0,0)) x3 + (14,80) U64#_A(x1,x2,x3) = ((1,0),(0,0)) x2 + ((1,0),(0,0)) x3 + (13,80) U16_A(x1) = (23,2) U15_A(x1,x2) = (24,3) U64_A(x1,x2,x3) = ((1,0),(1,0)) x2 + ((1,0),(1,0)) x3 + (26,19) plus_A(x1,x2) = ((1,0),(1,1)) x1 + ((1,0),(1,1)) x2 + (12,113) U14_A(x1,x2,x3) = (25,4) U63_A(x1,x2,x3) = ((1,0),(1,0)) x2 + ((1,0),(1,0)) x3 + (26,20) U13_A(x1,x2,x3) = (26,5) U23_A(x1) = (23,2) U52_A(x1,x2) = ((1,0),(1,1)) x2 + (1,22) U62_A(x1,x2,x3) = ((1,0),(1,0)) x2 + ((1,0),(1,0)) x3 + (26,22) U12_A(x1,x2,x3) = (27,22) U22_A(x1,x2) = (24,3) U32_A(x1) = ((1,0),(0,0)) x1 + (1,2) U51_A(x1,x2) = ((1,0),(0,0)) x2 + (11,20) U61_A(x1,x2,x3) = ((1,0),(1,0)) x2 + ((1,0),(1,0)) x3 + (26,82) U11_A(x1,x2,x3) = ((1,0),(0,0)) x1 + (6,23) U21_A(x1,x2) = x1 + (3,21) U31_A(x1,x2) = ((1,0),(0,0)) x1 + ((1,0),(0,0)) x2 + (3,22) U41_A(x1) = (23,6) n__0_A() = (13,2) precedence: U62 > U63 > U12 > U13 > isNatKind > U41 > U31 > U32 > tt = U13# = U14# = n__0 > isNat > U64 = U23 = U22 = U21 > activate = n__plus = plus = U52 = U51 = U61 > U11# = isNat# = plus# = U21# = U22# = U64# > U31# = U51# > activate# = U61# = U62# = U63# > s > n__s > U12# > isNatKind# > U11 > U15# > |0| > U14 > U16 > U15 partial status: pi(U11#) = [] pi(tt) = [] pi(U12#) = [3] pi(isNatKind) = [] pi(activate) = [1] pi(U13#) = [] pi(U14#) = [] pi(U15#) = [] pi(isNat) = [1] pi(isNat#) = [] pi(n__plus) = [] pi(isNatKind#) = [1] pi(U31#) = [] pi(activate#) = [1] pi(plus#) = [] pi(|0|) = [] pi(U51#) = [] pi(n__s) = [] pi(U21#) = [] pi(U22#) = [] pi(s) = [] pi(U61#) = [3] pi(U62#) = [2] pi(U63#) = [2] 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) = [1] pi(U31) = [] pi(U41) = [] pi(n__0) = [] The next rules are strictly ordered: p47 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#(V2) p12: activate#(n__plus(X1,X2)) -> plus#(X1,X2) p13: plus#(N,|0|()) -> U51#(isNat(N),N) p14: U51#(tt(),N) -> isNatKind#(activate(N)) p15: isNatKind#(n__s(V1)) -> isNatKind#(activate(V1)) p16: isNatKind#(n__s(V1)) -> activate#(V1) p17: U51#(tt(),N) -> activate#(N) p18: plus#(N,|0|()) -> isNat#(N) p19: isNat#(n__plus(V1,V2)) -> isNatKind#(activate(V1)) p20: isNat#(n__plus(V1,V2)) -> activate#(V1) p21: isNat#(n__plus(V1,V2)) -> activate#(V2) p22: isNat#(n__s(V1)) -> U21#(isNatKind(activate(V1)),activate(V1)) p23: U21#(tt(),V1) -> U22#(isNatKind(activate(V1)),activate(V1)) p24: U22#(tt(),V1) -> isNat#(activate(V1)) p25: isNat#(n__s(V1)) -> isNatKind#(activate(V1)) p26: isNat#(n__s(V1)) -> activate#(V1) p27: U22#(tt(),V1) -> activate#(V1) p28: U21#(tt(),V1) -> isNatKind#(activate(V1)) p29: U21#(tt(),V1) -> activate#(V1) p30: plus#(N,s(M)) -> U61#(isNat(M),M,N) p31: U61#(tt(),M,N) -> U62#(isNatKind(activate(M)),activate(M),activate(N)) p32: U62#(tt(),M,N) -> U63#(isNat(activate(N)),activate(M),activate(N)) p33: U63#(tt(),M,N) -> U64#(isNatKind(activate(N)),activate(M),activate(N)) p34: U64#(tt(),M,N) -> plus#(activate(N),activate(M)) p35: plus#(N,s(M)) -> isNat#(M) p36: U64#(tt(),M,N) -> activate#(N) p37: U64#(tt(),M,N) -> activate#(M) p38: U63#(tt(),M,N) -> isNatKind#(activate(N)) p39: U63#(tt(),M,N) -> activate#(N) p40: U63#(tt(),M,N) -> activate#(M) p41: U62#(tt(),M,N) -> isNat#(activate(N)) p42: U62#(tt(),M,N) -> activate#(N) p43: U62#(tt(),M,N) -> activate#(M) p44: U61#(tt(),M,N) -> isNatKind#(activate(M)) p45: U61#(tt(),M,N) -> activate#(M) p46: U61#(tt(),M,N) -> activate#(N) p47: U11#(tt(),V1,V2) -> activate#(V1) p48: U11#(tt(),V1,V2) -> activate#(V2) p49: U15#(tt(),V2) -> activate#(V2) p50: U14#(tt(),V1,V2) -> isNat#(activate(V1)) p51: U14#(tt(),V1,V2) -> activate#(V1) p52: U14#(tt(),V1,V2) -> activate#(V2) p53: U13#(tt(),V1,V2) -> isNatKind#(activate(V2)) p54: U13#(tt(),V1,V2) -> activate#(V2) p55: U13#(tt(),V1,V2) -> activate#(V1) p56: U12#(tt(),V1,V2) -> isNatKind#(activate(V2)) p57: U12#(tt(),V1,V2) -> 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(X1,X2) r32: activate(n__s(X)) -> s(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} -- 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#(V2) p3: activate#(n__plus(X1,X2)) -> plus#(X1,X2) p4: plus#(N,s(M)) -> isNat#(M) p5: isNat#(n__s(V1)) -> activate#(V1) p6: isNat#(n__s(V1)) -> isNatKind#(activate(V1)) p7: isNatKind#(n__s(V1)) -> activate#(V1) p8: isNatKind#(n__s(V1)) -> isNatKind#(activate(V1)) p9: isNatKind#(n__plus(V1,V2)) -> activate#(V2) p10: isNatKind#(n__plus(V1,V2)) -> isNatKind#(activate(V1)) p11: isNatKind#(n__plus(V1,V2)) -> U31#(isNatKind(activate(V1)),activate(V2)) p12: U31#(tt(),V2) -> isNatKind#(activate(V2)) p13: isNat#(n__s(V1)) -> U21#(isNatKind(activate(V1)),activate(V1)) p14: U21#(tt(),V1) -> activate#(V1) p15: U21#(tt(),V1) -> isNatKind#(activate(V1)) p16: U21#(tt(),V1) -> U22#(isNatKind(activate(V1)),activate(V1)) p17: U22#(tt(),V1) -> activate#(V1) p18: U22#(tt(),V1) -> isNat#(activate(V1)) p19: isNat#(n__plus(V1,V2)) -> activate#(V2) p20: isNat#(n__plus(V1,V2)) -> activate#(V1) p21: isNat#(n__plus(V1,V2)) -> isNatKind#(activate(V1)) p22: isNat#(n__plus(V1,V2)) -> U11#(isNatKind(activate(V1)),activate(V1),activate(V2)) p23: U11#(tt(),V1,V2) -> activate#(V2) p24: U11#(tt(),V1,V2) -> activate#(V1) p25: U11#(tt(),V1,V2) -> isNatKind#(activate(V1)) p26: plus#(N,s(M)) -> U61#(isNat(M),M,N) p27: U61#(tt(),M,N) -> activate#(N) p28: U61#(tt(),M,N) -> activate#(M) p29: U61#(tt(),M,N) -> isNatKind#(activate(M)) p30: U61#(tt(),M,N) -> U62#(isNatKind(activate(M)),activate(M),activate(N)) p31: U62#(tt(),M,N) -> activate#(M) p32: U62#(tt(),M,N) -> activate#(N) p33: U62#(tt(),M,N) -> isNat#(activate(N)) p34: U62#(tt(),M,N) -> U63#(isNat(activate(N)),activate(M),activate(N)) p35: U63#(tt(),M,N) -> activate#(M) p36: U63#(tt(),M,N) -> activate#(N) p37: U63#(tt(),M,N) -> isNatKind#(activate(N)) p38: U63#(tt(),M,N) -> U64#(isNatKind(activate(N)),activate(M),activate(N)) p39: U64#(tt(),M,N) -> activate#(M) p40: U64#(tt(),M,N) -> activate#(N) p41: U64#(tt(),M,N) -> plus#(activate(N),activate(M)) p42: plus#(N,|0|()) -> isNat#(N) p43: plus#(N,|0|()) -> U51#(isNat(N),N) p44: U51#(tt(),N) -> activate#(N) p45: U51#(tt(),N) -> isNatKind#(activate(N)) p46: U12#(tt(),V1,V2) -> isNatKind#(activate(V2)) p47: U12#(tt(),V1,V2) -> U13#(isNatKind(activate(V2)),activate(V1),activate(V2)) p48: U13#(tt(),V1,V2) -> activate#(V1) p49: U13#(tt(),V1,V2) -> activate#(V2) p50: U13#(tt(),V1,V2) -> isNatKind#(activate(V2)) p51: U13#(tt(),V1,V2) -> U14#(isNatKind(activate(V2)),activate(V1),activate(V2)) p52: U14#(tt(),V1,V2) -> activate#(V2) p53: U14#(tt(),V1,V2) -> activate#(V1) p54: U14#(tt(),V1,V2) -> isNat#(activate(V1)) p55: U14#(tt(),V1,V2) -> U15#(isNat(activate(V1)),activate(V2)) p56: U15#(tt(),V2) -> activate#(V2) p57: 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(X1,X2) r32: activate(n__s(X)) -> s(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^2 order: lexicographic order interpretations: U11#_A(x1,x2,x3) = ((1,0),(0,0)) x2 + ((1,0),(0,0)) x3 + (34,314) tt_A() = (9,29) U12#_A(x1,x2,x3) = ((1,0),(1,0)) x1 + x2 + ((1,0),(1,1)) x3 + (17,241) isNatKind_A(x1) = ((0,0),(1,0)) x1 + (16,16) activate_A(x1) = x1 + (0,28) activate#_A(x1) = ((1,0),(0,0)) x1 + (1,43) n__plus_A(x1,x2) = ((1,0),(1,1)) x1 + ((1,0),(1,1)) x2 + (35,0) plus#_A(x1,x2) = ((1,0),(0,0)) x1 + x2 + (7,43) s_A(x1) = ((1,0),(1,0)) x1 + (14,47) isNat#_A(x1) = x1 + (1,91) n__s_A(x1) = ((1,0),(1,0)) x1 + (14,45) isNatKind#_A(x1) = ((1,0),(0,0)) x1 + (8,42) U31#_A(x1,x2) = ((1,0),(1,0)) x2 + (36,29) U21#_A(x1,x2) = ((1,0),(1,0)) x2 + (13,44) U22#_A(x1,x2) = x2 + (10,120) U61#_A(x1,x2,x3) = ((1,0),(1,1)) x2 + ((1,0),(1,1)) x3 + (20,91) isNat_A(x1) = ((1,0),(0,0)) x1 + (11,46) U62#_A(x1,x2,x3) = x1 + ((1,0),(0,0)) x2 + ((1,0),(0,0)) x3 + (3,14) U63#_A(x1,x2,x3) = x2 + x3 + (9,42) U64#_A(x1,x2,x3) = x2 + ((1,0),(1,0)) x3 + (8,43) |0|_A() = (12,1) U51#_A(x1,x2) = ((1,0),(0,0)) x2 + (11,43) U13#_A(x1,x2,x3) = ((1,0),(0,0)) x1 + x2 + ((1,0),(1,1)) x3 + (9,193) U14#_A(x1,x2,x3) = x1 + x2 + x3 + (1,120) U15#_A(x1,x2) = x2 + (2,120) U16_A(x1) = (10,30) U15_A(x1,x2) = ((1,0),(0,0)) x1 + (3,31) U64_A(x1,x2,x3) = ((1,0),(1,0)) x2 + ((1,0),(1,0)) x3 + (49,83) plus_A(x1,x2) = ((1,0),(1,1)) x1 + ((1,0),(1,1)) x2 + (35,28) U14_A(x1,x2,x3) = ((1,0),(0,0)) x2 + (15,42) U63_A(x1,x2,x3) = ((1,0),(1,0)) x2 + ((1,0),(1,0)) x3 + (49,84) U13_A(x1,x2,x3) = ((1,0),(0,0)) x1 + ((1,0),(0,0)) x2 + (8,43) U23_A(x1) = (10,30) U52_A(x1,x2) = ((1,0),(1,0)) x2 + (10,30) U62_A(x1,x2,x3) = ((1,0),(1,0)) x2 + ((1,0),(1,0)) x3 + (49,85) U12_A(x1,x2,x3) = ((1,0),(0,0)) x2 + (25,44) U22_A(x1,x2) = (12,31) U32_A(x1) = (10,30) U51_A(x1,x2) = ((0,0),(1,0)) x1 + ((1,0),(0,0)) x2 + (46,22) U61_A(x1,x2,x3) = ((1,0),(1,0)) x2 + ((1,0),(1,0)) x3 + (49,86) U11_A(x1,x2,x3) = ((1,0),(0,0)) x2 + (26,45) U21_A(x1,x2) = ((0,0),(1,0)) x1 + (13,29) U31_A(x1,x2) = ((0,0),(1,0)) x1 + (15,22) U41_A(x1) = (13,31) n__0_A() = (12,0) precedence: U11# > activate = n__plus = U15 = plus = U14 = U63 = U13 = U52 = U62 = U12 = U22 = U51 = U21 > U16 > U21# > isNatKind > tt = U23 = U41 > U12# > U31# > isNatKind# = U63# = U51# > U13# > U14# = U15# > isNat > U64# > activate# = plus# = U61# = U62# > isNat# > U61 > s = n__s = U64 > U22# > U11 = U31 > |0| = n__0 > U32 partial status: pi(U11#) = [] pi(tt) = [] pi(U12#) = [3] pi(isNatKind) = [] pi(activate) = [1] pi(activate#) = [] pi(n__plus) = [] pi(plus#) = [] pi(s) = [] pi(isNat#) = [1] pi(n__s) = [] pi(isNatKind#) = [] pi(U31#) = [] pi(U21#) = [] pi(U22#) = [2] pi(U61#) = [] pi(isNat) = [] pi(U62#) = [] pi(U63#) = [] pi(U64#) = [] pi(|0|) = [] pi(U51#) = [] pi(U13#) = [3] 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: p1 We remove them from the problem. -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: U12#(tt(),V1,V2) -> activate#(V2) p2: activate#(n__plus(X1,X2)) -> plus#(X1,X2) p3: plus#(N,s(M)) -> isNat#(M) p4: isNat#(n__s(V1)) -> activate#(V1) p5: isNat#(n__s(V1)) -> isNatKind#(activate(V1)) p6: isNatKind#(n__s(V1)) -> activate#(V1) p7: isNatKind#(n__s(V1)) -> isNatKind#(activate(V1)) p8: isNatKind#(n__plus(V1,V2)) -> activate#(V2) p9: isNatKind#(n__plus(V1,V2)) -> isNatKind#(activate(V1)) p10: isNatKind#(n__plus(V1,V2)) -> U31#(isNatKind(activate(V1)),activate(V2)) p11: U31#(tt(),V2) -> isNatKind#(activate(V2)) p12: isNat#(n__s(V1)) -> U21#(isNatKind(activate(V1)),activate(V1)) p13: U21#(tt(),V1) -> activate#(V1) p14: U21#(tt(),V1) -> isNatKind#(activate(V1)) p15: U21#(tt(),V1) -> U22#(isNatKind(activate(V1)),activate(V1)) p16: U22#(tt(),V1) -> activate#(V1) p17: U22#(tt(),V1) -> isNat#(activate(V1)) p18: isNat#(n__plus(V1,V2)) -> activate#(V2) p19: isNat#(n__plus(V1,V2)) -> activate#(V1) p20: isNat#(n__plus(V1,V2)) -> isNatKind#(activate(V1)) p21: isNat#(n__plus(V1,V2)) -> U11#(isNatKind(activate(V1)),activate(V1),activate(V2)) p22: U11#(tt(),V1,V2) -> activate#(V2) p23: U11#(tt(),V1,V2) -> activate#(V1) p24: U11#(tt(),V1,V2) -> isNatKind#(activate(V1)) p25: plus#(N,s(M)) -> U61#(isNat(M),M,N) p26: U61#(tt(),M,N) -> activate#(N) p27: U61#(tt(),M,N) -> activate#(M) p28: U61#(tt(),M,N) -> isNatKind#(activate(M)) p29: U61#(tt(),M,N) -> U62#(isNatKind(activate(M)),activate(M),activate(N)) p30: U62#(tt(),M,N) -> activate#(M) p31: U62#(tt(),M,N) -> activate#(N) p32: U62#(tt(),M,N) -> isNat#(activate(N)) p33: U62#(tt(),M,N) -> U63#(isNat(activate(N)),activate(M),activate(N)) p34: U63#(tt(),M,N) -> activate#(M) p35: U63#(tt(),M,N) -> activate#(N) p36: U63#(tt(),M,N) -> isNatKind#(activate(N)) p37: U63#(tt(),M,N) -> U64#(isNatKind(activate(N)),activate(M),activate(N)) p38: U64#(tt(),M,N) -> activate#(M) p39: U64#(tt(),M,N) -> activate#(N) p40: U64#(tt(),M,N) -> plus#(activate(N),activate(M)) p41: plus#(N,|0|()) -> isNat#(N) p42: plus#(N,|0|()) -> U51#(isNat(N),N) p43: U51#(tt(),N) -> activate#(N) p44: U51#(tt(),N) -> isNatKind#(activate(N)) p45: U12#(tt(),V1,V2) -> isNatKind#(activate(V2)) p46: U12#(tt(),V1,V2) -> U13#(isNatKind(activate(V2)),activate(V1),activate(V2)) p47: U13#(tt(),V1,V2) -> activate#(V1) p48: U13#(tt(),V1,V2) -> activate#(V2) p49: U13#(tt(),V1,V2) -> isNatKind#(activate(V2)) p50: U13#(tt(),V1,V2) -> U14#(isNatKind(activate(V2)),activate(V1),activate(V2)) p51: U14#(tt(),V1,V2) -> activate#(V2) p52: U14#(tt(),V1,V2) -> activate#(V1) p53: U14#(tt(),V1,V2) -> isNat#(activate(V1)) p54: U14#(tt(),V1,V2) -> U15#(isNat(activate(V1)),activate(V2)) p55: U15#(tt(),V2) -> activate#(V2) p56: 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(X1,X2) r32: activate(n__s(X)) -> s(X) r33: activate(X) -> X The estimated dependency graph contains the following SCCs: {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} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: activate#(n__plus(X1,X2)) -> plus#(X1,X2) p2: plus#(N,|0|()) -> U51#(isNat(N),N) p3: U51#(tt(),N) -> isNatKind#(activate(N)) p4: isNatKind#(n__plus(V1,V2)) -> U31#(isNatKind(activate(V1)),activate(V2)) p5: U31#(tt(),V2) -> isNatKind#(activate(V2)) p6: isNatKind#(n__plus(V1,V2)) -> isNatKind#(activate(V1)) p7: isNatKind#(n__plus(V1,V2)) -> activate#(V2) p8: isNatKind#(n__s(V1)) -> isNatKind#(activate(V1)) p9: isNatKind#(n__s(V1)) -> activate#(V1) p10: U51#(tt(),N) -> activate#(N) p11: plus#(N,|0|()) -> isNat#(N) p12: isNat#(n__plus(V1,V2)) -> U11#(isNatKind(activate(V1)),activate(V1),activate(V2)) p13: U11#(tt(),V1,V2) -> isNatKind#(activate(V1)) p14: U11#(tt(),V1,V2) -> activate#(V1) p15: U11#(tt(),V1,V2) -> activate#(V2) p16: isNat#(n__plus(V1,V2)) -> isNatKind#(activate(V1)) p17: isNat#(n__plus(V1,V2)) -> activate#(V1) p18: isNat#(n__plus(V1,V2)) -> activate#(V2) p19: isNat#(n__s(V1)) -> U21#(isNatKind(activate(V1)),activate(V1)) p20: U21#(tt(),V1) -> U22#(isNatKind(activate(V1)),activate(V1)) p21: U22#(tt(),V1) -> isNat#(activate(V1)) p22: isNat#(n__s(V1)) -> isNatKind#(activate(V1)) p23: isNat#(n__s(V1)) -> activate#(V1) p24: U22#(tt(),V1) -> activate#(V1) p25: U21#(tt(),V1) -> isNatKind#(activate(V1)) p26: U21#(tt(),V1) -> activate#(V1) p27: plus#(N,s(M)) -> U61#(isNat(M),M,N) p28: U61#(tt(),M,N) -> U62#(isNatKind(activate(M)),activate(M),activate(N)) p29: U62#(tt(),M,N) -> U63#(isNat(activate(N)),activate(M),activate(N)) p30: U63#(tt(),M,N) -> U64#(isNatKind(activate(N)),activate(M),activate(N)) p31: U64#(tt(),M,N) -> plus#(activate(N),activate(M)) p32: plus#(N,s(M)) -> isNat#(M) p33: U64#(tt(),M,N) -> activate#(N) p34: U64#(tt(),M,N) -> activate#(M) p35: U63#(tt(),M,N) -> isNatKind#(activate(N)) p36: U63#(tt(),M,N) -> activate#(N) p37: U63#(tt(),M,N) -> activate#(M) p38: U62#(tt(),M,N) -> isNat#(activate(N)) p39: U62#(tt(),M,N) -> activate#(N) p40: U62#(tt(),M,N) -> activate#(M) p41: U61#(tt(),M,N) -> isNatKind#(activate(M)) p42: U61#(tt(),M,N) -> activate#(M) p43: U61#(tt(),M,N) -> 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(X1,X2) r32: activate(n__s(X)) -> s(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^2 order: lexicographic order interpretations: activate#_A(x1) = x1 + (36,4) n__plus_A(x1,x2) = ((1,0),(1,1)) x1 + ((1,0),(0,0)) x2 + (39,2) plus#_A(x1,x2) = x1 + x2 + (36,6) |0|_A() = (47,4) U51#_A(x1,x2) = ((1,0),(0,0)) x1 + x2 + (0,11) isNat_A(x1) = (43,9) tt_A() = (37,36) isNatKind#_A(x1) = ((1,0),(0,0)) x1 + (36,51) activate_A(x1) = ((1,0),(1,1)) x1 + (0,12) U31#_A(x1,x2) = x2 + (39,40) isNatKind_A(x1) = ((1,0),(1,0)) x1 + (0,53) n__s_A(x1) = ((1,0),(0,0)) x1 + (49,1) isNat#_A(x1) = x1 + (46,1) U11#_A(x1,x2,x3) = ((1,0),(1,1)) x2 + ((1,0),(0,0)) x3 + (37,52) U21#_A(x1,x2) = ((1,0),(0,0)) x2 + (48,2) U22#_A(x1,x2) = ((1,0),(0,0)) x2 + (47,1) s_A(x1) = ((1,0),(0,0)) x1 + (49,2) U61#_A(x1,x2,x3) = ((1,0),(1,0)) x2 + ((1,0),(1,1)) x3 + (50,51) U62#_A(x1,x2,x3) = ((1,0),(1,0)) x2 + ((1,0),(1,1)) x3 + (46,38) U63#_A(x1,x2,x3) = x1 + x2 + ((1,0),(0,0)) x3 + (2,16) U64#_A(x1,x2,x3) = ((1,0),(1,0)) x2 + ((1,0),(0,0)) x3 + (38,13) U16_A(x1) = (38,7) U15_A(x1,x2) = ((0,0),(1,0)) x2 + (39,8) U64_A(x1,x2,x3) = ((1,0),(0,0)) x2 + ((1,0),(1,0)) x3 + (88,2) plus_A(x1,x2) = ((1,0),(1,1)) x1 + ((1,0),(0,0)) x2 + (39,6) U14_A(x1,x2,x3) = ((0,0),(1,0)) x2 + ((0,0),(1,0)) x3 + (40,37) U63_A(x1,x2,x3) = ((1,0),(0,0)) x2 + ((1,0),(1,0)) x3 + (88,3) U13_A(x1,x2,x3) = ((0,0),(1,0)) x2 + ((0,0),(1,0)) x3 + (41,38) U23_A(x1) = (38,37) U52_A(x1,x2) = ((1,0),(0,0)) x2 + (38,1) U62_A(x1,x2,x3) = ((1,0),(0,0)) x2 + ((1,0),(1,0)) x3 + (88,4) U12_A(x1,x2,x3) = (42,1) U22_A(x1,x2) = ((0,0),(1,0)) x2 + (39,38) U32_A(x1) = (38,37) U51_A(x1,x2) = x2 + (48,5) U61_A(x1,x2,x3) = ((1,0),(0,0)) x2 + ((1,0),(1,0)) x3 + (88,5) U11_A(x1,x2,x3) = (42,3) U21_A(x1,x2) = (40,2) U31_A(x1,x2) = ((0,0),(1,0)) x1 + (38,1) U41_A(x1) = (38,37) n__0_A() = (47,1) precedence: U61# = U62# > U11# > U13 > isNatKind = U12 > U21# = U22# > U63# > U64# > plus# = isNat# > activate# = isNatKind# = U31# > isNat > U14 > activate = plus > U15 = U51 > U52 = U62 = U61 > U63 > U64 > s > |0| = U51# = n__0 > U16 > n__s > n__plus > U11 > U31 = U41 > U32 > tt = U23 = U22 = U21 partial status: pi(activate#) = [] pi(n__plus) = [] pi(plus#) = [1] pi(|0|) = [] pi(U51#) = [2] pi(isNat) = [] pi(tt) = [] pi(isNatKind#) = [] pi(activate) = [1] pi(U31#) = [] pi(isNatKind) = [] pi(n__s) = [] pi(isNat#) = [1] pi(U11#) = [] pi(U21#) = [] pi(U22#) = [] pi(s) = [] pi(U61#) = [] pi(U62#) = [] pi(U63#) = [2] 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: p1 We remove them from the problem. -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: plus#(N,|0|()) -> U51#(isNat(N),N) p2: U51#(tt(),N) -> isNatKind#(activate(N)) p3: isNatKind#(n__plus(V1,V2)) -> U31#(isNatKind(activate(V1)),activate(V2)) p4: U31#(tt(),V2) -> isNatKind#(activate(V2)) p5: isNatKind#(n__plus(V1,V2)) -> isNatKind#(activate(V1)) p6: isNatKind#(n__plus(V1,V2)) -> activate#(V2) p7: isNatKind#(n__s(V1)) -> isNatKind#(activate(V1)) p8: isNatKind#(n__s(V1)) -> activate#(V1) p9: U51#(tt(),N) -> activate#(N) p10: plus#(N,|0|()) -> isNat#(N) p11: isNat#(n__plus(V1,V2)) -> U11#(isNatKind(activate(V1)),activate(V1),activate(V2)) p12: U11#(tt(),V1,V2) -> isNatKind#(activate(V1)) p13: U11#(tt(),V1,V2) -> activate#(V1) p14: U11#(tt(),V1,V2) -> activate#(V2) p15: isNat#(n__plus(V1,V2)) -> isNatKind#(activate(V1)) p16: isNat#(n__plus(V1,V2)) -> activate#(V1) p17: isNat#(n__plus(V1,V2)) -> activate#(V2) p18: isNat#(n__s(V1)) -> U21#(isNatKind(activate(V1)),activate(V1)) p19: U21#(tt(),V1) -> U22#(isNatKind(activate(V1)),activate(V1)) p20: U22#(tt(),V1) -> isNat#(activate(V1)) p21: isNat#(n__s(V1)) -> isNatKind#(activate(V1)) p22: isNat#(n__s(V1)) -> activate#(V1) p23: U22#(tt(),V1) -> activate#(V1) p24: U21#(tt(),V1) -> isNatKind#(activate(V1)) p25: U21#(tt(),V1) -> activate#(V1) p26: plus#(N,s(M)) -> U61#(isNat(M),M,N) p27: U61#(tt(),M,N) -> U62#(isNatKind(activate(M)),activate(M),activate(N)) p28: U62#(tt(),M,N) -> U63#(isNat(activate(N)),activate(M),activate(N)) p29: U63#(tt(),M,N) -> U64#(isNatKind(activate(N)),activate(M),activate(N)) p30: U64#(tt(),M,N) -> plus#(activate(N),activate(M)) p31: plus#(N,s(M)) -> isNat#(M) p32: U64#(tt(),M,N) -> activate#(N) p33: U64#(tt(),M,N) -> activate#(M) p34: U63#(tt(),M,N) -> isNatKind#(activate(N)) p35: U63#(tt(),M,N) -> activate#(N) p36: U63#(tt(),M,N) -> activate#(M) p37: U62#(tt(),M,N) -> isNat#(activate(N)) p38: U62#(tt(),M,N) -> activate#(N) p39: U62#(tt(),M,N) -> activate#(M) p40: U61#(tt(),M,N) -> isNatKind#(activate(M)) p41: U61#(tt(),M,N) -> activate#(M) p42: U61#(tt(),M,N) -> 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(X1,X2) r32: activate(n__s(X)) -> s(X) r33: activate(X) -> X The estimated dependency graph contains the following SCCs: {p26, p27, p28, p29, p30} {p18, p19, p20} {p3, p4, p5, p7} -- 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(X1,X2) r32: activate(n__s(X)) -> s(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^2 order: lexicographic order interpretations: U64#_A(x1,x2,x3) = ((1,0),(1,0)) x2 + ((0,0),(1,0)) x3 + (5,7) tt_A() = (4,5) plus#_A(x1,x2) = ((0,0),(1,0)) x1 + ((1,0),(1,0)) x2 + (5,6) activate_A(x1) = ((1,0),(1,1)) x1 + (0,11) s_A(x1) = ((1,0),(0,0)) x1 + (9,2) U61#_A(x1,x2,x3) = ((1,0),(1,0)) x2 + ((0,0),(1,0)) x3 + (6,10) isNat_A(x1) = ((1,0),(0,0)) x1 + (3,14) U62#_A(x1,x2,x3) = ((1,0),(1,0)) x2 + ((0,0),(1,0)) x3 + (6,9) isNatKind_A(x1) = ((1,0),(0,0)) x1 + (3,9) U63#_A(x1,x2,x3) = ((1,0),(1,0)) x2 + ((0,0),(1,0)) x3 + (6,8) U16_A(x1) = ((0,0),(1,0)) x1 + (5,3) U15_A(x1,x2) = ((0,0),(1,0)) x1 + ((0,0),(1,0)) x2 + (6,4) U64_A(x1,x2,x3) = ((1,0),(0,0)) x2 + ((1,0),(0,0)) x3 + (20,3) plus_A(x1,x2) = ((1,0),(1,1)) x1 + ((1,0),(1,1)) x2 + (11,13) U14_A(x1,x2,x3) = (7,6) U63_A(x1,x2,x3) = ((1,0),(0,0)) x2 + ((1,0),(0,0)) x3 + (20,4) U13_A(x1,x2,x3) = (8,10) U23_A(x1) = ((0,0),(1,0)) x1 + (5,10) U52_A(x1,x2) = ((1,0),(0,0)) x2 + (1,6) U62_A(x1,x2,x3) = ((1,0),(0,0)) x2 + ((1,0),(0,0)) x3 + (20,6) U12_A(x1,x2,x3) = ((1,0),(0,0)) x3 + (9,12) U22_A(x1,x2) = (6,12) U32_A(x1) = (4,5) U51_A(x1,x2) = ((0,0),(1,0)) x1 + x2 + (2,8) U61_A(x1,x2,x3) = ((1,0),(0,0)) x2 + ((1,0),(0,0)) x3 + (20,12) U11_A(x1,x2,x3) = ((1,0),(0,0)) x3 + (10,13) U21_A(x1,x2) = (7,13) U31_A(x1,x2) = ((0,0),(1,0)) x1 + (12,10) U41_A(x1) = (5,6) |0|_A() = (5,7) n__0_A() = (5,6) n__plus_A(x1,x2) = x1 + ((1,0),(1,1)) x2 + (11,12) n__s_A(x1) = ((1,0),(0,0)) x1 + (9,1) precedence: isNat = U52 > U64# = plus# = activate = U61# > isNatKind > plus = U51 > U15 > U64 > U16 > U63 = U31 = |0| > n__plus > tt = U32 = U41 > U62# > U63# > s = U12 = U61 = U11 > U13 > U14 > U23 = U62 = U22 = U21 = n__0 = n__s partial status: pi(U64#) = [] pi(tt) = [] pi(plus#) = [] pi(activate) = [1] pi(s) = [] 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) = [] pi(U11) = [] pi(U21) = [] pi(U31) = [] pi(U41) = [] pi(|0|) = [] pi(n__0) = [] pi(n__plus) = [] pi(n__s) = [] 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: U64#(tt(),M,N) -> plus#(activate(N),activate(M)) p2: plus#(N,s(M)) -> U61#(isNat(M),M,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(X1,X2) r32: activate(n__s(X)) -> s(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: isNat#(n__s(V1)) -> U21#(isNatKind(activate(V1)),activate(V1)) p2: U21#(tt(),V1) -> U22#(isNatKind(activate(V1)),activate(V1)) p3: 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(X1,X2) r32: activate(n__s(X)) -> s(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^2 order: lexicographic order interpretations: isNat#_A(x1) = ((1,0),(1,1)) x1 + (11,6) n__s_A(x1) = ((1,0),(0,0)) x1 + (14,46) U21#_A(x1,x2) = ((0,0),(1,0)) x1 + x2 + (13,29) isNatKind_A(x1) = ((1,0),(1,0)) x1 + (3,38) activate_A(x1) = x1 + (0,35) tt_A() = (10,42) U22#_A(x1,x2) = ((1,0),(1,0)) x2 + (12,40) U16_A(x1) = (11,1) U15_A(x1,x2) = (12,2) isNat_A(x1) = x1 + (9,106) U14_A(x1,x2,x3) = (13,3) U13_A(x1,x2,x3) = ((1,0),(0,0)) x1 + ((0,0),(1,0)) x3 + (4,4) U23_A(x1) = (11,43) U64_A(x1,x2,x3) = ((0,0),(1,0)) x1 + ((1,0),(0,0)) x2 + ((1,0),(0,0)) x3 + (14,98) s_A(x1) = ((1,0),(0,0)) x1 + (14,54) plus_A(x1,x2) = ((1,0),(1,1)) x1 + ((1,0),(1,1)) x2 + (0,37) U12_A(x1,x2,x3) = ((1,0),(0,0)) x3 + (8,5) U22_A(x1,x2) = (12,44) U63_A(x1,x2,x3) = ((1,0),(0,0)) x2 + ((1,0),(1,0)) x3 + (14,102) U11_A(x1,x2,x3) = ((1,0),(0,0)) x1 + ((0,0),(1,0)) x2 + ((1,0),(1,1)) x3 + (1,36) U21_A(x1,x2) = (13,45) U52_A(x1,x2) = ((1,0),(1,1)) x2 + (1,36) U62_A(x1,x2,x3) = ((1,0),(0,0)) x2 + ((1,0),(1,0)) x3 + (14,103) U32_A(x1) = x1 + (0,5) U51_A(x1,x2) = ((1,0),(1,1)) x2 + (4,72) U61_A(x1,x2,x3) = ((1,0),(1,0)) x2 + ((1,0),(1,0)) x3 + (14,104) n__0_A() = (8,43) n__plus_A(x1,x2) = ((1,0),(1,1)) x1 + ((1,0),(1,1)) x2 + (0,36) U31_A(x1,x2) = ((0,0),(1,0)) x1 + ((1,0),(1,0)) x2 + (3,34) U41_A(x1) = x1 + (1,0) |0|_A() = (8,62) precedence: U41 > U64 = s = U63 = U62 > U22# > tt = isNat = U11 > U13 = U12 > U16 = U15 = U14 > U23 = U22 = U21 > n__s > activate = |0| > U52 > n__0 > isNat# = U21# = isNatKind = plus = U32 = U51 = U61 = n__plus = U31 partial status: pi(isNat#) = [1] pi(n__s) = [] pi(U21#) = [] pi(isNatKind) = [] pi(activate) = [1] pi(tt) = [] pi(U22#) = [] pi(U16) = [] pi(U15) = [] pi(isNat) = [1] pi(U14) = [] pi(U13) = [] pi(U23) = [] pi(U64) = [] pi(s) = [] pi(plus) = [1] pi(U12) = [] pi(U22) = [] pi(U63) = [] pi(U11) = [3] pi(U21) = [] pi(U52) = [] pi(U62) = [] pi(U32) = [] pi(U51) = [2] pi(U61) = [] pi(n__0) = [] pi(n__plus) = [] pi(U31) = [] pi(U41) = [] pi(|0|) = [] The next rules are strictly ordered: p1 We remove them from the problem. -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: U21#(tt(),V1) -> U22#(isNatKind(activate(V1)),activate(V1)) p2: 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(X1,X2) r32: activate(n__s(X)) -> s(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__s(V1)) -> isNatKind#(activate(V1)) p4: 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(X1,X2) r32: activate(n__s(X)) -> s(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^2 order: lexicographic order interpretations: isNatKind#_A(x1) = ((1,0),(1,1)) x1 + (1,1) n__plus_A(x1,x2) = ((1,0),(1,0)) x1 + ((1,0),(1,1)) x2 + (3,11) U31#_A(x1,x2) = x2 + (2,6) isNatKind_A(x1) = ((1,0),(1,1)) x1 + (1,8) activate_A(x1) = x1 + (0,4) tt_A() = (23,7) n__s_A(x1) = x1 + (20,13) U16_A(x1) = (24,8) U15_A(x1,x2) = (25,9) isNat_A(x1) = ((1,0),(1,1)) x1 + (23,51) U14_A(x1,x2,x3) = x1 + (3,3) U13_A(x1,x2,x3) = ((1,0),(1,1)) x3 + (5,16) U23_A(x1) = (24,8) U64_A(x1,x2,x3) = ((1,0),(1,1)) x2 + ((1,0),(1,0)) x3 + (23,30) s_A(x1) = x1 + (20,14) plus_A(x1,x2) = ((1,0),(1,0)) x1 + ((1,0),(1,1)) x2 + (3,12) U12_A(x1,x2,x3) = ((0,0),(1,0)) x1 + ((1,0),(1,1)) x3 + (6,1) U22_A(x1,x2) = ((0,0),(1,0)) x1 + (25,7) U63_A(x1,x2,x3) = ((1,0),(1,1)) x2 + ((1,0),(1,0)) x3 + (23,35) U11_A(x1,x2,x3) = ((0,0),(1,0)) x1 + ((0,0),(1,0)) x2 + ((1,0),(1,1)) x3 + (7,7) U21_A(x1,x2) = ((0,0),(1,0)) x2 + (26,14) U52_A(x1,x2) = ((0,0),(1,0)) x1 + ((1,0),(1,0)) x2 + (24,13) U62_A(x1,x2,x3) = ((1,0),(1,1)) x2 + ((1,0),(1,0)) x3 + (23,40) U32_A(x1) = ((0,0),(1,0)) x1 + (24,1) U51_A(x1,x2) = ((1,0),(0,0)) x2 + (25,13) U61_A(x1,x2,x3) = ((1,0),(1,1)) x2 + ((1,0),(1,0)) x3 + (23,45) n__0_A() = (26,8) U31_A(x1,x2) = ((1,0),(0,0)) x1 + ((0,0),(1,0)) x2 + (3,3) U41_A(x1) = ((1,0),(0,0)) x1 + (20,8) |0|_A() = (26,12) precedence: n__s = isNat = U13 = U64 = s = U12 = U63 = U11 = U21 = U62 > U14 > U16 > activate > U31# = tt = U23 = U22 = U32 = U31 = U41 > isNatKind# = isNatKind > U15 > n__plus = plus = U61 > U52 = U51 > n__0 = |0| partial status: pi(isNatKind#) = [1] pi(n__plus) = [] pi(U31#) = [] pi(isNatKind) = [1] pi(activate) = [1] pi(tt) = [] pi(n__s) = [] pi(U16) = [] pi(U15) = [] pi(isNat) = [] pi(U14) = [] pi(U13) = [] pi(U23) = [] pi(U64) = [] pi(s) = [] pi(plus) = [2] pi(U12) = [] pi(U22) = [] pi(U63) = [] pi(U11) = [] pi(U21) = [] pi(U52) = [] pi(U62) = [] pi(U32) = [] pi(U51) = [] pi(U61) = [2] pi(n__0) = [] pi(U31) = [] pi(U41) = [] pi(|0|) = [] The next rules are strictly ordered: p1 We remove them from the problem. -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: U31#(tt(),V2) -> isNatKind#(activate(V2)) p2: isNatKind#(n__s(V1)) -> isNatKind#(activate(V1)) 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(X1,X2) r32: activate(n__s(X)) -> s(X) r33: activate(X) -> X The estimated dependency graph contains the following SCCs: {p2, p3} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: isNatKind#(n__s(V1)) -> isNatKind#(activate(V1)) 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(X1,X2) r32: activate(n__s(X)) -> s(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^2 order: lexicographic order interpretations: isNatKind#_A(x1) = ((1,0),(0,0)) x1 + (14,0) n__s_A(x1) = ((1,0),(0,0)) x1 + (14,9) activate_A(x1) = x1 n__plus_A(x1,x2) = x1 + ((1,0),(1,0)) x2 U16_A(x1) = ((1,0),(0,0)) x1 + (1,3) tt_A() = (7,2) U15_A(x1,x2) = ((1,0),(0,0)) x2 + (9,4) isNat_A(x1) = ((1,0),(0,0)) x1 + (7,11) U14_A(x1,x2,x3) = ((1,0),(0,0)) x3 + (10,5) U13_A(x1,x2,x3) = ((1,0),(0,0)) x3 + (11,6) isNatKind_A(x1) = ((1,0),(0,0)) x1 + (0,9) U23_A(x1) = (7,3) U32_A(x1) = ((1,0),(0,0)) x1 + (1,3) U64_A(x1,x2,x3) = ((1,0),(1,0)) x2 + ((1,0),(0,0)) x3 + (14,10) s_A(x1) = ((1,0),(0,0)) x1 + (14,9) plus_A(x1,x2) = x1 + ((1,0),(1,0)) x2 U12_A(x1,x2,x3) = ((1,0),(0,0)) x1 + ((1,0),(0,0)) x3 + (5,7) U22_A(x1,x2) = (8,4) U31_A(x1,x2) = ((1,0),(0,0)) x1 + ((1,0),(0,0)) x2 + (0,4) U41_A(x1) = ((1,0),(0,0)) x1 + (13,8) U63_A(x1,x2,x3) = ((1,0),(1,0)) x2 + ((1,0),(0,0)) x3 + (14,11) U11_A(x1,x2,x3) = ((1,0),(0,0)) x2 + ((1,0),(0,0)) x3 + (6,8) U21_A(x1,x2) = (15,10) U52_A(x1,x2) = ((1,0),(1,1)) x2 + (8,3) U62_A(x1,x2,x3) = ((1,0),(1,0)) x2 + ((1,0),(0,0)) x3 + (14,12) n__0_A() = (12,1) U51_A(x1,x2) = ((1,0),(0,0)) x2 + (11,2) U61_A(x1,x2,x3) = ((1,0),(1,0)) x2 + x3 + (14,13) |0|_A() = (12,1) precedence: isNatKind# > n__plus = isNatKind = U32 = plus = U31 = U62 = U61 > U64 = U63 > n__s = s = U52 > activate = U16 = tt = U15 = U14 = U13 = U12 > isNat = U23 = U22 = U11 = U21 = n__0 = |0| > U51 > U41 partial status: pi(isNatKind#) = [] pi(n__s) = [] pi(activate) = [1] pi(n__plus) = [] pi(U16) = [] pi(tt) = [] pi(U15) = [] pi(isNat) = [] 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) = [] pi(U21) = [] pi(U52) = [] pi(U62) = [] pi(n__0) = [] pi(U51) = [] pi(U61) = [] pi(|0|) = [] The next rules are strictly ordered: p1 We remove them from the problem. -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: 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(X1,X2) r32: activate(n__s(X)) -> s(X) r33: activate(X) -> X The estimated dependency graph contains the following SCCs: {p1} -- 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(X1,X2) r32: activate(n__s(X)) -> s(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^2 order: lexicographic order interpretations: isNatKind#_A(x1) = ((1,0),(0,0)) x1 n__plus_A(x1,x2) = ((1,0),(0,0)) x1 + ((1,0),(1,0)) x2 + (98,14) activate_A(x1) = ((1,0),(1,0)) x1 + (8,16) U16_A(x1) = (30,2) tt_A() = (29,3) U15_A(x1,x2) = x1 + ((0,0),(1,0)) x2 + (2,1) isNat_A(x1) = x1 + (18,3) U14_A(x1,x2,x3) = ((1,0),(1,0)) x1 + ((1,0),(1,0)) x2 + ((0,0),(1,0)) x3 U13_A(x1,x2,x3) = ((1,0),(1,0)) x2 + (55,0) isNatKind_A(x1) = (46,11) U23_A(x1) = (30,4) U32_A(x1) = (30,4) U64_A(x1,x2,x3) = (42,14) s_A(x1) = (41,13) plus_A(x1,x2) = ((1,0),(1,0)) x1 + ((1,0),(1,0)) x2 + (98,113) U12_A(x1,x2,x3) = x2 + ((1,0),(1,1)) x3 + (64,17) U22_A(x1,x2) = (31,5) U31_A(x1,x2) = (46,1) U41_A(x1) = (32,1) U63_A(x1,x2,x3) = (43,17) U11_A(x1,x2,x3) = ((1,0),(1,0)) x2 + ((1,0),(0,0)) x3 + (81,10) U21_A(x1,x2) = ((0,0),(1,0)) x2 + (32,6) U52_A(x1,x2) = ((1,0),(1,0)) x2 + (22,17) U62_A(x1,x2,x3) = (44,18) n__0_A() = (41,0) n__s_A(x1) = ((0,0),(1,0)) x1 + (33,12) U51_A(x1,x2) = ((1,0),(1,0)) x2 + (47,26) U61_A(x1,x2,x3) = (45,19) |0|_A() = (48,4) precedence: n__plus = isNat = U23 = U32 = U64 = plus = U63 = U21 = n__0 > isNatKind > U22 > isNatKind# = U31 = U11 > U15 = U14 = U41 = |0| > activate = U16 = tt = U13 = s = U12 > U62 = U61 > U52 = U51 > n__s partial status: pi(isNatKind#) = [] pi(n__plus) = [] pi(activate) = [] pi(U16) = [] pi(tt) = [] pi(U15) = [] pi(isNat) = [] pi(U14) = [] pi(U13) = [] pi(isNatKind) = [] pi(U23) = [] pi(U32) = [] pi(U64) = [] pi(s) = [] pi(plus) = [] pi(U12) = [2] pi(U22) = [] pi(U31) = [] pi(U41) = [] pi(U63) = [] pi(U11) = [] pi(U21) = [] pi(U52) = [] pi(U62) = [] pi(n__0) = [] pi(n__s) = [] pi(U51) = [] pi(U61) = [] pi(|0|) = [] The next rules are strictly ordered: p1 We remove them from the problem. Then no dependency pair remains.