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))
  active(U11(X1,X2,X3)) -> U11(active(X1),X2,X3)
  active(U12(X1,X2)) -> U12(active(X1),X2)
  active(U13(X)) -> U13(active(X))
  active(U21(X1,X2)) -> U21(active(X1),X2)
  active(U22(X)) -> U22(active(X))
  active(U31(X1,X2)) -> U31(active(X1),X2)
  active(U41(X1,X2,X3)) -> U41(active(X1),X2,X3)
  active(s(X)) -> s(active(X))
  active(plus(X1,X2)) -> plus(active(X1),X2)
  active(plus(X1,X2)) -> plus(X1,active(X2))
  active(and(X1,X2)) -> and(active(X1),X2)
  U11(mark(X1),X2,X3) -> mark(U11(X1,X2,X3))
  U12(mark(X1),X2) -> mark(U12(X1,X2))
  U13(mark(X)) -> mark(U13(X))
  U21(mark(X1),X2) -> mark(U21(X1,X2))
  U22(mark(X)) -> mark(U22(X))
  U31(mark(X1),X2) -> mark(U31(X1,X2))
  U41(mark(X1),X2,X3) -> mark(U41(X1,X2,X3))
  s(mark(X)) -> mark(s(X))
  plus(mark(X1),X2) -> mark(plus(X1,X2))
  plus(X1,mark(X2)) -> mark(plus(X1,X2))
  and(mark(X1),X2) -> mark(and(X1,X2))
  proper(U11(X1,X2,X3)) -> U11(proper(X1),proper(X2),proper(X3))
  proper(tt()) -> ok(tt())
  proper(U12(X1,X2)) -> U12(proper(X1),proper(X2))
  proper(isNat(X)) -> isNat(proper(X))
  proper(U13(X)) -> U13(proper(X))
  proper(U21(X1,X2)) -> U21(proper(X1),proper(X2))
  proper(U22(X)) -> U22(proper(X))
  proper(U31(X1,X2)) -> U31(proper(X1),proper(X2))
  proper(U41(X1,X2,X3)) -> U41(proper(X1),proper(X2),proper(X3))
  proper(s(X)) -> s(proper(X))
  proper(plus(X1,X2)) -> plus(proper(X1),proper(X2))
  proper(and(X1,X2)) -> and(proper(X1),proper(X2))
  proper(|0|()) -> ok(|0|())
  proper(isNatKind(X)) -> isNatKind(proper(X))
  U11(ok(X1),ok(X2),ok(X3)) -> ok(U11(X1,X2,X3))
  U12(ok(X1),ok(X2)) -> ok(U12(X1,X2))
  isNat(ok(X)) -> ok(isNat(X))
  U13(ok(X)) -> ok(U13(X))
  U21(ok(X1),ok(X2)) -> ok(U21(X1,X2))
  U22(ok(X)) -> ok(U22(X))
  U31(ok(X1),ok(X2)) -> ok(U31(X1,X2))
  U41(ok(X1),ok(X2),ok(X3)) -> ok(U41(X1,X2,X3))
  s(ok(X)) -> ok(s(X))
  plus(ok(X1),ok(X2)) -> ok(plus(X1,X2))
  and(ok(X1),ok(X2)) -> ok(and(X1,X2))
  isNatKind(ok(X)) -> ok(isNatKind(X))
  top(mark(X)) -> top(proper(X))
  top(ok(X)) -> top(active(X))

-- SCC decomposition.

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

p1: active#(U11(tt(),V1,V2)) -> U12#(isNat(V1),V2)
p2: active#(U11(tt(),V1,V2)) -> isNat#(V1)
p3: active#(U12(tt(),V2)) -> U13#(isNat(V2))
p4: active#(U12(tt(),V2)) -> isNat#(V2)
p5: active#(U21(tt(),V1)) -> U22#(isNat(V1))
p6: active#(U21(tt(),V1)) -> isNat#(V1)
p7: active#(U41(tt(),M,N)) -> s#(plus(N,M))
p8: active#(U41(tt(),M,N)) -> plus#(N,M)
p9: active#(isNat(plus(V1,V2))) -> U11#(and(isNatKind(V1),isNatKind(V2)),V1,V2)
p10: active#(isNat(plus(V1,V2))) -> and#(isNatKind(V1),isNatKind(V2))
p11: active#(isNat(plus(V1,V2))) -> isNatKind#(V1)
p12: active#(isNat(plus(V1,V2))) -> isNatKind#(V2)
p13: active#(isNat(s(V1))) -> U21#(isNatKind(V1),V1)
p14: active#(isNat(s(V1))) -> isNatKind#(V1)
p15: active#(isNatKind(plus(V1,V2))) -> and#(isNatKind(V1),isNatKind(V2))
p16: active#(isNatKind(plus(V1,V2))) -> isNatKind#(V1)
p17: active#(isNatKind(plus(V1,V2))) -> isNatKind#(V2)
p18: active#(isNatKind(s(V1))) -> isNatKind#(V1)
p19: active#(plus(N,|0|())) -> U31#(and(isNat(N),isNatKind(N)),N)
p20: active#(plus(N,|0|())) -> and#(isNat(N),isNatKind(N))
p21: active#(plus(N,|0|())) -> isNat#(N)
p22: active#(plus(N,|0|())) -> isNatKind#(N)
p23: active#(plus(N,s(M))) -> U41#(and(and(isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N)
p24: active#(plus(N,s(M))) -> and#(and(isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N)))
p25: active#(plus(N,s(M))) -> and#(isNat(M),isNatKind(M))
p26: active#(plus(N,s(M))) -> isNat#(M)
p27: active#(plus(N,s(M))) -> isNatKind#(M)
p28: active#(plus(N,s(M))) -> and#(isNat(N),isNatKind(N))
p29: active#(plus(N,s(M))) -> isNat#(N)
p30: active#(plus(N,s(M))) -> isNatKind#(N)
p31: active#(U11(X1,X2,X3)) -> U11#(active(X1),X2,X3)
p32: active#(U11(X1,X2,X3)) -> active#(X1)
p33: active#(U12(X1,X2)) -> U12#(active(X1),X2)
p34: active#(U12(X1,X2)) -> active#(X1)
p35: active#(U13(X)) -> U13#(active(X))
p36: active#(U13(X)) -> active#(X)
p37: active#(U21(X1,X2)) -> U21#(active(X1),X2)
p38: active#(U21(X1,X2)) -> active#(X1)
p39: active#(U22(X)) -> U22#(active(X))
p40: active#(U22(X)) -> active#(X)
p41: active#(U31(X1,X2)) -> U31#(active(X1),X2)
p42: active#(U31(X1,X2)) -> active#(X1)
p43: active#(U41(X1,X2,X3)) -> U41#(active(X1),X2,X3)
p44: active#(U41(X1,X2,X3)) -> active#(X1)
p45: active#(s(X)) -> s#(active(X))
p46: active#(s(X)) -> active#(X)
p47: active#(plus(X1,X2)) -> plus#(active(X1),X2)
p48: active#(plus(X1,X2)) -> active#(X1)
p49: active#(plus(X1,X2)) -> plus#(X1,active(X2))
p50: active#(plus(X1,X2)) -> active#(X2)
p51: active#(and(X1,X2)) -> and#(active(X1),X2)
p52: active#(and(X1,X2)) -> active#(X1)
p53: U11#(mark(X1),X2,X3) -> U11#(X1,X2,X3)
p54: U12#(mark(X1),X2) -> U12#(X1,X2)
p55: U13#(mark(X)) -> U13#(X)
p56: U21#(mark(X1),X2) -> U21#(X1,X2)
p57: U22#(mark(X)) -> U22#(X)
p58: U31#(mark(X1),X2) -> U31#(X1,X2)
p59: U41#(mark(X1),X2,X3) -> U41#(X1,X2,X3)
p60: s#(mark(X)) -> s#(X)
p61: plus#(mark(X1),X2) -> plus#(X1,X2)
p62: plus#(X1,mark(X2)) -> plus#(X1,X2)
p63: and#(mark(X1),X2) -> and#(X1,X2)
p64: proper#(U11(X1,X2,X3)) -> U11#(proper(X1),proper(X2),proper(X3))
p65: proper#(U11(X1,X2,X3)) -> proper#(X1)
p66: proper#(U11(X1,X2,X3)) -> proper#(X2)
p67: proper#(U11(X1,X2,X3)) -> proper#(X3)
p68: proper#(U12(X1,X2)) -> U12#(proper(X1),proper(X2))
p69: proper#(U12(X1,X2)) -> proper#(X1)
p70: proper#(U12(X1,X2)) -> proper#(X2)
p71: proper#(isNat(X)) -> isNat#(proper(X))
p72: proper#(isNat(X)) -> proper#(X)
p73: proper#(U13(X)) -> U13#(proper(X))
p74: proper#(U13(X)) -> proper#(X)
p75: proper#(U21(X1,X2)) -> U21#(proper(X1),proper(X2))
p76: proper#(U21(X1,X2)) -> proper#(X1)
p77: proper#(U21(X1,X2)) -> proper#(X2)
p78: proper#(U22(X)) -> U22#(proper(X))
p79: proper#(U22(X)) -> proper#(X)
p80: proper#(U31(X1,X2)) -> U31#(proper(X1),proper(X2))
p81: proper#(U31(X1,X2)) -> proper#(X1)
p82: proper#(U31(X1,X2)) -> proper#(X2)
p83: proper#(U41(X1,X2,X3)) -> U41#(proper(X1),proper(X2),proper(X3))
p84: proper#(U41(X1,X2,X3)) -> proper#(X1)
p85: proper#(U41(X1,X2,X3)) -> proper#(X2)
p86: proper#(U41(X1,X2,X3)) -> proper#(X3)
p87: proper#(s(X)) -> s#(proper(X))
p88: proper#(s(X)) -> proper#(X)
p89: proper#(plus(X1,X2)) -> plus#(proper(X1),proper(X2))
p90: proper#(plus(X1,X2)) -> proper#(X1)
p91: proper#(plus(X1,X2)) -> proper#(X2)
p92: proper#(and(X1,X2)) -> and#(proper(X1),proper(X2))
p93: proper#(and(X1,X2)) -> proper#(X1)
p94: proper#(and(X1,X2)) -> proper#(X2)
p95: proper#(isNatKind(X)) -> isNatKind#(proper(X))
p96: proper#(isNatKind(X)) -> proper#(X)
p97: U11#(ok(X1),ok(X2),ok(X3)) -> U11#(X1,X2,X3)
p98: U12#(ok(X1),ok(X2)) -> U12#(X1,X2)
p99: isNat#(ok(X)) -> isNat#(X)
p100: U13#(ok(X)) -> U13#(X)
p101: U21#(ok(X1),ok(X2)) -> U21#(X1,X2)
p102: U22#(ok(X)) -> U22#(X)
p103: U31#(ok(X1),ok(X2)) -> U31#(X1,X2)
p104: U41#(ok(X1),ok(X2),ok(X3)) -> U41#(X1,X2,X3)
p105: s#(ok(X)) -> s#(X)
p106: plus#(ok(X1),ok(X2)) -> plus#(X1,X2)
p107: and#(ok(X1),ok(X2)) -> and#(X1,X2)
p108: isNatKind#(ok(X)) -> isNatKind#(X)
p109: top#(mark(X)) -> top#(proper(X))
p110: top#(mark(X)) -> proper#(X)
p111: top#(ok(X)) -> top#(active(X))
p112: top#(ok(X)) -> active#(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: active(U11(X1,X2,X3)) -> U11(active(X1),X2,X3)
r18: active(U12(X1,X2)) -> U12(active(X1),X2)
r19: active(U13(X)) -> U13(active(X))
r20: active(U21(X1,X2)) -> U21(active(X1),X2)
r21: active(U22(X)) -> U22(active(X))
r22: active(U31(X1,X2)) -> U31(active(X1),X2)
r23: active(U41(X1,X2,X3)) -> U41(active(X1),X2,X3)
r24: active(s(X)) -> s(active(X))
r25: active(plus(X1,X2)) -> plus(active(X1),X2)
r26: active(plus(X1,X2)) -> plus(X1,active(X2))
r27: active(and(X1,X2)) -> and(active(X1),X2)
r28: U11(mark(X1),X2,X3) -> mark(U11(X1,X2,X3))
r29: U12(mark(X1),X2) -> mark(U12(X1,X2))
r30: U13(mark(X)) -> mark(U13(X))
r31: U21(mark(X1),X2) -> mark(U21(X1,X2))
r32: U22(mark(X)) -> mark(U22(X))
r33: U31(mark(X1),X2) -> mark(U31(X1,X2))
r34: U41(mark(X1),X2,X3) -> mark(U41(X1,X2,X3))
r35: s(mark(X)) -> mark(s(X))
r36: plus(mark(X1),X2) -> mark(plus(X1,X2))
r37: plus(X1,mark(X2)) -> mark(plus(X1,X2))
r38: and(mark(X1),X2) -> mark(and(X1,X2))
r39: proper(U11(X1,X2,X3)) -> U11(proper(X1),proper(X2),proper(X3))
r40: proper(tt()) -> ok(tt())
r41: proper(U12(X1,X2)) -> U12(proper(X1),proper(X2))
r42: proper(isNat(X)) -> isNat(proper(X))
r43: proper(U13(X)) -> U13(proper(X))
r44: proper(U21(X1,X2)) -> U21(proper(X1),proper(X2))
r45: proper(U22(X)) -> U22(proper(X))
r46: proper(U31(X1,X2)) -> U31(proper(X1),proper(X2))
r47: proper(U41(X1,X2,X3)) -> U41(proper(X1),proper(X2),proper(X3))
r48: proper(s(X)) -> s(proper(X))
r49: proper(plus(X1,X2)) -> plus(proper(X1),proper(X2))
r50: proper(and(X1,X2)) -> and(proper(X1),proper(X2))
r51: proper(|0|()) -> ok(|0|())
r52: proper(isNatKind(X)) -> isNatKind(proper(X))
r53: U11(ok(X1),ok(X2),ok(X3)) -> ok(U11(X1,X2,X3))
r54: U12(ok(X1),ok(X2)) -> ok(U12(X1,X2))
r55: isNat(ok(X)) -> ok(isNat(X))
r56: U13(ok(X)) -> ok(U13(X))
r57: U21(ok(X1),ok(X2)) -> ok(U21(X1,X2))
r58: U22(ok(X)) -> ok(U22(X))
r59: U31(ok(X1),ok(X2)) -> ok(U31(X1,X2))
r60: U41(ok(X1),ok(X2),ok(X3)) -> ok(U41(X1,X2,X3))
r61: s(ok(X)) -> ok(s(X))
r62: plus(ok(X1),ok(X2)) -> ok(plus(X1,X2))
r63: and(ok(X1),ok(X2)) -> ok(and(X1,X2))
r64: isNatKind(ok(X)) -> ok(isNatKind(X))
r65: top(mark(X)) -> top(proper(X))
r66: top(ok(X)) -> top(active(X))

The estimated dependency graph contains the following SCCs:

  {p109, p111}
  {p32, p34, p36, p38, p40, p42, p44, p46, p48, p50, p52}
  {p65, p66, p67, p69, p70, p72, p74, p76, p77, p79, p81, p82, p84, p85, p86, p88, p90, p91, p93, p94, p96}
  {p54, p98}
  {p99}
  {p55, p100}
  {p57, p102}
  {p60, p105}
  {p61, p62, p106}
  {p53, p97}
  {p63, p107}
  {p108}
  {p56, p101}
  {p58, p103}
  {p59, p104}


-- Reduction pair.

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

p1: top#(ok(X)) -> top#(active(X))
p2: top#(mark(X)) -> top#(proper(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: active(U11(X1,X2,X3)) -> U11(active(X1),X2,X3)
r18: active(U12(X1,X2)) -> U12(active(X1),X2)
r19: active(U13(X)) -> U13(active(X))
r20: active(U21(X1,X2)) -> U21(active(X1),X2)
r21: active(U22(X)) -> U22(active(X))
r22: active(U31(X1,X2)) -> U31(active(X1),X2)
r23: active(U41(X1,X2,X3)) -> U41(active(X1),X2,X3)
r24: active(s(X)) -> s(active(X))
r25: active(plus(X1,X2)) -> plus(active(X1),X2)
r26: active(plus(X1,X2)) -> plus(X1,active(X2))
r27: active(and(X1,X2)) -> and(active(X1),X2)
r28: U11(mark(X1),X2,X3) -> mark(U11(X1,X2,X3))
r29: U12(mark(X1),X2) -> mark(U12(X1,X2))
r30: U13(mark(X)) -> mark(U13(X))
r31: U21(mark(X1),X2) -> mark(U21(X1,X2))
r32: U22(mark(X)) -> mark(U22(X))
r33: U31(mark(X1),X2) -> mark(U31(X1,X2))
r34: U41(mark(X1),X2,X3) -> mark(U41(X1,X2,X3))
r35: s(mark(X)) -> mark(s(X))
r36: plus(mark(X1),X2) -> mark(plus(X1,X2))
r37: plus(X1,mark(X2)) -> mark(plus(X1,X2))
r38: and(mark(X1),X2) -> mark(and(X1,X2))
r39: proper(U11(X1,X2,X3)) -> U11(proper(X1),proper(X2),proper(X3))
r40: proper(tt()) -> ok(tt())
r41: proper(U12(X1,X2)) -> U12(proper(X1),proper(X2))
r42: proper(isNat(X)) -> isNat(proper(X))
r43: proper(U13(X)) -> U13(proper(X))
r44: proper(U21(X1,X2)) -> U21(proper(X1),proper(X2))
r45: proper(U22(X)) -> U22(proper(X))
r46: proper(U31(X1,X2)) -> U31(proper(X1),proper(X2))
r47: proper(U41(X1,X2,X3)) -> U41(proper(X1),proper(X2),proper(X3))
r48: proper(s(X)) -> s(proper(X))
r49: proper(plus(X1,X2)) -> plus(proper(X1),proper(X2))
r50: proper(and(X1,X2)) -> and(proper(X1),proper(X2))
r51: proper(|0|()) -> ok(|0|())
r52: proper(isNatKind(X)) -> isNatKind(proper(X))
r53: U11(ok(X1),ok(X2),ok(X3)) -> ok(U11(X1,X2,X3))
r54: U12(ok(X1),ok(X2)) -> ok(U12(X1,X2))
r55: isNat(ok(X)) -> ok(isNat(X))
r56: U13(ok(X)) -> ok(U13(X))
r57: U21(ok(X1),ok(X2)) -> ok(U21(X1,X2))
r58: U22(ok(X)) -> ok(U22(X))
r59: U31(ok(X1),ok(X2)) -> ok(U31(X1,X2))
r60: U41(ok(X1),ok(X2),ok(X3)) -> ok(U41(X1,X2,X3))
r61: s(ok(X)) -> ok(s(X))
r62: plus(ok(X1),ok(X2)) -> ok(plus(X1,X2))
r63: and(ok(X1),ok(X2)) -> ok(and(X1,X2))
r64: isNatKind(ok(X)) -> ok(isNatKind(X))
r65: top(mark(X)) -> top(proper(X))
r66: top(ok(X)) -> top(active(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

Take the reduction pair:

  matrix interpretations:
  
    carrier: N^4
    order: lexicographic order
    interpretations:
      top#_A(x1) = ((1,0,0,0),(1,1,0,0),(0,1,1,0),(0,0,1,1)) x1
      ok_A(x1) = x1
      active_A(x1) = x1
      mark_A(x1) = x1 + (0,0,0,2)
      proper_A(x1) = x1
      U11_A(x1,x2,x3) = x1 + ((0,0,0,0),(0,0,0,0),(1,0,0,0),(1,0,0,0)) x2 + ((0,0,0,0),(0,0,0,0),(1,0,0,0),(0,0,0,0)) x3 + (0,0,9,7)
      U12_A(x1,x2) = ((1,0,0,0),(0,1,0,0),(1,0,1,0),(0,0,1,1)) x1 + ((0,0,0,0),(0,0,0,0),(1,0,0,0),(0,0,0,0)) x2 + (0,0,5,1)
      U13_A(x1) = x1 + (0,0,1,1)
      U21_A(x1,x2) = ((1,0,0,0),(1,1,0,0),(0,0,1,0),(0,0,0,1)) x1 + ((0,0,0,0),(0,0,0,0),(1,0,0,0),(0,0,0,0)) x2 + (0,0,5,7)
      U22_A(x1) = ((1,0,0,0),(1,1,0,0),(1,0,1,0),(1,1,1,1)) x1 + (0,0,1,1)
      U31_A(x1,x2) = ((1,0,0,0),(1,1,0,0),(1,1,1,0),(1,1,0,1)) x1 + ((1,0,0,0),(1,0,0,0),(0,1,0,0),(1,1,1,0)) x2 + (1,4,0,2)
      U41_A(x1,x2,x3) = ((1,0,0,0),(1,1,0,0),(0,0,1,0),(0,0,0,1)) x1 + ((1,0,0,0),(1,1,0,0),(1,0,0,0),(0,0,1,0)) x2 + x3 + (10,3,1,13)
      s_A(x1) = ((1,0,0,0),(0,1,0,0),(1,1,1,0),(1,1,1,1)) x1 + (3,1,1,1)
      plus_A(x1,x2) = ((1,0,0,0),(0,1,0,0),(0,1,1,0),(1,1,0,1)) x1 + ((1,0,0,0),(1,1,0,0),(0,0,1,0),(1,1,1,1)) x2 + (7,1,1,1)
      and_A(x1,x2) = ((1,0,0,0),(1,1,0,0),(1,1,1,0),(1,1,0,1)) x1 + ((1,0,0,0),(0,1,0,0),(1,1,1,0),(1,1,1,1)) x2 + (0,0,0,2)
      isNat_A(x1) = ((0,0,0,0),(0,0,0,0),(1,0,0,0),(1,0,0,0)) x1 + (0,0,3,1)
      isNatKind_A(x1) = ((0,0,0,0),(0,0,0,0),(0,0,0,0),(1,0,0,0)) x1 + (0,0,0,3)
      tt_A() = (0,0,0,1)
      |0|_A() = (1,1,1,1)

The next rules are strictly ordered:

  p2

We remove them from the problem.

-- SCC decomposition.

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

p1: top#(ok(X)) -> top#(active(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: active(U11(X1,X2,X3)) -> U11(active(X1),X2,X3)
r18: active(U12(X1,X2)) -> U12(active(X1),X2)
r19: active(U13(X)) -> U13(active(X))
r20: active(U21(X1,X2)) -> U21(active(X1),X2)
r21: active(U22(X)) -> U22(active(X))
r22: active(U31(X1,X2)) -> U31(active(X1),X2)
r23: active(U41(X1,X2,X3)) -> U41(active(X1),X2,X3)
r24: active(s(X)) -> s(active(X))
r25: active(plus(X1,X2)) -> plus(active(X1),X2)
r26: active(plus(X1,X2)) -> plus(X1,active(X2))
r27: active(and(X1,X2)) -> and(active(X1),X2)
r28: U11(mark(X1),X2,X3) -> mark(U11(X1,X2,X3))
r29: U12(mark(X1),X2) -> mark(U12(X1,X2))
r30: U13(mark(X)) -> mark(U13(X))
r31: U21(mark(X1),X2) -> mark(U21(X1,X2))
r32: U22(mark(X)) -> mark(U22(X))
r33: U31(mark(X1),X2) -> mark(U31(X1,X2))
r34: U41(mark(X1),X2,X3) -> mark(U41(X1,X2,X3))
r35: s(mark(X)) -> mark(s(X))
r36: plus(mark(X1),X2) -> mark(plus(X1,X2))
r37: plus(X1,mark(X2)) -> mark(plus(X1,X2))
r38: and(mark(X1),X2) -> mark(and(X1,X2))
r39: proper(U11(X1,X2,X3)) -> U11(proper(X1),proper(X2),proper(X3))
r40: proper(tt()) -> ok(tt())
r41: proper(U12(X1,X2)) -> U12(proper(X1),proper(X2))
r42: proper(isNat(X)) -> isNat(proper(X))
r43: proper(U13(X)) -> U13(proper(X))
r44: proper(U21(X1,X2)) -> U21(proper(X1),proper(X2))
r45: proper(U22(X)) -> U22(proper(X))
r46: proper(U31(X1,X2)) -> U31(proper(X1),proper(X2))
r47: proper(U41(X1,X2,X3)) -> U41(proper(X1),proper(X2),proper(X3))
r48: proper(s(X)) -> s(proper(X))
r49: proper(plus(X1,X2)) -> plus(proper(X1),proper(X2))
r50: proper(and(X1,X2)) -> and(proper(X1),proper(X2))
r51: proper(|0|()) -> ok(|0|())
r52: proper(isNatKind(X)) -> isNatKind(proper(X))
r53: U11(ok(X1),ok(X2),ok(X3)) -> ok(U11(X1,X2,X3))
r54: U12(ok(X1),ok(X2)) -> ok(U12(X1,X2))
r55: isNat(ok(X)) -> ok(isNat(X))
r56: U13(ok(X)) -> ok(U13(X))
r57: U21(ok(X1),ok(X2)) -> ok(U21(X1,X2))
r58: U22(ok(X)) -> ok(U22(X))
r59: U31(ok(X1),ok(X2)) -> ok(U31(X1,X2))
r60: U41(ok(X1),ok(X2),ok(X3)) -> ok(U41(X1,X2,X3))
r61: s(ok(X)) -> ok(s(X))
r62: plus(ok(X1),ok(X2)) -> ok(plus(X1,X2))
r63: and(ok(X1),ok(X2)) -> ok(and(X1,X2))
r64: isNatKind(ok(X)) -> ok(isNatKind(X))
r65: top(mark(X)) -> top(proper(X))
r66: top(ok(X)) -> top(active(X))

The estimated dependency graph contains the following SCCs:

  {p1}


-- Reduction pair.

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

p1: top#(ok(X)) -> top#(active(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: active(U11(X1,X2,X3)) -> U11(active(X1),X2,X3)
r18: active(U12(X1,X2)) -> U12(active(X1),X2)
r19: active(U13(X)) -> U13(active(X))
r20: active(U21(X1,X2)) -> U21(active(X1),X2)
r21: active(U22(X)) -> U22(active(X))
r22: active(U31(X1,X2)) -> U31(active(X1),X2)
r23: active(U41(X1,X2,X3)) -> U41(active(X1),X2,X3)
r24: active(s(X)) -> s(active(X))
r25: active(plus(X1,X2)) -> plus(active(X1),X2)
r26: active(plus(X1,X2)) -> plus(X1,active(X2))
r27: active(and(X1,X2)) -> and(active(X1),X2)
r28: U11(mark(X1),X2,X3) -> mark(U11(X1,X2,X3))
r29: U12(mark(X1),X2) -> mark(U12(X1,X2))
r30: U13(mark(X)) -> mark(U13(X))
r31: U21(mark(X1),X2) -> mark(U21(X1,X2))
r32: U22(mark(X)) -> mark(U22(X))
r33: U31(mark(X1),X2) -> mark(U31(X1,X2))
r34: U41(mark(X1),X2,X3) -> mark(U41(X1,X2,X3))
r35: s(mark(X)) -> mark(s(X))
r36: plus(mark(X1),X2) -> mark(plus(X1,X2))
r37: plus(X1,mark(X2)) -> mark(plus(X1,X2))
r38: and(mark(X1),X2) -> mark(and(X1,X2))
r39: proper(U11(X1,X2,X3)) -> U11(proper(X1),proper(X2),proper(X3))
r40: proper(tt()) -> ok(tt())
r41: proper(U12(X1,X2)) -> U12(proper(X1),proper(X2))
r42: proper(isNat(X)) -> isNat(proper(X))
r43: proper(U13(X)) -> U13(proper(X))
r44: proper(U21(X1,X2)) -> U21(proper(X1),proper(X2))
r45: proper(U22(X)) -> U22(proper(X))
r46: proper(U31(X1,X2)) -> U31(proper(X1),proper(X2))
r47: proper(U41(X1,X2,X3)) -> U41(proper(X1),proper(X2),proper(X3))
r48: proper(s(X)) -> s(proper(X))
r49: proper(plus(X1,X2)) -> plus(proper(X1),proper(X2))
r50: proper(and(X1,X2)) -> and(proper(X1),proper(X2))
r51: proper(|0|()) -> ok(|0|())
r52: proper(isNatKind(X)) -> isNatKind(proper(X))
r53: U11(ok(X1),ok(X2),ok(X3)) -> ok(U11(X1,X2,X3))
r54: U12(ok(X1),ok(X2)) -> ok(U12(X1,X2))
r55: isNat(ok(X)) -> ok(isNat(X))
r56: U13(ok(X)) -> ok(U13(X))
r57: U21(ok(X1),ok(X2)) -> ok(U21(X1,X2))
r58: U22(ok(X)) -> ok(U22(X))
r59: U31(ok(X1),ok(X2)) -> ok(U31(X1,X2))
r60: U41(ok(X1),ok(X2),ok(X3)) -> ok(U41(X1,X2,X3))
r61: s(ok(X)) -> ok(s(X))
r62: plus(ok(X1),ok(X2)) -> ok(plus(X1,X2))
r63: and(ok(X1),ok(X2)) -> ok(and(X1,X2))
r64: isNatKind(ok(X)) -> ok(isNatKind(X))
r65: top(mark(X)) -> top(proper(X))
r66: top(ok(X)) -> top(active(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, r53, r54, r55, r56, r57, r58, r59, r60, r61, r62, r63, r64

Take the reduction pair:

  matrix interpretations:
  
    carrier: N^4
    order: lexicographic order
    interpretations:
      top#_A(x1) = ((0,0,0,0),(1,0,0,0),(0,1,0,0),(1,0,1,0)) x1
      ok_A(x1) = ((1,0,0,0),(0,0,0,0),(0,1,0,0),(1,1,1,0)) x1 + (9,1,18,1)
      active_A(x1) = ((1,0,0,0),(1,0,0,0),(0,0,0,0),(0,0,0,0)) x1 + (1,4,22,0)
      U11_A(x1,x2,x3) = x1 + x2 + x3 + (3,2,1,8)
      mark_A(x1) = (4,3,6,0)
      U12_A(x1,x2) = ((0,0,0,0),(0,0,0,0),(1,0,0,0),(1,1,0,0)) x1 + ((1,0,0,0),(1,0,0,0),(1,0,0,0),(0,0,0,0)) x2 + (5,0,1,1)
      U13_A(x1) = ((1,0,0,0),(0,0,0,0),(0,0,0,0),(1,0,0,0)) x1 + (1,2,21,1)
      U21_A(x1,x2) = ((0,0,0,0),(0,0,0,0),(1,0,0,0),(1,1,0,0)) x1 + ((1,0,0,0),(1,1,0,0),(1,1,0,0),(1,1,1,0)) x2 + (5,0,34,1)
      U22_A(x1) = ((1,0,0,0),(0,0,0,0),(1,0,0,0),(0,0,0,0)) x1 + (0,3,22,1)
      U31_A(x1,x2) = ((0,0,0,0),(1,0,0,0),(0,0,0,0),(0,0,0,0)) x1 + ((1,0,0,0),(0,0,0,0),(0,1,0,0),(1,0,0,0)) x2 + (5,0,23,1)
      U41_A(x1,x2,x3) = ((1,0,0,0),(1,0,0,0),(0,0,0,0),(0,0,0,0)) x1 + ((1,0,0,0),(0,0,0,0),(0,1,0,0),(1,1,0,0)) x2 + ((0,0,0,0),(0,0,0,0),(1,0,0,0),(0,1,0,0)) x3 + (0,0,7,1)
      s_A(x1) = x1 + (2,1,7,1)
      plus_A(x1,x2) = ((1,0,0,0),(0,0,0,0),(0,1,0,0),(1,0,1,0)) x1 + ((0,0,0,0),(0,0,0,0),(1,0,0,0),(1,1,0,0)) x2 + (4,4,19,1)
      and_A(x1,x2) = ((1,0,0,0),(0,0,0,0),(1,0,0,0),(0,0,0,0)) x1 + x2 + (1,4,14,1)
      isNat_A(x1) = ((1,0,0,0),(1,0,0,0),(0,0,0,0),(1,1,0,0)) x1 + (4,1,6,1)
      isNatKind_A(x1) = ((1,0,0,0),(1,1,0,0),(1,1,0,0),(0,0,0,0)) x1 + (4,0,1,1)
      tt_A() = (4,1,1,1)
      |0|_A() = (0,0,0,1)

The next rules are strictly ordered:

  p1

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

-- Reduction pair.

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

p1: active#(and(X1,X2)) -> active#(X1)
p2: active#(plus(X1,X2)) -> active#(X2)
p3: active#(plus(X1,X2)) -> active#(X1)
p4: active#(s(X)) -> active#(X)
p5: active#(U41(X1,X2,X3)) -> active#(X1)
p6: active#(U31(X1,X2)) -> active#(X1)
p7: active#(U22(X)) -> active#(X)
p8: active#(U21(X1,X2)) -> active#(X1)
p9: active#(U13(X)) -> active#(X)
p10: active#(U12(X1,X2)) -> active#(X1)
p11: active#(U11(X1,X2,X3)) -> active#(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: active(U11(X1,X2,X3)) -> U11(active(X1),X2,X3)
r18: active(U12(X1,X2)) -> U12(active(X1),X2)
r19: active(U13(X)) -> U13(active(X))
r20: active(U21(X1,X2)) -> U21(active(X1),X2)
r21: active(U22(X)) -> U22(active(X))
r22: active(U31(X1,X2)) -> U31(active(X1),X2)
r23: active(U41(X1,X2,X3)) -> U41(active(X1),X2,X3)
r24: active(s(X)) -> s(active(X))
r25: active(plus(X1,X2)) -> plus(active(X1),X2)
r26: active(plus(X1,X2)) -> plus(X1,active(X2))
r27: active(and(X1,X2)) -> and(active(X1),X2)
r28: U11(mark(X1),X2,X3) -> mark(U11(X1,X2,X3))
r29: U12(mark(X1),X2) -> mark(U12(X1,X2))
r30: U13(mark(X)) -> mark(U13(X))
r31: U21(mark(X1),X2) -> mark(U21(X1,X2))
r32: U22(mark(X)) -> mark(U22(X))
r33: U31(mark(X1),X2) -> mark(U31(X1,X2))
r34: U41(mark(X1),X2,X3) -> mark(U41(X1,X2,X3))
r35: s(mark(X)) -> mark(s(X))
r36: plus(mark(X1),X2) -> mark(plus(X1,X2))
r37: plus(X1,mark(X2)) -> mark(plus(X1,X2))
r38: and(mark(X1),X2) -> mark(and(X1,X2))
r39: proper(U11(X1,X2,X3)) -> U11(proper(X1),proper(X2),proper(X3))
r40: proper(tt()) -> ok(tt())
r41: proper(U12(X1,X2)) -> U12(proper(X1),proper(X2))
r42: proper(isNat(X)) -> isNat(proper(X))
r43: proper(U13(X)) -> U13(proper(X))
r44: proper(U21(X1,X2)) -> U21(proper(X1),proper(X2))
r45: proper(U22(X)) -> U22(proper(X))
r46: proper(U31(X1,X2)) -> U31(proper(X1),proper(X2))
r47: proper(U41(X1,X2,X3)) -> U41(proper(X1),proper(X2),proper(X3))
r48: proper(s(X)) -> s(proper(X))
r49: proper(plus(X1,X2)) -> plus(proper(X1),proper(X2))
r50: proper(and(X1,X2)) -> and(proper(X1),proper(X2))
r51: proper(|0|()) -> ok(|0|())
r52: proper(isNatKind(X)) -> isNatKind(proper(X))
r53: U11(ok(X1),ok(X2),ok(X3)) -> ok(U11(X1,X2,X3))
r54: U12(ok(X1),ok(X2)) -> ok(U12(X1,X2))
r55: isNat(ok(X)) -> ok(isNat(X))
r56: U13(ok(X)) -> ok(U13(X))
r57: U21(ok(X1),ok(X2)) -> ok(U21(X1,X2))
r58: U22(ok(X)) -> ok(U22(X))
r59: U31(ok(X1),ok(X2)) -> ok(U31(X1,X2))
r60: U41(ok(X1),ok(X2),ok(X3)) -> ok(U41(X1,X2,X3))
r61: s(ok(X)) -> ok(s(X))
r62: plus(ok(X1),ok(X2)) -> ok(plus(X1,X2))
r63: and(ok(X1),ok(X2)) -> ok(and(X1,X2))
r64: isNatKind(ok(X)) -> ok(isNatKind(X))
r65: top(mark(X)) -> top(proper(X))
r66: top(ok(X)) -> top(active(X))

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  matrix interpretations:
  
    carrier: N^4
    order: lexicographic order
    interpretations:
      active#_A(x1) = ((1,0,0,0),(1,1,0,0),(1,1,1,0),(1,1,1,0)) x1
      and_A(x1,x2) = ((1,0,0,0),(1,1,0,0),(1,1,1,0),(1,1,1,1)) x1 + ((1,0,0,0),(1,1,0,0),(1,1,1,0),(1,1,1,1)) x2 + (1,1,1,1)
      plus_A(x1,x2) = ((1,0,0,0),(1,1,0,0),(1,1,1,0),(1,1,1,1)) x1 + ((1,0,0,0),(1,1,0,0),(1,1,1,0),(1,1,1,1)) x2 + (1,1,1,1)
      s_A(x1) = ((1,0,0,0),(1,1,0,0),(1,1,1,0),(1,1,1,1)) x1 + (1,1,1,1)
      U41_A(x1,x2,x3) = ((1,0,0,0),(1,1,0,0),(1,1,1,0),(1,1,1,1)) x1 + ((1,0,0,0),(1,1,0,0),(1,1,1,0),(1,1,1,1)) x2 + ((1,0,0,0),(1,1,0,0),(1,1,1,0),(1,1,1,1)) x3 + (1,1,1,1)
      U31_A(x1,x2) = ((1,0,0,0),(1,1,0,0),(1,1,1,0),(1,1,1,1)) x1 + ((1,0,0,0),(1,1,0,0),(1,1,1,0),(1,1,1,1)) x2 + (1,1,1,1)
      U22_A(x1) = ((1,0,0,0),(1,1,0,0),(1,1,1,0),(1,1,1,1)) x1 + (1,1,1,1)
      U21_A(x1,x2) = ((1,0,0,0),(1,1,0,0),(1,1,1,0),(1,1,1,1)) x1 + ((1,0,0,0),(1,1,0,0),(1,1,1,0),(1,1,1,1)) x2 + (1,1,1,1)
      U13_A(x1) = ((1,0,0,0),(1,1,0,0),(1,1,1,0),(1,1,1,1)) x1 + (1,1,1,1)
      U12_A(x1,x2) = ((1,0,0,0),(1,1,0,0),(1,1,1,0),(1,1,1,1)) x1 + ((1,0,0,0),(1,1,0,0),(1,1,1,0),(1,1,1,1)) x2 + (1,1,1,1)
      U11_A(x1,x2,x3) = ((1,0,0,0),(1,1,0,0),(1,1,1,0),(1,1,1,1)) x1 + ((1,0,0,0),(1,1,0,0),(1,1,1,0),(1,1,1,1)) x2 + ((1,0,0,0),(1,1,0,0),(1,1,1,0),(1,1,1,1)) x3 + (1,1,1,1)

The next rules are strictly ordered:

  p1, p2, p3, p4, p5, p6, p7, p8, p9, p10, p11

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: proper#(isNatKind(X)) -> proper#(X)
p2: proper#(and(X1,X2)) -> proper#(X2)
p3: proper#(and(X1,X2)) -> proper#(X1)
p4: proper#(plus(X1,X2)) -> proper#(X2)
p5: proper#(plus(X1,X2)) -> proper#(X1)
p6: proper#(s(X)) -> proper#(X)
p7: proper#(U41(X1,X2,X3)) -> proper#(X3)
p8: proper#(U41(X1,X2,X3)) -> proper#(X2)
p9: proper#(U41(X1,X2,X3)) -> proper#(X1)
p10: proper#(U31(X1,X2)) -> proper#(X2)
p11: proper#(U31(X1,X2)) -> proper#(X1)
p12: proper#(U22(X)) -> proper#(X)
p13: proper#(U21(X1,X2)) -> proper#(X2)
p14: proper#(U21(X1,X2)) -> proper#(X1)
p15: proper#(U13(X)) -> proper#(X)
p16: proper#(isNat(X)) -> proper#(X)
p17: proper#(U12(X1,X2)) -> proper#(X2)
p18: proper#(U12(X1,X2)) -> proper#(X1)
p19: proper#(U11(X1,X2,X3)) -> proper#(X3)
p20: proper#(U11(X1,X2,X3)) -> proper#(X2)
p21: proper#(U11(X1,X2,X3)) -> proper#(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: active(U11(X1,X2,X3)) -> U11(active(X1),X2,X3)
r18: active(U12(X1,X2)) -> U12(active(X1),X2)
r19: active(U13(X)) -> U13(active(X))
r20: active(U21(X1,X2)) -> U21(active(X1),X2)
r21: active(U22(X)) -> U22(active(X))
r22: active(U31(X1,X2)) -> U31(active(X1),X2)
r23: active(U41(X1,X2,X3)) -> U41(active(X1),X2,X3)
r24: active(s(X)) -> s(active(X))
r25: active(plus(X1,X2)) -> plus(active(X1),X2)
r26: active(plus(X1,X2)) -> plus(X1,active(X2))
r27: active(and(X1,X2)) -> and(active(X1),X2)
r28: U11(mark(X1),X2,X3) -> mark(U11(X1,X2,X3))
r29: U12(mark(X1),X2) -> mark(U12(X1,X2))
r30: U13(mark(X)) -> mark(U13(X))
r31: U21(mark(X1),X2) -> mark(U21(X1,X2))
r32: U22(mark(X)) -> mark(U22(X))
r33: U31(mark(X1),X2) -> mark(U31(X1,X2))
r34: U41(mark(X1),X2,X3) -> mark(U41(X1,X2,X3))
r35: s(mark(X)) -> mark(s(X))
r36: plus(mark(X1),X2) -> mark(plus(X1,X2))
r37: plus(X1,mark(X2)) -> mark(plus(X1,X2))
r38: and(mark(X1),X2) -> mark(and(X1,X2))
r39: proper(U11(X1,X2,X3)) -> U11(proper(X1),proper(X2),proper(X3))
r40: proper(tt()) -> ok(tt())
r41: proper(U12(X1,X2)) -> U12(proper(X1),proper(X2))
r42: proper(isNat(X)) -> isNat(proper(X))
r43: proper(U13(X)) -> U13(proper(X))
r44: proper(U21(X1,X2)) -> U21(proper(X1),proper(X2))
r45: proper(U22(X)) -> U22(proper(X))
r46: proper(U31(X1,X2)) -> U31(proper(X1),proper(X2))
r47: proper(U41(X1,X2,X3)) -> U41(proper(X1),proper(X2),proper(X3))
r48: proper(s(X)) -> s(proper(X))
r49: proper(plus(X1,X2)) -> plus(proper(X1),proper(X2))
r50: proper(and(X1,X2)) -> and(proper(X1),proper(X2))
r51: proper(|0|()) -> ok(|0|())
r52: proper(isNatKind(X)) -> isNatKind(proper(X))
r53: U11(ok(X1),ok(X2),ok(X3)) -> ok(U11(X1,X2,X3))
r54: U12(ok(X1),ok(X2)) -> ok(U12(X1,X2))
r55: isNat(ok(X)) -> ok(isNat(X))
r56: U13(ok(X)) -> ok(U13(X))
r57: U21(ok(X1),ok(X2)) -> ok(U21(X1,X2))
r58: U22(ok(X)) -> ok(U22(X))
r59: U31(ok(X1),ok(X2)) -> ok(U31(X1,X2))
r60: U41(ok(X1),ok(X2),ok(X3)) -> ok(U41(X1,X2,X3))
r61: s(ok(X)) -> ok(s(X))
r62: plus(ok(X1),ok(X2)) -> ok(plus(X1,X2))
r63: and(ok(X1),ok(X2)) -> ok(and(X1,X2))
r64: isNatKind(ok(X)) -> ok(isNatKind(X))
r65: top(mark(X)) -> top(proper(X))
r66: top(ok(X)) -> top(active(X))

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  matrix interpretations:
  
    carrier: N^4
    order: lexicographic order
    interpretations:
      proper#_A(x1) = ((1,0,0,0),(0,1,0,0),(1,1,1,0),(1,1,1,1)) x1
      isNatKind_A(x1) = ((1,0,0,0),(1,1,0,0),(1,1,1,0),(1,1,1,1)) x1 + (1,1,1,1)
      and_A(x1,x2) = ((1,0,0,0),(1,1,0,0),(1,1,0,0),(1,1,0,0)) x1 + ((1,0,0,0),(1,1,0,0),(1,1,1,0),(1,1,1,1)) x2 + (1,1,1,1)
      plus_A(x1,x2) = ((1,0,0,0),(1,1,0,0),(1,1,1,0),(1,1,1,1)) x1 + ((1,0,0,0),(1,1,0,0),(1,1,1,0),(1,1,1,1)) x2 + (1,1,1,1)
      s_A(x1) = ((1,0,0,0),(1,1,0,0),(1,1,1,0),(1,1,1,1)) x1 + (1,1,1,1)
      U41_A(x1,x2,x3) = ((1,0,0,0),(1,1,0,0),(1,1,1,0),(1,1,1,1)) x1 + ((1,0,0,0),(1,1,0,0),(1,1,1,0),(1,1,1,1)) x2 + ((1,0,0,0),(1,1,0,0),(1,1,1,0),(1,1,1,1)) x3 + (1,1,1,1)
      U31_A(x1,x2) = ((1,0,0,0),(1,1,0,0),(1,1,1,0),(1,1,1,1)) x1 + ((1,0,0,0),(1,1,0,0),(1,1,1,0),(1,1,1,1)) x2 + (1,1,1,1)
      U22_A(x1) = ((1,0,0,0),(1,1,0,0),(1,1,1,0),(1,1,1,1)) x1 + (1,1,1,1)
      U21_A(x1,x2) = ((1,0,0,0),(1,1,0,0),(1,1,1,0),(1,1,1,1)) x1 + ((1,0,0,0),(1,1,0,0),(1,1,1,0),(1,1,1,1)) x2 + (1,1,1,1)
      U13_A(x1) = ((1,0,0,0),(1,1,0,0),(1,1,1,0),(1,1,1,1)) x1 + (1,1,1,1)
      isNat_A(x1) = ((1,0,0,0),(1,1,0,0),(1,1,1,0),(1,1,1,1)) x1 + (1,1,1,1)
      U12_A(x1,x2) = ((1,0,0,0),(1,1,0,0),(1,1,1,0),(1,1,1,1)) x1 + ((1,0,0,0),(1,1,0,0),(1,1,1,0),(1,1,1,1)) x2 + (1,1,1,1)
      U11_A(x1,x2,x3) = ((1,0,0,0),(1,1,0,0),(1,1,1,0),(1,1,1,1)) x1 + ((1,0,0,0),(1,1,0,0),(1,1,1,0),(1,1,1,1)) x2 + ((1,0,0,0),(1,1,0,0),(1,1,1,0),(1,1,1,1)) x3 + (1,1,1,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, p21

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

-- Reduction pair.

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

p1: U12#(mark(X1),X2) -> U12#(X1,X2)
p2: U12#(ok(X1),ok(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: active(U11(X1,X2,X3)) -> U11(active(X1),X2,X3)
r18: active(U12(X1,X2)) -> U12(active(X1),X2)
r19: active(U13(X)) -> U13(active(X))
r20: active(U21(X1,X2)) -> U21(active(X1),X2)
r21: active(U22(X)) -> U22(active(X))
r22: active(U31(X1,X2)) -> U31(active(X1),X2)
r23: active(U41(X1,X2,X3)) -> U41(active(X1),X2,X3)
r24: active(s(X)) -> s(active(X))
r25: active(plus(X1,X2)) -> plus(active(X1),X2)
r26: active(plus(X1,X2)) -> plus(X1,active(X2))
r27: active(and(X1,X2)) -> and(active(X1),X2)
r28: U11(mark(X1),X2,X3) -> mark(U11(X1,X2,X3))
r29: U12(mark(X1),X2) -> mark(U12(X1,X2))
r30: U13(mark(X)) -> mark(U13(X))
r31: U21(mark(X1),X2) -> mark(U21(X1,X2))
r32: U22(mark(X)) -> mark(U22(X))
r33: U31(mark(X1),X2) -> mark(U31(X1,X2))
r34: U41(mark(X1),X2,X3) -> mark(U41(X1,X2,X3))
r35: s(mark(X)) -> mark(s(X))
r36: plus(mark(X1),X2) -> mark(plus(X1,X2))
r37: plus(X1,mark(X2)) -> mark(plus(X1,X2))
r38: and(mark(X1),X2) -> mark(and(X1,X2))
r39: proper(U11(X1,X2,X3)) -> U11(proper(X1),proper(X2),proper(X3))
r40: proper(tt()) -> ok(tt())
r41: proper(U12(X1,X2)) -> U12(proper(X1),proper(X2))
r42: proper(isNat(X)) -> isNat(proper(X))
r43: proper(U13(X)) -> U13(proper(X))
r44: proper(U21(X1,X2)) -> U21(proper(X1),proper(X2))
r45: proper(U22(X)) -> U22(proper(X))
r46: proper(U31(X1,X2)) -> U31(proper(X1),proper(X2))
r47: proper(U41(X1,X2,X3)) -> U41(proper(X1),proper(X2),proper(X3))
r48: proper(s(X)) -> s(proper(X))
r49: proper(plus(X1,X2)) -> plus(proper(X1),proper(X2))
r50: proper(and(X1,X2)) -> and(proper(X1),proper(X2))
r51: proper(|0|()) -> ok(|0|())
r52: proper(isNatKind(X)) -> isNatKind(proper(X))
r53: U11(ok(X1),ok(X2),ok(X3)) -> ok(U11(X1,X2,X3))
r54: U12(ok(X1),ok(X2)) -> ok(U12(X1,X2))
r55: isNat(ok(X)) -> ok(isNat(X))
r56: U13(ok(X)) -> ok(U13(X))
r57: U21(ok(X1),ok(X2)) -> ok(U21(X1,X2))
r58: U22(ok(X)) -> ok(U22(X))
r59: U31(ok(X1),ok(X2)) -> ok(U31(X1,X2))
r60: U41(ok(X1),ok(X2),ok(X3)) -> ok(U41(X1,X2,X3))
r61: s(ok(X)) -> ok(s(X))
r62: plus(ok(X1),ok(X2)) -> ok(plus(X1,X2))
r63: and(ok(X1),ok(X2)) -> ok(and(X1,X2))
r64: isNatKind(ok(X)) -> ok(isNatKind(X))
r65: top(mark(X)) -> top(proper(X))
r66: top(ok(X)) -> top(active(X))

The set of usable rules consists of

  (no rules)

Take the reduction pair:

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

The next rules are strictly ordered:

  p1, p2

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#(ok(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: active(U11(X1,X2,X3)) -> U11(active(X1),X2,X3)
r18: active(U12(X1,X2)) -> U12(active(X1),X2)
r19: active(U13(X)) -> U13(active(X))
r20: active(U21(X1,X2)) -> U21(active(X1),X2)
r21: active(U22(X)) -> U22(active(X))
r22: active(U31(X1,X2)) -> U31(active(X1),X2)
r23: active(U41(X1,X2,X3)) -> U41(active(X1),X2,X3)
r24: active(s(X)) -> s(active(X))
r25: active(plus(X1,X2)) -> plus(active(X1),X2)
r26: active(plus(X1,X2)) -> plus(X1,active(X2))
r27: active(and(X1,X2)) -> and(active(X1),X2)
r28: U11(mark(X1),X2,X3) -> mark(U11(X1,X2,X3))
r29: U12(mark(X1),X2) -> mark(U12(X1,X2))
r30: U13(mark(X)) -> mark(U13(X))
r31: U21(mark(X1),X2) -> mark(U21(X1,X2))
r32: U22(mark(X)) -> mark(U22(X))
r33: U31(mark(X1),X2) -> mark(U31(X1,X2))
r34: U41(mark(X1),X2,X3) -> mark(U41(X1,X2,X3))
r35: s(mark(X)) -> mark(s(X))
r36: plus(mark(X1),X2) -> mark(plus(X1,X2))
r37: plus(X1,mark(X2)) -> mark(plus(X1,X2))
r38: and(mark(X1),X2) -> mark(and(X1,X2))
r39: proper(U11(X1,X2,X3)) -> U11(proper(X1),proper(X2),proper(X3))
r40: proper(tt()) -> ok(tt())
r41: proper(U12(X1,X2)) -> U12(proper(X1),proper(X2))
r42: proper(isNat(X)) -> isNat(proper(X))
r43: proper(U13(X)) -> U13(proper(X))
r44: proper(U21(X1,X2)) -> U21(proper(X1),proper(X2))
r45: proper(U22(X)) -> U22(proper(X))
r46: proper(U31(X1,X2)) -> U31(proper(X1),proper(X2))
r47: proper(U41(X1,X2,X3)) -> U41(proper(X1),proper(X2),proper(X3))
r48: proper(s(X)) -> s(proper(X))
r49: proper(plus(X1,X2)) -> plus(proper(X1),proper(X2))
r50: proper(and(X1,X2)) -> and(proper(X1),proper(X2))
r51: proper(|0|()) -> ok(|0|())
r52: proper(isNatKind(X)) -> isNatKind(proper(X))
r53: U11(ok(X1),ok(X2),ok(X3)) -> ok(U11(X1,X2,X3))
r54: U12(ok(X1),ok(X2)) -> ok(U12(X1,X2))
r55: isNat(ok(X)) -> ok(isNat(X))
r56: U13(ok(X)) -> ok(U13(X))
r57: U21(ok(X1),ok(X2)) -> ok(U21(X1,X2))
r58: U22(ok(X)) -> ok(U22(X))
r59: U31(ok(X1),ok(X2)) -> ok(U31(X1,X2))
r60: U41(ok(X1),ok(X2),ok(X3)) -> ok(U41(X1,X2,X3))
r61: s(ok(X)) -> ok(s(X))
r62: plus(ok(X1),ok(X2)) -> ok(plus(X1,X2))
r63: and(ok(X1),ok(X2)) -> ok(and(X1,X2))
r64: isNatKind(ok(X)) -> ok(isNatKind(X))
r65: top(mark(X)) -> top(proper(X))
r66: top(ok(X)) -> top(active(X))

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  matrix interpretations:
  
    carrier: N^4
    order: lexicographic order
    interpretations:
      isNat#_A(x1) = ((1,0,0,0),(0,1,0,0),(0,0,1,0),(0,1,1,1)) x1
      ok_A(x1) = ((1,0,0,0),(1,1,0,0),(1,1,1,0),(1,1,1,0)) x1 + (1,0,0,1)

The next rules are strictly ordered:

  p1

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

-- Reduction pair.

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

p1: U13#(mark(X)) -> U13#(X)
p2: U13#(ok(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: active(U11(X1,X2,X3)) -> U11(active(X1),X2,X3)
r18: active(U12(X1,X2)) -> U12(active(X1),X2)
r19: active(U13(X)) -> U13(active(X))
r20: active(U21(X1,X2)) -> U21(active(X1),X2)
r21: active(U22(X)) -> U22(active(X))
r22: active(U31(X1,X2)) -> U31(active(X1),X2)
r23: active(U41(X1,X2,X3)) -> U41(active(X1),X2,X3)
r24: active(s(X)) -> s(active(X))
r25: active(plus(X1,X2)) -> plus(active(X1),X2)
r26: active(plus(X1,X2)) -> plus(X1,active(X2))
r27: active(and(X1,X2)) -> and(active(X1),X2)
r28: U11(mark(X1),X2,X3) -> mark(U11(X1,X2,X3))
r29: U12(mark(X1),X2) -> mark(U12(X1,X2))
r30: U13(mark(X)) -> mark(U13(X))
r31: U21(mark(X1),X2) -> mark(U21(X1,X2))
r32: U22(mark(X)) -> mark(U22(X))
r33: U31(mark(X1),X2) -> mark(U31(X1,X2))
r34: U41(mark(X1),X2,X3) -> mark(U41(X1,X2,X3))
r35: s(mark(X)) -> mark(s(X))
r36: plus(mark(X1),X2) -> mark(plus(X1,X2))
r37: plus(X1,mark(X2)) -> mark(plus(X1,X2))
r38: and(mark(X1),X2) -> mark(and(X1,X2))
r39: proper(U11(X1,X2,X3)) -> U11(proper(X1),proper(X2),proper(X3))
r40: proper(tt()) -> ok(tt())
r41: proper(U12(X1,X2)) -> U12(proper(X1),proper(X2))
r42: proper(isNat(X)) -> isNat(proper(X))
r43: proper(U13(X)) -> U13(proper(X))
r44: proper(U21(X1,X2)) -> U21(proper(X1),proper(X2))
r45: proper(U22(X)) -> U22(proper(X))
r46: proper(U31(X1,X2)) -> U31(proper(X1),proper(X2))
r47: proper(U41(X1,X2,X3)) -> U41(proper(X1),proper(X2),proper(X3))
r48: proper(s(X)) -> s(proper(X))
r49: proper(plus(X1,X2)) -> plus(proper(X1),proper(X2))
r50: proper(and(X1,X2)) -> and(proper(X1),proper(X2))
r51: proper(|0|()) -> ok(|0|())
r52: proper(isNatKind(X)) -> isNatKind(proper(X))
r53: U11(ok(X1),ok(X2),ok(X3)) -> ok(U11(X1,X2,X3))
r54: U12(ok(X1),ok(X2)) -> ok(U12(X1,X2))
r55: isNat(ok(X)) -> ok(isNat(X))
r56: U13(ok(X)) -> ok(U13(X))
r57: U21(ok(X1),ok(X2)) -> ok(U21(X1,X2))
r58: U22(ok(X)) -> ok(U22(X))
r59: U31(ok(X1),ok(X2)) -> ok(U31(X1,X2))
r60: U41(ok(X1),ok(X2),ok(X3)) -> ok(U41(X1,X2,X3))
r61: s(ok(X)) -> ok(s(X))
r62: plus(ok(X1),ok(X2)) -> ok(plus(X1,X2))
r63: and(ok(X1),ok(X2)) -> ok(and(X1,X2))
r64: isNatKind(ok(X)) -> ok(isNatKind(X))
r65: top(mark(X)) -> top(proper(X))
r66: top(ok(X)) -> top(active(X))

The set of usable rules consists of

  (no rules)

Take the monotone reduction pair:

  matrix interpretations:
  
    carrier: N^4
    order: lexicographic order
    interpretations:
      U13#_A(x1) = ((1,0,0,0),(0,1,0,0),(0,1,1,0),(0,1,1,1)) x1
      mark_A(x1) = ((1,0,0,0),(1,1,0,0),(1,1,1,0),(1,1,1,1)) x1 + (1,1,1,1)
      ok_A(x1) = ((1,0,0,0),(1,1,0,0),(1,1,1,0),(1,1,1,1)) x1 + (1,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

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#(ok(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: active(U11(X1,X2,X3)) -> U11(active(X1),X2,X3)
r18: active(U12(X1,X2)) -> U12(active(X1),X2)
r19: active(U13(X)) -> U13(active(X))
r20: active(U21(X1,X2)) -> U21(active(X1),X2)
r21: active(U22(X)) -> U22(active(X))
r22: active(U31(X1,X2)) -> U31(active(X1),X2)
r23: active(U41(X1,X2,X3)) -> U41(active(X1),X2,X3)
r24: active(s(X)) -> s(active(X))
r25: active(plus(X1,X2)) -> plus(active(X1),X2)
r26: active(plus(X1,X2)) -> plus(X1,active(X2))
r27: active(and(X1,X2)) -> and(active(X1),X2)
r28: U11(mark(X1),X2,X3) -> mark(U11(X1,X2,X3))
r29: U12(mark(X1),X2) -> mark(U12(X1,X2))
r30: U13(mark(X)) -> mark(U13(X))
r31: U21(mark(X1),X2) -> mark(U21(X1,X2))
r32: U22(mark(X)) -> mark(U22(X))
r33: U31(mark(X1),X2) -> mark(U31(X1,X2))
r34: U41(mark(X1),X2,X3) -> mark(U41(X1,X2,X3))
r35: s(mark(X)) -> mark(s(X))
r36: plus(mark(X1),X2) -> mark(plus(X1,X2))
r37: plus(X1,mark(X2)) -> mark(plus(X1,X2))
r38: and(mark(X1),X2) -> mark(and(X1,X2))
r39: proper(U11(X1,X2,X3)) -> U11(proper(X1),proper(X2),proper(X3))
r40: proper(tt()) -> ok(tt())
r41: proper(U12(X1,X2)) -> U12(proper(X1),proper(X2))
r42: proper(isNat(X)) -> isNat(proper(X))
r43: proper(U13(X)) -> U13(proper(X))
r44: proper(U21(X1,X2)) -> U21(proper(X1),proper(X2))
r45: proper(U22(X)) -> U22(proper(X))
r46: proper(U31(X1,X2)) -> U31(proper(X1),proper(X2))
r47: proper(U41(X1,X2,X3)) -> U41(proper(X1),proper(X2),proper(X3))
r48: proper(s(X)) -> s(proper(X))
r49: proper(plus(X1,X2)) -> plus(proper(X1),proper(X2))
r50: proper(and(X1,X2)) -> and(proper(X1),proper(X2))
r51: proper(|0|()) -> ok(|0|())
r52: proper(isNatKind(X)) -> isNatKind(proper(X))
r53: U11(ok(X1),ok(X2),ok(X3)) -> ok(U11(X1,X2,X3))
r54: U12(ok(X1),ok(X2)) -> ok(U12(X1,X2))
r55: isNat(ok(X)) -> ok(isNat(X))
r56: U13(ok(X)) -> ok(U13(X))
r57: U21(ok(X1),ok(X2)) -> ok(U21(X1,X2))
r58: U22(ok(X)) -> ok(U22(X))
r59: U31(ok(X1),ok(X2)) -> ok(U31(X1,X2))
r60: U41(ok(X1),ok(X2),ok(X3)) -> ok(U41(X1,X2,X3))
r61: s(ok(X)) -> ok(s(X))
r62: plus(ok(X1),ok(X2)) -> ok(plus(X1,X2))
r63: and(ok(X1),ok(X2)) -> ok(and(X1,X2))
r64: isNatKind(ok(X)) -> ok(isNatKind(X))
r65: top(mark(X)) -> top(proper(X))
r66: top(ok(X)) -> top(active(X))

The set of usable rules consists of

  (no rules)

Take the monotone reduction pair:

  matrix interpretations:
  
    carrier: N^4
    order: lexicographic order
    interpretations:
      U22#_A(x1) = ((1,0,0,0),(1,1,0,0),(1,1,1,0),(1,1,1,1)) x1
      mark_A(x1) = ((1,0,0,0),(1,1,0,0),(1,1,1,0),(1,1,1,1)) x1 + (1,1,1,1)
      ok_A(x1) = ((1,0,0,0),(1,1,0,0),(1,1,1,0),(1,1,1,1)) x1 + (1,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

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#(ok(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: active(U11(X1,X2,X3)) -> U11(active(X1),X2,X3)
r18: active(U12(X1,X2)) -> U12(active(X1),X2)
r19: active(U13(X)) -> U13(active(X))
r20: active(U21(X1,X2)) -> U21(active(X1),X2)
r21: active(U22(X)) -> U22(active(X))
r22: active(U31(X1,X2)) -> U31(active(X1),X2)
r23: active(U41(X1,X2,X3)) -> U41(active(X1),X2,X3)
r24: active(s(X)) -> s(active(X))
r25: active(plus(X1,X2)) -> plus(active(X1),X2)
r26: active(plus(X1,X2)) -> plus(X1,active(X2))
r27: active(and(X1,X2)) -> and(active(X1),X2)
r28: U11(mark(X1),X2,X3) -> mark(U11(X1,X2,X3))
r29: U12(mark(X1),X2) -> mark(U12(X1,X2))
r30: U13(mark(X)) -> mark(U13(X))
r31: U21(mark(X1),X2) -> mark(U21(X1,X2))
r32: U22(mark(X)) -> mark(U22(X))
r33: U31(mark(X1),X2) -> mark(U31(X1,X2))
r34: U41(mark(X1),X2,X3) -> mark(U41(X1,X2,X3))
r35: s(mark(X)) -> mark(s(X))
r36: plus(mark(X1),X2) -> mark(plus(X1,X2))
r37: plus(X1,mark(X2)) -> mark(plus(X1,X2))
r38: and(mark(X1),X2) -> mark(and(X1,X2))
r39: proper(U11(X1,X2,X3)) -> U11(proper(X1),proper(X2),proper(X3))
r40: proper(tt()) -> ok(tt())
r41: proper(U12(X1,X2)) -> U12(proper(X1),proper(X2))
r42: proper(isNat(X)) -> isNat(proper(X))
r43: proper(U13(X)) -> U13(proper(X))
r44: proper(U21(X1,X2)) -> U21(proper(X1),proper(X2))
r45: proper(U22(X)) -> U22(proper(X))
r46: proper(U31(X1,X2)) -> U31(proper(X1),proper(X2))
r47: proper(U41(X1,X2,X3)) -> U41(proper(X1),proper(X2),proper(X3))
r48: proper(s(X)) -> s(proper(X))
r49: proper(plus(X1,X2)) -> plus(proper(X1),proper(X2))
r50: proper(and(X1,X2)) -> and(proper(X1),proper(X2))
r51: proper(|0|()) -> ok(|0|())
r52: proper(isNatKind(X)) -> isNatKind(proper(X))
r53: U11(ok(X1),ok(X2),ok(X3)) -> ok(U11(X1,X2,X3))
r54: U12(ok(X1),ok(X2)) -> ok(U12(X1,X2))
r55: isNat(ok(X)) -> ok(isNat(X))
r56: U13(ok(X)) -> ok(U13(X))
r57: U21(ok(X1),ok(X2)) -> ok(U21(X1,X2))
r58: U22(ok(X)) -> ok(U22(X))
r59: U31(ok(X1),ok(X2)) -> ok(U31(X1,X2))
r60: U41(ok(X1),ok(X2),ok(X3)) -> ok(U41(X1,X2,X3))
r61: s(ok(X)) -> ok(s(X))
r62: plus(ok(X1),ok(X2)) -> ok(plus(X1,X2))
r63: and(ok(X1),ok(X2)) -> ok(and(X1,X2))
r64: isNatKind(ok(X)) -> ok(isNatKind(X))
r65: top(mark(X)) -> top(proper(X))
r66: top(ok(X)) -> top(active(X))

The set of usable rules consists of

  (no rules)

Take the monotone reduction pair:

  matrix interpretations:
  
    carrier: N^4
    order: lexicographic order
    interpretations:
      s#_A(x1) = ((1,0,0,0),(0,1,0,0),(0,0,1,0),(0,1,1,1)) x1
      mark_A(x1) = ((1,0,0,0),(1,1,0,0),(1,1,1,0),(1,1,1,1)) x1 + (1,1,1,1)
      ok_A(x1) = ((1,0,0,0),(1,1,0,0),(1,1,1,0),(1,1,1,1)) x1 + (1,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

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#(ok(X1),ok(X2)) -> plus#(X1,X2)
p3: 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: active(U11(X1,X2,X3)) -> U11(active(X1),X2,X3)
r18: active(U12(X1,X2)) -> U12(active(X1),X2)
r19: active(U13(X)) -> U13(active(X))
r20: active(U21(X1,X2)) -> U21(active(X1),X2)
r21: active(U22(X)) -> U22(active(X))
r22: active(U31(X1,X2)) -> U31(active(X1),X2)
r23: active(U41(X1,X2,X3)) -> U41(active(X1),X2,X3)
r24: active(s(X)) -> s(active(X))
r25: active(plus(X1,X2)) -> plus(active(X1),X2)
r26: active(plus(X1,X2)) -> plus(X1,active(X2))
r27: active(and(X1,X2)) -> and(active(X1),X2)
r28: U11(mark(X1),X2,X3) -> mark(U11(X1,X2,X3))
r29: U12(mark(X1),X2) -> mark(U12(X1,X2))
r30: U13(mark(X)) -> mark(U13(X))
r31: U21(mark(X1),X2) -> mark(U21(X1,X2))
r32: U22(mark(X)) -> mark(U22(X))
r33: U31(mark(X1),X2) -> mark(U31(X1,X2))
r34: U41(mark(X1),X2,X3) -> mark(U41(X1,X2,X3))
r35: s(mark(X)) -> mark(s(X))
r36: plus(mark(X1),X2) -> mark(plus(X1,X2))
r37: plus(X1,mark(X2)) -> mark(plus(X1,X2))
r38: and(mark(X1),X2) -> mark(and(X1,X2))
r39: proper(U11(X1,X2,X3)) -> U11(proper(X1),proper(X2),proper(X3))
r40: proper(tt()) -> ok(tt())
r41: proper(U12(X1,X2)) -> U12(proper(X1),proper(X2))
r42: proper(isNat(X)) -> isNat(proper(X))
r43: proper(U13(X)) -> U13(proper(X))
r44: proper(U21(X1,X2)) -> U21(proper(X1),proper(X2))
r45: proper(U22(X)) -> U22(proper(X))
r46: proper(U31(X1,X2)) -> U31(proper(X1),proper(X2))
r47: proper(U41(X1,X2,X3)) -> U41(proper(X1),proper(X2),proper(X3))
r48: proper(s(X)) -> s(proper(X))
r49: proper(plus(X1,X2)) -> plus(proper(X1),proper(X2))
r50: proper(and(X1,X2)) -> and(proper(X1),proper(X2))
r51: proper(|0|()) -> ok(|0|())
r52: proper(isNatKind(X)) -> isNatKind(proper(X))
r53: U11(ok(X1),ok(X2),ok(X3)) -> ok(U11(X1,X2,X3))
r54: U12(ok(X1),ok(X2)) -> ok(U12(X1,X2))
r55: isNat(ok(X)) -> ok(isNat(X))
r56: U13(ok(X)) -> ok(U13(X))
r57: U21(ok(X1),ok(X2)) -> ok(U21(X1,X2))
r58: U22(ok(X)) -> ok(U22(X))
r59: U31(ok(X1),ok(X2)) -> ok(U31(X1,X2))
r60: U41(ok(X1),ok(X2),ok(X3)) -> ok(U41(X1,X2,X3))
r61: s(ok(X)) -> ok(s(X))
r62: plus(ok(X1),ok(X2)) -> ok(plus(X1,X2))
r63: and(ok(X1),ok(X2)) -> ok(and(X1,X2))
r64: isNatKind(ok(X)) -> ok(isNatKind(X))
r65: top(mark(X)) -> top(proper(X))
r66: top(ok(X)) -> top(active(X))

The set of usable rules consists of

  (no rules)

Take the monotone reduction pair:

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

The next rules are strictly ordered:

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

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#(ok(X1),ok(X2),ok(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: active(U11(X1,X2,X3)) -> U11(active(X1),X2,X3)
r18: active(U12(X1,X2)) -> U12(active(X1),X2)
r19: active(U13(X)) -> U13(active(X))
r20: active(U21(X1,X2)) -> U21(active(X1),X2)
r21: active(U22(X)) -> U22(active(X))
r22: active(U31(X1,X2)) -> U31(active(X1),X2)
r23: active(U41(X1,X2,X3)) -> U41(active(X1),X2,X3)
r24: active(s(X)) -> s(active(X))
r25: active(plus(X1,X2)) -> plus(active(X1),X2)
r26: active(plus(X1,X2)) -> plus(X1,active(X2))
r27: active(and(X1,X2)) -> and(active(X1),X2)
r28: U11(mark(X1),X2,X3) -> mark(U11(X1,X2,X3))
r29: U12(mark(X1),X2) -> mark(U12(X1,X2))
r30: U13(mark(X)) -> mark(U13(X))
r31: U21(mark(X1),X2) -> mark(U21(X1,X2))
r32: U22(mark(X)) -> mark(U22(X))
r33: U31(mark(X1),X2) -> mark(U31(X1,X2))
r34: U41(mark(X1),X2,X3) -> mark(U41(X1,X2,X3))
r35: s(mark(X)) -> mark(s(X))
r36: plus(mark(X1),X2) -> mark(plus(X1,X2))
r37: plus(X1,mark(X2)) -> mark(plus(X1,X2))
r38: and(mark(X1),X2) -> mark(and(X1,X2))
r39: proper(U11(X1,X2,X3)) -> U11(proper(X1),proper(X2),proper(X3))
r40: proper(tt()) -> ok(tt())
r41: proper(U12(X1,X2)) -> U12(proper(X1),proper(X2))
r42: proper(isNat(X)) -> isNat(proper(X))
r43: proper(U13(X)) -> U13(proper(X))
r44: proper(U21(X1,X2)) -> U21(proper(X1),proper(X2))
r45: proper(U22(X)) -> U22(proper(X))
r46: proper(U31(X1,X2)) -> U31(proper(X1),proper(X2))
r47: proper(U41(X1,X2,X3)) -> U41(proper(X1),proper(X2),proper(X3))
r48: proper(s(X)) -> s(proper(X))
r49: proper(plus(X1,X2)) -> plus(proper(X1),proper(X2))
r50: proper(and(X1,X2)) -> and(proper(X1),proper(X2))
r51: proper(|0|()) -> ok(|0|())
r52: proper(isNatKind(X)) -> isNatKind(proper(X))
r53: U11(ok(X1),ok(X2),ok(X3)) -> ok(U11(X1,X2,X3))
r54: U12(ok(X1),ok(X2)) -> ok(U12(X1,X2))
r55: isNat(ok(X)) -> ok(isNat(X))
r56: U13(ok(X)) -> ok(U13(X))
r57: U21(ok(X1),ok(X2)) -> ok(U21(X1,X2))
r58: U22(ok(X)) -> ok(U22(X))
r59: U31(ok(X1),ok(X2)) -> ok(U31(X1,X2))
r60: U41(ok(X1),ok(X2),ok(X3)) -> ok(U41(X1,X2,X3))
r61: s(ok(X)) -> ok(s(X))
r62: plus(ok(X1),ok(X2)) -> ok(plus(X1,X2))
r63: and(ok(X1),ok(X2)) -> ok(and(X1,X2))
r64: isNatKind(ok(X)) -> ok(isNatKind(X))
r65: top(mark(X)) -> top(proper(X))
r66: top(ok(X)) -> top(active(X))

The set of usable rules consists of

  (no rules)

Take the monotone reduction pair:

  matrix interpretations:
  
    carrier: N^4
    order: lexicographic order
    interpretations:
      U11#_A(x1,x2,x3) = ((1,0,0,0),(1,1,0,0),(1,1,1,0),(1,1,1,1)) x1 + ((1,0,0,0),(1,1,0,0),(1,1,1,0),(1,0,1,1)) x2 + ((1,0,0,0),(1,1,0,0),(1,1,1,0),(1,1,1,1)) x3
      mark_A(x1) = ((1,0,0,0),(1,1,0,0),(1,1,1,0),(1,1,1,1)) x1 + (1,1,1,1)
      ok_A(x1) = ((1,0,0,0),(1,1,0,0),(1,1,1,0),(1,1,1,1)) x1 + (1,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

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#(ok(X1),ok(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: active(U11(X1,X2,X3)) -> U11(active(X1),X2,X3)
r18: active(U12(X1,X2)) -> U12(active(X1),X2)
r19: active(U13(X)) -> U13(active(X))
r20: active(U21(X1,X2)) -> U21(active(X1),X2)
r21: active(U22(X)) -> U22(active(X))
r22: active(U31(X1,X2)) -> U31(active(X1),X2)
r23: active(U41(X1,X2,X3)) -> U41(active(X1),X2,X3)
r24: active(s(X)) -> s(active(X))
r25: active(plus(X1,X2)) -> plus(active(X1),X2)
r26: active(plus(X1,X2)) -> plus(X1,active(X2))
r27: active(and(X1,X2)) -> and(active(X1),X2)
r28: U11(mark(X1),X2,X3) -> mark(U11(X1,X2,X3))
r29: U12(mark(X1),X2) -> mark(U12(X1,X2))
r30: U13(mark(X)) -> mark(U13(X))
r31: U21(mark(X1),X2) -> mark(U21(X1,X2))
r32: U22(mark(X)) -> mark(U22(X))
r33: U31(mark(X1),X2) -> mark(U31(X1,X2))
r34: U41(mark(X1),X2,X3) -> mark(U41(X1,X2,X3))
r35: s(mark(X)) -> mark(s(X))
r36: plus(mark(X1),X2) -> mark(plus(X1,X2))
r37: plus(X1,mark(X2)) -> mark(plus(X1,X2))
r38: and(mark(X1),X2) -> mark(and(X1,X2))
r39: proper(U11(X1,X2,X3)) -> U11(proper(X1),proper(X2),proper(X3))
r40: proper(tt()) -> ok(tt())
r41: proper(U12(X1,X2)) -> U12(proper(X1),proper(X2))
r42: proper(isNat(X)) -> isNat(proper(X))
r43: proper(U13(X)) -> U13(proper(X))
r44: proper(U21(X1,X2)) -> U21(proper(X1),proper(X2))
r45: proper(U22(X)) -> U22(proper(X))
r46: proper(U31(X1,X2)) -> U31(proper(X1),proper(X2))
r47: proper(U41(X1,X2,X3)) -> U41(proper(X1),proper(X2),proper(X3))
r48: proper(s(X)) -> s(proper(X))
r49: proper(plus(X1,X2)) -> plus(proper(X1),proper(X2))
r50: proper(and(X1,X2)) -> and(proper(X1),proper(X2))
r51: proper(|0|()) -> ok(|0|())
r52: proper(isNatKind(X)) -> isNatKind(proper(X))
r53: U11(ok(X1),ok(X2),ok(X3)) -> ok(U11(X1,X2,X3))
r54: U12(ok(X1),ok(X2)) -> ok(U12(X1,X2))
r55: isNat(ok(X)) -> ok(isNat(X))
r56: U13(ok(X)) -> ok(U13(X))
r57: U21(ok(X1),ok(X2)) -> ok(U21(X1,X2))
r58: U22(ok(X)) -> ok(U22(X))
r59: U31(ok(X1),ok(X2)) -> ok(U31(X1,X2))
r60: U41(ok(X1),ok(X2),ok(X3)) -> ok(U41(X1,X2,X3))
r61: s(ok(X)) -> ok(s(X))
r62: plus(ok(X1),ok(X2)) -> ok(plus(X1,X2))
r63: and(ok(X1),ok(X2)) -> ok(and(X1,X2))
r64: isNatKind(ok(X)) -> ok(isNatKind(X))
r65: top(mark(X)) -> top(proper(X))
r66: top(ok(X)) -> top(active(X))

The set of usable rules consists of

  (no rules)

Take the reduction pair:

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

The next rules are strictly ordered:

  p1, p2

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#(ok(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: active(U11(X1,X2,X3)) -> U11(active(X1),X2,X3)
r18: active(U12(X1,X2)) -> U12(active(X1),X2)
r19: active(U13(X)) -> U13(active(X))
r20: active(U21(X1,X2)) -> U21(active(X1),X2)
r21: active(U22(X)) -> U22(active(X))
r22: active(U31(X1,X2)) -> U31(active(X1),X2)
r23: active(U41(X1,X2,X3)) -> U41(active(X1),X2,X3)
r24: active(s(X)) -> s(active(X))
r25: active(plus(X1,X2)) -> plus(active(X1),X2)
r26: active(plus(X1,X2)) -> plus(X1,active(X2))
r27: active(and(X1,X2)) -> and(active(X1),X2)
r28: U11(mark(X1),X2,X3) -> mark(U11(X1,X2,X3))
r29: U12(mark(X1),X2) -> mark(U12(X1,X2))
r30: U13(mark(X)) -> mark(U13(X))
r31: U21(mark(X1),X2) -> mark(U21(X1,X2))
r32: U22(mark(X)) -> mark(U22(X))
r33: U31(mark(X1),X2) -> mark(U31(X1,X2))
r34: U41(mark(X1),X2,X3) -> mark(U41(X1,X2,X3))
r35: s(mark(X)) -> mark(s(X))
r36: plus(mark(X1),X2) -> mark(plus(X1,X2))
r37: plus(X1,mark(X2)) -> mark(plus(X1,X2))
r38: and(mark(X1),X2) -> mark(and(X1,X2))
r39: proper(U11(X1,X2,X3)) -> U11(proper(X1),proper(X2),proper(X3))
r40: proper(tt()) -> ok(tt())
r41: proper(U12(X1,X2)) -> U12(proper(X1),proper(X2))
r42: proper(isNat(X)) -> isNat(proper(X))
r43: proper(U13(X)) -> U13(proper(X))
r44: proper(U21(X1,X2)) -> U21(proper(X1),proper(X2))
r45: proper(U22(X)) -> U22(proper(X))
r46: proper(U31(X1,X2)) -> U31(proper(X1),proper(X2))
r47: proper(U41(X1,X2,X3)) -> U41(proper(X1),proper(X2),proper(X3))
r48: proper(s(X)) -> s(proper(X))
r49: proper(plus(X1,X2)) -> plus(proper(X1),proper(X2))
r50: proper(and(X1,X2)) -> and(proper(X1),proper(X2))
r51: proper(|0|()) -> ok(|0|())
r52: proper(isNatKind(X)) -> isNatKind(proper(X))
r53: U11(ok(X1),ok(X2),ok(X3)) -> ok(U11(X1,X2,X3))
r54: U12(ok(X1),ok(X2)) -> ok(U12(X1,X2))
r55: isNat(ok(X)) -> ok(isNat(X))
r56: U13(ok(X)) -> ok(U13(X))
r57: U21(ok(X1),ok(X2)) -> ok(U21(X1,X2))
r58: U22(ok(X)) -> ok(U22(X))
r59: U31(ok(X1),ok(X2)) -> ok(U31(X1,X2))
r60: U41(ok(X1),ok(X2),ok(X3)) -> ok(U41(X1,X2,X3))
r61: s(ok(X)) -> ok(s(X))
r62: plus(ok(X1),ok(X2)) -> ok(plus(X1,X2))
r63: and(ok(X1),ok(X2)) -> ok(and(X1,X2))
r64: isNatKind(ok(X)) -> ok(isNatKind(X))
r65: top(mark(X)) -> top(proper(X))
r66: top(ok(X)) -> top(active(X))

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  matrix interpretations:
  
    carrier: N^4
    order: lexicographic order
    interpretations:
      isNatKind#_A(x1) = ((1,0,0,0),(0,1,0,0),(0,0,1,0),(0,1,1,1)) x1
      ok_A(x1) = ((1,0,0,0),(1,1,0,0),(1,1,1,0),(1,1,1,0)) x1 + (1,0,0,1)

The next rules are strictly ordered:

  p1

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

-- Reduction pair.

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

p1: U21#(mark(X1),X2) -> U21#(X1,X2)
p2: U21#(ok(X1),ok(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: active(U11(X1,X2,X3)) -> U11(active(X1),X2,X3)
r18: active(U12(X1,X2)) -> U12(active(X1),X2)
r19: active(U13(X)) -> U13(active(X))
r20: active(U21(X1,X2)) -> U21(active(X1),X2)
r21: active(U22(X)) -> U22(active(X))
r22: active(U31(X1,X2)) -> U31(active(X1),X2)
r23: active(U41(X1,X2,X3)) -> U41(active(X1),X2,X3)
r24: active(s(X)) -> s(active(X))
r25: active(plus(X1,X2)) -> plus(active(X1),X2)
r26: active(plus(X1,X2)) -> plus(X1,active(X2))
r27: active(and(X1,X2)) -> and(active(X1),X2)
r28: U11(mark(X1),X2,X3) -> mark(U11(X1,X2,X3))
r29: U12(mark(X1),X2) -> mark(U12(X1,X2))
r30: U13(mark(X)) -> mark(U13(X))
r31: U21(mark(X1),X2) -> mark(U21(X1,X2))
r32: U22(mark(X)) -> mark(U22(X))
r33: U31(mark(X1),X2) -> mark(U31(X1,X2))
r34: U41(mark(X1),X2,X3) -> mark(U41(X1,X2,X3))
r35: s(mark(X)) -> mark(s(X))
r36: plus(mark(X1),X2) -> mark(plus(X1,X2))
r37: plus(X1,mark(X2)) -> mark(plus(X1,X2))
r38: and(mark(X1),X2) -> mark(and(X1,X2))
r39: proper(U11(X1,X2,X3)) -> U11(proper(X1),proper(X2),proper(X3))
r40: proper(tt()) -> ok(tt())
r41: proper(U12(X1,X2)) -> U12(proper(X1),proper(X2))
r42: proper(isNat(X)) -> isNat(proper(X))
r43: proper(U13(X)) -> U13(proper(X))
r44: proper(U21(X1,X2)) -> U21(proper(X1),proper(X2))
r45: proper(U22(X)) -> U22(proper(X))
r46: proper(U31(X1,X2)) -> U31(proper(X1),proper(X2))
r47: proper(U41(X1,X2,X3)) -> U41(proper(X1),proper(X2),proper(X3))
r48: proper(s(X)) -> s(proper(X))
r49: proper(plus(X1,X2)) -> plus(proper(X1),proper(X2))
r50: proper(and(X1,X2)) -> and(proper(X1),proper(X2))
r51: proper(|0|()) -> ok(|0|())
r52: proper(isNatKind(X)) -> isNatKind(proper(X))
r53: U11(ok(X1),ok(X2),ok(X3)) -> ok(U11(X1,X2,X3))
r54: U12(ok(X1),ok(X2)) -> ok(U12(X1,X2))
r55: isNat(ok(X)) -> ok(isNat(X))
r56: U13(ok(X)) -> ok(U13(X))
r57: U21(ok(X1),ok(X2)) -> ok(U21(X1,X2))
r58: U22(ok(X)) -> ok(U22(X))
r59: U31(ok(X1),ok(X2)) -> ok(U31(X1,X2))
r60: U41(ok(X1),ok(X2),ok(X3)) -> ok(U41(X1,X2,X3))
r61: s(ok(X)) -> ok(s(X))
r62: plus(ok(X1),ok(X2)) -> ok(plus(X1,X2))
r63: and(ok(X1),ok(X2)) -> ok(and(X1,X2))
r64: isNatKind(ok(X)) -> ok(isNatKind(X))
r65: top(mark(X)) -> top(proper(X))
r66: top(ok(X)) -> top(active(X))

The set of usable rules consists of

  (no rules)

Take the reduction pair:

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

The next rules are strictly ordered:

  p1, p2

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#(ok(X1),ok(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: active(U11(X1,X2,X3)) -> U11(active(X1),X2,X3)
r18: active(U12(X1,X2)) -> U12(active(X1),X2)
r19: active(U13(X)) -> U13(active(X))
r20: active(U21(X1,X2)) -> U21(active(X1),X2)
r21: active(U22(X)) -> U22(active(X))
r22: active(U31(X1,X2)) -> U31(active(X1),X2)
r23: active(U41(X1,X2,X3)) -> U41(active(X1),X2,X3)
r24: active(s(X)) -> s(active(X))
r25: active(plus(X1,X2)) -> plus(active(X1),X2)
r26: active(plus(X1,X2)) -> plus(X1,active(X2))
r27: active(and(X1,X2)) -> and(active(X1),X2)
r28: U11(mark(X1),X2,X3) -> mark(U11(X1,X2,X3))
r29: U12(mark(X1),X2) -> mark(U12(X1,X2))
r30: U13(mark(X)) -> mark(U13(X))
r31: U21(mark(X1),X2) -> mark(U21(X1,X2))
r32: U22(mark(X)) -> mark(U22(X))
r33: U31(mark(X1),X2) -> mark(U31(X1,X2))
r34: U41(mark(X1),X2,X3) -> mark(U41(X1,X2,X3))
r35: s(mark(X)) -> mark(s(X))
r36: plus(mark(X1),X2) -> mark(plus(X1,X2))
r37: plus(X1,mark(X2)) -> mark(plus(X1,X2))
r38: and(mark(X1),X2) -> mark(and(X1,X2))
r39: proper(U11(X1,X2,X3)) -> U11(proper(X1),proper(X2),proper(X3))
r40: proper(tt()) -> ok(tt())
r41: proper(U12(X1,X2)) -> U12(proper(X1),proper(X2))
r42: proper(isNat(X)) -> isNat(proper(X))
r43: proper(U13(X)) -> U13(proper(X))
r44: proper(U21(X1,X2)) -> U21(proper(X1),proper(X2))
r45: proper(U22(X)) -> U22(proper(X))
r46: proper(U31(X1,X2)) -> U31(proper(X1),proper(X2))
r47: proper(U41(X1,X2,X3)) -> U41(proper(X1),proper(X2),proper(X3))
r48: proper(s(X)) -> s(proper(X))
r49: proper(plus(X1,X2)) -> plus(proper(X1),proper(X2))
r50: proper(and(X1,X2)) -> and(proper(X1),proper(X2))
r51: proper(|0|()) -> ok(|0|())
r52: proper(isNatKind(X)) -> isNatKind(proper(X))
r53: U11(ok(X1),ok(X2),ok(X3)) -> ok(U11(X1,X2,X3))
r54: U12(ok(X1),ok(X2)) -> ok(U12(X1,X2))
r55: isNat(ok(X)) -> ok(isNat(X))
r56: U13(ok(X)) -> ok(U13(X))
r57: U21(ok(X1),ok(X2)) -> ok(U21(X1,X2))
r58: U22(ok(X)) -> ok(U22(X))
r59: U31(ok(X1),ok(X2)) -> ok(U31(X1,X2))
r60: U41(ok(X1),ok(X2),ok(X3)) -> ok(U41(X1,X2,X3))
r61: s(ok(X)) -> ok(s(X))
r62: plus(ok(X1),ok(X2)) -> ok(plus(X1,X2))
r63: and(ok(X1),ok(X2)) -> ok(and(X1,X2))
r64: isNatKind(ok(X)) -> ok(isNatKind(X))
r65: top(mark(X)) -> top(proper(X))
r66: top(ok(X)) -> top(active(X))

The set of usable rules consists of

  (no rules)

Take the reduction pair:

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

The next rules are strictly ordered:

  p1, p2

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#(ok(X1),ok(X2),ok(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: active(U11(X1,X2,X3)) -> U11(active(X1),X2,X3)
r18: active(U12(X1,X2)) -> U12(active(X1),X2)
r19: active(U13(X)) -> U13(active(X))
r20: active(U21(X1,X2)) -> U21(active(X1),X2)
r21: active(U22(X)) -> U22(active(X))
r22: active(U31(X1,X2)) -> U31(active(X1),X2)
r23: active(U41(X1,X2,X3)) -> U41(active(X1),X2,X3)
r24: active(s(X)) -> s(active(X))
r25: active(plus(X1,X2)) -> plus(active(X1),X2)
r26: active(plus(X1,X2)) -> plus(X1,active(X2))
r27: active(and(X1,X2)) -> and(active(X1),X2)
r28: U11(mark(X1),X2,X3) -> mark(U11(X1,X2,X3))
r29: U12(mark(X1),X2) -> mark(U12(X1,X2))
r30: U13(mark(X)) -> mark(U13(X))
r31: U21(mark(X1),X2) -> mark(U21(X1,X2))
r32: U22(mark(X)) -> mark(U22(X))
r33: U31(mark(X1),X2) -> mark(U31(X1,X2))
r34: U41(mark(X1),X2,X3) -> mark(U41(X1,X2,X3))
r35: s(mark(X)) -> mark(s(X))
r36: plus(mark(X1),X2) -> mark(plus(X1,X2))
r37: plus(X1,mark(X2)) -> mark(plus(X1,X2))
r38: and(mark(X1),X2) -> mark(and(X1,X2))
r39: proper(U11(X1,X2,X3)) -> U11(proper(X1),proper(X2),proper(X3))
r40: proper(tt()) -> ok(tt())
r41: proper(U12(X1,X2)) -> U12(proper(X1),proper(X2))
r42: proper(isNat(X)) -> isNat(proper(X))
r43: proper(U13(X)) -> U13(proper(X))
r44: proper(U21(X1,X2)) -> U21(proper(X1),proper(X2))
r45: proper(U22(X)) -> U22(proper(X))
r46: proper(U31(X1,X2)) -> U31(proper(X1),proper(X2))
r47: proper(U41(X1,X2,X3)) -> U41(proper(X1),proper(X2),proper(X3))
r48: proper(s(X)) -> s(proper(X))
r49: proper(plus(X1,X2)) -> plus(proper(X1),proper(X2))
r50: proper(and(X1,X2)) -> and(proper(X1),proper(X2))
r51: proper(|0|()) -> ok(|0|())
r52: proper(isNatKind(X)) -> isNatKind(proper(X))
r53: U11(ok(X1),ok(X2),ok(X3)) -> ok(U11(X1,X2,X3))
r54: U12(ok(X1),ok(X2)) -> ok(U12(X1,X2))
r55: isNat(ok(X)) -> ok(isNat(X))
r56: U13(ok(X)) -> ok(U13(X))
r57: U21(ok(X1),ok(X2)) -> ok(U21(X1,X2))
r58: U22(ok(X)) -> ok(U22(X))
r59: U31(ok(X1),ok(X2)) -> ok(U31(X1,X2))
r60: U41(ok(X1),ok(X2),ok(X3)) -> ok(U41(X1,X2,X3))
r61: s(ok(X)) -> ok(s(X))
r62: plus(ok(X1),ok(X2)) -> ok(plus(X1,X2))
r63: and(ok(X1),ok(X2)) -> ok(and(X1,X2))
r64: isNatKind(ok(X)) -> ok(isNatKind(X))
r65: top(mark(X)) -> top(proper(X))
r66: top(ok(X)) -> top(active(X))

The set of usable rules consists of

  (no rules)

Take the monotone reduction pair:

  matrix interpretations:
  
    carrier: N^4
    order: lexicographic order
    interpretations:
      U41#_A(x1,x2,x3) = ((1,0,0,0),(1,1,0,0),(1,1,1,0),(1,1,1,1)) x1 + ((1,0,0,0),(1,1,0,0),(1,1,1,0),(1,0,1,1)) x2 + ((1,0,0,0),(1,1,0,0),(1,1,1,0),(1,1,1,1)) x3
      mark_A(x1) = ((1,0,0,0),(1,1,0,0),(1,1,1,0),(1,1,1,1)) x1 + (1,1,1,1)
      ok_A(x1) = ((1,0,0,0),(1,1,0,0),(1,1,1,0),(1,1,1,1)) x1 + (1,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

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