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

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

(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(a,g).

(1) PrologToDTProblemTransformerProof (SOUND transformation)

Built DT problem from termination graph.

(2) Obligation:

Triples:

balance23(tree(T307, T309, T313), T308, T314, X433, .(','(tree(T298, T299, T300), -(T301, T302)), T310), .(','(T298, -(T301, .(T299, T304))), .(','(T300, -(T304, T302)), T311)), X434, X435, T312, X436) :- balance23(T307, T308, T309, X429, T310, T311, X430, X431, T312, X432).
balance23(tree(T307, T309, T333), T308, T334, X433, .(','(tree(T298, T299, T300), -(T301, T302)), T310), .(','(T298, -(T301, .(T299, T304))), .(','(T300, -(T304, T302)), T311)), X434, X435, T312, X436) :- ','(balancec23(T307, T308, T309, T329, T310, T311, T330, T331, T312, T332), balance23(T333, T329, T334, X433, T330, T331, X434, X435, T332, X436)).
balance13(tree(T440, T442, T446), T441, .(','(tree(T430, T431, T432), -(T433, T434)), T443), .(','(T430, -(T433, .(T431, T436))), .(','(T432, -(T436, T434)), T444)), T447, T445) :- balance23(T440, T441, T442, X579, T443, T444, X580, X581, T445, X582).
balance13(tree(T440, T442, T466), T441, .(','(tree(T430, T431, T432), -(T433, T434)), T443), .(','(T430, -(T433, .(T431, T436))), .(','(T432, -(T436, T434)), T444)), T467, T445) :- ','(balancec23(T440, T441, T442, T462, T443, T444, T463, T464, T445, T465), balance13(T466, T462, T463, T464, T467, T465)).
balance1(tree(tree(T157, T159, T163), T164, T36), tree(tree(T148, T149, T150), T151, T153)) :- balance23(T157, T158, T159, X272, .(','(T153, -(T161, [])), .(','(T148, -(T158, .(T149, T162))), .(','(T150, -(T162, .(T151, T161))), T160))), T160, X273, X274, X279, X275).
balance1(tree(tree(T157, T159, T192), T193, T36), tree(tree(T148, T149, T150), T151, T153)) :- ','(balancec23(T157, T158, T159, T187, .(','(T153, -(T161, [])), .(','(T148, -(T158, .(T149, T162))), .(','(T150, -(T162, .(T151, T161))), T160))), T160, T188, T189, T190, T191), balance23(T192, T187, T193, X276, T188, T189, X277, X278, T191, X280)).
balance1(tree(T31, T33, T58), tree(T28, T29, T30)) :- ','(balancec12(T31, T32, T33, T53, T28, T29, T35, T30, T34, T54, T55, T56, T57), balance13(T58, T53, T54, T55, T56, T57)).

Clauses:

balancec23(nil, .(T259, T260), T259, T260, T261, T262, T261, T262, .(','(nil, -(T263, T263)), T264), T264).
balancec23(tree(T307, T309, T333), T308, T334, X433, .(','(tree(T298, T299, T300), -(T301, T302)), T310), .(','(T298, -(T301, .(T299, T304))), .(','(T300, -(T304, T302)), T311)), X434, X435, T312, X436) :- ','(balancec23(T307, T308, T309, T329, T310, T311, T330, T331, T312, T332), balancec23(T333, T329, T334, X433, T330, T331, X434, X435, T332, X436)).
balancec13(nil, [], T394, [], T394, .(','(nil, -(T396, T396)), [])).
balancec13(tree(T440, T442, T466), T441, .(','(tree(T430, T431, T432), -(T433, T434)), T443), .(','(T430, -(T433, .(T431, T436))), .(','(T432, -(T436, T434)), T444)), T467, T445) :- ','(balancec23(T440, T441, T442, T462, T443, T444, T463, T464, T445, T465), balancec13(T466, T462, T463, T464, T467, T465)).
balancec12(nil, .(T108, T109), T108, T109, T110, T111, T112, T113, T114, .(','(T110, -(.(T108, T109), .(T111, T112))), .(','(T113, -(T112, [])), T114)), T114, .(','(nil, -(X200, X200)), X201), X201).
balancec12(tree(T157, T159, T192), T158, T193, X276, tree(T148, T149, T150), T151, T161, T153, .(','(T148, -(T158, .(T149, T162))), .(','(T150, -(T162, .(T151, T161))), T160)), X277, X278, T190, X280) :- ','(balancec23(T157, T158, T159, T187, .(','(T153, -(T161, [])), .(','(T148, -(T158, .(T149, T162))), .(','(T150, -(T162, .(T151, T161))), T160))), T160, T188, T189, T190, T191), balancec23(T192, T187, T193, X276, T188, T189, X277, X278, T191, X280)).

Afs:

balance1(x1, x2)  =  balance1(x2)

(3) TriplesToPiDPProof (SOUND transformation)

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

BALANCE1_IN_AG(tree(tree(T157, T159, T163), T164, T36), tree(tree(T148, T149, T150), T151, T153)) → U7_AG(T157, T159, T163, T164, T36, T148, T149, T150, T151, T153, balance23_in_aaaaaaaaaa(T157, T158, T159, X272, .(','(T153, -(T161, [])), .(','(T148, -(T158, .(T149, T162))), .(','(T150, -(T162, .(T151, T161))), T160))), T160, X273, X274, X279, X275))
BALANCE1_IN_AG(tree(tree(T157, T159, T163), T164, T36), tree(tree(T148, T149, T150), T151, T153)) → BALANCE23_IN_AAAAAAAAAA(T157, T158, T159, X272, .(','(T153, -(T161, [])), .(','(T148, -(T158, .(T149, T162))), .(','(T150, -(T162, .(T151, T161))), T160))), T160, X273, X274, X279, X275)
BALANCE23_IN_AAAAAAAAAA(tree(T307, T309, T313), T308, T314, X433, .(','(tree(T298, T299, T300), -(T301, T302)), T310), .(','(T298, -(T301, .(T299, T304))), .(','(T300, -(T304, T302)), T311)), X434, X435, T312, X436) → U1_AAAAAAAAAA(T307, T309, T313, T308, T314, X433, T298, T299, T300, T301, T302, T310, T304, T311, X434, X435, T312, X436, balance23_in_aaaaaaaaaa(T307, T308, T309, X429, T310, T311, X430, X431, T312, X432))
BALANCE23_IN_AAAAAAAAAA(tree(T307, T309, T313), T308, T314, X433, .(','(tree(T298, T299, T300), -(T301, T302)), T310), .(','(T298, -(T301, .(T299, T304))), .(','(T300, -(T304, T302)), T311)), X434, X435, T312, X436) → BALANCE23_IN_AAAAAAAAAA(T307, T308, T309, X429, T310, T311, X430, X431, T312, X432)
BALANCE23_IN_AAAAAAAAAA(tree(T307, T309, T333), T308, T334, X433, .(','(tree(T298, T299, T300), -(T301, T302)), T310), .(','(T298, -(T301, .(T299, T304))), .(','(T300, -(T304, T302)), T311)), X434, X435, T312, X436) → U2_AAAAAAAAAA(T307, T309, T333, T308, T334, X433, T298, T299, T300, T301, T302, T310, T304, T311, X434, X435, T312, X436, balancec23_in_aaaaaaaaaa(T307, T308, T309, T329, T310, T311, T330, T331, T312, T332))
U2_AAAAAAAAAA(T307, T309, T333, T308, T334, X433, T298, T299, T300, T301, T302, T310, T304, T311, X434, X435, T312, X436, balancec23_out_aaaaaaaaaa(T307, T308, T309, T329, T310, T311, T330, T331, T312, T332)) → U3_AAAAAAAAAA(T307, T309, T333, T308, T334, X433, T298, T299, T300, T301, T302, T310, T304, T311, X434, X435, T312, X436, balance23_in_aaaaaaaaaa(T333, T329, T334, X433, T330, T331, X434, X435, T332, X436))
U2_AAAAAAAAAA(T307, T309, T333, T308, T334, X433, T298, T299, T300, T301, T302, T310, T304, T311, X434, X435, T312, X436, balancec23_out_aaaaaaaaaa(T307, T308, T309, T329, T310, T311, T330, T331, T312, T332)) → BALANCE23_IN_AAAAAAAAAA(T333, T329, T334, X433, T330, T331, X434, X435, T332, X436)
BALANCE1_IN_AG(tree(tree(T157, T159, T192), T193, T36), tree(tree(T148, T149, T150), T151, T153)) → U8_AG(T157, T159, T192, T193, T36, T148, T149, T150, T151, T153, balancec23_in_aaaaaaaaaa(T157, T158, T159, T187, .(','(T153, -(T161, [])), .(','(T148, -(T158, .(T149, T162))), .(','(T150, -(T162, .(T151, T161))), T160))), T160, T188, T189, T190, T191))
U8_AG(T157, T159, T192, T193, T36, T148, T149, T150, T151, T153, balancec23_out_aaaaaaaaaa(T157, T158, T159, T187, .(','(T153, -(T161, [])), .(','(T148, -(T158, .(T149, T162))), .(','(T150, -(T162, .(T151, T161))), T160))), T160, T188, T189, T190, T191)) → U9_AG(T157, T159, T192, T193, T36, T148, T149, T150, T151, T153, balance23_in_aaaaaaaaaa(T192, T187, T193, X276, T188, T189, X277, X278, T191, X280))
U8_AG(T157, T159, T192, T193, T36, T148, T149, T150, T151, T153, balancec23_out_aaaaaaaaaa(T157, T158, T159, T187, .(','(T153, -(T161, [])), .(','(T148, -(T158, .(T149, T162))), .(','(T150, -(T162, .(T151, T161))), T160))), T160, T188, T189, T190, T191)) → BALANCE23_IN_AAAAAAAAAA(T192, T187, T193, X276, T188, T189, X277, X278, T191, X280)
BALANCE1_IN_AG(tree(T31, T33, T58), tree(T28, T29, T30)) → U10_AG(T31, T33, T58, T28, T29, T30, balancec12_in_aaaaggagaaaaa(T31, T32, T33, T53, T28, T29, T35, T30, T34, T54, T55, T56, T57))
U10_AG(T31, T33, T58, T28, T29, T30, balancec12_out_aaaaggagaaaaa(T31, T32, T33, T53, T28, T29, T35, T30, T34, T54, T55, T56, T57)) → U11_AG(T31, T33, T58, T28, T29, T30, balance13_in_aaaaaa(T58, T53, T54, T55, T56, T57))
U10_AG(T31, T33, T58, T28, T29, T30, balancec12_out_aaaaggagaaaaa(T31, T32, T33, T53, T28, T29, T35, T30, T34, T54, T55, T56, T57)) → BALANCE13_IN_AAAAAA(T58, T53, T54, T55, T56, T57)
BALANCE13_IN_AAAAAA(tree(T440, T442, T446), T441, .(','(tree(T430, T431, T432), -(T433, T434)), T443), .(','(T430, -(T433, .(T431, T436))), .(','(T432, -(T436, T434)), T444)), T447, T445) → U4_AAAAAA(T440, T442, T446, T441, T430, T431, T432, T433, T434, T443, T436, T444, T447, T445, balance23_in_aaaaaaaaaa(T440, T441, T442, X579, T443, T444, X580, X581, T445, X582))
BALANCE13_IN_AAAAAA(tree(T440, T442, T446), T441, .(','(tree(T430, T431, T432), -(T433, T434)), T443), .(','(T430, -(T433, .(T431, T436))), .(','(T432, -(T436, T434)), T444)), T447, T445) → BALANCE23_IN_AAAAAAAAAA(T440, T441, T442, X579, T443, T444, X580, X581, T445, X582)
BALANCE13_IN_AAAAAA(tree(T440, T442, T466), T441, .(','(tree(T430, T431, T432), -(T433, T434)), T443), .(','(T430, -(T433, .(T431, T436))), .(','(T432, -(T436, T434)), T444)), T467, T445) → U5_AAAAAA(T440, T442, T466, T441, T430, T431, T432, T433, T434, T443, T436, T444, T467, T445, balancec23_in_aaaaaaaaaa(T440, T441, T442, T462, T443, T444, T463, T464, T445, T465))
U5_AAAAAA(T440, T442, T466, T441, T430, T431, T432, T433, T434, T443, T436, T444, T467, T445, balancec23_out_aaaaaaaaaa(T440, T441, T442, T462, T443, T444, T463, T464, T445, T465)) → U6_AAAAAA(T440, T442, T466, T441, T430, T431, T432, T433, T434, T443, T436, T444, T467, T445, balance13_in_aaaaaa(T466, T462, T463, T464, T467, T465))
U5_AAAAAA(T440, T442, T466, T441, T430, T431, T432, T433, T434, T443, T436, T444, T467, T445, balancec23_out_aaaaaaaaaa(T440, T441, T442, T462, T443, T444, T463, T464, T445, T465)) → BALANCE13_IN_AAAAAA(T466, T462, T463, T464, T467, T465)

The TRS R consists of the following rules:

balancec23_in_aaaaaaaaaa(nil, .(T259, T260), T259, T260, T261, T262, T261, T262, .(','(nil, -(T263, T263)), T264), T264) → balancec23_out_aaaaaaaaaa(nil, .(T259, T260), T259, T260, T261, T262, T261, T262, .(','(nil, -(T263, T263)), T264), T264)
balancec23_in_aaaaaaaaaa(tree(T307, T309, T333), T308, T334, X433, .(','(tree(T298, T299, T300), -(T301, T302)), T310), .(','(T298, -(T301, .(T299, T304))), .(','(T300, -(T304, T302)), T311)), X434, X435, T312, X436) → U13_aaaaaaaaaa(T307, T309, T333, T308, T334, X433, T298, T299, T300, T301, T302, T310, T304, T311, X434, X435, T312, X436, balancec23_in_aaaaaaaaaa(T307, T308, T309, T329, T310, T311, T330, T331, T312, T332))
U13_aaaaaaaaaa(T307, T309, T333, T308, T334, X433, T298, T299, T300, T301, T302, T310, T304, T311, X434, X435, T312, X436, balancec23_out_aaaaaaaaaa(T307, T308, T309, T329, T310, T311, T330, T331, T312, T332)) → U14_aaaaaaaaaa(T307, T309, T333, T308, T334, X433, T298, T299, T300, T301, T302, T310, T304, T311, X434, X435, T312, X436, T329, T330, T331, T332, balancec23_in_aaaaaaaaaa(T333, T329, T334, X433, T330, T331, X434, X435, T332, X436))
U14_aaaaaaaaaa(T307, T309, T333, T308, T334, X433, T298, T299, T300, T301, T302, T310, T304, T311, X434, X435, T312, X436, T329, T330, T331, T332, balancec23_out_aaaaaaaaaa(T333, T329, T334, X433, T330, T331, X434, X435, T332, X436)) → balancec23_out_aaaaaaaaaa(tree(T307, T309, T333), T308, T334, X433, .(','(tree(T298, T299, T300), -(T301, T302)), T310), .(','(T298, -(T301, .(T299, T304))), .(','(T300, -(T304, T302)), T311)), X434, X435, T312, X436)
balancec12_in_aaaaggagaaaaa(nil, .(T108, T109), T108, T109, T110, T111, T112, T113, T114, .(','(T110, -(.(T108, T109), .(T111, T112))), .(','(T113, -(T112, [])), T114)), T114, .(','(nil, -(X200, X200)), X201), X201) → balancec12_out_aaaaggagaaaaa(nil, .(T108, T109), T108, T109, T110, T111, T112, T113, T114, .(','(T110, -(.(T108, T109), .(T111, T112))), .(','(T113, -(T112, [])), T114)), T114, .(','(nil, -(X200, X200)), X201), X201)
balancec12_in_aaaaggagaaaaa(tree(T157, T159, T192), T158, T193, X276, tree(T148, T149, T150), T151, T161, T153, .(','(T148, -(T158, .(T149, T162))), .(','(T150, -(T162, .(T151, T161))), T160)), X277, X278, T190, X280) → U17_aaaaggagaaaaa(T157, T159, T192, T158, T193, X276, T148, T149, T150, T151, T161, T153, T162, T160, X277, X278, T190, X280, balancec23_in_aaaaaaaaaa(T157, T158, T159, T187, .(','(T153, -(T161, [])), .(','(T148, -(T158, .(T149, T162))), .(','(T150, -(T162, .(T151, T161))), T160))), T160, T188, T189, T190, T191))
U17_aaaaggagaaaaa(T157, T159, T192, T158, T193, X276, T148, T149, T150, T151, T161, T153, T162, T160, X277, X278, T190, X280, balancec23_out_aaaaaaaaaa(T157, T158, T159, T187, .(','(T153, -(T161, [])), .(','(T148, -(T158, .(T149, T162))), .(','(T150, -(T162, .(T151, T161))), T160))), T160, T188, T189, T190, T191)) → U18_aaaaggagaaaaa(T157, T159, T192, T158, T193, X276, T148, T149, T150, T151, T161, T153, T162, T160, X277, X278, T190, X280, T187, T188, T189, T191, balancec23_in_aaaaaaaaaa(T192, T187, T193, X276, T188, T189, X277, X278, T191, X280))
U18_aaaaggagaaaaa(T157, T159, T192, T158, T193, X276, T148, T149, T150, T151, T161, T153, T162, T160, X277, X278, T190, X280, T187, T188, T189, T191, balancec23_out_aaaaaaaaaa(T192, T187, T193, X276, T188, T189, X277, X278, T191, X280)) → balancec12_out_aaaaggagaaaaa(tree(T157, T159, T192), T158, T193, X276, tree(T148, T149, T150), T151, T161, T153, .(','(T148, -(T158, .(T149, T162))), .(','(T150, -(T162, .(T151, T161))), T160)), X277, X278, T190, X280)

The argument filtering Pi contains the following mapping:
tree(x1, x2, x3)  =  tree(x1, x2, x3)
balance23_in_aaaaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  balance23_in_aaaaaaaaaa
balancec23_in_aaaaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  balancec23_in_aaaaaaaaaa
balancec23_out_aaaaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  balancec23_out_aaaaaaaaaa
U13_aaaaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19)  =  U13_aaaaaaaaaa(x19)
U14_aaaaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22, x23)  =  U14_aaaaaaaaaa(x23)
balancec12_in_aaaaggagaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13)  =  balancec12_in_aaaaggagaaaaa(x5, x6, x8)
balancec12_out_aaaaggagaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13)  =  balancec12_out_aaaaggagaaaaa(x5, x6, x8)
U17_aaaaggagaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19)  =  U17_aaaaggagaaaaa(x7, x8, x9, x10, x12, x19)
U18_aaaaggagaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22, x23)  =  U18_aaaaggagaaaaa(x7, x8, x9, x10, x12, x23)
balance13_in_aaaaaa(x1, x2, x3, x4, x5, x6)  =  balance13_in_aaaaaa
BALANCE1_IN_AG(x1, x2)  =  BALANCE1_IN_AG(x2)
U7_AG(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11)  =  U7_AG(x6, x7, x8, x9, x10, x11)
BALANCE23_IN_AAAAAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  BALANCE23_IN_AAAAAAAAAA
U1_AAAAAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19)  =  U1_AAAAAAAAAA(x19)
U2_AAAAAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19)  =  U2_AAAAAAAAAA(x19)
U3_AAAAAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19)  =  U3_AAAAAAAAAA(x19)
U8_AG(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11)  =  U8_AG(x6, x7, x8, x9, x10, x11)
U9_AG(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11)  =  U9_AG(x6, x7, x8, x9, x10, x11)
U10_AG(x1, x2, x3, x4, x5, x6, x7)  =  U10_AG(x4, x5, x6, x7)
U11_AG(x1, x2, x3, x4, x5, x6, x7)  =  U11_AG(x4, x5, x6, x7)
BALANCE13_IN_AAAAAA(x1, x2, x3, x4, x5, x6)  =  BALANCE13_IN_AAAAAA
U4_AAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15)  =  U4_AAAAAA(x15)
U5_AAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15)  =  U5_AAAAAA(x15)
U6_AAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15)  =  U6_AAAAAA(x15)

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

Infinitary Constructor Rewriting Termination of PiDP implies Termination of TRIPLES

(4) Obligation:

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

BALANCE1_IN_AG(tree(tree(T157, T159, T163), T164, T36), tree(tree(T148, T149, T150), T151, T153)) → U7_AG(T157, T159, T163, T164, T36, T148, T149, T150, T151, T153, balance23_in_aaaaaaaaaa(T157, T158, T159, X272, .(','(T153, -(T161, [])), .(','(T148, -(T158, .(T149, T162))), .(','(T150, -(T162, .(T151, T161))), T160))), T160, X273, X274, X279, X275))
BALANCE1_IN_AG(tree(tree(T157, T159, T163), T164, T36), tree(tree(T148, T149, T150), T151, T153)) → BALANCE23_IN_AAAAAAAAAA(T157, T158, T159, X272, .(','(T153, -(T161, [])), .(','(T148, -(T158, .(T149, T162))), .(','(T150, -(T162, .(T151, T161))), T160))), T160, X273, X274, X279, X275)
BALANCE23_IN_AAAAAAAAAA(tree(T307, T309, T313), T308, T314, X433, .(','(tree(T298, T299, T300), -(T301, T302)), T310), .(','(T298, -(T301, .(T299, T304))), .(','(T300, -(T304, T302)), T311)), X434, X435, T312, X436) → U1_AAAAAAAAAA(T307, T309, T313, T308, T314, X433, T298, T299, T300, T301, T302, T310, T304, T311, X434, X435, T312, X436, balance23_in_aaaaaaaaaa(T307, T308, T309, X429, T310, T311, X430, X431, T312, X432))
BALANCE23_IN_AAAAAAAAAA(tree(T307, T309, T313), T308, T314, X433, .(','(tree(T298, T299, T300), -(T301, T302)), T310), .(','(T298, -(T301, .(T299, T304))), .(','(T300, -(T304, T302)), T311)), X434, X435, T312, X436) → BALANCE23_IN_AAAAAAAAAA(T307, T308, T309, X429, T310, T311, X430, X431, T312, X432)
BALANCE23_IN_AAAAAAAAAA(tree(T307, T309, T333), T308, T334, X433, .(','(tree(T298, T299, T300), -(T301, T302)), T310), .(','(T298, -(T301, .(T299, T304))), .(','(T300, -(T304, T302)), T311)), X434, X435, T312, X436) → U2_AAAAAAAAAA(T307, T309, T333, T308, T334, X433, T298, T299, T300, T301, T302, T310, T304, T311, X434, X435, T312, X436, balancec23_in_aaaaaaaaaa(T307, T308, T309, T329, T310, T311, T330, T331, T312, T332))
U2_AAAAAAAAAA(T307, T309, T333, T308, T334, X433, T298, T299, T300, T301, T302, T310, T304, T311, X434, X435, T312, X436, balancec23_out_aaaaaaaaaa(T307, T308, T309, T329, T310, T311, T330, T331, T312, T332)) → U3_AAAAAAAAAA(T307, T309, T333, T308, T334, X433, T298, T299, T300, T301, T302, T310, T304, T311, X434, X435, T312, X436, balance23_in_aaaaaaaaaa(T333, T329, T334, X433, T330, T331, X434, X435, T332, X436))
U2_AAAAAAAAAA(T307, T309, T333, T308, T334, X433, T298, T299, T300, T301, T302, T310, T304, T311, X434, X435, T312, X436, balancec23_out_aaaaaaaaaa(T307, T308, T309, T329, T310, T311, T330, T331, T312, T332)) → BALANCE23_IN_AAAAAAAAAA(T333, T329, T334, X433, T330, T331, X434, X435, T332, X436)
BALANCE1_IN_AG(tree(tree(T157, T159, T192), T193, T36), tree(tree(T148, T149, T150), T151, T153)) → U8_AG(T157, T159, T192, T193, T36, T148, T149, T150, T151, T153, balancec23_in_aaaaaaaaaa(T157, T158, T159, T187, .(','(T153, -(T161, [])), .(','(T148, -(T158, .(T149, T162))), .(','(T150, -(T162, .(T151, T161))), T160))), T160, T188, T189, T190, T191))
U8_AG(T157, T159, T192, T193, T36, T148, T149, T150, T151, T153, balancec23_out_aaaaaaaaaa(T157, T158, T159, T187, .(','(T153, -(T161, [])), .(','(T148, -(T158, .(T149, T162))), .(','(T150, -(T162, .(T151, T161))), T160))), T160, T188, T189, T190, T191)) → U9_AG(T157, T159, T192, T193, T36, T148, T149, T150, T151, T153, balance23_in_aaaaaaaaaa(T192, T187, T193, X276, T188, T189, X277, X278, T191, X280))
U8_AG(T157, T159, T192, T193, T36, T148, T149, T150, T151, T153, balancec23_out_aaaaaaaaaa(T157, T158, T159, T187, .(','(T153, -(T161, [])), .(','(T148, -(T158, .(T149, T162))), .(','(T150, -(T162, .(T151, T161))), T160))), T160, T188, T189, T190, T191)) → BALANCE23_IN_AAAAAAAAAA(T192, T187, T193, X276, T188, T189, X277, X278, T191, X280)
BALANCE1_IN_AG(tree(T31, T33, T58), tree(T28, T29, T30)) → U10_AG(T31, T33, T58, T28, T29, T30, balancec12_in_aaaaggagaaaaa(T31, T32, T33, T53, T28, T29, T35, T30, T34, T54, T55, T56, T57))
U10_AG(T31, T33, T58, T28, T29, T30, balancec12_out_aaaaggagaaaaa(T31, T32, T33, T53, T28, T29, T35, T30, T34, T54, T55, T56, T57)) → U11_AG(T31, T33, T58, T28, T29, T30, balance13_in_aaaaaa(T58, T53, T54, T55, T56, T57))
U10_AG(T31, T33, T58, T28, T29, T30, balancec12_out_aaaaggagaaaaa(T31, T32, T33, T53, T28, T29, T35, T30, T34, T54, T55, T56, T57)) → BALANCE13_IN_AAAAAA(T58, T53, T54, T55, T56, T57)
BALANCE13_IN_AAAAAA(tree(T440, T442, T446), T441, .(','(tree(T430, T431, T432), -(T433, T434)), T443), .(','(T430, -(T433, .(T431, T436))), .(','(T432, -(T436, T434)), T444)), T447, T445) → U4_AAAAAA(T440, T442, T446, T441, T430, T431, T432, T433, T434, T443, T436, T444, T447, T445, balance23_in_aaaaaaaaaa(T440, T441, T442, X579, T443, T444, X580, X581, T445, X582))
BALANCE13_IN_AAAAAA(tree(T440, T442, T446), T441, .(','(tree(T430, T431, T432), -(T433, T434)), T443), .(','(T430, -(T433, .(T431, T436))), .(','(T432, -(T436, T434)), T444)), T447, T445) → BALANCE23_IN_AAAAAAAAAA(T440, T441, T442, X579, T443, T444, X580, X581, T445, X582)
BALANCE13_IN_AAAAAA(tree(T440, T442, T466), T441, .(','(tree(T430, T431, T432), -(T433, T434)), T443), .(','(T430, -(T433, .(T431, T436))), .(','(T432, -(T436, T434)), T444)), T467, T445) → U5_AAAAAA(T440, T442, T466, T441, T430, T431, T432, T433, T434, T443, T436, T444, T467, T445, balancec23_in_aaaaaaaaaa(T440, T441, T442, T462, T443, T444, T463, T464, T445, T465))
U5_AAAAAA(T440, T442, T466, T441, T430, T431, T432, T433, T434, T443, T436, T444, T467, T445, balancec23_out_aaaaaaaaaa(T440, T441, T442, T462, T443, T444, T463, T464, T445, T465)) → U6_AAAAAA(T440, T442, T466, T441, T430, T431, T432, T433, T434, T443, T436, T444, T467, T445, balance13_in_aaaaaa(T466, T462, T463, T464, T467, T465))
U5_AAAAAA(T440, T442, T466, T441, T430, T431, T432, T433, T434, T443, T436, T444, T467, T445, balancec23_out_aaaaaaaaaa(T440, T441, T442, T462, T443, T444, T463, T464, T445, T465)) → BALANCE13_IN_AAAAAA(T466, T462, T463, T464, T467, T465)

The TRS R consists of the following rules:

balancec23_in_aaaaaaaaaa(nil, .(T259, T260), T259, T260, T261, T262, T261, T262, .(','(nil, -(T263, T263)), T264), T264) → balancec23_out_aaaaaaaaaa(nil, .(T259, T260), T259, T260, T261, T262, T261, T262, .(','(nil, -(T263, T263)), T264), T264)
balancec23_in_aaaaaaaaaa(tree(T307, T309, T333), T308, T334, X433, .(','(tree(T298, T299, T300), -(T301, T302)), T310), .(','(T298, -(T301, .(T299, T304))), .(','(T300, -(T304, T302)), T311)), X434, X435, T312, X436) → U13_aaaaaaaaaa(T307, T309, T333, T308, T334, X433, T298, T299, T300, T301, T302, T310, T304, T311, X434, X435, T312, X436, balancec23_in_aaaaaaaaaa(T307, T308, T309, T329, T310, T311, T330, T331, T312, T332))
U13_aaaaaaaaaa(T307, T309, T333, T308, T334, X433, T298, T299, T300, T301, T302, T310, T304, T311, X434, X435, T312, X436, balancec23_out_aaaaaaaaaa(T307, T308, T309, T329, T310, T311, T330, T331, T312, T332)) → U14_aaaaaaaaaa(T307, T309, T333, T308, T334, X433, T298, T299, T300, T301, T302, T310, T304, T311, X434, X435, T312, X436, T329, T330, T331, T332, balancec23_in_aaaaaaaaaa(T333, T329, T334, X433, T330, T331, X434, X435, T332, X436))
U14_aaaaaaaaaa(T307, T309, T333, T308, T334, X433, T298, T299, T300, T301, T302, T310, T304, T311, X434, X435, T312, X436, T329, T330, T331, T332, balancec23_out_aaaaaaaaaa(T333, T329, T334, X433, T330, T331, X434, X435, T332, X436)) → balancec23_out_aaaaaaaaaa(tree(T307, T309, T333), T308, T334, X433, .(','(tree(T298, T299, T300), -(T301, T302)), T310), .(','(T298, -(T301, .(T299, T304))), .(','(T300, -(T304, T302)), T311)), X434, X435, T312, X436)
balancec12_in_aaaaggagaaaaa(nil, .(T108, T109), T108, T109, T110, T111, T112, T113, T114, .(','(T110, -(.(T108, T109), .(T111, T112))), .(','(T113, -(T112, [])), T114)), T114, .(','(nil, -(X200, X200)), X201), X201) → balancec12_out_aaaaggagaaaaa(nil, .(T108, T109), T108, T109, T110, T111, T112, T113, T114, .(','(T110, -(.(T108, T109), .(T111, T112))), .(','(T113, -(T112, [])), T114)), T114, .(','(nil, -(X200, X200)), X201), X201)
balancec12_in_aaaaggagaaaaa(tree(T157, T159, T192), T158, T193, X276, tree(T148, T149, T150), T151, T161, T153, .(','(T148, -(T158, .(T149, T162))), .(','(T150, -(T162, .(T151, T161))), T160)), X277, X278, T190, X280) → U17_aaaaggagaaaaa(T157, T159, T192, T158, T193, X276, T148, T149, T150, T151, T161, T153, T162, T160, X277, X278, T190, X280, balancec23_in_aaaaaaaaaa(T157, T158, T159, T187, .(','(T153, -(T161, [])), .(','(T148, -(T158, .(T149, T162))), .(','(T150, -(T162, .(T151, T161))), T160))), T160, T188, T189, T190, T191))
U17_aaaaggagaaaaa(T157, T159, T192, T158, T193, X276, T148, T149, T150, T151, T161, T153, T162, T160, X277, X278, T190, X280, balancec23_out_aaaaaaaaaa(T157, T158, T159, T187, .(','(T153, -(T161, [])), .(','(T148, -(T158, .(T149, T162))), .(','(T150, -(T162, .(T151, T161))), T160))), T160, T188, T189, T190, T191)) → U18_aaaaggagaaaaa(T157, T159, T192, T158, T193, X276, T148, T149, T150, T151, T161, T153, T162, T160, X277, X278, T190, X280, T187, T188, T189, T191, balancec23_in_aaaaaaaaaa(T192, T187, T193, X276, T188, T189, X277, X278, T191, X280))
U18_aaaaggagaaaaa(T157, T159, T192, T158, T193, X276, T148, T149, T150, T151, T161, T153, T162, T160, X277, X278, T190, X280, T187, T188, T189, T191, balancec23_out_aaaaaaaaaa(T192, T187, T193, X276, T188, T189, X277, X278, T191, X280)) → balancec12_out_aaaaggagaaaaa(tree(T157, T159, T192), T158, T193, X276, tree(T148, T149, T150), T151, T161, T153, .(','(T148, -(T158, .(T149, T162))), .(','(T150, -(T162, .(T151, T161))), T160)), X277, X278, T190, X280)

The argument filtering Pi contains the following mapping:
tree(x1, x2, x3)  =  tree(x1, x2, x3)
balance23_in_aaaaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  balance23_in_aaaaaaaaaa
balancec23_in_aaaaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  balancec23_in_aaaaaaaaaa
balancec23_out_aaaaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  balancec23_out_aaaaaaaaaa
U13_aaaaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19)  =  U13_aaaaaaaaaa(x19)
U14_aaaaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22, x23)  =  U14_aaaaaaaaaa(x23)
balancec12_in_aaaaggagaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13)  =  balancec12_in_aaaaggagaaaaa(x5, x6, x8)
balancec12_out_aaaaggagaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13)  =  balancec12_out_aaaaggagaaaaa(x5, x6, x8)
U17_aaaaggagaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19)  =  U17_aaaaggagaaaaa(x7, x8, x9, x10, x12, x19)
U18_aaaaggagaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22, x23)  =  U18_aaaaggagaaaaa(x7, x8, x9, x10, x12, x23)
balance13_in_aaaaaa(x1, x2, x3, x4, x5, x6)  =  balance13_in_aaaaaa
BALANCE1_IN_AG(x1, x2)  =  BALANCE1_IN_AG(x2)
U7_AG(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11)  =  U7_AG(x6, x7, x8, x9, x10, x11)
BALANCE23_IN_AAAAAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  BALANCE23_IN_AAAAAAAAAA
U1_AAAAAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19)  =  U1_AAAAAAAAAA(x19)
U2_AAAAAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19)  =  U2_AAAAAAAAAA(x19)
U3_AAAAAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19)  =  U3_AAAAAAAAAA(x19)
U8_AG(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11)  =  U8_AG(x6, x7, x8, x9, x10, x11)
U9_AG(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11)  =  U9_AG(x6, x7, x8, x9, x10, x11)
U10_AG(x1, x2, x3, x4, x5, x6, x7)  =  U10_AG(x4, x5, x6, x7)
U11_AG(x1, x2, x3, x4, x5, x6, x7)  =  U11_AG(x4, x5, x6, x7)
BALANCE13_IN_AAAAAA(x1, x2, x3, x4, x5, x6)  =  BALANCE13_IN_AAAAAA
U4_AAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15)  =  U4_AAAAAA(x15)
U5_AAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15)  =  U5_AAAAAA(x15)
U6_AAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15)  =  U6_AAAAAA(x15)

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

(5) DependencyGraphProof (EQUIVALENT transformation)

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

(6) Complex Obligation (AND)

(7) Obligation:

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

BALANCE23_IN_AAAAAAAAAA(tree(T307, T309, T333), T308, T334, X433, .(','(tree(T298, T299, T300), -(T301, T302)), T310), .(','(T298, -(T301, .(T299, T304))), .(','(T300, -(T304, T302)), T311)), X434, X435, T312, X436) → U2_AAAAAAAAAA(T307, T309, T333, T308, T334, X433, T298, T299, T300, T301, T302, T310, T304, T311, X434, X435, T312, X436, balancec23_in_aaaaaaaaaa(T307, T308, T309, T329, T310, T311, T330, T331, T312, T332))
U2_AAAAAAAAAA(T307, T309, T333, T308, T334, X433, T298, T299, T300, T301, T302, T310, T304, T311, X434, X435, T312, X436, balancec23_out_aaaaaaaaaa(T307, T308, T309, T329, T310, T311, T330, T331, T312, T332)) → BALANCE23_IN_AAAAAAAAAA(T333, T329, T334, X433, T330, T331, X434, X435, T332, X436)
BALANCE23_IN_AAAAAAAAAA(tree(T307, T309, T313), T308, T314, X433, .(','(tree(T298, T299, T300), -(T301, T302)), T310), .(','(T298, -(T301, .(T299, T304))), .(','(T300, -(T304, T302)), T311)), X434, X435, T312, X436) → BALANCE23_IN_AAAAAAAAAA(T307, T308, T309, X429, T310, T311, X430, X431, T312, X432)

The TRS R consists of the following rules:

balancec23_in_aaaaaaaaaa(nil, .(T259, T260), T259, T260, T261, T262, T261, T262, .(','(nil, -(T263, T263)), T264), T264) → balancec23_out_aaaaaaaaaa(nil, .(T259, T260), T259, T260, T261, T262, T261, T262, .(','(nil, -(T263, T263)), T264), T264)
balancec23_in_aaaaaaaaaa(tree(T307, T309, T333), T308, T334, X433, .(','(tree(T298, T299, T300), -(T301, T302)), T310), .(','(T298, -(T301, .(T299, T304))), .(','(T300, -(T304, T302)), T311)), X434, X435, T312, X436) → U13_aaaaaaaaaa(T307, T309, T333, T308, T334, X433, T298, T299, T300, T301, T302, T310, T304, T311, X434, X435, T312, X436, balancec23_in_aaaaaaaaaa(T307, T308, T309, T329, T310, T311, T330, T331, T312, T332))
U13_aaaaaaaaaa(T307, T309, T333, T308, T334, X433, T298, T299, T300, T301, T302, T310, T304, T311, X434, X435, T312, X436, balancec23_out_aaaaaaaaaa(T307, T308, T309, T329, T310, T311, T330, T331, T312, T332)) → U14_aaaaaaaaaa(T307, T309, T333, T308, T334, X433, T298, T299, T300, T301, T302, T310, T304, T311, X434, X435, T312, X436, T329, T330, T331, T332, balancec23_in_aaaaaaaaaa(T333, T329, T334, X433, T330, T331, X434, X435, T332, X436))
U14_aaaaaaaaaa(T307, T309, T333, T308, T334, X433, T298, T299, T300, T301, T302, T310, T304, T311, X434, X435, T312, X436, T329, T330, T331, T332, balancec23_out_aaaaaaaaaa(T333, T329, T334, X433, T330, T331, X434, X435, T332, X436)) → balancec23_out_aaaaaaaaaa(tree(T307, T309, T333), T308, T334, X433, .(','(tree(T298, T299, T300), -(T301, T302)), T310), .(','(T298, -(T301, .(T299, T304))), .(','(T300, -(T304, T302)), T311)), X434, X435, T312, X436)
balancec12_in_aaaaggagaaaaa(nil, .(T108, T109), T108, T109, T110, T111, T112, T113, T114, .(','(T110, -(.(T108, T109), .(T111, T112))), .(','(T113, -(T112, [])), T114)), T114, .(','(nil, -(X200, X200)), X201), X201) → balancec12_out_aaaaggagaaaaa(nil, .(T108, T109), T108, T109, T110, T111, T112, T113, T114, .(','(T110, -(.(T108, T109), .(T111, T112))), .(','(T113, -(T112, [])), T114)), T114, .(','(nil, -(X200, X200)), X201), X201)
balancec12_in_aaaaggagaaaaa(tree(T157, T159, T192), T158, T193, X276, tree(T148, T149, T150), T151, T161, T153, .(','(T148, -(T158, .(T149, T162))), .(','(T150, -(T162, .(T151, T161))), T160)), X277, X278, T190, X280) → U17_aaaaggagaaaaa(T157, T159, T192, T158, T193, X276, T148, T149, T150, T151, T161, T153, T162, T160, X277, X278, T190, X280, balancec23_in_aaaaaaaaaa(T157, T158, T159, T187, .(','(T153, -(T161, [])), .(','(T148, -(T158, .(T149, T162))), .(','(T150, -(T162, .(T151, T161))), T160))), T160, T188, T189, T190, T191))
U17_aaaaggagaaaaa(T157, T159, T192, T158, T193, X276, T148, T149, T150, T151, T161, T153, T162, T160, X277, X278, T190, X280, balancec23_out_aaaaaaaaaa(T157, T158, T159, T187, .(','(T153, -(T161, [])), .(','(T148, -(T158, .(T149, T162))), .(','(T150, -(T162, .(T151, T161))), T160))), T160, T188, T189, T190, T191)) → U18_aaaaggagaaaaa(T157, T159, T192, T158, T193, X276, T148, T149, T150, T151, T161, T153, T162, T160, X277, X278, T190, X280, T187, T188, T189, T191, balancec23_in_aaaaaaaaaa(T192, T187, T193, X276, T188, T189, X277, X278, T191, X280))
U18_aaaaggagaaaaa(T157, T159, T192, T158, T193, X276, T148, T149, T150, T151, T161, T153, T162, T160, X277, X278, T190, X280, T187, T188, T189, T191, balancec23_out_aaaaaaaaaa(T192, T187, T193, X276, T188, T189, X277, X278, T191, X280)) → balancec12_out_aaaaggagaaaaa(tree(T157, T159, T192), T158, T193, X276, tree(T148, T149, T150), T151, T161, T153, .(','(T148, -(T158, .(T149, T162))), .(','(T150, -(T162, .(T151, T161))), T160)), X277, X278, T190, X280)

The argument filtering Pi contains the following mapping:
tree(x1, x2, x3)  =  tree(x1, x2, x3)
balancec23_in_aaaaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  balancec23_in_aaaaaaaaaa
balancec23_out_aaaaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  balancec23_out_aaaaaaaaaa
U13_aaaaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19)  =  U13_aaaaaaaaaa(x19)
U14_aaaaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22, x23)  =  U14_aaaaaaaaaa(x23)
balancec12_in_aaaaggagaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13)  =  balancec12_in_aaaaggagaaaaa(x5, x6, x8)
balancec12_out_aaaaggagaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13)  =  balancec12_out_aaaaggagaaaaa(x5, x6, x8)
U17_aaaaggagaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19)  =  U17_aaaaggagaaaaa(x7, x8, x9, x10, x12, x19)
U18_aaaaggagaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22, x23)  =  U18_aaaaggagaaaaa(x7, x8, x9, x10, x12, x23)
BALANCE23_IN_AAAAAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  BALANCE23_IN_AAAAAAAAAA
U2_AAAAAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19)  =  U2_AAAAAAAAAA(x19)

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

(8) UsableRulesProof (EQUIVALENT transformation)

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

(9) Obligation:

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

BALANCE23_IN_AAAAAAAAAA(tree(T307, T309, T333), T308, T334, X433, .(','(tree(T298, T299, T300), -(T301, T302)), T310), .(','(T298, -(T301, .(T299, T304))), .(','(T300, -(T304, T302)), T311)), X434, X435, T312, X436) → U2_AAAAAAAAAA(T307, T309, T333, T308, T334, X433, T298, T299, T300, T301, T302, T310, T304, T311, X434, X435, T312, X436, balancec23_in_aaaaaaaaaa(T307, T308, T309, T329, T310, T311, T330, T331, T312, T332))
U2_AAAAAAAAAA(T307, T309, T333, T308, T334, X433, T298, T299, T300, T301, T302, T310, T304, T311, X434, X435, T312, X436, balancec23_out_aaaaaaaaaa(T307, T308, T309, T329, T310, T311, T330, T331, T312, T332)) → BALANCE23_IN_AAAAAAAAAA(T333, T329, T334, X433, T330, T331, X434, X435, T332, X436)
BALANCE23_IN_AAAAAAAAAA(tree(T307, T309, T313), T308, T314, X433, .(','(tree(T298, T299, T300), -(T301, T302)), T310), .(','(T298, -(T301, .(T299, T304))), .(','(T300, -(T304, T302)), T311)), X434, X435, T312, X436) → BALANCE23_IN_AAAAAAAAAA(T307, T308, T309, X429, T310, T311, X430, X431, T312, X432)

The TRS R consists of the following rules:

balancec23_in_aaaaaaaaaa(nil, .(T259, T260), T259, T260, T261, T262, T261, T262, .(','(nil, -(T263, T263)), T264), T264) → balancec23_out_aaaaaaaaaa(nil, .(T259, T260), T259, T260, T261, T262, T261, T262, .(','(nil, -(T263, T263)), T264), T264)
balancec23_in_aaaaaaaaaa(tree(T307, T309, T333), T308, T334, X433, .(','(tree(T298, T299, T300), -(T301, T302)), T310), .(','(T298, -(T301, .(T299, T304))), .(','(T300, -(T304, T302)), T311)), X434, X435, T312, X436) → U13_aaaaaaaaaa(T307, T309, T333, T308, T334, X433, T298, T299, T300, T301, T302, T310, T304, T311, X434, X435, T312, X436, balancec23_in_aaaaaaaaaa(T307, T308, T309, T329, T310, T311, T330, T331, T312, T332))
U13_aaaaaaaaaa(T307, T309, T333, T308, T334, X433, T298, T299, T300, T301, T302, T310, T304, T311, X434, X435, T312, X436, balancec23_out_aaaaaaaaaa(T307, T308, T309, T329, T310, T311, T330, T331, T312, T332)) → U14_aaaaaaaaaa(T307, T309, T333, T308, T334, X433, T298, T299, T300, T301, T302, T310, T304, T311, X434, X435, T312, X436, T329, T330, T331, T332, balancec23_in_aaaaaaaaaa(T333, T329, T334, X433, T330, T331, X434, X435, T332, X436))
U14_aaaaaaaaaa(T307, T309, T333, T308, T334, X433, T298, T299, T300, T301, T302, T310, T304, T311, X434, X435, T312, X436, T329, T330, T331, T332, balancec23_out_aaaaaaaaaa(T333, T329, T334, X433, T330, T331, X434, X435, T332, X436)) → balancec23_out_aaaaaaaaaa(tree(T307, T309, T333), T308, T334, X433, .(','(tree(T298, T299, T300), -(T301, T302)), T310), .(','(T298, -(T301, .(T299, T304))), .(','(T300, -(T304, T302)), T311)), X434, X435, T312, X436)

The argument filtering Pi contains the following mapping:
tree(x1, x2, x3)  =  tree(x1, x2, x3)
balancec23_in_aaaaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  balancec23_in_aaaaaaaaaa
balancec23_out_aaaaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  balancec23_out_aaaaaaaaaa
U13_aaaaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19)  =  U13_aaaaaaaaaa(x19)
U14_aaaaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22, x23)  =  U14_aaaaaaaaaa(x23)
BALANCE23_IN_AAAAAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  BALANCE23_IN_AAAAAAAAAA
U2_AAAAAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19)  =  U2_AAAAAAAAAA(x19)

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

(10) PiDPToQDPProof (SOUND transformation)

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

(11) Obligation:

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

BALANCE23_IN_AAAAAAAAAA → U2_AAAAAAAAAA(balancec23_in_aaaaaaaaaa)
U2_AAAAAAAAAA(balancec23_out_aaaaaaaaaa) → BALANCE23_IN_AAAAAAAAAA
BALANCE23_IN_AAAAAAAAAA → BALANCE23_IN_AAAAAAAAAA

The TRS R consists of the following rules:

balancec23_in_aaaaaaaaaa → balancec23_out_aaaaaaaaaa
balancec23_in_aaaaaaaaaa → U13_aaaaaaaaaa(balancec23_in_aaaaaaaaaa)
U13_aaaaaaaaaa(balancec23_out_aaaaaaaaaa) → U14_aaaaaaaaaa(balancec23_in_aaaaaaaaaa)
U14_aaaaaaaaaa(balancec23_out_aaaaaaaaaa) → balancec23_out_aaaaaaaaaa

The set Q consists of the following terms:

balancec23_in_aaaaaaaaaa
U13_aaaaaaaaaa(x0)
U14_aaaaaaaaaa(x0)

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

(12) Narrowing (SOUND transformation)

By narrowing [LPAR04] the rule BALANCE23_IN_AAAAAAAAAA → U2_AAAAAAAAAA(balancec23_in_aaaaaaaaaa) at position [0] we obtained the following new rules [LPAR04]:

BALANCE23_IN_AAAAAAAAAA → U2_AAAAAAAAAA(balancec23_out_aaaaaaaaaa)
BALANCE23_IN_AAAAAAAAAA → U2_AAAAAAAAAA(U13_aaaaaaaaaa(balancec23_in_aaaaaaaaaa))

(13) Obligation:

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

U2_AAAAAAAAAA(balancec23_out_aaaaaaaaaa) → BALANCE23_IN_AAAAAAAAAA
BALANCE23_IN_AAAAAAAAAA → BALANCE23_IN_AAAAAAAAAA
BALANCE23_IN_AAAAAAAAAA → U2_AAAAAAAAAA(balancec23_out_aaaaaaaaaa)
BALANCE23_IN_AAAAAAAAAA → U2_AAAAAAAAAA(U13_aaaaaaaaaa(balancec23_in_aaaaaaaaaa))

The TRS R consists of the following rules:

balancec23_in_aaaaaaaaaa → balancec23_out_aaaaaaaaaa
balancec23_in_aaaaaaaaaa → U13_aaaaaaaaaa(balancec23_in_aaaaaaaaaa)
U13_aaaaaaaaaa(balancec23_out_aaaaaaaaaa) → U14_aaaaaaaaaa(balancec23_in_aaaaaaaaaa)
U14_aaaaaaaaaa(balancec23_out_aaaaaaaaaa) → balancec23_out_aaaaaaaaaa

The set Q consists of the following terms:

balancec23_in_aaaaaaaaaa
U13_aaaaaaaaaa(x0)
U14_aaaaaaaaaa(x0)

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

(14) NonTerminationProof (EQUIVALENT transformation)

We used the non-termination processor [FROCOS05] to show that the DP problem is infinite.
Found a loop by semiunifying a rule from P directly.

s = BALANCE23_IN_AAAAAAAAAA evaluates to t =BALANCE23_IN_AAAAAAAAAA

Thus s starts an infinite chain as s semiunifies with t with the following substitutions:
  • Matcher: [ ]
  • Semiunifier: [ ]



Rewriting sequence

The DP semiunifies directly so there is only one rewrite step from BALANCE23_IN_AAAAAAAAAA to BALANCE23_IN_AAAAAAAAAA.



(15) NO

(16) Obligation:

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

BALANCE13_IN_AAAAAA(tree(T440, T442, T466), T441, .(','(tree(T430, T431, T432), -(T433, T434)), T443), .(','(T430, -(T433, .(T431, T436))), .(','(T432, -(T436, T434)), T444)), T467, T445) → U5_AAAAAA(T440, T442, T466, T441, T430, T431, T432, T433, T434, T443, T436, T444, T467, T445, balancec23_in_aaaaaaaaaa(T440, T441, T442, T462, T443, T444, T463, T464, T445, T465))
U5_AAAAAA(T440, T442, T466, T441, T430, T431, T432, T433, T434, T443, T436, T444, T467, T445, balancec23_out_aaaaaaaaaa(T440, T441, T442, T462, T443, T444, T463, T464, T445, T465)) → BALANCE13_IN_AAAAAA(T466, T462, T463, T464, T467, T465)

The TRS R consists of the following rules:

balancec23_in_aaaaaaaaaa(nil, .(T259, T260), T259, T260, T261, T262, T261, T262, .(','(nil, -(T263, T263)), T264), T264) → balancec23_out_aaaaaaaaaa(nil, .(T259, T260), T259, T260, T261, T262, T261, T262, .(','(nil, -(T263, T263)), T264), T264)
balancec23_in_aaaaaaaaaa(tree(T307, T309, T333), T308, T334, X433, .(','(tree(T298, T299, T300), -(T301, T302)), T310), .(','(T298, -(T301, .(T299, T304))), .(','(T300, -(T304, T302)), T311)), X434, X435, T312, X436) → U13_aaaaaaaaaa(T307, T309, T333, T308, T334, X433, T298, T299, T300, T301, T302, T310, T304, T311, X434, X435, T312, X436, balancec23_in_aaaaaaaaaa(T307, T308, T309, T329, T310, T311, T330, T331, T312, T332))
U13_aaaaaaaaaa(T307, T309, T333, T308, T334, X433, T298, T299, T300, T301, T302, T310, T304, T311, X434, X435, T312, X436, balancec23_out_aaaaaaaaaa(T307, T308, T309, T329, T310, T311, T330, T331, T312, T332)) → U14_aaaaaaaaaa(T307, T309, T333, T308, T334, X433, T298, T299, T300, T301, T302, T310, T304, T311, X434, X435, T312, X436, T329, T330, T331, T332, balancec23_in_aaaaaaaaaa(T333, T329, T334, X433, T330, T331, X434, X435, T332, X436))
U14_aaaaaaaaaa(T307, T309, T333, T308, T334, X433, T298, T299, T300, T301, T302, T310, T304, T311, X434, X435, T312, X436, T329, T330, T331, T332, balancec23_out_aaaaaaaaaa(T333, T329, T334, X433, T330, T331, X434, X435, T332, X436)) → balancec23_out_aaaaaaaaaa(tree(T307, T309, T333), T308, T334, X433, .(','(tree(T298, T299, T300), -(T301, T302)), T310), .(','(T298, -(T301, .(T299, T304))), .(','(T300, -(T304, T302)), T311)), X434, X435, T312, X436)
balancec12_in_aaaaggagaaaaa(nil, .(T108, T109), T108, T109, T110, T111, T112, T113, T114, .(','(T110, -(.(T108, T109), .(T111, T112))), .(','(T113, -(T112, [])), T114)), T114, .(','(nil, -(X200, X200)), X201), X201) → balancec12_out_aaaaggagaaaaa(nil, .(T108, T109), T108, T109, T110, T111, T112, T113, T114, .(','(T110, -(.(T108, T109), .(T111, T112))), .(','(T113, -(T112, [])), T114)), T114, .(','(nil, -(X200, X200)), X201), X201)
balancec12_in_aaaaggagaaaaa(tree(T157, T159, T192), T158, T193, X276, tree(T148, T149, T150), T151, T161, T153, .(','(T148, -(T158, .(T149, T162))), .(','(T150, -(T162, .(T151, T161))), T160)), X277, X278, T190, X280) → U17_aaaaggagaaaaa(T157, T159, T192, T158, T193, X276, T148, T149, T150, T151, T161, T153, T162, T160, X277, X278, T190, X280, balancec23_in_aaaaaaaaaa(T157, T158, T159, T187, .(','(T153, -(T161, [])), .(','(T148, -(T158, .(T149, T162))), .(','(T150, -(T162, .(T151, T161))), T160))), T160, T188, T189, T190, T191))
U17_aaaaggagaaaaa(T157, T159, T192, T158, T193, X276, T148, T149, T150, T151, T161, T153, T162, T160, X277, X278, T190, X280, balancec23_out_aaaaaaaaaa(T157, T158, T159, T187, .(','(T153, -(T161, [])), .(','(T148, -(T158, .(T149, T162))), .(','(T150, -(T162, .(T151, T161))), T160))), T160, T188, T189, T190, T191)) → U18_aaaaggagaaaaa(T157, T159, T192, T158, T193, X276, T148, T149, T150, T151, T161, T153, T162, T160, X277, X278, T190, X280, T187, T188, T189, T191, balancec23_in_aaaaaaaaaa(T192, T187, T193, X276, T188, T189, X277, X278, T191, X280))
U18_aaaaggagaaaaa(T157, T159, T192, T158, T193, X276, T148, T149, T150, T151, T161, T153, T162, T160, X277, X278, T190, X280, T187, T188, T189, T191, balancec23_out_aaaaaaaaaa(T192, T187, T193, X276, T188, T189, X277, X278, T191, X280)) → balancec12_out_aaaaggagaaaaa(tree(T157, T159, T192), T158, T193, X276, tree(T148, T149, T150), T151, T161, T153, .(','(T148, -(T158, .(T149, T162))), .(','(T150, -(T162, .(T151, T161))), T160)), X277, X278, T190, X280)

The argument filtering Pi contains the following mapping:
tree(x1, x2, x3)  =  tree(x1, x2, x3)
balancec23_in_aaaaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  balancec23_in_aaaaaaaaaa
balancec23_out_aaaaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  balancec23_out_aaaaaaaaaa
U13_aaaaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19)  =  U13_aaaaaaaaaa(x19)
U14_aaaaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22, x23)  =  U14_aaaaaaaaaa(x23)
balancec12_in_aaaaggagaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13)  =  balancec12_in_aaaaggagaaaaa(x5, x6, x8)
balancec12_out_aaaaggagaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13)  =  balancec12_out_aaaaggagaaaaa(x5, x6, x8)
U17_aaaaggagaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19)  =  U17_aaaaggagaaaaa(x7, x8, x9, x10, x12, x19)
U18_aaaaggagaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22, x23)  =  U18_aaaaggagaaaaa(x7, x8, x9, x10, x12, x23)
BALANCE13_IN_AAAAAA(x1, x2, x3, x4, x5, x6)  =  BALANCE13_IN_AAAAAA
U5_AAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15)  =  U5_AAAAAA(x15)

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

(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_AAAAAA(tree(T440, T442, T466), T441, .(','(tree(T430, T431, T432), -(T433, T434)), T443), .(','(T430, -(T433, .(T431, T436))), .(','(T432, -(T436, T434)), T444)), T467, T445) → U5_AAAAAA(T440, T442, T466, T441, T430, T431, T432, T433, T434, T443, T436, T444, T467, T445, balancec23_in_aaaaaaaaaa(T440, T441, T442, T462, T443, T444, T463, T464, T445, T465))
U5_AAAAAA(T440, T442, T466, T441, T430, T431, T432, T433, T434, T443, T436, T444, T467, T445, balancec23_out_aaaaaaaaaa(T440, T441, T442, T462, T443, T444, T463, T464, T445, T465)) → BALANCE13_IN_AAAAAA(T466, T462, T463, T464, T467, T465)

The TRS R consists of the following rules:

balancec23_in_aaaaaaaaaa(nil, .(T259, T260), T259, T260, T261, T262, T261, T262, .(','(nil, -(T263, T263)), T264), T264) → balancec23_out_aaaaaaaaaa(nil, .(T259, T260), T259, T260, T261, T262, T261, T262, .(','(nil, -(T263, T263)), T264), T264)
balancec23_in_aaaaaaaaaa(tree(T307, T309, T333), T308, T334, X433, .(','(tree(T298, T299, T300), -(T301, T302)), T310), .(','(T298, -(T301, .(T299, T304))), .(','(T300, -(T304, T302)), T311)), X434, X435, T312, X436) → U13_aaaaaaaaaa(T307, T309, T333, T308, T334, X433, T298, T299, T300, T301, T302, T310, T304, T311, X434, X435, T312, X436, balancec23_in_aaaaaaaaaa(T307, T308, T309, T329, T310, T311, T330, T331, T312, T332))
U13_aaaaaaaaaa(T307, T309, T333, T308, T334, X433, T298, T299, T300, T301, T302, T310, T304, T311, X434, X435, T312, X436, balancec23_out_aaaaaaaaaa(T307, T308, T309, T329, T310, T311, T330, T331, T312, T332)) → U14_aaaaaaaaaa(T307, T309, T333, T308, T334, X433, T298, T299, T300, T301, T302, T310, T304, T311, X434, X435, T312, X436, T329, T330, T331, T332, balancec23_in_aaaaaaaaaa(T333, T329, T334, X433, T330, T331, X434, X435, T332, X436))
U14_aaaaaaaaaa(T307, T309, T333, T308, T334, X433, T298, T299, T300, T301, T302, T310, T304, T311, X434, X435, T312, X436, T329, T330, T331, T332, balancec23_out_aaaaaaaaaa(T333, T329, T334, X433, T330, T331, X434, X435, T332, X436)) → balancec23_out_aaaaaaaaaa(tree(T307, T309, T333), T308, T334, X433, .(','(tree(T298, T299, T300), -(T301, T302)), T310), .(','(T298, -(T301, .(T299, T304))), .(','(T300, -(T304, T302)), T311)), X434, X435, T312, X436)

The argument filtering Pi contains the following mapping:
tree(x1, x2, x3)  =  tree(x1, x2, x3)
balancec23_in_aaaaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  balancec23_in_aaaaaaaaaa
balancec23_out_aaaaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  balancec23_out_aaaaaaaaaa
U13_aaaaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19)  =  U13_aaaaaaaaaa(x19)
U14_aaaaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22, x23)  =  U14_aaaaaaaaaa(x23)
BALANCE13_IN_AAAAAA(x1, x2, x3, x4, x5, x6)  =  BALANCE13_IN_AAAAAA
U5_AAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15)  =  U5_AAAAAA(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_AAAAAA → U5_AAAAAA(balancec23_in_aaaaaaaaaa)
U5_AAAAAA(balancec23_out_aaaaaaaaaa) → BALANCE13_IN_AAAAAA

The TRS R consists of the following rules:

balancec23_in_aaaaaaaaaa → balancec23_out_aaaaaaaaaa
balancec23_in_aaaaaaaaaa → U13_aaaaaaaaaa(balancec23_in_aaaaaaaaaa)
U13_aaaaaaaaaa(balancec23_out_aaaaaaaaaa) → U14_aaaaaaaaaa(balancec23_in_aaaaaaaaaa)
U14_aaaaaaaaaa(balancec23_out_aaaaaaaaaa) → balancec23_out_aaaaaaaaaa

The set Q consists of the following terms:

balancec23_in_aaaaaaaaaa
U13_aaaaaaaaaa(x0)
U14_aaaaaaaaaa(x0)

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

(21) Narrowing (SOUND transformation)

By narrowing [LPAR04] the rule BALANCE13_IN_AAAAAA → U5_AAAAAA(balancec23_in_aaaaaaaaaa) at position [0] we obtained the following new rules [LPAR04]:

BALANCE13_IN_AAAAAA → U5_AAAAAA(balancec23_out_aaaaaaaaaa)
BALANCE13_IN_AAAAAA → U5_AAAAAA(U13_aaaaaaaaaa(balancec23_in_aaaaaaaaaa))

(22) Obligation:

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

U5_AAAAAA(balancec23_out_aaaaaaaaaa) → BALANCE13_IN_AAAAAA
BALANCE13_IN_AAAAAA → U5_AAAAAA(balancec23_out_aaaaaaaaaa)
BALANCE13_IN_AAAAAA → U5_AAAAAA(U13_aaaaaaaaaa(balancec23_in_aaaaaaaaaa))

The TRS R consists of the following rules:

balancec23_in_aaaaaaaaaa → balancec23_out_aaaaaaaaaa
balancec23_in_aaaaaaaaaa → U13_aaaaaaaaaa(balancec23_in_aaaaaaaaaa)
U13_aaaaaaaaaa(balancec23_out_aaaaaaaaaa) → U14_aaaaaaaaaa(balancec23_in_aaaaaaaaaa)
U14_aaaaaaaaaa(balancec23_out_aaaaaaaaaa) → balancec23_out_aaaaaaaaaa

The set Q consists of the following terms:

balancec23_in_aaaaaaaaaa
U13_aaaaaaaaaa(x0)
U14_aaaaaaaaaa(x0)

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

(23) NonTerminationProof (EQUIVALENT transformation)

We used the non-termination processor [FROCOS05] to show that the DP problem is infinite.
Found a loop by narrowing to the left:

s = BALANCE13_IN_AAAAAA evaluates to t =BALANCE13_IN_AAAAAA

Thus s starts an infinite chain as s semiunifies with t with the following substitutions:
  • Matcher: [ ]
  • Semiunifier: [ ]



Rewriting sequence

BALANCE13_IN_AAAAAA → U5_AAAAAA(balancec23_out_aaaaaaaaaa)
with rule BALANCE13_IN_AAAAAA → U5_AAAAAA(balancec23_out_aaaaaaaaaa) at position [] and matcher [ ]

U5_AAAAAA(balancec23_out_aaaaaaaaaa) → BALANCE13_IN_AAAAAA
with rule U5_AAAAAA(balancec23_out_aaaaaaaaaa) → BALANCE13_IN_AAAAAA

Now applying the matcher to the start term leads to a term which is equal to the last term in the rewriting sequence


All these steps are and every following step will be a correct step w.r.t to Q.



(24) NO