Left Termination proof of /tmp/tmplKj724/search

Left Termination of the query pattern search_tree(b) w.r.t. the given Prolog program could successfully be proven:

↳ PROLOG

  ↳ PrologToPiTRSProof

search_tree₁(void₀).
search_tree₁(T) :- search_tree₃(T, underscore, underscore1).
search_tree₃(tree₃(X, void₀, void₀), X, X).
search_tree₃(tree₃(X, void₀, Right), X, Max) :- search_tree₃(Right, Min, Max), less₂(X, Min).
search_tree₃(tree₃(X, Left, void₀), Min, X) :- search_tree₃(Left, Min, Max), less₂(Max, X).
search_tree₃(tree₃(X, Left, Right), Min1, Max2) :- search_tree₃(Left, Min1, Max1), less₂(Max1, X), search_tree₃(Right, Min2, Max2), less₂(X, Min2).
less₂(0₀, s₁(underscore2)).
less₂(s₁(X), s₁(Y)) :- less₂(X, Y).

With regard to the inferred argument filtering the predicates were used in the following modes:
search_tree₁: (b)
search_tree₃: (b,f,f)
less₂: (b,b)
Transforming PROLOG into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:

search_tree_1_in_g₁(void_0) -> search_tree_1_out_g₁(void_0)
search_tree_1_in_g₁(T) -> if_search_tree_1_in_1_g₂(T, search_tree_3_in_gaa₃(T, underscore, underscore1))
search_tree_3_in_gaa₃(tree_3₃(X, void_0, void_0), X, X) -> search_tree_3_out_gaa₃(tree_3₃(X, void_0, void_0), X, X)
search_tree_3_in_gaa₃(tree_3₃(X, void_0, Right), X, Max) -> if_search_tree_3_in_1_gaa₄(X, Right, Max, search_tree_3_in_gaa₃(Right, Min, Max))
search_tree_3_in_gaa₃(tree_3₃(X, Left, void_0), Min, X) -> if_search_tree_3_in_3_gaa₄(X, Left, Min, search_tree_3_in_gaa₃(Left, Min, Max))
search_tree_3_in_gaa₃(tree_3₃(X, Left, Right), Min1, Max2) -> if_search_tree_3_in_5_gaa₆(X, Left, Right, Min1, Max2, search_tree_3_in_gaa₃(Left, Min1, Max1))
if_search_tree_3_in_5_gaa₆(X, Left, Right, Min1, Max2, search_tree_3_out_gaa₃(Left, Min1, Max1)) -> if_search_tree_3_in_6_gaa₇(X, Left, Right, Min1, Max2, Max1, less_2_in_gg₂(Max1, X))
less_2_in_gg₂(0_0, s_1₁(underscore2)) -> less_2_out_gg₂(0_0, s_1₁(underscore2))
less_2_in_gg₂(s_1₁(X), s_1₁(Y)) -> if_less_2_in_1_gg₃(X, Y, less_2_in_gg₂(X, Y))
if_less_2_in_1_gg₃(X, Y, less_2_out_gg₂(X, Y)) -> less_2_out_gg₂(s_1₁(X), s_1₁(Y))
if_search_tree_3_in_6_gaa₇(X, Left, Right, Min1, Max2, Max1, less_2_out_gg₂(Max1, X)) -> if_search_tree_3_in_7_gaa₆(X, Left, Right, Min1, Max2, search_tree_3_in_gaa₃(Right, Min2, Max2))
if_search_tree_3_in_7_gaa₆(X, Left, Right, Min1, Max2, search_tree_3_out_gaa₃(Right, Min2, Max2)) -> if_search_tree_3_in_8_gaa₇(X, Left, Right, Min1, Max2, Min2, less_2_in_gg₂(X, Min2))
if_search_tree_3_in_8_gaa₇(X, Left, Right, Min1, Max2, Min2, less_2_out_gg₂(X, Min2)) -> search_tree_3_out_gaa₃(tree_3₃(X, Left, Right), Min1, Max2)
if_search_tree_3_in_3_gaa₄(X, Left, Min, search_tree_3_out_gaa₃(Left, Min, Max)) -> if_search_tree_3_in_4_gaa₅(X, Left, Min, Max, less_2_in_gg₂(Max, X))
if_search_tree_3_in_4_gaa₅(X, Left, Min, Max, less_2_out_gg₂(Max, X)) -> search_tree_3_out_gaa₃(tree_3₃(X, Left, void_0), Min, X)
if_search_tree_3_in_1_gaa₄(X, Right, Max, search_tree_3_out_gaa₃(Right, Min, Max)) -> if_search_tree_3_in_2_gaa₅(X, Right, Max, Min, less_2_in_gg₂(X, Min))
if_search_tree_3_in_2_gaa₅(X, Right, Max, Min, less_2_out_gg₂(X, Min)) -> search_tree_3_out_gaa₃(tree_3₃(X, void_0, Right), X, Max)
if_search_tree_1_in_1_g₂(T, search_tree_3_out_gaa₃(T, underscore, underscore1)) -> search_tree_1_out_g₁(T)

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of PROLOG

↳ PROLOG

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

Pi-finite rewrite system:
The TRS R consists of the following rules:

search_tree_1_in_g₁(void_0) -> search_tree_1_out_g₁(void_0)
search_tree_1_in_g₁(T) -> if_search_tree_1_in_1_g₂(T, search_tree_3_in_gaa₃(T, underscore, underscore1))
search_tree_3_in_gaa₃(tree_3₃(X, void_0, void_0), X, X) -> search_tree_3_out_gaa₃(tree_3₃(X, void_0, void_0), X, X)
search_tree_3_in_gaa₃(tree_3₃(X, void_0, Right), X, Max) -> if_search_tree_3_in_1_gaa₄(X, Right, Max, search_tree_3_in_gaa₃(Right, Min, Max))
search_tree_3_in_gaa₃(tree_3₃(X, Left, void_0), Min, X) -> if_search_tree_3_in_3_gaa₄(X, Left, Min, search_tree_3_in_gaa₃(Left, Min, Max))
search_tree_3_in_gaa₃(tree_3₃(X, Left, Right), Min1, Max2) -> if_search_tree_3_in_5_gaa₆(X, Left, Right, Min1, Max2, search_tree_3_in_gaa₃(Left, Min1, Max1))
if_search_tree_3_in_5_gaa₆(X, Left, Right, Min1, Max2, search_tree_3_out_gaa₃(Left, Min1, Max1)) -> if_search_tree_3_in_6_gaa₇(X, Left, Right, Min1, Max2, Max1, less_2_in_gg₂(Max1, X))
less_2_in_gg₂(0_0, s_1₁(underscore2)) -> less_2_out_gg₂(0_0, s_1₁(underscore2))
less_2_in_gg₂(s_1₁(X), s_1₁(Y)) -> if_less_2_in_1_gg₃(X, Y, less_2_in_gg₂(X, Y))
if_less_2_in_1_gg₃(X, Y, less_2_out_gg₂(X, Y)) -> less_2_out_gg₂(s_1₁(X), s_1₁(Y))
if_search_tree_3_in_6_gaa₇(X, Left, Right, Min1, Max2, Max1, less_2_out_gg₂(Max1, X)) -> if_search_tree_3_in_7_gaa₆(X, Left, Right, Min1, Max2, search_tree_3_in_gaa₃(Right, Min2, Max2))
if_search_tree_3_in_7_gaa₆(X, Left, Right, Min1, Max2, search_tree_3_out_gaa₃(Right, Min2, Max2)) -> if_search_tree_3_in_8_gaa₇(X, Left, Right, Min1, Max2, Min2, less_2_in_gg₂(X, Min2))
if_search_tree_3_in_8_gaa₇(X, Left, Right, Min1, Max2, Min2, less_2_out_gg₂(X, Min2)) -> search_tree_3_out_gaa₃(tree_3₃(X, Left, Right), Min1, Max2)
if_search_tree_3_in_3_gaa₄(X, Left, Min, search_tree_3_out_gaa₃(Left, Min, Max)) -> if_search_tree_3_in_4_gaa₅(X, Left, Min, Max, less_2_in_gg₂(Max, X))
if_search_tree_3_in_4_gaa₅(X, Left, Min, Max, less_2_out_gg₂(Max, X)) -> search_tree_3_out_gaa₃(tree_3₃(X, Left, void_0), Min, X)
if_search_tree_3_in_1_gaa₄(X, Right, Max, search_tree_3_out_gaa₃(Right, Min, Max)) -> if_search_tree_3_in_2_gaa₅(X, Right, Max, Min, less_2_in_gg₂(X, Min))
if_search_tree_3_in_2_gaa₅(X, Right, Max, Min, less_2_out_gg₂(X, Min)) -> search_tree_3_out_gaa₃(tree_3₃(X, void_0, Right), X, Max)
if_search_tree_1_in_1_g₂(T, search_tree_3_out_gaa₃(T, underscore, underscore1)) -> search_tree_1_out_g₁(T)

SEARCH_TREE_1_IN_G₁(T) -> IF_SEARCH_TREE_1_IN_1_G₂(T, search_tree_3_in_gaa₃(T, underscore, underscore1))
SEARCH_TREE_1_IN_G₁(T) -> SEARCH_TREE_3_IN_GAA₃(T, underscore, underscore1)
SEARCH_TREE_3_IN_GAA₃(tree_3₃(X, void_0, Right), X, Max) -> IF_SEARCH_TREE_3_IN_1_GAA₄(X, Right, Max, search_tree_3_in_gaa₃(Right, Min, Max))
SEARCH_TREE_3_IN_GAA₃(tree_3₃(X, void_0, Right), X, Max) -> SEARCH_TREE_3_IN_GAA₃(Right, Min, Max)
SEARCH_TREE_3_IN_GAA₃(tree_3₃(X, Left, void_0), Min, X) -> IF_SEARCH_TREE_3_IN_3_GAA₄(X, Left, Min, search_tree_3_in_gaa₃(Left, Min, Max))
SEARCH_TREE_3_IN_GAA₃(tree_3₃(X, Left, void_0), Min, X) -> SEARCH_TREE_3_IN_GAA₃(Left, Min, Max)
SEARCH_TREE_3_IN_GAA₃(tree_3₃(X, Left, Right), Min1, Max2) -> IF_SEARCH_TREE_3_IN_5_GAA₆(X, Left, Right, Min1, Max2, search_tree_3_in_gaa₃(Left, Min1, Max1))
SEARCH_TREE_3_IN_GAA₃(tree_3₃(X, Left, Right), Min1, Max2) -> SEARCH_TREE_3_IN_GAA₃(Left, Min1, Max1)
IF_SEARCH_TREE_3_IN_5_GAA₆(X, Left, Right, Min1, Max2, search_tree_3_out_gaa₃(Left, Min1, Max1)) -> IF_SEARCH_TREE_3_IN_6_GAA₇(X, Left, Right, Min1, Max2, Max1, less_2_in_gg₂(Max1, X))
IF_SEARCH_TREE_3_IN_5_GAA₆(X, Left, Right, Min1, Max2, search_tree_3_out_gaa₃(Left, Min1, Max1)) -> LESS_2_IN_GG₂(Max1, X)
LESS_2_IN_GG₂(s_1₁(X), s_1₁(Y)) -> IF_LESS_2_IN_1_GG₃(X, Y, less_2_in_gg₂(X, Y))
LESS_2_IN_GG₂(s_1₁(X), s_1₁(Y)) -> LESS_2_IN_GG₂(X, Y)
IF_SEARCH_TREE_3_IN_6_GAA₇(X, Left, Right, Min1, Max2, Max1, less_2_out_gg₂(Max1, X)) -> IF_SEARCH_TREE_3_IN_7_GAA₆(X, Left, Right, Min1, Max2, search_tree_3_in_gaa₃(Right, Min2, Max2))
IF_SEARCH_TREE_3_IN_6_GAA₇(X, Left, Right, Min1, Max2, Max1, less_2_out_gg₂(Max1, X)) -> SEARCH_TREE_3_IN_GAA₃(Right, Min2, Max2)
IF_SEARCH_TREE_3_IN_7_GAA₆(X, Left, Right, Min1, Max2, search_tree_3_out_gaa₃(Right, Min2, Max2)) -> IF_SEARCH_TREE_3_IN_8_GAA₇(X, Left, Right, Min1, Max2, Min2, less_2_in_gg₂(X, Min2))
IF_SEARCH_TREE_3_IN_7_GAA₆(X, Left, Right, Min1, Max2, search_tree_3_out_gaa₃(Right, Min2, Max2)) -> LESS_2_IN_GG₂(X, Min2)
IF_SEARCH_TREE_3_IN_3_GAA₄(X, Left, Min, search_tree_3_out_gaa₃(Left, Min, Max)) -> IF_SEARCH_TREE_3_IN_4_GAA₅(X, Left, Min, Max, less_2_in_gg₂(Max, X))
IF_SEARCH_TREE_3_IN_3_GAA₄(X, Left, Min, search_tree_3_out_gaa₃(Left, Min, Max)) -> LESS_2_IN_GG₂(Max, X)
IF_SEARCH_TREE_3_IN_1_GAA₄(X, Right, Max, search_tree_3_out_gaa₃(Right, Min, Max)) -> IF_SEARCH_TREE_3_IN_2_GAA₅(X, Right, Max, Min, less_2_in_gg₂(X, Min))
IF_SEARCH_TREE_3_IN_1_GAA₄(X, Right, Max, search_tree_3_out_gaa₃(Right, Min, Max)) -> LESS_2_IN_GG₂(X, Min)

The TRS R consists of the following rules:

search_tree_1_in_g₁(void_0) -> search_tree_1_out_g₁(void_0)
search_tree_1_in_g₁(T) -> if_search_tree_1_in_1_g₂(T, search_tree_3_in_gaa₃(T, underscore, underscore1))
search_tree_3_in_gaa₃(tree_3₃(X, void_0, void_0), X, X) -> search_tree_3_out_gaa₃(tree_3₃(X, void_0, void_0), X, X)
search_tree_3_in_gaa₃(tree_3₃(X, void_0, Right), X, Max) -> if_search_tree_3_in_1_gaa₄(X, Right, Max, search_tree_3_in_gaa₃(Right, Min, Max))
search_tree_3_in_gaa₃(tree_3₃(X, Left, void_0), Min, X) -> if_search_tree_3_in_3_gaa₄(X, Left, Min, search_tree_3_in_gaa₃(Left, Min, Max))
search_tree_3_in_gaa₃(tree_3₃(X, Left, Right), Min1, Max2) -> if_search_tree_3_in_5_gaa₆(X, Left, Right, Min1, Max2, search_tree_3_in_gaa₃(Left, Min1, Max1))
if_search_tree_3_in_5_gaa₆(X, Left, Right, Min1, Max2, search_tree_3_out_gaa₃(Left, Min1, Max1)) -> if_search_tree_3_in_6_gaa₇(X, Left, Right, Min1, Max2, Max1, less_2_in_gg₂(Max1, X))
less_2_in_gg₂(0_0, s_1₁(underscore2)) -> less_2_out_gg₂(0_0, s_1₁(underscore2))
less_2_in_gg₂(s_1₁(X), s_1₁(Y)) -> if_less_2_in_1_gg₃(X, Y, less_2_in_gg₂(X, Y))
if_less_2_in_1_gg₃(X, Y, less_2_out_gg₂(X, Y)) -> less_2_out_gg₂(s_1₁(X), s_1₁(Y))
if_search_tree_3_in_6_gaa₇(X, Left, Right, Min1, Max2, Max1, less_2_out_gg₂(Max1, X)) -> if_search_tree_3_in_7_gaa₆(X, Left, Right, Min1, Max2, search_tree_3_in_gaa₃(Right, Min2, Max2))
if_search_tree_3_in_7_gaa₆(X, Left, Right, Min1, Max2, search_tree_3_out_gaa₃(Right, Min2, Max2)) -> if_search_tree_3_in_8_gaa₇(X, Left, Right, Min1, Max2, Min2, less_2_in_gg₂(X, Min2))
if_search_tree_3_in_8_gaa₇(X, Left, Right, Min1, Max2, Min2, less_2_out_gg₂(X, Min2)) -> search_tree_3_out_gaa₃(tree_3₃(X, Left, Right), Min1, Max2)
if_search_tree_3_in_3_gaa₄(X, Left, Min, search_tree_3_out_gaa₃(Left, Min, Max)) -> if_search_tree_3_in_4_gaa₅(X, Left, Min, Max, less_2_in_gg₂(Max, X))
if_search_tree_3_in_4_gaa₅(X, Left, Min, Max, less_2_out_gg₂(Max, X)) -> search_tree_3_out_gaa₃(tree_3₃(X, Left, void_0), Min, X)
if_search_tree_3_in_1_gaa₄(X, Right, Max, search_tree_3_out_gaa₃(Right, Min, Max)) -> if_search_tree_3_in_2_gaa₅(X, Right, Max, Min, less_2_in_gg₂(X, Min))
if_search_tree_3_in_2_gaa₅(X, Right, Max, Min, less_2_out_gg₂(X, Min)) -> search_tree_3_out_gaa₃(tree_3₃(X, void_0, Right), X, Max)
if_search_tree_1_in_1_g₂(T, search_tree_3_out_gaa₃(T, underscore, underscore1)) -> search_tree_1_out_g₁(T)

The argument filtering Pi contains the following mapping:
search_tree_1_in_g₁(x1) = search_tree_1_in_g₁(x1)
void_0 = void_0
tree_3₃(x1, x2, x3) = tree_3₃(x1, x2, x3)
0_0 = 0_0
s_1₁(x1) = s_1₁(x1)
search_tree_1_out_g₁(x1) = search_tree_1_out_g
if_search_tree_1_in_1_g₂(x1, x2) = if_search_tree_1_in_1_g₁(x2)
search_tree_3_in_gaa₃(x1, x2, x3) = search_tree_3_in_gaa₁(x1)
search_tree_3_out_gaa₃(x1, x2, x3) = search_tree_3_out_gaa₂(x2, x3)
if_search_tree_3_in_1_gaa₄(x1, x2, x3, x4) = if_search_tree_3_in_1_gaa₂(x1, x4)
if_search_tree_3_in_3_gaa₄(x1, x2, x3, x4) = if_search_tree_3_in_3_gaa₂(x1, x4)
if_search_tree_3_in_5_gaa₆(x1, x2, x3, x4, x5, x6) = if_search_tree_3_in_5_gaa₃(x1, x3, x6)
if_search_tree_3_in_6_gaa₇(x1, x2, x3, x4, x5, x6, x7) = if_search_tree_3_in_6_gaa₄(x1, x3, x4, x7)
less_2_in_gg₂(x1, x2) = less_2_in_gg₂(x1, x2)
less_2_out_gg₂(x1, x2) = less_2_out_gg
if_less_2_in_1_gg₃(x1, x2, x3) = if_less_2_in_1_gg₁(x3)
if_search_tree_3_in_7_gaa₆(x1, x2, x3, x4, x5, x6) = if_search_tree_3_in_7_gaa₃(x1, x4, x6)
if_search_tree_3_in_8_gaa₇(x1, x2, x3, x4, x5, x6, x7) = if_search_tree_3_in_8_gaa₃(x4, x5, x7)
if_search_tree_3_in_4_gaa₅(x1, x2, x3, x4, x5) = if_search_tree_3_in_4_gaa₃(x1, x3, x5)
if_search_tree_3_in_2_gaa₅(x1, x2, x3, x4, x5) = if_search_tree_3_in_2_gaa₃(x1, x3, x5)
IF_SEARCH_TREE_3_IN_1_GAA₄(x1, x2, x3, x4) = IF_SEARCH_TREE_3_IN_1_GAA₂(x1, x4)
IF_SEARCH_TREE_3_IN_5_GAA₆(x1, x2, x3, x4, x5, x6) = IF_SEARCH_TREE_3_IN_5_GAA₃(x1, x3, x6)
IF_SEARCH_TREE_3_IN_8_GAA₇(x1, x2, x3, x4, x5, x6, x7) = IF_SEARCH_TREE_3_IN_8_GAA₃(x4, x5, x7)
SEARCH_TREE_3_IN_GAA₃(x1, x2, x3) = SEARCH_TREE_3_IN_GAA₁(x1)
IF_SEARCH_TREE_3_IN_6_GAA₇(x1, x2, x3, x4, x5, x6, x7) = IF_SEARCH_TREE_3_IN_6_GAA₄(x1, x3, x4, x7)
IF_SEARCH_TREE_3_IN_3_GAA₄(x1, x2, x3, x4) = IF_SEARCH_TREE_3_IN_3_GAA₂(x1, x4)
IF_SEARCH_TREE_1_IN_1_G₂(x1, x2) = IF_SEARCH_TREE_1_IN_1_G₁(x2)
IF_LESS_2_IN_1_GG₃(x1, x2, x3) = IF_LESS_2_IN_1_GG₁(x3)
IF_SEARCH_TREE_3_IN_4_GAA₅(x1, x2, x3, x4, x5) = IF_SEARCH_TREE_3_IN_4_GAA₃(x1, x3, x5)
IF_SEARCH_TREE_3_IN_2_GAA₅(x1, x2, x3, x4, x5) = IF_SEARCH_TREE_3_IN_2_GAA₃(x1, x3, x5)
IF_SEARCH_TREE_3_IN_7_GAA₆(x1, x2, x3, x4, x5, x6) = IF_SEARCH_TREE_3_IN_7_GAA₃(x1, x4, x6)
SEARCH_TREE_1_IN_G₁(x1) = SEARCH_TREE_1_IN_G₁(x1)
LESS_2_IN_GG₂(x1, x2) = LESS_2_IN_GG₂(x1, x2)

We have to consider all (P,R,Pi)-chains

↳ PROLOG

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

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

SEARCH_TREE_1_IN_G₁(T) -> IF_SEARCH_TREE_1_IN_1_G₂(T, search_tree_3_in_gaa₃(T, underscore, underscore1))
SEARCH_TREE_1_IN_G₁(T) -> SEARCH_TREE_3_IN_GAA₃(T, underscore, underscore1)
SEARCH_TREE_3_IN_GAA₃(tree_3₃(X, void_0, Right), X, Max) -> IF_SEARCH_TREE_3_IN_1_GAA₄(X, Right, Max, search_tree_3_in_gaa₃(Right, Min, Max))
SEARCH_TREE_3_IN_GAA₃(tree_3₃(X, void_0, Right), X, Max) -> SEARCH_TREE_3_IN_GAA₃(Right, Min, Max)
SEARCH_TREE_3_IN_GAA₃(tree_3₃(X, Left, void_0), Min, X) -> IF_SEARCH_TREE_3_IN_3_GAA₄(X, Left, Min, search_tree_3_in_gaa₃(Left, Min, Max))
SEARCH_TREE_3_IN_GAA₃(tree_3₃(X, Left, void_0), Min, X) -> SEARCH_TREE_3_IN_GAA₃(Left, Min, Max)
SEARCH_TREE_3_IN_GAA₃(tree_3₃(X, Left, Right), Min1, Max2) -> IF_SEARCH_TREE_3_IN_5_GAA₆(X, Left, Right, Min1, Max2, search_tree_3_in_gaa₃(Left, Min1, Max1))
SEARCH_TREE_3_IN_GAA₃(tree_3₃(X, Left, Right), Min1, Max2) -> SEARCH_TREE_3_IN_GAA₃(Left, Min1, Max1)
IF_SEARCH_TREE_3_IN_5_GAA₆(X, Left, Right, Min1, Max2, search_tree_3_out_gaa₃(Left, Min1, Max1)) -> IF_SEARCH_TREE_3_IN_6_GAA₇(X, Left, Right, Min1, Max2, Max1, less_2_in_gg₂(Max1, X))
IF_SEARCH_TREE_3_IN_5_GAA₆(X, Left, Right, Min1, Max2, search_tree_3_out_gaa₃(Left, Min1, Max1)) -> LESS_2_IN_GG₂(Max1, X)
LESS_2_IN_GG₂(s_1₁(X), s_1₁(Y)) -> IF_LESS_2_IN_1_GG₃(X, Y, less_2_in_gg₂(X, Y))
LESS_2_IN_GG₂(s_1₁(X), s_1₁(Y)) -> LESS_2_IN_GG₂(X, Y)
IF_SEARCH_TREE_3_IN_6_GAA₇(X, Left, Right, Min1, Max2, Max1, less_2_out_gg₂(Max1, X)) -> IF_SEARCH_TREE_3_IN_7_GAA₆(X, Left, Right, Min1, Max2, search_tree_3_in_gaa₃(Right, Min2, Max2))
IF_SEARCH_TREE_3_IN_6_GAA₇(X, Left, Right, Min1, Max2, Max1, less_2_out_gg₂(Max1, X)) -> SEARCH_TREE_3_IN_GAA₃(Right, Min2, Max2)
IF_SEARCH_TREE_3_IN_7_GAA₆(X, Left, Right, Min1, Max2, search_tree_3_out_gaa₃(Right, Min2, Max2)) -> IF_SEARCH_TREE_3_IN_8_GAA₇(X, Left, Right, Min1, Max2, Min2, less_2_in_gg₂(X, Min2))
IF_SEARCH_TREE_3_IN_7_GAA₆(X, Left, Right, Min1, Max2, search_tree_3_out_gaa₃(Right, Min2, Max2)) -> LESS_2_IN_GG₂(X, Min2)
IF_SEARCH_TREE_3_IN_3_GAA₄(X, Left, Min, search_tree_3_out_gaa₃(Left, Min, Max)) -> IF_SEARCH_TREE_3_IN_4_GAA₅(X, Left, Min, Max, less_2_in_gg₂(Max, X))
IF_SEARCH_TREE_3_IN_3_GAA₄(X, Left, Min, search_tree_3_out_gaa₃(Left, Min, Max)) -> LESS_2_IN_GG₂(Max, X)
IF_SEARCH_TREE_3_IN_1_GAA₄(X, Right, Max, search_tree_3_out_gaa₃(Right, Min, Max)) -> IF_SEARCH_TREE_3_IN_2_GAA₅(X, Right, Max, Min, less_2_in_gg₂(X, Min))
IF_SEARCH_TREE_3_IN_1_GAA₄(X, Right, Max, search_tree_3_out_gaa₃(Right, Min, Max)) -> LESS_2_IN_GG₂(X, Min)

The TRS R consists of the following rules:

search_tree_1_in_g₁(void_0) -> search_tree_1_out_g₁(void_0)
search_tree_1_in_g₁(T) -> if_search_tree_1_in_1_g₂(T, search_tree_3_in_gaa₃(T, underscore, underscore1))
search_tree_3_in_gaa₃(tree_3₃(X, void_0, void_0), X, X) -> search_tree_3_out_gaa₃(tree_3₃(X, void_0, void_0), X, X)
search_tree_3_in_gaa₃(tree_3₃(X, void_0, Right), X, Max) -> if_search_tree_3_in_1_gaa₄(X, Right, Max, search_tree_3_in_gaa₃(Right, Min, Max))
search_tree_3_in_gaa₃(tree_3₃(X, Left, void_0), Min, X) -> if_search_tree_3_in_3_gaa₄(X, Left, Min, search_tree_3_in_gaa₃(Left, Min, Max))
search_tree_3_in_gaa₃(tree_3₃(X, Left, Right), Min1, Max2) -> if_search_tree_3_in_5_gaa₆(X, Left, Right, Min1, Max2, search_tree_3_in_gaa₃(Left, Min1, Max1))
if_search_tree_3_in_5_gaa₆(X, Left, Right, Min1, Max2, search_tree_3_out_gaa₃(Left, Min1, Max1)) -> if_search_tree_3_in_6_gaa₇(X, Left, Right, Min1, Max2, Max1, less_2_in_gg₂(Max1, X))
less_2_in_gg₂(0_0, s_1₁(underscore2)) -> less_2_out_gg₂(0_0, s_1₁(underscore2))
less_2_in_gg₂(s_1₁(X), s_1₁(Y)) -> if_less_2_in_1_gg₃(X, Y, less_2_in_gg₂(X, Y))
if_less_2_in_1_gg₃(X, Y, less_2_out_gg₂(X, Y)) -> less_2_out_gg₂(s_1₁(X), s_1₁(Y))
if_search_tree_3_in_6_gaa₇(X, Left, Right, Min1, Max2, Max1, less_2_out_gg₂(Max1, X)) -> if_search_tree_3_in_7_gaa₆(X, Left, Right, Min1, Max2, search_tree_3_in_gaa₃(Right, Min2, Max2))
if_search_tree_3_in_7_gaa₆(X, Left, Right, Min1, Max2, search_tree_3_out_gaa₃(Right, Min2, Max2)) -> if_search_tree_3_in_8_gaa₇(X, Left, Right, Min1, Max2, Min2, less_2_in_gg₂(X, Min2))
if_search_tree_3_in_8_gaa₇(X, Left, Right, Min1, Max2, Min2, less_2_out_gg₂(X, Min2)) -> search_tree_3_out_gaa₃(tree_3₃(X, Left, Right), Min1, Max2)
if_search_tree_3_in_3_gaa₄(X, Left, Min, search_tree_3_out_gaa₃(Left, Min, Max)) -> if_search_tree_3_in_4_gaa₅(X, Left, Min, Max, less_2_in_gg₂(Max, X))
if_search_tree_3_in_4_gaa₅(X, Left, Min, Max, less_2_out_gg₂(Max, X)) -> search_tree_3_out_gaa₃(tree_3₃(X, Left, void_0), Min, X)
if_search_tree_3_in_1_gaa₄(X, Right, Max, search_tree_3_out_gaa₃(Right, Min, Max)) -> if_search_tree_3_in_2_gaa₅(X, Right, Max, Min, less_2_in_gg₂(X, Min))
if_search_tree_3_in_2_gaa₅(X, Right, Max, Min, less_2_out_gg₂(X, Min)) -> search_tree_3_out_gaa₃(tree_3₃(X, void_0, Right), X, Max)
if_search_tree_1_in_1_g₂(T, search_tree_3_out_gaa₃(T, underscore, underscore1)) -> search_tree_1_out_g₁(T)

↳ PROLOG

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

                ↳ UsableRulesProof

              ↳ PiDP

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

LESS_2_IN_GG₂(s_1₁(X), s_1₁(Y)) -> LESS_2_IN_GG₂(X, Y)

The TRS R consists of the following rules:

search_tree_1_in_g₁(void_0) -> search_tree_1_out_g₁(void_0)
search_tree_1_in_g₁(T) -> if_search_tree_1_in_1_g₂(T, search_tree_3_in_gaa₃(T, underscore, underscore1))
search_tree_3_in_gaa₃(tree_3₃(X, void_0, void_0), X, X) -> search_tree_3_out_gaa₃(tree_3₃(X, void_0, void_0), X, X)
search_tree_3_in_gaa₃(tree_3₃(X, void_0, Right), X, Max) -> if_search_tree_3_in_1_gaa₄(X, Right, Max, search_tree_3_in_gaa₃(Right, Min, Max))
search_tree_3_in_gaa₃(tree_3₃(X, Left, void_0), Min, X) -> if_search_tree_3_in_3_gaa₄(X, Left, Min, search_tree_3_in_gaa₃(Left, Min, Max))
search_tree_3_in_gaa₃(tree_3₃(X, Left, Right), Min1, Max2) -> if_search_tree_3_in_5_gaa₆(X, Left, Right, Min1, Max2, search_tree_3_in_gaa₃(Left, Min1, Max1))
if_search_tree_3_in_5_gaa₆(X, Left, Right, Min1, Max2, search_tree_3_out_gaa₃(Left, Min1, Max1)) -> if_search_tree_3_in_6_gaa₇(X, Left, Right, Min1, Max2, Max1, less_2_in_gg₂(Max1, X))
less_2_in_gg₂(0_0, s_1₁(underscore2)) -> less_2_out_gg₂(0_0, s_1₁(underscore2))
less_2_in_gg₂(s_1₁(X), s_1₁(Y)) -> if_less_2_in_1_gg₃(X, Y, less_2_in_gg₂(X, Y))
if_less_2_in_1_gg₃(X, Y, less_2_out_gg₂(X, Y)) -> less_2_out_gg₂(s_1₁(X), s_1₁(Y))
if_search_tree_3_in_6_gaa₇(X, Left, Right, Min1, Max2, Max1, less_2_out_gg₂(Max1, X)) -> if_search_tree_3_in_7_gaa₆(X, Left, Right, Min1, Max2, search_tree_3_in_gaa₃(Right, Min2, Max2))
if_search_tree_3_in_7_gaa₆(X, Left, Right, Min1, Max2, search_tree_3_out_gaa₃(Right, Min2, Max2)) -> if_search_tree_3_in_8_gaa₇(X, Left, Right, Min1, Max2, Min2, less_2_in_gg₂(X, Min2))
if_search_tree_3_in_8_gaa₇(X, Left, Right, Min1, Max2, Min2, less_2_out_gg₂(X, Min2)) -> search_tree_3_out_gaa₃(tree_3₃(X, Left, Right), Min1, Max2)
if_search_tree_3_in_3_gaa₄(X, Left, Min, search_tree_3_out_gaa₃(Left, Min, Max)) -> if_search_tree_3_in_4_gaa₅(X, Left, Min, Max, less_2_in_gg₂(Max, X))
if_search_tree_3_in_4_gaa₅(X, Left, Min, Max, less_2_out_gg₂(Max, X)) -> search_tree_3_out_gaa₃(tree_3₃(X, Left, void_0), Min, X)
if_search_tree_3_in_1_gaa₄(X, Right, Max, search_tree_3_out_gaa₃(Right, Min, Max)) -> if_search_tree_3_in_2_gaa₅(X, Right, Max, Min, less_2_in_gg₂(X, Min))
if_search_tree_3_in_2_gaa₅(X, Right, Max, Min, less_2_out_gg₂(X, Min)) -> search_tree_3_out_gaa₃(tree_3₃(X, void_0, Right), X, Max)
if_search_tree_1_in_1_g₂(T, search_tree_3_out_gaa₃(T, underscore, underscore1)) -> search_tree_1_out_g₁(T)

↳ PROLOG

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

              ↳ PiDP

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

LESS_2_IN_GG₂(s_1₁(X), s_1₁(Y)) -> LESS_2_IN_GG₂(X, Y)

R is empty.
Pi is empty.
We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem into ordinary QDP problem by application of Pi.

↳ PROLOG

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ QDPSizeChangeProof

              ↳ PiDP

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

LESS_2_IN_GG₂(s_1₁(X), s_1₁(Y)) -> LESS_2_IN_GG₂(X, Y)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
The head symbols of this DP problem are {LESS_2_IN_GG₂}.
By using the subterm criterion together with the size-change analysis we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

LESS_2_IN_GG₂(s_1₁(X), s_1₁(Y)) -> LESS_2_IN_GG₂(X, Y)
The graph contains the following edges 1 > 1, 2 > 2

↳ PROLOG

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

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

SEARCH_TREE_3_IN_GAA₃(tree_3₃(X, Left, Right), Min1, Max2) -> IF_SEARCH_TREE_3_IN_5_GAA₆(X, Left, Right, Min1, Max2, search_tree_3_in_gaa₃(Left, Min1, Max1))
SEARCH_TREE_3_IN_GAA₃(tree_3₃(X, void_0, Right), X, Max) -> SEARCH_TREE_3_IN_GAA₃(Right, Min, Max)
SEARCH_TREE_3_IN_GAA₃(tree_3₃(X, Left, void_0), Min, X) -> SEARCH_TREE_3_IN_GAA₃(Left, Min, Max)
IF_SEARCH_TREE_3_IN_6_GAA₇(X, Left, Right, Min1, Max2, Max1, less_2_out_gg₂(Max1, X)) -> SEARCH_TREE_3_IN_GAA₃(Right, Min2, Max2)
IF_SEARCH_TREE_3_IN_5_GAA₆(X, Left, Right, Min1, Max2, search_tree_3_out_gaa₃(Left, Min1, Max1)) -> IF_SEARCH_TREE_3_IN_6_GAA₇(X, Left, Right, Min1, Max2, Max1, less_2_in_gg₂(Max1, X))
SEARCH_TREE_3_IN_GAA₃(tree_3₃(X, Left, Right), Min1, Max2) -> SEARCH_TREE_3_IN_GAA₃(Left, Min1, Max1)

The TRS R consists of the following rules:

search_tree_1_in_g₁(void_0) -> search_tree_1_out_g₁(void_0)
search_tree_1_in_g₁(T) -> if_search_tree_1_in_1_g₂(T, search_tree_3_in_gaa₃(T, underscore, underscore1))
search_tree_3_in_gaa₃(tree_3₃(X, void_0, void_0), X, X) -> search_tree_3_out_gaa₃(tree_3₃(X, void_0, void_0), X, X)
search_tree_3_in_gaa₃(tree_3₃(X, void_0, Right), X, Max) -> if_search_tree_3_in_1_gaa₄(X, Right, Max, search_tree_3_in_gaa₃(Right, Min, Max))
search_tree_3_in_gaa₃(tree_3₃(X, Left, void_0), Min, X) -> if_search_tree_3_in_3_gaa₄(X, Left, Min, search_tree_3_in_gaa₃(Left, Min, Max))
search_tree_3_in_gaa₃(tree_3₃(X, Left, Right), Min1, Max2) -> if_search_tree_3_in_5_gaa₆(X, Left, Right, Min1, Max2, search_tree_3_in_gaa₃(Left, Min1, Max1))
if_search_tree_3_in_5_gaa₆(X, Left, Right, Min1, Max2, search_tree_3_out_gaa₃(Left, Min1, Max1)) -> if_search_tree_3_in_6_gaa₇(X, Left, Right, Min1, Max2, Max1, less_2_in_gg₂(Max1, X))
less_2_in_gg₂(0_0, s_1₁(underscore2)) -> less_2_out_gg₂(0_0, s_1₁(underscore2))
less_2_in_gg₂(s_1₁(X), s_1₁(Y)) -> if_less_2_in_1_gg₃(X, Y, less_2_in_gg₂(X, Y))
if_less_2_in_1_gg₃(X, Y, less_2_out_gg₂(X, Y)) -> less_2_out_gg₂(s_1₁(X), s_1₁(Y))
if_search_tree_3_in_6_gaa₇(X, Left, Right, Min1, Max2, Max1, less_2_out_gg₂(Max1, X)) -> if_search_tree_3_in_7_gaa₆(X, Left, Right, Min1, Max2, search_tree_3_in_gaa₃(Right, Min2, Max2))
if_search_tree_3_in_7_gaa₆(X, Left, Right, Min1, Max2, search_tree_3_out_gaa₃(Right, Min2, Max2)) -> if_search_tree_3_in_8_gaa₇(X, Left, Right, Min1, Max2, Min2, less_2_in_gg₂(X, Min2))
if_search_tree_3_in_8_gaa₇(X, Left, Right, Min1, Max2, Min2, less_2_out_gg₂(X, Min2)) -> search_tree_3_out_gaa₃(tree_3₃(X, Left, Right), Min1, Max2)
if_search_tree_3_in_3_gaa₄(X, Left, Min, search_tree_3_out_gaa₃(Left, Min, Max)) -> if_search_tree_3_in_4_gaa₅(X, Left, Min, Max, less_2_in_gg₂(Max, X))
if_search_tree_3_in_4_gaa₅(X, Left, Min, Max, less_2_out_gg₂(Max, X)) -> search_tree_3_out_gaa₃(tree_3₃(X, Left, void_0), Min, X)
if_search_tree_3_in_1_gaa₄(X, Right, Max, search_tree_3_out_gaa₃(Right, Min, Max)) -> if_search_tree_3_in_2_gaa₅(X, Right, Max, Min, less_2_in_gg₂(X, Min))
if_search_tree_3_in_2_gaa₅(X, Right, Max, Min, less_2_out_gg₂(X, Min)) -> search_tree_3_out_gaa₃(tree_3₃(X, void_0, Right), X, Max)
if_search_tree_1_in_1_g₂(T, search_tree_3_out_gaa₃(T, underscore, underscore1)) -> search_tree_1_out_g₁(T)

↳ PROLOG

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

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

SEARCH_TREE_3_IN_GAA₃(tree_3₃(X, Left, Right), Min1, Max2) -> IF_SEARCH_TREE_3_IN_5_GAA₆(X, Left, Right, Min1, Max2, search_tree_3_in_gaa₃(Left, Min1, Max1))
SEARCH_TREE_3_IN_GAA₃(tree_3₃(X, void_0, Right), X, Max) -> SEARCH_TREE_3_IN_GAA₃(Right, Min, Max)
SEARCH_TREE_3_IN_GAA₃(tree_3₃(X, Left, void_0), Min, X) -> SEARCH_TREE_3_IN_GAA₃(Left, Min, Max)
IF_SEARCH_TREE_3_IN_6_GAA₇(X, Left, Right, Min1, Max2, Max1, less_2_out_gg₂(Max1, X)) -> SEARCH_TREE_3_IN_GAA₃(Right, Min2, Max2)
IF_SEARCH_TREE_3_IN_5_GAA₆(X, Left, Right, Min1, Max2, search_tree_3_out_gaa₃(Left, Min1, Max1)) -> IF_SEARCH_TREE_3_IN_6_GAA₇(X, Left, Right, Min1, Max2, Max1, less_2_in_gg₂(Max1, X))
SEARCH_TREE_3_IN_GAA₃(tree_3₃(X, Left, Right), Min1, Max2) -> SEARCH_TREE_3_IN_GAA₃(Left, Min1, Max1)

The TRS R consists of the following rules:

search_tree_3_in_gaa₃(tree_3₃(X, void_0, void_0), X, X) -> search_tree_3_out_gaa₃(tree_3₃(X, void_0, void_0), X, X)
search_tree_3_in_gaa₃(tree_3₃(X, void_0, Right), X, Max) -> if_search_tree_3_in_1_gaa₄(X, Right, Max, search_tree_3_in_gaa₃(Right, Min, Max))
search_tree_3_in_gaa₃(tree_3₃(X, Left, void_0), Min, X) -> if_search_tree_3_in_3_gaa₄(X, Left, Min, search_tree_3_in_gaa₃(Left, Min, Max))
search_tree_3_in_gaa₃(tree_3₃(X, Left, Right), Min1, Max2) -> if_search_tree_3_in_5_gaa₆(X, Left, Right, Min1, Max2, search_tree_3_in_gaa₃(Left, Min1, Max1))
less_2_in_gg₂(0_0, s_1₁(underscore2)) -> less_2_out_gg₂(0_0, s_1₁(underscore2))
less_2_in_gg₂(s_1₁(X), s_1₁(Y)) -> if_less_2_in_1_gg₃(X, Y, less_2_in_gg₂(X, Y))
if_search_tree_3_in_1_gaa₄(X, Right, Max, search_tree_3_out_gaa₃(Right, Min, Max)) -> if_search_tree_3_in_2_gaa₅(X, Right, Max, Min, less_2_in_gg₂(X, Min))
if_search_tree_3_in_3_gaa₄(X, Left, Min, search_tree_3_out_gaa₃(Left, Min, Max)) -> if_search_tree_3_in_4_gaa₅(X, Left, Min, Max, less_2_in_gg₂(Max, X))
if_search_tree_3_in_5_gaa₆(X, Left, Right, Min1, Max2, search_tree_3_out_gaa₃(Left, Min1, Max1)) -> if_search_tree_3_in_6_gaa₇(X, Left, Right, Min1, Max2, Max1, less_2_in_gg₂(Max1, X))
if_less_2_in_1_gg₃(X, Y, less_2_out_gg₂(X, Y)) -> less_2_out_gg₂(s_1₁(X), s_1₁(Y))
if_search_tree_3_in_2_gaa₅(X, Right, Max, Min, less_2_out_gg₂(X, Min)) -> search_tree_3_out_gaa₃(tree_3₃(X, void_0, Right), X, Max)
if_search_tree_3_in_4_gaa₅(X, Left, Min, Max, less_2_out_gg₂(Max, X)) -> search_tree_3_out_gaa₃(tree_3₃(X, Left, void_0), Min, X)
if_search_tree_3_in_6_gaa₇(X, Left, Right, Min1, Max2, Max1, less_2_out_gg₂(Max1, X)) -> if_search_tree_3_in_7_gaa₆(X, Left, Right, Min1, Max2, search_tree_3_in_gaa₃(Right, Min2, Max2))
if_search_tree_3_in_7_gaa₆(X, Left, Right, Min1, Max2, search_tree_3_out_gaa₃(Right, Min2, Max2)) -> if_search_tree_3_in_8_gaa₇(X, Left, Right, Min1, Max2, Min2, less_2_in_gg₂(X, Min2))
if_search_tree_3_in_8_gaa₇(X, Left, Right, Min1, Max2, Min2, less_2_out_gg₂(X, Min2)) -> search_tree_3_out_gaa₃(tree_3₃(X, Left, Right), Min1, Max2)

The argument filtering Pi contains the following mapping:
void_0 = void_0
tree_3₃(x1, x2, x3) = tree_3₃(x1, x2, x3)
0_0 = 0_0
s_1₁(x1) = s_1₁(x1)
search_tree_3_in_gaa₃(x1, x2, x3) = search_tree_3_in_gaa₁(x1)
search_tree_3_out_gaa₃(x1, x2, x3) = search_tree_3_out_gaa₂(x2, x3)
if_search_tree_3_in_1_gaa₄(x1, x2, x3, x4) = if_search_tree_3_in_1_gaa₂(x1, x4)
if_search_tree_3_in_3_gaa₄(x1, x2, x3, x4) = if_search_tree_3_in_3_gaa₂(x1, x4)
if_search_tree_3_in_5_gaa₆(x1, x2, x3, x4, x5, x6) = if_search_tree_3_in_5_gaa₃(x1, x3, x6)
if_search_tree_3_in_6_gaa₇(x1, x2, x3, x4, x5, x6, x7) = if_search_tree_3_in_6_gaa₄(x1, x3, x4, x7)
less_2_in_gg₂(x1, x2) = less_2_in_gg₂(x1, x2)
less_2_out_gg₂(x1, x2) = less_2_out_gg
if_less_2_in_1_gg₃(x1, x2, x3) = if_less_2_in_1_gg₁(x3)
if_search_tree_3_in_7_gaa₆(x1, x2, x3, x4, x5, x6) = if_search_tree_3_in_7_gaa₃(x1, x4, x6)
if_search_tree_3_in_8_gaa₇(x1, x2, x3, x4, x5, x6, x7) = if_search_tree_3_in_8_gaa₃(x4, x5, x7)
if_search_tree_3_in_4_gaa₅(x1, x2, x3, x4, x5) = if_search_tree_3_in_4_gaa₃(x1, x3, x5)
if_search_tree_3_in_2_gaa₅(x1, x2, x3, x4, x5) = if_search_tree_3_in_2_gaa₃(x1, x3, x5)
IF_SEARCH_TREE_3_IN_5_GAA₆(x1, x2, x3, x4, x5, x6) = IF_SEARCH_TREE_3_IN_5_GAA₃(x1, x3, x6)
SEARCH_TREE_3_IN_GAA₃(x1, x2, x3) = SEARCH_TREE_3_IN_GAA₁(x1)
IF_SEARCH_TREE_3_IN_6_GAA₇(x1, x2, x3, x4, x5, x6, x7) = IF_SEARCH_TREE_3_IN_6_GAA₄(x1, x3, x4, x7)

We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem into ordinary QDP problem by application of Pi.

↳ PROLOG

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ QDPSizeChangeProof

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

SEARCH_TREE_3_IN_GAA₁(tree_3₃(X, Left, Right)) -> IF_SEARCH_TREE_3_IN_5_GAA₃(X, Right, search_tree_3_in_gaa₁(Left))
SEARCH_TREE_3_IN_GAA₁(tree_3₃(X, void_0, Right)) -> SEARCH_TREE_3_IN_GAA₁(Right)
SEARCH_TREE_3_IN_GAA₁(tree_3₃(X, Left, void_0)) -> SEARCH_TREE_3_IN_GAA₁(Left)
IF_SEARCH_TREE_3_IN_6_GAA₄(X, Right, Min1, less_2_out_gg) -> SEARCH_TREE_3_IN_GAA₁(Right)
IF_SEARCH_TREE_3_IN_5_GAA₃(X, Right, search_tree_3_out_gaa₂(Min1, Max1)) -> IF_SEARCH_TREE_3_IN_6_GAA₄(X, Right, Min1, less_2_in_gg₂(Max1, X))
SEARCH_TREE_3_IN_GAA₁(tree_3₃(X, Left, Right)) -> SEARCH_TREE_3_IN_GAA₁(Left)

The TRS R consists of the following rules:

search_tree_3_in_gaa₁(tree_3₃(X, void_0, void_0)) -> search_tree_3_out_gaa₂(X, X)
search_tree_3_in_gaa₁(tree_3₃(X, void_0, Right)) -> if_search_tree_3_in_1_gaa₂(X, search_tree_3_in_gaa₁(Right))
search_tree_3_in_gaa₁(tree_3₃(X, Left, void_0)) -> if_search_tree_3_in_3_gaa₂(X, search_tree_3_in_gaa₁(Left))
search_tree_3_in_gaa₁(tree_3₃(X, Left, Right)) -> if_search_tree_3_in_5_gaa₃(X, Right, search_tree_3_in_gaa₁(Left))
less_2_in_gg₂(0_0, s_1₁(underscore2)) -> less_2_out_gg
less_2_in_gg₂(s_1₁(X), s_1₁(Y)) -> if_less_2_in_1_gg₁(less_2_in_gg₂(X, Y))
if_search_tree_3_in_1_gaa₂(X, search_tree_3_out_gaa₂(Min, Max)) -> if_search_tree_3_in_2_gaa₃(X, Max, less_2_in_gg₂(X, Min))
if_search_tree_3_in_3_gaa₂(X, search_tree_3_out_gaa₂(Min, Max)) -> if_search_tree_3_in_4_gaa₃(X, Min, less_2_in_gg₂(Max, X))
if_search_tree_3_in_5_gaa₃(X, Right, search_tree_3_out_gaa₂(Min1, Max1)) -> if_search_tree_3_in_6_gaa₄(X, Right, Min1, less_2_in_gg₂(Max1, X))
if_less_2_in_1_gg₁(less_2_out_gg) -> less_2_out_gg
if_search_tree_3_in_2_gaa₃(X, Max, less_2_out_gg) -> search_tree_3_out_gaa₂(X, Max)
if_search_tree_3_in_4_gaa₃(X, Min, less_2_out_gg) -> search_tree_3_out_gaa₂(Min, X)
if_search_tree_3_in_6_gaa₄(X, Right, Min1, less_2_out_gg) -> if_search_tree_3_in_7_gaa₃(X, Min1, search_tree_3_in_gaa₁(Right))
if_search_tree_3_in_7_gaa₃(X, Min1, search_tree_3_out_gaa₂(Min2, Max2)) -> if_search_tree_3_in_8_gaa₃(Min1, Max2, less_2_in_gg₂(X, Min2))
if_search_tree_3_in_8_gaa₃(Min1, Max2, less_2_out_gg) -> search_tree_3_out_gaa₂(Min1, Max2)

The set Q consists of the following terms:

search_tree_3_in_gaa₁(x0)
less_2_in_gg₂(x0, x1)
if_search_tree_3_in_1_gaa₂(x0, x1)
if_search_tree_3_in_3_gaa₂(x0, x1)
if_search_tree_3_in_5_gaa₃(x0, x1, x2)
if_less_2_in_1_gg₁(x0)
if_search_tree_3_in_2_gaa₃(x0, x1, x2)
if_search_tree_3_in_4_gaa₃(x0, x1, x2)
if_search_tree_3_in_6_gaa₄(x0, x1, x2, x3)
if_search_tree_3_in_7_gaa₃(x0, x1, x2)
if_search_tree_3_in_8_gaa₃(x0, x1, x2)

We have to consider all (P,Q,R)-chains.
The head symbols of this DP problem are {IF_SEARCH_TREE_3_IN_5_GAA₃, SEARCH_TREE_3_IN_GAA₁, IF_SEARCH_TREE_3_IN_6_GAA₄}.
By using the subterm criterion together with the size-change analysis we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

IF_SEARCH_TREE_3_IN_5_GAA₃(X, Right, search_tree_3_out_gaa₂(Min1, Max1)) -> IF_SEARCH_TREE_3_IN_6_GAA₄(X, Right, Min1, less_2_in_gg₂(Max1, X))
The graph contains the following edges 1 >= 1, 2 >= 2, 3 > 3
SEARCH_TREE_3_IN_GAA₁(tree_3₃(X, Left, Right)) -> IF_SEARCH_TREE_3_IN_5_GAA₃(X, Right, search_tree_3_in_gaa₁(Left))
The graph contains the following edges 1 > 1, 1 > 2
IF_SEARCH_TREE_3_IN_6_GAA₄(X, Right, Min1, less_2_out_gg) -> SEARCH_TREE_3_IN_GAA₁(Right)
The graph contains the following edges 2 >= 1
SEARCH_TREE_3_IN_GAA₁(tree_3₃(X, void_0, Right)) -> SEARCH_TREE_3_IN_GAA₁(Right)
The graph contains the following edges 1 > 1
SEARCH_TREE_3_IN_GAA₁(tree_3₃(X, Left, void_0)) -> SEARCH_TREE_3_IN_GAA₁(Left)
The graph contains the following edges 1 > 1
SEARCH_TREE_3_IN_GAA₁(tree_3₃(X, Left, Right)) -> SEARCH_TREE_3_IN_GAA₁(Left)
The graph contains the following edges 1 > 1