YES

We show the termination of the TRS R:

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

-- SCC decomposition.

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

p1: active#(U11(tt(),V2)) -> mark#(U12(isNat(V2)))
p2: active#(U11(tt(),V2)) -> U12#(isNat(V2))
p3: active#(U11(tt(),V2)) -> isNat#(V2)
p4: active#(U12(tt())) -> mark#(tt())
p5: active#(U21(tt())) -> mark#(tt())
p6: active#(U31(tt(),N)) -> mark#(N)
p7: active#(U41(tt(),M,N)) -> mark#(U42(isNat(N),M,N))
p8: active#(U41(tt(),M,N)) -> U42#(isNat(N),M,N)
p9: active#(U41(tt(),M,N)) -> isNat#(N)
p10: active#(U42(tt(),M,N)) -> mark#(s(plus(N,M)))
p11: active#(U42(tt(),M,N)) -> s#(plus(N,M))
p12: active#(U42(tt(),M,N)) -> plus#(N,M)
p13: active#(isNat(|0|())) -> mark#(tt())
p14: active#(isNat(plus(V1,V2))) -> mark#(U11(isNat(V1),V2))
p15: active#(isNat(plus(V1,V2))) -> U11#(isNat(V1),V2)
p16: active#(isNat(plus(V1,V2))) -> isNat#(V1)
p17: active#(isNat(s(V1))) -> mark#(U21(isNat(V1)))
p18: active#(isNat(s(V1))) -> U21#(isNat(V1))
p19: active#(isNat(s(V1))) -> isNat#(V1)
p20: active#(plus(N,|0|())) -> mark#(U31(isNat(N),N))
p21: active#(plus(N,|0|())) -> U31#(isNat(N),N)
p22: active#(plus(N,|0|())) -> isNat#(N)
p23: active#(plus(N,s(M))) -> mark#(U41(isNat(M),M,N))
p24: active#(plus(N,s(M))) -> U41#(isNat(M),M,N)
p25: active#(plus(N,s(M))) -> isNat#(M)
p26: mark#(U11(X1,X2)) -> active#(U11(mark(X1),X2))
p27: mark#(U11(X1,X2)) -> U11#(mark(X1),X2)
p28: mark#(U11(X1,X2)) -> mark#(X1)
p29: mark#(tt()) -> active#(tt())
p30: mark#(U12(X)) -> active#(U12(mark(X)))
p31: mark#(U12(X)) -> U12#(mark(X))
p32: mark#(U12(X)) -> mark#(X)
p33: mark#(isNat(X)) -> active#(isNat(X))
p34: mark#(U21(X)) -> active#(U21(mark(X)))
p35: mark#(U21(X)) -> U21#(mark(X))
p36: mark#(U21(X)) -> mark#(X)
p37: mark#(U31(X1,X2)) -> active#(U31(mark(X1),X2))
p38: mark#(U31(X1,X2)) -> U31#(mark(X1),X2)
p39: mark#(U31(X1,X2)) -> mark#(X1)
p40: mark#(U41(X1,X2,X3)) -> active#(U41(mark(X1),X2,X3))
p41: mark#(U41(X1,X2,X3)) -> U41#(mark(X1),X2,X3)
p42: mark#(U41(X1,X2,X3)) -> mark#(X1)
p43: mark#(U42(X1,X2,X3)) -> active#(U42(mark(X1),X2,X3))
p44: mark#(U42(X1,X2,X3)) -> U42#(mark(X1),X2,X3)
p45: mark#(U42(X1,X2,X3)) -> mark#(X1)
p46: mark#(s(X)) -> active#(s(mark(X)))
p47: mark#(s(X)) -> s#(mark(X))
p48: mark#(s(X)) -> mark#(X)
p49: mark#(plus(X1,X2)) -> active#(plus(mark(X1),mark(X2)))
p50: mark#(plus(X1,X2)) -> plus#(mark(X1),mark(X2))
p51: mark#(plus(X1,X2)) -> mark#(X1)
p52: mark#(plus(X1,X2)) -> mark#(X2)
p53: mark#(|0|()) -> active#(|0|())
p54: U11#(mark(X1),X2) -> U11#(X1,X2)
p55: U11#(X1,mark(X2)) -> U11#(X1,X2)
p56: U11#(active(X1),X2) -> U11#(X1,X2)
p57: U11#(X1,active(X2)) -> U11#(X1,X2)
p58: U12#(mark(X)) -> U12#(X)
p59: U12#(active(X)) -> U12#(X)
p60: isNat#(mark(X)) -> isNat#(X)
p61: isNat#(active(X)) -> isNat#(X)
p62: U21#(mark(X)) -> U21#(X)
p63: U21#(active(X)) -> U21#(X)
p64: U31#(mark(X1),X2) -> U31#(X1,X2)
p65: U31#(X1,mark(X2)) -> U31#(X1,X2)
p66: U31#(active(X1),X2) -> U31#(X1,X2)
p67: U31#(X1,active(X2)) -> U31#(X1,X2)
p68: U41#(mark(X1),X2,X3) -> U41#(X1,X2,X3)
p69: U41#(X1,mark(X2),X3) -> U41#(X1,X2,X3)
p70: U41#(X1,X2,mark(X3)) -> U41#(X1,X2,X3)
p71: U41#(active(X1),X2,X3) -> U41#(X1,X2,X3)
p72: U41#(X1,active(X2),X3) -> U41#(X1,X2,X3)
p73: U41#(X1,X2,active(X3)) -> U41#(X1,X2,X3)
p74: U42#(mark(X1),X2,X3) -> U42#(X1,X2,X3)
p75: U42#(X1,mark(X2),X3) -> U42#(X1,X2,X3)
p76: U42#(X1,X2,mark(X3)) -> U42#(X1,X2,X3)
p77: U42#(active(X1),X2,X3) -> U42#(X1,X2,X3)
p78: U42#(X1,active(X2),X3) -> U42#(X1,X2,X3)
p79: U42#(X1,X2,active(X3)) -> U42#(X1,X2,X3)
p80: s#(mark(X)) -> s#(X)
p81: s#(active(X)) -> s#(X)
p82: plus#(mark(X1),X2) -> plus#(X1,X2)
p83: plus#(X1,mark(X2)) -> plus#(X1,X2)
p84: plus#(active(X1),X2) -> plus#(X1,X2)
p85: plus#(X1,active(X2)) -> plus#(X1,X2)

and R consists of:

r1: active(U11(tt(),V2)) -> mark(U12(isNat(V2)))
r2: active(U12(tt())) -> mark(tt())
r3: active(U21(tt())) -> mark(tt())
r4: active(U31(tt(),N)) -> mark(N)
r5: active(U41(tt(),M,N)) -> mark(U42(isNat(N),M,N))
r6: active(U42(tt(),M,N)) -> mark(s(plus(N,M)))
r7: active(isNat(|0|())) -> mark(tt())
r8: active(isNat(plus(V1,V2))) -> mark(U11(isNat(V1),V2))
r9: active(isNat(s(V1))) -> mark(U21(isNat(V1)))
r10: active(plus(N,|0|())) -> mark(U31(isNat(N),N))
r11: active(plus(N,s(M))) -> mark(U41(isNat(M),M,N))
r12: mark(U11(X1,X2)) -> active(U11(mark(X1),X2))
r13: mark(tt()) -> active(tt())
r14: mark(U12(X)) -> active(U12(mark(X)))
r15: mark(isNat(X)) -> active(isNat(X))
r16: mark(U21(X)) -> active(U21(mark(X)))
r17: mark(U31(X1,X2)) -> active(U31(mark(X1),X2))
r18: mark(U41(X1,X2,X3)) -> active(U41(mark(X1),X2,X3))
r19: mark(U42(X1,X2,X3)) -> active(U42(mark(X1),X2,X3))
r20: mark(s(X)) -> active(s(mark(X)))
r21: mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2)))
r22: mark(|0|()) -> active(|0|())
r23: U11(mark(X1),X2) -> U11(X1,X2)
r24: U11(X1,mark(X2)) -> U11(X1,X2)
r25: U11(active(X1),X2) -> U11(X1,X2)
r26: U11(X1,active(X2)) -> U11(X1,X2)
r27: U12(mark(X)) -> U12(X)
r28: U12(active(X)) -> U12(X)
r29: isNat(mark(X)) -> isNat(X)
r30: isNat(active(X)) -> isNat(X)
r31: U21(mark(X)) -> U21(X)
r32: U21(active(X)) -> U21(X)
r33: U31(mark(X1),X2) -> U31(X1,X2)
r34: U31(X1,mark(X2)) -> U31(X1,X2)
r35: U31(active(X1),X2) -> U31(X1,X2)
r36: U31(X1,active(X2)) -> U31(X1,X2)
r37: U41(mark(X1),X2,X3) -> U41(X1,X2,X3)
r38: U41(X1,mark(X2),X3) -> U41(X1,X2,X3)
r39: U41(X1,X2,mark(X3)) -> U41(X1,X2,X3)
r40: U41(active(X1),X2,X3) -> U41(X1,X2,X3)
r41: U41(X1,active(X2),X3) -> U41(X1,X2,X3)
r42: U41(X1,X2,active(X3)) -> U41(X1,X2,X3)
r43: U42(mark(X1),X2,X3) -> U42(X1,X2,X3)
r44: U42(X1,mark(X2),X3) -> U42(X1,X2,X3)
r45: U42(X1,X2,mark(X3)) -> U42(X1,X2,X3)
r46: U42(active(X1),X2,X3) -> U42(X1,X2,X3)
r47: U42(X1,active(X2),X3) -> U42(X1,X2,X3)
r48: U42(X1,X2,active(X3)) -> U42(X1,X2,X3)
r49: s(mark(X)) -> s(X)
r50: s(active(X)) -> s(X)
r51: plus(mark(X1),X2) -> plus(X1,X2)
r52: plus(X1,mark(X2)) -> plus(X1,X2)
r53: plus(active(X1),X2) -> plus(X1,X2)
r54: plus(X1,active(X2)) -> plus(X1,X2)

The estimated dependency graph contains the following SCCs:

  {p1, p6, p7, p10, p14, p17, p20, p23, p26, p28, p30, p32, p33, p34, p36, p37, p39, p40, p42, p43, p45, p46, p48, p49, p51, p52}
  {p58, p59}
  {p60, p61}
  {p74, p75, p76, p77, p78, p79}
  {p80, p81}
  {p82, p83, p84, p85}
  {p54, p55, p56, p57}
  {p62, p63}
  {p64, p65, p66, p67}
  {p68, p69, p70, p71, p72, p73}


-- Reduction pair.

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

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

and R consists of:

r1: active(U11(tt(),V2)) -> mark(U12(isNat(V2)))
r2: active(U12(tt())) -> mark(tt())
r3: active(U21(tt())) -> mark(tt())
r4: active(U31(tt(),N)) -> mark(N)
r5: active(U41(tt(),M,N)) -> mark(U42(isNat(N),M,N))
r6: active(U42(tt(),M,N)) -> mark(s(plus(N,M)))
r7: active(isNat(|0|())) -> mark(tt())
r8: active(isNat(plus(V1,V2))) -> mark(U11(isNat(V1),V2))
r9: active(isNat(s(V1))) -> mark(U21(isNat(V1)))
r10: active(plus(N,|0|())) -> mark(U31(isNat(N),N))
r11: active(plus(N,s(M))) -> mark(U41(isNat(M),M,N))
r12: mark(U11(X1,X2)) -> active(U11(mark(X1),X2))
r13: mark(tt()) -> active(tt())
r14: mark(U12(X)) -> active(U12(mark(X)))
r15: mark(isNat(X)) -> active(isNat(X))
r16: mark(U21(X)) -> active(U21(mark(X)))
r17: mark(U31(X1,X2)) -> active(U31(mark(X1),X2))
r18: mark(U41(X1,X2,X3)) -> active(U41(mark(X1),X2,X3))
r19: mark(U42(X1,X2,X3)) -> active(U42(mark(X1),X2,X3))
r20: mark(s(X)) -> active(s(mark(X)))
r21: mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2)))
r22: mark(|0|()) -> active(|0|())
r23: U11(mark(X1),X2) -> U11(X1,X2)
r24: U11(X1,mark(X2)) -> U11(X1,X2)
r25: U11(active(X1),X2) -> U11(X1,X2)
r26: U11(X1,active(X2)) -> U11(X1,X2)
r27: U12(mark(X)) -> U12(X)
r28: U12(active(X)) -> U12(X)
r29: isNat(mark(X)) -> isNat(X)
r30: isNat(active(X)) -> isNat(X)
r31: U21(mark(X)) -> U21(X)
r32: U21(active(X)) -> U21(X)
r33: U31(mark(X1),X2) -> U31(X1,X2)
r34: U31(X1,mark(X2)) -> U31(X1,X2)
r35: U31(active(X1),X2) -> U31(X1,X2)
r36: U31(X1,active(X2)) -> U31(X1,X2)
r37: U41(mark(X1),X2,X3) -> U41(X1,X2,X3)
r38: U41(X1,mark(X2),X3) -> U41(X1,X2,X3)
r39: U41(X1,X2,mark(X3)) -> U41(X1,X2,X3)
r40: U41(active(X1),X2,X3) -> U41(X1,X2,X3)
r41: U41(X1,active(X2),X3) -> U41(X1,X2,X3)
r42: U41(X1,X2,active(X3)) -> U41(X1,X2,X3)
r43: U42(mark(X1),X2,X3) -> U42(X1,X2,X3)
r44: U42(X1,mark(X2),X3) -> U42(X1,X2,X3)
r45: U42(X1,X2,mark(X3)) -> U42(X1,X2,X3)
r46: U42(active(X1),X2,X3) -> U42(X1,X2,X3)
r47: U42(X1,active(X2),X3) -> U42(X1,X2,X3)
r48: U42(X1,X2,active(X3)) -> U42(X1,X2,X3)
r49: s(mark(X)) -> s(X)
r50: s(active(X)) -> s(X)
r51: plus(mark(X1),X2) -> plus(X1,X2)
r52: plus(X1,mark(X2)) -> plus(X1,X2)
r53: plus(active(X1),X2) -> plus(X1,X2)
r54: plus(X1,active(X2)) -> plus(X1,X2)

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

Take the reduction pair:

  lexicographic combination of reduction pairs:
  
    1. matrix interpretations:
    
      carrier: N^4
      order: lexicographic order
      interpretations:
        active#_A(x1) = ((1,0,0,0),(1,0,0,0),(0,0,0,0),(0,1,0,0)) x1
        U11_A(x1,x2) = ((1,0,0,0),(1,1,0,0),(1,0,1,0),(1,0,0,1)) x1 + ((0,0,0,0),(1,0,0,0),(0,1,0,0),(1,1,1,0)) x2 + (0,8,1,32)
        tt_A() = (1,2,1,1)
        mark#_A(x1) = ((1,0,0,0),(1,0,0,0),(0,0,0,0),(0,1,0,0)) x1 + (0,0,0,5)
        U12_A(x1) = x1 + (0,5,3,0)
        isNat_A(x1) = ((0,0,0,0),(1,0,0,0),(0,0,0,0),(1,1,0,0)) x1 + (1,0,1,0)
        plus_A(x1,x2) = ((1,0,0,0),(1,0,0,0),(0,0,0,0),(0,0,0,0)) x1 + x2 + (15,15,0,1)
        mark_A(x1) = ((1,0,0,0),(0,1,0,0),(0,1,1,0),(1,0,0,0)) x1 + (0,4,0,47)
        s_A(x1) = ((1,0,0,0),(0,0,0,0),(1,0,0,0),(0,0,0,0)) x1 + (11,48,0,0)
        U41_A(x1,x2,x3) = ((1,0,0,0),(0,0,0,0),(1,1,0,0),(0,0,1,0)) x1 + x2 + ((1,0,0,0),(1,0,0,0),(1,0,0,0),(1,0,0,0)) x3 + (25,58,1,1)
        |0|_A() = (7,2,1,0)
        U31_A(x1,x2) = ((1,0,0,0),(0,0,0,0),(0,0,0,0),(0,1,0,0)) x1 + ((1,0,0,0),(0,0,0,0),(1,1,0,0),(1,1,0,0)) x2 + (1,11,0,0)
        U42_A(x1,x2,x3) = ((1,0,0,0),(1,1,0,0),(1,1,1,0),(1,1,0,0)) x1 + ((1,0,0,0),(0,0,0,0),(1,0,0,0),(1,0,0,0)) x2 + ((1,0,0,0),(0,0,0,0),(0,0,0,0),(1,0,0,0)) x3 + (25,51,0,0)
        U21_A(x1) = x1 + (0,5,3,36)
        active_A(x1) = ((1,0,0,0),(0,1,0,0),(0,0,1,0),(1,1,1,1)) x1 + (0,0,1,0)
    
    2. lexicographic path order with precedence:
    
      precedence:
      
        tt > U21 > U41 > active# > isNat > plus > U42 > U11 > mark# > mark > |0| > U31 > active > U12 > s
      
      argument filter:
    
        pi(active#) = []
        pi(U11) = 1
        pi(tt) = []
        pi(mark#) = []
        pi(U12) = []
        pi(isNat) = []
        pi(plus) = []
        pi(mark) = []
        pi(s) = []
        pi(U41) = []
        pi(|0|) = []
        pi(U31) = []
        pi(U42) = []
        pi(U21) = []
        pi(active) = 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, p22, p23, p24, p25, p26

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

and R consists of:

r1: active(U11(tt(),V2)) -> mark(U12(isNat(V2)))
r2: active(U12(tt())) -> mark(tt())
r3: active(U21(tt())) -> mark(tt())
r4: active(U31(tt(),N)) -> mark(N)
r5: active(U41(tt(),M,N)) -> mark(U42(isNat(N),M,N))
r6: active(U42(tt(),M,N)) -> mark(s(plus(N,M)))
r7: active(isNat(|0|())) -> mark(tt())
r8: active(isNat(plus(V1,V2))) -> mark(U11(isNat(V1),V2))
r9: active(isNat(s(V1))) -> mark(U21(isNat(V1)))
r10: active(plus(N,|0|())) -> mark(U31(isNat(N),N))
r11: active(plus(N,s(M))) -> mark(U41(isNat(M),M,N))
r12: mark(U11(X1,X2)) -> active(U11(mark(X1),X2))
r13: mark(tt()) -> active(tt())
r14: mark(U12(X)) -> active(U12(mark(X)))
r15: mark(isNat(X)) -> active(isNat(X))
r16: mark(U21(X)) -> active(U21(mark(X)))
r17: mark(U31(X1,X2)) -> active(U31(mark(X1),X2))
r18: mark(U41(X1,X2,X3)) -> active(U41(mark(X1),X2,X3))
r19: mark(U42(X1,X2,X3)) -> active(U42(mark(X1),X2,X3))
r20: mark(s(X)) -> active(s(mark(X)))
r21: mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2)))
r22: mark(|0|()) -> active(|0|())
r23: U11(mark(X1),X2) -> U11(X1,X2)
r24: U11(X1,mark(X2)) -> U11(X1,X2)
r25: U11(active(X1),X2) -> U11(X1,X2)
r26: U11(X1,active(X2)) -> U11(X1,X2)
r27: U12(mark(X)) -> U12(X)
r28: U12(active(X)) -> U12(X)
r29: isNat(mark(X)) -> isNat(X)
r30: isNat(active(X)) -> isNat(X)
r31: U21(mark(X)) -> U21(X)
r32: U21(active(X)) -> U21(X)
r33: U31(mark(X1),X2) -> U31(X1,X2)
r34: U31(X1,mark(X2)) -> U31(X1,X2)
r35: U31(active(X1),X2) -> U31(X1,X2)
r36: U31(X1,active(X2)) -> U31(X1,X2)
r37: U41(mark(X1),X2,X3) -> U41(X1,X2,X3)
r38: U41(X1,mark(X2),X3) -> U41(X1,X2,X3)
r39: U41(X1,X2,mark(X3)) -> U41(X1,X2,X3)
r40: U41(active(X1),X2,X3) -> U41(X1,X2,X3)
r41: U41(X1,active(X2),X3) -> U41(X1,X2,X3)
r42: U41(X1,X2,active(X3)) -> U41(X1,X2,X3)
r43: U42(mark(X1),X2,X3) -> U42(X1,X2,X3)
r44: U42(X1,mark(X2),X3) -> U42(X1,X2,X3)
r45: U42(X1,X2,mark(X3)) -> U42(X1,X2,X3)
r46: U42(active(X1),X2,X3) -> U42(X1,X2,X3)
r47: U42(X1,active(X2),X3) -> U42(X1,X2,X3)
r48: U42(X1,X2,active(X3)) -> U42(X1,X2,X3)
r49: s(mark(X)) -> s(X)
r50: s(active(X)) -> s(X)
r51: plus(mark(X1),X2) -> plus(X1,X2)
r52: plus(X1,mark(X2)) -> plus(X1,X2)
r53: plus(active(X1),X2) -> plus(X1,X2)
r54: plus(X1,active(X2)) -> plus(X1,X2)

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  lexicographic combination of reduction pairs:
  
    1. matrix interpretations:
    
      carrier: N^4
      order: lexicographic order
      interpretations:
        U12#_A(x1) = ((1,0,0,0),(0,1,0,0),(0,0,0,0),(0,0,1,0)) x1
        mark_A(x1) = ((1,0,0,0),(1,1,0,0),(1,1,1,0),(1,1,1,1)) x1 + (1,1,0,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)
    
    2. lexicographic path order with precedence:
    
      precedence:
      
        mark > U12# > active
      
      argument filter:
    
        pi(U12#) = []
        pi(mark) = []
        pi(active) = []
    

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

and R consists of:

r1: active(U11(tt(),V2)) -> mark(U12(isNat(V2)))
r2: active(U12(tt())) -> mark(tt())
r3: active(U21(tt())) -> mark(tt())
r4: active(U31(tt(),N)) -> mark(N)
r5: active(U41(tt(),M,N)) -> mark(U42(isNat(N),M,N))
r6: active(U42(tt(),M,N)) -> mark(s(plus(N,M)))
r7: active(isNat(|0|())) -> mark(tt())
r8: active(isNat(plus(V1,V2))) -> mark(U11(isNat(V1),V2))
r9: active(isNat(s(V1))) -> mark(U21(isNat(V1)))
r10: active(plus(N,|0|())) -> mark(U31(isNat(N),N))
r11: active(plus(N,s(M))) -> mark(U41(isNat(M),M,N))
r12: mark(U11(X1,X2)) -> active(U11(mark(X1),X2))
r13: mark(tt()) -> active(tt())
r14: mark(U12(X)) -> active(U12(mark(X)))
r15: mark(isNat(X)) -> active(isNat(X))
r16: mark(U21(X)) -> active(U21(mark(X)))
r17: mark(U31(X1,X2)) -> active(U31(mark(X1),X2))
r18: mark(U41(X1,X2,X3)) -> active(U41(mark(X1),X2,X3))
r19: mark(U42(X1,X2,X3)) -> active(U42(mark(X1),X2,X3))
r20: mark(s(X)) -> active(s(mark(X)))
r21: mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2)))
r22: mark(|0|()) -> active(|0|())
r23: U11(mark(X1),X2) -> U11(X1,X2)
r24: U11(X1,mark(X2)) -> U11(X1,X2)
r25: U11(active(X1),X2) -> U11(X1,X2)
r26: U11(X1,active(X2)) -> U11(X1,X2)
r27: U12(mark(X)) -> U12(X)
r28: U12(active(X)) -> U12(X)
r29: isNat(mark(X)) -> isNat(X)
r30: isNat(active(X)) -> isNat(X)
r31: U21(mark(X)) -> U21(X)
r32: U21(active(X)) -> U21(X)
r33: U31(mark(X1),X2) -> U31(X1,X2)
r34: U31(X1,mark(X2)) -> U31(X1,X2)
r35: U31(active(X1),X2) -> U31(X1,X2)
r36: U31(X1,active(X2)) -> U31(X1,X2)
r37: U41(mark(X1),X2,X3) -> U41(X1,X2,X3)
r38: U41(X1,mark(X2),X3) -> U41(X1,X2,X3)
r39: U41(X1,X2,mark(X3)) -> U41(X1,X2,X3)
r40: U41(active(X1),X2,X3) -> U41(X1,X2,X3)
r41: U41(X1,active(X2),X3) -> U41(X1,X2,X3)
r42: U41(X1,X2,active(X3)) -> U41(X1,X2,X3)
r43: U42(mark(X1),X2,X3) -> U42(X1,X2,X3)
r44: U42(X1,mark(X2),X3) -> U42(X1,X2,X3)
r45: U42(X1,X2,mark(X3)) -> U42(X1,X2,X3)
r46: U42(active(X1),X2,X3) -> U42(X1,X2,X3)
r47: U42(X1,active(X2),X3) -> U42(X1,X2,X3)
r48: U42(X1,X2,active(X3)) -> U42(X1,X2,X3)
r49: s(mark(X)) -> s(X)
r50: s(active(X)) -> s(X)
r51: plus(mark(X1),X2) -> plus(X1,X2)
r52: plus(X1,mark(X2)) -> plus(X1,X2)
r53: plus(active(X1),X2) -> plus(X1,X2)
r54: plus(X1,active(X2)) -> plus(X1,X2)

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  lexicographic combination of reduction pairs:
  
    1. matrix interpretations:
    
      carrier: N^4
      order: lexicographic order
      interpretations:
        isNat#_A(x1) = ((0,0,0,0),(1,0,0,0),(1,0,0,0),(0,0,0,0)) x1
        mark_A(x1) = ((1,0,0,0),(0,0,0,0),(0,1,0,0),(1,1,1,0)) x1 + (1,1,1,1)
        active_A(x1) = ((1,0,0,0),(0,0,0,0),(0,0,0,0),(1,1,0,0)) x1 + (1,1,1,1)
    
    2. lexicographic path order with precedence:
    
      precedence:
      
        mark > isNat# > active
      
      argument filter:
    
        pi(isNat#) = []
        pi(mark) = []
        pi(active) = []
    

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

and R consists of:

r1: active(U11(tt(),V2)) -> mark(U12(isNat(V2)))
r2: active(U12(tt())) -> mark(tt())
r3: active(U21(tt())) -> mark(tt())
r4: active(U31(tt(),N)) -> mark(N)
r5: active(U41(tt(),M,N)) -> mark(U42(isNat(N),M,N))
r6: active(U42(tt(),M,N)) -> mark(s(plus(N,M)))
r7: active(isNat(|0|())) -> mark(tt())
r8: active(isNat(plus(V1,V2))) -> mark(U11(isNat(V1),V2))
r9: active(isNat(s(V1))) -> mark(U21(isNat(V1)))
r10: active(plus(N,|0|())) -> mark(U31(isNat(N),N))
r11: active(plus(N,s(M))) -> mark(U41(isNat(M),M,N))
r12: mark(U11(X1,X2)) -> active(U11(mark(X1),X2))
r13: mark(tt()) -> active(tt())
r14: mark(U12(X)) -> active(U12(mark(X)))
r15: mark(isNat(X)) -> active(isNat(X))
r16: mark(U21(X)) -> active(U21(mark(X)))
r17: mark(U31(X1,X2)) -> active(U31(mark(X1),X2))
r18: mark(U41(X1,X2,X3)) -> active(U41(mark(X1),X2,X3))
r19: mark(U42(X1,X2,X3)) -> active(U42(mark(X1),X2,X3))
r20: mark(s(X)) -> active(s(mark(X)))
r21: mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2)))
r22: mark(|0|()) -> active(|0|())
r23: U11(mark(X1),X2) -> U11(X1,X2)
r24: U11(X1,mark(X2)) -> U11(X1,X2)
r25: U11(active(X1),X2) -> U11(X1,X2)
r26: U11(X1,active(X2)) -> U11(X1,X2)
r27: U12(mark(X)) -> U12(X)
r28: U12(active(X)) -> U12(X)
r29: isNat(mark(X)) -> isNat(X)
r30: isNat(active(X)) -> isNat(X)
r31: U21(mark(X)) -> U21(X)
r32: U21(active(X)) -> U21(X)
r33: U31(mark(X1),X2) -> U31(X1,X2)
r34: U31(X1,mark(X2)) -> U31(X1,X2)
r35: U31(active(X1),X2) -> U31(X1,X2)
r36: U31(X1,active(X2)) -> U31(X1,X2)
r37: U41(mark(X1),X2,X3) -> U41(X1,X2,X3)
r38: U41(X1,mark(X2),X3) -> U41(X1,X2,X3)
r39: U41(X1,X2,mark(X3)) -> U41(X1,X2,X3)
r40: U41(active(X1),X2,X3) -> U41(X1,X2,X3)
r41: U41(X1,active(X2),X3) -> U41(X1,X2,X3)
r42: U41(X1,X2,active(X3)) -> U41(X1,X2,X3)
r43: U42(mark(X1),X2,X3) -> U42(X1,X2,X3)
r44: U42(X1,mark(X2),X3) -> U42(X1,X2,X3)
r45: U42(X1,X2,mark(X3)) -> U42(X1,X2,X3)
r46: U42(active(X1),X2,X3) -> U42(X1,X2,X3)
r47: U42(X1,active(X2),X3) -> U42(X1,X2,X3)
r48: U42(X1,X2,active(X3)) -> U42(X1,X2,X3)
r49: s(mark(X)) -> s(X)
r50: s(active(X)) -> s(X)
r51: plus(mark(X1),X2) -> plus(X1,X2)
r52: plus(X1,mark(X2)) -> plus(X1,X2)
r53: plus(active(X1),X2) -> plus(X1,X2)
r54: plus(X1,active(X2)) -> plus(X1,X2)

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  lexicographic combination of reduction pairs:
  
    1. matrix interpretations:
    
      carrier: N^4
      order: lexicographic order
      interpretations:
        U42#_A(x1,x2,x3) = ((1,0,0,0),(0,0,0,0),(1,1,0,0),(1,1,1,0)) x1 + ((1,0,0,0),(0,1,0,0),(0,1,1,0),(0,1,1,0)) x2 + ((1,0,0,0),(0,1,0,0),(0,0,1,0),(0,1,1,0)) x3
        mark_A(x1) = ((1,0,0,0),(0,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,0)
    
    2. lexicographic path order with precedence:
    
      precedence:
      
        mark > active > U42#
      
      argument filter:
    
        pi(U42#) = []
        pi(mark) = []
        pi(active) = []
    

The next rules are strictly ordered:

  p1, p2, p3, p4, p5, p6

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

-- Reduction pair.

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

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

and R consists of:

r1: active(U11(tt(),V2)) -> mark(U12(isNat(V2)))
r2: active(U12(tt())) -> mark(tt())
r3: active(U21(tt())) -> mark(tt())
r4: active(U31(tt(),N)) -> mark(N)
r5: active(U41(tt(),M,N)) -> mark(U42(isNat(N),M,N))
r6: active(U42(tt(),M,N)) -> mark(s(plus(N,M)))
r7: active(isNat(|0|())) -> mark(tt())
r8: active(isNat(plus(V1,V2))) -> mark(U11(isNat(V1),V2))
r9: active(isNat(s(V1))) -> mark(U21(isNat(V1)))
r10: active(plus(N,|0|())) -> mark(U31(isNat(N),N))
r11: active(plus(N,s(M))) -> mark(U41(isNat(M),M,N))
r12: mark(U11(X1,X2)) -> active(U11(mark(X1),X2))
r13: mark(tt()) -> active(tt())
r14: mark(U12(X)) -> active(U12(mark(X)))
r15: mark(isNat(X)) -> active(isNat(X))
r16: mark(U21(X)) -> active(U21(mark(X)))
r17: mark(U31(X1,X2)) -> active(U31(mark(X1),X2))
r18: mark(U41(X1,X2,X3)) -> active(U41(mark(X1),X2,X3))
r19: mark(U42(X1,X2,X3)) -> active(U42(mark(X1),X2,X3))
r20: mark(s(X)) -> active(s(mark(X)))
r21: mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2)))
r22: mark(|0|()) -> active(|0|())
r23: U11(mark(X1),X2) -> U11(X1,X2)
r24: U11(X1,mark(X2)) -> U11(X1,X2)
r25: U11(active(X1),X2) -> U11(X1,X2)
r26: U11(X1,active(X2)) -> U11(X1,X2)
r27: U12(mark(X)) -> U12(X)
r28: U12(active(X)) -> U12(X)
r29: isNat(mark(X)) -> isNat(X)
r30: isNat(active(X)) -> isNat(X)
r31: U21(mark(X)) -> U21(X)
r32: U21(active(X)) -> U21(X)
r33: U31(mark(X1),X2) -> U31(X1,X2)
r34: U31(X1,mark(X2)) -> U31(X1,X2)
r35: U31(active(X1),X2) -> U31(X1,X2)
r36: U31(X1,active(X2)) -> U31(X1,X2)
r37: U41(mark(X1),X2,X3) -> U41(X1,X2,X3)
r38: U41(X1,mark(X2),X3) -> U41(X1,X2,X3)
r39: U41(X1,X2,mark(X3)) -> U41(X1,X2,X3)
r40: U41(active(X1),X2,X3) -> U41(X1,X2,X3)
r41: U41(X1,active(X2),X3) -> U41(X1,X2,X3)
r42: U41(X1,X2,active(X3)) -> U41(X1,X2,X3)
r43: U42(mark(X1),X2,X3) -> U42(X1,X2,X3)
r44: U42(X1,mark(X2),X3) -> U42(X1,X2,X3)
r45: U42(X1,X2,mark(X3)) -> U42(X1,X2,X3)
r46: U42(active(X1),X2,X3) -> U42(X1,X2,X3)
r47: U42(X1,active(X2),X3) -> U42(X1,X2,X3)
r48: U42(X1,X2,active(X3)) -> U42(X1,X2,X3)
r49: s(mark(X)) -> s(X)
r50: s(active(X)) -> s(X)
r51: plus(mark(X1),X2) -> plus(X1,X2)
r52: plus(X1,mark(X2)) -> plus(X1,X2)
r53: plus(active(X1),X2) -> plus(X1,X2)
r54: plus(X1,active(X2)) -> plus(X1,X2)

The set of usable rules consists of

  (no rules)

Take the monotone reduction pair:

  lexicographic combination of reduction pairs:
  
    1. 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)
    
    2. lexicographic path order with precedence:
    
      precedence:
      
        s# > active > mark
      
      argument filter:
    
        pi(s#) = 1
        pi(mark) = [1]
        pi(active) = [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

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(),V2)) -> mark(U12(isNat(V2)))
r2: active(U12(tt())) -> mark(tt())
r3: active(U21(tt())) -> mark(tt())
r4: active(U31(tt(),N)) -> mark(N)
r5: active(U41(tt(),M,N)) -> mark(U42(isNat(N),M,N))
r6: active(U42(tt(),M,N)) -> mark(s(plus(N,M)))
r7: active(isNat(|0|())) -> mark(tt())
r8: active(isNat(plus(V1,V2))) -> mark(U11(isNat(V1),V2))
r9: active(isNat(s(V1))) -> mark(U21(isNat(V1)))
r10: active(plus(N,|0|())) -> mark(U31(isNat(N),N))
r11: active(plus(N,s(M))) -> mark(U41(isNat(M),M,N))
r12: mark(U11(X1,X2)) -> active(U11(mark(X1),X2))
r13: mark(tt()) -> active(tt())
r14: mark(U12(X)) -> active(U12(mark(X)))
r15: mark(isNat(X)) -> active(isNat(X))
r16: mark(U21(X)) -> active(U21(mark(X)))
r17: mark(U31(X1,X2)) -> active(U31(mark(X1),X2))
r18: mark(U41(X1,X2,X3)) -> active(U41(mark(X1),X2,X3))
r19: mark(U42(X1,X2,X3)) -> active(U42(mark(X1),X2,X3))
r20: mark(s(X)) -> active(s(mark(X)))
r21: mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2)))
r22: mark(|0|()) -> active(|0|())
r23: U11(mark(X1),X2) -> U11(X1,X2)
r24: U11(X1,mark(X2)) -> U11(X1,X2)
r25: U11(active(X1),X2) -> U11(X1,X2)
r26: U11(X1,active(X2)) -> U11(X1,X2)
r27: U12(mark(X)) -> U12(X)
r28: U12(active(X)) -> U12(X)
r29: isNat(mark(X)) -> isNat(X)
r30: isNat(active(X)) -> isNat(X)
r31: U21(mark(X)) -> U21(X)
r32: U21(active(X)) -> U21(X)
r33: U31(mark(X1),X2) -> U31(X1,X2)
r34: U31(X1,mark(X2)) -> U31(X1,X2)
r35: U31(active(X1),X2) -> U31(X1,X2)
r36: U31(X1,active(X2)) -> U31(X1,X2)
r37: U41(mark(X1),X2,X3) -> U41(X1,X2,X3)
r38: U41(X1,mark(X2),X3) -> U41(X1,X2,X3)
r39: U41(X1,X2,mark(X3)) -> U41(X1,X2,X3)
r40: U41(active(X1),X2,X3) -> U41(X1,X2,X3)
r41: U41(X1,active(X2),X3) -> U41(X1,X2,X3)
r42: U41(X1,X2,active(X3)) -> U41(X1,X2,X3)
r43: U42(mark(X1),X2,X3) -> U42(X1,X2,X3)
r44: U42(X1,mark(X2),X3) -> U42(X1,X2,X3)
r45: U42(X1,X2,mark(X3)) -> U42(X1,X2,X3)
r46: U42(active(X1),X2,X3) -> U42(X1,X2,X3)
r47: U42(X1,active(X2),X3) -> U42(X1,X2,X3)
r48: U42(X1,X2,active(X3)) -> U42(X1,X2,X3)
r49: s(mark(X)) -> s(X)
r50: s(active(X)) -> s(X)
r51: plus(mark(X1),X2) -> plus(X1,X2)
r52: plus(X1,mark(X2)) -> plus(X1,X2)
r53: plus(active(X1),X2) -> plus(X1,X2)
r54: plus(X1,active(X2)) -> plus(X1,X2)

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  lexicographic combination of reduction pairs:
  
    1. matrix interpretations:
    
      carrier: N^4
      order: lexicographic order
      interpretations:
        plus#_A(x1,x2) = ((1,0,0,0),(0,1,0,0),(0,0,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),(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)
    
    2. lexicographic path order with precedence:
    
      precedence:
      
        plus# > active > mark
      
      argument filter:
    
        pi(plus#) = 2
        pi(mark) = [1]
        pi(active) = 1
    

The next rules are strictly ordered:

  p1, p2, p3, p4

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(),V2)) -> mark(U12(isNat(V2)))
r2: active(U12(tt())) -> mark(tt())
r3: active(U21(tt())) -> mark(tt())
r4: active(U31(tt(),N)) -> mark(N)
r5: active(U41(tt(),M,N)) -> mark(U42(isNat(N),M,N))
r6: active(U42(tt(),M,N)) -> mark(s(plus(N,M)))
r7: active(isNat(|0|())) -> mark(tt())
r8: active(isNat(plus(V1,V2))) -> mark(U11(isNat(V1),V2))
r9: active(isNat(s(V1))) -> mark(U21(isNat(V1)))
r10: active(plus(N,|0|())) -> mark(U31(isNat(N),N))
r11: active(plus(N,s(M))) -> mark(U41(isNat(M),M,N))
r12: mark(U11(X1,X2)) -> active(U11(mark(X1),X2))
r13: mark(tt()) -> active(tt())
r14: mark(U12(X)) -> active(U12(mark(X)))
r15: mark(isNat(X)) -> active(isNat(X))
r16: mark(U21(X)) -> active(U21(mark(X)))
r17: mark(U31(X1,X2)) -> active(U31(mark(X1),X2))
r18: mark(U41(X1,X2,X3)) -> active(U41(mark(X1),X2,X3))
r19: mark(U42(X1,X2,X3)) -> active(U42(mark(X1),X2,X3))
r20: mark(s(X)) -> active(s(mark(X)))
r21: mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2)))
r22: mark(|0|()) -> active(|0|())
r23: U11(mark(X1),X2) -> U11(X1,X2)
r24: U11(X1,mark(X2)) -> U11(X1,X2)
r25: U11(active(X1),X2) -> U11(X1,X2)
r26: U11(X1,active(X2)) -> U11(X1,X2)
r27: U12(mark(X)) -> U12(X)
r28: U12(active(X)) -> U12(X)
r29: isNat(mark(X)) -> isNat(X)
r30: isNat(active(X)) -> isNat(X)
r31: U21(mark(X)) -> U21(X)
r32: U21(active(X)) -> U21(X)
r33: U31(mark(X1),X2) -> U31(X1,X2)
r34: U31(X1,mark(X2)) -> U31(X1,X2)
r35: U31(active(X1),X2) -> U31(X1,X2)
r36: U31(X1,active(X2)) -> U31(X1,X2)
r37: U41(mark(X1),X2,X3) -> U41(X1,X2,X3)
r38: U41(X1,mark(X2),X3) -> U41(X1,X2,X3)
r39: U41(X1,X2,mark(X3)) -> U41(X1,X2,X3)
r40: U41(active(X1),X2,X3) -> U41(X1,X2,X3)
r41: U41(X1,active(X2),X3) -> U41(X1,X2,X3)
r42: U41(X1,X2,active(X3)) -> U41(X1,X2,X3)
r43: U42(mark(X1),X2,X3) -> U42(X1,X2,X3)
r44: U42(X1,mark(X2),X3) -> U42(X1,X2,X3)
r45: U42(X1,X2,mark(X3)) -> U42(X1,X2,X3)
r46: U42(active(X1),X2,X3) -> U42(X1,X2,X3)
r47: U42(X1,active(X2),X3) -> U42(X1,X2,X3)
r48: U42(X1,X2,active(X3)) -> U42(X1,X2,X3)
r49: s(mark(X)) -> s(X)
r50: s(active(X)) -> s(X)
r51: plus(mark(X1),X2) -> plus(X1,X2)
r52: plus(X1,mark(X2)) -> plus(X1,X2)
r53: plus(active(X1),X2) -> plus(X1,X2)
r54: plus(X1,active(X2)) -> plus(X1,X2)

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  lexicographic combination of reduction pairs:
  
    1. matrix interpretations:
    
      carrier: N^4
      order: lexicographic order
      interpretations:
        U11#_A(x1,x2) = ((1,0,0,0),(0,1,0,0),(0,0,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),(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)
    
    2. lexicographic path order with precedence:
    
      precedence:
      
        U11# > active > mark
      
      argument filter:
    
        pi(U11#) = 2
        pi(mark) = [1]
        pi(active) = 1
    

The next rules are strictly ordered:

  p1, p2, p3, p4

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

and R consists of:

r1: active(U11(tt(),V2)) -> mark(U12(isNat(V2)))
r2: active(U12(tt())) -> mark(tt())
r3: active(U21(tt())) -> mark(tt())
r4: active(U31(tt(),N)) -> mark(N)
r5: active(U41(tt(),M,N)) -> mark(U42(isNat(N),M,N))
r6: active(U42(tt(),M,N)) -> mark(s(plus(N,M)))
r7: active(isNat(|0|())) -> mark(tt())
r8: active(isNat(plus(V1,V2))) -> mark(U11(isNat(V1),V2))
r9: active(isNat(s(V1))) -> mark(U21(isNat(V1)))
r10: active(plus(N,|0|())) -> mark(U31(isNat(N),N))
r11: active(plus(N,s(M))) -> mark(U41(isNat(M),M,N))
r12: mark(U11(X1,X2)) -> active(U11(mark(X1),X2))
r13: mark(tt()) -> active(tt())
r14: mark(U12(X)) -> active(U12(mark(X)))
r15: mark(isNat(X)) -> active(isNat(X))
r16: mark(U21(X)) -> active(U21(mark(X)))
r17: mark(U31(X1,X2)) -> active(U31(mark(X1),X2))
r18: mark(U41(X1,X2,X3)) -> active(U41(mark(X1),X2,X3))
r19: mark(U42(X1,X2,X3)) -> active(U42(mark(X1),X2,X3))
r20: mark(s(X)) -> active(s(mark(X)))
r21: mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2)))
r22: mark(|0|()) -> active(|0|())
r23: U11(mark(X1),X2) -> U11(X1,X2)
r24: U11(X1,mark(X2)) -> U11(X1,X2)
r25: U11(active(X1),X2) -> U11(X1,X2)
r26: U11(X1,active(X2)) -> U11(X1,X2)
r27: U12(mark(X)) -> U12(X)
r28: U12(active(X)) -> U12(X)
r29: isNat(mark(X)) -> isNat(X)
r30: isNat(active(X)) -> isNat(X)
r31: U21(mark(X)) -> U21(X)
r32: U21(active(X)) -> U21(X)
r33: U31(mark(X1),X2) -> U31(X1,X2)
r34: U31(X1,mark(X2)) -> U31(X1,X2)
r35: U31(active(X1),X2) -> U31(X1,X2)
r36: U31(X1,active(X2)) -> U31(X1,X2)
r37: U41(mark(X1),X2,X3) -> U41(X1,X2,X3)
r38: U41(X1,mark(X2),X3) -> U41(X1,X2,X3)
r39: U41(X1,X2,mark(X3)) -> U41(X1,X2,X3)
r40: U41(active(X1),X2,X3) -> U41(X1,X2,X3)
r41: U41(X1,active(X2),X3) -> U41(X1,X2,X3)
r42: U41(X1,X2,active(X3)) -> U41(X1,X2,X3)
r43: U42(mark(X1),X2,X3) -> U42(X1,X2,X3)
r44: U42(X1,mark(X2),X3) -> U42(X1,X2,X3)
r45: U42(X1,X2,mark(X3)) -> U42(X1,X2,X3)
r46: U42(active(X1),X2,X3) -> U42(X1,X2,X3)
r47: U42(X1,active(X2),X3) -> U42(X1,X2,X3)
r48: U42(X1,X2,active(X3)) -> U42(X1,X2,X3)
r49: s(mark(X)) -> s(X)
r50: s(active(X)) -> s(X)
r51: plus(mark(X1),X2) -> plus(X1,X2)
r52: plus(X1,mark(X2)) -> plus(X1,X2)
r53: plus(active(X1),X2) -> plus(X1,X2)
r54: plus(X1,active(X2)) -> plus(X1,X2)

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  lexicographic combination of reduction pairs:
  
    1. matrix interpretations:
    
      carrier: N^4
      order: lexicographic order
      interpretations:
        U21#_A(x1) = ((1,0,0,0),(1,0,0,0),(0,0,0,0),(1,0,0,0)) x1
        mark_A(x1) = ((1,0,0,0),(0,0,0,0),(0,1,0,0),(1,1,1,0)) x1 + (1,1,0,1)
        active_A(x1) = ((1,0,0,0),(1,1,0,0),(1,1,1,0),(1,1,1,1)) x1 + (1,0,1,1)
    
    2. lexicographic path order with precedence:
    
      precedence:
      
        mark > active > U21#
      
      argument filter:
    
        pi(U21#) = []
        pi(mark) = []
        pi(active) = []
    

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

and R consists of:

r1: active(U11(tt(),V2)) -> mark(U12(isNat(V2)))
r2: active(U12(tt())) -> mark(tt())
r3: active(U21(tt())) -> mark(tt())
r4: active(U31(tt(),N)) -> mark(N)
r5: active(U41(tt(),M,N)) -> mark(U42(isNat(N),M,N))
r6: active(U42(tt(),M,N)) -> mark(s(plus(N,M)))
r7: active(isNat(|0|())) -> mark(tt())
r8: active(isNat(plus(V1,V2))) -> mark(U11(isNat(V1),V2))
r9: active(isNat(s(V1))) -> mark(U21(isNat(V1)))
r10: active(plus(N,|0|())) -> mark(U31(isNat(N),N))
r11: active(plus(N,s(M))) -> mark(U41(isNat(M),M,N))
r12: mark(U11(X1,X2)) -> active(U11(mark(X1),X2))
r13: mark(tt()) -> active(tt())
r14: mark(U12(X)) -> active(U12(mark(X)))
r15: mark(isNat(X)) -> active(isNat(X))
r16: mark(U21(X)) -> active(U21(mark(X)))
r17: mark(U31(X1,X2)) -> active(U31(mark(X1),X2))
r18: mark(U41(X1,X2,X3)) -> active(U41(mark(X1),X2,X3))
r19: mark(U42(X1,X2,X3)) -> active(U42(mark(X1),X2,X3))
r20: mark(s(X)) -> active(s(mark(X)))
r21: mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2)))
r22: mark(|0|()) -> active(|0|())
r23: U11(mark(X1),X2) -> U11(X1,X2)
r24: U11(X1,mark(X2)) -> U11(X1,X2)
r25: U11(active(X1),X2) -> U11(X1,X2)
r26: U11(X1,active(X2)) -> U11(X1,X2)
r27: U12(mark(X)) -> U12(X)
r28: U12(active(X)) -> U12(X)
r29: isNat(mark(X)) -> isNat(X)
r30: isNat(active(X)) -> isNat(X)
r31: U21(mark(X)) -> U21(X)
r32: U21(active(X)) -> U21(X)
r33: U31(mark(X1),X2) -> U31(X1,X2)
r34: U31(X1,mark(X2)) -> U31(X1,X2)
r35: U31(active(X1),X2) -> U31(X1,X2)
r36: U31(X1,active(X2)) -> U31(X1,X2)
r37: U41(mark(X1),X2,X3) -> U41(X1,X2,X3)
r38: U41(X1,mark(X2),X3) -> U41(X1,X2,X3)
r39: U41(X1,X2,mark(X3)) -> U41(X1,X2,X3)
r40: U41(active(X1),X2,X3) -> U41(X1,X2,X3)
r41: U41(X1,active(X2),X3) -> U41(X1,X2,X3)
r42: U41(X1,X2,active(X3)) -> U41(X1,X2,X3)
r43: U42(mark(X1),X2,X3) -> U42(X1,X2,X3)
r44: U42(X1,mark(X2),X3) -> U42(X1,X2,X3)
r45: U42(X1,X2,mark(X3)) -> U42(X1,X2,X3)
r46: U42(active(X1),X2,X3) -> U42(X1,X2,X3)
r47: U42(X1,active(X2),X3) -> U42(X1,X2,X3)
r48: U42(X1,X2,active(X3)) -> U42(X1,X2,X3)
r49: s(mark(X)) -> s(X)
r50: s(active(X)) -> s(X)
r51: plus(mark(X1),X2) -> plus(X1,X2)
r52: plus(X1,mark(X2)) -> plus(X1,X2)
r53: plus(active(X1),X2) -> plus(X1,X2)
r54: plus(X1,active(X2)) -> plus(X1,X2)

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  lexicographic combination of reduction pairs:
  
    1. matrix interpretations:
    
      carrier: N^4
      order: lexicographic order
      interpretations:
        U31#_A(x1,x2) = ((1,0,0,0),(0,1,0,0),(0,0,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),(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)
    
    2. lexicographic path order with precedence:
    
      precedence:
      
        U31# > active > mark
      
      argument filter:
    
        pi(U31#) = 2
        pi(mark) = [1]
        pi(active) = 1
    

The next rules are strictly ordered:

  p1, p2, p3, p4

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

-- Reduction pair.

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

p1: U41#(mark(X1),X2,X3) -> U41#(X1,X2,X3)
p2: U41#(X1,X2,active(X3)) -> U41#(X1,X2,X3)
p3: U41#(X1,active(X2),X3) -> U41#(X1,X2,X3)
p4: U41#(active(X1),X2,X3) -> U41#(X1,X2,X3)
p5: U41#(X1,X2,mark(X3)) -> U41#(X1,X2,X3)
p6: U41#(X1,mark(X2),X3) -> U41#(X1,X2,X3)

and R consists of:

r1: active(U11(tt(),V2)) -> mark(U12(isNat(V2)))
r2: active(U12(tt())) -> mark(tt())
r3: active(U21(tt())) -> mark(tt())
r4: active(U31(tt(),N)) -> mark(N)
r5: active(U41(tt(),M,N)) -> mark(U42(isNat(N),M,N))
r6: active(U42(tt(),M,N)) -> mark(s(plus(N,M)))
r7: active(isNat(|0|())) -> mark(tt())
r8: active(isNat(plus(V1,V2))) -> mark(U11(isNat(V1),V2))
r9: active(isNat(s(V1))) -> mark(U21(isNat(V1)))
r10: active(plus(N,|0|())) -> mark(U31(isNat(N),N))
r11: active(plus(N,s(M))) -> mark(U41(isNat(M),M,N))
r12: mark(U11(X1,X2)) -> active(U11(mark(X1),X2))
r13: mark(tt()) -> active(tt())
r14: mark(U12(X)) -> active(U12(mark(X)))
r15: mark(isNat(X)) -> active(isNat(X))
r16: mark(U21(X)) -> active(U21(mark(X)))
r17: mark(U31(X1,X2)) -> active(U31(mark(X1),X2))
r18: mark(U41(X1,X2,X3)) -> active(U41(mark(X1),X2,X3))
r19: mark(U42(X1,X2,X3)) -> active(U42(mark(X1),X2,X3))
r20: mark(s(X)) -> active(s(mark(X)))
r21: mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2)))
r22: mark(|0|()) -> active(|0|())
r23: U11(mark(X1),X2) -> U11(X1,X2)
r24: U11(X1,mark(X2)) -> U11(X1,X2)
r25: U11(active(X1),X2) -> U11(X1,X2)
r26: U11(X1,active(X2)) -> U11(X1,X2)
r27: U12(mark(X)) -> U12(X)
r28: U12(active(X)) -> U12(X)
r29: isNat(mark(X)) -> isNat(X)
r30: isNat(active(X)) -> isNat(X)
r31: U21(mark(X)) -> U21(X)
r32: U21(active(X)) -> U21(X)
r33: U31(mark(X1),X2) -> U31(X1,X2)
r34: U31(X1,mark(X2)) -> U31(X1,X2)
r35: U31(active(X1),X2) -> U31(X1,X2)
r36: U31(X1,active(X2)) -> U31(X1,X2)
r37: U41(mark(X1),X2,X3) -> U41(X1,X2,X3)
r38: U41(X1,mark(X2),X3) -> U41(X1,X2,X3)
r39: U41(X1,X2,mark(X3)) -> U41(X1,X2,X3)
r40: U41(active(X1),X2,X3) -> U41(X1,X2,X3)
r41: U41(X1,active(X2),X3) -> U41(X1,X2,X3)
r42: U41(X1,X2,active(X3)) -> U41(X1,X2,X3)
r43: U42(mark(X1),X2,X3) -> U42(X1,X2,X3)
r44: U42(X1,mark(X2),X3) -> U42(X1,X2,X3)
r45: U42(X1,X2,mark(X3)) -> U42(X1,X2,X3)
r46: U42(active(X1),X2,X3) -> U42(X1,X2,X3)
r47: U42(X1,active(X2),X3) -> U42(X1,X2,X3)
r48: U42(X1,X2,active(X3)) -> U42(X1,X2,X3)
r49: s(mark(X)) -> s(X)
r50: s(active(X)) -> s(X)
r51: plus(mark(X1),X2) -> plus(X1,X2)
r52: plus(X1,mark(X2)) -> plus(X1,X2)
r53: plus(active(X1),X2) -> plus(X1,X2)
r54: plus(X1,active(X2)) -> plus(X1,X2)

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  lexicographic combination of reduction pairs:
  
    1. matrix interpretations:
    
      carrier: N^4
      order: lexicographic order
      interpretations:
        U41#_A(x1,x2,x3) = ((1,0,0,0),(0,1,0,0),(0,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),(0,1,0,0),(0,0,0,0),(1,1,1,0)) 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,0,1,0),(1,1,1,1)) x1 + (1,1,1,1)
    
    2. lexicographic path order with precedence:
    
      precedence:
      
        U41# > active > mark
      
      argument filter:
    
        pi(U41#) = [1, 2]
        pi(mark) = [1]
        pi(active) = [1]
    

The next rules are strictly ordered:

  p1, p2, p3, p4, p5, p6

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