0 Prolog
↳1 PrologToPiTRSViaGraphTransformerProof (⇒, 134 ms)
↳2 PiTRS
↳3 DependencyPairsProof (⇔, 95 ms)
↳4 PiDP
↳5 DependencyGraphProof (⇔, 0 ms)
↳6 AND
↳7 PiDP
↳8 UsableRulesProof (⇔, 0 ms)
↳9 PiDP
↳10 PiDPToQDPProof (⇒, 18 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
multA_in_gga(0, T5, 0) → multA_out_gga(0, T5, 0)
multA_in_gga(s(0), T24, T24) → multA_out_gga(s(0), T24, T24)
multA_in_gga(s(s(T29)), T30, T12) → U1_gga(T29, T30, T12, pB_in_ggaaa(T29, T30, X40, X41, T12))
pB_in_ggaaa(T29, T30, T33, X41, T12) → U5_ggaaa(T29, T30, T33, X41, T12, multC_in_gga(T29, T30, T33))
multC_in_gga(0, T40, 0) → multC_out_gga(0, T40, 0)
multC_in_gga(s(T45), T46, X64) → U2_gga(T45, T46, X64, pD_in_ggaa(T45, T46, X63, X64))
pD_in_ggaa(T45, T46, T49, X64) → U9_ggaa(T45, T46, T49, X64, multC_in_gga(T45, T46, T49))
U9_ggaa(T45, T46, T49, X64, multC_out_gga(T45, T46, T49)) → U10_ggaa(T45, T46, T49, X64, addE_in_gga(T49, T46, X64))
addE_in_gga(0, T58, T58) → addE_out_gga(0, T58, T58)
addE_in_gga(s(T63), T64, s(X87)) → U3_gga(T63, T64, X87, addE_in_gga(T63, T64, X87))
U3_gga(T63, T64, X87, addE_out_gga(T63, T64, X87)) → addE_out_gga(s(T63), T64, s(X87))
U10_ggaa(T45, T46, T49, X64, addE_out_gga(T49, T46, X64)) → pD_out_ggaa(T45, T46, T49, X64)
U2_gga(T45, T46, X64, pD_out_ggaa(T45, T46, X63, X64)) → multC_out_gga(s(T45), T46, X64)
U5_ggaaa(T29, T30, T33, X41, T12, multC_out_gga(T29, T30, T33)) → U6_ggaaa(T29, T30, T33, X41, T12, pG_in_ggaa(T33, T30, X41, T12))
pG_in_ggaa(T33, T30, T69, T12) → U7_ggaa(T33, T30, T69, T12, addE_in_gga(T33, T30, T69))
U7_ggaa(T33, T30, T69, T12, addE_out_gga(T33, T30, T69)) → U8_ggaa(T33, T30, T69, T12, addF_in_gga(T69, T30, T12))
addF_in_gga(0, T78, T78) → addF_out_gga(0, T78, T78)
addF_in_gga(s(T85), T86, s(T88)) → U4_gga(T85, T86, T88, addF_in_gga(T85, T86, T88))
U4_gga(T85, T86, T88, addF_out_gga(T85, T86, T88)) → addF_out_gga(s(T85), T86, s(T88))
U8_ggaa(T33, T30, T69, T12, addF_out_gga(T69, T30, T12)) → pG_out_ggaa(T33, T30, T69, T12)
U6_ggaaa(T29, T30, T33, X41, T12, pG_out_ggaa(T33, T30, X41, T12)) → pB_out_ggaaa(T29, T30, T33, X41, T12)
U1_gga(T29, T30, T12, pB_out_ggaaa(T29, T30, X40, X41, T12)) → multA_out_gga(s(s(T29)), T30, T12)
MULTA_IN_GGA(s(s(T29)), T30, T12) → U1_GGA(T29, T30, T12, pB_in_ggaaa(T29, T30, X40, X41, T12))
MULTA_IN_GGA(s(s(T29)), T30, T12) → PB_IN_GGAAA(T29, T30, X40, X41, T12)
PB_IN_GGAAA(T29, T30, T33, X41, T12) → U5_GGAAA(T29, T30, T33, X41, T12, multC_in_gga(T29, T30, T33))
PB_IN_GGAAA(T29, T30, T33, X41, T12) → MULTC_IN_GGA(T29, T30, T33)
MULTC_IN_GGA(s(T45), T46, X64) → U2_GGA(T45, T46, X64, pD_in_ggaa(T45, T46, X63, X64))
MULTC_IN_GGA(s(T45), T46, X64) → PD_IN_GGAA(T45, T46, X63, X64)
PD_IN_GGAA(T45, T46, T49, X64) → U9_GGAA(T45, T46, T49, X64, multC_in_gga(T45, T46, T49))
PD_IN_GGAA(T45, T46, T49, X64) → MULTC_IN_GGA(T45, T46, T49)
U9_GGAA(T45, T46, T49, X64, multC_out_gga(T45, T46, T49)) → U10_GGAA(T45, T46, T49, X64, addE_in_gga(T49, T46, X64))
U9_GGAA(T45, T46, T49, X64, multC_out_gga(T45, T46, T49)) → ADDE_IN_GGA(T49, T46, X64)
ADDE_IN_GGA(s(T63), T64, s(X87)) → U3_GGA(T63, T64, X87, addE_in_gga(T63, T64, X87))
ADDE_IN_GGA(s(T63), T64, s(X87)) → ADDE_IN_GGA(T63, T64, X87)
U5_GGAAA(T29, T30, T33, X41, T12, multC_out_gga(T29, T30, T33)) → U6_GGAAA(T29, T30, T33, X41, T12, pG_in_ggaa(T33, T30, X41, T12))
U5_GGAAA(T29, T30, T33, X41, T12, multC_out_gga(T29, T30, T33)) → PG_IN_GGAA(T33, T30, X41, T12)
PG_IN_GGAA(T33, T30, T69, T12) → U7_GGAA(T33, T30, T69, T12, addE_in_gga(T33, T30, T69))
PG_IN_GGAA(T33, T30, T69, T12) → ADDE_IN_GGA(T33, T30, T69)
U7_GGAA(T33, T30, T69, T12, addE_out_gga(T33, T30, T69)) → U8_GGAA(T33, T30, T69, T12, addF_in_gga(T69, T30, T12))
U7_GGAA(T33, T30, T69, T12, addE_out_gga(T33, T30, T69)) → ADDF_IN_GGA(T69, T30, T12)
ADDF_IN_GGA(s(T85), T86, s(T88)) → U4_GGA(T85, T86, T88, addF_in_gga(T85, T86, T88))
ADDF_IN_GGA(s(T85), T86, s(T88)) → ADDF_IN_GGA(T85, T86, T88)
multA_in_gga(0, T5, 0) → multA_out_gga(0, T5, 0)
multA_in_gga(s(0), T24, T24) → multA_out_gga(s(0), T24, T24)
multA_in_gga(s(s(T29)), T30, T12) → U1_gga(T29, T30, T12, pB_in_ggaaa(T29, T30, X40, X41, T12))
pB_in_ggaaa(T29, T30, T33, X41, T12) → U5_ggaaa(T29, T30, T33, X41, T12, multC_in_gga(T29, T30, T33))
multC_in_gga(0, T40, 0) → multC_out_gga(0, T40, 0)
multC_in_gga(s(T45), T46, X64) → U2_gga(T45, T46, X64, pD_in_ggaa(T45, T46, X63, X64))
pD_in_ggaa(T45, T46, T49, X64) → U9_ggaa(T45, T46, T49, X64, multC_in_gga(T45, T46, T49))
U9_ggaa(T45, T46, T49, X64, multC_out_gga(T45, T46, T49)) → U10_ggaa(T45, T46, T49, X64, addE_in_gga(T49, T46, X64))
addE_in_gga(0, T58, T58) → addE_out_gga(0, T58, T58)
addE_in_gga(s(T63), T64, s(X87)) → U3_gga(T63, T64, X87, addE_in_gga(T63, T64, X87))
U3_gga(T63, T64, X87, addE_out_gga(T63, T64, X87)) → addE_out_gga(s(T63), T64, s(X87))
U10_ggaa(T45, T46, T49, X64, addE_out_gga(T49, T46, X64)) → pD_out_ggaa(T45, T46, T49, X64)
U2_gga(T45, T46, X64, pD_out_ggaa(T45, T46, X63, X64)) → multC_out_gga(s(T45), T46, X64)
U5_ggaaa(T29, T30, T33, X41, T12, multC_out_gga(T29, T30, T33)) → U6_ggaaa(T29, T30, T33, X41, T12, pG_in_ggaa(T33, T30, X41, T12))
pG_in_ggaa(T33, T30, T69, T12) → U7_ggaa(T33, T30, T69, T12, addE_in_gga(T33, T30, T69))
U7_ggaa(T33, T30, T69, T12, addE_out_gga(T33, T30, T69)) → U8_ggaa(T33, T30, T69, T12, addF_in_gga(T69, T30, T12))
addF_in_gga(0, T78, T78) → addF_out_gga(0, T78, T78)
addF_in_gga(s(T85), T86, s(T88)) → U4_gga(T85, T86, T88, addF_in_gga(T85, T86, T88))
U4_gga(T85, T86, T88, addF_out_gga(T85, T86, T88)) → addF_out_gga(s(T85), T86, s(T88))
U8_ggaa(T33, T30, T69, T12, addF_out_gga(T69, T30, T12)) → pG_out_ggaa(T33, T30, T69, T12)
U6_ggaaa(T29, T30, T33, X41, T12, pG_out_ggaa(T33, T30, X41, T12)) → pB_out_ggaaa(T29, T30, T33, X41, T12)
U1_gga(T29, T30, T12, pB_out_ggaaa(T29, T30, X40, X41, T12)) → multA_out_gga(s(s(T29)), T30, T12)
MULTA_IN_GGA(s(s(T29)), T30, T12) → U1_GGA(T29, T30, T12, pB_in_ggaaa(T29, T30, X40, X41, T12))
MULTA_IN_GGA(s(s(T29)), T30, T12) → PB_IN_GGAAA(T29, T30, X40, X41, T12)
PB_IN_GGAAA(T29, T30, T33, X41, T12) → U5_GGAAA(T29, T30, T33, X41, T12, multC_in_gga(T29, T30, T33))
PB_IN_GGAAA(T29, T30, T33, X41, T12) → MULTC_IN_GGA(T29, T30, T33)
MULTC_IN_GGA(s(T45), T46, X64) → U2_GGA(T45, T46, X64, pD_in_ggaa(T45, T46, X63, X64))
MULTC_IN_GGA(s(T45), T46, X64) → PD_IN_GGAA(T45, T46, X63, X64)
PD_IN_GGAA(T45, T46, T49, X64) → U9_GGAA(T45, T46, T49, X64, multC_in_gga(T45, T46, T49))
PD_IN_GGAA(T45, T46, T49, X64) → MULTC_IN_GGA(T45, T46, T49)
U9_GGAA(T45, T46, T49, X64, multC_out_gga(T45, T46, T49)) → U10_GGAA(T45, T46, T49, X64, addE_in_gga(T49, T46, X64))
U9_GGAA(T45, T46, T49, X64, multC_out_gga(T45, T46, T49)) → ADDE_IN_GGA(T49, T46, X64)
ADDE_IN_GGA(s(T63), T64, s(X87)) → U3_GGA(T63, T64, X87, addE_in_gga(T63, T64, X87))
ADDE_IN_GGA(s(T63), T64, s(X87)) → ADDE_IN_GGA(T63, T64, X87)
U5_GGAAA(T29, T30, T33, X41, T12, multC_out_gga(T29, T30, T33)) → U6_GGAAA(T29, T30, T33, X41, T12, pG_in_ggaa(T33, T30, X41, T12))
U5_GGAAA(T29, T30, T33, X41, T12, multC_out_gga(T29, T30, T33)) → PG_IN_GGAA(T33, T30, X41, T12)
PG_IN_GGAA(T33, T30, T69, T12) → U7_GGAA(T33, T30, T69, T12, addE_in_gga(T33, T30, T69))
PG_IN_GGAA(T33, T30, T69, T12) → ADDE_IN_GGA(T33, T30, T69)
U7_GGAA(T33, T30, T69, T12, addE_out_gga(T33, T30, T69)) → U8_GGAA(T33, T30, T69, T12, addF_in_gga(T69, T30, T12))
U7_GGAA(T33, T30, T69, T12, addE_out_gga(T33, T30, T69)) → ADDF_IN_GGA(T69, T30, T12)
ADDF_IN_GGA(s(T85), T86, s(T88)) → U4_GGA(T85, T86, T88, addF_in_gga(T85, T86, T88))
ADDF_IN_GGA(s(T85), T86, s(T88)) → ADDF_IN_GGA(T85, T86, T88)
multA_in_gga(0, T5, 0) → multA_out_gga(0, T5, 0)
multA_in_gga(s(0), T24, T24) → multA_out_gga(s(0), T24, T24)
multA_in_gga(s(s(T29)), T30, T12) → U1_gga(T29, T30, T12, pB_in_ggaaa(T29, T30, X40, X41, T12))
pB_in_ggaaa(T29, T30, T33, X41, T12) → U5_ggaaa(T29, T30, T33, X41, T12, multC_in_gga(T29, T30, T33))
multC_in_gga(0, T40, 0) → multC_out_gga(0, T40, 0)
multC_in_gga(s(T45), T46, X64) → U2_gga(T45, T46, X64, pD_in_ggaa(T45, T46, X63, X64))
pD_in_ggaa(T45, T46, T49, X64) → U9_ggaa(T45, T46, T49, X64, multC_in_gga(T45, T46, T49))
U9_ggaa(T45, T46, T49, X64, multC_out_gga(T45, T46, T49)) → U10_ggaa(T45, T46, T49, X64, addE_in_gga(T49, T46, X64))
addE_in_gga(0, T58, T58) → addE_out_gga(0, T58, T58)
addE_in_gga(s(T63), T64, s(X87)) → U3_gga(T63, T64, X87, addE_in_gga(T63, T64, X87))
U3_gga(T63, T64, X87, addE_out_gga(T63, T64, X87)) → addE_out_gga(s(T63), T64, s(X87))
U10_ggaa(T45, T46, T49, X64, addE_out_gga(T49, T46, X64)) → pD_out_ggaa(T45, T46, T49, X64)
U2_gga(T45, T46, X64, pD_out_ggaa(T45, T46, X63, X64)) → multC_out_gga(s(T45), T46, X64)
U5_ggaaa(T29, T30, T33, X41, T12, multC_out_gga(T29, T30, T33)) → U6_ggaaa(T29, T30, T33, X41, T12, pG_in_ggaa(T33, T30, X41, T12))
pG_in_ggaa(T33, T30, T69, T12) → U7_ggaa(T33, T30, T69, T12, addE_in_gga(T33, T30, T69))
U7_ggaa(T33, T30, T69, T12, addE_out_gga(T33, T30, T69)) → U8_ggaa(T33, T30, T69, T12, addF_in_gga(T69, T30, T12))
addF_in_gga(0, T78, T78) → addF_out_gga(0, T78, T78)
addF_in_gga(s(T85), T86, s(T88)) → U4_gga(T85, T86, T88, addF_in_gga(T85, T86, T88))
U4_gga(T85, T86, T88, addF_out_gga(T85, T86, T88)) → addF_out_gga(s(T85), T86, s(T88))
U8_ggaa(T33, T30, T69, T12, addF_out_gga(T69, T30, T12)) → pG_out_ggaa(T33, T30, T69, T12)
U6_ggaaa(T29, T30, T33, X41, T12, pG_out_ggaa(T33, T30, X41, T12)) → pB_out_ggaaa(T29, T30, T33, X41, T12)
U1_gga(T29, T30, T12, pB_out_ggaaa(T29, T30, X40, X41, T12)) → multA_out_gga(s(s(T29)), T30, T12)
ADDF_IN_GGA(s(T85), T86, s(T88)) → ADDF_IN_GGA(T85, T86, T88)
multA_in_gga(0, T5, 0) → multA_out_gga(0, T5, 0)
multA_in_gga(s(0), T24, T24) → multA_out_gga(s(0), T24, T24)
multA_in_gga(s(s(T29)), T30, T12) → U1_gga(T29, T30, T12, pB_in_ggaaa(T29, T30, X40, X41, T12))
pB_in_ggaaa(T29, T30, T33, X41, T12) → U5_ggaaa(T29, T30, T33, X41, T12, multC_in_gga(T29, T30, T33))
multC_in_gga(0, T40, 0) → multC_out_gga(0, T40, 0)
multC_in_gga(s(T45), T46, X64) → U2_gga(T45, T46, X64, pD_in_ggaa(T45, T46, X63, X64))
pD_in_ggaa(T45, T46, T49, X64) → U9_ggaa(T45, T46, T49, X64, multC_in_gga(T45, T46, T49))
U9_ggaa(T45, T46, T49, X64, multC_out_gga(T45, T46, T49)) → U10_ggaa(T45, T46, T49, X64, addE_in_gga(T49, T46, X64))
addE_in_gga(0, T58, T58) → addE_out_gga(0, T58, T58)
addE_in_gga(s(T63), T64, s(X87)) → U3_gga(T63, T64, X87, addE_in_gga(T63, T64, X87))
U3_gga(T63, T64, X87, addE_out_gga(T63, T64, X87)) → addE_out_gga(s(T63), T64, s(X87))
U10_ggaa(T45, T46, T49, X64, addE_out_gga(T49, T46, X64)) → pD_out_ggaa(T45, T46, T49, X64)
U2_gga(T45, T46, X64, pD_out_ggaa(T45, T46, X63, X64)) → multC_out_gga(s(T45), T46, X64)
U5_ggaaa(T29, T30, T33, X41, T12, multC_out_gga(T29, T30, T33)) → U6_ggaaa(T29, T30, T33, X41, T12, pG_in_ggaa(T33, T30, X41, T12))
pG_in_ggaa(T33, T30, T69, T12) → U7_ggaa(T33, T30, T69, T12, addE_in_gga(T33, T30, T69))
U7_ggaa(T33, T30, T69, T12, addE_out_gga(T33, T30, T69)) → U8_ggaa(T33, T30, T69, T12, addF_in_gga(T69, T30, T12))
addF_in_gga(0, T78, T78) → addF_out_gga(0, T78, T78)
addF_in_gga(s(T85), T86, s(T88)) → U4_gga(T85, T86, T88, addF_in_gga(T85, T86, T88))
U4_gga(T85, T86, T88, addF_out_gga(T85, T86, T88)) → addF_out_gga(s(T85), T86, s(T88))
U8_ggaa(T33, T30, T69, T12, addF_out_gga(T69, T30, T12)) → pG_out_ggaa(T33, T30, T69, T12)
U6_ggaaa(T29, T30, T33, X41, T12, pG_out_ggaa(T33, T30, X41, T12)) → pB_out_ggaaa(T29, T30, T33, X41, T12)
U1_gga(T29, T30, T12, pB_out_ggaaa(T29, T30, X40, X41, T12)) → multA_out_gga(s(s(T29)), T30, T12)
ADDF_IN_GGA(s(T85), T86, s(T88)) → ADDF_IN_GGA(T85, T86, T88)
ADDF_IN_GGA(s(T85), T86) → ADDF_IN_GGA(T85, T86)
From the DPs we obtained the following set of size-change graphs:
ADDE_IN_GGA(s(T63), T64, s(X87)) → ADDE_IN_GGA(T63, T64, X87)
multA_in_gga(0, T5, 0) → multA_out_gga(0, T5, 0)
multA_in_gga(s(0), T24, T24) → multA_out_gga(s(0), T24, T24)
multA_in_gga(s(s(T29)), T30, T12) → U1_gga(T29, T30, T12, pB_in_ggaaa(T29, T30, X40, X41, T12))
pB_in_ggaaa(T29, T30, T33, X41, T12) → U5_ggaaa(T29, T30, T33, X41, T12, multC_in_gga(T29, T30, T33))
multC_in_gga(0, T40, 0) → multC_out_gga(0, T40, 0)
multC_in_gga(s(T45), T46, X64) → U2_gga(T45, T46, X64, pD_in_ggaa(T45, T46, X63, X64))
pD_in_ggaa(T45, T46, T49, X64) → U9_ggaa(T45, T46, T49, X64, multC_in_gga(T45, T46, T49))
U9_ggaa(T45, T46, T49, X64, multC_out_gga(T45, T46, T49)) → U10_ggaa(T45, T46, T49, X64, addE_in_gga(T49, T46, X64))
addE_in_gga(0, T58, T58) → addE_out_gga(0, T58, T58)
addE_in_gga(s(T63), T64, s(X87)) → U3_gga(T63, T64, X87, addE_in_gga(T63, T64, X87))
U3_gga(T63, T64, X87, addE_out_gga(T63, T64, X87)) → addE_out_gga(s(T63), T64, s(X87))
U10_ggaa(T45, T46, T49, X64, addE_out_gga(T49, T46, X64)) → pD_out_ggaa(T45, T46, T49, X64)
U2_gga(T45, T46, X64, pD_out_ggaa(T45, T46, X63, X64)) → multC_out_gga(s(T45), T46, X64)
U5_ggaaa(T29, T30, T33, X41, T12, multC_out_gga(T29, T30, T33)) → U6_ggaaa(T29, T30, T33, X41, T12, pG_in_ggaa(T33, T30, X41, T12))
pG_in_ggaa(T33, T30, T69, T12) → U7_ggaa(T33, T30, T69, T12, addE_in_gga(T33, T30, T69))
U7_ggaa(T33, T30, T69, T12, addE_out_gga(T33, T30, T69)) → U8_ggaa(T33, T30, T69, T12, addF_in_gga(T69, T30, T12))
addF_in_gga(0, T78, T78) → addF_out_gga(0, T78, T78)
addF_in_gga(s(T85), T86, s(T88)) → U4_gga(T85, T86, T88, addF_in_gga(T85, T86, T88))
U4_gga(T85, T86, T88, addF_out_gga(T85, T86, T88)) → addF_out_gga(s(T85), T86, s(T88))
U8_ggaa(T33, T30, T69, T12, addF_out_gga(T69, T30, T12)) → pG_out_ggaa(T33, T30, T69, T12)
U6_ggaaa(T29, T30, T33, X41, T12, pG_out_ggaa(T33, T30, X41, T12)) → pB_out_ggaaa(T29, T30, T33, X41, T12)
U1_gga(T29, T30, T12, pB_out_ggaaa(T29, T30, X40, X41, T12)) → multA_out_gga(s(s(T29)), T30, T12)
ADDE_IN_GGA(s(T63), T64, s(X87)) → ADDE_IN_GGA(T63, T64, X87)
ADDE_IN_GGA(s(T63), T64) → ADDE_IN_GGA(T63, T64)
From the DPs we obtained the following set of size-change graphs:
MULTC_IN_GGA(s(T45), T46, X64) → PD_IN_GGAA(T45, T46, X63, X64)
PD_IN_GGAA(T45, T46, T49, X64) → MULTC_IN_GGA(T45, T46, T49)
multA_in_gga(0, T5, 0) → multA_out_gga(0, T5, 0)
multA_in_gga(s(0), T24, T24) → multA_out_gga(s(0), T24, T24)
multA_in_gga(s(s(T29)), T30, T12) → U1_gga(T29, T30, T12, pB_in_ggaaa(T29, T30, X40, X41, T12))
pB_in_ggaaa(T29, T30, T33, X41, T12) → U5_ggaaa(T29, T30, T33, X41, T12, multC_in_gga(T29, T30, T33))
multC_in_gga(0, T40, 0) → multC_out_gga(0, T40, 0)
multC_in_gga(s(T45), T46, X64) → U2_gga(T45, T46, X64, pD_in_ggaa(T45, T46, X63, X64))
pD_in_ggaa(T45, T46, T49, X64) → U9_ggaa(T45, T46, T49, X64, multC_in_gga(T45, T46, T49))
U9_ggaa(T45, T46, T49, X64, multC_out_gga(T45, T46, T49)) → U10_ggaa(T45, T46, T49, X64, addE_in_gga(T49, T46, X64))
addE_in_gga(0, T58, T58) → addE_out_gga(0, T58, T58)
addE_in_gga(s(T63), T64, s(X87)) → U3_gga(T63, T64, X87, addE_in_gga(T63, T64, X87))
U3_gga(T63, T64, X87, addE_out_gga(T63, T64, X87)) → addE_out_gga(s(T63), T64, s(X87))
U10_ggaa(T45, T46, T49, X64, addE_out_gga(T49, T46, X64)) → pD_out_ggaa(T45, T46, T49, X64)
U2_gga(T45, T46, X64, pD_out_ggaa(T45, T46, X63, X64)) → multC_out_gga(s(T45), T46, X64)
U5_ggaaa(T29, T30, T33, X41, T12, multC_out_gga(T29, T30, T33)) → U6_ggaaa(T29, T30, T33, X41, T12, pG_in_ggaa(T33, T30, X41, T12))
pG_in_ggaa(T33, T30, T69, T12) → U7_ggaa(T33, T30, T69, T12, addE_in_gga(T33, T30, T69))
U7_ggaa(T33, T30, T69, T12, addE_out_gga(T33, T30, T69)) → U8_ggaa(T33, T30, T69, T12, addF_in_gga(T69, T30, T12))
addF_in_gga(0, T78, T78) → addF_out_gga(0, T78, T78)
addF_in_gga(s(T85), T86, s(T88)) → U4_gga(T85, T86, T88, addF_in_gga(T85, T86, T88))
U4_gga(T85, T86, T88, addF_out_gga(T85, T86, T88)) → addF_out_gga(s(T85), T86, s(T88))
U8_ggaa(T33, T30, T69, T12, addF_out_gga(T69, T30, T12)) → pG_out_ggaa(T33, T30, T69, T12)
U6_ggaaa(T29, T30, T33, X41, T12, pG_out_ggaa(T33, T30, X41, T12)) → pB_out_ggaaa(T29, T30, T33, X41, T12)
U1_gga(T29, T30, T12, pB_out_ggaaa(T29, T30, X40, X41, T12)) → multA_out_gga(s(s(T29)), T30, T12)
MULTC_IN_GGA(s(T45), T46, X64) → PD_IN_GGAA(T45, T46, X63, X64)
PD_IN_GGAA(T45, T46, T49, X64) → MULTC_IN_GGA(T45, T46, T49)
MULTC_IN_GGA(s(T45), T46) → PD_IN_GGAA(T45, T46)
PD_IN_GGAA(T45, T46) → MULTC_IN_GGA(T45, T46)
From the DPs we obtained the following set of size-change graphs: