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: lexicographic combination of reduction pairs: 1. weighted path order base order: matrix interpretations: carrier: N^2 order: lexicographic order interpretations: U11#_A(x1,x2,x3) = ((0,0),(1,0)) x1 + x2 + ((1,0),(0,0)) x3 + (53,91) tt_A() = (0,93) U12#_A(x1,x2,x3) = x1 + x2 + x3 + (38,0) isNatKind_A(x1) = ((0,0),(1,0)) x1 + (14,93) activate_A(x1) = ((1,0),(1,1)) x1 + (0,45) activate#_A(x1) = ((1,0),(1,0)) x1 + (1,93) n__plus_A(x1,x2) = ((1,0),(1,1)) x1 + ((1,0),(0,0)) x2 + (52,47) plus#_A(x1,x2) = x1 + x2 + (9,146) s_A(x1) = ((1,0),(0,0)) x1 + (11,2) isNat#_A(x1) = ((1,0),(0,0)) x1 + (2,149) n__s_A(x1) = ((1,0),(0,0)) x1 + (11,1) isNatKind#_A(x1) = x1 + (2,47) U31#_A(x1,x2) = x1 + ((1,0),(1,0)) x2 + (39,2) U21#_A(x1,x2) = ((1,0),(0,0)) x2 + (13,148) U22#_A(x1,x2) = ((0,0),(1,0)) x1 + ((1,0),(0,0)) x2 + (13,133) U61#_A(x1,x2,x3) = x2 + x3 + (13,185) isNat_A(x1) = x1 + (19,297) U62#_A(x1,x2,x3) = x2 + x3 + (12,94) U63#_A(x1,x2,x3) = x2 + x3 + (11,94) U64#_A(x1,x2,x3) = ((1,0),(0,0)) x2 + x3 + (10,50) |0|_A() = (20,150) U51#_A(x1,x2) = x2 + (21,296) U52#_A(x1,x2) = ((1,0),(1,1)) x2 + (2,93) U13#_A(x1,x2,x3) = x1 + x2 + ((1,0),(1,1)) x3 + (23,0) U14#_A(x1,x2,x3) = ((1,0),(0,0)) x2 + ((1,0),(1,0)) x3 + (22,93) U15#_A(x1,x2) = ((1,0),(0,0)) x1 + ((1,0),(1,0)) x2 + (2,150) U16_A(x1) = ((1,0),(1,1)) x1 + (1,1) U15_A(x1,x2) = ((1,0),(1,0)) x2 + (21,44) U64_A(x1,x2,x3) = ((1,0),(0,0)) x2 + ((1,0),(0,0)) x3 + (63,150) plus_A(x1,x2) = ((1,0),(1,1)) x1 + ((1,0),(1,0)) x2 + (52,143) U14_A(x1,x2,x3) = ((1,0),(0,0)) x1 + ((1,0),(0,0)) x3 + (22,1) U63_A(x1,x2,x3) = ((1,0),(0,0)) x2 + ((1,0),(0,0)) x3 + (63,151) U13_A(x1,x2,x3) = ((1,0),(0,0)) x2 + ((1,0),(0,0)) x3 + (37,2) U23_A(x1) = (1,94) U52_A(x1,x2) = x2 + (1,46) U62_A(x1,x2,x3) = ((1,0),(0,0)) x2 + ((1,0),(0,0)) x3 + (63,152) U12_A(x1,x2,x3) = ((1,0),(0,0)) x2 + ((1,0),(0,0)) x3 + (38,3) U22_A(x1,x2) = (14,343) U32_A(x1) = (0,94) U51_A(x1,x2) = ((1,0),(1,0)) x2 + (2,92) U61_A(x1,x2,x3) = ((1,0),(0,0)) x2 + ((1,0),(0,0)) x3 + (63,153) U11_A(x1,x2,x3) = x2 + ((1,0),(0,0)) x3 + (39,44) U21_A(x1,x2) = x1 + (15,1) U31_A(x1,x2) = (0,95) U41_A(x1) = (14,103) n__0_A() = (20,94) precedence: n__s > isNatKind > U62# > U64 > |0| > n__plus = s = isNat# = U15# = plus > activate = U52 = n__0 > U11# > U12# > U13# = U41 > U12 > U61 > U13 > U11 > isNat > U21 > U23 > U22 > U16 > tt = U32 > U31# > U14# = U15 = U51 > U64# = U62 = U31 > U21# > plus# = U61# > U51# = U52# > isNatKind# > activate# = U22# = U63# > U14 > U63 partial status: pi(U11#) = [2] pi(tt) = [] pi(U12#) = [1, 3] pi(isNatKind) = [] pi(activate) = [1] pi(activate#) = [] pi(n__plus) = [] pi(plus#) = [1, 2] pi(s) = [] pi(isNat#) = [] pi(n__s) = [] pi(isNatKind#) = [1] pi(U31#) = [1] pi(U21#) = [] pi(U22#) = [] pi(U61#) = [3] pi(isNat) = [1] pi(U62#) = [] pi(U63#) = [2] pi(U64#) = [3] pi(|0|) = [] pi(U51#) = [2] pi(U52#) = [] pi(U13#) = [1, 2, 3] pi(U14#) = [] pi(U15#) = [] pi(U16) = [1] pi(U15) = [] pi(U64) = [] pi(plus) = [1] pi(U14) = [] pi(U63) = [] pi(U13) = [] pi(U23) = [] pi(U52) = [2] pi(U62) = [] pi(U12) = [] pi(U22) = [] pi(U32) = [] pi(U51) = [] pi(U61) = [] pi(U11) = [] pi(U21) = [] pi(U31) = [] pi(U41) = [] pi(n__0) = [] 2. weighted path order base order: matrix interpretations: carrier: N^2 order: lexicographic order interpretations: U11#_A(x1,x2,x3) = ((1,0),(1,1)) x2 + (17,24) tt_A() = (23,20) U12#_A(x1,x2,x3) = ((1,0),(0,0)) x1 + ((0,0),(1,0)) x3 + (11,21) isNatKind_A(x1) = (6,18) activate_A(x1) = (3,5) activate#_A(x1) = (17,24) n__plus_A(x1,x2) = (0,3) plus#_A(x1,x2) = x1 + ((1,0),(1,1)) x2 + (18,25) s_A(x1) = (25,33) isNat#_A(x1) = (44,32) n__s_A(x1) = (0,19) isNatKind#_A(x1) = ((1,0),(0,0)) x1 + (19,20) U31#_A(x1,x2) = ((1,0),(1,0)) x1 + (1,1) U21#_A(x1,x2) = (21,25) U22#_A(x1,x2) = (20,4) U61#_A(x1,x2,x3) = (23,23) isNat_A(x1) = ((1,0),(0,0)) x1 + (44,84) U62#_A(x1,x2,x3) = (45,46) U63#_A(x1,x2,x3) = x2 + (29,40) U64#_A(x1,x2,x3) = ((1,0),(0,0)) x3 + (25,39) |0|_A() = (25,85) U51#_A(x1,x2) = (24,25) U52#_A(x1,x2) = (23,0) U13#_A(x1,x2,x3) = x1 + ((1,0),(1,0)) x2 + (24,0) U14#_A(x1,x2,x3) = (46,33) U15#_A(x1,x2) = (45,4) U16_A(x1) = x1 + (1,1) U15_A(x1,x2) = (49,86) U64_A(x1,x2,x3) = (26,34) plus_A(x1,x2) = (45,2) U14_A(x1,x2,x3) = (50,87) U63_A(x1,x2,x3) = (27,35) U13_A(x1,x2,x3) = (2,88) U23_A(x1) = (24,21) U52_A(x1,x2) = ((1,0),(1,0)) x2 + (21,18) U62_A(x1,x2,x3) = (28,36) U12_A(x1,x2,x3) = (4,89) U22_A(x1,x2) = (25,85) U32_A(x1) = (1,1) U51_A(x1,x2) = (46,86) U61_A(x1,x2,x3) = (29,1) U11_A(x1,x2,x3) = (5,90) U21_A(x1,x2) = (26,86) U31_A(x1,x2) = (3,4) U41_A(x1) = (24,21) n__0_A() = (1,0) precedence: s = U41 = n__0 > U23 > |0| > U12 > U51 > U52 > U14 > U63 > U63# > isNat# > U11# = U12# > activate > n__s > U64# > plus# = U31# = isNat > isNatKind > U61# > tt > U62# > isNatKind# = U13# > n__plus = plus > U61 > U13 > U31 > U32 > U11 > U15 > U16 > U14# > U62 > U21 > U51# > U64 > U21# > activate# > U22 > U15# > U22# > U52# partial status: pi(U11#) = [] pi(tt) = [] pi(U12#) = [] pi(isNatKind) = [] pi(activate) = [] pi(activate#) = [] pi(n__plus) = [] pi(plus#) = [2] 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#) = [1] pi(U14#) = [] pi(U15#) = [] pi(U16) = [] pi(U15) = [] pi(U64) = [] pi(plus) = [] pi(U14) = [] pi(U63) = [] pi(U13) = [] pi(U23) = [] pi(U52) = [] pi(U62) = [] pi(U12) = [] pi(U22) = [] pi(U32) = [] pi(U51) = [] pi(U61) = [] pi(U11) = [] pi(U21) = [] pi(U31) = [] pi(U41) = [] pi(n__0) = [] The next rules are strictly ordered: p3, p4, p5, p6, p7, p8, p9, p10, p11, p12, p14, p16, p17, p18, p19, p20, p21, p22, p23, p27, p28, p29, p30, p31, p32, p33, p34, p36, p37, p39, p40, p41, p42, p44, p45, p46, p47, p48, p49, p51, p56, p58, p59, p60, p61, p62 We remove them from the problem. -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: U11#(tt(),V1,V2) -> U12#(isNatKind(activate(V1)),activate(V1),activate(V2)) p2: U12#(tt(),V1,V2) -> activate#(V1) p3: U31#(tt(),V2) -> activate#(V2) p4: isNat#(n__s(V1)) -> U21#(isNatKind(activate(V1)),activate(V1)) p5: isNat#(n__plus(V1,V2)) -> U11#(isNatKind(activate(V1)),activate(V1),activate(V2)) p6: U11#(tt(),V1,V2) -> activate#(V2) p7: U11#(tt(),V1,V2) -> activate#(V1) p8: U62#(tt(),M,N) -> isNat#(activate(N)) p9: U63#(tt(),M,N) -> activate#(N) p10: U64#(tt(),M,N) -> plus#(activate(N),activate(M)) p11: U12#(tt(),V1,V2) -> activate#(V2) p12: U12#(tt(),V1,V2) -> U13#(isNatKind(activate(V2)),activate(V1),activate(V2)) p13: U13#(tt(),V1,V2) -> activate#(V1) p14: U13#(tt(),V1,V2) -> activate#(V2) p15: U13#(tt(),V1,V2) -> isNatKind#(activate(V2)) p16: U14#(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: (no SCCs)