YES

We show the termination of the TRS R:

  active(U11(tt(),V1,V2)) -> mark(U12(isNat(V1),V2))
  active(U12(tt(),V2)) -> mark(U13(isNat(V2)))
  active(U13(tt())) -> mark(tt())
  active(U21(tt(),V1)) -> mark(U22(isNat(V1)))
  active(U22(tt())) -> mark(tt())
  active(U31(tt(),N)) -> mark(N)
  active(U41(tt(),M,N)) -> mark(s(plus(N,M)))
  active(and(tt(),X)) -> mark(X)
  active(isNat(|0|())) -> mark(tt())
  active(isNat(plus(V1,V2))) -> mark(U11(and(isNatKind(V1),isNatKind(V2)),V1,V2))
  active(isNat(s(V1))) -> mark(U21(isNatKind(V1),V1))
  active(isNatKind(|0|())) -> mark(tt())
  active(isNatKind(plus(V1,V2))) -> mark(and(isNatKind(V1),isNatKind(V2)))
  active(isNatKind(s(V1))) -> mark(isNatKind(V1))
  active(plus(N,|0|())) -> mark(U31(and(isNat(N),isNatKind(N)),N))
  active(plus(N,s(M))) -> mark(U41(and(and(isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N))
  mark(U11(X1,X2,X3)) -> active(U11(mark(X1),X2,X3))
  mark(tt()) -> active(tt())
  mark(U12(X1,X2)) -> active(U12(mark(X1),X2))
  mark(isNat(X)) -> active(isNat(X))
  mark(U13(X)) -> active(U13(mark(X)))
  mark(U21(X1,X2)) -> active(U21(mark(X1),X2))
  mark(U22(X)) -> active(U22(mark(X)))
  mark(U31(X1,X2)) -> active(U31(mark(X1),X2))
  mark(U41(X1,X2,X3)) -> active(U41(mark(X1),X2,X3))
  mark(s(X)) -> active(s(mark(X)))
  mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2)))
  mark(and(X1,X2)) -> active(and(mark(X1),X2))
  mark(|0|()) -> active(|0|())
  mark(isNatKind(X)) -> active(isNatKind(X))
  U11(mark(X1),X2,X3) -> U11(X1,X2,X3)
  U11(X1,mark(X2),X3) -> U11(X1,X2,X3)
  U11(X1,X2,mark(X3)) -> U11(X1,X2,X3)
  U11(active(X1),X2,X3) -> U11(X1,X2,X3)
  U11(X1,active(X2),X3) -> U11(X1,X2,X3)
  U11(X1,X2,active(X3)) -> U11(X1,X2,X3)
  U12(mark(X1),X2) -> U12(X1,X2)
  U12(X1,mark(X2)) -> U12(X1,X2)
  U12(active(X1),X2) -> U12(X1,X2)
  U12(X1,active(X2)) -> U12(X1,X2)
  isNat(mark(X)) -> isNat(X)
  isNat(active(X)) -> isNat(X)
  U13(mark(X)) -> U13(X)
  U13(active(X)) -> U13(X)
  U21(mark(X1),X2) -> U21(X1,X2)
  U21(X1,mark(X2)) -> U21(X1,X2)
  U21(active(X1),X2) -> U21(X1,X2)
  U21(X1,active(X2)) -> U21(X1,X2)
  U22(mark(X)) -> U22(X)
  U22(active(X)) -> U22(X)
  U31(mark(X1),X2) -> U31(X1,X2)
  U31(X1,mark(X2)) -> U31(X1,X2)
  U31(active(X1),X2) -> U31(X1,X2)
  U31(X1,active(X2)) -> U31(X1,X2)
  U41(mark(X1),X2,X3) -> U41(X1,X2,X3)
  U41(X1,mark(X2),X3) -> U41(X1,X2,X3)
  U41(X1,X2,mark(X3)) -> U41(X1,X2,X3)
  U41(active(X1),X2,X3) -> U41(X1,X2,X3)
  U41(X1,active(X2),X3) -> U41(X1,X2,X3)
  U41(X1,X2,active(X3)) -> U41(X1,X2,X3)
  s(mark(X)) -> s(X)
  s(active(X)) -> s(X)
  plus(mark(X1),X2) -> plus(X1,X2)
  plus(X1,mark(X2)) -> plus(X1,X2)
  plus(active(X1),X2) -> plus(X1,X2)
  plus(X1,active(X2)) -> plus(X1,X2)
  and(mark(X1),X2) -> and(X1,X2)
  and(X1,mark(X2)) -> and(X1,X2)
  and(active(X1),X2) -> and(X1,X2)
  and(X1,active(X2)) -> and(X1,X2)
  isNatKind(mark(X)) -> isNatKind(X)
  isNatKind(active(X)) -> isNatKind(X)

-- SCC decomposition.

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

p1: active#(U11(tt(),V1,V2)) -> mark#(U12(isNat(V1),V2))
p2: active#(U11(tt(),V1,V2)) -> U12#(isNat(V1),V2)
p3: active#(U11(tt(),V1,V2)) -> isNat#(V1)
p4: active#(U12(tt(),V2)) -> mark#(U13(isNat(V2)))
p5: active#(U12(tt(),V2)) -> U13#(isNat(V2))
p6: active#(U12(tt(),V2)) -> isNat#(V2)
p7: active#(U13(tt())) -> mark#(tt())
p8: active#(U21(tt(),V1)) -> mark#(U22(isNat(V1)))
p9: active#(U21(tt(),V1)) -> U22#(isNat(V1))
p10: active#(U21(tt(),V1)) -> isNat#(V1)
p11: active#(U22(tt())) -> mark#(tt())
p12: active#(U31(tt(),N)) -> mark#(N)
p13: active#(U41(tt(),M,N)) -> mark#(s(plus(N,M)))
p14: active#(U41(tt(),M,N)) -> s#(plus(N,M))
p15: active#(U41(tt(),M,N)) -> plus#(N,M)
p16: active#(and(tt(),X)) -> mark#(X)
p17: active#(isNat(|0|())) -> mark#(tt())
p18: active#(isNat(plus(V1,V2))) -> mark#(U11(and(isNatKind(V1),isNatKind(V2)),V1,V2))
p19: active#(isNat(plus(V1,V2))) -> U11#(and(isNatKind(V1),isNatKind(V2)),V1,V2)
p20: active#(isNat(plus(V1,V2))) -> and#(isNatKind(V1),isNatKind(V2))
p21: active#(isNat(plus(V1,V2))) -> isNatKind#(V1)
p22: active#(isNat(plus(V1,V2))) -> isNatKind#(V2)
p23: active#(isNat(s(V1))) -> mark#(U21(isNatKind(V1),V1))
p24: active#(isNat(s(V1))) -> U21#(isNatKind(V1),V1)
p25: active#(isNat(s(V1))) -> isNatKind#(V1)
p26: active#(isNatKind(|0|())) -> mark#(tt())
p27: active#(isNatKind(plus(V1,V2))) -> mark#(and(isNatKind(V1),isNatKind(V2)))
p28: active#(isNatKind(plus(V1,V2))) -> and#(isNatKind(V1),isNatKind(V2))
p29: active#(isNatKind(plus(V1,V2))) -> isNatKind#(V1)
p30: active#(isNatKind(plus(V1,V2))) -> isNatKind#(V2)
p31: active#(isNatKind(s(V1))) -> mark#(isNatKind(V1))
p32: active#(isNatKind(s(V1))) -> isNatKind#(V1)
p33: active#(plus(N,|0|())) -> mark#(U31(and(isNat(N),isNatKind(N)),N))
p34: active#(plus(N,|0|())) -> U31#(and(isNat(N),isNatKind(N)),N)
p35: active#(plus(N,|0|())) -> and#(isNat(N),isNatKind(N))
p36: active#(plus(N,|0|())) -> isNat#(N)
p37: active#(plus(N,|0|())) -> isNatKind#(N)
p38: active#(plus(N,s(M))) -> mark#(U41(and(and(isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N))
p39: active#(plus(N,s(M))) -> U41#(and(and(isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N)
p40: active#(plus(N,s(M))) -> and#(and(isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N)))
p41: active#(plus(N,s(M))) -> and#(isNat(M),isNatKind(M))
p42: active#(plus(N,s(M))) -> isNat#(M)
p43: active#(plus(N,s(M))) -> isNatKind#(M)
p44: active#(plus(N,s(M))) -> and#(isNat(N),isNatKind(N))
p45: active#(plus(N,s(M))) -> isNat#(N)
p46: active#(plus(N,s(M))) -> isNatKind#(N)
p47: mark#(U11(X1,X2,X3)) -> active#(U11(mark(X1),X2,X3))
p48: mark#(U11(X1,X2,X3)) -> U11#(mark(X1),X2,X3)
p49: mark#(U11(X1,X2,X3)) -> mark#(X1)
p50: mark#(tt()) -> active#(tt())
p51: mark#(U12(X1,X2)) -> active#(U12(mark(X1),X2))
p52: mark#(U12(X1,X2)) -> U12#(mark(X1),X2)
p53: mark#(U12(X1,X2)) -> mark#(X1)
p54: mark#(isNat(X)) -> active#(isNat(X))
p55: mark#(U13(X)) -> active#(U13(mark(X)))
p56: mark#(U13(X)) -> U13#(mark(X))
p57: mark#(U13(X)) -> mark#(X)
p58: mark#(U21(X1,X2)) -> active#(U21(mark(X1),X2))
p59: mark#(U21(X1,X2)) -> U21#(mark(X1),X2)
p60: mark#(U21(X1,X2)) -> mark#(X1)
p61: mark#(U22(X)) -> active#(U22(mark(X)))
p62: mark#(U22(X)) -> U22#(mark(X))
p63: mark#(U22(X)) -> mark#(X)
p64: mark#(U31(X1,X2)) -> active#(U31(mark(X1),X2))
p65: mark#(U31(X1,X2)) -> U31#(mark(X1),X2)
p66: mark#(U31(X1,X2)) -> mark#(X1)
p67: mark#(U41(X1,X2,X3)) -> active#(U41(mark(X1),X2,X3))
p68: mark#(U41(X1,X2,X3)) -> U41#(mark(X1),X2,X3)
p69: mark#(U41(X1,X2,X3)) -> mark#(X1)
p70: mark#(s(X)) -> active#(s(mark(X)))
p71: mark#(s(X)) -> s#(mark(X))
p72: mark#(s(X)) -> mark#(X)
p73: mark#(plus(X1,X2)) -> active#(plus(mark(X1),mark(X2)))
p74: mark#(plus(X1,X2)) -> plus#(mark(X1),mark(X2))
p75: mark#(plus(X1,X2)) -> mark#(X1)
p76: mark#(plus(X1,X2)) -> mark#(X2)
p77: mark#(and(X1,X2)) -> active#(and(mark(X1),X2))
p78: mark#(and(X1,X2)) -> and#(mark(X1),X2)
p79: mark#(and(X1,X2)) -> mark#(X1)
p80: mark#(|0|()) -> active#(|0|())
p81: mark#(isNatKind(X)) -> active#(isNatKind(X))
p82: U11#(mark(X1),X2,X3) -> U11#(X1,X2,X3)
p83: U11#(X1,mark(X2),X3) -> U11#(X1,X2,X3)
p84: U11#(X1,X2,mark(X3)) -> U11#(X1,X2,X3)
p85: U11#(active(X1),X2,X3) -> U11#(X1,X2,X3)
p86: U11#(X1,active(X2),X3) -> U11#(X1,X2,X3)
p87: U11#(X1,X2,active(X3)) -> U11#(X1,X2,X3)
p88: U12#(mark(X1),X2) -> U12#(X1,X2)
p89: U12#(X1,mark(X2)) -> U12#(X1,X2)
p90: U12#(active(X1),X2) -> U12#(X1,X2)
p91: U12#(X1,active(X2)) -> U12#(X1,X2)
p92: isNat#(mark(X)) -> isNat#(X)
p93: isNat#(active(X)) -> isNat#(X)
p94: U13#(mark(X)) -> U13#(X)
p95: U13#(active(X)) -> U13#(X)
p96: U21#(mark(X1),X2) -> U21#(X1,X2)
p97: U21#(X1,mark(X2)) -> U21#(X1,X2)
p98: U21#(active(X1),X2) -> U21#(X1,X2)
p99: U21#(X1,active(X2)) -> U21#(X1,X2)
p100: U22#(mark(X)) -> U22#(X)
p101: U22#(active(X)) -> U22#(X)
p102: U31#(mark(X1),X2) -> U31#(X1,X2)
p103: U31#(X1,mark(X2)) -> U31#(X1,X2)
p104: U31#(active(X1),X2) -> U31#(X1,X2)
p105: U31#(X1,active(X2)) -> U31#(X1,X2)
p106: U41#(mark(X1),X2,X3) -> U41#(X1,X2,X3)
p107: U41#(X1,mark(X2),X3) -> U41#(X1,X2,X3)
p108: U41#(X1,X2,mark(X3)) -> U41#(X1,X2,X3)
p109: U41#(active(X1),X2,X3) -> U41#(X1,X2,X3)
p110: U41#(X1,active(X2),X3) -> U41#(X1,X2,X3)
p111: U41#(X1,X2,active(X3)) -> U41#(X1,X2,X3)
p112: s#(mark(X)) -> s#(X)
p113: s#(active(X)) -> s#(X)
p114: plus#(mark(X1),X2) -> plus#(X1,X2)
p115: plus#(X1,mark(X2)) -> plus#(X1,X2)
p116: plus#(active(X1),X2) -> plus#(X1,X2)
p117: plus#(X1,active(X2)) -> plus#(X1,X2)
p118: and#(mark(X1),X2) -> and#(X1,X2)
p119: and#(X1,mark(X2)) -> and#(X1,X2)
p120: and#(active(X1),X2) -> and#(X1,X2)
p121: and#(X1,active(X2)) -> and#(X1,X2)
p122: isNatKind#(mark(X)) -> isNatKind#(X)
p123: isNatKind#(active(X)) -> isNatKind#(X)

and R consists of:

r1: active(U11(tt(),V1,V2)) -> mark(U12(isNat(V1),V2))
r2: active(U12(tt(),V2)) -> mark(U13(isNat(V2)))
r3: active(U13(tt())) -> mark(tt())
r4: active(U21(tt(),V1)) -> mark(U22(isNat(V1)))
r5: active(U22(tt())) -> mark(tt())
r6: active(U31(tt(),N)) -> mark(N)
r7: active(U41(tt(),M,N)) -> mark(s(plus(N,M)))
r8: active(and(tt(),X)) -> mark(X)
r9: active(isNat(|0|())) -> mark(tt())
r10: active(isNat(plus(V1,V2))) -> mark(U11(and(isNatKind(V1),isNatKind(V2)),V1,V2))
r11: active(isNat(s(V1))) -> mark(U21(isNatKind(V1),V1))
r12: active(isNatKind(|0|())) -> mark(tt())
r13: active(isNatKind(plus(V1,V2))) -> mark(and(isNatKind(V1),isNatKind(V2)))
r14: active(isNatKind(s(V1))) -> mark(isNatKind(V1))
r15: active(plus(N,|0|())) -> mark(U31(and(isNat(N),isNatKind(N)),N))
r16: active(plus(N,s(M))) -> mark(U41(and(and(isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N))
r17: mark(U11(X1,X2,X3)) -> active(U11(mark(X1),X2,X3))
r18: mark(tt()) -> active(tt())
r19: mark(U12(X1,X2)) -> active(U12(mark(X1),X2))
r20: mark(isNat(X)) -> active(isNat(X))
r21: mark(U13(X)) -> active(U13(mark(X)))
r22: mark(U21(X1,X2)) -> active(U21(mark(X1),X2))
r23: mark(U22(X)) -> active(U22(mark(X)))
r24: mark(U31(X1,X2)) -> active(U31(mark(X1),X2))
r25: mark(U41(X1,X2,X3)) -> active(U41(mark(X1),X2,X3))
r26: mark(s(X)) -> active(s(mark(X)))
r27: mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2)))
r28: mark(and(X1,X2)) -> active(and(mark(X1),X2))
r29: mark(|0|()) -> active(|0|())
r30: mark(isNatKind(X)) -> active(isNatKind(X))
r31: U11(mark(X1),X2,X3) -> U11(X1,X2,X3)
r32: U11(X1,mark(X2),X3) -> U11(X1,X2,X3)
r33: U11(X1,X2,mark(X3)) -> U11(X1,X2,X3)
r34: U11(active(X1),X2,X3) -> U11(X1,X2,X3)
r35: U11(X1,active(X2),X3) -> U11(X1,X2,X3)
r36: U11(X1,X2,active(X3)) -> U11(X1,X2,X3)
r37: U12(mark(X1),X2) -> U12(X1,X2)
r38: U12(X1,mark(X2)) -> U12(X1,X2)
r39: U12(active(X1),X2) -> U12(X1,X2)
r40: U12(X1,active(X2)) -> U12(X1,X2)
r41: isNat(mark(X)) -> isNat(X)
r42: isNat(active(X)) -> isNat(X)
r43: U13(mark(X)) -> U13(X)
r44: U13(active(X)) -> U13(X)
r45: U21(mark(X1),X2) -> U21(X1,X2)
r46: U21(X1,mark(X2)) -> U21(X1,X2)
r47: U21(active(X1),X2) -> U21(X1,X2)
r48: U21(X1,active(X2)) -> U21(X1,X2)
r49: U22(mark(X)) -> U22(X)
r50: U22(active(X)) -> U22(X)
r51: U31(mark(X1),X2) -> U31(X1,X2)
r52: U31(X1,mark(X2)) -> U31(X1,X2)
r53: U31(active(X1),X2) -> U31(X1,X2)
r54: U31(X1,active(X2)) -> U31(X1,X2)
r55: U41(mark(X1),X2,X3) -> U41(X1,X2,X3)
r56: U41(X1,mark(X2),X3) -> U41(X1,X2,X3)
r57: U41(X1,X2,mark(X3)) -> U41(X1,X2,X3)
r58: U41(active(X1),X2,X3) -> U41(X1,X2,X3)
r59: U41(X1,active(X2),X3) -> U41(X1,X2,X3)
r60: U41(X1,X2,active(X3)) -> U41(X1,X2,X3)
r61: s(mark(X)) -> s(X)
r62: s(active(X)) -> s(X)
r63: plus(mark(X1),X2) -> plus(X1,X2)
r64: plus(X1,mark(X2)) -> plus(X1,X2)
r65: plus(active(X1),X2) -> plus(X1,X2)
r66: plus(X1,active(X2)) -> plus(X1,X2)
r67: and(mark(X1),X2) -> and(X1,X2)
r68: and(X1,mark(X2)) -> and(X1,X2)
r69: and(active(X1),X2) -> and(X1,X2)
r70: and(X1,active(X2)) -> and(X1,X2)
r71: isNatKind(mark(X)) -> isNatKind(X)
r72: isNatKind(active(X)) -> isNatKind(X)

The estimated dependency graph contains the following SCCs:

  {p1, p4, p8, p12, p13, p16, p18, p23, p27, p31, p33, p38, p47, p49, p51, p53, p54, p55, p57, p58, p60, p61, p63, p64, p66, p67, p69, p70, p72, p73, p75, p76, p77, p79, p81}
  {p88, p89, p90, p91}
  {p92, p93}
  {p94, p95}
  {p100, p101}
  {p112, p113}
  {p114, p115, p116, p117}
  {p82, p83, p84, p85, p86, p87}
  {p118, p119, p120, p121}
  {p122, p123}
  {p96, p97, p98, p99}
  {p102, p103, p104, p105}
  {p106, p107, p108, p109, p110, p111}


-- Reduction pair.

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

p1: active#(U11(tt(),V1,V2)) -> mark#(U12(isNat(V1),V2))
p2: mark#(isNatKind(X)) -> active#(isNatKind(X))
p3: active#(plus(N,s(M))) -> mark#(U41(and(and(isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N))
p4: mark#(and(X1,X2)) -> mark#(X1)
p5: mark#(and(X1,X2)) -> active#(and(mark(X1),X2))
p6: active#(plus(N,|0|())) -> mark#(U31(and(isNat(N),isNatKind(N)),N))
p7: mark#(plus(X1,X2)) -> mark#(X2)
p8: mark#(plus(X1,X2)) -> mark#(X1)
p9: mark#(plus(X1,X2)) -> active#(plus(mark(X1),mark(X2)))
p10: active#(isNatKind(s(V1))) -> mark#(isNatKind(V1))
p11: mark#(s(X)) -> mark#(X)
p12: mark#(s(X)) -> active#(s(mark(X)))
p13: active#(isNatKind(plus(V1,V2))) -> mark#(and(isNatKind(V1),isNatKind(V2)))
p14: mark#(U41(X1,X2,X3)) -> mark#(X1)
p15: mark#(U41(X1,X2,X3)) -> active#(U41(mark(X1),X2,X3))
p16: active#(isNat(s(V1))) -> mark#(U21(isNatKind(V1),V1))
p17: mark#(U31(X1,X2)) -> mark#(X1)
p18: mark#(U31(X1,X2)) -> active#(U31(mark(X1),X2))
p19: active#(isNat(plus(V1,V2))) -> mark#(U11(and(isNatKind(V1),isNatKind(V2)),V1,V2))
p20: mark#(U22(X)) -> mark#(X)
p21: mark#(U22(X)) -> active#(U22(mark(X)))
p22: active#(and(tt(),X)) -> mark#(X)
p23: mark#(U21(X1,X2)) -> mark#(X1)
p24: mark#(U21(X1,X2)) -> active#(U21(mark(X1),X2))
p25: active#(U41(tt(),M,N)) -> mark#(s(plus(N,M)))
p26: mark#(U13(X)) -> mark#(X)
p27: mark#(U13(X)) -> active#(U13(mark(X)))
p28: active#(U31(tt(),N)) -> mark#(N)
p29: mark#(isNat(X)) -> active#(isNat(X))
p30: active#(U21(tt(),V1)) -> mark#(U22(isNat(V1)))
p31: mark#(U12(X1,X2)) -> mark#(X1)
p32: mark#(U12(X1,X2)) -> active#(U12(mark(X1),X2))
p33: active#(U12(tt(),V2)) -> mark#(U13(isNat(V2)))
p34: mark#(U11(X1,X2,X3)) -> mark#(X1)
p35: mark#(U11(X1,X2,X3)) -> active#(U11(mark(X1),X2,X3))

and R consists of:

r1: active(U11(tt(),V1,V2)) -> mark(U12(isNat(V1),V2))
r2: active(U12(tt(),V2)) -> mark(U13(isNat(V2)))
r3: active(U13(tt())) -> mark(tt())
r4: active(U21(tt(),V1)) -> mark(U22(isNat(V1)))
r5: active(U22(tt())) -> mark(tt())
r6: active(U31(tt(),N)) -> mark(N)
r7: active(U41(tt(),M,N)) -> mark(s(plus(N,M)))
r8: active(and(tt(),X)) -> mark(X)
r9: active(isNat(|0|())) -> mark(tt())
r10: active(isNat(plus(V1,V2))) -> mark(U11(and(isNatKind(V1),isNatKind(V2)),V1,V2))
r11: active(isNat(s(V1))) -> mark(U21(isNatKind(V1),V1))
r12: active(isNatKind(|0|())) -> mark(tt())
r13: active(isNatKind(plus(V1,V2))) -> mark(and(isNatKind(V1),isNatKind(V2)))
r14: active(isNatKind(s(V1))) -> mark(isNatKind(V1))
r15: active(plus(N,|0|())) -> mark(U31(and(isNat(N),isNatKind(N)),N))
r16: active(plus(N,s(M))) -> mark(U41(and(and(isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N))
r17: mark(U11(X1,X2,X3)) -> active(U11(mark(X1),X2,X3))
r18: mark(tt()) -> active(tt())
r19: mark(U12(X1,X2)) -> active(U12(mark(X1),X2))
r20: mark(isNat(X)) -> active(isNat(X))
r21: mark(U13(X)) -> active(U13(mark(X)))
r22: mark(U21(X1,X2)) -> active(U21(mark(X1),X2))
r23: mark(U22(X)) -> active(U22(mark(X)))
r24: mark(U31(X1,X2)) -> active(U31(mark(X1),X2))
r25: mark(U41(X1,X2,X3)) -> active(U41(mark(X1),X2,X3))
r26: mark(s(X)) -> active(s(mark(X)))
r27: mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2)))
r28: mark(and(X1,X2)) -> active(and(mark(X1),X2))
r29: mark(|0|()) -> active(|0|())
r30: mark(isNatKind(X)) -> active(isNatKind(X))
r31: U11(mark(X1),X2,X3) -> U11(X1,X2,X3)
r32: U11(X1,mark(X2),X3) -> U11(X1,X2,X3)
r33: U11(X1,X2,mark(X3)) -> U11(X1,X2,X3)
r34: U11(active(X1),X2,X3) -> U11(X1,X2,X3)
r35: U11(X1,active(X2),X3) -> U11(X1,X2,X3)
r36: U11(X1,X2,active(X3)) -> U11(X1,X2,X3)
r37: U12(mark(X1),X2) -> U12(X1,X2)
r38: U12(X1,mark(X2)) -> U12(X1,X2)
r39: U12(active(X1),X2) -> U12(X1,X2)
r40: U12(X1,active(X2)) -> U12(X1,X2)
r41: isNat(mark(X)) -> isNat(X)
r42: isNat(active(X)) -> isNat(X)
r43: U13(mark(X)) -> U13(X)
r44: U13(active(X)) -> U13(X)
r45: U21(mark(X1),X2) -> U21(X1,X2)
r46: U21(X1,mark(X2)) -> U21(X1,X2)
r47: U21(active(X1),X2) -> U21(X1,X2)
r48: U21(X1,active(X2)) -> U21(X1,X2)
r49: U22(mark(X)) -> U22(X)
r50: U22(active(X)) -> U22(X)
r51: U31(mark(X1),X2) -> U31(X1,X2)
r52: U31(X1,mark(X2)) -> U31(X1,X2)
r53: U31(active(X1),X2) -> U31(X1,X2)
r54: U31(X1,active(X2)) -> U31(X1,X2)
r55: U41(mark(X1),X2,X3) -> U41(X1,X2,X3)
r56: U41(X1,mark(X2),X3) -> U41(X1,X2,X3)
r57: U41(X1,X2,mark(X3)) -> U41(X1,X2,X3)
r58: U41(active(X1),X2,X3) -> U41(X1,X2,X3)
r59: U41(X1,active(X2),X3) -> U41(X1,X2,X3)
r60: U41(X1,X2,active(X3)) -> U41(X1,X2,X3)
r61: s(mark(X)) -> s(X)
r62: s(active(X)) -> s(X)
r63: plus(mark(X1),X2) -> plus(X1,X2)
r64: plus(X1,mark(X2)) -> plus(X1,X2)
r65: plus(active(X1),X2) -> plus(X1,X2)
r66: plus(X1,active(X2)) -> plus(X1,X2)
r67: and(mark(X1),X2) -> and(X1,X2)
r68: and(X1,mark(X2)) -> and(X1,X2)
r69: and(active(X1),X2) -> and(X1,X2)
r70: and(X1,active(X2)) -> and(X1,X2)
r71: isNatKind(mark(X)) -> isNatKind(X)
r72: isNatKind(active(X)) -> isNatKind(X)

The set of usable rules consists of

  r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r12, r13, r14, r15, r16, r17, r18, r19, r20, r21, r22, r23, r24, r25, r26, r27, r28, r29, r30, r31, r32, r33, 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, r72

Take the reduction pair:

  matrix interpretations:
  
    carrier: N^3
    order: lexicographic order
    interpretations:
      active#_A(x1) = ((0,0,0),(0,0,0),(1,0,0)) x1
      U11_A(x1,x2,x3) = ((1,0,0),(1,0,0),(0,0,0)) x1
      tt_A() = (0,0,0)
      mark#_A(x1) = ((0,0,0),(0,0,0),(1,0,0)) x1
      U12_A(x1,x2) = x1 + ((0,0,0),(0,0,0),(1,0,0)) x2 + (0,1,0)
      isNat_A(x1) = (0,0,0)
      isNatKind_A(x1) = ((0,0,0),(1,0,0),(0,0,0)) x1
      plus_A(x1,x2) = x1 + ((1,0,0),(0,0,0),(1,0,0)) x2 + (1,1,0)
      s_A(x1) = ((1,0,0),(0,0,0),(1,0,0)) x1 + (1,0,0)
      U41_A(x1,x2,x3) = x1 + x2 + ((1,0,0),(1,0,0),(1,0,0)) x3 + (2,0,0)
      and_A(x1,x2) = ((1,0,0),(0,0,0),(1,0,0)) x1 + ((1,0,0),(0,0,0),(1,0,0)) x2 + (0,0,1)
      mark_A(x1) = ((1,0,0),(1,0,0),(1,0,0)) x1 + (0,1,1)
      |0|_A() = (1,0,0)
      U31_A(x1,x2) = x1 + x2 + (1,0,0)
      U21_A(x1,x2) = x1 + ((0,0,0),(0,0,0),(1,0,0)) x2 + (0,0,1)
      U22_A(x1) = x1
      U13_A(x1) = x1 + (0,1,0)
      active_A(x1) = ((1,0,0),(1,0,0),(1,0,0)) x1 + (0,1,1)

The next rules are strictly ordered:

  p6, p7, p8, p11, p14, p17, p28

We remove them from the problem.

-- SCC decomposition.

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

p1: active#(U11(tt(),V1,V2)) -> mark#(U12(isNat(V1),V2))
p2: mark#(isNatKind(X)) -> active#(isNatKind(X))
p3: active#(plus(N,s(M))) -> mark#(U41(and(and(isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N))
p4: mark#(and(X1,X2)) -> mark#(X1)
p5: mark#(and(X1,X2)) -> active#(and(mark(X1),X2))
p6: mark#(plus(X1,X2)) -> active#(plus(mark(X1),mark(X2)))
p7: active#(isNatKind(s(V1))) -> mark#(isNatKind(V1))
p8: mark#(s(X)) -> active#(s(mark(X)))
p9: active#(isNatKind(plus(V1,V2))) -> mark#(and(isNatKind(V1),isNatKind(V2)))
p10: mark#(U41(X1,X2,X3)) -> active#(U41(mark(X1),X2,X3))
p11: active#(isNat(s(V1))) -> mark#(U21(isNatKind(V1),V1))
p12: mark#(U31(X1,X2)) -> active#(U31(mark(X1),X2))
p13: active#(isNat(plus(V1,V2))) -> mark#(U11(and(isNatKind(V1),isNatKind(V2)),V1,V2))
p14: mark#(U22(X)) -> mark#(X)
p15: mark#(U22(X)) -> active#(U22(mark(X)))
p16: active#(and(tt(),X)) -> mark#(X)
p17: mark#(U21(X1,X2)) -> mark#(X1)
p18: mark#(U21(X1,X2)) -> active#(U21(mark(X1),X2))
p19: active#(U41(tt(),M,N)) -> mark#(s(plus(N,M)))
p20: mark#(U13(X)) -> mark#(X)
p21: mark#(U13(X)) -> active#(U13(mark(X)))
p22: mark#(isNat(X)) -> active#(isNat(X))
p23: active#(U21(tt(),V1)) -> mark#(U22(isNat(V1)))
p24: mark#(U12(X1,X2)) -> mark#(X1)
p25: mark#(U12(X1,X2)) -> active#(U12(mark(X1),X2))
p26: active#(U12(tt(),V2)) -> mark#(U13(isNat(V2)))
p27: mark#(U11(X1,X2,X3)) -> mark#(X1)
p28: mark#(U11(X1,X2,X3)) -> active#(U11(mark(X1),X2,X3))

and R consists of:

r1: active(U11(tt(),V1,V2)) -> mark(U12(isNat(V1),V2))
r2: active(U12(tt(),V2)) -> mark(U13(isNat(V2)))
r3: active(U13(tt())) -> mark(tt())
r4: active(U21(tt(),V1)) -> mark(U22(isNat(V1)))
r5: active(U22(tt())) -> mark(tt())
r6: active(U31(tt(),N)) -> mark(N)
r7: active(U41(tt(),M,N)) -> mark(s(plus(N,M)))
r8: active(and(tt(),X)) -> mark(X)
r9: active(isNat(|0|())) -> mark(tt())
r10: active(isNat(plus(V1,V2))) -> mark(U11(and(isNatKind(V1),isNatKind(V2)),V1,V2))
r11: active(isNat(s(V1))) -> mark(U21(isNatKind(V1),V1))
r12: active(isNatKind(|0|())) -> mark(tt())
r13: active(isNatKind(plus(V1,V2))) -> mark(and(isNatKind(V1),isNatKind(V2)))
r14: active(isNatKind(s(V1))) -> mark(isNatKind(V1))
r15: active(plus(N,|0|())) -> mark(U31(and(isNat(N),isNatKind(N)),N))
r16: active(plus(N,s(M))) -> mark(U41(and(and(isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N))
r17: mark(U11(X1,X2,X3)) -> active(U11(mark(X1),X2,X3))
r18: mark(tt()) -> active(tt())
r19: mark(U12(X1,X2)) -> active(U12(mark(X1),X2))
r20: mark(isNat(X)) -> active(isNat(X))
r21: mark(U13(X)) -> active(U13(mark(X)))
r22: mark(U21(X1,X2)) -> active(U21(mark(X1),X2))
r23: mark(U22(X)) -> active(U22(mark(X)))
r24: mark(U31(X1,X2)) -> active(U31(mark(X1),X2))
r25: mark(U41(X1,X2,X3)) -> active(U41(mark(X1),X2,X3))
r26: mark(s(X)) -> active(s(mark(X)))
r27: mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2)))
r28: mark(and(X1,X2)) -> active(and(mark(X1),X2))
r29: mark(|0|()) -> active(|0|())
r30: mark(isNatKind(X)) -> active(isNatKind(X))
r31: U11(mark(X1),X2,X3) -> U11(X1,X2,X3)
r32: U11(X1,mark(X2),X3) -> U11(X1,X2,X3)
r33: U11(X1,X2,mark(X3)) -> U11(X1,X2,X3)
r34: U11(active(X1),X2,X3) -> U11(X1,X2,X3)
r35: U11(X1,active(X2),X3) -> U11(X1,X2,X3)
r36: U11(X1,X2,active(X3)) -> U11(X1,X2,X3)
r37: U12(mark(X1),X2) -> U12(X1,X2)
r38: U12(X1,mark(X2)) -> U12(X1,X2)
r39: U12(active(X1),X2) -> U12(X1,X2)
r40: U12(X1,active(X2)) -> U12(X1,X2)
r41: isNat(mark(X)) -> isNat(X)
r42: isNat(active(X)) -> isNat(X)
r43: U13(mark(X)) -> U13(X)
r44: U13(active(X)) -> U13(X)
r45: U21(mark(X1),X2) -> U21(X1,X2)
r46: U21(X1,mark(X2)) -> U21(X1,X2)
r47: U21(active(X1),X2) -> U21(X1,X2)
r48: U21(X1,active(X2)) -> U21(X1,X2)
r49: U22(mark(X)) -> U22(X)
r50: U22(active(X)) -> U22(X)
r51: U31(mark(X1),X2) -> U31(X1,X2)
r52: U31(X1,mark(X2)) -> U31(X1,X2)
r53: U31(active(X1),X2) -> U31(X1,X2)
r54: U31(X1,active(X2)) -> U31(X1,X2)
r55: U41(mark(X1),X2,X3) -> U41(X1,X2,X3)
r56: U41(X1,mark(X2),X3) -> U41(X1,X2,X3)
r57: U41(X1,X2,mark(X3)) -> U41(X1,X2,X3)
r58: U41(active(X1),X2,X3) -> U41(X1,X2,X3)
r59: U41(X1,active(X2),X3) -> U41(X1,X2,X3)
r60: U41(X1,X2,active(X3)) -> U41(X1,X2,X3)
r61: s(mark(X)) -> s(X)
r62: s(active(X)) -> s(X)
r63: plus(mark(X1),X2) -> plus(X1,X2)
r64: plus(X1,mark(X2)) -> plus(X1,X2)
r65: plus(active(X1),X2) -> plus(X1,X2)
r66: plus(X1,active(X2)) -> plus(X1,X2)
r67: and(mark(X1),X2) -> and(X1,X2)
r68: and(X1,mark(X2)) -> and(X1,X2)
r69: and(active(X1),X2) -> and(X1,X2)
r70: and(X1,active(X2)) -> and(X1,X2)
r71: isNatKind(mark(X)) -> isNatKind(X)
r72: isNatKind(active(X)) -> isNatKind(X)

The estimated dependency graph contains the following SCCs:

  {p1, p2, p3, p4, p5, p6, p7, p8, p9, p10, p11, p12, p13, p14, p15, p16, p17, p18, p19, p20, p21, p22, p23, p24, p25, p26, p27, p28}


-- Reduction pair.

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

p1: active#(U11(tt(),V1,V2)) -> mark#(U12(isNat(V1),V2))
p2: mark#(U11(X1,X2,X3)) -> active#(U11(mark(X1),X2,X3))
p3: active#(U12(tt(),V2)) -> mark#(U13(isNat(V2)))
p4: mark#(U11(X1,X2,X3)) -> mark#(X1)
p5: mark#(U12(X1,X2)) -> active#(U12(mark(X1),X2))
p6: active#(U21(tt(),V1)) -> mark#(U22(isNat(V1)))
p7: mark#(U12(X1,X2)) -> mark#(X1)
p8: mark#(isNat(X)) -> active#(isNat(X))
p9: active#(U41(tt(),M,N)) -> mark#(s(plus(N,M)))
p10: mark#(U13(X)) -> active#(U13(mark(X)))
p11: active#(and(tt(),X)) -> mark#(X)
p12: mark#(U13(X)) -> mark#(X)
p13: mark#(U21(X1,X2)) -> active#(U21(mark(X1),X2))
p14: active#(isNat(plus(V1,V2))) -> mark#(U11(and(isNatKind(V1),isNatKind(V2)),V1,V2))
p15: mark#(U21(X1,X2)) -> mark#(X1)
p16: mark#(U22(X)) -> active#(U22(mark(X)))
p17: active#(isNat(s(V1))) -> mark#(U21(isNatKind(V1),V1))
p18: mark#(U22(X)) -> mark#(X)
p19: mark#(U31(X1,X2)) -> active#(U31(mark(X1),X2))
p20: active#(isNatKind(plus(V1,V2))) -> mark#(and(isNatKind(V1),isNatKind(V2)))
p21: mark#(U41(X1,X2,X3)) -> active#(U41(mark(X1),X2,X3))
p22: active#(isNatKind(s(V1))) -> mark#(isNatKind(V1))
p23: mark#(s(X)) -> active#(s(mark(X)))
p24: active#(plus(N,s(M))) -> mark#(U41(and(and(isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N))
p25: mark#(plus(X1,X2)) -> active#(plus(mark(X1),mark(X2)))
p26: mark#(and(X1,X2)) -> active#(and(mark(X1),X2))
p27: mark#(and(X1,X2)) -> mark#(X1)
p28: mark#(isNatKind(X)) -> active#(isNatKind(X))

and R consists of:

r1: active(U11(tt(),V1,V2)) -> mark(U12(isNat(V1),V2))
r2: active(U12(tt(),V2)) -> mark(U13(isNat(V2)))
r3: active(U13(tt())) -> mark(tt())
r4: active(U21(tt(),V1)) -> mark(U22(isNat(V1)))
r5: active(U22(tt())) -> mark(tt())
r6: active(U31(tt(),N)) -> mark(N)
r7: active(U41(tt(),M,N)) -> mark(s(plus(N,M)))
r8: active(and(tt(),X)) -> mark(X)
r9: active(isNat(|0|())) -> mark(tt())
r10: active(isNat(plus(V1,V2))) -> mark(U11(and(isNatKind(V1),isNatKind(V2)),V1,V2))
r11: active(isNat(s(V1))) -> mark(U21(isNatKind(V1),V1))
r12: active(isNatKind(|0|())) -> mark(tt())
r13: active(isNatKind(plus(V1,V2))) -> mark(and(isNatKind(V1),isNatKind(V2)))
r14: active(isNatKind(s(V1))) -> mark(isNatKind(V1))
r15: active(plus(N,|0|())) -> mark(U31(and(isNat(N),isNatKind(N)),N))
r16: active(plus(N,s(M))) -> mark(U41(and(and(isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N))
r17: mark(U11(X1,X2,X3)) -> active(U11(mark(X1),X2,X3))
r18: mark(tt()) -> active(tt())
r19: mark(U12(X1,X2)) -> active(U12(mark(X1),X2))
r20: mark(isNat(X)) -> active(isNat(X))
r21: mark(U13(X)) -> active(U13(mark(X)))
r22: mark(U21(X1,X2)) -> active(U21(mark(X1),X2))
r23: mark(U22(X)) -> active(U22(mark(X)))
r24: mark(U31(X1,X2)) -> active(U31(mark(X1),X2))
r25: mark(U41(X1,X2,X3)) -> active(U41(mark(X1),X2,X3))
r26: mark(s(X)) -> active(s(mark(X)))
r27: mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2)))
r28: mark(and(X1,X2)) -> active(and(mark(X1),X2))
r29: mark(|0|()) -> active(|0|())
r30: mark(isNatKind(X)) -> active(isNatKind(X))
r31: U11(mark(X1),X2,X3) -> U11(X1,X2,X3)
r32: U11(X1,mark(X2),X3) -> U11(X1,X2,X3)
r33: U11(X1,X2,mark(X3)) -> U11(X1,X2,X3)
r34: U11(active(X1),X2,X3) -> U11(X1,X2,X3)
r35: U11(X1,active(X2),X3) -> U11(X1,X2,X3)
r36: U11(X1,X2,active(X3)) -> U11(X1,X2,X3)
r37: U12(mark(X1),X2) -> U12(X1,X2)
r38: U12(X1,mark(X2)) -> U12(X1,X2)
r39: U12(active(X1),X2) -> U12(X1,X2)
r40: U12(X1,active(X2)) -> U12(X1,X2)
r41: isNat(mark(X)) -> isNat(X)
r42: isNat(active(X)) -> isNat(X)
r43: U13(mark(X)) -> U13(X)
r44: U13(active(X)) -> U13(X)
r45: U21(mark(X1),X2) -> U21(X1,X2)
r46: U21(X1,mark(X2)) -> U21(X1,X2)
r47: U21(active(X1),X2) -> U21(X1,X2)
r48: U21(X1,active(X2)) -> U21(X1,X2)
r49: U22(mark(X)) -> U22(X)
r50: U22(active(X)) -> U22(X)
r51: U31(mark(X1),X2) -> U31(X1,X2)
r52: U31(X1,mark(X2)) -> U31(X1,X2)
r53: U31(active(X1),X2) -> U31(X1,X2)
r54: U31(X1,active(X2)) -> U31(X1,X2)
r55: U41(mark(X1),X2,X3) -> U41(X1,X2,X3)
r56: U41(X1,mark(X2),X3) -> U41(X1,X2,X3)
r57: U41(X1,X2,mark(X3)) -> U41(X1,X2,X3)
r58: U41(active(X1),X2,X3) -> U41(X1,X2,X3)
r59: U41(X1,active(X2),X3) -> U41(X1,X2,X3)
r60: U41(X1,X2,active(X3)) -> U41(X1,X2,X3)
r61: s(mark(X)) -> s(X)
r62: s(active(X)) -> s(X)
r63: plus(mark(X1),X2) -> plus(X1,X2)
r64: plus(X1,mark(X2)) -> plus(X1,X2)
r65: plus(active(X1),X2) -> plus(X1,X2)
r66: plus(X1,active(X2)) -> plus(X1,X2)
r67: and(mark(X1),X2) -> and(X1,X2)
r68: and(X1,mark(X2)) -> and(X1,X2)
r69: and(active(X1),X2) -> and(X1,X2)
r70: and(X1,active(X2)) -> and(X1,X2)
r71: isNatKind(mark(X)) -> isNatKind(X)
r72: isNatKind(active(X)) -> isNatKind(X)

The set of usable rules consists of

  r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r12, r13, r14, r15, r16, r17, r18, r19, r20, r21, r22, r23, r24, r25, r26, r27, r28, r29, r30, r31, r32, r33, 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, r72

Take the reduction pair:

  matrix interpretations:
  
    carrier: N^3
    order: lexicographic order
    interpretations:
      active#_A(x1) = ((0,0,0),(0,0,0),(1,0,0)) x1
      U11_A(x1,x2,x3) = (2,1,1)
      tt_A() = (1,1,1)
      mark#_A(x1) = (0,0,2)
      U12_A(x1,x2) = (2,1,1)
      isNat_A(x1) = (2,1,1)
      mark_A(x1) = (1,1,1)
      U13_A(x1) = (1,1,1)
      U21_A(x1,x2) = (2,1,1)
      U22_A(x1) = (1,1,1)
      U41_A(x1,x2,x3) = (2,1,1)
      s_A(x1) = (1,1,1)
      plus_A(x1,x2) = (2,0,1)
      and_A(x1,x2) = (2,1,1)
      isNatKind_A(x1) = (2,1,1)
      U31_A(x1,x2) = (1,1,1)
      active_A(x1) = (1,1,1)
      |0|_A() = (1,1,1)

The next rules are strictly ordered:

  p10, p16, p19, p23

We remove them from the problem.

-- SCC decomposition.

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

p1: active#(U11(tt(),V1,V2)) -> mark#(U12(isNat(V1),V2))
p2: mark#(U11(X1,X2,X3)) -> active#(U11(mark(X1),X2,X3))
p3: active#(U12(tt(),V2)) -> mark#(U13(isNat(V2)))
p4: mark#(U11(X1,X2,X3)) -> mark#(X1)
p5: mark#(U12(X1,X2)) -> active#(U12(mark(X1),X2))
p6: active#(U21(tt(),V1)) -> mark#(U22(isNat(V1)))
p7: mark#(U12(X1,X2)) -> mark#(X1)
p8: mark#(isNat(X)) -> active#(isNat(X))
p9: active#(U41(tt(),M,N)) -> mark#(s(plus(N,M)))
p10: active#(and(tt(),X)) -> mark#(X)
p11: mark#(U13(X)) -> mark#(X)
p12: mark#(U21(X1,X2)) -> active#(U21(mark(X1),X2))
p13: active#(isNat(plus(V1,V2))) -> mark#(U11(and(isNatKind(V1),isNatKind(V2)),V1,V2))
p14: mark#(U21(X1,X2)) -> mark#(X1)
p15: active#(isNat(s(V1))) -> mark#(U21(isNatKind(V1),V1))
p16: mark#(U22(X)) -> mark#(X)
p17: active#(isNatKind(plus(V1,V2))) -> mark#(and(isNatKind(V1),isNatKind(V2)))
p18: mark#(U41(X1,X2,X3)) -> active#(U41(mark(X1),X2,X3))
p19: active#(isNatKind(s(V1))) -> mark#(isNatKind(V1))
p20: active#(plus(N,s(M))) -> mark#(U41(and(and(isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N))
p21: mark#(plus(X1,X2)) -> active#(plus(mark(X1),mark(X2)))
p22: mark#(and(X1,X2)) -> active#(and(mark(X1),X2))
p23: mark#(and(X1,X2)) -> mark#(X1)
p24: mark#(isNatKind(X)) -> active#(isNatKind(X))

and R consists of:

r1: active(U11(tt(),V1,V2)) -> mark(U12(isNat(V1),V2))
r2: active(U12(tt(),V2)) -> mark(U13(isNat(V2)))
r3: active(U13(tt())) -> mark(tt())
r4: active(U21(tt(),V1)) -> mark(U22(isNat(V1)))
r5: active(U22(tt())) -> mark(tt())
r6: active(U31(tt(),N)) -> mark(N)
r7: active(U41(tt(),M,N)) -> mark(s(plus(N,M)))
r8: active(and(tt(),X)) -> mark(X)
r9: active(isNat(|0|())) -> mark(tt())
r10: active(isNat(plus(V1,V2))) -> mark(U11(and(isNatKind(V1),isNatKind(V2)),V1,V2))
r11: active(isNat(s(V1))) -> mark(U21(isNatKind(V1),V1))
r12: active(isNatKind(|0|())) -> mark(tt())
r13: active(isNatKind(plus(V1,V2))) -> mark(and(isNatKind(V1),isNatKind(V2)))
r14: active(isNatKind(s(V1))) -> mark(isNatKind(V1))
r15: active(plus(N,|0|())) -> mark(U31(and(isNat(N),isNatKind(N)),N))
r16: active(plus(N,s(M))) -> mark(U41(and(and(isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N))
r17: mark(U11(X1,X2,X3)) -> active(U11(mark(X1),X2,X3))
r18: mark(tt()) -> active(tt())
r19: mark(U12(X1,X2)) -> active(U12(mark(X1),X2))
r20: mark(isNat(X)) -> active(isNat(X))
r21: mark(U13(X)) -> active(U13(mark(X)))
r22: mark(U21(X1,X2)) -> active(U21(mark(X1),X2))
r23: mark(U22(X)) -> active(U22(mark(X)))
r24: mark(U31(X1,X2)) -> active(U31(mark(X1),X2))
r25: mark(U41(X1,X2,X3)) -> active(U41(mark(X1),X2,X3))
r26: mark(s(X)) -> active(s(mark(X)))
r27: mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2)))
r28: mark(and(X1,X2)) -> active(and(mark(X1),X2))
r29: mark(|0|()) -> active(|0|())
r30: mark(isNatKind(X)) -> active(isNatKind(X))
r31: U11(mark(X1),X2,X3) -> U11(X1,X2,X3)
r32: U11(X1,mark(X2),X3) -> U11(X1,X2,X3)
r33: U11(X1,X2,mark(X3)) -> U11(X1,X2,X3)
r34: U11(active(X1),X2,X3) -> U11(X1,X2,X3)
r35: U11(X1,active(X2),X3) -> U11(X1,X2,X3)
r36: U11(X1,X2,active(X3)) -> U11(X1,X2,X3)
r37: U12(mark(X1),X2) -> U12(X1,X2)
r38: U12(X1,mark(X2)) -> U12(X1,X2)
r39: U12(active(X1),X2) -> U12(X1,X2)
r40: U12(X1,active(X2)) -> U12(X1,X2)
r41: isNat(mark(X)) -> isNat(X)
r42: isNat(active(X)) -> isNat(X)
r43: U13(mark(X)) -> U13(X)
r44: U13(active(X)) -> U13(X)
r45: U21(mark(X1),X2) -> U21(X1,X2)
r46: U21(X1,mark(X2)) -> U21(X1,X2)
r47: U21(active(X1),X2) -> U21(X1,X2)
r48: U21(X1,active(X2)) -> U21(X1,X2)
r49: U22(mark(X)) -> U22(X)
r50: U22(active(X)) -> U22(X)
r51: U31(mark(X1),X2) -> U31(X1,X2)
r52: U31(X1,mark(X2)) -> U31(X1,X2)
r53: U31(active(X1),X2) -> U31(X1,X2)
r54: U31(X1,active(X2)) -> U31(X1,X2)
r55: U41(mark(X1),X2,X3) -> U41(X1,X2,X3)
r56: U41(X1,mark(X2),X3) -> U41(X1,X2,X3)
r57: U41(X1,X2,mark(X3)) -> U41(X1,X2,X3)
r58: U41(active(X1),X2,X3) -> U41(X1,X2,X3)
r59: U41(X1,active(X2),X3) -> U41(X1,X2,X3)
r60: U41(X1,X2,active(X3)) -> U41(X1,X2,X3)
r61: s(mark(X)) -> s(X)
r62: s(active(X)) -> s(X)
r63: plus(mark(X1),X2) -> plus(X1,X2)
r64: plus(X1,mark(X2)) -> plus(X1,X2)
r65: plus(active(X1),X2) -> plus(X1,X2)
r66: plus(X1,active(X2)) -> plus(X1,X2)
r67: and(mark(X1),X2) -> and(X1,X2)
r68: and(X1,mark(X2)) -> and(X1,X2)
r69: and(active(X1),X2) -> and(X1,X2)
r70: and(X1,active(X2)) -> and(X1,X2)
r71: isNatKind(mark(X)) -> isNatKind(X)
r72: isNatKind(active(X)) -> isNatKind(X)

The estimated dependency graph contains the following SCCs:

  {p1, p2, p3, p4, p5, p6, p7, p8, p9, p10, p11, p12, p13, p14, p15, p16, p17, p18, p19, p20, p21, p22, p23, p24}


-- Reduction pair.

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

p1: active#(U11(tt(),V1,V2)) -> mark#(U12(isNat(V1),V2))
p2: mark#(isNatKind(X)) -> active#(isNatKind(X))
p3: active#(plus(N,s(M))) -> mark#(U41(and(and(isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N))
p4: mark#(and(X1,X2)) -> mark#(X1)
p5: mark#(and(X1,X2)) -> active#(and(mark(X1),X2))
p6: active#(isNatKind(s(V1))) -> mark#(isNatKind(V1))
p7: mark#(plus(X1,X2)) -> active#(plus(mark(X1),mark(X2)))
p8: active#(isNatKind(plus(V1,V2))) -> mark#(and(isNatKind(V1),isNatKind(V2)))
p9: mark#(U41(X1,X2,X3)) -> active#(U41(mark(X1),X2,X3))
p10: active#(isNat(s(V1))) -> mark#(U21(isNatKind(V1),V1))
p11: mark#(U22(X)) -> mark#(X)
p12: mark#(U21(X1,X2)) -> mark#(X1)
p13: mark#(U21(X1,X2)) -> active#(U21(mark(X1),X2))
p14: active#(isNat(plus(V1,V2))) -> mark#(U11(and(isNatKind(V1),isNatKind(V2)),V1,V2))
p15: mark#(U13(X)) -> mark#(X)
p16: mark#(isNat(X)) -> active#(isNat(X))
p17: active#(and(tt(),X)) -> mark#(X)
p18: mark#(U12(X1,X2)) -> mark#(X1)
p19: mark#(U12(X1,X2)) -> active#(U12(mark(X1),X2))
p20: active#(U41(tt(),M,N)) -> mark#(s(plus(N,M)))
p21: mark#(U11(X1,X2,X3)) -> mark#(X1)
p22: mark#(U11(X1,X2,X3)) -> active#(U11(mark(X1),X2,X3))
p23: active#(U21(tt(),V1)) -> mark#(U22(isNat(V1)))
p24: active#(U12(tt(),V2)) -> mark#(U13(isNat(V2)))

and R consists of:

r1: active(U11(tt(),V1,V2)) -> mark(U12(isNat(V1),V2))
r2: active(U12(tt(),V2)) -> mark(U13(isNat(V2)))
r3: active(U13(tt())) -> mark(tt())
r4: active(U21(tt(),V1)) -> mark(U22(isNat(V1)))
r5: active(U22(tt())) -> mark(tt())
r6: active(U31(tt(),N)) -> mark(N)
r7: active(U41(tt(),M,N)) -> mark(s(plus(N,M)))
r8: active(and(tt(),X)) -> mark(X)
r9: active(isNat(|0|())) -> mark(tt())
r10: active(isNat(plus(V1,V2))) -> mark(U11(and(isNatKind(V1),isNatKind(V2)),V1,V2))
r11: active(isNat(s(V1))) -> mark(U21(isNatKind(V1),V1))
r12: active(isNatKind(|0|())) -> mark(tt())
r13: active(isNatKind(plus(V1,V2))) -> mark(and(isNatKind(V1),isNatKind(V2)))
r14: active(isNatKind(s(V1))) -> mark(isNatKind(V1))
r15: active(plus(N,|0|())) -> mark(U31(and(isNat(N),isNatKind(N)),N))
r16: active(plus(N,s(M))) -> mark(U41(and(and(isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N))
r17: mark(U11(X1,X2,X3)) -> active(U11(mark(X1),X2,X3))
r18: mark(tt()) -> active(tt())
r19: mark(U12(X1,X2)) -> active(U12(mark(X1),X2))
r20: mark(isNat(X)) -> active(isNat(X))
r21: mark(U13(X)) -> active(U13(mark(X)))
r22: mark(U21(X1,X2)) -> active(U21(mark(X1),X2))
r23: mark(U22(X)) -> active(U22(mark(X)))
r24: mark(U31(X1,X2)) -> active(U31(mark(X1),X2))
r25: mark(U41(X1,X2,X3)) -> active(U41(mark(X1),X2,X3))
r26: mark(s(X)) -> active(s(mark(X)))
r27: mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2)))
r28: mark(and(X1,X2)) -> active(and(mark(X1),X2))
r29: mark(|0|()) -> active(|0|())
r30: mark(isNatKind(X)) -> active(isNatKind(X))
r31: U11(mark(X1),X2,X3) -> U11(X1,X2,X3)
r32: U11(X1,mark(X2),X3) -> U11(X1,X2,X3)
r33: U11(X1,X2,mark(X3)) -> U11(X1,X2,X3)
r34: U11(active(X1),X2,X3) -> U11(X1,X2,X3)
r35: U11(X1,active(X2),X3) -> U11(X1,X2,X3)
r36: U11(X1,X2,active(X3)) -> U11(X1,X2,X3)
r37: U12(mark(X1),X2) -> U12(X1,X2)
r38: U12(X1,mark(X2)) -> U12(X1,X2)
r39: U12(active(X1),X2) -> U12(X1,X2)
r40: U12(X1,active(X2)) -> U12(X1,X2)
r41: isNat(mark(X)) -> isNat(X)
r42: isNat(active(X)) -> isNat(X)
r43: U13(mark(X)) -> U13(X)
r44: U13(active(X)) -> U13(X)
r45: U21(mark(X1),X2) -> U21(X1,X2)
r46: U21(X1,mark(X2)) -> U21(X1,X2)
r47: U21(active(X1),X2) -> U21(X1,X2)
r48: U21(X1,active(X2)) -> U21(X1,X2)
r49: U22(mark(X)) -> U22(X)
r50: U22(active(X)) -> U22(X)
r51: U31(mark(X1),X2) -> U31(X1,X2)
r52: U31(X1,mark(X2)) -> U31(X1,X2)
r53: U31(active(X1),X2) -> U31(X1,X2)
r54: U31(X1,active(X2)) -> U31(X1,X2)
r55: U41(mark(X1),X2,X3) -> U41(X1,X2,X3)
r56: U41(X1,mark(X2),X3) -> U41(X1,X2,X3)
r57: U41(X1,X2,mark(X3)) -> U41(X1,X2,X3)
r58: U41(active(X1),X2,X3) -> U41(X1,X2,X3)
r59: U41(X1,active(X2),X3) -> U41(X1,X2,X3)
r60: U41(X1,X2,active(X3)) -> U41(X1,X2,X3)
r61: s(mark(X)) -> s(X)
r62: s(active(X)) -> s(X)
r63: plus(mark(X1),X2) -> plus(X1,X2)
r64: plus(X1,mark(X2)) -> plus(X1,X2)
r65: plus(active(X1),X2) -> plus(X1,X2)
r66: plus(X1,active(X2)) -> plus(X1,X2)
r67: and(mark(X1),X2) -> and(X1,X2)
r68: and(X1,mark(X2)) -> and(X1,X2)
r69: and(active(X1),X2) -> and(X1,X2)
r70: and(X1,active(X2)) -> and(X1,X2)
r71: isNatKind(mark(X)) -> isNatKind(X)
r72: isNatKind(active(X)) -> isNatKind(X)

The set of usable rules consists of

  r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r12, r13, r14, r15, r16, r17, r18, r19, r20, r21, r22, r23, r24, r25, r26, r27, r28, r29, r30, r31, r32, r33, 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, r72

Take the reduction pair:

  matrix interpretations:
  
    carrier: N^3
    order: lexicographic order
    interpretations:
      active#_A(x1) = ((1,0,0),(1,1,0),(0,0,1)) x1
      U11_A(x1,x2,x3) = ((1,0,0),(0,1,0),(1,0,0)) x1 + ((1,0,0),(0,1,0),(1,0,0)) x2 + ((1,0,0),(1,1,0),(1,0,0)) x3
      tt_A() = (0,5,1)
      mark#_A(x1) = ((1,0,0),(1,1,0),(1,0,0)) x1 + (0,2,2)
      U12_A(x1,x2) = x1 + ((1,0,0),(1,1,0),(1,0,0)) x2 + (0,1,3)
      isNat_A(x1) = ((1,0,0),(0,1,0),(1,0,0)) x1 + (0,1,1)
      isNatKind_A(x1) = ((0,0,0),(1,0,0),(0,0,0)) x1 + (0,8,0)
      plus_A(x1,x2) = ((1,0,0),(1,0,0),(0,1,0)) x1 + x2 + (12,6,1)
      s_A(x1) = x1 + (3,7,1)
      U41_A(x1,x2,x3) = ((1,0,0),(0,0,0),(1,0,0)) x2 + ((1,0,0),(1,0,0),(0,0,0)) x3 + (15,10,18)
      and_A(x1,x2) = ((1,0,0),(0,1,0),(1,0,0)) x1 + ((1,0,0),(1,1,0),(1,1,0)) x2 + (0,1,0)
      mark_A(x1) = ((1,0,0),(0,1,0),(1,0,1)) x1 + (0,1,2)
      U21_A(x1,x2) = x1 + ((1,0,0),(1,0,0),(1,0,0)) x2 + (1,0,1)
      U22_A(x1) = x1 + (1,2,1)
      U13_A(x1) = x1 + (0,3,1)
      active_A(x1) = x1 + (0,0,1)
      U31_A(x1,x2) = ((0,0,0),(1,0,0),(0,1,0)) x1 + ((1,0,0),(1,1,0),(0,1,0)) x2 + (1,6,1)
      |0|_A() = (1,0,1)

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, p22, p23, p24

We remove them from the problem.

-- SCC decomposition.

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

p1: mark#(U11(X1,X2,X3)) -> mark#(X1)

and R consists of:

r1: active(U11(tt(),V1,V2)) -> mark(U12(isNat(V1),V2))
r2: active(U12(tt(),V2)) -> mark(U13(isNat(V2)))
r3: active(U13(tt())) -> mark(tt())
r4: active(U21(tt(),V1)) -> mark(U22(isNat(V1)))
r5: active(U22(tt())) -> mark(tt())
r6: active(U31(tt(),N)) -> mark(N)
r7: active(U41(tt(),M,N)) -> mark(s(plus(N,M)))
r8: active(and(tt(),X)) -> mark(X)
r9: active(isNat(|0|())) -> mark(tt())
r10: active(isNat(plus(V1,V2))) -> mark(U11(and(isNatKind(V1),isNatKind(V2)),V1,V2))
r11: active(isNat(s(V1))) -> mark(U21(isNatKind(V1),V1))
r12: active(isNatKind(|0|())) -> mark(tt())
r13: active(isNatKind(plus(V1,V2))) -> mark(and(isNatKind(V1),isNatKind(V2)))
r14: active(isNatKind(s(V1))) -> mark(isNatKind(V1))
r15: active(plus(N,|0|())) -> mark(U31(and(isNat(N),isNatKind(N)),N))
r16: active(plus(N,s(M))) -> mark(U41(and(and(isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N))
r17: mark(U11(X1,X2,X3)) -> active(U11(mark(X1),X2,X3))
r18: mark(tt()) -> active(tt())
r19: mark(U12(X1,X2)) -> active(U12(mark(X1),X2))
r20: mark(isNat(X)) -> active(isNat(X))
r21: mark(U13(X)) -> active(U13(mark(X)))
r22: mark(U21(X1,X2)) -> active(U21(mark(X1),X2))
r23: mark(U22(X)) -> active(U22(mark(X)))
r24: mark(U31(X1,X2)) -> active(U31(mark(X1),X2))
r25: mark(U41(X1,X2,X3)) -> active(U41(mark(X1),X2,X3))
r26: mark(s(X)) -> active(s(mark(X)))
r27: mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2)))
r28: mark(and(X1,X2)) -> active(and(mark(X1),X2))
r29: mark(|0|()) -> active(|0|())
r30: mark(isNatKind(X)) -> active(isNatKind(X))
r31: U11(mark(X1),X2,X3) -> U11(X1,X2,X3)
r32: U11(X1,mark(X2),X3) -> U11(X1,X2,X3)
r33: U11(X1,X2,mark(X3)) -> U11(X1,X2,X3)
r34: U11(active(X1),X2,X3) -> U11(X1,X2,X3)
r35: U11(X1,active(X2),X3) -> U11(X1,X2,X3)
r36: U11(X1,X2,active(X3)) -> U11(X1,X2,X3)
r37: U12(mark(X1),X2) -> U12(X1,X2)
r38: U12(X1,mark(X2)) -> U12(X1,X2)
r39: U12(active(X1),X2) -> U12(X1,X2)
r40: U12(X1,active(X2)) -> U12(X1,X2)
r41: isNat(mark(X)) -> isNat(X)
r42: isNat(active(X)) -> isNat(X)
r43: U13(mark(X)) -> U13(X)
r44: U13(active(X)) -> U13(X)
r45: U21(mark(X1),X2) -> U21(X1,X2)
r46: U21(X1,mark(X2)) -> U21(X1,X2)
r47: U21(active(X1),X2) -> U21(X1,X2)
r48: U21(X1,active(X2)) -> U21(X1,X2)
r49: U22(mark(X)) -> U22(X)
r50: U22(active(X)) -> U22(X)
r51: U31(mark(X1),X2) -> U31(X1,X2)
r52: U31(X1,mark(X2)) -> U31(X1,X2)
r53: U31(active(X1),X2) -> U31(X1,X2)
r54: U31(X1,active(X2)) -> U31(X1,X2)
r55: U41(mark(X1),X2,X3) -> U41(X1,X2,X3)
r56: U41(X1,mark(X2),X3) -> U41(X1,X2,X3)
r57: U41(X1,X2,mark(X3)) -> U41(X1,X2,X3)
r58: U41(active(X1),X2,X3) -> U41(X1,X2,X3)
r59: U41(X1,active(X2),X3) -> U41(X1,X2,X3)
r60: U41(X1,X2,active(X3)) -> U41(X1,X2,X3)
r61: s(mark(X)) -> s(X)
r62: s(active(X)) -> s(X)
r63: plus(mark(X1),X2) -> plus(X1,X2)
r64: plus(X1,mark(X2)) -> plus(X1,X2)
r65: plus(active(X1),X2) -> plus(X1,X2)
r66: plus(X1,active(X2)) -> plus(X1,X2)
r67: and(mark(X1),X2) -> and(X1,X2)
r68: and(X1,mark(X2)) -> and(X1,X2)
r69: and(active(X1),X2) -> and(X1,X2)
r70: and(X1,active(X2)) -> and(X1,X2)
r71: isNatKind(mark(X)) -> isNatKind(X)
r72: isNatKind(active(X)) -> isNatKind(X)

The estimated dependency graph contains the following SCCs:

  {p1}


-- Reduction pair.

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

p1: mark#(U11(X1,X2,X3)) -> mark#(X1)

and R consists of:

r1: active(U11(tt(),V1,V2)) -> mark(U12(isNat(V1),V2))
r2: active(U12(tt(),V2)) -> mark(U13(isNat(V2)))
r3: active(U13(tt())) -> mark(tt())
r4: active(U21(tt(),V1)) -> mark(U22(isNat(V1)))
r5: active(U22(tt())) -> mark(tt())
r6: active(U31(tt(),N)) -> mark(N)
r7: active(U41(tt(),M,N)) -> mark(s(plus(N,M)))
r8: active(and(tt(),X)) -> mark(X)
r9: active(isNat(|0|())) -> mark(tt())
r10: active(isNat(plus(V1,V2))) -> mark(U11(and(isNatKind(V1),isNatKind(V2)),V1,V2))
r11: active(isNat(s(V1))) -> mark(U21(isNatKind(V1),V1))
r12: active(isNatKind(|0|())) -> mark(tt())
r13: active(isNatKind(plus(V1,V2))) -> mark(and(isNatKind(V1),isNatKind(V2)))
r14: active(isNatKind(s(V1))) -> mark(isNatKind(V1))
r15: active(plus(N,|0|())) -> mark(U31(and(isNat(N),isNatKind(N)),N))
r16: active(plus(N,s(M))) -> mark(U41(and(and(isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N))
r17: mark(U11(X1,X2,X3)) -> active(U11(mark(X1),X2,X3))
r18: mark(tt()) -> active(tt())
r19: mark(U12(X1,X2)) -> active(U12(mark(X1),X2))
r20: mark(isNat(X)) -> active(isNat(X))
r21: mark(U13(X)) -> active(U13(mark(X)))
r22: mark(U21(X1,X2)) -> active(U21(mark(X1),X2))
r23: mark(U22(X)) -> active(U22(mark(X)))
r24: mark(U31(X1,X2)) -> active(U31(mark(X1),X2))
r25: mark(U41(X1,X2,X3)) -> active(U41(mark(X1),X2,X3))
r26: mark(s(X)) -> active(s(mark(X)))
r27: mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2)))
r28: mark(and(X1,X2)) -> active(and(mark(X1),X2))
r29: mark(|0|()) -> active(|0|())
r30: mark(isNatKind(X)) -> active(isNatKind(X))
r31: U11(mark(X1),X2,X3) -> U11(X1,X2,X3)
r32: U11(X1,mark(X2),X3) -> U11(X1,X2,X3)
r33: U11(X1,X2,mark(X3)) -> U11(X1,X2,X3)
r34: U11(active(X1),X2,X3) -> U11(X1,X2,X3)
r35: U11(X1,active(X2),X3) -> U11(X1,X2,X3)
r36: U11(X1,X2,active(X3)) -> U11(X1,X2,X3)
r37: U12(mark(X1),X2) -> U12(X1,X2)
r38: U12(X1,mark(X2)) -> U12(X1,X2)
r39: U12(active(X1),X2) -> U12(X1,X2)
r40: U12(X1,active(X2)) -> U12(X1,X2)
r41: isNat(mark(X)) -> isNat(X)
r42: isNat(active(X)) -> isNat(X)
r43: U13(mark(X)) -> U13(X)
r44: U13(active(X)) -> U13(X)
r45: U21(mark(X1),X2) -> U21(X1,X2)
r46: U21(X1,mark(X2)) -> U21(X1,X2)
r47: U21(active(X1),X2) -> U21(X1,X2)
r48: U21(X1,active(X2)) -> U21(X1,X2)
r49: U22(mark(X)) -> U22(X)
r50: U22(active(X)) -> U22(X)
r51: U31(mark(X1),X2) -> U31(X1,X2)
r52: U31(X1,mark(X2)) -> U31(X1,X2)
r53: U31(active(X1),X2) -> U31(X1,X2)
r54: U31(X1,active(X2)) -> U31(X1,X2)
r55: U41(mark(X1),X2,X3) -> U41(X1,X2,X3)
r56: U41(X1,mark(X2),X3) -> U41(X1,X2,X3)
r57: U41(X1,X2,mark(X3)) -> U41(X1,X2,X3)
r58: U41(active(X1),X2,X3) -> U41(X1,X2,X3)
r59: U41(X1,active(X2),X3) -> U41(X1,X2,X3)
r60: U41(X1,X2,active(X3)) -> U41(X1,X2,X3)
r61: s(mark(X)) -> s(X)
r62: s(active(X)) -> s(X)
r63: plus(mark(X1),X2) -> plus(X1,X2)
r64: plus(X1,mark(X2)) -> plus(X1,X2)
r65: plus(active(X1),X2) -> plus(X1,X2)
r66: plus(X1,active(X2)) -> plus(X1,X2)
r67: and(mark(X1),X2) -> and(X1,X2)
r68: and(X1,mark(X2)) -> and(X1,X2)
r69: and(active(X1),X2) -> and(X1,X2)
r70: and(X1,active(X2)) -> and(X1,X2)
r71: isNatKind(mark(X)) -> isNatKind(X)
r72: isNatKind(active(X)) -> isNatKind(X)

The set of usable rules consists of

  (no rules)

Take the monotone reduction pair:

  matrix interpretations:
  
    carrier: N^3
    order: lexicographic order
    interpretations:
      mark#_A(x1) = ((1,0,0),(0,1,0),(1,1,1)) x1
      U11_A(x1,x2,x3) = ((1,0,0),(1,1,0),(1,1,1)) x1 + ((1,0,0),(1,1,0),(1,1,1)) x2 + ((1,0,0),(1,1,0),(1,1,1)) x3 + (1,1,1)

The next rules are strictly ordered:

  p1
  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, r72

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: U12#(mark(X1),X2) -> U12#(X1,X2)
p2: U12#(X1,active(X2)) -> U12#(X1,X2)
p3: U12#(active(X1),X2) -> U12#(X1,X2)
p4: U12#(X1,mark(X2)) -> U12#(X1,X2)

and R consists of:

r1: active(U11(tt(),V1,V2)) -> mark(U12(isNat(V1),V2))
r2: active(U12(tt(),V2)) -> mark(U13(isNat(V2)))
r3: active(U13(tt())) -> mark(tt())
r4: active(U21(tt(),V1)) -> mark(U22(isNat(V1)))
r5: active(U22(tt())) -> mark(tt())
r6: active(U31(tt(),N)) -> mark(N)
r7: active(U41(tt(),M,N)) -> mark(s(plus(N,M)))
r8: active(and(tt(),X)) -> mark(X)
r9: active(isNat(|0|())) -> mark(tt())
r10: active(isNat(plus(V1,V2))) -> mark(U11(and(isNatKind(V1),isNatKind(V2)),V1,V2))
r11: active(isNat(s(V1))) -> mark(U21(isNatKind(V1),V1))
r12: active(isNatKind(|0|())) -> mark(tt())
r13: active(isNatKind(plus(V1,V2))) -> mark(and(isNatKind(V1),isNatKind(V2)))
r14: active(isNatKind(s(V1))) -> mark(isNatKind(V1))
r15: active(plus(N,|0|())) -> mark(U31(and(isNat(N),isNatKind(N)),N))
r16: active(plus(N,s(M))) -> mark(U41(and(and(isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N))
r17: mark(U11(X1,X2,X3)) -> active(U11(mark(X1),X2,X3))
r18: mark(tt()) -> active(tt())
r19: mark(U12(X1,X2)) -> active(U12(mark(X1),X2))
r20: mark(isNat(X)) -> active(isNat(X))
r21: mark(U13(X)) -> active(U13(mark(X)))
r22: mark(U21(X1,X2)) -> active(U21(mark(X1),X2))
r23: mark(U22(X)) -> active(U22(mark(X)))
r24: mark(U31(X1,X2)) -> active(U31(mark(X1),X2))
r25: mark(U41(X1,X2,X3)) -> active(U41(mark(X1),X2,X3))
r26: mark(s(X)) -> active(s(mark(X)))
r27: mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2)))
r28: mark(and(X1,X2)) -> active(and(mark(X1),X2))
r29: mark(|0|()) -> active(|0|())
r30: mark(isNatKind(X)) -> active(isNatKind(X))
r31: U11(mark(X1),X2,X3) -> U11(X1,X2,X3)
r32: U11(X1,mark(X2),X3) -> U11(X1,X2,X3)
r33: U11(X1,X2,mark(X3)) -> U11(X1,X2,X3)
r34: U11(active(X1),X2,X3) -> U11(X1,X2,X3)
r35: U11(X1,active(X2),X3) -> U11(X1,X2,X3)
r36: U11(X1,X2,active(X3)) -> U11(X1,X2,X3)
r37: U12(mark(X1),X2) -> U12(X1,X2)
r38: U12(X1,mark(X2)) -> U12(X1,X2)
r39: U12(active(X1),X2) -> U12(X1,X2)
r40: U12(X1,active(X2)) -> U12(X1,X2)
r41: isNat(mark(X)) -> isNat(X)
r42: isNat(active(X)) -> isNat(X)
r43: U13(mark(X)) -> U13(X)
r44: U13(active(X)) -> U13(X)
r45: U21(mark(X1),X2) -> U21(X1,X2)
r46: U21(X1,mark(X2)) -> U21(X1,X2)
r47: U21(active(X1),X2) -> U21(X1,X2)
r48: U21(X1,active(X2)) -> U21(X1,X2)
r49: U22(mark(X)) -> U22(X)
r50: U22(active(X)) -> U22(X)
r51: U31(mark(X1),X2) -> U31(X1,X2)
r52: U31(X1,mark(X2)) -> U31(X1,X2)
r53: U31(active(X1),X2) -> U31(X1,X2)
r54: U31(X1,active(X2)) -> U31(X1,X2)
r55: U41(mark(X1),X2,X3) -> U41(X1,X2,X3)
r56: U41(X1,mark(X2),X3) -> U41(X1,X2,X3)
r57: U41(X1,X2,mark(X3)) -> U41(X1,X2,X3)
r58: U41(active(X1),X2,X3) -> U41(X1,X2,X3)
r59: U41(X1,active(X2),X3) -> U41(X1,X2,X3)
r60: U41(X1,X2,active(X3)) -> U41(X1,X2,X3)
r61: s(mark(X)) -> s(X)
r62: s(active(X)) -> s(X)
r63: plus(mark(X1),X2) -> plus(X1,X2)
r64: plus(X1,mark(X2)) -> plus(X1,X2)
r65: plus(active(X1),X2) -> plus(X1,X2)
r66: plus(X1,active(X2)) -> plus(X1,X2)
r67: and(mark(X1),X2) -> and(X1,X2)
r68: and(X1,mark(X2)) -> and(X1,X2)
r69: and(active(X1),X2) -> and(X1,X2)
r70: and(X1,active(X2)) -> and(X1,X2)
r71: isNatKind(mark(X)) -> isNatKind(X)
r72: isNatKind(active(X)) -> isNatKind(X)

The set of usable rules consists of

  (no rules)

Take the monotone reduction pair:

  matrix interpretations:
  
    carrier: N^3
    order: lexicographic order
    interpretations:
      U12#_A(x1,x2) = ((1,0,0),(0,1,0),(1,1,1)) x1 + ((1,0,0),(1,1,0),(1,1,1)) x2
      mark_A(x1) = ((1,0,0),(1,1,0),(1,1,1)) x1 + (1,1,1)
      active_A(x1) = ((1,0,0),(1,1,0),(1,1,1)) x1 + (1,1,1)

The next rules are strictly ordered:

  p1, p2, p3, p4
  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, r72

We remove them from the problem.  Then no dependency pair remains.

-- Reduction pair.

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

p1: isNat#(mark(X)) -> isNat#(X)
p2: isNat#(active(X)) -> isNat#(X)

and R consists of:

r1: active(U11(tt(),V1,V2)) -> mark(U12(isNat(V1),V2))
r2: active(U12(tt(),V2)) -> mark(U13(isNat(V2)))
r3: active(U13(tt())) -> mark(tt())
r4: active(U21(tt(),V1)) -> mark(U22(isNat(V1)))
r5: active(U22(tt())) -> mark(tt())
r6: active(U31(tt(),N)) -> mark(N)
r7: active(U41(tt(),M,N)) -> mark(s(plus(N,M)))
r8: active(and(tt(),X)) -> mark(X)
r9: active(isNat(|0|())) -> mark(tt())
r10: active(isNat(plus(V1,V2))) -> mark(U11(and(isNatKind(V1),isNatKind(V2)),V1,V2))
r11: active(isNat(s(V1))) -> mark(U21(isNatKind(V1),V1))
r12: active(isNatKind(|0|())) -> mark(tt())
r13: active(isNatKind(plus(V1,V2))) -> mark(and(isNatKind(V1),isNatKind(V2)))
r14: active(isNatKind(s(V1))) -> mark(isNatKind(V1))
r15: active(plus(N,|0|())) -> mark(U31(and(isNat(N),isNatKind(N)),N))
r16: active(plus(N,s(M))) -> mark(U41(and(and(isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N))
r17: mark(U11(X1,X2,X3)) -> active(U11(mark(X1),X2,X3))
r18: mark(tt()) -> active(tt())
r19: mark(U12(X1,X2)) -> active(U12(mark(X1),X2))
r20: mark(isNat(X)) -> active(isNat(X))
r21: mark(U13(X)) -> active(U13(mark(X)))
r22: mark(U21(X1,X2)) -> active(U21(mark(X1),X2))
r23: mark(U22(X)) -> active(U22(mark(X)))
r24: mark(U31(X1,X2)) -> active(U31(mark(X1),X2))
r25: mark(U41(X1,X2,X3)) -> active(U41(mark(X1),X2,X3))
r26: mark(s(X)) -> active(s(mark(X)))
r27: mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2)))
r28: mark(and(X1,X2)) -> active(and(mark(X1),X2))
r29: mark(|0|()) -> active(|0|())
r30: mark(isNatKind(X)) -> active(isNatKind(X))
r31: U11(mark(X1),X2,X3) -> U11(X1,X2,X3)
r32: U11(X1,mark(X2),X3) -> U11(X1,X2,X3)
r33: U11(X1,X2,mark(X3)) -> U11(X1,X2,X3)
r34: U11(active(X1),X2,X3) -> U11(X1,X2,X3)
r35: U11(X1,active(X2),X3) -> U11(X1,X2,X3)
r36: U11(X1,X2,active(X3)) -> U11(X1,X2,X3)
r37: U12(mark(X1),X2) -> U12(X1,X2)
r38: U12(X1,mark(X2)) -> U12(X1,X2)
r39: U12(active(X1),X2) -> U12(X1,X2)
r40: U12(X1,active(X2)) -> U12(X1,X2)
r41: isNat(mark(X)) -> isNat(X)
r42: isNat(active(X)) -> isNat(X)
r43: U13(mark(X)) -> U13(X)
r44: U13(active(X)) -> U13(X)
r45: U21(mark(X1),X2) -> U21(X1,X2)
r46: U21(X1,mark(X2)) -> U21(X1,X2)
r47: U21(active(X1),X2) -> U21(X1,X2)
r48: U21(X1,active(X2)) -> U21(X1,X2)
r49: U22(mark(X)) -> U22(X)
r50: U22(active(X)) -> U22(X)
r51: U31(mark(X1),X2) -> U31(X1,X2)
r52: U31(X1,mark(X2)) -> U31(X1,X2)
r53: U31(active(X1),X2) -> U31(X1,X2)
r54: U31(X1,active(X2)) -> U31(X1,X2)
r55: U41(mark(X1),X2,X3) -> U41(X1,X2,X3)
r56: U41(X1,mark(X2),X3) -> U41(X1,X2,X3)
r57: U41(X1,X2,mark(X3)) -> U41(X1,X2,X3)
r58: U41(active(X1),X2,X3) -> U41(X1,X2,X3)
r59: U41(X1,active(X2),X3) -> U41(X1,X2,X3)
r60: U41(X1,X2,active(X3)) -> U41(X1,X2,X3)
r61: s(mark(X)) -> s(X)
r62: s(active(X)) -> s(X)
r63: plus(mark(X1),X2) -> plus(X1,X2)
r64: plus(X1,mark(X2)) -> plus(X1,X2)
r65: plus(active(X1),X2) -> plus(X1,X2)
r66: plus(X1,active(X2)) -> plus(X1,X2)
r67: and(mark(X1),X2) -> and(X1,X2)
r68: and(X1,mark(X2)) -> and(X1,X2)
r69: and(active(X1),X2) -> and(X1,X2)
r70: and(X1,active(X2)) -> and(X1,X2)
r71: isNatKind(mark(X)) -> isNatKind(X)
r72: isNatKind(active(X)) -> isNatKind(X)

The set of usable rules consists of

  (no rules)

Take the monotone reduction pair:

  matrix interpretations:
  
    carrier: N^3
    order: lexicographic order
    interpretations:
      isNat#_A(x1) = ((1,0,0),(1,1,0),(1,1,1)) x1
      mark_A(x1) = ((1,0,0),(1,1,0),(1,1,1)) x1 + (1,1,1)
      active_A(x1) = ((1,0,0),(1,1,0),(1,1,1)) x1 + (1,1,1)

The next rules are strictly ordered:

  p1, p2
  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, r72

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: U13#(mark(X)) -> U13#(X)
p2: U13#(active(X)) -> U13#(X)

and R consists of:

r1: active(U11(tt(),V1,V2)) -> mark(U12(isNat(V1),V2))
r2: active(U12(tt(),V2)) -> mark(U13(isNat(V2)))
r3: active(U13(tt())) -> mark(tt())
r4: active(U21(tt(),V1)) -> mark(U22(isNat(V1)))
r5: active(U22(tt())) -> mark(tt())
r6: active(U31(tt(),N)) -> mark(N)
r7: active(U41(tt(),M,N)) -> mark(s(plus(N,M)))
r8: active(and(tt(),X)) -> mark(X)
r9: active(isNat(|0|())) -> mark(tt())
r10: active(isNat(plus(V1,V2))) -> mark(U11(and(isNatKind(V1),isNatKind(V2)),V1,V2))
r11: active(isNat(s(V1))) -> mark(U21(isNatKind(V1),V1))
r12: active(isNatKind(|0|())) -> mark(tt())
r13: active(isNatKind(plus(V1,V2))) -> mark(and(isNatKind(V1),isNatKind(V2)))
r14: active(isNatKind(s(V1))) -> mark(isNatKind(V1))
r15: active(plus(N,|0|())) -> mark(U31(and(isNat(N),isNatKind(N)),N))
r16: active(plus(N,s(M))) -> mark(U41(and(and(isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N))
r17: mark(U11(X1,X2,X3)) -> active(U11(mark(X1),X2,X3))
r18: mark(tt()) -> active(tt())
r19: mark(U12(X1,X2)) -> active(U12(mark(X1),X2))
r20: mark(isNat(X)) -> active(isNat(X))
r21: mark(U13(X)) -> active(U13(mark(X)))
r22: mark(U21(X1,X2)) -> active(U21(mark(X1),X2))
r23: mark(U22(X)) -> active(U22(mark(X)))
r24: mark(U31(X1,X2)) -> active(U31(mark(X1),X2))
r25: mark(U41(X1,X2,X3)) -> active(U41(mark(X1),X2,X3))
r26: mark(s(X)) -> active(s(mark(X)))
r27: mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2)))
r28: mark(and(X1,X2)) -> active(and(mark(X1),X2))
r29: mark(|0|()) -> active(|0|())
r30: mark(isNatKind(X)) -> active(isNatKind(X))
r31: U11(mark(X1),X2,X3) -> U11(X1,X2,X3)
r32: U11(X1,mark(X2),X3) -> U11(X1,X2,X3)
r33: U11(X1,X2,mark(X3)) -> U11(X1,X2,X3)
r34: U11(active(X1),X2,X3) -> U11(X1,X2,X3)
r35: U11(X1,active(X2),X3) -> U11(X1,X2,X3)
r36: U11(X1,X2,active(X3)) -> U11(X1,X2,X3)
r37: U12(mark(X1),X2) -> U12(X1,X2)
r38: U12(X1,mark(X2)) -> U12(X1,X2)
r39: U12(active(X1),X2) -> U12(X1,X2)
r40: U12(X1,active(X2)) -> U12(X1,X2)
r41: isNat(mark(X)) -> isNat(X)
r42: isNat(active(X)) -> isNat(X)
r43: U13(mark(X)) -> U13(X)
r44: U13(active(X)) -> U13(X)
r45: U21(mark(X1),X2) -> U21(X1,X2)
r46: U21(X1,mark(X2)) -> U21(X1,X2)
r47: U21(active(X1),X2) -> U21(X1,X2)
r48: U21(X1,active(X2)) -> U21(X1,X2)
r49: U22(mark(X)) -> U22(X)
r50: U22(active(X)) -> U22(X)
r51: U31(mark(X1),X2) -> U31(X1,X2)
r52: U31(X1,mark(X2)) -> U31(X1,X2)
r53: U31(active(X1),X2) -> U31(X1,X2)
r54: U31(X1,active(X2)) -> U31(X1,X2)
r55: U41(mark(X1),X2,X3) -> U41(X1,X2,X3)
r56: U41(X1,mark(X2),X3) -> U41(X1,X2,X3)
r57: U41(X1,X2,mark(X3)) -> U41(X1,X2,X3)
r58: U41(active(X1),X2,X3) -> U41(X1,X2,X3)
r59: U41(X1,active(X2),X3) -> U41(X1,X2,X3)
r60: U41(X1,X2,active(X3)) -> U41(X1,X2,X3)
r61: s(mark(X)) -> s(X)
r62: s(active(X)) -> s(X)
r63: plus(mark(X1),X2) -> plus(X1,X2)
r64: plus(X1,mark(X2)) -> plus(X1,X2)
r65: plus(active(X1),X2) -> plus(X1,X2)
r66: plus(X1,active(X2)) -> plus(X1,X2)
r67: and(mark(X1),X2) -> and(X1,X2)
r68: and(X1,mark(X2)) -> and(X1,X2)
r69: and(active(X1),X2) -> and(X1,X2)
r70: and(X1,active(X2)) -> and(X1,X2)
r71: isNatKind(mark(X)) -> isNatKind(X)
r72: isNatKind(active(X)) -> isNatKind(X)

The set of usable rules consists of

  (no rules)

Take the monotone reduction pair:

  matrix interpretations:
  
    carrier: N^3
    order: lexicographic order
    interpretations:
      U13#_A(x1) = ((1,0,0),(1,1,0),(1,1,1)) x1
      mark_A(x1) = ((1,0,0),(0,1,0),(1,1,1)) x1 + (1,1,1)
      active_A(x1) = ((1,0,0),(1,1,0),(1,1,1)) x1 + (1,1,1)

The next rules are strictly ordered:

  p1, p2
  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, r72

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: U22#(mark(X)) -> U22#(X)
p2: U22#(active(X)) -> U22#(X)

and R consists of:

r1: active(U11(tt(),V1,V2)) -> mark(U12(isNat(V1),V2))
r2: active(U12(tt(),V2)) -> mark(U13(isNat(V2)))
r3: active(U13(tt())) -> mark(tt())
r4: active(U21(tt(),V1)) -> mark(U22(isNat(V1)))
r5: active(U22(tt())) -> mark(tt())
r6: active(U31(tt(),N)) -> mark(N)
r7: active(U41(tt(),M,N)) -> mark(s(plus(N,M)))
r8: active(and(tt(),X)) -> mark(X)
r9: active(isNat(|0|())) -> mark(tt())
r10: active(isNat(plus(V1,V2))) -> mark(U11(and(isNatKind(V1),isNatKind(V2)),V1,V2))
r11: active(isNat(s(V1))) -> mark(U21(isNatKind(V1),V1))
r12: active(isNatKind(|0|())) -> mark(tt())
r13: active(isNatKind(plus(V1,V2))) -> mark(and(isNatKind(V1),isNatKind(V2)))
r14: active(isNatKind(s(V1))) -> mark(isNatKind(V1))
r15: active(plus(N,|0|())) -> mark(U31(and(isNat(N),isNatKind(N)),N))
r16: active(plus(N,s(M))) -> mark(U41(and(and(isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N))
r17: mark(U11(X1,X2,X3)) -> active(U11(mark(X1),X2,X3))
r18: mark(tt()) -> active(tt())
r19: mark(U12(X1,X2)) -> active(U12(mark(X1),X2))
r20: mark(isNat(X)) -> active(isNat(X))
r21: mark(U13(X)) -> active(U13(mark(X)))
r22: mark(U21(X1,X2)) -> active(U21(mark(X1),X2))
r23: mark(U22(X)) -> active(U22(mark(X)))
r24: mark(U31(X1,X2)) -> active(U31(mark(X1),X2))
r25: mark(U41(X1,X2,X3)) -> active(U41(mark(X1),X2,X3))
r26: mark(s(X)) -> active(s(mark(X)))
r27: mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2)))
r28: mark(and(X1,X2)) -> active(and(mark(X1),X2))
r29: mark(|0|()) -> active(|0|())
r30: mark(isNatKind(X)) -> active(isNatKind(X))
r31: U11(mark(X1),X2,X3) -> U11(X1,X2,X3)
r32: U11(X1,mark(X2),X3) -> U11(X1,X2,X3)
r33: U11(X1,X2,mark(X3)) -> U11(X1,X2,X3)
r34: U11(active(X1),X2,X3) -> U11(X1,X2,X3)
r35: U11(X1,active(X2),X3) -> U11(X1,X2,X3)
r36: U11(X1,X2,active(X3)) -> U11(X1,X2,X3)
r37: U12(mark(X1),X2) -> U12(X1,X2)
r38: U12(X1,mark(X2)) -> U12(X1,X2)
r39: U12(active(X1),X2) -> U12(X1,X2)
r40: U12(X1,active(X2)) -> U12(X1,X2)
r41: isNat(mark(X)) -> isNat(X)
r42: isNat(active(X)) -> isNat(X)
r43: U13(mark(X)) -> U13(X)
r44: U13(active(X)) -> U13(X)
r45: U21(mark(X1),X2) -> U21(X1,X2)
r46: U21(X1,mark(X2)) -> U21(X1,X2)
r47: U21(active(X1),X2) -> U21(X1,X2)
r48: U21(X1,active(X2)) -> U21(X1,X2)
r49: U22(mark(X)) -> U22(X)
r50: U22(active(X)) -> U22(X)
r51: U31(mark(X1),X2) -> U31(X1,X2)
r52: U31(X1,mark(X2)) -> U31(X1,X2)
r53: U31(active(X1),X2) -> U31(X1,X2)
r54: U31(X1,active(X2)) -> U31(X1,X2)
r55: U41(mark(X1),X2,X3) -> U41(X1,X2,X3)
r56: U41(X1,mark(X2),X3) -> U41(X1,X2,X3)
r57: U41(X1,X2,mark(X3)) -> U41(X1,X2,X3)
r58: U41(active(X1),X2,X3) -> U41(X1,X2,X3)
r59: U41(X1,active(X2),X3) -> U41(X1,X2,X3)
r60: U41(X1,X2,active(X3)) -> U41(X1,X2,X3)
r61: s(mark(X)) -> s(X)
r62: s(active(X)) -> s(X)
r63: plus(mark(X1),X2) -> plus(X1,X2)
r64: plus(X1,mark(X2)) -> plus(X1,X2)
r65: plus(active(X1),X2) -> plus(X1,X2)
r66: plus(X1,active(X2)) -> plus(X1,X2)
r67: and(mark(X1),X2) -> and(X1,X2)
r68: and(X1,mark(X2)) -> and(X1,X2)
r69: and(active(X1),X2) -> and(X1,X2)
r70: and(X1,active(X2)) -> and(X1,X2)
r71: isNatKind(mark(X)) -> isNatKind(X)
r72: isNatKind(active(X)) -> isNatKind(X)

The set of usable rules consists of

  (no rules)

Take the monotone reduction pair:

  matrix interpretations:
  
    carrier: N^3
    order: lexicographic order
    interpretations:
      U22#_A(x1) = ((1,0,0),(1,1,0),(1,1,1)) x1
      mark_A(x1) = ((1,0,0),(1,1,0),(1,1,1)) x1 + (1,1,1)
      active_A(x1) = ((1,0,0),(1,1,0),(1,1,1)) x1 + (1,1,1)

The next rules are strictly ordered:

  p1, p2
  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, r72

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: s#(mark(X)) -> s#(X)
p2: s#(active(X)) -> s#(X)

and R consists of:

r1: active(U11(tt(),V1,V2)) -> mark(U12(isNat(V1),V2))
r2: active(U12(tt(),V2)) -> mark(U13(isNat(V2)))
r3: active(U13(tt())) -> mark(tt())
r4: active(U21(tt(),V1)) -> mark(U22(isNat(V1)))
r5: active(U22(tt())) -> mark(tt())
r6: active(U31(tt(),N)) -> mark(N)
r7: active(U41(tt(),M,N)) -> mark(s(plus(N,M)))
r8: active(and(tt(),X)) -> mark(X)
r9: active(isNat(|0|())) -> mark(tt())
r10: active(isNat(plus(V1,V2))) -> mark(U11(and(isNatKind(V1),isNatKind(V2)),V1,V2))
r11: active(isNat(s(V1))) -> mark(U21(isNatKind(V1),V1))
r12: active(isNatKind(|0|())) -> mark(tt())
r13: active(isNatKind(plus(V1,V2))) -> mark(and(isNatKind(V1),isNatKind(V2)))
r14: active(isNatKind(s(V1))) -> mark(isNatKind(V1))
r15: active(plus(N,|0|())) -> mark(U31(and(isNat(N),isNatKind(N)),N))
r16: active(plus(N,s(M))) -> mark(U41(and(and(isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N))
r17: mark(U11(X1,X2,X3)) -> active(U11(mark(X1),X2,X3))
r18: mark(tt()) -> active(tt())
r19: mark(U12(X1,X2)) -> active(U12(mark(X1),X2))
r20: mark(isNat(X)) -> active(isNat(X))
r21: mark(U13(X)) -> active(U13(mark(X)))
r22: mark(U21(X1,X2)) -> active(U21(mark(X1),X2))
r23: mark(U22(X)) -> active(U22(mark(X)))
r24: mark(U31(X1,X2)) -> active(U31(mark(X1),X2))
r25: mark(U41(X1,X2,X3)) -> active(U41(mark(X1),X2,X3))
r26: mark(s(X)) -> active(s(mark(X)))
r27: mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2)))
r28: mark(and(X1,X2)) -> active(and(mark(X1),X2))
r29: mark(|0|()) -> active(|0|())
r30: mark(isNatKind(X)) -> active(isNatKind(X))
r31: U11(mark(X1),X2,X3) -> U11(X1,X2,X3)
r32: U11(X1,mark(X2),X3) -> U11(X1,X2,X3)
r33: U11(X1,X2,mark(X3)) -> U11(X1,X2,X3)
r34: U11(active(X1),X2,X3) -> U11(X1,X2,X3)
r35: U11(X1,active(X2),X3) -> U11(X1,X2,X3)
r36: U11(X1,X2,active(X3)) -> U11(X1,X2,X3)
r37: U12(mark(X1),X2) -> U12(X1,X2)
r38: U12(X1,mark(X2)) -> U12(X1,X2)
r39: U12(active(X1),X2) -> U12(X1,X2)
r40: U12(X1,active(X2)) -> U12(X1,X2)
r41: isNat(mark(X)) -> isNat(X)
r42: isNat(active(X)) -> isNat(X)
r43: U13(mark(X)) -> U13(X)
r44: U13(active(X)) -> U13(X)
r45: U21(mark(X1),X2) -> U21(X1,X2)
r46: U21(X1,mark(X2)) -> U21(X1,X2)
r47: U21(active(X1),X2) -> U21(X1,X2)
r48: U21(X1,active(X2)) -> U21(X1,X2)
r49: U22(mark(X)) -> U22(X)
r50: U22(active(X)) -> U22(X)
r51: U31(mark(X1),X2) -> U31(X1,X2)
r52: U31(X1,mark(X2)) -> U31(X1,X2)
r53: U31(active(X1),X2) -> U31(X1,X2)
r54: U31(X1,active(X2)) -> U31(X1,X2)
r55: U41(mark(X1),X2,X3) -> U41(X1,X2,X3)
r56: U41(X1,mark(X2),X3) -> U41(X1,X2,X3)
r57: U41(X1,X2,mark(X3)) -> U41(X1,X2,X3)
r58: U41(active(X1),X2,X3) -> U41(X1,X2,X3)
r59: U41(X1,active(X2),X3) -> U41(X1,X2,X3)
r60: U41(X1,X2,active(X3)) -> U41(X1,X2,X3)
r61: s(mark(X)) -> s(X)
r62: s(active(X)) -> s(X)
r63: plus(mark(X1),X2) -> plus(X1,X2)
r64: plus(X1,mark(X2)) -> plus(X1,X2)
r65: plus(active(X1),X2) -> plus(X1,X2)
r66: plus(X1,active(X2)) -> plus(X1,X2)
r67: and(mark(X1),X2) -> and(X1,X2)
r68: and(X1,mark(X2)) -> and(X1,X2)
r69: and(active(X1),X2) -> and(X1,X2)
r70: and(X1,active(X2)) -> and(X1,X2)
r71: isNatKind(mark(X)) -> isNatKind(X)
r72: isNatKind(active(X)) -> isNatKind(X)

The set of usable rules consists of

  (no rules)

Take the monotone reduction pair:

  matrix interpretations:
  
    carrier: N^3
    order: lexicographic order
    interpretations:
      s#_A(x1) = ((1,0,0),(1,1,0),(1,1,1)) x1
      mark_A(x1) = ((1,0,0),(0,1,0),(1,1,1)) x1 + (1,1,1)
      active_A(x1) = ((1,0,0),(1,1,0),(1,1,1)) x1 + (1,1,1)

The next rules are strictly ordered:

  p1, p2
  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, r72

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: plus#(mark(X1),X2) -> plus#(X1,X2)
p2: plus#(X1,active(X2)) -> plus#(X1,X2)
p3: plus#(active(X1),X2) -> plus#(X1,X2)
p4: plus#(X1,mark(X2)) -> plus#(X1,X2)

and R consists of:

r1: active(U11(tt(),V1,V2)) -> mark(U12(isNat(V1),V2))
r2: active(U12(tt(),V2)) -> mark(U13(isNat(V2)))
r3: active(U13(tt())) -> mark(tt())
r4: active(U21(tt(),V1)) -> mark(U22(isNat(V1)))
r5: active(U22(tt())) -> mark(tt())
r6: active(U31(tt(),N)) -> mark(N)
r7: active(U41(tt(),M,N)) -> mark(s(plus(N,M)))
r8: active(and(tt(),X)) -> mark(X)
r9: active(isNat(|0|())) -> mark(tt())
r10: active(isNat(plus(V1,V2))) -> mark(U11(and(isNatKind(V1),isNatKind(V2)),V1,V2))
r11: active(isNat(s(V1))) -> mark(U21(isNatKind(V1),V1))
r12: active(isNatKind(|0|())) -> mark(tt())
r13: active(isNatKind(plus(V1,V2))) -> mark(and(isNatKind(V1),isNatKind(V2)))
r14: active(isNatKind(s(V1))) -> mark(isNatKind(V1))
r15: active(plus(N,|0|())) -> mark(U31(and(isNat(N),isNatKind(N)),N))
r16: active(plus(N,s(M))) -> mark(U41(and(and(isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N))
r17: mark(U11(X1,X2,X3)) -> active(U11(mark(X1),X2,X3))
r18: mark(tt()) -> active(tt())
r19: mark(U12(X1,X2)) -> active(U12(mark(X1),X2))
r20: mark(isNat(X)) -> active(isNat(X))
r21: mark(U13(X)) -> active(U13(mark(X)))
r22: mark(U21(X1,X2)) -> active(U21(mark(X1),X2))
r23: mark(U22(X)) -> active(U22(mark(X)))
r24: mark(U31(X1,X2)) -> active(U31(mark(X1),X2))
r25: mark(U41(X1,X2,X3)) -> active(U41(mark(X1),X2,X3))
r26: mark(s(X)) -> active(s(mark(X)))
r27: mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2)))
r28: mark(and(X1,X2)) -> active(and(mark(X1),X2))
r29: mark(|0|()) -> active(|0|())
r30: mark(isNatKind(X)) -> active(isNatKind(X))
r31: U11(mark(X1),X2,X3) -> U11(X1,X2,X3)
r32: U11(X1,mark(X2),X3) -> U11(X1,X2,X3)
r33: U11(X1,X2,mark(X3)) -> U11(X1,X2,X3)
r34: U11(active(X1),X2,X3) -> U11(X1,X2,X3)
r35: U11(X1,active(X2),X3) -> U11(X1,X2,X3)
r36: U11(X1,X2,active(X3)) -> U11(X1,X2,X3)
r37: U12(mark(X1),X2) -> U12(X1,X2)
r38: U12(X1,mark(X2)) -> U12(X1,X2)
r39: U12(active(X1),X2) -> U12(X1,X2)
r40: U12(X1,active(X2)) -> U12(X1,X2)
r41: isNat(mark(X)) -> isNat(X)
r42: isNat(active(X)) -> isNat(X)
r43: U13(mark(X)) -> U13(X)
r44: U13(active(X)) -> U13(X)
r45: U21(mark(X1),X2) -> U21(X1,X2)
r46: U21(X1,mark(X2)) -> U21(X1,X2)
r47: U21(active(X1),X2) -> U21(X1,X2)
r48: U21(X1,active(X2)) -> U21(X1,X2)
r49: U22(mark(X)) -> U22(X)
r50: U22(active(X)) -> U22(X)
r51: U31(mark(X1),X2) -> U31(X1,X2)
r52: U31(X1,mark(X2)) -> U31(X1,X2)
r53: U31(active(X1),X2) -> U31(X1,X2)
r54: U31(X1,active(X2)) -> U31(X1,X2)
r55: U41(mark(X1),X2,X3) -> U41(X1,X2,X3)
r56: U41(X1,mark(X2),X3) -> U41(X1,X2,X3)
r57: U41(X1,X2,mark(X3)) -> U41(X1,X2,X3)
r58: U41(active(X1),X2,X3) -> U41(X1,X2,X3)
r59: U41(X1,active(X2),X3) -> U41(X1,X2,X3)
r60: U41(X1,X2,active(X3)) -> U41(X1,X2,X3)
r61: s(mark(X)) -> s(X)
r62: s(active(X)) -> s(X)
r63: plus(mark(X1),X2) -> plus(X1,X2)
r64: plus(X1,mark(X2)) -> plus(X1,X2)
r65: plus(active(X1),X2) -> plus(X1,X2)
r66: plus(X1,active(X2)) -> plus(X1,X2)
r67: and(mark(X1),X2) -> and(X1,X2)
r68: and(X1,mark(X2)) -> and(X1,X2)
r69: and(active(X1),X2) -> and(X1,X2)
r70: and(X1,active(X2)) -> and(X1,X2)
r71: isNatKind(mark(X)) -> isNatKind(X)
r72: isNatKind(active(X)) -> isNatKind(X)

The set of usable rules consists of

  (no rules)

Take the monotone reduction pair:

  matrix interpretations:
  
    carrier: N^3
    order: lexicographic order
    interpretations:
      plus#_A(x1,x2) = ((1,0,0),(1,1,0),(1,1,1)) x1 + ((1,0,0),(1,1,0),(1,1,1)) x2
      mark_A(x1) = ((1,0,0),(1,1,0),(1,1,1)) x1 + (1,1,1)
      active_A(x1) = ((1,0,0),(1,1,0),(1,1,1)) x1 + (1,1,1)

The next rules are strictly ordered:

  p1, p2, p3, p4
  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, r72

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: U11#(mark(X1),X2,X3) -> U11#(X1,X2,X3)
p2: U11#(X1,X2,active(X3)) -> U11#(X1,X2,X3)
p3: U11#(X1,active(X2),X3) -> U11#(X1,X2,X3)
p4: U11#(active(X1),X2,X3) -> U11#(X1,X2,X3)
p5: U11#(X1,X2,mark(X3)) -> U11#(X1,X2,X3)
p6: U11#(X1,mark(X2),X3) -> U11#(X1,X2,X3)

and R consists of:

r1: active(U11(tt(),V1,V2)) -> mark(U12(isNat(V1),V2))
r2: active(U12(tt(),V2)) -> mark(U13(isNat(V2)))
r3: active(U13(tt())) -> mark(tt())
r4: active(U21(tt(),V1)) -> mark(U22(isNat(V1)))
r5: active(U22(tt())) -> mark(tt())
r6: active(U31(tt(),N)) -> mark(N)
r7: active(U41(tt(),M,N)) -> mark(s(plus(N,M)))
r8: active(and(tt(),X)) -> mark(X)
r9: active(isNat(|0|())) -> mark(tt())
r10: active(isNat(plus(V1,V2))) -> mark(U11(and(isNatKind(V1),isNatKind(V2)),V1,V2))
r11: active(isNat(s(V1))) -> mark(U21(isNatKind(V1),V1))
r12: active(isNatKind(|0|())) -> mark(tt())
r13: active(isNatKind(plus(V1,V2))) -> mark(and(isNatKind(V1),isNatKind(V2)))
r14: active(isNatKind(s(V1))) -> mark(isNatKind(V1))
r15: active(plus(N,|0|())) -> mark(U31(and(isNat(N),isNatKind(N)),N))
r16: active(plus(N,s(M))) -> mark(U41(and(and(isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N))
r17: mark(U11(X1,X2,X3)) -> active(U11(mark(X1),X2,X3))
r18: mark(tt()) -> active(tt())
r19: mark(U12(X1,X2)) -> active(U12(mark(X1),X2))
r20: mark(isNat(X)) -> active(isNat(X))
r21: mark(U13(X)) -> active(U13(mark(X)))
r22: mark(U21(X1,X2)) -> active(U21(mark(X1),X2))
r23: mark(U22(X)) -> active(U22(mark(X)))
r24: mark(U31(X1,X2)) -> active(U31(mark(X1),X2))
r25: mark(U41(X1,X2,X3)) -> active(U41(mark(X1),X2,X3))
r26: mark(s(X)) -> active(s(mark(X)))
r27: mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2)))
r28: mark(and(X1,X2)) -> active(and(mark(X1),X2))
r29: mark(|0|()) -> active(|0|())
r30: mark(isNatKind(X)) -> active(isNatKind(X))
r31: U11(mark(X1),X2,X3) -> U11(X1,X2,X3)
r32: U11(X1,mark(X2),X3) -> U11(X1,X2,X3)
r33: U11(X1,X2,mark(X3)) -> U11(X1,X2,X3)
r34: U11(active(X1),X2,X3) -> U11(X1,X2,X3)
r35: U11(X1,active(X2),X3) -> U11(X1,X2,X3)
r36: U11(X1,X2,active(X3)) -> U11(X1,X2,X3)
r37: U12(mark(X1),X2) -> U12(X1,X2)
r38: U12(X1,mark(X2)) -> U12(X1,X2)
r39: U12(active(X1),X2) -> U12(X1,X2)
r40: U12(X1,active(X2)) -> U12(X1,X2)
r41: isNat(mark(X)) -> isNat(X)
r42: isNat(active(X)) -> isNat(X)
r43: U13(mark(X)) -> U13(X)
r44: U13(active(X)) -> U13(X)
r45: U21(mark(X1),X2) -> U21(X1,X2)
r46: U21(X1,mark(X2)) -> U21(X1,X2)
r47: U21(active(X1),X2) -> U21(X1,X2)
r48: U21(X1,active(X2)) -> U21(X1,X2)
r49: U22(mark(X)) -> U22(X)
r50: U22(active(X)) -> U22(X)
r51: U31(mark(X1),X2) -> U31(X1,X2)
r52: U31(X1,mark(X2)) -> U31(X1,X2)
r53: U31(active(X1),X2) -> U31(X1,X2)
r54: U31(X1,active(X2)) -> U31(X1,X2)
r55: U41(mark(X1),X2,X3) -> U41(X1,X2,X3)
r56: U41(X1,mark(X2),X3) -> U41(X1,X2,X3)
r57: U41(X1,X2,mark(X3)) -> U41(X1,X2,X3)
r58: U41(active(X1),X2,X3) -> U41(X1,X2,X3)
r59: U41(X1,active(X2),X3) -> U41(X1,X2,X3)
r60: U41(X1,X2,active(X3)) -> U41(X1,X2,X3)
r61: s(mark(X)) -> s(X)
r62: s(active(X)) -> s(X)
r63: plus(mark(X1),X2) -> plus(X1,X2)
r64: plus(X1,mark(X2)) -> plus(X1,X2)
r65: plus(active(X1),X2) -> plus(X1,X2)
r66: plus(X1,active(X2)) -> plus(X1,X2)
r67: and(mark(X1),X2) -> and(X1,X2)
r68: and(X1,mark(X2)) -> and(X1,X2)
r69: and(active(X1),X2) -> and(X1,X2)
r70: and(X1,active(X2)) -> and(X1,X2)
r71: isNatKind(mark(X)) -> isNatKind(X)
r72: isNatKind(active(X)) -> isNatKind(X)

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  matrix interpretations:
  
    carrier: N^3
    order: lexicographic order
    interpretations:
      U11#_A(x1,x2,x3) = ((1,0,0),(1,1,0),(1,1,1)) x1 + ((1,0,0),(1,1,0),(1,1,1)) x2 + ((1,0,0),(1,1,0),(1,1,0)) x3
      mark_A(x1) = ((1,0,0),(1,1,0),(1,1,1)) x1 + (1,1,1)
      active_A(x1) = ((1,0,0),(1,1,0),(1,1,1)) x1 + (1,1,1)

The next rules are strictly ordered:

  p1, p2, p3, p4, p5, p6

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: and#(mark(X1),X2) -> and#(X1,X2)
p2: and#(X1,active(X2)) -> and#(X1,X2)
p3: and#(active(X1),X2) -> and#(X1,X2)
p4: and#(X1,mark(X2)) -> and#(X1,X2)

and R consists of:

r1: active(U11(tt(),V1,V2)) -> mark(U12(isNat(V1),V2))
r2: active(U12(tt(),V2)) -> mark(U13(isNat(V2)))
r3: active(U13(tt())) -> mark(tt())
r4: active(U21(tt(),V1)) -> mark(U22(isNat(V1)))
r5: active(U22(tt())) -> mark(tt())
r6: active(U31(tt(),N)) -> mark(N)
r7: active(U41(tt(),M,N)) -> mark(s(plus(N,M)))
r8: active(and(tt(),X)) -> mark(X)
r9: active(isNat(|0|())) -> mark(tt())
r10: active(isNat(plus(V1,V2))) -> mark(U11(and(isNatKind(V1),isNatKind(V2)),V1,V2))
r11: active(isNat(s(V1))) -> mark(U21(isNatKind(V1),V1))
r12: active(isNatKind(|0|())) -> mark(tt())
r13: active(isNatKind(plus(V1,V2))) -> mark(and(isNatKind(V1),isNatKind(V2)))
r14: active(isNatKind(s(V1))) -> mark(isNatKind(V1))
r15: active(plus(N,|0|())) -> mark(U31(and(isNat(N),isNatKind(N)),N))
r16: active(plus(N,s(M))) -> mark(U41(and(and(isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N))
r17: mark(U11(X1,X2,X3)) -> active(U11(mark(X1),X2,X3))
r18: mark(tt()) -> active(tt())
r19: mark(U12(X1,X2)) -> active(U12(mark(X1),X2))
r20: mark(isNat(X)) -> active(isNat(X))
r21: mark(U13(X)) -> active(U13(mark(X)))
r22: mark(U21(X1,X2)) -> active(U21(mark(X1),X2))
r23: mark(U22(X)) -> active(U22(mark(X)))
r24: mark(U31(X1,X2)) -> active(U31(mark(X1),X2))
r25: mark(U41(X1,X2,X3)) -> active(U41(mark(X1),X2,X3))
r26: mark(s(X)) -> active(s(mark(X)))
r27: mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2)))
r28: mark(and(X1,X2)) -> active(and(mark(X1),X2))
r29: mark(|0|()) -> active(|0|())
r30: mark(isNatKind(X)) -> active(isNatKind(X))
r31: U11(mark(X1),X2,X3) -> U11(X1,X2,X3)
r32: U11(X1,mark(X2),X3) -> U11(X1,X2,X3)
r33: U11(X1,X2,mark(X3)) -> U11(X1,X2,X3)
r34: U11(active(X1),X2,X3) -> U11(X1,X2,X3)
r35: U11(X1,active(X2),X3) -> U11(X1,X2,X3)
r36: U11(X1,X2,active(X3)) -> U11(X1,X2,X3)
r37: U12(mark(X1),X2) -> U12(X1,X2)
r38: U12(X1,mark(X2)) -> U12(X1,X2)
r39: U12(active(X1),X2) -> U12(X1,X2)
r40: U12(X1,active(X2)) -> U12(X1,X2)
r41: isNat(mark(X)) -> isNat(X)
r42: isNat(active(X)) -> isNat(X)
r43: U13(mark(X)) -> U13(X)
r44: U13(active(X)) -> U13(X)
r45: U21(mark(X1),X2) -> U21(X1,X2)
r46: U21(X1,mark(X2)) -> U21(X1,X2)
r47: U21(active(X1),X2) -> U21(X1,X2)
r48: U21(X1,active(X2)) -> U21(X1,X2)
r49: U22(mark(X)) -> U22(X)
r50: U22(active(X)) -> U22(X)
r51: U31(mark(X1),X2) -> U31(X1,X2)
r52: U31(X1,mark(X2)) -> U31(X1,X2)
r53: U31(active(X1),X2) -> U31(X1,X2)
r54: U31(X1,active(X2)) -> U31(X1,X2)
r55: U41(mark(X1),X2,X3) -> U41(X1,X2,X3)
r56: U41(X1,mark(X2),X3) -> U41(X1,X2,X3)
r57: U41(X1,X2,mark(X3)) -> U41(X1,X2,X3)
r58: U41(active(X1),X2,X3) -> U41(X1,X2,X3)
r59: U41(X1,active(X2),X3) -> U41(X1,X2,X3)
r60: U41(X1,X2,active(X3)) -> U41(X1,X2,X3)
r61: s(mark(X)) -> s(X)
r62: s(active(X)) -> s(X)
r63: plus(mark(X1),X2) -> plus(X1,X2)
r64: plus(X1,mark(X2)) -> plus(X1,X2)
r65: plus(active(X1),X2) -> plus(X1,X2)
r66: plus(X1,active(X2)) -> plus(X1,X2)
r67: and(mark(X1),X2) -> and(X1,X2)
r68: and(X1,mark(X2)) -> and(X1,X2)
r69: and(active(X1),X2) -> and(X1,X2)
r70: and(X1,active(X2)) -> and(X1,X2)
r71: isNatKind(mark(X)) -> isNatKind(X)
r72: isNatKind(active(X)) -> isNatKind(X)

The set of usable rules consists of

  (no rules)

Take the monotone reduction pair:

  matrix interpretations:
  
    carrier: N^3
    order: lexicographic order
    interpretations:
      and#_A(x1,x2) = ((1,0,0),(0,1,0),(1,1,1)) x1 + ((1,0,0),(1,1,0),(1,1,1)) x2
      mark_A(x1) = ((1,0,0),(1,1,0),(1,1,1)) x1 + (1,1,1)
      active_A(x1) = ((1,0,0),(1,1,0),(1,1,1)) x1 + (1,1,1)

The next rules are strictly ordered:

  p1, p2, p3, p4
  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, r72

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: isNatKind#(mark(X)) -> isNatKind#(X)
p2: isNatKind#(active(X)) -> isNatKind#(X)

and R consists of:

r1: active(U11(tt(),V1,V2)) -> mark(U12(isNat(V1),V2))
r2: active(U12(tt(),V2)) -> mark(U13(isNat(V2)))
r3: active(U13(tt())) -> mark(tt())
r4: active(U21(tt(),V1)) -> mark(U22(isNat(V1)))
r5: active(U22(tt())) -> mark(tt())
r6: active(U31(tt(),N)) -> mark(N)
r7: active(U41(tt(),M,N)) -> mark(s(plus(N,M)))
r8: active(and(tt(),X)) -> mark(X)
r9: active(isNat(|0|())) -> mark(tt())
r10: active(isNat(plus(V1,V2))) -> mark(U11(and(isNatKind(V1),isNatKind(V2)),V1,V2))
r11: active(isNat(s(V1))) -> mark(U21(isNatKind(V1),V1))
r12: active(isNatKind(|0|())) -> mark(tt())
r13: active(isNatKind(plus(V1,V2))) -> mark(and(isNatKind(V1),isNatKind(V2)))
r14: active(isNatKind(s(V1))) -> mark(isNatKind(V1))
r15: active(plus(N,|0|())) -> mark(U31(and(isNat(N),isNatKind(N)),N))
r16: active(plus(N,s(M))) -> mark(U41(and(and(isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N))
r17: mark(U11(X1,X2,X3)) -> active(U11(mark(X1),X2,X3))
r18: mark(tt()) -> active(tt())
r19: mark(U12(X1,X2)) -> active(U12(mark(X1),X2))
r20: mark(isNat(X)) -> active(isNat(X))
r21: mark(U13(X)) -> active(U13(mark(X)))
r22: mark(U21(X1,X2)) -> active(U21(mark(X1),X2))
r23: mark(U22(X)) -> active(U22(mark(X)))
r24: mark(U31(X1,X2)) -> active(U31(mark(X1),X2))
r25: mark(U41(X1,X2,X3)) -> active(U41(mark(X1),X2,X3))
r26: mark(s(X)) -> active(s(mark(X)))
r27: mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2)))
r28: mark(and(X1,X2)) -> active(and(mark(X1),X2))
r29: mark(|0|()) -> active(|0|())
r30: mark(isNatKind(X)) -> active(isNatKind(X))
r31: U11(mark(X1),X2,X3) -> U11(X1,X2,X3)
r32: U11(X1,mark(X2),X3) -> U11(X1,X2,X3)
r33: U11(X1,X2,mark(X3)) -> U11(X1,X2,X3)
r34: U11(active(X1),X2,X3) -> U11(X1,X2,X3)
r35: U11(X1,active(X2),X3) -> U11(X1,X2,X3)
r36: U11(X1,X2,active(X3)) -> U11(X1,X2,X3)
r37: U12(mark(X1),X2) -> U12(X1,X2)
r38: U12(X1,mark(X2)) -> U12(X1,X2)
r39: U12(active(X1),X2) -> U12(X1,X2)
r40: U12(X1,active(X2)) -> U12(X1,X2)
r41: isNat(mark(X)) -> isNat(X)
r42: isNat(active(X)) -> isNat(X)
r43: U13(mark(X)) -> U13(X)
r44: U13(active(X)) -> U13(X)
r45: U21(mark(X1),X2) -> U21(X1,X2)
r46: U21(X1,mark(X2)) -> U21(X1,X2)
r47: U21(active(X1),X2) -> U21(X1,X2)
r48: U21(X1,active(X2)) -> U21(X1,X2)
r49: U22(mark(X)) -> U22(X)
r50: U22(active(X)) -> U22(X)
r51: U31(mark(X1),X2) -> U31(X1,X2)
r52: U31(X1,mark(X2)) -> U31(X1,X2)
r53: U31(active(X1),X2) -> U31(X1,X2)
r54: U31(X1,active(X2)) -> U31(X1,X2)
r55: U41(mark(X1),X2,X3) -> U41(X1,X2,X3)
r56: U41(X1,mark(X2),X3) -> U41(X1,X2,X3)
r57: U41(X1,X2,mark(X3)) -> U41(X1,X2,X3)
r58: U41(active(X1),X2,X3) -> U41(X1,X2,X3)
r59: U41(X1,active(X2),X3) -> U41(X1,X2,X3)
r60: U41(X1,X2,active(X3)) -> U41(X1,X2,X3)
r61: s(mark(X)) -> s(X)
r62: s(active(X)) -> s(X)
r63: plus(mark(X1),X2) -> plus(X1,X2)
r64: plus(X1,mark(X2)) -> plus(X1,X2)
r65: plus(active(X1),X2) -> plus(X1,X2)
r66: plus(X1,active(X2)) -> plus(X1,X2)
r67: and(mark(X1),X2) -> and(X1,X2)
r68: and(X1,mark(X2)) -> and(X1,X2)
r69: and(active(X1),X2) -> and(X1,X2)
r70: and(X1,active(X2)) -> and(X1,X2)
r71: isNatKind(mark(X)) -> isNatKind(X)
r72: isNatKind(active(X)) -> isNatKind(X)

The set of usable rules consists of

  (no rules)

Take the monotone reduction pair:

  matrix interpretations:
  
    carrier: N^3
    order: lexicographic order
    interpretations:
      isNatKind#_A(x1) = ((1,0,0),(1,1,0),(1,1,1)) x1
      mark_A(x1) = ((1,0,0),(1,1,0),(1,1,1)) x1 + (1,1,1)
      active_A(x1) = ((1,0,0),(1,1,0),(1,1,1)) x1 + (1,1,1)

The next rules are strictly ordered:

  p1, p2
  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, r72

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: U21#(mark(X1),X2) -> U21#(X1,X2)
p2: U21#(X1,active(X2)) -> U21#(X1,X2)
p3: U21#(active(X1),X2) -> U21#(X1,X2)
p4: U21#(X1,mark(X2)) -> U21#(X1,X2)

and R consists of:

r1: active(U11(tt(),V1,V2)) -> mark(U12(isNat(V1),V2))
r2: active(U12(tt(),V2)) -> mark(U13(isNat(V2)))
r3: active(U13(tt())) -> mark(tt())
r4: active(U21(tt(),V1)) -> mark(U22(isNat(V1)))
r5: active(U22(tt())) -> mark(tt())
r6: active(U31(tt(),N)) -> mark(N)
r7: active(U41(tt(),M,N)) -> mark(s(plus(N,M)))
r8: active(and(tt(),X)) -> mark(X)
r9: active(isNat(|0|())) -> mark(tt())
r10: active(isNat(plus(V1,V2))) -> mark(U11(and(isNatKind(V1),isNatKind(V2)),V1,V2))
r11: active(isNat(s(V1))) -> mark(U21(isNatKind(V1),V1))
r12: active(isNatKind(|0|())) -> mark(tt())
r13: active(isNatKind(plus(V1,V2))) -> mark(and(isNatKind(V1),isNatKind(V2)))
r14: active(isNatKind(s(V1))) -> mark(isNatKind(V1))
r15: active(plus(N,|0|())) -> mark(U31(and(isNat(N),isNatKind(N)),N))
r16: active(plus(N,s(M))) -> mark(U41(and(and(isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N))
r17: mark(U11(X1,X2,X3)) -> active(U11(mark(X1),X2,X3))
r18: mark(tt()) -> active(tt())
r19: mark(U12(X1,X2)) -> active(U12(mark(X1),X2))
r20: mark(isNat(X)) -> active(isNat(X))
r21: mark(U13(X)) -> active(U13(mark(X)))
r22: mark(U21(X1,X2)) -> active(U21(mark(X1),X2))
r23: mark(U22(X)) -> active(U22(mark(X)))
r24: mark(U31(X1,X2)) -> active(U31(mark(X1),X2))
r25: mark(U41(X1,X2,X3)) -> active(U41(mark(X1),X2,X3))
r26: mark(s(X)) -> active(s(mark(X)))
r27: mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2)))
r28: mark(and(X1,X2)) -> active(and(mark(X1),X2))
r29: mark(|0|()) -> active(|0|())
r30: mark(isNatKind(X)) -> active(isNatKind(X))
r31: U11(mark(X1),X2,X3) -> U11(X1,X2,X3)
r32: U11(X1,mark(X2),X3) -> U11(X1,X2,X3)
r33: U11(X1,X2,mark(X3)) -> U11(X1,X2,X3)
r34: U11(active(X1),X2,X3) -> U11(X1,X2,X3)
r35: U11(X1,active(X2),X3) -> U11(X1,X2,X3)
r36: U11(X1,X2,active(X3)) -> U11(X1,X2,X3)
r37: U12(mark(X1),X2) -> U12(X1,X2)
r38: U12(X1,mark(X2)) -> U12(X1,X2)
r39: U12(active(X1),X2) -> U12(X1,X2)
r40: U12(X1,active(X2)) -> U12(X1,X2)
r41: isNat(mark(X)) -> isNat(X)
r42: isNat(active(X)) -> isNat(X)
r43: U13(mark(X)) -> U13(X)
r44: U13(active(X)) -> U13(X)
r45: U21(mark(X1),X2) -> U21(X1,X2)
r46: U21(X1,mark(X2)) -> U21(X1,X2)
r47: U21(active(X1),X2) -> U21(X1,X2)
r48: U21(X1,active(X2)) -> U21(X1,X2)
r49: U22(mark(X)) -> U22(X)
r50: U22(active(X)) -> U22(X)
r51: U31(mark(X1),X2) -> U31(X1,X2)
r52: U31(X1,mark(X2)) -> U31(X1,X2)
r53: U31(active(X1),X2) -> U31(X1,X2)
r54: U31(X1,active(X2)) -> U31(X1,X2)
r55: U41(mark(X1),X2,X3) -> U41(X1,X2,X3)
r56: U41(X1,mark(X2),X3) -> U41(X1,X2,X3)
r57: U41(X1,X2,mark(X3)) -> U41(X1,X2,X3)
r58: U41(active(X1),X2,X3) -> U41(X1,X2,X3)
r59: U41(X1,active(X2),X3) -> U41(X1,X2,X3)
r60: U41(X1,X2,active(X3)) -> U41(X1,X2,X3)
r61: s(mark(X)) -> s(X)
r62: s(active(X)) -> s(X)
r63: plus(mark(X1),X2) -> plus(X1,X2)
r64: plus(X1,mark(X2)) -> plus(X1,X2)
r65: plus(active(X1),X2) -> plus(X1,X2)
r66: plus(X1,active(X2)) -> plus(X1,X2)
r67: and(mark(X1),X2) -> and(X1,X2)
r68: and(X1,mark(X2)) -> and(X1,X2)
r69: and(active(X1),X2) -> and(X1,X2)
r70: and(X1,active(X2)) -> and(X1,X2)
r71: isNatKind(mark(X)) -> isNatKind(X)
r72: isNatKind(active(X)) -> isNatKind(X)

The set of usable rules consists of

  (no rules)

Take the monotone reduction pair:

  matrix interpretations:
  
    carrier: N^3
    order: lexicographic order
    interpretations:
      U21#_A(x1,x2) = ((1,0,0),(1,1,0),(1,1,1)) x1 + ((1,0,0),(1,1,0),(1,1,1)) x2
      mark_A(x1) = ((1,0,0),(1,1,0),(1,1,1)) x1 + (1,1,1)
      active_A(x1) = ((1,0,0),(1,1,0),(1,1,1)) x1 + (1,1,1)

The next rules are strictly ordered:

  p1, p2, p3, p4
  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, r72

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: U31#(mark(X1),X2) -> U31#(X1,X2)
p2: U31#(X1,active(X2)) -> U31#(X1,X2)
p3: U31#(active(X1),X2) -> U31#(X1,X2)
p4: U31#(X1,mark(X2)) -> U31#(X1,X2)

and R consists of:

r1: active(U11(tt(),V1,V2)) -> mark(U12(isNat(V1),V2))
r2: active(U12(tt(),V2)) -> mark(U13(isNat(V2)))
r3: active(U13(tt())) -> mark(tt())
r4: active(U21(tt(),V1)) -> mark(U22(isNat(V1)))
r5: active(U22(tt())) -> mark(tt())
r6: active(U31(tt(),N)) -> mark(N)
r7: active(U41(tt(),M,N)) -> mark(s(plus(N,M)))
r8: active(and(tt(),X)) -> mark(X)
r9: active(isNat(|0|())) -> mark(tt())
r10: active(isNat(plus(V1,V2))) -> mark(U11(and(isNatKind(V1),isNatKind(V2)),V1,V2))
r11: active(isNat(s(V1))) -> mark(U21(isNatKind(V1),V1))
r12: active(isNatKind(|0|())) -> mark(tt())
r13: active(isNatKind(plus(V1,V2))) -> mark(and(isNatKind(V1),isNatKind(V2)))
r14: active(isNatKind(s(V1))) -> mark(isNatKind(V1))
r15: active(plus(N,|0|())) -> mark(U31(and(isNat(N),isNatKind(N)),N))
r16: active(plus(N,s(M))) -> mark(U41(and(and(isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N))
r17: mark(U11(X1,X2,X3)) -> active(U11(mark(X1),X2,X3))
r18: mark(tt()) -> active(tt())
r19: mark(U12(X1,X2)) -> active(U12(mark(X1),X2))
r20: mark(isNat(X)) -> active(isNat(X))
r21: mark(U13(X)) -> active(U13(mark(X)))
r22: mark(U21(X1,X2)) -> active(U21(mark(X1),X2))
r23: mark(U22(X)) -> active(U22(mark(X)))
r24: mark(U31(X1,X2)) -> active(U31(mark(X1),X2))
r25: mark(U41(X1,X2,X3)) -> active(U41(mark(X1),X2,X3))
r26: mark(s(X)) -> active(s(mark(X)))
r27: mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2)))
r28: mark(and(X1,X2)) -> active(and(mark(X1),X2))
r29: mark(|0|()) -> active(|0|())
r30: mark(isNatKind(X)) -> active(isNatKind(X))
r31: U11(mark(X1),X2,X3) -> U11(X1,X2,X3)
r32: U11(X1,mark(X2),X3) -> U11(X1,X2,X3)
r33: U11(X1,X2,mark(X3)) -> U11(X1,X2,X3)
r34: U11(active(X1),X2,X3) -> U11(X1,X2,X3)
r35: U11(X1,active(X2),X3) -> U11(X1,X2,X3)
r36: U11(X1,X2,active(X3)) -> U11(X1,X2,X3)
r37: U12(mark(X1),X2) -> U12(X1,X2)
r38: U12(X1,mark(X2)) -> U12(X1,X2)
r39: U12(active(X1),X2) -> U12(X1,X2)
r40: U12(X1,active(X2)) -> U12(X1,X2)
r41: isNat(mark(X)) -> isNat(X)
r42: isNat(active(X)) -> isNat(X)
r43: U13(mark(X)) -> U13(X)
r44: U13(active(X)) -> U13(X)
r45: U21(mark(X1),X2) -> U21(X1,X2)
r46: U21(X1,mark(X2)) -> U21(X1,X2)
r47: U21(active(X1),X2) -> U21(X1,X2)
r48: U21(X1,active(X2)) -> U21(X1,X2)
r49: U22(mark(X)) -> U22(X)
r50: U22(active(X)) -> U22(X)
r51: U31(mark(X1),X2) -> U31(X1,X2)
r52: U31(X1,mark(X2)) -> U31(X1,X2)
r53: U31(active(X1),X2) -> U31(X1,X2)
r54: U31(X1,active(X2)) -> U31(X1,X2)
r55: U41(mark(X1),X2,X3) -> U41(X1,X2,X3)
r56: U41(X1,mark(X2),X3) -> U41(X1,X2,X3)
r57: U41(X1,X2,mark(X3)) -> U41(X1,X2,X3)
r58: U41(active(X1),X2,X3) -> U41(X1,X2,X3)
r59: U41(X1,active(X2),X3) -> U41(X1,X2,X3)
r60: U41(X1,X2,active(X3)) -> U41(X1,X2,X3)
r61: s(mark(X)) -> s(X)
r62: s(active(X)) -> s(X)
r63: plus(mark(X1),X2) -> plus(X1,X2)
r64: plus(X1,mark(X2)) -> plus(X1,X2)
r65: plus(active(X1),X2) -> plus(X1,X2)
r66: plus(X1,active(X2)) -> plus(X1,X2)
r67: and(mark(X1),X2) -> and(X1,X2)
r68: and(X1,mark(X2)) -> and(X1,X2)
r69: and(active(X1),X2) -> and(X1,X2)
r70: and(X1,active(X2)) -> and(X1,X2)
r71: isNatKind(mark(X)) -> isNatKind(X)
r72: isNatKind(active(X)) -> isNatKind(X)

The set of usable rules consists of

  (no rules)

Take the monotone reduction pair:

  matrix interpretations:
  
    carrier: N^3
    order: lexicographic order
    interpretations:
      U31#_A(x1,x2) = ((1,0,0),(0,1,0),(1,1,1)) x1 + ((1,0,0),(1,1,0),(1,1,1)) x2
      mark_A(x1) = ((1,0,0),(1,1,0),(1,1,1)) x1 + (1,1,1)
      active_A(x1) = ((1,0,0),(1,1,0),(1,1,1)) x1 + (1,1,1)

The next rules are strictly ordered:

  p1, p2, p3, p4
  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, r72

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: U41#(mark(X1),X2,X3) -> U41#(X1,X2,X3)
p2: U41#(X1,X2,active(X3)) -> U41#(X1,X2,X3)
p3: U41#(X1,active(X2),X3) -> U41#(X1,X2,X3)
p4: U41#(active(X1),X2,X3) -> U41#(X1,X2,X3)
p5: U41#(X1,X2,mark(X3)) -> U41#(X1,X2,X3)
p6: U41#(X1,mark(X2),X3) -> U41#(X1,X2,X3)

and R consists of:

r1: active(U11(tt(),V1,V2)) -> mark(U12(isNat(V1),V2))
r2: active(U12(tt(),V2)) -> mark(U13(isNat(V2)))
r3: active(U13(tt())) -> mark(tt())
r4: active(U21(tt(),V1)) -> mark(U22(isNat(V1)))
r5: active(U22(tt())) -> mark(tt())
r6: active(U31(tt(),N)) -> mark(N)
r7: active(U41(tt(),M,N)) -> mark(s(plus(N,M)))
r8: active(and(tt(),X)) -> mark(X)
r9: active(isNat(|0|())) -> mark(tt())
r10: active(isNat(plus(V1,V2))) -> mark(U11(and(isNatKind(V1),isNatKind(V2)),V1,V2))
r11: active(isNat(s(V1))) -> mark(U21(isNatKind(V1),V1))
r12: active(isNatKind(|0|())) -> mark(tt())
r13: active(isNatKind(plus(V1,V2))) -> mark(and(isNatKind(V1),isNatKind(V2)))
r14: active(isNatKind(s(V1))) -> mark(isNatKind(V1))
r15: active(plus(N,|0|())) -> mark(U31(and(isNat(N),isNatKind(N)),N))
r16: active(plus(N,s(M))) -> mark(U41(and(and(isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N))
r17: mark(U11(X1,X2,X3)) -> active(U11(mark(X1),X2,X3))
r18: mark(tt()) -> active(tt())
r19: mark(U12(X1,X2)) -> active(U12(mark(X1),X2))
r20: mark(isNat(X)) -> active(isNat(X))
r21: mark(U13(X)) -> active(U13(mark(X)))
r22: mark(U21(X1,X2)) -> active(U21(mark(X1),X2))
r23: mark(U22(X)) -> active(U22(mark(X)))
r24: mark(U31(X1,X2)) -> active(U31(mark(X1),X2))
r25: mark(U41(X1,X2,X3)) -> active(U41(mark(X1),X2,X3))
r26: mark(s(X)) -> active(s(mark(X)))
r27: mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2)))
r28: mark(and(X1,X2)) -> active(and(mark(X1),X2))
r29: mark(|0|()) -> active(|0|())
r30: mark(isNatKind(X)) -> active(isNatKind(X))
r31: U11(mark(X1),X2,X3) -> U11(X1,X2,X3)
r32: U11(X1,mark(X2),X3) -> U11(X1,X2,X3)
r33: U11(X1,X2,mark(X3)) -> U11(X1,X2,X3)
r34: U11(active(X1),X2,X3) -> U11(X1,X2,X3)
r35: U11(X1,active(X2),X3) -> U11(X1,X2,X3)
r36: U11(X1,X2,active(X3)) -> U11(X1,X2,X3)
r37: U12(mark(X1),X2) -> U12(X1,X2)
r38: U12(X1,mark(X2)) -> U12(X1,X2)
r39: U12(active(X1),X2) -> U12(X1,X2)
r40: U12(X1,active(X2)) -> U12(X1,X2)
r41: isNat(mark(X)) -> isNat(X)
r42: isNat(active(X)) -> isNat(X)
r43: U13(mark(X)) -> U13(X)
r44: U13(active(X)) -> U13(X)
r45: U21(mark(X1),X2) -> U21(X1,X2)
r46: U21(X1,mark(X2)) -> U21(X1,X2)
r47: U21(active(X1),X2) -> U21(X1,X2)
r48: U21(X1,active(X2)) -> U21(X1,X2)
r49: U22(mark(X)) -> U22(X)
r50: U22(active(X)) -> U22(X)
r51: U31(mark(X1),X2) -> U31(X1,X2)
r52: U31(X1,mark(X2)) -> U31(X1,X2)
r53: U31(active(X1),X2) -> U31(X1,X2)
r54: U31(X1,active(X2)) -> U31(X1,X2)
r55: U41(mark(X1),X2,X3) -> U41(X1,X2,X3)
r56: U41(X1,mark(X2),X3) -> U41(X1,X2,X3)
r57: U41(X1,X2,mark(X3)) -> U41(X1,X2,X3)
r58: U41(active(X1),X2,X3) -> U41(X1,X2,X3)
r59: U41(X1,active(X2),X3) -> U41(X1,X2,X3)
r60: U41(X1,X2,active(X3)) -> U41(X1,X2,X3)
r61: s(mark(X)) -> s(X)
r62: s(active(X)) -> s(X)
r63: plus(mark(X1),X2) -> plus(X1,X2)
r64: plus(X1,mark(X2)) -> plus(X1,X2)
r65: plus(active(X1),X2) -> plus(X1,X2)
r66: plus(X1,active(X2)) -> plus(X1,X2)
r67: and(mark(X1),X2) -> and(X1,X2)
r68: and(X1,mark(X2)) -> and(X1,X2)
r69: and(active(X1),X2) -> and(X1,X2)
r70: and(X1,active(X2)) -> and(X1,X2)
r71: isNatKind(mark(X)) -> isNatKind(X)
r72: isNatKind(active(X)) -> isNatKind(X)

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  matrix interpretations:
  
    carrier: N^3
    order: lexicographic order
    interpretations:
      U41#_A(x1,x2,x3) = ((1,0,0),(1,1,0),(1,1,1)) x1 + ((1,0,0),(1,1,0),(1,1,1)) x2 + ((1,0,0),(1,1,0),(1,1,0)) x3
      mark_A(x1) = ((1,0,0),(1,1,0),(1,1,1)) x1 + (1,1,1)
      active_A(x1) = ((1,0,0),(1,1,0),(1,1,1)) x1 + (1,1,1)

The next rules are strictly ordered:

  p1, p2, p3, p4, p5, p6

We remove them from the problem.  Then no dependency pair remains.