YES

We show the termination of the TRS R:

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

-- SCC decomposition.

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

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

and R consists of:

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

The estimated dependency graph contains the following SCCs:

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


-- Reduction pair.

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

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

and R consists of:

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

The set of usable rules consists of

  r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r12, r13, r14, r15, r16, r17, r18, r19, r20, r21, r22, r23, r24, r25, r26, r27, r28, r29, r30, r31, r32, r33, r34, r35, r36, r37, r38

Take the reduction pair:

  lexicographic combination of reduction pairs:
  
    1. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          active#_A(x1) = max{1, x1 - 2}
          U11_A(x1,x2) = max{19, x1, x2}
          tt_A = 7
          mark#_A(x1) = max{2, x1 - 2}
          isNat_A(x1) = 8
          plus_A(x1,x2) = max{16, x1, x2 + 8}
          s_A(x1) = max{8, x1}
          U21_A(x1,x2,x3) = max{16, x1, x2 + 8, x3}
          and_A(x1,x2) = max{8, x1, x2}
          mark_A(x1) = max{8, x1}
          |0|_A = 12
          active_A(x1) = max{8, x1}
    
      precedence:
      
        |0| > active# = tt = mark# = isNat = mark = active > U11 = plus > U21 > s > and
      
      partial status:
    
        pi(active#) = []
        pi(U11) = []
        pi(tt) = []
        pi(mark#) = []
        pi(isNat) = []
        pi(plus) = []
        pi(s) = []
        pi(U21) = []
        pi(and) = []
        pi(mark) = []
        pi(|0|) = []
        pi(active) = []
    
    2. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          active#_A(x1) = 0
          U11_A(x1,x2) = 40
          tt_A = 26
          mark#_A(x1) = 0
          isNat_A(x1) = 21
          plus_A(x1,x2) = 172
          s_A(x1) = 20
          U21_A(x1,x2,x3) = 184
          and_A(x1,x2) = 26
          mark_A(x1) = 36
          |0|_A = 35
          active_A(x1) = 36
    
      precedence:
      
        U11 = tt = isNat = plus = s = |0| > U21 > active# = mark# = and > mark = active
      
      partial status:
    
        pi(active#) = []
        pi(U11) = []
        pi(tt) = []
        pi(mark#) = []
        pi(isNat) = []
        pi(plus) = []
        pi(s) = []
        pi(U21) = []
        pi(and) = []
        pi(mark) = []
        pi(|0|) = []
        pi(active) = []
    

The next rules are strictly ordered:

  p7

We remove them from the problem.

-- SCC decomposition.

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

p1: active#(U11(tt(),N)) -> mark#(N)
p2: mark#(isNat(X)) -> active#(isNat(X))
p3: active#(plus(N,s(M))) -> mark#(U21(and(isNat(M),isNat(N)),M,N))
p4: mark#(and(X1,X2)) -> mark#(X1)
p5: mark#(and(X1,X2)) -> active#(and(mark(X1),X2))
p6: active#(plus(N,|0|())) -> mark#(U11(isNat(N),N))
p7: mark#(plus(X1,X2)) -> mark#(X1)
p8: mark#(plus(X1,X2)) -> active#(plus(mark(X1),mark(X2)))
p9: active#(isNat(s(V1))) -> mark#(isNat(V1))
p10: mark#(s(X)) -> mark#(X)
p11: mark#(s(X)) -> active#(s(mark(X)))
p12: active#(isNat(plus(V1,V2))) -> mark#(and(isNat(V1),isNat(V2)))
p13: mark#(U21(X1,X2,X3)) -> mark#(X1)
p14: mark#(U21(X1,X2,X3)) -> active#(U21(mark(X1),X2,X3))
p15: active#(and(tt(),X)) -> mark#(X)
p16: mark#(U11(X1,X2)) -> mark#(X1)
p17: mark#(U11(X1,X2)) -> active#(U11(mark(X1),X2))
p18: active#(U21(tt(),M,N)) -> mark#(s(plus(N,M)))

and R consists of:

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

The estimated dependency graph contains the following SCCs:

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


-- Reduction pair.

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

p1: active#(U11(tt(),N)) -> mark#(N)
p2: mark#(U11(X1,X2)) -> active#(U11(mark(X1),X2))
p3: active#(U21(tt(),M,N)) -> mark#(s(plus(N,M)))
p4: mark#(U11(X1,X2)) -> mark#(X1)
p5: mark#(U21(X1,X2,X3)) -> active#(U21(mark(X1),X2,X3))
p6: active#(and(tt(),X)) -> mark#(X)
p7: mark#(U21(X1,X2,X3)) -> mark#(X1)
p8: mark#(s(X)) -> active#(s(mark(X)))
p9: active#(isNat(plus(V1,V2))) -> mark#(and(isNat(V1),isNat(V2)))
p10: mark#(s(X)) -> mark#(X)
p11: mark#(plus(X1,X2)) -> active#(plus(mark(X1),mark(X2)))
p12: active#(isNat(s(V1))) -> mark#(isNat(V1))
p13: mark#(plus(X1,X2)) -> mark#(X1)
p14: mark#(and(X1,X2)) -> active#(and(mark(X1),X2))
p15: active#(plus(N,|0|())) -> mark#(U11(isNat(N),N))
p16: mark#(and(X1,X2)) -> mark#(X1)
p17: mark#(isNat(X)) -> active#(isNat(X))
p18: active#(plus(N,s(M))) -> mark#(U21(and(isNat(M),isNat(N)),M,N))

and R consists of:

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

The set of usable rules consists of

  r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r12, r13, r14, r15, r16, r17, r18, r19, r20, r21, r22, r23, r24, r25, r26, r27, r28, r29, r30, r31, r32, r33, r34, r35, r36, r37, r38

Take the reduction pair:

  lexicographic combination of reduction pairs:
  
    1. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          active#_A(x1) = x1 + 32
          U11_A(x1,x2) = max{x1 + 2, x2}
          tt_A = 38
          mark#_A(x1) = x1 + 32
          mark_A(x1) = x1
          U21_A(x1,x2,x3) = max{x1, x2 + 21, x3 + 42}
          s_A(x1) = max{22, x1}
          plus_A(x1,x2) = max{x1 + 42, x2 + 21}
          and_A(x1,x2) = max{x1 + 22, x2 + 12}
          isNat_A(x1) = max{7, x1 - 1}
          |0|_A = 40
          active_A(x1) = max{2, x1}
    
      precedence:
      
        tt = plus > U21 > mark = and = active > |0| > active# = U11 = mark# = s = isNat
      
      partial status:
    
        pi(active#) = []
        pi(U11) = []
        pi(tt) = []
        pi(mark#) = []
        pi(mark) = []
        pi(U21) = []
        pi(s) = []
        pi(plus) = []
        pi(and) = []
        pi(isNat) = []
        pi(|0|) = []
        pi(active) = []
    
    2. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          active#_A(x1) = 603
          U11_A(x1,x2) = 141
          tt_A = 121
          mark#_A(x1) = 603
          mark_A(x1) = 141
          U21_A(x1,x2,x3) = 3
          s_A(x1) = 172
          plus_A(x1,x2) = 141
          and_A(x1,x2) = 140
          isNat_A(x1) = 172
          |0|_A = 130
          active_A(x1) = 141
    
      precedence:
      
        active# = mark# = plus > mark = s = and = isNat = active > U21 = |0| > U11 = tt
      
      partial status:
    
        pi(active#) = []
        pi(U11) = []
        pi(tt) = []
        pi(mark#) = []
        pi(mark) = []
        pi(U21) = []
        pi(s) = []
        pi(plus) = []
        pi(and) = []
        pi(isNat) = []
        pi(|0|) = []
        pi(active) = []
    

The next rules are strictly ordered:

  p9

We remove them from the problem.

-- SCC decomposition.

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

p1: active#(U11(tt(),N)) -> mark#(N)
p2: mark#(U11(X1,X2)) -> active#(U11(mark(X1),X2))
p3: active#(U21(tt(),M,N)) -> mark#(s(plus(N,M)))
p4: mark#(U11(X1,X2)) -> mark#(X1)
p5: mark#(U21(X1,X2,X3)) -> active#(U21(mark(X1),X2,X3))
p6: active#(and(tt(),X)) -> mark#(X)
p7: mark#(U21(X1,X2,X3)) -> mark#(X1)
p8: mark#(s(X)) -> active#(s(mark(X)))
p9: mark#(s(X)) -> mark#(X)
p10: mark#(plus(X1,X2)) -> active#(plus(mark(X1),mark(X2)))
p11: active#(isNat(s(V1))) -> mark#(isNat(V1))
p12: mark#(plus(X1,X2)) -> mark#(X1)
p13: mark#(and(X1,X2)) -> active#(and(mark(X1),X2))
p14: active#(plus(N,|0|())) -> mark#(U11(isNat(N),N))
p15: mark#(and(X1,X2)) -> mark#(X1)
p16: mark#(isNat(X)) -> active#(isNat(X))
p17: active#(plus(N,s(M))) -> mark#(U21(and(isNat(M),isNat(N)),M,N))

and R consists of:

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

The estimated dependency graph contains the following SCCs:

  {p1, p2, 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(),N)) -> mark#(N)
p2: mark#(isNat(X)) -> active#(isNat(X))
p3: active#(plus(N,s(M))) -> mark#(U21(and(isNat(M),isNat(N)),M,N))
p4: mark#(and(X1,X2)) -> mark#(X1)
p5: mark#(and(X1,X2)) -> active#(and(mark(X1),X2))
p6: active#(plus(N,|0|())) -> mark#(U11(isNat(N),N))
p7: mark#(plus(X1,X2)) -> mark#(X1)
p8: mark#(plus(X1,X2)) -> active#(plus(mark(X1),mark(X2)))
p9: active#(isNat(s(V1))) -> mark#(isNat(V1))
p10: mark#(s(X)) -> mark#(X)
p11: mark#(s(X)) -> active#(s(mark(X)))
p12: active#(and(tt(),X)) -> mark#(X)
p13: mark#(U21(X1,X2,X3)) -> mark#(X1)
p14: mark#(U21(X1,X2,X3)) -> active#(U21(mark(X1),X2,X3))
p15: active#(U21(tt(),M,N)) -> mark#(s(plus(N,M)))
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(),N)) -> mark(N)
r2: active(U21(tt(),M,N)) -> mark(s(plus(N,M)))
r3: active(and(tt(),X)) -> mark(X)
r4: active(isNat(|0|())) -> mark(tt())
r5: active(isNat(plus(V1,V2))) -> mark(and(isNat(V1),isNat(V2)))
r6: active(isNat(s(V1))) -> mark(isNat(V1))
r7: active(plus(N,|0|())) -> mark(U11(isNat(N),N))
r8: active(plus(N,s(M))) -> mark(U21(and(isNat(M),isNat(N)),M,N))
r9: mark(U11(X1,X2)) -> active(U11(mark(X1),X2))
r10: mark(tt()) -> active(tt())
r11: mark(U21(X1,X2,X3)) -> active(U21(mark(X1),X2,X3))
r12: mark(s(X)) -> active(s(mark(X)))
r13: mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2)))
r14: mark(and(X1,X2)) -> active(and(mark(X1),X2))
r15: mark(isNat(X)) -> active(isNat(X))
r16: mark(|0|()) -> active(|0|())
r17: U11(mark(X1),X2) -> U11(X1,X2)
r18: U11(X1,mark(X2)) -> U11(X1,X2)
r19: U11(active(X1),X2) -> U11(X1,X2)
r20: U11(X1,active(X2)) -> U11(X1,X2)
r21: U21(mark(X1),X2,X3) -> U21(X1,X2,X3)
r22: U21(X1,mark(X2),X3) -> U21(X1,X2,X3)
r23: U21(X1,X2,mark(X3)) -> U21(X1,X2,X3)
r24: U21(active(X1),X2,X3) -> U21(X1,X2,X3)
r25: U21(X1,active(X2),X3) -> U21(X1,X2,X3)
r26: U21(X1,X2,active(X3)) -> U21(X1,X2,X3)
r27: s(mark(X)) -> s(X)
r28: s(active(X)) -> s(X)
r29: plus(mark(X1),X2) -> plus(X1,X2)
r30: plus(X1,mark(X2)) -> plus(X1,X2)
r31: plus(active(X1),X2) -> plus(X1,X2)
r32: plus(X1,active(X2)) -> plus(X1,X2)
r33: and(mark(X1),X2) -> and(X1,X2)
r34: and(X1,mark(X2)) -> and(X1,X2)
r35: and(active(X1),X2) -> and(X1,X2)
r36: and(X1,active(X2)) -> and(X1,X2)
r37: isNat(mark(X)) -> isNat(X)
r38: isNat(active(X)) -> isNat(X)

The set of usable rules consists of

  r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r12, r13, r14, r15, r16, r17, r18, r19, r20, r21, r22, r23, r24, r25, r26, r27, r28, r29, r30, r31, r32, r33, r34, r35, r36, r37, r38

Take the reduction pair:

  lexicographic combination of reduction pairs:
  
    1. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          active#_A(x1) = max{27, x1 + 22}
          U11_A(x1,x2) = max{13, x1 + 11, x2 + 10}
          tt_A = 32
          mark#_A(x1) = max{31, x1 + 22}
          isNat_A(x1) = max{22, x1 + 10}
          plus_A(x1,x2) = max{32, x1 + 22, x2 + 27}
          s_A(x1) = max{4, x1}
          U21_A(x1,x2,x3) = max{x1, x2 + 27, x3 + 22}
          and_A(x1,x2) = max{23, x1, x2 + 5}
          mark_A(x1) = max{2, x1}
          |0|_A = 23
          active_A(x1) = max{3, x1}
    
      precedence:
      
        and > plus > active# = U11 = mark# = U21 > tt > isNat = s > mark = |0| = active
      
      partial status:
    
        pi(active#) = []
        pi(U11) = []
        pi(tt) = []
        pi(mark#) = []
        pi(isNat) = []
        pi(plus) = []
        pi(s) = []
        pi(U21) = []
        pi(and) = []
        pi(mark) = [1]
        pi(|0|) = []
        pi(active) = [1]
    
    2. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          active#_A(x1) = 177
          U11_A(x1,x2) = 177
          tt_A = 134
          mark#_A(x1) = 177
          isNat_A(x1) = 177
          plus_A(x1,x2) = 167
          s_A(x1) = 46
          U21_A(x1,x2,x3) = 166
          and_A(x1,x2) = 177
          mark_A(x1) = max{226, x1 + 45}
          |0|_A = 177
          active_A(x1) = max{178, x1 + 49}
    
      precedence:
      
        mark = active > plus > active# = U11 = tt = mark# = isNat = s = U21 = and = |0|
      
      partial status:
    
        pi(active#) = []
        pi(U11) = []
        pi(tt) = []
        pi(mark#) = []
        pi(isNat) = []
        pi(plus) = []
        pi(s) = []
        pi(U21) = []
        pi(and) = []
        pi(mark) = []
        pi(|0|) = []
        pi(active) = []
    

The next rules are strictly ordered:

  p6

We remove them from the problem.

-- SCC decomposition.

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

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

The estimated dependency graph contains the following SCCs:

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

and R consists of:

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

The set of usable rules consists of

  r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r12, r13, r14, r15, r16, r17, r18, r19, r20, r21, r22, r23, r24, r25, r26, r27, r28, r29, r30, r31, r32, r33, r34, r35, r36, r37, r38

Take the reduction pair:

  lexicographic combination of reduction pairs:
  
    1. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          active#_A(x1) = max{38, x1 + 5}
          U11_A(x1,x2) = max{x1 + 13, x2 + 45}
          tt_A = 3
          mark#_A(x1) = max{38, x1 + 5}
          mark_A(x1) = x1
          U21_A(x1,x2,x3) = max{x1, x2 + 17, x3 + 45}
          s_A(x1) = max{39, x1}
          plus_A(x1,x2) = max{x1 + 45, x2 + 17}
          and_A(x1,x2) = max{6, x1, x2}
          isNat_A(x1) = max{32, x1 - 10}
          active_A(x1) = max{2, x1}
          |0|_A = 14
    
      precedence:
      
        U11 = mark = U21 = s = plus = and = isNat = active = |0| > tt > active# = mark#
      
      partial status:
    
        pi(active#) = [1]
        pi(U11) = []
        pi(tt) = []
        pi(mark#) = [1]
        pi(mark) = []
        pi(U21) = []
        pi(s) = []
        pi(plus) = []
        pi(and) = []
        pi(isNat) = []
        pi(active) = []
        pi(|0|) = []
    
    2. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          active#_A(x1) = 68
          U11_A(x1,x2) = 1
          tt_A = 64
          mark#_A(x1) = 68
          mark_A(x1) = 0
          U21_A(x1,x2,x3) = 7
          s_A(x1) = 18
          plus_A(x1,x2) = 7
          and_A(x1,x2) = 7
          isNat_A(x1) = 65
          active_A(x1) = 0
          |0|_A = 56
    
      precedence:
      
        tt > active# = U11 = mark# = and = isNat = |0| > mark = active > U21 = s = plus
      
      partial status:
    
        pi(active#) = []
        pi(U11) = []
        pi(tt) = []
        pi(mark#) = []
        pi(mark) = []
        pi(U21) = []
        pi(s) = []
        pi(plus) = []
        pi(and) = []
        pi(isNat) = []
        pi(active) = []
        pi(|0|) = []
    

The next rules are strictly ordered:

  p1

We remove them from the problem.

-- SCC decomposition.

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

p1: mark#(U11(X1,X2)) -> active#(U11(mark(X1),X2))
p2: active#(U21(tt(),M,N)) -> mark#(s(plus(N,M)))
p3: mark#(U11(X1,X2)) -> mark#(X1)
p4: mark#(U21(X1,X2,X3)) -> active#(U21(mark(X1),X2,X3))
p5: active#(and(tt(),X)) -> mark#(X)
p6: mark#(U21(X1,X2,X3)) -> mark#(X1)
p7: mark#(s(X)) -> active#(s(mark(X)))
p8: active#(isNat(s(V1))) -> mark#(isNat(V1))
p9: mark#(s(X)) -> mark#(X)
p10: mark#(plus(X1,X2)) -> active#(plus(mark(X1),mark(X2)))
p11: active#(plus(N,s(M))) -> mark#(U21(and(isNat(M),isNat(N)),M,N))
p12: mark#(plus(X1,X2)) -> mark#(X1)
p13: mark#(and(X1,X2)) -> active#(and(mark(X1),X2))
p14: mark#(and(X1,X2)) -> mark#(X1)
p15: mark#(isNat(X)) -> active#(isNat(X))

and R consists of:

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

The estimated dependency graph contains the following SCCs:

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


-- Reduction pair.

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

p1: mark#(U11(X1,X2)) -> active#(U11(mark(X1),X2))
p2: active#(plus(N,s(M))) -> mark#(U21(and(isNat(M),isNat(N)),M,N))
p3: mark#(isNat(X)) -> active#(isNat(X))
p4: active#(isNat(s(V1))) -> mark#(isNat(V1))
p5: mark#(and(X1,X2)) -> mark#(X1)
p6: mark#(and(X1,X2)) -> active#(and(mark(X1),X2))
p7: active#(and(tt(),X)) -> mark#(X)
p8: mark#(plus(X1,X2)) -> mark#(X1)
p9: mark#(plus(X1,X2)) -> active#(plus(mark(X1),mark(X2)))
p10: active#(U21(tt(),M,N)) -> mark#(s(plus(N,M)))
p11: mark#(s(X)) -> mark#(X)
p12: mark#(s(X)) -> active#(s(mark(X)))
p13: mark#(U21(X1,X2,X3)) -> mark#(X1)
p14: mark#(U21(X1,X2,X3)) -> active#(U21(mark(X1),X2,X3))
p15: mark#(U11(X1,X2)) -> mark#(X1)

and R consists of:

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

The set of usable rules consists of

  r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r12, r13, r14, r15, r16, r17, r18, r19, r20, r21, r22, r23, r24, r25, r26, r27, r28, r29, r30, r31, r32, r33, r34, r35, r36, r37, r38

Take the reduction pair:

  lexicographic combination of reduction pairs:
  
    1. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          mark#_A(x1) = x1 + 5
          U11_A(x1,x2) = max{x1, x2}
          active#_A(x1) = x1 + 5
          mark_A(x1) = x1
          plus_A(x1,x2) = max{x1 + 19, x2 + 19}
          s_A(x1) = x1
          U21_A(x1,x2,x3) = max{x1 + 9, x2 + 19, x3 + 19}
          and_A(x1,x2) = max{x1 + 1, x2 + 10}
          isNat_A(x1) = max{0, x1 - 1}
          tt_A = 4
          active_A(x1) = x1
          |0|_A = 6
    
      precedence:
      
        tt > U11 > plus > U21 > mark# = active# > mark = active > and > |0| > s = isNat
      
      partial status:
    
        pi(mark#) = []
        pi(U11) = [2]
        pi(active#) = []
        pi(mark) = [1]
        pi(plus) = []
        pi(s) = []
        pi(U21) = [2]
        pi(and) = []
        pi(isNat) = []
        pi(tt) = []
        pi(active) = [1]
        pi(|0|) = []
    
    2. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          mark#_A(x1) = 61
          U11_A(x1,x2) = 0
          active#_A(x1) = 61
          mark_A(x1) = 59
          plus_A(x1,x2) = 0
          s_A(x1) = 0
          U21_A(x1,x2,x3) = 0
          and_A(x1,x2) = 0
          isNat_A(x1) = 0
          tt_A = 0
          active_A(x1) = x1 + 59
          |0|_A = 0
    
      precedence:
      
        U11 = mark = active = |0| > U21 > plus > mark# = active# = s = isNat > and = tt
      
      partial status:
    
        pi(mark#) = []
        pi(U11) = []
        pi(active#) = []
        pi(mark) = []
        pi(plus) = []
        pi(s) = []
        pi(U21) = []
        pi(and) = []
        pi(isNat) = []
        pi(tt) = []
        pi(active) = []
        pi(|0|) = []
    

The next rules are strictly ordered:

  p5

We remove them from the problem.

-- SCC decomposition.

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

p1: mark#(U11(X1,X2)) -> active#(U11(mark(X1),X2))
p2: active#(plus(N,s(M))) -> mark#(U21(and(isNat(M),isNat(N)),M,N))
p3: mark#(isNat(X)) -> active#(isNat(X))
p4: active#(isNat(s(V1))) -> mark#(isNat(V1))
p5: mark#(and(X1,X2)) -> active#(and(mark(X1),X2))
p6: active#(and(tt(),X)) -> mark#(X)
p7: mark#(plus(X1,X2)) -> mark#(X1)
p8: mark#(plus(X1,X2)) -> active#(plus(mark(X1),mark(X2)))
p9: active#(U21(tt(),M,N)) -> mark#(s(plus(N,M)))
p10: mark#(s(X)) -> mark#(X)
p11: mark#(s(X)) -> active#(s(mark(X)))
p12: mark#(U21(X1,X2,X3)) -> mark#(X1)
p13: mark#(U21(X1,X2,X3)) -> active#(U21(mark(X1),X2,X3))
p14: mark#(U11(X1,X2)) -> mark#(X1)

and R consists of:

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

The estimated dependency graph contains the following SCCs:

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


-- Reduction pair.

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

p1: mark#(U11(X1,X2)) -> active#(U11(mark(X1),X2))
p2: active#(U21(tt(),M,N)) -> mark#(s(plus(N,M)))
p3: mark#(U11(X1,X2)) -> mark#(X1)
p4: mark#(U21(X1,X2,X3)) -> active#(U21(mark(X1),X2,X3))
p5: active#(and(tt(),X)) -> mark#(X)
p6: mark#(U21(X1,X2,X3)) -> mark#(X1)
p7: mark#(s(X)) -> active#(s(mark(X)))
p8: active#(isNat(s(V1))) -> mark#(isNat(V1))
p9: mark#(s(X)) -> mark#(X)
p10: mark#(plus(X1,X2)) -> active#(plus(mark(X1),mark(X2)))
p11: active#(plus(N,s(M))) -> mark#(U21(and(isNat(M),isNat(N)),M,N))
p12: mark#(plus(X1,X2)) -> mark#(X1)
p13: mark#(and(X1,X2)) -> active#(and(mark(X1),X2))
p14: mark#(isNat(X)) -> active#(isNat(X))

and R consists of:

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

The set of usable rules consists of

  r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r12, r13, r14, r15, r16, r17, r18, r19, r20, r21, r22, r23, r24, r25, r26, r27, r28, r29, r30, r31, r32, r33, r34, r35, r36, r37, r38

Take the reduction pair:

  lexicographic combination of reduction pairs:
  
    1. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          mark#_A(x1) = max{2, x1 - 3}
          U11_A(x1,x2) = max{x1 + 13, x2 + 23}
          active#_A(x1) = max{6, x1 - 3}
          mark_A(x1) = max{9, x1}
          U21_A(x1,x2,x3) = max{58, x1 + 36, x3 + 49}
          tt_A = 16
          s_A(x1) = max{9, x1}
          plus_A(x1,x2) = max{58, x1 + 49}
          and_A(x1,x2) = max{9, x1 - 8, x2}
          isNat_A(x1) = 17
          active_A(x1) = x1
          |0|_A = 8
    
      precedence:
      
        mark# = U11 = active# = mark = U21 = tt = s = plus = and = isNat = active = |0|
      
      partial status:
    
        pi(mark#) = []
        pi(U11) = []
        pi(active#) = []
        pi(mark) = []
        pi(U21) = []
        pi(tt) = []
        pi(s) = []
        pi(plus) = []
        pi(and) = []
        pi(isNat) = []
        pi(active) = []
        pi(|0|) = []
    
    2. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          mark#_A(x1) = 513
          U11_A(x1,x2) = 399
          active#_A(x1) = 513
          mark_A(x1) = 494
          U21_A(x1,x2,x3) = 260
          tt_A = 513
          s_A(x1) = 495
          plus_A(x1,x2) = 106
          and_A(x1,x2) = 513
          isNat_A(x1) = 504
          active_A(x1) = 494
          |0|_A = 0
    
      precedence:
      
        tt = s = and > mark = plus = active = |0| > isNat > mark# = U11 = active# = U21
      
      partial status:
    
        pi(mark#) = []
        pi(U11) = []
        pi(active#) = []
        pi(mark) = []
        pi(U21) = []
        pi(tt) = []
        pi(s) = []
        pi(plus) = []
        pi(and) = []
        pi(isNat) = []
        pi(active) = []
        pi(|0|) = []
    

The next rules are strictly ordered:

  p6, p12

We remove them from the problem.

-- SCC decomposition.

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

p1: mark#(U11(X1,X2)) -> active#(U11(mark(X1),X2))
p2: active#(U21(tt(),M,N)) -> mark#(s(plus(N,M)))
p3: mark#(U11(X1,X2)) -> mark#(X1)
p4: mark#(U21(X1,X2,X3)) -> active#(U21(mark(X1),X2,X3))
p5: active#(and(tt(),X)) -> mark#(X)
p6: mark#(s(X)) -> active#(s(mark(X)))
p7: active#(isNat(s(V1))) -> mark#(isNat(V1))
p8: mark#(s(X)) -> mark#(X)
p9: mark#(plus(X1,X2)) -> active#(plus(mark(X1),mark(X2)))
p10: active#(plus(N,s(M))) -> mark#(U21(and(isNat(M),isNat(N)),M,N))
p11: mark#(and(X1,X2)) -> active#(and(mark(X1),X2))
p12: mark#(isNat(X)) -> active#(isNat(X))

and R consists of:

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

The estimated dependency graph contains the following SCCs:

  {p1, p2, p3, p4, p5, p6, p7, p8, p9, p10, p11, p12}


-- Reduction pair.

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

p1: mark#(U11(X1,X2)) -> active#(U11(mark(X1),X2))
p2: active#(plus(N,s(M))) -> mark#(U21(and(isNat(M),isNat(N)),M,N))
p3: mark#(isNat(X)) -> active#(isNat(X))
p4: active#(isNat(s(V1))) -> mark#(isNat(V1))
p5: mark#(and(X1,X2)) -> active#(and(mark(X1),X2))
p6: active#(and(tt(),X)) -> mark#(X)
p7: mark#(plus(X1,X2)) -> active#(plus(mark(X1),mark(X2)))
p8: active#(U21(tt(),M,N)) -> mark#(s(plus(N,M)))
p9: mark#(s(X)) -> mark#(X)
p10: mark#(s(X)) -> active#(s(mark(X)))
p11: mark#(U21(X1,X2,X3)) -> active#(U21(mark(X1),X2,X3))
p12: mark#(U11(X1,X2)) -> mark#(X1)

and R consists of:

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

The set of usable rules consists of

  r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r12, r13, r14, r15, r16, r17, r18, r19, r20, r21, r22, r23, r24, r25, r26, r27, r28, r29, r30, r31, r32, r33, r34, r35, r36, r37, r38

Take the reduction pair:

  lexicographic combination of reduction pairs:
  
    1. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          mark#_A(x1) = max{16, x1 - 39}
          U11_A(x1,x2) = max{x1 + 85, x2 + 124}
          active#_A(x1) = max{2, x1 - 39}
          mark_A(x1) = x1
          plus_A(x1,x2) = max{x1 + 142, x2 + 30}
          s_A(x1) = max{23, x1}
          U21_A(x1,x2,x3) = max{x2 + 30, x3 + 142}
          and_A(x1,x2) = max{42, x1 - 84, x2 + 4}
          isNat_A(x1) = max{56, x1 + 31}
          tt_A = 140
          active_A(x1) = max{23, x1}
          |0|_A = 110
    
      precedence:
      
        mark = plus = s = and = active = |0| > U21 > mark# = U11 = active# = isNat = tt
      
      partial status:
    
        pi(mark#) = []
        pi(U11) = [2]
        pi(active#) = []
        pi(mark) = []
        pi(plus) = []
        pi(s) = []
        pi(U21) = [2]
        pi(and) = []
        pi(isNat) = []
        pi(tt) = []
        pi(active) = []
        pi(|0|) = []
    
    2. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          mark#_A(x1) = 173
          U11_A(x1,x2) = 56
          active#_A(x1) = 173
          mark_A(x1) = 112
          plus_A(x1,x2) = 56
          s_A(x1) = 157
          U21_A(x1,x2,x3) = 172
          and_A(x1,x2) = 56
          isNat_A(x1) = 393
          tt_A = 2
          active_A(x1) = 112
          |0|_A = 22
    
      precedence:
      
        mark# = active# > U21 > mark = plus = s = and = isNat = active = |0| > U11 = tt
      
      partial status:
    
        pi(mark#) = []
        pi(U11) = []
        pi(active#) = []
        pi(mark) = []
        pi(plus) = []
        pi(s) = []
        pi(U21) = []
        pi(and) = []
        pi(isNat) = []
        pi(tt) = []
        pi(active) = []
        pi(|0|) = []
    

The next rules are strictly ordered:

  p12

We remove them from the problem.

-- SCC decomposition.

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

p1: mark#(U11(X1,X2)) -> active#(U11(mark(X1),X2))
p2: active#(plus(N,s(M))) -> mark#(U21(and(isNat(M),isNat(N)),M,N))
p3: mark#(isNat(X)) -> active#(isNat(X))
p4: active#(isNat(s(V1))) -> mark#(isNat(V1))
p5: mark#(and(X1,X2)) -> active#(and(mark(X1),X2))
p6: active#(and(tt(),X)) -> mark#(X)
p7: mark#(plus(X1,X2)) -> active#(plus(mark(X1),mark(X2)))
p8: active#(U21(tt(),M,N)) -> mark#(s(plus(N,M)))
p9: mark#(s(X)) -> mark#(X)
p10: mark#(s(X)) -> active#(s(mark(X)))
p11: mark#(U21(X1,X2,X3)) -> active#(U21(mark(X1),X2,X3))

and R consists of:

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

The estimated dependency graph contains the following SCCs:

  {p1, p2, p3, p4, p5, p6, p7, p8, p9, p10, p11}


-- Reduction pair.

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

p1: mark#(U11(X1,X2)) -> active#(U11(mark(X1),X2))
p2: active#(U21(tt(),M,N)) -> mark#(s(plus(N,M)))
p3: mark#(U21(X1,X2,X3)) -> active#(U21(mark(X1),X2,X3))
p4: active#(and(tt(),X)) -> mark#(X)
p5: mark#(s(X)) -> active#(s(mark(X)))
p6: active#(isNat(s(V1))) -> mark#(isNat(V1))
p7: mark#(s(X)) -> mark#(X)
p8: mark#(plus(X1,X2)) -> active#(plus(mark(X1),mark(X2)))
p9: active#(plus(N,s(M))) -> mark#(U21(and(isNat(M),isNat(N)),M,N))
p10: mark#(and(X1,X2)) -> active#(and(mark(X1),X2))
p11: mark#(isNat(X)) -> active#(isNat(X))

and R consists of:

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

The set of usable rules consists of

  r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r12, r13, r14, r15, r16, r17, r18, r19, r20, r21, r22, r23, r24, r25, r26, r27, r28, r29, r30, r31, r32, r33, r34, r35, r36, r37, r38

Take the reduction pair:

  lexicographic combination of reduction pairs:
  
    1. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          mark#_A(x1) = max{3, x1 + 2}
          U11_A(x1,x2) = max{57, x1 + 21, x2 + 1}
          active#_A(x1) = max{4, x1 + 2}
          mark_A(x1) = max{22, x1}
          U21_A(x1,x2,x3) = max{58, x3 + 36}
          tt_A = 13
          s_A(x1) = max{25, x1}
          plus_A(x1,x2) = max{58, x1 + 36}
          and_A(x1,x2) = max{6, x1 - 22, x2 + 5}
          isNat_A(x1) = 13
          active_A(x1) = max{22, x1}
          |0|_A = 91
    
      precedence:
      
        U21 = tt = s = plus > and > mark# = active# = isNat = |0| > U11 > mark = active
      
      partial status:
    
        pi(mark#) = [1]
        pi(U11) = []
        pi(active#) = [1]
        pi(mark) = []
        pi(U21) = []
        pi(tt) = []
        pi(s) = []
        pi(plus) = []
        pi(and) = []
        pi(isNat) = []
        pi(active) = []
        pi(|0|) = []
    
    2. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          mark#_A(x1) = 193
          U11_A(x1,x2) = 357
          active#_A(x1) = 193
          mark_A(x1) = 206
          U21_A(x1,x2,x3) = 170
          tt_A = 370
          s_A(x1) = 146
          plus_A(x1,x2) = 193
          and_A(x1,x2) = 166
          isNat_A(x1) = 191
          active_A(x1) = 206
          |0|_A = 266
    
      precedence:
      
        U11 = U21 = tt > mark# = active# = isNat > s = plus = |0| > and > mark = active
      
      partial status:
    
        pi(mark#) = []
        pi(U11) = []
        pi(active#) = []
        pi(mark) = []
        pi(U21) = []
        pi(tt) = []
        pi(s) = []
        pi(plus) = []
        pi(and) = []
        pi(isNat) = []
        pi(active) = []
        pi(|0|) = []
    

The next rules are strictly ordered:

  p4

We remove them from the problem.

-- SCC decomposition.

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

p1: mark#(U11(X1,X2)) -> active#(U11(mark(X1),X2))
p2: active#(U21(tt(),M,N)) -> mark#(s(plus(N,M)))
p3: mark#(U21(X1,X2,X3)) -> active#(U21(mark(X1),X2,X3))
p4: mark#(s(X)) -> active#(s(mark(X)))
p5: active#(isNat(s(V1))) -> mark#(isNat(V1))
p6: mark#(s(X)) -> mark#(X)
p7: mark#(plus(X1,X2)) -> active#(plus(mark(X1),mark(X2)))
p8: active#(plus(N,s(M))) -> mark#(U21(and(isNat(M),isNat(N)),M,N))
p9: mark#(and(X1,X2)) -> active#(and(mark(X1),X2))
p10: mark#(isNat(X)) -> active#(isNat(X))

and R consists of:

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

The estimated dependency graph contains the following SCCs:

  {p1, p2, p3, p4, p5, p6, p7, p8, p9, p10}


-- Reduction pair.

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

p1: mark#(U11(X1,X2)) -> active#(U11(mark(X1),X2))
p2: active#(plus(N,s(M))) -> mark#(U21(and(isNat(M),isNat(N)),M,N))
p3: mark#(isNat(X)) -> active#(isNat(X))
p4: active#(isNat(s(V1))) -> mark#(isNat(V1))
p5: mark#(and(X1,X2)) -> active#(and(mark(X1),X2))
p6: active#(U21(tt(),M,N)) -> mark#(s(plus(N,M)))
p7: mark#(plus(X1,X2)) -> active#(plus(mark(X1),mark(X2)))
p8: mark#(s(X)) -> mark#(X)
p9: mark#(s(X)) -> active#(s(mark(X)))
p10: mark#(U21(X1,X2,X3)) -> active#(U21(mark(X1),X2,X3))

and R consists of:

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

The set of usable rules consists of

  r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r12, r13, r14, r15, r16, r17, r18, r19, r20, r21, r22, r23, r24, r25, r26, r27, r28, r29, r30, r31, r32, r33, r34, r35, r36, r37, r38

Take the reduction pair:

  lexicographic combination of reduction pairs:
  
    1. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          mark#_A(x1) = x1
          U11_A(x1,x2) = max{15, x2 + 6}
          active#_A(x1) = x1
          mark_A(x1) = max{3, x1}
          plus_A(x1,x2) = max{22, x1 + 14}
          s_A(x1) = max{16, x1}
          U21_A(x1,x2,x3) = max{22, x3 + 14}
          and_A(x1,x2) = max{22, x1, x2}
          isNat_A(x1) = 22
          tt_A = 17
          active_A(x1) = max{15, x1}
          |0|_A = 18
    
      precedence:
      
        mark# = U11 = active# = mark = plus = s = U21 = and = isNat = tt = active = |0|
      
      partial status:
    
        pi(mark#) = []
        pi(U11) = []
        pi(active#) = []
        pi(mark) = []
        pi(plus) = []
        pi(s) = []
        pi(U21) = []
        pi(and) = []
        pi(isNat) = []
        pi(tt) = []
        pi(active) = []
        pi(|0|) = []
    
    2. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          mark#_A(x1) = 100
          U11_A(x1,x2) = 53
          active#_A(x1) = max{54, x1 - 46}
          mark_A(x1) = 0
          plus_A(x1,x2) = 146
          s_A(x1) = 146
          U21_A(x1,x2,x3) = 146
          and_A(x1,x2) = 127
          isNat_A(x1) = 146
          tt_A = 1
          active_A(x1) = 0
          |0|_A = 2
    
      precedence:
      
        and > mark = plus = s = isNat = active > mark# = active# > U11 = U21 = tt = |0|
      
      partial status:
    
        pi(mark#) = []
        pi(U11) = []
        pi(active#) = []
        pi(mark) = []
        pi(plus) = []
        pi(s) = []
        pi(U21) = []
        pi(and) = []
        pi(isNat) = []
        pi(tt) = []
        pi(active) = []
        pi(|0|) = []
    

The next rules are strictly ordered:

  p1, p5

We remove them from the problem.

-- SCC decomposition.

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

p1: active#(plus(N,s(M))) -> mark#(U21(and(isNat(M),isNat(N)),M,N))
p2: mark#(isNat(X)) -> active#(isNat(X))
p3: active#(isNat(s(V1))) -> mark#(isNat(V1))
p4: active#(U21(tt(),M,N)) -> mark#(s(plus(N,M)))
p5: mark#(plus(X1,X2)) -> active#(plus(mark(X1),mark(X2)))
p6: mark#(s(X)) -> mark#(X)
p7: mark#(s(X)) -> active#(s(mark(X)))
p8: mark#(U21(X1,X2,X3)) -> active#(U21(mark(X1),X2,X3))

and R consists of:

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

The estimated dependency graph contains the following SCCs:

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


-- Reduction pair.

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

p1: active#(plus(N,s(M))) -> mark#(U21(and(isNat(M),isNat(N)),M,N))
p2: mark#(U21(X1,X2,X3)) -> active#(U21(mark(X1),X2,X3))
p3: active#(U21(tt(),M,N)) -> mark#(s(plus(N,M)))
p4: mark#(s(X)) -> active#(s(mark(X)))
p5: active#(isNat(s(V1))) -> mark#(isNat(V1))
p6: mark#(s(X)) -> mark#(X)
p7: mark#(plus(X1,X2)) -> active#(plus(mark(X1),mark(X2)))
p8: mark#(isNat(X)) -> active#(isNat(X))

and R consists of:

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

The set of usable rules consists of

  r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r12, r13, r14, r15, r16, r17, r18, r19, r20, r21, r22, r23, r24, r25, r26, r27, r28, r29, r30, r31, r32, r33, r34, r35, r36, r37, r38

Take the reduction pair:

  lexicographic combination of reduction pairs:
  
    1. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          active#_A(x1) = x1 + 5
          plus_A(x1,x2) = 2
          s_A(x1) = 0
          mark#_A(x1) = 7
          U21_A(x1,x2,x3) = 2
          and_A(x1,x2) = 36
          isNat_A(x1) = 2
          mark_A(x1) = 61
          tt_A = 36
          active_A(x1) = max{61, x1 + 25}
          U11_A(x1,x2) = 26
          |0|_A = 11
    
      precedence:
      
        active# = plus = s = mark# = U21 = and = isNat = mark = tt = active = U11 = |0|
      
      partial status:
    
        pi(active#) = []
        pi(plus) = []
        pi(s) = []
        pi(mark#) = []
        pi(U21) = []
        pi(and) = []
        pi(isNat) = []
        pi(mark) = []
        pi(tt) = []
        pi(active) = []
        pi(U11) = []
        pi(|0|) = []
    
    2. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          active#_A(x1) = max{457, x1 + 73}
          plus_A(x1,x2) = 385
          s_A(x1) = 402
          mark#_A(x1) = 458
          U21_A(x1,x2,x3) = 385
          and_A(x1,x2) = 317
          isNat_A(x1) = 385
          mark_A(x1) = 366
          tt_A = 464
          active_A(x1) = 366
          U11_A(x1,x2) = 268
          |0|_A = 0
    
      precedence:
      
        plus > active# = mark# = U11 = |0| > s > U21 = and = isNat = mark = tt = active
      
      partial status:
    
        pi(active#) = []
        pi(plus) = []
        pi(s) = []
        pi(mark#) = []
        pi(U21) = []
        pi(and) = []
        pi(isNat) = []
        pi(mark) = []
        pi(tt) = []
        pi(active) = []
        pi(U11) = []
        pi(|0|) = []
    

The next rules are strictly ordered:

  p4

We remove them from the problem.

-- SCC decomposition.

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

p1: active#(plus(N,s(M))) -> mark#(U21(and(isNat(M),isNat(N)),M,N))
p2: mark#(U21(X1,X2,X3)) -> active#(U21(mark(X1),X2,X3))
p3: active#(U21(tt(),M,N)) -> mark#(s(plus(N,M)))
p4: active#(isNat(s(V1))) -> mark#(isNat(V1))
p5: mark#(s(X)) -> mark#(X)
p6: mark#(plus(X1,X2)) -> active#(plus(mark(X1),mark(X2)))
p7: mark#(isNat(X)) -> active#(isNat(X))

and R consists of:

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

The estimated dependency graph contains the following SCCs:

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


-- Reduction pair.

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

p1: active#(plus(N,s(M))) -> mark#(U21(and(isNat(M),isNat(N)),M,N))
p2: mark#(isNat(X)) -> active#(isNat(X))
p3: active#(isNat(s(V1))) -> mark#(isNat(V1))
p4: mark#(plus(X1,X2)) -> active#(plus(mark(X1),mark(X2)))
p5: active#(U21(tt(),M,N)) -> mark#(s(plus(N,M)))
p6: mark#(s(X)) -> mark#(X)
p7: mark#(U21(X1,X2,X3)) -> active#(U21(mark(X1),X2,X3))

and R consists of:

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

The set of usable rules consists of

  r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r12, r13, r14, r15, r16, r17, r18, r19, r20, r21, r22, r23, r24, r25, r26, r27, r28, r29, r30, r31, r32, r33, r34, r35, r36, r37, r38

Take the reduction pair:

  lexicographic combination of reduction pairs:
  
    1. weighted path order
    
      base order:
    
        matrix interpretations:
        
          carrier: N^2
          order: lexicographic order
          interpretations:
            active#_A(x1) = ((1,0),(0,0)) x1 + (2,7)
            plus_A(x1,x2) = ((1,0),(0,0)) x1 + ((1,0),(0,0)) x2 + (2,0)
            s_A(x1) = ((1,0),(0,0)) x1 + (1,4)
            mark#_A(x1) = ((1,0),(0,0)) x1 + (2,7)
            U21_A(x1,x2,x3) = ((1,0),(0,0)) x2 + ((1,0),(1,0)) x3 + (3,3)
            and_A(x1,x2) = ((1,0),(0,0)) x2 + (0,5)
            isNat_A(x1) = (6,6)
            mark_A(x1) = ((1,0),(0,0)) x1 + (0,2)
            tt_A() = (4,5)
            active_A(x1) = ((1,0),(0,0)) x1 + (0,2)
            U11_A(x1,x2) = ((1,0),(0,0)) x2 + (4,1)
            |0|_A() = (3,3)
    
      precedence:
      
        active# = plus = mark# = U21 = and = isNat = mark = tt = active > s = U11 = |0|
      
      partial status:
    
        pi(active#) = []
        pi(plus) = []
        pi(s) = []
        pi(mark#) = []
        pi(U21) = []
        pi(and) = []
        pi(isNat) = []
        pi(mark) = []
        pi(tt) = []
        pi(active) = []
        pi(U11) = []
        pi(|0|) = []
    
    2. weighted path order
    
      base order:
    
        matrix interpretations:
        
          carrier: N^2
          order: lexicographic order
          interpretations:
            active#_A(x1) = (0,0)
            plus_A(x1,x2) = (1,0)
            s_A(x1) = (0,0)
            mark#_A(x1) = (0,0)
            U21_A(x1,x2,x3) = (1,2)
            and_A(x1,x2) = (0,0)
            isNat_A(x1) = (0,0)
            mark_A(x1) = (2,1)
            tt_A() = (3,2)
            active_A(x1) = (2,1)
            U11_A(x1,x2) = (0,0)
            |0|_A() = (4,0)
    
      precedence:
      
        active# = plus = mark# = U21 = and = isNat = mark = tt = active = |0| > s = U11
      
      partial status:
    
        pi(active#) = []
        pi(plus) = []
        pi(s) = []
        pi(mark#) = []
        pi(U21) = []
        pi(and) = []
        pi(isNat) = []
        pi(mark) = []
        pi(tt) = []
        pi(active) = []
        pi(U11) = []
        pi(|0|) = []
    

The next rules are strictly ordered:

  p6

We remove them from the problem.

-- SCC decomposition.

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

p1: active#(plus(N,s(M))) -> mark#(U21(and(isNat(M),isNat(N)),M,N))
p2: mark#(isNat(X)) -> active#(isNat(X))
p3: active#(isNat(s(V1))) -> mark#(isNat(V1))
p4: mark#(plus(X1,X2)) -> active#(plus(mark(X1),mark(X2)))
p5: active#(U21(tt(),M,N)) -> mark#(s(plus(N,M)))
p6: mark#(U21(X1,X2,X3)) -> active#(U21(mark(X1),X2,X3))

and R consists of:

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

The estimated dependency graph contains the following SCCs:

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


-- Reduction pair.

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

p1: active#(plus(N,s(M))) -> mark#(U21(and(isNat(M),isNat(N)),M,N))
p2: mark#(U21(X1,X2,X3)) -> active#(U21(mark(X1),X2,X3))
p3: active#(U21(tt(),M,N)) -> mark#(s(plus(N,M)))
p4: mark#(plus(X1,X2)) -> active#(plus(mark(X1),mark(X2)))
p5: active#(isNat(s(V1))) -> mark#(isNat(V1))
p6: mark#(isNat(X)) -> active#(isNat(X))

and R consists of:

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

The set of usable rules consists of

  r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r12, r13, r14, r15, r16, r17, r18, r19, r20, r21, r22, r23, r24, r25, r26, r27, r28, r29, r30, r31, r32, r33, r34, r35, r36, r37, r38

Take the reduction pair:

  lexicographic combination of reduction pairs:
  
    1. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          active#_A(x1) = x1 + 11
          plus_A(x1,x2) = max{x1 + 6, x2 + 6}
          s_A(x1) = x1
          mark#_A(x1) = x1 + 11
          U21_A(x1,x2,x3) = max{x1 - 2, x2 + 6, x3 + 6}
          and_A(x1,x2) = max{x1 + 4, x2 + 6}
          isNat_A(x1) = x1 + 1
          mark_A(x1) = x1
          tt_A = 1
          active_A(x1) = x1
          U11_A(x1,x2) = max{x1 + 4, x2 + 4}
          |0|_A = 0
    
      precedence:
      
        active# = plus = s = mark# = U21 = and = isNat = mark = tt = active = U11 = |0|
      
      partial status:
    
        pi(active#) = []
        pi(plus) = []
        pi(s) = []
        pi(mark#) = []
        pi(U21) = []
        pi(and) = []
        pi(isNat) = []
        pi(mark) = []
        pi(tt) = []
        pi(active) = []
        pi(U11) = []
        pi(|0|) = []
    
    2. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          active#_A(x1) = 69
          plus_A(x1,x2) = 124
          s_A(x1) = max{50, x1 - 47}
          mark#_A(x1) = max{8, x1 - 8}
          U21_A(x1,x2,x3) = 77
          and_A(x1,x2) = 79
          isNat_A(x1) = 77
          mark_A(x1) = max{119, x1 + 40}
          tt_A = 79
          active_A(x1) = max{119, x1}
          U11_A(x1,x2) = 83
          |0|_A = 80
    
      precedence:
      
        plus > active# = mark# = U21 = |0| > tt > isNat > and = mark = active = U11 > s
      
      partial status:
    
        pi(active#) = []
        pi(plus) = []
        pi(s) = []
        pi(mark#) = []
        pi(U21) = []
        pi(and) = []
        pi(isNat) = []
        pi(mark) = []
        pi(tt) = []
        pi(active) = []
        pi(U11) = []
        pi(|0|) = []
    

The next rules are strictly ordered:

  p4

We remove them from the problem.

-- SCC decomposition.

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

p1: active#(plus(N,s(M))) -> mark#(U21(and(isNat(M),isNat(N)),M,N))
p2: mark#(U21(X1,X2,X3)) -> active#(U21(mark(X1),X2,X3))
p3: active#(U21(tt(),M,N)) -> mark#(s(plus(N,M)))
p4: active#(isNat(s(V1))) -> mark#(isNat(V1))
p5: mark#(isNat(X)) -> active#(isNat(X))

and R consists of:

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

The estimated dependency graph contains the following SCCs:

  {p1, p2, p3, p4, p5}


-- Reduction pair.

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

p1: active#(plus(N,s(M))) -> mark#(U21(and(isNat(M),isNat(N)),M,N))
p2: mark#(isNat(X)) -> active#(isNat(X))
p3: active#(isNat(s(V1))) -> mark#(isNat(V1))
p4: mark#(U21(X1,X2,X3)) -> active#(U21(mark(X1),X2,X3))
p5: active#(U21(tt(),M,N)) -> mark#(s(plus(N,M)))

and R consists of:

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

The set of usable rules consists of

  r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r12, r13, r14, r15, r16, r17, r18, r19, r20, r21, r22, r23, r24, r25, r26, r27, r28, r29, r30, r31, r32, r33, r34, r35, r36, r37, r38

Take the reduction pair:

  lexicographic combination of reduction pairs:
  
    1. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          active#_A(x1) = max{5, x1 - 3}
          plus_A(x1,x2) = 11
          s_A(x1) = 9
          mark#_A(x1) = max{7, x1 - 3}
          U21_A(x1,x2,x3) = 11
          and_A(x1,x2) = 11
          isNat_A(x1) = 11
          mark_A(x1) = 31
          tt_A = 2
          active_A(x1) = x1 + 20
          U11_A(x1,x2) = 11
          |0|_A = 0
    
      precedence:
      
        s = and > plus = U21 = mark = tt = active > active# = mark# = isNat = U11 = |0|
      
      partial status:
    
        pi(active#) = []
        pi(plus) = []
        pi(s) = []
        pi(mark#) = []
        pi(U21) = []
        pi(and) = []
        pi(isNat) = []
        pi(mark) = []
        pi(tt) = []
        pi(active) = []
        pi(U11) = []
        pi(|0|) = []
    
    2. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          active#_A(x1) = 189
          plus_A(x1,x2) = 205
          s_A(x1) = 203
          mark#_A(x1) = 189
          U21_A(x1,x2,x3) = 203
          and_A(x1,x2) = 190
          isNat_A(x1) = 285
          mark_A(x1) = 202
          tt_A = 335
          active_A(x1) = 202
          U11_A(x1,x2) = 181
          |0|_A = 147
    
      precedence:
      
        active# = plus = s = mark# = U21 = and = isNat = mark = tt = active = U11 = |0|
      
      partial status:
    
        pi(active#) = []
        pi(plus) = []
        pi(s) = []
        pi(mark#) = []
        pi(U21) = []
        pi(and) = []
        pi(isNat) = []
        pi(mark) = []
        pi(tt) = []
        pi(active) = []
        pi(U11) = []
        pi(|0|) = []
    

The next rules are strictly ordered:

  p5

We remove them from the problem.

-- SCC decomposition.

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

p1: active#(plus(N,s(M))) -> mark#(U21(and(isNat(M),isNat(N)),M,N))
p2: mark#(isNat(X)) -> active#(isNat(X))
p3: active#(isNat(s(V1))) -> mark#(isNat(V1))
p4: mark#(U21(X1,X2,X3)) -> active#(U21(mark(X1),X2,X3))

and R consists of:

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

The estimated dependency graph contains the following SCCs:

  {p1, p2, p3, p4}


-- Reduction pair.

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

p1: active#(plus(N,s(M))) -> mark#(U21(and(isNat(M),isNat(N)),M,N))
p2: mark#(U21(X1,X2,X3)) -> active#(U21(mark(X1),X2,X3))
p3: active#(isNat(s(V1))) -> mark#(isNat(V1))
p4: mark#(isNat(X)) -> active#(isNat(X))

and R consists of:

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

The set of usable rules consists of

  r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r12, r13, r14, r15, r16, r17, r18, r19, r20, r21, r22, r23, r24, r25, r26, r27, r28, r29, r30, r31, r32, r33, r34, r35, r36, r37, r38

Take the reduction pair:

  lexicographic combination of reduction pairs:
  
    1. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          active#_A(x1) = max{157, x1 + 117}
          plus_A(x1,x2) = max{41, x1 + 11, x2 + 11}
          s_A(x1) = 35
          mark#_A(x1) = max{157, x1 + 87}
          U21_A(x1,x2,x3) = 40
          and_A(x1,x2) = max{30, x2 + 4}
          isNat_A(x1) = 26
          mark_A(x1) = max{34, x1 + 4}
          active_A(x1) = max{34, x1}
          U11_A(x1,x2) = max{31, x2 + 4}
          tt_A = 30
          |0|_A = 35
    
      precedence:
      
        plus = s = U21 = and = isNat = mark = active = tt = |0| > active# = mark# = U11
      
      partial status:
    
        pi(active#) = [1]
        pi(plus) = []
        pi(s) = []
        pi(mark#) = [1]
        pi(U21) = []
        pi(and) = []
        pi(isNat) = []
        pi(mark) = []
        pi(active) = []
        pi(U11) = [2]
        pi(tt) = []
        pi(|0|) = []
    
    2. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          active#_A(x1) = max{76, x1 - 30}
          plus_A(x1,x2) = 124
          s_A(x1) = 204
          mark#_A(x1) = max{61, x1 - 16}
          U21_A(x1,x2,x3) = 93
          and_A(x1,x2) = 91
          isNat_A(x1) = 92
          mark_A(x1) = 91
          active_A(x1) = 91
          U11_A(x1,x2) = 1
          tt_A = 188
          |0|_A = 19
    
      precedence:
      
        s = tt > isNat > and > U21 = mark = active = U11 = |0| > active# = mark# > plus
      
      partial status:
    
        pi(active#) = []
        pi(plus) = []
        pi(s) = []
        pi(mark#) = []
        pi(U21) = []
        pi(and) = []
        pi(isNat) = []
        pi(mark) = []
        pi(active) = []
        pi(U11) = []
        pi(tt) = []
        pi(|0|) = []
    

The next rules are strictly ordered:

  p1, p2

We remove them from the problem.

-- SCC decomposition.

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

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

and R consists of:

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

The estimated dependency graph contains the following SCCs:

  {p1, p2}


-- Reduction pair.

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

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

and R consists of:

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

The set of usable rules consists of

  r37, r38

Take the reduction pair:

  lexicographic combination of reduction pairs:
  
    1. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          active#_A(x1) = max{13, x1 + 3}
          isNat_A(x1) = max{12, x1 + 7}
          s_A(x1) = max{6, x1 + 3}
          mark#_A(x1) = max{9, x1 + 4}
          mark_A(x1) = max{7, x1 + 6}
          active_A(x1) = max{14, x1 + 13}
    
      precedence:
      
        active# = s = mark# = mark = active > isNat
      
      partial status:
    
        pi(active#) = [1]
        pi(isNat) = [1]
        pi(s) = [1]
        pi(mark#) = [1]
        pi(mark) = [1]
        pi(active) = [1]
    
    2. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          active#_A(x1) = max{8, x1 + 2}
          isNat_A(x1) = max{5, x1 + 1}
          s_A(x1) = x1 + 6
          mark#_A(x1) = max{4, x1 + 3}
          mark_A(x1) = x1
          active_A(x1) = x1
    
      precedence:
      
        active# = isNat = s = mark# = mark = active
      
      partial status:
    
        pi(active#) = []
        pi(isNat) = [1]
        pi(s) = [1]
        pi(mark#) = [1]
        pi(mark) = [1]
        pi(active) = [1]
    

The next rules are strictly ordered:

  p1, p2

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

-- Reduction pair.

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

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

and R consists of:

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

The set of usable rules consists of

  (no rules)

Take the monotone reduction pair:

  lexicographic combination of reduction pairs:
  
    1. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          s#_A(x1) = max{6, x1 + 4}
          mark_A(x1) = max{4, x1 + 3}
          active_A(x1) = max{2, x1 + 1}
    
      precedence:
      
        s# = mark = active
      
      partial status:
    
        pi(s#) = [1]
        pi(mark) = [1]
        pi(active) = [1]
    
    2. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          s#_A(x1) = x1 + 1
          mark_A(x1) = x1
          active_A(x1) = x1
    
      precedence:
      
        s# = mark = active
      
      partial status:
    
        pi(s#) = [1]
        pi(mark) = [1]
        pi(active) = [1]
    

The next rules are strictly ordered:

  p1, p2

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

-- Reduction pair.

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

p1: plus#(mark(X1),X2) -> plus#(X1,X2)
p2: plus#(X1,active(X2)) -> plus#(X1,X2)
p3: plus#(active(X1),X2) -> plus#(X1,X2)
p4: plus#(X1,mark(X2)) -> plus#(X1,X2)

and R consists of:

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

The set of usable rules consists of

  (no rules)

Take the monotone reduction pair:

  lexicographic combination of reduction pairs:
  
    1. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          plus#_A(x1,x2) = max{4, x1 + 1, x2 + 3}
          mark_A(x1) = max{3, x1 + 2}
          active_A(x1) = max{1, x1}
    
      precedence:
      
        plus# = mark = active
      
      partial status:
    
        pi(plus#) = [1, 2]
        pi(mark) = [1]
        pi(active) = [1]
    
    2. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          plus#_A(x1,x2) = max{x1 + 1, x2 + 1}
          mark_A(x1) = x1
          active_A(x1) = x1
    
      precedence:
      
        plus# = mark = active
      
      partial status:
    
        pi(plus#) = [1, 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: and#(mark(X1),X2) -> and#(X1,X2)
p2: and#(X1,active(X2)) -> and#(X1,X2)
p3: and#(active(X1),X2) -> and#(X1,X2)
p4: and#(X1,mark(X2)) -> and#(X1,X2)

and R consists of:

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

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  lexicographic combination of reduction pairs:
  
    1. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          and#_A(x1,x2) = max{2, x1 + 1, x2 + 1}
          mark_A(x1) = max{1, x1}
          active_A(x1) = max{1, x1}
    
      precedence:
      
        and# = mark = active
      
      partial status:
    
        pi(and#) = [1, 2]
        pi(mark) = [1]
        pi(active) = [1]
    
    2. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          and#_A(x1,x2) = max{x1 + 1, x2 - 1}
          mark_A(x1) = x1
          active_A(x1) = x1
    
      precedence:
      
        and# = mark = active
      
      partial status:
    
        pi(and#) = [1]
        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: isNat#(mark(X)) -> isNat#(X)
p2: isNat#(active(X)) -> isNat#(X)

and R consists of:

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

The set of usable rules consists of

  (no rules)

Take the monotone reduction pair:

  lexicographic combination of reduction pairs:
  
    1. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          isNat#_A(x1) = x1 + 2
          mark_A(x1) = x1
          active_A(x1) = x1 + 2
    
      precedence:
      
        mark > active > isNat#
      
      partial status:
    
        pi(isNat#) = [1]
        pi(mark) = [1]
        pi(active) = [1]
    
    2. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          isNat#_A(x1) = x1 + 1
          mark_A(x1) = x1
          active_A(x1) = x1
    
      precedence:
      
        isNat# = mark = active
      
      partial status:
    
        pi(isNat#) = [1]
        pi(mark) = [1]
        pi(active) = [1]
    

The next rules are strictly ordered:

  p1, p2

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

-- Reduction pair.

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

p1: U11#(mark(X1),X2) -> U11#(X1,X2)
p2: U11#(X1,active(X2)) -> U11#(X1,X2)
p3: U11#(active(X1),X2) -> U11#(X1,X2)
p4: U11#(X1,mark(X2)) -> U11#(X1,X2)

and R consists of:

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

The set of usable rules consists of

  (no rules)

Take the monotone reduction pair:

  lexicographic combination of reduction pairs:
  
    1. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          U11#_A(x1,x2) = max{3, x1 + 1, x2 + 1}
          mark_A(x1) = max{2, x1 + 1}
          active_A(x1) = max{1, x1}
    
      precedence:
      
        U11# = mark = active
      
      partial status:
    
        pi(U11#) = [1, 2]
        pi(mark) = [1]
        pi(active) = [1]
    
    2. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          U11#_A(x1,x2) = max{x1 + 1, x2 + 1}
          mark_A(x1) = x1
          active_A(x1) = x1
    
      precedence:
      
        U11# = mark = active
      
      partial status:
    
        pi(U11#) = [1, 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(X1),X2,X3) -> U21#(X1,X2,X3)
p2: U21#(X1,X2,active(X3)) -> U21#(X1,X2,X3)
p3: U21#(X1,active(X2),X3) -> U21#(X1,X2,X3)
p4: U21#(active(X1),X2,X3) -> U21#(X1,X2,X3)
p5: U21#(X1,X2,mark(X3)) -> U21#(X1,X2,X3)
p6: U21#(X1,mark(X2),X3) -> U21#(X1,X2,X3)

and R consists of:

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

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  lexicographic combination of reduction pairs:
  
    1. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          U21#_A(x1,x2,x3) = max{x1 + 1, x2 + 3, x3 + 1}
          mark_A(x1) = max{1, x1}
          active_A(x1) = max{1, x1}
    
      precedence:
      
        U21# = mark = active
      
      partial status:
    
        pi(U21#) = [1, 2, 3]
        pi(mark) = [1]
        pi(active) = [1]
    
    2. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          U21#_A(x1,x2,x3) = max{0, x1 - 2}
          mark_A(x1) = max{3, x1 + 1}
          active_A(x1) = max{3, x1 + 1}
    
      precedence:
      
        U21# = mark = active
      
      partial status:
    
        pi(U21#) = []
        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.