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))
  active(U11(X1,X2)) -> U11(active(X1),X2)
  active(U21(X1,X2,X3)) -> U21(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) -> mark(U11(X1,X2))
  U21(mark(X1),X2,X3) -> mark(U21(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)) -> U11(proper(X1),proper(X2))
  proper(tt()) -> ok(tt())
  proper(U21(X1,X2,X3)) -> U21(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(isNat(X)) -> isNat(proper(X))
  proper(|0|()) -> ok(|0|())
  U11(ok(X1),ok(X2)) -> ok(U11(X1,X2))
  U21(ok(X1),ok(X2),ok(X3)) -> ok(U21(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))
  isNat(ok(X)) -> ok(isNat(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#(U21(tt(),M,N)) -> s#(plus(N,M))
p2: active#(U21(tt(),M,N)) -> plus#(N,M)
p3: active#(isNat(plus(V1,V2))) -> and#(isNat(V1),isNat(V2))
p4: active#(isNat(plus(V1,V2))) -> isNat#(V1)
p5: active#(isNat(plus(V1,V2))) -> isNat#(V2)
p6: active#(isNat(s(V1))) -> isNat#(V1)
p7: active#(plus(N,|0|())) -> U11#(isNat(N),N)
p8: active#(plus(N,|0|())) -> isNat#(N)
p9: active#(plus(N,s(M))) -> U21#(and(isNat(M),isNat(N)),M,N)
p10: active#(plus(N,s(M))) -> and#(isNat(M),isNat(N))
p11: active#(plus(N,s(M))) -> isNat#(M)
p12: active#(plus(N,s(M))) -> isNat#(N)
p13: active#(U11(X1,X2)) -> U11#(active(X1),X2)
p14: active#(U11(X1,X2)) -> active#(X1)
p15: active#(U21(X1,X2,X3)) -> U21#(active(X1),X2,X3)
p16: active#(U21(X1,X2,X3)) -> active#(X1)
p17: active#(s(X)) -> s#(active(X))
p18: active#(s(X)) -> active#(X)
p19: active#(plus(X1,X2)) -> plus#(active(X1),X2)
p20: active#(plus(X1,X2)) -> active#(X1)
p21: active#(plus(X1,X2)) -> plus#(X1,active(X2))
p22: active#(plus(X1,X2)) -> active#(X2)
p23: active#(and(X1,X2)) -> and#(active(X1),X2)
p24: active#(and(X1,X2)) -> active#(X1)
p25: U11#(mark(X1),X2) -> U11#(X1,X2)
p26: U21#(mark(X1),X2,X3) -> U21#(X1,X2,X3)
p27: s#(mark(X)) -> s#(X)
p28: plus#(mark(X1),X2) -> plus#(X1,X2)
p29: plus#(X1,mark(X2)) -> plus#(X1,X2)
p30: and#(mark(X1),X2) -> and#(X1,X2)
p31: proper#(U11(X1,X2)) -> U11#(proper(X1),proper(X2))
p32: proper#(U11(X1,X2)) -> proper#(X1)
p33: proper#(U11(X1,X2)) -> proper#(X2)
p34: proper#(U21(X1,X2,X3)) -> U21#(proper(X1),proper(X2),proper(X3))
p35: proper#(U21(X1,X2,X3)) -> proper#(X1)
p36: proper#(U21(X1,X2,X3)) -> proper#(X2)
p37: proper#(U21(X1,X2,X3)) -> proper#(X3)
p38: proper#(s(X)) -> s#(proper(X))
p39: proper#(s(X)) -> proper#(X)
p40: proper#(plus(X1,X2)) -> plus#(proper(X1),proper(X2))
p41: proper#(plus(X1,X2)) -> proper#(X1)
p42: proper#(plus(X1,X2)) -> proper#(X2)
p43: proper#(and(X1,X2)) -> and#(proper(X1),proper(X2))
p44: proper#(and(X1,X2)) -> proper#(X1)
p45: proper#(and(X1,X2)) -> proper#(X2)
p46: proper#(isNat(X)) -> isNat#(proper(X))
p47: proper#(isNat(X)) -> proper#(X)
p48: U11#(ok(X1),ok(X2)) -> U11#(X1,X2)
p49: U21#(ok(X1),ok(X2),ok(X3)) -> U21#(X1,X2,X3)
p50: s#(ok(X)) -> s#(X)
p51: plus#(ok(X1),ok(X2)) -> plus#(X1,X2)
p52: and#(ok(X1),ok(X2)) -> and#(X1,X2)
p53: isNat#(ok(X)) -> isNat#(X)
p54: top#(mark(X)) -> top#(proper(X))
p55: top#(mark(X)) -> proper#(X)
p56: top#(ok(X)) -> top#(active(X))
p57: top#(ok(X)) -> active#(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: active(U11(X1,X2)) -> U11(active(X1),X2)
r10: active(U21(X1,X2,X3)) -> U21(active(X1),X2,X3)
r11: active(s(X)) -> s(active(X))
r12: active(plus(X1,X2)) -> plus(active(X1),X2)
r13: active(plus(X1,X2)) -> plus(X1,active(X2))
r14: active(and(X1,X2)) -> and(active(X1),X2)
r15: U11(mark(X1),X2) -> mark(U11(X1,X2))
r16: U21(mark(X1),X2,X3) -> mark(U21(X1,X2,X3))
r17: s(mark(X)) -> mark(s(X))
r18: plus(mark(X1),X2) -> mark(plus(X1,X2))
r19: plus(X1,mark(X2)) -> mark(plus(X1,X2))
r20: and(mark(X1),X2) -> mark(and(X1,X2))
r21: proper(U11(X1,X2)) -> U11(proper(X1),proper(X2))
r22: proper(tt()) -> ok(tt())
r23: proper(U21(X1,X2,X3)) -> U21(proper(X1),proper(X2),proper(X3))
r24: proper(s(X)) -> s(proper(X))
r25: proper(plus(X1,X2)) -> plus(proper(X1),proper(X2))
r26: proper(and(X1,X2)) -> and(proper(X1),proper(X2))
r27: proper(isNat(X)) -> isNat(proper(X))
r28: proper(|0|()) -> ok(|0|())
r29: U11(ok(X1),ok(X2)) -> ok(U11(X1,X2))
r30: U21(ok(X1),ok(X2),ok(X3)) -> ok(U21(X1,X2,X3))
r31: s(ok(X)) -> ok(s(X))
r32: plus(ok(X1),ok(X2)) -> ok(plus(X1,X2))
r33: and(ok(X1),ok(X2)) -> ok(and(X1,X2))
r34: isNat(ok(X)) -> ok(isNat(X))
r35: top(mark(X)) -> top(proper(X))
r36: top(ok(X)) -> top(active(X))

The estimated dependency graph contains the following SCCs:

  {p54, p56}
  {p14, p16, p18, p20, p22, p24}
  {p32, p33, p35, p36, p37, p39, p41, p42, p44, p45, p47}
  {p27, p50}
  {p28, p29, p51}
  {p30, p52}
  {p53}
  {p25, p48}
  {p26, p49}


-- 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(),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: active(U11(X1,X2)) -> U11(active(X1),X2)
r10: active(U21(X1,X2,X3)) -> U21(active(X1),X2,X3)
r11: active(s(X)) -> s(active(X))
r12: active(plus(X1,X2)) -> plus(active(X1),X2)
r13: active(plus(X1,X2)) -> plus(X1,active(X2))
r14: active(and(X1,X2)) -> and(active(X1),X2)
r15: U11(mark(X1),X2) -> mark(U11(X1,X2))
r16: U21(mark(X1),X2,X3) -> mark(U21(X1,X2,X3))
r17: s(mark(X)) -> mark(s(X))
r18: plus(mark(X1),X2) -> mark(plus(X1,X2))
r19: plus(X1,mark(X2)) -> mark(plus(X1,X2))
r20: and(mark(X1),X2) -> mark(and(X1,X2))
r21: proper(U11(X1,X2)) -> U11(proper(X1),proper(X2))
r22: proper(tt()) -> ok(tt())
r23: proper(U21(X1,X2,X3)) -> U21(proper(X1),proper(X2),proper(X3))
r24: proper(s(X)) -> s(proper(X))
r25: proper(plus(X1,X2)) -> plus(proper(X1),proper(X2))
r26: proper(and(X1,X2)) -> and(proper(X1),proper(X2))
r27: proper(isNat(X)) -> isNat(proper(X))
r28: proper(|0|()) -> ok(|0|())
r29: U11(ok(X1),ok(X2)) -> ok(U11(X1,X2))
r30: U21(ok(X1),ok(X2),ok(X3)) -> ok(U21(X1,X2,X3))
r31: s(ok(X)) -> ok(s(X))
r32: plus(ok(X1),ok(X2)) -> ok(plus(X1,X2))
r33: and(ok(X1),ok(X2)) -> ok(and(X1,X2))
r34: isNat(ok(X)) -> ok(isNat(X))
r35: top(mark(X)) -> top(proper(X))
r36: 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

Take the reduction pair:

  matrix interpretations:
  
    carrier: N^4
    order: lexicographic order
    interpretations:
      top#_A(x1) = ((0,0,0,0),(1,0,0,0),(1,1,0,0),(1,0,1,0)) x1
      ok_A(x1) = x1
      active_A(x1) = ((1,0,0,0),(0,1,0,0),(0,0,1,0),(1,0,1,1)) x1 + (0,0,0,1)
      mark_A(x1) = x1 + (0,0,3,0)
      proper_A(x1) = x1
      U11_A(x1,x2) = x1 + ((1,0,0,0),(1,1,0,0),(1,1,1,0),(1,0,1,1)) x2 + (1,1,1,1)
      U21_A(x1,x2,x3) = ((1,0,0,0),(0,1,0,0),(1,0,1,0),(1,0,1,0)) x1 + ((1,0,0,0),(1,1,0,0),(1,1,1,0),(0,0,0,0)) x2 + ((1,0,0,0),(0,1,0,0),(0,1,0,0),(0,0,0,0)) x3 + (9,3,1,1)
      s_A(x1) = ((1,0,0,0),(0,1,0,0),(1,1,1,0),(0,0,0,0)) x1 + (3,1,1,0)
      plus_A(x1,x2) = ((1,0,0,0),(0,1,0,0),(1,0,1,0),(0,0,0,0)) x1 + ((1,0,0,0),(1,1,0,0),(1,0,1,0),(0,0,0,0)) x2 + (6,1,1,1)
      and_A(x1,x2) = ((1,0,0,0),(1,1,0,0),(1,1,1,0),(1,0,0,1)) x1 + ((1,0,0,0),(0,1,0,0),(1,0,1,0),(1,1,1,0)) x2 + (0,0,3,0)
      isNat_A(x1) = ((0,0,0,0),(0,0,0,0),(1,0,0,0),(0,1,0,0)) x1
      tt_A() = (0,0,1,1)
      |0|_A() = (4,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(),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: active(U11(X1,X2)) -> U11(active(X1),X2)
r10: active(U21(X1,X2,X3)) -> U21(active(X1),X2,X3)
r11: active(s(X)) -> s(active(X))
r12: active(plus(X1,X2)) -> plus(active(X1),X2)
r13: active(plus(X1,X2)) -> plus(X1,active(X2))
r14: active(and(X1,X2)) -> and(active(X1),X2)
r15: U11(mark(X1),X2) -> mark(U11(X1,X2))
r16: U21(mark(X1),X2,X3) -> mark(U21(X1,X2,X3))
r17: s(mark(X)) -> mark(s(X))
r18: plus(mark(X1),X2) -> mark(plus(X1,X2))
r19: plus(X1,mark(X2)) -> mark(plus(X1,X2))
r20: and(mark(X1),X2) -> mark(and(X1,X2))
r21: proper(U11(X1,X2)) -> U11(proper(X1),proper(X2))
r22: proper(tt()) -> ok(tt())
r23: proper(U21(X1,X2,X3)) -> U21(proper(X1),proper(X2),proper(X3))
r24: proper(s(X)) -> s(proper(X))
r25: proper(plus(X1,X2)) -> plus(proper(X1),proper(X2))
r26: proper(and(X1,X2)) -> and(proper(X1),proper(X2))
r27: proper(isNat(X)) -> isNat(proper(X))
r28: proper(|0|()) -> ok(|0|())
r29: U11(ok(X1),ok(X2)) -> ok(U11(X1,X2))
r30: U21(ok(X1),ok(X2),ok(X3)) -> ok(U21(X1,X2,X3))
r31: s(ok(X)) -> ok(s(X))
r32: plus(ok(X1),ok(X2)) -> ok(plus(X1,X2))
r33: and(ok(X1),ok(X2)) -> ok(and(X1,X2))
r34: isNat(ok(X)) -> ok(isNat(X))
r35: top(mark(X)) -> top(proper(X))
r36: 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(),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: active(U11(X1,X2)) -> U11(active(X1),X2)
r10: active(U21(X1,X2,X3)) -> U21(active(X1),X2,X3)
r11: active(s(X)) -> s(active(X))
r12: active(plus(X1,X2)) -> plus(active(X1),X2)
r13: active(plus(X1,X2)) -> plus(X1,active(X2))
r14: active(and(X1,X2)) -> and(active(X1),X2)
r15: U11(mark(X1),X2) -> mark(U11(X1,X2))
r16: U21(mark(X1),X2,X3) -> mark(U21(X1,X2,X3))
r17: s(mark(X)) -> mark(s(X))
r18: plus(mark(X1),X2) -> mark(plus(X1,X2))
r19: plus(X1,mark(X2)) -> mark(plus(X1,X2))
r20: and(mark(X1),X2) -> mark(and(X1,X2))
r21: proper(U11(X1,X2)) -> U11(proper(X1),proper(X2))
r22: proper(tt()) -> ok(tt())
r23: proper(U21(X1,X2,X3)) -> U21(proper(X1),proper(X2),proper(X3))
r24: proper(s(X)) -> s(proper(X))
r25: proper(plus(X1,X2)) -> plus(proper(X1),proper(X2))
r26: proper(and(X1,X2)) -> and(proper(X1),proper(X2))
r27: proper(isNat(X)) -> isNat(proper(X))
r28: proper(|0|()) -> ok(|0|())
r29: U11(ok(X1),ok(X2)) -> ok(U11(X1,X2))
r30: U21(ok(X1),ok(X2),ok(X3)) -> ok(U21(X1,X2,X3))
r31: s(ok(X)) -> ok(s(X))
r32: plus(ok(X1),ok(X2)) -> ok(plus(X1,X2))
r33: and(ok(X1),ok(X2)) -> ok(and(X1,X2))
r34: isNat(ok(X)) -> ok(isNat(X))
r35: top(mark(X)) -> top(proper(X))
r36: 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, r29, r30, r31, r32, r33, r34

Take the reduction pair:

  matrix interpretations:
  
    carrier: N^4
    order: lexicographic order
    interpretations:
      top#_A(x1) = ((1,0,0,0),(0,1,0,0),(0,1,1,0),(1,0,1,0)) x1
      ok_A(x1) = ((1,0,0,0),(1,0,0,0),(0,0,0,0),(1,0,0,0)) x1 + (5,12,0,9)
      active_A(x1) = ((1,0,0,0),(1,1,0,0),(1,0,0,0),(0,0,0,0)) x1 + (4,1,12,8)
      U11_A(x1,x2) = x1 + ((0,0,0,0),(1,0,0,0),(0,0,0,0),(0,0,0,0)) x2 + (0,1,0,8)
      mark_A(x1) = ((0,0,0,0),(1,0,0,0),(1,1,0,0),(1,1,1,0)) x1 + (1,2,25,1)
      U21_A(x1,x2,x3) = ((1,0,0,0),(0,1,0,0),(1,0,1,0),(1,1,0,1)) x2 + ((0,0,0,0),(0,0,0,0),(0,0,0,0),(1,0,0,0)) x3 + (2,3,15,9)
      s_A(x1) = ((1,0,0,0),(1,0,0,0),(0,0,0,0),(0,0,0,0)) x1 + (3,10,1,1)
      plus_A(x1,x2) = ((1,0,0,0),(0,1,0,0),(0,1,1,0),(1,0,0,1)) x1 + x2 + (16,1,0,1)
      and_A(x1,x2) = ((0,0,0,0),(1,0,0,0),(0,1,0,0),(0,0,1,0)) x1 + ((1,0,0,0),(1,0,0,0),(1,0,0,0),(0,0,0,0)) x2 + (2,4,30,1)
      isNat_A(x1) = ((1,0,0,0),(1,1,0,0),(1,0,0,0),(0,0,0,0)) x1 + (4,0,1,1)
      tt_A() = (8,0,0,1)
      |0|_A() = (1,1,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#(U21(X1,X2,X3)) -> active#(X1)
p6: active#(U11(X1,X2)) -> active#(X1)

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: active(U11(X1,X2)) -> U11(active(X1),X2)
r10: active(U21(X1,X2,X3)) -> U21(active(X1),X2,X3)
r11: active(s(X)) -> s(active(X))
r12: active(plus(X1,X2)) -> plus(active(X1),X2)
r13: active(plus(X1,X2)) -> plus(X1,active(X2))
r14: active(and(X1,X2)) -> and(active(X1),X2)
r15: U11(mark(X1),X2) -> mark(U11(X1,X2))
r16: U21(mark(X1),X2,X3) -> mark(U21(X1,X2,X3))
r17: s(mark(X)) -> mark(s(X))
r18: plus(mark(X1),X2) -> mark(plus(X1,X2))
r19: plus(X1,mark(X2)) -> mark(plus(X1,X2))
r20: and(mark(X1),X2) -> mark(and(X1,X2))
r21: proper(U11(X1,X2)) -> U11(proper(X1),proper(X2))
r22: proper(tt()) -> ok(tt())
r23: proper(U21(X1,X2,X3)) -> U21(proper(X1),proper(X2),proper(X3))
r24: proper(s(X)) -> s(proper(X))
r25: proper(plus(X1,X2)) -> plus(proper(X1),proper(X2))
r26: proper(and(X1,X2)) -> and(proper(X1),proper(X2))
r27: proper(isNat(X)) -> isNat(proper(X))
r28: proper(|0|()) -> ok(|0|())
r29: U11(ok(X1),ok(X2)) -> ok(U11(X1,X2))
r30: U21(ok(X1),ok(X2),ok(X3)) -> ok(U21(X1,X2,X3))
r31: s(ok(X)) -> ok(s(X))
r32: plus(ok(X1),ok(X2)) -> ok(plus(X1,X2))
r33: and(ok(X1),ok(X2)) -> ok(and(X1,X2))
r34: isNat(ok(X)) -> ok(isNat(X))
r35: top(mark(X)) -> top(proper(X))
r36: 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:
      active#_A(x1) = ((1,0,0,0),(1,1,0,0),(1,1,1,0),(1,1,1,1)) 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)
      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,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)
      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 + (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

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#(isNat(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#(U21(X1,X2,X3)) -> proper#(X3)
p8: proper#(U21(X1,X2,X3)) -> proper#(X2)
p9: proper#(U21(X1,X2,X3)) -> proper#(X1)
p10: proper#(U11(X1,X2)) -> proper#(X2)
p11: proper#(U11(X1,X2)) -> proper#(X1)

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: active(U11(X1,X2)) -> U11(active(X1),X2)
r10: active(U21(X1,X2,X3)) -> U21(active(X1),X2,X3)
r11: active(s(X)) -> s(active(X))
r12: active(plus(X1,X2)) -> plus(active(X1),X2)
r13: active(plus(X1,X2)) -> plus(X1,active(X2))
r14: active(and(X1,X2)) -> and(active(X1),X2)
r15: U11(mark(X1),X2) -> mark(U11(X1,X2))
r16: U21(mark(X1),X2,X3) -> mark(U21(X1,X2,X3))
r17: s(mark(X)) -> mark(s(X))
r18: plus(mark(X1),X2) -> mark(plus(X1,X2))
r19: plus(X1,mark(X2)) -> mark(plus(X1,X2))
r20: and(mark(X1),X2) -> mark(and(X1,X2))
r21: proper(U11(X1,X2)) -> U11(proper(X1),proper(X2))
r22: proper(tt()) -> ok(tt())
r23: proper(U21(X1,X2,X3)) -> U21(proper(X1),proper(X2),proper(X3))
r24: proper(s(X)) -> s(proper(X))
r25: proper(plus(X1,X2)) -> plus(proper(X1),proper(X2))
r26: proper(and(X1,X2)) -> and(proper(X1),proper(X2))
r27: proper(isNat(X)) -> isNat(proper(X))
r28: proper(|0|()) -> ok(|0|())
r29: U11(ok(X1),ok(X2)) -> ok(U11(X1,X2))
r30: U21(ok(X1),ok(X2),ok(X3)) -> ok(U21(X1,X2,X3))
r31: s(ok(X)) -> ok(s(X))
r32: plus(ok(X1),ok(X2)) -> ok(plus(X1,X2))
r33: and(ok(X1),ok(X2)) -> ok(and(X1,X2))
r34: isNat(ok(X)) -> ok(isNat(X))
r35: top(mark(X)) -> top(proper(X))
r36: 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:
      proper#_A(x1) = ((1,0,0,0),(0,1,0,0),(1,1,1,0),(1,1,1,1)) x1
      isNat_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,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,0,1,0),(1,1,1,1)) x1 + (1,1,1,1)
      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,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)
      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 + (1,1,1,1)

The next rules are strictly ordered:

  p1, p2, p3, p4, p5, p6, p7, p8, p9, p10, p11
  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

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(),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: active(U11(X1,X2)) -> U11(active(X1),X2)
r10: active(U21(X1,X2,X3)) -> U21(active(X1),X2,X3)
r11: active(s(X)) -> s(active(X))
r12: active(plus(X1,X2)) -> plus(active(X1),X2)
r13: active(plus(X1,X2)) -> plus(X1,active(X2))
r14: active(and(X1,X2)) -> and(active(X1),X2)
r15: U11(mark(X1),X2) -> mark(U11(X1,X2))
r16: U21(mark(X1),X2,X3) -> mark(U21(X1,X2,X3))
r17: s(mark(X)) -> mark(s(X))
r18: plus(mark(X1),X2) -> mark(plus(X1,X2))
r19: plus(X1,mark(X2)) -> mark(plus(X1,X2))
r20: and(mark(X1),X2) -> mark(and(X1,X2))
r21: proper(U11(X1,X2)) -> U11(proper(X1),proper(X2))
r22: proper(tt()) -> ok(tt())
r23: proper(U21(X1,X2,X3)) -> U21(proper(X1),proper(X2),proper(X3))
r24: proper(s(X)) -> s(proper(X))
r25: proper(plus(X1,X2)) -> plus(proper(X1),proper(X2))
r26: proper(and(X1,X2)) -> and(proper(X1),proper(X2))
r27: proper(isNat(X)) -> isNat(proper(X))
r28: proper(|0|()) -> ok(|0|())
r29: U11(ok(X1),ok(X2)) -> ok(U11(X1,X2))
r30: U21(ok(X1),ok(X2),ok(X3)) -> ok(U21(X1,X2,X3))
r31: s(ok(X)) -> ok(s(X))
r32: plus(ok(X1),ok(X2)) -> ok(plus(X1,X2))
r33: and(ok(X1),ok(X2)) -> ok(and(X1,X2))
r34: isNat(ok(X)) -> ok(isNat(X))
r35: top(mark(X)) -> top(proper(X))
r36: 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

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(),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: active(U11(X1,X2)) -> U11(active(X1),X2)
r10: active(U21(X1,X2,X3)) -> U21(active(X1),X2,X3)
r11: active(s(X)) -> s(active(X))
r12: active(plus(X1,X2)) -> plus(active(X1),X2)
r13: active(plus(X1,X2)) -> plus(X1,active(X2))
r14: active(and(X1,X2)) -> and(active(X1),X2)
r15: U11(mark(X1),X2) -> mark(U11(X1,X2))
r16: U21(mark(X1),X2,X3) -> mark(U21(X1,X2,X3))
r17: s(mark(X)) -> mark(s(X))
r18: plus(mark(X1),X2) -> mark(plus(X1,X2))
r19: plus(X1,mark(X2)) -> mark(plus(X1,X2))
r20: and(mark(X1),X2) -> mark(and(X1,X2))
r21: proper(U11(X1,X2)) -> U11(proper(X1),proper(X2))
r22: proper(tt()) -> ok(tt())
r23: proper(U21(X1,X2,X3)) -> U21(proper(X1),proper(X2),proper(X3))
r24: proper(s(X)) -> s(proper(X))
r25: proper(plus(X1,X2)) -> plus(proper(X1),proper(X2))
r26: proper(and(X1,X2)) -> and(proper(X1),proper(X2))
r27: proper(isNat(X)) -> isNat(proper(X))
r28: proper(|0|()) -> ok(|0|())
r29: U11(ok(X1),ok(X2)) -> ok(U11(X1,X2))
r30: U21(ok(X1),ok(X2),ok(X3)) -> ok(U21(X1,X2,X3))
r31: s(ok(X)) -> ok(s(X))
r32: plus(ok(X1),ok(X2)) -> ok(plus(X1,X2))
r33: and(ok(X1),ok(X2)) -> ok(and(X1,X2))
r34: isNat(ok(X)) -> ok(isNat(X))
r35: top(mark(X)) -> top(proper(X))
r36: 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

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(),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: active(U11(X1,X2)) -> U11(active(X1),X2)
r10: active(U21(X1,X2,X3)) -> U21(active(X1),X2,X3)
r11: active(s(X)) -> s(active(X))
r12: active(plus(X1,X2)) -> plus(active(X1),X2)
r13: active(plus(X1,X2)) -> plus(X1,active(X2))
r14: active(and(X1,X2)) -> and(active(X1),X2)
r15: U11(mark(X1),X2) -> mark(U11(X1,X2))
r16: U21(mark(X1),X2,X3) -> mark(U21(X1,X2,X3))
r17: s(mark(X)) -> mark(s(X))
r18: plus(mark(X1),X2) -> mark(plus(X1,X2))
r19: plus(X1,mark(X2)) -> mark(plus(X1,X2))
r20: and(mark(X1),X2) -> mark(and(X1,X2))
r21: proper(U11(X1,X2)) -> U11(proper(X1),proper(X2))
r22: proper(tt()) -> ok(tt())
r23: proper(U21(X1,X2,X3)) -> U21(proper(X1),proper(X2),proper(X3))
r24: proper(s(X)) -> s(proper(X))
r25: proper(plus(X1,X2)) -> plus(proper(X1),proper(X2))
r26: proper(and(X1,X2)) -> and(proper(X1),proper(X2))
r27: proper(isNat(X)) -> isNat(proper(X))
r28: proper(|0|()) -> ok(|0|())
r29: U11(ok(X1),ok(X2)) -> ok(U11(X1,X2))
r30: U21(ok(X1),ok(X2),ok(X3)) -> ok(U21(X1,X2,X3))
r31: s(ok(X)) -> ok(s(X))
r32: plus(ok(X1),ok(X2)) -> ok(plus(X1,X2))
r33: and(ok(X1),ok(X2)) -> ok(and(X1,X2))
r34: isNat(ok(X)) -> ok(isNat(X))
r35: top(mark(X)) -> top(proper(X))
r36: 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: isNat#(ok(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: active(U11(X1,X2)) -> U11(active(X1),X2)
r10: active(U21(X1,X2,X3)) -> U21(active(X1),X2,X3)
r11: active(s(X)) -> s(active(X))
r12: active(plus(X1,X2)) -> plus(active(X1),X2)
r13: active(plus(X1,X2)) -> plus(X1,active(X2))
r14: active(and(X1,X2)) -> and(active(X1),X2)
r15: U11(mark(X1),X2) -> mark(U11(X1,X2))
r16: U21(mark(X1),X2,X3) -> mark(U21(X1,X2,X3))
r17: s(mark(X)) -> mark(s(X))
r18: plus(mark(X1),X2) -> mark(plus(X1,X2))
r19: plus(X1,mark(X2)) -> mark(plus(X1,X2))
r20: and(mark(X1),X2) -> mark(and(X1,X2))
r21: proper(U11(X1,X2)) -> U11(proper(X1),proper(X2))
r22: proper(tt()) -> ok(tt())
r23: proper(U21(X1,X2,X3)) -> U21(proper(X1),proper(X2),proper(X3))
r24: proper(s(X)) -> s(proper(X))
r25: proper(plus(X1,X2)) -> plus(proper(X1),proper(X2))
r26: proper(and(X1,X2)) -> and(proper(X1),proper(X2))
r27: proper(isNat(X)) -> isNat(proper(X))
r28: proper(|0|()) -> ok(|0|())
r29: U11(ok(X1),ok(X2)) -> ok(U11(X1,X2))
r30: U21(ok(X1),ok(X2),ok(X3)) -> ok(U21(X1,X2,X3))
r31: s(ok(X)) -> ok(s(X))
r32: plus(ok(X1),ok(X2)) -> ok(plus(X1,X2))
r33: and(ok(X1),ok(X2)) -> ok(and(X1,X2))
r34: isNat(ok(X)) -> ok(isNat(X))
r35: top(mark(X)) -> top(proper(X))
r36: 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: U11#(mark(X1),X2) -> U11#(X1,X2)
p2: U11#(ok(X1),ok(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: active(U11(X1,X2)) -> U11(active(X1),X2)
r10: active(U21(X1,X2,X3)) -> U21(active(X1),X2,X3)
r11: active(s(X)) -> s(active(X))
r12: active(plus(X1,X2)) -> plus(active(X1),X2)
r13: active(plus(X1,X2)) -> plus(X1,active(X2))
r14: active(and(X1,X2)) -> and(active(X1),X2)
r15: U11(mark(X1),X2) -> mark(U11(X1,X2))
r16: U21(mark(X1),X2,X3) -> mark(U21(X1,X2,X3))
r17: s(mark(X)) -> mark(s(X))
r18: plus(mark(X1),X2) -> mark(plus(X1,X2))
r19: plus(X1,mark(X2)) -> mark(plus(X1,X2))
r20: and(mark(X1),X2) -> mark(and(X1,X2))
r21: proper(U11(X1,X2)) -> U11(proper(X1),proper(X2))
r22: proper(tt()) -> ok(tt())
r23: proper(U21(X1,X2,X3)) -> U21(proper(X1),proper(X2),proper(X3))
r24: proper(s(X)) -> s(proper(X))
r25: proper(plus(X1,X2)) -> plus(proper(X1),proper(X2))
r26: proper(and(X1,X2)) -> and(proper(X1),proper(X2))
r27: proper(isNat(X)) -> isNat(proper(X))
r28: proper(|0|()) -> ok(|0|())
r29: U11(ok(X1),ok(X2)) -> ok(U11(X1,X2))
r30: U21(ok(X1),ok(X2),ok(X3)) -> ok(U21(X1,X2,X3))
r31: s(ok(X)) -> ok(s(X))
r32: plus(ok(X1),ok(X2)) -> ok(plus(X1,X2))
r33: and(ok(X1),ok(X2)) -> ok(and(X1,X2))
r34: isNat(ok(X)) -> ok(isNat(X))
r35: top(mark(X)) -> top(proper(X))
r36: 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:
      U11#_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: U21#(mark(X1),X2,X3) -> U21#(X1,X2,X3)
p2: U21#(ok(X1),ok(X2),ok(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: active(U11(X1,X2)) -> U11(active(X1),X2)
r10: active(U21(X1,X2,X3)) -> U21(active(X1),X2,X3)
r11: active(s(X)) -> s(active(X))
r12: active(plus(X1,X2)) -> plus(active(X1),X2)
r13: active(plus(X1,X2)) -> plus(X1,active(X2))
r14: active(and(X1,X2)) -> and(active(X1),X2)
r15: U11(mark(X1),X2) -> mark(U11(X1,X2))
r16: U21(mark(X1),X2,X3) -> mark(U21(X1,X2,X3))
r17: s(mark(X)) -> mark(s(X))
r18: plus(mark(X1),X2) -> mark(plus(X1,X2))
r19: plus(X1,mark(X2)) -> mark(plus(X1,X2))
r20: and(mark(X1),X2) -> mark(and(X1,X2))
r21: proper(U11(X1,X2)) -> U11(proper(X1),proper(X2))
r22: proper(tt()) -> ok(tt())
r23: proper(U21(X1,X2,X3)) -> U21(proper(X1),proper(X2),proper(X3))
r24: proper(s(X)) -> s(proper(X))
r25: proper(plus(X1,X2)) -> plus(proper(X1),proper(X2))
r26: proper(and(X1,X2)) -> and(proper(X1),proper(X2))
r27: proper(isNat(X)) -> isNat(proper(X))
r28: proper(|0|()) -> ok(|0|())
r29: U11(ok(X1),ok(X2)) -> ok(U11(X1,X2))
r30: U21(ok(X1),ok(X2),ok(X3)) -> ok(U21(X1,X2,X3))
r31: s(ok(X)) -> ok(s(X))
r32: plus(ok(X1),ok(X2)) -> ok(plus(X1,X2))
r33: and(ok(X1),ok(X2)) -> ok(and(X1,X2))
r34: isNat(ok(X)) -> ok(isNat(X))
r35: top(mark(X)) -> top(proper(X))
r36: 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:
      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)
      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

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