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: max/plus interpretations on natural numbers: U11#_A(x1,x2,x3) = max{x1 - 69, x2 + 744, x3 + 75} tt_A = 251 U12#_A(x1,x2,x3) = max{x1 - 125, x2 + 472, x3 - 88} isNatKind_A(x1) = max{199, x1 - 13} activate_A(x1) = max{271, x1} activate#_A(x1) = max{163, x1 - 189} n__plus_A(x1,x2) = max{x1 + 1121, x2 + 188} plus#_A(x1,x2) = max{185, x1 + 167, x2 - 14} s_A(x1) = max{1206, x1} isNat#_A(x1) = max{165, x1 - 105} n__s_A(x1) = max{1206, x1} isNatKind#_A(x1) = max{161, x1 - 187} U31#_A(x1,x2) = max{163, x1 - 166, x2 - 110} U21#_A(x1,x2) = max{168, x2 - 105} U22#_A(x1,x2) = max{166, x2 - 105} U61#_A(x1,x2,x3) = max{440, x1 + 2, x2 - 14, x3 + 167} isNat_A(x1) = max{166, x1 - 17} U62#_A(x1,x2,x3) = max{440, x1 - 1, x2 - 14, x3 + 167} U63#_A(x1,x2,x3) = max{439, x1 - 181, x2 - 14, x3 + 167} U64#_A(x1,x2,x3) = max{438, x1 + 180, x2 - 14, x3 + 167} |0|_A = 270 U51#_A(x1,x2) = max{161, x1 + 18, x2} U52#_A(x1,x2) = max{x1 + 10, x2 - 111} U13#_A(x1,x2,x3) = max{x2 + 200, x3 - 89} U14#_A(x1,x2,x3) = max{178, x2 - 95, x3 - 89} U15#_A(x1,x2) = max{164, x1 - 79, x2 - 94} U16_A(x1) = 252 U15_A(x1,x2) = max{47, x1 + 1} U64_A(x1,x2,x3) = max{1392, x2 + 188, x3 + 1121} plus_A(x1,x2) = max{x1 + 1121, x2 + 188} U14_A(x1,x2,x3) = max{48, x1 + 4, x2 - 16} U63_A(x1,x2,x3) = max{1393, x2 + 188, x3 + 1121} U13_A(x1,x2,x3) = max{49, x1 + 11, x2 - 1, x3 - 9} U23_A(x1) = 270 U52_A(x1,x2) = max{x1 + 74, x2 + 2} U62_A(x1,x2,x3) = max{1394, x1 + 21, x2 + 188, x3 + 1121} U12_A(x1,x2,x3) = max{x2 + 272, x3 - 2} U22_A(x1,x2) = 270 U32_A(x1) = 252 U51_A(x1,x2) = max{333, x1 + 82, x2 + 272} U61_A(x1,x2,x3) = max{1394, x2 + 188, x3 + 1121} U11_A(x1,x2,x3) = max{x1 - 93, x2 + 543, x3 - 1} U21_A(x1,x2) = max{272, x2 - 289} U31_A(x1,x2) = max{272, x2 + 62} U41_A(x1) = 1009 n__0_A = 269 precedence: isNat > U11 > isNatKind > n__plus = U15# = plus > U51 > U31 > U32 > |0| > isNat# = U21# = U22# = n__0 > U51# = U61 > U62 > U11# > U12# > U13# > isNatKind# > U31# > U63 > U52 > U14# > activate# > U12 > U21 > U13 > U14 > U15 > U52# = U16 = U22 > U23 > activate > U64 > s > n__s = U41 > tt = plus# = U61# = U62# = U63# = U64# partial status: pi(U11#) = [2, 3] pi(tt) = [] pi(U12#) = [2] pi(isNatKind) = [] pi(activate) = [1] pi(activate#) = [] pi(n__plus) = [1] 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#) = [1, 2] pi(U52#) = [] pi(U13#) = [] pi(U14#) = [] pi(U15#) = [] pi(U16) = [] pi(U15) = [] pi(U64) = [2] pi(plus) = [1] pi(U14) = [] pi(U63) = [2, 3] pi(U13) = [] pi(U23) = [] pi(U52) = [1] pi(U62) = [1, 2, 3] pi(U12) = [] pi(U22) = [] pi(U32) = [] pi(U51) = [1, 2] pi(U61) = [] pi(U11) = [2] pi(U21) = [] pi(U31) = [2] pi(U41) = [] pi(n__0) = [] 2. weighted path order base order: max/plus interpretations on natural numbers: U11#_A(x1,x2,x3) = max{x2 + 215, x3 - 202} tt_A = 38 U12#_A(x1,x2,x3) = x2 + 8 isNatKind_A(x1) = 261 activate_A(x1) = 206 activate#_A(x1) = 6 n__plus_A(x1,x2) = 7 plus#_A(x1,x2) = 218 s_A(x1) = 18 isNat#_A(x1) = 5 n__s_A(x1) = 4 isNatKind#_A(x1) = 216 U31#_A(x1,x2) = 216 U21#_A(x1,x2) = 5 U22#_A(x1,x2) = 5 U61#_A(x1,x2,x3) = 218 isNat_A(x1) = 226 U62#_A(x1,x2,x3) = 218 U63#_A(x1,x2,x3) = 218 U64#_A(x1,x2,x3) = 218 |0|_A = 0 U51#_A(x1,x2) = max{216, x1 - 35, x2 + 2} U52#_A(x1,x2) = 0 U13#_A(x1,x2,x3) = 8 U14#_A(x1,x2,x3) = 7 U15#_A(x1,x2) = 220 U16_A(x1) = 1 U15_A(x1,x2) = 1 U64_A(x1,x2,x3) = x2 + 432 plus_A(x1,x2) = 405 U14_A(x1,x2,x3) = 207 U63_A(x1,x2,x3) = max{x2 + 639, x3 + 18} U13_A(x1,x2,x3) = 208 U23_A(x1) = 39 U52_A(x1,x2) = x1 + 345 U62_A(x1,x2,x3) = max{x1 + 181, x2 + 205, x3 + 225} U12_A(x1,x2,x3) = 209 U22_A(x1,x2) = 39 U32_A(x1) = 261 U51_A(x1,x2) = max{x1 + 567, x2 + 606} U61_A(x1,x2,x3) = 218 U11_A(x1,x2,x3) = max{225, x2 + 1} U21_A(x1,x2) = 248 U31_A(x1,x2) = 261 U41_A(x1) = 5 n__0_A = 1 precedence: U12# > U14 > U15# > U52# > isNat# = U21# = U22# > U11# = U31# = U13 > n__plus > U15 > s = |0| = U21 > U22 > U13# > U14# > U63 > plus > U51 > U16 > isNatKind = U12 = U31 > n__s > U11 > isNat > plus# = U61# = U62# = U63# = U64# > U32 > U51# > activate = U52 > U61 > U41 > tt = isNatKind# = U62 = n__0 > activate# > U64 = U23 partial status: pi(U11#) = [2] 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) = [1] pi(U62) = [2] pi(U12) = [] pi(U22) = [] pi(U32) = [] pi(U51) = [] pi(U61) = [] pi(U11) = [2] pi(U21) = [] pi(U31) = [] pi(U41) = [] pi(n__0) = [] The next rules are strictly ordered: p1, p3, p4, p5, p6, p7, p11, p12, p13, p16, p17, p19, p21, p22, p23, p24, p25, p26, p27, p29, p31, p33, p34, p35, p37, p38, p39, p41, p42, p45, p46, p49, p50, p51, p53, p54, p55, 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: U12#(tt(),V1,V2) -> activate#(V1) p2: isNatKind#(n__s(V1)) -> isNatKind#(activate(V1)) p3: isNatKind#(n__plus(V1,V2)) -> activate#(V2) p4: isNatKind#(n__plus(V1,V2)) -> activate#(V1) p5: U31#(tt(),V2) -> isNatKind#(activate(V2)) p6: isNat#(n__s(V1)) -> U21#(isNatKind(activate(V1)),activate(V1)) p7: U21#(tt(),V1) -> U22#(isNatKind(activate(V1)),activate(V1)) p8: U22#(tt(),V1) -> isNat#(activate(V1)) p9: plus#(N,s(M)) -> U61#(isNat(M),M,N) p10: U61#(tt(),M,N) -> activate#(M) p11: U61#(tt(),M,N) -> U62#(isNatKind(activate(M)),activate(M),activate(N)) p12: U62#(tt(),M,N) -> U63#(isNat(activate(N)),activate(M),activate(N)) p13: U63#(tt(),M,N) -> U64#(isNatKind(activate(N)),activate(M),activate(N)) p14: U64#(tt(),M,N) -> plus#(activate(N),activate(M)) p15: plus#(N,|0|()) -> isNat#(N) p16: U51#(tt(),N) -> isNatKind#(activate(N)) p17: U51#(tt(),N) -> U52#(isNatKind(activate(N)),activate(N)) p18: U12#(tt(),V1,V2) -> U13#(isNatKind(activate(V2)),activate(V1),activate(V2)) p19: 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: {p2} {p9, p11, p12, p13, p14} {p6, p7, p8} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: isNatKind#(n__s(V1)) -> 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: lexicographic combination of reduction pairs: 1. weighted path order base order: matrix interpretations: carrier: N^2 order: standard order interpretations: isNatKind#_A(x1) = ((0,1),(0,0)) x1 + (2,1) n__s_A(x1) = ((0,0),(0,1)) x1 + (51,1) activate_A(x1) = x1 + (2,0) U16_A(x1) = x1 + (23,0) tt_A() = (79,2) U15_A(x1,x2) = x1 + ((1,0),(0,0)) x2 + (2,0) isNat_A(x1) = ((1,0),(0,0)) x1 + (55,2) U14_A(x1,x2,x3) = ((1,0),(0,0)) x2 + ((1,0),(0,0)) x3 + (62,2) U13_A(x1,x2,x3) = ((1,0),(0,0)) x2 + ((1,0),(0,0)) x3 + (67,2) isNatKind_A(x1) = ((1,1),(0,0)) x1 + (69,2) U23_A(x1) = (80,2) U32_A(x1) = (80,2) U64_A(x1,x2,x3) = ((1,0),(0,0)) x1 + ((0,0),(0,1)) x2 + ((0,0),(0,1)) x3 + (1,4) s_A(x1) = ((0,0),(0,1)) x1 + (52,1) plus_A(x1,x2) = ((1,1),(0,1)) x1 + x2 + (28,3) U12_A(x1,x2,x3) = ((0,0),(0,1)) x1 + ((1,0),(0,0)) x2 + ((1,0),(0,0)) x3 + (72,0) U22_A(x1,x2) = (81,2) U31_A(x1,x2) = ((1,0),(0,0)) x1 + (2,2) U41_A(x1) = (80,2) U63_A(x1,x2,x3) = ((0,0),(0,1)) x2 + ((1,1),(0,1)) x3 + (73,4) U11_A(x1,x2,x3) = ((1,1),(0,0)) x2 + ((1,0),(0,0)) x3 + (77,2) U21_A(x1,x2) = (82,2) U52_A(x1,x2) = x2 + (3,1) U62_A(x1,x2,x3) = ((0,0),(0,1)) x1 + ((0,0),(0,1)) x2 + ((1,1),(0,1)) x3 + (76,2) n__0_A() = (24,2) n__plus_A(x1,x2) = ((1,1),(0,1)) x1 + x2 + (27,3) U51_A(x1,x2) = x2 + (27,1) U61_A(x1,x2,x3) = ((0,0),(0,1)) x1 + ((0,0),(0,1)) x2 + ((1,1),(0,1)) x3 + (79,2) |0|_A() = (26,2) precedence: isNatKind# = n__s = activate = U16 = tt = U15 = isNat = U14 = U13 = isNatKind = U23 = U32 = U64 = s = plus = U12 = U22 = U31 = U41 = U63 = U11 = U21 = U52 = U62 = n__0 = n__plus = U51 = U61 = |0| partial status: pi(isNatKind#) = [] pi(n__s) = [] 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) = [] pi(U22) = [] pi(U31) = [] pi(U41) = [] pi(U63) = [] pi(U11) = [] pi(U21) = [] pi(U52) = [] pi(U62) = [] pi(n__0) = [] pi(n__plus) = [] pi(U51) = [] pi(U61) = [] pi(|0|) = [] 2. weighted path order base order: matrix interpretations: carrier: N^2 order: standard order interpretations: isNatKind#_A(x1) = (0,15) n__s_A(x1) = (2,14) activate_A(x1) = ((1,1),(1,1)) x1 + (3,4) U16_A(x1) = ((1,1),(0,1)) x1 + (1,0) tt_A() = (17,1) U15_A(x1,x2) = ((0,1),(0,0)) x2 + (32,2) isNat_A(x1) = ((0,1),(1,1)) x1 + (17,2) U14_A(x1,x2,x3) = (1,2) U13_A(x1,x2,x3) = ((0,0),(0,1)) x3 + (2,2) isNatKind_A(x1) = ((1,1),(0,0)) x1 + (1,3) U23_A(x1) = (21,1) U32_A(x1) = (16,0) U64_A(x1,x2,x3) = ((1,1),(1,1)) x1 + (8,0) s_A(x1) = (18,19) plus_A(x1,x2) = ((1,0),(1,1)) x2 + (9,5) U12_A(x1,x2,x3) = ((1,1),(0,1)) x2 + ((0,0),(1,1)) x3 + (9,6) U22_A(x1,x2) = (21,1) U31_A(x1,x2) = ((1,0),(0,0)) x1 + (1,2) U41_A(x1) = (3,3) U63_A(x1,x2,x3) = (18,10) U11_A(x1,x2,x3) = (0,0) U21_A(x1,x2) = (21,15) U52_A(x1,x2) = x2 + (15,0) U62_A(x1,x2,x3) = ((0,0),(0,1)) x3 + (22,38) n__0_A() = (15,1) n__plus_A(x1,x2) = ((1,1),(1,1)) x1 + ((1,1),(1,1)) x2 + (8,4) U51_A(x1,x2) = ((1,1),(1,1)) x2 + (25,4) U61_A(x1,x2,x3) = ((0,1),(1,1)) x3 + (23,42) |0|_A() = (15,1) precedence: isNat = U21 > U11 > activate = |0| > n__0 > isNatKind > n__plus > plus > U61 > U51 > U52 > U62 > U63 > U64 > s > U12 > U31 > U16 = U41 > tt > U22 > U23 > U14 > isNatKind# = n__s = U15 = U13 = U32 partial status: pi(isNatKind#) = [] pi(n__s) = [] pi(activate) = [] pi(U16) = [1] pi(tt) = [] pi(U15) = [] pi(isNat) = [] pi(U14) = [] pi(U13) = [] pi(isNatKind) = [] pi(U23) = [] pi(U32) = [] pi(U64) = [1] pi(s) = [] pi(plus) = [2] pi(U12) = [] pi(U22) = [] pi(U31) = [] pi(U41) = [] pi(U63) = [] pi(U11) = [] pi(U21) = [] pi(U52) = [] pi(U62) = [] pi(n__0) = [] pi(n__plus) = [] pi(U51) = [] pi(U61) = [] pi(|0|) = [] The next rules are strictly ordered: p1 We remove them from the problem. Then no dependency pair remains. -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: 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: lexicographic combination of reduction pairs: 1. weighted path order base order: matrix interpretations: carrier: N^2 order: standard order interpretations: U64#_A(x1,x2,x3) = x2 tt_A() = (2,0) plus#_A(x1,x2) = x2 activate_A(x1) = x1 s_A(x1) = x1 + (0,22) U61#_A(x1,x2,x3) = x2 isNat_A(x1) = ((0,1),(1,1)) x1 + (0,23) U62#_A(x1,x2,x3) = x2 isNatKind_A(x1) = (10,0) U63#_A(x1,x2,x3) = x2 U16_A(x1) = (3,0) U15_A(x1,x2) = (4,0) U64_A(x1,x2,x3) = ((1,0),(0,0)) x1 + ((1,1),(1,1)) x2 + ((1,0),(1,1)) x3 + (5,31) plus_A(x1,x2) = ((1,0),(1,1)) x1 + ((1,1),(1,1)) x2 + (7,9) U14_A(x1,x2,x3) = (5,0) U63_A(x1,x2,x3) = ((1,1),(1,1)) x2 + ((1,0),(1,1)) x3 + (15,31) U13_A(x1,x2,x3) = ((0,1),(0,0)) x3 + (6,0) U23_A(x1) = (3,1) U52_A(x1,x2) = x1 + x2 + (1,14) U62_A(x1,x2,x3) = ((0,0),(0,1)) x1 + ((1,1),(1,1)) x2 + ((1,0),(1,1)) x3 + (15,31) U12_A(x1,x2,x3) = ((1,0),(0,0)) x2 + ((1,1),(0,1)) x3 + (7,1) U22_A(x1,x2) = ((1,0),(0,0)) x1 + (2,1) U32_A(x1) = ((0,0),(0,1)) x1 + (3,0) U51_A(x1,x2) = x2 + (12,14) U61_A(x1,x2,x3) = ((1,1),(1,1)) x2 + ((1,0),(1,1)) x3 + (15,31) U11_A(x1,x2,x3) = ((0,1),(1,0)) x1 + ((1,0),(0,0)) x2 + ((1,1),(0,1)) x3 + (8,0) U21_A(x1,x2) = ((1,0),(0,0)) x1 + ((0,1),(1,0)) x2 + (11,1) U31_A(x1,x2) = (4,0) U41_A(x1) = (3,0) |0|_A() = (1,13) n__0_A() = (1,13) n__plus_A(x1,x2) = ((1,0),(1,1)) x1 + ((1,1),(1,1)) x2 + (7,9) n__s_A(x1) = x1 + (0,22) precedence: isNatKind > U31 = U41 > U32 > U23 > tt > U61 > U63 = U62 > U64 > s = U61# = n__s > U62# > U63# > U64# > activate = |0| = n__0 > plus = n__plus > isNat > U13 = U21 > U14 > U51 > U11 > U22 > plus# > U15 > U16 > U12 > U52 partial status: pi(U64#) = [2] pi(tt) = [] pi(plus#) = [2] pi(activate) = [1] pi(s) = [1] pi(U61#) = [2] pi(isNat) = [] pi(U62#) = [2] pi(isNatKind) = [] pi(U63#) = [2] pi(U16) = [] pi(U15) = [] pi(U64) = [3] pi(plus) = [2] pi(U14) = [] pi(U63) = [] pi(U13) = [] pi(U23) = [] pi(U52) = [1] pi(U62) = [] pi(U12) = [3] pi(U22) = [] pi(U32) = [] pi(U51) = [] pi(U61) = [3] pi(U11) = [] pi(U21) = [] pi(U31) = [] pi(U41) = [] pi(|0|) = [] pi(n__0) = [] pi(n__plus) = [] pi(n__s) = [1] 2. weighted path order base order: matrix interpretations: carrier: N^2 order: standard order interpretations: U64#_A(x1,x2,x3) = (3,2) tt_A() = (2,1) plus#_A(x1,x2) = ((1,1),(1,1)) x2 + (4,3) activate_A(x1) = (0,0) s_A(x1) = ((1,1),(0,1)) x1 + (2,7) U61#_A(x1,x2,x3) = ((1,1),(0,1)) x2 + (0,1) isNat_A(x1) = (20,10) U62#_A(x1,x2,x3) = (0,0) isNatKind_A(x1) = (7,3) U63#_A(x1,x2,x3) = x2 + (1,1) U16_A(x1) = (3,0) U15_A(x1,x2) = (4,0) U64_A(x1,x2,x3) = (17,9) plus_A(x1,x2) = ((0,1),(0,1)) x2 + (12,2) U14_A(x1,x2,x3) = (4,0) U63_A(x1,x2,x3) = (17,9) U13_A(x1,x2,x3) = (5,1) U23_A(x1) = (3,2) U52_A(x1,x2) = ((1,1),(0,0)) x1 + (1,1) U62_A(x1,x2,x3) = (17,9) U12_A(x1,x2,x3) = ((0,1),(0,0)) x3 + (6,1) U22_A(x1,x2) = (4,2) U32_A(x1) = (2,1) U51_A(x1,x2) = (11,1) U61_A(x1,x2,x3) = (18,9) U11_A(x1,x2,x3) = (19,1) U21_A(x1,x2) = (5,3) U31_A(x1,x2) = (7,3) U41_A(x1) = (7,2) |0|_A() = (0,0) n__0_A() = (0,0) n__plus_A(x1,x2) = (7,2) n__s_A(x1) = (1,1) precedence: U14 = U13 > U51 > U63# > U64# > U61# > isNatKind > U31 > isNat = U15 > activate > plus# = |0| > n__0 > U16 > plus > U61 > U62 > U63 > U11 > n__plus > U32 > U23 > U12 > U21 > U22 > U64 > U41 > tt > s = U62# = U52 = n__s partial status: pi(U64#) = [] pi(tt) = [] pi(plus#) = [2] pi(activate) = [] pi(s) = [1] pi(U61#) = [2] pi(isNat) = [] pi(U62#) = [] pi(isNatKind) = [] pi(U63#) = [2] 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: p1, p2, p3, p4, p5 We remove them from the problem. Then no dependency pair remains. -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: 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: lexicographic combination of reduction pairs: 1. weighted path order base order: matrix interpretations: carrier: N^2 order: standard order interpretations: isNat#_A(x1) = ((1,1),(1,1)) x1 + (1,89) n__s_A(x1) = ((0,1),(1,0)) x1 + (93,0) U21#_A(x1,x2) = ((1,1),(1,1)) x2 + (11,97) isNatKind_A(x1) = ((1,0),(1,1)) x1 + (9,0) activate_A(x1) = x1 + (3,1) tt_A() = (0,92) U22#_A(x1,x2) = ((1,1),(1,1)) x2 + (6,93) U16_A(x1) = ((0,0),(0,1)) x1 U15_A(x1,x2) = (0,118) isNat_A(x1) = ((1,1),(0,0)) x1 + (0,118) U14_A(x1,x2,x3) = ((0,1),(0,0)) x2 + (12,118) U13_A(x1,x2,x3) = ((1,1),(0,0)) x2 + (13,118) U23_A(x1) = (1,93) U64_A(x1,x2,x3) = ((1,1),(1,1)) x2 + ((1,1),(1,1)) x3 + (125,93) s_A(x1) = ((0,1),(1,0)) x1 + (94,1) plus_A(x1,x2) = ((1,1),(1,1)) x1 + ((1,1),(1,1)) x2 + (84,22) U12_A(x1,x2,x3) = ((1,1),(0,0)) x2 + (18,118) U22_A(x1,x2) = (2,93) U63_A(x1,x2,x3) = ((1,1),(1,1)) x2 + ((1,1),(1,1)) x3 + (134,101) U11_A(x1,x2,x3) = ((1,0),(0,0)) x1 + ((1,1),(0,0)) x2 + (67,118) U21_A(x1,x2) = (13,93) U52_A(x1,x2) = x2 + (4,92) U62_A(x1,x2,x3) = ((1,1),(1,1)) x2 + ((1,1),(1,1)) x3 + (143,109) U32_A(x1) = (0,93) U51_A(x1,x2) = x2 + (13,94) U61_A(x1,x2,x3) = ((0,1),(0,0)) x1 + ((1,1),(1,1)) x2 + ((1,1),(1,1)) x3 + (60,117) n__0_A() = (1,92) n__plus_A(x1,x2) = ((1,1),(1,1)) x1 + ((1,1),(1,1)) x2 + (82,21) U31_A(x1,x2) = ((1,0),(0,0)) x1 + x2 + (13,93) U41_A(x1) = (0,93) |0|_A() = (2,93) precedence: isNat# = n__s = U21# = isNatKind = activate = tt = U22# = U16 = U15 = isNat = U14 = U13 = U23 = U64 = s = plus = U12 = U22 = U63 = U11 = U21 = U52 = U62 = U32 = U51 = U61 = n__0 = n__plus = U31 = U41 = |0| partial status: pi(isNat#) = [] pi(n__s) = [] pi(U21#) = [] pi(isNatKind) = [] pi(activate) = [] pi(tt) = [] pi(U22#) = [] pi(U16) = [] pi(U15) = [] pi(isNat) = [] pi(U14) = [] pi(U13) = [] pi(U23) = [] pi(U64) = [] pi(s) = [] pi(plus) = [] pi(U12) = [] pi(U22) = [] pi(U63) = [] pi(U11) = [] pi(U21) = [] pi(U52) = [] pi(U62) = [] pi(U32) = [] pi(U51) = [] pi(U61) = [] pi(n__0) = [] pi(n__plus) = [] pi(U31) = [] pi(U41) = [] pi(|0|) = [] 2. weighted path order base order: matrix interpretations: carrier: N^2 order: standard order interpretations: isNat#_A(x1) = (8,2) n__s_A(x1) = (18,6) U21#_A(x1,x2) = (8,2) isNatKind_A(x1) = ((0,1),(1,1)) x1 + (0,14) activate_A(x1) = ((1,0),(1,0)) x1 + (7,0) tt_A() = (0,1) U22#_A(x1,x2) = (8,2) U16_A(x1) = (1,2) U15_A(x1,x2) = (2,2) isNat_A(x1) = ((0,1),(1,1)) x1 + (18,11) U14_A(x1,x2,x3) = (3,2) U13_A(x1,x2,x3) = (4,2) U23_A(x1) = (1,1) U64_A(x1,x2,x3) = ((0,0),(1,0)) x2 + (23,13) s_A(x1) = (17,2) plus_A(x1,x2) = ((1,0),(1,0)) x1 + ((1,1),(0,1)) x2 + (8,6) U12_A(x1,x2,x3) = (5,2) U22_A(x1,x2) = (6,2) U63_A(x1,x2,x3) = ((0,0),(1,0)) x2 + (24,20) U11_A(x1,x2,x3) = ((0,0),(0,1)) x1 + ((0,0),(0,1)) x2 + (5,1) U21_A(x1,x2) = (19,7) U52_A(x1,x2) = ((1,0),(0,0)) x2 + (7,1) U62_A(x1,x2,x3) = ((1,0),(0,0)) x3 + (8,1) U32_A(x1) = (6,2) U51_A(x1,x2) = ((1,0),(0,0)) x2 + (14,1) U61_A(x1,x2,x3) = ((0,0),(0,1)) x2 + ((1,0),(1,0)) x3 + (16,2) n__0_A() = (0,0) n__plus_A(x1,x2) = ((1,0),(1,0)) x1 + ((1,1),(0,0)) x2 + (6,5) U31_A(x1,x2) = (5,21) U41_A(x1) = (6,1) |0|_A() = (6,0) precedence: n__s > |0| > U32 > isNat > U21 > n__0 > isNat# = U21# > isNatKind > activate = tt > U22# > U14 > U31 > U61 > U23 > U62 > U22 > plus = n__plus > U11 > U12 > s > U13 > U41 > U16 = U15 > U63 > U51 > U52 > U64 partial status: pi(isNat#) = [] pi(n__s) = [] pi(U21#) = [] pi(isNatKind) = [] pi(activate) = [] pi(tt) = [] pi(U22#) = [] 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) = [] pi(n__0) = [] pi(n__plus) = [] pi(U31) = [] pi(U41) = [] pi(|0|) = [] The next rules are strictly ordered: p2, p3 We remove them from the problem. -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: isNat#(n__s(V1)) -> U21#(isNatKind(activate(V1)),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)