YES

We show the termination of the TRS R:

  O(|0|()) -> |0|()
  +(|0|(),x) -> x
  +(x,|0|()) -> x
  +(O(x),O(y)) -> O(+(x,y))
  +(O(x),I(y)) -> I(+(x,y))
  +(I(x),O(y)) -> I(+(x,y))
  +(I(x),I(y)) -> O(+(+(x,y),I(|0|())))
  +(x,+(y,z)) -> +(+(x,y),z)
  -(x,|0|()) -> x
  -(|0|(),x) -> |0|()
  -(O(x),O(y)) -> O(-(x,y))
  -(O(x),I(y)) -> I(-(-(x,y),I(|1|())))
  -(I(x),O(y)) -> I(-(x,y))
  -(I(x),I(y)) -> O(-(x,y))
  not(true()) -> false()
  not(false()) -> true()
  and(x,true()) -> x
  and(x,false()) -> false()
  if(true(),x,y) -> x
  if(false(),x,y) -> y
  ge(O(x),O(y)) -> ge(x,y)
  ge(O(x),I(y)) -> not(ge(y,x))
  ge(I(x),O(y)) -> ge(x,y)
  ge(I(x),I(y)) -> ge(x,y)
  ge(x,|0|()) -> true()
  ge(|0|(),O(x)) -> ge(|0|(),x)
  ge(|0|(),I(x)) -> false()
  |Log'|(|0|()) -> |0|()
  |Log'|(I(x)) -> +(|Log'|(x),I(|0|()))
  |Log'|(O(x)) -> if(ge(x,I(|0|())),+(|Log'|(x),I(|0|())),|0|())
  Log(x) -> -(|Log'|(x),I(|0|()))
  Val(L(x)) -> x
  Val(N(x,l(),r())) -> x
  Min(L(x)) -> x
  Min(N(x,l(),r())) -> Min(l())
  Max(L(x)) -> x
  Max(N(x,l(),r())) -> Max(r())
  BS(L(x)) -> true()
  BS(N(x,l(),r())) -> and(and(ge(x,Max(l())),ge(Min(r()),x)),and(BS(l()),BS(r())))
  Size(L(x)) -> I(|0|())
  Size(N(x,l(),r())) -> +(+(Size(l()),Size(r())),I(|1|()))
  WB(L(x)) -> true()
  WB(N(x,l(),r())) -> and(if(ge(Size(l()),Size(r())),ge(I(|0|()),-(Size(l()),Size(r()))),ge(I(|0|()),-(Size(r()),Size(l())))),and(WB(l()),WB(r())))

-- SCC decomposition.

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

p1: +#(O(x),O(y)) -> O#(+(x,y))
p2: +#(O(x),O(y)) -> +#(x,y)
p3: +#(O(x),I(y)) -> +#(x,y)
p4: +#(I(x),O(y)) -> +#(x,y)
p5: +#(I(x),I(y)) -> O#(+(+(x,y),I(|0|())))
p6: +#(I(x),I(y)) -> +#(+(x,y),I(|0|()))
p7: +#(I(x),I(y)) -> +#(x,y)
p8: +#(x,+(y,z)) -> +#(+(x,y),z)
p9: +#(x,+(y,z)) -> +#(x,y)
p10: -#(O(x),O(y)) -> O#(-(x,y))
p11: -#(O(x),O(y)) -> -#(x,y)
p12: -#(O(x),I(y)) -> -#(-(x,y),I(|1|()))
p13: -#(O(x),I(y)) -> -#(x,y)
p14: -#(I(x),O(y)) -> -#(x,y)
p15: -#(I(x),I(y)) -> O#(-(x,y))
p16: -#(I(x),I(y)) -> -#(x,y)
p17: ge#(O(x),O(y)) -> ge#(x,y)
p18: ge#(O(x),I(y)) -> not#(ge(y,x))
p19: ge#(O(x),I(y)) -> ge#(y,x)
p20: ge#(I(x),O(y)) -> ge#(x,y)
p21: ge#(I(x),I(y)) -> ge#(x,y)
p22: ge#(|0|(),O(x)) -> ge#(|0|(),x)
p23: |Log'|#(I(x)) -> +#(|Log'|(x),I(|0|()))
p24: |Log'|#(I(x)) -> |Log'|#(x)
p25: |Log'|#(O(x)) -> if#(ge(x,I(|0|())),+(|Log'|(x),I(|0|())),|0|())
p26: |Log'|#(O(x)) -> ge#(x,I(|0|()))
p27: |Log'|#(O(x)) -> +#(|Log'|(x),I(|0|()))
p28: |Log'|#(O(x)) -> |Log'|#(x)
p29: Log#(x) -> -#(|Log'|(x),I(|0|()))
p30: Log#(x) -> |Log'|#(x)
p31: Min#(N(x,l(),r())) -> Min#(l())
p32: Max#(N(x,l(),r())) -> Max#(r())
p33: BS#(N(x,l(),r())) -> and#(and(ge(x,Max(l())),ge(Min(r()),x)),and(BS(l()),BS(r())))
p34: BS#(N(x,l(),r())) -> and#(ge(x,Max(l())),ge(Min(r()),x))
p35: BS#(N(x,l(),r())) -> ge#(x,Max(l()))
p36: BS#(N(x,l(),r())) -> Max#(l())
p37: BS#(N(x,l(),r())) -> ge#(Min(r()),x)
p38: BS#(N(x,l(),r())) -> Min#(r())
p39: BS#(N(x,l(),r())) -> and#(BS(l()),BS(r()))
p40: BS#(N(x,l(),r())) -> BS#(l())
p41: BS#(N(x,l(),r())) -> BS#(r())
p42: Size#(N(x,l(),r())) -> +#(+(Size(l()),Size(r())),I(|1|()))
p43: Size#(N(x,l(),r())) -> +#(Size(l()),Size(r()))
p44: Size#(N(x,l(),r())) -> Size#(l())
p45: Size#(N(x,l(),r())) -> Size#(r())
p46: WB#(N(x,l(),r())) -> and#(if(ge(Size(l()),Size(r())),ge(I(|0|()),-(Size(l()),Size(r()))),ge(I(|0|()),-(Size(r()),Size(l())))),and(WB(l()),WB(r())))
p47: WB#(N(x,l(),r())) -> if#(ge(Size(l()),Size(r())),ge(I(|0|()),-(Size(l()),Size(r()))),ge(I(|0|()),-(Size(r()),Size(l()))))
p48: WB#(N(x,l(),r())) -> ge#(Size(l()),Size(r()))
p49: WB#(N(x,l(),r())) -> Size#(l())
p50: WB#(N(x,l(),r())) -> Size#(r())
p51: WB#(N(x,l(),r())) -> ge#(I(|0|()),-(Size(l()),Size(r())))
p52: WB#(N(x,l(),r())) -> -#(Size(l()),Size(r()))
p53: WB#(N(x,l(),r())) -> ge#(I(|0|()),-(Size(r()),Size(l())))
p54: WB#(N(x,l(),r())) -> -#(Size(r()),Size(l()))
p55: WB#(N(x,l(),r())) -> and#(WB(l()),WB(r()))
p56: WB#(N(x,l(),r())) -> WB#(l())
p57: WB#(N(x,l(),r())) -> WB#(r())

and R consists of:

r1: O(|0|()) -> |0|()
r2: +(|0|(),x) -> x
r3: +(x,|0|()) -> x
r4: +(O(x),O(y)) -> O(+(x,y))
r5: +(O(x),I(y)) -> I(+(x,y))
r6: +(I(x),O(y)) -> I(+(x,y))
r7: +(I(x),I(y)) -> O(+(+(x,y),I(|0|())))
r8: +(x,+(y,z)) -> +(+(x,y),z)
r9: -(x,|0|()) -> x
r10: -(|0|(),x) -> |0|()
r11: -(O(x),O(y)) -> O(-(x,y))
r12: -(O(x),I(y)) -> I(-(-(x,y),I(|1|())))
r13: -(I(x),O(y)) -> I(-(x,y))
r14: -(I(x),I(y)) -> O(-(x,y))
r15: not(true()) -> false()
r16: not(false()) -> true()
r17: and(x,true()) -> x
r18: and(x,false()) -> false()
r19: if(true(),x,y) -> x
r20: if(false(),x,y) -> y
r21: ge(O(x),O(y)) -> ge(x,y)
r22: ge(O(x),I(y)) -> not(ge(y,x))
r23: ge(I(x),O(y)) -> ge(x,y)
r24: ge(I(x),I(y)) -> ge(x,y)
r25: ge(x,|0|()) -> true()
r26: ge(|0|(),O(x)) -> ge(|0|(),x)
r27: ge(|0|(),I(x)) -> false()
r28: |Log'|(|0|()) -> |0|()
r29: |Log'|(I(x)) -> +(|Log'|(x),I(|0|()))
r30: |Log'|(O(x)) -> if(ge(x,I(|0|())),+(|Log'|(x),I(|0|())),|0|())
r31: Log(x) -> -(|Log'|(x),I(|0|()))
r32: Val(L(x)) -> x
r33: Val(N(x,l(),r())) -> x
r34: Min(L(x)) -> x
r35: Min(N(x,l(),r())) -> Min(l())
r36: Max(L(x)) -> x
r37: Max(N(x,l(),r())) -> Max(r())
r38: BS(L(x)) -> true()
r39: BS(N(x,l(),r())) -> and(and(ge(x,Max(l())),ge(Min(r()),x)),and(BS(l()),BS(r())))
r40: Size(L(x)) -> I(|0|())
r41: Size(N(x,l(),r())) -> +(+(Size(l()),Size(r())),I(|1|()))
r42: WB(L(x)) -> true()
r43: WB(N(x,l(),r())) -> and(if(ge(Size(l()),Size(r())),ge(I(|0|()),-(Size(l()),Size(r()))),ge(I(|0|()),-(Size(r()),Size(l())))),and(WB(l()),WB(r())))

The estimated dependency graph contains the following SCCs:

  {p24, p28}
  {p2, p3, p4, p6, p7, p8, p9}
  {p11, p12, p13, p14, p16}
  {p17, p19, p20, p21}
  {p22}


-- Reduction pair.

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

p1: |Log'|#(O(x)) -> |Log'|#(x)
p2: |Log'|#(I(x)) -> |Log'|#(x)

and R consists of:

r1: O(|0|()) -> |0|()
r2: +(|0|(),x) -> x
r3: +(x,|0|()) -> x
r4: +(O(x),O(y)) -> O(+(x,y))
r5: +(O(x),I(y)) -> I(+(x,y))
r6: +(I(x),O(y)) -> I(+(x,y))
r7: +(I(x),I(y)) -> O(+(+(x,y),I(|0|())))
r8: +(x,+(y,z)) -> +(+(x,y),z)
r9: -(x,|0|()) -> x
r10: -(|0|(),x) -> |0|()
r11: -(O(x),O(y)) -> O(-(x,y))
r12: -(O(x),I(y)) -> I(-(-(x,y),I(|1|())))
r13: -(I(x),O(y)) -> I(-(x,y))
r14: -(I(x),I(y)) -> O(-(x,y))
r15: not(true()) -> false()
r16: not(false()) -> true()
r17: and(x,true()) -> x
r18: and(x,false()) -> false()
r19: if(true(),x,y) -> x
r20: if(false(),x,y) -> y
r21: ge(O(x),O(y)) -> ge(x,y)
r22: ge(O(x),I(y)) -> not(ge(y,x))
r23: ge(I(x),O(y)) -> ge(x,y)
r24: ge(I(x),I(y)) -> ge(x,y)
r25: ge(x,|0|()) -> true()
r26: ge(|0|(),O(x)) -> ge(|0|(),x)
r27: ge(|0|(),I(x)) -> false()
r28: |Log'|(|0|()) -> |0|()
r29: |Log'|(I(x)) -> +(|Log'|(x),I(|0|()))
r30: |Log'|(O(x)) -> if(ge(x,I(|0|())),+(|Log'|(x),I(|0|())),|0|())
r31: Log(x) -> -(|Log'|(x),I(|0|()))
r32: Val(L(x)) -> x
r33: Val(N(x,l(),r())) -> x
r34: Min(L(x)) -> x
r35: Min(N(x,l(),r())) -> Min(l())
r36: Max(L(x)) -> x
r37: Max(N(x,l(),r())) -> Max(r())
r38: BS(L(x)) -> true()
r39: BS(N(x,l(),r())) -> and(and(ge(x,Max(l())),ge(Min(r()),x)),and(BS(l()),BS(r())))
r40: Size(L(x)) -> I(|0|())
r41: Size(N(x,l(),r())) -> +(+(Size(l()),Size(r())),I(|1|()))
r42: WB(L(x)) -> true()
r43: WB(N(x,l(),r())) -> and(if(ge(Size(l()),Size(r())),ge(I(|0|()),-(Size(l()),Size(r()))),ge(I(|0|()),-(Size(r()),Size(l())))),and(WB(l()),WB(r())))

The set of usable rules consists of

  (no rules)

Take the monotone reduction pair:

  matrix interpretations:
  
    carrier: N^4
    order: lexicographic order
    interpretations:
      |Log'|#_A(x1) = ((1,0,0,0),(0,1,0,0),(0,0,1,0),(0,1,1,1)) x1
      O_A(x1) = ((1,0,0,0),(1,1,0,0),(1,1,1,0),(1,1,1,1)) x1 + (1,1,1,1)
      I_A(x1) = ((1,0,0,0),(1,1,0,0),(1,1,1,0),(1,0,1,1)) x1 + (1,1,1,1)

The next rules are strictly ordered:

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

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: +#(O(x),O(y)) -> +#(x,y)
p2: +#(x,+(y,z)) -> +#(x,y)
p3: +#(x,+(y,z)) -> +#(+(x,y),z)
p4: +#(I(x),I(y)) -> +#(x,y)
p5: +#(I(x),I(y)) -> +#(+(x,y),I(|0|()))
p6: +#(O(x),I(y)) -> +#(x,y)
p7: +#(I(x),O(y)) -> +#(x,y)

and R consists of:

r1: O(|0|()) -> |0|()
r2: +(|0|(),x) -> x
r3: +(x,|0|()) -> x
r4: +(O(x),O(y)) -> O(+(x,y))
r5: +(O(x),I(y)) -> I(+(x,y))
r6: +(I(x),O(y)) -> I(+(x,y))
r7: +(I(x),I(y)) -> O(+(+(x,y),I(|0|())))
r8: +(x,+(y,z)) -> +(+(x,y),z)
r9: -(x,|0|()) -> x
r10: -(|0|(),x) -> |0|()
r11: -(O(x),O(y)) -> O(-(x,y))
r12: -(O(x),I(y)) -> I(-(-(x,y),I(|1|())))
r13: -(I(x),O(y)) -> I(-(x,y))
r14: -(I(x),I(y)) -> O(-(x,y))
r15: not(true()) -> false()
r16: not(false()) -> true()
r17: and(x,true()) -> x
r18: and(x,false()) -> false()
r19: if(true(),x,y) -> x
r20: if(false(),x,y) -> y
r21: ge(O(x),O(y)) -> ge(x,y)
r22: ge(O(x),I(y)) -> not(ge(y,x))
r23: ge(I(x),O(y)) -> ge(x,y)
r24: ge(I(x),I(y)) -> ge(x,y)
r25: ge(x,|0|()) -> true()
r26: ge(|0|(),O(x)) -> ge(|0|(),x)
r27: ge(|0|(),I(x)) -> false()
r28: |Log'|(|0|()) -> |0|()
r29: |Log'|(I(x)) -> +(|Log'|(x),I(|0|()))
r30: |Log'|(O(x)) -> if(ge(x,I(|0|())),+(|Log'|(x),I(|0|())),|0|())
r31: Log(x) -> -(|Log'|(x),I(|0|()))
r32: Val(L(x)) -> x
r33: Val(N(x,l(),r())) -> x
r34: Min(L(x)) -> x
r35: Min(N(x,l(),r())) -> Min(l())
r36: Max(L(x)) -> x
r37: Max(N(x,l(),r())) -> Max(r())
r38: BS(L(x)) -> true()
r39: BS(N(x,l(),r())) -> and(and(ge(x,Max(l())),ge(Min(r()),x)),and(BS(l()),BS(r())))
r40: Size(L(x)) -> I(|0|())
r41: Size(N(x,l(),r())) -> +(+(Size(l()),Size(r())),I(|1|()))
r42: WB(L(x)) -> true()
r43: WB(N(x,l(),r())) -> and(if(ge(Size(l()),Size(r())),ge(I(|0|()),-(Size(l()),Size(r()))),ge(I(|0|()),-(Size(r()),Size(l())))),and(WB(l()),WB(r())))

The set of usable rules consists of

  r1, r2, r3, r4, r5, r6, r7, r8

Take the reduction pair:

  matrix interpretations:
  
    carrier: N^4
    order: lexicographic order
    interpretations:
      +#_A(x1,x2) = ((0,0,0,0),(0,0,0,0),(1,0,0,0),(1,0,0,0)) x1 + ((1,0,0,0),(1,1,0,0),(1,0,1,0),(0,0,1,1)) x2
      O_A(x1) = ((1,0,0,0),(1,1,0,0),(0,1,1,0),(0,0,0,0)) x1 + (1,1,0,9)
      +_A(x1,x2) = ((1,0,0,0),(0,1,0,0),(0,0,1,0),(1,1,0,1)) x1 + ((1,0,0,0),(0,1,0,0),(1,0,1,0),(0,0,0,1)) x2 + (2,5,2,1)
      I_A(x1) = ((1,0,0,0),(0,0,0,0),(1,1,0,0),(0,0,0,0)) x1 + (4,1,1,1)
      |0|_A() = (0,1,1,1)

The next rules are strictly ordered:

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

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: -#(O(x),O(y)) -> -#(x,y)
p2: -#(I(x),I(y)) -> -#(x,y)
p3: -#(I(x),O(y)) -> -#(x,y)
p4: -#(O(x),I(y)) -> -#(x,y)
p5: -#(O(x),I(y)) -> -#(-(x,y),I(|1|()))

and R consists of:

r1: O(|0|()) -> |0|()
r2: +(|0|(),x) -> x
r3: +(x,|0|()) -> x
r4: +(O(x),O(y)) -> O(+(x,y))
r5: +(O(x),I(y)) -> I(+(x,y))
r6: +(I(x),O(y)) -> I(+(x,y))
r7: +(I(x),I(y)) -> O(+(+(x,y),I(|0|())))
r8: +(x,+(y,z)) -> +(+(x,y),z)
r9: -(x,|0|()) -> x
r10: -(|0|(),x) -> |0|()
r11: -(O(x),O(y)) -> O(-(x,y))
r12: -(O(x),I(y)) -> I(-(-(x,y),I(|1|())))
r13: -(I(x),O(y)) -> I(-(x,y))
r14: -(I(x),I(y)) -> O(-(x,y))
r15: not(true()) -> false()
r16: not(false()) -> true()
r17: and(x,true()) -> x
r18: and(x,false()) -> false()
r19: if(true(),x,y) -> x
r20: if(false(),x,y) -> y
r21: ge(O(x),O(y)) -> ge(x,y)
r22: ge(O(x),I(y)) -> not(ge(y,x))
r23: ge(I(x),O(y)) -> ge(x,y)
r24: ge(I(x),I(y)) -> ge(x,y)
r25: ge(x,|0|()) -> true()
r26: ge(|0|(),O(x)) -> ge(|0|(),x)
r27: ge(|0|(),I(x)) -> false()
r28: |Log'|(|0|()) -> |0|()
r29: |Log'|(I(x)) -> +(|Log'|(x),I(|0|()))
r30: |Log'|(O(x)) -> if(ge(x,I(|0|())),+(|Log'|(x),I(|0|())),|0|())
r31: Log(x) -> -(|Log'|(x),I(|0|()))
r32: Val(L(x)) -> x
r33: Val(N(x,l(),r())) -> x
r34: Min(L(x)) -> x
r35: Min(N(x,l(),r())) -> Min(l())
r36: Max(L(x)) -> x
r37: Max(N(x,l(),r())) -> Max(r())
r38: BS(L(x)) -> true()
r39: BS(N(x,l(),r())) -> and(and(ge(x,Max(l())),ge(Min(r()),x)),and(BS(l()),BS(r())))
r40: Size(L(x)) -> I(|0|())
r41: Size(N(x,l(),r())) -> +(+(Size(l()),Size(r())),I(|1|()))
r42: WB(L(x)) -> true()
r43: WB(N(x,l(),r())) -> and(if(ge(Size(l()),Size(r())),ge(I(|0|()),-(Size(l()),Size(r()))),ge(I(|0|()),-(Size(r()),Size(l())))),and(WB(l()),WB(r())))

The set of usable rules consists of

  r1, r9, r10, r11, r12, r13, r14

Take the reduction pair:

  matrix interpretations:
  
    carrier: N^4
    order: lexicographic order
    interpretations:
      -#_A(x1,x2) = ((1,0,0,0),(0,0,0,0),(0,0,0,0),(1,0,0,0)) x1 + ((1,0,0,0),(1,1,0,0),(1,1,0,0),(0,0,0,0)) x2
      O_A(x1) = ((1,0,0,0),(1,1,0,0),(1,0,1,0),(1,1,0,0)) x1 + (7,10,6,0)
      I_A(x1) = ((1,0,0,0),(0,0,0,0),(0,0,0,0),(1,1,0,0)) x1 + (4,1,1,0)
      -_A(x1,x2) = ((1,0,0,0),(1,1,0,0),(0,0,0,0),(0,1,1,0)) x1 + ((1,0,0,0),(1,1,0,0),(1,1,1,0),(0,1,0,0)) x2 + (1,27,2,1)
      |1|_A() = (1,1,1,1)
      |0|_A() = (4,1,1,4)

The next rules are strictly ordered:

  p1, p2, p3, p4, p5

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: ge#(O(x),O(y)) -> ge#(x,y)
p2: ge#(I(x),I(y)) -> ge#(x,y)
p3: ge#(I(x),O(y)) -> ge#(x,y)
p4: ge#(O(x),I(y)) -> ge#(y,x)

and R consists of:

r1: O(|0|()) -> |0|()
r2: +(|0|(),x) -> x
r3: +(x,|0|()) -> x
r4: +(O(x),O(y)) -> O(+(x,y))
r5: +(O(x),I(y)) -> I(+(x,y))
r6: +(I(x),O(y)) -> I(+(x,y))
r7: +(I(x),I(y)) -> O(+(+(x,y),I(|0|())))
r8: +(x,+(y,z)) -> +(+(x,y),z)
r9: -(x,|0|()) -> x
r10: -(|0|(),x) -> |0|()
r11: -(O(x),O(y)) -> O(-(x,y))
r12: -(O(x),I(y)) -> I(-(-(x,y),I(|1|())))
r13: -(I(x),O(y)) -> I(-(x,y))
r14: -(I(x),I(y)) -> O(-(x,y))
r15: not(true()) -> false()
r16: not(false()) -> true()
r17: and(x,true()) -> x
r18: and(x,false()) -> false()
r19: if(true(),x,y) -> x
r20: if(false(),x,y) -> y
r21: ge(O(x),O(y)) -> ge(x,y)
r22: ge(O(x),I(y)) -> not(ge(y,x))
r23: ge(I(x),O(y)) -> ge(x,y)
r24: ge(I(x),I(y)) -> ge(x,y)
r25: ge(x,|0|()) -> true()
r26: ge(|0|(),O(x)) -> ge(|0|(),x)
r27: ge(|0|(),I(x)) -> false()
r28: |Log'|(|0|()) -> |0|()
r29: |Log'|(I(x)) -> +(|Log'|(x),I(|0|()))
r30: |Log'|(O(x)) -> if(ge(x,I(|0|())),+(|Log'|(x),I(|0|())),|0|())
r31: Log(x) -> -(|Log'|(x),I(|0|()))
r32: Val(L(x)) -> x
r33: Val(N(x,l(),r())) -> x
r34: Min(L(x)) -> x
r35: Min(N(x,l(),r())) -> Min(l())
r36: Max(L(x)) -> x
r37: Max(N(x,l(),r())) -> Max(r())
r38: BS(L(x)) -> true()
r39: BS(N(x,l(),r())) -> and(and(ge(x,Max(l())),ge(Min(r()),x)),and(BS(l()),BS(r())))
r40: Size(L(x)) -> I(|0|())
r41: Size(N(x,l(),r())) -> +(+(Size(l()),Size(r())),I(|1|()))
r42: WB(L(x)) -> true()
r43: WB(N(x,l(),r())) -> and(if(ge(Size(l()),Size(r())),ge(I(|0|()),-(Size(l()),Size(r()))),ge(I(|0|()),-(Size(r()),Size(l())))),and(WB(l()),WB(r())))

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  matrix interpretations:
  
    carrier: N^4
    order: lexicographic order
    interpretations:
      ge#_A(x1,x2) = ((1,0,0,0),(0,1,0,0),(0,0,0,0),(1,1,1,0)) x1 + ((1,0,0,0),(0,1,0,0),(0,0,1,0),(0,0,1,1)) x2
      O_A(x1) = ((1,0,0,0),(1,1,0,0),(1,1,1,0),(1,0,1,1)) x1 + (1,1,1,1)
      I_A(x1) = ((1,0,0,0),(1,1,0,0),(0,0,1,0),(1,1,0,1)) x1 + (1,1,1,1)

The next rules are strictly ordered:

  p1, p2, p3, p4

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

-- Reduction pair.

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

p1: ge#(|0|(),O(x)) -> ge#(|0|(),x)

and R consists of:

r1: O(|0|()) -> |0|()
r2: +(|0|(),x) -> x
r3: +(x,|0|()) -> x
r4: +(O(x),O(y)) -> O(+(x,y))
r5: +(O(x),I(y)) -> I(+(x,y))
r6: +(I(x),O(y)) -> I(+(x,y))
r7: +(I(x),I(y)) -> O(+(+(x,y),I(|0|())))
r8: +(x,+(y,z)) -> +(+(x,y),z)
r9: -(x,|0|()) -> x
r10: -(|0|(),x) -> |0|()
r11: -(O(x),O(y)) -> O(-(x,y))
r12: -(O(x),I(y)) -> I(-(-(x,y),I(|1|())))
r13: -(I(x),O(y)) -> I(-(x,y))
r14: -(I(x),I(y)) -> O(-(x,y))
r15: not(true()) -> false()
r16: not(false()) -> true()
r17: and(x,true()) -> x
r18: and(x,false()) -> false()
r19: if(true(),x,y) -> x
r20: if(false(),x,y) -> y
r21: ge(O(x),O(y)) -> ge(x,y)
r22: ge(O(x),I(y)) -> not(ge(y,x))
r23: ge(I(x),O(y)) -> ge(x,y)
r24: ge(I(x),I(y)) -> ge(x,y)
r25: ge(x,|0|()) -> true()
r26: ge(|0|(),O(x)) -> ge(|0|(),x)
r27: ge(|0|(),I(x)) -> false()
r28: |Log'|(|0|()) -> |0|()
r29: |Log'|(I(x)) -> +(|Log'|(x),I(|0|()))
r30: |Log'|(O(x)) -> if(ge(x,I(|0|())),+(|Log'|(x),I(|0|())),|0|())
r31: Log(x) -> -(|Log'|(x),I(|0|()))
r32: Val(L(x)) -> x
r33: Val(N(x,l(),r())) -> x
r34: Min(L(x)) -> x
r35: Min(N(x,l(),r())) -> Min(l())
r36: Max(L(x)) -> x
r37: Max(N(x,l(),r())) -> Max(r())
r38: BS(L(x)) -> true()
r39: BS(N(x,l(),r())) -> and(and(ge(x,Max(l())),ge(Min(r()),x)),and(BS(l()),BS(r())))
r40: Size(L(x)) -> I(|0|())
r41: Size(N(x,l(),r())) -> +(+(Size(l()),Size(r())),I(|1|()))
r42: WB(L(x)) -> true()
r43: WB(N(x,l(),r())) -> and(if(ge(Size(l()),Size(r())),ge(I(|0|()),-(Size(l()),Size(r()))),ge(I(|0|()),-(Size(r()),Size(l())))),and(WB(l()),WB(r())))

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  matrix interpretations:
  
    carrier: N^4
    order: lexicographic order
    interpretations:
      ge#_A(x1,x2) = ((0,0,0,0),(0,0,0,0),(1,0,0,0),(0,1,0,0)) x1 + ((1,0,0,0),(0,1,0,0),(0,0,1,0),(1,1,1,1)) x2
      |0|_A() = (0,0,0,0)
      O_A(x1) = ((1,0,0,0),(1,1,0,0),(1,1,1,0),(1,1,1,1)) x1 + (1,1,1,1)

The next rules are strictly ordered:

  p1

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