YES

We show the termination of the TRS R:

  active(U11(tt(),V2)) -> mark(U12(isNat(V2)))
  active(U12(tt())) -> mark(tt())
  active(U21(tt())) -> mark(tt())
  active(U31(tt(),N)) -> mark(N)
  active(U41(tt(),M,N)) -> mark(U42(isNat(N),M,N))
  active(U42(tt(),M,N)) -> mark(s(plus(N,M)))
  active(isNat(|0|())) -> mark(tt())
  active(isNat(plus(V1,V2))) -> mark(U11(isNat(V1),V2))
  active(isNat(s(V1))) -> mark(U21(isNat(V1)))
  active(plus(N,|0|())) -> mark(U31(isNat(N),N))
  active(plus(N,s(M))) -> mark(U41(isNat(M),M,N))
  active(U11(X1,X2)) -> U11(active(X1),X2)
  active(U12(X)) -> U12(active(X))
  active(U21(X)) -> U21(active(X))
  active(U31(X1,X2)) -> U31(active(X1),X2)
  active(U41(X1,X2,X3)) -> U41(active(X1),X2,X3)
  active(U42(X1,X2,X3)) -> U42(active(X1),X2,X3)
  active(s(X)) -> s(active(X))
  active(plus(X1,X2)) -> plus(active(X1),X2)
  active(plus(X1,X2)) -> plus(X1,active(X2))
  U11(mark(X1),X2) -> mark(U11(X1,X2))
  U12(mark(X)) -> mark(U12(X))
  U21(mark(X)) -> mark(U21(X))
  U31(mark(X1),X2) -> mark(U31(X1,X2))
  U41(mark(X1),X2,X3) -> mark(U41(X1,X2,X3))
  U42(mark(X1),X2,X3) -> mark(U42(X1,X2,X3))
  s(mark(X)) -> mark(s(X))
  plus(mark(X1),X2) -> mark(plus(X1,X2))
  plus(X1,mark(X2)) -> mark(plus(X1,X2))
  proper(U11(X1,X2)) -> U11(proper(X1),proper(X2))
  proper(tt()) -> ok(tt())
  proper(U12(X)) -> U12(proper(X))
  proper(isNat(X)) -> isNat(proper(X))
  proper(U21(X)) -> U21(proper(X))
  proper(U31(X1,X2)) -> U31(proper(X1),proper(X2))
  proper(U41(X1,X2,X3)) -> U41(proper(X1),proper(X2),proper(X3))
  proper(U42(X1,X2,X3)) -> U42(proper(X1),proper(X2),proper(X3))
  proper(s(X)) -> s(proper(X))
  proper(plus(X1,X2)) -> plus(proper(X1),proper(X2))
  proper(|0|()) -> ok(|0|())
  U11(ok(X1),ok(X2)) -> ok(U11(X1,X2))
  U12(ok(X)) -> ok(U12(X))
  isNat(ok(X)) -> ok(isNat(X))
  U21(ok(X)) -> ok(U21(X))
  U31(ok(X1),ok(X2)) -> ok(U31(X1,X2))
  U41(ok(X1),ok(X2),ok(X3)) -> ok(U41(X1,X2,X3))
  U42(ok(X1),ok(X2),ok(X3)) -> ok(U42(X1,X2,X3))
  s(ok(X)) -> ok(s(X))
  plus(ok(X1),ok(X2)) -> ok(plus(X1,X2))
  top(mark(X)) -> top(proper(X))
  top(ok(X)) -> top(active(X))

-- SCC decomposition.

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

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

and R consists of:

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

The estimated dependency graph contains the following SCCs:

  {p76, p78}
  {p16, p18, p20, p22, p24, p26, p28, p30, p32}
  {p43, p44, p46, p48, p50, p52, p53, p55, p56, p57, p59, p60, p61, p63, p65, p66}
  {p34, p68}
  {p69}
  {p38, p73}
  {p39, p74}
  {p40, p41, p75}
  {p33, p67}
  {p35, p70}
  {p36, p71}
  {p37, p72}


-- Reduction pair.

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

p1: top#(ok(X)) -> top#(active(X))
p2: top#(mark(X)) -> top#(proper(X))

and R consists of:

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

The set of usable rules consists of

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

Take the reduction pair:

  lexicographic combination of reduction pairs:
  
    1. matrix interpretations:
    
      carrier: N^4
      order: lexicographic order
      interpretations:
        top#_A(x1) = ((0,0,0,0),(1,0,0,0),(0,1,0,0),(0,0,1,0)) x1
        ok_A(x1) = x1 + (0,0,0,2)
        active_A(x1) = x1 + (0,0,0,1)
        mark_A(x1) = x1 + (0,0,2,0)
        proper_A(x1) = ((1,0,0,0),(0,1,0,0),(0,0,1,0),(0,1,1,0)) x1 + (0,0,0,1)
        U11_A(x1,x2) = x1 + ((0,0,0,0),(0,0,0,0),(1,0,0,0),(0,0,0,0)) x2 + (0,0,8,9)
        U12_A(x1) = ((1,0,0,0),(0,1,0,0),(0,1,1,0),(0,0,0,1)) x1 + (0,0,2,0)
        U21_A(x1) = x1 + (0,0,3,0)
        U31_A(x1,x2) = x1 + ((1,0,0,0),(0,1,0,0),(1,1,0,0),(0,0,0,0)) x2 + (1,2,1,3)
        U41_A(x1,x2,x3) = x1 + ((1,0,0,0),(1,1,0,0),(0,0,0,0),(0,0,0,0)) x2 + ((1,0,0,0),(0,1,0,0),(1,0,1,0),(0,0,0,0)) x3 + (16,4,6,3)
        U42_A(x1,x2,x3) = x1 + ((1,0,0,0),(1,1,0,0),(0,0,0,0),(0,0,0,0)) x2 + x3 + (16,3,1,3)
        s_A(x1) = x1 + (6,1,1,0)
        plus_A(x1,x2) = ((1,0,0,0),(0,1,0,0),(1,1,1,0),(0,0,1,0)) x1 + ((1,0,0,0),(1,1,0,0),(1,1,1,0),(0,1,0,1)) x2 + (11,2,1,1)
        isNat_A(x1) = ((0,0,0,0),(0,0,0,0),(1,0,0,0),(0,0,0,0)) x1 + (1,1,2,3)
        tt_A() = (1,1,0,0)
        |0|_A() = (1,0,2,1)
    
    2. lexicographic path order with precedence:
    
      precedence:
      
        U31 > U41 > proper > plus > U11 > isNat > s > ok > active > top# > U42 > mark > U12 > tt > |0| > U21
      
      argument filter:
    
        pi(top#) = []
        pi(ok) = []
        pi(active) = [1]
        pi(mark) = []
        pi(proper) = []
        pi(U11) = []
        pi(U12) = [1]
        pi(U21) = [1]
        pi(U31) = []
        pi(U41) = []
        pi(U42) = []
        pi(s) = []
        pi(plus) = 2
        pi(isNat) = []
        pi(tt) = []
        pi(|0|) = []
    

The next rules are strictly ordered:

  p2

We remove them from the problem.

-- SCC decomposition.

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

p1: top#(ok(X)) -> top#(active(X))

and R consists of:

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

The estimated dependency graph contains the following SCCs:

  {p1}


-- Reduction pair.

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

p1: top#(ok(X)) -> top#(active(X))

and R consists of:

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

The set of usable rules consists of

  r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r12, r13, r14, r15, r16, r17, r18, r19, r20, r21, r22, r23, r24, r25, r26, r27, r28, r29, r41, r42, r43, r44, r45, r46, r47, r48, r49

Take the reduction pair:

  lexicographic combination of reduction pairs:
  
    1. matrix interpretations:
    
      carrier: N^4
      order: lexicographic order
      interpretations:
        top#_A(x1) = ((1,0,0,0),(0,1,0,0),(0,0,1,0),(1,0,0,1)) x1
        ok_A(x1) = x1 + (10,16,10,45)
        active_A(x1) = ((1,0,0,0),(1,1,0,0),(1,0,1,0),(0,0,1,0)) x1 + (0,8,9,16)
        U11_A(x1,x2) = ((1,0,0,0),(0,0,0,0),(1,1,0,0),(1,0,1,0)) x1 + ((0,0,0,0),(0,0,0,0),(1,0,0,0),(0,0,0,0)) x2 + (0,17,2,10)
        mark_A(x1) = ((0,0,0,0),(0,0,0,0),(1,0,0,0),(0,1,0,0)) x1 + (0,1,13,15)
        U12_A(x1) = ((1,0,0,0),(1,1,0,0),(1,1,1,0),(0,1,0,1)) x1 + (1,0,1,1)
        U21_A(x1) = ((1,0,0,0),(0,0,0,0),(0,1,0,0),(0,1,0,0)) x1 + (0,16,0,29)
        U31_A(x1,x2) = ((1,0,0,0),(0,1,0,0),(0,1,1,0),(1,1,1,1)) x1 + ((0,0,0,0),(1,0,0,0),(0,0,0,0),(0,0,0,0)) x2 + (1,0,19,1)
        U41_A(x1,x2,x3) = ((1,0,0,0),(0,1,0,0),(1,0,1,0),(1,0,0,1)) x1 + ((0,0,0,0),(1,0,0,0),(0,1,0,0),(0,0,0,0)) x3 + (0,0,2,1)
        U42_A(x1,x2,x3) = ((1,0,0,0),(0,1,0,0),(1,0,1,0),(0,0,1,1)) x1 + ((1,0,0,0),(0,1,0,0),(1,0,0,0),(0,1,1,0)) x2 + ((1,0,0,0),(0,1,0,0),(1,0,0,0),(0,1,1,0)) x3 + (1,0,3,1)
        s_A(x1) = ((1,0,0,0),(1,1,0,0),(1,0,0,0),(0,1,1,0)) x1 + (0,1,1,1)
        plus_A(x1,x2) = ((1,0,0,0),(0,0,0,0),(0,0,0,0),(0,1,0,0)) x2 + (0,17,11,28)
        isNat_A(x1) = ((1,0,0,0),(1,1,0,0),(0,1,1,0),(1,1,0,1)) x1 + (1,13,1,1)
        tt_A() = (0,5,1,1)
        |0|_A() = (1,4,0,1)
    
    2. lexicographic path order with precedence:
    
      precedence:
      
        |0| > U11 > U21 > isNat > plus > U42 > U31 > U12 > U41 > tt > top# > ok > active > s > mark
      
      argument filter:
    
        pi(top#) = 1
        pi(ok) = []
        pi(active) = []
        pi(U11) = []
        pi(mark) = []
        pi(U12) = []
        pi(U21) = []
        pi(U31) = 1
        pi(U41) = 1
        pi(U42) = []
        pi(s) = []
        pi(plus) = []
        pi(isNat) = []
        pi(tt) = []
        pi(|0|) = []
    

The next rules are strictly ordered:

  p1

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

-- Reduction pair.

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

p1: active#(plus(X1,X2)) -> active#(X2)
p2: active#(plus(X1,X2)) -> active#(X1)
p3: active#(s(X)) -> active#(X)
p4: active#(U42(X1,X2,X3)) -> active#(X1)
p5: active#(U41(X1,X2,X3)) -> active#(X1)
p6: active#(U31(X1,X2)) -> active#(X1)
p7: active#(U21(X)) -> active#(X)
p8: active#(U12(X)) -> active#(X)
p9: active#(U11(X1,X2)) -> active#(X1)

and R consists of:

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

The set of usable rules consists of

  (no rules)

Take the monotone reduction pair:

  lexicographic combination of reduction pairs:
  
    1. matrix interpretations:
    
      carrier: N^4
      order: lexicographic order
      interpretations:
        active#_A(x1) = ((1,0,0,0),(1,1,0,0),(1,1,1,0),(1,1,1,1)) x1
        plus_A(x1,x2) = ((1,0,0,0),(1,1,0,0),(1,1,1,0),(1,1,1,1)) x1 + ((1,0,0,0),(1,1,0,0),(1,1,1,0),(1,1,1,1)) x2 + (1,1,1,1)
        s_A(x1) = ((1,0,0,0),(1,1,0,0),(1,1,1,0),(1,1,1,1)) x1 + (1,1,1,1)
        U42_A(x1,x2,x3) = ((1,0,0,0),(1,1,0,0),(1,1,1,0),(1,1,1,1)) x1 + ((1,0,0,0),(1,1,0,0),(1,1,1,0),(1,1,1,1)) x2 + ((1,0,0,0),(1,1,0,0),(1,0,1,0),(1,1,1,1)) x3 + (1,1,1,1)
        U41_A(x1,x2,x3) = ((1,0,0,0),(1,1,0,0),(1,1,1,0),(1,1,1,1)) x1 + ((1,0,0,0),(1,1,0,0),(1,1,1,0),(1,1,1,1)) x2 + ((1,0,0,0),(1,1,0,0),(1,1,1,0),(1,1,1,1)) x3 + (1,1,1,1)
        U31_A(x1,x2) = ((1,0,0,0),(1,1,0,0),(1,1,1,0),(1,1,1,1)) x1 + ((1,0,0,0),(1,1,0,0),(1,1,1,0),(1,1,1,1)) x2 + (1,1,1,1)
        U21_A(x1) = ((1,0,0,0),(1,1,0,0),(1,1,1,0),(1,1,1,1)) x1 + (1,1,1,1)
        U12_A(x1) = ((1,0,0,0),(1,1,0,0),(1,1,1,0),(1,1,1,1)) x1 + (1,1,1,1)
        U11_A(x1,x2) = ((1,0,0,0),(1,1,0,0),(1,1,1,0),(1,1,1,1)) x1 + ((1,0,0,0),(1,1,0,0),(1,1,1,0),(1,1,1,1)) x2 + (1,1,1,1)
    
    2. lexicographic path order with precedence:
    
      precedence:
      
        active# > U11 > U12 > U21 > U31 > U41 > U42 > s > plus
      
      argument filter:
    
        pi(active#) = 1
        pi(plus) = [1, 2]
        pi(s) = [1]
        pi(U42) = [1, 2, 3]
        pi(U41) = [1, 2, 3]
        pi(U31) = [1, 2]
        pi(U21) = [1]
        pi(U12) = [1]
        pi(U11) = [1, 2]
    

The next rules are strictly ordered:

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

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

-- Reduction pair.

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

p1: proper#(plus(X1,X2)) -> proper#(X2)
p2: proper#(plus(X1,X2)) -> proper#(X1)
p3: proper#(s(X)) -> proper#(X)
p4: proper#(U42(X1,X2,X3)) -> proper#(X3)
p5: proper#(U42(X1,X2,X3)) -> proper#(X2)
p6: proper#(U42(X1,X2,X3)) -> proper#(X1)
p7: proper#(U41(X1,X2,X3)) -> proper#(X3)
p8: proper#(U41(X1,X2,X3)) -> proper#(X2)
p9: proper#(U41(X1,X2,X3)) -> proper#(X1)
p10: proper#(U31(X1,X2)) -> proper#(X2)
p11: proper#(U31(X1,X2)) -> proper#(X1)
p12: proper#(U21(X)) -> proper#(X)
p13: proper#(isNat(X)) -> proper#(X)
p14: proper#(U12(X)) -> proper#(X)
p15: proper#(U11(X1,X2)) -> proper#(X2)
p16: proper#(U11(X1,X2)) -> proper#(X1)

and R consists of:

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

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  lexicographic combination of reduction pairs:
  
    1. matrix interpretations:
    
      carrier: N^4
      order: lexicographic order
      interpretations:
        proper#_A(x1) = ((1,0,0,0),(0,1,0,0),(1,1,1,0),(1,1,1,1)) x1
        plus_A(x1,x2) = ((1,0,0,0),(1,1,0,0),(1,1,1,0),(1,1,1,1)) x1 + ((1,0,0,0),(1,1,0,0),(1,1,1,0),(1,1,1,1)) x2 + (1,1,1,1)
        s_A(x1) = ((1,0,0,0),(1,1,0,0),(1,1,1,0),(1,1,1,1)) x1 + (1,1,1,1)
        U42_A(x1,x2,x3) = ((1,0,0,0),(1,1,0,0),(1,1,1,0),(1,1,1,1)) x1 + ((1,0,0,0),(1,1,0,0),(1,1,1,0),(1,1,1,1)) x2 + ((1,0,0,0),(1,1,0,0),(1,1,1,0),(1,1,1,1)) x3 + (1,1,1,1)
        U41_A(x1,x2,x3) = ((1,0,0,0),(1,1,0,0),(1,1,1,0),(1,1,1,1)) x1 + ((1,0,0,0),(1,1,0,0),(1,1,1,0),(1,1,1,1)) x2 + ((1,0,0,0),(1,1,0,0),(1,1,1,0),(1,1,1,1)) x3 + (1,1,1,1)
        U31_A(x1,x2) = ((1,0,0,0),(1,1,0,0),(1,1,1,0),(1,1,1,1)) x1 + ((1,0,0,0),(1,1,0,0),(1,1,1,0),(1,1,1,1)) x2 + (1,1,1,1)
        U21_A(x1) = ((1,0,0,0),(1,1,0,0),(1,1,1,0),(1,1,1,1)) x1 + (1,1,1,1)
        isNat_A(x1) = ((1,0,0,0),(1,1,0,0),(1,1,1,0),(1,1,1,1)) x1 + (1,1,1,1)
        U12_A(x1) = ((1,0,0,0),(1,1,0,0),(1,1,1,0),(1,1,1,1)) x1 + (1,1,1,1)
        U11_A(x1,x2) = ((1,0,0,0),(1,1,0,0),(1,1,1,0),(1,1,1,1)) x1 + ((1,0,0,0),(1,1,0,0),(1,1,1,0),(1,1,1,1)) x2 + (1,1,1,1)
    
    2. lexicographic path order with precedence:
    
      precedence:
      
        proper# > U11 > U12 > isNat > U21 > U31 > U41 > U42 > s > plus
      
      argument filter:
    
        pi(proper#) = 1
        pi(plus) = 1
        pi(s) = [1]
        pi(U42) = 2
        pi(U41) = [1, 2, 3]
        pi(U31) = [1, 2]
        pi(U21) = [1]
        pi(isNat) = [1]
        pi(U12) = [1]
        pi(U11) = [1, 2]
    

The next rules are strictly ordered:

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

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

-- Reduction pair.

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

p1: U12#(mark(X)) -> U12#(X)
p2: U12#(ok(X)) -> U12#(X)

and R consists of:

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

The set of usable rules consists of

  (no rules)

Take the reduction pair:

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

The next rules are strictly ordered:

  p1, p2

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

-- Reduction pair.

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

p1: isNat#(ok(X)) -> isNat#(X)

and R consists of:

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

The set of usable rules consists of

  (no rules)

Take the reduction pair:

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

The next rules are strictly ordered:

  p1

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

-- Reduction pair.

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

p1: U42#(mark(X1),X2,X3) -> U42#(X1,X2,X3)
p2: U42#(ok(X1),ok(X2),ok(X3)) -> U42#(X1,X2,X3)

and R consists of:

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

The set of usable rules consists of

  (no rules)

Take the reduction pair:

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

and R consists of:

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

The set of usable rules consists of

  (no rules)

Take the reduction pair:

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

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#(ok(X1),ok(X2)) -> plus#(X1,X2)
p3: plus#(X1,mark(X2)) -> plus#(X1,X2)

and R consists of:

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

The set of usable rules consists of

  (no rules)

Take the reduction pair:

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

The next rules are strictly ordered:

  p1, p2, p3

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

-- Reduction pair.

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

p1: U11#(mark(X1),X2) -> U11#(X1,X2)
p2: U11#(ok(X1),ok(X2)) -> U11#(X1,X2)

and R consists of:

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

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  lexicographic combination of reduction pairs:
  
    1. matrix interpretations:
    
      carrier: N^4
      order: lexicographic order
      interpretations:
        U11#_A(x1,x2) = ((1,0,0,0),(1,1,0,0),(1,1,1,0),(1,1,1,1)) x1 + ((1,0,0,0),(0,1,0,0),(0,0,1,0),(1,1,1,1)) x2
        mark_A(x1) = ((1,0,0,0),(1,1,0,0),(1,1,1,0),(1,1,1,1)) x1 + (1,1,1,1)
        ok_A(x1) = ((1,0,0,0),(1,1,0,0),(1,1,1,0),(1,1,1,1)) x1 + (1,1,1,1)
    
    2. lexicographic path order with precedence:
    
      precedence:
      
        U11# > ok > mark
      
      argument filter:
    
        pi(U11#) = 1
        pi(mark) = 1
        pi(ok) = 1
    

The next rules are strictly ordered:

  p1, p2

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

-- Reduction pair.

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

p1: U21#(mark(X)) -> U21#(X)
p2: U21#(ok(X)) -> U21#(X)

and R consists of:

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

The set of usable rules consists of

  (no rules)

Take the reduction pair:

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

The next rules are strictly ordered:

  p1, p2

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

-- Reduction pair.

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

p1: U31#(mark(X1),X2) -> U31#(X1,X2)
p2: U31#(ok(X1),ok(X2)) -> U31#(X1,X2)

and R consists of:

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

The set of usable rules consists of

  (no rules)

Take the reduction pair:

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

and R consists of:

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

The set of usable rules consists of

  (no rules)

Take the reduction pair:

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

The next rules are strictly ordered:

  p1, p2

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