Left Termination proof of /tmp/tmpD5QGmM/balance

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) :- balance(T, -(I, []), -(.(','(TB, -(I, [])), X), X), -(Rest, []), -(Rest, [])).
balance(nil, -(X, X), -(A, B), -(A, B), -(.(','(nil, -(C, C)), T), T)).
balance(tree(L, V, R), -(IH, IT), -(.(','(tree(LB, VB, RB), -(A, D)), H), .(','(LB, -(A, .(VB, X))), .(','(RB, -(X, D)), T))), -(HR, TR), -(NH, NT)) :- ','(balance(L, -(IH, .(V, IT1)), -(H, T), -(HR1, TR1), -(NH, NT1)), balance(R, -(IT1, IT), -(HR1, TR1), -(HR, TR), -(NT1, NT))).

Queries:

balance(g,a).

(1) PrologToPrologProblemTransformerProof (SOUND transformation)

Built Prolog problem from termination graph.

(2) Obligation:

Clauses:

balance23(nil, .(T257, T258), T257, T258, T259, T260, T259, T260, .(','(nil, -(T261, T261)), T262), T262).
balance23(tree(T291, T292, T293), T305, T295, X433, .(','(tree(T296, T297, T298), -(T299, T300)), T306), .(','(T296, -(T299, .(T297, T302))), .(','(T298, -(T302, T300)), T307)), X434, X435, T308, X436) :- balance23(T291, T305, T292, X429, T306, T307, X430, X431, T308, X432).
balance23(tree(T291, T292, T293), T305, T295, X433, .(','(tree(T296, T297, T298), -(T299, T300)), T306), .(','(T296, -(T299, .(T297, T302))), .(','(T298, -(T302, T300)), T307)), X434, X435, T308, X436) :- ','(balance23(T291, T305, T292, T323, T306, T307, T324, T325, T308, T326), balance23(T293, T323, T295, X433, T324, T325, X434, X435, T326, X436)).
balance13(nil, [], T386, [], T386, .(','(nil, -(T388, T388)), [])).
balance13(tree(T418, T419, T420), T432, .(','(tree(T422, T423, T424), -(T425, T426)), T433), .(','(T422, -(T425, .(T423, T428))), .(','(T424, -(T428, T426)), T434)), T436, T435) :- balance23(T418, T432, T419, X579, T433, T434, X580, X581, T435, X582).
balance13(tree(T418, T419, T420), T432, .(','(tree(T422, T423, T424), -(T425, T426)), T433), .(','(T422, -(T425, .(T423, T428))), .(','(T424, -(T428, T426)), T434)), T455, T435) :- ','(balance23(T418, T432, T419, T451, T433, T434, T452, T453, T435, T454), balance13(T420, T451, T452, T453, T455, T454)).
balance12(nil, .(T107, T108), T107, T108, T109, T110, T111, T112, T113, .(','(T109, -(.(T107, T108), .(T110, T111))), .(','(T112, -(T111, [])), T113)), T113, .(','(nil, -(X200, X200)), X201), X201).
balance12(tree(T142, T143, T144), T156, T146, X276, tree(T160, T161, T163), T164, T159, T158, .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157)), X277, X278, X279, X280) :- balance23(T142, T156, T143, X272, .(','(T158, -(T159, [])), .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157))), T157, X273, X274, X279, X275).
balance12(tree(T142, T143, T144), T156, T146, X276, tree(T160, T161, T163), T164, T159, T158, .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157)), X277, X278, T190, X280) :- ','(balance23(T142, T156, T143, T187, .(','(T158, -(T159, [])), .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157))), T157, T188, T189, T190, T191), balance23(T144, T187, T146, X276, T188, T189, X277, X278, T191, X280)).
balance1(nil, nil).
balance1(tree(T25, T26, T27), tree(T33, T34, T36)) :- balance12(T25, T31, T26, X113, T33, T34, T35, T36, T32, X114, X115, X121, X116).
balance1(tree(T25, T26, T27), tree(T33, T34, T36)) :- ','(balance12(T25, T31, T26, T53, T33, T34, T35, T36, T32, T54, T55, T56, T57), balance13(T27, T53, T54, T55, T56, T57)).

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)
balance12_in: (b,f,b,f,f,f,f,f,f,f,f,f,f)
balance23_in: (b,f,b,f,f,f,f,f,f,f)
balance13_in: (b,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(T25, T26, T27), tree(T33, T34, T36)) → U10_ga(T25, T26, T27, T33, T34, T36, balance12_in_gagaaaaaaaaaa(T25, T31, T26, X113, T33, T34, T35, T36, T32, X114, X115, X121, X116))
balance12_in_gagaaaaaaaaaa(nil, .(T107, T108), T107, T108, T109, T110, T111, T112, T113, .(','(T109, -(.(T107, T108), .(T110, T111))), .(','(T112, -(T111, [])), T113)), T113, .(','(nil, -(X200, X200)), X201), X201) → balance12_out_gagaaaaaaaaaa(nil, .(T107, T108), T107, T108, T109, T110, T111, T112, T113, .(','(T109, -(.(T107, T108), .(T110, T111))), .(','(T112, -(T111, [])), T113)), T113, .(','(nil, -(X200, X200)), X201), X201)
balance12_in_gagaaaaaaaaaa(tree(T142, T143, T144), T156, T146, X276, tree(T160, T161, T163), T164, T159, T158, .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157)), X277, X278, X279, X280) → U7_gagaaaaaaaaaa(T142, T143, T144, T156, T146, X276, T160, T161, T163, T164, T159, T158, T162, T157, X277, X278, X279, X280, balance23_in_gagaaaaaaa(T142, T156, T143, X272, .(','(T158, -(T159, [])), .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157))), T157, X273, X274, X279, X275))
balance23_in_gagaaaaaaa(nil, .(T257, T258), T257, T258, T259, T260, T259, T260, .(','(nil, -(T261, T261)), T262), T262) → balance23_out_gagaaaaaaa(nil, .(T257, T258), T257, T258, T259, T260, T259, T260, .(','(nil, -(T261, T261)), T262), T262)
balance23_in_gagaaaaaaa(tree(T291, T292, T293), T305, T295, X433, .(','(tree(T296, T297, T298), -(T299, T300)), T306), .(','(T296, -(T299, .(T297, T302))), .(','(T298, -(T302, T300)), T307)), X434, X435, T308, X436) → U1_gagaaaaaaa(T291, T292, T293, T305, T295, X433, T296, T297, T298, T299, T300, T306, T302, T307, X434, X435, T308, X436, balance23_in_gagaaaaaaa(T291, T305, T292, X429, T306, T307, X430, X431, T308, X432))
balance23_in_gagaaaaaaa(tree(T291, T292, T293), T305, T295, X433, .(','(tree(T296, T297, T298), -(T299, T300)), T306), .(','(T296, -(T299, .(T297, T302))), .(','(T298, -(T302, T300)), T307)), X434, X435, T308, X436) → U2_gagaaaaaaa(T291, T292, T293, T305, T295, X433, T296, T297, T298, T299, T300, T306, T302, T307, X434, X435, T308, X436, balance23_in_gagaaaaaaa(T291, T305, T292, T323, T306, T307, T324, T325, T308, T326))
U2_gagaaaaaaa(T291, T292, T293, T305, T295, X433, T296, T297, T298, T299, T300, T306, T302, T307, X434, X435, T308, X436, balance23_out_gagaaaaaaa(T291, T305, T292, T323, T306, T307, T324, T325, T308, T326)) → U3_gagaaaaaaa(T291, T292, T293, T305, T295, X433, T296, T297, T298, T299, T300, T306, T302, T307, X434, X435, T308, X436, balance23_in_gagaaaaaaa(T293, T323, T295, X433, T324, T325, X434, X435, T326, X436))
U3_gagaaaaaaa(T291, T292, T293, T305, T295, X433, T296, T297, T298, T299, T300, T306, T302, T307, X434, X435, T308, X436, balance23_out_gagaaaaaaa(T293, T323, T295, X433, T324, T325, X434, X435, T326, X436)) → balance23_out_gagaaaaaaa(tree(T291, T292, T293), T305, T295, X433, .(','(tree(T296, T297, T298), -(T299, T300)), T306), .(','(T296, -(T299, .(T297, T302))), .(','(T298, -(T302, T300)), T307)), X434, X435, T308, X436)
U1_gagaaaaaaa(T291, T292, T293, T305, T295, X433, T296, T297, T298, T299, T300, T306, T302, T307, X434, X435, T308, X436, balance23_out_gagaaaaaaa(T291, T305, T292, X429, T306, T307, X430, X431, T308, X432)) → balance23_out_gagaaaaaaa(tree(T291, T292, T293), T305, T295, X433, .(','(tree(T296, T297, T298), -(T299, T300)), T306), .(','(T296, -(T299, .(T297, T302))), .(','(T298, -(T302, T300)), T307)), X434, X435, T308, X436)
U7_gagaaaaaaaaaa(T142, T143, T144, T156, T146, X276, T160, T161, T163, T164, T159, T158, T162, T157, X277, X278, X279, X280, balance23_out_gagaaaaaaa(T142, T156, T143, X272, .(','(T158, -(T159, [])), .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157))), T157, X273, X274, X279, X275)) → balance12_out_gagaaaaaaaaaa(tree(T142, T143, T144), T156, T146, X276, tree(T160, T161, T163), T164, T159, T158, .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157)), X277, X278, X279, X280)
balance12_in_gagaaaaaaaaaa(tree(T142, T143, T144), T156, T146, X276, tree(T160, T161, T163), T164, T159, T158, .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157)), X277, X278, T190, X280) → U8_gagaaaaaaaaaa(T142, T143, T144, T156, T146, X276, T160, T161, T163, T164, T159, T158, T162, T157, X277, X278, T190, X280, balance23_in_gagaaaaaaa(T142, T156, T143, T187, .(','(T158, -(T159, [])), .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157))), T157, T188, T189, T190, T191))
U8_gagaaaaaaaaaa(T142, T143, T144, T156, T146, X276, T160, T161, T163, T164, T159, T158, T162, T157, X277, X278, T190, X280, balance23_out_gagaaaaaaa(T142, T156, T143, T187, .(','(T158, -(T159, [])), .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157))), T157, T188, T189, T190, T191)) → U9_gagaaaaaaaaaa(T142, T143, T144, T156, T146, X276, T160, T161, T163, T164, T159, T158, T162, T157, X277, X278, T190, X280, balance23_in_gagaaaaaaa(T144, T187, T146, X276, T188, T189, X277, X278, T191, X280))
U9_gagaaaaaaaaaa(T142, T143, T144, T156, T146, X276, T160, T161, T163, T164, T159, T158, T162, T157, X277, X278, T190, X280, balance23_out_gagaaaaaaa(T144, T187, T146, X276, T188, T189, X277, X278, T191, X280)) → balance12_out_gagaaaaaaaaaa(tree(T142, T143, T144), T156, T146, X276, tree(T160, T161, T163), T164, T159, T158, .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157)), X277, X278, T190, X280)
U10_ga(T25, T26, T27, T33, T34, T36, balance12_out_gagaaaaaaaaaa(T25, T31, T26, X113, T33, T34, T35, T36, T32, X114, X115, X121, X116)) → balance1_out_ga(tree(T25, T26, T27), tree(T33, T34, T36))
balance1_in_ga(tree(T25, T26, T27), tree(T33, T34, T36)) → U11_ga(T25, T26, T27, T33, T34, T36, balance12_in_gagaaaaaaaaaa(T25, T31, T26, T53, T33, T34, T35, T36, T32, T54, T55, T56, T57))
U11_ga(T25, T26, T27, T33, T34, T36, balance12_out_gagaaaaaaaaaa(T25, T31, T26, T53, T33, T34, T35, T36, T32, T54, T55, T56, T57)) → U12_ga(T25, T26, T27, T33, T34, T36, balance13_in_gaaaaa(T27, T53, T54, T55, T56, T57))
balance13_in_gaaaaa(nil, [], T386, [], T386, .(','(nil, -(T388, T388)), [])) → balance13_out_gaaaaa(nil, [], T386, [], T386, .(','(nil, -(T388, T388)), []))
balance13_in_gaaaaa(tree(T418, T419, T420), T432, .(','(tree(T422, T423, T424), -(T425, T426)), T433), .(','(T422, -(T425, .(T423, T428))), .(','(T424, -(T428, T426)), T434)), T436, T435) → U4_gaaaaa(T418, T419, T420, T432, T422, T423, T424, T425, T426, T433, T428, T434, T436, T435, balance23_in_gagaaaaaaa(T418, T432, T419, X579, T433, T434, X580, X581, T435, X582))
U4_gaaaaa(T418, T419, T420, T432, T422, T423, T424, T425, T426, T433, T428, T434, T436, T435, balance23_out_gagaaaaaaa(T418, T432, T419, X579, T433, T434, X580, X581, T435, X582)) → balance13_out_gaaaaa(tree(T418, T419, T420), T432, .(','(tree(T422, T423, T424), -(T425, T426)), T433), .(','(T422, -(T425, .(T423, T428))), .(','(T424, -(T428, T426)), T434)), T436, T435)
balance13_in_gaaaaa(tree(T418, T419, T420), T432, .(','(tree(T422, T423, T424), -(T425, T426)), T433), .(','(T422, -(T425, .(T423, T428))), .(','(T424, -(T428, T426)), T434)), T455, T435) → U5_gaaaaa(T418, T419, T420, T432, T422, T423, T424, T425, T426, T433, T428, T434, T455, T435, balance23_in_gagaaaaaaa(T418, T432, T419, T451, T433, T434, T452, T453, T435, T454))
U5_gaaaaa(T418, T419, T420, T432, T422, T423, T424, T425, T426, T433, T428, T434, T455, T435, balance23_out_gagaaaaaaa(T418, T432, T419, T451, T433, T434, T452, T453, T435, T454)) → U6_gaaaaa(T418, T419, T420, T432, T422, T423, T424, T425, T426, T433, T428, T434, T455, T435, balance13_in_gaaaaa(T420, T451, T452, T453, T455, T454))
U6_gaaaaa(T418, T419, T420, T432, T422, T423, T424, T425, T426, T433, T428, T434, T455, T435, balance13_out_gaaaaa(T420, T451, T452, T453, T455, T454)) → balance13_out_gaaaaa(tree(T418, T419, T420), T432, .(','(tree(T422, T423, T424), -(T425, T426)), T433), .(','(T422, -(T425, .(T423, T428))), .(','(T424, -(T428, T426)), T434)), T455, T435)
U12_ga(T25, T26, T27, T33, T34, T36, balance13_out_gaaaaa(T27, T53, T54, T55, T56, T57)) → balance1_out_ga(tree(T25, T26, T27), tree(T33, T34, T36))

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(T25, T26, T27), tree(T33, T34, T36)) → U10_ga(T25, T26, T27, T33, T34, T36, balance12_in_gagaaaaaaaaaa(T25, T31, T26, X113, T33, T34, T35, T36, T32, X114, X115, X121, X116))
balance12_in_gagaaaaaaaaaa(nil, .(T107, T108), T107, T108, T109, T110, T111, T112, T113, .(','(T109, -(.(T107, T108), .(T110, T111))), .(','(T112, -(T111, [])), T113)), T113, .(','(nil, -(X200, X200)), X201), X201) → balance12_out_gagaaaaaaaaaa(nil, .(T107, T108), T107, T108, T109, T110, T111, T112, T113, .(','(T109, -(.(T107, T108), .(T110, T111))), .(','(T112, -(T111, [])), T113)), T113, .(','(nil, -(X200, X200)), X201), X201)
balance12_in_gagaaaaaaaaaa(tree(T142, T143, T144), T156, T146, X276, tree(T160, T161, T163), T164, T159, T158, .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157)), X277, X278, X279, X280) → U7_gagaaaaaaaaaa(T142, T143, T144, T156, T146, X276, T160, T161, T163, T164, T159, T158, T162, T157, X277, X278, X279, X280, balance23_in_gagaaaaaaa(T142, T156, T143, X272, .(','(T158, -(T159, [])), .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157))), T157, X273, X274, X279, X275))
balance23_in_gagaaaaaaa(nil, .(T257, T258), T257, T258, T259, T260, T259, T260, .(','(nil, -(T261, T261)), T262), T262) → balance23_out_gagaaaaaaa(nil, .(T257, T258), T257, T258, T259, T260, T259, T260, .(','(nil, -(T261, T261)), T262), T262)
balance23_in_gagaaaaaaa(tree(T291, T292, T293), T305, T295, X433, .(','(tree(T296, T297, T298), -(T299, T300)), T306), .(','(T296, -(T299, .(T297, T302))), .(','(T298, -(T302, T300)), T307)), X434, X435, T308, X436) → U1_gagaaaaaaa(T291, T292, T293, T305, T295, X433, T296, T297, T298, T299, T300, T306, T302, T307, X434, X435, T308, X436, balance23_in_gagaaaaaaa(T291, T305, T292, X429, T306, T307, X430, X431, T308, X432))
balance23_in_gagaaaaaaa(tree(T291, T292, T293), T305, T295, X433, .(','(tree(T296, T297, T298), -(T299, T300)), T306), .(','(T296, -(T299, .(T297, T302))), .(','(T298, -(T302, T300)), T307)), X434, X435, T308, X436) → U2_gagaaaaaaa(T291, T292, T293, T305, T295, X433, T296, T297, T298, T299, T300, T306, T302, T307, X434, X435, T308, X436, balance23_in_gagaaaaaaa(T291, T305, T292, T323, T306, T307, T324, T325, T308, T326))
U2_gagaaaaaaa(T291, T292, T293, T305, T295, X433, T296, T297, T298, T299, T300, T306, T302, T307, X434, X435, T308, X436, balance23_out_gagaaaaaaa(T291, T305, T292, T323, T306, T307, T324, T325, T308, T326)) → U3_gagaaaaaaa(T291, T292, T293, T305, T295, X433, T296, T297, T298, T299, T300, T306, T302, T307, X434, X435, T308, X436, balance23_in_gagaaaaaaa(T293, T323, T295, X433, T324, T325, X434, X435, T326, X436))
U3_gagaaaaaaa(T291, T292, T293, T305, T295, X433, T296, T297, T298, T299, T300, T306, T302, T307, X434, X435, T308, X436, balance23_out_gagaaaaaaa(T293, T323, T295, X433, T324, T325, X434, X435, T326, X436)) → balance23_out_gagaaaaaaa(tree(T291, T292, T293), T305, T295, X433, .(','(tree(T296, T297, T298), -(T299, T300)), T306), .(','(T296, -(T299, .(T297, T302))), .(','(T298, -(T302, T300)), T307)), X434, X435, T308, X436)
U1_gagaaaaaaa(T291, T292, T293, T305, T295, X433, T296, T297, T298, T299, T300, T306, T302, T307, X434, X435, T308, X436, balance23_out_gagaaaaaaa(T291, T305, T292, X429, T306, T307, X430, X431, T308, X432)) → balance23_out_gagaaaaaaa(tree(T291, T292, T293), T305, T295, X433, .(','(tree(T296, T297, T298), -(T299, T300)), T306), .(','(T296, -(T299, .(T297, T302))), .(','(T298, -(T302, T300)), T307)), X434, X435, T308, X436)
U7_gagaaaaaaaaaa(T142, T143, T144, T156, T146, X276, T160, T161, T163, T164, T159, T158, T162, T157, X277, X278, X279, X280, balance23_out_gagaaaaaaa(T142, T156, T143, X272, .(','(T158, -(T159, [])), .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157))), T157, X273, X274, X279, X275)) → balance12_out_gagaaaaaaaaaa(tree(T142, T143, T144), T156, T146, X276, tree(T160, T161, T163), T164, T159, T158, .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157)), X277, X278, X279, X280)
balance12_in_gagaaaaaaaaaa(tree(T142, T143, T144), T156, T146, X276, tree(T160, T161, T163), T164, T159, T158, .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157)), X277, X278, T190, X280) → U8_gagaaaaaaaaaa(T142, T143, T144, T156, T146, X276, T160, T161, T163, T164, T159, T158, T162, T157, X277, X278, T190, X280, balance23_in_gagaaaaaaa(T142, T156, T143, T187, .(','(T158, -(T159, [])), .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157))), T157, T188, T189, T190, T191))
U8_gagaaaaaaaaaa(T142, T143, T144, T156, T146, X276, T160, T161, T163, T164, T159, T158, T162, T157, X277, X278, T190, X280, balance23_out_gagaaaaaaa(T142, T156, T143, T187, .(','(T158, -(T159, [])), .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157))), T157, T188, T189, T190, T191)) → U9_gagaaaaaaaaaa(T142, T143, T144, T156, T146, X276, T160, T161, T163, T164, T159, T158, T162, T157, X277, X278, T190, X280, balance23_in_gagaaaaaaa(T144, T187, T146, X276, T188, T189, X277, X278, T191, X280))
U9_gagaaaaaaaaaa(T142, T143, T144, T156, T146, X276, T160, T161, T163, T164, T159, T158, T162, T157, X277, X278, T190, X280, balance23_out_gagaaaaaaa(T144, T187, T146, X276, T188, T189, X277, X278, T191, X280)) → balance12_out_gagaaaaaaaaaa(tree(T142, T143, T144), T156, T146, X276, tree(T160, T161, T163), T164, T159, T158, .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157)), X277, X278, T190, X280)
U10_ga(T25, T26, T27, T33, T34, T36, balance12_out_gagaaaaaaaaaa(T25, T31, T26, X113, T33, T34, T35, T36, T32, X114, X115, X121, X116)) → balance1_out_ga(tree(T25, T26, T27), tree(T33, T34, T36))
balance1_in_ga(tree(T25, T26, T27), tree(T33, T34, T36)) → U11_ga(T25, T26, T27, T33, T34, T36, balance12_in_gagaaaaaaaaaa(T25, T31, T26, T53, T33, T34, T35, T36, T32, T54, T55, T56, T57))
U11_ga(T25, T26, T27, T33, T34, T36, balance12_out_gagaaaaaaaaaa(T25, T31, T26, T53, T33, T34, T35, T36, T32, T54, T55, T56, T57)) → U12_ga(T25, T26, T27, T33, T34, T36, balance13_in_gaaaaa(T27, T53, T54, T55, T56, T57))
balance13_in_gaaaaa(nil, [], T386, [], T386, .(','(nil, -(T388, T388)), [])) → balance13_out_gaaaaa(nil, [], T386, [], T386, .(','(nil, -(T388, T388)), []))
balance13_in_gaaaaa(tree(T418, T419, T420), T432, .(','(tree(T422, T423, T424), -(T425, T426)), T433), .(','(T422, -(T425, .(T423, T428))), .(','(T424, -(T428, T426)), T434)), T436, T435) → U4_gaaaaa(T418, T419, T420, T432, T422, T423, T424, T425, T426, T433, T428, T434, T436, T435, balance23_in_gagaaaaaaa(T418, T432, T419, X579, T433, T434, X580, X581, T435, X582))
U4_gaaaaa(T418, T419, T420, T432, T422, T423, T424, T425, T426, T433, T428, T434, T436, T435, balance23_out_gagaaaaaaa(T418, T432, T419, X579, T433, T434, X580, X581, T435, X582)) → balance13_out_gaaaaa(tree(T418, T419, T420), T432, .(','(tree(T422, T423, T424), -(T425, T426)), T433), .(','(T422, -(T425, .(T423, T428))), .(','(T424, -(T428, T426)), T434)), T436, T435)
balance13_in_gaaaaa(tree(T418, T419, T420), T432, .(','(tree(T422, T423, T424), -(T425, T426)), T433), .(','(T422, -(T425, .(T423, T428))), .(','(T424, -(T428, T426)), T434)), T455, T435) → U5_gaaaaa(T418, T419, T420, T432, T422, T423, T424, T425, T426, T433, T428, T434, T455, T435, balance23_in_gagaaaaaaa(T418, T432, T419, T451, T433, T434, T452, T453, T435, T454))
U5_gaaaaa(T418, T419, T420, T432, T422, T423, T424, T425, T426, T433, T428, T434, T455, T435, balance23_out_gagaaaaaaa(T418, T432, T419, T451, T433, T434, T452, T453, T435, T454)) → U6_gaaaaa(T418, T419, T420, T432, T422, T423, T424, T425, T426, T433, T428, T434, T455, T435, balance13_in_gaaaaa(T420, T451, T452, T453, T455, T454))
U6_gaaaaa(T418, T419, T420, T432, T422, T423, T424, T425, T426, T433, T428, T434, T455, T435, balance13_out_gaaaaa(T420, T451, T452, T453, T455, T454)) → balance13_out_gaaaaa(tree(T418, T419, T420), T432, .(','(tree(T422, T423, T424), -(T425, T426)), T433), .(','(T422, -(T425, .(T423, T428))), .(','(T424, -(T428, T426)), T434)), T455, T435)
U12_ga(T25, T26, T27, T33, T34, T36, balance13_out_gaaaaa(T27, T53, T54, T55, T56, T57)) → balance1_out_ga(tree(T25, T26, T27), tree(T33, T34, T36))

(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(T25, T26, T27), tree(T33, T34, T36)) → U10_GA(T25, T26, T27, T33, T34, T36, balance12_in_gagaaaaaaaaaa(T25, T31, T26, X113, T33, T34, T35, T36, T32, X114, X115, X121, X116))
BALANCE1_IN_GA(tree(T25, T26, T27), tree(T33, T34, T36)) → BALANCE12_IN_GAGAAAAAAAAAA(T25, T31, T26, X113, T33, T34, T35, T36, T32, X114, X115, X121, X116)
BALANCE12_IN_GAGAAAAAAAAAA(tree(T142, T143, T144), T156, T146, X276, tree(T160, T161, T163), T164, T159, T158, .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157)), X277, X278, X279, X280) → U7_GAGAAAAAAAAAA(T142, T143, T144, T156, T146, X276, T160, T161, T163, T164, T159, T158, T162, T157, X277, X278, X279, X280, balance23_in_gagaaaaaaa(T142, T156, T143, X272, .(','(T158, -(T159, [])), .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157))), T157, X273, X274, X279, X275))
BALANCE12_IN_GAGAAAAAAAAAA(tree(T142, T143, T144), T156, T146, X276, tree(T160, T161, T163), T164, T159, T158, .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157)), X277, X278, X279, X280) → BALANCE23_IN_GAGAAAAAAA(T142, T156, T143, X272, .(','(T158, -(T159, [])), .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157))), T157, X273, X274, X279, X275)
BALANCE23_IN_GAGAAAAAAA(tree(T291, T292, T293), T305, T295, X433, .(','(tree(T296, T297, T298), -(T299, T300)), T306), .(','(T296, -(T299, .(T297, T302))), .(','(T298, -(T302, T300)), T307)), X434, X435, T308, X436) → U1_GAGAAAAAAA(T291, T292, T293, T305, T295, X433, T296, T297, T298, T299, T300, T306, T302, T307, X434, X435, T308, X436, balance23_in_gagaaaaaaa(T291, T305, T292, X429, T306, T307, X430, X431, T308, X432))
BALANCE23_IN_GAGAAAAAAA(tree(T291, T292, T293), T305, T295, X433, .(','(tree(T296, T297, T298), -(T299, T300)), T306), .(','(T296, -(T299, .(T297, T302))), .(','(T298, -(T302, T300)), T307)), X434, X435, T308, X436) → BALANCE23_IN_GAGAAAAAAA(T291, T305, T292, X429, T306, T307, X430, X431, T308, X432)
BALANCE23_IN_GAGAAAAAAA(tree(T291, T292, T293), T305, T295, X433, .(','(tree(T296, T297, T298), -(T299, T300)), T306), .(','(T296, -(T299, .(T297, T302))), .(','(T298, -(T302, T300)), T307)), X434, X435, T308, X436) → U2_GAGAAAAAAA(T291, T292, T293, T305, T295, X433, T296, T297, T298, T299, T300, T306, T302, T307, X434, X435, T308, X436, balance23_in_gagaaaaaaa(T291, T305, T292, T323, T306, T307, T324, T325, T308, T326))
U2_GAGAAAAAAA(T291, T292, T293, T305, T295, X433, T296, T297, T298, T299, T300, T306, T302, T307, X434, X435, T308, X436, balance23_out_gagaaaaaaa(T291, T305, T292, T323, T306, T307, T324, T325, T308, T326)) → U3_GAGAAAAAAA(T291, T292, T293, T305, T295, X433, T296, T297, T298, T299, T300, T306, T302, T307, X434, X435, T308, X436, balance23_in_gagaaaaaaa(T293, T323, T295, X433, T324, T325, X434, X435, T326, X436))
U2_GAGAAAAAAA(T291, T292, T293, T305, T295, X433, T296, T297, T298, T299, T300, T306, T302, T307, X434, X435, T308, X436, balance23_out_gagaaaaaaa(T291, T305, T292, T323, T306, T307, T324, T325, T308, T326)) → BALANCE23_IN_GAGAAAAAAA(T293, T323, T295, X433, T324, T325, X434, X435, T326, X436)
BALANCE12_IN_GAGAAAAAAAAAA(tree(T142, T143, T144), T156, T146, X276, tree(T160, T161, T163), T164, T159, T158, .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157)), X277, X278, T190, X280) → U8_GAGAAAAAAAAAA(T142, T143, T144, T156, T146, X276, T160, T161, T163, T164, T159, T158, T162, T157, X277, X278, T190, X280, balance23_in_gagaaaaaaa(T142, T156, T143, T187, .(','(T158, -(T159, [])), .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157))), T157, T188, T189, T190, T191))
U8_GAGAAAAAAAAAA(T142, T143, T144, T156, T146, X276, T160, T161, T163, T164, T159, T158, T162, T157, X277, X278, T190, X280, balance23_out_gagaaaaaaa(T142, T156, T143, T187, .(','(T158, -(T159, [])), .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157))), T157, T188, T189, T190, T191)) → U9_GAGAAAAAAAAAA(T142, T143, T144, T156, T146, X276, T160, T161, T163, T164, T159, T158, T162, T157, X277, X278, T190, X280, balance23_in_gagaaaaaaa(T144, T187, T146, X276, T188, T189, X277, X278, T191, X280))
U8_GAGAAAAAAAAAA(T142, T143, T144, T156, T146, X276, T160, T161, T163, T164, T159, T158, T162, T157, X277, X278, T190, X280, balance23_out_gagaaaaaaa(T142, T156, T143, T187, .(','(T158, -(T159, [])), .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157))), T157, T188, T189, T190, T191)) → BALANCE23_IN_GAGAAAAAAA(T144, T187, T146, X276, T188, T189, X277, X278, T191, X280)
BALANCE1_IN_GA(tree(T25, T26, T27), tree(T33, T34, T36)) → U11_GA(T25, T26, T27, T33, T34, T36, balance12_in_gagaaaaaaaaaa(T25, T31, T26, T53, T33, T34, T35, T36, T32, T54, T55, T56, T57))
U11_GA(T25, T26, T27, T33, T34, T36, balance12_out_gagaaaaaaaaaa(T25, T31, T26, T53, T33, T34, T35, T36, T32, T54, T55, T56, T57)) → U12_GA(T25, T26, T27, T33, T34, T36, balance13_in_gaaaaa(T27, T53, T54, T55, T56, T57))
U11_GA(T25, T26, T27, T33, T34, T36, balance12_out_gagaaaaaaaaaa(T25, T31, T26, T53, T33, T34, T35, T36, T32, T54, T55, T56, T57)) → BALANCE13_IN_GAAAAA(T27, T53, T54, T55, T56, T57)
BALANCE13_IN_GAAAAA(tree(T418, T419, T420), T432, .(','(tree(T422, T423, T424), -(T425, T426)), T433), .(','(T422, -(T425, .(T423, T428))), .(','(T424, -(T428, T426)), T434)), T436, T435) → U4_GAAAAA(T418, T419, T420, T432, T422, T423, T424, T425, T426, T433, T428, T434, T436, T435, balance23_in_gagaaaaaaa(T418, T432, T419, X579, T433, T434, X580, X581, T435, X582))
BALANCE13_IN_GAAAAA(tree(T418, T419, T420), T432, .(','(tree(T422, T423, T424), -(T425, T426)), T433), .(','(T422, -(T425, .(T423, T428))), .(','(T424, -(T428, T426)), T434)), T436, T435) → BALANCE23_IN_GAGAAAAAAA(T418, T432, T419, X579, T433, T434, X580, X581, T435, X582)
BALANCE13_IN_GAAAAA(tree(T418, T419, T420), T432, .(','(tree(T422, T423, T424), -(T425, T426)), T433), .(','(T422, -(T425, .(T423, T428))), .(','(T424, -(T428, T426)), T434)), T455, T435) → U5_GAAAAA(T418, T419, T420, T432, T422, T423, T424, T425, T426, T433, T428, T434, T455, T435, balance23_in_gagaaaaaaa(T418, T432, T419, T451, T433, T434, T452, T453, T435, T454))
U5_GAAAAA(T418, T419, T420, T432, T422, T423, T424, T425, T426, T433, T428, T434, T455, T435, balance23_out_gagaaaaaaa(T418, T432, T419, T451, T433, T434, T452, T453, T435, T454)) → U6_GAAAAA(T418, T419, T420, T432, T422, T423, T424, T425, T426, T433, T428, T434, T455, T435, balance13_in_gaaaaa(T420, T451, T452, T453, T455, T454))
U5_GAAAAA(T418, T419, T420, T432, T422, T423, T424, T425, T426, T433, T428, T434, T455, T435, balance23_out_gagaaaaaaa(T418, T432, T419, T451, T433, T434, T452, T453, T435, T454)) → BALANCE13_IN_GAAAAA(T420, T451, T452, T453, T455, T454)

The TRS R consists of the following rules:

balance1_in_ga(nil, nil) → balance1_out_ga(nil, nil)
balance1_in_ga(tree(T25, T26, T27), tree(T33, T34, T36)) → U10_ga(T25, T26, T27, T33, T34, T36, balance12_in_gagaaaaaaaaaa(T25, T31, T26, X113, T33, T34, T35, T36, T32, X114, X115, X121, X116))
balance12_in_gagaaaaaaaaaa(nil, .(T107, T108), T107, T108, T109, T110, T111, T112, T113, .(','(T109, -(.(T107, T108), .(T110, T111))), .(','(T112, -(T111, [])), T113)), T113, .(','(nil, -(X200, X200)), X201), X201) → balance12_out_gagaaaaaaaaaa(nil, .(T107, T108), T107, T108, T109, T110, T111, T112, T113, .(','(T109, -(.(T107, T108), .(T110, T111))), .(','(T112, -(T111, [])), T113)), T113, .(','(nil, -(X200, X200)), X201), X201)
balance12_in_gagaaaaaaaaaa(tree(T142, T143, T144), T156, T146, X276, tree(T160, T161, T163), T164, T159, T158, .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157)), X277, X278, X279, X280) → U7_gagaaaaaaaaaa(T142, T143, T144, T156, T146, X276, T160, T161, T163, T164, T159, T158, T162, T157, X277, X278, X279, X280, balance23_in_gagaaaaaaa(T142, T156, T143, X272, .(','(T158, -(T159, [])), .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157))), T157, X273, X274, X279, X275))
balance23_in_gagaaaaaaa(nil, .(T257, T258), T257, T258, T259, T260, T259, T260, .(','(nil, -(T261, T261)), T262), T262) → balance23_out_gagaaaaaaa(nil, .(T257, T258), T257, T258, T259, T260, T259, T260, .(','(nil, -(T261, T261)), T262), T262)
balance23_in_gagaaaaaaa(tree(T291, T292, T293), T305, T295, X433, .(','(tree(T296, T297, T298), -(T299, T300)), T306), .(','(T296, -(T299, .(T297, T302))), .(','(T298, -(T302, T300)), T307)), X434, X435, T308, X436) → U1_gagaaaaaaa(T291, T292, T293, T305, T295, X433, T296, T297, T298, T299, T300, T306, T302, T307, X434, X435, T308, X436, balance23_in_gagaaaaaaa(T291, T305, T292, X429, T306, T307, X430, X431, T308, X432))
balance23_in_gagaaaaaaa(tree(T291, T292, T293), T305, T295, X433, .(','(tree(T296, T297, T298), -(T299, T300)), T306), .(','(T296, -(T299, .(T297, T302))), .(','(T298, -(T302, T300)), T307)), X434, X435, T308, X436) → U2_gagaaaaaaa(T291, T292, T293, T305, T295, X433, T296, T297, T298, T299, T300, T306, T302, T307, X434, X435, T308, X436, balance23_in_gagaaaaaaa(T291, T305, T292, T323, T306, T307, T324, T325, T308, T326))
U2_gagaaaaaaa(T291, T292, T293, T305, T295, X433, T296, T297, T298, T299, T300, T306, T302, T307, X434, X435, T308, X436, balance23_out_gagaaaaaaa(T291, T305, T292, T323, T306, T307, T324, T325, T308, T326)) → U3_gagaaaaaaa(T291, T292, T293, T305, T295, X433, T296, T297, T298, T299, T300, T306, T302, T307, X434, X435, T308, X436, balance23_in_gagaaaaaaa(T293, T323, T295, X433, T324, T325, X434, X435, T326, X436))
U3_gagaaaaaaa(T291, T292, T293, T305, T295, X433, T296, T297, T298, T299, T300, T306, T302, T307, X434, X435, T308, X436, balance23_out_gagaaaaaaa(T293, T323, T295, X433, T324, T325, X434, X435, T326, X436)) → balance23_out_gagaaaaaaa(tree(T291, T292, T293), T305, T295, X433, .(','(tree(T296, T297, T298), -(T299, T300)), T306), .(','(T296, -(T299, .(T297, T302))), .(','(T298, -(T302, T300)), T307)), X434, X435, T308, X436)
U1_gagaaaaaaa(T291, T292, T293, T305, T295, X433, T296, T297, T298, T299, T300, T306, T302, T307, X434, X435, T308, X436, balance23_out_gagaaaaaaa(T291, T305, T292, X429, T306, T307, X430, X431, T308, X432)) → balance23_out_gagaaaaaaa(tree(T291, T292, T293), T305, T295, X433, .(','(tree(T296, T297, T298), -(T299, T300)), T306), .(','(T296, -(T299, .(T297, T302))), .(','(T298, -(T302, T300)), T307)), X434, X435, T308, X436)
U7_gagaaaaaaaaaa(T142, T143, T144, T156, T146, X276, T160, T161, T163, T164, T159, T158, T162, T157, X277, X278, X279, X280, balance23_out_gagaaaaaaa(T142, T156, T143, X272, .(','(T158, -(T159, [])), .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157))), T157, X273, X274, X279, X275)) → balance12_out_gagaaaaaaaaaa(tree(T142, T143, T144), T156, T146, X276, tree(T160, T161, T163), T164, T159, T158, .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157)), X277, X278, X279, X280)
balance12_in_gagaaaaaaaaaa(tree(T142, T143, T144), T156, T146, X276, tree(T160, T161, T163), T164, T159, T158, .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157)), X277, X278, T190, X280) → U8_gagaaaaaaaaaa(T142, T143, T144, T156, T146, X276, T160, T161, T163, T164, T159, T158, T162, T157, X277, X278, T190, X280, balance23_in_gagaaaaaaa(T142, T156, T143, T187, .(','(T158, -(T159, [])), .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157))), T157, T188, T189, T190, T191))
U8_gagaaaaaaaaaa(T142, T143, T144, T156, T146, X276, T160, T161, T163, T164, T159, T158, T162, T157, X277, X278, T190, X280, balance23_out_gagaaaaaaa(T142, T156, T143, T187, .(','(T158, -(T159, [])), .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157))), T157, T188, T189, T190, T191)) → U9_gagaaaaaaaaaa(T142, T143, T144, T156, T146, X276, T160, T161, T163, T164, T159, T158, T162, T157, X277, X278, T190, X280, balance23_in_gagaaaaaaa(T144, T187, T146, X276, T188, T189, X277, X278, T191, X280))
U9_gagaaaaaaaaaa(T142, T143, T144, T156, T146, X276, T160, T161, T163, T164, T159, T158, T162, T157, X277, X278, T190, X280, balance23_out_gagaaaaaaa(T144, T187, T146, X276, T188, T189, X277, X278, T191, X280)) → balance12_out_gagaaaaaaaaaa(tree(T142, T143, T144), T156, T146, X276, tree(T160, T161, T163), T164, T159, T158, .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157)), X277, X278, T190, X280)
U10_ga(T25, T26, T27, T33, T34, T36, balance12_out_gagaaaaaaaaaa(T25, T31, T26, X113, T33, T34, T35, T36, T32, X114, X115, X121, X116)) → balance1_out_ga(tree(T25, T26, T27), tree(T33, T34, T36))
balance1_in_ga(tree(T25, T26, T27), tree(T33, T34, T36)) → U11_ga(T25, T26, T27, T33, T34, T36, balance12_in_gagaaaaaaaaaa(T25, T31, T26, T53, T33, T34, T35, T36, T32, T54, T55, T56, T57))
U11_ga(T25, T26, T27, T33, T34, T36, balance12_out_gagaaaaaaaaaa(T25, T31, T26, T53, T33, T34, T35, T36, T32, T54, T55, T56, T57)) → U12_ga(T25, T26, T27, T33, T34, T36, balance13_in_gaaaaa(T27, T53, T54, T55, T56, T57))
balance13_in_gaaaaa(nil, [], T386, [], T386, .(','(nil, -(T388, T388)), [])) → balance13_out_gaaaaa(nil, [], T386, [], T386, .(','(nil, -(T388, T388)), []))
balance13_in_gaaaaa(tree(T418, T419, T420), T432, .(','(tree(T422, T423, T424), -(T425, T426)), T433), .(','(T422, -(T425, .(T423, T428))), .(','(T424, -(T428, T426)), T434)), T436, T435) → U4_gaaaaa(T418, T419, T420, T432, T422, T423, T424, T425, T426, T433, T428, T434, T436, T435, balance23_in_gagaaaaaaa(T418, T432, T419, X579, T433, T434, X580, X581, T435, X582))
U4_gaaaaa(T418, T419, T420, T432, T422, T423, T424, T425, T426, T433, T428, T434, T436, T435, balance23_out_gagaaaaaaa(T418, T432, T419, X579, T433, T434, X580, X581, T435, X582)) → balance13_out_gaaaaa(tree(T418, T419, T420), T432, .(','(tree(T422, T423, T424), -(T425, T426)), T433), .(','(T422, -(T425, .(T423, T428))), .(','(T424, -(T428, T426)), T434)), T436, T435)
balance13_in_gaaaaa(tree(T418, T419, T420), T432, .(','(tree(T422, T423, T424), -(T425, T426)), T433), .(','(T422, -(T425, .(T423, T428))), .(','(T424, -(T428, T426)), T434)), T455, T435) → U5_gaaaaa(T418, T419, T420, T432, T422, T423, T424, T425, T426, T433, T428, T434, T455, T435, balance23_in_gagaaaaaaa(T418, T432, T419, T451, T433, T434, T452, T453, T435, T454))
U5_gaaaaa(T418, T419, T420, T432, T422, T423, T424, T425, T426, T433, T428, T434, T455, T435, balance23_out_gagaaaaaaa(T418, T432, T419, T451, T433, T434, T452, T453, T435, T454)) → U6_gaaaaa(T418, T419, T420, T432, T422, T423, T424, T425, T426, T433, T428, T434, T455, T435, balance13_in_gaaaaa(T420, T451, T452, T453, T455, T454))
U6_gaaaaa(T418, T419, T420, T432, T422, T423, T424, T425, T426, T433, T428, T434, T455, T435, balance13_out_gaaaaa(T420, T451, T452, T453, T455, T454)) → balance13_out_gaaaaa(tree(T418, T419, T420), T432, .(','(tree(T422, T423, T424), -(T425, T426)), T433), .(','(T422, -(T425, .(T423, T428))), .(','(T424, -(T428, T426)), T434)), T455, T435)
U12_ga(T25, T26, T27, T33, T34, T36, balance13_out_gaaaaa(T27, T53, T54, T55, T56, T57)) → balance1_out_ga(tree(T25, T26, T27), tree(T33, T34, T36))

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(x1)
tree(x1, x2, x3) = tree(x1, x2, x3)
U10_ga(x1, x2, x3, x4, x5, x6, x7) = U10_ga(x1, x2, x3, x7)
balance12_in_gagaaaaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13) = balance12_in_gagaaaaaaaaaa(x1, x3)
balance12_out_gagaaaaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13) = balance12_out_gagaaaaaaaaaa(x1, x3)
U7_gagaaaaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19) = U7_gagaaaaaaaaaa(x1, x2, x3, x5, x19)
balance23_in_gagaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10) = balance23_in_gagaaaaaaa(x1, x3)
balance23_out_gagaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10) = balance23_out_gagaaaaaaa(x1, x3)
U1_gagaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19) = U1_gagaaaaaaa(x1, x2, x3, x5, x19)
U2_gagaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19) = U2_gagaaaaaaa(x1, x2, x3, x5, x19)
U3_gagaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19) = U3_gagaaaaaaa(x1, x2, x3, x5, x19)
U8_gagaaaaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19) = U8_gagaaaaaaaaaa(x1, x2, x3, x5, x19)
U9_gagaaaaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19) = U9_gagaaaaaaaaaa(x1, x2, x3, x5, x19)
U11_ga(x1, x2, x3, x4, x5, x6, x7) = U11_ga(x1, x2, x3, x7)
U12_ga(x1, x2, x3, x4, x5, x6, x7) = U12_ga(x1, x2, x3, x7)
balance13_in_gaaaaa(x1, x2, x3, x4, x5, x6) = balance13_in_gaaaaa(x1)
balance13_out_gaaaaa(x1, x2, x3, x4, x5, x6) = balance13_out_gaaaaa(x1)
U4_gaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15) = U4_gaaaaa(x1, x2, x3, x15)
U5_gaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15) = U5_gaaaaa(x1, x2, x3, x15)
U6_gaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15) = U6_gaaaaa(x1, x2, x3, x15)
BALANCE1_IN_GA(x1, x2) = BALANCE1_IN_GA(x1)
U10_GA(x1, x2, x3, x4, x5, x6, x7) = U10_GA(x1, x2, x3, x7)
BALANCE12_IN_GAGAAAAAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13) = BALANCE12_IN_GAGAAAAAAAAAA(x1, x3)
U7_GAGAAAAAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19) = U7_GAGAAAAAAAAAA(x1, x2, x3, x5, x19)
BALANCE23_IN_GAGAAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10) = BALANCE23_IN_GAGAAAAAAA(x1, x3)
U1_GAGAAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19) = U1_GAGAAAAAAA(x1, x2, x3, x5, x19)
U2_GAGAAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19) = U2_GAGAAAAAAA(x1, x2, x3, x5, x19)
U3_GAGAAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19) = U3_GAGAAAAAAA(x1, x2, x3, x5, x19)
U8_GAGAAAAAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19) = U8_GAGAAAAAAAAAA(x1, x2, x3, x5, x19)
U9_GAGAAAAAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19) = U9_GAGAAAAAAAAAA(x1, x2, x3, x5, x19)
U11_GA(x1, x2, x3, x4, x5, x6, x7) = U11_GA(x1, x2, x3, x7)
U12_GA(x1, x2, x3, x4, x5, x6, x7) = U12_GA(x1, x2, x3, x7)
BALANCE13_IN_GAAAAA(x1, x2, x3, x4, x5, x6) = BALANCE13_IN_GAAAAA(x1)
U4_GAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15) = U4_GAAAAA(x1, x2, x3, x15)
U5_GAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15) = U5_GAAAAA(x1, x2, x3, x15)
U6_GAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15) = U6_GAAAAA(x1, x2, x3, x15)

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(T25, T26, T27), tree(T33, T34, T36)) → U10_GA(T25, T26, T27, T33, T34, T36, balance12_in_gagaaaaaaaaaa(T25, T31, T26, X113, T33, T34, T35, T36, T32, X114, X115, X121, X116))
BALANCE1_IN_GA(tree(T25, T26, T27), tree(T33, T34, T36)) → BALANCE12_IN_GAGAAAAAAAAAA(T25, T31, T26, X113, T33, T34, T35, T36, T32, X114, X115, X121, X116)
BALANCE12_IN_GAGAAAAAAAAAA(tree(T142, T143, T144), T156, T146, X276, tree(T160, T161, T163), T164, T159, T158, .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157)), X277, X278, X279, X280) → U7_GAGAAAAAAAAAA(T142, T143, T144, T156, T146, X276, T160, T161, T163, T164, T159, T158, T162, T157, X277, X278, X279, X280, balance23_in_gagaaaaaaa(T142, T156, T143, X272, .(','(T158, -(T159, [])), .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157))), T157, X273, X274, X279, X275))
BALANCE12_IN_GAGAAAAAAAAAA(tree(T142, T143, T144), T156, T146, X276, tree(T160, T161, T163), T164, T159, T158, .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157)), X277, X278, X279, X280) → BALANCE23_IN_GAGAAAAAAA(T142, T156, T143, X272, .(','(T158, -(T159, [])), .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157))), T157, X273, X274, X279, X275)
BALANCE23_IN_GAGAAAAAAA(tree(T291, T292, T293), T305, T295, X433, .(','(tree(T296, T297, T298), -(T299, T300)), T306), .(','(T296, -(T299, .(T297, T302))), .(','(T298, -(T302, T300)), T307)), X434, X435, T308, X436) → U1_GAGAAAAAAA(T291, T292, T293, T305, T295, X433, T296, T297, T298, T299, T300, T306, T302, T307, X434, X435, T308, X436, balance23_in_gagaaaaaaa(T291, T305, T292, X429, T306, T307, X430, X431, T308, X432))
BALANCE23_IN_GAGAAAAAAA(tree(T291, T292, T293), T305, T295, X433, .(','(tree(T296, T297, T298), -(T299, T300)), T306), .(','(T296, -(T299, .(T297, T302))), .(','(T298, -(T302, T300)), T307)), X434, X435, T308, X436) → BALANCE23_IN_GAGAAAAAAA(T291, T305, T292, X429, T306, T307, X430, X431, T308, X432)
BALANCE23_IN_GAGAAAAAAA(tree(T291, T292, T293), T305, T295, X433, .(','(tree(T296, T297, T298), -(T299, T300)), T306), .(','(T296, -(T299, .(T297, T302))), .(','(T298, -(T302, T300)), T307)), X434, X435, T308, X436) → U2_GAGAAAAAAA(T291, T292, T293, T305, T295, X433, T296, T297, T298, T299, T300, T306, T302, T307, X434, X435, T308, X436, balance23_in_gagaaaaaaa(T291, T305, T292, T323, T306, T307, T324, T325, T308, T326))
U2_GAGAAAAAAA(T291, T292, T293, T305, T295, X433, T296, T297, T298, T299, T300, T306, T302, T307, X434, X435, T308, X436, balance23_out_gagaaaaaaa(T291, T305, T292, T323, T306, T307, T324, T325, T308, T326)) → U3_GAGAAAAAAA(T291, T292, T293, T305, T295, X433, T296, T297, T298, T299, T300, T306, T302, T307, X434, X435, T308, X436, balance23_in_gagaaaaaaa(T293, T323, T295, X433, T324, T325, X434, X435, T326, X436))
U2_GAGAAAAAAA(T291, T292, T293, T305, T295, X433, T296, T297, T298, T299, T300, T306, T302, T307, X434, X435, T308, X436, balance23_out_gagaaaaaaa(T291, T305, T292, T323, T306, T307, T324, T325, T308, T326)) → BALANCE23_IN_GAGAAAAAAA(T293, T323, T295, X433, T324, T325, X434, X435, T326, X436)
BALANCE12_IN_GAGAAAAAAAAAA(tree(T142, T143, T144), T156, T146, X276, tree(T160, T161, T163), T164, T159, T158, .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157)), X277, X278, T190, X280) → U8_GAGAAAAAAAAAA(T142, T143, T144, T156, T146, X276, T160, T161, T163, T164, T159, T158, T162, T157, X277, X278, T190, X280, balance23_in_gagaaaaaaa(T142, T156, T143, T187, .(','(T158, -(T159, [])), .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157))), T157, T188, T189, T190, T191))
U8_GAGAAAAAAAAAA(T142, T143, T144, T156, T146, X276, T160, T161, T163, T164, T159, T158, T162, T157, X277, X278, T190, X280, balance23_out_gagaaaaaaa(T142, T156, T143, T187, .(','(T158, -(T159, [])), .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157))), T157, T188, T189, T190, T191)) → U9_GAGAAAAAAAAAA(T142, T143, T144, T156, T146, X276, T160, T161, T163, T164, T159, T158, T162, T157, X277, X278, T190, X280, balance23_in_gagaaaaaaa(T144, T187, T146, X276, T188, T189, X277, X278, T191, X280))
U8_GAGAAAAAAAAAA(T142, T143, T144, T156, T146, X276, T160, T161, T163, T164, T159, T158, T162, T157, X277, X278, T190, X280, balance23_out_gagaaaaaaa(T142, T156, T143, T187, .(','(T158, -(T159, [])), .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157))), T157, T188, T189, T190, T191)) → BALANCE23_IN_GAGAAAAAAA(T144, T187, T146, X276, T188, T189, X277, X278, T191, X280)
BALANCE1_IN_GA(tree(T25, T26, T27), tree(T33, T34, T36)) → U11_GA(T25, T26, T27, T33, T34, T36, balance12_in_gagaaaaaaaaaa(T25, T31, T26, T53, T33, T34, T35, T36, T32, T54, T55, T56, T57))
U11_GA(T25, T26, T27, T33, T34, T36, balance12_out_gagaaaaaaaaaa(T25, T31, T26, T53, T33, T34, T35, T36, T32, T54, T55, T56, T57)) → U12_GA(T25, T26, T27, T33, T34, T36, balance13_in_gaaaaa(T27, T53, T54, T55, T56, T57))
U11_GA(T25, T26, T27, T33, T34, T36, balance12_out_gagaaaaaaaaaa(T25, T31, T26, T53, T33, T34, T35, T36, T32, T54, T55, T56, T57)) → BALANCE13_IN_GAAAAA(T27, T53, T54, T55, T56, T57)
BALANCE13_IN_GAAAAA(tree(T418, T419, T420), T432, .(','(tree(T422, T423, T424), -(T425, T426)), T433), .(','(T422, -(T425, .(T423, T428))), .(','(T424, -(T428, T426)), T434)), T436, T435) → U4_GAAAAA(T418, T419, T420, T432, T422, T423, T424, T425, T426, T433, T428, T434, T436, T435, balance23_in_gagaaaaaaa(T418, T432, T419, X579, T433, T434, X580, X581, T435, X582))
BALANCE13_IN_GAAAAA(tree(T418, T419, T420), T432, .(','(tree(T422, T423, T424), -(T425, T426)), T433), .(','(T422, -(T425, .(T423, T428))), .(','(T424, -(T428, T426)), T434)), T436, T435) → BALANCE23_IN_GAGAAAAAAA(T418, T432, T419, X579, T433, T434, X580, X581, T435, X582)
BALANCE13_IN_GAAAAA(tree(T418, T419, T420), T432, .(','(tree(T422, T423, T424), -(T425, T426)), T433), .(','(T422, -(T425, .(T423, T428))), .(','(T424, -(T428, T426)), T434)), T455, T435) → U5_GAAAAA(T418, T419, T420, T432, T422, T423, T424, T425, T426, T433, T428, T434, T455, T435, balance23_in_gagaaaaaaa(T418, T432, T419, T451, T433, T434, T452, T453, T435, T454))
U5_GAAAAA(T418, T419, T420, T432, T422, T423, T424, T425, T426, T433, T428, T434, T455, T435, balance23_out_gagaaaaaaa(T418, T432, T419, T451, T433, T434, T452, T453, T435, T454)) → U6_GAAAAA(T418, T419, T420, T432, T422, T423, T424, T425, T426, T433, T428, T434, T455, T435, balance13_in_gaaaaa(T420, T451, T452, T453, T455, T454))
U5_GAAAAA(T418, T419, T420, T432, T422, T423, T424, T425, T426, T433, T428, T434, T455, T435, balance23_out_gagaaaaaaa(T418, T432, T419, T451, T433, T434, T452, T453, T435, T454)) → BALANCE13_IN_GAAAAA(T420, T451, T452, T453, T455, T454)

The TRS R consists of the following rules:

balance1_in_ga(nil, nil) → balance1_out_ga(nil, nil)
balance1_in_ga(tree(T25, T26, T27), tree(T33, T34, T36)) → U10_ga(T25, T26, T27, T33, T34, T36, balance12_in_gagaaaaaaaaaa(T25, T31, T26, X113, T33, T34, T35, T36, T32, X114, X115, X121, X116))
balance12_in_gagaaaaaaaaaa(nil, .(T107, T108), T107, T108, T109, T110, T111, T112, T113, .(','(T109, -(.(T107, T108), .(T110, T111))), .(','(T112, -(T111, [])), T113)), T113, .(','(nil, -(X200, X200)), X201), X201) → balance12_out_gagaaaaaaaaaa(nil, .(T107, T108), T107, T108, T109, T110, T111, T112, T113, .(','(T109, -(.(T107, T108), .(T110, T111))), .(','(T112, -(T111, [])), T113)), T113, .(','(nil, -(X200, X200)), X201), X201)
balance12_in_gagaaaaaaaaaa(tree(T142, T143, T144), T156, T146, X276, tree(T160, T161, T163), T164, T159, T158, .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157)), X277, X278, X279, X280) → U7_gagaaaaaaaaaa(T142, T143, T144, T156, T146, X276, T160, T161, T163, T164, T159, T158, T162, T157, X277, X278, X279, X280, balance23_in_gagaaaaaaa(T142, T156, T143, X272, .(','(T158, -(T159, [])), .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157))), T157, X273, X274, X279, X275))
balance23_in_gagaaaaaaa(nil, .(T257, T258), T257, T258, T259, T260, T259, T260, .(','(nil, -(T261, T261)), T262), T262) → balance23_out_gagaaaaaaa(nil, .(T257, T258), T257, T258, T259, T260, T259, T260, .(','(nil, -(T261, T261)), T262), T262)
balance23_in_gagaaaaaaa(tree(T291, T292, T293), T305, T295, X433, .(','(tree(T296, T297, T298), -(T299, T300)), T306), .(','(T296, -(T299, .(T297, T302))), .(','(T298, -(T302, T300)), T307)), X434, X435, T308, X436) → U1_gagaaaaaaa(T291, T292, T293, T305, T295, X433, T296, T297, T298, T299, T300, T306, T302, T307, X434, X435, T308, X436, balance23_in_gagaaaaaaa(T291, T305, T292, X429, T306, T307, X430, X431, T308, X432))
balance23_in_gagaaaaaaa(tree(T291, T292, T293), T305, T295, X433, .(','(tree(T296, T297, T298), -(T299, T300)), T306), .(','(T296, -(T299, .(T297, T302))), .(','(T298, -(T302, T300)), T307)), X434, X435, T308, X436) → U2_gagaaaaaaa(T291, T292, T293, T305, T295, X433, T296, T297, T298, T299, T300, T306, T302, T307, X434, X435, T308, X436, balance23_in_gagaaaaaaa(T291, T305, T292, T323, T306, T307, T324, T325, T308, T326))
U2_gagaaaaaaa(T291, T292, T293, T305, T295, X433, T296, T297, T298, T299, T300, T306, T302, T307, X434, X435, T308, X436, balance23_out_gagaaaaaaa(T291, T305, T292, T323, T306, T307, T324, T325, T308, T326)) → U3_gagaaaaaaa(T291, T292, T293, T305, T295, X433, T296, T297, T298, T299, T300, T306, T302, T307, X434, X435, T308, X436, balance23_in_gagaaaaaaa(T293, T323, T295, X433, T324, T325, X434, X435, T326, X436))
U3_gagaaaaaaa(T291, T292, T293, T305, T295, X433, T296, T297, T298, T299, T300, T306, T302, T307, X434, X435, T308, X436, balance23_out_gagaaaaaaa(T293, T323, T295, X433, T324, T325, X434, X435, T326, X436)) → balance23_out_gagaaaaaaa(tree(T291, T292, T293), T305, T295, X433, .(','(tree(T296, T297, T298), -(T299, T300)), T306), .(','(T296, -(T299, .(T297, T302))), .(','(T298, -(T302, T300)), T307)), X434, X435, T308, X436)
U1_gagaaaaaaa(T291, T292, T293, T305, T295, X433, T296, T297, T298, T299, T300, T306, T302, T307, X434, X435, T308, X436, balance23_out_gagaaaaaaa(T291, T305, T292, X429, T306, T307, X430, X431, T308, X432)) → balance23_out_gagaaaaaaa(tree(T291, T292, T293), T305, T295, X433, .(','(tree(T296, T297, T298), -(T299, T300)), T306), .(','(T296, -(T299, .(T297, T302))), .(','(T298, -(T302, T300)), T307)), X434, X435, T308, X436)
U7_gagaaaaaaaaaa(T142, T143, T144, T156, T146, X276, T160, T161, T163, T164, T159, T158, T162, T157, X277, X278, X279, X280, balance23_out_gagaaaaaaa(T142, T156, T143, X272, .(','(T158, -(T159, [])), .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157))), T157, X273, X274, X279, X275)) → balance12_out_gagaaaaaaaaaa(tree(T142, T143, T144), T156, T146, X276, tree(T160, T161, T163), T164, T159, T158, .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157)), X277, X278, X279, X280)
balance12_in_gagaaaaaaaaaa(tree(T142, T143, T144), T156, T146, X276, tree(T160, T161, T163), T164, T159, T158, .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157)), X277, X278, T190, X280) → U8_gagaaaaaaaaaa(T142, T143, T144, T156, T146, X276, T160, T161, T163, T164, T159, T158, T162, T157, X277, X278, T190, X280, balance23_in_gagaaaaaaa(T142, T156, T143, T187, .(','(T158, -(T159, [])), .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157))), T157, T188, T189, T190, T191))
U8_gagaaaaaaaaaa(T142, T143, T144, T156, T146, X276, T160, T161, T163, T164, T159, T158, T162, T157, X277, X278, T190, X280, balance23_out_gagaaaaaaa(T142, T156, T143, T187, .(','(T158, -(T159, [])), .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157))), T157, T188, T189, T190, T191)) → U9_gagaaaaaaaaaa(T142, T143, T144, T156, T146, X276, T160, T161, T163, T164, T159, T158, T162, T157, X277, X278, T190, X280, balance23_in_gagaaaaaaa(T144, T187, T146, X276, T188, T189, X277, X278, T191, X280))
U9_gagaaaaaaaaaa(T142, T143, T144, T156, T146, X276, T160, T161, T163, T164, T159, T158, T162, T157, X277, X278, T190, X280, balance23_out_gagaaaaaaa(T144, T187, T146, X276, T188, T189, X277, X278, T191, X280)) → balance12_out_gagaaaaaaaaaa(tree(T142, T143, T144), T156, T146, X276, tree(T160, T161, T163), T164, T159, T158, .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157)), X277, X278, T190, X280)
U10_ga(T25, T26, T27, T33, T34, T36, balance12_out_gagaaaaaaaaaa(T25, T31, T26, X113, T33, T34, T35, T36, T32, X114, X115, X121, X116)) → balance1_out_ga(tree(T25, T26, T27), tree(T33, T34, T36))
balance1_in_ga(tree(T25, T26, T27), tree(T33, T34, T36)) → U11_ga(T25, T26, T27, T33, T34, T36, balance12_in_gagaaaaaaaaaa(T25, T31, T26, T53, T33, T34, T35, T36, T32, T54, T55, T56, T57))
U11_ga(T25, T26, T27, T33, T34, T36, balance12_out_gagaaaaaaaaaa(T25, T31, T26, T53, T33, T34, T35, T36, T32, T54, T55, T56, T57)) → U12_ga(T25, T26, T27, T33, T34, T36, balance13_in_gaaaaa(T27, T53, T54, T55, T56, T57))
balance13_in_gaaaaa(nil, [], T386, [], T386, .(','(nil, -(T388, T388)), [])) → balance13_out_gaaaaa(nil, [], T386, [], T386, .(','(nil, -(T388, T388)), []))
balance13_in_gaaaaa(tree(T418, T419, T420), T432, .(','(tree(T422, T423, T424), -(T425, T426)), T433), .(','(T422, -(T425, .(T423, T428))), .(','(T424, -(T428, T426)), T434)), T436, T435) → U4_gaaaaa(T418, T419, T420, T432, T422, T423, T424, T425, T426, T433, T428, T434, T436, T435, balance23_in_gagaaaaaaa(T418, T432, T419, X579, T433, T434, X580, X581, T435, X582))
U4_gaaaaa(T418, T419, T420, T432, T422, T423, T424, T425, T426, T433, T428, T434, T436, T435, balance23_out_gagaaaaaaa(T418, T432, T419, X579, T433, T434, X580, X581, T435, X582)) → balance13_out_gaaaaa(tree(T418, T419, T420), T432, .(','(tree(T422, T423, T424), -(T425, T426)), T433), .(','(T422, -(T425, .(T423, T428))), .(','(T424, -(T428, T426)), T434)), T436, T435)
balance13_in_gaaaaa(tree(T418, T419, T420), T432, .(','(tree(T422, T423, T424), -(T425, T426)), T433), .(','(T422, -(T425, .(T423, T428))), .(','(T424, -(T428, T426)), T434)), T455, T435) → U5_gaaaaa(T418, T419, T420, T432, T422, T423, T424, T425, T426, T433, T428, T434, T455, T435, balance23_in_gagaaaaaaa(T418, T432, T419, T451, T433, T434, T452, T453, T435, T454))
U5_gaaaaa(T418, T419, T420, T432, T422, T423, T424, T425, T426, T433, T428, T434, T455, T435, balance23_out_gagaaaaaaa(T418, T432, T419, T451, T433, T434, T452, T453, T435, T454)) → U6_gaaaaa(T418, T419, T420, T432, T422, T423, T424, T425, T426, T433, T428, T434, T455, T435, balance13_in_gaaaaa(T420, T451, T452, T453, T455, T454))
U6_gaaaaa(T418, T419, T420, T432, T422, T423, T424, T425, T426, T433, T428, T434, T455, T435, balance13_out_gaaaaa(T420, T451, T452, T453, T455, T454)) → balance13_out_gaaaaa(tree(T418, T419, T420), T432, .(','(tree(T422, T423, T424), -(T425, T426)), T433), .(','(T422, -(T425, .(T423, T428))), .(','(T424, -(T428, T426)), T434)), T455, T435)
U12_ga(T25, T26, T27, T33, T34, T36, balance13_out_gaaaaa(T27, T53, T54, T55, T56, T57)) → balance1_out_ga(tree(T25, T26, T27), tree(T33, T34, T36))

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

BALANCE23_IN_GAGAAAAAAA(tree(T291, T292, T293), T305, T295, X433, .(','(tree(T296, T297, T298), -(T299, T300)), T306), .(','(T296, -(T299, .(T297, T302))), .(','(T298, -(T302, T300)), T307)), X434, X435, T308, X436) → U2_GAGAAAAAAA(T291, T292, T293, T305, T295, X433, T296, T297, T298, T299, T300, T306, T302, T307, X434, X435, T308, X436, balance23_in_gagaaaaaaa(T291, T305, T292, T323, T306, T307, T324, T325, T308, T326))
U2_GAGAAAAAAA(T291, T292, T293, T305, T295, X433, T296, T297, T298, T299, T300, T306, T302, T307, X434, X435, T308, X436, balance23_out_gagaaaaaaa(T291, T305, T292, T323, T306, T307, T324, T325, T308, T326)) → BALANCE23_IN_GAGAAAAAAA(T293, T323, T295, X433, T324, T325, X434, X435, T326, X436)
BALANCE23_IN_GAGAAAAAAA(tree(T291, T292, T293), T305, T295, X433, .(','(tree(T296, T297, T298), -(T299, T300)), T306), .(','(T296, -(T299, .(T297, T302))), .(','(T298, -(T302, T300)), T307)), X434, X435, T308, X436) → BALANCE23_IN_GAGAAAAAAA(T291, T305, T292, X429, T306, T307, X430, X431, T308, X432)

The TRS R consists of the following rules:

balance1_in_ga(nil, nil) → balance1_out_ga(nil, nil)
balance1_in_ga(tree(T25, T26, T27), tree(T33, T34, T36)) → U10_ga(T25, T26, T27, T33, T34, T36, balance12_in_gagaaaaaaaaaa(T25, T31, T26, X113, T33, T34, T35, T36, T32, X114, X115, X121, X116))
balance12_in_gagaaaaaaaaaa(nil, .(T107, T108), T107, T108, T109, T110, T111, T112, T113, .(','(T109, -(.(T107, T108), .(T110, T111))), .(','(T112, -(T111, [])), T113)), T113, .(','(nil, -(X200, X200)), X201), X201) → balance12_out_gagaaaaaaaaaa(nil, .(T107, T108), T107, T108, T109, T110, T111, T112, T113, .(','(T109, -(.(T107, T108), .(T110, T111))), .(','(T112, -(T111, [])), T113)), T113, .(','(nil, -(X200, X200)), X201), X201)
balance12_in_gagaaaaaaaaaa(tree(T142, T143, T144), T156, T146, X276, tree(T160, T161, T163), T164, T159, T158, .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157)), X277, X278, X279, X280) → U7_gagaaaaaaaaaa(T142, T143, T144, T156, T146, X276, T160, T161, T163, T164, T159, T158, T162, T157, X277, X278, X279, X280, balance23_in_gagaaaaaaa(T142, T156, T143, X272, .(','(T158, -(T159, [])), .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157))), T157, X273, X274, X279, X275))
balance23_in_gagaaaaaaa(nil, .(T257, T258), T257, T258, T259, T260, T259, T260, .(','(nil, -(T261, T261)), T262), T262) → balance23_out_gagaaaaaaa(nil, .(T257, T258), T257, T258, T259, T260, T259, T260, .(','(nil, -(T261, T261)), T262), T262)
balance23_in_gagaaaaaaa(tree(T291, T292, T293), T305, T295, X433, .(','(tree(T296, T297, T298), -(T299, T300)), T306), .(','(T296, -(T299, .(T297, T302))), .(','(T298, -(T302, T300)), T307)), X434, X435, T308, X436) → U1_gagaaaaaaa(T291, T292, T293, T305, T295, X433, T296, T297, T298, T299, T300, T306, T302, T307, X434, X435, T308, X436, balance23_in_gagaaaaaaa(T291, T305, T292, X429, T306, T307, X430, X431, T308, X432))
balance23_in_gagaaaaaaa(tree(T291, T292, T293), T305, T295, X433, .(','(tree(T296, T297, T298), -(T299, T300)), T306), .(','(T296, -(T299, .(T297, T302))), .(','(T298, -(T302, T300)), T307)), X434, X435, T308, X436) → U2_gagaaaaaaa(T291, T292, T293, T305, T295, X433, T296, T297, T298, T299, T300, T306, T302, T307, X434, X435, T308, X436, balance23_in_gagaaaaaaa(T291, T305, T292, T323, T306, T307, T324, T325, T308, T326))
U2_gagaaaaaaa(T291, T292, T293, T305, T295, X433, T296, T297, T298, T299, T300, T306, T302, T307, X434, X435, T308, X436, balance23_out_gagaaaaaaa(T291, T305, T292, T323, T306, T307, T324, T325, T308, T326)) → U3_gagaaaaaaa(T291, T292, T293, T305, T295, X433, T296, T297, T298, T299, T300, T306, T302, T307, X434, X435, T308, X436, balance23_in_gagaaaaaaa(T293, T323, T295, X433, T324, T325, X434, X435, T326, X436))
U3_gagaaaaaaa(T291, T292, T293, T305, T295, X433, T296, T297, T298, T299, T300, T306, T302, T307, X434, X435, T308, X436, balance23_out_gagaaaaaaa(T293, T323, T295, X433, T324, T325, X434, X435, T326, X436)) → balance23_out_gagaaaaaaa(tree(T291, T292, T293), T305, T295, X433, .(','(tree(T296, T297, T298), -(T299, T300)), T306), .(','(T296, -(T299, .(T297, T302))), .(','(T298, -(T302, T300)), T307)), X434, X435, T308, X436)
U1_gagaaaaaaa(T291, T292, T293, T305, T295, X433, T296, T297, T298, T299, T300, T306, T302, T307, X434, X435, T308, X436, balance23_out_gagaaaaaaa(T291, T305, T292, X429, T306, T307, X430, X431, T308, X432)) → balance23_out_gagaaaaaaa(tree(T291, T292, T293), T305, T295, X433, .(','(tree(T296, T297, T298), -(T299, T300)), T306), .(','(T296, -(T299, .(T297, T302))), .(','(T298, -(T302, T300)), T307)), X434, X435, T308, X436)
U7_gagaaaaaaaaaa(T142, T143, T144, T156, T146, X276, T160, T161, T163, T164, T159, T158, T162, T157, X277, X278, X279, X280, balance23_out_gagaaaaaaa(T142, T156, T143, X272, .(','(T158, -(T159, [])), .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157))), T157, X273, X274, X279, X275)) → balance12_out_gagaaaaaaaaaa(tree(T142, T143, T144), T156, T146, X276, tree(T160, T161, T163), T164, T159, T158, .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157)), X277, X278, X279, X280)
balance12_in_gagaaaaaaaaaa(tree(T142, T143, T144), T156, T146, X276, tree(T160, T161, T163), T164, T159, T158, .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157)), X277, X278, T190, X280) → U8_gagaaaaaaaaaa(T142, T143, T144, T156, T146, X276, T160, T161, T163, T164, T159, T158, T162, T157, X277, X278, T190, X280, balance23_in_gagaaaaaaa(T142, T156, T143, T187, .(','(T158, -(T159, [])), .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157))), T157, T188, T189, T190, T191))
U8_gagaaaaaaaaaa(T142, T143, T144, T156, T146, X276, T160, T161, T163, T164, T159, T158, T162, T157, X277, X278, T190, X280, balance23_out_gagaaaaaaa(T142, T156, T143, T187, .(','(T158, -(T159, [])), .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157))), T157, T188, T189, T190, T191)) → U9_gagaaaaaaaaaa(T142, T143, T144, T156, T146, X276, T160, T161, T163, T164, T159, T158, T162, T157, X277, X278, T190, X280, balance23_in_gagaaaaaaa(T144, T187, T146, X276, T188, T189, X277, X278, T191, X280))
U9_gagaaaaaaaaaa(T142, T143, T144, T156, T146, X276, T160, T161, T163, T164, T159, T158, T162, T157, X277, X278, T190, X280, balance23_out_gagaaaaaaa(T144, T187, T146, X276, T188, T189, X277, X278, T191, X280)) → balance12_out_gagaaaaaaaaaa(tree(T142, T143, T144), T156, T146, X276, tree(T160, T161, T163), T164, T159, T158, .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157)), X277, X278, T190, X280)
U10_ga(T25, T26, T27, T33, T34, T36, balance12_out_gagaaaaaaaaaa(T25, T31, T26, X113, T33, T34, T35, T36, T32, X114, X115, X121, X116)) → balance1_out_ga(tree(T25, T26, T27), tree(T33, T34, T36))
balance1_in_ga(tree(T25, T26, T27), tree(T33, T34, T36)) → U11_ga(T25, T26, T27, T33, T34, T36, balance12_in_gagaaaaaaaaaa(T25, T31, T26, T53, T33, T34, T35, T36, T32, T54, T55, T56, T57))
U11_ga(T25, T26, T27, T33, T34, T36, balance12_out_gagaaaaaaaaaa(T25, T31, T26, T53, T33, T34, T35, T36, T32, T54, T55, T56, T57)) → U12_ga(T25, T26, T27, T33, T34, T36, balance13_in_gaaaaa(T27, T53, T54, T55, T56, T57))
balance13_in_gaaaaa(nil, [], T386, [], T386, .(','(nil, -(T388, T388)), [])) → balance13_out_gaaaaa(nil, [], T386, [], T386, .(','(nil, -(T388, T388)), []))
balance13_in_gaaaaa(tree(T418, T419, T420), T432, .(','(tree(T422, T423, T424), -(T425, T426)), T433), .(','(T422, -(T425, .(T423, T428))), .(','(T424, -(T428, T426)), T434)), T436, T435) → U4_gaaaaa(T418, T419, T420, T432, T422, T423, T424, T425, T426, T433, T428, T434, T436, T435, balance23_in_gagaaaaaaa(T418, T432, T419, X579, T433, T434, X580, X581, T435, X582))
U4_gaaaaa(T418, T419, T420, T432, T422, T423, T424, T425, T426, T433, T428, T434, T436, T435, balance23_out_gagaaaaaaa(T418, T432, T419, X579, T433, T434, X580, X581, T435, X582)) → balance13_out_gaaaaa(tree(T418, T419, T420), T432, .(','(tree(T422, T423, T424), -(T425, T426)), T433), .(','(T422, -(T425, .(T423, T428))), .(','(T424, -(T428, T426)), T434)), T436, T435)
balance13_in_gaaaaa(tree(T418, T419, T420), T432, .(','(tree(T422, T423, T424), -(T425, T426)), T433), .(','(T422, -(T425, .(T423, T428))), .(','(T424, -(T428, T426)), T434)), T455, T435) → U5_gaaaaa(T418, T419, T420, T432, T422, T423, T424, T425, T426, T433, T428, T434, T455, T435, balance23_in_gagaaaaaaa(T418, T432, T419, T451, T433, T434, T452, T453, T435, T454))
U5_gaaaaa(T418, T419, T420, T432, T422, T423, T424, T425, T426, T433, T428, T434, T455, T435, balance23_out_gagaaaaaaa(T418, T432, T419, T451, T433, T434, T452, T453, T435, T454)) → U6_gaaaaa(T418, T419, T420, T432, T422, T423, T424, T425, T426, T433, T428, T434, T455, T435, balance13_in_gaaaaa(T420, T451, T452, T453, T455, T454))
U6_gaaaaa(T418, T419, T420, T432, T422, T423, T424, T425, T426, T433, T428, T434, T455, T435, balance13_out_gaaaaa(T420, T451, T452, T453, T455, T454)) → balance13_out_gaaaaa(tree(T418, T419, T420), T432, .(','(tree(T422, T423, T424), -(T425, T426)), T433), .(','(T422, -(T425, .(T423, T428))), .(','(T424, -(T428, T426)), T434)), T455, T435)
U12_ga(T25, T26, T27, T33, T34, T36, balance13_out_gaaaaa(T27, T53, T54, T55, T56, T57)) → balance1_out_ga(tree(T25, T26, T27), tree(T33, T34, T36))

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

BALANCE23_IN_GAGAAAAAAA(tree(T291, T292, T293), T305, T295, X433, .(','(tree(T296, T297, T298), -(T299, T300)), T306), .(','(T296, -(T299, .(T297, T302))), .(','(T298, -(T302, T300)), T307)), X434, X435, T308, X436) → U2_GAGAAAAAAA(T291, T292, T293, T305, T295, X433, T296, T297, T298, T299, T300, T306, T302, T307, X434, X435, T308, X436, balance23_in_gagaaaaaaa(T291, T305, T292, T323, T306, T307, T324, T325, T308, T326))
U2_GAGAAAAAAA(T291, T292, T293, T305, T295, X433, T296, T297, T298, T299, T300, T306, T302, T307, X434, X435, T308, X436, balance23_out_gagaaaaaaa(T291, T305, T292, T323, T306, T307, T324, T325, T308, T326)) → BALANCE23_IN_GAGAAAAAAA(T293, T323, T295, X433, T324, T325, X434, X435, T326, X436)
BALANCE23_IN_GAGAAAAAAA(tree(T291, T292, T293), T305, T295, X433, .(','(tree(T296, T297, T298), -(T299, T300)), T306), .(','(T296, -(T299, .(T297, T302))), .(','(T298, -(T302, T300)), T307)), X434, X435, T308, X436) → BALANCE23_IN_GAGAAAAAAA(T291, T305, T292, X429, T306, T307, X430, X431, T308, X432)

The TRS R consists of the following rules:

balance23_in_gagaaaaaaa(nil, .(T257, T258), T257, T258, T259, T260, T259, T260, .(','(nil, -(T261, T261)), T262), T262) → balance23_out_gagaaaaaaa(nil, .(T257, T258), T257, T258, T259, T260, T259, T260, .(','(nil, -(T261, T261)), T262), T262)
balance23_in_gagaaaaaaa(tree(T291, T292, T293), T305, T295, X433, .(','(tree(T296, T297, T298), -(T299, T300)), T306), .(','(T296, -(T299, .(T297, T302))), .(','(T298, -(T302, T300)), T307)), X434, X435, T308, X436) → U1_gagaaaaaaa(T291, T292, T293, T305, T295, X433, T296, T297, T298, T299, T300, T306, T302, T307, X434, X435, T308, X436, balance23_in_gagaaaaaaa(T291, T305, T292, X429, T306, T307, X430, X431, T308, X432))
balance23_in_gagaaaaaaa(tree(T291, T292, T293), T305, T295, X433, .(','(tree(T296, T297, T298), -(T299, T300)), T306), .(','(T296, -(T299, .(T297, T302))), .(','(T298, -(T302, T300)), T307)), X434, X435, T308, X436) → U2_gagaaaaaaa(T291, T292, T293, T305, T295, X433, T296, T297, T298, T299, T300, T306, T302, T307, X434, X435, T308, X436, balance23_in_gagaaaaaaa(T291, T305, T292, T323, T306, T307, T324, T325, T308, T326))
U1_gagaaaaaaa(T291, T292, T293, T305, T295, X433, T296, T297, T298, T299, T300, T306, T302, T307, X434, X435, T308, X436, balance23_out_gagaaaaaaa(T291, T305, T292, X429, T306, T307, X430, X431, T308, X432)) → balance23_out_gagaaaaaaa(tree(T291, T292, T293), T305, T295, X433, .(','(tree(T296, T297, T298), -(T299, T300)), T306), .(','(T296, -(T299, .(T297, T302))), .(','(T298, -(T302, T300)), T307)), X434, X435, T308, X436)
U2_gagaaaaaaa(T291, T292, T293, T305, T295, X433, T296, T297, T298, T299, T300, T306, T302, T307, X434, X435, T308, X436, balance23_out_gagaaaaaaa(T291, T305, T292, T323, T306, T307, T324, T325, T308, T326)) → U3_gagaaaaaaa(T291, T292, T293, T305, T295, X433, T296, T297, T298, T299, T300, T306, T302, T307, X434, X435, T308, X436, balance23_in_gagaaaaaaa(T293, T323, T295, X433, T324, T325, X434, X435, T326, X436))
U3_gagaaaaaaa(T291, T292, T293, T305, T295, X433, T296, T297, T298, T299, T300, T306, T302, T307, X434, X435, T308, X436, balance23_out_gagaaaaaaa(T293, T323, T295, X433, T324, T325, X434, X435, T326, X436)) → balance23_out_gagaaaaaaa(tree(T291, T292, T293), T305, T295, X433, .(','(tree(T296, T297, T298), -(T299, T300)), T306), .(','(T296, -(T299, .(T297, T302))), .(','(T298, -(T302, T300)), T307)), X434, X435, T308, X436)

The argument filtering Pi contains the following mapping:
nil = nil
tree(x1, x2, x3) = tree(x1, x2, x3)
balance23_in_gagaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10) = balance23_in_gagaaaaaaa(x1, x3)
balance23_out_gagaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10) = balance23_out_gagaaaaaaa(x1, x3)
U1_gagaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19) = U1_gagaaaaaaa(x1, x2, x3, x5, x19)
U2_gagaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19) = U2_gagaaaaaaa(x1, x2, x3, x5, x19)
U3_gagaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19) = U3_gagaaaaaaa(x1, x2, x3, x5, x19)
BALANCE23_IN_GAGAAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10) = BALANCE23_IN_GAGAAAAAAA(x1, x3)
U2_GAGAAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19) = U2_GAGAAAAAAA(x1, x2, x3, x5, x19)

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:

BALANCE23_IN_GAGAAAAAAA(tree(T291, T292, T293), T295) → U2_GAGAAAAAAA(T291, T292, T293, T295, balance23_in_gagaaaaaaa(T291, T292))
U2_GAGAAAAAAA(T291, T292, T293, T295, balance23_out_gagaaaaaaa(T291, T292)) → BALANCE23_IN_GAGAAAAAAA(T293, T295)
BALANCE23_IN_GAGAAAAAAA(tree(T291, T292, T293), T295) → BALANCE23_IN_GAGAAAAAAA(T291, T292)

The TRS R consists of the following rules:

balance23_in_gagaaaaaaa(nil, T257) → balance23_out_gagaaaaaaa(nil, T257)
balance23_in_gagaaaaaaa(tree(T291, T292, T293), T295) → U1_gagaaaaaaa(T291, T292, T293, T295, balance23_in_gagaaaaaaa(T291, T292))
balance23_in_gagaaaaaaa(tree(T291, T292, T293), T295) → U2_gagaaaaaaa(T291, T292, T293, T295, balance23_in_gagaaaaaaa(T291, T292))
U1_gagaaaaaaa(T291, T292, T293, T295, balance23_out_gagaaaaaaa(T291, T292)) → balance23_out_gagaaaaaaa(tree(T291, T292, T293), T295)
U2_gagaaaaaaa(T291, T292, T293, T295, balance23_out_gagaaaaaaa(T291, T292)) → U3_gagaaaaaaa(T291, T292, T293, T295, balance23_in_gagaaaaaaa(T293, T295))
U3_gagaaaaaaa(T291, T292, T293, T295, balance23_out_gagaaaaaaa(T293, T295)) → balance23_out_gagaaaaaaa(tree(T291, T292, T293), T295)

The set Q consists of the following terms:

balance23_in_gagaaaaaaa(x0, x1)
U1_gagaaaaaaa(x0, x1, x2, x3, x4)
U2_gagaaaaaaa(x0, x1, x2, x3, x4)
U3_gagaaaaaaa(x0, x1, x2, x3, x4)

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_GAGAAAAAAA(T291, T292, T293, T295, balance23_out_gagaaaaaaa(T291, T292)) → BALANCE23_IN_GAGAAAAAAA(T293, T295)
The graph contains the following edges 3 >= 1, 4 >= 2
BALANCE23_IN_GAGAAAAAAA(tree(T291, T292, T293), T295) → BALANCE23_IN_GAGAAAAAAA(T291, T292)
The graph contains the following edges 1 > 1, 1 > 2
BALANCE23_IN_GAGAAAAAAA(tree(T291, T292, T293), T295) → U2_GAGAAAAAAA(T291, T292, T293, T295, balance23_in_gagaaaaaaa(T291, T292))
The graph contains the following edges 1 > 1, 1 > 2, 1 > 3, 2 >= 4

(15) YES

(16) Obligation:

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

BALANCE13_IN_GAAAAA(tree(T418, T419, T420), T432, .(','(tree(T422, T423, T424), -(T425, T426)), T433), .(','(T422, -(T425, .(T423, T428))), .(','(T424, -(T428, T426)), T434)), T455, T435) → U5_GAAAAA(T418, T419, T420, T432, T422, T423, T424, T425, T426, T433, T428, T434, T455, T435, balance23_in_gagaaaaaaa(T418, T432, T419, T451, T433, T434, T452, T453, T435, T454))
U5_GAAAAA(T418, T419, T420, T432, T422, T423, T424, T425, T426, T433, T428, T434, T455, T435, balance23_out_gagaaaaaaa(T418, T432, T419, T451, T433, T434, T452, T453, T435, T454)) → BALANCE13_IN_GAAAAA(T420, T451, T452, T453, T455, T454)

The TRS R consists of the following rules:

balance1_in_ga(nil, nil) → balance1_out_ga(nil, nil)
balance1_in_ga(tree(T25, T26, T27), tree(T33, T34, T36)) → U10_ga(T25, T26, T27, T33, T34, T36, balance12_in_gagaaaaaaaaaa(T25, T31, T26, X113, T33, T34, T35, T36, T32, X114, X115, X121, X116))
balance12_in_gagaaaaaaaaaa(nil, .(T107, T108), T107, T108, T109, T110, T111, T112, T113, .(','(T109, -(.(T107, T108), .(T110, T111))), .(','(T112, -(T111, [])), T113)), T113, .(','(nil, -(X200, X200)), X201), X201) → balance12_out_gagaaaaaaaaaa(nil, .(T107, T108), T107, T108, T109, T110, T111, T112, T113, .(','(T109, -(.(T107, T108), .(T110, T111))), .(','(T112, -(T111, [])), T113)), T113, .(','(nil, -(X200, X200)), X201), X201)
balance12_in_gagaaaaaaaaaa(tree(T142, T143, T144), T156, T146, X276, tree(T160, T161, T163), T164, T159, T158, .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157)), X277, X278, X279, X280) → U7_gagaaaaaaaaaa(T142, T143, T144, T156, T146, X276, T160, T161, T163, T164, T159, T158, T162, T157, X277, X278, X279, X280, balance23_in_gagaaaaaaa(T142, T156, T143, X272, .(','(T158, -(T159, [])), .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157))), T157, X273, X274, X279, X275))
balance23_in_gagaaaaaaa(nil, .(T257, T258), T257, T258, T259, T260, T259, T260, .(','(nil, -(T261, T261)), T262), T262) → balance23_out_gagaaaaaaa(nil, .(T257, T258), T257, T258, T259, T260, T259, T260, .(','(nil, -(T261, T261)), T262), T262)
balance23_in_gagaaaaaaa(tree(T291, T292, T293), T305, T295, X433, .(','(tree(T296, T297, T298), -(T299, T300)), T306), .(','(T296, -(T299, .(T297, T302))), .(','(T298, -(T302, T300)), T307)), X434, X435, T308, X436) → U1_gagaaaaaaa(T291, T292, T293, T305, T295, X433, T296, T297, T298, T299, T300, T306, T302, T307, X434, X435, T308, X436, balance23_in_gagaaaaaaa(T291, T305, T292, X429, T306, T307, X430, X431, T308, X432))
balance23_in_gagaaaaaaa(tree(T291, T292, T293), T305, T295, X433, .(','(tree(T296, T297, T298), -(T299, T300)), T306), .(','(T296, -(T299, .(T297, T302))), .(','(T298, -(T302, T300)), T307)), X434, X435, T308, X436) → U2_gagaaaaaaa(T291, T292, T293, T305, T295, X433, T296, T297, T298, T299, T300, T306, T302, T307, X434, X435, T308, X436, balance23_in_gagaaaaaaa(T291, T305, T292, T323, T306, T307, T324, T325, T308, T326))
U2_gagaaaaaaa(T291, T292, T293, T305, T295, X433, T296, T297, T298, T299, T300, T306, T302, T307, X434, X435, T308, X436, balance23_out_gagaaaaaaa(T291, T305, T292, T323, T306, T307, T324, T325, T308, T326)) → U3_gagaaaaaaa(T291, T292, T293, T305, T295, X433, T296, T297, T298, T299, T300, T306, T302, T307, X434, X435, T308, X436, balance23_in_gagaaaaaaa(T293, T323, T295, X433, T324, T325, X434, X435, T326, X436))
U3_gagaaaaaaa(T291, T292, T293, T305, T295, X433, T296, T297, T298, T299, T300, T306, T302, T307, X434, X435, T308, X436, balance23_out_gagaaaaaaa(T293, T323, T295, X433, T324, T325, X434, X435, T326, X436)) → balance23_out_gagaaaaaaa(tree(T291, T292, T293), T305, T295, X433, .(','(tree(T296, T297, T298), -(T299, T300)), T306), .(','(T296, -(T299, .(T297, T302))), .(','(T298, -(T302, T300)), T307)), X434, X435, T308, X436)
U1_gagaaaaaaa(T291, T292, T293, T305, T295, X433, T296, T297, T298, T299, T300, T306, T302, T307, X434, X435, T308, X436, balance23_out_gagaaaaaaa(T291, T305, T292, X429, T306, T307, X430, X431, T308, X432)) → balance23_out_gagaaaaaaa(tree(T291, T292, T293), T305, T295, X433, .(','(tree(T296, T297, T298), -(T299, T300)), T306), .(','(T296, -(T299, .(T297, T302))), .(','(T298, -(T302, T300)), T307)), X434, X435, T308, X436)
U7_gagaaaaaaaaaa(T142, T143, T144, T156, T146, X276, T160, T161, T163, T164, T159, T158, T162, T157, X277, X278, X279, X280, balance23_out_gagaaaaaaa(T142, T156, T143, X272, .(','(T158, -(T159, [])), .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157))), T157, X273, X274, X279, X275)) → balance12_out_gagaaaaaaaaaa(tree(T142, T143, T144), T156, T146, X276, tree(T160, T161, T163), T164, T159, T158, .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157)), X277, X278, X279, X280)
balance12_in_gagaaaaaaaaaa(tree(T142, T143, T144), T156, T146, X276, tree(T160, T161, T163), T164, T159, T158, .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157)), X277, X278, T190, X280) → U8_gagaaaaaaaaaa(T142, T143, T144, T156, T146, X276, T160, T161, T163, T164, T159, T158, T162, T157, X277, X278, T190, X280, balance23_in_gagaaaaaaa(T142, T156, T143, T187, .(','(T158, -(T159, [])), .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157))), T157, T188, T189, T190, T191))
U8_gagaaaaaaaaaa(T142, T143, T144, T156, T146, X276, T160, T161, T163, T164, T159, T158, T162, T157, X277, X278, T190, X280, balance23_out_gagaaaaaaa(T142, T156, T143, T187, .(','(T158, -(T159, [])), .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157))), T157, T188, T189, T190, T191)) → U9_gagaaaaaaaaaa(T142, T143, T144, T156, T146, X276, T160, T161, T163, T164, T159, T158, T162, T157, X277, X278, T190, X280, balance23_in_gagaaaaaaa(T144, T187, T146, X276, T188, T189, X277, X278, T191, X280))
U9_gagaaaaaaaaaa(T142, T143, T144, T156, T146, X276, T160, T161, T163, T164, T159, T158, T162, T157, X277, X278, T190, X280, balance23_out_gagaaaaaaa(T144, T187, T146, X276, T188, T189, X277, X278, T191, X280)) → balance12_out_gagaaaaaaaaaa(tree(T142, T143, T144), T156, T146, X276, tree(T160, T161, T163), T164, T159, T158, .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157)), X277, X278, T190, X280)
U10_ga(T25, T26, T27, T33, T34, T36, balance12_out_gagaaaaaaaaaa(T25, T31, T26, X113, T33, T34, T35, T36, T32, X114, X115, X121, X116)) → balance1_out_ga(tree(T25, T26, T27), tree(T33, T34, T36))
balance1_in_ga(tree(T25, T26, T27), tree(T33, T34, T36)) → U11_ga(T25, T26, T27, T33, T34, T36, balance12_in_gagaaaaaaaaaa(T25, T31, T26, T53, T33, T34, T35, T36, T32, T54, T55, T56, T57))
U11_ga(T25, T26, T27, T33, T34, T36, balance12_out_gagaaaaaaaaaa(T25, T31, T26, T53, T33, T34, T35, T36, T32, T54, T55, T56, T57)) → U12_ga(T25, T26, T27, T33, T34, T36, balance13_in_gaaaaa(T27, T53, T54, T55, T56, T57))
balance13_in_gaaaaa(nil, [], T386, [], T386, .(','(nil, -(T388, T388)), [])) → balance13_out_gaaaaa(nil, [], T386, [], T386, .(','(nil, -(T388, T388)), []))
balance13_in_gaaaaa(tree(T418, T419, T420), T432, .(','(tree(T422, T423, T424), -(T425, T426)), T433), .(','(T422, -(T425, .(T423, T428))), .(','(T424, -(T428, T426)), T434)), T436, T435) → U4_gaaaaa(T418, T419, T420, T432, T422, T423, T424, T425, T426, T433, T428, T434, T436, T435, balance23_in_gagaaaaaaa(T418, T432, T419, X579, T433, T434, X580, X581, T435, X582))
U4_gaaaaa(T418, T419, T420, T432, T422, T423, T424, T425, T426, T433, T428, T434, T436, T435, balance23_out_gagaaaaaaa(T418, T432, T419, X579, T433, T434, X580, X581, T435, X582)) → balance13_out_gaaaaa(tree(T418, T419, T420), T432, .(','(tree(T422, T423, T424), -(T425, T426)), T433), .(','(T422, -(T425, .(T423, T428))), .(','(T424, -(T428, T426)), T434)), T436, T435)
balance13_in_gaaaaa(tree(T418, T419, T420), T432, .(','(tree(T422, T423, T424), -(T425, T426)), T433), .(','(T422, -(T425, .(T423, T428))), .(','(T424, -(T428, T426)), T434)), T455, T435) → U5_gaaaaa(T418, T419, T420, T432, T422, T423, T424, T425, T426, T433, T428, T434, T455, T435, balance23_in_gagaaaaaaa(T418, T432, T419, T451, T433, T434, T452, T453, T435, T454))
U5_gaaaaa(T418, T419, T420, T432, T422, T423, T424, T425, T426, T433, T428, T434, T455, T435, balance23_out_gagaaaaaaa(T418, T432, T419, T451, T433, T434, T452, T453, T435, T454)) → U6_gaaaaa(T418, T419, T420, T432, T422, T423, T424, T425, T426, T433, T428, T434, T455, T435, balance13_in_gaaaaa(T420, T451, T452, T453, T455, T454))
U6_gaaaaa(T418, T419, T420, T432, T422, T423, T424, T425, T426, T433, T428, T434, T455, T435, balance13_out_gaaaaa(T420, T451, T452, T453, T455, T454)) → balance13_out_gaaaaa(tree(T418, T419, T420), T432, .(','(tree(T422, T423, T424), -(T425, T426)), T433), .(','(T422, -(T425, .(T423, T428))), .(','(T424, -(T428, T426)), T434)), T455, T435)
U12_ga(T25, T26, T27, T33, T34, T36, balance13_out_gaaaaa(T27, T53, T54, T55, T56, T57)) → balance1_out_ga(tree(T25, T26, T27), tree(T33, T34, T36))

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

BALANCE13_IN_GAAAAA(tree(T418, T419, T420), T432, .(','(tree(T422, T423, T424), -(T425, T426)), T433), .(','(T422, -(T425, .(T423, T428))), .(','(T424, -(T428, T426)), T434)), T455, T435) → U5_GAAAAA(T418, T419, T420, T432, T422, T423, T424, T425, T426, T433, T428, T434, T455, T435, balance23_in_gagaaaaaaa(T418, T432, T419, T451, T433, T434, T452, T453, T435, T454))
U5_GAAAAA(T418, T419, T420, T432, T422, T423, T424, T425, T426, T433, T428, T434, T455, T435, balance23_out_gagaaaaaaa(T418, T432, T419, T451, T433, T434, T452, T453, T435, T454)) → BALANCE13_IN_GAAAAA(T420, T451, T452, T453, T455, T454)

The TRS R consists of the following rules:

balance23_in_gagaaaaaaa(nil, .(T257, T258), T257, T258, T259, T260, T259, T260, .(','(nil, -(T261, T261)), T262), T262) → balance23_out_gagaaaaaaa(nil, .(T257, T258), T257, T258, T259, T260, T259, T260, .(','(nil, -(T261, T261)), T262), T262)
balance23_in_gagaaaaaaa(tree(T291, T292, T293), T305, T295, X433, .(','(tree(T296, T297, T298), -(T299, T300)), T306), .(','(T296, -(T299, .(T297, T302))), .(','(T298, -(T302, T300)), T307)), X434, X435, T308, X436) → U1_gagaaaaaaa(T291, T292, T293, T305, T295, X433, T296, T297, T298, T299, T300, T306, T302, T307, X434, X435, T308, X436, balance23_in_gagaaaaaaa(T291, T305, T292, X429, T306, T307, X430, X431, T308, X432))
balance23_in_gagaaaaaaa(tree(T291, T292, T293), T305, T295, X433, .(','(tree(T296, T297, T298), -(T299, T300)), T306), .(','(T296, -(T299, .(T297, T302))), .(','(T298, -(T302, T300)), T307)), X434, X435, T308, X436) → U2_gagaaaaaaa(T291, T292, T293, T305, T295, X433, T296, T297, T298, T299, T300, T306, T302, T307, X434, X435, T308, X436, balance23_in_gagaaaaaaa(T291, T305, T292, T323, T306, T307, T324, T325, T308, T326))
U1_gagaaaaaaa(T291, T292, T293, T305, T295, X433, T296, T297, T298, T299, T300, T306, T302, T307, X434, X435, T308, X436, balance23_out_gagaaaaaaa(T291, T305, T292, X429, T306, T307, X430, X431, T308, X432)) → balance23_out_gagaaaaaaa(tree(T291, T292, T293), T305, T295, X433, .(','(tree(T296, T297, T298), -(T299, T300)), T306), .(','(T296, -(T299, .(T297, T302))), .(','(T298, -(T302, T300)), T307)), X434, X435, T308, X436)
U2_gagaaaaaaa(T291, T292, T293, T305, T295, X433, T296, T297, T298, T299, T300, T306, T302, T307, X434, X435, T308, X436, balance23_out_gagaaaaaaa(T291, T305, T292, T323, T306, T307, T324, T325, T308, T326)) → U3_gagaaaaaaa(T291, T292, T293, T305, T295, X433, T296, T297, T298, T299, T300, T306, T302, T307, X434, X435, T308, X436, balance23_in_gagaaaaaaa(T293, T323, T295, X433, T324, T325, X434, X435, T326, X436))
U3_gagaaaaaaa(T291, T292, T293, T305, T295, X433, T296, T297, T298, T299, T300, T306, T302, T307, X434, X435, T308, X436, balance23_out_gagaaaaaaa(T293, T323, T295, X433, T324, T325, X434, X435, T326, X436)) → balance23_out_gagaaaaaaa(tree(T291, T292, T293), T305, T295, X433, .(','(tree(T296, T297, T298), -(T299, T300)), T306), .(','(T296, -(T299, .(T297, T302))), .(','(T298, -(T302, T300)), T307)), X434, X435, T308, X436)

The argument filtering Pi contains the following mapping:
nil = nil
tree(x1, x2, x3) = tree(x1, x2, x3)
balance23_in_gagaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10) = balance23_in_gagaaaaaaa(x1, x3)
balance23_out_gagaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10) = balance23_out_gagaaaaaaa(x1, x3)
U1_gagaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19) = U1_gagaaaaaaa(x1, x2, x3, x5, x19)
U2_gagaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19) = U2_gagaaaaaaa(x1, x2, x3, x5, x19)
U3_gagaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19) = U3_gagaaaaaaa(x1, x2, x3, x5, x19)
BALANCE13_IN_GAAAAA(x1, x2, x3, x4, x5, x6) = BALANCE13_IN_GAAAAA(x1)
U5_GAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15) = U5_GAAAAA(x1, x2, x3, x15)

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:

BALANCE13_IN_GAAAAA(tree(T418, T419, T420)) → U5_GAAAAA(T418, T419, T420, balance23_in_gagaaaaaaa(T418, T419))
U5_GAAAAA(T418, T419, T420, balance23_out_gagaaaaaaa(T418, T419)) → BALANCE13_IN_GAAAAA(T420)

The TRS R consists of the following rules:

balance23_in_gagaaaaaaa(nil, T257) → balance23_out_gagaaaaaaa(nil, T257)
balance23_in_gagaaaaaaa(tree(T291, T292, T293), T295) → U1_gagaaaaaaa(T291, T292, T293, T295, balance23_in_gagaaaaaaa(T291, T292))
balance23_in_gagaaaaaaa(tree(T291, T292, T293), T295) → U2_gagaaaaaaa(T291, T292, T293, T295, balance23_in_gagaaaaaaa(T291, T292))
U1_gagaaaaaaa(T291, T292, T293, T295, balance23_out_gagaaaaaaa(T291, T292)) → balance23_out_gagaaaaaaa(tree(T291, T292, T293), T295)
U2_gagaaaaaaa(T291, T292, T293, T295, balance23_out_gagaaaaaaa(T291, T292)) → U3_gagaaaaaaa(T291, T292, T293, T295, balance23_in_gagaaaaaaa(T293, T295))
U3_gagaaaaaaa(T291, T292, T293, T295, balance23_out_gagaaaaaaa(T293, T295)) → balance23_out_gagaaaaaaa(tree(T291, T292, T293), T295)

The set Q consists of the following terms:

balance23_in_gagaaaaaaa(x0, x1)
U1_gagaaaaaaa(x0, x1, x2, x3, x4)
U2_gagaaaaaaa(x0, x1, x2, x3, x4)
U3_gagaaaaaaa(x0, x1, x2, x3, x4)

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_GAAAAA(T418, T419, T420, balance23_out_gagaaaaaaa(T418, T419)) → BALANCE13_IN_GAAAAA(T420)
The graph contains the following edges 3 >= 1
BALANCE13_IN_GAAAAA(tree(T418, T419, T420)) → U5_GAAAAA(T418, T419, T420, balance23_in_gagaaaaaaa(T418, T419))
The graph contains the following edges 1 > 1, 1 > 2, 1 > 3

(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