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



↳ PROLOG
  ↳ PrologToPiTRSProof

balance2(T, TB) :- balance5(T, I - {}0, .2(tuple2(TB, I - {}0), X) - X, Rest - {}0, Rest - {}0).
balance5(nil0, X - X, A - B, A - B, .2(tuple2(nil0, C - C), T) - T).
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, NH - NT) :- balance5(L, IH - .2(V, IT1), H - T, HR1 - TR1, NH - NT1), balance5(R, IT1 - IT, HR1 - TR1, HR - TR, NT1 - NT).


With regard to the inferred argument filtering the predicates were used in the following modes:
balance2: (b,f)
balance5: (b,b,b,b,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, balance_5_in_ggggg5(T, -2(I, []_0), -2(._22(tuple_22(TB, -2(I, []_0)), X), X), -2(Rest, []_0), -2(Rest, []_0)))
balance_5_in_ggggg5(nil_0, -2(X, X), -2(A, B), -2(A, B), -2(._22(tuple_22(nil_0, -2(C, C)), T), T)) -> balance_5_out_ggggg5(nil_0, -2(X, X), -2(A, B), -2(A, B), -2(._22(tuple_22(nil_0, -2(C, C)), T), T))
balance_5_in_ggggg5(tree_33(L, V, R), -2(IH, IT), -2(._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))), -2(HR, TR), -2(NH, NT)) -> if_balance_5_in_1_ggggg18(L, V, R, IH, IT, LB, VB, RB, A, D, H, X, T, HR, TR, NH, NT, balance_5_in_ggggg5(L, -2(IH, ._22(V, IT1)), -2(H, T), -2(HR1, TR1), -2(NH, NT1)))
if_balance_5_in_1_ggggg18(L, V, R, IH, IT, LB, VB, RB, A, D, H, X, T, HR, TR, NH, NT, balance_5_out_ggggg5(L, -2(IH, ._22(V, IT1)), -2(H, T), -2(HR1, TR1), -2(NH, NT1))) -> if_balance_5_in_2_ggggg22(L, V, R, IH, IT, LB, VB, RB, A, D, H, X, T, HR, TR, NH, NT, IT1, HR1, TR1, NT1, balance_5_in_ggggg5(R, -2(IT1, IT), -2(HR1, TR1), -2(HR, TR), -2(NT1, NT)))
if_balance_5_in_2_ggggg22(L, V, R, IH, IT, LB, VB, RB, A, D, H, X, T, HR, TR, NH, NT, IT1, HR1, TR1, NT1, balance_5_out_ggggg5(R, -2(IT1, IT), -2(HR1, TR1), -2(HR, TR), -2(NT1, NT))) -> balance_5_out_ggggg5(tree_33(L, V, R), -2(IH, IT), -2(._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))), -2(HR, TR), -2(NH, NT))
if_balance_2_in_1_ga3(T, TB, balance_5_out_ggggg5(T, -2(I, []_0), -2(._22(tuple_22(TB, -2(I, []_0)), X), X), -2(Rest, []_0), -2(Rest, []_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)
-2(x1, x2)  =  -
[]_0  =  []_0
._22(x1, x2)  =  ._22(x1, x2)
tuple_22(x1, x2)  =  tuple_22(x1, x2)
nil_0  =  nil_0
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)
balance_5_in_ggggg5(x1, x2, x3, x4, x5)  =  balance_5_in_ggggg5(x1, x2, x3, x4, x5)
balance_5_out_ggggg5(x1, x2, x3, x4, x5)  =  balance_5_out_ggggg
if_balance_5_in_1_ggggg18(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18)  =  if_balance_5_in_1_ggggg2(x3, x18)
if_balance_5_in_2_ggggg22(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22)  =  if_balance_5_in_2_ggggg1(x22)
balance_2_out_ga2(x1, x2)  =  balance_2_out_ga

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of PROLOG



↳ PROLOG
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof

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

balance_2_in_ga2(T, TB) -> if_balance_2_in_1_ga3(T, TB, balance_5_in_ggggg5(T, -2(I, []_0), -2(._22(tuple_22(TB, -2(I, []_0)), X), X), -2(Rest, []_0), -2(Rest, []_0)))
balance_5_in_ggggg5(nil_0, -2(X, X), -2(A, B), -2(A, B), -2(._22(tuple_22(nil_0, -2(C, C)), T), T)) -> balance_5_out_ggggg5(nil_0, -2(X, X), -2(A, B), -2(A, B), -2(._22(tuple_22(nil_0, -2(C, C)), T), T))
balance_5_in_ggggg5(tree_33(L, V, R), -2(IH, IT), -2(._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))), -2(HR, TR), -2(NH, NT)) -> if_balance_5_in_1_ggggg18(L, V, R, IH, IT, LB, VB, RB, A, D, H, X, T, HR, TR, NH, NT, balance_5_in_ggggg5(L, -2(IH, ._22(V, IT1)), -2(H, T), -2(HR1, TR1), -2(NH, NT1)))
if_balance_5_in_1_ggggg18(L, V, R, IH, IT, LB, VB, RB, A, D, H, X, T, HR, TR, NH, NT, balance_5_out_ggggg5(L, -2(IH, ._22(V, IT1)), -2(H, T), -2(HR1, TR1), -2(NH, NT1))) -> if_balance_5_in_2_ggggg22(L, V, R, IH, IT, LB, VB, RB, A, D, H, X, T, HR, TR, NH, NT, IT1, HR1, TR1, NT1, balance_5_in_ggggg5(R, -2(IT1, IT), -2(HR1, TR1), -2(HR, TR), -2(NT1, NT)))
if_balance_5_in_2_ggggg22(L, V, R, IH, IT, LB, VB, RB, A, D, H, X, T, HR, TR, NH, NT, IT1, HR1, TR1, NT1, balance_5_out_ggggg5(R, -2(IT1, IT), -2(HR1, TR1), -2(HR, TR), -2(NT1, NT))) -> balance_5_out_ggggg5(tree_33(L, V, R), -2(IH, IT), -2(._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))), -2(HR, TR), -2(NH, NT))
if_balance_2_in_1_ga3(T, TB, balance_5_out_ggggg5(T, -2(I, []_0), -2(._22(tuple_22(TB, -2(I, []_0)), X), X), -2(Rest, []_0), -2(Rest, []_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)
-2(x1, x2)  =  -
[]_0  =  []_0
._22(x1, x2)  =  ._22(x1, x2)
tuple_22(x1, x2)  =  tuple_22(x1, x2)
nil_0  =  nil_0
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)
balance_5_in_ggggg5(x1, x2, x3, x4, x5)  =  balance_5_in_ggggg5(x1, x2, x3, x4, x5)
balance_5_out_ggggg5(x1, x2, x3, x4, x5)  =  balance_5_out_ggggg
if_balance_5_in_1_ggggg18(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18)  =  if_balance_5_in_1_ggggg2(x3, x18)
if_balance_5_in_2_ggggg22(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22)  =  if_balance_5_in_2_ggggg1(x22)
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, balance_5_in_ggggg5(T, -2(I, []_0), -2(._22(tuple_22(TB, -2(I, []_0)), X), X), -2(Rest, []_0), -2(Rest, []_0)))
BALANCE_2_IN_GA2(T, TB) -> BALANCE_5_IN_GGGGG5(T, -2(I, []_0), -2(._22(tuple_22(TB, -2(I, []_0)), X), X), -2(Rest, []_0), -2(Rest, []_0))
BALANCE_5_IN_GGGGG5(tree_33(L, V, R), -2(IH, IT), -2(._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))), -2(HR, TR), -2(NH, NT)) -> IF_BALANCE_5_IN_1_GGGGG18(L, V, R, IH, IT, LB, VB, RB, A, D, H, X, T, HR, TR, NH, NT, balance_5_in_ggggg5(L, -2(IH, ._22(V, IT1)), -2(H, T), -2(HR1, TR1), -2(NH, NT1)))
BALANCE_5_IN_GGGGG5(tree_33(L, V, R), -2(IH, IT), -2(._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))), -2(HR, TR), -2(NH, NT)) -> BALANCE_5_IN_GGGGG5(L, -2(IH, ._22(V, IT1)), -2(H, T), -2(HR1, TR1), -2(NH, NT1))
IF_BALANCE_5_IN_1_GGGGG18(L, V, R, IH, IT, LB, VB, RB, A, D, H, X, T, HR, TR, NH, NT, balance_5_out_ggggg5(L, -2(IH, ._22(V, IT1)), -2(H, T), -2(HR1, TR1), -2(NH, NT1))) -> IF_BALANCE_5_IN_2_GGGGG22(L, V, R, IH, IT, LB, VB, RB, A, D, H, X, T, HR, TR, NH, NT, IT1, HR1, TR1, NT1, balance_5_in_ggggg5(R, -2(IT1, IT), -2(HR1, TR1), -2(HR, TR), -2(NT1, NT)))
IF_BALANCE_5_IN_1_GGGGG18(L, V, R, IH, IT, LB, VB, RB, A, D, H, X, T, HR, TR, NH, NT, balance_5_out_ggggg5(L, -2(IH, ._22(V, IT1)), -2(H, T), -2(HR1, TR1), -2(NH, NT1))) -> BALANCE_5_IN_GGGGG5(R, -2(IT1, IT), -2(HR1, TR1), -2(HR, TR), -2(NT1, NT))

The TRS R consists of the following rules:

balance_2_in_ga2(T, TB) -> if_balance_2_in_1_ga3(T, TB, balance_5_in_ggggg5(T, -2(I, []_0), -2(._22(tuple_22(TB, -2(I, []_0)), X), X), -2(Rest, []_0), -2(Rest, []_0)))
balance_5_in_ggggg5(nil_0, -2(X, X), -2(A, B), -2(A, B), -2(._22(tuple_22(nil_0, -2(C, C)), T), T)) -> balance_5_out_ggggg5(nil_0, -2(X, X), -2(A, B), -2(A, B), -2(._22(tuple_22(nil_0, -2(C, C)), T), T))
balance_5_in_ggggg5(tree_33(L, V, R), -2(IH, IT), -2(._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))), -2(HR, TR), -2(NH, NT)) -> if_balance_5_in_1_ggggg18(L, V, R, IH, IT, LB, VB, RB, A, D, H, X, T, HR, TR, NH, NT, balance_5_in_ggggg5(L, -2(IH, ._22(V, IT1)), -2(H, T), -2(HR1, TR1), -2(NH, NT1)))
if_balance_5_in_1_ggggg18(L, V, R, IH, IT, LB, VB, RB, A, D, H, X, T, HR, TR, NH, NT, balance_5_out_ggggg5(L, -2(IH, ._22(V, IT1)), -2(H, T), -2(HR1, TR1), -2(NH, NT1))) -> if_balance_5_in_2_ggggg22(L, V, R, IH, IT, LB, VB, RB, A, D, H, X, T, HR, TR, NH, NT, IT1, HR1, TR1, NT1, balance_5_in_ggggg5(R, -2(IT1, IT), -2(HR1, TR1), -2(HR, TR), -2(NT1, NT)))
if_balance_5_in_2_ggggg22(L, V, R, IH, IT, LB, VB, RB, A, D, H, X, T, HR, TR, NH, NT, IT1, HR1, TR1, NT1, balance_5_out_ggggg5(R, -2(IT1, IT), -2(HR1, TR1), -2(HR, TR), -2(NT1, NT))) -> balance_5_out_ggggg5(tree_33(L, V, R), -2(IH, IT), -2(._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))), -2(HR, TR), -2(NH, NT))
if_balance_2_in_1_ga3(T, TB, balance_5_out_ggggg5(T, -2(I, []_0), -2(._22(tuple_22(TB, -2(I, []_0)), X), X), -2(Rest, []_0), -2(Rest, []_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)
-2(x1, x2)  =  -
[]_0  =  []_0
._22(x1, x2)  =  ._22(x1, x2)
tuple_22(x1, x2)  =  tuple_22(x1, x2)
nil_0  =  nil_0
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)
balance_5_in_ggggg5(x1, x2, x3, x4, x5)  =  balance_5_in_ggggg5(x1, x2, x3, x4, x5)
balance_5_out_ggggg5(x1, x2, x3, x4, x5)  =  balance_5_out_ggggg
if_balance_5_in_1_ggggg18(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18)  =  if_balance_5_in_1_ggggg2(x3, x18)
if_balance_5_in_2_ggggg22(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22)  =  if_balance_5_in_2_ggggg1(x22)
balance_2_out_ga2(x1, x2)  =  balance_2_out_ga
IF_BALANCE_2_IN_1_GA3(x1, x2, x3)  =  IF_BALANCE_2_IN_1_GA1(x3)
IF_BALANCE_5_IN_1_GGGGG18(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18)  =  IF_BALANCE_5_IN_1_GGGGG2(x3, x18)
IF_BALANCE_5_IN_2_GGGGG22(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22)  =  IF_BALANCE_5_IN_2_GGGGG1(x22)
BALANCE_5_IN_GGGGG5(x1, x2, x3, x4, x5)  =  BALANCE_5_IN_GGGGG5(x1, x2, x3, x4, x5)
BALANCE_2_IN_GA2(x1, x2)  =  BALANCE_2_IN_GA1(x1)

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

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

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

BALANCE_2_IN_GA2(T, TB) -> IF_BALANCE_2_IN_1_GA3(T, TB, balance_5_in_ggggg5(T, -2(I, []_0), -2(._22(tuple_22(TB, -2(I, []_0)), X), X), -2(Rest, []_0), -2(Rest, []_0)))
BALANCE_2_IN_GA2(T, TB) -> BALANCE_5_IN_GGGGG5(T, -2(I, []_0), -2(._22(tuple_22(TB, -2(I, []_0)), X), X), -2(Rest, []_0), -2(Rest, []_0))
BALANCE_5_IN_GGGGG5(tree_33(L, V, R), -2(IH, IT), -2(._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))), -2(HR, TR), -2(NH, NT)) -> IF_BALANCE_5_IN_1_GGGGG18(L, V, R, IH, IT, LB, VB, RB, A, D, H, X, T, HR, TR, NH, NT, balance_5_in_ggggg5(L, -2(IH, ._22(V, IT1)), -2(H, T), -2(HR1, TR1), -2(NH, NT1)))
BALANCE_5_IN_GGGGG5(tree_33(L, V, R), -2(IH, IT), -2(._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))), -2(HR, TR), -2(NH, NT)) -> BALANCE_5_IN_GGGGG5(L, -2(IH, ._22(V, IT1)), -2(H, T), -2(HR1, TR1), -2(NH, NT1))
IF_BALANCE_5_IN_1_GGGGG18(L, V, R, IH, IT, LB, VB, RB, A, D, H, X, T, HR, TR, NH, NT, balance_5_out_ggggg5(L, -2(IH, ._22(V, IT1)), -2(H, T), -2(HR1, TR1), -2(NH, NT1))) -> IF_BALANCE_5_IN_2_GGGGG22(L, V, R, IH, IT, LB, VB, RB, A, D, H, X, T, HR, TR, NH, NT, IT1, HR1, TR1, NT1, balance_5_in_ggggg5(R, -2(IT1, IT), -2(HR1, TR1), -2(HR, TR), -2(NT1, NT)))
IF_BALANCE_5_IN_1_GGGGG18(L, V, R, IH, IT, LB, VB, RB, A, D, H, X, T, HR, TR, NH, NT, balance_5_out_ggggg5(L, -2(IH, ._22(V, IT1)), -2(H, T), -2(HR1, TR1), -2(NH, NT1))) -> BALANCE_5_IN_GGGGG5(R, -2(IT1, IT), -2(HR1, TR1), -2(HR, TR), -2(NT1, NT))

The TRS R consists of the following rules:

balance_2_in_ga2(T, TB) -> if_balance_2_in_1_ga3(T, TB, balance_5_in_ggggg5(T, -2(I, []_0), -2(._22(tuple_22(TB, -2(I, []_0)), X), X), -2(Rest, []_0), -2(Rest, []_0)))
balance_5_in_ggggg5(nil_0, -2(X, X), -2(A, B), -2(A, B), -2(._22(tuple_22(nil_0, -2(C, C)), T), T)) -> balance_5_out_ggggg5(nil_0, -2(X, X), -2(A, B), -2(A, B), -2(._22(tuple_22(nil_0, -2(C, C)), T), T))
balance_5_in_ggggg5(tree_33(L, V, R), -2(IH, IT), -2(._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))), -2(HR, TR), -2(NH, NT)) -> if_balance_5_in_1_ggggg18(L, V, R, IH, IT, LB, VB, RB, A, D, H, X, T, HR, TR, NH, NT, balance_5_in_ggggg5(L, -2(IH, ._22(V, IT1)), -2(H, T), -2(HR1, TR1), -2(NH, NT1)))
if_balance_5_in_1_ggggg18(L, V, R, IH, IT, LB, VB, RB, A, D, H, X, T, HR, TR, NH, NT, balance_5_out_ggggg5(L, -2(IH, ._22(V, IT1)), -2(H, T), -2(HR1, TR1), -2(NH, NT1))) -> if_balance_5_in_2_ggggg22(L, V, R, IH, IT, LB, VB, RB, A, D, H, X, T, HR, TR, NH, NT, IT1, HR1, TR1, NT1, balance_5_in_ggggg5(R, -2(IT1, IT), -2(HR1, TR1), -2(HR, TR), -2(NT1, NT)))
if_balance_5_in_2_ggggg22(L, V, R, IH, IT, LB, VB, RB, A, D, H, X, T, HR, TR, NH, NT, IT1, HR1, TR1, NT1, balance_5_out_ggggg5(R, -2(IT1, IT), -2(HR1, TR1), -2(HR, TR), -2(NT1, NT))) -> balance_5_out_ggggg5(tree_33(L, V, R), -2(IH, IT), -2(._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))), -2(HR, TR), -2(NH, NT))
if_balance_2_in_1_ga3(T, TB, balance_5_out_ggggg5(T, -2(I, []_0), -2(._22(tuple_22(TB, -2(I, []_0)), X), X), -2(Rest, []_0), -2(Rest, []_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)
-2(x1, x2)  =  -
[]_0  =  []_0
._22(x1, x2)  =  ._22(x1, x2)
tuple_22(x1, x2)  =  tuple_22(x1, x2)
nil_0  =  nil_0
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)
balance_5_in_ggggg5(x1, x2, x3, x4, x5)  =  balance_5_in_ggggg5(x1, x2, x3, x4, x5)
balance_5_out_ggggg5(x1, x2, x3, x4, x5)  =  balance_5_out_ggggg
if_balance_5_in_1_ggggg18(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18)  =  if_balance_5_in_1_ggggg2(x3, x18)
if_balance_5_in_2_ggggg22(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22)  =  if_balance_5_in_2_ggggg1(x22)
balance_2_out_ga2(x1, x2)  =  balance_2_out_ga
IF_BALANCE_2_IN_1_GA3(x1, x2, x3)  =  IF_BALANCE_2_IN_1_GA1(x3)
IF_BALANCE_5_IN_1_GGGGG18(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18)  =  IF_BALANCE_5_IN_1_GGGGG2(x3, x18)
IF_BALANCE_5_IN_2_GGGGG22(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22)  =  IF_BALANCE_5_IN_2_GGGGG1(x22)
BALANCE_5_IN_GGGGG5(x1, x2, x3, x4, x5)  =  BALANCE_5_IN_GGGGG5(x1, x2, x3, x4, x5)
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 1 SCC with 3 less nodes.

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

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

BALANCE_5_IN_GGGGG5(tree_33(L, V, R), -2(IH, IT), -2(._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))), -2(HR, TR), -2(NH, NT)) -> BALANCE_5_IN_GGGGG5(L, -2(IH, ._22(V, IT1)), -2(H, T), -2(HR1, TR1), -2(NH, NT1))
IF_BALANCE_5_IN_1_GGGGG18(L, V, R, IH, IT, LB, VB, RB, A, D, H, X, T, HR, TR, NH, NT, balance_5_out_ggggg5(L, -2(IH, ._22(V, IT1)), -2(H, T), -2(HR1, TR1), -2(NH, NT1))) -> BALANCE_5_IN_GGGGG5(R, -2(IT1, IT), -2(HR1, TR1), -2(HR, TR), -2(NT1, NT))
BALANCE_5_IN_GGGGG5(tree_33(L, V, R), -2(IH, IT), -2(._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))), -2(HR, TR), -2(NH, NT)) -> IF_BALANCE_5_IN_1_GGGGG18(L, V, R, IH, IT, LB, VB, RB, A, D, H, X, T, HR, TR, NH, NT, balance_5_in_ggggg5(L, -2(IH, ._22(V, IT1)), -2(H, T), -2(HR1, TR1), -2(NH, NT1)))

The TRS R consists of the following rules:

balance_2_in_ga2(T, TB) -> if_balance_2_in_1_ga3(T, TB, balance_5_in_ggggg5(T, -2(I, []_0), -2(._22(tuple_22(TB, -2(I, []_0)), X), X), -2(Rest, []_0), -2(Rest, []_0)))
balance_5_in_ggggg5(nil_0, -2(X, X), -2(A, B), -2(A, B), -2(._22(tuple_22(nil_0, -2(C, C)), T), T)) -> balance_5_out_ggggg5(nil_0, -2(X, X), -2(A, B), -2(A, B), -2(._22(tuple_22(nil_0, -2(C, C)), T), T))
balance_5_in_ggggg5(tree_33(L, V, R), -2(IH, IT), -2(._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))), -2(HR, TR), -2(NH, NT)) -> if_balance_5_in_1_ggggg18(L, V, R, IH, IT, LB, VB, RB, A, D, H, X, T, HR, TR, NH, NT, balance_5_in_ggggg5(L, -2(IH, ._22(V, IT1)), -2(H, T), -2(HR1, TR1), -2(NH, NT1)))
if_balance_5_in_1_ggggg18(L, V, R, IH, IT, LB, VB, RB, A, D, H, X, T, HR, TR, NH, NT, balance_5_out_ggggg5(L, -2(IH, ._22(V, IT1)), -2(H, T), -2(HR1, TR1), -2(NH, NT1))) -> if_balance_5_in_2_ggggg22(L, V, R, IH, IT, LB, VB, RB, A, D, H, X, T, HR, TR, NH, NT, IT1, HR1, TR1, NT1, balance_5_in_ggggg5(R, -2(IT1, IT), -2(HR1, TR1), -2(HR, TR), -2(NT1, NT)))
if_balance_5_in_2_ggggg22(L, V, R, IH, IT, LB, VB, RB, A, D, H, X, T, HR, TR, NH, NT, IT1, HR1, TR1, NT1, balance_5_out_ggggg5(R, -2(IT1, IT), -2(HR1, TR1), -2(HR, TR), -2(NT1, NT))) -> balance_5_out_ggggg5(tree_33(L, V, R), -2(IH, IT), -2(._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))), -2(HR, TR), -2(NH, NT))
if_balance_2_in_1_ga3(T, TB, balance_5_out_ggggg5(T, -2(I, []_0), -2(._22(tuple_22(TB, -2(I, []_0)), X), X), -2(Rest, []_0), -2(Rest, []_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)
-2(x1, x2)  =  -
[]_0  =  []_0
._22(x1, x2)  =  ._22(x1, x2)
tuple_22(x1, x2)  =  tuple_22(x1, x2)
nil_0  =  nil_0
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)
balance_5_in_ggggg5(x1, x2, x3, x4, x5)  =  balance_5_in_ggggg5(x1, x2, x3, x4, x5)
balance_5_out_ggggg5(x1, x2, x3, x4, x5)  =  balance_5_out_ggggg
if_balance_5_in_1_ggggg18(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18)  =  if_balance_5_in_1_ggggg2(x3, x18)
if_balance_5_in_2_ggggg22(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22)  =  if_balance_5_in_2_ggggg1(x22)
balance_2_out_ga2(x1, x2)  =  balance_2_out_ga
IF_BALANCE_5_IN_1_GGGGG18(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18)  =  IF_BALANCE_5_IN_1_GGGGG2(x3, x18)
BALANCE_5_IN_GGGGG5(x1, x2, x3, x4, x5)  =  BALANCE_5_IN_GGGGG5(x1, x2, x3, x4, x5)

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

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

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

BALANCE_5_IN_GGGGG5(tree_33(L, V, R), -2(IH, IT), -2(._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))), -2(HR, TR), -2(NH, NT)) -> BALANCE_5_IN_GGGGG5(L, -2(IH, ._22(V, IT1)), -2(H, T), -2(HR1, TR1), -2(NH, NT1))
IF_BALANCE_5_IN_1_GGGGG18(L, V, R, IH, IT, LB, VB, RB, A, D, H, X, T, HR, TR, NH, NT, balance_5_out_ggggg5(L, -2(IH, ._22(V, IT1)), -2(H, T), -2(HR1, TR1), -2(NH, NT1))) -> BALANCE_5_IN_GGGGG5(R, -2(IT1, IT), -2(HR1, TR1), -2(HR, TR), -2(NT1, NT))
BALANCE_5_IN_GGGGG5(tree_33(L, V, R), -2(IH, IT), -2(._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))), -2(HR, TR), -2(NH, NT)) -> IF_BALANCE_5_IN_1_GGGGG18(L, V, R, IH, IT, LB, VB, RB, A, D, H, X, T, HR, TR, NH, NT, balance_5_in_ggggg5(L, -2(IH, ._22(V, IT1)), -2(H, T), -2(HR1, TR1), -2(NH, NT1)))

The TRS R consists of the following rules:

balance_5_in_ggggg5(nil_0, -2(X, X), -2(A, B), -2(A, B), -2(._22(tuple_22(nil_0, -2(C, C)), T), T)) -> balance_5_out_ggggg5(nil_0, -2(X, X), -2(A, B), -2(A, B), -2(._22(tuple_22(nil_0, -2(C, C)), T), T))
balance_5_in_ggggg5(tree_33(L, V, R), -2(IH, IT), -2(._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))), -2(HR, TR), -2(NH, NT)) -> if_balance_5_in_1_ggggg18(L, V, R, IH, IT, LB, VB, RB, A, D, H, X, T, HR, TR, NH, NT, balance_5_in_ggggg5(L, -2(IH, ._22(V, IT1)), -2(H, T), -2(HR1, TR1), -2(NH, NT1)))
if_balance_5_in_1_ggggg18(L, V, R, IH, IT, LB, VB, RB, A, D, H, X, T, HR, TR, NH, NT, balance_5_out_ggggg5(L, -2(IH, ._22(V, IT1)), -2(H, T), -2(HR1, TR1), -2(NH, NT1))) -> if_balance_5_in_2_ggggg22(L, V, R, IH, IT, LB, VB, RB, A, D, H, X, T, HR, TR, NH, NT, IT1, HR1, TR1, NT1, balance_5_in_ggggg5(R, -2(IT1, IT), -2(HR1, TR1), -2(HR, TR), -2(NT1, NT)))
if_balance_5_in_2_ggggg22(L, V, R, IH, IT, LB, VB, RB, A, D, H, X, T, HR, TR, NH, NT, IT1, HR1, TR1, NT1, balance_5_out_ggggg5(R, -2(IT1, IT), -2(HR1, TR1), -2(HR, TR), -2(NT1, NT))) -> balance_5_out_ggggg5(tree_33(L, V, R), -2(IH, IT), -2(._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))), -2(HR, TR), -2(NH, NT))

The argument filtering Pi contains the following mapping:
-2(x1, x2)  =  -
._22(x1, x2)  =  ._22(x1, x2)
tuple_22(x1, x2)  =  tuple_22(x1, x2)
nil_0  =  nil_0
tree_33(x1, x2, x3)  =  tree_33(x1, x2, x3)
balance_5_in_ggggg5(x1, x2, x3, x4, x5)  =  balance_5_in_ggggg5(x1, x2, x3, x4, x5)
balance_5_out_ggggg5(x1, x2, x3, x4, x5)  =  balance_5_out_ggggg
if_balance_5_in_1_ggggg18(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18)  =  if_balance_5_in_1_ggggg2(x3, x18)
if_balance_5_in_2_ggggg22(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22)  =  if_balance_5_in_2_ggggg1(x22)
IF_BALANCE_5_IN_1_GGGGG18(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18)  =  IF_BALANCE_5_IN_1_GGGGG2(x3, x18)
BALANCE_5_IN_GGGGG5(x1, x2, x3, x4, x5)  =  BALANCE_5_IN_GGGGG5(x1, x2, x3, x4, x5)

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
            ↳ PiDP
              ↳ UsableRulesProof
                ↳ PiDP
                  ↳ PiDPToQDPProof
                    ↳ QDP
                      ↳ QDPSizeChangeProof

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

BALANCE_5_IN_GGGGG5(tree_33(L, V, R), -, -, -, -) -> BALANCE_5_IN_GGGGG5(L, -, -, -, -)
IF_BALANCE_5_IN_1_GGGGG2(R, balance_5_out_ggggg) -> BALANCE_5_IN_GGGGG5(R, -, -, -, -)
BALANCE_5_IN_GGGGG5(tree_33(L, V, R), -, -, -, -) -> IF_BALANCE_5_IN_1_GGGGG2(R, balance_5_in_ggggg5(L, -, -, -, -))

The TRS R consists of the following rules:

balance_5_in_ggggg5(nil_0, -, -, -, -) -> balance_5_out_ggggg
balance_5_in_ggggg5(tree_33(L, V, R), -, -, -, -) -> if_balance_5_in_1_ggggg2(R, balance_5_in_ggggg5(L, -, -, -, -))
if_balance_5_in_1_ggggg2(R, balance_5_out_ggggg) -> if_balance_5_in_2_ggggg1(balance_5_in_ggggg5(R, -, -, -, -))
if_balance_5_in_2_ggggg1(balance_5_out_ggggg) -> balance_5_out_ggggg

The set Q consists of the following terms:

balance_5_in_ggggg5(x0, x1, x2, x3, x4)
if_balance_5_in_1_ggggg2(x0, x1)
if_balance_5_in_2_ggggg1(x0)

We have to consider all (P,Q,R)-chains.
The head symbols of this DP problem are {BALANCE_5_IN_GGGGG5, IF_BALANCE_5_IN_1_GGGGG2}.
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: