YES We show the termination of the TRS R: a__U11(tt(),V1,V2) -> a__U12(a__isNatKind(V1),V1,V2) a__U12(tt(),V1,V2) -> a__U13(a__isNatKind(V2),V1,V2) a__U13(tt(),V1,V2) -> a__U14(a__isNatKind(V2),V1,V2) a__U14(tt(),V1,V2) -> a__U15(a__isNat(V1),V2) a__U15(tt(),V2) -> a__U16(a__isNat(V2)) a__U16(tt()) -> tt() a__U21(tt(),V1) -> a__U22(a__isNatKind(V1),V1) a__U22(tt(),V1) -> a__U23(a__isNat(V1)) a__U23(tt()) -> tt() a__U31(tt(),V2) -> a__U32(a__isNatKind(V2)) a__U32(tt()) -> tt() a__U41(tt()) -> tt() a__U51(tt(),N) -> a__U52(a__isNatKind(N),N) a__U52(tt(),N) -> mark(N) a__U61(tt(),M,N) -> a__U62(a__isNatKind(M),M,N) a__U62(tt(),M,N) -> a__U63(a__isNat(N),M,N) a__U63(tt(),M,N) -> a__U64(a__isNatKind(N),M,N) a__U64(tt(),M,N) -> s(a__plus(mark(N),mark(M))) a__isNat(|0|()) -> tt() a__isNat(plus(V1,V2)) -> a__U11(a__isNatKind(V1),V1,V2) a__isNat(s(V1)) -> a__U21(a__isNatKind(V1),V1) a__isNatKind(|0|()) -> tt() a__isNatKind(plus(V1,V2)) -> a__U31(a__isNatKind(V1),V2) a__isNatKind(s(V1)) -> a__U41(a__isNatKind(V1)) a__plus(N,|0|()) -> a__U51(a__isNat(N),N) a__plus(N,s(M)) -> a__U61(a__isNat(M),M,N) mark(U11(X1,X2,X3)) -> a__U11(mark(X1),X2,X3) mark(U12(X1,X2,X3)) -> a__U12(mark(X1),X2,X3) mark(isNatKind(X)) -> a__isNatKind(X) mark(U13(X1,X2,X3)) -> a__U13(mark(X1),X2,X3) mark(U14(X1,X2,X3)) -> a__U14(mark(X1),X2,X3) mark(U15(X1,X2)) -> a__U15(mark(X1),X2) mark(isNat(X)) -> a__isNat(X) mark(U16(X)) -> a__U16(mark(X)) mark(U21(X1,X2)) -> a__U21(mark(X1),X2) mark(U22(X1,X2)) -> a__U22(mark(X1),X2) mark(U23(X)) -> a__U23(mark(X)) mark(U31(X1,X2)) -> a__U31(mark(X1),X2) mark(U32(X)) -> a__U32(mark(X)) mark(U41(X)) -> a__U41(mark(X)) mark(U51(X1,X2)) -> a__U51(mark(X1),X2) mark(U52(X1,X2)) -> a__U52(mark(X1),X2) mark(U61(X1,X2,X3)) -> a__U61(mark(X1),X2,X3) mark(U62(X1,X2,X3)) -> a__U62(mark(X1),X2,X3) mark(U63(X1,X2,X3)) -> a__U63(mark(X1),X2,X3) mark(U64(X1,X2,X3)) -> a__U64(mark(X1),X2,X3) mark(plus(X1,X2)) -> a__plus(mark(X1),mark(X2)) mark(tt()) -> tt() mark(s(X)) -> s(mark(X)) mark(|0|()) -> |0|() a__U11(X1,X2,X3) -> U11(X1,X2,X3) a__U12(X1,X2,X3) -> U12(X1,X2,X3) a__isNatKind(X) -> isNatKind(X) a__U13(X1,X2,X3) -> U13(X1,X2,X3) a__U14(X1,X2,X3) -> U14(X1,X2,X3) a__U15(X1,X2) -> U15(X1,X2) a__isNat(X) -> isNat(X) a__U16(X) -> U16(X) a__U21(X1,X2) -> U21(X1,X2) a__U22(X1,X2) -> U22(X1,X2) a__U23(X) -> U23(X) a__U31(X1,X2) -> U31(X1,X2) a__U32(X) -> U32(X) a__U41(X) -> U41(X) a__U51(X1,X2) -> U51(X1,X2) a__U52(X1,X2) -> U52(X1,X2) a__U61(X1,X2,X3) -> U61(X1,X2,X3) a__U62(X1,X2,X3) -> U62(X1,X2,X3) a__U63(X1,X2,X3) -> U63(X1,X2,X3) a__U64(X1,X2,X3) -> U64(X1,X2,X3) a__plus(X1,X2) -> plus(X1,X2) -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: a__U11#(tt(),V1,V2) -> a__U12#(a__isNatKind(V1),V1,V2) p2: a__U11#(tt(),V1,V2) -> a__isNatKind#(V1) p3: a__U12#(tt(),V1,V2) -> a__U13#(a__isNatKind(V2),V1,V2) p4: a__U12#(tt(),V1,V2) -> a__isNatKind#(V2) p5: a__U13#(tt(),V1,V2) -> a__U14#(a__isNatKind(V2),V1,V2) p6: a__U13#(tt(),V1,V2) -> a__isNatKind#(V2) p7: a__U14#(tt(),V1,V2) -> a__U15#(a__isNat(V1),V2) p8: a__U14#(tt(),V1,V2) -> a__isNat#(V1) p9: a__U15#(tt(),V2) -> a__U16#(a__isNat(V2)) p10: a__U15#(tt(),V2) -> a__isNat#(V2) p11: a__U21#(tt(),V1) -> a__U22#(a__isNatKind(V1),V1) p12: a__U21#(tt(),V1) -> a__isNatKind#(V1) p13: a__U22#(tt(),V1) -> a__U23#(a__isNat(V1)) p14: a__U22#(tt(),V1) -> a__isNat#(V1) p15: a__U31#(tt(),V2) -> a__U32#(a__isNatKind(V2)) p16: a__U31#(tt(),V2) -> a__isNatKind#(V2) p17: a__U51#(tt(),N) -> a__U52#(a__isNatKind(N),N) p18: a__U51#(tt(),N) -> a__isNatKind#(N) p19: a__U52#(tt(),N) -> mark#(N) p20: a__U61#(tt(),M,N) -> a__U62#(a__isNatKind(M),M,N) p21: a__U61#(tt(),M,N) -> a__isNatKind#(M) p22: a__U62#(tt(),M,N) -> a__U63#(a__isNat(N),M,N) p23: a__U62#(tt(),M,N) -> a__isNat#(N) p24: a__U63#(tt(),M,N) -> a__U64#(a__isNatKind(N),M,N) p25: a__U63#(tt(),M,N) -> a__isNatKind#(N) p26: a__U64#(tt(),M,N) -> a__plus#(mark(N),mark(M)) p27: a__U64#(tt(),M,N) -> mark#(N) p28: a__U64#(tt(),M,N) -> mark#(M) p29: a__isNat#(plus(V1,V2)) -> a__U11#(a__isNatKind(V1),V1,V2) p30: a__isNat#(plus(V1,V2)) -> a__isNatKind#(V1) p31: a__isNat#(s(V1)) -> a__U21#(a__isNatKind(V1),V1) p32: a__isNat#(s(V1)) -> a__isNatKind#(V1) p33: a__isNatKind#(plus(V1,V2)) -> a__U31#(a__isNatKind(V1),V2) p34: a__isNatKind#(plus(V1,V2)) -> a__isNatKind#(V1) p35: a__isNatKind#(s(V1)) -> a__U41#(a__isNatKind(V1)) p36: a__isNatKind#(s(V1)) -> a__isNatKind#(V1) p37: a__plus#(N,|0|()) -> a__U51#(a__isNat(N),N) p38: a__plus#(N,|0|()) -> a__isNat#(N) p39: a__plus#(N,s(M)) -> a__U61#(a__isNat(M),M,N) p40: a__plus#(N,s(M)) -> a__isNat#(M) p41: mark#(U11(X1,X2,X3)) -> a__U11#(mark(X1),X2,X3) p42: mark#(U11(X1,X2,X3)) -> mark#(X1) p43: mark#(U12(X1,X2,X3)) -> a__U12#(mark(X1),X2,X3) p44: mark#(U12(X1,X2,X3)) -> mark#(X1) p45: mark#(isNatKind(X)) -> a__isNatKind#(X) p46: mark#(U13(X1,X2,X3)) -> a__U13#(mark(X1),X2,X3) p47: mark#(U13(X1,X2,X3)) -> mark#(X1) p48: mark#(U14(X1,X2,X3)) -> a__U14#(mark(X1),X2,X3) p49: mark#(U14(X1,X2,X3)) -> mark#(X1) p50: mark#(U15(X1,X2)) -> a__U15#(mark(X1),X2) p51: mark#(U15(X1,X2)) -> mark#(X1) p52: mark#(isNat(X)) -> a__isNat#(X) p53: mark#(U16(X)) -> a__U16#(mark(X)) p54: mark#(U16(X)) -> mark#(X) p55: mark#(U21(X1,X2)) -> a__U21#(mark(X1),X2) p56: mark#(U21(X1,X2)) -> mark#(X1) p57: mark#(U22(X1,X2)) -> a__U22#(mark(X1),X2) p58: mark#(U22(X1,X2)) -> mark#(X1) p59: mark#(U23(X)) -> a__U23#(mark(X)) p60: mark#(U23(X)) -> mark#(X) p61: mark#(U31(X1,X2)) -> a__U31#(mark(X1),X2) p62: mark#(U31(X1,X2)) -> mark#(X1) p63: mark#(U32(X)) -> a__U32#(mark(X)) p64: mark#(U32(X)) -> mark#(X) p65: mark#(U41(X)) -> a__U41#(mark(X)) p66: mark#(U41(X)) -> mark#(X) p67: mark#(U51(X1,X2)) -> a__U51#(mark(X1),X2) p68: mark#(U51(X1,X2)) -> mark#(X1) p69: mark#(U52(X1,X2)) -> a__U52#(mark(X1),X2) p70: mark#(U52(X1,X2)) -> mark#(X1) p71: mark#(U61(X1,X2,X3)) -> a__U61#(mark(X1),X2,X3) p72: mark#(U61(X1,X2,X3)) -> mark#(X1) p73: mark#(U62(X1,X2,X3)) -> a__U62#(mark(X1),X2,X3) p74: mark#(U62(X1,X2,X3)) -> mark#(X1) p75: mark#(U63(X1,X2,X3)) -> a__U63#(mark(X1),X2,X3) p76: mark#(U63(X1,X2,X3)) -> mark#(X1) p77: mark#(U64(X1,X2,X3)) -> a__U64#(mark(X1),X2,X3) p78: mark#(U64(X1,X2,X3)) -> mark#(X1) p79: mark#(plus(X1,X2)) -> a__plus#(mark(X1),mark(X2)) p80: mark#(plus(X1,X2)) -> mark#(X1) p81: mark#(plus(X1,X2)) -> mark#(X2) p82: mark#(s(X)) -> mark#(X) and R consists of: r1: a__U11(tt(),V1,V2) -> a__U12(a__isNatKind(V1),V1,V2) r2: a__U12(tt(),V1,V2) -> a__U13(a__isNatKind(V2),V1,V2) r3: a__U13(tt(),V1,V2) -> a__U14(a__isNatKind(V2),V1,V2) r4: a__U14(tt(),V1,V2) -> a__U15(a__isNat(V1),V2) r5: a__U15(tt(),V2) -> a__U16(a__isNat(V2)) r6: a__U16(tt()) -> tt() r7: a__U21(tt(),V1) -> a__U22(a__isNatKind(V1),V1) r8: a__U22(tt(),V1) -> a__U23(a__isNat(V1)) r9: a__U23(tt()) -> tt() r10: a__U31(tt(),V2) -> a__U32(a__isNatKind(V2)) r11: a__U32(tt()) -> tt() r12: a__U41(tt()) -> tt() r13: a__U51(tt(),N) -> a__U52(a__isNatKind(N),N) r14: a__U52(tt(),N) -> mark(N) r15: a__U61(tt(),M,N) -> a__U62(a__isNatKind(M),M,N) r16: a__U62(tt(),M,N) -> a__U63(a__isNat(N),M,N) r17: a__U63(tt(),M,N) -> a__U64(a__isNatKind(N),M,N) r18: a__U64(tt(),M,N) -> s(a__plus(mark(N),mark(M))) r19: a__isNat(|0|()) -> tt() r20: a__isNat(plus(V1,V2)) -> a__U11(a__isNatKind(V1),V1,V2) r21: a__isNat(s(V1)) -> a__U21(a__isNatKind(V1),V1) r22: a__isNatKind(|0|()) -> tt() r23: a__isNatKind(plus(V1,V2)) -> a__U31(a__isNatKind(V1),V2) r24: a__isNatKind(s(V1)) -> a__U41(a__isNatKind(V1)) r25: a__plus(N,|0|()) -> a__U51(a__isNat(N),N) r26: a__plus(N,s(M)) -> a__U61(a__isNat(M),M,N) r27: mark(U11(X1,X2,X3)) -> a__U11(mark(X1),X2,X3) r28: mark(U12(X1,X2,X3)) -> a__U12(mark(X1),X2,X3) r29: mark(isNatKind(X)) -> a__isNatKind(X) r30: mark(U13(X1,X2,X3)) -> a__U13(mark(X1),X2,X3) r31: mark(U14(X1,X2,X3)) -> a__U14(mark(X1),X2,X3) r32: mark(U15(X1,X2)) -> a__U15(mark(X1),X2) r33: mark(isNat(X)) -> a__isNat(X) r34: mark(U16(X)) -> a__U16(mark(X)) r35: mark(U21(X1,X2)) -> a__U21(mark(X1),X2) r36: mark(U22(X1,X2)) -> a__U22(mark(X1),X2) r37: mark(U23(X)) -> a__U23(mark(X)) r38: mark(U31(X1,X2)) -> a__U31(mark(X1),X2) r39: mark(U32(X)) -> a__U32(mark(X)) r40: mark(U41(X)) -> a__U41(mark(X)) r41: mark(U51(X1,X2)) -> a__U51(mark(X1),X2) r42: mark(U52(X1,X2)) -> a__U52(mark(X1),X2) r43: mark(U61(X1,X2,X3)) -> a__U61(mark(X1),X2,X3) r44: mark(U62(X1,X2,X3)) -> a__U62(mark(X1),X2,X3) r45: mark(U63(X1,X2,X3)) -> a__U63(mark(X1),X2,X3) r46: mark(U64(X1,X2,X3)) -> a__U64(mark(X1),X2,X3) r47: mark(plus(X1,X2)) -> a__plus(mark(X1),mark(X2)) r48: mark(tt()) -> tt() r49: mark(s(X)) -> s(mark(X)) r50: mark(|0|()) -> |0|() r51: a__U11(X1,X2,X3) -> U11(X1,X2,X3) r52: a__U12(X1,X2,X3) -> U12(X1,X2,X3) r53: a__isNatKind(X) -> isNatKind(X) r54: a__U13(X1,X2,X3) -> U13(X1,X2,X3) r55: a__U14(X1,X2,X3) -> U14(X1,X2,X3) r56: a__U15(X1,X2) -> U15(X1,X2) r57: a__isNat(X) -> isNat(X) r58: a__U16(X) -> U16(X) r59: a__U21(X1,X2) -> U21(X1,X2) r60: a__U22(X1,X2) -> U22(X1,X2) r61: a__U23(X) -> U23(X) r62: a__U31(X1,X2) -> U31(X1,X2) r63: a__U32(X) -> U32(X) r64: a__U41(X) -> U41(X) r65: a__U51(X1,X2) -> U51(X1,X2) r66: a__U52(X1,X2) -> U52(X1,X2) r67: a__U61(X1,X2,X3) -> U61(X1,X2,X3) r68: a__U62(X1,X2,X3) -> U62(X1,X2,X3) r69: a__U63(X1,X2,X3) -> U63(X1,X2,X3) r70: a__U64(X1,X2,X3) -> U64(X1,X2,X3) r71: a__plus(X1,X2) -> plus(X1,X2) The estimated dependency graph contains the following SCCs: {p17, p19, p20, p22, p24, p26, p27, p28, p37, p39, p42, p44, p47, p49, p51, p54, p56, p58, p60, p62, p64, p66, p67, p68, p69, p70, p71, p72, p73, p74, p75, p76, p77, p78, p79, p80, p81, p82} {p1, p3, p5, p7, p8, p10, p11, p14, p29, p31} {p16, p33, p34, p36} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: a__U64#(tt(),M,N) -> mark#(M) p2: mark#(s(X)) -> mark#(X) p3: mark#(plus(X1,X2)) -> mark#(X2) p4: mark#(plus(X1,X2)) -> mark#(X1) p5: mark#(plus(X1,X2)) -> a__plus#(mark(X1),mark(X2)) p6: a__plus#(N,s(M)) -> a__U61#(a__isNat(M),M,N) p7: a__U61#(tt(),M,N) -> a__U62#(a__isNatKind(M),M,N) p8: a__U62#(tt(),M,N) -> a__U63#(a__isNat(N),M,N) p9: a__U63#(tt(),M,N) -> a__U64#(a__isNatKind(N),M,N) p10: a__U64#(tt(),M,N) -> mark#(N) p11: mark#(U64(X1,X2,X3)) -> mark#(X1) p12: mark#(U64(X1,X2,X3)) -> a__U64#(mark(X1),X2,X3) p13: a__U64#(tt(),M,N) -> a__plus#(mark(N),mark(M)) p14: a__plus#(N,|0|()) -> a__U51#(a__isNat(N),N) p15: a__U51#(tt(),N) -> a__U52#(a__isNatKind(N),N) p16: a__U52#(tt(),N) -> mark#(N) p17: mark#(U63(X1,X2,X3)) -> mark#(X1) p18: mark#(U63(X1,X2,X3)) -> a__U63#(mark(X1),X2,X3) p19: mark#(U62(X1,X2,X3)) -> mark#(X1) p20: mark#(U62(X1,X2,X3)) -> a__U62#(mark(X1),X2,X3) p21: mark#(U61(X1,X2,X3)) -> mark#(X1) p22: mark#(U61(X1,X2,X3)) -> a__U61#(mark(X1),X2,X3) p23: mark#(U52(X1,X2)) -> mark#(X1) p24: mark#(U52(X1,X2)) -> a__U52#(mark(X1),X2) p25: mark#(U51(X1,X2)) -> mark#(X1) p26: mark#(U51(X1,X2)) -> a__U51#(mark(X1),X2) p27: mark#(U41(X)) -> mark#(X) p28: mark#(U32(X)) -> mark#(X) p29: mark#(U31(X1,X2)) -> mark#(X1) p30: mark#(U23(X)) -> mark#(X) p31: mark#(U22(X1,X2)) -> mark#(X1) p32: mark#(U21(X1,X2)) -> mark#(X1) p33: mark#(U16(X)) -> mark#(X) p34: mark#(U15(X1,X2)) -> mark#(X1) p35: mark#(U14(X1,X2,X3)) -> mark#(X1) p36: mark#(U13(X1,X2,X3)) -> mark#(X1) p37: mark#(U12(X1,X2,X3)) -> mark#(X1) p38: mark#(U11(X1,X2,X3)) -> mark#(X1) and R consists of: r1: a__U11(tt(),V1,V2) -> a__U12(a__isNatKind(V1),V1,V2) r2: a__U12(tt(),V1,V2) -> a__U13(a__isNatKind(V2),V1,V2) r3: a__U13(tt(),V1,V2) -> a__U14(a__isNatKind(V2),V1,V2) r4: a__U14(tt(),V1,V2) -> a__U15(a__isNat(V1),V2) r5: a__U15(tt(),V2) -> a__U16(a__isNat(V2)) r6: a__U16(tt()) -> tt() r7: a__U21(tt(),V1) -> a__U22(a__isNatKind(V1),V1) r8: a__U22(tt(),V1) -> a__U23(a__isNat(V1)) r9: a__U23(tt()) -> tt() r10: a__U31(tt(),V2) -> a__U32(a__isNatKind(V2)) r11: a__U32(tt()) -> tt() r12: a__U41(tt()) -> tt() r13: a__U51(tt(),N) -> a__U52(a__isNatKind(N),N) r14: a__U52(tt(),N) -> mark(N) r15: a__U61(tt(),M,N) -> a__U62(a__isNatKind(M),M,N) r16: a__U62(tt(),M,N) -> a__U63(a__isNat(N),M,N) r17: a__U63(tt(),M,N) -> a__U64(a__isNatKind(N),M,N) r18: a__U64(tt(),M,N) -> s(a__plus(mark(N),mark(M))) r19: a__isNat(|0|()) -> tt() r20: a__isNat(plus(V1,V2)) -> a__U11(a__isNatKind(V1),V1,V2) r21: a__isNat(s(V1)) -> a__U21(a__isNatKind(V1),V1) r22: a__isNatKind(|0|()) -> tt() r23: a__isNatKind(plus(V1,V2)) -> a__U31(a__isNatKind(V1),V2) r24: a__isNatKind(s(V1)) -> a__U41(a__isNatKind(V1)) r25: a__plus(N,|0|()) -> a__U51(a__isNat(N),N) r26: a__plus(N,s(M)) -> a__U61(a__isNat(M),M,N) r27: mark(U11(X1,X2,X3)) -> a__U11(mark(X1),X2,X3) r28: mark(U12(X1,X2,X3)) -> a__U12(mark(X1),X2,X3) r29: mark(isNatKind(X)) -> a__isNatKind(X) r30: mark(U13(X1,X2,X3)) -> a__U13(mark(X1),X2,X3) r31: mark(U14(X1,X2,X3)) -> a__U14(mark(X1),X2,X3) r32: mark(U15(X1,X2)) -> a__U15(mark(X1),X2) r33: mark(isNat(X)) -> a__isNat(X) r34: mark(U16(X)) -> a__U16(mark(X)) r35: mark(U21(X1,X2)) -> a__U21(mark(X1),X2) r36: mark(U22(X1,X2)) -> a__U22(mark(X1),X2) r37: mark(U23(X)) -> a__U23(mark(X)) r38: mark(U31(X1,X2)) -> a__U31(mark(X1),X2) r39: mark(U32(X)) -> a__U32(mark(X)) r40: mark(U41(X)) -> a__U41(mark(X)) r41: mark(U51(X1,X2)) -> a__U51(mark(X1),X2) r42: mark(U52(X1,X2)) -> a__U52(mark(X1),X2) r43: mark(U61(X1,X2,X3)) -> a__U61(mark(X1),X2,X3) r44: mark(U62(X1,X2,X3)) -> a__U62(mark(X1),X2,X3) r45: mark(U63(X1,X2,X3)) -> a__U63(mark(X1),X2,X3) r46: mark(U64(X1,X2,X3)) -> a__U64(mark(X1),X2,X3) r47: mark(plus(X1,X2)) -> a__plus(mark(X1),mark(X2)) r48: mark(tt()) -> tt() r49: mark(s(X)) -> s(mark(X)) r50: mark(|0|()) -> |0|() r51: a__U11(X1,X2,X3) -> U11(X1,X2,X3) r52: a__U12(X1,X2,X3) -> U12(X1,X2,X3) r53: a__isNatKind(X) -> isNatKind(X) r54: a__U13(X1,X2,X3) -> U13(X1,X2,X3) r55: a__U14(X1,X2,X3) -> U14(X1,X2,X3) r56: a__U15(X1,X2) -> U15(X1,X2) r57: a__isNat(X) -> isNat(X) r58: a__U16(X) -> U16(X) r59: a__U21(X1,X2) -> U21(X1,X2) r60: a__U22(X1,X2) -> U22(X1,X2) r61: a__U23(X) -> U23(X) r62: a__U31(X1,X2) -> U31(X1,X2) r63: a__U32(X) -> U32(X) r64: a__U41(X) -> U41(X) r65: a__U51(X1,X2) -> U51(X1,X2) r66: a__U52(X1,X2) -> U52(X1,X2) r67: a__U61(X1,X2,X3) -> U61(X1,X2,X3) r68: a__U62(X1,X2,X3) -> U62(X1,X2,X3) r69: a__U63(X1,X2,X3) -> U63(X1,X2,X3) r70: a__U64(X1,X2,X3) -> U64(X1,X2,X3) r71: a__plus(X1,X2) -> plus(X1,X2) The set of usable rules consists of r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r12, r13, r14, r15, r16, r17, r18, r19, r20, r21, r22, r23, r24, r25, r26, r27, r28, r29, r30, r31, r32, r33, r34, r35, r36, r37, r38, r39, r40, r41, r42, r43, r44, r45, r46, r47, r48, r49, r50, r51, r52, r53, r54, r55, r56, r57, r58, r59, r60, r61, r62, r63, r64, r65, r66, r67, r68, r69, r70, r71 Take the reduction pair: lexicographic combination of reduction pairs: 1. matrix interpretations: carrier: N^1 order: standard order interpretations: a__U64#_A(x1,x2,x3) = x2 + x3 + 4 tt_A() = 0 mark#_A(x1) = x1 s_A(x1) = x1 + 5 plus_A(x1,x2) = x1 + x2 + 4 a__plus#_A(x1,x2) = x1 + x2 + 3 mark_A(x1) = x1 a__U61#_A(x1,x2,x3) = x2 + x3 + 7 a__isNat_A(x1) = 0 a__U62#_A(x1,x2,x3) = x2 + x3 + 6 a__isNatKind_A(x1) = 0 a__U63#_A(x1,x2,x3) = x2 + x3 + 5 U64_A(x1,x2,x3) = x1 + x2 + x3 + 9 |0|_A() = 0 a__U51#_A(x1,x2) = x2 + 2 a__U52#_A(x1,x2) = x2 + 1 U63_A(x1,x2,x3) = x1 + x2 + x3 + 9 U62_A(x1,x2,x3) = x1 + x2 + x3 + 9 U61_A(x1,x2,x3) = x1 + x2 + x3 + 9 U52_A(x1,x2) = x1 + x2 + 2 U51_A(x1,x2) = x1 + x2 + 3 U41_A(x1) = x1 U32_A(x1) = x1 U31_A(x1,x2) = x1 U23_A(x1) = x1 U22_A(x1,x2) = x1 U21_A(x1,x2) = x1 U16_A(x1) = x1 U15_A(x1,x2) = x1 U14_A(x1,x2,x3) = x1 U13_A(x1,x2,x3) = x1 U12_A(x1,x2,x3) = x1 U11_A(x1,x2,x3) = x1 a__U11_A(x1,x2,x3) = x1 a__U12_A(x1,x2,x3) = x1 a__U13_A(x1,x2,x3) = x1 a__U14_A(x1,x2,x3) = x1 a__U15_A(x1,x2) = x1 a__U16_A(x1) = x1 a__U21_A(x1,x2) = x1 a__U22_A(x1,x2) = x1 a__U23_A(x1) = x1 a__U31_A(x1,x2) = x1 a__U32_A(x1) = x1 a__U41_A(x1) = x1 a__U51_A(x1,x2) = x1 + x2 + 3 a__U52_A(x1,x2) = x1 + x2 + 2 a__U61_A(x1,x2,x3) = x1 + x2 + x3 + 9 a__U62_A(x1,x2,x3) = x1 + x2 + x3 + 9 a__U63_A(x1,x2,x3) = x1 + x2 + x3 + 9 a__U64_A(x1,x2,x3) = x1 + x2 + x3 + 9 a__plus_A(x1,x2) = x1 + x2 + 4 isNatKind_A(x1) = 0 isNat_A(x1) = 0 2. lexicographic path order with precedence: precedence: mark > U51 > a__plus > a__isNat > a__U11 > a__U12 > a__U13 > a__U14 > a__U15 > a__U21 > isNat > plus > a__isNatKind > a__U22 > isNatKind > U61 > a__U61 > U22 > U11 > mark# > U14 > a__U31 > a__U32 > U32 > a__U23 > a__U16 > tt > U12 > U13 > U16 > U21 > U23 > a__U51 > a__U62 > a__U63 > a__U64 > s > a__U52 > a__U41 > U15 > U31 > U41 > a__U52# > U52 > a__U61# > a__U62# > U62 > a__U63# > U63 > a__U64# > U64 > a__plus# > a__U51# > |0| argument filter: pi(a__U64#) = [] pi(tt) = [] pi(mark#) = [] pi(s) = [] pi(plus) = [2] pi(a__plus#) = 1 pi(mark) = [1] pi(a__U61#) = 2 pi(a__isNat) = [] pi(a__U62#) = 3 pi(a__isNatKind) = [] pi(a__U63#) = [2, 3] pi(U64) = [] pi(|0|) = [] pi(a__U51#) = [] pi(a__U52#) = [] pi(U63) = [] pi(U62) = [] pi(U61) = 1 pi(U52) = 2 pi(U51) = 1 pi(U41) = 1 pi(U32) = [] pi(U31) = [] pi(U23) = [] pi(U22) = [] pi(U21) = [] pi(U16) = [] pi(U15) = [] pi(U14) = [] pi(U13) = [] pi(U12) = [] pi(U11) = [] pi(a__U11) = [] pi(a__U12) = [] pi(a__U13) = [] pi(a__U14) = [] pi(a__U15) = [] pi(a__U16) = [] pi(a__U21) = [] pi(a__U22) = [] pi(a__U23) = [] pi(a__U31) = [] pi(a__U32) = [] pi(a__U41) = 1 pi(a__U51) = 1 pi(a__U52) = 2 pi(a__U61) = 1 pi(a__U62) = [] pi(a__U63) = [] pi(a__U64) = [] pi(a__plus) = [2] pi(isNatKind) = [] pi(isNat) = [] The next rules are strictly ordered: 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 We remove them from the problem. -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: mark#(U41(X)) -> mark#(X) p2: mark#(U32(X)) -> mark#(X) p3: mark#(U31(X1,X2)) -> mark#(X1) p4: mark#(U23(X)) -> mark#(X) p5: mark#(U22(X1,X2)) -> mark#(X1) p6: mark#(U21(X1,X2)) -> mark#(X1) p7: mark#(U16(X)) -> mark#(X) p8: mark#(U15(X1,X2)) -> mark#(X1) p9: mark#(U14(X1,X2,X3)) -> mark#(X1) p10: mark#(U13(X1,X2,X3)) -> mark#(X1) p11: mark#(U12(X1,X2,X3)) -> mark#(X1) p12: mark#(U11(X1,X2,X3)) -> mark#(X1) and R consists of: r1: a__U11(tt(),V1,V2) -> a__U12(a__isNatKind(V1),V1,V2) r2: a__U12(tt(),V1,V2) -> a__U13(a__isNatKind(V2),V1,V2) r3: a__U13(tt(),V1,V2) -> a__U14(a__isNatKind(V2),V1,V2) r4: a__U14(tt(),V1,V2) -> a__U15(a__isNat(V1),V2) r5: a__U15(tt(),V2) -> a__U16(a__isNat(V2)) r6: a__U16(tt()) -> tt() r7: a__U21(tt(),V1) -> a__U22(a__isNatKind(V1),V1) r8: a__U22(tt(),V1) -> a__U23(a__isNat(V1)) r9: a__U23(tt()) -> tt() r10: a__U31(tt(),V2) -> a__U32(a__isNatKind(V2)) r11: a__U32(tt()) -> tt() r12: a__U41(tt()) -> tt() r13: a__U51(tt(),N) -> a__U52(a__isNatKind(N),N) r14: a__U52(tt(),N) -> mark(N) r15: a__U61(tt(),M,N) -> a__U62(a__isNatKind(M),M,N) r16: a__U62(tt(),M,N) -> a__U63(a__isNat(N),M,N) r17: a__U63(tt(),M,N) -> a__U64(a__isNatKind(N),M,N) r18: a__U64(tt(),M,N) -> s(a__plus(mark(N),mark(M))) r19: a__isNat(|0|()) -> tt() r20: a__isNat(plus(V1,V2)) -> a__U11(a__isNatKind(V1),V1,V2) r21: a__isNat(s(V1)) -> a__U21(a__isNatKind(V1),V1) r22: a__isNatKind(|0|()) -> tt() r23: a__isNatKind(plus(V1,V2)) -> a__U31(a__isNatKind(V1),V2) r24: a__isNatKind(s(V1)) -> a__U41(a__isNatKind(V1)) r25: a__plus(N,|0|()) -> a__U51(a__isNat(N),N) r26: a__plus(N,s(M)) -> a__U61(a__isNat(M),M,N) r27: mark(U11(X1,X2,X3)) -> a__U11(mark(X1),X2,X3) r28: mark(U12(X1,X2,X3)) -> a__U12(mark(X1),X2,X3) r29: mark(isNatKind(X)) -> a__isNatKind(X) r30: mark(U13(X1,X2,X3)) -> a__U13(mark(X1),X2,X3) r31: mark(U14(X1,X2,X3)) -> a__U14(mark(X1),X2,X3) r32: mark(U15(X1,X2)) -> a__U15(mark(X1),X2) r33: mark(isNat(X)) -> a__isNat(X) r34: mark(U16(X)) -> a__U16(mark(X)) r35: mark(U21(X1,X2)) -> a__U21(mark(X1),X2) r36: mark(U22(X1,X2)) -> a__U22(mark(X1),X2) r37: mark(U23(X)) -> a__U23(mark(X)) r38: mark(U31(X1,X2)) -> a__U31(mark(X1),X2) r39: mark(U32(X)) -> a__U32(mark(X)) r40: mark(U41(X)) -> a__U41(mark(X)) r41: mark(U51(X1,X2)) -> a__U51(mark(X1),X2) r42: mark(U52(X1,X2)) -> a__U52(mark(X1),X2) r43: mark(U61(X1,X2,X3)) -> a__U61(mark(X1),X2,X3) r44: mark(U62(X1,X2,X3)) -> a__U62(mark(X1),X2,X3) r45: mark(U63(X1,X2,X3)) -> a__U63(mark(X1),X2,X3) r46: mark(U64(X1,X2,X3)) -> a__U64(mark(X1),X2,X3) r47: mark(plus(X1,X2)) -> a__plus(mark(X1),mark(X2)) r48: mark(tt()) -> tt() r49: mark(s(X)) -> s(mark(X)) r50: mark(|0|()) -> |0|() r51: a__U11(X1,X2,X3) -> U11(X1,X2,X3) r52: a__U12(X1,X2,X3) -> U12(X1,X2,X3) r53: a__isNatKind(X) -> isNatKind(X) r54: a__U13(X1,X2,X3) -> U13(X1,X2,X3) r55: a__U14(X1,X2,X3) -> U14(X1,X2,X3) r56: a__U15(X1,X2) -> U15(X1,X2) r57: a__isNat(X) -> isNat(X) r58: a__U16(X) -> U16(X) r59: a__U21(X1,X2) -> U21(X1,X2) r60: a__U22(X1,X2) -> U22(X1,X2) r61: a__U23(X) -> U23(X) r62: a__U31(X1,X2) -> U31(X1,X2) r63: a__U32(X) -> U32(X) r64: a__U41(X) -> U41(X) r65: a__U51(X1,X2) -> U51(X1,X2) r66: a__U52(X1,X2) -> U52(X1,X2) r67: a__U61(X1,X2,X3) -> U61(X1,X2,X3) r68: a__U62(X1,X2,X3) -> U62(X1,X2,X3) r69: a__U63(X1,X2,X3) -> U63(X1,X2,X3) r70: a__U64(X1,X2,X3) -> U64(X1,X2,X3) r71: a__plus(X1,X2) -> plus(X1,X2) The estimated dependency graph contains the following SCCs: {p1, p2, p3, p4, p5, p6, p7, p8, p9, p10, p11, p12} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: mark#(U41(X)) -> mark#(X) p2: mark#(U11(X1,X2,X3)) -> mark#(X1) p3: mark#(U12(X1,X2,X3)) -> mark#(X1) p4: mark#(U13(X1,X2,X3)) -> mark#(X1) p5: mark#(U14(X1,X2,X3)) -> mark#(X1) p6: mark#(U15(X1,X2)) -> mark#(X1) p7: mark#(U16(X)) -> mark#(X) p8: mark#(U21(X1,X2)) -> mark#(X1) p9: mark#(U22(X1,X2)) -> mark#(X1) p10: mark#(U23(X)) -> mark#(X) p11: mark#(U31(X1,X2)) -> mark#(X1) p12: mark#(U32(X)) -> mark#(X) and R consists of: r1: a__U11(tt(),V1,V2) -> a__U12(a__isNatKind(V1),V1,V2) r2: a__U12(tt(),V1,V2) -> a__U13(a__isNatKind(V2),V1,V2) r3: a__U13(tt(),V1,V2) -> a__U14(a__isNatKind(V2),V1,V2) r4: a__U14(tt(),V1,V2) -> a__U15(a__isNat(V1),V2) r5: a__U15(tt(),V2) -> a__U16(a__isNat(V2)) r6: a__U16(tt()) -> tt() r7: a__U21(tt(),V1) -> a__U22(a__isNatKind(V1),V1) r8: a__U22(tt(),V1) -> a__U23(a__isNat(V1)) r9: a__U23(tt()) -> tt() r10: a__U31(tt(),V2) -> a__U32(a__isNatKind(V2)) r11: a__U32(tt()) -> tt() r12: a__U41(tt()) -> tt() r13: a__U51(tt(),N) -> a__U52(a__isNatKind(N),N) r14: a__U52(tt(),N) -> mark(N) r15: a__U61(tt(),M,N) -> a__U62(a__isNatKind(M),M,N) r16: a__U62(tt(),M,N) -> a__U63(a__isNat(N),M,N) r17: a__U63(tt(),M,N) -> a__U64(a__isNatKind(N),M,N) r18: a__U64(tt(),M,N) -> s(a__plus(mark(N),mark(M))) r19: a__isNat(|0|()) -> tt() r20: a__isNat(plus(V1,V2)) -> a__U11(a__isNatKind(V1),V1,V2) r21: a__isNat(s(V1)) -> a__U21(a__isNatKind(V1),V1) r22: a__isNatKind(|0|()) -> tt() r23: a__isNatKind(plus(V1,V2)) -> a__U31(a__isNatKind(V1),V2) r24: a__isNatKind(s(V1)) -> a__U41(a__isNatKind(V1)) r25: a__plus(N,|0|()) -> a__U51(a__isNat(N),N) r26: a__plus(N,s(M)) -> a__U61(a__isNat(M),M,N) r27: mark(U11(X1,X2,X3)) -> a__U11(mark(X1),X2,X3) r28: mark(U12(X1,X2,X3)) -> a__U12(mark(X1),X2,X3) r29: mark(isNatKind(X)) -> a__isNatKind(X) r30: mark(U13(X1,X2,X3)) -> a__U13(mark(X1),X2,X3) r31: mark(U14(X1,X2,X3)) -> a__U14(mark(X1),X2,X3) r32: mark(U15(X1,X2)) -> a__U15(mark(X1),X2) r33: mark(isNat(X)) -> a__isNat(X) r34: mark(U16(X)) -> a__U16(mark(X)) r35: mark(U21(X1,X2)) -> a__U21(mark(X1),X2) r36: mark(U22(X1,X2)) -> a__U22(mark(X1),X2) r37: mark(U23(X)) -> a__U23(mark(X)) r38: mark(U31(X1,X2)) -> a__U31(mark(X1),X2) r39: mark(U32(X)) -> a__U32(mark(X)) r40: mark(U41(X)) -> a__U41(mark(X)) r41: mark(U51(X1,X2)) -> a__U51(mark(X1),X2) r42: mark(U52(X1,X2)) -> a__U52(mark(X1),X2) r43: mark(U61(X1,X2,X3)) -> a__U61(mark(X1),X2,X3) r44: mark(U62(X1,X2,X3)) -> a__U62(mark(X1),X2,X3) r45: mark(U63(X1,X2,X3)) -> a__U63(mark(X1),X2,X3) r46: mark(U64(X1,X2,X3)) -> a__U64(mark(X1),X2,X3) r47: mark(plus(X1,X2)) -> a__plus(mark(X1),mark(X2)) r48: mark(tt()) -> tt() r49: mark(s(X)) -> s(mark(X)) r50: mark(|0|()) -> |0|() r51: a__U11(X1,X2,X3) -> U11(X1,X2,X3) r52: a__U12(X1,X2,X3) -> U12(X1,X2,X3) r53: a__isNatKind(X) -> isNatKind(X) r54: a__U13(X1,X2,X3) -> U13(X1,X2,X3) r55: a__U14(X1,X2,X3) -> U14(X1,X2,X3) r56: a__U15(X1,X2) -> U15(X1,X2) r57: a__isNat(X) -> isNat(X) r58: a__U16(X) -> U16(X) r59: a__U21(X1,X2) -> U21(X1,X2) r60: a__U22(X1,X2) -> U22(X1,X2) r61: a__U23(X) -> U23(X) r62: a__U31(X1,X2) -> U31(X1,X2) r63: a__U32(X) -> U32(X) r64: a__U41(X) -> U41(X) r65: a__U51(X1,X2) -> U51(X1,X2) r66: a__U52(X1,X2) -> U52(X1,X2) r67: a__U61(X1,X2,X3) -> U61(X1,X2,X3) r68: a__U62(X1,X2,X3) -> U62(X1,X2,X3) r69: a__U63(X1,X2,X3) -> U63(X1,X2,X3) r70: a__U64(X1,X2,X3) -> U64(X1,X2,X3) r71: a__plus(X1,X2) -> plus(X1,X2) The set of usable rules consists of (no rules) Take the monotone reduction pair: lexicographic combination of reduction pairs: 1. matrix interpretations: carrier: N^1 order: standard order interpretations: mark#_A(x1) = x1 U41_A(x1) = x1 + 1 U11_A(x1,x2,x3) = x1 + x2 + x3 + 1 U12_A(x1,x2,x3) = x1 + x2 + x3 + 1 U13_A(x1,x2,x3) = x1 + x2 + x3 + 1 U14_A(x1,x2,x3) = x1 + x2 + x3 + 1 U15_A(x1,x2) = x1 + x2 + 1 U16_A(x1) = x1 + 1 U21_A(x1,x2) = x1 + x2 + 1 U22_A(x1,x2) = x1 + x2 + 1 U23_A(x1) = x1 + 1 U31_A(x1,x2) = x1 + x2 + 1 U32_A(x1) = x1 + 1 2. lexicographic path order with precedence: precedence: mark# > U32 > U31 > U23 > U22 > U21 > U16 > U15 > U14 > U13 > U12 > U11 > U41 argument filter: pi(mark#) = 1 pi(U41) = [1] pi(U11) = [1, 2, 3] pi(U12) = [1, 2, 3] pi(U13) = [1, 2, 3] pi(U14) = [1, 2, 3] pi(U15) = [1, 2] pi(U16) = [1] pi(U21) = [1, 2] pi(U22) = [1, 2] pi(U23) = [1] pi(U31) = [1, 2] pi(U32) = [1] The next rules are strictly ordered: p1, p2, p3, p4, p5, p6, p7, p8, p9, p10, p11, p12 r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r12, r13, r14, r15, r16, r17, r18, r19, r20, r21, r22, r23, r24, r25, r26, r27, r28, r29, r30, r31, r32, r33, r34, r35, r36, r37, r38, r39, r40, r41, r42, r43, r44, r45, r46, r47, r48, r49, r50, r51, r52, r53, r54, r55, r56, r57, r58, r59, r60, r61, r62, r63, r64, r65, r66, r67, r68, r69, r70, r71 We remove them from the problem. Then no dependency pair remains. -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: a__U11#(tt(),V1,V2) -> a__U12#(a__isNatKind(V1),V1,V2) p2: a__U12#(tt(),V1,V2) -> a__U13#(a__isNatKind(V2),V1,V2) p3: a__U13#(tt(),V1,V2) -> a__U14#(a__isNatKind(V2),V1,V2) p4: a__U14#(tt(),V1,V2) -> a__isNat#(V1) p5: a__isNat#(s(V1)) -> a__U21#(a__isNatKind(V1),V1) p6: a__U21#(tt(),V1) -> a__U22#(a__isNatKind(V1),V1) p7: a__U22#(tt(),V1) -> a__isNat#(V1) p8: a__isNat#(plus(V1,V2)) -> a__U11#(a__isNatKind(V1),V1,V2) p9: a__U14#(tt(),V1,V2) -> a__U15#(a__isNat(V1),V2) p10: a__U15#(tt(),V2) -> a__isNat#(V2) and R consists of: r1: a__U11(tt(),V1,V2) -> a__U12(a__isNatKind(V1),V1,V2) r2: a__U12(tt(),V1,V2) -> a__U13(a__isNatKind(V2),V1,V2) r3: a__U13(tt(),V1,V2) -> a__U14(a__isNatKind(V2),V1,V2) r4: a__U14(tt(),V1,V2) -> a__U15(a__isNat(V1),V2) r5: a__U15(tt(),V2) -> a__U16(a__isNat(V2)) r6: a__U16(tt()) -> tt() r7: a__U21(tt(),V1) -> a__U22(a__isNatKind(V1),V1) r8: a__U22(tt(),V1) -> a__U23(a__isNat(V1)) r9: a__U23(tt()) -> tt() r10: a__U31(tt(),V2) -> a__U32(a__isNatKind(V2)) r11: a__U32(tt()) -> tt() r12: a__U41(tt()) -> tt() r13: a__U51(tt(),N) -> a__U52(a__isNatKind(N),N) r14: a__U52(tt(),N) -> mark(N) r15: a__U61(tt(),M,N) -> a__U62(a__isNatKind(M),M,N) r16: a__U62(tt(),M,N) -> a__U63(a__isNat(N),M,N) r17: a__U63(tt(),M,N) -> a__U64(a__isNatKind(N),M,N) r18: a__U64(tt(),M,N) -> s(a__plus(mark(N),mark(M))) r19: a__isNat(|0|()) -> tt() r20: a__isNat(plus(V1,V2)) -> a__U11(a__isNatKind(V1),V1,V2) r21: a__isNat(s(V1)) -> a__U21(a__isNatKind(V1),V1) r22: a__isNatKind(|0|()) -> tt() r23: a__isNatKind(plus(V1,V2)) -> a__U31(a__isNatKind(V1),V2) r24: a__isNatKind(s(V1)) -> a__U41(a__isNatKind(V1)) r25: a__plus(N,|0|()) -> a__U51(a__isNat(N),N) r26: a__plus(N,s(M)) -> a__U61(a__isNat(M),M,N) r27: mark(U11(X1,X2,X3)) -> a__U11(mark(X1),X2,X3) r28: mark(U12(X1,X2,X3)) -> a__U12(mark(X1),X2,X3) r29: mark(isNatKind(X)) -> a__isNatKind(X) r30: mark(U13(X1,X2,X3)) -> a__U13(mark(X1),X2,X3) r31: mark(U14(X1,X2,X3)) -> a__U14(mark(X1),X2,X3) r32: mark(U15(X1,X2)) -> a__U15(mark(X1),X2) r33: mark(isNat(X)) -> a__isNat(X) r34: mark(U16(X)) -> a__U16(mark(X)) r35: mark(U21(X1,X2)) -> a__U21(mark(X1),X2) r36: mark(U22(X1,X2)) -> a__U22(mark(X1),X2) r37: mark(U23(X)) -> a__U23(mark(X)) r38: mark(U31(X1,X2)) -> a__U31(mark(X1),X2) r39: mark(U32(X)) -> a__U32(mark(X)) r40: mark(U41(X)) -> a__U41(mark(X)) r41: mark(U51(X1,X2)) -> a__U51(mark(X1),X2) r42: mark(U52(X1,X2)) -> a__U52(mark(X1),X2) r43: mark(U61(X1,X2,X3)) -> a__U61(mark(X1),X2,X3) r44: mark(U62(X1,X2,X3)) -> a__U62(mark(X1),X2,X3) r45: mark(U63(X1,X2,X3)) -> a__U63(mark(X1),X2,X3) r46: mark(U64(X1,X2,X3)) -> a__U64(mark(X1),X2,X3) r47: mark(plus(X1,X2)) -> a__plus(mark(X1),mark(X2)) r48: mark(tt()) -> tt() r49: mark(s(X)) -> s(mark(X)) r50: mark(|0|()) -> |0|() r51: a__U11(X1,X2,X3) -> U11(X1,X2,X3) r52: a__U12(X1,X2,X3) -> U12(X1,X2,X3) r53: a__isNatKind(X) -> isNatKind(X) r54: a__U13(X1,X2,X3) -> U13(X1,X2,X3) r55: a__U14(X1,X2,X3) -> U14(X1,X2,X3) r56: a__U15(X1,X2) -> U15(X1,X2) r57: a__isNat(X) -> isNat(X) r58: a__U16(X) -> U16(X) r59: a__U21(X1,X2) -> U21(X1,X2) r60: a__U22(X1,X2) -> U22(X1,X2) r61: a__U23(X) -> U23(X) r62: a__U31(X1,X2) -> U31(X1,X2) r63: a__U32(X) -> U32(X) r64: a__U41(X) -> U41(X) r65: a__U51(X1,X2) -> U51(X1,X2) r66: a__U52(X1,X2) -> U52(X1,X2) r67: a__U61(X1,X2,X3) -> U61(X1,X2,X3) r68: a__U62(X1,X2,X3) -> U62(X1,X2,X3) r69: a__U63(X1,X2,X3) -> U63(X1,X2,X3) r70: a__U64(X1,X2,X3) -> U64(X1,X2,X3) r71: a__plus(X1,X2) -> plus(X1,X2) The set of usable rules consists of r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r12, r19, r20, r21, r22, r23, r24, r51, r52, r53, r54, r55, r56, r57, r58, r59, r60, r61, r62, r63, r64 Take the reduction pair: lexicographic combination of reduction pairs: 1. matrix interpretations: carrier: N^1 order: standard order interpretations: a__U11#_A(x1,x2,x3) = x2 + x3 + 5 tt_A() = 1 a__U12#_A(x1,x2,x3) = x2 + x3 + 4 a__isNatKind_A(x1) = x1 + 1 a__U13#_A(x1,x2,x3) = x2 + x3 + 3 a__U14#_A(x1,x2,x3) = x2 + x3 + 2 a__isNat#_A(x1) = x1 s_A(x1) = x1 + 4 a__U21#_A(x1,x2) = x2 + 2 a__U22#_A(x1,x2) = x2 + 1 plus_A(x1,x2) = x1 + x2 + 7 a__U15#_A(x1,x2) = x1 + x2 a__isNat_A(x1) = x1 + 1 a__U16_A(x1) = 2 U16_A(x1) = 0 a__U15_A(x1,x2) = 3 U15_A(x1,x2) = 0 a__U14_A(x1,x2,x3) = 4 U14_A(x1,x2,x3) = 3 a__U13_A(x1,x2,x3) = x1 + 4 a__U23_A(x1) = 2 U13_A(x1,x2,x3) = 3 U23_A(x1) = 1 a__U12_A(x1,x2,x3) = x3 + 6 a__U22_A(x1,x2) = 3 a__U32_A(x1) = x1 + 1 U12_A(x1,x2,x3) = 0 U22_A(x1,x2) = 0 U32_A(x1) = 0 a__U11_A(x1,x2,x3) = x1 + x3 + 6 a__U21_A(x1,x2) = x1 + 3 a__U31_A(x1,x2) = x1 + x2 + 2 a__U41_A(x1) = x1 + 1 U11_A(x1,x2,x3) = 0 U21_A(x1,x2) = 2 U31_A(x1,x2) = 1 U41_A(x1) = 0 |0|_A() = 1 isNatKind_A(x1) = 0 isNat_A(x1) = 0 2. lexicographic path order with precedence: precedence: isNat > U31 > U12 > U23 > a__U23 > U15 > a__U15 > U16 > a__isNat# > a__U21# > a__U22# > a__isNatKind > a__U14# > a__U11# > a__U15# > tt > a__U13# > isNatKind > |0| > U41 > U21 > U11 > a__U41 > a__U32 > a__U31 > a__U12 > a__U22 > a__U21 > a__U11 > U32 > U22 > U13 > a__U14 > a__U13 > U14 > a__U16 > a__isNat > plus > s > a__U12# argument filter: pi(a__U11#) = [] pi(tt) = [] pi(a__U12#) = [] pi(a__isNatKind) = 1 pi(a__U13#) = [] pi(a__U14#) = 3 pi(a__isNat#) = [] pi(s) = 1 pi(a__U21#) = [] pi(a__U22#) = [] pi(plus) = [2] pi(a__U15#) = 2 pi(a__isNat) = 1 pi(a__U16) = [] pi(U16) = [] pi(a__U15) = [] pi(U15) = [] pi(a__U14) = [] pi(U14) = [] pi(a__U13) = [] pi(a__U23) = [] pi(U13) = [] pi(U23) = [] pi(a__U12) = [] pi(a__U22) = [] pi(a__U32) = [] pi(U12) = [] pi(U22) = [] pi(U32) = [] pi(a__U11) = 1 pi(a__U21) = [] pi(a__U31) = 1 pi(a__U41) = 1 pi(U11) = [] pi(U21) = [] pi(U31) = [] pi(U41) = [] pi(|0|) = [] pi(isNatKind) = [] pi(isNat) = [] The next rules are strictly ordered: p1, p2, p3, p4, p5, p6, p7, p8, p9, p10 We remove them from the problem. Then no dependency pair remains. -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: a__isNatKind#(plus(V1,V2)) -> a__U31#(a__isNatKind(V1),V2) p2: a__U31#(tt(),V2) -> a__isNatKind#(V2) p3: a__isNatKind#(s(V1)) -> a__isNatKind#(V1) p4: a__isNatKind#(plus(V1,V2)) -> a__isNatKind#(V1) and R consists of: r1: a__U11(tt(),V1,V2) -> a__U12(a__isNatKind(V1),V1,V2) r2: a__U12(tt(),V1,V2) -> a__U13(a__isNatKind(V2),V1,V2) r3: a__U13(tt(),V1,V2) -> a__U14(a__isNatKind(V2),V1,V2) r4: a__U14(tt(),V1,V2) -> a__U15(a__isNat(V1),V2) r5: a__U15(tt(),V2) -> a__U16(a__isNat(V2)) r6: a__U16(tt()) -> tt() r7: a__U21(tt(),V1) -> a__U22(a__isNatKind(V1),V1) r8: a__U22(tt(),V1) -> a__U23(a__isNat(V1)) r9: a__U23(tt()) -> tt() r10: a__U31(tt(),V2) -> a__U32(a__isNatKind(V2)) r11: a__U32(tt()) -> tt() r12: a__U41(tt()) -> tt() r13: a__U51(tt(),N) -> a__U52(a__isNatKind(N),N) r14: a__U52(tt(),N) -> mark(N) r15: a__U61(tt(),M,N) -> a__U62(a__isNatKind(M),M,N) r16: a__U62(tt(),M,N) -> a__U63(a__isNat(N),M,N) r17: a__U63(tt(),M,N) -> a__U64(a__isNatKind(N),M,N) r18: a__U64(tt(),M,N) -> s(a__plus(mark(N),mark(M))) r19: a__isNat(|0|()) -> tt() r20: a__isNat(plus(V1,V2)) -> a__U11(a__isNatKind(V1),V1,V2) r21: a__isNat(s(V1)) -> a__U21(a__isNatKind(V1),V1) r22: a__isNatKind(|0|()) -> tt() r23: a__isNatKind(plus(V1,V2)) -> a__U31(a__isNatKind(V1),V2) r24: a__isNatKind(s(V1)) -> a__U41(a__isNatKind(V1)) r25: a__plus(N,|0|()) -> a__U51(a__isNat(N),N) r26: a__plus(N,s(M)) -> a__U61(a__isNat(M),M,N) r27: mark(U11(X1,X2,X3)) -> a__U11(mark(X1),X2,X3) r28: mark(U12(X1,X2,X3)) -> a__U12(mark(X1),X2,X3) r29: mark(isNatKind(X)) -> a__isNatKind(X) r30: mark(U13(X1,X2,X3)) -> a__U13(mark(X1),X2,X3) r31: mark(U14(X1,X2,X3)) -> a__U14(mark(X1),X2,X3) r32: mark(U15(X1,X2)) -> a__U15(mark(X1),X2) r33: mark(isNat(X)) -> a__isNat(X) r34: mark(U16(X)) -> a__U16(mark(X)) r35: mark(U21(X1,X2)) -> a__U21(mark(X1),X2) r36: mark(U22(X1,X2)) -> a__U22(mark(X1),X2) r37: mark(U23(X)) -> a__U23(mark(X)) r38: mark(U31(X1,X2)) -> a__U31(mark(X1),X2) r39: mark(U32(X)) -> a__U32(mark(X)) r40: mark(U41(X)) -> a__U41(mark(X)) r41: mark(U51(X1,X2)) -> a__U51(mark(X1),X2) r42: mark(U52(X1,X2)) -> a__U52(mark(X1),X2) r43: mark(U61(X1,X2,X3)) -> a__U61(mark(X1),X2,X3) r44: mark(U62(X1,X2,X3)) -> a__U62(mark(X1),X2,X3) r45: mark(U63(X1,X2,X3)) -> a__U63(mark(X1),X2,X3) r46: mark(U64(X1,X2,X3)) -> a__U64(mark(X1),X2,X3) r47: mark(plus(X1,X2)) -> a__plus(mark(X1),mark(X2)) r48: mark(tt()) -> tt() r49: mark(s(X)) -> s(mark(X)) r50: mark(|0|()) -> |0|() r51: a__U11(X1,X2,X3) -> U11(X1,X2,X3) r52: a__U12(X1,X2,X3) -> U12(X1,X2,X3) r53: a__isNatKind(X) -> isNatKind(X) r54: a__U13(X1,X2,X3) -> U13(X1,X2,X3) r55: a__U14(X1,X2,X3) -> U14(X1,X2,X3) r56: a__U15(X1,X2) -> U15(X1,X2) r57: a__isNat(X) -> isNat(X) r58: a__U16(X) -> U16(X) r59: a__U21(X1,X2) -> U21(X1,X2) r60: a__U22(X1,X2) -> U22(X1,X2) r61: a__U23(X) -> U23(X) r62: a__U31(X1,X2) -> U31(X1,X2) r63: a__U32(X) -> U32(X) r64: a__U41(X) -> U41(X) r65: a__U51(X1,X2) -> U51(X1,X2) r66: a__U52(X1,X2) -> U52(X1,X2) r67: a__U61(X1,X2,X3) -> U61(X1,X2,X3) r68: a__U62(X1,X2,X3) -> U62(X1,X2,X3) r69: a__U63(X1,X2,X3) -> U63(X1,X2,X3) r70: a__U64(X1,X2,X3) -> U64(X1,X2,X3) r71: a__plus(X1,X2) -> plus(X1,X2) The set of usable rules consists of r10, r11, r12, r22, r23, r24, r53, r62, r63, r64 Take the reduction pair: lexicographic combination of reduction pairs: 1. matrix interpretations: carrier: N^1 order: standard order interpretations: a__isNatKind#_A(x1) = x1 plus_A(x1,x2) = x1 + x2 + 2 a__U31#_A(x1,x2) = x2 + 1 a__isNatKind_A(x1) = 4 tt_A() = 1 s_A(x1) = x1 + 1 a__U32_A(x1) = 2 U32_A(x1) = 0 a__U31_A(x1,x2) = 3 a__U41_A(x1) = 2 U31_A(x1,x2) = 2 U41_A(x1) = 0 |0|_A() = 1 isNatKind_A(x1) = 0 2. lexicographic path order with precedence: precedence: isNatKind > |0| > a__isNatKind > a__U41 > U41 > a__U31 > U31 > U32 > tt > a__U32 > a__isNatKind# > s > a__U31# > plus argument filter: pi(a__isNatKind#) = [1] pi(plus) = 2 pi(a__U31#) = 2 pi(a__isNatKind) = [] pi(tt) = [] pi(s) = [1] pi(a__U32) = [] pi(U32) = [] pi(a__U31) = [] pi(a__U41) = [] pi(U31) = [] pi(U41) = [] pi(|0|) = [] pi(isNatKind) = [] The next rules are strictly ordered: p1, p2, p3, p4 We remove them from the problem. Then no dependency pair remains.