0 Prolog
↳1 PrologToPiTRSViaGraphTransformerProof (⇒, 549 ms)
↳2 PiTRS
↳3 DependencyPairsProof (⇔, 1140 ms)
↳4 PiDP
↳5 DependencyGraphProof (⇔, 110 ms)
↳6 AND
↳7 PiDP
↳8 UsableRulesProof (⇔, 0 ms)
↳9 PiDP
↳10 PiDPToQDPProof (⇒, 24 ms)
↳11 QDP
↳12 QDPSizeChangeProof (⇔, 0 ms)
↳13 YES
↳14 PiDP
↳15 UsableRulesProof (⇔, 0 ms)
↳16 PiDP
↳17 PiDPToQDPProof (⇒, 0 ms)
↳18 QDP
↳19 QDPSizeChangeProof (⇔, 0 ms)
↳20 YES
↳21 PiDP
↳22 UsableRulesProof (⇔, 0 ms)
↳23 PiDP
↳24 PiDPToQDPProof (⇒, 0 ms)
↳25 QDP
↳26 QDPSizeChangeProof (⇔, 0 ms)
↳27 YES
↳28 PiDP
↳29 UsableRulesProof (⇔, 0 ms)
↳30 PiDP
↳31 PiDPToQDPProof (⇒, 0 ms)
↳32 QDP
↳33 QDPSizeChangeProof (⇔, 0 ms)
↳34 YES
↳35 PiDP
↳36 UsableRulesProof (⇔, 0 ms)
↳37 PiDP
↳38 PiDPToQDPProof (⇒, 9 ms)
↳39 QDP
↳40 QDPOrderProof (⇔, 126 ms)
↳41 QDP
↳42 DependencyGraphProof (⇔, 0 ms)
↳43 QDP
↳44 QDPQMonotonicMRRProof (⇔, 278 ms)
↳45 QDP
↳46 QDPOrderProof (⇔, 330 ms)
↳47 QDP
↳48 DependencyGraphProof (⇔, 0 ms)
↳49 TRUE
↳50 PiDP
↳51 UsableRulesProof (⇔, 0 ms)
↳52 PiDP
↳53 PiDPToQDPProof (⇒, 0 ms)
↳54 QDP
↳55 QDPSizeChangeProof (⇔, 0 ms)
↳56 YES
timesA_in_gga(0, T5, 0) → timesA_out_gga(0, T5, 0)
timesA_in_gga(s(0), T21, T23) → U1_gga(T21, T23, pB_in_gaa(T21, X37, T23))
pB_in_gaa(T21, T27, T23) → U16_gaa(T21, T27, T23, timesK_in_ga(T21, T27))
timesK_in_ga(T33, 0) → timesK_out_ga(T33, 0)
U16_gaa(T21, T27, T23, timesK_out_ga(T21, T27)) → U17_gaa(T21, T27, T23, plusD_in_gga(T21, T27, T23))
plusD_in_gga(0, T40, T40) → plusD_out_gga(0, T40, T40)
plusD_in_gga(s(T47), T48, s(T50)) → U3_gga(T47, T48, T50, plusD_in_gga(T47, T48, T50))
U3_gga(T47, T48, T50, plusD_out_gga(T47, T48, T50)) → plusD_out_gga(s(T47), T48, s(T50))
U17_gaa(T21, T27, T23, plusD_out_gga(T21, T27, T23)) → pB_out_gaa(T21, T27, T23)
U1_gga(T21, T23, pB_out_gaa(T21, X37, T23)) → timesA_out_gga(s(0), T21, T23)
timesA_in_gga(s(s(T55)), T10, T12) → U2_gga(T55, T10, T12, pC_in_gaga(T55, X78, T10, T12))
pC_in_gaga(T55, T56, T10, T12) → U18_gaga(T55, T56, T10, T12, evenE_in_ga(T55, T56))
evenE_in_ga(0, true) → evenE_out_ga(0, true)
evenE_in_ga(s(0), false) → evenE_out_ga(s(0), false)
evenE_in_ga(s(s(T59)), X87) → U4_ga(T59, X87, evenE_in_ga(T59, X87))
U4_ga(T59, X87, evenE_out_ga(T59, X87)) → evenE_out_ga(s(s(T59)), X87)
U18_gaga(T55, T56, T10, T12, evenE_out_ga(T55, T56)) → U19_gaga(T55, T56, T10, T12, ifL_in_ggga(T56, T55, T10, T12))
ifL_in_ggga(true, T75, T76, T78) → U9_ggga(T75, T76, T78, pM_in_gagaa(T75, X112, T76, X113, T78))
pM_in_gagaa(T75, T79, T76, X113, T78) → U20_gagaa(T75, T79, T76, X113, T78, halfO_in_ga(T75, T79))
halfO_in_ga(T82, s(X122)) → U11_ga(T82, X122, halfF_in_ga(T82, X122))
halfF_in_ga(0, 0) → halfF_out_ga(0, 0)
halfF_in_ga(s(s(T85)), s(X131)) → U5_ga(T85, X131, halfF_in_ga(T85, X131))
U5_ga(T85, X131, halfF_out_ga(T85, X131)) → halfF_out_ga(s(s(T85)), s(X131))
U11_ga(T82, X122, halfF_out_ga(T82, X122)) → halfO_out_ga(T82, s(X122))
U20_gagaa(T75, T79, T76, X113, T78, halfO_out_ga(T75, T79)) → U21_gagaa(T75, T79, T76, X113, T78, pU_in_ggaa(T79, T76, X113, T78))
pU_in_ggaa(T79, T76, T88, T78) → U22_ggaa(T79, T76, T88, T78, timesG_in_gga(T79, T76, T88))
timesG_in_gga(0, T95, 0) → timesG_out_gga(0, T95, 0)
timesG_in_gga(s(T100), T101, X154) → U6_gga(T100, T101, X154, pH_in_gaga(T100, X153, T101, X154))
pH_in_gaga(T100, T102, T101, X154) → U24_gaga(T100, T102, T101, X154, evenE_in_ga(s(T100), T102))
U24_gaga(T100, T102, T101, X154, evenE_out_ga(s(T100), T102)) → U25_gaga(T100, T102, T101, X154, ifQ_in_ggga(T102, T100, T101, X154))
ifQ_in_ggga(true, T113, T114, X186) → U13_ggga(T113, T114, X186, pR_in_gagaa(T113, X184, T114, X185, X186))
pR_in_gagaa(T113, T115, T114, X185, X186) → U26_gagaa(T113, T115, T114, X185, X186, halfF_in_ga(s(T113), T115))
U26_gagaa(T113, T115, T114, X185, X186, halfF_out_ga(s(T113), T115)) → U27_gagaa(T113, T115, T114, X185, X186, pV_in_ggaa(T115, T114, X185, X186))
pV_in_ggaa(T115, T114, T118, X186) → U28_ggaa(T115, T114, T118, X186, timesG_in_gga(T115, T114, T118))
U28_ggaa(T115, T114, T118, X186, timesG_out_gga(T115, T114, T118)) → U29_ggaa(T115, T114, T118, X186, plusT_in_ga(T118, X186))
plusT_in_ga(0, 0) → plusT_out_ga(0, 0)
plusT_in_ga(s(0), s(s(0))) → plusT_out_ga(s(0), s(s(0)))
plusT_in_ga(s(s(0)), s(s(s(s(0))))) → plusT_out_ga(s(s(0)), s(s(s(s(0)))))
plusT_in_ga(s(s(s(0))), s(s(s(s(s(s(0))))))) → plusT_out_ga(s(s(s(0))), s(s(s(s(s(s(0)))))))
plusT_in_ga(s(s(s(s(0)))), s(s(s(s(s(s(s(s(0))))))))) → plusT_out_ga(s(s(s(s(0)))), s(s(s(s(s(s(s(s(0)))))))))
plusT_in_ga(s(s(s(s(s(0))))), s(s(s(s(s(s(s(s(s(s(0))))))))))) → plusT_out_ga(s(s(s(s(s(0))))), s(s(s(s(s(s(s(s(s(s(0)))))))))))
plusT_in_ga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))) → plusT_out_ga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))
plusT_in_ga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))))) → plusT_out_ga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))))
plusT_in_ga(s(s(s(s(s(s(s(s(T144)))))))), s(s(s(s(s(s(s(s(X342))))))))) → U15_ga(T144, X342, plusI_in_gga(T144, s(s(s(s(s(s(s(T144))))))), X342))
plusI_in_gga(0, T152, s(T152)) → plusI_out_gga(0, T152, s(T152))
plusI_in_gga(s(T157), T158, s(X363)) → U7_gga(T157, T158, X363, plusI_in_gga(T157, T158, X363))
U7_gga(T157, T158, X363, plusI_out_gga(T157, T158, X363)) → plusI_out_gga(s(T157), T158, s(X363))
U15_ga(T144, X342, plusI_out_gga(T144, s(s(s(s(s(s(s(T144))))))), X342)) → plusT_out_ga(s(s(s(s(s(s(s(s(T144)))))))), s(s(s(s(s(s(s(s(X342)))))))))
U29_ggaa(T115, T114, T118, X186, plusT_out_ga(T118, X186)) → pV_out_ggaa(T115, T114, T118, X186)
U27_gagaa(T113, T115, T114, X185, X186, pV_out_ggaa(T115, T114, X185, X186)) → pR_out_gagaa(T113, T115, T114, X185, X186)
U13_ggga(T113, T114, X186, pR_out_gagaa(T113, X184, T114, X185, X186)) → ifQ_out_ggga(true, T113, T114, X186)
ifQ_in_ggga(false, T165, T166, X379) → U14_ggga(T165, T166, X379, pS_in_ggaa(T165, T166, X378, X379))
pS_in_ggaa(T165, T166, T169, X379) → U30_ggaa(T165, T166, T169, X379, timesG_in_gga(T165, T166, T169))
U30_ggaa(T165, T166, T169, X379, timesG_out_gga(T165, T166, T169)) → U31_ggaa(T165, T166, T169, X379, plusJ_in_gga(T166, T169, X379))
plusJ_in_gga(0, T178, T178) → plusJ_out_gga(0, T178, T178)
plusJ_in_gga(s(T183), T184, s(X402)) → U8_gga(T183, T184, X402, plusJ_in_gga(T183, T184, X402))
U8_gga(T183, T184, X402, plusJ_out_gga(T183, T184, X402)) → plusJ_out_gga(s(T183), T184, s(X402))
U31_ggaa(T165, T166, T169, X379, plusJ_out_gga(T166, T169, X379)) → pS_out_ggaa(T165, T166, T169, X379)
U14_ggga(T165, T166, X379, pS_out_ggaa(T165, T166, X378, X379)) → ifQ_out_ggga(false, T165, T166, X379)
U25_gaga(T100, T102, T101, X154, ifQ_out_ggga(T102, T100, T101, X154)) → pH_out_gaga(T100, T102, T101, X154)
U6_gga(T100, T101, X154, pH_out_gaga(T100, X153, T101, X154)) → timesG_out_gga(s(T100), T101, X154)
U22_ggaa(T79, T76, T88, T78, timesG_out_gga(T79, T76, T88)) → U23_ggaa(T79, T76, T88, T78, plusP_in_ga(T88, T78))
plusP_in_ga(0, 0) → plusP_out_ga(0, 0)
plusP_in_ga(s(0), s(s(0))) → plusP_out_ga(s(0), s(s(0)))
plusP_in_ga(s(s(0)), s(s(s(s(0))))) → plusP_out_ga(s(s(0)), s(s(s(s(0)))))
plusP_in_ga(s(s(s(0))), s(s(s(s(s(s(0))))))) → plusP_out_ga(s(s(s(0))), s(s(s(s(s(s(0)))))))
plusP_in_ga(s(s(s(s(0)))), s(s(s(s(s(s(s(s(0))))))))) → plusP_out_ga(s(s(s(s(0)))), s(s(s(s(s(s(s(s(0)))))))))
plusP_in_ga(s(s(s(s(s(0))))), s(s(s(s(s(s(s(s(s(s(0))))))))))) → plusP_out_ga(s(s(s(s(s(0))))), s(s(s(s(s(s(s(s(s(s(0)))))))))))
plusP_in_ga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))) → plusP_out_ga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))
plusP_in_ga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))))) → plusP_out_ga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))))
plusP_in_ga(s(s(s(s(s(s(s(s(T240)))))))), s(s(s(s(s(s(s(s(T242))))))))) → U12_ga(T240, T242, plusD_in_gga(T240, s(s(s(s(s(s(s(s(T240)))))))), T242))
U12_ga(T240, T242, plusD_out_gga(T240, s(s(s(s(s(s(s(s(T240)))))))), T242)) → plusP_out_ga(s(s(s(s(s(s(s(s(T240)))))))), s(s(s(s(s(s(s(s(T242)))))))))
U23_ggaa(T79, T76, T88, T78, plusP_out_ga(T88, T78)) → pU_out_ggaa(T79, T76, T88, T78)
U21_gagaa(T75, T79, T76, X113, T78, pU_out_ggaa(T79, T76, X113, T78)) → pM_out_gagaa(T75, T79, T76, X113, T78)
U9_ggga(T75, T76, T78, pM_out_gagaa(T75, X112, T76, X113, T78)) → ifL_out_ggga(true, T75, T76, T78)
ifL_in_ggga(false, T252, T253, T255) → U10_ggga(T252, T253, T255, pN_in_ggaa(T252, T253, X547, T255))
pN_in_ggaa(T252, T253, T256, T255) → U32_ggaa(T252, T253, T256, T255, timesG_in_gga(s(T252), T253, T256))
U32_ggaa(T252, T253, T256, T255, timesG_out_gga(s(T252), T253, T256)) → U33_ggaa(T252, T253, T256, T255, plusD_in_gga(T253, T256, T255))
U33_ggaa(T252, T253, T256, T255, plusD_out_gga(T253, T256, T255)) → pN_out_ggaa(T252, T253, T256, T255)
U10_ggga(T252, T253, T255, pN_out_ggaa(T252, T253, X547, T255)) → ifL_out_ggga(false, T252, T253, T255)
U19_gaga(T55, T56, T10, T12, ifL_out_ggga(T56, T55, T10, T12)) → pC_out_gaga(T55, T56, T10, T12)
U2_gga(T55, T10, T12, pC_out_gaga(T55, X78, T10, T12)) → timesA_out_gga(s(s(T55)), T10, T12)
TIMESA_IN_GGA(s(0), T21, T23) → U1_GGA(T21, T23, pB_in_gaa(T21, X37, T23))
TIMESA_IN_GGA(s(0), T21, T23) → PB_IN_GAA(T21, X37, T23)
PB_IN_GAA(T21, T27, T23) → U16_GAA(T21, T27, T23, timesK_in_ga(T21, T27))
PB_IN_GAA(T21, T27, T23) → TIMESK_IN_GA(T21, T27)
U16_GAA(T21, T27, T23, timesK_out_ga(T21, T27)) → U17_GAA(T21, T27, T23, plusD_in_gga(T21, T27, T23))
U16_GAA(T21, T27, T23, timesK_out_ga(T21, T27)) → PLUSD_IN_GGA(T21, T27, T23)
PLUSD_IN_GGA(s(T47), T48, s(T50)) → U3_GGA(T47, T48, T50, plusD_in_gga(T47, T48, T50))
PLUSD_IN_GGA(s(T47), T48, s(T50)) → PLUSD_IN_GGA(T47, T48, T50)
TIMESA_IN_GGA(s(s(T55)), T10, T12) → U2_GGA(T55, T10, T12, pC_in_gaga(T55, X78, T10, T12))
TIMESA_IN_GGA(s(s(T55)), T10, T12) → PC_IN_GAGA(T55, X78, T10, T12)
PC_IN_GAGA(T55, T56, T10, T12) → U18_GAGA(T55, T56, T10, T12, evenE_in_ga(T55, T56))
PC_IN_GAGA(T55, T56, T10, T12) → EVENE_IN_GA(T55, T56)
EVENE_IN_GA(s(s(T59)), X87) → U4_GA(T59, X87, evenE_in_ga(T59, X87))
EVENE_IN_GA(s(s(T59)), X87) → EVENE_IN_GA(T59, X87)
U18_GAGA(T55, T56, T10, T12, evenE_out_ga(T55, T56)) → U19_GAGA(T55, T56, T10, T12, ifL_in_ggga(T56, T55, T10, T12))
U18_GAGA(T55, T56, T10, T12, evenE_out_ga(T55, T56)) → IFL_IN_GGGA(T56, T55, T10, T12)
IFL_IN_GGGA(true, T75, T76, T78) → U9_GGGA(T75, T76, T78, pM_in_gagaa(T75, X112, T76, X113, T78))
IFL_IN_GGGA(true, T75, T76, T78) → PM_IN_GAGAA(T75, X112, T76, X113, T78)
PM_IN_GAGAA(T75, T79, T76, X113, T78) → U20_GAGAA(T75, T79, T76, X113, T78, halfO_in_ga(T75, T79))
PM_IN_GAGAA(T75, T79, T76, X113, T78) → HALFO_IN_GA(T75, T79)
HALFO_IN_GA(T82, s(X122)) → U11_GA(T82, X122, halfF_in_ga(T82, X122))
HALFO_IN_GA(T82, s(X122)) → HALFF_IN_GA(T82, X122)
HALFF_IN_GA(s(s(T85)), s(X131)) → U5_GA(T85, X131, halfF_in_ga(T85, X131))
HALFF_IN_GA(s(s(T85)), s(X131)) → HALFF_IN_GA(T85, X131)
U20_GAGAA(T75, T79, T76, X113, T78, halfO_out_ga(T75, T79)) → U21_GAGAA(T75, T79, T76, X113, T78, pU_in_ggaa(T79, T76, X113, T78))
U20_GAGAA(T75, T79, T76, X113, T78, halfO_out_ga(T75, T79)) → PU_IN_GGAA(T79, T76, X113, T78)
PU_IN_GGAA(T79, T76, T88, T78) → U22_GGAA(T79, T76, T88, T78, timesG_in_gga(T79, T76, T88))
PU_IN_GGAA(T79, T76, T88, T78) → TIMESG_IN_GGA(T79, T76, T88)
TIMESG_IN_GGA(s(T100), T101, X154) → U6_GGA(T100, T101, X154, pH_in_gaga(T100, X153, T101, X154))
TIMESG_IN_GGA(s(T100), T101, X154) → PH_IN_GAGA(T100, X153, T101, X154)
PH_IN_GAGA(T100, T102, T101, X154) → U24_GAGA(T100, T102, T101, X154, evenE_in_ga(s(T100), T102))
PH_IN_GAGA(T100, T102, T101, X154) → EVENE_IN_GA(s(T100), T102)
U24_GAGA(T100, T102, T101, X154, evenE_out_ga(s(T100), T102)) → U25_GAGA(T100, T102, T101, X154, ifQ_in_ggga(T102, T100, T101, X154))
U24_GAGA(T100, T102, T101, X154, evenE_out_ga(s(T100), T102)) → IFQ_IN_GGGA(T102, T100, T101, X154)
IFQ_IN_GGGA(true, T113, T114, X186) → U13_GGGA(T113, T114, X186, pR_in_gagaa(T113, X184, T114, X185, X186))
IFQ_IN_GGGA(true, T113, T114, X186) → PR_IN_GAGAA(T113, X184, T114, X185, X186)
PR_IN_GAGAA(T113, T115, T114, X185, X186) → U26_GAGAA(T113, T115, T114, X185, X186, halfF_in_ga(s(T113), T115))
PR_IN_GAGAA(T113, T115, T114, X185, X186) → HALFF_IN_GA(s(T113), T115)
U26_GAGAA(T113, T115, T114, X185, X186, halfF_out_ga(s(T113), T115)) → U27_GAGAA(T113, T115, T114, X185, X186, pV_in_ggaa(T115, T114, X185, X186))
U26_GAGAA(T113, T115, T114, X185, X186, halfF_out_ga(s(T113), T115)) → PV_IN_GGAA(T115, T114, X185, X186)
PV_IN_GGAA(T115, T114, T118, X186) → U28_GGAA(T115, T114, T118, X186, timesG_in_gga(T115, T114, T118))
PV_IN_GGAA(T115, T114, T118, X186) → TIMESG_IN_GGA(T115, T114, T118)
U28_GGAA(T115, T114, T118, X186, timesG_out_gga(T115, T114, T118)) → U29_GGAA(T115, T114, T118, X186, plusT_in_ga(T118, X186))
U28_GGAA(T115, T114, T118, X186, timesG_out_gga(T115, T114, T118)) → PLUST_IN_GA(T118, X186)
PLUST_IN_GA(s(s(s(s(s(s(s(s(T144)))))))), s(s(s(s(s(s(s(s(X342))))))))) → U15_GA(T144, X342, plusI_in_gga(T144, s(s(s(s(s(s(s(T144))))))), X342))
PLUST_IN_GA(s(s(s(s(s(s(s(s(T144)))))))), s(s(s(s(s(s(s(s(X342))))))))) → PLUSI_IN_GGA(T144, s(s(s(s(s(s(s(T144))))))), X342)
PLUSI_IN_GGA(s(T157), T158, s(X363)) → U7_GGA(T157, T158, X363, plusI_in_gga(T157, T158, X363))
PLUSI_IN_GGA(s(T157), T158, s(X363)) → PLUSI_IN_GGA(T157, T158, X363)
IFQ_IN_GGGA(false, T165, T166, X379) → U14_GGGA(T165, T166, X379, pS_in_ggaa(T165, T166, X378, X379))
IFQ_IN_GGGA(false, T165, T166, X379) → PS_IN_GGAA(T165, T166, X378, X379)
PS_IN_GGAA(T165, T166, T169, X379) → U30_GGAA(T165, T166, T169, X379, timesG_in_gga(T165, T166, T169))
PS_IN_GGAA(T165, T166, T169, X379) → TIMESG_IN_GGA(T165, T166, T169)
U30_GGAA(T165, T166, T169, X379, timesG_out_gga(T165, T166, T169)) → U31_GGAA(T165, T166, T169, X379, plusJ_in_gga(T166, T169, X379))
U30_GGAA(T165, T166, T169, X379, timesG_out_gga(T165, T166, T169)) → PLUSJ_IN_GGA(T166, T169, X379)
PLUSJ_IN_GGA(s(T183), T184, s(X402)) → U8_GGA(T183, T184, X402, plusJ_in_gga(T183, T184, X402))
PLUSJ_IN_GGA(s(T183), T184, s(X402)) → PLUSJ_IN_GGA(T183, T184, X402)
U22_GGAA(T79, T76, T88, T78, timesG_out_gga(T79, T76, T88)) → U23_GGAA(T79, T76, T88, T78, plusP_in_ga(T88, T78))
U22_GGAA(T79, T76, T88, T78, timesG_out_gga(T79, T76, T88)) → PLUSP_IN_GA(T88, T78)
PLUSP_IN_GA(s(s(s(s(s(s(s(s(T240)))))))), s(s(s(s(s(s(s(s(T242))))))))) → U12_GA(T240, T242, plusD_in_gga(T240, s(s(s(s(s(s(s(s(T240)))))))), T242))
PLUSP_IN_GA(s(s(s(s(s(s(s(s(T240)))))))), s(s(s(s(s(s(s(s(T242))))))))) → PLUSD_IN_GGA(T240, s(s(s(s(s(s(s(s(T240)))))))), T242)
IFL_IN_GGGA(false, T252, T253, T255) → U10_GGGA(T252, T253, T255, pN_in_ggaa(T252, T253, X547, T255))
IFL_IN_GGGA(false, T252, T253, T255) → PN_IN_GGAA(T252, T253, X547, T255)
PN_IN_GGAA(T252, T253, T256, T255) → U32_GGAA(T252, T253, T256, T255, timesG_in_gga(s(T252), T253, T256))
PN_IN_GGAA(T252, T253, T256, T255) → TIMESG_IN_GGA(s(T252), T253, T256)
U32_GGAA(T252, T253, T256, T255, timesG_out_gga(s(T252), T253, T256)) → U33_GGAA(T252, T253, T256, T255, plusD_in_gga(T253, T256, T255))
U32_GGAA(T252, T253, T256, T255, timesG_out_gga(s(T252), T253, T256)) → PLUSD_IN_GGA(T253, T256, T255)
timesA_in_gga(0, T5, 0) → timesA_out_gga(0, T5, 0)
timesA_in_gga(s(0), T21, T23) → U1_gga(T21, T23, pB_in_gaa(T21, X37, T23))
pB_in_gaa(T21, T27, T23) → U16_gaa(T21, T27, T23, timesK_in_ga(T21, T27))
timesK_in_ga(T33, 0) → timesK_out_ga(T33, 0)
U16_gaa(T21, T27, T23, timesK_out_ga(T21, T27)) → U17_gaa(T21, T27, T23, plusD_in_gga(T21, T27, T23))
plusD_in_gga(0, T40, T40) → plusD_out_gga(0, T40, T40)
plusD_in_gga(s(T47), T48, s(T50)) → U3_gga(T47, T48, T50, plusD_in_gga(T47, T48, T50))
U3_gga(T47, T48, T50, plusD_out_gga(T47, T48, T50)) → plusD_out_gga(s(T47), T48, s(T50))
U17_gaa(T21, T27, T23, plusD_out_gga(T21, T27, T23)) → pB_out_gaa(T21, T27, T23)
U1_gga(T21, T23, pB_out_gaa(T21, X37, T23)) → timesA_out_gga(s(0), T21, T23)
timesA_in_gga(s(s(T55)), T10, T12) → U2_gga(T55, T10, T12, pC_in_gaga(T55, X78, T10, T12))
pC_in_gaga(T55, T56, T10, T12) → U18_gaga(T55, T56, T10, T12, evenE_in_ga(T55, T56))
evenE_in_ga(0, true) → evenE_out_ga(0, true)
evenE_in_ga(s(0), false) → evenE_out_ga(s(0), false)
evenE_in_ga(s(s(T59)), X87) → U4_ga(T59, X87, evenE_in_ga(T59, X87))
U4_ga(T59, X87, evenE_out_ga(T59, X87)) → evenE_out_ga(s(s(T59)), X87)
U18_gaga(T55, T56, T10, T12, evenE_out_ga(T55, T56)) → U19_gaga(T55, T56, T10, T12, ifL_in_ggga(T56, T55, T10, T12))
ifL_in_ggga(true, T75, T76, T78) → U9_ggga(T75, T76, T78, pM_in_gagaa(T75, X112, T76, X113, T78))
pM_in_gagaa(T75, T79, T76, X113, T78) → U20_gagaa(T75, T79, T76, X113, T78, halfO_in_ga(T75, T79))
halfO_in_ga(T82, s(X122)) → U11_ga(T82, X122, halfF_in_ga(T82, X122))
halfF_in_ga(0, 0) → halfF_out_ga(0, 0)
halfF_in_ga(s(s(T85)), s(X131)) → U5_ga(T85, X131, halfF_in_ga(T85, X131))
U5_ga(T85, X131, halfF_out_ga(T85, X131)) → halfF_out_ga(s(s(T85)), s(X131))
U11_ga(T82, X122, halfF_out_ga(T82, X122)) → halfO_out_ga(T82, s(X122))
U20_gagaa(T75, T79, T76, X113, T78, halfO_out_ga(T75, T79)) → U21_gagaa(T75, T79, T76, X113, T78, pU_in_ggaa(T79, T76, X113, T78))
pU_in_ggaa(T79, T76, T88, T78) → U22_ggaa(T79, T76, T88, T78, timesG_in_gga(T79, T76, T88))
timesG_in_gga(0, T95, 0) → timesG_out_gga(0, T95, 0)
timesG_in_gga(s(T100), T101, X154) → U6_gga(T100, T101, X154, pH_in_gaga(T100, X153, T101, X154))
pH_in_gaga(T100, T102, T101, X154) → U24_gaga(T100, T102, T101, X154, evenE_in_ga(s(T100), T102))
U24_gaga(T100, T102, T101, X154, evenE_out_ga(s(T100), T102)) → U25_gaga(T100, T102, T101, X154, ifQ_in_ggga(T102, T100, T101, X154))
ifQ_in_ggga(true, T113, T114, X186) → U13_ggga(T113, T114, X186, pR_in_gagaa(T113, X184, T114, X185, X186))
pR_in_gagaa(T113, T115, T114, X185, X186) → U26_gagaa(T113, T115, T114, X185, X186, halfF_in_ga(s(T113), T115))
U26_gagaa(T113, T115, T114, X185, X186, halfF_out_ga(s(T113), T115)) → U27_gagaa(T113, T115, T114, X185, X186, pV_in_ggaa(T115, T114, X185, X186))
pV_in_ggaa(T115, T114, T118, X186) → U28_ggaa(T115, T114, T118, X186, timesG_in_gga(T115, T114, T118))
U28_ggaa(T115, T114, T118, X186, timesG_out_gga(T115, T114, T118)) → U29_ggaa(T115, T114, T118, X186, plusT_in_ga(T118, X186))
plusT_in_ga(0, 0) → plusT_out_ga(0, 0)
plusT_in_ga(s(0), s(s(0))) → plusT_out_ga(s(0), s(s(0)))
plusT_in_ga(s(s(0)), s(s(s(s(0))))) → plusT_out_ga(s(s(0)), s(s(s(s(0)))))
plusT_in_ga(s(s(s(0))), s(s(s(s(s(s(0))))))) → plusT_out_ga(s(s(s(0))), s(s(s(s(s(s(0)))))))
plusT_in_ga(s(s(s(s(0)))), s(s(s(s(s(s(s(s(0))))))))) → plusT_out_ga(s(s(s(s(0)))), s(s(s(s(s(s(s(s(0)))))))))
plusT_in_ga(s(s(s(s(s(0))))), s(s(s(s(s(s(s(s(s(s(0))))))))))) → plusT_out_ga(s(s(s(s(s(0))))), s(s(s(s(s(s(s(s(s(s(0)))))))))))
plusT_in_ga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))) → plusT_out_ga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))
plusT_in_ga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))))) → plusT_out_ga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))))
plusT_in_ga(s(s(s(s(s(s(s(s(T144)))))))), s(s(s(s(s(s(s(s(X342))))))))) → U15_ga(T144, X342, plusI_in_gga(T144, s(s(s(s(s(s(s(T144))))))), X342))
plusI_in_gga(0, T152, s(T152)) → plusI_out_gga(0, T152, s(T152))
plusI_in_gga(s(T157), T158, s(X363)) → U7_gga(T157, T158, X363, plusI_in_gga(T157, T158, X363))
U7_gga(T157, T158, X363, plusI_out_gga(T157, T158, X363)) → plusI_out_gga(s(T157), T158, s(X363))
U15_ga(T144, X342, plusI_out_gga(T144, s(s(s(s(s(s(s(T144))))))), X342)) → plusT_out_ga(s(s(s(s(s(s(s(s(T144)))))))), s(s(s(s(s(s(s(s(X342)))))))))
U29_ggaa(T115, T114, T118, X186, plusT_out_ga(T118, X186)) → pV_out_ggaa(T115, T114, T118, X186)
U27_gagaa(T113, T115, T114, X185, X186, pV_out_ggaa(T115, T114, X185, X186)) → pR_out_gagaa(T113, T115, T114, X185, X186)
U13_ggga(T113, T114, X186, pR_out_gagaa(T113, X184, T114, X185, X186)) → ifQ_out_ggga(true, T113, T114, X186)
ifQ_in_ggga(false, T165, T166, X379) → U14_ggga(T165, T166, X379, pS_in_ggaa(T165, T166, X378, X379))
pS_in_ggaa(T165, T166, T169, X379) → U30_ggaa(T165, T166, T169, X379, timesG_in_gga(T165, T166, T169))
U30_ggaa(T165, T166, T169, X379, timesG_out_gga(T165, T166, T169)) → U31_ggaa(T165, T166, T169, X379, plusJ_in_gga(T166, T169, X379))
plusJ_in_gga(0, T178, T178) → plusJ_out_gga(0, T178, T178)
plusJ_in_gga(s(T183), T184, s(X402)) → U8_gga(T183, T184, X402, plusJ_in_gga(T183, T184, X402))
U8_gga(T183, T184, X402, plusJ_out_gga(T183, T184, X402)) → plusJ_out_gga(s(T183), T184, s(X402))
U31_ggaa(T165, T166, T169, X379, plusJ_out_gga(T166, T169, X379)) → pS_out_ggaa(T165, T166, T169, X379)
U14_ggga(T165, T166, X379, pS_out_ggaa(T165, T166, X378, X379)) → ifQ_out_ggga(false, T165, T166, X379)
U25_gaga(T100, T102, T101, X154, ifQ_out_ggga(T102, T100, T101, X154)) → pH_out_gaga(T100, T102, T101, X154)
U6_gga(T100, T101, X154, pH_out_gaga(T100, X153, T101, X154)) → timesG_out_gga(s(T100), T101, X154)
U22_ggaa(T79, T76, T88, T78, timesG_out_gga(T79, T76, T88)) → U23_ggaa(T79, T76, T88, T78, plusP_in_ga(T88, T78))
plusP_in_ga(0, 0) → plusP_out_ga(0, 0)
plusP_in_ga(s(0), s(s(0))) → plusP_out_ga(s(0), s(s(0)))
plusP_in_ga(s(s(0)), s(s(s(s(0))))) → plusP_out_ga(s(s(0)), s(s(s(s(0)))))
plusP_in_ga(s(s(s(0))), s(s(s(s(s(s(0))))))) → plusP_out_ga(s(s(s(0))), s(s(s(s(s(s(0)))))))
plusP_in_ga(s(s(s(s(0)))), s(s(s(s(s(s(s(s(0))))))))) → plusP_out_ga(s(s(s(s(0)))), s(s(s(s(s(s(s(s(0)))))))))
plusP_in_ga(s(s(s(s(s(0))))), s(s(s(s(s(s(s(s(s(s(0))))))))))) → plusP_out_ga(s(s(s(s(s(0))))), s(s(s(s(s(s(s(s(s(s(0)))))))))))
plusP_in_ga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))) → plusP_out_ga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))
plusP_in_ga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))))) → plusP_out_ga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))))
plusP_in_ga(s(s(s(s(s(s(s(s(T240)))))))), s(s(s(s(s(s(s(s(T242))))))))) → U12_ga(T240, T242, plusD_in_gga(T240, s(s(s(s(s(s(s(s(T240)))))))), T242))
U12_ga(T240, T242, plusD_out_gga(T240, s(s(s(s(s(s(s(s(T240)))))))), T242)) → plusP_out_ga(s(s(s(s(s(s(s(s(T240)))))))), s(s(s(s(s(s(s(s(T242)))))))))
U23_ggaa(T79, T76, T88, T78, plusP_out_ga(T88, T78)) → pU_out_ggaa(T79, T76, T88, T78)
U21_gagaa(T75, T79, T76, X113, T78, pU_out_ggaa(T79, T76, X113, T78)) → pM_out_gagaa(T75, T79, T76, X113, T78)
U9_ggga(T75, T76, T78, pM_out_gagaa(T75, X112, T76, X113, T78)) → ifL_out_ggga(true, T75, T76, T78)
ifL_in_ggga(false, T252, T253, T255) → U10_ggga(T252, T253, T255, pN_in_ggaa(T252, T253, X547, T255))
pN_in_ggaa(T252, T253, T256, T255) → U32_ggaa(T252, T253, T256, T255, timesG_in_gga(s(T252), T253, T256))
U32_ggaa(T252, T253, T256, T255, timesG_out_gga(s(T252), T253, T256)) → U33_ggaa(T252, T253, T256, T255, plusD_in_gga(T253, T256, T255))
U33_ggaa(T252, T253, T256, T255, plusD_out_gga(T253, T256, T255)) → pN_out_ggaa(T252, T253, T256, T255)
U10_ggga(T252, T253, T255, pN_out_ggaa(T252, T253, X547, T255)) → ifL_out_ggga(false, T252, T253, T255)
U19_gaga(T55, T56, T10, T12, ifL_out_ggga(T56, T55, T10, T12)) → pC_out_gaga(T55, T56, T10, T12)
U2_gga(T55, T10, T12, pC_out_gaga(T55, X78, T10, T12)) → timesA_out_gga(s(s(T55)), T10, T12)
TIMESA_IN_GGA(s(0), T21, T23) → U1_GGA(T21, T23, pB_in_gaa(T21, X37, T23))
TIMESA_IN_GGA(s(0), T21, T23) → PB_IN_GAA(T21, X37, T23)
PB_IN_GAA(T21, T27, T23) → U16_GAA(T21, T27, T23, timesK_in_ga(T21, T27))
PB_IN_GAA(T21, T27, T23) → TIMESK_IN_GA(T21, T27)
U16_GAA(T21, T27, T23, timesK_out_ga(T21, T27)) → U17_GAA(T21, T27, T23, plusD_in_gga(T21, T27, T23))
U16_GAA(T21, T27, T23, timesK_out_ga(T21, T27)) → PLUSD_IN_GGA(T21, T27, T23)
PLUSD_IN_GGA(s(T47), T48, s(T50)) → U3_GGA(T47, T48, T50, plusD_in_gga(T47, T48, T50))
PLUSD_IN_GGA(s(T47), T48, s(T50)) → PLUSD_IN_GGA(T47, T48, T50)
TIMESA_IN_GGA(s(s(T55)), T10, T12) → U2_GGA(T55, T10, T12, pC_in_gaga(T55, X78, T10, T12))
TIMESA_IN_GGA(s(s(T55)), T10, T12) → PC_IN_GAGA(T55, X78, T10, T12)
PC_IN_GAGA(T55, T56, T10, T12) → U18_GAGA(T55, T56, T10, T12, evenE_in_ga(T55, T56))
PC_IN_GAGA(T55, T56, T10, T12) → EVENE_IN_GA(T55, T56)
EVENE_IN_GA(s(s(T59)), X87) → U4_GA(T59, X87, evenE_in_ga(T59, X87))
EVENE_IN_GA(s(s(T59)), X87) → EVENE_IN_GA(T59, X87)
U18_GAGA(T55, T56, T10, T12, evenE_out_ga(T55, T56)) → U19_GAGA(T55, T56, T10, T12, ifL_in_ggga(T56, T55, T10, T12))
U18_GAGA(T55, T56, T10, T12, evenE_out_ga(T55, T56)) → IFL_IN_GGGA(T56, T55, T10, T12)
IFL_IN_GGGA(true, T75, T76, T78) → U9_GGGA(T75, T76, T78, pM_in_gagaa(T75, X112, T76, X113, T78))
IFL_IN_GGGA(true, T75, T76, T78) → PM_IN_GAGAA(T75, X112, T76, X113, T78)
PM_IN_GAGAA(T75, T79, T76, X113, T78) → U20_GAGAA(T75, T79, T76, X113, T78, halfO_in_ga(T75, T79))
PM_IN_GAGAA(T75, T79, T76, X113, T78) → HALFO_IN_GA(T75, T79)
HALFO_IN_GA(T82, s(X122)) → U11_GA(T82, X122, halfF_in_ga(T82, X122))
HALFO_IN_GA(T82, s(X122)) → HALFF_IN_GA(T82, X122)
HALFF_IN_GA(s(s(T85)), s(X131)) → U5_GA(T85, X131, halfF_in_ga(T85, X131))
HALFF_IN_GA(s(s(T85)), s(X131)) → HALFF_IN_GA(T85, X131)
U20_GAGAA(T75, T79, T76, X113, T78, halfO_out_ga(T75, T79)) → U21_GAGAA(T75, T79, T76, X113, T78, pU_in_ggaa(T79, T76, X113, T78))
U20_GAGAA(T75, T79, T76, X113, T78, halfO_out_ga(T75, T79)) → PU_IN_GGAA(T79, T76, X113, T78)
PU_IN_GGAA(T79, T76, T88, T78) → U22_GGAA(T79, T76, T88, T78, timesG_in_gga(T79, T76, T88))
PU_IN_GGAA(T79, T76, T88, T78) → TIMESG_IN_GGA(T79, T76, T88)
TIMESG_IN_GGA(s(T100), T101, X154) → U6_GGA(T100, T101, X154, pH_in_gaga(T100, X153, T101, X154))
TIMESG_IN_GGA(s(T100), T101, X154) → PH_IN_GAGA(T100, X153, T101, X154)
PH_IN_GAGA(T100, T102, T101, X154) → U24_GAGA(T100, T102, T101, X154, evenE_in_ga(s(T100), T102))
PH_IN_GAGA(T100, T102, T101, X154) → EVENE_IN_GA(s(T100), T102)
U24_GAGA(T100, T102, T101, X154, evenE_out_ga(s(T100), T102)) → U25_GAGA(T100, T102, T101, X154, ifQ_in_ggga(T102, T100, T101, X154))
U24_GAGA(T100, T102, T101, X154, evenE_out_ga(s(T100), T102)) → IFQ_IN_GGGA(T102, T100, T101, X154)
IFQ_IN_GGGA(true, T113, T114, X186) → U13_GGGA(T113, T114, X186, pR_in_gagaa(T113, X184, T114, X185, X186))
IFQ_IN_GGGA(true, T113, T114, X186) → PR_IN_GAGAA(T113, X184, T114, X185, X186)
PR_IN_GAGAA(T113, T115, T114, X185, X186) → U26_GAGAA(T113, T115, T114, X185, X186, halfF_in_ga(s(T113), T115))
PR_IN_GAGAA(T113, T115, T114, X185, X186) → HALFF_IN_GA(s(T113), T115)
U26_GAGAA(T113, T115, T114, X185, X186, halfF_out_ga(s(T113), T115)) → U27_GAGAA(T113, T115, T114, X185, X186, pV_in_ggaa(T115, T114, X185, X186))
U26_GAGAA(T113, T115, T114, X185, X186, halfF_out_ga(s(T113), T115)) → PV_IN_GGAA(T115, T114, X185, X186)
PV_IN_GGAA(T115, T114, T118, X186) → U28_GGAA(T115, T114, T118, X186, timesG_in_gga(T115, T114, T118))
PV_IN_GGAA(T115, T114, T118, X186) → TIMESG_IN_GGA(T115, T114, T118)
U28_GGAA(T115, T114, T118, X186, timesG_out_gga(T115, T114, T118)) → U29_GGAA(T115, T114, T118, X186, plusT_in_ga(T118, X186))
U28_GGAA(T115, T114, T118, X186, timesG_out_gga(T115, T114, T118)) → PLUST_IN_GA(T118, X186)
PLUST_IN_GA(s(s(s(s(s(s(s(s(T144)))))))), s(s(s(s(s(s(s(s(X342))))))))) → U15_GA(T144, X342, plusI_in_gga(T144, s(s(s(s(s(s(s(T144))))))), X342))
PLUST_IN_GA(s(s(s(s(s(s(s(s(T144)))))))), s(s(s(s(s(s(s(s(X342))))))))) → PLUSI_IN_GGA(T144, s(s(s(s(s(s(s(T144))))))), X342)
PLUSI_IN_GGA(s(T157), T158, s(X363)) → U7_GGA(T157, T158, X363, plusI_in_gga(T157, T158, X363))
PLUSI_IN_GGA(s(T157), T158, s(X363)) → PLUSI_IN_GGA(T157, T158, X363)
IFQ_IN_GGGA(false, T165, T166, X379) → U14_GGGA(T165, T166, X379, pS_in_ggaa(T165, T166, X378, X379))
IFQ_IN_GGGA(false, T165, T166, X379) → PS_IN_GGAA(T165, T166, X378, X379)
PS_IN_GGAA(T165, T166, T169, X379) → U30_GGAA(T165, T166, T169, X379, timesG_in_gga(T165, T166, T169))
PS_IN_GGAA(T165, T166, T169, X379) → TIMESG_IN_GGA(T165, T166, T169)
U30_GGAA(T165, T166, T169, X379, timesG_out_gga(T165, T166, T169)) → U31_GGAA(T165, T166, T169, X379, plusJ_in_gga(T166, T169, X379))
U30_GGAA(T165, T166, T169, X379, timesG_out_gga(T165, T166, T169)) → PLUSJ_IN_GGA(T166, T169, X379)
PLUSJ_IN_GGA(s(T183), T184, s(X402)) → U8_GGA(T183, T184, X402, plusJ_in_gga(T183, T184, X402))
PLUSJ_IN_GGA(s(T183), T184, s(X402)) → PLUSJ_IN_GGA(T183, T184, X402)
U22_GGAA(T79, T76, T88, T78, timesG_out_gga(T79, T76, T88)) → U23_GGAA(T79, T76, T88, T78, plusP_in_ga(T88, T78))
U22_GGAA(T79, T76, T88, T78, timesG_out_gga(T79, T76, T88)) → PLUSP_IN_GA(T88, T78)
PLUSP_IN_GA(s(s(s(s(s(s(s(s(T240)))))))), s(s(s(s(s(s(s(s(T242))))))))) → U12_GA(T240, T242, plusD_in_gga(T240, s(s(s(s(s(s(s(s(T240)))))))), T242))
PLUSP_IN_GA(s(s(s(s(s(s(s(s(T240)))))))), s(s(s(s(s(s(s(s(T242))))))))) → PLUSD_IN_GGA(T240, s(s(s(s(s(s(s(s(T240)))))))), T242)
IFL_IN_GGGA(false, T252, T253, T255) → U10_GGGA(T252, T253, T255, pN_in_ggaa(T252, T253, X547, T255))
IFL_IN_GGGA(false, T252, T253, T255) → PN_IN_GGAA(T252, T253, X547, T255)
PN_IN_GGAA(T252, T253, T256, T255) → U32_GGAA(T252, T253, T256, T255, timesG_in_gga(s(T252), T253, T256))
PN_IN_GGAA(T252, T253, T256, T255) → TIMESG_IN_GGA(s(T252), T253, T256)
U32_GGAA(T252, T253, T256, T255, timesG_out_gga(s(T252), T253, T256)) → U33_GGAA(T252, T253, T256, T255, plusD_in_gga(T253, T256, T255))
U32_GGAA(T252, T253, T256, T255, timesG_out_gga(s(T252), T253, T256)) → PLUSD_IN_GGA(T253, T256, T255)
timesA_in_gga(0, T5, 0) → timesA_out_gga(0, T5, 0)
timesA_in_gga(s(0), T21, T23) → U1_gga(T21, T23, pB_in_gaa(T21, X37, T23))
pB_in_gaa(T21, T27, T23) → U16_gaa(T21, T27, T23, timesK_in_ga(T21, T27))
timesK_in_ga(T33, 0) → timesK_out_ga(T33, 0)
U16_gaa(T21, T27, T23, timesK_out_ga(T21, T27)) → U17_gaa(T21, T27, T23, plusD_in_gga(T21, T27, T23))
plusD_in_gga(0, T40, T40) → plusD_out_gga(0, T40, T40)
plusD_in_gga(s(T47), T48, s(T50)) → U3_gga(T47, T48, T50, plusD_in_gga(T47, T48, T50))
U3_gga(T47, T48, T50, plusD_out_gga(T47, T48, T50)) → plusD_out_gga(s(T47), T48, s(T50))
U17_gaa(T21, T27, T23, plusD_out_gga(T21, T27, T23)) → pB_out_gaa(T21, T27, T23)
U1_gga(T21, T23, pB_out_gaa(T21, X37, T23)) → timesA_out_gga(s(0), T21, T23)
timesA_in_gga(s(s(T55)), T10, T12) → U2_gga(T55, T10, T12, pC_in_gaga(T55, X78, T10, T12))
pC_in_gaga(T55, T56, T10, T12) → U18_gaga(T55, T56, T10, T12, evenE_in_ga(T55, T56))
evenE_in_ga(0, true) → evenE_out_ga(0, true)
evenE_in_ga(s(0), false) → evenE_out_ga(s(0), false)
evenE_in_ga(s(s(T59)), X87) → U4_ga(T59, X87, evenE_in_ga(T59, X87))
U4_ga(T59, X87, evenE_out_ga(T59, X87)) → evenE_out_ga(s(s(T59)), X87)
U18_gaga(T55, T56, T10, T12, evenE_out_ga(T55, T56)) → U19_gaga(T55, T56, T10, T12, ifL_in_ggga(T56, T55, T10, T12))
ifL_in_ggga(true, T75, T76, T78) → U9_ggga(T75, T76, T78, pM_in_gagaa(T75, X112, T76, X113, T78))
pM_in_gagaa(T75, T79, T76, X113, T78) → U20_gagaa(T75, T79, T76, X113, T78, halfO_in_ga(T75, T79))
halfO_in_ga(T82, s(X122)) → U11_ga(T82, X122, halfF_in_ga(T82, X122))
halfF_in_ga(0, 0) → halfF_out_ga(0, 0)
halfF_in_ga(s(s(T85)), s(X131)) → U5_ga(T85, X131, halfF_in_ga(T85, X131))
U5_ga(T85, X131, halfF_out_ga(T85, X131)) → halfF_out_ga(s(s(T85)), s(X131))
U11_ga(T82, X122, halfF_out_ga(T82, X122)) → halfO_out_ga(T82, s(X122))
U20_gagaa(T75, T79, T76, X113, T78, halfO_out_ga(T75, T79)) → U21_gagaa(T75, T79, T76, X113, T78, pU_in_ggaa(T79, T76, X113, T78))
pU_in_ggaa(T79, T76, T88, T78) → U22_ggaa(T79, T76, T88, T78, timesG_in_gga(T79, T76, T88))
timesG_in_gga(0, T95, 0) → timesG_out_gga(0, T95, 0)
timesG_in_gga(s(T100), T101, X154) → U6_gga(T100, T101, X154, pH_in_gaga(T100, X153, T101, X154))
pH_in_gaga(T100, T102, T101, X154) → U24_gaga(T100, T102, T101, X154, evenE_in_ga(s(T100), T102))
U24_gaga(T100, T102, T101, X154, evenE_out_ga(s(T100), T102)) → U25_gaga(T100, T102, T101, X154, ifQ_in_ggga(T102, T100, T101, X154))
ifQ_in_ggga(true, T113, T114, X186) → U13_ggga(T113, T114, X186, pR_in_gagaa(T113, X184, T114, X185, X186))
pR_in_gagaa(T113, T115, T114, X185, X186) → U26_gagaa(T113, T115, T114, X185, X186, halfF_in_ga(s(T113), T115))
U26_gagaa(T113, T115, T114, X185, X186, halfF_out_ga(s(T113), T115)) → U27_gagaa(T113, T115, T114, X185, X186, pV_in_ggaa(T115, T114, X185, X186))
pV_in_ggaa(T115, T114, T118, X186) → U28_ggaa(T115, T114, T118, X186, timesG_in_gga(T115, T114, T118))
U28_ggaa(T115, T114, T118, X186, timesG_out_gga(T115, T114, T118)) → U29_ggaa(T115, T114, T118, X186, plusT_in_ga(T118, X186))
plusT_in_ga(0, 0) → plusT_out_ga(0, 0)
plusT_in_ga(s(0), s(s(0))) → plusT_out_ga(s(0), s(s(0)))
plusT_in_ga(s(s(0)), s(s(s(s(0))))) → plusT_out_ga(s(s(0)), s(s(s(s(0)))))
plusT_in_ga(s(s(s(0))), s(s(s(s(s(s(0))))))) → plusT_out_ga(s(s(s(0))), s(s(s(s(s(s(0)))))))
plusT_in_ga(s(s(s(s(0)))), s(s(s(s(s(s(s(s(0))))))))) → plusT_out_ga(s(s(s(s(0)))), s(s(s(s(s(s(s(s(0)))))))))
plusT_in_ga(s(s(s(s(s(0))))), s(s(s(s(s(s(s(s(s(s(0))))))))))) → plusT_out_ga(s(s(s(s(s(0))))), s(s(s(s(s(s(s(s(s(s(0)))))))))))
plusT_in_ga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))) → plusT_out_ga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))
plusT_in_ga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))))) → plusT_out_ga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))))
plusT_in_ga(s(s(s(s(s(s(s(s(T144)))))))), s(s(s(s(s(s(s(s(X342))))))))) → U15_ga(T144, X342, plusI_in_gga(T144, s(s(s(s(s(s(s(T144))))))), X342))
plusI_in_gga(0, T152, s(T152)) → plusI_out_gga(0, T152, s(T152))
plusI_in_gga(s(T157), T158, s(X363)) → U7_gga(T157, T158, X363, plusI_in_gga(T157, T158, X363))
U7_gga(T157, T158, X363, plusI_out_gga(T157, T158, X363)) → plusI_out_gga(s(T157), T158, s(X363))
U15_ga(T144, X342, plusI_out_gga(T144, s(s(s(s(s(s(s(T144))))))), X342)) → plusT_out_ga(s(s(s(s(s(s(s(s(T144)))))))), s(s(s(s(s(s(s(s(X342)))))))))
U29_ggaa(T115, T114, T118, X186, plusT_out_ga(T118, X186)) → pV_out_ggaa(T115, T114, T118, X186)
U27_gagaa(T113, T115, T114, X185, X186, pV_out_ggaa(T115, T114, X185, X186)) → pR_out_gagaa(T113, T115, T114, X185, X186)
U13_ggga(T113, T114, X186, pR_out_gagaa(T113, X184, T114, X185, X186)) → ifQ_out_ggga(true, T113, T114, X186)
ifQ_in_ggga(false, T165, T166, X379) → U14_ggga(T165, T166, X379, pS_in_ggaa(T165, T166, X378, X379))
pS_in_ggaa(T165, T166, T169, X379) → U30_ggaa(T165, T166, T169, X379, timesG_in_gga(T165, T166, T169))
U30_ggaa(T165, T166, T169, X379, timesG_out_gga(T165, T166, T169)) → U31_ggaa(T165, T166, T169, X379, plusJ_in_gga(T166, T169, X379))
plusJ_in_gga(0, T178, T178) → plusJ_out_gga(0, T178, T178)
plusJ_in_gga(s(T183), T184, s(X402)) → U8_gga(T183, T184, X402, plusJ_in_gga(T183, T184, X402))
U8_gga(T183, T184, X402, plusJ_out_gga(T183, T184, X402)) → plusJ_out_gga(s(T183), T184, s(X402))
U31_ggaa(T165, T166, T169, X379, plusJ_out_gga(T166, T169, X379)) → pS_out_ggaa(T165, T166, T169, X379)
U14_ggga(T165, T166, X379, pS_out_ggaa(T165, T166, X378, X379)) → ifQ_out_ggga(false, T165, T166, X379)
U25_gaga(T100, T102, T101, X154, ifQ_out_ggga(T102, T100, T101, X154)) → pH_out_gaga(T100, T102, T101, X154)
U6_gga(T100, T101, X154, pH_out_gaga(T100, X153, T101, X154)) → timesG_out_gga(s(T100), T101, X154)
U22_ggaa(T79, T76, T88, T78, timesG_out_gga(T79, T76, T88)) → U23_ggaa(T79, T76, T88, T78, plusP_in_ga(T88, T78))
plusP_in_ga(0, 0) → plusP_out_ga(0, 0)
plusP_in_ga(s(0), s(s(0))) → plusP_out_ga(s(0), s(s(0)))
plusP_in_ga(s(s(0)), s(s(s(s(0))))) → plusP_out_ga(s(s(0)), s(s(s(s(0)))))
plusP_in_ga(s(s(s(0))), s(s(s(s(s(s(0))))))) → plusP_out_ga(s(s(s(0))), s(s(s(s(s(s(0)))))))
plusP_in_ga(s(s(s(s(0)))), s(s(s(s(s(s(s(s(0))))))))) → plusP_out_ga(s(s(s(s(0)))), s(s(s(s(s(s(s(s(0)))))))))
plusP_in_ga(s(s(s(s(s(0))))), s(s(s(s(s(s(s(s(s(s(0))))))))))) → plusP_out_ga(s(s(s(s(s(0))))), s(s(s(s(s(s(s(s(s(s(0)))))))))))
plusP_in_ga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))) → plusP_out_ga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))
plusP_in_ga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))))) → plusP_out_ga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))))
plusP_in_ga(s(s(s(s(s(s(s(s(T240)))))))), s(s(s(s(s(s(s(s(T242))))))))) → U12_ga(T240, T242, plusD_in_gga(T240, s(s(s(s(s(s(s(s(T240)))))))), T242))
U12_ga(T240, T242, plusD_out_gga(T240, s(s(s(s(s(s(s(s(T240)))))))), T242)) → plusP_out_ga(s(s(s(s(s(s(s(s(T240)))))))), s(s(s(s(s(s(s(s(T242)))))))))
U23_ggaa(T79, T76, T88, T78, plusP_out_ga(T88, T78)) → pU_out_ggaa(T79, T76, T88, T78)
U21_gagaa(T75, T79, T76, X113, T78, pU_out_ggaa(T79, T76, X113, T78)) → pM_out_gagaa(T75, T79, T76, X113, T78)
U9_ggga(T75, T76, T78, pM_out_gagaa(T75, X112, T76, X113, T78)) → ifL_out_ggga(true, T75, T76, T78)
ifL_in_ggga(false, T252, T253, T255) → U10_ggga(T252, T253, T255, pN_in_ggaa(T252, T253, X547, T255))
pN_in_ggaa(T252, T253, T256, T255) → U32_ggaa(T252, T253, T256, T255, timesG_in_gga(s(T252), T253, T256))
U32_ggaa(T252, T253, T256, T255, timesG_out_gga(s(T252), T253, T256)) → U33_ggaa(T252, T253, T256, T255, plusD_in_gga(T253, T256, T255))
U33_ggaa(T252, T253, T256, T255, plusD_out_gga(T253, T256, T255)) → pN_out_ggaa(T252, T253, T256, T255)
U10_ggga(T252, T253, T255, pN_out_ggaa(T252, T253, X547, T255)) → ifL_out_ggga(false, T252, T253, T255)
U19_gaga(T55, T56, T10, T12, ifL_out_ggga(T56, T55, T10, T12)) → pC_out_gaga(T55, T56, T10, T12)
U2_gga(T55, T10, T12, pC_out_gaga(T55, X78, T10, T12)) → timesA_out_gga(s(s(T55)), T10, T12)
PLUSJ_IN_GGA(s(T183), T184, s(X402)) → PLUSJ_IN_GGA(T183, T184, X402)
timesA_in_gga(0, T5, 0) → timesA_out_gga(0, T5, 0)
timesA_in_gga(s(0), T21, T23) → U1_gga(T21, T23, pB_in_gaa(T21, X37, T23))
pB_in_gaa(T21, T27, T23) → U16_gaa(T21, T27, T23, timesK_in_ga(T21, T27))
timesK_in_ga(T33, 0) → timesK_out_ga(T33, 0)
U16_gaa(T21, T27, T23, timesK_out_ga(T21, T27)) → U17_gaa(T21, T27, T23, plusD_in_gga(T21, T27, T23))
plusD_in_gga(0, T40, T40) → plusD_out_gga(0, T40, T40)
plusD_in_gga(s(T47), T48, s(T50)) → U3_gga(T47, T48, T50, plusD_in_gga(T47, T48, T50))
U3_gga(T47, T48, T50, plusD_out_gga(T47, T48, T50)) → plusD_out_gga(s(T47), T48, s(T50))
U17_gaa(T21, T27, T23, plusD_out_gga(T21, T27, T23)) → pB_out_gaa(T21, T27, T23)
U1_gga(T21, T23, pB_out_gaa(T21, X37, T23)) → timesA_out_gga(s(0), T21, T23)
timesA_in_gga(s(s(T55)), T10, T12) → U2_gga(T55, T10, T12, pC_in_gaga(T55, X78, T10, T12))
pC_in_gaga(T55, T56, T10, T12) → U18_gaga(T55, T56, T10, T12, evenE_in_ga(T55, T56))
evenE_in_ga(0, true) → evenE_out_ga(0, true)
evenE_in_ga(s(0), false) → evenE_out_ga(s(0), false)
evenE_in_ga(s(s(T59)), X87) → U4_ga(T59, X87, evenE_in_ga(T59, X87))
U4_ga(T59, X87, evenE_out_ga(T59, X87)) → evenE_out_ga(s(s(T59)), X87)
U18_gaga(T55, T56, T10, T12, evenE_out_ga(T55, T56)) → U19_gaga(T55, T56, T10, T12, ifL_in_ggga(T56, T55, T10, T12))
ifL_in_ggga(true, T75, T76, T78) → U9_ggga(T75, T76, T78, pM_in_gagaa(T75, X112, T76, X113, T78))
pM_in_gagaa(T75, T79, T76, X113, T78) → U20_gagaa(T75, T79, T76, X113, T78, halfO_in_ga(T75, T79))
halfO_in_ga(T82, s(X122)) → U11_ga(T82, X122, halfF_in_ga(T82, X122))
halfF_in_ga(0, 0) → halfF_out_ga(0, 0)
halfF_in_ga(s(s(T85)), s(X131)) → U5_ga(T85, X131, halfF_in_ga(T85, X131))
U5_ga(T85, X131, halfF_out_ga(T85, X131)) → halfF_out_ga(s(s(T85)), s(X131))
U11_ga(T82, X122, halfF_out_ga(T82, X122)) → halfO_out_ga(T82, s(X122))
U20_gagaa(T75, T79, T76, X113, T78, halfO_out_ga(T75, T79)) → U21_gagaa(T75, T79, T76, X113, T78, pU_in_ggaa(T79, T76, X113, T78))
pU_in_ggaa(T79, T76, T88, T78) → U22_ggaa(T79, T76, T88, T78, timesG_in_gga(T79, T76, T88))
timesG_in_gga(0, T95, 0) → timesG_out_gga(0, T95, 0)
timesG_in_gga(s(T100), T101, X154) → U6_gga(T100, T101, X154, pH_in_gaga(T100, X153, T101, X154))
pH_in_gaga(T100, T102, T101, X154) → U24_gaga(T100, T102, T101, X154, evenE_in_ga(s(T100), T102))
U24_gaga(T100, T102, T101, X154, evenE_out_ga(s(T100), T102)) → U25_gaga(T100, T102, T101, X154, ifQ_in_ggga(T102, T100, T101, X154))
ifQ_in_ggga(true, T113, T114, X186) → U13_ggga(T113, T114, X186, pR_in_gagaa(T113, X184, T114, X185, X186))
pR_in_gagaa(T113, T115, T114, X185, X186) → U26_gagaa(T113, T115, T114, X185, X186, halfF_in_ga(s(T113), T115))
U26_gagaa(T113, T115, T114, X185, X186, halfF_out_ga(s(T113), T115)) → U27_gagaa(T113, T115, T114, X185, X186, pV_in_ggaa(T115, T114, X185, X186))
pV_in_ggaa(T115, T114, T118, X186) → U28_ggaa(T115, T114, T118, X186, timesG_in_gga(T115, T114, T118))
U28_ggaa(T115, T114, T118, X186, timesG_out_gga(T115, T114, T118)) → U29_ggaa(T115, T114, T118, X186, plusT_in_ga(T118, X186))
plusT_in_ga(0, 0) → plusT_out_ga(0, 0)
plusT_in_ga(s(0), s(s(0))) → plusT_out_ga(s(0), s(s(0)))
plusT_in_ga(s(s(0)), s(s(s(s(0))))) → plusT_out_ga(s(s(0)), s(s(s(s(0)))))
plusT_in_ga(s(s(s(0))), s(s(s(s(s(s(0))))))) → plusT_out_ga(s(s(s(0))), s(s(s(s(s(s(0)))))))
plusT_in_ga(s(s(s(s(0)))), s(s(s(s(s(s(s(s(0))))))))) → plusT_out_ga(s(s(s(s(0)))), s(s(s(s(s(s(s(s(0)))))))))
plusT_in_ga(s(s(s(s(s(0))))), s(s(s(s(s(s(s(s(s(s(0))))))))))) → plusT_out_ga(s(s(s(s(s(0))))), s(s(s(s(s(s(s(s(s(s(0)))))))))))
plusT_in_ga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))) → plusT_out_ga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))
plusT_in_ga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))))) → plusT_out_ga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))))
plusT_in_ga(s(s(s(s(s(s(s(s(T144)))))))), s(s(s(s(s(s(s(s(X342))))))))) → U15_ga(T144, X342, plusI_in_gga(T144, s(s(s(s(s(s(s(T144))))))), X342))
plusI_in_gga(0, T152, s(T152)) → plusI_out_gga(0, T152, s(T152))
plusI_in_gga(s(T157), T158, s(X363)) → U7_gga(T157, T158, X363, plusI_in_gga(T157, T158, X363))
U7_gga(T157, T158, X363, plusI_out_gga(T157, T158, X363)) → plusI_out_gga(s(T157), T158, s(X363))
U15_ga(T144, X342, plusI_out_gga(T144, s(s(s(s(s(s(s(T144))))))), X342)) → plusT_out_ga(s(s(s(s(s(s(s(s(T144)))))))), s(s(s(s(s(s(s(s(X342)))))))))
U29_ggaa(T115, T114, T118, X186, plusT_out_ga(T118, X186)) → pV_out_ggaa(T115, T114, T118, X186)
U27_gagaa(T113, T115, T114, X185, X186, pV_out_ggaa(T115, T114, X185, X186)) → pR_out_gagaa(T113, T115, T114, X185, X186)
U13_ggga(T113, T114, X186, pR_out_gagaa(T113, X184, T114, X185, X186)) → ifQ_out_ggga(true, T113, T114, X186)
ifQ_in_ggga(false, T165, T166, X379) → U14_ggga(T165, T166, X379, pS_in_ggaa(T165, T166, X378, X379))
pS_in_ggaa(T165, T166, T169, X379) → U30_ggaa(T165, T166, T169, X379, timesG_in_gga(T165, T166, T169))
U30_ggaa(T165, T166, T169, X379, timesG_out_gga(T165, T166, T169)) → U31_ggaa(T165, T166, T169, X379, plusJ_in_gga(T166, T169, X379))
plusJ_in_gga(0, T178, T178) → plusJ_out_gga(0, T178, T178)
plusJ_in_gga(s(T183), T184, s(X402)) → U8_gga(T183, T184, X402, plusJ_in_gga(T183, T184, X402))
U8_gga(T183, T184, X402, plusJ_out_gga(T183, T184, X402)) → plusJ_out_gga(s(T183), T184, s(X402))
U31_ggaa(T165, T166, T169, X379, plusJ_out_gga(T166, T169, X379)) → pS_out_ggaa(T165, T166, T169, X379)
U14_ggga(T165, T166, X379, pS_out_ggaa(T165, T166, X378, X379)) → ifQ_out_ggga(false, T165, T166, X379)
U25_gaga(T100, T102, T101, X154, ifQ_out_ggga(T102, T100, T101, X154)) → pH_out_gaga(T100, T102, T101, X154)
U6_gga(T100, T101, X154, pH_out_gaga(T100, X153, T101, X154)) → timesG_out_gga(s(T100), T101, X154)
U22_ggaa(T79, T76, T88, T78, timesG_out_gga(T79, T76, T88)) → U23_ggaa(T79, T76, T88, T78, plusP_in_ga(T88, T78))
plusP_in_ga(0, 0) → plusP_out_ga(0, 0)
plusP_in_ga(s(0), s(s(0))) → plusP_out_ga(s(0), s(s(0)))
plusP_in_ga(s(s(0)), s(s(s(s(0))))) → plusP_out_ga(s(s(0)), s(s(s(s(0)))))
plusP_in_ga(s(s(s(0))), s(s(s(s(s(s(0))))))) → plusP_out_ga(s(s(s(0))), s(s(s(s(s(s(0)))))))
plusP_in_ga(s(s(s(s(0)))), s(s(s(s(s(s(s(s(0))))))))) → plusP_out_ga(s(s(s(s(0)))), s(s(s(s(s(s(s(s(0)))))))))
plusP_in_ga(s(s(s(s(s(0))))), s(s(s(s(s(s(s(s(s(s(0))))))))))) → plusP_out_ga(s(s(s(s(s(0))))), s(s(s(s(s(s(s(s(s(s(0)))))))))))
plusP_in_ga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))) → plusP_out_ga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))
plusP_in_ga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))))) → plusP_out_ga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))))
plusP_in_ga(s(s(s(s(s(s(s(s(T240)))))))), s(s(s(s(s(s(s(s(T242))))))))) → U12_ga(T240, T242, plusD_in_gga(T240, s(s(s(s(s(s(s(s(T240)))))))), T242))
U12_ga(T240, T242, plusD_out_gga(T240, s(s(s(s(s(s(s(s(T240)))))))), T242)) → plusP_out_ga(s(s(s(s(s(s(s(s(T240)))))))), s(s(s(s(s(s(s(s(T242)))))))))
U23_ggaa(T79, T76, T88, T78, plusP_out_ga(T88, T78)) → pU_out_ggaa(T79, T76, T88, T78)
U21_gagaa(T75, T79, T76, X113, T78, pU_out_ggaa(T79, T76, X113, T78)) → pM_out_gagaa(T75, T79, T76, X113, T78)
U9_ggga(T75, T76, T78, pM_out_gagaa(T75, X112, T76, X113, T78)) → ifL_out_ggga(true, T75, T76, T78)
ifL_in_ggga(false, T252, T253, T255) → U10_ggga(T252, T253, T255, pN_in_ggaa(T252, T253, X547, T255))
pN_in_ggaa(T252, T253, T256, T255) → U32_ggaa(T252, T253, T256, T255, timesG_in_gga(s(T252), T253, T256))
U32_ggaa(T252, T253, T256, T255, timesG_out_gga(s(T252), T253, T256)) → U33_ggaa(T252, T253, T256, T255, plusD_in_gga(T253, T256, T255))
U33_ggaa(T252, T253, T256, T255, plusD_out_gga(T253, T256, T255)) → pN_out_ggaa(T252, T253, T256, T255)
U10_ggga(T252, T253, T255, pN_out_ggaa(T252, T253, X547, T255)) → ifL_out_ggga(false, T252, T253, T255)
U19_gaga(T55, T56, T10, T12, ifL_out_ggga(T56, T55, T10, T12)) → pC_out_gaga(T55, T56, T10, T12)
U2_gga(T55, T10, T12, pC_out_gaga(T55, X78, T10, T12)) → timesA_out_gga(s(s(T55)), T10, T12)
PLUSJ_IN_GGA(s(T183), T184, s(X402)) → PLUSJ_IN_GGA(T183, T184, X402)
PLUSJ_IN_GGA(s(T183), T184) → PLUSJ_IN_GGA(T183, T184)
From the DPs we obtained the following set of size-change graphs:
PLUSI_IN_GGA(s(T157), T158, s(X363)) → PLUSI_IN_GGA(T157, T158, X363)
timesA_in_gga(0, T5, 0) → timesA_out_gga(0, T5, 0)
timesA_in_gga(s(0), T21, T23) → U1_gga(T21, T23, pB_in_gaa(T21, X37, T23))
pB_in_gaa(T21, T27, T23) → U16_gaa(T21, T27, T23, timesK_in_ga(T21, T27))
timesK_in_ga(T33, 0) → timesK_out_ga(T33, 0)
U16_gaa(T21, T27, T23, timesK_out_ga(T21, T27)) → U17_gaa(T21, T27, T23, plusD_in_gga(T21, T27, T23))
plusD_in_gga(0, T40, T40) → plusD_out_gga(0, T40, T40)
plusD_in_gga(s(T47), T48, s(T50)) → U3_gga(T47, T48, T50, plusD_in_gga(T47, T48, T50))
U3_gga(T47, T48, T50, plusD_out_gga(T47, T48, T50)) → plusD_out_gga(s(T47), T48, s(T50))
U17_gaa(T21, T27, T23, plusD_out_gga(T21, T27, T23)) → pB_out_gaa(T21, T27, T23)
U1_gga(T21, T23, pB_out_gaa(T21, X37, T23)) → timesA_out_gga(s(0), T21, T23)
timesA_in_gga(s(s(T55)), T10, T12) → U2_gga(T55, T10, T12, pC_in_gaga(T55, X78, T10, T12))
pC_in_gaga(T55, T56, T10, T12) → U18_gaga(T55, T56, T10, T12, evenE_in_ga(T55, T56))
evenE_in_ga(0, true) → evenE_out_ga(0, true)
evenE_in_ga(s(0), false) → evenE_out_ga(s(0), false)
evenE_in_ga(s(s(T59)), X87) → U4_ga(T59, X87, evenE_in_ga(T59, X87))
U4_ga(T59, X87, evenE_out_ga(T59, X87)) → evenE_out_ga(s(s(T59)), X87)
U18_gaga(T55, T56, T10, T12, evenE_out_ga(T55, T56)) → U19_gaga(T55, T56, T10, T12, ifL_in_ggga(T56, T55, T10, T12))
ifL_in_ggga(true, T75, T76, T78) → U9_ggga(T75, T76, T78, pM_in_gagaa(T75, X112, T76, X113, T78))
pM_in_gagaa(T75, T79, T76, X113, T78) → U20_gagaa(T75, T79, T76, X113, T78, halfO_in_ga(T75, T79))
halfO_in_ga(T82, s(X122)) → U11_ga(T82, X122, halfF_in_ga(T82, X122))
halfF_in_ga(0, 0) → halfF_out_ga(0, 0)
halfF_in_ga(s(s(T85)), s(X131)) → U5_ga(T85, X131, halfF_in_ga(T85, X131))
U5_ga(T85, X131, halfF_out_ga(T85, X131)) → halfF_out_ga(s(s(T85)), s(X131))
U11_ga(T82, X122, halfF_out_ga(T82, X122)) → halfO_out_ga(T82, s(X122))
U20_gagaa(T75, T79, T76, X113, T78, halfO_out_ga(T75, T79)) → U21_gagaa(T75, T79, T76, X113, T78, pU_in_ggaa(T79, T76, X113, T78))
pU_in_ggaa(T79, T76, T88, T78) → U22_ggaa(T79, T76, T88, T78, timesG_in_gga(T79, T76, T88))
timesG_in_gga(0, T95, 0) → timesG_out_gga(0, T95, 0)
timesG_in_gga(s(T100), T101, X154) → U6_gga(T100, T101, X154, pH_in_gaga(T100, X153, T101, X154))
pH_in_gaga(T100, T102, T101, X154) → U24_gaga(T100, T102, T101, X154, evenE_in_ga(s(T100), T102))
U24_gaga(T100, T102, T101, X154, evenE_out_ga(s(T100), T102)) → U25_gaga(T100, T102, T101, X154, ifQ_in_ggga(T102, T100, T101, X154))
ifQ_in_ggga(true, T113, T114, X186) → U13_ggga(T113, T114, X186, pR_in_gagaa(T113, X184, T114, X185, X186))
pR_in_gagaa(T113, T115, T114, X185, X186) → U26_gagaa(T113, T115, T114, X185, X186, halfF_in_ga(s(T113), T115))
U26_gagaa(T113, T115, T114, X185, X186, halfF_out_ga(s(T113), T115)) → U27_gagaa(T113, T115, T114, X185, X186, pV_in_ggaa(T115, T114, X185, X186))
pV_in_ggaa(T115, T114, T118, X186) → U28_ggaa(T115, T114, T118, X186, timesG_in_gga(T115, T114, T118))
U28_ggaa(T115, T114, T118, X186, timesG_out_gga(T115, T114, T118)) → U29_ggaa(T115, T114, T118, X186, plusT_in_ga(T118, X186))
plusT_in_ga(0, 0) → plusT_out_ga(0, 0)
plusT_in_ga(s(0), s(s(0))) → plusT_out_ga(s(0), s(s(0)))
plusT_in_ga(s(s(0)), s(s(s(s(0))))) → plusT_out_ga(s(s(0)), s(s(s(s(0)))))
plusT_in_ga(s(s(s(0))), s(s(s(s(s(s(0))))))) → plusT_out_ga(s(s(s(0))), s(s(s(s(s(s(0)))))))
plusT_in_ga(s(s(s(s(0)))), s(s(s(s(s(s(s(s(0))))))))) → plusT_out_ga(s(s(s(s(0)))), s(s(s(s(s(s(s(s(0)))))))))
plusT_in_ga(s(s(s(s(s(0))))), s(s(s(s(s(s(s(s(s(s(0))))))))))) → plusT_out_ga(s(s(s(s(s(0))))), s(s(s(s(s(s(s(s(s(s(0)))))))))))
plusT_in_ga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))) → plusT_out_ga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))
plusT_in_ga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))))) → plusT_out_ga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))))
plusT_in_ga(s(s(s(s(s(s(s(s(T144)))))))), s(s(s(s(s(s(s(s(X342))))))))) → U15_ga(T144, X342, plusI_in_gga(T144, s(s(s(s(s(s(s(T144))))))), X342))
plusI_in_gga(0, T152, s(T152)) → plusI_out_gga(0, T152, s(T152))
plusI_in_gga(s(T157), T158, s(X363)) → U7_gga(T157, T158, X363, plusI_in_gga(T157, T158, X363))
U7_gga(T157, T158, X363, plusI_out_gga(T157, T158, X363)) → plusI_out_gga(s(T157), T158, s(X363))
U15_ga(T144, X342, plusI_out_gga(T144, s(s(s(s(s(s(s(T144))))))), X342)) → plusT_out_ga(s(s(s(s(s(s(s(s(T144)))))))), s(s(s(s(s(s(s(s(X342)))))))))
U29_ggaa(T115, T114, T118, X186, plusT_out_ga(T118, X186)) → pV_out_ggaa(T115, T114, T118, X186)
U27_gagaa(T113, T115, T114, X185, X186, pV_out_ggaa(T115, T114, X185, X186)) → pR_out_gagaa(T113, T115, T114, X185, X186)
U13_ggga(T113, T114, X186, pR_out_gagaa(T113, X184, T114, X185, X186)) → ifQ_out_ggga(true, T113, T114, X186)
ifQ_in_ggga(false, T165, T166, X379) → U14_ggga(T165, T166, X379, pS_in_ggaa(T165, T166, X378, X379))
pS_in_ggaa(T165, T166, T169, X379) → U30_ggaa(T165, T166, T169, X379, timesG_in_gga(T165, T166, T169))
U30_ggaa(T165, T166, T169, X379, timesG_out_gga(T165, T166, T169)) → U31_ggaa(T165, T166, T169, X379, plusJ_in_gga(T166, T169, X379))
plusJ_in_gga(0, T178, T178) → plusJ_out_gga(0, T178, T178)
plusJ_in_gga(s(T183), T184, s(X402)) → U8_gga(T183, T184, X402, plusJ_in_gga(T183, T184, X402))
U8_gga(T183, T184, X402, plusJ_out_gga(T183, T184, X402)) → plusJ_out_gga(s(T183), T184, s(X402))
U31_ggaa(T165, T166, T169, X379, plusJ_out_gga(T166, T169, X379)) → pS_out_ggaa(T165, T166, T169, X379)
U14_ggga(T165, T166, X379, pS_out_ggaa(T165, T166, X378, X379)) → ifQ_out_ggga(false, T165, T166, X379)
U25_gaga(T100, T102, T101, X154, ifQ_out_ggga(T102, T100, T101, X154)) → pH_out_gaga(T100, T102, T101, X154)
U6_gga(T100, T101, X154, pH_out_gaga(T100, X153, T101, X154)) → timesG_out_gga(s(T100), T101, X154)
U22_ggaa(T79, T76, T88, T78, timesG_out_gga(T79, T76, T88)) → U23_ggaa(T79, T76, T88, T78, plusP_in_ga(T88, T78))
plusP_in_ga(0, 0) → plusP_out_ga(0, 0)
plusP_in_ga(s(0), s(s(0))) → plusP_out_ga(s(0), s(s(0)))
plusP_in_ga(s(s(0)), s(s(s(s(0))))) → plusP_out_ga(s(s(0)), s(s(s(s(0)))))
plusP_in_ga(s(s(s(0))), s(s(s(s(s(s(0))))))) → plusP_out_ga(s(s(s(0))), s(s(s(s(s(s(0)))))))
plusP_in_ga(s(s(s(s(0)))), s(s(s(s(s(s(s(s(0))))))))) → plusP_out_ga(s(s(s(s(0)))), s(s(s(s(s(s(s(s(0)))))))))
plusP_in_ga(s(s(s(s(s(0))))), s(s(s(s(s(s(s(s(s(s(0))))))))))) → plusP_out_ga(s(s(s(s(s(0))))), s(s(s(s(s(s(s(s(s(s(0)))))))))))
plusP_in_ga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))) → plusP_out_ga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))
plusP_in_ga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))))) → plusP_out_ga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))))
plusP_in_ga(s(s(s(s(s(s(s(s(T240)))))))), s(s(s(s(s(s(s(s(T242))))))))) → U12_ga(T240, T242, plusD_in_gga(T240, s(s(s(s(s(s(s(s(T240)))))))), T242))
U12_ga(T240, T242, plusD_out_gga(T240, s(s(s(s(s(s(s(s(T240)))))))), T242)) → plusP_out_ga(s(s(s(s(s(s(s(s(T240)))))))), s(s(s(s(s(s(s(s(T242)))))))))
U23_ggaa(T79, T76, T88, T78, plusP_out_ga(T88, T78)) → pU_out_ggaa(T79, T76, T88, T78)
U21_gagaa(T75, T79, T76, X113, T78, pU_out_ggaa(T79, T76, X113, T78)) → pM_out_gagaa(T75, T79, T76, X113, T78)
U9_ggga(T75, T76, T78, pM_out_gagaa(T75, X112, T76, X113, T78)) → ifL_out_ggga(true, T75, T76, T78)
ifL_in_ggga(false, T252, T253, T255) → U10_ggga(T252, T253, T255, pN_in_ggaa(T252, T253, X547, T255))
pN_in_ggaa(T252, T253, T256, T255) → U32_ggaa(T252, T253, T256, T255, timesG_in_gga(s(T252), T253, T256))
U32_ggaa(T252, T253, T256, T255, timesG_out_gga(s(T252), T253, T256)) → U33_ggaa(T252, T253, T256, T255, plusD_in_gga(T253, T256, T255))
U33_ggaa(T252, T253, T256, T255, plusD_out_gga(T253, T256, T255)) → pN_out_ggaa(T252, T253, T256, T255)
U10_ggga(T252, T253, T255, pN_out_ggaa(T252, T253, X547, T255)) → ifL_out_ggga(false, T252, T253, T255)
U19_gaga(T55, T56, T10, T12, ifL_out_ggga(T56, T55, T10, T12)) → pC_out_gaga(T55, T56, T10, T12)
U2_gga(T55, T10, T12, pC_out_gaga(T55, X78, T10, T12)) → timesA_out_gga(s(s(T55)), T10, T12)
PLUSI_IN_GGA(s(T157), T158, s(X363)) → PLUSI_IN_GGA(T157, T158, X363)
PLUSI_IN_GGA(s(T157), T158) → PLUSI_IN_GGA(T157, T158)
From the DPs we obtained the following set of size-change graphs:
HALFF_IN_GA(s(s(T85)), s(X131)) → HALFF_IN_GA(T85, X131)
timesA_in_gga(0, T5, 0) → timesA_out_gga(0, T5, 0)
timesA_in_gga(s(0), T21, T23) → U1_gga(T21, T23, pB_in_gaa(T21, X37, T23))
pB_in_gaa(T21, T27, T23) → U16_gaa(T21, T27, T23, timesK_in_ga(T21, T27))
timesK_in_ga(T33, 0) → timesK_out_ga(T33, 0)
U16_gaa(T21, T27, T23, timesK_out_ga(T21, T27)) → U17_gaa(T21, T27, T23, plusD_in_gga(T21, T27, T23))
plusD_in_gga(0, T40, T40) → plusD_out_gga(0, T40, T40)
plusD_in_gga(s(T47), T48, s(T50)) → U3_gga(T47, T48, T50, plusD_in_gga(T47, T48, T50))
U3_gga(T47, T48, T50, plusD_out_gga(T47, T48, T50)) → plusD_out_gga(s(T47), T48, s(T50))
U17_gaa(T21, T27, T23, plusD_out_gga(T21, T27, T23)) → pB_out_gaa(T21, T27, T23)
U1_gga(T21, T23, pB_out_gaa(T21, X37, T23)) → timesA_out_gga(s(0), T21, T23)
timesA_in_gga(s(s(T55)), T10, T12) → U2_gga(T55, T10, T12, pC_in_gaga(T55, X78, T10, T12))
pC_in_gaga(T55, T56, T10, T12) → U18_gaga(T55, T56, T10, T12, evenE_in_ga(T55, T56))
evenE_in_ga(0, true) → evenE_out_ga(0, true)
evenE_in_ga(s(0), false) → evenE_out_ga(s(0), false)
evenE_in_ga(s(s(T59)), X87) → U4_ga(T59, X87, evenE_in_ga(T59, X87))
U4_ga(T59, X87, evenE_out_ga(T59, X87)) → evenE_out_ga(s(s(T59)), X87)
U18_gaga(T55, T56, T10, T12, evenE_out_ga(T55, T56)) → U19_gaga(T55, T56, T10, T12, ifL_in_ggga(T56, T55, T10, T12))
ifL_in_ggga(true, T75, T76, T78) → U9_ggga(T75, T76, T78, pM_in_gagaa(T75, X112, T76, X113, T78))
pM_in_gagaa(T75, T79, T76, X113, T78) → U20_gagaa(T75, T79, T76, X113, T78, halfO_in_ga(T75, T79))
halfO_in_ga(T82, s(X122)) → U11_ga(T82, X122, halfF_in_ga(T82, X122))
halfF_in_ga(0, 0) → halfF_out_ga(0, 0)
halfF_in_ga(s(s(T85)), s(X131)) → U5_ga(T85, X131, halfF_in_ga(T85, X131))
U5_ga(T85, X131, halfF_out_ga(T85, X131)) → halfF_out_ga(s(s(T85)), s(X131))
U11_ga(T82, X122, halfF_out_ga(T82, X122)) → halfO_out_ga(T82, s(X122))
U20_gagaa(T75, T79, T76, X113, T78, halfO_out_ga(T75, T79)) → U21_gagaa(T75, T79, T76, X113, T78, pU_in_ggaa(T79, T76, X113, T78))
pU_in_ggaa(T79, T76, T88, T78) → U22_ggaa(T79, T76, T88, T78, timesG_in_gga(T79, T76, T88))
timesG_in_gga(0, T95, 0) → timesG_out_gga(0, T95, 0)
timesG_in_gga(s(T100), T101, X154) → U6_gga(T100, T101, X154, pH_in_gaga(T100, X153, T101, X154))
pH_in_gaga(T100, T102, T101, X154) → U24_gaga(T100, T102, T101, X154, evenE_in_ga(s(T100), T102))
U24_gaga(T100, T102, T101, X154, evenE_out_ga(s(T100), T102)) → U25_gaga(T100, T102, T101, X154, ifQ_in_ggga(T102, T100, T101, X154))
ifQ_in_ggga(true, T113, T114, X186) → U13_ggga(T113, T114, X186, pR_in_gagaa(T113, X184, T114, X185, X186))
pR_in_gagaa(T113, T115, T114, X185, X186) → U26_gagaa(T113, T115, T114, X185, X186, halfF_in_ga(s(T113), T115))
U26_gagaa(T113, T115, T114, X185, X186, halfF_out_ga(s(T113), T115)) → U27_gagaa(T113, T115, T114, X185, X186, pV_in_ggaa(T115, T114, X185, X186))
pV_in_ggaa(T115, T114, T118, X186) → U28_ggaa(T115, T114, T118, X186, timesG_in_gga(T115, T114, T118))
U28_ggaa(T115, T114, T118, X186, timesG_out_gga(T115, T114, T118)) → U29_ggaa(T115, T114, T118, X186, plusT_in_ga(T118, X186))
plusT_in_ga(0, 0) → plusT_out_ga(0, 0)
plusT_in_ga(s(0), s(s(0))) → plusT_out_ga(s(0), s(s(0)))
plusT_in_ga(s(s(0)), s(s(s(s(0))))) → plusT_out_ga(s(s(0)), s(s(s(s(0)))))
plusT_in_ga(s(s(s(0))), s(s(s(s(s(s(0))))))) → plusT_out_ga(s(s(s(0))), s(s(s(s(s(s(0)))))))
plusT_in_ga(s(s(s(s(0)))), s(s(s(s(s(s(s(s(0))))))))) → plusT_out_ga(s(s(s(s(0)))), s(s(s(s(s(s(s(s(0)))))))))
plusT_in_ga(s(s(s(s(s(0))))), s(s(s(s(s(s(s(s(s(s(0))))))))))) → plusT_out_ga(s(s(s(s(s(0))))), s(s(s(s(s(s(s(s(s(s(0)))))))))))
plusT_in_ga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))) → plusT_out_ga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))
plusT_in_ga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))))) → plusT_out_ga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))))
plusT_in_ga(s(s(s(s(s(s(s(s(T144)))))))), s(s(s(s(s(s(s(s(X342))))))))) → U15_ga(T144, X342, plusI_in_gga(T144, s(s(s(s(s(s(s(T144))))))), X342))
plusI_in_gga(0, T152, s(T152)) → plusI_out_gga(0, T152, s(T152))
plusI_in_gga(s(T157), T158, s(X363)) → U7_gga(T157, T158, X363, plusI_in_gga(T157, T158, X363))
U7_gga(T157, T158, X363, plusI_out_gga(T157, T158, X363)) → plusI_out_gga(s(T157), T158, s(X363))
U15_ga(T144, X342, plusI_out_gga(T144, s(s(s(s(s(s(s(T144))))))), X342)) → plusT_out_ga(s(s(s(s(s(s(s(s(T144)))))))), s(s(s(s(s(s(s(s(X342)))))))))
U29_ggaa(T115, T114, T118, X186, plusT_out_ga(T118, X186)) → pV_out_ggaa(T115, T114, T118, X186)
U27_gagaa(T113, T115, T114, X185, X186, pV_out_ggaa(T115, T114, X185, X186)) → pR_out_gagaa(T113, T115, T114, X185, X186)
U13_ggga(T113, T114, X186, pR_out_gagaa(T113, X184, T114, X185, X186)) → ifQ_out_ggga(true, T113, T114, X186)
ifQ_in_ggga(false, T165, T166, X379) → U14_ggga(T165, T166, X379, pS_in_ggaa(T165, T166, X378, X379))
pS_in_ggaa(T165, T166, T169, X379) → U30_ggaa(T165, T166, T169, X379, timesG_in_gga(T165, T166, T169))
U30_ggaa(T165, T166, T169, X379, timesG_out_gga(T165, T166, T169)) → U31_ggaa(T165, T166, T169, X379, plusJ_in_gga(T166, T169, X379))
plusJ_in_gga(0, T178, T178) → plusJ_out_gga(0, T178, T178)
plusJ_in_gga(s(T183), T184, s(X402)) → U8_gga(T183, T184, X402, plusJ_in_gga(T183, T184, X402))
U8_gga(T183, T184, X402, plusJ_out_gga(T183, T184, X402)) → plusJ_out_gga(s(T183), T184, s(X402))
U31_ggaa(T165, T166, T169, X379, plusJ_out_gga(T166, T169, X379)) → pS_out_ggaa(T165, T166, T169, X379)
U14_ggga(T165, T166, X379, pS_out_ggaa(T165, T166, X378, X379)) → ifQ_out_ggga(false, T165, T166, X379)
U25_gaga(T100, T102, T101, X154, ifQ_out_ggga(T102, T100, T101, X154)) → pH_out_gaga(T100, T102, T101, X154)
U6_gga(T100, T101, X154, pH_out_gaga(T100, X153, T101, X154)) → timesG_out_gga(s(T100), T101, X154)
U22_ggaa(T79, T76, T88, T78, timesG_out_gga(T79, T76, T88)) → U23_ggaa(T79, T76, T88, T78, plusP_in_ga(T88, T78))
plusP_in_ga(0, 0) → plusP_out_ga(0, 0)
plusP_in_ga(s(0), s(s(0))) → plusP_out_ga(s(0), s(s(0)))
plusP_in_ga(s(s(0)), s(s(s(s(0))))) → plusP_out_ga(s(s(0)), s(s(s(s(0)))))
plusP_in_ga(s(s(s(0))), s(s(s(s(s(s(0))))))) → plusP_out_ga(s(s(s(0))), s(s(s(s(s(s(0)))))))
plusP_in_ga(s(s(s(s(0)))), s(s(s(s(s(s(s(s(0))))))))) → plusP_out_ga(s(s(s(s(0)))), s(s(s(s(s(s(s(s(0)))))))))
plusP_in_ga(s(s(s(s(s(0))))), s(s(s(s(s(s(s(s(s(s(0))))))))))) → plusP_out_ga(s(s(s(s(s(0))))), s(s(s(s(s(s(s(s(s(s(0)))))))))))
plusP_in_ga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))) → plusP_out_ga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))
plusP_in_ga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))))) → plusP_out_ga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))))
plusP_in_ga(s(s(s(s(s(s(s(s(T240)))))))), s(s(s(s(s(s(s(s(T242))))))))) → U12_ga(T240, T242, plusD_in_gga(T240, s(s(s(s(s(s(s(s(T240)))))))), T242))
U12_ga(T240, T242, plusD_out_gga(T240, s(s(s(s(s(s(s(s(T240)))))))), T242)) → plusP_out_ga(s(s(s(s(s(s(s(s(T240)))))))), s(s(s(s(s(s(s(s(T242)))))))))
U23_ggaa(T79, T76, T88, T78, plusP_out_ga(T88, T78)) → pU_out_ggaa(T79, T76, T88, T78)
U21_gagaa(T75, T79, T76, X113, T78, pU_out_ggaa(T79, T76, X113, T78)) → pM_out_gagaa(T75, T79, T76, X113, T78)
U9_ggga(T75, T76, T78, pM_out_gagaa(T75, X112, T76, X113, T78)) → ifL_out_ggga(true, T75, T76, T78)
ifL_in_ggga(false, T252, T253, T255) → U10_ggga(T252, T253, T255, pN_in_ggaa(T252, T253, X547, T255))
pN_in_ggaa(T252, T253, T256, T255) → U32_ggaa(T252, T253, T256, T255, timesG_in_gga(s(T252), T253, T256))
U32_ggaa(T252, T253, T256, T255, timesG_out_gga(s(T252), T253, T256)) → U33_ggaa(T252, T253, T256, T255, plusD_in_gga(T253, T256, T255))
U33_ggaa(T252, T253, T256, T255, plusD_out_gga(T253, T256, T255)) → pN_out_ggaa(T252, T253, T256, T255)
U10_ggga(T252, T253, T255, pN_out_ggaa(T252, T253, X547, T255)) → ifL_out_ggga(false, T252, T253, T255)
U19_gaga(T55, T56, T10, T12, ifL_out_ggga(T56, T55, T10, T12)) → pC_out_gaga(T55, T56, T10, T12)
U2_gga(T55, T10, T12, pC_out_gaga(T55, X78, T10, T12)) → timesA_out_gga(s(s(T55)), T10, T12)
HALFF_IN_GA(s(s(T85)), s(X131)) → HALFF_IN_GA(T85, X131)
HALFF_IN_GA(s(s(T85))) → HALFF_IN_GA(T85)
From the DPs we obtained the following set of size-change graphs:
EVENE_IN_GA(s(s(T59)), X87) → EVENE_IN_GA(T59, X87)
timesA_in_gga(0, T5, 0) → timesA_out_gga(0, T5, 0)
timesA_in_gga(s(0), T21, T23) → U1_gga(T21, T23, pB_in_gaa(T21, X37, T23))
pB_in_gaa(T21, T27, T23) → U16_gaa(T21, T27, T23, timesK_in_ga(T21, T27))
timesK_in_ga(T33, 0) → timesK_out_ga(T33, 0)
U16_gaa(T21, T27, T23, timesK_out_ga(T21, T27)) → U17_gaa(T21, T27, T23, plusD_in_gga(T21, T27, T23))
plusD_in_gga(0, T40, T40) → plusD_out_gga(0, T40, T40)
plusD_in_gga(s(T47), T48, s(T50)) → U3_gga(T47, T48, T50, plusD_in_gga(T47, T48, T50))
U3_gga(T47, T48, T50, plusD_out_gga(T47, T48, T50)) → plusD_out_gga(s(T47), T48, s(T50))
U17_gaa(T21, T27, T23, plusD_out_gga(T21, T27, T23)) → pB_out_gaa(T21, T27, T23)
U1_gga(T21, T23, pB_out_gaa(T21, X37, T23)) → timesA_out_gga(s(0), T21, T23)
timesA_in_gga(s(s(T55)), T10, T12) → U2_gga(T55, T10, T12, pC_in_gaga(T55, X78, T10, T12))
pC_in_gaga(T55, T56, T10, T12) → U18_gaga(T55, T56, T10, T12, evenE_in_ga(T55, T56))
evenE_in_ga(0, true) → evenE_out_ga(0, true)
evenE_in_ga(s(0), false) → evenE_out_ga(s(0), false)
evenE_in_ga(s(s(T59)), X87) → U4_ga(T59, X87, evenE_in_ga(T59, X87))
U4_ga(T59, X87, evenE_out_ga(T59, X87)) → evenE_out_ga(s(s(T59)), X87)
U18_gaga(T55, T56, T10, T12, evenE_out_ga(T55, T56)) → U19_gaga(T55, T56, T10, T12, ifL_in_ggga(T56, T55, T10, T12))
ifL_in_ggga(true, T75, T76, T78) → U9_ggga(T75, T76, T78, pM_in_gagaa(T75, X112, T76, X113, T78))
pM_in_gagaa(T75, T79, T76, X113, T78) → U20_gagaa(T75, T79, T76, X113, T78, halfO_in_ga(T75, T79))
halfO_in_ga(T82, s(X122)) → U11_ga(T82, X122, halfF_in_ga(T82, X122))
halfF_in_ga(0, 0) → halfF_out_ga(0, 0)
halfF_in_ga(s(s(T85)), s(X131)) → U5_ga(T85, X131, halfF_in_ga(T85, X131))
U5_ga(T85, X131, halfF_out_ga(T85, X131)) → halfF_out_ga(s(s(T85)), s(X131))
U11_ga(T82, X122, halfF_out_ga(T82, X122)) → halfO_out_ga(T82, s(X122))
U20_gagaa(T75, T79, T76, X113, T78, halfO_out_ga(T75, T79)) → U21_gagaa(T75, T79, T76, X113, T78, pU_in_ggaa(T79, T76, X113, T78))
pU_in_ggaa(T79, T76, T88, T78) → U22_ggaa(T79, T76, T88, T78, timesG_in_gga(T79, T76, T88))
timesG_in_gga(0, T95, 0) → timesG_out_gga(0, T95, 0)
timesG_in_gga(s(T100), T101, X154) → U6_gga(T100, T101, X154, pH_in_gaga(T100, X153, T101, X154))
pH_in_gaga(T100, T102, T101, X154) → U24_gaga(T100, T102, T101, X154, evenE_in_ga(s(T100), T102))
U24_gaga(T100, T102, T101, X154, evenE_out_ga(s(T100), T102)) → U25_gaga(T100, T102, T101, X154, ifQ_in_ggga(T102, T100, T101, X154))
ifQ_in_ggga(true, T113, T114, X186) → U13_ggga(T113, T114, X186, pR_in_gagaa(T113, X184, T114, X185, X186))
pR_in_gagaa(T113, T115, T114, X185, X186) → U26_gagaa(T113, T115, T114, X185, X186, halfF_in_ga(s(T113), T115))
U26_gagaa(T113, T115, T114, X185, X186, halfF_out_ga(s(T113), T115)) → U27_gagaa(T113, T115, T114, X185, X186, pV_in_ggaa(T115, T114, X185, X186))
pV_in_ggaa(T115, T114, T118, X186) → U28_ggaa(T115, T114, T118, X186, timesG_in_gga(T115, T114, T118))
U28_ggaa(T115, T114, T118, X186, timesG_out_gga(T115, T114, T118)) → U29_ggaa(T115, T114, T118, X186, plusT_in_ga(T118, X186))
plusT_in_ga(0, 0) → plusT_out_ga(0, 0)
plusT_in_ga(s(0), s(s(0))) → plusT_out_ga(s(0), s(s(0)))
plusT_in_ga(s(s(0)), s(s(s(s(0))))) → plusT_out_ga(s(s(0)), s(s(s(s(0)))))
plusT_in_ga(s(s(s(0))), s(s(s(s(s(s(0))))))) → plusT_out_ga(s(s(s(0))), s(s(s(s(s(s(0)))))))
plusT_in_ga(s(s(s(s(0)))), s(s(s(s(s(s(s(s(0))))))))) → plusT_out_ga(s(s(s(s(0)))), s(s(s(s(s(s(s(s(0)))))))))
plusT_in_ga(s(s(s(s(s(0))))), s(s(s(s(s(s(s(s(s(s(0))))))))))) → plusT_out_ga(s(s(s(s(s(0))))), s(s(s(s(s(s(s(s(s(s(0)))))))))))
plusT_in_ga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))) → plusT_out_ga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))
plusT_in_ga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))))) → plusT_out_ga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))))
plusT_in_ga(s(s(s(s(s(s(s(s(T144)))))))), s(s(s(s(s(s(s(s(X342))))))))) → U15_ga(T144, X342, plusI_in_gga(T144, s(s(s(s(s(s(s(T144))))))), X342))
plusI_in_gga(0, T152, s(T152)) → plusI_out_gga(0, T152, s(T152))
plusI_in_gga(s(T157), T158, s(X363)) → U7_gga(T157, T158, X363, plusI_in_gga(T157, T158, X363))
U7_gga(T157, T158, X363, plusI_out_gga(T157, T158, X363)) → plusI_out_gga(s(T157), T158, s(X363))
U15_ga(T144, X342, plusI_out_gga(T144, s(s(s(s(s(s(s(T144))))))), X342)) → plusT_out_ga(s(s(s(s(s(s(s(s(T144)))))))), s(s(s(s(s(s(s(s(X342)))))))))
U29_ggaa(T115, T114, T118, X186, plusT_out_ga(T118, X186)) → pV_out_ggaa(T115, T114, T118, X186)
U27_gagaa(T113, T115, T114, X185, X186, pV_out_ggaa(T115, T114, X185, X186)) → pR_out_gagaa(T113, T115, T114, X185, X186)
U13_ggga(T113, T114, X186, pR_out_gagaa(T113, X184, T114, X185, X186)) → ifQ_out_ggga(true, T113, T114, X186)
ifQ_in_ggga(false, T165, T166, X379) → U14_ggga(T165, T166, X379, pS_in_ggaa(T165, T166, X378, X379))
pS_in_ggaa(T165, T166, T169, X379) → U30_ggaa(T165, T166, T169, X379, timesG_in_gga(T165, T166, T169))
U30_ggaa(T165, T166, T169, X379, timesG_out_gga(T165, T166, T169)) → U31_ggaa(T165, T166, T169, X379, plusJ_in_gga(T166, T169, X379))
plusJ_in_gga(0, T178, T178) → plusJ_out_gga(0, T178, T178)
plusJ_in_gga(s(T183), T184, s(X402)) → U8_gga(T183, T184, X402, plusJ_in_gga(T183, T184, X402))
U8_gga(T183, T184, X402, plusJ_out_gga(T183, T184, X402)) → plusJ_out_gga(s(T183), T184, s(X402))
U31_ggaa(T165, T166, T169, X379, plusJ_out_gga(T166, T169, X379)) → pS_out_ggaa(T165, T166, T169, X379)
U14_ggga(T165, T166, X379, pS_out_ggaa(T165, T166, X378, X379)) → ifQ_out_ggga(false, T165, T166, X379)
U25_gaga(T100, T102, T101, X154, ifQ_out_ggga(T102, T100, T101, X154)) → pH_out_gaga(T100, T102, T101, X154)
U6_gga(T100, T101, X154, pH_out_gaga(T100, X153, T101, X154)) → timesG_out_gga(s(T100), T101, X154)
U22_ggaa(T79, T76, T88, T78, timesG_out_gga(T79, T76, T88)) → U23_ggaa(T79, T76, T88, T78, plusP_in_ga(T88, T78))
plusP_in_ga(0, 0) → plusP_out_ga(0, 0)
plusP_in_ga(s(0), s(s(0))) → plusP_out_ga(s(0), s(s(0)))
plusP_in_ga(s(s(0)), s(s(s(s(0))))) → plusP_out_ga(s(s(0)), s(s(s(s(0)))))
plusP_in_ga(s(s(s(0))), s(s(s(s(s(s(0))))))) → plusP_out_ga(s(s(s(0))), s(s(s(s(s(s(0)))))))
plusP_in_ga(s(s(s(s(0)))), s(s(s(s(s(s(s(s(0))))))))) → plusP_out_ga(s(s(s(s(0)))), s(s(s(s(s(s(s(s(0)))))))))
plusP_in_ga(s(s(s(s(s(0))))), s(s(s(s(s(s(s(s(s(s(0))))))))))) → plusP_out_ga(s(s(s(s(s(0))))), s(s(s(s(s(s(s(s(s(s(0)))))))))))
plusP_in_ga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))) → plusP_out_ga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))
plusP_in_ga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))))) → plusP_out_ga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))))
plusP_in_ga(s(s(s(s(s(s(s(s(T240)))))))), s(s(s(s(s(s(s(s(T242))))))))) → U12_ga(T240, T242, plusD_in_gga(T240, s(s(s(s(s(s(s(s(T240)))))))), T242))
U12_ga(T240, T242, plusD_out_gga(T240, s(s(s(s(s(s(s(s(T240)))))))), T242)) → plusP_out_ga(s(s(s(s(s(s(s(s(T240)))))))), s(s(s(s(s(s(s(s(T242)))))))))
U23_ggaa(T79, T76, T88, T78, plusP_out_ga(T88, T78)) → pU_out_ggaa(T79, T76, T88, T78)
U21_gagaa(T75, T79, T76, X113, T78, pU_out_ggaa(T79, T76, X113, T78)) → pM_out_gagaa(T75, T79, T76, X113, T78)
U9_ggga(T75, T76, T78, pM_out_gagaa(T75, X112, T76, X113, T78)) → ifL_out_ggga(true, T75, T76, T78)
ifL_in_ggga(false, T252, T253, T255) → U10_ggga(T252, T253, T255, pN_in_ggaa(T252, T253, X547, T255))
pN_in_ggaa(T252, T253, T256, T255) → U32_ggaa(T252, T253, T256, T255, timesG_in_gga(s(T252), T253, T256))
U32_ggaa(T252, T253, T256, T255, timesG_out_gga(s(T252), T253, T256)) → U33_ggaa(T252, T253, T256, T255, plusD_in_gga(T253, T256, T255))
U33_ggaa(T252, T253, T256, T255, plusD_out_gga(T253, T256, T255)) → pN_out_ggaa(T252, T253, T256, T255)
U10_ggga(T252, T253, T255, pN_out_ggaa(T252, T253, X547, T255)) → ifL_out_ggga(false, T252, T253, T255)
U19_gaga(T55, T56, T10, T12, ifL_out_ggga(T56, T55, T10, T12)) → pC_out_gaga(T55, T56, T10, T12)
U2_gga(T55, T10, T12, pC_out_gaga(T55, X78, T10, T12)) → timesA_out_gga(s(s(T55)), T10, T12)
EVENE_IN_GA(s(s(T59)), X87) → EVENE_IN_GA(T59, X87)
EVENE_IN_GA(s(s(T59))) → EVENE_IN_GA(T59)
From the DPs we obtained the following set of size-change graphs:
PH_IN_GAGA(T100, T102, T101, X154) → U24_GAGA(T100, T102, T101, X154, evenE_in_ga(s(T100), T102))
U24_GAGA(T100, T102, T101, X154, evenE_out_ga(s(T100), T102)) → IFQ_IN_GGGA(T102, T100, T101, X154)
IFQ_IN_GGGA(true, T113, T114, X186) → PR_IN_GAGAA(T113, X184, T114, X185, X186)
PR_IN_GAGAA(T113, T115, T114, X185, X186) → U26_GAGAA(T113, T115, T114, X185, X186, halfF_in_ga(s(T113), T115))
U26_GAGAA(T113, T115, T114, X185, X186, halfF_out_ga(s(T113), T115)) → PV_IN_GGAA(T115, T114, X185, X186)
PV_IN_GGAA(T115, T114, T118, X186) → TIMESG_IN_GGA(T115, T114, T118)
TIMESG_IN_GGA(s(T100), T101, X154) → PH_IN_GAGA(T100, X153, T101, X154)
IFQ_IN_GGGA(false, T165, T166, X379) → PS_IN_GGAA(T165, T166, X378, X379)
PS_IN_GGAA(T165, T166, T169, X379) → TIMESG_IN_GGA(T165, T166, T169)
timesA_in_gga(0, T5, 0) → timesA_out_gga(0, T5, 0)
timesA_in_gga(s(0), T21, T23) → U1_gga(T21, T23, pB_in_gaa(T21, X37, T23))
pB_in_gaa(T21, T27, T23) → U16_gaa(T21, T27, T23, timesK_in_ga(T21, T27))
timesK_in_ga(T33, 0) → timesK_out_ga(T33, 0)
U16_gaa(T21, T27, T23, timesK_out_ga(T21, T27)) → U17_gaa(T21, T27, T23, plusD_in_gga(T21, T27, T23))
plusD_in_gga(0, T40, T40) → plusD_out_gga(0, T40, T40)
plusD_in_gga(s(T47), T48, s(T50)) → U3_gga(T47, T48, T50, plusD_in_gga(T47, T48, T50))
U3_gga(T47, T48, T50, plusD_out_gga(T47, T48, T50)) → plusD_out_gga(s(T47), T48, s(T50))
U17_gaa(T21, T27, T23, plusD_out_gga(T21, T27, T23)) → pB_out_gaa(T21, T27, T23)
U1_gga(T21, T23, pB_out_gaa(T21, X37, T23)) → timesA_out_gga(s(0), T21, T23)
timesA_in_gga(s(s(T55)), T10, T12) → U2_gga(T55, T10, T12, pC_in_gaga(T55, X78, T10, T12))
pC_in_gaga(T55, T56, T10, T12) → U18_gaga(T55, T56, T10, T12, evenE_in_ga(T55, T56))
evenE_in_ga(0, true) → evenE_out_ga(0, true)
evenE_in_ga(s(0), false) → evenE_out_ga(s(0), false)
evenE_in_ga(s(s(T59)), X87) → U4_ga(T59, X87, evenE_in_ga(T59, X87))
U4_ga(T59, X87, evenE_out_ga(T59, X87)) → evenE_out_ga(s(s(T59)), X87)
U18_gaga(T55, T56, T10, T12, evenE_out_ga(T55, T56)) → U19_gaga(T55, T56, T10, T12, ifL_in_ggga(T56, T55, T10, T12))
ifL_in_ggga(true, T75, T76, T78) → U9_ggga(T75, T76, T78, pM_in_gagaa(T75, X112, T76, X113, T78))
pM_in_gagaa(T75, T79, T76, X113, T78) → U20_gagaa(T75, T79, T76, X113, T78, halfO_in_ga(T75, T79))
halfO_in_ga(T82, s(X122)) → U11_ga(T82, X122, halfF_in_ga(T82, X122))
halfF_in_ga(0, 0) → halfF_out_ga(0, 0)
halfF_in_ga(s(s(T85)), s(X131)) → U5_ga(T85, X131, halfF_in_ga(T85, X131))
U5_ga(T85, X131, halfF_out_ga(T85, X131)) → halfF_out_ga(s(s(T85)), s(X131))
U11_ga(T82, X122, halfF_out_ga(T82, X122)) → halfO_out_ga(T82, s(X122))
U20_gagaa(T75, T79, T76, X113, T78, halfO_out_ga(T75, T79)) → U21_gagaa(T75, T79, T76, X113, T78, pU_in_ggaa(T79, T76, X113, T78))
pU_in_ggaa(T79, T76, T88, T78) → U22_ggaa(T79, T76, T88, T78, timesG_in_gga(T79, T76, T88))
timesG_in_gga(0, T95, 0) → timesG_out_gga(0, T95, 0)
timesG_in_gga(s(T100), T101, X154) → U6_gga(T100, T101, X154, pH_in_gaga(T100, X153, T101, X154))
pH_in_gaga(T100, T102, T101, X154) → U24_gaga(T100, T102, T101, X154, evenE_in_ga(s(T100), T102))
U24_gaga(T100, T102, T101, X154, evenE_out_ga(s(T100), T102)) → U25_gaga(T100, T102, T101, X154, ifQ_in_ggga(T102, T100, T101, X154))
ifQ_in_ggga(true, T113, T114, X186) → U13_ggga(T113, T114, X186, pR_in_gagaa(T113, X184, T114, X185, X186))
pR_in_gagaa(T113, T115, T114, X185, X186) → U26_gagaa(T113, T115, T114, X185, X186, halfF_in_ga(s(T113), T115))
U26_gagaa(T113, T115, T114, X185, X186, halfF_out_ga(s(T113), T115)) → U27_gagaa(T113, T115, T114, X185, X186, pV_in_ggaa(T115, T114, X185, X186))
pV_in_ggaa(T115, T114, T118, X186) → U28_ggaa(T115, T114, T118, X186, timesG_in_gga(T115, T114, T118))
U28_ggaa(T115, T114, T118, X186, timesG_out_gga(T115, T114, T118)) → U29_ggaa(T115, T114, T118, X186, plusT_in_ga(T118, X186))
plusT_in_ga(0, 0) → plusT_out_ga(0, 0)
plusT_in_ga(s(0), s(s(0))) → plusT_out_ga(s(0), s(s(0)))
plusT_in_ga(s(s(0)), s(s(s(s(0))))) → plusT_out_ga(s(s(0)), s(s(s(s(0)))))
plusT_in_ga(s(s(s(0))), s(s(s(s(s(s(0))))))) → plusT_out_ga(s(s(s(0))), s(s(s(s(s(s(0)))))))
plusT_in_ga(s(s(s(s(0)))), s(s(s(s(s(s(s(s(0))))))))) → plusT_out_ga(s(s(s(s(0)))), s(s(s(s(s(s(s(s(0)))))))))
plusT_in_ga(s(s(s(s(s(0))))), s(s(s(s(s(s(s(s(s(s(0))))))))))) → plusT_out_ga(s(s(s(s(s(0))))), s(s(s(s(s(s(s(s(s(s(0)))))))))))
plusT_in_ga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))) → plusT_out_ga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))
plusT_in_ga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))))) → plusT_out_ga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))))
plusT_in_ga(s(s(s(s(s(s(s(s(T144)))))))), s(s(s(s(s(s(s(s(X342))))))))) → U15_ga(T144, X342, plusI_in_gga(T144, s(s(s(s(s(s(s(T144))))))), X342))
plusI_in_gga(0, T152, s(T152)) → plusI_out_gga(0, T152, s(T152))
plusI_in_gga(s(T157), T158, s(X363)) → U7_gga(T157, T158, X363, plusI_in_gga(T157, T158, X363))
U7_gga(T157, T158, X363, plusI_out_gga(T157, T158, X363)) → plusI_out_gga(s(T157), T158, s(X363))
U15_ga(T144, X342, plusI_out_gga(T144, s(s(s(s(s(s(s(T144))))))), X342)) → plusT_out_ga(s(s(s(s(s(s(s(s(T144)))))))), s(s(s(s(s(s(s(s(X342)))))))))
U29_ggaa(T115, T114, T118, X186, plusT_out_ga(T118, X186)) → pV_out_ggaa(T115, T114, T118, X186)
U27_gagaa(T113, T115, T114, X185, X186, pV_out_ggaa(T115, T114, X185, X186)) → pR_out_gagaa(T113, T115, T114, X185, X186)
U13_ggga(T113, T114, X186, pR_out_gagaa(T113, X184, T114, X185, X186)) → ifQ_out_ggga(true, T113, T114, X186)
ifQ_in_ggga(false, T165, T166, X379) → U14_ggga(T165, T166, X379, pS_in_ggaa(T165, T166, X378, X379))
pS_in_ggaa(T165, T166, T169, X379) → U30_ggaa(T165, T166, T169, X379, timesG_in_gga(T165, T166, T169))
U30_ggaa(T165, T166, T169, X379, timesG_out_gga(T165, T166, T169)) → U31_ggaa(T165, T166, T169, X379, plusJ_in_gga(T166, T169, X379))
plusJ_in_gga(0, T178, T178) → plusJ_out_gga(0, T178, T178)
plusJ_in_gga(s(T183), T184, s(X402)) → U8_gga(T183, T184, X402, plusJ_in_gga(T183, T184, X402))
U8_gga(T183, T184, X402, plusJ_out_gga(T183, T184, X402)) → plusJ_out_gga(s(T183), T184, s(X402))
U31_ggaa(T165, T166, T169, X379, plusJ_out_gga(T166, T169, X379)) → pS_out_ggaa(T165, T166, T169, X379)
U14_ggga(T165, T166, X379, pS_out_ggaa(T165, T166, X378, X379)) → ifQ_out_ggga(false, T165, T166, X379)
U25_gaga(T100, T102, T101, X154, ifQ_out_ggga(T102, T100, T101, X154)) → pH_out_gaga(T100, T102, T101, X154)
U6_gga(T100, T101, X154, pH_out_gaga(T100, X153, T101, X154)) → timesG_out_gga(s(T100), T101, X154)
U22_ggaa(T79, T76, T88, T78, timesG_out_gga(T79, T76, T88)) → U23_ggaa(T79, T76, T88, T78, plusP_in_ga(T88, T78))
plusP_in_ga(0, 0) → plusP_out_ga(0, 0)
plusP_in_ga(s(0), s(s(0))) → plusP_out_ga(s(0), s(s(0)))
plusP_in_ga(s(s(0)), s(s(s(s(0))))) → plusP_out_ga(s(s(0)), s(s(s(s(0)))))
plusP_in_ga(s(s(s(0))), s(s(s(s(s(s(0))))))) → plusP_out_ga(s(s(s(0))), s(s(s(s(s(s(0)))))))
plusP_in_ga(s(s(s(s(0)))), s(s(s(s(s(s(s(s(0))))))))) → plusP_out_ga(s(s(s(s(0)))), s(s(s(s(s(s(s(s(0)))))))))
plusP_in_ga(s(s(s(s(s(0))))), s(s(s(s(s(s(s(s(s(s(0))))))))))) → plusP_out_ga(s(s(s(s(s(0))))), s(s(s(s(s(s(s(s(s(s(0)))))))))))
plusP_in_ga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))) → plusP_out_ga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))
plusP_in_ga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))))) → plusP_out_ga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))))
plusP_in_ga(s(s(s(s(s(s(s(s(T240)))))))), s(s(s(s(s(s(s(s(T242))))))))) → U12_ga(T240, T242, plusD_in_gga(T240, s(s(s(s(s(s(s(s(T240)))))))), T242))
U12_ga(T240, T242, plusD_out_gga(T240, s(s(s(s(s(s(s(s(T240)))))))), T242)) → plusP_out_ga(s(s(s(s(s(s(s(s(T240)))))))), s(s(s(s(s(s(s(s(T242)))))))))
U23_ggaa(T79, T76, T88, T78, plusP_out_ga(T88, T78)) → pU_out_ggaa(T79, T76, T88, T78)
U21_gagaa(T75, T79, T76, X113, T78, pU_out_ggaa(T79, T76, X113, T78)) → pM_out_gagaa(T75, T79, T76, X113, T78)
U9_ggga(T75, T76, T78, pM_out_gagaa(T75, X112, T76, X113, T78)) → ifL_out_ggga(true, T75, T76, T78)
ifL_in_ggga(false, T252, T253, T255) → U10_ggga(T252, T253, T255, pN_in_ggaa(T252, T253, X547, T255))
pN_in_ggaa(T252, T253, T256, T255) → U32_ggaa(T252, T253, T256, T255, timesG_in_gga(s(T252), T253, T256))
U32_ggaa(T252, T253, T256, T255, timesG_out_gga(s(T252), T253, T256)) → U33_ggaa(T252, T253, T256, T255, plusD_in_gga(T253, T256, T255))
U33_ggaa(T252, T253, T256, T255, plusD_out_gga(T253, T256, T255)) → pN_out_ggaa(T252, T253, T256, T255)
U10_ggga(T252, T253, T255, pN_out_ggaa(T252, T253, X547, T255)) → ifL_out_ggga(false, T252, T253, T255)
U19_gaga(T55, T56, T10, T12, ifL_out_ggga(T56, T55, T10, T12)) → pC_out_gaga(T55, T56, T10, T12)
U2_gga(T55, T10, T12, pC_out_gaga(T55, X78, T10, T12)) → timesA_out_gga(s(s(T55)), T10, T12)
PH_IN_GAGA(T100, T102, T101, X154) → U24_GAGA(T100, T102, T101, X154, evenE_in_ga(s(T100), T102))
U24_GAGA(T100, T102, T101, X154, evenE_out_ga(s(T100), T102)) → IFQ_IN_GGGA(T102, T100, T101, X154)
IFQ_IN_GGGA(true, T113, T114, X186) → PR_IN_GAGAA(T113, X184, T114, X185, X186)
PR_IN_GAGAA(T113, T115, T114, X185, X186) → U26_GAGAA(T113, T115, T114, X185, X186, halfF_in_ga(s(T113), T115))
U26_GAGAA(T113, T115, T114, X185, X186, halfF_out_ga(s(T113), T115)) → PV_IN_GGAA(T115, T114, X185, X186)
PV_IN_GGAA(T115, T114, T118, X186) → TIMESG_IN_GGA(T115, T114, T118)
TIMESG_IN_GGA(s(T100), T101, X154) → PH_IN_GAGA(T100, X153, T101, X154)
IFQ_IN_GGGA(false, T165, T166, X379) → PS_IN_GGAA(T165, T166, X378, X379)
PS_IN_GGAA(T165, T166, T169, X379) → TIMESG_IN_GGA(T165, T166, T169)
evenE_in_ga(s(0), false) → evenE_out_ga(s(0), false)
evenE_in_ga(s(s(T59)), X87) → U4_ga(T59, X87, evenE_in_ga(T59, X87))
halfF_in_ga(s(s(T85)), s(X131)) → U5_ga(T85, X131, halfF_in_ga(T85, X131))
U4_ga(T59, X87, evenE_out_ga(T59, X87)) → evenE_out_ga(s(s(T59)), X87)
U5_ga(T85, X131, halfF_out_ga(T85, X131)) → halfF_out_ga(s(s(T85)), s(X131))
evenE_in_ga(0, true) → evenE_out_ga(0, true)
halfF_in_ga(0, 0) → halfF_out_ga(0, 0)
PH_IN_GAGA(T100, T101) → U24_GAGA(T100, T101, evenE_in_ga(s(T100)))
U24_GAGA(T100, T101, evenE_out_ga(s(T100), T102)) → IFQ_IN_GGGA(T102, T100, T101)
IFQ_IN_GGGA(true, T113, T114) → PR_IN_GAGAA(T113, T114)
PR_IN_GAGAA(T113, T114) → U26_GAGAA(T113, T114, halfF_in_ga(s(T113)))
U26_GAGAA(T113, T114, halfF_out_ga(s(T113), T115)) → PV_IN_GGAA(T115, T114)
PV_IN_GGAA(T115, T114) → TIMESG_IN_GGA(T115, T114)
TIMESG_IN_GGA(s(T100), T101) → PH_IN_GAGA(T100, T101)
IFQ_IN_GGGA(false, T165, T166) → PS_IN_GGAA(T165, T166)
PS_IN_GGAA(T165, T166) → TIMESG_IN_GGA(T165, T166)
evenE_in_ga(s(0)) → evenE_out_ga(s(0), false)
evenE_in_ga(s(s(T59))) → U4_ga(T59, evenE_in_ga(T59))
halfF_in_ga(s(s(T85))) → U5_ga(T85, halfF_in_ga(T85))
U4_ga(T59, evenE_out_ga(T59, X87)) → evenE_out_ga(s(s(T59)), X87)
U5_ga(T85, halfF_out_ga(T85, X131)) → halfF_out_ga(s(s(T85)), s(X131))
evenE_in_ga(0) → evenE_out_ga(0, true)
halfF_in_ga(0) → halfF_out_ga(0, 0)
evenE_in_ga(x0)
halfF_in_ga(x0)
U4_ga(x0, x1)
U5_ga(x0, x1)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
PS_IN_GGAA(T165, T166) → TIMESG_IN_GGA(T165, T166)
POL(0) = 0
POL(IFQ_IN_GGGA(x1, x2, x3)) = 1 + x2
POL(PH_IN_GAGA(x1, x2)) = 1 + x1
POL(PR_IN_GAGAA(x1, x2)) = 1 + x1
POL(PS_IN_GGAA(x1, x2)) = 1 + x1
POL(PV_IN_GGAA(x1, x2)) = x1
POL(TIMESG_IN_GGA(x1, x2)) = x1
POL(U24_GAGA(x1, x2, x3)) = 1 + x1
POL(U26_GAGAA(x1, x2, x3)) = x3
POL(U4_ga(x1, x2)) = 0
POL(U5_ga(x1, x2)) = 1 + x2
POL(evenE_in_ga(x1)) = 0
POL(evenE_out_ga(x1, x2)) = 0
POL(false) = 0
POL(halfF_in_ga(x1)) = x1
POL(halfF_out_ga(x1, x2)) = x2
POL(s(x1)) = 1 + x1
POL(true) = 0
halfF_in_ga(s(s(T85))) → U5_ga(T85, halfF_in_ga(T85))
halfF_in_ga(0) → halfF_out_ga(0, 0)
U5_ga(T85, halfF_out_ga(T85, X131)) → halfF_out_ga(s(s(T85)), s(X131))
PH_IN_GAGA(T100, T101) → U24_GAGA(T100, T101, evenE_in_ga(s(T100)))
U24_GAGA(T100, T101, evenE_out_ga(s(T100), T102)) → IFQ_IN_GGGA(T102, T100, T101)
IFQ_IN_GGGA(true, T113, T114) → PR_IN_GAGAA(T113, T114)
PR_IN_GAGAA(T113, T114) → U26_GAGAA(T113, T114, halfF_in_ga(s(T113)))
U26_GAGAA(T113, T114, halfF_out_ga(s(T113), T115)) → PV_IN_GGAA(T115, T114)
PV_IN_GGAA(T115, T114) → TIMESG_IN_GGA(T115, T114)
TIMESG_IN_GGA(s(T100), T101) → PH_IN_GAGA(T100, T101)
IFQ_IN_GGGA(false, T165, T166) → PS_IN_GGAA(T165, T166)
evenE_in_ga(s(0)) → evenE_out_ga(s(0), false)
evenE_in_ga(s(s(T59))) → U4_ga(T59, evenE_in_ga(T59))
halfF_in_ga(s(s(T85))) → U5_ga(T85, halfF_in_ga(T85))
U4_ga(T59, evenE_out_ga(T59, X87)) → evenE_out_ga(s(s(T59)), X87)
U5_ga(T85, halfF_out_ga(T85, X131)) → halfF_out_ga(s(s(T85)), s(X131))
evenE_in_ga(0) → evenE_out_ga(0, true)
halfF_in_ga(0) → halfF_out_ga(0, 0)
evenE_in_ga(x0)
halfF_in_ga(x0)
U4_ga(x0, x1)
U5_ga(x0, x1)
U24_GAGA(T100, T101, evenE_out_ga(s(T100), T102)) → IFQ_IN_GGGA(T102, T100, T101)
IFQ_IN_GGGA(true, T113, T114) → PR_IN_GAGAA(T113, T114)
PR_IN_GAGAA(T113, T114) → U26_GAGAA(T113, T114, halfF_in_ga(s(T113)))
U26_GAGAA(T113, T114, halfF_out_ga(s(T113), T115)) → PV_IN_GGAA(T115, T114)
PV_IN_GGAA(T115, T114) → TIMESG_IN_GGA(T115, T114)
TIMESG_IN_GGA(s(T100), T101) → PH_IN_GAGA(T100, T101)
PH_IN_GAGA(T100, T101) → U24_GAGA(T100, T101, evenE_in_ga(s(T100)))
evenE_in_ga(s(0)) → evenE_out_ga(s(0), false)
evenE_in_ga(s(s(T59))) → U4_ga(T59, evenE_in_ga(T59))
halfF_in_ga(s(s(T85))) → U5_ga(T85, halfF_in_ga(T85))
U4_ga(T59, evenE_out_ga(T59, X87)) → evenE_out_ga(s(s(T59)), X87)
U5_ga(T85, halfF_out_ga(T85, X131)) → halfF_out_ga(s(s(T85)), s(X131))
evenE_in_ga(0) → evenE_out_ga(0, true)
halfF_in_ga(0) → halfF_out_ga(0, 0)
evenE_in_ga(x0)
halfF_in_ga(x0)
U4_ga(x0, x1)
U5_ga(x0, x1)
evenE_in_ga(s(0)) → evenE_out_ga(s(0), false)
POL(0) = 0
POL(IFQ_IN_GGGA(x1, x2, x3)) = x1
POL(PH_IN_GAGA(x1, x2)) = 1
POL(PR_IN_GAGAA(x1, x2)) = 1
POL(PV_IN_GGAA(x1, x2)) = 1
POL(TIMESG_IN_GGA(x1, x2)) = 1
POL(U24_GAGA(x1, x2, x3)) = x3
POL(U26_GAGAA(x1, x2, x3)) = 1
POL(U4_ga(x1, x2)) = x2
POL(U5_ga(x1, x2)) = 0
POL(evenE_in_ga(x1)) = 1
POL(evenE_out_ga(x1, x2)) = x2
POL(false) = 0
POL(halfF_in_ga(x1)) = 0
POL(halfF_out_ga(x1, x2)) = 0
POL(s(x1)) = 0
POL(true) = 1
U24_GAGA(T100, T101, evenE_out_ga(s(T100), T102)) → IFQ_IN_GGGA(T102, T100, T101)
IFQ_IN_GGGA(true, T113, T114) → PR_IN_GAGAA(T113, T114)
PR_IN_GAGAA(T113, T114) → U26_GAGAA(T113, T114, halfF_in_ga(s(T113)))
U26_GAGAA(T113, T114, halfF_out_ga(s(T113), T115)) → PV_IN_GGAA(T115, T114)
PV_IN_GGAA(T115, T114) → TIMESG_IN_GGA(T115, T114)
TIMESG_IN_GGA(s(T100), T101) → PH_IN_GAGA(T100, T101)
PH_IN_GAGA(T100, T101) → U24_GAGA(T100, T101, evenE_in_ga(s(T100)))
evenE_in_ga(s(s(T59))) → U4_ga(T59, evenE_in_ga(T59))
halfF_in_ga(s(s(T85))) → U5_ga(T85, halfF_in_ga(T85))
U4_ga(T59, evenE_out_ga(T59, X87)) → evenE_out_ga(s(s(T59)), X87)
U5_ga(T85, halfF_out_ga(T85, X131)) → halfF_out_ga(s(s(T85)), s(X131))
evenE_in_ga(0) → evenE_out_ga(0, true)
halfF_in_ga(0) → halfF_out_ga(0, 0)
evenE_in_ga(x0)
halfF_in_ga(x0)
U4_ga(x0, x1)
U5_ga(x0, x1)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
U24_GAGA(T100, T101, evenE_out_ga(s(T100), T102)) → IFQ_IN_GGGA(T102, T100, T101)
TIMESG_IN_GGA(s(T100), T101) → PH_IN_GAGA(T100, T101)
POL( U26_GAGAA(x1, ..., x3) ) = x2 + x3
POL( halfF_in_ga(x1) ) = max{0, x1 - 2}
POL( s(x1) ) = 2x1 + 2
POL( U5_ga(x1, x2) ) = 2x1 + 2x2 + 2
POL( U24_GAGA(x1, ..., x3) ) = 2x1 + x2 + 1
POL( evenE_in_ga(x1) ) = 1
POL( U4_ga(x1, x2) ) = x1 + 2
POL( 0 ) = 0
POL( evenE_out_ga(x1, x2) ) = 2x1 + 2
POL( true ) = 0
POL( halfF_out_ga(x1, x2) ) = x2
POL( IFQ_IN_GGGA(x1, ..., x3) ) = 2x2 + x3
POL( PR_IN_GAGAA(x1, x2) ) = 2x1 + x2
POL( PV_IN_GGAA(x1, x2) ) = x1 + x2
POL( TIMESG_IN_GGA(x1, x2) ) = x1 + x2
POL( PH_IN_GAGA(x1, x2) ) = 2x1 + x2 + 1
halfF_in_ga(s(s(T85))) → U5_ga(T85, halfF_in_ga(T85))
halfF_in_ga(0) → halfF_out_ga(0, 0)
U5_ga(T85, halfF_out_ga(T85, X131)) → halfF_out_ga(s(s(T85)), s(X131))
IFQ_IN_GGGA(true, T113, T114) → PR_IN_GAGAA(T113, T114)
PR_IN_GAGAA(T113, T114) → U26_GAGAA(T113, T114, halfF_in_ga(s(T113)))
U26_GAGAA(T113, T114, halfF_out_ga(s(T113), T115)) → PV_IN_GGAA(T115, T114)
PV_IN_GGAA(T115, T114) → TIMESG_IN_GGA(T115, T114)
PH_IN_GAGA(T100, T101) → U24_GAGA(T100, T101, evenE_in_ga(s(T100)))
evenE_in_ga(s(s(T59))) → U4_ga(T59, evenE_in_ga(T59))
halfF_in_ga(s(s(T85))) → U5_ga(T85, halfF_in_ga(T85))
U4_ga(T59, evenE_out_ga(T59, X87)) → evenE_out_ga(s(s(T59)), X87)
U5_ga(T85, halfF_out_ga(T85, X131)) → halfF_out_ga(s(s(T85)), s(X131))
evenE_in_ga(0) → evenE_out_ga(0, true)
halfF_in_ga(0) → halfF_out_ga(0, 0)
evenE_in_ga(x0)
halfF_in_ga(x0)
U4_ga(x0, x1)
U5_ga(x0, x1)
PLUSD_IN_GGA(s(T47), T48, s(T50)) → PLUSD_IN_GGA(T47, T48, T50)
timesA_in_gga(0, T5, 0) → timesA_out_gga(0, T5, 0)
timesA_in_gga(s(0), T21, T23) → U1_gga(T21, T23, pB_in_gaa(T21, X37, T23))
pB_in_gaa(T21, T27, T23) → U16_gaa(T21, T27, T23, timesK_in_ga(T21, T27))
timesK_in_ga(T33, 0) → timesK_out_ga(T33, 0)
U16_gaa(T21, T27, T23, timesK_out_ga(T21, T27)) → U17_gaa(T21, T27, T23, plusD_in_gga(T21, T27, T23))
plusD_in_gga(0, T40, T40) → plusD_out_gga(0, T40, T40)
plusD_in_gga(s(T47), T48, s(T50)) → U3_gga(T47, T48, T50, plusD_in_gga(T47, T48, T50))
U3_gga(T47, T48, T50, plusD_out_gga(T47, T48, T50)) → plusD_out_gga(s(T47), T48, s(T50))
U17_gaa(T21, T27, T23, plusD_out_gga(T21, T27, T23)) → pB_out_gaa(T21, T27, T23)
U1_gga(T21, T23, pB_out_gaa(T21, X37, T23)) → timesA_out_gga(s(0), T21, T23)
timesA_in_gga(s(s(T55)), T10, T12) → U2_gga(T55, T10, T12, pC_in_gaga(T55, X78, T10, T12))
pC_in_gaga(T55, T56, T10, T12) → U18_gaga(T55, T56, T10, T12, evenE_in_ga(T55, T56))
evenE_in_ga(0, true) → evenE_out_ga(0, true)
evenE_in_ga(s(0), false) → evenE_out_ga(s(0), false)
evenE_in_ga(s(s(T59)), X87) → U4_ga(T59, X87, evenE_in_ga(T59, X87))
U4_ga(T59, X87, evenE_out_ga(T59, X87)) → evenE_out_ga(s(s(T59)), X87)
U18_gaga(T55, T56, T10, T12, evenE_out_ga(T55, T56)) → U19_gaga(T55, T56, T10, T12, ifL_in_ggga(T56, T55, T10, T12))
ifL_in_ggga(true, T75, T76, T78) → U9_ggga(T75, T76, T78, pM_in_gagaa(T75, X112, T76, X113, T78))
pM_in_gagaa(T75, T79, T76, X113, T78) → U20_gagaa(T75, T79, T76, X113, T78, halfO_in_ga(T75, T79))
halfO_in_ga(T82, s(X122)) → U11_ga(T82, X122, halfF_in_ga(T82, X122))
halfF_in_ga(0, 0) → halfF_out_ga(0, 0)
halfF_in_ga(s(s(T85)), s(X131)) → U5_ga(T85, X131, halfF_in_ga(T85, X131))
U5_ga(T85, X131, halfF_out_ga(T85, X131)) → halfF_out_ga(s(s(T85)), s(X131))
U11_ga(T82, X122, halfF_out_ga(T82, X122)) → halfO_out_ga(T82, s(X122))
U20_gagaa(T75, T79, T76, X113, T78, halfO_out_ga(T75, T79)) → U21_gagaa(T75, T79, T76, X113, T78, pU_in_ggaa(T79, T76, X113, T78))
pU_in_ggaa(T79, T76, T88, T78) → U22_ggaa(T79, T76, T88, T78, timesG_in_gga(T79, T76, T88))
timesG_in_gga(0, T95, 0) → timesG_out_gga(0, T95, 0)
timesG_in_gga(s(T100), T101, X154) → U6_gga(T100, T101, X154, pH_in_gaga(T100, X153, T101, X154))
pH_in_gaga(T100, T102, T101, X154) → U24_gaga(T100, T102, T101, X154, evenE_in_ga(s(T100), T102))
U24_gaga(T100, T102, T101, X154, evenE_out_ga(s(T100), T102)) → U25_gaga(T100, T102, T101, X154, ifQ_in_ggga(T102, T100, T101, X154))
ifQ_in_ggga(true, T113, T114, X186) → U13_ggga(T113, T114, X186, pR_in_gagaa(T113, X184, T114, X185, X186))
pR_in_gagaa(T113, T115, T114, X185, X186) → U26_gagaa(T113, T115, T114, X185, X186, halfF_in_ga(s(T113), T115))
U26_gagaa(T113, T115, T114, X185, X186, halfF_out_ga(s(T113), T115)) → U27_gagaa(T113, T115, T114, X185, X186, pV_in_ggaa(T115, T114, X185, X186))
pV_in_ggaa(T115, T114, T118, X186) → U28_ggaa(T115, T114, T118, X186, timesG_in_gga(T115, T114, T118))
U28_ggaa(T115, T114, T118, X186, timesG_out_gga(T115, T114, T118)) → U29_ggaa(T115, T114, T118, X186, plusT_in_ga(T118, X186))
plusT_in_ga(0, 0) → plusT_out_ga(0, 0)
plusT_in_ga(s(0), s(s(0))) → plusT_out_ga(s(0), s(s(0)))
plusT_in_ga(s(s(0)), s(s(s(s(0))))) → plusT_out_ga(s(s(0)), s(s(s(s(0)))))
plusT_in_ga(s(s(s(0))), s(s(s(s(s(s(0))))))) → plusT_out_ga(s(s(s(0))), s(s(s(s(s(s(0)))))))
plusT_in_ga(s(s(s(s(0)))), s(s(s(s(s(s(s(s(0))))))))) → plusT_out_ga(s(s(s(s(0)))), s(s(s(s(s(s(s(s(0)))))))))
plusT_in_ga(s(s(s(s(s(0))))), s(s(s(s(s(s(s(s(s(s(0))))))))))) → plusT_out_ga(s(s(s(s(s(0))))), s(s(s(s(s(s(s(s(s(s(0)))))))))))
plusT_in_ga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))) → plusT_out_ga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))
plusT_in_ga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))))) → plusT_out_ga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))))
plusT_in_ga(s(s(s(s(s(s(s(s(T144)))))))), s(s(s(s(s(s(s(s(X342))))))))) → U15_ga(T144, X342, plusI_in_gga(T144, s(s(s(s(s(s(s(T144))))))), X342))
plusI_in_gga(0, T152, s(T152)) → plusI_out_gga(0, T152, s(T152))
plusI_in_gga(s(T157), T158, s(X363)) → U7_gga(T157, T158, X363, plusI_in_gga(T157, T158, X363))
U7_gga(T157, T158, X363, plusI_out_gga(T157, T158, X363)) → plusI_out_gga(s(T157), T158, s(X363))
U15_ga(T144, X342, plusI_out_gga(T144, s(s(s(s(s(s(s(T144))))))), X342)) → plusT_out_ga(s(s(s(s(s(s(s(s(T144)))))))), s(s(s(s(s(s(s(s(X342)))))))))
U29_ggaa(T115, T114, T118, X186, plusT_out_ga(T118, X186)) → pV_out_ggaa(T115, T114, T118, X186)
U27_gagaa(T113, T115, T114, X185, X186, pV_out_ggaa(T115, T114, X185, X186)) → pR_out_gagaa(T113, T115, T114, X185, X186)
U13_ggga(T113, T114, X186, pR_out_gagaa(T113, X184, T114, X185, X186)) → ifQ_out_ggga(true, T113, T114, X186)
ifQ_in_ggga(false, T165, T166, X379) → U14_ggga(T165, T166, X379, pS_in_ggaa(T165, T166, X378, X379))
pS_in_ggaa(T165, T166, T169, X379) → U30_ggaa(T165, T166, T169, X379, timesG_in_gga(T165, T166, T169))
U30_ggaa(T165, T166, T169, X379, timesG_out_gga(T165, T166, T169)) → U31_ggaa(T165, T166, T169, X379, plusJ_in_gga(T166, T169, X379))
plusJ_in_gga(0, T178, T178) → plusJ_out_gga(0, T178, T178)
plusJ_in_gga(s(T183), T184, s(X402)) → U8_gga(T183, T184, X402, plusJ_in_gga(T183, T184, X402))
U8_gga(T183, T184, X402, plusJ_out_gga(T183, T184, X402)) → plusJ_out_gga(s(T183), T184, s(X402))
U31_ggaa(T165, T166, T169, X379, plusJ_out_gga(T166, T169, X379)) → pS_out_ggaa(T165, T166, T169, X379)
U14_ggga(T165, T166, X379, pS_out_ggaa(T165, T166, X378, X379)) → ifQ_out_ggga(false, T165, T166, X379)
U25_gaga(T100, T102, T101, X154, ifQ_out_ggga(T102, T100, T101, X154)) → pH_out_gaga(T100, T102, T101, X154)
U6_gga(T100, T101, X154, pH_out_gaga(T100, X153, T101, X154)) → timesG_out_gga(s(T100), T101, X154)
U22_ggaa(T79, T76, T88, T78, timesG_out_gga(T79, T76, T88)) → U23_ggaa(T79, T76, T88, T78, plusP_in_ga(T88, T78))
plusP_in_ga(0, 0) → plusP_out_ga(0, 0)
plusP_in_ga(s(0), s(s(0))) → plusP_out_ga(s(0), s(s(0)))
plusP_in_ga(s(s(0)), s(s(s(s(0))))) → plusP_out_ga(s(s(0)), s(s(s(s(0)))))
plusP_in_ga(s(s(s(0))), s(s(s(s(s(s(0))))))) → plusP_out_ga(s(s(s(0))), s(s(s(s(s(s(0)))))))
plusP_in_ga(s(s(s(s(0)))), s(s(s(s(s(s(s(s(0))))))))) → plusP_out_ga(s(s(s(s(0)))), s(s(s(s(s(s(s(s(0)))))))))
plusP_in_ga(s(s(s(s(s(0))))), s(s(s(s(s(s(s(s(s(s(0))))))))))) → plusP_out_ga(s(s(s(s(s(0))))), s(s(s(s(s(s(s(s(s(s(0)))))))))))
plusP_in_ga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))) → plusP_out_ga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))
plusP_in_ga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))))) → plusP_out_ga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))))
plusP_in_ga(s(s(s(s(s(s(s(s(T240)))))))), s(s(s(s(s(s(s(s(T242))))))))) → U12_ga(T240, T242, plusD_in_gga(T240, s(s(s(s(s(s(s(s(T240)))))))), T242))
U12_ga(T240, T242, plusD_out_gga(T240, s(s(s(s(s(s(s(s(T240)))))))), T242)) → plusP_out_ga(s(s(s(s(s(s(s(s(T240)))))))), s(s(s(s(s(s(s(s(T242)))))))))
U23_ggaa(T79, T76, T88, T78, plusP_out_ga(T88, T78)) → pU_out_ggaa(T79, T76, T88, T78)
U21_gagaa(T75, T79, T76, X113, T78, pU_out_ggaa(T79, T76, X113, T78)) → pM_out_gagaa(T75, T79, T76, X113, T78)
U9_ggga(T75, T76, T78, pM_out_gagaa(T75, X112, T76, X113, T78)) → ifL_out_ggga(true, T75, T76, T78)
ifL_in_ggga(false, T252, T253, T255) → U10_ggga(T252, T253, T255, pN_in_ggaa(T252, T253, X547, T255))
pN_in_ggaa(T252, T253, T256, T255) → U32_ggaa(T252, T253, T256, T255, timesG_in_gga(s(T252), T253, T256))
U32_ggaa(T252, T253, T256, T255, timesG_out_gga(s(T252), T253, T256)) → U33_ggaa(T252, T253, T256, T255, plusD_in_gga(T253, T256, T255))
U33_ggaa(T252, T253, T256, T255, plusD_out_gga(T253, T256, T255)) → pN_out_ggaa(T252, T253, T256, T255)
U10_ggga(T252, T253, T255, pN_out_ggaa(T252, T253, X547, T255)) → ifL_out_ggga(false, T252, T253, T255)
U19_gaga(T55, T56, T10, T12, ifL_out_ggga(T56, T55, T10, T12)) → pC_out_gaga(T55, T56, T10, T12)
U2_gga(T55, T10, T12, pC_out_gaga(T55, X78, T10, T12)) → timesA_out_gga(s(s(T55)), T10, T12)
PLUSD_IN_GGA(s(T47), T48, s(T50)) → PLUSD_IN_GGA(T47, T48, T50)
PLUSD_IN_GGA(s(T47), T48) → PLUSD_IN_GGA(T47, T48)
From the DPs we obtained the following set of size-change graphs: