0 Prolog
↳1 PrologToPiTRSViaGraphTransformerProof (⇒, 436 ms)
↳2 PiTRS
↳3 DependencyPairsProof (⇔, 801 ms)
↳4 PiDP
↳5 DependencyGraphProof (⇔, 24 ms)
↳6 AND
↳7 PiDP
↳8 UsableRulesProof (⇔, 0 ms)
↳9 PiDP
↳10 PiDPToQDPProof (⇔, 0 ms)
↳11 QDP
↳12 QDPSizeChangeProof (⇔, 0 ms)
↳13 YES
↳14 PiDP
↳15 UsableRulesProof (⇔, 0 ms)
↳16 PiDP
↳17 PiDPToQDPProof (⇔, 0 ms)
↳18 QDP
↳19 QDPSizeChangeProof (⇔, 0 ms)
↳20 YES
↳21 PiDP
↳22 UsableRulesProof (⇔, 0 ms)
↳23 PiDP
↳24 PiDPToQDPProof (⇒, 0 ms)
↳25 QDP
↳26 QDPSizeChangeProof (⇔, 0 ms)
↳27 YES
↳28 PiDP
↳29 UsableRulesProof (⇔, 0 ms)
↳30 PiDP
↳31 PiDPToQDPProof (⇒, 0 ms)
↳32 QDP
↳33 QDPSizeChangeProof (⇔, 0 ms)
↳34 YES
↳35 PiDP
↳36 UsableRulesProof (⇔, 0 ms)
↳37 PiDP
↳38 PiDPToQDPProof (⇒, 11 ms)
↳39 QDP
↳40 Rewriting (⇔, 289 ms)
↳41 QDP
↳42 Rewriting (⇔, 0 ms)
↳43 QDP
↳44 QDPOrderProof (⇔, 2214 ms)
↳45 QDP
↳46 DependencyGraphProof (⇔, 0 ms)
↳47 TRUE
↳48 PiDP
↳49 UsableRulesProof (⇔, 0 ms)
↳50 PiDP
↳51 PiDPToQDPProof (⇒, 1 ms)
↳52 QDP
↳53 Rewriting (⇔, 0 ms)
↳54 QDP
↳55 UsableRulesProof (⇔, 0 ms)
↳56 QDP
↳57 QReductionProof (⇔, 0 ms)
↳58 QDP
↳59 QDPOrderProof (⇔, 0 ms)
↳60 QDP
↳61 DependencyGraphProof (⇔, 0 ms)
↳62 TRUE
mergesortA_in_gaa([], [], T5) → mergesortA_out_gaa([], [], T5)
mergesortA_in_gaa(.(T8, []), .(T8, []), T9) → mergesortA_out_gaa(.(T8, []), .(T8, []), T9)
mergesortA_in_gaa(.(T39, .(T40, T41)), T45, .(T46, T44)) → U1_gaa(T39, T40, T41, T45, T46, T44, pB_in_ggaaagaaaa(T40, T41, X63, X62, T44, T39, X35, X36, T45, T46))
pB_in_ggaaagaaaa(T40, T41, T47, T48, T49, T39, X35, X36, T50, T51) → U13_ggaaagaaaa(T40, T41, T47, T48, T49, T39, X35, X36, T50, T51, splitD_in_ggaaa(T40, T41, T47, T48, T49))
splitD_in_ggaaa(T60, T61, .(T60, X91), X92, .(T62, T64)) → U3_ggaaa(T60, T61, X91, X92, T62, T64, splitC_in_gaaa(T61, X92, X91, T64))
splitC_in_gaaa([], [], [], T71) → splitC_out_gaaa([], [], [], T71)
splitC_in_gaaa(.(T80, T81), .(T80, X122), X123, .(T82, T84)) → U2_gaaa(T80, T81, X122, X123, T82, T84, splitC_in_gaaa(T81, X123, X122, T84))
U2_gaaa(T80, T81, X122, X123, T82, T84, splitC_out_gaaa(T81, X123, X122, T84)) → splitC_out_gaaa(.(T80, T81), .(T80, X122), X123, .(T82, T84))
U3_ggaaa(T60, T61, X91, X92, T62, T64, splitC_out_gaaa(T61, X92, X91, T64)) → splitD_out_ggaaa(T60, T61, .(T60, X91), X92, .(T62, T64))
U13_ggaaagaaaa(T40, T41, T47, T48, T49, T39, X35, X36, T50, T51, splitD_out_ggaaa(T40, T41, T47, T48, T49)) → U14_ggaaagaaaa(T40, T41, T47, T48, T49, T39, X35, X36, T50, T51, pN_in_ggaagaaa(T39, T48, X35, T49, T47, X36, T50, T51))
pN_in_ggaagaaa(T39, T48, T87, T88, T47, X36, T89, T90) → U15_ggaagaaa(T39, T48, T87, T88, T47, X36, T89, T90, mergesortA_in_gaa(.(T39, T48), T87, T88))
U15_ggaagaaa(T39, T48, T87, T88, T47, X36, T89, T90, mergesortA_out_gaa(.(T39, T48), T87, T88)) → U16_ggaagaaa(T39, T48, T87, T88, T47, X36, T89, T90, pO_in_gaagaa(T47, X36, T88, T87, T89, T90))
pO_in_gaagaa(T47, T93, T96, T87, T94, T95) → U17_gaagaa(T47, T93, T96, T87, T94, T95, mergesortE_in_gaa(T47, T93, T96))
mergesortE_in_gaa([], [], T103) → mergesortE_out_gaa([], [], T103)
mergesortE_in_gaa(.(T112, []), .(T112, []), T113) → mergesortE_out_gaa(.(T112, []), .(T112, []), T113)
mergesortE_in_gaa(.(T124, .(T125, T126)), X177, .(T129, T130)) → U4_gaa(T124, T125, T126, X177, T129, T130, pF_in_gggaaaaaaa(T124, T125, T126, X173, X174, T129, T130, X175, X176, X177))
pF_in_gggaaaaaaa(T124, T125, T126, T131, T132, T134, T133, X175, X176, X177) → U19_gggaaaaaaa(T124, T125, T126, T131, T132, T134, T133, X175, X176, X177, splitD_in_ggaaa(T124, .(T125, T126), T131, T132, .(T134, T133)))
U19_gggaaaaaaa(T124, T125, T126, T131, T132, T134, T133, X175, X176, X177, splitD_out_ggaaa(T124, .(T125, T126), T131, T132, .(T134, T133))) → U20_gggaaaaaaa(T124, T125, T126, T131, T132, T134, T133, X175, X176, X177, pP_in_gaagaaa(T131, X175, T133, T132, X176, X177, T134))
pP_in_gaagaaa(T131, T137, T138, T132, X176, X177, T139) → U21_gaagaaa(T131, T137, T138, T132, X176, X177, T139, mergesortE_in_gaa(T131, T137, T138))
U21_gaagaaa(T131, T137, T138, T132, X176, X177, T139, mergesortE_out_gaa(T131, T137, T138)) → U22_gaagaaa(T131, T137, T138, T132, X176, X177, T139, pQ_in_gaagaa(T132, X176, T138, T137, X177, T139))
pQ_in_gaagaa(T132, T144, T146, T137, X177, T145) → U23_gaagaa(T132, T144, T146, T137, X177, T145, mergesortE_in_gaa(T132, T144, T146))
U23_gaagaa(T132, T144, T146, T137, X177, T145, mergesortE_out_gaa(T132, T144, T146)) → U24_gaagaa(T132, T144, T146, T137, X177, T145, mergeG_in_ggaaa(T137, T144, X177, T145, T146))
mergeG_in_ggaaa([], T173, T173, T174, T175) → mergeG_out_ggaaa([], T173, T173, T174, T175)
mergeG_in_ggaaa(T188, [], T188, T189, T190) → mergeG_out_ggaaa(T188, [], T188, T189, T190)
mergeG_in_ggaaa(.(T219, T220), .(T221, T222), .(T219, T226), T224, T227) → U5_ggaaa(T219, T220, T221, T222, T226, T224, T227, pH_in_ggggaa(T219, T221, T220, T222, T226, T227))
pH_in_ggggaa(T219, T221, T220, T222, T226, T227) → U25_ggggaa(T219, T221, T220, T222, T226, T227, leJ_in_gg(T219, T221))
leJ_in_gg(s(T240), s(T241)) → U7_gg(T240, T241, leJ_in_gg(T240, T241))
leJ_in_gg(0, s(0)) → leJ_out_gg(0, s(0))
leJ_in_gg(0, 0) → leJ_out_gg(0, 0)
U7_gg(T240, T241, leJ_out_gg(T240, T241)) → leJ_out_gg(s(T240), s(T241))
U25_ggggaa(T219, T221, T220, T222, T226, T227, leJ_out_gg(T219, T221)) → U26_ggggaa(T219, T221, T220, T222, T226, T227, mergeL_in_gggaa(T220, T221, T222, T226, T227))
mergeL_in_gggaa([], T262, T263, .(T262, T263), T264) → mergeL_out_gggaa([], T262, T263, .(T262, T263), T264)
mergeL_in_gggaa(.(T294, T295), T296, T297, .(T294, T301), .(T299, T302)) → U9_gggaa(T294, T295, T296, T297, T301, T299, T302, pH_in_ggggaa(T294, T296, T295, T297, T301, T302))
U9_gggaa(T294, T295, T296, T297, T301, T299, T302, pH_out_ggggaa(T294, T296, T295, T297, T301, T302)) → mergeL_out_gggaa(.(T294, T295), T296, T297, .(T294, T301), .(T299, T302))
mergeL_in_gggaa(.(T319, T320), T321, T322, .(T321, T326), .(T324, T327)) → U10_gggaa(T319, T320, T321, T322, T326, T324, T327, pI_in_ggggaa(T319, T321, T320, T322, T326, T327))
pI_in_ggggaa(T319, T321, T320, T322, T326, T327) → U27_ggggaa(T319, T321, T320, T322, T326, T327, gtK_in_gg(T319, T321))
gtK_in_gg(s(T340), s(T341)) → U8_gg(T340, T341, gtK_in_gg(T340, T341))
gtK_in_gg(s(0), 0) → gtK_out_gg(s(0), 0)
U8_gg(T340, T341, gtK_out_gg(T340, T341)) → gtK_out_gg(s(T340), s(T341))
U27_ggggaa(T319, T321, T320, T322, T326, T327, gtK_out_gg(T319, T321)) → U28_ggggaa(T319, T321, T320, T322, T326, T327, mergeM_in_gggaa(T319, T320, T322, T326, T327))
mergeM_in_gggaa(T356, T357, [], .(T356, T357), T358) → mergeM_out_gggaa(T356, T357, [], .(T356, T357), T358)
mergeM_in_gggaa(T387, T388, .(T389, T390), .(T387, T394), .(T392, T395)) → U11_gggaa(T387, T388, T389, T390, T394, T392, T395, pH_in_ggggaa(T387, T389, T388, T390, T394, T395))
U11_gggaa(T387, T388, T389, T390, T394, T392, T395, pH_out_ggggaa(T387, T389, T388, T390, T394, T395)) → mergeM_out_gggaa(T387, T388, .(T389, T390), .(T387, T394), .(T392, T395))
mergeM_in_gggaa(T412, T413, .(T414, T415), .(T414, T419), .(T417, T420)) → U12_gggaa(T412, T413, T414, T415, T419, T417, T420, pI_in_ggggaa(T412, T414, T413, T415, T419, T420))
U12_gggaa(T412, T413, T414, T415, T419, T417, T420, pI_out_ggggaa(T412, T414, T413, T415, T419, T420)) → mergeM_out_gggaa(T412, T413, .(T414, T415), .(T414, T419), .(T417, T420))
U28_ggggaa(T319, T321, T320, T322, T326, T327, mergeM_out_gggaa(T319, T320, T322, T326, T327)) → pI_out_ggggaa(T319, T321, T320, T322, T326, T327)
U10_gggaa(T319, T320, T321, T322, T326, T324, T327, pI_out_ggggaa(T319, T321, T320, T322, T326, T327)) → mergeL_out_gggaa(.(T319, T320), T321, T322, .(T321, T326), .(T324, T327))
U26_ggggaa(T219, T221, T220, T222, T226, T227, mergeL_out_gggaa(T220, T221, T222, T226, T227)) → pH_out_ggggaa(T219, T221, T220, T222, T226, T227)
U5_ggaaa(T219, T220, T221, T222, T226, T224, T227, pH_out_ggggaa(T219, T221, T220, T222, T226, T227)) → mergeG_out_ggaaa(.(T219, T220), .(T221, T222), .(T219, T226), T224, T227)
mergeG_in_ggaaa(.(T437, T438), .(T439, T440), .(T439, T444), T442, T445) → U6_ggaaa(T437, T438, T439, T440, T444, T442, T445, pI_in_ggggaa(T437, T439, T438, T440, T444, T445))
U6_ggaaa(T437, T438, T439, T440, T444, T442, T445, pI_out_ggggaa(T437, T439, T438, T440, T444, T445)) → mergeG_out_ggaaa(.(T437, T438), .(T439, T440), .(T439, T444), T442, T445)
U24_gaagaa(T132, T144, T146, T137, X177, T145, mergeG_out_ggaaa(T137, T144, X177, T145, T146)) → pQ_out_gaagaa(T132, T144, T146, T137, X177, T145)
U22_gaagaaa(T131, T137, T138, T132, X176, X177, T139, pQ_out_gaagaa(T132, X176, T138, T137, X177, T139)) → pP_out_gaagaaa(T131, T137, T138, T132, X176, X177, T139)
U20_gggaaaaaaa(T124, T125, T126, T131, T132, T134, T133, X175, X176, X177, pP_out_gaagaaa(T131, X175, T133, T132, X176, X177, T134)) → pF_out_gggaaaaaaa(T124, T125, T126, T131, T132, T134, T133, X175, X176, X177)
U4_gaa(T124, T125, T126, X177, T129, T130, pF_out_gggaaaaaaa(T124, T125, T126, X173, X174, T129, T130, X175, X176, X177)) → mergesortE_out_gaa(.(T124, .(T125, T126)), X177, .(T129, T130))
U17_gaagaa(T47, T93, T96, T87, T94, T95, mergesortE_out_gaa(T47, T93, T96)) → U18_gaagaa(T47, T93, T96, T87, T94, T95, mergeG_in_ggaaa(T87, T93, T94, T95, T96))
U18_gaagaa(T47, T93, T96, T87, T94, T95, mergeG_out_ggaaa(T87, T93, T94, T95, T96)) → pO_out_gaagaa(T47, T93, T96, T87, T94, T95)
U16_ggaagaaa(T39, T48, T87, T88, T47, X36, T89, T90, pO_out_gaagaa(T47, X36, T88, T87, T89, T90)) → pN_out_ggaagaaa(T39, T48, T87, T88, T47, X36, T89, T90)
U14_ggaaagaaaa(T40, T41, T47, T48, T49, T39, X35, X36, T50, T51, pN_out_ggaagaaa(T39, T48, X35, T49, T47, X36, T50, T51)) → pB_out_ggaaagaaaa(T40, T41, T47, T48, T49, T39, X35, X36, T50, T51)
U1_gaa(T39, T40, T41, T45, T46, T44, pB_out_ggaaagaaaa(T40, T41, X63, X62, T44, T39, X35, X36, T45, T46)) → mergesortA_out_gaa(.(T39, .(T40, T41)), T45, .(T46, T44))
MERGESORTA_IN_GAA(.(T39, .(T40, T41)), T45, .(T46, T44)) → U1_GAA(T39, T40, T41, T45, T46, T44, pB_in_ggaaagaaaa(T40, T41, X63, X62, T44, T39, X35, X36, T45, T46))
MERGESORTA_IN_GAA(.(T39, .(T40, T41)), T45, .(T46, T44)) → PB_IN_GGAAAGAAAA(T40, T41, X63, X62, T44, T39, X35, X36, T45, T46)
PB_IN_GGAAAGAAAA(T40, T41, T47, T48, T49, T39, X35, X36, T50, T51) → U13_GGAAAGAAAA(T40, T41, T47, T48, T49, T39, X35, X36, T50, T51, splitD_in_ggaaa(T40, T41, T47, T48, T49))
PB_IN_GGAAAGAAAA(T40, T41, T47, T48, T49, T39, X35, X36, T50, T51) → SPLITD_IN_GGAAA(T40, T41, T47, T48, T49)
SPLITD_IN_GGAAA(T60, T61, .(T60, X91), X92, .(T62, T64)) → U3_GGAAA(T60, T61, X91, X92, T62, T64, splitC_in_gaaa(T61, X92, X91, T64))
SPLITD_IN_GGAAA(T60, T61, .(T60, X91), X92, .(T62, T64)) → SPLITC_IN_GAAA(T61, X92, X91, T64)
SPLITC_IN_GAAA(.(T80, T81), .(T80, X122), X123, .(T82, T84)) → U2_GAAA(T80, T81, X122, X123, T82, T84, splitC_in_gaaa(T81, X123, X122, T84))
SPLITC_IN_GAAA(.(T80, T81), .(T80, X122), X123, .(T82, T84)) → SPLITC_IN_GAAA(T81, X123, X122, T84)
U13_GGAAAGAAAA(T40, T41, T47, T48, T49, T39, X35, X36, T50, T51, splitD_out_ggaaa(T40, T41, T47, T48, T49)) → U14_GGAAAGAAAA(T40, T41, T47, T48, T49, T39, X35, X36, T50, T51, pN_in_ggaagaaa(T39, T48, X35, T49, T47, X36, T50, T51))
U13_GGAAAGAAAA(T40, T41, T47, T48, T49, T39, X35, X36, T50, T51, splitD_out_ggaaa(T40, T41, T47, T48, T49)) → PN_IN_GGAAGAAA(T39, T48, X35, T49, T47, X36, T50, T51)
PN_IN_GGAAGAAA(T39, T48, T87, T88, T47, X36, T89, T90) → U15_GGAAGAAA(T39, T48, T87, T88, T47, X36, T89, T90, mergesortA_in_gaa(.(T39, T48), T87, T88))
PN_IN_GGAAGAAA(T39, T48, T87, T88, T47, X36, T89, T90) → MERGESORTA_IN_GAA(.(T39, T48), T87, T88)
U15_GGAAGAAA(T39, T48, T87, T88, T47, X36, T89, T90, mergesortA_out_gaa(.(T39, T48), T87, T88)) → U16_GGAAGAAA(T39, T48, T87, T88, T47, X36, T89, T90, pO_in_gaagaa(T47, X36, T88, T87, T89, T90))
U15_GGAAGAAA(T39, T48, T87, T88, T47, X36, T89, T90, mergesortA_out_gaa(.(T39, T48), T87, T88)) → PO_IN_GAAGAA(T47, X36, T88, T87, T89, T90)
PO_IN_GAAGAA(T47, T93, T96, T87, T94, T95) → U17_GAAGAA(T47, T93, T96, T87, T94, T95, mergesortE_in_gaa(T47, T93, T96))
PO_IN_GAAGAA(T47, T93, T96, T87, T94, T95) → MERGESORTE_IN_GAA(T47, T93, T96)
MERGESORTE_IN_GAA(.(T124, .(T125, T126)), X177, .(T129, T130)) → U4_GAA(T124, T125, T126, X177, T129, T130, pF_in_gggaaaaaaa(T124, T125, T126, X173, X174, T129, T130, X175, X176, X177))
MERGESORTE_IN_GAA(.(T124, .(T125, T126)), X177, .(T129, T130)) → PF_IN_GGGAAAAAAA(T124, T125, T126, X173, X174, T129, T130, X175, X176, X177)
PF_IN_GGGAAAAAAA(T124, T125, T126, T131, T132, T134, T133, X175, X176, X177) → U19_GGGAAAAAAA(T124, T125, T126, T131, T132, T134, T133, X175, X176, X177, splitD_in_ggaaa(T124, .(T125, T126), T131, T132, .(T134, T133)))
PF_IN_GGGAAAAAAA(T124, T125, T126, T131, T132, T134, T133, X175, X176, X177) → SPLITD_IN_GGAAA(T124, .(T125, T126), T131, T132, .(T134, T133))
U19_GGGAAAAAAA(T124, T125, T126, T131, T132, T134, T133, X175, X176, X177, splitD_out_ggaaa(T124, .(T125, T126), T131, T132, .(T134, T133))) → U20_GGGAAAAAAA(T124, T125, T126, T131, T132, T134, T133, X175, X176, X177, pP_in_gaagaaa(T131, X175, T133, T132, X176, X177, T134))
U19_GGGAAAAAAA(T124, T125, T126, T131, T132, T134, T133, X175, X176, X177, splitD_out_ggaaa(T124, .(T125, T126), T131, T132, .(T134, T133))) → PP_IN_GAAGAAA(T131, X175, T133, T132, X176, X177, T134)
PP_IN_GAAGAAA(T131, T137, T138, T132, X176, X177, T139) → U21_GAAGAAA(T131, T137, T138, T132, X176, X177, T139, mergesortE_in_gaa(T131, T137, T138))
PP_IN_GAAGAAA(T131, T137, T138, T132, X176, X177, T139) → MERGESORTE_IN_GAA(T131, T137, T138)
U21_GAAGAAA(T131, T137, T138, T132, X176, X177, T139, mergesortE_out_gaa(T131, T137, T138)) → U22_GAAGAAA(T131, T137, T138, T132, X176, X177, T139, pQ_in_gaagaa(T132, X176, T138, T137, X177, T139))
U21_GAAGAAA(T131, T137, T138, T132, X176, X177, T139, mergesortE_out_gaa(T131, T137, T138)) → PQ_IN_GAAGAA(T132, X176, T138, T137, X177, T139)
PQ_IN_GAAGAA(T132, T144, T146, T137, X177, T145) → U23_GAAGAA(T132, T144, T146, T137, X177, T145, mergesortE_in_gaa(T132, T144, T146))
PQ_IN_GAAGAA(T132, T144, T146, T137, X177, T145) → MERGESORTE_IN_GAA(T132, T144, T146)
U23_GAAGAA(T132, T144, T146, T137, X177, T145, mergesortE_out_gaa(T132, T144, T146)) → U24_GAAGAA(T132, T144, T146, T137, X177, T145, mergeG_in_ggaaa(T137, T144, X177, T145, T146))
U23_GAAGAA(T132, T144, T146, T137, X177, T145, mergesortE_out_gaa(T132, T144, T146)) → MERGEG_IN_GGAAA(T137, T144, X177, T145, T146)
MERGEG_IN_GGAAA(.(T219, T220), .(T221, T222), .(T219, T226), T224, T227) → U5_GGAAA(T219, T220, T221, T222, T226, T224, T227, pH_in_ggggaa(T219, T221, T220, T222, T226, T227))
MERGEG_IN_GGAAA(.(T219, T220), .(T221, T222), .(T219, T226), T224, T227) → PH_IN_GGGGAA(T219, T221, T220, T222, T226, T227)
PH_IN_GGGGAA(T219, T221, T220, T222, T226, T227) → U25_GGGGAA(T219, T221, T220, T222, T226, T227, leJ_in_gg(T219, T221))
PH_IN_GGGGAA(T219, T221, T220, T222, T226, T227) → LEJ_IN_GG(T219, T221)
LEJ_IN_GG(s(T240), s(T241)) → U7_GG(T240, T241, leJ_in_gg(T240, T241))
LEJ_IN_GG(s(T240), s(T241)) → LEJ_IN_GG(T240, T241)
U25_GGGGAA(T219, T221, T220, T222, T226, T227, leJ_out_gg(T219, T221)) → U26_GGGGAA(T219, T221, T220, T222, T226, T227, mergeL_in_gggaa(T220, T221, T222, T226, T227))
U25_GGGGAA(T219, T221, T220, T222, T226, T227, leJ_out_gg(T219, T221)) → MERGEL_IN_GGGAA(T220, T221, T222, T226, T227)
MERGEL_IN_GGGAA(.(T294, T295), T296, T297, .(T294, T301), .(T299, T302)) → U9_GGGAA(T294, T295, T296, T297, T301, T299, T302, pH_in_ggggaa(T294, T296, T295, T297, T301, T302))
MERGEL_IN_GGGAA(.(T294, T295), T296, T297, .(T294, T301), .(T299, T302)) → PH_IN_GGGGAA(T294, T296, T295, T297, T301, T302)
MERGEL_IN_GGGAA(.(T319, T320), T321, T322, .(T321, T326), .(T324, T327)) → U10_GGGAA(T319, T320, T321, T322, T326, T324, T327, pI_in_ggggaa(T319, T321, T320, T322, T326, T327))
MERGEL_IN_GGGAA(.(T319, T320), T321, T322, .(T321, T326), .(T324, T327)) → PI_IN_GGGGAA(T319, T321, T320, T322, T326, T327)
PI_IN_GGGGAA(T319, T321, T320, T322, T326, T327) → U27_GGGGAA(T319, T321, T320, T322, T326, T327, gtK_in_gg(T319, T321))
PI_IN_GGGGAA(T319, T321, T320, T322, T326, T327) → GTK_IN_GG(T319, T321)
GTK_IN_GG(s(T340), s(T341)) → U8_GG(T340, T341, gtK_in_gg(T340, T341))
GTK_IN_GG(s(T340), s(T341)) → GTK_IN_GG(T340, T341)
U27_GGGGAA(T319, T321, T320, T322, T326, T327, gtK_out_gg(T319, T321)) → U28_GGGGAA(T319, T321, T320, T322, T326, T327, mergeM_in_gggaa(T319, T320, T322, T326, T327))
U27_GGGGAA(T319, T321, T320, T322, T326, T327, gtK_out_gg(T319, T321)) → MERGEM_IN_GGGAA(T319, T320, T322, T326, T327)
MERGEM_IN_GGGAA(T387, T388, .(T389, T390), .(T387, T394), .(T392, T395)) → U11_GGGAA(T387, T388, T389, T390, T394, T392, T395, pH_in_ggggaa(T387, T389, T388, T390, T394, T395))
MERGEM_IN_GGGAA(T387, T388, .(T389, T390), .(T387, T394), .(T392, T395)) → PH_IN_GGGGAA(T387, T389, T388, T390, T394, T395)
MERGEM_IN_GGGAA(T412, T413, .(T414, T415), .(T414, T419), .(T417, T420)) → U12_GGGAA(T412, T413, T414, T415, T419, T417, T420, pI_in_ggggaa(T412, T414, T413, T415, T419, T420))
MERGEM_IN_GGGAA(T412, T413, .(T414, T415), .(T414, T419), .(T417, T420)) → PI_IN_GGGGAA(T412, T414, T413, T415, T419, T420)
MERGEG_IN_GGAAA(.(T437, T438), .(T439, T440), .(T439, T444), T442, T445) → U6_GGAAA(T437, T438, T439, T440, T444, T442, T445, pI_in_ggggaa(T437, T439, T438, T440, T444, T445))
MERGEG_IN_GGAAA(.(T437, T438), .(T439, T440), .(T439, T444), T442, T445) → PI_IN_GGGGAA(T437, T439, T438, T440, T444, T445)
U17_GAAGAA(T47, T93, T96, T87, T94, T95, mergesortE_out_gaa(T47, T93, T96)) → U18_GAAGAA(T47, T93, T96, T87, T94, T95, mergeG_in_ggaaa(T87, T93, T94, T95, T96))
U17_GAAGAA(T47, T93, T96, T87, T94, T95, mergesortE_out_gaa(T47, T93, T96)) → MERGEG_IN_GGAAA(T87, T93, T94, T95, T96)
mergesortA_in_gaa([], [], T5) → mergesortA_out_gaa([], [], T5)
mergesortA_in_gaa(.(T8, []), .(T8, []), T9) → mergesortA_out_gaa(.(T8, []), .(T8, []), T9)
mergesortA_in_gaa(.(T39, .(T40, T41)), T45, .(T46, T44)) → U1_gaa(T39, T40, T41, T45, T46, T44, pB_in_ggaaagaaaa(T40, T41, X63, X62, T44, T39, X35, X36, T45, T46))
pB_in_ggaaagaaaa(T40, T41, T47, T48, T49, T39, X35, X36, T50, T51) → U13_ggaaagaaaa(T40, T41, T47, T48, T49, T39, X35, X36, T50, T51, splitD_in_ggaaa(T40, T41, T47, T48, T49))
splitD_in_ggaaa(T60, T61, .(T60, X91), X92, .(T62, T64)) → U3_ggaaa(T60, T61, X91, X92, T62, T64, splitC_in_gaaa(T61, X92, X91, T64))
splitC_in_gaaa([], [], [], T71) → splitC_out_gaaa([], [], [], T71)
splitC_in_gaaa(.(T80, T81), .(T80, X122), X123, .(T82, T84)) → U2_gaaa(T80, T81, X122, X123, T82, T84, splitC_in_gaaa(T81, X123, X122, T84))
U2_gaaa(T80, T81, X122, X123, T82, T84, splitC_out_gaaa(T81, X123, X122, T84)) → splitC_out_gaaa(.(T80, T81), .(T80, X122), X123, .(T82, T84))
U3_ggaaa(T60, T61, X91, X92, T62, T64, splitC_out_gaaa(T61, X92, X91, T64)) → splitD_out_ggaaa(T60, T61, .(T60, X91), X92, .(T62, T64))
U13_ggaaagaaaa(T40, T41, T47, T48, T49, T39, X35, X36, T50, T51, splitD_out_ggaaa(T40, T41, T47, T48, T49)) → U14_ggaaagaaaa(T40, T41, T47, T48, T49, T39, X35, X36, T50, T51, pN_in_ggaagaaa(T39, T48, X35, T49, T47, X36, T50, T51))
pN_in_ggaagaaa(T39, T48, T87, T88, T47, X36, T89, T90) → U15_ggaagaaa(T39, T48, T87, T88, T47, X36, T89, T90, mergesortA_in_gaa(.(T39, T48), T87, T88))
U15_ggaagaaa(T39, T48, T87, T88, T47, X36, T89, T90, mergesortA_out_gaa(.(T39, T48), T87, T88)) → U16_ggaagaaa(T39, T48, T87, T88, T47, X36, T89, T90, pO_in_gaagaa(T47, X36, T88, T87, T89, T90))
pO_in_gaagaa(T47, T93, T96, T87, T94, T95) → U17_gaagaa(T47, T93, T96, T87, T94, T95, mergesortE_in_gaa(T47, T93, T96))
mergesortE_in_gaa([], [], T103) → mergesortE_out_gaa([], [], T103)
mergesortE_in_gaa(.(T112, []), .(T112, []), T113) → mergesortE_out_gaa(.(T112, []), .(T112, []), T113)
mergesortE_in_gaa(.(T124, .(T125, T126)), X177, .(T129, T130)) → U4_gaa(T124, T125, T126, X177, T129, T130, pF_in_gggaaaaaaa(T124, T125, T126, X173, X174, T129, T130, X175, X176, X177))
pF_in_gggaaaaaaa(T124, T125, T126, T131, T132, T134, T133, X175, X176, X177) → U19_gggaaaaaaa(T124, T125, T126, T131, T132, T134, T133, X175, X176, X177, splitD_in_ggaaa(T124, .(T125, T126), T131, T132, .(T134, T133)))
U19_gggaaaaaaa(T124, T125, T126, T131, T132, T134, T133, X175, X176, X177, splitD_out_ggaaa(T124, .(T125, T126), T131, T132, .(T134, T133))) → U20_gggaaaaaaa(T124, T125, T126, T131, T132, T134, T133, X175, X176, X177, pP_in_gaagaaa(T131, X175, T133, T132, X176, X177, T134))
pP_in_gaagaaa(T131, T137, T138, T132, X176, X177, T139) → U21_gaagaaa(T131, T137, T138, T132, X176, X177, T139, mergesortE_in_gaa(T131, T137, T138))
U21_gaagaaa(T131, T137, T138, T132, X176, X177, T139, mergesortE_out_gaa(T131, T137, T138)) → U22_gaagaaa(T131, T137, T138, T132, X176, X177, T139, pQ_in_gaagaa(T132, X176, T138, T137, X177, T139))
pQ_in_gaagaa(T132, T144, T146, T137, X177, T145) → U23_gaagaa(T132, T144, T146, T137, X177, T145, mergesortE_in_gaa(T132, T144, T146))
U23_gaagaa(T132, T144, T146, T137, X177, T145, mergesortE_out_gaa(T132, T144, T146)) → U24_gaagaa(T132, T144, T146, T137, X177, T145, mergeG_in_ggaaa(T137, T144, X177, T145, T146))
mergeG_in_ggaaa([], T173, T173, T174, T175) → mergeG_out_ggaaa([], T173, T173, T174, T175)
mergeG_in_ggaaa(T188, [], T188, T189, T190) → mergeG_out_ggaaa(T188, [], T188, T189, T190)
mergeG_in_ggaaa(.(T219, T220), .(T221, T222), .(T219, T226), T224, T227) → U5_ggaaa(T219, T220, T221, T222, T226, T224, T227, pH_in_ggggaa(T219, T221, T220, T222, T226, T227))
pH_in_ggggaa(T219, T221, T220, T222, T226, T227) → U25_ggggaa(T219, T221, T220, T222, T226, T227, leJ_in_gg(T219, T221))
leJ_in_gg(s(T240), s(T241)) → U7_gg(T240, T241, leJ_in_gg(T240, T241))
leJ_in_gg(0, s(0)) → leJ_out_gg(0, s(0))
leJ_in_gg(0, 0) → leJ_out_gg(0, 0)
U7_gg(T240, T241, leJ_out_gg(T240, T241)) → leJ_out_gg(s(T240), s(T241))
U25_ggggaa(T219, T221, T220, T222, T226, T227, leJ_out_gg(T219, T221)) → U26_ggggaa(T219, T221, T220, T222, T226, T227, mergeL_in_gggaa(T220, T221, T222, T226, T227))
mergeL_in_gggaa([], T262, T263, .(T262, T263), T264) → mergeL_out_gggaa([], T262, T263, .(T262, T263), T264)
mergeL_in_gggaa(.(T294, T295), T296, T297, .(T294, T301), .(T299, T302)) → U9_gggaa(T294, T295, T296, T297, T301, T299, T302, pH_in_ggggaa(T294, T296, T295, T297, T301, T302))
U9_gggaa(T294, T295, T296, T297, T301, T299, T302, pH_out_ggggaa(T294, T296, T295, T297, T301, T302)) → mergeL_out_gggaa(.(T294, T295), T296, T297, .(T294, T301), .(T299, T302))
mergeL_in_gggaa(.(T319, T320), T321, T322, .(T321, T326), .(T324, T327)) → U10_gggaa(T319, T320, T321, T322, T326, T324, T327, pI_in_ggggaa(T319, T321, T320, T322, T326, T327))
pI_in_ggggaa(T319, T321, T320, T322, T326, T327) → U27_ggggaa(T319, T321, T320, T322, T326, T327, gtK_in_gg(T319, T321))
gtK_in_gg(s(T340), s(T341)) → U8_gg(T340, T341, gtK_in_gg(T340, T341))
gtK_in_gg(s(0), 0) → gtK_out_gg(s(0), 0)
U8_gg(T340, T341, gtK_out_gg(T340, T341)) → gtK_out_gg(s(T340), s(T341))
U27_ggggaa(T319, T321, T320, T322, T326, T327, gtK_out_gg(T319, T321)) → U28_ggggaa(T319, T321, T320, T322, T326, T327, mergeM_in_gggaa(T319, T320, T322, T326, T327))
mergeM_in_gggaa(T356, T357, [], .(T356, T357), T358) → mergeM_out_gggaa(T356, T357, [], .(T356, T357), T358)
mergeM_in_gggaa(T387, T388, .(T389, T390), .(T387, T394), .(T392, T395)) → U11_gggaa(T387, T388, T389, T390, T394, T392, T395, pH_in_ggggaa(T387, T389, T388, T390, T394, T395))
U11_gggaa(T387, T388, T389, T390, T394, T392, T395, pH_out_ggggaa(T387, T389, T388, T390, T394, T395)) → mergeM_out_gggaa(T387, T388, .(T389, T390), .(T387, T394), .(T392, T395))
mergeM_in_gggaa(T412, T413, .(T414, T415), .(T414, T419), .(T417, T420)) → U12_gggaa(T412, T413, T414, T415, T419, T417, T420, pI_in_ggggaa(T412, T414, T413, T415, T419, T420))
U12_gggaa(T412, T413, T414, T415, T419, T417, T420, pI_out_ggggaa(T412, T414, T413, T415, T419, T420)) → mergeM_out_gggaa(T412, T413, .(T414, T415), .(T414, T419), .(T417, T420))
U28_ggggaa(T319, T321, T320, T322, T326, T327, mergeM_out_gggaa(T319, T320, T322, T326, T327)) → pI_out_ggggaa(T319, T321, T320, T322, T326, T327)
U10_gggaa(T319, T320, T321, T322, T326, T324, T327, pI_out_ggggaa(T319, T321, T320, T322, T326, T327)) → mergeL_out_gggaa(.(T319, T320), T321, T322, .(T321, T326), .(T324, T327))
U26_ggggaa(T219, T221, T220, T222, T226, T227, mergeL_out_gggaa(T220, T221, T222, T226, T227)) → pH_out_ggggaa(T219, T221, T220, T222, T226, T227)
U5_ggaaa(T219, T220, T221, T222, T226, T224, T227, pH_out_ggggaa(T219, T221, T220, T222, T226, T227)) → mergeG_out_ggaaa(.(T219, T220), .(T221, T222), .(T219, T226), T224, T227)
mergeG_in_ggaaa(.(T437, T438), .(T439, T440), .(T439, T444), T442, T445) → U6_ggaaa(T437, T438, T439, T440, T444, T442, T445, pI_in_ggggaa(T437, T439, T438, T440, T444, T445))
U6_ggaaa(T437, T438, T439, T440, T444, T442, T445, pI_out_ggggaa(T437, T439, T438, T440, T444, T445)) → mergeG_out_ggaaa(.(T437, T438), .(T439, T440), .(T439, T444), T442, T445)
U24_gaagaa(T132, T144, T146, T137, X177, T145, mergeG_out_ggaaa(T137, T144, X177, T145, T146)) → pQ_out_gaagaa(T132, T144, T146, T137, X177, T145)
U22_gaagaaa(T131, T137, T138, T132, X176, X177, T139, pQ_out_gaagaa(T132, X176, T138, T137, X177, T139)) → pP_out_gaagaaa(T131, T137, T138, T132, X176, X177, T139)
U20_gggaaaaaaa(T124, T125, T126, T131, T132, T134, T133, X175, X176, X177, pP_out_gaagaaa(T131, X175, T133, T132, X176, X177, T134)) → pF_out_gggaaaaaaa(T124, T125, T126, T131, T132, T134, T133, X175, X176, X177)
U4_gaa(T124, T125, T126, X177, T129, T130, pF_out_gggaaaaaaa(T124, T125, T126, X173, X174, T129, T130, X175, X176, X177)) → mergesortE_out_gaa(.(T124, .(T125, T126)), X177, .(T129, T130))
U17_gaagaa(T47, T93, T96, T87, T94, T95, mergesortE_out_gaa(T47, T93, T96)) → U18_gaagaa(T47, T93, T96, T87, T94, T95, mergeG_in_ggaaa(T87, T93, T94, T95, T96))
U18_gaagaa(T47, T93, T96, T87, T94, T95, mergeG_out_ggaaa(T87, T93, T94, T95, T96)) → pO_out_gaagaa(T47, T93, T96, T87, T94, T95)
U16_ggaagaaa(T39, T48, T87, T88, T47, X36, T89, T90, pO_out_gaagaa(T47, X36, T88, T87, T89, T90)) → pN_out_ggaagaaa(T39, T48, T87, T88, T47, X36, T89, T90)
U14_ggaaagaaaa(T40, T41, T47, T48, T49, T39, X35, X36, T50, T51, pN_out_ggaagaaa(T39, T48, X35, T49, T47, X36, T50, T51)) → pB_out_ggaaagaaaa(T40, T41, T47, T48, T49, T39, X35, X36, T50, T51)
U1_gaa(T39, T40, T41, T45, T46, T44, pB_out_ggaaagaaaa(T40, T41, X63, X62, T44, T39, X35, X36, T45, T46)) → mergesortA_out_gaa(.(T39, .(T40, T41)), T45, .(T46, T44))
MERGESORTA_IN_GAA(.(T39, .(T40, T41)), T45, .(T46, T44)) → U1_GAA(T39, T40, T41, T45, T46, T44, pB_in_ggaaagaaaa(T40, T41, X63, X62, T44, T39, X35, X36, T45, T46))
MERGESORTA_IN_GAA(.(T39, .(T40, T41)), T45, .(T46, T44)) → PB_IN_GGAAAGAAAA(T40, T41, X63, X62, T44, T39, X35, X36, T45, T46)
PB_IN_GGAAAGAAAA(T40, T41, T47, T48, T49, T39, X35, X36, T50, T51) → U13_GGAAAGAAAA(T40, T41, T47, T48, T49, T39, X35, X36, T50, T51, splitD_in_ggaaa(T40, T41, T47, T48, T49))
PB_IN_GGAAAGAAAA(T40, T41, T47, T48, T49, T39, X35, X36, T50, T51) → SPLITD_IN_GGAAA(T40, T41, T47, T48, T49)
SPLITD_IN_GGAAA(T60, T61, .(T60, X91), X92, .(T62, T64)) → U3_GGAAA(T60, T61, X91, X92, T62, T64, splitC_in_gaaa(T61, X92, X91, T64))
SPLITD_IN_GGAAA(T60, T61, .(T60, X91), X92, .(T62, T64)) → SPLITC_IN_GAAA(T61, X92, X91, T64)
SPLITC_IN_GAAA(.(T80, T81), .(T80, X122), X123, .(T82, T84)) → U2_GAAA(T80, T81, X122, X123, T82, T84, splitC_in_gaaa(T81, X123, X122, T84))
SPLITC_IN_GAAA(.(T80, T81), .(T80, X122), X123, .(T82, T84)) → SPLITC_IN_GAAA(T81, X123, X122, T84)
U13_GGAAAGAAAA(T40, T41, T47, T48, T49, T39, X35, X36, T50, T51, splitD_out_ggaaa(T40, T41, T47, T48, T49)) → U14_GGAAAGAAAA(T40, T41, T47, T48, T49, T39, X35, X36, T50, T51, pN_in_ggaagaaa(T39, T48, X35, T49, T47, X36, T50, T51))
U13_GGAAAGAAAA(T40, T41, T47, T48, T49, T39, X35, X36, T50, T51, splitD_out_ggaaa(T40, T41, T47, T48, T49)) → PN_IN_GGAAGAAA(T39, T48, X35, T49, T47, X36, T50, T51)
PN_IN_GGAAGAAA(T39, T48, T87, T88, T47, X36, T89, T90) → U15_GGAAGAAA(T39, T48, T87, T88, T47, X36, T89, T90, mergesortA_in_gaa(.(T39, T48), T87, T88))
PN_IN_GGAAGAAA(T39, T48, T87, T88, T47, X36, T89, T90) → MERGESORTA_IN_GAA(.(T39, T48), T87, T88)
U15_GGAAGAAA(T39, T48, T87, T88, T47, X36, T89, T90, mergesortA_out_gaa(.(T39, T48), T87, T88)) → U16_GGAAGAAA(T39, T48, T87, T88, T47, X36, T89, T90, pO_in_gaagaa(T47, X36, T88, T87, T89, T90))
U15_GGAAGAAA(T39, T48, T87, T88, T47, X36, T89, T90, mergesortA_out_gaa(.(T39, T48), T87, T88)) → PO_IN_GAAGAA(T47, X36, T88, T87, T89, T90)
PO_IN_GAAGAA(T47, T93, T96, T87, T94, T95) → U17_GAAGAA(T47, T93, T96, T87, T94, T95, mergesortE_in_gaa(T47, T93, T96))
PO_IN_GAAGAA(T47, T93, T96, T87, T94, T95) → MERGESORTE_IN_GAA(T47, T93, T96)
MERGESORTE_IN_GAA(.(T124, .(T125, T126)), X177, .(T129, T130)) → U4_GAA(T124, T125, T126, X177, T129, T130, pF_in_gggaaaaaaa(T124, T125, T126, X173, X174, T129, T130, X175, X176, X177))
MERGESORTE_IN_GAA(.(T124, .(T125, T126)), X177, .(T129, T130)) → PF_IN_GGGAAAAAAA(T124, T125, T126, X173, X174, T129, T130, X175, X176, X177)
PF_IN_GGGAAAAAAA(T124, T125, T126, T131, T132, T134, T133, X175, X176, X177) → U19_GGGAAAAAAA(T124, T125, T126, T131, T132, T134, T133, X175, X176, X177, splitD_in_ggaaa(T124, .(T125, T126), T131, T132, .(T134, T133)))
PF_IN_GGGAAAAAAA(T124, T125, T126, T131, T132, T134, T133, X175, X176, X177) → SPLITD_IN_GGAAA(T124, .(T125, T126), T131, T132, .(T134, T133))
U19_GGGAAAAAAA(T124, T125, T126, T131, T132, T134, T133, X175, X176, X177, splitD_out_ggaaa(T124, .(T125, T126), T131, T132, .(T134, T133))) → U20_GGGAAAAAAA(T124, T125, T126, T131, T132, T134, T133, X175, X176, X177, pP_in_gaagaaa(T131, X175, T133, T132, X176, X177, T134))
U19_GGGAAAAAAA(T124, T125, T126, T131, T132, T134, T133, X175, X176, X177, splitD_out_ggaaa(T124, .(T125, T126), T131, T132, .(T134, T133))) → PP_IN_GAAGAAA(T131, X175, T133, T132, X176, X177, T134)
PP_IN_GAAGAAA(T131, T137, T138, T132, X176, X177, T139) → U21_GAAGAAA(T131, T137, T138, T132, X176, X177, T139, mergesortE_in_gaa(T131, T137, T138))
PP_IN_GAAGAAA(T131, T137, T138, T132, X176, X177, T139) → MERGESORTE_IN_GAA(T131, T137, T138)
U21_GAAGAAA(T131, T137, T138, T132, X176, X177, T139, mergesortE_out_gaa(T131, T137, T138)) → U22_GAAGAAA(T131, T137, T138, T132, X176, X177, T139, pQ_in_gaagaa(T132, X176, T138, T137, X177, T139))
U21_GAAGAAA(T131, T137, T138, T132, X176, X177, T139, mergesortE_out_gaa(T131, T137, T138)) → PQ_IN_GAAGAA(T132, X176, T138, T137, X177, T139)
PQ_IN_GAAGAA(T132, T144, T146, T137, X177, T145) → U23_GAAGAA(T132, T144, T146, T137, X177, T145, mergesortE_in_gaa(T132, T144, T146))
PQ_IN_GAAGAA(T132, T144, T146, T137, X177, T145) → MERGESORTE_IN_GAA(T132, T144, T146)
U23_GAAGAA(T132, T144, T146, T137, X177, T145, mergesortE_out_gaa(T132, T144, T146)) → U24_GAAGAA(T132, T144, T146, T137, X177, T145, mergeG_in_ggaaa(T137, T144, X177, T145, T146))
U23_GAAGAA(T132, T144, T146, T137, X177, T145, mergesortE_out_gaa(T132, T144, T146)) → MERGEG_IN_GGAAA(T137, T144, X177, T145, T146)
MERGEG_IN_GGAAA(.(T219, T220), .(T221, T222), .(T219, T226), T224, T227) → U5_GGAAA(T219, T220, T221, T222, T226, T224, T227, pH_in_ggggaa(T219, T221, T220, T222, T226, T227))
MERGEG_IN_GGAAA(.(T219, T220), .(T221, T222), .(T219, T226), T224, T227) → PH_IN_GGGGAA(T219, T221, T220, T222, T226, T227)
PH_IN_GGGGAA(T219, T221, T220, T222, T226, T227) → U25_GGGGAA(T219, T221, T220, T222, T226, T227, leJ_in_gg(T219, T221))
PH_IN_GGGGAA(T219, T221, T220, T222, T226, T227) → LEJ_IN_GG(T219, T221)
LEJ_IN_GG(s(T240), s(T241)) → U7_GG(T240, T241, leJ_in_gg(T240, T241))
LEJ_IN_GG(s(T240), s(T241)) → LEJ_IN_GG(T240, T241)
U25_GGGGAA(T219, T221, T220, T222, T226, T227, leJ_out_gg(T219, T221)) → U26_GGGGAA(T219, T221, T220, T222, T226, T227, mergeL_in_gggaa(T220, T221, T222, T226, T227))
U25_GGGGAA(T219, T221, T220, T222, T226, T227, leJ_out_gg(T219, T221)) → MERGEL_IN_GGGAA(T220, T221, T222, T226, T227)
MERGEL_IN_GGGAA(.(T294, T295), T296, T297, .(T294, T301), .(T299, T302)) → U9_GGGAA(T294, T295, T296, T297, T301, T299, T302, pH_in_ggggaa(T294, T296, T295, T297, T301, T302))
MERGEL_IN_GGGAA(.(T294, T295), T296, T297, .(T294, T301), .(T299, T302)) → PH_IN_GGGGAA(T294, T296, T295, T297, T301, T302)
MERGEL_IN_GGGAA(.(T319, T320), T321, T322, .(T321, T326), .(T324, T327)) → U10_GGGAA(T319, T320, T321, T322, T326, T324, T327, pI_in_ggggaa(T319, T321, T320, T322, T326, T327))
MERGEL_IN_GGGAA(.(T319, T320), T321, T322, .(T321, T326), .(T324, T327)) → PI_IN_GGGGAA(T319, T321, T320, T322, T326, T327)
PI_IN_GGGGAA(T319, T321, T320, T322, T326, T327) → U27_GGGGAA(T319, T321, T320, T322, T326, T327, gtK_in_gg(T319, T321))
PI_IN_GGGGAA(T319, T321, T320, T322, T326, T327) → GTK_IN_GG(T319, T321)
GTK_IN_GG(s(T340), s(T341)) → U8_GG(T340, T341, gtK_in_gg(T340, T341))
GTK_IN_GG(s(T340), s(T341)) → GTK_IN_GG(T340, T341)
U27_GGGGAA(T319, T321, T320, T322, T326, T327, gtK_out_gg(T319, T321)) → U28_GGGGAA(T319, T321, T320, T322, T326, T327, mergeM_in_gggaa(T319, T320, T322, T326, T327))
U27_GGGGAA(T319, T321, T320, T322, T326, T327, gtK_out_gg(T319, T321)) → MERGEM_IN_GGGAA(T319, T320, T322, T326, T327)
MERGEM_IN_GGGAA(T387, T388, .(T389, T390), .(T387, T394), .(T392, T395)) → U11_GGGAA(T387, T388, T389, T390, T394, T392, T395, pH_in_ggggaa(T387, T389, T388, T390, T394, T395))
MERGEM_IN_GGGAA(T387, T388, .(T389, T390), .(T387, T394), .(T392, T395)) → PH_IN_GGGGAA(T387, T389, T388, T390, T394, T395)
MERGEM_IN_GGGAA(T412, T413, .(T414, T415), .(T414, T419), .(T417, T420)) → U12_GGGAA(T412, T413, T414, T415, T419, T417, T420, pI_in_ggggaa(T412, T414, T413, T415, T419, T420))
MERGEM_IN_GGGAA(T412, T413, .(T414, T415), .(T414, T419), .(T417, T420)) → PI_IN_GGGGAA(T412, T414, T413, T415, T419, T420)
MERGEG_IN_GGAAA(.(T437, T438), .(T439, T440), .(T439, T444), T442, T445) → U6_GGAAA(T437, T438, T439, T440, T444, T442, T445, pI_in_ggggaa(T437, T439, T438, T440, T444, T445))
MERGEG_IN_GGAAA(.(T437, T438), .(T439, T440), .(T439, T444), T442, T445) → PI_IN_GGGGAA(T437, T439, T438, T440, T444, T445)
U17_GAAGAA(T47, T93, T96, T87, T94, T95, mergesortE_out_gaa(T47, T93, T96)) → U18_GAAGAA(T47, T93, T96, T87, T94, T95, mergeG_in_ggaaa(T87, T93, T94, T95, T96))
U17_GAAGAA(T47, T93, T96, T87, T94, T95, mergesortE_out_gaa(T47, T93, T96)) → MERGEG_IN_GGAAA(T87, T93, T94, T95, T96)
mergesortA_in_gaa([], [], T5) → mergesortA_out_gaa([], [], T5)
mergesortA_in_gaa(.(T8, []), .(T8, []), T9) → mergesortA_out_gaa(.(T8, []), .(T8, []), T9)
mergesortA_in_gaa(.(T39, .(T40, T41)), T45, .(T46, T44)) → U1_gaa(T39, T40, T41, T45, T46, T44, pB_in_ggaaagaaaa(T40, T41, X63, X62, T44, T39, X35, X36, T45, T46))
pB_in_ggaaagaaaa(T40, T41, T47, T48, T49, T39, X35, X36, T50, T51) → U13_ggaaagaaaa(T40, T41, T47, T48, T49, T39, X35, X36, T50, T51, splitD_in_ggaaa(T40, T41, T47, T48, T49))
splitD_in_ggaaa(T60, T61, .(T60, X91), X92, .(T62, T64)) → U3_ggaaa(T60, T61, X91, X92, T62, T64, splitC_in_gaaa(T61, X92, X91, T64))
splitC_in_gaaa([], [], [], T71) → splitC_out_gaaa([], [], [], T71)
splitC_in_gaaa(.(T80, T81), .(T80, X122), X123, .(T82, T84)) → U2_gaaa(T80, T81, X122, X123, T82, T84, splitC_in_gaaa(T81, X123, X122, T84))
U2_gaaa(T80, T81, X122, X123, T82, T84, splitC_out_gaaa(T81, X123, X122, T84)) → splitC_out_gaaa(.(T80, T81), .(T80, X122), X123, .(T82, T84))
U3_ggaaa(T60, T61, X91, X92, T62, T64, splitC_out_gaaa(T61, X92, X91, T64)) → splitD_out_ggaaa(T60, T61, .(T60, X91), X92, .(T62, T64))
U13_ggaaagaaaa(T40, T41, T47, T48, T49, T39, X35, X36, T50, T51, splitD_out_ggaaa(T40, T41, T47, T48, T49)) → U14_ggaaagaaaa(T40, T41, T47, T48, T49, T39, X35, X36, T50, T51, pN_in_ggaagaaa(T39, T48, X35, T49, T47, X36, T50, T51))
pN_in_ggaagaaa(T39, T48, T87, T88, T47, X36, T89, T90) → U15_ggaagaaa(T39, T48, T87, T88, T47, X36, T89, T90, mergesortA_in_gaa(.(T39, T48), T87, T88))
U15_ggaagaaa(T39, T48, T87, T88, T47, X36, T89, T90, mergesortA_out_gaa(.(T39, T48), T87, T88)) → U16_ggaagaaa(T39, T48, T87, T88, T47, X36, T89, T90, pO_in_gaagaa(T47, X36, T88, T87, T89, T90))
pO_in_gaagaa(T47, T93, T96, T87, T94, T95) → U17_gaagaa(T47, T93, T96, T87, T94, T95, mergesortE_in_gaa(T47, T93, T96))
mergesortE_in_gaa([], [], T103) → mergesortE_out_gaa([], [], T103)
mergesortE_in_gaa(.(T112, []), .(T112, []), T113) → mergesortE_out_gaa(.(T112, []), .(T112, []), T113)
mergesortE_in_gaa(.(T124, .(T125, T126)), X177, .(T129, T130)) → U4_gaa(T124, T125, T126, X177, T129, T130, pF_in_gggaaaaaaa(T124, T125, T126, X173, X174, T129, T130, X175, X176, X177))
pF_in_gggaaaaaaa(T124, T125, T126, T131, T132, T134, T133, X175, X176, X177) → U19_gggaaaaaaa(T124, T125, T126, T131, T132, T134, T133, X175, X176, X177, splitD_in_ggaaa(T124, .(T125, T126), T131, T132, .(T134, T133)))
U19_gggaaaaaaa(T124, T125, T126, T131, T132, T134, T133, X175, X176, X177, splitD_out_ggaaa(T124, .(T125, T126), T131, T132, .(T134, T133))) → U20_gggaaaaaaa(T124, T125, T126, T131, T132, T134, T133, X175, X176, X177, pP_in_gaagaaa(T131, X175, T133, T132, X176, X177, T134))
pP_in_gaagaaa(T131, T137, T138, T132, X176, X177, T139) → U21_gaagaaa(T131, T137, T138, T132, X176, X177, T139, mergesortE_in_gaa(T131, T137, T138))
U21_gaagaaa(T131, T137, T138, T132, X176, X177, T139, mergesortE_out_gaa(T131, T137, T138)) → U22_gaagaaa(T131, T137, T138, T132, X176, X177, T139, pQ_in_gaagaa(T132, X176, T138, T137, X177, T139))
pQ_in_gaagaa(T132, T144, T146, T137, X177, T145) → U23_gaagaa(T132, T144, T146, T137, X177, T145, mergesortE_in_gaa(T132, T144, T146))
U23_gaagaa(T132, T144, T146, T137, X177, T145, mergesortE_out_gaa(T132, T144, T146)) → U24_gaagaa(T132, T144, T146, T137, X177, T145, mergeG_in_ggaaa(T137, T144, X177, T145, T146))
mergeG_in_ggaaa([], T173, T173, T174, T175) → mergeG_out_ggaaa([], T173, T173, T174, T175)
mergeG_in_ggaaa(T188, [], T188, T189, T190) → mergeG_out_ggaaa(T188, [], T188, T189, T190)
mergeG_in_ggaaa(.(T219, T220), .(T221, T222), .(T219, T226), T224, T227) → U5_ggaaa(T219, T220, T221, T222, T226, T224, T227, pH_in_ggggaa(T219, T221, T220, T222, T226, T227))
pH_in_ggggaa(T219, T221, T220, T222, T226, T227) → U25_ggggaa(T219, T221, T220, T222, T226, T227, leJ_in_gg(T219, T221))
leJ_in_gg(s(T240), s(T241)) → U7_gg(T240, T241, leJ_in_gg(T240, T241))
leJ_in_gg(0, s(0)) → leJ_out_gg(0, s(0))
leJ_in_gg(0, 0) → leJ_out_gg(0, 0)
U7_gg(T240, T241, leJ_out_gg(T240, T241)) → leJ_out_gg(s(T240), s(T241))
U25_ggggaa(T219, T221, T220, T222, T226, T227, leJ_out_gg(T219, T221)) → U26_ggggaa(T219, T221, T220, T222, T226, T227, mergeL_in_gggaa(T220, T221, T222, T226, T227))
mergeL_in_gggaa([], T262, T263, .(T262, T263), T264) → mergeL_out_gggaa([], T262, T263, .(T262, T263), T264)
mergeL_in_gggaa(.(T294, T295), T296, T297, .(T294, T301), .(T299, T302)) → U9_gggaa(T294, T295, T296, T297, T301, T299, T302, pH_in_ggggaa(T294, T296, T295, T297, T301, T302))
U9_gggaa(T294, T295, T296, T297, T301, T299, T302, pH_out_ggggaa(T294, T296, T295, T297, T301, T302)) → mergeL_out_gggaa(.(T294, T295), T296, T297, .(T294, T301), .(T299, T302))
mergeL_in_gggaa(.(T319, T320), T321, T322, .(T321, T326), .(T324, T327)) → U10_gggaa(T319, T320, T321, T322, T326, T324, T327, pI_in_ggggaa(T319, T321, T320, T322, T326, T327))
pI_in_ggggaa(T319, T321, T320, T322, T326, T327) → U27_ggggaa(T319, T321, T320, T322, T326, T327, gtK_in_gg(T319, T321))
gtK_in_gg(s(T340), s(T341)) → U8_gg(T340, T341, gtK_in_gg(T340, T341))
gtK_in_gg(s(0), 0) → gtK_out_gg(s(0), 0)
U8_gg(T340, T341, gtK_out_gg(T340, T341)) → gtK_out_gg(s(T340), s(T341))
U27_ggggaa(T319, T321, T320, T322, T326, T327, gtK_out_gg(T319, T321)) → U28_ggggaa(T319, T321, T320, T322, T326, T327, mergeM_in_gggaa(T319, T320, T322, T326, T327))
mergeM_in_gggaa(T356, T357, [], .(T356, T357), T358) → mergeM_out_gggaa(T356, T357, [], .(T356, T357), T358)
mergeM_in_gggaa(T387, T388, .(T389, T390), .(T387, T394), .(T392, T395)) → U11_gggaa(T387, T388, T389, T390, T394, T392, T395, pH_in_ggggaa(T387, T389, T388, T390, T394, T395))
U11_gggaa(T387, T388, T389, T390, T394, T392, T395, pH_out_ggggaa(T387, T389, T388, T390, T394, T395)) → mergeM_out_gggaa(T387, T388, .(T389, T390), .(T387, T394), .(T392, T395))
mergeM_in_gggaa(T412, T413, .(T414, T415), .(T414, T419), .(T417, T420)) → U12_gggaa(T412, T413, T414, T415, T419, T417, T420, pI_in_ggggaa(T412, T414, T413, T415, T419, T420))
U12_gggaa(T412, T413, T414, T415, T419, T417, T420, pI_out_ggggaa(T412, T414, T413, T415, T419, T420)) → mergeM_out_gggaa(T412, T413, .(T414, T415), .(T414, T419), .(T417, T420))
U28_ggggaa(T319, T321, T320, T322, T326, T327, mergeM_out_gggaa(T319, T320, T322, T326, T327)) → pI_out_ggggaa(T319, T321, T320, T322, T326, T327)
U10_gggaa(T319, T320, T321, T322, T326, T324, T327, pI_out_ggggaa(T319, T321, T320, T322, T326, T327)) → mergeL_out_gggaa(.(T319, T320), T321, T322, .(T321, T326), .(T324, T327))
U26_ggggaa(T219, T221, T220, T222, T226, T227, mergeL_out_gggaa(T220, T221, T222, T226, T227)) → pH_out_ggggaa(T219, T221, T220, T222, T226, T227)
U5_ggaaa(T219, T220, T221, T222, T226, T224, T227, pH_out_ggggaa(T219, T221, T220, T222, T226, T227)) → mergeG_out_ggaaa(.(T219, T220), .(T221, T222), .(T219, T226), T224, T227)
mergeG_in_ggaaa(.(T437, T438), .(T439, T440), .(T439, T444), T442, T445) → U6_ggaaa(T437, T438, T439, T440, T444, T442, T445, pI_in_ggggaa(T437, T439, T438, T440, T444, T445))
U6_ggaaa(T437, T438, T439, T440, T444, T442, T445, pI_out_ggggaa(T437, T439, T438, T440, T444, T445)) → mergeG_out_ggaaa(.(T437, T438), .(T439, T440), .(T439, T444), T442, T445)
U24_gaagaa(T132, T144, T146, T137, X177, T145, mergeG_out_ggaaa(T137, T144, X177, T145, T146)) → pQ_out_gaagaa(T132, T144, T146, T137, X177, T145)
U22_gaagaaa(T131, T137, T138, T132, X176, X177, T139, pQ_out_gaagaa(T132, X176, T138, T137, X177, T139)) → pP_out_gaagaaa(T131, T137, T138, T132, X176, X177, T139)
U20_gggaaaaaaa(T124, T125, T126, T131, T132, T134, T133, X175, X176, X177, pP_out_gaagaaa(T131, X175, T133, T132, X176, X177, T134)) → pF_out_gggaaaaaaa(T124, T125, T126, T131, T132, T134, T133, X175, X176, X177)
U4_gaa(T124, T125, T126, X177, T129, T130, pF_out_gggaaaaaaa(T124, T125, T126, X173, X174, T129, T130, X175, X176, X177)) → mergesortE_out_gaa(.(T124, .(T125, T126)), X177, .(T129, T130))
U17_gaagaa(T47, T93, T96, T87, T94, T95, mergesortE_out_gaa(T47, T93, T96)) → U18_gaagaa(T47, T93, T96, T87, T94, T95, mergeG_in_ggaaa(T87, T93, T94, T95, T96))
U18_gaagaa(T47, T93, T96, T87, T94, T95, mergeG_out_ggaaa(T87, T93, T94, T95, T96)) → pO_out_gaagaa(T47, T93, T96, T87, T94, T95)
U16_ggaagaaa(T39, T48, T87, T88, T47, X36, T89, T90, pO_out_gaagaa(T47, X36, T88, T87, T89, T90)) → pN_out_ggaagaaa(T39, T48, T87, T88, T47, X36, T89, T90)
U14_ggaaagaaaa(T40, T41, T47, T48, T49, T39, X35, X36, T50, T51, pN_out_ggaagaaa(T39, T48, X35, T49, T47, X36, T50, T51)) → pB_out_ggaaagaaaa(T40, T41, T47, T48, T49, T39, X35, X36, T50, T51)
U1_gaa(T39, T40, T41, T45, T46, T44, pB_out_ggaaagaaaa(T40, T41, X63, X62, T44, T39, X35, X36, T45, T46)) → mergesortA_out_gaa(.(T39, .(T40, T41)), T45, .(T46, T44))
GTK_IN_GG(s(T340), s(T341)) → GTK_IN_GG(T340, T341)
mergesortA_in_gaa([], [], T5) → mergesortA_out_gaa([], [], T5)
mergesortA_in_gaa(.(T8, []), .(T8, []), T9) → mergesortA_out_gaa(.(T8, []), .(T8, []), T9)
mergesortA_in_gaa(.(T39, .(T40, T41)), T45, .(T46, T44)) → U1_gaa(T39, T40, T41, T45, T46, T44, pB_in_ggaaagaaaa(T40, T41, X63, X62, T44, T39, X35, X36, T45, T46))
pB_in_ggaaagaaaa(T40, T41, T47, T48, T49, T39, X35, X36, T50, T51) → U13_ggaaagaaaa(T40, T41, T47, T48, T49, T39, X35, X36, T50, T51, splitD_in_ggaaa(T40, T41, T47, T48, T49))
splitD_in_ggaaa(T60, T61, .(T60, X91), X92, .(T62, T64)) → U3_ggaaa(T60, T61, X91, X92, T62, T64, splitC_in_gaaa(T61, X92, X91, T64))
splitC_in_gaaa([], [], [], T71) → splitC_out_gaaa([], [], [], T71)
splitC_in_gaaa(.(T80, T81), .(T80, X122), X123, .(T82, T84)) → U2_gaaa(T80, T81, X122, X123, T82, T84, splitC_in_gaaa(T81, X123, X122, T84))
U2_gaaa(T80, T81, X122, X123, T82, T84, splitC_out_gaaa(T81, X123, X122, T84)) → splitC_out_gaaa(.(T80, T81), .(T80, X122), X123, .(T82, T84))
U3_ggaaa(T60, T61, X91, X92, T62, T64, splitC_out_gaaa(T61, X92, X91, T64)) → splitD_out_ggaaa(T60, T61, .(T60, X91), X92, .(T62, T64))
U13_ggaaagaaaa(T40, T41, T47, T48, T49, T39, X35, X36, T50, T51, splitD_out_ggaaa(T40, T41, T47, T48, T49)) → U14_ggaaagaaaa(T40, T41, T47, T48, T49, T39, X35, X36, T50, T51, pN_in_ggaagaaa(T39, T48, X35, T49, T47, X36, T50, T51))
pN_in_ggaagaaa(T39, T48, T87, T88, T47, X36, T89, T90) → U15_ggaagaaa(T39, T48, T87, T88, T47, X36, T89, T90, mergesortA_in_gaa(.(T39, T48), T87, T88))
U15_ggaagaaa(T39, T48, T87, T88, T47, X36, T89, T90, mergesortA_out_gaa(.(T39, T48), T87, T88)) → U16_ggaagaaa(T39, T48, T87, T88, T47, X36, T89, T90, pO_in_gaagaa(T47, X36, T88, T87, T89, T90))
pO_in_gaagaa(T47, T93, T96, T87, T94, T95) → U17_gaagaa(T47, T93, T96, T87, T94, T95, mergesortE_in_gaa(T47, T93, T96))
mergesortE_in_gaa([], [], T103) → mergesortE_out_gaa([], [], T103)
mergesortE_in_gaa(.(T112, []), .(T112, []), T113) → mergesortE_out_gaa(.(T112, []), .(T112, []), T113)
mergesortE_in_gaa(.(T124, .(T125, T126)), X177, .(T129, T130)) → U4_gaa(T124, T125, T126, X177, T129, T130, pF_in_gggaaaaaaa(T124, T125, T126, X173, X174, T129, T130, X175, X176, X177))
pF_in_gggaaaaaaa(T124, T125, T126, T131, T132, T134, T133, X175, X176, X177) → U19_gggaaaaaaa(T124, T125, T126, T131, T132, T134, T133, X175, X176, X177, splitD_in_ggaaa(T124, .(T125, T126), T131, T132, .(T134, T133)))
U19_gggaaaaaaa(T124, T125, T126, T131, T132, T134, T133, X175, X176, X177, splitD_out_ggaaa(T124, .(T125, T126), T131, T132, .(T134, T133))) → U20_gggaaaaaaa(T124, T125, T126, T131, T132, T134, T133, X175, X176, X177, pP_in_gaagaaa(T131, X175, T133, T132, X176, X177, T134))
pP_in_gaagaaa(T131, T137, T138, T132, X176, X177, T139) → U21_gaagaaa(T131, T137, T138, T132, X176, X177, T139, mergesortE_in_gaa(T131, T137, T138))
U21_gaagaaa(T131, T137, T138, T132, X176, X177, T139, mergesortE_out_gaa(T131, T137, T138)) → U22_gaagaaa(T131, T137, T138, T132, X176, X177, T139, pQ_in_gaagaa(T132, X176, T138, T137, X177, T139))
pQ_in_gaagaa(T132, T144, T146, T137, X177, T145) → U23_gaagaa(T132, T144, T146, T137, X177, T145, mergesortE_in_gaa(T132, T144, T146))
U23_gaagaa(T132, T144, T146, T137, X177, T145, mergesortE_out_gaa(T132, T144, T146)) → U24_gaagaa(T132, T144, T146, T137, X177, T145, mergeG_in_ggaaa(T137, T144, X177, T145, T146))
mergeG_in_ggaaa([], T173, T173, T174, T175) → mergeG_out_ggaaa([], T173, T173, T174, T175)
mergeG_in_ggaaa(T188, [], T188, T189, T190) → mergeG_out_ggaaa(T188, [], T188, T189, T190)
mergeG_in_ggaaa(.(T219, T220), .(T221, T222), .(T219, T226), T224, T227) → U5_ggaaa(T219, T220, T221, T222, T226, T224, T227, pH_in_ggggaa(T219, T221, T220, T222, T226, T227))
pH_in_ggggaa(T219, T221, T220, T222, T226, T227) → U25_ggggaa(T219, T221, T220, T222, T226, T227, leJ_in_gg(T219, T221))
leJ_in_gg(s(T240), s(T241)) → U7_gg(T240, T241, leJ_in_gg(T240, T241))
leJ_in_gg(0, s(0)) → leJ_out_gg(0, s(0))
leJ_in_gg(0, 0) → leJ_out_gg(0, 0)
U7_gg(T240, T241, leJ_out_gg(T240, T241)) → leJ_out_gg(s(T240), s(T241))
U25_ggggaa(T219, T221, T220, T222, T226, T227, leJ_out_gg(T219, T221)) → U26_ggggaa(T219, T221, T220, T222, T226, T227, mergeL_in_gggaa(T220, T221, T222, T226, T227))
mergeL_in_gggaa([], T262, T263, .(T262, T263), T264) → mergeL_out_gggaa([], T262, T263, .(T262, T263), T264)
mergeL_in_gggaa(.(T294, T295), T296, T297, .(T294, T301), .(T299, T302)) → U9_gggaa(T294, T295, T296, T297, T301, T299, T302, pH_in_ggggaa(T294, T296, T295, T297, T301, T302))
U9_gggaa(T294, T295, T296, T297, T301, T299, T302, pH_out_ggggaa(T294, T296, T295, T297, T301, T302)) → mergeL_out_gggaa(.(T294, T295), T296, T297, .(T294, T301), .(T299, T302))
mergeL_in_gggaa(.(T319, T320), T321, T322, .(T321, T326), .(T324, T327)) → U10_gggaa(T319, T320, T321, T322, T326, T324, T327, pI_in_ggggaa(T319, T321, T320, T322, T326, T327))
pI_in_ggggaa(T319, T321, T320, T322, T326, T327) → U27_ggggaa(T319, T321, T320, T322, T326, T327, gtK_in_gg(T319, T321))
gtK_in_gg(s(T340), s(T341)) → U8_gg(T340, T341, gtK_in_gg(T340, T341))
gtK_in_gg(s(0), 0) → gtK_out_gg(s(0), 0)
U8_gg(T340, T341, gtK_out_gg(T340, T341)) → gtK_out_gg(s(T340), s(T341))
U27_ggggaa(T319, T321, T320, T322, T326, T327, gtK_out_gg(T319, T321)) → U28_ggggaa(T319, T321, T320, T322, T326, T327, mergeM_in_gggaa(T319, T320, T322, T326, T327))
mergeM_in_gggaa(T356, T357, [], .(T356, T357), T358) → mergeM_out_gggaa(T356, T357, [], .(T356, T357), T358)
mergeM_in_gggaa(T387, T388, .(T389, T390), .(T387, T394), .(T392, T395)) → U11_gggaa(T387, T388, T389, T390, T394, T392, T395, pH_in_ggggaa(T387, T389, T388, T390, T394, T395))
U11_gggaa(T387, T388, T389, T390, T394, T392, T395, pH_out_ggggaa(T387, T389, T388, T390, T394, T395)) → mergeM_out_gggaa(T387, T388, .(T389, T390), .(T387, T394), .(T392, T395))
mergeM_in_gggaa(T412, T413, .(T414, T415), .(T414, T419), .(T417, T420)) → U12_gggaa(T412, T413, T414, T415, T419, T417, T420, pI_in_ggggaa(T412, T414, T413, T415, T419, T420))
U12_gggaa(T412, T413, T414, T415, T419, T417, T420, pI_out_ggggaa(T412, T414, T413, T415, T419, T420)) → mergeM_out_gggaa(T412, T413, .(T414, T415), .(T414, T419), .(T417, T420))
U28_ggggaa(T319, T321, T320, T322, T326, T327, mergeM_out_gggaa(T319, T320, T322, T326, T327)) → pI_out_ggggaa(T319, T321, T320, T322, T326, T327)
U10_gggaa(T319, T320, T321, T322, T326, T324, T327, pI_out_ggggaa(T319, T321, T320, T322, T326, T327)) → mergeL_out_gggaa(.(T319, T320), T321, T322, .(T321, T326), .(T324, T327))
U26_ggggaa(T219, T221, T220, T222, T226, T227, mergeL_out_gggaa(T220, T221, T222, T226, T227)) → pH_out_ggggaa(T219, T221, T220, T222, T226, T227)
U5_ggaaa(T219, T220, T221, T222, T226, T224, T227, pH_out_ggggaa(T219, T221, T220, T222, T226, T227)) → mergeG_out_ggaaa(.(T219, T220), .(T221, T222), .(T219, T226), T224, T227)
mergeG_in_ggaaa(.(T437, T438), .(T439, T440), .(T439, T444), T442, T445) → U6_ggaaa(T437, T438, T439, T440, T444, T442, T445, pI_in_ggggaa(T437, T439, T438, T440, T444, T445))
U6_ggaaa(T437, T438, T439, T440, T444, T442, T445, pI_out_ggggaa(T437, T439, T438, T440, T444, T445)) → mergeG_out_ggaaa(.(T437, T438), .(T439, T440), .(T439, T444), T442, T445)
U24_gaagaa(T132, T144, T146, T137, X177, T145, mergeG_out_ggaaa(T137, T144, X177, T145, T146)) → pQ_out_gaagaa(T132, T144, T146, T137, X177, T145)
U22_gaagaaa(T131, T137, T138, T132, X176, X177, T139, pQ_out_gaagaa(T132, X176, T138, T137, X177, T139)) → pP_out_gaagaaa(T131, T137, T138, T132, X176, X177, T139)
U20_gggaaaaaaa(T124, T125, T126, T131, T132, T134, T133, X175, X176, X177, pP_out_gaagaaa(T131, X175, T133, T132, X176, X177, T134)) → pF_out_gggaaaaaaa(T124, T125, T126, T131, T132, T134, T133, X175, X176, X177)
U4_gaa(T124, T125, T126, X177, T129, T130, pF_out_gggaaaaaaa(T124, T125, T126, X173, X174, T129, T130, X175, X176, X177)) → mergesortE_out_gaa(.(T124, .(T125, T126)), X177, .(T129, T130))
U17_gaagaa(T47, T93, T96, T87, T94, T95, mergesortE_out_gaa(T47, T93, T96)) → U18_gaagaa(T47, T93, T96, T87, T94, T95, mergeG_in_ggaaa(T87, T93, T94, T95, T96))
U18_gaagaa(T47, T93, T96, T87, T94, T95, mergeG_out_ggaaa(T87, T93, T94, T95, T96)) → pO_out_gaagaa(T47, T93, T96, T87, T94, T95)
U16_ggaagaaa(T39, T48, T87, T88, T47, X36, T89, T90, pO_out_gaagaa(T47, X36, T88, T87, T89, T90)) → pN_out_ggaagaaa(T39, T48, T87, T88, T47, X36, T89, T90)
U14_ggaaagaaaa(T40, T41, T47, T48, T49, T39, X35, X36, T50, T51, pN_out_ggaagaaa(T39, T48, X35, T49, T47, X36, T50, T51)) → pB_out_ggaaagaaaa(T40, T41, T47, T48, T49, T39, X35, X36, T50, T51)
U1_gaa(T39, T40, T41, T45, T46, T44, pB_out_ggaaagaaaa(T40, T41, X63, X62, T44, T39, X35, X36, T45, T46)) → mergesortA_out_gaa(.(T39, .(T40, T41)), T45, .(T46, T44))
GTK_IN_GG(s(T340), s(T341)) → GTK_IN_GG(T340, T341)
GTK_IN_GG(s(T340), s(T341)) → GTK_IN_GG(T340, T341)
From the DPs we obtained the following set of size-change graphs:
LEJ_IN_GG(s(T240), s(T241)) → LEJ_IN_GG(T240, T241)
mergesortA_in_gaa([], [], T5) → mergesortA_out_gaa([], [], T5)
mergesortA_in_gaa(.(T8, []), .(T8, []), T9) → mergesortA_out_gaa(.(T8, []), .(T8, []), T9)
mergesortA_in_gaa(.(T39, .(T40, T41)), T45, .(T46, T44)) → U1_gaa(T39, T40, T41, T45, T46, T44, pB_in_ggaaagaaaa(T40, T41, X63, X62, T44, T39, X35, X36, T45, T46))
pB_in_ggaaagaaaa(T40, T41, T47, T48, T49, T39, X35, X36, T50, T51) → U13_ggaaagaaaa(T40, T41, T47, T48, T49, T39, X35, X36, T50, T51, splitD_in_ggaaa(T40, T41, T47, T48, T49))
splitD_in_ggaaa(T60, T61, .(T60, X91), X92, .(T62, T64)) → U3_ggaaa(T60, T61, X91, X92, T62, T64, splitC_in_gaaa(T61, X92, X91, T64))
splitC_in_gaaa([], [], [], T71) → splitC_out_gaaa([], [], [], T71)
splitC_in_gaaa(.(T80, T81), .(T80, X122), X123, .(T82, T84)) → U2_gaaa(T80, T81, X122, X123, T82, T84, splitC_in_gaaa(T81, X123, X122, T84))
U2_gaaa(T80, T81, X122, X123, T82, T84, splitC_out_gaaa(T81, X123, X122, T84)) → splitC_out_gaaa(.(T80, T81), .(T80, X122), X123, .(T82, T84))
U3_ggaaa(T60, T61, X91, X92, T62, T64, splitC_out_gaaa(T61, X92, X91, T64)) → splitD_out_ggaaa(T60, T61, .(T60, X91), X92, .(T62, T64))
U13_ggaaagaaaa(T40, T41, T47, T48, T49, T39, X35, X36, T50, T51, splitD_out_ggaaa(T40, T41, T47, T48, T49)) → U14_ggaaagaaaa(T40, T41, T47, T48, T49, T39, X35, X36, T50, T51, pN_in_ggaagaaa(T39, T48, X35, T49, T47, X36, T50, T51))
pN_in_ggaagaaa(T39, T48, T87, T88, T47, X36, T89, T90) → U15_ggaagaaa(T39, T48, T87, T88, T47, X36, T89, T90, mergesortA_in_gaa(.(T39, T48), T87, T88))
U15_ggaagaaa(T39, T48, T87, T88, T47, X36, T89, T90, mergesortA_out_gaa(.(T39, T48), T87, T88)) → U16_ggaagaaa(T39, T48, T87, T88, T47, X36, T89, T90, pO_in_gaagaa(T47, X36, T88, T87, T89, T90))
pO_in_gaagaa(T47, T93, T96, T87, T94, T95) → U17_gaagaa(T47, T93, T96, T87, T94, T95, mergesortE_in_gaa(T47, T93, T96))
mergesortE_in_gaa([], [], T103) → mergesortE_out_gaa([], [], T103)
mergesortE_in_gaa(.(T112, []), .(T112, []), T113) → mergesortE_out_gaa(.(T112, []), .(T112, []), T113)
mergesortE_in_gaa(.(T124, .(T125, T126)), X177, .(T129, T130)) → U4_gaa(T124, T125, T126, X177, T129, T130, pF_in_gggaaaaaaa(T124, T125, T126, X173, X174, T129, T130, X175, X176, X177))
pF_in_gggaaaaaaa(T124, T125, T126, T131, T132, T134, T133, X175, X176, X177) → U19_gggaaaaaaa(T124, T125, T126, T131, T132, T134, T133, X175, X176, X177, splitD_in_ggaaa(T124, .(T125, T126), T131, T132, .(T134, T133)))
U19_gggaaaaaaa(T124, T125, T126, T131, T132, T134, T133, X175, X176, X177, splitD_out_ggaaa(T124, .(T125, T126), T131, T132, .(T134, T133))) → U20_gggaaaaaaa(T124, T125, T126, T131, T132, T134, T133, X175, X176, X177, pP_in_gaagaaa(T131, X175, T133, T132, X176, X177, T134))
pP_in_gaagaaa(T131, T137, T138, T132, X176, X177, T139) → U21_gaagaaa(T131, T137, T138, T132, X176, X177, T139, mergesortE_in_gaa(T131, T137, T138))
U21_gaagaaa(T131, T137, T138, T132, X176, X177, T139, mergesortE_out_gaa(T131, T137, T138)) → U22_gaagaaa(T131, T137, T138, T132, X176, X177, T139, pQ_in_gaagaa(T132, X176, T138, T137, X177, T139))
pQ_in_gaagaa(T132, T144, T146, T137, X177, T145) → U23_gaagaa(T132, T144, T146, T137, X177, T145, mergesortE_in_gaa(T132, T144, T146))
U23_gaagaa(T132, T144, T146, T137, X177, T145, mergesortE_out_gaa(T132, T144, T146)) → U24_gaagaa(T132, T144, T146, T137, X177, T145, mergeG_in_ggaaa(T137, T144, X177, T145, T146))
mergeG_in_ggaaa([], T173, T173, T174, T175) → mergeG_out_ggaaa([], T173, T173, T174, T175)
mergeG_in_ggaaa(T188, [], T188, T189, T190) → mergeG_out_ggaaa(T188, [], T188, T189, T190)
mergeG_in_ggaaa(.(T219, T220), .(T221, T222), .(T219, T226), T224, T227) → U5_ggaaa(T219, T220, T221, T222, T226, T224, T227, pH_in_ggggaa(T219, T221, T220, T222, T226, T227))
pH_in_ggggaa(T219, T221, T220, T222, T226, T227) → U25_ggggaa(T219, T221, T220, T222, T226, T227, leJ_in_gg(T219, T221))
leJ_in_gg(s(T240), s(T241)) → U7_gg(T240, T241, leJ_in_gg(T240, T241))
leJ_in_gg(0, s(0)) → leJ_out_gg(0, s(0))
leJ_in_gg(0, 0) → leJ_out_gg(0, 0)
U7_gg(T240, T241, leJ_out_gg(T240, T241)) → leJ_out_gg(s(T240), s(T241))
U25_ggggaa(T219, T221, T220, T222, T226, T227, leJ_out_gg(T219, T221)) → U26_ggggaa(T219, T221, T220, T222, T226, T227, mergeL_in_gggaa(T220, T221, T222, T226, T227))
mergeL_in_gggaa([], T262, T263, .(T262, T263), T264) → mergeL_out_gggaa([], T262, T263, .(T262, T263), T264)
mergeL_in_gggaa(.(T294, T295), T296, T297, .(T294, T301), .(T299, T302)) → U9_gggaa(T294, T295, T296, T297, T301, T299, T302, pH_in_ggggaa(T294, T296, T295, T297, T301, T302))
U9_gggaa(T294, T295, T296, T297, T301, T299, T302, pH_out_ggggaa(T294, T296, T295, T297, T301, T302)) → mergeL_out_gggaa(.(T294, T295), T296, T297, .(T294, T301), .(T299, T302))
mergeL_in_gggaa(.(T319, T320), T321, T322, .(T321, T326), .(T324, T327)) → U10_gggaa(T319, T320, T321, T322, T326, T324, T327, pI_in_ggggaa(T319, T321, T320, T322, T326, T327))
pI_in_ggggaa(T319, T321, T320, T322, T326, T327) → U27_ggggaa(T319, T321, T320, T322, T326, T327, gtK_in_gg(T319, T321))
gtK_in_gg(s(T340), s(T341)) → U8_gg(T340, T341, gtK_in_gg(T340, T341))
gtK_in_gg(s(0), 0) → gtK_out_gg(s(0), 0)
U8_gg(T340, T341, gtK_out_gg(T340, T341)) → gtK_out_gg(s(T340), s(T341))
U27_ggggaa(T319, T321, T320, T322, T326, T327, gtK_out_gg(T319, T321)) → U28_ggggaa(T319, T321, T320, T322, T326, T327, mergeM_in_gggaa(T319, T320, T322, T326, T327))
mergeM_in_gggaa(T356, T357, [], .(T356, T357), T358) → mergeM_out_gggaa(T356, T357, [], .(T356, T357), T358)
mergeM_in_gggaa(T387, T388, .(T389, T390), .(T387, T394), .(T392, T395)) → U11_gggaa(T387, T388, T389, T390, T394, T392, T395, pH_in_ggggaa(T387, T389, T388, T390, T394, T395))
U11_gggaa(T387, T388, T389, T390, T394, T392, T395, pH_out_ggggaa(T387, T389, T388, T390, T394, T395)) → mergeM_out_gggaa(T387, T388, .(T389, T390), .(T387, T394), .(T392, T395))
mergeM_in_gggaa(T412, T413, .(T414, T415), .(T414, T419), .(T417, T420)) → U12_gggaa(T412, T413, T414, T415, T419, T417, T420, pI_in_ggggaa(T412, T414, T413, T415, T419, T420))
U12_gggaa(T412, T413, T414, T415, T419, T417, T420, pI_out_ggggaa(T412, T414, T413, T415, T419, T420)) → mergeM_out_gggaa(T412, T413, .(T414, T415), .(T414, T419), .(T417, T420))
U28_ggggaa(T319, T321, T320, T322, T326, T327, mergeM_out_gggaa(T319, T320, T322, T326, T327)) → pI_out_ggggaa(T319, T321, T320, T322, T326, T327)
U10_gggaa(T319, T320, T321, T322, T326, T324, T327, pI_out_ggggaa(T319, T321, T320, T322, T326, T327)) → mergeL_out_gggaa(.(T319, T320), T321, T322, .(T321, T326), .(T324, T327))
U26_ggggaa(T219, T221, T220, T222, T226, T227, mergeL_out_gggaa(T220, T221, T222, T226, T227)) → pH_out_ggggaa(T219, T221, T220, T222, T226, T227)
U5_ggaaa(T219, T220, T221, T222, T226, T224, T227, pH_out_ggggaa(T219, T221, T220, T222, T226, T227)) → mergeG_out_ggaaa(.(T219, T220), .(T221, T222), .(T219, T226), T224, T227)
mergeG_in_ggaaa(.(T437, T438), .(T439, T440), .(T439, T444), T442, T445) → U6_ggaaa(T437, T438, T439, T440, T444, T442, T445, pI_in_ggggaa(T437, T439, T438, T440, T444, T445))
U6_ggaaa(T437, T438, T439, T440, T444, T442, T445, pI_out_ggggaa(T437, T439, T438, T440, T444, T445)) → mergeG_out_ggaaa(.(T437, T438), .(T439, T440), .(T439, T444), T442, T445)
U24_gaagaa(T132, T144, T146, T137, X177, T145, mergeG_out_ggaaa(T137, T144, X177, T145, T146)) → pQ_out_gaagaa(T132, T144, T146, T137, X177, T145)
U22_gaagaaa(T131, T137, T138, T132, X176, X177, T139, pQ_out_gaagaa(T132, X176, T138, T137, X177, T139)) → pP_out_gaagaaa(T131, T137, T138, T132, X176, X177, T139)
U20_gggaaaaaaa(T124, T125, T126, T131, T132, T134, T133, X175, X176, X177, pP_out_gaagaaa(T131, X175, T133, T132, X176, X177, T134)) → pF_out_gggaaaaaaa(T124, T125, T126, T131, T132, T134, T133, X175, X176, X177)
U4_gaa(T124, T125, T126, X177, T129, T130, pF_out_gggaaaaaaa(T124, T125, T126, X173, X174, T129, T130, X175, X176, X177)) → mergesortE_out_gaa(.(T124, .(T125, T126)), X177, .(T129, T130))
U17_gaagaa(T47, T93, T96, T87, T94, T95, mergesortE_out_gaa(T47, T93, T96)) → U18_gaagaa(T47, T93, T96, T87, T94, T95, mergeG_in_ggaaa(T87, T93, T94, T95, T96))
U18_gaagaa(T47, T93, T96, T87, T94, T95, mergeG_out_ggaaa(T87, T93, T94, T95, T96)) → pO_out_gaagaa(T47, T93, T96, T87, T94, T95)
U16_ggaagaaa(T39, T48, T87, T88, T47, X36, T89, T90, pO_out_gaagaa(T47, X36, T88, T87, T89, T90)) → pN_out_ggaagaaa(T39, T48, T87, T88, T47, X36, T89, T90)
U14_ggaaagaaaa(T40, T41, T47, T48, T49, T39, X35, X36, T50, T51, pN_out_ggaagaaa(T39, T48, X35, T49, T47, X36, T50, T51)) → pB_out_ggaaagaaaa(T40, T41, T47, T48, T49, T39, X35, X36, T50, T51)
U1_gaa(T39, T40, T41, T45, T46, T44, pB_out_ggaaagaaaa(T40, T41, X63, X62, T44, T39, X35, X36, T45, T46)) → mergesortA_out_gaa(.(T39, .(T40, T41)), T45, .(T46, T44))
LEJ_IN_GG(s(T240), s(T241)) → LEJ_IN_GG(T240, T241)
LEJ_IN_GG(s(T240), s(T241)) → LEJ_IN_GG(T240, T241)
From the DPs we obtained the following set of size-change graphs:
U25_GGGGAA(T219, T221, T220, T222, T226, T227, leJ_out_gg(T219, T221)) → MERGEL_IN_GGGAA(T220, T221, T222, T226, T227)
MERGEL_IN_GGGAA(.(T294, T295), T296, T297, .(T294, T301), .(T299, T302)) → PH_IN_GGGGAA(T294, T296, T295, T297, T301, T302)
PH_IN_GGGGAA(T219, T221, T220, T222, T226, T227) → U25_GGGGAA(T219, T221, T220, T222, T226, T227, leJ_in_gg(T219, T221))
MERGEL_IN_GGGAA(.(T319, T320), T321, T322, .(T321, T326), .(T324, T327)) → PI_IN_GGGGAA(T319, T321, T320, T322, T326, T327)
PI_IN_GGGGAA(T319, T321, T320, T322, T326, T327) → U27_GGGGAA(T319, T321, T320, T322, T326, T327, gtK_in_gg(T319, T321))
U27_GGGGAA(T319, T321, T320, T322, T326, T327, gtK_out_gg(T319, T321)) → MERGEM_IN_GGGAA(T319, T320, T322, T326, T327)
MERGEM_IN_GGGAA(T387, T388, .(T389, T390), .(T387, T394), .(T392, T395)) → PH_IN_GGGGAA(T387, T389, T388, T390, T394, T395)
MERGEM_IN_GGGAA(T412, T413, .(T414, T415), .(T414, T419), .(T417, T420)) → PI_IN_GGGGAA(T412, T414, T413, T415, T419, T420)
mergesortA_in_gaa([], [], T5) → mergesortA_out_gaa([], [], T5)
mergesortA_in_gaa(.(T8, []), .(T8, []), T9) → mergesortA_out_gaa(.(T8, []), .(T8, []), T9)
mergesortA_in_gaa(.(T39, .(T40, T41)), T45, .(T46, T44)) → U1_gaa(T39, T40, T41, T45, T46, T44, pB_in_ggaaagaaaa(T40, T41, X63, X62, T44, T39, X35, X36, T45, T46))
pB_in_ggaaagaaaa(T40, T41, T47, T48, T49, T39, X35, X36, T50, T51) → U13_ggaaagaaaa(T40, T41, T47, T48, T49, T39, X35, X36, T50, T51, splitD_in_ggaaa(T40, T41, T47, T48, T49))
splitD_in_ggaaa(T60, T61, .(T60, X91), X92, .(T62, T64)) → U3_ggaaa(T60, T61, X91, X92, T62, T64, splitC_in_gaaa(T61, X92, X91, T64))
splitC_in_gaaa([], [], [], T71) → splitC_out_gaaa([], [], [], T71)
splitC_in_gaaa(.(T80, T81), .(T80, X122), X123, .(T82, T84)) → U2_gaaa(T80, T81, X122, X123, T82, T84, splitC_in_gaaa(T81, X123, X122, T84))
U2_gaaa(T80, T81, X122, X123, T82, T84, splitC_out_gaaa(T81, X123, X122, T84)) → splitC_out_gaaa(.(T80, T81), .(T80, X122), X123, .(T82, T84))
U3_ggaaa(T60, T61, X91, X92, T62, T64, splitC_out_gaaa(T61, X92, X91, T64)) → splitD_out_ggaaa(T60, T61, .(T60, X91), X92, .(T62, T64))
U13_ggaaagaaaa(T40, T41, T47, T48, T49, T39, X35, X36, T50, T51, splitD_out_ggaaa(T40, T41, T47, T48, T49)) → U14_ggaaagaaaa(T40, T41, T47, T48, T49, T39, X35, X36, T50, T51, pN_in_ggaagaaa(T39, T48, X35, T49, T47, X36, T50, T51))
pN_in_ggaagaaa(T39, T48, T87, T88, T47, X36, T89, T90) → U15_ggaagaaa(T39, T48, T87, T88, T47, X36, T89, T90, mergesortA_in_gaa(.(T39, T48), T87, T88))
U15_ggaagaaa(T39, T48, T87, T88, T47, X36, T89, T90, mergesortA_out_gaa(.(T39, T48), T87, T88)) → U16_ggaagaaa(T39, T48, T87, T88, T47, X36, T89, T90, pO_in_gaagaa(T47, X36, T88, T87, T89, T90))
pO_in_gaagaa(T47, T93, T96, T87, T94, T95) → U17_gaagaa(T47, T93, T96, T87, T94, T95, mergesortE_in_gaa(T47, T93, T96))
mergesortE_in_gaa([], [], T103) → mergesortE_out_gaa([], [], T103)
mergesortE_in_gaa(.(T112, []), .(T112, []), T113) → mergesortE_out_gaa(.(T112, []), .(T112, []), T113)
mergesortE_in_gaa(.(T124, .(T125, T126)), X177, .(T129, T130)) → U4_gaa(T124, T125, T126, X177, T129, T130, pF_in_gggaaaaaaa(T124, T125, T126, X173, X174, T129, T130, X175, X176, X177))
pF_in_gggaaaaaaa(T124, T125, T126, T131, T132, T134, T133, X175, X176, X177) → U19_gggaaaaaaa(T124, T125, T126, T131, T132, T134, T133, X175, X176, X177, splitD_in_ggaaa(T124, .(T125, T126), T131, T132, .(T134, T133)))
U19_gggaaaaaaa(T124, T125, T126, T131, T132, T134, T133, X175, X176, X177, splitD_out_ggaaa(T124, .(T125, T126), T131, T132, .(T134, T133))) → U20_gggaaaaaaa(T124, T125, T126, T131, T132, T134, T133, X175, X176, X177, pP_in_gaagaaa(T131, X175, T133, T132, X176, X177, T134))
pP_in_gaagaaa(T131, T137, T138, T132, X176, X177, T139) → U21_gaagaaa(T131, T137, T138, T132, X176, X177, T139, mergesortE_in_gaa(T131, T137, T138))
U21_gaagaaa(T131, T137, T138, T132, X176, X177, T139, mergesortE_out_gaa(T131, T137, T138)) → U22_gaagaaa(T131, T137, T138, T132, X176, X177, T139, pQ_in_gaagaa(T132, X176, T138, T137, X177, T139))
pQ_in_gaagaa(T132, T144, T146, T137, X177, T145) → U23_gaagaa(T132, T144, T146, T137, X177, T145, mergesortE_in_gaa(T132, T144, T146))
U23_gaagaa(T132, T144, T146, T137, X177, T145, mergesortE_out_gaa(T132, T144, T146)) → U24_gaagaa(T132, T144, T146, T137, X177, T145, mergeG_in_ggaaa(T137, T144, X177, T145, T146))
mergeG_in_ggaaa([], T173, T173, T174, T175) → mergeG_out_ggaaa([], T173, T173, T174, T175)
mergeG_in_ggaaa(T188, [], T188, T189, T190) → mergeG_out_ggaaa(T188, [], T188, T189, T190)
mergeG_in_ggaaa(.(T219, T220), .(T221, T222), .(T219, T226), T224, T227) → U5_ggaaa(T219, T220, T221, T222, T226, T224, T227, pH_in_ggggaa(T219, T221, T220, T222, T226, T227))
pH_in_ggggaa(T219, T221, T220, T222, T226, T227) → U25_ggggaa(T219, T221, T220, T222, T226, T227, leJ_in_gg(T219, T221))
leJ_in_gg(s(T240), s(T241)) → U7_gg(T240, T241, leJ_in_gg(T240, T241))
leJ_in_gg(0, s(0)) → leJ_out_gg(0, s(0))
leJ_in_gg(0, 0) → leJ_out_gg(0, 0)
U7_gg(T240, T241, leJ_out_gg(T240, T241)) → leJ_out_gg(s(T240), s(T241))
U25_ggggaa(T219, T221, T220, T222, T226, T227, leJ_out_gg(T219, T221)) → U26_ggggaa(T219, T221, T220, T222, T226, T227, mergeL_in_gggaa(T220, T221, T222, T226, T227))
mergeL_in_gggaa([], T262, T263, .(T262, T263), T264) → mergeL_out_gggaa([], T262, T263, .(T262, T263), T264)
mergeL_in_gggaa(.(T294, T295), T296, T297, .(T294, T301), .(T299, T302)) → U9_gggaa(T294, T295, T296, T297, T301, T299, T302, pH_in_ggggaa(T294, T296, T295, T297, T301, T302))
U9_gggaa(T294, T295, T296, T297, T301, T299, T302, pH_out_ggggaa(T294, T296, T295, T297, T301, T302)) → mergeL_out_gggaa(.(T294, T295), T296, T297, .(T294, T301), .(T299, T302))
mergeL_in_gggaa(.(T319, T320), T321, T322, .(T321, T326), .(T324, T327)) → U10_gggaa(T319, T320, T321, T322, T326, T324, T327, pI_in_ggggaa(T319, T321, T320, T322, T326, T327))
pI_in_ggggaa(T319, T321, T320, T322, T326, T327) → U27_ggggaa(T319, T321, T320, T322, T326, T327, gtK_in_gg(T319, T321))
gtK_in_gg(s(T340), s(T341)) → U8_gg(T340, T341, gtK_in_gg(T340, T341))
gtK_in_gg(s(0), 0) → gtK_out_gg(s(0), 0)
U8_gg(T340, T341, gtK_out_gg(T340, T341)) → gtK_out_gg(s(T340), s(T341))
U27_ggggaa(T319, T321, T320, T322, T326, T327, gtK_out_gg(T319, T321)) → U28_ggggaa(T319, T321, T320, T322, T326, T327, mergeM_in_gggaa(T319, T320, T322, T326, T327))
mergeM_in_gggaa(T356, T357, [], .(T356, T357), T358) → mergeM_out_gggaa(T356, T357, [], .(T356, T357), T358)
mergeM_in_gggaa(T387, T388, .(T389, T390), .(T387, T394), .(T392, T395)) → U11_gggaa(T387, T388, T389, T390, T394, T392, T395, pH_in_ggggaa(T387, T389, T388, T390, T394, T395))
U11_gggaa(T387, T388, T389, T390, T394, T392, T395, pH_out_ggggaa(T387, T389, T388, T390, T394, T395)) → mergeM_out_gggaa(T387, T388, .(T389, T390), .(T387, T394), .(T392, T395))
mergeM_in_gggaa(T412, T413, .(T414, T415), .(T414, T419), .(T417, T420)) → U12_gggaa(T412, T413, T414, T415, T419, T417, T420, pI_in_ggggaa(T412, T414, T413, T415, T419, T420))
U12_gggaa(T412, T413, T414, T415, T419, T417, T420, pI_out_ggggaa(T412, T414, T413, T415, T419, T420)) → mergeM_out_gggaa(T412, T413, .(T414, T415), .(T414, T419), .(T417, T420))
U28_ggggaa(T319, T321, T320, T322, T326, T327, mergeM_out_gggaa(T319, T320, T322, T326, T327)) → pI_out_ggggaa(T319, T321, T320, T322, T326, T327)
U10_gggaa(T319, T320, T321, T322, T326, T324, T327, pI_out_ggggaa(T319, T321, T320, T322, T326, T327)) → mergeL_out_gggaa(.(T319, T320), T321, T322, .(T321, T326), .(T324, T327))
U26_ggggaa(T219, T221, T220, T222, T226, T227, mergeL_out_gggaa(T220, T221, T222, T226, T227)) → pH_out_ggggaa(T219, T221, T220, T222, T226, T227)
U5_ggaaa(T219, T220, T221, T222, T226, T224, T227, pH_out_ggggaa(T219, T221, T220, T222, T226, T227)) → mergeG_out_ggaaa(.(T219, T220), .(T221, T222), .(T219, T226), T224, T227)
mergeG_in_ggaaa(.(T437, T438), .(T439, T440), .(T439, T444), T442, T445) → U6_ggaaa(T437, T438, T439, T440, T444, T442, T445, pI_in_ggggaa(T437, T439, T438, T440, T444, T445))
U6_ggaaa(T437, T438, T439, T440, T444, T442, T445, pI_out_ggggaa(T437, T439, T438, T440, T444, T445)) → mergeG_out_ggaaa(.(T437, T438), .(T439, T440), .(T439, T444), T442, T445)
U24_gaagaa(T132, T144, T146, T137, X177, T145, mergeG_out_ggaaa(T137, T144, X177, T145, T146)) → pQ_out_gaagaa(T132, T144, T146, T137, X177, T145)
U22_gaagaaa(T131, T137, T138, T132, X176, X177, T139, pQ_out_gaagaa(T132, X176, T138, T137, X177, T139)) → pP_out_gaagaaa(T131, T137, T138, T132, X176, X177, T139)
U20_gggaaaaaaa(T124, T125, T126, T131, T132, T134, T133, X175, X176, X177, pP_out_gaagaaa(T131, X175, T133, T132, X176, X177, T134)) → pF_out_gggaaaaaaa(T124, T125, T126, T131, T132, T134, T133, X175, X176, X177)
U4_gaa(T124, T125, T126, X177, T129, T130, pF_out_gggaaaaaaa(T124, T125, T126, X173, X174, T129, T130, X175, X176, X177)) → mergesortE_out_gaa(.(T124, .(T125, T126)), X177, .(T129, T130))
U17_gaagaa(T47, T93, T96, T87, T94, T95, mergesortE_out_gaa(T47, T93, T96)) → U18_gaagaa(T47, T93, T96, T87, T94, T95, mergeG_in_ggaaa(T87, T93, T94, T95, T96))
U18_gaagaa(T47, T93, T96, T87, T94, T95, mergeG_out_ggaaa(T87, T93, T94, T95, T96)) → pO_out_gaagaa(T47, T93, T96, T87, T94, T95)
U16_ggaagaaa(T39, T48, T87, T88, T47, X36, T89, T90, pO_out_gaagaa(T47, X36, T88, T87, T89, T90)) → pN_out_ggaagaaa(T39, T48, T87, T88, T47, X36, T89, T90)
U14_ggaaagaaaa(T40, T41, T47, T48, T49, T39, X35, X36, T50, T51, pN_out_ggaagaaa(T39, T48, X35, T49, T47, X36, T50, T51)) → pB_out_ggaaagaaaa(T40, T41, T47, T48, T49, T39, X35, X36, T50, T51)
U1_gaa(T39, T40, T41, T45, T46, T44, pB_out_ggaaagaaaa(T40, T41, X63, X62, T44, T39, X35, X36, T45, T46)) → mergesortA_out_gaa(.(T39, .(T40, T41)), T45, .(T46, T44))
U25_GGGGAA(T219, T221, T220, T222, T226, T227, leJ_out_gg(T219, T221)) → MERGEL_IN_GGGAA(T220, T221, T222, T226, T227)
MERGEL_IN_GGGAA(.(T294, T295), T296, T297, .(T294, T301), .(T299, T302)) → PH_IN_GGGGAA(T294, T296, T295, T297, T301, T302)
PH_IN_GGGGAA(T219, T221, T220, T222, T226, T227) → U25_GGGGAA(T219, T221, T220, T222, T226, T227, leJ_in_gg(T219, T221))
MERGEL_IN_GGGAA(.(T319, T320), T321, T322, .(T321, T326), .(T324, T327)) → PI_IN_GGGGAA(T319, T321, T320, T322, T326, T327)
PI_IN_GGGGAA(T319, T321, T320, T322, T326, T327) → U27_GGGGAA(T319, T321, T320, T322, T326, T327, gtK_in_gg(T319, T321))
U27_GGGGAA(T319, T321, T320, T322, T326, T327, gtK_out_gg(T319, T321)) → MERGEM_IN_GGGAA(T319, T320, T322, T326, T327)
MERGEM_IN_GGGAA(T387, T388, .(T389, T390), .(T387, T394), .(T392, T395)) → PH_IN_GGGGAA(T387, T389, T388, T390, T394, T395)
MERGEM_IN_GGGAA(T412, T413, .(T414, T415), .(T414, T419), .(T417, T420)) → PI_IN_GGGGAA(T412, T414, T413, T415, T419, T420)
leJ_in_gg(s(T240), s(T241)) → U7_gg(T240, T241, leJ_in_gg(T240, T241))
leJ_in_gg(0, s(0)) → leJ_out_gg(0, s(0))
leJ_in_gg(0, 0) → leJ_out_gg(0, 0)
gtK_in_gg(s(T340), s(T341)) → U8_gg(T340, T341, gtK_in_gg(T340, T341))
gtK_in_gg(s(0), 0) → gtK_out_gg(s(0), 0)
U7_gg(T240, T241, leJ_out_gg(T240, T241)) → leJ_out_gg(s(T240), s(T241))
U8_gg(T340, T341, gtK_out_gg(T340, T341)) → gtK_out_gg(s(T340), s(T341))
U25_GGGGAA(T219, T221, T220, T222, leJ_out_gg(T219, T221)) → MERGEL_IN_GGGAA(T220, T221, T222)
MERGEL_IN_GGGAA(.(T294, T295), T296, T297) → PH_IN_GGGGAA(T294, T296, T295, T297)
PH_IN_GGGGAA(T219, T221, T220, T222) → U25_GGGGAA(T219, T221, T220, T222, leJ_in_gg(T219, T221))
MERGEL_IN_GGGAA(.(T319, T320), T321, T322) → PI_IN_GGGGAA(T319, T321, T320, T322)
PI_IN_GGGGAA(T319, T321, T320, T322) → U27_GGGGAA(T319, T321, T320, T322, gtK_in_gg(T319, T321))
U27_GGGGAA(T319, T321, T320, T322, gtK_out_gg(T319, T321)) → MERGEM_IN_GGGAA(T319, T320, T322)
MERGEM_IN_GGGAA(T387, T388, .(T389, T390)) → PH_IN_GGGGAA(T387, T389, T388, T390)
MERGEM_IN_GGGAA(T412, T413, .(T414, T415)) → PI_IN_GGGGAA(T412, T414, T413, T415)
leJ_in_gg(s(T240), s(T241)) → U7_gg(T240, T241, leJ_in_gg(T240, T241))
leJ_in_gg(0, s(0)) → leJ_out_gg(0, s(0))
leJ_in_gg(0, 0) → leJ_out_gg(0, 0)
gtK_in_gg(s(T340), s(T341)) → U8_gg(T340, T341, gtK_in_gg(T340, T341))
gtK_in_gg(s(0), 0) → gtK_out_gg(s(0), 0)
U7_gg(T240, T241, leJ_out_gg(T240, T241)) → leJ_out_gg(s(T240), s(T241))
U8_gg(T340, T341, gtK_out_gg(T340, T341)) → gtK_out_gg(s(T340), s(T341))
leJ_in_gg(x0, x1)
gtK_in_gg(x0, x1)
U7_gg(x0, x1, x2)
U8_gg(x0, x1, x2)
From the DPs we obtained the following set of size-change graphs:
SPLITC_IN_GAAA(.(T80, T81), .(T80, X122), X123, .(T82, T84)) → SPLITC_IN_GAAA(T81, X123, X122, T84)
mergesortA_in_gaa([], [], T5) → mergesortA_out_gaa([], [], T5)
mergesortA_in_gaa(.(T8, []), .(T8, []), T9) → mergesortA_out_gaa(.(T8, []), .(T8, []), T9)
mergesortA_in_gaa(.(T39, .(T40, T41)), T45, .(T46, T44)) → U1_gaa(T39, T40, T41, T45, T46, T44, pB_in_ggaaagaaaa(T40, T41, X63, X62, T44, T39, X35, X36, T45, T46))
pB_in_ggaaagaaaa(T40, T41, T47, T48, T49, T39, X35, X36, T50, T51) → U13_ggaaagaaaa(T40, T41, T47, T48, T49, T39, X35, X36, T50, T51, splitD_in_ggaaa(T40, T41, T47, T48, T49))
splitD_in_ggaaa(T60, T61, .(T60, X91), X92, .(T62, T64)) → U3_ggaaa(T60, T61, X91, X92, T62, T64, splitC_in_gaaa(T61, X92, X91, T64))
splitC_in_gaaa([], [], [], T71) → splitC_out_gaaa([], [], [], T71)
splitC_in_gaaa(.(T80, T81), .(T80, X122), X123, .(T82, T84)) → U2_gaaa(T80, T81, X122, X123, T82, T84, splitC_in_gaaa(T81, X123, X122, T84))
U2_gaaa(T80, T81, X122, X123, T82, T84, splitC_out_gaaa(T81, X123, X122, T84)) → splitC_out_gaaa(.(T80, T81), .(T80, X122), X123, .(T82, T84))
U3_ggaaa(T60, T61, X91, X92, T62, T64, splitC_out_gaaa(T61, X92, X91, T64)) → splitD_out_ggaaa(T60, T61, .(T60, X91), X92, .(T62, T64))
U13_ggaaagaaaa(T40, T41, T47, T48, T49, T39, X35, X36, T50, T51, splitD_out_ggaaa(T40, T41, T47, T48, T49)) → U14_ggaaagaaaa(T40, T41, T47, T48, T49, T39, X35, X36, T50, T51, pN_in_ggaagaaa(T39, T48, X35, T49, T47, X36, T50, T51))
pN_in_ggaagaaa(T39, T48, T87, T88, T47, X36, T89, T90) → U15_ggaagaaa(T39, T48, T87, T88, T47, X36, T89, T90, mergesortA_in_gaa(.(T39, T48), T87, T88))
U15_ggaagaaa(T39, T48, T87, T88, T47, X36, T89, T90, mergesortA_out_gaa(.(T39, T48), T87, T88)) → U16_ggaagaaa(T39, T48, T87, T88, T47, X36, T89, T90, pO_in_gaagaa(T47, X36, T88, T87, T89, T90))
pO_in_gaagaa(T47, T93, T96, T87, T94, T95) → U17_gaagaa(T47, T93, T96, T87, T94, T95, mergesortE_in_gaa(T47, T93, T96))
mergesortE_in_gaa([], [], T103) → mergesortE_out_gaa([], [], T103)
mergesortE_in_gaa(.(T112, []), .(T112, []), T113) → mergesortE_out_gaa(.(T112, []), .(T112, []), T113)
mergesortE_in_gaa(.(T124, .(T125, T126)), X177, .(T129, T130)) → U4_gaa(T124, T125, T126, X177, T129, T130, pF_in_gggaaaaaaa(T124, T125, T126, X173, X174, T129, T130, X175, X176, X177))
pF_in_gggaaaaaaa(T124, T125, T126, T131, T132, T134, T133, X175, X176, X177) → U19_gggaaaaaaa(T124, T125, T126, T131, T132, T134, T133, X175, X176, X177, splitD_in_ggaaa(T124, .(T125, T126), T131, T132, .(T134, T133)))
U19_gggaaaaaaa(T124, T125, T126, T131, T132, T134, T133, X175, X176, X177, splitD_out_ggaaa(T124, .(T125, T126), T131, T132, .(T134, T133))) → U20_gggaaaaaaa(T124, T125, T126, T131, T132, T134, T133, X175, X176, X177, pP_in_gaagaaa(T131, X175, T133, T132, X176, X177, T134))
pP_in_gaagaaa(T131, T137, T138, T132, X176, X177, T139) → U21_gaagaaa(T131, T137, T138, T132, X176, X177, T139, mergesortE_in_gaa(T131, T137, T138))
U21_gaagaaa(T131, T137, T138, T132, X176, X177, T139, mergesortE_out_gaa(T131, T137, T138)) → U22_gaagaaa(T131, T137, T138, T132, X176, X177, T139, pQ_in_gaagaa(T132, X176, T138, T137, X177, T139))
pQ_in_gaagaa(T132, T144, T146, T137, X177, T145) → U23_gaagaa(T132, T144, T146, T137, X177, T145, mergesortE_in_gaa(T132, T144, T146))
U23_gaagaa(T132, T144, T146, T137, X177, T145, mergesortE_out_gaa(T132, T144, T146)) → U24_gaagaa(T132, T144, T146, T137, X177, T145, mergeG_in_ggaaa(T137, T144, X177, T145, T146))
mergeG_in_ggaaa([], T173, T173, T174, T175) → mergeG_out_ggaaa([], T173, T173, T174, T175)
mergeG_in_ggaaa(T188, [], T188, T189, T190) → mergeG_out_ggaaa(T188, [], T188, T189, T190)
mergeG_in_ggaaa(.(T219, T220), .(T221, T222), .(T219, T226), T224, T227) → U5_ggaaa(T219, T220, T221, T222, T226, T224, T227, pH_in_ggggaa(T219, T221, T220, T222, T226, T227))
pH_in_ggggaa(T219, T221, T220, T222, T226, T227) → U25_ggggaa(T219, T221, T220, T222, T226, T227, leJ_in_gg(T219, T221))
leJ_in_gg(s(T240), s(T241)) → U7_gg(T240, T241, leJ_in_gg(T240, T241))
leJ_in_gg(0, s(0)) → leJ_out_gg(0, s(0))
leJ_in_gg(0, 0) → leJ_out_gg(0, 0)
U7_gg(T240, T241, leJ_out_gg(T240, T241)) → leJ_out_gg(s(T240), s(T241))
U25_ggggaa(T219, T221, T220, T222, T226, T227, leJ_out_gg(T219, T221)) → U26_ggggaa(T219, T221, T220, T222, T226, T227, mergeL_in_gggaa(T220, T221, T222, T226, T227))
mergeL_in_gggaa([], T262, T263, .(T262, T263), T264) → mergeL_out_gggaa([], T262, T263, .(T262, T263), T264)
mergeL_in_gggaa(.(T294, T295), T296, T297, .(T294, T301), .(T299, T302)) → U9_gggaa(T294, T295, T296, T297, T301, T299, T302, pH_in_ggggaa(T294, T296, T295, T297, T301, T302))
U9_gggaa(T294, T295, T296, T297, T301, T299, T302, pH_out_ggggaa(T294, T296, T295, T297, T301, T302)) → mergeL_out_gggaa(.(T294, T295), T296, T297, .(T294, T301), .(T299, T302))
mergeL_in_gggaa(.(T319, T320), T321, T322, .(T321, T326), .(T324, T327)) → U10_gggaa(T319, T320, T321, T322, T326, T324, T327, pI_in_ggggaa(T319, T321, T320, T322, T326, T327))
pI_in_ggggaa(T319, T321, T320, T322, T326, T327) → U27_ggggaa(T319, T321, T320, T322, T326, T327, gtK_in_gg(T319, T321))
gtK_in_gg(s(T340), s(T341)) → U8_gg(T340, T341, gtK_in_gg(T340, T341))
gtK_in_gg(s(0), 0) → gtK_out_gg(s(0), 0)
U8_gg(T340, T341, gtK_out_gg(T340, T341)) → gtK_out_gg(s(T340), s(T341))
U27_ggggaa(T319, T321, T320, T322, T326, T327, gtK_out_gg(T319, T321)) → U28_ggggaa(T319, T321, T320, T322, T326, T327, mergeM_in_gggaa(T319, T320, T322, T326, T327))
mergeM_in_gggaa(T356, T357, [], .(T356, T357), T358) → mergeM_out_gggaa(T356, T357, [], .(T356, T357), T358)
mergeM_in_gggaa(T387, T388, .(T389, T390), .(T387, T394), .(T392, T395)) → U11_gggaa(T387, T388, T389, T390, T394, T392, T395, pH_in_ggggaa(T387, T389, T388, T390, T394, T395))
U11_gggaa(T387, T388, T389, T390, T394, T392, T395, pH_out_ggggaa(T387, T389, T388, T390, T394, T395)) → mergeM_out_gggaa(T387, T388, .(T389, T390), .(T387, T394), .(T392, T395))
mergeM_in_gggaa(T412, T413, .(T414, T415), .(T414, T419), .(T417, T420)) → U12_gggaa(T412, T413, T414, T415, T419, T417, T420, pI_in_ggggaa(T412, T414, T413, T415, T419, T420))
U12_gggaa(T412, T413, T414, T415, T419, T417, T420, pI_out_ggggaa(T412, T414, T413, T415, T419, T420)) → mergeM_out_gggaa(T412, T413, .(T414, T415), .(T414, T419), .(T417, T420))
U28_ggggaa(T319, T321, T320, T322, T326, T327, mergeM_out_gggaa(T319, T320, T322, T326, T327)) → pI_out_ggggaa(T319, T321, T320, T322, T326, T327)
U10_gggaa(T319, T320, T321, T322, T326, T324, T327, pI_out_ggggaa(T319, T321, T320, T322, T326, T327)) → mergeL_out_gggaa(.(T319, T320), T321, T322, .(T321, T326), .(T324, T327))
U26_ggggaa(T219, T221, T220, T222, T226, T227, mergeL_out_gggaa(T220, T221, T222, T226, T227)) → pH_out_ggggaa(T219, T221, T220, T222, T226, T227)
U5_ggaaa(T219, T220, T221, T222, T226, T224, T227, pH_out_ggggaa(T219, T221, T220, T222, T226, T227)) → mergeG_out_ggaaa(.(T219, T220), .(T221, T222), .(T219, T226), T224, T227)
mergeG_in_ggaaa(.(T437, T438), .(T439, T440), .(T439, T444), T442, T445) → U6_ggaaa(T437, T438, T439, T440, T444, T442, T445, pI_in_ggggaa(T437, T439, T438, T440, T444, T445))
U6_ggaaa(T437, T438, T439, T440, T444, T442, T445, pI_out_ggggaa(T437, T439, T438, T440, T444, T445)) → mergeG_out_ggaaa(.(T437, T438), .(T439, T440), .(T439, T444), T442, T445)
U24_gaagaa(T132, T144, T146, T137, X177, T145, mergeG_out_ggaaa(T137, T144, X177, T145, T146)) → pQ_out_gaagaa(T132, T144, T146, T137, X177, T145)
U22_gaagaaa(T131, T137, T138, T132, X176, X177, T139, pQ_out_gaagaa(T132, X176, T138, T137, X177, T139)) → pP_out_gaagaaa(T131, T137, T138, T132, X176, X177, T139)
U20_gggaaaaaaa(T124, T125, T126, T131, T132, T134, T133, X175, X176, X177, pP_out_gaagaaa(T131, X175, T133, T132, X176, X177, T134)) → pF_out_gggaaaaaaa(T124, T125, T126, T131, T132, T134, T133, X175, X176, X177)
U4_gaa(T124, T125, T126, X177, T129, T130, pF_out_gggaaaaaaa(T124, T125, T126, X173, X174, T129, T130, X175, X176, X177)) → mergesortE_out_gaa(.(T124, .(T125, T126)), X177, .(T129, T130))
U17_gaagaa(T47, T93, T96, T87, T94, T95, mergesortE_out_gaa(T47, T93, T96)) → U18_gaagaa(T47, T93, T96, T87, T94, T95, mergeG_in_ggaaa(T87, T93, T94, T95, T96))
U18_gaagaa(T47, T93, T96, T87, T94, T95, mergeG_out_ggaaa(T87, T93, T94, T95, T96)) → pO_out_gaagaa(T47, T93, T96, T87, T94, T95)
U16_ggaagaaa(T39, T48, T87, T88, T47, X36, T89, T90, pO_out_gaagaa(T47, X36, T88, T87, T89, T90)) → pN_out_ggaagaaa(T39, T48, T87, T88, T47, X36, T89, T90)
U14_ggaaagaaaa(T40, T41, T47, T48, T49, T39, X35, X36, T50, T51, pN_out_ggaagaaa(T39, T48, X35, T49, T47, X36, T50, T51)) → pB_out_ggaaagaaaa(T40, T41, T47, T48, T49, T39, X35, X36, T50, T51)
U1_gaa(T39, T40, T41, T45, T46, T44, pB_out_ggaaagaaaa(T40, T41, X63, X62, T44, T39, X35, X36, T45, T46)) → mergesortA_out_gaa(.(T39, .(T40, T41)), T45, .(T46, T44))
SPLITC_IN_GAAA(.(T80, T81), .(T80, X122), X123, .(T82, T84)) → SPLITC_IN_GAAA(T81, X123, X122, T84)
SPLITC_IN_GAAA(.(T80, T81)) → SPLITC_IN_GAAA(T81)
From the DPs we obtained the following set of size-change graphs:
PF_IN_GGGAAAAAAA(T124, T125, T126, T131, T132, T134, T133, X175, X176, X177) → U19_GGGAAAAAAA(T124, T125, T126, T131, T132, T134, T133, X175, X176, X177, splitD_in_ggaaa(T124, .(T125, T126), T131, T132, .(T134, T133)))
U19_GGGAAAAAAA(T124, T125, T126, T131, T132, T134, T133, X175, X176, X177, splitD_out_ggaaa(T124, .(T125, T126), T131, T132, .(T134, T133))) → PP_IN_GAAGAAA(T131, X175, T133, T132, X176, X177, T134)
PP_IN_GAAGAAA(T131, T137, T138, T132, X176, X177, T139) → U21_GAAGAAA(T131, T137, T138, T132, X176, X177, T139, mergesortE_in_gaa(T131, T137, T138))
U21_GAAGAAA(T131, T137, T138, T132, X176, X177, T139, mergesortE_out_gaa(T131, T137, T138)) → PQ_IN_GAAGAA(T132, X176, T138, T137, X177, T139)
PQ_IN_GAAGAA(T132, T144, T146, T137, X177, T145) → MERGESORTE_IN_GAA(T132, T144, T146)
MERGESORTE_IN_GAA(.(T124, .(T125, T126)), X177, .(T129, T130)) → PF_IN_GGGAAAAAAA(T124, T125, T126, X173, X174, T129, T130, X175, X176, X177)
PP_IN_GAAGAAA(T131, T137, T138, T132, X176, X177, T139) → MERGESORTE_IN_GAA(T131, T137, T138)
mergesortA_in_gaa([], [], T5) → mergesortA_out_gaa([], [], T5)
mergesortA_in_gaa(.(T8, []), .(T8, []), T9) → mergesortA_out_gaa(.(T8, []), .(T8, []), T9)
mergesortA_in_gaa(.(T39, .(T40, T41)), T45, .(T46, T44)) → U1_gaa(T39, T40, T41, T45, T46, T44, pB_in_ggaaagaaaa(T40, T41, X63, X62, T44, T39, X35, X36, T45, T46))
pB_in_ggaaagaaaa(T40, T41, T47, T48, T49, T39, X35, X36, T50, T51) → U13_ggaaagaaaa(T40, T41, T47, T48, T49, T39, X35, X36, T50, T51, splitD_in_ggaaa(T40, T41, T47, T48, T49))
splitD_in_ggaaa(T60, T61, .(T60, X91), X92, .(T62, T64)) → U3_ggaaa(T60, T61, X91, X92, T62, T64, splitC_in_gaaa(T61, X92, X91, T64))
splitC_in_gaaa([], [], [], T71) → splitC_out_gaaa([], [], [], T71)
splitC_in_gaaa(.(T80, T81), .(T80, X122), X123, .(T82, T84)) → U2_gaaa(T80, T81, X122, X123, T82, T84, splitC_in_gaaa(T81, X123, X122, T84))
U2_gaaa(T80, T81, X122, X123, T82, T84, splitC_out_gaaa(T81, X123, X122, T84)) → splitC_out_gaaa(.(T80, T81), .(T80, X122), X123, .(T82, T84))
U3_ggaaa(T60, T61, X91, X92, T62, T64, splitC_out_gaaa(T61, X92, X91, T64)) → splitD_out_ggaaa(T60, T61, .(T60, X91), X92, .(T62, T64))
U13_ggaaagaaaa(T40, T41, T47, T48, T49, T39, X35, X36, T50, T51, splitD_out_ggaaa(T40, T41, T47, T48, T49)) → U14_ggaaagaaaa(T40, T41, T47, T48, T49, T39, X35, X36, T50, T51, pN_in_ggaagaaa(T39, T48, X35, T49, T47, X36, T50, T51))
pN_in_ggaagaaa(T39, T48, T87, T88, T47, X36, T89, T90) → U15_ggaagaaa(T39, T48, T87, T88, T47, X36, T89, T90, mergesortA_in_gaa(.(T39, T48), T87, T88))
U15_ggaagaaa(T39, T48, T87, T88, T47, X36, T89, T90, mergesortA_out_gaa(.(T39, T48), T87, T88)) → U16_ggaagaaa(T39, T48, T87, T88, T47, X36, T89, T90, pO_in_gaagaa(T47, X36, T88, T87, T89, T90))
pO_in_gaagaa(T47, T93, T96, T87, T94, T95) → U17_gaagaa(T47, T93, T96, T87, T94, T95, mergesortE_in_gaa(T47, T93, T96))
mergesortE_in_gaa([], [], T103) → mergesortE_out_gaa([], [], T103)
mergesortE_in_gaa(.(T112, []), .(T112, []), T113) → mergesortE_out_gaa(.(T112, []), .(T112, []), T113)
mergesortE_in_gaa(.(T124, .(T125, T126)), X177, .(T129, T130)) → U4_gaa(T124, T125, T126, X177, T129, T130, pF_in_gggaaaaaaa(T124, T125, T126, X173, X174, T129, T130, X175, X176, X177))
pF_in_gggaaaaaaa(T124, T125, T126, T131, T132, T134, T133, X175, X176, X177) → U19_gggaaaaaaa(T124, T125, T126, T131, T132, T134, T133, X175, X176, X177, splitD_in_ggaaa(T124, .(T125, T126), T131, T132, .(T134, T133)))
U19_gggaaaaaaa(T124, T125, T126, T131, T132, T134, T133, X175, X176, X177, splitD_out_ggaaa(T124, .(T125, T126), T131, T132, .(T134, T133))) → U20_gggaaaaaaa(T124, T125, T126, T131, T132, T134, T133, X175, X176, X177, pP_in_gaagaaa(T131, X175, T133, T132, X176, X177, T134))
pP_in_gaagaaa(T131, T137, T138, T132, X176, X177, T139) → U21_gaagaaa(T131, T137, T138, T132, X176, X177, T139, mergesortE_in_gaa(T131, T137, T138))
U21_gaagaaa(T131, T137, T138, T132, X176, X177, T139, mergesortE_out_gaa(T131, T137, T138)) → U22_gaagaaa(T131, T137, T138, T132, X176, X177, T139, pQ_in_gaagaa(T132, X176, T138, T137, X177, T139))
pQ_in_gaagaa(T132, T144, T146, T137, X177, T145) → U23_gaagaa(T132, T144, T146, T137, X177, T145, mergesortE_in_gaa(T132, T144, T146))
U23_gaagaa(T132, T144, T146, T137, X177, T145, mergesortE_out_gaa(T132, T144, T146)) → U24_gaagaa(T132, T144, T146, T137, X177, T145, mergeG_in_ggaaa(T137, T144, X177, T145, T146))
mergeG_in_ggaaa([], T173, T173, T174, T175) → mergeG_out_ggaaa([], T173, T173, T174, T175)
mergeG_in_ggaaa(T188, [], T188, T189, T190) → mergeG_out_ggaaa(T188, [], T188, T189, T190)
mergeG_in_ggaaa(.(T219, T220), .(T221, T222), .(T219, T226), T224, T227) → U5_ggaaa(T219, T220, T221, T222, T226, T224, T227, pH_in_ggggaa(T219, T221, T220, T222, T226, T227))
pH_in_ggggaa(T219, T221, T220, T222, T226, T227) → U25_ggggaa(T219, T221, T220, T222, T226, T227, leJ_in_gg(T219, T221))
leJ_in_gg(s(T240), s(T241)) → U7_gg(T240, T241, leJ_in_gg(T240, T241))
leJ_in_gg(0, s(0)) → leJ_out_gg(0, s(0))
leJ_in_gg(0, 0) → leJ_out_gg(0, 0)
U7_gg(T240, T241, leJ_out_gg(T240, T241)) → leJ_out_gg(s(T240), s(T241))
U25_ggggaa(T219, T221, T220, T222, T226, T227, leJ_out_gg(T219, T221)) → U26_ggggaa(T219, T221, T220, T222, T226, T227, mergeL_in_gggaa(T220, T221, T222, T226, T227))
mergeL_in_gggaa([], T262, T263, .(T262, T263), T264) → mergeL_out_gggaa([], T262, T263, .(T262, T263), T264)
mergeL_in_gggaa(.(T294, T295), T296, T297, .(T294, T301), .(T299, T302)) → U9_gggaa(T294, T295, T296, T297, T301, T299, T302, pH_in_ggggaa(T294, T296, T295, T297, T301, T302))
U9_gggaa(T294, T295, T296, T297, T301, T299, T302, pH_out_ggggaa(T294, T296, T295, T297, T301, T302)) → mergeL_out_gggaa(.(T294, T295), T296, T297, .(T294, T301), .(T299, T302))
mergeL_in_gggaa(.(T319, T320), T321, T322, .(T321, T326), .(T324, T327)) → U10_gggaa(T319, T320, T321, T322, T326, T324, T327, pI_in_ggggaa(T319, T321, T320, T322, T326, T327))
pI_in_ggggaa(T319, T321, T320, T322, T326, T327) → U27_ggggaa(T319, T321, T320, T322, T326, T327, gtK_in_gg(T319, T321))
gtK_in_gg(s(T340), s(T341)) → U8_gg(T340, T341, gtK_in_gg(T340, T341))
gtK_in_gg(s(0), 0) → gtK_out_gg(s(0), 0)
U8_gg(T340, T341, gtK_out_gg(T340, T341)) → gtK_out_gg(s(T340), s(T341))
U27_ggggaa(T319, T321, T320, T322, T326, T327, gtK_out_gg(T319, T321)) → U28_ggggaa(T319, T321, T320, T322, T326, T327, mergeM_in_gggaa(T319, T320, T322, T326, T327))
mergeM_in_gggaa(T356, T357, [], .(T356, T357), T358) → mergeM_out_gggaa(T356, T357, [], .(T356, T357), T358)
mergeM_in_gggaa(T387, T388, .(T389, T390), .(T387, T394), .(T392, T395)) → U11_gggaa(T387, T388, T389, T390, T394, T392, T395, pH_in_ggggaa(T387, T389, T388, T390, T394, T395))
U11_gggaa(T387, T388, T389, T390, T394, T392, T395, pH_out_ggggaa(T387, T389, T388, T390, T394, T395)) → mergeM_out_gggaa(T387, T388, .(T389, T390), .(T387, T394), .(T392, T395))
mergeM_in_gggaa(T412, T413, .(T414, T415), .(T414, T419), .(T417, T420)) → U12_gggaa(T412, T413, T414, T415, T419, T417, T420, pI_in_ggggaa(T412, T414, T413, T415, T419, T420))
U12_gggaa(T412, T413, T414, T415, T419, T417, T420, pI_out_ggggaa(T412, T414, T413, T415, T419, T420)) → mergeM_out_gggaa(T412, T413, .(T414, T415), .(T414, T419), .(T417, T420))
U28_ggggaa(T319, T321, T320, T322, T326, T327, mergeM_out_gggaa(T319, T320, T322, T326, T327)) → pI_out_ggggaa(T319, T321, T320, T322, T326, T327)
U10_gggaa(T319, T320, T321, T322, T326, T324, T327, pI_out_ggggaa(T319, T321, T320, T322, T326, T327)) → mergeL_out_gggaa(.(T319, T320), T321, T322, .(T321, T326), .(T324, T327))
U26_ggggaa(T219, T221, T220, T222, T226, T227, mergeL_out_gggaa(T220, T221, T222, T226, T227)) → pH_out_ggggaa(T219, T221, T220, T222, T226, T227)
U5_ggaaa(T219, T220, T221, T222, T226, T224, T227, pH_out_ggggaa(T219, T221, T220, T222, T226, T227)) → mergeG_out_ggaaa(.(T219, T220), .(T221, T222), .(T219, T226), T224, T227)
mergeG_in_ggaaa(.(T437, T438), .(T439, T440), .(T439, T444), T442, T445) → U6_ggaaa(T437, T438, T439, T440, T444, T442, T445, pI_in_ggggaa(T437, T439, T438, T440, T444, T445))
U6_ggaaa(T437, T438, T439, T440, T444, T442, T445, pI_out_ggggaa(T437, T439, T438, T440, T444, T445)) → mergeG_out_ggaaa(.(T437, T438), .(T439, T440), .(T439, T444), T442, T445)
U24_gaagaa(T132, T144, T146, T137, X177, T145, mergeG_out_ggaaa(T137, T144, X177, T145, T146)) → pQ_out_gaagaa(T132, T144, T146, T137, X177, T145)
U22_gaagaaa(T131, T137, T138, T132, X176, X177, T139, pQ_out_gaagaa(T132, X176, T138, T137, X177, T139)) → pP_out_gaagaaa(T131, T137, T138, T132, X176, X177, T139)
U20_gggaaaaaaa(T124, T125, T126, T131, T132, T134, T133, X175, X176, X177, pP_out_gaagaaa(T131, X175, T133, T132, X176, X177, T134)) → pF_out_gggaaaaaaa(T124, T125, T126, T131, T132, T134, T133, X175, X176, X177)
U4_gaa(T124, T125, T126, X177, T129, T130, pF_out_gggaaaaaaa(T124, T125, T126, X173, X174, T129, T130, X175, X176, X177)) → mergesortE_out_gaa(.(T124, .(T125, T126)), X177, .(T129, T130))
U17_gaagaa(T47, T93, T96, T87, T94, T95, mergesortE_out_gaa(T47, T93, T96)) → U18_gaagaa(T47, T93, T96, T87, T94, T95, mergeG_in_ggaaa(T87, T93, T94, T95, T96))
U18_gaagaa(T47, T93, T96, T87, T94, T95, mergeG_out_ggaaa(T87, T93, T94, T95, T96)) → pO_out_gaagaa(T47, T93, T96, T87, T94, T95)
U16_ggaagaaa(T39, T48, T87, T88, T47, X36, T89, T90, pO_out_gaagaa(T47, X36, T88, T87, T89, T90)) → pN_out_ggaagaaa(T39, T48, T87, T88, T47, X36, T89, T90)
U14_ggaaagaaaa(T40, T41, T47, T48, T49, T39, X35, X36, T50, T51, pN_out_ggaagaaa(T39, T48, X35, T49, T47, X36, T50, T51)) → pB_out_ggaaagaaaa(T40, T41, T47, T48, T49, T39, X35, X36, T50, T51)
U1_gaa(T39, T40, T41, T45, T46, T44, pB_out_ggaaagaaaa(T40, T41, X63, X62, T44, T39, X35, X36, T45, T46)) → mergesortA_out_gaa(.(T39, .(T40, T41)), T45, .(T46, T44))
PF_IN_GGGAAAAAAA(T124, T125, T126, T131, T132, T134, T133, X175, X176, X177) → U19_GGGAAAAAAA(T124, T125, T126, T131, T132, T134, T133, X175, X176, X177, splitD_in_ggaaa(T124, .(T125, T126), T131, T132, .(T134, T133)))
U19_GGGAAAAAAA(T124, T125, T126, T131, T132, T134, T133, X175, X176, X177, splitD_out_ggaaa(T124, .(T125, T126), T131, T132, .(T134, T133))) → PP_IN_GAAGAAA(T131, X175, T133, T132, X176, X177, T134)
PP_IN_GAAGAAA(T131, T137, T138, T132, X176, X177, T139) → U21_GAAGAAA(T131, T137, T138, T132, X176, X177, T139, mergesortE_in_gaa(T131, T137, T138))
U21_GAAGAAA(T131, T137, T138, T132, X176, X177, T139, mergesortE_out_gaa(T131, T137, T138)) → PQ_IN_GAAGAA(T132, X176, T138, T137, X177, T139)
PQ_IN_GAAGAA(T132, T144, T146, T137, X177, T145) → MERGESORTE_IN_GAA(T132, T144, T146)
MERGESORTE_IN_GAA(.(T124, .(T125, T126)), X177, .(T129, T130)) → PF_IN_GGGAAAAAAA(T124, T125, T126, X173, X174, T129, T130, X175, X176, X177)
PP_IN_GAAGAAA(T131, T137, T138, T132, X176, X177, T139) → MERGESORTE_IN_GAA(T131, T137, T138)
splitD_in_ggaaa(T60, T61, .(T60, X91), X92, .(T62, T64)) → U3_ggaaa(T60, T61, X91, X92, T62, T64, splitC_in_gaaa(T61, X92, X91, T64))
mergesortE_in_gaa([], [], T103) → mergesortE_out_gaa([], [], T103)
mergesortE_in_gaa(.(T112, []), .(T112, []), T113) → mergesortE_out_gaa(.(T112, []), .(T112, []), T113)
mergesortE_in_gaa(.(T124, .(T125, T126)), X177, .(T129, T130)) → U4_gaa(T124, T125, T126, X177, T129, T130, pF_in_gggaaaaaaa(T124, T125, T126, X173, X174, T129, T130, X175, X176, X177))
U3_ggaaa(T60, T61, X91, X92, T62, T64, splitC_out_gaaa(T61, X92, X91, T64)) → splitD_out_ggaaa(T60, T61, .(T60, X91), X92, .(T62, T64))
U4_gaa(T124, T125, T126, X177, T129, T130, pF_out_gggaaaaaaa(T124, T125, T126, X173, X174, T129, T130, X175, X176, X177)) → mergesortE_out_gaa(.(T124, .(T125, T126)), X177, .(T129, T130))
splitC_in_gaaa([], [], [], T71) → splitC_out_gaaa([], [], [], T71)
splitC_in_gaaa(.(T80, T81), .(T80, X122), X123, .(T82, T84)) → U2_gaaa(T80, T81, X122, X123, T82, T84, splitC_in_gaaa(T81, X123, X122, T84))
pF_in_gggaaaaaaa(T124, T125, T126, T131, T132, T134, T133, X175, X176, X177) → U19_gggaaaaaaa(T124, T125, T126, T131, T132, T134, T133, X175, X176, X177, splitD_in_ggaaa(T124, .(T125, T126), T131, T132, .(T134, T133)))
U2_gaaa(T80, T81, X122, X123, T82, T84, splitC_out_gaaa(T81, X123, X122, T84)) → splitC_out_gaaa(.(T80, T81), .(T80, X122), X123, .(T82, T84))
U19_gggaaaaaaa(T124, T125, T126, T131, T132, T134, T133, X175, X176, X177, splitD_out_ggaaa(T124, .(T125, T126), T131, T132, .(T134, T133))) → U20_gggaaaaaaa(T124, T125, T126, T131, T132, T134, T133, X175, X176, X177, pP_in_gaagaaa(T131, X175, T133, T132, X176, X177, T134))
U20_gggaaaaaaa(T124, T125, T126, T131, T132, T134, T133, X175, X176, X177, pP_out_gaagaaa(T131, X175, T133, T132, X176, X177, T134)) → pF_out_gggaaaaaaa(T124, T125, T126, T131, T132, T134, T133, X175, X176, X177)
pP_in_gaagaaa(T131, T137, T138, T132, X176, X177, T139) → U21_gaagaaa(T131, T137, T138, T132, X176, X177, T139, mergesortE_in_gaa(T131, T137, T138))
U21_gaagaaa(T131, T137, T138, T132, X176, X177, T139, mergesortE_out_gaa(T131, T137, T138)) → U22_gaagaaa(T131, T137, T138, T132, X176, X177, T139, pQ_in_gaagaa(T132, X176, T138, T137, X177, T139))
U22_gaagaaa(T131, T137, T138, T132, X176, X177, T139, pQ_out_gaagaa(T132, X176, T138, T137, X177, T139)) → pP_out_gaagaaa(T131, T137, T138, T132, X176, X177, T139)
pQ_in_gaagaa(T132, T144, T146, T137, X177, T145) → U23_gaagaa(T132, T144, T146, T137, X177, T145, mergesortE_in_gaa(T132, T144, T146))
U23_gaagaa(T132, T144, T146, T137, X177, T145, mergesortE_out_gaa(T132, T144, T146)) → U24_gaagaa(T132, T144, T146, T137, X177, T145, mergeG_in_ggaaa(T137, T144, X177, T145, T146))
U24_gaagaa(T132, T144, T146, T137, X177, T145, mergeG_out_ggaaa(T137, T144, X177, T145, T146)) → pQ_out_gaagaa(T132, T144, T146, T137, X177, T145)
mergeG_in_ggaaa([], T173, T173, T174, T175) → mergeG_out_ggaaa([], T173, T173, T174, T175)
mergeG_in_ggaaa(T188, [], T188, T189, T190) → mergeG_out_ggaaa(T188, [], T188, T189, T190)
mergeG_in_ggaaa(.(T219, T220), .(T221, T222), .(T219, T226), T224, T227) → U5_ggaaa(T219, T220, T221, T222, T226, T224, T227, pH_in_ggggaa(T219, T221, T220, T222, T226, T227))
mergeG_in_ggaaa(.(T437, T438), .(T439, T440), .(T439, T444), T442, T445) → U6_ggaaa(T437, T438, T439, T440, T444, T442, T445, pI_in_ggggaa(T437, T439, T438, T440, T444, T445))
U5_ggaaa(T219, T220, T221, T222, T226, T224, T227, pH_out_ggggaa(T219, T221, T220, T222, T226, T227)) → mergeG_out_ggaaa(.(T219, T220), .(T221, T222), .(T219, T226), T224, T227)
U6_ggaaa(T437, T438, T439, T440, T444, T442, T445, pI_out_ggggaa(T437, T439, T438, T440, T444, T445)) → mergeG_out_ggaaa(.(T437, T438), .(T439, T440), .(T439, T444), T442, T445)
pH_in_ggggaa(T219, T221, T220, T222, T226, T227) → U25_ggggaa(T219, T221, T220, T222, T226, T227, leJ_in_gg(T219, T221))
pI_in_ggggaa(T319, T321, T320, T322, T326, T327) → U27_ggggaa(T319, T321, T320, T322, T326, T327, gtK_in_gg(T319, T321))
U25_ggggaa(T219, T221, T220, T222, T226, T227, leJ_out_gg(T219, T221)) → U26_ggggaa(T219, T221, T220, T222, T226, T227, mergeL_in_gggaa(T220, T221, T222, T226, T227))
U27_ggggaa(T319, T321, T320, T322, T326, T327, gtK_out_gg(T319, T321)) → U28_ggggaa(T319, T321, T320, T322, T326, T327, mergeM_in_gggaa(T319, T320, T322, T326, T327))
leJ_in_gg(s(T240), s(T241)) → U7_gg(T240, T241, leJ_in_gg(T240, T241))
leJ_in_gg(0, s(0)) → leJ_out_gg(0, s(0))
leJ_in_gg(0, 0) → leJ_out_gg(0, 0)
U26_ggggaa(T219, T221, T220, T222, T226, T227, mergeL_out_gggaa(T220, T221, T222, T226, T227)) → pH_out_ggggaa(T219, T221, T220, T222, T226, T227)
gtK_in_gg(s(T340), s(T341)) → U8_gg(T340, T341, gtK_in_gg(T340, T341))
gtK_in_gg(s(0), 0) → gtK_out_gg(s(0), 0)
U28_ggggaa(T319, T321, T320, T322, T326, T327, mergeM_out_gggaa(T319, T320, T322, T326, T327)) → pI_out_ggggaa(T319, T321, T320, T322, T326, T327)
U7_gg(T240, T241, leJ_out_gg(T240, T241)) → leJ_out_gg(s(T240), s(T241))
mergeL_in_gggaa([], T262, T263, .(T262, T263), T264) → mergeL_out_gggaa([], T262, T263, .(T262, T263), T264)
mergeL_in_gggaa(.(T294, T295), T296, T297, .(T294, T301), .(T299, T302)) → U9_gggaa(T294, T295, T296, T297, T301, T299, T302, pH_in_ggggaa(T294, T296, T295, T297, T301, T302))
mergeL_in_gggaa(.(T319, T320), T321, T322, .(T321, T326), .(T324, T327)) → U10_gggaa(T319, T320, T321, T322, T326, T324, T327, pI_in_ggggaa(T319, T321, T320, T322, T326, T327))
U8_gg(T340, T341, gtK_out_gg(T340, T341)) → gtK_out_gg(s(T340), s(T341))
mergeM_in_gggaa(T356, T357, [], .(T356, T357), T358) → mergeM_out_gggaa(T356, T357, [], .(T356, T357), T358)
mergeM_in_gggaa(T387, T388, .(T389, T390), .(T387, T394), .(T392, T395)) → U11_gggaa(T387, T388, T389, T390, T394, T392, T395, pH_in_ggggaa(T387, T389, T388, T390, T394, T395))
mergeM_in_gggaa(T412, T413, .(T414, T415), .(T414, T419), .(T417, T420)) → U12_gggaa(T412, T413, T414, T415, T419, T417, T420, pI_in_ggggaa(T412, T414, T413, T415, T419, T420))
U9_gggaa(T294, T295, T296, T297, T301, T299, T302, pH_out_ggggaa(T294, T296, T295, T297, T301, T302)) → mergeL_out_gggaa(.(T294, T295), T296, T297, .(T294, T301), .(T299, T302))
U10_gggaa(T319, T320, T321, T322, T326, T324, T327, pI_out_ggggaa(T319, T321, T320, T322, T326, T327)) → mergeL_out_gggaa(.(T319, T320), T321, T322, .(T321, T326), .(T324, T327))
U11_gggaa(T387, T388, T389, T390, T394, T392, T395, pH_out_ggggaa(T387, T389, T388, T390, T394, T395)) → mergeM_out_gggaa(T387, T388, .(T389, T390), .(T387, T394), .(T392, T395))
U12_gggaa(T412, T413, T414, T415, T419, T417, T420, pI_out_ggggaa(T412, T414, T413, T415, T419, T420)) → mergeM_out_gggaa(T412, T413, .(T414, T415), .(T414, T419), .(T417, T420))
PF_IN_GGGAAAAAAA(T124, T125, T126) → U19_GGGAAAAAAA(T124, T125, T126, splitD_in_ggaaa(T124, .(T125, T126)))
U19_GGGAAAAAAA(T124, T125, T126, splitD_out_ggaaa(T124, .(T125, T126), T131, T132)) → PP_IN_GAAGAAA(T131, T132)
PP_IN_GAAGAAA(T131, T132) → U21_GAAGAAA(T131, T132, mergesortE_in_gaa(T131))
U21_GAAGAAA(T131, T132, mergesortE_out_gaa(T131, T137)) → PQ_IN_GAAGAA(T132, T137)
PQ_IN_GAAGAA(T132, T137) → MERGESORTE_IN_GAA(T132)
MERGESORTE_IN_GAA(.(T124, .(T125, T126))) → PF_IN_GGGAAAAAAA(T124, T125, T126)
PP_IN_GAAGAAA(T131, T132) → MERGESORTE_IN_GAA(T131)
splitD_in_ggaaa(T60, T61) → U3_ggaaa(T60, T61, splitC_in_gaaa(T61))
mergesortE_in_gaa([]) → mergesortE_out_gaa([], [])
mergesortE_in_gaa(.(T112, [])) → mergesortE_out_gaa(.(T112, []), .(T112, []))
mergesortE_in_gaa(.(T124, .(T125, T126))) → U4_gaa(T124, T125, T126, pF_in_gggaaaaaaa(T124, T125, T126))
U3_ggaaa(T60, T61, splitC_out_gaaa(T61, X92, X91)) → splitD_out_ggaaa(T60, T61, .(T60, X91), X92)
U4_gaa(T124, T125, T126, pF_out_gggaaaaaaa(T124, T125, T126, X173, X174, X175, X176, X177)) → mergesortE_out_gaa(.(T124, .(T125, T126)), X177)
splitC_in_gaaa([]) → splitC_out_gaaa([], [], [])
splitC_in_gaaa(.(T80, T81)) → U2_gaaa(T80, T81, splitC_in_gaaa(T81))
pF_in_gggaaaaaaa(T124, T125, T126) → U19_gggaaaaaaa(T124, T125, T126, splitD_in_ggaaa(T124, .(T125, T126)))
U2_gaaa(T80, T81, splitC_out_gaaa(T81, X123, X122)) → splitC_out_gaaa(.(T80, T81), .(T80, X122), X123)
U19_gggaaaaaaa(T124, T125, T126, splitD_out_ggaaa(T124, .(T125, T126), T131, T132)) → U20_gggaaaaaaa(T124, T125, T126, T131, T132, pP_in_gaagaaa(T131, T132))
U20_gggaaaaaaa(T124, T125, T126, T131, T132, pP_out_gaagaaa(T131, X175, T132, X176, X177)) → pF_out_gggaaaaaaa(T124, T125, T126, T131, T132, X175, X176, X177)
pP_in_gaagaaa(T131, T132) → U21_gaagaaa(T131, T132, mergesortE_in_gaa(T131))
U21_gaagaaa(T131, T132, mergesortE_out_gaa(T131, T137)) → U22_gaagaaa(T131, T137, T132, pQ_in_gaagaa(T132, T137))
U22_gaagaaa(T131, T137, T132, pQ_out_gaagaa(T132, X176, T137, X177)) → pP_out_gaagaaa(T131, T137, T132, X176, X177)
pQ_in_gaagaa(T132, T137) → U23_gaagaa(T132, T137, mergesortE_in_gaa(T132))
U23_gaagaa(T132, T137, mergesortE_out_gaa(T132, T144)) → U24_gaagaa(T132, T144, T137, mergeG_in_ggaaa(T137, T144))
U24_gaagaa(T132, T144, T137, mergeG_out_ggaaa(T137, T144, X177)) → pQ_out_gaagaa(T132, T144, T137, X177)
mergeG_in_ggaaa([], T173) → mergeG_out_ggaaa([], T173, T173)
mergeG_in_ggaaa(T188, []) → mergeG_out_ggaaa(T188, [], T188)
mergeG_in_ggaaa(.(T219, T220), .(T221, T222)) → U5_ggaaa(T219, T220, T221, T222, pH_in_ggggaa(T219, T221, T220, T222))
mergeG_in_ggaaa(.(T437, T438), .(T439, T440)) → U6_ggaaa(T437, T438, T439, T440, pI_in_ggggaa(T437, T439, T438, T440))
U5_ggaaa(T219, T220, T221, T222, pH_out_ggggaa(T219, T221, T220, T222, T226)) → mergeG_out_ggaaa(.(T219, T220), .(T221, T222), .(T219, T226))
U6_ggaaa(T437, T438, T439, T440, pI_out_ggggaa(T437, T439, T438, T440, T444)) → mergeG_out_ggaaa(.(T437, T438), .(T439, T440), .(T439, T444))
pH_in_ggggaa(T219, T221, T220, T222) → U25_ggggaa(T219, T221, T220, T222, leJ_in_gg(T219, T221))
pI_in_ggggaa(T319, T321, T320, T322) → U27_ggggaa(T319, T321, T320, T322, gtK_in_gg(T319, T321))
U25_ggggaa(T219, T221, T220, T222, leJ_out_gg(T219, T221)) → U26_ggggaa(T219, T221, T220, T222, mergeL_in_gggaa(T220, T221, T222))
U27_ggggaa(T319, T321, T320, T322, gtK_out_gg(T319, T321)) → U28_ggggaa(T319, T321, T320, T322, mergeM_in_gggaa(T319, T320, T322))
leJ_in_gg(s(T240), s(T241)) → U7_gg(T240, T241, leJ_in_gg(T240, T241))
leJ_in_gg(0, s(0)) → leJ_out_gg(0, s(0))
leJ_in_gg(0, 0) → leJ_out_gg(0, 0)
U26_ggggaa(T219, T221, T220, T222, mergeL_out_gggaa(T220, T221, T222, T226)) → pH_out_ggggaa(T219, T221, T220, T222, T226)
gtK_in_gg(s(T340), s(T341)) → U8_gg(T340, T341, gtK_in_gg(T340, T341))
gtK_in_gg(s(0), 0) → gtK_out_gg(s(0), 0)
U28_ggggaa(T319, T321, T320, T322, mergeM_out_gggaa(T319, T320, T322, T326)) → pI_out_ggggaa(T319, T321, T320, T322, T326)
U7_gg(T240, T241, leJ_out_gg(T240, T241)) → leJ_out_gg(s(T240), s(T241))
mergeL_in_gggaa([], T262, T263) → mergeL_out_gggaa([], T262, T263, .(T262, T263))
mergeL_in_gggaa(.(T294, T295), T296, T297) → U9_gggaa(T294, T295, T296, T297, pH_in_ggggaa(T294, T296, T295, T297))
mergeL_in_gggaa(.(T319, T320), T321, T322) → U10_gggaa(T319, T320, T321, T322, pI_in_ggggaa(T319, T321, T320, T322))
U8_gg(T340, T341, gtK_out_gg(T340, T341)) → gtK_out_gg(s(T340), s(T341))
mergeM_in_gggaa(T356, T357, []) → mergeM_out_gggaa(T356, T357, [], .(T356, T357))
mergeM_in_gggaa(T387, T388, .(T389, T390)) → U11_gggaa(T387, T388, T389, T390, pH_in_ggggaa(T387, T389, T388, T390))
mergeM_in_gggaa(T412, T413, .(T414, T415)) → U12_gggaa(T412, T413, T414, T415, pI_in_ggggaa(T412, T414, T413, T415))
U9_gggaa(T294, T295, T296, T297, pH_out_ggggaa(T294, T296, T295, T297, T301)) → mergeL_out_gggaa(.(T294, T295), T296, T297, .(T294, T301))
U10_gggaa(T319, T320, T321, T322, pI_out_ggggaa(T319, T321, T320, T322, T326)) → mergeL_out_gggaa(.(T319, T320), T321, T322, .(T321, T326))
U11_gggaa(T387, T388, T389, T390, pH_out_ggggaa(T387, T389, T388, T390, T394)) → mergeM_out_gggaa(T387, T388, .(T389, T390), .(T387, T394))
U12_gggaa(T412, T413, T414, T415, pI_out_ggggaa(T412, T414, T413, T415, T419)) → mergeM_out_gggaa(T412, T413, .(T414, T415), .(T414, T419))
splitD_in_ggaaa(x0, x1)
mergesortE_in_gaa(x0)
U3_ggaaa(x0, x1, x2)
U4_gaa(x0, x1, x2, x3)
splitC_in_gaaa(x0)
pF_in_gggaaaaaaa(x0, x1, x2)
U2_gaaa(x0, x1, x2)
U19_gggaaaaaaa(x0, x1, x2, x3)
U20_gggaaaaaaa(x0, x1, x2, x3, x4, x5)
pP_in_gaagaaa(x0, x1)
U21_gaagaaa(x0, x1, x2)
U22_gaagaaa(x0, x1, x2, x3)
pQ_in_gaagaa(x0, x1)
U23_gaagaa(x0, x1, x2)
U24_gaagaa(x0, x1, x2, x3)
mergeG_in_ggaaa(x0, x1)
U5_ggaaa(x0, x1, x2, x3, x4)
U6_ggaaa(x0, x1, x2, x3, x4)
pH_in_ggggaa(x0, x1, x2, x3)
pI_in_ggggaa(x0, x1, x2, x3)
U25_ggggaa(x0, x1, x2, x3, x4)
U27_ggggaa(x0, x1, x2, x3, x4)
leJ_in_gg(x0, x1)
U26_ggggaa(x0, x1, x2, x3, x4)
gtK_in_gg(x0, x1)
U28_ggggaa(x0, x1, x2, x3, x4)
U7_gg(x0, x1, x2)
mergeL_in_gggaa(x0, x1, x2)
U8_gg(x0, x1, x2)
mergeM_in_gggaa(x0, x1, x2)
U9_gggaa(x0, x1, x2, x3, x4)
U10_gggaa(x0, x1, x2, x3, x4)
U11_gggaa(x0, x1, x2, x3, x4)
U12_gggaa(x0, x1, x2, x3, x4)
PF_IN_GGGAAAAAAA(T124, T125, T126) → U19_GGGAAAAAAA(T124, T125, T126, U3_ggaaa(T124, .(T125, T126), splitC_in_gaaa(.(T125, T126))))
U19_GGGAAAAAAA(T124, T125, T126, splitD_out_ggaaa(T124, .(T125, T126), T131, T132)) → PP_IN_GAAGAAA(T131, T132)
PP_IN_GAAGAAA(T131, T132) → U21_GAAGAAA(T131, T132, mergesortE_in_gaa(T131))
U21_GAAGAAA(T131, T132, mergesortE_out_gaa(T131, T137)) → PQ_IN_GAAGAA(T132, T137)
PQ_IN_GAAGAA(T132, T137) → MERGESORTE_IN_GAA(T132)
MERGESORTE_IN_GAA(.(T124, .(T125, T126))) → PF_IN_GGGAAAAAAA(T124, T125, T126)
PP_IN_GAAGAAA(T131, T132) → MERGESORTE_IN_GAA(T131)
PF_IN_GGGAAAAAAA(T124, T125, T126) → U19_GGGAAAAAAA(T124, T125, T126, U3_ggaaa(T124, .(T125, T126), splitC_in_gaaa(.(T125, T126))))
splitD_in_ggaaa(T60, T61) → U3_ggaaa(T60, T61, splitC_in_gaaa(T61))
mergesortE_in_gaa([]) → mergesortE_out_gaa([], [])
mergesortE_in_gaa(.(T112, [])) → mergesortE_out_gaa(.(T112, []), .(T112, []))
mergesortE_in_gaa(.(T124, .(T125, T126))) → U4_gaa(T124, T125, T126, pF_in_gggaaaaaaa(T124, T125, T126))
U3_ggaaa(T60, T61, splitC_out_gaaa(T61, X92, X91)) → splitD_out_ggaaa(T60, T61, .(T60, X91), X92)
U4_gaa(T124, T125, T126, pF_out_gggaaaaaaa(T124, T125, T126, X173, X174, X175, X176, X177)) → mergesortE_out_gaa(.(T124, .(T125, T126)), X177)
splitC_in_gaaa([]) → splitC_out_gaaa([], [], [])
splitC_in_gaaa(.(T80, T81)) → U2_gaaa(T80, T81, splitC_in_gaaa(T81))
pF_in_gggaaaaaaa(T124, T125, T126) → U19_gggaaaaaaa(T124, T125, T126, splitD_in_ggaaa(T124, .(T125, T126)))
U2_gaaa(T80, T81, splitC_out_gaaa(T81, X123, X122)) → splitC_out_gaaa(.(T80, T81), .(T80, X122), X123)
U19_gggaaaaaaa(T124, T125, T126, splitD_out_ggaaa(T124, .(T125, T126), T131, T132)) → U20_gggaaaaaaa(T124, T125, T126, T131, T132, pP_in_gaagaaa(T131, T132))
U20_gggaaaaaaa(T124, T125, T126, T131, T132, pP_out_gaagaaa(T131, X175, T132, X176, X177)) → pF_out_gggaaaaaaa(T124, T125, T126, T131, T132, X175, X176, X177)
pP_in_gaagaaa(T131, T132) → U21_gaagaaa(T131, T132, mergesortE_in_gaa(T131))
U21_gaagaaa(T131, T132, mergesortE_out_gaa(T131, T137)) → U22_gaagaaa(T131, T137, T132, pQ_in_gaagaa(T132, T137))
U22_gaagaaa(T131, T137, T132, pQ_out_gaagaa(T132, X176, T137, X177)) → pP_out_gaagaaa(T131, T137, T132, X176, X177)
pQ_in_gaagaa(T132, T137) → U23_gaagaa(T132, T137, mergesortE_in_gaa(T132))
U23_gaagaa(T132, T137, mergesortE_out_gaa(T132, T144)) → U24_gaagaa(T132, T144, T137, mergeG_in_ggaaa(T137, T144))
U24_gaagaa(T132, T144, T137, mergeG_out_ggaaa(T137, T144, X177)) → pQ_out_gaagaa(T132, T144, T137, X177)
mergeG_in_ggaaa([], T173) → mergeG_out_ggaaa([], T173, T173)
mergeG_in_ggaaa(T188, []) → mergeG_out_ggaaa(T188, [], T188)
mergeG_in_ggaaa(.(T219, T220), .(T221, T222)) → U5_ggaaa(T219, T220, T221, T222, pH_in_ggggaa(T219, T221, T220, T222))
mergeG_in_ggaaa(.(T437, T438), .(T439, T440)) → U6_ggaaa(T437, T438, T439, T440, pI_in_ggggaa(T437, T439, T438, T440))
U5_ggaaa(T219, T220, T221, T222, pH_out_ggggaa(T219, T221, T220, T222, T226)) → mergeG_out_ggaaa(.(T219, T220), .(T221, T222), .(T219, T226))
U6_ggaaa(T437, T438, T439, T440, pI_out_ggggaa(T437, T439, T438, T440, T444)) → mergeG_out_ggaaa(.(T437, T438), .(T439, T440), .(T439, T444))
pH_in_ggggaa(T219, T221, T220, T222) → U25_ggggaa(T219, T221, T220, T222, leJ_in_gg(T219, T221))
pI_in_ggggaa(T319, T321, T320, T322) → U27_ggggaa(T319, T321, T320, T322, gtK_in_gg(T319, T321))
U25_ggggaa(T219, T221, T220, T222, leJ_out_gg(T219, T221)) → U26_ggggaa(T219, T221, T220, T222, mergeL_in_gggaa(T220, T221, T222))
U27_ggggaa(T319, T321, T320, T322, gtK_out_gg(T319, T321)) → U28_ggggaa(T319, T321, T320, T322, mergeM_in_gggaa(T319, T320, T322))
leJ_in_gg(s(T240), s(T241)) → U7_gg(T240, T241, leJ_in_gg(T240, T241))
leJ_in_gg(0, s(0)) → leJ_out_gg(0, s(0))
leJ_in_gg(0, 0) → leJ_out_gg(0, 0)
U26_ggggaa(T219, T221, T220, T222, mergeL_out_gggaa(T220, T221, T222, T226)) → pH_out_ggggaa(T219, T221, T220, T222, T226)
gtK_in_gg(s(T340), s(T341)) → U8_gg(T340, T341, gtK_in_gg(T340, T341))
gtK_in_gg(s(0), 0) → gtK_out_gg(s(0), 0)
U28_ggggaa(T319, T321, T320, T322, mergeM_out_gggaa(T319, T320, T322, T326)) → pI_out_ggggaa(T319, T321, T320, T322, T326)
U7_gg(T240, T241, leJ_out_gg(T240, T241)) → leJ_out_gg(s(T240), s(T241))
mergeL_in_gggaa([], T262, T263) → mergeL_out_gggaa([], T262, T263, .(T262, T263))
mergeL_in_gggaa(.(T294, T295), T296, T297) → U9_gggaa(T294, T295, T296, T297, pH_in_ggggaa(T294, T296, T295, T297))
mergeL_in_gggaa(.(T319, T320), T321, T322) → U10_gggaa(T319, T320, T321, T322, pI_in_ggggaa(T319, T321, T320, T322))
U8_gg(T340, T341, gtK_out_gg(T340, T341)) → gtK_out_gg(s(T340), s(T341))
mergeM_in_gggaa(T356, T357, []) → mergeM_out_gggaa(T356, T357, [], .(T356, T357))
mergeM_in_gggaa(T387, T388, .(T389, T390)) → U11_gggaa(T387, T388, T389, T390, pH_in_ggggaa(T387, T389, T388, T390))
mergeM_in_gggaa(T412, T413, .(T414, T415)) → U12_gggaa(T412, T413, T414, T415, pI_in_ggggaa(T412, T414, T413, T415))
U9_gggaa(T294, T295, T296, T297, pH_out_ggggaa(T294, T296, T295, T297, T301)) → mergeL_out_gggaa(.(T294, T295), T296, T297, .(T294, T301))
U10_gggaa(T319, T320, T321, T322, pI_out_ggggaa(T319, T321, T320, T322, T326)) → mergeL_out_gggaa(.(T319, T320), T321, T322, .(T321, T326))
U11_gggaa(T387, T388, T389, T390, pH_out_ggggaa(T387, T389, T388, T390, T394)) → mergeM_out_gggaa(T387, T388, .(T389, T390), .(T387, T394))
U12_gggaa(T412, T413, T414, T415, pI_out_ggggaa(T412, T414, T413, T415, T419)) → mergeM_out_gggaa(T412, T413, .(T414, T415), .(T414, T419))
splitD_in_ggaaa(x0, x1)
mergesortE_in_gaa(x0)
U3_ggaaa(x0, x1, x2)
U4_gaa(x0, x1, x2, x3)
splitC_in_gaaa(x0)
pF_in_gggaaaaaaa(x0, x1, x2)
U2_gaaa(x0, x1, x2)
U19_gggaaaaaaa(x0, x1, x2, x3)
U20_gggaaaaaaa(x0, x1, x2, x3, x4, x5)
pP_in_gaagaaa(x0, x1)
U21_gaagaaa(x0, x1, x2)
U22_gaagaaa(x0, x1, x2, x3)
pQ_in_gaagaa(x0, x1)
U23_gaagaa(x0, x1, x2)
U24_gaagaa(x0, x1, x2, x3)
mergeG_in_ggaaa(x0, x1)
U5_ggaaa(x0, x1, x2, x3, x4)
U6_ggaaa(x0, x1, x2, x3, x4)
pH_in_ggggaa(x0, x1, x2, x3)
pI_in_ggggaa(x0, x1, x2, x3)
U25_ggggaa(x0, x1, x2, x3, x4)
U27_ggggaa(x0, x1, x2, x3, x4)
leJ_in_gg(x0, x1)
U26_ggggaa(x0, x1, x2, x3, x4)
gtK_in_gg(x0, x1)
U28_ggggaa(x0, x1, x2, x3, x4)
U7_gg(x0, x1, x2)
mergeL_in_gggaa(x0, x1, x2)
U8_gg(x0, x1, x2)
mergeM_in_gggaa(x0, x1, x2)
U9_gggaa(x0, x1, x2, x3, x4)
U10_gggaa(x0, x1, x2, x3, x4)
U11_gggaa(x0, x1, x2, x3, x4)
U12_gggaa(x0, x1, x2, x3, x4)
PF_IN_GGGAAAAAAA(T124, T125, T126) → U19_GGGAAAAAAA(T124, T125, T126, U3_ggaaa(T124, .(T125, T126), U2_gaaa(T125, T126, splitC_in_gaaa(T126))))
U19_GGGAAAAAAA(T124, T125, T126, splitD_out_ggaaa(T124, .(T125, T126), T131, T132)) → PP_IN_GAAGAAA(T131, T132)
PP_IN_GAAGAAA(T131, T132) → U21_GAAGAAA(T131, T132, mergesortE_in_gaa(T131))
U21_GAAGAAA(T131, T132, mergesortE_out_gaa(T131, T137)) → PQ_IN_GAAGAA(T132, T137)
PQ_IN_GAAGAA(T132, T137) → MERGESORTE_IN_GAA(T132)
MERGESORTE_IN_GAA(.(T124, .(T125, T126))) → PF_IN_GGGAAAAAAA(T124, T125, T126)
PP_IN_GAAGAAA(T131, T132) → MERGESORTE_IN_GAA(T131)
PF_IN_GGGAAAAAAA(T124, T125, T126) → U19_GGGAAAAAAA(T124, T125, T126, U3_ggaaa(T124, .(T125, T126), U2_gaaa(T125, T126, splitC_in_gaaa(T126))))
splitD_in_ggaaa(T60, T61) → U3_ggaaa(T60, T61, splitC_in_gaaa(T61))
mergesortE_in_gaa([]) → mergesortE_out_gaa([], [])
mergesortE_in_gaa(.(T112, [])) → mergesortE_out_gaa(.(T112, []), .(T112, []))
mergesortE_in_gaa(.(T124, .(T125, T126))) → U4_gaa(T124, T125, T126, pF_in_gggaaaaaaa(T124, T125, T126))
U3_ggaaa(T60, T61, splitC_out_gaaa(T61, X92, X91)) → splitD_out_ggaaa(T60, T61, .(T60, X91), X92)
U4_gaa(T124, T125, T126, pF_out_gggaaaaaaa(T124, T125, T126, X173, X174, X175, X176, X177)) → mergesortE_out_gaa(.(T124, .(T125, T126)), X177)
splitC_in_gaaa([]) → splitC_out_gaaa([], [], [])
splitC_in_gaaa(.(T80, T81)) → U2_gaaa(T80, T81, splitC_in_gaaa(T81))
pF_in_gggaaaaaaa(T124, T125, T126) → U19_gggaaaaaaa(T124, T125, T126, splitD_in_ggaaa(T124, .(T125, T126)))
U2_gaaa(T80, T81, splitC_out_gaaa(T81, X123, X122)) → splitC_out_gaaa(.(T80, T81), .(T80, X122), X123)
U19_gggaaaaaaa(T124, T125, T126, splitD_out_ggaaa(T124, .(T125, T126), T131, T132)) → U20_gggaaaaaaa(T124, T125, T126, T131, T132, pP_in_gaagaaa(T131, T132))
U20_gggaaaaaaa(T124, T125, T126, T131, T132, pP_out_gaagaaa(T131, X175, T132, X176, X177)) → pF_out_gggaaaaaaa(T124, T125, T126, T131, T132, X175, X176, X177)
pP_in_gaagaaa(T131, T132) → U21_gaagaaa(T131, T132, mergesortE_in_gaa(T131))
U21_gaagaaa(T131, T132, mergesortE_out_gaa(T131, T137)) → U22_gaagaaa(T131, T137, T132, pQ_in_gaagaa(T132, T137))
U22_gaagaaa(T131, T137, T132, pQ_out_gaagaa(T132, X176, T137, X177)) → pP_out_gaagaaa(T131, T137, T132, X176, X177)
pQ_in_gaagaa(T132, T137) → U23_gaagaa(T132, T137, mergesortE_in_gaa(T132))
U23_gaagaa(T132, T137, mergesortE_out_gaa(T132, T144)) → U24_gaagaa(T132, T144, T137, mergeG_in_ggaaa(T137, T144))
U24_gaagaa(T132, T144, T137, mergeG_out_ggaaa(T137, T144, X177)) → pQ_out_gaagaa(T132, T144, T137, X177)
mergeG_in_ggaaa([], T173) → mergeG_out_ggaaa([], T173, T173)
mergeG_in_ggaaa(T188, []) → mergeG_out_ggaaa(T188, [], T188)
mergeG_in_ggaaa(.(T219, T220), .(T221, T222)) → U5_ggaaa(T219, T220, T221, T222, pH_in_ggggaa(T219, T221, T220, T222))
mergeG_in_ggaaa(.(T437, T438), .(T439, T440)) → U6_ggaaa(T437, T438, T439, T440, pI_in_ggggaa(T437, T439, T438, T440))
U5_ggaaa(T219, T220, T221, T222, pH_out_ggggaa(T219, T221, T220, T222, T226)) → mergeG_out_ggaaa(.(T219, T220), .(T221, T222), .(T219, T226))
U6_ggaaa(T437, T438, T439, T440, pI_out_ggggaa(T437, T439, T438, T440, T444)) → mergeG_out_ggaaa(.(T437, T438), .(T439, T440), .(T439, T444))
pH_in_ggggaa(T219, T221, T220, T222) → U25_ggggaa(T219, T221, T220, T222, leJ_in_gg(T219, T221))
pI_in_ggggaa(T319, T321, T320, T322) → U27_ggggaa(T319, T321, T320, T322, gtK_in_gg(T319, T321))
U25_ggggaa(T219, T221, T220, T222, leJ_out_gg(T219, T221)) → U26_ggggaa(T219, T221, T220, T222, mergeL_in_gggaa(T220, T221, T222))
U27_ggggaa(T319, T321, T320, T322, gtK_out_gg(T319, T321)) → U28_ggggaa(T319, T321, T320, T322, mergeM_in_gggaa(T319, T320, T322))
leJ_in_gg(s(T240), s(T241)) → U7_gg(T240, T241, leJ_in_gg(T240, T241))
leJ_in_gg(0, s(0)) → leJ_out_gg(0, s(0))
leJ_in_gg(0, 0) → leJ_out_gg(0, 0)
U26_ggggaa(T219, T221, T220, T222, mergeL_out_gggaa(T220, T221, T222, T226)) → pH_out_ggggaa(T219, T221, T220, T222, T226)
gtK_in_gg(s(T340), s(T341)) → U8_gg(T340, T341, gtK_in_gg(T340, T341))
gtK_in_gg(s(0), 0) → gtK_out_gg(s(0), 0)
U28_ggggaa(T319, T321, T320, T322, mergeM_out_gggaa(T319, T320, T322, T326)) → pI_out_ggggaa(T319, T321, T320, T322, T326)
U7_gg(T240, T241, leJ_out_gg(T240, T241)) → leJ_out_gg(s(T240), s(T241))
mergeL_in_gggaa([], T262, T263) → mergeL_out_gggaa([], T262, T263, .(T262, T263))
mergeL_in_gggaa(.(T294, T295), T296, T297) → U9_gggaa(T294, T295, T296, T297, pH_in_ggggaa(T294, T296, T295, T297))
mergeL_in_gggaa(.(T319, T320), T321, T322) → U10_gggaa(T319, T320, T321, T322, pI_in_ggggaa(T319, T321, T320, T322))
U8_gg(T340, T341, gtK_out_gg(T340, T341)) → gtK_out_gg(s(T340), s(T341))
mergeM_in_gggaa(T356, T357, []) → mergeM_out_gggaa(T356, T357, [], .(T356, T357))
mergeM_in_gggaa(T387, T388, .(T389, T390)) → U11_gggaa(T387, T388, T389, T390, pH_in_ggggaa(T387, T389, T388, T390))
mergeM_in_gggaa(T412, T413, .(T414, T415)) → U12_gggaa(T412, T413, T414, T415, pI_in_ggggaa(T412, T414, T413, T415))
U9_gggaa(T294, T295, T296, T297, pH_out_ggggaa(T294, T296, T295, T297, T301)) → mergeL_out_gggaa(.(T294, T295), T296, T297, .(T294, T301))
U10_gggaa(T319, T320, T321, T322, pI_out_ggggaa(T319, T321, T320, T322, T326)) → mergeL_out_gggaa(.(T319, T320), T321, T322, .(T321, T326))
U11_gggaa(T387, T388, T389, T390, pH_out_ggggaa(T387, T389, T388, T390, T394)) → mergeM_out_gggaa(T387, T388, .(T389, T390), .(T387, T394))
U12_gggaa(T412, T413, T414, T415, pI_out_ggggaa(T412, T414, T413, T415, T419)) → mergeM_out_gggaa(T412, T413, .(T414, T415), .(T414, T419))
splitD_in_ggaaa(x0, x1)
mergesortE_in_gaa(x0)
U3_ggaaa(x0, x1, x2)
U4_gaa(x0, x1, x2, x3)
splitC_in_gaaa(x0)
pF_in_gggaaaaaaa(x0, x1, x2)
U2_gaaa(x0, x1, x2)
U19_gggaaaaaaa(x0, x1, x2, x3)
U20_gggaaaaaaa(x0, x1, x2, x3, x4, x5)
pP_in_gaagaaa(x0, x1)
U21_gaagaaa(x0, x1, x2)
U22_gaagaaa(x0, x1, x2, x3)
pQ_in_gaagaa(x0, x1)
U23_gaagaa(x0, x1, x2)
U24_gaagaa(x0, x1, x2, x3)
mergeG_in_ggaaa(x0, x1)
U5_ggaaa(x0, x1, x2, x3, x4)
U6_ggaaa(x0, x1, x2, x3, x4)
pH_in_ggggaa(x0, x1, x2, x3)
pI_in_ggggaa(x0, x1, x2, x3)
U25_ggggaa(x0, x1, x2, x3, x4)
U27_ggggaa(x0, x1, x2, x3, x4)
leJ_in_gg(x0, x1)
U26_ggggaa(x0, x1, x2, x3, x4)
gtK_in_gg(x0, x1)
U28_ggggaa(x0, x1, x2, x3, x4)
U7_gg(x0, x1, x2)
mergeL_in_gggaa(x0, x1, x2)
U8_gg(x0, x1, x2)
mergeM_in_gggaa(x0, x1, x2)
U9_gggaa(x0, x1, x2, x3, x4)
U10_gggaa(x0, x1, x2, x3, x4)
U11_gggaa(x0, x1, x2, x3, x4)
U12_gggaa(x0, x1, x2, x3, x4)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
MERGESORTE_IN_GAA(.(T124, .(T125, T126))) → PF_IN_GGGAAAAAAA(T124, T125, T126)
POL( U21_GAAGAAA(x1, ..., x3) ) = x2
POL( mergesortE_in_gaa(x1) ) = 0
POL( [] ) = 0
POL( mergesortE_out_gaa(x1, x2) ) = 2x2 + 2
POL( .(x1, x2) ) = 2x2 + 1
POL( U4_gaa(x1, ..., x4) ) = max{0, -1}
POL( pF_in_gggaaaaaaa(x1, ..., x3) ) = x1 + 2x3
POL( U19_GGGAAAAAAA(x1, ..., x4) ) = x4 + 1
POL( U2_gaaa(x1, ..., x3) ) = 2x3 + 1
POL( U3_ggaaa(x1, ..., x3) ) = x3
POL( U19_gggaaaaaaa(x1, ..., x4) ) = max{0, -2}
POL( splitC_in_gaaa(x1) ) = x1
POL( splitC_out_gaaa(x1, ..., x3) ) = x2 + 2x3
POL( splitD_out_ggaaa(x1, ..., x4) ) = max{0, x3 + x4 - 1}
POL( U20_gggaaaaaaa(x1, ..., x6) ) = max{0, 2x1 + x2 + x4 + x5 + 2x6 - 1}
POL( pP_in_gaagaaa(x1, x2) ) = 2x1
POL( pP_out_gaagaaa(x1, ..., x5) ) = 2x2 + x4 + x5 + 2
POL( pF_out_gggaaaaaaa(x1, ..., x8) ) = 2x1 + 2x2 + 2x3 + 2x4 + 2x5 + 2x6 + 2x7 + x8
POL( U21_gaagaaa(x1, ..., x3) ) = 2x2 + 2
POL( splitD_in_ggaaa(x1, x2) ) = max{0, -2}
POL( U22_gaagaaa(x1, ..., x4) ) = x1 + x2 + x3
POL( pQ_in_gaagaa(x1, x2) ) = 2x1 + x2 + 1
POL( pQ_out_gaagaa(x1, ..., x4) ) = x1 + 2x2 + x3 + x4 + 2
POL( U23_gaagaa(x1, ..., x3) ) = x1 + 2x2 + 2x3 + 2
POL( U24_gaagaa(x1, ..., x4) ) = 2x1 + x2 + 2x3
POL( mergeG_in_ggaaa(x1, x2) ) = 0
POL( mergeG_out_ggaaa(x1, ..., x3) ) = max{0, x2 - 2}
POL( U5_ggaaa(x1, ..., x5) ) = 2x1 + x3 + 2x5 + 2
POL( pH_in_ggggaa(x1, ..., x4) ) = x1 + x3
POL( U6_ggaaa(x1, ..., x5) ) = x1 + 2x5 + 2
POL( pI_in_ggggaa(x1, ..., x4) ) = 2x2 + 2x3 + x4 + 2
POL( U25_ggggaa(x1, ..., x5) ) = max{0, x1 + x3 + x4 - 1}
POL( leJ_in_gg(x1, x2) ) = 2x2
POL( pH_out_ggggaa(x1, ..., x5) ) = x2 + 2x4
POL( U27_ggggaa(x1, ..., x5) ) = max{0, -2}
POL( gtK_in_gg(x1, x2) ) = 0
POL( pI_out_ggggaa(x1, ..., x5) ) = 2x3 + 2x4 + x5
POL( leJ_out_gg(x1, x2) ) = 1
POL( U26_ggggaa(x1, ..., x5) ) = max{0, 2x2 + x4 - 2}
POL( mergeL_in_gggaa(x1, ..., x3) ) = x2
POL( mergeL_out_gggaa(x1, ..., x4) ) = max{0, 2x1 + x2 + 2x3 + x4 - 2}
POL( U9_gggaa(x1, ..., x5) ) = 2x2 + 2x3 + x4 + 2x5 + 1
POL( s(x1) ) = 2x1 + 1
POL( U7_gg(x1, ..., x3) ) = max{0, -2}
POL( 0 ) = 0
POL( U10_gggaa(x1, ..., x5) ) = max{0, x4 - 2}
POL( U8_gg(x1, ..., x3) ) = x2 + 2
POL( gtK_out_gg(x1, x2) ) = max{0, x2 - 2}
POL( U28_ggggaa(x1, ..., x5) ) = x1 + 2x2 + x3 + 2x4 + x5 + 2
POL( mergeM_in_gggaa(x1, ..., x3) ) = 2x1 + x2 + x3 + 2
POL( mergeM_out_gggaa(x1, ..., x4) ) = 2x1 + 2x2 + 2x3
POL( U11_gggaa(x1, ..., x5) ) = max{0, 2x1 + x2 + 2x4 - 2}
POL( U12_gggaa(x1, ..., x5) ) = max{0, x1 + x2 + x3 - 2}
POL( PP_IN_GAAGAAA(x1, x2) ) = x1 + x2
POL( PQ_IN_GAAGAA(x1, x2) ) = x1
POL( MERGESORTE_IN_GAA(x1) ) = x1
POL( PF_IN_GGGAAAAAAA(x1, ..., x3) ) = 2x3 + 2
splitC_in_gaaa([]) → splitC_out_gaaa([], [], [])
splitC_in_gaaa(.(T80, T81)) → U2_gaaa(T80, T81, splitC_in_gaaa(T81))
U2_gaaa(T80, T81, splitC_out_gaaa(T81, X123, X122)) → splitC_out_gaaa(.(T80, T81), .(T80, X122), X123)
U3_ggaaa(T60, T61, splitC_out_gaaa(T61, X92, X91)) → splitD_out_ggaaa(T60, T61, .(T60, X91), X92)
U19_GGGAAAAAAA(T124, T125, T126, splitD_out_ggaaa(T124, .(T125, T126), T131, T132)) → PP_IN_GAAGAAA(T131, T132)
PP_IN_GAAGAAA(T131, T132) → U21_GAAGAAA(T131, T132, mergesortE_in_gaa(T131))
U21_GAAGAAA(T131, T132, mergesortE_out_gaa(T131, T137)) → PQ_IN_GAAGAA(T132, T137)
PQ_IN_GAAGAA(T132, T137) → MERGESORTE_IN_GAA(T132)
PP_IN_GAAGAAA(T131, T132) → MERGESORTE_IN_GAA(T131)
PF_IN_GGGAAAAAAA(T124, T125, T126) → U19_GGGAAAAAAA(T124, T125, T126, U3_ggaaa(T124, .(T125, T126), U2_gaaa(T125, T126, splitC_in_gaaa(T126))))
splitD_in_ggaaa(T60, T61) → U3_ggaaa(T60, T61, splitC_in_gaaa(T61))
mergesortE_in_gaa([]) → mergesortE_out_gaa([], [])
mergesortE_in_gaa(.(T112, [])) → mergesortE_out_gaa(.(T112, []), .(T112, []))
mergesortE_in_gaa(.(T124, .(T125, T126))) → U4_gaa(T124, T125, T126, pF_in_gggaaaaaaa(T124, T125, T126))
U3_ggaaa(T60, T61, splitC_out_gaaa(T61, X92, X91)) → splitD_out_ggaaa(T60, T61, .(T60, X91), X92)
U4_gaa(T124, T125, T126, pF_out_gggaaaaaaa(T124, T125, T126, X173, X174, X175, X176, X177)) → mergesortE_out_gaa(.(T124, .(T125, T126)), X177)
splitC_in_gaaa([]) → splitC_out_gaaa([], [], [])
splitC_in_gaaa(.(T80, T81)) → U2_gaaa(T80, T81, splitC_in_gaaa(T81))
pF_in_gggaaaaaaa(T124, T125, T126) → U19_gggaaaaaaa(T124, T125, T126, splitD_in_ggaaa(T124, .(T125, T126)))
U2_gaaa(T80, T81, splitC_out_gaaa(T81, X123, X122)) → splitC_out_gaaa(.(T80, T81), .(T80, X122), X123)
U19_gggaaaaaaa(T124, T125, T126, splitD_out_ggaaa(T124, .(T125, T126), T131, T132)) → U20_gggaaaaaaa(T124, T125, T126, T131, T132, pP_in_gaagaaa(T131, T132))
U20_gggaaaaaaa(T124, T125, T126, T131, T132, pP_out_gaagaaa(T131, X175, T132, X176, X177)) → pF_out_gggaaaaaaa(T124, T125, T126, T131, T132, X175, X176, X177)
pP_in_gaagaaa(T131, T132) → U21_gaagaaa(T131, T132, mergesortE_in_gaa(T131))
U21_gaagaaa(T131, T132, mergesortE_out_gaa(T131, T137)) → U22_gaagaaa(T131, T137, T132, pQ_in_gaagaa(T132, T137))
U22_gaagaaa(T131, T137, T132, pQ_out_gaagaa(T132, X176, T137, X177)) → pP_out_gaagaaa(T131, T137, T132, X176, X177)
pQ_in_gaagaa(T132, T137) → U23_gaagaa(T132, T137, mergesortE_in_gaa(T132))
U23_gaagaa(T132, T137, mergesortE_out_gaa(T132, T144)) → U24_gaagaa(T132, T144, T137, mergeG_in_ggaaa(T137, T144))
U24_gaagaa(T132, T144, T137, mergeG_out_ggaaa(T137, T144, X177)) → pQ_out_gaagaa(T132, T144, T137, X177)
mergeG_in_ggaaa([], T173) → mergeG_out_ggaaa([], T173, T173)
mergeG_in_ggaaa(T188, []) → mergeG_out_ggaaa(T188, [], T188)
mergeG_in_ggaaa(.(T219, T220), .(T221, T222)) → U5_ggaaa(T219, T220, T221, T222, pH_in_ggggaa(T219, T221, T220, T222))
mergeG_in_ggaaa(.(T437, T438), .(T439, T440)) → U6_ggaaa(T437, T438, T439, T440, pI_in_ggggaa(T437, T439, T438, T440))
U5_ggaaa(T219, T220, T221, T222, pH_out_ggggaa(T219, T221, T220, T222, T226)) → mergeG_out_ggaaa(.(T219, T220), .(T221, T222), .(T219, T226))
U6_ggaaa(T437, T438, T439, T440, pI_out_ggggaa(T437, T439, T438, T440, T444)) → mergeG_out_ggaaa(.(T437, T438), .(T439, T440), .(T439, T444))
pH_in_ggggaa(T219, T221, T220, T222) → U25_ggggaa(T219, T221, T220, T222, leJ_in_gg(T219, T221))
pI_in_ggggaa(T319, T321, T320, T322) → U27_ggggaa(T319, T321, T320, T322, gtK_in_gg(T319, T321))
U25_ggggaa(T219, T221, T220, T222, leJ_out_gg(T219, T221)) → U26_ggggaa(T219, T221, T220, T222, mergeL_in_gggaa(T220, T221, T222))
U27_ggggaa(T319, T321, T320, T322, gtK_out_gg(T319, T321)) → U28_ggggaa(T319, T321, T320, T322, mergeM_in_gggaa(T319, T320, T322))
leJ_in_gg(s(T240), s(T241)) → U7_gg(T240, T241, leJ_in_gg(T240, T241))
leJ_in_gg(0, s(0)) → leJ_out_gg(0, s(0))
leJ_in_gg(0, 0) → leJ_out_gg(0, 0)
U26_ggggaa(T219, T221, T220, T222, mergeL_out_gggaa(T220, T221, T222, T226)) → pH_out_ggggaa(T219, T221, T220, T222, T226)
gtK_in_gg(s(T340), s(T341)) → U8_gg(T340, T341, gtK_in_gg(T340, T341))
gtK_in_gg(s(0), 0) → gtK_out_gg(s(0), 0)
U28_ggggaa(T319, T321, T320, T322, mergeM_out_gggaa(T319, T320, T322, T326)) → pI_out_ggggaa(T319, T321, T320, T322, T326)
U7_gg(T240, T241, leJ_out_gg(T240, T241)) → leJ_out_gg(s(T240), s(T241))
mergeL_in_gggaa([], T262, T263) → mergeL_out_gggaa([], T262, T263, .(T262, T263))
mergeL_in_gggaa(.(T294, T295), T296, T297) → U9_gggaa(T294, T295, T296, T297, pH_in_ggggaa(T294, T296, T295, T297))
mergeL_in_gggaa(.(T319, T320), T321, T322) → U10_gggaa(T319, T320, T321, T322, pI_in_ggggaa(T319, T321, T320, T322))
U8_gg(T340, T341, gtK_out_gg(T340, T341)) → gtK_out_gg(s(T340), s(T341))
mergeM_in_gggaa(T356, T357, []) → mergeM_out_gggaa(T356, T357, [], .(T356, T357))
mergeM_in_gggaa(T387, T388, .(T389, T390)) → U11_gggaa(T387, T388, T389, T390, pH_in_ggggaa(T387, T389, T388, T390))
mergeM_in_gggaa(T412, T413, .(T414, T415)) → U12_gggaa(T412, T413, T414, T415, pI_in_ggggaa(T412, T414, T413, T415))
U9_gggaa(T294, T295, T296, T297, pH_out_ggggaa(T294, T296, T295, T297, T301)) → mergeL_out_gggaa(.(T294, T295), T296, T297, .(T294, T301))
U10_gggaa(T319, T320, T321, T322, pI_out_ggggaa(T319, T321, T320, T322, T326)) → mergeL_out_gggaa(.(T319, T320), T321, T322, .(T321, T326))
U11_gggaa(T387, T388, T389, T390, pH_out_ggggaa(T387, T389, T388, T390, T394)) → mergeM_out_gggaa(T387, T388, .(T389, T390), .(T387, T394))
U12_gggaa(T412, T413, T414, T415, pI_out_ggggaa(T412, T414, T413, T415, T419)) → mergeM_out_gggaa(T412, T413, .(T414, T415), .(T414, T419))
splitD_in_ggaaa(x0, x1)
mergesortE_in_gaa(x0)
U3_ggaaa(x0, x1, x2)
U4_gaa(x0, x1, x2, x3)
splitC_in_gaaa(x0)
pF_in_gggaaaaaaa(x0, x1, x2)
U2_gaaa(x0, x1, x2)
U19_gggaaaaaaa(x0, x1, x2, x3)
U20_gggaaaaaaa(x0, x1, x2, x3, x4, x5)
pP_in_gaagaaa(x0, x1)
U21_gaagaaa(x0, x1, x2)
U22_gaagaaa(x0, x1, x2, x3)
pQ_in_gaagaa(x0, x1)
U23_gaagaa(x0, x1, x2)
U24_gaagaa(x0, x1, x2, x3)
mergeG_in_ggaaa(x0, x1)
U5_ggaaa(x0, x1, x2, x3, x4)
U6_ggaaa(x0, x1, x2, x3, x4)
pH_in_ggggaa(x0, x1, x2, x3)
pI_in_ggggaa(x0, x1, x2, x3)
U25_ggggaa(x0, x1, x2, x3, x4)
U27_ggggaa(x0, x1, x2, x3, x4)
leJ_in_gg(x0, x1)
U26_ggggaa(x0, x1, x2, x3, x4)
gtK_in_gg(x0, x1)
U28_ggggaa(x0, x1, x2, x3, x4)
U7_gg(x0, x1, x2)
mergeL_in_gggaa(x0, x1, x2)
U8_gg(x0, x1, x2)
mergeM_in_gggaa(x0, x1, x2)
U9_gggaa(x0, x1, x2, x3, x4)
U10_gggaa(x0, x1, x2, x3, x4)
U11_gggaa(x0, x1, x2, x3, x4)
U12_gggaa(x0, x1, x2, x3, x4)
MERGESORTA_IN_GAA(.(T39, .(T40, T41)), T45, .(T46, T44)) → PB_IN_GGAAAGAAAA(T40, T41, X63, X62, T44, T39, X35, X36, T45, T46)
PB_IN_GGAAAGAAAA(T40, T41, T47, T48, T49, T39, X35, X36, T50, T51) → U13_GGAAAGAAAA(T40, T41, T47, T48, T49, T39, X35, X36, T50, T51, splitD_in_ggaaa(T40, T41, T47, T48, T49))
U13_GGAAAGAAAA(T40, T41, T47, T48, T49, T39, X35, X36, T50, T51, splitD_out_ggaaa(T40, T41, T47, T48, T49)) → PN_IN_GGAAGAAA(T39, T48, X35, T49, T47, X36, T50, T51)
PN_IN_GGAAGAAA(T39, T48, T87, T88, T47, X36, T89, T90) → MERGESORTA_IN_GAA(.(T39, T48), T87, T88)
mergesortA_in_gaa([], [], T5) → mergesortA_out_gaa([], [], T5)
mergesortA_in_gaa(.(T8, []), .(T8, []), T9) → mergesortA_out_gaa(.(T8, []), .(T8, []), T9)
mergesortA_in_gaa(.(T39, .(T40, T41)), T45, .(T46, T44)) → U1_gaa(T39, T40, T41, T45, T46, T44, pB_in_ggaaagaaaa(T40, T41, X63, X62, T44, T39, X35, X36, T45, T46))
pB_in_ggaaagaaaa(T40, T41, T47, T48, T49, T39, X35, X36, T50, T51) → U13_ggaaagaaaa(T40, T41, T47, T48, T49, T39, X35, X36, T50, T51, splitD_in_ggaaa(T40, T41, T47, T48, T49))
splitD_in_ggaaa(T60, T61, .(T60, X91), X92, .(T62, T64)) → U3_ggaaa(T60, T61, X91, X92, T62, T64, splitC_in_gaaa(T61, X92, X91, T64))
splitC_in_gaaa([], [], [], T71) → splitC_out_gaaa([], [], [], T71)
splitC_in_gaaa(.(T80, T81), .(T80, X122), X123, .(T82, T84)) → U2_gaaa(T80, T81, X122, X123, T82, T84, splitC_in_gaaa(T81, X123, X122, T84))
U2_gaaa(T80, T81, X122, X123, T82, T84, splitC_out_gaaa(T81, X123, X122, T84)) → splitC_out_gaaa(.(T80, T81), .(T80, X122), X123, .(T82, T84))
U3_ggaaa(T60, T61, X91, X92, T62, T64, splitC_out_gaaa(T61, X92, X91, T64)) → splitD_out_ggaaa(T60, T61, .(T60, X91), X92, .(T62, T64))
U13_ggaaagaaaa(T40, T41, T47, T48, T49, T39, X35, X36, T50, T51, splitD_out_ggaaa(T40, T41, T47, T48, T49)) → U14_ggaaagaaaa(T40, T41, T47, T48, T49, T39, X35, X36, T50, T51, pN_in_ggaagaaa(T39, T48, X35, T49, T47, X36, T50, T51))
pN_in_ggaagaaa(T39, T48, T87, T88, T47, X36, T89, T90) → U15_ggaagaaa(T39, T48, T87, T88, T47, X36, T89, T90, mergesortA_in_gaa(.(T39, T48), T87, T88))
U15_ggaagaaa(T39, T48, T87, T88, T47, X36, T89, T90, mergesortA_out_gaa(.(T39, T48), T87, T88)) → U16_ggaagaaa(T39, T48, T87, T88, T47, X36, T89, T90, pO_in_gaagaa(T47, X36, T88, T87, T89, T90))
pO_in_gaagaa(T47, T93, T96, T87, T94, T95) → U17_gaagaa(T47, T93, T96, T87, T94, T95, mergesortE_in_gaa(T47, T93, T96))
mergesortE_in_gaa([], [], T103) → mergesortE_out_gaa([], [], T103)
mergesortE_in_gaa(.(T112, []), .(T112, []), T113) → mergesortE_out_gaa(.(T112, []), .(T112, []), T113)
mergesortE_in_gaa(.(T124, .(T125, T126)), X177, .(T129, T130)) → U4_gaa(T124, T125, T126, X177, T129, T130, pF_in_gggaaaaaaa(T124, T125, T126, X173, X174, T129, T130, X175, X176, X177))
pF_in_gggaaaaaaa(T124, T125, T126, T131, T132, T134, T133, X175, X176, X177) → U19_gggaaaaaaa(T124, T125, T126, T131, T132, T134, T133, X175, X176, X177, splitD_in_ggaaa(T124, .(T125, T126), T131, T132, .(T134, T133)))
U19_gggaaaaaaa(T124, T125, T126, T131, T132, T134, T133, X175, X176, X177, splitD_out_ggaaa(T124, .(T125, T126), T131, T132, .(T134, T133))) → U20_gggaaaaaaa(T124, T125, T126, T131, T132, T134, T133, X175, X176, X177, pP_in_gaagaaa(T131, X175, T133, T132, X176, X177, T134))
pP_in_gaagaaa(T131, T137, T138, T132, X176, X177, T139) → U21_gaagaaa(T131, T137, T138, T132, X176, X177, T139, mergesortE_in_gaa(T131, T137, T138))
U21_gaagaaa(T131, T137, T138, T132, X176, X177, T139, mergesortE_out_gaa(T131, T137, T138)) → U22_gaagaaa(T131, T137, T138, T132, X176, X177, T139, pQ_in_gaagaa(T132, X176, T138, T137, X177, T139))
pQ_in_gaagaa(T132, T144, T146, T137, X177, T145) → U23_gaagaa(T132, T144, T146, T137, X177, T145, mergesortE_in_gaa(T132, T144, T146))
U23_gaagaa(T132, T144, T146, T137, X177, T145, mergesortE_out_gaa(T132, T144, T146)) → U24_gaagaa(T132, T144, T146, T137, X177, T145, mergeG_in_ggaaa(T137, T144, X177, T145, T146))
mergeG_in_ggaaa([], T173, T173, T174, T175) → mergeG_out_ggaaa([], T173, T173, T174, T175)
mergeG_in_ggaaa(T188, [], T188, T189, T190) → mergeG_out_ggaaa(T188, [], T188, T189, T190)
mergeG_in_ggaaa(.(T219, T220), .(T221, T222), .(T219, T226), T224, T227) → U5_ggaaa(T219, T220, T221, T222, T226, T224, T227, pH_in_ggggaa(T219, T221, T220, T222, T226, T227))
pH_in_ggggaa(T219, T221, T220, T222, T226, T227) → U25_ggggaa(T219, T221, T220, T222, T226, T227, leJ_in_gg(T219, T221))
leJ_in_gg(s(T240), s(T241)) → U7_gg(T240, T241, leJ_in_gg(T240, T241))
leJ_in_gg(0, s(0)) → leJ_out_gg(0, s(0))
leJ_in_gg(0, 0) → leJ_out_gg(0, 0)
U7_gg(T240, T241, leJ_out_gg(T240, T241)) → leJ_out_gg(s(T240), s(T241))
U25_ggggaa(T219, T221, T220, T222, T226, T227, leJ_out_gg(T219, T221)) → U26_ggggaa(T219, T221, T220, T222, T226, T227, mergeL_in_gggaa(T220, T221, T222, T226, T227))
mergeL_in_gggaa([], T262, T263, .(T262, T263), T264) → mergeL_out_gggaa([], T262, T263, .(T262, T263), T264)
mergeL_in_gggaa(.(T294, T295), T296, T297, .(T294, T301), .(T299, T302)) → U9_gggaa(T294, T295, T296, T297, T301, T299, T302, pH_in_ggggaa(T294, T296, T295, T297, T301, T302))
U9_gggaa(T294, T295, T296, T297, T301, T299, T302, pH_out_ggggaa(T294, T296, T295, T297, T301, T302)) → mergeL_out_gggaa(.(T294, T295), T296, T297, .(T294, T301), .(T299, T302))
mergeL_in_gggaa(.(T319, T320), T321, T322, .(T321, T326), .(T324, T327)) → U10_gggaa(T319, T320, T321, T322, T326, T324, T327, pI_in_ggggaa(T319, T321, T320, T322, T326, T327))
pI_in_ggggaa(T319, T321, T320, T322, T326, T327) → U27_ggggaa(T319, T321, T320, T322, T326, T327, gtK_in_gg(T319, T321))
gtK_in_gg(s(T340), s(T341)) → U8_gg(T340, T341, gtK_in_gg(T340, T341))
gtK_in_gg(s(0), 0) → gtK_out_gg(s(0), 0)
U8_gg(T340, T341, gtK_out_gg(T340, T341)) → gtK_out_gg(s(T340), s(T341))
U27_ggggaa(T319, T321, T320, T322, T326, T327, gtK_out_gg(T319, T321)) → U28_ggggaa(T319, T321, T320, T322, T326, T327, mergeM_in_gggaa(T319, T320, T322, T326, T327))
mergeM_in_gggaa(T356, T357, [], .(T356, T357), T358) → mergeM_out_gggaa(T356, T357, [], .(T356, T357), T358)
mergeM_in_gggaa(T387, T388, .(T389, T390), .(T387, T394), .(T392, T395)) → U11_gggaa(T387, T388, T389, T390, T394, T392, T395, pH_in_ggggaa(T387, T389, T388, T390, T394, T395))
U11_gggaa(T387, T388, T389, T390, T394, T392, T395, pH_out_ggggaa(T387, T389, T388, T390, T394, T395)) → mergeM_out_gggaa(T387, T388, .(T389, T390), .(T387, T394), .(T392, T395))
mergeM_in_gggaa(T412, T413, .(T414, T415), .(T414, T419), .(T417, T420)) → U12_gggaa(T412, T413, T414, T415, T419, T417, T420, pI_in_ggggaa(T412, T414, T413, T415, T419, T420))
U12_gggaa(T412, T413, T414, T415, T419, T417, T420, pI_out_ggggaa(T412, T414, T413, T415, T419, T420)) → mergeM_out_gggaa(T412, T413, .(T414, T415), .(T414, T419), .(T417, T420))
U28_ggggaa(T319, T321, T320, T322, T326, T327, mergeM_out_gggaa(T319, T320, T322, T326, T327)) → pI_out_ggggaa(T319, T321, T320, T322, T326, T327)
U10_gggaa(T319, T320, T321, T322, T326, T324, T327, pI_out_ggggaa(T319, T321, T320, T322, T326, T327)) → mergeL_out_gggaa(.(T319, T320), T321, T322, .(T321, T326), .(T324, T327))
U26_ggggaa(T219, T221, T220, T222, T226, T227, mergeL_out_gggaa(T220, T221, T222, T226, T227)) → pH_out_ggggaa(T219, T221, T220, T222, T226, T227)
U5_ggaaa(T219, T220, T221, T222, T226, T224, T227, pH_out_ggggaa(T219, T221, T220, T222, T226, T227)) → mergeG_out_ggaaa(.(T219, T220), .(T221, T222), .(T219, T226), T224, T227)
mergeG_in_ggaaa(.(T437, T438), .(T439, T440), .(T439, T444), T442, T445) → U6_ggaaa(T437, T438, T439, T440, T444, T442, T445, pI_in_ggggaa(T437, T439, T438, T440, T444, T445))
U6_ggaaa(T437, T438, T439, T440, T444, T442, T445, pI_out_ggggaa(T437, T439, T438, T440, T444, T445)) → mergeG_out_ggaaa(.(T437, T438), .(T439, T440), .(T439, T444), T442, T445)
U24_gaagaa(T132, T144, T146, T137, X177, T145, mergeG_out_ggaaa(T137, T144, X177, T145, T146)) → pQ_out_gaagaa(T132, T144, T146, T137, X177, T145)
U22_gaagaaa(T131, T137, T138, T132, X176, X177, T139, pQ_out_gaagaa(T132, X176, T138, T137, X177, T139)) → pP_out_gaagaaa(T131, T137, T138, T132, X176, X177, T139)
U20_gggaaaaaaa(T124, T125, T126, T131, T132, T134, T133, X175, X176, X177, pP_out_gaagaaa(T131, X175, T133, T132, X176, X177, T134)) → pF_out_gggaaaaaaa(T124, T125, T126, T131, T132, T134, T133, X175, X176, X177)
U4_gaa(T124, T125, T126, X177, T129, T130, pF_out_gggaaaaaaa(T124, T125, T126, X173, X174, T129, T130, X175, X176, X177)) → mergesortE_out_gaa(.(T124, .(T125, T126)), X177, .(T129, T130))
U17_gaagaa(T47, T93, T96, T87, T94, T95, mergesortE_out_gaa(T47, T93, T96)) → U18_gaagaa(T47, T93, T96, T87, T94, T95, mergeG_in_ggaaa(T87, T93, T94, T95, T96))
U18_gaagaa(T47, T93, T96, T87, T94, T95, mergeG_out_ggaaa(T87, T93, T94, T95, T96)) → pO_out_gaagaa(T47, T93, T96, T87, T94, T95)
U16_ggaagaaa(T39, T48, T87, T88, T47, X36, T89, T90, pO_out_gaagaa(T47, X36, T88, T87, T89, T90)) → pN_out_ggaagaaa(T39, T48, T87, T88, T47, X36, T89, T90)
U14_ggaaagaaaa(T40, T41, T47, T48, T49, T39, X35, X36, T50, T51, pN_out_ggaagaaa(T39, T48, X35, T49, T47, X36, T50, T51)) → pB_out_ggaaagaaaa(T40, T41, T47, T48, T49, T39, X35, X36, T50, T51)
U1_gaa(T39, T40, T41, T45, T46, T44, pB_out_ggaaagaaaa(T40, T41, X63, X62, T44, T39, X35, X36, T45, T46)) → mergesortA_out_gaa(.(T39, .(T40, T41)), T45, .(T46, T44))
MERGESORTA_IN_GAA(.(T39, .(T40, T41)), T45, .(T46, T44)) → PB_IN_GGAAAGAAAA(T40, T41, X63, X62, T44, T39, X35, X36, T45, T46)
PB_IN_GGAAAGAAAA(T40, T41, T47, T48, T49, T39, X35, X36, T50, T51) → U13_GGAAAGAAAA(T40, T41, T47, T48, T49, T39, X35, X36, T50, T51, splitD_in_ggaaa(T40, T41, T47, T48, T49))
U13_GGAAAGAAAA(T40, T41, T47, T48, T49, T39, X35, X36, T50, T51, splitD_out_ggaaa(T40, T41, T47, T48, T49)) → PN_IN_GGAAGAAA(T39, T48, X35, T49, T47, X36, T50, T51)
PN_IN_GGAAGAAA(T39, T48, T87, T88, T47, X36, T89, T90) → MERGESORTA_IN_GAA(.(T39, T48), T87, T88)
splitD_in_ggaaa(T60, T61, .(T60, X91), X92, .(T62, T64)) → U3_ggaaa(T60, T61, X91, X92, T62, T64, splitC_in_gaaa(T61, X92, X91, T64))
U3_ggaaa(T60, T61, X91, X92, T62, T64, splitC_out_gaaa(T61, X92, X91, T64)) → splitD_out_ggaaa(T60, T61, .(T60, X91), X92, .(T62, T64))
splitC_in_gaaa([], [], [], T71) → splitC_out_gaaa([], [], [], T71)
splitC_in_gaaa(.(T80, T81), .(T80, X122), X123, .(T82, T84)) → U2_gaaa(T80, T81, X122, X123, T82, T84, splitC_in_gaaa(T81, X123, X122, T84))
U2_gaaa(T80, T81, X122, X123, T82, T84, splitC_out_gaaa(T81, X123, X122, T84)) → splitC_out_gaaa(.(T80, T81), .(T80, X122), X123, .(T82, T84))
MERGESORTA_IN_GAA(.(T39, .(T40, T41))) → PB_IN_GGAAAGAAAA(T40, T41, T39)
PB_IN_GGAAAGAAAA(T40, T41, T39) → U13_GGAAAGAAAA(T40, T41, T39, splitD_in_ggaaa(T40, T41))
U13_GGAAAGAAAA(T40, T41, T39, splitD_out_ggaaa(T40, T41, T47, T48)) → PN_IN_GGAAGAAA(T39, T48, T47)
PN_IN_GGAAGAAA(T39, T48, T47) → MERGESORTA_IN_GAA(.(T39, T48))
splitD_in_ggaaa(T60, T61) → U3_ggaaa(T60, T61, splitC_in_gaaa(T61))
U3_ggaaa(T60, T61, splitC_out_gaaa(T61, X92, X91)) → splitD_out_ggaaa(T60, T61, .(T60, X91), X92)
splitC_in_gaaa([]) → splitC_out_gaaa([], [], [])
splitC_in_gaaa(.(T80, T81)) → U2_gaaa(T80, T81, splitC_in_gaaa(T81))
U2_gaaa(T80, T81, splitC_out_gaaa(T81, X123, X122)) → splitC_out_gaaa(.(T80, T81), .(T80, X122), X123)
splitD_in_ggaaa(x0, x1)
U3_ggaaa(x0, x1, x2)
splitC_in_gaaa(x0)
U2_gaaa(x0, x1, x2)
PB_IN_GGAAAGAAAA(T40, T41, T39) → U13_GGAAAGAAAA(T40, T41, T39, U3_ggaaa(T40, T41, splitC_in_gaaa(T41)))
MERGESORTA_IN_GAA(.(T39, .(T40, T41))) → PB_IN_GGAAAGAAAA(T40, T41, T39)
U13_GGAAAGAAAA(T40, T41, T39, splitD_out_ggaaa(T40, T41, T47, T48)) → PN_IN_GGAAGAAA(T39, T48, T47)
PN_IN_GGAAGAAA(T39, T48, T47) → MERGESORTA_IN_GAA(.(T39, T48))
PB_IN_GGAAAGAAAA(T40, T41, T39) → U13_GGAAAGAAAA(T40, T41, T39, U3_ggaaa(T40, T41, splitC_in_gaaa(T41)))
splitD_in_ggaaa(T60, T61) → U3_ggaaa(T60, T61, splitC_in_gaaa(T61))
U3_ggaaa(T60, T61, splitC_out_gaaa(T61, X92, X91)) → splitD_out_ggaaa(T60, T61, .(T60, X91), X92)
splitC_in_gaaa([]) → splitC_out_gaaa([], [], [])
splitC_in_gaaa(.(T80, T81)) → U2_gaaa(T80, T81, splitC_in_gaaa(T81))
U2_gaaa(T80, T81, splitC_out_gaaa(T81, X123, X122)) → splitC_out_gaaa(.(T80, T81), .(T80, X122), X123)
splitD_in_ggaaa(x0, x1)
U3_ggaaa(x0, x1, x2)
splitC_in_gaaa(x0)
U2_gaaa(x0, x1, x2)
MERGESORTA_IN_GAA(.(T39, .(T40, T41))) → PB_IN_GGAAAGAAAA(T40, T41, T39)
U13_GGAAAGAAAA(T40, T41, T39, splitD_out_ggaaa(T40, T41, T47, T48)) → PN_IN_GGAAGAAA(T39, T48, T47)
PN_IN_GGAAGAAA(T39, T48, T47) → MERGESORTA_IN_GAA(.(T39, T48))
PB_IN_GGAAAGAAAA(T40, T41, T39) → U13_GGAAAGAAAA(T40, T41, T39, U3_ggaaa(T40, T41, splitC_in_gaaa(T41)))
splitC_in_gaaa([]) → splitC_out_gaaa([], [], [])
splitC_in_gaaa(.(T80, T81)) → U2_gaaa(T80, T81, splitC_in_gaaa(T81))
U3_ggaaa(T60, T61, splitC_out_gaaa(T61, X92, X91)) → splitD_out_ggaaa(T60, T61, .(T60, X91), X92)
U2_gaaa(T80, T81, splitC_out_gaaa(T81, X123, X122)) → splitC_out_gaaa(.(T80, T81), .(T80, X122), X123)
splitD_in_ggaaa(x0, x1)
U3_ggaaa(x0, x1, x2)
splitC_in_gaaa(x0)
U2_gaaa(x0, x1, x2)
splitD_in_ggaaa(x0, x1)
MERGESORTA_IN_GAA(.(T39, .(T40, T41))) → PB_IN_GGAAAGAAAA(T40, T41, T39)
U13_GGAAAGAAAA(T40, T41, T39, splitD_out_ggaaa(T40, T41, T47, T48)) → PN_IN_GGAAGAAA(T39, T48, T47)
PN_IN_GGAAGAAA(T39, T48, T47) → MERGESORTA_IN_GAA(.(T39, T48))
PB_IN_GGAAAGAAAA(T40, T41, T39) → U13_GGAAAGAAAA(T40, T41, T39, U3_ggaaa(T40, T41, splitC_in_gaaa(T41)))
splitC_in_gaaa([]) → splitC_out_gaaa([], [], [])
splitC_in_gaaa(.(T80, T81)) → U2_gaaa(T80, T81, splitC_in_gaaa(T81))
U3_ggaaa(T60, T61, splitC_out_gaaa(T61, X92, X91)) → splitD_out_ggaaa(T60, T61, .(T60, X91), X92)
U2_gaaa(T80, T81, splitC_out_gaaa(T81, X123, X122)) → splitC_out_gaaa(.(T80, T81), .(T80, X122), X123)
U3_ggaaa(x0, x1, x2)
splitC_in_gaaa(x0)
U2_gaaa(x0, x1, x2)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
MERGESORTA_IN_GAA(.(T39, .(T40, T41))) → PB_IN_GGAAAGAAAA(T40, T41, T39)
POL(.(x1, x2)) = 1 + x2
POL(MERGESORTA_IN_GAA(x1)) = x1
POL(PB_IN_GGAAAGAAAA(x1, x2, x3)) = 1 + x2
POL(PN_IN_GGAAGAAA(x1, x2, x3)) = 1 + x2
POL(U13_GGAAAGAAAA(x1, x2, x3, x4)) = x4
POL(U2_gaaa(x1, x2, x3)) = 1 + x3
POL(U3_ggaaa(x1, x2, x3)) = x3
POL([]) = 0
POL(splitC_in_gaaa(x1)) = 1 + x1
POL(splitC_out_gaaa(x1, x2, x3)) = 1 + x2 + x3
POL(splitD_out_ggaaa(x1, x2, x3, x4)) = 1 + x4
splitC_in_gaaa([]) → splitC_out_gaaa([], [], [])
splitC_in_gaaa(.(T80, T81)) → U2_gaaa(T80, T81, splitC_in_gaaa(T81))
U3_ggaaa(T60, T61, splitC_out_gaaa(T61, X92, X91)) → splitD_out_ggaaa(T60, T61, .(T60, X91), X92)
U2_gaaa(T80, T81, splitC_out_gaaa(T81, X123, X122)) → splitC_out_gaaa(.(T80, T81), .(T80, X122), X123)
U13_GGAAAGAAAA(T40, T41, T39, splitD_out_ggaaa(T40, T41, T47, T48)) → PN_IN_GGAAGAAA(T39, T48, T47)
PN_IN_GGAAGAAA(T39, T48, T47) → MERGESORTA_IN_GAA(.(T39, T48))
PB_IN_GGAAAGAAAA(T40, T41, T39) → U13_GGAAAGAAAA(T40, T41, T39, U3_ggaaa(T40, T41, splitC_in_gaaa(T41)))
splitC_in_gaaa([]) → splitC_out_gaaa([], [], [])
splitC_in_gaaa(.(T80, T81)) → U2_gaaa(T80, T81, splitC_in_gaaa(T81))
U3_ggaaa(T60, T61, splitC_out_gaaa(T61, X92, X91)) → splitD_out_ggaaa(T60, T61, .(T60, X91), X92)
U2_gaaa(T80, T81, splitC_out_gaaa(T81, X123, X122)) → splitC_out_gaaa(.(T80, T81), .(T80, X122), X123)
U3_ggaaa(x0, x1, x2)
splitC_in_gaaa(x0)
U2_gaaa(x0, x1, x2)