0 Prolog
↳1 PrologToPrologProblemTransformerProof (⇐)
↳2 Prolog
↳3 PrologToPiTRSProof (⇐)
↳4 PiTRS
↳5 DependencyPairsProof (⇔)
↳6 PiDP
↳7 DependencyGraphProof (⇔)
↳8 AND
↳9 PiDP
↳10 UsableRulesProof (⇔)
↳11 PiDP
↳12 PiDPToQDPProof (⇐)
↳13 QDP
↳14 QDPSizeChangeProof (⇔)
↳15 YES
↳16 PiDP
↳17 UsableRulesProof (⇔)
↳18 PiDP
↳19 PiDPToQDPProof (⇐)
↳20 QDP
↳21 QDPSizeChangeProof (⇔)
↳22 YES
↳23 PiDP
↳24 UsableRulesProof (⇔)
↳25 PiDP
↳26 PiDPToQDPProof (⇐)
↳27 QDP
↳28 QDPSizeChangeProof (⇔)
↳29 YES
↳30 PiDP
↳31 UsableRulesProof (⇔)
↳32 PiDP
↳33 PiDPToQDPProof (⇐)
↳34 QDP
↳35 QDPSizeChangeProof (⇔)
↳36 YES
↳37 PiDP
↳38 UsableRulesProof (⇔)
↳39 PiDP
↳40 PiDPToQDPProof (⇐)
↳41 QDP
↳42 QDPSizeChangeProof (⇔)
↳43 YES
↳44 PiDP
↳45 UsableRulesProof (⇔)
↳46 PiDP
↳47 PiDPToQDPProof (⇐)
↳48 QDP
↳49 QDPSizeChangeProof (⇔)
↳50 YES
↳51 PiDP
↳52 UsableRulesProof (⇔)
↳53 PiDP
↳54 PiDPToQDPProof (⇐)
↳55 QDP
↳56 QDPSizeChangeProof (⇔)
↳57 YES
↳58 PiDP
↳59 UsableRulesProof (⇔)
↳60 PiDP
↳61 PiDPToQDPProof (⇐)
↳62 QDP
↳63 QDPSizeChangeProof (⇔)
↳64 YES
↳65 PiDP
↳66 UsableRulesProof (⇔)
↳67 PiDP
↳68 PiDPToQDPProof (⇐)
↳69 QDP
↳70 QDPSizeChangeProof (⇔)
↳71 YES
times1_in_gga(0, T15, 0) → times1_out_gga(0, T15, 0)
times1_in_gga(s(T28), T29, T31) → U20_gga(T28, T29, T31, mult12_in_gga(T28, T29, T31))
mult12_in_gga(0, 0, 0) → mult12_out_gga(0, 0, 0)
mult12_in_gga(s(T51), 0, T54) → U9_gga(T51, T54, mult22_in_ga(T51, T54))
mult22_in_ga(0, 0) → mult22_out_ga(0, 0)
mult22_in_ga(s(T63), T65) → U1_ga(T63, T65, mult22_in_ga(T63, T65))
U1_ga(T63, T65, mult22_out_ga(T63, T65)) → mult22_out_ga(s(T63), T65)
U9_gga(T51, T54, mult22_out_ga(T51, T54)) → mult12_out_gga(s(T51), 0, T54)
mult12_in_gga(0, s(0), s(0)) → mult12_out_gga(0, s(0), s(0))
mult12_in_gga(s(T99), s(0), s(T102)) → U10_gga(T99, T102, mult45_in_ga(T99, T102))
mult45_in_ga(0, s(0)) → mult45_out_ga(0, s(0))
mult45_in_ga(s(T122), s(T124)) → U2_ga(T122, T124, mult45_in_ga(T122, T124))
U2_ga(T122, T124, mult45_out_ga(T122, T124)) → mult45_out_ga(s(T122), s(T124))
U10_gga(T99, T102, mult45_out_ga(T99, T102)) → mult12_out_gga(s(T99), s(0), s(T102))
mult12_in_gga(0, s(s(0)), s(s(0))) → mult12_out_gga(0, s(s(0)), s(s(0)))
mult12_in_gga(s(T161), s(s(0)), s(s(T164))) → U11_gga(T161, T164, mult73_in_ga(T161, T164))
mult73_in_ga(0, s(s(0))) → mult73_out_ga(0, s(s(0)))
mult73_in_ga(s(T195), s(s(T197))) → U3_ga(T195, T197, mult73_in_ga(T195, T197))
U3_ga(T195, T197, mult73_out_ga(T195, T197)) → mult73_out_ga(s(T195), s(s(T197)))
U11_gga(T161, T164, mult73_out_ga(T161, T164)) → mult12_out_gga(s(T161), s(s(0)), s(s(T164)))
mult12_in_gga(0, s(s(s(0))), s(s(s(0)))) → mult12_out_gga(0, s(s(s(0))), s(s(s(0))))
mult12_in_gga(s(T234), s(s(s(0))), s(s(s(T237)))) → U12_gga(T234, T237, mult106_in_ga(T234, T237))
mult106_in_ga(0, s(s(s(0)))) → mult106_out_ga(0, s(s(s(0))))
mult106_in_ga(s(T279), s(s(s(T281)))) → U4_ga(T279, T281, mult106_in_ga(T279, T281))
U4_ga(T279, T281, mult106_out_ga(T279, T281)) → mult106_out_ga(s(T279), s(s(s(T281))))
U12_gga(T234, T237, mult106_out_ga(T234, T237)) → mult12_out_gga(s(T234), s(s(s(0))), s(s(s(T237))))
mult12_in_gga(0, s(s(s(s(0)))), s(s(s(s(0))))) → mult12_out_gga(0, s(s(s(s(0)))), s(s(s(s(0)))))
mult12_in_gga(s(T318), s(s(s(s(0)))), s(s(s(s(T321))))) → U13_gga(T318, T321, mult144_in_ga(T318, T321))
mult144_in_ga(0, s(s(s(s(0))))) → mult144_out_ga(0, s(s(s(s(0)))))
mult144_in_ga(s(T374), s(s(s(s(T376))))) → U5_ga(T374, T376, mult144_in_ga(T374, T376))
U5_ga(T374, T376, mult144_out_ga(T374, T376)) → mult144_out_ga(s(T374), s(s(s(s(T376)))))
U13_gga(T318, T321, mult144_out_ga(T318, T321)) → mult12_out_gga(s(T318), s(s(s(s(0)))), s(s(s(s(T321)))))
mult12_in_gga(0, s(s(s(s(s(0))))), s(s(s(s(s(0)))))) → mult12_out_gga(0, s(s(s(s(s(0))))), s(s(s(s(s(0))))))
mult12_in_gga(s(T413), s(s(s(s(s(0))))), s(s(s(s(s(T416)))))) → U14_gga(T413, T416, mult187_in_ga(T413, T416))
mult187_in_ga(0, s(s(s(s(s(0)))))) → mult187_out_ga(0, s(s(s(s(s(0))))))
mult187_in_ga(s(T480), s(s(s(s(s(T482)))))) → U6_ga(T480, T482, mult187_in_ga(T480, T482))
U6_ga(T480, T482, mult187_out_ga(T480, T482)) → mult187_out_ga(s(T480), s(s(s(s(s(T482))))))
U14_gga(T413, T416, mult187_out_ga(T413, T416)) → mult12_out_gga(s(T413), s(s(s(s(s(0))))), s(s(s(s(s(T416))))))
mult12_in_gga(0, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(0))))))) → mult12_out_gga(0, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(0)))))))
mult12_in_gga(s(T519), s(s(s(s(s(s(0)))))), s(s(s(s(s(s(T522))))))) → U15_gga(T519, T522, mult235_in_ga(T519, T522))
mult235_in_ga(0, s(s(s(s(s(s(0))))))) → mult235_out_ga(0, s(s(s(s(s(s(0)))))))
mult235_in_ga(s(T597), s(s(s(s(s(s(T599))))))) → U7_ga(T597, T599, mult235_in_ga(T597, T599))
U7_ga(T597, T599, mult235_out_ga(T597, T599)) → mult235_out_ga(s(T597), s(s(s(s(s(s(T599)))))))
U15_gga(T519, T522, mult235_out_ga(T519, T522)) → mult12_out_gga(s(T519), s(s(s(s(s(s(0)))))), s(s(s(s(s(s(T522)))))))
mult12_in_gga(0, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(0)))))))) → mult12_out_gga(0, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(0))))))))
mult12_in_gga(s(T636), s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(T639)))))))) → U16_gga(T636, T639, mult288_in_ga(T636, T639))
mult288_in_ga(0, s(s(s(s(s(s(s(0)))))))) → mult288_out_ga(0, s(s(s(s(s(s(s(0))))))))
mult288_in_ga(s(T725), s(s(s(s(s(s(s(T727)))))))) → U8_ga(T725, T727, mult288_in_ga(T725, T727))
U8_ga(T725, T727, mult288_out_ga(T725, T727)) → mult288_out_ga(s(T725), s(s(s(s(s(s(s(T727))))))))
U16_gga(T636, T639, mult288_out_ga(T636, T639)) → mult12_out_gga(s(T636), s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(T639))))))))
mult12_in_gga(T740, s(s(s(s(s(s(s(s(T742)))))))), s(s(s(s(s(s(s(s(T744))))))))) → U17_gga(T740, T742, T744, mult338_in_ggga(T740, s(s(s(s(s(s(s(T742))))))), T742, T744))
mult338_in_ggga(0, T754, 0, 0) → mult338_out_ggga(0, T754, 0, 0)
mult338_in_ggga(s(T767), T768, 0, T770) → U18_ggga(T767, T768, T770, mult12_in_gga(T767, s(T768), T770))
U18_ggga(T767, T768, T770, mult12_out_gga(T767, s(T768), T770)) → mult338_out_ggga(s(T767), T768, 0, T770)
mult338_in_ggga(T786, T787, s(T788), s(T790)) → U19_ggga(T786, T787, T788, T790, mult338_in_ggga(T786, T787, T788, T790))
U19_ggga(T786, T787, T788, T790, mult338_out_ggga(T786, T787, T788, T790)) → mult338_out_ggga(T786, T787, s(T788), s(T790))
U17_gga(T740, T742, T744, mult338_out_ggga(T740, s(s(s(s(s(s(s(T742))))))), T742, T744)) → mult12_out_gga(T740, s(s(s(s(s(s(s(s(T742)))))))), s(s(s(s(s(s(s(s(T744)))))))))
U20_gga(T28, T29, T31, mult12_out_gga(T28, T29, T31)) → times1_out_gga(s(T28), T29, T31)
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
times1_in_gga(0, T15, 0) → times1_out_gga(0, T15, 0)
times1_in_gga(s(T28), T29, T31) → U20_gga(T28, T29, T31, mult12_in_gga(T28, T29, T31))
mult12_in_gga(0, 0, 0) → mult12_out_gga(0, 0, 0)
mult12_in_gga(s(T51), 0, T54) → U9_gga(T51, T54, mult22_in_ga(T51, T54))
mult22_in_ga(0, 0) → mult22_out_ga(0, 0)
mult22_in_ga(s(T63), T65) → U1_ga(T63, T65, mult22_in_ga(T63, T65))
U1_ga(T63, T65, mult22_out_ga(T63, T65)) → mult22_out_ga(s(T63), T65)
U9_gga(T51, T54, mult22_out_ga(T51, T54)) → mult12_out_gga(s(T51), 0, T54)
mult12_in_gga(0, s(0), s(0)) → mult12_out_gga(0, s(0), s(0))
mult12_in_gga(s(T99), s(0), s(T102)) → U10_gga(T99, T102, mult45_in_ga(T99, T102))
mult45_in_ga(0, s(0)) → mult45_out_ga(0, s(0))
mult45_in_ga(s(T122), s(T124)) → U2_ga(T122, T124, mult45_in_ga(T122, T124))
U2_ga(T122, T124, mult45_out_ga(T122, T124)) → mult45_out_ga(s(T122), s(T124))
U10_gga(T99, T102, mult45_out_ga(T99, T102)) → mult12_out_gga(s(T99), s(0), s(T102))
mult12_in_gga(0, s(s(0)), s(s(0))) → mult12_out_gga(0, s(s(0)), s(s(0)))
mult12_in_gga(s(T161), s(s(0)), s(s(T164))) → U11_gga(T161, T164, mult73_in_ga(T161, T164))
mult73_in_ga(0, s(s(0))) → mult73_out_ga(0, s(s(0)))
mult73_in_ga(s(T195), s(s(T197))) → U3_ga(T195, T197, mult73_in_ga(T195, T197))
U3_ga(T195, T197, mult73_out_ga(T195, T197)) → mult73_out_ga(s(T195), s(s(T197)))
U11_gga(T161, T164, mult73_out_ga(T161, T164)) → mult12_out_gga(s(T161), s(s(0)), s(s(T164)))
mult12_in_gga(0, s(s(s(0))), s(s(s(0)))) → mult12_out_gga(0, s(s(s(0))), s(s(s(0))))
mult12_in_gga(s(T234), s(s(s(0))), s(s(s(T237)))) → U12_gga(T234, T237, mult106_in_ga(T234, T237))
mult106_in_ga(0, s(s(s(0)))) → mult106_out_ga(0, s(s(s(0))))
mult106_in_ga(s(T279), s(s(s(T281)))) → U4_ga(T279, T281, mult106_in_ga(T279, T281))
U4_ga(T279, T281, mult106_out_ga(T279, T281)) → mult106_out_ga(s(T279), s(s(s(T281))))
U12_gga(T234, T237, mult106_out_ga(T234, T237)) → mult12_out_gga(s(T234), s(s(s(0))), s(s(s(T237))))
mult12_in_gga(0, s(s(s(s(0)))), s(s(s(s(0))))) → mult12_out_gga(0, s(s(s(s(0)))), s(s(s(s(0)))))
mult12_in_gga(s(T318), s(s(s(s(0)))), s(s(s(s(T321))))) → U13_gga(T318, T321, mult144_in_ga(T318, T321))
mult144_in_ga(0, s(s(s(s(0))))) → mult144_out_ga(0, s(s(s(s(0)))))
mult144_in_ga(s(T374), s(s(s(s(T376))))) → U5_ga(T374, T376, mult144_in_ga(T374, T376))
U5_ga(T374, T376, mult144_out_ga(T374, T376)) → mult144_out_ga(s(T374), s(s(s(s(T376)))))
U13_gga(T318, T321, mult144_out_ga(T318, T321)) → mult12_out_gga(s(T318), s(s(s(s(0)))), s(s(s(s(T321)))))
mult12_in_gga(0, s(s(s(s(s(0))))), s(s(s(s(s(0)))))) → mult12_out_gga(0, s(s(s(s(s(0))))), s(s(s(s(s(0))))))
mult12_in_gga(s(T413), s(s(s(s(s(0))))), s(s(s(s(s(T416)))))) → U14_gga(T413, T416, mult187_in_ga(T413, T416))
mult187_in_ga(0, s(s(s(s(s(0)))))) → mult187_out_ga(0, s(s(s(s(s(0))))))
mult187_in_ga(s(T480), s(s(s(s(s(T482)))))) → U6_ga(T480, T482, mult187_in_ga(T480, T482))
U6_ga(T480, T482, mult187_out_ga(T480, T482)) → mult187_out_ga(s(T480), s(s(s(s(s(T482))))))
U14_gga(T413, T416, mult187_out_ga(T413, T416)) → mult12_out_gga(s(T413), s(s(s(s(s(0))))), s(s(s(s(s(T416))))))
mult12_in_gga(0, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(0))))))) → mult12_out_gga(0, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(0)))))))
mult12_in_gga(s(T519), s(s(s(s(s(s(0)))))), s(s(s(s(s(s(T522))))))) → U15_gga(T519, T522, mult235_in_ga(T519, T522))
mult235_in_ga(0, s(s(s(s(s(s(0))))))) → mult235_out_ga(0, s(s(s(s(s(s(0)))))))
mult235_in_ga(s(T597), s(s(s(s(s(s(T599))))))) → U7_ga(T597, T599, mult235_in_ga(T597, T599))
U7_ga(T597, T599, mult235_out_ga(T597, T599)) → mult235_out_ga(s(T597), s(s(s(s(s(s(T599)))))))
U15_gga(T519, T522, mult235_out_ga(T519, T522)) → mult12_out_gga(s(T519), s(s(s(s(s(s(0)))))), s(s(s(s(s(s(T522)))))))
mult12_in_gga(0, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(0)))))))) → mult12_out_gga(0, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(0))))))))
mult12_in_gga(s(T636), s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(T639)))))))) → U16_gga(T636, T639, mult288_in_ga(T636, T639))
mult288_in_ga(0, s(s(s(s(s(s(s(0)))))))) → mult288_out_ga(0, s(s(s(s(s(s(s(0))))))))
mult288_in_ga(s(T725), s(s(s(s(s(s(s(T727)))))))) → U8_ga(T725, T727, mult288_in_ga(T725, T727))
U8_ga(T725, T727, mult288_out_ga(T725, T727)) → mult288_out_ga(s(T725), s(s(s(s(s(s(s(T727))))))))
U16_gga(T636, T639, mult288_out_ga(T636, T639)) → mult12_out_gga(s(T636), s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(T639))))))))
mult12_in_gga(T740, s(s(s(s(s(s(s(s(T742)))))))), s(s(s(s(s(s(s(s(T744))))))))) → U17_gga(T740, T742, T744, mult338_in_ggga(T740, s(s(s(s(s(s(s(T742))))))), T742, T744))
mult338_in_ggga(0, T754, 0, 0) → mult338_out_ggga(0, T754, 0, 0)
mult338_in_ggga(s(T767), T768, 0, T770) → U18_ggga(T767, T768, T770, mult12_in_gga(T767, s(T768), T770))
U18_ggga(T767, T768, T770, mult12_out_gga(T767, s(T768), T770)) → mult338_out_ggga(s(T767), T768, 0, T770)
mult338_in_ggga(T786, T787, s(T788), s(T790)) → U19_ggga(T786, T787, T788, T790, mult338_in_ggga(T786, T787, T788, T790))
U19_ggga(T786, T787, T788, T790, mult338_out_ggga(T786, T787, T788, T790)) → mult338_out_ggga(T786, T787, s(T788), s(T790))
U17_gga(T740, T742, T744, mult338_out_ggga(T740, s(s(s(s(s(s(s(T742))))))), T742, T744)) → mult12_out_gga(T740, s(s(s(s(s(s(s(s(T742)))))))), s(s(s(s(s(s(s(s(T744)))))))))
U20_gga(T28, T29, T31, mult12_out_gga(T28, T29, T31)) → times1_out_gga(s(T28), T29, T31)
TIMES1_IN_GGA(s(T28), T29, T31) → U20_GGA(T28, T29, T31, mult12_in_gga(T28, T29, T31))
TIMES1_IN_GGA(s(T28), T29, T31) → MULT12_IN_GGA(T28, T29, T31)
MULT12_IN_GGA(s(T51), 0, T54) → U9_GGA(T51, T54, mult22_in_ga(T51, T54))
MULT12_IN_GGA(s(T51), 0, T54) → MULT22_IN_GA(T51, T54)
MULT22_IN_GA(s(T63), T65) → U1_GA(T63, T65, mult22_in_ga(T63, T65))
MULT22_IN_GA(s(T63), T65) → MULT22_IN_GA(T63, T65)
MULT12_IN_GGA(s(T99), s(0), s(T102)) → U10_GGA(T99, T102, mult45_in_ga(T99, T102))
MULT12_IN_GGA(s(T99), s(0), s(T102)) → MULT45_IN_GA(T99, T102)
MULT45_IN_GA(s(T122), s(T124)) → U2_GA(T122, T124, mult45_in_ga(T122, T124))
MULT45_IN_GA(s(T122), s(T124)) → MULT45_IN_GA(T122, T124)
MULT12_IN_GGA(s(T161), s(s(0)), s(s(T164))) → U11_GGA(T161, T164, mult73_in_ga(T161, T164))
MULT12_IN_GGA(s(T161), s(s(0)), s(s(T164))) → MULT73_IN_GA(T161, T164)
MULT73_IN_GA(s(T195), s(s(T197))) → U3_GA(T195, T197, mult73_in_ga(T195, T197))
MULT73_IN_GA(s(T195), s(s(T197))) → MULT73_IN_GA(T195, T197)
MULT12_IN_GGA(s(T234), s(s(s(0))), s(s(s(T237)))) → U12_GGA(T234, T237, mult106_in_ga(T234, T237))
MULT12_IN_GGA(s(T234), s(s(s(0))), s(s(s(T237)))) → MULT106_IN_GA(T234, T237)
MULT106_IN_GA(s(T279), s(s(s(T281)))) → U4_GA(T279, T281, mult106_in_ga(T279, T281))
MULT106_IN_GA(s(T279), s(s(s(T281)))) → MULT106_IN_GA(T279, T281)
MULT12_IN_GGA(s(T318), s(s(s(s(0)))), s(s(s(s(T321))))) → U13_GGA(T318, T321, mult144_in_ga(T318, T321))
MULT12_IN_GGA(s(T318), s(s(s(s(0)))), s(s(s(s(T321))))) → MULT144_IN_GA(T318, T321)
MULT144_IN_GA(s(T374), s(s(s(s(T376))))) → U5_GA(T374, T376, mult144_in_ga(T374, T376))
MULT144_IN_GA(s(T374), s(s(s(s(T376))))) → MULT144_IN_GA(T374, T376)
MULT12_IN_GGA(s(T413), s(s(s(s(s(0))))), s(s(s(s(s(T416)))))) → U14_GGA(T413, T416, mult187_in_ga(T413, T416))
MULT12_IN_GGA(s(T413), s(s(s(s(s(0))))), s(s(s(s(s(T416)))))) → MULT187_IN_GA(T413, T416)
MULT187_IN_GA(s(T480), s(s(s(s(s(T482)))))) → U6_GA(T480, T482, mult187_in_ga(T480, T482))
MULT187_IN_GA(s(T480), s(s(s(s(s(T482)))))) → MULT187_IN_GA(T480, T482)
MULT12_IN_GGA(s(T519), s(s(s(s(s(s(0)))))), s(s(s(s(s(s(T522))))))) → U15_GGA(T519, T522, mult235_in_ga(T519, T522))
MULT12_IN_GGA(s(T519), s(s(s(s(s(s(0)))))), s(s(s(s(s(s(T522))))))) → MULT235_IN_GA(T519, T522)
MULT235_IN_GA(s(T597), s(s(s(s(s(s(T599))))))) → U7_GA(T597, T599, mult235_in_ga(T597, T599))
MULT235_IN_GA(s(T597), s(s(s(s(s(s(T599))))))) → MULT235_IN_GA(T597, T599)
MULT12_IN_GGA(s(T636), s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(T639)))))))) → U16_GGA(T636, T639, mult288_in_ga(T636, T639))
MULT12_IN_GGA(s(T636), s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(T639)))))))) → MULT288_IN_GA(T636, T639)
MULT288_IN_GA(s(T725), s(s(s(s(s(s(s(T727)))))))) → U8_GA(T725, T727, mult288_in_ga(T725, T727))
MULT288_IN_GA(s(T725), s(s(s(s(s(s(s(T727)))))))) → MULT288_IN_GA(T725, T727)
MULT12_IN_GGA(T740, s(s(s(s(s(s(s(s(T742)))))))), s(s(s(s(s(s(s(s(T744))))))))) → U17_GGA(T740, T742, T744, mult338_in_ggga(T740, s(s(s(s(s(s(s(T742))))))), T742, T744))
MULT12_IN_GGA(T740, s(s(s(s(s(s(s(s(T742)))))))), s(s(s(s(s(s(s(s(T744))))))))) → MULT338_IN_GGGA(T740, s(s(s(s(s(s(s(T742))))))), T742, T744)
MULT338_IN_GGGA(s(T767), T768, 0, T770) → U18_GGGA(T767, T768, T770, mult12_in_gga(T767, s(T768), T770))
MULT338_IN_GGGA(s(T767), T768, 0, T770) → MULT12_IN_GGA(T767, s(T768), T770)
MULT338_IN_GGGA(T786, T787, s(T788), s(T790)) → U19_GGGA(T786, T787, T788, T790, mult338_in_ggga(T786, T787, T788, T790))
MULT338_IN_GGGA(T786, T787, s(T788), s(T790)) → MULT338_IN_GGGA(T786, T787, T788, T790)
times1_in_gga(0, T15, 0) → times1_out_gga(0, T15, 0)
times1_in_gga(s(T28), T29, T31) → U20_gga(T28, T29, T31, mult12_in_gga(T28, T29, T31))
mult12_in_gga(0, 0, 0) → mult12_out_gga(0, 0, 0)
mult12_in_gga(s(T51), 0, T54) → U9_gga(T51, T54, mult22_in_ga(T51, T54))
mult22_in_ga(0, 0) → mult22_out_ga(0, 0)
mult22_in_ga(s(T63), T65) → U1_ga(T63, T65, mult22_in_ga(T63, T65))
U1_ga(T63, T65, mult22_out_ga(T63, T65)) → mult22_out_ga(s(T63), T65)
U9_gga(T51, T54, mult22_out_ga(T51, T54)) → mult12_out_gga(s(T51), 0, T54)
mult12_in_gga(0, s(0), s(0)) → mult12_out_gga(0, s(0), s(0))
mult12_in_gga(s(T99), s(0), s(T102)) → U10_gga(T99, T102, mult45_in_ga(T99, T102))
mult45_in_ga(0, s(0)) → mult45_out_ga(0, s(0))
mult45_in_ga(s(T122), s(T124)) → U2_ga(T122, T124, mult45_in_ga(T122, T124))
U2_ga(T122, T124, mult45_out_ga(T122, T124)) → mult45_out_ga(s(T122), s(T124))
U10_gga(T99, T102, mult45_out_ga(T99, T102)) → mult12_out_gga(s(T99), s(0), s(T102))
mult12_in_gga(0, s(s(0)), s(s(0))) → mult12_out_gga(0, s(s(0)), s(s(0)))
mult12_in_gga(s(T161), s(s(0)), s(s(T164))) → U11_gga(T161, T164, mult73_in_ga(T161, T164))
mult73_in_ga(0, s(s(0))) → mult73_out_ga(0, s(s(0)))
mult73_in_ga(s(T195), s(s(T197))) → U3_ga(T195, T197, mult73_in_ga(T195, T197))
U3_ga(T195, T197, mult73_out_ga(T195, T197)) → mult73_out_ga(s(T195), s(s(T197)))
U11_gga(T161, T164, mult73_out_ga(T161, T164)) → mult12_out_gga(s(T161), s(s(0)), s(s(T164)))
mult12_in_gga(0, s(s(s(0))), s(s(s(0)))) → mult12_out_gga(0, s(s(s(0))), s(s(s(0))))
mult12_in_gga(s(T234), s(s(s(0))), s(s(s(T237)))) → U12_gga(T234, T237, mult106_in_ga(T234, T237))
mult106_in_ga(0, s(s(s(0)))) → mult106_out_ga(0, s(s(s(0))))
mult106_in_ga(s(T279), s(s(s(T281)))) → U4_ga(T279, T281, mult106_in_ga(T279, T281))
U4_ga(T279, T281, mult106_out_ga(T279, T281)) → mult106_out_ga(s(T279), s(s(s(T281))))
U12_gga(T234, T237, mult106_out_ga(T234, T237)) → mult12_out_gga(s(T234), s(s(s(0))), s(s(s(T237))))
mult12_in_gga(0, s(s(s(s(0)))), s(s(s(s(0))))) → mult12_out_gga(0, s(s(s(s(0)))), s(s(s(s(0)))))
mult12_in_gga(s(T318), s(s(s(s(0)))), s(s(s(s(T321))))) → U13_gga(T318, T321, mult144_in_ga(T318, T321))
mult144_in_ga(0, s(s(s(s(0))))) → mult144_out_ga(0, s(s(s(s(0)))))
mult144_in_ga(s(T374), s(s(s(s(T376))))) → U5_ga(T374, T376, mult144_in_ga(T374, T376))
U5_ga(T374, T376, mult144_out_ga(T374, T376)) → mult144_out_ga(s(T374), s(s(s(s(T376)))))
U13_gga(T318, T321, mult144_out_ga(T318, T321)) → mult12_out_gga(s(T318), s(s(s(s(0)))), s(s(s(s(T321)))))
mult12_in_gga(0, s(s(s(s(s(0))))), s(s(s(s(s(0)))))) → mult12_out_gga(0, s(s(s(s(s(0))))), s(s(s(s(s(0))))))
mult12_in_gga(s(T413), s(s(s(s(s(0))))), s(s(s(s(s(T416)))))) → U14_gga(T413, T416, mult187_in_ga(T413, T416))
mult187_in_ga(0, s(s(s(s(s(0)))))) → mult187_out_ga(0, s(s(s(s(s(0))))))
mult187_in_ga(s(T480), s(s(s(s(s(T482)))))) → U6_ga(T480, T482, mult187_in_ga(T480, T482))
U6_ga(T480, T482, mult187_out_ga(T480, T482)) → mult187_out_ga(s(T480), s(s(s(s(s(T482))))))
U14_gga(T413, T416, mult187_out_ga(T413, T416)) → mult12_out_gga(s(T413), s(s(s(s(s(0))))), s(s(s(s(s(T416))))))
mult12_in_gga(0, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(0))))))) → mult12_out_gga(0, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(0)))))))
mult12_in_gga(s(T519), s(s(s(s(s(s(0)))))), s(s(s(s(s(s(T522))))))) → U15_gga(T519, T522, mult235_in_ga(T519, T522))
mult235_in_ga(0, s(s(s(s(s(s(0))))))) → mult235_out_ga(0, s(s(s(s(s(s(0)))))))
mult235_in_ga(s(T597), s(s(s(s(s(s(T599))))))) → U7_ga(T597, T599, mult235_in_ga(T597, T599))
U7_ga(T597, T599, mult235_out_ga(T597, T599)) → mult235_out_ga(s(T597), s(s(s(s(s(s(T599)))))))
U15_gga(T519, T522, mult235_out_ga(T519, T522)) → mult12_out_gga(s(T519), s(s(s(s(s(s(0)))))), s(s(s(s(s(s(T522)))))))
mult12_in_gga(0, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(0)))))))) → mult12_out_gga(0, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(0))))))))
mult12_in_gga(s(T636), s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(T639)))))))) → U16_gga(T636, T639, mult288_in_ga(T636, T639))
mult288_in_ga(0, s(s(s(s(s(s(s(0)))))))) → mult288_out_ga(0, s(s(s(s(s(s(s(0))))))))
mult288_in_ga(s(T725), s(s(s(s(s(s(s(T727)))))))) → U8_ga(T725, T727, mult288_in_ga(T725, T727))
U8_ga(T725, T727, mult288_out_ga(T725, T727)) → mult288_out_ga(s(T725), s(s(s(s(s(s(s(T727))))))))
U16_gga(T636, T639, mult288_out_ga(T636, T639)) → mult12_out_gga(s(T636), s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(T639))))))))
mult12_in_gga(T740, s(s(s(s(s(s(s(s(T742)))))))), s(s(s(s(s(s(s(s(T744))))))))) → U17_gga(T740, T742, T744, mult338_in_ggga(T740, s(s(s(s(s(s(s(T742))))))), T742, T744))
mult338_in_ggga(0, T754, 0, 0) → mult338_out_ggga(0, T754, 0, 0)
mult338_in_ggga(s(T767), T768, 0, T770) → U18_ggga(T767, T768, T770, mult12_in_gga(T767, s(T768), T770))
U18_ggga(T767, T768, T770, mult12_out_gga(T767, s(T768), T770)) → mult338_out_ggga(s(T767), T768, 0, T770)
mult338_in_ggga(T786, T787, s(T788), s(T790)) → U19_ggga(T786, T787, T788, T790, mult338_in_ggga(T786, T787, T788, T790))
U19_ggga(T786, T787, T788, T790, mult338_out_ggga(T786, T787, T788, T790)) → mult338_out_ggga(T786, T787, s(T788), s(T790))
U17_gga(T740, T742, T744, mult338_out_ggga(T740, s(s(s(s(s(s(s(T742))))))), T742, T744)) → mult12_out_gga(T740, s(s(s(s(s(s(s(s(T742)))))))), s(s(s(s(s(s(s(s(T744)))))))))
U20_gga(T28, T29, T31, mult12_out_gga(T28, T29, T31)) → times1_out_gga(s(T28), T29, T31)
TIMES1_IN_GGA(s(T28), T29, T31) → U20_GGA(T28, T29, T31, mult12_in_gga(T28, T29, T31))
TIMES1_IN_GGA(s(T28), T29, T31) → MULT12_IN_GGA(T28, T29, T31)
MULT12_IN_GGA(s(T51), 0, T54) → U9_GGA(T51, T54, mult22_in_ga(T51, T54))
MULT12_IN_GGA(s(T51), 0, T54) → MULT22_IN_GA(T51, T54)
MULT22_IN_GA(s(T63), T65) → U1_GA(T63, T65, mult22_in_ga(T63, T65))
MULT22_IN_GA(s(T63), T65) → MULT22_IN_GA(T63, T65)
MULT12_IN_GGA(s(T99), s(0), s(T102)) → U10_GGA(T99, T102, mult45_in_ga(T99, T102))
MULT12_IN_GGA(s(T99), s(0), s(T102)) → MULT45_IN_GA(T99, T102)
MULT45_IN_GA(s(T122), s(T124)) → U2_GA(T122, T124, mult45_in_ga(T122, T124))
MULT45_IN_GA(s(T122), s(T124)) → MULT45_IN_GA(T122, T124)
MULT12_IN_GGA(s(T161), s(s(0)), s(s(T164))) → U11_GGA(T161, T164, mult73_in_ga(T161, T164))
MULT12_IN_GGA(s(T161), s(s(0)), s(s(T164))) → MULT73_IN_GA(T161, T164)
MULT73_IN_GA(s(T195), s(s(T197))) → U3_GA(T195, T197, mult73_in_ga(T195, T197))
MULT73_IN_GA(s(T195), s(s(T197))) → MULT73_IN_GA(T195, T197)
MULT12_IN_GGA(s(T234), s(s(s(0))), s(s(s(T237)))) → U12_GGA(T234, T237, mult106_in_ga(T234, T237))
MULT12_IN_GGA(s(T234), s(s(s(0))), s(s(s(T237)))) → MULT106_IN_GA(T234, T237)
MULT106_IN_GA(s(T279), s(s(s(T281)))) → U4_GA(T279, T281, mult106_in_ga(T279, T281))
MULT106_IN_GA(s(T279), s(s(s(T281)))) → MULT106_IN_GA(T279, T281)
MULT12_IN_GGA(s(T318), s(s(s(s(0)))), s(s(s(s(T321))))) → U13_GGA(T318, T321, mult144_in_ga(T318, T321))
MULT12_IN_GGA(s(T318), s(s(s(s(0)))), s(s(s(s(T321))))) → MULT144_IN_GA(T318, T321)
MULT144_IN_GA(s(T374), s(s(s(s(T376))))) → U5_GA(T374, T376, mult144_in_ga(T374, T376))
MULT144_IN_GA(s(T374), s(s(s(s(T376))))) → MULT144_IN_GA(T374, T376)
MULT12_IN_GGA(s(T413), s(s(s(s(s(0))))), s(s(s(s(s(T416)))))) → U14_GGA(T413, T416, mult187_in_ga(T413, T416))
MULT12_IN_GGA(s(T413), s(s(s(s(s(0))))), s(s(s(s(s(T416)))))) → MULT187_IN_GA(T413, T416)
MULT187_IN_GA(s(T480), s(s(s(s(s(T482)))))) → U6_GA(T480, T482, mult187_in_ga(T480, T482))
MULT187_IN_GA(s(T480), s(s(s(s(s(T482)))))) → MULT187_IN_GA(T480, T482)
MULT12_IN_GGA(s(T519), s(s(s(s(s(s(0)))))), s(s(s(s(s(s(T522))))))) → U15_GGA(T519, T522, mult235_in_ga(T519, T522))
MULT12_IN_GGA(s(T519), s(s(s(s(s(s(0)))))), s(s(s(s(s(s(T522))))))) → MULT235_IN_GA(T519, T522)
MULT235_IN_GA(s(T597), s(s(s(s(s(s(T599))))))) → U7_GA(T597, T599, mult235_in_ga(T597, T599))
MULT235_IN_GA(s(T597), s(s(s(s(s(s(T599))))))) → MULT235_IN_GA(T597, T599)
MULT12_IN_GGA(s(T636), s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(T639)))))))) → U16_GGA(T636, T639, mult288_in_ga(T636, T639))
MULT12_IN_GGA(s(T636), s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(T639)))))))) → MULT288_IN_GA(T636, T639)
MULT288_IN_GA(s(T725), s(s(s(s(s(s(s(T727)))))))) → U8_GA(T725, T727, mult288_in_ga(T725, T727))
MULT288_IN_GA(s(T725), s(s(s(s(s(s(s(T727)))))))) → MULT288_IN_GA(T725, T727)
MULT12_IN_GGA(T740, s(s(s(s(s(s(s(s(T742)))))))), s(s(s(s(s(s(s(s(T744))))))))) → U17_GGA(T740, T742, T744, mult338_in_ggga(T740, s(s(s(s(s(s(s(T742))))))), T742, T744))
MULT12_IN_GGA(T740, s(s(s(s(s(s(s(s(T742)))))))), s(s(s(s(s(s(s(s(T744))))))))) → MULT338_IN_GGGA(T740, s(s(s(s(s(s(s(T742))))))), T742, T744)
MULT338_IN_GGGA(s(T767), T768, 0, T770) → U18_GGGA(T767, T768, T770, mult12_in_gga(T767, s(T768), T770))
MULT338_IN_GGGA(s(T767), T768, 0, T770) → MULT12_IN_GGA(T767, s(T768), T770)
MULT338_IN_GGGA(T786, T787, s(T788), s(T790)) → U19_GGGA(T786, T787, T788, T790, mult338_in_ggga(T786, T787, T788, T790))
MULT338_IN_GGGA(T786, T787, s(T788), s(T790)) → MULT338_IN_GGGA(T786, T787, T788, T790)
times1_in_gga(0, T15, 0) → times1_out_gga(0, T15, 0)
times1_in_gga(s(T28), T29, T31) → U20_gga(T28, T29, T31, mult12_in_gga(T28, T29, T31))
mult12_in_gga(0, 0, 0) → mult12_out_gga(0, 0, 0)
mult12_in_gga(s(T51), 0, T54) → U9_gga(T51, T54, mult22_in_ga(T51, T54))
mult22_in_ga(0, 0) → mult22_out_ga(0, 0)
mult22_in_ga(s(T63), T65) → U1_ga(T63, T65, mult22_in_ga(T63, T65))
U1_ga(T63, T65, mult22_out_ga(T63, T65)) → mult22_out_ga(s(T63), T65)
U9_gga(T51, T54, mult22_out_ga(T51, T54)) → mult12_out_gga(s(T51), 0, T54)
mult12_in_gga(0, s(0), s(0)) → mult12_out_gga(0, s(0), s(0))
mult12_in_gga(s(T99), s(0), s(T102)) → U10_gga(T99, T102, mult45_in_ga(T99, T102))
mult45_in_ga(0, s(0)) → mult45_out_ga(0, s(0))
mult45_in_ga(s(T122), s(T124)) → U2_ga(T122, T124, mult45_in_ga(T122, T124))
U2_ga(T122, T124, mult45_out_ga(T122, T124)) → mult45_out_ga(s(T122), s(T124))
U10_gga(T99, T102, mult45_out_ga(T99, T102)) → mult12_out_gga(s(T99), s(0), s(T102))
mult12_in_gga(0, s(s(0)), s(s(0))) → mult12_out_gga(0, s(s(0)), s(s(0)))
mult12_in_gga(s(T161), s(s(0)), s(s(T164))) → U11_gga(T161, T164, mult73_in_ga(T161, T164))
mult73_in_ga(0, s(s(0))) → mult73_out_ga(0, s(s(0)))
mult73_in_ga(s(T195), s(s(T197))) → U3_ga(T195, T197, mult73_in_ga(T195, T197))
U3_ga(T195, T197, mult73_out_ga(T195, T197)) → mult73_out_ga(s(T195), s(s(T197)))
U11_gga(T161, T164, mult73_out_ga(T161, T164)) → mult12_out_gga(s(T161), s(s(0)), s(s(T164)))
mult12_in_gga(0, s(s(s(0))), s(s(s(0)))) → mult12_out_gga(0, s(s(s(0))), s(s(s(0))))
mult12_in_gga(s(T234), s(s(s(0))), s(s(s(T237)))) → U12_gga(T234, T237, mult106_in_ga(T234, T237))
mult106_in_ga(0, s(s(s(0)))) → mult106_out_ga(0, s(s(s(0))))
mult106_in_ga(s(T279), s(s(s(T281)))) → U4_ga(T279, T281, mult106_in_ga(T279, T281))
U4_ga(T279, T281, mult106_out_ga(T279, T281)) → mult106_out_ga(s(T279), s(s(s(T281))))
U12_gga(T234, T237, mult106_out_ga(T234, T237)) → mult12_out_gga(s(T234), s(s(s(0))), s(s(s(T237))))
mult12_in_gga(0, s(s(s(s(0)))), s(s(s(s(0))))) → mult12_out_gga(0, s(s(s(s(0)))), s(s(s(s(0)))))
mult12_in_gga(s(T318), s(s(s(s(0)))), s(s(s(s(T321))))) → U13_gga(T318, T321, mult144_in_ga(T318, T321))
mult144_in_ga(0, s(s(s(s(0))))) → mult144_out_ga(0, s(s(s(s(0)))))
mult144_in_ga(s(T374), s(s(s(s(T376))))) → U5_ga(T374, T376, mult144_in_ga(T374, T376))
U5_ga(T374, T376, mult144_out_ga(T374, T376)) → mult144_out_ga(s(T374), s(s(s(s(T376)))))
U13_gga(T318, T321, mult144_out_ga(T318, T321)) → mult12_out_gga(s(T318), s(s(s(s(0)))), s(s(s(s(T321)))))
mult12_in_gga(0, s(s(s(s(s(0))))), s(s(s(s(s(0)))))) → mult12_out_gga(0, s(s(s(s(s(0))))), s(s(s(s(s(0))))))
mult12_in_gga(s(T413), s(s(s(s(s(0))))), s(s(s(s(s(T416)))))) → U14_gga(T413, T416, mult187_in_ga(T413, T416))
mult187_in_ga(0, s(s(s(s(s(0)))))) → mult187_out_ga(0, s(s(s(s(s(0))))))
mult187_in_ga(s(T480), s(s(s(s(s(T482)))))) → U6_ga(T480, T482, mult187_in_ga(T480, T482))
U6_ga(T480, T482, mult187_out_ga(T480, T482)) → mult187_out_ga(s(T480), s(s(s(s(s(T482))))))
U14_gga(T413, T416, mult187_out_ga(T413, T416)) → mult12_out_gga(s(T413), s(s(s(s(s(0))))), s(s(s(s(s(T416))))))
mult12_in_gga(0, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(0))))))) → mult12_out_gga(0, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(0)))))))
mult12_in_gga(s(T519), s(s(s(s(s(s(0)))))), s(s(s(s(s(s(T522))))))) → U15_gga(T519, T522, mult235_in_ga(T519, T522))
mult235_in_ga(0, s(s(s(s(s(s(0))))))) → mult235_out_ga(0, s(s(s(s(s(s(0)))))))
mult235_in_ga(s(T597), s(s(s(s(s(s(T599))))))) → U7_ga(T597, T599, mult235_in_ga(T597, T599))
U7_ga(T597, T599, mult235_out_ga(T597, T599)) → mult235_out_ga(s(T597), s(s(s(s(s(s(T599)))))))
U15_gga(T519, T522, mult235_out_ga(T519, T522)) → mult12_out_gga(s(T519), s(s(s(s(s(s(0)))))), s(s(s(s(s(s(T522)))))))
mult12_in_gga(0, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(0)))))))) → mult12_out_gga(0, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(0))))))))
mult12_in_gga(s(T636), s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(T639)))))))) → U16_gga(T636, T639, mult288_in_ga(T636, T639))
mult288_in_ga(0, s(s(s(s(s(s(s(0)))))))) → mult288_out_ga(0, s(s(s(s(s(s(s(0))))))))
mult288_in_ga(s(T725), s(s(s(s(s(s(s(T727)))))))) → U8_ga(T725, T727, mult288_in_ga(T725, T727))
U8_ga(T725, T727, mult288_out_ga(T725, T727)) → mult288_out_ga(s(T725), s(s(s(s(s(s(s(T727))))))))
U16_gga(T636, T639, mult288_out_ga(T636, T639)) → mult12_out_gga(s(T636), s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(T639))))))))
mult12_in_gga(T740, s(s(s(s(s(s(s(s(T742)))))))), s(s(s(s(s(s(s(s(T744))))))))) → U17_gga(T740, T742, T744, mult338_in_ggga(T740, s(s(s(s(s(s(s(T742))))))), T742, T744))
mult338_in_ggga(0, T754, 0, 0) → mult338_out_ggga(0, T754, 0, 0)
mult338_in_ggga(s(T767), T768, 0, T770) → U18_ggga(T767, T768, T770, mult12_in_gga(T767, s(T768), T770))
U18_ggga(T767, T768, T770, mult12_out_gga(T767, s(T768), T770)) → mult338_out_ggga(s(T767), T768, 0, T770)
mult338_in_ggga(T786, T787, s(T788), s(T790)) → U19_ggga(T786, T787, T788, T790, mult338_in_ggga(T786, T787, T788, T790))
U19_ggga(T786, T787, T788, T790, mult338_out_ggga(T786, T787, T788, T790)) → mult338_out_ggga(T786, T787, s(T788), s(T790))
U17_gga(T740, T742, T744, mult338_out_ggga(T740, s(s(s(s(s(s(s(T742))))))), T742, T744)) → mult12_out_gga(T740, s(s(s(s(s(s(s(s(T742)))))))), s(s(s(s(s(s(s(s(T744)))))))))
U20_gga(T28, T29, T31, mult12_out_gga(T28, T29, T31)) → times1_out_gga(s(T28), T29, T31)
MULT288_IN_GA(s(T725), s(s(s(s(s(s(s(T727)))))))) → MULT288_IN_GA(T725, T727)
times1_in_gga(0, T15, 0) → times1_out_gga(0, T15, 0)
times1_in_gga(s(T28), T29, T31) → U20_gga(T28, T29, T31, mult12_in_gga(T28, T29, T31))
mult12_in_gga(0, 0, 0) → mult12_out_gga(0, 0, 0)
mult12_in_gga(s(T51), 0, T54) → U9_gga(T51, T54, mult22_in_ga(T51, T54))
mult22_in_ga(0, 0) → mult22_out_ga(0, 0)
mult22_in_ga(s(T63), T65) → U1_ga(T63, T65, mult22_in_ga(T63, T65))
U1_ga(T63, T65, mult22_out_ga(T63, T65)) → mult22_out_ga(s(T63), T65)
U9_gga(T51, T54, mult22_out_ga(T51, T54)) → mult12_out_gga(s(T51), 0, T54)
mult12_in_gga(0, s(0), s(0)) → mult12_out_gga(0, s(0), s(0))
mult12_in_gga(s(T99), s(0), s(T102)) → U10_gga(T99, T102, mult45_in_ga(T99, T102))
mult45_in_ga(0, s(0)) → mult45_out_ga(0, s(0))
mult45_in_ga(s(T122), s(T124)) → U2_ga(T122, T124, mult45_in_ga(T122, T124))
U2_ga(T122, T124, mult45_out_ga(T122, T124)) → mult45_out_ga(s(T122), s(T124))
U10_gga(T99, T102, mult45_out_ga(T99, T102)) → mult12_out_gga(s(T99), s(0), s(T102))
mult12_in_gga(0, s(s(0)), s(s(0))) → mult12_out_gga(0, s(s(0)), s(s(0)))
mult12_in_gga(s(T161), s(s(0)), s(s(T164))) → U11_gga(T161, T164, mult73_in_ga(T161, T164))
mult73_in_ga(0, s(s(0))) → mult73_out_ga(0, s(s(0)))
mult73_in_ga(s(T195), s(s(T197))) → U3_ga(T195, T197, mult73_in_ga(T195, T197))
U3_ga(T195, T197, mult73_out_ga(T195, T197)) → mult73_out_ga(s(T195), s(s(T197)))
U11_gga(T161, T164, mult73_out_ga(T161, T164)) → mult12_out_gga(s(T161), s(s(0)), s(s(T164)))
mult12_in_gga(0, s(s(s(0))), s(s(s(0)))) → mult12_out_gga(0, s(s(s(0))), s(s(s(0))))
mult12_in_gga(s(T234), s(s(s(0))), s(s(s(T237)))) → U12_gga(T234, T237, mult106_in_ga(T234, T237))
mult106_in_ga(0, s(s(s(0)))) → mult106_out_ga(0, s(s(s(0))))
mult106_in_ga(s(T279), s(s(s(T281)))) → U4_ga(T279, T281, mult106_in_ga(T279, T281))
U4_ga(T279, T281, mult106_out_ga(T279, T281)) → mult106_out_ga(s(T279), s(s(s(T281))))
U12_gga(T234, T237, mult106_out_ga(T234, T237)) → mult12_out_gga(s(T234), s(s(s(0))), s(s(s(T237))))
mult12_in_gga(0, s(s(s(s(0)))), s(s(s(s(0))))) → mult12_out_gga(0, s(s(s(s(0)))), s(s(s(s(0)))))
mult12_in_gga(s(T318), s(s(s(s(0)))), s(s(s(s(T321))))) → U13_gga(T318, T321, mult144_in_ga(T318, T321))
mult144_in_ga(0, s(s(s(s(0))))) → mult144_out_ga(0, s(s(s(s(0)))))
mult144_in_ga(s(T374), s(s(s(s(T376))))) → U5_ga(T374, T376, mult144_in_ga(T374, T376))
U5_ga(T374, T376, mult144_out_ga(T374, T376)) → mult144_out_ga(s(T374), s(s(s(s(T376)))))
U13_gga(T318, T321, mult144_out_ga(T318, T321)) → mult12_out_gga(s(T318), s(s(s(s(0)))), s(s(s(s(T321)))))
mult12_in_gga(0, s(s(s(s(s(0))))), s(s(s(s(s(0)))))) → mult12_out_gga(0, s(s(s(s(s(0))))), s(s(s(s(s(0))))))
mult12_in_gga(s(T413), s(s(s(s(s(0))))), s(s(s(s(s(T416)))))) → U14_gga(T413, T416, mult187_in_ga(T413, T416))
mult187_in_ga(0, s(s(s(s(s(0)))))) → mult187_out_ga(0, s(s(s(s(s(0))))))
mult187_in_ga(s(T480), s(s(s(s(s(T482)))))) → U6_ga(T480, T482, mult187_in_ga(T480, T482))
U6_ga(T480, T482, mult187_out_ga(T480, T482)) → mult187_out_ga(s(T480), s(s(s(s(s(T482))))))
U14_gga(T413, T416, mult187_out_ga(T413, T416)) → mult12_out_gga(s(T413), s(s(s(s(s(0))))), s(s(s(s(s(T416))))))
mult12_in_gga(0, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(0))))))) → mult12_out_gga(0, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(0)))))))
mult12_in_gga(s(T519), s(s(s(s(s(s(0)))))), s(s(s(s(s(s(T522))))))) → U15_gga(T519, T522, mult235_in_ga(T519, T522))
mult235_in_ga(0, s(s(s(s(s(s(0))))))) → mult235_out_ga(0, s(s(s(s(s(s(0)))))))
mult235_in_ga(s(T597), s(s(s(s(s(s(T599))))))) → U7_ga(T597, T599, mult235_in_ga(T597, T599))
U7_ga(T597, T599, mult235_out_ga(T597, T599)) → mult235_out_ga(s(T597), s(s(s(s(s(s(T599)))))))
U15_gga(T519, T522, mult235_out_ga(T519, T522)) → mult12_out_gga(s(T519), s(s(s(s(s(s(0)))))), s(s(s(s(s(s(T522)))))))
mult12_in_gga(0, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(0)))))))) → mult12_out_gga(0, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(0))))))))
mult12_in_gga(s(T636), s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(T639)))))))) → U16_gga(T636, T639, mult288_in_ga(T636, T639))
mult288_in_ga(0, s(s(s(s(s(s(s(0)))))))) → mult288_out_ga(0, s(s(s(s(s(s(s(0))))))))
mult288_in_ga(s(T725), s(s(s(s(s(s(s(T727)))))))) → U8_ga(T725, T727, mult288_in_ga(T725, T727))
U8_ga(T725, T727, mult288_out_ga(T725, T727)) → mult288_out_ga(s(T725), s(s(s(s(s(s(s(T727))))))))
U16_gga(T636, T639, mult288_out_ga(T636, T639)) → mult12_out_gga(s(T636), s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(T639))))))))
mult12_in_gga(T740, s(s(s(s(s(s(s(s(T742)))))))), s(s(s(s(s(s(s(s(T744))))))))) → U17_gga(T740, T742, T744, mult338_in_ggga(T740, s(s(s(s(s(s(s(T742))))))), T742, T744))
mult338_in_ggga(0, T754, 0, 0) → mult338_out_ggga(0, T754, 0, 0)
mult338_in_ggga(s(T767), T768, 0, T770) → U18_ggga(T767, T768, T770, mult12_in_gga(T767, s(T768), T770))
U18_ggga(T767, T768, T770, mult12_out_gga(T767, s(T768), T770)) → mult338_out_ggga(s(T767), T768, 0, T770)
mult338_in_ggga(T786, T787, s(T788), s(T790)) → U19_ggga(T786, T787, T788, T790, mult338_in_ggga(T786, T787, T788, T790))
U19_ggga(T786, T787, T788, T790, mult338_out_ggga(T786, T787, T788, T790)) → mult338_out_ggga(T786, T787, s(T788), s(T790))
U17_gga(T740, T742, T744, mult338_out_ggga(T740, s(s(s(s(s(s(s(T742))))))), T742, T744)) → mult12_out_gga(T740, s(s(s(s(s(s(s(s(T742)))))))), s(s(s(s(s(s(s(s(T744)))))))))
U20_gga(T28, T29, T31, mult12_out_gga(T28, T29, T31)) → times1_out_gga(s(T28), T29, T31)
MULT288_IN_GA(s(T725), s(s(s(s(s(s(s(T727)))))))) → MULT288_IN_GA(T725, T727)
MULT288_IN_GA(s(T725)) → MULT288_IN_GA(T725)
From the DPs we obtained the following set of size-change graphs:
MULT235_IN_GA(s(T597), s(s(s(s(s(s(T599))))))) → MULT235_IN_GA(T597, T599)
times1_in_gga(0, T15, 0) → times1_out_gga(0, T15, 0)
times1_in_gga(s(T28), T29, T31) → U20_gga(T28, T29, T31, mult12_in_gga(T28, T29, T31))
mult12_in_gga(0, 0, 0) → mult12_out_gga(0, 0, 0)
mult12_in_gga(s(T51), 0, T54) → U9_gga(T51, T54, mult22_in_ga(T51, T54))
mult22_in_ga(0, 0) → mult22_out_ga(0, 0)
mult22_in_ga(s(T63), T65) → U1_ga(T63, T65, mult22_in_ga(T63, T65))
U1_ga(T63, T65, mult22_out_ga(T63, T65)) → mult22_out_ga(s(T63), T65)
U9_gga(T51, T54, mult22_out_ga(T51, T54)) → mult12_out_gga(s(T51), 0, T54)
mult12_in_gga(0, s(0), s(0)) → mult12_out_gga(0, s(0), s(0))
mult12_in_gga(s(T99), s(0), s(T102)) → U10_gga(T99, T102, mult45_in_ga(T99, T102))
mult45_in_ga(0, s(0)) → mult45_out_ga(0, s(0))
mult45_in_ga(s(T122), s(T124)) → U2_ga(T122, T124, mult45_in_ga(T122, T124))
U2_ga(T122, T124, mult45_out_ga(T122, T124)) → mult45_out_ga(s(T122), s(T124))
U10_gga(T99, T102, mult45_out_ga(T99, T102)) → mult12_out_gga(s(T99), s(0), s(T102))
mult12_in_gga(0, s(s(0)), s(s(0))) → mult12_out_gga(0, s(s(0)), s(s(0)))
mult12_in_gga(s(T161), s(s(0)), s(s(T164))) → U11_gga(T161, T164, mult73_in_ga(T161, T164))
mult73_in_ga(0, s(s(0))) → mult73_out_ga(0, s(s(0)))
mult73_in_ga(s(T195), s(s(T197))) → U3_ga(T195, T197, mult73_in_ga(T195, T197))
U3_ga(T195, T197, mult73_out_ga(T195, T197)) → mult73_out_ga(s(T195), s(s(T197)))
U11_gga(T161, T164, mult73_out_ga(T161, T164)) → mult12_out_gga(s(T161), s(s(0)), s(s(T164)))
mult12_in_gga(0, s(s(s(0))), s(s(s(0)))) → mult12_out_gga(0, s(s(s(0))), s(s(s(0))))
mult12_in_gga(s(T234), s(s(s(0))), s(s(s(T237)))) → U12_gga(T234, T237, mult106_in_ga(T234, T237))
mult106_in_ga(0, s(s(s(0)))) → mult106_out_ga(0, s(s(s(0))))
mult106_in_ga(s(T279), s(s(s(T281)))) → U4_ga(T279, T281, mult106_in_ga(T279, T281))
U4_ga(T279, T281, mult106_out_ga(T279, T281)) → mult106_out_ga(s(T279), s(s(s(T281))))
U12_gga(T234, T237, mult106_out_ga(T234, T237)) → mult12_out_gga(s(T234), s(s(s(0))), s(s(s(T237))))
mult12_in_gga(0, s(s(s(s(0)))), s(s(s(s(0))))) → mult12_out_gga(0, s(s(s(s(0)))), s(s(s(s(0)))))
mult12_in_gga(s(T318), s(s(s(s(0)))), s(s(s(s(T321))))) → U13_gga(T318, T321, mult144_in_ga(T318, T321))
mult144_in_ga(0, s(s(s(s(0))))) → mult144_out_ga(0, s(s(s(s(0)))))
mult144_in_ga(s(T374), s(s(s(s(T376))))) → U5_ga(T374, T376, mult144_in_ga(T374, T376))
U5_ga(T374, T376, mult144_out_ga(T374, T376)) → mult144_out_ga(s(T374), s(s(s(s(T376)))))
U13_gga(T318, T321, mult144_out_ga(T318, T321)) → mult12_out_gga(s(T318), s(s(s(s(0)))), s(s(s(s(T321)))))
mult12_in_gga(0, s(s(s(s(s(0))))), s(s(s(s(s(0)))))) → mult12_out_gga(0, s(s(s(s(s(0))))), s(s(s(s(s(0))))))
mult12_in_gga(s(T413), s(s(s(s(s(0))))), s(s(s(s(s(T416)))))) → U14_gga(T413, T416, mult187_in_ga(T413, T416))
mult187_in_ga(0, s(s(s(s(s(0)))))) → mult187_out_ga(0, s(s(s(s(s(0))))))
mult187_in_ga(s(T480), s(s(s(s(s(T482)))))) → U6_ga(T480, T482, mult187_in_ga(T480, T482))
U6_ga(T480, T482, mult187_out_ga(T480, T482)) → mult187_out_ga(s(T480), s(s(s(s(s(T482))))))
U14_gga(T413, T416, mult187_out_ga(T413, T416)) → mult12_out_gga(s(T413), s(s(s(s(s(0))))), s(s(s(s(s(T416))))))
mult12_in_gga(0, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(0))))))) → mult12_out_gga(0, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(0)))))))
mult12_in_gga(s(T519), s(s(s(s(s(s(0)))))), s(s(s(s(s(s(T522))))))) → U15_gga(T519, T522, mult235_in_ga(T519, T522))
mult235_in_ga(0, s(s(s(s(s(s(0))))))) → mult235_out_ga(0, s(s(s(s(s(s(0)))))))
mult235_in_ga(s(T597), s(s(s(s(s(s(T599))))))) → U7_ga(T597, T599, mult235_in_ga(T597, T599))
U7_ga(T597, T599, mult235_out_ga(T597, T599)) → mult235_out_ga(s(T597), s(s(s(s(s(s(T599)))))))
U15_gga(T519, T522, mult235_out_ga(T519, T522)) → mult12_out_gga(s(T519), s(s(s(s(s(s(0)))))), s(s(s(s(s(s(T522)))))))
mult12_in_gga(0, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(0)))))))) → mult12_out_gga(0, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(0))))))))
mult12_in_gga(s(T636), s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(T639)))))))) → U16_gga(T636, T639, mult288_in_ga(T636, T639))
mult288_in_ga(0, s(s(s(s(s(s(s(0)))))))) → mult288_out_ga(0, s(s(s(s(s(s(s(0))))))))
mult288_in_ga(s(T725), s(s(s(s(s(s(s(T727)))))))) → U8_ga(T725, T727, mult288_in_ga(T725, T727))
U8_ga(T725, T727, mult288_out_ga(T725, T727)) → mult288_out_ga(s(T725), s(s(s(s(s(s(s(T727))))))))
U16_gga(T636, T639, mult288_out_ga(T636, T639)) → mult12_out_gga(s(T636), s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(T639))))))))
mult12_in_gga(T740, s(s(s(s(s(s(s(s(T742)))))))), s(s(s(s(s(s(s(s(T744))))))))) → U17_gga(T740, T742, T744, mult338_in_ggga(T740, s(s(s(s(s(s(s(T742))))))), T742, T744))
mult338_in_ggga(0, T754, 0, 0) → mult338_out_ggga(0, T754, 0, 0)
mult338_in_ggga(s(T767), T768, 0, T770) → U18_ggga(T767, T768, T770, mult12_in_gga(T767, s(T768), T770))
U18_ggga(T767, T768, T770, mult12_out_gga(T767, s(T768), T770)) → mult338_out_ggga(s(T767), T768, 0, T770)
mult338_in_ggga(T786, T787, s(T788), s(T790)) → U19_ggga(T786, T787, T788, T790, mult338_in_ggga(T786, T787, T788, T790))
U19_ggga(T786, T787, T788, T790, mult338_out_ggga(T786, T787, T788, T790)) → mult338_out_ggga(T786, T787, s(T788), s(T790))
U17_gga(T740, T742, T744, mult338_out_ggga(T740, s(s(s(s(s(s(s(T742))))))), T742, T744)) → mult12_out_gga(T740, s(s(s(s(s(s(s(s(T742)))))))), s(s(s(s(s(s(s(s(T744)))))))))
U20_gga(T28, T29, T31, mult12_out_gga(T28, T29, T31)) → times1_out_gga(s(T28), T29, T31)
MULT235_IN_GA(s(T597), s(s(s(s(s(s(T599))))))) → MULT235_IN_GA(T597, T599)
MULT235_IN_GA(s(T597)) → MULT235_IN_GA(T597)
From the DPs we obtained the following set of size-change graphs:
MULT187_IN_GA(s(T480), s(s(s(s(s(T482)))))) → MULT187_IN_GA(T480, T482)
times1_in_gga(0, T15, 0) → times1_out_gga(0, T15, 0)
times1_in_gga(s(T28), T29, T31) → U20_gga(T28, T29, T31, mult12_in_gga(T28, T29, T31))
mult12_in_gga(0, 0, 0) → mult12_out_gga(0, 0, 0)
mult12_in_gga(s(T51), 0, T54) → U9_gga(T51, T54, mult22_in_ga(T51, T54))
mult22_in_ga(0, 0) → mult22_out_ga(0, 0)
mult22_in_ga(s(T63), T65) → U1_ga(T63, T65, mult22_in_ga(T63, T65))
U1_ga(T63, T65, mult22_out_ga(T63, T65)) → mult22_out_ga(s(T63), T65)
U9_gga(T51, T54, mult22_out_ga(T51, T54)) → mult12_out_gga(s(T51), 0, T54)
mult12_in_gga(0, s(0), s(0)) → mult12_out_gga(0, s(0), s(0))
mult12_in_gga(s(T99), s(0), s(T102)) → U10_gga(T99, T102, mult45_in_ga(T99, T102))
mult45_in_ga(0, s(0)) → mult45_out_ga(0, s(0))
mult45_in_ga(s(T122), s(T124)) → U2_ga(T122, T124, mult45_in_ga(T122, T124))
U2_ga(T122, T124, mult45_out_ga(T122, T124)) → mult45_out_ga(s(T122), s(T124))
U10_gga(T99, T102, mult45_out_ga(T99, T102)) → mult12_out_gga(s(T99), s(0), s(T102))
mult12_in_gga(0, s(s(0)), s(s(0))) → mult12_out_gga(0, s(s(0)), s(s(0)))
mult12_in_gga(s(T161), s(s(0)), s(s(T164))) → U11_gga(T161, T164, mult73_in_ga(T161, T164))
mult73_in_ga(0, s(s(0))) → mult73_out_ga(0, s(s(0)))
mult73_in_ga(s(T195), s(s(T197))) → U3_ga(T195, T197, mult73_in_ga(T195, T197))
U3_ga(T195, T197, mult73_out_ga(T195, T197)) → mult73_out_ga(s(T195), s(s(T197)))
U11_gga(T161, T164, mult73_out_ga(T161, T164)) → mult12_out_gga(s(T161), s(s(0)), s(s(T164)))
mult12_in_gga(0, s(s(s(0))), s(s(s(0)))) → mult12_out_gga(0, s(s(s(0))), s(s(s(0))))
mult12_in_gga(s(T234), s(s(s(0))), s(s(s(T237)))) → U12_gga(T234, T237, mult106_in_ga(T234, T237))
mult106_in_ga(0, s(s(s(0)))) → mult106_out_ga(0, s(s(s(0))))
mult106_in_ga(s(T279), s(s(s(T281)))) → U4_ga(T279, T281, mult106_in_ga(T279, T281))
U4_ga(T279, T281, mult106_out_ga(T279, T281)) → mult106_out_ga(s(T279), s(s(s(T281))))
U12_gga(T234, T237, mult106_out_ga(T234, T237)) → mult12_out_gga(s(T234), s(s(s(0))), s(s(s(T237))))
mult12_in_gga(0, s(s(s(s(0)))), s(s(s(s(0))))) → mult12_out_gga(0, s(s(s(s(0)))), s(s(s(s(0)))))
mult12_in_gga(s(T318), s(s(s(s(0)))), s(s(s(s(T321))))) → U13_gga(T318, T321, mult144_in_ga(T318, T321))
mult144_in_ga(0, s(s(s(s(0))))) → mult144_out_ga(0, s(s(s(s(0)))))
mult144_in_ga(s(T374), s(s(s(s(T376))))) → U5_ga(T374, T376, mult144_in_ga(T374, T376))
U5_ga(T374, T376, mult144_out_ga(T374, T376)) → mult144_out_ga(s(T374), s(s(s(s(T376)))))
U13_gga(T318, T321, mult144_out_ga(T318, T321)) → mult12_out_gga(s(T318), s(s(s(s(0)))), s(s(s(s(T321)))))
mult12_in_gga(0, s(s(s(s(s(0))))), s(s(s(s(s(0)))))) → mult12_out_gga(0, s(s(s(s(s(0))))), s(s(s(s(s(0))))))
mult12_in_gga(s(T413), s(s(s(s(s(0))))), s(s(s(s(s(T416)))))) → U14_gga(T413, T416, mult187_in_ga(T413, T416))
mult187_in_ga(0, s(s(s(s(s(0)))))) → mult187_out_ga(0, s(s(s(s(s(0))))))
mult187_in_ga(s(T480), s(s(s(s(s(T482)))))) → U6_ga(T480, T482, mult187_in_ga(T480, T482))
U6_ga(T480, T482, mult187_out_ga(T480, T482)) → mult187_out_ga(s(T480), s(s(s(s(s(T482))))))
U14_gga(T413, T416, mult187_out_ga(T413, T416)) → mult12_out_gga(s(T413), s(s(s(s(s(0))))), s(s(s(s(s(T416))))))
mult12_in_gga(0, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(0))))))) → mult12_out_gga(0, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(0)))))))
mult12_in_gga(s(T519), s(s(s(s(s(s(0)))))), s(s(s(s(s(s(T522))))))) → U15_gga(T519, T522, mult235_in_ga(T519, T522))
mult235_in_ga(0, s(s(s(s(s(s(0))))))) → mult235_out_ga(0, s(s(s(s(s(s(0)))))))
mult235_in_ga(s(T597), s(s(s(s(s(s(T599))))))) → U7_ga(T597, T599, mult235_in_ga(T597, T599))
U7_ga(T597, T599, mult235_out_ga(T597, T599)) → mult235_out_ga(s(T597), s(s(s(s(s(s(T599)))))))
U15_gga(T519, T522, mult235_out_ga(T519, T522)) → mult12_out_gga(s(T519), s(s(s(s(s(s(0)))))), s(s(s(s(s(s(T522)))))))
mult12_in_gga(0, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(0)))))))) → mult12_out_gga(0, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(0))))))))
mult12_in_gga(s(T636), s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(T639)))))))) → U16_gga(T636, T639, mult288_in_ga(T636, T639))
mult288_in_ga(0, s(s(s(s(s(s(s(0)))))))) → mult288_out_ga(0, s(s(s(s(s(s(s(0))))))))
mult288_in_ga(s(T725), s(s(s(s(s(s(s(T727)))))))) → U8_ga(T725, T727, mult288_in_ga(T725, T727))
U8_ga(T725, T727, mult288_out_ga(T725, T727)) → mult288_out_ga(s(T725), s(s(s(s(s(s(s(T727))))))))
U16_gga(T636, T639, mult288_out_ga(T636, T639)) → mult12_out_gga(s(T636), s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(T639))))))))
mult12_in_gga(T740, s(s(s(s(s(s(s(s(T742)))))))), s(s(s(s(s(s(s(s(T744))))))))) → U17_gga(T740, T742, T744, mult338_in_ggga(T740, s(s(s(s(s(s(s(T742))))))), T742, T744))
mult338_in_ggga(0, T754, 0, 0) → mult338_out_ggga(0, T754, 0, 0)
mult338_in_ggga(s(T767), T768, 0, T770) → U18_ggga(T767, T768, T770, mult12_in_gga(T767, s(T768), T770))
U18_ggga(T767, T768, T770, mult12_out_gga(T767, s(T768), T770)) → mult338_out_ggga(s(T767), T768, 0, T770)
mult338_in_ggga(T786, T787, s(T788), s(T790)) → U19_ggga(T786, T787, T788, T790, mult338_in_ggga(T786, T787, T788, T790))
U19_ggga(T786, T787, T788, T790, mult338_out_ggga(T786, T787, T788, T790)) → mult338_out_ggga(T786, T787, s(T788), s(T790))
U17_gga(T740, T742, T744, mult338_out_ggga(T740, s(s(s(s(s(s(s(T742))))))), T742, T744)) → mult12_out_gga(T740, s(s(s(s(s(s(s(s(T742)))))))), s(s(s(s(s(s(s(s(T744)))))))))
U20_gga(T28, T29, T31, mult12_out_gga(T28, T29, T31)) → times1_out_gga(s(T28), T29, T31)
MULT187_IN_GA(s(T480), s(s(s(s(s(T482)))))) → MULT187_IN_GA(T480, T482)
MULT187_IN_GA(s(T480)) → MULT187_IN_GA(T480)
From the DPs we obtained the following set of size-change graphs:
MULT144_IN_GA(s(T374), s(s(s(s(T376))))) → MULT144_IN_GA(T374, T376)
times1_in_gga(0, T15, 0) → times1_out_gga(0, T15, 0)
times1_in_gga(s(T28), T29, T31) → U20_gga(T28, T29, T31, mult12_in_gga(T28, T29, T31))
mult12_in_gga(0, 0, 0) → mult12_out_gga(0, 0, 0)
mult12_in_gga(s(T51), 0, T54) → U9_gga(T51, T54, mult22_in_ga(T51, T54))
mult22_in_ga(0, 0) → mult22_out_ga(0, 0)
mult22_in_ga(s(T63), T65) → U1_ga(T63, T65, mult22_in_ga(T63, T65))
U1_ga(T63, T65, mult22_out_ga(T63, T65)) → mult22_out_ga(s(T63), T65)
U9_gga(T51, T54, mult22_out_ga(T51, T54)) → mult12_out_gga(s(T51), 0, T54)
mult12_in_gga(0, s(0), s(0)) → mult12_out_gga(0, s(0), s(0))
mult12_in_gga(s(T99), s(0), s(T102)) → U10_gga(T99, T102, mult45_in_ga(T99, T102))
mult45_in_ga(0, s(0)) → mult45_out_ga(0, s(0))
mult45_in_ga(s(T122), s(T124)) → U2_ga(T122, T124, mult45_in_ga(T122, T124))
U2_ga(T122, T124, mult45_out_ga(T122, T124)) → mult45_out_ga(s(T122), s(T124))
U10_gga(T99, T102, mult45_out_ga(T99, T102)) → mult12_out_gga(s(T99), s(0), s(T102))
mult12_in_gga(0, s(s(0)), s(s(0))) → mult12_out_gga(0, s(s(0)), s(s(0)))
mult12_in_gga(s(T161), s(s(0)), s(s(T164))) → U11_gga(T161, T164, mult73_in_ga(T161, T164))
mult73_in_ga(0, s(s(0))) → mult73_out_ga(0, s(s(0)))
mult73_in_ga(s(T195), s(s(T197))) → U3_ga(T195, T197, mult73_in_ga(T195, T197))
U3_ga(T195, T197, mult73_out_ga(T195, T197)) → mult73_out_ga(s(T195), s(s(T197)))
U11_gga(T161, T164, mult73_out_ga(T161, T164)) → mult12_out_gga(s(T161), s(s(0)), s(s(T164)))
mult12_in_gga(0, s(s(s(0))), s(s(s(0)))) → mult12_out_gga(0, s(s(s(0))), s(s(s(0))))
mult12_in_gga(s(T234), s(s(s(0))), s(s(s(T237)))) → U12_gga(T234, T237, mult106_in_ga(T234, T237))
mult106_in_ga(0, s(s(s(0)))) → mult106_out_ga(0, s(s(s(0))))
mult106_in_ga(s(T279), s(s(s(T281)))) → U4_ga(T279, T281, mult106_in_ga(T279, T281))
U4_ga(T279, T281, mult106_out_ga(T279, T281)) → mult106_out_ga(s(T279), s(s(s(T281))))
U12_gga(T234, T237, mult106_out_ga(T234, T237)) → mult12_out_gga(s(T234), s(s(s(0))), s(s(s(T237))))
mult12_in_gga(0, s(s(s(s(0)))), s(s(s(s(0))))) → mult12_out_gga(0, s(s(s(s(0)))), s(s(s(s(0)))))
mult12_in_gga(s(T318), s(s(s(s(0)))), s(s(s(s(T321))))) → U13_gga(T318, T321, mult144_in_ga(T318, T321))
mult144_in_ga(0, s(s(s(s(0))))) → mult144_out_ga(0, s(s(s(s(0)))))
mult144_in_ga(s(T374), s(s(s(s(T376))))) → U5_ga(T374, T376, mult144_in_ga(T374, T376))
U5_ga(T374, T376, mult144_out_ga(T374, T376)) → mult144_out_ga(s(T374), s(s(s(s(T376)))))
U13_gga(T318, T321, mult144_out_ga(T318, T321)) → mult12_out_gga(s(T318), s(s(s(s(0)))), s(s(s(s(T321)))))
mult12_in_gga(0, s(s(s(s(s(0))))), s(s(s(s(s(0)))))) → mult12_out_gga(0, s(s(s(s(s(0))))), s(s(s(s(s(0))))))
mult12_in_gga(s(T413), s(s(s(s(s(0))))), s(s(s(s(s(T416)))))) → U14_gga(T413, T416, mult187_in_ga(T413, T416))
mult187_in_ga(0, s(s(s(s(s(0)))))) → mult187_out_ga(0, s(s(s(s(s(0))))))
mult187_in_ga(s(T480), s(s(s(s(s(T482)))))) → U6_ga(T480, T482, mult187_in_ga(T480, T482))
U6_ga(T480, T482, mult187_out_ga(T480, T482)) → mult187_out_ga(s(T480), s(s(s(s(s(T482))))))
U14_gga(T413, T416, mult187_out_ga(T413, T416)) → mult12_out_gga(s(T413), s(s(s(s(s(0))))), s(s(s(s(s(T416))))))
mult12_in_gga(0, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(0))))))) → mult12_out_gga(0, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(0)))))))
mult12_in_gga(s(T519), s(s(s(s(s(s(0)))))), s(s(s(s(s(s(T522))))))) → U15_gga(T519, T522, mult235_in_ga(T519, T522))
mult235_in_ga(0, s(s(s(s(s(s(0))))))) → mult235_out_ga(0, s(s(s(s(s(s(0)))))))
mult235_in_ga(s(T597), s(s(s(s(s(s(T599))))))) → U7_ga(T597, T599, mult235_in_ga(T597, T599))
U7_ga(T597, T599, mult235_out_ga(T597, T599)) → mult235_out_ga(s(T597), s(s(s(s(s(s(T599)))))))
U15_gga(T519, T522, mult235_out_ga(T519, T522)) → mult12_out_gga(s(T519), s(s(s(s(s(s(0)))))), s(s(s(s(s(s(T522)))))))
mult12_in_gga(0, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(0)))))))) → mult12_out_gga(0, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(0))))))))
mult12_in_gga(s(T636), s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(T639)))))))) → U16_gga(T636, T639, mult288_in_ga(T636, T639))
mult288_in_ga(0, s(s(s(s(s(s(s(0)))))))) → mult288_out_ga(0, s(s(s(s(s(s(s(0))))))))
mult288_in_ga(s(T725), s(s(s(s(s(s(s(T727)))))))) → U8_ga(T725, T727, mult288_in_ga(T725, T727))
U8_ga(T725, T727, mult288_out_ga(T725, T727)) → mult288_out_ga(s(T725), s(s(s(s(s(s(s(T727))))))))
U16_gga(T636, T639, mult288_out_ga(T636, T639)) → mult12_out_gga(s(T636), s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(T639))))))))
mult12_in_gga(T740, s(s(s(s(s(s(s(s(T742)))))))), s(s(s(s(s(s(s(s(T744))))))))) → U17_gga(T740, T742, T744, mult338_in_ggga(T740, s(s(s(s(s(s(s(T742))))))), T742, T744))
mult338_in_ggga(0, T754, 0, 0) → mult338_out_ggga(0, T754, 0, 0)
mult338_in_ggga(s(T767), T768, 0, T770) → U18_ggga(T767, T768, T770, mult12_in_gga(T767, s(T768), T770))
U18_ggga(T767, T768, T770, mult12_out_gga(T767, s(T768), T770)) → mult338_out_ggga(s(T767), T768, 0, T770)
mult338_in_ggga(T786, T787, s(T788), s(T790)) → U19_ggga(T786, T787, T788, T790, mult338_in_ggga(T786, T787, T788, T790))
U19_ggga(T786, T787, T788, T790, mult338_out_ggga(T786, T787, T788, T790)) → mult338_out_ggga(T786, T787, s(T788), s(T790))
U17_gga(T740, T742, T744, mult338_out_ggga(T740, s(s(s(s(s(s(s(T742))))))), T742, T744)) → mult12_out_gga(T740, s(s(s(s(s(s(s(s(T742)))))))), s(s(s(s(s(s(s(s(T744)))))))))
U20_gga(T28, T29, T31, mult12_out_gga(T28, T29, T31)) → times1_out_gga(s(T28), T29, T31)
MULT144_IN_GA(s(T374), s(s(s(s(T376))))) → MULT144_IN_GA(T374, T376)
MULT144_IN_GA(s(T374)) → MULT144_IN_GA(T374)
From the DPs we obtained the following set of size-change graphs:
MULT106_IN_GA(s(T279), s(s(s(T281)))) → MULT106_IN_GA(T279, T281)
times1_in_gga(0, T15, 0) → times1_out_gga(0, T15, 0)
times1_in_gga(s(T28), T29, T31) → U20_gga(T28, T29, T31, mult12_in_gga(T28, T29, T31))
mult12_in_gga(0, 0, 0) → mult12_out_gga(0, 0, 0)
mult12_in_gga(s(T51), 0, T54) → U9_gga(T51, T54, mult22_in_ga(T51, T54))
mult22_in_ga(0, 0) → mult22_out_ga(0, 0)
mult22_in_ga(s(T63), T65) → U1_ga(T63, T65, mult22_in_ga(T63, T65))
U1_ga(T63, T65, mult22_out_ga(T63, T65)) → mult22_out_ga(s(T63), T65)
U9_gga(T51, T54, mult22_out_ga(T51, T54)) → mult12_out_gga(s(T51), 0, T54)
mult12_in_gga(0, s(0), s(0)) → mult12_out_gga(0, s(0), s(0))
mult12_in_gga(s(T99), s(0), s(T102)) → U10_gga(T99, T102, mult45_in_ga(T99, T102))
mult45_in_ga(0, s(0)) → mult45_out_ga(0, s(0))
mult45_in_ga(s(T122), s(T124)) → U2_ga(T122, T124, mult45_in_ga(T122, T124))
U2_ga(T122, T124, mult45_out_ga(T122, T124)) → mult45_out_ga(s(T122), s(T124))
U10_gga(T99, T102, mult45_out_ga(T99, T102)) → mult12_out_gga(s(T99), s(0), s(T102))
mult12_in_gga(0, s(s(0)), s(s(0))) → mult12_out_gga(0, s(s(0)), s(s(0)))
mult12_in_gga(s(T161), s(s(0)), s(s(T164))) → U11_gga(T161, T164, mult73_in_ga(T161, T164))
mult73_in_ga(0, s(s(0))) → mult73_out_ga(0, s(s(0)))
mult73_in_ga(s(T195), s(s(T197))) → U3_ga(T195, T197, mult73_in_ga(T195, T197))
U3_ga(T195, T197, mult73_out_ga(T195, T197)) → mult73_out_ga(s(T195), s(s(T197)))
U11_gga(T161, T164, mult73_out_ga(T161, T164)) → mult12_out_gga(s(T161), s(s(0)), s(s(T164)))
mult12_in_gga(0, s(s(s(0))), s(s(s(0)))) → mult12_out_gga(0, s(s(s(0))), s(s(s(0))))
mult12_in_gga(s(T234), s(s(s(0))), s(s(s(T237)))) → U12_gga(T234, T237, mult106_in_ga(T234, T237))
mult106_in_ga(0, s(s(s(0)))) → mult106_out_ga(0, s(s(s(0))))
mult106_in_ga(s(T279), s(s(s(T281)))) → U4_ga(T279, T281, mult106_in_ga(T279, T281))
U4_ga(T279, T281, mult106_out_ga(T279, T281)) → mult106_out_ga(s(T279), s(s(s(T281))))
U12_gga(T234, T237, mult106_out_ga(T234, T237)) → mult12_out_gga(s(T234), s(s(s(0))), s(s(s(T237))))
mult12_in_gga(0, s(s(s(s(0)))), s(s(s(s(0))))) → mult12_out_gga(0, s(s(s(s(0)))), s(s(s(s(0)))))
mult12_in_gga(s(T318), s(s(s(s(0)))), s(s(s(s(T321))))) → U13_gga(T318, T321, mult144_in_ga(T318, T321))
mult144_in_ga(0, s(s(s(s(0))))) → mult144_out_ga(0, s(s(s(s(0)))))
mult144_in_ga(s(T374), s(s(s(s(T376))))) → U5_ga(T374, T376, mult144_in_ga(T374, T376))
U5_ga(T374, T376, mult144_out_ga(T374, T376)) → mult144_out_ga(s(T374), s(s(s(s(T376)))))
U13_gga(T318, T321, mult144_out_ga(T318, T321)) → mult12_out_gga(s(T318), s(s(s(s(0)))), s(s(s(s(T321)))))
mult12_in_gga(0, s(s(s(s(s(0))))), s(s(s(s(s(0)))))) → mult12_out_gga(0, s(s(s(s(s(0))))), s(s(s(s(s(0))))))
mult12_in_gga(s(T413), s(s(s(s(s(0))))), s(s(s(s(s(T416)))))) → U14_gga(T413, T416, mult187_in_ga(T413, T416))
mult187_in_ga(0, s(s(s(s(s(0)))))) → mult187_out_ga(0, s(s(s(s(s(0))))))
mult187_in_ga(s(T480), s(s(s(s(s(T482)))))) → U6_ga(T480, T482, mult187_in_ga(T480, T482))
U6_ga(T480, T482, mult187_out_ga(T480, T482)) → mult187_out_ga(s(T480), s(s(s(s(s(T482))))))
U14_gga(T413, T416, mult187_out_ga(T413, T416)) → mult12_out_gga(s(T413), s(s(s(s(s(0))))), s(s(s(s(s(T416))))))
mult12_in_gga(0, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(0))))))) → mult12_out_gga(0, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(0)))))))
mult12_in_gga(s(T519), s(s(s(s(s(s(0)))))), s(s(s(s(s(s(T522))))))) → U15_gga(T519, T522, mult235_in_ga(T519, T522))
mult235_in_ga(0, s(s(s(s(s(s(0))))))) → mult235_out_ga(0, s(s(s(s(s(s(0)))))))
mult235_in_ga(s(T597), s(s(s(s(s(s(T599))))))) → U7_ga(T597, T599, mult235_in_ga(T597, T599))
U7_ga(T597, T599, mult235_out_ga(T597, T599)) → mult235_out_ga(s(T597), s(s(s(s(s(s(T599)))))))
U15_gga(T519, T522, mult235_out_ga(T519, T522)) → mult12_out_gga(s(T519), s(s(s(s(s(s(0)))))), s(s(s(s(s(s(T522)))))))
mult12_in_gga(0, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(0)))))))) → mult12_out_gga(0, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(0))))))))
mult12_in_gga(s(T636), s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(T639)))))))) → U16_gga(T636, T639, mult288_in_ga(T636, T639))
mult288_in_ga(0, s(s(s(s(s(s(s(0)))))))) → mult288_out_ga(0, s(s(s(s(s(s(s(0))))))))
mult288_in_ga(s(T725), s(s(s(s(s(s(s(T727)))))))) → U8_ga(T725, T727, mult288_in_ga(T725, T727))
U8_ga(T725, T727, mult288_out_ga(T725, T727)) → mult288_out_ga(s(T725), s(s(s(s(s(s(s(T727))))))))
U16_gga(T636, T639, mult288_out_ga(T636, T639)) → mult12_out_gga(s(T636), s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(T639))))))))
mult12_in_gga(T740, s(s(s(s(s(s(s(s(T742)))))))), s(s(s(s(s(s(s(s(T744))))))))) → U17_gga(T740, T742, T744, mult338_in_ggga(T740, s(s(s(s(s(s(s(T742))))))), T742, T744))
mult338_in_ggga(0, T754, 0, 0) → mult338_out_ggga(0, T754, 0, 0)
mult338_in_ggga(s(T767), T768, 0, T770) → U18_ggga(T767, T768, T770, mult12_in_gga(T767, s(T768), T770))
U18_ggga(T767, T768, T770, mult12_out_gga(T767, s(T768), T770)) → mult338_out_ggga(s(T767), T768, 0, T770)
mult338_in_ggga(T786, T787, s(T788), s(T790)) → U19_ggga(T786, T787, T788, T790, mult338_in_ggga(T786, T787, T788, T790))
U19_ggga(T786, T787, T788, T790, mult338_out_ggga(T786, T787, T788, T790)) → mult338_out_ggga(T786, T787, s(T788), s(T790))
U17_gga(T740, T742, T744, mult338_out_ggga(T740, s(s(s(s(s(s(s(T742))))))), T742, T744)) → mult12_out_gga(T740, s(s(s(s(s(s(s(s(T742)))))))), s(s(s(s(s(s(s(s(T744)))))))))
U20_gga(T28, T29, T31, mult12_out_gga(T28, T29, T31)) → times1_out_gga(s(T28), T29, T31)
MULT106_IN_GA(s(T279), s(s(s(T281)))) → MULT106_IN_GA(T279, T281)
MULT106_IN_GA(s(T279)) → MULT106_IN_GA(T279)
From the DPs we obtained the following set of size-change graphs:
MULT73_IN_GA(s(T195), s(s(T197))) → MULT73_IN_GA(T195, T197)
times1_in_gga(0, T15, 0) → times1_out_gga(0, T15, 0)
times1_in_gga(s(T28), T29, T31) → U20_gga(T28, T29, T31, mult12_in_gga(T28, T29, T31))
mult12_in_gga(0, 0, 0) → mult12_out_gga(0, 0, 0)
mult12_in_gga(s(T51), 0, T54) → U9_gga(T51, T54, mult22_in_ga(T51, T54))
mult22_in_ga(0, 0) → mult22_out_ga(0, 0)
mult22_in_ga(s(T63), T65) → U1_ga(T63, T65, mult22_in_ga(T63, T65))
U1_ga(T63, T65, mult22_out_ga(T63, T65)) → mult22_out_ga(s(T63), T65)
U9_gga(T51, T54, mult22_out_ga(T51, T54)) → mult12_out_gga(s(T51), 0, T54)
mult12_in_gga(0, s(0), s(0)) → mult12_out_gga(0, s(0), s(0))
mult12_in_gga(s(T99), s(0), s(T102)) → U10_gga(T99, T102, mult45_in_ga(T99, T102))
mult45_in_ga(0, s(0)) → mult45_out_ga(0, s(0))
mult45_in_ga(s(T122), s(T124)) → U2_ga(T122, T124, mult45_in_ga(T122, T124))
U2_ga(T122, T124, mult45_out_ga(T122, T124)) → mult45_out_ga(s(T122), s(T124))
U10_gga(T99, T102, mult45_out_ga(T99, T102)) → mult12_out_gga(s(T99), s(0), s(T102))
mult12_in_gga(0, s(s(0)), s(s(0))) → mult12_out_gga(0, s(s(0)), s(s(0)))
mult12_in_gga(s(T161), s(s(0)), s(s(T164))) → U11_gga(T161, T164, mult73_in_ga(T161, T164))
mult73_in_ga(0, s(s(0))) → mult73_out_ga(0, s(s(0)))
mult73_in_ga(s(T195), s(s(T197))) → U3_ga(T195, T197, mult73_in_ga(T195, T197))
U3_ga(T195, T197, mult73_out_ga(T195, T197)) → mult73_out_ga(s(T195), s(s(T197)))
U11_gga(T161, T164, mult73_out_ga(T161, T164)) → mult12_out_gga(s(T161), s(s(0)), s(s(T164)))
mult12_in_gga(0, s(s(s(0))), s(s(s(0)))) → mult12_out_gga(0, s(s(s(0))), s(s(s(0))))
mult12_in_gga(s(T234), s(s(s(0))), s(s(s(T237)))) → U12_gga(T234, T237, mult106_in_ga(T234, T237))
mult106_in_ga(0, s(s(s(0)))) → mult106_out_ga(0, s(s(s(0))))
mult106_in_ga(s(T279), s(s(s(T281)))) → U4_ga(T279, T281, mult106_in_ga(T279, T281))
U4_ga(T279, T281, mult106_out_ga(T279, T281)) → mult106_out_ga(s(T279), s(s(s(T281))))
U12_gga(T234, T237, mult106_out_ga(T234, T237)) → mult12_out_gga(s(T234), s(s(s(0))), s(s(s(T237))))
mult12_in_gga(0, s(s(s(s(0)))), s(s(s(s(0))))) → mult12_out_gga(0, s(s(s(s(0)))), s(s(s(s(0)))))
mult12_in_gga(s(T318), s(s(s(s(0)))), s(s(s(s(T321))))) → U13_gga(T318, T321, mult144_in_ga(T318, T321))
mult144_in_ga(0, s(s(s(s(0))))) → mult144_out_ga(0, s(s(s(s(0)))))
mult144_in_ga(s(T374), s(s(s(s(T376))))) → U5_ga(T374, T376, mult144_in_ga(T374, T376))
U5_ga(T374, T376, mult144_out_ga(T374, T376)) → mult144_out_ga(s(T374), s(s(s(s(T376)))))
U13_gga(T318, T321, mult144_out_ga(T318, T321)) → mult12_out_gga(s(T318), s(s(s(s(0)))), s(s(s(s(T321)))))
mult12_in_gga(0, s(s(s(s(s(0))))), s(s(s(s(s(0)))))) → mult12_out_gga(0, s(s(s(s(s(0))))), s(s(s(s(s(0))))))
mult12_in_gga(s(T413), s(s(s(s(s(0))))), s(s(s(s(s(T416)))))) → U14_gga(T413, T416, mult187_in_ga(T413, T416))
mult187_in_ga(0, s(s(s(s(s(0)))))) → mult187_out_ga(0, s(s(s(s(s(0))))))
mult187_in_ga(s(T480), s(s(s(s(s(T482)))))) → U6_ga(T480, T482, mult187_in_ga(T480, T482))
U6_ga(T480, T482, mult187_out_ga(T480, T482)) → mult187_out_ga(s(T480), s(s(s(s(s(T482))))))
U14_gga(T413, T416, mult187_out_ga(T413, T416)) → mult12_out_gga(s(T413), s(s(s(s(s(0))))), s(s(s(s(s(T416))))))
mult12_in_gga(0, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(0))))))) → mult12_out_gga(0, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(0)))))))
mult12_in_gga(s(T519), s(s(s(s(s(s(0)))))), s(s(s(s(s(s(T522))))))) → U15_gga(T519, T522, mult235_in_ga(T519, T522))
mult235_in_ga(0, s(s(s(s(s(s(0))))))) → mult235_out_ga(0, s(s(s(s(s(s(0)))))))
mult235_in_ga(s(T597), s(s(s(s(s(s(T599))))))) → U7_ga(T597, T599, mult235_in_ga(T597, T599))
U7_ga(T597, T599, mult235_out_ga(T597, T599)) → mult235_out_ga(s(T597), s(s(s(s(s(s(T599)))))))
U15_gga(T519, T522, mult235_out_ga(T519, T522)) → mult12_out_gga(s(T519), s(s(s(s(s(s(0)))))), s(s(s(s(s(s(T522)))))))
mult12_in_gga(0, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(0)))))))) → mult12_out_gga(0, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(0))))))))
mult12_in_gga(s(T636), s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(T639)))))))) → U16_gga(T636, T639, mult288_in_ga(T636, T639))
mult288_in_ga(0, s(s(s(s(s(s(s(0)))))))) → mult288_out_ga(0, s(s(s(s(s(s(s(0))))))))
mult288_in_ga(s(T725), s(s(s(s(s(s(s(T727)))))))) → U8_ga(T725, T727, mult288_in_ga(T725, T727))
U8_ga(T725, T727, mult288_out_ga(T725, T727)) → mult288_out_ga(s(T725), s(s(s(s(s(s(s(T727))))))))
U16_gga(T636, T639, mult288_out_ga(T636, T639)) → mult12_out_gga(s(T636), s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(T639))))))))
mult12_in_gga(T740, s(s(s(s(s(s(s(s(T742)))))))), s(s(s(s(s(s(s(s(T744))))))))) → U17_gga(T740, T742, T744, mult338_in_ggga(T740, s(s(s(s(s(s(s(T742))))))), T742, T744))
mult338_in_ggga(0, T754, 0, 0) → mult338_out_ggga(0, T754, 0, 0)
mult338_in_ggga(s(T767), T768, 0, T770) → U18_ggga(T767, T768, T770, mult12_in_gga(T767, s(T768), T770))
U18_ggga(T767, T768, T770, mult12_out_gga(T767, s(T768), T770)) → mult338_out_ggga(s(T767), T768, 0, T770)
mult338_in_ggga(T786, T787, s(T788), s(T790)) → U19_ggga(T786, T787, T788, T790, mult338_in_ggga(T786, T787, T788, T790))
U19_ggga(T786, T787, T788, T790, mult338_out_ggga(T786, T787, T788, T790)) → mult338_out_ggga(T786, T787, s(T788), s(T790))
U17_gga(T740, T742, T744, mult338_out_ggga(T740, s(s(s(s(s(s(s(T742))))))), T742, T744)) → mult12_out_gga(T740, s(s(s(s(s(s(s(s(T742)))))))), s(s(s(s(s(s(s(s(T744)))))))))
U20_gga(T28, T29, T31, mult12_out_gga(T28, T29, T31)) → times1_out_gga(s(T28), T29, T31)
MULT73_IN_GA(s(T195), s(s(T197))) → MULT73_IN_GA(T195, T197)
MULT73_IN_GA(s(T195)) → MULT73_IN_GA(T195)
From the DPs we obtained the following set of size-change graphs:
MULT45_IN_GA(s(T122), s(T124)) → MULT45_IN_GA(T122, T124)
times1_in_gga(0, T15, 0) → times1_out_gga(0, T15, 0)
times1_in_gga(s(T28), T29, T31) → U20_gga(T28, T29, T31, mult12_in_gga(T28, T29, T31))
mult12_in_gga(0, 0, 0) → mult12_out_gga(0, 0, 0)
mult12_in_gga(s(T51), 0, T54) → U9_gga(T51, T54, mult22_in_ga(T51, T54))
mult22_in_ga(0, 0) → mult22_out_ga(0, 0)
mult22_in_ga(s(T63), T65) → U1_ga(T63, T65, mult22_in_ga(T63, T65))
U1_ga(T63, T65, mult22_out_ga(T63, T65)) → mult22_out_ga(s(T63), T65)
U9_gga(T51, T54, mult22_out_ga(T51, T54)) → mult12_out_gga(s(T51), 0, T54)
mult12_in_gga(0, s(0), s(0)) → mult12_out_gga(0, s(0), s(0))
mult12_in_gga(s(T99), s(0), s(T102)) → U10_gga(T99, T102, mult45_in_ga(T99, T102))
mult45_in_ga(0, s(0)) → mult45_out_ga(0, s(0))
mult45_in_ga(s(T122), s(T124)) → U2_ga(T122, T124, mult45_in_ga(T122, T124))
U2_ga(T122, T124, mult45_out_ga(T122, T124)) → mult45_out_ga(s(T122), s(T124))
U10_gga(T99, T102, mult45_out_ga(T99, T102)) → mult12_out_gga(s(T99), s(0), s(T102))
mult12_in_gga(0, s(s(0)), s(s(0))) → mult12_out_gga(0, s(s(0)), s(s(0)))
mult12_in_gga(s(T161), s(s(0)), s(s(T164))) → U11_gga(T161, T164, mult73_in_ga(T161, T164))
mult73_in_ga(0, s(s(0))) → mult73_out_ga(0, s(s(0)))
mult73_in_ga(s(T195), s(s(T197))) → U3_ga(T195, T197, mult73_in_ga(T195, T197))
U3_ga(T195, T197, mult73_out_ga(T195, T197)) → mult73_out_ga(s(T195), s(s(T197)))
U11_gga(T161, T164, mult73_out_ga(T161, T164)) → mult12_out_gga(s(T161), s(s(0)), s(s(T164)))
mult12_in_gga(0, s(s(s(0))), s(s(s(0)))) → mult12_out_gga(0, s(s(s(0))), s(s(s(0))))
mult12_in_gga(s(T234), s(s(s(0))), s(s(s(T237)))) → U12_gga(T234, T237, mult106_in_ga(T234, T237))
mult106_in_ga(0, s(s(s(0)))) → mult106_out_ga(0, s(s(s(0))))
mult106_in_ga(s(T279), s(s(s(T281)))) → U4_ga(T279, T281, mult106_in_ga(T279, T281))
U4_ga(T279, T281, mult106_out_ga(T279, T281)) → mult106_out_ga(s(T279), s(s(s(T281))))
U12_gga(T234, T237, mult106_out_ga(T234, T237)) → mult12_out_gga(s(T234), s(s(s(0))), s(s(s(T237))))
mult12_in_gga(0, s(s(s(s(0)))), s(s(s(s(0))))) → mult12_out_gga(0, s(s(s(s(0)))), s(s(s(s(0)))))
mult12_in_gga(s(T318), s(s(s(s(0)))), s(s(s(s(T321))))) → U13_gga(T318, T321, mult144_in_ga(T318, T321))
mult144_in_ga(0, s(s(s(s(0))))) → mult144_out_ga(0, s(s(s(s(0)))))
mult144_in_ga(s(T374), s(s(s(s(T376))))) → U5_ga(T374, T376, mult144_in_ga(T374, T376))
U5_ga(T374, T376, mult144_out_ga(T374, T376)) → mult144_out_ga(s(T374), s(s(s(s(T376)))))
U13_gga(T318, T321, mult144_out_ga(T318, T321)) → mult12_out_gga(s(T318), s(s(s(s(0)))), s(s(s(s(T321)))))
mult12_in_gga(0, s(s(s(s(s(0))))), s(s(s(s(s(0)))))) → mult12_out_gga(0, s(s(s(s(s(0))))), s(s(s(s(s(0))))))
mult12_in_gga(s(T413), s(s(s(s(s(0))))), s(s(s(s(s(T416)))))) → U14_gga(T413, T416, mult187_in_ga(T413, T416))
mult187_in_ga(0, s(s(s(s(s(0)))))) → mult187_out_ga(0, s(s(s(s(s(0))))))
mult187_in_ga(s(T480), s(s(s(s(s(T482)))))) → U6_ga(T480, T482, mult187_in_ga(T480, T482))
U6_ga(T480, T482, mult187_out_ga(T480, T482)) → mult187_out_ga(s(T480), s(s(s(s(s(T482))))))
U14_gga(T413, T416, mult187_out_ga(T413, T416)) → mult12_out_gga(s(T413), s(s(s(s(s(0))))), s(s(s(s(s(T416))))))
mult12_in_gga(0, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(0))))))) → mult12_out_gga(0, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(0)))))))
mult12_in_gga(s(T519), s(s(s(s(s(s(0)))))), s(s(s(s(s(s(T522))))))) → U15_gga(T519, T522, mult235_in_ga(T519, T522))
mult235_in_ga(0, s(s(s(s(s(s(0))))))) → mult235_out_ga(0, s(s(s(s(s(s(0)))))))
mult235_in_ga(s(T597), s(s(s(s(s(s(T599))))))) → U7_ga(T597, T599, mult235_in_ga(T597, T599))
U7_ga(T597, T599, mult235_out_ga(T597, T599)) → mult235_out_ga(s(T597), s(s(s(s(s(s(T599)))))))
U15_gga(T519, T522, mult235_out_ga(T519, T522)) → mult12_out_gga(s(T519), s(s(s(s(s(s(0)))))), s(s(s(s(s(s(T522)))))))
mult12_in_gga(0, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(0)))))))) → mult12_out_gga(0, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(0))))))))
mult12_in_gga(s(T636), s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(T639)))))))) → U16_gga(T636, T639, mult288_in_ga(T636, T639))
mult288_in_ga(0, s(s(s(s(s(s(s(0)))))))) → mult288_out_ga(0, s(s(s(s(s(s(s(0))))))))
mult288_in_ga(s(T725), s(s(s(s(s(s(s(T727)))))))) → U8_ga(T725, T727, mult288_in_ga(T725, T727))
U8_ga(T725, T727, mult288_out_ga(T725, T727)) → mult288_out_ga(s(T725), s(s(s(s(s(s(s(T727))))))))
U16_gga(T636, T639, mult288_out_ga(T636, T639)) → mult12_out_gga(s(T636), s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(T639))))))))
mult12_in_gga(T740, s(s(s(s(s(s(s(s(T742)))))))), s(s(s(s(s(s(s(s(T744))))))))) → U17_gga(T740, T742, T744, mult338_in_ggga(T740, s(s(s(s(s(s(s(T742))))))), T742, T744))
mult338_in_ggga(0, T754, 0, 0) → mult338_out_ggga(0, T754, 0, 0)
mult338_in_ggga(s(T767), T768, 0, T770) → U18_ggga(T767, T768, T770, mult12_in_gga(T767, s(T768), T770))
U18_ggga(T767, T768, T770, mult12_out_gga(T767, s(T768), T770)) → mult338_out_ggga(s(T767), T768, 0, T770)
mult338_in_ggga(T786, T787, s(T788), s(T790)) → U19_ggga(T786, T787, T788, T790, mult338_in_ggga(T786, T787, T788, T790))
U19_ggga(T786, T787, T788, T790, mult338_out_ggga(T786, T787, T788, T790)) → mult338_out_ggga(T786, T787, s(T788), s(T790))
U17_gga(T740, T742, T744, mult338_out_ggga(T740, s(s(s(s(s(s(s(T742))))))), T742, T744)) → mult12_out_gga(T740, s(s(s(s(s(s(s(s(T742)))))))), s(s(s(s(s(s(s(s(T744)))))))))
U20_gga(T28, T29, T31, mult12_out_gga(T28, T29, T31)) → times1_out_gga(s(T28), T29, T31)
MULT45_IN_GA(s(T122), s(T124)) → MULT45_IN_GA(T122, T124)
MULT45_IN_GA(s(T122)) → MULT45_IN_GA(T122)
From the DPs we obtained the following set of size-change graphs:
MULT12_IN_GGA(T740, s(s(s(s(s(s(s(s(T742)))))))), s(s(s(s(s(s(s(s(T744))))))))) → MULT338_IN_GGGA(T740, s(s(s(s(s(s(s(T742))))))), T742, T744)
MULT338_IN_GGGA(s(T767), T768, 0, T770) → MULT12_IN_GGA(T767, s(T768), T770)
MULT338_IN_GGGA(T786, T787, s(T788), s(T790)) → MULT338_IN_GGGA(T786, T787, T788, T790)
times1_in_gga(0, T15, 0) → times1_out_gga(0, T15, 0)
times1_in_gga(s(T28), T29, T31) → U20_gga(T28, T29, T31, mult12_in_gga(T28, T29, T31))
mult12_in_gga(0, 0, 0) → mult12_out_gga(0, 0, 0)
mult12_in_gga(s(T51), 0, T54) → U9_gga(T51, T54, mult22_in_ga(T51, T54))
mult22_in_ga(0, 0) → mult22_out_ga(0, 0)
mult22_in_ga(s(T63), T65) → U1_ga(T63, T65, mult22_in_ga(T63, T65))
U1_ga(T63, T65, mult22_out_ga(T63, T65)) → mult22_out_ga(s(T63), T65)
U9_gga(T51, T54, mult22_out_ga(T51, T54)) → mult12_out_gga(s(T51), 0, T54)
mult12_in_gga(0, s(0), s(0)) → mult12_out_gga(0, s(0), s(0))
mult12_in_gga(s(T99), s(0), s(T102)) → U10_gga(T99, T102, mult45_in_ga(T99, T102))
mult45_in_ga(0, s(0)) → mult45_out_ga(0, s(0))
mult45_in_ga(s(T122), s(T124)) → U2_ga(T122, T124, mult45_in_ga(T122, T124))
U2_ga(T122, T124, mult45_out_ga(T122, T124)) → mult45_out_ga(s(T122), s(T124))
U10_gga(T99, T102, mult45_out_ga(T99, T102)) → mult12_out_gga(s(T99), s(0), s(T102))
mult12_in_gga(0, s(s(0)), s(s(0))) → mult12_out_gga(0, s(s(0)), s(s(0)))
mult12_in_gga(s(T161), s(s(0)), s(s(T164))) → U11_gga(T161, T164, mult73_in_ga(T161, T164))
mult73_in_ga(0, s(s(0))) → mult73_out_ga(0, s(s(0)))
mult73_in_ga(s(T195), s(s(T197))) → U3_ga(T195, T197, mult73_in_ga(T195, T197))
U3_ga(T195, T197, mult73_out_ga(T195, T197)) → mult73_out_ga(s(T195), s(s(T197)))
U11_gga(T161, T164, mult73_out_ga(T161, T164)) → mult12_out_gga(s(T161), s(s(0)), s(s(T164)))
mult12_in_gga(0, s(s(s(0))), s(s(s(0)))) → mult12_out_gga(0, s(s(s(0))), s(s(s(0))))
mult12_in_gga(s(T234), s(s(s(0))), s(s(s(T237)))) → U12_gga(T234, T237, mult106_in_ga(T234, T237))
mult106_in_ga(0, s(s(s(0)))) → mult106_out_ga(0, s(s(s(0))))
mult106_in_ga(s(T279), s(s(s(T281)))) → U4_ga(T279, T281, mult106_in_ga(T279, T281))
U4_ga(T279, T281, mult106_out_ga(T279, T281)) → mult106_out_ga(s(T279), s(s(s(T281))))
U12_gga(T234, T237, mult106_out_ga(T234, T237)) → mult12_out_gga(s(T234), s(s(s(0))), s(s(s(T237))))
mult12_in_gga(0, s(s(s(s(0)))), s(s(s(s(0))))) → mult12_out_gga(0, s(s(s(s(0)))), s(s(s(s(0)))))
mult12_in_gga(s(T318), s(s(s(s(0)))), s(s(s(s(T321))))) → U13_gga(T318, T321, mult144_in_ga(T318, T321))
mult144_in_ga(0, s(s(s(s(0))))) → mult144_out_ga(0, s(s(s(s(0)))))
mult144_in_ga(s(T374), s(s(s(s(T376))))) → U5_ga(T374, T376, mult144_in_ga(T374, T376))
U5_ga(T374, T376, mult144_out_ga(T374, T376)) → mult144_out_ga(s(T374), s(s(s(s(T376)))))
U13_gga(T318, T321, mult144_out_ga(T318, T321)) → mult12_out_gga(s(T318), s(s(s(s(0)))), s(s(s(s(T321)))))
mult12_in_gga(0, s(s(s(s(s(0))))), s(s(s(s(s(0)))))) → mult12_out_gga(0, s(s(s(s(s(0))))), s(s(s(s(s(0))))))
mult12_in_gga(s(T413), s(s(s(s(s(0))))), s(s(s(s(s(T416)))))) → U14_gga(T413, T416, mult187_in_ga(T413, T416))
mult187_in_ga(0, s(s(s(s(s(0)))))) → mult187_out_ga(0, s(s(s(s(s(0))))))
mult187_in_ga(s(T480), s(s(s(s(s(T482)))))) → U6_ga(T480, T482, mult187_in_ga(T480, T482))
U6_ga(T480, T482, mult187_out_ga(T480, T482)) → mult187_out_ga(s(T480), s(s(s(s(s(T482))))))
U14_gga(T413, T416, mult187_out_ga(T413, T416)) → mult12_out_gga(s(T413), s(s(s(s(s(0))))), s(s(s(s(s(T416))))))
mult12_in_gga(0, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(0))))))) → mult12_out_gga(0, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(0)))))))
mult12_in_gga(s(T519), s(s(s(s(s(s(0)))))), s(s(s(s(s(s(T522))))))) → U15_gga(T519, T522, mult235_in_ga(T519, T522))
mult235_in_ga(0, s(s(s(s(s(s(0))))))) → mult235_out_ga(0, s(s(s(s(s(s(0)))))))
mult235_in_ga(s(T597), s(s(s(s(s(s(T599))))))) → U7_ga(T597, T599, mult235_in_ga(T597, T599))
U7_ga(T597, T599, mult235_out_ga(T597, T599)) → mult235_out_ga(s(T597), s(s(s(s(s(s(T599)))))))
U15_gga(T519, T522, mult235_out_ga(T519, T522)) → mult12_out_gga(s(T519), s(s(s(s(s(s(0)))))), s(s(s(s(s(s(T522)))))))
mult12_in_gga(0, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(0)))))))) → mult12_out_gga(0, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(0))))))))
mult12_in_gga(s(T636), s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(T639)))))))) → U16_gga(T636, T639, mult288_in_ga(T636, T639))
mult288_in_ga(0, s(s(s(s(s(s(s(0)))))))) → mult288_out_ga(0, s(s(s(s(s(s(s(0))))))))
mult288_in_ga(s(T725), s(s(s(s(s(s(s(T727)))))))) → U8_ga(T725, T727, mult288_in_ga(T725, T727))
U8_ga(T725, T727, mult288_out_ga(T725, T727)) → mult288_out_ga(s(T725), s(s(s(s(s(s(s(T727))))))))
U16_gga(T636, T639, mult288_out_ga(T636, T639)) → mult12_out_gga(s(T636), s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(T639))))))))
mult12_in_gga(T740, s(s(s(s(s(s(s(s(T742)))))))), s(s(s(s(s(s(s(s(T744))))))))) → U17_gga(T740, T742, T744, mult338_in_ggga(T740, s(s(s(s(s(s(s(T742))))))), T742, T744))
mult338_in_ggga(0, T754, 0, 0) → mult338_out_ggga(0, T754, 0, 0)
mult338_in_ggga(s(T767), T768, 0, T770) → U18_ggga(T767, T768, T770, mult12_in_gga(T767, s(T768), T770))
U18_ggga(T767, T768, T770, mult12_out_gga(T767, s(T768), T770)) → mult338_out_ggga(s(T767), T768, 0, T770)
mult338_in_ggga(T786, T787, s(T788), s(T790)) → U19_ggga(T786, T787, T788, T790, mult338_in_ggga(T786, T787, T788, T790))
U19_ggga(T786, T787, T788, T790, mult338_out_ggga(T786, T787, T788, T790)) → mult338_out_ggga(T786, T787, s(T788), s(T790))
U17_gga(T740, T742, T744, mult338_out_ggga(T740, s(s(s(s(s(s(s(T742))))))), T742, T744)) → mult12_out_gga(T740, s(s(s(s(s(s(s(s(T742)))))))), s(s(s(s(s(s(s(s(T744)))))))))
U20_gga(T28, T29, T31, mult12_out_gga(T28, T29, T31)) → times1_out_gga(s(T28), T29, T31)
MULT12_IN_GGA(T740, s(s(s(s(s(s(s(s(T742)))))))), s(s(s(s(s(s(s(s(T744))))))))) → MULT338_IN_GGGA(T740, s(s(s(s(s(s(s(T742))))))), T742, T744)
MULT338_IN_GGGA(s(T767), T768, 0, T770) → MULT12_IN_GGA(T767, s(T768), T770)
MULT338_IN_GGGA(T786, T787, s(T788), s(T790)) → MULT338_IN_GGGA(T786, T787, T788, T790)
MULT12_IN_GGA(T740, s(s(s(s(s(s(s(s(T742))))))))) → MULT338_IN_GGGA(T740, s(s(s(s(s(s(s(T742))))))), T742)
MULT338_IN_GGGA(s(T767), T768, 0) → MULT12_IN_GGA(T767, s(T768))
MULT338_IN_GGGA(T786, T787, s(T788)) → MULT338_IN_GGGA(T786, T787, T788)
From the DPs we obtained the following set of size-change graphs:
MULT22_IN_GA(s(T63), T65) → MULT22_IN_GA(T63, T65)
times1_in_gga(0, T15, 0) → times1_out_gga(0, T15, 0)
times1_in_gga(s(T28), T29, T31) → U20_gga(T28, T29, T31, mult12_in_gga(T28, T29, T31))
mult12_in_gga(0, 0, 0) → mult12_out_gga(0, 0, 0)
mult12_in_gga(s(T51), 0, T54) → U9_gga(T51, T54, mult22_in_ga(T51, T54))
mult22_in_ga(0, 0) → mult22_out_ga(0, 0)
mult22_in_ga(s(T63), T65) → U1_ga(T63, T65, mult22_in_ga(T63, T65))
U1_ga(T63, T65, mult22_out_ga(T63, T65)) → mult22_out_ga(s(T63), T65)
U9_gga(T51, T54, mult22_out_ga(T51, T54)) → mult12_out_gga(s(T51), 0, T54)
mult12_in_gga(0, s(0), s(0)) → mult12_out_gga(0, s(0), s(0))
mult12_in_gga(s(T99), s(0), s(T102)) → U10_gga(T99, T102, mult45_in_ga(T99, T102))
mult45_in_ga(0, s(0)) → mult45_out_ga(0, s(0))
mult45_in_ga(s(T122), s(T124)) → U2_ga(T122, T124, mult45_in_ga(T122, T124))
U2_ga(T122, T124, mult45_out_ga(T122, T124)) → mult45_out_ga(s(T122), s(T124))
U10_gga(T99, T102, mult45_out_ga(T99, T102)) → mult12_out_gga(s(T99), s(0), s(T102))
mult12_in_gga(0, s(s(0)), s(s(0))) → mult12_out_gga(0, s(s(0)), s(s(0)))
mult12_in_gga(s(T161), s(s(0)), s(s(T164))) → U11_gga(T161, T164, mult73_in_ga(T161, T164))
mult73_in_ga(0, s(s(0))) → mult73_out_ga(0, s(s(0)))
mult73_in_ga(s(T195), s(s(T197))) → U3_ga(T195, T197, mult73_in_ga(T195, T197))
U3_ga(T195, T197, mult73_out_ga(T195, T197)) → mult73_out_ga(s(T195), s(s(T197)))
U11_gga(T161, T164, mult73_out_ga(T161, T164)) → mult12_out_gga(s(T161), s(s(0)), s(s(T164)))
mult12_in_gga(0, s(s(s(0))), s(s(s(0)))) → mult12_out_gga(0, s(s(s(0))), s(s(s(0))))
mult12_in_gga(s(T234), s(s(s(0))), s(s(s(T237)))) → U12_gga(T234, T237, mult106_in_ga(T234, T237))
mult106_in_ga(0, s(s(s(0)))) → mult106_out_ga(0, s(s(s(0))))
mult106_in_ga(s(T279), s(s(s(T281)))) → U4_ga(T279, T281, mult106_in_ga(T279, T281))
U4_ga(T279, T281, mult106_out_ga(T279, T281)) → mult106_out_ga(s(T279), s(s(s(T281))))
U12_gga(T234, T237, mult106_out_ga(T234, T237)) → mult12_out_gga(s(T234), s(s(s(0))), s(s(s(T237))))
mult12_in_gga(0, s(s(s(s(0)))), s(s(s(s(0))))) → mult12_out_gga(0, s(s(s(s(0)))), s(s(s(s(0)))))
mult12_in_gga(s(T318), s(s(s(s(0)))), s(s(s(s(T321))))) → U13_gga(T318, T321, mult144_in_ga(T318, T321))
mult144_in_ga(0, s(s(s(s(0))))) → mult144_out_ga(0, s(s(s(s(0)))))
mult144_in_ga(s(T374), s(s(s(s(T376))))) → U5_ga(T374, T376, mult144_in_ga(T374, T376))
U5_ga(T374, T376, mult144_out_ga(T374, T376)) → mult144_out_ga(s(T374), s(s(s(s(T376)))))
U13_gga(T318, T321, mult144_out_ga(T318, T321)) → mult12_out_gga(s(T318), s(s(s(s(0)))), s(s(s(s(T321)))))
mult12_in_gga(0, s(s(s(s(s(0))))), s(s(s(s(s(0)))))) → mult12_out_gga(0, s(s(s(s(s(0))))), s(s(s(s(s(0))))))
mult12_in_gga(s(T413), s(s(s(s(s(0))))), s(s(s(s(s(T416)))))) → U14_gga(T413, T416, mult187_in_ga(T413, T416))
mult187_in_ga(0, s(s(s(s(s(0)))))) → mult187_out_ga(0, s(s(s(s(s(0))))))
mult187_in_ga(s(T480), s(s(s(s(s(T482)))))) → U6_ga(T480, T482, mult187_in_ga(T480, T482))
U6_ga(T480, T482, mult187_out_ga(T480, T482)) → mult187_out_ga(s(T480), s(s(s(s(s(T482))))))
U14_gga(T413, T416, mult187_out_ga(T413, T416)) → mult12_out_gga(s(T413), s(s(s(s(s(0))))), s(s(s(s(s(T416))))))
mult12_in_gga(0, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(0))))))) → mult12_out_gga(0, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(0)))))))
mult12_in_gga(s(T519), s(s(s(s(s(s(0)))))), s(s(s(s(s(s(T522))))))) → U15_gga(T519, T522, mult235_in_ga(T519, T522))
mult235_in_ga(0, s(s(s(s(s(s(0))))))) → mult235_out_ga(0, s(s(s(s(s(s(0)))))))
mult235_in_ga(s(T597), s(s(s(s(s(s(T599))))))) → U7_ga(T597, T599, mult235_in_ga(T597, T599))
U7_ga(T597, T599, mult235_out_ga(T597, T599)) → mult235_out_ga(s(T597), s(s(s(s(s(s(T599)))))))
U15_gga(T519, T522, mult235_out_ga(T519, T522)) → mult12_out_gga(s(T519), s(s(s(s(s(s(0)))))), s(s(s(s(s(s(T522)))))))
mult12_in_gga(0, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(0)))))))) → mult12_out_gga(0, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(0))))))))
mult12_in_gga(s(T636), s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(T639)))))))) → U16_gga(T636, T639, mult288_in_ga(T636, T639))
mult288_in_ga(0, s(s(s(s(s(s(s(0)))))))) → mult288_out_ga(0, s(s(s(s(s(s(s(0))))))))
mult288_in_ga(s(T725), s(s(s(s(s(s(s(T727)))))))) → U8_ga(T725, T727, mult288_in_ga(T725, T727))
U8_ga(T725, T727, mult288_out_ga(T725, T727)) → mult288_out_ga(s(T725), s(s(s(s(s(s(s(T727))))))))
U16_gga(T636, T639, mult288_out_ga(T636, T639)) → mult12_out_gga(s(T636), s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(T639))))))))
mult12_in_gga(T740, s(s(s(s(s(s(s(s(T742)))))))), s(s(s(s(s(s(s(s(T744))))))))) → U17_gga(T740, T742, T744, mult338_in_ggga(T740, s(s(s(s(s(s(s(T742))))))), T742, T744))
mult338_in_ggga(0, T754, 0, 0) → mult338_out_ggga(0, T754, 0, 0)
mult338_in_ggga(s(T767), T768, 0, T770) → U18_ggga(T767, T768, T770, mult12_in_gga(T767, s(T768), T770))
U18_ggga(T767, T768, T770, mult12_out_gga(T767, s(T768), T770)) → mult338_out_ggga(s(T767), T768, 0, T770)
mult338_in_ggga(T786, T787, s(T788), s(T790)) → U19_ggga(T786, T787, T788, T790, mult338_in_ggga(T786, T787, T788, T790))
U19_ggga(T786, T787, T788, T790, mult338_out_ggga(T786, T787, T788, T790)) → mult338_out_ggga(T786, T787, s(T788), s(T790))
U17_gga(T740, T742, T744, mult338_out_ggga(T740, s(s(s(s(s(s(s(T742))))))), T742, T744)) → mult12_out_gga(T740, s(s(s(s(s(s(s(s(T742)))))))), s(s(s(s(s(s(s(s(T744)))))))))
U20_gga(T28, T29, T31, mult12_out_gga(T28, T29, T31)) → times1_out_gga(s(T28), T29, T31)
MULT22_IN_GA(s(T63), T65) → MULT22_IN_GA(T63, T65)
MULT22_IN_GA(s(T63)) → MULT22_IN_GA(T63)
From the DPs we obtained the following set of size-change graphs: