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



↳ PROLOG
  ↳ UnrequestedClauseRemoverProof

balance2(T, TB) :- balance5510(T, XX0, XX1, {}0, .2(tuple2(nil0, XX0 - XX0), XX1), {}0, .2(tuple2(TB, I - {}0), X), X, I, {}0).
balance5510(nil0, C, T, T, A, B, A, B, X, X).
balance5510(tree3(L, V, R), XX0, XX1, NT, HR, TR, .2(tuple2(tree3(LB, VB, RB), A - D), H), .2(tuple2(LB, A - .2(VB, X)), .2(tuple2(RB, X - D), T)), IH, IT) :- balance5510(L, XX0, XX1, .2(tuple2(nil0, XX2 - XX2), XX3), HR1, TR1, H, T, IH, .2(V, IT1)), balance5510(R, XX2, XX3, NT, HR, TR, HR1, TR1, IT1, IT).
balance510(nil0, C, T, T, A, B, A, B, X, X) :- balance5510(nil0, C, T, T, A, B, A, B, X, X).
balance510(tree3(L, V, R), XX0, XX1, NT, HR, TR, .2(tuple2(tree3(LB, VB, RB), A - D), H), .2(tuple2(LB, A - .2(VB, X)), .2(tuple2(RB, X - D), T)), IH, IT) :- balance5510(tree3(L, V, R), XX0, XX1, NT, HR, TR, .2(tuple2(tree3(LB, VB, RB), A - D), H), .2(tuple2(LB, A - .2(VB, X)), .2(tuple2(RB, X - D), T)), IH, IT).
balance5(nil0, X - X, A - B, A - B, .2(tuple2(nil0, C - C), T) - T) :- balance510(nil0, C, T, T, A, B, A, B, X, X).
balance5(tree3(L, V, R), IH - IT, .2(tuple2(tree3(LB, VB, RB), A - D), H) - .2(tuple2(LB, A - .2(VB, X)), .2(tuple2(RB, X - D), T)), HR - TR, .2(tuple2(nil0, XX0 - XX0), XX1) - NT) :- balance510(tree3(L, V, R), XX0, XX1, NT, HR, TR, .2(tuple2(tree3(LB, VB, RB), A - D), H), .2(tuple2(LB, A - .2(VB, X)), .2(tuple2(RB, X - D), T)), IH, IT).


The clauses

balance510(nil0, C, T, T, A, B, A, B, X, X) :- balance5510(nil0, C, T, T, A, B, A, B, X, X).
balance510(tree3(L, V, R), XX0, XX1, NT, HR, TR, .2(tuple2(tree3(LB, VB, RB), A - D), H), .2(tuple2(LB, A - .2(VB, X)), .2(tuple2(RB, X - D), T)), IH, IT) :- balance5510(tree3(L, V, R), XX0, XX1, NT, HR, TR, .2(tuple2(tree3(LB, VB, RB), A - D), H), .2(tuple2(LB, A - .2(VB, X)), .2(tuple2(RB, X - D), T)), IH, IT).
balance5(nil0, X - X, A - B, A - B, .2(tuple2(nil0, C - C), T) - T) :- balance510(nil0, C, T, T, A, B, A, B, X, X).
balance5(tree3(L, V, R), IH - IT, .2(tuple2(tree3(LB, VB, RB), A - D), H) - .2(tuple2(LB, A - .2(VB, X)), .2(tuple2(RB, X - D), T)), HR - TR, .2(tuple2(nil0, XX0 - XX0), XX1) - NT) :- balance510(tree3(L, V, R), XX0, XX1, NT, HR, TR, .2(tuple2(tree3(LB, VB, RB), A - D), H), .2(tuple2(LB, A - .2(VB, X)), .2(tuple2(RB, X - D), T)), IH, IT).

can be ignored, as they are not needed by any of the given querys.

Deleting these clauses results in the following prolog program:

balance2(T, TB) :- balance5510(T, XX0, XX1, {}0, .2(tuple2(nil0, XX0 - XX0), XX1), {}0, .2(tuple2(TB, I - {}0), X), X, I, {}0).
balance5510(nil0, C, T, T, A, B, A, B, X, X).
balance5510(tree3(L, V, R), XX0, XX1, NT, HR, TR, .2(tuple2(tree3(LB, VB, RB), A - D), H), .2(tuple2(LB, A - .2(VB, X)), .2(tuple2(RB, X - D), T)), IH, IT) :- balance5510(L, XX0, XX1, .2(tuple2(nil0, XX2 - XX2), XX3), HR1, TR1, H, T, IH, .2(V, IT1)), balance5510(R, XX2, XX3, NT, HR, TR, HR1, TR1, IT1, IT).



↳ PROLOG
  ↳ UnrequestedClauseRemoverProof
    ↳ PROLOG
      ↳ PrologToPiTRSProof

balance2(T, TB) :- balance5510(T, XX0, XX1, {}0, .2(tuple2(nil0, XX0 - XX0), XX1), {}0, .2(tuple2(TB, I - {}0), X), X, I, {}0).
balance5510(nil0, C, T, T, A, B, A, B, X, X).
balance5510(tree3(L, V, R), XX0, XX1, NT, HR, TR, .2(tuple2(tree3(LB, VB, RB), A - D), H), .2(tuple2(LB, A - .2(VB, X)), .2(tuple2(RB, X - D), T)), IH, IT) :- balance5510(L, XX0, XX1, .2(tuple2(nil0, XX2 - XX2), XX3), HR1, TR1, H, T, IH, .2(V, IT1)), balance5510(R, XX2, XX3, NT, HR, TR, HR1, TR1, IT1, IT).


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


balance_2_in_ga2(T, TB) -> if_balance_2_in_1_ga3(T, TB, balance55_10_in_gaaggggaag10(T, XX0, XX1, []_0, ._22(tuple_22(nil_0, -2(XX0, XX0)), XX1), []_0, ._22(tuple_22(TB, -2(I, []_0)), X), X, I, []_0))
balance55_10_in_gaaggggaag10(nil_0, C, T, T, A, B, A, B, X, X) -> balance55_10_out_gaaggggaag10(nil_0, C, T, T, A, B, A, B, X, X)
balance55_10_in_gaaggggaag10(tree_33(L, V, R), XX0, XX1, NT, HR, TR, ._22(tuple_22(tree_33(LB, VB, RB), -2(A, D)), H), ._22(tuple_22(LB, -2(A, ._22(VB, X))), ._22(tuple_22(RB, -2(X, D)), T)), IH, IT) -> if_balance55_10_in_1_gaaggggaag19(L, V, R, XX0, XX1, NT, HR, TR, LB, VB, RB, A, D, H, X, T, IH, IT, balance55_10_in_gaagaaaaag10(L, XX0, XX1, ._22(tuple_22(nil_0, -2(XX2, XX2)), XX3), HR1, TR1, H, T, IH, ._22(V, IT1)))
balance55_10_in_gaagaaaaag10(nil_0, C, T, T, A, B, A, B, X, X) -> balance55_10_out_gaagaaaaag10(nil_0, C, T, T, A, B, A, B, X, X)
balance55_10_in_gaagaaaaag10(tree_33(L, V, R), XX0, XX1, NT, HR, TR, ._22(tuple_22(tree_33(LB, VB, RB), -2(A, D)), H), ._22(tuple_22(LB, -2(A, ._22(VB, X))), ._22(tuple_22(RB, -2(X, D)), T)), IH, IT) -> if_balance55_10_in_1_gaagaaaaag19(L, V, R, XX0, XX1, NT, HR, TR, LB, VB, RB, A, D, H, X, T, IH, IT, balance55_10_in_gaagaaaaag10(L, XX0, XX1, ._22(tuple_22(nil_0, -2(XX2, XX2)), XX3), HR1, TR1, H, T, IH, ._22(V, IT1)))
if_balance55_10_in_1_gaagaaaaag19(L, V, R, XX0, XX1, NT, HR, TR, LB, VB, RB, A, D, H, X, T, IH, IT, balance55_10_out_gaagaaaaag10(L, XX0, XX1, ._22(tuple_22(nil_0, -2(XX2, XX2)), XX3), HR1, TR1, H, T, IH, ._22(V, IT1))) -> if_balance55_10_in_2_gaagaaaaag24(L, V, R, XX0, XX1, NT, HR, TR, LB, VB, RB, A, D, H, X, T, IH, IT, XX2, XX3, HR1, TR1, IT1, balance55_10_in_gaagaaaaag10(R, XX2, XX3, NT, HR, TR, HR1, TR1, IT1, IT))
if_balance55_10_in_2_gaagaaaaag24(L, V, R, XX0, XX1, NT, HR, TR, LB, VB, RB, A, D, H, X, T, IH, IT, XX2, XX3, HR1, TR1, IT1, balance55_10_out_gaagaaaaag10(R, XX2, XX3, NT, HR, TR, HR1, TR1, IT1, IT)) -> balance55_10_out_gaagaaaaag10(tree_33(L, V, R), XX0, XX1, NT, HR, TR, ._22(tuple_22(tree_33(LB, VB, RB), -2(A, D)), H), ._22(tuple_22(LB, -2(A, ._22(VB, X))), ._22(tuple_22(RB, -2(X, D)), T)), IH, IT)
if_balance55_10_in_1_gaaggggaag19(L, V, R, XX0, XX1, NT, HR, TR, LB, VB, RB, A, D, H, X, T, IH, IT, balance55_10_out_gaagaaaaag10(L, XX0, XX1, ._22(tuple_22(nil_0, -2(XX2, XX2)), XX3), HR1, TR1, H, T, IH, ._22(V, IT1))) -> if_balance55_10_in_2_gaaggggaag24(L, V, R, XX0, XX1, NT, HR, TR, LB, VB, RB, A, D, H, X, T, IH, IT, XX2, XX3, HR1, TR1, IT1, balance55_10_in_gaagggaaag10(R, XX2, XX3, NT, HR, TR, HR1, TR1, IT1, IT))
balance55_10_in_gaagggaaag10(nil_0, C, T, T, A, B, A, B, X, X) -> balance55_10_out_gaagggaaag10(nil_0, C, T, T, A, B, A, B, X, X)
balance55_10_in_gaagggaaag10(tree_33(L, V, R), XX0, XX1, NT, HR, TR, ._22(tuple_22(tree_33(LB, VB, RB), -2(A, D)), H), ._22(tuple_22(LB, -2(A, ._22(VB, X))), ._22(tuple_22(RB, -2(X, D)), T)), IH, IT) -> if_balance55_10_in_1_gaagggaaag19(L, V, R, XX0, XX1, NT, HR, TR, LB, VB, RB, A, D, H, X, T, IH, IT, balance55_10_in_gaagaaaaag10(L, XX0, XX1, ._22(tuple_22(nil_0, -2(XX2, XX2)), XX3), HR1, TR1, H, T, IH, ._22(V, IT1)))
if_balance55_10_in_1_gaagggaaag19(L, V, R, XX0, XX1, NT, HR, TR, LB, VB, RB, A, D, H, X, T, IH, IT, balance55_10_out_gaagaaaaag10(L, XX0, XX1, ._22(tuple_22(nil_0, -2(XX2, XX2)), XX3), HR1, TR1, H, T, IH, ._22(V, IT1))) -> if_balance55_10_in_2_gaagggaaag24(L, V, R, XX0, XX1, NT, HR, TR, LB, VB, RB, A, D, H, X, T, IH, IT, XX2, XX3, HR1, TR1, IT1, balance55_10_in_gaagggaaag10(R, XX2, XX3, NT, HR, TR, HR1, TR1, IT1, IT))
if_balance55_10_in_2_gaagggaaag24(L, V, R, XX0, XX1, NT, HR, TR, LB, VB, RB, A, D, H, X, T, IH, IT, XX2, XX3, HR1, TR1, IT1, balance55_10_out_gaagggaaag10(R, XX2, XX3, NT, HR, TR, HR1, TR1, IT1, IT)) -> balance55_10_out_gaagggaaag10(tree_33(L, V, R), XX0, XX1, NT, HR, TR, ._22(tuple_22(tree_33(LB, VB, RB), -2(A, D)), H), ._22(tuple_22(LB, -2(A, ._22(VB, X))), ._22(tuple_22(RB, -2(X, D)), T)), IH, IT)
if_balance55_10_in_2_gaaggggaag24(L, V, R, XX0, XX1, NT, HR, TR, LB, VB, RB, A, D, H, X, T, IH, IT, XX2, XX3, HR1, TR1, IT1, balance55_10_out_gaagggaaag10(R, XX2, XX3, NT, HR, TR, HR1, TR1, IT1, IT)) -> balance55_10_out_gaaggggaag10(tree_33(L, V, R), XX0, XX1, NT, HR, TR, ._22(tuple_22(tree_33(LB, VB, RB), -2(A, D)), H), ._22(tuple_22(LB, -2(A, ._22(VB, X))), ._22(tuple_22(RB, -2(X, D)), T)), IH, IT)
if_balance_2_in_1_ga3(T, TB, balance55_10_out_gaaggggaag10(T, XX0, XX1, []_0, ._22(tuple_22(nil_0, -2(XX0, XX0)), XX1), []_0, ._22(tuple_22(TB, -2(I, []_0)), X), X, I, []_0)) -> balance_2_out_ga2(T, TB)

The argument filtering Pi contains the following mapping:
balance_2_in_ga2(x1, x2)  =  balance_2_in_ga1(x1)
[]_0  =  []_0
._22(x1, x2)  =  ._21(x1)
tuple_22(x1, x2)  =  tuple_21(x2)
nil_0  =  nil_0
-2(x1, x2)  =  -
tree_33(x1, x2, x3)  =  tree_33(x1, x2, x3)
if_balance_2_in_1_ga3(x1, x2, x3)  =  if_balance_2_in_1_ga1(x3)
balance55_10_in_gaaggggaag10(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  balance55_10_in_gaaggggaag6(x1, x4, x5, x6, x7, x10)
balance55_10_out_gaaggggaag10(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  balance55_10_out_gaaggggaag3(x3, x8, x9)
if_balance55_10_in_1_gaaggggaag19(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19)  =  if_balance55_10_in_1_gaaggggaag6(x3, x6, x7, x8, x18, x19)
balance55_10_in_gaagaaaaag10(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  balance55_10_in_gaagaaaaag3(x1, x4, x10)
balance55_10_out_gaagaaaaag10(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  balance55_10_out_gaagaaaaag2(x3, x9)
if_balance55_10_in_1_gaagaaaaag19(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19)  =  if_balance55_10_in_1_gaagaaaaag4(x3, x6, x18, x19)
if_balance55_10_in_2_gaagaaaaag24(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22, x23, x24)  =  if_balance55_10_in_2_gaagaaaaag3(x5, x17, x24)
if_balance55_10_in_2_gaaggggaag24(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22, x23, x24)  =  if_balance55_10_in_2_gaaggggaag3(x5, x17, x24)
balance55_10_in_gaagggaaag10(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  balance55_10_in_gaagggaaag5(x1, x4, x5, x6, x10)
balance55_10_out_gaagggaaag10(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  balance55_10_out_gaagggaaag4(x3, x7, x8, x9)
if_balance55_10_in_1_gaagggaaag19(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19)  =  if_balance55_10_in_1_gaagggaaag6(x3, x6, x7, x8, x18, x19)
if_balance55_10_in_2_gaagggaaag24(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22, x23, x24)  =  if_balance55_10_in_2_gaagggaaag3(x5, x17, x24)
balance_2_out_ga2(x1, x2)  =  balance_2_out_ga

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of PROLOG



↳ PROLOG
  ↳ UnrequestedClauseRemoverProof
    ↳ PROLOG
      ↳ PrologToPiTRSProof
        ↳ PiTRS
          ↳ DependencyPairsProof

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

balance_2_in_ga2(T, TB) -> if_balance_2_in_1_ga3(T, TB, balance55_10_in_gaaggggaag10(T, XX0, XX1, []_0, ._22(tuple_22(nil_0, -2(XX0, XX0)), XX1), []_0, ._22(tuple_22(TB, -2(I, []_0)), X), X, I, []_0))
balance55_10_in_gaaggggaag10(nil_0, C, T, T, A, B, A, B, X, X) -> balance55_10_out_gaaggggaag10(nil_0, C, T, T, A, B, A, B, X, X)
balance55_10_in_gaaggggaag10(tree_33(L, V, R), XX0, XX1, NT, HR, TR, ._22(tuple_22(tree_33(LB, VB, RB), -2(A, D)), H), ._22(tuple_22(LB, -2(A, ._22(VB, X))), ._22(tuple_22(RB, -2(X, D)), T)), IH, IT) -> if_balance55_10_in_1_gaaggggaag19(L, V, R, XX0, XX1, NT, HR, TR, LB, VB, RB, A, D, H, X, T, IH, IT, balance55_10_in_gaagaaaaag10(L, XX0, XX1, ._22(tuple_22(nil_0, -2(XX2, XX2)), XX3), HR1, TR1, H, T, IH, ._22(V, IT1)))
balance55_10_in_gaagaaaaag10(nil_0, C, T, T, A, B, A, B, X, X) -> balance55_10_out_gaagaaaaag10(nil_0, C, T, T, A, B, A, B, X, X)
balance55_10_in_gaagaaaaag10(tree_33(L, V, R), XX0, XX1, NT, HR, TR, ._22(tuple_22(tree_33(LB, VB, RB), -2(A, D)), H), ._22(tuple_22(LB, -2(A, ._22(VB, X))), ._22(tuple_22(RB, -2(X, D)), T)), IH, IT) -> if_balance55_10_in_1_gaagaaaaag19(L, V, R, XX0, XX1, NT, HR, TR, LB, VB, RB, A, D, H, X, T, IH, IT, balance55_10_in_gaagaaaaag10(L, XX0, XX1, ._22(tuple_22(nil_0, -2(XX2, XX2)), XX3), HR1, TR1, H, T, IH, ._22(V, IT1)))
if_balance55_10_in_1_gaagaaaaag19(L, V, R, XX0, XX1, NT, HR, TR, LB, VB, RB, A, D, H, X, T, IH, IT, balance55_10_out_gaagaaaaag10(L, XX0, XX1, ._22(tuple_22(nil_0, -2(XX2, XX2)), XX3), HR1, TR1, H, T, IH, ._22(V, IT1))) -> if_balance55_10_in_2_gaagaaaaag24(L, V, R, XX0, XX1, NT, HR, TR, LB, VB, RB, A, D, H, X, T, IH, IT, XX2, XX3, HR1, TR1, IT1, balance55_10_in_gaagaaaaag10(R, XX2, XX3, NT, HR, TR, HR1, TR1, IT1, IT))
if_balance55_10_in_2_gaagaaaaag24(L, V, R, XX0, XX1, NT, HR, TR, LB, VB, RB, A, D, H, X, T, IH, IT, XX2, XX3, HR1, TR1, IT1, balance55_10_out_gaagaaaaag10(R, XX2, XX3, NT, HR, TR, HR1, TR1, IT1, IT)) -> balance55_10_out_gaagaaaaag10(tree_33(L, V, R), XX0, XX1, NT, HR, TR, ._22(tuple_22(tree_33(LB, VB, RB), -2(A, D)), H), ._22(tuple_22(LB, -2(A, ._22(VB, X))), ._22(tuple_22(RB, -2(X, D)), T)), IH, IT)
if_balance55_10_in_1_gaaggggaag19(L, V, R, XX0, XX1, NT, HR, TR, LB, VB, RB, A, D, H, X, T, IH, IT, balance55_10_out_gaagaaaaag10(L, XX0, XX1, ._22(tuple_22(nil_0, -2(XX2, XX2)), XX3), HR1, TR1, H, T, IH, ._22(V, IT1))) -> if_balance55_10_in_2_gaaggggaag24(L, V, R, XX0, XX1, NT, HR, TR, LB, VB, RB, A, D, H, X, T, IH, IT, XX2, XX3, HR1, TR1, IT1, balance55_10_in_gaagggaaag10(R, XX2, XX3, NT, HR, TR, HR1, TR1, IT1, IT))
balance55_10_in_gaagggaaag10(nil_0, C, T, T, A, B, A, B, X, X) -> balance55_10_out_gaagggaaag10(nil_0, C, T, T, A, B, A, B, X, X)
balance55_10_in_gaagggaaag10(tree_33(L, V, R), XX0, XX1, NT, HR, TR, ._22(tuple_22(tree_33(LB, VB, RB), -2(A, D)), H), ._22(tuple_22(LB, -2(A, ._22(VB, X))), ._22(tuple_22(RB, -2(X, D)), T)), IH, IT) -> if_balance55_10_in_1_gaagggaaag19(L, V, R, XX0, XX1, NT, HR, TR, LB, VB, RB, A, D, H, X, T, IH, IT, balance55_10_in_gaagaaaaag10(L, XX0, XX1, ._22(tuple_22(nil_0, -2(XX2, XX2)), XX3), HR1, TR1, H, T, IH, ._22(V, IT1)))
if_balance55_10_in_1_gaagggaaag19(L, V, R, XX0, XX1, NT, HR, TR, LB, VB, RB, A, D, H, X, T, IH, IT, balance55_10_out_gaagaaaaag10(L, XX0, XX1, ._22(tuple_22(nil_0, -2(XX2, XX2)), XX3), HR1, TR1, H, T, IH, ._22(V, IT1))) -> if_balance55_10_in_2_gaagggaaag24(L, V, R, XX0, XX1, NT, HR, TR, LB, VB, RB, A, D, H, X, T, IH, IT, XX2, XX3, HR1, TR1, IT1, balance55_10_in_gaagggaaag10(R, XX2, XX3, NT, HR, TR, HR1, TR1, IT1, IT))
if_balance55_10_in_2_gaagggaaag24(L, V, R, XX0, XX1, NT, HR, TR, LB, VB, RB, A, D, H, X, T, IH, IT, XX2, XX3, HR1, TR1, IT1, balance55_10_out_gaagggaaag10(R, XX2, XX3, NT, HR, TR, HR1, TR1, IT1, IT)) -> balance55_10_out_gaagggaaag10(tree_33(L, V, R), XX0, XX1, NT, HR, TR, ._22(tuple_22(tree_33(LB, VB, RB), -2(A, D)), H), ._22(tuple_22(LB, -2(A, ._22(VB, X))), ._22(tuple_22(RB, -2(X, D)), T)), IH, IT)
if_balance55_10_in_2_gaaggggaag24(L, V, R, XX0, XX1, NT, HR, TR, LB, VB, RB, A, D, H, X, T, IH, IT, XX2, XX3, HR1, TR1, IT1, balance55_10_out_gaagggaaag10(R, XX2, XX3, NT, HR, TR, HR1, TR1, IT1, IT)) -> balance55_10_out_gaaggggaag10(tree_33(L, V, R), XX0, XX1, NT, HR, TR, ._22(tuple_22(tree_33(LB, VB, RB), -2(A, D)), H), ._22(tuple_22(LB, -2(A, ._22(VB, X))), ._22(tuple_22(RB, -2(X, D)), T)), IH, IT)
if_balance_2_in_1_ga3(T, TB, balance55_10_out_gaaggggaag10(T, XX0, XX1, []_0, ._22(tuple_22(nil_0, -2(XX0, XX0)), XX1), []_0, ._22(tuple_22(TB, -2(I, []_0)), X), X, I, []_0)) -> balance_2_out_ga2(T, TB)

The argument filtering Pi contains the following mapping:
balance_2_in_ga2(x1, x2)  =  balance_2_in_ga1(x1)
[]_0  =  []_0
._22(x1, x2)  =  ._21(x1)
tuple_22(x1, x2)  =  tuple_21(x2)
nil_0  =  nil_0
-2(x1, x2)  =  -
tree_33(x1, x2, x3)  =  tree_33(x1, x2, x3)
if_balance_2_in_1_ga3(x1, x2, x3)  =  if_balance_2_in_1_ga1(x3)
balance55_10_in_gaaggggaag10(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  balance55_10_in_gaaggggaag6(x1, x4, x5, x6, x7, x10)
balance55_10_out_gaaggggaag10(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  balance55_10_out_gaaggggaag3(x3, x8, x9)
if_balance55_10_in_1_gaaggggaag19(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19)  =  if_balance55_10_in_1_gaaggggaag6(x3, x6, x7, x8, x18, x19)
balance55_10_in_gaagaaaaag10(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  balance55_10_in_gaagaaaaag3(x1, x4, x10)
balance55_10_out_gaagaaaaag10(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  balance55_10_out_gaagaaaaag2(x3, x9)
if_balance55_10_in_1_gaagaaaaag19(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19)  =  if_balance55_10_in_1_gaagaaaaag4(x3, x6, x18, x19)
if_balance55_10_in_2_gaagaaaaag24(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22, x23, x24)  =  if_balance55_10_in_2_gaagaaaaag3(x5, x17, x24)
if_balance55_10_in_2_gaaggggaag24(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22, x23, x24)  =  if_balance55_10_in_2_gaaggggaag3(x5, x17, x24)
balance55_10_in_gaagggaaag10(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  balance55_10_in_gaagggaaag5(x1, x4, x5, x6, x10)
balance55_10_out_gaagggaaag10(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  balance55_10_out_gaagggaaag4(x3, x7, x8, x9)
if_balance55_10_in_1_gaagggaaag19(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19)  =  if_balance55_10_in_1_gaagggaaag6(x3, x6, x7, x8, x18, x19)
if_balance55_10_in_2_gaagggaaag24(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22, x23, x24)  =  if_balance55_10_in_2_gaagggaaag3(x5, x17, x24)
balance_2_out_ga2(x1, x2)  =  balance_2_out_ga


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

BALANCE_2_IN_GA2(T, TB) -> IF_BALANCE_2_IN_1_GA3(T, TB, balance55_10_in_gaaggggaag10(T, XX0, XX1, []_0, ._22(tuple_22(nil_0, -2(XX0, XX0)), XX1), []_0, ._22(tuple_22(TB, -2(I, []_0)), X), X, I, []_0))
BALANCE_2_IN_GA2(T, TB) -> BALANCE55_10_IN_GAAGGGGAAG10(T, XX0, XX1, []_0, ._22(tuple_22(nil_0, -2(XX0, XX0)), XX1), []_0, ._22(tuple_22(TB, -2(I, []_0)), X), X, I, []_0)
BALANCE55_10_IN_GAAGGGGAAG10(tree_33(L, V, R), XX0, XX1, NT, HR, TR, ._22(tuple_22(tree_33(LB, VB, RB), -2(A, D)), H), ._22(tuple_22(LB, -2(A, ._22(VB, X))), ._22(tuple_22(RB, -2(X, D)), T)), IH, IT) -> IF_BALANCE55_10_IN_1_GAAGGGGAAG19(L, V, R, XX0, XX1, NT, HR, TR, LB, VB, RB, A, D, H, X, T, IH, IT, balance55_10_in_gaagaaaaag10(L, XX0, XX1, ._22(tuple_22(nil_0, -2(XX2, XX2)), XX3), HR1, TR1, H, T, IH, ._22(V, IT1)))
BALANCE55_10_IN_GAAGGGGAAG10(tree_33(L, V, R), XX0, XX1, NT, HR, TR, ._22(tuple_22(tree_33(LB, VB, RB), -2(A, D)), H), ._22(tuple_22(LB, -2(A, ._22(VB, X))), ._22(tuple_22(RB, -2(X, D)), T)), IH, IT) -> BALANCE55_10_IN_GAAGAAAAAG10(L, XX0, XX1, ._22(tuple_22(nil_0, -2(XX2, XX2)), XX3), HR1, TR1, H, T, IH, ._22(V, IT1))
BALANCE55_10_IN_GAAGAAAAAG10(tree_33(L, V, R), XX0, XX1, NT, HR, TR, ._22(tuple_22(tree_33(LB, VB, RB), -2(A, D)), H), ._22(tuple_22(LB, -2(A, ._22(VB, X))), ._22(tuple_22(RB, -2(X, D)), T)), IH, IT) -> IF_BALANCE55_10_IN_1_GAAGAAAAAG19(L, V, R, XX0, XX1, NT, HR, TR, LB, VB, RB, A, D, H, X, T, IH, IT, balance55_10_in_gaagaaaaag10(L, XX0, XX1, ._22(tuple_22(nil_0, -2(XX2, XX2)), XX3), HR1, TR1, H, T, IH, ._22(V, IT1)))
BALANCE55_10_IN_GAAGAAAAAG10(tree_33(L, V, R), XX0, XX1, NT, HR, TR, ._22(tuple_22(tree_33(LB, VB, RB), -2(A, D)), H), ._22(tuple_22(LB, -2(A, ._22(VB, X))), ._22(tuple_22(RB, -2(X, D)), T)), IH, IT) -> BALANCE55_10_IN_GAAGAAAAAG10(L, XX0, XX1, ._22(tuple_22(nil_0, -2(XX2, XX2)), XX3), HR1, TR1, H, T, IH, ._22(V, IT1))
IF_BALANCE55_10_IN_1_GAAGAAAAAG19(L, V, R, XX0, XX1, NT, HR, TR, LB, VB, RB, A, D, H, X, T, IH, IT, balance55_10_out_gaagaaaaag10(L, XX0, XX1, ._22(tuple_22(nil_0, -2(XX2, XX2)), XX3), HR1, TR1, H, T, IH, ._22(V, IT1))) -> IF_BALANCE55_10_IN_2_GAAGAAAAAG24(L, V, R, XX0, XX1, NT, HR, TR, LB, VB, RB, A, D, H, X, T, IH, IT, XX2, XX3, HR1, TR1, IT1, balance55_10_in_gaagaaaaag10(R, XX2, XX3, NT, HR, TR, HR1, TR1, IT1, IT))
IF_BALANCE55_10_IN_1_GAAGAAAAAG19(L, V, R, XX0, XX1, NT, HR, TR, LB, VB, RB, A, D, H, X, T, IH, IT, balance55_10_out_gaagaaaaag10(L, XX0, XX1, ._22(tuple_22(nil_0, -2(XX2, XX2)), XX3), HR1, TR1, H, T, IH, ._22(V, IT1))) -> BALANCE55_10_IN_GAAGAAAAAG10(R, XX2, XX3, NT, HR, TR, HR1, TR1, IT1, IT)
IF_BALANCE55_10_IN_1_GAAGGGGAAG19(L, V, R, XX0, XX1, NT, HR, TR, LB, VB, RB, A, D, H, X, T, IH, IT, balance55_10_out_gaagaaaaag10(L, XX0, XX1, ._22(tuple_22(nil_0, -2(XX2, XX2)), XX3), HR1, TR1, H, T, IH, ._22(V, IT1))) -> IF_BALANCE55_10_IN_2_GAAGGGGAAG24(L, V, R, XX0, XX1, NT, HR, TR, LB, VB, RB, A, D, H, X, T, IH, IT, XX2, XX3, HR1, TR1, IT1, balance55_10_in_gaagggaaag10(R, XX2, XX3, NT, HR, TR, HR1, TR1, IT1, IT))
IF_BALANCE55_10_IN_1_GAAGGGGAAG19(L, V, R, XX0, XX1, NT, HR, TR, LB, VB, RB, A, D, H, X, T, IH, IT, balance55_10_out_gaagaaaaag10(L, XX0, XX1, ._22(tuple_22(nil_0, -2(XX2, XX2)), XX3), HR1, TR1, H, T, IH, ._22(V, IT1))) -> BALANCE55_10_IN_GAAGGGAAAG10(R, XX2, XX3, NT, HR, TR, HR1, TR1, IT1, IT)
BALANCE55_10_IN_GAAGGGAAAG10(tree_33(L, V, R), XX0, XX1, NT, HR, TR, ._22(tuple_22(tree_33(LB, VB, RB), -2(A, D)), H), ._22(tuple_22(LB, -2(A, ._22(VB, X))), ._22(tuple_22(RB, -2(X, D)), T)), IH, IT) -> IF_BALANCE55_10_IN_1_GAAGGGAAAG19(L, V, R, XX0, XX1, NT, HR, TR, LB, VB, RB, A, D, H, X, T, IH, IT, balance55_10_in_gaagaaaaag10(L, XX0, XX1, ._22(tuple_22(nil_0, -2(XX2, XX2)), XX3), HR1, TR1, H, T, IH, ._22(V, IT1)))
BALANCE55_10_IN_GAAGGGAAAG10(tree_33(L, V, R), XX0, XX1, NT, HR, TR, ._22(tuple_22(tree_33(LB, VB, RB), -2(A, D)), H), ._22(tuple_22(LB, -2(A, ._22(VB, X))), ._22(tuple_22(RB, -2(X, D)), T)), IH, IT) -> BALANCE55_10_IN_GAAGAAAAAG10(L, XX0, XX1, ._22(tuple_22(nil_0, -2(XX2, XX2)), XX3), HR1, TR1, H, T, IH, ._22(V, IT1))
IF_BALANCE55_10_IN_1_GAAGGGAAAG19(L, V, R, XX0, XX1, NT, HR, TR, LB, VB, RB, A, D, H, X, T, IH, IT, balance55_10_out_gaagaaaaag10(L, XX0, XX1, ._22(tuple_22(nil_0, -2(XX2, XX2)), XX3), HR1, TR1, H, T, IH, ._22(V, IT1))) -> IF_BALANCE55_10_IN_2_GAAGGGAAAG24(L, V, R, XX0, XX1, NT, HR, TR, LB, VB, RB, A, D, H, X, T, IH, IT, XX2, XX3, HR1, TR1, IT1, balance55_10_in_gaagggaaag10(R, XX2, XX3, NT, HR, TR, HR1, TR1, IT1, IT))
IF_BALANCE55_10_IN_1_GAAGGGAAAG19(L, V, R, XX0, XX1, NT, HR, TR, LB, VB, RB, A, D, H, X, T, IH, IT, balance55_10_out_gaagaaaaag10(L, XX0, XX1, ._22(tuple_22(nil_0, -2(XX2, XX2)), XX3), HR1, TR1, H, T, IH, ._22(V, IT1))) -> BALANCE55_10_IN_GAAGGGAAAG10(R, XX2, XX3, NT, HR, TR, HR1, TR1, IT1, IT)

The TRS R consists of the following rules:

balance_2_in_ga2(T, TB) -> if_balance_2_in_1_ga3(T, TB, balance55_10_in_gaaggggaag10(T, XX0, XX1, []_0, ._22(tuple_22(nil_0, -2(XX0, XX0)), XX1), []_0, ._22(tuple_22(TB, -2(I, []_0)), X), X, I, []_0))
balance55_10_in_gaaggggaag10(nil_0, C, T, T, A, B, A, B, X, X) -> balance55_10_out_gaaggggaag10(nil_0, C, T, T, A, B, A, B, X, X)
balance55_10_in_gaaggggaag10(tree_33(L, V, R), XX0, XX1, NT, HR, TR, ._22(tuple_22(tree_33(LB, VB, RB), -2(A, D)), H), ._22(tuple_22(LB, -2(A, ._22(VB, X))), ._22(tuple_22(RB, -2(X, D)), T)), IH, IT) -> if_balance55_10_in_1_gaaggggaag19(L, V, R, XX0, XX1, NT, HR, TR, LB, VB, RB, A, D, H, X, T, IH, IT, balance55_10_in_gaagaaaaag10(L, XX0, XX1, ._22(tuple_22(nil_0, -2(XX2, XX2)), XX3), HR1, TR1, H, T, IH, ._22(V, IT1)))
balance55_10_in_gaagaaaaag10(nil_0, C, T, T, A, B, A, B, X, X) -> balance55_10_out_gaagaaaaag10(nil_0, C, T, T, A, B, A, B, X, X)
balance55_10_in_gaagaaaaag10(tree_33(L, V, R), XX0, XX1, NT, HR, TR, ._22(tuple_22(tree_33(LB, VB, RB), -2(A, D)), H), ._22(tuple_22(LB, -2(A, ._22(VB, X))), ._22(tuple_22(RB, -2(X, D)), T)), IH, IT) -> if_balance55_10_in_1_gaagaaaaag19(L, V, R, XX0, XX1, NT, HR, TR, LB, VB, RB, A, D, H, X, T, IH, IT, balance55_10_in_gaagaaaaag10(L, XX0, XX1, ._22(tuple_22(nil_0, -2(XX2, XX2)), XX3), HR1, TR1, H, T, IH, ._22(V, IT1)))
if_balance55_10_in_1_gaagaaaaag19(L, V, R, XX0, XX1, NT, HR, TR, LB, VB, RB, A, D, H, X, T, IH, IT, balance55_10_out_gaagaaaaag10(L, XX0, XX1, ._22(tuple_22(nil_0, -2(XX2, XX2)), XX3), HR1, TR1, H, T, IH, ._22(V, IT1))) -> if_balance55_10_in_2_gaagaaaaag24(L, V, R, XX0, XX1, NT, HR, TR, LB, VB, RB, A, D, H, X, T, IH, IT, XX2, XX3, HR1, TR1, IT1, balance55_10_in_gaagaaaaag10(R, XX2, XX3, NT, HR, TR, HR1, TR1, IT1, IT))
if_balance55_10_in_2_gaagaaaaag24(L, V, R, XX0, XX1, NT, HR, TR, LB, VB, RB, A, D, H, X, T, IH, IT, XX2, XX3, HR1, TR1, IT1, balance55_10_out_gaagaaaaag10(R, XX2, XX3, NT, HR, TR, HR1, TR1, IT1, IT)) -> balance55_10_out_gaagaaaaag10(tree_33(L, V, R), XX0, XX1, NT, HR, TR, ._22(tuple_22(tree_33(LB, VB, RB), -2(A, D)), H), ._22(tuple_22(LB, -2(A, ._22(VB, X))), ._22(tuple_22(RB, -2(X, D)), T)), IH, IT)
if_balance55_10_in_1_gaaggggaag19(L, V, R, XX0, XX1, NT, HR, TR, LB, VB, RB, A, D, H, X, T, IH, IT, balance55_10_out_gaagaaaaag10(L, XX0, XX1, ._22(tuple_22(nil_0, -2(XX2, XX2)), XX3), HR1, TR1, H, T, IH, ._22(V, IT1))) -> if_balance55_10_in_2_gaaggggaag24(L, V, R, XX0, XX1, NT, HR, TR, LB, VB, RB, A, D, H, X, T, IH, IT, XX2, XX3, HR1, TR1, IT1, balance55_10_in_gaagggaaag10(R, XX2, XX3, NT, HR, TR, HR1, TR1, IT1, IT))
balance55_10_in_gaagggaaag10(nil_0, C, T, T, A, B, A, B, X, X) -> balance55_10_out_gaagggaaag10(nil_0, C, T, T, A, B, A, B, X, X)
balance55_10_in_gaagggaaag10(tree_33(L, V, R), XX0, XX1, NT, HR, TR, ._22(tuple_22(tree_33(LB, VB, RB), -2(A, D)), H), ._22(tuple_22(LB, -2(A, ._22(VB, X))), ._22(tuple_22(RB, -2(X, D)), T)), IH, IT) -> if_balance55_10_in_1_gaagggaaag19(L, V, R, XX0, XX1, NT, HR, TR, LB, VB, RB, A, D, H, X, T, IH, IT, balance55_10_in_gaagaaaaag10(L, XX0, XX1, ._22(tuple_22(nil_0, -2(XX2, XX2)), XX3), HR1, TR1, H, T, IH, ._22(V, IT1)))
if_balance55_10_in_1_gaagggaaag19(L, V, R, XX0, XX1, NT, HR, TR, LB, VB, RB, A, D, H, X, T, IH, IT, balance55_10_out_gaagaaaaag10(L, XX0, XX1, ._22(tuple_22(nil_0, -2(XX2, XX2)), XX3), HR1, TR1, H, T, IH, ._22(V, IT1))) -> if_balance55_10_in_2_gaagggaaag24(L, V, R, XX0, XX1, NT, HR, TR, LB, VB, RB, A, D, H, X, T, IH, IT, XX2, XX3, HR1, TR1, IT1, balance55_10_in_gaagggaaag10(R, XX2, XX3, NT, HR, TR, HR1, TR1, IT1, IT))
if_balance55_10_in_2_gaagggaaag24(L, V, R, XX0, XX1, NT, HR, TR, LB, VB, RB, A, D, H, X, T, IH, IT, XX2, XX3, HR1, TR1, IT1, balance55_10_out_gaagggaaag10(R, XX2, XX3, NT, HR, TR, HR1, TR1, IT1, IT)) -> balance55_10_out_gaagggaaag10(tree_33(L, V, R), XX0, XX1, NT, HR, TR, ._22(tuple_22(tree_33(LB, VB, RB), -2(A, D)), H), ._22(tuple_22(LB, -2(A, ._22(VB, X))), ._22(tuple_22(RB, -2(X, D)), T)), IH, IT)
if_balance55_10_in_2_gaaggggaag24(L, V, R, XX0, XX1, NT, HR, TR, LB, VB, RB, A, D, H, X, T, IH, IT, XX2, XX3, HR1, TR1, IT1, balance55_10_out_gaagggaaag10(R, XX2, XX3, NT, HR, TR, HR1, TR1, IT1, IT)) -> balance55_10_out_gaaggggaag10(tree_33(L, V, R), XX0, XX1, NT, HR, TR, ._22(tuple_22(tree_33(LB, VB, RB), -2(A, D)), H), ._22(tuple_22(LB, -2(A, ._22(VB, X))), ._22(tuple_22(RB, -2(X, D)), T)), IH, IT)
if_balance_2_in_1_ga3(T, TB, balance55_10_out_gaaggggaag10(T, XX0, XX1, []_0, ._22(tuple_22(nil_0, -2(XX0, XX0)), XX1), []_0, ._22(tuple_22(TB, -2(I, []_0)), X), X, I, []_0)) -> balance_2_out_ga2(T, TB)

The argument filtering Pi contains the following mapping:
balance_2_in_ga2(x1, x2)  =  balance_2_in_ga1(x1)
[]_0  =  []_0
._22(x1, x2)  =  ._21(x1)
tuple_22(x1, x2)  =  tuple_21(x2)
nil_0  =  nil_0
-2(x1, x2)  =  -
tree_33(x1, x2, x3)  =  tree_33(x1, x2, x3)
if_balance_2_in_1_ga3(x1, x2, x3)  =  if_balance_2_in_1_ga1(x3)
balance55_10_in_gaaggggaag10(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  balance55_10_in_gaaggggaag6(x1, x4, x5, x6, x7, x10)
balance55_10_out_gaaggggaag10(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  balance55_10_out_gaaggggaag3(x3, x8, x9)
if_balance55_10_in_1_gaaggggaag19(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19)  =  if_balance55_10_in_1_gaaggggaag6(x3, x6, x7, x8, x18, x19)
balance55_10_in_gaagaaaaag10(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  balance55_10_in_gaagaaaaag3(x1, x4, x10)
balance55_10_out_gaagaaaaag10(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  balance55_10_out_gaagaaaaag2(x3, x9)
if_balance55_10_in_1_gaagaaaaag19(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19)  =  if_balance55_10_in_1_gaagaaaaag4(x3, x6, x18, x19)
if_balance55_10_in_2_gaagaaaaag24(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22, x23, x24)  =  if_balance55_10_in_2_gaagaaaaag3(x5, x17, x24)
if_balance55_10_in_2_gaaggggaag24(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22, x23, x24)  =  if_balance55_10_in_2_gaaggggaag3(x5, x17, x24)
balance55_10_in_gaagggaaag10(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  balance55_10_in_gaagggaaag5(x1, x4, x5, x6, x10)
balance55_10_out_gaagggaaag10(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  balance55_10_out_gaagggaaag4(x3, x7, x8, x9)
if_balance55_10_in_1_gaagggaaag19(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19)  =  if_balance55_10_in_1_gaagggaaag6(x3, x6, x7, x8, x18, x19)
if_balance55_10_in_2_gaagggaaag24(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22, x23, x24)  =  if_balance55_10_in_2_gaagggaaag3(x5, x17, x24)
balance_2_out_ga2(x1, x2)  =  balance_2_out_ga
IF_BALANCE55_10_IN_2_GAAGAAAAAG24(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22, x23, x24)  =  IF_BALANCE55_10_IN_2_GAAGAAAAAG3(x5, x17, x24)
IF_BALANCE55_10_IN_1_GAAGGGGAAG19(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19)  =  IF_BALANCE55_10_IN_1_GAAGGGGAAG6(x3, x6, x7, x8, x18, x19)
IF_BALANCE_2_IN_1_GA3(x1, x2, x3)  =  IF_BALANCE_2_IN_1_GA1(x3)
BALANCE55_10_IN_GAAGGGGAAG10(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  BALANCE55_10_IN_GAAGGGGAAG6(x1, x4, x5, x6, x7, x10)
IF_BALANCE55_10_IN_1_GAAGGGAAAG19(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19)  =  IF_BALANCE55_10_IN_1_GAAGGGAAAG6(x3, x6, x7, x8, x18, x19)
IF_BALANCE55_10_IN_2_GAAGGGGAAG24(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22, x23, x24)  =  IF_BALANCE55_10_IN_2_GAAGGGGAAG3(x5, x17, x24)
IF_BALANCE55_10_IN_1_GAAGAAAAAG19(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19)  =  IF_BALANCE55_10_IN_1_GAAGAAAAAG4(x3, x6, x18, x19)
IF_BALANCE55_10_IN_2_GAAGGGAAAG24(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22, x23, x24)  =  IF_BALANCE55_10_IN_2_GAAGGGAAAG3(x5, x17, x24)
BALANCE55_10_IN_GAAGGGAAAG10(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  BALANCE55_10_IN_GAAGGGAAAG5(x1, x4, x5, x6, x10)
BALANCE55_10_IN_GAAGAAAAAG10(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  BALANCE55_10_IN_GAAGAAAAAG3(x1, x4, x10)
BALANCE_2_IN_GA2(x1, x2)  =  BALANCE_2_IN_GA1(x1)

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

↳ PROLOG
  ↳ UnrequestedClauseRemoverProof
    ↳ PROLOG
      ↳ PrologToPiTRSProof
        ↳ PiTRS
          ↳ DependencyPairsProof
            ↳ PiDP
              ↳ DependencyGraphProof

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

BALANCE_2_IN_GA2(T, TB) -> IF_BALANCE_2_IN_1_GA3(T, TB, balance55_10_in_gaaggggaag10(T, XX0, XX1, []_0, ._22(tuple_22(nil_0, -2(XX0, XX0)), XX1), []_0, ._22(tuple_22(TB, -2(I, []_0)), X), X, I, []_0))
BALANCE_2_IN_GA2(T, TB) -> BALANCE55_10_IN_GAAGGGGAAG10(T, XX0, XX1, []_0, ._22(tuple_22(nil_0, -2(XX0, XX0)), XX1), []_0, ._22(tuple_22(TB, -2(I, []_0)), X), X, I, []_0)
BALANCE55_10_IN_GAAGGGGAAG10(tree_33(L, V, R), XX0, XX1, NT, HR, TR, ._22(tuple_22(tree_33(LB, VB, RB), -2(A, D)), H), ._22(tuple_22(LB, -2(A, ._22(VB, X))), ._22(tuple_22(RB, -2(X, D)), T)), IH, IT) -> IF_BALANCE55_10_IN_1_GAAGGGGAAG19(L, V, R, XX0, XX1, NT, HR, TR, LB, VB, RB, A, D, H, X, T, IH, IT, balance55_10_in_gaagaaaaag10(L, XX0, XX1, ._22(tuple_22(nil_0, -2(XX2, XX2)), XX3), HR1, TR1, H, T, IH, ._22(V, IT1)))
BALANCE55_10_IN_GAAGGGGAAG10(tree_33(L, V, R), XX0, XX1, NT, HR, TR, ._22(tuple_22(tree_33(LB, VB, RB), -2(A, D)), H), ._22(tuple_22(LB, -2(A, ._22(VB, X))), ._22(tuple_22(RB, -2(X, D)), T)), IH, IT) -> BALANCE55_10_IN_GAAGAAAAAG10(L, XX0, XX1, ._22(tuple_22(nil_0, -2(XX2, XX2)), XX3), HR1, TR1, H, T, IH, ._22(V, IT1))
BALANCE55_10_IN_GAAGAAAAAG10(tree_33(L, V, R), XX0, XX1, NT, HR, TR, ._22(tuple_22(tree_33(LB, VB, RB), -2(A, D)), H), ._22(tuple_22(LB, -2(A, ._22(VB, X))), ._22(tuple_22(RB, -2(X, D)), T)), IH, IT) -> IF_BALANCE55_10_IN_1_GAAGAAAAAG19(L, V, R, XX0, XX1, NT, HR, TR, LB, VB, RB, A, D, H, X, T, IH, IT, balance55_10_in_gaagaaaaag10(L, XX0, XX1, ._22(tuple_22(nil_0, -2(XX2, XX2)), XX3), HR1, TR1, H, T, IH, ._22(V, IT1)))
BALANCE55_10_IN_GAAGAAAAAG10(tree_33(L, V, R), XX0, XX1, NT, HR, TR, ._22(tuple_22(tree_33(LB, VB, RB), -2(A, D)), H), ._22(tuple_22(LB, -2(A, ._22(VB, X))), ._22(tuple_22(RB, -2(X, D)), T)), IH, IT) -> BALANCE55_10_IN_GAAGAAAAAG10(L, XX0, XX1, ._22(tuple_22(nil_0, -2(XX2, XX2)), XX3), HR1, TR1, H, T, IH, ._22(V, IT1))
IF_BALANCE55_10_IN_1_GAAGAAAAAG19(L, V, R, XX0, XX1, NT, HR, TR, LB, VB, RB, A, D, H, X, T, IH, IT, balance55_10_out_gaagaaaaag10(L, XX0, XX1, ._22(tuple_22(nil_0, -2(XX2, XX2)), XX3), HR1, TR1, H, T, IH, ._22(V, IT1))) -> IF_BALANCE55_10_IN_2_GAAGAAAAAG24(L, V, R, XX0, XX1, NT, HR, TR, LB, VB, RB, A, D, H, X, T, IH, IT, XX2, XX3, HR1, TR1, IT1, balance55_10_in_gaagaaaaag10(R, XX2, XX3, NT, HR, TR, HR1, TR1, IT1, IT))
IF_BALANCE55_10_IN_1_GAAGAAAAAG19(L, V, R, XX0, XX1, NT, HR, TR, LB, VB, RB, A, D, H, X, T, IH, IT, balance55_10_out_gaagaaaaag10(L, XX0, XX1, ._22(tuple_22(nil_0, -2(XX2, XX2)), XX3), HR1, TR1, H, T, IH, ._22(V, IT1))) -> BALANCE55_10_IN_GAAGAAAAAG10(R, XX2, XX3, NT, HR, TR, HR1, TR1, IT1, IT)
IF_BALANCE55_10_IN_1_GAAGGGGAAG19(L, V, R, XX0, XX1, NT, HR, TR, LB, VB, RB, A, D, H, X, T, IH, IT, balance55_10_out_gaagaaaaag10(L, XX0, XX1, ._22(tuple_22(nil_0, -2(XX2, XX2)), XX3), HR1, TR1, H, T, IH, ._22(V, IT1))) -> IF_BALANCE55_10_IN_2_GAAGGGGAAG24(L, V, R, XX0, XX1, NT, HR, TR, LB, VB, RB, A, D, H, X, T, IH, IT, XX2, XX3, HR1, TR1, IT1, balance55_10_in_gaagggaaag10(R, XX2, XX3, NT, HR, TR, HR1, TR1, IT1, IT))
IF_BALANCE55_10_IN_1_GAAGGGGAAG19(L, V, R, XX0, XX1, NT, HR, TR, LB, VB, RB, A, D, H, X, T, IH, IT, balance55_10_out_gaagaaaaag10(L, XX0, XX1, ._22(tuple_22(nil_0, -2(XX2, XX2)), XX3), HR1, TR1, H, T, IH, ._22(V, IT1))) -> BALANCE55_10_IN_GAAGGGAAAG10(R, XX2, XX3, NT, HR, TR, HR1, TR1, IT1, IT)
BALANCE55_10_IN_GAAGGGAAAG10(tree_33(L, V, R), XX0, XX1, NT, HR, TR, ._22(tuple_22(tree_33(LB, VB, RB), -2(A, D)), H), ._22(tuple_22(LB, -2(A, ._22(VB, X))), ._22(tuple_22(RB, -2(X, D)), T)), IH, IT) -> IF_BALANCE55_10_IN_1_GAAGGGAAAG19(L, V, R, XX0, XX1, NT, HR, TR, LB, VB, RB, A, D, H, X, T, IH, IT, balance55_10_in_gaagaaaaag10(L, XX0, XX1, ._22(tuple_22(nil_0, -2(XX2, XX2)), XX3), HR1, TR1, H, T, IH, ._22(V, IT1)))
BALANCE55_10_IN_GAAGGGAAAG10(tree_33(L, V, R), XX0, XX1, NT, HR, TR, ._22(tuple_22(tree_33(LB, VB, RB), -2(A, D)), H), ._22(tuple_22(LB, -2(A, ._22(VB, X))), ._22(tuple_22(RB, -2(X, D)), T)), IH, IT) -> BALANCE55_10_IN_GAAGAAAAAG10(L, XX0, XX1, ._22(tuple_22(nil_0, -2(XX2, XX2)), XX3), HR1, TR1, H, T, IH, ._22(V, IT1))
IF_BALANCE55_10_IN_1_GAAGGGAAAG19(L, V, R, XX0, XX1, NT, HR, TR, LB, VB, RB, A, D, H, X, T, IH, IT, balance55_10_out_gaagaaaaag10(L, XX0, XX1, ._22(tuple_22(nil_0, -2(XX2, XX2)), XX3), HR1, TR1, H, T, IH, ._22(V, IT1))) -> IF_BALANCE55_10_IN_2_GAAGGGAAAG24(L, V, R, XX0, XX1, NT, HR, TR, LB, VB, RB, A, D, H, X, T, IH, IT, XX2, XX3, HR1, TR1, IT1, balance55_10_in_gaagggaaag10(R, XX2, XX3, NT, HR, TR, HR1, TR1, IT1, IT))
IF_BALANCE55_10_IN_1_GAAGGGAAAG19(L, V, R, XX0, XX1, NT, HR, TR, LB, VB, RB, A, D, H, X, T, IH, IT, balance55_10_out_gaagaaaaag10(L, XX0, XX1, ._22(tuple_22(nil_0, -2(XX2, XX2)), XX3), HR1, TR1, H, T, IH, ._22(V, IT1))) -> BALANCE55_10_IN_GAAGGGAAAG10(R, XX2, XX3, NT, HR, TR, HR1, TR1, IT1, IT)

The TRS R consists of the following rules:

balance_2_in_ga2(T, TB) -> if_balance_2_in_1_ga3(T, TB, balance55_10_in_gaaggggaag10(T, XX0, XX1, []_0, ._22(tuple_22(nil_0, -2(XX0, XX0)), XX1), []_0, ._22(tuple_22(TB, -2(I, []_0)), X), X, I, []_0))
balance55_10_in_gaaggggaag10(nil_0, C, T, T, A, B, A, B, X, X) -> balance55_10_out_gaaggggaag10(nil_0, C, T, T, A, B, A, B, X, X)
balance55_10_in_gaaggggaag10(tree_33(L, V, R), XX0, XX1, NT, HR, TR, ._22(tuple_22(tree_33(LB, VB, RB), -2(A, D)), H), ._22(tuple_22(LB, -2(A, ._22(VB, X))), ._22(tuple_22(RB, -2(X, D)), T)), IH, IT) -> if_balance55_10_in_1_gaaggggaag19(L, V, R, XX0, XX1, NT, HR, TR, LB, VB, RB, A, D, H, X, T, IH, IT, balance55_10_in_gaagaaaaag10(L, XX0, XX1, ._22(tuple_22(nil_0, -2(XX2, XX2)), XX3), HR1, TR1, H, T, IH, ._22(V, IT1)))
balance55_10_in_gaagaaaaag10(nil_0, C, T, T, A, B, A, B, X, X) -> balance55_10_out_gaagaaaaag10(nil_0, C, T, T, A, B, A, B, X, X)
balance55_10_in_gaagaaaaag10(tree_33(L, V, R), XX0, XX1, NT, HR, TR, ._22(tuple_22(tree_33(LB, VB, RB), -2(A, D)), H), ._22(tuple_22(LB, -2(A, ._22(VB, X))), ._22(tuple_22(RB, -2(X, D)), T)), IH, IT) -> if_balance55_10_in_1_gaagaaaaag19(L, V, R, XX0, XX1, NT, HR, TR, LB, VB, RB, A, D, H, X, T, IH, IT, balance55_10_in_gaagaaaaag10(L, XX0, XX1, ._22(tuple_22(nil_0, -2(XX2, XX2)), XX3), HR1, TR1, H, T, IH, ._22(V, IT1)))
if_balance55_10_in_1_gaagaaaaag19(L, V, R, XX0, XX1, NT, HR, TR, LB, VB, RB, A, D, H, X, T, IH, IT, balance55_10_out_gaagaaaaag10(L, XX0, XX1, ._22(tuple_22(nil_0, -2(XX2, XX2)), XX3), HR1, TR1, H, T, IH, ._22(V, IT1))) -> if_balance55_10_in_2_gaagaaaaag24(L, V, R, XX0, XX1, NT, HR, TR, LB, VB, RB, A, D, H, X, T, IH, IT, XX2, XX3, HR1, TR1, IT1, balance55_10_in_gaagaaaaag10(R, XX2, XX3, NT, HR, TR, HR1, TR1, IT1, IT))
if_balance55_10_in_2_gaagaaaaag24(L, V, R, XX0, XX1, NT, HR, TR, LB, VB, RB, A, D, H, X, T, IH, IT, XX2, XX3, HR1, TR1, IT1, balance55_10_out_gaagaaaaag10(R, XX2, XX3, NT, HR, TR, HR1, TR1, IT1, IT)) -> balance55_10_out_gaagaaaaag10(tree_33(L, V, R), XX0, XX1, NT, HR, TR, ._22(tuple_22(tree_33(LB, VB, RB), -2(A, D)), H), ._22(tuple_22(LB, -2(A, ._22(VB, X))), ._22(tuple_22(RB, -2(X, D)), T)), IH, IT)
if_balance55_10_in_1_gaaggggaag19(L, V, R, XX0, XX1, NT, HR, TR, LB, VB, RB, A, D, H, X, T, IH, IT, balance55_10_out_gaagaaaaag10(L, XX0, XX1, ._22(tuple_22(nil_0, -2(XX2, XX2)), XX3), HR1, TR1, H, T, IH, ._22(V, IT1))) -> if_balance55_10_in_2_gaaggggaag24(L, V, R, XX0, XX1, NT, HR, TR, LB, VB, RB, A, D, H, X, T, IH, IT, XX2, XX3, HR1, TR1, IT1, balance55_10_in_gaagggaaag10(R, XX2, XX3, NT, HR, TR, HR1, TR1, IT1, IT))
balance55_10_in_gaagggaaag10(nil_0, C, T, T, A, B, A, B, X, X) -> balance55_10_out_gaagggaaag10(nil_0, C, T, T, A, B, A, B, X, X)
balance55_10_in_gaagggaaag10(tree_33(L, V, R), XX0, XX1, NT, HR, TR, ._22(tuple_22(tree_33(LB, VB, RB), -2(A, D)), H), ._22(tuple_22(LB, -2(A, ._22(VB, X))), ._22(tuple_22(RB, -2(X, D)), T)), IH, IT) -> if_balance55_10_in_1_gaagggaaag19(L, V, R, XX0, XX1, NT, HR, TR, LB, VB, RB, A, D, H, X, T, IH, IT, balance55_10_in_gaagaaaaag10(L, XX0, XX1, ._22(tuple_22(nil_0, -2(XX2, XX2)), XX3), HR1, TR1, H, T, IH, ._22(V, IT1)))
if_balance55_10_in_1_gaagggaaag19(L, V, R, XX0, XX1, NT, HR, TR, LB, VB, RB, A, D, H, X, T, IH, IT, balance55_10_out_gaagaaaaag10(L, XX0, XX1, ._22(tuple_22(nil_0, -2(XX2, XX2)), XX3), HR1, TR1, H, T, IH, ._22(V, IT1))) -> if_balance55_10_in_2_gaagggaaag24(L, V, R, XX0, XX1, NT, HR, TR, LB, VB, RB, A, D, H, X, T, IH, IT, XX2, XX3, HR1, TR1, IT1, balance55_10_in_gaagggaaag10(R, XX2, XX3, NT, HR, TR, HR1, TR1, IT1, IT))
if_balance55_10_in_2_gaagggaaag24(L, V, R, XX0, XX1, NT, HR, TR, LB, VB, RB, A, D, H, X, T, IH, IT, XX2, XX3, HR1, TR1, IT1, balance55_10_out_gaagggaaag10(R, XX2, XX3, NT, HR, TR, HR1, TR1, IT1, IT)) -> balance55_10_out_gaagggaaag10(tree_33(L, V, R), XX0, XX1, NT, HR, TR, ._22(tuple_22(tree_33(LB, VB, RB), -2(A, D)), H), ._22(tuple_22(LB, -2(A, ._22(VB, X))), ._22(tuple_22(RB, -2(X, D)), T)), IH, IT)
if_balance55_10_in_2_gaaggggaag24(L, V, R, XX0, XX1, NT, HR, TR, LB, VB, RB, A, D, H, X, T, IH, IT, XX2, XX3, HR1, TR1, IT1, balance55_10_out_gaagggaaag10(R, XX2, XX3, NT, HR, TR, HR1, TR1, IT1, IT)) -> balance55_10_out_gaaggggaag10(tree_33(L, V, R), XX0, XX1, NT, HR, TR, ._22(tuple_22(tree_33(LB, VB, RB), -2(A, D)), H), ._22(tuple_22(LB, -2(A, ._22(VB, X))), ._22(tuple_22(RB, -2(X, D)), T)), IH, IT)
if_balance_2_in_1_ga3(T, TB, balance55_10_out_gaaggggaag10(T, XX0, XX1, []_0, ._22(tuple_22(nil_0, -2(XX0, XX0)), XX1), []_0, ._22(tuple_22(TB, -2(I, []_0)), X), X, I, []_0)) -> balance_2_out_ga2(T, TB)

The argument filtering Pi contains the following mapping:
balance_2_in_ga2(x1, x2)  =  balance_2_in_ga1(x1)
[]_0  =  []_0
._22(x1, x2)  =  ._21(x1)
tuple_22(x1, x2)  =  tuple_21(x2)
nil_0  =  nil_0
-2(x1, x2)  =  -
tree_33(x1, x2, x3)  =  tree_33(x1, x2, x3)
if_balance_2_in_1_ga3(x1, x2, x3)  =  if_balance_2_in_1_ga1(x3)
balance55_10_in_gaaggggaag10(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  balance55_10_in_gaaggggaag6(x1, x4, x5, x6, x7, x10)
balance55_10_out_gaaggggaag10(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  balance55_10_out_gaaggggaag3(x3, x8, x9)
if_balance55_10_in_1_gaaggggaag19(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19)  =  if_balance55_10_in_1_gaaggggaag6(x3, x6, x7, x8, x18, x19)
balance55_10_in_gaagaaaaag10(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  balance55_10_in_gaagaaaaag3(x1, x4, x10)
balance55_10_out_gaagaaaaag10(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  balance55_10_out_gaagaaaaag2(x3, x9)
if_balance55_10_in_1_gaagaaaaag19(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19)  =  if_balance55_10_in_1_gaagaaaaag4(x3, x6, x18, x19)
if_balance55_10_in_2_gaagaaaaag24(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22, x23, x24)  =  if_balance55_10_in_2_gaagaaaaag3(x5, x17, x24)
if_balance55_10_in_2_gaaggggaag24(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22, x23, x24)  =  if_balance55_10_in_2_gaaggggaag3(x5, x17, x24)
balance55_10_in_gaagggaaag10(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  balance55_10_in_gaagggaaag5(x1, x4, x5, x6, x10)
balance55_10_out_gaagggaaag10(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  balance55_10_out_gaagggaaag4(x3, x7, x8, x9)
if_balance55_10_in_1_gaagggaaag19(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19)  =  if_balance55_10_in_1_gaagggaaag6(x3, x6, x7, x8, x18, x19)
if_balance55_10_in_2_gaagggaaag24(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22, x23, x24)  =  if_balance55_10_in_2_gaagggaaag3(x5, x17, x24)
balance_2_out_ga2(x1, x2)  =  balance_2_out_ga
IF_BALANCE55_10_IN_2_GAAGAAAAAG24(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22, x23, x24)  =  IF_BALANCE55_10_IN_2_GAAGAAAAAG3(x5, x17, x24)
IF_BALANCE55_10_IN_1_GAAGGGGAAG19(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19)  =  IF_BALANCE55_10_IN_1_GAAGGGGAAG6(x3, x6, x7, x8, x18, x19)
IF_BALANCE_2_IN_1_GA3(x1, x2, x3)  =  IF_BALANCE_2_IN_1_GA1(x3)
BALANCE55_10_IN_GAAGGGGAAG10(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  BALANCE55_10_IN_GAAGGGGAAG6(x1, x4, x5, x6, x7, x10)
IF_BALANCE55_10_IN_1_GAAGGGAAAG19(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19)  =  IF_BALANCE55_10_IN_1_GAAGGGAAAG6(x3, x6, x7, x8, x18, x19)
IF_BALANCE55_10_IN_2_GAAGGGGAAG24(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22, x23, x24)  =  IF_BALANCE55_10_IN_2_GAAGGGGAAG3(x5, x17, x24)
IF_BALANCE55_10_IN_1_GAAGAAAAAG19(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19)  =  IF_BALANCE55_10_IN_1_GAAGAAAAAG4(x3, x6, x18, x19)
IF_BALANCE55_10_IN_2_GAAGGGAAAG24(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22, x23, x24)  =  IF_BALANCE55_10_IN_2_GAAGGGAAAG3(x5, x17, x24)
BALANCE55_10_IN_GAAGGGAAAG10(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  BALANCE55_10_IN_GAAGGGAAAG5(x1, x4, x5, x6, x10)
BALANCE55_10_IN_GAAGAAAAAG10(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  BALANCE55_10_IN_GAAGAAAAAG3(x1, x4, x10)
BALANCE_2_IN_GA2(x1, x2)  =  BALANCE_2_IN_GA1(x1)

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

↳ PROLOG
  ↳ UnrequestedClauseRemoverProof
    ↳ PROLOG
      ↳ PrologToPiTRSProof
        ↳ PiTRS
          ↳ DependencyPairsProof
            ↳ PiDP
              ↳ DependencyGraphProof
                ↳ AND
                  ↳ PiDP
                    ↳ UsableRulesProof
                  ↳ PiDP

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

IF_BALANCE55_10_IN_1_GAAGAAAAAG19(L, V, R, XX0, XX1, NT, HR, TR, LB, VB, RB, A, D, H, X, T, IH, IT, balance55_10_out_gaagaaaaag10(L, XX0, XX1, ._22(tuple_22(nil_0, -2(XX2, XX2)), XX3), HR1, TR1, H, T, IH, ._22(V, IT1))) -> BALANCE55_10_IN_GAAGAAAAAG10(R, XX2, XX3, NT, HR, TR, HR1, TR1, IT1, IT)
BALANCE55_10_IN_GAAGAAAAAG10(tree_33(L, V, R), XX0, XX1, NT, HR, TR, ._22(tuple_22(tree_33(LB, VB, RB), -2(A, D)), H), ._22(tuple_22(LB, -2(A, ._22(VB, X))), ._22(tuple_22(RB, -2(X, D)), T)), IH, IT) -> IF_BALANCE55_10_IN_1_GAAGAAAAAG19(L, V, R, XX0, XX1, NT, HR, TR, LB, VB, RB, A, D, H, X, T, IH, IT, balance55_10_in_gaagaaaaag10(L, XX0, XX1, ._22(tuple_22(nil_0, -2(XX2, XX2)), XX3), HR1, TR1, H, T, IH, ._22(V, IT1)))
BALANCE55_10_IN_GAAGAAAAAG10(tree_33(L, V, R), XX0, XX1, NT, HR, TR, ._22(tuple_22(tree_33(LB, VB, RB), -2(A, D)), H), ._22(tuple_22(LB, -2(A, ._22(VB, X))), ._22(tuple_22(RB, -2(X, D)), T)), IH, IT) -> BALANCE55_10_IN_GAAGAAAAAG10(L, XX0, XX1, ._22(tuple_22(nil_0, -2(XX2, XX2)), XX3), HR1, TR1, H, T, IH, ._22(V, IT1))

The TRS R consists of the following rules:

balance_2_in_ga2(T, TB) -> if_balance_2_in_1_ga3(T, TB, balance55_10_in_gaaggggaag10(T, XX0, XX1, []_0, ._22(tuple_22(nil_0, -2(XX0, XX0)), XX1), []_0, ._22(tuple_22(TB, -2(I, []_0)), X), X, I, []_0))
balance55_10_in_gaaggggaag10(nil_0, C, T, T, A, B, A, B, X, X) -> balance55_10_out_gaaggggaag10(nil_0, C, T, T, A, B, A, B, X, X)
balance55_10_in_gaaggggaag10(tree_33(L, V, R), XX0, XX1, NT, HR, TR, ._22(tuple_22(tree_33(LB, VB, RB), -2(A, D)), H), ._22(tuple_22(LB, -2(A, ._22(VB, X))), ._22(tuple_22(RB, -2(X, D)), T)), IH, IT) -> if_balance55_10_in_1_gaaggggaag19(L, V, R, XX0, XX1, NT, HR, TR, LB, VB, RB, A, D, H, X, T, IH, IT, balance55_10_in_gaagaaaaag10(L, XX0, XX1, ._22(tuple_22(nil_0, -2(XX2, XX2)), XX3), HR1, TR1, H, T, IH, ._22(V, IT1)))
balance55_10_in_gaagaaaaag10(nil_0, C, T, T, A, B, A, B, X, X) -> balance55_10_out_gaagaaaaag10(nil_0, C, T, T, A, B, A, B, X, X)
balance55_10_in_gaagaaaaag10(tree_33(L, V, R), XX0, XX1, NT, HR, TR, ._22(tuple_22(tree_33(LB, VB, RB), -2(A, D)), H), ._22(tuple_22(LB, -2(A, ._22(VB, X))), ._22(tuple_22(RB, -2(X, D)), T)), IH, IT) -> if_balance55_10_in_1_gaagaaaaag19(L, V, R, XX0, XX1, NT, HR, TR, LB, VB, RB, A, D, H, X, T, IH, IT, balance55_10_in_gaagaaaaag10(L, XX0, XX1, ._22(tuple_22(nil_0, -2(XX2, XX2)), XX3), HR1, TR1, H, T, IH, ._22(V, IT1)))
if_balance55_10_in_1_gaagaaaaag19(L, V, R, XX0, XX1, NT, HR, TR, LB, VB, RB, A, D, H, X, T, IH, IT, balance55_10_out_gaagaaaaag10(L, XX0, XX1, ._22(tuple_22(nil_0, -2(XX2, XX2)), XX3), HR1, TR1, H, T, IH, ._22(V, IT1))) -> if_balance55_10_in_2_gaagaaaaag24(L, V, R, XX0, XX1, NT, HR, TR, LB, VB, RB, A, D, H, X, T, IH, IT, XX2, XX3, HR1, TR1, IT1, balance55_10_in_gaagaaaaag10(R, XX2, XX3, NT, HR, TR, HR1, TR1, IT1, IT))
if_balance55_10_in_2_gaagaaaaag24(L, V, R, XX0, XX1, NT, HR, TR, LB, VB, RB, A, D, H, X, T, IH, IT, XX2, XX3, HR1, TR1, IT1, balance55_10_out_gaagaaaaag10(R, XX2, XX3, NT, HR, TR, HR1, TR1, IT1, IT)) -> balance55_10_out_gaagaaaaag10(tree_33(L, V, R), XX0, XX1, NT, HR, TR, ._22(tuple_22(tree_33(LB, VB, RB), -2(A, D)), H), ._22(tuple_22(LB, -2(A, ._22(VB, X))), ._22(tuple_22(RB, -2(X, D)), T)), IH, IT)
if_balance55_10_in_1_gaaggggaag19(L, V, R, XX0, XX1, NT, HR, TR, LB, VB, RB, A, D, H, X, T, IH, IT, balance55_10_out_gaagaaaaag10(L, XX0, XX1, ._22(tuple_22(nil_0, -2(XX2, XX2)), XX3), HR1, TR1, H, T, IH, ._22(V, IT1))) -> if_balance55_10_in_2_gaaggggaag24(L, V, R, XX0, XX1, NT, HR, TR, LB, VB, RB, A, D, H, X, T, IH, IT, XX2, XX3, HR1, TR1, IT1, balance55_10_in_gaagggaaag10(R, XX2, XX3, NT, HR, TR, HR1, TR1, IT1, IT))
balance55_10_in_gaagggaaag10(nil_0, C, T, T, A, B, A, B, X, X) -> balance55_10_out_gaagggaaag10(nil_0, C, T, T, A, B, A, B, X, X)
balance55_10_in_gaagggaaag10(tree_33(L, V, R), XX0, XX1, NT, HR, TR, ._22(tuple_22(tree_33(LB, VB, RB), -2(A, D)), H), ._22(tuple_22(LB, -2(A, ._22(VB, X))), ._22(tuple_22(RB, -2(X, D)), T)), IH, IT) -> if_balance55_10_in_1_gaagggaaag19(L, V, R, XX0, XX1, NT, HR, TR, LB, VB, RB, A, D, H, X, T, IH, IT, balance55_10_in_gaagaaaaag10(L, XX0, XX1, ._22(tuple_22(nil_0, -2(XX2, XX2)), XX3), HR1, TR1, H, T, IH, ._22(V, IT1)))
if_balance55_10_in_1_gaagggaaag19(L, V, R, XX0, XX1, NT, HR, TR, LB, VB, RB, A, D, H, X, T, IH, IT, balance55_10_out_gaagaaaaag10(L, XX0, XX1, ._22(tuple_22(nil_0, -2(XX2, XX2)), XX3), HR1, TR1, H, T, IH, ._22(V, IT1))) -> if_balance55_10_in_2_gaagggaaag24(L, V, R, XX0, XX1, NT, HR, TR, LB, VB, RB, A, D, H, X, T, IH, IT, XX2, XX3, HR1, TR1, IT1, balance55_10_in_gaagggaaag10(R, XX2, XX3, NT, HR, TR, HR1, TR1, IT1, IT))
if_balance55_10_in_2_gaagggaaag24(L, V, R, XX0, XX1, NT, HR, TR, LB, VB, RB, A, D, H, X, T, IH, IT, XX2, XX3, HR1, TR1, IT1, balance55_10_out_gaagggaaag10(R, XX2, XX3, NT, HR, TR, HR1, TR1, IT1, IT)) -> balance55_10_out_gaagggaaag10(tree_33(L, V, R), XX0, XX1, NT, HR, TR, ._22(tuple_22(tree_33(LB, VB, RB), -2(A, D)), H), ._22(tuple_22(LB, -2(A, ._22(VB, X))), ._22(tuple_22(RB, -2(X, D)), T)), IH, IT)
if_balance55_10_in_2_gaaggggaag24(L, V, R, XX0, XX1, NT, HR, TR, LB, VB, RB, A, D, H, X, T, IH, IT, XX2, XX3, HR1, TR1, IT1, balance55_10_out_gaagggaaag10(R, XX2, XX3, NT, HR, TR, HR1, TR1, IT1, IT)) -> balance55_10_out_gaaggggaag10(tree_33(L, V, R), XX0, XX1, NT, HR, TR, ._22(tuple_22(tree_33(LB, VB, RB), -2(A, D)), H), ._22(tuple_22(LB, -2(A, ._22(VB, X))), ._22(tuple_22(RB, -2(X, D)), T)), IH, IT)
if_balance_2_in_1_ga3(T, TB, balance55_10_out_gaaggggaag10(T, XX0, XX1, []_0, ._22(tuple_22(nil_0, -2(XX0, XX0)), XX1), []_0, ._22(tuple_22(TB, -2(I, []_0)), X), X, I, []_0)) -> balance_2_out_ga2(T, TB)

The argument filtering Pi contains the following mapping:
balance_2_in_ga2(x1, x2)  =  balance_2_in_ga1(x1)
[]_0  =  []_0
._22(x1, x2)  =  ._21(x1)
tuple_22(x1, x2)  =  tuple_21(x2)
nil_0  =  nil_0
-2(x1, x2)  =  -
tree_33(x1, x2, x3)  =  tree_33(x1, x2, x3)
if_balance_2_in_1_ga3(x1, x2, x3)  =  if_balance_2_in_1_ga1(x3)
balance55_10_in_gaaggggaag10(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  balance55_10_in_gaaggggaag6(x1, x4, x5, x6, x7, x10)
balance55_10_out_gaaggggaag10(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  balance55_10_out_gaaggggaag3(x3, x8, x9)
if_balance55_10_in_1_gaaggggaag19(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19)  =  if_balance55_10_in_1_gaaggggaag6(x3, x6, x7, x8, x18, x19)
balance55_10_in_gaagaaaaag10(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  balance55_10_in_gaagaaaaag3(x1, x4, x10)
balance55_10_out_gaagaaaaag10(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  balance55_10_out_gaagaaaaag2(x3, x9)
if_balance55_10_in_1_gaagaaaaag19(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19)  =  if_balance55_10_in_1_gaagaaaaag4(x3, x6, x18, x19)
if_balance55_10_in_2_gaagaaaaag24(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22, x23, x24)  =  if_balance55_10_in_2_gaagaaaaag3(x5, x17, x24)
if_balance55_10_in_2_gaaggggaag24(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22, x23, x24)  =  if_balance55_10_in_2_gaaggggaag3(x5, x17, x24)
balance55_10_in_gaagggaaag10(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  balance55_10_in_gaagggaaag5(x1, x4, x5, x6, x10)
balance55_10_out_gaagggaaag10(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  balance55_10_out_gaagggaaag4(x3, x7, x8, x9)
if_balance55_10_in_1_gaagggaaag19(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19)  =  if_balance55_10_in_1_gaagggaaag6(x3, x6, x7, x8, x18, x19)
if_balance55_10_in_2_gaagggaaag24(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22, x23, x24)  =  if_balance55_10_in_2_gaagggaaag3(x5, x17, x24)
balance_2_out_ga2(x1, x2)  =  balance_2_out_ga
IF_BALANCE55_10_IN_1_GAAGAAAAAG19(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19)  =  IF_BALANCE55_10_IN_1_GAAGAAAAAG4(x3, x6, x18, x19)
BALANCE55_10_IN_GAAGAAAAAG10(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  BALANCE55_10_IN_GAAGAAAAAG3(x1, x4, x10)

We have to consider all (P,R,Pi)-chains
For (infinitary) constructor rewriting we can delete all non-usable rules from R.

↳ PROLOG
  ↳ UnrequestedClauseRemoverProof
    ↳ PROLOG
      ↳ PrologToPiTRSProof
        ↳ PiTRS
          ↳ DependencyPairsProof
            ↳ PiDP
              ↳ DependencyGraphProof
                ↳ AND
                  ↳ PiDP
                    ↳ UsableRulesProof
                      ↳ PiDP
                        ↳ PiDPToQDPProof
                  ↳ PiDP

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

IF_BALANCE55_10_IN_1_GAAGAAAAAG19(L, V, R, XX0, XX1, NT, HR, TR, LB, VB, RB, A, D, H, X, T, IH, IT, balance55_10_out_gaagaaaaag10(L, XX0, XX1, ._22(tuple_22(nil_0, -2(XX2, XX2)), XX3), HR1, TR1, H, T, IH, ._22(V, IT1))) -> BALANCE55_10_IN_GAAGAAAAAG10(R, XX2, XX3, NT, HR, TR, HR1, TR1, IT1, IT)
BALANCE55_10_IN_GAAGAAAAAG10(tree_33(L, V, R), XX0, XX1, NT, HR, TR, ._22(tuple_22(tree_33(LB, VB, RB), -2(A, D)), H), ._22(tuple_22(LB, -2(A, ._22(VB, X))), ._22(tuple_22(RB, -2(X, D)), T)), IH, IT) -> IF_BALANCE55_10_IN_1_GAAGAAAAAG19(L, V, R, XX0, XX1, NT, HR, TR, LB, VB, RB, A, D, H, X, T, IH, IT, balance55_10_in_gaagaaaaag10(L, XX0, XX1, ._22(tuple_22(nil_0, -2(XX2, XX2)), XX3), HR1, TR1, H, T, IH, ._22(V, IT1)))
BALANCE55_10_IN_GAAGAAAAAG10(tree_33(L, V, R), XX0, XX1, NT, HR, TR, ._22(tuple_22(tree_33(LB, VB, RB), -2(A, D)), H), ._22(tuple_22(LB, -2(A, ._22(VB, X))), ._22(tuple_22(RB, -2(X, D)), T)), IH, IT) -> BALANCE55_10_IN_GAAGAAAAAG10(L, XX0, XX1, ._22(tuple_22(nil_0, -2(XX2, XX2)), XX3), HR1, TR1, H, T, IH, ._22(V, IT1))

The TRS R consists of the following rules:

balance55_10_in_gaagaaaaag10(nil_0, C, T, T, A, B, A, B, X, X) -> balance55_10_out_gaagaaaaag10(nil_0, C, T, T, A, B, A, B, X, X)
balance55_10_in_gaagaaaaag10(tree_33(L, V, R), XX0, XX1, NT, HR, TR, ._22(tuple_22(tree_33(LB, VB, RB), -2(A, D)), H), ._22(tuple_22(LB, -2(A, ._22(VB, X))), ._22(tuple_22(RB, -2(X, D)), T)), IH, IT) -> if_balance55_10_in_1_gaagaaaaag19(L, V, R, XX0, XX1, NT, HR, TR, LB, VB, RB, A, D, H, X, T, IH, IT, balance55_10_in_gaagaaaaag10(L, XX0, XX1, ._22(tuple_22(nil_0, -2(XX2, XX2)), XX3), HR1, TR1, H, T, IH, ._22(V, IT1)))
if_balance55_10_in_1_gaagaaaaag19(L, V, R, XX0, XX1, NT, HR, TR, LB, VB, RB, A, D, H, X, T, IH, IT, balance55_10_out_gaagaaaaag10(L, XX0, XX1, ._22(tuple_22(nil_0, -2(XX2, XX2)), XX3), HR1, TR1, H, T, IH, ._22(V, IT1))) -> if_balance55_10_in_2_gaagaaaaag24(L, V, R, XX0, XX1, NT, HR, TR, LB, VB, RB, A, D, H, X, T, IH, IT, XX2, XX3, HR1, TR1, IT1, balance55_10_in_gaagaaaaag10(R, XX2, XX3, NT, HR, TR, HR1, TR1, IT1, IT))
if_balance55_10_in_2_gaagaaaaag24(L, V, R, XX0, XX1, NT, HR, TR, LB, VB, RB, A, D, H, X, T, IH, IT, XX2, XX3, HR1, TR1, IT1, balance55_10_out_gaagaaaaag10(R, XX2, XX3, NT, HR, TR, HR1, TR1, IT1, IT)) -> balance55_10_out_gaagaaaaag10(tree_33(L, V, R), XX0, XX1, NT, HR, TR, ._22(tuple_22(tree_33(LB, VB, RB), -2(A, D)), H), ._22(tuple_22(LB, -2(A, ._22(VB, X))), ._22(tuple_22(RB, -2(X, D)), T)), IH, IT)

The argument filtering Pi contains the following mapping:
._22(x1, x2)  =  ._21(x1)
tuple_22(x1, x2)  =  tuple_21(x2)
nil_0  =  nil_0
-2(x1, x2)  =  -
tree_33(x1, x2, x3)  =  tree_33(x1, x2, x3)
balance55_10_in_gaagaaaaag10(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  balance55_10_in_gaagaaaaag3(x1, x4, x10)
balance55_10_out_gaagaaaaag10(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  balance55_10_out_gaagaaaaag2(x3, x9)
if_balance55_10_in_1_gaagaaaaag19(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19)  =  if_balance55_10_in_1_gaagaaaaag4(x3, x6, x18, x19)
if_balance55_10_in_2_gaagaaaaag24(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22, x23, x24)  =  if_balance55_10_in_2_gaagaaaaag3(x5, x17, x24)
IF_BALANCE55_10_IN_1_GAAGAAAAAG19(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19)  =  IF_BALANCE55_10_IN_1_GAAGAAAAAG4(x3, x6, x18, x19)
BALANCE55_10_IN_GAAGAAAAAG10(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  BALANCE55_10_IN_GAAGAAAAAG3(x1, x4, x10)

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
  ↳ UnrequestedClauseRemoverProof
    ↳ PROLOG
      ↳ PrologToPiTRSProof
        ↳ PiTRS
          ↳ DependencyPairsProof
            ↳ PiDP
              ↳ DependencyGraphProof
                ↳ AND
                  ↳ PiDP
                    ↳ UsableRulesProof
                      ↳ PiDP
                        ↳ PiDPToQDPProof
                          ↳ QDP
                            ↳ QDPSizeChangeProof
                  ↳ PiDP

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

IF_BALANCE55_10_IN_1_GAAGAAAAAG4(R, NT, IT, balance55_10_out_gaagaaaaag2(XX1, IH)) -> BALANCE55_10_IN_GAAGAAAAAG3(R, NT, IT)
BALANCE55_10_IN_GAAGAAAAAG3(tree_33(L, V, R), NT, IT) -> IF_BALANCE55_10_IN_1_GAAGAAAAAG4(R, NT, IT, balance55_10_in_gaagaaaaag3(L, ._21(tuple_21(-)), ._21(V)))
BALANCE55_10_IN_GAAGAAAAAG3(tree_33(L, V, R), NT, IT) -> BALANCE55_10_IN_GAAGAAAAAG3(L, ._21(tuple_21(-)), ._21(V))

The TRS R consists of the following rules:

balance55_10_in_gaagaaaaag3(nil_0, T, X) -> balance55_10_out_gaagaaaaag2(T, X)
balance55_10_in_gaagaaaaag3(tree_33(L, V, R), NT, IT) -> if_balance55_10_in_1_gaagaaaaag4(R, NT, IT, balance55_10_in_gaagaaaaag3(L, ._21(tuple_21(-)), ._21(V)))
if_balance55_10_in_1_gaagaaaaag4(R, NT, IT, balance55_10_out_gaagaaaaag2(XX1, IH)) -> if_balance55_10_in_2_gaagaaaaag3(XX1, IH, balance55_10_in_gaagaaaaag3(R, NT, IT))
if_balance55_10_in_2_gaagaaaaag3(XX1, IH, balance55_10_out_gaagaaaaag2(XX3, IT1)) -> balance55_10_out_gaagaaaaag2(XX1, IH)

The set Q consists of the following terms:

balance55_10_in_gaagaaaaag3(x0, x1, x2)
if_balance55_10_in_1_gaagaaaaag4(x0, x1, x2, x3)
if_balance55_10_in_2_gaagaaaaag3(x0, x1, x2)

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

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



↳ PROLOG
  ↳ UnrequestedClauseRemoverProof
    ↳ PROLOG
      ↳ PrologToPiTRSProof
        ↳ PiTRS
          ↳ DependencyPairsProof
            ↳ PiDP
              ↳ DependencyGraphProof
                ↳ AND
                  ↳ PiDP
                  ↳ PiDP
                    ↳ UsableRulesProof

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

BALANCE55_10_IN_GAAGGGAAAG10(tree_33(L, V, R), XX0, XX1, NT, HR, TR, ._22(tuple_22(tree_33(LB, VB, RB), -2(A, D)), H), ._22(tuple_22(LB, -2(A, ._22(VB, X))), ._22(tuple_22(RB, -2(X, D)), T)), IH, IT) -> IF_BALANCE55_10_IN_1_GAAGGGAAAG19(L, V, R, XX0, XX1, NT, HR, TR, LB, VB, RB, A, D, H, X, T, IH, IT, balance55_10_in_gaagaaaaag10(L, XX0, XX1, ._22(tuple_22(nil_0, -2(XX2, XX2)), XX3), HR1, TR1, H, T, IH, ._22(V, IT1)))
IF_BALANCE55_10_IN_1_GAAGGGAAAG19(L, V, R, XX0, XX1, NT, HR, TR, LB, VB, RB, A, D, H, X, T, IH, IT, balance55_10_out_gaagaaaaag10(L, XX0, XX1, ._22(tuple_22(nil_0, -2(XX2, XX2)), XX3), HR1, TR1, H, T, IH, ._22(V, IT1))) -> BALANCE55_10_IN_GAAGGGAAAG10(R, XX2, XX3, NT, HR, TR, HR1, TR1, IT1, IT)

The TRS R consists of the following rules:

balance_2_in_ga2(T, TB) -> if_balance_2_in_1_ga3(T, TB, balance55_10_in_gaaggggaag10(T, XX0, XX1, []_0, ._22(tuple_22(nil_0, -2(XX0, XX0)), XX1), []_0, ._22(tuple_22(TB, -2(I, []_0)), X), X, I, []_0))
balance55_10_in_gaaggggaag10(nil_0, C, T, T, A, B, A, B, X, X) -> balance55_10_out_gaaggggaag10(nil_0, C, T, T, A, B, A, B, X, X)
balance55_10_in_gaaggggaag10(tree_33(L, V, R), XX0, XX1, NT, HR, TR, ._22(tuple_22(tree_33(LB, VB, RB), -2(A, D)), H), ._22(tuple_22(LB, -2(A, ._22(VB, X))), ._22(tuple_22(RB, -2(X, D)), T)), IH, IT) -> if_balance55_10_in_1_gaaggggaag19(L, V, R, XX0, XX1, NT, HR, TR, LB, VB, RB, A, D, H, X, T, IH, IT, balance55_10_in_gaagaaaaag10(L, XX0, XX1, ._22(tuple_22(nil_0, -2(XX2, XX2)), XX3), HR1, TR1, H, T, IH, ._22(V, IT1)))
balance55_10_in_gaagaaaaag10(nil_0, C, T, T, A, B, A, B, X, X) -> balance55_10_out_gaagaaaaag10(nil_0, C, T, T, A, B, A, B, X, X)
balance55_10_in_gaagaaaaag10(tree_33(L, V, R), XX0, XX1, NT, HR, TR, ._22(tuple_22(tree_33(LB, VB, RB), -2(A, D)), H), ._22(tuple_22(LB, -2(A, ._22(VB, X))), ._22(tuple_22(RB, -2(X, D)), T)), IH, IT) -> if_balance55_10_in_1_gaagaaaaag19(L, V, R, XX0, XX1, NT, HR, TR, LB, VB, RB, A, D, H, X, T, IH, IT, balance55_10_in_gaagaaaaag10(L, XX0, XX1, ._22(tuple_22(nil_0, -2(XX2, XX2)), XX3), HR1, TR1, H, T, IH, ._22(V, IT1)))
if_balance55_10_in_1_gaagaaaaag19(L, V, R, XX0, XX1, NT, HR, TR, LB, VB, RB, A, D, H, X, T, IH, IT, balance55_10_out_gaagaaaaag10(L, XX0, XX1, ._22(tuple_22(nil_0, -2(XX2, XX2)), XX3), HR1, TR1, H, T, IH, ._22(V, IT1))) -> if_balance55_10_in_2_gaagaaaaag24(L, V, R, XX0, XX1, NT, HR, TR, LB, VB, RB, A, D, H, X, T, IH, IT, XX2, XX3, HR1, TR1, IT1, balance55_10_in_gaagaaaaag10(R, XX2, XX3, NT, HR, TR, HR1, TR1, IT1, IT))
if_balance55_10_in_2_gaagaaaaag24(L, V, R, XX0, XX1, NT, HR, TR, LB, VB, RB, A, D, H, X, T, IH, IT, XX2, XX3, HR1, TR1, IT1, balance55_10_out_gaagaaaaag10(R, XX2, XX3, NT, HR, TR, HR1, TR1, IT1, IT)) -> balance55_10_out_gaagaaaaag10(tree_33(L, V, R), XX0, XX1, NT, HR, TR, ._22(tuple_22(tree_33(LB, VB, RB), -2(A, D)), H), ._22(tuple_22(LB, -2(A, ._22(VB, X))), ._22(tuple_22(RB, -2(X, D)), T)), IH, IT)
if_balance55_10_in_1_gaaggggaag19(L, V, R, XX0, XX1, NT, HR, TR, LB, VB, RB, A, D, H, X, T, IH, IT, balance55_10_out_gaagaaaaag10(L, XX0, XX1, ._22(tuple_22(nil_0, -2(XX2, XX2)), XX3), HR1, TR1, H, T, IH, ._22(V, IT1))) -> if_balance55_10_in_2_gaaggggaag24(L, V, R, XX0, XX1, NT, HR, TR, LB, VB, RB, A, D, H, X, T, IH, IT, XX2, XX3, HR1, TR1, IT1, balance55_10_in_gaagggaaag10(R, XX2, XX3, NT, HR, TR, HR1, TR1, IT1, IT))
balance55_10_in_gaagggaaag10(nil_0, C, T, T, A, B, A, B, X, X) -> balance55_10_out_gaagggaaag10(nil_0, C, T, T, A, B, A, B, X, X)
balance55_10_in_gaagggaaag10(tree_33(L, V, R), XX0, XX1, NT, HR, TR, ._22(tuple_22(tree_33(LB, VB, RB), -2(A, D)), H), ._22(tuple_22(LB, -2(A, ._22(VB, X))), ._22(tuple_22(RB, -2(X, D)), T)), IH, IT) -> if_balance55_10_in_1_gaagggaaag19(L, V, R, XX0, XX1, NT, HR, TR, LB, VB, RB, A, D, H, X, T, IH, IT, balance55_10_in_gaagaaaaag10(L, XX0, XX1, ._22(tuple_22(nil_0, -2(XX2, XX2)), XX3), HR1, TR1, H, T, IH, ._22(V, IT1)))
if_balance55_10_in_1_gaagggaaag19(L, V, R, XX0, XX1, NT, HR, TR, LB, VB, RB, A, D, H, X, T, IH, IT, balance55_10_out_gaagaaaaag10(L, XX0, XX1, ._22(tuple_22(nil_0, -2(XX2, XX2)), XX3), HR1, TR1, H, T, IH, ._22(V, IT1))) -> if_balance55_10_in_2_gaagggaaag24(L, V, R, XX0, XX1, NT, HR, TR, LB, VB, RB, A, D, H, X, T, IH, IT, XX2, XX3, HR1, TR1, IT1, balance55_10_in_gaagggaaag10(R, XX2, XX3, NT, HR, TR, HR1, TR1, IT1, IT))
if_balance55_10_in_2_gaagggaaag24(L, V, R, XX0, XX1, NT, HR, TR, LB, VB, RB, A, D, H, X, T, IH, IT, XX2, XX3, HR1, TR1, IT1, balance55_10_out_gaagggaaag10(R, XX2, XX3, NT, HR, TR, HR1, TR1, IT1, IT)) -> balance55_10_out_gaagggaaag10(tree_33(L, V, R), XX0, XX1, NT, HR, TR, ._22(tuple_22(tree_33(LB, VB, RB), -2(A, D)), H), ._22(tuple_22(LB, -2(A, ._22(VB, X))), ._22(tuple_22(RB, -2(X, D)), T)), IH, IT)
if_balance55_10_in_2_gaaggggaag24(L, V, R, XX0, XX1, NT, HR, TR, LB, VB, RB, A, D, H, X, T, IH, IT, XX2, XX3, HR1, TR1, IT1, balance55_10_out_gaagggaaag10(R, XX2, XX3, NT, HR, TR, HR1, TR1, IT1, IT)) -> balance55_10_out_gaaggggaag10(tree_33(L, V, R), XX0, XX1, NT, HR, TR, ._22(tuple_22(tree_33(LB, VB, RB), -2(A, D)), H), ._22(tuple_22(LB, -2(A, ._22(VB, X))), ._22(tuple_22(RB, -2(X, D)), T)), IH, IT)
if_balance_2_in_1_ga3(T, TB, balance55_10_out_gaaggggaag10(T, XX0, XX1, []_0, ._22(tuple_22(nil_0, -2(XX0, XX0)), XX1), []_0, ._22(tuple_22(TB, -2(I, []_0)), X), X, I, []_0)) -> balance_2_out_ga2(T, TB)

The argument filtering Pi contains the following mapping:
balance_2_in_ga2(x1, x2)  =  balance_2_in_ga1(x1)
[]_0  =  []_0
._22(x1, x2)  =  ._21(x1)
tuple_22(x1, x2)  =  tuple_21(x2)
nil_0  =  nil_0
-2(x1, x2)  =  -
tree_33(x1, x2, x3)  =  tree_33(x1, x2, x3)
if_balance_2_in_1_ga3(x1, x2, x3)  =  if_balance_2_in_1_ga1(x3)
balance55_10_in_gaaggggaag10(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  balance55_10_in_gaaggggaag6(x1, x4, x5, x6, x7, x10)
balance55_10_out_gaaggggaag10(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  balance55_10_out_gaaggggaag3(x3, x8, x9)
if_balance55_10_in_1_gaaggggaag19(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19)  =  if_balance55_10_in_1_gaaggggaag6(x3, x6, x7, x8, x18, x19)
balance55_10_in_gaagaaaaag10(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  balance55_10_in_gaagaaaaag3(x1, x4, x10)
balance55_10_out_gaagaaaaag10(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  balance55_10_out_gaagaaaaag2(x3, x9)
if_balance55_10_in_1_gaagaaaaag19(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19)  =  if_balance55_10_in_1_gaagaaaaag4(x3, x6, x18, x19)
if_balance55_10_in_2_gaagaaaaag24(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22, x23, x24)  =  if_balance55_10_in_2_gaagaaaaag3(x5, x17, x24)
if_balance55_10_in_2_gaaggggaag24(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22, x23, x24)  =  if_balance55_10_in_2_gaaggggaag3(x5, x17, x24)
balance55_10_in_gaagggaaag10(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  balance55_10_in_gaagggaaag5(x1, x4, x5, x6, x10)
balance55_10_out_gaagggaaag10(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  balance55_10_out_gaagggaaag4(x3, x7, x8, x9)
if_balance55_10_in_1_gaagggaaag19(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19)  =  if_balance55_10_in_1_gaagggaaag6(x3, x6, x7, x8, x18, x19)
if_balance55_10_in_2_gaagggaaag24(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22, x23, x24)  =  if_balance55_10_in_2_gaagggaaag3(x5, x17, x24)
balance_2_out_ga2(x1, x2)  =  balance_2_out_ga
IF_BALANCE55_10_IN_1_GAAGGGAAAG19(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19)  =  IF_BALANCE55_10_IN_1_GAAGGGAAAG6(x3, x6, x7, x8, x18, x19)
BALANCE55_10_IN_GAAGGGAAAG10(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  BALANCE55_10_IN_GAAGGGAAAG5(x1, x4, x5, x6, x10)

We have to consider all (P,R,Pi)-chains
For (infinitary) constructor rewriting we can delete all non-usable rules from R.

↳ PROLOG
  ↳ UnrequestedClauseRemoverProof
    ↳ PROLOG
      ↳ PrologToPiTRSProof
        ↳ PiTRS
          ↳ DependencyPairsProof
            ↳ PiDP
              ↳ DependencyGraphProof
                ↳ AND
                  ↳ PiDP
                  ↳ PiDP
                    ↳ UsableRulesProof
                      ↳ PiDP
                        ↳ PiDPToQDPProof

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

BALANCE55_10_IN_GAAGGGAAAG10(tree_33(L, V, R), XX0, XX1, NT, HR, TR, ._22(tuple_22(tree_33(LB, VB, RB), -2(A, D)), H), ._22(tuple_22(LB, -2(A, ._22(VB, X))), ._22(tuple_22(RB, -2(X, D)), T)), IH, IT) -> IF_BALANCE55_10_IN_1_GAAGGGAAAG19(L, V, R, XX0, XX1, NT, HR, TR, LB, VB, RB, A, D, H, X, T, IH, IT, balance55_10_in_gaagaaaaag10(L, XX0, XX1, ._22(tuple_22(nil_0, -2(XX2, XX2)), XX3), HR1, TR1, H, T, IH, ._22(V, IT1)))
IF_BALANCE55_10_IN_1_GAAGGGAAAG19(L, V, R, XX0, XX1, NT, HR, TR, LB, VB, RB, A, D, H, X, T, IH, IT, balance55_10_out_gaagaaaaag10(L, XX0, XX1, ._22(tuple_22(nil_0, -2(XX2, XX2)), XX3), HR1, TR1, H, T, IH, ._22(V, IT1))) -> BALANCE55_10_IN_GAAGGGAAAG10(R, XX2, XX3, NT, HR, TR, HR1, TR1, IT1, IT)

The TRS R consists of the following rules:

balance55_10_in_gaagaaaaag10(nil_0, C, T, T, A, B, A, B, X, X) -> balance55_10_out_gaagaaaaag10(nil_0, C, T, T, A, B, A, B, X, X)
balance55_10_in_gaagaaaaag10(tree_33(L, V, R), XX0, XX1, NT, HR, TR, ._22(tuple_22(tree_33(LB, VB, RB), -2(A, D)), H), ._22(tuple_22(LB, -2(A, ._22(VB, X))), ._22(tuple_22(RB, -2(X, D)), T)), IH, IT) -> if_balance55_10_in_1_gaagaaaaag19(L, V, R, XX0, XX1, NT, HR, TR, LB, VB, RB, A, D, H, X, T, IH, IT, balance55_10_in_gaagaaaaag10(L, XX0, XX1, ._22(tuple_22(nil_0, -2(XX2, XX2)), XX3), HR1, TR1, H, T, IH, ._22(V, IT1)))
if_balance55_10_in_1_gaagaaaaag19(L, V, R, XX0, XX1, NT, HR, TR, LB, VB, RB, A, D, H, X, T, IH, IT, balance55_10_out_gaagaaaaag10(L, XX0, XX1, ._22(tuple_22(nil_0, -2(XX2, XX2)), XX3), HR1, TR1, H, T, IH, ._22(V, IT1))) -> if_balance55_10_in_2_gaagaaaaag24(L, V, R, XX0, XX1, NT, HR, TR, LB, VB, RB, A, D, H, X, T, IH, IT, XX2, XX3, HR1, TR1, IT1, balance55_10_in_gaagaaaaag10(R, XX2, XX3, NT, HR, TR, HR1, TR1, IT1, IT))
if_balance55_10_in_2_gaagaaaaag24(L, V, R, XX0, XX1, NT, HR, TR, LB, VB, RB, A, D, H, X, T, IH, IT, XX2, XX3, HR1, TR1, IT1, balance55_10_out_gaagaaaaag10(R, XX2, XX3, NT, HR, TR, HR1, TR1, IT1, IT)) -> balance55_10_out_gaagaaaaag10(tree_33(L, V, R), XX0, XX1, NT, HR, TR, ._22(tuple_22(tree_33(LB, VB, RB), -2(A, D)), H), ._22(tuple_22(LB, -2(A, ._22(VB, X))), ._22(tuple_22(RB, -2(X, D)), T)), IH, IT)

The argument filtering Pi contains the following mapping:
._22(x1, x2)  =  ._21(x1)
tuple_22(x1, x2)  =  tuple_21(x2)
nil_0  =  nil_0
-2(x1, x2)  =  -
tree_33(x1, x2, x3)  =  tree_33(x1, x2, x3)
balance55_10_in_gaagaaaaag10(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  balance55_10_in_gaagaaaaag3(x1, x4, x10)
balance55_10_out_gaagaaaaag10(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  balance55_10_out_gaagaaaaag2(x3, x9)
if_balance55_10_in_1_gaagaaaaag19(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19)  =  if_balance55_10_in_1_gaagaaaaag4(x3, x6, x18, x19)
if_balance55_10_in_2_gaagaaaaag24(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22, x23, x24)  =  if_balance55_10_in_2_gaagaaaaag3(x5, x17, x24)
IF_BALANCE55_10_IN_1_GAAGGGAAAG19(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19)  =  IF_BALANCE55_10_IN_1_GAAGGGAAAG6(x3, x6, x7, x8, x18, x19)
BALANCE55_10_IN_GAAGGGAAAG10(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  BALANCE55_10_IN_GAAGGGAAAG5(x1, x4, x5, x6, x10)

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
  ↳ UnrequestedClauseRemoverProof
    ↳ PROLOG
      ↳ PrologToPiTRSProof
        ↳ PiTRS
          ↳ DependencyPairsProof
            ↳ PiDP
              ↳ DependencyGraphProof
                ↳ AND
                  ↳ PiDP
                  ↳ PiDP
                    ↳ UsableRulesProof
                      ↳ PiDP
                        ↳ PiDPToQDPProof
                          ↳ QDP
                            ↳ QDPSizeChangeProof

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

BALANCE55_10_IN_GAAGGGAAAG5(tree_33(L, V, R), NT, HR, TR, IT) -> IF_BALANCE55_10_IN_1_GAAGGGAAAG6(R, NT, HR, TR, IT, balance55_10_in_gaagaaaaag3(L, ._21(tuple_21(-)), ._21(V)))
IF_BALANCE55_10_IN_1_GAAGGGAAAG6(R, NT, HR, TR, IT, balance55_10_out_gaagaaaaag2(XX1, IH)) -> BALANCE55_10_IN_GAAGGGAAAG5(R, NT, HR, TR, IT)

The TRS R consists of the following rules:

balance55_10_in_gaagaaaaag3(nil_0, T, X) -> balance55_10_out_gaagaaaaag2(T, X)
balance55_10_in_gaagaaaaag3(tree_33(L, V, R), NT, IT) -> if_balance55_10_in_1_gaagaaaaag4(R, NT, IT, balance55_10_in_gaagaaaaag3(L, ._21(tuple_21(-)), ._21(V)))
if_balance55_10_in_1_gaagaaaaag4(R, NT, IT, balance55_10_out_gaagaaaaag2(XX1, IH)) -> if_balance55_10_in_2_gaagaaaaag3(XX1, IH, balance55_10_in_gaagaaaaag3(R, NT, IT))
if_balance55_10_in_2_gaagaaaaag3(XX1, IH, balance55_10_out_gaagaaaaag2(XX3, IT1)) -> balance55_10_out_gaagaaaaag2(XX1, IH)

The set Q consists of the following terms:

balance55_10_in_gaagaaaaag3(x0, x1, x2)
if_balance55_10_in_1_gaagaaaaag4(x0, x1, x2, x3)
if_balance55_10_in_2_gaagaaaaag3(x0, x1, x2)

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

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