Left Termination of the query pattern balance_in_2(g, a) w.r.t. the given Prolog program could successfully be proven:

0 Prolog
↳1 PrologToDTProblemTransformerProof (⇐)
↳2 TRIPLES
↳3 TriplesToPiDPProof (⇐)
↳4 PiDP
↳5 DependencyGraphProof (⇔)
↳6 AND
    ↳7 PiDP
        ↳8 UsableRulesProof (⇔)
        ↳9 PiDP
        ↳10 PiDPToQDPProof (⇐)
        ↳11 QDP
        ↳12 QDPSizeChangeProof (⇔)
        ↳13 YES
    ↳14 PiDP
        ↳15 UsableRulesProof (⇔)
        ↳16 PiDP
        ↳17 PiDPToQDPProof (⇐)
        ↳18 QDP
        ↳19 QDPSizeChangeProof (⇔)
        ↳20 YES

(0) Obligation:

Clauses:

balance(T, TB) :- balance55(T, XX0, XX1, [], .(','(nil, -(XX0, XX0)), XX1), [], .(','(TB, -(I, [])), X), X, I, []).
balance55(nil, C, T, T, A, B, A, B, X, X).
balance55(tree(L, V, R), XX0, XX1, NT, HR, TR, .(','(tree(LB, VB, RB), -(A, D)), H), .(','(LB, -(A, .(VB, X))), .(','(RB, -(X, D)), T)), IH, IT) :- ','(balance55(L, XX0, XX1, .(','(nil, -(XX2, XX2)), XX3), HR1, TR1, H, T, IH, .(V, IT1)), balance55(R, XX2, XX3, NT, HR, TR, HR1, TR1, IT1, IT)).
balance5(nil, C, T, T, A, B, A, B, X, X) :- balance55(nil, C, T, T, A, B, A, B, X, X).
balance5(tree(L, V, R), XX0, XX1, NT, HR, TR, .(','(tree(LB, VB, RB), -(A, D)), H), .(','(LB, -(A, .(VB, X))), .(','(RB, -(X, D)), T)), IH, IT) :- balance55(tree(L, V, R), XX0, XX1, NT, HR, TR, .(','(tree(LB, VB, RB), -(A, D)), H), .(','(LB, -(A, .(VB, X))), .(','(RB, -(X, D)), T)), IH, IT).
balance(nil, -(X, X), -(A, B), -(A, B), -(.(','(nil, -(C, C)), T), T)) :- balance5(nil, C, T, T, A, B, A, B, X, X).
balance(tree(L, V, R), -(IH, IT), -(.(','(tree(LB, VB, RB), -(A, D)), H), .(','(LB, -(A, .(VB, X))), .(','(RB, -(X, D)), T))), -(HR, TR), -(.(','(nil, -(XX0, XX0)), XX1), NT)) :- balance5(tree(L, V, R), XX0, XX1, NT, HR, TR, .(','(tree(LB, VB, RB), -(A, D)), H), .(','(LB, -(A, .(VB, X))), .(','(RB, -(X, D)), T)), IH, IT).

Queries:

balance(g,a).

(1) PrologToDTProblemTransformerProof (SOUND transformation)

Built DT problem from termination graph.

(2) Obligation:

Triples:

balance5523(tree(T306, T307, T308), T321, T322, X528, X529, X530, X531, .(','(tree(T311, T312, T313), -(T314, T315)), T323), .(','(T311, -(T314, .(T312, T317))), .(','(T313, -(T317, T315)), T324)), T325, T320, X532) :- balance5523(T306, T321, T322, X523, X524, X525, X526, T323, T324, T325, T307, X527).
balance5523(tree(T306, T307, T308), T321, T322, X528, X529, X530, X531, .(','(tree(T311, T312, T313), -(T314, T315)), T323), .(','(T311, -(T314, .(T312, T317))), .(','(T313, -(T317, T315)), T324)), T325, T320, X532) :- ','(balance55c23(T306, T321, T322, T344, T345, T346, T347, T323, T324, T325, T307, T348), balance5523(T308, T344, T345, X528, X529, X530, X531, T346, T347, T348, T320, X532)).
balance5513(tree(T452, T453, T454), T468, T469, T474, T473, .(','(tree(T459, T460, T461), -(T462, T463)), T470), .(','(T459, -(T462, .(T460, T465))), .(','(T461, -(T465, T463)), T471)), T472) :- balance5523(T452, T468, T469, X692, X693, X694, X695, T470, T471, T472, T453, X696).
balance5513(tree(T452, T453, T454), T468, T469, T498, T499, .(','(tree(T459, T460, T461), -(T462, T463)), T470), .(','(T459, -(T462, .(T460, T465))), .(','(T461, -(T465, T463)), T471)), T472) :- ','(balance55c23(T452, T468, T469, T493, T494, T495, T496, T470, T471, T472, T453, T497), balance5513(T454, T493, T494, T498, T499, T495, T496, T497)).
balance1(tree(tree(T139, T140, T141), T152, T22), tree(tree(T157, T158, T160), T161, T155)) :- balance5523(T139, X331, X332, X326, X327, X328, X329, .(','(T155, -(T156, [])), .(','(T157, -(T154, .(T158, T159))), .(','(T160, -(T159, .(T161, T156))), T153))), T153, T154, T140, X330).
balance1(tree(tree(T139, T140, T141), T152, T22), tree(tree(T157, T158, T160), T161, T155)) :- ','(balance55c23(T139, T184, T185, T186, T187, T188, T189, .(','(T155, -(T156, [])), .(','(T157, -(T154, .(T158, T159))), .(','(T160, -(T159, .(T161, T156))), T153))), T153, T154, T140, T190), balance5523(T141, T186, T187, X333, X334, X335, X336, T188, T189, T190, T152, X337)).
balance1(tree(T20, T21, T22), tree(T28, T29, T31)) :- ','(balance55c12(T20, T48, T49, T50, T51, T52, T53, T28, T27, T29, T30, T31, T26, T21, T54), balance5513(T22, T50, T51, T48, T49, T52, T53, T54)).

Clauses:

balance55c23(nil, T267, .(','(nil, -(T269, T269)), T270), T269, T270, T271, T272, T271, T272, .(T274, T275), T274, T275).
balance55c23(tree(T306, T307, T308), T321, T322, X528, X529, X530, X531, .(','(tree(T311, T312, T313), -(T314, T315)), T323), .(','(T311, -(T314, .(T312, T317))), .(','(T313, -(T317, T315)), T324)), T325, T320, X532) :- ','(balance55c23(T306, T321, T322, T344, T345, T346, T347, T323, T324, T325, T307, T348), balance55c23(T308, T344, T345, X528, X529, X530, X531, T346, T347, T348, T320, X532)).
balance55c13(nil, T415, [], T417, T418, .(','(nil, -(T417, T417)), T418), [], []).
balance55c13(tree(T452, T453, T454), T468, T469, T498, T499, .(','(tree(T459, T460, T461), -(T462, T463)), T470), .(','(T459, -(T462, .(T460, T465))), .(','(T461, -(T465, T463)), T471)), T472) :- ','(balance55c23(T452, T468, T469, T493, T494, T495, T496, T470, T471, T472, T453, T497), balance55c13(T454, T493, T494, T498, T499, T495, T496, T497)).
balance55c12(nil, X242, .(','(nil, -(X244, X244)), X245), X244, X245, .(','(T103, -(.(T109, T110), .(T105, T106))), .(','(T107, -(T106, [])), T108)), T108, T103, .(T109, T110), T105, T106, T107, T108, T109, T110).
balance55c12(tree(T139, T140, T141), T184, T185, X333, X334, X335, X336, tree(T157, T158, T160), T154, T161, T156, T155, .(','(T157, -(T154, .(T158, T159))), .(','(T160, -(T159, .(T161, T156))), T153)), T152, X337) :- ','(balance55c23(T139, T184, T185, T186, T187, T188, T189, .(','(T155, -(T156, [])), .(','(T157, -(T154, .(T158, T159))), .(','(T160, -(T159, .(T161, T156))), T153))), T153, T154, T140, T190), balance55c23(T141, T186, T187, X333, X334, X335, X336, T188, T189, T190, T152, X337)).

Afs:

balance1(x1, x2)  =  balance1(x1)

(3) TriplesToPiDPProof (SOUND transformation)

We use the technique of [LOPSTR]. With regard to the inferred argument filtering the predicates were used in the following modes:
balance1_in: (b,f)
balance5523_in: (b,f,f,f,f,f,f,f,f,f,b,f)
balance55c23_in: (b,f,f,f,f,f,f,f,f,f,b,f)
balance55c12_in: (b,f,f,f,f,f,f,f,f,f,f,f,f,b,f)
balance5513_in: (b,f,f,f,f,f,f,f)
Transforming TRIPLES into the following Term Rewriting System:
Pi DP problem:
The TRS P consists of the following rules:

BALANCE1_IN_GA(tree(tree(T139, T140, T141), T152, T22), tree(tree(T157, T158, T160), T161, T155)) → U7_GA(T139, T140, T141, T152, T22, T157, T158, T160, T161, T155, balance5523_in_gaaaaaaaaaga(T139, X331, X332, X326, X327, X328, X329, .(','(T155, -(T156, [])), .(','(T157, -(T154, .(T158, T159))), .(','(T160, -(T159, .(T161, T156))), T153))), T153, T154, T140, X330))
BALANCE1_IN_GA(tree(tree(T139, T140, T141), T152, T22), tree(tree(T157, T158, T160), T161, T155)) → BALANCE5523_IN_GAAAAAAAAAGA(T139, X331, X332, X326, X327, X328, X329, .(','(T155, -(T156, [])), .(','(T157, -(T154, .(T158, T159))), .(','(T160, -(T159, .(T161, T156))), T153))), T153, T154, T140, X330)
BALANCE5523_IN_GAAAAAAAAAGA(tree(T306, T307, T308), T321, T322, X528, X529, X530, X531, .(','(tree(T311, T312, T313), -(T314, T315)), T323), .(','(T311, -(T314, .(T312, T317))), .(','(T313, -(T317, T315)), T324)), T325, T320, X532) → U1_GAAAAAAAAAGA(T306, T307, T308, T321, T322, X528, X529, X530, X531, T311, T312, T313, T314, T315, T323, T317, T324, T325, T320, X532, balance5523_in_gaaaaaaaaaga(T306, T321, T322, X523, X524, X525, X526, T323, T324, T325, T307, X527))
BALANCE5523_IN_GAAAAAAAAAGA(tree(T306, T307, T308), T321, T322, X528, X529, X530, X531, .(','(tree(T311, T312, T313), -(T314, T315)), T323), .(','(T311, -(T314, .(T312, T317))), .(','(T313, -(T317, T315)), T324)), T325, T320, X532) → BALANCE5523_IN_GAAAAAAAAAGA(T306, T321, T322, X523, X524, X525, X526, T323, T324, T325, T307, X527)
BALANCE5523_IN_GAAAAAAAAAGA(tree(T306, T307, T308), T321, T322, X528, X529, X530, X531, .(','(tree(T311, T312, T313), -(T314, T315)), T323), .(','(T311, -(T314, .(T312, T317))), .(','(T313, -(T317, T315)), T324)), T325, T320, X532) → U2_GAAAAAAAAAGA(T306, T307, T308, T321, T322, X528, X529, X530, X531, T311, T312, T313, T314, T315, T323, T317, T324, T325, T320, X532, balance55c23_in_gaaaaaaaaaga(T306, T321, T322, T344, T345, T346, T347, T323, T324, T325, T307, T348))
U2_GAAAAAAAAAGA(T306, T307, T308, T321, T322, X528, X529, X530, X531, T311, T312, T313, T314, T315, T323, T317, T324, T325, T320, X532, balance55c23_out_gaaaaaaaaaga(T306, T321, T322, T344, T345, T346, T347, T323, T324, T325, T307, T348)) → U3_GAAAAAAAAAGA(T306, T307, T308, T321, T322, X528, X529, X530, X531, T311, T312, T313, T314, T315, T323, T317, T324, T325, T320, X532, balance5523_in_gaaaaaaaaaga(T308, T344, T345, X528, X529, X530, X531, T346, T347, T348, T320, X532))
U2_GAAAAAAAAAGA(T306, T307, T308, T321, T322, X528, X529, X530, X531, T311, T312, T313, T314, T315, T323, T317, T324, T325, T320, X532, balance55c23_out_gaaaaaaaaaga(T306, T321, T322, T344, T345, T346, T347, T323, T324, T325, T307, T348)) → BALANCE5523_IN_GAAAAAAAAAGA(T308, T344, T345, X528, X529, X530, X531, T346, T347, T348, T320, X532)
BALANCE1_IN_GA(tree(tree(T139, T140, T141), T152, T22), tree(tree(T157, T158, T160), T161, T155)) → U8_GA(T139, T140, T141, T152, T22, T157, T158, T160, T161, T155, balance55c23_in_gaaaaaaaaaga(T139, T184, T185, T186, T187, T188, T189, .(','(T155, -(T156, [])), .(','(T157, -(T154, .(T158, T159))), .(','(T160, -(T159, .(T161, T156))), T153))), T153, T154, T140, T190))
U8_GA(T139, T140, T141, T152, T22, T157, T158, T160, T161, T155, balance55c23_out_gaaaaaaaaaga(T139, T184, T185, T186, T187, T188, T189, .(','(T155, -(T156, [])), .(','(T157, -(T154, .(T158, T159))), .(','(T160, -(T159, .(T161, T156))), T153))), T153, T154, T140, T190)) → U9_GA(T139, T140, T141, T152, T22, T157, T158, T160, T161, T155, balance5523_in_gaaaaaaaaaga(T141, T186, T187, X333, X334, X335, X336, T188, T189, T190, T152, X337))
U8_GA(T139, T140, T141, T152, T22, T157, T158, T160, T161, T155, balance55c23_out_gaaaaaaaaaga(T139, T184, T185, T186, T187, T188, T189, .(','(T155, -(T156, [])), .(','(T157, -(T154, .(T158, T159))), .(','(T160, -(T159, .(T161, T156))), T153))), T153, T154, T140, T190)) → BALANCE5523_IN_GAAAAAAAAAGA(T141, T186, T187, X333, X334, X335, X336, T188, T189, T190, T152, X337)
BALANCE1_IN_GA(tree(T20, T21, T22), tree(T28, T29, T31)) → U10_GA(T20, T21, T22, T28, T29, T31, balance55c12_in_gaaaaaaaaaaaaga(T20, T48, T49, T50, T51, T52, T53, T28, T27, T29, T30, T31, T26, T21, T54))
U10_GA(T20, T21, T22, T28, T29, T31, balance55c12_out_gaaaaaaaaaaaaga(T20, T48, T49, T50, T51, T52, T53, T28, T27, T29, T30, T31, T26, T21, T54)) → U11_GA(T20, T21, T22, T28, T29, T31, balance5513_in_gaaaaaaa(T22, T50, T51, T48, T49, T52, T53, T54))
U10_GA(T20, T21, T22, T28, T29, T31, balance55c12_out_gaaaaaaaaaaaaga(T20, T48, T49, T50, T51, T52, T53, T28, T27, T29, T30, T31, T26, T21, T54)) → BALANCE5513_IN_GAAAAAAA(T22, T50, T51, T48, T49, T52, T53, T54)
BALANCE5513_IN_GAAAAAAA(tree(T452, T453, T454), T468, T469, T474, T473, .(','(tree(T459, T460, T461), -(T462, T463)), T470), .(','(T459, -(T462, .(T460, T465))), .(','(T461, -(T465, T463)), T471)), T472) → U4_GAAAAAAA(T452, T453, T454, T468, T469, T474, T473, T459, T460, T461, T462, T463, T470, T465, T471, T472, balance5523_in_gaaaaaaaaaga(T452, T468, T469, X692, X693, X694, X695, T470, T471, T472, T453, X696))
BALANCE5513_IN_GAAAAAAA(tree(T452, T453, T454), T468, T469, T474, T473, .(','(tree(T459, T460, T461), -(T462, T463)), T470), .(','(T459, -(T462, .(T460, T465))), .(','(T461, -(T465, T463)), T471)), T472) → BALANCE5523_IN_GAAAAAAAAAGA(T452, T468, T469, X692, X693, X694, X695, T470, T471, T472, T453, X696)
BALANCE5513_IN_GAAAAAAA(tree(T452, T453, T454), T468, T469, T498, T499, .(','(tree(T459, T460, T461), -(T462, T463)), T470), .(','(T459, -(T462, .(T460, T465))), .(','(T461, -(T465, T463)), T471)), T472) → U5_GAAAAAAA(T452, T453, T454, T468, T469, T498, T499, T459, T460, T461, T462, T463, T470, T465, T471, T472, balance55c23_in_gaaaaaaaaaga(T452, T468, T469, T493, T494, T495, T496, T470, T471, T472, T453, T497))
U5_GAAAAAAA(T452, T453, T454, T468, T469, T498, T499, T459, T460, T461, T462, T463, T470, T465, T471, T472, balance55c23_out_gaaaaaaaaaga(T452, T468, T469, T493, T494, T495, T496, T470, T471, T472, T453, T497)) → U6_GAAAAAAA(T452, T453, T454, T468, T469, T498, T499, T459, T460, T461, T462, T463, T470, T465, T471, T472, balance5513_in_gaaaaaaa(T454, T493, T494, T498, T499, T495, T496, T497))
U5_GAAAAAAA(T452, T453, T454, T468, T469, T498, T499, T459, T460, T461, T462, T463, T470, T465, T471, T472, balance55c23_out_gaaaaaaaaaga(T452, T468, T469, T493, T494, T495, T496, T470, T471, T472, T453, T497)) → BALANCE5513_IN_GAAAAAAA(T454, T493, T494, T498, T499, T495, T496, T497)

The TRS R consists of the following rules:

balance55c23_in_gaaaaaaaaaga(nil, T267, .(','(nil, -(T269, T269)), T270), T269, T270, T271, T272, T271, T272, .(T274, T275), T274, T275) → balance55c23_out_gaaaaaaaaaga(nil, T267, .(','(nil, -(T269, T269)), T270), T269, T270, T271, T272, T271, T272, .(T274, T275), T274, T275)
balance55c23_in_gaaaaaaaaaga(tree(T306, T307, T308), T321, T322, X528, X529, X530, X531, .(','(tree(T311, T312, T313), -(T314, T315)), T323), .(','(T311, -(T314, .(T312, T317))), .(','(T313, -(T317, T315)), T324)), T325, T320, X532) → U13_gaaaaaaaaaga(T306, T307, T308, T321, T322, X528, X529, X530, X531, T311, T312, T313, T314, T315, T323, T317, T324, T325, T320, X532, balance55c23_in_gaaaaaaaaaga(T306, T321, T322, T344, T345, T346, T347, T323, T324, T325, T307, T348))
U13_gaaaaaaaaaga(T306, T307, T308, T321, T322, X528, X529, X530, X531, T311, T312, T313, T314, T315, T323, T317, T324, T325, T320, X532, balance55c23_out_gaaaaaaaaaga(T306, T321, T322, T344, T345, T346, T347, T323, T324, T325, T307, T348)) → U14_gaaaaaaaaaga(T306, T307, T308, T321, T322, X528, X529, X530, X531, T311, T312, T313, T314, T315, T323, T317, T324, T325, T320, X532, T344, T345, T346, T347, T348, balance55c23_in_gaaaaaaaaaga(T308, T344, T345, X528, X529, X530, X531, T346, T347, T348, T320, X532))
U14_gaaaaaaaaaga(T306, T307, T308, T321, T322, X528, X529, X530, X531, T311, T312, T313, T314, T315, T323, T317, T324, T325, T320, X532, T344, T345, T346, T347, T348, balance55c23_out_gaaaaaaaaaga(T308, T344, T345, X528, X529, X530, X531, T346, T347, T348, T320, X532)) → balance55c23_out_gaaaaaaaaaga(tree(T306, T307, T308), T321, T322, X528, X529, X530, X531, .(','(tree(T311, T312, T313), -(T314, T315)), T323), .(','(T311, -(T314, .(T312, T317))), .(','(T313, -(T317, T315)), T324)), T325, T320, X532)
balance55c12_in_gaaaaaaaaaaaaga(nil, X242, .(','(nil, -(X244, X244)), X245), X244, X245, .(','(T103, -(.(T109, T110), .(T105, T106))), .(','(T107, -(T106, [])), T108)), T108, T103, .(T109, T110), T105, T106, T107, T108, T109, T110) → balance55c12_out_gaaaaaaaaaaaaga(nil, X242, .(','(nil, -(X244, X244)), X245), X244, X245, .(','(T103, -(.(T109, T110), .(T105, T106))), .(','(T107, -(T106, [])), T108)), T108, T103, .(T109, T110), T105, T106, T107, T108, T109, T110)
balance55c12_in_gaaaaaaaaaaaaga(tree(T139, T140, T141), T184, T185, X333, X334, X335, X336, tree(T157, T158, T160), T154, T161, T156, T155, .(','(T157, -(T154, .(T158, T159))), .(','(T160, -(T159, .(T161, T156))), T153)), T152, X337) → U17_gaaaaaaaaaaaaga(T139, T140, T141, T184, T185, X333, X334, X335, X336, T157, T158, T160, T154, T161, T156, T155, T159, T153, T152, X337, balance55c23_in_gaaaaaaaaaga(T139, T184, T185, T186, T187, T188, T189, .(','(T155, -(T156, [])), .(','(T157, -(T154, .(T158, T159))), .(','(T160, -(T159, .(T161, T156))), T153))), T153, T154, T140, T190))
U17_gaaaaaaaaaaaaga(T139, T140, T141, T184, T185, X333, X334, X335, X336, T157, T158, T160, T154, T161, T156, T155, T159, T153, T152, X337, balance55c23_out_gaaaaaaaaaga(T139, T184, T185, T186, T187, T188, T189, .(','(T155, -(T156, [])), .(','(T157, -(T154, .(T158, T159))), .(','(T160, -(T159, .(T161, T156))), T153))), T153, T154, T140, T190)) → U18_gaaaaaaaaaaaaga(T139, T140, T141, T184, T185, X333, X334, X335, X336, T157, T158, T160, T154, T161, T156, T155, T159, T153, T152, X337, T186, T187, T188, T189, T190, balance55c23_in_gaaaaaaaaaga(T141, T186, T187, X333, X334, X335, X336, T188, T189, T190, T152, X337))
U18_gaaaaaaaaaaaaga(T139, T140, T141, T184, T185, X333, X334, X335, X336, T157, T158, T160, T154, T161, T156, T155, T159, T153, T152, X337, T186, T187, T188, T189, T190, balance55c23_out_gaaaaaaaaaga(T141, T186, T187, X333, X334, X335, X336, T188, T189, T190, T152, X337)) → balance55c12_out_gaaaaaaaaaaaaga(tree(T139, T140, T141), T184, T185, X333, X334, X335, X336, tree(T157, T158, T160), T154, T161, T156, T155, .(','(T157, -(T154, .(T158, T159))), .(','(T160, -(T159, .(T161, T156))), T153)), T152, X337)

The argument filtering Pi contains the following mapping:
tree(x1, x2, x3)  =  tree(x1, x2, x3)
balance5523_in_gaaaaaaaaaga(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12)  =  balance5523_in_gaaaaaaaaaga(x1, x11)
balance55c23_in_gaaaaaaaaaga(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12)  =  balance55c23_in_gaaaaaaaaaga(x1, x11)
nil  =  nil
balance55c23_out_gaaaaaaaaaga(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12)  =  balance55c23_out_gaaaaaaaaaga(x1, x11)
U13_gaaaaaaaaaga(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21)  =  U13_gaaaaaaaaaga(x1, x2, x3, x19, x21)
U14_gaaaaaaaaaga(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22, x23, x24, x25, x26)  =  U14_gaaaaaaaaaga(x1, x2, x3, x19, x26)
balance55c12_in_gaaaaaaaaaaaaga(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15)  =  balance55c12_in_gaaaaaaaaaaaaga(x1, x14)
balance55c12_out_gaaaaaaaaaaaaga(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15)  =  balance55c12_out_gaaaaaaaaaaaaga(x1, x14)
U17_gaaaaaaaaaaaaga(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21)  =  U17_gaaaaaaaaaaaaga(x1, x2, x3, x19, x21)
U18_gaaaaaaaaaaaaga(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22, x23, x24, x25, x26)  =  U18_gaaaaaaaaaaaaga(x1, x2, x3, x19, x26)
balance5513_in_gaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  balance5513_in_gaaaaaaa(x1)
BALANCE1_IN_GA(x1, x2)  =  BALANCE1_IN_GA(x1)
U7_GA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11)  =  U7_GA(x1, x2, x3, x4, x5, x11)
BALANCE5523_IN_GAAAAAAAAAGA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12)  =  BALANCE5523_IN_GAAAAAAAAAGA(x1, x11)
U1_GAAAAAAAAAGA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21)  =  U1_GAAAAAAAAAGA(x1, x2, x3, x19, x21)
U2_GAAAAAAAAAGA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21)  =  U2_GAAAAAAAAAGA(x1, x2, x3, x19, x21)
U3_GAAAAAAAAAGA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21)  =  U3_GAAAAAAAAAGA(x1, x2, x3, x19, x21)
U8_GA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11)  =  U8_GA(x1, x2, x3, x4, x5, x11)
U9_GA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11)  =  U9_GA(x1, x2, x3, x4, x5, x11)
U10_GA(x1, x2, x3, x4, x5, x6, x7)  =  U10_GA(x1, x2, x3, x7)
U11_GA(x1, x2, x3, x4, x5, x6, x7)  =  U11_GA(x1, x2, x3, x7)
BALANCE5513_IN_GAAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8)  =  BALANCE5513_IN_GAAAAAAA(x1)
U4_GAAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17)  =  U4_GAAAAAAA(x1, x2, x3, x17)
U5_GAAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17)  =  U5_GAAAAAAA(x1, x2, x3, x17)
U6_GAAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17)  =  U6_GAAAAAAA(x1, x2, x3, x17)

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

Infinitary Constructor Rewriting Termination of PiDP implies Termination of TRIPLES

(4) Obligation:

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

BALANCE1_IN_GA(tree(tree(T139, T140, T141), T152, T22), tree(tree(T157, T158, T160), T161, T155)) → U7_GA(T139, T140, T141, T152, T22, T157, T158, T160, T161, T155, balance5523_in_gaaaaaaaaaga(T139, X331, X332, X326, X327, X328, X329, .(','(T155, -(T156, [])), .(','(T157, -(T154, .(T158, T159))), .(','(T160, -(T159, .(T161, T156))), T153))), T153, T154, T140, X330))
BALANCE1_IN_GA(tree(tree(T139, T140, T141), T152, T22), tree(tree(T157, T158, T160), T161, T155)) → BALANCE5523_IN_GAAAAAAAAAGA(T139, X331, X332, X326, X327, X328, X329, .(','(T155, -(T156, [])), .(','(T157, -(T154, .(T158, T159))), .(','(T160, -(T159, .(T161, T156))), T153))), T153, T154, T140, X330)
BALANCE5523_IN_GAAAAAAAAAGA(tree(T306, T307, T308), T321, T322, X528, X529, X530, X531, .(','(tree(T311, T312, T313), -(T314, T315)), T323), .(','(T311, -(T314, .(T312, T317))), .(','(T313, -(T317, T315)), T324)), T325, T320, X532) → U1_GAAAAAAAAAGA(T306, T307, T308, T321, T322, X528, X529, X530, X531, T311, T312, T313, T314, T315, T323, T317, T324, T325, T320, X532, balance5523_in_gaaaaaaaaaga(T306, T321, T322, X523, X524, X525, X526, T323, T324, T325, T307, X527))
BALANCE5523_IN_GAAAAAAAAAGA(tree(T306, T307, T308), T321, T322, X528, X529, X530, X531, .(','(tree(T311, T312, T313), -(T314, T315)), T323), .(','(T311, -(T314, .(T312, T317))), .(','(T313, -(T317, T315)), T324)), T325, T320, X532) → BALANCE5523_IN_GAAAAAAAAAGA(T306, T321, T322, X523, X524, X525, X526, T323, T324, T325, T307, X527)
BALANCE5523_IN_GAAAAAAAAAGA(tree(T306, T307, T308), T321, T322, X528, X529, X530, X531, .(','(tree(T311, T312, T313), -(T314, T315)), T323), .(','(T311, -(T314, .(T312, T317))), .(','(T313, -(T317, T315)), T324)), T325, T320, X532) → U2_GAAAAAAAAAGA(T306, T307, T308, T321, T322, X528, X529, X530, X531, T311, T312, T313, T314, T315, T323, T317, T324, T325, T320, X532, balance55c23_in_gaaaaaaaaaga(T306, T321, T322, T344, T345, T346, T347, T323, T324, T325, T307, T348))
U2_GAAAAAAAAAGA(T306, T307, T308, T321, T322, X528, X529, X530, X531, T311, T312, T313, T314, T315, T323, T317, T324, T325, T320, X532, balance55c23_out_gaaaaaaaaaga(T306, T321, T322, T344, T345, T346, T347, T323, T324, T325, T307, T348)) → U3_GAAAAAAAAAGA(T306, T307, T308, T321, T322, X528, X529, X530, X531, T311, T312, T313, T314, T315, T323, T317, T324, T325, T320, X532, balance5523_in_gaaaaaaaaaga(T308, T344, T345, X528, X529, X530, X531, T346, T347, T348, T320, X532))
U2_GAAAAAAAAAGA(T306, T307, T308, T321, T322, X528, X529, X530, X531, T311, T312, T313, T314, T315, T323, T317, T324, T325, T320, X532, balance55c23_out_gaaaaaaaaaga(T306, T321, T322, T344, T345, T346, T347, T323, T324, T325, T307, T348)) → BALANCE5523_IN_GAAAAAAAAAGA(T308, T344, T345, X528, X529, X530, X531, T346, T347, T348, T320, X532)
BALANCE1_IN_GA(tree(tree(T139, T140, T141), T152, T22), tree(tree(T157, T158, T160), T161, T155)) → U8_GA(T139, T140, T141, T152, T22, T157, T158, T160, T161, T155, balance55c23_in_gaaaaaaaaaga(T139, T184, T185, T186, T187, T188, T189, .(','(T155, -(T156, [])), .(','(T157, -(T154, .(T158, T159))), .(','(T160, -(T159, .(T161, T156))), T153))), T153, T154, T140, T190))
U8_GA(T139, T140, T141, T152, T22, T157, T158, T160, T161, T155, balance55c23_out_gaaaaaaaaaga(T139, T184, T185, T186, T187, T188, T189, .(','(T155, -(T156, [])), .(','(T157, -(T154, .(T158, T159))), .(','(T160, -(T159, .(T161, T156))), T153))), T153, T154, T140, T190)) → U9_GA(T139, T140, T141, T152, T22, T157, T158, T160, T161, T155, balance5523_in_gaaaaaaaaaga(T141, T186, T187, X333, X334, X335, X336, T188, T189, T190, T152, X337))
U8_GA(T139, T140, T141, T152, T22, T157, T158, T160, T161, T155, balance55c23_out_gaaaaaaaaaga(T139, T184, T185, T186, T187, T188, T189, .(','(T155, -(T156, [])), .(','(T157, -(T154, .(T158, T159))), .(','(T160, -(T159, .(T161, T156))), T153))), T153, T154, T140, T190)) → BALANCE5523_IN_GAAAAAAAAAGA(T141, T186, T187, X333, X334, X335, X336, T188, T189, T190, T152, X337)
BALANCE1_IN_GA(tree(T20, T21, T22), tree(T28, T29, T31)) → U10_GA(T20, T21, T22, T28, T29, T31, balance55c12_in_gaaaaaaaaaaaaga(T20, T48, T49, T50, T51, T52, T53, T28, T27, T29, T30, T31, T26, T21, T54))
U10_GA(T20, T21, T22, T28, T29, T31, balance55c12_out_gaaaaaaaaaaaaga(T20, T48, T49, T50, T51, T52, T53, T28, T27, T29, T30, T31, T26, T21, T54)) → U11_GA(T20, T21, T22, T28, T29, T31, balance5513_in_gaaaaaaa(T22, T50, T51, T48, T49, T52, T53, T54))
U10_GA(T20, T21, T22, T28, T29, T31, balance55c12_out_gaaaaaaaaaaaaga(T20, T48, T49, T50, T51, T52, T53, T28, T27, T29, T30, T31, T26, T21, T54)) → BALANCE5513_IN_GAAAAAAA(T22, T50, T51, T48, T49, T52, T53, T54)
BALANCE5513_IN_GAAAAAAA(tree(T452, T453, T454), T468, T469, T474, T473, .(','(tree(T459, T460, T461), -(T462, T463)), T470), .(','(T459, -(T462, .(T460, T465))), .(','(T461, -(T465, T463)), T471)), T472) → U4_GAAAAAAA(T452, T453, T454, T468, T469, T474, T473, T459, T460, T461, T462, T463, T470, T465, T471, T472, balance5523_in_gaaaaaaaaaga(T452, T468, T469, X692, X693, X694, X695, T470, T471, T472, T453, X696))
BALANCE5513_IN_GAAAAAAA(tree(T452, T453, T454), T468, T469, T474, T473, .(','(tree(T459, T460, T461), -(T462, T463)), T470), .(','(T459, -(T462, .(T460, T465))), .(','(T461, -(T465, T463)), T471)), T472) → BALANCE5523_IN_GAAAAAAAAAGA(T452, T468, T469, X692, X693, X694, X695, T470, T471, T472, T453, X696)
BALANCE5513_IN_GAAAAAAA(tree(T452, T453, T454), T468, T469, T498, T499, .(','(tree(T459, T460, T461), -(T462, T463)), T470), .(','(T459, -(T462, .(T460, T465))), .(','(T461, -(T465, T463)), T471)), T472) → U5_GAAAAAAA(T452, T453, T454, T468, T469, T498, T499, T459, T460, T461, T462, T463, T470, T465, T471, T472, balance55c23_in_gaaaaaaaaaga(T452, T468, T469, T493, T494, T495, T496, T470, T471, T472, T453, T497))
U5_GAAAAAAA(T452, T453, T454, T468, T469, T498, T499, T459, T460, T461, T462, T463, T470, T465, T471, T472, balance55c23_out_gaaaaaaaaaga(T452, T468, T469, T493, T494, T495, T496, T470, T471, T472, T453, T497)) → U6_GAAAAAAA(T452, T453, T454, T468, T469, T498, T499, T459, T460, T461, T462, T463, T470, T465, T471, T472, balance5513_in_gaaaaaaa(T454, T493, T494, T498, T499, T495, T496, T497))
U5_GAAAAAAA(T452, T453, T454, T468, T469, T498, T499, T459, T460, T461, T462, T463, T470, T465, T471, T472, balance55c23_out_gaaaaaaaaaga(T452, T468, T469, T493, T494, T495, T496, T470, T471, T472, T453, T497)) → BALANCE5513_IN_GAAAAAAA(T454, T493, T494, T498, T499, T495, T496, T497)

The TRS R consists of the following rules:

balance55c23_in_gaaaaaaaaaga(nil, T267, .(','(nil, -(T269, T269)), T270), T269, T270, T271, T272, T271, T272, .(T274, T275), T274, T275) → balance55c23_out_gaaaaaaaaaga(nil, T267, .(','(nil, -(T269, T269)), T270), T269, T270, T271, T272, T271, T272, .(T274, T275), T274, T275)
balance55c23_in_gaaaaaaaaaga(tree(T306, T307, T308), T321, T322, X528, X529, X530, X531, .(','(tree(T311, T312, T313), -(T314, T315)), T323), .(','(T311, -(T314, .(T312, T317))), .(','(T313, -(T317, T315)), T324)), T325, T320, X532) → U13_gaaaaaaaaaga(T306, T307, T308, T321, T322, X528, X529, X530, X531, T311, T312, T313, T314, T315, T323, T317, T324, T325, T320, X532, balance55c23_in_gaaaaaaaaaga(T306, T321, T322, T344, T345, T346, T347, T323, T324, T325, T307, T348))
U13_gaaaaaaaaaga(T306, T307, T308, T321, T322, X528, X529, X530, X531, T311, T312, T313, T314, T315, T323, T317, T324, T325, T320, X532, balance55c23_out_gaaaaaaaaaga(T306, T321, T322, T344, T345, T346, T347, T323, T324, T325, T307, T348)) → U14_gaaaaaaaaaga(T306, T307, T308, T321, T322, X528, X529, X530, X531, T311, T312, T313, T314, T315, T323, T317, T324, T325, T320, X532, T344, T345, T346, T347, T348, balance55c23_in_gaaaaaaaaaga(T308, T344, T345, X528, X529, X530, X531, T346, T347, T348, T320, X532))
U14_gaaaaaaaaaga(T306, T307, T308, T321, T322, X528, X529, X530, X531, T311, T312, T313, T314, T315, T323, T317, T324, T325, T320, X532, T344, T345, T346, T347, T348, balance55c23_out_gaaaaaaaaaga(T308, T344, T345, X528, X529, X530, X531, T346, T347, T348, T320, X532)) → balance55c23_out_gaaaaaaaaaga(tree(T306, T307, T308), T321, T322, X528, X529, X530, X531, .(','(tree(T311, T312, T313), -(T314, T315)), T323), .(','(T311, -(T314, .(T312, T317))), .(','(T313, -(T317, T315)), T324)), T325, T320, X532)
balance55c12_in_gaaaaaaaaaaaaga(nil, X242, .(','(nil, -(X244, X244)), X245), X244, X245, .(','(T103, -(.(T109, T110), .(T105, T106))), .(','(T107, -(T106, [])), T108)), T108, T103, .(T109, T110), T105, T106, T107, T108, T109, T110) → balance55c12_out_gaaaaaaaaaaaaga(nil, X242, .(','(nil, -(X244, X244)), X245), X244, X245, .(','(T103, -(.(T109, T110), .(T105, T106))), .(','(T107, -(T106, [])), T108)), T108, T103, .(T109, T110), T105, T106, T107, T108, T109, T110)
balance55c12_in_gaaaaaaaaaaaaga(tree(T139, T140, T141), T184, T185, X333, X334, X335, X336, tree(T157, T158, T160), T154, T161, T156, T155, .(','(T157, -(T154, .(T158, T159))), .(','(T160, -(T159, .(T161, T156))), T153)), T152, X337) → U17_gaaaaaaaaaaaaga(T139, T140, T141, T184, T185, X333, X334, X335, X336, T157, T158, T160, T154, T161, T156, T155, T159, T153, T152, X337, balance55c23_in_gaaaaaaaaaga(T139, T184, T185, T186, T187, T188, T189, .(','(T155, -(T156, [])), .(','(T157, -(T154, .(T158, T159))), .(','(T160, -(T159, .(T161, T156))), T153))), T153, T154, T140, T190))
U17_gaaaaaaaaaaaaga(T139, T140, T141, T184, T185, X333, X334, X335, X336, T157, T158, T160, T154, T161, T156, T155, T159, T153, T152, X337, balance55c23_out_gaaaaaaaaaga(T139, T184, T185, T186, T187, T188, T189, .(','(T155, -(T156, [])), .(','(T157, -(T154, .(T158, T159))), .(','(T160, -(T159, .(T161, T156))), T153))), T153, T154, T140, T190)) → U18_gaaaaaaaaaaaaga(T139, T140, T141, T184, T185, X333, X334, X335, X336, T157, T158, T160, T154, T161, T156, T155, T159, T153, T152, X337, T186, T187, T188, T189, T190, balance55c23_in_gaaaaaaaaaga(T141, T186, T187, X333, X334, X335, X336, T188, T189, T190, T152, X337))
U18_gaaaaaaaaaaaaga(T139, T140, T141, T184, T185, X333, X334, X335, X336, T157, T158, T160, T154, T161, T156, T155, T159, T153, T152, X337, T186, T187, T188, T189, T190, balance55c23_out_gaaaaaaaaaga(T141, T186, T187, X333, X334, X335, X336, T188, T189, T190, T152, X337)) → balance55c12_out_gaaaaaaaaaaaaga(tree(T139, T140, T141), T184, T185, X333, X334, X335, X336, tree(T157, T158, T160), T154, T161, T156, T155, .(','(T157, -(T154, .(T158, T159))), .(','(T160, -(T159, .(T161, T156))), T153)), T152, X337)

The argument filtering Pi contains the following mapping:
tree(x1, x2, x3)  =  tree(x1, x2, x3)
balance5523_in_gaaaaaaaaaga(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12)  =  balance5523_in_gaaaaaaaaaga(x1, x11)
balance55c23_in_gaaaaaaaaaga(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12)  =  balance55c23_in_gaaaaaaaaaga(x1, x11)
nil  =  nil
balance55c23_out_gaaaaaaaaaga(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12)  =  balance55c23_out_gaaaaaaaaaga(x1, x11)
U13_gaaaaaaaaaga(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21)  =  U13_gaaaaaaaaaga(x1, x2, x3, x19, x21)
U14_gaaaaaaaaaga(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22, x23, x24, x25, x26)  =  U14_gaaaaaaaaaga(x1, x2, x3, x19, x26)
balance55c12_in_gaaaaaaaaaaaaga(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15)  =  balance55c12_in_gaaaaaaaaaaaaga(x1, x14)
balance55c12_out_gaaaaaaaaaaaaga(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15)  =  balance55c12_out_gaaaaaaaaaaaaga(x1, x14)
U17_gaaaaaaaaaaaaga(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21)  =  U17_gaaaaaaaaaaaaga(x1, x2, x3, x19, x21)
U18_gaaaaaaaaaaaaga(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22, x23, x24, x25, x26)  =  U18_gaaaaaaaaaaaaga(x1, x2, x3, x19, x26)
balance5513_in_gaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  balance5513_in_gaaaaaaa(x1)
BALANCE1_IN_GA(x1, x2)  =  BALANCE1_IN_GA(x1)
U7_GA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11)  =  U7_GA(x1, x2, x3, x4, x5, x11)
BALANCE5523_IN_GAAAAAAAAAGA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12)  =  BALANCE5523_IN_GAAAAAAAAAGA(x1, x11)
U1_GAAAAAAAAAGA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21)  =  U1_GAAAAAAAAAGA(x1, x2, x3, x19, x21)
U2_GAAAAAAAAAGA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21)  =  U2_GAAAAAAAAAGA(x1, x2, x3, x19, x21)
U3_GAAAAAAAAAGA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21)  =  U3_GAAAAAAAAAGA(x1, x2, x3, x19, x21)
U8_GA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11)  =  U8_GA(x1, x2, x3, x4, x5, x11)
U9_GA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11)  =  U9_GA(x1, x2, x3, x4, x5, x11)
U10_GA(x1, x2, x3, x4, x5, x6, x7)  =  U10_GA(x1, x2, x3, x7)
U11_GA(x1, x2, x3, x4, x5, x6, x7)  =  U11_GA(x1, x2, x3, x7)
BALANCE5513_IN_GAAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8)  =  BALANCE5513_IN_GAAAAAAA(x1)
U4_GAAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17)  =  U4_GAAAAAAA(x1, x2, x3, x17)
U5_GAAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17)  =  U5_GAAAAAAA(x1, x2, x3, x17)
U6_GAAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17)  =  U6_GAAAAAAA(x1, x2, x3, x17)

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

(5) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 2 SCCs with 13 less nodes.

(6) Complex Obligation (AND)

(7) Obligation:

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

BALANCE5523_IN_GAAAAAAAAAGA(tree(T306, T307, T308), T321, T322, X528, X529, X530, X531, .(','(tree(T311, T312, T313), -(T314, T315)), T323), .(','(T311, -(T314, .(T312, T317))), .(','(T313, -(T317, T315)), T324)), T325, T320, X532) → U2_GAAAAAAAAAGA(T306, T307, T308, T321, T322, X528, X529, X530, X531, T311, T312, T313, T314, T315, T323, T317, T324, T325, T320, X532, balance55c23_in_gaaaaaaaaaga(T306, T321, T322, T344, T345, T346, T347, T323, T324, T325, T307, T348))
U2_GAAAAAAAAAGA(T306, T307, T308, T321, T322, X528, X529, X530, X531, T311, T312, T313, T314, T315, T323, T317, T324, T325, T320, X532, balance55c23_out_gaaaaaaaaaga(T306, T321, T322, T344, T345, T346, T347, T323, T324, T325, T307, T348)) → BALANCE5523_IN_GAAAAAAAAAGA(T308, T344, T345, X528, X529, X530, X531, T346, T347, T348, T320, X532)
BALANCE5523_IN_GAAAAAAAAAGA(tree(T306, T307, T308), T321, T322, X528, X529, X530, X531, .(','(tree(T311, T312, T313), -(T314, T315)), T323), .(','(T311, -(T314, .(T312, T317))), .(','(T313, -(T317, T315)), T324)), T325, T320, X532) → BALANCE5523_IN_GAAAAAAAAAGA(T306, T321, T322, X523, X524, X525, X526, T323, T324, T325, T307, X527)

The TRS R consists of the following rules:

balance55c23_in_gaaaaaaaaaga(nil, T267, .(','(nil, -(T269, T269)), T270), T269, T270, T271, T272, T271, T272, .(T274, T275), T274, T275) → balance55c23_out_gaaaaaaaaaga(nil, T267, .(','(nil, -(T269, T269)), T270), T269, T270, T271, T272, T271, T272, .(T274, T275), T274, T275)
balance55c23_in_gaaaaaaaaaga(tree(T306, T307, T308), T321, T322, X528, X529, X530, X531, .(','(tree(T311, T312, T313), -(T314, T315)), T323), .(','(T311, -(T314, .(T312, T317))), .(','(T313, -(T317, T315)), T324)), T325, T320, X532) → U13_gaaaaaaaaaga(T306, T307, T308, T321, T322, X528, X529, X530, X531, T311, T312, T313, T314, T315, T323, T317, T324, T325, T320, X532, balance55c23_in_gaaaaaaaaaga(T306, T321, T322, T344, T345, T346, T347, T323, T324, T325, T307, T348))
U13_gaaaaaaaaaga(T306, T307, T308, T321, T322, X528, X529, X530, X531, T311, T312, T313, T314, T315, T323, T317, T324, T325, T320, X532, balance55c23_out_gaaaaaaaaaga(T306, T321, T322, T344, T345, T346, T347, T323, T324, T325, T307, T348)) → U14_gaaaaaaaaaga(T306, T307, T308, T321, T322, X528, X529, X530, X531, T311, T312, T313, T314, T315, T323, T317, T324, T325, T320, X532, T344, T345, T346, T347, T348, balance55c23_in_gaaaaaaaaaga(T308, T344, T345, X528, X529, X530, X531, T346, T347, T348, T320, X532))
U14_gaaaaaaaaaga(T306, T307, T308, T321, T322, X528, X529, X530, X531, T311, T312, T313, T314, T315, T323, T317, T324, T325, T320, X532, T344, T345, T346, T347, T348, balance55c23_out_gaaaaaaaaaga(T308, T344, T345, X528, X529, X530, X531, T346, T347, T348, T320, X532)) → balance55c23_out_gaaaaaaaaaga(tree(T306, T307, T308), T321, T322, X528, X529, X530, X531, .(','(tree(T311, T312, T313), -(T314, T315)), T323), .(','(T311, -(T314, .(T312, T317))), .(','(T313, -(T317, T315)), T324)), T325, T320, X532)
balance55c12_in_gaaaaaaaaaaaaga(nil, X242, .(','(nil, -(X244, X244)), X245), X244, X245, .(','(T103, -(.(T109, T110), .(T105, T106))), .(','(T107, -(T106, [])), T108)), T108, T103, .(T109, T110), T105, T106, T107, T108, T109, T110) → balance55c12_out_gaaaaaaaaaaaaga(nil, X242, .(','(nil, -(X244, X244)), X245), X244, X245, .(','(T103, -(.(T109, T110), .(T105, T106))), .(','(T107, -(T106, [])), T108)), T108, T103, .(T109, T110), T105, T106, T107, T108, T109, T110)
balance55c12_in_gaaaaaaaaaaaaga(tree(T139, T140, T141), T184, T185, X333, X334, X335, X336, tree(T157, T158, T160), T154, T161, T156, T155, .(','(T157, -(T154, .(T158, T159))), .(','(T160, -(T159, .(T161, T156))), T153)), T152, X337) → U17_gaaaaaaaaaaaaga(T139, T140, T141, T184, T185, X333, X334, X335, X336, T157, T158, T160, T154, T161, T156, T155, T159, T153, T152, X337, balance55c23_in_gaaaaaaaaaga(T139, T184, T185, T186, T187, T188, T189, .(','(T155, -(T156, [])), .(','(T157, -(T154, .(T158, T159))), .(','(T160, -(T159, .(T161, T156))), T153))), T153, T154, T140, T190))
U17_gaaaaaaaaaaaaga(T139, T140, T141, T184, T185, X333, X334, X335, X336, T157, T158, T160, T154, T161, T156, T155, T159, T153, T152, X337, balance55c23_out_gaaaaaaaaaga(T139, T184, T185, T186, T187, T188, T189, .(','(T155, -(T156, [])), .(','(T157, -(T154, .(T158, T159))), .(','(T160, -(T159, .(T161, T156))), T153))), T153, T154, T140, T190)) → U18_gaaaaaaaaaaaaga(T139, T140, T141, T184, T185, X333, X334, X335, X336, T157, T158, T160, T154, T161, T156, T155, T159, T153, T152, X337, T186, T187, T188, T189, T190, balance55c23_in_gaaaaaaaaaga(T141, T186, T187, X333, X334, X335, X336, T188, T189, T190, T152, X337))
U18_gaaaaaaaaaaaaga(T139, T140, T141, T184, T185, X333, X334, X335, X336, T157, T158, T160, T154, T161, T156, T155, T159, T153, T152, X337, T186, T187, T188, T189, T190, balance55c23_out_gaaaaaaaaaga(T141, T186, T187, X333, X334, X335, X336, T188, T189, T190, T152, X337)) → balance55c12_out_gaaaaaaaaaaaaga(tree(T139, T140, T141), T184, T185, X333, X334, X335, X336, tree(T157, T158, T160), T154, T161, T156, T155, .(','(T157, -(T154, .(T158, T159))), .(','(T160, -(T159, .(T161, T156))), T153)), T152, X337)

The argument filtering Pi contains the following mapping:
tree(x1, x2, x3)  =  tree(x1, x2, x3)
balance55c23_in_gaaaaaaaaaga(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12)  =  balance55c23_in_gaaaaaaaaaga(x1, x11)
nil  =  nil
balance55c23_out_gaaaaaaaaaga(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12)  =  balance55c23_out_gaaaaaaaaaga(x1, x11)
U13_gaaaaaaaaaga(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21)  =  U13_gaaaaaaaaaga(x1, x2, x3, x19, x21)
U14_gaaaaaaaaaga(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22, x23, x24, x25, x26)  =  U14_gaaaaaaaaaga(x1, x2, x3, x19, x26)
balance55c12_in_gaaaaaaaaaaaaga(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15)  =  balance55c12_in_gaaaaaaaaaaaaga(x1, x14)
balance55c12_out_gaaaaaaaaaaaaga(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15)  =  balance55c12_out_gaaaaaaaaaaaaga(x1, x14)
U17_gaaaaaaaaaaaaga(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21)  =  U17_gaaaaaaaaaaaaga(x1, x2, x3, x19, x21)
U18_gaaaaaaaaaaaaga(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22, x23, x24, x25, x26)  =  U18_gaaaaaaaaaaaaga(x1, x2, x3, x19, x26)
BALANCE5523_IN_GAAAAAAAAAGA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12)  =  BALANCE5523_IN_GAAAAAAAAAGA(x1, x11)
U2_GAAAAAAAAAGA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21)  =  U2_GAAAAAAAAAGA(x1, x2, x3, x19, x21)

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

(8) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(9) Obligation:

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

BALANCE5523_IN_GAAAAAAAAAGA(tree(T306, T307, T308), T321, T322, X528, X529, X530, X531, .(','(tree(T311, T312, T313), -(T314, T315)), T323), .(','(T311, -(T314, .(T312, T317))), .(','(T313, -(T317, T315)), T324)), T325, T320, X532) → U2_GAAAAAAAAAGA(T306, T307, T308, T321, T322, X528, X529, X530, X531, T311, T312, T313, T314, T315, T323, T317, T324, T325, T320, X532, balance55c23_in_gaaaaaaaaaga(T306, T321, T322, T344, T345, T346, T347, T323, T324, T325, T307, T348))
U2_GAAAAAAAAAGA(T306, T307, T308, T321, T322, X528, X529, X530, X531, T311, T312, T313, T314, T315, T323, T317, T324, T325, T320, X532, balance55c23_out_gaaaaaaaaaga(T306, T321, T322, T344, T345, T346, T347, T323, T324, T325, T307, T348)) → BALANCE5523_IN_GAAAAAAAAAGA(T308, T344, T345, X528, X529, X530, X531, T346, T347, T348, T320, X532)
BALANCE5523_IN_GAAAAAAAAAGA(tree(T306, T307, T308), T321, T322, X528, X529, X530, X531, .(','(tree(T311, T312, T313), -(T314, T315)), T323), .(','(T311, -(T314, .(T312, T317))), .(','(T313, -(T317, T315)), T324)), T325, T320, X532) → BALANCE5523_IN_GAAAAAAAAAGA(T306, T321, T322, X523, X524, X525, X526, T323, T324, T325, T307, X527)

The TRS R consists of the following rules:

balance55c23_in_gaaaaaaaaaga(nil, T267, .(','(nil, -(T269, T269)), T270), T269, T270, T271, T272, T271, T272, .(T274, T275), T274, T275) → balance55c23_out_gaaaaaaaaaga(nil, T267, .(','(nil, -(T269, T269)), T270), T269, T270, T271, T272, T271, T272, .(T274, T275), T274, T275)
balance55c23_in_gaaaaaaaaaga(tree(T306, T307, T308), T321, T322, X528, X529, X530, X531, .(','(tree(T311, T312, T313), -(T314, T315)), T323), .(','(T311, -(T314, .(T312, T317))), .(','(T313, -(T317, T315)), T324)), T325, T320, X532) → U13_gaaaaaaaaaga(T306, T307, T308, T321, T322, X528, X529, X530, X531, T311, T312, T313, T314, T315, T323, T317, T324, T325, T320, X532, balance55c23_in_gaaaaaaaaaga(T306, T321, T322, T344, T345, T346, T347, T323, T324, T325, T307, T348))
U13_gaaaaaaaaaga(T306, T307, T308, T321, T322, X528, X529, X530, X531, T311, T312, T313, T314, T315, T323, T317, T324, T325, T320, X532, balance55c23_out_gaaaaaaaaaga(T306, T321, T322, T344, T345, T346, T347, T323, T324, T325, T307, T348)) → U14_gaaaaaaaaaga(T306, T307, T308, T321, T322, X528, X529, X530, X531, T311, T312, T313, T314, T315, T323, T317, T324, T325, T320, X532, T344, T345, T346, T347, T348, balance55c23_in_gaaaaaaaaaga(T308, T344, T345, X528, X529, X530, X531, T346, T347, T348, T320, X532))
U14_gaaaaaaaaaga(T306, T307, T308, T321, T322, X528, X529, X530, X531, T311, T312, T313, T314, T315, T323, T317, T324, T325, T320, X532, T344, T345, T346, T347, T348, balance55c23_out_gaaaaaaaaaga(T308, T344, T345, X528, X529, X530, X531, T346, T347, T348, T320, X532)) → balance55c23_out_gaaaaaaaaaga(tree(T306, T307, T308), T321, T322, X528, X529, X530, X531, .(','(tree(T311, T312, T313), -(T314, T315)), T323), .(','(T311, -(T314, .(T312, T317))), .(','(T313, -(T317, T315)), T324)), T325, T320, X532)

The argument filtering Pi contains the following mapping:
tree(x1, x2, x3)  =  tree(x1, x2, x3)
balance55c23_in_gaaaaaaaaaga(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12)  =  balance55c23_in_gaaaaaaaaaga(x1, x11)
nil  =  nil
balance55c23_out_gaaaaaaaaaga(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12)  =  balance55c23_out_gaaaaaaaaaga(x1, x11)
U13_gaaaaaaaaaga(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21)  =  U13_gaaaaaaaaaga(x1, x2, x3, x19, x21)
U14_gaaaaaaaaaga(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22, x23, x24, x25, x26)  =  U14_gaaaaaaaaaga(x1, x2, x3, x19, x26)
BALANCE5523_IN_GAAAAAAAAAGA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12)  =  BALANCE5523_IN_GAAAAAAAAAGA(x1, x11)
U2_GAAAAAAAAAGA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21)  =  U2_GAAAAAAAAAGA(x1, x2, x3, x19, x21)

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

(10) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(11) Obligation:

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

BALANCE5523_IN_GAAAAAAAAAGA(tree(T306, T307, T308), T320) → U2_GAAAAAAAAAGA(T306, T307, T308, T320, balance55c23_in_gaaaaaaaaaga(T306, T307))
U2_GAAAAAAAAAGA(T306, T307, T308, T320, balance55c23_out_gaaaaaaaaaga(T306, T307)) → BALANCE5523_IN_GAAAAAAAAAGA(T308, T320)
BALANCE5523_IN_GAAAAAAAAAGA(tree(T306, T307, T308), T320) → BALANCE5523_IN_GAAAAAAAAAGA(T306, T307)

The TRS R consists of the following rules:

balance55c23_in_gaaaaaaaaaga(nil, T274) → balance55c23_out_gaaaaaaaaaga(nil, T274)
balance55c23_in_gaaaaaaaaaga(tree(T306, T307, T308), T320) → U13_gaaaaaaaaaga(T306, T307, T308, T320, balance55c23_in_gaaaaaaaaaga(T306, T307))
U13_gaaaaaaaaaga(T306, T307, T308, T320, balance55c23_out_gaaaaaaaaaga(T306, T307)) → U14_gaaaaaaaaaga(T306, T307, T308, T320, balance55c23_in_gaaaaaaaaaga(T308, T320))
U14_gaaaaaaaaaga(T306, T307, T308, T320, balance55c23_out_gaaaaaaaaaga(T308, T320)) → balance55c23_out_gaaaaaaaaaga(tree(T306, T307, T308), T320)

The set Q consists of the following terms:

balance55c23_in_gaaaaaaaaaga(x0, x1)
U13_gaaaaaaaaaga(x0, x1, x2, x3, x4)
U14_gaaaaaaaaaga(x0, x1, x2, x3, x4)

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

(12) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] 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:

  • U2_GAAAAAAAAAGA(T306, T307, T308, T320, balance55c23_out_gaaaaaaaaaga(T306, T307)) → BALANCE5523_IN_GAAAAAAAAAGA(T308, T320)
    The graph contains the following edges 3 >= 1, 4 >= 2

  • BALANCE5523_IN_GAAAAAAAAAGA(tree(T306, T307, T308), T320) → BALANCE5523_IN_GAAAAAAAAAGA(T306, T307)
    The graph contains the following edges 1 > 1, 1 > 2

  • BALANCE5523_IN_GAAAAAAAAAGA(tree(T306, T307, T308), T320) → U2_GAAAAAAAAAGA(T306, T307, T308, T320, balance55c23_in_gaaaaaaaaaga(T306, T307))
    The graph contains the following edges 1 > 1, 1 > 2, 1 > 3, 2 >= 4

(13) YES

(14) Obligation:

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

BALANCE5513_IN_GAAAAAAA(tree(T452, T453, T454), T468, T469, T498, T499, .(','(tree(T459, T460, T461), -(T462, T463)), T470), .(','(T459, -(T462, .(T460, T465))), .(','(T461, -(T465, T463)), T471)), T472) → U5_GAAAAAAA(T452, T453, T454, T468, T469, T498, T499, T459, T460, T461, T462, T463, T470, T465, T471, T472, balance55c23_in_gaaaaaaaaaga(T452, T468, T469, T493, T494, T495, T496, T470, T471, T472, T453, T497))
U5_GAAAAAAA(T452, T453, T454, T468, T469, T498, T499, T459, T460, T461, T462, T463, T470, T465, T471, T472, balance55c23_out_gaaaaaaaaaga(T452, T468, T469, T493, T494, T495, T496, T470, T471, T472, T453, T497)) → BALANCE5513_IN_GAAAAAAA(T454, T493, T494, T498, T499, T495, T496, T497)

The TRS R consists of the following rules:

balance55c23_in_gaaaaaaaaaga(nil, T267, .(','(nil, -(T269, T269)), T270), T269, T270, T271, T272, T271, T272, .(T274, T275), T274, T275) → balance55c23_out_gaaaaaaaaaga(nil, T267, .(','(nil, -(T269, T269)), T270), T269, T270, T271, T272, T271, T272, .(T274, T275), T274, T275)
balance55c23_in_gaaaaaaaaaga(tree(T306, T307, T308), T321, T322, X528, X529, X530, X531, .(','(tree(T311, T312, T313), -(T314, T315)), T323), .(','(T311, -(T314, .(T312, T317))), .(','(T313, -(T317, T315)), T324)), T325, T320, X532) → U13_gaaaaaaaaaga(T306, T307, T308, T321, T322, X528, X529, X530, X531, T311, T312, T313, T314, T315, T323, T317, T324, T325, T320, X532, balance55c23_in_gaaaaaaaaaga(T306, T321, T322, T344, T345, T346, T347, T323, T324, T325, T307, T348))
U13_gaaaaaaaaaga(T306, T307, T308, T321, T322, X528, X529, X530, X531, T311, T312, T313, T314, T315, T323, T317, T324, T325, T320, X532, balance55c23_out_gaaaaaaaaaga(T306, T321, T322, T344, T345, T346, T347, T323, T324, T325, T307, T348)) → U14_gaaaaaaaaaga(T306, T307, T308, T321, T322, X528, X529, X530, X531, T311, T312, T313, T314, T315, T323, T317, T324, T325, T320, X532, T344, T345, T346, T347, T348, balance55c23_in_gaaaaaaaaaga(T308, T344, T345, X528, X529, X530, X531, T346, T347, T348, T320, X532))
U14_gaaaaaaaaaga(T306, T307, T308, T321, T322, X528, X529, X530, X531, T311, T312, T313, T314, T315, T323, T317, T324, T325, T320, X532, T344, T345, T346, T347, T348, balance55c23_out_gaaaaaaaaaga(T308, T344, T345, X528, X529, X530, X531, T346, T347, T348, T320, X532)) → balance55c23_out_gaaaaaaaaaga(tree(T306, T307, T308), T321, T322, X528, X529, X530, X531, .(','(tree(T311, T312, T313), -(T314, T315)), T323), .(','(T311, -(T314, .(T312, T317))), .(','(T313, -(T317, T315)), T324)), T325, T320, X532)
balance55c12_in_gaaaaaaaaaaaaga(nil, X242, .(','(nil, -(X244, X244)), X245), X244, X245, .(','(T103, -(.(T109, T110), .(T105, T106))), .(','(T107, -(T106, [])), T108)), T108, T103, .(T109, T110), T105, T106, T107, T108, T109, T110) → balance55c12_out_gaaaaaaaaaaaaga(nil, X242, .(','(nil, -(X244, X244)), X245), X244, X245, .(','(T103, -(.(T109, T110), .(T105, T106))), .(','(T107, -(T106, [])), T108)), T108, T103, .(T109, T110), T105, T106, T107, T108, T109, T110)
balance55c12_in_gaaaaaaaaaaaaga(tree(T139, T140, T141), T184, T185, X333, X334, X335, X336, tree(T157, T158, T160), T154, T161, T156, T155, .(','(T157, -(T154, .(T158, T159))), .(','(T160, -(T159, .(T161, T156))), T153)), T152, X337) → U17_gaaaaaaaaaaaaga(T139, T140, T141, T184, T185, X333, X334, X335, X336, T157, T158, T160, T154, T161, T156, T155, T159, T153, T152, X337, balance55c23_in_gaaaaaaaaaga(T139, T184, T185, T186, T187, T188, T189, .(','(T155, -(T156, [])), .(','(T157, -(T154, .(T158, T159))), .(','(T160, -(T159, .(T161, T156))), T153))), T153, T154, T140, T190))
U17_gaaaaaaaaaaaaga(T139, T140, T141, T184, T185, X333, X334, X335, X336, T157, T158, T160, T154, T161, T156, T155, T159, T153, T152, X337, balance55c23_out_gaaaaaaaaaga(T139, T184, T185, T186, T187, T188, T189, .(','(T155, -(T156, [])), .(','(T157, -(T154, .(T158, T159))), .(','(T160, -(T159, .(T161, T156))), T153))), T153, T154, T140, T190)) → U18_gaaaaaaaaaaaaga(T139, T140, T141, T184, T185, X333, X334, X335, X336, T157, T158, T160, T154, T161, T156, T155, T159, T153, T152, X337, T186, T187, T188, T189, T190, balance55c23_in_gaaaaaaaaaga(T141, T186, T187, X333, X334, X335, X336, T188, T189, T190, T152, X337))
U18_gaaaaaaaaaaaaga(T139, T140, T141, T184, T185, X333, X334, X335, X336, T157, T158, T160, T154, T161, T156, T155, T159, T153, T152, X337, T186, T187, T188, T189, T190, balance55c23_out_gaaaaaaaaaga(T141, T186, T187, X333, X334, X335, X336, T188, T189, T190, T152, X337)) → balance55c12_out_gaaaaaaaaaaaaga(tree(T139, T140, T141), T184, T185, X333, X334, X335, X336, tree(T157, T158, T160), T154, T161, T156, T155, .(','(T157, -(T154, .(T158, T159))), .(','(T160, -(T159, .(T161, T156))), T153)), T152, X337)

The argument filtering Pi contains the following mapping:
tree(x1, x2, x3)  =  tree(x1, x2, x3)
balance55c23_in_gaaaaaaaaaga(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12)  =  balance55c23_in_gaaaaaaaaaga(x1, x11)
nil  =  nil
balance55c23_out_gaaaaaaaaaga(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12)  =  balance55c23_out_gaaaaaaaaaga(x1, x11)
U13_gaaaaaaaaaga(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21)  =  U13_gaaaaaaaaaga(x1, x2, x3, x19, x21)
U14_gaaaaaaaaaga(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22, x23, x24, x25, x26)  =  U14_gaaaaaaaaaga(x1, x2, x3, x19, x26)
balance55c12_in_gaaaaaaaaaaaaga(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15)  =  balance55c12_in_gaaaaaaaaaaaaga(x1, x14)
balance55c12_out_gaaaaaaaaaaaaga(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15)  =  balance55c12_out_gaaaaaaaaaaaaga(x1, x14)
U17_gaaaaaaaaaaaaga(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21)  =  U17_gaaaaaaaaaaaaga(x1, x2, x3, x19, x21)
U18_gaaaaaaaaaaaaga(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22, x23, x24, x25, x26)  =  U18_gaaaaaaaaaaaaga(x1, x2, x3, x19, x26)
BALANCE5513_IN_GAAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8)  =  BALANCE5513_IN_GAAAAAAA(x1)
U5_GAAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17)  =  U5_GAAAAAAA(x1, x2, x3, x17)

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

(15) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(16) Obligation:

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

BALANCE5513_IN_GAAAAAAA(tree(T452, T453, T454), T468, T469, T498, T499, .(','(tree(T459, T460, T461), -(T462, T463)), T470), .(','(T459, -(T462, .(T460, T465))), .(','(T461, -(T465, T463)), T471)), T472) → U5_GAAAAAAA(T452, T453, T454, T468, T469, T498, T499, T459, T460, T461, T462, T463, T470, T465, T471, T472, balance55c23_in_gaaaaaaaaaga(T452, T468, T469, T493, T494, T495, T496, T470, T471, T472, T453, T497))
U5_GAAAAAAA(T452, T453, T454, T468, T469, T498, T499, T459, T460, T461, T462, T463, T470, T465, T471, T472, balance55c23_out_gaaaaaaaaaga(T452, T468, T469, T493, T494, T495, T496, T470, T471, T472, T453, T497)) → BALANCE5513_IN_GAAAAAAA(T454, T493, T494, T498, T499, T495, T496, T497)

The TRS R consists of the following rules:

balance55c23_in_gaaaaaaaaaga(nil, T267, .(','(nil, -(T269, T269)), T270), T269, T270, T271, T272, T271, T272, .(T274, T275), T274, T275) → balance55c23_out_gaaaaaaaaaga(nil, T267, .(','(nil, -(T269, T269)), T270), T269, T270, T271, T272, T271, T272, .(T274, T275), T274, T275)
balance55c23_in_gaaaaaaaaaga(tree(T306, T307, T308), T321, T322, X528, X529, X530, X531, .(','(tree(T311, T312, T313), -(T314, T315)), T323), .(','(T311, -(T314, .(T312, T317))), .(','(T313, -(T317, T315)), T324)), T325, T320, X532) → U13_gaaaaaaaaaga(T306, T307, T308, T321, T322, X528, X529, X530, X531, T311, T312, T313, T314, T315, T323, T317, T324, T325, T320, X532, balance55c23_in_gaaaaaaaaaga(T306, T321, T322, T344, T345, T346, T347, T323, T324, T325, T307, T348))
U13_gaaaaaaaaaga(T306, T307, T308, T321, T322, X528, X529, X530, X531, T311, T312, T313, T314, T315, T323, T317, T324, T325, T320, X532, balance55c23_out_gaaaaaaaaaga(T306, T321, T322, T344, T345, T346, T347, T323, T324, T325, T307, T348)) → U14_gaaaaaaaaaga(T306, T307, T308, T321, T322, X528, X529, X530, X531, T311, T312, T313, T314, T315, T323, T317, T324, T325, T320, X532, T344, T345, T346, T347, T348, balance55c23_in_gaaaaaaaaaga(T308, T344, T345, X528, X529, X530, X531, T346, T347, T348, T320, X532))
U14_gaaaaaaaaaga(T306, T307, T308, T321, T322, X528, X529, X530, X531, T311, T312, T313, T314, T315, T323, T317, T324, T325, T320, X532, T344, T345, T346, T347, T348, balance55c23_out_gaaaaaaaaaga(T308, T344, T345, X528, X529, X530, X531, T346, T347, T348, T320, X532)) → balance55c23_out_gaaaaaaaaaga(tree(T306, T307, T308), T321, T322, X528, X529, X530, X531, .(','(tree(T311, T312, T313), -(T314, T315)), T323), .(','(T311, -(T314, .(T312, T317))), .(','(T313, -(T317, T315)), T324)), T325, T320, X532)

The argument filtering Pi contains the following mapping:
tree(x1, x2, x3)  =  tree(x1, x2, x3)
balance55c23_in_gaaaaaaaaaga(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12)  =  balance55c23_in_gaaaaaaaaaga(x1, x11)
nil  =  nil
balance55c23_out_gaaaaaaaaaga(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12)  =  balance55c23_out_gaaaaaaaaaga(x1, x11)
U13_gaaaaaaaaaga(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21)  =  U13_gaaaaaaaaaga(x1, x2, x3, x19, x21)
U14_gaaaaaaaaaga(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22, x23, x24, x25, x26)  =  U14_gaaaaaaaaaga(x1, x2, x3, x19, x26)
BALANCE5513_IN_GAAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8)  =  BALANCE5513_IN_GAAAAAAA(x1)
U5_GAAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17)  =  U5_GAAAAAAA(x1, x2, x3, x17)

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

(17) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(18) Obligation:

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

BALANCE5513_IN_GAAAAAAA(tree(T452, T453, T454)) → U5_GAAAAAAA(T452, T453, T454, balance55c23_in_gaaaaaaaaaga(T452, T453))
U5_GAAAAAAA(T452, T453, T454, balance55c23_out_gaaaaaaaaaga(T452, T453)) → BALANCE5513_IN_GAAAAAAA(T454)

The TRS R consists of the following rules:

balance55c23_in_gaaaaaaaaaga(nil, T274) → balance55c23_out_gaaaaaaaaaga(nil, T274)
balance55c23_in_gaaaaaaaaaga(tree(T306, T307, T308), T320) → U13_gaaaaaaaaaga(T306, T307, T308, T320, balance55c23_in_gaaaaaaaaaga(T306, T307))
U13_gaaaaaaaaaga(T306, T307, T308, T320, balance55c23_out_gaaaaaaaaaga(T306, T307)) → U14_gaaaaaaaaaga(T306, T307, T308, T320, balance55c23_in_gaaaaaaaaaga(T308, T320))
U14_gaaaaaaaaaga(T306, T307, T308, T320, balance55c23_out_gaaaaaaaaaga(T308, T320)) → balance55c23_out_gaaaaaaaaaga(tree(T306, T307, T308), T320)

The set Q consists of the following terms:

balance55c23_in_gaaaaaaaaaga(x0, x1)
U13_gaaaaaaaaaga(x0, x1, x2, x3, x4)
U14_gaaaaaaaaaga(x0, x1, x2, x3, x4)

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

(19) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] 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:

  • U5_GAAAAAAA(T452, T453, T454, balance55c23_out_gaaaaaaaaaga(T452, T453)) → BALANCE5513_IN_GAAAAAAA(T454)
    The graph contains the following edges 3 >= 1

  • BALANCE5513_IN_GAAAAAAA(tree(T452, T453, T454)) → U5_GAAAAAAA(T452, T453, T454, balance55c23_in_gaaaaaaaaaga(T452, T453))
    The graph contains the following edges 1 > 1, 1 > 2, 1 > 3

(20) YES