0 Prolog
↳1 PrologToDTProblemTransformerProof (⇒, 280 ms)
↳2 TRIPLES
↳3 UndefinedPredicateInTriplesTransformerProof (⇒, 0 ms)
↳4 TRIPLES
↳5 TriplesToPiDPProof (⇒, 470 ms)
↳6 PiDP
↳7 DependencyGraphProof (⇔, 17 ms)
↳8 AND
↳9 PiDP
↳10 UsableRulesProof (⇔, 0 ms)
↳11 PiDP
↳12 PiDPToQDPProof (⇒, 33 ms)
↳13 QDP
↳14 QDPSizeChangeProof (⇔, 0 ms)
↳15 YES
↳16 PiDP
↳17 UsableRulesProof (⇔, 0 ms)
↳18 PiDP
↳19 PiDPToQDPProof (⇔, 0 ms)
↳20 QDP
↳21 QDPSizeChangeProof (⇔, 0 ms)
↳22 YES
↳23 PiDP
↳24 UsableRulesProof (⇔, 0 ms)
↳25 PiDP
↳26 PiDPToQDPProof (⇔, 0 ms)
↳27 QDP
↳28 QDPSizeChangeProof (⇔, 0 ms)
↳29 YES
↳30 PiDP
↳31 UsableRulesProof (⇔, 0 ms)
↳32 PiDP
↳33 PiDPToQDPProof (⇒, 0 ms)
↳34 QDP
↳35 QDPSizeChangeProof (⇔, 0 ms)
↳36 YES
↳37 PiDP
↳38 UsableRulesProof (⇔, 0 ms)
↳39 PiDP
↳40 PiDPToQDPProof (⇒, 0 ms)
↳41 QDP
↳42 QDPOrderProof (⇔, 206 ms)
↳43 QDP
↳44 DependencyGraphProof (⇔, 0 ms)
↳45 TRUE
↳46 PiDP
↳47 UsableRulesProof (⇔, 0 ms)
↳48 PiDP
↳49 PiDPToQDPProof (⇒, 0 ms)
↳50 QDP
↳51 QDPSizeChangeProof (⇔, 0 ms)
↳52 YES
↳53 PiDP
↳54 UsableRulesProof (⇔, 0 ms)
↳55 PiDP
↳56 PiDPToQDPProof (⇒, 0 ms)
↳57 QDP
↳58 QDPOrderProof (⇔, 179 ms)
↳59 QDP
↳60 DependencyGraphProof (⇔, 0 ms)
↳61 TRUE
QSF_IN_GA(cons(X1, []), X2) → U21_GA(X1, X2, qscA_in_a(X3))
U21_GA(X1, X2, qscA_out_a(X3)) → U22_GA(X1, X2, X3, qscA_in_a(X4))
U22_GA(X1, X2, X3, qscA_out_a(X4)) → U23_GA(X1, X2, appendB_in_ggga(X3, X1, X4, X2))
U22_GA(X1, X2, X3, qscA_out_a(X4)) → APPENDB_IN_GGGA(X3, X1, X4, X2)
APPENDB_IN_GGGA(cons(X1, X2), X3, X4, cons(X1, X5)) → U1_GGGA(X1, X2, X3, X4, X5, appendB_in_ggga(X2, X3, X4, X5))
APPENDB_IN_GGGA(cons(X1, X2), X3, X4, cons(X1, X5)) → APPENDB_IN_GGGA(X2, X3, X4, X5)
QSF_IN_GA(cons(X1, cons(X2, X3)), X4) → U24_GA(X1, X2, X3, X4, lessC_in_gg(X2, X1))
QSF_IN_GA(cons(X1, cons(X2, X3)), X4) → LESSC_IN_GG(X2, X1)
LESSC_IN_GG(s(X1), s(X2)) → U2_GG(X1, X2, lessC_in_gg(X1, X2))
LESSC_IN_GG(s(X1), s(X2)) → LESSC_IN_GG(X1, X2)
QSF_IN_GA(cons(X1, cons(X2, X3)), X4) → U25_GA(X1, X2, X3, X4, lesscC_in_gg(X2, X1))
U25_GA(X1, X2, X3, X4, lesscC_out_gg(X2, X1)) → U26_GA(X1, X2, X3, X4, splitD_in_ggaa(X3, X1, X5, X6))
U25_GA(X1, X2, X3, X4, lesscC_out_gg(X2, X1)) → SPLITD_IN_GGAA(X3, X1, X5, X6)
SPLITD_IN_GGAA(cons(X1, X2), X3, cons(X1, X4), X5) → U3_GGAA(X1, X2, X3, X4, X5, lessC_in_gg(X1, X3))
SPLITD_IN_GGAA(cons(X1, X2), X3, cons(X1, X4), X5) → LESSC_IN_GG(X1, X3)
SPLITD_IN_GGAA(cons(X1, X2), X3, cons(X1, X4), X5) → U4_GGAA(X1, X2, X3, X4, X5, lesscC_in_gg(X1, X3))
U4_GGAA(X1, X2, X3, X4, X5, lesscC_out_gg(X1, X3)) → U5_GGAA(X1, X2, X3, X4, X5, splitD_in_ggaa(X2, X3, X4, X5))
U4_GGAA(X1, X2, X3, X4, X5, lesscC_out_gg(X1, X3)) → SPLITD_IN_GGAA(X2, X3, X4, X5)
SPLITD_IN_GGAA(cons(X1, X2), X3, X4, cons(X1, X5)) → U6_GGAA(X1, X2, X3, X4, X5, geqE_in_gg(X1, X3))
SPLITD_IN_GGAA(cons(X1, X2), X3, X4, cons(X1, X5)) → GEQE_IN_GG(X1, X3)
GEQE_IN_GG(s(X1), s(X2)) → U9_GG(X1, X2, geqE_in_gg(X1, X2))
GEQE_IN_GG(s(X1), s(X2)) → GEQE_IN_GG(X1, X2)
SPLITD_IN_GGAA(cons(X1, X2), X3, X4, cons(X1, X5)) → U7_GGAA(X1, X2, X3, X4, X5, geqcE_in_gg(X1, X3))
U7_GGAA(X1, X2, X3, X4, X5, geqcE_out_gg(X1, X3)) → U8_GGAA(X1, X2, X3, X4, X5, splitD_in_ggaa(X2, X3, X4, X5))
U7_GGAA(X1, X2, X3, X4, X5, geqcE_out_gg(X1, X3)) → SPLITD_IN_GGAA(X2, X3, X4, X5)
U25_GA(X1, X2, X3, X4, lesscC_out_gg(X2, X1)) → U27_GA(X1, X2, X3, X4, splitcD_in_ggaa(X3, X1, X5, X6))
U27_GA(X1, X2, X3, X4, splitcD_out_ggaa(X3, X1, X5, X6)) → U28_GA(X1, X2, X3, X4, qsF_in_ga(cons(X2, X5), X7))
U27_GA(X1, X2, X3, X4, splitcD_out_ggaa(X3, X1, X5, X6)) → QSF_IN_GA(cons(X2, X5), X7)
QSF_IN_GA(cons(X1, cons(X2, X3)), X4) → U31_GA(X1, X2, X3, X4, geqE_in_gg(X2, X1))
QSF_IN_GA(cons(X1, cons(X2, X3)), X4) → GEQE_IN_GG(X2, X1)
QSF_IN_GA(cons(X1, cons(X2, X3)), X4) → U32_GA(X1, X2, X3, X4, geqcE_in_gg(X2, X1))
U32_GA(X1, X2, X3, X4, geqcE_out_gg(X2, X1)) → U33_GA(X1, X2, X3, X4, splitD_in_ggaa(X3, X1, X5, X6))
U32_GA(X1, X2, X3, X4, geqcE_out_gg(X2, X1)) → SPLITD_IN_GGAA(X3, X1, X5, X6)
U32_GA(X1, X2, X3, X4, geqcE_out_gg(X2, X1)) → U34_GA(X1, X2, X3, X4, splitcD_in_ggaa(X3, X1, X5, X6))
U34_GA(X1, X2, X3, X4, splitcD_out_ggaa(X3, X1, X5, X6)) → U35_GA(X1, X2, X3, X4, qsH_in_ga(X5, X7))
U34_GA(X1, X2, X3, X4, splitcD_out_ggaa(X3, X1, X5, X6)) → QSH_IN_GA(X5, X7)
QSH_IN_GA(cons(X1, X2), X3) → U10_GA(X1, X2, X3, splitD_in_ggaa(X2, X1, X4, X5))
QSH_IN_GA(cons(X1, X2), X3) → SPLITD_IN_GGAA(X2, X1, X4, X5)
QSH_IN_GA(cons(X1, X2), X3) → U11_GA(X1, X2, X3, splitcD_in_ggaa(X2, X1, X4, X5))
U11_GA(X1, X2, X3, splitcD_out_ggaa(X2, X1, X4, X5)) → U12_GA(X1, X2, X3, qsH_in_ga(X4, X6))
U11_GA(X1, X2, X3, splitcD_out_ggaa(X2, X1, X4, X5)) → QSH_IN_GA(X4, X6)
U11_GA(X1, X2, X3, splitcD_out_ggaa(X2, X1, X4, X5)) → U13_GA(X1, X2, X3, X5, qscH_in_ga(X4, X6))
U13_GA(X1, X2, X3, X5, qscH_out_ga(X4, X6)) → U14_GA(X1, X2, X3, qsH_in_ga(X5, X7))
U13_GA(X1, X2, X3, X5, qscH_out_ga(X4, X6)) → QSH_IN_GA(X5, X7)
U13_GA(X1, X2, X3, X5, qscH_out_ga(X4, X6)) → U15_GA(X1, X2, X3, X6, qscH_in_ga(X5, X7))
U15_GA(X1, X2, X3, X6, qscH_out_ga(X5, X7)) → U16_GA(X1, X2, X3, appendI_in_ggga(X6, X1, X7, X3))
U15_GA(X1, X2, X3, X6, qscH_out_ga(X5, X7)) → APPENDI_IN_GGGA(X6, X1, X7, X3)
APPENDI_IN_GGGA(cons(X1, X2), X3, X4, cons(X1, X5)) → U17_GGGA(X1, X2, X3, X4, X5, appendI_in_ggga(X2, X3, X4, X5))
APPENDI_IN_GGGA(cons(X1, X2), X3, X4, cons(X1, X5)) → APPENDI_IN_GGGA(X2, X3, X4, X5)
U34_GA(X1, X2, X3, X4, splitcD_out_ggaa(X3, X1, X5, X6)) → U36_GA(X1, X2, X3, X4, X6, qscH_in_ga(X5, X7))
U36_GA(X1, X2, X3, X4, X6, qscH_out_ga(X5, X7)) → U37_GA(X1, X2, X3, X4, pG_in_gagga(cons(X2, X6), X8, X7, X1, X4))
U36_GA(X1, X2, X3, X4, X6, qscH_out_ga(X5, X7)) → PG_IN_GAGGA(cons(X2, X6), X8, X7, X1, X4)
PG_IN_GAGGA(X1, X2, X3, X4, X5) → U18_GAGGA(X1, X2, X3, X4, X5, qsH_in_ga(X1, X2))
PG_IN_GAGGA(X1, X2, X3, X4, X5) → QSH_IN_GA(X1, X2)
PG_IN_GAGGA(X1, X2, X3, X4, X5) → U19_GAGGA(X1, X2, X3, X4, X5, qscH_in_ga(X1, X2))
U19_GAGGA(X1, X2, X3, X4, X5, qscH_out_ga(X1, X2)) → U20_GAGGA(X1, X2, X3, X4, X5, appendB_in_ggga(X3, X4, X2, X5))
U19_GAGGA(X1, X2, X3, X4, X5, qscH_out_ga(X1, X2)) → APPENDB_IN_GGGA(X3, X4, X2, X5)
U27_GA(X1, X2, X3, X4, splitcD_out_ggaa(X3, X1, X5, X6)) → U29_GA(X1, X2, X3, X4, X6, qscF_in_ga(cons(X2, X5), X7))
U29_GA(X1, X2, X3, X4, X6, qscF_out_ga(cons(X2, X5), X7)) → U30_GA(X1, X2, X3, X4, pG_in_gagga(X6, X8, X7, X1, X4))
U29_GA(X1, X2, X3, X4, X6, qscF_out_ga(cons(X2, X5), X7)) → PG_IN_GAGGA(X6, X8, X7, X1, X4)
qscA_in_a([]) → qscA_out_a([])
lesscC_in_gg(0, s(X1)) → lesscC_out_gg(0, s(X1))
lesscC_in_gg(s(X1), s(X2)) → U40_gg(X1, X2, lesscC_in_gg(X1, X2))
U40_gg(X1, X2, lesscC_out_gg(X1, X2)) → lesscC_out_gg(s(X1), s(X2))
geqcE_in_gg(X1, X1) → geqcE_out_gg(X1, X1)
geqcE_in_gg(s(X1), 0) → geqcE_out_gg(s(X1), 0)
geqcE_in_gg(s(X1), s(X2)) → U45_gg(X1, X2, geqcE_in_gg(X1, X2))
U45_gg(X1, X2, geqcE_out_gg(X1, X2)) → geqcE_out_gg(s(X1), s(X2))
splitcD_in_ggaa([], X1, [], []) → splitcD_out_ggaa([], X1, [], [])
splitcD_in_ggaa(cons(X1, X2), X3, cons(X1, X4), X5) → U41_ggaa(X1, X2, X3, X4, X5, lesscC_in_gg(X1, X3))
U41_ggaa(X1, X2, X3, X4, X5, lesscC_out_gg(X1, X3)) → U42_ggaa(X1, X2, X3, X4, X5, splitcD_in_ggaa(X2, X3, X4, X5))
splitcD_in_ggaa(cons(X1, X2), X3, X4, cons(X1, X5)) → U43_ggaa(X1, X2, X3, X4, X5, geqcE_in_gg(X1, X3))
U43_ggaa(X1, X2, X3, X4, X5, geqcE_out_gg(X1, X3)) → U44_ggaa(X1, X2, X3, X4, X5, splitcD_in_ggaa(X2, X3, X4, X5))
U44_ggaa(X1, X2, X3, X4, X5, splitcD_out_ggaa(X2, X3, X4, X5)) → splitcD_out_ggaa(cons(X1, X2), X3, X4, cons(X1, X5))
U42_ggaa(X1, X2, X3, X4, X5, splitcD_out_ggaa(X2, X3, X4, X5)) → splitcD_out_ggaa(cons(X1, X2), X3, cons(X1, X4), X5)
qscH_in_ga([], []) → qscH_out_ga([], [])
qscH_in_ga(cons(X1, X2), X3) → U57_ga(X1, X2, X3, splitcD_in_ggaa(X2, X1, X4, X5))
U57_ga(X1, X2, X3, splitcD_out_ggaa(X2, X1, X4, X5)) → U58_ga(X1, X2, X3, X5, qscH_in_ga(X4, X6))
U58_ga(X1, X2, X3, X5, qscH_out_ga(X4, X6)) → U59_ga(X1, X2, X3, X6, qscH_in_ga(X5, X7))
U59_ga(X1, X2, X3, X6, qscH_out_ga(X5, X7)) → U60_ga(X1, X2, X3, appendcI_in_ggga(X6, X1, X7, X3))
appendcI_in_ggga([], X1, X2, cons(X1, X2)) → appendcI_out_ggga([], X1, X2, cons(X1, X2))
appendcI_in_ggga(cons(X1, X2), X3, X4, cons(X1, X5)) → U61_ggga(X1, X2, X3, X4, X5, appendcI_in_ggga(X2, X3, X4, X5))
U61_ggga(X1, X2, X3, X4, X5, appendcI_out_ggga(X2, X3, X4, X5)) → appendcI_out_ggga(cons(X1, X2), X3, X4, cons(X1, X5))
U60_ga(X1, X2, X3, appendcI_out_ggga(X6, X1, X7, X3)) → qscH_out_ga(cons(X1, X2), X3)
qscF_in_ga([], []) → qscF_out_ga([], [])
qscF_in_ga(cons(X1, []), X2) → U46_ga(X1, X2, qscA_in_a(X3))
U46_ga(X1, X2, qscA_out_a(X3)) → U47_ga(X1, X2, X3, qscA_in_a(X4))
U47_ga(X1, X2, X3, qscA_out_a(X4)) → U48_ga(X1, X2, appendcB_in_ggga(X3, X1, X4, X2))
appendcB_in_ggga([], X1, X2, cons(X1, X2)) → appendcB_out_ggga([], X1, X2, cons(X1, X2))
appendcB_in_ggga(cons(X1, X2), X3, X4, cons(X1, X5)) → U39_ggga(X1, X2, X3, X4, X5, appendcB_in_ggga(X2, X3, X4, X5))
U39_ggga(X1, X2, X3, X4, X5, appendcB_out_ggga(X2, X3, X4, X5)) → appendcB_out_ggga(cons(X1, X2), X3, X4, cons(X1, X5))
U48_ga(X1, X2, appendcB_out_ggga(X3, X1, X4, X2)) → qscF_out_ga(cons(X1, []), X2)
qscF_in_ga(cons(X1, cons(X2, X3)), X4) → U49_ga(X1, X2, X3, X4, lesscC_in_gg(X2, X1))
U49_ga(X1, X2, X3, X4, lesscC_out_gg(X2, X1)) → U50_ga(X1, X2, X3, X4, splitcD_in_ggaa(X3, X1, X5, X6))
U50_ga(X1, X2, X3, X4, splitcD_out_ggaa(X3, X1, X5, X6)) → U51_ga(X1, X2, X3, X4, X6, qscF_in_ga(cons(X2, X5), X7))
qscF_in_ga(cons(X1, cons(X2, X3)), X4) → U53_ga(X1, X2, X3, X4, geqcE_in_gg(X2, X1))
U53_ga(X1, X2, X3, X4, geqcE_out_gg(X2, X1)) → U54_ga(X1, X2, X3, X4, splitcD_in_ggaa(X3, X1, X5, X6))
U54_ga(X1, X2, X3, X4, splitcD_out_ggaa(X3, X1, X5, X6)) → U55_ga(X1, X2, X3, X4, X6, qscH_in_ga(X5, X7))
U55_ga(X1, X2, X3, X4, X6, qscH_out_ga(X5, X7)) → U56_ga(X1, X2, X3, X4, qcG_in_gagga(cons(X2, X6), X8, X7, X1, X4))
qcG_in_gagga(X1, X2, X3, X4, X5) → U62_gagga(X1, X2, X3, X4, X5, qscH_in_ga(X1, X2))
U62_gagga(X1, X2, X3, X4, X5, qscH_out_ga(X1, X2)) → U63_gagga(X1, X2, X3, X4, X5, appendcB_in_ggga(X3, X4, X2, X5))
U63_gagga(X1, X2, X3, X4, X5, appendcB_out_ggga(X3, X4, X2, X5)) → qcG_out_gagga(X1, X2, X3, X4, X5)
U56_ga(X1, X2, X3, X4, qcG_out_gagga(cons(X2, X6), X8, X7, X1, X4)) → qscF_out_ga(cons(X1, cons(X2, X3)), X4)
U51_ga(X1, X2, X3, X4, X6, qscF_out_ga(cons(X2, X5), X7)) → U52_ga(X1, X2, X3, X4, qcG_in_gagga(X6, X8, X7, X1, X4))
U52_ga(X1, X2, X3, X4, qcG_out_gagga(X6, X8, X7, X1, X4)) → qscF_out_ga(cons(X1, cons(X2, X3)), X4)
Infinitary Constructor Rewriting Termination of PiDP implies Termination of TRIPLES
QSF_IN_GA(cons(X1, []), X2) → U21_GA(X1, X2, qscA_in_a(X3))
U21_GA(X1, X2, qscA_out_a(X3)) → U22_GA(X1, X2, X3, qscA_in_a(X4))
U22_GA(X1, X2, X3, qscA_out_a(X4)) → U23_GA(X1, X2, appendB_in_ggga(X3, X1, X4, X2))
U22_GA(X1, X2, X3, qscA_out_a(X4)) → APPENDB_IN_GGGA(X3, X1, X4, X2)
APPENDB_IN_GGGA(cons(X1, X2), X3, X4, cons(X1, X5)) → U1_GGGA(X1, X2, X3, X4, X5, appendB_in_ggga(X2, X3, X4, X5))
APPENDB_IN_GGGA(cons(X1, X2), X3, X4, cons(X1, X5)) → APPENDB_IN_GGGA(X2, X3, X4, X5)
QSF_IN_GA(cons(X1, cons(X2, X3)), X4) → U24_GA(X1, X2, X3, X4, lessC_in_gg(X2, X1))
QSF_IN_GA(cons(X1, cons(X2, X3)), X4) → LESSC_IN_GG(X2, X1)
LESSC_IN_GG(s(X1), s(X2)) → U2_GG(X1, X2, lessC_in_gg(X1, X2))
LESSC_IN_GG(s(X1), s(X2)) → LESSC_IN_GG(X1, X2)
QSF_IN_GA(cons(X1, cons(X2, X3)), X4) → U25_GA(X1, X2, X3, X4, lesscC_in_gg(X2, X1))
U25_GA(X1, X2, X3, X4, lesscC_out_gg(X2, X1)) → U26_GA(X1, X2, X3, X4, splitD_in_ggaa(X3, X1, X5, X6))
U25_GA(X1, X2, X3, X4, lesscC_out_gg(X2, X1)) → SPLITD_IN_GGAA(X3, X1, X5, X6)
SPLITD_IN_GGAA(cons(X1, X2), X3, cons(X1, X4), X5) → U3_GGAA(X1, X2, X3, X4, X5, lessC_in_gg(X1, X3))
SPLITD_IN_GGAA(cons(X1, X2), X3, cons(X1, X4), X5) → LESSC_IN_GG(X1, X3)
SPLITD_IN_GGAA(cons(X1, X2), X3, cons(X1, X4), X5) → U4_GGAA(X1, X2, X3, X4, X5, lesscC_in_gg(X1, X3))
U4_GGAA(X1, X2, X3, X4, X5, lesscC_out_gg(X1, X3)) → U5_GGAA(X1, X2, X3, X4, X5, splitD_in_ggaa(X2, X3, X4, X5))
U4_GGAA(X1, X2, X3, X4, X5, lesscC_out_gg(X1, X3)) → SPLITD_IN_GGAA(X2, X3, X4, X5)
SPLITD_IN_GGAA(cons(X1, X2), X3, X4, cons(X1, X5)) → U6_GGAA(X1, X2, X3, X4, X5, geqE_in_gg(X1, X3))
SPLITD_IN_GGAA(cons(X1, X2), X3, X4, cons(X1, X5)) → GEQE_IN_GG(X1, X3)
GEQE_IN_GG(s(X1), s(X2)) → U9_GG(X1, X2, geqE_in_gg(X1, X2))
GEQE_IN_GG(s(X1), s(X2)) → GEQE_IN_GG(X1, X2)
SPLITD_IN_GGAA(cons(X1, X2), X3, X4, cons(X1, X5)) → U7_GGAA(X1, X2, X3, X4, X5, geqcE_in_gg(X1, X3))
U7_GGAA(X1, X2, X3, X4, X5, geqcE_out_gg(X1, X3)) → U8_GGAA(X1, X2, X3, X4, X5, splitD_in_ggaa(X2, X3, X4, X5))
U7_GGAA(X1, X2, X3, X4, X5, geqcE_out_gg(X1, X3)) → SPLITD_IN_GGAA(X2, X3, X4, X5)
U25_GA(X1, X2, X3, X4, lesscC_out_gg(X2, X1)) → U27_GA(X1, X2, X3, X4, splitcD_in_ggaa(X3, X1, X5, X6))
U27_GA(X1, X2, X3, X4, splitcD_out_ggaa(X3, X1, X5, X6)) → U28_GA(X1, X2, X3, X4, qsF_in_ga(cons(X2, X5), X7))
U27_GA(X1, X2, X3, X4, splitcD_out_ggaa(X3, X1, X5, X6)) → QSF_IN_GA(cons(X2, X5), X7)
QSF_IN_GA(cons(X1, cons(X2, X3)), X4) → U31_GA(X1, X2, X3, X4, geqE_in_gg(X2, X1))
QSF_IN_GA(cons(X1, cons(X2, X3)), X4) → GEQE_IN_GG(X2, X1)
QSF_IN_GA(cons(X1, cons(X2, X3)), X4) → U32_GA(X1, X2, X3, X4, geqcE_in_gg(X2, X1))
U32_GA(X1, X2, X3, X4, geqcE_out_gg(X2, X1)) → U33_GA(X1, X2, X3, X4, splitD_in_ggaa(X3, X1, X5, X6))
U32_GA(X1, X2, X3, X4, geqcE_out_gg(X2, X1)) → SPLITD_IN_GGAA(X3, X1, X5, X6)
U32_GA(X1, X2, X3, X4, geqcE_out_gg(X2, X1)) → U34_GA(X1, X2, X3, X4, splitcD_in_ggaa(X3, X1, X5, X6))
U34_GA(X1, X2, X3, X4, splitcD_out_ggaa(X3, X1, X5, X6)) → U35_GA(X1, X2, X3, X4, qsH_in_ga(X5, X7))
U34_GA(X1, X2, X3, X4, splitcD_out_ggaa(X3, X1, X5, X6)) → QSH_IN_GA(X5, X7)
QSH_IN_GA(cons(X1, X2), X3) → U10_GA(X1, X2, X3, splitD_in_ggaa(X2, X1, X4, X5))
QSH_IN_GA(cons(X1, X2), X3) → SPLITD_IN_GGAA(X2, X1, X4, X5)
QSH_IN_GA(cons(X1, X2), X3) → U11_GA(X1, X2, X3, splitcD_in_ggaa(X2, X1, X4, X5))
U11_GA(X1, X2, X3, splitcD_out_ggaa(X2, X1, X4, X5)) → U12_GA(X1, X2, X3, qsH_in_ga(X4, X6))
U11_GA(X1, X2, X3, splitcD_out_ggaa(X2, X1, X4, X5)) → QSH_IN_GA(X4, X6)
U11_GA(X1, X2, X3, splitcD_out_ggaa(X2, X1, X4, X5)) → U13_GA(X1, X2, X3, X5, qscH_in_ga(X4, X6))
U13_GA(X1, X2, X3, X5, qscH_out_ga(X4, X6)) → U14_GA(X1, X2, X3, qsH_in_ga(X5, X7))
U13_GA(X1, X2, X3, X5, qscH_out_ga(X4, X6)) → QSH_IN_GA(X5, X7)
U13_GA(X1, X2, X3, X5, qscH_out_ga(X4, X6)) → U15_GA(X1, X2, X3, X6, qscH_in_ga(X5, X7))
U15_GA(X1, X2, X3, X6, qscH_out_ga(X5, X7)) → U16_GA(X1, X2, X3, appendI_in_ggga(X6, X1, X7, X3))
U15_GA(X1, X2, X3, X6, qscH_out_ga(X5, X7)) → APPENDI_IN_GGGA(X6, X1, X7, X3)
APPENDI_IN_GGGA(cons(X1, X2), X3, X4, cons(X1, X5)) → U17_GGGA(X1, X2, X3, X4, X5, appendI_in_ggga(X2, X3, X4, X5))
APPENDI_IN_GGGA(cons(X1, X2), X3, X4, cons(X1, X5)) → APPENDI_IN_GGGA(X2, X3, X4, X5)
U34_GA(X1, X2, X3, X4, splitcD_out_ggaa(X3, X1, X5, X6)) → U36_GA(X1, X2, X3, X4, X6, qscH_in_ga(X5, X7))
U36_GA(X1, X2, X3, X4, X6, qscH_out_ga(X5, X7)) → U37_GA(X1, X2, X3, X4, pG_in_gagga(cons(X2, X6), X8, X7, X1, X4))
U36_GA(X1, X2, X3, X4, X6, qscH_out_ga(X5, X7)) → PG_IN_GAGGA(cons(X2, X6), X8, X7, X1, X4)
PG_IN_GAGGA(X1, X2, X3, X4, X5) → U18_GAGGA(X1, X2, X3, X4, X5, qsH_in_ga(X1, X2))
PG_IN_GAGGA(X1, X2, X3, X4, X5) → QSH_IN_GA(X1, X2)
PG_IN_GAGGA(X1, X2, X3, X4, X5) → U19_GAGGA(X1, X2, X3, X4, X5, qscH_in_ga(X1, X2))
U19_GAGGA(X1, X2, X3, X4, X5, qscH_out_ga(X1, X2)) → U20_GAGGA(X1, X2, X3, X4, X5, appendB_in_ggga(X3, X4, X2, X5))
U19_GAGGA(X1, X2, X3, X4, X5, qscH_out_ga(X1, X2)) → APPENDB_IN_GGGA(X3, X4, X2, X5)
U27_GA(X1, X2, X3, X4, splitcD_out_ggaa(X3, X1, X5, X6)) → U29_GA(X1, X2, X3, X4, X6, qscF_in_ga(cons(X2, X5), X7))
U29_GA(X1, X2, X3, X4, X6, qscF_out_ga(cons(X2, X5), X7)) → U30_GA(X1, X2, X3, X4, pG_in_gagga(X6, X8, X7, X1, X4))
U29_GA(X1, X2, X3, X4, X6, qscF_out_ga(cons(X2, X5), X7)) → PG_IN_GAGGA(X6, X8, X7, X1, X4)
qscA_in_a([]) → qscA_out_a([])
lesscC_in_gg(0, s(X1)) → lesscC_out_gg(0, s(X1))
lesscC_in_gg(s(X1), s(X2)) → U40_gg(X1, X2, lesscC_in_gg(X1, X2))
U40_gg(X1, X2, lesscC_out_gg(X1, X2)) → lesscC_out_gg(s(X1), s(X2))
geqcE_in_gg(X1, X1) → geqcE_out_gg(X1, X1)
geqcE_in_gg(s(X1), 0) → geqcE_out_gg(s(X1), 0)
geqcE_in_gg(s(X1), s(X2)) → U45_gg(X1, X2, geqcE_in_gg(X1, X2))
U45_gg(X1, X2, geqcE_out_gg(X1, X2)) → geqcE_out_gg(s(X1), s(X2))
splitcD_in_ggaa([], X1, [], []) → splitcD_out_ggaa([], X1, [], [])
splitcD_in_ggaa(cons(X1, X2), X3, cons(X1, X4), X5) → U41_ggaa(X1, X2, X3, X4, X5, lesscC_in_gg(X1, X3))
U41_ggaa(X1, X2, X3, X4, X5, lesscC_out_gg(X1, X3)) → U42_ggaa(X1, X2, X3, X4, X5, splitcD_in_ggaa(X2, X3, X4, X5))
splitcD_in_ggaa(cons(X1, X2), X3, X4, cons(X1, X5)) → U43_ggaa(X1, X2, X3, X4, X5, geqcE_in_gg(X1, X3))
U43_ggaa(X1, X2, X3, X4, X5, geqcE_out_gg(X1, X3)) → U44_ggaa(X1, X2, X3, X4, X5, splitcD_in_ggaa(X2, X3, X4, X5))
U44_ggaa(X1, X2, X3, X4, X5, splitcD_out_ggaa(X2, X3, X4, X5)) → splitcD_out_ggaa(cons(X1, X2), X3, X4, cons(X1, X5))
U42_ggaa(X1, X2, X3, X4, X5, splitcD_out_ggaa(X2, X3, X4, X5)) → splitcD_out_ggaa(cons(X1, X2), X3, cons(X1, X4), X5)
qscH_in_ga([], []) → qscH_out_ga([], [])
qscH_in_ga(cons(X1, X2), X3) → U57_ga(X1, X2, X3, splitcD_in_ggaa(X2, X1, X4, X5))
U57_ga(X1, X2, X3, splitcD_out_ggaa(X2, X1, X4, X5)) → U58_ga(X1, X2, X3, X5, qscH_in_ga(X4, X6))
U58_ga(X1, X2, X3, X5, qscH_out_ga(X4, X6)) → U59_ga(X1, X2, X3, X6, qscH_in_ga(X5, X7))
U59_ga(X1, X2, X3, X6, qscH_out_ga(X5, X7)) → U60_ga(X1, X2, X3, appendcI_in_ggga(X6, X1, X7, X3))
appendcI_in_ggga([], X1, X2, cons(X1, X2)) → appendcI_out_ggga([], X1, X2, cons(X1, X2))
appendcI_in_ggga(cons(X1, X2), X3, X4, cons(X1, X5)) → U61_ggga(X1, X2, X3, X4, X5, appendcI_in_ggga(X2, X3, X4, X5))
U61_ggga(X1, X2, X3, X4, X5, appendcI_out_ggga(X2, X3, X4, X5)) → appendcI_out_ggga(cons(X1, X2), X3, X4, cons(X1, X5))
U60_ga(X1, X2, X3, appendcI_out_ggga(X6, X1, X7, X3)) → qscH_out_ga(cons(X1, X2), X3)
qscF_in_ga([], []) → qscF_out_ga([], [])
qscF_in_ga(cons(X1, []), X2) → U46_ga(X1, X2, qscA_in_a(X3))
U46_ga(X1, X2, qscA_out_a(X3)) → U47_ga(X1, X2, X3, qscA_in_a(X4))
U47_ga(X1, X2, X3, qscA_out_a(X4)) → U48_ga(X1, X2, appendcB_in_ggga(X3, X1, X4, X2))
appendcB_in_ggga([], X1, X2, cons(X1, X2)) → appendcB_out_ggga([], X1, X2, cons(X1, X2))
appendcB_in_ggga(cons(X1, X2), X3, X4, cons(X1, X5)) → U39_ggga(X1, X2, X3, X4, X5, appendcB_in_ggga(X2, X3, X4, X5))
U39_ggga(X1, X2, X3, X4, X5, appendcB_out_ggga(X2, X3, X4, X5)) → appendcB_out_ggga(cons(X1, X2), X3, X4, cons(X1, X5))
U48_ga(X1, X2, appendcB_out_ggga(X3, X1, X4, X2)) → qscF_out_ga(cons(X1, []), X2)
qscF_in_ga(cons(X1, cons(X2, X3)), X4) → U49_ga(X1, X2, X3, X4, lesscC_in_gg(X2, X1))
U49_ga(X1, X2, X3, X4, lesscC_out_gg(X2, X1)) → U50_ga(X1, X2, X3, X4, splitcD_in_ggaa(X3, X1, X5, X6))
U50_ga(X1, X2, X3, X4, splitcD_out_ggaa(X3, X1, X5, X6)) → U51_ga(X1, X2, X3, X4, X6, qscF_in_ga(cons(X2, X5), X7))
qscF_in_ga(cons(X1, cons(X2, X3)), X4) → U53_ga(X1, X2, X3, X4, geqcE_in_gg(X2, X1))
U53_ga(X1, X2, X3, X4, geqcE_out_gg(X2, X1)) → U54_ga(X1, X2, X3, X4, splitcD_in_ggaa(X3, X1, X5, X6))
U54_ga(X1, X2, X3, X4, splitcD_out_ggaa(X3, X1, X5, X6)) → U55_ga(X1, X2, X3, X4, X6, qscH_in_ga(X5, X7))
U55_ga(X1, X2, X3, X4, X6, qscH_out_ga(X5, X7)) → U56_ga(X1, X2, X3, X4, qcG_in_gagga(cons(X2, X6), X8, X7, X1, X4))
qcG_in_gagga(X1, X2, X3, X4, X5) → U62_gagga(X1, X2, X3, X4, X5, qscH_in_ga(X1, X2))
U62_gagga(X1, X2, X3, X4, X5, qscH_out_ga(X1, X2)) → U63_gagga(X1, X2, X3, X4, X5, appendcB_in_ggga(X3, X4, X2, X5))
U63_gagga(X1, X2, X3, X4, X5, appendcB_out_ggga(X3, X4, X2, X5)) → qcG_out_gagga(X1, X2, X3, X4, X5)
U56_ga(X1, X2, X3, X4, qcG_out_gagga(cons(X2, X6), X8, X7, X1, X4)) → qscF_out_ga(cons(X1, cons(X2, X3)), X4)
U51_ga(X1, X2, X3, X4, X6, qscF_out_ga(cons(X2, X5), X7)) → U52_ga(X1, X2, X3, X4, qcG_in_gagga(X6, X8, X7, X1, X4))
U52_ga(X1, X2, X3, X4, qcG_out_gagga(X6, X8, X7, X1, X4)) → qscF_out_ga(cons(X1, cons(X2, X3)), X4)
APPENDI_IN_GGGA(cons(X1, X2), X3, X4, cons(X1, X5)) → APPENDI_IN_GGGA(X2, X3, X4, X5)
qscA_in_a([]) → qscA_out_a([])
lesscC_in_gg(0, s(X1)) → lesscC_out_gg(0, s(X1))
lesscC_in_gg(s(X1), s(X2)) → U40_gg(X1, X2, lesscC_in_gg(X1, X2))
U40_gg(X1, X2, lesscC_out_gg(X1, X2)) → lesscC_out_gg(s(X1), s(X2))
geqcE_in_gg(X1, X1) → geqcE_out_gg(X1, X1)
geqcE_in_gg(s(X1), 0) → geqcE_out_gg(s(X1), 0)
geqcE_in_gg(s(X1), s(X2)) → U45_gg(X1, X2, geqcE_in_gg(X1, X2))
U45_gg(X1, X2, geqcE_out_gg(X1, X2)) → geqcE_out_gg(s(X1), s(X2))
splitcD_in_ggaa([], X1, [], []) → splitcD_out_ggaa([], X1, [], [])
splitcD_in_ggaa(cons(X1, X2), X3, cons(X1, X4), X5) → U41_ggaa(X1, X2, X3, X4, X5, lesscC_in_gg(X1, X3))
U41_ggaa(X1, X2, X3, X4, X5, lesscC_out_gg(X1, X3)) → U42_ggaa(X1, X2, X3, X4, X5, splitcD_in_ggaa(X2, X3, X4, X5))
splitcD_in_ggaa(cons(X1, X2), X3, X4, cons(X1, X5)) → U43_ggaa(X1, X2, X3, X4, X5, geqcE_in_gg(X1, X3))
U43_ggaa(X1, X2, X3, X4, X5, geqcE_out_gg(X1, X3)) → U44_ggaa(X1, X2, X3, X4, X5, splitcD_in_ggaa(X2, X3, X4, X5))
U44_ggaa(X1, X2, X3, X4, X5, splitcD_out_ggaa(X2, X3, X4, X5)) → splitcD_out_ggaa(cons(X1, X2), X3, X4, cons(X1, X5))
U42_ggaa(X1, X2, X3, X4, X5, splitcD_out_ggaa(X2, X3, X4, X5)) → splitcD_out_ggaa(cons(X1, X2), X3, cons(X1, X4), X5)
qscH_in_ga([], []) → qscH_out_ga([], [])
qscH_in_ga(cons(X1, X2), X3) → U57_ga(X1, X2, X3, splitcD_in_ggaa(X2, X1, X4, X5))
U57_ga(X1, X2, X3, splitcD_out_ggaa(X2, X1, X4, X5)) → U58_ga(X1, X2, X3, X5, qscH_in_ga(X4, X6))
U58_ga(X1, X2, X3, X5, qscH_out_ga(X4, X6)) → U59_ga(X1, X2, X3, X6, qscH_in_ga(X5, X7))
U59_ga(X1, X2, X3, X6, qscH_out_ga(X5, X7)) → U60_ga(X1, X2, X3, appendcI_in_ggga(X6, X1, X7, X3))
appendcI_in_ggga([], X1, X2, cons(X1, X2)) → appendcI_out_ggga([], X1, X2, cons(X1, X2))
appendcI_in_ggga(cons(X1, X2), X3, X4, cons(X1, X5)) → U61_ggga(X1, X2, X3, X4, X5, appendcI_in_ggga(X2, X3, X4, X5))
U61_ggga(X1, X2, X3, X4, X5, appendcI_out_ggga(X2, X3, X4, X5)) → appendcI_out_ggga(cons(X1, X2), X3, X4, cons(X1, X5))
U60_ga(X1, X2, X3, appendcI_out_ggga(X6, X1, X7, X3)) → qscH_out_ga(cons(X1, X2), X3)
qscF_in_ga([], []) → qscF_out_ga([], [])
qscF_in_ga(cons(X1, []), X2) → U46_ga(X1, X2, qscA_in_a(X3))
U46_ga(X1, X2, qscA_out_a(X3)) → U47_ga(X1, X2, X3, qscA_in_a(X4))
U47_ga(X1, X2, X3, qscA_out_a(X4)) → U48_ga(X1, X2, appendcB_in_ggga(X3, X1, X4, X2))
appendcB_in_ggga([], X1, X2, cons(X1, X2)) → appendcB_out_ggga([], X1, X2, cons(X1, X2))
appendcB_in_ggga(cons(X1, X2), X3, X4, cons(X1, X5)) → U39_ggga(X1, X2, X3, X4, X5, appendcB_in_ggga(X2, X3, X4, X5))
U39_ggga(X1, X2, X3, X4, X5, appendcB_out_ggga(X2, X3, X4, X5)) → appendcB_out_ggga(cons(X1, X2), X3, X4, cons(X1, X5))
U48_ga(X1, X2, appendcB_out_ggga(X3, X1, X4, X2)) → qscF_out_ga(cons(X1, []), X2)
qscF_in_ga(cons(X1, cons(X2, X3)), X4) → U49_ga(X1, X2, X3, X4, lesscC_in_gg(X2, X1))
U49_ga(X1, X2, X3, X4, lesscC_out_gg(X2, X1)) → U50_ga(X1, X2, X3, X4, splitcD_in_ggaa(X3, X1, X5, X6))
U50_ga(X1, X2, X3, X4, splitcD_out_ggaa(X3, X1, X5, X6)) → U51_ga(X1, X2, X3, X4, X6, qscF_in_ga(cons(X2, X5), X7))
qscF_in_ga(cons(X1, cons(X2, X3)), X4) → U53_ga(X1, X2, X3, X4, geqcE_in_gg(X2, X1))
U53_ga(X1, X2, X3, X4, geqcE_out_gg(X2, X1)) → U54_ga(X1, X2, X3, X4, splitcD_in_ggaa(X3, X1, X5, X6))
U54_ga(X1, X2, X3, X4, splitcD_out_ggaa(X3, X1, X5, X6)) → U55_ga(X1, X2, X3, X4, X6, qscH_in_ga(X5, X7))
U55_ga(X1, X2, X3, X4, X6, qscH_out_ga(X5, X7)) → U56_ga(X1, X2, X3, X4, qcG_in_gagga(cons(X2, X6), X8, X7, X1, X4))
qcG_in_gagga(X1, X2, X3, X4, X5) → U62_gagga(X1, X2, X3, X4, X5, qscH_in_ga(X1, X2))
U62_gagga(X1, X2, X3, X4, X5, qscH_out_ga(X1, X2)) → U63_gagga(X1, X2, X3, X4, X5, appendcB_in_ggga(X3, X4, X2, X5))
U63_gagga(X1, X2, X3, X4, X5, appendcB_out_ggga(X3, X4, X2, X5)) → qcG_out_gagga(X1, X2, X3, X4, X5)
U56_ga(X1, X2, X3, X4, qcG_out_gagga(cons(X2, X6), X8, X7, X1, X4)) → qscF_out_ga(cons(X1, cons(X2, X3)), X4)
U51_ga(X1, X2, X3, X4, X6, qscF_out_ga(cons(X2, X5), X7)) → U52_ga(X1, X2, X3, X4, qcG_in_gagga(X6, X8, X7, X1, X4))
U52_ga(X1, X2, X3, X4, qcG_out_gagga(X6, X8, X7, X1, X4)) → qscF_out_ga(cons(X1, cons(X2, X3)), X4)
APPENDI_IN_GGGA(cons(X1, X2), X3, X4, cons(X1, X5)) → APPENDI_IN_GGGA(X2, X3, X4, X5)
APPENDI_IN_GGGA(cons(X1, X2), X3, X4) → APPENDI_IN_GGGA(X2, X3, X4)
From the DPs we obtained the following set of size-change graphs:
GEQE_IN_GG(s(X1), s(X2)) → GEQE_IN_GG(X1, X2)
qscA_in_a([]) → qscA_out_a([])
lesscC_in_gg(0, s(X1)) → lesscC_out_gg(0, s(X1))
lesscC_in_gg(s(X1), s(X2)) → U40_gg(X1, X2, lesscC_in_gg(X1, X2))
U40_gg(X1, X2, lesscC_out_gg(X1, X2)) → lesscC_out_gg(s(X1), s(X2))
geqcE_in_gg(X1, X1) → geqcE_out_gg(X1, X1)
geqcE_in_gg(s(X1), 0) → geqcE_out_gg(s(X1), 0)
geqcE_in_gg(s(X1), s(X2)) → U45_gg(X1, X2, geqcE_in_gg(X1, X2))
U45_gg(X1, X2, geqcE_out_gg(X1, X2)) → geqcE_out_gg(s(X1), s(X2))
splitcD_in_ggaa([], X1, [], []) → splitcD_out_ggaa([], X1, [], [])
splitcD_in_ggaa(cons(X1, X2), X3, cons(X1, X4), X5) → U41_ggaa(X1, X2, X3, X4, X5, lesscC_in_gg(X1, X3))
U41_ggaa(X1, X2, X3, X4, X5, lesscC_out_gg(X1, X3)) → U42_ggaa(X1, X2, X3, X4, X5, splitcD_in_ggaa(X2, X3, X4, X5))
splitcD_in_ggaa(cons(X1, X2), X3, X4, cons(X1, X5)) → U43_ggaa(X1, X2, X3, X4, X5, geqcE_in_gg(X1, X3))
U43_ggaa(X1, X2, X3, X4, X5, geqcE_out_gg(X1, X3)) → U44_ggaa(X1, X2, X3, X4, X5, splitcD_in_ggaa(X2, X3, X4, X5))
U44_ggaa(X1, X2, X3, X4, X5, splitcD_out_ggaa(X2, X3, X4, X5)) → splitcD_out_ggaa(cons(X1, X2), X3, X4, cons(X1, X5))
U42_ggaa(X1, X2, X3, X4, X5, splitcD_out_ggaa(X2, X3, X4, X5)) → splitcD_out_ggaa(cons(X1, X2), X3, cons(X1, X4), X5)
qscH_in_ga([], []) → qscH_out_ga([], [])
qscH_in_ga(cons(X1, X2), X3) → U57_ga(X1, X2, X3, splitcD_in_ggaa(X2, X1, X4, X5))
U57_ga(X1, X2, X3, splitcD_out_ggaa(X2, X1, X4, X5)) → U58_ga(X1, X2, X3, X5, qscH_in_ga(X4, X6))
U58_ga(X1, X2, X3, X5, qscH_out_ga(X4, X6)) → U59_ga(X1, X2, X3, X6, qscH_in_ga(X5, X7))
U59_ga(X1, X2, X3, X6, qscH_out_ga(X5, X7)) → U60_ga(X1, X2, X3, appendcI_in_ggga(X6, X1, X7, X3))
appendcI_in_ggga([], X1, X2, cons(X1, X2)) → appendcI_out_ggga([], X1, X2, cons(X1, X2))
appendcI_in_ggga(cons(X1, X2), X3, X4, cons(X1, X5)) → U61_ggga(X1, X2, X3, X4, X5, appendcI_in_ggga(X2, X3, X4, X5))
U61_ggga(X1, X2, X3, X4, X5, appendcI_out_ggga(X2, X3, X4, X5)) → appendcI_out_ggga(cons(X1, X2), X3, X4, cons(X1, X5))
U60_ga(X1, X2, X3, appendcI_out_ggga(X6, X1, X7, X3)) → qscH_out_ga(cons(X1, X2), X3)
qscF_in_ga([], []) → qscF_out_ga([], [])
qscF_in_ga(cons(X1, []), X2) → U46_ga(X1, X2, qscA_in_a(X3))
U46_ga(X1, X2, qscA_out_a(X3)) → U47_ga(X1, X2, X3, qscA_in_a(X4))
U47_ga(X1, X2, X3, qscA_out_a(X4)) → U48_ga(X1, X2, appendcB_in_ggga(X3, X1, X4, X2))
appendcB_in_ggga([], X1, X2, cons(X1, X2)) → appendcB_out_ggga([], X1, X2, cons(X1, X2))
appendcB_in_ggga(cons(X1, X2), X3, X4, cons(X1, X5)) → U39_ggga(X1, X2, X3, X4, X5, appendcB_in_ggga(X2, X3, X4, X5))
U39_ggga(X1, X2, X3, X4, X5, appendcB_out_ggga(X2, X3, X4, X5)) → appendcB_out_ggga(cons(X1, X2), X3, X4, cons(X1, X5))
U48_ga(X1, X2, appendcB_out_ggga(X3, X1, X4, X2)) → qscF_out_ga(cons(X1, []), X2)
qscF_in_ga(cons(X1, cons(X2, X3)), X4) → U49_ga(X1, X2, X3, X4, lesscC_in_gg(X2, X1))
U49_ga(X1, X2, X3, X4, lesscC_out_gg(X2, X1)) → U50_ga(X1, X2, X3, X4, splitcD_in_ggaa(X3, X1, X5, X6))
U50_ga(X1, X2, X3, X4, splitcD_out_ggaa(X3, X1, X5, X6)) → U51_ga(X1, X2, X3, X4, X6, qscF_in_ga(cons(X2, X5), X7))
qscF_in_ga(cons(X1, cons(X2, X3)), X4) → U53_ga(X1, X2, X3, X4, geqcE_in_gg(X2, X1))
U53_ga(X1, X2, X3, X4, geqcE_out_gg(X2, X1)) → U54_ga(X1, X2, X3, X4, splitcD_in_ggaa(X3, X1, X5, X6))
U54_ga(X1, X2, X3, X4, splitcD_out_ggaa(X3, X1, X5, X6)) → U55_ga(X1, X2, X3, X4, X6, qscH_in_ga(X5, X7))
U55_ga(X1, X2, X3, X4, X6, qscH_out_ga(X5, X7)) → U56_ga(X1, X2, X3, X4, qcG_in_gagga(cons(X2, X6), X8, X7, X1, X4))
qcG_in_gagga(X1, X2, X3, X4, X5) → U62_gagga(X1, X2, X3, X4, X5, qscH_in_ga(X1, X2))
U62_gagga(X1, X2, X3, X4, X5, qscH_out_ga(X1, X2)) → U63_gagga(X1, X2, X3, X4, X5, appendcB_in_ggga(X3, X4, X2, X5))
U63_gagga(X1, X2, X3, X4, X5, appendcB_out_ggga(X3, X4, X2, X5)) → qcG_out_gagga(X1, X2, X3, X4, X5)
U56_ga(X1, X2, X3, X4, qcG_out_gagga(cons(X2, X6), X8, X7, X1, X4)) → qscF_out_ga(cons(X1, cons(X2, X3)), X4)
U51_ga(X1, X2, X3, X4, X6, qscF_out_ga(cons(X2, X5), X7)) → U52_ga(X1, X2, X3, X4, qcG_in_gagga(X6, X8, X7, X1, X4))
U52_ga(X1, X2, X3, X4, qcG_out_gagga(X6, X8, X7, X1, X4)) → qscF_out_ga(cons(X1, cons(X2, X3)), X4)
GEQE_IN_GG(s(X1), s(X2)) → GEQE_IN_GG(X1, X2)
GEQE_IN_GG(s(X1), s(X2)) → GEQE_IN_GG(X1, X2)
From the DPs we obtained the following set of size-change graphs:
LESSC_IN_GG(s(X1), s(X2)) → LESSC_IN_GG(X1, X2)
qscA_in_a([]) → qscA_out_a([])
lesscC_in_gg(0, s(X1)) → lesscC_out_gg(0, s(X1))
lesscC_in_gg(s(X1), s(X2)) → U40_gg(X1, X2, lesscC_in_gg(X1, X2))
U40_gg(X1, X2, lesscC_out_gg(X1, X2)) → lesscC_out_gg(s(X1), s(X2))
geqcE_in_gg(X1, X1) → geqcE_out_gg(X1, X1)
geqcE_in_gg(s(X1), 0) → geqcE_out_gg(s(X1), 0)
geqcE_in_gg(s(X1), s(X2)) → U45_gg(X1, X2, geqcE_in_gg(X1, X2))
U45_gg(X1, X2, geqcE_out_gg(X1, X2)) → geqcE_out_gg(s(X1), s(X2))
splitcD_in_ggaa([], X1, [], []) → splitcD_out_ggaa([], X1, [], [])
splitcD_in_ggaa(cons(X1, X2), X3, cons(X1, X4), X5) → U41_ggaa(X1, X2, X3, X4, X5, lesscC_in_gg(X1, X3))
U41_ggaa(X1, X2, X3, X4, X5, lesscC_out_gg(X1, X3)) → U42_ggaa(X1, X2, X3, X4, X5, splitcD_in_ggaa(X2, X3, X4, X5))
splitcD_in_ggaa(cons(X1, X2), X3, X4, cons(X1, X5)) → U43_ggaa(X1, X2, X3, X4, X5, geqcE_in_gg(X1, X3))
U43_ggaa(X1, X2, X3, X4, X5, geqcE_out_gg(X1, X3)) → U44_ggaa(X1, X2, X3, X4, X5, splitcD_in_ggaa(X2, X3, X4, X5))
U44_ggaa(X1, X2, X3, X4, X5, splitcD_out_ggaa(X2, X3, X4, X5)) → splitcD_out_ggaa(cons(X1, X2), X3, X4, cons(X1, X5))
U42_ggaa(X1, X2, X3, X4, X5, splitcD_out_ggaa(X2, X3, X4, X5)) → splitcD_out_ggaa(cons(X1, X2), X3, cons(X1, X4), X5)
qscH_in_ga([], []) → qscH_out_ga([], [])
qscH_in_ga(cons(X1, X2), X3) → U57_ga(X1, X2, X3, splitcD_in_ggaa(X2, X1, X4, X5))
U57_ga(X1, X2, X3, splitcD_out_ggaa(X2, X1, X4, X5)) → U58_ga(X1, X2, X3, X5, qscH_in_ga(X4, X6))
U58_ga(X1, X2, X3, X5, qscH_out_ga(X4, X6)) → U59_ga(X1, X2, X3, X6, qscH_in_ga(X5, X7))
U59_ga(X1, X2, X3, X6, qscH_out_ga(X5, X7)) → U60_ga(X1, X2, X3, appendcI_in_ggga(X6, X1, X7, X3))
appendcI_in_ggga([], X1, X2, cons(X1, X2)) → appendcI_out_ggga([], X1, X2, cons(X1, X2))
appendcI_in_ggga(cons(X1, X2), X3, X4, cons(X1, X5)) → U61_ggga(X1, X2, X3, X4, X5, appendcI_in_ggga(X2, X3, X4, X5))
U61_ggga(X1, X2, X3, X4, X5, appendcI_out_ggga(X2, X3, X4, X5)) → appendcI_out_ggga(cons(X1, X2), X3, X4, cons(X1, X5))
U60_ga(X1, X2, X3, appendcI_out_ggga(X6, X1, X7, X3)) → qscH_out_ga(cons(X1, X2), X3)
qscF_in_ga([], []) → qscF_out_ga([], [])
qscF_in_ga(cons(X1, []), X2) → U46_ga(X1, X2, qscA_in_a(X3))
U46_ga(X1, X2, qscA_out_a(X3)) → U47_ga(X1, X2, X3, qscA_in_a(X4))
U47_ga(X1, X2, X3, qscA_out_a(X4)) → U48_ga(X1, X2, appendcB_in_ggga(X3, X1, X4, X2))
appendcB_in_ggga([], X1, X2, cons(X1, X2)) → appendcB_out_ggga([], X1, X2, cons(X1, X2))
appendcB_in_ggga(cons(X1, X2), X3, X4, cons(X1, X5)) → U39_ggga(X1, X2, X3, X4, X5, appendcB_in_ggga(X2, X3, X4, X5))
U39_ggga(X1, X2, X3, X4, X5, appendcB_out_ggga(X2, X3, X4, X5)) → appendcB_out_ggga(cons(X1, X2), X3, X4, cons(X1, X5))
U48_ga(X1, X2, appendcB_out_ggga(X3, X1, X4, X2)) → qscF_out_ga(cons(X1, []), X2)
qscF_in_ga(cons(X1, cons(X2, X3)), X4) → U49_ga(X1, X2, X3, X4, lesscC_in_gg(X2, X1))
U49_ga(X1, X2, X3, X4, lesscC_out_gg(X2, X1)) → U50_ga(X1, X2, X3, X4, splitcD_in_ggaa(X3, X1, X5, X6))
U50_ga(X1, X2, X3, X4, splitcD_out_ggaa(X3, X1, X5, X6)) → U51_ga(X1, X2, X3, X4, X6, qscF_in_ga(cons(X2, X5), X7))
qscF_in_ga(cons(X1, cons(X2, X3)), X4) → U53_ga(X1, X2, X3, X4, geqcE_in_gg(X2, X1))
U53_ga(X1, X2, X3, X4, geqcE_out_gg(X2, X1)) → U54_ga(X1, X2, X3, X4, splitcD_in_ggaa(X3, X1, X5, X6))
U54_ga(X1, X2, X3, X4, splitcD_out_ggaa(X3, X1, X5, X6)) → U55_ga(X1, X2, X3, X4, X6, qscH_in_ga(X5, X7))
U55_ga(X1, X2, X3, X4, X6, qscH_out_ga(X5, X7)) → U56_ga(X1, X2, X3, X4, qcG_in_gagga(cons(X2, X6), X8, X7, X1, X4))
qcG_in_gagga(X1, X2, X3, X4, X5) → U62_gagga(X1, X2, X3, X4, X5, qscH_in_ga(X1, X2))
U62_gagga(X1, X2, X3, X4, X5, qscH_out_ga(X1, X2)) → U63_gagga(X1, X2, X3, X4, X5, appendcB_in_ggga(X3, X4, X2, X5))
U63_gagga(X1, X2, X3, X4, X5, appendcB_out_ggga(X3, X4, X2, X5)) → qcG_out_gagga(X1, X2, X3, X4, X5)
U56_ga(X1, X2, X3, X4, qcG_out_gagga(cons(X2, X6), X8, X7, X1, X4)) → qscF_out_ga(cons(X1, cons(X2, X3)), X4)
U51_ga(X1, X2, X3, X4, X6, qscF_out_ga(cons(X2, X5), X7)) → U52_ga(X1, X2, X3, X4, qcG_in_gagga(X6, X8, X7, X1, X4))
U52_ga(X1, X2, X3, X4, qcG_out_gagga(X6, X8, X7, X1, X4)) → qscF_out_ga(cons(X1, cons(X2, X3)), X4)
LESSC_IN_GG(s(X1), s(X2)) → LESSC_IN_GG(X1, X2)
LESSC_IN_GG(s(X1), s(X2)) → LESSC_IN_GG(X1, X2)
From the DPs we obtained the following set of size-change graphs:
SPLITD_IN_GGAA(cons(X1, X2), X3, cons(X1, X4), X5) → U4_GGAA(X1, X2, X3, X4, X5, lesscC_in_gg(X1, X3))
U4_GGAA(X1, X2, X3, X4, X5, lesscC_out_gg(X1, X3)) → SPLITD_IN_GGAA(X2, X3, X4, X5)
SPLITD_IN_GGAA(cons(X1, X2), X3, X4, cons(X1, X5)) → U7_GGAA(X1, X2, X3, X4, X5, geqcE_in_gg(X1, X3))
U7_GGAA(X1, X2, X3, X4, X5, geqcE_out_gg(X1, X3)) → SPLITD_IN_GGAA(X2, X3, X4, X5)
qscA_in_a([]) → qscA_out_a([])
lesscC_in_gg(0, s(X1)) → lesscC_out_gg(0, s(X1))
lesscC_in_gg(s(X1), s(X2)) → U40_gg(X1, X2, lesscC_in_gg(X1, X2))
U40_gg(X1, X2, lesscC_out_gg(X1, X2)) → lesscC_out_gg(s(X1), s(X2))
geqcE_in_gg(X1, X1) → geqcE_out_gg(X1, X1)
geqcE_in_gg(s(X1), 0) → geqcE_out_gg(s(X1), 0)
geqcE_in_gg(s(X1), s(X2)) → U45_gg(X1, X2, geqcE_in_gg(X1, X2))
U45_gg(X1, X2, geqcE_out_gg(X1, X2)) → geqcE_out_gg(s(X1), s(X2))
splitcD_in_ggaa([], X1, [], []) → splitcD_out_ggaa([], X1, [], [])
splitcD_in_ggaa(cons(X1, X2), X3, cons(X1, X4), X5) → U41_ggaa(X1, X2, X3, X4, X5, lesscC_in_gg(X1, X3))
U41_ggaa(X1, X2, X3, X4, X5, lesscC_out_gg(X1, X3)) → U42_ggaa(X1, X2, X3, X4, X5, splitcD_in_ggaa(X2, X3, X4, X5))
splitcD_in_ggaa(cons(X1, X2), X3, X4, cons(X1, X5)) → U43_ggaa(X1, X2, X3, X4, X5, geqcE_in_gg(X1, X3))
U43_ggaa(X1, X2, X3, X4, X5, geqcE_out_gg(X1, X3)) → U44_ggaa(X1, X2, X3, X4, X5, splitcD_in_ggaa(X2, X3, X4, X5))
U44_ggaa(X1, X2, X3, X4, X5, splitcD_out_ggaa(X2, X3, X4, X5)) → splitcD_out_ggaa(cons(X1, X2), X3, X4, cons(X1, X5))
U42_ggaa(X1, X2, X3, X4, X5, splitcD_out_ggaa(X2, X3, X4, X5)) → splitcD_out_ggaa(cons(X1, X2), X3, cons(X1, X4), X5)
qscH_in_ga([], []) → qscH_out_ga([], [])
qscH_in_ga(cons(X1, X2), X3) → U57_ga(X1, X2, X3, splitcD_in_ggaa(X2, X1, X4, X5))
U57_ga(X1, X2, X3, splitcD_out_ggaa(X2, X1, X4, X5)) → U58_ga(X1, X2, X3, X5, qscH_in_ga(X4, X6))
U58_ga(X1, X2, X3, X5, qscH_out_ga(X4, X6)) → U59_ga(X1, X2, X3, X6, qscH_in_ga(X5, X7))
U59_ga(X1, X2, X3, X6, qscH_out_ga(X5, X7)) → U60_ga(X1, X2, X3, appendcI_in_ggga(X6, X1, X7, X3))
appendcI_in_ggga([], X1, X2, cons(X1, X2)) → appendcI_out_ggga([], X1, X2, cons(X1, X2))
appendcI_in_ggga(cons(X1, X2), X3, X4, cons(X1, X5)) → U61_ggga(X1, X2, X3, X4, X5, appendcI_in_ggga(X2, X3, X4, X5))
U61_ggga(X1, X2, X3, X4, X5, appendcI_out_ggga(X2, X3, X4, X5)) → appendcI_out_ggga(cons(X1, X2), X3, X4, cons(X1, X5))
U60_ga(X1, X2, X3, appendcI_out_ggga(X6, X1, X7, X3)) → qscH_out_ga(cons(X1, X2), X3)
qscF_in_ga([], []) → qscF_out_ga([], [])
qscF_in_ga(cons(X1, []), X2) → U46_ga(X1, X2, qscA_in_a(X3))
U46_ga(X1, X2, qscA_out_a(X3)) → U47_ga(X1, X2, X3, qscA_in_a(X4))
U47_ga(X1, X2, X3, qscA_out_a(X4)) → U48_ga(X1, X2, appendcB_in_ggga(X3, X1, X4, X2))
appendcB_in_ggga([], X1, X2, cons(X1, X2)) → appendcB_out_ggga([], X1, X2, cons(X1, X2))
appendcB_in_ggga(cons(X1, X2), X3, X4, cons(X1, X5)) → U39_ggga(X1, X2, X3, X4, X5, appendcB_in_ggga(X2, X3, X4, X5))
U39_ggga(X1, X2, X3, X4, X5, appendcB_out_ggga(X2, X3, X4, X5)) → appendcB_out_ggga(cons(X1, X2), X3, X4, cons(X1, X5))
U48_ga(X1, X2, appendcB_out_ggga(X3, X1, X4, X2)) → qscF_out_ga(cons(X1, []), X2)
qscF_in_ga(cons(X1, cons(X2, X3)), X4) → U49_ga(X1, X2, X3, X4, lesscC_in_gg(X2, X1))
U49_ga(X1, X2, X3, X4, lesscC_out_gg(X2, X1)) → U50_ga(X1, X2, X3, X4, splitcD_in_ggaa(X3, X1, X5, X6))
U50_ga(X1, X2, X3, X4, splitcD_out_ggaa(X3, X1, X5, X6)) → U51_ga(X1, X2, X3, X4, X6, qscF_in_ga(cons(X2, X5), X7))
qscF_in_ga(cons(X1, cons(X2, X3)), X4) → U53_ga(X1, X2, X3, X4, geqcE_in_gg(X2, X1))
U53_ga(X1, X2, X3, X4, geqcE_out_gg(X2, X1)) → U54_ga(X1, X2, X3, X4, splitcD_in_ggaa(X3, X1, X5, X6))
U54_ga(X1, X2, X3, X4, splitcD_out_ggaa(X3, X1, X5, X6)) → U55_ga(X1, X2, X3, X4, X6, qscH_in_ga(X5, X7))
U55_ga(X1, X2, X3, X4, X6, qscH_out_ga(X5, X7)) → U56_ga(X1, X2, X3, X4, qcG_in_gagga(cons(X2, X6), X8, X7, X1, X4))
qcG_in_gagga(X1, X2, X3, X4, X5) → U62_gagga(X1, X2, X3, X4, X5, qscH_in_ga(X1, X2))
U62_gagga(X1, X2, X3, X4, X5, qscH_out_ga(X1, X2)) → U63_gagga(X1, X2, X3, X4, X5, appendcB_in_ggga(X3, X4, X2, X5))
U63_gagga(X1, X2, X3, X4, X5, appendcB_out_ggga(X3, X4, X2, X5)) → qcG_out_gagga(X1, X2, X3, X4, X5)
U56_ga(X1, X2, X3, X4, qcG_out_gagga(cons(X2, X6), X8, X7, X1, X4)) → qscF_out_ga(cons(X1, cons(X2, X3)), X4)
U51_ga(X1, X2, X3, X4, X6, qscF_out_ga(cons(X2, X5), X7)) → U52_ga(X1, X2, X3, X4, qcG_in_gagga(X6, X8, X7, X1, X4))
U52_ga(X1, X2, X3, X4, qcG_out_gagga(X6, X8, X7, X1, X4)) → qscF_out_ga(cons(X1, cons(X2, X3)), X4)
SPLITD_IN_GGAA(cons(X1, X2), X3, cons(X1, X4), X5) → U4_GGAA(X1, X2, X3, X4, X5, lesscC_in_gg(X1, X3))
U4_GGAA(X1, X2, X3, X4, X5, lesscC_out_gg(X1, X3)) → SPLITD_IN_GGAA(X2, X3, X4, X5)
SPLITD_IN_GGAA(cons(X1, X2), X3, X4, cons(X1, X5)) → U7_GGAA(X1, X2, X3, X4, X5, geqcE_in_gg(X1, X3))
U7_GGAA(X1, X2, X3, X4, X5, geqcE_out_gg(X1, X3)) → SPLITD_IN_GGAA(X2, X3, X4, X5)
lesscC_in_gg(0, s(X1)) → lesscC_out_gg(0, s(X1))
lesscC_in_gg(s(X1), s(X2)) → U40_gg(X1, X2, lesscC_in_gg(X1, X2))
geqcE_in_gg(X1, X1) → geqcE_out_gg(X1, X1)
geqcE_in_gg(s(X1), 0) → geqcE_out_gg(s(X1), 0)
geqcE_in_gg(s(X1), s(X2)) → U45_gg(X1, X2, geqcE_in_gg(X1, X2))
U40_gg(X1, X2, lesscC_out_gg(X1, X2)) → lesscC_out_gg(s(X1), s(X2))
U45_gg(X1, X2, geqcE_out_gg(X1, X2)) → geqcE_out_gg(s(X1), s(X2))
SPLITD_IN_GGAA(cons(X1, X2), X3) → U4_GGAA(X1, X2, X3, lesscC_in_gg(X1, X3))
U4_GGAA(X1, X2, X3, lesscC_out_gg(X1, X3)) → SPLITD_IN_GGAA(X2, X3)
SPLITD_IN_GGAA(cons(X1, X2), X3) → U7_GGAA(X1, X2, X3, geqcE_in_gg(X1, X3))
U7_GGAA(X1, X2, X3, geqcE_out_gg(X1, X3)) → SPLITD_IN_GGAA(X2, X3)
lesscC_in_gg(0, s(X1)) → lesscC_out_gg(0, s(X1))
lesscC_in_gg(s(X1), s(X2)) → U40_gg(X1, X2, lesscC_in_gg(X1, X2))
geqcE_in_gg(X1, X1) → geqcE_out_gg(X1, X1)
geqcE_in_gg(s(X1), 0) → geqcE_out_gg(s(X1), 0)
geqcE_in_gg(s(X1), s(X2)) → U45_gg(X1, X2, geqcE_in_gg(X1, X2))
U40_gg(X1, X2, lesscC_out_gg(X1, X2)) → lesscC_out_gg(s(X1), s(X2))
U45_gg(X1, X2, geqcE_out_gg(X1, X2)) → geqcE_out_gg(s(X1), s(X2))
lesscC_in_gg(x0, x1)
geqcE_in_gg(x0, x1)
U40_gg(x0, x1, x2)
U45_gg(x0, x1, x2)
From the DPs we obtained the following set of size-change graphs:
QSH_IN_GA(cons(X1, X2), X3) → U11_GA(X1, X2, X3, splitcD_in_ggaa(X2, X1, X4, X5))
U11_GA(X1, X2, X3, splitcD_out_ggaa(X2, X1, X4, X5)) → QSH_IN_GA(X4, X6)
U11_GA(X1, X2, X3, splitcD_out_ggaa(X2, X1, X4, X5)) → U13_GA(X1, X2, X3, X5, qscH_in_ga(X4, X6))
U13_GA(X1, X2, X3, X5, qscH_out_ga(X4, X6)) → QSH_IN_GA(X5, X7)
qscA_in_a([]) → qscA_out_a([])
lesscC_in_gg(0, s(X1)) → lesscC_out_gg(0, s(X1))
lesscC_in_gg(s(X1), s(X2)) → U40_gg(X1, X2, lesscC_in_gg(X1, X2))
U40_gg(X1, X2, lesscC_out_gg(X1, X2)) → lesscC_out_gg(s(X1), s(X2))
geqcE_in_gg(X1, X1) → geqcE_out_gg(X1, X1)
geqcE_in_gg(s(X1), 0) → geqcE_out_gg(s(X1), 0)
geqcE_in_gg(s(X1), s(X2)) → U45_gg(X1, X2, geqcE_in_gg(X1, X2))
U45_gg(X1, X2, geqcE_out_gg(X1, X2)) → geqcE_out_gg(s(X1), s(X2))
splitcD_in_ggaa([], X1, [], []) → splitcD_out_ggaa([], X1, [], [])
splitcD_in_ggaa(cons(X1, X2), X3, cons(X1, X4), X5) → U41_ggaa(X1, X2, X3, X4, X5, lesscC_in_gg(X1, X3))
U41_ggaa(X1, X2, X3, X4, X5, lesscC_out_gg(X1, X3)) → U42_ggaa(X1, X2, X3, X4, X5, splitcD_in_ggaa(X2, X3, X4, X5))
splitcD_in_ggaa(cons(X1, X2), X3, X4, cons(X1, X5)) → U43_ggaa(X1, X2, X3, X4, X5, geqcE_in_gg(X1, X3))
U43_ggaa(X1, X2, X3, X4, X5, geqcE_out_gg(X1, X3)) → U44_ggaa(X1, X2, X3, X4, X5, splitcD_in_ggaa(X2, X3, X4, X5))
U44_ggaa(X1, X2, X3, X4, X5, splitcD_out_ggaa(X2, X3, X4, X5)) → splitcD_out_ggaa(cons(X1, X2), X3, X4, cons(X1, X5))
U42_ggaa(X1, X2, X3, X4, X5, splitcD_out_ggaa(X2, X3, X4, X5)) → splitcD_out_ggaa(cons(X1, X2), X3, cons(X1, X4), X5)
qscH_in_ga([], []) → qscH_out_ga([], [])
qscH_in_ga(cons(X1, X2), X3) → U57_ga(X1, X2, X3, splitcD_in_ggaa(X2, X1, X4, X5))
U57_ga(X1, X2, X3, splitcD_out_ggaa(X2, X1, X4, X5)) → U58_ga(X1, X2, X3, X5, qscH_in_ga(X4, X6))
U58_ga(X1, X2, X3, X5, qscH_out_ga(X4, X6)) → U59_ga(X1, X2, X3, X6, qscH_in_ga(X5, X7))
U59_ga(X1, X2, X3, X6, qscH_out_ga(X5, X7)) → U60_ga(X1, X2, X3, appendcI_in_ggga(X6, X1, X7, X3))
appendcI_in_ggga([], X1, X2, cons(X1, X2)) → appendcI_out_ggga([], X1, X2, cons(X1, X2))
appendcI_in_ggga(cons(X1, X2), X3, X4, cons(X1, X5)) → U61_ggga(X1, X2, X3, X4, X5, appendcI_in_ggga(X2, X3, X4, X5))
U61_ggga(X1, X2, X3, X4, X5, appendcI_out_ggga(X2, X3, X4, X5)) → appendcI_out_ggga(cons(X1, X2), X3, X4, cons(X1, X5))
U60_ga(X1, X2, X3, appendcI_out_ggga(X6, X1, X7, X3)) → qscH_out_ga(cons(X1, X2), X3)
qscF_in_ga([], []) → qscF_out_ga([], [])
qscF_in_ga(cons(X1, []), X2) → U46_ga(X1, X2, qscA_in_a(X3))
U46_ga(X1, X2, qscA_out_a(X3)) → U47_ga(X1, X2, X3, qscA_in_a(X4))
U47_ga(X1, X2, X3, qscA_out_a(X4)) → U48_ga(X1, X2, appendcB_in_ggga(X3, X1, X4, X2))
appendcB_in_ggga([], X1, X2, cons(X1, X2)) → appendcB_out_ggga([], X1, X2, cons(X1, X2))
appendcB_in_ggga(cons(X1, X2), X3, X4, cons(X1, X5)) → U39_ggga(X1, X2, X3, X4, X5, appendcB_in_ggga(X2, X3, X4, X5))
U39_ggga(X1, X2, X3, X4, X5, appendcB_out_ggga(X2, X3, X4, X5)) → appendcB_out_ggga(cons(X1, X2), X3, X4, cons(X1, X5))
U48_ga(X1, X2, appendcB_out_ggga(X3, X1, X4, X2)) → qscF_out_ga(cons(X1, []), X2)
qscF_in_ga(cons(X1, cons(X2, X3)), X4) → U49_ga(X1, X2, X3, X4, lesscC_in_gg(X2, X1))
U49_ga(X1, X2, X3, X4, lesscC_out_gg(X2, X1)) → U50_ga(X1, X2, X3, X4, splitcD_in_ggaa(X3, X1, X5, X6))
U50_ga(X1, X2, X3, X4, splitcD_out_ggaa(X3, X1, X5, X6)) → U51_ga(X1, X2, X3, X4, X6, qscF_in_ga(cons(X2, X5), X7))
qscF_in_ga(cons(X1, cons(X2, X3)), X4) → U53_ga(X1, X2, X3, X4, geqcE_in_gg(X2, X1))
U53_ga(X1, X2, X3, X4, geqcE_out_gg(X2, X1)) → U54_ga(X1, X2, X3, X4, splitcD_in_ggaa(X3, X1, X5, X6))
U54_ga(X1, X2, X3, X4, splitcD_out_ggaa(X3, X1, X5, X6)) → U55_ga(X1, X2, X3, X4, X6, qscH_in_ga(X5, X7))
U55_ga(X1, X2, X3, X4, X6, qscH_out_ga(X5, X7)) → U56_ga(X1, X2, X3, X4, qcG_in_gagga(cons(X2, X6), X8, X7, X1, X4))
qcG_in_gagga(X1, X2, X3, X4, X5) → U62_gagga(X1, X2, X3, X4, X5, qscH_in_ga(X1, X2))
U62_gagga(X1, X2, X3, X4, X5, qscH_out_ga(X1, X2)) → U63_gagga(X1, X2, X3, X4, X5, appendcB_in_ggga(X3, X4, X2, X5))
U63_gagga(X1, X2, X3, X4, X5, appendcB_out_ggga(X3, X4, X2, X5)) → qcG_out_gagga(X1, X2, X3, X4, X5)
U56_ga(X1, X2, X3, X4, qcG_out_gagga(cons(X2, X6), X8, X7, X1, X4)) → qscF_out_ga(cons(X1, cons(X2, X3)), X4)
U51_ga(X1, X2, X3, X4, X6, qscF_out_ga(cons(X2, X5), X7)) → U52_ga(X1, X2, X3, X4, qcG_in_gagga(X6, X8, X7, X1, X4))
U52_ga(X1, X2, X3, X4, qcG_out_gagga(X6, X8, X7, X1, X4)) → qscF_out_ga(cons(X1, cons(X2, X3)), X4)
QSH_IN_GA(cons(X1, X2), X3) → U11_GA(X1, X2, X3, splitcD_in_ggaa(X2, X1, X4, X5))
U11_GA(X1, X2, X3, splitcD_out_ggaa(X2, X1, X4, X5)) → QSH_IN_GA(X4, X6)
U11_GA(X1, X2, X3, splitcD_out_ggaa(X2, X1, X4, X5)) → U13_GA(X1, X2, X3, X5, qscH_in_ga(X4, X6))
U13_GA(X1, X2, X3, X5, qscH_out_ga(X4, X6)) → QSH_IN_GA(X5, X7)
splitcD_in_ggaa([], X1, [], []) → splitcD_out_ggaa([], X1, [], [])
splitcD_in_ggaa(cons(X1, X2), X3, cons(X1, X4), X5) → U41_ggaa(X1, X2, X3, X4, X5, lesscC_in_gg(X1, X3))
splitcD_in_ggaa(cons(X1, X2), X3, X4, cons(X1, X5)) → U43_ggaa(X1, X2, X3, X4, X5, geqcE_in_gg(X1, X3))
qscH_in_ga([], []) → qscH_out_ga([], [])
qscH_in_ga(cons(X1, X2), X3) → U57_ga(X1, X2, X3, splitcD_in_ggaa(X2, X1, X4, X5))
U41_ggaa(X1, X2, X3, X4, X5, lesscC_out_gg(X1, X3)) → U42_ggaa(X1, X2, X3, X4, X5, splitcD_in_ggaa(X2, X3, X4, X5))
U43_ggaa(X1, X2, X3, X4, X5, geqcE_out_gg(X1, X3)) → U44_ggaa(X1, X2, X3, X4, X5, splitcD_in_ggaa(X2, X3, X4, X5))
U57_ga(X1, X2, X3, splitcD_out_ggaa(X2, X1, X4, X5)) → U58_ga(X1, X2, X3, X5, qscH_in_ga(X4, X6))
lesscC_in_gg(0, s(X1)) → lesscC_out_gg(0, s(X1))
lesscC_in_gg(s(X1), s(X2)) → U40_gg(X1, X2, lesscC_in_gg(X1, X2))
U42_ggaa(X1, X2, X3, X4, X5, splitcD_out_ggaa(X2, X3, X4, X5)) → splitcD_out_ggaa(cons(X1, X2), X3, cons(X1, X4), X5)
geqcE_in_gg(X1, X1) → geqcE_out_gg(X1, X1)
geqcE_in_gg(s(X1), 0) → geqcE_out_gg(s(X1), 0)
geqcE_in_gg(s(X1), s(X2)) → U45_gg(X1, X2, geqcE_in_gg(X1, X2))
U44_ggaa(X1, X2, X3, X4, X5, splitcD_out_ggaa(X2, X3, X4, X5)) → splitcD_out_ggaa(cons(X1, X2), X3, X4, cons(X1, X5))
U58_ga(X1, X2, X3, X5, qscH_out_ga(X4, X6)) → U59_ga(X1, X2, X3, X6, qscH_in_ga(X5, X7))
U40_gg(X1, X2, lesscC_out_gg(X1, X2)) → lesscC_out_gg(s(X1), s(X2))
U45_gg(X1, X2, geqcE_out_gg(X1, X2)) → geqcE_out_gg(s(X1), s(X2))
U59_ga(X1, X2, X3, X6, qscH_out_ga(X5, X7)) → U60_ga(X1, X2, X3, appendcI_in_ggga(X6, X1, X7, X3))
U60_ga(X1, X2, X3, appendcI_out_ggga(X6, X1, X7, X3)) → qscH_out_ga(cons(X1, X2), X3)
appendcI_in_ggga([], X1, X2, cons(X1, X2)) → appendcI_out_ggga([], X1, X2, cons(X1, X2))
appendcI_in_ggga(cons(X1, X2), X3, X4, cons(X1, X5)) → U61_ggga(X1, X2, X3, X4, X5, appendcI_in_ggga(X2, X3, X4, X5))
U61_ggga(X1, X2, X3, X4, X5, appendcI_out_ggga(X2, X3, X4, X5)) → appendcI_out_ggga(cons(X1, X2), X3, X4, cons(X1, X5))
QSH_IN_GA(cons(X1, X2)) → U11_GA(X1, X2, splitcD_in_ggaa(X2, X1))
U11_GA(X1, X2, splitcD_out_ggaa(X2, X1, X4, X5)) → QSH_IN_GA(X4)
U11_GA(X1, X2, splitcD_out_ggaa(X2, X1, X4, X5)) → U13_GA(X1, X2, X5, qscH_in_ga(X4))
U13_GA(X1, X2, X5, qscH_out_ga(X4, X6)) → QSH_IN_GA(X5)
splitcD_in_ggaa([], X1) → splitcD_out_ggaa([], X1, [], [])
splitcD_in_ggaa(cons(X1, X2), X3) → U41_ggaa(X1, X2, X3, lesscC_in_gg(X1, X3))
splitcD_in_ggaa(cons(X1, X2), X3) → U43_ggaa(X1, X2, X3, geqcE_in_gg(X1, X3))
qscH_in_ga([]) → qscH_out_ga([], [])
qscH_in_ga(cons(X1, X2)) → U57_ga(X1, X2, splitcD_in_ggaa(X2, X1))
U41_ggaa(X1, X2, X3, lesscC_out_gg(X1, X3)) → U42_ggaa(X1, X2, X3, splitcD_in_ggaa(X2, X3))
U43_ggaa(X1, X2, X3, geqcE_out_gg(X1, X3)) → U44_ggaa(X1, X2, X3, splitcD_in_ggaa(X2, X3))
U57_ga(X1, X2, splitcD_out_ggaa(X2, X1, X4, X5)) → U58_ga(X1, X2, X5, qscH_in_ga(X4))
lesscC_in_gg(0, s(X1)) → lesscC_out_gg(0, s(X1))
lesscC_in_gg(s(X1), s(X2)) → U40_gg(X1, X2, lesscC_in_gg(X1, X2))
U42_ggaa(X1, X2, X3, splitcD_out_ggaa(X2, X3, X4, X5)) → splitcD_out_ggaa(cons(X1, X2), X3, cons(X1, X4), X5)
geqcE_in_gg(X1, X1) → geqcE_out_gg(X1, X1)
geqcE_in_gg(s(X1), 0) → geqcE_out_gg(s(X1), 0)
geqcE_in_gg(s(X1), s(X2)) → U45_gg(X1, X2, geqcE_in_gg(X1, X2))
U44_ggaa(X1, X2, X3, splitcD_out_ggaa(X2, X3, X4, X5)) → splitcD_out_ggaa(cons(X1, X2), X3, X4, cons(X1, X5))
U58_ga(X1, X2, X5, qscH_out_ga(X4, X6)) → U59_ga(X1, X2, X6, qscH_in_ga(X5))
U40_gg(X1, X2, lesscC_out_gg(X1, X2)) → lesscC_out_gg(s(X1), s(X2))
U45_gg(X1, X2, geqcE_out_gg(X1, X2)) → geqcE_out_gg(s(X1), s(X2))
U59_ga(X1, X2, X6, qscH_out_ga(X5, X7)) → U60_ga(X1, X2, appendcI_in_ggga(X6, X1, X7))
U60_ga(X1, X2, appendcI_out_ggga(X6, X1, X7, X3)) → qscH_out_ga(cons(X1, X2), X3)
appendcI_in_ggga([], X1, X2) → appendcI_out_ggga([], X1, X2, cons(X1, X2))
appendcI_in_ggga(cons(X1, X2), X3, X4) → U61_ggga(X1, X2, X3, X4, appendcI_in_ggga(X2, X3, X4))
U61_ggga(X1, X2, X3, X4, appendcI_out_ggga(X2, X3, X4, X5)) → appendcI_out_ggga(cons(X1, X2), X3, X4, cons(X1, X5))
splitcD_in_ggaa(x0, x1)
qscH_in_ga(x0)
U41_ggaa(x0, x1, x2, x3)
U43_ggaa(x0, x1, x2, x3)
U57_ga(x0, x1, x2)
lesscC_in_gg(x0, x1)
U42_ggaa(x0, x1, x2, x3)
geqcE_in_gg(x0, x1)
U44_ggaa(x0, x1, x2, x3)
U58_ga(x0, x1, x2, x3)
U40_gg(x0, x1, x2)
U45_gg(x0, x1, x2)
U59_ga(x0, x1, x2, x3)
U60_ga(x0, x1, x2)
appendcI_in_ggga(x0, x1, x2)
U61_ggga(x0, x1, x2, x3, x4)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
QSH_IN_GA(cons(X1, X2)) → U11_GA(X1, X2, splitcD_in_ggaa(X2, X1))
POL(0) = 0
POL(QSH_IN_GA(x1)) = 1 + x1
POL(U11_GA(x1, x2, x3)) = 1 + x3
POL(U13_GA(x1, x2, x3, x4)) = 1 + x3
POL(U40_gg(x1, x2, x3)) = x2
POL(U41_ggaa(x1, x2, x3, x4)) = 1 + x2
POL(U42_ggaa(x1, x2, x3, x4)) = 1 + x4
POL(U43_ggaa(x1, x2, x3, x4)) = 1 + x2
POL(U44_ggaa(x1, x2, x3, x4)) = 1 + x4
POL(U45_gg(x1, x2, x3)) = 0
POL(U57_ga(x1, x2, x3)) = 0
POL(U58_ga(x1, x2, x3, x4)) = 0
POL(U59_ga(x1, x2, x3, x4)) = 0
POL(U60_ga(x1, x2, x3)) = 0
POL(U61_ggga(x1, x2, x3, x4, x5)) = 0
POL([]) = 0
POL(appendcI_in_ggga(x1, x2, x3)) = 0
POL(appendcI_out_ggga(x1, x2, x3, x4)) = 0
POL(cons(x1, x2)) = 1 + x2
POL(geqcE_in_gg(x1, x2)) = 0
POL(geqcE_out_gg(x1, x2)) = 0
POL(lesscC_in_gg(x1, x2)) = x2
POL(lesscC_out_gg(x1, x2)) = 0
POL(qscH_in_ga(x1)) = 0
POL(qscH_out_ga(x1, x2)) = 0
POL(s(x1)) = 1 + x1
POL(splitcD_in_ggaa(x1, x2)) = x1
POL(splitcD_out_ggaa(x1, x2, x3, x4)) = x3 + x4
splitcD_in_ggaa([], X1) → splitcD_out_ggaa([], X1, [], [])
splitcD_in_ggaa(cons(X1, X2), X3) → U41_ggaa(X1, X2, X3, lesscC_in_gg(X1, X3))
splitcD_in_ggaa(cons(X1, X2), X3) → U43_ggaa(X1, X2, X3, geqcE_in_gg(X1, X3))
U41_ggaa(X1, X2, X3, lesscC_out_gg(X1, X3)) → U42_ggaa(X1, X2, X3, splitcD_in_ggaa(X2, X3))
U42_ggaa(X1, X2, X3, splitcD_out_ggaa(X2, X3, X4, X5)) → splitcD_out_ggaa(cons(X1, X2), X3, cons(X1, X4), X5)
U43_ggaa(X1, X2, X3, geqcE_out_gg(X1, X3)) → U44_ggaa(X1, X2, X3, splitcD_in_ggaa(X2, X3))
U44_ggaa(X1, X2, X3, splitcD_out_ggaa(X2, X3, X4, X5)) → splitcD_out_ggaa(cons(X1, X2), X3, X4, cons(X1, X5))
U11_GA(X1, X2, splitcD_out_ggaa(X2, X1, X4, X5)) → QSH_IN_GA(X4)
U11_GA(X1, X2, splitcD_out_ggaa(X2, X1, X4, X5)) → U13_GA(X1, X2, X5, qscH_in_ga(X4))
U13_GA(X1, X2, X5, qscH_out_ga(X4, X6)) → QSH_IN_GA(X5)
splitcD_in_ggaa([], X1) → splitcD_out_ggaa([], X1, [], [])
splitcD_in_ggaa(cons(X1, X2), X3) → U41_ggaa(X1, X2, X3, lesscC_in_gg(X1, X3))
splitcD_in_ggaa(cons(X1, X2), X3) → U43_ggaa(X1, X2, X3, geqcE_in_gg(X1, X3))
qscH_in_ga([]) → qscH_out_ga([], [])
qscH_in_ga(cons(X1, X2)) → U57_ga(X1, X2, splitcD_in_ggaa(X2, X1))
U41_ggaa(X1, X2, X3, lesscC_out_gg(X1, X3)) → U42_ggaa(X1, X2, X3, splitcD_in_ggaa(X2, X3))
U43_ggaa(X1, X2, X3, geqcE_out_gg(X1, X3)) → U44_ggaa(X1, X2, X3, splitcD_in_ggaa(X2, X3))
U57_ga(X1, X2, splitcD_out_ggaa(X2, X1, X4, X5)) → U58_ga(X1, X2, X5, qscH_in_ga(X4))
lesscC_in_gg(0, s(X1)) → lesscC_out_gg(0, s(X1))
lesscC_in_gg(s(X1), s(X2)) → U40_gg(X1, X2, lesscC_in_gg(X1, X2))
U42_ggaa(X1, X2, X3, splitcD_out_ggaa(X2, X3, X4, X5)) → splitcD_out_ggaa(cons(X1, X2), X3, cons(X1, X4), X5)
geqcE_in_gg(X1, X1) → geqcE_out_gg(X1, X1)
geqcE_in_gg(s(X1), 0) → geqcE_out_gg(s(X1), 0)
geqcE_in_gg(s(X1), s(X2)) → U45_gg(X1, X2, geqcE_in_gg(X1, X2))
U44_ggaa(X1, X2, X3, splitcD_out_ggaa(X2, X3, X4, X5)) → splitcD_out_ggaa(cons(X1, X2), X3, X4, cons(X1, X5))
U58_ga(X1, X2, X5, qscH_out_ga(X4, X6)) → U59_ga(X1, X2, X6, qscH_in_ga(X5))
U40_gg(X1, X2, lesscC_out_gg(X1, X2)) → lesscC_out_gg(s(X1), s(X2))
U45_gg(X1, X2, geqcE_out_gg(X1, X2)) → geqcE_out_gg(s(X1), s(X2))
U59_ga(X1, X2, X6, qscH_out_ga(X5, X7)) → U60_ga(X1, X2, appendcI_in_ggga(X6, X1, X7))
U60_ga(X1, X2, appendcI_out_ggga(X6, X1, X7, X3)) → qscH_out_ga(cons(X1, X2), X3)
appendcI_in_ggga([], X1, X2) → appendcI_out_ggga([], X1, X2, cons(X1, X2))
appendcI_in_ggga(cons(X1, X2), X3, X4) → U61_ggga(X1, X2, X3, X4, appendcI_in_ggga(X2, X3, X4))
U61_ggga(X1, X2, X3, X4, appendcI_out_ggga(X2, X3, X4, X5)) → appendcI_out_ggga(cons(X1, X2), X3, X4, cons(X1, X5))
splitcD_in_ggaa(x0, x1)
qscH_in_ga(x0)
U41_ggaa(x0, x1, x2, x3)
U43_ggaa(x0, x1, x2, x3)
U57_ga(x0, x1, x2)
lesscC_in_gg(x0, x1)
U42_ggaa(x0, x1, x2, x3)
geqcE_in_gg(x0, x1)
U44_ggaa(x0, x1, x2, x3)
U58_ga(x0, x1, x2, x3)
U40_gg(x0, x1, x2)
U45_gg(x0, x1, x2)
U59_ga(x0, x1, x2, x3)
U60_ga(x0, x1, x2)
appendcI_in_ggga(x0, x1, x2)
U61_ggga(x0, x1, x2, x3, x4)
APPENDB_IN_GGGA(cons(X1, X2), X3, X4, cons(X1, X5)) → APPENDB_IN_GGGA(X2, X3, X4, X5)
qscA_in_a([]) → qscA_out_a([])
lesscC_in_gg(0, s(X1)) → lesscC_out_gg(0, s(X1))
lesscC_in_gg(s(X1), s(X2)) → U40_gg(X1, X2, lesscC_in_gg(X1, X2))
U40_gg(X1, X2, lesscC_out_gg(X1, X2)) → lesscC_out_gg(s(X1), s(X2))
geqcE_in_gg(X1, X1) → geqcE_out_gg(X1, X1)
geqcE_in_gg(s(X1), 0) → geqcE_out_gg(s(X1), 0)
geqcE_in_gg(s(X1), s(X2)) → U45_gg(X1, X2, geqcE_in_gg(X1, X2))
U45_gg(X1, X2, geqcE_out_gg(X1, X2)) → geqcE_out_gg(s(X1), s(X2))
splitcD_in_ggaa([], X1, [], []) → splitcD_out_ggaa([], X1, [], [])
splitcD_in_ggaa(cons(X1, X2), X3, cons(X1, X4), X5) → U41_ggaa(X1, X2, X3, X4, X5, lesscC_in_gg(X1, X3))
U41_ggaa(X1, X2, X3, X4, X5, lesscC_out_gg(X1, X3)) → U42_ggaa(X1, X2, X3, X4, X5, splitcD_in_ggaa(X2, X3, X4, X5))
splitcD_in_ggaa(cons(X1, X2), X3, X4, cons(X1, X5)) → U43_ggaa(X1, X2, X3, X4, X5, geqcE_in_gg(X1, X3))
U43_ggaa(X1, X2, X3, X4, X5, geqcE_out_gg(X1, X3)) → U44_ggaa(X1, X2, X3, X4, X5, splitcD_in_ggaa(X2, X3, X4, X5))
U44_ggaa(X1, X2, X3, X4, X5, splitcD_out_ggaa(X2, X3, X4, X5)) → splitcD_out_ggaa(cons(X1, X2), X3, X4, cons(X1, X5))
U42_ggaa(X1, X2, X3, X4, X5, splitcD_out_ggaa(X2, X3, X4, X5)) → splitcD_out_ggaa(cons(X1, X2), X3, cons(X1, X4), X5)
qscH_in_ga([], []) → qscH_out_ga([], [])
qscH_in_ga(cons(X1, X2), X3) → U57_ga(X1, X2, X3, splitcD_in_ggaa(X2, X1, X4, X5))
U57_ga(X1, X2, X3, splitcD_out_ggaa(X2, X1, X4, X5)) → U58_ga(X1, X2, X3, X5, qscH_in_ga(X4, X6))
U58_ga(X1, X2, X3, X5, qscH_out_ga(X4, X6)) → U59_ga(X1, X2, X3, X6, qscH_in_ga(X5, X7))
U59_ga(X1, X2, X3, X6, qscH_out_ga(X5, X7)) → U60_ga(X1, X2, X3, appendcI_in_ggga(X6, X1, X7, X3))
appendcI_in_ggga([], X1, X2, cons(X1, X2)) → appendcI_out_ggga([], X1, X2, cons(X1, X2))
appendcI_in_ggga(cons(X1, X2), X3, X4, cons(X1, X5)) → U61_ggga(X1, X2, X3, X4, X5, appendcI_in_ggga(X2, X3, X4, X5))
U61_ggga(X1, X2, X3, X4, X5, appendcI_out_ggga(X2, X3, X4, X5)) → appendcI_out_ggga(cons(X1, X2), X3, X4, cons(X1, X5))
U60_ga(X1, X2, X3, appendcI_out_ggga(X6, X1, X7, X3)) → qscH_out_ga(cons(X1, X2), X3)
qscF_in_ga([], []) → qscF_out_ga([], [])
qscF_in_ga(cons(X1, []), X2) → U46_ga(X1, X2, qscA_in_a(X3))
U46_ga(X1, X2, qscA_out_a(X3)) → U47_ga(X1, X2, X3, qscA_in_a(X4))
U47_ga(X1, X2, X3, qscA_out_a(X4)) → U48_ga(X1, X2, appendcB_in_ggga(X3, X1, X4, X2))
appendcB_in_ggga([], X1, X2, cons(X1, X2)) → appendcB_out_ggga([], X1, X2, cons(X1, X2))
appendcB_in_ggga(cons(X1, X2), X3, X4, cons(X1, X5)) → U39_ggga(X1, X2, X3, X4, X5, appendcB_in_ggga(X2, X3, X4, X5))
U39_ggga(X1, X2, X3, X4, X5, appendcB_out_ggga(X2, X3, X4, X5)) → appendcB_out_ggga(cons(X1, X2), X3, X4, cons(X1, X5))
U48_ga(X1, X2, appendcB_out_ggga(X3, X1, X4, X2)) → qscF_out_ga(cons(X1, []), X2)
qscF_in_ga(cons(X1, cons(X2, X3)), X4) → U49_ga(X1, X2, X3, X4, lesscC_in_gg(X2, X1))
U49_ga(X1, X2, X3, X4, lesscC_out_gg(X2, X1)) → U50_ga(X1, X2, X3, X4, splitcD_in_ggaa(X3, X1, X5, X6))
U50_ga(X1, X2, X3, X4, splitcD_out_ggaa(X3, X1, X5, X6)) → U51_ga(X1, X2, X3, X4, X6, qscF_in_ga(cons(X2, X5), X7))
qscF_in_ga(cons(X1, cons(X2, X3)), X4) → U53_ga(X1, X2, X3, X4, geqcE_in_gg(X2, X1))
U53_ga(X1, X2, X3, X4, geqcE_out_gg(X2, X1)) → U54_ga(X1, X2, X3, X4, splitcD_in_ggaa(X3, X1, X5, X6))
U54_ga(X1, X2, X3, X4, splitcD_out_ggaa(X3, X1, X5, X6)) → U55_ga(X1, X2, X3, X4, X6, qscH_in_ga(X5, X7))
U55_ga(X1, X2, X3, X4, X6, qscH_out_ga(X5, X7)) → U56_ga(X1, X2, X3, X4, qcG_in_gagga(cons(X2, X6), X8, X7, X1, X4))
qcG_in_gagga(X1, X2, X3, X4, X5) → U62_gagga(X1, X2, X3, X4, X5, qscH_in_ga(X1, X2))
U62_gagga(X1, X2, X3, X4, X5, qscH_out_ga(X1, X2)) → U63_gagga(X1, X2, X3, X4, X5, appendcB_in_ggga(X3, X4, X2, X5))
U63_gagga(X1, X2, X3, X4, X5, appendcB_out_ggga(X3, X4, X2, X5)) → qcG_out_gagga(X1, X2, X3, X4, X5)
U56_ga(X1, X2, X3, X4, qcG_out_gagga(cons(X2, X6), X8, X7, X1, X4)) → qscF_out_ga(cons(X1, cons(X2, X3)), X4)
U51_ga(X1, X2, X3, X4, X6, qscF_out_ga(cons(X2, X5), X7)) → U52_ga(X1, X2, X3, X4, qcG_in_gagga(X6, X8, X7, X1, X4))
U52_ga(X1, X2, X3, X4, qcG_out_gagga(X6, X8, X7, X1, X4)) → qscF_out_ga(cons(X1, cons(X2, X3)), X4)
APPENDB_IN_GGGA(cons(X1, X2), X3, X4, cons(X1, X5)) → APPENDB_IN_GGGA(X2, X3, X4, X5)
APPENDB_IN_GGGA(cons(X1, X2), X3, X4) → APPENDB_IN_GGGA(X2, X3, X4)
From the DPs we obtained the following set of size-change graphs:
QSF_IN_GA(cons(X1, cons(X2, X3)), X4) → U25_GA(X1, X2, X3, X4, lesscC_in_gg(X2, X1))
U25_GA(X1, X2, X3, X4, lesscC_out_gg(X2, X1)) → U27_GA(X1, X2, X3, X4, splitcD_in_ggaa(X3, X1, X5, X6))
U27_GA(X1, X2, X3, X4, splitcD_out_ggaa(X3, X1, X5, X6)) → QSF_IN_GA(cons(X2, X5), X7)
qscA_in_a([]) → qscA_out_a([])
lesscC_in_gg(0, s(X1)) → lesscC_out_gg(0, s(X1))
lesscC_in_gg(s(X1), s(X2)) → U40_gg(X1, X2, lesscC_in_gg(X1, X2))
U40_gg(X1, X2, lesscC_out_gg(X1, X2)) → lesscC_out_gg(s(X1), s(X2))
geqcE_in_gg(X1, X1) → geqcE_out_gg(X1, X1)
geqcE_in_gg(s(X1), 0) → geqcE_out_gg(s(X1), 0)
geqcE_in_gg(s(X1), s(X2)) → U45_gg(X1, X2, geqcE_in_gg(X1, X2))
U45_gg(X1, X2, geqcE_out_gg(X1, X2)) → geqcE_out_gg(s(X1), s(X2))
splitcD_in_ggaa([], X1, [], []) → splitcD_out_ggaa([], X1, [], [])
splitcD_in_ggaa(cons(X1, X2), X3, cons(X1, X4), X5) → U41_ggaa(X1, X2, X3, X4, X5, lesscC_in_gg(X1, X3))
U41_ggaa(X1, X2, X3, X4, X5, lesscC_out_gg(X1, X3)) → U42_ggaa(X1, X2, X3, X4, X5, splitcD_in_ggaa(X2, X3, X4, X5))
splitcD_in_ggaa(cons(X1, X2), X3, X4, cons(X1, X5)) → U43_ggaa(X1, X2, X3, X4, X5, geqcE_in_gg(X1, X3))
U43_ggaa(X1, X2, X3, X4, X5, geqcE_out_gg(X1, X3)) → U44_ggaa(X1, X2, X3, X4, X5, splitcD_in_ggaa(X2, X3, X4, X5))
U44_ggaa(X1, X2, X3, X4, X5, splitcD_out_ggaa(X2, X3, X4, X5)) → splitcD_out_ggaa(cons(X1, X2), X3, X4, cons(X1, X5))
U42_ggaa(X1, X2, X3, X4, X5, splitcD_out_ggaa(X2, X3, X4, X5)) → splitcD_out_ggaa(cons(X1, X2), X3, cons(X1, X4), X5)
qscH_in_ga([], []) → qscH_out_ga([], [])
qscH_in_ga(cons(X1, X2), X3) → U57_ga(X1, X2, X3, splitcD_in_ggaa(X2, X1, X4, X5))
U57_ga(X1, X2, X3, splitcD_out_ggaa(X2, X1, X4, X5)) → U58_ga(X1, X2, X3, X5, qscH_in_ga(X4, X6))
U58_ga(X1, X2, X3, X5, qscH_out_ga(X4, X6)) → U59_ga(X1, X2, X3, X6, qscH_in_ga(X5, X7))
U59_ga(X1, X2, X3, X6, qscH_out_ga(X5, X7)) → U60_ga(X1, X2, X3, appendcI_in_ggga(X6, X1, X7, X3))
appendcI_in_ggga([], X1, X2, cons(X1, X2)) → appendcI_out_ggga([], X1, X2, cons(X1, X2))
appendcI_in_ggga(cons(X1, X2), X3, X4, cons(X1, X5)) → U61_ggga(X1, X2, X3, X4, X5, appendcI_in_ggga(X2, X3, X4, X5))
U61_ggga(X1, X2, X3, X4, X5, appendcI_out_ggga(X2, X3, X4, X5)) → appendcI_out_ggga(cons(X1, X2), X3, X4, cons(X1, X5))
U60_ga(X1, X2, X3, appendcI_out_ggga(X6, X1, X7, X3)) → qscH_out_ga(cons(X1, X2), X3)
qscF_in_ga([], []) → qscF_out_ga([], [])
qscF_in_ga(cons(X1, []), X2) → U46_ga(X1, X2, qscA_in_a(X3))
U46_ga(X1, X2, qscA_out_a(X3)) → U47_ga(X1, X2, X3, qscA_in_a(X4))
U47_ga(X1, X2, X3, qscA_out_a(X4)) → U48_ga(X1, X2, appendcB_in_ggga(X3, X1, X4, X2))
appendcB_in_ggga([], X1, X2, cons(X1, X2)) → appendcB_out_ggga([], X1, X2, cons(X1, X2))
appendcB_in_ggga(cons(X1, X2), X3, X4, cons(X1, X5)) → U39_ggga(X1, X2, X3, X4, X5, appendcB_in_ggga(X2, X3, X4, X5))
U39_ggga(X1, X2, X3, X4, X5, appendcB_out_ggga(X2, X3, X4, X5)) → appendcB_out_ggga(cons(X1, X2), X3, X4, cons(X1, X5))
U48_ga(X1, X2, appendcB_out_ggga(X3, X1, X4, X2)) → qscF_out_ga(cons(X1, []), X2)
qscF_in_ga(cons(X1, cons(X2, X3)), X4) → U49_ga(X1, X2, X3, X4, lesscC_in_gg(X2, X1))
U49_ga(X1, X2, X3, X4, lesscC_out_gg(X2, X1)) → U50_ga(X1, X2, X3, X4, splitcD_in_ggaa(X3, X1, X5, X6))
U50_ga(X1, X2, X3, X4, splitcD_out_ggaa(X3, X1, X5, X6)) → U51_ga(X1, X2, X3, X4, X6, qscF_in_ga(cons(X2, X5), X7))
qscF_in_ga(cons(X1, cons(X2, X3)), X4) → U53_ga(X1, X2, X3, X4, geqcE_in_gg(X2, X1))
U53_ga(X1, X2, X3, X4, geqcE_out_gg(X2, X1)) → U54_ga(X1, X2, X3, X4, splitcD_in_ggaa(X3, X1, X5, X6))
U54_ga(X1, X2, X3, X4, splitcD_out_ggaa(X3, X1, X5, X6)) → U55_ga(X1, X2, X3, X4, X6, qscH_in_ga(X5, X7))
U55_ga(X1, X2, X3, X4, X6, qscH_out_ga(X5, X7)) → U56_ga(X1, X2, X3, X4, qcG_in_gagga(cons(X2, X6), X8, X7, X1, X4))
qcG_in_gagga(X1, X2, X3, X4, X5) → U62_gagga(X1, X2, X3, X4, X5, qscH_in_ga(X1, X2))
U62_gagga(X1, X2, X3, X4, X5, qscH_out_ga(X1, X2)) → U63_gagga(X1, X2, X3, X4, X5, appendcB_in_ggga(X3, X4, X2, X5))
U63_gagga(X1, X2, X3, X4, X5, appendcB_out_ggga(X3, X4, X2, X5)) → qcG_out_gagga(X1, X2, X3, X4, X5)
U56_ga(X1, X2, X3, X4, qcG_out_gagga(cons(X2, X6), X8, X7, X1, X4)) → qscF_out_ga(cons(X1, cons(X2, X3)), X4)
U51_ga(X1, X2, X3, X4, X6, qscF_out_ga(cons(X2, X5), X7)) → U52_ga(X1, X2, X3, X4, qcG_in_gagga(X6, X8, X7, X1, X4))
U52_ga(X1, X2, X3, X4, qcG_out_gagga(X6, X8, X7, X1, X4)) → qscF_out_ga(cons(X1, cons(X2, X3)), X4)
QSF_IN_GA(cons(X1, cons(X2, X3)), X4) → U25_GA(X1, X2, X3, X4, lesscC_in_gg(X2, X1))
U25_GA(X1, X2, X3, X4, lesscC_out_gg(X2, X1)) → U27_GA(X1, X2, X3, X4, splitcD_in_ggaa(X3, X1, X5, X6))
U27_GA(X1, X2, X3, X4, splitcD_out_ggaa(X3, X1, X5, X6)) → QSF_IN_GA(cons(X2, X5), X7)
lesscC_in_gg(0, s(X1)) → lesscC_out_gg(0, s(X1))
lesscC_in_gg(s(X1), s(X2)) → U40_gg(X1, X2, lesscC_in_gg(X1, X2))
splitcD_in_ggaa([], X1, [], []) → splitcD_out_ggaa([], X1, [], [])
splitcD_in_ggaa(cons(X1, X2), X3, cons(X1, X4), X5) → U41_ggaa(X1, X2, X3, X4, X5, lesscC_in_gg(X1, X3))
splitcD_in_ggaa(cons(X1, X2), X3, X4, cons(X1, X5)) → U43_ggaa(X1, X2, X3, X4, X5, geqcE_in_gg(X1, X3))
U40_gg(X1, X2, lesscC_out_gg(X1, X2)) → lesscC_out_gg(s(X1), s(X2))
U41_ggaa(X1, X2, X3, X4, X5, lesscC_out_gg(X1, X3)) → U42_ggaa(X1, X2, X3, X4, X5, splitcD_in_ggaa(X2, X3, X4, X5))
U43_ggaa(X1, X2, X3, X4, X5, geqcE_out_gg(X1, X3)) → U44_ggaa(X1, X2, X3, X4, X5, splitcD_in_ggaa(X2, X3, X4, X5))
U42_ggaa(X1, X2, X3, X4, X5, splitcD_out_ggaa(X2, X3, X4, X5)) → splitcD_out_ggaa(cons(X1, X2), X3, cons(X1, X4), X5)
geqcE_in_gg(X1, X1) → geqcE_out_gg(X1, X1)
geqcE_in_gg(s(X1), 0) → geqcE_out_gg(s(X1), 0)
geqcE_in_gg(s(X1), s(X2)) → U45_gg(X1, X2, geqcE_in_gg(X1, X2))
U44_ggaa(X1, X2, X3, X4, X5, splitcD_out_ggaa(X2, X3, X4, X5)) → splitcD_out_ggaa(cons(X1, X2), X3, X4, cons(X1, X5))
U45_gg(X1, X2, geqcE_out_gg(X1, X2)) → geqcE_out_gg(s(X1), s(X2))
QSF_IN_GA(cons(X1, cons(X2, X3))) → U25_GA(X1, X2, X3, lesscC_in_gg(X2, X1))
U25_GA(X1, X2, X3, lesscC_out_gg(X2, X1)) → U27_GA(X1, X2, X3, splitcD_in_ggaa(X3, X1))
U27_GA(X1, X2, X3, splitcD_out_ggaa(X3, X1, X5, X6)) → QSF_IN_GA(cons(X2, X5))
lesscC_in_gg(0, s(X1)) → lesscC_out_gg(0, s(X1))
lesscC_in_gg(s(X1), s(X2)) → U40_gg(X1, X2, lesscC_in_gg(X1, X2))
splitcD_in_ggaa([], X1) → splitcD_out_ggaa([], X1, [], [])
splitcD_in_ggaa(cons(X1, X2), X3) → U41_ggaa(X1, X2, X3, lesscC_in_gg(X1, X3))
splitcD_in_ggaa(cons(X1, X2), X3) → U43_ggaa(X1, X2, X3, geqcE_in_gg(X1, X3))
U40_gg(X1, X2, lesscC_out_gg(X1, X2)) → lesscC_out_gg(s(X1), s(X2))
U41_ggaa(X1, X2, X3, lesscC_out_gg(X1, X3)) → U42_ggaa(X1, X2, X3, splitcD_in_ggaa(X2, X3))
U43_ggaa(X1, X2, X3, geqcE_out_gg(X1, X3)) → U44_ggaa(X1, X2, X3, splitcD_in_ggaa(X2, X3))
U42_ggaa(X1, X2, X3, splitcD_out_ggaa(X2, X3, X4, X5)) → splitcD_out_ggaa(cons(X1, X2), X3, cons(X1, X4), X5)
geqcE_in_gg(X1, X1) → geqcE_out_gg(X1, X1)
geqcE_in_gg(s(X1), 0) → geqcE_out_gg(s(X1), 0)
geqcE_in_gg(s(X1), s(X2)) → U45_gg(X1, X2, geqcE_in_gg(X1, X2))
U44_ggaa(X1, X2, X3, splitcD_out_ggaa(X2, X3, X4, X5)) → splitcD_out_ggaa(cons(X1, X2), X3, X4, cons(X1, X5))
U45_gg(X1, X2, geqcE_out_gg(X1, X2)) → geqcE_out_gg(s(X1), s(X2))
lesscC_in_gg(x0, x1)
splitcD_in_ggaa(x0, x1)
U40_gg(x0, x1, x2)
U41_ggaa(x0, x1, x2, x3)
U43_ggaa(x0, x1, x2, x3)
U42_ggaa(x0, x1, x2, x3)
geqcE_in_gg(x0, x1)
U44_ggaa(x0, x1, x2, x3)
U45_gg(x0, x1, x2)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
QSF_IN_GA(cons(X1, cons(X2, X3))) → U25_GA(X1, X2, X3, lesscC_in_gg(X2, X1))
POL(0) = 0
POL(QSF_IN_GA(x1)) = 1 + x1
POL(U25_GA(x1, x2, x3, x4)) = 1 + x1 + x3 + x4
POL(U27_GA(x1, x2, x3, x4)) = 1 + x2 + x4
POL(U40_gg(x1, x2, x3)) = 1
POL(U41_ggaa(x1, x2, x3, x4)) = 1 + x1 + x2 + x4
POL(U42_ggaa(x1, x2, x3, x4)) = 1 + x1 + x4
POL(U43_ggaa(x1, x2, x3, x4)) = 1 + x2 + x4
POL(U44_ggaa(x1, x2, x3, x4)) = x4
POL(U45_gg(x1, x2, x3)) = 1
POL([]) = 0
POL(cons(x1, x2)) = 1 + x1 + x2
POL(geqcE_in_gg(x1, x2)) = 1
POL(geqcE_out_gg(x1, x2)) = 1
POL(lesscC_in_gg(x1, x2)) = 1
POL(lesscC_out_gg(x1, x2)) = 1 + x1
POL(s(x1)) = 0
POL(splitcD_in_ggaa(x1, x2)) = 1 + x1
POL(splitcD_out_ggaa(x1, x2, x3, x4)) = 1 + x3
lesscC_in_gg(0, s(X1)) → lesscC_out_gg(0, s(X1))
lesscC_in_gg(s(X1), s(X2)) → U40_gg(X1, X2, lesscC_in_gg(X1, X2))
splitcD_in_ggaa([], X1) → splitcD_out_ggaa([], X1, [], [])
splitcD_in_ggaa(cons(X1, X2), X3) → U41_ggaa(X1, X2, X3, lesscC_in_gg(X1, X3))
splitcD_in_ggaa(cons(X1, X2), X3) → U43_ggaa(X1, X2, X3, geqcE_in_gg(X1, X3))
U41_ggaa(X1, X2, X3, lesscC_out_gg(X1, X3)) → U42_ggaa(X1, X2, X3, splitcD_in_ggaa(X2, X3))
U42_ggaa(X1, X2, X3, splitcD_out_ggaa(X2, X3, X4, X5)) → splitcD_out_ggaa(cons(X1, X2), X3, cons(X1, X4), X5)
geqcE_in_gg(X1, X1) → geqcE_out_gg(X1, X1)
geqcE_in_gg(s(X1), 0) → geqcE_out_gg(s(X1), 0)
geqcE_in_gg(s(X1), s(X2)) → U45_gg(X1, X2, geqcE_in_gg(X1, X2))
U43_ggaa(X1, X2, X3, geqcE_out_gg(X1, X3)) → U44_ggaa(X1, X2, X3, splitcD_in_ggaa(X2, X3))
U44_ggaa(X1, X2, X3, splitcD_out_ggaa(X2, X3, X4, X5)) → splitcD_out_ggaa(cons(X1, X2), X3, X4, cons(X1, X5))
U40_gg(X1, X2, lesscC_out_gg(X1, X2)) → lesscC_out_gg(s(X1), s(X2))
U45_gg(X1, X2, geqcE_out_gg(X1, X2)) → geqcE_out_gg(s(X1), s(X2))
U25_GA(X1, X2, X3, lesscC_out_gg(X2, X1)) → U27_GA(X1, X2, X3, splitcD_in_ggaa(X3, X1))
U27_GA(X1, X2, X3, splitcD_out_ggaa(X3, X1, X5, X6)) → QSF_IN_GA(cons(X2, X5))
lesscC_in_gg(0, s(X1)) → lesscC_out_gg(0, s(X1))
lesscC_in_gg(s(X1), s(X2)) → U40_gg(X1, X2, lesscC_in_gg(X1, X2))
splitcD_in_ggaa([], X1) → splitcD_out_ggaa([], X1, [], [])
splitcD_in_ggaa(cons(X1, X2), X3) → U41_ggaa(X1, X2, X3, lesscC_in_gg(X1, X3))
splitcD_in_ggaa(cons(X1, X2), X3) → U43_ggaa(X1, X2, X3, geqcE_in_gg(X1, X3))
U40_gg(X1, X2, lesscC_out_gg(X1, X2)) → lesscC_out_gg(s(X1), s(X2))
U41_ggaa(X1, X2, X3, lesscC_out_gg(X1, X3)) → U42_ggaa(X1, X2, X3, splitcD_in_ggaa(X2, X3))
U43_ggaa(X1, X2, X3, geqcE_out_gg(X1, X3)) → U44_ggaa(X1, X2, X3, splitcD_in_ggaa(X2, X3))
U42_ggaa(X1, X2, X3, splitcD_out_ggaa(X2, X3, X4, X5)) → splitcD_out_ggaa(cons(X1, X2), X3, cons(X1, X4), X5)
geqcE_in_gg(X1, X1) → geqcE_out_gg(X1, X1)
geqcE_in_gg(s(X1), 0) → geqcE_out_gg(s(X1), 0)
geqcE_in_gg(s(X1), s(X2)) → U45_gg(X1, X2, geqcE_in_gg(X1, X2))
U44_ggaa(X1, X2, X3, splitcD_out_ggaa(X2, X3, X4, X5)) → splitcD_out_ggaa(cons(X1, X2), X3, X4, cons(X1, X5))
U45_gg(X1, X2, geqcE_out_gg(X1, X2)) → geqcE_out_gg(s(X1), s(X2))
lesscC_in_gg(x0, x1)
splitcD_in_ggaa(x0, x1)
U40_gg(x0, x1, x2)
U41_ggaa(x0, x1, x2, x3)
U43_ggaa(x0, x1, x2, x3)
U42_ggaa(x0, x1, x2, x3)
geqcE_in_gg(x0, x1)
U44_ggaa(x0, x1, x2, x3)
U45_gg(x0, x1, x2)