Termination w.r.t. Q proof of TRS/various14.trs

Termination w.r.t. Q of the following Term Rewriting System could be proven:

Q restricted rewrite system:
The TRS R consists of the following rules:

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)))

Q is empty.

↳ QTRS

  ↳ DependencyPairsProof

Q restricted rewrite system:
The TRS R consists of the following rules:

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)))

Q is empty.

Using Dependency Pairs [1,13] we result in the following initial DP problem:
Q DP problem:
The TRS P consists of the following rules:

-¹₂(I₁(x), I₁(y)) -> O¹₁(-₂(x, y))
SIZE₁(N₃(x, l, r)) -> +¹₂(Size₁(l), Size₁(r))
+¹₂(O₁(x), I₁(y)) -> +¹₂(x, y)
+¹₂(I₁(x), O₁(y)) -> +¹₂(x, y)
+¹₂(x, +₂(y, z)) -> +¹₂(+₂(x, y), z)
BS¹₁(N₃(x, l, r)) -> AND₂(ge₂(x, Max₁(l)), ge₂(Min₁(r), x))
BS¹₁(N₃(x, l, r)) -> MAX₁(l)
WB¹₁(N₃(x, l, r)) -> GE₂(Size₁(l), Size₁(r))
GE₂(0, O₁(x)) -> GE₂(0, x)
SIZE₁(N₃(x, l, r)) -> SIZE₁(l)
+¹₂(I₁(x), I₁(y)) -> +¹₂(+₂(x, y), I₁(0))
WB¹₁(N₃(x, l, r)) -> AND₂(WB₁(l), WB₁(r))
GE₂(I₁(x), I₁(y)) -> GE₂(x, y)
LOG'₁(O₁(x)) -> +¹₂(Log'₁(x), I₁(0))
GE₂(I₁(x), O₁(y)) -> GE₂(x, y)
GE₂(O₁(x), I₁(y)) -> GE₂(y, x)
+¹₂(x, +₂(y, z)) -> +¹₂(x, y)
WB¹₁(N₃(x, l, r)) -> SIZE₁(l)
WB¹₁(N₃(x, l, r)) -> WB¹₁(r)
-¹₂(I₁(x), I₁(y)) -> -¹₂(x, y)
LOG'₁(O₁(x)) -> LOG'₁(x)
-¹₂(I₁(x), O₁(y)) -> -¹₂(x, y)
+¹₂(I₁(x), I₁(y)) -> O¹₁(+₂(+₂(x, y), I₁(0)))
-¹₂(O₁(x), I₁(y)) -> -¹₂(x, y)
-¹₂(O₁(x), O₁(y)) -> -¹₂(x, y)
SIZE₁(N₃(x, l, r)) -> +¹₂(+₂(Size₁(l), Size₁(r)), I₁(1))
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)))
BS¹₁(N₃(x, l, r)) -> BS¹₁(l)
WB¹₁(N₃(x, l, r)) -> -¹₂(Size₁(r), Size₁(l))
WB¹₁(N₃(x, l, r)) -> -¹₂(Size₁(l), Size₁(r))
BS¹₁(N₃(x, l, r)) -> GE₂(Min₁(r), x)
SIZE₁(N₃(x, l, r)) -> SIZE₁(r)
LOG'₁(I₁(x)) -> +¹₂(Log'₁(x), I₁(0))
-¹₂(O₁(x), I₁(y)) -> -¹₂(-₂(x, y), I₁(1))
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))))
GE₂(O₁(x), I₁(y)) -> NOT₁(ge₂(y, x))
WB¹₁(N₃(x, l, r)) -> GE₂(I₁(0), -₂(Size₁(r), Size₁(l)))
WB¹₁(N₃(x, l, r)) -> GE₂(I₁(0), -₂(Size₁(l), Size₁(r)))
LOG'₁(O₁(x)) -> GE₂(x, I₁(0))
LOG₁(x) -> -¹₂(Log'₁(x), I₁(0))
BS¹₁(N₃(x, l, r)) -> BS¹₁(r)
LOG₁(x) -> LOG'₁(x)
BS¹₁(N₃(x, l, r)) -> AND₂(BS₁(l), BS₁(r))
BS¹₁(N₃(x, l, r)) -> AND₂(and₂(ge₂(x, Max₁(l)), ge₂(Min₁(r), x)), and₂(BS₁(l), BS₁(r)))
+¹₂(O₁(x), O₁(y)) -> O¹₁(+₂(x, y))
BS¹₁(N₃(x, l, r)) -> MIN₁(r)
GE₂(O₁(x), O₁(y)) -> GE₂(x, y)
+¹₂(I₁(x), I₁(y)) -> +¹₂(x, y)
WB¹₁(N₃(x, l, r)) -> WB¹₁(l)
WB¹₁(N₃(x, l, r)) -> SIZE₁(r)
BS¹₁(N₃(x, l, r)) -> GE₂(x, Max₁(l))
LOG'₁(O₁(x)) -> IF₃(ge₂(x, I₁(0)), +₂(Log'₁(x), I₁(0)), 0)
-¹₂(O₁(x), O₁(y)) -> O¹₁(-₂(x, y))
MAX₁(N₃(x, l, r)) -> MAX₁(r)
LOG'₁(I₁(x)) -> LOG'₁(x)
MIN₁(N₃(x, l, r)) -> MIN₁(l)
+¹₂(O₁(x), O₁(y)) -> +¹₂(x, y)

The TRS R consists of the following rules:

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)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

-¹₂(I₁(x), I₁(y)) -> O¹₁(-₂(x, y))
SIZE₁(N₃(x, l, r)) -> +¹₂(Size₁(l), Size₁(r))
+¹₂(O₁(x), I₁(y)) -> +¹₂(x, y)
+¹₂(I₁(x), O₁(y)) -> +¹₂(x, y)
+¹₂(x, +₂(y, z)) -> +¹₂(+₂(x, y), z)
BS¹₁(N₃(x, l, r)) -> AND₂(ge₂(x, Max₁(l)), ge₂(Min₁(r), x))
BS¹₁(N₃(x, l, r)) -> MAX₁(l)
WB¹₁(N₃(x, l, r)) -> GE₂(Size₁(l), Size₁(r))
GE₂(0, O₁(x)) -> GE₂(0, x)
SIZE₁(N₃(x, l, r)) -> SIZE₁(l)
+¹₂(I₁(x), I₁(y)) -> +¹₂(+₂(x, y), I₁(0))
WB¹₁(N₃(x, l, r)) -> AND₂(WB₁(l), WB₁(r))
GE₂(I₁(x), I₁(y)) -> GE₂(x, y)
LOG'₁(O₁(x)) -> +¹₂(Log'₁(x), I₁(0))
GE₂(I₁(x), O₁(y)) -> GE₂(x, y)
GE₂(O₁(x), I₁(y)) -> GE₂(y, x)
+¹₂(x, +₂(y, z)) -> +¹₂(x, y)
WB¹₁(N₃(x, l, r)) -> SIZE₁(l)
WB¹₁(N₃(x, l, r)) -> WB¹₁(r)
-¹₂(I₁(x), I₁(y)) -> -¹₂(x, y)
LOG'₁(O₁(x)) -> LOG'₁(x)
-¹₂(I₁(x), O₁(y)) -> -¹₂(x, y)
+¹₂(I₁(x), I₁(y)) -> O¹₁(+₂(+₂(x, y), I₁(0)))
-¹₂(O₁(x), I₁(y)) -> -¹₂(x, y)
-¹₂(O₁(x), O₁(y)) -> -¹₂(x, y)
SIZE₁(N₃(x, l, r)) -> +¹₂(+₂(Size₁(l), Size₁(r)), I₁(1))
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)))
BS¹₁(N₃(x, l, r)) -> BS¹₁(l)
WB¹₁(N₃(x, l, r)) -> -¹₂(Size₁(r), Size₁(l))
WB¹₁(N₃(x, l, r)) -> -¹₂(Size₁(l), Size₁(r))
BS¹₁(N₃(x, l, r)) -> GE₂(Min₁(r), x)
SIZE₁(N₃(x, l, r)) -> SIZE₁(r)
LOG'₁(I₁(x)) -> +¹₂(Log'₁(x), I₁(0))
-¹₂(O₁(x), I₁(y)) -> -¹₂(-₂(x, y), I₁(1))
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))))
GE₂(O₁(x), I₁(y)) -> NOT₁(ge₂(y, x))
WB¹₁(N₃(x, l, r)) -> GE₂(I₁(0), -₂(Size₁(r), Size₁(l)))
WB¹₁(N₃(x, l, r)) -> GE₂(I₁(0), -₂(Size₁(l), Size₁(r)))
LOG'₁(O₁(x)) -> GE₂(x, I₁(0))
LOG₁(x) -> -¹₂(Log'₁(x), I₁(0))
BS¹₁(N₃(x, l, r)) -> BS¹₁(r)
LOG₁(x) -> LOG'₁(x)
BS¹₁(N₃(x, l, r)) -> AND₂(BS₁(l), BS₁(r))
BS¹₁(N₃(x, l, r)) -> AND₂(and₂(ge₂(x, Max₁(l)), ge₂(Min₁(r), x)), and₂(BS₁(l), BS₁(r)))
+¹₂(O₁(x), O₁(y)) -> O¹₁(+₂(x, y))
BS¹₁(N₃(x, l, r)) -> MIN₁(r)
GE₂(O₁(x), O₁(y)) -> GE₂(x, y)
+¹₂(I₁(x), I₁(y)) -> +¹₂(x, y)
WB¹₁(N₃(x, l, r)) -> WB¹₁(l)
WB¹₁(N₃(x, l, r)) -> SIZE₁(r)
BS¹₁(N₃(x, l, r)) -> GE₂(x, Max₁(l))
LOG'₁(O₁(x)) -> IF₃(ge₂(x, I₁(0)), +₂(Log'₁(x), I₁(0)), 0)
-¹₂(O₁(x), O₁(y)) -> O¹₁(-₂(x, y))
MAX₁(N₃(x, l, r)) -> MAX₁(r)
LOG'₁(I₁(x)) -> LOG'₁(x)
MIN₁(N₃(x, l, r)) -> MIN₁(l)
+¹₂(O₁(x), O₁(y)) -> +¹₂(x, y)

The TRS R consists of the following rules:

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)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [13,14,18] contains 5 SCCs with 38 less nodes.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

            ↳ QDPOrderProof

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

GE₂(0, O₁(x)) -> GE₂(0, x)

The TRS R consists of the following rules:

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)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].

The following pairs can be oriented strictly and are deleted.

GE₂(0, O₁(x)) -> GE₂(0, x)

The remaining pairs can at least be oriented weakly.
none
Used ordering: Polynomial interpretation [21]:

POL(0) = 0
POL(GE₂(x₁, x₂)) = x₂
POL(O₁(x₁)) = 1 + x₁

The following usable rules [14] were oriented: none

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

            ↳ QDPOrderProof

              ↳ QDP

                ↳ PisEmptyProof

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

Q DP problem:
P is empty.
The TRS R consists of the following rules:

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)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

          ↳ QDP

          ↳ QDP

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

GE₂(I₁(x), I₁(y)) -> GE₂(x, y)
GE₂(I₁(x), O₁(y)) -> GE₂(x, y)
GE₂(O₁(x), I₁(y)) -> GE₂(y, x)
GE₂(O₁(x), O₁(y)) -> GE₂(x, y)

The TRS R consists of the following rules:

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)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].

The following pairs can be oriented strictly and are deleted.

GE₂(I₁(x), I₁(y)) -> GE₂(x, y)
GE₂(I₁(x), O₁(y)) -> GE₂(x, y)
GE₂(O₁(x), I₁(y)) -> GE₂(y, x)

The remaining pairs can at least be oriented weakly.

GE₂(O₁(x), O₁(y)) -> GE₂(x, y)

Used ordering: Polynomial interpretation [21]:

POL(GE₂(x₁, x₂)) = x₁ + x₂
POL(I₁(x₁)) = 1 + x₁
POL(O₁(x₁)) = x₁

The following usable rules [14] were oriented: none

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

              ↳ QDP

                ↳ QDPOrderProof

          ↳ QDP

          ↳ QDP

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

GE₂(O₁(x), O₁(y)) -> GE₂(x, y)

The TRS R consists of the following rules:

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)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].

The following pairs can be oriented strictly and are deleted.

GE₂(O₁(x), O₁(y)) -> GE₂(x, y)

The remaining pairs can at least be oriented weakly.
none
Used ordering: Polynomial interpretation [21]:

POL(GE₂(x₁, x₂)) = x₂
POL(O₁(x₁)) = 1 + x₁

The following usable rules [14] were oriented: none

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

              ↳ QDP

                ↳ QDPOrderProof

                  ↳ QDP

                    ↳ PisEmptyProof

          ↳ QDP

          ↳ QDP

          ↳ QDP

Q DP problem:
P is empty.
The TRS R consists of the following rules:

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)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

          ↳ QDP

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

-¹₂(I₁(x), I₁(y)) -> -¹₂(x, y)
-¹₂(I₁(x), O₁(y)) -> -¹₂(x, y)
-¹₂(O₁(x), I₁(y)) -> -¹₂(x, y)
-¹₂(O₁(x), O₁(y)) -> -¹₂(x, y)
-¹₂(O₁(x), I₁(y)) -> -¹₂(-₂(x, y), I₁(1))

The TRS R consists of the following rules:

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)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].

The following pairs can be oriented strictly and are deleted.

-¹₂(I₁(x), O₁(y)) -> -¹₂(x, y)
-¹₂(O₁(x), O₁(y)) -> -¹₂(x, y)

The remaining pairs can at least be oriented weakly.

-¹₂(I₁(x), I₁(y)) -> -¹₂(x, y)
-¹₂(O₁(x), I₁(y)) -> -¹₂(x, y)
-¹₂(O₁(x), I₁(y)) -> -¹₂(-₂(x, y), I₁(1))

Used ordering: Polynomial interpretation [21]:

POL(-₂(x₁, x₂)) = 0
POL(-¹₂(x₁, x₂)) = x₂
POL(0) = 0
POL(1) = 0
POL(I₁(x₁)) = x₁
POL(O₁(x₁)) = 1 + x₁

The following usable rules [14] were oriented: none

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

              ↳ QDP

                ↳ QDPOrderProof

          ↳ QDP

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

-¹₂(I₁(x), I₁(y)) -> -¹₂(x, y)
-¹₂(O₁(x), I₁(y)) -> -¹₂(x, y)
-¹₂(O₁(x), I₁(y)) -> -¹₂(-₂(x, y), I₁(1))

The TRS R consists of the following rules:

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)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].

The following pairs can be oriented strictly and are deleted.

-¹₂(I₁(x), I₁(y)) -> -¹₂(x, y)
-¹₂(O₁(x), I₁(y)) -> -¹₂(x, y)

The remaining pairs can at least be oriented weakly.

-¹₂(O₁(x), I₁(y)) -> -¹₂(-₂(x, y), I₁(1))

Used ordering: Polynomial interpretation [21]:

POL(-₂(x₁, x₂)) = 0
POL(-¹₂(x₁, x₂)) = x₂
POL(0) = 0
POL(1) = 0
POL(I₁(x₁)) = 1 + x₁
POL(O₁(x₁)) = 0

The following usable rules [14] were oriented: none

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

              ↳ QDP

                ↳ QDPOrderProof

                  ↳ QDP

                    ↳ QDPOrderProof

          ↳ QDP

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

-¹₂(O₁(x), I₁(y)) -> -¹₂(-₂(x, y), I₁(1))

The TRS R consists of the following rules:

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)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].

The following pairs can be oriented strictly and are deleted.

-¹₂(O₁(x), I₁(y)) -> -¹₂(-₂(x, y), I₁(1))

The remaining pairs can at least be oriented weakly.
none
Used ordering: Polynomial interpretation [21]:

POL(-₂(x₁, x₂)) = x₁
POL(-¹₂(x₁, x₂)) = x₁
POL(0) = 0
POL(1) = 0
POL(I₁(x₁)) = 1 + x₁
POL(O₁(x₁)) = 1 + x₁

The following usable rules [14] were oriented:

-₂(I₁(x), O₁(y)) -> I₁(-₂(x, y))
O₁(0) -> 0
-₂(O₁(x), O₁(y)) -> O₁(-₂(x, y))
-₂(x, 0) -> x
-₂(O₁(x), I₁(y)) -> I₁(-₂(-₂(x, y), I₁(1)))
-₂(0, x) -> 0
-₂(I₁(x), I₁(y)) -> O₁(-₂(x, y))

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

              ↳ QDP

                ↳ QDPOrderProof

                  ↳ QDP

                    ↳ QDPOrderProof

                      ↳ QDP

                        ↳ PisEmptyProof

          ↳ QDP

          ↳ QDP

Q DP problem:
P is empty.
The TRS R consists of the following rules:

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)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

+¹₂(I₁(x), O₁(y)) -> +¹₂(x, y)
+¹₂(O₁(x), I₁(y)) -> +¹₂(x, y)
+¹₂(I₁(x), I₁(y)) -> +¹₂(+₂(x, y), I₁(0))
+¹₂(x, +₂(y, z)) -> +¹₂(x, y)
+¹₂(I₁(x), I₁(y)) -> +¹₂(x, y)
+¹₂(O₁(x), O₁(y)) -> +¹₂(x, y)
+¹₂(x, +₂(y, z)) -> +¹₂(+₂(x, y), z)

The TRS R consists of the following rules:

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)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].

The following pairs can be oriented strictly and are deleted.

+¹₂(I₁(x), O₁(y)) -> +¹₂(x, y)
+¹₂(O₁(x), O₁(y)) -> +¹₂(x, y)

The remaining pairs can at least be oriented weakly.

+¹₂(O₁(x), I₁(y)) -> +¹₂(x, y)
+¹₂(I₁(x), I₁(y)) -> +¹₂(+₂(x, y), I₁(0))
+¹₂(x, +₂(y, z)) -> +¹₂(x, y)
+¹₂(I₁(x), I₁(y)) -> +¹₂(x, y)
+¹₂(x, +₂(y, z)) -> +¹₂(+₂(x, y), z)

Used ordering: Polynomial interpretation [21]:

POL(+₂(x₁, x₂)) = x₁ + x₂
POL(+¹₂(x₁, x₂)) = x₂
POL(0) = 0
POL(I₁(x₁)) = x₁
POL(O₁(x₁)) = 1 + x₁

The following usable rules [14] were oriented: none

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

              ↳ QDP

                ↳ QDPOrderProof

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

+¹₂(O₁(x), I₁(y)) -> +¹₂(x, y)
+¹₂(I₁(x), I₁(y)) -> +¹₂(+₂(x, y), I₁(0))
+¹₂(I₁(x), I₁(y)) -> +¹₂(x, y)
+¹₂(x, +₂(y, z)) -> +¹₂(x, y)
+¹₂(x, +₂(y, z)) -> +¹₂(+₂(x, y), z)

The TRS R consists of the following rules:

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)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].

The following pairs can be oriented strictly and are deleted.

+¹₂(x, +₂(y, z)) -> +¹₂(x, y)
+¹₂(x, +₂(y, z)) -> +¹₂(+₂(x, y), z)

The remaining pairs can at least be oriented weakly.

+¹₂(O₁(x), I₁(y)) -> +¹₂(x, y)
+¹₂(I₁(x), I₁(y)) -> +¹₂(+₂(x, y), I₁(0))
+¹₂(I₁(x), I₁(y)) -> +¹₂(x, y)

Used ordering: Polynomial interpretation [21]:

POL(+₂(x₁, x₂)) = 1 + x₁ + x₂
POL(+¹₂(x₁, x₂)) = x₂
POL(0) = 0
POL(I₁(x₁)) = x₁
POL(O₁(x₁)) = 0

The following usable rules [14] were oriented: none

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

              ↳ QDP

                ↳ QDPOrderProof

                  ↳ QDP

                    ↳ QDPOrderProof

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

+¹₂(O₁(x), I₁(y)) -> +¹₂(x, y)
+¹₂(I₁(x), I₁(y)) -> +¹₂(+₂(x, y), I₁(0))
+¹₂(I₁(x), I₁(y)) -> +¹₂(x, y)

The TRS R consists of the following rules:

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)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].

The following pairs can be oriented strictly and are deleted.

+¹₂(O₁(x), I₁(y)) -> +¹₂(x, y)
+¹₂(I₁(x), I₁(y)) -> +¹₂(x, y)

The remaining pairs can at least be oriented weakly.

+¹₂(I₁(x), I₁(y)) -> +¹₂(+₂(x, y), I₁(0))

Used ordering: Polynomial interpretation [21]:

POL(+₂(x₁, x₂)) = 0
POL(+¹₂(x₁, x₂)) = x₂
POL(0) = 0
POL(I₁(x₁)) = 1 + x₁
POL(O₁(x₁)) = 0

The following usable rules [14] were oriented: none

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

              ↳ QDP

                ↳ QDPOrderProof

                  ↳ QDP

                    ↳ QDPOrderProof

                      ↳ QDP

                        ↳ QDPOrderProof

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

+¹₂(I₁(x), I₁(y)) -> +¹₂(+₂(x, y), I₁(0))

The TRS R consists of the following rules:

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)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].

The following pairs can be oriented strictly and are deleted.

+¹₂(I₁(x), I₁(y)) -> +¹₂(+₂(x, y), I₁(0))

The remaining pairs can at least be oriented weakly.
none
Used ordering: Polynomial interpretation [21]:

POL(+₂(x₁, x₂)) = x₁ + x₂
POL(+¹₂(x₁, x₂)) = x₁ + x₂
POL(0) = 0
POL(I₁(x₁)) = 1 + x₁
POL(O₁(x₁)) = x₁

The following usable rules [14] were oriented:

O₁(0) -> 0
+₂(I₁(x), O₁(y)) -> I₁(+₂(x, y))
+₂(O₁(x), I₁(y)) -> I₁(+₂(x, y))
+₂(I₁(x), I₁(y)) -> O₁(+₂(+₂(x, y), I₁(0)))
+₂(x, 0) -> x
+₂(0, x) -> x
+₂(x, +₂(y, z)) -> +₂(+₂(x, y), z)
+₂(O₁(x), O₁(y)) -> O₁(+₂(x, y))

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

              ↳ QDP

                ↳ QDPOrderProof

                  ↳ QDP

                    ↳ QDPOrderProof

                      ↳ QDP

                        ↳ QDPOrderProof

                          ↳ QDP

                            ↳ PisEmptyProof

          ↳ QDP

Q DP problem:
P is empty.
The TRS R consists of the following rules:

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)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

Q DP problem:
The TRS P consists of the following rules:

LOG'₁(O₁(x)) -> LOG'₁(x)
LOG'₁(I₁(x)) -> LOG'₁(x)

The TRS R consists of the following rules:

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)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].

The following pairs can be oriented strictly and are deleted.

LOG'₁(O₁(x)) -> LOG'₁(x)

The remaining pairs can at least be oriented weakly.

LOG'₁(I₁(x)) -> LOG'₁(x)

Used ordering: Polynomial interpretation [21]:

POL(I₁(x₁)) = x₁
POL(LOG'₁(x₁)) = x₁
POL(O₁(x₁)) = 1 + x₁

The following usable rules [14] were oriented: none

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

              ↳ QDP

                ↳ QDPOrderProof

Q DP problem:
The TRS P consists of the following rules:

LOG'₁(I₁(x)) -> LOG'₁(x)

The TRS R consists of the following rules:

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)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].

The following pairs can be oriented strictly and are deleted.

LOG'₁(I₁(x)) -> LOG'₁(x)

The remaining pairs can at least be oriented weakly.
none
Used ordering: Polynomial interpretation [21]:

POL(I₁(x₁)) = 1 + x₁
POL(LOG'₁(x₁)) = x₁

The following usable rules [14] were oriented: none

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

              ↳ QDP

                ↳ QDPOrderProof

                  ↳ QDP

                    ↳ PisEmptyProof

Q DP problem:
P is empty.
The TRS R consists of the following rules:

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)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.