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:

  matrix interpretations:
  
    carrier: N^2
    order: standard order
    interpretations:
      active#_A(x1) = ((1,0),(1,0)) x1
      U11_A(x1,x2) = ((1,1),(0,0)) x1
      tt_A() = (0,0)
      mark#_A(x1) = ((1,0),(1,0)) x1
      U12_A(x1) = ((1,1),(0,0)) x1
      isNat_A(x1) = (0,0)
      plus_A(x1,x2) = ((1,1),(0,0)) x1 + ((1,1),(0,0)) x2 + (1,1)
      mark_A(x1) = ((1,1),(0,0)) x1
      s_A(x1) = ((1,1),(0,0)) x1 + (1,3)
      U41_A(x1,x2,x3) = ((1,1),(0,0)) x1 + ((1,1),(0,0)) x2 + ((1,1),(0,0)) x3 + (4,2)
      |0|_A() = (1,1)
      U31_A(x1,x2) = ((1,1),(0,0)) x1 + ((1,1),(0,0)) x2 + (3,1)
      U42_A(x1,x2,x3) = ((1,1),(0,0)) x1 + ((1,1),(0,0)) x2 + ((1,1),(0,0)) x3 + (4,2)
      U21_A(x1) = ((1,1),(0,0)) x1
      active_A(x1) = ((1,1),(0,0)) x1

The next rules are strictly ordered:

  p2, p3, p5, p6, p9, p12, p15, p17, p22

We remove them from the problem.

-- SCC decomposition.

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)) -> active#(plus(mark(X1),mark(X2)))
p3: mark#(s(X)) -> active#(s(mark(X)))
p4: active#(plus(N,|0|())) -> mark#(U31(isNat(N),N))
p5: mark#(U42(X1,X2,X3)) -> active#(U42(mark(X1),X2,X3))
p6: active#(isNat(s(V1))) -> mark#(U21(isNat(V1)))
p7: mark#(U41(X1,X2,X3)) -> active#(U41(mark(X1),X2,X3))
p8: active#(isNat(plus(V1,V2))) -> mark#(U11(isNat(V1),V2))
p9: mark#(U31(X1,X2)) -> active#(U31(mark(X1),X2))
p10: mark#(U21(X)) -> mark#(X)
p11: mark#(U21(X)) -> active#(U21(mark(X)))
p12: active#(U41(tt(),M,N)) -> mark#(U42(isNat(N),M,N))
p13: mark#(isNat(X)) -> active#(isNat(X))
p14: mark#(U12(X)) -> mark#(X)
p15: mark#(U12(X)) -> active#(U12(mark(X)))
p16: mark#(U11(X1,X2)) -> mark#(X1)
p17: 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 estimated dependency graph contains the following SCCs:

  {p1, p2, p3, p4, p5, p6, p7, p8, p9, p10, p11, p12, p13, p14, p15, p16, p17}


-- Reduction pair.

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

p1: active#(U11(tt(),V2)) -> mark#(U12(isNat(V2)))
p2: mark#(U11(X1,X2)) -> active#(U11(mark(X1),X2))
p3: active#(U41(tt(),M,N)) -> mark#(U42(isNat(N),M,N))
p4: mark#(U11(X1,X2)) -> mark#(X1)
p5: mark#(U12(X)) -> active#(U12(mark(X)))
p6: active#(isNat(plus(V1,V2))) -> mark#(U11(isNat(V1),V2))
p7: mark#(U12(X)) -> mark#(X)
p8: mark#(isNat(X)) -> active#(isNat(X))
p9: active#(isNat(s(V1))) -> mark#(U21(isNat(V1)))
p10: mark#(U21(X)) -> active#(U21(mark(X)))
p11: active#(plus(N,|0|())) -> mark#(U31(isNat(N),N))
p12: mark#(U21(X)) -> mark#(X)
p13: mark#(U31(X1,X2)) -> active#(U31(mark(X1),X2))
p14: mark#(U41(X1,X2,X3)) -> active#(U41(mark(X1),X2,X3))
p15: mark#(U42(X1,X2,X3)) -> active#(U42(mark(X1),X2,X3))
p16: mark#(s(X)) -> active#(s(mark(X)))
p17: mark#(plus(X1,X2)) -> active#(plus(mark(X1),mark(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:

  matrix interpretations:
  
    carrier: N^2
    order: standard order
    interpretations:
      active#_A(x1) = x1
      U11_A(x1,x2) = (2,1)
      tt_A() = (1,1)
      mark#_A(x1) = (2,0)
      U12_A(x1) = (2,1)
      isNat_A(x1) = (2,1)
      mark_A(x1) = (1,3)
      U41_A(x1,x2,x3) = (2,1)
      U42_A(x1,x2,x3) = (2,1)
      plus_A(x1,x2) = (2,1)
      s_A(x1) = (1,1)
      U21_A(x1) = (2,1)
      |0|_A() = (1,1)
      U31_A(x1,x2) = (2,1)
      active_A(x1) = ((0,0),(1,0)) x1 + (1,1)

The next rules are strictly ordered:

  p16

We remove them from the problem.

-- SCC decomposition.

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

p1: active#(U11(tt(),V2)) -> mark#(U12(isNat(V2)))
p2: mark#(U11(X1,X2)) -> active#(U11(mark(X1),X2))
p3: active#(U41(tt(),M,N)) -> mark#(U42(isNat(N),M,N))
p4: mark#(U11(X1,X2)) -> mark#(X1)
p5: mark#(U12(X)) -> active#(U12(mark(X)))
p6: active#(isNat(plus(V1,V2))) -> mark#(U11(isNat(V1),V2))
p7: mark#(U12(X)) -> mark#(X)
p8: mark#(isNat(X)) -> active#(isNat(X))
p9: active#(isNat(s(V1))) -> mark#(U21(isNat(V1)))
p10: mark#(U21(X)) -> active#(U21(mark(X)))
p11: active#(plus(N,|0|())) -> mark#(U31(isNat(N),N))
p12: mark#(U21(X)) -> mark#(X)
p13: mark#(U31(X1,X2)) -> active#(U31(mark(X1),X2))
p14: mark#(U41(X1,X2,X3)) -> active#(U41(mark(X1),X2,X3))
p15: mark#(U42(X1,X2,X3)) -> active#(U42(mark(X1),X2,X3))
p16: mark#(plus(X1,X2)) -> active#(plus(mark(X1),mark(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, p2, p3, p4, p5, p6, p7, p8, p9, p10, p11, p12, p13, p14, p15, p16}


-- 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)) -> active#(plus(mark(X1),mark(X2)))
p3: active#(plus(N,|0|())) -> mark#(U31(isNat(N),N))
p4: mark#(U42(X1,X2,X3)) -> active#(U42(mark(X1),X2,X3))
p5: active#(isNat(s(V1))) -> mark#(U21(isNat(V1)))
p6: mark#(U41(X1,X2,X3)) -> active#(U41(mark(X1),X2,X3))
p7: active#(isNat(plus(V1,V2))) -> mark#(U11(isNat(V1),V2))
p8: mark#(U31(X1,X2)) -> active#(U31(mark(X1),X2))
p9: active#(U41(tt(),M,N)) -> mark#(U42(isNat(N),M,N))
p10: mark#(U21(X)) -> mark#(X)
p11: mark#(U21(X)) -> active#(U21(mark(X)))
p12: mark#(isNat(X)) -> active#(isNat(X))
p13: mark#(U12(X)) -> mark#(X)
p14: mark#(U12(X)) -> active#(U12(mark(X)))
p15: mark#(U11(X1,X2)) -> mark#(X1)
p16: 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:

  matrix interpretations:
  
    carrier: N^2
    order: standard order
    interpretations:
      active#_A(x1) = x1
      U11_A(x1,x2) = ((1,1),(0,0)) x1 + ((1,1),(0,0)) x2 + (2,0)
      tt_A() = (1,1)
      mark#_A(x1) = x1 + (2,0)
      U12_A(x1) = ((1,1),(0,0)) x1
      isNat_A(x1) = ((1,1),(0,0)) x1 + (1,1)
      plus_A(x1,x2) = ((1,1),(1,1)) x1 + ((0,0),(1,1)) x2 + (4,1)
      mark_A(x1) = ((1,1),(0,0)) x1
      |0|_A() = (0,1)
      U31_A(x1,x2) = ((0,0),(1,1)) x1 + ((1,1),(0,0)) x2 + (1,1)
      U42_A(x1,x2,x3) = ((0,0),(1,1)) x2 + ((1,1),(1,1)) x3 + (6,4)
      s_A(x1) = ((1,1),(0,0)) x1 + (0,5)
      U21_A(x1) = ((1,1),(0,0)) x1 + (1,1)
      U41_A(x1,x2,x3) = ((0,0),(1,1)) x2 + ((1,1),(1,1)) x3 + (9,1)
      active_A(x1) = ((1,1),(0,0)) x1

The next rules are strictly ordered:

  p2, p3, p4, p5, p6, p8, p9, p10, p11, p12, p14, p15, p16

We remove them from the problem.

-- SCC decomposition.

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

p1: active#(U11(tt(),V2)) -> mark#(U12(isNat(V2)))
p2: active#(isNat(plus(V1,V2))) -> mark#(U11(isNat(V1),V2))
p3: mark#(U12(X)) -> mark#(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 estimated dependency graph contains the following SCCs:

  {p3}


-- Reduction pair.

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

p1: mark#(U12(X)) -> mark#(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:

  matrix interpretations:
  
    carrier: N^2
    order: standard order
    interpretations:
      mark#_A(x1) = ((1,0),(1,0)) x1
      U12_A(x1) = ((1,1),(1,1)) x1 + (1,0)

The next rules are strictly ordered:

  p1
  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: 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 monotone reduction pair:

  matrix interpretations:
  
    carrier: N^2
    order: standard order
    interpretations:
      U12#_A(x1) = ((1,0),(1,1)) x1
      mark_A(x1) = ((1,1),(1,1)) x1 + (1,1)
      active_A(x1) = ((1,1),(1,1)) x1 + (1,1)

The next rules are strictly ordered:

  p1, p2
  r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r12, r13, r14, r15, r16, r17, r18, r19, r20, r21, r22, r23, r24, r25, r26, r27, r28, r29, r30, r31, r32, r33, r34, r35, r36, r37, r38, r39, r40, r41, r42, r43, r44, r45, r46, r47, r48, r49, r50, r51, r52, r53, r54

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 monotone reduction pair:

  matrix interpretations:
  
    carrier: N^2
    order: standard order
    interpretations:
      isNat#_A(x1) = ((1,0),(1,1)) x1
      mark_A(x1) = ((1,1),(1,1)) x1 + (1,1)
      active_A(x1) = ((1,1),(1,1)) x1 + (1,1)

The next rules are strictly ordered:

  p1, p2
  r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r12, r13, r14, r15, r16, r17, r18, r19, r20, r21, r22, r23, r24, r25, r26, r27, r28, r29, r30, r31, r32, r33, r34, r35, r36, r37, r38, r39, r40, r41, r42, r43, r44, r45, r46, r47, r48, r49, r50, r51, r52, r53, r54

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 monotone reduction pair:

  matrix interpretations:
  
    carrier: N^2
    order: standard order
    interpretations:
      U42#_A(x1,x2,x3) = ((1,1),(1,1)) x1 + ((1,1),(1,1)) x2 + ((1,1),(1,1)) x3
      mark_A(x1) = ((1,1),(1,1)) x1 + (1,1)
      active_A(x1) = ((1,1),(1,1)) x1 + (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, 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: 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:

  matrix interpretations:
  
    carrier: N^2
    order: standard order
    interpretations:
      s#_A(x1) = ((1,0),(1,1)) x1
      mark_A(x1) = ((1,1),(1,1)) x1 + (1,1)
      active_A(x1) = ((1,1),(1,1)) x1 + (1,1)

The next rules are strictly ordered:

  p1, p2
  r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r12, r13, r14, r15, r16, r17, r18, r19, r20, r21, r22, r23, r24, r25, r26, r27, r28, r29, r30, r31, r32, r33, r34, r35, r36, r37, r38, r39, r40, r41, r42, r43, r44, r45, r46, r47, r48, r49, r50, r51, r52, r53, r54

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:

  matrix interpretations:
  
    carrier: N^2
    order: standard order
    interpretations:
      plus#_A(x1,x2) = ((1,1),(1,1)) x1 + ((1,1),(1,1)) x2
      mark_A(x1) = ((0,1),(1,1)) x1 + (1,1)
      active_A(x1) = ((1,1),(1,1)) x1 + (1,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:

  matrix interpretations:
  
    carrier: N^2
    order: standard order
    interpretations:
      U11#_A(x1,x2) = ((1,1),(1,1)) x1 + ((1,1),(1,1)) x2
      mark_A(x1) = ((0,1),(1,1)) x1 + (1,1)
      active_A(x1) = ((1,1),(1,1)) x1 + (1,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 monotone reduction pair:

  matrix interpretations:
  
    carrier: N^2
    order: standard order
    interpretations:
      U21#_A(x1) = ((1,0),(1,1)) x1
      mark_A(x1) = ((1,1),(1,1)) x1 + (1,1)
      active_A(x1) = ((1,1),(1,1)) x1 + (1,1)

The next rules are strictly ordered:

  p1, p2
  r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r12, r13, r14, r15, r16, r17, r18, r19, r20, r21, r22, r23, r24, r25, r26, r27, r28, r29, r30, r31, r32, r33, r34, r35, r36, r37, r38, r39, r40, r41, r42, r43, r44, r45, r46, r47, r48, r49, r50, r51, r52, r53, r54

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:

  matrix interpretations:
  
    carrier: N^2
    order: standard order
    interpretations:
      U31#_A(x1,x2) = ((1,1),(1,1)) x1 + ((1,1),(1,1)) x2
      mark_A(x1) = ((0,1),(1,1)) x1 + (1,1)
      active_A(x1) = ((1,1),(1,1)) x1 + (1,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 monotone reduction pair:

  matrix interpretations:
  
    carrier: N^2
    order: standard order
    interpretations:
      U41#_A(x1,x2,x3) = ((1,1),(1,1)) x1 + ((1,1),(1,1)) x2 + ((1,1),(1,1)) x3
      mark_A(x1) = ((1,1),(1,1)) x1 + (1,1)
      active_A(x1) = ((1,1),(1,1)) x1 + (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, 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.