0 Prolog
↳1 PrologToPrologProblemTransformerProof (⇒, 281 ms)
↳2 Prolog
↳3 PrologToPiTRSProof (⇒, 128 ms)
↳4 PiTRS
↳5 DependencyPairsProof (⇔, 331 ms)
↳6 PiDP
↳7 DependencyGraphProof (⇔, 0 ms)
↳8 AND
↳9 PiDP
↳10 UsableRulesProof (⇔, 0 ms)
↳11 PiDP
↳12 PiDPToQDPProof (⇒, 0 ms)
↳13 QDP
↳14 QDPSizeChangeProof (⇔, 0 ms)
↳15 YES
↳16 PiDP
↳17 UsableRulesProof (⇔, 0 ms)
↳18 PiDP
↳19 PiDPToQDPProof (⇒, 0 ms)
↳20 QDP
↳21 QDPSizeChangeProof (⇔, 0 ms)
↳22 YES
↳23 PiDP
↳24 UsableRulesProof (⇔, 0 ms)
↳25 PiDP
↳26 PiDPToQDPProof (⇒, 0 ms)
↳27 QDP
↳28 QDPSizeChangeProof (⇔, 0 ms)
↳29 YES
goalF_in_gaa(s(T19), T13, T14) → U13_gaa(T19, T13, T14, s2tA_in_ga(T19, X31))
s2tA_in_ga(s(T27), node(X66, X67, X66)) → U1_ga(T27, X66, X67, s2tA_in_ga(T27, X66))
s2tA_in_ga(s(T33), node(nil, X96, X97)) → U2_ga(T33, X96, X97, s2tA_in_ga(T33, X97))
s2tA_in_ga(s(T39), node(X126, X127, nil)) → U3_ga(T39, X126, X127, s2tA_in_ga(T39, X126))
s2tA_in_ga(s(T45), node(nil, X147, nil)) → s2tA_out_ga(s(T45), node(nil, X147, nil))
s2tA_in_ga(0, nil) → s2tA_out_ga(0, nil)
U3_ga(T39, X126, X127, s2tA_out_ga(T39, X126)) → s2tA_out_ga(s(T39), node(X126, X127, nil))
U2_ga(T33, X96, X97, s2tA_out_ga(T33, X97)) → s2tA_out_ga(s(T33), node(nil, X96, X97))
U1_ga(T27, X66, X67, s2tA_out_ga(T27, X66)) → s2tA_out_ga(s(T27), node(X66, X67, X66))
U13_gaa(T19, T13, T14, s2tA_out_ga(T19, X31)) → goalF_out_gaa(s(T19), T13, T14)
goalF_in_gaa(s(T19), T62, T63) → U14_gaa(T19, T62, T63, s2tA_in_ga(T19, T61))
U14_gaa(T19, T62, T63, s2tA_out_ga(T19, T61)) → U15_gaa(T19, T62, T63, pD_in_gaaaa(T61, X168, T62, X167, T63))
pD_in_gaaaa(T61, X168, T62, X167, T63) → U8_gaaaa(T61, X168, T62, X167, T63, tappendE_in_gaaa(T61, X168, T62, X167))
tappendE_in_gaaa(nil, X193, T71, node(node(nil, T71, nil), X193, nil)) → tappendE_out_gaaa(nil, X193, T71, node(node(nil, T71, nil), X193, nil))
tappendE_in_gaaa(nil, X213, T81, node(nil, X213, node(nil, T81, nil))) → tappendE_out_gaaa(nil, X213, T81, node(nil, X213, node(nil, T81, nil)))
tappendE_in_gaaa(T100, X251, T101, node(X252, X251, T100)) → U11_gaaa(T100, X251, T101, X252, tappendB_in_gaa(T100, T101, X252))
tappendB_in_gaa(nil, T108, node(nil, T108, nil)) → tappendB_out_gaa(nil, T108, node(nil, T108, nil))
tappendB_in_gaa(node(nil, T121, T122), T123, node(node(nil, T123, nil), T121, T122)) → tappendB_out_gaa(node(nil, T121, T122), T123, node(node(nil, T123, nil), T121, T122))
tappendB_in_gaa(node(T136, T137, nil), T138, node(T136, T137, node(nil, T138, nil))) → tappendB_out_gaa(node(T136, T137, nil), T138, node(T136, T137, node(nil, T138, nil)))
tappendB_in_gaa(node(T159, T156, T157), T160, node(X319, T156, T157)) → U4_gaa(T159, T156, T157, T160, X319, tappendB_in_gaa(T159, T160, X319))
tappendB_in_gaa(node(T171, T172, T175), T176, node(T171, T172, X339)) → U5_gaa(T171, T172, T175, T176, X339, tappendB_in_gaa(T175, T176, X339))
U5_gaa(T171, T172, T175, T176, X339, tappendB_out_gaa(T175, T176, X339)) → tappendB_out_gaa(node(T171, T172, T175), T176, node(T171, T172, X339))
U4_gaa(T159, T156, T157, T160, X319, tappendB_out_gaa(T159, T160, X319)) → tappendB_out_gaa(node(T159, T156, T157), T160, node(X319, T156, T157))
U11_gaaa(T100, X251, T101, X252, tappendB_out_gaa(T100, T101, X252)) → tappendE_out_gaaa(T100, X251, T101, node(X252, X251, T100))
tappendE_in_gaaa(T189, X363, T190, node(T189, X363, X364)) → U12_gaaa(T189, X363, T190, X364, tappendB_in_gaa(T189, T190, X364))
U12_gaaa(T189, X363, T190, X364, tappendB_out_gaa(T189, T190, X364)) → tappendE_out_gaaa(T189, X363, T190, node(T189, X363, X364))
U8_gaaaa(T61, X168, T62, X167, T63, tappendE_out_gaaa(T61, X168, T62, X167)) → pD_out_gaaaa(T61, X168, T62, X167, T63)
pD_in_gaaaa(T61, T64, T62, T65, T66) → U9_gaaaa(T61, T64, T62, T65, T66, tappendE_in_gaaa(T61, T64, T62, T65))
U9_gaaaa(T61, T64, T62, T65, T66, tappendE_out_gaaa(T61, T64, T62, T65)) → U10_gaaaa(T61, T64, T62, T65, T66, tlastC_in_ag(T66, T65))
tlastC_in_ag(T199, node(nil, T199, nil)) → tlastC_out_ag(T199, node(nil, T199, nil))
tlastC_in_ag(T220, node(T221, T218, T219)) → U6_ag(T220, T221, T218, T219, tlastC_in_ag(T220, T221))
tlastC_in_ag(T236, node(T233, T234, T237)) → U7_ag(T236, T233, T234, T237, tlastC_in_ag(T236, T237))
U7_ag(T236, T233, T234, T237, tlastC_out_ag(T236, T237)) → tlastC_out_ag(T236, node(T233, T234, T237))
U6_ag(T220, T221, T218, T219, tlastC_out_ag(T220, T221)) → tlastC_out_ag(T220, node(T221, T218, T219))
U10_gaaaa(T61, T64, T62, T65, T66, tlastC_out_ag(T66, T65)) → pD_out_gaaaa(T61, T64, T62, T65, T66)
U15_gaa(T19, T62, T63, pD_out_gaaaa(T61, X168, T62, X167, T63)) → goalF_out_gaa(s(T19), T62, T63)
goalF_in_gaa(s(T244), T13, T14) → U16_gaa(T244, T13, T14, s2tA_in_ga(T244, X434))
U16_gaa(T244, T13, T14, s2tA_out_ga(T244, X434)) → goalF_out_gaa(s(T244), T13, T14)
goalF_in_gaa(s(T244), T264, T265) → U17_gaa(T244, T264, T265, s2tA_in_ga(T244, T263))
U17_gaa(T244, T264, T265, s2tA_out_ga(T244, T263)) → U18_gaa(T244, T264, T265, tappendB_in_gaa(node(nil, X465, T263), T264, X464))
U18_gaa(T244, T264, T265, tappendB_out_gaa(node(nil, X465, T263), T264, X464)) → goalF_out_gaa(s(T244), T264, T265)
goalF_in_gaa(s(T244), T264, T268) → U19_gaa(T244, T264, T268, s2tA_in_ga(T244, T263))
U19_gaa(T244, T264, T268, s2tA_out_ga(T244, T263)) → U20_gaa(T244, T264, T268, tappendB_in_gaa(node(nil, T266, T263), T264, T267))
U20_gaa(T244, T264, T268, tappendB_out_gaa(node(nil, T266, T263), T264, T267)) → U21_gaa(T244, T264, T268, tlastC_in_ag(T268, T267))
U21_gaa(T244, T264, T268, tlastC_out_ag(T268, T267)) → goalF_out_gaa(s(T244), T264, T268)
goalF_in_gaa(s(T275), T13, T14) → U22_gaa(T275, T13, T14, s2tA_in_ga(T275, X495))
U22_gaa(T275, T13, T14, s2tA_out_ga(T275, X495)) → goalF_out_gaa(s(T275), T13, T14)
goalF_in_gaa(s(T275), T295, T296) → U23_gaa(T275, T295, T296, s2tA_in_ga(T275, T294))
U23_gaa(T275, T295, T296, s2tA_out_ga(T275, T294)) → U24_gaa(T275, T295, T296, tappendB_in_gaa(node(T294, X527, nil), T295, X526))
U24_gaa(T275, T295, T296, tappendB_out_gaa(node(T294, X527, nil), T295, X526)) → goalF_out_gaa(s(T275), T295, T296)
goalF_in_gaa(s(T275), T295, T299) → U25_gaa(T275, T295, T299, s2tA_in_ga(T275, T294))
U25_gaa(T275, T295, T299, s2tA_out_ga(T275, T294)) → U26_gaa(T275, T295, T299, tappendB_in_gaa(node(T294, T297, nil), T295, T298))
U26_gaa(T275, T295, T299, tappendB_out_gaa(node(T294, T297, nil), T295, T298)) → U27_gaa(T275, T295, T299, tlastC_in_ag(T299, T298))
U27_gaa(T275, T295, T299, tlastC_out_ag(T299, T298)) → goalF_out_gaa(s(T275), T295, T299)
goalF_in_gaa(s(T306), T317, T318) → U28_gaa(T306, T317, T318, pD_in_gaaaa(nil, X569, T317, X568, T318))
U28_gaa(T306, T317, T318, pD_out_gaaaa(nil, X569, T317, X568, T318)) → goalF_out_gaa(s(T306), T317, T318)
goalF_in_gaa(0, T331, T332) → U29_gaa(T331, T332, tappendB_in_gaa(nil, T331, X588))
U29_gaa(T331, T332, tappendB_out_gaa(nil, T331, X588)) → goalF_out_gaa(0, T331, T332)
goalF_in_gaa(0, T331, T336) → U30_gaa(T331, T336, tappendB_in_gaa(nil, T331, T335))
U30_gaa(T331, T336, tappendB_out_gaa(nil, T331, T335)) → U31_gaa(T331, T336, tlastC_in_ag(T336, T335))
U31_gaa(T331, T336, tlastC_out_ag(T336, T335)) → goalF_out_gaa(0, T331, T336)
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
goalF_in_gaa(s(T19), T13, T14) → U13_gaa(T19, T13, T14, s2tA_in_ga(T19, X31))
s2tA_in_ga(s(T27), node(X66, X67, X66)) → U1_ga(T27, X66, X67, s2tA_in_ga(T27, X66))
s2tA_in_ga(s(T33), node(nil, X96, X97)) → U2_ga(T33, X96, X97, s2tA_in_ga(T33, X97))
s2tA_in_ga(s(T39), node(X126, X127, nil)) → U3_ga(T39, X126, X127, s2tA_in_ga(T39, X126))
s2tA_in_ga(s(T45), node(nil, X147, nil)) → s2tA_out_ga(s(T45), node(nil, X147, nil))
s2tA_in_ga(0, nil) → s2tA_out_ga(0, nil)
U3_ga(T39, X126, X127, s2tA_out_ga(T39, X126)) → s2tA_out_ga(s(T39), node(X126, X127, nil))
U2_ga(T33, X96, X97, s2tA_out_ga(T33, X97)) → s2tA_out_ga(s(T33), node(nil, X96, X97))
U1_ga(T27, X66, X67, s2tA_out_ga(T27, X66)) → s2tA_out_ga(s(T27), node(X66, X67, X66))
U13_gaa(T19, T13, T14, s2tA_out_ga(T19, X31)) → goalF_out_gaa(s(T19), T13, T14)
goalF_in_gaa(s(T19), T62, T63) → U14_gaa(T19, T62, T63, s2tA_in_ga(T19, T61))
U14_gaa(T19, T62, T63, s2tA_out_ga(T19, T61)) → U15_gaa(T19, T62, T63, pD_in_gaaaa(T61, X168, T62, X167, T63))
pD_in_gaaaa(T61, X168, T62, X167, T63) → U8_gaaaa(T61, X168, T62, X167, T63, tappendE_in_gaaa(T61, X168, T62, X167))
tappendE_in_gaaa(nil, X193, T71, node(node(nil, T71, nil), X193, nil)) → tappendE_out_gaaa(nil, X193, T71, node(node(nil, T71, nil), X193, nil))
tappendE_in_gaaa(nil, X213, T81, node(nil, X213, node(nil, T81, nil))) → tappendE_out_gaaa(nil, X213, T81, node(nil, X213, node(nil, T81, nil)))
tappendE_in_gaaa(T100, X251, T101, node(X252, X251, T100)) → U11_gaaa(T100, X251, T101, X252, tappendB_in_gaa(T100, T101, X252))
tappendB_in_gaa(nil, T108, node(nil, T108, nil)) → tappendB_out_gaa(nil, T108, node(nil, T108, nil))
tappendB_in_gaa(node(nil, T121, T122), T123, node(node(nil, T123, nil), T121, T122)) → tappendB_out_gaa(node(nil, T121, T122), T123, node(node(nil, T123, nil), T121, T122))
tappendB_in_gaa(node(T136, T137, nil), T138, node(T136, T137, node(nil, T138, nil))) → tappendB_out_gaa(node(T136, T137, nil), T138, node(T136, T137, node(nil, T138, nil)))
tappendB_in_gaa(node(T159, T156, T157), T160, node(X319, T156, T157)) → U4_gaa(T159, T156, T157, T160, X319, tappendB_in_gaa(T159, T160, X319))
tappendB_in_gaa(node(T171, T172, T175), T176, node(T171, T172, X339)) → U5_gaa(T171, T172, T175, T176, X339, tappendB_in_gaa(T175, T176, X339))
U5_gaa(T171, T172, T175, T176, X339, tappendB_out_gaa(T175, T176, X339)) → tappendB_out_gaa(node(T171, T172, T175), T176, node(T171, T172, X339))
U4_gaa(T159, T156, T157, T160, X319, tappendB_out_gaa(T159, T160, X319)) → tappendB_out_gaa(node(T159, T156, T157), T160, node(X319, T156, T157))
U11_gaaa(T100, X251, T101, X252, tappendB_out_gaa(T100, T101, X252)) → tappendE_out_gaaa(T100, X251, T101, node(X252, X251, T100))
tappendE_in_gaaa(T189, X363, T190, node(T189, X363, X364)) → U12_gaaa(T189, X363, T190, X364, tappendB_in_gaa(T189, T190, X364))
U12_gaaa(T189, X363, T190, X364, tappendB_out_gaa(T189, T190, X364)) → tappendE_out_gaaa(T189, X363, T190, node(T189, X363, X364))
U8_gaaaa(T61, X168, T62, X167, T63, tappendE_out_gaaa(T61, X168, T62, X167)) → pD_out_gaaaa(T61, X168, T62, X167, T63)
pD_in_gaaaa(T61, T64, T62, T65, T66) → U9_gaaaa(T61, T64, T62, T65, T66, tappendE_in_gaaa(T61, T64, T62, T65))
U9_gaaaa(T61, T64, T62, T65, T66, tappendE_out_gaaa(T61, T64, T62, T65)) → U10_gaaaa(T61, T64, T62, T65, T66, tlastC_in_ag(T66, T65))
tlastC_in_ag(T199, node(nil, T199, nil)) → tlastC_out_ag(T199, node(nil, T199, nil))
tlastC_in_ag(T220, node(T221, T218, T219)) → U6_ag(T220, T221, T218, T219, tlastC_in_ag(T220, T221))
tlastC_in_ag(T236, node(T233, T234, T237)) → U7_ag(T236, T233, T234, T237, tlastC_in_ag(T236, T237))
U7_ag(T236, T233, T234, T237, tlastC_out_ag(T236, T237)) → tlastC_out_ag(T236, node(T233, T234, T237))
U6_ag(T220, T221, T218, T219, tlastC_out_ag(T220, T221)) → tlastC_out_ag(T220, node(T221, T218, T219))
U10_gaaaa(T61, T64, T62, T65, T66, tlastC_out_ag(T66, T65)) → pD_out_gaaaa(T61, T64, T62, T65, T66)
U15_gaa(T19, T62, T63, pD_out_gaaaa(T61, X168, T62, X167, T63)) → goalF_out_gaa(s(T19), T62, T63)
goalF_in_gaa(s(T244), T13, T14) → U16_gaa(T244, T13, T14, s2tA_in_ga(T244, X434))
U16_gaa(T244, T13, T14, s2tA_out_ga(T244, X434)) → goalF_out_gaa(s(T244), T13, T14)
goalF_in_gaa(s(T244), T264, T265) → U17_gaa(T244, T264, T265, s2tA_in_ga(T244, T263))
U17_gaa(T244, T264, T265, s2tA_out_ga(T244, T263)) → U18_gaa(T244, T264, T265, tappendB_in_gaa(node(nil, X465, T263), T264, X464))
U18_gaa(T244, T264, T265, tappendB_out_gaa(node(nil, X465, T263), T264, X464)) → goalF_out_gaa(s(T244), T264, T265)
goalF_in_gaa(s(T244), T264, T268) → U19_gaa(T244, T264, T268, s2tA_in_ga(T244, T263))
U19_gaa(T244, T264, T268, s2tA_out_ga(T244, T263)) → U20_gaa(T244, T264, T268, tappendB_in_gaa(node(nil, T266, T263), T264, T267))
U20_gaa(T244, T264, T268, tappendB_out_gaa(node(nil, T266, T263), T264, T267)) → U21_gaa(T244, T264, T268, tlastC_in_ag(T268, T267))
U21_gaa(T244, T264, T268, tlastC_out_ag(T268, T267)) → goalF_out_gaa(s(T244), T264, T268)
goalF_in_gaa(s(T275), T13, T14) → U22_gaa(T275, T13, T14, s2tA_in_ga(T275, X495))
U22_gaa(T275, T13, T14, s2tA_out_ga(T275, X495)) → goalF_out_gaa(s(T275), T13, T14)
goalF_in_gaa(s(T275), T295, T296) → U23_gaa(T275, T295, T296, s2tA_in_ga(T275, T294))
U23_gaa(T275, T295, T296, s2tA_out_ga(T275, T294)) → U24_gaa(T275, T295, T296, tappendB_in_gaa(node(T294, X527, nil), T295, X526))
U24_gaa(T275, T295, T296, tappendB_out_gaa(node(T294, X527, nil), T295, X526)) → goalF_out_gaa(s(T275), T295, T296)
goalF_in_gaa(s(T275), T295, T299) → U25_gaa(T275, T295, T299, s2tA_in_ga(T275, T294))
U25_gaa(T275, T295, T299, s2tA_out_ga(T275, T294)) → U26_gaa(T275, T295, T299, tappendB_in_gaa(node(T294, T297, nil), T295, T298))
U26_gaa(T275, T295, T299, tappendB_out_gaa(node(T294, T297, nil), T295, T298)) → U27_gaa(T275, T295, T299, tlastC_in_ag(T299, T298))
U27_gaa(T275, T295, T299, tlastC_out_ag(T299, T298)) → goalF_out_gaa(s(T275), T295, T299)
goalF_in_gaa(s(T306), T317, T318) → U28_gaa(T306, T317, T318, pD_in_gaaaa(nil, X569, T317, X568, T318))
U28_gaa(T306, T317, T318, pD_out_gaaaa(nil, X569, T317, X568, T318)) → goalF_out_gaa(s(T306), T317, T318)
goalF_in_gaa(0, T331, T332) → U29_gaa(T331, T332, tappendB_in_gaa(nil, T331, X588))
U29_gaa(T331, T332, tappendB_out_gaa(nil, T331, X588)) → goalF_out_gaa(0, T331, T332)
goalF_in_gaa(0, T331, T336) → U30_gaa(T331, T336, tappendB_in_gaa(nil, T331, T335))
U30_gaa(T331, T336, tappendB_out_gaa(nil, T331, T335)) → U31_gaa(T331, T336, tlastC_in_ag(T336, T335))
U31_gaa(T331, T336, tlastC_out_ag(T336, T335)) → goalF_out_gaa(0, T331, T336)
GOALF_IN_GAA(s(T19), T13, T14) → U13_GAA(T19, T13, T14, s2tA_in_ga(T19, X31))
GOALF_IN_GAA(s(T19), T13, T14) → S2TA_IN_GA(T19, X31)
S2TA_IN_GA(s(T27), node(X66, X67, X66)) → U1_GA(T27, X66, X67, s2tA_in_ga(T27, X66))
S2TA_IN_GA(s(T27), node(X66, X67, X66)) → S2TA_IN_GA(T27, X66)
S2TA_IN_GA(s(T33), node(nil, X96, X97)) → U2_GA(T33, X96, X97, s2tA_in_ga(T33, X97))
S2TA_IN_GA(s(T33), node(nil, X96, X97)) → S2TA_IN_GA(T33, X97)
S2TA_IN_GA(s(T39), node(X126, X127, nil)) → U3_GA(T39, X126, X127, s2tA_in_ga(T39, X126))
S2TA_IN_GA(s(T39), node(X126, X127, nil)) → S2TA_IN_GA(T39, X126)
GOALF_IN_GAA(s(T19), T62, T63) → U14_GAA(T19, T62, T63, s2tA_in_ga(T19, T61))
U14_GAA(T19, T62, T63, s2tA_out_ga(T19, T61)) → U15_GAA(T19, T62, T63, pD_in_gaaaa(T61, X168, T62, X167, T63))
U14_GAA(T19, T62, T63, s2tA_out_ga(T19, T61)) → PD_IN_GAAAA(T61, X168, T62, X167, T63)
PD_IN_GAAAA(T61, X168, T62, X167, T63) → U8_GAAAA(T61, X168, T62, X167, T63, tappendE_in_gaaa(T61, X168, T62, X167))
PD_IN_GAAAA(T61, X168, T62, X167, T63) → TAPPENDE_IN_GAAA(T61, X168, T62, X167)
TAPPENDE_IN_GAAA(T100, X251, T101, node(X252, X251, T100)) → U11_GAAA(T100, X251, T101, X252, tappendB_in_gaa(T100, T101, X252))
TAPPENDE_IN_GAAA(T100, X251, T101, node(X252, X251, T100)) → TAPPENDB_IN_GAA(T100, T101, X252)
TAPPENDB_IN_GAA(node(T159, T156, T157), T160, node(X319, T156, T157)) → U4_GAA(T159, T156, T157, T160, X319, tappendB_in_gaa(T159, T160, X319))
TAPPENDB_IN_GAA(node(T159, T156, T157), T160, node(X319, T156, T157)) → TAPPENDB_IN_GAA(T159, T160, X319)
TAPPENDB_IN_GAA(node(T171, T172, T175), T176, node(T171, T172, X339)) → U5_GAA(T171, T172, T175, T176, X339, tappendB_in_gaa(T175, T176, X339))
TAPPENDB_IN_GAA(node(T171, T172, T175), T176, node(T171, T172, X339)) → TAPPENDB_IN_GAA(T175, T176, X339)
TAPPENDE_IN_GAAA(T189, X363, T190, node(T189, X363, X364)) → U12_GAAA(T189, X363, T190, X364, tappendB_in_gaa(T189, T190, X364))
TAPPENDE_IN_GAAA(T189, X363, T190, node(T189, X363, X364)) → TAPPENDB_IN_GAA(T189, T190, X364)
PD_IN_GAAAA(T61, T64, T62, T65, T66) → U9_GAAAA(T61, T64, T62, T65, T66, tappendE_in_gaaa(T61, T64, T62, T65))
U9_GAAAA(T61, T64, T62, T65, T66, tappendE_out_gaaa(T61, T64, T62, T65)) → U10_GAAAA(T61, T64, T62, T65, T66, tlastC_in_ag(T66, T65))
U9_GAAAA(T61, T64, T62, T65, T66, tappendE_out_gaaa(T61, T64, T62, T65)) → TLASTC_IN_AG(T66, T65)
TLASTC_IN_AG(T220, node(T221, T218, T219)) → U6_AG(T220, T221, T218, T219, tlastC_in_ag(T220, T221))
TLASTC_IN_AG(T220, node(T221, T218, T219)) → TLASTC_IN_AG(T220, T221)
TLASTC_IN_AG(T236, node(T233, T234, T237)) → U7_AG(T236, T233, T234, T237, tlastC_in_ag(T236, T237))
TLASTC_IN_AG(T236, node(T233, T234, T237)) → TLASTC_IN_AG(T236, T237)
GOALF_IN_GAA(s(T244), T13, T14) → U16_GAA(T244, T13, T14, s2tA_in_ga(T244, X434))
GOALF_IN_GAA(s(T244), T264, T265) → U17_GAA(T244, T264, T265, s2tA_in_ga(T244, T263))
U17_GAA(T244, T264, T265, s2tA_out_ga(T244, T263)) → U18_GAA(T244, T264, T265, tappendB_in_gaa(node(nil, X465, T263), T264, X464))
U17_GAA(T244, T264, T265, s2tA_out_ga(T244, T263)) → TAPPENDB_IN_GAA(node(nil, X465, T263), T264, X464)
GOALF_IN_GAA(s(T244), T264, T268) → U19_GAA(T244, T264, T268, s2tA_in_ga(T244, T263))
U19_GAA(T244, T264, T268, s2tA_out_ga(T244, T263)) → U20_GAA(T244, T264, T268, tappendB_in_gaa(node(nil, T266, T263), T264, T267))
U19_GAA(T244, T264, T268, s2tA_out_ga(T244, T263)) → TAPPENDB_IN_GAA(node(nil, T266, T263), T264, T267)
U20_GAA(T244, T264, T268, tappendB_out_gaa(node(nil, T266, T263), T264, T267)) → U21_GAA(T244, T264, T268, tlastC_in_ag(T268, T267))
U20_GAA(T244, T264, T268, tappendB_out_gaa(node(nil, T266, T263), T264, T267)) → TLASTC_IN_AG(T268, T267)
GOALF_IN_GAA(s(T275), T13, T14) → U22_GAA(T275, T13, T14, s2tA_in_ga(T275, X495))
GOALF_IN_GAA(s(T275), T295, T296) → U23_GAA(T275, T295, T296, s2tA_in_ga(T275, T294))
U23_GAA(T275, T295, T296, s2tA_out_ga(T275, T294)) → U24_GAA(T275, T295, T296, tappendB_in_gaa(node(T294, X527, nil), T295, X526))
U23_GAA(T275, T295, T296, s2tA_out_ga(T275, T294)) → TAPPENDB_IN_GAA(node(T294, X527, nil), T295, X526)
GOALF_IN_GAA(s(T275), T295, T299) → U25_GAA(T275, T295, T299, s2tA_in_ga(T275, T294))
U25_GAA(T275, T295, T299, s2tA_out_ga(T275, T294)) → U26_GAA(T275, T295, T299, tappendB_in_gaa(node(T294, T297, nil), T295, T298))
U25_GAA(T275, T295, T299, s2tA_out_ga(T275, T294)) → TAPPENDB_IN_GAA(node(T294, T297, nil), T295, T298)
U26_GAA(T275, T295, T299, tappendB_out_gaa(node(T294, T297, nil), T295, T298)) → U27_GAA(T275, T295, T299, tlastC_in_ag(T299, T298))
U26_GAA(T275, T295, T299, tappendB_out_gaa(node(T294, T297, nil), T295, T298)) → TLASTC_IN_AG(T299, T298)
GOALF_IN_GAA(s(T306), T317, T318) → U28_GAA(T306, T317, T318, pD_in_gaaaa(nil, X569, T317, X568, T318))
GOALF_IN_GAA(s(T306), T317, T318) → PD_IN_GAAAA(nil, X569, T317, X568, T318)
GOALF_IN_GAA(0, T331, T332) → U29_GAA(T331, T332, tappendB_in_gaa(nil, T331, X588))
GOALF_IN_GAA(0, T331, T332) → TAPPENDB_IN_GAA(nil, T331, X588)
GOALF_IN_GAA(0, T331, T336) → U30_GAA(T331, T336, tappendB_in_gaa(nil, T331, T335))
U30_GAA(T331, T336, tappendB_out_gaa(nil, T331, T335)) → U31_GAA(T331, T336, tlastC_in_ag(T336, T335))
U30_GAA(T331, T336, tappendB_out_gaa(nil, T331, T335)) → TLASTC_IN_AG(T336, T335)
goalF_in_gaa(s(T19), T13, T14) → U13_gaa(T19, T13, T14, s2tA_in_ga(T19, X31))
s2tA_in_ga(s(T27), node(X66, X67, X66)) → U1_ga(T27, X66, X67, s2tA_in_ga(T27, X66))
s2tA_in_ga(s(T33), node(nil, X96, X97)) → U2_ga(T33, X96, X97, s2tA_in_ga(T33, X97))
s2tA_in_ga(s(T39), node(X126, X127, nil)) → U3_ga(T39, X126, X127, s2tA_in_ga(T39, X126))
s2tA_in_ga(s(T45), node(nil, X147, nil)) → s2tA_out_ga(s(T45), node(nil, X147, nil))
s2tA_in_ga(0, nil) → s2tA_out_ga(0, nil)
U3_ga(T39, X126, X127, s2tA_out_ga(T39, X126)) → s2tA_out_ga(s(T39), node(X126, X127, nil))
U2_ga(T33, X96, X97, s2tA_out_ga(T33, X97)) → s2tA_out_ga(s(T33), node(nil, X96, X97))
U1_ga(T27, X66, X67, s2tA_out_ga(T27, X66)) → s2tA_out_ga(s(T27), node(X66, X67, X66))
U13_gaa(T19, T13, T14, s2tA_out_ga(T19, X31)) → goalF_out_gaa(s(T19), T13, T14)
goalF_in_gaa(s(T19), T62, T63) → U14_gaa(T19, T62, T63, s2tA_in_ga(T19, T61))
U14_gaa(T19, T62, T63, s2tA_out_ga(T19, T61)) → U15_gaa(T19, T62, T63, pD_in_gaaaa(T61, X168, T62, X167, T63))
pD_in_gaaaa(T61, X168, T62, X167, T63) → U8_gaaaa(T61, X168, T62, X167, T63, tappendE_in_gaaa(T61, X168, T62, X167))
tappendE_in_gaaa(nil, X193, T71, node(node(nil, T71, nil), X193, nil)) → tappendE_out_gaaa(nil, X193, T71, node(node(nil, T71, nil), X193, nil))
tappendE_in_gaaa(nil, X213, T81, node(nil, X213, node(nil, T81, nil))) → tappendE_out_gaaa(nil, X213, T81, node(nil, X213, node(nil, T81, nil)))
tappendE_in_gaaa(T100, X251, T101, node(X252, X251, T100)) → U11_gaaa(T100, X251, T101, X252, tappendB_in_gaa(T100, T101, X252))
tappendB_in_gaa(nil, T108, node(nil, T108, nil)) → tappendB_out_gaa(nil, T108, node(nil, T108, nil))
tappendB_in_gaa(node(nil, T121, T122), T123, node(node(nil, T123, nil), T121, T122)) → tappendB_out_gaa(node(nil, T121, T122), T123, node(node(nil, T123, nil), T121, T122))
tappendB_in_gaa(node(T136, T137, nil), T138, node(T136, T137, node(nil, T138, nil))) → tappendB_out_gaa(node(T136, T137, nil), T138, node(T136, T137, node(nil, T138, nil)))
tappendB_in_gaa(node(T159, T156, T157), T160, node(X319, T156, T157)) → U4_gaa(T159, T156, T157, T160, X319, tappendB_in_gaa(T159, T160, X319))
tappendB_in_gaa(node(T171, T172, T175), T176, node(T171, T172, X339)) → U5_gaa(T171, T172, T175, T176, X339, tappendB_in_gaa(T175, T176, X339))
U5_gaa(T171, T172, T175, T176, X339, tappendB_out_gaa(T175, T176, X339)) → tappendB_out_gaa(node(T171, T172, T175), T176, node(T171, T172, X339))
U4_gaa(T159, T156, T157, T160, X319, tappendB_out_gaa(T159, T160, X319)) → tappendB_out_gaa(node(T159, T156, T157), T160, node(X319, T156, T157))
U11_gaaa(T100, X251, T101, X252, tappendB_out_gaa(T100, T101, X252)) → tappendE_out_gaaa(T100, X251, T101, node(X252, X251, T100))
tappendE_in_gaaa(T189, X363, T190, node(T189, X363, X364)) → U12_gaaa(T189, X363, T190, X364, tappendB_in_gaa(T189, T190, X364))
U12_gaaa(T189, X363, T190, X364, tappendB_out_gaa(T189, T190, X364)) → tappendE_out_gaaa(T189, X363, T190, node(T189, X363, X364))
U8_gaaaa(T61, X168, T62, X167, T63, tappendE_out_gaaa(T61, X168, T62, X167)) → pD_out_gaaaa(T61, X168, T62, X167, T63)
pD_in_gaaaa(T61, T64, T62, T65, T66) → U9_gaaaa(T61, T64, T62, T65, T66, tappendE_in_gaaa(T61, T64, T62, T65))
U9_gaaaa(T61, T64, T62, T65, T66, tappendE_out_gaaa(T61, T64, T62, T65)) → U10_gaaaa(T61, T64, T62, T65, T66, tlastC_in_ag(T66, T65))
tlastC_in_ag(T199, node(nil, T199, nil)) → tlastC_out_ag(T199, node(nil, T199, nil))
tlastC_in_ag(T220, node(T221, T218, T219)) → U6_ag(T220, T221, T218, T219, tlastC_in_ag(T220, T221))
tlastC_in_ag(T236, node(T233, T234, T237)) → U7_ag(T236, T233, T234, T237, tlastC_in_ag(T236, T237))
U7_ag(T236, T233, T234, T237, tlastC_out_ag(T236, T237)) → tlastC_out_ag(T236, node(T233, T234, T237))
U6_ag(T220, T221, T218, T219, tlastC_out_ag(T220, T221)) → tlastC_out_ag(T220, node(T221, T218, T219))
U10_gaaaa(T61, T64, T62, T65, T66, tlastC_out_ag(T66, T65)) → pD_out_gaaaa(T61, T64, T62, T65, T66)
U15_gaa(T19, T62, T63, pD_out_gaaaa(T61, X168, T62, X167, T63)) → goalF_out_gaa(s(T19), T62, T63)
goalF_in_gaa(s(T244), T13, T14) → U16_gaa(T244, T13, T14, s2tA_in_ga(T244, X434))
U16_gaa(T244, T13, T14, s2tA_out_ga(T244, X434)) → goalF_out_gaa(s(T244), T13, T14)
goalF_in_gaa(s(T244), T264, T265) → U17_gaa(T244, T264, T265, s2tA_in_ga(T244, T263))
U17_gaa(T244, T264, T265, s2tA_out_ga(T244, T263)) → U18_gaa(T244, T264, T265, tappendB_in_gaa(node(nil, X465, T263), T264, X464))
U18_gaa(T244, T264, T265, tappendB_out_gaa(node(nil, X465, T263), T264, X464)) → goalF_out_gaa(s(T244), T264, T265)
goalF_in_gaa(s(T244), T264, T268) → U19_gaa(T244, T264, T268, s2tA_in_ga(T244, T263))
U19_gaa(T244, T264, T268, s2tA_out_ga(T244, T263)) → U20_gaa(T244, T264, T268, tappendB_in_gaa(node(nil, T266, T263), T264, T267))
U20_gaa(T244, T264, T268, tappendB_out_gaa(node(nil, T266, T263), T264, T267)) → U21_gaa(T244, T264, T268, tlastC_in_ag(T268, T267))
U21_gaa(T244, T264, T268, tlastC_out_ag(T268, T267)) → goalF_out_gaa(s(T244), T264, T268)
goalF_in_gaa(s(T275), T13, T14) → U22_gaa(T275, T13, T14, s2tA_in_ga(T275, X495))
U22_gaa(T275, T13, T14, s2tA_out_ga(T275, X495)) → goalF_out_gaa(s(T275), T13, T14)
goalF_in_gaa(s(T275), T295, T296) → U23_gaa(T275, T295, T296, s2tA_in_ga(T275, T294))
U23_gaa(T275, T295, T296, s2tA_out_ga(T275, T294)) → U24_gaa(T275, T295, T296, tappendB_in_gaa(node(T294, X527, nil), T295, X526))
U24_gaa(T275, T295, T296, tappendB_out_gaa(node(T294, X527, nil), T295, X526)) → goalF_out_gaa(s(T275), T295, T296)
goalF_in_gaa(s(T275), T295, T299) → U25_gaa(T275, T295, T299, s2tA_in_ga(T275, T294))
U25_gaa(T275, T295, T299, s2tA_out_ga(T275, T294)) → U26_gaa(T275, T295, T299, tappendB_in_gaa(node(T294, T297, nil), T295, T298))
U26_gaa(T275, T295, T299, tappendB_out_gaa(node(T294, T297, nil), T295, T298)) → U27_gaa(T275, T295, T299, tlastC_in_ag(T299, T298))
U27_gaa(T275, T295, T299, tlastC_out_ag(T299, T298)) → goalF_out_gaa(s(T275), T295, T299)
goalF_in_gaa(s(T306), T317, T318) → U28_gaa(T306, T317, T318, pD_in_gaaaa(nil, X569, T317, X568, T318))
U28_gaa(T306, T317, T318, pD_out_gaaaa(nil, X569, T317, X568, T318)) → goalF_out_gaa(s(T306), T317, T318)
goalF_in_gaa(0, T331, T332) → U29_gaa(T331, T332, tappendB_in_gaa(nil, T331, X588))
U29_gaa(T331, T332, tappendB_out_gaa(nil, T331, X588)) → goalF_out_gaa(0, T331, T332)
goalF_in_gaa(0, T331, T336) → U30_gaa(T331, T336, tappendB_in_gaa(nil, T331, T335))
U30_gaa(T331, T336, tappendB_out_gaa(nil, T331, T335)) → U31_gaa(T331, T336, tlastC_in_ag(T336, T335))
U31_gaa(T331, T336, tlastC_out_ag(T336, T335)) → goalF_out_gaa(0, T331, T336)
GOALF_IN_GAA(s(T19), T13, T14) → U13_GAA(T19, T13, T14, s2tA_in_ga(T19, X31))
GOALF_IN_GAA(s(T19), T13, T14) → S2TA_IN_GA(T19, X31)
S2TA_IN_GA(s(T27), node(X66, X67, X66)) → U1_GA(T27, X66, X67, s2tA_in_ga(T27, X66))
S2TA_IN_GA(s(T27), node(X66, X67, X66)) → S2TA_IN_GA(T27, X66)
S2TA_IN_GA(s(T33), node(nil, X96, X97)) → U2_GA(T33, X96, X97, s2tA_in_ga(T33, X97))
S2TA_IN_GA(s(T33), node(nil, X96, X97)) → S2TA_IN_GA(T33, X97)
S2TA_IN_GA(s(T39), node(X126, X127, nil)) → U3_GA(T39, X126, X127, s2tA_in_ga(T39, X126))
S2TA_IN_GA(s(T39), node(X126, X127, nil)) → S2TA_IN_GA(T39, X126)
GOALF_IN_GAA(s(T19), T62, T63) → U14_GAA(T19, T62, T63, s2tA_in_ga(T19, T61))
U14_GAA(T19, T62, T63, s2tA_out_ga(T19, T61)) → U15_GAA(T19, T62, T63, pD_in_gaaaa(T61, X168, T62, X167, T63))
U14_GAA(T19, T62, T63, s2tA_out_ga(T19, T61)) → PD_IN_GAAAA(T61, X168, T62, X167, T63)
PD_IN_GAAAA(T61, X168, T62, X167, T63) → U8_GAAAA(T61, X168, T62, X167, T63, tappendE_in_gaaa(T61, X168, T62, X167))
PD_IN_GAAAA(T61, X168, T62, X167, T63) → TAPPENDE_IN_GAAA(T61, X168, T62, X167)
TAPPENDE_IN_GAAA(T100, X251, T101, node(X252, X251, T100)) → U11_GAAA(T100, X251, T101, X252, tappendB_in_gaa(T100, T101, X252))
TAPPENDE_IN_GAAA(T100, X251, T101, node(X252, X251, T100)) → TAPPENDB_IN_GAA(T100, T101, X252)
TAPPENDB_IN_GAA(node(T159, T156, T157), T160, node(X319, T156, T157)) → U4_GAA(T159, T156, T157, T160, X319, tappendB_in_gaa(T159, T160, X319))
TAPPENDB_IN_GAA(node(T159, T156, T157), T160, node(X319, T156, T157)) → TAPPENDB_IN_GAA(T159, T160, X319)
TAPPENDB_IN_GAA(node(T171, T172, T175), T176, node(T171, T172, X339)) → U5_GAA(T171, T172, T175, T176, X339, tappendB_in_gaa(T175, T176, X339))
TAPPENDB_IN_GAA(node(T171, T172, T175), T176, node(T171, T172, X339)) → TAPPENDB_IN_GAA(T175, T176, X339)
TAPPENDE_IN_GAAA(T189, X363, T190, node(T189, X363, X364)) → U12_GAAA(T189, X363, T190, X364, tappendB_in_gaa(T189, T190, X364))
TAPPENDE_IN_GAAA(T189, X363, T190, node(T189, X363, X364)) → TAPPENDB_IN_GAA(T189, T190, X364)
PD_IN_GAAAA(T61, T64, T62, T65, T66) → U9_GAAAA(T61, T64, T62, T65, T66, tappendE_in_gaaa(T61, T64, T62, T65))
U9_GAAAA(T61, T64, T62, T65, T66, tappendE_out_gaaa(T61, T64, T62, T65)) → U10_GAAAA(T61, T64, T62, T65, T66, tlastC_in_ag(T66, T65))
U9_GAAAA(T61, T64, T62, T65, T66, tappendE_out_gaaa(T61, T64, T62, T65)) → TLASTC_IN_AG(T66, T65)
TLASTC_IN_AG(T220, node(T221, T218, T219)) → U6_AG(T220, T221, T218, T219, tlastC_in_ag(T220, T221))
TLASTC_IN_AG(T220, node(T221, T218, T219)) → TLASTC_IN_AG(T220, T221)
TLASTC_IN_AG(T236, node(T233, T234, T237)) → U7_AG(T236, T233, T234, T237, tlastC_in_ag(T236, T237))
TLASTC_IN_AG(T236, node(T233, T234, T237)) → TLASTC_IN_AG(T236, T237)
GOALF_IN_GAA(s(T244), T13, T14) → U16_GAA(T244, T13, T14, s2tA_in_ga(T244, X434))
GOALF_IN_GAA(s(T244), T264, T265) → U17_GAA(T244, T264, T265, s2tA_in_ga(T244, T263))
U17_GAA(T244, T264, T265, s2tA_out_ga(T244, T263)) → U18_GAA(T244, T264, T265, tappendB_in_gaa(node(nil, X465, T263), T264, X464))
U17_GAA(T244, T264, T265, s2tA_out_ga(T244, T263)) → TAPPENDB_IN_GAA(node(nil, X465, T263), T264, X464)
GOALF_IN_GAA(s(T244), T264, T268) → U19_GAA(T244, T264, T268, s2tA_in_ga(T244, T263))
U19_GAA(T244, T264, T268, s2tA_out_ga(T244, T263)) → U20_GAA(T244, T264, T268, tappendB_in_gaa(node(nil, T266, T263), T264, T267))
U19_GAA(T244, T264, T268, s2tA_out_ga(T244, T263)) → TAPPENDB_IN_GAA(node(nil, T266, T263), T264, T267)
U20_GAA(T244, T264, T268, tappendB_out_gaa(node(nil, T266, T263), T264, T267)) → U21_GAA(T244, T264, T268, tlastC_in_ag(T268, T267))
U20_GAA(T244, T264, T268, tappendB_out_gaa(node(nil, T266, T263), T264, T267)) → TLASTC_IN_AG(T268, T267)
GOALF_IN_GAA(s(T275), T13, T14) → U22_GAA(T275, T13, T14, s2tA_in_ga(T275, X495))
GOALF_IN_GAA(s(T275), T295, T296) → U23_GAA(T275, T295, T296, s2tA_in_ga(T275, T294))
U23_GAA(T275, T295, T296, s2tA_out_ga(T275, T294)) → U24_GAA(T275, T295, T296, tappendB_in_gaa(node(T294, X527, nil), T295, X526))
U23_GAA(T275, T295, T296, s2tA_out_ga(T275, T294)) → TAPPENDB_IN_GAA(node(T294, X527, nil), T295, X526)
GOALF_IN_GAA(s(T275), T295, T299) → U25_GAA(T275, T295, T299, s2tA_in_ga(T275, T294))
U25_GAA(T275, T295, T299, s2tA_out_ga(T275, T294)) → U26_GAA(T275, T295, T299, tappendB_in_gaa(node(T294, T297, nil), T295, T298))
U25_GAA(T275, T295, T299, s2tA_out_ga(T275, T294)) → TAPPENDB_IN_GAA(node(T294, T297, nil), T295, T298)
U26_GAA(T275, T295, T299, tappendB_out_gaa(node(T294, T297, nil), T295, T298)) → U27_GAA(T275, T295, T299, tlastC_in_ag(T299, T298))
U26_GAA(T275, T295, T299, tappendB_out_gaa(node(T294, T297, nil), T295, T298)) → TLASTC_IN_AG(T299, T298)
GOALF_IN_GAA(s(T306), T317, T318) → U28_GAA(T306, T317, T318, pD_in_gaaaa(nil, X569, T317, X568, T318))
GOALF_IN_GAA(s(T306), T317, T318) → PD_IN_GAAAA(nil, X569, T317, X568, T318)
GOALF_IN_GAA(0, T331, T332) → U29_GAA(T331, T332, tappendB_in_gaa(nil, T331, X588))
GOALF_IN_GAA(0, T331, T332) → TAPPENDB_IN_GAA(nil, T331, X588)
GOALF_IN_GAA(0, T331, T336) → U30_GAA(T331, T336, tappendB_in_gaa(nil, T331, T335))
U30_GAA(T331, T336, tappendB_out_gaa(nil, T331, T335)) → U31_GAA(T331, T336, tlastC_in_ag(T336, T335))
U30_GAA(T331, T336, tappendB_out_gaa(nil, T331, T335)) → TLASTC_IN_AG(T336, T335)
goalF_in_gaa(s(T19), T13, T14) → U13_gaa(T19, T13, T14, s2tA_in_ga(T19, X31))
s2tA_in_ga(s(T27), node(X66, X67, X66)) → U1_ga(T27, X66, X67, s2tA_in_ga(T27, X66))
s2tA_in_ga(s(T33), node(nil, X96, X97)) → U2_ga(T33, X96, X97, s2tA_in_ga(T33, X97))
s2tA_in_ga(s(T39), node(X126, X127, nil)) → U3_ga(T39, X126, X127, s2tA_in_ga(T39, X126))
s2tA_in_ga(s(T45), node(nil, X147, nil)) → s2tA_out_ga(s(T45), node(nil, X147, nil))
s2tA_in_ga(0, nil) → s2tA_out_ga(0, nil)
U3_ga(T39, X126, X127, s2tA_out_ga(T39, X126)) → s2tA_out_ga(s(T39), node(X126, X127, nil))
U2_ga(T33, X96, X97, s2tA_out_ga(T33, X97)) → s2tA_out_ga(s(T33), node(nil, X96, X97))
U1_ga(T27, X66, X67, s2tA_out_ga(T27, X66)) → s2tA_out_ga(s(T27), node(X66, X67, X66))
U13_gaa(T19, T13, T14, s2tA_out_ga(T19, X31)) → goalF_out_gaa(s(T19), T13, T14)
goalF_in_gaa(s(T19), T62, T63) → U14_gaa(T19, T62, T63, s2tA_in_ga(T19, T61))
U14_gaa(T19, T62, T63, s2tA_out_ga(T19, T61)) → U15_gaa(T19, T62, T63, pD_in_gaaaa(T61, X168, T62, X167, T63))
pD_in_gaaaa(T61, X168, T62, X167, T63) → U8_gaaaa(T61, X168, T62, X167, T63, tappendE_in_gaaa(T61, X168, T62, X167))
tappendE_in_gaaa(nil, X193, T71, node(node(nil, T71, nil), X193, nil)) → tappendE_out_gaaa(nil, X193, T71, node(node(nil, T71, nil), X193, nil))
tappendE_in_gaaa(nil, X213, T81, node(nil, X213, node(nil, T81, nil))) → tappendE_out_gaaa(nil, X213, T81, node(nil, X213, node(nil, T81, nil)))
tappendE_in_gaaa(T100, X251, T101, node(X252, X251, T100)) → U11_gaaa(T100, X251, T101, X252, tappendB_in_gaa(T100, T101, X252))
tappendB_in_gaa(nil, T108, node(nil, T108, nil)) → tappendB_out_gaa(nil, T108, node(nil, T108, nil))
tappendB_in_gaa(node(nil, T121, T122), T123, node(node(nil, T123, nil), T121, T122)) → tappendB_out_gaa(node(nil, T121, T122), T123, node(node(nil, T123, nil), T121, T122))
tappendB_in_gaa(node(T136, T137, nil), T138, node(T136, T137, node(nil, T138, nil))) → tappendB_out_gaa(node(T136, T137, nil), T138, node(T136, T137, node(nil, T138, nil)))
tappendB_in_gaa(node(T159, T156, T157), T160, node(X319, T156, T157)) → U4_gaa(T159, T156, T157, T160, X319, tappendB_in_gaa(T159, T160, X319))
tappendB_in_gaa(node(T171, T172, T175), T176, node(T171, T172, X339)) → U5_gaa(T171, T172, T175, T176, X339, tappendB_in_gaa(T175, T176, X339))
U5_gaa(T171, T172, T175, T176, X339, tappendB_out_gaa(T175, T176, X339)) → tappendB_out_gaa(node(T171, T172, T175), T176, node(T171, T172, X339))
U4_gaa(T159, T156, T157, T160, X319, tappendB_out_gaa(T159, T160, X319)) → tappendB_out_gaa(node(T159, T156, T157), T160, node(X319, T156, T157))
U11_gaaa(T100, X251, T101, X252, tappendB_out_gaa(T100, T101, X252)) → tappendE_out_gaaa(T100, X251, T101, node(X252, X251, T100))
tappendE_in_gaaa(T189, X363, T190, node(T189, X363, X364)) → U12_gaaa(T189, X363, T190, X364, tappendB_in_gaa(T189, T190, X364))
U12_gaaa(T189, X363, T190, X364, tappendB_out_gaa(T189, T190, X364)) → tappendE_out_gaaa(T189, X363, T190, node(T189, X363, X364))
U8_gaaaa(T61, X168, T62, X167, T63, tappendE_out_gaaa(T61, X168, T62, X167)) → pD_out_gaaaa(T61, X168, T62, X167, T63)
pD_in_gaaaa(T61, T64, T62, T65, T66) → U9_gaaaa(T61, T64, T62, T65, T66, tappendE_in_gaaa(T61, T64, T62, T65))
U9_gaaaa(T61, T64, T62, T65, T66, tappendE_out_gaaa(T61, T64, T62, T65)) → U10_gaaaa(T61, T64, T62, T65, T66, tlastC_in_ag(T66, T65))
tlastC_in_ag(T199, node(nil, T199, nil)) → tlastC_out_ag(T199, node(nil, T199, nil))
tlastC_in_ag(T220, node(T221, T218, T219)) → U6_ag(T220, T221, T218, T219, tlastC_in_ag(T220, T221))
tlastC_in_ag(T236, node(T233, T234, T237)) → U7_ag(T236, T233, T234, T237, tlastC_in_ag(T236, T237))
U7_ag(T236, T233, T234, T237, tlastC_out_ag(T236, T237)) → tlastC_out_ag(T236, node(T233, T234, T237))
U6_ag(T220, T221, T218, T219, tlastC_out_ag(T220, T221)) → tlastC_out_ag(T220, node(T221, T218, T219))
U10_gaaaa(T61, T64, T62, T65, T66, tlastC_out_ag(T66, T65)) → pD_out_gaaaa(T61, T64, T62, T65, T66)
U15_gaa(T19, T62, T63, pD_out_gaaaa(T61, X168, T62, X167, T63)) → goalF_out_gaa(s(T19), T62, T63)
goalF_in_gaa(s(T244), T13, T14) → U16_gaa(T244, T13, T14, s2tA_in_ga(T244, X434))
U16_gaa(T244, T13, T14, s2tA_out_ga(T244, X434)) → goalF_out_gaa(s(T244), T13, T14)
goalF_in_gaa(s(T244), T264, T265) → U17_gaa(T244, T264, T265, s2tA_in_ga(T244, T263))
U17_gaa(T244, T264, T265, s2tA_out_ga(T244, T263)) → U18_gaa(T244, T264, T265, tappendB_in_gaa(node(nil, X465, T263), T264, X464))
U18_gaa(T244, T264, T265, tappendB_out_gaa(node(nil, X465, T263), T264, X464)) → goalF_out_gaa(s(T244), T264, T265)
goalF_in_gaa(s(T244), T264, T268) → U19_gaa(T244, T264, T268, s2tA_in_ga(T244, T263))
U19_gaa(T244, T264, T268, s2tA_out_ga(T244, T263)) → U20_gaa(T244, T264, T268, tappendB_in_gaa(node(nil, T266, T263), T264, T267))
U20_gaa(T244, T264, T268, tappendB_out_gaa(node(nil, T266, T263), T264, T267)) → U21_gaa(T244, T264, T268, tlastC_in_ag(T268, T267))
U21_gaa(T244, T264, T268, tlastC_out_ag(T268, T267)) → goalF_out_gaa(s(T244), T264, T268)
goalF_in_gaa(s(T275), T13, T14) → U22_gaa(T275, T13, T14, s2tA_in_ga(T275, X495))
U22_gaa(T275, T13, T14, s2tA_out_ga(T275, X495)) → goalF_out_gaa(s(T275), T13, T14)
goalF_in_gaa(s(T275), T295, T296) → U23_gaa(T275, T295, T296, s2tA_in_ga(T275, T294))
U23_gaa(T275, T295, T296, s2tA_out_ga(T275, T294)) → U24_gaa(T275, T295, T296, tappendB_in_gaa(node(T294, X527, nil), T295, X526))
U24_gaa(T275, T295, T296, tappendB_out_gaa(node(T294, X527, nil), T295, X526)) → goalF_out_gaa(s(T275), T295, T296)
goalF_in_gaa(s(T275), T295, T299) → U25_gaa(T275, T295, T299, s2tA_in_ga(T275, T294))
U25_gaa(T275, T295, T299, s2tA_out_ga(T275, T294)) → U26_gaa(T275, T295, T299, tappendB_in_gaa(node(T294, T297, nil), T295, T298))
U26_gaa(T275, T295, T299, tappendB_out_gaa(node(T294, T297, nil), T295, T298)) → U27_gaa(T275, T295, T299, tlastC_in_ag(T299, T298))
U27_gaa(T275, T295, T299, tlastC_out_ag(T299, T298)) → goalF_out_gaa(s(T275), T295, T299)
goalF_in_gaa(s(T306), T317, T318) → U28_gaa(T306, T317, T318, pD_in_gaaaa(nil, X569, T317, X568, T318))
U28_gaa(T306, T317, T318, pD_out_gaaaa(nil, X569, T317, X568, T318)) → goalF_out_gaa(s(T306), T317, T318)
goalF_in_gaa(0, T331, T332) → U29_gaa(T331, T332, tappendB_in_gaa(nil, T331, X588))
U29_gaa(T331, T332, tappendB_out_gaa(nil, T331, X588)) → goalF_out_gaa(0, T331, T332)
goalF_in_gaa(0, T331, T336) → U30_gaa(T331, T336, tappendB_in_gaa(nil, T331, T335))
U30_gaa(T331, T336, tappendB_out_gaa(nil, T331, T335)) → U31_gaa(T331, T336, tlastC_in_ag(T336, T335))
U31_gaa(T331, T336, tlastC_out_ag(T336, T335)) → goalF_out_gaa(0, T331, T336)
TLASTC_IN_AG(T236, node(T233, T234, T237)) → TLASTC_IN_AG(T236, T237)
TLASTC_IN_AG(T220, node(T221, T218, T219)) → TLASTC_IN_AG(T220, T221)
goalF_in_gaa(s(T19), T13, T14) → U13_gaa(T19, T13, T14, s2tA_in_ga(T19, X31))
s2tA_in_ga(s(T27), node(X66, X67, X66)) → U1_ga(T27, X66, X67, s2tA_in_ga(T27, X66))
s2tA_in_ga(s(T33), node(nil, X96, X97)) → U2_ga(T33, X96, X97, s2tA_in_ga(T33, X97))
s2tA_in_ga(s(T39), node(X126, X127, nil)) → U3_ga(T39, X126, X127, s2tA_in_ga(T39, X126))
s2tA_in_ga(s(T45), node(nil, X147, nil)) → s2tA_out_ga(s(T45), node(nil, X147, nil))
s2tA_in_ga(0, nil) → s2tA_out_ga(0, nil)
U3_ga(T39, X126, X127, s2tA_out_ga(T39, X126)) → s2tA_out_ga(s(T39), node(X126, X127, nil))
U2_ga(T33, X96, X97, s2tA_out_ga(T33, X97)) → s2tA_out_ga(s(T33), node(nil, X96, X97))
U1_ga(T27, X66, X67, s2tA_out_ga(T27, X66)) → s2tA_out_ga(s(T27), node(X66, X67, X66))
U13_gaa(T19, T13, T14, s2tA_out_ga(T19, X31)) → goalF_out_gaa(s(T19), T13, T14)
goalF_in_gaa(s(T19), T62, T63) → U14_gaa(T19, T62, T63, s2tA_in_ga(T19, T61))
U14_gaa(T19, T62, T63, s2tA_out_ga(T19, T61)) → U15_gaa(T19, T62, T63, pD_in_gaaaa(T61, X168, T62, X167, T63))
pD_in_gaaaa(T61, X168, T62, X167, T63) → U8_gaaaa(T61, X168, T62, X167, T63, tappendE_in_gaaa(T61, X168, T62, X167))
tappendE_in_gaaa(nil, X193, T71, node(node(nil, T71, nil), X193, nil)) → tappendE_out_gaaa(nil, X193, T71, node(node(nil, T71, nil), X193, nil))
tappendE_in_gaaa(nil, X213, T81, node(nil, X213, node(nil, T81, nil))) → tappendE_out_gaaa(nil, X213, T81, node(nil, X213, node(nil, T81, nil)))
tappendE_in_gaaa(T100, X251, T101, node(X252, X251, T100)) → U11_gaaa(T100, X251, T101, X252, tappendB_in_gaa(T100, T101, X252))
tappendB_in_gaa(nil, T108, node(nil, T108, nil)) → tappendB_out_gaa(nil, T108, node(nil, T108, nil))
tappendB_in_gaa(node(nil, T121, T122), T123, node(node(nil, T123, nil), T121, T122)) → tappendB_out_gaa(node(nil, T121, T122), T123, node(node(nil, T123, nil), T121, T122))
tappendB_in_gaa(node(T136, T137, nil), T138, node(T136, T137, node(nil, T138, nil))) → tappendB_out_gaa(node(T136, T137, nil), T138, node(T136, T137, node(nil, T138, nil)))
tappendB_in_gaa(node(T159, T156, T157), T160, node(X319, T156, T157)) → U4_gaa(T159, T156, T157, T160, X319, tappendB_in_gaa(T159, T160, X319))
tappendB_in_gaa(node(T171, T172, T175), T176, node(T171, T172, X339)) → U5_gaa(T171, T172, T175, T176, X339, tappendB_in_gaa(T175, T176, X339))
U5_gaa(T171, T172, T175, T176, X339, tappendB_out_gaa(T175, T176, X339)) → tappendB_out_gaa(node(T171, T172, T175), T176, node(T171, T172, X339))
U4_gaa(T159, T156, T157, T160, X319, tappendB_out_gaa(T159, T160, X319)) → tappendB_out_gaa(node(T159, T156, T157), T160, node(X319, T156, T157))
U11_gaaa(T100, X251, T101, X252, tappendB_out_gaa(T100, T101, X252)) → tappendE_out_gaaa(T100, X251, T101, node(X252, X251, T100))
tappendE_in_gaaa(T189, X363, T190, node(T189, X363, X364)) → U12_gaaa(T189, X363, T190, X364, tappendB_in_gaa(T189, T190, X364))
U12_gaaa(T189, X363, T190, X364, tappendB_out_gaa(T189, T190, X364)) → tappendE_out_gaaa(T189, X363, T190, node(T189, X363, X364))
U8_gaaaa(T61, X168, T62, X167, T63, tappendE_out_gaaa(T61, X168, T62, X167)) → pD_out_gaaaa(T61, X168, T62, X167, T63)
pD_in_gaaaa(T61, T64, T62, T65, T66) → U9_gaaaa(T61, T64, T62, T65, T66, tappendE_in_gaaa(T61, T64, T62, T65))
U9_gaaaa(T61, T64, T62, T65, T66, tappendE_out_gaaa(T61, T64, T62, T65)) → U10_gaaaa(T61, T64, T62, T65, T66, tlastC_in_ag(T66, T65))
tlastC_in_ag(T199, node(nil, T199, nil)) → tlastC_out_ag(T199, node(nil, T199, nil))
tlastC_in_ag(T220, node(T221, T218, T219)) → U6_ag(T220, T221, T218, T219, tlastC_in_ag(T220, T221))
tlastC_in_ag(T236, node(T233, T234, T237)) → U7_ag(T236, T233, T234, T237, tlastC_in_ag(T236, T237))
U7_ag(T236, T233, T234, T237, tlastC_out_ag(T236, T237)) → tlastC_out_ag(T236, node(T233, T234, T237))
U6_ag(T220, T221, T218, T219, tlastC_out_ag(T220, T221)) → tlastC_out_ag(T220, node(T221, T218, T219))
U10_gaaaa(T61, T64, T62, T65, T66, tlastC_out_ag(T66, T65)) → pD_out_gaaaa(T61, T64, T62, T65, T66)
U15_gaa(T19, T62, T63, pD_out_gaaaa(T61, X168, T62, X167, T63)) → goalF_out_gaa(s(T19), T62, T63)
goalF_in_gaa(s(T244), T13, T14) → U16_gaa(T244, T13, T14, s2tA_in_ga(T244, X434))
U16_gaa(T244, T13, T14, s2tA_out_ga(T244, X434)) → goalF_out_gaa(s(T244), T13, T14)
goalF_in_gaa(s(T244), T264, T265) → U17_gaa(T244, T264, T265, s2tA_in_ga(T244, T263))
U17_gaa(T244, T264, T265, s2tA_out_ga(T244, T263)) → U18_gaa(T244, T264, T265, tappendB_in_gaa(node(nil, X465, T263), T264, X464))
U18_gaa(T244, T264, T265, tappendB_out_gaa(node(nil, X465, T263), T264, X464)) → goalF_out_gaa(s(T244), T264, T265)
goalF_in_gaa(s(T244), T264, T268) → U19_gaa(T244, T264, T268, s2tA_in_ga(T244, T263))
U19_gaa(T244, T264, T268, s2tA_out_ga(T244, T263)) → U20_gaa(T244, T264, T268, tappendB_in_gaa(node(nil, T266, T263), T264, T267))
U20_gaa(T244, T264, T268, tappendB_out_gaa(node(nil, T266, T263), T264, T267)) → U21_gaa(T244, T264, T268, tlastC_in_ag(T268, T267))
U21_gaa(T244, T264, T268, tlastC_out_ag(T268, T267)) → goalF_out_gaa(s(T244), T264, T268)
goalF_in_gaa(s(T275), T13, T14) → U22_gaa(T275, T13, T14, s2tA_in_ga(T275, X495))
U22_gaa(T275, T13, T14, s2tA_out_ga(T275, X495)) → goalF_out_gaa(s(T275), T13, T14)
goalF_in_gaa(s(T275), T295, T296) → U23_gaa(T275, T295, T296, s2tA_in_ga(T275, T294))
U23_gaa(T275, T295, T296, s2tA_out_ga(T275, T294)) → U24_gaa(T275, T295, T296, tappendB_in_gaa(node(T294, X527, nil), T295, X526))
U24_gaa(T275, T295, T296, tappendB_out_gaa(node(T294, X527, nil), T295, X526)) → goalF_out_gaa(s(T275), T295, T296)
goalF_in_gaa(s(T275), T295, T299) → U25_gaa(T275, T295, T299, s2tA_in_ga(T275, T294))
U25_gaa(T275, T295, T299, s2tA_out_ga(T275, T294)) → U26_gaa(T275, T295, T299, tappendB_in_gaa(node(T294, T297, nil), T295, T298))
U26_gaa(T275, T295, T299, tappendB_out_gaa(node(T294, T297, nil), T295, T298)) → U27_gaa(T275, T295, T299, tlastC_in_ag(T299, T298))
U27_gaa(T275, T295, T299, tlastC_out_ag(T299, T298)) → goalF_out_gaa(s(T275), T295, T299)
goalF_in_gaa(s(T306), T317, T318) → U28_gaa(T306, T317, T318, pD_in_gaaaa(nil, X569, T317, X568, T318))
U28_gaa(T306, T317, T318, pD_out_gaaaa(nil, X569, T317, X568, T318)) → goalF_out_gaa(s(T306), T317, T318)
goalF_in_gaa(0, T331, T332) → U29_gaa(T331, T332, tappendB_in_gaa(nil, T331, X588))
U29_gaa(T331, T332, tappendB_out_gaa(nil, T331, X588)) → goalF_out_gaa(0, T331, T332)
goalF_in_gaa(0, T331, T336) → U30_gaa(T331, T336, tappendB_in_gaa(nil, T331, T335))
U30_gaa(T331, T336, tappendB_out_gaa(nil, T331, T335)) → U31_gaa(T331, T336, tlastC_in_ag(T336, T335))
U31_gaa(T331, T336, tlastC_out_ag(T336, T335)) → goalF_out_gaa(0, T331, T336)
TLASTC_IN_AG(T236, node(T233, T234, T237)) → TLASTC_IN_AG(T236, T237)
TLASTC_IN_AG(T220, node(T221, T218, T219)) → TLASTC_IN_AG(T220, T221)
TLASTC_IN_AG(node(T233, T237)) → TLASTC_IN_AG(T237)
TLASTC_IN_AG(node(T221, T219)) → TLASTC_IN_AG(T221)
From the DPs we obtained the following set of size-change graphs:
TAPPENDB_IN_GAA(node(T171, T172, T175), T176, node(T171, T172, X339)) → TAPPENDB_IN_GAA(T175, T176, X339)
TAPPENDB_IN_GAA(node(T159, T156, T157), T160, node(X319, T156, T157)) → TAPPENDB_IN_GAA(T159, T160, X319)
goalF_in_gaa(s(T19), T13, T14) → U13_gaa(T19, T13, T14, s2tA_in_ga(T19, X31))
s2tA_in_ga(s(T27), node(X66, X67, X66)) → U1_ga(T27, X66, X67, s2tA_in_ga(T27, X66))
s2tA_in_ga(s(T33), node(nil, X96, X97)) → U2_ga(T33, X96, X97, s2tA_in_ga(T33, X97))
s2tA_in_ga(s(T39), node(X126, X127, nil)) → U3_ga(T39, X126, X127, s2tA_in_ga(T39, X126))
s2tA_in_ga(s(T45), node(nil, X147, nil)) → s2tA_out_ga(s(T45), node(nil, X147, nil))
s2tA_in_ga(0, nil) → s2tA_out_ga(0, nil)
U3_ga(T39, X126, X127, s2tA_out_ga(T39, X126)) → s2tA_out_ga(s(T39), node(X126, X127, nil))
U2_ga(T33, X96, X97, s2tA_out_ga(T33, X97)) → s2tA_out_ga(s(T33), node(nil, X96, X97))
U1_ga(T27, X66, X67, s2tA_out_ga(T27, X66)) → s2tA_out_ga(s(T27), node(X66, X67, X66))
U13_gaa(T19, T13, T14, s2tA_out_ga(T19, X31)) → goalF_out_gaa(s(T19), T13, T14)
goalF_in_gaa(s(T19), T62, T63) → U14_gaa(T19, T62, T63, s2tA_in_ga(T19, T61))
U14_gaa(T19, T62, T63, s2tA_out_ga(T19, T61)) → U15_gaa(T19, T62, T63, pD_in_gaaaa(T61, X168, T62, X167, T63))
pD_in_gaaaa(T61, X168, T62, X167, T63) → U8_gaaaa(T61, X168, T62, X167, T63, tappendE_in_gaaa(T61, X168, T62, X167))
tappendE_in_gaaa(nil, X193, T71, node(node(nil, T71, nil), X193, nil)) → tappendE_out_gaaa(nil, X193, T71, node(node(nil, T71, nil), X193, nil))
tappendE_in_gaaa(nil, X213, T81, node(nil, X213, node(nil, T81, nil))) → tappendE_out_gaaa(nil, X213, T81, node(nil, X213, node(nil, T81, nil)))
tappendE_in_gaaa(T100, X251, T101, node(X252, X251, T100)) → U11_gaaa(T100, X251, T101, X252, tappendB_in_gaa(T100, T101, X252))
tappendB_in_gaa(nil, T108, node(nil, T108, nil)) → tappendB_out_gaa(nil, T108, node(nil, T108, nil))
tappendB_in_gaa(node(nil, T121, T122), T123, node(node(nil, T123, nil), T121, T122)) → tappendB_out_gaa(node(nil, T121, T122), T123, node(node(nil, T123, nil), T121, T122))
tappendB_in_gaa(node(T136, T137, nil), T138, node(T136, T137, node(nil, T138, nil))) → tappendB_out_gaa(node(T136, T137, nil), T138, node(T136, T137, node(nil, T138, nil)))
tappendB_in_gaa(node(T159, T156, T157), T160, node(X319, T156, T157)) → U4_gaa(T159, T156, T157, T160, X319, tappendB_in_gaa(T159, T160, X319))
tappendB_in_gaa(node(T171, T172, T175), T176, node(T171, T172, X339)) → U5_gaa(T171, T172, T175, T176, X339, tappendB_in_gaa(T175, T176, X339))
U5_gaa(T171, T172, T175, T176, X339, tappendB_out_gaa(T175, T176, X339)) → tappendB_out_gaa(node(T171, T172, T175), T176, node(T171, T172, X339))
U4_gaa(T159, T156, T157, T160, X319, tappendB_out_gaa(T159, T160, X319)) → tappendB_out_gaa(node(T159, T156, T157), T160, node(X319, T156, T157))
U11_gaaa(T100, X251, T101, X252, tappendB_out_gaa(T100, T101, X252)) → tappendE_out_gaaa(T100, X251, T101, node(X252, X251, T100))
tappendE_in_gaaa(T189, X363, T190, node(T189, X363, X364)) → U12_gaaa(T189, X363, T190, X364, tappendB_in_gaa(T189, T190, X364))
U12_gaaa(T189, X363, T190, X364, tappendB_out_gaa(T189, T190, X364)) → tappendE_out_gaaa(T189, X363, T190, node(T189, X363, X364))
U8_gaaaa(T61, X168, T62, X167, T63, tappendE_out_gaaa(T61, X168, T62, X167)) → pD_out_gaaaa(T61, X168, T62, X167, T63)
pD_in_gaaaa(T61, T64, T62, T65, T66) → U9_gaaaa(T61, T64, T62, T65, T66, tappendE_in_gaaa(T61, T64, T62, T65))
U9_gaaaa(T61, T64, T62, T65, T66, tappendE_out_gaaa(T61, T64, T62, T65)) → U10_gaaaa(T61, T64, T62, T65, T66, tlastC_in_ag(T66, T65))
tlastC_in_ag(T199, node(nil, T199, nil)) → tlastC_out_ag(T199, node(nil, T199, nil))
tlastC_in_ag(T220, node(T221, T218, T219)) → U6_ag(T220, T221, T218, T219, tlastC_in_ag(T220, T221))
tlastC_in_ag(T236, node(T233, T234, T237)) → U7_ag(T236, T233, T234, T237, tlastC_in_ag(T236, T237))
U7_ag(T236, T233, T234, T237, tlastC_out_ag(T236, T237)) → tlastC_out_ag(T236, node(T233, T234, T237))
U6_ag(T220, T221, T218, T219, tlastC_out_ag(T220, T221)) → tlastC_out_ag(T220, node(T221, T218, T219))
U10_gaaaa(T61, T64, T62, T65, T66, tlastC_out_ag(T66, T65)) → pD_out_gaaaa(T61, T64, T62, T65, T66)
U15_gaa(T19, T62, T63, pD_out_gaaaa(T61, X168, T62, X167, T63)) → goalF_out_gaa(s(T19), T62, T63)
goalF_in_gaa(s(T244), T13, T14) → U16_gaa(T244, T13, T14, s2tA_in_ga(T244, X434))
U16_gaa(T244, T13, T14, s2tA_out_ga(T244, X434)) → goalF_out_gaa(s(T244), T13, T14)
goalF_in_gaa(s(T244), T264, T265) → U17_gaa(T244, T264, T265, s2tA_in_ga(T244, T263))
U17_gaa(T244, T264, T265, s2tA_out_ga(T244, T263)) → U18_gaa(T244, T264, T265, tappendB_in_gaa(node(nil, X465, T263), T264, X464))
U18_gaa(T244, T264, T265, tappendB_out_gaa(node(nil, X465, T263), T264, X464)) → goalF_out_gaa(s(T244), T264, T265)
goalF_in_gaa(s(T244), T264, T268) → U19_gaa(T244, T264, T268, s2tA_in_ga(T244, T263))
U19_gaa(T244, T264, T268, s2tA_out_ga(T244, T263)) → U20_gaa(T244, T264, T268, tappendB_in_gaa(node(nil, T266, T263), T264, T267))
U20_gaa(T244, T264, T268, tappendB_out_gaa(node(nil, T266, T263), T264, T267)) → U21_gaa(T244, T264, T268, tlastC_in_ag(T268, T267))
U21_gaa(T244, T264, T268, tlastC_out_ag(T268, T267)) → goalF_out_gaa(s(T244), T264, T268)
goalF_in_gaa(s(T275), T13, T14) → U22_gaa(T275, T13, T14, s2tA_in_ga(T275, X495))
U22_gaa(T275, T13, T14, s2tA_out_ga(T275, X495)) → goalF_out_gaa(s(T275), T13, T14)
goalF_in_gaa(s(T275), T295, T296) → U23_gaa(T275, T295, T296, s2tA_in_ga(T275, T294))
U23_gaa(T275, T295, T296, s2tA_out_ga(T275, T294)) → U24_gaa(T275, T295, T296, tappendB_in_gaa(node(T294, X527, nil), T295, X526))
U24_gaa(T275, T295, T296, tappendB_out_gaa(node(T294, X527, nil), T295, X526)) → goalF_out_gaa(s(T275), T295, T296)
goalF_in_gaa(s(T275), T295, T299) → U25_gaa(T275, T295, T299, s2tA_in_ga(T275, T294))
U25_gaa(T275, T295, T299, s2tA_out_ga(T275, T294)) → U26_gaa(T275, T295, T299, tappendB_in_gaa(node(T294, T297, nil), T295, T298))
U26_gaa(T275, T295, T299, tappendB_out_gaa(node(T294, T297, nil), T295, T298)) → U27_gaa(T275, T295, T299, tlastC_in_ag(T299, T298))
U27_gaa(T275, T295, T299, tlastC_out_ag(T299, T298)) → goalF_out_gaa(s(T275), T295, T299)
goalF_in_gaa(s(T306), T317, T318) → U28_gaa(T306, T317, T318, pD_in_gaaaa(nil, X569, T317, X568, T318))
U28_gaa(T306, T317, T318, pD_out_gaaaa(nil, X569, T317, X568, T318)) → goalF_out_gaa(s(T306), T317, T318)
goalF_in_gaa(0, T331, T332) → U29_gaa(T331, T332, tappendB_in_gaa(nil, T331, X588))
U29_gaa(T331, T332, tappendB_out_gaa(nil, T331, X588)) → goalF_out_gaa(0, T331, T332)
goalF_in_gaa(0, T331, T336) → U30_gaa(T331, T336, tappendB_in_gaa(nil, T331, T335))
U30_gaa(T331, T336, tappendB_out_gaa(nil, T331, T335)) → U31_gaa(T331, T336, tlastC_in_ag(T336, T335))
U31_gaa(T331, T336, tlastC_out_ag(T336, T335)) → goalF_out_gaa(0, T331, T336)
TAPPENDB_IN_GAA(node(T171, T172, T175), T176, node(T171, T172, X339)) → TAPPENDB_IN_GAA(T175, T176, X339)
TAPPENDB_IN_GAA(node(T159, T156, T157), T160, node(X319, T156, T157)) → TAPPENDB_IN_GAA(T159, T160, X319)
TAPPENDB_IN_GAA(node(T171, T175)) → TAPPENDB_IN_GAA(T175)
TAPPENDB_IN_GAA(node(T159, T157)) → TAPPENDB_IN_GAA(T159)
From the DPs we obtained the following set of size-change graphs:
S2TA_IN_GA(s(T33), node(nil, X96, X97)) → S2TA_IN_GA(T33, X97)
S2TA_IN_GA(s(T27), node(X66, X67, X66)) → S2TA_IN_GA(T27, X66)
S2TA_IN_GA(s(T39), node(X126, X127, nil)) → S2TA_IN_GA(T39, X126)
goalF_in_gaa(s(T19), T13, T14) → U13_gaa(T19, T13, T14, s2tA_in_ga(T19, X31))
s2tA_in_ga(s(T27), node(X66, X67, X66)) → U1_ga(T27, X66, X67, s2tA_in_ga(T27, X66))
s2tA_in_ga(s(T33), node(nil, X96, X97)) → U2_ga(T33, X96, X97, s2tA_in_ga(T33, X97))
s2tA_in_ga(s(T39), node(X126, X127, nil)) → U3_ga(T39, X126, X127, s2tA_in_ga(T39, X126))
s2tA_in_ga(s(T45), node(nil, X147, nil)) → s2tA_out_ga(s(T45), node(nil, X147, nil))
s2tA_in_ga(0, nil) → s2tA_out_ga(0, nil)
U3_ga(T39, X126, X127, s2tA_out_ga(T39, X126)) → s2tA_out_ga(s(T39), node(X126, X127, nil))
U2_ga(T33, X96, X97, s2tA_out_ga(T33, X97)) → s2tA_out_ga(s(T33), node(nil, X96, X97))
U1_ga(T27, X66, X67, s2tA_out_ga(T27, X66)) → s2tA_out_ga(s(T27), node(X66, X67, X66))
U13_gaa(T19, T13, T14, s2tA_out_ga(T19, X31)) → goalF_out_gaa(s(T19), T13, T14)
goalF_in_gaa(s(T19), T62, T63) → U14_gaa(T19, T62, T63, s2tA_in_ga(T19, T61))
U14_gaa(T19, T62, T63, s2tA_out_ga(T19, T61)) → U15_gaa(T19, T62, T63, pD_in_gaaaa(T61, X168, T62, X167, T63))
pD_in_gaaaa(T61, X168, T62, X167, T63) → U8_gaaaa(T61, X168, T62, X167, T63, tappendE_in_gaaa(T61, X168, T62, X167))
tappendE_in_gaaa(nil, X193, T71, node(node(nil, T71, nil), X193, nil)) → tappendE_out_gaaa(nil, X193, T71, node(node(nil, T71, nil), X193, nil))
tappendE_in_gaaa(nil, X213, T81, node(nil, X213, node(nil, T81, nil))) → tappendE_out_gaaa(nil, X213, T81, node(nil, X213, node(nil, T81, nil)))
tappendE_in_gaaa(T100, X251, T101, node(X252, X251, T100)) → U11_gaaa(T100, X251, T101, X252, tappendB_in_gaa(T100, T101, X252))
tappendB_in_gaa(nil, T108, node(nil, T108, nil)) → tappendB_out_gaa(nil, T108, node(nil, T108, nil))
tappendB_in_gaa(node(nil, T121, T122), T123, node(node(nil, T123, nil), T121, T122)) → tappendB_out_gaa(node(nil, T121, T122), T123, node(node(nil, T123, nil), T121, T122))
tappendB_in_gaa(node(T136, T137, nil), T138, node(T136, T137, node(nil, T138, nil))) → tappendB_out_gaa(node(T136, T137, nil), T138, node(T136, T137, node(nil, T138, nil)))
tappendB_in_gaa(node(T159, T156, T157), T160, node(X319, T156, T157)) → U4_gaa(T159, T156, T157, T160, X319, tappendB_in_gaa(T159, T160, X319))
tappendB_in_gaa(node(T171, T172, T175), T176, node(T171, T172, X339)) → U5_gaa(T171, T172, T175, T176, X339, tappendB_in_gaa(T175, T176, X339))
U5_gaa(T171, T172, T175, T176, X339, tappendB_out_gaa(T175, T176, X339)) → tappendB_out_gaa(node(T171, T172, T175), T176, node(T171, T172, X339))
U4_gaa(T159, T156, T157, T160, X319, tappendB_out_gaa(T159, T160, X319)) → tappendB_out_gaa(node(T159, T156, T157), T160, node(X319, T156, T157))
U11_gaaa(T100, X251, T101, X252, tappendB_out_gaa(T100, T101, X252)) → tappendE_out_gaaa(T100, X251, T101, node(X252, X251, T100))
tappendE_in_gaaa(T189, X363, T190, node(T189, X363, X364)) → U12_gaaa(T189, X363, T190, X364, tappendB_in_gaa(T189, T190, X364))
U12_gaaa(T189, X363, T190, X364, tappendB_out_gaa(T189, T190, X364)) → tappendE_out_gaaa(T189, X363, T190, node(T189, X363, X364))
U8_gaaaa(T61, X168, T62, X167, T63, tappendE_out_gaaa(T61, X168, T62, X167)) → pD_out_gaaaa(T61, X168, T62, X167, T63)
pD_in_gaaaa(T61, T64, T62, T65, T66) → U9_gaaaa(T61, T64, T62, T65, T66, tappendE_in_gaaa(T61, T64, T62, T65))
U9_gaaaa(T61, T64, T62, T65, T66, tappendE_out_gaaa(T61, T64, T62, T65)) → U10_gaaaa(T61, T64, T62, T65, T66, tlastC_in_ag(T66, T65))
tlastC_in_ag(T199, node(nil, T199, nil)) → tlastC_out_ag(T199, node(nil, T199, nil))
tlastC_in_ag(T220, node(T221, T218, T219)) → U6_ag(T220, T221, T218, T219, tlastC_in_ag(T220, T221))
tlastC_in_ag(T236, node(T233, T234, T237)) → U7_ag(T236, T233, T234, T237, tlastC_in_ag(T236, T237))
U7_ag(T236, T233, T234, T237, tlastC_out_ag(T236, T237)) → tlastC_out_ag(T236, node(T233, T234, T237))
U6_ag(T220, T221, T218, T219, tlastC_out_ag(T220, T221)) → tlastC_out_ag(T220, node(T221, T218, T219))
U10_gaaaa(T61, T64, T62, T65, T66, tlastC_out_ag(T66, T65)) → pD_out_gaaaa(T61, T64, T62, T65, T66)
U15_gaa(T19, T62, T63, pD_out_gaaaa(T61, X168, T62, X167, T63)) → goalF_out_gaa(s(T19), T62, T63)
goalF_in_gaa(s(T244), T13, T14) → U16_gaa(T244, T13, T14, s2tA_in_ga(T244, X434))
U16_gaa(T244, T13, T14, s2tA_out_ga(T244, X434)) → goalF_out_gaa(s(T244), T13, T14)
goalF_in_gaa(s(T244), T264, T265) → U17_gaa(T244, T264, T265, s2tA_in_ga(T244, T263))
U17_gaa(T244, T264, T265, s2tA_out_ga(T244, T263)) → U18_gaa(T244, T264, T265, tappendB_in_gaa(node(nil, X465, T263), T264, X464))
U18_gaa(T244, T264, T265, tappendB_out_gaa(node(nil, X465, T263), T264, X464)) → goalF_out_gaa(s(T244), T264, T265)
goalF_in_gaa(s(T244), T264, T268) → U19_gaa(T244, T264, T268, s2tA_in_ga(T244, T263))
U19_gaa(T244, T264, T268, s2tA_out_ga(T244, T263)) → U20_gaa(T244, T264, T268, tappendB_in_gaa(node(nil, T266, T263), T264, T267))
U20_gaa(T244, T264, T268, tappendB_out_gaa(node(nil, T266, T263), T264, T267)) → U21_gaa(T244, T264, T268, tlastC_in_ag(T268, T267))
U21_gaa(T244, T264, T268, tlastC_out_ag(T268, T267)) → goalF_out_gaa(s(T244), T264, T268)
goalF_in_gaa(s(T275), T13, T14) → U22_gaa(T275, T13, T14, s2tA_in_ga(T275, X495))
U22_gaa(T275, T13, T14, s2tA_out_ga(T275, X495)) → goalF_out_gaa(s(T275), T13, T14)
goalF_in_gaa(s(T275), T295, T296) → U23_gaa(T275, T295, T296, s2tA_in_ga(T275, T294))
U23_gaa(T275, T295, T296, s2tA_out_ga(T275, T294)) → U24_gaa(T275, T295, T296, tappendB_in_gaa(node(T294, X527, nil), T295, X526))
U24_gaa(T275, T295, T296, tappendB_out_gaa(node(T294, X527, nil), T295, X526)) → goalF_out_gaa(s(T275), T295, T296)
goalF_in_gaa(s(T275), T295, T299) → U25_gaa(T275, T295, T299, s2tA_in_ga(T275, T294))
U25_gaa(T275, T295, T299, s2tA_out_ga(T275, T294)) → U26_gaa(T275, T295, T299, tappendB_in_gaa(node(T294, T297, nil), T295, T298))
U26_gaa(T275, T295, T299, tappendB_out_gaa(node(T294, T297, nil), T295, T298)) → U27_gaa(T275, T295, T299, tlastC_in_ag(T299, T298))
U27_gaa(T275, T295, T299, tlastC_out_ag(T299, T298)) → goalF_out_gaa(s(T275), T295, T299)
goalF_in_gaa(s(T306), T317, T318) → U28_gaa(T306, T317, T318, pD_in_gaaaa(nil, X569, T317, X568, T318))
U28_gaa(T306, T317, T318, pD_out_gaaaa(nil, X569, T317, X568, T318)) → goalF_out_gaa(s(T306), T317, T318)
goalF_in_gaa(0, T331, T332) → U29_gaa(T331, T332, tappendB_in_gaa(nil, T331, X588))
U29_gaa(T331, T332, tappendB_out_gaa(nil, T331, X588)) → goalF_out_gaa(0, T331, T332)
goalF_in_gaa(0, T331, T336) → U30_gaa(T331, T336, tappendB_in_gaa(nil, T331, T335))
U30_gaa(T331, T336, tappendB_out_gaa(nil, T331, T335)) → U31_gaa(T331, T336, tlastC_in_ag(T336, T335))
U31_gaa(T331, T336, tlastC_out_ag(T336, T335)) → goalF_out_gaa(0, T331, T336)
S2TA_IN_GA(s(T33), node(nil, X96, X97)) → S2TA_IN_GA(T33, X97)
S2TA_IN_GA(s(T27), node(X66, X67, X66)) → S2TA_IN_GA(T27, X66)
S2TA_IN_GA(s(T39), node(X126, X127, nil)) → S2TA_IN_GA(T39, X126)
S2TA_IN_GA(s(T33)) → S2TA_IN_GA(T33)
From the DPs we obtained the following set of size-change graphs: