(0) Obligation:

Clauses:

times(X, Y, Z) :- mult(X, Y, 0, Z).
mult(0, Y, 0, 0).
mult(s(U), Y, 0, Z) :- mult(U, Y, Y, Z).
mult(X, Y, s(W), s(Z)) :- mult(X, Y, W, Z).

Query: times(g,g,a)

(1) PrologToPiTRSViaGraphTransformerProof (SOUND transformation)

Transformed Prolog program to (Pi-)TRS.

(2) Obligation:

Pi-finite rewrite system:
The TRS R consists of the following rules:

timesA_in_gga(0, T15, 0) → timesA_out_gga(0, T15, 0)
timesA_in_gga(s(T28), T29, T31) → U1_gga(T28, T29, T31, multB_in_gga(T28, T29, T31))
multB_in_gga(0, 0, 0) → multB_out_gga(0, 0, 0)
multB_in_gga(s(T51), 0, T54) → U12_gga(T51, T54, multC_in_ga(T51, T54))
multC_in_ga(0, 0) → multC_out_ga(0, 0)
multC_in_ga(s(T63), T65) → U2_ga(T63, T65, multC_in_ga(T63, T65))
U2_ga(T63, T65, multC_out_ga(T63, T65)) → multC_out_ga(s(T63), T65)
U12_gga(T51, T54, multC_out_ga(T51, T54)) → multB_out_gga(s(T51), 0, T54)
multB_in_gga(0, s(0), s(0)) → multB_out_gga(0, s(0), s(0))
multB_in_gga(s(T99), s(0), s(T102)) → U13_gga(T99, T102, multD_in_ga(T99, T102))
multD_in_ga(0, s(0)) → multD_out_ga(0, s(0))
multD_in_ga(s(T119), s(T121)) → U3_ga(T119, T121, multD_in_ga(T119, T121))
U3_ga(T119, T121, multD_out_ga(T119, T121)) → multD_out_ga(s(T119), s(T121))
U13_gga(T99, T102, multD_out_ga(T99, T102)) → multB_out_gga(s(T99), s(0), s(T102))
multB_in_gga(0, s(s(0)), s(s(0))) → multB_out_gga(0, s(s(0)), s(s(0)))
multB_in_gga(s(T155), s(s(0)), s(s(T158))) → U14_gga(T155, T158, multE_in_ga(T155, T158))
multE_in_ga(0, s(s(0))) → multE_out_ga(0, s(s(0)))
multE_in_ga(s(T183), s(s(T185))) → U4_ga(T183, T185, multE_in_ga(T183, T185))
U4_ga(T183, T185, multE_out_ga(T183, T185)) → multE_out_ga(s(T183), s(s(T185)))
U14_gga(T155, T158, multE_out_ga(T155, T158)) → multB_out_gga(s(T155), s(s(0)), s(s(T158)))
multB_in_gga(0, s(s(s(0))), s(s(s(0)))) → multB_out_gga(0, s(s(s(0))), s(s(s(0))))
multB_in_gga(s(T219), s(s(s(0))), s(s(s(T222)))) → U15_gga(T219, T222, multF_in_ga(T219, T222))
multF_in_ga(0, s(s(s(0)))) → multF_out_ga(0, s(s(s(0))))
multF_in_ga(s(T255), s(s(s(T257)))) → U5_ga(T255, T257, multF_in_ga(T255, T257))
U5_ga(T255, T257, multF_out_ga(T255, T257)) → multF_out_ga(s(T255), s(s(s(T257))))
U15_gga(T219, T222, multF_out_ga(T219, T222)) → multB_out_gga(s(T219), s(s(s(0))), s(s(s(T222))))
multB_in_gga(0, s(s(s(s(0)))), s(s(s(s(0))))) → multB_out_gga(0, s(s(s(s(0)))), s(s(s(s(0)))))
multB_in_gga(s(T291), s(s(s(s(0)))), s(s(s(s(T294))))) → U16_gga(T291, T294, multG_in_ga(T291, T294))
multG_in_ga(0, s(s(s(s(0))))) → multG_out_ga(0, s(s(s(s(0)))))
multG_in_ga(s(T335), s(s(s(s(T337))))) → U6_ga(T335, T337, multG_in_ga(T335, T337))
U6_ga(T335, T337, multG_out_ga(T335, T337)) → multG_out_ga(s(T335), s(s(s(s(T337)))))
U16_gga(T291, T294, multG_out_ga(T291, T294)) → multB_out_gga(s(T291), s(s(s(s(0)))), s(s(s(s(T294)))))
multB_in_gga(0, s(s(s(s(s(0))))), s(s(s(s(s(0)))))) → multB_out_gga(0, s(s(s(s(s(0))))), s(s(s(s(s(0))))))
multB_in_gga(s(T371), s(s(s(s(s(0))))), s(s(s(s(s(T374)))))) → U17_gga(T371, T374, multH_in_ga(T371, T374))
multH_in_ga(0, s(s(s(s(s(0)))))) → multH_out_ga(0, s(s(s(s(s(0))))))
multH_in_ga(s(T423), s(s(s(s(s(T425)))))) → U7_ga(T423, T425, multH_in_ga(T423, T425))
U7_ga(T423, T425, multH_out_ga(T423, T425)) → multH_out_ga(s(T423), s(s(s(s(s(T425))))))
U17_gga(T371, T374, multH_out_ga(T371, T374)) → multB_out_gga(s(T371), s(s(s(s(s(0))))), s(s(s(s(s(T374))))))
multB_in_gga(0, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(0))))))) → multB_out_gga(0, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(0)))))))
multB_in_gga(s(T459), s(s(s(s(s(s(0)))))), s(s(s(s(s(s(T462))))))) → U18_gga(T459, T462, multI_in_ga(T459, T462))
multI_in_ga(0, s(s(s(s(s(s(0))))))) → multI_out_ga(0, s(s(s(s(s(s(0)))))))
multI_in_ga(s(T519), s(s(s(s(s(s(T521))))))) → U8_ga(T519, T521, multI_in_ga(T519, T521))
U8_ga(T519, T521, multI_out_ga(T519, T521)) → multI_out_ga(s(T519), s(s(s(s(s(s(T521)))))))
U18_gga(T459, T462, multI_out_ga(T459, T462)) → multB_out_gga(s(T459), s(s(s(s(s(s(0)))))), s(s(s(s(s(s(T462)))))))
multB_in_gga(0, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(0)))))))) → multB_out_gga(0, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(0))))))))
multB_in_gga(s(T555), s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(T558)))))))) → U19_gga(T555, T558, multJ_in_ga(T555, T558))
multJ_in_ga(0, s(s(s(s(s(s(s(0)))))))) → multJ_out_ga(0, s(s(s(s(s(s(s(0))))))))
multJ_in_ga(s(T623), s(s(s(s(s(s(s(T625)))))))) → U9_ga(T623, T625, multJ_in_ga(T623, T625))
U9_ga(T623, T625, multJ_out_ga(T623, T625)) → multJ_out_ga(s(T623), s(s(s(s(s(s(s(T625))))))))
U19_gga(T555, T558, multJ_out_ga(T555, T558)) → multB_out_gga(s(T555), s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(T558))))))))
multB_in_gga(T635, s(s(s(s(s(s(s(s(T637)))))))), s(s(s(s(s(s(s(s(T639))))))))) → U20_gga(T635, T637, T639, multK_in_ggga(T635, s(s(s(s(s(s(s(T637))))))), T637, T639))
multK_in_ggga(0, T649, 0, 0) → multK_out_ggga(0, T649, 0, 0)
multK_in_ggga(s(T662), T663, 0, T665) → U10_ggga(T662, T663, T665, multB_in_gga(T662, s(T663), T665))
U10_ggga(T662, T663, T665, multB_out_gga(T662, s(T663), T665)) → multK_out_ggga(s(T662), T663, 0, T665)
multK_in_ggga(T676, T677, s(T678), s(T680)) → U11_ggga(T676, T677, T678, T680, multK_in_ggga(T676, T677, T678, T680))
U11_ggga(T676, T677, T678, T680, multK_out_ggga(T676, T677, T678, T680)) → multK_out_ggga(T676, T677, s(T678), s(T680))
U20_gga(T635, T637, T639, multK_out_ggga(T635, s(s(s(s(s(s(s(T637))))))), T637, T639)) → multB_out_gga(T635, s(s(s(s(s(s(s(s(T637)))))))), s(s(s(s(s(s(s(s(T639)))))))))
U1_gga(T28, T29, T31, multB_out_gga(T28, T29, T31)) → timesA_out_gga(s(T28), T29, T31)

The argument filtering Pi contains the following mapping:
timesA_in_gga(x1, x2, x3)  =  timesA_in_gga(x1, x2)
0  =  0
timesA_out_gga(x1, x2, x3)  =  timesA_out_gga(x1, x2, x3)
s(x1)  =  s(x1)
U1_gga(x1, x2, x3, x4)  =  U1_gga(x1, x2, x4)
multB_in_gga(x1, x2, x3)  =  multB_in_gga(x1, x2)
multB_out_gga(x1, x2, x3)  =  multB_out_gga(x1, x2, x3)
U12_gga(x1, x2, x3)  =  U12_gga(x1, x3)
multC_in_ga(x1, x2)  =  multC_in_ga(x1)
multC_out_ga(x1, x2)  =  multC_out_ga(x1, x2)
U2_ga(x1, x2, x3)  =  U2_ga(x1, x3)
U13_gga(x1, x2, x3)  =  U13_gga(x1, x3)
multD_in_ga(x1, x2)  =  multD_in_ga(x1)
multD_out_ga(x1, x2)  =  multD_out_ga(x1, x2)
U3_ga(x1, x2, x3)  =  U3_ga(x1, x3)
U14_gga(x1, x2, x3)  =  U14_gga(x1, x3)
multE_in_ga(x1, x2)  =  multE_in_ga(x1)
multE_out_ga(x1, x2)  =  multE_out_ga(x1, x2)
U4_ga(x1, x2, x3)  =  U4_ga(x1, x3)
U15_gga(x1, x2, x3)  =  U15_gga(x1, x3)
multF_in_ga(x1, x2)  =  multF_in_ga(x1)
multF_out_ga(x1, x2)  =  multF_out_ga(x1, x2)
U5_ga(x1, x2, x3)  =  U5_ga(x1, x3)
U16_gga(x1, x2, x3)  =  U16_gga(x1, x3)
multG_in_ga(x1, x2)  =  multG_in_ga(x1)
multG_out_ga(x1, x2)  =  multG_out_ga(x1, x2)
U6_ga(x1, x2, x3)  =  U6_ga(x1, x3)
U17_gga(x1, x2, x3)  =  U17_gga(x1, x3)
multH_in_ga(x1, x2)  =  multH_in_ga(x1)
multH_out_ga(x1, x2)  =  multH_out_ga(x1, x2)
U7_ga(x1, x2, x3)  =  U7_ga(x1, x3)
U18_gga(x1, x2, x3)  =  U18_gga(x1, x3)
multI_in_ga(x1, x2)  =  multI_in_ga(x1)
multI_out_ga(x1, x2)  =  multI_out_ga(x1, x2)
U8_ga(x1, x2, x3)  =  U8_ga(x1, x3)
U19_gga(x1, x2, x3)  =  U19_gga(x1, x3)
multJ_in_ga(x1, x2)  =  multJ_in_ga(x1)
multJ_out_ga(x1, x2)  =  multJ_out_ga(x1, x2)
U9_ga(x1, x2, x3)  =  U9_ga(x1, x3)
U20_gga(x1, x2, x3, x4)  =  U20_gga(x1, x2, x4)
multK_in_ggga(x1, x2, x3, x4)  =  multK_in_ggga(x1, x2, x3)
multK_out_ggga(x1, x2, x3, x4)  =  multK_out_ggga(x1, x2, x3, x4)
U10_ggga(x1, x2, x3, x4)  =  U10_ggga(x1, x2, x4)
U11_ggga(x1, x2, x3, x4, x5)  =  U11_ggga(x1, x2, x3, x5)

(3) DependencyPairsProof (EQUIVALENT transformation)

Using Dependency Pairs [AG00,LOPSTR] we result in the following initial DP problem:
Pi DP problem:
The TRS P consists of the following rules:

TIMESA_IN_GGA(s(T28), T29, T31) → U1_GGA(T28, T29, T31, multB_in_gga(T28, T29, T31))
TIMESA_IN_GGA(s(T28), T29, T31) → MULTB_IN_GGA(T28, T29, T31)
MULTB_IN_GGA(s(T51), 0, T54) → U12_GGA(T51, T54, multC_in_ga(T51, T54))
MULTB_IN_GGA(s(T51), 0, T54) → MULTC_IN_GA(T51, T54)
MULTC_IN_GA(s(T63), T65) → U2_GA(T63, T65, multC_in_ga(T63, T65))
MULTC_IN_GA(s(T63), T65) → MULTC_IN_GA(T63, T65)
MULTB_IN_GGA(s(T99), s(0), s(T102)) → U13_GGA(T99, T102, multD_in_ga(T99, T102))
MULTB_IN_GGA(s(T99), s(0), s(T102)) → MULTD_IN_GA(T99, T102)
MULTD_IN_GA(s(T119), s(T121)) → U3_GA(T119, T121, multD_in_ga(T119, T121))
MULTD_IN_GA(s(T119), s(T121)) → MULTD_IN_GA(T119, T121)
MULTB_IN_GGA(s(T155), s(s(0)), s(s(T158))) → U14_GGA(T155, T158, multE_in_ga(T155, T158))
MULTB_IN_GGA(s(T155), s(s(0)), s(s(T158))) → MULTE_IN_GA(T155, T158)
MULTE_IN_GA(s(T183), s(s(T185))) → U4_GA(T183, T185, multE_in_ga(T183, T185))
MULTE_IN_GA(s(T183), s(s(T185))) → MULTE_IN_GA(T183, T185)
MULTB_IN_GGA(s(T219), s(s(s(0))), s(s(s(T222)))) → U15_GGA(T219, T222, multF_in_ga(T219, T222))
MULTB_IN_GGA(s(T219), s(s(s(0))), s(s(s(T222)))) → MULTF_IN_GA(T219, T222)
MULTF_IN_GA(s(T255), s(s(s(T257)))) → U5_GA(T255, T257, multF_in_ga(T255, T257))
MULTF_IN_GA(s(T255), s(s(s(T257)))) → MULTF_IN_GA(T255, T257)
MULTB_IN_GGA(s(T291), s(s(s(s(0)))), s(s(s(s(T294))))) → U16_GGA(T291, T294, multG_in_ga(T291, T294))
MULTB_IN_GGA(s(T291), s(s(s(s(0)))), s(s(s(s(T294))))) → MULTG_IN_GA(T291, T294)
MULTG_IN_GA(s(T335), s(s(s(s(T337))))) → U6_GA(T335, T337, multG_in_ga(T335, T337))
MULTG_IN_GA(s(T335), s(s(s(s(T337))))) → MULTG_IN_GA(T335, T337)
MULTB_IN_GGA(s(T371), s(s(s(s(s(0))))), s(s(s(s(s(T374)))))) → U17_GGA(T371, T374, multH_in_ga(T371, T374))
MULTB_IN_GGA(s(T371), s(s(s(s(s(0))))), s(s(s(s(s(T374)))))) → MULTH_IN_GA(T371, T374)
MULTH_IN_GA(s(T423), s(s(s(s(s(T425)))))) → U7_GA(T423, T425, multH_in_ga(T423, T425))
MULTH_IN_GA(s(T423), s(s(s(s(s(T425)))))) → MULTH_IN_GA(T423, T425)
MULTB_IN_GGA(s(T459), s(s(s(s(s(s(0)))))), s(s(s(s(s(s(T462))))))) → U18_GGA(T459, T462, multI_in_ga(T459, T462))
MULTB_IN_GGA(s(T459), s(s(s(s(s(s(0)))))), s(s(s(s(s(s(T462))))))) → MULTI_IN_GA(T459, T462)
MULTI_IN_GA(s(T519), s(s(s(s(s(s(T521))))))) → U8_GA(T519, T521, multI_in_ga(T519, T521))
MULTI_IN_GA(s(T519), s(s(s(s(s(s(T521))))))) → MULTI_IN_GA(T519, T521)
MULTB_IN_GGA(s(T555), s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(T558)))))))) → U19_GGA(T555, T558, multJ_in_ga(T555, T558))
MULTB_IN_GGA(s(T555), s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(T558)))))))) → MULTJ_IN_GA(T555, T558)
MULTJ_IN_GA(s(T623), s(s(s(s(s(s(s(T625)))))))) → U9_GA(T623, T625, multJ_in_ga(T623, T625))
MULTJ_IN_GA(s(T623), s(s(s(s(s(s(s(T625)))))))) → MULTJ_IN_GA(T623, T625)
MULTB_IN_GGA(T635, s(s(s(s(s(s(s(s(T637)))))))), s(s(s(s(s(s(s(s(T639))))))))) → U20_GGA(T635, T637, T639, multK_in_ggga(T635, s(s(s(s(s(s(s(T637))))))), T637, T639))
MULTB_IN_GGA(T635, s(s(s(s(s(s(s(s(T637)))))))), s(s(s(s(s(s(s(s(T639))))))))) → MULTK_IN_GGGA(T635, s(s(s(s(s(s(s(T637))))))), T637, T639)
MULTK_IN_GGGA(s(T662), T663, 0, T665) → U10_GGGA(T662, T663, T665, multB_in_gga(T662, s(T663), T665))
MULTK_IN_GGGA(s(T662), T663, 0, T665) → MULTB_IN_GGA(T662, s(T663), T665)
MULTK_IN_GGGA(T676, T677, s(T678), s(T680)) → U11_GGGA(T676, T677, T678, T680, multK_in_ggga(T676, T677, T678, T680))
MULTK_IN_GGGA(T676, T677, s(T678), s(T680)) → MULTK_IN_GGGA(T676, T677, T678, T680)

The TRS R consists of the following rules:

timesA_in_gga(0, T15, 0) → timesA_out_gga(0, T15, 0)
timesA_in_gga(s(T28), T29, T31) → U1_gga(T28, T29, T31, multB_in_gga(T28, T29, T31))
multB_in_gga(0, 0, 0) → multB_out_gga(0, 0, 0)
multB_in_gga(s(T51), 0, T54) → U12_gga(T51, T54, multC_in_ga(T51, T54))
multC_in_ga(0, 0) → multC_out_ga(0, 0)
multC_in_ga(s(T63), T65) → U2_ga(T63, T65, multC_in_ga(T63, T65))
U2_ga(T63, T65, multC_out_ga(T63, T65)) → multC_out_ga(s(T63), T65)
U12_gga(T51, T54, multC_out_ga(T51, T54)) → multB_out_gga(s(T51), 0, T54)
multB_in_gga(0, s(0), s(0)) → multB_out_gga(0, s(0), s(0))
multB_in_gga(s(T99), s(0), s(T102)) → U13_gga(T99, T102, multD_in_ga(T99, T102))
multD_in_ga(0, s(0)) → multD_out_ga(0, s(0))
multD_in_ga(s(T119), s(T121)) → U3_ga(T119, T121, multD_in_ga(T119, T121))
U3_ga(T119, T121, multD_out_ga(T119, T121)) → multD_out_ga(s(T119), s(T121))
U13_gga(T99, T102, multD_out_ga(T99, T102)) → multB_out_gga(s(T99), s(0), s(T102))
multB_in_gga(0, s(s(0)), s(s(0))) → multB_out_gga(0, s(s(0)), s(s(0)))
multB_in_gga(s(T155), s(s(0)), s(s(T158))) → U14_gga(T155, T158, multE_in_ga(T155, T158))
multE_in_ga(0, s(s(0))) → multE_out_ga(0, s(s(0)))
multE_in_ga(s(T183), s(s(T185))) → U4_ga(T183, T185, multE_in_ga(T183, T185))
U4_ga(T183, T185, multE_out_ga(T183, T185)) → multE_out_ga(s(T183), s(s(T185)))
U14_gga(T155, T158, multE_out_ga(T155, T158)) → multB_out_gga(s(T155), s(s(0)), s(s(T158)))
multB_in_gga(0, s(s(s(0))), s(s(s(0)))) → multB_out_gga(0, s(s(s(0))), s(s(s(0))))
multB_in_gga(s(T219), s(s(s(0))), s(s(s(T222)))) → U15_gga(T219, T222, multF_in_ga(T219, T222))
multF_in_ga(0, s(s(s(0)))) → multF_out_ga(0, s(s(s(0))))
multF_in_ga(s(T255), s(s(s(T257)))) → U5_ga(T255, T257, multF_in_ga(T255, T257))
U5_ga(T255, T257, multF_out_ga(T255, T257)) → multF_out_ga(s(T255), s(s(s(T257))))
U15_gga(T219, T222, multF_out_ga(T219, T222)) → multB_out_gga(s(T219), s(s(s(0))), s(s(s(T222))))
multB_in_gga(0, s(s(s(s(0)))), s(s(s(s(0))))) → multB_out_gga(0, s(s(s(s(0)))), s(s(s(s(0)))))
multB_in_gga(s(T291), s(s(s(s(0)))), s(s(s(s(T294))))) → U16_gga(T291, T294, multG_in_ga(T291, T294))
multG_in_ga(0, s(s(s(s(0))))) → multG_out_ga(0, s(s(s(s(0)))))
multG_in_ga(s(T335), s(s(s(s(T337))))) → U6_ga(T335, T337, multG_in_ga(T335, T337))
U6_ga(T335, T337, multG_out_ga(T335, T337)) → multG_out_ga(s(T335), s(s(s(s(T337)))))
U16_gga(T291, T294, multG_out_ga(T291, T294)) → multB_out_gga(s(T291), s(s(s(s(0)))), s(s(s(s(T294)))))
multB_in_gga(0, s(s(s(s(s(0))))), s(s(s(s(s(0)))))) → multB_out_gga(0, s(s(s(s(s(0))))), s(s(s(s(s(0))))))
multB_in_gga(s(T371), s(s(s(s(s(0))))), s(s(s(s(s(T374)))))) → U17_gga(T371, T374, multH_in_ga(T371, T374))
multH_in_ga(0, s(s(s(s(s(0)))))) → multH_out_ga(0, s(s(s(s(s(0))))))
multH_in_ga(s(T423), s(s(s(s(s(T425)))))) → U7_ga(T423, T425, multH_in_ga(T423, T425))
U7_ga(T423, T425, multH_out_ga(T423, T425)) → multH_out_ga(s(T423), s(s(s(s(s(T425))))))
U17_gga(T371, T374, multH_out_ga(T371, T374)) → multB_out_gga(s(T371), s(s(s(s(s(0))))), s(s(s(s(s(T374))))))
multB_in_gga(0, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(0))))))) → multB_out_gga(0, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(0)))))))
multB_in_gga(s(T459), s(s(s(s(s(s(0)))))), s(s(s(s(s(s(T462))))))) → U18_gga(T459, T462, multI_in_ga(T459, T462))
multI_in_ga(0, s(s(s(s(s(s(0))))))) → multI_out_ga(0, s(s(s(s(s(s(0)))))))
multI_in_ga(s(T519), s(s(s(s(s(s(T521))))))) → U8_ga(T519, T521, multI_in_ga(T519, T521))
U8_ga(T519, T521, multI_out_ga(T519, T521)) → multI_out_ga(s(T519), s(s(s(s(s(s(T521)))))))
U18_gga(T459, T462, multI_out_ga(T459, T462)) → multB_out_gga(s(T459), s(s(s(s(s(s(0)))))), s(s(s(s(s(s(T462)))))))
multB_in_gga(0, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(0)))))))) → multB_out_gga(0, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(0))))))))
multB_in_gga(s(T555), s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(T558)))))))) → U19_gga(T555, T558, multJ_in_ga(T555, T558))
multJ_in_ga(0, s(s(s(s(s(s(s(0)))))))) → multJ_out_ga(0, s(s(s(s(s(s(s(0))))))))
multJ_in_ga(s(T623), s(s(s(s(s(s(s(T625)))))))) → U9_ga(T623, T625, multJ_in_ga(T623, T625))
U9_ga(T623, T625, multJ_out_ga(T623, T625)) → multJ_out_ga(s(T623), s(s(s(s(s(s(s(T625))))))))
U19_gga(T555, T558, multJ_out_ga(T555, T558)) → multB_out_gga(s(T555), s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(T558))))))))
multB_in_gga(T635, s(s(s(s(s(s(s(s(T637)))))))), s(s(s(s(s(s(s(s(T639))))))))) → U20_gga(T635, T637, T639, multK_in_ggga(T635, s(s(s(s(s(s(s(T637))))))), T637, T639))
multK_in_ggga(0, T649, 0, 0) → multK_out_ggga(0, T649, 0, 0)
multK_in_ggga(s(T662), T663, 0, T665) → U10_ggga(T662, T663, T665, multB_in_gga(T662, s(T663), T665))
U10_ggga(T662, T663, T665, multB_out_gga(T662, s(T663), T665)) → multK_out_ggga(s(T662), T663, 0, T665)
multK_in_ggga(T676, T677, s(T678), s(T680)) → U11_ggga(T676, T677, T678, T680, multK_in_ggga(T676, T677, T678, T680))
U11_ggga(T676, T677, T678, T680, multK_out_ggga(T676, T677, T678, T680)) → multK_out_ggga(T676, T677, s(T678), s(T680))
U20_gga(T635, T637, T639, multK_out_ggga(T635, s(s(s(s(s(s(s(T637))))))), T637, T639)) → multB_out_gga(T635, s(s(s(s(s(s(s(s(T637)))))))), s(s(s(s(s(s(s(s(T639)))))))))
U1_gga(T28, T29, T31, multB_out_gga(T28, T29, T31)) → timesA_out_gga(s(T28), T29, T31)

The argument filtering Pi contains the following mapping:
timesA_in_gga(x1, x2, x3)  =  timesA_in_gga(x1, x2)
0  =  0
timesA_out_gga(x1, x2, x3)  =  timesA_out_gga(x1, x2, x3)
s(x1)  =  s(x1)
U1_gga(x1, x2, x3, x4)  =  U1_gga(x1, x2, x4)
multB_in_gga(x1, x2, x3)  =  multB_in_gga(x1, x2)
multB_out_gga(x1, x2, x3)  =  multB_out_gga(x1, x2, x3)
U12_gga(x1, x2, x3)  =  U12_gga(x1, x3)
multC_in_ga(x1, x2)  =  multC_in_ga(x1)
multC_out_ga(x1, x2)  =  multC_out_ga(x1, x2)
U2_ga(x1, x2, x3)  =  U2_ga(x1, x3)
U13_gga(x1, x2, x3)  =  U13_gga(x1, x3)
multD_in_ga(x1, x2)  =  multD_in_ga(x1)
multD_out_ga(x1, x2)  =  multD_out_ga(x1, x2)
U3_ga(x1, x2, x3)  =  U3_ga(x1, x3)
U14_gga(x1, x2, x3)  =  U14_gga(x1, x3)
multE_in_ga(x1, x2)  =  multE_in_ga(x1)
multE_out_ga(x1, x2)  =  multE_out_ga(x1, x2)
U4_ga(x1, x2, x3)  =  U4_ga(x1, x3)
U15_gga(x1, x2, x3)  =  U15_gga(x1, x3)
multF_in_ga(x1, x2)  =  multF_in_ga(x1)
multF_out_ga(x1, x2)  =  multF_out_ga(x1, x2)
U5_ga(x1, x2, x3)  =  U5_ga(x1, x3)
U16_gga(x1, x2, x3)  =  U16_gga(x1, x3)
multG_in_ga(x1, x2)  =  multG_in_ga(x1)
multG_out_ga(x1, x2)  =  multG_out_ga(x1, x2)
U6_ga(x1, x2, x3)  =  U6_ga(x1, x3)
U17_gga(x1, x2, x3)  =  U17_gga(x1, x3)
multH_in_ga(x1, x2)  =  multH_in_ga(x1)
multH_out_ga(x1, x2)  =  multH_out_ga(x1, x2)
U7_ga(x1, x2, x3)  =  U7_ga(x1, x3)
U18_gga(x1, x2, x3)  =  U18_gga(x1, x3)
multI_in_ga(x1, x2)  =  multI_in_ga(x1)
multI_out_ga(x1, x2)  =  multI_out_ga(x1, x2)
U8_ga(x1, x2, x3)  =  U8_ga(x1, x3)
U19_gga(x1, x2, x3)  =  U19_gga(x1, x3)
multJ_in_ga(x1, x2)  =  multJ_in_ga(x1)
multJ_out_ga(x1, x2)  =  multJ_out_ga(x1, x2)
U9_ga(x1, x2, x3)  =  U9_ga(x1, x3)
U20_gga(x1, x2, x3, x4)  =  U20_gga(x1, x2, x4)
multK_in_ggga(x1, x2, x3, x4)  =  multK_in_ggga(x1, x2, x3)
multK_out_ggga(x1, x2, x3, x4)  =  multK_out_ggga(x1, x2, x3, x4)
U10_ggga(x1, x2, x3, x4)  =  U10_ggga(x1, x2, x4)
U11_ggga(x1, x2, x3, x4, x5)  =  U11_ggga(x1, x2, x3, x5)
TIMESA_IN_GGA(x1, x2, x3)  =  TIMESA_IN_GGA(x1, x2)
U1_GGA(x1, x2, x3, x4)  =  U1_GGA(x1, x2, x4)
MULTB_IN_GGA(x1, x2, x3)  =  MULTB_IN_GGA(x1, x2)
U12_GGA(x1, x2, x3)  =  U12_GGA(x1, x3)
MULTC_IN_GA(x1, x2)  =  MULTC_IN_GA(x1)
U2_GA(x1, x2, x3)  =  U2_GA(x1, x3)
U13_GGA(x1, x2, x3)  =  U13_GGA(x1, x3)
MULTD_IN_GA(x1, x2)  =  MULTD_IN_GA(x1)
U3_GA(x1, x2, x3)  =  U3_GA(x1, x3)
U14_GGA(x1, x2, x3)  =  U14_GGA(x1, x3)
MULTE_IN_GA(x1, x2)  =  MULTE_IN_GA(x1)
U4_GA(x1, x2, x3)  =  U4_GA(x1, x3)
U15_GGA(x1, x2, x3)  =  U15_GGA(x1, x3)
MULTF_IN_GA(x1, x2)  =  MULTF_IN_GA(x1)
U5_GA(x1, x2, x3)  =  U5_GA(x1, x3)
U16_GGA(x1, x2, x3)  =  U16_GGA(x1, x3)
MULTG_IN_GA(x1, x2)  =  MULTG_IN_GA(x1)
U6_GA(x1, x2, x3)  =  U6_GA(x1, x3)
U17_GGA(x1, x2, x3)  =  U17_GGA(x1, x3)
MULTH_IN_GA(x1, x2)  =  MULTH_IN_GA(x1)
U7_GA(x1, x2, x3)  =  U7_GA(x1, x3)
U18_GGA(x1, x2, x3)  =  U18_GGA(x1, x3)
MULTI_IN_GA(x1, x2)  =  MULTI_IN_GA(x1)
U8_GA(x1, x2, x3)  =  U8_GA(x1, x3)
U19_GGA(x1, x2, x3)  =  U19_GGA(x1, x3)
MULTJ_IN_GA(x1, x2)  =  MULTJ_IN_GA(x1)
U9_GA(x1, x2, x3)  =  U9_GA(x1, x3)
U20_GGA(x1, x2, x3, x4)  =  U20_GGA(x1, x2, x4)
MULTK_IN_GGGA(x1, x2, x3, x4)  =  MULTK_IN_GGGA(x1, x2, x3)
U10_GGGA(x1, x2, x3, x4)  =  U10_GGGA(x1, x2, x4)
U11_GGGA(x1, x2, x3, x4, x5)  =  U11_GGGA(x1, x2, x3, x5)

We have to consider all (P,R,Pi)-chains

(4) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

TIMESA_IN_GGA(s(T28), T29, T31) → U1_GGA(T28, T29, T31, multB_in_gga(T28, T29, T31))
TIMESA_IN_GGA(s(T28), T29, T31) → MULTB_IN_GGA(T28, T29, T31)
MULTB_IN_GGA(s(T51), 0, T54) → U12_GGA(T51, T54, multC_in_ga(T51, T54))
MULTB_IN_GGA(s(T51), 0, T54) → MULTC_IN_GA(T51, T54)
MULTC_IN_GA(s(T63), T65) → U2_GA(T63, T65, multC_in_ga(T63, T65))
MULTC_IN_GA(s(T63), T65) → MULTC_IN_GA(T63, T65)
MULTB_IN_GGA(s(T99), s(0), s(T102)) → U13_GGA(T99, T102, multD_in_ga(T99, T102))
MULTB_IN_GGA(s(T99), s(0), s(T102)) → MULTD_IN_GA(T99, T102)
MULTD_IN_GA(s(T119), s(T121)) → U3_GA(T119, T121, multD_in_ga(T119, T121))
MULTD_IN_GA(s(T119), s(T121)) → MULTD_IN_GA(T119, T121)
MULTB_IN_GGA(s(T155), s(s(0)), s(s(T158))) → U14_GGA(T155, T158, multE_in_ga(T155, T158))
MULTB_IN_GGA(s(T155), s(s(0)), s(s(T158))) → MULTE_IN_GA(T155, T158)
MULTE_IN_GA(s(T183), s(s(T185))) → U4_GA(T183, T185, multE_in_ga(T183, T185))
MULTE_IN_GA(s(T183), s(s(T185))) → MULTE_IN_GA(T183, T185)
MULTB_IN_GGA(s(T219), s(s(s(0))), s(s(s(T222)))) → U15_GGA(T219, T222, multF_in_ga(T219, T222))
MULTB_IN_GGA(s(T219), s(s(s(0))), s(s(s(T222)))) → MULTF_IN_GA(T219, T222)
MULTF_IN_GA(s(T255), s(s(s(T257)))) → U5_GA(T255, T257, multF_in_ga(T255, T257))
MULTF_IN_GA(s(T255), s(s(s(T257)))) → MULTF_IN_GA(T255, T257)
MULTB_IN_GGA(s(T291), s(s(s(s(0)))), s(s(s(s(T294))))) → U16_GGA(T291, T294, multG_in_ga(T291, T294))
MULTB_IN_GGA(s(T291), s(s(s(s(0)))), s(s(s(s(T294))))) → MULTG_IN_GA(T291, T294)
MULTG_IN_GA(s(T335), s(s(s(s(T337))))) → U6_GA(T335, T337, multG_in_ga(T335, T337))
MULTG_IN_GA(s(T335), s(s(s(s(T337))))) → MULTG_IN_GA(T335, T337)
MULTB_IN_GGA(s(T371), s(s(s(s(s(0))))), s(s(s(s(s(T374)))))) → U17_GGA(T371, T374, multH_in_ga(T371, T374))
MULTB_IN_GGA(s(T371), s(s(s(s(s(0))))), s(s(s(s(s(T374)))))) → MULTH_IN_GA(T371, T374)
MULTH_IN_GA(s(T423), s(s(s(s(s(T425)))))) → U7_GA(T423, T425, multH_in_ga(T423, T425))
MULTH_IN_GA(s(T423), s(s(s(s(s(T425)))))) → MULTH_IN_GA(T423, T425)
MULTB_IN_GGA(s(T459), s(s(s(s(s(s(0)))))), s(s(s(s(s(s(T462))))))) → U18_GGA(T459, T462, multI_in_ga(T459, T462))
MULTB_IN_GGA(s(T459), s(s(s(s(s(s(0)))))), s(s(s(s(s(s(T462))))))) → MULTI_IN_GA(T459, T462)
MULTI_IN_GA(s(T519), s(s(s(s(s(s(T521))))))) → U8_GA(T519, T521, multI_in_ga(T519, T521))
MULTI_IN_GA(s(T519), s(s(s(s(s(s(T521))))))) → MULTI_IN_GA(T519, T521)
MULTB_IN_GGA(s(T555), s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(T558)))))))) → U19_GGA(T555, T558, multJ_in_ga(T555, T558))
MULTB_IN_GGA(s(T555), s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(T558)))))))) → MULTJ_IN_GA(T555, T558)
MULTJ_IN_GA(s(T623), s(s(s(s(s(s(s(T625)))))))) → U9_GA(T623, T625, multJ_in_ga(T623, T625))
MULTJ_IN_GA(s(T623), s(s(s(s(s(s(s(T625)))))))) → MULTJ_IN_GA(T623, T625)
MULTB_IN_GGA(T635, s(s(s(s(s(s(s(s(T637)))))))), s(s(s(s(s(s(s(s(T639))))))))) → U20_GGA(T635, T637, T639, multK_in_ggga(T635, s(s(s(s(s(s(s(T637))))))), T637, T639))
MULTB_IN_GGA(T635, s(s(s(s(s(s(s(s(T637)))))))), s(s(s(s(s(s(s(s(T639))))))))) → MULTK_IN_GGGA(T635, s(s(s(s(s(s(s(T637))))))), T637, T639)
MULTK_IN_GGGA(s(T662), T663, 0, T665) → U10_GGGA(T662, T663, T665, multB_in_gga(T662, s(T663), T665))
MULTK_IN_GGGA(s(T662), T663, 0, T665) → MULTB_IN_GGA(T662, s(T663), T665)
MULTK_IN_GGGA(T676, T677, s(T678), s(T680)) → U11_GGGA(T676, T677, T678, T680, multK_in_ggga(T676, T677, T678, T680))
MULTK_IN_GGGA(T676, T677, s(T678), s(T680)) → MULTK_IN_GGGA(T676, T677, T678, T680)

The TRS R consists of the following rules:

timesA_in_gga(0, T15, 0) → timesA_out_gga(0, T15, 0)
timesA_in_gga(s(T28), T29, T31) → U1_gga(T28, T29, T31, multB_in_gga(T28, T29, T31))
multB_in_gga(0, 0, 0) → multB_out_gga(0, 0, 0)
multB_in_gga(s(T51), 0, T54) → U12_gga(T51, T54, multC_in_ga(T51, T54))
multC_in_ga(0, 0) → multC_out_ga(0, 0)
multC_in_ga(s(T63), T65) → U2_ga(T63, T65, multC_in_ga(T63, T65))
U2_ga(T63, T65, multC_out_ga(T63, T65)) → multC_out_ga(s(T63), T65)
U12_gga(T51, T54, multC_out_ga(T51, T54)) → multB_out_gga(s(T51), 0, T54)
multB_in_gga(0, s(0), s(0)) → multB_out_gga(0, s(0), s(0))
multB_in_gga(s(T99), s(0), s(T102)) → U13_gga(T99, T102, multD_in_ga(T99, T102))
multD_in_ga(0, s(0)) → multD_out_ga(0, s(0))
multD_in_ga(s(T119), s(T121)) → U3_ga(T119, T121, multD_in_ga(T119, T121))
U3_ga(T119, T121, multD_out_ga(T119, T121)) → multD_out_ga(s(T119), s(T121))
U13_gga(T99, T102, multD_out_ga(T99, T102)) → multB_out_gga(s(T99), s(0), s(T102))
multB_in_gga(0, s(s(0)), s(s(0))) → multB_out_gga(0, s(s(0)), s(s(0)))
multB_in_gga(s(T155), s(s(0)), s(s(T158))) → U14_gga(T155, T158, multE_in_ga(T155, T158))
multE_in_ga(0, s(s(0))) → multE_out_ga(0, s(s(0)))
multE_in_ga(s(T183), s(s(T185))) → U4_ga(T183, T185, multE_in_ga(T183, T185))
U4_ga(T183, T185, multE_out_ga(T183, T185)) → multE_out_ga(s(T183), s(s(T185)))
U14_gga(T155, T158, multE_out_ga(T155, T158)) → multB_out_gga(s(T155), s(s(0)), s(s(T158)))
multB_in_gga(0, s(s(s(0))), s(s(s(0)))) → multB_out_gga(0, s(s(s(0))), s(s(s(0))))
multB_in_gga(s(T219), s(s(s(0))), s(s(s(T222)))) → U15_gga(T219, T222, multF_in_ga(T219, T222))
multF_in_ga(0, s(s(s(0)))) → multF_out_ga(0, s(s(s(0))))
multF_in_ga(s(T255), s(s(s(T257)))) → U5_ga(T255, T257, multF_in_ga(T255, T257))
U5_ga(T255, T257, multF_out_ga(T255, T257)) → multF_out_ga(s(T255), s(s(s(T257))))
U15_gga(T219, T222, multF_out_ga(T219, T222)) → multB_out_gga(s(T219), s(s(s(0))), s(s(s(T222))))
multB_in_gga(0, s(s(s(s(0)))), s(s(s(s(0))))) → multB_out_gga(0, s(s(s(s(0)))), s(s(s(s(0)))))
multB_in_gga(s(T291), s(s(s(s(0)))), s(s(s(s(T294))))) → U16_gga(T291, T294, multG_in_ga(T291, T294))
multG_in_ga(0, s(s(s(s(0))))) → multG_out_ga(0, s(s(s(s(0)))))
multG_in_ga(s(T335), s(s(s(s(T337))))) → U6_ga(T335, T337, multG_in_ga(T335, T337))
U6_ga(T335, T337, multG_out_ga(T335, T337)) → multG_out_ga(s(T335), s(s(s(s(T337)))))
U16_gga(T291, T294, multG_out_ga(T291, T294)) → multB_out_gga(s(T291), s(s(s(s(0)))), s(s(s(s(T294)))))
multB_in_gga(0, s(s(s(s(s(0))))), s(s(s(s(s(0)))))) → multB_out_gga(0, s(s(s(s(s(0))))), s(s(s(s(s(0))))))
multB_in_gga(s(T371), s(s(s(s(s(0))))), s(s(s(s(s(T374)))))) → U17_gga(T371, T374, multH_in_ga(T371, T374))
multH_in_ga(0, s(s(s(s(s(0)))))) → multH_out_ga(0, s(s(s(s(s(0))))))
multH_in_ga(s(T423), s(s(s(s(s(T425)))))) → U7_ga(T423, T425, multH_in_ga(T423, T425))
U7_ga(T423, T425, multH_out_ga(T423, T425)) → multH_out_ga(s(T423), s(s(s(s(s(T425))))))
U17_gga(T371, T374, multH_out_ga(T371, T374)) → multB_out_gga(s(T371), s(s(s(s(s(0))))), s(s(s(s(s(T374))))))
multB_in_gga(0, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(0))))))) → multB_out_gga(0, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(0)))))))
multB_in_gga(s(T459), s(s(s(s(s(s(0)))))), s(s(s(s(s(s(T462))))))) → U18_gga(T459, T462, multI_in_ga(T459, T462))
multI_in_ga(0, s(s(s(s(s(s(0))))))) → multI_out_ga(0, s(s(s(s(s(s(0)))))))
multI_in_ga(s(T519), s(s(s(s(s(s(T521))))))) → U8_ga(T519, T521, multI_in_ga(T519, T521))
U8_ga(T519, T521, multI_out_ga(T519, T521)) → multI_out_ga(s(T519), s(s(s(s(s(s(T521)))))))
U18_gga(T459, T462, multI_out_ga(T459, T462)) → multB_out_gga(s(T459), s(s(s(s(s(s(0)))))), s(s(s(s(s(s(T462)))))))
multB_in_gga(0, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(0)))))))) → multB_out_gga(0, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(0))))))))
multB_in_gga(s(T555), s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(T558)))))))) → U19_gga(T555, T558, multJ_in_ga(T555, T558))
multJ_in_ga(0, s(s(s(s(s(s(s(0)))))))) → multJ_out_ga(0, s(s(s(s(s(s(s(0))))))))
multJ_in_ga(s(T623), s(s(s(s(s(s(s(T625)))))))) → U9_ga(T623, T625, multJ_in_ga(T623, T625))
U9_ga(T623, T625, multJ_out_ga(T623, T625)) → multJ_out_ga(s(T623), s(s(s(s(s(s(s(T625))))))))
U19_gga(T555, T558, multJ_out_ga(T555, T558)) → multB_out_gga(s(T555), s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(T558))))))))
multB_in_gga(T635, s(s(s(s(s(s(s(s(T637)))))))), s(s(s(s(s(s(s(s(T639))))))))) → U20_gga(T635, T637, T639, multK_in_ggga(T635, s(s(s(s(s(s(s(T637))))))), T637, T639))
multK_in_ggga(0, T649, 0, 0) → multK_out_ggga(0, T649, 0, 0)
multK_in_ggga(s(T662), T663, 0, T665) → U10_ggga(T662, T663, T665, multB_in_gga(T662, s(T663), T665))
U10_ggga(T662, T663, T665, multB_out_gga(T662, s(T663), T665)) → multK_out_ggga(s(T662), T663, 0, T665)
multK_in_ggga(T676, T677, s(T678), s(T680)) → U11_ggga(T676, T677, T678, T680, multK_in_ggga(T676, T677, T678, T680))
U11_ggga(T676, T677, T678, T680, multK_out_ggga(T676, T677, T678, T680)) → multK_out_ggga(T676, T677, s(T678), s(T680))
U20_gga(T635, T637, T639, multK_out_ggga(T635, s(s(s(s(s(s(s(T637))))))), T637, T639)) → multB_out_gga(T635, s(s(s(s(s(s(s(s(T637)))))))), s(s(s(s(s(s(s(s(T639)))))))))
U1_gga(T28, T29, T31, multB_out_gga(T28, T29, T31)) → timesA_out_gga(s(T28), T29, T31)

The argument filtering Pi contains the following mapping:
timesA_in_gga(x1, x2, x3)  =  timesA_in_gga(x1, x2)
0  =  0
timesA_out_gga(x1, x2, x3)  =  timesA_out_gga(x1, x2, x3)
s(x1)  =  s(x1)
U1_gga(x1, x2, x3, x4)  =  U1_gga(x1, x2, x4)
multB_in_gga(x1, x2, x3)  =  multB_in_gga(x1, x2)
multB_out_gga(x1, x2, x3)  =  multB_out_gga(x1, x2, x3)
U12_gga(x1, x2, x3)  =  U12_gga(x1, x3)
multC_in_ga(x1, x2)  =  multC_in_ga(x1)
multC_out_ga(x1, x2)  =  multC_out_ga(x1, x2)
U2_ga(x1, x2, x3)  =  U2_ga(x1, x3)
U13_gga(x1, x2, x3)  =  U13_gga(x1, x3)
multD_in_ga(x1, x2)  =  multD_in_ga(x1)
multD_out_ga(x1, x2)  =  multD_out_ga(x1, x2)
U3_ga(x1, x2, x3)  =  U3_ga(x1, x3)
U14_gga(x1, x2, x3)  =  U14_gga(x1, x3)
multE_in_ga(x1, x2)  =  multE_in_ga(x1)
multE_out_ga(x1, x2)  =  multE_out_ga(x1, x2)
U4_ga(x1, x2, x3)  =  U4_ga(x1, x3)
U15_gga(x1, x2, x3)  =  U15_gga(x1, x3)
multF_in_ga(x1, x2)  =  multF_in_ga(x1)
multF_out_ga(x1, x2)  =  multF_out_ga(x1, x2)
U5_ga(x1, x2, x3)  =  U5_ga(x1, x3)
U16_gga(x1, x2, x3)  =  U16_gga(x1, x3)
multG_in_ga(x1, x2)  =  multG_in_ga(x1)
multG_out_ga(x1, x2)  =  multG_out_ga(x1, x2)
U6_ga(x1, x2, x3)  =  U6_ga(x1, x3)
U17_gga(x1, x2, x3)  =  U17_gga(x1, x3)
multH_in_ga(x1, x2)  =  multH_in_ga(x1)
multH_out_ga(x1, x2)  =  multH_out_ga(x1, x2)
U7_ga(x1, x2, x3)  =  U7_ga(x1, x3)
U18_gga(x1, x2, x3)  =  U18_gga(x1, x3)
multI_in_ga(x1, x2)  =  multI_in_ga(x1)
multI_out_ga(x1, x2)  =  multI_out_ga(x1, x2)
U8_ga(x1, x2, x3)  =  U8_ga(x1, x3)
U19_gga(x1, x2, x3)  =  U19_gga(x1, x3)
multJ_in_ga(x1, x2)  =  multJ_in_ga(x1)
multJ_out_ga(x1, x2)  =  multJ_out_ga(x1, x2)
U9_ga(x1, x2, x3)  =  U9_ga(x1, x3)
U20_gga(x1, x2, x3, x4)  =  U20_gga(x1, x2, x4)
multK_in_ggga(x1, x2, x3, x4)  =  multK_in_ggga(x1, x2, x3)
multK_out_ggga(x1, x2, x3, x4)  =  multK_out_ggga(x1, x2, x3, x4)
U10_ggga(x1, x2, x3, x4)  =  U10_ggga(x1, x2, x4)
U11_ggga(x1, x2, x3, x4, x5)  =  U11_ggga(x1, x2, x3, x5)
TIMESA_IN_GGA(x1, x2, x3)  =  TIMESA_IN_GGA(x1, x2)
U1_GGA(x1, x2, x3, x4)  =  U1_GGA(x1, x2, x4)
MULTB_IN_GGA(x1, x2, x3)  =  MULTB_IN_GGA(x1, x2)
U12_GGA(x1, x2, x3)  =  U12_GGA(x1, x3)
MULTC_IN_GA(x1, x2)  =  MULTC_IN_GA(x1)
U2_GA(x1, x2, x3)  =  U2_GA(x1, x3)
U13_GGA(x1, x2, x3)  =  U13_GGA(x1, x3)
MULTD_IN_GA(x1, x2)  =  MULTD_IN_GA(x1)
U3_GA(x1, x2, x3)  =  U3_GA(x1, x3)
U14_GGA(x1, x2, x3)  =  U14_GGA(x1, x3)
MULTE_IN_GA(x1, x2)  =  MULTE_IN_GA(x1)
U4_GA(x1, x2, x3)  =  U4_GA(x1, x3)
U15_GGA(x1, x2, x3)  =  U15_GGA(x1, x3)
MULTF_IN_GA(x1, x2)  =  MULTF_IN_GA(x1)
U5_GA(x1, x2, x3)  =  U5_GA(x1, x3)
U16_GGA(x1, x2, x3)  =  U16_GGA(x1, x3)
MULTG_IN_GA(x1, x2)  =  MULTG_IN_GA(x1)
U6_GA(x1, x2, x3)  =  U6_GA(x1, x3)
U17_GGA(x1, x2, x3)  =  U17_GGA(x1, x3)
MULTH_IN_GA(x1, x2)  =  MULTH_IN_GA(x1)
U7_GA(x1, x2, x3)  =  U7_GA(x1, x3)
U18_GGA(x1, x2, x3)  =  U18_GGA(x1, x3)
MULTI_IN_GA(x1, x2)  =  MULTI_IN_GA(x1)
U8_GA(x1, x2, x3)  =  U8_GA(x1, x3)
U19_GGA(x1, x2, x3)  =  U19_GGA(x1, x3)
MULTJ_IN_GA(x1, x2)  =  MULTJ_IN_GA(x1)
U9_GA(x1, x2, x3)  =  U9_GA(x1, x3)
U20_GGA(x1, x2, x3, x4)  =  U20_GGA(x1, x2, x4)
MULTK_IN_GGGA(x1, x2, x3, x4)  =  MULTK_IN_GGGA(x1, x2, x3)
U10_GGGA(x1, x2, x3, x4)  =  U10_GGGA(x1, x2, x4)
U11_GGGA(x1, x2, x3, x4, x5)  =  U11_GGGA(x1, x2, x3, x5)

We have to consider all (P,R,Pi)-chains

(5) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 9 SCCs with 29 less nodes.

(6) Complex Obligation (AND)

(7) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

MULTJ_IN_GA(s(T623), s(s(s(s(s(s(s(T625)))))))) → MULTJ_IN_GA(T623, T625)

The TRS R consists of the following rules:

timesA_in_gga(0, T15, 0) → timesA_out_gga(0, T15, 0)
timesA_in_gga(s(T28), T29, T31) → U1_gga(T28, T29, T31, multB_in_gga(T28, T29, T31))
multB_in_gga(0, 0, 0) → multB_out_gga(0, 0, 0)
multB_in_gga(s(T51), 0, T54) → U12_gga(T51, T54, multC_in_ga(T51, T54))
multC_in_ga(0, 0) → multC_out_ga(0, 0)
multC_in_ga(s(T63), T65) → U2_ga(T63, T65, multC_in_ga(T63, T65))
U2_ga(T63, T65, multC_out_ga(T63, T65)) → multC_out_ga(s(T63), T65)
U12_gga(T51, T54, multC_out_ga(T51, T54)) → multB_out_gga(s(T51), 0, T54)
multB_in_gga(0, s(0), s(0)) → multB_out_gga(0, s(0), s(0))
multB_in_gga(s(T99), s(0), s(T102)) → U13_gga(T99, T102, multD_in_ga(T99, T102))
multD_in_ga(0, s(0)) → multD_out_ga(0, s(0))
multD_in_ga(s(T119), s(T121)) → U3_ga(T119, T121, multD_in_ga(T119, T121))
U3_ga(T119, T121, multD_out_ga(T119, T121)) → multD_out_ga(s(T119), s(T121))
U13_gga(T99, T102, multD_out_ga(T99, T102)) → multB_out_gga(s(T99), s(0), s(T102))
multB_in_gga(0, s(s(0)), s(s(0))) → multB_out_gga(0, s(s(0)), s(s(0)))
multB_in_gga(s(T155), s(s(0)), s(s(T158))) → U14_gga(T155, T158, multE_in_ga(T155, T158))
multE_in_ga(0, s(s(0))) → multE_out_ga(0, s(s(0)))
multE_in_ga(s(T183), s(s(T185))) → U4_ga(T183, T185, multE_in_ga(T183, T185))
U4_ga(T183, T185, multE_out_ga(T183, T185)) → multE_out_ga(s(T183), s(s(T185)))
U14_gga(T155, T158, multE_out_ga(T155, T158)) → multB_out_gga(s(T155), s(s(0)), s(s(T158)))
multB_in_gga(0, s(s(s(0))), s(s(s(0)))) → multB_out_gga(0, s(s(s(0))), s(s(s(0))))
multB_in_gga(s(T219), s(s(s(0))), s(s(s(T222)))) → U15_gga(T219, T222, multF_in_ga(T219, T222))
multF_in_ga(0, s(s(s(0)))) → multF_out_ga(0, s(s(s(0))))
multF_in_ga(s(T255), s(s(s(T257)))) → U5_ga(T255, T257, multF_in_ga(T255, T257))
U5_ga(T255, T257, multF_out_ga(T255, T257)) → multF_out_ga(s(T255), s(s(s(T257))))
U15_gga(T219, T222, multF_out_ga(T219, T222)) → multB_out_gga(s(T219), s(s(s(0))), s(s(s(T222))))
multB_in_gga(0, s(s(s(s(0)))), s(s(s(s(0))))) → multB_out_gga(0, s(s(s(s(0)))), s(s(s(s(0)))))
multB_in_gga(s(T291), s(s(s(s(0)))), s(s(s(s(T294))))) → U16_gga(T291, T294, multG_in_ga(T291, T294))
multG_in_ga(0, s(s(s(s(0))))) → multG_out_ga(0, s(s(s(s(0)))))
multG_in_ga(s(T335), s(s(s(s(T337))))) → U6_ga(T335, T337, multG_in_ga(T335, T337))
U6_ga(T335, T337, multG_out_ga(T335, T337)) → multG_out_ga(s(T335), s(s(s(s(T337)))))
U16_gga(T291, T294, multG_out_ga(T291, T294)) → multB_out_gga(s(T291), s(s(s(s(0)))), s(s(s(s(T294)))))
multB_in_gga(0, s(s(s(s(s(0))))), s(s(s(s(s(0)))))) → multB_out_gga(0, s(s(s(s(s(0))))), s(s(s(s(s(0))))))
multB_in_gga(s(T371), s(s(s(s(s(0))))), s(s(s(s(s(T374)))))) → U17_gga(T371, T374, multH_in_ga(T371, T374))
multH_in_ga(0, s(s(s(s(s(0)))))) → multH_out_ga(0, s(s(s(s(s(0))))))
multH_in_ga(s(T423), s(s(s(s(s(T425)))))) → U7_ga(T423, T425, multH_in_ga(T423, T425))
U7_ga(T423, T425, multH_out_ga(T423, T425)) → multH_out_ga(s(T423), s(s(s(s(s(T425))))))
U17_gga(T371, T374, multH_out_ga(T371, T374)) → multB_out_gga(s(T371), s(s(s(s(s(0))))), s(s(s(s(s(T374))))))
multB_in_gga(0, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(0))))))) → multB_out_gga(0, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(0)))))))
multB_in_gga(s(T459), s(s(s(s(s(s(0)))))), s(s(s(s(s(s(T462))))))) → U18_gga(T459, T462, multI_in_ga(T459, T462))
multI_in_ga(0, s(s(s(s(s(s(0))))))) → multI_out_ga(0, s(s(s(s(s(s(0)))))))
multI_in_ga(s(T519), s(s(s(s(s(s(T521))))))) → U8_ga(T519, T521, multI_in_ga(T519, T521))
U8_ga(T519, T521, multI_out_ga(T519, T521)) → multI_out_ga(s(T519), s(s(s(s(s(s(T521)))))))
U18_gga(T459, T462, multI_out_ga(T459, T462)) → multB_out_gga(s(T459), s(s(s(s(s(s(0)))))), s(s(s(s(s(s(T462)))))))
multB_in_gga(0, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(0)))))))) → multB_out_gga(0, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(0))))))))
multB_in_gga(s(T555), s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(T558)))))))) → U19_gga(T555, T558, multJ_in_ga(T555, T558))
multJ_in_ga(0, s(s(s(s(s(s(s(0)))))))) → multJ_out_ga(0, s(s(s(s(s(s(s(0))))))))
multJ_in_ga(s(T623), s(s(s(s(s(s(s(T625)))))))) → U9_ga(T623, T625, multJ_in_ga(T623, T625))
U9_ga(T623, T625, multJ_out_ga(T623, T625)) → multJ_out_ga(s(T623), s(s(s(s(s(s(s(T625))))))))
U19_gga(T555, T558, multJ_out_ga(T555, T558)) → multB_out_gga(s(T555), s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(T558))))))))
multB_in_gga(T635, s(s(s(s(s(s(s(s(T637)))))))), s(s(s(s(s(s(s(s(T639))))))))) → U20_gga(T635, T637, T639, multK_in_ggga(T635, s(s(s(s(s(s(s(T637))))))), T637, T639))
multK_in_ggga(0, T649, 0, 0) → multK_out_ggga(0, T649, 0, 0)
multK_in_ggga(s(T662), T663, 0, T665) → U10_ggga(T662, T663, T665, multB_in_gga(T662, s(T663), T665))
U10_ggga(T662, T663, T665, multB_out_gga(T662, s(T663), T665)) → multK_out_ggga(s(T662), T663, 0, T665)
multK_in_ggga(T676, T677, s(T678), s(T680)) → U11_ggga(T676, T677, T678, T680, multK_in_ggga(T676, T677, T678, T680))
U11_ggga(T676, T677, T678, T680, multK_out_ggga(T676, T677, T678, T680)) → multK_out_ggga(T676, T677, s(T678), s(T680))
U20_gga(T635, T637, T639, multK_out_ggga(T635, s(s(s(s(s(s(s(T637))))))), T637, T639)) → multB_out_gga(T635, s(s(s(s(s(s(s(s(T637)))))))), s(s(s(s(s(s(s(s(T639)))))))))
U1_gga(T28, T29, T31, multB_out_gga(T28, T29, T31)) → timesA_out_gga(s(T28), T29, T31)

The argument filtering Pi contains the following mapping:
timesA_in_gga(x1, x2, x3)  =  timesA_in_gga(x1, x2)
0  =  0
timesA_out_gga(x1, x2, x3)  =  timesA_out_gga(x1, x2, x3)
s(x1)  =  s(x1)
U1_gga(x1, x2, x3, x4)  =  U1_gga(x1, x2, x4)
multB_in_gga(x1, x2, x3)  =  multB_in_gga(x1, x2)
multB_out_gga(x1, x2, x3)  =  multB_out_gga(x1, x2, x3)
U12_gga(x1, x2, x3)  =  U12_gga(x1, x3)
multC_in_ga(x1, x2)  =  multC_in_ga(x1)
multC_out_ga(x1, x2)  =  multC_out_ga(x1, x2)
U2_ga(x1, x2, x3)  =  U2_ga(x1, x3)
U13_gga(x1, x2, x3)  =  U13_gga(x1, x3)
multD_in_ga(x1, x2)  =  multD_in_ga(x1)
multD_out_ga(x1, x2)  =  multD_out_ga(x1, x2)
U3_ga(x1, x2, x3)  =  U3_ga(x1, x3)
U14_gga(x1, x2, x3)  =  U14_gga(x1, x3)
multE_in_ga(x1, x2)  =  multE_in_ga(x1)
multE_out_ga(x1, x2)  =  multE_out_ga(x1, x2)
U4_ga(x1, x2, x3)  =  U4_ga(x1, x3)
U15_gga(x1, x2, x3)  =  U15_gga(x1, x3)
multF_in_ga(x1, x2)  =  multF_in_ga(x1)
multF_out_ga(x1, x2)  =  multF_out_ga(x1, x2)
U5_ga(x1, x2, x3)  =  U5_ga(x1, x3)
U16_gga(x1, x2, x3)  =  U16_gga(x1, x3)
multG_in_ga(x1, x2)  =  multG_in_ga(x1)
multG_out_ga(x1, x2)  =  multG_out_ga(x1, x2)
U6_ga(x1, x2, x3)  =  U6_ga(x1, x3)
U17_gga(x1, x2, x3)  =  U17_gga(x1, x3)
multH_in_ga(x1, x2)  =  multH_in_ga(x1)
multH_out_ga(x1, x2)  =  multH_out_ga(x1, x2)
U7_ga(x1, x2, x3)  =  U7_ga(x1, x3)
U18_gga(x1, x2, x3)  =  U18_gga(x1, x3)
multI_in_ga(x1, x2)  =  multI_in_ga(x1)
multI_out_ga(x1, x2)  =  multI_out_ga(x1, x2)
U8_ga(x1, x2, x3)  =  U8_ga(x1, x3)
U19_gga(x1, x2, x3)  =  U19_gga(x1, x3)
multJ_in_ga(x1, x2)  =  multJ_in_ga(x1)
multJ_out_ga(x1, x2)  =  multJ_out_ga(x1, x2)
U9_ga(x1, x2, x3)  =  U9_ga(x1, x3)
U20_gga(x1, x2, x3, x4)  =  U20_gga(x1, x2, x4)
multK_in_ggga(x1, x2, x3, x4)  =  multK_in_ggga(x1, x2, x3)
multK_out_ggga(x1, x2, x3, x4)  =  multK_out_ggga(x1, x2, x3, x4)
U10_ggga(x1, x2, x3, x4)  =  U10_ggga(x1, x2, x4)
U11_ggga(x1, x2, x3, x4, x5)  =  U11_ggga(x1, x2, x3, x5)
MULTJ_IN_GA(x1, x2)  =  MULTJ_IN_GA(x1)

We have to consider all (P,R,Pi)-chains

(8) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(9) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

MULTJ_IN_GA(s(T623), s(s(s(s(s(s(s(T625)))))))) → MULTJ_IN_GA(T623, T625)

R is empty.
The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
MULTJ_IN_GA(x1, x2)  =  MULTJ_IN_GA(x1)

We have to consider all (P,R,Pi)-chains

(10) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(11) Obligation:

Q DP problem:
The TRS P consists of the following rules:

MULTJ_IN_GA(s(T623)) → MULTJ_IN_GA(T623)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(12) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • MULTJ_IN_GA(s(T623)) → MULTJ_IN_GA(T623)
    The graph contains the following edges 1 > 1

(13) YES

(14) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

MULTI_IN_GA(s(T519), s(s(s(s(s(s(T521))))))) → MULTI_IN_GA(T519, T521)

The TRS R consists of the following rules:

timesA_in_gga(0, T15, 0) → timesA_out_gga(0, T15, 0)
timesA_in_gga(s(T28), T29, T31) → U1_gga(T28, T29, T31, multB_in_gga(T28, T29, T31))
multB_in_gga(0, 0, 0) → multB_out_gga(0, 0, 0)
multB_in_gga(s(T51), 0, T54) → U12_gga(T51, T54, multC_in_ga(T51, T54))
multC_in_ga(0, 0) → multC_out_ga(0, 0)
multC_in_ga(s(T63), T65) → U2_ga(T63, T65, multC_in_ga(T63, T65))
U2_ga(T63, T65, multC_out_ga(T63, T65)) → multC_out_ga(s(T63), T65)
U12_gga(T51, T54, multC_out_ga(T51, T54)) → multB_out_gga(s(T51), 0, T54)
multB_in_gga(0, s(0), s(0)) → multB_out_gga(0, s(0), s(0))
multB_in_gga(s(T99), s(0), s(T102)) → U13_gga(T99, T102, multD_in_ga(T99, T102))
multD_in_ga(0, s(0)) → multD_out_ga(0, s(0))
multD_in_ga(s(T119), s(T121)) → U3_ga(T119, T121, multD_in_ga(T119, T121))
U3_ga(T119, T121, multD_out_ga(T119, T121)) → multD_out_ga(s(T119), s(T121))
U13_gga(T99, T102, multD_out_ga(T99, T102)) → multB_out_gga(s(T99), s(0), s(T102))
multB_in_gga(0, s(s(0)), s(s(0))) → multB_out_gga(0, s(s(0)), s(s(0)))
multB_in_gga(s(T155), s(s(0)), s(s(T158))) → U14_gga(T155, T158, multE_in_ga(T155, T158))
multE_in_ga(0, s(s(0))) → multE_out_ga(0, s(s(0)))
multE_in_ga(s(T183), s(s(T185))) → U4_ga(T183, T185, multE_in_ga(T183, T185))
U4_ga(T183, T185, multE_out_ga(T183, T185)) → multE_out_ga(s(T183), s(s(T185)))
U14_gga(T155, T158, multE_out_ga(T155, T158)) → multB_out_gga(s(T155), s(s(0)), s(s(T158)))
multB_in_gga(0, s(s(s(0))), s(s(s(0)))) → multB_out_gga(0, s(s(s(0))), s(s(s(0))))
multB_in_gga(s(T219), s(s(s(0))), s(s(s(T222)))) → U15_gga(T219, T222, multF_in_ga(T219, T222))
multF_in_ga(0, s(s(s(0)))) → multF_out_ga(0, s(s(s(0))))
multF_in_ga(s(T255), s(s(s(T257)))) → U5_ga(T255, T257, multF_in_ga(T255, T257))
U5_ga(T255, T257, multF_out_ga(T255, T257)) → multF_out_ga(s(T255), s(s(s(T257))))
U15_gga(T219, T222, multF_out_ga(T219, T222)) → multB_out_gga(s(T219), s(s(s(0))), s(s(s(T222))))
multB_in_gga(0, s(s(s(s(0)))), s(s(s(s(0))))) → multB_out_gga(0, s(s(s(s(0)))), s(s(s(s(0)))))
multB_in_gga(s(T291), s(s(s(s(0)))), s(s(s(s(T294))))) → U16_gga(T291, T294, multG_in_ga(T291, T294))
multG_in_ga(0, s(s(s(s(0))))) → multG_out_ga(0, s(s(s(s(0)))))
multG_in_ga(s(T335), s(s(s(s(T337))))) → U6_ga(T335, T337, multG_in_ga(T335, T337))
U6_ga(T335, T337, multG_out_ga(T335, T337)) → multG_out_ga(s(T335), s(s(s(s(T337)))))
U16_gga(T291, T294, multG_out_ga(T291, T294)) → multB_out_gga(s(T291), s(s(s(s(0)))), s(s(s(s(T294)))))
multB_in_gga(0, s(s(s(s(s(0))))), s(s(s(s(s(0)))))) → multB_out_gga(0, s(s(s(s(s(0))))), s(s(s(s(s(0))))))
multB_in_gga(s(T371), s(s(s(s(s(0))))), s(s(s(s(s(T374)))))) → U17_gga(T371, T374, multH_in_ga(T371, T374))
multH_in_ga(0, s(s(s(s(s(0)))))) → multH_out_ga(0, s(s(s(s(s(0))))))
multH_in_ga(s(T423), s(s(s(s(s(T425)))))) → U7_ga(T423, T425, multH_in_ga(T423, T425))
U7_ga(T423, T425, multH_out_ga(T423, T425)) → multH_out_ga(s(T423), s(s(s(s(s(T425))))))
U17_gga(T371, T374, multH_out_ga(T371, T374)) → multB_out_gga(s(T371), s(s(s(s(s(0))))), s(s(s(s(s(T374))))))
multB_in_gga(0, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(0))))))) → multB_out_gga(0, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(0)))))))
multB_in_gga(s(T459), s(s(s(s(s(s(0)))))), s(s(s(s(s(s(T462))))))) → U18_gga(T459, T462, multI_in_ga(T459, T462))
multI_in_ga(0, s(s(s(s(s(s(0))))))) → multI_out_ga(0, s(s(s(s(s(s(0)))))))
multI_in_ga(s(T519), s(s(s(s(s(s(T521))))))) → U8_ga(T519, T521, multI_in_ga(T519, T521))
U8_ga(T519, T521, multI_out_ga(T519, T521)) → multI_out_ga(s(T519), s(s(s(s(s(s(T521)))))))
U18_gga(T459, T462, multI_out_ga(T459, T462)) → multB_out_gga(s(T459), s(s(s(s(s(s(0)))))), s(s(s(s(s(s(T462)))))))
multB_in_gga(0, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(0)))))))) → multB_out_gga(0, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(0))))))))
multB_in_gga(s(T555), s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(T558)))))))) → U19_gga(T555, T558, multJ_in_ga(T555, T558))
multJ_in_ga(0, s(s(s(s(s(s(s(0)))))))) → multJ_out_ga(0, s(s(s(s(s(s(s(0))))))))
multJ_in_ga(s(T623), s(s(s(s(s(s(s(T625)))))))) → U9_ga(T623, T625, multJ_in_ga(T623, T625))
U9_ga(T623, T625, multJ_out_ga(T623, T625)) → multJ_out_ga(s(T623), s(s(s(s(s(s(s(T625))))))))
U19_gga(T555, T558, multJ_out_ga(T555, T558)) → multB_out_gga(s(T555), s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(T558))))))))
multB_in_gga(T635, s(s(s(s(s(s(s(s(T637)))))))), s(s(s(s(s(s(s(s(T639))))))))) → U20_gga(T635, T637, T639, multK_in_ggga(T635, s(s(s(s(s(s(s(T637))))))), T637, T639))
multK_in_ggga(0, T649, 0, 0) → multK_out_ggga(0, T649, 0, 0)
multK_in_ggga(s(T662), T663, 0, T665) → U10_ggga(T662, T663, T665, multB_in_gga(T662, s(T663), T665))
U10_ggga(T662, T663, T665, multB_out_gga(T662, s(T663), T665)) → multK_out_ggga(s(T662), T663, 0, T665)
multK_in_ggga(T676, T677, s(T678), s(T680)) → U11_ggga(T676, T677, T678, T680, multK_in_ggga(T676, T677, T678, T680))
U11_ggga(T676, T677, T678, T680, multK_out_ggga(T676, T677, T678, T680)) → multK_out_ggga(T676, T677, s(T678), s(T680))
U20_gga(T635, T637, T639, multK_out_ggga(T635, s(s(s(s(s(s(s(T637))))))), T637, T639)) → multB_out_gga(T635, s(s(s(s(s(s(s(s(T637)))))))), s(s(s(s(s(s(s(s(T639)))))))))
U1_gga(T28, T29, T31, multB_out_gga(T28, T29, T31)) → timesA_out_gga(s(T28), T29, T31)

The argument filtering Pi contains the following mapping:
timesA_in_gga(x1, x2, x3)  =  timesA_in_gga(x1, x2)
0  =  0
timesA_out_gga(x1, x2, x3)  =  timesA_out_gga(x1, x2, x3)
s(x1)  =  s(x1)
U1_gga(x1, x2, x3, x4)  =  U1_gga(x1, x2, x4)
multB_in_gga(x1, x2, x3)  =  multB_in_gga(x1, x2)
multB_out_gga(x1, x2, x3)  =  multB_out_gga(x1, x2, x3)
U12_gga(x1, x2, x3)  =  U12_gga(x1, x3)
multC_in_ga(x1, x2)  =  multC_in_ga(x1)
multC_out_ga(x1, x2)  =  multC_out_ga(x1, x2)
U2_ga(x1, x2, x3)  =  U2_ga(x1, x3)
U13_gga(x1, x2, x3)  =  U13_gga(x1, x3)
multD_in_ga(x1, x2)  =  multD_in_ga(x1)
multD_out_ga(x1, x2)  =  multD_out_ga(x1, x2)
U3_ga(x1, x2, x3)  =  U3_ga(x1, x3)
U14_gga(x1, x2, x3)  =  U14_gga(x1, x3)
multE_in_ga(x1, x2)  =  multE_in_ga(x1)
multE_out_ga(x1, x2)  =  multE_out_ga(x1, x2)
U4_ga(x1, x2, x3)  =  U4_ga(x1, x3)
U15_gga(x1, x2, x3)  =  U15_gga(x1, x3)
multF_in_ga(x1, x2)  =  multF_in_ga(x1)
multF_out_ga(x1, x2)  =  multF_out_ga(x1, x2)
U5_ga(x1, x2, x3)  =  U5_ga(x1, x3)
U16_gga(x1, x2, x3)  =  U16_gga(x1, x3)
multG_in_ga(x1, x2)  =  multG_in_ga(x1)
multG_out_ga(x1, x2)  =  multG_out_ga(x1, x2)
U6_ga(x1, x2, x3)  =  U6_ga(x1, x3)
U17_gga(x1, x2, x3)  =  U17_gga(x1, x3)
multH_in_ga(x1, x2)  =  multH_in_ga(x1)
multH_out_ga(x1, x2)  =  multH_out_ga(x1, x2)
U7_ga(x1, x2, x3)  =  U7_ga(x1, x3)
U18_gga(x1, x2, x3)  =  U18_gga(x1, x3)
multI_in_ga(x1, x2)  =  multI_in_ga(x1)
multI_out_ga(x1, x2)  =  multI_out_ga(x1, x2)
U8_ga(x1, x2, x3)  =  U8_ga(x1, x3)
U19_gga(x1, x2, x3)  =  U19_gga(x1, x3)
multJ_in_ga(x1, x2)  =  multJ_in_ga(x1)
multJ_out_ga(x1, x2)  =  multJ_out_ga(x1, x2)
U9_ga(x1, x2, x3)  =  U9_ga(x1, x3)
U20_gga(x1, x2, x3, x4)  =  U20_gga(x1, x2, x4)
multK_in_ggga(x1, x2, x3, x4)  =  multK_in_ggga(x1, x2, x3)
multK_out_ggga(x1, x2, x3, x4)  =  multK_out_ggga(x1, x2, x3, x4)
U10_ggga(x1, x2, x3, x4)  =  U10_ggga(x1, x2, x4)
U11_ggga(x1, x2, x3, x4, x5)  =  U11_ggga(x1, x2, x3, x5)
MULTI_IN_GA(x1, x2)  =  MULTI_IN_GA(x1)

We have to consider all (P,R,Pi)-chains

(15) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(16) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

MULTI_IN_GA(s(T519), s(s(s(s(s(s(T521))))))) → MULTI_IN_GA(T519, T521)

R is empty.
The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
MULTI_IN_GA(x1, x2)  =  MULTI_IN_GA(x1)

We have to consider all (P,R,Pi)-chains

(17) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(18) Obligation:

Q DP problem:
The TRS P consists of the following rules:

MULTI_IN_GA(s(T519)) → MULTI_IN_GA(T519)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(19) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • MULTI_IN_GA(s(T519)) → MULTI_IN_GA(T519)
    The graph contains the following edges 1 > 1

(20) YES

(21) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

MULTH_IN_GA(s(T423), s(s(s(s(s(T425)))))) → MULTH_IN_GA(T423, T425)

The TRS R consists of the following rules:

timesA_in_gga(0, T15, 0) → timesA_out_gga(0, T15, 0)
timesA_in_gga(s(T28), T29, T31) → U1_gga(T28, T29, T31, multB_in_gga(T28, T29, T31))
multB_in_gga(0, 0, 0) → multB_out_gga(0, 0, 0)
multB_in_gga(s(T51), 0, T54) → U12_gga(T51, T54, multC_in_ga(T51, T54))
multC_in_ga(0, 0) → multC_out_ga(0, 0)
multC_in_ga(s(T63), T65) → U2_ga(T63, T65, multC_in_ga(T63, T65))
U2_ga(T63, T65, multC_out_ga(T63, T65)) → multC_out_ga(s(T63), T65)
U12_gga(T51, T54, multC_out_ga(T51, T54)) → multB_out_gga(s(T51), 0, T54)
multB_in_gga(0, s(0), s(0)) → multB_out_gga(0, s(0), s(0))
multB_in_gga(s(T99), s(0), s(T102)) → U13_gga(T99, T102, multD_in_ga(T99, T102))
multD_in_ga(0, s(0)) → multD_out_ga(0, s(0))
multD_in_ga(s(T119), s(T121)) → U3_ga(T119, T121, multD_in_ga(T119, T121))
U3_ga(T119, T121, multD_out_ga(T119, T121)) → multD_out_ga(s(T119), s(T121))
U13_gga(T99, T102, multD_out_ga(T99, T102)) → multB_out_gga(s(T99), s(0), s(T102))
multB_in_gga(0, s(s(0)), s(s(0))) → multB_out_gga(0, s(s(0)), s(s(0)))
multB_in_gga(s(T155), s(s(0)), s(s(T158))) → U14_gga(T155, T158, multE_in_ga(T155, T158))
multE_in_ga(0, s(s(0))) → multE_out_ga(0, s(s(0)))
multE_in_ga(s(T183), s(s(T185))) → U4_ga(T183, T185, multE_in_ga(T183, T185))
U4_ga(T183, T185, multE_out_ga(T183, T185)) → multE_out_ga(s(T183), s(s(T185)))
U14_gga(T155, T158, multE_out_ga(T155, T158)) → multB_out_gga(s(T155), s(s(0)), s(s(T158)))
multB_in_gga(0, s(s(s(0))), s(s(s(0)))) → multB_out_gga(0, s(s(s(0))), s(s(s(0))))
multB_in_gga(s(T219), s(s(s(0))), s(s(s(T222)))) → U15_gga(T219, T222, multF_in_ga(T219, T222))
multF_in_ga(0, s(s(s(0)))) → multF_out_ga(0, s(s(s(0))))
multF_in_ga(s(T255), s(s(s(T257)))) → U5_ga(T255, T257, multF_in_ga(T255, T257))
U5_ga(T255, T257, multF_out_ga(T255, T257)) → multF_out_ga(s(T255), s(s(s(T257))))
U15_gga(T219, T222, multF_out_ga(T219, T222)) → multB_out_gga(s(T219), s(s(s(0))), s(s(s(T222))))
multB_in_gga(0, s(s(s(s(0)))), s(s(s(s(0))))) → multB_out_gga(0, s(s(s(s(0)))), s(s(s(s(0)))))
multB_in_gga(s(T291), s(s(s(s(0)))), s(s(s(s(T294))))) → U16_gga(T291, T294, multG_in_ga(T291, T294))
multG_in_ga(0, s(s(s(s(0))))) → multG_out_ga(0, s(s(s(s(0)))))
multG_in_ga(s(T335), s(s(s(s(T337))))) → U6_ga(T335, T337, multG_in_ga(T335, T337))
U6_ga(T335, T337, multG_out_ga(T335, T337)) → multG_out_ga(s(T335), s(s(s(s(T337)))))
U16_gga(T291, T294, multG_out_ga(T291, T294)) → multB_out_gga(s(T291), s(s(s(s(0)))), s(s(s(s(T294)))))
multB_in_gga(0, s(s(s(s(s(0))))), s(s(s(s(s(0)))))) → multB_out_gga(0, s(s(s(s(s(0))))), s(s(s(s(s(0))))))
multB_in_gga(s(T371), s(s(s(s(s(0))))), s(s(s(s(s(T374)))))) → U17_gga(T371, T374, multH_in_ga(T371, T374))
multH_in_ga(0, s(s(s(s(s(0)))))) → multH_out_ga(0, s(s(s(s(s(0))))))
multH_in_ga(s(T423), s(s(s(s(s(T425)))))) → U7_ga(T423, T425, multH_in_ga(T423, T425))
U7_ga(T423, T425, multH_out_ga(T423, T425)) → multH_out_ga(s(T423), s(s(s(s(s(T425))))))
U17_gga(T371, T374, multH_out_ga(T371, T374)) → multB_out_gga(s(T371), s(s(s(s(s(0))))), s(s(s(s(s(T374))))))
multB_in_gga(0, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(0))))))) → multB_out_gga(0, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(0)))))))
multB_in_gga(s(T459), s(s(s(s(s(s(0)))))), s(s(s(s(s(s(T462))))))) → U18_gga(T459, T462, multI_in_ga(T459, T462))
multI_in_ga(0, s(s(s(s(s(s(0))))))) → multI_out_ga(0, s(s(s(s(s(s(0)))))))
multI_in_ga(s(T519), s(s(s(s(s(s(T521))))))) → U8_ga(T519, T521, multI_in_ga(T519, T521))
U8_ga(T519, T521, multI_out_ga(T519, T521)) → multI_out_ga(s(T519), s(s(s(s(s(s(T521)))))))
U18_gga(T459, T462, multI_out_ga(T459, T462)) → multB_out_gga(s(T459), s(s(s(s(s(s(0)))))), s(s(s(s(s(s(T462)))))))
multB_in_gga(0, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(0)))))))) → multB_out_gga(0, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(0))))))))
multB_in_gga(s(T555), s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(T558)))))))) → U19_gga(T555, T558, multJ_in_ga(T555, T558))
multJ_in_ga(0, s(s(s(s(s(s(s(0)))))))) → multJ_out_ga(0, s(s(s(s(s(s(s(0))))))))
multJ_in_ga(s(T623), s(s(s(s(s(s(s(T625)))))))) → U9_ga(T623, T625, multJ_in_ga(T623, T625))
U9_ga(T623, T625, multJ_out_ga(T623, T625)) → multJ_out_ga(s(T623), s(s(s(s(s(s(s(T625))))))))
U19_gga(T555, T558, multJ_out_ga(T555, T558)) → multB_out_gga(s(T555), s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(T558))))))))
multB_in_gga(T635, s(s(s(s(s(s(s(s(T637)))))))), s(s(s(s(s(s(s(s(T639))))))))) → U20_gga(T635, T637, T639, multK_in_ggga(T635, s(s(s(s(s(s(s(T637))))))), T637, T639))
multK_in_ggga(0, T649, 0, 0) → multK_out_ggga(0, T649, 0, 0)
multK_in_ggga(s(T662), T663, 0, T665) → U10_ggga(T662, T663, T665, multB_in_gga(T662, s(T663), T665))
U10_ggga(T662, T663, T665, multB_out_gga(T662, s(T663), T665)) → multK_out_ggga(s(T662), T663, 0, T665)
multK_in_ggga(T676, T677, s(T678), s(T680)) → U11_ggga(T676, T677, T678, T680, multK_in_ggga(T676, T677, T678, T680))
U11_ggga(T676, T677, T678, T680, multK_out_ggga(T676, T677, T678, T680)) → multK_out_ggga(T676, T677, s(T678), s(T680))
U20_gga(T635, T637, T639, multK_out_ggga(T635, s(s(s(s(s(s(s(T637))))))), T637, T639)) → multB_out_gga(T635, s(s(s(s(s(s(s(s(T637)))))))), s(s(s(s(s(s(s(s(T639)))))))))
U1_gga(T28, T29, T31, multB_out_gga(T28, T29, T31)) → timesA_out_gga(s(T28), T29, T31)

The argument filtering Pi contains the following mapping:
timesA_in_gga(x1, x2, x3)  =  timesA_in_gga(x1, x2)
0  =  0
timesA_out_gga(x1, x2, x3)  =  timesA_out_gga(x1, x2, x3)
s(x1)  =  s(x1)
U1_gga(x1, x2, x3, x4)  =  U1_gga(x1, x2, x4)
multB_in_gga(x1, x2, x3)  =  multB_in_gga(x1, x2)
multB_out_gga(x1, x2, x3)  =  multB_out_gga(x1, x2, x3)
U12_gga(x1, x2, x3)  =  U12_gga(x1, x3)
multC_in_ga(x1, x2)  =  multC_in_ga(x1)
multC_out_ga(x1, x2)  =  multC_out_ga(x1, x2)
U2_ga(x1, x2, x3)  =  U2_ga(x1, x3)
U13_gga(x1, x2, x3)  =  U13_gga(x1, x3)
multD_in_ga(x1, x2)  =  multD_in_ga(x1)
multD_out_ga(x1, x2)  =  multD_out_ga(x1, x2)
U3_ga(x1, x2, x3)  =  U3_ga(x1, x3)
U14_gga(x1, x2, x3)  =  U14_gga(x1, x3)
multE_in_ga(x1, x2)  =  multE_in_ga(x1)
multE_out_ga(x1, x2)  =  multE_out_ga(x1, x2)
U4_ga(x1, x2, x3)  =  U4_ga(x1, x3)
U15_gga(x1, x2, x3)  =  U15_gga(x1, x3)
multF_in_ga(x1, x2)  =  multF_in_ga(x1)
multF_out_ga(x1, x2)  =  multF_out_ga(x1, x2)
U5_ga(x1, x2, x3)  =  U5_ga(x1, x3)
U16_gga(x1, x2, x3)  =  U16_gga(x1, x3)
multG_in_ga(x1, x2)  =  multG_in_ga(x1)
multG_out_ga(x1, x2)  =  multG_out_ga(x1, x2)
U6_ga(x1, x2, x3)  =  U6_ga(x1, x3)
U17_gga(x1, x2, x3)  =  U17_gga(x1, x3)
multH_in_ga(x1, x2)  =  multH_in_ga(x1)
multH_out_ga(x1, x2)  =  multH_out_ga(x1, x2)
U7_ga(x1, x2, x3)  =  U7_ga(x1, x3)
U18_gga(x1, x2, x3)  =  U18_gga(x1, x3)
multI_in_ga(x1, x2)  =  multI_in_ga(x1)
multI_out_ga(x1, x2)  =  multI_out_ga(x1, x2)
U8_ga(x1, x2, x3)  =  U8_ga(x1, x3)
U19_gga(x1, x2, x3)  =  U19_gga(x1, x3)
multJ_in_ga(x1, x2)  =  multJ_in_ga(x1)
multJ_out_ga(x1, x2)  =  multJ_out_ga(x1, x2)
U9_ga(x1, x2, x3)  =  U9_ga(x1, x3)
U20_gga(x1, x2, x3, x4)  =  U20_gga(x1, x2, x4)
multK_in_ggga(x1, x2, x3, x4)  =  multK_in_ggga(x1, x2, x3)
multK_out_ggga(x1, x2, x3, x4)  =  multK_out_ggga(x1, x2, x3, x4)
U10_ggga(x1, x2, x3, x4)  =  U10_ggga(x1, x2, x4)
U11_ggga(x1, x2, x3, x4, x5)  =  U11_ggga(x1, x2, x3, x5)
MULTH_IN_GA(x1, x2)  =  MULTH_IN_GA(x1)

We have to consider all (P,R,Pi)-chains

(22) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(23) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

MULTH_IN_GA(s(T423), s(s(s(s(s(T425)))))) → MULTH_IN_GA(T423, T425)

R is empty.
The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
MULTH_IN_GA(x1, x2)  =  MULTH_IN_GA(x1)

We have to consider all (P,R,Pi)-chains

(24) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(25) Obligation:

Q DP problem:
The TRS P consists of the following rules:

MULTH_IN_GA(s(T423)) → MULTH_IN_GA(T423)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(26) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • MULTH_IN_GA(s(T423)) → MULTH_IN_GA(T423)
    The graph contains the following edges 1 > 1

(27) YES

(28) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

MULTG_IN_GA(s(T335), s(s(s(s(T337))))) → MULTG_IN_GA(T335, T337)

The TRS R consists of the following rules:

timesA_in_gga(0, T15, 0) → timesA_out_gga(0, T15, 0)
timesA_in_gga(s(T28), T29, T31) → U1_gga(T28, T29, T31, multB_in_gga(T28, T29, T31))
multB_in_gga(0, 0, 0) → multB_out_gga(0, 0, 0)
multB_in_gga(s(T51), 0, T54) → U12_gga(T51, T54, multC_in_ga(T51, T54))
multC_in_ga(0, 0) → multC_out_ga(0, 0)
multC_in_ga(s(T63), T65) → U2_ga(T63, T65, multC_in_ga(T63, T65))
U2_ga(T63, T65, multC_out_ga(T63, T65)) → multC_out_ga(s(T63), T65)
U12_gga(T51, T54, multC_out_ga(T51, T54)) → multB_out_gga(s(T51), 0, T54)
multB_in_gga(0, s(0), s(0)) → multB_out_gga(0, s(0), s(0))
multB_in_gga(s(T99), s(0), s(T102)) → U13_gga(T99, T102, multD_in_ga(T99, T102))
multD_in_ga(0, s(0)) → multD_out_ga(0, s(0))
multD_in_ga(s(T119), s(T121)) → U3_ga(T119, T121, multD_in_ga(T119, T121))
U3_ga(T119, T121, multD_out_ga(T119, T121)) → multD_out_ga(s(T119), s(T121))
U13_gga(T99, T102, multD_out_ga(T99, T102)) → multB_out_gga(s(T99), s(0), s(T102))
multB_in_gga(0, s(s(0)), s(s(0))) → multB_out_gga(0, s(s(0)), s(s(0)))
multB_in_gga(s(T155), s(s(0)), s(s(T158))) → U14_gga(T155, T158, multE_in_ga(T155, T158))
multE_in_ga(0, s(s(0))) → multE_out_ga(0, s(s(0)))
multE_in_ga(s(T183), s(s(T185))) → U4_ga(T183, T185, multE_in_ga(T183, T185))
U4_ga(T183, T185, multE_out_ga(T183, T185)) → multE_out_ga(s(T183), s(s(T185)))
U14_gga(T155, T158, multE_out_ga(T155, T158)) → multB_out_gga(s(T155), s(s(0)), s(s(T158)))
multB_in_gga(0, s(s(s(0))), s(s(s(0)))) → multB_out_gga(0, s(s(s(0))), s(s(s(0))))
multB_in_gga(s(T219), s(s(s(0))), s(s(s(T222)))) → U15_gga(T219, T222, multF_in_ga(T219, T222))
multF_in_ga(0, s(s(s(0)))) → multF_out_ga(0, s(s(s(0))))
multF_in_ga(s(T255), s(s(s(T257)))) → U5_ga(T255, T257, multF_in_ga(T255, T257))
U5_ga(T255, T257, multF_out_ga(T255, T257)) → multF_out_ga(s(T255), s(s(s(T257))))
U15_gga(T219, T222, multF_out_ga(T219, T222)) → multB_out_gga(s(T219), s(s(s(0))), s(s(s(T222))))
multB_in_gga(0, s(s(s(s(0)))), s(s(s(s(0))))) → multB_out_gga(0, s(s(s(s(0)))), s(s(s(s(0)))))
multB_in_gga(s(T291), s(s(s(s(0)))), s(s(s(s(T294))))) → U16_gga(T291, T294, multG_in_ga(T291, T294))
multG_in_ga(0, s(s(s(s(0))))) → multG_out_ga(0, s(s(s(s(0)))))
multG_in_ga(s(T335), s(s(s(s(T337))))) → U6_ga(T335, T337, multG_in_ga(T335, T337))
U6_ga(T335, T337, multG_out_ga(T335, T337)) → multG_out_ga(s(T335), s(s(s(s(T337)))))
U16_gga(T291, T294, multG_out_ga(T291, T294)) → multB_out_gga(s(T291), s(s(s(s(0)))), s(s(s(s(T294)))))
multB_in_gga(0, s(s(s(s(s(0))))), s(s(s(s(s(0)))))) → multB_out_gga(0, s(s(s(s(s(0))))), s(s(s(s(s(0))))))
multB_in_gga(s(T371), s(s(s(s(s(0))))), s(s(s(s(s(T374)))))) → U17_gga(T371, T374, multH_in_ga(T371, T374))
multH_in_ga(0, s(s(s(s(s(0)))))) → multH_out_ga(0, s(s(s(s(s(0))))))
multH_in_ga(s(T423), s(s(s(s(s(T425)))))) → U7_ga(T423, T425, multH_in_ga(T423, T425))
U7_ga(T423, T425, multH_out_ga(T423, T425)) → multH_out_ga(s(T423), s(s(s(s(s(T425))))))
U17_gga(T371, T374, multH_out_ga(T371, T374)) → multB_out_gga(s(T371), s(s(s(s(s(0))))), s(s(s(s(s(T374))))))
multB_in_gga(0, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(0))))))) → multB_out_gga(0, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(0)))))))
multB_in_gga(s(T459), s(s(s(s(s(s(0)))))), s(s(s(s(s(s(T462))))))) → U18_gga(T459, T462, multI_in_ga(T459, T462))
multI_in_ga(0, s(s(s(s(s(s(0))))))) → multI_out_ga(0, s(s(s(s(s(s(0)))))))
multI_in_ga(s(T519), s(s(s(s(s(s(T521))))))) → U8_ga(T519, T521, multI_in_ga(T519, T521))
U8_ga(T519, T521, multI_out_ga(T519, T521)) → multI_out_ga(s(T519), s(s(s(s(s(s(T521)))))))
U18_gga(T459, T462, multI_out_ga(T459, T462)) → multB_out_gga(s(T459), s(s(s(s(s(s(0)))))), s(s(s(s(s(s(T462)))))))
multB_in_gga(0, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(0)))))))) → multB_out_gga(0, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(0))))))))
multB_in_gga(s(T555), s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(T558)))))))) → U19_gga(T555, T558, multJ_in_ga(T555, T558))
multJ_in_ga(0, s(s(s(s(s(s(s(0)))))))) → multJ_out_ga(0, s(s(s(s(s(s(s(0))))))))
multJ_in_ga(s(T623), s(s(s(s(s(s(s(T625)))))))) → U9_ga(T623, T625, multJ_in_ga(T623, T625))
U9_ga(T623, T625, multJ_out_ga(T623, T625)) → multJ_out_ga(s(T623), s(s(s(s(s(s(s(T625))))))))
U19_gga(T555, T558, multJ_out_ga(T555, T558)) → multB_out_gga(s(T555), s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(T558))))))))
multB_in_gga(T635, s(s(s(s(s(s(s(s(T637)))))))), s(s(s(s(s(s(s(s(T639))))))))) → U20_gga(T635, T637, T639, multK_in_ggga(T635, s(s(s(s(s(s(s(T637))))))), T637, T639))
multK_in_ggga(0, T649, 0, 0) → multK_out_ggga(0, T649, 0, 0)
multK_in_ggga(s(T662), T663, 0, T665) → U10_ggga(T662, T663, T665, multB_in_gga(T662, s(T663), T665))
U10_ggga(T662, T663, T665, multB_out_gga(T662, s(T663), T665)) → multK_out_ggga(s(T662), T663, 0, T665)
multK_in_ggga(T676, T677, s(T678), s(T680)) → U11_ggga(T676, T677, T678, T680, multK_in_ggga(T676, T677, T678, T680))
U11_ggga(T676, T677, T678, T680, multK_out_ggga(T676, T677, T678, T680)) → multK_out_ggga(T676, T677, s(T678), s(T680))
U20_gga(T635, T637, T639, multK_out_ggga(T635, s(s(s(s(s(s(s(T637))))))), T637, T639)) → multB_out_gga(T635, s(s(s(s(s(s(s(s(T637)))))))), s(s(s(s(s(s(s(s(T639)))))))))
U1_gga(T28, T29, T31, multB_out_gga(T28, T29, T31)) → timesA_out_gga(s(T28), T29, T31)

The argument filtering Pi contains the following mapping:
timesA_in_gga(x1, x2, x3)  =  timesA_in_gga(x1, x2)
0  =  0
timesA_out_gga(x1, x2, x3)  =  timesA_out_gga(x1, x2, x3)
s(x1)  =  s(x1)
U1_gga(x1, x2, x3, x4)  =  U1_gga(x1, x2, x4)
multB_in_gga(x1, x2, x3)  =  multB_in_gga(x1, x2)
multB_out_gga(x1, x2, x3)  =  multB_out_gga(x1, x2, x3)
U12_gga(x1, x2, x3)  =  U12_gga(x1, x3)
multC_in_ga(x1, x2)  =  multC_in_ga(x1)
multC_out_ga(x1, x2)  =  multC_out_ga(x1, x2)
U2_ga(x1, x2, x3)  =  U2_ga(x1, x3)
U13_gga(x1, x2, x3)  =  U13_gga(x1, x3)
multD_in_ga(x1, x2)  =  multD_in_ga(x1)
multD_out_ga(x1, x2)  =  multD_out_ga(x1, x2)
U3_ga(x1, x2, x3)  =  U3_ga(x1, x3)
U14_gga(x1, x2, x3)  =  U14_gga(x1, x3)
multE_in_ga(x1, x2)  =  multE_in_ga(x1)
multE_out_ga(x1, x2)  =  multE_out_ga(x1, x2)
U4_ga(x1, x2, x3)  =  U4_ga(x1, x3)
U15_gga(x1, x2, x3)  =  U15_gga(x1, x3)
multF_in_ga(x1, x2)  =  multF_in_ga(x1)
multF_out_ga(x1, x2)  =  multF_out_ga(x1, x2)
U5_ga(x1, x2, x3)  =  U5_ga(x1, x3)
U16_gga(x1, x2, x3)  =  U16_gga(x1, x3)
multG_in_ga(x1, x2)  =  multG_in_ga(x1)
multG_out_ga(x1, x2)  =  multG_out_ga(x1, x2)
U6_ga(x1, x2, x3)  =  U6_ga(x1, x3)
U17_gga(x1, x2, x3)  =  U17_gga(x1, x3)
multH_in_ga(x1, x2)  =  multH_in_ga(x1)
multH_out_ga(x1, x2)  =  multH_out_ga(x1, x2)
U7_ga(x1, x2, x3)  =  U7_ga(x1, x3)
U18_gga(x1, x2, x3)  =  U18_gga(x1, x3)
multI_in_ga(x1, x2)  =  multI_in_ga(x1)
multI_out_ga(x1, x2)  =  multI_out_ga(x1, x2)
U8_ga(x1, x2, x3)  =  U8_ga(x1, x3)
U19_gga(x1, x2, x3)  =  U19_gga(x1, x3)
multJ_in_ga(x1, x2)  =  multJ_in_ga(x1)
multJ_out_ga(x1, x2)  =  multJ_out_ga(x1, x2)
U9_ga(x1, x2, x3)  =  U9_ga(x1, x3)
U20_gga(x1, x2, x3, x4)  =  U20_gga(x1, x2, x4)
multK_in_ggga(x1, x2, x3, x4)  =  multK_in_ggga(x1, x2, x3)
multK_out_ggga(x1, x2, x3, x4)  =  multK_out_ggga(x1, x2, x3, x4)
U10_ggga(x1, x2, x3, x4)  =  U10_ggga(x1, x2, x4)
U11_ggga(x1, x2, x3, x4, x5)  =  U11_ggga(x1, x2, x3, x5)
MULTG_IN_GA(x1, x2)  =  MULTG_IN_GA(x1)

We have to consider all (P,R,Pi)-chains

(29) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(30) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

MULTG_IN_GA(s(T335), s(s(s(s(T337))))) → MULTG_IN_GA(T335, T337)

R is empty.
The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
MULTG_IN_GA(x1, x2)  =  MULTG_IN_GA(x1)

We have to consider all (P,R,Pi)-chains

(31) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(32) Obligation:

Q DP problem:
The TRS P consists of the following rules:

MULTG_IN_GA(s(T335)) → MULTG_IN_GA(T335)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(33) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • MULTG_IN_GA(s(T335)) → MULTG_IN_GA(T335)
    The graph contains the following edges 1 > 1

(34) YES

(35) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

MULTF_IN_GA(s(T255), s(s(s(T257)))) → MULTF_IN_GA(T255, T257)

The TRS R consists of the following rules:

timesA_in_gga(0, T15, 0) → timesA_out_gga(0, T15, 0)
timesA_in_gga(s(T28), T29, T31) → U1_gga(T28, T29, T31, multB_in_gga(T28, T29, T31))
multB_in_gga(0, 0, 0) → multB_out_gga(0, 0, 0)
multB_in_gga(s(T51), 0, T54) → U12_gga(T51, T54, multC_in_ga(T51, T54))
multC_in_ga(0, 0) → multC_out_ga(0, 0)
multC_in_ga(s(T63), T65) → U2_ga(T63, T65, multC_in_ga(T63, T65))
U2_ga(T63, T65, multC_out_ga(T63, T65)) → multC_out_ga(s(T63), T65)
U12_gga(T51, T54, multC_out_ga(T51, T54)) → multB_out_gga(s(T51), 0, T54)
multB_in_gga(0, s(0), s(0)) → multB_out_gga(0, s(0), s(0))
multB_in_gga(s(T99), s(0), s(T102)) → U13_gga(T99, T102, multD_in_ga(T99, T102))
multD_in_ga(0, s(0)) → multD_out_ga(0, s(0))
multD_in_ga(s(T119), s(T121)) → U3_ga(T119, T121, multD_in_ga(T119, T121))
U3_ga(T119, T121, multD_out_ga(T119, T121)) → multD_out_ga(s(T119), s(T121))
U13_gga(T99, T102, multD_out_ga(T99, T102)) → multB_out_gga(s(T99), s(0), s(T102))
multB_in_gga(0, s(s(0)), s(s(0))) → multB_out_gga(0, s(s(0)), s(s(0)))
multB_in_gga(s(T155), s(s(0)), s(s(T158))) → U14_gga(T155, T158, multE_in_ga(T155, T158))
multE_in_ga(0, s(s(0))) → multE_out_ga(0, s(s(0)))
multE_in_ga(s(T183), s(s(T185))) → U4_ga(T183, T185, multE_in_ga(T183, T185))
U4_ga(T183, T185, multE_out_ga(T183, T185)) → multE_out_ga(s(T183), s(s(T185)))
U14_gga(T155, T158, multE_out_ga(T155, T158)) → multB_out_gga(s(T155), s(s(0)), s(s(T158)))
multB_in_gga(0, s(s(s(0))), s(s(s(0)))) → multB_out_gga(0, s(s(s(0))), s(s(s(0))))
multB_in_gga(s(T219), s(s(s(0))), s(s(s(T222)))) → U15_gga(T219, T222, multF_in_ga(T219, T222))
multF_in_ga(0, s(s(s(0)))) → multF_out_ga(0, s(s(s(0))))
multF_in_ga(s(T255), s(s(s(T257)))) → U5_ga(T255, T257, multF_in_ga(T255, T257))
U5_ga(T255, T257, multF_out_ga(T255, T257)) → multF_out_ga(s(T255), s(s(s(T257))))
U15_gga(T219, T222, multF_out_ga(T219, T222)) → multB_out_gga(s(T219), s(s(s(0))), s(s(s(T222))))
multB_in_gga(0, s(s(s(s(0)))), s(s(s(s(0))))) → multB_out_gga(0, s(s(s(s(0)))), s(s(s(s(0)))))
multB_in_gga(s(T291), s(s(s(s(0)))), s(s(s(s(T294))))) → U16_gga(T291, T294, multG_in_ga(T291, T294))
multG_in_ga(0, s(s(s(s(0))))) → multG_out_ga(0, s(s(s(s(0)))))
multG_in_ga(s(T335), s(s(s(s(T337))))) → U6_ga(T335, T337, multG_in_ga(T335, T337))
U6_ga(T335, T337, multG_out_ga(T335, T337)) → multG_out_ga(s(T335), s(s(s(s(T337)))))
U16_gga(T291, T294, multG_out_ga(T291, T294)) → multB_out_gga(s(T291), s(s(s(s(0)))), s(s(s(s(T294)))))
multB_in_gga(0, s(s(s(s(s(0))))), s(s(s(s(s(0)))))) → multB_out_gga(0, s(s(s(s(s(0))))), s(s(s(s(s(0))))))
multB_in_gga(s(T371), s(s(s(s(s(0))))), s(s(s(s(s(T374)))))) → U17_gga(T371, T374, multH_in_ga(T371, T374))
multH_in_ga(0, s(s(s(s(s(0)))))) → multH_out_ga(0, s(s(s(s(s(0))))))
multH_in_ga(s(T423), s(s(s(s(s(T425)))))) → U7_ga(T423, T425, multH_in_ga(T423, T425))
U7_ga(T423, T425, multH_out_ga(T423, T425)) → multH_out_ga(s(T423), s(s(s(s(s(T425))))))
U17_gga(T371, T374, multH_out_ga(T371, T374)) → multB_out_gga(s(T371), s(s(s(s(s(0))))), s(s(s(s(s(T374))))))
multB_in_gga(0, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(0))))))) → multB_out_gga(0, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(0)))))))
multB_in_gga(s(T459), s(s(s(s(s(s(0)))))), s(s(s(s(s(s(T462))))))) → U18_gga(T459, T462, multI_in_ga(T459, T462))
multI_in_ga(0, s(s(s(s(s(s(0))))))) → multI_out_ga(0, s(s(s(s(s(s(0)))))))
multI_in_ga(s(T519), s(s(s(s(s(s(T521))))))) → U8_ga(T519, T521, multI_in_ga(T519, T521))
U8_ga(T519, T521, multI_out_ga(T519, T521)) → multI_out_ga(s(T519), s(s(s(s(s(s(T521)))))))
U18_gga(T459, T462, multI_out_ga(T459, T462)) → multB_out_gga(s(T459), s(s(s(s(s(s(0)))))), s(s(s(s(s(s(T462)))))))
multB_in_gga(0, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(0)))))))) → multB_out_gga(0, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(0))))))))
multB_in_gga(s(T555), s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(T558)))))))) → U19_gga(T555, T558, multJ_in_ga(T555, T558))
multJ_in_ga(0, s(s(s(s(s(s(s(0)))))))) → multJ_out_ga(0, s(s(s(s(s(s(s(0))))))))
multJ_in_ga(s(T623), s(s(s(s(s(s(s(T625)))))))) → U9_ga(T623, T625, multJ_in_ga(T623, T625))
U9_ga(T623, T625, multJ_out_ga(T623, T625)) → multJ_out_ga(s(T623), s(s(s(s(s(s(s(T625))))))))
U19_gga(T555, T558, multJ_out_ga(T555, T558)) → multB_out_gga(s(T555), s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(T558))))))))
multB_in_gga(T635, s(s(s(s(s(s(s(s(T637)))))))), s(s(s(s(s(s(s(s(T639))))))))) → U20_gga(T635, T637, T639, multK_in_ggga(T635, s(s(s(s(s(s(s(T637))))))), T637, T639))
multK_in_ggga(0, T649, 0, 0) → multK_out_ggga(0, T649, 0, 0)
multK_in_ggga(s(T662), T663, 0, T665) → U10_ggga(T662, T663, T665, multB_in_gga(T662, s(T663), T665))
U10_ggga(T662, T663, T665, multB_out_gga(T662, s(T663), T665)) → multK_out_ggga(s(T662), T663, 0, T665)
multK_in_ggga(T676, T677, s(T678), s(T680)) → U11_ggga(T676, T677, T678, T680, multK_in_ggga(T676, T677, T678, T680))
U11_ggga(T676, T677, T678, T680, multK_out_ggga(T676, T677, T678, T680)) → multK_out_ggga(T676, T677, s(T678), s(T680))
U20_gga(T635, T637, T639, multK_out_ggga(T635, s(s(s(s(s(s(s(T637))))))), T637, T639)) → multB_out_gga(T635, s(s(s(s(s(s(s(s(T637)))))))), s(s(s(s(s(s(s(s(T639)))))))))
U1_gga(T28, T29, T31, multB_out_gga(T28, T29, T31)) → timesA_out_gga(s(T28), T29, T31)

The argument filtering Pi contains the following mapping:
timesA_in_gga(x1, x2, x3)  =  timesA_in_gga(x1, x2)
0  =  0
timesA_out_gga(x1, x2, x3)  =  timesA_out_gga(x1, x2, x3)
s(x1)  =  s(x1)
U1_gga(x1, x2, x3, x4)  =  U1_gga(x1, x2, x4)
multB_in_gga(x1, x2, x3)  =  multB_in_gga(x1, x2)
multB_out_gga(x1, x2, x3)  =  multB_out_gga(x1, x2, x3)
U12_gga(x1, x2, x3)  =  U12_gga(x1, x3)
multC_in_ga(x1, x2)  =  multC_in_ga(x1)
multC_out_ga(x1, x2)  =  multC_out_ga(x1, x2)
U2_ga(x1, x2, x3)  =  U2_ga(x1, x3)
U13_gga(x1, x2, x3)  =  U13_gga(x1, x3)
multD_in_ga(x1, x2)  =  multD_in_ga(x1)
multD_out_ga(x1, x2)  =  multD_out_ga(x1, x2)
U3_ga(x1, x2, x3)  =  U3_ga(x1, x3)
U14_gga(x1, x2, x3)  =  U14_gga(x1, x3)
multE_in_ga(x1, x2)  =  multE_in_ga(x1)
multE_out_ga(x1, x2)  =  multE_out_ga(x1, x2)
U4_ga(x1, x2, x3)  =  U4_ga(x1, x3)
U15_gga(x1, x2, x3)  =  U15_gga(x1, x3)
multF_in_ga(x1, x2)  =  multF_in_ga(x1)
multF_out_ga(x1, x2)  =  multF_out_ga(x1, x2)
U5_ga(x1, x2, x3)  =  U5_ga(x1, x3)
U16_gga(x1, x2, x3)  =  U16_gga(x1, x3)
multG_in_ga(x1, x2)  =  multG_in_ga(x1)
multG_out_ga(x1, x2)  =  multG_out_ga(x1, x2)
U6_ga(x1, x2, x3)  =  U6_ga(x1, x3)
U17_gga(x1, x2, x3)  =  U17_gga(x1, x3)
multH_in_ga(x1, x2)  =  multH_in_ga(x1)
multH_out_ga(x1, x2)  =  multH_out_ga(x1, x2)
U7_ga(x1, x2, x3)  =  U7_ga(x1, x3)
U18_gga(x1, x2, x3)  =  U18_gga(x1, x3)
multI_in_ga(x1, x2)  =  multI_in_ga(x1)
multI_out_ga(x1, x2)  =  multI_out_ga(x1, x2)
U8_ga(x1, x2, x3)  =  U8_ga(x1, x3)
U19_gga(x1, x2, x3)  =  U19_gga(x1, x3)
multJ_in_ga(x1, x2)  =  multJ_in_ga(x1)
multJ_out_ga(x1, x2)  =  multJ_out_ga(x1, x2)
U9_ga(x1, x2, x3)  =  U9_ga(x1, x3)
U20_gga(x1, x2, x3, x4)  =  U20_gga(x1, x2, x4)
multK_in_ggga(x1, x2, x3, x4)  =  multK_in_ggga(x1, x2, x3)
multK_out_ggga(x1, x2, x3, x4)  =  multK_out_ggga(x1, x2, x3, x4)
U10_ggga(x1, x2, x3, x4)  =  U10_ggga(x1, x2, x4)
U11_ggga(x1, x2, x3, x4, x5)  =  U11_ggga(x1, x2, x3, x5)
MULTF_IN_GA(x1, x2)  =  MULTF_IN_GA(x1)

We have to consider all (P,R,Pi)-chains

(36) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(37) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

MULTF_IN_GA(s(T255), s(s(s(T257)))) → MULTF_IN_GA(T255, T257)

R is empty.
The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
MULTF_IN_GA(x1, x2)  =  MULTF_IN_GA(x1)

We have to consider all (P,R,Pi)-chains

(38) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(39) Obligation:

Q DP problem:
The TRS P consists of the following rules:

MULTF_IN_GA(s(T255)) → MULTF_IN_GA(T255)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(40) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • MULTF_IN_GA(s(T255)) → MULTF_IN_GA(T255)
    The graph contains the following edges 1 > 1

(41) YES

(42) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

MULTE_IN_GA(s(T183), s(s(T185))) → MULTE_IN_GA(T183, T185)

The TRS R consists of the following rules:

timesA_in_gga(0, T15, 0) → timesA_out_gga(0, T15, 0)
timesA_in_gga(s(T28), T29, T31) → U1_gga(T28, T29, T31, multB_in_gga(T28, T29, T31))
multB_in_gga(0, 0, 0) → multB_out_gga(0, 0, 0)
multB_in_gga(s(T51), 0, T54) → U12_gga(T51, T54, multC_in_ga(T51, T54))
multC_in_ga(0, 0) → multC_out_ga(0, 0)
multC_in_ga(s(T63), T65) → U2_ga(T63, T65, multC_in_ga(T63, T65))
U2_ga(T63, T65, multC_out_ga(T63, T65)) → multC_out_ga(s(T63), T65)
U12_gga(T51, T54, multC_out_ga(T51, T54)) → multB_out_gga(s(T51), 0, T54)
multB_in_gga(0, s(0), s(0)) → multB_out_gga(0, s(0), s(0))
multB_in_gga(s(T99), s(0), s(T102)) → U13_gga(T99, T102, multD_in_ga(T99, T102))
multD_in_ga(0, s(0)) → multD_out_ga(0, s(0))
multD_in_ga(s(T119), s(T121)) → U3_ga(T119, T121, multD_in_ga(T119, T121))
U3_ga(T119, T121, multD_out_ga(T119, T121)) → multD_out_ga(s(T119), s(T121))
U13_gga(T99, T102, multD_out_ga(T99, T102)) → multB_out_gga(s(T99), s(0), s(T102))
multB_in_gga(0, s(s(0)), s(s(0))) → multB_out_gga(0, s(s(0)), s(s(0)))
multB_in_gga(s(T155), s(s(0)), s(s(T158))) → U14_gga(T155, T158, multE_in_ga(T155, T158))
multE_in_ga(0, s(s(0))) → multE_out_ga(0, s(s(0)))
multE_in_ga(s(T183), s(s(T185))) → U4_ga(T183, T185, multE_in_ga(T183, T185))
U4_ga(T183, T185, multE_out_ga(T183, T185)) → multE_out_ga(s(T183), s(s(T185)))
U14_gga(T155, T158, multE_out_ga(T155, T158)) → multB_out_gga(s(T155), s(s(0)), s(s(T158)))
multB_in_gga(0, s(s(s(0))), s(s(s(0)))) → multB_out_gga(0, s(s(s(0))), s(s(s(0))))
multB_in_gga(s(T219), s(s(s(0))), s(s(s(T222)))) → U15_gga(T219, T222, multF_in_ga(T219, T222))
multF_in_ga(0, s(s(s(0)))) → multF_out_ga(0, s(s(s(0))))
multF_in_ga(s(T255), s(s(s(T257)))) → U5_ga(T255, T257, multF_in_ga(T255, T257))
U5_ga(T255, T257, multF_out_ga(T255, T257)) → multF_out_ga(s(T255), s(s(s(T257))))
U15_gga(T219, T222, multF_out_ga(T219, T222)) → multB_out_gga(s(T219), s(s(s(0))), s(s(s(T222))))
multB_in_gga(0, s(s(s(s(0)))), s(s(s(s(0))))) → multB_out_gga(0, s(s(s(s(0)))), s(s(s(s(0)))))
multB_in_gga(s(T291), s(s(s(s(0)))), s(s(s(s(T294))))) → U16_gga(T291, T294, multG_in_ga(T291, T294))
multG_in_ga(0, s(s(s(s(0))))) → multG_out_ga(0, s(s(s(s(0)))))
multG_in_ga(s(T335), s(s(s(s(T337))))) → U6_ga(T335, T337, multG_in_ga(T335, T337))
U6_ga(T335, T337, multG_out_ga(T335, T337)) → multG_out_ga(s(T335), s(s(s(s(T337)))))
U16_gga(T291, T294, multG_out_ga(T291, T294)) → multB_out_gga(s(T291), s(s(s(s(0)))), s(s(s(s(T294)))))
multB_in_gga(0, s(s(s(s(s(0))))), s(s(s(s(s(0)))))) → multB_out_gga(0, s(s(s(s(s(0))))), s(s(s(s(s(0))))))
multB_in_gga(s(T371), s(s(s(s(s(0))))), s(s(s(s(s(T374)))))) → U17_gga(T371, T374, multH_in_ga(T371, T374))
multH_in_ga(0, s(s(s(s(s(0)))))) → multH_out_ga(0, s(s(s(s(s(0))))))
multH_in_ga(s(T423), s(s(s(s(s(T425)))))) → U7_ga(T423, T425, multH_in_ga(T423, T425))
U7_ga(T423, T425, multH_out_ga(T423, T425)) → multH_out_ga(s(T423), s(s(s(s(s(T425))))))
U17_gga(T371, T374, multH_out_ga(T371, T374)) → multB_out_gga(s(T371), s(s(s(s(s(0))))), s(s(s(s(s(T374))))))
multB_in_gga(0, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(0))))))) → multB_out_gga(0, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(0)))))))
multB_in_gga(s(T459), s(s(s(s(s(s(0)))))), s(s(s(s(s(s(T462))))))) → U18_gga(T459, T462, multI_in_ga(T459, T462))
multI_in_ga(0, s(s(s(s(s(s(0))))))) → multI_out_ga(0, s(s(s(s(s(s(0)))))))
multI_in_ga(s(T519), s(s(s(s(s(s(T521))))))) → U8_ga(T519, T521, multI_in_ga(T519, T521))
U8_ga(T519, T521, multI_out_ga(T519, T521)) → multI_out_ga(s(T519), s(s(s(s(s(s(T521)))))))
U18_gga(T459, T462, multI_out_ga(T459, T462)) → multB_out_gga(s(T459), s(s(s(s(s(s(0)))))), s(s(s(s(s(s(T462)))))))
multB_in_gga(0, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(0)))))))) → multB_out_gga(0, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(0))))))))
multB_in_gga(s(T555), s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(T558)))))))) → U19_gga(T555, T558, multJ_in_ga(T555, T558))
multJ_in_ga(0, s(s(s(s(s(s(s(0)))))))) → multJ_out_ga(0, s(s(s(s(s(s(s(0))))))))
multJ_in_ga(s(T623), s(s(s(s(s(s(s(T625)))))))) → U9_ga(T623, T625, multJ_in_ga(T623, T625))
U9_ga(T623, T625, multJ_out_ga(T623, T625)) → multJ_out_ga(s(T623), s(s(s(s(s(s(s(T625))))))))
U19_gga(T555, T558, multJ_out_ga(T555, T558)) → multB_out_gga(s(T555), s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(T558))))))))
multB_in_gga(T635, s(s(s(s(s(s(s(s(T637)))))))), s(s(s(s(s(s(s(s(T639))))))))) → U20_gga(T635, T637, T639, multK_in_ggga(T635, s(s(s(s(s(s(s(T637))))))), T637, T639))
multK_in_ggga(0, T649, 0, 0) → multK_out_ggga(0, T649, 0, 0)
multK_in_ggga(s(T662), T663, 0, T665) → U10_ggga(T662, T663, T665, multB_in_gga(T662, s(T663), T665))
U10_ggga(T662, T663, T665, multB_out_gga(T662, s(T663), T665)) → multK_out_ggga(s(T662), T663, 0, T665)
multK_in_ggga(T676, T677, s(T678), s(T680)) → U11_ggga(T676, T677, T678, T680, multK_in_ggga(T676, T677, T678, T680))
U11_ggga(T676, T677, T678, T680, multK_out_ggga(T676, T677, T678, T680)) → multK_out_ggga(T676, T677, s(T678), s(T680))
U20_gga(T635, T637, T639, multK_out_ggga(T635, s(s(s(s(s(s(s(T637))))))), T637, T639)) → multB_out_gga(T635, s(s(s(s(s(s(s(s(T637)))))))), s(s(s(s(s(s(s(s(T639)))))))))
U1_gga(T28, T29, T31, multB_out_gga(T28, T29, T31)) → timesA_out_gga(s(T28), T29, T31)

The argument filtering Pi contains the following mapping:
timesA_in_gga(x1, x2, x3)  =  timesA_in_gga(x1, x2)
0  =  0
timesA_out_gga(x1, x2, x3)  =  timesA_out_gga(x1, x2, x3)
s(x1)  =  s(x1)
U1_gga(x1, x2, x3, x4)  =  U1_gga(x1, x2, x4)
multB_in_gga(x1, x2, x3)  =  multB_in_gga(x1, x2)
multB_out_gga(x1, x2, x3)  =  multB_out_gga(x1, x2, x3)
U12_gga(x1, x2, x3)  =  U12_gga(x1, x3)
multC_in_ga(x1, x2)  =  multC_in_ga(x1)
multC_out_ga(x1, x2)  =  multC_out_ga(x1, x2)
U2_ga(x1, x2, x3)  =  U2_ga(x1, x3)
U13_gga(x1, x2, x3)  =  U13_gga(x1, x3)
multD_in_ga(x1, x2)  =  multD_in_ga(x1)
multD_out_ga(x1, x2)  =  multD_out_ga(x1, x2)
U3_ga(x1, x2, x3)  =  U3_ga(x1, x3)
U14_gga(x1, x2, x3)  =  U14_gga(x1, x3)
multE_in_ga(x1, x2)  =  multE_in_ga(x1)
multE_out_ga(x1, x2)  =  multE_out_ga(x1, x2)
U4_ga(x1, x2, x3)  =  U4_ga(x1, x3)
U15_gga(x1, x2, x3)  =  U15_gga(x1, x3)
multF_in_ga(x1, x2)  =  multF_in_ga(x1)
multF_out_ga(x1, x2)  =  multF_out_ga(x1, x2)
U5_ga(x1, x2, x3)  =  U5_ga(x1, x3)
U16_gga(x1, x2, x3)  =  U16_gga(x1, x3)
multG_in_ga(x1, x2)  =  multG_in_ga(x1)
multG_out_ga(x1, x2)  =  multG_out_ga(x1, x2)
U6_ga(x1, x2, x3)  =  U6_ga(x1, x3)
U17_gga(x1, x2, x3)  =  U17_gga(x1, x3)
multH_in_ga(x1, x2)  =  multH_in_ga(x1)
multH_out_ga(x1, x2)  =  multH_out_ga(x1, x2)
U7_ga(x1, x2, x3)  =  U7_ga(x1, x3)
U18_gga(x1, x2, x3)  =  U18_gga(x1, x3)
multI_in_ga(x1, x2)  =  multI_in_ga(x1)
multI_out_ga(x1, x2)  =  multI_out_ga(x1, x2)
U8_ga(x1, x2, x3)  =  U8_ga(x1, x3)
U19_gga(x1, x2, x3)  =  U19_gga(x1, x3)
multJ_in_ga(x1, x2)  =  multJ_in_ga(x1)
multJ_out_ga(x1, x2)  =  multJ_out_ga(x1, x2)
U9_ga(x1, x2, x3)  =  U9_ga(x1, x3)
U20_gga(x1, x2, x3, x4)  =  U20_gga(x1, x2, x4)
multK_in_ggga(x1, x2, x3, x4)  =  multK_in_ggga(x1, x2, x3)
multK_out_ggga(x1, x2, x3, x4)  =  multK_out_ggga(x1, x2, x3, x4)
U10_ggga(x1, x2, x3, x4)  =  U10_ggga(x1, x2, x4)
U11_ggga(x1, x2, x3, x4, x5)  =  U11_ggga(x1, x2, x3, x5)
MULTE_IN_GA(x1, x2)  =  MULTE_IN_GA(x1)

We have to consider all (P,R,Pi)-chains

(43) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(44) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

MULTE_IN_GA(s(T183), s(s(T185))) → MULTE_IN_GA(T183, T185)

R is empty.
The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
MULTE_IN_GA(x1, x2)  =  MULTE_IN_GA(x1)

We have to consider all (P,R,Pi)-chains

(45) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(46) Obligation:

Q DP problem:
The TRS P consists of the following rules:

MULTE_IN_GA(s(T183)) → MULTE_IN_GA(T183)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(47) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • MULTE_IN_GA(s(T183)) → MULTE_IN_GA(T183)
    The graph contains the following edges 1 > 1

(48) YES

(49) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

MULTD_IN_GA(s(T119), s(T121)) → MULTD_IN_GA(T119, T121)

The TRS R consists of the following rules:

timesA_in_gga(0, T15, 0) → timesA_out_gga(0, T15, 0)
timesA_in_gga(s(T28), T29, T31) → U1_gga(T28, T29, T31, multB_in_gga(T28, T29, T31))
multB_in_gga(0, 0, 0) → multB_out_gga(0, 0, 0)
multB_in_gga(s(T51), 0, T54) → U12_gga(T51, T54, multC_in_ga(T51, T54))
multC_in_ga(0, 0) → multC_out_ga(0, 0)
multC_in_ga(s(T63), T65) → U2_ga(T63, T65, multC_in_ga(T63, T65))
U2_ga(T63, T65, multC_out_ga(T63, T65)) → multC_out_ga(s(T63), T65)
U12_gga(T51, T54, multC_out_ga(T51, T54)) → multB_out_gga(s(T51), 0, T54)
multB_in_gga(0, s(0), s(0)) → multB_out_gga(0, s(0), s(0))
multB_in_gga(s(T99), s(0), s(T102)) → U13_gga(T99, T102, multD_in_ga(T99, T102))
multD_in_ga(0, s(0)) → multD_out_ga(0, s(0))
multD_in_ga(s(T119), s(T121)) → U3_ga(T119, T121, multD_in_ga(T119, T121))
U3_ga(T119, T121, multD_out_ga(T119, T121)) → multD_out_ga(s(T119), s(T121))
U13_gga(T99, T102, multD_out_ga(T99, T102)) → multB_out_gga(s(T99), s(0), s(T102))
multB_in_gga(0, s(s(0)), s(s(0))) → multB_out_gga(0, s(s(0)), s(s(0)))
multB_in_gga(s(T155), s(s(0)), s(s(T158))) → U14_gga(T155, T158, multE_in_ga(T155, T158))
multE_in_ga(0, s(s(0))) → multE_out_ga(0, s(s(0)))
multE_in_ga(s(T183), s(s(T185))) → U4_ga(T183, T185, multE_in_ga(T183, T185))
U4_ga(T183, T185, multE_out_ga(T183, T185)) → multE_out_ga(s(T183), s(s(T185)))
U14_gga(T155, T158, multE_out_ga(T155, T158)) → multB_out_gga(s(T155), s(s(0)), s(s(T158)))
multB_in_gga(0, s(s(s(0))), s(s(s(0)))) → multB_out_gga(0, s(s(s(0))), s(s(s(0))))
multB_in_gga(s(T219), s(s(s(0))), s(s(s(T222)))) → U15_gga(T219, T222, multF_in_ga(T219, T222))
multF_in_ga(0, s(s(s(0)))) → multF_out_ga(0, s(s(s(0))))
multF_in_ga(s(T255), s(s(s(T257)))) → U5_ga(T255, T257, multF_in_ga(T255, T257))
U5_ga(T255, T257, multF_out_ga(T255, T257)) → multF_out_ga(s(T255), s(s(s(T257))))
U15_gga(T219, T222, multF_out_ga(T219, T222)) → multB_out_gga(s(T219), s(s(s(0))), s(s(s(T222))))
multB_in_gga(0, s(s(s(s(0)))), s(s(s(s(0))))) → multB_out_gga(0, s(s(s(s(0)))), s(s(s(s(0)))))
multB_in_gga(s(T291), s(s(s(s(0)))), s(s(s(s(T294))))) → U16_gga(T291, T294, multG_in_ga(T291, T294))
multG_in_ga(0, s(s(s(s(0))))) → multG_out_ga(0, s(s(s(s(0)))))
multG_in_ga(s(T335), s(s(s(s(T337))))) → U6_ga(T335, T337, multG_in_ga(T335, T337))
U6_ga(T335, T337, multG_out_ga(T335, T337)) → multG_out_ga(s(T335), s(s(s(s(T337)))))
U16_gga(T291, T294, multG_out_ga(T291, T294)) → multB_out_gga(s(T291), s(s(s(s(0)))), s(s(s(s(T294)))))
multB_in_gga(0, s(s(s(s(s(0))))), s(s(s(s(s(0)))))) → multB_out_gga(0, s(s(s(s(s(0))))), s(s(s(s(s(0))))))
multB_in_gga(s(T371), s(s(s(s(s(0))))), s(s(s(s(s(T374)))))) → U17_gga(T371, T374, multH_in_ga(T371, T374))
multH_in_ga(0, s(s(s(s(s(0)))))) → multH_out_ga(0, s(s(s(s(s(0))))))
multH_in_ga(s(T423), s(s(s(s(s(T425)))))) → U7_ga(T423, T425, multH_in_ga(T423, T425))
U7_ga(T423, T425, multH_out_ga(T423, T425)) → multH_out_ga(s(T423), s(s(s(s(s(T425))))))
U17_gga(T371, T374, multH_out_ga(T371, T374)) → multB_out_gga(s(T371), s(s(s(s(s(0))))), s(s(s(s(s(T374))))))
multB_in_gga(0, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(0))))))) → multB_out_gga(0, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(0)))))))
multB_in_gga(s(T459), s(s(s(s(s(s(0)))))), s(s(s(s(s(s(T462))))))) → U18_gga(T459, T462, multI_in_ga(T459, T462))
multI_in_ga(0, s(s(s(s(s(s(0))))))) → multI_out_ga(0, s(s(s(s(s(s(0)))))))
multI_in_ga(s(T519), s(s(s(s(s(s(T521))))))) → U8_ga(T519, T521, multI_in_ga(T519, T521))
U8_ga(T519, T521, multI_out_ga(T519, T521)) → multI_out_ga(s(T519), s(s(s(s(s(s(T521)))))))
U18_gga(T459, T462, multI_out_ga(T459, T462)) → multB_out_gga(s(T459), s(s(s(s(s(s(0)))))), s(s(s(s(s(s(T462)))))))
multB_in_gga(0, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(0)))))))) → multB_out_gga(0, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(0))))))))
multB_in_gga(s(T555), s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(T558)))))))) → U19_gga(T555, T558, multJ_in_ga(T555, T558))
multJ_in_ga(0, s(s(s(s(s(s(s(0)))))))) → multJ_out_ga(0, s(s(s(s(s(s(s(0))))))))
multJ_in_ga(s(T623), s(s(s(s(s(s(s(T625)))))))) → U9_ga(T623, T625, multJ_in_ga(T623, T625))
U9_ga(T623, T625, multJ_out_ga(T623, T625)) → multJ_out_ga(s(T623), s(s(s(s(s(s(s(T625))))))))
U19_gga(T555, T558, multJ_out_ga(T555, T558)) → multB_out_gga(s(T555), s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(T558))))))))
multB_in_gga(T635, s(s(s(s(s(s(s(s(T637)))))))), s(s(s(s(s(s(s(s(T639))))))))) → U20_gga(T635, T637, T639, multK_in_ggga(T635, s(s(s(s(s(s(s(T637))))))), T637, T639))
multK_in_ggga(0, T649, 0, 0) → multK_out_ggga(0, T649, 0, 0)
multK_in_ggga(s(T662), T663, 0, T665) → U10_ggga(T662, T663, T665, multB_in_gga(T662, s(T663), T665))
U10_ggga(T662, T663, T665, multB_out_gga(T662, s(T663), T665)) → multK_out_ggga(s(T662), T663, 0, T665)
multK_in_ggga(T676, T677, s(T678), s(T680)) → U11_ggga(T676, T677, T678, T680, multK_in_ggga(T676, T677, T678, T680))
U11_ggga(T676, T677, T678, T680, multK_out_ggga(T676, T677, T678, T680)) → multK_out_ggga(T676, T677, s(T678), s(T680))
U20_gga(T635, T637, T639, multK_out_ggga(T635, s(s(s(s(s(s(s(T637))))))), T637, T639)) → multB_out_gga(T635, s(s(s(s(s(s(s(s(T637)))))))), s(s(s(s(s(s(s(s(T639)))))))))
U1_gga(T28, T29, T31, multB_out_gga(T28, T29, T31)) → timesA_out_gga(s(T28), T29, T31)

The argument filtering Pi contains the following mapping:
timesA_in_gga(x1, x2, x3)  =  timesA_in_gga(x1, x2)
0  =  0
timesA_out_gga(x1, x2, x3)  =  timesA_out_gga(x1, x2, x3)
s(x1)  =  s(x1)
U1_gga(x1, x2, x3, x4)  =  U1_gga(x1, x2, x4)
multB_in_gga(x1, x2, x3)  =  multB_in_gga(x1, x2)
multB_out_gga(x1, x2, x3)  =  multB_out_gga(x1, x2, x3)
U12_gga(x1, x2, x3)  =  U12_gga(x1, x3)
multC_in_ga(x1, x2)  =  multC_in_ga(x1)
multC_out_ga(x1, x2)  =  multC_out_ga(x1, x2)
U2_ga(x1, x2, x3)  =  U2_ga(x1, x3)
U13_gga(x1, x2, x3)  =  U13_gga(x1, x3)
multD_in_ga(x1, x2)  =  multD_in_ga(x1)
multD_out_ga(x1, x2)  =  multD_out_ga(x1, x2)
U3_ga(x1, x2, x3)  =  U3_ga(x1, x3)
U14_gga(x1, x2, x3)  =  U14_gga(x1, x3)
multE_in_ga(x1, x2)  =  multE_in_ga(x1)
multE_out_ga(x1, x2)  =  multE_out_ga(x1, x2)
U4_ga(x1, x2, x3)  =  U4_ga(x1, x3)
U15_gga(x1, x2, x3)  =  U15_gga(x1, x3)
multF_in_ga(x1, x2)  =  multF_in_ga(x1)
multF_out_ga(x1, x2)  =  multF_out_ga(x1, x2)
U5_ga(x1, x2, x3)  =  U5_ga(x1, x3)
U16_gga(x1, x2, x3)  =  U16_gga(x1, x3)
multG_in_ga(x1, x2)  =  multG_in_ga(x1)
multG_out_ga(x1, x2)  =  multG_out_ga(x1, x2)
U6_ga(x1, x2, x3)  =  U6_ga(x1, x3)
U17_gga(x1, x2, x3)  =  U17_gga(x1, x3)
multH_in_ga(x1, x2)  =  multH_in_ga(x1)
multH_out_ga(x1, x2)  =  multH_out_ga(x1, x2)
U7_ga(x1, x2, x3)  =  U7_ga(x1, x3)
U18_gga(x1, x2, x3)  =  U18_gga(x1, x3)
multI_in_ga(x1, x2)  =  multI_in_ga(x1)
multI_out_ga(x1, x2)  =  multI_out_ga(x1, x2)
U8_ga(x1, x2, x3)  =  U8_ga(x1, x3)
U19_gga(x1, x2, x3)  =  U19_gga(x1, x3)
multJ_in_ga(x1, x2)  =  multJ_in_ga(x1)
multJ_out_ga(x1, x2)  =  multJ_out_ga(x1, x2)
U9_ga(x1, x2, x3)  =  U9_ga(x1, x3)
U20_gga(x1, x2, x3, x4)  =  U20_gga(x1, x2, x4)
multK_in_ggga(x1, x2, x3, x4)  =  multK_in_ggga(x1, x2, x3)
multK_out_ggga(x1, x2, x3, x4)  =  multK_out_ggga(x1, x2, x3, x4)
U10_ggga(x1, x2, x3, x4)  =  U10_ggga(x1, x2, x4)
U11_ggga(x1, x2, x3, x4, x5)  =  U11_ggga(x1, x2, x3, x5)
MULTD_IN_GA(x1, x2)  =  MULTD_IN_GA(x1)

We have to consider all (P,R,Pi)-chains

(50) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(51) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

MULTD_IN_GA(s(T119), s(T121)) → MULTD_IN_GA(T119, T121)

R is empty.
The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
MULTD_IN_GA(x1, x2)  =  MULTD_IN_GA(x1)

We have to consider all (P,R,Pi)-chains

(52) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(53) Obligation:

Q DP problem:
The TRS P consists of the following rules:

MULTD_IN_GA(s(T119)) → MULTD_IN_GA(T119)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(54) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • MULTD_IN_GA(s(T119)) → MULTD_IN_GA(T119)
    The graph contains the following edges 1 > 1

(55) YES

(56) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

MULTB_IN_GGA(T635, s(s(s(s(s(s(s(s(T637)))))))), s(s(s(s(s(s(s(s(T639))))))))) → MULTK_IN_GGGA(T635, s(s(s(s(s(s(s(T637))))))), T637, T639)
MULTK_IN_GGGA(s(T662), T663, 0, T665) → MULTB_IN_GGA(T662, s(T663), T665)
MULTK_IN_GGGA(T676, T677, s(T678), s(T680)) → MULTK_IN_GGGA(T676, T677, T678, T680)

The TRS R consists of the following rules:

timesA_in_gga(0, T15, 0) → timesA_out_gga(0, T15, 0)
timesA_in_gga(s(T28), T29, T31) → U1_gga(T28, T29, T31, multB_in_gga(T28, T29, T31))
multB_in_gga(0, 0, 0) → multB_out_gga(0, 0, 0)
multB_in_gga(s(T51), 0, T54) → U12_gga(T51, T54, multC_in_ga(T51, T54))
multC_in_ga(0, 0) → multC_out_ga(0, 0)
multC_in_ga(s(T63), T65) → U2_ga(T63, T65, multC_in_ga(T63, T65))
U2_ga(T63, T65, multC_out_ga(T63, T65)) → multC_out_ga(s(T63), T65)
U12_gga(T51, T54, multC_out_ga(T51, T54)) → multB_out_gga(s(T51), 0, T54)
multB_in_gga(0, s(0), s(0)) → multB_out_gga(0, s(0), s(0))
multB_in_gga(s(T99), s(0), s(T102)) → U13_gga(T99, T102, multD_in_ga(T99, T102))
multD_in_ga(0, s(0)) → multD_out_ga(0, s(0))
multD_in_ga(s(T119), s(T121)) → U3_ga(T119, T121, multD_in_ga(T119, T121))
U3_ga(T119, T121, multD_out_ga(T119, T121)) → multD_out_ga(s(T119), s(T121))
U13_gga(T99, T102, multD_out_ga(T99, T102)) → multB_out_gga(s(T99), s(0), s(T102))
multB_in_gga(0, s(s(0)), s(s(0))) → multB_out_gga(0, s(s(0)), s(s(0)))
multB_in_gga(s(T155), s(s(0)), s(s(T158))) → U14_gga(T155, T158, multE_in_ga(T155, T158))
multE_in_ga(0, s(s(0))) → multE_out_ga(0, s(s(0)))
multE_in_ga(s(T183), s(s(T185))) → U4_ga(T183, T185, multE_in_ga(T183, T185))
U4_ga(T183, T185, multE_out_ga(T183, T185)) → multE_out_ga(s(T183), s(s(T185)))
U14_gga(T155, T158, multE_out_ga(T155, T158)) → multB_out_gga(s(T155), s(s(0)), s(s(T158)))
multB_in_gga(0, s(s(s(0))), s(s(s(0)))) → multB_out_gga(0, s(s(s(0))), s(s(s(0))))
multB_in_gga(s(T219), s(s(s(0))), s(s(s(T222)))) → U15_gga(T219, T222, multF_in_ga(T219, T222))
multF_in_ga(0, s(s(s(0)))) → multF_out_ga(0, s(s(s(0))))
multF_in_ga(s(T255), s(s(s(T257)))) → U5_ga(T255, T257, multF_in_ga(T255, T257))
U5_ga(T255, T257, multF_out_ga(T255, T257)) → multF_out_ga(s(T255), s(s(s(T257))))
U15_gga(T219, T222, multF_out_ga(T219, T222)) → multB_out_gga(s(T219), s(s(s(0))), s(s(s(T222))))
multB_in_gga(0, s(s(s(s(0)))), s(s(s(s(0))))) → multB_out_gga(0, s(s(s(s(0)))), s(s(s(s(0)))))
multB_in_gga(s(T291), s(s(s(s(0)))), s(s(s(s(T294))))) → U16_gga(T291, T294, multG_in_ga(T291, T294))
multG_in_ga(0, s(s(s(s(0))))) → multG_out_ga(0, s(s(s(s(0)))))
multG_in_ga(s(T335), s(s(s(s(T337))))) → U6_ga(T335, T337, multG_in_ga(T335, T337))
U6_ga(T335, T337, multG_out_ga(T335, T337)) → multG_out_ga(s(T335), s(s(s(s(T337)))))
U16_gga(T291, T294, multG_out_ga(T291, T294)) → multB_out_gga(s(T291), s(s(s(s(0)))), s(s(s(s(T294)))))
multB_in_gga(0, s(s(s(s(s(0))))), s(s(s(s(s(0)))))) → multB_out_gga(0, s(s(s(s(s(0))))), s(s(s(s(s(0))))))
multB_in_gga(s(T371), s(s(s(s(s(0))))), s(s(s(s(s(T374)))))) → U17_gga(T371, T374, multH_in_ga(T371, T374))
multH_in_ga(0, s(s(s(s(s(0)))))) → multH_out_ga(0, s(s(s(s(s(0))))))
multH_in_ga(s(T423), s(s(s(s(s(T425)))))) → U7_ga(T423, T425, multH_in_ga(T423, T425))
U7_ga(T423, T425, multH_out_ga(T423, T425)) → multH_out_ga(s(T423), s(s(s(s(s(T425))))))
U17_gga(T371, T374, multH_out_ga(T371, T374)) → multB_out_gga(s(T371), s(s(s(s(s(0))))), s(s(s(s(s(T374))))))
multB_in_gga(0, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(0))))))) → multB_out_gga(0, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(0)))))))
multB_in_gga(s(T459), s(s(s(s(s(s(0)))))), s(s(s(s(s(s(T462))))))) → U18_gga(T459, T462, multI_in_ga(T459, T462))
multI_in_ga(0, s(s(s(s(s(s(0))))))) → multI_out_ga(0, s(s(s(s(s(s(0)))))))
multI_in_ga(s(T519), s(s(s(s(s(s(T521))))))) → U8_ga(T519, T521, multI_in_ga(T519, T521))
U8_ga(T519, T521, multI_out_ga(T519, T521)) → multI_out_ga(s(T519), s(s(s(s(s(s(T521)))))))
U18_gga(T459, T462, multI_out_ga(T459, T462)) → multB_out_gga(s(T459), s(s(s(s(s(s(0)))))), s(s(s(s(s(s(T462)))))))
multB_in_gga(0, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(0)))))))) → multB_out_gga(0, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(0))))))))
multB_in_gga(s(T555), s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(T558)))))))) → U19_gga(T555, T558, multJ_in_ga(T555, T558))
multJ_in_ga(0, s(s(s(s(s(s(s(0)))))))) → multJ_out_ga(0, s(s(s(s(s(s(s(0))))))))
multJ_in_ga(s(T623), s(s(s(s(s(s(s(T625)))))))) → U9_ga(T623, T625, multJ_in_ga(T623, T625))
U9_ga(T623, T625, multJ_out_ga(T623, T625)) → multJ_out_ga(s(T623), s(s(s(s(s(s(s(T625))))))))
U19_gga(T555, T558, multJ_out_ga(T555, T558)) → multB_out_gga(s(T555), s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(T558))))))))
multB_in_gga(T635, s(s(s(s(s(s(s(s(T637)))))))), s(s(s(s(s(s(s(s(T639))))))))) → U20_gga(T635, T637, T639, multK_in_ggga(T635, s(s(s(s(s(s(s(T637))))))), T637, T639))
multK_in_ggga(0, T649, 0, 0) → multK_out_ggga(0, T649, 0, 0)
multK_in_ggga(s(T662), T663, 0, T665) → U10_ggga(T662, T663, T665, multB_in_gga(T662, s(T663), T665))
U10_ggga(T662, T663, T665, multB_out_gga(T662, s(T663), T665)) → multK_out_ggga(s(T662), T663, 0, T665)
multK_in_ggga(T676, T677, s(T678), s(T680)) → U11_ggga(T676, T677, T678, T680, multK_in_ggga(T676, T677, T678, T680))
U11_ggga(T676, T677, T678, T680, multK_out_ggga(T676, T677, T678, T680)) → multK_out_ggga(T676, T677, s(T678), s(T680))
U20_gga(T635, T637, T639, multK_out_ggga(T635, s(s(s(s(s(s(s(T637))))))), T637, T639)) → multB_out_gga(T635, s(s(s(s(s(s(s(s(T637)))))))), s(s(s(s(s(s(s(s(T639)))))))))
U1_gga(T28, T29, T31, multB_out_gga(T28, T29, T31)) → timesA_out_gga(s(T28), T29, T31)

The argument filtering Pi contains the following mapping:
timesA_in_gga(x1, x2, x3)  =  timesA_in_gga(x1, x2)
0  =  0
timesA_out_gga(x1, x2, x3)  =  timesA_out_gga(x1, x2, x3)
s(x1)  =  s(x1)
U1_gga(x1, x2, x3, x4)  =  U1_gga(x1, x2, x4)
multB_in_gga(x1, x2, x3)  =  multB_in_gga(x1, x2)
multB_out_gga(x1, x2, x3)  =  multB_out_gga(x1, x2, x3)
U12_gga(x1, x2, x3)  =  U12_gga(x1, x3)
multC_in_ga(x1, x2)  =  multC_in_ga(x1)
multC_out_ga(x1, x2)  =  multC_out_ga(x1, x2)
U2_ga(x1, x2, x3)  =  U2_ga(x1, x3)
U13_gga(x1, x2, x3)  =  U13_gga(x1, x3)
multD_in_ga(x1, x2)  =  multD_in_ga(x1)
multD_out_ga(x1, x2)  =  multD_out_ga(x1, x2)
U3_ga(x1, x2, x3)  =  U3_ga(x1, x3)
U14_gga(x1, x2, x3)  =  U14_gga(x1, x3)
multE_in_ga(x1, x2)  =  multE_in_ga(x1)
multE_out_ga(x1, x2)  =  multE_out_ga(x1, x2)
U4_ga(x1, x2, x3)  =  U4_ga(x1, x3)
U15_gga(x1, x2, x3)  =  U15_gga(x1, x3)
multF_in_ga(x1, x2)  =  multF_in_ga(x1)
multF_out_ga(x1, x2)  =  multF_out_ga(x1, x2)
U5_ga(x1, x2, x3)  =  U5_ga(x1, x3)
U16_gga(x1, x2, x3)  =  U16_gga(x1, x3)
multG_in_ga(x1, x2)  =  multG_in_ga(x1)
multG_out_ga(x1, x2)  =  multG_out_ga(x1, x2)
U6_ga(x1, x2, x3)  =  U6_ga(x1, x3)
U17_gga(x1, x2, x3)  =  U17_gga(x1, x3)
multH_in_ga(x1, x2)  =  multH_in_ga(x1)
multH_out_ga(x1, x2)  =  multH_out_ga(x1, x2)
U7_ga(x1, x2, x3)  =  U7_ga(x1, x3)
U18_gga(x1, x2, x3)  =  U18_gga(x1, x3)
multI_in_ga(x1, x2)  =  multI_in_ga(x1)
multI_out_ga(x1, x2)  =  multI_out_ga(x1, x2)
U8_ga(x1, x2, x3)  =  U8_ga(x1, x3)
U19_gga(x1, x2, x3)  =  U19_gga(x1, x3)
multJ_in_ga(x1, x2)  =  multJ_in_ga(x1)
multJ_out_ga(x1, x2)  =  multJ_out_ga(x1, x2)
U9_ga(x1, x2, x3)  =  U9_ga(x1, x3)
U20_gga(x1, x2, x3, x4)  =  U20_gga(x1, x2, x4)
multK_in_ggga(x1, x2, x3, x4)  =  multK_in_ggga(x1, x2, x3)
multK_out_ggga(x1, x2, x3, x4)  =  multK_out_ggga(x1, x2, x3, x4)
U10_ggga(x1, x2, x3, x4)  =  U10_ggga(x1, x2, x4)
U11_ggga(x1, x2, x3, x4, x5)  =  U11_ggga(x1, x2, x3, x5)
MULTB_IN_GGA(x1, x2, x3)  =  MULTB_IN_GGA(x1, x2)
MULTK_IN_GGGA(x1, x2, x3, x4)  =  MULTK_IN_GGGA(x1, x2, x3)

We have to consider all (P,R,Pi)-chains

(57) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(58) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

MULTB_IN_GGA(T635, s(s(s(s(s(s(s(s(T637)))))))), s(s(s(s(s(s(s(s(T639))))))))) → MULTK_IN_GGGA(T635, s(s(s(s(s(s(s(T637))))))), T637, T639)
MULTK_IN_GGGA(s(T662), T663, 0, T665) → MULTB_IN_GGA(T662, s(T663), T665)
MULTK_IN_GGGA(T676, T677, s(T678), s(T680)) → MULTK_IN_GGGA(T676, T677, T678, T680)

R is empty.
The argument filtering Pi contains the following mapping:
0  =  0
s(x1)  =  s(x1)
MULTB_IN_GGA(x1, x2, x3)  =  MULTB_IN_GGA(x1, x2)
MULTK_IN_GGGA(x1, x2, x3, x4)  =  MULTK_IN_GGGA(x1, x2, x3)

We have to consider all (P,R,Pi)-chains

(59) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(60) Obligation:

Q DP problem:
The TRS P consists of the following rules:

MULTB_IN_GGA(T635, s(s(s(s(s(s(s(s(T637))))))))) → MULTK_IN_GGGA(T635, s(s(s(s(s(s(s(T637))))))), T637)
MULTK_IN_GGGA(s(T662), T663, 0) → MULTB_IN_GGA(T662, s(T663))
MULTK_IN_GGGA(T676, T677, s(T678)) → MULTK_IN_GGGA(T676, T677, T678)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(61) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • MULTK_IN_GGGA(s(T662), T663, 0) → MULTB_IN_GGA(T662, s(T663))
    The graph contains the following edges 1 > 1

  • MULTK_IN_GGGA(T676, T677, s(T678)) → MULTK_IN_GGGA(T676, T677, T678)
    The graph contains the following edges 1 >= 1, 2 >= 2, 3 > 3

  • MULTB_IN_GGA(T635, s(s(s(s(s(s(s(s(T637))))))))) → MULTK_IN_GGGA(T635, s(s(s(s(s(s(s(T637))))))), T637)
    The graph contains the following edges 1 >= 1, 2 > 2, 2 > 3

(62) YES

(63) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

MULTC_IN_GA(s(T63), T65) → MULTC_IN_GA(T63, T65)

The TRS R consists of the following rules:

timesA_in_gga(0, T15, 0) → timesA_out_gga(0, T15, 0)
timesA_in_gga(s(T28), T29, T31) → U1_gga(T28, T29, T31, multB_in_gga(T28, T29, T31))
multB_in_gga(0, 0, 0) → multB_out_gga(0, 0, 0)
multB_in_gga(s(T51), 0, T54) → U12_gga(T51, T54, multC_in_ga(T51, T54))
multC_in_ga(0, 0) → multC_out_ga(0, 0)
multC_in_ga(s(T63), T65) → U2_ga(T63, T65, multC_in_ga(T63, T65))
U2_ga(T63, T65, multC_out_ga(T63, T65)) → multC_out_ga(s(T63), T65)
U12_gga(T51, T54, multC_out_ga(T51, T54)) → multB_out_gga(s(T51), 0, T54)
multB_in_gga(0, s(0), s(0)) → multB_out_gga(0, s(0), s(0))
multB_in_gga(s(T99), s(0), s(T102)) → U13_gga(T99, T102, multD_in_ga(T99, T102))
multD_in_ga(0, s(0)) → multD_out_ga(0, s(0))
multD_in_ga(s(T119), s(T121)) → U3_ga(T119, T121, multD_in_ga(T119, T121))
U3_ga(T119, T121, multD_out_ga(T119, T121)) → multD_out_ga(s(T119), s(T121))
U13_gga(T99, T102, multD_out_ga(T99, T102)) → multB_out_gga(s(T99), s(0), s(T102))
multB_in_gga(0, s(s(0)), s(s(0))) → multB_out_gga(0, s(s(0)), s(s(0)))
multB_in_gga(s(T155), s(s(0)), s(s(T158))) → U14_gga(T155, T158, multE_in_ga(T155, T158))
multE_in_ga(0, s(s(0))) → multE_out_ga(0, s(s(0)))
multE_in_ga(s(T183), s(s(T185))) → U4_ga(T183, T185, multE_in_ga(T183, T185))
U4_ga(T183, T185, multE_out_ga(T183, T185)) → multE_out_ga(s(T183), s(s(T185)))
U14_gga(T155, T158, multE_out_ga(T155, T158)) → multB_out_gga(s(T155), s(s(0)), s(s(T158)))
multB_in_gga(0, s(s(s(0))), s(s(s(0)))) → multB_out_gga(0, s(s(s(0))), s(s(s(0))))
multB_in_gga(s(T219), s(s(s(0))), s(s(s(T222)))) → U15_gga(T219, T222, multF_in_ga(T219, T222))
multF_in_ga(0, s(s(s(0)))) → multF_out_ga(0, s(s(s(0))))
multF_in_ga(s(T255), s(s(s(T257)))) → U5_ga(T255, T257, multF_in_ga(T255, T257))
U5_ga(T255, T257, multF_out_ga(T255, T257)) → multF_out_ga(s(T255), s(s(s(T257))))
U15_gga(T219, T222, multF_out_ga(T219, T222)) → multB_out_gga(s(T219), s(s(s(0))), s(s(s(T222))))
multB_in_gga(0, s(s(s(s(0)))), s(s(s(s(0))))) → multB_out_gga(0, s(s(s(s(0)))), s(s(s(s(0)))))
multB_in_gga(s(T291), s(s(s(s(0)))), s(s(s(s(T294))))) → U16_gga(T291, T294, multG_in_ga(T291, T294))
multG_in_ga(0, s(s(s(s(0))))) → multG_out_ga(0, s(s(s(s(0)))))
multG_in_ga(s(T335), s(s(s(s(T337))))) → U6_ga(T335, T337, multG_in_ga(T335, T337))
U6_ga(T335, T337, multG_out_ga(T335, T337)) → multG_out_ga(s(T335), s(s(s(s(T337)))))
U16_gga(T291, T294, multG_out_ga(T291, T294)) → multB_out_gga(s(T291), s(s(s(s(0)))), s(s(s(s(T294)))))
multB_in_gga(0, s(s(s(s(s(0))))), s(s(s(s(s(0)))))) → multB_out_gga(0, s(s(s(s(s(0))))), s(s(s(s(s(0))))))
multB_in_gga(s(T371), s(s(s(s(s(0))))), s(s(s(s(s(T374)))))) → U17_gga(T371, T374, multH_in_ga(T371, T374))
multH_in_ga(0, s(s(s(s(s(0)))))) → multH_out_ga(0, s(s(s(s(s(0))))))
multH_in_ga(s(T423), s(s(s(s(s(T425)))))) → U7_ga(T423, T425, multH_in_ga(T423, T425))
U7_ga(T423, T425, multH_out_ga(T423, T425)) → multH_out_ga(s(T423), s(s(s(s(s(T425))))))
U17_gga(T371, T374, multH_out_ga(T371, T374)) → multB_out_gga(s(T371), s(s(s(s(s(0))))), s(s(s(s(s(T374))))))
multB_in_gga(0, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(0))))))) → multB_out_gga(0, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(0)))))))
multB_in_gga(s(T459), s(s(s(s(s(s(0)))))), s(s(s(s(s(s(T462))))))) → U18_gga(T459, T462, multI_in_ga(T459, T462))
multI_in_ga(0, s(s(s(s(s(s(0))))))) → multI_out_ga(0, s(s(s(s(s(s(0)))))))
multI_in_ga(s(T519), s(s(s(s(s(s(T521))))))) → U8_ga(T519, T521, multI_in_ga(T519, T521))
U8_ga(T519, T521, multI_out_ga(T519, T521)) → multI_out_ga(s(T519), s(s(s(s(s(s(T521)))))))
U18_gga(T459, T462, multI_out_ga(T459, T462)) → multB_out_gga(s(T459), s(s(s(s(s(s(0)))))), s(s(s(s(s(s(T462)))))))
multB_in_gga(0, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(0)))))))) → multB_out_gga(0, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(0))))))))
multB_in_gga(s(T555), s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(T558)))))))) → U19_gga(T555, T558, multJ_in_ga(T555, T558))
multJ_in_ga(0, s(s(s(s(s(s(s(0)))))))) → multJ_out_ga(0, s(s(s(s(s(s(s(0))))))))
multJ_in_ga(s(T623), s(s(s(s(s(s(s(T625)))))))) → U9_ga(T623, T625, multJ_in_ga(T623, T625))
U9_ga(T623, T625, multJ_out_ga(T623, T625)) → multJ_out_ga(s(T623), s(s(s(s(s(s(s(T625))))))))
U19_gga(T555, T558, multJ_out_ga(T555, T558)) → multB_out_gga(s(T555), s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(T558))))))))
multB_in_gga(T635, s(s(s(s(s(s(s(s(T637)))))))), s(s(s(s(s(s(s(s(T639))))))))) → U20_gga(T635, T637, T639, multK_in_ggga(T635, s(s(s(s(s(s(s(T637))))))), T637, T639))
multK_in_ggga(0, T649, 0, 0) → multK_out_ggga(0, T649, 0, 0)
multK_in_ggga(s(T662), T663, 0, T665) → U10_ggga(T662, T663, T665, multB_in_gga(T662, s(T663), T665))
U10_ggga(T662, T663, T665, multB_out_gga(T662, s(T663), T665)) → multK_out_ggga(s(T662), T663, 0, T665)
multK_in_ggga(T676, T677, s(T678), s(T680)) → U11_ggga(T676, T677, T678, T680, multK_in_ggga(T676, T677, T678, T680))
U11_ggga(T676, T677, T678, T680, multK_out_ggga(T676, T677, T678, T680)) → multK_out_ggga(T676, T677, s(T678), s(T680))
U20_gga(T635, T637, T639, multK_out_ggga(T635, s(s(s(s(s(s(s(T637))))))), T637, T639)) → multB_out_gga(T635, s(s(s(s(s(s(s(s(T637)))))))), s(s(s(s(s(s(s(s(T639)))))))))
U1_gga(T28, T29, T31, multB_out_gga(T28, T29, T31)) → timesA_out_gga(s(T28), T29, T31)

The argument filtering Pi contains the following mapping:
timesA_in_gga(x1, x2, x3)  =  timesA_in_gga(x1, x2)
0  =  0
timesA_out_gga(x1, x2, x3)  =  timesA_out_gga(x1, x2, x3)
s(x1)  =  s(x1)
U1_gga(x1, x2, x3, x4)  =  U1_gga(x1, x2, x4)
multB_in_gga(x1, x2, x3)  =  multB_in_gga(x1, x2)
multB_out_gga(x1, x2, x3)  =  multB_out_gga(x1, x2, x3)
U12_gga(x1, x2, x3)  =  U12_gga(x1, x3)
multC_in_ga(x1, x2)  =  multC_in_ga(x1)
multC_out_ga(x1, x2)  =  multC_out_ga(x1, x2)
U2_ga(x1, x2, x3)  =  U2_ga(x1, x3)
U13_gga(x1, x2, x3)  =  U13_gga(x1, x3)
multD_in_ga(x1, x2)  =  multD_in_ga(x1)
multD_out_ga(x1, x2)  =  multD_out_ga(x1, x2)
U3_ga(x1, x2, x3)  =  U3_ga(x1, x3)
U14_gga(x1, x2, x3)  =  U14_gga(x1, x3)
multE_in_ga(x1, x2)  =  multE_in_ga(x1)
multE_out_ga(x1, x2)  =  multE_out_ga(x1, x2)
U4_ga(x1, x2, x3)  =  U4_ga(x1, x3)
U15_gga(x1, x2, x3)  =  U15_gga(x1, x3)
multF_in_ga(x1, x2)  =  multF_in_ga(x1)
multF_out_ga(x1, x2)  =  multF_out_ga(x1, x2)
U5_ga(x1, x2, x3)  =  U5_ga(x1, x3)
U16_gga(x1, x2, x3)  =  U16_gga(x1, x3)
multG_in_ga(x1, x2)  =  multG_in_ga(x1)
multG_out_ga(x1, x2)  =  multG_out_ga(x1, x2)
U6_ga(x1, x2, x3)  =  U6_ga(x1, x3)
U17_gga(x1, x2, x3)  =  U17_gga(x1, x3)
multH_in_ga(x1, x2)  =  multH_in_ga(x1)
multH_out_ga(x1, x2)  =  multH_out_ga(x1, x2)
U7_ga(x1, x2, x3)  =  U7_ga(x1, x3)
U18_gga(x1, x2, x3)  =  U18_gga(x1, x3)
multI_in_ga(x1, x2)  =  multI_in_ga(x1)
multI_out_ga(x1, x2)  =  multI_out_ga(x1, x2)
U8_ga(x1, x2, x3)  =  U8_ga(x1, x3)
U19_gga(x1, x2, x3)  =  U19_gga(x1, x3)
multJ_in_ga(x1, x2)  =  multJ_in_ga(x1)
multJ_out_ga(x1, x2)  =  multJ_out_ga(x1, x2)
U9_ga(x1, x2, x3)  =  U9_ga(x1, x3)
U20_gga(x1, x2, x3, x4)  =  U20_gga(x1, x2, x4)
multK_in_ggga(x1, x2, x3, x4)  =  multK_in_ggga(x1, x2, x3)
multK_out_ggga(x1, x2, x3, x4)  =  multK_out_ggga(x1, x2, x3, x4)
U10_ggga(x1, x2, x3, x4)  =  U10_ggga(x1, x2, x4)
U11_ggga(x1, x2, x3, x4, x5)  =  U11_ggga(x1, x2, x3, x5)
MULTC_IN_GA(x1, x2)  =  MULTC_IN_GA(x1)

We have to consider all (P,R,Pi)-chains

(64) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(65) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

MULTC_IN_GA(s(T63), T65) → MULTC_IN_GA(T63, T65)

R is empty.
The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
MULTC_IN_GA(x1, x2)  =  MULTC_IN_GA(x1)

We have to consider all (P,R,Pi)-chains

(66) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(67) Obligation:

Q DP problem:
The TRS P consists of the following rules:

MULTC_IN_GA(s(T63)) → MULTC_IN_GA(T63)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(68) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • MULTC_IN_GA(s(T63)) → MULTC_IN_GA(T63)
    The graph contains the following edges 1 > 1

(69) YES