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. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          a__U64#_A(x1,x2,x3) = max{35, x1 - 15, x2 - 10, x3 - 8}
          tt_A = 37
          mark#_A(x1) = max{34, x1 - 11}
          s_A(x1) = max{262, x1}
          plus_A(x1,x2) = max{312, x1 + 176, x2 + 218}
          a__plus#_A(x1,x2) = max{6, x1 - 8, x2 - 10}
          mark_A(x1) = max{41, x1}
          a__U61#_A(x1,x2,x3) = max{x1 + 92, x2 - 10, x3 - 8}
          a__isNat_A(x1) = max{36, x1 - 102}
          a__U62#_A(x1,x2,x3) = max{0, x1 - 2, x2 - 10, x3 - 8}
          a__isNatKind_A(x1) = max{4, x1 - 219}
          a__U63#_A(x1,x2,x3) = max{35, x2 - 10, x3 - 8}
          U64_A(x1,x2,x3) = max{313, x1 + 221, x2 + 218, x3 + 176}
          |0|_A = 257
          a__U51#_A(x1,x2) = max{x1 + 79, x2 - 9}
          a__U52#_A(x1,x2) = max{x1 + 20, x2 - 10}
          U63_A(x1,x2,x3) = max{318, x1 + 277, x2 + 218, x3 + 176}
          U62_A(x1,x2,x3) = max{319, x1 + 10, x2 + 218, x3 + 176}
          U61_A(x1,x2,x3) = max{362, x1 + 320, x2 + 218, x3 + 176}
          U52_A(x1,x2) = max{x1 + 32, x2 + 74}
          U51_A(x1,x2) = max{x1 + 132, x2 + 175}
          U41_A(x1) = max{42, x1}
          U32_A(x1) = max{88, x1 + 46}
          U31_A(x1,x2) = max{92, x1 + 51, x2 - 1}
          U23_A(x1) = max{7, x1}
          U22_A(x1,x2) = max{x1, x2 - 102}
          U21_A(x1,x2) = max{5, x1, x2 - 102}
          U16_A(x1) = max{54, x1 + 12}
          U15_A(x1,x2) = max{x1 + 18, x2 + 61}
          U14_A(x1,x2,x3) = max{x1 + 12, x2 + 64, x3 + 62}
          U13_A(x1,x2,x3) = max{x1 + 25, x2 + 65, x3 + 68}
          U12_A(x1,x2,x3) = max{x1 + 32, x2 + 74, x3 + 73}
          U11_A(x1,x2,x3) = max{x1 + 33, x2 + 74, x3 + 115}
          a__U11_A(x1,x2,x3) = max{x1 + 33, x2 + 74, x3 + 115}
          a__U12_A(x1,x2,x3) = max{x1 + 32, x2 + 74, x3 + 73}
          a__U13_A(x1,x2,x3) = max{x1 + 25, x2 + 65, x3 + 68}
          a__U14_A(x1,x2,x3) = max{x1 + 12, x2 + 64, x3 + 62}
          a__U15_A(x1,x2) = max{x1 + 18, x2 + 61}
          a__U16_A(x1) = max{54, x1 + 12}
          a__U21_A(x1,x2) = max{5, x1, x2 - 102}
          a__U22_A(x1,x2) = max{6, x1, x2 - 102}
          a__U23_A(x1) = max{7, x1}
          a__U31_A(x1,x2) = max{92, x1 + 51, x2 - 1}
          a__U32_A(x1) = max{88, x1 + 46}
          a__U41_A(x1) = max{42, x1}
          a__U51_A(x1,x2) = max{x1 + 132, x2 + 175}
          a__U52_A(x1,x2) = max{x1 + 32, x2 + 74}
          a__U61_A(x1,x2,x3) = max{362, x1 + 320, x2 + 218, x3 + 176}
          a__U62_A(x1,x2,x3) = max{319, x1 + 10, x2 + 218, x3 + 176}
          a__U63_A(x1,x2,x3) = max{318, x1 + 277, x2 + 218, x3 + 176}
          a__U64_A(x1,x2,x3) = max{313, x1 + 221, x2 + 218, x3 + 176}
          a__plus_A(x1,x2) = max{312, x1 + 176, x2 + 218}
          isNatKind_A(x1) = max{4, x1 - 219}
          isNat_A(x1) = max{36, x1 - 102}
    
      precedence:
      
        a__U64# = plus = a__plus# = a__U61# = a__U62# = a__U63# = a__plus > mark# > a__U51# > a__U52# > a__isNatKind = U52 = a__U52 = isNatKind > a__isNat = isNat > mark = U14 = a__U14 = a__U31 = a__U32 > U61 = a__U61 > a__U62 > a__U63 > U62 = a__U64 > s > a__U21 > a__U22 > a__U23 > |0| = U31 > U41 = a__U41 > tt > U22 = U21 > U32 > U64 > U11 = a__U11 > a__U12 > U12 > a__U51 > U51 = U13 = a__U13 > a__U15 > U15 > U63 > U23 = U16 = a__U16
      
      partial status:
    
        pi(a__U64#) = []
        pi(tt) = []
        pi(mark#) = []
        pi(s) = []
        pi(plus) = []
        pi(a__plus#) = []
        pi(mark) = [1]
        pi(a__U61#) = []
        pi(a__isNat) = []
        pi(a__U62#) = []
        pi(a__isNatKind) = []
        pi(a__U63#) = []
        pi(U64) = []
        pi(|0|) = []
        pi(a__U51#) = []
        pi(a__U52#) = []
        pi(U63) = [1, 2]
        pi(U62) = [2, 3]
        pi(U61) = []
        pi(U52) = [2]
        pi(U51) = [2]
        pi(U41) = []
        pi(U32) = []
        pi(U31) = []
        pi(U23) = []
        pi(U22) = [1]
        pi(U21) = []
        pi(U16) = []
        pi(U15) = []
        pi(U14) = []
        pi(U13) = [1]
        pi(U12) = [1, 2, 3]
        pi(U11) = []
        pi(a__U11) = [2]
        pi(a__U12) = [1, 2, 3]
        pi(a__U13) = [1, 2]
        pi(a__U14) = []
        pi(a__U15) = [2]
        pi(a__U16) = []
        pi(a__U21) = []
        pi(a__U22) = [1]
        pi(a__U23) = []
        pi(a__U31) = []
        pi(a__U32) = []
        pi(a__U41) = []
        pi(a__U51) = [1, 2]
        pi(a__U52) = [2]
        pi(a__U61) = [1, 3]
        pi(a__U62) = [1]
        pi(a__U63) = [1]
        pi(a__U64) = []
        pi(a__plus) = []
        pi(isNatKind) = []
        pi(isNat) = []
    
    2. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          a__U64#_A(x1,x2,x3) = 572
          tt_A = 202
          mark#_A(x1) = 572
          s_A(x1) = 29
          plus_A(x1,x2) = 47
          a__plus#_A(x1,x2) = 572
          mark_A(x1) = 191
          a__U61#_A(x1,x2,x3) = 572
          a__isNat_A(x1) = 191
          a__U62#_A(x1,x2,x3) = 572
          a__isNatKind_A(x1) = 348
          a__U63#_A(x1,x2,x3) = 572
          U64_A(x1,x2,x3) = 16
          |0|_A = 203
          a__U51#_A(x1,x2) = 571
          a__U52#_A(x1,x2) = 571
          U63_A(x1,x2,x3) = x1 + 19
          U62_A(x1,x2,x3) = 0
          U61_A(x1,x2,x3) = 0
          U52_A(x1,x2) = 203
          U51_A(x1,x2) = x2 + 16
          U41_A(x1) = 191
          U32_A(x1) = 190
          U31_A(x1,x2) = 191
          U23_A(x1) = 28
          U22_A(x1,x2) = 15
          U21_A(x1,x2) = 174
          U16_A(x1) = 187
          U15_A(x1,x2) = 186
          U14_A(x1,x2,x3) = 189
          U13_A(x1,x2,x3) = 378
          U12_A(x1,x2,x3) = max{x1 + 192, x2 + 572, x3 + 192}
          U11_A(x1,x2,x3) = 191
          a__U11_A(x1,x2,x3) = 191
          a__U12_A(x1,x2,x3) = 190
          a__U13_A(x1,x2,x3) = x1 + 379
          a__U14_A(x1,x2,x3) = 190
          a__U15_A(x1,x2) = 187
          a__U16_A(x1) = 187
          a__U21_A(x1,x2) = 174
          a__U22_A(x1,x2) = 28
          a__U23_A(x1) = 28
          a__U31_A(x1,x2) = 191
          a__U32_A(x1) = 190
          a__U41_A(x1) = 191
          a__U51_A(x1,x2) = max{x1, x2 + 554}
          a__U52_A(x1,x2) = 203
          a__U61_A(x1,x2,x3) = max{1, x1}
          a__U62_A(x1,x2,x3) = max{30, x1}
          a__U63_A(x1,x2,x3) = max{30, x1 - 172}
          a__U64_A(x1,x2,x3) = 29
          a__plus_A(x1,x2) = 191
          isNatKind_A(x1) = 348
          isNat_A(x1) = 191
    
      precedence:
      
        a__isNatKind > a__U51 = a__U52 > mark > U32 = a__U32 > a__U31 > a__U14 > U31 > a__U41 > plus = a__isNat = U52 = a__plus > tt > a__U21 > isNat > a__U15 > a__U16 > U15 > |0| = U14 = isNatKind > a__U64 > a__U61 > s > U63 = a__U22 > U22 = U21 > U16 = a__U11 > U13 = U11 = a__U12 = a__U13 > a__U64# = mark# = a__plus# = a__U61# = a__U62# = a__U63# = U62 = a__U62 = a__U63 > a__U51# > a__U52# > U12 > a__U23 > U23 > U41 > U64 = U61 = U51
      
      partial status:
    
        pi(a__U64#) = []
        pi(tt) = []
        pi(mark#) = []
        pi(s) = []
        pi(plus) = []
        pi(a__plus#) = []
        pi(mark) = []
        pi(a__U61#) = []
        pi(a__isNat) = []
        pi(a__U62#) = []
        pi(a__isNatKind) = []
        pi(a__U63#) = []
        pi(U64) = []
        pi(|0|) = []
        pi(a__U51#) = []
        pi(a__U52#) = []
        pi(U63) = []
        pi(U62) = []
        pi(U61) = []
        pi(U52) = []
        pi(U51) = [2]
        pi(U41) = []
        pi(U32) = []
        pi(U31) = []
        pi(U23) = []
        pi(U22) = []
        pi(U21) = []
        pi(U16) = []
        pi(U15) = []
        pi(U14) = []
        pi(U13) = []
        pi(U12) = [1]
        pi(U11) = []
        pi(a__U11) = []
        pi(a__U12) = []
        pi(a__U13) = [1]
        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) = []
        pi(a__U51) = [1]
        pi(a__U52) = []
        pi(a__U61) = []
        pi(a__U62) = []
        pi(a__U63) = []
        pi(a__U64) = []
        pi(a__plus) = []
        pi(isNatKind) = []
        pi(isNat) = []
    

The next rules are strictly ordered:

  p1, p10, p15, p16, p24, p26

We remove them from the problem.

-- SCC decomposition.

Consider the dependency pair problem (P, R), where P consists of

p1: mark#(s(X)) -> mark#(X)
p2: mark#(plus(X1,X2)) -> mark#(X2)
p3: mark#(plus(X1,X2)) -> mark#(X1)
p4: mark#(plus(X1,X2)) -> a__plus#(mark(X1),mark(X2))
p5: a__plus#(N,s(M)) -> a__U61#(a__isNat(M),M,N)
p6: a__U61#(tt(),M,N) -> a__U62#(a__isNatKind(M),M,N)
p7: a__U62#(tt(),M,N) -> a__U63#(a__isNat(N),M,N)
p8: a__U63#(tt(),M,N) -> a__U64#(a__isNatKind(N),M,N)
p9: mark#(U64(X1,X2,X3)) -> mark#(X1)
p10: mark#(U64(X1,X2,X3)) -> a__U64#(mark(X1),X2,X3)
p11: a__U64#(tt(),M,N) -> a__plus#(mark(N),mark(M))
p12: a__plus#(N,|0|()) -> a__U51#(a__isNat(N),N)
p13: mark#(U63(X1,X2,X3)) -> mark#(X1)
p14: mark#(U63(X1,X2,X3)) -> a__U63#(mark(X1),X2,X3)
p15: mark#(U62(X1,X2,X3)) -> mark#(X1)
p16: mark#(U62(X1,X2,X3)) -> a__U62#(mark(X1),X2,X3)
p17: mark#(U61(X1,X2,X3)) -> mark#(X1)
p18: mark#(U61(X1,X2,X3)) -> a__U61#(mark(X1),X2,X3)
p19: mark#(U52(X1,X2)) -> mark#(X1)
p20: mark#(U51(X1,X2)) -> mark#(X1)
p21: mark#(U41(X)) -> mark#(X)
p22: mark#(U32(X)) -> mark#(X)
p23: mark#(U31(X1,X2)) -> mark#(X1)
p24: mark#(U23(X)) -> mark#(X)
p25: mark#(U22(X1,X2)) -> mark#(X1)
p26: mark#(U21(X1,X2)) -> mark#(X1)
p27: mark#(U16(X)) -> mark#(X)
p28: mark#(U15(X1,X2)) -> mark#(X1)
p29: mark#(U14(X1,X2,X3)) -> mark#(X1)
p30: mark#(U13(X1,X2,X3)) -> mark#(X1)
p31: mark#(U12(X1,X2,X3)) -> mark#(X1)
p32: 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, p9, p13, p15, p17, p19, p20, p21, p22, p23, p24, p25, p26, p27, p28, p29, p30, p31, p32}
  {p5, p6, p7, p8, p11}


-- Reduction pair.

Consider the dependency pair problem (P, R), where P consists of

p1: mark#(s(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)
p13: mark#(U41(X)) -> mark#(X)
p14: mark#(U51(X1,X2)) -> mark#(X1)
p15: mark#(U52(X1,X2)) -> mark#(X1)
p16: mark#(U61(X1,X2,X3)) -> mark#(X1)
p17: mark#(U62(X1,X2,X3)) -> mark#(X1)
p18: mark#(U63(X1,X2,X3)) -> mark#(X1)
p19: mark#(U64(X1,X2,X3)) -> mark#(X1)
p20: mark#(plus(X1,X2)) -> mark#(X1)
p21: mark#(plus(X1,X2)) -> mark#(X2)

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 reduction pair:

  lexicographic combination of reduction pairs:
  
    1. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          mark#_A(x1) = max{6, x1 + 4}
          s_A(x1) = max{1, x1}
          U11_A(x1,x2,x3) = max{x1, x2, x3}
          U12_A(x1,x2,x3) = max{x1 + 3, x2 + 3, x3 + 3}
          U13_A(x1,x2,x3) = max{x1, x2, x3 + 1}
          U14_A(x1,x2,x3) = max{x1, x2, x3}
          U15_A(x1,x2) = max{x1, x2 + 1}
          U16_A(x1) = max{4, x1 + 3}
          U21_A(x1,x2) = max{x1, x2}
          U22_A(x1,x2) = max{x1, x2}
          U23_A(x1) = max{4, x1 + 3}
          U31_A(x1,x2) = max{x1, x2 + 1}
          U32_A(x1) = max{1, x1}
          U41_A(x1) = max{2, x1 + 1}
          U51_A(x1,x2) = max{x1 + 6, x2 + 6}
          U52_A(x1,x2) = max{x1 + 6, x2 + 6}
          U61_A(x1,x2,x3) = max{x1 + 3, x2 + 3, x3 + 3}
          U62_A(x1,x2,x3) = max{x1, x2 + 1, x3 + 1}
          U63_A(x1,x2,x3) = max{x1 + 2, x2, x3}
          U64_A(x1,x2,x3) = max{x1, x2, x3}
          plus_A(x1,x2) = max{x1 + 3, x2}
    
      precedence:
      
        s = U11 = U12 = U13 = U14 = U15 = U16 = U21 > mark# = U22 = U23 = U31 = U32 = U41 = U51 = U52 = U61 = U62 = U63 = U64 = plus
      
      partial status:
    
        pi(mark#) = [1]
        pi(s) = [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]
        pi(U41) = [1]
        pi(U51) = [1, 2]
        pi(U52) = [1, 2]
        pi(U61) = [1, 2, 3]
        pi(U62) = [1, 2, 3]
        pi(U63) = [2, 3]
        pi(U64) = [1, 2, 3]
        pi(plus) = [1, 2]
    
    2. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          mark#_A(x1) = x1 + 3
          s_A(x1) = x1
          U11_A(x1,x2,x3) = max{x1, x2 - 1, x3}
          U12_A(x1,x2,x3) = max{x1, x2 - 1, x3}
          U13_A(x1,x2,x3) = max{x1, x2 - 1, x3}
          U14_A(x1,x2,x3) = max{x1, x2 - 1, x3}
          U15_A(x1,x2) = max{x1, x2}
          U16_A(x1) = x1
          U21_A(x1,x2) = max{x1, x2}
          U22_A(x1,x2) = max{x1, x2}
          U23_A(x1) = x1
          U31_A(x1,x2) = max{x1, x2}
          U32_A(x1) = x1
          U41_A(x1) = x1
          U51_A(x1,x2) = max{x1, x2}
          U52_A(x1,x2) = max{x1, x2}
          U61_A(x1,x2,x3) = max{x1, x2 - 1, x3}
          U62_A(x1,x2,x3) = max{x1, x2 - 1, x3}
          U63_A(x1,x2,x3) = max{x2 - 1, x3}
          U64_A(x1,x2,x3) = max{x1, x2 - 1, x3}
          plus_A(x1,x2) = max{x1 + 2, x2 + 4}
    
      precedence:
      
        mark# = s = U11 = U12 = U13 = U14 = U15 > U16 = U21 = U22 = U23 = U31 = U32 = U41 = U51 = U52 = U61 = U62 = U63 = U64 = plus
      
      partial status:
    
        pi(mark#) = [1]
        pi(s) = [1]
        pi(U11) = [1, 3]
        pi(U12) = [1, 3]
        pi(U13) = [1, 3]
        pi(U14) = [1, 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]
        pi(U41) = [1]
        pi(U51) = [1, 2]
        pi(U52) = [1, 2]
        pi(U61) = [1, 3]
        pi(U62) = [1, 3]
        pi(U63) = [3]
        pi(U64) = [1, 3]
        pi(plus) = [1, 2]
    

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

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__plus#(N,s(M)) -> a__U61#(a__isNat(M),M,N)
p2: a__U61#(tt(),M,N) -> a__U62#(a__isNatKind(M),M,N)
p3: a__U62#(tt(),M,N) -> a__U63#(a__isNat(N),M,N)
p4: a__U63#(tt(),M,N) -> a__U64#(a__isNatKind(N),M,N)
p5: a__U64#(tt(),M,N) -> a__plus#(mark(N),mark(M))

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. weighted path order
    
      base order:
    
        matrix interpretations:
        
          carrier: N^2
          order: lexicographic order
          interpretations:
            a__plus#_A(x1,x2) = ((1,0),(0,0)) x2 + (28,60)
            s_A(x1) = ((1,0),(0,0)) x1 + (14,11)
            a__U61#_A(x1,x2,x3) = ((1,0),(0,0)) x1 + ((1,0),(1,0)) x2 + ((0,0),(1,0)) x3 + (6,59)
            a__isNat_A(x1) = (35,59)
            tt_A() = (29,53)
            a__U62#_A(x1,x2,x3) = ((1,0),(0,0)) x1 + ((1,0),(0,0)) x2 + (4,52)
            a__isNatKind_A(x1) = ((0,0),(1,0)) x1 + (30,42)
            a__U63#_A(x1,x2,x3) = x2 + ((0,0),(1,0)) x3 + (32,51)
            a__U64#_A(x1,x2,x3) = x1 + x2 + ((0,0),(1,0)) x3 + (1,8)
            mark_A(x1) = ((1,0),(1,1)) x1 + (0,11)
            a__U11_A(x1,x2,x3) = (35,58)
            a__U12_A(x1,x2,x3) = ((1,0),(1,1)) x1 + ((0,0),(1,0)) x3 + (3,12)
            a__U13_A(x1,x2,x3) = ((0,0),(1,0)) x3 + (32,57)
            a__U14_A(x1,x2,x3) = x1 + (2,14)
            a__U15_A(x1,x2) = ((0,0),(1,0)) x1 + (30,31)
            a__U16_A(x1) = (29,54)
            a__U21_A(x1,x2) = (34,55)
            a__U22_A(x1,x2) = x1 + (2,12)
            a__U23_A(x1) = (31,54)
            a__U31_A(x1,x2) = ((0,0),(1,0)) x1 + ((0,0),(1,0)) x2 + (30,25)
            a__U32_A(x1) = ((1,0),(0,0)) x1 + (0,54)
            a__U41_A(x1) = (29,54)
            a__U51_A(x1,x2) = ((1,0),(1,1)) x2 + (31,41)
            a__U52_A(x1,x2) = ((1,0),(1,0)) x1 + ((1,0),(1,1)) x2 + (0,24)
            a__U61_A(x1,x2,x3) = ((1,0),(0,0)) x2 + x3 + (28,38)
            a__U62_A(x1,x2,x3) = ((1,0),(0,0)) x2 + x3 + (28,37)
            a__U63_A(x1,x2,x3) = ((0,0),(1,0)) x1 + ((1,0),(0,0)) x2 + x3 + (28,2)
            a__U64_A(x1,x2,x3) = ((1,0),(0,0)) x2 + ((1,0),(0,0)) x3 + (28,30)
            a__plus_A(x1,x2) = x1 + ((1,0),(1,1)) x2 + (14,21)
            |0|_A() = (18,1)
            U11_A(x1,x2,x3) = (35,12)
            U12_A(x1,x2,x3) = ((1,0),(1,1)) x1 + ((0,0),(1,0)) x3 + (3,11)
            U13_A(x1,x2,x3) = ((0,0),(1,0)) x3 + (32,15)
            U14_A(x1,x2,x3) = x1 + (2,12)
            U15_A(x1,x2) = ((0,0),(1,0)) x1 + (30,30)
            U16_A(x1) = (29,15)
            U21_A(x1,x2) = (34,11)
            U22_A(x1,x2) = x1 + (2,11)
            U23_A(x1) = (31,13)
            U31_A(x1,x2) = ((0,0),(1,0)) x1 + ((0,0),(1,0)) x2 + (30,25)
            U32_A(x1) = ((1,0),(0,0)) x1 + (0,44)
            U41_A(x1) = (29,15)
            U51_A(x1,x2) = ((1,0),(1,1)) x2 + (31,12)
            U52_A(x1,x2) = ((1,0),(0,0)) x1 + x2 + (0,14)
            U61_A(x1,x2,x3) = ((1,0),(0,0)) x2 + x3 + (28,0)
            U62_A(x1,x2,x3) = ((1,0),(0,0)) x2 + x3 + (28,12)
            U63_A(x1,x2,x3) = ((0,0),(1,0)) x1 + ((1,0),(0,0)) x2 + x3 + (28,1)
            U64_A(x1,x2,x3) = ((1,0),(0,0)) x2 + ((1,0),(0,0)) x3 + (28,29)
            plus_A(x1,x2) = x1 + ((1,0),(1,1)) x2 + (14,20)
            isNatKind_A(x1) = ((0,0),(1,0)) x1 + (30,1)
            isNat_A(x1) = (35,14)
    
      precedence:
      
        a__U64 = U64 > a__U31 = U31 > a__U16 = U21 > a__U13 = U13 > s = a__U61 = U22 = U41 = plus > a__plus# > a__U61# > U16 > a__U62# = U61 > U63 > isNatKind > a__U63# > a__isNat = a__U64# = mark = a__U14 = a__U32 = a__plus > a__U15 = a__U51 = U51 > U15 > U32 > U12 > a__U21 = U14 > a__U22 > a__isNatKind = a__U41 = |0| > a__U23 = U23 > tt > a__U62 > a__U11 = a__U52 = U11 = U52 > U62 > a__U63 > a__U12 > isNat
      
      partial status:
    
        pi(a__plus#) = []
        pi(s) = []
        pi(a__U61#) = []
        pi(a__isNat) = []
        pi(tt) = []
        pi(a__U62#) = []
        pi(a__isNatKind) = []
        pi(a__U63#) = []
        pi(a__U64#) = [2]
        pi(mark) = [1]
        pi(a__U11) = []
        pi(a__U12) = [1]
        pi(a__U13) = []
        pi(a__U14) = [1]
        pi(a__U15) = []
        pi(a__U16) = []
        pi(a__U21) = []
        pi(a__U22) = [1]
        pi(a__U23) = []
        pi(a__U31) = []
        pi(a__U32) = []
        pi(a__U41) = []
        pi(a__U51) = [2]
        pi(a__U52) = [2]
        pi(a__U61) = []
        pi(a__U62) = [3]
        pi(a__U63) = [3]
        pi(a__U64) = []
        pi(a__plus) = [2]
        pi(|0|) = []
        pi(U11) = []
        pi(U12) = [1]
        pi(U13) = []
        pi(U14) = [1]
        pi(U15) = []
        pi(U16) = []
        pi(U21) = []
        pi(U22) = [1]
        pi(U23) = []
        pi(U31) = []
        pi(U32) = []
        pi(U41) = []
        pi(U51) = [2]
        pi(U52) = [2]
        pi(U61) = []
        pi(U62) = [3]
        pi(U63) = [3]
        pi(U64) = []
        pi(plus) = [2]
        pi(isNatKind) = []
        pi(isNat) = []
    
    2. weighted path order
    
      base order:
    
        matrix interpretations:
        
          carrier: N^2
          order: lexicographic order
          interpretations:
            a__plus#_A(x1,x2) = (19,25)
            s_A(x1) = (12,2)
            a__U61#_A(x1,x2,x3) = (9,1)
            a__isNat_A(x1) = (18,49)
            tt_A() = (5,30)
            a__U62#_A(x1,x2,x3) = (19,35)
            a__isNatKind_A(x1) = (8,33)
            a__U63#_A(x1,x2,x3) = (21,34)
            a__U64#_A(x1,x2,x3) = (20,26)
            mark_A(x1) = ((1,0),(1,1)) x1 + (21,27)
            a__U11_A(x1,x2,x3) = (17,48)
            a__U12_A(x1,x2,x3) = ((1,0),(1,0)) x1 + (8,39)
            a__U13_A(x1,x2,x3) = (12,43)
            a__U14_A(x1,x2,x3) = ((1,0),(1,1)) x1 + (3,1)
            a__U15_A(x1,x2) = (7,35)
            a__U16_A(x1) = (6,2)
            a__U21_A(x1,x2) = (23,50)
            a__U22_A(x1,x2) = (24,1)
            a__U23_A(x1) = (2,29)
            a__U31_A(x1,x2) = (7,32)
            a__U32_A(x1) = (6,30)
            a__U41_A(x1) = (0,31)
            a__U51_A(x1,x2) = ((1,0),(0,0)) x2 + (44,78)
            a__U52_A(x1,x2) = ((1,0),(0,0)) x2 + (6,2)
            a__U61_A(x1,x2,x3) = (16,32)
            a__U62_A(x1,x2,x3) = ((1,0),(1,0)) x3 + (15,31)
            a__U63_A(x1,x2,x3) = (14,52)
            a__U64_A(x1,x2,x3) = (13,51)
            a__plus_A(x1,x2) = ((1,0),(0,0)) x2 + (5,50)
            |0|_A() = (0,1)
            U11_A(x1,x2,x3) = (1,49)
            U12_A(x1,x2,x3) = ((1,0),(1,0)) x1 + (8,26)
            U13_A(x1,x2,x3) = (1,16)
            U14_A(x1,x2,x3) = ((1,0),(1,1)) x1 + (21,28)
            U15_A(x1,x2) = (7,35)
            U16_A(x1) = (1,1)
            U21_A(x1,x2) = (1,1)
            U22_A(x1,x2) = (3,28)
            U23_A(x1) = (1,1)
            U31_A(x1,x2) = (7,32)
            U32_A(x1) = (5,26)
            U41_A(x1) = (0,1)
            U51_A(x1,x2) = (22,28)
            U52_A(x1,x2) = x2 + (1,1)
            U61_A(x1,x2,x3) = (6,0)
            U62_A(x1,x2,x3) = ((1,0),(0,0)) x3 + (14,26)
            U63_A(x1,x2,x3) = x3 + (1,1)
            U64_A(x1,x2,x3) = (1,1)
            plus_A(x1,x2) = x2 + (27,32)
            isNatKind_A(x1) = (7,0)
            isNat_A(x1) = (1,22)
    
      precedence:
      
        plus > a__U51 > U22 > a__U31 = U31 > U51 > mark = a__U32 > a__isNatKind = isNatKind > a__U61# > a__U41 > a__U21 > a__U15 = U15 > a__U22 > a__U23 > U41 > a__U62 = a__U63 = U63 > U64 > a__U16 > U16 > U21 > a__U12 > U12 > a__U64 > a__isNat > isNat > a__U11 > U14 > a__U62# > a__U61 = a__plus > U61 > s = a__U13 = a__U14 > a__plus# > U11 > U13 = U32 = U62 > a__U63# > a__U64# > a__U52 = U52 > |0| > tt > U23
      
      partial status:
    
        pi(a__plus#) = []
        pi(s) = []
        pi(a__U61#) = []
        pi(a__isNat) = []
        pi(tt) = []
        pi(a__U62#) = []
        pi(a__isNatKind) = []
        pi(a__U63#) = []
        pi(a__U64#) = []
        pi(mark) = [1]
        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) = []
        pi(a__U51) = []
        pi(a__U52) = []
        pi(a__U61) = []
        pi(a__U62) = []
        pi(a__U63) = []
        pi(a__U64) = []
        pi(a__plus) = []
        pi(|0|) = []
        pi(U11) = []
        pi(U12) = []
        pi(U13) = []
        pi(U14) = [1]
        pi(U15) = []
        pi(U16) = []
        pi(U21) = []
        pi(U22) = []
        pi(U23) = []
        pi(U31) = []
        pi(U32) = []
        pi(U41) = []
        pi(U51) = []
        pi(U52) = []
        pi(U61) = []
        pi(U62) = []
        pi(U63) = []
        pi(U64) = []
        pi(plus) = [2]
        pi(isNatKind) = []
        pi(isNat) = []
    

The next rules are strictly ordered:

  p2, p3, p5

We remove them from the problem.

-- SCC decomposition.

Consider the dependency pair problem (P, R), where P consists of

p1: a__plus#(N,s(M)) -> a__U61#(a__isNat(M),M,N)
p2: a__U63#(tt(),M,N) -> a__U64#(a__isNatKind(N),M,N)

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:

  (no SCCs)

-- 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. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          a__U11#_A(x1,x2,x3) = max{x1 + 6, x2 + 29, x3 + 29}
          tt_A = 24
          a__U12#_A(x1,x2,x3) = max{x1 - 19, x2 + 28, x3 + 28}
          a__isNatKind_A(x1) = max{7, x1 + 6}
          a__U13#_A(x1,x2,x3) = max{x1 + 21, x2 + 28, x3 + 28}
          a__U14#_A(x1,x2,x3) = max{x1 + 1, x2 + 27, x3 + 23}
          a__isNat#_A(x1) = max{21, x1 + 19}
          s_A(x1) = x1 + 9
          a__U21#_A(x1,x2) = max{x1 + 21, x2 + 28}
          a__U22#_A(x1,x2) = max{x1 + 1, x2 + 22}
          plus_A(x1,x2) = max{x1 + 11, x2 + 11}
          a__U15#_A(x1,x2) = max{x1 - 2, x2 + 22}
          a__isNat_A(x1) = x1 + 28
          a__U16_A(x1) = max{4, x1 + 3}
          U16_A(x1) = max{2, x1 + 1}
          a__U15_A(x1,x2) = max{x1, x2 + 32}
          U15_A(x1,x2) = max{x1, x2 + 32}
          a__U14_A(x1,x2,x3) = max{x1 + 1, x2 + 29, x3 + 33}
          U14_A(x1,x2,x3) = max{x1 + 1, x2 + 29, x3 + 33}
          a__U13_A(x1,x2,x3) = max{x1 + 23, x2 + 32, x3 + 34}
          a__U23_A(x1) = max{4, x1 + 3}
          U13_A(x1,x2,x3) = max{x1 + 1, x2, x3}
          U23_A(x1) = max{2, x1 + 1}
          a__U12_A(x1,x2,x3) = max{x1 + 31, x2 + 37, x3 + 38}
          a__U22_A(x1,x2) = max{x1 + 29, x2 + 36}
          a__U32_A(x1) = max{4, x1 + 3}
          U12_A(x1,x2,x3) = max{30, x1, x2, x3}
          U22_A(x1,x2) = max{x1, x2 + 35}
          U32_A(x1) = max{2, x1 + 1}
          a__U11_A(x1,x2,x3) = max{x1 + 14, x2 + 37, x3 + 38}
          a__U21_A(x1,x2) = max{x1 + 12, x2 + 36}
          a__U31_A(x1,x2) = max{x1 + 4, x2 + 11}
          a__U41_A(x1) = max{8, x1 + 1}
          U11_A(x1,x2,x3) = max{x1 + 14, x2 + 37, x3 + 38}
          U21_A(x1,x2) = max{11, x1 + 1, x2 + 1}
          U31_A(x1,x2) = max{x1 + 4, x2 + 11}
          U41_A(x1) = x1
          |0|_A = 25
          isNatKind_A(x1) = max{5, x1 + 1}
          isNat_A(x1) = x1 + 28
    
      precedence:
      
        a__U22# = a__U16 = U16 = a__U15 > a__U15# = U15 = a__U14 = U14 = a__U13 = a__U23 = U23 = a__U32 = U22 = U32 = a__U11 > a__U41 = U11 > U41 = |0| = isNatKind > a__U11# = tt = a__U12# = a__isNatKind = a__U14# = a__isNat# = s = a__U21# = plus = a__isNat = a__U21 > a__U22 > a__U31 = U21 = U31 > a__U13# = U13 = a__U12 = U12 = isNat
      
      partial status:
    
        pi(a__U11#) = [1, 2, 3]
        pi(tt) = []
        pi(a__U12#) = [2, 3]
        pi(a__isNatKind) = []
        pi(a__U13#) = [1, 2, 3]
        pi(a__U14#) = [1, 2, 3]
        pi(a__isNat#) = [1]
        pi(s) = [1]
        pi(a__U21#) = [1, 2]
        pi(a__U22#) = [1, 2]
        pi(plus) = [1, 2]
        pi(a__U15#) = [2]
        pi(a__isNat) = [1]
        pi(a__U16) = [1]
        pi(U16) = [1]
        pi(a__U15) = [1, 2]
        pi(U15) = [1, 2]
        pi(a__U14) = [1, 2, 3]
        pi(U14) = [1, 2]
        pi(a__U13) = [1, 2]
        pi(a__U23) = [1]
        pi(U13) = [1, 2, 3]
        pi(U23) = [1]
        pi(a__U12) = [1, 2, 3]
        pi(a__U22) = [1, 2]
        pi(a__U32) = [1]
        pi(U12) = [1, 2, 3]
        pi(U22) = [1, 2]
        pi(U32) = [1]
        pi(a__U11) = [1, 2, 3]
        pi(a__U21) = [1, 2]
        pi(a__U31) = [1, 2]
        pi(a__U41) = [1]
        pi(U11) = [1, 2, 3]
        pi(U21) = [1, 2]
        pi(U31) = []
        pi(U41) = [1]
        pi(|0|) = []
        pi(isNatKind) = [1]
        pi(isNat) = [1]
    
    2. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          a__U11#_A(x1,x2,x3) = max{x1 - 30, x2 + 37, x3 + 39}
          tt_A = 65
          a__U12#_A(x1,x2,x3) = max{x2 + 36, x3 + 36}
          a__isNatKind_A(x1) = 61
          a__U13#_A(x1,x2,x3) = max{x1 - 28, x2 + 35, x3 + 35}
          a__U14#_A(x1,x2,x3) = max{x1 - 31, x2 + 34, x3 + 34}
          a__isNat#_A(x1) = x1 + 33
          s_A(x1) = x1 + 3
          a__U21#_A(x1,x2) = max{x1 - 30, x2 + 35}
          a__U22#_A(x1,x2) = max{x1 - 32, x2 + 34}
          plus_A(x1,x2) = max{x1 + 5, x2 + 7}
          a__U15#_A(x1,x2) = x2 + 33
          a__isNat_A(x1) = x1 + 38
          a__U16_A(x1) = max{98, x1 + 63}
          U16_A(x1) = max{99, x1 + 64}
          a__U15_A(x1,x2) = max{67, x1 + 32, x2 + 37}
          U15_A(x1,x2) = max{68, x1 + 33, x2 + 38}
          a__U14_A(x1,x2,x3) = max{61, x1 + 1, x2 + 47, x3 + 36}
          U14_A(x1,x2,x3) = max{62, x1 + 2, x2 + 48}
          a__U13_A(x1,x2,x3) = max{56, x1 - 5, x2 + 46}
          a__U23_A(x1) = max{80, x1 + 45}
          U13_A(x1,x2,x3) = max{57, x1 - 4, x2 + 47, x3 - 8}
          U23_A(x1) = max{81, x1 + 46}
          a__U12_A(x1,x2,x3) = max{51, x1 - 10, x2 + 45, x3 + 47}
          a__U22_A(x1,x2) = max{75, x1 + 14, x2 + 63}
          a__U32_A(x1) = max{64, x1 + 9}
          U12_A(x1,x2,x3) = max{52, x1 - 9, x2 + 46, x3 + 48}
          U22_A(x1,x2) = max{76, x1 + 15, x2 + 64}
          U32_A(x1) = max{65, x1 + 10}
          a__U11_A(x1,x2,x3) = max{50, x1 - 15, x2 + 44, x3 + 46}
          a__U21_A(x1,x2) = max{x1 + 9, x2 + 62}
          a__U31_A(x1,x2) = max{x1 - 2, x2 + 62}
          a__U41_A(x1) = max{64, x1 + 10}
          U11_A(x1,x2,x3) = max{51, x1 - 14, x2 + 45, x3 + 47}
          U21_A(x1,x2) = max{x1 + 10, x2 + 63}
          U31_A(x1,x2) = 63
          U41_A(x1) = max{65, x1 + 11}
          |0|_A = 64
          isNatKind_A(x1) = max{62, x1 - 7}
          isNat_A(x1) = x1 + 39
    
      precedence:
      
        a__U11# = tt = a__U12# = a__isNatKind = a__U13# = a__U14# = a__isNat# = s = a__U21# = a__U22# = plus = a__U15# = a__isNat = a__U16 = U16 = a__U15 = U15 = a__U14 = U14 = a__U13 = a__U23 = U13 = U23 = a__U12 = a__U22 = a__U32 = U12 = U22 = U32 = a__U11 = a__U21 = a__U31 = a__U41 = U11 = U21 = U31 = U41 = |0| = isNatKind = isNat
      
      partial status:
    
        pi(a__U11#) = []
        pi(tt) = []
        pi(a__U12#) = [3]
        pi(a__isNatKind) = []
        pi(a__U13#) = [3]
        pi(a__U14#) = [2, 3]
        pi(a__isNat#) = []
        pi(s) = [1]
        pi(a__U21#) = [2]
        pi(a__U22#) = [2]
        pi(plus) = [2]
        pi(a__U15#) = [2]
        pi(a__isNat) = [1]
        pi(a__U16) = [1]
        pi(U16) = []
        pi(a__U15) = []
        pi(U15) = []
        pi(a__U14) = [3]
        pi(U14) = []
        pi(a__U13) = []
        pi(a__U23) = []
        pi(U13) = []
        pi(U23) = []
        pi(a__U12) = [3]
        pi(a__U22) = [2]
        pi(a__U32) = [1]
        pi(U12) = []
        pi(U22) = []
        pi(U32) = [1]
        pi(a__U11) = []
        pi(a__U21) = []
        pi(a__U31) = []
        pi(a__U41) = []
        pi(U11) = []
        pi(U21) = []
        pi(U31) = []
        pi(U41) = []
        pi(|0|) = []
        pi(isNatKind) = []
        pi(isNat) = [1]
    

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. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          a__isNatKind#_A(x1) = max{38, x1 + 6}
          plus_A(x1,x2) = max{x1 + 27, x2 + 40}
          a__U31#_A(x1,x2) = max{40, x1 + 6, x2 + 39}
          a__isNatKind_A(x1) = max{34, x1 + 21}
          tt_A = 33
          s_A(x1) = x1 + 39
          a__U32_A(x1) = max{1, x1}
          U32_A(x1) = x1
          a__U31_A(x1,x2) = max{41, x1 + 2, x2 + 21}
          a__U41_A(x1) = max{53, x1 + 19}
          U31_A(x1,x2) = max{x1, x2}
          U41_A(x1) = max{1, x1}
          |0|_A = 34
          isNatKind_A(x1) = max{20, x1 + 19}
    
      precedence:
      
        s > a__isNatKind# = plus = a__U31# = tt = a__U31 > a__isNatKind = a__U32 > U32 = a__U41 = U31 = U41 = |0| = isNatKind
      
      partial status:
    
        pi(a__isNatKind#) = [1]
        pi(plus) = [1, 2]
        pi(a__U31#) = [2]
        pi(a__isNatKind) = [1]
        pi(tt) = []
        pi(s) = [1]
        pi(a__U32) = [1]
        pi(U32) = [1]
        pi(a__U31) = [1]
        pi(a__U41) = [1]
        pi(U31) = [1, 2]
        pi(U41) = [1]
        pi(|0|) = []
        pi(isNatKind) = [1]
    
    2. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          a__isNatKind#_A(x1) = max{7, x1 + 5}
          plus_A(x1,x2) = max{x1 + 5, x2 + 5}
          a__U31#_A(x1,x2) = x2 + 8
          a__isNatKind_A(x1) = max{16, x1 + 11}
          tt_A = 18
          s_A(x1) = max{5, x1 + 3}
          a__U32_A(x1) = max{25, x1 + 9}
          U32_A(x1) = max{26, x1 + 10}
          a__U31_A(x1,x2) = max{17, x1 + 6}
          a__U41_A(x1) = max{17, x1 + 4}
          U31_A(x1,x2) = max{18, x1 + 7, x2 + 11}
          U41_A(x1) = max{18, x1 + 5}
          |0|_A = 17
          isNatKind_A(x1) = max{17, x1 + 12}
    
      precedence:
      
        a__isNatKind# = plus = a__U31# = a__isNatKind = tt = s = a__U32 = U32 = a__U31 = a__U41 = U31 = U41 = |0| = isNatKind
      
      partial status:
    
        pi(a__isNatKind#) = []
        pi(plus) = [2]
        pi(a__U31#) = []
        pi(a__isNatKind) = [1]
        pi(tt) = []
        pi(s) = [1]
        pi(a__U32) = [1]
        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.