0 Prolog
↳1 PrologToPiTRSViaGraphTransformerProof (⇒, 1035 ms)
↳2 PiTRS
↳3 DependencyPairsProof (⇔, 917 ms)
↳4 PiDP
↳5 DependencyGraphProof (⇔, 210 ms)
↳6 AND
↳7 PiDP
↳8 UsableRulesProof (⇔, 0 ms)
↳9 PiDP
↳10 PiDPToQDPProof (⇒, 2 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 (⇒, 0 ms)
↳39 QDP
↳40 QDPSizeChangeProof (⇔, 0 ms)
↳41 YES
↳42 PiDP
↳43 UsableRulesProof (⇔, 0 ms)
↳44 PiDP
↳45 PiDPToQDPProof (⇒, 0 ms)
↳46 QDP
↳47 QDPSizeChangeProof (⇔, 0 ms)
↳48 YES
↳49 PiDP
↳50 UsableRulesProof (⇔, 0 ms)
↳51 PiDP
↳52 PiDPToQDPProof (⇒, 0 ms)
↳53 QDP
↳54 QDPSizeChangeProof (⇔, 0 ms)
↳55 YES
↳56 PiDP
↳57 UsableRulesProof (⇔, 0 ms)
↳58 PiDP
↳59 PiDPToQDPProof (⇒, 0 ms)
↳60 QDP
↳61 QDPSizeChangeProof (⇔, 0 ms)
↳62 YES
↳63 PiDP
↳64 UsableRulesProof (⇔, 0 ms)
↳65 PiDP
↳66 PiDPToQDPProof (⇒, 0 ms)
↳67 QDP
↳68 QDPSizeChangeProof (⇔, 0 ms)
↳69 YES
timesA_in_gga(0, T15, 0) → timesA_out_gga(0, T15, 0)
timesA_in_gga(s(T28), T29, T31) → U1_gga(T28, T29, T31, multB_in_gga(T28, T29, T31))
multB_in_gga(0, 0, 0) → multB_out_gga(0, 0, 0)
multB_in_gga(s(T51), 0, T54) → U12_gga(T51, T54, multC_in_ga(T51, T54))
multC_in_ga(0, 0) → multC_out_ga(0, 0)
multC_in_ga(s(T63), T65) → U2_ga(T63, T65, multC_in_ga(T63, T65))
U2_ga(T63, T65, multC_out_ga(T63, T65)) → multC_out_ga(s(T63), T65)
U12_gga(T51, T54, multC_out_ga(T51, T54)) → multB_out_gga(s(T51), 0, T54)
multB_in_gga(0, s(0), s(0)) → multB_out_gga(0, s(0), s(0))
multB_in_gga(s(T99), s(0), s(T102)) → U13_gga(T99, T102, multD_in_ga(T99, T102))
multD_in_ga(0, s(0)) → multD_out_ga(0, s(0))
multD_in_ga(s(T119), s(T121)) → U3_ga(T119, T121, multD_in_ga(T119, T121))
U3_ga(T119, T121, multD_out_ga(T119, T121)) → multD_out_ga(s(T119), s(T121))
U13_gga(T99, T102, multD_out_ga(T99, T102)) → multB_out_gga(s(T99), s(0), s(T102))
multB_in_gga(0, s(s(0)), s(s(0))) → multB_out_gga(0, s(s(0)), s(s(0)))
multB_in_gga(s(T155), s(s(0)), s(s(T158))) → U14_gga(T155, T158, multE_in_ga(T155, T158))
multE_in_ga(0, s(s(0))) → multE_out_ga(0, s(s(0)))
multE_in_ga(s(T183), s(s(T185))) → U4_ga(T183, T185, multE_in_ga(T183, T185))
U4_ga(T183, T185, multE_out_ga(T183, T185)) → multE_out_ga(s(T183), s(s(T185)))
U14_gga(T155, T158, multE_out_ga(T155, T158)) → multB_out_gga(s(T155), s(s(0)), s(s(T158)))
multB_in_gga(0, s(s(s(0))), s(s(s(0)))) → multB_out_gga(0, s(s(s(0))), s(s(s(0))))
multB_in_gga(s(T219), s(s(s(0))), s(s(s(T222)))) → U15_gga(T219, T222, multF_in_ga(T219, T222))
multF_in_ga(0, s(s(s(0)))) → multF_out_ga(0, s(s(s(0))))
multF_in_ga(s(T255), s(s(s(T257)))) → U5_ga(T255, T257, multF_in_ga(T255, T257))
U5_ga(T255, T257, multF_out_ga(T255, T257)) → multF_out_ga(s(T255), s(s(s(T257))))
U15_gga(T219, T222, multF_out_ga(T219, T222)) → multB_out_gga(s(T219), s(s(s(0))), s(s(s(T222))))
multB_in_gga(0, s(s(s(s(0)))), s(s(s(s(0))))) → multB_out_gga(0, s(s(s(s(0)))), s(s(s(s(0)))))
multB_in_gga(s(T291), s(s(s(s(0)))), s(s(s(s(T294))))) → U16_gga(T291, T294, multG_in_ga(T291, T294))
multG_in_ga(0, s(s(s(s(0))))) → multG_out_ga(0, s(s(s(s(0)))))
multG_in_ga(s(T335), s(s(s(s(T337))))) → U6_ga(T335, T337, multG_in_ga(T335, T337))
U6_ga(T335, T337, multG_out_ga(T335, T337)) → multG_out_ga(s(T335), s(s(s(s(T337)))))
U16_gga(T291, T294, multG_out_ga(T291, T294)) → multB_out_gga(s(T291), s(s(s(s(0)))), s(s(s(s(T294)))))
multB_in_gga(0, s(s(s(s(s(0))))), s(s(s(s(s(0)))))) → multB_out_gga(0, s(s(s(s(s(0))))), s(s(s(s(s(0))))))
multB_in_gga(s(T371), s(s(s(s(s(0))))), s(s(s(s(s(T374)))))) → U17_gga(T371, T374, multH_in_ga(T371, T374))
multH_in_ga(0, s(s(s(s(s(0)))))) → multH_out_ga(0, s(s(s(s(s(0))))))
multH_in_ga(s(T423), s(s(s(s(s(T425)))))) → U7_ga(T423, T425, multH_in_ga(T423, T425))
U7_ga(T423, T425, multH_out_ga(T423, T425)) → multH_out_ga(s(T423), s(s(s(s(s(T425))))))
U17_gga(T371, T374, multH_out_ga(T371, T374)) → multB_out_gga(s(T371), s(s(s(s(s(0))))), s(s(s(s(s(T374))))))
multB_in_gga(0, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(0))))))) → multB_out_gga(0, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(0)))))))
multB_in_gga(s(T459), s(s(s(s(s(s(0)))))), s(s(s(s(s(s(T462))))))) → U18_gga(T459, T462, multI_in_ga(T459, T462))
multI_in_ga(0, s(s(s(s(s(s(0))))))) → multI_out_ga(0, s(s(s(s(s(s(0)))))))
multI_in_ga(s(T519), s(s(s(s(s(s(T521))))))) → U8_ga(T519, T521, multI_in_ga(T519, T521))
U8_ga(T519, T521, multI_out_ga(T519, T521)) → multI_out_ga(s(T519), s(s(s(s(s(s(T521)))))))
U18_gga(T459, T462, multI_out_ga(T459, T462)) → multB_out_gga(s(T459), s(s(s(s(s(s(0)))))), s(s(s(s(s(s(T462)))))))
multB_in_gga(0, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(0)))))))) → multB_out_gga(0, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(0))))))))
multB_in_gga(s(T555), s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(T558)))))))) → U19_gga(T555, T558, multJ_in_ga(T555, T558))
multJ_in_ga(0, s(s(s(s(s(s(s(0)))))))) → multJ_out_ga(0, s(s(s(s(s(s(s(0))))))))
multJ_in_ga(s(T623), s(s(s(s(s(s(s(T625)))))))) → U9_ga(T623, T625, multJ_in_ga(T623, T625))
U9_ga(T623, T625, multJ_out_ga(T623, T625)) → multJ_out_ga(s(T623), s(s(s(s(s(s(s(T625))))))))
U19_gga(T555, T558, multJ_out_ga(T555, T558)) → multB_out_gga(s(T555), s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(T558))))))))
multB_in_gga(T635, s(s(s(s(s(s(s(s(T637)))))))), s(s(s(s(s(s(s(s(T639))))))))) → U20_gga(T635, T637, T639, multK_in_ggga(T635, s(s(s(s(s(s(s(T637))))))), T637, T639))
multK_in_ggga(0, T649, 0, 0) → multK_out_ggga(0, T649, 0, 0)
multK_in_ggga(s(T662), T663, 0, T665) → U10_ggga(T662, T663, T665, multB_in_gga(T662, s(T663), T665))
U10_ggga(T662, T663, T665, multB_out_gga(T662, s(T663), T665)) → multK_out_ggga(s(T662), T663, 0, T665)
multK_in_ggga(T676, T677, s(T678), s(T680)) → U11_ggga(T676, T677, T678, T680, multK_in_ggga(T676, T677, T678, T680))
U11_ggga(T676, T677, T678, T680, multK_out_ggga(T676, T677, T678, T680)) → multK_out_ggga(T676, T677, s(T678), s(T680))
U20_gga(T635, T637, T639, multK_out_ggga(T635, s(s(s(s(s(s(s(T637))))))), T637, T639)) → multB_out_gga(T635, s(s(s(s(s(s(s(s(T637)))))))), s(s(s(s(s(s(s(s(T639)))))))))
U1_gga(T28, T29, T31, multB_out_gga(T28, T29, T31)) → timesA_out_gga(s(T28), T29, T31)
TIMESA_IN_GGA(s(T28), T29, T31) → U1_GGA(T28, T29, T31, multB_in_gga(T28, T29, T31))
TIMESA_IN_GGA(s(T28), T29, T31) → MULTB_IN_GGA(T28, T29, T31)
MULTB_IN_GGA(s(T51), 0, T54) → U12_GGA(T51, T54, multC_in_ga(T51, T54))
MULTB_IN_GGA(s(T51), 0, T54) → MULTC_IN_GA(T51, T54)
MULTC_IN_GA(s(T63), T65) → U2_GA(T63, T65, multC_in_ga(T63, T65))
MULTC_IN_GA(s(T63), T65) → MULTC_IN_GA(T63, T65)
MULTB_IN_GGA(s(T99), s(0), s(T102)) → U13_GGA(T99, T102, multD_in_ga(T99, T102))
MULTB_IN_GGA(s(T99), s(0), s(T102)) → MULTD_IN_GA(T99, T102)
MULTD_IN_GA(s(T119), s(T121)) → U3_GA(T119, T121, multD_in_ga(T119, T121))
MULTD_IN_GA(s(T119), s(T121)) → MULTD_IN_GA(T119, T121)
MULTB_IN_GGA(s(T155), s(s(0)), s(s(T158))) → U14_GGA(T155, T158, multE_in_ga(T155, T158))
MULTB_IN_GGA(s(T155), s(s(0)), s(s(T158))) → MULTE_IN_GA(T155, T158)
MULTE_IN_GA(s(T183), s(s(T185))) → U4_GA(T183, T185, multE_in_ga(T183, T185))
MULTE_IN_GA(s(T183), s(s(T185))) → MULTE_IN_GA(T183, T185)
MULTB_IN_GGA(s(T219), s(s(s(0))), s(s(s(T222)))) → U15_GGA(T219, T222, multF_in_ga(T219, T222))
MULTB_IN_GGA(s(T219), s(s(s(0))), s(s(s(T222)))) → MULTF_IN_GA(T219, T222)
MULTF_IN_GA(s(T255), s(s(s(T257)))) → U5_GA(T255, T257, multF_in_ga(T255, T257))
MULTF_IN_GA(s(T255), s(s(s(T257)))) → MULTF_IN_GA(T255, T257)
MULTB_IN_GGA(s(T291), s(s(s(s(0)))), s(s(s(s(T294))))) → U16_GGA(T291, T294, multG_in_ga(T291, T294))
MULTB_IN_GGA(s(T291), s(s(s(s(0)))), s(s(s(s(T294))))) → MULTG_IN_GA(T291, T294)
MULTG_IN_GA(s(T335), s(s(s(s(T337))))) → U6_GA(T335, T337, multG_in_ga(T335, T337))
MULTG_IN_GA(s(T335), s(s(s(s(T337))))) → MULTG_IN_GA(T335, T337)
MULTB_IN_GGA(s(T371), s(s(s(s(s(0))))), s(s(s(s(s(T374)))))) → U17_GGA(T371, T374, multH_in_ga(T371, T374))
MULTB_IN_GGA(s(T371), s(s(s(s(s(0))))), s(s(s(s(s(T374)))))) → MULTH_IN_GA(T371, T374)
MULTH_IN_GA(s(T423), s(s(s(s(s(T425)))))) → U7_GA(T423, T425, multH_in_ga(T423, T425))
MULTH_IN_GA(s(T423), s(s(s(s(s(T425)))))) → MULTH_IN_GA(T423, T425)
MULTB_IN_GGA(s(T459), s(s(s(s(s(s(0)))))), s(s(s(s(s(s(T462))))))) → U18_GGA(T459, T462, multI_in_ga(T459, T462))
MULTB_IN_GGA(s(T459), s(s(s(s(s(s(0)))))), s(s(s(s(s(s(T462))))))) → MULTI_IN_GA(T459, T462)
MULTI_IN_GA(s(T519), s(s(s(s(s(s(T521))))))) → U8_GA(T519, T521, multI_in_ga(T519, T521))
MULTI_IN_GA(s(T519), s(s(s(s(s(s(T521))))))) → MULTI_IN_GA(T519, T521)
MULTB_IN_GGA(s(T555), s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(T558)))))))) → U19_GGA(T555, T558, multJ_in_ga(T555, T558))
MULTB_IN_GGA(s(T555), s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(T558)))))))) → MULTJ_IN_GA(T555, T558)
MULTJ_IN_GA(s(T623), s(s(s(s(s(s(s(T625)))))))) → U9_GA(T623, T625, multJ_in_ga(T623, T625))
MULTJ_IN_GA(s(T623), s(s(s(s(s(s(s(T625)))))))) → MULTJ_IN_GA(T623, T625)
MULTB_IN_GGA(T635, s(s(s(s(s(s(s(s(T637)))))))), s(s(s(s(s(s(s(s(T639))))))))) → U20_GGA(T635, T637, T639, multK_in_ggga(T635, s(s(s(s(s(s(s(T637))))))), T637, T639))
MULTB_IN_GGA(T635, s(s(s(s(s(s(s(s(T637)))))))), s(s(s(s(s(s(s(s(T639))))))))) → MULTK_IN_GGGA(T635, s(s(s(s(s(s(s(T637))))))), T637, T639)
MULTK_IN_GGGA(s(T662), T663, 0, T665) → U10_GGGA(T662, T663, T665, multB_in_gga(T662, s(T663), T665))
MULTK_IN_GGGA(s(T662), T663, 0, T665) → MULTB_IN_GGA(T662, s(T663), T665)
MULTK_IN_GGGA(T676, T677, s(T678), s(T680)) → U11_GGGA(T676, T677, T678, T680, multK_in_ggga(T676, T677, T678, T680))
MULTK_IN_GGGA(T676, T677, s(T678), s(T680)) → MULTK_IN_GGGA(T676, T677, T678, T680)
timesA_in_gga(0, T15, 0) → timesA_out_gga(0, T15, 0)
timesA_in_gga(s(T28), T29, T31) → U1_gga(T28, T29, T31, multB_in_gga(T28, T29, T31))
multB_in_gga(0, 0, 0) → multB_out_gga(0, 0, 0)
multB_in_gga(s(T51), 0, T54) → U12_gga(T51, T54, multC_in_ga(T51, T54))
multC_in_ga(0, 0) → multC_out_ga(0, 0)
multC_in_ga(s(T63), T65) → U2_ga(T63, T65, multC_in_ga(T63, T65))
U2_ga(T63, T65, multC_out_ga(T63, T65)) → multC_out_ga(s(T63), T65)
U12_gga(T51, T54, multC_out_ga(T51, T54)) → multB_out_gga(s(T51), 0, T54)
multB_in_gga(0, s(0), s(0)) → multB_out_gga(0, s(0), s(0))
multB_in_gga(s(T99), s(0), s(T102)) → U13_gga(T99, T102, multD_in_ga(T99, T102))
multD_in_ga(0, s(0)) → multD_out_ga(0, s(0))
multD_in_ga(s(T119), s(T121)) → U3_ga(T119, T121, multD_in_ga(T119, T121))
U3_ga(T119, T121, multD_out_ga(T119, T121)) → multD_out_ga(s(T119), s(T121))
U13_gga(T99, T102, multD_out_ga(T99, T102)) → multB_out_gga(s(T99), s(0), s(T102))
multB_in_gga(0, s(s(0)), s(s(0))) → multB_out_gga(0, s(s(0)), s(s(0)))
multB_in_gga(s(T155), s(s(0)), s(s(T158))) → U14_gga(T155, T158, multE_in_ga(T155, T158))
multE_in_ga(0, s(s(0))) → multE_out_ga(0, s(s(0)))
multE_in_ga(s(T183), s(s(T185))) → U4_ga(T183, T185, multE_in_ga(T183, T185))
U4_ga(T183, T185, multE_out_ga(T183, T185)) → multE_out_ga(s(T183), s(s(T185)))
U14_gga(T155, T158, multE_out_ga(T155, T158)) → multB_out_gga(s(T155), s(s(0)), s(s(T158)))
multB_in_gga(0, s(s(s(0))), s(s(s(0)))) → multB_out_gga(0, s(s(s(0))), s(s(s(0))))
multB_in_gga(s(T219), s(s(s(0))), s(s(s(T222)))) → U15_gga(T219, T222, multF_in_ga(T219, T222))
multF_in_ga(0, s(s(s(0)))) → multF_out_ga(0, s(s(s(0))))
multF_in_ga(s(T255), s(s(s(T257)))) → U5_ga(T255, T257, multF_in_ga(T255, T257))
U5_ga(T255, T257, multF_out_ga(T255, T257)) → multF_out_ga(s(T255), s(s(s(T257))))
U15_gga(T219, T222, multF_out_ga(T219, T222)) → multB_out_gga(s(T219), s(s(s(0))), s(s(s(T222))))
multB_in_gga(0, s(s(s(s(0)))), s(s(s(s(0))))) → multB_out_gga(0, s(s(s(s(0)))), s(s(s(s(0)))))
multB_in_gga(s(T291), s(s(s(s(0)))), s(s(s(s(T294))))) → U16_gga(T291, T294, multG_in_ga(T291, T294))
multG_in_ga(0, s(s(s(s(0))))) → multG_out_ga(0, s(s(s(s(0)))))
multG_in_ga(s(T335), s(s(s(s(T337))))) → U6_ga(T335, T337, multG_in_ga(T335, T337))
U6_ga(T335, T337, multG_out_ga(T335, T337)) → multG_out_ga(s(T335), s(s(s(s(T337)))))
U16_gga(T291, T294, multG_out_ga(T291, T294)) → multB_out_gga(s(T291), s(s(s(s(0)))), s(s(s(s(T294)))))
multB_in_gga(0, s(s(s(s(s(0))))), s(s(s(s(s(0)))))) → multB_out_gga(0, s(s(s(s(s(0))))), s(s(s(s(s(0))))))
multB_in_gga(s(T371), s(s(s(s(s(0))))), s(s(s(s(s(T374)))))) → U17_gga(T371, T374, multH_in_ga(T371, T374))
multH_in_ga(0, s(s(s(s(s(0)))))) → multH_out_ga(0, s(s(s(s(s(0))))))
multH_in_ga(s(T423), s(s(s(s(s(T425)))))) → U7_ga(T423, T425, multH_in_ga(T423, T425))
U7_ga(T423, T425, multH_out_ga(T423, T425)) → multH_out_ga(s(T423), s(s(s(s(s(T425))))))
U17_gga(T371, T374, multH_out_ga(T371, T374)) → multB_out_gga(s(T371), s(s(s(s(s(0))))), s(s(s(s(s(T374))))))
multB_in_gga(0, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(0))))))) → multB_out_gga(0, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(0)))))))
multB_in_gga(s(T459), s(s(s(s(s(s(0)))))), s(s(s(s(s(s(T462))))))) → U18_gga(T459, T462, multI_in_ga(T459, T462))
multI_in_ga(0, s(s(s(s(s(s(0))))))) → multI_out_ga(0, s(s(s(s(s(s(0)))))))
multI_in_ga(s(T519), s(s(s(s(s(s(T521))))))) → U8_ga(T519, T521, multI_in_ga(T519, T521))
U8_ga(T519, T521, multI_out_ga(T519, T521)) → multI_out_ga(s(T519), s(s(s(s(s(s(T521)))))))
U18_gga(T459, T462, multI_out_ga(T459, T462)) → multB_out_gga(s(T459), s(s(s(s(s(s(0)))))), s(s(s(s(s(s(T462)))))))
multB_in_gga(0, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(0)))))))) → multB_out_gga(0, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(0))))))))
multB_in_gga(s(T555), s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(T558)))))))) → U19_gga(T555, T558, multJ_in_ga(T555, T558))
multJ_in_ga(0, s(s(s(s(s(s(s(0)))))))) → multJ_out_ga(0, s(s(s(s(s(s(s(0))))))))
multJ_in_ga(s(T623), s(s(s(s(s(s(s(T625)))))))) → U9_ga(T623, T625, multJ_in_ga(T623, T625))
U9_ga(T623, T625, multJ_out_ga(T623, T625)) → multJ_out_ga(s(T623), s(s(s(s(s(s(s(T625))))))))
U19_gga(T555, T558, multJ_out_ga(T555, T558)) → multB_out_gga(s(T555), s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(T558))))))))
multB_in_gga(T635, s(s(s(s(s(s(s(s(T637)))))))), s(s(s(s(s(s(s(s(T639))))))))) → U20_gga(T635, T637, T639, multK_in_ggga(T635, s(s(s(s(s(s(s(T637))))))), T637, T639))
multK_in_ggga(0, T649, 0, 0) → multK_out_ggga(0, T649, 0, 0)
multK_in_ggga(s(T662), T663, 0, T665) → U10_ggga(T662, T663, T665, multB_in_gga(T662, s(T663), T665))
U10_ggga(T662, T663, T665, multB_out_gga(T662, s(T663), T665)) → multK_out_ggga(s(T662), T663, 0, T665)
multK_in_ggga(T676, T677, s(T678), s(T680)) → U11_ggga(T676, T677, T678, T680, multK_in_ggga(T676, T677, T678, T680))
U11_ggga(T676, T677, T678, T680, multK_out_ggga(T676, T677, T678, T680)) → multK_out_ggga(T676, T677, s(T678), s(T680))
U20_gga(T635, T637, T639, multK_out_ggga(T635, s(s(s(s(s(s(s(T637))))))), T637, T639)) → multB_out_gga(T635, s(s(s(s(s(s(s(s(T637)))))))), s(s(s(s(s(s(s(s(T639)))))))))
U1_gga(T28, T29, T31, multB_out_gga(T28, T29, T31)) → timesA_out_gga(s(T28), T29, T31)
TIMESA_IN_GGA(s(T28), T29, T31) → U1_GGA(T28, T29, T31, multB_in_gga(T28, T29, T31))
TIMESA_IN_GGA(s(T28), T29, T31) → MULTB_IN_GGA(T28, T29, T31)
MULTB_IN_GGA(s(T51), 0, T54) → U12_GGA(T51, T54, multC_in_ga(T51, T54))
MULTB_IN_GGA(s(T51), 0, T54) → MULTC_IN_GA(T51, T54)
MULTC_IN_GA(s(T63), T65) → U2_GA(T63, T65, multC_in_ga(T63, T65))
MULTC_IN_GA(s(T63), T65) → MULTC_IN_GA(T63, T65)
MULTB_IN_GGA(s(T99), s(0), s(T102)) → U13_GGA(T99, T102, multD_in_ga(T99, T102))
MULTB_IN_GGA(s(T99), s(0), s(T102)) → MULTD_IN_GA(T99, T102)
MULTD_IN_GA(s(T119), s(T121)) → U3_GA(T119, T121, multD_in_ga(T119, T121))
MULTD_IN_GA(s(T119), s(T121)) → MULTD_IN_GA(T119, T121)
MULTB_IN_GGA(s(T155), s(s(0)), s(s(T158))) → U14_GGA(T155, T158, multE_in_ga(T155, T158))
MULTB_IN_GGA(s(T155), s(s(0)), s(s(T158))) → MULTE_IN_GA(T155, T158)
MULTE_IN_GA(s(T183), s(s(T185))) → U4_GA(T183, T185, multE_in_ga(T183, T185))
MULTE_IN_GA(s(T183), s(s(T185))) → MULTE_IN_GA(T183, T185)
MULTB_IN_GGA(s(T219), s(s(s(0))), s(s(s(T222)))) → U15_GGA(T219, T222, multF_in_ga(T219, T222))
MULTB_IN_GGA(s(T219), s(s(s(0))), s(s(s(T222)))) → MULTF_IN_GA(T219, T222)
MULTF_IN_GA(s(T255), s(s(s(T257)))) → U5_GA(T255, T257, multF_in_ga(T255, T257))
MULTF_IN_GA(s(T255), s(s(s(T257)))) → MULTF_IN_GA(T255, T257)
MULTB_IN_GGA(s(T291), s(s(s(s(0)))), s(s(s(s(T294))))) → U16_GGA(T291, T294, multG_in_ga(T291, T294))
MULTB_IN_GGA(s(T291), s(s(s(s(0)))), s(s(s(s(T294))))) → MULTG_IN_GA(T291, T294)
MULTG_IN_GA(s(T335), s(s(s(s(T337))))) → U6_GA(T335, T337, multG_in_ga(T335, T337))
MULTG_IN_GA(s(T335), s(s(s(s(T337))))) → MULTG_IN_GA(T335, T337)
MULTB_IN_GGA(s(T371), s(s(s(s(s(0))))), s(s(s(s(s(T374)))))) → U17_GGA(T371, T374, multH_in_ga(T371, T374))
MULTB_IN_GGA(s(T371), s(s(s(s(s(0))))), s(s(s(s(s(T374)))))) → MULTH_IN_GA(T371, T374)
MULTH_IN_GA(s(T423), s(s(s(s(s(T425)))))) → U7_GA(T423, T425, multH_in_ga(T423, T425))
MULTH_IN_GA(s(T423), s(s(s(s(s(T425)))))) → MULTH_IN_GA(T423, T425)
MULTB_IN_GGA(s(T459), s(s(s(s(s(s(0)))))), s(s(s(s(s(s(T462))))))) → U18_GGA(T459, T462, multI_in_ga(T459, T462))
MULTB_IN_GGA(s(T459), s(s(s(s(s(s(0)))))), s(s(s(s(s(s(T462))))))) → MULTI_IN_GA(T459, T462)
MULTI_IN_GA(s(T519), s(s(s(s(s(s(T521))))))) → U8_GA(T519, T521, multI_in_ga(T519, T521))
MULTI_IN_GA(s(T519), s(s(s(s(s(s(T521))))))) → MULTI_IN_GA(T519, T521)
MULTB_IN_GGA(s(T555), s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(T558)))))))) → U19_GGA(T555, T558, multJ_in_ga(T555, T558))
MULTB_IN_GGA(s(T555), s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(T558)))))))) → MULTJ_IN_GA(T555, T558)
MULTJ_IN_GA(s(T623), s(s(s(s(s(s(s(T625)))))))) → U9_GA(T623, T625, multJ_in_ga(T623, T625))
MULTJ_IN_GA(s(T623), s(s(s(s(s(s(s(T625)))))))) → MULTJ_IN_GA(T623, T625)
MULTB_IN_GGA(T635, s(s(s(s(s(s(s(s(T637)))))))), s(s(s(s(s(s(s(s(T639))))))))) → U20_GGA(T635, T637, T639, multK_in_ggga(T635, s(s(s(s(s(s(s(T637))))))), T637, T639))
MULTB_IN_GGA(T635, s(s(s(s(s(s(s(s(T637)))))))), s(s(s(s(s(s(s(s(T639))))))))) → MULTK_IN_GGGA(T635, s(s(s(s(s(s(s(T637))))))), T637, T639)
MULTK_IN_GGGA(s(T662), T663, 0, T665) → U10_GGGA(T662, T663, T665, multB_in_gga(T662, s(T663), T665))
MULTK_IN_GGGA(s(T662), T663, 0, T665) → MULTB_IN_GGA(T662, s(T663), T665)
MULTK_IN_GGGA(T676, T677, s(T678), s(T680)) → U11_GGGA(T676, T677, T678, T680, multK_in_ggga(T676, T677, T678, T680))
MULTK_IN_GGGA(T676, T677, s(T678), s(T680)) → MULTK_IN_GGGA(T676, T677, T678, T680)
timesA_in_gga(0, T15, 0) → timesA_out_gga(0, T15, 0)
timesA_in_gga(s(T28), T29, T31) → U1_gga(T28, T29, T31, multB_in_gga(T28, T29, T31))
multB_in_gga(0, 0, 0) → multB_out_gga(0, 0, 0)
multB_in_gga(s(T51), 0, T54) → U12_gga(T51, T54, multC_in_ga(T51, T54))
multC_in_ga(0, 0) → multC_out_ga(0, 0)
multC_in_ga(s(T63), T65) → U2_ga(T63, T65, multC_in_ga(T63, T65))
U2_ga(T63, T65, multC_out_ga(T63, T65)) → multC_out_ga(s(T63), T65)
U12_gga(T51, T54, multC_out_ga(T51, T54)) → multB_out_gga(s(T51), 0, T54)
multB_in_gga(0, s(0), s(0)) → multB_out_gga(0, s(0), s(0))
multB_in_gga(s(T99), s(0), s(T102)) → U13_gga(T99, T102, multD_in_ga(T99, T102))
multD_in_ga(0, s(0)) → multD_out_ga(0, s(0))
multD_in_ga(s(T119), s(T121)) → U3_ga(T119, T121, multD_in_ga(T119, T121))
U3_ga(T119, T121, multD_out_ga(T119, T121)) → multD_out_ga(s(T119), s(T121))
U13_gga(T99, T102, multD_out_ga(T99, T102)) → multB_out_gga(s(T99), s(0), s(T102))
multB_in_gga(0, s(s(0)), s(s(0))) → multB_out_gga(0, s(s(0)), s(s(0)))
multB_in_gga(s(T155), s(s(0)), s(s(T158))) → U14_gga(T155, T158, multE_in_ga(T155, T158))
multE_in_ga(0, s(s(0))) → multE_out_ga(0, s(s(0)))
multE_in_ga(s(T183), s(s(T185))) → U4_ga(T183, T185, multE_in_ga(T183, T185))
U4_ga(T183, T185, multE_out_ga(T183, T185)) → multE_out_ga(s(T183), s(s(T185)))
U14_gga(T155, T158, multE_out_ga(T155, T158)) → multB_out_gga(s(T155), s(s(0)), s(s(T158)))
multB_in_gga(0, s(s(s(0))), s(s(s(0)))) → multB_out_gga(0, s(s(s(0))), s(s(s(0))))
multB_in_gga(s(T219), s(s(s(0))), s(s(s(T222)))) → U15_gga(T219, T222, multF_in_ga(T219, T222))
multF_in_ga(0, s(s(s(0)))) → multF_out_ga(0, s(s(s(0))))
multF_in_ga(s(T255), s(s(s(T257)))) → U5_ga(T255, T257, multF_in_ga(T255, T257))
U5_ga(T255, T257, multF_out_ga(T255, T257)) → multF_out_ga(s(T255), s(s(s(T257))))
U15_gga(T219, T222, multF_out_ga(T219, T222)) → multB_out_gga(s(T219), s(s(s(0))), s(s(s(T222))))
multB_in_gga(0, s(s(s(s(0)))), s(s(s(s(0))))) → multB_out_gga(0, s(s(s(s(0)))), s(s(s(s(0)))))
multB_in_gga(s(T291), s(s(s(s(0)))), s(s(s(s(T294))))) → U16_gga(T291, T294, multG_in_ga(T291, T294))
multG_in_ga(0, s(s(s(s(0))))) → multG_out_ga(0, s(s(s(s(0)))))
multG_in_ga(s(T335), s(s(s(s(T337))))) → U6_ga(T335, T337, multG_in_ga(T335, T337))
U6_ga(T335, T337, multG_out_ga(T335, T337)) → multG_out_ga(s(T335), s(s(s(s(T337)))))
U16_gga(T291, T294, multG_out_ga(T291, T294)) → multB_out_gga(s(T291), s(s(s(s(0)))), s(s(s(s(T294)))))
multB_in_gga(0, s(s(s(s(s(0))))), s(s(s(s(s(0)))))) → multB_out_gga(0, s(s(s(s(s(0))))), s(s(s(s(s(0))))))
multB_in_gga(s(T371), s(s(s(s(s(0))))), s(s(s(s(s(T374)))))) → U17_gga(T371, T374, multH_in_ga(T371, T374))
multH_in_ga(0, s(s(s(s(s(0)))))) → multH_out_ga(0, s(s(s(s(s(0))))))
multH_in_ga(s(T423), s(s(s(s(s(T425)))))) → U7_ga(T423, T425, multH_in_ga(T423, T425))
U7_ga(T423, T425, multH_out_ga(T423, T425)) → multH_out_ga(s(T423), s(s(s(s(s(T425))))))
U17_gga(T371, T374, multH_out_ga(T371, T374)) → multB_out_gga(s(T371), s(s(s(s(s(0))))), s(s(s(s(s(T374))))))
multB_in_gga(0, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(0))))))) → multB_out_gga(0, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(0)))))))
multB_in_gga(s(T459), s(s(s(s(s(s(0)))))), s(s(s(s(s(s(T462))))))) → U18_gga(T459, T462, multI_in_ga(T459, T462))
multI_in_ga(0, s(s(s(s(s(s(0))))))) → multI_out_ga(0, s(s(s(s(s(s(0)))))))
multI_in_ga(s(T519), s(s(s(s(s(s(T521))))))) → U8_ga(T519, T521, multI_in_ga(T519, T521))
U8_ga(T519, T521, multI_out_ga(T519, T521)) → multI_out_ga(s(T519), s(s(s(s(s(s(T521)))))))
U18_gga(T459, T462, multI_out_ga(T459, T462)) → multB_out_gga(s(T459), s(s(s(s(s(s(0)))))), s(s(s(s(s(s(T462)))))))
multB_in_gga(0, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(0)))))))) → multB_out_gga(0, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(0))))))))
multB_in_gga(s(T555), s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(T558)))))))) → U19_gga(T555, T558, multJ_in_ga(T555, T558))
multJ_in_ga(0, s(s(s(s(s(s(s(0)))))))) → multJ_out_ga(0, s(s(s(s(s(s(s(0))))))))
multJ_in_ga(s(T623), s(s(s(s(s(s(s(T625)))))))) → U9_ga(T623, T625, multJ_in_ga(T623, T625))
U9_ga(T623, T625, multJ_out_ga(T623, T625)) → multJ_out_ga(s(T623), s(s(s(s(s(s(s(T625))))))))
U19_gga(T555, T558, multJ_out_ga(T555, T558)) → multB_out_gga(s(T555), s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(T558))))))))
multB_in_gga(T635, s(s(s(s(s(s(s(s(T637)))))))), s(s(s(s(s(s(s(s(T639))))))))) → U20_gga(T635, T637, T639, multK_in_ggga(T635, s(s(s(s(s(s(s(T637))))))), T637, T639))
multK_in_ggga(0, T649, 0, 0) → multK_out_ggga(0, T649, 0, 0)
multK_in_ggga(s(T662), T663, 0, T665) → U10_ggga(T662, T663, T665, multB_in_gga(T662, s(T663), T665))
U10_ggga(T662, T663, T665, multB_out_gga(T662, s(T663), T665)) → multK_out_ggga(s(T662), T663, 0, T665)
multK_in_ggga(T676, T677, s(T678), s(T680)) → U11_ggga(T676, T677, T678, T680, multK_in_ggga(T676, T677, T678, T680))
U11_ggga(T676, T677, T678, T680, multK_out_ggga(T676, T677, T678, T680)) → multK_out_ggga(T676, T677, s(T678), s(T680))
U20_gga(T635, T637, T639, multK_out_ggga(T635, s(s(s(s(s(s(s(T637))))))), T637, T639)) → multB_out_gga(T635, s(s(s(s(s(s(s(s(T637)))))))), s(s(s(s(s(s(s(s(T639)))))))))
U1_gga(T28, T29, T31, multB_out_gga(T28, T29, T31)) → timesA_out_gga(s(T28), T29, T31)
MULTJ_IN_GA(s(T623), s(s(s(s(s(s(s(T625)))))))) → MULTJ_IN_GA(T623, T625)
timesA_in_gga(0, T15, 0) → timesA_out_gga(0, T15, 0)
timesA_in_gga(s(T28), T29, T31) → U1_gga(T28, T29, T31, multB_in_gga(T28, T29, T31))
multB_in_gga(0, 0, 0) → multB_out_gga(0, 0, 0)
multB_in_gga(s(T51), 0, T54) → U12_gga(T51, T54, multC_in_ga(T51, T54))
multC_in_ga(0, 0) → multC_out_ga(0, 0)
multC_in_ga(s(T63), T65) → U2_ga(T63, T65, multC_in_ga(T63, T65))
U2_ga(T63, T65, multC_out_ga(T63, T65)) → multC_out_ga(s(T63), T65)
U12_gga(T51, T54, multC_out_ga(T51, T54)) → multB_out_gga(s(T51), 0, T54)
multB_in_gga(0, s(0), s(0)) → multB_out_gga(0, s(0), s(0))
multB_in_gga(s(T99), s(0), s(T102)) → U13_gga(T99, T102, multD_in_ga(T99, T102))
multD_in_ga(0, s(0)) → multD_out_ga(0, s(0))
multD_in_ga(s(T119), s(T121)) → U3_ga(T119, T121, multD_in_ga(T119, T121))
U3_ga(T119, T121, multD_out_ga(T119, T121)) → multD_out_ga(s(T119), s(T121))
U13_gga(T99, T102, multD_out_ga(T99, T102)) → multB_out_gga(s(T99), s(0), s(T102))
multB_in_gga(0, s(s(0)), s(s(0))) → multB_out_gga(0, s(s(0)), s(s(0)))
multB_in_gga(s(T155), s(s(0)), s(s(T158))) → U14_gga(T155, T158, multE_in_ga(T155, T158))
multE_in_ga(0, s(s(0))) → multE_out_ga(0, s(s(0)))
multE_in_ga(s(T183), s(s(T185))) → U4_ga(T183, T185, multE_in_ga(T183, T185))
U4_ga(T183, T185, multE_out_ga(T183, T185)) → multE_out_ga(s(T183), s(s(T185)))
U14_gga(T155, T158, multE_out_ga(T155, T158)) → multB_out_gga(s(T155), s(s(0)), s(s(T158)))
multB_in_gga(0, s(s(s(0))), s(s(s(0)))) → multB_out_gga(0, s(s(s(0))), s(s(s(0))))
multB_in_gga(s(T219), s(s(s(0))), s(s(s(T222)))) → U15_gga(T219, T222, multF_in_ga(T219, T222))
multF_in_ga(0, s(s(s(0)))) → multF_out_ga(0, s(s(s(0))))
multF_in_ga(s(T255), s(s(s(T257)))) → U5_ga(T255, T257, multF_in_ga(T255, T257))
U5_ga(T255, T257, multF_out_ga(T255, T257)) → multF_out_ga(s(T255), s(s(s(T257))))
U15_gga(T219, T222, multF_out_ga(T219, T222)) → multB_out_gga(s(T219), s(s(s(0))), s(s(s(T222))))
multB_in_gga(0, s(s(s(s(0)))), s(s(s(s(0))))) → multB_out_gga(0, s(s(s(s(0)))), s(s(s(s(0)))))
multB_in_gga(s(T291), s(s(s(s(0)))), s(s(s(s(T294))))) → U16_gga(T291, T294, multG_in_ga(T291, T294))
multG_in_ga(0, s(s(s(s(0))))) → multG_out_ga(0, s(s(s(s(0)))))
multG_in_ga(s(T335), s(s(s(s(T337))))) → U6_ga(T335, T337, multG_in_ga(T335, T337))
U6_ga(T335, T337, multG_out_ga(T335, T337)) → multG_out_ga(s(T335), s(s(s(s(T337)))))
U16_gga(T291, T294, multG_out_ga(T291, T294)) → multB_out_gga(s(T291), s(s(s(s(0)))), s(s(s(s(T294)))))
multB_in_gga(0, s(s(s(s(s(0))))), s(s(s(s(s(0)))))) → multB_out_gga(0, s(s(s(s(s(0))))), s(s(s(s(s(0))))))
multB_in_gga(s(T371), s(s(s(s(s(0))))), s(s(s(s(s(T374)))))) → U17_gga(T371, T374, multH_in_ga(T371, T374))
multH_in_ga(0, s(s(s(s(s(0)))))) → multH_out_ga(0, s(s(s(s(s(0))))))
multH_in_ga(s(T423), s(s(s(s(s(T425)))))) → U7_ga(T423, T425, multH_in_ga(T423, T425))
U7_ga(T423, T425, multH_out_ga(T423, T425)) → multH_out_ga(s(T423), s(s(s(s(s(T425))))))
U17_gga(T371, T374, multH_out_ga(T371, T374)) → multB_out_gga(s(T371), s(s(s(s(s(0))))), s(s(s(s(s(T374))))))
multB_in_gga(0, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(0))))))) → multB_out_gga(0, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(0)))))))
multB_in_gga(s(T459), s(s(s(s(s(s(0)))))), s(s(s(s(s(s(T462))))))) → U18_gga(T459, T462, multI_in_ga(T459, T462))
multI_in_ga(0, s(s(s(s(s(s(0))))))) → multI_out_ga(0, s(s(s(s(s(s(0)))))))
multI_in_ga(s(T519), s(s(s(s(s(s(T521))))))) → U8_ga(T519, T521, multI_in_ga(T519, T521))
U8_ga(T519, T521, multI_out_ga(T519, T521)) → multI_out_ga(s(T519), s(s(s(s(s(s(T521)))))))
U18_gga(T459, T462, multI_out_ga(T459, T462)) → multB_out_gga(s(T459), s(s(s(s(s(s(0)))))), s(s(s(s(s(s(T462)))))))
multB_in_gga(0, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(0)))))))) → multB_out_gga(0, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(0))))))))
multB_in_gga(s(T555), s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(T558)))))))) → U19_gga(T555, T558, multJ_in_ga(T555, T558))
multJ_in_ga(0, s(s(s(s(s(s(s(0)))))))) → multJ_out_ga(0, s(s(s(s(s(s(s(0))))))))
multJ_in_ga(s(T623), s(s(s(s(s(s(s(T625)))))))) → U9_ga(T623, T625, multJ_in_ga(T623, T625))
U9_ga(T623, T625, multJ_out_ga(T623, T625)) → multJ_out_ga(s(T623), s(s(s(s(s(s(s(T625))))))))
U19_gga(T555, T558, multJ_out_ga(T555, T558)) → multB_out_gga(s(T555), s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(T558))))))))
multB_in_gga(T635, s(s(s(s(s(s(s(s(T637)))))))), s(s(s(s(s(s(s(s(T639))))))))) → U20_gga(T635, T637, T639, multK_in_ggga(T635, s(s(s(s(s(s(s(T637))))))), T637, T639))
multK_in_ggga(0, T649, 0, 0) → multK_out_ggga(0, T649, 0, 0)
multK_in_ggga(s(T662), T663, 0, T665) → U10_ggga(T662, T663, T665, multB_in_gga(T662, s(T663), T665))
U10_ggga(T662, T663, T665, multB_out_gga(T662, s(T663), T665)) → multK_out_ggga(s(T662), T663, 0, T665)
multK_in_ggga(T676, T677, s(T678), s(T680)) → U11_ggga(T676, T677, T678, T680, multK_in_ggga(T676, T677, T678, T680))
U11_ggga(T676, T677, T678, T680, multK_out_ggga(T676, T677, T678, T680)) → multK_out_ggga(T676, T677, s(T678), s(T680))
U20_gga(T635, T637, T639, multK_out_ggga(T635, s(s(s(s(s(s(s(T637))))))), T637, T639)) → multB_out_gga(T635, s(s(s(s(s(s(s(s(T637)))))))), s(s(s(s(s(s(s(s(T639)))))))))
U1_gga(T28, T29, T31, multB_out_gga(T28, T29, T31)) → timesA_out_gga(s(T28), T29, T31)
MULTJ_IN_GA(s(T623), s(s(s(s(s(s(s(T625)))))))) → MULTJ_IN_GA(T623, T625)
MULTJ_IN_GA(s(T623)) → MULTJ_IN_GA(T623)
From the DPs we obtained the following set of size-change graphs:
MULTI_IN_GA(s(T519), s(s(s(s(s(s(T521))))))) → MULTI_IN_GA(T519, T521)
timesA_in_gga(0, T15, 0) → timesA_out_gga(0, T15, 0)
timesA_in_gga(s(T28), T29, T31) → U1_gga(T28, T29, T31, multB_in_gga(T28, T29, T31))
multB_in_gga(0, 0, 0) → multB_out_gga(0, 0, 0)
multB_in_gga(s(T51), 0, T54) → U12_gga(T51, T54, multC_in_ga(T51, T54))
multC_in_ga(0, 0) → multC_out_ga(0, 0)
multC_in_ga(s(T63), T65) → U2_ga(T63, T65, multC_in_ga(T63, T65))
U2_ga(T63, T65, multC_out_ga(T63, T65)) → multC_out_ga(s(T63), T65)
U12_gga(T51, T54, multC_out_ga(T51, T54)) → multB_out_gga(s(T51), 0, T54)
multB_in_gga(0, s(0), s(0)) → multB_out_gga(0, s(0), s(0))
multB_in_gga(s(T99), s(0), s(T102)) → U13_gga(T99, T102, multD_in_ga(T99, T102))
multD_in_ga(0, s(0)) → multD_out_ga(0, s(0))
multD_in_ga(s(T119), s(T121)) → U3_ga(T119, T121, multD_in_ga(T119, T121))
U3_ga(T119, T121, multD_out_ga(T119, T121)) → multD_out_ga(s(T119), s(T121))
U13_gga(T99, T102, multD_out_ga(T99, T102)) → multB_out_gga(s(T99), s(0), s(T102))
multB_in_gga(0, s(s(0)), s(s(0))) → multB_out_gga(0, s(s(0)), s(s(0)))
multB_in_gga(s(T155), s(s(0)), s(s(T158))) → U14_gga(T155, T158, multE_in_ga(T155, T158))
multE_in_ga(0, s(s(0))) → multE_out_ga(0, s(s(0)))
multE_in_ga(s(T183), s(s(T185))) → U4_ga(T183, T185, multE_in_ga(T183, T185))
U4_ga(T183, T185, multE_out_ga(T183, T185)) → multE_out_ga(s(T183), s(s(T185)))
U14_gga(T155, T158, multE_out_ga(T155, T158)) → multB_out_gga(s(T155), s(s(0)), s(s(T158)))
multB_in_gga(0, s(s(s(0))), s(s(s(0)))) → multB_out_gga(0, s(s(s(0))), s(s(s(0))))
multB_in_gga(s(T219), s(s(s(0))), s(s(s(T222)))) → U15_gga(T219, T222, multF_in_ga(T219, T222))
multF_in_ga(0, s(s(s(0)))) → multF_out_ga(0, s(s(s(0))))
multF_in_ga(s(T255), s(s(s(T257)))) → U5_ga(T255, T257, multF_in_ga(T255, T257))
U5_ga(T255, T257, multF_out_ga(T255, T257)) → multF_out_ga(s(T255), s(s(s(T257))))
U15_gga(T219, T222, multF_out_ga(T219, T222)) → multB_out_gga(s(T219), s(s(s(0))), s(s(s(T222))))
multB_in_gga(0, s(s(s(s(0)))), s(s(s(s(0))))) → multB_out_gga(0, s(s(s(s(0)))), s(s(s(s(0)))))
multB_in_gga(s(T291), s(s(s(s(0)))), s(s(s(s(T294))))) → U16_gga(T291, T294, multG_in_ga(T291, T294))
multG_in_ga(0, s(s(s(s(0))))) → multG_out_ga(0, s(s(s(s(0)))))
multG_in_ga(s(T335), s(s(s(s(T337))))) → U6_ga(T335, T337, multG_in_ga(T335, T337))
U6_ga(T335, T337, multG_out_ga(T335, T337)) → multG_out_ga(s(T335), s(s(s(s(T337)))))
U16_gga(T291, T294, multG_out_ga(T291, T294)) → multB_out_gga(s(T291), s(s(s(s(0)))), s(s(s(s(T294)))))
multB_in_gga(0, s(s(s(s(s(0))))), s(s(s(s(s(0)))))) → multB_out_gga(0, s(s(s(s(s(0))))), s(s(s(s(s(0))))))
multB_in_gga(s(T371), s(s(s(s(s(0))))), s(s(s(s(s(T374)))))) → U17_gga(T371, T374, multH_in_ga(T371, T374))
multH_in_ga(0, s(s(s(s(s(0)))))) → multH_out_ga(0, s(s(s(s(s(0))))))
multH_in_ga(s(T423), s(s(s(s(s(T425)))))) → U7_ga(T423, T425, multH_in_ga(T423, T425))
U7_ga(T423, T425, multH_out_ga(T423, T425)) → multH_out_ga(s(T423), s(s(s(s(s(T425))))))
U17_gga(T371, T374, multH_out_ga(T371, T374)) → multB_out_gga(s(T371), s(s(s(s(s(0))))), s(s(s(s(s(T374))))))
multB_in_gga(0, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(0))))))) → multB_out_gga(0, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(0)))))))
multB_in_gga(s(T459), s(s(s(s(s(s(0)))))), s(s(s(s(s(s(T462))))))) → U18_gga(T459, T462, multI_in_ga(T459, T462))
multI_in_ga(0, s(s(s(s(s(s(0))))))) → multI_out_ga(0, s(s(s(s(s(s(0)))))))
multI_in_ga(s(T519), s(s(s(s(s(s(T521))))))) → U8_ga(T519, T521, multI_in_ga(T519, T521))
U8_ga(T519, T521, multI_out_ga(T519, T521)) → multI_out_ga(s(T519), s(s(s(s(s(s(T521)))))))
U18_gga(T459, T462, multI_out_ga(T459, T462)) → multB_out_gga(s(T459), s(s(s(s(s(s(0)))))), s(s(s(s(s(s(T462)))))))
multB_in_gga(0, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(0)))))))) → multB_out_gga(0, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(0))))))))
multB_in_gga(s(T555), s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(T558)))))))) → U19_gga(T555, T558, multJ_in_ga(T555, T558))
multJ_in_ga(0, s(s(s(s(s(s(s(0)))))))) → multJ_out_ga(0, s(s(s(s(s(s(s(0))))))))
multJ_in_ga(s(T623), s(s(s(s(s(s(s(T625)))))))) → U9_ga(T623, T625, multJ_in_ga(T623, T625))
U9_ga(T623, T625, multJ_out_ga(T623, T625)) → multJ_out_ga(s(T623), s(s(s(s(s(s(s(T625))))))))
U19_gga(T555, T558, multJ_out_ga(T555, T558)) → multB_out_gga(s(T555), s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(T558))))))))
multB_in_gga(T635, s(s(s(s(s(s(s(s(T637)))))))), s(s(s(s(s(s(s(s(T639))))))))) → U20_gga(T635, T637, T639, multK_in_ggga(T635, s(s(s(s(s(s(s(T637))))))), T637, T639))
multK_in_ggga(0, T649, 0, 0) → multK_out_ggga(0, T649, 0, 0)
multK_in_ggga(s(T662), T663, 0, T665) → U10_ggga(T662, T663, T665, multB_in_gga(T662, s(T663), T665))
U10_ggga(T662, T663, T665, multB_out_gga(T662, s(T663), T665)) → multK_out_ggga(s(T662), T663, 0, T665)
multK_in_ggga(T676, T677, s(T678), s(T680)) → U11_ggga(T676, T677, T678, T680, multK_in_ggga(T676, T677, T678, T680))
U11_ggga(T676, T677, T678, T680, multK_out_ggga(T676, T677, T678, T680)) → multK_out_ggga(T676, T677, s(T678), s(T680))
U20_gga(T635, T637, T639, multK_out_ggga(T635, s(s(s(s(s(s(s(T637))))))), T637, T639)) → multB_out_gga(T635, s(s(s(s(s(s(s(s(T637)))))))), s(s(s(s(s(s(s(s(T639)))))))))
U1_gga(T28, T29, T31, multB_out_gga(T28, T29, T31)) → timesA_out_gga(s(T28), T29, T31)
MULTI_IN_GA(s(T519), s(s(s(s(s(s(T521))))))) → MULTI_IN_GA(T519, T521)
MULTI_IN_GA(s(T519)) → MULTI_IN_GA(T519)
From the DPs we obtained the following set of size-change graphs:
MULTH_IN_GA(s(T423), s(s(s(s(s(T425)))))) → MULTH_IN_GA(T423, T425)
timesA_in_gga(0, T15, 0) → timesA_out_gga(0, T15, 0)
timesA_in_gga(s(T28), T29, T31) → U1_gga(T28, T29, T31, multB_in_gga(T28, T29, T31))
multB_in_gga(0, 0, 0) → multB_out_gga(0, 0, 0)
multB_in_gga(s(T51), 0, T54) → U12_gga(T51, T54, multC_in_ga(T51, T54))
multC_in_ga(0, 0) → multC_out_ga(0, 0)
multC_in_ga(s(T63), T65) → U2_ga(T63, T65, multC_in_ga(T63, T65))
U2_ga(T63, T65, multC_out_ga(T63, T65)) → multC_out_ga(s(T63), T65)
U12_gga(T51, T54, multC_out_ga(T51, T54)) → multB_out_gga(s(T51), 0, T54)
multB_in_gga(0, s(0), s(0)) → multB_out_gga(0, s(0), s(0))
multB_in_gga(s(T99), s(0), s(T102)) → U13_gga(T99, T102, multD_in_ga(T99, T102))
multD_in_ga(0, s(0)) → multD_out_ga(0, s(0))
multD_in_ga(s(T119), s(T121)) → U3_ga(T119, T121, multD_in_ga(T119, T121))
U3_ga(T119, T121, multD_out_ga(T119, T121)) → multD_out_ga(s(T119), s(T121))
U13_gga(T99, T102, multD_out_ga(T99, T102)) → multB_out_gga(s(T99), s(0), s(T102))
multB_in_gga(0, s(s(0)), s(s(0))) → multB_out_gga(0, s(s(0)), s(s(0)))
multB_in_gga(s(T155), s(s(0)), s(s(T158))) → U14_gga(T155, T158, multE_in_ga(T155, T158))
multE_in_ga(0, s(s(0))) → multE_out_ga(0, s(s(0)))
multE_in_ga(s(T183), s(s(T185))) → U4_ga(T183, T185, multE_in_ga(T183, T185))
U4_ga(T183, T185, multE_out_ga(T183, T185)) → multE_out_ga(s(T183), s(s(T185)))
U14_gga(T155, T158, multE_out_ga(T155, T158)) → multB_out_gga(s(T155), s(s(0)), s(s(T158)))
multB_in_gga(0, s(s(s(0))), s(s(s(0)))) → multB_out_gga(0, s(s(s(0))), s(s(s(0))))
multB_in_gga(s(T219), s(s(s(0))), s(s(s(T222)))) → U15_gga(T219, T222, multF_in_ga(T219, T222))
multF_in_ga(0, s(s(s(0)))) → multF_out_ga(0, s(s(s(0))))
multF_in_ga(s(T255), s(s(s(T257)))) → U5_ga(T255, T257, multF_in_ga(T255, T257))
U5_ga(T255, T257, multF_out_ga(T255, T257)) → multF_out_ga(s(T255), s(s(s(T257))))
U15_gga(T219, T222, multF_out_ga(T219, T222)) → multB_out_gga(s(T219), s(s(s(0))), s(s(s(T222))))
multB_in_gga(0, s(s(s(s(0)))), s(s(s(s(0))))) → multB_out_gga(0, s(s(s(s(0)))), s(s(s(s(0)))))
multB_in_gga(s(T291), s(s(s(s(0)))), s(s(s(s(T294))))) → U16_gga(T291, T294, multG_in_ga(T291, T294))
multG_in_ga(0, s(s(s(s(0))))) → multG_out_ga(0, s(s(s(s(0)))))
multG_in_ga(s(T335), s(s(s(s(T337))))) → U6_ga(T335, T337, multG_in_ga(T335, T337))
U6_ga(T335, T337, multG_out_ga(T335, T337)) → multG_out_ga(s(T335), s(s(s(s(T337)))))
U16_gga(T291, T294, multG_out_ga(T291, T294)) → multB_out_gga(s(T291), s(s(s(s(0)))), s(s(s(s(T294)))))
multB_in_gga(0, s(s(s(s(s(0))))), s(s(s(s(s(0)))))) → multB_out_gga(0, s(s(s(s(s(0))))), s(s(s(s(s(0))))))
multB_in_gga(s(T371), s(s(s(s(s(0))))), s(s(s(s(s(T374)))))) → U17_gga(T371, T374, multH_in_ga(T371, T374))
multH_in_ga(0, s(s(s(s(s(0)))))) → multH_out_ga(0, s(s(s(s(s(0))))))
multH_in_ga(s(T423), s(s(s(s(s(T425)))))) → U7_ga(T423, T425, multH_in_ga(T423, T425))
U7_ga(T423, T425, multH_out_ga(T423, T425)) → multH_out_ga(s(T423), s(s(s(s(s(T425))))))
U17_gga(T371, T374, multH_out_ga(T371, T374)) → multB_out_gga(s(T371), s(s(s(s(s(0))))), s(s(s(s(s(T374))))))
multB_in_gga(0, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(0))))))) → multB_out_gga(0, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(0)))))))
multB_in_gga(s(T459), s(s(s(s(s(s(0)))))), s(s(s(s(s(s(T462))))))) → U18_gga(T459, T462, multI_in_ga(T459, T462))
multI_in_ga(0, s(s(s(s(s(s(0))))))) → multI_out_ga(0, s(s(s(s(s(s(0)))))))
multI_in_ga(s(T519), s(s(s(s(s(s(T521))))))) → U8_ga(T519, T521, multI_in_ga(T519, T521))
U8_ga(T519, T521, multI_out_ga(T519, T521)) → multI_out_ga(s(T519), s(s(s(s(s(s(T521)))))))
U18_gga(T459, T462, multI_out_ga(T459, T462)) → multB_out_gga(s(T459), s(s(s(s(s(s(0)))))), s(s(s(s(s(s(T462)))))))
multB_in_gga(0, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(0)))))))) → multB_out_gga(0, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(0))))))))
multB_in_gga(s(T555), s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(T558)))))))) → U19_gga(T555, T558, multJ_in_ga(T555, T558))
multJ_in_ga(0, s(s(s(s(s(s(s(0)))))))) → multJ_out_ga(0, s(s(s(s(s(s(s(0))))))))
multJ_in_ga(s(T623), s(s(s(s(s(s(s(T625)))))))) → U9_ga(T623, T625, multJ_in_ga(T623, T625))
U9_ga(T623, T625, multJ_out_ga(T623, T625)) → multJ_out_ga(s(T623), s(s(s(s(s(s(s(T625))))))))
U19_gga(T555, T558, multJ_out_ga(T555, T558)) → multB_out_gga(s(T555), s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(T558))))))))
multB_in_gga(T635, s(s(s(s(s(s(s(s(T637)))))))), s(s(s(s(s(s(s(s(T639))))))))) → U20_gga(T635, T637, T639, multK_in_ggga(T635, s(s(s(s(s(s(s(T637))))))), T637, T639))
multK_in_ggga(0, T649, 0, 0) → multK_out_ggga(0, T649, 0, 0)
multK_in_ggga(s(T662), T663, 0, T665) → U10_ggga(T662, T663, T665, multB_in_gga(T662, s(T663), T665))
U10_ggga(T662, T663, T665, multB_out_gga(T662, s(T663), T665)) → multK_out_ggga(s(T662), T663, 0, T665)
multK_in_ggga(T676, T677, s(T678), s(T680)) → U11_ggga(T676, T677, T678, T680, multK_in_ggga(T676, T677, T678, T680))
U11_ggga(T676, T677, T678, T680, multK_out_ggga(T676, T677, T678, T680)) → multK_out_ggga(T676, T677, s(T678), s(T680))
U20_gga(T635, T637, T639, multK_out_ggga(T635, s(s(s(s(s(s(s(T637))))))), T637, T639)) → multB_out_gga(T635, s(s(s(s(s(s(s(s(T637)))))))), s(s(s(s(s(s(s(s(T639)))))))))
U1_gga(T28, T29, T31, multB_out_gga(T28, T29, T31)) → timesA_out_gga(s(T28), T29, T31)
MULTH_IN_GA(s(T423), s(s(s(s(s(T425)))))) → MULTH_IN_GA(T423, T425)
MULTH_IN_GA(s(T423)) → MULTH_IN_GA(T423)
From the DPs we obtained the following set of size-change graphs:
MULTG_IN_GA(s(T335), s(s(s(s(T337))))) → MULTG_IN_GA(T335, T337)
timesA_in_gga(0, T15, 0) → timesA_out_gga(0, T15, 0)
timesA_in_gga(s(T28), T29, T31) → U1_gga(T28, T29, T31, multB_in_gga(T28, T29, T31))
multB_in_gga(0, 0, 0) → multB_out_gga(0, 0, 0)
multB_in_gga(s(T51), 0, T54) → U12_gga(T51, T54, multC_in_ga(T51, T54))
multC_in_ga(0, 0) → multC_out_ga(0, 0)
multC_in_ga(s(T63), T65) → U2_ga(T63, T65, multC_in_ga(T63, T65))
U2_ga(T63, T65, multC_out_ga(T63, T65)) → multC_out_ga(s(T63), T65)
U12_gga(T51, T54, multC_out_ga(T51, T54)) → multB_out_gga(s(T51), 0, T54)
multB_in_gga(0, s(0), s(0)) → multB_out_gga(0, s(0), s(0))
multB_in_gga(s(T99), s(0), s(T102)) → U13_gga(T99, T102, multD_in_ga(T99, T102))
multD_in_ga(0, s(0)) → multD_out_ga(0, s(0))
multD_in_ga(s(T119), s(T121)) → U3_ga(T119, T121, multD_in_ga(T119, T121))
U3_ga(T119, T121, multD_out_ga(T119, T121)) → multD_out_ga(s(T119), s(T121))
U13_gga(T99, T102, multD_out_ga(T99, T102)) → multB_out_gga(s(T99), s(0), s(T102))
multB_in_gga(0, s(s(0)), s(s(0))) → multB_out_gga(0, s(s(0)), s(s(0)))
multB_in_gga(s(T155), s(s(0)), s(s(T158))) → U14_gga(T155, T158, multE_in_ga(T155, T158))
multE_in_ga(0, s(s(0))) → multE_out_ga(0, s(s(0)))
multE_in_ga(s(T183), s(s(T185))) → U4_ga(T183, T185, multE_in_ga(T183, T185))
U4_ga(T183, T185, multE_out_ga(T183, T185)) → multE_out_ga(s(T183), s(s(T185)))
U14_gga(T155, T158, multE_out_ga(T155, T158)) → multB_out_gga(s(T155), s(s(0)), s(s(T158)))
multB_in_gga(0, s(s(s(0))), s(s(s(0)))) → multB_out_gga(0, s(s(s(0))), s(s(s(0))))
multB_in_gga(s(T219), s(s(s(0))), s(s(s(T222)))) → U15_gga(T219, T222, multF_in_ga(T219, T222))
multF_in_ga(0, s(s(s(0)))) → multF_out_ga(0, s(s(s(0))))
multF_in_ga(s(T255), s(s(s(T257)))) → U5_ga(T255, T257, multF_in_ga(T255, T257))
U5_ga(T255, T257, multF_out_ga(T255, T257)) → multF_out_ga(s(T255), s(s(s(T257))))
U15_gga(T219, T222, multF_out_ga(T219, T222)) → multB_out_gga(s(T219), s(s(s(0))), s(s(s(T222))))
multB_in_gga(0, s(s(s(s(0)))), s(s(s(s(0))))) → multB_out_gga(0, s(s(s(s(0)))), s(s(s(s(0)))))
multB_in_gga(s(T291), s(s(s(s(0)))), s(s(s(s(T294))))) → U16_gga(T291, T294, multG_in_ga(T291, T294))
multG_in_ga(0, s(s(s(s(0))))) → multG_out_ga(0, s(s(s(s(0)))))
multG_in_ga(s(T335), s(s(s(s(T337))))) → U6_ga(T335, T337, multG_in_ga(T335, T337))
U6_ga(T335, T337, multG_out_ga(T335, T337)) → multG_out_ga(s(T335), s(s(s(s(T337)))))
U16_gga(T291, T294, multG_out_ga(T291, T294)) → multB_out_gga(s(T291), s(s(s(s(0)))), s(s(s(s(T294)))))
multB_in_gga(0, s(s(s(s(s(0))))), s(s(s(s(s(0)))))) → multB_out_gga(0, s(s(s(s(s(0))))), s(s(s(s(s(0))))))
multB_in_gga(s(T371), s(s(s(s(s(0))))), s(s(s(s(s(T374)))))) → U17_gga(T371, T374, multH_in_ga(T371, T374))
multH_in_ga(0, s(s(s(s(s(0)))))) → multH_out_ga(0, s(s(s(s(s(0))))))
multH_in_ga(s(T423), s(s(s(s(s(T425)))))) → U7_ga(T423, T425, multH_in_ga(T423, T425))
U7_ga(T423, T425, multH_out_ga(T423, T425)) → multH_out_ga(s(T423), s(s(s(s(s(T425))))))
U17_gga(T371, T374, multH_out_ga(T371, T374)) → multB_out_gga(s(T371), s(s(s(s(s(0))))), s(s(s(s(s(T374))))))
multB_in_gga(0, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(0))))))) → multB_out_gga(0, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(0)))))))
multB_in_gga(s(T459), s(s(s(s(s(s(0)))))), s(s(s(s(s(s(T462))))))) → U18_gga(T459, T462, multI_in_ga(T459, T462))
multI_in_ga(0, s(s(s(s(s(s(0))))))) → multI_out_ga(0, s(s(s(s(s(s(0)))))))
multI_in_ga(s(T519), s(s(s(s(s(s(T521))))))) → U8_ga(T519, T521, multI_in_ga(T519, T521))
U8_ga(T519, T521, multI_out_ga(T519, T521)) → multI_out_ga(s(T519), s(s(s(s(s(s(T521)))))))
U18_gga(T459, T462, multI_out_ga(T459, T462)) → multB_out_gga(s(T459), s(s(s(s(s(s(0)))))), s(s(s(s(s(s(T462)))))))
multB_in_gga(0, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(0)))))))) → multB_out_gga(0, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(0))))))))
multB_in_gga(s(T555), s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(T558)))))))) → U19_gga(T555, T558, multJ_in_ga(T555, T558))
multJ_in_ga(0, s(s(s(s(s(s(s(0)))))))) → multJ_out_ga(0, s(s(s(s(s(s(s(0))))))))
multJ_in_ga(s(T623), s(s(s(s(s(s(s(T625)))))))) → U9_ga(T623, T625, multJ_in_ga(T623, T625))
U9_ga(T623, T625, multJ_out_ga(T623, T625)) → multJ_out_ga(s(T623), s(s(s(s(s(s(s(T625))))))))
U19_gga(T555, T558, multJ_out_ga(T555, T558)) → multB_out_gga(s(T555), s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(T558))))))))
multB_in_gga(T635, s(s(s(s(s(s(s(s(T637)))))))), s(s(s(s(s(s(s(s(T639))))))))) → U20_gga(T635, T637, T639, multK_in_ggga(T635, s(s(s(s(s(s(s(T637))))))), T637, T639))
multK_in_ggga(0, T649, 0, 0) → multK_out_ggga(0, T649, 0, 0)
multK_in_ggga(s(T662), T663, 0, T665) → U10_ggga(T662, T663, T665, multB_in_gga(T662, s(T663), T665))
U10_ggga(T662, T663, T665, multB_out_gga(T662, s(T663), T665)) → multK_out_ggga(s(T662), T663, 0, T665)
multK_in_ggga(T676, T677, s(T678), s(T680)) → U11_ggga(T676, T677, T678, T680, multK_in_ggga(T676, T677, T678, T680))
U11_ggga(T676, T677, T678, T680, multK_out_ggga(T676, T677, T678, T680)) → multK_out_ggga(T676, T677, s(T678), s(T680))
U20_gga(T635, T637, T639, multK_out_ggga(T635, s(s(s(s(s(s(s(T637))))))), T637, T639)) → multB_out_gga(T635, s(s(s(s(s(s(s(s(T637)))))))), s(s(s(s(s(s(s(s(T639)))))))))
U1_gga(T28, T29, T31, multB_out_gga(T28, T29, T31)) → timesA_out_gga(s(T28), T29, T31)
MULTG_IN_GA(s(T335), s(s(s(s(T337))))) → MULTG_IN_GA(T335, T337)
MULTG_IN_GA(s(T335)) → MULTG_IN_GA(T335)
From the DPs we obtained the following set of size-change graphs:
MULTF_IN_GA(s(T255), s(s(s(T257)))) → MULTF_IN_GA(T255, T257)
timesA_in_gga(0, T15, 0) → timesA_out_gga(0, T15, 0)
timesA_in_gga(s(T28), T29, T31) → U1_gga(T28, T29, T31, multB_in_gga(T28, T29, T31))
multB_in_gga(0, 0, 0) → multB_out_gga(0, 0, 0)
multB_in_gga(s(T51), 0, T54) → U12_gga(T51, T54, multC_in_ga(T51, T54))
multC_in_ga(0, 0) → multC_out_ga(0, 0)
multC_in_ga(s(T63), T65) → U2_ga(T63, T65, multC_in_ga(T63, T65))
U2_ga(T63, T65, multC_out_ga(T63, T65)) → multC_out_ga(s(T63), T65)
U12_gga(T51, T54, multC_out_ga(T51, T54)) → multB_out_gga(s(T51), 0, T54)
multB_in_gga(0, s(0), s(0)) → multB_out_gga(0, s(0), s(0))
multB_in_gga(s(T99), s(0), s(T102)) → U13_gga(T99, T102, multD_in_ga(T99, T102))
multD_in_ga(0, s(0)) → multD_out_ga(0, s(0))
multD_in_ga(s(T119), s(T121)) → U3_ga(T119, T121, multD_in_ga(T119, T121))
U3_ga(T119, T121, multD_out_ga(T119, T121)) → multD_out_ga(s(T119), s(T121))
U13_gga(T99, T102, multD_out_ga(T99, T102)) → multB_out_gga(s(T99), s(0), s(T102))
multB_in_gga(0, s(s(0)), s(s(0))) → multB_out_gga(0, s(s(0)), s(s(0)))
multB_in_gga(s(T155), s(s(0)), s(s(T158))) → U14_gga(T155, T158, multE_in_ga(T155, T158))
multE_in_ga(0, s(s(0))) → multE_out_ga(0, s(s(0)))
multE_in_ga(s(T183), s(s(T185))) → U4_ga(T183, T185, multE_in_ga(T183, T185))
U4_ga(T183, T185, multE_out_ga(T183, T185)) → multE_out_ga(s(T183), s(s(T185)))
U14_gga(T155, T158, multE_out_ga(T155, T158)) → multB_out_gga(s(T155), s(s(0)), s(s(T158)))
multB_in_gga(0, s(s(s(0))), s(s(s(0)))) → multB_out_gga(0, s(s(s(0))), s(s(s(0))))
multB_in_gga(s(T219), s(s(s(0))), s(s(s(T222)))) → U15_gga(T219, T222, multF_in_ga(T219, T222))
multF_in_ga(0, s(s(s(0)))) → multF_out_ga(0, s(s(s(0))))
multF_in_ga(s(T255), s(s(s(T257)))) → U5_ga(T255, T257, multF_in_ga(T255, T257))
U5_ga(T255, T257, multF_out_ga(T255, T257)) → multF_out_ga(s(T255), s(s(s(T257))))
U15_gga(T219, T222, multF_out_ga(T219, T222)) → multB_out_gga(s(T219), s(s(s(0))), s(s(s(T222))))
multB_in_gga(0, s(s(s(s(0)))), s(s(s(s(0))))) → multB_out_gga(0, s(s(s(s(0)))), s(s(s(s(0)))))
multB_in_gga(s(T291), s(s(s(s(0)))), s(s(s(s(T294))))) → U16_gga(T291, T294, multG_in_ga(T291, T294))
multG_in_ga(0, s(s(s(s(0))))) → multG_out_ga(0, s(s(s(s(0)))))
multG_in_ga(s(T335), s(s(s(s(T337))))) → U6_ga(T335, T337, multG_in_ga(T335, T337))
U6_ga(T335, T337, multG_out_ga(T335, T337)) → multG_out_ga(s(T335), s(s(s(s(T337)))))
U16_gga(T291, T294, multG_out_ga(T291, T294)) → multB_out_gga(s(T291), s(s(s(s(0)))), s(s(s(s(T294)))))
multB_in_gga(0, s(s(s(s(s(0))))), s(s(s(s(s(0)))))) → multB_out_gga(0, s(s(s(s(s(0))))), s(s(s(s(s(0))))))
multB_in_gga(s(T371), s(s(s(s(s(0))))), s(s(s(s(s(T374)))))) → U17_gga(T371, T374, multH_in_ga(T371, T374))
multH_in_ga(0, s(s(s(s(s(0)))))) → multH_out_ga(0, s(s(s(s(s(0))))))
multH_in_ga(s(T423), s(s(s(s(s(T425)))))) → U7_ga(T423, T425, multH_in_ga(T423, T425))
U7_ga(T423, T425, multH_out_ga(T423, T425)) → multH_out_ga(s(T423), s(s(s(s(s(T425))))))
U17_gga(T371, T374, multH_out_ga(T371, T374)) → multB_out_gga(s(T371), s(s(s(s(s(0))))), s(s(s(s(s(T374))))))
multB_in_gga(0, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(0))))))) → multB_out_gga(0, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(0)))))))
multB_in_gga(s(T459), s(s(s(s(s(s(0)))))), s(s(s(s(s(s(T462))))))) → U18_gga(T459, T462, multI_in_ga(T459, T462))
multI_in_ga(0, s(s(s(s(s(s(0))))))) → multI_out_ga(0, s(s(s(s(s(s(0)))))))
multI_in_ga(s(T519), s(s(s(s(s(s(T521))))))) → U8_ga(T519, T521, multI_in_ga(T519, T521))
U8_ga(T519, T521, multI_out_ga(T519, T521)) → multI_out_ga(s(T519), s(s(s(s(s(s(T521)))))))
U18_gga(T459, T462, multI_out_ga(T459, T462)) → multB_out_gga(s(T459), s(s(s(s(s(s(0)))))), s(s(s(s(s(s(T462)))))))
multB_in_gga(0, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(0)))))))) → multB_out_gga(0, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(0))))))))
multB_in_gga(s(T555), s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(T558)))))))) → U19_gga(T555, T558, multJ_in_ga(T555, T558))
multJ_in_ga(0, s(s(s(s(s(s(s(0)))))))) → multJ_out_ga(0, s(s(s(s(s(s(s(0))))))))
multJ_in_ga(s(T623), s(s(s(s(s(s(s(T625)))))))) → U9_ga(T623, T625, multJ_in_ga(T623, T625))
U9_ga(T623, T625, multJ_out_ga(T623, T625)) → multJ_out_ga(s(T623), s(s(s(s(s(s(s(T625))))))))
U19_gga(T555, T558, multJ_out_ga(T555, T558)) → multB_out_gga(s(T555), s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(T558))))))))
multB_in_gga(T635, s(s(s(s(s(s(s(s(T637)))))))), s(s(s(s(s(s(s(s(T639))))))))) → U20_gga(T635, T637, T639, multK_in_ggga(T635, s(s(s(s(s(s(s(T637))))))), T637, T639))
multK_in_ggga(0, T649, 0, 0) → multK_out_ggga(0, T649, 0, 0)
multK_in_ggga(s(T662), T663, 0, T665) → U10_ggga(T662, T663, T665, multB_in_gga(T662, s(T663), T665))
U10_ggga(T662, T663, T665, multB_out_gga(T662, s(T663), T665)) → multK_out_ggga(s(T662), T663, 0, T665)
multK_in_ggga(T676, T677, s(T678), s(T680)) → U11_ggga(T676, T677, T678, T680, multK_in_ggga(T676, T677, T678, T680))
U11_ggga(T676, T677, T678, T680, multK_out_ggga(T676, T677, T678, T680)) → multK_out_ggga(T676, T677, s(T678), s(T680))
U20_gga(T635, T637, T639, multK_out_ggga(T635, s(s(s(s(s(s(s(T637))))))), T637, T639)) → multB_out_gga(T635, s(s(s(s(s(s(s(s(T637)))))))), s(s(s(s(s(s(s(s(T639)))))))))
U1_gga(T28, T29, T31, multB_out_gga(T28, T29, T31)) → timesA_out_gga(s(T28), T29, T31)
MULTF_IN_GA(s(T255), s(s(s(T257)))) → MULTF_IN_GA(T255, T257)
MULTF_IN_GA(s(T255)) → MULTF_IN_GA(T255)
From the DPs we obtained the following set of size-change graphs:
MULTE_IN_GA(s(T183), s(s(T185))) → MULTE_IN_GA(T183, T185)
timesA_in_gga(0, T15, 0) → timesA_out_gga(0, T15, 0)
timesA_in_gga(s(T28), T29, T31) → U1_gga(T28, T29, T31, multB_in_gga(T28, T29, T31))
multB_in_gga(0, 0, 0) → multB_out_gga(0, 0, 0)
multB_in_gga(s(T51), 0, T54) → U12_gga(T51, T54, multC_in_ga(T51, T54))
multC_in_ga(0, 0) → multC_out_ga(0, 0)
multC_in_ga(s(T63), T65) → U2_ga(T63, T65, multC_in_ga(T63, T65))
U2_ga(T63, T65, multC_out_ga(T63, T65)) → multC_out_ga(s(T63), T65)
U12_gga(T51, T54, multC_out_ga(T51, T54)) → multB_out_gga(s(T51), 0, T54)
multB_in_gga(0, s(0), s(0)) → multB_out_gga(0, s(0), s(0))
multB_in_gga(s(T99), s(0), s(T102)) → U13_gga(T99, T102, multD_in_ga(T99, T102))
multD_in_ga(0, s(0)) → multD_out_ga(0, s(0))
multD_in_ga(s(T119), s(T121)) → U3_ga(T119, T121, multD_in_ga(T119, T121))
U3_ga(T119, T121, multD_out_ga(T119, T121)) → multD_out_ga(s(T119), s(T121))
U13_gga(T99, T102, multD_out_ga(T99, T102)) → multB_out_gga(s(T99), s(0), s(T102))
multB_in_gga(0, s(s(0)), s(s(0))) → multB_out_gga(0, s(s(0)), s(s(0)))
multB_in_gga(s(T155), s(s(0)), s(s(T158))) → U14_gga(T155, T158, multE_in_ga(T155, T158))
multE_in_ga(0, s(s(0))) → multE_out_ga(0, s(s(0)))
multE_in_ga(s(T183), s(s(T185))) → U4_ga(T183, T185, multE_in_ga(T183, T185))
U4_ga(T183, T185, multE_out_ga(T183, T185)) → multE_out_ga(s(T183), s(s(T185)))
U14_gga(T155, T158, multE_out_ga(T155, T158)) → multB_out_gga(s(T155), s(s(0)), s(s(T158)))
multB_in_gga(0, s(s(s(0))), s(s(s(0)))) → multB_out_gga(0, s(s(s(0))), s(s(s(0))))
multB_in_gga(s(T219), s(s(s(0))), s(s(s(T222)))) → U15_gga(T219, T222, multF_in_ga(T219, T222))
multF_in_ga(0, s(s(s(0)))) → multF_out_ga(0, s(s(s(0))))
multF_in_ga(s(T255), s(s(s(T257)))) → U5_ga(T255, T257, multF_in_ga(T255, T257))
U5_ga(T255, T257, multF_out_ga(T255, T257)) → multF_out_ga(s(T255), s(s(s(T257))))
U15_gga(T219, T222, multF_out_ga(T219, T222)) → multB_out_gga(s(T219), s(s(s(0))), s(s(s(T222))))
multB_in_gga(0, s(s(s(s(0)))), s(s(s(s(0))))) → multB_out_gga(0, s(s(s(s(0)))), s(s(s(s(0)))))
multB_in_gga(s(T291), s(s(s(s(0)))), s(s(s(s(T294))))) → U16_gga(T291, T294, multG_in_ga(T291, T294))
multG_in_ga(0, s(s(s(s(0))))) → multG_out_ga(0, s(s(s(s(0)))))
multG_in_ga(s(T335), s(s(s(s(T337))))) → U6_ga(T335, T337, multG_in_ga(T335, T337))
U6_ga(T335, T337, multG_out_ga(T335, T337)) → multG_out_ga(s(T335), s(s(s(s(T337)))))
U16_gga(T291, T294, multG_out_ga(T291, T294)) → multB_out_gga(s(T291), s(s(s(s(0)))), s(s(s(s(T294)))))
multB_in_gga(0, s(s(s(s(s(0))))), s(s(s(s(s(0)))))) → multB_out_gga(0, s(s(s(s(s(0))))), s(s(s(s(s(0))))))
multB_in_gga(s(T371), s(s(s(s(s(0))))), s(s(s(s(s(T374)))))) → U17_gga(T371, T374, multH_in_ga(T371, T374))
multH_in_ga(0, s(s(s(s(s(0)))))) → multH_out_ga(0, s(s(s(s(s(0))))))
multH_in_ga(s(T423), s(s(s(s(s(T425)))))) → U7_ga(T423, T425, multH_in_ga(T423, T425))
U7_ga(T423, T425, multH_out_ga(T423, T425)) → multH_out_ga(s(T423), s(s(s(s(s(T425))))))
U17_gga(T371, T374, multH_out_ga(T371, T374)) → multB_out_gga(s(T371), s(s(s(s(s(0))))), s(s(s(s(s(T374))))))
multB_in_gga(0, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(0))))))) → multB_out_gga(0, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(0)))))))
multB_in_gga(s(T459), s(s(s(s(s(s(0)))))), s(s(s(s(s(s(T462))))))) → U18_gga(T459, T462, multI_in_ga(T459, T462))
multI_in_ga(0, s(s(s(s(s(s(0))))))) → multI_out_ga(0, s(s(s(s(s(s(0)))))))
multI_in_ga(s(T519), s(s(s(s(s(s(T521))))))) → U8_ga(T519, T521, multI_in_ga(T519, T521))
U8_ga(T519, T521, multI_out_ga(T519, T521)) → multI_out_ga(s(T519), s(s(s(s(s(s(T521)))))))
U18_gga(T459, T462, multI_out_ga(T459, T462)) → multB_out_gga(s(T459), s(s(s(s(s(s(0)))))), s(s(s(s(s(s(T462)))))))
multB_in_gga(0, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(0)))))))) → multB_out_gga(0, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(0))))))))
multB_in_gga(s(T555), s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(T558)))))))) → U19_gga(T555, T558, multJ_in_ga(T555, T558))
multJ_in_ga(0, s(s(s(s(s(s(s(0)))))))) → multJ_out_ga(0, s(s(s(s(s(s(s(0))))))))
multJ_in_ga(s(T623), s(s(s(s(s(s(s(T625)))))))) → U9_ga(T623, T625, multJ_in_ga(T623, T625))
U9_ga(T623, T625, multJ_out_ga(T623, T625)) → multJ_out_ga(s(T623), s(s(s(s(s(s(s(T625))))))))
U19_gga(T555, T558, multJ_out_ga(T555, T558)) → multB_out_gga(s(T555), s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(T558))))))))
multB_in_gga(T635, s(s(s(s(s(s(s(s(T637)))))))), s(s(s(s(s(s(s(s(T639))))))))) → U20_gga(T635, T637, T639, multK_in_ggga(T635, s(s(s(s(s(s(s(T637))))))), T637, T639))
multK_in_ggga(0, T649, 0, 0) → multK_out_ggga(0, T649, 0, 0)
multK_in_ggga(s(T662), T663, 0, T665) → U10_ggga(T662, T663, T665, multB_in_gga(T662, s(T663), T665))
U10_ggga(T662, T663, T665, multB_out_gga(T662, s(T663), T665)) → multK_out_ggga(s(T662), T663, 0, T665)
multK_in_ggga(T676, T677, s(T678), s(T680)) → U11_ggga(T676, T677, T678, T680, multK_in_ggga(T676, T677, T678, T680))
U11_ggga(T676, T677, T678, T680, multK_out_ggga(T676, T677, T678, T680)) → multK_out_ggga(T676, T677, s(T678), s(T680))
U20_gga(T635, T637, T639, multK_out_ggga(T635, s(s(s(s(s(s(s(T637))))))), T637, T639)) → multB_out_gga(T635, s(s(s(s(s(s(s(s(T637)))))))), s(s(s(s(s(s(s(s(T639)))))))))
U1_gga(T28, T29, T31, multB_out_gga(T28, T29, T31)) → timesA_out_gga(s(T28), T29, T31)
MULTE_IN_GA(s(T183), s(s(T185))) → MULTE_IN_GA(T183, T185)
MULTE_IN_GA(s(T183)) → MULTE_IN_GA(T183)
From the DPs we obtained the following set of size-change graphs:
MULTD_IN_GA(s(T119), s(T121)) → MULTD_IN_GA(T119, T121)
timesA_in_gga(0, T15, 0) → timesA_out_gga(0, T15, 0)
timesA_in_gga(s(T28), T29, T31) → U1_gga(T28, T29, T31, multB_in_gga(T28, T29, T31))
multB_in_gga(0, 0, 0) → multB_out_gga(0, 0, 0)
multB_in_gga(s(T51), 0, T54) → U12_gga(T51, T54, multC_in_ga(T51, T54))
multC_in_ga(0, 0) → multC_out_ga(0, 0)
multC_in_ga(s(T63), T65) → U2_ga(T63, T65, multC_in_ga(T63, T65))
U2_ga(T63, T65, multC_out_ga(T63, T65)) → multC_out_ga(s(T63), T65)
U12_gga(T51, T54, multC_out_ga(T51, T54)) → multB_out_gga(s(T51), 0, T54)
multB_in_gga(0, s(0), s(0)) → multB_out_gga(0, s(0), s(0))
multB_in_gga(s(T99), s(0), s(T102)) → U13_gga(T99, T102, multD_in_ga(T99, T102))
multD_in_ga(0, s(0)) → multD_out_ga(0, s(0))
multD_in_ga(s(T119), s(T121)) → U3_ga(T119, T121, multD_in_ga(T119, T121))
U3_ga(T119, T121, multD_out_ga(T119, T121)) → multD_out_ga(s(T119), s(T121))
U13_gga(T99, T102, multD_out_ga(T99, T102)) → multB_out_gga(s(T99), s(0), s(T102))
multB_in_gga(0, s(s(0)), s(s(0))) → multB_out_gga(0, s(s(0)), s(s(0)))
multB_in_gga(s(T155), s(s(0)), s(s(T158))) → U14_gga(T155, T158, multE_in_ga(T155, T158))
multE_in_ga(0, s(s(0))) → multE_out_ga(0, s(s(0)))
multE_in_ga(s(T183), s(s(T185))) → U4_ga(T183, T185, multE_in_ga(T183, T185))
U4_ga(T183, T185, multE_out_ga(T183, T185)) → multE_out_ga(s(T183), s(s(T185)))
U14_gga(T155, T158, multE_out_ga(T155, T158)) → multB_out_gga(s(T155), s(s(0)), s(s(T158)))
multB_in_gga(0, s(s(s(0))), s(s(s(0)))) → multB_out_gga(0, s(s(s(0))), s(s(s(0))))
multB_in_gga(s(T219), s(s(s(0))), s(s(s(T222)))) → U15_gga(T219, T222, multF_in_ga(T219, T222))
multF_in_ga(0, s(s(s(0)))) → multF_out_ga(0, s(s(s(0))))
multF_in_ga(s(T255), s(s(s(T257)))) → U5_ga(T255, T257, multF_in_ga(T255, T257))
U5_ga(T255, T257, multF_out_ga(T255, T257)) → multF_out_ga(s(T255), s(s(s(T257))))
U15_gga(T219, T222, multF_out_ga(T219, T222)) → multB_out_gga(s(T219), s(s(s(0))), s(s(s(T222))))
multB_in_gga(0, s(s(s(s(0)))), s(s(s(s(0))))) → multB_out_gga(0, s(s(s(s(0)))), s(s(s(s(0)))))
multB_in_gga(s(T291), s(s(s(s(0)))), s(s(s(s(T294))))) → U16_gga(T291, T294, multG_in_ga(T291, T294))
multG_in_ga(0, s(s(s(s(0))))) → multG_out_ga(0, s(s(s(s(0)))))
multG_in_ga(s(T335), s(s(s(s(T337))))) → U6_ga(T335, T337, multG_in_ga(T335, T337))
U6_ga(T335, T337, multG_out_ga(T335, T337)) → multG_out_ga(s(T335), s(s(s(s(T337)))))
U16_gga(T291, T294, multG_out_ga(T291, T294)) → multB_out_gga(s(T291), s(s(s(s(0)))), s(s(s(s(T294)))))
multB_in_gga(0, s(s(s(s(s(0))))), s(s(s(s(s(0)))))) → multB_out_gga(0, s(s(s(s(s(0))))), s(s(s(s(s(0))))))
multB_in_gga(s(T371), s(s(s(s(s(0))))), s(s(s(s(s(T374)))))) → U17_gga(T371, T374, multH_in_ga(T371, T374))
multH_in_ga(0, s(s(s(s(s(0)))))) → multH_out_ga(0, s(s(s(s(s(0))))))
multH_in_ga(s(T423), s(s(s(s(s(T425)))))) → U7_ga(T423, T425, multH_in_ga(T423, T425))
U7_ga(T423, T425, multH_out_ga(T423, T425)) → multH_out_ga(s(T423), s(s(s(s(s(T425))))))
U17_gga(T371, T374, multH_out_ga(T371, T374)) → multB_out_gga(s(T371), s(s(s(s(s(0))))), s(s(s(s(s(T374))))))
multB_in_gga(0, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(0))))))) → multB_out_gga(0, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(0)))))))
multB_in_gga(s(T459), s(s(s(s(s(s(0)))))), s(s(s(s(s(s(T462))))))) → U18_gga(T459, T462, multI_in_ga(T459, T462))
multI_in_ga(0, s(s(s(s(s(s(0))))))) → multI_out_ga(0, s(s(s(s(s(s(0)))))))
multI_in_ga(s(T519), s(s(s(s(s(s(T521))))))) → U8_ga(T519, T521, multI_in_ga(T519, T521))
U8_ga(T519, T521, multI_out_ga(T519, T521)) → multI_out_ga(s(T519), s(s(s(s(s(s(T521)))))))
U18_gga(T459, T462, multI_out_ga(T459, T462)) → multB_out_gga(s(T459), s(s(s(s(s(s(0)))))), s(s(s(s(s(s(T462)))))))
multB_in_gga(0, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(0)))))))) → multB_out_gga(0, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(0))))))))
multB_in_gga(s(T555), s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(T558)))))))) → U19_gga(T555, T558, multJ_in_ga(T555, T558))
multJ_in_ga(0, s(s(s(s(s(s(s(0)))))))) → multJ_out_ga(0, s(s(s(s(s(s(s(0))))))))
multJ_in_ga(s(T623), s(s(s(s(s(s(s(T625)))))))) → U9_ga(T623, T625, multJ_in_ga(T623, T625))
U9_ga(T623, T625, multJ_out_ga(T623, T625)) → multJ_out_ga(s(T623), s(s(s(s(s(s(s(T625))))))))
U19_gga(T555, T558, multJ_out_ga(T555, T558)) → multB_out_gga(s(T555), s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(T558))))))))
multB_in_gga(T635, s(s(s(s(s(s(s(s(T637)))))))), s(s(s(s(s(s(s(s(T639))))))))) → U20_gga(T635, T637, T639, multK_in_ggga(T635, s(s(s(s(s(s(s(T637))))))), T637, T639))
multK_in_ggga(0, T649, 0, 0) → multK_out_ggga(0, T649, 0, 0)
multK_in_ggga(s(T662), T663, 0, T665) → U10_ggga(T662, T663, T665, multB_in_gga(T662, s(T663), T665))
U10_ggga(T662, T663, T665, multB_out_gga(T662, s(T663), T665)) → multK_out_ggga(s(T662), T663, 0, T665)
multK_in_ggga(T676, T677, s(T678), s(T680)) → U11_ggga(T676, T677, T678, T680, multK_in_ggga(T676, T677, T678, T680))
U11_ggga(T676, T677, T678, T680, multK_out_ggga(T676, T677, T678, T680)) → multK_out_ggga(T676, T677, s(T678), s(T680))
U20_gga(T635, T637, T639, multK_out_ggga(T635, s(s(s(s(s(s(s(T637))))))), T637, T639)) → multB_out_gga(T635, s(s(s(s(s(s(s(s(T637)))))))), s(s(s(s(s(s(s(s(T639)))))))))
U1_gga(T28, T29, T31, multB_out_gga(T28, T29, T31)) → timesA_out_gga(s(T28), T29, T31)
MULTD_IN_GA(s(T119), s(T121)) → MULTD_IN_GA(T119, T121)
MULTD_IN_GA(s(T119)) → MULTD_IN_GA(T119)
From the DPs we obtained the following set of size-change graphs:
MULTB_IN_GGA(T635, s(s(s(s(s(s(s(s(T637)))))))), s(s(s(s(s(s(s(s(T639))))))))) → MULTK_IN_GGGA(T635, s(s(s(s(s(s(s(T637))))))), T637, T639)
MULTK_IN_GGGA(s(T662), T663, 0, T665) → MULTB_IN_GGA(T662, s(T663), T665)
MULTK_IN_GGGA(T676, T677, s(T678), s(T680)) → MULTK_IN_GGGA(T676, T677, T678, T680)
timesA_in_gga(0, T15, 0) → timesA_out_gga(0, T15, 0)
timesA_in_gga(s(T28), T29, T31) → U1_gga(T28, T29, T31, multB_in_gga(T28, T29, T31))
multB_in_gga(0, 0, 0) → multB_out_gga(0, 0, 0)
multB_in_gga(s(T51), 0, T54) → U12_gga(T51, T54, multC_in_ga(T51, T54))
multC_in_ga(0, 0) → multC_out_ga(0, 0)
multC_in_ga(s(T63), T65) → U2_ga(T63, T65, multC_in_ga(T63, T65))
U2_ga(T63, T65, multC_out_ga(T63, T65)) → multC_out_ga(s(T63), T65)
U12_gga(T51, T54, multC_out_ga(T51, T54)) → multB_out_gga(s(T51), 0, T54)
multB_in_gga(0, s(0), s(0)) → multB_out_gga(0, s(0), s(0))
multB_in_gga(s(T99), s(0), s(T102)) → U13_gga(T99, T102, multD_in_ga(T99, T102))
multD_in_ga(0, s(0)) → multD_out_ga(0, s(0))
multD_in_ga(s(T119), s(T121)) → U3_ga(T119, T121, multD_in_ga(T119, T121))
U3_ga(T119, T121, multD_out_ga(T119, T121)) → multD_out_ga(s(T119), s(T121))
U13_gga(T99, T102, multD_out_ga(T99, T102)) → multB_out_gga(s(T99), s(0), s(T102))
multB_in_gga(0, s(s(0)), s(s(0))) → multB_out_gga(0, s(s(0)), s(s(0)))
multB_in_gga(s(T155), s(s(0)), s(s(T158))) → U14_gga(T155, T158, multE_in_ga(T155, T158))
multE_in_ga(0, s(s(0))) → multE_out_ga(0, s(s(0)))
multE_in_ga(s(T183), s(s(T185))) → U4_ga(T183, T185, multE_in_ga(T183, T185))
U4_ga(T183, T185, multE_out_ga(T183, T185)) → multE_out_ga(s(T183), s(s(T185)))
U14_gga(T155, T158, multE_out_ga(T155, T158)) → multB_out_gga(s(T155), s(s(0)), s(s(T158)))
multB_in_gga(0, s(s(s(0))), s(s(s(0)))) → multB_out_gga(0, s(s(s(0))), s(s(s(0))))
multB_in_gga(s(T219), s(s(s(0))), s(s(s(T222)))) → U15_gga(T219, T222, multF_in_ga(T219, T222))
multF_in_ga(0, s(s(s(0)))) → multF_out_ga(0, s(s(s(0))))
multF_in_ga(s(T255), s(s(s(T257)))) → U5_ga(T255, T257, multF_in_ga(T255, T257))
U5_ga(T255, T257, multF_out_ga(T255, T257)) → multF_out_ga(s(T255), s(s(s(T257))))
U15_gga(T219, T222, multF_out_ga(T219, T222)) → multB_out_gga(s(T219), s(s(s(0))), s(s(s(T222))))
multB_in_gga(0, s(s(s(s(0)))), s(s(s(s(0))))) → multB_out_gga(0, s(s(s(s(0)))), s(s(s(s(0)))))
multB_in_gga(s(T291), s(s(s(s(0)))), s(s(s(s(T294))))) → U16_gga(T291, T294, multG_in_ga(T291, T294))
multG_in_ga(0, s(s(s(s(0))))) → multG_out_ga(0, s(s(s(s(0)))))
multG_in_ga(s(T335), s(s(s(s(T337))))) → U6_ga(T335, T337, multG_in_ga(T335, T337))
U6_ga(T335, T337, multG_out_ga(T335, T337)) → multG_out_ga(s(T335), s(s(s(s(T337)))))
U16_gga(T291, T294, multG_out_ga(T291, T294)) → multB_out_gga(s(T291), s(s(s(s(0)))), s(s(s(s(T294)))))
multB_in_gga(0, s(s(s(s(s(0))))), s(s(s(s(s(0)))))) → multB_out_gga(0, s(s(s(s(s(0))))), s(s(s(s(s(0))))))
multB_in_gga(s(T371), s(s(s(s(s(0))))), s(s(s(s(s(T374)))))) → U17_gga(T371, T374, multH_in_ga(T371, T374))
multH_in_ga(0, s(s(s(s(s(0)))))) → multH_out_ga(0, s(s(s(s(s(0))))))
multH_in_ga(s(T423), s(s(s(s(s(T425)))))) → U7_ga(T423, T425, multH_in_ga(T423, T425))
U7_ga(T423, T425, multH_out_ga(T423, T425)) → multH_out_ga(s(T423), s(s(s(s(s(T425))))))
U17_gga(T371, T374, multH_out_ga(T371, T374)) → multB_out_gga(s(T371), s(s(s(s(s(0))))), s(s(s(s(s(T374))))))
multB_in_gga(0, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(0))))))) → multB_out_gga(0, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(0)))))))
multB_in_gga(s(T459), s(s(s(s(s(s(0)))))), s(s(s(s(s(s(T462))))))) → U18_gga(T459, T462, multI_in_ga(T459, T462))
multI_in_ga(0, s(s(s(s(s(s(0))))))) → multI_out_ga(0, s(s(s(s(s(s(0)))))))
multI_in_ga(s(T519), s(s(s(s(s(s(T521))))))) → U8_ga(T519, T521, multI_in_ga(T519, T521))
U8_ga(T519, T521, multI_out_ga(T519, T521)) → multI_out_ga(s(T519), s(s(s(s(s(s(T521)))))))
U18_gga(T459, T462, multI_out_ga(T459, T462)) → multB_out_gga(s(T459), s(s(s(s(s(s(0)))))), s(s(s(s(s(s(T462)))))))
multB_in_gga(0, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(0)))))))) → multB_out_gga(0, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(0))))))))
multB_in_gga(s(T555), s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(T558)))))))) → U19_gga(T555, T558, multJ_in_ga(T555, T558))
multJ_in_ga(0, s(s(s(s(s(s(s(0)))))))) → multJ_out_ga(0, s(s(s(s(s(s(s(0))))))))
multJ_in_ga(s(T623), s(s(s(s(s(s(s(T625)))))))) → U9_ga(T623, T625, multJ_in_ga(T623, T625))
U9_ga(T623, T625, multJ_out_ga(T623, T625)) → multJ_out_ga(s(T623), s(s(s(s(s(s(s(T625))))))))
U19_gga(T555, T558, multJ_out_ga(T555, T558)) → multB_out_gga(s(T555), s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(T558))))))))
multB_in_gga(T635, s(s(s(s(s(s(s(s(T637)))))))), s(s(s(s(s(s(s(s(T639))))))))) → U20_gga(T635, T637, T639, multK_in_ggga(T635, s(s(s(s(s(s(s(T637))))))), T637, T639))
multK_in_ggga(0, T649, 0, 0) → multK_out_ggga(0, T649, 0, 0)
multK_in_ggga(s(T662), T663, 0, T665) → U10_ggga(T662, T663, T665, multB_in_gga(T662, s(T663), T665))
U10_ggga(T662, T663, T665, multB_out_gga(T662, s(T663), T665)) → multK_out_ggga(s(T662), T663, 0, T665)
multK_in_ggga(T676, T677, s(T678), s(T680)) → U11_ggga(T676, T677, T678, T680, multK_in_ggga(T676, T677, T678, T680))
U11_ggga(T676, T677, T678, T680, multK_out_ggga(T676, T677, T678, T680)) → multK_out_ggga(T676, T677, s(T678), s(T680))
U20_gga(T635, T637, T639, multK_out_ggga(T635, s(s(s(s(s(s(s(T637))))))), T637, T639)) → multB_out_gga(T635, s(s(s(s(s(s(s(s(T637)))))))), s(s(s(s(s(s(s(s(T639)))))))))
U1_gga(T28, T29, T31, multB_out_gga(T28, T29, T31)) → timesA_out_gga(s(T28), T29, T31)
MULTB_IN_GGA(T635, s(s(s(s(s(s(s(s(T637)))))))), s(s(s(s(s(s(s(s(T639))))))))) → MULTK_IN_GGGA(T635, s(s(s(s(s(s(s(T637))))))), T637, T639)
MULTK_IN_GGGA(s(T662), T663, 0, T665) → MULTB_IN_GGA(T662, s(T663), T665)
MULTK_IN_GGGA(T676, T677, s(T678), s(T680)) → MULTK_IN_GGGA(T676, T677, T678, T680)
MULTB_IN_GGA(T635, s(s(s(s(s(s(s(s(T637))))))))) → MULTK_IN_GGGA(T635, s(s(s(s(s(s(s(T637))))))), T637)
MULTK_IN_GGGA(s(T662), T663, 0) → MULTB_IN_GGA(T662, s(T663))
MULTK_IN_GGGA(T676, T677, s(T678)) → MULTK_IN_GGGA(T676, T677, T678)
From the DPs we obtained the following set of size-change graphs:
MULTC_IN_GA(s(T63), T65) → MULTC_IN_GA(T63, T65)
timesA_in_gga(0, T15, 0) → timesA_out_gga(0, T15, 0)
timesA_in_gga(s(T28), T29, T31) → U1_gga(T28, T29, T31, multB_in_gga(T28, T29, T31))
multB_in_gga(0, 0, 0) → multB_out_gga(0, 0, 0)
multB_in_gga(s(T51), 0, T54) → U12_gga(T51, T54, multC_in_ga(T51, T54))
multC_in_ga(0, 0) → multC_out_ga(0, 0)
multC_in_ga(s(T63), T65) → U2_ga(T63, T65, multC_in_ga(T63, T65))
U2_ga(T63, T65, multC_out_ga(T63, T65)) → multC_out_ga(s(T63), T65)
U12_gga(T51, T54, multC_out_ga(T51, T54)) → multB_out_gga(s(T51), 0, T54)
multB_in_gga(0, s(0), s(0)) → multB_out_gga(0, s(0), s(0))
multB_in_gga(s(T99), s(0), s(T102)) → U13_gga(T99, T102, multD_in_ga(T99, T102))
multD_in_ga(0, s(0)) → multD_out_ga(0, s(0))
multD_in_ga(s(T119), s(T121)) → U3_ga(T119, T121, multD_in_ga(T119, T121))
U3_ga(T119, T121, multD_out_ga(T119, T121)) → multD_out_ga(s(T119), s(T121))
U13_gga(T99, T102, multD_out_ga(T99, T102)) → multB_out_gga(s(T99), s(0), s(T102))
multB_in_gga(0, s(s(0)), s(s(0))) → multB_out_gga(0, s(s(0)), s(s(0)))
multB_in_gga(s(T155), s(s(0)), s(s(T158))) → U14_gga(T155, T158, multE_in_ga(T155, T158))
multE_in_ga(0, s(s(0))) → multE_out_ga(0, s(s(0)))
multE_in_ga(s(T183), s(s(T185))) → U4_ga(T183, T185, multE_in_ga(T183, T185))
U4_ga(T183, T185, multE_out_ga(T183, T185)) → multE_out_ga(s(T183), s(s(T185)))
U14_gga(T155, T158, multE_out_ga(T155, T158)) → multB_out_gga(s(T155), s(s(0)), s(s(T158)))
multB_in_gga(0, s(s(s(0))), s(s(s(0)))) → multB_out_gga(0, s(s(s(0))), s(s(s(0))))
multB_in_gga(s(T219), s(s(s(0))), s(s(s(T222)))) → U15_gga(T219, T222, multF_in_ga(T219, T222))
multF_in_ga(0, s(s(s(0)))) → multF_out_ga(0, s(s(s(0))))
multF_in_ga(s(T255), s(s(s(T257)))) → U5_ga(T255, T257, multF_in_ga(T255, T257))
U5_ga(T255, T257, multF_out_ga(T255, T257)) → multF_out_ga(s(T255), s(s(s(T257))))
U15_gga(T219, T222, multF_out_ga(T219, T222)) → multB_out_gga(s(T219), s(s(s(0))), s(s(s(T222))))
multB_in_gga(0, s(s(s(s(0)))), s(s(s(s(0))))) → multB_out_gga(0, s(s(s(s(0)))), s(s(s(s(0)))))
multB_in_gga(s(T291), s(s(s(s(0)))), s(s(s(s(T294))))) → U16_gga(T291, T294, multG_in_ga(T291, T294))
multG_in_ga(0, s(s(s(s(0))))) → multG_out_ga(0, s(s(s(s(0)))))
multG_in_ga(s(T335), s(s(s(s(T337))))) → U6_ga(T335, T337, multG_in_ga(T335, T337))
U6_ga(T335, T337, multG_out_ga(T335, T337)) → multG_out_ga(s(T335), s(s(s(s(T337)))))
U16_gga(T291, T294, multG_out_ga(T291, T294)) → multB_out_gga(s(T291), s(s(s(s(0)))), s(s(s(s(T294)))))
multB_in_gga(0, s(s(s(s(s(0))))), s(s(s(s(s(0)))))) → multB_out_gga(0, s(s(s(s(s(0))))), s(s(s(s(s(0))))))
multB_in_gga(s(T371), s(s(s(s(s(0))))), s(s(s(s(s(T374)))))) → U17_gga(T371, T374, multH_in_ga(T371, T374))
multH_in_ga(0, s(s(s(s(s(0)))))) → multH_out_ga(0, s(s(s(s(s(0))))))
multH_in_ga(s(T423), s(s(s(s(s(T425)))))) → U7_ga(T423, T425, multH_in_ga(T423, T425))
U7_ga(T423, T425, multH_out_ga(T423, T425)) → multH_out_ga(s(T423), s(s(s(s(s(T425))))))
U17_gga(T371, T374, multH_out_ga(T371, T374)) → multB_out_gga(s(T371), s(s(s(s(s(0))))), s(s(s(s(s(T374))))))
multB_in_gga(0, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(0))))))) → multB_out_gga(0, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(0)))))))
multB_in_gga(s(T459), s(s(s(s(s(s(0)))))), s(s(s(s(s(s(T462))))))) → U18_gga(T459, T462, multI_in_ga(T459, T462))
multI_in_ga(0, s(s(s(s(s(s(0))))))) → multI_out_ga(0, s(s(s(s(s(s(0)))))))
multI_in_ga(s(T519), s(s(s(s(s(s(T521))))))) → U8_ga(T519, T521, multI_in_ga(T519, T521))
U8_ga(T519, T521, multI_out_ga(T519, T521)) → multI_out_ga(s(T519), s(s(s(s(s(s(T521)))))))
U18_gga(T459, T462, multI_out_ga(T459, T462)) → multB_out_gga(s(T459), s(s(s(s(s(s(0)))))), s(s(s(s(s(s(T462)))))))
multB_in_gga(0, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(0)))))))) → multB_out_gga(0, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(0))))))))
multB_in_gga(s(T555), s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(T558)))))))) → U19_gga(T555, T558, multJ_in_ga(T555, T558))
multJ_in_ga(0, s(s(s(s(s(s(s(0)))))))) → multJ_out_ga(0, s(s(s(s(s(s(s(0))))))))
multJ_in_ga(s(T623), s(s(s(s(s(s(s(T625)))))))) → U9_ga(T623, T625, multJ_in_ga(T623, T625))
U9_ga(T623, T625, multJ_out_ga(T623, T625)) → multJ_out_ga(s(T623), s(s(s(s(s(s(s(T625))))))))
U19_gga(T555, T558, multJ_out_ga(T555, T558)) → multB_out_gga(s(T555), s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(T558))))))))
multB_in_gga(T635, s(s(s(s(s(s(s(s(T637)))))))), s(s(s(s(s(s(s(s(T639))))))))) → U20_gga(T635, T637, T639, multK_in_ggga(T635, s(s(s(s(s(s(s(T637))))))), T637, T639))
multK_in_ggga(0, T649, 0, 0) → multK_out_ggga(0, T649, 0, 0)
multK_in_ggga(s(T662), T663, 0, T665) → U10_ggga(T662, T663, T665, multB_in_gga(T662, s(T663), T665))
U10_ggga(T662, T663, T665, multB_out_gga(T662, s(T663), T665)) → multK_out_ggga(s(T662), T663, 0, T665)
multK_in_ggga(T676, T677, s(T678), s(T680)) → U11_ggga(T676, T677, T678, T680, multK_in_ggga(T676, T677, T678, T680))
U11_ggga(T676, T677, T678, T680, multK_out_ggga(T676, T677, T678, T680)) → multK_out_ggga(T676, T677, s(T678), s(T680))
U20_gga(T635, T637, T639, multK_out_ggga(T635, s(s(s(s(s(s(s(T637))))))), T637, T639)) → multB_out_gga(T635, s(s(s(s(s(s(s(s(T637)))))))), s(s(s(s(s(s(s(s(T639)))))))))
U1_gga(T28, T29, T31, multB_out_gga(T28, T29, T31)) → timesA_out_gga(s(T28), T29, T31)
MULTC_IN_GA(s(T63), T65) → MULTC_IN_GA(T63, T65)
MULTC_IN_GA(s(T63)) → MULTC_IN_GA(T63)
From the DPs we obtained the following set of size-change graphs: