0 Prolog
↳1 PrologToDTProblemTransformerProof (⇒, 285 ms)
↳2 TRIPLES
↳3 UndefinedPredicateInTriplesTransformerProof (⇒, 0 ms)
↳4 TRIPLES
↳5 TriplesToPiDPProof (⇒, 540 ms)
↳6 PiDP
↳7 DependencyGraphProof (⇔, 0 ms)
↳8 AND
↳9 PiDP
↳10 UsableRulesProof (⇔, 0 ms)
↳11 PiDP
↳12 PiDPToQDPProof (⇒, 0 ms)
↳13 QDP
↳14 QDPSizeChangeProof (⇔, 0 ms)
↳15 YES
↳16 PiDP
↳17 UsableRulesProof (⇔, 0 ms)
↳18 PiDP
↳19 PiDPToQDPProof (⇒, 0 ms)
↳20 QDP
↳21 QDPSizeChangeProof (⇔, 0 ms)
↳22 YES
↳23 PiDP
↳24 UsableRulesProof (⇔, 0 ms)
↳25 PiDP
↳26 PiDPToQDPProof (⇔, 0 ms)
↳27 QDP
↳28 QDPSizeChangeProof (⇔, 0 ms)
↳29 YES
↳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 QDPSizeChangeProof (⇔, 0 ms)
↳43 YES
↳44 PiDP
↳45 UsableRulesProof (⇔, 0 ms)
↳46 PiDP
↳47 PiDPToQDPProof (⇒, 0 ms)
↳48 QDP
↳49 QDPOrderProof (⇔, 225 ms)
↳50 QDP
↳51 DependencyGraphProof (⇔, 0 ms)
↳52 TRUE
↳53 PiDP
↳54 UsableRulesProof (⇔, 0 ms)
↳55 PiDP
↳56 PiDPToQDPProof (⇒, 0 ms)
↳57 QDP
↳58 QDPQMonotonicMRRProof (⇔, 292 ms)
↳59 QDP
↳60 DependencyGraphProof (⇔, 0 ms)
↳61 TRUE
QSD_IN_GA(.(X1, .(X2, X3)), X4) → U21_GA(X1, X2, X3, X4, gtA_in_gg(X1, X2))
QSD_IN_GA(.(X1, .(X2, X3)), X4) → GTA_IN_GG(X1, X2)
GTA_IN_GG(s(X1), s(X2)) → U1_GG(X1, X2, gtA_in_gg(X1, X2))
GTA_IN_GG(s(X1), s(X2)) → GTA_IN_GG(X1, X2)
QSD_IN_GA(.(X1, .(X2, X3)), X4) → U22_GA(X1, X2, X3, X4, gtcA_in_gg(X1, X2))
U22_GA(X1, X2, X3, X4, gtcA_out_gg(X1, X2)) → U23_GA(X1, X2, X3, X4, partB_in_ggaa(X1, X3, X5, X6))
U22_GA(X1, X2, X3, X4, gtcA_out_gg(X1, X2)) → PARTB_IN_GGAA(X1, X3, X5, X6)
PARTB_IN_GGAA(X1, .(X2, X3), .(X2, X4), X5) → U2_GGAA(X1, X2, X3, X4, X5, gtA_in_gg(X1, X2))
PARTB_IN_GGAA(X1, .(X2, X3), .(X2, X4), X5) → GTA_IN_GG(X1, X2)
PARTB_IN_GGAA(X1, .(X2, X3), .(X2, X4), X5) → U3_GGAA(X1, X2, X3, X4, X5, gtcA_in_gg(X1, X2))
U3_GGAA(X1, X2, X3, X4, X5, gtcA_out_gg(X1, X2)) → U4_GGAA(X1, X2, X3, X4, X5, partB_in_ggaa(X1, X3, X4, X5))
U3_GGAA(X1, X2, X3, X4, X5, gtcA_out_gg(X1, X2)) → PARTB_IN_GGAA(X1, X3, X4, X5)
PARTB_IN_GGAA(X1, .(X2, X3), X4, .(X2, X5)) → U5_GGAA(X1, X2, X3, X4, X5, leC_in_gg(X1, X2))
PARTB_IN_GGAA(X1, .(X2, X3), X4, .(X2, X5)) → LEC_IN_GG(X1, X2)
LEC_IN_GG(s(X1), s(X2)) → U8_GG(X1, X2, leC_in_gg(X1, X2))
LEC_IN_GG(s(X1), s(X2)) → LEC_IN_GG(X1, X2)
PARTB_IN_GGAA(X1, .(X2, X3), X4, .(X2, X5)) → U6_GGAA(X1, X2, X3, X4, X5, lecC_in_gg(X1, X2))
U6_GGAA(X1, X2, X3, X4, X5, lecC_out_gg(X1, X2)) → U7_GGAA(X1, X2, X3, X4, X5, partB_in_ggaa(X1, X3, X4, X5))
U6_GGAA(X1, X2, X3, X4, X5, lecC_out_gg(X1, X2)) → PARTB_IN_GGAA(X1, X3, X4, X5)
U22_GA(X1, X2, X3, X4, gtcA_out_gg(X1, X2)) → U24_GA(X1, X2, X3, X4, partcB_in_ggaa(X1, X3, X5, X6))
U24_GA(X1, X2, X3, X4, partcB_out_ggaa(X1, X3, X5, X6)) → U25_GA(X1, X2, X3, X4, qsD_in_ga(.(X2, X5), X7))
U24_GA(X1, X2, X3, X4, partcB_out_ggaa(X1, X3, X5, X6)) → QSD_IN_GA(.(X2, X5), X7)
QSD_IN_GA(.(X1, .(X2, X3)), X4) → U28_GA(X1, X2, X3, X4, leC_in_gg(X1, X2))
QSD_IN_GA(.(X1, .(X2, X3)), X4) → LEC_IN_GG(X1, X2)
QSD_IN_GA(.(X1, .(X2, X3)), X4) → U29_GA(X1, X2, X3, X4, lecC_in_gg(X1, X2))
U29_GA(X1, X2, X3, X4, lecC_out_gg(X1, X2)) → U30_GA(X1, X2, X3, X4, partB_in_ggaa(X1, X3, X5, X6))
U29_GA(X1, X2, X3, X4, lecC_out_gg(X1, X2)) → PARTB_IN_GGAA(X1, X3, X5, X6)
U29_GA(X1, X2, X3, X4, lecC_out_gg(X1, X2)) → U31_GA(X1, X2, X3, X4, partcB_in_ggaa(X1, X3, X5, X6))
U31_GA(X1, X2, X3, X4, partcB_out_ggaa(X1, X3, X5, X6)) → U32_GA(X1, X2, X3, X4, qsF_in_ga(X5, X7))
U31_GA(X1, X2, X3, X4, partcB_out_ggaa(X1, X3, X5, X6)) → QSF_IN_GA(X5, X7)
QSF_IN_GA(.(X1, X2), X3) → U9_GA(X1, X2, X3, partB_in_ggaa(X1, X2, X4, X5))
QSF_IN_GA(.(X1, X2), X3) → PARTB_IN_GGAA(X1, X2, X4, X5)
QSF_IN_GA(.(X1, X2), X3) → U10_GA(X1, X2, X3, partcB_in_ggaa(X1, X2, X4, X5))
U10_GA(X1, X2, X3, partcB_out_ggaa(X1, X2, X4, X5)) → U11_GA(X1, X2, X3, qsF_in_ga(X4, X6))
U10_GA(X1, X2, X3, partcB_out_ggaa(X1, X2, X4, X5)) → QSF_IN_GA(X4, X6)
U10_GA(X1, X2, X3, partcB_out_ggaa(X1, X2, X4, X5)) → U12_GA(X1, X2, X3, X5, qscF_in_ga(X4, X6))
U12_GA(X1, X2, X3, X5, qscF_out_ga(X4, X6)) → U13_GA(X1, X2, X3, qsF_in_ga(X5, X7))
U12_GA(X1, X2, X3, X5, qscF_out_ga(X4, X6)) → QSF_IN_GA(X5, X7)
U12_GA(X1, X2, X3, X5, qscF_out_ga(X4, X6)) → U14_GA(X1, X2, X3, X6, qscF_in_ga(X5, X7))
U14_GA(X1, X2, X3, X6, qscF_out_ga(X5, X7)) → U15_GA(X1, X2, X3, appI_in_ggga(X6, X1, X7, X3))
U14_GA(X1, X2, X3, X6, qscF_out_ga(X5, X7)) → APPI_IN_GGGA(X6, X1, X7, X3)
APPI_IN_GGGA(.(X1, X2), X3, X4, .(X1, X5)) → U16_GGGA(X1, X2, X3, X4, X5, appI_in_ggga(X2, X3, X4, X5))
APPI_IN_GGGA(.(X1, X2), X3, X4, .(X1, X5)) → APPI_IN_GGGA(X2, X3, X4, X5)
U31_GA(X1, X2, X3, X4, partcB_out_ggaa(X1, X3, X5, X6)) → U33_GA(X1, X2, X3, X4, X6, qscF_in_ga(X5, X7))
U33_GA(X1, X2, X3, X4, X6, qscF_out_ga(X5, X7)) → U34_GA(X1, X2, X3, X4, pE_in_gagga(.(X2, X6), X8, X7, X1, X4))
U33_GA(X1, X2, X3, X4, X6, qscF_out_ga(X5, X7)) → PE_IN_GAGGA(.(X2, X6), X8, X7, X1, X4)
PE_IN_GAGGA(X1, X2, X3, X4, X5) → U18_GAGGA(X1, X2, X3, X4, X5, qsF_in_ga(X1, X2))
PE_IN_GAGGA(X1, X2, X3, X4, X5) → QSF_IN_GA(X1, X2)
PE_IN_GAGGA(X1, X2, X3, X4, X5) → U19_GAGGA(X1, X2, X3, X4, X5, qscF_in_ga(X1, X2))
U19_GAGGA(X1, X2, X3, X4, X5, qscF_out_ga(X1, X2)) → U20_GAGGA(X1, X2, X3, X4, X5, appG_in_ggga(X3, X4, X2, X5))
U19_GAGGA(X1, X2, X3, X4, X5, qscF_out_ga(X1, X2)) → APPG_IN_GGGA(X3, X4, X2, X5)
APPG_IN_GGGA(.(X1, X2), X3, X4, .(X1, X5)) → U17_GGGA(X1, X2, X3, X4, X5, appG_in_ggga(X2, X3, X4, X5))
APPG_IN_GGGA(.(X1, X2), X3, X4, .(X1, X5)) → APPG_IN_GGGA(X2, X3, X4, X5)
QSD_IN_GA(.(X1, []), X2) → U35_GA(X1, X2, qscH_in_a(X3))
U35_GA(X1, X2, qscH_out_a(X3)) → U36_GA(X1, X2, X3, qscH_in_a(X4))
U36_GA(X1, X2, X3, qscH_out_a(X4)) → U37_GA(X1, X2, appG_in_ggga(X3, X1, X4, X2))
U36_GA(X1, X2, X3, qscH_out_a(X4)) → APPG_IN_GGGA(X3, X1, X4, X2)
U24_GA(X1, X2, X3, X4, partcB_out_ggaa(X1, X3, X5, X6)) → U26_GA(X1, X2, X3, X4, X6, qscD_in_ga(.(X2, X5), X7))
U26_GA(X1, X2, X3, X4, X6, qscD_out_ga(.(X2, X5), X7)) → U27_GA(X1, X2, X3, X4, pE_in_gagga(X6, X8, X7, X1, X4))
U26_GA(X1, X2, X3, X4, X6, qscD_out_ga(.(X2, X5), X7)) → PE_IN_GAGGA(X6, X8, X7, X1, X4)
gtcA_in_gg(s(X1), s(X2)) → U39_gg(X1, X2, gtcA_in_gg(X1, X2))
gtcA_in_gg(s(0), 0) → gtcA_out_gg(s(0), 0)
U39_gg(X1, X2, gtcA_out_gg(X1, X2)) → gtcA_out_gg(s(X1), s(X2))
lecC_in_gg(s(X1), s(X2)) → U44_gg(X1, X2, lecC_in_gg(X1, X2))
lecC_in_gg(0, s(0)) → lecC_out_gg(0, s(0))
lecC_in_gg(0, 0) → lecC_out_gg(0, 0)
U44_gg(X1, X2, lecC_out_gg(X1, X2)) → lecC_out_gg(s(X1), s(X2))
partcB_in_ggaa(X1, .(X2, X3), .(X2, X4), X5) → U40_ggaa(X1, X2, X3, X4, X5, gtcA_in_gg(X1, X2))
U40_ggaa(X1, X2, X3, X4, X5, gtcA_out_gg(X1, X2)) → U41_ggaa(X1, X2, X3, X4, X5, partcB_in_ggaa(X1, X3, X4, X5))
partcB_in_ggaa(X1, .(X2, X3), X4, .(X2, X5)) → U42_ggaa(X1, X2, X3, X4, X5, lecC_in_gg(X1, X2))
U42_ggaa(X1, X2, X3, X4, X5, lecC_out_gg(X1, X2)) → U43_ggaa(X1, X2, X3, X4, X5, partcB_in_ggaa(X1, X3, X4, X5))
partcB_in_ggaa(X1, [], [], []) → partcB_out_ggaa(X1, [], [], [])
U43_ggaa(X1, X2, X3, X4, X5, partcB_out_ggaa(X1, X3, X4, X5)) → partcB_out_ggaa(X1, .(X2, X3), X4, .(X2, X5))
U41_ggaa(X1, X2, X3, X4, X5, partcB_out_ggaa(X1, X3, X4, X5)) → partcB_out_ggaa(X1, .(X2, X3), .(X2, X4), X5)
qscF_in_ga(.(X1, X2), X3) → U56_ga(X1, X2, X3, partcB_in_ggaa(X1, X2, X4, X5))
U56_ga(X1, X2, X3, partcB_out_ggaa(X1, X2, X4, X5)) → U57_ga(X1, X2, X3, X5, qscF_in_ga(X4, X6))
qscF_in_ga([], []) → qscF_out_ga([], [])
U57_ga(X1, X2, X3, X5, qscF_out_ga(X4, X6)) → U58_ga(X1, X2, X3, X6, qscF_in_ga(X5, X7))
U58_ga(X1, X2, X3, X6, qscF_out_ga(X5, X7)) → U59_ga(X1, X2, X3, appcI_in_ggga(X6, X1, X7, X3))
appcI_in_ggga(.(X1, X2), X3, X4, .(X1, X5)) → U60_ggga(X1, X2, X3, X4, X5, appcI_in_ggga(X2, X3, X4, X5))
appcI_in_ggga([], X1, X2, .(X1, X2)) → appcI_out_ggga([], X1, X2, .(X1, X2))
U60_ggga(X1, X2, X3, X4, X5, appcI_out_ggga(X2, X3, X4, X5)) → appcI_out_ggga(.(X1, X2), X3, X4, .(X1, X5))
U59_ga(X1, X2, X3, appcI_out_ggga(X6, X1, X7, X3)) → qscF_out_ga(.(X1, X2), X3)
qscH_in_a([]) → qscH_out_a([])
qscD_in_ga(.(X1, .(X2, X3)), X4) → U45_ga(X1, X2, X3, X4, gtcA_in_gg(X1, X2))
U45_ga(X1, X2, X3, X4, gtcA_out_gg(X1, X2)) → U46_ga(X1, X2, X3, X4, partcB_in_ggaa(X1, X3, X5, X6))
U46_ga(X1, X2, X3, X4, partcB_out_ggaa(X1, X3, X5, X6)) → U47_ga(X1, X2, X3, X4, X6, qscD_in_ga(.(X2, X5), X7))
qscD_in_ga(.(X1, .(X2, X3)), X4) → U49_ga(X1, X2, X3, X4, lecC_in_gg(X1, X2))
U49_ga(X1, X2, X3, X4, lecC_out_gg(X1, X2)) → U50_ga(X1, X2, X3, X4, partcB_in_ggaa(X1, X3, X5, X6))
U50_ga(X1, X2, X3, X4, partcB_out_ggaa(X1, X3, X5, X6)) → U51_ga(X1, X2, X3, X4, X6, qscF_in_ga(X5, X7))
U51_ga(X1, X2, X3, X4, X6, qscF_out_ga(X5, X7)) → U52_ga(X1, X2, X3, X4, qcE_in_gagga(.(X2, X6), X8, X7, X1, X4))
qcE_in_gagga(X1, X2, X3, X4, X5) → U62_gagga(X1, X2, X3, X4, X5, qscF_in_ga(X1, X2))
U62_gagga(X1, X2, X3, X4, X5, qscF_out_ga(X1, X2)) → U63_gagga(X1, X2, X3, X4, X5, appcG_in_ggga(X3, X4, X2, X5))
appcG_in_ggga(.(X1, X2), X3, X4, .(X1, X5)) → U61_ggga(X1, X2, X3, X4, X5, appcG_in_ggga(X2, X3, X4, X5))
appcG_in_ggga([], X1, X2, .(X1, X2)) → appcG_out_ggga([], X1, X2, .(X1, X2))
U61_ggga(X1, X2, X3, X4, X5, appcG_out_ggga(X2, X3, X4, X5)) → appcG_out_ggga(.(X1, X2), X3, X4, .(X1, X5))
U63_gagga(X1, X2, X3, X4, X5, appcG_out_ggga(X3, X4, X2, X5)) → qcE_out_gagga(X1, X2, X3, X4, X5)
U52_ga(X1, X2, X3, X4, qcE_out_gagga(.(X2, X6), X8, X7, X1, X4)) → qscD_out_ga(.(X1, .(X2, X3)), X4)
qscD_in_ga(.(X1, []), X2) → U53_ga(X1, X2, qscH_in_a(X3))
U53_ga(X1, X2, qscH_out_a(X3)) → U54_ga(X1, X2, X3, qscH_in_a(X4))
U54_ga(X1, X2, X3, qscH_out_a(X4)) → U55_ga(X1, X2, appcG_in_ggga(X3, X1, X4, X2))
U55_ga(X1, X2, appcG_out_ggga(X3, X1, X4, X2)) → qscD_out_ga(.(X1, []), X2)
qscD_in_ga([], []) → qscD_out_ga([], [])
U47_ga(X1, X2, X3, X4, X6, qscD_out_ga(.(X2, X5), X7)) → U48_ga(X1, X2, X3, X4, qcE_in_gagga(X6, X8, X7, X1, X4))
U48_ga(X1, X2, X3, X4, qcE_out_gagga(X6, X8, X7, X1, X4)) → qscD_out_ga(.(X1, .(X2, X3)), X4)
Infinitary Constructor Rewriting Termination of PiDP implies Termination of TRIPLES
QSD_IN_GA(.(X1, .(X2, X3)), X4) → U21_GA(X1, X2, X3, X4, gtA_in_gg(X1, X2))
QSD_IN_GA(.(X1, .(X2, X3)), X4) → GTA_IN_GG(X1, X2)
GTA_IN_GG(s(X1), s(X2)) → U1_GG(X1, X2, gtA_in_gg(X1, X2))
GTA_IN_GG(s(X1), s(X2)) → GTA_IN_GG(X1, X2)
QSD_IN_GA(.(X1, .(X2, X3)), X4) → U22_GA(X1, X2, X3, X4, gtcA_in_gg(X1, X2))
U22_GA(X1, X2, X3, X4, gtcA_out_gg(X1, X2)) → U23_GA(X1, X2, X3, X4, partB_in_ggaa(X1, X3, X5, X6))
U22_GA(X1, X2, X3, X4, gtcA_out_gg(X1, X2)) → PARTB_IN_GGAA(X1, X3, X5, X6)
PARTB_IN_GGAA(X1, .(X2, X3), .(X2, X4), X5) → U2_GGAA(X1, X2, X3, X4, X5, gtA_in_gg(X1, X2))
PARTB_IN_GGAA(X1, .(X2, X3), .(X2, X4), X5) → GTA_IN_GG(X1, X2)
PARTB_IN_GGAA(X1, .(X2, X3), .(X2, X4), X5) → U3_GGAA(X1, X2, X3, X4, X5, gtcA_in_gg(X1, X2))
U3_GGAA(X1, X2, X3, X4, X5, gtcA_out_gg(X1, X2)) → U4_GGAA(X1, X2, X3, X4, X5, partB_in_ggaa(X1, X3, X4, X5))
U3_GGAA(X1, X2, X3, X4, X5, gtcA_out_gg(X1, X2)) → PARTB_IN_GGAA(X1, X3, X4, X5)
PARTB_IN_GGAA(X1, .(X2, X3), X4, .(X2, X5)) → U5_GGAA(X1, X2, X3, X4, X5, leC_in_gg(X1, X2))
PARTB_IN_GGAA(X1, .(X2, X3), X4, .(X2, X5)) → LEC_IN_GG(X1, X2)
LEC_IN_GG(s(X1), s(X2)) → U8_GG(X1, X2, leC_in_gg(X1, X2))
LEC_IN_GG(s(X1), s(X2)) → LEC_IN_GG(X1, X2)
PARTB_IN_GGAA(X1, .(X2, X3), X4, .(X2, X5)) → U6_GGAA(X1, X2, X3, X4, X5, lecC_in_gg(X1, X2))
U6_GGAA(X1, X2, X3, X4, X5, lecC_out_gg(X1, X2)) → U7_GGAA(X1, X2, X3, X4, X5, partB_in_ggaa(X1, X3, X4, X5))
U6_GGAA(X1, X2, X3, X4, X5, lecC_out_gg(X1, X2)) → PARTB_IN_GGAA(X1, X3, X4, X5)
U22_GA(X1, X2, X3, X4, gtcA_out_gg(X1, X2)) → U24_GA(X1, X2, X3, X4, partcB_in_ggaa(X1, X3, X5, X6))
U24_GA(X1, X2, X3, X4, partcB_out_ggaa(X1, X3, X5, X6)) → U25_GA(X1, X2, X3, X4, qsD_in_ga(.(X2, X5), X7))
U24_GA(X1, X2, X3, X4, partcB_out_ggaa(X1, X3, X5, X6)) → QSD_IN_GA(.(X2, X5), X7)
QSD_IN_GA(.(X1, .(X2, X3)), X4) → U28_GA(X1, X2, X3, X4, leC_in_gg(X1, X2))
QSD_IN_GA(.(X1, .(X2, X3)), X4) → LEC_IN_GG(X1, X2)
QSD_IN_GA(.(X1, .(X2, X3)), X4) → U29_GA(X1, X2, X3, X4, lecC_in_gg(X1, X2))
U29_GA(X1, X2, X3, X4, lecC_out_gg(X1, X2)) → U30_GA(X1, X2, X3, X4, partB_in_ggaa(X1, X3, X5, X6))
U29_GA(X1, X2, X3, X4, lecC_out_gg(X1, X2)) → PARTB_IN_GGAA(X1, X3, X5, X6)
U29_GA(X1, X2, X3, X4, lecC_out_gg(X1, X2)) → U31_GA(X1, X2, X3, X4, partcB_in_ggaa(X1, X3, X5, X6))
U31_GA(X1, X2, X3, X4, partcB_out_ggaa(X1, X3, X5, X6)) → U32_GA(X1, X2, X3, X4, qsF_in_ga(X5, X7))
U31_GA(X1, X2, X3, X4, partcB_out_ggaa(X1, X3, X5, X6)) → QSF_IN_GA(X5, X7)
QSF_IN_GA(.(X1, X2), X3) → U9_GA(X1, X2, X3, partB_in_ggaa(X1, X2, X4, X5))
QSF_IN_GA(.(X1, X2), X3) → PARTB_IN_GGAA(X1, X2, X4, X5)
QSF_IN_GA(.(X1, X2), X3) → U10_GA(X1, X2, X3, partcB_in_ggaa(X1, X2, X4, X5))
U10_GA(X1, X2, X3, partcB_out_ggaa(X1, X2, X4, X5)) → U11_GA(X1, X2, X3, qsF_in_ga(X4, X6))
U10_GA(X1, X2, X3, partcB_out_ggaa(X1, X2, X4, X5)) → QSF_IN_GA(X4, X6)
U10_GA(X1, X2, X3, partcB_out_ggaa(X1, X2, X4, X5)) → U12_GA(X1, X2, X3, X5, qscF_in_ga(X4, X6))
U12_GA(X1, X2, X3, X5, qscF_out_ga(X4, X6)) → U13_GA(X1, X2, X3, qsF_in_ga(X5, X7))
U12_GA(X1, X2, X3, X5, qscF_out_ga(X4, X6)) → QSF_IN_GA(X5, X7)
U12_GA(X1, X2, X3, X5, qscF_out_ga(X4, X6)) → U14_GA(X1, X2, X3, X6, qscF_in_ga(X5, X7))
U14_GA(X1, X2, X3, X6, qscF_out_ga(X5, X7)) → U15_GA(X1, X2, X3, appI_in_ggga(X6, X1, X7, X3))
U14_GA(X1, X2, X3, X6, qscF_out_ga(X5, X7)) → APPI_IN_GGGA(X6, X1, X7, X3)
APPI_IN_GGGA(.(X1, X2), X3, X4, .(X1, X5)) → U16_GGGA(X1, X2, X3, X4, X5, appI_in_ggga(X2, X3, X4, X5))
APPI_IN_GGGA(.(X1, X2), X3, X4, .(X1, X5)) → APPI_IN_GGGA(X2, X3, X4, X5)
U31_GA(X1, X2, X3, X4, partcB_out_ggaa(X1, X3, X5, X6)) → U33_GA(X1, X2, X3, X4, X6, qscF_in_ga(X5, X7))
U33_GA(X1, X2, X3, X4, X6, qscF_out_ga(X5, X7)) → U34_GA(X1, X2, X3, X4, pE_in_gagga(.(X2, X6), X8, X7, X1, X4))
U33_GA(X1, X2, X3, X4, X6, qscF_out_ga(X5, X7)) → PE_IN_GAGGA(.(X2, X6), X8, X7, X1, X4)
PE_IN_GAGGA(X1, X2, X3, X4, X5) → U18_GAGGA(X1, X2, X3, X4, X5, qsF_in_ga(X1, X2))
PE_IN_GAGGA(X1, X2, X3, X4, X5) → QSF_IN_GA(X1, X2)
PE_IN_GAGGA(X1, X2, X3, X4, X5) → U19_GAGGA(X1, X2, X3, X4, X5, qscF_in_ga(X1, X2))
U19_GAGGA(X1, X2, X3, X4, X5, qscF_out_ga(X1, X2)) → U20_GAGGA(X1, X2, X3, X4, X5, appG_in_ggga(X3, X4, X2, X5))
U19_GAGGA(X1, X2, X3, X4, X5, qscF_out_ga(X1, X2)) → APPG_IN_GGGA(X3, X4, X2, X5)
APPG_IN_GGGA(.(X1, X2), X3, X4, .(X1, X5)) → U17_GGGA(X1, X2, X3, X4, X5, appG_in_ggga(X2, X3, X4, X5))
APPG_IN_GGGA(.(X1, X2), X3, X4, .(X1, X5)) → APPG_IN_GGGA(X2, X3, X4, X5)
QSD_IN_GA(.(X1, []), X2) → U35_GA(X1, X2, qscH_in_a(X3))
U35_GA(X1, X2, qscH_out_a(X3)) → U36_GA(X1, X2, X3, qscH_in_a(X4))
U36_GA(X1, X2, X3, qscH_out_a(X4)) → U37_GA(X1, X2, appG_in_ggga(X3, X1, X4, X2))
U36_GA(X1, X2, X3, qscH_out_a(X4)) → APPG_IN_GGGA(X3, X1, X4, X2)
U24_GA(X1, X2, X3, X4, partcB_out_ggaa(X1, X3, X5, X6)) → U26_GA(X1, X2, X3, X4, X6, qscD_in_ga(.(X2, X5), X7))
U26_GA(X1, X2, X3, X4, X6, qscD_out_ga(.(X2, X5), X7)) → U27_GA(X1, X2, X3, X4, pE_in_gagga(X6, X8, X7, X1, X4))
U26_GA(X1, X2, X3, X4, X6, qscD_out_ga(.(X2, X5), X7)) → PE_IN_GAGGA(X6, X8, X7, X1, X4)
gtcA_in_gg(s(X1), s(X2)) → U39_gg(X1, X2, gtcA_in_gg(X1, X2))
gtcA_in_gg(s(0), 0) → gtcA_out_gg(s(0), 0)
U39_gg(X1, X2, gtcA_out_gg(X1, X2)) → gtcA_out_gg(s(X1), s(X2))
lecC_in_gg(s(X1), s(X2)) → U44_gg(X1, X2, lecC_in_gg(X1, X2))
lecC_in_gg(0, s(0)) → lecC_out_gg(0, s(0))
lecC_in_gg(0, 0) → lecC_out_gg(0, 0)
U44_gg(X1, X2, lecC_out_gg(X1, X2)) → lecC_out_gg(s(X1), s(X2))
partcB_in_ggaa(X1, .(X2, X3), .(X2, X4), X5) → U40_ggaa(X1, X2, X3, X4, X5, gtcA_in_gg(X1, X2))
U40_ggaa(X1, X2, X3, X4, X5, gtcA_out_gg(X1, X2)) → U41_ggaa(X1, X2, X3, X4, X5, partcB_in_ggaa(X1, X3, X4, X5))
partcB_in_ggaa(X1, .(X2, X3), X4, .(X2, X5)) → U42_ggaa(X1, X2, X3, X4, X5, lecC_in_gg(X1, X2))
U42_ggaa(X1, X2, X3, X4, X5, lecC_out_gg(X1, X2)) → U43_ggaa(X1, X2, X3, X4, X5, partcB_in_ggaa(X1, X3, X4, X5))
partcB_in_ggaa(X1, [], [], []) → partcB_out_ggaa(X1, [], [], [])
U43_ggaa(X1, X2, X3, X4, X5, partcB_out_ggaa(X1, X3, X4, X5)) → partcB_out_ggaa(X1, .(X2, X3), X4, .(X2, X5))
U41_ggaa(X1, X2, X3, X4, X5, partcB_out_ggaa(X1, X3, X4, X5)) → partcB_out_ggaa(X1, .(X2, X3), .(X2, X4), X5)
qscF_in_ga(.(X1, X2), X3) → U56_ga(X1, X2, X3, partcB_in_ggaa(X1, X2, X4, X5))
U56_ga(X1, X2, X3, partcB_out_ggaa(X1, X2, X4, X5)) → U57_ga(X1, X2, X3, X5, qscF_in_ga(X4, X6))
qscF_in_ga([], []) → qscF_out_ga([], [])
U57_ga(X1, X2, X3, X5, qscF_out_ga(X4, X6)) → U58_ga(X1, X2, X3, X6, qscF_in_ga(X5, X7))
U58_ga(X1, X2, X3, X6, qscF_out_ga(X5, X7)) → U59_ga(X1, X2, X3, appcI_in_ggga(X6, X1, X7, X3))
appcI_in_ggga(.(X1, X2), X3, X4, .(X1, X5)) → U60_ggga(X1, X2, X3, X4, X5, appcI_in_ggga(X2, X3, X4, X5))
appcI_in_ggga([], X1, X2, .(X1, X2)) → appcI_out_ggga([], X1, X2, .(X1, X2))
U60_ggga(X1, X2, X3, X4, X5, appcI_out_ggga(X2, X3, X4, X5)) → appcI_out_ggga(.(X1, X2), X3, X4, .(X1, X5))
U59_ga(X1, X2, X3, appcI_out_ggga(X6, X1, X7, X3)) → qscF_out_ga(.(X1, X2), X3)
qscH_in_a([]) → qscH_out_a([])
qscD_in_ga(.(X1, .(X2, X3)), X4) → U45_ga(X1, X2, X3, X4, gtcA_in_gg(X1, X2))
U45_ga(X1, X2, X3, X4, gtcA_out_gg(X1, X2)) → U46_ga(X1, X2, X3, X4, partcB_in_ggaa(X1, X3, X5, X6))
U46_ga(X1, X2, X3, X4, partcB_out_ggaa(X1, X3, X5, X6)) → U47_ga(X1, X2, X3, X4, X6, qscD_in_ga(.(X2, X5), X7))
qscD_in_ga(.(X1, .(X2, X3)), X4) → U49_ga(X1, X2, X3, X4, lecC_in_gg(X1, X2))
U49_ga(X1, X2, X3, X4, lecC_out_gg(X1, X2)) → U50_ga(X1, X2, X3, X4, partcB_in_ggaa(X1, X3, X5, X6))
U50_ga(X1, X2, X3, X4, partcB_out_ggaa(X1, X3, X5, X6)) → U51_ga(X1, X2, X3, X4, X6, qscF_in_ga(X5, X7))
U51_ga(X1, X2, X3, X4, X6, qscF_out_ga(X5, X7)) → U52_ga(X1, X2, X3, X4, qcE_in_gagga(.(X2, X6), X8, X7, X1, X4))
qcE_in_gagga(X1, X2, X3, X4, X5) → U62_gagga(X1, X2, X3, X4, X5, qscF_in_ga(X1, X2))
U62_gagga(X1, X2, X3, X4, X5, qscF_out_ga(X1, X2)) → U63_gagga(X1, X2, X3, X4, X5, appcG_in_ggga(X3, X4, X2, X5))
appcG_in_ggga(.(X1, X2), X3, X4, .(X1, X5)) → U61_ggga(X1, X2, X3, X4, X5, appcG_in_ggga(X2, X3, X4, X5))
appcG_in_ggga([], X1, X2, .(X1, X2)) → appcG_out_ggga([], X1, X2, .(X1, X2))
U61_ggga(X1, X2, X3, X4, X5, appcG_out_ggga(X2, X3, X4, X5)) → appcG_out_ggga(.(X1, X2), X3, X4, .(X1, X5))
U63_gagga(X1, X2, X3, X4, X5, appcG_out_ggga(X3, X4, X2, X5)) → qcE_out_gagga(X1, X2, X3, X4, X5)
U52_ga(X1, X2, X3, X4, qcE_out_gagga(.(X2, X6), X8, X7, X1, X4)) → qscD_out_ga(.(X1, .(X2, X3)), X4)
qscD_in_ga(.(X1, []), X2) → U53_ga(X1, X2, qscH_in_a(X3))
U53_ga(X1, X2, qscH_out_a(X3)) → U54_ga(X1, X2, X3, qscH_in_a(X4))
U54_ga(X1, X2, X3, qscH_out_a(X4)) → U55_ga(X1, X2, appcG_in_ggga(X3, X1, X4, X2))
U55_ga(X1, X2, appcG_out_ggga(X3, X1, X4, X2)) → qscD_out_ga(.(X1, []), X2)
qscD_in_ga([], []) → qscD_out_ga([], [])
U47_ga(X1, X2, X3, X4, X6, qscD_out_ga(.(X2, X5), X7)) → U48_ga(X1, X2, X3, X4, qcE_in_gagga(X6, X8, X7, X1, X4))
U48_ga(X1, X2, X3, X4, qcE_out_gagga(X6, X8, X7, X1, X4)) → qscD_out_ga(.(X1, .(X2, X3)), X4)
APPG_IN_GGGA(.(X1, X2), X3, X4, .(X1, X5)) → APPG_IN_GGGA(X2, X3, X4, X5)
gtcA_in_gg(s(X1), s(X2)) → U39_gg(X1, X2, gtcA_in_gg(X1, X2))
gtcA_in_gg(s(0), 0) → gtcA_out_gg(s(0), 0)
U39_gg(X1, X2, gtcA_out_gg(X1, X2)) → gtcA_out_gg(s(X1), s(X2))
lecC_in_gg(s(X1), s(X2)) → U44_gg(X1, X2, lecC_in_gg(X1, X2))
lecC_in_gg(0, s(0)) → lecC_out_gg(0, s(0))
lecC_in_gg(0, 0) → lecC_out_gg(0, 0)
U44_gg(X1, X2, lecC_out_gg(X1, X2)) → lecC_out_gg(s(X1), s(X2))
partcB_in_ggaa(X1, .(X2, X3), .(X2, X4), X5) → U40_ggaa(X1, X2, X3, X4, X5, gtcA_in_gg(X1, X2))
U40_ggaa(X1, X2, X3, X4, X5, gtcA_out_gg(X1, X2)) → U41_ggaa(X1, X2, X3, X4, X5, partcB_in_ggaa(X1, X3, X4, X5))
partcB_in_ggaa(X1, .(X2, X3), X4, .(X2, X5)) → U42_ggaa(X1, X2, X3, X4, X5, lecC_in_gg(X1, X2))
U42_ggaa(X1, X2, X3, X4, X5, lecC_out_gg(X1, X2)) → U43_ggaa(X1, X2, X3, X4, X5, partcB_in_ggaa(X1, X3, X4, X5))
partcB_in_ggaa(X1, [], [], []) → partcB_out_ggaa(X1, [], [], [])
U43_ggaa(X1, X2, X3, X4, X5, partcB_out_ggaa(X1, X3, X4, X5)) → partcB_out_ggaa(X1, .(X2, X3), X4, .(X2, X5))
U41_ggaa(X1, X2, X3, X4, X5, partcB_out_ggaa(X1, X3, X4, X5)) → partcB_out_ggaa(X1, .(X2, X3), .(X2, X4), X5)
qscF_in_ga(.(X1, X2), X3) → U56_ga(X1, X2, X3, partcB_in_ggaa(X1, X2, X4, X5))
U56_ga(X1, X2, X3, partcB_out_ggaa(X1, X2, X4, X5)) → U57_ga(X1, X2, X3, X5, qscF_in_ga(X4, X6))
qscF_in_ga([], []) → qscF_out_ga([], [])
U57_ga(X1, X2, X3, X5, qscF_out_ga(X4, X6)) → U58_ga(X1, X2, X3, X6, qscF_in_ga(X5, X7))
U58_ga(X1, X2, X3, X6, qscF_out_ga(X5, X7)) → U59_ga(X1, X2, X3, appcI_in_ggga(X6, X1, X7, X3))
appcI_in_ggga(.(X1, X2), X3, X4, .(X1, X5)) → U60_ggga(X1, X2, X3, X4, X5, appcI_in_ggga(X2, X3, X4, X5))
appcI_in_ggga([], X1, X2, .(X1, X2)) → appcI_out_ggga([], X1, X2, .(X1, X2))
U60_ggga(X1, X2, X3, X4, X5, appcI_out_ggga(X2, X3, X4, X5)) → appcI_out_ggga(.(X1, X2), X3, X4, .(X1, X5))
U59_ga(X1, X2, X3, appcI_out_ggga(X6, X1, X7, X3)) → qscF_out_ga(.(X1, X2), X3)
qscH_in_a([]) → qscH_out_a([])
qscD_in_ga(.(X1, .(X2, X3)), X4) → U45_ga(X1, X2, X3, X4, gtcA_in_gg(X1, X2))
U45_ga(X1, X2, X3, X4, gtcA_out_gg(X1, X2)) → U46_ga(X1, X2, X3, X4, partcB_in_ggaa(X1, X3, X5, X6))
U46_ga(X1, X2, X3, X4, partcB_out_ggaa(X1, X3, X5, X6)) → U47_ga(X1, X2, X3, X4, X6, qscD_in_ga(.(X2, X5), X7))
qscD_in_ga(.(X1, .(X2, X3)), X4) → U49_ga(X1, X2, X3, X4, lecC_in_gg(X1, X2))
U49_ga(X1, X2, X3, X4, lecC_out_gg(X1, X2)) → U50_ga(X1, X2, X3, X4, partcB_in_ggaa(X1, X3, X5, X6))
U50_ga(X1, X2, X3, X4, partcB_out_ggaa(X1, X3, X5, X6)) → U51_ga(X1, X2, X3, X4, X6, qscF_in_ga(X5, X7))
U51_ga(X1, X2, X3, X4, X6, qscF_out_ga(X5, X7)) → U52_ga(X1, X2, X3, X4, qcE_in_gagga(.(X2, X6), X8, X7, X1, X4))
qcE_in_gagga(X1, X2, X3, X4, X5) → U62_gagga(X1, X2, X3, X4, X5, qscF_in_ga(X1, X2))
U62_gagga(X1, X2, X3, X4, X5, qscF_out_ga(X1, X2)) → U63_gagga(X1, X2, X3, X4, X5, appcG_in_ggga(X3, X4, X2, X5))
appcG_in_ggga(.(X1, X2), X3, X4, .(X1, X5)) → U61_ggga(X1, X2, X3, X4, X5, appcG_in_ggga(X2, X3, X4, X5))
appcG_in_ggga([], X1, X2, .(X1, X2)) → appcG_out_ggga([], X1, X2, .(X1, X2))
U61_ggga(X1, X2, X3, X4, X5, appcG_out_ggga(X2, X3, X4, X5)) → appcG_out_ggga(.(X1, X2), X3, X4, .(X1, X5))
U63_gagga(X1, X2, X3, X4, X5, appcG_out_ggga(X3, X4, X2, X5)) → qcE_out_gagga(X1, X2, X3, X4, X5)
U52_ga(X1, X2, X3, X4, qcE_out_gagga(.(X2, X6), X8, X7, X1, X4)) → qscD_out_ga(.(X1, .(X2, X3)), X4)
qscD_in_ga(.(X1, []), X2) → U53_ga(X1, X2, qscH_in_a(X3))
U53_ga(X1, X2, qscH_out_a(X3)) → U54_ga(X1, X2, X3, qscH_in_a(X4))
U54_ga(X1, X2, X3, qscH_out_a(X4)) → U55_ga(X1, X2, appcG_in_ggga(X3, X1, X4, X2))
U55_ga(X1, X2, appcG_out_ggga(X3, X1, X4, X2)) → qscD_out_ga(.(X1, []), X2)
qscD_in_ga([], []) → qscD_out_ga([], [])
U47_ga(X1, X2, X3, X4, X6, qscD_out_ga(.(X2, X5), X7)) → U48_ga(X1, X2, X3, X4, qcE_in_gagga(X6, X8, X7, X1, X4))
U48_ga(X1, X2, X3, X4, qcE_out_gagga(X6, X8, X7, X1, X4)) → qscD_out_ga(.(X1, .(X2, X3)), X4)
APPG_IN_GGGA(.(X1, X2), X3, X4, .(X1, X5)) → APPG_IN_GGGA(X2, X3, X4, X5)
APPG_IN_GGGA(.(X1, X2), X3, X4) → APPG_IN_GGGA(X2, X3, X4)
From the DPs we obtained the following set of size-change graphs:
APPI_IN_GGGA(.(X1, X2), X3, X4, .(X1, X5)) → APPI_IN_GGGA(X2, X3, X4, X5)
gtcA_in_gg(s(X1), s(X2)) → U39_gg(X1, X2, gtcA_in_gg(X1, X2))
gtcA_in_gg(s(0), 0) → gtcA_out_gg(s(0), 0)
U39_gg(X1, X2, gtcA_out_gg(X1, X2)) → gtcA_out_gg(s(X1), s(X2))
lecC_in_gg(s(X1), s(X2)) → U44_gg(X1, X2, lecC_in_gg(X1, X2))
lecC_in_gg(0, s(0)) → lecC_out_gg(0, s(0))
lecC_in_gg(0, 0) → lecC_out_gg(0, 0)
U44_gg(X1, X2, lecC_out_gg(X1, X2)) → lecC_out_gg(s(X1), s(X2))
partcB_in_ggaa(X1, .(X2, X3), .(X2, X4), X5) → U40_ggaa(X1, X2, X3, X4, X5, gtcA_in_gg(X1, X2))
U40_ggaa(X1, X2, X3, X4, X5, gtcA_out_gg(X1, X2)) → U41_ggaa(X1, X2, X3, X4, X5, partcB_in_ggaa(X1, X3, X4, X5))
partcB_in_ggaa(X1, .(X2, X3), X4, .(X2, X5)) → U42_ggaa(X1, X2, X3, X4, X5, lecC_in_gg(X1, X2))
U42_ggaa(X1, X2, X3, X4, X5, lecC_out_gg(X1, X2)) → U43_ggaa(X1, X2, X3, X4, X5, partcB_in_ggaa(X1, X3, X4, X5))
partcB_in_ggaa(X1, [], [], []) → partcB_out_ggaa(X1, [], [], [])
U43_ggaa(X1, X2, X3, X4, X5, partcB_out_ggaa(X1, X3, X4, X5)) → partcB_out_ggaa(X1, .(X2, X3), X4, .(X2, X5))
U41_ggaa(X1, X2, X3, X4, X5, partcB_out_ggaa(X1, X3, X4, X5)) → partcB_out_ggaa(X1, .(X2, X3), .(X2, X4), X5)
qscF_in_ga(.(X1, X2), X3) → U56_ga(X1, X2, X3, partcB_in_ggaa(X1, X2, X4, X5))
U56_ga(X1, X2, X3, partcB_out_ggaa(X1, X2, X4, X5)) → U57_ga(X1, X2, X3, X5, qscF_in_ga(X4, X6))
qscF_in_ga([], []) → qscF_out_ga([], [])
U57_ga(X1, X2, X3, X5, qscF_out_ga(X4, X6)) → U58_ga(X1, X2, X3, X6, qscF_in_ga(X5, X7))
U58_ga(X1, X2, X3, X6, qscF_out_ga(X5, X7)) → U59_ga(X1, X2, X3, appcI_in_ggga(X6, X1, X7, X3))
appcI_in_ggga(.(X1, X2), X3, X4, .(X1, X5)) → U60_ggga(X1, X2, X3, X4, X5, appcI_in_ggga(X2, X3, X4, X5))
appcI_in_ggga([], X1, X2, .(X1, X2)) → appcI_out_ggga([], X1, X2, .(X1, X2))
U60_ggga(X1, X2, X3, X4, X5, appcI_out_ggga(X2, X3, X4, X5)) → appcI_out_ggga(.(X1, X2), X3, X4, .(X1, X5))
U59_ga(X1, X2, X3, appcI_out_ggga(X6, X1, X7, X3)) → qscF_out_ga(.(X1, X2), X3)
qscH_in_a([]) → qscH_out_a([])
qscD_in_ga(.(X1, .(X2, X3)), X4) → U45_ga(X1, X2, X3, X4, gtcA_in_gg(X1, X2))
U45_ga(X1, X2, X3, X4, gtcA_out_gg(X1, X2)) → U46_ga(X1, X2, X3, X4, partcB_in_ggaa(X1, X3, X5, X6))
U46_ga(X1, X2, X3, X4, partcB_out_ggaa(X1, X3, X5, X6)) → U47_ga(X1, X2, X3, X4, X6, qscD_in_ga(.(X2, X5), X7))
qscD_in_ga(.(X1, .(X2, X3)), X4) → U49_ga(X1, X2, X3, X4, lecC_in_gg(X1, X2))
U49_ga(X1, X2, X3, X4, lecC_out_gg(X1, X2)) → U50_ga(X1, X2, X3, X4, partcB_in_ggaa(X1, X3, X5, X6))
U50_ga(X1, X2, X3, X4, partcB_out_ggaa(X1, X3, X5, X6)) → U51_ga(X1, X2, X3, X4, X6, qscF_in_ga(X5, X7))
U51_ga(X1, X2, X3, X4, X6, qscF_out_ga(X5, X7)) → U52_ga(X1, X2, X3, X4, qcE_in_gagga(.(X2, X6), X8, X7, X1, X4))
qcE_in_gagga(X1, X2, X3, X4, X5) → U62_gagga(X1, X2, X3, X4, X5, qscF_in_ga(X1, X2))
U62_gagga(X1, X2, X3, X4, X5, qscF_out_ga(X1, X2)) → U63_gagga(X1, X2, X3, X4, X5, appcG_in_ggga(X3, X4, X2, X5))
appcG_in_ggga(.(X1, X2), X3, X4, .(X1, X5)) → U61_ggga(X1, X2, X3, X4, X5, appcG_in_ggga(X2, X3, X4, X5))
appcG_in_ggga([], X1, X2, .(X1, X2)) → appcG_out_ggga([], X1, X2, .(X1, X2))
U61_ggga(X1, X2, X3, X4, X5, appcG_out_ggga(X2, X3, X4, X5)) → appcG_out_ggga(.(X1, X2), X3, X4, .(X1, X5))
U63_gagga(X1, X2, X3, X4, X5, appcG_out_ggga(X3, X4, X2, X5)) → qcE_out_gagga(X1, X2, X3, X4, X5)
U52_ga(X1, X2, X3, X4, qcE_out_gagga(.(X2, X6), X8, X7, X1, X4)) → qscD_out_ga(.(X1, .(X2, X3)), X4)
qscD_in_ga(.(X1, []), X2) → U53_ga(X1, X2, qscH_in_a(X3))
U53_ga(X1, X2, qscH_out_a(X3)) → U54_ga(X1, X2, X3, qscH_in_a(X4))
U54_ga(X1, X2, X3, qscH_out_a(X4)) → U55_ga(X1, X2, appcG_in_ggga(X3, X1, X4, X2))
U55_ga(X1, X2, appcG_out_ggga(X3, X1, X4, X2)) → qscD_out_ga(.(X1, []), X2)
qscD_in_ga([], []) → qscD_out_ga([], [])
U47_ga(X1, X2, X3, X4, X6, qscD_out_ga(.(X2, X5), X7)) → U48_ga(X1, X2, X3, X4, qcE_in_gagga(X6, X8, X7, X1, X4))
U48_ga(X1, X2, X3, X4, qcE_out_gagga(X6, X8, X7, X1, X4)) → qscD_out_ga(.(X1, .(X2, X3)), X4)
APPI_IN_GGGA(.(X1, X2), X3, X4, .(X1, X5)) → APPI_IN_GGGA(X2, X3, X4, X5)
APPI_IN_GGGA(.(X1, X2), X3, X4) → APPI_IN_GGGA(X2, X3, X4)
From the DPs we obtained the following set of size-change graphs:
LEC_IN_GG(s(X1), s(X2)) → LEC_IN_GG(X1, X2)
gtcA_in_gg(s(X1), s(X2)) → U39_gg(X1, X2, gtcA_in_gg(X1, X2))
gtcA_in_gg(s(0), 0) → gtcA_out_gg(s(0), 0)
U39_gg(X1, X2, gtcA_out_gg(X1, X2)) → gtcA_out_gg(s(X1), s(X2))
lecC_in_gg(s(X1), s(X2)) → U44_gg(X1, X2, lecC_in_gg(X1, X2))
lecC_in_gg(0, s(0)) → lecC_out_gg(0, s(0))
lecC_in_gg(0, 0) → lecC_out_gg(0, 0)
U44_gg(X1, X2, lecC_out_gg(X1, X2)) → lecC_out_gg(s(X1), s(X2))
partcB_in_ggaa(X1, .(X2, X3), .(X2, X4), X5) → U40_ggaa(X1, X2, X3, X4, X5, gtcA_in_gg(X1, X2))
U40_ggaa(X1, X2, X3, X4, X5, gtcA_out_gg(X1, X2)) → U41_ggaa(X1, X2, X3, X4, X5, partcB_in_ggaa(X1, X3, X4, X5))
partcB_in_ggaa(X1, .(X2, X3), X4, .(X2, X5)) → U42_ggaa(X1, X2, X3, X4, X5, lecC_in_gg(X1, X2))
U42_ggaa(X1, X2, X3, X4, X5, lecC_out_gg(X1, X2)) → U43_ggaa(X1, X2, X3, X4, X5, partcB_in_ggaa(X1, X3, X4, X5))
partcB_in_ggaa(X1, [], [], []) → partcB_out_ggaa(X1, [], [], [])
U43_ggaa(X1, X2, X3, X4, X5, partcB_out_ggaa(X1, X3, X4, X5)) → partcB_out_ggaa(X1, .(X2, X3), X4, .(X2, X5))
U41_ggaa(X1, X2, X3, X4, X5, partcB_out_ggaa(X1, X3, X4, X5)) → partcB_out_ggaa(X1, .(X2, X3), .(X2, X4), X5)
qscF_in_ga(.(X1, X2), X3) → U56_ga(X1, X2, X3, partcB_in_ggaa(X1, X2, X4, X5))
U56_ga(X1, X2, X3, partcB_out_ggaa(X1, X2, X4, X5)) → U57_ga(X1, X2, X3, X5, qscF_in_ga(X4, X6))
qscF_in_ga([], []) → qscF_out_ga([], [])
U57_ga(X1, X2, X3, X5, qscF_out_ga(X4, X6)) → U58_ga(X1, X2, X3, X6, qscF_in_ga(X5, X7))
U58_ga(X1, X2, X3, X6, qscF_out_ga(X5, X7)) → U59_ga(X1, X2, X3, appcI_in_ggga(X6, X1, X7, X3))
appcI_in_ggga(.(X1, X2), X3, X4, .(X1, X5)) → U60_ggga(X1, X2, X3, X4, X5, appcI_in_ggga(X2, X3, X4, X5))
appcI_in_ggga([], X1, X2, .(X1, X2)) → appcI_out_ggga([], X1, X2, .(X1, X2))
U60_ggga(X1, X2, X3, X4, X5, appcI_out_ggga(X2, X3, X4, X5)) → appcI_out_ggga(.(X1, X2), X3, X4, .(X1, X5))
U59_ga(X1, X2, X3, appcI_out_ggga(X6, X1, X7, X3)) → qscF_out_ga(.(X1, X2), X3)
qscH_in_a([]) → qscH_out_a([])
qscD_in_ga(.(X1, .(X2, X3)), X4) → U45_ga(X1, X2, X3, X4, gtcA_in_gg(X1, X2))
U45_ga(X1, X2, X3, X4, gtcA_out_gg(X1, X2)) → U46_ga(X1, X2, X3, X4, partcB_in_ggaa(X1, X3, X5, X6))
U46_ga(X1, X2, X3, X4, partcB_out_ggaa(X1, X3, X5, X6)) → U47_ga(X1, X2, X3, X4, X6, qscD_in_ga(.(X2, X5), X7))
qscD_in_ga(.(X1, .(X2, X3)), X4) → U49_ga(X1, X2, X3, X4, lecC_in_gg(X1, X2))
U49_ga(X1, X2, X3, X4, lecC_out_gg(X1, X2)) → U50_ga(X1, X2, X3, X4, partcB_in_ggaa(X1, X3, X5, X6))
U50_ga(X1, X2, X3, X4, partcB_out_ggaa(X1, X3, X5, X6)) → U51_ga(X1, X2, X3, X4, X6, qscF_in_ga(X5, X7))
U51_ga(X1, X2, X3, X4, X6, qscF_out_ga(X5, X7)) → U52_ga(X1, X2, X3, X4, qcE_in_gagga(.(X2, X6), X8, X7, X1, X4))
qcE_in_gagga(X1, X2, X3, X4, X5) → U62_gagga(X1, X2, X3, X4, X5, qscF_in_ga(X1, X2))
U62_gagga(X1, X2, X3, X4, X5, qscF_out_ga(X1, X2)) → U63_gagga(X1, X2, X3, X4, X5, appcG_in_ggga(X3, X4, X2, X5))
appcG_in_ggga(.(X1, X2), X3, X4, .(X1, X5)) → U61_ggga(X1, X2, X3, X4, X5, appcG_in_ggga(X2, X3, X4, X5))
appcG_in_ggga([], X1, X2, .(X1, X2)) → appcG_out_ggga([], X1, X2, .(X1, X2))
U61_ggga(X1, X2, X3, X4, X5, appcG_out_ggga(X2, X3, X4, X5)) → appcG_out_ggga(.(X1, X2), X3, X4, .(X1, X5))
U63_gagga(X1, X2, X3, X4, X5, appcG_out_ggga(X3, X4, X2, X5)) → qcE_out_gagga(X1, X2, X3, X4, X5)
U52_ga(X1, X2, X3, X4, qcE_out_gagga(.(X2, X6), X8, X7, X1, X4)) → qscD_out_ga(.(X1, .(X2, X3)), X4)
qscD_in_ga(.(X1, []), X2) → U53_ga(X1, X2, qscH_in_a(X3))
U53_ga(X1, X2, qscH_out_a(X3)) → U54_ga(X1, X2, X3, qscH_in_a(X4))
U54_ga(X1, X2, X3, qscH_out_a(X4)) → U55_ga(X1, X2, appcG_in_ggga(X3, X1, X4, X2))
U55_ga(X1, X2, appcG_out_ggga(X3, X1, X4, X2)) → qscD_out_ga(.(X1, []), X2)
qscD_in_ga([], []) → qscD_out_ga([], [])
U47_ga(X1, X2, X3, X4, X6, qscD_out_ga(.(X2, X5), X7)) → U48_ga(X1, X2, X3, X4, qcE_in_gagga(X6, X8, X7, X1, X4))
U48_ga(X1, X2, X3, X4, qcE_out_gagga(X6, X8, X7, X1, X4)) → qscD_out_ga(.(X1, .(X2, X3)), X4)
LEC_IN_GG(s(X1), s(X2)) → LEC_IN_GG(X1, X2)
LEC_IN_GG(s(X1), s(X2)) → LEC_IN_GG(X1, X2)
From the DPs we obtained the following set of size-change graphs:
GTA_IN_GG(s(X1), s(X2)) → GTA_IN_GG(X1, X2)
gtcA_in_gg(s(X1), s(X2)) → U39_gg(X1, X2, gtcA_in_gg(X1, X2))
gtcA_in_gg(s(0), 0) → gtcA_out_gg(s(0), 0)
U39_gg(X1, X2, gtcA_out_gg(X1, X2)) → gtcA_out_gg(s(X1), s(X2))
lecC_in_gg(s(X1), s(X2)) → U44_gg(X1, X2, lecC_in_gg(X1, X2))
lecC_in_gg(0, s(0)) → lecC_out_gg(0, s(0))
lecC_in_gg(0, 0) → lecC_out_gg(0, 0)
U44_gg(X1, X2, lecC_out_gg(X1, X2)) → lecC_out_gg(s(X1), s(X2))
partcB_in_ggaa(X1, .(X2, X3), .(X2, X4), X5) → U40_ggaa(X1, X2, X3, X4, X5, gtcA_in_gg(X1, X2))
U40_ggaa(X1, X2, X3, X4, X5, gtcA_out_gg(X1, X2)) → U41_ggaa(X1, X2, X3, X4, X5, partcB_in_ggaa(X1, X3, X4, X5))
partcB_in_ggaa(X1, .(X2, X3), X4, .(X2, X5)) → U42_ggaa(X1, X2, X3, X4, X5, lecC_in_gg(X1, X2))
U42_ggaa(X1, X2, X3, X4, X5, lecC_out_gg(X1, X2)) → U43_ggaa(X1, X2, X3, X4, X5, partcB_in_ggaa(X1, X3, X4, X5))
partcB_in_ggaa(X1, [], [], []) → partcB_out_ggaa(X1, [], [], [])
U43_ggaa(X1, X2, X3, X4, X5, partcB_out_ggaa(X1, X3, X4, X5)) → partcB_out_ggaa(X1, .(X2, X3), X4, .(X2, X5))
U41_ggaa(X1, X2, X3, X4, X5, partcB_out_ggaa(X1, X3, X4, X5)) → partcB_out_ggaa(X1, .(X2, X3), .(X2, X4), X5)
qscF_in_ga(.(X1, X2), X3) → U56_ga(X1, X2, X3, partcB_in_ggaa(X1, X2, X4, X5))
U56_ga(X1, X2, X3, partcB_out_ggaa(X1, X2, X4, X5)) → U57_ga(X1, X2, X3, X5, qscF_in_ga(X4, X6))
qscF_in_ga([], []) → qscF_out_ga([], [])
U57_ga(X1, X2, X3, X5, qscF_out_ga(X4, X6)) → U58_ga(X1, X2, X3, X6, qscF_in_ga(X5, X7))
U58_ga(X1, X2, X3, X6, qscF_out_ga(X5, X7)) → U59_ga(X1, X2, X3, appcI_in_ggga(X6, X1, X7, X3))
appcI_in_ggga(.(X1, X2), X3, X4, .(X1, X5)) → U60_ggga(X1, X2, X3, X4, X5, appcI_in_ggga(X2, X3, X4, X5))
appcI_in_ggga([], X1, X2, .(X1, X2)) → appcI_out_ggga([], X1, X2, .(X1, X2))
U60_ggga(X1, X2, X3, X4, X5, appcI_out_ggga(X2, X3, X4, X5)) → appcI_out_ggga(.(X1, X2), X3, X4, .(X1, X5))
U59_ga(X1, X2, X3, appcI_out_ggga(X6, X1, X7, X3)) → qscF_out_ga(.(X1, X2), X3)
qscH_in_a([]) → qscH_out_a([])
qscD_in_ga(.(X1, .(X2, X3)), X4) → U45_ga(X1, X2, X3, X4, gtcA_in_gg(X1, X2))
U45_ga(X1, X2, X3, X4, gtcA_out_gg(X1, X2)) → U46_ga(X1, X2, X3, X4, partcB_in_ggaa(X1, X3, X5, X6))
U46_ga(X1, X2, X3, X4, partcB_out_ggaa(X1, X3, X5, X6)) → U47_ga(X1, X2, X3, X4, X6, qscD_in_ga(.(X2, X5), X7))
qscD_in_ga(.(X1, .(X2, X3)), X4) → U49_ga(X1, X2, X3, X4, lecC_in_gg(X1, X2))
U49_ga(X1, X2, X3, X4, lecC_out_gg(X1, X2)) → U50_ga(X1, X2, X3, X4, partcB_in_ggaa(X1, X3, X5, X6))
U50_ga(X1, X2, X3, X4, partcB_out_ggaa(X1, X3, X5, X6)) → U51_ga(X1, X2, X3, X4, X6, qscF_in_ga(X5, X7))
U51_ga(X1, X2, X3, X4, X6, qscF_out_ga(X5, X7)) → U52_ga(X1, X2, X3, X4, qcE_in_gagga(.(X2, X6), X8, X7, X1, X4))
qcE_in_gagga(X1, X2, X3, X4, X5) → U62_gagga(X1, X2, X3, X4, X5, qscF_in_ga(X1, X2))
U62_gagga(X1, X2, X3, X4, X5, qscF_out_ga(X1, X2)) → U63_gagga(X1, X2, X3, X4, X5, appcG_in_ggga(X3, X4, X2, X5))
appcG_in_ggga(.(X1, X2), X3, X4, .(X1, X5)) → U61_ggga(X1, X2, X3, X4, X5, appcG_in_ggga(X2, X3, X4, X5))
appcG_in_ggga([], X1, X2, .(X1, X2)) → appcG_out_ggga([], X1, X2, .(X1, X2))
U61_ggga(X1, X2, X3, X4, X5, appcG_out_ggga(X2, X3, X4, X5)) → appcG_out_ggga(.(X1, X2), X3, X4, .(X1, X5))
U63_gagga(X1, X2, X3, X4, X5, appcG_out_ggga(X3, X4, X2, X5)) → qcE_out_gagga(X1, X2, X3, X4, X5)
U52_ga(X1, X2, X3, X4, qcE_out_gagga(.(X2, X6), X8, X7, X1, X4)) → qscD_out_ga(.(X1, .(X2, X3)), X4)
qscD_in_ga(.(X1, []), X2) → U53_ga(X1, X2, qscH_in_a(X3))
U53_ga(X1, X2, qscH_out_a(X3)) → U54_ga(X1, X2, X3, qscH_in_a(X4))
U54_ga(X1, X2, X3, qscH_out_a(X4)) → U55_ga(X1, X2, appcG_in_ggga(X3, X1, X4, X2))
U55_ga(X1, X2, appcG_out_ggga(X3, X1, X4, X2)) → qscD_out_ga(.(X1, []), X2)
qscD_in_ga([], []) → qscD_out_ga([], [])
U47_ga(X1, X2, X3, X4, X6, qscD_out_ga(.(X2, X5), X7)) → U48_ga(X1, X2, X3, X4, qcE_in_gagga(X6, X8, X7, X1, X4))
U48_ga(X1, X2, X3, X4, qcE_out_gagga(X6, X8, X7, X1, X4)) → qscD_out_ga(.(X1, .(X2, X3)), X4)
GTA_IN_GG(s(X1), s(X2)) → GTA_IN_GG(X1, X2)
GTA_IN_GG(s(X1), s(X2)) → GTA_IN_GG(X1, X2)
From the DPs we obtained the following set of size-change graphs:
PARTB_IN_GGAA(X1, .(X2, X3), .(X2, X4), X5) → U3_GGAA(X1, X2, X3, X4, X5, gtcA_in_gg(X1, X2))
U3_GGAA(X1, X2, X3, X4, X5, gtcA_out_gg(X1, X2)) → PARTB_IN_GGAA(X1, X3, X4, X5)
PARTB_IN_GGAA(X1, .(X2, X3), X4, .(X2, X5)) → U6_GGAA(X1, X2, X3, X4, X5, lecC_in_gg(X1, X2))
U6_GGAA(X1, X2, X3, X4, X5, lecC_out_gg(X1, X2)) → PARTB_IN_GGAA(X1, X3, X4, X5)
gtcA_in_gg(s(X1), s(X2)) → U39_gg(X1, X2, gtcA_in_gg(X1, X2))
gtcA_in_gg(s(0), 0) → gtcA_out_gg(s(0), 0)
U39_gg(X1, X2, gtcA_out_gg(X1, X2)) → gtcA_out_gg(s(X1), s(X2))
lecC_in_gg(s(X1), s(X2)) → U44_gg(X1, X2, lecC_in_gg(X1, X2))
lecC_in_gg(0, s(0)) → lecC_out_gg(0, s(0))
lecC_in_gg(0, 0) → lecC_out_gg(0, 0)
U44_gg(X1, X2, lecC_out_gg(X1, X2)) → lecC_out_gg(s(X1), s(X2))
partcB_in_ggaa(X1, .(X2, X3), .(X2, X4), X5) → U40_ggaa(X1, X2, X3, X4, X5, gtcA_in_gg(X1, X2))
U40_ggaa(X1, X2, X3, X4, X5, gtcA_out_gg(X1, X2)) → U41_ggaa(X1, X2, X3, X4, X5, partcB_in_ggaa(X1, X3, X4, X5))
partcB_in_ggaa(X1, .(X2, X3), X4, .(X2, X5)) → U42_ggaa(X1, X2, X3, X4, X5, lecC_in_gg(X1, X2))
U42_ggaa(X1, X2, X3, X4, X5, lecC_out_gg(X1, X2)) → U43_ggaa(X1, X2, X3, X4, X5, partcB_in_ggaa(X1, X3, X4, X5))
partcB_in_ggaa(X1, [], [], []) → partcB_out_ggaa(X1, [], [], [])
U43_ggaa(X1, X2, X3, X4, X5, partcB_out_ggaa(X1, X3, X4, X5)) → partcB_out_ggaa(X1, .(X2, X3), X4, .(X2, X5))
U41_ggaa(X1, X2, X3, X4, X5, partcB_out_ggaa(X1, X3, X4, X5)) → partcB_out_ggaa(X1, .(X2, X3), .(X2, X4), X5)
qscF_in_ga(.(X1, X2), X3) → U56_ga(X1, X2, X3, partcB_in_ggaa(X1, X2, X4, X5))
U56_ga(X1, X2, X3, partcB_out_ggaa(X1, X2, X4, X5)) → U57_ga(X1, X2, X3, X5, qscF_in_ga(X4, X6))
qscF_in_ga([], []) → qscF_out_ga([], [])
U57_ga(X1, X2, X3, X5, qscF_out_ga(X4, X6)) → U58_ga(X1, X2, X3, X6, qscF_in_ga(X5, X7))
U58_ga(X1, X2, X3, X6, qscF_out_ga(X5, X7)) → U59_ga(X1, X2, X3, appcI_in_ggga(X6, X1, X7, X3))
appcI_in_ggga(.(X1, X2), X3, X4, .(X1, X5)) → U60_ggga(X1, X2, X3, X4, X5, appcI_in_ggga(X2, X3, X4, X5))
appcI_in_ggga([], X1, X2, .(X1, X2)) → appcI_out_ggga([], X1, X2, .(X1, X2))
U60_ggga(X1, X2, X3, X4, X5, appcI_out_ggga(X2, X3, X4, X5)) → appcI_out_ggga(.(X1, X2), X3, X4, .(X1, X5))
U59_ga(X1, X2, X3, appcI_out_ggga(X6, X1, X7, X3)) → qscF_out_ga(.(X1, X2), X3)
qscH_in_a([]) → qscH_out_a([])
qscD_in_ga(.(X1, .(X2, X3)), X4) → U45_ga(X1, X2, X3, X4, gtcA_in_gg(X1, X2))
U45_ga(X1, X2, X3, X4, gtcA_out_gg(X1, X2)) → U46_ga(X1, X2, X3, X4, partcB_in_ggaa(X1, X3, X5, X6))
U46_ga(X1, X2, X3, X4, partcB_out_ggaa(X1, X3, X5, X6)) → U47_ga(X1, X2, X3, X4, X6, qscD_in_ga(.(X2, X5), X7))
qscD_in_ga(.(X1, .(X2, X3)), X4) → U49_ga(X1, X2, X3, X4, lecC_in_gg(X1, X2))
U49_ga(X1, X2, X3, X4, lecC_out_gg(X1, X2)) → U50_ga(X1, X2, X3, X4, partcB_in_ggaa(X1, X3, X5, X6))
U50_ga(X1, X2, X3, X4, partcB_out_ggaa(X1, X3, X5, X6)) → U51_ga(X1, X2, X3, X4, X6, qscF_in_ga(X5, X7))
U51_ga(X1, X2, X3, X4, X6, qscF_out_ga(X5, X7)) → U52_ga(X1, X2, X3, X4, qcE_in_gagga(.(X2, X6), X8, X7, X1, X4))
qcE_in_gagga(X1, X2, X3, X4, X5) → U62_gagga(X1, X2, X3, X4, X5, qscF_in_ga(X1, X2))
U62_gagga(X1, X2, X3, X4, X5, qscF_out_ga(X1, X2)) → U63_gagga(X1, X2, X3, X4, X5, appcG_in_ggga(X3, X4, X2, X5))
appcG_in_ggga(.(X1, X2), X3, X4, .(X1, X5)) → U61_ggga(X1, X2, X3, X4, X5, appcG_in_ggga(X2, X3, X4, X5))
appcG_in_ggga([], X1, X2, .(X1, X2)) → appcG_out_ggga([], X1, X2, .(X1, X2))
U61_ggga(X1, X2, X3, X4, X5, appcG_out_ggga(X2, X3, X4, X5)) → appcG_out_ggga(.(X1, X2), X3, X4, .(X1, X5))
U63_gagga(X1, X2, X3, X4, X5, appcG_out_ggga(X3, X4, X2, X5)) → qcE_out_gagga(X1, X2, X3, X4, X5)
U52_ga(X1, X2, X3, X4, qcE_out_gagga(.(X2, X6), X8, X7, X1, X4)) → qscD_out_ga(.(X1, .(X2, X3)), X4)
qscD_in_ga(.(X1, []), X2) → U53_ga(X1, X2, qscH_in_a(X3))
U53_ga(X1, X2, qscH_out_a(X3)) → U54_ga(X1, X2, X3, qscH_in_a(X4))
U54_ga(X1, X2, X3, qscH_out_a(X4)) → U55_ga(X1, X2, appcG_in_ggga(X3, X1, X4, X2))
U55_ga(X1, X2, appcG_out_ggga(X3, X1, X4, X2)) → qscD_out_ga(.(X1, []), X2)
qscD_in_ga([], []) → qscD_out_ga([], [])
U47_ga(X1, X2, X3, X4, X6, qscD_out_ga(.(X2, X5), X7)) → U48_ga(X1, X2, X3, X4, qcE_in_gagga(X6, X8, X7, X1, X4))
U48_ga(X1, X2, X3, X4, qcE_out_gagga(X6, X8, X7, X1, X4)) → qscD_out_ga(.(X1, .(X2, X3)), X4)
PARTB_IN_GGAA(X1, .(X2, X3), .(X2, X4), X5) → U3_GGAA(X1, X2, X3, X4, X5, gtcA_in_gg(X1, X2))
U3_GGAA(X1, X2, X3, X4, X5, gtcA_out_gg(X1, X2)) → PARTB_IN_GGAA(X1, X3, X4, X5)
PARTB_IN_GGAA(X1, .(X2, X3), X4, .(X2, X5)) → U6_GGAA(X1, X2, X3, X4, X5, lecC_in_gg(X1, X2))
U6_GGAA(X1, X2, X3, X4, X5, lecC_out_gg(X1, X2)) → PARTB_IN_GGAA(X1, X3, X4, X5)
gtcA_in_gg(s(X1), s(X2)) → U39_gg(X1, X2, gtcA_in_gg(X1, X2))
gtcA_in_gg(s(0), 0) → gtcA_out_gg(s(0), 0)
lecC_in_gg(s(X1), s(X2)) → U44_gg(X1, X2, lecC_in_gg(X1, X2))
lecC_in_gg(0, s(0)) → lecC_out_gg(0, s(0))
lecC_in_gg(0, 0) → lecC_out_gg(0, 0)
U39_gg(X1, X2, gtcA_out_gg(X1, X2)) → gtcA_out_gg(s(X1), s(X2))
U44_gg(X1, X2, lecC_out_gg(X1, X2)) → lecC_out_gg(s(X1), s(X2))
PARTB_IN_GGAA(X1, .(X2, X3)) → U3_GGAA(X1, X2, X3, gtcA_in_gg(X1, X2))
U3_GGAA(X1, X2, X3, gtcA_out_gg(X1, X2)) → PARTB_IN_GGAA(X1, X3)
PARTB_IN_GGAA(X1, .(X2, X3)) → U6_GGAA(X1, X2, X3, lecC_in_gg(X1, X2))
U6_GGAA(X1, X2, X3, lecC_out_gg(X1, X2)) → PARTB_IN_GGAA(X1, X3)
gtcA_in_gg(s(X1), s(X2)) → U39_gg(X1, X2, gtcA_in_gg(X1, X2))
gtcA_in_gg(s(0), 0) → gtcA_out_gg(s(0), 0)
lecC_in_gg(s(X1), s(X2)) → U44_gg(X1, X2, lecC_in_gg(X1, X2))
lecC_in_gg(0, s(0)) → lecC_out_gg(0, s(0))
lecC_in_gg(0, 0) → lecC_out_gg(0, 0)
U39_gg(X1, X2, gtcA_out_gg(X1, X2)) → gtcA_out_gg(s(X1), s(X2))
U44_gg(X1, X2, lecC_out_gg(X1, X2)) → lecC_out_gg(s(X1), s(X2))
gtcA_in_gg(x0, x1)
lecC_in_gg(x0, x1)
U39_gg(x0, x1, x2)
U44_gg(x0, x1, x2)
From the DPs we obtained the following set of size-change graphs:
QSF_IN_GA(.(X1, X2), X3) → U10_GA(X1, X2, X3, partcB_in_ggaa(X1, X2, X4, X5))
U10_GA(X1, X2, X3, partcB_out_ggaa(X1, X2, X4, X5)) → QSF_IN_GA(X4, X6)
U10_GA(X1, X2, X3, partcB_out_ggaa(X1, X2, X4, X5)) → U12_GA(X1, X2, X3, X5, qscF_in_ga(X4, X6))
U12_GA(X1, X2, X3, X5, qscF_out_ga(X4, X6)) → QSF_IN_GA(X5, X7)
gtcA_in_gg(s(X1), s(X2)) → U39_gg(X1, X2, gtcA_in_gg(X1, X2))
gtcA_in_gg(s(0), 0) → gtcA_out_gg(s(0), 0)
U39_gg(X1, X2, gtcA_out_gg(X1, X2)) → gtcA_out_gg(s(X1), s(X2))
lecC_in_gg(s(X1), s(X2)) → U44_gg(X1, X2, lecC_in_gg(X1, X2))
lecC_in_gg(0, s(0)) → lecC_out_gg(0, s(0))
lecC_in_gg(0, 0) → lecC_out_gg(0, 0)
U44_gg(X1, X2, lecC_out_gg(X1, X2)) → lecC_out_gg(s(X1), s(X2))
partcB_in_ggaa(X1, .(X2, X3), .(X2, X4), X5) → U40_ggaa(X1, X2, X3, X4, X5, gtcA_in_gg(X1, X2))
U40_ggaa(X1, X2, X3, X4, X5, gtcA_out_gg(X1, X2)) → U41_ggaa(X1, X2, X3, X4, X5, partcB_in_ggaa(X1, X3, X4, X5))
partcB_in_ggaa(X1, .(X2, X3), X4, .(X2, X5)) → U42_ggaa(X1, X2, X3, X4, X5, lecC_in_gg(X1, X2))
U42_ggaa(X1, X2, X3, X4, X5, lecC_out_gg(X1, X2)) → U43_ggaa(X1, X2, X3, X4, X5, partcB_in_ggaa(X1, X3, X4, X5))
partcB_in_ggaa(X1, [], [], []) → partcB_out_ggaa(X1, [], [], [])
U43_ggaa(X1, X2, X3, X4, X5, partcB_out_ggaa(X1, X3, X4, X5)) → partcB_out_ggaa(X1, .(X2, X3), X4, .(X2, X5))
U41_ggaa(X1, X2, X3, X4, X5, partcB_out_ggaa(X1, X3, X4, X5)) → partcB_out_ggaa(X1, .(X2, X3), .(X2, X4), X5)
qscF_in_ga(.(X1, X2), X3) → U56_ga(X1, X2, X3, partcB_in_ggaa(X1, X2, X4, X5))
U56_ga(X1, X2, X3, partcB_out_ggaa(X1, X2, X4, X5)) → U57_ga(X1, X2, X3, X5, qscF_in_ga(X4, X6))
qscF_in_ga([], []) → qscF_out_ga([], [])
U57_ga(X1, X2, X3, X5, qscF_out_ga(X4, X6)) → U58_ga(X1, X2, X3, X6, qscF_in_ga(X5, X7))
U58_ga(X1, X2, X3, X6, qscF_out_ga(X5, X7)) → U59_ga(X1, X2, X3, appcI_in_ggga(X6, X1, X7, X3))
appcI_in_ggga(.(X1, X2), X3, X4, .(X1, X5)) → U60_ggga(X1, X2, X3, X4, X5, appcI_in_ggga(X2, X3, X4, X5))
appcI_in_ggga([], X1, X2, .(X1, X2)) → appcI_out_ggga([], X1, X2, .(X1, X2))
U60_ggga(X1, X2, X3, X4, X5, appcI_out_ggga(X2, X3, X4, X5)) → appcI_out_ggga(.(X1, X2), X3, X4, .(X1, X5))
U59_ga(X1, X2, X3, appcI_out_ggga(X6, X1, X7, X3)) → qscF_out_ga(.(X1, X2), X3)
qscH_in_a([]) → qscH_out_a([])
qscD_in_ga(.(X1, .(X2, X3)), X4) → U45_ga(X1, X2, X3, X4, gtcA_in_gg(X1, X2))
U45_ga(X1, X2, X3, X4, gtcA_out_gg(X1, X2)) → U46_ga(X1, X2, X3, X4, partcB_in_ggaa(X1, X3, X5, X6))
U46_ga(X1, X2, X3, X4, partcB_out_ggaa(X1, X3, X5, X6)) → U47_ga(X1, X2, X3, X4, X6, qscD_in_ga(.(X2, X5), X7))
qscD_in_ga(.(X1, .(X2, X3)), X4) → U49_ga(X1, X2, X3, X4, lecC_in_gg(X1, X2))
U49_ga(X1, X2, X3, X4, lecC_out_gg(X1, X2)) → U50_ga(X1, X2, X3, X4, partcB_in_ggaa(X1, X3, X5, X6))
U50_ga(X1, X2, X3, X4, partcB_out_ggaa(X1, X3, X5, X6)) → U51_ga(X1, X2, X3, X4, X6, qscF_in_ga(X5, X7))
U51_ga(X1, X2, X3, X4, X6, qscF_out_ga(X5, X7)) → U52_ga(X1, X2, X3, X4, qcE_in_gagga(.(X2, X6), X8, X7, X1, X4))
qcE_in_gagga(X1, X2, X3, X4, X5) → U62_gagga(X1, X2, X3, X4, X5, qscF_in_ga(X1, X2))
U62_gagga(X1, X2, X3, X4, X5, qscF_out_ga(X1, X2)) → U63_gagga(X1, X2, X3, X4, X5, appcG_in_ggga(X3, X4, X2, X5))
appcG_in_ggga(.(X1, X2), X3, X4, .(X1, X5)) → U61_ggga(X1, X2, X3, X4, X5, appcG_in_ggga(X2, X3, X4, X5))
appcG_in_ggga([], X1, X2, .(X1, X2)) → appcG_out_ggga([], X1, X2, .(X1, X2))
U61_ggga(X1, X2, X3, X4, X5, appcG_out_ggga(X2, X3, X4, X5)) → appcG_out_ggga(.(X1, X2), X3, X4, .(X1, X5))
U63_gagga(X1, X2, X3, X4, X5, appcG_out_ggga(X3, X4, X2, X5)) → qcE_out_gagga(X1, X2, X3, X4, X5)
U52_ga(X1, X2, X3, X4, qcE_out_gagga(.(X2, X6), X8, X7, X1, X4)) → qscD_out_ga(.(X1, .(X2, X3)), X4)
qscD_in_ga(.(X1, []), X2) → U53_ga(X1, X2, qscH_in_a(X3))
U53_ga(X1, X2, qscH_out_a(X3)) → U54_ga(X1, X2, X3, qscH_in_a(X4))
U54_ga(X1, X2, X3, qscH_out_a(X4)) → U55_ga(X1, X2, appcG_in_ggga(X3, X1, X4, X2))
U55_ga(X1, X2, appcG_out_ggga(X3, X1, X4, X2)) → qscD_out_ga(.(X1, []), X2)
qscD_in_ga([], []) → qscD_out_ga([], [])
U47_ga(X1, X2, X3, X4, X6, qscD_out_ga(.(X2, X5), X7)) → U48_ga(X1, X2, X3, X4, qcE_in_gagga(X6, X8, X7, X1, X4))
U48_ga(X1, X2, X3, X4, qcE_out_gagga(X6, X8, X7, X1, X4)) → qscD_out_ga(.(X1, .(X2, X3)), X4)
QSF_IN_GA(.(X1, X2), X3) → U10_GA(X1, X2, X3, partcB_in_ggaa(X1, X2, X4, X5))
U10_GA(X1, X2, X3, partcB_out_ggaa(X1, X2, X4, X5)) → QSF_IN_GA(X4, X6)
U10_GA(X1, X2, X3, partcB_out_ggaa(X1, X2, X4, X5)) → U12_GA(X1, X2, X3, X5, qscF_in_ga(X4, X6))
U12_GA(X1, X2, X3, X5, qscF_out_ga(X4, X6)) → QSF_IN_GA(X5, X7)
partcB_in_ggaa(X1, .(X2, X3), .(X2, X4), X5) → U40_ggaa(X1, X2, X3, X4, X5, gtcA_in_gg(X1, X2))
partcB_in_ggaa(X1, .(X2, X3), X4, .(X2, X5)) → U42_ggaa(X1, X2, X3, X4, X5, lecC_in_gg(X1, X2))
partcB_in_ggaa(X1, [], [], []) → partcB_out_ggaa(X1, [], [], [])
qscF_in_ga(.(X1, X2), X3) → U56_ga(X1, X2, X3, partcB_in_ggaa(X1, X2, X4, X5))
qscF_in_ga([], []) → qscF_out_ga([], [])
U40_ggaa(X1, X2, X3, X4, X5, gtcA_out_gg(X1, X2)) → U41_ggaa(X1, X2, X3, X4, X5, partcB_in_ggaa(X1, X3, X4, X5))
U42_ggaa(X1, X2, X3, X4, X5, lecC_out_gg(X1, X2)) → U43_ggaa(X1, X2, X3, X4, X5, partcB_in_ggaa(X1, X3, X4, X5))
U56_ga(X1, X2, X3, partcB_out_ggaa(X1, X2, X4, X5)) → U57_ga(X1, X2, X3, X5, qscF_in_ga(X4, X6))
gtcA_in_gg(s(X1), s(X2)) → U39_gg(X1, X2, gtcA_in_gg(X1, X2))
gtcA_in_gg(s(0), 0) → gtcA_out_gg(s(0), 0)
U41_ggaa(X1, X2, X3, X4, X5, partcB_out_ggaa(X1, X3, X4, X5)) → partcB_out_ggaa(X1, .(X2, X3), .(X2, X4), X5)
lecC_in_gg(s(X1), s(X2)) → U44_gg(X1, X2, lecC_in_gg(X1, X2))
lecC_in_gg(0, s(0)) → lecC_out_gg(0, s(0))
lecC_in_gg(0, 0) → lecC_out_gg(0, 0)
U43_ggaa(X1, X2, X3, X4, X5, partcB_out_ggaa(X1, X3, X4, X5)) → partcB_out_ggaa(X1, .(X2, X3), X4, .(X2, X5))
U57_ga(X1, X2, X3, X5, qscF_out_ga(X4, X6)) → U58_ga(X1, X2, X3, X6, qscF_in_ga(X5, X7))
U39_gg(X1, X2, gtcA_out_gg(X1, X2)) → gtcA_out_gg(s(X1), s(X2))
U44_gg(X1, X2, lecC_out_gg(X1, X2)) → lecC_out_gg(s(X1), s(X2))
U58_ga(X1, X2, X3, X6, qscF_out_ga(X5, X7)) → U59_ga(X1, X2, X3, appcI_in_ggga(X6, X1, X7, X3))
U59_ga(X1, X2, X3, appcI_out_ggga(X6, X1, X7, X3)) → qscF_out_ga(.(X1, X2), X3)
appcI_in_ggga(.(X1, X2), X3, X4, .(X1, X5)) → U60_ggga(X1, X2, X3, X4, X5, appcI_in_ggga(X2, X3, X4, X5))
appcI_in_ggga([], X1, X2, .(X1, X2)) → appcI_out_ggga([], X1, X2, .(X1, X2))
U60_ggga(X1, X2, X3, X4, X5, appcI_out_ggga(X2, X3, X4, X5)) → appcI_out_ggga(.(X1, X2), X3, X4, .(X1, X5))
QSF_IN_GA(.(X1, X2)) → U10_GA(X1, X2, partcB_in_ggaa(X1, X2))
U10_GA(X1, X2, partcB_out_ggaa(X1, X2, X4, X5)) → QSF_IN_GA(X4)
U10_GA(X1, X2, partcB_out_ggaa(X1, X2, X4, X5)) → U12_GA(X1, X2, X5, qscF_in_ga(X4))
U12_GA(X1, X2, X5, qscF_out_ga(X4, X6)) → QSF_IN_GA(X5)
partcB_in_ggaa(X1, .(X2, X3)) → U40_ggaa(X1, X2, X3, gtcA_in_gg(X1, X2))
partcB_in_ggaa(X1, .(X2, X3)) → U42_ggaa(X1, X2, X3, lecC_in_gg(X1, X2))
partcB_in_ggaa(X1, []) → partcB_out_ggaa(X1, [], [], [])
qscF_in_ga(.(X1, X2)) → U56_ga(X1, X2, partcB_in_ggaa(X1, X2))
qscF_in_ga([]) → qscF_out_ga([], [])
U40_ggaa(X1, X2, X3, gtcA_out_gg(X1, X2)) → U41_ggaa(X1, X2, X3, partcB_in_ggaa(X1, X3))
U42_ggaa(X1, X2, X3, lecC_out_gg(X1, X2)) → U43_ggaa(X1, X2, X3, partcB_in_ggaa(X1, X3))
U56_ga(X1, X2, partcB_out_ggaa(X1, X2, X4, X5)) → U57_ga(X1, X2, X5, qscF_in_ga(X4))
gtcA_in_gg(s(X1), s(X2)) → U39_gg(X1, X2, gtcA_in_gg(X1, X2))
gtcA_in_gg(s(0), 0) → gtcA_out_gg(s(0), 0)
U41_ggaa(X1, X2, X3, partcB_out_ggaa(X1, X3, X4, X5)) → partcB_out_ggaa(X1, .(X2, X3), .(X2, X4), X5)
lecC_in_gg(s(X1), s(X2)) → U44_gg(X1, X2, lecC_in_gg(X1, X2))
lecC_in_gg(0, s(0)) → lecC_out_gg(0, s(0))
lecC_in_gg(0, 0) → lecC_out_gg(0, 0)
U43_ggaa(X1, X2, X3, partcB_out_ggaa(X1, X3, X4, X5)) → partcB_out_ggaa(X1, .(X2, X3), X4, .(X2, X5))
U57_ga(X1, X2, X5, qscF_out_ga(X4, X6)) → U58_ga(X1, X2, X6, qscF_in_ga(X5))
U39_gg(X1, X2, gtcA_out_gg(X1, X2)) → gtcA_out_gg(s(X1), s(X2))
U44_gg(X1, X2, lecC_out_gg(X1, X2)) → lecC_out_gg(s(X1), s(X2))
U58_ga(X1, X2, X6, qscF_out_ga(X5, X7)) → U59_ga(X1, X2, appcI_in_ggga(X6, X1, X7))
U59_ga(X1, X2, appcI_out_ggga(X6, X1, X7, X3)) → qscF_out_ga(.(X1, X2), X3)
appcI_in_ggga(.(X1, X2), X3, X4) → U60_ggga(X1, X2, X3, X4, appcI_in_ggga(X2, X3, X4))
appcI_in_ggga([], X1, X2) → appcI_out_ggga([], X1, X2, .(X1, X2))
U60_ggga(X1, X2, X3, X4, appcI_out_ggga(X2, X3, X4, X5)) → appcI_out_ggga(.(X1, X2), X3, X4, .(X1, X5))
partcB_in_ggaa(x0, x1)
qscF_in_ga(x0)
U40_ggaa(x0, x1, x2, x3)
U42_ggaa(x0, x1, x2, x3)
U56_ga(x0, x1, x2)
gtcA_in_gg(x0, x1)
U41_ggaa(x0, x1, x2, x3)
lecC_in_gg(x0, x1)
U43_ggaa(x0, x1, x2, x3)
U57_ga(x0, x1, x2, x3)
U39_gg(x0, x1, x2)
U44_gg(x0, x1, x2)
U58_ga(x0, x1, x2, x3)
U59_ga(x0, x1, x2)
appcI_in_ggga(x0, x1, x2)
U60_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.
QSF_IN_GA(.(X1, X2)) → U10_GA(X1, X2, partcB_in_ggaa(X1, X2))
POL(.(x1, x2)) = 1 + x2
POL(0) = 0
POL(QSF_IN_GA(x1)) = x1
POL(U10_GA(x1, x2, x3)) = x3
POL(U12_GA(x1, x2, x3, x4)) = x3
POL(U39_gg(x1, x2, x3)) = 0
POL(U40_ggaa(x1, x2, x3, x4)) = 1 + x3
POL(U41_ggaa(x1, x2, x3, x4)) = 1 + x4
POL(U42_ggaa(x1, x2, x3, x4)) = 1 + x3
POL(U43_ggaa(x1, x2, x3, x4)) = 1 + x4
POL(U44_gg(x1, x2, x3)) = 0
POL(U56_ga(x1, x2, x3)) = 0
POL(U57_ga(x1, x2, x3, x4)) = 0
POL(U58_ga(x1, x2, x3, x4)) = 0
POL(U59_ga(x1, x2, x3)) = 0
POL(U60_ggga(x1, x2, x3, x4, x5)) = 0
POL([]) = 0
POL(appcI_in_ggga(x1, x2, x3)) = 0
POL(appcI_out_ggga(x1, x2, x3, x4)) = 0
POL(gtcA_in_gg(x1, x2)) = 0
POL(gtcA_out_gg(x1, x2)) = 0
POL(lecC_in_gg(x1, x2)) = 1
POL(lecC_out_gg(x1, x2)) = 0
POL(partcB_in_ggaa(x1, x2)) = x2
POL(partcB_out_ggaa(x1, x2, x3, x4)) = x3 + x4
POL(qscF_in_ga(x1)) = 0
POL(qscF_out_ga(x1, x2)) = 0
POL(s(x1)) = 0
partcB_in_ggaa(X1, .(X2, X3)) → U40_ggaa(X1, X2, X3, gtcA_in_gg(X1, X2))
partcB_in_ggaa(X1, .(X2, X3)) → U42_ggaa(X1, X2, X3, lecC_in_gg(X1, X2))
partcB_in_ggaa(X1, []) → partcB_out_ggaa(X1, [], [], [])
U40_ggaa(X1, X2, X3, gtcA_out_gg(X1, X2)) → U41_ggaa(X1, X2, X3, partcB_in_ggaa(X1, X3))
U41_ggaa(X1, X2, X3, partcB_out_ggaa(X1, X3, X4, X5)) → partcB_out_ggaa(X1, .(X2, X3), .(X2, X4), X5)
U42_ggaa(X1, X2, X3, lecC_out_gg(X1, X2)) → U43_ggaa(X1, X2, X3, partcB_in_ggaa(X1, X3))
U43_ggaa(X1, X2, X3, partcB_out_ggaa(X1, X3, X4, X5)) → partcB_out_ggaa(X1, .(X2, X3), X4, .(X2, X5))
U10_GA(X1, X2, partcB_out_ggaa(X1, X2, X4, X5)) → QSF_IN_GA(X4)
U10_GA(X1, X2, partcB_out_ggaa(X1, X2, X4, X5)) → U12_GA(X1, X2, X5, qscF_in_ga(X4))
U12_GA(X1, X2, X5, qscF_out_ga(X4, X6)) → QSF_IN_GA(X5)
partcB_in_ggaa(X1, .(X2, X3)) → U40_ggaa(X1, X2, X3, gtcA_in_gg(X1, X2))
partcB_in_ggaa(X1, .(X2, X3)) → U42_ggaa(X1, X2, X3, lecC_in_gg(X1, X2))
partcB_in_ggaa(X1, []) → partcB_out_ggaa(X1, [], [], [])
qscF_in_ga(.(X1, X2)) → U56_ga(X1, X2, partcB_in_ggaa(X1, X2))
qscF_in_ga([]) → qscF_out_ga([], [])
U40_ggaa(X1, X2, X3, gtcA_out_gg(X1, X2)) → U41_ggaa(X1, X2, X3, partcB_in_ggaa(X1, X3))
U42_ggaa(X1, X2, X3, lecC_out_gg(X1, X2)) → U43_ggaa(X1, X2, X3, partcB_in_ggaa(X1, X3))
U56_ga(X1, X2, partcB_out_ggaa(X1, X2, X4, X5)) → U57_ga(X1, X2, X5, qscF_in_ga(X4))
gtcA_in_gg(s(X1), s(X2)) → U39_gg(X1, X2, gtcA_in_gg(X1, X2))
gtcA_in_gg(s(0), 0) → gtcA_out_gg(s(0), 0)
U41_ggaa(X1, X2, X3, partcB_out_ggaa(X1, X3, X4, X5)) → partcB_out_ggaa(X1, .(X2, X3), .(X2, X4), X5)
lecC_in_gg(s(X1), s(X2)) → U44_gg(X1, X2, lecC_in_gg(X1, X2))
lecC_in_gg(0, s(0)) → lecC_out_gg(0, s(0))
lecC_in_gg(0, 0) → lecC_out_gg(0, 0)
U43_ggaa(X1, X2, X3, partcB_out_ggaa(X1, X3, X4, X5)) → partcB_out_ggaa(X1, .(X2, X3), X4, .(X2, X5))
U57_ga(X1, X2, X5, qscF_out_ga(X4, X6)) → U58_ga(X1, X2, X6, qscF_in_ga(X5))
U39_gg(X1, X2, gtcA_out_gg(X1, X2)) → gtcA_out_gg(s(X1), s(X2))
U44_gg(X1, X2, lecC_out_gg(X1, X2)) → lecC_out_gg(s(X1), s(X2))
U58_ga(X1, X2, X6, qscF_out_ga(X5, X7)) → U59_ga(X1, X2, appcI_in_ggga(X6, X1, X7))
U59_ga(X1, X2, appcI_out_ggga(X6, X1, X7, X3)) → qscF_out_ga(.(X1, X2), X3)
appcI_in_ggga(.(X1, X2), X3, X4) → U60_ggga(X1, X2, X3, X4, appcI_in_ggga(X2, X3, X4))
appcI_in_ggga([], X1, X2) → appcI_out_ggga([], X1, X2, .(X1, X2))
U60_ggga(X1, X2, X3, X4, appcI_out_ggga(X2, X3, X4, X5)) → appcI_out_ggga(.(X1, X2), X3, X4, .(X1, X5))
partcB_in_ggaa(x0, x1)
qscF_in_ga(x0)
U40_ggaa(x0, x1, x2, x3)
U42_ggaa(x0, x1, x2, x3)
U56_ga(x0, x1, x2)
gtcA_in_gg(x0, x1)
U41_ggaa(x0, x1, x2, x3)
lecC_in_gg(x0, x1)
U43_ggaa(x0, x1, x2, x3)
U57_ga(x0, x1, x2, x3)
U39_gg(x0, x1, x2)
U44_gg(x0, x1, x2)
U58_ga(x0, x1, x2, x3)
U59_ga(x0, x1, x2)
appcI_in_ggga(x0, x1, x2)
U60_ggga(x0, x1, x2, x3, x4)
QSD_IN_GA(.(X1, .(X2, X3)), X4) → U22_GA(X1, X2, X3, X4, gtcA_in_gg(X1, X2))
U22_GA(X1, X2, X3, X4, gtcA_out_gg(X1, X2)) → U24_GA(X1, X2, X3, X4, partcB_in_ggaa(X1, X3, X5, X6))
U24_GA(X1, X2, X3, X4, partcB_out_ggaa(X1, X3, X5, X6)) → QSD_IN_GA(.(X2, X5), X7)
gtcA_in_gg(s(X1), s(X2)) → U39_gg(X1, X2, gtcA_in_gg(X1, X2))
gtcA_in_gg(s(0), 0) → gtcA_out_gg(s(0), 0)
U39_gg(X1, X2, gtcA_out_gg(X1, X2)) → gtcA_out_gg(s(X1), s(X2))
lecC_in_gg(s(X1), s(X2)) → U44_gg(X1, X2, lecC_in_gg(X1, X2))
lecC_in_gg(0, s(0)) → lecC_out_gg(0, s(0))
lecC_in_gg(0, 0) → lecC_out_gg(0, 0)
U44_gg(X1, X2, lecC_out_gg(X1, X2)) → lecC_out_gg(s(X1), s(X2))
partcB_in_ggaa(X1, .(X2, X3), .(X2, X4), X5) → U40_ggaa(X1, X2, X3, X4, X5, gtcA_in_gg(X1, X2))
U40_ggaa(X1, X2, X3, X4, X5, gtcA_out_gg(X1, X2)) → U41_ggaa(X1, X2, X3, X4, X5, partcB_in_ggaa(X1, X3, X4, X5))
partcB_in_ggaa(X1, .(X2, X3), X4, .(X2, X5)) → U42_ggaa(X1, X2, X3, X4, X5, lecC_in_gg(X1, X2))
U42_ggaa(X1, X2, X3, X4, X5, lecC_out_gg(X1, X2)) → U43_ggaa(X1, X2, X3, X4, X5, partcB_in_ggaa(X1, X3, X4, X5))
partcB_in_ggaa(X1, [], [], []) → partcB_out_ggaa(X1, [], [], [])
U43_ggaa(X1, X2, X3, X4, X5, partcB_out_ggaa(X1, X3, X4, X5)) → partcB_out_ggaa(X1, .(X2, X3), X4, .(X2, X5))
U41_ggaa(X1, X2, X3, X4, X5, partcB_out_ggaa(X1, X3, X4, X5)) → partcB_out_ggaa(X1, .(X2, X3), .(X2, X4), X5)
qscF_in_ga(.(X1, X2), X3) → U56_ga(X1, X2, X3, partcB_in_ggaa(X1, X2, X4, X5))
U56_ga(X1, X2, X3, partcB_out_ggaa(X1, X2, X4, X5)) → U57_ga(X1, X2, X3, X5, qscF_in_ga(X4, X6))
qscF_in_ga([], []) → qscF_out_ga([], [])
U57_ga(X1, X2, X3, X5, qscF_out_ga(X4, X6)) → U58_ga(X1, X2, X3, X6, qscF_in_ga(X5, X7))
U58_ga(X1, X2, X3, X6, qscF_out_ga(X5, X7)) → U59_ga(X1, X2, X3, appcI_in_ggga(X6, X1, X7, X3))
appcI_in_ggga(.(X1, X2), X3, X4, .(X1, X5)) → U60_ggga(X1, X2, X3, X4, X5, appcI_in_ggga(X2, X3, X4, X5))
appcI_in_ggga([], X1, X2, .(X1, X2)) → appcI_out_ggga([], X1, X2, .(X1, X2))
U60_ggga(X1, X2, X3, X4, X5, appcI_out_ggga(X2, X3, X4, X5)) → appcI_out_ggga(.(X1, X2), X3, X4, .(X1, X5))
U59_ga(X1, X2, X3, appcI_out_ggga(X6, X1, X7, X3)) → qscF_out_ga(.(X1, X2), X3)
qscH_in_a([]) → qscH_out_a([])
qscD_in_ga(.(X1, .(X2, X3)), X4) → U45_ga(X1, X2, X3, X4, gtcA_in_gg(X1, X2))
U45_ga(X1, X2, X3, X4, gtcA_out_gg(X1, X2)) → U46_ga(X1, X2, X3, X4, partcB_in_ggaa(X1, X3, X5, X6))
U46_ga(X1, X2, X3, X4, partcB_out_ggaa(X1, X3, X5, X6)) → U47_ga(X1, X2, X3, X4, X6, qscD_in_ga(.(X2, X5), X7))
qscD_in_ga(.(X1, .(X2, X3)), X4) → U49_ga(X1, X2, X3, X4, lecC_in_gg(X1, X2))
U49_ga(X1, X2, X3, X4, lecC_out_gg(X1, X2)) → U50_ga(X1, X2, X3, X4, partcB_in_ggaa(X1, X3, X5, X6))
U50_ga(X1, X2, X3, X4, partcB_out_ggaa(X1, X3, X5, X6)) → U51_ga(X1, X2, X3, X4, X6, qscF_in_ga(X5, X7))
U51_ga(X1, X2, X3, X4, X6, qscF_out_ga(X5, X7)) → U52_ga(X1, X2, X3, X4, qcE_in_gagga(.(X2, X6), X8, X7, X1, X4))
qcE_in_gagga(X1, X2, X3, X4, X5) → U62_gagga(X1, X2, X3, X4, X5, qscF_in_ga(X1, X2))
U62_gagga(X1, X2, X3, X4, X5, qscF_out_ga(X1, X2)) → U63_gagga(X1, X2, X3, X4, X5, appcG_in_ggga(X3, X4, X2, X5))
appcG_in_ggga(.(X1, X2), X3, X4, .(X1, X5)) → U61_ggga(X1, X2, X3, X4, X5, appcG_in_ggga(X2, X3, X4, X5))
appcG_in_ggga([], X1, X2, .(X1, X2)) → appcG_out_ggga([], X1, X2, .(X1, X2))
U61_ggga(X1, X2, X3, X4, X5, appcG_out_ggga(X2, X3, X4, X5)) → appcG_out_ggga(.(X1, X2), X3, X4, .(X1, X5))
U63_gagga(X1, X2, X3, X4, X5, appcG_out_ggga(X3, X4, X2, X5)) → qcE_out_gagga(X1, X2, X3, X4, X5)
U52_ga(X1, X2, X3, X4, qcE_out_gagga(.(X2, X6), X8, X7, X1, X4)) → qscD_out_ga(.(X1, .(X2, X3)), X4)
qscD_in_ga(.(X1, []), X2) → U53_ga(X1, X2, qscH_in_a(X3))
U53_ga(X1, X2, qscH_out_a(X3)) → U54_ga(X1, X2, X3, qscH_in_a(X4))
U54_ga(X1, X2, X3, qscH_out_a(X4)) → U55_ga(X1, X2, appcG_in_ggga(X3, X1, X4, X2))
U55_ga(X1, X2, appcG_out_ggga(X3, X1, X4, X2)) → qscD_out_ga(.(X1, []), X2)
qscD_in_ga([], []) → qscD_out_ga([], [])
U47_ga(X1, X2, X3, X4, X6, qscD_out_ga(.(X2, X5), X7)) → U48_ga(X1, X2, X3, X4, qcE_in_gagga(X6, X8, X7, X1, X4))
U48_ga(X1, X2, X3, X4, qcE_out_gagga(X6, X8, X7, X1, X4)) → qscD_out_ga(.(X1, .(X2, X3)), X4)
QSD_IN_GA(.(X1, .(X2, X3)), X4) → U22_GA(X1, X2, X3, X4, gtcA_in_gg(X1, X2))
U22_GA(X1, X2, X3, X4, gtcA_out_gg(X1, X2)) → U24_GA(X1, X2, X3, X4, partcB_in_ggaa(X1, X3, X5, X6))
U24_GA(X1, X2, X3, X4, partcB_out_ggaa(X1, X3, X5, X6)) → QSD_IN_GA(.(X2, X5), X7)
gtcA_in_gg(s(X1), s(X2)) → U39_gg(X1, X2, gtcA_in_gg(X1, X2))
gtcA_in_gg(s(0), 0) → gtcA_out_gg(s(0), 0)
partcB_in_ggaa(X1, .(X2, X3), .(X2, X4), X5) → U40_ggaa(X1, X2, X3, X4, X5, gtcA_in_gg(X1, X2))
partcB_in_ggaa(X1, .(X2, X3), X4, .(X2, X5)) → U42_ggaa(X1, X2, X3, X4, X5, lecC_in_gg(X1, X2))
partcB_in_ggaa(X1, [], [], []) → partcB_out_ggaa(X1, [], [], [])
U39_gg(X1, X2, gtcA_out_gg(X1, X2)) → gtcA_out_gg(s(X1), s(X2))
U40_ggaa(X1, X2, X3, X4, X5, gtcA_out_gg(X1, X2)) → U41_ggaa(X1, X2, X3, X4, X5, partcB_in_ggaa(X1, X3, X4, X5))
U42_ggaa(X1, X2, X3, X4, X5, lecC_out_gg(X1, X2)) → U43_ggaa(X1, X2, X3, X4, X5, partcB_in_ggaa(X1, X3, X4, X5))
U41_ggaa(X1, X2, X3, X4, X5, partcB_out_ggaa(X1, X3, X4, X5)) → partcB_out_ggaa(X1, .(X2, X3), .(X2, X4), X5)
lecC_in_gg(s(X1), s(X2)) → U44_gg(X1, X2, lecC_in_gg(X1, X2))
lecC_in_gg(0, s(0)) → lecC_out_gg(0, s(0))
lecC_in_gg(0, 0) → lecC_out_gg(0, 0)
U43_ggaa(X1, X2, X3, X4, X5, partcB_out_ggaa(X1, X3, X4, X5)) → partcB_out_ggaa(X1, .(X2, X3), X4, .(X2, X5))
U44_gg(X1, X2, lecC_out_gg(X1, X2)) → lecC_out_gg(s(X1), s(X2))
QSD_IN_GA(.(X1, .(X2, X3))) → U22_GA(X1, X2, X3, gtcA_in_gg(X1, X2))
U22_GA(X1, X2, X3, gtcA_out_gg(X1, X2)) → U24_GA(X1, X2, X3, partcB_in_ggaa(X1, X3))
U24_GA(X1, X2, X3, partcB_out_ggaa(X1, X3, X5, X6)) → QSD_IN_GA(.(X2, X5))
gtcA_in_gg(s(X1), s(X2)) → U39_gg(X1, X2, gtcA_in_gg(X1, X2))
gtcA_in_gg(s(0), 0) → gtcA_out_gg(s(0), 0)
partcB_in_ggaa(X1, .(X2, X3)) → U40_ggaa(X1, X2, X3, gtcA_in_gg(X1, X2))
partcB_in_ggaa(X1, .(X2, X3)) → U42_ggaa(X1, X2, X3, lecC_in_gg(X1, X2))
partcB_in_ggaa(X1, []) → partcB_out_ggaa(X1, [], [], [])
U39_gg(X1, X2, gtcA_out_gg(X1, X2)) → gtcA_out_gg(s(X1), s(X2))
U40_ggaa(X1, X2, X3, gtcA_out_gg(X1, X2)) → U41_ggaa(X1, X2, X3, partcB_in_ggaa(X1, X3))
U42_ggaa(X1, X2, X3, lecC_out_gg(X1, X2)) → U43_ggaa(X1, X2, X3, partcB_in_ggaa(X1, X3))
U41_ggaa(X1, X2, X3, partcB_out_ggaa(X1, X3, X4, X5)) → partcB_out_ggaa(X1, .(X2, X3), .(X2, X4), X5)
lecC_in_gg(s(X1), s(X2)) → U44_gg(X1, X2, lecC_in_gg(X1, X2))
lecC_in_gg(0, s(0)) → lecC_out_gg(0, s(0))
lecC_in_gg(0, 0) → lecC_out_gg(0, 0)
U43_ggaa(X1, X2, X3, partcB_out_ggaa(X1, X3, X4, X5)) → partcB_out_ggaa(X1, .(X2, X3), X4, .(X2, X5))
U44_gg(X1, X2, lecC_out_gg(X1, X2)) → lecC_out_gg(s(X1), s(X2))
gtcA_in_gg(x0, x1)
partcB_in_ggaa(x0, x1)
U39_gg(x0, x1, x2)
U40_ggaa(x0, x1, x2, x3)
U42_ggaa(x0, x1, x2, x3)
U41_ggaa(x0, x1, x2, x3)
lecC_in_gg(x0, x1)
U43_ggaa(x0, x1, x2, x3)
U44_gg(x0, x1, x2)
QSD_IN_GA(.(X1, .(X2, X3))) → U22_GA(X1, X2, X3, gtcA_in_gg(X1, X2))
U22_GA(X1, X2, X3, gtcA_out_gg(X1, X2)) → U24_GA(X1, X2, X3, partcB_in_ggaa(X1, X3))
POL(.(x1, x2)) = x1
POL(0) = 0
POL(QSD_IN_GA(x1)) = 2 + 2·x1
POL(U22_GA(x1, x2, x3, x4)) = 2·x4
POL(U24_GA(x1, x2, x3, x4)) = 2 + 2·x2
POL(U39_gg(x1, x2, x3)) = 2 + 2·x3
POL(U40_ggaa(x1, x2, x3, x4)) = x1
POL(U41_ggaa(x1, x2, x3, x4)) = x1
POL(U42_ggaa(x1, x2, x3, x4)) = x1
POL(U43_ggaa(x1, x2, x3, x4)) = 0
POL(U44_gg(x1, x2, x3)) = x1
POL([]) = 0
POL(gtcA_in_gg(x1, x2)) = x1
POL(gtcA_out_gg(x1, x2)) = 2 + 2·x2
POL(lecC_in_gg(x1, x2)) = 2·x1
POL(lecC_out_gg(x1, x2)) = 0
POL(partcB_in_ggaa(x1, x2)) = 1 + x1
POL(partcB_out_ggaa(x1, x2, x3, x4)) = 0
POL(s(x1)) = 2 + 2·x1
U24_GA(X1, X2, X3, partcB_out_ggaa(X1, X3, X5, X6)) → QSD_IN_GA(.(X2, X5))
gtcA_in_gg(s(X1), s(X2)) → U39_gg(X1, X2, gtcA_in_gg(X1, X2))
gtcA_in_gg(s(0), 0) → gtcA_out_gg(s(0), 0)
partcB_in_ggaa(X1, .(X2, X3)) → U40_ggaa(X1, X2, X3, gtcA_in_gg(X1, X2))
partcB_in_ggaa(X1, .(X2, X3)) → U42_ggaa(X1, X2, X3, lecC_in_gg(X1, X2))
partcB_in_ggaa(X1, []) → partcB_out_ggaa(X1, [], [], [])
U39_gg(X1, X2, gtcA_out_gg(X1, X2)) → gtcA_out_gg(s(X1), s(X2))
U40_ggaa(X1, X2, X3, gtcA_out_gg(X1, X2)) → U41_ggaa(X1, X2, X3, partcB_in_ggaa(X1, X3))
U42_ggaa(X1, X2, X3, lecC_out_gg(X1, X2)) → U43_ggaa(X1, X2, X3, partcB_in_ggaa(X1, X3))
U41_ggaa(X1, X2, X3, partcB_out_ggaa(X1, X3, X4, X5)) → partcB_out_ggaa(X1, .(X2, X3), .(X2, X4), X5)
lecC_in_gg(s(X1), s(X2)) → U44_gg(X1, X2, lecC_in_gg(X1, X2))
lecC_in_gg(0, s(0)) → lecC_out_gg(0, s(0))
lecC_in_gg(0, 0) → lecC_out_gg(0, 0)
U43_ggaa(X1, X2, X3, partcB_out_ggaa(X1, X3, X4, X5)) → partcB_out_ggaa(X1, .(X2, X3), X4, .(X2, X5))
U44_gg(X1, X2, lecC_out_gg(X1, X2)) → lecC_out_gg(s(X1), s(X2))
gtcA_in_gg(x0, x1)
partcB_in_ggaa(x0, x1)
U39_gg(x0, x1, x2)
U40_ggaa(x0, x1, x2, x3)
U42_ggaa(x0, x1, x2, x3)
U41_ggaa(x0, x1, x2, x3)
lecC_in_gg(x0, x1)
U43_ggaa(x0, x1, x2, x3)
U44_gg(x0, x1, x2)