0 Prolog
↳1 PrologToPrologProblemTransformerProof (⇒, 181 ms)
↳2 Prolog
↳3 PrologToPiTRSProof (⇒, 132 ms)
↳4 PiTRS
↳5 DependencyPairsProof (⇔, 496 ms)
↳6 PiDP
↳7 DependencyGraphProof (⇔, 26 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
↳30 PiDP
↳31 UsableRulesProof (⇔, 0 ms)
↳32 PiDP
↳33 PiDPToQDPProof (⇔, 0 ms)
↳34 QDP
↳35 QDPSizeChangeProof (⇔, 0 ms)
↳36 YES
↳37 PiDP
↳38 UsableRulesProof (⇔, 2 ms)
↳39 PiDP
↳40 PiDPToQDPProof (⇒, 0 ms)
↳41 QDP
↳42 QDPSizeChangeProof (⇔, 16 ms)
↳43 YES
↳44 PiDP
↳45 UsableRulesProof (⇔, 0 ms)
↳46 PiDP
↳47 PiDPToQDPProof (⇒, 0 ms)
↳48 QDP
↳49 QDPSizeChangeProof (⇔, 0 ms)
↳50 YES
insertD_in_aga(T5, void, tree(T5, void, void)) → insertD_out_aga(T5, void, tree(T5, void, void))
insertD_in_aga(T12, tree(T12, T13, T14), tree(T12, T13, T14)) → insertD_out_aga(T12, tree(T12, T13, T14), tree(T12, T13, T14))
insertD_in_aga(0, tree(s(T31), T22, T23), tree(s(T31), T32, T23)) → U9_aga(T31, T22, T23, T32, insertD_in_gga(0, T22, T32))
insertD_in_gga(T5, void, tree(T5, void, void)) → insertD_out_gga(T5, void, tree(T5, void, void))
insertD_in_gga(T12, tree(T12, T13, T14), tree(T12, T13, T14)) → insertD_out_gga(T12, tree(T12, T13, T14), tree(T12, T13, T14))
insertD_in_gga(0, tree(s(T31), T22, T23), tree(s(T31), T32, T23)) → U9_gga(T31, T22, T23, T32, insertD_in_gga(0, T22, T32))
insertD_in_gga(s(T43), tree(s(T42), T22, T23), tree(s(T42), T44, T23)) → U10_gga(T43, T42, T22, T23, T44, pC_in_ggga(T43, T42, T22, T44))
pC_in_ggga(T43, T42, T22, T44) → U3_ggga(T43, T42, T22, T44, lessA_in_gg(T43, T42))
lessA_in_gg(0, s(T55)) → lessA_out_gg(0, s(T55))
lessA_in_gg(s(T62), s(T61)) → U1_gg(T62, T61, lessA_in_gg(T62, T61))
U1_gg(T62, T61, lessA_out_gg(T62, T61)) → lessA_out_gg(s(T62), s(T61))
U3_ggga(T43, T42, T22, T44, lessA_out_gg(T43, T42)) → pC_out_ggga(T43, T42, T22, T44)
pC_in_ggga(T47, T42, T22, T48) → U4_ggga(T47, T42, T22, T48, lessA_in_gg(T47, T42))
U4_ggga(T47, T42, T22, T48, lessA_out_gg(T47, T42)) → U5_ggga(T47, T42, T22, T48, insertD_in_gga(s(T47), T22, T48))
insertD_in_gga(T82, tree(T78, T79, T80), tree(T78, T79, T83)) → U11_gga(T82, T78, T79, T80, T83, pE_in_ggga(T78, T82, T80, T83))
pE_in_ggga(T78, T82, T80, T83) → U6_ggga(T78, T82, T80, T83, lessB_in_gg(T78, T82))
lessB_in_gg(0, s(T94)) → lessB_out_gg(0, s(T94))
lessB_in_gg(s(T99), s(T101)) → U2_gg(T99, T101, lessB_in_gg(T99, T101))
U2_gg(T99, T101, lessB_out_gg(T99, T101)) → lessB_out_gg(s(T99), s(T101))
U6_ggga(T78, T82, T80, T83, lessB_out_gg(T78, T82)) → pE_out_ggga(T78, T82, T80, T83)
pE_in_ggga(T78, T86, T80, T87) → U7_ggga(T78, T86, T80, T87, lessB_in_gg(T78, T86))
U7_ggga(T78, T86, T80, T87, lessB_out_gg(T78, T86)) → U8_ggga(T78, T86, T80, T87, insertD_in_gga(T86, T80, T87))
insertD_in_gga(s(T124), tree(0, T113, T114), tree(0, T113, T123)) → U12_gga(T124, T113, T114, T123, insertD_in_gga(s(T124), T114, T123))
insertD_in_gga(s(T133), tree(s(T131), T113, T114), tree(s(T131), T113, T134)) → U13_gga(T133, T131, T113, T114, T134, lessB_in_gg(T131, T133))
U13_gga(T133, T131, T113, T114, T134, lessB_out_gg(T131, T133)) → insertD_out_gga(s(T133), tree(s(T131), T113, T114), tree(s(T131), T113, T134))
insertD_in_gga(s(T137), tree(s(T131), T113, T114), tree(s(T131), T113, T138)) → U14_gga(T137, T131, T113, T114, T138, lessB_in_gg(T131, T137))
U14_gga(T137, T131, T113, T114, T138, lessB_out_gg(T131, T137)) → U15_gga(T137, T131, T113, T114, T138, insertD_in_gga(s(T137), T114, T138))
insertD_in_gga(0, tree(s(T161), T152, T153), tree(s(T161), T162, T153)) → U16_gga(T161, T152, T153, T162, insertD_in_gga(0, T152, T162))
insertD_in_gga(s(T173), tree(s(T172), T152, T153), tree(s(T172), T174, T153)) → U17_gga(T173, T172, T152, T153, T174, pC_in_ggga(T173, T172, T152, T174))
U17_gga(T173, T172, T152, T153, T174, pC_out_ggga(T173, T172, T152, T174)) → insertD_out_gga(s(T173), tree(s(T172), T152, T153), tree(s(T172), T174, T153))
insertD_in_gga(T192, tree(T188, T189, T190), tree(T188, T189, T193)) → U18_gga(T192, T188, T189, T190, T193, pE_in_ggga(T188, T192, T190, T193))
U18_gga(T192, T188, T189, T190, T193, pE_out_ggga(T188, T192, T190, T193)) → insertD_out_gga(T192, tree(T188, T189, T190), tree(T188, T189, T193))
insertD_in_gga(s(T214), tree(0, T203, T204), tree(0, T203, T213)) → U19_gga(T214, T203, T204, T213, insertD_in_gga(s(T214), T204, T213))
insertD_in_gga(s(T223), tree(s(T221), T203, T204), tree(s(T221), T203, T224)) → U20_gga(T223, T221, T203, T204, T224, lessB_in_gg(T221, T223))
U20_gga(T223, T221, T203, T204, T224, lessB_out_gg(T221, T223)) → insertD_out_gga(s(T223), tree(s(T221), T203, T204), tree(s(T221), T203, T224))
insertD_in_gga(s(T227), tree(s(T221), T203, T204), tree(s(T221), T203, T228)) → U21_gga(T227, T221, T203, T204, T228, lessB_in_gg(T221, T227))
U21_gga(T227, T221, T203, T204, T228, lessB_out_gg(T221, T227)) → U22_gga(T227, T221, T203, T204, T228, insertD_in_gga(s(T227), T204, T228))
U22_gga(T227, T221, T203, T204, T228, insertD_out_gga(s(T227), T204, T228)) → insertD_out_gga(s(T227), tree(s(T221), T203, T204), tree(s(T221), T203, T228))
U19_gga(T214, T203, T204, T213, insertD_out_gga(s(T214), T204, T213)) → insertD_out_gga(s(T214), tree(0, T203, T204), tree(0, T203, T213))
U16_gga(T161, T152, T153, T162, insertD_out_gga(0, T152, T162)) → insertD_out_gga(0, tree(s(T161), T152, T153), tree(s(T161), T162, T153))
U15_gga(T137, T131, T113, T114, T138, insertD_out_gga(s(T137), T114, T138)) → insertD_out_gga(s(T137), tree(s(T131), T113, T114), tree(s(T131), T113, T138))
U12_gga(T124, T113, T114, T123, insertD_out_gga(s(T124), T114, T123)) → insertD_out_gga(s(T124), tree(0, T113, T114), tree(0, T113, T123))
U8_ggga(T78, T86, T80, T87, insertD_out_gga(T86, T80, T87)) → pE_out_ggga(T78, T86, T80, T87)
U11_gga(T82, T78, T79, T80, T83, pE_out_ggga(T78, T82, T80, T83)) → insertD_out_gga(T82, tree(T78, T79, T80), tree(T78, T79, T83))
U5_ggga(T47, T42, T22, T48, insertD_out_gga(s(T47), T22, T48)) → pC_out_ggga(T47, T42, T22, T48)
U10_gga(T43, T42, T22, T23, T44, pC_out_ggga(T43, T42, T22, T44)) → insertD_out_gga(s(T43), tree(s(T42), T22, T23), tree(s(T42), T44, T23))
U9_gga(T31, T22, T23, T32, insertD_out_gga(0, T22, T32)) → insertD_out_gga(0, tree(s(T31), T22, T23), tree(s(T31), T32, T23))
U9_aga(T31, T22, T23, T32, insertD_out_gga(0, T22, T32)) → insertD_out_aga(0, tree(s(T31), T22, T23), tree(s(T31), T32, T23))
insertD_in_aga(s(T43), tree(s(T42), T22, T23), tree(s(T42), T44, T23)) → U10_aga(T43, T42, T22, T23, T44, pC_in_agga(T43, T42, T22, T44))
pC_in_agga(T43, T42, T22, T44) → U3_agga(T43, T42, T22, T44, lessA_in_ag(T43, T42))
lessA_in_ag(0, s(T55)) → lessA_out_ag(0, s(T55))
lessA_in_ag(s(T62), s(T61)) → U1_ag(T62, T61, lessA_in_ag(T62, T61))
U1_ag(T62, T61, lessA_out_ag(T62, T61)) → lessA_out_ag(s(T62), s(T61))
U3_agga(T43, T42, T22, T44, lessA_out_ag(T43, T42)) → pC_out_agga(T43, T42, T22, T44)
pC_in_agga(T47, T42, T22, T48) → U4_agga(T47, T42, T22, T48, lessA_in_ag(T47, T42))
U4_agga(T47, T42, T22, T48, lessA_out_ag(T47, T42)) → U5_agga(T47, T42, T22, T48, insertD_in_gga(s(T47), T22, T48))
U5_agga(T47, T42, T22, T48, insertD_out_gga(s(T47), T22, T48)) → pC_out_agga(T47, T42, T22, T48)
U10_aga(T43, T42, T22, T23, T44, pC_out_agga(T43, T42, T22, T44)) → insertD_out_aga(s(T43), tree(s(T42), T22, T23), tree(s(T42), T44, T23))
insertD_in_aga(T82, tree(T78, T79, T80), tree(T78, T79, T83)) → U11_aga(T82, T78, T79, T80, T83, pE_in_gaga(T78, T82, T80, T83))
pE_in_gaga(T78, T82, T80, T83) → U6_gaga(T78, T82, T80, T83, lessB_in_ga(T78, T82))
lessB_in_ga(0, s(T94)) → lessB_out_ga(0, s(T94))
lessB_in_ga(s(T99), s(T101)) → U2_ga(T99, T101, lessB_in_ga(T99, T101))
U2_ga(T99, T101, lessB_out_ga(T99, T101)) → lessB_out_ga(s(T99), s(T101))
U6_gaga(T78, T82, T80, T83, lessB_out_ga(T78, T82)) → pE_out_gaga(T78, T82, T80, T83)
pE_in_gaga(T78, T86, T80, T87) → U7_gaga(T78, T86, T80, T87, lessB_in_ga(T78, T86))
U7_gaga(T78, T86, T80, T87, lessB_out_ga(T78, T86)) → U8_gaga(T78, T86, T80, T87, insertD_in_aga(T86, T80, T87))
insertD_in_aga(s(T124), tree(0, T113, T114), tree(0, T113, T123)) → U12_aga(T124, T113, T114, T123, insertD_in_aga(s(T124), T114, T123))
insertD_in_aga(s(T133), tree(s(T131), T113, T114), tree(s(T131), T113, T134)) → U13_aga(T133, T131, T113, T114, T134, lessB_in_ga(T131, T133))
U13_aga(T133, T131, T113, T114, T134, lessB_out_ga(T131, T133)) → insertD_out_aga(s(T133), tree(s(T131), T113, T114), tree(s(T131), T113, T134))
insertD_in_aga(s(T137), tree(s(T131), T113, T114), tree(s(T131), T113, T138)) → U14_aga(T137, T131, T113, T114, T138, lessB_in_ga(T131, T137))
U14_aga(T137, T131, T113, T114, T138, lessB_out_ga(T131, T137)) → U15_aga(T137, T131, T113, T114, T138, insertD_in_aga(s(T137), T114, T138))
insertD_in_aga(0, tree(s(T161), T152, T153), tree(s(T161), T162, T153)) → U16_aga(T161, T152, T153, T162, insertD_in_gga(0, T152, T162))
U16_aga(T161, T152, T153, T162, insertD_out_gga(0, T152, T162)) → insertD_out_aga(0, tree(s(T161), T152, T153), tree(s(T161), T162, T153))
insertD_in_aga(s(T173), tree(s(T172), T152, T153), tree(s(T172), T174, T153)) → U17_aga(T173, T172, T152, T153, T174, pC_in_agga(T173, T172, T152, T174))
U17_aga(T173, T172, T152, T153, T174, pC_out_agga(T173, T172, T152, T174)) → insertD_out_aga(s(T173), tree(s(T172), T152, T153), tree(s(T172), T174, T153))
insertD_in_aga(T192, tree(T188, T189, T190), tree(T188, T189, T193)) → U18_aga(T192, T188, T189, T190, T193, pE_in_gaga(T188, T192, T190, T193))
U18_aga(T192, T188, T189, T190, T193, pE_out_gaga(T188, T192, T190, T193)) → insertD_out_aga(T192, tree(T188, T189, T190), tree(T188, T189, T193))
insertD_in_aga(s(T214), tree(0, T203, T204), tree(0, T203, T213)) → U19_aga(T214, T203, T204, T213, insertD_in_aga(s(T214), T204, T213))
insertD_in_aga(s(T223), tree(s(T221), T203, T204), tree(s(T221), T203, T224)) → U20_aga(T223, T221, T203, T204, T224, lessB_in_ga(T221, T223))
U20_aga(T223, T221, T203, T204, T224, lessB_out_ga(T221, T223)) → insertD_out_aga(s(T223), tree(s(T221), T203, T204), tree(s(T221), T203, T224))
insertD_in_aga(s(T227), tree(s(T221), T203, T204), tree(s(T221), T203, T228)) → U21_aga(T227, T221, T203, T204, T228, lessB_in_ga(T221, T227))
U21_aga(T227, T221, T203, T204, T228, lessB_out_ga(T221, T227)) → U22_aga(T227, T221, T203, T204, T228, insertD_in_aga(s(T227), T204, T228))
U22_aga(T227, T221, T203, T204, T228, insertD_out_aga(s(T227), T204, T228)) → insertD_out_aga(s(T227), tree(s(T221), T203, T204), tree(s(T221), T203, T228))
U19_aga(T214, T203, T204, T213, insertD_out_aga(s(T214), T204, T213)) → insertD_out_aga(s(T214), tree(0, T203, T204), tree(0, T203, T213))
U15_aga(T137, T131, T113, T114, T138, insertD_out_aga(s(T137), T114, T138)) → insertD_out_aga(s(T137), tree(s(T131), T113, T114), tree(s(T131), T113, T138))
U12_aga(T124, T113, T114, T123, insertD_out_aga(s(T124), T114, T123)) → insertD_out_aga(s(T124), tree(0, T113, T114), tree(0, T113, T123))
U8_gaga(T78, T86, T80, T87, insertD_out_aga(T86, T80, T87)) → pE_out_gaga(T78, T86, T80, T87)
U11_aga(T82, T78, T79, T80, T83, pE_out_gaga(T78, T82, T80, T83)) → insertD_out_aga(T82, tree(T78, T79, T80), tree(T78, T79, T83))
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
insertD_in_aga(T5, void, tree(T5, void, void)) → insertD_out_aga(T5, void, tree(T5, void, void))
insertD_in_aga(T12, tree(T12, T13, T14), tree(T12, T13, T14)) → insertD_out_aga(T12, tree(T12, T13, T14), tree(T12, T13, T14))
insertD_in_aga(0, tree(s(T31), T22, T23), tree(s(T31), T32, T23)) → U9_aga(T31, T22, T23, T32, insertD_in_gga(0, T22, T32))
insertD_in_gga(T5, void, tree(T5, void, void)) → insertD_out_gga(T5, void, tree(T5, void, void))
insertD_in_gga(T12, tree(T12, T13, T14), tree(T12, T13, T14)) → insertD_out_gga(T12, tree(T12, T13, T14), tree(T12, T13, T14))
insertD_in_gga(0, tree(s(T31), T22, T23), tree(s(T31), T32, T23)) → U9_gga(T31, T22, T23, T32, insertD_in_gga(0, T22, T32))
insertD_in_gga(s(T43), tree(s(T42), T22, T23), tree(s(T42), T44, T23)) → U10_gga(T43, T42, T22, T23, T44, pC_in_ggga(T43, T42, T22, T44))
pC_in_ggga(T43, T42, T22, T44) → U3_ggga(T43, T42, T22, T44, lessA_in_gg(T43, T42))
lessA_in_gg(0, s(T55)) → lessA_out_gg(0, s(T55))
lessA_in_gg(s(T62), s(T61)) → U1_gg(T62, T61, lessA_in_gg(T62, T61))
U1_gg(T62, T61, lessA_out_gg(T62, T61)) → lessA_out_gg(s(T62), s(T61))
U3_ggga(T43, T42, T22, T44, lessA_out_gg(T43, T42)) → pC_out_ggga(T43, T42, T22, T44)
pC_in_ggga(T47, T42, T22, T48) → U4_ggga(T47, T42, T22, T48, lessA_in_gg(T47, T42))
U4_ggga(T47, T42, T22, T48, lessA_out_gg(T47, T42)) → U5_ggga(T47, T42, T22, T48, insertD_in_gga(s(T47), T22, T48))
insertD_in_gga(T82, tree(T78, T79, T80), tree(T78, T79, T83)) → U11_gga(T82, T78, T79, T80, T83, pE_in_ggga(T78, T82, T80, T83))
pE_in_ggga(T78, T82, T80, T83) → U6_ggga(T78, T82, T80, T83, lessB_in_gg(T78, T82))
lessB_in_gg(0, s(T94)) → lessB_out_gg(0, s(T94))
lessB_in_gg(s(T99), s(T101)) → U2_gg(T99, T101, lessB_in_gg(T99, T101))
U2_gg(T99, T101, lessB_out_gg(T99, T101)) → lessB_out_gg(s(T99), s(T101))
U6_ggga(T78, T82, T80, T83, lessB_out_gg(T78, T82)) → pE_out_ggga(T78, T82, T80, T83)
pE_in_ggga(T78, T86, T80, T87) → U7_ggga(T78, T86, T80, T87, lessB_in_gg(T78, T86))
U7_ggga(T78, T86, T80, T87, lessB_out_gg(T78, T86)) → U8_ggga(T78, T86, T80, T87, insertD_in_gga(T86, T80, T87))
insertD_in_gga(s(T124), tree(0, T113, T114), tree(0, T113, T123)) → U12_gga(T124, T113, T114, T123, insertD_in_gga(s(T124), T114, T123))
insertD_in_gga(s(T133), tree(s(T131), T113, T114), tree(s(T131), T113, T134)) → U13_gga(T133, T131, T113, T114, T134, lessB_in_gg(T131, T133))
U13_gga(T133, T131, T113, T114, T134, lessB_out_gg(T131, T133)) → insertD_out_gga(s(T133), tree(s(T131), T113, T114), tree(s(T131), T113, T134))
insertD_in_gga(s(T137), tree(s(T131), T113, T114), tree(s(T131), T113, T138)) → U14_gga(T137, T131, T113, T114, T138, lessB_in_gg(T131, T137))
U14_gga(T137, T131, T113, T114, T138, lessB_out_gg(T131, T137)) → U15_gga(T137, T131, T113, T114, T138, insertD_in_gga(s(T137), T114, T138))
insertD_in_gga(0, tree(s(T161), T152, T153), tree(s(T161), T162, T153)) → U16_gga(T161, T152, T153, T162, insertD_in_gga(0, T152, T162))
insertD_in_gga(s(T173), tree(s(T172), T152, T153), tree(s(T172), T174, T153)) → U17_gga(T173, T172, T152, T153, T174, pC_in_ggga(T173, T172, T152, T174))
U17_gga(T173, T172, T152, T153, T174, pC_out_ggga(T173, T172, T152, T174)) → insertD_out_gga(s(T173), tree(s(T172), T152, T153), tree(s(T172), T174, T153))
insertD_in_gga(T192, tree(T188, T189, T190), tree(T188, T189, T193)) → U18_gga(T192, T188, T189, T190, T193, pE_in_ggga(T188, T192, T190, T193))
U18_gga(T192, T188, T189, T190, T193, pE_out_ggga(T188, T192, T190, T193)) → insertD_out_gga(T192, tree(T188, T189, T190), tree(T188, T189, T193))
insertD_in_gga(s(T214), tree(0, T203, T204), tree(0, T203, T213)) → U19_gga(T214, T203, T204, T213, insertD_in_gga(s(T214), T204, T213))
insertD_in_gga(s(T223), tree(s(T221), T203, T204), tree(s(T221), T203, T224)) → U20_gga(T223, T221, T203, T204, T224, lessB_in_gg(T221, T223))
U20_gga(T223, T221, T203, T204, T224, lessB_out_gg(T221, T223)) → insertD_out_gga(s(T223), tree(s(T221), T203, T204), tree(s(T221), T203, T224))
insertD_in_gga(s(T227), tree(s(T221), T203, T204), tree(s(T221), T203, T228)) → U21_gga(T227, T221, T203, T204, T228, lessB_in_gg(T221, T227))
U21_gga(T227, T221, T203, T204, T228, lessB_out_gg(T221, T227)) → U22_gga(T227, T221, T203, T204, T228, insertD_in_gga(s(T227), T204, T228))
U22_gga(T227, T221, T203, T204, T228, insertD_out_gga(s(T227), T204, T228)) → insertD_out_gga(s(T227), tree(s(T221), T203, T204), tree(s(T221), T203, T228))
U19_gga(T214, T203, T204, T213, insertD_out_gga(s(T214), T204, T213)) → insertD_out_gga(s(T214), tree(0, T203, T204), tree(0, T203, T213))
U16_gga(T161, T152, T153, T162, insertD_out_gga(0, T152, T162)) → insertD_out_gga(0, tree(s(T161), T152, T153), tree(s(T161), T162, T153))
U15_gga(T137, T131, T113, T114, T138, insertD_out_gga(s(T137), T114, T138)) → insertD_out_gga(s(T137), tree(s(T131), T113, T114), tree(s(T131), T113, T138))
U12_gga(T124, T113, T114, T123, insertD_out_gga(s(T124), T114, T123)) → insertD_out_gga(s(T124), tree(0, T113, T114), tree(0, T113, T123))
U8_ggga(T78, T86, T80, T87, insertD_out_gga(T86, T80, T87)) → pE_out_ggga(T78, T86, T80, T87)
U11_gga(T82, T78, T79, T80, T83, pE_out_ggga(T78, T82, T80, T83)) → insertD_out_gga(T82, tree(T78, T79, T80), tree(T78, T79, T83))
U5_ggga(T47, T42, T22, T48, insertD_out_gga(s(T47), T22, T48)) → pC_out_ggga(T47, T42, T22, T48)
U10_gga(T43, T42, T22, T23, T44, pC_out_ggga(T43, T42, T22, T44)) → insertD_out_gga(s(T43), tree(s(T42), T22, T23), tree(s(T42), T44, T23))
U9_gga(T31, T22, T23, T32, insertD_out_gga(0, T22, T32)) → insertD_out_gga(0, tree(s(T31), T22, T23), tree(s(T31), T32, T23))
U9_aga(T31, T22, T23, T32, insertD_out_gga(0, T22, T32)) → insertD_out_aga(0, tree(s(T31), T22, T23), tree(s(T31), T32, T23))
insertD_in_aga(s(T43), tree(s(T42), T22, T23), tree(s(T42), T44, T23)) → U10_aga(T43, T42, T22, T23, T44, pC_in_agga(T43, T42, T22, T44))
pC_in_agga(T43, T42, T22, T44) → U3_agga(T43, T42, T22, T44, lessA_in_ag(T43, T42))
lessA_in_ag(0, s(T55)) → lessA_out_ag(0, s(T55))
lessA_in_ag(s(T62), s(T61)) → U1_ag(T62, T61, lessA_in_ag(T62, T61))
U1_ag(T62, T61, lessA_out_ag(T62, T61)) → lessA_out_ag(s(T62), s(T61))
U3_agga(T43, T42, T22, T44, lessA_out_ag(T43, T42)) → pC_out_agga(T43, T42, T22, T44)
pC_in_agga(T47, T42, T22, T48) → U4_agga(T47, T42, T22, T48, lessA_in_ag(T47, T42))
U4_agga(T47, T42, T22, T48, lessA_out_ag(T47, T42)) → U5_agga(T47, T42, T22, T48, insertD_in_gga(s(T47), T22, T48))
U5_agga(T47, T42, T22, T48, insertD_out_gga(s(T47), T22, T48)) → pC_out_agga(T47, T42, T22, T48)
U10_aga(T43, T42, T22, T23, T44, pC_out_agga(T43, T42, T22, T44)) → insertD_out_aga(s(T43), tree(s(T42), T22, T23), tree(s(T42), T44, T23))
insertD_in_aga(T82, tree(T78, T79, T80), tree(T78, T79, T83)) → U11_aga(T82, T78, T79, T80, T83, pE_in_gaga(T78, T82, T80, T83))
pE_in_gaga(T78, T82, T80, T83) → U6_gaga(T78, T82, T80, T83, lessB_in_ga(T78, T82))
lessB_in_ga(0, s(T94)) → lessB_out_ga(0, s(T94))
lessB_in_ga(s(T99), s(T101)) → U2_ga(T99, T101, lessB_in_ga(T99, T101))
U2_ga(T99, T101, lessB_out_ga(T99, T101)) → lessB_out_ga(s(T99), s(T101))
U6_gaga(T78, T82, T80, T83, lessB_out_ga(T78, T82)) → pE_out_gaga(T78, T82, T80, T83)
pE_in_gaga(T78, T86, T80, T87) → U7_gaga(T78, T86, T80, T87, lessB_in_ga(T78, T86))
U7_gaga(T78, T86, T80, T87, lessB_out_ga(T78, T86)) → U8_gaga(T78, T86, T80, T87, insertD_in_aga(T86, T80, T87))
insertD_in_aga(s(T124), tree(0, T113, T114), tree(0, T113, T123)) → U12_aga(T124, T113, T114, T123, insertD_in_aga(s(T124), T114, T123))
insertD_in_aga(s(T133), tree(s(T131), T113, T114), tree(s(T131), T113, T134)) → U13_aga(T133, T131, T113, T114, T134, lessB_in_ga(T131, T133))
U13_aga(T133, T131, T113, T114, T134, lessB_out_ga(T131, T133)) → insertD_out_aga(s(T133), tree(s(T131), T113, T114), tree(s(T131), T113, T134))
insertD_in_aga(s(T137), tree(s(T131), T113, T114), tree(s(T131), T113, T138)) → U14_aga(T137, T131, T113, T114, T138, lessB_in_ga(T131, T137))
U14_aga(T137, T131, T113, T114, T138, lessB_out_ga(T131, T137)) → U15_aga(T137, T131, T113, T114, T138, insertD_in_aga(s(T137), T114, T138))
insertD_in_aga(0, tree(s(T161), T152, T153), tree(s(T161), T162, T153)) → U16_aga(T161, T152, T153, T162, insertD_in_gga(0, T152, T162))
U16_aga(T161, T152, T153, T162, insertD_out_gga(0, T152, T162)) → insertD_out_aga(0, tree(s(T161), T152, T153), tree(s(T161), T162, T153))
insertD_in_aga(s(T173), tree(s(T172), T152, T153), tree(s(T172), T174, T153)) → U17_aga(T173, T172, T152, T153, T174, pC_in_agga(T173, T172, T152, T174))
U17_aga(T173, T172, T152, T153, T174, pC_out_agga(T173, T172, T152, T174)) → insertD_out_aga(s(T173), tree(s(T172), T152, T153), tree(s(T172), T174, T153))
insertD_in_aga(T192, tree(T188, T189, T190), tree(T188, T189, T193)) → U18_aga(T192, T188, T189, T190, T193, pE_in_gaga(T188, T192, T190, T193))
U18_aga(T192, T188, T189, T190, T193, pE_out_gaga(T188, T192, T190, T193)) → insertD_out_aga(T192, tree(T188, T189, T190), tree(T188, T189, T193))
insertD_in_aga(s(T214), tree(0, T203, T204), tree(0, T203, T213)) → U19_aga(T214, T203, T204, T213, insertD_in_aga(s(T214), T204, T213))
insertD_in_aga(s(T223), tree(s(T221), T203, T204), tree(s(T221), T203, T224)) → U20_aga(T223, T221, T203, T204, T224, lessB_in_ga(T221, T223))
U20_aga(T223, T221, T203, T204, T224, lessB_out_ga(T221, T223)) → insertD_out_aga(s(T223), tree(s(T221), T203, T204), tree(s(T221), T203, T224))
insertD_in_aga(s(T227), tree(s(T221), T203, T204), tree(s(T221), T203, T228)) → U21_aga(T227, T221, T203, T204, T228, lessB_in_ga(T221, T227))
U21_aga(T227, T221, T203, T204, T228, lessB_out_ga(T221, T227)) → U22_aga(T227, T221, T203, T204, T228, insertD_in_aga(s(T227), T204, T228))
U22_aga(T227, T221, T203, T204, T228, insertD_out_aga(s(T227), T204, T228)) → insertD_out_aga(s(T227), tree(s(T221), T203, T204), tree(s(T221), T203, T228))
U19_aga(T214, T203, T204, T213, insertD_out_aga(s(T214), T204, T213)) → insertD_out_aga(s(T214), tree(0, T203, T204), tree(0, T203, T213))
U15_aga(T137, T131, T113, T114, T138, insertD_out_aga(s(T137), T114, T138)) → insertD_out_aga(s(T137), tree(s(T131), T113, T114), tree(s(T131), T113, T138))
U12_aga(T124, T113, T114, T123, insertD_out_aga(s(T124), T114, T123)) → insertD_out_aga(s(T124), tree(0, T113, T114), tree(0, T113, T123))
U8_gaga(T78, T86, T80, T87, insertD_out_aga(T86, T80, T87)) → pE_out_gaga(T78, T86, T80, T87)
U11_aga(T82, T78, T79, T80, T83, pE_out_gaga(T78, T82, T80, T83)) → insertD_out_aga(T82, tree(T78, T79, T80), tree(T78, T79, T83))
INSERTD_IN_AGA(0, tree(s(T31), T22, T23), tree(s(T31), T32, T23)) → U9_AGA(T31, T22, T23, T32, insertD_in_gga(0, T22, T32))
INSERTD_IN_AGA(0, tree(s(T31), T22, T23), tree(s(T31), T32, T23)) → INSERTD_IN_GGA(0, T22, T32)
INSERTD_IN_GGA(0, tree(s(T31), T22, T23), tree(s(T31), T32, T23)) → U9_GGA(T31, T22, T23, T32, insertD_in_gga(0, T22, T32))
INSERTD_IN_GGA(0, tree(s(T31), T22, T23), tree(s(T31), T32, T23)) → INSERTD_IN_GGA(0, T22, T32)
INSERTD_IN_GGA(s(T43), tree(s(T42), T22, T23), tree(s(T42), T44, T23)) → U10_GGA(T43, T42, T22, T23, T44, pC_in_ggga(T43, T42, T22, T44))
INSERTD_IN_GGA(s(T43), tree(s(T42), T22, T23), tree(s(T42), T44, T23)) → PC_IN_GGGA(T43, T42, T22, T44)
PC_IN_GGGA(T43, T42, T22, T44) → U3_GGGA(T43, T42, T22, T44, lessA_in_gg(T43, T42))
PC_IN_GGGA(T43, T42, T22, T44) → LESSA_IN_GG(T43, T42)
LESSA_IN_GG(s(T62), s(T61)) → U1_GG(T62, T61, lessA_in_gg(T62, T61))
LESSA_IN_GG(s(T62), s(T61)) → LESSA_IN_GG(T62, T61)
PC_IN_GGGA(T47, T42, T22, T48) → U4_GGGA(T47, T42, T22, T48, lessA_in_gg(T47, T42))
U4_GGGA(T47, T42, T22, T48, lessA_out_gg(T47, T42)) → U5_GGGA(T47, T42, T22, T48, insertD_in_gga(s(T47), T22, T48))
U4_GGGA(T47, T42, T22, T48, lessA_out_gg(T47, T42)) → INSERTD_IN_GGA(s(T47), T22, T48)
INSERTD_IN_GGA(T82, tree(T78, T79, T80), tree(T78, T79, T83)) → U11_GGA(T82, T78, T79, T80, T83, pE_in_ggga(T78, T82, T80, T83))
INSERTD_IN_GGA(T82, tree(T78, T79, T80), tree(T78, T79, T83)) → PE_IN_GGGA(T78, T82, T80, T83)
PE_IN_GGGA(T78, T82, T80, T83) → U6_GGGA(T78, T82, T80, T83, lessB_in_gg(T78, T82))
PE_IN_GGGA(T78, T82, T80, T83) → LESSB_IN_GG(T78, T82)
LESSB_IN_GG(s(T99), s(T101)) → U2_GG(T99, T101, lessB_in_gg(T99, T101))
LESSB_IN_GG(s(T99), s(T101)) → LESSB_IN_GG(T99, T101)
PE_IN_GGGA(T78, T86, T80, T87) → U7_GGGA(T78, T86, T80, T87, lessB_in_gg(T78, T86))
U7_GGGA(T78, T86, T80, T87, lessB_out_gg(T78, T86)) → U8_GGGA(T78, T86, T80, T87, insertD_in_gga(T86, T80, T87))
U7_GGGA(T78, T86, T80, T87, lessB_out_gg(T78, T86)) → INSERTD_IN_GGA(T86, T80, T87)
INSERTD_IN_GGA(s(T124), tree(0, T113, T114), tree(0, T113, T123)) → U12_GGA(T124, T113, T114, T123, insertD_in_gga(s(T124), T114, T123))
INSERTD_IN_GGA(s(T124), tree(0, T113, T114), tree(0, T113, T123)) → INSERTD_IN_GGA(s(T124), T114, T123)
INSERTD_IN_GGA(s(T133), tree(s(T131), T113, T114), tree(s(T131), T113, T134)) → U13_GGA(T133, T131, T113, T114, T134, lessB_in_gg(T131, T133))
INSERTD_IN_GGA(s(T133), tree(s(T131), T113, T114), tree(s(T131), T113, T134)) → LESSB_IN_GG(T131, T133)
INSERTD_IN_GGA(s(T137), tree(s(T131), T113, T114), tree(s(T131), T113, T138)) → U14_GGA(T137, T131, T113, T114, T138, lessB_in_gg(T131, T137))
U14_GGA(T137, T131, T113, T114, T138, lessB_out_gg(T131, T137)) → U15_GGA(T137, T131, T113, T114, T138, insertD_in_gga(s(T137), T114, T138))
U14_GGA(T137, T131, T113, T114, T138, lessB_out_gg(T131, T137)) → INSERTD_IN_GGA(s(T137), T114, T138)
INSERTD_IN_GGA(0, tree(s(T161), T152, T153), tree(s(T161), T162, T153)) → U16_GGA(T161, T152, T153, T162, insertD_in_gga(0, T152, T162))
INSERTD_IN_GGA(s(T173), tree(s(T172), T152, T153), tree(s(T172), T174, T153)) → U17_GGA(T173, T172, T152, T153, T174, pC_in_ggga(T173, T172, T152, T174))
INSERTD_IN_GGA(T192, tree(T188, T189, T190), tree(T188, T189, T193)) → U18_GGA(T192, T188, T189, T190, T193, pE_in_ggga(T188, T192, T190, T193))
INSERTD_IN_GGA(s(T214), tree(0, T203, T204), tree(0, T203, T213)) → U19_GGA(T214, T203, T204, T213, insertD_in_gga(s(T214), T204, T213))
INSERTD_IN_GGA(s(T223), tree(s(T221), T203, T204), tree(s(T221), T203, T224)) → U20_GGA(T223, T221, T203, T204, T224, lessB_in_gg(T221, T223))
INSERTD_IN_GGA(s(T227), tree(s(T221), T203, T204), tree(s(T221), T203, T228)) → U21_GGA(T227, T221, T203, T204, T228, lessB_in_gg(T221, T227))
U21_GGA(T227, T221, T203, T204, T228, lessB_out_gg(T221, T227)) → U22_GGA(T227, T221, T203, T204, T228, insertD_in_gga(s(T227), T204, T228))
U21_GGA(T227, T221, T203, T204, T228, lessB_out_gg(T221, T227)) → INSERTD_IN_GGA(s(T227), T204, T228)
INSERTD_IN_AGA(s(T43), tree(s(T42), T22, T23), tree(s(T42), T44, T23)) → U10_AGA(T43, T42, T22, T23, T44, pC_in_agga(T43, T42, T22, T44))
INSERTD_IN_AGA(s(T43), tree(s(T42), T22, T23), tree(s(T42), T44, T23)) → PC_IN_AGGA(T43, T42, T22, T44)
PC_IN_AGGA(T43, T42, T22, T44) → U3_AGGA(T43, T42, T22, T44, lessA_in_ag(T43, T42))
PC_IN_AGGA(T43, T42, T22, T44) → LESSA_IN_AG(T43, T42)
LESSA_IN_AG(s(T62), s(T61)) → U1_AG(T62, T61, lessA_in_ag(T62, T61))
LESSA_IN_AG(s(T62), s(T61)) → LESSA_IN_AG(T62, T61)
PC_IN_AGGA(T47, T42, T22, T48) → U4_AGGA(T47, T42, T22, T48, lessA_in_ag(T47, T42))
U4_AGGA(T47, T42, T22, T48, lessA_out_ag(T47, T42)) → U5_AGGA(T47, T42, T22, T48, insertD_in_gga(s(T47), T22, T48))
U4_AGGA(T47, T42, T22, T48, lessA_out_ag(T47, T42)) → INSERTD_IN_GGA(s(T47), T22, T48)
INSERTD_IN_AGA(T82, tree(T78, T79, T80), tree(T78, T79, T83)) → U11_AGA(T82, T78, T79, T80, T83, pE_in_gaga(T78, T82, T80, T83))
INSERTD_IN_AGA(T82, tree(T78, T79, T80), tree(T78, T79, T83)) → PE_IN_GAGA(T78, T82, T80, T83)
PE_IN_GAGA(T78, T82, T80, T83) → U6_GAGA(T78, T82, T80, T83, lessB_in_ga(T78, T82))
PE_IN_GAGA(T78, T82, T80, T83) → LESSB_IN_GA(T78, T82)
LESSB_IN_GA(s(T99), s(T101)) → U2_GA(T99, T101, lessB_in_ga(T99, T101))
LESSB_IN_GA(s(T99), s(T101)) → LESSB_IN_GA(T99, T101)
PE_IN_GAGA(T78, T86, T80, T87) → U7_GAGA(T78, T86, T80, T87, lessB_in_ga(T78, T86))
U7_GAGA(T78, T86, T80, T87, lessB_out_ga(T78, T86)) → U8_GAGA(T78, T86, T80, T87, insertD_in_aga(T86, T80, T87))
U7_GAGA(T78, T86, T80, T87, lessB_out_ga(T78, T86)) → INSERTD_IN_AGA(T86, T80, T87)
INSERTD_IN_AGA(s(T124), tree(0, T113, T114), tree(0, T113, T123)) → U12_AGA(T124, T113, T114, T123, insertD_in_aga(s(T124), T114, T123))
INSERTD_IN_AGA(s(T124), tree(0, T113, T114), tree(0, T113, T123)) → INSERTD_IN_AGA(s(T124), T114, T123)
INSERTD_IN_AGA(s(T133), tree(s(T131), T113, T114), tree(s(T131), T113, T134)) → U13_AGA(T133, T131, T113, T114, T134, lessB_in_ga(T131, T133))
INSERTD_IN_AGA(s(T133), tree(s(T131), T113, T114), tree(s(T131), T113, T134)) → LESSB_IN_GA(T131, T133)
INSERTD_IN_AGA(s(T137), tree(s(T131), T113, T114), tree(s(T131), T113, T138)) → U14_AGA(T137, T131, T113, T114, T138, lessB_in_ga(T131, T137))
U14_AGA(T137, T131, T113, T114, T138, lessB_out_ga(T131, T137)) → U15_AGA(T137, T131, T113, T114, T138, insertD_in_aga(s(T137), T114, T138))
U14_AGA(T137, T131, T113, T114, T138, lessB_out_ga(T131, T137)) → INSERTD_IN_AGA(s(T137), T114, T138)
INSERTD_IN_AGA(0, tree(s(T161), T152, T153), tree(s(T161), T162, T153)) → U16_AGA(T161, T152, T153, T162, insertD_in_gga(0, T152, T162))
INSERTD_IN_AGA(s(T173), tree(s(T172), T152, T153), tree(s(T172), T174, T153)) → U17_AGA(T173, T172, T152, T153, T174, pC_in_agga(T173, T172, T152, T174))
INSERTD_IN_AGA(T192, tree(T188, T189, T190), tree(T188, T189, T193)) → U18_AGA(T192, T188, T189, T190, T193, pE_in_gaga(T188, T192, T190, T193))
INSERTD_IN_AGA(s(T214), tree(0, T203, T204), tree(0, T203, T213)) → U19_AGA(T214, T203, T204, T213, insertD_in_aga(s(T214), T204, T213))
INSERTD_IN_AGA(s(T223), tree(s(T221), T203, T204), tree(s(T221), T203, T224)) → U20_AGA(T223, T221, T203, T204, T224, lessB_in_ga(T221, T223))
INSERTD_IN_AGA(s(T227), tree(s(T221), T203, T204), tree(s(T221), T203, T228)) → U21_AGA(T227, T221, T203, T204, T228, lessB_in_ga(T221, T227))
U21_AGA(T227, T221, T203, T204, T228, lessB_out_ga(T221, T227)) → U22_AGA(T227, T221, T203, T204, T228, insertD_in_aga(s(T227), T204, T228))
U21_AGA(T227, T221, T203, T204, T228, lessB_out_ga(T221, T227)) → INSERTD_IN_AGA(s(T227), T204, T228)
insertD_in_aga(T5, void, tree(T5, void, void)) → insertD_out_aga(T5, void, tree(T5, void, void))
insertD_in_aga(T12, tree(T12, T13, T14), tree(T12, T13, T14)) → insertD_out_aga(T12, tree(T12, T13, T14), tree(T12, T13, T14))
insertD_in_aga(0, tree(s(T31), T22, T23), tree(s(T31), T32, T23)) → U9_aga(T31, T22, T23, T32, insertD_in_gga(0, T22, T32))
insertD_in_gga(T5, void, tree(T5, void, void)) → insertD_out_gga(T5, void, tree(T5, void, void))
insertD_in_gga(T12, tree(T12, T13, T14), tree(T12, T13, T14)) → insertD_out_gga(T12, tree(T12, T13, T14), tree(T12, T13, T14))
insertD_in_gga(0, tree(s(T31), T22, T23), tree(s(T31), T32, T23)) → U9_gga(T31, T22, T23, T32, insertD_in_gga(0, T22, T32))
insertD_in_gga(s(T43), tree(s(T42), T22, T23), tree(s(T42), T44, T23)) → U10_gga(T43, T42, T22, T23, T44, pC_in_ggga(T43, T42, T22, T44))
pC_in_ggga(T43, T42, T22, T44) → U3_ggga(T43, T42, T22, T44, lessA_in_gg(T43, T42))
lessA_in_gg(0, s(T55)) → lessA_out_gg(0, s(T55))
lessA_in_gg(s(T62), s(T61)) → U1_gg(T62, T61, lessA_in_gg(T62, T61))
U1_gg(T62, T61, lessA_out_gg(T62, T61)) → lessA_out_gg(s(T62), s(T61))
U3_ggga(T43, T42, T22, T44, lessA_out_gg(T43, T42)) → pC_out_ggga(T43, T42, T22, T44)
pC_in_ggga(T47, T42, T22, T48) → U4_ggga(T47, T42, T22, T48, lessA_in_gg(T47, T42))
U4_ggga(T47, T42, T22, T48, lessA_out_gg(T47, T42)) → U5_ggga(T47, T42, T22, T48, insertD_in_gga(s(T47), T22, T48))
insertD_in_gga(T82, tree(T78, T79, T80), tree(T78, T79, T83)) → U11_gga(T82, T78, T79, T80, T83, pE_in_ggga(T78, T82, T80, T83))
pE_in_ggga(T78, T82, T80, T83) → U6_ggga(T78, T82, T80, T83, lessB_in_gg(T78, T82))
lessB_in_gg(0, s(T94)) → lessB_out_gg(0, s(T94))
lessB_in_gg(s(T99), s(T101)) → U2_gg(T99, T101, lessB_in_gg(T99, T101))
U2_gg(T99, T101, lessB_out_gg(T99, T101)) → lessB_out_gg(s(T99), s(T101))
U6_ggga(T78, T82, T80, T83, lessB_out_gg(T78, T82)) → pE_out_ggga(T78, T82, T80, T83)
pE_in_ggga(T78, T86, T80, T87) → U7_ggga(T78, T86, T80, T87, lessB_in_gg(T78, T86))
U7_ggga(T78, T86, T80, T87, lessB_out_gg(T78, T86)) → U8_ggga(T78, T86, T80, T87, insertD_in_gga(T86, T80, T87))
insertD_in_gga(s(T124), tree(0, T113, T114), tree(0, T113, T123)) → U12_gga(T124, T113, T114, T123, insertD_in_gga(s(T124), T114, T123))
insertD_in_gga(s(T133), tree(s(T131), T113, T114), tree(s(T131), T113, T134)) → U13_gga(T133, T131, T113, T114, T134, lessB_in_gg(T131, T133))
U13_gga(T133, T131, T113, T114, T134, lessB_out_gg(T131, T133)) → insertD_out_gga(s(T133), tree(s(T131), T113, T114), tree(s(T131), T113, T134))
insertD_in_gga(s(T137), tree(s(T131), T113, T114), tree(s(T131), T113, T138)) → U14_gga(T137, T131, T113, T114, T138, lessB_in_gg(T131, T137))
U14_gga(T137, T131, T113, T114, T138, lessB_out_gg(T131, T137)) → U15_gga(T137, T131, T113, T114, T138, insertD_in_gga(s(T137), T114, T138))
insertD_in_gga(0, tree(s(T161), T152, T153), tree(s(T161), T162, T153)) → U16_gga(T161, T152, T153, T162, insertD_in_gga(0, T152, T162))
insertD_in_gga(s(T173), tree(s(T172), T152, T153), tree(s(T172), T174, T153)) → U17_gga(T173, T172, T152, T153, T174, pC_in_ggga(T173, T172, T152, T174))
U17_gga(T173, T172, T152, T153, T174, pC_out_ggga(T173, T172, T152, T174)) → insertD_out_gga(s(T173), tree(s(T172), T152, T153), tree(s(T172), T174, T153))
insertD_in_gga(T192, tree(T188, T189, T190), tree(T188, T189, T193)) → U18_gga(T192, T188, T189, T190, T193, pE_in_ggga(T188, T192, T190, T193))
U18_gga(T192, T188, T189, T190, T193, pE_out_ggga(T188, T192, T190, T193)) → insertD_out_gga(T192, tree(T188, T189, T190), tree(T188, T189, T193))
insertD_in_gga(s(T214), tree(0, T203, T204), tree(0, T203, T213)) → U19_gga(T214, T203, T204, T213, insertD_in_gga(s(T214), T204, T213))
insertD_in_gga(s(T223), tree(s(T221), T203, T204), tree(s(T221), T203, T224)) → U20_gga(T223, T221, T203, T204, T224, lessB_in_gg(T221, T223))
U20_gga(T223, T221, T203, T204, T224, lessB_out_gg(T221, T223)) → insertD_out_gga(s(T223), tree(s(T221), T203, T204), tree(s(T221), T203, T224))
insertD_in_gga(s(T227), tree(s(T221), T203, T204), tree(s(T221), T203, T228)) → U21_gga(T227, T221, T203, T204, T228, lessB_in_gg(T221, T227))
U21_gga(T227, T221, T203, T204, T228, lessB_out_gg(T221, T227)) → U22_gga(T227, T221, T203, T204, T228, insertD_in_gga(s(T227), T204, T228))
U22_gga(T227, T221, T203, T204, T228, insertD_out_gga(s(T227), T204, T228)) → insertD_out_gga(s(T227), tree(s(T221), T203, T204), tree(s(T221), T203, T228))
U19_gga(T214, T203, T204, T213, insertD_out_gga(s(T214), T204, T213)) → insertD_out_gga(s(T214), tree(0, T203, T204), tree(0, T203, T213))
U16_gga(T161, T152, T153, T162, insertD_out_gga(0, T152, T162)) → insertD_out_gga(0, tree(s(T161), T152, T153), tree(s(T161), T162, T153))
U15_gga(T137, T131, T113, T114, T138, insertD_out_gga(s(T137), T114, T138)) → insertD_out_gga(s(T137), tree(s(T131), T113, T114), tree(s(T131), T113, T138))
U12_gga(T124, T113, T114, T123, insertD_out_gga(s(T124), T114, T123)) → insertD_out_gga(s(T124), tree(0, T113, T114), tree(0, T113, T123))
U8_ggga(T78, T86, T80, T87, insertD_out_gga(T86, T80, T87)) → pE_out_ggga(T78, T86, T80, T87)
U11_gga(T82, T78, T79, T80, T83, pE_out_ggga(T78, T82, T80, T83)) → insertD_out_gga(T82, tree(T78, T79, T80), tree(T78, T79, T83))
U5_ggga(T47, T42, T22, T48, insertD_out_gga(s(T47), T22, T48)) → pC_out_ggga(T47, T42, T22, T48)
U10_gga(T43, T42, T22, T23, T44, pC_out_ggga(T43, T42, T22, T44)) → insertD_out_gga(s(T43), tree(s(T42), T22, T23), tree(s(T42), T44, T23))
U9_gga(T31, T22, T23, T32, insertD_out_gga(0, T22, T32)) → insertD_out_gga(0, tree(s(T31), T22, T23), tree(s(T31), T32, T23))
U9_aga(T31, T22, T23, T32, insertD_out_gga(0, T22, T32)) → insertD_out_aga(0, tree(s(T31), T22, T23), tree(s(T31), T32, T23))
insertD_in_aga(s(T43), tree(s(T42), T22, T23), tree(s(T42), T44, T23)) → U10_aga(T43, T42, T22, T23, T44, pC_in_agga(T43, T42, T22, T44))
pC_in_agga(T43, T42, T22, T44) → U3_agga(T43, T42, T22, T44, lessA_in_ag(T43, T42))
lessA_in_ag(0, s(T55)) → lessA_out_ag(0, s(T55))
lessA_in_ag(s(T62), s(T61)) → U1_ag(T62, T61, lessA_in_ag(T62, T61))
U1_ag(T62, T61, lessA_out_ag(T62, T61)) → lessA_out_ag(s(T62), s(T61))
U3_agga(T43, T42, T22, T44, lessA_out_ag(T43, T42)) → pC_out_agga(T43, T42, T22, T44)
pC_in_agga(T47, T42, T22, T48) → U4_agga(T47, T42, T22, T48, lessA_in_ag(T47, T42))
U4_agga(T47, T42, T22, T48, lessA_out_ag(T47, T42)) → U5_agga(T47, T42, T22, T48, insertD_in_gga(s(T47), T22, T48))
U5_agga(T47, T42, T22, T48, insertD_out_gga(s(T47), T22, T48)) → pC_out_agga(T47, T42, T22, T48)
U10_aga(T43, T42, T22, T23, T44, pC_out_agga(T43, T42, T22, T44)) → insertD_out_aga(s(T43), tree(s(T42), T22, T23), tree(s(T42), T44, T23))
insertD_in_aga(T82, tree(T78, T79, T80), tree(T78, T79, T83)) → U11_aga(T82, T78, T79, T80, T83, pE_in_gaga(T78, T82, T80, T83))
pE_in_gaga(T78, T82, T80, T83) → U6_gaga(T78, T82, T80, T83, lessB_in_ga(T78, T82))
lessB_in_ga(0, s(T94)) → lessB_out_ga(0, s(T94))
lessB_in_ga(s(T99), s(T101)) → U2_ga(T99, T101, lessB_in_ga(T99, T101))
U2_ga(T99, T101, lessB_out_ga(T99, T101)) → lessB_out_ga(s(T99), s(T101))
U6_gaga(T78, T82, T80, T83, lessB_out_ga(T78, T82)) → pE_out_gaga(T78, T82, T80, T83)
pE_in_gaga(T78, T86, T80, T87) → U7_gaga(T78, T86, T80, T87, lessB_in_ga(T78, T86))
U7_gaga(T78, T86, T80, T87, lessB_out_ga(T78, T86)) → U8_gaga(T78, T86, T80, T87, insertD_in_aga(T86, T80, T87))
insertD_in_aga(s(T124), tree(0, T113, T114), tree(0, T113, T123)) → U12_aga(T124, T113, T114, T123, insertD_in_aga(s(T124), T114, T123))
insertD_in_aga(s(T133), tree(s(T131), T113, T114), tree(s(T131), T113, T134)) → U13_aga(T133, T131, T113, T114, T134, lessB_in_ga(T131, T133))
U13_aga(T133, T131, T113, T114, T134, lessB_out_ga(T131, T133)) → insertD_out_aga(s(T133), tree(s(T131), T113, T114), tree(s(T131), T113, T134))
insertD_in_aga(s(T137), tree(s(T131), T113, T114), tree(s(T131), T113, T138)) → U14_aga(T137, T131, T113, T114, T138, lessB_in_ga(T131, T137))
U14_aga(T137, T131, T113, T114, T138, lessB_out_ga(T131, T137)) → U15_aga(T137, T131, T113, T114, T138, insertD_in_aga(s(T137), T114, T138))
insertD_in_aga(0, tree(s(T161), T152, T153), tree(s(T161), T162, T153)) → U16_aga(T161, T152, T153, T162, insertD_in_gga(0, T152, T162))
U16_aga(T161, T152, T153, T162, insertD_out_gga(0, T152, T162)) → insertD_out_aga(0, tree(s(T161), T152, T153), tree(s(T161), T162, T153))
insertD_in_aga(s(T173), tree(s(T172), T152, T153), tree(s(T172), T174, T153)) → U17_aga(T173, T172, T152, T153, T174, pC_in_agga(T173, T172, T152, T174))
U17_aga(T173, T172, T152, T153, T174, pC_out_agga(T173, T172, T152, T174)) → insertD_out_aga(s(T173), tree(s(T172), T152, T153), tree(s(T172), T174, T153))
insertD_in_aga(T192, tree(T188, T189, T190), tree(T188, T189, T193)) → U18_aga(T192, T188, T189, T190, T193, pE_in_gaga(T188, T192, T190, T193))
U18_aga(T192, T188, T189, T190, T193, pE_out_gaga(T188, T192, T190, T193)) → insertD_out_aga(T192, tree(T188, T189, T190), tree(T188, T189, T193))
insertD_in_aga(s(T214), tree(0, T203, T204), tree(0, T203, T213)) → U19_aga(T214, T203, T204, T213, insertD_in_aga(s(T214), T204, T213))
insertD_in_aga(s(T223), tree(s(T221), T203, T204), tree(s(T221), T203, T224)) → U20_aga(T223, T221, T203, T204, T224, lessB_in_ga(T221, T223))
U20_aga(T223, T221, T203, T204, T224, lessB_out_ga(T221, T223)) → insertD_out_aga(s(T223), tree(s(T221), T203, T204), tree(s(T221), T203, T224))
insertD_in_aga(s(T227), tree(s(T221), T203, T204), tree(s(T221), T203, T228)) → U21_aga(T227, T221, T203, T204, T228, lessB_in_ga(T221, T227))
U21_aga(T227, T221, T203, T204, T228, lessB_out_ga(T221, T227)) → U22_aga(T227, T221, T203, T204, T228, insertD_in_aga(s(T227), T204, T228))
U22_aga(T227, T221, T203, T204, T228, insertD_out_aga(s(T227), T204, T228)) → insertD_out_aga(s(T227), tree(s(T221), T203, T204), tree(s(T221), T203, T228))
U19_aga(T214, T203, T204, T213, insertD_out_aga(s(T214), T204, T213)) → insertD_out_aga(s(T214), tree(0, T203, T204), tree(0, T203, T213))
U15_aga(T137, T131, T113, T114, T138, insertD_out_aga(s(T137), T114, T138)) → insertD_out_aga(s(T137), tree(s(T131), T113, T114), tree(s(T131), T113, T138))
U12_aga(T124, T113, T114, T123, insertD_out_aga(s(T124), T114, T123)) → insertD_out_aga(s(T124), tree(0, T113, T114), tree(0, T113, T123))
U8_gaga(T78, T86, T80, T87, insertD_out_aga(T86, T80, T87)) → pE_out_gaga(T78, T86, T80, T87)
U11_aga(T82, T78, T79, T80, T83, pE_out_gaga(T78, T82, T80, T83)) → insertD_out_aga(T82, tree(T78, T79, T80), tree(T78, T79, T83))
INSERTD_IN_AGA(0, tree(s(T31), T22, T23), tree(s(T31), T32, T23)) → U9_AGA(T31, T22, T23, T32, insertD_in_gga(0, T22, T32))
INSERTD_IN_AGA(0, tree(s(T31), T22, T23), tree(s(T31), T32, T23)) → INSERTD_IN_GGA(0, T22, T32)
INSERTD_IN_GGA(0, tree(s(T31), T22, T23), tree(s(T31), T32, T23)) → U9_GGA(T31, T22, T23, T32, insertD_in_gga(0, T22, T32))
INSERTD_IN_GGA(0, tree(s(T31), T22, T23), tree(s(T31), T32, T23)) → INSERTD_IN_GGA(0, T22, T32)
INSERTD_IN_GGA(s(T43), tree(s(T42), T22, T23), tree(s(T42), T44, T23)) → U10_GGA(T43, T42, T22, T23, T44, pC_in_ggga(T43, T42, T22, T44))
INSERTD_IN_GGA(s(T43), tree(s(T42), T22, T23), tree(s(T42), T44, T23)) → PC_IN_GGGA(T43, T42, T22, T44)
PC_IN_GGGA(T43, T42, T22, T44) → U3_GGGA(T43, T42, T22, T44, lessA_in_gg(T43, T42))
PC_IN_GGGA(T43, T42, T22, T44) → LESSA_IN_GG(T43, T42)
LESSA_IN_GG(s(T62), s(T61)) → U1_GG(T62, T61, lessA_in_gg(T62, T61))
LESSA_IN_GG(s(T62), s(T61)) → LESSA_IN_GG(T62, T61)
PC_IN_GGGA(T47, T42, T22, T48) → U4_GGGA(T47, T42, T22, T48, lessA_in_gg(T47, T42))
U4_GGGA(T47, T42, T22, T48, lessA_out_gg(T47, T42)) → U5_GGGA(T47, T42, T22, T48, insertD_in_gga(s(T47), T22, T48))
U4_GGGA(T47, T42, T22, T48, lessA_out_gg(T47, T42)) → INSERTD_IN_GGA(s(T47), T22, T48)
INSERTD_IN_GGA(T82, tree(T78, T79, T80), tree(T78, T79, T83)) → U11_GGA(T82, T78, T79, T80, T83, pE_in_ggga(T78, T82, T80, T83))
INSERTD_IN_GGA(T82, tree(T78, T79, T80), tree(T78, T79, T83)) → PE_IN_GGGA(T78, T82, T80, T83)
PE_IN_GGGA(T78, T82, T80, T83) → U6_GGGA(T78, T82, T80, T83, lessB_in_gg(T78, T82))
PE_IN_GGGA(T78, T82, T80, T83) → LESSB_IN_GG(T78, T82)
LESSB_IN_GG(s(T99), s(T101)) → U2_GG(T99, T101, lessB_in_gg(T99, T101))
LESSB_IN_GG(s(T99), s(T101)) → LESSB_IN_GG(T99, T101)
PE_IN_GGGA(T78, T86, T80, T87) → U7_GGGA(T78, T86, T80, T87, lessB_in_gg(T78, T86))
U7_GGGA(T78, T86, T80, T87, lessB_out_gg(T78, T86)) → U8_GGGA(T78, T86, T80, T87, insertD_in_gga(T86, T80, T87))
U7_GGGA(T78, T86, T80, T87, lessB_out_gg(T78, T86)) → INSERTD_IN_GGA(T86, T80, T87)
INSERTD_IN_GGA(s(T124), tree(0, T113, T114), tree(0, T113, T123)) → U12_GGA(T124, T113, T114, T123, insertD_in_gga(s(T124), T114, T123))
INSERTD_IN_GGA(s(T124), tree(0, T113, T114), tree(0, T113, T123)) → INSERTD_IN_GGA(s(T124), T114, T123)
INSERTD_IN_GGA(s(T133), tree(s(T131), T113, T114), tree(s(T131), T113, T134)) → U13_GGA(T133, T131, T113, T114, T134, lessB_in_gg(T131, T133))
INSERTD_IN_GGA(s(T133), tree(s(T131), T113, T114), tree(s(T131), T113, T134)) → LESSB_IN_GG(T131, T133)
INSERTD_IN_GGA(s(T137), tree(s(T131), T113, T114), tree(s(T131), T113, T138)) → U14_GGA(T137, T131, T113, T114, T138, lessB_in_gg(T131, T137))
U14_GGA(T137, T131, T113, T114, T138, lessB_out_gg(T131, T137)) → U15_GGA(T137, T131, T113, T114, T138, insertD_in_gga(s(T137), T114, T138))
U14_GGA(T137, T131, T113, T114, T138, lessB_out_gg(T131, T137)) → INSERTD_IN_GGA(s(T137), T114, T138)
INSERTD_IN_GGA(0, tree(s(T161), T152, T153), tree(s(T161), T162, T153)) → U16_GGA(T161, T152, T153, T162, insertD_in_gga(0, T152, T162))
INSERTD_IN_GGA(s(T173), tree(s(T172), T152, T153), tree(s(T172), T174, T153)) → U17_GGA(T173, T172, T152, T153, T174, pC_in_ggga(T173, T172, T152, T174))
INSERTD_IN_GGA(T192, tree(T188, T189, T190), tree(T188, T189, T193)) → U18_GGA(T192, T188, T189, T190, T193, pE_in_ggga(T188, T192, T190, T193))
INSERTD_IN_GGA(s(T214), tree(0, T203, T204), tree(0, T203, T213)) → U19_GGA(T214, T203, T204, T213, insertD_in_gga(s(T214), T204, T213))
INSERTD_IN_GGA(s(T223), tree(s(T221), T203, T204), tree(s(T221), T203, T224)) → U20_GGA(T223, T221, T203, T204, T224, lessB_in_gg(T221, T223))
INSERTD_IN_GGA(s(T227), tree(s(T221), T203, T204), tree(s(T221), T203, T228)) → U21_GGA(T227, T221, T203, T204, T228, lessB_in_gg(T221, T227))
U21_GGA(T227, T221, T203, T204, T228, lessB_out_gg(T221, T227)) → U22_GGA(T227, T221, T203, T204, T228, insertD_in_gga(s(T227), T204, T228))
U21_GGA(T227, T221, T203, T204, T228, lessB_out_gg(T221, T227)) → INSERTD_IN_GGA(s(T227), T204, T228)
INSERTD_IN_AGA(s(T43), tree(s(T42), T22, T23), tree(s(T42), T44, T23)) → U10_AGA(T43, T42, T22, T23, T44, pC_in_agga(T43, T42, T22, T44))
INSERTD_IN_AGA(s(T43), tree(s(T42), T22, T23), tree(s(T42), T44, T23)) → PC_IN_AGGA(T43, T42, T22, T44)
PC_IN_AGGA(T43, T42, T22, T44) → U3_AGGA(T43, T42, T22, T44, lessA_in_ag(T43, T42))
PC_IN_AGGA(T43, T42, T22, T44) → LESSA_IN_AG(T43, T42)
LESSA_IN_AG(s(T62), s(T61)) → U1_AG(T62, T61, lessA_in_ag(T62, T61))
LESSA_IN_AG(s(T62), s(T61)) → LESSA_IN_AG(T62, T61)
PC_IN_AGGA(T47, T42, T22, T48) → U4_AGGA(T47, T42, T22, T48, lessA_in_ag(T47, T42))
U4_AGGA(T47, T42, T22, T48, lessA_out_ag(T47, T42)) → U5_AGGA(T47, T42, T22, T48, insertD_in_gga(s(T47), T22, T48))
U4_AGGA(T47, T42, T22, T48, lessA_out_ag(T47, T42)) → INSERTD_IN_GGA(s(T47), T22, T48)
INSERTD_IN_AGA(T82, tree(T78, T79, T80), tree(T78, T79, T83)) → U11_AGA(T82, T78, T79, T80, T83, pE_in_gaga(T78, T82, T80, T83))
INSERTD_IN_AGA(T82, tree(T78, T79, T80), tree(T78, T79, T83)) → PE_IN_GAGA(T78, T82, T80, T83)
PE_IN_GAGA(T78, T82, T80, T83) → U6_GAGA(T78, T82, T80, T83, lessB_in_ga(T78, T82))
PE_IN_GAGA(T78, T82, T80, T83) → LESSB_IN_GA(T78, T82)
LESSB_IN_GA(s(T99), s(T101)) → U2_GA(T99, T101, lessB_in_ga(T99, T101))
LESSB_IN_GA(s(T99), s(T101)) → LESSB_IN_GA(T99, T101)
PE_IN_GAGA(T78, T86, T80, T87) → U7_GAGA(T78, T86, T80, T87, lessB_in_ga(T78, T86))
U7_GAGA(T78, T86, T80, T87, lessB_out_ga(T78, T86)) → U8_GAGA(T78, T86, T80, T87, insertD_in_aga(T86, T80, T87))
U7_GAGA(T78, T86, T80, T87, lessB_out_ga(T78, T86)) → INSERTD_IN_AGA(T86, T80, T87)
INSERTD_IN_AGA(s(T124), tree(0, T113, T114), tree(0, T113, T123)) → U12_AGA(T124, T113, T114, T123, insertD_in_aga(s(T124), T114, T123))
INSERTD_IN_AGA(s(T124), tree(0, T113, T114), tree(0, T113, T123)) → INSERTD_IN_AGA(s(T124), T114, T123)
INSERTD_IN_AGA(s(T133), tree(s(T131), T113, T114), tree(s(T131), T113, T134)) → U13_AGA(T133, T131, T113, T114, T134, lessB_in_ga(T131, T133))
INSERTD_IN_AGA(s(T133), tree(s(T131), T113, T114), tree(s(T131), T113, T134)) → LESSB_IN_GA(T131, T133)
INSERTD_IN_AGA(s(T137), tree(s(T131), T113, T114), tree(s(T131), T113, T138)) → U14_AGA(T137, T131, T113, T114, T138, lessB_in_ga(T131, T137))
U14_AGA(T137, T131, T113, T114, T138, lessB_out_ga(T131, T137)) → U15_AGA(T137, T131, T113, T114, T138, insertD_in_aga(s(T137), T114, T138))
U14_AGA(T137, T131, T113, T114, T138, lessB_out_ga(T131, T137)) → INSERTD_IN_AGA(s(T137), T114, T138)
INSERTD_IN_AGA(0, tree(s(T161), T152, T153), tree(s(T161), T162, T153)) → U16_AGA(T161, T152, T153, T162, insertD_in_gga(0, T152, T162))
INSERTD_IN_AGA(s(T173), tree(s(T172), T152, T153), tree(s(T172), T174, T153)) → U17_AGA(T173, T172, T152, T153, T174, pC_in_agga(T173, T172, T152, T174))
INSERTD_IN_AGA(T192, tree(T188, T189, T190), tree(T188, T189, T193)) → U18_AGA(T192, T188, T189, T190, T193, pE_in_gaga(T188, T192, T190, T193))
INSERTD_IN_AGA(s(T214), tree(0, T203, T204), tree(0, T203, T213)) → U19_AGA(T214, T203, T204, T213, insertD_in_aga(s(T214), T204, T213))
INSERTD_IN_AGA(s(T223), tree(s(T221), T203, T204), tree(s(T221), T203, T224)) → U20_AGA(T223, T221, T203, T204, T224, lessB_in_ga(T221, T223))
INSERTD_IN_AGA(s(T227), tree(s(T221), T203, T204), tree(s(T221), T203, T228)) → U21_AGA(T227, T221, T203, T204, T228, lessB_in_ga(T221, T227))
U21_AGA(T227, T221, T203, T204, T228, lessB_out_ga(T221, T227)) → U22_AGA(T227, T221, T203, T204, T228, insertD_in_aga(s(T227), T204, T228))
U21_AGA(T227, T221, T203, T204, T228, lessB_out_ga(T221, T227)) → INSERTD_IN_AGA(s(T227), T204, T228)
insertD_in_aga(T5, void, tree(T5, void, void)) → insertD_out_aga(T5, void, tree(T5, void, void))
insertD_in_aga(T12, tree(T12, T13, T14), tree(T12, T13, T14)) → insertD_out_aga(T12, tree(T12, T13, T14), tree(T12, T13, T14))
insertD_in_aga(0, tree(s(T31), T22, T23), tree(s(T31), T32, T23)) → U9_aga(T31, T22, T23, T32, insertD_in_gga(0, T22, T32))
insertD_in_gga(T5, void, tree(T5, void, void)) → insertD_out_gga(T5, void, tree(T5, void, void))
insertD_in_gga(T12, tree(T12, T13, T14), tree(T12, T13, T14)) → insertD_out_gga(T12, tree(T12, T13, T14), tree(T12, T13, T14))
insertD_in_gga(0, tree(s(T31), T22, T23), tree(s(T31), T32, T23)) → U9_gga(T31, T22, T23, T32, insertD_in_gga(0, T22, T32))
insertD_in_gga(s(T43), tree(s(T42), T22, T23), tree(s(T42), T44, T23)) → U10_gga(T43, T42, T22, T23, T44, pC_in_ggga(T43, T42, T22, T44))
pC_in_ggga(T43, T42, T22, T44) → U3_ggga(T43, T42, T22, T44, lessA_in_gg(T43, T42))
lessA_in_gg(0, s(T55)) → lessA_out_gg(0, s(T55))
lessA_in_gg(s(T62), s(T61)) → U1_gg(T62, T61, lessA_in_gg(T62, T61))
U1_gg(T62, T61, lessA_out_gg(T62, T61)) → lessA_out_gg(s(T62), s(T61))
U3_ggga(T43, T42, T22, T44, lessA_out_gg(T43, T42)) → pC_out_ggga(T43, T42, T22, T44)
pC_in_ggga(T47, T42, T22, T48) → U4_ggga(T47, T42, T22, T48, lessA_in_gg(T47, T42))
U4_ggga(T47, T42, T22, T48, lessA_out_gg(T47, T42)) → U5_ggga(T47, T42, T22, T48, insertD_in_gga(s(T47), T22, T48))
insertD_in_gga(T82, tree(T78, T79, T80), tree(T78, T79, T83)) → U11_gga(T82, T78, T79, T80, T83, pE_in_ggga(T78, T82, T80, T83))
pE_in_ggga(T78, T82, T80, T83) → U6_ggga(T78, T82, T80, T83, lessB_in_gg(T78, T82))
lessB_in_gg(0, s(T94)) → lessB_out_gg(0, s(T94))
lessB_in_gg(s(T99), s(T101)) → U2_gg(T99, T101, lessB_in_gg(T99, T101))
U2_gg(T99, T101, lessB_out_gg(T99, T101)) → lessB_out_gg(s(T99), s(T101))
U6_ggga(T78, T82, T80, T83, lessB_out_gg(T78, T82)) → pE_out_ggga(T78, T82, T80, T83)
pE_in_ggga(T78, T86, T80, T87) → U7_ggga(T78, T86, T80, T87, lessB_in_gg(T78, T86))
U7_ggga(T78, T86, T80, T87, lessB_out_gg(T78, T86)) → U8_ggga(T78, T86, T80, T87, insertD_in_gga(T86, T80, T87))
insertD_in_gga(s(T124), tree(0, T113, T114), tree(0, T113, T123)) → U12_gga(T124, T113, T114, T123, insertD_in_gga(s(T124), T114, T123))
insertD_in_gga(s(T133), tree(s(T131), T113, T114), tree(s(T131), T113, T134)) → U13_gga(T133, T131, T113, T114, T134, lessB_in_gg(T131, T133))
U13_gga(T133, T131, T113, T114, T134, lessB_out_gg(T131, T133)) → insertD_out_gga(s(T133), tree(s(T131), T113, T114), tree(s(T131), T113, T134))
insertD_in_gga(s(T137), tree(s(T131), T113, T114), tree(s(T131), T113, T138)) → U14_gga(T137, T131, T113, T114, T138, lessB_in_gg(T131, T137))
U14_gga(T137, T131, T113, T114, T138, lessB_out_gg(T131, T137)) → U15_gga(T137, T131, T113, T114, T138, insertD_in_gga(s(T137), T114, T138))
insertD_in_gga(0, tree(s(T161), T152, T153), tree(s(T161), T162, T153)) → U16_gga(T161, T152, T153, T162, insertD_in_gga(0, T152, T162))
insertD_in_gga(s(T173), tree(s(T172), T152, T153), tree(s(T172), T174, T153)) → U17_gga(T173, T172, T152, T153, T174, pC_in_ggga(T173, T172, T152, T174))
U17_gga(T173, T172, T152, T153, T174, pC_out_ggga(T173, T172, T152, T174)) → insertD_out_gga(s(T173), tree(s(T172), T152, T153), tree(s(T172), T174, T153))
insertD_in_gga(T192, tree(T188, T189, T190), tree(T188, T189, T193)) → U18_gga(T192, T188, T189, T190, T193, pE_in_ggga(T188, T192, T190, T193))
U18_gga(T192, T188, T189, T190, T193, pE_out_ggga(T188, T192, T190, T193)) → insertD_out_gga(T192, tree(T188, T189, T190), tree(T188, T189, T193))
insertD_in_gga(s(T214), tree(0, T203, T204), tree(0, T203, T213)) → U19_gga(T214, T203, T204, T213, insertD_in_gga(s(T214), T204, T213))
insertD_in_gga(s(T223), tree(s(T221), T203, T204), tree(s(T221), T203, T224)) → U20_gga(T223, T221, T203, T204, T224, lessB_in_gg(T221, T223))
U20_gga(T223, T221, T203, T204, T224, lessB_out_gg(T221, T223)) → insertD_out_gga(s(T223), tree(s(T221), T203, T204), tree(s(T221), T203, T224))
insertD_in_gga(s(T227), tree(s(T221), T203, T204), tree(s(T221), T203, T228)) → U21_gga(T227, T221, T203, T204, T228, lessB_in_gg(T221, T227))
U21_gga(T227, T221, T203, T204, T228, lessB_out_gg(T221, T227)) → U22_gga(T227, T221, T203, T204, T228, insertD_in_gga(s(T227), T204, T228))
U22_gga(T227, T221, T203, T204, T228, insertD_out_gga(s(T227), T204, T228)) → insertD_out_gga(s(T227), tree(s(T221), T203, T204), tree(s(T221), T203, T228))
U19_gga(T214, T203, T204, T213, insertD_out_gga(s(T214), T204, T213)) → insertD_out_gga(s(T214), tree(0, T203, T204), tree(0, T203, T213))
U16_gga(T161, T152, T153, T162, insertD_out_gga(0, T152, T162)) → insertD_out_gga(0, tree(s(T161), T152, T153), tree(s(T161), T162, T153))
U15_gga(T137, T131, T113, T114, T138, insertD_out_gga(s(T137), T114, T138)) → insertD_out_gga(s(T137), tree(s(T131), T113, T114), tree(s(T131), T113, T138))
U12_gga(T124, T113, T114, T123, insertD_out_gga(s(T124), T114, T123)) → insertD_out_gga(s(T124), tree(0, T113, T114), tree(0, T113, T123))
U8_ggga(T78, T86, T80, T87, insertD_out_gga(T86, T80, T87)) → pE_out_ggga(T78, T86, T80, T87)
U11_gga(T82, T78, T79, T80, T83, pE_out_ggga(T78, T82, T80, T83)) → insertD_out_gga(T82, tree(T78, T79, T80), tree(T78, T79, T83))
U5_ggga(T47, T42, T22, T48, insertD_out_gga(s(T47), T22, T48)) → pC_out_ggga(T47, T42, T22, T48)
U10_gga(T43, T42, T22, T23, T44, pC_out_ggga(T43, T42, T22, T44)) → insertD_out_gga(s(T43), tree(s(T42), T22, T23), tree(s(T42), T44, T23))
U9_gga(T31, T22, T23, T32, insertD_out_gga(0, T22, T32)) → insertD_out_gga(0, tree(s(T31), T22, T23), tree(s(T31), T32, T23))
U9_aga(T31, T22, T23, T32, insertD_out_gga(0, T22, T32)) → insertD_out_aga(0, tree(s(T31), T22, T23), tree(s(T31), T32, T23))
insertD_in_aga(s(T43), tree(s(T42), T22, T23), tree(s(T42), T44, T23)) → U10_aga(T43, T42, T22, T23, T44, pC_in_agga(T43, T42, T22, T44))
pC_in_agga(T43, T42, T22, T44) → U3_agga(T43, T42, T22, T44, lessA_in_ag(T43, T42))
lessA_in_ag(0, s(T55)) → lessA_out_ag(0, s(T55))
lessA_in_ag(s(T62), s(T61)) → U1_ag(T62, T61, lessA_in_ag(T62, T61))
U1_ag(T62, T61, lessA_out_ag(T62, T61)) → lessA_out_ag(s(T62), s(T61))
U3_agga(T43, T42, T22, T44, lessA_out_ag(T43, T42)) → pC_out_agga(T43, T42, T22, T44)
pC_in_agga(T47, T42, T22, T48) → U4_agga(T47, T42, T22, T48, lessA_in_ag(T47, T42))
U4_agga(T47, T42, T22, T48, lessA_out_ag(T47, T42)) → U5_agga(T47, T42, T22, T48, insertD_in_gga(s(T47), T22, T48))
U5_agga(T47, T42, T22, T48, insertD_out_gga(s(T47), T22, T48)) → pC_out_agga(T47, T42, T22, T48)
U10_aga(T43, T42, T22, T23, T44, pC_out_agga(T43, T42, T22, T44)) → insertD_out_aga(s(T43), tree(s(T42), T22, T23), tree(s(T42), T44, T23))
insertD_in_aga(T82, tree(T78, T79, T80), tree(T78, T79, T83)) → U11_aga(T82, T78, T79, T80, T83, pE_in_gaga(T78, T82, T80, T83))
pE_in_gaga(T78, T82, T80, T83) → U6_gaga(T78, T82, T80, T83, lessB_in_ga(T78, T82))
lessB_in_ga(0, s(T94)) → lessB_out_ga(0, s(T94))
lessB_in_ga(s(T99), s(T101)) → U2_ga(T99, T101, lessB_in_ga(T99, T101))
U2_ga(T99, T101, lessB_out_ga(T99, T101)) → lessB_out_ga(s(T99), s(T101))
U6_gaga(T78, T82, T80, T83, lessB_out_ga(T78, T82)) → pE_out_gaga(T78, T82, T80, T83)
pE_in_gaga(T78, T86, T80, T87) → U7_gaga(T78, T86, T80, T87, lessB_in_ga(T78, T86))
U7_gaga(T78, T86, T80, T87, lessB_out_ga(T78, T86)) → U8_gaga(T78, T86, T80, T87, insertD_in_aga(T86, T80, T87))
insertD_in_aga(s(T124), tree(0, T113, T114), tree(0, T113, T123)) → U12_aga(T124, T113, T114, T123, insertD_in_aga(s(T124), T114, T123))
insertD_in_aga(s(T133), tree(s(T131), T113, T114), tree(s(T131), T113, T134)) → U13_aga(T133, T131, T113, T114, T134, lessB_in_ga(T131, T133))
U13_aga(T133, T131, T113, T114, T134, lessB_out_ga(T131, T133)) → insertD_out_aga(s(T133), tree(s(T131), T113, T114), tree(s(T131), T113, T134))
insertD_in_aga(s(T137), tree(s(T131), T113, T114), tree(s(T131), T113, T138)) → U14_aga(T137, T131, T113, T114, T138, lessB_in_ga(T131, T137))
U14_aga(T137, T131, T113, T114, T138, lessB_out_ga(T131, T137)) → U15_aga(T137, T131, T113, T114, T138, insertD_in_aga(s(T137), T114, T138))
insertD_in_aga(0, tree(s(T161), T152, T153), tree(s(T161), T162, T153)) → U16_aga(T161, T152, T153, T162, insertD_in_gga(0, T152, T162))
U16_aga(T161, T152, T153, T162, insertD_out_gga(0, T152, T162)) → insertD_out_aga(0, tree(s(T161), T152, T153), tree(s(T161), T162, T153))
insertD_in_aga(s(T173), tree(s(T172), T152, T153), tree(s(T172), T174, T153)) → U17_aga(T173, T172, T152, T153, T174, pC_in_agga(T173, T172, T152, T174))
U17_aga(T173, T172, T152, T153, T174, pC_out_agga(T173, T172, T152, T174)) → insertD_out_aga(s(T173), tree(s(T172), T152, T153), tree(s(T172), T174, T153))
insertD_in_aga(T192, tree(T188, T189, T190), tree(T188, T189, T193)) → U18_aga(T192, T188, T189, T190, T193, pE_in_gaga(T188, T192, T190, T193))
U18_aga(T192, T188, T189, T190, T193, pE_out_gaga(T188, T192, T190, T193)) → insertD_out_aga(T192, tree(T188, T189, T190), tree(T188, T189, T193))
insertD_in_aga(s(T214), tree(0, T203, T204), tree(0, T203, T213)) → U19_aga(T214, T203, T204, T213, insertD_in_aga(s(T214), T204, T213))
insertD_in_aga(s(T223), tree(s(T221), T203, T204), tree(s(T221), T203, T224)) → U20_aga(T223, T221, T203, T204, T224, lessB_in_ga(T221, T223))
U20_aga(T223, T221, T203, T204, T224, lessB_out_ga(T221, T223)) → insertD_out_aga(s(T223), tree(s(T221), T203, T204), tree(s(T221), T203, T224))
insertD_in_aga(s(T227), tree(s(T221), T203, T204), tree(s(T221), T203, T228)) → U21_aga(T227, T221, T203, T204, T228, lessB_in_ga(T221, T227))
U21_aga(T227, T221, T203, T204, T228, lessB_out_ga(T221, T227)) → U22_aga(T227, T221, T203, T204, T228, insertD_in_aga(s(T227), T204, T228))
U22_aga(T227, T221, T203, T204, T228, insertD_out_aga(s(T227), T204, T228)) → insertD_out_aga(s(T227), tree(s(T221), T203, T204), tree(s(T221), T203, T228))
U19_aga(T214, T203, T204, T213, insertD_out_aga(s(T214), T204, T213)) → insertD_out_aga(s(T214), tree(0, T203, T204), tree(0, T203, T213))
U15_aga(T137, T131, T113, T114, T138, insertD_out_aga(s(T137), T114, T138)) → insertD_out_aga(s(T137), tree(s(T131), T113, T114), tree(s(T131), T113, T138))
U12_aga(T124, T113, T114, T123, insertD_out_aga(s(T124), T114, T123)) → insertD_out_aga(s(T124), tree(0, T113, T114), tree(0, T113, T123))
U8_gaga(T78, T86, T80, T87, insertD_out_aga(T86, T80, T87)) → pE_out_gaga(T78, T86, T80, T87)
U11_aga(T82, T78, T79, T80, T83, pE_out_gaga(T78, T82, T80, T83)) → insertD_out_aga(T82, tree(T78, T79, T80), tree(T78, T79, T83))
LESSB_IN_GA(s(T99), s(T101)) → LESSB_IN_GA(T99, T101)
insertD_in_aga(T5, void, tree(T5, void, void)) → insertD_out_aga(T5, void, tree(T5, void, void))
insertD_in_aga(T12, tree(T12, T13, T14), tree(T12, T13, T14)) → insertD_out_aga(T12, tree(T12, T13, T14), tree(T12, T13, T14))
insertD_in_aga(0, tree(s(T31), T22, T23), tree(s(T31), T32, T23)) → U9_aga(T31, T22, T23, T32, insertD_in_gga(0, T22, T32))
insertD_in_gga(T5, void, tree(T5, void, void)) → insertD_out_gga(T5, void, tree(T5, void, void))
insertD_in_gga(T12, tree(T12, T13, T14), tree(T12, T13, T14)) → insertD_out_gga(T12, tree(T12, T13, T14), tree(T12, T13, T14))
insertD_in_gga(0, tree(s(T31), T22, T23), tree(s(T31), T32, T23)) → U9_gga(T31, T22, T23, T32, insertD_in_gga(0, T22, T32))
insertD_in_gga(s(T43), tree(s(T42), T22, T23), tree(s(T42), T44, T23)) → U10_gga(T43, T42, T22, T23, T44, pC_in_ggga(T43, T42, T22, T44))
pC_in_ggga(T43, T42, T22, T44) → U3_ggga(T43, T42, T22, T44, lessA_in_gg(T43, T42))
lessA_in_gg(0, s(T55)) → lessA_out_gg(0, s(T55))
lessA_in_gg(s(T62), s(T61)) → U1_gg(T62, T61, lessA_in_gg(T62, T61))
U1_gg(T62, T61, lessA_out_gg(T62, T61)) → lessA_out_gg(s(T62), s(T61))
U3_ggga(T43, T42, T22, T44, lessA_out_gg(T43, T42)) → pC_out_ggga(T43, T42, T22, T44)
pC_in_ggga(T47, T42, T22, T48) → U4_ggga(T47, T42, T22, T48, lessA_in_gg(T47, T42))
U4_ggga(T47, T42, T22, T48, lessA_out_gg(T47, T42)) → U5_ggga(T47, T42, T22, T48, insertD_in_gga(s(T47), T22, T48))
insertD_in_gga(T82, tree(T78, T79, T80), tree(T78, T79, T83)) → U11_gga(T82, T78, T79, T80, T83, pE_in_ggga(T78, T82, T80, T83))
pE_in_ggga(T78, T82, T80, T83) → U6_ggga(T78, T82, T80, T83, lessB_in_gg(T78, T82))
lessB_in_gg(0, s(T94)) → lessB_out_gg(0, s(T94))
lessB_in_gg(s(T99), s(T101)) → U2_gg(T99, T101, lessB_in_gg(T99, T101))
U2_gg(T99, T101, lessB_out_gg(T99, T101)) → lessB_out_gg(s(T99), s(T101))
U6_ggga(T78, T82, T80, T83, lessB_out_gg(T78, T82)) → pE_out_ggga(T78, T82, T80, T83)
pE_in_ggga(T78, T86, T80, T87) → U7_ggga(T78, T86, T80, T87, lessB_in_gg(T78, T86))
U7_ggga(T78, T86, T80, T87, lessB_out_gg(T78, T86)) → U8_ggga(T78, T86, T80, T87, insertD_in_gga(T86, T80, T87))
insertD_in_gga(s(T124), tree(0, T113, T114), tree(0, T113, T123)) → U12_gga(T124, T113, T114, T123, insertD_in_gga(s(T124), T114, T123))
insertD_in_gga(s(T133), tree(s(T131), T113, T114), tree(s(T131), T113, T134)) → U13_gga(T133, T131, T113, T114, T134, lessB_in_gg(T131, T133))
U13_gga(T133, T131, T113, T114, T134, lessB_out_gg(T131, T133)) → insertD_out_gga(s(T133), tree(s(T131), T113, T114), tree(s(T131), T113, T134))
insertD_in_gga(s(T137), tree(s(T131), T113, T114), tree(s(T131), T113, T138)) → U14_gga(T137, T131, T113, T114, T138, lessB_in_gg(T131, T137))
U14_gga(T137, T131, T113, T114, T138, lessB_out_gg(T131, T137)) → U15_gga(T137, T131, T113, T114, T138, insertD_in_gga(s(T137), T114, T138))
insertD_in_gga(0, tree(s(T161), T152, T153), tree(s(T161), T162, T153)) → U16_gga(T161, T152, T153, T162, insertD_in_gga(0, T152, T162))
insertD_in_gga(s(T173), tree(s(T172), T152, T153), tree(s(T172), T174, T153)) → U17_gga(T173, T172, T152, T153, T174, pC_in_ggga(T173, T172, T152, T174))
U17_gga(T173, T172, T152, T153, T174, pC_out_ggga(T173, T172, T152, T174)) → insertD_out_gga(s(T173), tree(s(T172), T152, T153), tree(s(T172), T174, T153))
insertD_in_gga(T192, tree(T188, T189, T190), tree(T188, T189, T193)) → U18_gga(T192, T188, T189, T190, T193, pE_in_ggga(T188, T192, T190, T193))
U18_gga(T192, T188, T189, T190, T193, pE_out_ggga(T188, T192, T190, T193)) → insertD_out_gga(T192, tree(T188, T189, T190), tree(T188, T189, T193))
insertD_in_gga(s(T214), tree(0, T203, T204), tree(0, T203, T213)) → U19_gga(T214, T203, T204, T213, insertD_in_gga(s(T214), T204, T213))
insertD_in_gga(s(T223), tree(s(T221), T203, T204), tree(s(T221), T203, T224)) → U20_gga(T223, T221, T203, T204, T224, lessB_in_gg(T221, T223))
U20_gga(T223, T221, T203, T204, T224, lessB_out_gg(T221, T223)) → insertD_out_gga(s(T223), tree(s(T221), T203, T204), tree(s(T221), T203, T224))
insertD_in_gga(s(T227), tree(s(T221), T203, T204), tree(s(T221), T203, T228)) → U21_gga(T227, T221, T203, T204, T228, lessB_in_gg(T221, T227))
U21_gga(T227, T221, T203, T204, T228, lessB_out_gg(T221, T227)) → U22_gga(T227, T221, T203, T204, T228, insertD_in_gga(s(T227), T204, T228))
U22_gga(T227, T221, T203, T204, T228, insertD_out_gga(s(T227), T204, T228)) → insertD_out_gga(s(T227), tree(s(T221), T203, T204), tree(s(T221), T203, T228))
U19_gga(T214, T203, T204, T213, insertD_out_gga(s(T214), T204, T213)) → insertD_out_gga(s(T214), tree(0, T203, T204), tree(0, T203, T213))
U16_gga(T161, T152, T153, T162, insertD_out_gga(0, T152, T162)) → insertD_out_gga(0, tree(s(T161), T152, T153), tree(s(T161), T162, T153))
U15_gga(T137, T131, T113, T114, T138, insertD_out_gga(s(T137), T114, T138)) → insertD_out_gga(s(T137), tree(s(T131), T113, T114), tree(s(T131), T113, T138))
U12_gga(T124, T113, T114, T123, insertD_out_gga(s(T124), T114, T123)) → insertD_out_gga(s(T124), tree(0, T113, T114), tree(0, T113, T123))
U8_ggga(T78, T86, T80, T87, insertD_out_gga(T86, T80, T87)) → pE_out_ggga(T78, T86, T80, T87)
U11_gga(T82, T78, T79, T80, T83, pE_out_ggga(T78, T82, T80, T83)) → insertD_out_gga(T82, tree(T78, T79, T80), tree(T78, T79, T83))
U5_ggga(T47, T42, T22, T48, insertD_out_gga(s(T47), T22, T48)) → pC_out_ggga(T47, T42, T22, T48)
U10_gga(T43, T42, T22, T23, T44, pC_out_ggga(T43, T42, T22, T44)) → insertD_out_gga(s(T43), tree(s(T42), T22, T23), tree(s(T42), T44, T23))
U9_gga(T31, T22, T23, T32, insertD_out_gga(0, T22, T32)) → insertD_out_gga(0, tree(s(T31), T22, T23), tree(s(T31), T32, T23))
U9_aga(T31, T22, T23, T32, insertD_out_gga(0, T22, T32)) → insertD_out_aga(0, tree(s(T31), T22, T23), tree(s(T31), T32, T23))
insertD_in_aga(s(T43), tree(s(T42), T22, T23), tree(s(T42), T44, T23)) → U10_aga(T43, T42, T22, T23, T44, pC_in_agga(T43, T42, T22, T44))
pC_in_agga(T43, T42, T22, T44) → U3_agga(T43, T42, T22, T44, lessA_in_ag(T43, T42))
lessA_in_ag(0, s(T55)) → lessA_out_ag(0, s(T55))
lessA_in_ag(s(T62), s(T61)) → U1_ag(T62, T61, lessA_in_ag(T62, T61))
U1_ag(T62, T61, lessA_out_ag(T62, T61)) → lessA_out_ag(s(T62), s(T61))
U3_agga(T43, T42, T22, T44, lessA_out_ag(T43, T42)) → pC_out_agga(T43, T42, T22, T44)
pC_in_agga(T47, T42, T22, T48) → U4_agga(T47, T42, T22, T48, lessA_in_ag(T47, T42))
U4_agga(T47, T42, T22, T48, lessA_out_ag(T47, T42)) → U5_agga(T47, T42, T22, T48, insertD_in_gga(s(T47), T22, T48))
U5_agga(T47, T42, T22, T48, insertD_out_gga(s(T47), T22, T48)) → pC_out_agga(T47, T42, T22, T48)
U10_aga(T43, T42, T22, T23, T44, pC_out_agga(T43, T42, T22, T44)) → insertD_out_aga(s(T43), tree(s(T42), T22, T23), tree(s(T42), T44, T23))
insertD_in_aga(T82, tree(T78, T79, T80), tree(T78, T79, T83)) → U11_aga(T82, T78, T79, T80, T83, pE_in_gaga(T78, T82, T80, T83))
pE_in_gaga(T78, T82, T80, T83) → U6_gaga(T78, T82, T80, T83, lessB_in_ga(T78, T82))
lessB_in_ga(0, s(T94)) → lessB_out_ga(0, s(T94))
lessB_in_ga(s(T99), s(T101)) → U2_ga(T99, T101, lessB_in_ga(T99, T101))
U2_ga(T99, T101, lessB_out_ga(T99, T101)) → lessB_out_ga(s(T99), s(T101))
U6_gaga(T78, T82, T80, T83, lessB_out_ga(T78, T82)) → pE_out_gaga(T78, T82, T80, T83)
pE_in_gaga(T78, T86, T80, T87) → U7_gaga(T78, T86, T80, T87, lessB_in_ga(T78, T86))
U7_gaga(T78, T86, T80, T87, lessB_out_ga(T78, T86)) → U8_gaga(T78, T86, T80, T87, insertD_in_aga(T86, T80, T87))
insertD_in_aga(s(T124), tree(0, T113, T114), tree(0, T113, T123)) → U12_aga(T124, T113, T114, T123, insertD_in_aga(s(T124), T114, T123))
insertD_in_aga(s(T133), tree(s(T131), T113, T114), tree(s(T131), T113, T134)) → U13_aga(T133, T131, T113, T114, T134, lessB_in_ga(T131, T133))
U13_aga(T133, T131, T113, T114, T134, lessB_out_ga(T131, T133)) → insertD_out_aga(s(T133), tree(s(T131), T113, T114), tree(s(T131), T113, T134))
insertD_in_aga(s(T137), tree(s(T131), T113, T114), tree(s(T131), T113, T138)) → U14_aga(T137, T131, T113, T114, T138, lessB_in_ga(T131, T137))
U14_aga(T137, T131, T113, T114, T138, lessB_out_ga(T131, T137)) → U15_aga(T137, T131, T113, T114, T138, insertD_in_aga(s(T137), T114, T138))
insertD_in_aga(0, tree(s(T161), T152, T153), tree(s(T161), T162, T153)) → U16_aga(T161, T152, T153, T162, insertD_in_gga(0, T152, T162))
U16_aga(T161, T152, T153, T162, insertD_out_gga(0, T152, T162)) → insertD_out_aga(0, tree(s(T161), T152, T153), tree(s(T161), T162, T153))
insertD_in_aga(s(T173), tree(s(T172), T152, T153), tree(s(T172), T174, T153)) → U17_aga(T173, T172, T152, T153, T174, pC_in_agga(T173, T172, T152, T174))
U17_aga(T173, T172, T152, T153, T174, pC_out_agga(T173, T172, T152, T174)) → insertD_out_aga(s(T173), tree(s(T172), T152, T153), tree(s(T172), T174, T153))
insertD_in_aga(T192, tree(T188, T189, T190), tree(T188, T189, T193)) → U18_aga(T192, T188, T189, T190, T193, pE_in_gaga(T188, T192, T190, T193))
U18_aga(T192, T188, T189, T190, T193, pE_out_gaga(T188, T192, T190, T193)) → insertD_out_aga(T192, tree(T188, T189, T190), tree(T188, T189, T193))
insertD_in_aga(s(T214), tree(0, T203, T204), tree(0, T203, T213)) → U19_aga(T214, T203, T204, T213, insertD_in_aga(s(T214), T204, T213))
insertD_in_aga(s(T223), tree(s(T221), T203, T204), tree(s(T221), T203, T224)) → U20_aga(T223, T221, T203, T204, T224, lessB_in_ga(T221, T223))
U20_aga(T223, T221, T203, T204, T224, lessB_out_ga(T221, T223)) → insertD_out_aga(s(T223), tree(s(T221), T203, T204), tree(s(T221), T203, T224))
insertD_in_aga(s(T227), tree(s(T221), T203, T204), tree(s(T221), T203, T228)) → U21_aga(T227, T221, T203, T204, T228, lessB_in_ga(T221, T227))
U21_aga(T227, T221, T203, T204, T228, lessB_out_ga(T221, T227)) → U22_aga(T227, T221, T203, T204, T228, insertD_in_aga(s(T227), T204, T228))
U22_aga(T227, T221, T203, T204, T228, insertD_out_aga(s(T227), T204, T228)) → insertD_out_aga(s(T227), tree(s(T221), T203, T204), tree(s(T221), T203, T228))
U19_aga(T214, T203, T204, T213, insertD_out_aga(s(T214), T204, T213)) → insertD_out_aga(s(T214), tree(0, T203, T204), tree(0, T203, T213))
U15_aga(T137, T131, T113, T114, T138, insertD_out_aga(s(T137), T114, T138)) → insertD_out_aga(s(T137), tree(s(T131), T113, T114), tree(s(T131), T113, T138))
U12_aga(T124, T113, T114, T123, insertD_out_aga(s(T124), T114, T123)) → insertD_out_aga(s(T124), tree(0, T113, T114), tree(0, T113, T123))
U8_gaga(T78, T86, T80, T87, insertD_out_aga(T86, T80, T87)) → pE_out_gaga(T78, T86, T80, T87)
U11_aga(T82, T78, T79, T80, T83, pE_out_gaga(T78, T82, T80, T83)) → insertD_out_aga(T82, tree(T78, T79, T80), tree(T78, T79, T83))
LESSB_IN_GA(s(T99), s(T101)) → LESSB_IN_GA(T99, T101)
LESSB_IN_GA(s(T99)) → LESSB_IN_GA(T99)
From the DPs we obtained the following set of size-change graphs:
LESSA_IN_AG(s(T62), s(T61)) → LESSA_IN_AG(T62, T61)
insertD_in_aga(T5, void, tree(T5, void, void)) → insertD_out_aga(T5, void, tree(T5, void, void))
insertD_in_aga(T12, tree(T12, T13, T14), tree(T12, T13, T14)) → insertD_out_aga(T12, tree(T12, T13, T14), tree(T12, T13, T14))
insertD_in_aga(0, tree(s(T31), T22, T23), tree(s(T31), T32, T23)) → U9_aga(T31, T22, T23, T32, insertD_in_gga(0, T22, T32))
insertD_in_gga(T5, void, tree(T5, void, void)) → insertD_out_gga(T5, void, tree(T5, void, void))
insertD_in_gga(T12, tree(T12, T13, T14), tree(T12, T13, T14)) → insertD_out_gga(T12, tree(T12, T13, T14), tree(T12, T13, T14))
insertD_in_gga(0, tree(s(T31), T22, T23), tree(s(T31), T32, T23)) → U9_gga(T31, T22, T23, T32, insertD_in_gga(0, T22, T32))
insertD_in_gga(s(T43), tree(s(T42), T22, T23), tree(s(T42), T44, T23)) → U10_gga(T43, T42, T22, T23, T44, pC_in_ggga(T43, T42, T22, T44))
pC_in_ggga(T43, T42, T22, T44) → U3_ggga(T43, T42, T22, T44, lessA_in_gg(T43, T42))
lessA_in_gg(0, s(T55)) → lessA_out_gg(0, s(T55))
lessA_in_gg(s(T62), s(T61)) → U1_gg(T62, T61, lessA_in_gg(T62, T61))
U1_gg(T62, T61, lessA_out_gg(T62, T61)) → lessA_out_gg(s(T62), s(T61))
U3_ggga(T43, T42, T22, T44, lessA_out_gg(T43, T42)) → pC_out_ggga(T43, T42, T22, T44)
pC_in_ggga(T47, T42, T22, T48) → U4_ggga(T47, T42, T22, T48, lessA_in_gg(T47, T42))
U4_ggga(T47, T42, T22, T48, lessA_out_gg(T47, T42)) → U5_ggga(T47, T42, T22, T48, insertD_in_gga(s(T47), T22, T48))
insertD_in_gga(T82, tree(T78, T79, T80), tree(T78, T79, T83)) → U11_gga(T82, T78, T79, T80, T83, pE_in_ggga(T78, T82, T80, T83))
pE_in_ggga(T78, T82, T80, T83) → U6_ggga(T78, T82, T80, T83, lessB_in_gg(T78, T82))
lessB_in_gg(0, s(T94)) → lessB_out_gg(0, s(T94))
lessB_in_gg(s(T99), s(T101)) → U2_gg(T99, T101, lessB_in_gg(T99, T101))
U2_gg(T99, T101, lessB_out_gg(T99, T101)) → lessB_out_gg(s(T99), s(T101))
U6_ggga(T78, T82, T80, T83, lessB_out_gg(T78, T82)) → pE_out_ggga(T78, T82, T80, T83)
pE_in_ggga(T78, T86, T80, T87) → U7_ggga(T78, T86, T80, T87, lessB_in_gg(T78, T86))
U7_ggga(T78, T86, T80, T87, lessB_out_gg(T78, T86)) → U8_ggga(T78, T86, T80, T87, insertD_in_gga(T86, T80, T87))
insertD_in_gga(s(T124), tree(0, T113, T114), tree(0, T113, T123)) → U12_gga(T124, T113, T114, T123, insertD_in_gga(s(T124), T114, T123))
insertD_in_gga(s(T133), tree(s(T131), T113, T114), tree(s(T131), T113, T134)) → U13_gga(T133, T131, T113, T114, T134, lessB_in_gg(T131, T133))
U13_gga(T133, T131, T113, T114, T134, lessB_out_gg(T131, T133)) → insertD_out_gga(s(T133), tree(s(T131), T113, T114), tree(s(T131), T113, T134))
insertD_in_gga(s(T137), tree(s(T131), T113, T114), tree(s(T131), T113, T138)) → U14_gga(T137, T131, T113, T114, T138, lessB_in_gg(T131, T137))
U14_gga(T137, T131, T113, T114, T138, lessB_out_gg(T131, T137)) → U15_gga(T137, T131, T113, T114, T138, insertD_in_gga(s(T137), T114, T138))
insertD_in_gga(0, tree(s(T161), T152, T153), tree(s(T161), T162, T153)) → U16_gga(T161, T152, T153, T162, insertD_in_gga(0, T152, T162))
insertD_in_gga(s(T173), tree(s(T172), T152, T153), tree(s(T172), T174, T153)) → U17_gga(T173, T172, T152, T153, T174, pC_in_ggga(T173, T172, T152, T174))
U17_gga(T173, T172, T152, T153, T174, pC_out_ggga(T173, T172, T152, T174)) → insertD_out_gga(s(T173), tree(s(T172), T152, T153), tree(s(T172), T174, T153))
insertD_in_gga(T192, tree(T188, T189, T190), tree(T188, T189, T193)) → U18_gga(T192, T188, T189, T190, T193, pE_in_ggga(T188, T192, T190, T193))
U18_gga(T192, T188, T189, T190, T193, pE_out_ggga(T188, T192, T190, T193)) → insertD_out_gga(T192, tree(T188, T189, T190), tree(T188, T189, T193))
insertD_in_gga(s(T214), tree(0, T203, T204), tree(0, T203, T213)) → U19_gga(T214, T203, T204, T213, insertD_in_gga(s(T214), T204, T213))
insertD_in_gga(s(T223), tree(s(T221), T203, T204), tree(s(T221), T203, T224)) → U20_gga(T223, T221, T203, T204, T224, lessB_in_gg(T221, T223))
U20_gga(T223, T221, T203, T204, T224, lessB_out_gg(T221, T223)) → insertD_out_gga(s(T223), tree(s(T221), T203, T204), tree(s(T221), T203, T224))
insertD_in_gga(s(T227), tree(s(T221), T203, T204), tree(s(T221), T203, T228)) → U21_gga(T227, T221, T203, T204, T228, lessB_in_gg(T221, T227))
U21_gga(T227, T221, T203, T204, T228, lessB_out_gg(T221, T227)) → U22_gga(T227, T221, T203, T204, T228, insertD_in_gga(s(T227), T204, T228))
U22_gga(T227, T221, T203, T204, T228, insertD_out_gga(s(T227), T204, T228)) → insertD_out_gga(s(T227), tree(s(T221), T203, T204), tree(s(T221), T203, T228))
U19_gga(T214, T203, T204, T213, insertD_out_gga(s(T214), T204, T213)) → insertD_out_gga(s(T214), tree(0, T203, T204), tree(0, T203, T213))
U16_gga(T161, T152, T153, T162, insertD_out_gga(0, T152, T162)) → insertD_out_gga(0, tree(s(T161), T152, T153), tree(s(T161), T162, T153))
U15_gga(T137, T131, T113, T114, T138, insertD_out_gga(s(T137), T114, T138)) → insertD_out_gga(s(T137), tree(s(T131), T113, T114), tree(s(T131), T113, T138))
U12_gga(T124, T113, T114, T123, insertD_out_gga(s(T124), T114, T123)) → insertD_out_gga(s(T124), tree(0, T113, T114), tree(0, T113, T123))
U8_ggga(T78, T86, T80, T87, insertD_out_gga(T86, T80, T87)) → pE_out_ggga(T78, T86, T80, T87)
U11_gga(T82, T78, T79, T80, T83, pE_out_ggga(T78, T82, T80, T83)) → insertD_out_gga(T82, tree(T78, T79, T80), tree(T78, T79, T83))
U5_ggga(T47, T42, T22, T48, insertD_out_gga(s(T47), T22, T48)) → pC_out_ggga(T47, T42, T22, T48)
U10_gga(T43, T42, T22, T23, T44, pC_out_ggga(T43, T42, T22, T44)) → insertD_out_gga(s(T43), tree(s(T42), T22, T23), tree(s(T42), T44, T23))
U9_gga(T31, T22, T23, T32, insertD_out_gga(0, T22, T32)) → insertD_out_gga(0, tree(s(T31), T22, T23), tree(s(T31), T32, T23))
U9_aga(T31, T22, T23, T32, insertD_out_gga(0, T22, T32)) → insertD_out_aga(0, tree(s(T31), T22, T23), tree(s(T31), T32, T23))
insertD_in_aga(s(T43), tree(s(T42), T22, T23), tree(s(T42), T44, T23)) → U10_aga(T43, T42, T22, T23, T44, pC_in_agga(T43, T42, T22, T44))
pC_in_agga(T43, T42, T22, T44) → U3_agga(T43, T42, T22, T44, lessA_in_ag(T43, T42))
lessA_in_ag(0, s(T55)) → lessA_out_ag(0, s(T55))
lessA_in_ag(s(T62), s(T61)) → U1_ag(T62, T61, lessA_in_ag(T62, T61))
U1_ag(T62, T61, lessA_out_ag(T62, T61)) → lessA_out_ag(s(T62), s(T61))
U3_agga(T43, T42, T22, T44, lessA_out_ag(T43, T42)) → pC_out_agga(T43, T42, T22, T44)
pC_in_agga(T47, T42, T22, T48) → U4_agga(T47, T42, T22, T48, lessA_in_ag(T47, T42))
U4_agga(T47, T42, T22, T48, lessA_out_ag(T47, T42)) → U5_agga(T47, T42, T22, T48, insertD_in_gga(s(T47), T22, T48))
U5_agga(T47, T42, T22, T48, insertD_out_gga(s(T47), T22, T48)) → pC_out_agga(T47, T42, T22, T48)
U10_aga(T43, T42, T22, T23, T44, pC_out_agga(T43, T42, T22, T44)) → insertD_out_aga(s(T43), tree(s(T42), T22, T23), tree(s(T42), T44, T23))
insertD_in_aga(T82, tree(T78, T79, T80), tree(T78, T79, T83)) → U11_aga(T82, T78, T79, T80, T83, pE_in_gaga(T78, T82, T80, T83))
pE_in_gaga(T78, T82, T80, T83) → U6_gaga(T78, T82, T80, T83, lessB_in_ga(T78, T82))
lessB_in_ga(0, s(T94)) → lessB_out_ga(0, s(T94))
lessB_in_ga(s(T99), s(T101)) → U2_ga(T99, T101, lessB_in_ga(T99, T101))
U2_ga(T99, T101, lessB_out_ga(T99, T101)) → lessB_out_ga(s(T99), s(T101))
U6_gaga(T78, T82, T80, T83, lessB_out_ga(T78, T82)) → pE_out_gaga(T78, T82, T80, T83)
pE_in_gaga(T78, T86, T80, T87) → U7_gaga(T78, T86, T80, T87, lessB_in_ga(T78, T86))
U7_gaga(T78, T86, T80, T87, lessB_out_ga(T78, T86)) → U8_gaga(T78, T86, T80, T87, insertD_in_aga(T86, T80, T87))
insertD_in_aga(s(T124), tree(0, T113, T114), tree(0, T113, T123)) → U12_aga(T124, T113, T114, T123, insertD_in_aga(s(T124), T114, T123))
insertD_in_aga(s(T133), tree(s(T131), T113, T114), tree(s(T131), T113, T134)) → U13_aga(T133, T131, T113, T114, T134, lessB_in_ga(T131, T133))
U13_aga(T133, T131, T113, T114, T134, lessB_out_ga(T131, T133)) → insertD_out_aga(s(T133), tree(s(T131), T113, T114), tree(s(T131), T113, T134))
insertD_in_aga(s(T137), tree(s(T131), T113, T114), tree(s(T131), T113, T138)) → U14_aga(T137, T131, T113, T114, T138, lessB_in_ga(T131, T137))
U14_aga(T137, T131, T113, T114, T138, lessB_out_ga(T131, T137)) → U15_aga(T137, T131, T113, T114, T138, insertD_in_aga(s(T137), T114, T138))
insertD_in_aga(0, tree(s(T161), T152, T153), tree(s(T161), T162, T153)) → U16_aga(T161, T152, T153, T162, insertD_in_gga(0, T152, T162))
U16_aga(T161, T152, T153, T162, insertD_out_gga(0, T152, T162)) → insertD_out_aga(0, tree(s(T161), T152, T153), tree(s(T161), T162, T153))
insertD_in_aga(s(T173), tree(s(T172), T152, T153), tree(s(T172), T174, T153)) → U17_aga(T173, T172, T152, T153, T174, pC_in_agga(T173, T172, T152, T174))
U17_aga(T173, T172, T152, T153, T174, pC_out_agga(T173, T172, T152, T174)) → insertD_out_aga(s(T173), tree(s(T172), T152, T153), tree(s(T172), T174, T153))
insertD_in_aga(T192, tree(T188, T189, T190), tree(T188, T189, T193)) → U18_aga(T192, T188, T189, T190, T193, pE_in_gaga(T188, T192, T190, T193))
U18_aga(T192, T188, T189, T190, T193, pE_out_gaga(T188, T192, T190, T193)) → insertD_out_aga(T192, tree(T188, T189, T190), tree(T188, T189, T193))
insertD_in_aga(s(T214), tree(0, T203, T204), tree(0, T203, T213)) → U19_aga(T214, T203, T204, T213, insertD_in_aga(s(T214), T204, T213))
insertD_in_aga(s(T223), tree(s(T221), T203, T204), tree(s(T221), T203, T224)) → U20_aga(T223, T221, T203, T204, T224, lessB_in_ga(T221, T223))
U20_aga(T223, T221, T203, T204, T224, lessB_out_ga(T221, T223)) → insertD_out_aga(s(T223), tree(s(T221), T203, T204), tree(s(T221), T203, T224))
insertD_in_aga(s(T227), tree(s(T221), T203, T204), tree(s(T221), T203, T228)) → U21_aga(T227, T221, T203, T204, T228, lessB_in_ga(T221, T227))
U21_aga(T227, T221, T203, T204, T228, lessB_out_ga(T221, T227)) → U22_aga(T227, T221, T203, T204, T228, insertD_in_aga(s(T227), T204, T228))
U22_aga(T227, T221, T203, T204, T228, insertD_out_aga(s(T227), T204, T228)) → insertD_out_aga(s(T227), tree(s(T221), T203, T204), tree(s(T221), T203, T228))
U19_aga(T214, T203, T204, T213, insertD_out_aga(s(T214), T204, T213)) → insertD_out_aga(s(T214), tree(0, T203, T204), tree(0, T203, T213))
U15_aga(T137, T131, T113, T114, T138, insertD_out_aga(s(T137), T114, T138)) → insertD_out_aga(s(T137), tree(s(T131), T113, T114), tree(s(T131), T113, T138))
U12_aga(T124, T113, T114, T123, insertD_out_aga(s(T124), T114, T123)) → insertD_out_aga(s(T124), tree(0, T113, T114), tree(0, T113, T123))
U8_gaga(T78, T86, T80, T87, insertD_out_aga(T86, T80, T87)) → pE_out_gaga(T78, T86, T80, T87)
U11_aga(T82, T78, T79, T80, T83, pE_out_gaga(T78, T82, T80, T83)) → insertD_out_aga(T82, tree(T78, T79, T80), tree(T78, T79, T83))
LESSA_IN_AG(s(T62), s(T61)) → LESSA_IN_AG(T62, T61)
LESSA_IN_AG(s(T61)) → LESSA_IN_AG(T61)
From the DPs we obtained the following set of size-change graphs:
LESSB_IN_GG(s(T99), s(T101)) → LESSB_IN_GG(T99, T101)
insertD_in_aga(T5, void, tree(T5, void, void)) → insertD_out_aga(T5, void, tree(T5, void, void))
insertD_in_aga(T12, tree(T12, T13, T14), tree(T12, T13, T14)) → insertD_out_aga(T12, tree(T12, T13, T14), tree(T12, T13, T14))
insertD_in_aga(0, tree(s(T31), T22, T23), tree(s(T31), T32, T23)) → U9_aga(T31, T22, T23, T32, insertD_in_gga(0, T22, T32))
insertD_in_gga(T5, void, tree(T5, void, void)) → insertD_out_gga(T5, void, tree(T5, void, void))
insertD_in_gga(T12, tree(T12, T13, T14), tree(T12, T13, T14)) → insertD_out_gga(T12, tree(T12, T13, T14), tree(T12, T13, T14))
insertD_in_gga(0, tree(s(T31), T22, T23), tree(s(T31), T32, T23)) → U9_gga(T31, T22, T23, T32, insertD_in_gga(0, T22, T32))
insertD_in_gga(s(T43), tree(s(T42), T22, T23), tree(s(T42), T44, T23)) → U10_gga(T43, T42, T22, T23, T44, pC_in_ggga(T43, T42, T22, T44))
pC_in_ggga(T43, T42, T22, T44) → U3_ggga(T43, T42, T22, T44, lessA_in_gg(T43, T42))
lessA_in_gg(0, s(T55)) → lessA_out_gg(0, s(T55))
lessA_in_gg(s(T62), s(T61)) → U1_gg(T62, T61, lessA_in_gg(T62, T61))
U1_gg(T62, T61, lessA_out_gg(T62, T61)) → lessA_out_gg(s(T62), s(T61))
U3_ggga(T43, T42, T22, T44, lessA_out_gg(T43, T42)) → pC_out_ggga(T43, T42, T22, T44)
pC_in_ggga(T47, T42, T22, T48) → U4_ggga(T47, T42, T22, T48, lessA_in_gg(T47, T42))
U4_ggga(T47, T42, T22, T48, lessA_out_gg(T47, T42)) → U5_ggga(T47, T42, T22, T48, insertD_in_gga(s(T47), T22, T48))
insertD_in_gga(T82, tree(T78, T79, T80), tree(T78, T79, T83)) → U11_gga(T82, T78, T79, T80, T83, pE_in_ggga(T78, T82, T80, T83))
pE_in_ggga(T78, T82, T80, T83) → U6_ggga(T78, T82, T80, T83, lessB_in_gg(T78, T82))
lessB_in_gg(0, s(T94)) → lessB_out_gg(0, s(T94))
lessB_in_gg(s(T99), s(T101)) → U2_gg(T99, T101, lessB_in_gg(T99, T101))
U2_gg(T99, T101, lessB_out_gg(T99, T101)) → lessB_out_gg(s(T99), s(T101))
U6_ggga(T78, T82, T80, T83, lessB_out_gg(T78, T82)) → pE_out_ggga(T78, T82, T80, T83)
pE_in_ggga(T78, T86, T80, T87) → U7_ggga(T78, T86, T80, T87, lessB_in_gg(T78, T86))
U7_ggga(T78, T86, T80, T87, lessB_out_gg(T78, T86)) → U8_ggga(T78, T86, T80, T87, insertD_in_gga(T86, T80, T87))
insertD_in_gga(s(T124), tree(0, T113, T114), tree(0, T113, T123)) → U12_gga(T124, T113, T114, T123, insertD_in_gga(s(T124), T114, T123))
insertD_in_gga(s(T133), tree(s(T131), T113, T114), tree(s(T131), T113, T134)) → U13_gga(T133, T131, T113, T114, T134, lessB_in_gg(T131, T133))
U13_gga(T133, T131, T113, T114, T134, lessB_out_gg(T131, T133)) → insertD_out_gga(s(T133), tree(s(T131), T113, T114), tree(s(T131), T113, T134))
insertD_in_gga(s(T137), tree(s(T131), T113, T114), tree(s(T131), T113, T138)) → U14_gga(T137, T131, T113, T114, T138, lessB_in_gg(T131, T137))
U14_gga(T137, T131, T113, T114, T138, lessB_out_gg(T131, T137)) → U15_gga(T137, T131, T113, T114, T138, insertD_in_gga(s(T137), T114, T138))
insertD_in_gga(0, tree(s(T161), T152, T153), tree(s(T161), T162, T153)) → U16_gga(T161, T152, T153, T162, insertD_in_gga(0, T152, T162))
insertD_in_gga(s(T173), tree(s(T172), T152, T153), tree(s(T172), T174, T153)) → U17_gga(T173, T172, T152, T153, T174, pC_in_ggga(T173, T172, T152, T174))
U17_gga(T173, T172, T152, T153, T174, pC_out_ggga(T173, T172, T152, T174)) → insertD_out_gga(s(T173), tree(s(T172), T152, T153), tree(s(T172), T174, T153))
insertD_in_gga(T192, tree(T188, T189, T190), tree(T188, T189, T193)) → U18_gga(T192, T188, T189, T190, T193, pE_in_ggga(T188, T192, T190, T193))
U18_gga(T192, T188, T189, T190, T193, pE_out_ggga(T188, T192, T190, T193)) → insertD_out_gga(T192, tree(T188, T189, T190), tree(T188, T189, T193))
insertD_in_gga(s(T214), tree(0, T203, T204), tree(0, T203, T213)) → U19_gga(T214, T203, T204, T213, insertD_in_gga(s(T214), T204, T213))
insertD_in_gga(s(T223), tree(s(T221), T203, T204), tree(s(T221), T203, T224)) → U20_gga(T223, T221, T203, T204, T224, lessB_in_gg(T221, T223))
U20_gga(T223, T221, T203, T204, T224, lessB_out_gg(T221, T223)) → insertD_out_gga(s(T223), tree(s(T221), T203, T204), tree(s(T221), T203, T224))
insertD_in_gga(s(T227), tree(s(T221), T203, T204), tree(s(T221), T203, T228)) → U21_gga(T227, T221, T203, T204, T228, lessB_in_gg(T221, T227))
U21_gga(T227, T221, T203, T204, T228, lessB_out_gg(T221, T227)) → U22_gga(T227, T221, T203, T204, T228, insertD_in_gga(s(T227), T204, T228))
U22_gga(T227, T221, T203, T204, T228, insertD_out_gga(s(T227), T204, T228)) → insertD_out_gga(s(T227), tree(s(T221), T203, T204), tree(s(T221), T203, T228))
U19_gga(T214, T203, T204, T213, insertD_out_gga(s(T214), T204, T213)) → insertD_out_gga(s(T214), tree(0, T203, T204), tree(0, T203, T213))
U16_gga(T161, T152, T153, T162, insertD_out_gga(0, T152, T162)) → insertD_out_gga(0, tree(s(T161), T152, T153), tree(s(T161), T162, T153))
U15_gga(T137, T131, T113, T114, T138, insertD_out_gga(s(T137), T114, T138)) → insertD_out_gga(s(T137), tree(s(T131), T113, T114), tree(s(T131), T113, T138))
U12_gga(T124, T113, T114, T123, insertD_out_gga(s(T124), T114, T123)) → insertD_out_gga(s(T124), tree(0, T113, T114), tree(0, T113, T123))
U8_ggga(T78, T86, T80, T87, insertD_out_gga(T86, T80, T87)) → pE_out_ggga(T78, T86, T80, T87)
U11_gga(T82, T78, T79, T80, T83, pE_out_ggga(T78, T82, T80, T83)) → insertD_out_gga(T82, tree(T78, T79, T80), tree(T78, T79, T83))
U5_ggga(T47, T42, T22, T48, insertD_out_gga(s(T47), T22, T48)) → pC_out_ggga(T47, T42, T22, T48)
U10_gga(T43, T42, T22, T23, T44, pC_out_ggga(T43, T42, T22, T44)) → insertD_out_gga(s(T43), tree(s(T42), T22, T23), tree(s(T42), T44, T23))
U9_gga(T31, T22, T23, T32, insertD_out_gga(0, T22, T32)) → insertD_out_gga(0, tree(s(T31), T22, T23), tree(s(T31), T32, T23))
U9_aga(T31, T22, T23, T32, insertD_out_gga(0, T22, T32)) → insertD_out_aga(0, tree(s(T31), T22, T23), tree(s(T31), T32, T23))
insertD_in_aga(s(T43), tree(s(T42), T22, T23), tree(s(T42), T44, T23)) → U10_aga(T43, T42, T22, T23, T44, pC_in_agga(T43, T42, T22, T44))
pC_in_agga(T43, T42, T22, T44) → U3_agga(T43, T42, T22, T44, lessA_in_ag(T43, T42))
lessA_in_ag(0, s(T55)) → lessA_out_ag(0, s(T55))
lessA_in_ag(s(T62), s(T61)) → U1_ag(T62, T61, lessA_in_ag(T62, T61))
U1_ag(T62, T61, lessA_out_ag(T62, T61)) → lessA_out_ag(s(T62), s(T61))
U3_agga(T43, T42, T22, T44, lessA_out_ag(T43, T42)) → pC_out_agga(T43, T42, T22, T44)
pC_in_agga(T47, T42, T22, T48) → U4_agga(T47, T42, T22, T48, lessA_in_ag(T47, T42))
U4_agga(T47, T42, T22, T48, lessA_out_ag(T47, T42)) → U5_agga(T47, T42, T22, T48, insertD_in_gga(s(T47), T22, T48))
U5_agga(T47, T42, T22, T48, insertD_out_gga(s(T47), T22, T48)) → pC_out_agga(T47, T42, T22, T48)
U10_aga(T43, T42, T22, T23, T44, pC_out_agga(T43, T42, T22, T44)) → insertD_out_aga(s(T43), tree(s(T42), T22, T23), tree(s(T42), T44, T23))
insertD_in_aga(T82, tree(T78, T79, T80), tree(T78, T79, T83)) → U11_aga(T82, T78, T79, T80, T83, pE_in_gaga(T78, T82, T80, T83))
pE_in_gaga(T78, T82, T80, T83) → U6_gaga(T78, T82, T80, T83, lessB_in_ga(T78, T82))
lessB_in_ga(0, s(T94)) → lessB_out_ga(0, s(T94))
lessB_in_ga(s(T99), s(T101)) → U2_ga(T99, T101, lessB_in_ga(T99, T101))
U2_ga(T99, T101, lessB_out_ga(T99, T101)) → lessB_out_ga(s(T99), s(T101))
U6_gaga(T78, T82, T80, T83, lessB_out_ga(T78, T82)) → pE_out_gaga(T78, T82, T80, T83)
pE_in_gaga(T78, T86, T80, T87) → U7_gaga(T78, T86, T80, T87, lessB_in_ga(T78, T86))
U7_gaga(T78, T86, T80, T87, lessB_out_ga(T78, T86)) → U8_gaga(T78, T86, T80, T87, insertD_in_aga(T86, T80, T87))
insertD_in_aga(s(T124), tree(0, T113, T114), tree(0, T113, T123)) → U12_aga(T124, T113, T114, T123, insertD_in_aga(s(T124), T114, T123))
insertD_in_aga(s(T133), tree(s(T131), T113, T114), tree(s(T131), T113, T134)) → U13_aga(T133, T131, T113, T114, T134, lessB_in_ga(T131, T133))
U13_aga(T133, T131, T113, T114, T134, lessB_out_ga(T131, T133)) → insertD_out_aga(s(T133), tree(s(T131), T113, T114), tree(s(T131), T113, T134))
insertD_in_aga(s(T137), tree(s(T131), T113, T114), tree(s(T131), T113, T138)) → U14_aga(T137, T131, T113, T114, T138, lessB_in_ga(T131, T137))
U14_aga(T137, T131, T113, T114, T138, lessB_out_ga(T131, T137)) → U15_aga(T137, T131, T113, T114, T138, insertD_in_aga(s(T137), T114, T138))
insertD_in_aga(0, tree(s(T161), T152, T153), tree(s(T161), T162, T153)) → U16_aga(T161, T152, T153, T162, insertD_in_gga(0, T152, T162))
U16_aga(T161, T152, T153, T162, insertD_out_gga(0, T152, T162)) → insertD_out_aga(0, tree(s(T161), T152, T153), tree(s(T161), T162, T153))
insertD_in_aga(s(T173), tree(s(T172), T152, T153), tree(s(T172), T174, T153)) → U17_aga(T173, T172, T152, T153, T174, pC_in_agga(T173, T172, T152, T174))
U17_aga(T173, T172, T152, T153, T174, pC_out_agga(T173, T172, T152, T174)) → insertD_out_aga(s(T173), tree(s(T172), T152, T153), tree(s(T172), T174, T153))
insertD_in_aga(T192, tree(T188, T189, T190), tree(T188, T189, T193)) → U18_aga(T192, T188, T189, T190, T193, pE_in_gaga(T188, T192, T190, T193))
U18_aga(T192, T188, T189, T190, T193, pE_out_gaga(T188, T192, T190, T193)) → insertD_out_aga(T192, tree(T188, T189, T190), tree(T188, T189, T193))
insertD_in_aga(s(T214), tree(0, T203, T204), tree(0, T203, T213)) → U19_aga(T214, T203, T204, T213, insertD_in_aga(s(T214), T204, T213))
insertD_in_aga(s(T223), tree(s(T221), T203, T204), tree(s(T221), T203, T224)) → U20_aga(T223, T221, T203, T204, T224, lessB_in_ga(T221, T223))
U20_aga(T223, T221, T203, T204, T224, lessB_out_ga(T221, T223)) → insertD_out_aga(s(T223), tree(s(T221), T203, T204), tree(s(T221), T203, T224))
insertD_in_aga(s(T227), tree(s(T221), T203, T204), tree(s(T221), T203, T228)) → U21_aga(T227, T221, T203, T204, T228, lessB_in_ga(T221, T227))
U21_aga(T227, T221, T203, T204, T228, lessB_out_ga(T221, T227)) → U22_aga(T227, T221, T203, T204, T228, insertD_in_aga(s(T227), T204, T228))
U22_aga(T227, T221, T203, T204, T228, insertD_out_aga(s(T227), T204, T228)) → insertD_out_aga(s(T227), tree(s(T221), T203, T204), tree(s(T221), T203, T228))
U19_aga(T214, T203, T204, T213, insertD_out_aga(s(T214), T204, T213)) → insertD_out_aga(s(T214), tree(0, T203, T204), tree(0, T203, T213))
U15_aga(T137, T131, T113, T114, T138, insertD_out_aga(s(T137), T114, T138)) → insertD_out_aga(s(T137), tree(s(T131), T113, T114), tree(s(T131), T113, T138))
U12_aga(T124, T113, T114, T123, insertD_out_aga(s(T124), T114, T123)) → insertD_out_aga(s(T124), tree(0, T113, T114), tree(0, T113, T123))
U8_gaga(T78, T86, T80, T87, insertD_out_aga(T86, T80, T87)) → pE_out_gaga(T78, T86, T80, T87)
U11_aga(T82, T78, T79, T80, T83, pE_out_gaga(T78, T82, T80, T83)) → insertD_out_aga(T82, tree(T78, T79, T80), tree(T78, T79, T83))
LESSB_IN_GG(s(T99), s(T101)) → LESSB_IN_GG(T99, T101)
LESSB_IN_GG(s(T99), s(T101)) → LESSB_IN_GG(T99, T101)
From the DPs we obtained the following set of size-change graphs:
LESSA_IN_GG(s(T62), s(T61)) → LESSA_IN_GG(T62, T61)
insertD_in_aga(T5, void, tree(T5, void, void)) → insertD_out_aga(T5, void, tree(T5, void, void))
insertD_in_aga(T12, tree(T12, T13, T14), tree(T12, T13, T14)) → insertD_out_aga(T12, tree(T12, T13, T14), tree(T12, T13, T14))
insertD_in_aga(0, tree(s(T31), T22, T23), tree(s(T31), T32, T23)) → U9_aga(T31, T22, T23, T32, insertD_in_gga(0, T22, T32))
insertD_in_gga(T5, void, tree(T5, void, void)) → insertD_out_gga(T5, void, tree(T5, void, void))
insertD_in_gga(T12, tree(T12, T13, T14), tree(T12, T13, T14)) → insertD_out_gga(T12, tree(T12, T13, T14), tree(T12, T13, T14))
insertD_in_gga(0, tree(s(T31), T22, T23), tree(s(T31), T32, T23)) → U9_gga(T31, T22, T23, T32, insertD_in_gga(0, T22, T32))
insertD_in_gga(s(T43), tree(s(T42), T22, T23), tree(s(T42), T44, T23)) → U10_gga(T43, T42, T22, T23, T44, pC_in_ggga(T43, T42, T22, T44))
pC_in_ggga(T43, T42, T22, T44) → U3_ggga(T43, T42, T22, T44, lessA_in_gg(T43, T42))
lessA_in_gg(0, s(T55)) → lessA_out_gg(0, s(T55))
lessA_in_gg(s(T62), s(T61)) → U1_gg(T62, T61, lessA_in_gg(T62, T61))
U1_gg(T62, T61, lessA_out_gg(T62, T61)) → lessA_out_gg(s(T62), s(T61))
U3_ggga(T43, T42, T22, T44, lessA_out_gg(T43, T42)) → pC_out_ggga(T43, T42, T22, T44)
pC_in_ggga(T47, T42, T22, T48) → U4_ggga(T47, T42, T22, T48, lessA_in_gg(T47, T42))
U4_ggga(T47, T42, T22, T48, lessA_out_gg(T47, T42)) → U5_ggga(T47, T42, T22, T48, insertD_in_gga(s(T47), T22, T48))
insertD_in_gga(T82, tree(T78, T79, T80), tree(T78, T79, T83)) → U11_gga(T82, T78, T79, T80, T83, pE_in_ggga(T78, T82, T80, T83))
pE_in_ggga(T78, T82, T80, T83) → U6_ggga(T78, T82, T80, T83, lessB_in_gg(T78, T82))
lessB_in_gg(0, s(T94)) → lessB_out_gg(0, s(T94))
lessB_in_gg(s(T99), s(T101)) → U2_gg(T99, T101, lessB_in_gg(T99, T101))
U2_gg(T99, T101, lessB_out_gg(T99, T101)) → lessB_out_gg(s(T99), s(T101))
U6_ggga(T78, T82, T80, T83, lessB_out_gg(T78, T82)) → pE_out_ggga(T78, T82, T80, T83)
pE_in_ggga(T78, T86, T80, T87) → U7_ggga(T78, T86, T80, T87, lessB_in_gg(T78, T86))
U7_ggga(T78, T86, T80, T87, lessB_out_gg(T78, T86)) → U8_ggga(T78, T86, T80, T87, insertD_in_gga(T86, T80, T87))
insertD_in_gga(s(T124), tree(0, T113, T114), tree(0, T113, T123)) → U12_gga(T124, T113, T114, T123, insertD_in_gga(s(T124), T114, T123))
insertD_in_gga(s(T133), tree(s(T131), T113, T114), tree(s(T131), T113, T134)) → U13_gga(T133, T131, T113, T114, T134, lessB_in_gg(T131, T133))
U13_gga(T133, T131, T113, T114, T134, lessB_out_gg(T131, T133)) → insertD_out_gga(s(T133), tree(s(T131), T113, T114), tree(s(T131), T113, T134))
insertD_in_gga(s(T137), tree(s(T131), T113, T114), tree(s(T131), T113, T138)) → U14_gga(T137, T131, T113, T114, T138, lessB_in_gg(T131, T137))
U14_gga(T137, T131, T113, T114, T138, lessB_out_gg(T131, T137)) → U15_gga(T137, T131, T113, T114, T138, insertD_in_gga(s(T137), T114, T138))
insertD_in_gga(0, tree(s(T161), T152, T153), tree(s(T161), T162, T153)) → U16_gga(T161, T152, T153, T162, insertD_in_gga(0, T152, T162))
insertD_in_gga(s(T173), tree(s(T172), T152, T153), tree(s(T172), T174, T153)) → U17_gga(T173, T172, T152, T153, T174, pC_in_ggga(T173, T172, T152, T174))
U17_gga(T173, T172, T152, T153, T174, pC_out_ggga(T173, T172, T152, T174)) → insertD_out_gga(s(T173), tree(s(T172), T152, T153), tree(s(T172), T174, T153))
insertD_in_gga(T192, tree(T188, T189, T190), tree(T188, T189, T193)) → U18_gga(T192, T188, T189, T190, T193, pE_in_ggga(T188, T192, T190, T193))
U18_gga(T192, T188, T189, T190, T193, pE_out_ggga(T188, T192, T190, T193)) → insertD_out_gga(T192, tree(T188, T189, T190), tree(T188, T189, T193))
insertD_in_gga(s(T214), tree(0, T203, T204), tree(0, T203, T213)) → U19_gga(T214, T203, T204, T213, insertD_in_gga(s(T214), T204, T213))
insertD_in_gga(s(T223), tree(s(T221), T203, T204), tree(s(T221), T203, T224)) → U20_gga(T223, T221, T203, T204, T224, lessB_in_gg(T221, T223))
U20_gga(T223, T221, T203, T204, T224, lessB_out_gg(T221, T223)) → insertD_out_gga(s(T223), tree(s(T221), T203, T204), tree(s(T221), T203, T224))
insertD_in_gga(s(T227), tree(s(T221), T203, T204), tree(s(T221), T203, T228)) → U21_gga(T227, T221, T203, T204, T228, lessB_in_gg(T221, T227))
U21_gga(T227, T221, T203, T204, T228, lessB_out_gg(T221, T227)) → U22_gga(T227, T221, T203, T204, T228, insertD_in_gga(s(T227), T204, T228))
U22_gga(T227, T221, T203, T204, T228, insertD_out_gga(s(T227), T204, T228)) → insertD_out_gga(s(T227), tree(s(T221), T203, T204), tree(s(T221), T203, T228))
U19_gga(T214, T203, T204, T213, insertD_out_gga(s(T214), T204, T213)) → insertD_out_gga(s(T214), tree(0, T203, T204), tree(0, T203, T213))
U16_gga(T161, T152, T153, T162, insertD_out_gga(0, T152, T162)) → insertD_out_gga(0, tree(s(T161), T152, T153), tree(s(T161), T162, T153))
U15_gga(T137, T131, T113, T114, T138, insertD_out_gga(s(T137), T114, T138)) → insertD_out_gga(s(T137), tree(s(T131), T113, T114), tree(s(T131), T113, T138))
U12_gga(T124, T113, T114, T123, insertD_out_gga(s(T124), T114, T123)) → insertD_out_gga(s(T124), tree(0, T113, T114), tree(0, T113, T123))
U8_ggga(T78, T86, T80, T87, insertD_out_gga(T86, T80, T87)) → pE_out_ggga(T78, T86, T80, T87)
U11_gga(T82, T78, T79, T80, T83, pE_out_ggga(T78, T82, T80, T83)) → insertD_out_gga(T82, tree(T78, T79, T80), tree(T78, T79, T83))
U5_ggga(T47, T42, T22, T48, insertD_out_gga(s(T47), T22, T48)) → pC_out_ggga(T47, T42, T22, T48)
U10_gga(T43, T42, T22, T23, T44, pC_out_ggga(T43, T42, T22, T44)) → insertD_out_gga(s(T43), tree(s(T42), T22, T23), tree(s(T42), T44, T23))
U9_gga(T31, T22, T23, T32, insertD_out_gga(0, T22, T32)) → insertD_out_gga(0, tree(s(T31), T22, T23), tree(s(T31), T32, T23))
U9_aga(T31, T22, T23, T32, insertD_out_gga(0, T22, T32)) → insertD_out_aga(0, tree(s(T31), T22, T23), tree(s(T31), T32, T23))
insertD_in_aga(s(T43), tree(s(T42), T22, T23), tree(s(T42), T44, T23)) → U10_aga(T43, T42, T22, T23, T44, pC_in_agga(T43, T42, T22, T44))
pC_in_agga(T43, T42, T22, T44) → U3_agga(T43, T42, T22, T44, lessA_in_ag(T43, T42))
lessA_in_ag(0, s(T55)) → lessA_out_ag(0, s(T55))
lessA_in_ag(s(T62), s(T61)) → U1_ag(T62, T61, lessA_in_ag(T62, T61))
U1_ag(T62, T61, lessA_out_ag(T62, T61)) → lessA_out_ag(s(T62), s(T61))
U3_agga(T43, T42, T22, T44, lessA_out_ag(T43, T42)) → pC_out_agga(T43, T42, T22, T44)
pC_in_agga(T47, T42, T22, T48) → U4_agga(T47, T42, T22, T48, lessA_in_ag(T47, T42))
U4_agga(T47, T42, T22, T48, lessA_out_ag(T47, T42)) → U5_agga(T47, T42, T22, T48, insertD_in_gga(s(T47), T22, T48))
U5_agga(T47, T42, T22, T48, insertD_out_gga(s(T47), T22, T48)) → pC_out_agga(T47, T42, T22, T48)
U10_aga(T43, T42, T22, T23, T44, pC_out_agga(T43, T42, T22, T44)) → insertD_out_aga(s(T43), tree(s(T42), T22, T23), tree(s(T42), T44, T23))
insertD_in_aga(T82, tree(T78, T79, T80), tree(T78, T79, T83)) → U11_aga(T82, T78, T79, T80, T83, pE_in_gaga(T78, T82, T80, T83))
pE_in_gaga(T78, T82, T80, T83) → U6_gaga(T78, T82, T80, T83, lessB_in_ga(T78, T82))
lessB_in_ga(0, s(T94)) → lessB_out_ga(0, s(T94))
lessB_in_ga(s(T99), s(T101)) → U2_ga(T99, T101, lessB_in_ga(T99, T101))
U2_ga(T99, T101, lessB_out_ga(T99, T101)) → lessB_out_ga(s(T99), s(T101))
U6_gaga(T78, T82, T80, T83, lessB_out_ga(T78, T82)) → pE_out_gaga(T78, T82, T80, T83)
pE_in_gaga(T78, T86, T80, T87) → U7_gaga(T78, T86, T80, T87, lessB_in_ga(T78, T86))
U7_gaga(T78, T86, T80, T87, lessB_out_ga(T78, T86)) → U8_gaga(T78, T86, T80, T87, insertD_in_aga(T86, T80, T87))
insertD_in_aga(s(T124), tree(0, T113, T114), tree(0, T113, T123)) → U12_aga(T124, T113, T114, T123, insertD_in_aga(s(T124), T114, T123))
insertD_in_aga(s(T133), tree(s(T131), T113, T114), tree(s(T131), T113, T134)) → U13_aga(T133, T131, T113, T114, T134, lessB_in_ga(T131, T133))
U13_aga(T133, T131, T113, T114, T134, lessB_out_ga(T131, T133)) → insertD_out_aga(s(T133), tree(s(T131), T113, T114), tree(s(T131), T113, T134))
insertD_in_aga(s(T137), tree(s(T131), T113, T114), tree(s(T131), T113, T138)) → U14_aga(T137, T131, T113, T114, T138, lessB_in_ga(T131, T137))
U14_aga(T137, T131, T113, T114, T138, lessB_out_ga(T131, T137)) → U15_aga(T137, T131, T113, T114, T138, insertD_in_aga(s(T137), T114, T138))
insertD_in_aga(0, tree(s(T161), T152, T153), tree(s(T161), T162, T153)) → U16_aga(T161, T152, T153, T162, insertD_in_gga(0, T152, T162))
U16_aga(T161, T152, T153, T162, insertD_out_gga(0, T152, T162)) → insertD_out_aga(0, tree(s(T161), T152, T153), tree(s(T161), T162, T153))
insertD_in_aga(s(T173), tree(s(T172), T152, T153), tree(s(T172), T174, T153)) → U17_aga(T173, T172, T152, T153, T174, pC_in_agga(T173, T172, T152, T174))
U17_aga(T173, T172, T152, T153, T174, pC_out_agga(T173, T172, T152, T174)) → insertD_out_aga(s(T173), tree(s(T172), T152, T153), tree(s(T172), T174, T153))
insertD_in_aga(T192, tree(T188, T189, T190), tree(T188, T189, T193)) → U18_aga(T192, T188, T189, T190, T193, pE_in_gaga(T188, T192, T190, T193))
U18_aga(T192, T188, T189, T190, T193, pE_out_gaga(T188, T192, T190, T193)) → insertD_out_aga(T192, tree(T188, T189, T190), tree(T188, T189, T193))
insertD_in_aga(s(T214), tree(0, T203, T204), tree(0, T203, T213)) → U19_aga(T214, T203, T204, T213, insertD_in_aga(s(T214), T204, T213))
insertD_in_aga(s(T223), tree(s(T221), T203, T204), tree(s(T221), T203, T224)) → U20_aga(T223, T221, T203, T204, T224, lessB_in_ga(T221, T223))
U20_aga(T223, T221, T203, T204, T224, lessB_out_ga(T221, T223)) → insertD_out_aga(s(T223), tree(s(T221), T203, T204), tree(s(T221), T203, T224))
insertD_in_aga(s(T227), tree(s(T221), T203, T204), tree(s(T221), T203, T228)) → U21_aga(T227, T221, T203, T204, T228, lessB_in_ga(T221, T227))
U21_aga(T227, T221, T203, T204, T228, lessB_out_ga(T221, T227)) → U22_aga(T227, T221, T203, T204, T228, insertD_in_aga(s(T227), T204, T228))
U22_aga(T227, T221, T203, T204, T228, insertD_out_aga(s(T227), T204, T228)) → insertD_out_aga(s(T227), tree(s(T221), T203, T204), tree(s(T221), T203, T228))
U19_aga(T214, T203, T204, T213, insertD_out_aga(s(T214), T204, T213)) → insertD_out_aga(s(T214), tree(0, T203, T204), tree(0, T203, T213))
U15_aga(T137, T131, T113, T114, T138, insertD_out_aga(s(T137), T114, T138)) → insertD_out_aga(s(T137), tree(s(T131), T113, T114), tree(s(T131), T113, T138))
U12_aga(T124, T113, T114, T123, insertD_out_aga(s(T124), T114, T123)) → insertD_out_aga(s(T124), tree(0, T113, T114), tree(0, T113, T123))
U8_gaga(T78, T86, T80, T87, insertD_out_aga(T86, T80, T87)) → pE_out_gaga(T78, T86, T80, T87)
U11_aga(T82, T78, T79, T80, T83, pE_out_gaga(T78, T82, T80, T83)) → insertD_out_aga(T82, tree(T78, T79, T80), tree(T78, T79, T83))
LESSA_IN_GG(s(T62), s(T61)) → LESSA_IN_GG(T62, T61)
LESSA_IN_GG(s(T62), s(T61)) → LESSA_IN_GG(T62, T61)
From the DPs we obtained the following set of size-change graphs:
INSERTD_IN_GGA(T82, tree(T78, T79, T80), tree(T78, T79, T83)) → PE_IN_GGGA(T78, T82, T80, T83)
PE_IN_GGGA(T78, T86, T80, T87) → U7_GGGA(T78, T86, T80, T87, lessB_in_gg(T78, T86))
U7_GGGA(T78, T86, T80, T87, lessB_out_gg(T78, T86)) → INSERTD_IN_GGA(T86, T80, T87)
INSERTD_IN_GGA(0, tree(s(T31), T22, T23), tree(s(T31), T32, T23)) → INSERTD_IN_GGA(0, T22, T32)
INSERTD_IN_GGA(s(T43), tree(s(T42), T22, T23), tree(s(T42), T44, T23)) → PC_IN_GGGA(T43, T42, T22, T44)
PC_IN_GGGA(T47, T42, T22, T48) → U4_GGGA(T47, T42, T22, T48, lessA_in_gg(T47, T42))
U4_GGGA(T47, T42, T22, T48, lessA_out_gg(T47, T42)) → INSERTD_IN_GGA(s(T47), T22, T48)
INSERTD_IN_GGA(s(T124), tree(0, T113, T114), tree(0, T113, T123)) → INSERTD_IN_GGA(s(T124), T114, T123)
INSERTD_IN_GGA(s(T137), tree(s(T131), T113, T114), tree(s(T131), T113, T138)) → U14_GGA(T137, T131, T113, T114, T138, lessB_in_gg(T131, T137))
U14_GGA(T137, T131, T113, T114, T138, lessB_out_gg(T131, T137)) → INSERTD_IN_GGA(s(T137), T114, T138)
INSERTD_IN_GGA(s(T227), tree(s(T221), T203, T204), tree(s(T221), T203, T228)) → U21_GGA(T227, T221, T203, T204, T228, lessB_in_gg(T221, T227))
U21_GGA(T227, T221, T203, T204, T228, lessB_out_gg(T221, T227)) → INSERTD_IN_GGA(s(T227), T204, T228)
insertD_in_aga(T5, void, tree(T5, void, void)) → insertD_out_aga(T5, void, tree(T5, void, void))
insertD_in_aga(T12, tree(T12, T13, T14), tree(T12, T13, T14)) → insertD_out_aga(T12, tree(T12, T13, T14), tree(T12, T13, T14))
insertD_in_aga(0, tree(s(T31), T22, T23), tree(s(T31), T32, T23)) → U9_aga(T31, T22, T23, T32, insertD_in_gga(0, T22, T32))
insertD_in_gga(T5, void, tree(T5, void, void)) → insertD_out_gga(T5, void, tree(T5, void, void))
insertD_in_gga(T12, tree(T12, T13, T14), tree(T12, T13, T14)) → insertD_out_gga(T12, tree(T12, T13, T14), tree(T12, T13, T14))
insertD_in_gga(0, tree(s(T31), T22, T23), tree(s(T31), T32, T23)) → U9_gga(T31, T22, T23, T32, insertD_in_gga(0, T22, T32))
insertD_in_gga(s(T43), tree(s(T42), T22, T23), tree(s(T42), T44, T23)) → U10_gga(T43, T42, T22, T23, T44, pC_in_ggga(T43, T42, T22, T44))
pC_in_ggga(T43, T42, T22, T44) → U3_ggga(T43, T42, T22, T44, lessA_in_gg(T43, T42))
lessA_in_gg(0, s(T55)) → lessA_out_gg(0, s(T55))
lessA_in_gg(s(T62), s(T61)) → U1_gg(T62, T61, lessA_in_gg(T62, T61))
U1_gg(T62, T61, lessA_out_gg(T62, T61)) → lessA_out_gg(s(T62), s(T61))
U3_ggga(T43, T42, T22, T44, lessA_out_gg(T43, T42)) → pC_out_ggga(T43, T42, T22, T44)
pC_in_ggga(T47, T42, T22, T48) → U4_ggga(T47, T42, T22, T48, lessA_in_gg(T47, T42))
U4_ggga(T47, T42, T22, T48, lessA_out_gg(T47, T42)) → U5_ggga(T47, T42, T22, T48, insertD_in_gga(s(T47), T22, T48))
insertD_in_gga(T82, tree(T78, T79, T80), tree(T78, T79, T83)) → U11_gga(T82, T78, T79, T80, T83, pE_in_ggga(T78, T82, T80, T83))
pE_in_ggga(T78, T82, T80, T83) → U6_ggga(T78, T82, T80, T83, lessB_in_gg(T78, T82))
lessB_in_gg(0, s(T94)) → lessB_out_gg(0, s(T94))
lessB_in_gg(s(T99), s(T101)) → U2_gg(T99, T101, lessB_in_gg(T99, T101))
U2_gg(T99, T101, lessB_out_gg(T99, T101)) → lessB_out_gg(s(T99), s(T101))
U6_ggga(T78, T82, T80, T83, lessB_out_gg(T78, T82)) → pE_out_ggga(T78, T82, T80, T83)
pE_in_ggga(T78, T86, T80, T87) → U7_ggga(T78, T86, T80, T87, lessB_in_gg(T78, T86))
U7_ggga(T78, T86, T80, T87, lessB_out_gg(T78, T86)) → U8_ggga(T78, T86, T80, T87, insertD_in_gga(T86, T80, T87))
insertD_in_gga(s(T124), tree(0, T113, T114), tree(0, T113, T123)) → U12_gga(T124, T113, T114, T123, insertD_in_gga(s(T124), T114, T123))
insertD_in_gga(s(T133), tree(s(T131), T113, T114), tree(s(T131), T113, T134)) → U13_gga(T133, T131, T113, T114, T134, lessB_in_gg(T131, T133))
U13_gga(T133, T131, T113, T114, T134, lessB_out_gg(T131, T133)) → insertD_out_gga(s(T133), tree(s(T131), T113, T114), tree(s(T131), T113, T134))
insertD_in_gga(s(T137), tree(s(T131), T113, T114), tree(s(T131), T113, T138)) → U14_gga(T137, T131, T113, T114, T138, lessB_in_gg(T131, T137))
U14_gga(T137, T131, T113, T114, T138, lessB_out_gg(T131, T137)) → U15_gga(T137, T131, T113, T114, T138, insertD_in_gga(s(T137), T114, T138))
insertD_in_gga(0, tree(s(T161), T152, T153), tree(s(T161), T162, T153)) → U16_gga(T161, T152, T153, T162, insertD_in_gga(0, T152, T162))
insertD_in_gga(s(T173), tree(s(T172), T152, T153), tree(s(T172), T174, T153)) → U17_gga(T173, T172, T152, T153, T174, pC_in_ggga(T173, T172, T152, T174))
U17_gga(T173, T172, T152, T153, T174, pC_out_ggga(T173, T172, T152, T174)) → insertD_out_gga(s(T173), tree(s(T172), T152, T153), tree(s(T172), T174, T153))
insertD_in_gga(T192, tree(T188, T189, T190), tree(T188, T189, T193)) → U18_gga(T192, T188, T189, T190, T193, pE_in_ggga(T188, T192, T190, T193))
U18_gga(T192, T188, T189, T190, T193, pE_out_ggga(T188, T192, T190, T193)) → insertD_out_gga(T192, tree(T188, T189, T190), tree(T188, T189, T193))
insertD_in_gga(s(T214), tree(0, T203, T204), tree(0, T203, T213)) → U19_gga(T214, T203, T204, T213, insertD_in_gga(s(T214), T204, T213))
insertD_in_gga(s(T223), tree(s(T221), T203, T204), tree(s(T221), T203, T224)) → U20_gga(T223, T221, T203, T204, T224, lessB_in_gg(T221, T223))
U20_gga(T223, T221, T203, T204, T224, lessB_out_gg(T221, T223)) → insertD_out_gga(s(T223), tree(s(T221), T203, T204), tree(s(T221), T203, T224))
insertD_in_gga(s(T227), tree(s(T221), T203, T204), tree(s(T221), T203, T228)) → U21_gga(T227, T221, T203, T204, T228, lessB_in_gg(T221, T227))
U21_gga(T227, T221, T203, T204, T228, lessB_out_gg(T221, T227)) → U22_gga(T227, T221, T203, T204, T228, insertD_in_gga(s(T227), T204, T228))
U22_gga(T227, T221, T203, T204, T228, insertD_out_gga(s(T227), T204, T228)) → insertD_out_gga(s(T227), tree(s(T221), T203, T204), tree(s(T221), T203, T228))
U19_gga(T214, T203, T204, T213, insertD_out_gga(s(T214), T204, T213)) → insertD_out_gga(s(T214), tree(0, T203, T204), tree(0, T203, T213))
U16_gga(T161, T152, T153, T162, insertD_out_gga(0, T152, T162)) → insertD_out_gga(0, tree(s(T161), T152, T153), tree(s(T161), T162, T153))
U15_gga(T137, T131, T113, T114, T138, insertD_out_gga(s(T137), T114, T138)) → insertD_out_gga(s(T137), tree(s(T131), T113, T114), tree(s(T131), T113, T138))
U12_gga(T124, T113, T114, T123, insertD_out_gga(s(T124), T114, T123)) → insertD_out_gga(s(T124), tree(0, T113, T114), tree(0, T113, T123))
U8_ggga(T78, T86, T80, T87, insertD_out_gga(T86, T80, T87)) → pE_out_ggga(T78, T86, T80, T87)
U11_gga(T82, T78, T79, T80, T83, pE_out_ggga(T78, T82, T80, T83)) → insertD_out_gga(T82, tree(T78, T79, T80), tree(T78, T79, T83))
U5_ggga(T47, T42, T22, T48, insertD_out_gga(s(T47), T22, T48)) → pC_out_ggga(T47, T42, T22, T48)
U10_gga(T43, T42, T22, T23, T44, pC_out_ggga(T43, T42, T22, T44)) → insertD_out_gga(s(T43), tree(s(T42), T22, T23), tree(s(T42), T44, T23))
U9_gga(T31, T22, T23, T32, insertD_out_gga(0, T22, T32)) → insertD_out_gga(0, tree(s(T31), T22, T23), tree(s(T31), T32, T23))
U9_aga(T31, T22, T23, T32, insertD_out_gga(0, T22, T32)) → insertD_out_aga(0, tree(s(T31), T22, T23), tree(s(T31), T32, T23))
insertD_in_aga(s(T43), tree(s(T42), T22, T23), tree(s(T42), T44, T23)) → U10_aga(T43, T42, T22, T23, T44, pC_in_agga(T43, T42, T22, T44))
pC_in_agga(T43, T42, T22, T44) → U3_agga(T43, T42, T22, T44, lessA_in_ag(T43, T42))
lessA_in_ag(0, s(T55)) → lessA_out_ag(0, s(T55))
lessA_in_ag(s(T62), s(T61)) → U1_ag(T62, T61, lessA_in_ag(T62, T61))
U1_ag(T62, T61, lessA_out_ag(T62, T61)) → lessA_out_ag(s(T62), s(T61))
U3_agga(T43, T42, T22, T44, lessA_out_ag(T43, T42)) → pC_out_agga(T43, T42, T22, T44)
pC_in_agga(T47, T42, T22, T48) → U4_agga(T47, T42, T22, T48, lessA_in_ag(T47, T42))
U4_agga(T47, T42, T22, T48, lessA_out_ag(T47, T42)) → U5_agga(T47, T42, T22, T48, insertD_in_gga(s(T47), T22, T48))
U5_agga(T47, T42, T22, T48, insertD_out_gga(s(T47), T22, T48)) → pC_out_agga(T47, T42, T22, T48)
U10_aga(T43, T42, T22, T23, T44, pC_out_agga(T43, T42, T22, T44)) → insertD_out_aga(s(T43), tree(s(T42), T22, T23), tree(s(T42), T44, T23))
insertD_in_aga(T82, tree(T78, T79, T80), tree(T78, T79, T83)) → U11_aga(T82, T78, T79, T80, T83, pE_in_gaga(T78, T82, T80, T83))
pE_in_gaga(T78, T82, T80, T83) → U6_gaga(T78, T82, T80, T83, lessB_in_ga(T78, T82))
lessB_in_ga(0, s(T94)) → lessB_out_ga(0, s(T94))
lessB_in_ga(s(T99), s(T101)) → U2_ga(T99, T101, lessB_in_ga(T99, T101))
U2_ga(T99, T101, lessB_out_ga(T99, T101)) → lessB_out_ga(s(T99), s(T101))
U6_gaga(T78, T82, T80, T83, lessB_out_ga(T78, T82)) → pE_out_gaga(T78, T82, T80, T83)
pE_in_gaga(T78, T86, T80, T87) → U7_gaga(T78, T86, T80, T87, lessB_in_ga(T78, T86))
U7_gaga(T78, T86, T80, T87, lessB_out_ga(T78, T86)) → U8_gaga(T78, T86, T80, T87, insertD_in_aga(T86, T80, T87))
insertD_in_aga(s(T124), tree(0, T113, T114), tree(0, T113, T123)) → U12_aga(T124, T113, T114, T123, insertD_in_aga(s(T124), T114, T123))
insertD_in_aga(s(T133), tree(s(T131), T113, T114), tree(s(T131), T113, T134)) → U13_aga(T133, T131, T113, T114, T134, lessB_in_ga(T131, T133))
U13_aga(T133, T131, T113, T114, T134, lessB_out_ga(T131, T133)) → insertD_out_aga(s(T133), tree(s(T131), T113, T114), tree(s(T131), T113, T134))
insertD_in_aga(s(T137), tree(s(T131), T113, T114), tree(s(T131), T113, T138)) → U14_aga(T137, T131, T113, T114, T138, lessB_in_ga(T131, T137))
U14_aga(T137, T131, T113, T114, T138, lessB_out_ga(T131, T137)) → U15_aga(T137, T131, T113, T114, T138, insertD_in_aga(s(T137), T114, T138))
insertD_in_aga(0, tree(s(T161), T152, T153), tree(s(T161), T162, T153)) → U16_aga(T161, T152, T153, T162, insertD_in_gga(0, T152, T162))
U16_aga(T161, T152, T153, T162, insertD_out_gga(0, T152, T162)) → insertD_out_aga(0, tree(s(T161), T152, T153), tree(s(T161), T162, T153))
insertD_in_aga(s(T173), tree(s(T172), T152, T153), tree(s(T172), T174, T153)) → U17_aga(T173, T172, T152, T153, T174, pC_in_agga(T173, T172, T152, T174))
U17_aga(T173, T172, T152, T153, T174, pC_out_agga(T173, T172, T152, T174)) → insertD_out_aga(s(T173), tree(s(T172), T152, T153), tree(s(T172), T174, T153))
insertD_in_aga(T192, tree(T188, T189, T190), tree(T188, T189, T193)) → U18_aga(T192, T188, T189, T190, T193, pE_in_gaga(T188, T192, T190, T193))
U18_aga(T192, T188, T189, T190, T193, pE_out_gaga(T188, T192, T190, T193)) → insertD_out_aga(T192, tree(T188, T189, T190), tree(T188, T189, T193))
insertD_in_aga(s(T214), tree(0, T203, T204), tree(0, T203, T213)) → U19_aga(T214, T203, T204, T213, insertD_in_aga(s(T214), T204, T213))
insertD_in_aga(s(T223), tree(s(T221), T203, T204), tree(s(T221), T203, T224)) → U20_aga(T223, T221, T203, T204, T224, lessB_in_ga(T221, T223))
U20_aga(T223, T221, T203, T204, T224, lessB_out_ga(T221, T223)) → insertD_out_aga(s(T223), tree(s(T221), T203, T204), tree(s(T221), T203, T224))
insertD_in_aga(s(T227), tree(s(T221), T203, T204), tree(s(T221), T203, T228)) → U21_aga(T227, T221, T203, T204, T228, lessB_in_ga(T221, T227))
U21_aga(T227, T221, T203, T204, T228, lessB_out_ga(T221, T227)) → U22_aga(T227, T221, T203, T204, T228, insertD_in_aga(s(T227), T204, T228))
U22_aga(T227, T221, T203, T204, T228, insertD_out_aga(s(T227), T204, T228)) → insertD_out_aga(s(T227), tree(s(T221), T203, T204), tree(s(T221), T203, T228))
U19_aga(T214, T203, T204, T213, insertD_out_aga(s(T214), T204, T213)) → insertD_out_aga(s(T214), tree(0, T203, T204), tree(0, T203, T213))
U15_aga(T137, T131, T113, T114, T138, insertD_out_aga(s(T137), T114, T138)) → insertD_out_aga(s(T137), tree(s(T131), T113, T114), tree(s(T131), T113, T138))
U12_aga(T124, T113, T114, T123, insertD_out_aga(s(T124), T114, T123)) → insertD_out_aga(s(T124), tree(0, T113, T114), tree(0, T113, T123))
U8_gaga(T78, T86, T80, T87, insertD_out_aga(T86, T80, T87)) → pE_out_gaga(T78, T86, T80, T87)
U11_aga(T82, T78, T79, T80, T83, pE_out_gaga(T78, T82, T80, T83)) → insertD_out_aga(T82, tree(T78, T79, T80), tree(T78, T79, T83))
INSERTD_IN_GGA(T82, tree(T78, T79, T80), tree(T78, T79, T83)) → PE_IN_GGGA(T78, T82, T80, T83)
PE_IN_GGGA(T78, T86, T80, T87) → U7_GGGA(T78, T86, T80, T87, lessB_in_gg(T78, T86))
U7_GGGA(T78, T86, T80, T87, lessB_out_gg(T78, T86)) → INSERTD_IN_GGA(T86, T80, T87)
INSERTD_IN_GGA(0, tree(s(T31), T22, T23), tree(s(T31), T32, T23)) → INSERTD_IN_GGA(0, T22, T32)
INSERTD_IN_GGA(s(T43), tree(s(T42), T22, T23), tree(s(T42), T44, T23)) → PC_IN_GGGA(T43, T42, T22, T44)
PC_IN_GGGA(T47, T42, T22, T48) → U4_GGGA(T47, T42, T22, T48, lessA_in_gg(T47, T42))
U4_GGGA(T47, T42, T22, T48, lessA_out_gg(T47, T42)) → INSERTD_IN_GGA(s(T47), T22, T48)
INSERTD_IN_GGA(s(T124), tree(0, T113, T114), tree(0, T113, T123)) → INSERTD_IN_GGA(s(T124), T114, T123)
INSERTD_IN_GGA(s(T137), tree(s(T131), T113, T114), tree(s(T131), T113, T138)) → U14_GGA(T137, T131, T113, T114, T138, lessB_in_gg(T131, T137))
U14_GGA(T137, T131, T113, T114, T138, lessB_out_gg(T131, T137)) → INSERTD_IN_GGA(s(T137), T114, T138)
INSERTD_IN_GGA(s(T227), tree(s(T221), T203, T204), tree(s(T221), T203, T228)) → U21_GGA(T227, T221, T203, T204, T228, lessB_in_gg(T221, T227))
U21_GGA(T227, T221, T203, T204, T228, lessB_out_gg(T221, T227)) → INSERTD_IN_GGA(s(T227), T204, T228)
lessB_in_gg(0, s(T94)) → lessB_out_gg(0, s(T94))
lessB_in_gg(s(T99), s(T101)) → U2_gg(T99, T101, lessB_in_gg(T99, T101))
lessA_in_gg(0, s(T55)) → lessA_out_gg(0, s(T55))
lessA_in_gg(s(T62), s(T61)) → U1_gg(T62, T61, lessA_in_gg(T62, T61))
U2_gg(T99, T101, lessB_out_gg(T99, T101)) → lessB_out_gg(s(T99), s(T101))
U1_gg(T62, T61, lessA_out_gg(T62, T61)) → lessA_out_gg(s(T62), s(T61))
INSERTD_IN_GGA(T82, tree(T78, T79, T80)) → PE_IN_GGGA(T78, T82, T80)
PE_IN_GGGA(T78, T86, T80) → U7_GGGA(T78, T86, T80, lessB_in_gg(T78, T86))
U7_GGGA(T78, T86, T80, lessB_out_gg(T78, T86)) → INSERTD_IN_GGA(T86, T80)
INSERTD_IN_GGA(0, tree(s(T31), T22, T23)) → INSERTD_IN_GGA(0, T22)
INSERTD_IN_GGA(s(T43), tree(s(T42), T22, T23)) → PC_IN_GGGA(T43, T42, T22)
PC_IN_GGGA(T47, T42, T22) → U4_GGGA(T47, T42, T22, lessA_in_gg(T47, T42))
U4_GGGA(T47, T42, T22, lessA_out_gg(T47, T42)) → INSERTD_IN_GGA(s(T47), T22)
INSERTD_IN_GGA(s(T124), tree(0, T113, T114)) → INSERTD_IN_GGA(s(T124), T114)
INSERTD_IN_GGA(s(T137), tree(s(T131), T113, T114)) → U14_GGA(T137, T131, T113, T114, lessB_in_gg(T131, T137))
U14_GGA(T137, T131, T113, T114, lessB_out_gg(T131, T137)) → INSERTD_IN_GGA(s(T137), T114)
INSERTD_IN_GGA(s(T227), tree(s(T221), T203, T204)) → U21_GGA(T227, T221, T203, T204, lessB_in_gg(T221, T227))
U21_GGA(T227, T221, T203, T204, lessB_out_gg(T221, T227)) → INSERTD_IN_GGA(s(T227), T204)
lessB_in_gg(0, s(T94)) → lessB_out_gg(0, s(T94))
lessB_in_gg(s(T99), s(T101)) → U2_gg(T99, T101, lessB_in_gg(T99, T101))
lessA_in_gg(0, s(T55)) → lessA_out_gg(0, s(T55))
lessA_in_gg(s(T62), s(T61)) → U1_gg(T62, T61, lessA_in_gg(T62, T61))
U2_gg(T99, T101, lessB_out_gg(T99, T101)) → lessB_out_gg(s(T99), s(T101))
U1_gg(T62, T61, lessA_out_gg(T62, T61)) → lessA_out_gg(s(T62), s(T61))
lessB_in_gg(x0, x1)
lessA_in_gg(x0, x1)
U2_gg(x0, x1, x2)
U1_gg(x0, x1, x2)
From the DPs we obtained the following set of size-change graphs:
INSERTD_IN_AGA(T82, tree(T78, T79, T80), tree(T78, T79, T83)) → PE_IN_GAGA(T78, T82, T80, T83)
PE_IN_GAGA(T78, T86, T80, T87) → U7_GAGA(T78, T86, T80, T87, lessB_in_ga(T78, T86))
U7_GAGA(T78, T86, T80, T87, lessB_out_ga(T78, T86)) → INSERTD_IN_AGA(T86, T80, T87)
INSERTD_IN_AGA(s(T124), tree(0, T113, T114), tree(0, T113, T123)) → INSERTD_IN_AGA(s(T124), T114, T123)
INSERTD_IN_AGA(s(T137), tree(s(T131), T113, T114), tree(s(T131), T113, T138)) → U14_AGA(T137, T131, T113, T114, T138, lessB_in_ga(T131, T137))
U14_AGA(T137, T131, T113, T114, T138, lessB_out_ga(T131, T137)) → INSERTD_IN_AGA(s(T137), T114, T138)
INSERTD_IN_AGA(s(T227), tree(s(T221), T203, T204), tree(s(T221), T203, T228)) → U21_AGA(T227, T221, T203, T204, T228, lessB_in_ga(T221, T227))
U21_AGA(T227, T221, T203, T204, T228, lessB_out_ga(T221, T227)) → INSERTD_IN_AGA(s(T227), T204, T228)
insertD_in_aga(T5, void, tree(T5, void, void)) → insertD_out_aga(T5, void, tree(T5, void, void))
insertD_in_aga(T12, tree(T12, T13, T14), tree(T12, T13, T14)) → insertD_out_aga(T12, tree(T12, T13, T14), tree(T12, T13, T14))
insertD_in_aga(0, tree(s(T31), T22, T23), tree(s(T31), T32, T23)) → U9_aga(T31, T22, T23, T32, insertD_in_gga(0, T22, T32))
insertD_in_gga(T5, void, tree(T5, void, void)) → insertD_out_gga(T5, void, tree(T5, void, void))
insertD_in_gga(T12, tree(T12, T13, T14), tree(T12, T13, T14)) → insertD_out_gga(T12, tree(T12, T13, T14), tree(T12, T13, T14))
insertD_in_gga(0, tree(s(T31), T22, T23), tree(s(T31), T32, T23)) → U9_gga(T31, T22, T23, T32, insertD_in_gga(0, T22, T32))
insertD_in_gga(s(T43), tree(s(T42), T22, T23), tree(s(T42), T44, T23)) → U10_gga(T43, T42, T22, T23, T44, pC_in_ggga(T43, T42, T22, T44))
pC_in_ggga(T43, T42, T22, T44) → U3_ggga(T43, T42, T22, T44, lessA_in_gg(T43, T42))
lessA_in_gg(0, s(T55)) → lessA_out_gg(0, s(T55))
lessA_in_gg(s(T62), s(T61)) → U1_gg(T62, T61, lessA_in_gg(T62, T61))
U1_gg(T62, T61, lessA_out_gg(T62, T61)) → lessA_out_gg(s(T62), s(T61))
U3_ggga(T43, T42, T22, T44, lessA_out_gg(T43, T42)) → pC_out_ggga(T43, T42, T22, T44)
pC_in_ggga(T47, T42, T22, T48) → U4_ggga(T47, T42, T22, T48, lessA_in_gg(T47, T42))
U4_ggga(T47, T42, T22, T48, lessA_out_gg(T47, T42)) → U5_ggga(T47, T42, T22, T48, insertD_in_gga(s(T47), T22, T48))
insertD_in_gga(T82, tree(T78, T79, T80), tree(T78, T79, T83)) → U11_gga(T82, T78, T79, T80, T83, pE_in_ggga(T78, T82, T80, T83))
pE_in_ggga(T78, T82, T80, T83) → U6_ggga(T78, T82, T80, T83, lessB_in_gg(T78, T82))
lessB_in_gg(0, s(T94)) → lessB_out_gg(0, s(T94))
lessB_in_gg(s(T99), s(T101)) → U2_gg(T99, T101, lessB_in_gg(T99, T101))
U2_gg(T99, T101, lessB_out_gg(T99, T101)) → lessB_out_gg(s(T99), s(T101))
U6_ggga(T78, T82, T80, T83, lessB_out_gg(T78, T82)) → pE_out_ggga(T78, T82, T80, T83)
pE_in_ggga(T78, T86, T80, T87) → U7_ggga(T78, T86, T80, T87, lessB_in_gg(T78, T86))
U7_ggga(T78, T86, T80, T87, lessB_out_gg(T78, T86)) → U8_ggga(T78, T86, T80, T87, insertD_in_gga(T86, T80, T87))
insertD_in_gga(s(T124), tree(0, T113, T114), tree(0, T113, T123)) → U12_gga(T124, T113, T114, T123, insertD_in_gga(s(T124), T114, T123))
insertD_in_gga(s(T133), tree(s(T131), T113, T114), tree(s(T131), T113, T134)) → U13_gga(T133, T131, T113, T114, T134, lessB_in_gg(T131, T133))
U13_gga(T133, T131, T113, T114, T134, lessB_out_gg(T131, T133)) → insertD_out_gga(s(T133), tree(s(T131), T113, T114), tree(s(T131), T113, T134))
insertD_in_gga(s(T137), tree(s(T131), T113, T114), tree(s(T131), T113, T138)) → U14_gga(T137, T131, T113, T114, T138, lessB_in_gg(T131, T137))
U14_gga(T137, T131, T113, T114, T138, lessB_out_gg(T131, T137)) → U15_gga(T137, T131, T113, T114, T138, insertD_in_gga(s(T137), T114, T138))
insertD_in_gga(0, tree(s(T161), T152, T153), tree(s(T161), T162, T153)) → U16_gga(T161, T152, T153, T162, insertD_in_gga(0, T152, T162))
insertD_in_gga(s(T173), tree(s(T172), T152, T153), tree(s(T172), T174, T153)) → U17_gga(T173, T172, T152, T153, T174, pC_in_ggga(T173, T172, T152, T174))
U17_gga(T173, T172, T152, T153, T174, pC_out_ggga(T173, T172, T152, T174)) → insertD_out_gga(s(T173), tree(s(T172), T152, T153), tree(s(T172), T174, T153))
insertD_in_gga(T192, tree(T188, T189, T190), tree(T188, T189, T193)) → U18_gga(T192, T188, T189, T190, T193, pE_in_ggga(T188, T192, T190, T193))
U18_gga(T192, T188, T189, T190, T193, pE_out_ggga(T188, T192, T190, T193)) → insertD_out_gga(T192, tree(T188, T189, T190), tree(T188, T189, T193))
insertD_in_gga(s(T214), tree(0, T203, T204), tree(0, T203, T213)) → U19_gga(T214, T203, T204, T213, insertD_in_gga(s(T214), T204, T213))
insertD_in_gga(s(T223), tree(s(T221), T203, T204), tree(s(T221), T203, T224)) → U20_gga(T223, T221, T203, T204, T224, lessB_in_gg(T221, T223))
U20_gga(T223, T221, T203, T204, T224, lessB_out_gg(T221, T223)) → insertD_out_gga(s(T223), tree(s(T221), T203, T204), tree(s(T221), T203, T224))
insertD_in_gga(s(T227), tree(s(T221), T203, T204), tree(s(T221), T203, T228)) → U21_gga(T227, T221, T203, T204, T228, lessB_in_gg(T221, T227))
U21_gga(T227, T221, T203, T204, T228, lessB_out_gg(T221, T227)) → U22_gga(T227, T221, T203, T204, T228, insertD_in_gga(s(T227), T204, T228))
U22_gga(T227, T221, T203, T204, T228, insertD_out_gga(s(T227), T204, T228)) → insertD_out_gga(s(T227), tree(s(T221), T203, T204), tree(s(T221), T203, T228))
U19_gga(T214, T203, T204, T213, insertD_out_gga(s(T214), T204, T213)) → insertD_out_gga(s(T214), tree(0, T203, T204), tree(0, T203, T213))
U16_gga(T161, T152, T153, T162, insertD_out_gga(0, T152, T162)) → insertD_out_gga(0, tree(s(T161), T152, T153), tree(s(T161), T162, T153))
U15_gga(T137, T131, T113, T114, T138, insertD_out_gga(s(T137), T114, T138)) → insertD_out_gga(s(T137), tree(s(T131), T113, T114), tree(s(T131), T113, T138))
U12_gga(T124, T113, T114, T123, insertD_out_gga(s(T124), T114, T123)) → insertD_out_gga(s(T124), tree(0, T113, T114), tree(0, T113, T123))
U8_ggga(T78, T86, T80, T87, insertD_out_gga(T86, T80, T87)) → pE_out_ggga(T78, T86, T80, T87)
U11_gga(T82, T78, T79, T80, T83, pE_out_ggga(T78, T82, T80, T83)) → insertD_out_gga(T82, tree(T78, T79, T80), tree(T78, T79, T83))
U5_ggga(T47, T42, T22, T48, insertD_out_gga(s(T47), T22, T48)) → pC_out_ggga(T47, T42, T22, T48)
U10_gga(T43, T42, T22, T23, T44, pC_out_ggga(T43, T42, T22, T44)) → insertD_out_gga(s(T43), tree(s(T42), T22, T23), tree(s(T42), T44, T23))
U9_gga(T31, T22, T23, T32, insertD_out_gga(0, T22, T32)) → insertD_out_gga(0, tree(s(T31), T22, T23), tree(s(T31), T32, T23))
U9_aga(T31, T22, T23, T32, insertD_out_gga(0, T22, T32)) → insertD_out_aga(0, tree(s(T31), T22, T23), tree(s(T31), T32, T23))
insertD_in_aga(s(T43), tree(s(T42), T22, T23), tree(s(T42), T44, T23)) → U10_aga(T43, T42, T22, T23, T44, pC_in_agga(T43, T42, T22, T44))
pC_in_agga(T43, T42, T22, T44) → U3_agga(T43, T42, T22, T44, lessA_in_ag(T43, T42))
lessA_in_ag(0, s(T55)) → lessA_out_ag(0, s(T55))
lessA_in_ag(s(T62), s(T61)) → U1_ag(T62, T61, lessA_in_ag(T62, T61))
U1_ag(T62, T61, lessA_out_ag(T62, T61)) → lessA_out_ag(s(T62), s(T61))
U3_agga(T43, T42, T22, T44, lessA_out_ag(T43, T42)) → pC_out_agga(T43, T42, T22, T44)
pC_in_agga(T47, T42, T22, T48) → U4_agga(T47, T42, T22, T48, lessA_in_ag(T47, T42))
U4_agga(T47, T42, T22, T48, lessA_out_ag(T47, T42)) → U5_agga(T47, T42, T22, T48, insertD_in_gga(s(T47), T22, T48))
U5_agga(T47, T42, T22, T48, insertD_out_gga(s(T47), T22, T48)) → pC_out_agga(T47, T42, T22, T48)
U10_aga(T43, T42, T22, T23, T44, pC_out_agga(T43, T42, T22, T44)) → insertD_out_aga(s(T43), tree(s(T42), T22, T23), tree(s(T42), T44, T23))
insertD_in_aga(T82, tree(T78, T79, T80), tree(T78, T79, T83)) → U11_aga(T82, T78, T79, T80, T83, pE_in_gaga(T78, T82, T80, T83))
pE_in_gaga(T78, T82, T80, T83) → U6_gaga(T78, T82, T80, T83, lessB_in_ga(T78, T82))
lessB_in_ga(0, s(T94)) → lessB_out_ga(0, s(T94))
lessB_in_ga(s(T99), s(T101)) → U2_ga(T99, T101, lessB_in_ga(T99, T101))
U2_ga(T99, T101, lessB_out_ga(T99, T101)) → lessB_out_ga(s(T99), s(T101))
U6_gaga(T78, T82, T80, T83, lessB_out_ga(T78, T82)) → pE_out_gaga(T78, T82, T80, T83)
pE_in_gaga(T78, T86, T80, T87) → U7_gaga(T78, T86, T80, T87, lessB_in_ga(T78, T86))
U7_gaga(T78, T86, T80, T87, lessB_out_ga(T78, T86)) → U8_gaga(T78, T86, T80, T87, insertD_in_aga(T86, T80, T87))
insertD_in_aga(s(T124), tree(0, T113, T114), tree(0, T113, T123)) → U12_aga(T124, T113, T114, T123, insertD_in_aga(s(T124), T114, T123))
insertD_in_aga(s(T133), tree(s(T131), T113, T114), tree(s(T131), T113, T134)) → U13_aga(T133, T131, T113, T114, T134, lessB_in_ga(T131, T133))
U13_aga(T133, T131, T113, T114, T134, lessB_out_ga(T131, T133)) → insertD_out_aga(s(T133), tree(s(T131), T113, T114), tree(s(T131), T113, T134))
insertD_in_aga(s(T137), tree(s(T131), T113, T114), tree(s(T131), T113, T138)) → U14_aga(T137, T131, T113, T114, T138, lessB_in_ga(T131, T137))
U14_aga(T137, T131, T113, T114, T138, lessB_out_ga(T131, T137)) → U15_aga(T137, T131, T113, T114, T138, insertD_in_aga(s(T137), T114, T138))
insertD_in_aga(0, tree(s(T161), T152, T153), tree(s(T161), T162, T153)) → U16_aga(T161, T152, T153, T162, insertD_in_gga(0, T152, T162))
U16_aga(T161, T152, T153, T162, insertD_out_gga(0, T152, T162)) → insertD_out_aga(0, tree(s(T161), T152, T153), tree(s(T161), T162, T153))
insertD_in_aga(s(T173), tree(s(T172), T152, T153), tree(s(T172), T174, T153)) → U17_aga(T173, T172, T152, T153, T174, pC_in_agga(T173, T172, T152, T174))
U17_aga(T173, T172, T152, T153, T174, pC_out_agga(T173, T172, T152, T174)) → insertD_out_aga(s(T173), tree(s(T172), T152, T153), tree(s(T172), T174, T153))
insertD_in_aga(T192, tree(T188, T189, T190), tree(T188, T189, T193)) → U18_aga(T192, T188, T189, T190, T193, pE_in_gaga(T188, T192, T190, T193))
U18_aga(T192, T188, T189, T190, T193, pE_out_gaga(T188, T192, T190, T193)) → insertD_out_aga(T192, tree(T188, T189, T190), tree(T188, T189, T193))
insertD_in_aga(s(T214), tree(0, T203, T204), tree(0, T203, T213)) → U19_aga(T214, T203, T204, T213, insertD_in_aga(s(T214), T204, T213))
insertD_in_aga(s(T223), tree(s(T221), T203, T204), tree(s(T221), T203, T224)) → U20_aga(T223, T221, T203, T204, T224, lessB_in_ga(T221, T223))
U20_aga(T223, T221, T203, T204, T224, lessB_out_ga(T221, T223)) → insertD_out_aga(s(T223), tree(s(T221), T203, T204), tree(s(T221), T203, T224))
insertD_in_aga(s(T227), tree(s(T221), T203, T204), tree(s(T221), T203, T228)) → U21_aga(T227, T221, T203, T204, T228, lessB_in_ga(T221, T227))
U21_aga(T227, T221, T203, T204, T228, lessB_out_ga(T221, T227)) → U22_aga(T227, T221, T203, T204, T228, insertD_in_aga(s(T227), T204, T228))
U22_aga(T227, T221, T203, T204, T228, insertD_out_aga(s(T227), T204, T228)) → insertD_out_aga(s(T227), tree(s(T221), T203, T204), tree(s(T221), T203, T228))
U19_aga(T214, T203, T204, T213, insertD_out_aga(s(T214), T204, T213)) → insertD_out_aga(s(T214), tree(0, T203, T204), tree(0, T203, T213))
U15_aga(T137, T131, T113, T114, T138, insertD_out_aga(s(T137), T114, T138)) → insertD_out_aga(s(T137), tree(s(T131), T113, T114), tree(s(T131), T113, T138))
U12_aga(T124, T113, T114, T123, insertD_out_aga(s(T124), T114, T123)) → insertD_out_aga(s(T124), tree(0, T113, T114), tree(0, T113, T123))
U8_gaga(T78, T86, T80, T87, insertD_out_aga(T86, T80, T87)) → pE_out_gaga(T78, T86, T80, T87)
U11_aga(T82, T78, T79, T80, T83, pE_out_gaga(T78, T82, T80, T83)) → insertD_out_aga(T82, tree(T78, T79, T80), tree(T78, T79, T83))
INSERTD_IN_AGA(T82, tree(T78, T79, T80), tree(T78, T79, T83)) → PE_IN_GAGA(T78, T82, T80, T83)
PE_IN_GAGA(T78, T86, T80, T87) → U7_GAGA(T78, T86, T80, T87, lessB_in_ga(T78, T86))
U7_GAGA(T78, T86, T80, T87, lessB_out_ga(T78, T86)) → INSERTD_IN_AGA(T86, T80, T87)
INSERTD_IN_AGA(s(T124), tree(0, T113, T114), tree(0, T113, T123)) → INSERTD_IN_AGA(s(T124), T114, T123)
INSERTD_IN_AGA(s(T137), tree(s(T131), T113, T114), tree(s(T131), T113, T138)) → U14_AGA(T137, T131, T113, T114, T138, lessB_in_ga(T131, T137))
U14_AGA(T137, T131, T113, T114, T138, lessB_out_ga(T131, T137)) → INSERTD_IN_AGA(s(T137), T114, T138)
INSERTD_IN_AGA(s(T227), tree(s(T221), T203, T204), tree(s(T221), T203, T228)) → U21_AGA(T227, T221, T203, T204, T228, lessB_in_ga(T221, T227))
U21_AGA(T227, T221, T203, T204, T228, lessB_out_ga(T221, T227)) → INSERTD_IN_AGA(s(T227), T204, T228)
lessB_in_ga(0, s(T94)) → lessB_out_ga(0, s(T94))
lessB_in_ga(s(T99), s(T101)) → U2_ga(T99, T101, lessB_in_ga(T99, T101))
U2_ga(T99, T101, lessB_out_ga(T99, T101)) → lessB_out_ga(s(T99), s(T101))
INSERTD_IN_AGA(tree(T78, T79, T80)) → PE_IN_GAGA(T78, T80)
PE_IN_GAGA(T78, T80) → U7_GAGA(T78, T80, lessB_in_ga(T78))
U7_GAGA(T78, T80, lessB_out_ga(T78)) → INSERTD_IN_AGA(T80)
INSERTD_IN_AGA(tree(0, T113, T114)) → INSERTD_IN_AGA(T114)
INSERTD_IN_AGA(tree(s(T131), T113, T114)) → U14_AGA(T131, T113, T114, lessB_in_ga(T131))
U14_AGA(T131, T113, T114, lessB_out_ga(T131)) → INSERTD_IN_AGA(T114)
INSERTD_IN_AGA(tree(s(T221), T203, T204)) → U21_AGA(T221, T203, T204, lessB_in_ga(T221))
U21_AGA(T221, T203, T204, lessB_out_ga(T221)) → INSERTD_IN_AGA(T204)
lessB_in_ga(0) → lessB_out_ga(0)
lessB_in_ga(s(T99)) → U2_ga(T99, lessB_in_ga(T99))
U2_ga(T99, lessB_out_ga(T99)) → lessB_out_ga(s(T99))
lessB_in_ga(x0)
U2_ga(x0, x1)
From the DPs we obtained the following set of size-change graphs: