Left Termination proof of /tmp/tmpIz85BG/untupled_bal

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 PrologToPrologProblemTransformerProof (⇐)

↳2 Prolog

↳3 PrologToPiTRSProof (⇐)

↳4 PiTRS

↳5 DependencyPairsProof (⇔)

↳6 PiDP

↳7 DependencyGraphProof (⇔)

↳8 AND

    ↳9 PiDP

        ↳10 UsableRulesProof (⇔)

        ↳11 PiDP

        ↳12 PiDPToQDPProof (⇐)

        ↳13 QDP

        ↳14 QDPSizeChangeProof (⇔)

        ↳15 YES

    ↳16 PiDP

        ↳17 UsableRulesProof (⇔)

        ↳18 PiDP

        ↳19 PiDPToQDPProof (⇐)

        ↳20 QDP

        ↳21 QDPSizeChangeProof (⇔)

        ↳22 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) PrologToPrologProblemTransformerProof (SOUND transformation)

Built Prolog problem from termination graph.

(2) Obligation:

Clauses:

balance5523(nil, T267, .(','(nil, -(T269, T269)), T270), T269, T270, T271, T272, T271, T272, .(T274, T275), T274, T275).
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) :- ','(balance5523(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(nil, T415, [], T417, T418, .(','(nil, -(T417, T417)), T418), [], []).
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) :- ','(balance5523(T452, T468, T469, T493, T494, T495, T496, T470, T471, T472, T453, T497), balance5513(T454, T493, T494, T498, T499, T495, T496, T497)).
balance5512(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).
balance5512(tree(T139, T140, T141), X331, X332, X333, X334, X335, X336, tree(T157, T158, T160), T154, T161, T156, T155, .(','(T157, -(T154, .(T158, T159))), .(','(T160, -(T159, .(T161, T156))), T153)), T152, X337) :- balance5523(T139, X331, X332, X326, X327, X328, X329, .(','(T155, -(T156, [])), .(','(T157, -(T154, .(T158, T159))), .(','(T160, -(T159, .(T161, T156))), T153))), T153, T154, T140, X330).
balance5512(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) :- ','(balance5523(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(nil, nil).
balance1(tree(T20, T21, T22), tree(T28, T29, T31)) :- balance5512(T20, X125, X126, X120, X121, X122, X123, T28, T27, T29, T30, T31, T26, T21, X124).
balance1(tree(T20, T21, T22), tree(T28, T29, T31)) :- ','(balance5512(T20, T48, T49, T50, T51, T52, T53, T28, T27, T29, T30, T31, T26, T21, T54), balance5513(T22, T50, T51, T48, T49, T52, T53, T54)).

Queries:

balance1(g,a).

(3) PrologToPiTRSProof (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)
balance5512_in: (b,f,f,f,f,f,f,f,f,f,f,f,f,b,f)
balance5523_in: (b,f,f,f,f,f,f,f,f,f,b,f)
balance5513_in: (b,f,f,f,f,f,f,f)
Transforming Prolog into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:

balance1_in_ga(nil, nil) → balance1_out_ga(nil, nil)
balance1_in_ga(tree(T20, T21, T22), tree(T28, T29, T31)) → U10_ga(T20, T21, T22, T28, T29, T31, balance5512_in_gaaaaaaaaaaaaga(T20, X125, X126, X120, X121, X122, X123, T28, T27, T29, T30, T31, T26, T21, X124))
balance5512_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) → balance5512_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)
balance5512_in_gaaaaaaaaaaaaga(tree(T139, T140, T141), X331, X332, X333, X334, X335, X336, tree(T157, T158, T160), T154, T161, T156, T155, .(','(T157, -(T154, .(T158, T159))), .(','(T160, -(T159, .(T161, T156))), T153)), T152, X337) → U7_gaaaaaaaaaaaaga(T139, T140, T141, X331, X332, X333, X334, X335, X336, T157, T158, T160, T154, T161, T156, T155, T159, T153, T152, X337, 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(nil, T267, .(','(nil, -(T269, T269)), T270), T269, T270, T271, T272, T271, T272, .(T274, T275), T274, T275) → balance5523_out_gaaaaaaaaaga(nil, T267, .(','(nil, -(T269, T269)), T270), T269, T270, T271, T272, T271, T272, .(T274, T275), T274, T275)
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) → U2_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, 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, balance5523_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))
U3_gaaaaaaaaaga(T306, T307, T308, T321, T322, X528, X529, X530, X531, T311, T312, T313, T314, T315, T323, T317, T324, T325, T320, X532, balance5523_out_gaaaaaaaaaga(T308, T344, T345, X528, X529, X530, X531, T346, T347, T348, T320, X532)) → balance5523_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)
U1_gaaaaaaaaaga(T306, T307, T308, T321, T322, X528, X529, X530, X531, T311, T312, T313, T314, T315, T323, T317, T324, T325, T320, X532, balance5523_out_gaaaaaaaaaga(T306, T321, T322, X523, X524, X525, X526, T323, T324, T325, T307, X527)) → balance5523_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)
U7_gaaaaaaaaaaaaga(T139, T140, T141, X331, X332, X333, X334, X335, X336, T157, T158, T160, T154, T161, T156, T155, T159, T153, T152, X337, balance5523_out_gaaaaaaaaaga(T139, X331, X332, X326, X327, X328, X329, .(','(T155, -(T156, [])), .(','(T157, -(T154, .(T158, T159))), .(','(T160, -(T159, .(T161, T156))), T153))), T153, T154, T140, X330)) → balance5512_out_gaaaaaaaaaaaaga(tree(T139, T140, T141), X331, X332, X333, X334, X335, X336, tree(T157, T158, T160), T154, T161, T156, T155, .(','(T157, -(T154, .(T158, T159))), .(','(T160, -(T159, .(T161, T156))), T153)), T152, X337)
balance5512_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) → U8_gaaaaaaaaaaaaga(T139, T140, T141, T184, T185, X333, X334, X335, X336, T157, T158, T160, T154, T161, T156, T155, T159, T153, T152, X337, balance5523_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_gaaaaaaaaaaaaga(T139, T140, T141, T184, T185, X333, X334, X335, X336, T157, T158, T160, T154, T161, T156, T155, T159, T153, T152, X337, balance5523_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_gaaaaaaaaaaaaga(T139, T140, T141, T184, T185, X333, X334, X335, X336, T157, T158, T160, T154, T161, T156, T155, T159, T153, T152, X337, balance5523_in_gaaaaaaaaaga(T141, T186, T187, X333, X334, X335, X336, T188, T189, T190, T152, X337))
U9_gaaaaaaaaaaaaga(T139, T140, T141, T184, T185, X333, X334, X335, X336, T157, T158, T160, T154, T161, T156, T155, T159, T153, T152, X337, balance5523_out_gaaaaaaaaaga(T141, T186, T187, X333, X334, X335, X336, T188, T189, T190, T152, X337)) → balance5512_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)
U10_ga(T20, T21, T22, T28, T29, T31, balance5512_out_gaaaaaaaaaaaaga(T20, X125, X126, X120, X121, X122, X123, T28, T27, T29, T30, T31, T26, T21, X124)) → balance1_out_ga(tree(T20, T21, T22), tree(T28, T29, T31))
balance1_in_ga(tree(T20, T21, T22), tree(T28, T29, T31)) → U11_ga(T20, T21, T22, T28, T29, T31, balance5512_in_gaaaaaaaaaaaaga(T20, T48, T49, T50, T51, T52, T53, T28, T27, T29, T30, T31, T26, T21, T54))
U11_ga(T20, T21, T22, T28, T29, T31, balance5512_out_gaaaaaaaaaaaaga(T20, T48, T49, T50, T51, T52, T53, T28, T27, T29, T30, T31, T26, T21, T54)) → U12_ga(T20, T21, T22, T28, T29, T31, balance5513_in_gaaaaaaa(T22, T50, T51, T48, T49, T52, T53, T54))
balance5513_in_gaaaaaaa(nil, T415, [], T417, T418, .(','(nil, -(T417, T417)), T418), [], []) → balance5513_out_gaaaaaaa(nil, T415, [], T417, T418, .(','(nil, -(T417, T417)), T418), [], [])
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))
U4_gaaaaaaa(T452, T453, T454, T468, T469, T474, T473, T459, T460, T461, T462, T463, T470, T465, T471, T472, balance5523_out_gaaaaaaaaaga(T452, T468, T469, X692, X693, X694, X695, T470, T471, T472, T453, X696)) → balance5513_out_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)
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, balance5523_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, balance5523_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))
U6_gaaaaaaa(T452, T453, T454, T468, T469, T498, T499, T459, T460, T461, T462, T463, T470, T465, T471, T472, balance5513_out_gaaaaaaa(T454, T493, T494, T498, T499, T495, T496, T497)) → balance5513_out_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)
U12_ga(T20, T21, T22, T28, T29, T31, balance5513_out_gaaaaaaa(T22, T50, T51, T48, T49, T52, T53, T54)) → balance1_out_ga(tree(T20, T21, T22), tree(T28, T29, T31))

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog

(4) Obligation:

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

balance1_in_ga(nil, nil) → balance1_out_ga(nil, nil)
balance1_in_ga(tree(T20, T21, T22), tree(T28, T29, T31)) → U10_ga(T20, T21, T22, T28, T29, T31, balance5512_in_gaaaaaaaaaaaaga(T20, X125, X126, X120, X121, X122, X123, T28, T27, T29, T30, T31, T26, T21, X124))
balance5512_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) → balance5512_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)
balance5512_in_gaaaaaaaaaaaaga(tree(T139, T140, T141), X331, X332, X333, X334, X335, X336, tree(T157, T158, T160), T154, T161, T156, T155, .(','(T157, -(T154, .(T158, T159))), .(','(T160, -(T159, .(T161, T156))), T153)), T152, X337) → U7_gaaaaaaaaaaaaga(T139, T140, T141, X331, X332, X333, X334, X335, X336, T157, T158, T160, T154, T161, T156, T155, T159, T153, T152, X337, 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(nil, T267, .(','(nil, -(T269, T269)), T270), T269, T270, T271, T272, T271, T272, .(T274, T275), T274, T275) → balance5523_out_gaaaaaaaaaga(nil, T267, .(','(nil, -(T269, T269)), T270), T269, T270, T271, T272, T271, T272, .(T274, T275), T274, T275)
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) → U2_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, 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, balance5523_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))
U3_gaaaaaaaaaga(T306, T307, T308, T321, T322, X528, X529, X530, X531, T311, T312, T313, T314, T315, T323, T317, T324, T325, T320, X532, balance5523_out_gaaaaaaaaaga(T308, T344, T345, X528, X529, X530, X531, T346, T347, T348, T320, X532)) → balance5523_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)
U1_gaaaaaaaaaga(T306, T307, T308, T321, T322, X528, X529, X530, X531, T311, T312, T313, T314, T315, T323, T317, T324, T325, T320, X532, balance5523_out_gaaaaaaaaaga(T306, T321, T322, X523, X524, X525, X526, T323, T324, T325, T307, X527)) → balance5523_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)
U7_gaaaaaaaaaaaaga(T139, T140, T141, X331, X332, X333, X334, X335, X336, T157, T158, T160, T154, T161, T156, T155, T159, T153, T152, X337, balance5523_out_gaaaaaaaaaga(T139, X331, X332, X326, X327, X328, X329, .(','(T155, -(T156, [])), .(','(T157, -(T154, .(T158, T159))), .(','(T160, -(T159, .(T161, T156))), T153))), T153, T154, T140, X330)) → balance5512_out_gaaaaaaaaaaaaga(tree(T139, T140, T141), X331, X332, X333, X334, X335, X336, tree(T157, T158, T160), T154, T161, T156, T155, .(','(T157, -(T154, .(T158, T159))), .(','(T160, -(T159, .(T161, T156))), T153)), T152, X337)
balance5512_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) → U8_gaaaaaaaaaaaaga(T139, T140, T141, T184, T185, X333, X334, X335, X336, T157, T158, T160, T154, T161, T156, T155, T159, T153, T152, X337, balance5523_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_gaaaaaaaaaaaaga(T139, T140, T141, T184, T185, X333, X334, X335, X336, T157, T158, T160, T154, T161, T156, T155, T159, T153, T152, X337, balance5523_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_gaaaaaaaaaaaaga(T139, T140, T141, T184, T185, X333, X334, X335, X336, T157, T158, T160, T154, T161, T156, T155, T159, T153, T152, X337, balance5523_in_gaaaaaaaaaga(T141, T186, T187, X333, X334, X335, X336, T188, T189, T190, T152, X337))
U9_gaaaaaaaaaaaaga(T139, T140, T141, T184, T185, X333, X334, X335, X336, T157, T158, T160, T154, T161, T156, T155, T159, T153, T152, X337, balance5523_out_gaaaaaaaaaga(T141, T186, T187, X333, X334, X335, X336, T188, T189, T190, T152, X337)) → balance5512_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)
U10_ga(T20, T21, T22, T28, T29, T31, balance5512_out_gaaaaaaaaaaaaga(T20, X125, X126, X120, X121, X122, X123, T28, T27, T29, T30, T31, T26, T21, X124)) → balance1_out_ga(tree(T20, T21, T22), tree(T28, T29, T31))
balance1_in_ga(tree(T20, T21, T22), tree(T28, T29, T31)) → U11_ga(T20, T21, T22, T28, T29, T31, balance5512_in_gaaaaaaaaaaaaga(T20, T48, T49, T50, T51, T52, T53, T28, T27, T29, T30, T31, T26, T21, T54))
U11_ga(T20, T21, T22, T28, T29, T31, balance5512_out_gaaaaaaaaaaaaga(T20, T48, T49, T50, T51, T52, T53, T28, T27, T29, T30, T31, T26, T21, T54)) → U12_ga(T20, T21, T22, T28, T29, T31, balance5513_in_gaaaaaaa(T22, T50, T51, T48, T49, T52, T53, T54))
balance5513_in_gaaaaaaa(nil, T415, [], T417, T418, .(','(nil, -(T417, T417)), T418), [], []) → balance5513_out_gaaaaaaa(nil, T415, [], T417, T418, .(','(nil, -(T417, T417)), T418), [], [])
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))
U4_gaaaaaaa(T452, T453, T454, T468, T469, T474, T473, T459, T460, T461, T462, T463, T470, T465, T471, T472, balance5523_out_gaaaaaaaaaga(T452, T468, T469, X692, X693, X694, X695, T470, T471, T472, T453, X696)) → balance5513_out_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)
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, balance5523_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, balance5523_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))
U6_gaaaaaaa(T452, T453, T454, T468, T469, T498, T499, T459, T460, T461, T462, T463, T470, T465, T471, T472, balance5513_out_gaaaaaaa(T454, T493, T494, T498, T499, T495, T496, T497)) → balance5513_out_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)
U12_ga(T20, T21, T22, T28, T29, T31, balance5513_out_gaaaaaaa(T22, T50, T51, T48, T49, T52, T53, T54)) → balance1_out_ga(tree(T20, T21, T22), tree(T28, T29, T31))

(5) DependencyPairsProof (EQUIVALENT transformation)

Using Dependency Pairs [AG00,LOPSTR] we result in the following initial DP problem:
Pi DP problem:
The TRS P consists of the following rules:

BALANCE1_IN_GA(tree(T20, T21, T22), tree(T28, T29, T31)) → U10_GA(T20, T21, T22, T28, T29, T31, balance5512_in_gaaaaaaaaaaaaga(T20, X125, X126, X120, X121, X122, X123, T28, T27, T29, T30, T31, T26, T21, X124))
BALANCE1_IN_GA(tree(T20, T21, T22), tree(T28, T29, T31)) → BALANCE5512_IN_GAAAAAAAAAAAAGA(T20, X125, X126, X120, X121, X122, X123, T28, T27, T29, T30, T31, T26, T21, X124)
BALANCE5512_IN_GAAAAAAAAAAAAGA(tree(T139, T140, T141), X331, X332, X333, X334, X335, X336, tree(T157, T158, T160), T154, T161, T156, T155, .(','(T157, -(T154, .(T158, T159))), .(','(T160, -(T159, .(T161, T156))), T153)), T152, X337) → U7_GAAAAAAAAAAAAGA(T139, T140, T141, X331, X332, X333, X334, X335, X336, T157, T158, T160, T154, T161, T156, T155, T159, T153, T152, X337, 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))
BALANCE5512_IN_GAAAAAAAAAAAAGA(tree(T139, T140, T141), X331, X332, X333, X334, X335, X336, tree(T157, T158, T160), T154, T161, T156, T155, .(','(T157, -(T154, .(T158, T159))), .(','(T160, -(T159, .(T161, T156))), T153)), T152, X337) → 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, balance5523_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, balance5523_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, balance5523_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)
BALANCE5512_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) → U8_GAAAAAAAAAAAAGA(T139, T140, T141, T184, T185, X333, X334, X335, X336, T157, T158, T160, T154, T161, T156, T155, T159, T153, T152, X337, balance5523_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_GAAAAAAAAAAAAGA(T139, T140, T141, T184, T185, X333, X334, X335, X336, T157, T158, T160, T154, T161, T156, T155, T159, T153, T152, X337, balance5523_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_GAAAAAAAAAAAAGA(T139, T140, T141, T184, T185, X333, X334, X335, X336, T157, T158, T160, T154, T161, T156, T155, T159, T153, T152, X337, balance5523_in_gaaaaaaaaaga(T141, T186, T187, X333, X334, X335, X336, T188, T189, T190, T152, X337))
U8_GAAAAAAAAAAAAGA(T139, T140, T141, T184, T185, X333, X334, X335, X336, T157, T158, T160, T154, T161, T156, T155, T159, T153, T152, X337, balance5523_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)) → U11_GA(T20, T21, T22, T28, T29, T31, balance5512_in_gaaaaaaaaaaaaga(T20, T48, T49, T50, T51, T52, T53, T28, T27, T29, T30, T31, T26, T21, T54))
U11_GA(T20, T21, T22, T28, T29, T31, balance5512_out_gaaaaaaaaaaaaga(T20, T48, T49, T50, T51, T52, T53, T28, T27, T29, T30, T31, T26, T21, T54)) → U12_GA(T20, T21, T22, T28, T29, T31, balance5513_in_gaaaaaaa(T22, T50, T51, T48, T49, T52, T53, T54))
U11_GA(T20, T21, T22, T28, T29, T31, balance5512_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, balance5523_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, balance5523_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, balance5523_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:

balance1_in_ga(nil, nil) → balance1_out_ga(nil, nil)
balance1_in_ga(tree(T20, T21, T22), tree(T28, T29, T31)) → U10_ga(T20, T21, T22, T28, T29, T31, balance5512_in_gaaaaaaaaaaaaga(T20, X125, X126, X120, X121, X122, X123, T28, T27, T29, T30, T31, T26, T21, X124))
balance5512_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) → balance5512_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)
balance5512_in_gaaaaaaaaaaaaga(tree(T139, T140, T141), X331, X332, X333, X334, X335, X336, tree(T157, T158, T160), T154, T161, T156, T155, .(','(T157, -(T154, .(T158, T159))), .(','(T160, -(T159, .(T161, T156))), T153)), T152, X337) → U7_gaaaaaaaaaaaaga(T139, T140, T141, X331, X332, X333, X334, X335, X336, T157, T158, T160, T154, T161, T156, T155, T159, T153, T152, X337, 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(nil, T267, .(','(nil, -(T269, T269)), T270), T269, T270, T271, T272, T271, T272, .(T274, T275), T274, T275) → balance5523_out_gaaaaaaaaaga(nil, T267, .(','(nil, -(T269, T269)), T270), T269, T270, T271, T272, T271, T272, .(T274, T275), T274, T275)
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) → U2_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, 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, balance5523_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))
U3_gaaaaaaaaaga(T306, T307, T308, T321, T322, X528, X529, X530, X531, T311, T312, T313, T314, T315, T323, T317, T324, T325, T320, X532, balance5523_out_gaaaaaaaaaga(T308, T344, T345, X528, X529, X530, X531, T346, T347, T348, T320, X532)) → balance5523_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)
U1_gaaaaaaaaaga(T306, T307, T308, T321, T322, X528, X529, X530, X531, T311, T312, T313, T314, T315, T323, T317, T324, T325, T320, X532, balance5523_out_gaaaaaaaaaga(T306, T321, T322, X523, X524, X525, X526, T323, T324, T325, T307, X527)) → balance5523_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)
U7_gaaaaaaaaaaaaga(T139, T140, T141, X331, X332, X333, X334, X335, X336, T157, T158, T160, T154, T161, T156, T155, T159, T153, T152, X337, balance5523_out_gaaaaaaaaaga(T139, X331, X332, X326, X327, X328, X329, .(','(T155, -(T156, [])), .(','(T157, -(T154, .(T158, T159))), .(','(T160, -(T159, .(T161, T156))), T153))), T153, T154, T140, X330)) → balance5512_out_gaaaaaaaaaaaaga(tree(T139, T140, T141), X331, X332, X333, X334, X335, X336, tree(T157, T158, T160), T154, T161, T156, T155, .(','(T157, -(T154, .(T158, T159))), .(','(T160, -(T159, .(T161, T156))), T153)), T152, X337)
balance5512_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) → U8_gaaaaaaaaaaaaga(T139, T140, T141, T184, T185, X333, X334, X335, X336, T157, T158, T160, T154, T161, T156, T155, T159, T153, T152, X337, balance5523_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_gaaaaaaaaaaaaga(T139, T140, T141, T184, T185, X333, X334, X335, X336, T157, T158, T160, T154, T161, T156, T155, T159, T153, T152, X337, balance5523_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_gaaaaaaaaaaaaga(T139, T140, T141, T184, T185, X333, X334, X335, X336, T157, T158, T160, T154, T161, T156, T155, T159, T153, T152, X337, balance5523_in_gaaaaaaaaaga(T141, T186, T187, X333, X334, X335, X336, T188, T189, T190, T152, X337))
U9_gaaaaaaaaaaaaga(T139, T140, T141, T184, T185, X333, X334, X335, X336, T157, T158, T160, T154, T161, T156, T155, T159, T153, T152, X337, balance5523_out_gaaaaaaaaaga(T141, T186, T187, X333, X334, X335, X336, T188, T189, T190, T152, X337)) → balance5512_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)
U10_ga(T20, T21, T22, T28, T29, T31, balance5512_out_gaaaaaaaaaaaaga(T20, X125, X126, X120, X121, X122, X123, T28, T27, T29, T30, T31, T26, T21, X124)) → balance1_out_ga(tree(T20, T21, T22), tree(T28, T29, T31))
balance1_in_ga(tree(T20, T21, T22), tree(T28, T29, T31)) → U11_ga(T20, T21, T22, T28, T29, T31, balance5512_in_gaaaaaaaaaaaaga(T20, T48, T49, T50, T51, T52, T53, T28, T27, T29, T30, T31, T26, T21, T54))
U11_ga(T20, T21, T22, T28, T29, T31, balance5512_out_gaaaaaaaaaaaaga(T20, T48, T49, T50, T51, T52, T53, T28, T27, T29, T30, T31, T26, T21, T54)) → U12_ga(T20, T21, T22, T28, T29, T31, balance5513_in_gaaaaaaa(T22, T50, T51, T48, T49, T52, T53, T54))
balance5513_in_gaaaaaaa(nil, T415, [], T417, T418, .(','(nil, -(T417, T417)), T418), [], []) → balance5513_out_gaaaaaaa(nil, T415, [], T417, T418, .(','(nil, -(T417, T417)), T418), [], [])
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))
U4_gaaaaaaa(T452, T453, T454, T468, T469, T474, T473, T459, T460, T461, T462, T463, T470, T465, T471, T472, balance5523_out_gaaaaaaaaaga(T452, T468, T469, X692, X693, X694, X695, T470, T471, T472, T453, X696)) → balance5513_out_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)
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, balance5523_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, balance5523_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))
U6_gaaaaaaa(T452, T453, T454, T468, T469, T498, T499, T459, T460, T461, T462, T463, T470, T465, T471, T472, balance5513_out_gaaaaaaa(T454, T493, T494, T498, T499, T495, T496, T497)) → balance5513_out_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)
U12_ga(T20, T21, T22, T28, T29, T31, balance5513_out_gaaaaaaa(T22, T50, T51, T48, T49, T52, T53, T54)) → balance1_out_ga(tree(T20, T21, T22), tree(T28, T29, T31))

The argument filtering Pi contains the following mapping:
balance1_in_ga(x1, x2) = balance1_in_ga(x1)
nil = nil
balance1_out_ga(x1, x2) = balance1_out_ga
tree(x1, x2, x3) = tree(x1, x2, x3)
U10_ga(x1, x2, x3, x4, x5, x6, x7) = U10_ga(x7)
balance5512_in_gaaaaaaaaaaaaga(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15) = balance5512_in_gaaaaaaaaaaaaga(x1, x14)
balance5512_out_gaaaaaaaaaaaaga(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15) = balance5512_out_gaaaaaaaaaaaaga
U7_gaaaaaaaaaaaaga(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21) = U7_gaaaaaaaaaaaaga(x21)
balance5523_in_gaaaaaaaaaga(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12) = balance5523_in_gaaaaaaaaaga(x1, x11)
balance5523_out_gaaaaaaaaaga(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12) = balance5523_out_gaaaaaaaaaga
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(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(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(x21)
U8_gaaaaaaaaaaaaga(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21) = U8_gaaaaaaaaaaaaga(x3, x19, x21)
U9_gaaaaaaaaaaaaga(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21) = U9_gaaaaaaaaaaaaga(x21)
U11_ga(x1, x2, x3, x4, x5, x6, x7) = U11_ga(x3, x7)
U12_ga(x1, x2, x3, x4, x5, x6, x7) = U12_ga(x7)
balance5513_in_gaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8) = balance5513_in_gaaaaaaa(x1)
balance5513_out_gaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8) = balance5513_out_gaaaaaaa
U4_gaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17) = U4_gaaaaaaa(x17)
U5_gaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17) = U5_gaaaaaaa(x3, x17)
U6_gaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17) = U6_gaaaaaaa(x17)
BALANCE1_IN_GA(x1, x2) = BALANCE1_IN_GA(x1)
U10_GA(x1, x2, x3, x4, x5, x6, x7) = U10_GA(x7)
BALANCE5512_IN_GAAAAAAAAAAAAGA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15) = BALANCE5512_IN_GAAAAAAAAAAAAGA(x1, x14)
U7_GAAAAAAAAAAAAGA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21) = U7_GAAAAAAAAAAAAGA(x21)
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(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(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(x21)
U8_GAAAAAAAAAAAAGA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21) = U8_GAAAAAAAAAAAAGA(x3, x19, x21)
U9_GAAAAAAAAAAAAGA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21) = U9_GAAAAAAAAAAAAGA(x21)
U11_GA(x1, x2, x3, x4, x5, x6, x7) = U11_GA(x3, x7)
U12_GA(x1, x2, x3, x4, x5, x6, x7) = U12_GA(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(x17)
U5_GAAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17) = U5_GAAAAAAA(x3, x17)
U6_GAAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17) = U6_GAAAAAAA(x17)

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

(6) Obligation:

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

BALANCE1_IN_GA(tree(T20, T21, T22), tree(T28, T29, T31)) → U10_GA(T20, T21, T22, T28, T29, T31, balance5512_in_gaaaaaaaaaaaaga(T20, X125, X126, X120, X121, X122, X123, T28, T27, T29, T30, T31, T26, T21, X124))
BALANCE1_IN_GA(tree(T20, T21, T22), tree(T28, T29, T31)) → BALANCE5512_IN_GAAAAAAAAAAAAGA(T20, X125, X126, X120, X121, X122, X123, T28, T27, T29, T30, T31, T26, T21, X124)
BALANCE5512_IN_GAAAAAAAAAAAAGA(tree(T139, T140, T141), X331, X332, X333, X334, X335, X336, tree(T157, T158, T160), T154, T161, T156, T155, .(','(T157, -(T154, .(T158, T159))), .(','(T160, -(T159, .(T161, T156))), T153)), T152, X337) → U7_GAAAAAAAAAAAAGA(T139, T140, T141, X331, X332, X333, X334, X335, X336, T157, T158, T160, T154, T161, T156, T155, T159, T153, T152, X337, 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))
BALANCE5512_IN_GAAAAAAAAAAAAGA(tree(T139, T140, T141), X331, X332, X333, X334, X335, X336, tree(T157, T158, T160), T154, T161, T156, T155, .(','(T157, -(T154, .(T158, T159))), .(','(T160, -(T159, .(T161, T156))), T153)), T152, X337) → 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, balance5523_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, balance5523_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, balance5523_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)
BALANCE5512_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) → U8_GAAAAAAAAAAAAGA(T139, T140, T141, T184, T185, X333, X334, X335, X336, T157, T158, T160, T154, T161, T156, T155, T159, T153, T152, X337, balance5523_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_GAAAAAAAAAAAAGA(T139, T140, T141, T184, T185, X333, X334, X335, X336, T157, T158, T160, T154, T161, T156, T155, T159, T153, T152, X337, balance5523_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_GAAAAAAAAAAAAGA(T139, T140, T141, T184, T185, X333, X334, X335, X336, T157, T158, T160, T154, T161, T156, T155, T159, T153, T152, X337, balance5523_in_gaaaaaaaaaga(T141, T186, T187, X333, X334, X335, X336, T188, T189, T190, T152, X337))
U8_GAAAAAAAAAAAAGA(T139, T140, T141, T184, T185, X333, X334, X335, X336, T157, T158, T160, T154, T161, T156, T155, T159, T153, T152, X337, balance5523_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)) → U11_GA(T20, T21, T22, T28, T29, T31, balance5512_in_gaaaaaaaaaaaaga(T20, T48, T49, T50, T51, T52, T53, T28, T27, T29, T30, T31, T26, T21, T54))
U11_GA(T20, T21, T22, T28, T29, T31, balance5512_out_gaaaaaaaaaaaaga(T20, T48, T49, T50, T51, T52, T53, T28, T27, T29, T30, T31, T26, T21, T54)) → U12_GA(T20, T21, T22, T28, T29, T31, balance5513_in_gaaaaaaa(T22, T50, T51, T48, T49, T52, T53, T54))
U11_GA(T20, T21, T22, T28, T29, T31, balance5512_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, balance5523_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, balance5523_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, balance5523_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:

balance1_in_ga(nil, nil) → balance1_out_ga(nil, nil)
balance1_in_ga(tree(T20, T21, T22), tree(T28, T29, T31)) → U10_ga(T20, T21, T22, T28, T29, T31, balance5512_in_gaaaaaaaaaaaaga(T20, X125, X126, X120, X121, X122, X123, T28, T27, T29, T30, T31, T26, T21, X124))
balance5512_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) → balance5512_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)
balance5512_in_gaaaaaaaaaaaaga(tree(T139, T140, T141), X331, X332, X333, X334, X335, X336, tree(T157, T158, T160), T154, T161, T156, T155, .(','(T157, -(T154, .(T158, T159))), .(','(T160, -(T159, .(T161, T156))), T153)), T152, X337) → U7_gaaaaaaaaaaaaga(T139, T140, T141, X331, X332, X333, X334, X335, X336, T157, T158, T160, T154, T161, T156, T155, T159, T153, T152, X337, 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(nil, T267, .(','(nil, -(T269, T269)), T270), T269, T270, T271, T272, T271, T272, .(T274, T275), T274, T275) → balance5523_out_gaaaaaaaaaga(nil, T267, .(','(nil, -(T269, T269)), T270), T269, T270, T271, T272, T271, T272, .(T274, T275), T274, T275)
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) → U2_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, 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, balance5523_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))
U3_gaaaaaaaaaga(T306, T307, T308, T321, T322, X528, X529, X530, X531, T311, T312, T313, T314, T315, T323, T317, T324, T325, T320, X532, balance5523_out_gaaaaaaaaaga(T308, T344, T345, X528, X529, X530, X531, T346, T347, T348, T320, X532)) → balance5523_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)
U1_gaaaaaaaaaga(T306, T307, T308, T321, T322, X528, X529, X530, X531, T311, T312, T313, T314, T315, T323, T317, T324, T325, T320, X532, balance5523_out_gaaaaaaaaaga(T306, T321, T322, X523, X524, X525, X526, T323, T324, T325, T307, X527)) → balance5523_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)
U7_gaaaaaaaaaaaaga(T139, T140, T141, X331, X332, X333, X334, X335, X336, T157, T158, T160, T154, T161, T156, T155, T159, T153, T152, X337, balance5523_out_gaaaaaaaaaga(T139, X331, X332, X326, X327, X328, X329, .(','(T155, -(T156, [])), .(','(T157, -(T154, .(T158, T159))), .(','(T160, -(T159, .(T161, T156))), T153))), T153, T154, T140, X330)) → balance5512_out_gaaaaaaaaaaaaga(tree(T139, T140, T141), X331, X332, X333, X334, X335, X336, tree(T157, T158, T160), T154, T161, T156, T155, .(','(T157, -(T154, .(T158, T159))), .(','(T160, -(T159, .(T161, T156))), T153)), T152, X337)
balance5512_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) → U8_gaaaaaaaaaaaaga(T139, T140, T141, T184, T185, X333, X334, X335, X336, T157, T158, T160, T154, T161, T156, T155, T159, T153, T152, X337, balance5523_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_gaaaaaaaaaaaaga(T139, T140, T141, T184, T185, X333, X334, X335, X336, T157, T158, T160, T154, T161, T156, T155, T159, T153, T152, X337, balance5523_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_gaaaaaaaaaaaaga(T139, T140, T141, T184, T185, X333, X334, X335, X336, T157, T158, T160, T154, T161, T156, T155, T159, T153, T152, X337, balance5523_in_gaaaaaaaaaga(T141, T186, T187, X333, X334, X335, X336, T188, T189, T190, T152, X337))
U9_gaaaaaaaaaaaaga(T139, T140, T141, T184, T185, X333, X334, X335, X336, T157, T158, T160, T154, T161, T156, T155, T159, T153, T152, X337, balance5523_out_gaaaaaaaaaga(T141, T186, T187, X333, X334, X335, X336, T188, T189, T190, T152, X337)) → balance5512_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)
U10_ga(T20, T21, T22, T28, T29, T31, balance5512_out_gaaaaaaaaaaaaga(T20, X125, X126, X120, X121, X122, X123, T28, T27, T29, T30, T31, T26, T21, X124)) → balance1_out_ga(tree(T20, T21, T22), tree(T28, T29, T31))
balance1_in_ga(tree(T20, T21, T22), tree(T28, T29, T31)) → U11_ga(T20, T21, T22, T28, T29, T31, balance5512_in_gaaaaaaaaaaaaga(T20, T48, T49, T50, T51, T52, T53, T28, T27, T29, T30, T31, T26, T21, T54))
U11_ga(T20, T21, T22, T28, T29, T31, balance5512_out_gaaaaaaaaaaaaga(T20, T48, T49, T50, T51, T52, T53, T28, T27, T29, T30, T31, T26, T21, T54)) → U12_ga(T20, T21, T22, T28, T29, T31, balance5513_in_gaaaaaaa(T22, T50, T51, T48, T49, T52, T53, T54))
balance5513_in_gaaaaaaa(nil, T415, [], T417, T418, .(','(nil, -(T417, T417)), T418), [], []) → balance5513_out_gaaaaaaa(nil, T415, [], T417, T418, .(','(nil, -(T417, T417)), T418), [], [])
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))
U4_gaaaaaaa(T452, T453, T454, T468, T469, T474, T473, T459, T460, T461, T462, T463, T470, T465, T471, T472, balance5523_out_gaaaaaaaaaga(T452, T468, T469, X692, X693, X694, X695, T470, T471, T472, T453, X696)) → balance5513_out_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)
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, balance5523_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, balance5523_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))
U6_gaaaaaaa(T452, T453, T454, T468, T469, T498, T499, T459, T460, T461, T462, T463, T470, T465, T471, T472, balance5513_out_gaaaaaaa(T454, T493, T494, T498, T499, T495, T496, T497)) → balance5513_out_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)
U12_ga(T20, T21, T22, T28, T29, T31, balance5513_out_gaaaaaaa(T22, T50, T51, T48, T49, T52, T53, T54)) → balance1_out_ga(tree(T20, T21, T22), tree(T28, T29, T31))

(7) DependencyGraphProof (EQUIVALENT transformation)

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

(8) Complex Obligation (AND)

(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, balance5523_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, balance5523_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:

balance1_in_ga(nil, nil) → balance1_out_ga(nil, nil)
balance1_in_ga(tree(T20, T21, T22), tree(T28, T29, T31)) → U10_ga(T20, T21, T22, T28, T29, T31, balance5512_in_gaaaaaaaaaaaaga(T20, X125, X126, X120, X121, X122, X123, T28, T27, T29, T30, T31, T26, T21, X124))
balance5512_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) → balance5512_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)
balance5512_in_gaaaaaaaaaaaaga(tree(T139, T140, T141), X331, X332, X333, X334, X335, X336, tree(T157, T158, T160), T154, T161, T156, T155, .(','(T157, -(T154, .(T158, T159))), .(','(T160, -(T159, .(T161, T156))), T153)), T152, X337) → U7_gaaaaaaaaaaaaga(T139, T140, T141, X331, X332, X333, X334, X335, X336, T157, T158, T160, T154, T161, T156, T155, T159, T153, T152, X337, 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(nil, T267, .(','(nil, -(T269, T269)), T270), T269, T270, T271, T272, T271, T272, .(T274, T275), T274, T275) → balance5523_out_gaaaaaaaaaga(nil, T267, .(','(nil, -(T269, T269)), T270), T269, T270, T271, T272, T271, T272, .(T274, T275), T274, T275)
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) → U2_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, 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, balance5523_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))
U3_gaaaaaaaaaga(T306, T307, T308, T321, T322, X528, X529, X530, X531, T311, T312, T313, T314, T315, T323, T317, T324, T325, T320, X532, balance5523_out_gaaaaaaaaaga(T308, T344, T345, X528, X529, X530, X531, T346, T347, T348, T320, X532)) → balance5523_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)
U1_gaaaaaaaaaga(T306, T307, T308, T321, T322, X528, X529, X530, X531, T311, T312, T313, T314, T315, T323, T317, T324, T325, T320, X532, balance5523_out_gaaaaaaaaaga(T306, T321, T322, X523, X524, X525, X526, T323, T324, T325, T307, X527)) → balance5523_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)
U7_gaaaaaaaaaaaaga(T139, T140, T141, X331, X332, X333, X334, X335, X336, T157, T158, T160, T154, T161, T156, T155, T159, T153, T152, X337, balance5523_out_gaaaaaaaaaga(T139, X331, X332, X326, X327, X328, X329, .(','(T155, -(T156, [])), .(','(T157, -(T154, .(T158, T159))), .(','(T160, -(T159, .(T161, T156))), T153))), T153, T154, T140, X330)) → balance5512_out_gaaaaaaaaaaaaga(tree(T139, T140, T141), X331, X332, X333, X334, X335, X336, tree(T157, T158, T160), T154, T161, T156, T155, .(','(T157, -(T154, .(T158, T159))), .(','(T160, -(T159, .(T161, T156))), T153)), T152, X337)
balance5512_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) → U8_gaaaaaaaaaaaaga(T139, T140, T141, T184, T185, X333, X334, X335, X336, T157, T158, T160, T154, T161, T156, T155, T159, T153, T152, X337, balance5523_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_gaaaaaaaaaaaaga(T139, T140, T141, T184, T185, X333, X334, X335, X336, T157, T158, T160, T154, T161, T156, T155, T159, T153, T152, X337, balance5523_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_gaaaaaaaaaaaaga(T139, T140, T141, T184, T185, X333, X334, X335, X336, T157, T158, T160, T154, T161, T156, T155, T159, T153, T152, X337, balance5523_in_gaaaaaaaaaga(T141, T186, T187, X333, X334, X335, X336, T188, T189, T190, T152, X337))
U9_gaaaaaaaaaaaaga(T139, T140, T141, T184, T185, X333, X334, X335, X336, T157, T158, T160, T154, T161, T156, T155, T159, T153, T152, X337, balance5523_out_gaaaaaaaaaga(T141, T186, T187, X333, X334, X335, X336, T188, T189, T190, T152, X337)) → balance5512_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)
U10_ga(T20, T21, T22, T28, T29, T31, balance5512_out_gaaaaaaaaaaaaga(T20, X125, X126, X120, X121, X122, X123, T28, T27, T29, T30, T31, T26, T21, X124)) → balance1_out_ga(tree(T20, T21, T22), tree(T28, T29, T31))
balance1_in_ga(tree(T20, T21, T22), tree(T28, T29, T31)) → U11_ga(T20, T21, T22, T28, T29, T31, balance5512_in_gaaaaaaaaaaaaga(T20, T48, T49, T50, T51, T52, T53, T28, T27, T29, T30, T31, T26, T21, T54))
U11_ga(T20, T21, T22, T28, T29, T31, balance5512_out_gaaaaaaaaaaaaga(T20, T48, T49, T50, T51, T52, T53, T28, T27, T29, T30, T31, T26, T21, T54)) → U12_ga(T20, T21, T22, T28, T29, T31, balance5513_in_gaaaaaaa(T22, T50, T51, T48, T49, T52, T53, T54))
balance5513_in_gaaaaaaa(nil, T415, [], T417, T418, .(','(nil, -(T417, T417)), T418), [], []) → balance5513_out_gaaaaaaa(nil, T415, [], T417, T418, .(','(nil, -(T417, T417)), T418), [], [])
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))
U4_gaaaaaaa(T452, T453, T454, T468, T469, T474, T473, T459, T460, T461, T462, T463, T470, T465, T471, T472, balance5523_out_gaaaaaaaaaga(T452, T468, T469, X692, X693, X694, X695, T470, T471, T472, T453, X696)) → balance5513_out_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)
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, balance5523_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, balance5523_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))
U6_gaaaaaaa(T452, T453, T454, T468, T469, T498, T499, T459, T460, T461, T462, T463, T470, T465, T471, T472, balance5513_out_gaaaaaaa(T454, T493, T494, T498, T499, T495, T496, T497)) → balance5513_out_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)
U12_ga(T20, T21, T22, T28, T29, T31, balance5513_out_gaaaaaaa(T22, T50, T51, T48, T49, T52, T53, T54)) → balance1_out_ga(tree(T20, T21, T22), tree(T28, T29, T31))

(10) UsableRulesProof (EQUIVALENT transformation)

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

(11) 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, balance5523_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, balance5523_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:

balance5523_in_gaaaaaaaaaga(nil, T267, .(','(nil, -(T269, T269)), T270), T269, T270, T271, T272, T271, T272, .(T274, T275), T274, T275) → balance5523_out_gaaaaaaaaaga(nil, T267, .(','(nil, -(T269, T269)), T270), T269, T270, T271, T272, T271, T272, .(T274, T275), T274, T275)
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) → U2_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, T344, T345, T346, T347, T323, T324, T325, T307, T348))
U1_gaaaaaaaaaga(T306, T307, T308, T321, T322, X528, X529, X530, X531, T311, T312, T313, T314, T315, T323, T317, T324, T325, T320, X532, balance5523_out_gaaaaaaaaaga(T306, T321, T322, X523, X524, X525, X526, T323, T324, T325, T307, X527)) → balance5523_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)
U2_gaaaaaaaaaga(T306, T307, T308, T321, T322, X528, X529, X530, X531, T311, T312, T313, T314, T315, T323, T317, T324, T325, T320, X532, balance5523_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))
U3_gaaaaaaaaaga(T306, T307, T308, T321, T322, X528, X529, X530, X531, T311, T312, T313, T314, T315, T323, T317, T324, T325, T320, X532, balance5523_out_gaaaaaaaaaga(T308, T344, T345, X528, X529, X530, X531, T346, T347, T348, T320, X532)) → balance5523_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:
nil = nil
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)
balance5523_out_gaaaaaaaaaga(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12) = balance5523_out_gaaaaaaaaaga
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(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(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(x21)
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(x3, x19, x21)

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

(12) PiDPToQDPProof (SOUND transformation)

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

(13) Obligation:

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

BALANCE5523_IN_GAAAAAAAAAGA(tree(T306, T307, T308), T320) → U2_GAAAAAAAAAGA(T308, T320, balance5523_in_gaaaaaaaaaga(T306, T307))
U2_GAAAAAAAAAGA(T308, T320, balance5523_out_gaaaaaaaaaga) → 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:

balance5523_in_gaaaaaaaaaga(nil, T274) → balance5523_out_gaaaaaaaaaga
balance5523_in_gaaaaaaaaaga(tree(T306, T307, T308), T320) → U1_gaaaaaaaaaga(balance5523_in_gaaaaaaaaaga(T306, T307))
balance5523_in_gaaaaaaaaaga(tree(T306, T307, T308), T320) → U2_gaaaaaaaaaga(T308, T320, balance5523_in_gaaaaaaaaaga(T306, T307))
U1_gaaaaaaaaaga(balance5523_out_gaaaaaaaaaga) → balance5523_out_gaaaaaaaaaga
U2_gaaaaaaaaaga(T308, T320, balance5523_out_gaaaaaaaaaga) → U3_gaaaaaaaaaga(balance5523_in_gaaaaaaaaaga(T308, T320))
U3_gaaaaaaaaaga(balance5523_out_gaaaaaaaaaga) → balance5523_out_gaaaaaaaaaga

The set Q consists of the following terms:

balance5523_in_gaaaaaaaaaga(x0, x1)
U1_gaaaaaaaaaga(x0)
U2_gaaaaaaaaaga(x0, x1, x2)
U3_gaaaaaaaaaga(x0)

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

(14) 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(T308, T320, balance5523_out_gaaaaaaaaaga) → BALANCE5523_IN_GAAAAAAAAAGA(T308, T320)
The graph contains the following edges 1 >= 1, 2 >= 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(T308, T320, balance5523_in_gaaaaaaaaaga(T306, T307))
The graph contains the following edges 1 > 1, 2 >= 2

(15) YES

(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, balance5523_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, balance5523_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:

balance1_in_ga(nil, nil) → balance1_out_ga(nil, nil)
balance1_in_ga(tree(T20, T21, T22), tree(T28, T29, T31)) → U10_ga(T20, T21, T22, T28, T29, T31, balance5512_in_gaaaaaaaaaaaaga(T20, X125, X126, X120, X121, X122, X123, T28, T27, T29, T30, T31, T26, T21, X124))
balance5512_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) → balance5512_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)
balance5512_in_gaaaaaaaaaaaaga(tree(T139, T140, T141), X331, X332, X333, X334, X335, X336, tree(T157, T158, T160), T154, T161, T156, T155, .(','(T157, -(T154, .(T158, T159))), .(','(T160, -(T159, .(T161, T156))), T153)), T152, X337) → U7_gaaaaaaaaaaaaga(T139, T140, T141, X331, X332, X333, X334, X335, X336, T157, T158, T160, T154, T161, T156, T155, T159, T153, T152, X337, 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(nil, T267, .(','(nil, -(T269, T269)), T270), T269, T270, T271, T272, T271, T272, .(T274, T275), T274, T275) → balance5523_out_gaaaaaaaaaga(nil, T267, .(','(nil, -(T269, T269)), T270), T269, T270, T271, T272, T271, T272, .(T274, T275), T274, T275)
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) → U2_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, 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, balance5523_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))
U3_gaaaaaaaaaga(T306, T307, T308, T321, T322, X528, X529, X530, X531, T311, T312, T313, T314, T315, T323, T317, T324, T325, T320, X532, balance5523_out_gaaaaaaaaaga(T308, T344, T345, X528, X529, X530, X531, T346, T347, T348, T320, X532)) → balance5523_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)
U1_gaaaaaaaaaga(T306, T307, T308, T321, T322, X528, X529, X530, X531, T311, T312, T313, T314, T315, T323, T317, T324, T325, T320, X532, balance5523_out_gaaaaaaaaaga(T306, T321, T322, X523, X524, X525, X526, T323, T324, T325, T307, X527)) → balance5523_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)
U7_gaaaaaaaaaaaaga(T139, T140, T141, X331, X332, X333, X334, X335, X336, T157, T158, T160, T154, T161, T156, T155, T159, T153, T152, X337, balance5523_out_gaaaaaaaaaga(T139, X331, X332, X326, X327, X328, X329, .(','(T155, -(T156, [])), .(','(T157, -(T154, .(T158, T159))), .(','(T160, -(T159, .(T161, T156))), T153))), T153, T154, T140, X330)) → balance5512_out_gaaaaaaaaaaaaga(tree(T139, T140, T141), X331, X332, X333, X334, X335, X336, tree(T157, T158, T160), T154, T161, T156, T155, .(','(T157, -(T154, .(T158, T159))), .(','(T160, -(T159, .(T161, T156))), T153)), T152, X337)
balance5512_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) → U8_gaaaaaaaaaaaaga(T139, T140, T141, T184, T185, X333, X334, X335, X336, T157, T158, T160, T154, T161, T156, T155, T159, T153, T152, X337, balance5523_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_gaaaaaaaaaaaaga(T139, T140, T141, T184, T185, X333, X334, X335, X336, T157, T158, T160, T154, T161, T156, T155, T159, T153, T152, X337, balance5523_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_gaaaaaaaaaaaaga(T139, T140, T141, T184, T185, X333, X334, X335, X336, T157, T158, T160, T154, T161, T156, T155, T159, T153, T152, X337, balance5523_in_gaaaaaaaaaga(T141, T186, T187, X333, X334, X335, X336, T188, T189, T190, T152, X337))
U9_gaaaaaaaaaaaaga(T139, T140, T141, T184, T185, X333, X334, X335, X336, T157, T158, T160, T154, T161, T156, T155, T159, T153, T152, X337, balance5523_out_gaaaaaaaaaga(T141, T186, T187, X333, X334, X335, X336, T188, T189, T190, T152, X337)) → balance5512_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)
U10_ga(T20, T21, T22, T28, T29, T31, balance5512_out_gaaaaaaaaaaaaga(T20, X125, X126, X120, X121, X122, X123, T28, T27, T29, T30, T31, T26, T21, X124)) → balance1_out_ga(tree(T20, T21, T22), tree(T28, T29, T31))
balance1_in_ga(tree(T20, T21, T22), tree(T28, T29, T31)) → U11_ga(T20, T21, T22, T28, T29, T31, balance5512_in_gaaaaaaaaaaaaga(T20, T48, T49, T50, T51, T52, T53, T28, T27, T29, T30, T31, T26, T21, T54))
U11_ga(T20, T21, T22, T28, T29, T31, balance5512_out_gaaaaaaaaaaaaga(T20, T48, T49, T50, T51, T52, T53, T28, T27, T29, T30, T31, T26, T21, T54)) → U12_ga(T20, T21, T22, T28, T29, T31, balance5513_in_gaaaaaaa(T22, T50, T51, T48, T49, T52, T53, T54))
balance5513_in_gaaaaaaa(nil, T415, [], T417, T418, .(','(nil, -(T417, T417)), T418), [], []) → balance5513_out_gaaaaaaa(nil, T415, [], T417, T418, .(','(nil, -(T417, T417)), T418), [], [])
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))
U4_gaaaaaaa(T452, T453, T454, T468, T469, T474, T473, T459, T460, T461, T462, T463, T470, T465, T471, T472, balance5523_out_gaaaaaaaaaga(T452, T468, T469, X692, X693, X694, X695, T470, T471, T472, T453, X696)) → balance5513_out_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)
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, balance5523_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, balance5523_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))
U6_gaaaaaaa(T452, T453, T454, T468, T469, T498, T499, T459, T460, T461, T462, T463, T470, T465, T471, T472, balance5513_out_gaaaaaaa(T454, T493, T494, T498, T499, T495, T496, T497)) → balance5513_out_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)
U12_ga(T20, T21, T22, T28, T29, T31, balance5513_out_gaaaaaaa(T22, T50, T51, T48, T49, T52, T53, T54)) → balance1_out_ga(tree(T20, T21, T22), tree(T28, T29, T31))

(17) UsableRulesProof (EQUIVALENT transformation)

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

(18) 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, balance5523_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, balance5523_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:

balance5523_in_gaaaaaaaaaga(nil, T267, .(','(nil, -(T269, T269)), T270), T269, T270, T271, T272, T271, T272, .(T274, T275), T274, T275) → balance5523_out_gaaaaaaaaaga(nil, T267, .(','(nil, -(T269, T269)), T270), T269, T270, T271, T272, T271, T272, .(T274, T275), T274, T275)
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) → U2_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, T344, T345, T346, T347, T323, T324, T325, T307, T348))
U1_gaaaaaaaaaga(T306, T307, T308, T321, T322, X528, X529, X530, X531, T311, T312, T313, T314, T315, T323, T317, T324, T325, T320, X532, balance5523_out_gaaaaaaaaaga(T306, T321, T322, X523, X524, X525, X526, T323, T324, T325, T307, X527)) → balance5523_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)
U2_gaaaaaaaaaga(T306, T307, T308, T321, T322, X528, X529, X530, X531, T311, T312, T313, T314, T315, T323, T317, T324, T325, T320, X532, balance5523_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))
U3_gaaaaaaaaaga(T306, T307, T308, T321, T322, X528, X529, X530, X531, T311, T312, T313, T314, T315, T323, T317, T324, T325, T320, X532, balance5523_out_gaaaaaaaaaga(T308, T344, T345, X528, X529, X530, X531, T346, T347, T348, T320, X532)) → balance5523_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:
nil = nil
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)
balance5523_out_gaaaaaaaaaga(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12) = balance5523_out_gaaaaaaaaaga
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(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(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(x21)
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(x3, x17)

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

(19) PiDPToQDPProof (SOUND transformation)

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

(20) Obligation:

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

BALANCE5513_IN_GAAAAAAA(tree(T452, T453, T454)) → U5_GAAAAAAA(T454, balance5523_in_gaaaaaaaaaga(T452, T453))
U5_GAAAAAAA(T454, balance5523_out_gaaaaaaaaaga) → BALANCE5513_IN_GAAAAAAA(T454)

The TRS R consists of the following rules:

balance5523_in_gaaaaaaaaaga(nil, T274) → balance5523_out_gaaaaaaaaaga
balance5523_in_gaaaaaaaaaga(tree(T306, T307, T308), T320) → U1_gaaaaaaaaaga(balance5523_in_gaaaaaaaaaga(T306, T307))
balance5523_in_gaaaaaaaaaga(tree(T306, T307, T308), T320) → U2_gaaaaaaaaaga(T308, T320, balance5523_in_gaaaaaaaaaga(T306, T307))
U1_gaaaaaaaaaga(balance5523_out_gaaaaaaaaaga) → balance5523_out_gaaaaaaaaaga
U2_gaaaaaaaaaga(T308, T320, balance5523_out_gaaaaaaaaaga) → U3_gaaaaaaaaaga(balance5523_in_gaaaaaaaaaga(T308, T320))
U3_gaaaaaaaaaga(balance5523_out_gaaaaaaaaaga) → balance5523_out_gaaaaaaaaaga

The set Q consists of the following terms:

balance5523_in_gaaaaaaaaaga(x0, x1)
U1_gaaaaaaaaaga(x0)
U2_gaaaaaaaaaga(x0, x1, x2)
U3_gaaaaaaaaaga(x0)

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

(21) 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(T454, balance5523_out_gaaaaaaaaaga) → BALANCE5513_IN_GAAAAAAA(T454)
The graph contains the following edges 1 >= 1
BALANCE5513_IN_GAAAAAAA(tree(T452, T453, T454)) → U5_GAAAAAAA(T454, balance5523_in_gaaaaaaaaaga(T452, T453))
The graph contains the following edges 1 > 1

(0) Obligation:

(1) PrologToPrologProblemTransformerProof (SOUND transformation)

(2) Obligation:

(3) PrologToPiTRSProof (SOUND transformation)

(4) Obligation:

(5) DependencyPairsProof (EQUIVALENT transformation)

(6) Obligation:

(7) DependencyGraphProof (EQUIVALENT transformation)

(8) Complex Obligation (AND)

(9) Obligation:

(10) UsableRulesProof (EQUIVALENT transformation)

(11) Obligation:

(12) PiDPToQDPProof (SOUND transformation)

(13) Obligation:

(14) QDPSizeChangeProof (EQUIVALENT transformation)

(15) YES

(16) Obligation:

(17) UsableRulesProof (EQUIVALENT transformation)

(18) Obligation:

(19) PiDPToQDPProof (SOUND transformation)

(20) Obligation:

(21) QDPSizeChangeProof (EQUIVALENT transformation)

(22) YES