Left Termination proof of /tmp/tmpqyH-W

Left Termination of the query pattern delete(b,b,f) w.r.t. the given Prolog program could not be shown:

↳ PROLOG

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

delete₃(X, tree₃(X, void₀, Right), Right).
delete₃(X, tree₃(X, Left, void₀), Left).
delete₃(X, tree₃(X, Left, Right), tree₃(Y, Left, Right1)) :- delmin₃(Right, Y, Right1).
delete₃(X, tree₃(Y, Left, Right), tree₃(Y, Left1, Right)) :- less₂(X, Y), delete₃(X, Left, Left1).
delete₃(X, tree₃(Y, Left, Right), tree₃(Y, Left, Right1)) :- less₂(Y, X), delete₃(X, Right, Right1).
delmin₃(tree₃(Y, void₀, Right), Y, Right).
delmin₃(tree₃(X, Left, underscore), Y, tree₃(X, Left1, underscore1)) :- delmin₃(Left, Y, Left1).
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:
delete₃: (b,b,f) (b,f,f)
delmin₃: (f,f,f)
less₂: (b,f) (f,f) (f,b)
Transforming PROLOG into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:

delete_3_in_gga₃(X, tree_3₃(X, void_0, Right), Right) -> delete_3_out_gga₃(X, tree_3₃(X, void_0, Right), Right)
delete_3_in_gga₃(X, tree_3₃(X, Left, void_0), Left) -> delete_3_out_gga₃(X, tree_3₃(X, Left, void_0), Left)
delete_3_in_gga₃(X, tree_3₃(X, Left, Right), tree_3₃(Y, Left, Right1)) -> if_delete_3_in_1_gga₆(X, Left, Right, Y, Right1, delmin_3_in_aaa₃(Right, Y, Right1))
delmin_3_in_aaa₃(tree_3₃(Y, void_0, Right), Y, Right) -> delmin_3_out_aaa₃(tree_3₃(Y, void_0, Right), Y, Right)
delmin_3_in_aaa₃(tree_3₃(X, Left, underscore), Y, tree_3₃(X, Left1, underscore1)) -> if_delmin_3_in_1_aaa₇(X, Left, underscore, Y, Left1, underscore1, delmin_3_in_aaa₃(Left, Y, Left1))
if_delmin_3_in_1_aaa₇(X, Left, underscore, Y, Left1, underscore1, delmin_3_out_aaa₃(Left, Y, Left1)) -> delmin_3_out_aaa₃(tree_3₃(X, Left, underscore), Y, tree_3₃(X, Left1, underscore1))
if_delete_3_in_1_gga₆(X, Left, Right, Y, Right1, delmin_3_out_aaa₃(Right, Y, Right1)) -> delete_3_out_gga₃(X, tree_3₃(X, Left, Right), tree_3₃(Y, Left, Right1))
delete_3_in_gga₃(X, tree_3₃(Y, Left, Right), tree_3₃(Y, Left1, Right)) -> if_delete_3_in_2_gga₆(X, Y, Left, Right, Left1, less_2_in_ga₂(X, Y))
less_2_in_ga₂(0_0, s_1₁(underscore2)) -> less_2_out_ga₂(0_0, s_1₁(underscore2))
less_2_in_ga₂(s_1₁(X), s_1₁(Y)) -> if_less_2_in_1_ga₃(X, Y, less_2_in_aa₂(X, Y))
less_2_in_aa₂(0_0, s_1₁(underscore2)) -> less_2_out_aa₂(0_0, s_1₁(underscore2))
less_2_in_aa₂(s_1₁(X), s_1₁(Y)) -> if_less_2_in_1_aa₃(X, Y, less_2_in_aa₂(X, Y))
if_less_2_in_1_aa₃(X, Y, less_2_out_aa₂(X, Y)) -> less_2_out_aa₂(s_1₁(X), s_1₁(Y))
if_less_2_in_1_ga₃(X, Y, less_2_out_aa₂(X, Y)) -> less_2_out_ga₂(s_1₁(X), s_1₁(Y))
if_delete_3_in_2_gga₆(X, Y, Left, Right, Left1, less_2_out_ga₂(X, Y)) -> if_delete_3_in_3_gga₆(X, Y, Left, Right, Left1, delete_3_in_gaa₃(X, Left, Left1))
delete_3_in_gaa₃(X, tree_3₃(X, void_0, Right), Right) -> delete_3_out_gaa₃(X, tree_3₃(X, void_0, Right), Right)
delete_3_in_gaa₃(X, tree_3₃(X, Left, void_0), Left) -> delete_3_out_gaa₃(X, tree_3₃(X, Left, void_0), Left)
delete_3_in_gaa₃(X, tree_3₃(X, Left, Right), tree_3₃(Y, Left, Right1)) -> if_delete_3_in_1_gaa₆(X, Left, Right, Y, Right1, delmin_3_in_aaa₃(Right, Y, Right1))
if_delete_3_in_1_gaa₆(X, Left, Right, Y, Right1, delmin_3_out_aaa₃(Right, Y, Right1)) -> delete_3_out_gaa₃(X, tree_3₃(X, Left, Right), tree_3₃(Y, Left, Right1))
delete_3_in_gaa₃(X, tree_3₃(Y, Left, Right), tree_3₃(Y, Left1, Right)) -> if_delete_3_in_2_gaa₆(X, Y, Left, Right, Left1, less_2_in_ga₂(X, Y))
if_delete_3_in_2_gaa₆(X, Y, Left, Right, Left1, less_2_out_ga₂(X, Y)) -> if_delete_3_in_3_gaa₆(X, Y, Left, Right, Left1, delete_3_in_gaa₃(X, Left, Left1))
delete_3_in_gaa₃(X, tree_3₃(Y, Left, Right), tree_3₃(Y, Left, Right1)) -> if_delete_3_in_4_gaa₆(X, Y, Left, Right, Right1, less_2_in_ag₂(Y, X))
less_2_in_ag₂(0_0, s_1₁(underscore2)) -> less_2_out_ag₂(0_0, s_1₁(underscore2))
less_2_in_ag₂(s_1₁(X), s_1₁(Y)) -> if_less_2_in_1_ag₃(X, Y, less_2_in_aa₂(X, Y))
if_less_2_in_1_ag₃(X, Y, less_2_out_aa₂(X, Y)) -> less_2_out_ag₂(s_1₁(X), s_1₁(Y))
if_delete_3_in_4_gaa₆(X, Y, Left, Right, Right1, less_2_out_ag₂(Y, X)) -> if_delete_3_in_5_gaa₆(X, Y, Left, Right, Right1, delete_3_in_gaa₃(X, Right, Right1))
if_delete_3_in_5_gaa₆(X, Y, Left, Right, Right1, delete_3_out_gaa₃(X, Right, Right1)) -> delete_3_out_gaa₃(X, tree_3₃(Y, Left, Right), tree_3₃(Y, Left, Right1))
if_delete_3_in_3_gaa₆(X, Y, Left, Right, Left1, delete_3_out_gaa₃(X, Left, Left1)) -> delete_3_out_gaa₃(X, tree_3₃(Y, Left, Right), tree_3₃(Y, Left1, Right))
if_delete_3_in_3_gga₆(X, Y, Left, Right, Left1, delete_3_out_gaa₃(X, Left, Left1)) -> delete_3_out_gga₃(X, tree_3₃(Y, Left, Right), tree_3₃(Y, Left1, Right))
delete_3_in_gga₃(X, tree_3₃(Y, Left, Right), tree_3₃(Y, Left, Right1)) -> if_delete_3_in_4_gga₆(X, Y, Left, Right, Right1, less_2_in_ag₂(Y, X))
if_delete_3_in_4_gga₆(X, Y, Left, Right, Right1, less_2_out_ag₂(Y, X)) -> if_delete_3_in_5_gga₆(X, Y, Left, Right, Right1, delete_3_in_gaa₃(X, Right, Right1))
if_delete_3_in_5_gga₆(X, Y, Left, Right, Right1, delete_3_out_gaa₃(X, Right, Right1)) -> delete_3_out_gga₃(X, tree_3₃(Y, Left, Right), tree_3₃(Y, Left, Right1))

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of PROLOG

↳ PROLOG

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

  ↳ PrologToPiTRSProof

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

delete_3_in_gga₃(X, tree_3₃(X, void_0, Right), Right) -> delete_3_out_gga₃(X, tree_3₃(X, void_0, Right), Right)
delete_3_in_gga₃(X, tree_3₃(X, Left, void_0), Left) -> delete_3_out_gga₃(X, tree_3₃(X, Left, void_0), Left)
delete_3_in_gga₃(X, tree_3₃(X, Left, Right), tree_3₃(Y, Left, Right1)) -> if_delete_3_in_1_gga₆(X, Left, Right, Y, Right1, delmin_3_in_aaa₃(Right, Y, Right1))
delmin_3_in_aaa₃(tree_3₃(Y, void_0, Right), Y, Right) -> delmin_3_out_aaa₃(tree_3₃(Y, void_0, Right), Y, Right)
delmin_3_in_aaa₃(tree_3₃(X, Left, underscore), Y, tree_3₃(X, Left1, underscore1)) -> if_delmin_3_in_1_aaa₇(X, Left, underscore, Y, Left1, underscore1, delmin_3_in_aaa₃(Left, Y, Left1))
if_delmin_3_in_1_aaa₇(X, Left, underscore, Y, Left1, underscore1, delmin_3_out_aaa₃(Left, Y, Left1)) -> delmin_3_out_aaa₃(tree_3₃(X, Left, underscore), Y, tree_3₃(X, Left1, underscore1))
if_delete_3_in_1_gga₆(X, Left, Right, Y, Right1, delmin_3_out_aaa₃(Right, Y, Right1)) -> delete_3_out_gga₃(X, tree_3₃(X, Left, Right), tree_3₃(Y, Left, Right1))
delete_3_in_gga₃(X, tree_3₃(Y, Left, Right), tree_3₃(Y, Left1, Right)) -> if_delete_3_in_2_gga₆(X, Y, Left, Right, Left1, less_2_in_ga₂(X, Y))
less_2_in_ga₂(0_0, s_1₁(underscore2)) -> less_2_out_ga₂(0_0, s_1₁(underscore2))
less_2_in_ga₂(s_1₁(X), s_1₁(Y)) -> if_less_2_in_1_ga₃(X, Y, less_2_in_aa₂(X, Y))
less_2_in_aa₂(0_0, s_1₁(underscore2)) -> less_2_out_aa₂(0_0, s_1₁(underscore2))
less_2_in_aa₂(s_1₁(X), s_1₁(Y)) -> if_less_2_in_1_aa₃(X, Y, less_2_in_aa₂(X, Y))
if_less_2_in_1_aa₃(X, Y, less_2_out_aa₂(X, Y)) -> less_2_out_aa₂(s_1₁(X), s_1₁(Y))
if_less_2_in_1_ga₃(X, Y, less_2_out_aa₂(X, Y)) -> less_2_out_ga₂(s_1₁(X), s_1₁(Y))
if_delete_3_in_2_gga₆(X, Y, Left, Right, Left1, less_2_out_ga₂(X, Y)) -> if_delete_3_in_3_gga₆(X, Y, Left, Right, Left1, delete_3_in_gaa₃(X, Left, Left1))
delete_3_in_gaa₃(X, tree_3₃(X, void_0, Right), Right) -> delete_3_out_gaa₃(X, tree_3₃(X, void_0, Right), Right)
delete_3_in_gaa₃(X, tree_3₃(X, Left, void_0), Left) -> delete_3_out_gaa₃(X, tree_3₃(X, Left, void_0), Left)
delete_3_in_gaa₃(X, tree_3₃(X, Left, Right), tree_3₃(Y, Left, Right1)) -> if_delete_3_in_1_gaa₆(X, Left, Right, Y, Right1, delmin_3_in_aaa₃(Right, Y, Right1))
if_delete_3_in_1_gaa₆(X, Left, Right, Y, Right1, delmin_3_out_aaa₃(Right, Y, Right1)) -> delete_3_out_gaa₃(X, tree_3₃(X, Left, Right), tree_3₃(Y, Left, Right1))
delete_3_in_gaa₃(X, tree_3₃(Y, Left, Right), tree_3₃(Y, Left1, Right)) -> if_delete_3_in_2_gaa₆(X, Y, Left, Right, Left1, less_2_in_ga₂(X, Y))
if_delete_3_in_2_gaa₆(X, Y, Left, Right, Left1, less_2_out_ga₂(X, Y)) -> if_delete_3_in_3_gaa₆(X, Y, Left, Right, Left1, delete_3_in_gaa₃(X, Left, Left1))
delete_3_in_gaa₃(X, tree_3₃(Y, Left, Right), tree_3₃(Y, Left, Right1)) -> if_delete_3_in_4_gaa₆(X, Y, Left, Right, Right1, less_2_in_ag₂(Y, X))
less_2_in_ag₂(0_0, s_1₁(underscore2)) -> less_2_out_ag₂(0_0, s_1₁(underscore2))
less_2_in_ag₂(s_1₁(X), s_1₁(Y)) -> if_less_2_in_1_ag₃(X, Y, less_2_in_aa₂(X, Y))
if_less_2_in_1_ag₃(X, Y, less_2_out_aa₂(X, Y)) -> less_2_out_ag₂(s_1₁(X), s_1₁(Y))
if_delete_3_in_4_gaa₆(X, Y, Left, Right, Right1, less_2_out_ag₂(Y, X)) -> if_delete_3_in_5_gaa₆(X, Y, Left, Right, Right1, delete_3_in_gaa₃(X, Right, Right1))
if_delete_3_in_5_gaa₆(X, Y, Left, Right, Right1, delete_3_out_gaa₃(X, Right, Right1)) -> delete_3_out_gaa₃(X, tree_3₃(Y, Left, Right), tree_3₃(Y, Left, Right1))
if_delete_3_in_3_gaa₆(X, Y, Left, Right, Left1, delete_3_out_gaa₃(X, Left, Left1)) -> delete_3_out_gaa₃(X, tree_3₃(Y, Left, Right), tree_3₃(Y, Left1, Right))
if_delete_3_in_3_gga₆(X, Y, Left, Right, Left1, delete_3_out_gaa₃(X, Left, Left1)) -> delete_3_out_gga₃(X, tree_3₃(Y, Left, Right), tree_3₃(Y, Left1, Right))
delete_3_in_gga₃(X, tree_3₃(Y, Left, Right), tree_3₃(Y, Left, Right1)) -> if_delete_3_in_4_gga₆(X, Y, Left, Right, Right1, less_2_in_ag₂(Y, X))
if_delete_3_in_4_gga₆(X, Y, Left, Right, Right1, less_2_out_ag₂(Y, X)) -> if_delete_3_in_5_gga₆(X, Y, Left, Right, Right1, delete_3_in_gaa₃(X, Right, Right1))
if_delete_3_in_5_gga₆(X, Y, Left, Right, Right1, delete_3_out_gaa₃(X, Right, Right1)) -> delete_3_out_gga₃(X, tree_3₃(Y, Left, Right), tree_3₃(Y, Left, Right1))

DELETE_3_IN_GGA₃(X, tree_3₃(X, Left, Right), tree_3₃(Y, Left, Right1)) -> IF_DELETE_3_IN_1_GGA₆(X, Left, Right, Y, Right1, delmin_3_in_aaa₃(Right, Y, Right1))
DELETE_3_IN_GGA₃(X, tree_3₃(X, Left, Right), tree_3₃(Y, Left, Right1)) -> DELMIN_3_IN_AAA₃(Right, Y, Right1)
DELMIN_3_IN_AAA₃(tree_3₃(X, Left, underscore), Y, tree_3₃(X, Left1, underscore1)) -> IF_DELMIN_3_IN_1_AAA₇(X, Left, underscore, Y, Left1, underscore1, delmin_3_in_aaa₃(Left, Y, Left1))
DELMIN_3_IN_AAA₃(tree_3₃(X, Left, underscore), Y, tree_3₃(X, Left1, underscore1)) -> DELMIN_3_IN_AAA₃(Left, Y, Left1)
DELETE_3_IN_GGA₃(X, tree_3₃(Y, Left, Right), tree_3₃(Y, Left1, Right)) -> IF_DELETE_3_IN_2_GGA₆(X, Y, Left, Right, Left1, less_2_in_ga₂(X, Y))
DELETE_3_IN_GGA₃(X, tree_3₃(Y, Left, Right), tree_3₃(Y, Left1, Right)) -> LESS_2_IN_GA₂(X, Y)
LESS_2_IN_GA₂(s_1₁(X), s_1₁(Y)) -> IF_LESS_2_IN_1_GA₃(X, Y, less_2_in_aa₂(X, Y))
LESS_2_IN_GA₂(s_1₁(X), s_1₁(Y)) -> LESS_2_IN_AA₂(X, Y)
LESS_2_IN_AA₂(s_1₁(X), s_1₁(Y)) -> IF_LESS_2_IN_1_AA₃(X, Y, less_2_in_aa₂(X, Y))
LESS_2_IN_AA₂(s_1₁(X), s_1₁(Y)) -> LESS_2_IN_AA₂(X, Y)
IF_DELETE_3_IN_2_GGA₆(X, Y, Left, Right, Left1, less_2_out_ga₂(X, Y)) -> IF_DELETE_3_IN_3_GGA₆(X, Y, Left, Right, Left1, delete_3_in_gaa₃(X, Left, Left1))
IF_DELETE_3_IN_2_GGA₆(X, Y, Left, Right, Left1, less_2_out_ga₂(X, Y)) -> DELETE_3_IN_GAA₃(X, Left, Left1)
DELETE_3_IN_GAA₃(X, tree_3₃(X, Left, Right), tree_3₃(Y, Left, Right1)) -> IF_DELETE_3_IN_1_GAA₆(X, Left, Right, Y, Right1, delmin_3_in_aaa₃(Right, Y, Right1))
DELETE_3_IN_GAA₃(X, tree_3₃(X, Left, Right), tree_3₃(Y, Left, Right1)) -> DELMIN_3_IN_AAA₃(Right, Y, Right1)
DELETE_3_IN_GAA₃(X, tree_3₃(Y, Left, Right), tree_3₃(Y, Left1, Right)) -> IF_DELETE_3_IN_2_GAA₆(X, Y, Left, Right, Left1, less_2_in_ga₂(X, Y))
DELETE_3_IN_GAA₃(X, tree_3₃(Y, Left, Right), tree_3₃(Y, Left1, Right)) -> LESS_2_IN_GA₂(X, Y)
IF_DELETE_3_IN_2_GAA₆(X, Y, Left, Right, Left1, less_2_out_ga₂(X, Y)) -> IF_DELETE_3_IN_3_GAA₆(X, Y, Left, Right, Left1, delete_3_in_gaa₃(X, Left, Left1))
IF_DELETE_3_IN_2_GAA₆(X, Y, Left, Right, Left1, less_2_out_ga₂(X, Y)) -> DELETE_3_IN_GAA₃(X, Left, Left1)
DELETE_3_IN_GAA₃(X, tree_3₃(Y, Left, Right), tree_3₃(Y, Left, Right1)) -> IF_DELETE_3_IN_4_GAA₆(X, Y, Left, Right, Right1, less_2_in_ag₂(Y, X))
DELETE_3_IN_GAA₃(X, tree_3₃(Y, Left, Right), tree_3₃(Y, Left, Right1)) -> LESS_2_IN_AG₂(Y, X)
LESS_2_IN_AG₂(s_1₁(X), s_1₁(Y)) -> IF_LESS_2_IN_1_AG₃(X, Y, less_2_in_aa₂(X, Y))
LESS_2_IN_AG₂(s_1₁(X), s_1₁(Y)) -> LESS_2_IN_AA₂(X, Y)
IF_DELETE_3_IN_4_GAA₆(X, Y, Left, Right, Right1, less_2_out_ag₂(Y, X)) -> IF_DELETE_3_IN_5_GAA₆(X, Y, Left, Right, Right1, delete_3_in_gaa₃(X, Right, Right1))
IF_DELETE_3_IN_4_GAA₆(X, Y, Left, Right, Right1, less_2_out_ag₂(Y, X)) -> DELETE_3_IN_GAA₃(X, Right, Right1)
DELETE_3_IN_GGA₃(X, tree_3₃(Y, Left, Right), tree_3₃(Y, Left, Right1)) -> IF_DELETE_3_IN_4_GGA₆(X, Y, Left, Right, Right1, less_2_in_ag₂(Y, X))
DELETE_3_IN_GGA₃(X, tree_3₃(Y, Left, Right), tree_3₃(Y, Left, Right1)) -> LESS_2_IN_AG₂(Y, X)
IF_DELETE_3_IN_4_GGA₆(X, Y, Left, Right, Right1, less_2_out_ag₂(Y, X)) -> IF_DELETE_3_IN_5_GGA₆(X, Y, Left, Right, Right1, delete_3_in_gaa₃(X, Right, Right1))
IF_DELETE_3_IN_4_GGA₆(X, Y, Left, Right, Right1, less_2_out_ag₂(Y, X)) -> DELETE_3_IN_GAA₃(X, Right, Right1)

The TRS R consists of the following rules:

delete_3_in_gga₃(X, tree_3₃(X, void_0, Right), Right) -> delete_3_out_gga₃(X, tree_3₃(X, void_0, Right), Right)
delete_3_in_gga₃(X, tree_3₃(X, Left, void_0), Left) -> delete_3_out_gga₃(X, tree_3₃(X, Left, void_0), Left)
delete_3_in_gga₃(X, tree_3₃(X, Left, Right), tree_3₃(Y, Left, Right1)) -> if_delete_3_in_1_gga₆(X, Left, Right, Y, Right1, delmin_3_in_aaa₃(Right, Y, Right1))
delmin_3_in_aaa₃(tree_3₃(Y, void_0, Right), Y, Right) -> delmin_3_out_aaa₃(tree_3₃(Y, void_0, Right), Y, Right)
delmin_3_in_aaa₃(tree_3₃(X, Left, underscore), Y, tree_3₃(X, Left1, underscore1)) -> if_delmin_3_in_1_aaa₇(X, Left, underscore, Y, Left1, underscore1, delmin_3_in_aaa₃(Left, Y, Left1))
if_delmin_3_in_1_aaa₇(X, Left, underscore, Y, Left1, underscore1, delmin_3_out_aaa₃(Left, Y, Left1)) -> delmin_3_out_aaa₃(tree_3₃(X, Left, underscore), Y, tree_3₃(X, Left1, underscore1))
if_delete_3_in_1_gga₆(X, Left, Right, Y, Right1, delmin_3_out_aaa₃(Right, Y, Right1)) -> delete_3_out_gga₃(X, tree_3₃(X, Left, Right), tree_3₃(Y, Left, Right1))
delete_3_in_gga₃(X, tree_3₃(Y, Left, Right), tree_3₃(Y, Left1, Right)) -> if_delete_3_in_2_gga₆(X, Y, Left, Right, Left1, less_2_in_ga₂(X, Y))
less_2_in_ga₂(0_0, s_1₁(underscore2)) -> less_2_out_ga₂(0_0, s_1₁(underscore2))
less_2_in_ga₂(s_1₁(X), s_1₁(Y)) -> if_less_2_in_1_ga₃(X, Y, less_2_in_aa₂(X, Y))
less_2_in_aa₂(0_0, s_1₁(underscore2)) -> less_2_out_aa₂(0_0, s_1₁(underscore2))
less_2_in_aa₂(s_1₁(X), s_1₁(Y)) -> if_less_2_in_1_aa₃(X, Y, less_2_in_aa₂(X, Y))
if_less_2_in_1_aa₃(X, Y, less_2_out_aa₂(X, Y)) -> less_2_out_aa₂(s_1₁(X), s_1₁(Y))
if_less_2_in_1_ga₃(X, Y, less_2_out_aa₂(X, Y)) -> less_2_out_ga₂(s_1₁(X), s_1₁(Y))
if_delete_3_in_2_gga₆(X, Y, Left, Right, Left1, less_2_out_ga₂(X, Y)) -> if_delete_3_in_3_gga₆(X, Y, Left, Right, Left1, delete_3_in_gaa₃(X, Left, Left1))
delete_3_in_gaa₃(X, tree_3₃(X, void_0, Right), Right) -> delete_3_out_gaa₃(X, tree_3₃(X, void_0, Right), Right)
delete_3_in_gaa₃(X, tree_3₃(X, Left, void_0), Left) -> delete_3_out_gaa₃(X, tree_3₃(X, Left, void_0), Left)
delete_3_in_gaa₃(X, tree_3₃(X, Left, Right), tree_3₃(Y, Left, Right1)) -> if_delete_3_in_1_gaa₆(X, Left, Right, Y, Right1, delmin_3_in_aaa₃(Right, Y, Right1))
if_delete_3_in_1_gaa₆(X, Left, Right, Y, Right1, delmin_3_out_aaa₃(Right, Y, Right1)) -> delete_3_out_gaa₃(X, tree_3₃(X, Left, Right), tree_3₃(Y, Left, Right1))
delete_3_in_gaa₃(X, tree_3₃(Y, Left, Right), tree_3₃(Y, Left1, Right)) -> if_delete_3_in_2_gaa₆(X, Y, Left, Right, Left1, less_2_in_ga₂(X, Y))
if_delete_3_in_2_gaa₆(X, Y, Left, Right, Left1, less_2_out_ga₂(X, Y)) -> if_delete_3_in_3_gaa₆(X, Y, Left, Right, Left1, delete_3_in_gaa₃(X, Left, Left1))
delete_3_in_gaa₃(X, tree_3₃(Y, Left, Right), tree_3₃(Y, Left, Right1)) -> if_delete_3_in_4_gaa₆(X, Y, Left, Right, Right1, less_2_in_ag₂(Y, X))
less_2_in_ag₂(0_0, s_1₁(underscore2)) -> less_2_out_ag₂(0_0, s_1₁(underscore2))
less_2_in_ag₂(s_1₁(X), s_1₁(Y)) -> if_less_2_in_1_ag₃(X, Y, less_2_in_aa₂(X, Y))
if_less_2_in_1_ag₃(X, Y, less_2_out_aa₂(X, Y)) -> less_2_out_ag₂(s_1₁(X), s_1₁(Y))
if_delete_3_in_4_gaa₆(X, Y, Left, Right, Right1, less_2_out_ag₂(Y, X)) -> if_delete_3_in_5_gaa₆(X, Y, Left, Right, Right1, delete_3_in_gaa₃(X, Right, Right1))
if_delete_3_in_5_gaa₆(X, Y, Left, Right, Right1, delete_3_out_gaa₃(X, Right, Right1)) -> delete_3_out_gaa₃(X, tree_3₃(Y, Left, Right), tree_3₃(Y, Left, Right1))
if_delete_3_in_3_gaa₆(X, Y, Left, Right, Left1, delete_3_out_gaa₃(X, Left, Left1)) -> delete_3_out_gaa₃(X, tree_3₃(Y, Left, Right), tree_3₃(Y, Left1, Right))
if_delete_3_in_3_gga₆(X, Y, Left, Right, Left1, delete_3_out_gaa₃(X, Left, Left1)) -> delete_3_out_gga₃(X, tree_3₃(Y, Left, Right), tree_3₃(Y, Left1, Right))
delete_3_in_gga₃(X, tree_3₃(Y, Left, Right), tree_3₃(Y, Left, Right1)) -> if_delete_3_in_4_gga₆(X, Y, Left, Right, Right1, less_2_in_ag₂(Y, X))
if_delete_3_in_4_gga₆(X, Y, Left, Right, Right1, less_2_out_ag₂(Y, X)) -> if_delete_3_in_5_gga₆(X, Y, Left, Right, Right1, delete_3_in_gaa₃(X, Right, Right1))
if_delete_3_in_5_gga₆(X, Y, Left, Right, Right1, delete_3_out_gaa₃(X, Right, Right1)) -> delete_3_out_gga₃(X, tree_3₃(Y, Left, Right), tree_3₃(Y, Left, Right1))

The argument filtering Pi contains the following mapping:
delete_3_in_gga₃(x1, x2, x3) = delete_3_in_gga₂(x1, x2)
tree_3₃(x1, x2, x3) = tree_3
void_0 = void_0
0_0 = 0_0
s_1₁(x1) = s_1
delete_3_out_gga₃(x1, x2, x3) = delete_3_out_gga
if_delete_3_in_1_gga₆(x1, x2, x3, x4, x5, x6) = if_delete_3_in_1_gga₁(x6)
delmin_3_in_aaa₃(x1, x2, x3) = delmin_3_in_aaa
delmin_3_out_aaa₃(x1, x2, x3) = delmin_3_out_aaa₁(x1)
if_delmin_3_in_1_aaa₇(x1, x2, x3, x4, x5, x6, x7) = if_delmin_3_in_1_aaa₁(x7)
if_delete_3_in_2_gga₆(x1, x2, x3, x4, x5, x6) = if_delete_3_in_2_gga₂(x1, x6)
less_2_in_ga₂(x1, x2) = less_2_in_ga₁(x1)
less_2_out_ga₂(x1, x2) = less_2_out_ga₁(x2)
if_less_2_in_1_ga₃(x1, x2, x3) = if_less_2_in_1_ga₁(x3)
less_2_in_aa₂(x1, x2) = less_2_in_aa
less_2_out_aa₂(x1, x2) = less_2_out_aa₂(x1, x2)
if_less_2_in_1_aa₃(x1, x2, x3) = if_less_2_in_1_aa₁(x3)
if_delete_3_in_3_gga₆(x1, x2, x3, x4, x5, x6) = if_delete_3_in_3_gga₁(x6)
if_delete_3_in_4_gga₆(x1, x2, x3, x4, x5, x6) = if_delete_3_in_4_gga₂(x1, x6)
less_2_in_ag₂(x1, x2) = less_2_in_ag₁(x2)
less_2_out_ag₂(x1, x2) = less_2_out_ag₁(x1)
if_less_2_in_1_ag₃(x1, x2, x3) = if_less_2_in_1_ag₁(x3)
if_delete_3_in_5_gga₆(x1, x2, x3, x4, x5, x6) = if_delete_3_in_5_gga₁(x6)
delete_3_in_gaa₃(x1, x2, x3) = delete_3_in_gaa₁(x1)
delete_3_out_gaa₃(x1, x2, x3) = delete_3_out_gaa₁(x2)
if_delete_3_in_1_gaa₆(x1, x2, x3, x4, x5, x6) = if_delete_3_in_1_gaa₁(x6)
if_delete_3_in_2_gaa₆(x1, x2, x3, x4, x5, x6) = if_delete_3_in_2_gaa₂(x1, x6)
if_delete_3_in_3_gaa₆(x1, x2, x3, x4, x5, x6) = if_delete_3_in_3_gaa₁(x6)
if_delete_3_in_4_gaa₆(x1, x2, x3, x4, x5, x6) = if_delete_3_in_4_gaa₂(x1, x6)
if_delete_3_in_5_gaa₆(x1, x2, x3, x4, x5, x6) = if_delete_3_in_5_gaa₁(x6)
IF_DELETE_3_IN_1_GAA₆(x1, x2, x3, x4, x5, x6) = IF_DELETE_3_IN_1_GAA₁(x6)
LESS_2_IN_AG₂(x1, x2) = LESS_2_IN_AG₁(x2)
LESS_2_IN_GA₂(x1, x2) = LESS_2_IN_GA₁(x1)
IF_LESS_2_IN_1_AG₃(x1, x2, x3) = IF_LESS_2_IN_1_AG₁(x3)
IF_DELETE_3_IN_4_GGA₆(x1, x2, x3, x4, x5, x6) = IF_DELETE_3_IN_4_GGA₂(x1, x6)
DELMIN_3_IN_AAA₃(x1, x2, x3) = DELMIN_3_IN_AAA
IF_LESS_2_IN_1_AA₃(x1, x2, x3) = IF_LESS_2_IN_1_AA₁(x3)
IF_DELETE_3_IN_5_GAA₆(x1, x2, x3, x4, x5, x6) = IF_DELETE_3_IN_5_GAA₁(x6)
IF_DELETE_3_IN_4_GAA₆(x1, x2, x3, x4, x5, x6) = IF_DELETE_3_IN_4_GAA₂(x1, x6)
IF_DELETE_3_IN_5_GGA₆(x1, x2, x3, x4, x5, x6) = IF_DELETE_3_IN_5_GGA₁(x6)
IF_DELETE_3_IN_1_GGA₆(x1, x2, x3, x4, x5, x6) = IF_DELETE_3_IN_1_GGA₁(x6)
IF_LESS_2_IN_1_GA₃(x1, x2, x3) = IF_LESS_2_IN_1_GA₁(x3)
DELETE_3_IN_GGA₃(x1, x2, x3) = DELETE_3_IN_GGA₂(x1, x2)
DELETE_3_IN_GAA₃(x1, x2, x3) = DELETE_3_IN_GAA₁(x1)
IF_DELETE_3_IN_2_GAA₆(x1, x2, x3, x4, x5, x6) = IF_DELETE_3_IN_2_GAA₂(x1, x6)
LESS_2_IN_AA₂(x1, x2) = LESS_2_IN_AA
IF_DELETE_3_IN_2_GGA₆(x1, x2, x3, x4, x5, x6) = IF_DELETE_3_IN_2_GGA₂(x1, x6)
IF_DELMIN_3_IN_1_AAA₇(x1, x2, x3, x4, x5, x6, x7) = IF_DELMIN_3_IN_1_AAA₁(x7)
IF_DELETE_3_IN_3_GGA₆(x1, x2, x3, x4, x5, x6) = IF_DELETE_3_IN_3_GGA₁(x6)
IF_DELETE_3_IN_3_GAA₆(x1, x2, x3, x4, x5, x6) = IF_DELETE_3_IN_3_GAA₁(x6)

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

↳ PROLOG

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

  ↳ PrologToPiTRSProof

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

DELETE_3_IN_GGA₃(X, tree_3₃(X, Left, Right), tree_3₃(Y, Left, Right1)) -> IF_DELETE_3_IN_1_GGA₆(X, Left, Right, Y, Right1, delmin_3_in_aaa₃(Right, Y, Right1))
DELETE_3_IN_GGA₃(X, tree_3₃(X, Left, Right), tree_3₃(Y, Left, Right1)) -> DELMIN_3_IN_AAA₃(Right, Y, Right1)
DELMIN_3_IN_AAA₃(tree_3₃(X, Left, underscore), Y, tree_3₃(X, Left1, underscore1)) -> IF_DELMIN_3_IN_1_AAA₇(X, Left, underscore, Y, Left1, underscore1, delmin_3_in_aaa₃(Left, Y, Left1))
DELMIN_3_IN_AAA₃(tree_3₃(X, Left, underscore), Y, tree_3₃(X, Left1, underscore1)) -> DELMIN_3_IN_AAA₃(Left, Y, Left1)
DELETE_3_IN_GGA₃(X, tree_3₃(Y, Left, Right), tree_3₃(Y, Left1, Right)) -> IF_DELETE_3_IN_2_GGA₆(X, Y, Left, Right, Left1, less_2_in_ga₂(X, Y))
DELETE_3_IN_GGA₃(X, tree_3₃(Y, Left, Right), tree_3₃(Y, Left1, Right)) -> LESS_2_IN_GA₂(X, Y)
LESS_2_IN_GA₂(s_1₁(X), s_1₁(Y)) -> IF_LESS_2_IN_1_GA₃(X, Y, less_2_in_aa₂(X, Y))
LESS_2_IN_GA₂(s_1₁(X), s_1₁(Y)) -> LESS_2_IN_AA₂(X, Y)
LESS_2_IN_AA₂(s_1₁(X), s_1₁(Y)) -> IF_LESS_2_IN_1_AA₃(X, Y, less_2_in_aa₂(X, Y))
LESS_2_IN_AA₂(s_1₁(X), s_1₁(Y)) -> LESS_2_IN_AA₂(X, Y)
IF_DELETE_3_IN_2_GGA₆(X, Y, Left, Right, Left1, less_2_out_ga₂(X, Y)) -> IF_DELETE_3_IN_3_GGA₆(X, Y, Left, Right, Left1, delete_3_in_gaa₃(X, Left, Left1))
IF_DELETE_3_IN_2_GGA₆(X, Y, Left, Right, Left1, less_2_out_ga₂(X, Y)) -> DELETE_3_IN_GAA₃(X, Left, Left1)
DELETE_3_IN_GAA₃(X, tree_3₃(X, Left, Right), tree_3₃(Y, Left, Right1)) -> IF_DELETE_3_IN_1_GAA₆(X, Left, Right, Y, Right1, delmin_3_in_aaa₃(Right, Y, Right1))
DELETE_3_IN_GAA₃(X, tree_3₃(X, Left, Right), tree_3₃(Y, Left, Right1)) -> DELMIN_3_IN_AAA₃(Right, Y, Right1)
DELETE_3_IN_GAA₃(X, tree_3₃(Y, Left, Right), tree_3₃(Y, Left1, Right)) -> IF_DELETE_3_IN_2_GAA₆(X, Y, Left, Right, Left1, less_2_in_ga₂(X, Y))
DELETE_3_IN_GAA₃(X, tree_3₃(Y, Left, Right), tree_3₃(Y, Left1, Right)) -> LESS_2_IN_GA₂(X, Y)
IF_DELETE_3_IN_2_GAA₆(X, Y, Left, Right, Left1, less_2_out_ga₂(X, Y)) -> IF_DELETE_3_IN_3_GAA₆(X, Y, Left, Right, Left1, delete_3_in_gaa₃(X, Left, Left1))
IF_DELETE_3_IN_2_GAA₆(X, Y, Left, Right, Left1, less_2_out_ga₂(X, Y)) -> DELETE_3_IN_GAA₃(X, Left, Left1)
DELETE_3_IN_GAA₃(X, tree_3₃(Y, Left, Right), tree_3₃(Y, Left, Right1)) -> IF_DELETE_3_IN_4_GAA₆(X, Y, Left, Right, Right1, less_2_in_ag₂(Y, X))
DELETE_3_IN_GAA₃(X, tree_3₃(Y, Left, Right), tree_3₃(Y, Left, Right1)) -> LESS_2_IN_AG₂(Y, X)
LESS_2_IN_AG₂(s_1₁(X), s_1₁(Y)) -> IF_LESS_2_IN_1_AG₃(X, Y, less_2_in_aa₂(X, Y))
LESS_2_IN_AG₂(s_1₁(X), s_1₁(Y)) -> LESS_2_IN_AA₂(X, Y)
IF_DELETE_3_IN_4_GAA₆(X, Y, Left, Right, Right1, less_2_out_ag₂(Y, X)) -> IF_DELETE_3_IN_5_GAA₆(X, Y, Left, Right, Right1, delete_3_in_gaa₃(X, Right, Right1))
IF_DELETE_3_IN_4_GAA₆(X, Y, Left, Right, Right1, less_2_out_ag₂(Y, X)) -> DELETE_3_IN_GAA₃(X, Right, Right1)
DELETE_3_IN_GGA₃(X, tree_3₃(Y, Left, Right), tree_3₃(Y, Left, Right1)) -> IF_DELETE_3_IN_4_GGA₆(X, Y, Left, Right, Right1, less_2_in_ag₂(Y, X))
DELETE_3_IN_GGA₃(X, tree_3₃(Y, Left, Right), tree_3₃(Y, Left, Right1)) -> LESS_2_IN_AG₂(Y, X)
IF_DELETE_3_IN_4_GGA₆(X, Y, Left, Right, Right1, less_2_out_ag₂(Y, X)) -> IF_DELETE_3_IN_5_GGA₆(X, Y, Left, Right, Right1, delete_3_in_gaa₃(X, Right, Right1))
IF_DELETE_3_IN_4_GGA₆(X, Y, Left, Right, Right1, less_2_out_ag₂(Y, X)) -> DELETE_3_IN_GAA₃(X, Right, Right1)

The TRS R consists of the following rules:

delete_3_in_gga₃(X, tree_3₃(X, void_0, Right), Right) -> delete_3_out_gga₃(X, tree_3₃(X, void_0, Right), Right)
delete_3_in_gga₃(X, tree_3₃(X, Left, void_0), Left) -> delete_3_out_gga₃(X, tree_3₃(X, Left, void_0), Left)
delete_3_in_gga₃(X, tree_3₃(X, Left, Right), tree_3₃(Y, Left, Right1)) -> if_delete_3_in_1_gga₆(X, Left, Right, Y, Right1, delmin_3_in_aaa₃(Right, Y, Right1))
delmin_3_in_aaa₃(tree_3₃(Y, void_0, Right), Y, Right) -> delmin_3_out_aaa₃(tree_3₃(Y, void_0, Right), Y, Right)
delmin_3_in_aaa₃(tree_3₃(X, Left, underscore), Y, tree_3₃(X, Left1, underscore1)) -> if_delmin_3_in_1_aaa₇(X, Left, underscore, Y, Left1, underscore1, delmin_3_in_aaa₃(Left, Y, Left1))
if_delmin_3_in_1_aaa₇(X, Left, underscore, Y, Left1, underscore1, delmin_3_out_aaa₃(Left, Y, Left1)) -> delmin_3_out_aaa₃(tree_3₃(X, Left, underscore), Y, tree_3₃(X, Left1, underscore1))
if_delete_3_in_1_gga₆(X, Left, Right, Y, Right1, delmin_3_out_aaa₃(Right, Y, Right1)) -> delete_3_out_gga₃(X, tree_3₃(X, Left, Right), tree_3₃(Y, Left, Right1))
delete_3_in_gga₃(X, tree_3₃(Y, Left, Right), tree_3₃(Y, Left1, Right)) -> if_delete_3_in_2_gga₆(X, Y, Left, Right, Left1, less_2_in_ga₂(X, Y))
less_2_in_ga₂(0_0, s_1₁(underscore2)) -> less_2_out_ga₂(0_0, s_1₁(underscore2))
less_2_in_ga₂(s_1₁(X), s_1₁(Y)) -> if_less_2_in_1_ga₃(X, Y, less_2_in_aa₂(X, Y))
less_2_in_aa₂(0_0, s_1₁(underscore2)) -> less_2_out_aa₂(0_0, s_1₁(underscore2))
less_2_in_aa₂(s_1₁(X), s_1₁(Y)) -> if_less_2_in_1_aa₃(X, Y, less_2_in_aa₂(X, Y))
if_less_2_in_1_aa₃(X, Y, less_2_out_aa₂(X, Y)) -> less_2_out_aa₂(s_1₁(X), s_1₁(Y))
if_less_2_in_1_ga₃(X, Y, less_2_out_aa₂(X, Y)) -> less_2_out_ga₂(s_1₁(X), s_1₁(Y))
if_delete_3_in_2_gga₆(X, Y, Left, Right, Left1, less_2_out_ga₂(X, Y)) -> if_delete_3_in_3_gga₆(X, Y, Left, Right, Left1, delete_3_in_gaa₃(X, Left, Left1))
delete_3_in_gaa₃(X, tree_3₃(X, void_0, Right), Right) -> delete_3_out_gaa₃(X, tree_3₃(X, void_0, Right), Right)
delete_3_in_gaa₃(X, tree_3₃(X, Left, void_0), Left) -> delete_3_out_gaa₃(X, tree_3₃(X, Left, void_0), Left)
delete_3_in_gaa₃(X, tree_3₃(X, Left, Right), tree_3₃(Y, Left, Right1)) -> if_delete_3_in_1_gaa₆(X, Left, Right, Y, Right1, delmin_3_in_aaa₃(Right, Y, Right1))
if_delete_3_in_1_gaa₆(X, Left, Right, Y, Right1, delmin_3_out_aaa₃(Right, Y, Right1)) -> delete_3_out_gaa₃(X, tree_3₃(X, Left, Right), tree_3₃(Y, Left, Right1))
delete_3_in_gaa₃(X, tree_3₃(Y, Left, Right), tree_3₃(Y, Left1, Right)) -> if_delete_3_in_2_gaa₆(X, Y, Left, Right, Left1, less_2_in_ga₂(X, Y))
if_delete_3_in_2_gaa₆(X, Y, Left, Right, Left1, less_2_out_ga₂(X, Y)) -> if_delete_3_in_3_gaa₆(X, Y, Left, Right, Left1, delete_3_in_gaa₃(X, Left, Left1))
delete_3_in_gaa₃(X, tree_3₃(Y, Left, Right), tree_3₃(Y, Left, Right1)) -> if_delete_3_in_4_gaa₆(X, Y, Left, Right, Right1, less_2_in_ag₂(Y, X))
less_2_in_ag₂(0_0, s_1₁(underscore2)) -> less_2_out_ag₂(0_0, s_1₁(underscore2))
less_2_in_ag₂(s_1₁(X), s_1₁(Y)) -> if_less_2_in_1_ag₃(X, Y, less_2_in_aa₂(X, Y))
if_less_2_in_1_ag₃(X, Y, less_2_out_aa₂(X, Y)) -> less_2_out_ag₂(s_1₁(X), s_1₁(Y))
if_delete_3_in_4_gaa₆(X, Y, Left, Right, Right1, less_2_out_ag₂(Y, X)) -> if_delete_3_in_5_gaa₆(X, Y, Left, Right, Right1, delete_3_in_gaa₃(X, Right, Right1))
if_delete_3_in_5_gaa₆(X, Y, Left, Right, Right1, delete_3_out_gaa₃(X, Right, Right1)) -> delete_3_out_gaa₃(X, tree_3₃(Y, Left, Right), tree_3₃(Y, Left, Right1))
if_delete_3_in_3_gaa₆(X, Y, Left, Right, Left1, delete_3_out_gaa₃(X, Left, Left1)) -> delete_3_out_gaa₃(X, tree_3₃(Y, Left, Right), tree_3₃(Y, Left1, Right))
if_delete_3_in_3_gga₆(X, Y, Left, Right, Left1, delete_3_out_gaa₃(X, Left, Left1)) -> delete_3_out_gga₃(X, tree_3₃(Y, Left, Right), tree_3₃(Y, Left1, Right))
delete_3_in_gga₃(X, tree_3₃(Y, Left, Right), tree_3₃(Y, Left, Right1)) -> if_delete_3_in_4_gga₆(X, Y, Left, Right, Right1, less_2_in_ag₂(Y, X))
if_delete_3_in_4_gga₆(X, Y, Left, Right, Right1, less_2_out_ag₂(Y, X)) -> if_delete_3_in_5_gga₆(X, Y, Left, Right, Right1, delete_3_in_gaa₃(X, Right, Right1))
if_delete_3_in_5_gga₆(X, Y, Left, Right, Right1, delete_3_out_gaa₃(X, Right, Right1)) -> delete_3_out_gga₃(X, tree_3₃(Y, Left, Right), tree_3₃(Y, Left, Right1))

↳ PROLOG

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

                ↳ UsableRulesProof

              ↳ PiDP

              ↳ PiDP

  ↳ PrologToPiTRSProof

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

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

The TRS R consists of the following rules:

delete_3_in_gga₃(X, tree_3₃(X, void_0, Right), Right) -> delete_3_out_gga₃(X, tree_3₃(X, void_0, Right), Right)
delete_3_in_gga₃(X, tree_3₃(X, Left, void_0), Left) -> delete_3_out_gga₃(X, tree_3₃(X, Left, void_0), Left)
delete_3_in_gga₃(X, tree_3₃(X, Left, Right), tree_3₃(Y, Left, Right1)) -> if_delete_3_in_1_gga₆(X, Left, Right, Y, Right1, delmin_3_in_aaa₃(Right, Y, Right1))
delmin_3_in_aaa₃(tree_3₃(Y, void_0, Right), Y, Right) -> delmin_3_out_aaa₃(tree_3₃(Y, void_0, Right), Y, Right)
delmin_3_in_aaa₃(tree_3₃(X, Left, underscore), Y, tree_3₃(X, Left1, underscore1)) -> if_delmin_3_in_1_aaa₇(X, Left, underscore, Y, Left1, underscore1, delmin_3_in_aaa₃(Left, Y, Left1))
if_delmin_3_in_1_aaa₇(X, Left, underscore, Y, Left1, underscore1, delmin_3_out_aaa₃(Left, Y, Left1)) -> delmin_3_out_aaa₃(tree_3₃(X, Left, underscore), Y, tree_3₃(X, Left1, underscore1))
if_delete_3_in_1_gga₆(X, Left, Right, Y, Right1, delmin_3_out_aaa₃(Right, Y, Right1)) -> delete_3_out_gga₃(X, tree_3₃(X, Left, Right), tree_3₃(Y, Left, Right1))
delete_3_in_gga₃(X, tree_3₃(Y, Left, Right), tree_3₃(Y, Left1, Right)) -> if_delete_3_in_2_gga₆(X, Y, Left, Right, Left1, less_2_in_ga₂(X, Y))
less_2_in_ga₂(0_0, s_1₁(underscore2)) -> less_2_out_ga₂(0_0, s_1₁(underscore2))
less_2_in_ga₂(s_1₁(X), s_1₁(Y)) -> if_less_2_in_1_ga₃(X, Y, less_2_in_aa₂(X, Y))
less_2_in_aa₂(0_0, s_1₁(underscore2)) -> less_2_out_aa₂(0_0, s_1₁(underscore2))
less_2_in_aa₂(s_1₁(X), s_1₁(Y)) -> if_less_2_in_1_aa₃(X, Y, less_2_in_aa₂(X, Y))
if_less_2_in_1_aa₃(X, Y, less_2_out_aa₂(X, Y)) -> less_2_out_aa₂(s_1₁(X), s_1₁(Y))
if_less_2_in_1_ga₃(X, Y, less_2_out_aa₂(X, Y)) -> less_2_out_ga₂(s_1₁(X), s_1₁(Y))
if_delete_3_in_2_gga₆(X, Y, Left, Right, Left1, less_2_out_ga₂(X, Y)) -> if_delete_3_in_3_gga₆(X, Y, Left, Right, Left1, delete_3_in_gaa₃(X, Left, Left1))
delete_3_in_gaa₃(X, tree_3₃(X, void_0, Right), Right) -> delete_3_out_gaa₃(X, tree_3₃(X, void_0, Right), Right)
delete_3_in_gaa₃(X, tree_3₃(X, Left, void_0), Left) -> delete_3_out_gaa₃(X, tree_3₃(X, Left, void_0), Left)
delete_3_in_gaa₃(X, tree_3₃(X, Left, Right), tree_3₃(Y, Left, Right1)) -> if_delete_3_in_1_gaa₆(X, Left, Right, Y, Right1, delmin_3_in_aaa₃(Right, Y, Right1))
if_delete_3_in_1_gaa₆(X, Left, Right, Y, Right1, delmin_3_out_aaa₃(Right, Y, Right1)) -> delete_3_out_gaa₃(X, tree_3₃(X, Left, Right), tree_3₃(Y, Left, Right1))
delete_3_in_gaa₃(X, tree_3₃(Y, Left, Right), tree_3₃(Y, Left1, Right)) -> if_delete_3_in_2_gaa₆(X, Y, Left, Right, Left1, less_2_in_ga₂(X, Y))
if_delete_3_in_2_gaa₆(X, Y, Left, Right, Left1, less_2_out_ga₂(X, Y)) -> if_delete_3_in_3_gaa₆(X, Y, Left, Right, Left1, delete_3_in_gaa₃(X, Left, Left1))
delete_3_in_gaa₃(X, tree_3₃(Y, Left, Right), tree_3₃(Y, Left, Right1)) -> if_delete_3_in_4_gaa₆(X, Y, Left, Right, Right1, less_2_in_ag₂(Y, X))
less_2_in_ag₂(0_0, s_1₁(underscore2)) -> less_2_out_ag₂(0_0, s_1₁(underscore2))
less_2_in_ag₂(s_1₁(X), s_1₁(Y)) -> if_less_2_in_1_ag₃(X, Y, less_2_in_aa₂(X, Y))
if_less_2_in_1_ag₃(X, Y, less_2_out_aa₂(X, Y)) -> less_2_out_ag₂(s_1₁(X), s_1₁(Y))
if_delete_3_in_4_gaa₆(X, Y, Left, Right, Right1, less_2_out_ag₂(Y, X)) -> if_delete_3_in_5_gaa₆(X, Y, Left, Right, Right1, delete_3_in_gaa₃(X, Right, Right1))
if_delete_3_in_5_gaa₆(X, Y, Left, Right, Right1, delete_3_out_gaa₃(X, Right, Right1)) -> delete_3_out_gaa₃(X, tree_3₃(Y, Left, Right), tree_3₃(Y, Left, Right1))
if_delete_3_in_3_gaa₆(X, Y, Left, Right, Left1, delete_3_out_gaa₃(X, Left, Left1)) -> delete_3_out_gaa₃(X, tree_3₃(Y, Left, Right), tree_3₃(Y, Left1, Right))
if_delete_3_in_3_gga₆(X, Y, Left, Right, Left1, delete_3_out_gaa₃(X, Left, Left1)) -> delete_3_out_gga₃(X, tree_3₃(Y, Left, Right), tree_3₃(Y, Left1, Right))
delete_3_in_gga₃(X, tree_3₃(Y, Left, Right), tree_3₃(Y, Left, Right1)) -> if_delete_3_in_4_gga₆(X, Y, Left, Right, Right1, less_2_in_ag₂(Y, X))
if_delete_3_in_4_gga₆(X, Y, Left, Right, Right1, less_2_out_ag₂(Y, X)) -> if_delete_3_in_5_gga₆(X, Y, Left, Right, Right1, delete_3_in_gaa₃(X, Right, Right1))
if_delete_3_in_5_gga₆(X, Y, Left, Right, Right1, delete_3_out_gaa₃(X, Right, Right1)) -> delete_3_out_gga₃(X, tree_3₃(Y, Left, Right), tree_3₃(Y, Left, Right1))

↳ PROLOG

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

              ↳ PiDP

              ↳ PiDP

  ↳ PrologToPiTRSProof

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

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

R is empty.
The argument filtering Pi contains the following mapping:
s_1₁(x1) = s_1
LESS_2_IN_AA₂(x1, x2) = LESS_2_IN_AA

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

              ↳ PiDP

              ↳ PiDP

  ↳ PrologToPiTRSProof

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

LESS_2_IN_AA -> LESS_2_IN_AA

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_AA}.

↳ PROLOG

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

              ↳ PiDP

  ↳ PrologToPiTRSProof

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

DELMIN_3_IN_AAA₃(tree_3₃(X, Left, underscore), Y, tree_3₃(X, Left1, underscore1)) -> DELMIN_3_IN_AAA₃(Left, Y, Left1)

The TRS R consists of the following rules:

delete_3_in_gga₃(X, tree_3₃(X, void_0, Right), Right) -> delete_3_out_gga₃(X, tree_3₃(X, void_0, Right), Right)
delete_3_in_gga₃(X, tree_3₃(X, Left, void_0), Left) -> delete_3_out_gga₃(X, tree_3₃(X, Left, void_0), Left)
delete_3_in_gga₃(X, tree_3₃(X, Left, Right), tree_3₃(Y, Left, Right1)) -> if_delete_3_in_1_gga₆(X, Left, Right, Y, Right1, delmin_3_in_aaa₃(Right, Y, Right1))
delmin_3_in_aaa₃(tree_3₃(Y, void_0, Right), Y, Right) -> delmin_3_out_aaa₃(tree_3₃(Y, void_0, Right), Y, Right)
delmin_3_in_aaa₃(tree_3₃(X, Left, underscore), Y, tree_3₃(X, Left1, underscore1)) -> if_delmin_3_in_1_aaa₇(X, Left, underscore, Y, Left1, underscore1, delmin_3_in_aaa₃(Left, Y, Left1))
if_delmin_3_in_1_aaa₇(X, Left, underscore, Y, Left1, underscore1, delmin_3_out_aaa₃(Left, Y, Left1)) -> delmin_3_out_aaa₃(tree_3₃(X, Left, underscore), Y, tree_3₃(X, Left1, underscore1))
if_delete_3_in_1_gga₆(X, Left, Right, Y, Right1, delmin_3_out_aaa₃(Right, Y, Right1)) -> delete_3_out_gga₃(X, tree_3₃(X, Left, Right), tree_3₃(Y, Left, Right1))
delete_3_in_gga₃(X, tree_3₃(Y, Left, Right), tree_3₃(Y, Left1, Right)) -> if_delete_3_in_2_gga₆(X, Y, Left, Right, Left1, less_2_in_ga₂(X, Y))
less_2_in_ga₂(0_0, s_1₁(underscore2)) -> less_2_out_ga₂(0_0, s_1₁(underscore2))
less_2_in_ga₂(s_1₁(X), s_1₁(Y)) -> if_less_2_in_1_ga₃(X, Y, less_2_in_aa₂(X, Y))
less_2_in_aa₂(0_0, s_1₁(underscore2)) -> less_2_out_aa₂(0_0, s_1₁(underscore2))
less_2_in_aa₂(s_1₁(X), s_1₁(Y)) -> if_less_2_in_1_aa₃(X, Y, less_2_in_aa₂(X, Y))
if_less_2_in_1_aa₃(X, Y, less_2_out_aa₂(X, Y)) -> less_2_out_aa₂(s_1₁(X), s_1₁(Y))
if_less_2_in_1_ga₃(X, Y, less_2_out_aa₂(X, Y)) -> less_2_out_ga₂(s_1₁(X), s_1₁(Y))
if_delete_3_in_2_gga₆(X, Y, Left, Right, Left1, less_2_out_ga₂(X, Y)) -> if_delete_3_in_3_gga₆(X, Y, Left, Right, Left1, delete_3_in_gaa₃(X, Left, Left1))
delete_3_in_gaa₃(X, tree_3₃(X, void_0, Right), Right) -> delete_3_out_gaa₃(X, tree_3₃(X, void_0, Right), Right)
delete_3_in_gaa₃(X, tree_3₃(X, Left, void_0), Left) -> delete_3_out_gaa₃(X, tree_3₃(X, Left, void_0), Left)
delete_3_in_gaa₃(X, tree_3₃(X, Left, Right), tree_3₃(Y, Left, Right1)) -> if_delete_3_in_1_gaa₆(X, Left, Right, Y, Right1, delmin_3_in_aaa₃(Right, Y, Right1))
if_delete_3_in_1_gaa₆(X, Left, Right, Y, Right1, delmin_3_out_aaa₃(Right, Y, Right1)) -> delete_3_out_gaa₃(X, tree_3₃(X, Left, Right), tree_3₃(Y, Left, Right1))
delete_3_in_gaa₃(X, tree_3₃(Y, Left, Right), tree_3₃(Y, Left1, Right)) -> if_delete_3_in_2_gaa₆(X, Y, Left, Right, Left1, less_2_in_ga₂(X, Y))
if_delete_3_in_2_gaa₆(X, Y, Left, Right, Left1, less_2_out_ga₂(X, Y)) -> if_delete_3_in_3_gaa₆(X, Y, Left, Right, Left1, delete_3_in_gaa₃(X, Left, Left1))
delete_3_in_gaa₃(X, tree_3₃(Y, Left, Right), tree_3₃(Y, Left, Right1)) -> if_delete_3_in_4_gaa₆(X, Y, Left, Right, Right1, less_2_in_ag₂(Y, X))
less_2_in_ag₂(0_0, s_1₁(underscore2)) -> less_2_out_ag₂(0_0, s_1₁(underscore2))
less_2_in_ag₂(s_1₁(X), s_1₁(Y)) -> if_less_2_in_1_ag₃(X, Y, less_2_in_aa₂(X, Y))
if_less_2_in_1_ag₃(X, Y, less_2_out_aa₂(X, Y)) -> less_2_out_ag₂(s_1₁(X), s_1₁(Y))
if_delete_3_in_4_gaa₆(X, Y, Left, Right, Right1, less_2_out_ag₂(Y, X)) -> if_delete_3_in_5_gaa₆(X, Y, Left, Right, Right1, delete_3_in_gaa₃(X, Right, Right1))
if_delete_3_in_5_gaa₆(X, Y, Left, Right, Right1, delete_3_out_gaa₃(X, Right, Right1)) -> delete_3_out_gaa₃(X, tree_3₃(Y, Left, Right), tree_3₃(Y, Left, Right1))
if_delete_3_in_3_gaa₆(X, Y, Left, Right, Left1, delete_3_out_gaa₃(X, Left, Left1)) -> delete_3_out_gaa₃(X, tree_3₃(Y, Left, Right), tree_3₃(Y, Left1, Right))
if_delete_3_in_3_gga₆(X, Y, Left, Right, Left1, delete_3_out_gaa₃(X, Left, Left1)) -> delete_3_out_gga₃(X, tree_3₃(Y, Left, Right), tree_3₃(Y, Left1, Right))
delete_3_in_gga₃(X, tree_3₃(Y, Left, Right), tree_3₃(Y, Left, Right1)) -> if_delete_3_in_4_gga₆(X, Y, Left, Right, Right1, less_2_in_ag₂(Y, X))
if_delete_3_in_4_gga₆(X, Y, Left, Right, Right1, less_2_out_ag₂(Y, X)) -> if_delete_3_in_5_gga₆(X, Y, Left, Right, Right1, delete_3_in_gaa₃(X, Right, Right1))
if_delete_3_in_5_gga₆(X, Y, Left, Right, Right1, delete_3_out_gaa₃(X, Right, Right1)) -> delete_3_out_gga₃(X, tree_3₃(Y, Left, Right), tree_3₃(Y, Left, Right1))

↳ PROLOG

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

              ↳ PiDP

  ↳ PrologToPiTRSProof

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

DELMIN_3_IN_AAA₃(tree_3₃(X, Left, underscore), Y, tree_3₃(X, Left1, underscore1)) -> DELMIN_3_IN_AAA₃(Left, Y, Left1)

R is empty.
The argument filtering Pi contains the following mapping:
tree_3₃(x1, x2, x3) = tree_3
DELMIN_3_IN_AAA₃(x1, x2, x3) = DELMIN_3_IN_AAA

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

              ↳ PiDP

  ↳ PrologToPiTRSProof

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

DELMIN_3_IN_AAA -> DELMIN_3_IN_AAA

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
The head symbols of this DP problem are {DELMIN_3_IN_AAA}.

↳ PROLOG

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

  ↳ PrologToPiTRSProof

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

DELETE_3_IN_GAA₃(X, tree_3₃(Y, Left, Right), tree_3₃(Y, Left1, Right)) -> IF_DELETE_3_IN_2_GAA₆(X, Y, Left, Right, Left1, less_2_in_ga₂(X, Y))
DELETE_3_IN_GAA₃(X, tree_3₃(Y, Left, Right), tree_3₃(Y, Left, Right1)) -> IF_DELETE_3_IN_4_GAA₆(X, Y, Left, Right, Right1, less_2_in_ag₂(Y, X))
IF_DELETE_3_IN_4_GAA₆(X, Y, Left, Right, Right1, less_2_out_ag₂(Y, X)) -> DELETE_3_IN_GAA₃(X, Right, Right1)
IF_DELETE_3_IN_2_GAA₆(X, Y, Left, Right, Left1, less_2_out_ga₂(X, Y)) -> DELETE_3_IN_GAA₃(X, Left, Left1)

The TRS R consists of the following rules:

delete_3_in_gga₃(X, tree_3₃(X, void_0, Right), Right) -> delete_3_out_gga₃(X, tree_3₃(X, void_0, Right), Right)
delete_3_in_gga₃(X, tree_3₃(X, Left, void_0), Left) -> delete_3_out_gga₃(X, tree_3₃(X, Left, void_0), Left)
delete_3_in_gga₃(X, tree_3₃(X, Left, Right), tree_3₃(Y, Left, Right1)) -> if_delete_3_in_1_gga₆(X, Left, Right, Y, Right1, delmin_3_in_aaa₃(Right, Y, Right1))
delmin_3_in_aaa₃(tree_3₃(Y, void_0, Right), Y, Right) -> delmin_3_out_aaa₃(tree_3₃(Y, void_0, Right), Y, Right)
delmin_3_in_aaa₃(tree_3₃(X, Left, underscore), Y, tree_3₃(X, Left1, underscore1)) -> if_delmin_3_in_1_aaa₇(X, Left, underscore, Y, Left1, underscore1, delmin_3_in_aaa₃(Left, Y, Left1))
if_delmin_3_in_1_aaa₇(X, Left, underscore, Y, Left1, underscore1, delmin_3_out_aaa₃(Left, Y, Left1)) -> delmin_3_out_aaa₃(tree_3₃(X, Left, underscore), Y, tree_3₃(X, Left1, underscore1))
if_delete_3_in_1_gga₆(X, Left, Right, Y, Right1, delmin_3_out_aaa₃(Right, Y, Right1)) -> delete_3_out_gga₃(X, tree_3₃(X, Left, Right), tree_3₃(Y, Left, Right1))
delete_3_in_gga₃(X, tree_3₃(Y, Left, Right), tree_3₃(Y, Left1, Right)) -> if_delete_3_in_2_gga₆(X, Y, Left, Right, Left1, less_2_in_ga₂(X, Y))
less_2_in_ga₂(0_0, s_1₁(underscore2)) -> less_2_out_ga₂(0_0, s_1₁(underscore2))
less_2_in_ga₂(s_1₁(X), s_1₁(Y)) -> if_less_2_in_1_ga₃(X, Y, less_2_in_aa₂(X, Y))
less_2_in_aa₂(0_0, s_1₁(underscore2)) -> less_2_out_aa₂(0_0, s_1₁(underscore2))
less_2_in_aa₂(s_1₁(X), s_1₁(Y)) -> if_less_2_in_1_aa₃(X, Y, less_2_in_aa₂(X, Y))
if_less_2_in_1_aa₃(X, Y, less_2_out_aa₂(X, Y)) -> less_2_out_aa₂(s_1₁(X), s_1₁(Y))
if_less_2_in_1_ga₃(X, Y, less_2_out_aa₂(X, Y)) -> less_2_out_ga₂(s_1₁(X), s_1₁(Y))
if_delete_3_in_2_gga₆(X, Y, Left, Right, Left1, less_2_out_ga₂(X, Y)) -> if_delete_3_in_3_gga₆(X, Y, Left, Right, Left1, delete_3_in_gaa₃(X, Left, Left1))
delete_3_in_gaa₃(X, tree_3₃(X, void_0, Right), Right) -> delete_3_out_gaa₃(X, tree_3₃(X, void_0, Right), Right)
delete_3_in_gaa₃(X, tree_3₃(X, Left, void_0), Left) -> delete_3_out_gaa₃(X, tree_3₃(X, Left, void_0), Left)
delete_3_in_gaa₃(X, tree_3₃(X, Left, Right), tree_3₃(Y, Left, Right1)) -> if_delete_3_in_1_gaa₆(X, Left, Right, Y, Right1, delmin_3_in_aaa₃(Right, Y, Right1))
if_delete_3_in_1_gaa₆(X, Left, Right, Y, Right1, delmin_3_out_aaa₃(Right, Y, Right1)) -> delete_3_out_gaa₃(X, tree_3₃(X, Left, Right), tree_3₃(Y, Left, Right1))
delete_3_in_gaa₃(X, tree_3₃(Y, Left, Right), tree_3₃(Y, Left1, Right)) -> if_delete_3_in_2_gaa₆(X, Y, Left, Right, Left1, less_2_in_ga₂(X, Y))
if_delete_3_in_2_gaa₆(X, Y, Left, Right, Left1, less_2_out_ga₂(X, Y)) -> if_delete_3_in_3_gaa₆(X, Y, Left, Right, Left1, delete_3_in_gaa₃(X, Left, Left1))
delete_3_in_gaa₃(X, tree_3₃(Y, Left, Right), tree_3₃(Y, Left, Right1)) -> if_delete_3_in_4_gaa₆(X, Y, Left, Right, Right1, less_2_in_ag₂(Y, X))
less_2_in_ag₂(0_0, s_1₁(underscore2)) -> less_2_out_ag₂(0_0, s_1₁(underscore2))
less_2_in_ag₂(s_1₁(X), s_1₁(Y)) -> if_less_2_in_1_ag₃(X, Y, less_2_in_aa₂(X, Y))
if_less_2_in_1_ag₃(X, Y, less_2_out_aa₂(X, Y)) -> less_2_out_ag₂(s_1₁(X), s_1₁(Y))
if_delete_3_in_4_gaa₆(X, Y, Left, Right, Right1, less_2_out_ag₂(Y, X)) -> if_delete_3_in_5_gaa₆(X, Y, Left, Right, Right1, delete_3_in_gaa₃(X, Right, Right1))
if_delete_3_in_5_gaa₆(X, Y, Left, Right, Right1, delete_3_out_gaa₃(X, Right, Right1)) -> delete_3_out_gaa₃(X, tree_3₃(Y, Left, Right), tree_3₃(Y, Left, Right1))
if_delete_3_in_3_gaa₆(X, Y, Left, Right, Left1, delete_3_out_gaa₃(X, Left, Left1)) -> delete_3_out_gaa₃(X, tree_3₃(Y, Left, Right), tree_3₃(Y, Left1, Right))
if_delete_3_in_3_gga₆(X, Y, Left, Right, Left1, delete_3_out_gaa₃(X, Left, Left1)) -> delete_3_out_gga₃(X, tree_3₃(Y, Left, Right), tree_3₃(Y, Left1, Right))
delete_3_in_gga₃(X, tree_3₃(Y, Left, Right), tree_3₃(Y, Left, Right1)) -> if_delete_3_in_4_gga₆(X, Y, Left, Right, Right1, less_2_in_ag₂(Y, X))
if_delete_3_in_4_gga₆(X, Y, Left, Right, Right1, less_2_out_ag₂(Y, X)) -> if_delete_3_in_5_gga₆(X, Y, Left, Right, Right1, delete_3_in_gaa₃(X, Right, Right1))
if_delete_3_in_5_gga₆(X, Y, Left, Right, Right1, delete_3_out_gaa₃(X, Right, Right1)) -> delete_3_out_gga₃(X, tree_3₃(Y, Left, Right), tree_3₃(Y, Left, Right1))

↳ PROLOG

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

  ↳ PrologToPiTRSProof

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

DELETE_3_IN_GAA₃(X, tree_3₃(Y, Left, Right), tree_3₃(Y, Left1, Right)) -> IF_DELETE_3_IN_2_GAA₆(X, Y, Left, Right, Left1, less_2_in_ga₂(X, Y))
DELETE_3_IN_GAA₃(X, tree_3₃(Y, Left, Right), tree_3₃(Y, Left, Right1)) -> IF_DELETE_3_IN_4_GAA₆(X, Y, Left, Right, Right1, less_2_in_ag₂(Y, X))
IF_DELETE_3_IN_4_GAA₆(X, Y, Left, Right, Right1, less_2_out_ag₂(Y, X)) -> DELETE_3_IN_GAA₃(X, Right, Right1)
IF_DELETE_3_IN_2_GAA₆(X, Y, Left, Right, Left1, less_2_out_ga₂(X, Y)) -> DELETE_3_IN_GAA₃(X, Left, Left1)

The TRS R consists of the following rules:

less_2_in_ga₂(0_0, s_1₁(underscore2)) -> less_2_out_ga₂(0_0, s_1₁(underscore2))
less_2_in_ga₂(s_1₁(X), s_1₁(Y)) -> if_less_2_in_1_ga₃(X, Y, less_2_in_aa₂(X, Y))
less_2_in_ag₂(0_0, s_1₁(underscore2)) -> less_2_out_ag₂(0_0, s_1₁(underscore2))
less_2_in_ag₂(s_1₁(X), s_1₁(Y)) -> if_less_2_in_1_ag₃(X, Y, less_2_in_aa₂(X, Y))
if_less_2_in_1_ga₃(X, Y, less_2_out_aa₂(X, Y)) -> less_2_out_ga₂(s_1₁(X), s_1₁(Y))
if_less_2_in_1_ag₃(X, Y, less_2_out_aa₂(X, Y)) -> less_2_out_ag₂(s_1₁(X), s_1₁(Y))
less_2_in_aa₂(0_0, s_1₁(underscore2)) -> less_2_out_aa₂(0_0, s_1₁(underscore2))
less_2_in_aa₂(s_1₁(X), s_1₁(Y)) -> if_less_2_in_1_aa₃(X, Y, less_2_in_aa₂(X, Y))
if_less_2_in_1_aa₃(X, Y, less_2_out_aa₂(X, Y)) -> less_2_out_aa₂(s_1₁(X), s_1₁(Y))

The argument filtering Pi contains the following mapping:
tree_3₃(x1, x2, x3) = tree_3
0_0 = 0_0
s_1₁(x1) = s_1
less_2_in_ga₂(x1, x2) = less_2_in_ga₁(x1)
less_2_out_ga₂(x1, x2) = less_2_out_ga₁(x2)
if_less_2_in_1_ga₃(x1, x2, x3) = if_less_2_in_1_ga₁(x3)
less_2_in_aa₂(x1, x2) = less_2_in_aa
less_2_out_aa₂(x1, x2) = less_2_out_aa₂(x1, x2)
if_less_2_in_1_aa₃(x1, x2, x3) = if_less_2_in_1_aa₁(x3)
less_2_in_ag₂(x1, x2) = less_2_in_ag₁(x2)
less_2_out_ag₂(x1, x2) = less_2_out_ag₁(x1)
if_less_2_in_1_ag₃(x1, x2, x3) = if_less_2_in_1_ag₁(x3)
IF_DELETE_3_IN_4_GAA₆(x1, x2, x3, x4, x5, x6) = IF_DELETE_3_IN_4_GAA₂(x1, x6)
DELETE_3_IN_GAA₃(x1, x2, x3) = DELETE_3_IN_GAA₁(x1)
IF_DELETE_3_IN_2_GAA₆(x1, x2, x3, x4, x5, x6) = IF_DELETE_3_IN_2_GAA₂(x1, x6)

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

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

  ↳ PrologToPiTRSProof

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

DELETE_3_IN_GAA₁(X) -> IF_DELETE_3_IN_2_GAA₂(X, less_2_in_ga₁(X))
DELETE_3_IN_GAA₁(X) -> IF_DELETE_3_IN_4_GAA₂(X, less_2_in_ag₁(X))
IF_DELETE_3_IN_4_GAA₂(X, less_2_out_ag₁(Y)) -> DELETE_3_IN_GAA₁(X)
IF_DELETE_3_IN_2_GAA₂(X, less_2_out_ga₁(Y)) -> DELETE_3_IN_GAA₁(X)

The TRS R consists of the following rules:

less_2_in_ga₁(0_0) -> less_2_out_ga₁(s_1)
less_2_in_ga₁(s_1) -> if_less_2_in_1_ga₁(less_2_in_aa)
less_2_in_ag₁(s_1) -> less_2_out_ag₁(0_0)
less_2_in_ag₁(s_1) -> if_less_2_in_1_ag₁(less_2_in_aa)
if_less_2_in_1_ga₁(less_2_out_aa₂(X, Y)) -> less_2_out_ga₁(s_1)
if_less_2_in_1_ag₁(less_2_out_aa₂(X, Y)) -> less_2_out_ag₁(s_1)
less_2_in_aa -> less_2_out_aa₂(0_0, s_1)
less_2_in_aa -> if_less_2_in_1_aa₁(less_2_in_aa)
if_less_2_in_1_aa₁(less_2_out_aa₂(X, Y)) -> less_2_out_aa₂(s_1, s_1)

The set Q consists of the following terms:

less_2_in_ga₁(x0)
less_2_in_ag₁(x0)
if_less_2_in_1_ga₁(x0)
if_less_2_in_1_ag₁(x0)
less_2_in_aa
if_less_2_in_1_aa₁(x0)

We have to consider all (P,Q,R)-chains.
The head symbols of this DP problem are {IF_DELETE_3_IN_2_GAA₂, DELETE_3_IN_GAA₁, IF_DELETE_3_IN_4_GAA₂}.
With regard to the inferred argument filtering the predicates were used in the following modes:
delete₃: (b,b,f) (b,f,f)
delmin₃: (f,f,f)
less₂: (b,f) (f,f) (f,b)
Transforming PROLOG into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:

delete_3_in_gga₃(X, tree_3₃(X, void_0, Right), Right) -> delete_3_out_gga₃(X, tree_3₃(X, void_0, Right), Right)
delete_3_in_gga₃(X, tree_3₃(X, Left, void_0), Left) -> delete_3_out_gga₃(X, tree_3₃(X, Left, void_0), Left)
delete_3_in_gga₃(X, tree_3₃(X, Left, Right), tree_3₃(Y, Left, Right1)) -> if_delete_3_in_1_gga₆(X, Left, Right, Y, Right1, delmin_3_in_aaa₃(Right, Y, Right1))
delmin_3_in_aaa₃(tree_3₃(Y, void_0, Right), Y, Right) -> delmin_3_out_aaa₃(tree_3₃(Y, void_0, Right), Y, Right)
delmin_3_in_aaa₃(tree_3₃(X, Left, underscore), Y, tree_3₃(X, Left1, underscore1)) -> if_delmin_3_in_1_aaa₇(X, Left, underscore, Y, Left1, underscore1, delmin_3_in_aaa₃(Left, Y, Left1))
if_delmin_3_in_1_aaa₇(X, Left, underscore, Y, Left1, underscore1, delmin_3_out_aaa₃(Left, Y, Left1)) -> delmin_3_out_aaa₃(tree_3₃(X, Left, underscore), Y, tree_3₃(X, Left1, underscore1))
if_delete_3_in_1_gga₆(X, Left, Right, Y, Right1, delmin_3_out_aaa₃(Right, Y, Right1)) -> delete_3_out_gga₃(X, tree_3₃(X, Left, Right), tree_3₃(Y, Left, Right1))
delete_3_in_gga₃(X, tree_3₃(Y, Left, Right), tree_3₃(Y, Left1, Right)) -> if_delete_3_in_2_gga₆(X, Y, Left, Right, Left1, less_2_in_ga₂(X, Y))
less_2_in_ga₂(0_0, s_1₁(underscore2)) -> less_2_out_ga₂(0_0, s_1₁(underscore2))
less_2_in_ga₂(s_1₁(X), s_1₁(Y)) -> if_less_2_in_1_ga₃(X, Y, less_2_in_aa₂(X, Y))
less_2_in_aa₂(0_0, s_1₁(underscore2)) -> less_2_out_aa₂(0_0, s_1₁(underscore2))
less_2_in_aa₂(s_1₁(X), s_1₁(Y)) -> if_less_2_in_1_aa₃(X, Y, less_2_in_aa₂(X, Y))
if_less_2_in_1_aa₃(X, Y, less_2_out_aa₂(X, Y)) -> less_2_out_aa₂(s_1₁(X), s_1₁(Y))
if_less_2_in_1_ga₃(X, Y, less_2_out_aa₂(X, Y)) -> less_2_out_ga₂(s_1₁(X), s_1₁(Y))
if_delete_3_in_2_gga₆(X, Y, Left, Right, Left1, less_2_out_ga₂(X, Y)) -> if_delete_3_in_3_gga₆(X, Y, Left, Right, Left1, delete_3_in_gaa₃(X, Left, Left1))
delete_3_in_gaa₃(X, tree_3₃(X, void_0, Right), Right) -> delete_3_out_gaa₃(X, tree_3₃(X, void_0, Right), Right)
delete_3_in_gaa₃(X, tree_3₃(X, Left, void_0), Left) -> delete_3_out_gaa₃(X, tree_3₃(X, Left, void_0), Left)
delete_3_in_gaa₃(X, tree_3₃(X, Left, Right), tree_3₃(Y, Left, Right1)) -> if_delete_3_in_1_gaa₆(X, Left, Right, Y, Right1, delmin_3_in_aaa₃(Right, Y, Right1))
if_delete_3_in_1_gaa₆(X, Left, Right, Y, Right1, delmin_3_out_aaa₃(Right, Y, Right1)) -> delete_3_out_gaa₃(X, tree_3₃(X, Left, Right), tree_3₃(Y, Left, Right1))
delete_3_in_gaa₃(X, tree_3₃(Y, Left, Right), tree_3₃(Y, Left1, Right)) -> if_delete_3_in_2_gaa₆(X, Y, Left, Right, Left1, less_2_in_ga₂(X, Y))
if_delete_3_in_2_gaa₆(X, Y, Left, Right, Left1, less_2_out_ga₂(X, Y)) -> if_delete_3_in_3_gaa₆(X, Y, Left, Right, Left1, delete_3_in_gaa₃(X, Left, Left1))
delete_3_in_gaa₃(X, tree_3₃(Y, Left, Right), tree_3₃(Y, Left, Right1)) -> if_delete_3_in_4_gaa₆(X, Y, Left, Right, Right1, less_2_in_ag₂(Y, X))
less_2_in_ag₂(0_0, s_1₁(underscore2)) -> less_2_out_ag₂(0_0, s_1₁(underscore2))
less_2_in_ag₂(s_1₁(X), s_1₁(Y)) -> if_less_2_in_1_ag₃(X, Y, less_2_in_aa₂(X, Y))
if_less_2_in_1_ag₃(X, Y, less_2_out_aa₂(X, Y)) -> less_2_out_ag₂(s_1₁(X), s_1₁(Y))
if_delete_3_in_4_gaa₆(X, Y, Left, Right, Right1, less_2_out_ag₂(Y, X)) -> if_delete_3_in_5_gaa₆(X, Y, Left, Right, Right1, delete_3_in_gaa₃(X, Right, Right1))
if_delete_3_in_5_gaa₆(X, Y, Left, Right, Right1, delete_3_out_gaa₃(X, Right, Right1)) -> delete_3_out_gaa₃(X, tree_3₃(Y, Left, Right), tree_3₃(Y, Left, Right1))
if_delete_3_in_3_gaa₆(X, Y, Left, Right, Left1, delete_3_out_gaa₃(X, Left, Left1)) -> delete_3_out_gaa₃(X, tree_3₃(Y, Left, Right), tree_3₃(Y, Left1, Right))
if_delete_3_in_3_gga₆(X, Y, Left, Right, Left1, delete_3_out_gaa₃(X, Left, Left1)) -> delete_3_out_gga₃(X, tree_3₃(Y, Left, Right), tree_3₃(Y, Left1, Right))
delete_3_in_gga₃(X, tree_3₃(Y, Left, Right), tree_3₃(Y, Left, Right1)) -> if_delete_3_in_4_gga₆(X, Y, Left, Right, Right1, less_2_in_ag₂(Y, X))
if_delete_3_in_4_gga₆(X, Y, Left, Right, Right1, less_2_out_ag₂(Y, X)) -> if_delete_3_in_5_gga₆(X, Y, Left, Right, Right1, delete_3_in_gaa₃(X, Right, Right1))
if_delete_3_in_5_gga₆(X, Y, Left, Right, Right1, delete_3_out_gaa₃(X, Right, Right1)) -> delete_3_out_gga₃(X, tree_3₃(Y, Left, Right), tree_3₃(Y, Left, Right1))

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of PROLOG

↳ PROLOG

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

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

delete_3_in_gga₃(X, tree_3₃(X, void_0, Right), Right) -> delete_3_out_gga₃(X, tree_3₃(X, void_0, Right), Right)
delete_3_in_gga₃(X, tree_3₃(X, Left, void_0), Left) -> delete_3_out_gga₃(X, tree_3₃(X, Left, void_0), Left)
delete_3_in_gga₃(X, tree_3₃(X, Left, Right), tree_3₃(Y, Left, Right1)) -> if_delete_3_in_1_gga₆(X, Left, Right, Y, Right1, delmin_3_in_aaa₃(Right, Y, Right1))
delmin_3_in_aaa₃(tree_3₃(Y, void_0, Right), Y, Right) -> delmin_3_out_aaa₃(tree_3₃(Y, void_0, Right), Y, Right)
delmin_3_in_aaa₃(tree_3₃(X, Left, underscore), Y, tree_3₃(X, Left1, underscore1)) -> if_delmin_3_in_1_aaa₇(X, Left, underscore, Y, Left1, underscore1, delmin_3_in_aaa₃(Left, Y, Left1))
if_delmin_3_in_1_aaa₇(X, Left, underscore, Y, Left1, underscore1, delmin_3_out_aaa₃(Left, Y, Left1)) -> delmin_3_out_aaa₃(tree_3₃(X, Left, underscore), Y, tree_3₃(X, Left1, underscore1))
if_delete_3_in_1_gga₆(X, Left, Right, Y, Right1, delmin_3_out_aaa₃(Right, Y, Right1)) -> delete_3_out_gga₃(X, tree_3₃(X, Left, Right), tree_3₃(Y, Left, Right1))
delete_3_in_gga₃(X, tree_3₃(Y, Left, Right), tree_3₃(Y, Left1, Right)) -> if_delete_3_in_2_gga₆(X, Y, Left, Right, Left1, less_2_in_ga₂(X, Y))
less_2_in_ga₂(0_0, s_1₁(underscore2)) -> less_2_out_ga₂(0_0, s_1₁(underscore2))
less_2_in_ga₂(s_1₁(X), s_1₁(Y)) -> if_less_2_in_1_ga₃(X, Y, less_2_in_aa₂(X, Y))
less_2_in_aa₂(0_0, s_1₁(underscore2)) -> less_2_out_aa₂(0_0, s_1₁(underscore2))
less_2_in_aa₂(s_1₁(X), s_1₁(Y)) -> if_less_2_in_1_aa₃(X, Y, less_2_in_aa₂(X, Y))
if_less_2_in_1_aa₃(X, Y, less_2_out_aa₂(X, Y)) -> less_2_out_aa₂(s_1₁(X), s_1₁(Y))
if_less_2_in_1_ga₃(X, Y, less_2_out_aa₂(X, Y)) -> less_2_out_ga₂(s_1₁(X), s_1₁(Y))
if_delete_3_in_2_gga₆(X, Y, Left, Right, Left1, less_2_out_ga₂(X, Y)) -> if_delete_3_in_3_gga₆(X, Y, Left, Right, Left1, delete_3_in_gaa₃(X, Left, Left1))
delete_3_in_gaa₃(X, tree_3₃(X, void_0, Right), Right) -> delete_3_out_gaa₃(X, tree_3₃(X, void_0, Right), Right)
delete_3_in_gaa₃(X, tree_3₃(X, Left, void_0), Left) -> delete_3_out_gaa₃(X, tree_3₃(X, Left, void_0), Left)
delete_3_in_gaa₃(X, tree_3₃(X, Left, Right), tree_3₃(Y, Left, Right1)) -> if_delete_3_in_1_gaa₆(X, Left, Right, Y, Right1, delmin_3_in_aaa₃(Right, Y, Right1))
if_delete_3_in_1_gaa₆(X, Left, Right, Y, Right1, delmin_3_out_aaa₃(Right, Y, Right1)) -> delete_3_out_gaa₃(X, tree_3₃(X, Left, Right), tree_3₃(Y, Left, Right1))
delete_3_in_gaa₃(X, tree_3₃(Y, Left, Right), tree_3₃(Y, Left1, Right)) -> if_delete_3_in_2_gaa₆(X, Y, Left, Right, Left1, less_2_in_ga₂(X, Y))
if_delete_3_in_2_gaa₆(X, Y, Left, Right, Left1, less_2_out_ga₂(X, Y)) -> if_delete_3_in_3_gaa₆(X, Y, Left, Right, Left1, delete_3_in_gaa₃(X, Left, Left1))
delete_3_in_gaa₃(X, tree_3₃(Y, Left, Right), tree_3₃(Y, Left, Right1)) -> if_delete_3_in_4_gaa₆(X, Y, Left, Right, Right1, less_2_in_ag₂(Y, X))
less_2_in_ag₂(0_0, s_1₁(underscore2)) -> less_2_out_ag₂(0_0, s_1₁(underscore2))
less_2_in_ag₂(s_1₁(X), s_1₁(Y)) -> if_less_2_in_1_ag₃(X, Y, less_2_in_aa₂(X, Y))
if_less_2_in_1_ag₃(X, Y, less_2_out_aa₂(X, Y)) -> less_2_out_ag₂(s_1₁(X), s_1₁(Y))
if_delete_3_in_4_gaa₆(X, Y, Left, Right, Right1, less_2_out_ag₂(Y, X)) -> if_delete_3_in_5_gaa₆(X, Y, Left, Right, Right1, delete_3_in_gaa₃(X, Right, Right1))
if_delete_3_in_5_gaa₆(X, Y, Left, Right, Right1, delete_3_out_gaa₃(X, Right, Right1)) -> delete_3_out_gaa₃(X, tree_3₃(Y, Left, Right), tree_3₃(Y, Left, Right1))
if_delete_3_in_3_gaa₆(X, Y, Left, Right, Left1, delete_3_out_gaa₃(X, Left, Left1)) -> delete_3_out_gaa₃(X, tree_3₃(Y, Left, Right), tree_3₃(Y, Left1, Right))
if_delete_3_in_3_gga₆(X, Y, Left, Right, Left1, delete_3_out_gaa₃(X, Left, Left1)) -> delete_3_out_gga₃(X, tree_3₃(Y, Left, Right), tree_3₃(Y, Left1, Right))
delete_3_in_gga₃(X, tree_3₃(Y, Left, Right), tree_3₃(Y, Left, Right1)) -> if_delete_3_in_4_gga₆(X, Y, Left, Right, Right1, less_2_in_ag₂(Y, X))
if_delete_3_in_4_gga₆(X, Y, Left, Right, Right1, less_2_out_ag₂(Y, X)) -> if_delete_3_in_5_gga₆(X, Y, Left, Right, Right1, delete_3_in_gaa₃(X, Right, Right1))
if_delete_3_in_5_gga₆(X, Y, Left, Right, Right1, delete_3_out_gaa₃(X, Right, Right1)) -> delete_3_out_gga₃(X, tree_3₃(Y, Left, Right), tree_3₃(Y, Left, Right1))

DELETE_3_IN_GGA₃(X, tree_3₃(X, Left, Right), tree_3₃(Y, Left, Right1)) -> IF_DELETE_3_IN_1_GGA₆(X, Left, Right, Y, Right1, delmin_3_in_aaa₃(Right, Y, Right1))
DELETE_3_IN_GGA₃(X, tree_3₃(X, Left, Right), tree_3₃(Y, Left, Right1)) -> DELMIN_3_IN_AAA₃(Right, Y, Right1)
DELMIN_3_IN_AAA₃(tree_3₃(X, Left, underscore), Y, tree_3₃(X, Left1, underscore1)) -> IF_DELMIN_3_IN_1_AAA₇(X, Left, underscore, Y, Left1, underscore1, delmin_3_in_aaa₃(Left, Y, Left1))
DELMIN_3_IN_AAA₃(tree_3₃(X, Left, underscore), Y, tree_3₃(X, Left1, underscore1)) -> DELMIN_3_IN_AAA₃(Left, Y, Left1)
DELETE_3_IN_GGA₃(X, tree_3₃(Y, Left, Right), tree_3₃(Y, Left1, Right)) -> IF_DELETE_3_IN_2_GGA₆(X, Y, Left, Right, Left1, less_2_in_ga₂(X, Y))
DELETE_3_IN_GGA₃(X, tree_3₃(Y, Left, Right), tree_3₃(Y, Left1, Right)) -> LESS_2_IN_GA₂(X, Y)
LESS_2_IN_GA₂(s_1₁(X), s_1₁(Y)) -> IF_LESS_2_IN_1_GA₃(X, Y, less_2_in_aa₂(X, Y))
LESS_2_IN_GA₂(s_1₁(X), s_1₁(Y)) -> LESS_2_IN_AA₂(X, Y)
LESS_2_IN_AA₂(s_1₁(X), s_1₁(Y)) -> IF_LESS_2_IN_1_AA₃(X, Y, less_2_in_aa₂(X, Y))
LESS_2_IN_AA₂(s_1₁(X), s_1₁(Y)) -> LESS_2_IN_AA₂(X, Y)
IF_DELETE_3_IN_2_GGA₆(X, Y, Left, Right, Left1, less_2_out_ga₂(X, Y)) -> IF_DELETE_3_IN_3_GGA₆(X, Y, Left, Right, Left1, delete_3_in_gaa₃(X, Left, Left1))
IF_DELETE_3_IN_2_GGA₆(X, Y, Left, Right, Left1, less_2_out_ga₂(X, Y)) -> DELETE_3_IN_GAA₃(X, Left, Left1)
DELETE_3_IN_GAA₃(X, tree_3₃(X, Left, Right), tree_3₃(Y, Left, Right1)) -> IF_DELETE_3_IN_1_GAA₆(X, Left, Right, Y, Right1, delmin_3_in_aaa₃(Right, Y, Right1))
DELETE_3_IN_GAA₃(X, tree_3₃(X, Left, Right), tree_3₃(Y, Left, Right1)) -> DELMIN_3_IN_AAA₃(Right, Y, Right1)
DELETE_3_IN_GAA₃(X, tree_3₃(Y, Left, Right), tree_3₃(Y, Left1, Right)) -> IF_DELETE_3_IN_2_GAA₆(X, Y, Left, Right, Left1, less_2_in_ga₂(X, Y))
DELETE_3_IN_GAA₃(X, tree_3₃(Y, Left, Right), tree_3₃(Y, Left1, Right)) -> LESS_2_IN_GA₂(X, Y)
IF_DELETE_3_IN_2_GAA₆(X, Y, Left, Right, Left1, less_2_out_ga₂(X, Y)) -> IF_DELETE_3_IN_3_GAA₆(X, Y, Left, Right, Left1, delete_3_in_gaa₃(X, Left, Left1))
IF_DELETE_3_IN_2_GAA₆(X, Y, Left, Right, Left1, less_2_out_ga₂(X, Y)) -> DELETE_3_IN_GAA₃(X, Left, Left1)
DELETE_3_IN_GAA₃(X, tree_3₃(Y, Left, Right), tree_3₃(Y, Left, Right1)) -> IF_DELETE_3_IN_4_GAA₆(X, Y, Left, Right, Right1, less_2_in_ag₂(Y, X))
DELETE_3_IN_GAA₃(X, tree_3₃(Y, Left, Right), tree_3₃(Y, Left, Right1)) -> LESS_2_IN_AG₂(Y, X)
LESS_2_IN_AG₂(s_1₁(X), s_1₁(Y)) -> IF_LESS_2_IN_1_AG₃(X, Y, less_2_in_aa₂(X, Y))
LESS_2_IN_AG₂(s_1₁(X), s_1₁(Y)) -> LESS_2_IN_AA₂(X, Y)
IF_DELETE_3_IN_4_GAA₆(X, Y, Left, Right, Right1, less_2_out_ag₂(Y, X)) -> IF_DELETE_3_IN_5_GAA₆(X, Y, Left, Right, Right1, delete_3_in_gaa₃(X, Right, Right1))
IF_DELETE_3_IN_4_GAA₆(X, Y, Left, Right, Right1, less_2_out_ag₂(Y, X)) -> DELETE_3_IN_GAA₃(X, Right, Right1)
DELETE_3_IN_GGA₃(X, tree_3₃(Y, Left, Right), tree_3₃(Y, Left, Right1)) -> IF_DELETE_3_IN_4_GGA₆(X, Y, Left, Right, Right1, less_2_in_ag₂(Y, X))
DELETE_3_IN_GGA₃(X, tree_3₃(Y, Left, Right), tree_3₃(Y, Left, Right1)) -> LESS_2_IN_AG₂(Y, X)
IF_DELETE_3_IN_4_GGA₆(X, Y, Left, Right, Right1, less_2_out_ag₂(Y, X)) -> IF_DELETE_3_IN_5_GGA₆(X, Y, Left, Right, Right1, delete_3_in_gaa₃(X, Right, Right1))
IF_DELETE_3_IN_4_GGA₆(X, Y, Left, Right, Right1, less_2_out_ag₂(Y, X)) -> DELETE_3_IN_GAA₃(X, Right, Right1)

The TRS R consists of the following rules:

delete_3_in_gga₃(X, tree_3₃(X, void_0, Right), Right) -> delete_3_out_gga₃(X, tree_3₃(X, void_0, Right), Right)
delete_3_in_gga₃(X, tree_3₃(X, Left, void_0), Left) -> delete_3_out_gga₃(X, tree_3₃(X, Left, void_0), Left)
delete_3_in_gga₃(X, tree_3₃(X, Left, Right), tree_3₃(Y, Left, Right1)) -> if_delete_3_in_1_gga₆(X, Left, Right, Y, Right1, delmin_3_in_aaa₃(Right, Y, Right1))
delmin_3_in_aaa₃(tree_3₃(Y, void_0, Right), Y, Right) -> delmin_3_out_aaa₃(tree_3₃(Y, void_0, Right), Y, Right)
delmin_3_in_aaa₃(tree_3₃(X, Left, underscore), Y, tree_3₃(X, Left1, underscore1)) -> if_delmin_3_in_1_aaa₇(X, Left, underscore, Y, Left1, underscore1, delmin_3_in_aaa₃(Left, Y, Left1))
if_delmin_3_in_1_aaa₇(X, Left, underscore, Y, Left1, underscore1, delmin_3_out_aaa₃(Left, Y, Left1)) -> delmin_3_out_aaa₃(tree_3₃(X, Left, underscore), Y, tree_3₃(X, Left1, underscore1))
if_delete_3_in_1_gga₆(X, Left, Right, Y, Right1, delmin_3_out_aaa₃(Right, Y, Right1)) -> delete_3_out_gga₃(X, tree_3₃(X, Left, Right), tree_3₃(Y, Left, Right1))
delete_3_in_gga₃(X, tree_3₃(Y, Left, Right), tree_3₃(Y, Left1, Right)) -> if_delete_3_in_2_gga₆(X, Y, Left, Right, Left1, less_2_in_ga₂(X, Y))
less_2_in_ga₂(0_0, s_1₁(underscore2)) -> less_2_out_ga₂(0_0, s_1₁(underscore2))
less_2_in_ga₂(s_1₁(X), s_1₁(Y)) -> if_less_2_in_1_ga₃(X, Y, less_2_in_aa₂(X, Y))
less_2_in_aa₂(0_0, s_1₁(underscore2)) -> less_2_out_aa₂(0_0, s_1₁(underscore2))
less_2_in_aa₂(s_1₁(X), s_1₁(Y)) -> if_less_2_in_1_aa₃(X, Y, less_2_in_aa₂(X, Y))
if_less_2_in_1_aa₃(X, Y, less_2_out_aa₂(X, Y)) -> less_2_out_aa₂(s_1₁(X), s_1₁(Y))
if_less_2_in_1_ga₃(X, Y, less_2_out_aa₂(X, Y)) -> less_2_out_ga₂(s_1₁(X), s_1₁(Y))
if_delete_3_in_2_gga₆(X, Y, Left, Right, Left1, less_2_out_ga₂(X, Y)) -> if_delete_3_in_3_gga₆(X, Y, Left, Right, Left1, delete_3_in_gaa₃(X, Left, Left1))
delete_3_in_gaa₃(X, tree_3₃(X, void_0, Right), Right) -> delete_3_out_gaa₃(X, tree_3₃(X, void_0, Right), Right)
delete_3_in_gaa₃(X, tree_3₃(X, Left, void_0), Left) -> delete_3_out_gaa₃(X, tree_3₃(X, Left, void_0), Left)
delete_3_in_gaa₃(X, tree_3₃(X, Left, Right), tree_3₃(Y, Left, Right1)) -> if_delete_3_in_1_gaa₆(X, Left, Right, Y, Right1, delmin_3_in_aaa₃(Right, Y, Right1))
if_delete_3_in_1_gaa₆(X, Left, Right, Y, Right1, delmin_3_out_aaa₃(Right, Y, Right1)) -> delete_3_out_gaa₃(X, tree_3₃(X, Left, Right), tree_3₃(Y, Left, Right1))
delete_3_in_gaa₃(X, tree_3₃(Y, Left, Right), tree_3₃(Y, Left1, Right)) -> if_delete_3_in_2_gaa₆(X, Y, Left, Right, Left1, less_2_in_ga₂(X, Y))
if_delete_3_in_2_gaa₆(X, Y, Left, Right, Left1, less_2_out_ga₂(X, Y)) -> if_delete_3_in_3_gaa₆(X, Y, Left, Right, Left1, delete_3_in_gaa₃(X, Left, Left1))
delete_3_in_gaa₃(X, tree_3₃(Y, Left, Right), tree_3₃(Y, Left, Right1)) -> if_delete_3_in_4_gaa₆(X, Y, Left, Right, Right1, less_2_in_ag₂(Y, X))
less_2_in_ag₂(0_0, s_1₁(underscore2)) -> less_2_out_ag₂(0_0, s_1₁(underscore2))
less_2_in_ag₂(s_1₁(X), s_1₁(Y)) -> if_less_2_in_1_ag₃(X, Y, less_2_in_aa₂(X, Y))
if_less_2_in_1_ag₃(X, Y, less_2_out_aa₂(X, Y)) -> less_2_out_ag₂(s_1₁(X), s_1₁(Y))
if_delete_3_in_4_gaa₆(X, Y, Left, Right, Right1, less_2_out_ag₂(Y, X)) -> if_delete_3_in_5_gaa₆(X, Y, Left, Right, Right1, delete_3_in_gaa₃(X, Right, Right1))
if_delete_3_in_5_gaa₆(X, Y, Left, Right, Right1, delete_3_out_gaa₃(X, Right, Right1)) -> delete_3_out_gaa₃(X, tree_3₃(Y, Left, Right), tree_3₃(Y, Left, Right1))
if_delete_3_in_3_gaa₆(X, Y, Left, Right, Left1, delete_3_out_gaa₃(X, Left, Left1)) -> delete_3_out_gaa₃(X, tree_3₃(Y, Left, Right), tree_3₃(Y, Left1, Right))
if_delete_3_in_3_gga₆(X, Y, Left, Right, Left1, delete_3_out_gaa₃(X, Left, Left1)) -> delete_3_out_gga₃(X, tree_3₃(Y, Left, Right), tree_3₃(Y, Left1, Right))
delete_3_in_gga₃(X, tree_3₃(Y, Left, Right), tree_3₃(Y, Left, Right1)) -> if_delete_3_in_4_gga₆(X, Y, Left, Right, Right1, less_2_in_ag₂(Y, X))
if_delete_3_in_4_gga₆(X, Y, Left, Right, Right1, less_2_out_ag₂(Y, X)) -> if_delete_3_in_5_gga₆(X, Y, Left, Right, Right1, delete_3_in_gaa₃(X, Right, Right1))
if_delete_3_in_5_gga₆(X, Y, Left, Right, Right1, delete_3_out_gaa₃(X, Right, Right1)) -> delete_3_out_gga₃(X, tree_3₃(Y, Left, Right), tree_3₃(Y, Left, Right1))

The argument filtering Pi contains the following mapping:
delete_3_in_gga₃(x1, x2, x3) = delete_3_in_gga₂(x1, x2)
tree_3₃(x1, x2, x3) = tree_3
void_0 = void_0
0_0 = 0_0
s_1₁(x1) = s_1
delete_3_out_gga₃(x1, x2, x3) = delete_3_out_gga₂(x1, x2)
if_delete_3_in_1_gga₆(x1, x2, x3, x4, x5, x6) = if_delete_3_in_1_gga₂(x1, x6)
delmin_3_in_aaa₃(x1, x2, x3) = delmin_3_in_aaa
delmin_3_out_aaa₃(x1, x2, x3) = delmin_3_out_aaa₁(x1)
if_delmin_3_in_1_aaa₇(x1, x2, x3, x4, x5, x6, x7) = if_delmin_3_in_1_aaa₁(x7)
if_delete_3_in_2_gga₆(x1, x2, x3, x4, x5, x6) = if_delete_3_in_2_gga₂(x1, x6)
less_2_in_ga₂(x1, x2) = less_2_in_ga₁(x1)
less_2_out_ga₂(x1, x2) = less_2_out_ga₂(x1, x2)
if_less_2_in_1_ga₃(x1, x2, x3) = if_less_2_in_1_ga₁(x3)
less_2_in_aa₂(x1, x2) = less_2_in_aa
less_2_out_aa₂(x1, x2) = less_2_out_aa₂(x1, x2)
if_less_2_in_1_aa₃(x1, x2, x3) = if_less_2_in_1_aa₁(x3)
if_delete_3_in_3_gga₆(x1, x2, x3, x4, x5, x6) = if_delete_3_in_3_gga₂(x1, x6)
if_delete_3_in_4_gga₆(x1, x2, x3, x4, x5, x6) = if_delete_3_in_4_gga₂(x1, x6)
less_2_in_ag₂(x1, x2) = less_2_in_ag₁(x2)
less_2_out_ag₂(x1, x2) = less_2_out_ag₂(x1, x2)
if_less_2_in_1_ag₃(x1, x2, x3) = if_less_2_in_1_ag₁(x3)
if_delete_3_in_5_gga₆(x1, x2, x3, x4, x5, x6) = if_delete_3_in_5_gga₂(x1, x6)
delete_3_in_gaa₃(x1, x2, x3) = delete_3_in_gaa₁(x1)
delete_3_out_gaa₃(x1, x2, x3) = delete_3_out_gaa₂(x1, x2)
if_delete_3_in_1_gaa₆(x1, x2, x3, x4, x5, x6) = if_delete_3_in_1_gaa₂(x1, x6)
if_delete_3_in_2_gaa₆(x1, x2, x3, x4, x5, x6) = if_delete_3_in_2_gaa₂(x1, x6)
if_delete_3_in_3_gaa₆(x1, x2, x3, x4, x5, x6) = if_delete_3_in_3_gaa₂(x1, x6)
if_delete_3_in_4_gaa₆(x1, x2, x3, x4, x5, x6) = if_delete_3_in_4_gaa₂(x1, x6)
if_delete_3_in_5_gaa₆(x1, x2, x3, x4, x5, x6) = if_delete_3_in_5_gaa₂(x1, x6)
IF_DELETE_3_IN_1_GAA₆(x1, x2, x3, x4, x5, x6) = IF_DELETE_3_IN_1_GAA₂(x1, x6)
LESS_2_IN_AG₂(x1, x2) = LESS_2_IN_AG₁(x2)
LESS_2_IN_GA₂(x1, x2) = LESS_2_IN_GA₁(x1)
IF_LESS_2_IN_1_AG₃(x1, x2, x3) = IF_LESS_2_IN_1_AG₁(x3)
IF_DELETE_3_IN_4_GGA₆(x1, x2, x3, x4, x5, x6) = IF_DELETE_3_IN_4_GGA₂(x1, x6)
DELMIN_3_IN_AAA₃(x1, x2, x3) = DELMIN_3_IN_AAA
IF_LESS_2_IN_1_AA₃(x1, x2, x3) = IF_LESS_2_IN_1_AA₁(x3)
IF_DELETE_3_IN_5_GAA₆(x1, x2, x3, x4, x5, x6) = IF_DELETE_3_IN_5_GAA₂(x1, x6)
IF_DELETE_3_IN_4_GAA₆(x1, x2, x3, x4, x5, x6) = IF_DELETE_3_IN_4_GAA₂(x1, x6)
IF_DELETE_3_IN_5_GGA₆(x1, x2, x3, x4, x5, x6) = IF_DELETE_3_IN_5_GGA₂(x1, x6)
IF_DELETE_3_IN_1_GGA₆(x1, x2, x3, x4, x5, x6) = IF_DELETE_3_IN_1_GGA₂(x1, x6)
IF_LESS_2_IN_1_GA₃(x1, x2, x3) = IF_LESS_2_IN_1_GA₁(x3)
DELETE_3_IN_GGA₃(x1, x2, x3) = DELETE_3_IN_GGA₂(x1, x2)
DELETE_3_IN_GAA₃(x1, x2, x3) = DELETE_3_IN_GAA₁(x1)
IF_DELETE_3_IN_2_GAA₆(x1, x2, x3, x4, x5, x6) = IF_DELETE_3_IN_2_GAA₂(x1, x6)
LESS_2_IN_AA₂(x1, x2) = LESS_2_IN_AA
IF_DELETE_3_IN_2_GGA₆(x1, x2, x3, x4, x5, x6) = IF_DELETE_3_IN_2_GGA₂(x1, x6)
IF_DELMIN_3_IN_1_AAA₇(x1, x2, x3, x4, x5, x6, x7) = IF_DELMIN_3_IN_1_AAA₁(x7)
IF_DELETE_3_IN_3_GGA₆(x1, x2, x3, x4, x5, x6) = IF_DELETE_3_IN_3_GGA₂(x1, x6)
IF_DELETE_3_IN_3_GAA₆(x1, x2, x3, x4, x5, x6) = IF_DELETE_3_IN_3_GAA₂(x1, x6)

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

↳ PROLOG

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

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

DELETE_3_IN_GGA₃(X, tree_3₃(X, Left, Right), tree_3₃(Y, Left, Right1)) -> IF_DELETE_3_IN_1_GGA₆(X, Left, Right, Y, Right1, delmin_3_in_aaa₃(Right, Y, Right1))
DELETE_3_IN_GGA₃(X, tree_3₃(X, Left, Right), tree_3₃(Y, Left, Right1)) -> DELMIN_3_IN_AAA₃(Right, Y, Right1)
DELMIN_3_IN_AAA₃(tree_3₃(X, Left, underscore), Y, tree_3₃(X, Left1, underscore1)) -> IF_DELMIN_3_IN_1_AAA₇(X, Left, underscore, Y, Left1, underscore1, delmin_3_in_aaa₃(Left, Y, Left1))
DELMIN_3_IN_AAA₃(tree_3₃(X, Left, underscore), Y, tree_3₃(X, Left1, underscore1)) -> DELMIN_3_IN_AAA₃(Left, Y, Left1)
DELETE_3_IN_GGA₃(X, tree_3₃(Y, Left, Right), tree_3₃(Y, Left1, Right)) -> IF_DELETE_3_IN_2_GGA₆(X, Y, Left, Right, Left1, less_2_in_ga₂(X, Y))
DELETE_3_IN_GGA₃(X, tree_3₃(Y, Left, Right), tree_3₃(Y, Left1, Right)) -> LESS_2_IN_GA₂(X, Y)
LESS_2_IN_GA₂(s_1₁(X), s_1₁(Y)) -> IF_LESS_2_IN_1_GA₃(X, Y, less_2_in_aa₂(X, Y))
LESS_2_IN_GA₂(s_1₁(X), s_1₁(Y)) -> LESS_2_IN_AA₂(X, Y)
LESS_2_IN_AA₂(s_1₁(X), s_1₁(Y)) -> IF_LESS_2_IN_1_AA₃(X, Y, less_2_in_aa₂(X, Y))
LESS_2_IN_AA₂(s_1₁(X), s_1₁(Y)) -> LESS_2_IN_AA₂(X, Y)
IF_DELETE_3_IN_2_GGA₆(X, Y, Left, Right, Left1, less_2_out_ga₂(X, Y)) -> IF_DELETE_3_IN_3_GGA₆(X, Y, Left, Right, Left1, delete_3_in_gaa₃(X, Left, Left1))
IF_DELETE_3_IN_2_GGA₆(X, Y, Left, Right, Left1, less_2_out_ga₂(X, Y)) -> DELETE_3_IN_GAA₃(X, Left, Left1)
DELETE_3_IN_GAA₃(X, tree_3₃(X, Left, Right), tree_3₃(Y, Left, Right1)) -> IF_DELETE_3_IN_1_GAA₆(X, Left, Right, Y, Right1, delmin_3_in_aaa₃(Right, Y, Right1))
DELETE_3_IN_GAA₃(X, tree_3₃(X, Left, Right), tree_3₃(Y, Left, Right1)) -> DELMIN_3_IN_AAA₃(Right, Y, Right1)
DELETE_3_IN_GAA₃(X, tree_3₃(Y, Left, Right), tree_3₃(Y, Left1, Right)) -> IF_DELETE_3_IN_2_GAA₆(X, Y, Left, Right, Left1, less_2_in_ga₂(X, Y))
DELETE_3_IN_GAA₃(X, tree_3₃(Y, Left, Right), tree_3₃(Y, Left1, Right)) -> LESS_2_IN_GA₂(X, Y)
IF_DELETE_3_IN_2_GAA₆(X, Y, Left, Right, Left1, less_2_out_ga₂(X, Y)) -> IF_DELETE_3_IN_3_GAA₆(X, Y, Left, Right, Left1, delete_3_in_gaa₃(X, Left, Left1))
IF_DELETE_3_IN_2_GAA₆(X, Y, Left, Right, Left1, less_2_out_ga₂(X, Y)) -> DELETE_3_IN_GAA₃(X, Left, Left1)
DELETE_3_IN_GAA₃(X, tree_3₃(Y, Left, Right), tree_3₃(Y, Left, Right1)) -> IF_DELETE_3_IN_4_GAA₆(X, Y, Left, Right, Right1, less_2_in_ag₂(Y, X))
DELETE_3_IN_GAA₃(X, tree_3₃(Y, Left, Right), tree_3₃(Y, Left, Right1)) -> LESS_2_IN_AG₂(Y, X)
LESS_2_IN_AG₂(s_1₁(X), s_1₁(Y)) -> IF_LESS_2_IN_1_AG₃(X, Y, less_2_in_aa₂(X, Y))
LESS_2_IN_AG₂(s_1₁(X), s_1₁(Y)) -> LESS_2_IN_AA₂(X, Y)
IF_DELETE_3_IN_4_GAA₆(X, Y, Left, Right, Right1, less_2_out_ag₂(Y, X)) -> IF_DELETE_3_IN_5_GAA₆(X, Y, Left, Right, Right1, delete_3_in_gaa₃(X, Right, Right1))
IF_DELETE_3_IN_4_GAA₆(X, Y, Left, Right, Right1, less_2_out_ag₂(Y, X)) -> DELETE_3_IN_GAA₃(X, Right, Right1)
DELETE_3_IN_GGA₃(X, tree_3₃(Y, Left, Right), tree_3₃(Y, Left, Right1)) -> IF_DELETE_3_IN_4_GGA₆(X, Y, Left, Right, Right1, less_2_in_ag₂(Y, X))
DELETE_3_IN_GGA₃(X, tree_3₃(Y, Left, Right), tree_3₃(Y, Left, Right1)) -> LESS_2_IN_AG₂(Y, X)
IF_DELETE_3_IN_4_GGA₆(X, Y, Left, Right, Right1, less_2_out_ag₂(Y, X)) -> IF_DELETE_3_IN_5_GGA₆(X, Y, Left, Right, Right1, delete_3_in_gaa₃(X, Right, Right1))
IF_DELETE_3_IN_4_GGA₆(X, Y, Left, Right, Right1, less_2_out_ag₂(Y, X)) -> DELETE_3_IN_GAA₃(X, Right, Right1)

The TRS R consists of the following rules:

delete_3_in_gga₃(X, tree_3₃(X, void_0, Right), Right) -> delete_3_out_gga₃(X, tree_3₃(X, void_0, Right), Right)
delete_3_in_gga₃(X, tree_3₃(X, Left, void_0), Left) -> delete_3_out_gga₃(X, tree_3₃(X, Left, void_0), Left)
delete_3_in_gga₃(X, tree_3₃(X, Left, Right), tree_3₃(Y, Left, Right1)) -> if_delete_3_in_1_gga₆(X, Left, Right, Y, Right1, delmin_3_in_aaa₃(Right, Y, Right1))
delmin_3_in_aaa₃(tree_3₃(Y, void_0, Right), Y, Right) -> delmin_3_out_aaa₃(tree_3₃(Y, void_0, Right), Y, Right)
delmin_3_in_aaa₃(tree_3₃(X, Left, underscore), Y, tree_3₃(X, Left1, underscore1)) -> if_delmin_3_in_1_aaa₇(X, Left, underscore, Y, Left1, underscore1, delmin_3_in_aaa₃(Left, Y, Left1))
if_delmin_3_in_1_aaa₇(X, Left, underscore, Y, Left1, underscore1, delmin_3_out_aaa₃(Left, Y, Left1)) -> delmin_3_out_aaa₃(tree_3₃(X, Left, underscore), Y, tree_3₃(X, Left1, underscore1))
if_delete_3_in_1_gga₆(X, Left, Right, Y, Right1, delmin_3_out_aaa₃(Right, Y, Right1)) -> delete_3_out_gga₃(X, tree_3₃(X, Left, Right), tree_3₃(Y, Left, Right1))
delete_3_in_gga₃(X, tree_3₃(Y, Left, Right), tree_3₃(Y, Left1, Right)) -> if_delete_3_in_2_gga₆(X, Y, Left, Right, Left1, less_2_in_ga₂(X, Y))
less_2_in_ga₂(0_0, s_1₁(underscore2)) -> less_2_out_ga₂(0_0, s_1₁(underscore2))
less_2_in_ga₂(s_1₁(X), s_1₁(Y)) -> if_less_2_in_1_ga₃(X, Y, less_2_in_aa₂(X, Y))
less_2_in_aa₂(0_0, s_1₁(underscore2)) -> less_2_out_aa₂(0_0, s_1₁(underscore2))
less_2_in_aa₂(s_1₁(X), s_1₁(Y)) -> if_less_2_in_1_aa₃(X, Y, less_2_in_aa₂(X, Y))
if_less_2_in_1_aa₃(X, Y, less_2_out_aa₂(X, Y)) -> less_2_out_aa₂(s_1₁(X), s_1₁(Y))
if_less_2_in_1_ga₃(X, Y, less_2_out_aa₂(X, Y)) -> less_2_out_ga₂(s_1₁(X), s_1₁(Y))
if_delete_3_in_2_gga₆(X, Y, Left, Right, Left1, less_2_out_ga₂(X, Y)) -> if_delete_3_in_3_gga₆(X, Y, Left, Right, Left1, delete_3_in_gaa₃(X, Left, Left1))
delete_3_in_gaa₃(X, tree_3₃(X, void_0, Right), Right) -> delete_3_out_gaa₃(X, tree_3₃(X, void_0, Right), Right)
delete_3_in_gaa₃(X, tree_3₃(X, Left, void_0), Left) -> delete_3_out_gaa₃(X, tree_3₃(X, Left, void_0), Left)
delete_3_in_gaa₃(X, tree_3₃(X, Left, Right), tree_3₃(Y, Left, Right1)) -> if_delete_3_in_1_gaa₆(X, Left, Right, Y, Right1, delmin_3_in_aaa₃(Right, Y, Right1))
if_delete_3_in_1_gaa₆(X, Left, Right, Y, Right1, delmin_3_out_aaa₃(Right, Y, Right1)) -> delete_3_out_gaa₃(X, tree_3₃(X, Left, Right), tree_3₃(Y, Left, Right1))
delete_3_in_gaa₃(X, tree_3₃(Y, Left, Right), tree_3₃(Y, Left1, Right)) -> if_delete_3_in_2_gaa₆(X, Y, Left, Right, Left1, less_2_in_ga₂(X, Y))
if_delete_3_in_2_gaa₆(X, Y, Left, Right, Left1, less_2_out_ga₂(X, Y)) -> if_delete_3_in_3_gaa₆(X, Y, Left, Right, Left1, delete_3_in_gaa₃(X, Left, Left1))
delete_3_in_gaa₃(X, tree_3₃(Y, Left, Right), tree_3₃(Y, Left, Right1)) -> if_delete_3_in_4_gaa₆(X, Y, Left, Right, Right1, less_2_in_ag₂(Y, X))
less_2_in_ag₂(0_0, s_1₁(underscore2)) -> less_2_out_ag₂(0_0, s_1₁(underscore2))
less_2_in_ag₂(s_1₁(X), s_1₁(Y)) -> if_less_2_in_1_ag₃(X, Y, less_2_in_aa₂(X, Y))
if_less_2_in_1_ag₃(X, Y, less_2_out_aa₂(X, Y)) -> less_2_out_ag₂(s_1₁(X), s_1₁(Y))
if_delete_3_in_4_gaa₆(X, Y, Left, Right, Right1, less_2_out_ag₂(Y, X)) -> if_delete_3_in_5_gaa₆(X, Y, Left, Right, Right1, delete_3_in_gaa₃(X, Right, Right1))
if_delete_3_in_5_gaa₆(X, Y, Left, Right, Right1, delete_3_out_gaa₃(X, Right, Right1)) -> delete_3_out_gaa₃(X, tree_3₃(Y, Left, Right), tree_3₃(Y, Left, Right1))
if_delete_3_in_3_gaa₆(X, Y, Left, Right, Left1, delete_3_out_gaa₃(X, Left, Left1)) -> delete_3_out_gaa₃(X, tree_3₃(Y, Left, Right), tree_3₃(Y, Left1, Right))
if_delete_3_in_3_gga₆(X, Y, Left, Right, Left1, delete_3_out_gaa₃(X, Left, Left1)) -> delete_3_out_gga₃(X, tree_3₃(Y, Left, Right), tree_3₃(Y, Left1, Right))
delete_3_in_gga₃(X, tree_3₃(Y, Left, Right), tree_3₃(Y, Left, Right1)) -> if_delete_3_in_4_gga₆(X, Y, Left, Right, Right1, less_2_in_ag₂(Y, X))
if_delete_3_in_4_gga₆(X, Y, Left, Right, Right1, less_2_out_ag₂(Y, X)) -> if_delete_3_in_5_gga₆(X, Y, Left, Right, Right1, delete_3_in_gaa₃(X, Right, Right1))
if_delete_3_in_5_gga₆(X, Y, Left, Right, Right1, delete_3_out_gaa₃(X, Right, Right1)) -> delete_3_out_gga₃(X, tree_3₃(Y, Left, Right), tree_3₃(Y, Left, Right1))

The argument filtering Pi contains the following mapping:
delete_3_in_gga₃(x1, x2, x3) = delete_3_in_gga₂(x1, x2)
tree_3₃(x1, x2, x3) = tree_3
void_0 = void_0
0_0 = 0_0
s_1₁(x1) = s_1
delete_3_out_gga₃(x1, x2, x3) = delete_3_out_gga₂(x1, x2)
if_delete_3_in_1_gga₆(x1, x2, x3, x4, x5, x6) = if_delete_3_in_1_gga₂(x1, x6)
delmin_3_in_aaa₃(x1, x2, x3) = delmin_3_in_aaa
delmin_3_out_aaa₃(x1, x2, x3) = delmin_3_out_aaa₁(x1)
if_delmin_3_in_1_aaa₇(x1, x2, x3, x4, x5, x6, x7) = if_delmin_3_in_1_aaa₁(x7)
if_delete_3_in_2_gga₆(x1, x2, x3, x4, x5, x6) = if_delete_3_in_2_gga₂(x1, x6)
less_2_in_ga₂(x1, x2) = less_2_in_ga₁(x1)
less_2_out_ga₂(x1, x2) = less_2_out_ga₂(x1, x2)
if_less_2_in_1_ga₃(x1, x2, x3) = if_less_2_in_1_ga₁(x3)
less_2_in_aa₂(x1, x2) = less_2_in_aa
less_2_out_aa₂(x1, x2) = less_2_out_aa₂(x1, x2)
if_less_2_in_1_aa₃(x1, x2, x3) = if_less_2_in_1_aa₁(x3)
if_delete_3_in_3_gga₆(x1, x2, x3, x4, x5, x6) = if_delete_3_in_3_gga₂(x1, x6)
if_delete_3_in_4_gga₆(x1, x2, x3, x4, x5, x6) = if_delete_3_in_4_gga₂(x1, x6)
less_2_in_ag₂(x1, x2) = less_2_in_ag₁(x2)
less_2_out_ag₂(x1, x2) = less_2_out_ag₂(x1, x2)
if_less_2_in_1_ag₃(x1, x2, x3) = if_less_2_in_1_ag₁(x3)
if_delete_3_in_5_gga₆(x1, x2, x3, x4, x5, x6) = if_delete_3_in_5_gga₂(x1, x6)
delete_3_in_gaa₃(x1, x2, x3) = delete_3_in_gaa₁(x1)
delete_3_out_gaa₃(x1, x2, x3) = delete_3_out_gaa₂(x1, x2)
if_delete_3_in_1_gaa₆(x1, x2, x3, x4, x5, x6) = if_delete_3_in_1_gaa₂(x1, x6)
if_delete_3_in_2_gaa₆(x1, x2, x3, x4, x5, x6) = if_delete_3_in_2_gaa₂(x1, x6)
if_delete_3_in_3_gaa₆(x1, x2, x3, x4, x5, x6) = if_delete_3_in_3_gaa₂(x1, x6)
if_delete_3_in_4_gaa₆(x1, x2, x3, x4, x5, x6) = if_delete_3_in_4_gaa₂(x1, x6)
if_delete_3_in_5_gaa₆(x1, x2, x3, x4, x5, x6) = if_delete_3_in_5_gaa₂(x1, x6)
IF_DELETE_3_IN_1_GAA₆(x1, x2, x3, x4, x5, x6) = IF_DELETE_3_IN_1_GAA₂(x1, x6)
LESS_2_IN_AG₂(x1, x2) = LESS_2_IN_AG₁(x2)
LESS_2_IN_GA₂(x1, x2) = LESS_2_IN_GA₁(x1)
IF_LESS_2_IN_1_AG₃(x1, x2, x3) = IF_LESS_2_IN_1_AG₁(x3)
IF_DELETE_3_IN_4_GGA₆(x1, x2, x3, x4, x5, x6) = IF_DELETE_3_IN_4_GGA₂(x1, x6)
DELMIN_3_IN_AAA₃(x1, x2, x3) = DELMIN_3_IN_AAA
IF_LESS_2_IN_1_AA₃(x1, x2, x3) = IF_LESS_2_IN_1_AA₁(x3)
IF_DELETE_3_IN_5_GAA₆(x1, x2, x3, x4, x5, x6) = IF_DELETE_3_IN_5_GAA₂(x1, x6)
IF_DELETE_3_IN_4_GAA₆(x1, x2, x3, x4, x5, x6) = IF_DELETE_3_IN_4_GAA₂(x1, x6)
IF_DELETE_3_IN_5_GGA₆(x1, x2, x3, x4, x5, x6) = IF_DELETE_3_IN_5_GGA₂(x1, x6)
IF_DELETE_3_IN_1_GGA₆(x1, x2, x3, x4, x5, x6) = IF_DELETE_3_IN_1_GGA₂(x1, x6)
IF_LESS_2_IN_1_GA₃(x1, x2, x3) = IF_LESS_2_IN_1_GA₁(x3)
DELETE_3_IN_GGA₃(x1, x2, x3) = DELETE_3_IN_GGA₂(x1, x2)
DELETE_3_IN_GAA₃(x1, x2, x3) = DELETE_3_IN_GAA₁(x1)
IF_DELETE_3_IN_2_GAA₆(x1, x2, x3, x4, x5, x6) = IF_DELETE_3_IN_2_GAA₂(x1, x6)
LESS_2_IN_AA₂(x1, x2) = LESS_2_IN_AA
IF_DELETE_3_IN_2_GGA₆(x1, x2, x3, x4, x5, x6) = IF_DELETE_3_IN_2_GGA₂(x1, x6)
IF_DELMIN_3_IN_1_AAA₇(x1, x2, x3, x4, x5, x6, x7) = IF_DELMIN_3_IN_1_AAA₁(x7)
IF_DELETE_3_IN_3_GGA₆(x1, x2, x3, x4, x5, x6) = IF_DELETE_3_IN_3_GGA₂(x1, x6)
IF_DELETE_3_IN_3_GAA₆(x1, x2, x3, x4, x5, x6) = IF_DELETE_3_IN_3_GAA₂(x1, x6)

We have to consider all (P,R,Pi)-chains
The approximation of the Dependency Graph contains 3 SCCs with 22 less nodes.

↳ PROLOG

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

                ↳ UsableRulesProof

              ↳ PiDP

              ↳ PiDP

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

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

The TRS R consists of the following rules:

delete_3_in_gga₃(X, tree_3₃(X, void_0, Right), Right) -> delete_3_out_gga₃(X, tree_3₃(X, void_0, Right), Right)
delete_3_in_gga₃(X, tree_3₃(X, Left, void_0), Left) -> delete_3_out_gga₃(X, tree_3₃(X, Left, void_0), Left)
delete_3_in_gga₃(X, tree_3₃(X, Left, Right), tree_3₃(Y, Left, Right1)) -> if_delete_3_in_1_gga₆(X, Left, Right, Y, Right1, delmin_3_in_aaa₃(Right, Y, Right1))
delmin_3_in_aaa₃(tree_3₃(Y, void_0, Right), Y, Right) -> delmin_3_out_aaa₃(tree_3₃(Y, void_0, Right), Y, Right)
delmin_3_in_aaa₃(tree_3₃(X, Left, underscore), Y, tree_3₃(X, Left1, underscore1)) -> if_delmin_3_in_1_aaa₇(X, Left, underscore, Y, Left1, underscore1, delmin_3_in_aaa₃(Left, Y, Left1))
if_delmin_3_in_1_aaa₇(X, Left, underscore, Y, Left1, underscore1, delmin_3_out_aaa₃(Left, Y, Left1)) -> delmin_3_out_aaa₃(tree_3₃(X, Left, underscore), Y, tree_3₃(X, Left1, underscore1))
if_delete_3_in_1_gga₆(X, Left, Right, Y, Right1, delmin_3_out_aaa₃(Right, Y, Right1)) -> delete_3_out_gga₃(X, tree_3₃(X, Left, Right), tree_3₃(Y, Left, Right1))
delete_3_in_gga₃(X, tree_3₃(Y, Left, Right), tree_3₃(Y, Left1, Right)) -> if_delete_3_in_2_gga₆(X, Y, Left, Right, Left1, less_2_in_ga₂(X, Y))
less_2_in_ga₂(0_0, s_1₁(underscore2)) -> less_2_out_ga₂(0_0, s_1₁(underscore2))
less_2_in_ga₂(s_1₁(X), s_1₁(Y)) -> if_less_2_in_1_ga₃(X, Y, less_2_in_aa₂(X, Y))
less_2_in_aa₂(0_0, s_1₁(underscore2)) -> less_2_out_aa₂(0_0, s_1₁(underscore2))
less_2_in_aa₂(s_1₁(X), s_1₁(Y)) -> if_less_2_in_1_aa₃(X, Y, less_2_in_aa₂(X, Y))
if_less_2_in_1_aa₃(X, Y, less_2_out_aa₂(X, Y)) -> less_2_out_aa₂(s_1₁(X), s_1₁(Y))
if_less_2_in_1_ga₃(X, Y, less_2_out_aa₂(X, Y)) -> less_2_out_ga₂(s_1₁(X), s_1₁(Y))
if_delete_3_in_2_gga₆(X, Y, Left, Right, Left1, less_2_out_ga₂(X, Y)) -> if_delete_3_in_3_gga₆(X, Y, Left, Right, Left1, delete_3_in_gaa₃(X, Left, Left1))
delete_3_in_gaa₃(X, tree_3₃(X, void_0, Right), Right) -> delete_3_out_gaa₃(X, tree_3₃(X, void_0, Right), Right)
delete_3_in_gaa₃(X, tree_3₃(X, Left, void_0), Left) -> delete_3_out_gaa₃(X, tree_3₃(X, Left, void_0), Left)
delete_3_in_gaa₃(X, tree_3₃(X, Left, Right), tree_3₃(Y, Left, Right1)) -> if_delete_3_in_1_gaa₆(X, Left, Right, Y, Right1, delmin_3_in_aaa₃(Right, Y, Right1))
if_delete_3_in_1_gaa₆(X, Left, Right, Y, Right1, delmin_3_out_aaa₃(Right, Y, Right1)) -> delete_3_out_gaa₃(X, tree_3₃(X, Left, Right), tree_3₃(Y, Left, Right1))
delete_3_in_gaa₃(X, tree_3₃(Y, Left, Right), tree_3₃(Y, Left1, Right)) -> if_delete_3_in_2_gaa₆(X, Y, Left, Right, Left1, less_2_in_ga₂(X, Y))
if_delete_3_in_2_gaa₆(X, Y, Left, Right, Left1, less_2_out_ga₂(X, Y)) -> if_delete_3_in_3_gaa₆(X, Y, Left, Right, Left1, delete_3_in_gaa₃(X, Left, Left1))
delete_3_in_gaa₃(X, tree_3₃(Y, Left, Right), tree_3₃(Y, Left, Right1)) -> if_delete_3_in_4_gaa₆(X, Y, Left, Right, Right1, less_2_in_ag₂(Y, X))
less_2_in_ag₂(0_0, s_1₁(underscore2)) -> less_2_out_ag₂(0_0, s_1₁(underscore2))
less_2_in_ag₂(s_1₁(X), s_1₁(Y)) -> if_less_2_in_1_ag₃(X, Y, less_2_in_aa₂(X, Y))
if_less_2_in_1_ag₃(X, Y, less_2_out_aa₂(X, Y)) -> less_2_out_ag₂(s_1₁(X), s_1₁(Y))
if_delete_3_in_4_gaa₆(X, Y, Left, Right, Right1, less_2_out_ag₂(Y, X)) -> if_delete_3_in_5_gaa₆(X, Y, Left, Right, Right1, delete_3_in_gaa₃(X, Right, Right1))
if_delete_3_in_5_gaa₆(X, Y, Left, Right, Right1, delete_3_out_gaa₃(X, Right, Right1)) -> delete_3_out_gaa₃(X, tree_3₃(Y, Left, Right), tree_3₃(Y, Left, Right1))
if_delete_3_in_3_gaa₆(X, Y, Left, Right, Left1, delete_3_out_gaa₃(X, Left, Left1)) -> delete_3_out_gaa₃(X, tree_3₃(Y, Left, Right), tree_3₃(Y, Left1, Right))
if_delete_3_in_3_gga₆(X, Y, Left, Right, Left1, delete_3_out_gaa₃(X, Left, Left1)) -> delete_3_out_gga₃(X, tree_3₃(Y, Left, Right), tree_3₃(Y, Left1, Right))
delete_3_in_gga₃(X, tree_3₃(Y, Left, Right), tree_3₃(Y, Left, Right1)) -> if_delete_3_in_4_gga₆(X, Y, Left, Right, Right1, less_2_in_ag₂(Y, X))
if_delete_3_in_4_gga₆(X, Y, Left, Right, Right1, less_2_out_ag₂(Y, X)) -> if_delete_3_in_5_gga₆(X, Y, Left, Right, Right1, delete_3_in_gaa₃(X, Right, Right1))
if_delete_3_in_5_gga₆(X, Y, Left, Right, Right1, delete_3_out_gaa₃(X, Right, Right1)) -> delete_3_out_gga₃(X, tree_3₃(Y, Left, Right), tree_3₃(Y, Left, Right1))

↳ PROLOG

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

              ↳ PiDP

              ↳ PiDP

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

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

↳ PROLOG

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

              ↳ PiDP

              ↳ PiDP

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

LESS_2_IN_AA -> LESS_2_IN_AA

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_AA}.

↳ PROLOG

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

              ↳ PiDP

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

DELMIN_3_IN_AAA₃(tree_3₃(X, Left, underscore), Y, tree_3₃(X, Left1, underscore1)) -> DELMIN_3_IN_AAA₃(Left, Y, Left1)

The TRS R consists of the following rules:

delete_3_in_gga₃(X, tree_3₃(X, void_0, Right), Right) -> delete_3_out_gga₃(X, tree_3₃(X, void_0, Right), Right)
delete_3_in_gga₃(X, tree_3₃(X, Left, void_0), Left) -> delete_3_out_gga₃(X, tree_3₃(X, Left, void_0), Left)
delete_3_in_gga₃(X, tree_3₃(X, Left, Right), tree_3₃(Y, Left, Right1)) -> if_delete_3_in_1_gga₆(X, Left, Right, Y, Right1, delmin_3_in_aaa₃(Right, Y, Right1))
delmin_3_in_aaa₃(tree_3₃(Y, void_0, Right), Y, Right) -> delmin_3_out_aaa₃(tree_3₃(Y, void_0, Right), Y, Right)
delmin_3_in_aaa₃(tree_3₃(X, Left, underscore), Y, tree_3₃(X, Left1, underscore1)) -> if_delmin_3_in_1_aaa₇(X, Left, underscore, Y, Left1, underscore1, delmin_3_in_aaa₃(Left, Y, Left1))
if_delmin_3_in_1_aaa₇(X, Left, underscore, Y, Left1, underscore1, delmin_3_out_aaa₃(Left, Y, Left1)) -> delmin_3_out_aaa₃(tree_3₃(X, Left, underscore), Y, tree_3₃(X, Left1, underscore1))
if_delete_3_in_1_gga₆(X, Left, Right, Y, Right1, delmin_3_out_aaa₃(Right, Y, Right1)) -> delete_3_out_gga₃(X, tree_3₃(X, Left, Right), tree_3₃(Y, Left, Right1))
delete_3_in_gga₃(X, tree_3₃(Y, Left, Right), tree_3₃(Y, Left1, Right)) -> if_delete_3_in_2_gga₆(X, Y, Left, Right, Left1, less_2_in_ga₂(X, Y))
less_2_in_ga₂(0_0, s_1₁(underscore2)) -> less_2_out_ga₂(0_0, s_1₁(underscore2))
less_2_in_ga₂(s_1₁(X), s_1₁(Y)) -> if_less_2_in_1_ga₃(X, Y, less_2_in_aa₂(X, Y))
less_2_in_aa₂(0_0, s_1₁(underscore2)) -> less_2_out_aa₂(0_0, s_1₁(underscore2))
less_2_in_aa₂(s_1₁(X), s_1₁(Y)) -> if_less_2_in_1_aa₃(X, Y, less_2_in_aa₂(X, Y))
if_less_2_in_1_aa₃(X, Y, less_2_out_aa₂(X, Y)) -> less_2_out_aa₂(s_1₁(X), s_1₁(Y))
if_less_2_in_1_ga₃(X, Y, less_2_out_aa₂(X, Y)) -> less_2_out_ga₂(s_1₁(X), s_1₁(Y))
if_delete_3_in_2_gga₆(X, Y, Left, Right, Left1, less_2_out_ga₂(X, Y)) -> if_delete_3_in_3_gga₆(X, Y, Left, Right, Left1, delete_3_in_gaa₃(X, Left, Left1))
delete_3_in_gaa₃(X, tree_3₃(X, void_0, Right), Right) -> delete_3_out_gaa₃(X, tree_3₃(X, void_0, Right), Right)
delete_3_in_gaa₃(X, tree_3₃(X, Left, void_0), Left) -> delete_3_out_gaa₃(X, tree_3₃(X, Left, void_0), Left)
delete_3_in_gaa₃(X, tree_3₃(X, Left, Right), tree_3₃(Y, Left, Right1)) -> if_delete_3_in_1_gaa₆(X, Left, Right, Y, Right1, delmin_3_in_aaa₃(Right, Y, Right1))
if_delete_3_in_1_gaa₆(X, Left, Right, Y, Right1, delmin_3_out_aaa₃(Right, Y, Right1)) -> delete_3_out_gaa₃(X, tree_3₃(X, Left, Right), tree_3₃(Y, Left, Right1))
delete_3_in_gaa₃(X, tree_3₃(Y, Left, Right), tree_3₃(Y, Left1, Right)) -> if_delete_3_in_2_gaa₆(X, Y, Left, Right, Left1, less_2_in_ga₂(X, Y))
if_delete_3_in_2_gaa₆(X, Y, Left, Right, Left1, less_2_out_ga₂(X, Y)) -> if_delete_3_in_3_gaa₆(X, Y, Left, Right, Left1, delete_3_in_gaa₃(X, Left, Left1))
delete_3_in_gaa₃(X, tree_3₃(Y, Left, Right), tree_3₃(Y, Left, Right1)) -> if_delete_3_in_4_gaa₆(X, Y, Left, Right, Right1, less_2_in_ag₂(Y, X))
less_2_in_ag₂(0_0, s_1₁(underscore2)) -> less_2_out_ag₂(0_0, s_1₁(underscore2))
less_2_in_ag₂(s_1₁(X), s_1₁(Y)) -> if_less_2_in_1_ag₃(X, Y, less_2_in_aa₂(X, Y))
if_less_2_in_1_ag₃(X, Y, less_2_out_aa₂(X, Y)) -> less_2_out_ag₂(s_1₁(X), s_1₁(Y))
if_delete_3_in_4_gaa₆(X, Y, Left, Right, Right1, less_2_out_ag₂(Y, X)) -> if_delete_3_in_5_gaa₆(X, Y, Left, Right, Right1, delete_3_in_gaa₃(X, Right, Right1))
if_delete_3_in_5_gaa₆(X, Y, Left, Right, Right1, delete_3_out_gaa₃(X, Right, Right1)) -> delete_3_out_gaa₃(X, tree_3₃(Y, Left, Right), tree_3₃(Y, Left, Right1))
if_delete_3_in_3_gaa₆(X, Y, Left, Right, Left1, delete_3_out_gaa₃(X, Left, Left1)) -> delete_3_out_gaa₃(X, tree_3₃(Y, Left, Right), tree_3₃(Y, Left1, Right))
if_delete_3_in_3_gga₆(X, Y, Left, Right, Left1, delete_3_out_gaa₃(X, Left, Left1)) -> delete_3_out_gga₃(X, tree_3₃(Y, Left, Right), tree_3₃(Y, Left1, Right))
delete_3_in_gga₃(X, tree_3₃(Y, Left, Right), tree_3₃(Y, Left, Right1)) -> if_delete_3_in_4_gga₆(X, Y, Left, Right, Right1, less_2_in_ag₂(Y, X))
if_delete_3_in_4_gga₆(X, Y, Left, Right, Right1, less_2_out_ag₂(Y, X)) -> if_delete_3_in_5_gga₆(X, Y, Left, Right, Right1, delete_3_in_gaa₃(X, Right, Right1))
if_delete_3_in_5_gga₆(X, Y, Left, Right, Right1, delete_3_out_gaa₃(X, Right, Right1)) -> delete_3_out_gga₃(X, tree_3₃(Y, Left, Right), tree_3₃(Y, Left, Right1))

↳ PROLOG

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

              ↳ PiDP

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

DELMIN_3_IN_AAA₃(tree_3₃(X, Left, underscore), Y, tree_3₃(X, Left1, underscore1)) -> DELMIN_3_IN_AAA₃(Left, Y, Left1)

↳ PROLOG

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

              ↳ PiDP

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

DELMIN_3_IN_AAA -> DELMIN_3_IN_AAA

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
The head symbols of this DP problem are {DELMIN_3_IN_AAA}.

↳ PROLOG

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

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

DELETE_3_IN_GAA₃(X, tree_3₃(Y, Left, Right), tree_3₃(Y, Left1, Right)) -> IF_DELETE_3_IN_2_GAA₆(X, Y, Left, Right, Left1, less_2_in_ga₂(X, Y))
DELETE_3_IN_GAA₃(X, tree_3₃(Y, Left, Right), tree_3₃(Y, Left, Right1)) -> IF_DELETE_3_IN_4_GAA₆(X, Y, Left, Right, Right1, less_2_in_ag₂(Y, X))
IF_DELETE_3_IN_4_GAA₆(X, Y, Left, Right, Right1, less_2_out_ag₂(Y, X)) -> DELETE_3_IN_GAA₃(X, Right, Right1)
IF_DELETE_3_IN_2_GAA₆(X, Y, Left, Right, Left1, less_2_out_ga₂(X, Y)) -> DELETE_3_IN_GAA₃(X, Left, Left1)

The TRS R consists of the following rules:

delete_3_in_gga₃(X, tree_3₃(X, void_0, Right), Right) -> delete_3_out_gga₃(X, tree_3₃(X, void_0, Right), Right)
delete_3_in_gga₃(X, tree_3₃(X, Left, void_0), Left) -> delete_3_out_gga₃(X, tree_3₃(X, Left, void_0), Left)
delete_3_in_gga₃(X, tree_3₃(X, Left, Right), tree_3₃(Y, Left, Right1)) -> if_delete_3_in_1_gga₆(X, Left, Right, Y, Right1, delmin_3_in_aaa₃(Right, Y, Right1))
delmin_3_in_aaa₃(tree_3₃(Y, void_0, Right), Y, Right) -> delmin_3_out_aaa₃(tree_3₃(Y, void_0, Right), Y, Right)
delmin_3_in_aaa₃(tree_3₃(X, Left, underscore), Y, tree_3₃(X, Left1, underscore1)) -> if_delmin_3_in_1_aaa₇(X, Left, underscore, Y, Left1, underscore1, delmin_3_in_aaa₃(Left, Y, Left1))
if_delmin_3_in_1_aaa₇(X, Left, underscore, Y, Left1, underscore1, delmin_3_out_aaa₃(Left, Y, Left1)) -> delmin_3_out_aaa₃(tree_3₃(X, Left, underscore), Y, tree_3₃(X, Left1, underscore1))
if_delete_3_in_1_gga₆(X, Left, Right, Y, Right1, delmin_3_out_aaa₃(Right, Y, Right1)) -> delete_3_out_gga₃(X, tree_3₃(X, Left, Right), tree_3₃(Y, Left, Right1))
delete_3_in_gga₃(X, tree_3₃(Y, Left, Right), tree_3₃(Y, Left1, Right)) -> if_delete_3_in_2_gga₆(X, Y, Left, Right, Left1, less_2_in_ga₂(X, Y))
less_2_in_ga₂(0_0, s_1₁(underscore2)) -> less_2_out_ga₂(0_0, s_1₁(underscore2))
less_2_in_ga₂(s_1₁(X), s_1₁(Y)) -> if_less_2_in_1_ga₃(X, Y, less_2_in_aa₂(X, Y))
less_2_in_aa₂(0_0, s_1₁(underscore2)) -> less_2_out_aa₂(0_0, s_1₁(underscore2))
less_2_in_aa₂(s_1₁(X), s_1₁(Y)) -> if_less_2_in_1_aa₃(X, Y, less_2_in_aa₂(X, Y))
if_less_2_in_1_aa₃(X, Y, less_2_out_aa₂(X, Y)) -> less_2_out_aa₂(s_1₁(X), s_1₁(Y))
if_less_2_in_1_ga₃(X, Y, less_2_out_aa₂(X, Y)) -> less_2_out_ga₂(s_1₁(X), s_1₁(Y))
if_delete_3_in_2_gga₆(X, Y, Left, Right, Left1, less_2_out_ga₂(X, Y)) -> if_delete_3_in_3_gga₆(X, Y, Left, Right, Left1, delete_3_in_gaa₃(X, Left, Left1))
delete_3_in_gaa₃(X, tree_3₃(X, void_0, Right), Right) -> delete_3_out_gaa₃(X, tree_3₃(X, void_0, Right), Right)
delete_3_in_gaa₃(X, tree_3₃(X, Left, void_0), Left) -> delete_3_out_gaa₃(X, tree_3₃(X, Left, void_0), Left)
delete_3_in_gaa₃(X, tree_3₃(X, Left, Right), tree_3₃(Y, Left, Right1)) -> if_delete_3_in_1_gaa₆(X, Left, Right, Y, Right1, delmin_3_in_aaa₃(Right, Y, Right1))
if_delete_3_in_1_gaa₆(X, Left, Right, Y, Right1, delmin_3_out_aaa₃(Right, Y, Right1)) -> delete_3_out_gaa₃(X, tree_3₃(X, Left, Right), tree_3₃(Y, Left, Right1))
delete_3_in_gaa₃(X, tree_3₃(Y, Left, Right), tree_3₃(Y, Left1, Right)) -> if_delete_3_in_2_gaa₆(X, Y, Left, Right, Left1, less_2_in_ga₂(X, Y))
if_delete_3_in_2_gaa₆(X, Y, Left, Right, Left1, less_2_out_ga₂(X, Y)) -> if_delete_3_in_3_gaa₆(X, Y, Left, Right, Left1, delete_3_in_gaa₃(X, Left, Left1))
delete_3_in_gaa₃(X, tree_3₃(Y, Left, Right), tree_3₃(Y, Left, Right1)) -> if_delete_3_in_4_gaa₆(X, Y, Left, Right, Right1, less_2_in_ag₂(Y, X))
less_2_in_ag₂(0_0, s_1₁(underscore2)) -> less_2_out_ag₂(0_0, s_1₁(underscore2))
less_2_in_ag₂(s_1₁(X), s_1₁(Y)) -> if_less_2_in_1_ag₃(X, Y, less_2_in_aa₂(X, Y))
if_less_2_in_1_ag₃(X, Y, less_2_out_aa₂(X, Y)) -> less_2_out_ag₂(s_1₁(X), s_1₁(Y))
if_delete_3_in_4_gaa₆(X, Y, Left, Right, Right1, less_2_out_ag₂(Y, X)) -> if_delete_3_in_5_gaa₆(X, Y, Left, Right, Right1, delete_3_in_gaa₃(X, Right, Right1))
if_delete_3_in_5_gaa₆(X, Y, Left, Right, Right1, delete_3_out_gaa₃(X, Right, Right1)) -> delete_3_out_gaa₃(X, tree_3₃(Y, Left, Right), tree_3₃(Y, Left, Right1))
if_delete_3_in_3_gaa₆(X, Y, Left, Right, Left1, delete_3_out_gaa₃(X, Left, Left1)) -> delete_3_out_gaa₃(X, tree_3₃(Y, Left, Right), tree_3₃(Y, Left1, Right))
if_delete_3_in_3_gga₆(X, Y, Left, Right, Left1, delete_3_out_gaa₃(X, Left, Left1)) -> delete_3_out_gga₃(X, tree_3₃(Y, Left, Right), tree_3₃(Y, Left1, Right))
delete_3_in_gga₃(X, tree_3₃(Y, Left, Right), tree_3₃(Y, Left, Right1)) -> if_delete_3_in_4_gga₆(X, Y, Left, Right, Right1, less_2_in_ag₂(Y, X))
if_delete_3_in_4_gga₆(X, Y, Left, Right, Right1, less_2_out_ag₂(Y, X)) -> if_delete_3_in_5_gga₆(X, Y, Left, Right, Right1, delete_3_in_gaa₃(X, Right, Right1))
if_delete_3_in_5_gga₆(X, Y, Left, Right, Right1, delete_3_out_gaa₃(X, Right, Right1)) -> delete_3_out_gga₃(X, tree_3₃(Y, Left, Right), tree_3₃(Y, Left, Right1))

↳ PROLOG

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

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

DELETE_3_IN_GAA₃(X, tree_3₃(Y, Left, Right), tree_3₃(Y, Left1, Right)) -> IF_DELETE_3_IN_2_GAA₆(X, Y, Left, Right, Left1, less_2_in_ga₂(X, Y))
DELETE_3_IN_GAA₃(X, tree_3₃(Y, Left, Right), tree_3₃(Y, Left, Right1)) -> IF_DELETE_3_IN_4_GAA₆(X, Y, Left, Right, Right1, less_2_in_ag₂(Y, X))
IF_DELETE_3_IN_4_GAA₆(X, Y, Left, Right, Right1, less_2_out_ag₂(Y, X)) -> DELETE_3_IN_GAA₃(X, Right, Right1)
IF_DELETE_3_IN_2_GAA₆(X, Y, Left, Right, Left1, less_2_out_ga₂(X, Y)) -> DELETE_3_IN_GAA₃(X, Left, Left1)

The TRS R consists of the following rules:

less_2_in_ga₂(0_0, s_1₁(underscore2)) -> less_2_out_ga₂(0_0, s_1₁(underscore2))
less_2_in_ga₂(s_1₁(X), s_1₁(Y)) -> if_less_2_in_1_ga₃(X, Y, less_2_in_aa₂(X, Y))
less_2_in_ag₂(0_0, s_1₁(underscore2)) -> less_2_out_ag₂(0_0, s_1₁(underscore2))
less_2_in_ag₂(s_1₁(X), s_1₁(Y)) -> if_less_2_in_1_ag₃(X, Y, less_2_in_aa₂(X, Y))
if_less_2_in_1_ga₃(X, Y, less_2_out_aa₂(X, Y)) -> less_2_out_ga₂(s_1₁(X), s_1₁(Y))
if_less_2_in_1_ag₃(X, Y, less_2_out_aa₂(X, Y)) -> less_2_out_ag₂(s_1₁(X), s_1₁(Y))
less_2_in_aa₂(0_0, s_1₁(underscore2)) -> less_2_out_aa₂(0_0, s_1₁(underscore2))
less_2_in_aa₂(s_1₁(X), s_1₁(Y)) -> if_less_2_in_1_aa₃(X, Y, less_2_in_aa₂(X, Y))
if_less_2_in_1_aa₃(X, Y, less_2_out_aa₂(X, Y)) -> less_2_out_aa₂(s_1₁(X), s_1₁(Y))

The argument filtering Pi contains the following mapping:
tree_3₃(x1, x2, x3) = tree_3
0_0 = 0_0
s_1₁(x1) = s_1
less_2_in_ga₂(x1, x2) = less_2_in_ga₁(x1)
less_2_out_ga₂(x1, x2) = less_2_out_ga₂(x1, x2)
if_less_2_in_1_ga₃(x1, x2, x3) = if_less_2_in_1_ga₁(x3)
less_2_in_aa₂(x1, x2) = less_2_in_aa
less_2_out_aa₂(x1, x2) = less_2_out_aa₂(x1, x2)
if_less_2_in_1_aa₃(x1, x2, x3) = if_less_2_in_1_aa₁(x3)
less_2_in_ag₂(x1, x2) = less_2_in_ag₁(x2)
less_2_out_ag₂(x1, x2) = less_2_out_ag₂(x1, x2)
if_less_2_in_1_ag₃(x1, x2, x3) = if_less_2_in_1_ag₁(x3)
IF_DELETE_3_IN_4_GAA₆(x1, x2, x3, x4, x5, x6) = IF_DELETE_3_IN_4_GAA₂(x1, x6)
DELETE_3_IN_GAA₃(x1, x2, x3) = DELETE_3_IN_GAA₁(x1)
IF_DELETE_3_IN_2_GAA₆(x1, x2, x3, x4, x5, x6) = IF_DELETE_3_IN_2_GAA₂(x1, x6)

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

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

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

DELETE_3_IN_GAA₁(X) -> IF_DELETE_3_IN_2_GAA₂(X, less_2_in_ga₁(X))
DELETE_3_IN_GAA₁(X) -> IF_DELETE_3_IN_4_GAA₂(X, less_2_in_ag₁(X))
IF_DELETE_3_IN_4_GAA₂(X, less_2_out_ag₂(Y, X)) -> DELETE_3_IN_GAA₁(X)
IF_DELETE_3_IN_2_GAA₂(X, less_2_out_ga₂(X, Y)) -> DELETE_3_IN_GAA₁(X)

The TRS R consists of the following rules:

less_2_in_ga₁(0_0) -> less_2_out_ga₂(0_0, s_1)
less_2_in_ga₁(s_1) -> if_less_2_in_1_ga₁(less_2_in_aa)
less_2_in_ag₁(s_1) -> less_2_out_ag₂(0_0, s_1)
less_2_in_ag₁(s_1) -> if_less_2_in_1_ag₁(less_2_in_aa)
if_less_2_in_1_ga₁(less_2_out_aa₂(X, Y)) -> less_2_out_ga₂(s_1, s_1)
if_less_2_in_1_ag₁(less_2_out_aa₂(X, Y)) -> less_2_out_ag₂(s_1, s_1)
less_2_in_aa -> less_2_out_aa₂(0_0, s_1)
less_2_in_aa -> if_less_2_in_1_aa₁(less_2_in_aa)
if_less_2_in_1_aa₁(less_2_out_aa₂(X, Y)) -> less_2_out_aa₂(s_1, s_1)

The set Q consists of the following terms:

less_2_in_ga₁(x0)
less_2_in_ag₁(x0)
if_less_2_in_1_ga₁(x0)
if_less_2_in_1_ag₁(x0)
less_2_in_aa
if_less_2_in_1_aa₁(x0)

We have to consider all (P,Q,R)-chains.
The head symbols of this DP problem are {IF_DELETE_3_IN_2_GAA₂, DELETE_3_IN_GAA₁, IF_DELETE_3_IN_4_GAA₂}.