YES

We show the termination of the TRS R:

  active(U11(tt(),N)) -> mark(N)
  active(U21(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(and(isNat(V1),isNat(V2)))
  active(isNat(s(V1))) -> mark(isNat(V1))
  active(plus(N,|0|())) -> mark(U11(isNat(N),N))
  active(plus(N,s(M))) -> mark(U21(and(isNat(M),isNat(N)),M,N))
  mark(U11(X1,X2)) -> active(U11(mark(X1),X2))
  mark(tt()) -> active(tt())
  mark(U21(X1,X2,X3)) -> active(U21(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(isNat(X)) -> active(isNat(X))
  mark(|0|()) -> active(|0|())
  U11(mark(X1),X2) -> U11(X1,X2)
  U11(X1,mark(X2)) -> U11(X1,X2)
  U11(active(X1),X2) -> U11(X1,X2)
  U11(X1,active(X2)) -> U11(X1,X2)
  U21(mark(X1),X2,X3) -> U21(X1,X2,X3)
  U21(X1,mark(X2),X3) -> U21(X1,X2,X3)
  U21(X1,X2,mark(X3)) -> U21(X1,X2,X3)
  U21(active(X1),X2,X3) -> U21(X1,X2,X3)
  U21(X1,active(X2),X3) -> U21(X1,X2,X3)
  U21(X1,X2,active(X3)) -> U21(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)
  isNat(mark(X)) -> isNat(X)
  isNat(active(X)) -> isNat(X)

-- SCC decomposition.

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

p1: active#(U11(tt(),N)) -> mark#(N)
p2: active#(U21(tt(),M,N)) -> mark#(s(plus(N,M)))
p3: active#(U21(tt(),M,N)) -> s#(plus(N,M))
p4: active#(U21(tt(),M,N)) -> plus#(N,M)
p5: active#(and(tt(),X)) -> mark#(X)
p6: active#(isNat(|0|())) -> mark#(tt())
p7: active#(isNat(plus(V1,V2))) -> mark#(and(isNat(V1),isNat(V2)))
p8: active#(isNat(plus(V1,V2))) -> and#(isNat(V1),isNat(V2))
p9: active#(isNat(plus(V1,V2))) -> isNat#(V1)
p10: active#(isNat(plus(V1,V2))) -> isNat#(V2)
p11: active#(isNat(s(V1))) -> mark#(isNat(V1))
p12: active#(isNat(s(V1))) -> isNat#(V1)
p13: active#(plus(N,|0|())) -> mark#(U11(isNat(N),N))
p14: active#(plus(N,|0|())) -> U11#(isNat(N),N)
p15: active#(plus(N,|0|())) -> isNat#(N)
p16: active#(plus(N,s(M))) -> mark#(U21(and(isNat(M),isNat(N)),M,N))
p17: active#(plus(N,s(M))) -> U21#(and(isNat(M),isNat(N)),M,N)
p18: active#(plus(N,s(M))) -> and#(isNat(M),isNat(N))
p19: active#(plus(N,s(M))) -> isNat#(M)
p20: active#(plus(N,s(M))) -> isNat#(N)
p21: mark#(U11(X1,X2)) -> active#(U11(mark(X1),X2))
p22: mark#(U11(X1,X2)) -> U11#(mark(X1),X2)
p23: mark#(U11(X1,X2)) -> mark#(X1)
p24: mark#(tt()) -> active#(tt())
p25: mark#(U21(X1,X2,X3)) -> active#(U21(mark(X1),X2,X3))
p26: mark#(U21(X1,X2,X3)) -> U21#(mark(X1),X2,X3)
p27: mark#(U21(X1,X2,X3)) -> mark#(X1)
p28: mark#(s(X)) -> active#(s(mark(X)))
p29: mark#(s(X)) -> s#(mark(X))
p30: mark#(s(X)) -> mark#(X)
p31: mark#(plus(X1,X2)) -> active#(plus(mark(X1),mark(X2)))
p32: mark#(plus(X1,X2)) -> plus#(mark(X1),mark(X2))
p33: mark#(plus(X1,X2)) -> mark#(X1)
p34: mark#(plus(X1,X2)) -> mark#(X2)
p35: mark#(and(X1,X2)) -> active#(and(mark(X1),X2))
p36: mark#(and(X1,X2)) -> and#(mark(X1),X2)
p37: mark#(and(X1,X2)) -> mark#(X1)
p38: mark#(isNat(X)) -> active#(isNat(X))
p39: mark#(|0|()) -> active#(|0|())
p40: U11#(mark(X1),X2) -> U11#(X1,X2)
p41: U11#(X1,mark(X2)) -> U11#(X1,X2)
p42: U11#(active(X1),X2) -> U11#(X1,X2)
p43: U11#(X1,active(X2)) -> U11#(X1,X2)
p44: U21#(mark(X1),X2,X3) -> U21#(X1,X2,X3)
p45: U21#(X1,mark(X2),X3) -> U21#(X1,X2,X3)
p46: U21#(X1,X2,mark(X3)) -> U21#(X1,X2,X3)
p47: U21#(active(X1),X2,X3) -> U21#(X1,X2,X3)
p48: U21#(X1,active(X2),X3) -> U21#(X1,X2,X3)
p49: U21#(X1,X2,active(X3)) -> U21#(X1,X2,X3)
p50: s#(mark(X)) -> s#(X)
p51: s#(active(X)) -> s#(X)
p52: plus#(mark(X1),X2) -> plus#(X1,X2)
p53: plus#(X1,mark(X2)) -> plus#(X1,X2)
p54: plus#(active(X1),X2) -> plus#(X1,X2)
p55: plus#(X1,active(X2)) -> plus#(X1,X2)
p56: and#(mark(X1),X2) -> and#(X1,X2)
p57: and#(X1,mark(X2)) -> and#(X1,X2)
p58: and#(active(X1),X2) -> and#(X1,X2)
p59: and#(X1,active(X2)) -> and#(X1,X2)
p60: isNat#(mark(X)) -> isNat#(X)
p61: isNat#(active(X)) -> isNat#(X)

and R consists of:

r1: active(U11(tt(),N)) -> mark(N)
r2: active(U21(tt(),M,N)) -> mark(s(plus(N,M)))
r3: active(and(tt(),X)) -> mark(X)
r4: active(isNat(|0|())) -> mark(tt())
r5: active(isNat(plus(V1,V2))) -> mark(and(isNat(V1),isNat(V2)))
r6: active(isNat(s(V1))) -> mark(isNat(V1))
r7: active(plus(N,|0|())) -> mark(U11(isNat(N),N))
r8: active(plus(N,s(M))) -> mark(U21(and(isNat(M),isNat(N)),M,N))
r9: mark(U11(X1,X2)) -> active(U11(mark(X1),X2))
r10: mark(tt()) -> active(tt())
r11: mark(U21(X1,X2,X3)) -> active(U21(mark(X1),X2,X3))
r12: mark(s(X)) -> active(s(mark(X)))
r13: mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2)))
r14: mark(and(X1,X2)) -> active(and(mark(X1),X2))
r15: mark(isNat(X)) -> active(isNat(X))
r16: mark(|0|()) -> active(|0|())
r17: U11(mark(X1),X2) -> U11(X1,X2)
r18: U11(X1,mark(X2)) -> U11(X1,X2)
r19: U11(active(X1),X2) -> U11(X1,X2)
r20: U11(X1,active(X2)) -> U11(X1,X2)
r21: U21(mark(X1),X2,X3) -> U21(X1,X2,X3)
r22: U21(X1,mark(X2),X3) -> U21(X1,X2,X3)
r23: U21(X1,X2,mark(X3)) -> U21(X1,X2,X3)
r24: U21(active(X1),X2,X3) -> U21(X1,X2,X3)
r25: U21(X1,active(X2),X3) -> U21(X1,X2,X3)
r26: U21(X1,X2,active(X3)) -> U21(X1,X2,X3)
r27: s(mark(X)) -> s(X)
r28: s(active(X)) -> s(X)
r29: plus(mark(X1),X2) -> plus(X1,X2)
r30: plus(X1,mark(X2)) -> plus(X1,X2)
r31: plus(active(X1),X2) -> plus(X1,X2)
r32: plus(X1,active(X2)) -> plus(X1,X2)
r33: and(mark(X1),X2) -> and(X1,X2)
r34: and(X1,mark(X2)) -> and(X1,X2)
r35: and(active(X1),X2) -> and(X1,X2)
r36: and(X1,active(X2)) -> and(X1,X2)
r37: isNat(mark(X)) -> isNat(X)
r38: isNat(active(X)) -> isNat(X)

The estimated dependency graph contains the following SCCs:

  {p1, p2, p5, p7, p11, p13, p16, p21, p23, p25, p27, p28, p30, p31, p33, p34, p35, p37, p38}
  {p50, p51}
  {p52, p53, p54, p55}
  {p56, p57, p58, p59}
  {p60, p61}
  {p40, p41, p42, p43}
  {p44, p45, p46, p47, p48, p49}


-- Reduction pair.

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

p1: active#(U11(tt(),N)) -> mark#(N)
p2: mark#(isNat(X)) -> active#(isNat(X))
p3: active#(plus(N,s(M))) -> mark#(U21(and(isNat(M),isNat(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#(U11(isNat(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#(isNat(s(V1))) -> mark#(isNat(V1))
p11: mark#(s(X)) -> mark#(X)
p12: mark#(s(X)) -> active#(s(mark(X)))
p13: active#(isNat(plus(V1,V2))) -> mark#(and(isNat(V1),isNat(V2)))
p14: mark#(U21(X1,X2,X3)) -> mark#(X1)
p15: mark#(U21(X1,X2,X3)) -> active#(U21(mark(X1),X2,X3))
p16: active#(and(tt(),X)) -> mark#(X)
p17: mark#(U11(X1,X2)) -> mark#(X1)
p18: mark#(U11(X1,X2)) -> active#(U11(mark(X1),X2))
p19: active#(U21(tt(),M,N)) -> mark#(s(plus(N,M)))

and R consists of:

r1: active(U11(tt(),N)) -> mark(N)
r2: active(U21(tt(),M,N)) -> mark(s(plus(N,M)))
r3: active(and(tt(),X)) -> mark(X)
r4: active(isNat(|0|())) -> mark(tt())
r5: active(isNat(plus(V1,V2))) -> mark(and(isNat(V1),isNat(V2)))
r6: active(isNat(s(V1))) -> mark(isNat(V1))
r7: active(plus(N,|0|())) -> mark(U11(isNat(N),N))
r8: active(plus(N,s(M))) -> mark(U21(and(isNat(M),isNat(N)),M,N))
r9: mark(U11(X1,X2)) -> active(U11(mark(X1),X2))
r10: mark(tt()) -> active(tt())
r11: mark(U21(X1,X2,X3)) -> active(U21(mark(X1),X2,X3))
r12: mark(s(X)) -> active(s(mark(X)))
r13: mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2)))
r14: mark(and(X1,X2)) -> active(and(mark(X1),X2))
r15: mark(isNat(X)) -> active(isNat(X))
r16: mark(|0|()) -> active(|0|())
r17: U11(mark(X1),X2) -> U11(X1,X2)
r18: U11(X1,mark(X2)) -> U11(X1,X2)
r19: U11(active(X1),X2) -> U11(X1,X2)
r20: U11(X1,active(X2)) -> U11(X1,X2)
r21: U21(mark(X1),X2,X3) -> U21(X1,X2,X3)
r22: U21(X1,mark(X2),X3) -> U21(X1,X2,X3)
r23: U21(X1,X2,mark(X3)) -> U21(X1,X2,X3)
r24: U21(active(X1),X2,X3) -> U21(X1,X2,X3)
r25: U21(X1,active(X2),X3) -> U21(X1,X2,X3)
r26: U21(X1,X2,active(X3)) -> U21(X1,X2,X3)
r27: s(mark(X)) -> s(X)
r28: s(active(X)) -> s(X)
r29: plus(mark(X1),X2) -> plus(X1,X2)
r30: plus(X1,mark(X2)) -> plus(X1,X2)
r31: plus(active(X1),X2) -> plus(X1,X2)
r32: plus(X1,active(X2)) -> plus(X1,X2)
r33: and(mark(X1),X2) -> and(X1,X2)
r34: and(X1,mark(X2)) -> and(X1,X2)
r35: and(active(X1),X2) -> and(X1,X2)
r36: and(X1,active(X2)) -> and(X1,X2)
r37: isNat(mark(X)) -> isNat(X)
r38: isNat(active(X)) -> isNat(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

Take the reduction pair:

  matrix interpretations:
  
    carrier: N^4
    order: lexicographic order
    interpretations:
      active#_A(x1) = ((0,0,0,0),(1,0,0,0),(0,1,0,0),(0,1,0,0)) x1 + (0,0,0,3)
      U11_A(x1,x2) = x1 + ((1,0,0,0),(0,1,0,0),(1,1,0,0),(0,1,0,0)) x2 + (1,0,1,0)
      tt_A() = (0,6,1,0)
      mark#_A(x1) = ((0,0,0,0),(1,0,0,0),(0,1,0,0),(1,0,1,0)) x1 + (0,0,2,0)
      isNat_A(x1) = ((0,0,0,0),(1,0,0,0),(1,0,0,0),(0,0,0,0)) x1 + (0,6,10,1)
      plus_A(x1,x2) = ((1,0,0,0),(0,0,0,0),(0,0,0,0),(0,1,0,0)) x1 + x2 + (15,36,55,1)
      s_A(x1) = x1 + (3,1,2,0)
      U21_A(x1,x2,x3) = x1 + ((1,0,0,0),(0,0,0,0),(0,0,0,0),(0,1,0,0)) x2 + ((1,0,0,0),(0,0,0,0),(0,1,0,0),(0,1,0,0)) x3 + (18,18,20,0)
      and_A(x1,x2) = ((1,0,0,0),(1,1,0,0),(1,0,1,0),(1,0,0,0)) x1 + x2 + (0,4,1,0)
      mark_A(x1) = ((1,0,0,0),(0,1,0,0),(1,1,1,0),(0,0,0,0)) x1 + (0,1,1,19)
      |0|_A() = (1,2,0,0)
      active_A(x1) = ((1,0,0,0),(0,1,0,0),(0,0,1,0),(1,0,0,0)) x1 + (0,0,3,0)

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

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(),N)) -> mark(N)
r2: active(U21(tt(),M,N)) -> mark(s(plus(N,M)))
r3: active(and(tt(),X)) -> mark(X)
r4: active(isNat(|0|())) -> mark(tt())
r5: active(isNat(plus(V1,V2))) -> mark(and(isNat(V1),isNat(V2)))
r6: active(isNat(s(V1))) -> mark(isNat(V1))
r7: active(plus(N,|0|())) -> mark(U11(isNat(N),N))
r8: active(plus(N,s(M))) -> mark(U21(and(isNat(M),isNat(N)),M,N))
r9: mark(U11(X1,X2)) -> active(U11(mark(X1),X2))
r10: mark(tt()) -> active(tt())
r11: mark(U21(X1,X2,X3)) -> active(U21(mark(X1),X2,X3))
r12: mark(s(X)) -> active(s(mark(X)))
r13: mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2)))
r14: mark(and(X1,X2)) -> active(and(mark(X1),X2))
r15: mark(isNat(X)) -> active(isNat(X))
r16: mark(|0|()) -> active(|0|())
r17: U11(mark(X1),X2) -> U11(X1,X2)
r18: U11(X1,mark(X2)) -> U11(X1,X2)
r19: U11(active(X1),X2) -> U11(X1,X2)
r20: U11(X1,active(X2)) -> U11(X1,X2)
r21: U21(mark(X1),X2,X3) -> U21(X1,X2,X3)
r22: U21(X1,mark(X2),X3) -> U21(X1,X2,X3)
r23: U21(X1,X2,mark(X3)) -> U21(X1,X2,X3)
r24: U21(active(X1),X2,X3) -> U21(X1,X2,X3)
r25: U21(X1,active(X2),X3) -> U21(X1,X2,X3)
r26: U21(X1,X2,active(X3)) -> U21(X1,X2,X3)
r27: s(mark(X)) -> s(X)
r28: s(active(X)) -> s(X)
r29: plus(mark(X1),X2) -> plus(X1,X2)
r30: plus(X1,mark(X2)) -> plus(X1,X2)
r31: plus(active(X1),X2) -> plus(X1,X2)
r32: plus(X1,active(X2)) -> plus(X1,X2)
r33: and(mark(X1),X2) -> and(X1,X2)
r34: and(X1,mark(X2)) -> and(X1,X2)
r35: and(active(X1),X2) -> and(X1,X2)
r36: and(X1,active(X2)) -> and(X1,X2)
r37: isNat(mark(X)) -> isNat(X)
r38: isNat(active(X)) -> isNat(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),(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)
      active_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

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(),N)) -> mark(N)
r2: active(U21(tt(),M,N)) -> mark(s(plus(N,M)))
r3: active(and(tt(),X)) -> mark(X)
r4: active(isNat(|0|())) -> mark(tt())
r5: active(isNat(plus(V1,V2))) -> mark(and(isNat(V1),isNat(V2)))
r6: active(isNat(s(V1))) -> mark(isNat(V1))
r7: active(plus(N,|0|())) -> mark(U11(isNat(N),N))
r8: active(plus(N,s(M))) -> mark(U21(and(isNat(M),isNat(N)),M,N))
r9: mark(U11(X1,X2)) -> active(U11(mark(X1),X2))
r10: mark(tt()) -> active(tt())
r11: mark(U21(X1,X2,X3)) -> active(U21(mark(X1),X2,X3))
r12: mark(s(X)) -> active(s(mark(X)))
r13: mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2)))
r14: mark(and(X1,X2)) -> active(and(mark(X1),X2))
r15: mark(isNat(X)) -> active(isNat(X))
r16: mark(|0|()) -> active(|0|())
r17: U11(mark(X1),X2) -> U11(X1,X2)
r18: U11(X1,mark(X2)) -> U11(X1,X2)
r19: U11(active(X1),X2) -> U11(X1,X2)
r20: U11(X1,active(X2)) -> U11(X1,X2)
r21: U21(mark(X1),X2,X3) -> U21(X1,X2,X3)
r22: U21(X1,mark(X2),X3) -> U21(X1,X2,X3)
r23: U21(X1,X2,mark(X3)) -> U21(X1,X2,X3)
r24: U21(active(X1),X2,X3) -> U21(X1,X2,X3)
r25: U21(X1,active(X2),X3) -> U21(X1,X2,X3)
r26: U21(X1,X2,active(X3)) -> U21(X1,X2,X3)
r27: s(mark(X)) -> s(X)
r28: s(active(X)) -> s(X)
r29: plus(mark(X1),X2) -> plus(X1,X2)
r30: plus(X1,mark(X2)) -> plus(X1,X2)
r31: plus(active(X1),X2) -> plus(X1,X2)
r32: plus(X1,active(X2)) -> plus(X1,X2)
r33: and(mark(X1),X2) -> and(X1,X2)
r34: and(X1,mark(X2)) -> and(X1,X2)
r35: and(active(X1),X2) -> and(X1,X2)
r36: and(X1,active(X2)) -> and(X1,X2)
r37: isNat(mark(X)) -> isNat(X)
r38: isNat(active(X)) -> isNat(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,1,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),(0,1,1,1)) x1 + (1,1,1,1)
      active_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, 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

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(),N)) -> mark(N)
r2: active(U21(tt(),M,N)) -> mark(s(plus(N,M)))
r3: active(and(tt(),X)) -> mark(X)
r4: active(isNat(|0|())) -> mark(tt())
r5: active(isNat(plus(V1,V2))) -> mark(and(isNat(V1),isNat(V2)))
r6: active(isNat(s(V1))) -> mark(isNat(V1))
r7: active(plus(N,|0|())) -> mark(U11(isNat(N),N))
r8: active(plus(N,s(M))) -> mark(U21(and(isNat(M),isNat(N)),M,N))
r9: mark(U11(X1,X2)) -> active(U11(mark(X1),X2))
r10: mark(tt()) -> active(tt())
r11: mark(U21(X1,X2,X3)) -> active(U21(mark(X1),X2,X3))
r12: mark(s(X)) -> active(s(mark(X)))
r13: mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2)))
r14: mark(and(X1,X2)) -> active(and(mark(X1),X2))
r15: mark(isNat(X)) -> active(isNat(X))
r16: mark(|0|()) -> active(|0|())
r17: U11(mark(X1),X2) -> U11(X1,X2)
r18: U11(X1,mark(X2)) -> U11(X1,X2)
r19: U11(active(X1),X2) -> U11(X1,X2)
r20: U11(X1,active(X2)) -> U11(X1,X2)
r21: U21(mark(X1),X2,X3) -> U21(X1,X2,X3)
r22: U21(X1,mark(X2),X3) -> U21(X1,X2,X3)
r23: U21(X1,X2,mark(X3)) -> U21(X1,X2,X3)
r24: U21(active(X1),X2,X3) -> U21(X1,X2,X3)
r25: U21(X1,active(X2),X3) -> U21(X1,X2,X3)
r26: U21(X1,X2,active(X3)) -> U21(X1,X2,X3)
r27: s(mark(X)) -> s(X)
r28: s(active(X)) -> s(X)
r29: plus(mark(X1),X2) -> plus(X1,X2)
r30: plus(X1,mark(X2)) -> plus(X1,X2)
r31: plus(active(X1),X2) -> plus(X1,X2)
r32: plus(X1,active(X2)) -> plus(X1,X2)
r33: and(mark(X1),X2) -> and(X1,X2)
r34: and(X1,mark(X2)) -> and(X1,X2)
r35: and(active(X1),X2) -> and(X1,X2)
r36: and(X1,active(X2)) -> and(X1,X2)
r37: isNat(mark(X)) -> isNat(X)
r38: isNat(active(X)) -> isNat(X)

The set of usable rules consists of

  (no rules)

Take the monotone 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,1,0),(1,1,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),(0,1,1,1)) x1 + (1,1,1,1)
      active_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, 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

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(),N)) -> mark(N)
r2: active(U21(tt(),M,N)) -> mark(s(plus(N,M)))
r3: active(and(tt(),X)) -> mark(X)
r4: active(isNat(|0|())) -> mark(tt())
r5: active(isNat(plus(V1,V2))) -> mark(and(isNat(V1),isNat(V2)))
r6: active(isNat(s(V1))) -> mark(isNat(V1))
r7: active(plus(N,|0|())) -> mark(U11(isNat(N),N))
r8: active(plus(N,s(M))) -> mark(U21(and(isNat(M),isNat(N)),M,N))
r9: mark(U11(X1,X2)) -> active(U11(mark(X1),X2))
r10: mark(tt()) -> active(tt())
r11: mark(U21(X1,X2,X3)) -> active(U21(mark(X1),X2,X3))
r12: mark(s(X)) -> active(s(mark(X)))
r13: mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2)))
r14: mark(and(X1,X2)) -> active(and(mark(X1),X2))
r15: mark(isNat(X)) -> active(isNat(X))
r16: mark(|0|()) -> active(|0|())
r17: U11(mark(X1),X2) -> U11(X1,X2)
r18: U11(X1,mark(X2)) -> U11(X1,X2)
r19: U11(active(X1),X2) -> U11(X1,X2)
r20: U11(X1,active(X2)) -> U11(X1,X2)
r21: U21(mark(X1),X2,X3) -> U21(X1,X2,X3)
r22: U21(X1,mark(X2),X3) -> U21(X1,X2,X3)
r23: U21(X1,X2,mark(X3)) -> U21(X1,X2,X3)
r24: U21(active(X1),X2,X3) -> U21(X1,X2,X3)
r25: U21(X1,active(X2),X3) -> U21(X1,X2,X3)
r26: U21(X1,X2,active(X3)) -> U21(X1,X2,X3)
r27: s(mark(X)) -> s(X)
r28: s(active(X)) -> s(X)
r29: plus(mark(X1),X2) -> plus(X1,X2)
r30: plus(X1,mark(X2)) -> plus(X1,X2)
r31: plus(active(X1),X2) -> plus(X1,X2)
r32: plus(X1,active(X2)) -> plus(X1,X2)
r33: and(mark(X1),X2) -> and(X1,X2)
r34: and(X1,mark(X2)) -> and(X1,X2)
r35: and(active(X1),X2) -> and(X1,X2)
r36: and(X1,active(X2)) -> and(X1,X2)
r37: isNat(mark(X)) -> isNat(X)
r38: isNat(active(X)) -> isNat(X)

The set of usable rules consists of

  (no rules)

Take the monotone reduction pair:

  matrix interpretations:
  
    carrier: N^4
    order: lexicographic order
    interpretations:
      isNat#_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)
      active_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

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

and R consists of:

r1: active(U11(tt(),N)) -> mark(N)
r2: active(U21(tt(),M,N)) -> mark(s(plus(N,M)))
r3: active(and(tt(),X)) -> mark(X)
r4: active(isNat(|0|())) -> mark(tt())
r5: active(isNat(plus(V1,V2))) -> mark(and(isNat(V1),isNat(V2)))
r6: active(isNat(s(V1))) -> mark(isNat(V1))
r7: active(plus(N,|0|())) -> mark(U11(isNat(N),N))
r8: active(plus(N,s(M))) -> mark(U21(and(isNat(M),isNat(N)),M,N))
r9: mark(U11(X1,X2)) -> active(U11(mark(X1),X2))
r10: mark(tt()) -> active(tt())
r11: mark(U21(X1,X2,X3)) -> active(U21(mark(X1),X2,X3))
r12: mark(s(X)) -> active(s(mark(X)))
r13: mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2)))
r14: mark(and(X1,X2)) -> active(and(mark(X1),X2))
r15: mark(isNat(X)) -> active(isNat(X))
r16: mark(|0|()) -> active(|0|())
r17: U11(mark(X1),X2) -> U11(X1,X2)
r18: U11(X1,mark(X2)) -> U11(X1,X2)
r19: U11(active(X1),X2) -> U11(X1,X2)
r20: U11(X1,active(X2)) -> U11(X1,X2)
r21: U21(mark(X1),X2,X3) -> U21(X1,X2,X3)
r22: U21(X1,mark(X2),X3) -> U21(X1,X2,X3)
r23: U21(X1,X2,mark(X3)) -> U21(X1,X2,X3)
r24: U21(active(X1),X2,X3) -> U21(X1,X2,X3)
r25: U21(X1,active(X2),X3) -> U21(X1,X2,X3)
r26: U21(X1,X2,active(X3)) -> U21(X1,X2,X3)
r27: s(mark(X)) -> s(X)
r28: s(active(X)) -> s(X)
r29: plus(mark(X1),X2) -> plus(X1,X2)
r30: plus(X1,mark(X2)) -> plus(X1,X2)
r31: plus(active(X1),X2) -> plus(X1,X2)
r32: plus(X1,active(X2)) -> plus(X1,X2)
r33: and(mark(X1),X2) -> and(X1,X2)
r34: and(X1,mark(X2)) -> and(X1,X2)
r35: and(active(X1),X2) -> and(X1,X2)
r36: and(X1,active(X2)) -> and(X1,X2)
r37: isNat(mark(X)) -> isNat(X)
r38: isNat(active(X)) -> isNat(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) = ((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
      mark_A(x1) = ((1,0,0,0),(1,1,0,0),(1,1,1,0),(0,1,1,1)) x1 + (1,1,1,1)
      active_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, 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

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

and R consists of:

r1: active(U11(tt(),N)) -> mark(N)
r2: active(U21(tt(),M,N)) -> mark(s(plus(N,M)))
r3: active(and(tt(),X)) -> mark(X)
r4: active(isNat(|0|())) -> mark(tt())
r5: active(isNat(plus(V1,V2))) -> mark(and(isNat(V1),isNat(V2)))
r6: active(isNat(s(V1))) -> mark(isNat(V1))
r7: active(plus(N,|0|())) -> mark(U11(isNat(N),N))
r8: active(plus(N,s(M))) -> mark(U21(and(isNat(M),isNat(N)),M,N))
r9: mark(U11(X1,X2)) -> active(U11(mark(X1),X2))
r10: mark(tt()) -> active(tt())
r11: mark(U21(X1,X2,X3)) -> active(U21(mark(X1),X2,X3))
r12: mark(s(X)) -> active(s(mark(X)))
r13: mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2)))
r14: mark(and(X1,X2)) -> active(and(mark(X1),X2))
r15: mark(isNat(X)) -> active(isNat(X))
r16: mark(|0|()) -> active(|0|())
r17: U11(mark(X1),X2) -> U11(X1,X2)
r18: U11(X1,mark(X2)) -> U11(X1,X2)
r19: U11(active(X1),X2) -> U11(X1,X2)
r20: U11(X1,active(X2)) -> U11(X1,X2)
r21: U21(mark(X1),X2,X3) -> U21(X1,X2,X3)
r22: U21(X1,mark(X2),X3) -> U21(X1,X2,X3)
r23: U21(X1,X2,mark(X3)) -> U21(X1,X2,X3)
r24: U21(active(X1),X2,X3) -> U21(X1,X2,X3)
r25: U21(X1,active(X2),X3) -> U21(X1,X2,X3)
r26: U21(X1,X2,active(X3)) -> U21(X1,X2,X3)
r27: s(mark(X)) -> s(X)
r28: s(active(X)) -> s(X)
r29: plus(mark(X1),X2) -> plus(X1,X2)
r30: plus(X1,mark(X2)) -> plus(X1,X2)
r31: plus(active(X1),X2) -> plus(X1,X2)
r32: plus(X1,active(X2)) -> plus(X1,X2)
r33: and(mark(X1),X2) -> and(X1,X2)
r34: and(X1,mark(X2)) -> and(X1,X2)
r35: and(active(X1),X2) -> and(X1,X2)
r36: and(X1,active(X2)) -> and(X1,X2)
r37: isNat(mark(X)) -> isNat(X)
r38: isNat(active(X)) -> isNat(X)

The set of usable rules consists of

  (no rules)

Take the monotone reduction pair:

  matrix interpretations:
  
    carrier: N^4
    order: lexicographic order
    interpretations:
      U21#_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)
      active_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, p4, p5, p6
  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

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