YES

We show the termination of the TRS R:

  a__U11(tt(),N) -> mark(N)
  a__U21(tt(),M,N) -> s(a__plus(mark(N),mark(M)))
  a__and(tt(),X) -> mark(X)
  a__isNat(|0|()) -> tt()
  a__isNat(plus(V1,V2)) -> a__and(a__isNat(V1),isNat(V2))
  a__isNat(s(V1)) -> a__isNat(V1)
  a__plus(N,|0|()) -> a__U11(a__isNat(N),N)
  a__plus(N,s(M)) -> a__U21(a__and(a__isNat(M),isNat(N)),M,N)
  mark(U11(X1,X2)) -> a__U11(mark(X1),X2)
  mark(U21(X1,X2,X3)) -> a__U21(mark(X1),X2,X3)
  mark(plus(X1,X2)) -> a__plus(mark(X1),mark(X2))
  mark(and(X1,X2)) -> a__and(mark(X1),X2)
  mark(isNat(X)) -> a__isNat(X)
  mark(tt()) -> tt()
  mark(s(X)) -> s(mark(X))
  mark(|0|()) -> |0|()
  a__U11(X1,X2) -> U11(X1,X2)
  a__U21(X1,X2,X3) -> U21(X1,X2,X3)
  a__plus(X1,X2) -> plus(X1,X2)
  a__and(X1,X2) -> and(X1,X2)
  a__isNat(X) -> isNat(X)

-- SCC decomposition.

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

p1: a__U11#(tt(),N) -> mark#(N)
p2: a__U21#(tt(),M,N) -> a__plus#(mark(N),mark(M))
p3: a__U21#(tt(),M,N) -> mark#(N)
p4: a__U21#(tt(),M,N) -> mark#(M)
p5: a__and#(tt(),X) -> mark#(X)
p6: a__isNat#(plus(V1,V2)) -> a__and#(a__isNat(V1),isNat(V2))
p7: a__isNat#(plus(V1,V2)) -> a__isNat#(V1)
p8: a__isNat#(s(V1)) -> a__isNat#(V1)
p9: a__plus#(N,|0|()) -> a__U11#(a__isNat(N),N)
p10: a__plus#(N,|0|()) -> a__isNat#(N)
p11: a__plus#(N,s(M)) -> a__U21#(a__and(a__isNat(M),isNat(N)),M,N)
p12: a__plus#(N,s(M)) -> a__and#(a__isNat(M),isNat(N))
p13: a__plus#(N,s(M)) -> a__isNat#(M)
p14: mark#(U11(X1,X2)) -> a__U11#(mark(X1),X2)
p15: mark#(U11(X1,X2)) -> mark#(X1)
p16: mark#(U21(X1,X2,X3)) -> a__U21#(mark(X1),X2,X3)
p17: mark#(U21(X1,X2,X3)) -> mark#(X1)
p18: mark#(plus(X1,X2)) -> a__plus#(mark(X1),mark(X2))
p19: mark#(plus(X1,X2)) -> mark#(X1)
p20: mark#(plus(X1,X2)) -> mark#(X2)
p21: mark#(and(X1,X2)) -> a__and#(mark(X1),X2)
p22: mark#(and(X1,X2)) -> mark#(X1)
p23: mark#(isNat(X)) -> a__isNat#(X)
p24: mark#(s(X)) -> mark#(X)

and R consists of:

r1: a__U11(tt(),N) -> mark(N)
r2: a__U21(tt(),M,N) -> s(a__plus(mark(N),mark(M)))
r3: a__and(tt(),X) -> mark(X)
r4: a__isNat(|0|()) -> tt()
r5: a__isNat(plus(V1,V2)) -> a__and(a__isNat(V1),isNat(V2))
r6: a__isNat(s(V1)) -> a__isNat(V1)
r7: a__plus(N,|0|()) -> a__U11(a__isNat(N),N)
r8: a__plus(N,s(M)) -> a__U21(a__and(a__isNat(M),isNat(N)),M,N)
r9: mark(U11(X1,X2)) -> a__U11(mark(X1),X2)
r10: mark(U21(X1,X2,X3)) -> a__U21(mark(X1),X2,X3)
r11: mark(plus(X1,X2)) -> a__plus(mark(X1),mark(X2))
r12: mark(and(X1,X2)) -> a__and(mark(X1),X2)
r13: mark(isNat(X)) -> a__isNat(X)
r14: mark(tt()) -> tt()
r15: mark(s(X)) -> s(mark(X))
r16: mark(|0|()) -> |0|()
r17: a__U11(X1,X2) -> U11(X1,X2)
r18: a__U21(X1,X2,X3) -> U21(X1,X2,X3)
r19: a__plus(X1,X2) -> plus(X1,X2)
r20: a__and(X1,X2) -> and(X1,X2)
r21: a__isNat(X) -> isNat(X)

The estimated dependency graph contains the following SCCs:

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


-- Reduction pair.

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

p1: a__U11#(tt(),N) -> mark#(N)
p2: mark#(s(X)) -> mark#(X)
p3: mark#(isNat(X)) -> a__isNat#(X)
p4: a__isNat#(s(V1)) -> a__isNat#(V1)
p5: a__isNat#(plus(V1,V2)) -> a__isNat#(V1)
p6: a__isNat#(plus(V1,V2)) -> a__and#(a__isNat(V1),isNat(V2))
p7: a__and#(tt(),X) -> mark#(X)
p8: mark#(and(X1,X2)) -> mark#(X1)
p9: mark#(and(X1,X2)) -> a__and#(mark(X1),X2)
p10: mark#(plus(X1,X2)) -> mark#(X2)
p11: mark#(plus(X1,X2)) -> mark#(X1)
p12: mark#(plus(X1,X2)) -> a__plus#(mark(X1),mark(X2))
p13: a__plus#(N,s(M)) -> a__isNat#(M)
p14: a__plus#(N,s(M)) -> a__and#(a__isNat(M),isNat(N))
p15: a__plus#(N,s(M)) -> a__U21#(a__and(a__isNat(M),isNat(N)),M,N)
p16: a__U21#(tt(),M,N) -> mark#(M)
p17: mark#(U21(X1,X2,X3)) -> mark#(X1)
p18: mark#(U21(X1,X2,X3)) -> a__U21#(mark(X1),X2,X3)
p19: a__U21#(tt(),M,N) -> mark#(N)
p20: mark#(U11(X1,X2)) -> mark#(X1)
p21: mark#(U11(X1,X2)) -> a__U11#(mark(X1),X2)
p22: a__U21#(tt(),M,N) -> a__plus#(mark(N),mark(M))
p23: a__plus#(N,|0|()) -> a__isNat#(N)
p24: a__plus#(N,|0|()) -> a__U11#(a__isNat(N),N)

and R consists of:

r1: a__U11(tt(),N) -> mark(N)
r2: a__U21(tt(),M,N) -> s(a__plus(mark(N),mark(M)))
r3: a__and(tt(),X) -> mark(X)
r4: a__isNat(|0|()) -> tt()
r5: a__isNat(plus(V1,V2)) -> a__and(a__isNat(V1),isNat(V2))
r6: a__isNat(s(V1)) -> a__isNat(V1)
r7: a__plus(N,|0|()) -> a__U11(a__isNat(N),N)
r8: a__plus(N,s(M)) -> a__U21(a__and(a__isNat(M),isNat(N)),M,N)
r9: mark(U11(X1,X2)) -> a__U11(mark(X1),X2)
r10: mark(U21(X1,X2,X3)) -> a__U21(mark(X1),X2,X3)
r11: mark(plus(X1,X2)) -> a__plus(mark(X1),mark(X2))
r12: mark(and(X1,X2)) -> a__and(mark(X1),X2)
r13: mark(isNat(X)) -> a__isNat(X)
r14: mark(tt()) -> tt()
r15: mark(s(X)) -> s(mark(X))
r16: mark(|0|()) -> |0|()
r17: a__U11(X1,X2) -> U11(X1,X2)
r18: a__U21(X1,X2,X3) -> U21(X1,X2,X3)
r19: a__plus(X1,X2) -> plus(X1,X2)
r20: a__and(X1,X2) -> and(X1,X2)
r21: a__isNat(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

Take the reduction pair:

  matrix interpretations:
  
    carrier: N^2
    order: lexicographic order
    interpretations:
      a__U11#_A(x1,x2) = ((1,0),(1,0)) x2 + (1,1)
      tt_A() = (0,1)
      mark#_A(x1) = x1 + (0,1)
      s_A(x1) = ((1,0),(1,0)) x1 + (2,1)
      isNat_A(x1) = ((0,0),(1,0)) x1 + (0,1)
      a__isNat#_A(x1) = (0,1)
      plus_A(x1,x2) = ((1,0),(1,0)) x1 + x2 + (3,5)
      a__and#_A(x1,x2) = x2 + (0,1)
      a__isNat_A(x1) = ((0,0),(1,0)) x1 + (0,6)
      and_A(x1,x2) = x1 + x2 + (0,2)
      mark_A(x1) = x1 + (0,6)
      a__plus#_A(x1,x2) = x1 + x2 + (2,0)
      a__U21#_A(x1,x2,x3) = x1 + x2 + ((1,0),(1,1)) x3 + (3,2)
      a__and_A(x1,x2) = x1 + x2 + (0,7)
      U21_A(x1,x2,x3) = ((1,0),(1,0)) x1 + ((1,0),(1,0)) x2 + ((1,0),(1,0)) x3 + (5,1)
      U11_A(x1,x2) = x1 + x2 + (3,1)
      |0|_A() = (0,1)
      a__U11_A(x1,x2) = x1 + x2 + (3,6)
      a__U21_A(x1,x2,x3) = ((1,0),(1,0)) x1 + ((1,0),(1,0)) x2 + ((1,0),(1,0)) x3 + (5,5)
      a__plus_A(x1,x2) = ((1,0),(1,0)) x1 + x2 + (3,5)

The next rules are strictly ordered:

  p1, p2, p10, p11, p12, p13, p14, p15, p16, p17, p18, p19, p20, p21, p22, p23, p24

We remove them from the problem.

-- SCC decomposition.

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

p1: mark#(isNat(X)) -> a__isNat#(X)
p2: a__isNat#(s(V1)) -> a__isNat#(V1)
p3: a__isNat#(plus(V1,V2)) -> a__isNat#(V1)
p4: a__isNat#(plus(V1,V2)) -> a__and#(a__isNat(V1),isNat(V2))
p5: a__and#(tt(),X) -> mark#(X)
p6: mark#(and(X1,X2)) -> mark#(X1)
p7: mark#(and(X1,X2)) -> a__and#(mark(X1),X2)

and R consists of:

r1: a__U11(tt(),N) -> mark(N)
r2: a__U21(tt(),M,N) -> s(a__plus(mark(N),mark(M)))
r3: a__and(tt(),X) -> mark(X)
r4: a__isNat(|0|()) -> tt()
r5: a__isNat(plus(V1,V2)) -> a__and(a__isNat(V1),isNat(V2))
r6: a__isNat(s(V1)) -> a__isNat(V1)
r7: a__plus(N,|0|()) -> a__U11(a__isNat(N),N)
r8: a__plus(N,s(M)) -> a__U21(a__and(a__isNat(M),isNat(N)),M,N)
r9: mark(U11(X1,X2)) -> a__U11(mark(X1),X2)
r10: mark(U21(X1,X2,X3)) -> a__U21(mark(X1),X2,X3)
r11: mark(plus(X1,X2)) -> a__plus(mark(X1),mark(X2))
r12: mark(and(X1,X2)) -> a__and(mark(X1),X2)
r13: mark(isNat(X)) -> a__isNat(X)
r14: mark(tt()) -> tt()
r15: mark(s(X)) -> s(mark(X))
r16: mark(|0|()) -> |0|()
r17: a__U11(X1,X2) -> U11(X1,X2)
r18: a__U21(X1,X2,X3) -> U21(X1,X2,X3)
r19: a__plus(X1,X2) -> plus(X1,X2)
r20: a__and(X1,X2) -> and(X1,X2)
r21: a__isNat(X) -> isNat(X)

The estimated dependency graph contains the following SCCs:

  {p1, p2, p3, p4, p5, p6, p7}


-- Reduction pair.

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

p1: mark#(isNat(X)) -> a__isNat#(X)
p2: a__isNat#(plus(V1,V2)) -> a__and#(a__isNat(V1),isNat(V2))
p3: a__and#(tt(),X) -> mark#(X)
p4: mark#(and(X1,X2)) -> a__and#(mark(X1),X2)
p5: mark#(and(X1,X2)) -> mark#(X1)
p6: a__isNat#(plus(V1,V2)) -> a__isNat#(V1)
p7: a__isNat#(s(V1)) -> a__isNat#(V1)

and R consists of:

r1: a__U11(tt(),N) -> mark(N)
r2: a__U21(tt(),M,N) -> s(a__plus(mark(N),mark(M)))
r3: a__and(tt(),X) -> mark(X)
r4: a__isNat(|0|()) -> tt()
r5: a__isNat(plus(V1,V2)) -> a__and(a__isNat(V1),isNat(V2))
r6: a__isNat(s(V1)) -> a__isNat(V1)
r7: a__plus(N,|0|()) -> a__U11(a__isNat(N),N)
r8: a__plus(N,s(M)) -> a__U21(a__and(a__isNat(M),isNat(N)),M,N)
r9: mark(U11(X1,X2)) -> a__U11(mark(X1),X2)
r10: mark(U21(X1,X2,X3)) -> a__U21(mark(X1),X2,X3)
r11: mark(plus(X1,X2)) -> a__plus(mark(X1),mark(X2))
r12: mark(and(X1,X2)) -> a__and(mark(X1),X2)
r13: mark(isNat(X)) -> a__isNat(X)
r14: mark(tt()) -> tt()
r15: mark(s(X)) -> s(mark(X))
r16: mark(|0|()) -> |0|()
r17: a__U11(X1,X2) -> U11(X1,X2)
r18: a__U21(X1,X2,X3) -> U21(X1,X2,X3)
r19: a__plus(X1,X2) -> plus(X1,X2)
r20: a__and(X1,X2) -> and(X1,X2)
r21: a__isNat(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

Take the reduction pair:

  matrix interpretations:
  
    carrier: N^2
    order: lexicographic order
    interpretations:
      mark#_A(x1) = x1 + (1,6)
      isNat_A(x1) = x1 + (0,1)
      a__isNat#_A(x1) = ((1,0),(1,1)) x1
      plus_A(x1,x2) = ((1,0),(1,1)) x1 + x2 + (3,1)
      a__and#_A(x1,x2) = x2 + (2,5)
      a__isNat_A(x1) = x1 + (0,2)
      tt_A() = (0,1)
      and_A(x1,x2) = x1 + x2 + (2,1)
      mark_A(x1) = ((1,0),(1,1)) x1 + (0,5)
      s_A(x1) = x1 + (1,1)
      a__U11_A(x1,x2) = ((1,0),(1,0)) x2 + (1,4)
      a__U21_A(x1,x2,x3) = x2 + ((1,0),(1,1)) x3 + (4,2)
      a__plus_A(x1,x2) = ((1,0),(1,1)) x1 + x2 + (3,3)
      a__and_A(x1,x2) = x1 + x2 + (2,4)
      |0|_A() = (0,1)
      U11_A(x1,x2) = ((1,0),(1,0)) x2 + (1,1)
      U21_A(x1,x2,x3) = x2 + ((1,0),(1,1)) x3 + (4,2)

The next rules are strictly ordered:

  p1, p2, p3, p4, p5, p6, p7

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