0 Prolog
↳1 PrologToDTProblemTransformerProof (⇐)
↳2 TRIPLES
↳3 TriplesToPiDPProof (⇐)
↳4 PiDP
↳5 DependencyGraphProof (⇔)
↳6 AND
↳7 PiDP
↳8 UsableRulesProof (⇔)
↳9 PiDP
↳10 PiDPToQDPProof (⇔)
↳11 QDP
↳12 QDPSizeChangeProof (⇔)
↳13 YES
↳14 PiDP
↳15 UsableRulesProof (⇔)
↳16 PiDP
↳17 PiDPToQDPProof (⇔)
↳18 QDP
↳19 QDPSizeChangeProof (⇔)
↳20 YES
↳21 PiDP
↳22 PiDPToQDPProof (⇐)
↳23 QDP
↳24 QDPSizeChangeProof (⇔)
↳25 YES
INSERT1_IN_GAG(s(T25), tree(s(T25), T20, void), tree(s(T25), void, void)) → U7_GAG(T25, T20, p15_in_ga(T25, T20))
INSERT1_IN_GAG(s(T25), tree(s(T25), T20, void), tree(s(T25), void, void)) → P15_IN_GA(T25, T20)
P15_IN_GA(T25, T20) → U2_GA(T25, T20, less17_in_g(T25))
P15_IN_GA(T25, T20) → LESS17_IN_G(T25)
LESS17_IN_G(s(T30)) → U1_G(T30, less17_in_g(T30))
LESS17_IN_G(s(T30)) → LESS17_IN_G(T30)
P15_IN_GA(T25, T20) → U3_GA(T25, T20, lessc17_in_g(T25))
U3_GA(T25, T20, lessc17_out_g(T25)) → U4_GA(T25, T20, insert1_in_gag(s(T25), T20, void))
U3_GA(T25, T20, lessc17_out_g(T25)) → INSERT1_IN_GAG(s(T25), T20, void)
INSERT1_IN_GAG(T56, tree(T56, void, T60), tree(T56, void, void)) → U8_GAG(T56, T60, less17_in_g(T56))
INSERT1_IN_GAG(T56, tree(T56, void, T60), tree(T56, void, void)) → LESS17_IN_G(T56)
INSERT1_IN_GAG(T56, tree(T56, void, T60), tree(T56, void, void)) → U9_GAG(T56, T60, lessc17_in_g(T56))
U9_GAG(T56, T60, lessc17_out_g(T56)) → U10_GAG(T56, T60, insert1_in_gag(T56, T60, void))
U9_GAG(T56, T60, lessc17_out_g(T56)) → INSERT1_IN_GAG(T56, T60, void)
INSERT1_IN_GAG(T83, tree(T83, void, T87), tree(T83, void, void)) → U11_GAG(T83, T87, p28_in_ga(T83, T87))
INSERT1_IN_GAG(T83, tree(T83, void, T87), tree(T83, void, void)) → P28_IN_GA(T83, T87)
P28_IN_GA(s(T90), T87) → U5_GA(T90, T87, p15_in_ga(T90, T87))
P28_IN_GA(s(T90), T87) → P15_IN_GA(T90, T87)
INSERT1_IN_GAG(s(T105), tree(s(T105), T100, void), tree(s(T105), void, void)) → U12_GAG(T105, T100, p15_in_ga(T105, T100))
INSERT1_IN_GAG(T115, tree(T115, void, T119), tree(T115, void, void)) → U13_GAG(T115, T119, p28_in_ga(T115, T119))
INSERT1_IN_GAG(s(T132), tree(s(T132), void, T129), tree(s(T132), void, void)) → U14_GAG(T132, T129, p15_in_ga(T132, T129))
INSERT1_IN_GAG(s(T132), tree(s(T132), void, T129), tree(s(T132), void, void)) → P15_IN_GA(T132, T129)
INSERT1_IN_GAG(s(T155), tree(s(T155), T150, T148), tree(s(T155), T149, T148)) → U15_GAG(T155, T150, T148, T149, less17_in_g(T155))
INSERT1_IN_GAG(s(T155), tree(s(T155), T150, T148), tree(s(T155), T149, T148)) → LESS17_IN_G(T155)
INSERT1_IN_GAG(s(T155), tree(s(T155), T150, T148), tree(s(T155), T149, T148)) → U16_GAG(T155, T150, T148, T149, lessc17_in_g(T155))
U16_GAG(T155, T150, T148, T149, lessc17_out_g(T155)) → U17_GAG(T155, T150, T148, T149, insert1_in_gag(s(T155), T150, T149))
U16_GAG(T155, T150, T148, T149, lessc17_out_g(T155)) → INSERT1_IN_GAG(s(T155), T150, T149)
INSERT1_IN_GAG(T170, tree(T170, T172, T175), tree(T170, T172, T174)) → U18_GAG(T170, T172, T175, T174, less17_in_g(T170))
INSERT1_IN_GAG(T170, tree(T170, T172, T175), tree(T170, T172, T174)) → LESS17_IN_G(T170)
INSERT1_IN_GAG(T170, tree(T170, T172, T175), tree(T170, T172, T174)) → U19_GAG(T170, T172, T175, T174, lessc17_in_g(T170))
U19_GAG(T170, T172, T175, T174, lessc17_out_g(T170)) → U20_GAG(T170, T172, T175, T174, insert1_in_gag(T170, T175, T174))
U19_GAG(T170, T172, T175, T174, lessc17_out_g(T170)) → INSERT1_IN_GAG(T170, T175, T174)
INSERT1_IN_GAG(s(T193), tree(s(T193), T187, T190), tree(s(T193), T187, T189)) → U21_GAG(T193, T187, T190, T189, less17_in_g(T193))
INSERT1_IN_GAG(s(T193), tree(s(T193), T187, T190), tree(s(T193), T187, T189)) → LESS17_IN_G(T193)
INSERT1_IN_GAG(s(T193), tree(s(T193), T187, T190), tree(s(T193), T187, T189)) → U22_GAG(T193, T187, T190, T189, lessc17_in_g(T193))
U22_GAG(T193, T187, T190, T189, lessc17_out_g(T193)) → U23_GAG(T193, T187, T190, T189, insert1_in_gag(s(T193), T190, T189))
U22_GAG(T193, T187, T190, T189, lessc17_out_g(T193)) → INSERT1_IN_GAG(s(T193), T190, T189)
INSERT1_IN_GAG(0, tree(s(T213), T208, T206), tree(s(T213), T207, T206)) → U24_GAG(T213, T208, T206, T207, insert1_in_gag(0, T208, T207))
INSERT1_IN_GAG(0, tree(s(T213), T208, T206), tree(s(T213), T207, T206)) → INSERT1_IN_GAG(0, T208, T207)
INSERT1_IN_GAG(s(s(s(s(s(s(s(s(T315)))))))), tree(s(s(s(s(s(s(s(s(T316)))))))), T208, T206), tree(s(s(s(s(s(s(s(s(T316)))))))), T207, T206)) → U25_GAG(T315, T316, T208, T206, T207, less146_in_gg(T315, T316))
INSERT1_IN_GAG(s(s(s(s(s(s(s(s(T315)))))))), tree(s(s(s(s(s(s(s(s(T316)))))))), T208, T206), tree(s(s(s(s(s(s(s(s(T316)))))))), T207, T206)) → LESS146_IN_GG(T315, T316)
LESS146_IN_GG(s(T332), s(T333)) → U6_GG(T332, T333, less146_in_gg(T332, T333))
LESS146_IN_GG(s(T332), s(T333)) → LESS146_IN_GG(T332, T333)
INSERT1_IN_GAG(s(T222), tree(s(T223), T208, T206), tree(s(T223), T207, T206)) → U26_GAG(T222, T223, T208, T206, T207, lessc88_in_gg(T222, T223))
U26_GAG(T222, T223, T208, T206, T207, lessc88_out_gg(T222, T223)) → U27_GAG(T222, T223, T208, T206, T207, insert1_in_gag(s(T222), T208, T207))
U26_GAG(T222, T223, T208, T206, T207, lessc88_out_gg(T222, T223)) → INSERT1_IN_GAG(s(T222), T208, T207)
INSERT1_IN_GAG(T348, tree(T349, T350, T353), tree(T349, T350, T352)) → U28_GAG(T348, T349, T350, T353, T352, less146_in_gg(T349, T348))
INSERT1_IN_GAG(T348, tree(T349, T350, T353), tree(T349, T350, T352)) → LESS146_IN_GG(T349, T348)
INSERT1_IN_GAG(T348, tree(T349, T350, T353), tree(T349, T350, T352)) → U29_GAG(T348, T349, T350, T353, T352, lessc146_in_gg(T349, T348))
U29_GAG(T348, T349, T350, T353, T352, lessc146_out_gg(T349, T348)) → U30_GAG(T348, T349, T350, T353, T352, insert1_in_gag(T348, T353, T352))
U29_GAG(T348, T349, T350, T353, T352, lessc146_out_gg(T349, T348)) → INSERT1_IN_GAG(T348, T353, T352)
INSERT1_IN_GAG(s(T375), tree(0, T367, T370), tree(0, T367, T369)) → U31_GAG(T375, T367, T370, T369, insert1_in_gag(s(T375), T370, T369))
INSERT1_IN_GAG(s(T375), tree(0, T367, T370), tree(0, T367, T369)) → INSERT1_IN_GAG(s(T375), T370, T369)
INSERT1_IN_GAG(s(T383), tree(s(T382), T367, T370), tree(s(T382), T367, T369)) → U32_GAG(T383, T382, T367, T370, T369, less146_in_gg(T382, T383))
INSERT1_IN_GAG(s(T383), tree(s(T382), T367, T370), tree(s(T382), T367, T369)) → LESS146_IN_GG(T382, T383)
INSERT1_IN_GAG(s(T383), tree(s(T382), T367, T370), tree(s(T382), T367, T369)) → U33_GAG(T383, T382, T367, T370, T369, lessc146_in_gg(T382, T383))
U33_GAG(T383, T382, T367, T370, T369, lessc146_out_gg(T382, T383)) → U34_GAG(T383, T382, T367, T370, T369, insert1_in_gag(s(T383), T370, T369))
U33_GAG(T383, T382, T367, T370, T369, lessc146_out_gg(T382, T383)) → INSERT1_IN_GAG(s(T383), T370, T369)
lessc17_in_g(s(T30)) → U57_g(T30, lessc17_in_g(T30))
U57_g(T30, lessc17_out_g(T30)) → lessc17_out_g(s(T30))
lessc88_in_gg(0, s(T232)) → lessc88_out_gg(0, s(T232))
lessc88_in_gg(s(0), s(s(T245))) → lessc88_out_gg(s(0), s(s(T245)))
lessc88_in_gg(s(s(0)), s(s(s(T258)))) → lessc88_out_gg(s(s(0)), s(s(s(T258))))
lessc88_in_gg(s(s(s(0))), s(s(s(s(T271))))) → lessc88_out_gg(s(s(s(0))), s(s(s(s(T271)))))
lessc88_in_gg(s(s(s(s(0)))), s(s(s(s(s(T284)))))) → lessc88_out_gg(s(s(s(s(0)))), s(s(s(s(s(T284))))))
lessc88_in_gg(s(s(s(s(s(0))))), s(s(s(s(s(s(T297))))))) → lessc88_out_gg(s(s(s(s(s(0))))), s(s(s(s(s(s(T297)))))))
lessc88_in_gg(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T310)))))))) → lessc88_out_gg(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T310))))))))
lessc88_in_gg(s(s(s(s(s(s(s(T315))))))), s(s(s(s(s(s(s(T316)))))))) → U62_gg(T315, T316, lessc146_in_gg(T315, T316))
lessc146_in_gg(0, s(T327)) → lessc146_out_gg(0, s(T327))
lessc146_in_gg(s(T332), s(T333)) → U61_gg(T332, T333, lessc146_in_gg(T332, T333))
U61_gg(T332, T333, lessc146_out_gg(T332, T333)) → lessc146_out_gg(s(T332), s(T333))
U62_gg(T315, T316, lessc146_out_gg(T315, T316)) → lessc88_out_gg(s(s(s(s(s(s(s(T315))))))), s(s(s(s(s(s(s(T316))))))))
Infinitary Constructor Rewriting Termination of PiDP implies Termination of TRIPLES
INSERT1_IN_GAG(s(T25), tree(s(T25), T20, void), tree(s(T25), void, void)) → U7_GAG(T25, T20, p15_in_ga(T25, T20))
INSERT1_IN_GAG(s(T25), tree(s(T25), T20, void), tree(s(T25), void, void)) → P15_IN_GA(T25, T20)
P15_IN_GA(T25, T20) → U2_GA(T25, T20, less17_in_g(T25))
P15_IN_GA(T25, T20) → LESS17_IN_G(T25)
LESS17_IN_G(s(T30)) → U1_G(T30, less17_in_g(T30))
LESS17_IN_G(s(T30)) → LESS17_IN_G(T30)
P15_IN_GA(T25, T20) → U3_GA(T25, T20, lessc17_in_g(T25))
U3_GA(T25, T20, lessc17_out_g(T25)) → U4_GA(T25, T20, insert1_in_gag(s(T25), T20, void))
U3_GA(T25, T20, lessc17_out_g(T25)) → INSERT1_IN_GAG(s(T25), T20, void)
INSERT1_IN_GAG(T56, tree(T56, void, T60), tree(T56, void, void)) → U8_GAG(T56, T60, less17_in_g(T56))
INSERT1_IN_GAG(T56, tree(T56, void, T60), tree(T56, void, void)) → LESS17_IN_G(T56)
INSERT1_IN_GAG(T56, tree(T56, void, T60), tree(T56, void, void)) → U9_GAG(T56, T60, lessc17_in_g(T56))
U9_GAG(T56, T60, lessc17_out_g(T56)) → U10_GAG(T56, T60, insert1_in_gag(T56, T60, void))
U9_GAG(T56, T60, lessc17_out_g(T56)) → INSERT1_IN_GAG(T56, T60, void)
INSERT1_IN_GAG(T83, tree(T83, void, T87), tree(T83, void, void)) → U11_GAG(T83, T87, p28_in_ga(T83, T87))
INSERT1_IN_GAG(T83, tree(T83, void, T87), tree(T83, void, void)) → P28_IN_GA(T83, T87)
P28_IN_GA(s(T90), T87) → U5_GA(T90, T87, p15_in_ga(T90, T87))
P28_IN_GA(s(T90), T87) → P15_IN_GA(T90, T87)
INSERT1_IN_GAG(s(T105), tree(s(T105), T100, void), tree(s(T105), void, void)) → U12_GAG(T105, T100, p15_in_ga(T105, T100))
INSERT1_IN_GAG(T115, tree(T115, void, T119), tree(T115, void, void)) → U13_GAG(T115, T119, p28_in_ga(T115, T119))
INSERT1_IN_GAG(s(T132), tree(s(T132), void, T129), tree(s(T132), void, void)) → U14_GAG(T132, T129, p15_in_ga(T132, T129))
INSERT1_IN_GAG(s(T132), tree(s(T132), void, T129), tree(s(T132), void, void)) → P15_IN_GA(T132, T129)
INSERT1_IN_GAG(s(T155), tree(s(T155), T150, T148), tree(s(T155), T149, T148)) → U15_GAG(T155, T150, T148, T149, less17_in_g(T155))
INSERT1_IN_GAG(s(T155), tree(s(T155), T150, T148), tree(s(T155), T149, T148)) → LESS17_IN_G(T155)
INSERT1_IN_GAG(s(T155), tree(s(T155), T150, T148), tree(s(T155), T149, T148)) → U16_GAG(T155, T150, T148, T149, lessc17_in_g(T155))
U16_GAG(T155, T150, T148, T149, lessc17_out_g(T155)) → U17_GAG(T155, T150, T148, T149, insert1_in_gag(s(T155), T150, T149))
U16_GAG(T155, T150, T148, T149, lessc17_out_g(T155)) → INSERT1_IN_GAG(s(T155), T150, T149)
INSERT1_IN_GAG(T170, tree(T170, T172, T175), tree(T170, T172, T174)) → U18_GAG(T170, T172, T175, T174, less17_in_g(T170))
INSERT1_IN_GAG(T170, tree(T170, T172, T175), tree(T170, T172, T174)) → LESS17_IN_G(T170)
INSERT1_IN_GAG(T170, tree(T170, T172, T175), tree(T170, T172, T174)) → U19_GAG(T170, T172, T175, T174, lessc17_in_g(T170))
U19_GAG(T170, T172, T175, T174, lessc17_out_g(T170)) → U20_GAG(T170, T172, T175, T174, insert1_in_gag(T170, T175, T174))
U19_GAG(T170, T172, T175, T174, lessc17_out_g(T170)) → INSERT1_IN_GAG(T170, T175, T174)
INSERT1_IN_GAG(s(T193), tree(s(T193), T187, T190), tree(s(T193), T187, T189)) → U21_GAG(T193, T187, T190, T189, less17_in_g(T193))
INSERT1_IN_GAG(s(T193), tree(s(T193), T187, T190), tree(s(T193), T187, T189)) → LESS17_IN_G(T193)
INSERT1_IN_GAG(s(T193), tree(s(T193), T187, T190), tree(s(T193), T187, T189)) → U22_GAG(T193, T187, T190, T189, lessc17_in_g(T193))
U22_GAG(T193, T187, T190, T189, lessc17_out_g(T193)) → U23_GAG(T193, T187, T190, T189, insert1_in_gag(s(T193), T190, T189))
U22_GAG(T193, T187, T190, T189, lessc17_out_g(T193)) → INSERT1_IN_GAG(s(T193), T190, T189)
INSERT1_IN_GAG(0, tree(s(T213), T208, T206), tree(s(T213), T207, T206)) → U24_GAG(T213, T208, T206, T207, insert1_in_gag(0, T208, T207))
INSERT1_IN_GAG(0, tree(s(T213), T208, T206), tree(s(T213), T207, T206)) → INSERT1_IN_GAG(0, T208, T207)
INSERT1_IN_GAG(s(s(s(s(s(s(s(s(T315)))))))), tree(s(s(s(s(s(s(s(s(T316)))))))), T208, T206), tree(s(s(s(s(s(s(s(s(T316)))))))), T207, T206)) → U25_GAG(T315, T316, T208, T206, T207, less146_in_gg(T315, T316))
INSERT1_IN_GAG(s(s(s(s(s(s(s(s(T315)))))))), tree(s(s(s(s(s(s(s(s(T316)))))))), T208, T206), tree(s(s(s(s(s(s(s(s(T316)))))))), T207, T206)) → LESS146_IN_GG(T315, T316)
LESS146_IN_GG(s(T332), s(T333)) → U6_GG(T332, T333, less146_in_gg(T332, T333))
LESS146_IN_GG(s(T332), s(T333)) → LESS146_IN_GG(T332, T333)
INSERT1_IN_GAG(s(T222), tree(s(T223), T208, T206), tree(s(T223), T207, T206)) → U26_GAG(T222, T223, T208, T206, T207, lessc88_in_gg(T222, T223))
U26_GAG(T222, T223, T208, T206, T207, lessc88_out_gg(T222, T223)) → U27_GAG(T222, T223, T208, T206, T207, insert1_in_gag(s(T222), T208, T207))
U26_GAG(T222, T223, T208, T206, T207, lessc88_out_gg(T222, T223)) → INSERT1_IN_GAG(s(T222), T208, T207)
INSERT1_IN_GAG(T348, tree(T349, T350, T353), tree(T349, T350, T352)) → U28_GAG(T348, T349, T350, T353, T352, less146_in_gg(T349, T348))
INSERT1_IN_GAG(T348, tree(T349, T350, T353), tree(T349, T350, T352)) → LESS146_IN_GG(T349, T348)
INSERT1_IN_GAG(T348, tree(T349, T350, T353), tree(T349, T350, T352)) → U29_GAG(T348, T349, T350, T353, T352, lessc146_in_gg(T349, T348))
U29_GAG(T348, T349, T350, T353, T352, lessc146_out_gg(T349, T348)) → U30_GAG(T348, T349, T350, T353, T352, insert1_in_gag(T348, T353, T352))
U29_GAG(T348, T349, T350, T353, T352, lessc146_out_gg(T349, T348)) → INSERT1_IN_GAG(T348, T353, T352)
INSERT1_IN_GAG(s(T375), tree(0, T367, T370), tree(0, T367, T369)) → U31_GAG(T375, T367, T370, T369, insert1_in_gag(s(T375), T370, T369))
INSERT1_IN_GAG(s(T375), tree(0, T367, T370), tree(0, T367, T369)) → INSERT1_IN_GAG(s(T375), T370, T369)
INSERT1_IN_GAG(s(T383), tree(s(T382), T367, T370), tree(s(T382), T367, T369)) → U32_GAG(T383, T382, T367, T370, T369, less146_in_gg(T382, T383))
INSERT1_IN_GAG(s(T383), tree(s(T382), T367, T370), tree(s(T382), T367, T369)) → LESS146_IN_GG(T382, T383)
INSERT1_IN_GAG(s(T383), tree(s(T382), T367, T370), tree(s(T382), T367, T369)) → U33_GAG(T383, T382, T367, T370, T369, lessc146_in_gg(T382, T383))
U33_GAG(T383, T382, T367, T370, T369, lessc146_out_gg(T382, T383)) → U34_GAG(T383, T382, T367, T370, T369, insert1_in_gag(s(T383), T370, T369))
U33_GAG(T383, T382, T367, T370, T369, lessc146_out_gg(T382, T383)) → INSERT1_IN_GAG(s(T383), T370, T369)
lessc17_in_g(s(T30)) → U57_g(T30, lessc17_in_g(T30))
U57_g(T30, lessc17_out_g(T30)) → lessc17_out_g(s(T30))
lessc88_in_gg(0, s(T232)) → lessc88_out_gg(0, s(T232))
lessc88_in_gg(s(0), s(s(T245))) → lessc88_out_gg(s(0), s(s(T245)))
lessc88_in_gg(s(s(0)), s(s(s(T258)))) → lessc88_out_gg(s(s(0)), s(s(s(T258))))
lessc88_in_gg(s(s(s(0))), s(s(s(s(T271))))) → lessc88_out_gg(s(s(s(0))), s(s(s(s(T271)))))
lessc88_in_gg(s(s(s(s(0)))), s(s(s(s(s(T284)))))) → lessc88_out_gg(s(s(s(s(0)))), s(s(s(s(s(T284))))))
lessc88_in_gg(s(s(s(s(s(0))))), s(s(s(s(s(s(T297))))))) → lessc88_out_gg(s(s(s(s(s(0))))), s(s(s(s(s(s(T297)))))))
lessc88_in_gg(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T310)))))))) → lessc88_out_gg(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T310))))))))
lessc88_in_gg(s(s(s(s(s(s(s(T315))))))), s(s(s(s(s(s(s(T316)))))))) → U62_gg(T315, T316, lessc146_in_gg(T315, T316))
lessc146_in_gg(0, s(T327)) → lessc146_out_gg(0, s(T327))
lessc146_in_gg(s(T332), s(T333)) → U61_gg(T332, T333, lessc146_in_gg(T332, T333))
U61_gg(T332, T333, lessc146_out_gg(T332, T333)) → lessc146_out_gg(s(T332), s(T333))
U62_gg(T315, T316, lessc146_out_gg(T315, T316)) → lessc88_out_gg(s(s(s(s(s(s(s(T315))))))), s(s(s(s(s(s(s(T316))))))))
LESS146_IN_GG(s(T332), s(T333)) → LESS146_IN_GG(T332, T333)
lessc17_in_g(s(T30)) → U57_g(T30, lessc17_in_g(T30))
U57_g(T30, lessc17_out_g(T30)) → lessc17_out_g(s(T30))
lessc88_in_gg(0, s(T232)) → lessc88_out_gg(0, s(T232))
lessc88_in_gg(s(0), s(s(T245))) → lessc88_out_gg(s(0), s(s(T245)))
lessc88_in_gg(s(s(0)), s(s(s(T258)))) → lessc88_out_gg(s(s(0)), s(s(s(T258))))
lessc88_in_gg(s(s(s(0))), s(s(s(s(T271))))) → lessc88_out_gg(s(s(s(0))), s(s(s(s(T271)))))
lessc88_in_gg(s(s(s(s(0)))), s(s(s(s(s(T284)))))) → lessc88_out_gg(s(s(s(s(0)))), s(s(s(s(s(T284))))))
lessc88_in_gg(s(s(s(s(s(0))))), s(s(s(s(s(s(T297))))))) → lessc88_out_gg(s(s(s(s(s(0))))), s(s(s(s(s(s(T297)))))))
lessc88_in_gg(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T310)))))))) → lessc88_out_gg(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T310))))))))
lessc88_in_gg(s(s(s(s(s(s(s(T315))))))), s(s(s(s(s(s(s(T316)))))))) → U62_gg(T315, T316, lessc146_in_gg(T315, T316))
lessc146_in_gg(0, s(T327)) → lessc146_out_gg(0, s(T327))
lessc146_in_gg(s(T332), s(T333)) → U61_gg(T332, T333, lessc146_in_gg(T332, T333))
U61_gg(T332, T333, lessc146_out_gg(T332, T333)) → lessc146_out_gg(s(T332), s(T333))
U62_gg(T315, T316, lessc146_out_gg(T315, T316)) → lessc88_out_gg(s(s(s(s(s(s(s(T315))))))), s(s(s(s(s(s(s(T316))))))))
LESS146_IN_GG(s(T332), s(T333)) → LESS146_IN_GG(T332, T333)
LESS146_IN_GG(s(T332), s(T333)) → LESS146_IN_GG(T332, T333)
From the DPs we obtained the following set of size-change graphs:
LESS17_IN_G(s(T30)) → LESS17_IN_G(T30)
lessc17_in_g(s(T30)) → U57_g(T30, lessc17_in_g(T30))
U57_g(T30, lessc17_out_g(T30)) → lessc17_out_g(s(T30))
lessc88_in_gg(0, s(T232)) → lessc88_out_gg(0, s(T232))
lessc88_in_gg(s(0), s(s(T245))) → lessc88_out_gg(s(0), s(s(T245)))
lessc88_in_gg(s(s(0)), s(s(s(T258)))) → lessc88_out_gg(s(s(0)), s(s(s(T258))))
lessc88_in_gg(s(s(s(0))), s(s(s(s(T271))))) → lessc88_out_gg(s(s(s(0))), s(s(s(s(T271)))))
lessc88_in_gg(s(s(s(s(0)))), s(s(s(s(s(T284)))))) → lessc88_out_gg(s(s(s(s(0)))), s(s(s(s(s(T284))))))
lessc88_in_gg(s(s(s(s(s(0))))), s(s(s(s(s(s(T297))))))) → lessc88_out_gg(s(s(s(s(s(0))))), s(s(s(s(s(s(T297)))))))
lessc88_in_gg(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T310)))))))) → lessc88_out_gg(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T310))))))))
lessc88_in_gg(s(s(s(s(s(s(s(T315))))))), s(s(s(s(s(s(s(T316)))))))) → U62_gg(T315, T316, lessc146_in_gg(T315, T316))
lessc146_in_gg(0, s(T327)) → lessc146_out_gg(0, s(T327))
lessc146_in_gg(s(T332), s(T333)) → U61_gg(T332, T333, lessc146_in_gg(T332, T333))
U61_gg(T332, T333, lessc146_out_gg(T332, T333)) → lessc146_out_gg(s(T332), s(T333))
U62_gg(T315, T316, lessc146_out_gg(T315, T316)) → lessc88_out_gg(s(s(s(s(s(s(s(T315))))))), s(s(s(s(s(s(s(T316))))))))
LESS17_IN_G(s(T30)) → LESS17_IN_G(T30)
LESS17_IN_G(s(T30)) → LESS17_IN_G(T30)
From the DPs we obtained the following set of size-change graphs:
INSERT1_IN_GAG(s(T155), tree(s(T155), T150, T148), tree(s(T155), T149, T148)) → U16_GAG(T155, T150, T148, T149, lessc17_in_g(T155))
U16_GAG(T155, T150, T148, T149, lessc17_out_g(T155)) → INSERT1_IN_GAG(s(T155), T150, T149)
INSERT1_IN_GAG(T170, tree(T170, T172, T175), tree(T170, T172, T174)) → U19_GAG(T170, T172, T175, T174, lessc17_in_g(T170))
U19_GAG(T170, T172, T175, T174, lessc17_out_g(T170)) → INSERT1_IN_GAG(T170, T175, T174)
INSERT1_IN_GAG(s(T193), tree(s(T193), T187, T190), tree(s(T193), T187, T189)) → U22_GAG(T193, T187, T190, T189, lessc17_in_g(T193))
U22_GAG(T193, T187, T190, T189, lessc17_out_g(T193)) → INSERT1_IN_GAG(s(T193), T190, T189)
INSERT1_IN_GAG(s(T222), tree(s(T223), T208, T206), tree(s(T223), T207, T206)) → U26_GAG(T222, T223, T208, T206, T207, lessc88_in_gg(T222, T223))
U26_GAG(T222, T223, T208, T206, T207, lessc88_out_gg(T222, T223)) → INSERT1_IN_GAG(s(T222), T208, T207)
INSERT1_IN_GAG(T348, tree(T349, T350, T353), tree(T349, T350, T352)) → U29_GAG(T348, T349, T350, T353, T352, lessc146_in_gg(T349, T348))
U29_GAG(T348, T349, T350, T353, T352, lessc146_out_gg(T349, T348)) → INSERT1_IN_GAG(T348, T353, T352)
INSERT1_IN_GAG(0, tree(s(T213), T208, T206), tree(s(T213), T207, T206)) → INSERT1_IN_GAG(0, T208, T207)
INSERT1_IN_GAG(s(T375), tree(0, T367, T370), tree(0, T367, T369)) → INSERT1_IN_GAG(s(T375), T370, T369)
INSERT1_IN_GAG(s(T383), tree(s(T382), T367, T370), tree(s(T382), T367, T369)) → U33_GAG(T383, T382, T367, T370, T369, lessc146_in_gg(T382, T383))
U33_GAG(T383, T382, T367, T370, T369, lessc146_out_gg(T382, T383)) → INSERT1_IN_GAG(s(T383), T370, T369)
lessc17_in_g(s(T30)) → U57_g(T30, lessc17_in_g(T30))
U57_g(T30, lessc17_out_g(T30)) → lessc17_out_g(s(T30))
lessc88_in_gg(0, s(T232)) → lessc88_out_gg(0, s(T232))
lessc88_in_gg(s(0), s(s(T245))) → lessc88_out_gg(s(0), s(s(T245)))
lessc88_in_gg(s(s(0)), s(s(s(T258)))) → lessc88_out_gg(s(s(0)), s(s(s(T258))))
lessc88_in_gg(s(s(s(0))), s(s(s(s(T271))))) → lessc88_out_gg(s(s(s(0))), s(s(s(s(T271)))))
lessc88_in_gg(s(s(s(s(0)))), s(s(s(s(s(T284)))))) → lessc88_out_gg(s(s(s(s(0)))), s(s(s(s(s(T284))))))
lessc88_in_gg(s(s(s(s(s(0))))), s(s(s(s(s(s(T297))))))) → lessc88_out_gg(s(s(s(s(s(0))))), s(s(s(s(s(s(T297)))))))
lessc88_in_gg(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T310)))))))) → lessc88_out_gg(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T310))))))))
lessc88_in_gg(s(s(s(s(s(s(s(T315))))))), s(s(s(s(s(s(s(T316)))))))) → U62_gg(T315, T316, lessc146_in_gg(T315, T316))
lessc146_in_gg(0, s(T327)) → lessc146_out_gg(0, s(T327))
lessc146_in_gg(s(T332), s(T333)) → U61_gg(T332, T333, lessc146_in_gg(T332, T333))
U61_gg(T332, T333, lessc146_out_gg(T332, T333)) → lessc146_out_gg(s(T332), s(T333))
U62_gg(T315, T316, lessc146_out_gg(T315, T316)) → lessc88_out_gg(s(s(s(s(s(s(s(T315))))))), s(s(s(s(s(s(s(T316))))))))
INSERT1_IN_GAG(s(T155), tree(s(T155), T149, T148)) → U16_GAG(T155, T148, T149, lessc17_in_g(T155))
U16_GAG(T155, T148, T149, lessc17_out_g(T155)) → INSERT1_IN_GAG(s(T155), T149)
INSERT1_IN_GAG(T170, tree(T170, T172, T174)) → U19_GAG(T170, T172, T174, lessc17_in_g(T170))
U19_GAG(T170, T172, T174, lessc17_out_g(T170)) → INSERT1_IN_GAG(T170, T174)
INSERT1_IN_GAG(s(T193), tree(s(T193), T187, T189)) → U22_GAG(T193, T187, T189, lessc17_in_g(T193))
U22_GAG(T193, T187, T189, lessc17_out_g(T193)) → INSERT1_IN_GAG(s(T193), T189)
INSERT1_IN_GAG(s(T222), tree(s(T223), T207, T206)) → U26_GAG(T222, T223, T206, T207, lessc88_in_gg(T222, T223))
U26_GAG(T222, T223, T206, T207, lessc88_out_gg(T222, T223)) → INSERT1_IN_GAG(s(T222), T207)
INSERT1_IN_GAG(T348, tree(T349, T350, T352)) → U29_GAG(T348, T349, T350, T352, lessc146_in_gg(T349, T348))
U29_GAG(T348, T349, T350, T352, lessc146_out_gg(T349, T348)) → INSERT1_IN_GAG(T348, T352)
INSERT1_IN_GAG(0, tree(s(T213), T207, T206)) → INSERT1_IN_GAG(0, T207)
INSERT1_IN_GAG(s(T375), tree(0, T367, T369)) → INSERT1_IN_GAG(s(T375), T369)
INSERT1_IN_GAG(s(T383), tree(s(T382), T367, T369)) → U33_GAG(T383, T382, T367, T369, lessc146_in_gg(T382, T383))
U33_GAG(T383, T382, T367, T369, lessc146_out_gg(T382, T383)) → INSERT1_IN_GAG(s(T383), T369)
lessc17_in_g(s(T30)) → U57_g(T30, lessc17_in_g(T30))
U57_g(T30, lessc17_out_g(T30)) → lessc17_out_g(s(T30))
lessc88_in_gg(0, s(T232)) → lessc88_out_gg(0, s(T232))
lessc88_in_gg(s(0), s(s(T245))) → lessc88_out_gg(s(0), s(s(T245)))
lessc88_in_gg(s(s(0)), s(s(s(T258)))) → lessc88_out_gg(s(s(0)), s(s(s(T258))))
lessc88_in_gg(s(s(s(0))), s(s(s(s(T271))))) → lessc88_out_gg(s(s(s(0))), s(s(s(s(T271)))))
lessc88_in_gg(s(s(s(s(0)))), s(s(s(s(s(T284)))))) → lessc88_out_gg(s(s(s(s(0)))), s(s(s(s(s(T284))))))
lessc88_in_gg(s(s(s(s(s(0))))), s(s(s(s(s(s(T297))))))) → lessc88_out_gg(s(s(s(s(s(0))))), s(s(s(s(s(s(T297)))))))
lessc88_in_gg(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T310)))))))) → lessc88_out_gg(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T310))))))))
lessc88_in_gg(s(s(s(s(s(s(s(T315))))))), s(s(s(s(s(s(s(T316)))))))) → U62_gg(T315, T316, lessc146_in_gg(T315, T316))
lessc146_in_gg(0, s(T327)) → lessc146_out_gg(0, s(T327))
lessc146_in_gg(s(T332), s(T333)) → U61_gg(T332, T333, lessc146_in_gg(T332, T333))
U61_gg(T332, T333, lessc146_out_gg(T332, T333)) → lessc146_out_gg(s(T332), s(T333))
U62_gg(T315, T316, lessc146_out_gg(T315, T316)) → lessc88_out_gg(s(s(s(s(s(s(s(T315))))))), s(s(s(s(s(s(s(T316))))))))
lessc17_in_g(x0)
U57_g(x0, x1)
lessc88_in_gg(x0, x1)
lessc146_in_gg(x0, x1)
U61_gg(x0, x1, x2)
U62_gg(x0, x1, x2)
From the DPs we obtained the following set of size-change graphs: