(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).

Queries:

times(g,g,a).

(1) PrologToPrologProblemTransformerProof (SOUND transformation)

Built Prolog problem from termination graph.

(2) Obligation:

Clauses:

mult22(0, 0).
mult22(s(T63), T65) :- mult22(T63, T65).
mult45(0, s(0)).
mult45(s(T122), s(T124)) :- mult45(T122, T124).
mult73(0, s(s(0))).
mult73(s(T195), s(s(T197))) :- mult73(T195, T197).
mult106(0, s(s(s(0)))).
mult106(s(T279), s(s(s(T281)))) :- mult106(T279, T281).
mult144(0, s(s(s(s(0))))).
mult144(s(T374), s(s(s(s(T376))))) :- mult144(T374, T376).
mult187(0, s(s(s(s(s(0)))))).
mult187(s(T480), s(s(s(s(s(T482)))))) :- mult187(T480, T482).
mult235(0, s(s(s(s(s(s(0))))))).
mult235(s(T597), s(s(s(s(s(s(T599))))))) :- mult235(T597, T599).
mult288(0, s(s(s(s(s(s(s(0)))))))).
mult288(s(T725), s(s(s(s(s(s(s(T727)))))))) :- mult288(T725, T727).
mult12(0, 0, 0).
mult12(s(T51), 0, T54) :- mult22(T51, T54).
mult12(0, s(0), s(0)).
mult12(s(T99), s(0), s(T102)) :- mult45(T99, T102).
mult12(0, s(s(0)), s(s(0))).
mult12(s(T161), s(s(0)), s(s(T164))) :- mult73(T161, T164).
mult12(0, s(s(s(0))), s(s(s(0)))).
mult12(s(T234), s(s(s(0))), s(s(s(T237)))) :- mult106(T234, T237).
mult12(0, s(s(s(s(0)))), s(s(s(s(0))))).
mult12(s(T318), s(s(s(s(0)))), s(s(s(s(T321))))) :- mult144(T318, T321).
mult12(0, s(s(s(s(s(0))))), s(s(s(s(s(0)))))).
mult12(s(T413), s(s(s(s(s(0))))), s(s(s(s(s(T416)))))) :- mult187(T413, T416).
mult12(0, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(0))))))).
mult12(s(T519), s(s(s(s(s(s(0)))))), s(s(s(s(s(s(T522))))))) :- mult235(T519, T522).
mult12(0, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(0)))))))).
mult12(s(T636), s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(T639)))))))) :- mult288(T636, T639).
mult12(T740, s(s(s(s(s(s(s(s(T742)))))))), s(s(s(s(s(s(s(s(T744))))))))) :- mult338(T740, s(s(s(s(s(s(s(T742))))))), T742, T744).
mult338(0, T754, 0, 0).
mult338(s(T767), T768, 0, T770) :- mult12(T767, s(T768), T770).
mult338(T786, T787, s(T788), s(T790)) :- mult338(T786, T787, T788, T790).
times1(0, T15, 0).
times1(s(T28), T29, T31) :- mult12(T28, T29, T31).

Queries:

times1(g,g,a).

(3) PrologToPiTRSProof (SOUND transformation)

We use the technique of [LOPSTR]. With regard to the inferred argument filtering the predicates were used in the following modes:
times1_in: (b,b,f)
mult12_in: (b,b,f)
mult22_in: (b,f)
mult45_in: (b,f)
mult73_in: (b,f)
mult106_in: (b,f)
mult144_in: (b,f)
mult187_in: (b,f)
mult235_in: (b,f)
mult288_in: (b,f)
mult338_in: (b,b,b,f)
Transforming Prolog into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:

times1_in_gga(0, T15, 0) → times1_out_gga(0, T15, 0)
times1_in_gga(s(T28), T29, T31) → U20_gga(T28, T29, T31, mult12_in_gga(T28, T29, T31))
mult12_in_gga(0, 0, 0) → mult12_out_gga(0, 0, 0)
mult12_in_gga(s(T51), 0, T54) → U9_gga(T51, T54, mult22_in_ga(T51, T54))
mult22_in_ga(0, 0) → mult22_out_ga(0, 0)
mult22_in_ga(s(T63), T65) → U1_ga(T63, T65, mult22_in_ga(T63, T65))
U1_ga(T63, T65, mult22_out_ga(T63, T65)) → mult22_out_ga(s(T63), T65)
U9_gga(T51, T54, mult22_out_ga(T51, T54)) → mult12_out_gga(s(T51), 0, T54)
mult12_in_gga(0, s(0), s(0)) → mult12_out_gga(0, s(0), s(0))
mult12_in_gga(s(T99), s(0), s(T102)) → U10_gga(T99, T102, mult45_in_ga(T99, T102))
mult45_in_ga(0, s(0)) → mult45_out_ga(0, s(0))
mult45_in_ga(s(T122), s(T124)) → U2_ga(T122, T124, mult45_in_ga(T122, T124))
U2_ga(T122, T124, mult45_out_ga(T122, T124)) → mult45_out_ga(s(T122), s(T124))
U10_gga(T99, T102, mult45_out_ga(T99, T102)) → mult12_out_gga(s(T99), s(0), s(T102))
mult12_in_gga(0, s(s(0)), s(s(0))) → mult12_out_gga(0, s(s(0)), s(s(0)))
mult12_in_gga(s(T161), s(s(0)), s(s(T164))) → U11_gga(T161, T164, mult73_in_ga(T161, T164))
mult73_in_ga(0, s(s(0))) → mult73_out_ga(0, s(s(0)))
mult73_in_ga(s(T195), s(s(T197))) → U3_ga(T195, T197, mult73_in_ga(T195, T197))
U3_ga(T195, T197, mult73_out_ga(T195, T197)) → mult73_out_ga(s(T195), s(s(T197)))
U11_gga(T161, T164, mult73_out_ga(T161, T164)) → mult12_out_gga(s(T161), s(s(0)), s(s(T164)))
mult12_in_gga(0, s(s(s(0))), s(s(s(0)))) → mult12_out_gga(0, s(s(s(0))), s(s(s(0))))
mult12_in_gga(s(T234), s(s(s(0))), s(s(s(T237)))) → U12_gga(T234, T237, mult106_in_ga(T234, T237))
mult106_in_ga(0, s(s(s(0)))) → mult106_out_ga(0, s(s(s(0))))
mult106_in_ga(s(T279), s(s(s(T281)))) → U4_ga(T279, T281, mult106_in_ga(T279, T281))
U4_ga(T279, T281, mult106_out_ga(T279, T281)) → mult106_out_ga(s(T279), s(s(s(T281))))
U12_gga(T234, T237, mult106_out_ga(T234, T237)) → mult12_out_gga(s(T234), s(s(s(0))), s(s(s(T237))))
mult12_in_gga(0, s(s(s(s(0)))), s(s(s(s(0))))) → mult12_out_gga(0, s(s(s(s(0)))), s(s(s(s(0)))))
mult12_in_gga(s(T318), s(s(s(s(0)))), s(s(s(s(T321))))) → U13_gga(T318, T321, mult144_in_ga(T318, T321))
mult144_in_ga(0, s(s(s(s(0))))) → mult144_out_ga(0, s(s(s(s(0)))))
mult144_in_ga(s(T374), s(s(s(s(T376))))) → U5_ga(T374, T376, mult144_in_ga(T374, T376))
U5_ga(T374, T376, mult144_out_ga(T374, T376)) → mult144_out_ga(s(T374), s(s(s(s(T376)))))
U13_gga(T318, T321, mult144_out_ga(T318, T321)) → mult12_out_gga(s(T318), s(s(s(s(0)))), s(s(s(s(T321)))))
mult12_in_gga(0, s(s(s(s(s(0))))), s(s(s(s(s(0)))))) → mult12_out_gga(0, s(s(s(s(s(0))))), s(s(s(s(s(0))))))
mult12_in_gga(s(T413), s(s(s(s(s(0))))), s(s(s(s(s(T416)))))) → U14_gga(T413, T416, mult187_in_ga(T413, T416))
mult187_in_ga(0, s(s(s(s(s(0)))))) → mult187_out_ga(0, s(s(s(s(s(0))))))
mult187_in_ga(s(T480), s(s(s(s(s(T482)))))) → U6_ga(T480, T482, mult187_in_ga(T480, T482))
U6_ga(T480, T482, mult187_out_ga(T480, T482)) → mult187_out_ga(s(T480), s(s(s(s(s(T482))))))
U14_gga(T413, T416, mult187_out_ga(T413, T416)) → mult12_out_gga(s(T413), s(s(s(s(s(0))))), s(s(s(s(s(T416))))))
mult12_in_gga(0, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(0))))))) → mult12_out_gga(0, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(0)))))))
mult12_in_gga(s(T519), s(s(s(s(s(s(0)))))), s(s(s(s(s(s(T522))))))) → U15_gga(T519, T522, mult235_in_ga(T519, T522))
mult235_in_ga(0, s(s(s(s(s(s(0))))))) → mult235_out_ga(0, s(s(s(s(s(s(0)))))))
mult235_in_ga(s(T597), s(s(s(s(s(s(T599))))))) → U7_ga(T597, T599, mult235_in_ga(T597, T599))
U7_ga(T597, T599, mult235_out_ga(T597, T599)) → mult235_out_ga(s(T597), s(s(s(s(s(s(T599)))))))
U15_gga(T519, T522, mult235_out_ga(T519, T522)) → mult12_out_gga(s(T519), s(s(s(s(s(s(0)))))), s(s(s(s(s(s(T522)))))))
mult12_in_gga(0, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(0)))))))) → mult12_out_gga(0, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(0))))))))
mult12_in_gga(s(T636), s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(T639)))))))) → U16_gga(T636, T639, mult288_in_ga(T636, T639))
mult288_in_ga(0, s(s(s(s(s(s(s(0)))))))) → mult288_out_ga(0, s(s(s(s(s(s(s(0))))))))
mult288_in_ga(s(T725), s(s(s(s(s(s(s(T727)))))))) → U8_ga(T725, T727, mult288_in_ga(T725, T727))
U8_ga(T725, T727, mult288_out_ga(T725, T727)) → mult288_out_ga(s(T725), s(s(s(s(s(s(s(T727))))))))
U16_gga(T636, T639, mult288_out_ga(T636, T639)) → mult12_out_gga(s(T636), s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(T639))))))))
mult12_in_gga(T740, s(s(s(s(s(s(s(s(T742)))))))), s(s(s(s(s(s(s(s(T744))))))))) → U17_gga(T740, T742, T744, mult338_in_ggga(T740, s(s(s(s(s(s(s(T742))))))), T742, T744))
mult338_in_ggga(0, T754, 0, 0) → mult338_out_ggga(0, T754, 0, 0)
mult338_in_ggga(s(T767), T768, 0, T770) → U18_ggga(T767, T768, T770, mult12_in_gga(T767, s(T768), T770))
U18_ggga(T767, T768, T770, mult12_out_gga(T767, s(T768), T770)) → mult338_out_ggga(s(T767), T768, 0, T770)
mult338_in_ggga(T786, T787, s(T788), s(T790)) → U19_ggga(T786, T787, T788, T790, mult338_in_ggga(T786, T787, T788, T790))
U19_ggga(T786, T787, T788, T790, mult338_out_ggga(T786, T787, T788, T790)) → mult338_out_ggga(T786, T787, s(T788), s(T790))
U17_gga(T740, T742, T744, mult338_out_ggga(T740, s(s(s(s(s(s(s(T742))))))), T742, T744)) → mult12_out_gga(T740, s(s(s(s(s(s(s(s(T742)))))))), s(s(s(s(s(s(s(s(T744)))))))))
U20_gga(T28, T29, T31, mult12_out_gga(T28, T29, T31)) → times1_out_gga(s(T28), T29, T31)

The argument filtering Pi contains the following mapping:
times1_in_gga(x1, x2, x3)  =  times1_in_gga(x1, x2)
0  =  0
times1_out_gga(x1, x2, x3)  =  times1_out_gga(x3)
s(x1)  =  s(x1)
U20_gga(x1, x2, x3, x4)  =  U20_gga(x4)
mult12_in_gga(x1, x2, x3)  =  mult12_in_gga(x1, x2)
mult12_out_gga(x1, x2, x3)  =  mult12_out_gga(x3)
U9_gga(x1, x2, x3)  =  U9_gga(x3)
mult22_in_ga(x1, x2)  =  mult22_in_ga(x1)
mult22_out_ga(x1, x2)  =  mult22_out_ga(x2)
U1_ga(x1, x2, x3)  =  U1_ga(x3)
U10_gga(x1, x2, x3)  =  U10_gga(x3)
mult45_in_ga(x1, x2)  =  mult45_in_ga(x1)
mult45_out_ga(x1, x2)  =  mult45_out_ga(x2)
U2_ga(x1, x2, x3)  =  U2_ga(x3)
U11_gga(x1, x2, x3)  =  U11_gga(x3)
mult73_in_ga(x1, x2)  =  mult73_in_ga(x1)
mult73_out_ga(x1, x2)  =  mult73_out_ga(x2)
U3_ga(x1, x2, x3)  =  U3_ga(x3)
U12_gga(x1, x2, x3)  =  U12_gga(x3)
mult106_in_ga(x1, x2)  =  mult106_in_ga(x1)
mult106_out_ga(x1, x2)  =  mult106_out_ga(x2)
U4_ga(x1, x2, x3)  =  U4_ga(x3)
U13_gga(x1, x2, x3)  =  U13_gga(x3)
mult144_in_ga(x1, x2)  =  mult144_in_ga(x1)
mult144_out_ga(x1, x2)  =  mult144_out_ga(x2)
U5_ga(x1, x2, x3)  =  U5_ga(x3)
U14_gga(x1, x2, x3)  =  U14_gga(x3)
mult187_in_ga(x1, x2)  =  mult187_in_ga(x1)
mult187_out_ga(x1, x2)  =  mult187_out_ga(x2)
U6_ga(x1, x2, x3)  =  U6_ga(x3)
U15_gga(x1, x2, x3)  =  U15_gga(x3)
mult235_in_ga(x1, x2)  =  mult235_in_ga(x1)
mult235_out_ga(x1, x2)  =  mult235_out_ga(x2)
U7_ga(x1, x2, x3)  =  U7_ga(x3)
U16_gga(x1, x2, x3)  =  U16_gga(x3)
mult288_in_ga(x1, x2)  =  mult288_in_ga(x1)
mult288_out_ga(x1, x2)  =  mult288_out_ga(x2)
U8_ga(x1, x2, x3)  =  U8_ga(x3)
U17_gga(x1, x2, x3, x4)  =  U17_gga(x4)
mult338_in_ggga(x1, x2, x3, x4)  =  mult338_in_ggga(x1, x2, x3)
mult338_out_ggga(x1, x2, x3, x4)  =  mult338_out_ggga(x4)
U18_ggga(x1, x2, x3, x4)  =  U18_ggga(x4)
U19_ggga(x1, x2, x3, x4, x5)  =  U19_ggga(x5)

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog

(4) Obligation:

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

times1_in_gga(0, T15, 0) → times1_out_gga(0, T15, 0)
times1_in_gga(s(T28), T29, T31) → U20_gga(T28, T29, T31, mult12_in_gga(T28, T29, T31))
mult12_in_gga(0, 0, 0) → mult12_out_gga(0, 0, 0)
mult12_in_gga(s(T51), 0, T54) → U9_gga(T51, T54, mult22_in_ga(T51, T54))
mult22_in_ga(0, 0) → mult22_out_ga(0, 0)
mult22_in_ga(s(T63), T65) → U1_ga(T63, T65, mult22_in_ga(T63, T65))
U1_ga(T63, T65, mult22_out_ga(T63, T65)) → mult22_out_ga(s(T63), T65)
U9_gga(T51, T54, mult22_out_ga(T51, T54)) → mult12_out_gga(s(T51), 0, T54)
mult12_in_gga(0, s(0), s(0)) → mult12_out_gga(0, s(0), s(0))
mult12_in_gga(s(T99), s(0), s(T102)) → U10_gga(T99, T102, mult45_in_ga(T99, T102))
mult45_in_ga(0, s(0)) → mult45_out_ga(0, s(0))
mult45_in_ga(s(T122), s(T124)) → U2_ga(T122, T124, mult45_in_ga(T122, T124))
U2_ga(T122, T124, mult45_out_ga(T122, T124)) → mult45_out_ga(s(T122), s(T124))
U10_gga(T99, T102, mult45_out_ga(T99, T102)) → mult12_out_gga(s(T99), s(0), s(T102))
mult12_in_gga(0, s(s(0)), s(s(0))) → mult12_out_gga(0, s(s(0)), s(s(0)))
mult12_in_gga(s(T161), s(s(0)), s(s(T164))) → U11_gga(T161, T164, mult73_in_ga(T161, T164))
mult73_in_ga(0, s(s(0))) → mult73_out_ga(0, s(s(0)))
mult73_in_ga(s(T195), s(s(T197))) → U3_ga(T195, T197, mult73_in_ga(T195, T197))
U3_ga(T195, T197, mult73_out_ga(T195, T197)) → mult73_out_ga(s(T195), s(s(T197)))
U11_gga(T161, T164, mult73_out_ga(T161, T164)) → mult12_out_gga(s(T161), s(s(0)), s(s(T164)))
mult12_in_gga(0, s(s(s(0))), s(s(s(0)))) → mult12_out_gga(0, s(s(s(0))), s(s(s(0))))
mult12_in_gga(s(T234), s(s(s(0))), s(s(s(T237)))) → U12_gga(T234, T237, mult106_in_ga(T234, T237))
mult106_in_ga(0, s(s(s(0)))) → mult106_out_ga(0, s(s(s(0))))
mult106_in_ga(s(T279), s(s(s(T281)))) → U4_ga(T279, T281, mult106_in_ga(T279, T281))
U4_ga(T279, T281, mult106_out_ga(T279, T281)) → mult106_out_ga(s(T279), s(s(s(T281))))
U12_gga(T234, T237, mult106_out_ga(T234, T237)) → mult12_out_gga(s(T234), s(s(s(0))), s(s(s(T237))))
mult12_in_gga(0, s(s(s(s(0)))), s(s(s(s(0))))) → mult12_out_gga(0, s(s(s(s(0)))), s(s(s(s(0)))))
mult12_in_gga(s(T318), s(s(s(s(0)))), s(s(s(s(T321))))) → U13_gga(T318, T321, mult144_in_ga(T318, T321))
mult144_in_ga(0, s(s(s(s(0))))) → mult144_out_ga(0, s(s(s(s(0)))))
mult144_in_ga(s(T374), s(s(s(s(T376))))) → U5_ga(T374, T376, mult144_in_ga(T374, T376))
U5_ga(T374, T376, mult144_out_ga(T374, T376)) → mult144_out_ga(s(T374), s(s(s(s(T376)))))
U13_gga(T318, T321, mult144_out_ga(T318, T321)) → mult12_out_gga(s(T318), s(s(s(s(0)))), s(s(s(s(T321)))))
mult12_in_gga(0, s(s(s(s(s(0))))), s(s(s(s(s(0)))))) → mult12_out_gga(0, s(s(s(s(s(0))))), s(s(s(s(s(0))))))
mult12_in_gga(s(T413), s(s(s(s(s(0))))), s(s(s(s(s(T416)))))) → U14_gga(T413, T416, mult187_in_ga(T413, T416))
mult187_in_ga(0, s(s(s(s(s(0)))))) → mult187_out_ga(0, s(s(s(s(s(0))))))
mult187_in_ga(s(T480), s(s(s(s(s(T482)))))) → U6_ga(T480, T482, mult187_in_ga(T480, T482))
U6_ga(T480, T482, mult187_out_ga(T480, T482)) → mult187_out_ga(s(T480), s(s(s(s(s(T482))))))
U14_gga(T413, T416, mult187_out_ga(T413, T416)) → mult12_out_gga(s(T413), s(s(s(s(s(0))))), s(s(s(s(s(T416))))))
mult12_in_gga(0, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(0))))))) → mult12_out_gga(0, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(0)))))))
mult12_in_gga(s(T519), s(s(s(s(s(s(0)))))), s(s(s(s(s(s(T522))))))) → U15_gga(T519, T522, mult235_in_ga(T519, T522))
mult235_in_ga(0, s(s(s(s(s(s(0))))))) → mult235_out_ga(0, s(s(s(s(s(s(0)))))))
mult235_in_ga(s(T597), s(s(s(s(s(s(T599))))))) → U7_ga(T597, T599, mult235_in_ga(T597, T599))
U7_ga(T597, T599, mult235_out_ga(T597, T599)) → mult235_out_ga(s(T597), s(s(s(s(s(s(T599)))))))
U15_gga(T519, T522, mult235_out_ga(T519, T522)) → mult12_out_gga(s(T519), s(s(s(s(s(s(0)))))), s(s(s(s(s(s(T522)))))))
mult12_in_gga(0, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(0)))))))) → mult12_out_gga(0, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(0))))))))
mult12_in_gga(s(T636), s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(T639)))))))) → U16_gga(T636, T639, mult288_in_ga(T636, T639))
mult288_in_ga(0, s(s(s(s(s(s(s(0)))))))) → mult288_out_ga(0, s(s(s(s(s(s(s(0))))))))
mult288_in_ga(s(T725), s(s(s(s(s(s(s(T727)))))))) → U8_ga(T725, T727, mult288_in_ga(T725, T727))
U8_ga(T725, T727, mult288_out_ga(T725, T727)) → mult288_out_ga(s(T725), s(s(s(s(s(s(s(T727))))))))
U16_gga(T636, T639, mult288_out_ga(T636, T639)) → mult12_out_gga(s(T636), s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(T639))))))))
mult12_in_gga(T740, s(s(s(s(s(s(s(s(T742)))))))), s(s(s(s(s(s(s(s(T744))))))))) → U17_gga(T740, T742, T744, mult338_in_ggga(T740, s(s(s(s(s(s(s(T742))))))), T742, T744))
mult338_in_ggga(0, T754, 0, 0) → mult338_out_ggga(0, T754, 0, 0)
mult338_in_ggga(s(T767), T768, 0, T770) → U18_ggga(T767, T768, T770, mult12_in_gga(T767, s(T768), T770))
U18_ggga(T767, T768, T770, mult12_out_gga(T767, s(T768), T770)) → mult338_out_ggga(s(T767), T768, 0, T770)
mult338_in_ggga(T786, T787, s(T788), s(T790)) → U19_ggga(T786, T787, T788, T790, mult338_in_ggga(T786, T787, T788, T790))
U19_ggga(T786, T787, T788, T790, mult338_out_ggga(T786, T787, T788, T790)) → mult338_out_ggga(T786, T787, s(T788), s(T790))
U17_gga(T740, T742, T744, mult338_out_ggga(T740, s(s(s(s(s(s(s(T742))))))), T742, T744)) → mult12_out_gga(T740, s(s(s(s(s(s(s(s(T742)))))))), s(s(s(s(s(s(s(s(T744)))))))))
U20_gga(T28, T29, T31, mult12_out_gga(T28, T29, T31)) → times1_out_gga(s(T28), T29, T31)

The argument filtering Pi contains the following mapping:
times1_in_gga(x1, x2, x3)  =  times1_in_gga(x1, x2)
0  =  0
times1_out_gga(x1, x2, x3)  =  times1_out_gga(x3)
s(x1)  =  s(x1)
U20_gga(x1, x2, x3, x4)  =  U20_gga(x4)
mult12_in_gga(x1, x2, x3)  =  mult12_in_gga(x1, x2)
mult12_out_gga(x1, x2, x3)  =  mult12_out_gga(x3)
U9_gga(x1, x2, x3)  =  U9_gga(x3)
mult22_in_ga(x1, x2)  =  mult22_in_ga(x1)
mult22_out_ga(x1, x2)  =  mult22_out_ga(x2)
U1_ga(x1, x2, x3)  =  U1_ga(x3)
U10_gga(x1, x2, x3)  =  U10_gga(x3)
mult45_in_ga(x1, x2)  =  mult45_in_ga(x1)
mult45_out_ga(x1, x2)  =  mult45_out_ga(x2)
U2_ga(x1, x2, x3)  =  U2_ga(x3)
U11_gga(x1, x2, x3)  =  U11_gga(x3)
mult73_in_ga(x1, x2)  =  mult73_in_ga(x1)
mult73_out_ga(x1, x2)  =  mult73_out_ga(x2)
U3_ga(x1, x2, x3)  =  U3_ga(x3)
U12_gga(x1, x2, x3)  =  U12_gga(x3)
mult106_in_ga(x1, x2)  =  mult106_in_ga(x1)
mult106_out_ga(x1, x2)  =  mult106_out_ga(x2)
U4_ga(x1, x2, x3)  =  U4_ga(x3)
U13_gga(x1, x2, x3)  =  U13_gga(x3)
mult144_in_ga(x1, x2)  =  mult144_in_ga(x1)
mult144_out_ga(x1, x2)  =  mult144_out_ga(x2)
U5_ga(x1, x2, x3)  =  U5_ga(x3)
U14_gga(x1, x2, x3)  =  U14_gga(x3)
mult187_in_ga(x1, x2)  =  mult187_in_ga(x1)
mult187_out_ga(x1, x2)  =  mult187_out_ga(x2)
U6_ga(x1, x2, x3)  =  U6_ga(x3)
U15_gga(x1, x2, x3)  =  U15_gga(x3)
mult235_in_ga(x1, x2)  =  mult235_in_ga(x1)
mult235_out_ga(x1, x2)  =  mult235_out_ga(x2)
U7_ga(x1, x2, x3)  =  U7_ga(x3)
U16_gga(x1, x2, x3)  =  U16_gga(x3)
mult288_in_ga(x1, x2)  =  mult288_in_ga(x1)
mult288_out_ga(x1, x2)  =  mult288_out_ga(x2)
U8_ga(x1, x2, x3)  =  U8_ga(x3)
U17_gga(x1, x2, x3, x4)  =  U17_gga(x4)
mult338_in_ggga(x1, x2, x3, x4)  =  mult338_in_ggga(x1, x2, x3)
mult338_out_ggga(x1, x2, x3, x4)  =  mult338_out_ggga(x4)
U18_ggga(x1, x2, x3, x4)  =  U18_ggga(x4)
U19_ggga(x1, x2, x3, x4, x5)  =  U19_ggga(x5)

(5) 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:

TIMES1_IN_GGA(s(T28), T29, T31) → U20_GGA(T28, T29, T31, mult12_in_gga(T28, T29, T31))
TIMES1_IN_GGA(s(T28), T29, T31) → MULT12_IN_GGA(T28, T29, T31)
MULT12_IN_GGA(s(T51), 0, T54) → U9_GGA(T51, T54, mult22_in_ga(T51, T54))
MULT12_IN_GGA(s(T51), 0, T54) → MULT22_IN_GA(T51, T54)
MULT22_IN_GA(s(T63), T65) → U1_GA(T63, T65, mult22_in_ga(T63, T65))
MULT22_IN_GA(s(T63), T65) → MULT22_IN_GA(T63, T65)
MULT12_IN_GGA(s(T99), s(0), s(T102)) → U10_GGA(T99, T102, mult45_in_ga(T99, T102))
MULT12_IN_GGA(s(T99), s(0), s(T102)) → MULT45_IN_GA(T99, T102)
MULT45_IN_GA(s(T122), s(T124)) → U2_GA(T122, T124, mult45_in_ga(T122, T124))
MULT45_IN_GA(s(T122), s(T124)) → MULT45_IN_GA(T122, T124)
MULT12_IN_GGA(s(T161), s(s(0)), s(s(T164))) → U11_GGA(T161, T164, mult73_in_ga(T161, T164))
MULT12_IN_GGA(s(T161), s(s(0)), s(s(T164))) → MULT73_IN_GA(T161, T164)
MULT73_IN_GA(s(T195), s(s(T197))) → U3_GA(T195, T197, mult73_in_ga(T195, T197))
MULT73_IN_GA(s(T195), s(s(T197))) → MULT73_IN_GA(T195, T197)
MULT12_IN_GGA(s(T234), s(s(s(0))), s(s(s(T237)))) → U12_GGA(T234, T237, mult106_in_ga(T234, T237))
MULT12_IN_GGA(s(T234), s(s(s(0))), s(s(s(T237)))) → MULT106_IN_GA(T234, T237)
MULT106_IN_GA(s(T279), s(s(s(T281)))) → U4_GA(T279, T281, mult106_in_ga(T279, T281))
MULT106_IN_GA(s(T279), s(s(s(T281)))) → MULT106_IN_GA(T279, T281)
MULT12_IN_GGA(s(T318), s(s(s(s(0)))), s(s(s(s(T321))))) → U13_GGA(T318, T321, mult144_in_ga(T318, T321))
MULT12_IN_GGA(s(T318), s(s(s(s(0)))), s(s(s(s(T321))))) → MULT144_IN_GA(T318, T321)
MULT144_IN_GA(s(T374), s(s(s(s(T376))))) → U5_GA(T374, T376, mult144_in_ga(T374, T376))
MULT144_IN_GA(s(T374), s(s(s(s(T376))))) → MULT144_IN_GA(T374, T376)
MULT12_IN_GGA(s(T413), s(s(s(s(s(0))))), s(s(s(s(s(T416)))))) → U14_GGA(T413, T416, mult187_in_ga(T413, T416))
MULT12_IN_GGA(s(T413), s(s(s(s(s(0))))), s(s(s(s(s(T416)))))) → MULT187_IN_GA(T413, T416)
MULT187_IN_GA(s(T480), s(s(s(s(s(T482)))))) → U6_GA(T480, T482, mult187_in_ga(T480, T482))
MULT187_IN_GA(s(T480), s(s(s(s(s(T482)))))) → MULT187_IN_GA(T480, T482)
MULT12_IN_GGA(s(T519), s(s(s(s(s(s(0)))))), s(s(s(s(s(s(T522))))))) → U15_GGA(T519, T522, mult235_in_ga(T519, T522))
MULT12_IN_GGA(s(T519), s(s(s(s(s(s(0)))))), s(s(s(s(s(s(T522))))))) → MULT235_IN_GA(T519, T522)
MULT235_IN_GA(s(T597), s(s(s(s(s(s(T599))))))) → U7_GA(T597, T599, mult235_in_ga(T597, T599))
MULT235_IN_GA(s(T597), s(s(s(s(s(s(T599))))))) → MULT235_IN_GA(T597, T599)
MULT12_IN_GGA(s(T636), s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(T639)))))))) → U16_GGA(T636, T639, mult288_in_ga(T636, T639))
MULT12_IN_GGA(s(T636), s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(T639)))))))) → MULT288_IN_GA(T636, T639)
MULT288_IN_GA(s(T725), s(s(s(s(s(s(s(T727)))))))) → U8_GA(T725, T727, mult288_in_ga(T725, T727))
MULT288_IN_GA(s(T725), s(s(s(s(s(s(s(T727)))))))) → MULT288_IN_GA(T725, T727)
MULT12_IN_GGA(T740, s(s(s(s(s(s(s(s(T742)))))))), s(s(s(s(s(s(s(s(T744))))))))) → U17_GGA(T740, T742, T744, mult338_in_ggga(T740, s(s(s(s(s(s(s(T742))))))), T742, T744))
MULT12_IN_GGA(T740, s(s(s(s(s(s(s(s(T742)))))))), s(s(s(s(s(s(s(s(T744))))))))) → MULT338_IN_GGGA(T740, s(s(s(s(s(s(s(T742))))))), T742, T744)
MULT338_IN_GGGA(s(T767), T768, 0, T770) → U18_GGGA(T767, T768, T770, mult12_in_gga(T767, s(T768), T770))
MULT338_IN_GGGA(s(T767), T768, 0, T770) → MULT12_IN_GGA(T767, s(T768), T770)
MULT338_IN_GGGA(T786, T787, s(T788), s(T790)) → U19_GGGA(T786, T787, T788, T790, mult338_in_ggga(T786, T787, T788, T790))
MULT338_IN_GGGA(T786, T787, s(T788), s(T790)) → MULT338_IN_GGGA(T786, T787, T788, T790)

The TRS R consists of the following rules:

times1_in_gga(0, T15, 0) → times1_out_gga(0, T15, 0)
times1_in_gga(s(T28), T29, T31) → U20_gga(T28, T29, T31, mult12_in_gga(T28, T29, T31))
mult12_in_gga(0, 0, 0) → mult12_out_gga(0, 0, 0)
mult12_in_gga(s(T51), 0, T54) → U9_gga(T51, T54, mult22_in_ga(T51, T54))
mult22_in_ga(0, 0) → mult22_out_ga(0, 0)
mult22_in_ga(s(T63), T65) → U1_ga(T63, T65, mult22_in_ga(T63, T65))
U1_ga(T63, T65, mult22_out_ga(T63, T65)) → mult22_out_ga(s(T63), T65)
U9_gga(T51, T54, mult22_out_ga(T51, T54)) → mult12_out_gga(s(T51), 0, T54)
mult12_in_gga(0, s(0), s(0)) → mult12_out_gga(0, s(0), s(0))
mult12_in_gga(s(T99), s(0), s(T102)) → U10_gga(T99, T102, mult45_in_ga(T99, T102))
mult45_in_ga(0, s(0)) → mult45_out_ga(0, s(0))
mult45_in_ga(s(T122), s(T124)) → U2_ga(T122, T124, mult45_in_ga(T122, T124))
U2_ga(T122, T124, mult45_out_ga(T122, T124)) → mult45_out_ga(s(T122), s(T124))
U10_gga(T99, T102, mult45_out_ga(T99, T102)) → mult12_out_gga(s(T99), s(0), s(T102))
mult12_in_gga(0, s(s(0)), s(s(0))) → mult12_out_gga(0, s(s(0)), s(s(0)))
mult12_in_gga(s(T161), s(s(0)), s(s(T164))) → U11_gga(T161, T164, mult73_in_ga(T161, T164))
mult73_in_ga(0, s(s(0))) → mult73_out_ga(0, s(s(0)))
mult73_in_ga(s(T195), s(s(T197))) → U3_ga(T195, T197, mult73_in_ga(T195, T197))
U3_ga(T195, T197, mult73_out_ga(T195, T197)) → mult73_out_ga(s(T195), s(s(T197)))
U11_gga(T161, T164, mult73_out_ga(T161, T164)) → mult12_out_gga(s(T161), s(s(0)), s(s(T164)))
mult12_in_gga(0, s(s(s(0))), s(s(s(0)))) → mult12_out_gga(0, s(s(s(0))), s(s(s(0))))
mult12_in_gga(s(T234), s(s(s(0))), s(s(s(T237)))) → U12_gga(T234, T237, mult106_in_ga(T234, T237))
mult106_in_ga(0, s(s(s(0)))) → mult106_out_ga(0, s(s(s(0))))
mult106_in_ga(s(T279), s(s(s(T281)))) → U4_ga(T279, T281, mult106_in_ga(T279, T281))
U4_ga(T279, T281, mult106_out_ga(T279, T281)) → mult106_out_ga(s(T279), s(s(s(T281))))
U12_gga(T234, T237, mult106_out_ga(T234, T237)) → mult12_out_gga(s(T234), s(s(s(0))), s(s(s(T237))))
mult12_in_gga(0, s(s(s(s(0)))), s(s(s(s(0))))) → mult12_out_gga(0, s(s(s(s(0)))), s(s(s(s(0)))))
mult12_in_gga(s(T318), s(s(s(s(0)))), s(s(s(s(T321))))) → U13_gga(T318, T321, mult144_in_ga(T318, T321))
mult144_in_ga(0, s(s(s(s(0))))) → mult144_out_ga(0, s(s(s(s(0)))))
mult144_in_ga(s(T374), s(s(s(s(T376))))) → U5_ga(T374, T376, mult144_in_ga(T374, T376))
U5_ga(T374, T376, mult144_out_ga(T374, T376)) → mult144_out_ga(s(T374), s(s(s(s(T376)))))
U13_gga(T318, T321, mult144_out_ga(T318, T321)) → mult12_out_gga(s(T318), s(s(s(s(0)))), s(s(s(s(T321)))))
mult12_in_gga(0, s(s(s(s(s(0))))), s(s(s(s(s(0)))))) → mult12_out_gga(0, s(s(s(s(s(0))))), s(s(s(s(s(0))))))
mult12_in_gga(s(T413), s(s(s(s(s(0))))), s(s(s(s(s(T416)))))) → U14_gga(T413, T416, mult187_in_ga(T413, T416))
mult187_in_ga(0, s(s(s(s(s(0)))))) → mult187_out_ga(0, s(s(s(s(s(0))))))
mult187_in_ga(s(T480), s(s(s(s(s(T482)))))) → U6_ga(T480, T482, mult187_in_ga(T480, T482))
U6_ga(T480, T482, mult187_out_ga(T480, T482)) → mult187_out_ga(s(T480), s(s(s(s(s(T482))))))
U14_gga(T413, T416, mult187_out_ga(T413, T416)) → mult12_out_gga(s(T413), s(s(s(s(s(0))))), s(s(s(s(s(T416))))))
mult12_in_gga(0, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(0))))))) → mult12_out_gga(0, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(0)))))))
mult12_in_gga(s(T519), s(s(s(s(s(s(0)))))), s(s(s(s(s(s(T522))))))) → U15_gga(T519, T522, mult235_in_ga(T519, T522))
mult235_in_ga(0, s(s(s(s(s(s(0))))))) → mult235_out_ga(0, s(s(s(s(s(s(0)))))))
mult235_in_ga(s(T597), s(s(s(s(s(s(T599))))))) → U7_ga(T597, T599, mult235_in_ga(T597, T599))
U7_ga(T597, T599, mult235_out_ga(T597, T599)) → mult235_out_ga(s(T597), s(s(s(s(s(s(T599)))))))
U15_gga(T519, T522, mult235_out_ga(T519, T522)) → mult12_out_gga(s(T519), s(s(s(s(s(s(0)))))), s(s(s(s(s(s(T522)))))))
mult12_in_gga(0, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(0)))))))) → mult12_out_gga(0, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(0))))))))
mult12_in_gga(s(T636), s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(T639)))))))) → U16_gga(T636, T639, mult288_in_ga(T636, T639))
mult288_in_ga(0, s(s(s(s(s(s(s(0)))))))) → mult288_out_ga(0, s(s(s(s(s(s(s(0))))))))
mult288_in_ga(s(T725), s(s(s(s(s(s(s(T727)))))))) → U8_ga(T725, T727, mult288_in_ga(T725, T727))
U8_ga(T725, T727, mult288_out_ga(T725, T727)) → mult288_out_ga(s(T725), s(s(s(s(s(s(s(T727))))))))
U16_gga(T636, T639, mult288_out_ga(T636, T639)) → mult12_out_gga(s(T636), s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(T639))))))))
mult12_in_gga(T740, s(s(s(s(s(s(s(s(T742)))))))), s(s(s(s(s(s(s(s(T744))))))))) → U17_gga(T740, T742, T744, mult338_in_ggga(T740, s(s(s(s(s(s(s(T742))))))), T742, T744))
mult338_in_ggga(0, T754, 0, 0) → mult338_out_ggga(0, T754, 0, 0)
mult338_in_ggga(s(T767), T768, 0, T770) → U18_ggga(T767, T768, T770, mult12_in_gga(T767, s(T768), T770))
U18_ggga(T767, T768, T770, mult12_out_gga(T767, s(T768), T770)) → mult338_out_ggga(s(T767), T768, 0, T770)
mult338_in_ggga(T786, T787, s(T788), s(T790)) → U19_ggga(T786, T787, T788, T790, mult338_in_ggga(T786, T787, T788, T790))
U19_ggga(T786, T787, T788, T790, mult338_out_ggga(T786, T787, T788, T790)) → mult338_out_ggga(T786, T787, s(T788), s(T790))
U17_gga(T740, T742, T744, mult338_out_ggga(T740, s(s(s(s(s(s(s(T742))))))), T742, T744)) → mult12_out_gga(T740, s(s(s(s(s(s(s(s(T742)))))))), s(s(s(s(s(s(s(s(T744)))))))))
U20_gga(T28, T29, T31, mult12_out_gga(T28, T29, T31)) → times1_out_gga(s(T28), T29, T31)

The argument filtering Pi contains the following mapping:
times1_in_gga(x1, x2, x3)  =  times1_in_gga(x1, x2)
0  =  0
times1_out_gga(x1, x2, x3)  =  times1_out_gga(x3)
s(x1)  =  s(x1)
U20_gga(x1, x2, x3, x4)  =  U20_gga(x4)
mult12_in_gga(x1, x2, x3)  =  mult12_in_gga(x1, x2)
mult12_out_gga(x1, x2, x3)  =  mult12_out_gga(x3)
U9_gga(x1, x2, x3)  =  U9_gga(x3)
mult22_in_ga(x1, x2)  =  mult22_in_ga(x1)
mult22_out_ga(x1, x2)  =  mult22_out_ga(x2)
U1_ga(x1, x2, x3)  =  U1_ga(x3)
U10_gga(x1, x2, x3)  =  U10_gga(x3)
mult45_in_ga(x1, x2)  =  mult45_in_ga(x1)
mult45_out_ga(x1, x2)  =  mult45_out_ga(x2)
U2_ga(x1, x2, x3)  =  U2_ga(x3)
U11_gga(x1, x2, x3)  =  U11_gga(x3)
mult73_in_ga(x1, x2)  =  mult73_in_ga(x1)
mult73_out_ga(x1, x2)  =  mult73_out_ga(x2)
U3_ga(x1, x2, x3)  =  U3_ga(x3)
U12_gga(x1, x2, x3)  =  U12_gga(x3)
mult106_in_ga(x1, x2)  =  mult106_in_ga(x1)
mult106_out_ga(x1, x2)  =  mult106_out_ga(x2)
U4_ga(x1, x2, x3)  =  U4_ga(x3)
U13_gga(x1, x2, x3)  =  U13_gga(x3)
mult144_in_ga(x1, x2)  =  mult144_in_ga(x1)
mult144_out_ga(x1, x2)  =  mult144_out_ga(x2)
U5_ga(x1, x2, x3)  =  U5_ga(x3)
U14_gga(x1, x2, x3)  =  U14_gga(x3)
mult187_in_ga(x1, x2)  =  mult187_in_ga(x1)
mult187_out_ga(x1, x2)  =  mult187_out_ga(x2)
U6_ga(x1, x2, x3)  =  U6_ga(x3)
U15_gga(x1, x2, x3)  =  U15_gga(x3)
mult235_in_ga(x1, x2)  =  mult235_in_ga(x1)
mult235_out_ga(x1, x2)  =  mult235_out_ga(x2)
U7_ga(x1, x2, x3)  =  U7_ga(x3)
U16_gga(x1, x2, x3)  =  U16_gga(x3)
mult288_in_ga(x1, x2)  =  mult288_in_ga(x1)
mult288_out_ga(x1, x2)  =  mult288_out_ga(x2)
U8_ga(x1, x2, x3)  =  U8_ga(x3)
U17_gga(x1, x2, x3, x4)  =  U17_gga(x4)
mult338_in_ggga(x1, x2, x3, x4)  =  mult338_in_ggga(x1, x2, x3)
mult338_out_ggga(x1, x2, x3, x4)  =  mult338_out_ggga(x4)
U18_ggga(x1, x2, x3, x4)  =  U18_ggga(x4)
U19_ggga(x1, x2, x3, x4, x5)  =  U19_ggga(x5)
TIMES1_IN_GGA(x1, x2, x3)  =  TIMES1_IN_GGA(x1, x2)
U20_GGA(x1, x2, x3, x4)  =  U20_GGA(x4)
MULT12_IN_GGA(x1, x2, x3)  =  MULT12_IN_GGA(x1, x2)
U9_GGA(x1, x2, x3)  =  U9_GGA(x3)
MULT22_IN_GA(x1, x2)  =  MULT22_IN_GA(x1)
U1_GA(x1, x2, x3)  =  U1_GA(x3)
U10_GGA(x1, x2, x3)  =  U10_GGA(x3)
MULT45_IN_GA(x1, x2)  =  MULT45_IN_GA(x1)
U2_GA(x1, x2, x3)  =  U2_GA(x3)
U11_GGA(x1, x2, x3)  =  U11_GGA(x3)
MULT73_IN_GA(x1, x2)  =  MULT73_IN_GA(x1)
U3_GA(x1, x2, x3)  =  U3_GA(x3)
U12_GGA(x1, x2, x3)  =  U12_GGA(x3)
MULT106_IN_GA(x1, x2)  =  MULT106_IN_GA(x1)
U4_GA(x1, x2, x3)  =  U4_GA(x3)
U13_GGA(x1, x2, x3)  =  U13_GGA(x3)
MULT144_IN_GA(x1, x2)  =  MULT144_IN_GA(x1)
U5_GA(x1, x2, x3)  =  U5_GA(x3)
U14_GGA(x1, x2, x3)  =  U14_GGA(x3)
MULT187_IN_GA(x1, x2)  =  MULT187_IN_GA(x1)
U6_GA(x1, x2, x3)  =  U6_GA(x3)
U15_GGA(x1, x2, x3)  =  U15_GGA(x3)
MULT235_IN_GA(x1, x2)  =  MULT235_IN_GA(x1)
U7_GA(x1, x2, x3)  =  U7_GA(x3)
U16_GGA(x1, x2, x3)  =  U16_GGA(x3)
MULT288_IN_GA(x1, x2)  =  MULT288_IN_GA(x1)
U8_GA(x1, x2, x3)  =  U8_GA(x3)
U17_GGA(x1, x2, x3, x4)  =  U17_GGA(x4)
MULT338_IN_GGGA(x1, x2, x3, x4)  =  MULT338_IN_GGGA(x1, x2, x3)
U18_GGGA(x1, x2, x3, x4)  =  U18_GGGA(x4)
U19_GGGA(x1, x2, x3, x4, x5)  =  U19_GGGA(x5)

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

(6) Obligation:

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

TIMES1_IN_GGA(s(T28), T29, T31) → U20_GGA(T28, T29, T31, mult12_in_gga(T28, T29, T31))
TIMES1_IN_GGA(s(T28), T29, T31) → MULT12_IN_GGA(T28, T29, T31)
MULT12_IN_GGA(s(T51), 0, T54) → U9_GGA(T51, T54, mult22_in_ga(T51, T54))
MULT12_IN_GGA(s(T51), 0, T54) → MULT22_IN_GA(T51, T54)
MULT22_IN_GA(s(T63), T65) → U1_GA(T63, T65, mult22_in_ga(T63, T65))
MULT22_IN_GA(s(T63), T65) → MULT22_IN_GA(T63, T65)
MULT12_IN_GGA(s(T99), s(0), s(T102)) → U10_GGA(T99, T102, mult45_in_ga(T99, T102))
MULT12_IN_GGA(s(T99), s(0), s(T102)) → MULT45_IN_GA(T99, T102)
MULT45_IN_GA(s(T122), s(T124)) → U2_GA(T122, T124, mult45_in_ga(T122, T124))
MULT45_IN_GA(s(T122), s(T124)) → MULT45_IN_GA(T122, T124)
MULT12_IN_GGA(s(T161), s(s(0)), s(s(T164))) → U11_GGA(T161, T164, mult73_in_ga(T161, T164))
MULT12_IN_GGA(s(T161), s(s(0)), s(s(T164))) → MULT73_IN_GA(T161, T164)
MULT73_IN_GA(s(T195), s(s(T197))) → U3_GA(T195, T197, mult73_in_ga(T195, T197))
MULT73_IN_GA(s(T195), s(s(T197))) → MULT73_IN_GA(T195, T197)
MULT12_IN_GGA(s(T234), s(s(s(0))), s(s(s(T237)))) → U12_GGA(T234, T237, mult106_in_ga(T234, T237))
MULT12_IN_GGA(s(T234), s(s(s(0))), s(s(s(T237)))) → MULT106_IN_GA(T234, T237)
MULT106_IN_GA(s(T279), s(s(s(T281)))) → U4_GA(T279, T281, mult106_in_ga(T279, T281))
MULT106_IN_GA(s(T279), s(s(s(T281)))) → MULT106_IN_GA(T279, T281)
MULT12_IN_GGA(s(T318), s(s(s(s(0)))), s(s(s(s(T321))))) → U13_GGA(T318, T321, mult144_in_ga(T318, T321))
MULT12_IN_GGA(s(T318), s(s(s(s(0)))), s(s(s(s(T321))))) → MULT144_IN_GA(T318, T321)
MULT144_IN_GA(s(T374), s(s(s(s(T376))))) → U5_GA(T374, T376, mult144_in_ga(T374, T376))
MULT144_IN_GA(s(T374), s(s(s(s(T376))))) → MULT144_IN_GA(T374, T376)
MULT12_IN_GGA(s(T413), s(s(s(s(s(0))))), s(s(s(s(s(T416)))))) → U14_GGA(T413, T416, mult187_in_ga(T413, T416))
MULT12_IN_GGA(s(T413), s(s(s(s(s(0))))), s(s(s(s(s(T416)))))) → MULT187_IN_GA(T413, T416)
MULT187_IN_GA(s(T480), s(s(s(s(s(T482)))))) → U6_GA(T480, T482, mult187_in_ga(T480, T482))
MULT187_IN_GA(s(T480), s(s(s(s(s(T482)))))) → MULT187_IN_GA(T480, T482)
MULT12_IN_GGA(s(T519), s(s(s(s(s(s(0)))))), s(s(s(s(s(s(T522))))))) → U15_GGA(T519, T522, mult235_in_ga(T519, T522))
MULT12_IN_GGA(s(T519), s(s(s(s(s(s(0)))))), s(s(s(s(s(s(T522))))))) → MULT235_IN_GA(T519, T522)
MULT235_IN_GA(s(T597), s(s(s(s(s(s(T599))))))) → U7_GA(T597, T599, mult235_in_ga(T597, T599))
MULT235_IN_GA(s(T597), s(s(s(s(s(s(T599))))))) → MULT235_IN_GA(T597, T599)
MULT12_IN_GGA(s(T636), s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(T639)))))))) → U16_GGA(T636, T639, mult288_in_ga(T636, T639))
MULT12_IN_GGA(s(T636), s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(T639)))))))) → MULT288_IN_GA(T636, T639)
MULT288_IN_GA(s(T725), s(s(s(s(s(s(s(T727)))))))) → U8_GA(T725, T727, mult288_in_ga(T725, T727))
MULT288_IN_GA(s(T725), s(s(s(s(s(s(s(T727)))))))) → MULT288_IN_GA(T725, T727)
MULT12_IN_GGA(T740, s(s(s(s(s(s(s(s(T742)))))))), s(s(s(s(s(s(s(s(T744))))))))) → U17_GGA(T740, T742, T744, mult338_in_ggga(T740, s(s(s(s(s(s(s(T742))))))), T742, T744))
MULT12_IN_GGA(T740, s(s(s(s(s(s(s(s(T742)))))))), s(s(s(s(s(s(s(s(T744))))))))) → MULT338_IN_GGGA(T740, s(s(s(s(s(s(s(T742))))))), T742, T744)
MULT338_IN_GGGA(s(T767), T768, 0, T770) → U18_GGGA(T767, T768, T770, mult12_in_gga(T767, s(T768), T770))
MULT338_IN_GGGA(s(T767), T768, 0, T770) → MULT12_IN_GGA(T767, s(T768), T770)
MULT338_IN_GGGA(T786, T787, s(T788), s(T790)) → U19_GGGA(T786, T787, T788, T790, mult338_in_ggga(T786, T787, T788, T790))
MULT338_IN_GGGA(T786, T787, s(T788), s(T790)) → MULT338_IN_GGGA(T786, T787, T788, T790)

The TRS R consists of the following rules:

times1_in_gga(0, T15, 0) → times1_out_gga(0, T15, 0)
times1_in_gga(s(T28), T29, T31) → U20_gga(T28, T29, T31, mult12_in_gga(T28, T29, T31))
mult12_in_gga(0, 0, 0) → mult12_out_gga(0, 0, 0)
mult12_in_gga(s(T51), 0, T54) → U9_gga(T51, T54, mult22_in_ga(T51, T54))
mult22_in_ga(0, 0) → mult22_out_ga(0, 0)
mult22_in_ga(s(T63), T65) → U1_ga(T63, T65, mult22_in_ga(T63, T65))
U1_ga(T63, T65, mult22_out_ga(T63, T65)) → mult22_out_ga(s(T63), T65)
U9_gga(T51, T54, mult22_out_ga(T51, T54)) → mult12_out_gga(s(T51), 0, T54)
mult12_in_gga(0, s(0), s(0)) → mult12_out_gga(0, s(0), s(0))
mult12_in_gga(s(T99), s(0), s(T102)) → U10_gga(T99, T102, mult45_in_ga(T99, T102))
mult45_in_ga(0, s(0)) → mult45_out_ga(0, s(0))
mult45_in_ga(s(T122), s(T124)) → U2_ga(T122, T124, mult45_in_ga(T122, T124))
U2_ga(T122, T124, mult45_out_ga(T122, T124)) → mult45_out_ga(s(T122), s(T124))
U10_gga(T99, T102, mult45_out_ga(T99, T102)) → mult12_out_gga(s(T99), s(0), s(T102))
mult12_in_gga(0, s(s(0)), s(s(0))) → mult12_out_gga(0, s(s(0)), s(s(0)))
mult12_in_gga(s(T161), s(s(0)), s(s(T164))) → U11_gga(T161, T164, mult73_in_ga(T161, T164))
mult73_in_ga(0, s(s(0))) → mult73_out_ga(0, s(s(0)))
mult73_in_ga(s(T195), s(s(T197))) → U3_ga(T195, T197, mult73_in_ga(T195, T197))
U3_ga(T195, T197, mult73_out_ga(T195, T197)) → mult73_out_ga(s(T195), s(s(T197)))
U11_gga(T161, T164, mult73_out_ga(T161, T164)) → mult12_out_gga(s(T161), s(s(0)), s(s(T164)))
mult12_in_gga(0, s(s(s(0))), s(s(s(0)))) → mult12_out_gga(0, s(s(s(0))), s(s(s(0))))
mult12_in_gga(s(T234), s(s(s(0))), s(s(s(T237)))) → U12_gga(T234, T237, mult106_in_ga(T234, T237))
mult106_in_ga(0, s(s(s(0)))) → mult106_out_ga(0, s(s(s(0))))
mult106_in_ga(s(T279), s(s(s(T281)))) → U4_ga(T279, T281, mult106_in_ga(T279, T281))
U4_ga(T279, T281, mult106_out_ga(T279, T281)) → mult106_out_ga(s(T279), s(s(s(T281))))
U12_gga(T234, T237, mult106_out_ga(T234, T237)) → mult12_out_gga(s(T234), s(s(s(0))), s(s(s(T237))))
mult12_in_gga(0, s(s(s(s(0)))), s(s(s(s(0))))) → mult12_out_gga(0, s(s(s(s(0)))), s(s(s(s(0)))))
mult12_in_gga(s(T318), s(s(s(s(0)))), s(s(s(s(T321))))) → U13_gga(T318, T321, mult144_in_ga(T318, T321))
mult144_in_ga(0, s(s(s(s(0))))) → mult144_out_ga(0, s(s(s(s(0)))))
mult144_in_ga(s(T374), s(s(s(s(T376))))) → U5_ga(T374, T376, mult144_in_ga(T374, T376))
U5_ga(T374, T376, mult144_out_ga(T374, T376)) → mult144_out_ga(s(T374), s(s(s(s(T376)))))
U13_gga(T318, T321, mult144_out_ga(T318, T321)) → mult12_out_gga(s(T318), s(s(s(s(0)))), s(s(s(s(T321)))))
mult12_in_gga(0, s(s(s(s(s(0))))), s(s(s(s(s(0)))))) → mult12_out_gga(0, s(s(s(s(s(0))))), s(s(s(s(s(0))))))
mult12_in_gga(s(T413), s(s(s(s(s(0))))), s(s(s(s(s(T416)))))) → U14_gga(T413, T416, mult187_in_ga(T413, T416))
mult187_in_ga(0, s(s(s(s(s(0)))))) → mult187_out_ga(0, s(s(s(s(s(0))))))
mult187_in_ga(s(T480), s(s(s(s(s(T482)))))) → U6_ga(T480, T482, mult187_in_ga(T480, T482))
U6_ga(T480, T482, mult187_out_ga(T480, T482)) → mult187_out_ga(s(T480), s(s(s(s(s(T482))))))
U14_gga(T413, T416, mult187_out_ga(T413, T416)) → mult12_out_gga(s(T413), s(s(s(s(s(0))))), s(s(s(s(s(T416))))))
mult12_in_gga(0, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(0))))))) → mult12_out_gga(0, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(0)))))))
mult12_in_gga(s(T519), s(s(s(s(s(s(0)))))), s(s(s(s(s(s(T522))))))) → U15_gga(T519, T522, mult235_in_ga(T519, T522))
mult235_in_ga(0, s(s(s(s(s(s(0))))))) → mult235_out_ga(0, s(s(s(s(s(s(0)))))))
mult235_in_ga(s(T597), s(s(s(s(s(s(T599))))))) → U7_ga(T597, T599, mult235_in_ga(T597, T599))
U7_ga(T597, T599, mult235_out_ga(T597, T599)) → mult235_out_ga(s(T597), s(s(s(s(s(s(T599)))))))
U15_gga(T519, T522, mult235_out_ga(T519, T522)) → mult12_out_gga(s(T519), s(s(s(s(s(s(0)))))), s(s(s(s(s(s(T522)))))))
mult12_in_gga(0, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(0)))))))) → mult12_out_gga(0, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(0))))))))
mult12_in_gga(s(T636), s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(T639)))))))) → U16_gga(T636, T639, mult288_in_ga(T636, T639))
mult288_in_ga(0, s(s(s(s(s(s(s(0)))))))) → mult288_out_ga(0, s(s(s(s(s(s(s(0))))))))
mult288_in_ga(s(T725), s(s(s(s(s(s(s(T727)))))))) → U8_ga(T725, T727, mult288_in_ga(T725, T727))
U8_ga(T725, T727, mult288_out_ga(T725, T727)) → mult288_out_ga(s(T725), s(s(s(s(s(s(s(T727))))))))
U16_gga(T636, T639, mult288_out_ga(T636, T639)) → mult12_out_gga(s(T636), s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(T639))))))))
mult12_in_gga(T740, s(s(s(s(s(s(s(s(T742)))))))), s(s(s(s(s(s(s(s(T744))))))))) → U17_gga(T740, T742, T744, mult338_in_ggga(T740, s(s(s(s(s(s(s(T742))))))), T742, T744))
mult338_in_ggga(0, T754, 0, 0) → mult338_out_ggga(0, T754, 0, 0)
mult338_in_ggga(s(T767), T768, 0, T770) → U18_ggga(T767, T768, T770, mult12_in_gga(T767, s(T768), T770))
U18_ggga(T767, T768, T770, mult12_out_gga(T767, s(T768), T770)) → mult338_out_ggga(s(T767), T768, 0, T770)
mult338_in_ggga(T786, T787, s(T788), s(T790)) → U19_ggga(T786, T787, T788, T790, mult338_in_ggga(T786, T787, T788, T790))
U19_ggga(T786, T787, T788, T790, mult338_out_ggga(T786, T787, T788, T790)) → mult338_out_ggga(T786, T787, s(T788), s(T790))
U17_gga(T740, T742, T744, mult338_out_ggga(T740, s(s(s(s(s(s(s(T742))))))), T742, T744)) → mult12_out_gga(T740, s(s(s(s(s(s(s(s(T742)))))))), s(s(s(s(s(s(s(s(T744)))))))))
U20_gga(T28, T29, T31, mult12_out_gga(T28, T29, T31)) → times1_out_gga(s(T28), T29, T31)

The argument filtering Pi contains the following mapping:
times1_in_gga(x1, x2, x3)  =  times1_in_gga(x1, x2)
0  =  0
times1_out_gga(x1, x2, x3)  =  times1_out_gga(x3)
s(x1)  =  s(x1)
U20_gga(x1, x2, x3, x4)  =  U20_gga(x4)
mult12_in_gga(x1, x2, x3)  =  mult12_in_gga(x1, x2)
mult12_out_gga(x1, x2, x3)  =  mult12_out_gga(x3)
U9_gga(x1, x2, x3)  =  U9_gga(x3)
mult22_in_ga(x1, x2)  =  mult22_in_ga(x1)
mult22_out_ga(x1, x2)  =  mult22_out_ga(x2)
U1_ga(x1, x2, x3)  =  U1_ga(x3)
U10_gga(x1, x2, x3)  =  U10_gga(x3)
mult45_in_ga(x1, x2)  =  mult45_in_ga(x1)
mult45_out_ga(x1, x2)  =  mult45_out_ga(x2)
U2_ga(x1, x2, x3)  =  U2_ga(x3)
U11_gga(x1, x2, x3)  =  U11_gga(x3)
mult73_in_ga(x1, x2)  =  mult73_in_ga(x1)
mult73_out_ga(x1, x2)  =  mult73_out_ga(x2)
U3_ga(x1, x2, x3)  =  U3_ga(x3)
U12_gga(x1, x2, x3)  =  U12_gga(x3)
mult106_in_ga(x1, x2)  =  mult106_in_ga(x1)
mult106_out_ga(x1, x2)  =  mult106_out_ga(x2)
U4_ga(x1, x2, x3)  =  U4_ga(x3)
U13_gga(x1, x2, x3)  =  U13_gga(x3)
mult144_in_ga(x1, x2)  =  mult144_in_ga(x1)
mult144_out_ga(x1, x2)  =  mult144_out_ga(x2)
U5_ga(x1, x2, x3)  =  U5_ga(x3)
U14_gga(x1, x2, x3)  =  U14_gga(x3)
mult187_in_ga(x1, x2)  =  mult187_in_ga(x1)
mult187_out_ga(x1, x2)  =  mult187_out_ga(x2)
U6_ga(x1, x2, x3)  =  U6_ga(x3)
U15_gga(x1, x2, x3)  =  U15_gga(x3)
mult235_in_ga(x1, x2)  =  mult235_in_ga(x1)
mult235_out_ga(x1, x2)  =  mult235_out_ga(x2)
U7_ga(x1, x2, x3)  =  U7_ga(x3)
U16_gga(x1, x2, x3)  =  U16_gga(x3)
mult288_in_ga(x1, x2)  =  mult288_in_ga(x1)
mult288_out_ga(x1, x2)  =  mult288_out_ga(x2)
U8_ga(x1, x2, x3)  =  U8_ga(x3)
U17_gga(x1, x2, x3, x4)  =  U17_gga(x4)
mult338_in_ggga(x1, x2, x3, x4)  =  mult338_in_ggga(x1, x2, x3)
mult338_out_ggga(x1, x2, x3, x4)  =  mult338_out_ggga(x4)
U18_ggga(x1, x2, x3, x4)  =  U18_ggga(x4)
U19_ggga(x1, x2, x3, x4, x5)  =  U19_ggga(x5)
TIMES1_IN_GGA(x1, x2, x3)  =  TIMES1_IN_GGA(x1, x2)
U20_GGA(x1, x2, x3, x4)  =  U20_GGA(x4)
MULT12_IN_GGA(x1, x2, x3)  =  MULT12_IN_GGA(x1, x2)
U9_GGA(x1, x2, x3)  =  U9_GGA(x3)
MULT22_IN_GA(x1, x2)  =  MULT22_IN_GA(x1)
U1_GA(x1, x2, x3)  =  U1_GA(x3)
U10_GGA(x1, x2, x3)  =  U10_GGA(x3)
MULT45_IN_GA(x1, x2)  =  MULT45_IN_GA(x1)
U2_GA(x1, x2, x3)  =  U2_GA(x3)
U11_GGA(x1, x2, x3)  =  U11_GGA(x3)
MULT73_IN_GA(x1, x2)  =  MULT73_IN_GA(x1)
U3_GA(x1, x2, x3)  =  U3_GA(x3)
U12_GGA(x1, x2, x3)  =  U12_GGA(x3)
MULT106_IN_GA(x1, x2)  =  MULT106_IN_GA(x1)
U4_GA(x1, x2, x3)  =  U4_GA(x3)
U13_GGA(x1, x2, x3)  =  U13_GGA(x3)
MULT144_IN_GA(x1, x2)  =  MULT144_IN_GA(x1)
U5_GA(x1, x2, x3)  =  U5_GA(x3)
U14_GGA(x1, x2, x3)  =  U14_GGA(x3)
MULT187_IN_GA(x1, x2)  =  MULT187_IN_GA(x1)
U6_GA(x1, x2, x3)  =  U6_GA(x3)
U15_GGA(x1, x2, x3)  =  U15_GGA(x3)
MULT235_IN_GA(x1, x2)  =  MULT235_IN_GA(x1)
U7_GA(x1, x2, x3)  =  U7_GA(x3)
U16_GGA(x1, x2, x3)  =  U16_GGA(x3)
MULT288_IN_GA(x1, x2)  =  MULT288_IN_GA(x1)
U8_GA(x1, x2, x3)  =  U8_GA(x3)
U17_GGA(x1, x2, x3, x4)  =  U17_GGA(x4)
MULT338_IN_GGGA(x1, x2, x3, x4)  =  MULT338_IN_GGGA(x1, x2, x3)
U18_GGGA(x1, x2, x3, x4)  =  U18_GGGA(x4)
U19_GGGA(x1, x2, x3, x4, x5)  =  U19_GGGA(x5)

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

(7) DependencyGraphProof (EQUIVALENT transformation)

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

(8) Complex Obligation (AND)

(9) Obligation:

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

MULT288_IN_GA(s(T725), s(s(s(s(s(s(s(T727)))))))) → MULT288_IN_GA(T725, T727)

The TRS R consists of the following rules:

times1_in_gga(0, T15, 0) → times1_out_gga(0, T15, 0)
times1_in_gga(s(T28), T29, T31) → U20_gga(T28, T29, T31, mult12_in_gga(T28, T29, T31))
mult12_in_gga(0, 0, 0) → mult12_out_gga(0, 0, 0)
mult12_in_gga(s(T51), 0, T54) → U9_gga(T51, T54, mult22_in_ga(T51, T54))
mult22_in_ga(0, 0) → mult22_out_ga(0, 0)
mult22_in_ga(s(T63), T65) → U1_ga(T63, T65, mult22_in_ga(T63, T65))
U1_ga(T63, T65, mult22_out_ga(T63, T65)) → mult22_out_ga(s(T63), T65)
U9_gga(T51, T54, mult22_out_ga(T51, T54)) → mult12_out_gga(s(T51), 0, T54)
mult12_in_gga(0, s(0), s(0)) → mult12_out_gga(0, s(0), s(0))
mult12_in_gga(s(T99), s(0), s(T102)) → U10_gga(T99, T102, mult45_in_ga(T99, T102))
mult45_in_ga(0, s(0)) → mult45_out_ga(0, s(0))
mult45_in_ga(s(T122), s(T124)) → U2_ga(T122, T124, mult45_in_ga(T122, T124))
U2_ga(T122, T124, mult45_out_ga(T122, T124)) → mult45_out_ga(s(T122), s(T124))
U10_gga(T99, T102, mult45_out_ga(T99, T102)) → mult12_out_gga(s(T99), s(0), s(T102))
mult12_in_gga(0, s(s(0)), s(s(0))) → mult12_out_gga(0, s(s(0)), s(s(0)))
mult12_in_gga(s(T161), s(s(0)), s(s(T164))) → U11_gga(T161, T164, mult73_in_ga(T161, T164))
mult73_in_ga(0, s(s(0))) → mult73_out_ga(0, s(s(0)))
mult73_in_ga(s(T195), s(s(T197))) → U3_ga(T195, T197, mult73_in_ga(T195, T197))
U3_ga(T195, T197, mult73_out_ga(T195, T197)) → mult73_out_ga(s(T195), s(s(T197)))
U11_gga(T161, T164, mult73_out_ga(T161, T164)) → mult12_out_gga(s(T161), s(s(0)), s(s(T164)))
mult12_in_gga(0, s(s(s(0))), s(s(s(0)))) → mult12_out_gga(0, s(s(s(0))), s(s(s(0))))
mult12_in_gga(s(T234), s(s(s(0))), s(s(s(T237)))) → U12_gga(T234, T237, mult106_in_ga(T234, T237))
mult106_in_ga(0, s(s(s(0)))) → mult106_out_ga(0, s(s(s(0))))
mult106_in_ga(s(T279), s(s(s(T281)))) → U4_ga(T279, T281, mult106_in_ga(T279, T281))
U4_ga(T279, T281, mult106_out_ga(T279, T281)) → mult106_out_ga(s(T279), s(s(s(T281))))
U12_gga(T234, T237, mult106_out_ga(T234, T237)) → mult12_out_gga(s(T234), s(s(s(0))), s(s(s(T237))))
mult12_in_gga(0, s(s(s(s(0)))), s(s(s(s(0))))) → mult12_out_gga(0, s(s(s(s(0)))), s(s(s(s(0)))))
mult12_in_gga(s(T318), s(s(s(s(0)))), s(s(s(s(T321))))) → U13_gga(T318, T321, mult144_in_ga(T318, T321))
mult144_in_ga(0, s(s(s(s(0))))) → mult144_out_ga(0, s(s(s(s(0)))))
mult144_in_ga(s(T374), s(s(s(s(T376))))) → U5_ga(T374, T376, mult144_in_ga(T374, T376))
U5_ga(T374, T376, mult144_out_ga(T374, T376)) → mult144_out_ga(s(T374), s(s(s(s(T376)))))
U13_gga(T318, T321, mult144_out_ga(T318, T321)) → mult12_out_gga(s(T318), s(s(s(s(0)))), s(s(s(s(T321)))))
mult12_in_gga(0, s(s(s(s(s(0))))), s(s(s(s(s(0)))))) → mult12_out_gga(0, s(s(s(s(s(0))))), s(s(s(s(s(0))))))
mult12_in_gga(s(T413), s(s(s(s(s(0))))), s(s(s(s(s(T416)))))) → U14_gga(T413, T416, mult187_in_ga(T413, T416))
mult187_in_ga(0, s(s(s(s(s(0)))))) → mult187_out_ga(0, s(s(s(s(s(0))))))
mult187_in_ga(s(T480), s(s(s(s(s(T482)))))) → U6_ga(T480, T482, mult187_in_ga(T480, T482))
U6_ga(T480, T482, mult187_out_ga(T480, T482)) → mult187_out_ga(s(T480), s(s(s(s(s(T482))))))
U14_gga(T413, T416, mult187_out_ga(T413, T416)) → mult12_out_gga(s(T413), s(s(s(s(s(0))))), s(s(s(s(s(T416))))))
mult12_in_gga(0, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(0))))))) → mult12_out_gga(0, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(0)))))))
mult12_in_gga(s(T519), s(s(s(s(s(s(0)))))), s(s(s(s(s(s(T522))))))) → U15_gga(T519, T522, mult235_in_ga(T519, T522))
mult235_in_ga(0, s(s(s(s(s(s(0))))))) → mult235_out_ga(0, s(s(s(s(s(s(0)))))))
mult235_in_ga(s(T597), s(s(s(s(s(s(T599))))))) → U7_ga(T597, T599, mult235_in_ga(T597, T599))
U7_ga(T597, T599, mult235_out_ga(T597, T599)) → mult235_out_ga(s(T597), s(s(s(s(s(s(T599)))))))
U15_gga(T519, T522, mult235_out_ga(T519, T522)) → mult12_out_gga(s(T519), s(s(s(s(s(s(0)))))), s(s(s(s(s(s(T522)))))))
mult12_in_gga(0, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(0)))))))) → mult12_out_gga(0, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(0))))))))
mult12_in_gga(s(T636), s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(T639)))))))) → U16_gga(T636, T639, mult288_in_ga(T636, T639))
mult288_in_ga(0, s(s(s(s(s(s(s(0)))))))) → mult288_out_ga(0, s(s(s(s(s(s(s(0))))))))
mult288_in_ga(s(T725), s(s(s(s(s(s(s(T727)))))))) → U8_ga(T725, T727, mult288_in_ga(T725, T727))
U8_ga(T725, T727, mult288_out_ga(T725, T727)) → mult288_out_ga(s(T725), s(s(s(s(s(s(s(T727))))))))
U16_gga(T636, T639, mult288_out_ga(T636, T639)) → mult12_out_gga(s(T636), s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(T639))))))))
mult12_in_gga(T740, s(s(s(s(s(s(s(s(T742)))))))), s(s(s(s(s(s(s(s(T744))))))))) → U17_gga(T740, T742, T744, mult338_in_ggga(T740, s(s(s(s(s(s(s(T742))))))), T742, T744))
mult338_in_ggga(0, T754, 0, 0) → mult338_out_ggga(0, T754, 0, 0)
mult338_in_ggga(s(T767), T768, 0, T770) → U18_ggga(T767, T768, T770, mult12_in_gga(T767, s(T768), T770))
U18_ggga(T767, T768, T770, mult12_out_gga(T767, s(T768), T770)) → mult338_out_ggga(s(T767), T768, 0, T770)
mult338_in_ggga(T786, T787, s(T788), s(T790)) → U19_ggga(T786, T787, T788, T790, mult338_in_ggga(T786, T787, T788, T790))
U19_ggga(T786, T787, T788, T790, mult338_out_ggga(T786, T787, T788, T790)) → mult338_out_ggga(T786, T787, s(T788), s(T790))
U17_gga(T740, T742, T744, mult338_out_ggga(T740, s(s(s(s(s(s(s(T742))))))), T742, T744)) → mult12_out_gga(T740, s(s(s(s(s(s(s(s(T742)))))))), s(s(s(s(s(s(s(s(T744)))))))))
U20_gga(T28, T29, T31, mult12_out_gga(T28, T29, T31)) → times1_out_gga(s(T28), T29, T31)

The argument filtering Pi contains the following mapping:
times1_in_gga(x1, x2, x3)  =  times1_in_gga(x1, x2)
0  =  0
times1_out_gga(x1, x2, x3)  =  times1_out_gga(x3)
s(x1)  =  s(x1)
U20_gga(x1, x2, x3, x4)  =  U20_gga(x4)
mult12_in_gga(x1, x2, x3)  =  mult12_in_gga(x1, x2)
mult12_out_gga(x1, x2, x3)  =  mult12_out_gga(x3)
U9_gga(x1, x2, x3)  =  U9_gga(x3)
mult22_in_ga(x1, x2)  =  mult22_in_ga(x1)
mult22_out_ga(x1, x2)  =  mult22_out_ga(x2)
U1_ga(x1, x2, x3)  =  U1_ga(x3)
U10_gga(x1, x2, x3)  =  U10_gga(x3)
mult45_in_ga(x1, x2)  =  mult45_in_ga(x1)
mult45_out_ga(x1, x2)  =  mult45_out_ga(x2)
U2_ga(x1, x2, x3)  =  U2_ga(x3)
U11_gga(x1, x2, x3)  =  U11_gga(x3)
mult73_in_ga(x1, x2)  =  mult73_in_ga(x1)
mult73_out_ga(x1, x2)  =  mult73_out_ga(x2)
U3_ga(x1, x2, x3)  =  U3_ga(x3)
U12_gga(x1, x2, x3)  =  U12_gga(x3)
mult106_in_ga(x1, x2)  =  mult106_in_ga(x1)
mult106_out_ga(x1, x2)  =  mult106_out_ga(x2)
U4_ga(x1, x2, x3)  =  U4_ga(x3)
U13_gga(x1, x2, x3)  =  U13_gga(x3)
mult144_in_ga(x1, x2)  =  mult144_in_ga(x1)
mult144_out_ga(x1, x2)  =  mult144_out_ga(x2)
U5_ga(x1, x2, x3)  =  U5_ga(x3)
U14_gga(x1, x2, x3)  =  U14_gga(x3)
mult187_in_ga(x1, x2)  =  mult187_in_ga(x1)
mult187_out_ga(x1, x2)  =  mult187_out_ga(x2)
U6_ga(x1, x2, x3)  =  U6_ga(x3)
U15_gga(x1, x2, x3)  =  U15_gga(x3)
mult235_in_ga(x1, x2)  =  mult235_in_ga(x1)
mult235_out_ga(x1, x2)  =  mult235_out_ga(x2)
U7_ga(x1, x2, x3)  =  U7_ga(x3)
U16_gga(x1, x2, x3)  =  U16_gga(x3)
mult288_in_ga(x1, x2)  =  mult288_in_ga(x1)
mult288_out_ga(x1, x2)  =  mult288_out_ga(x2)
U8_ga(x1, x2, x3)  =  U8_ga(x3)
U17_gga(x1, x2, x3, x4)  =  U17_gga(x4)
mult338_in_ggga(x1, x2, x3, x4)  =  mult338_in_ggga(x1, x2, x3)
mult338_out_ggga(x1, x2, x3, x4)  =  mult338_out_ggga(x4)
U18_ggga(x1, x2, x3, x4)  =  U18_ggga(x4)
U19_ggga(x1, x2, x3, x4, x5)  =  U19_ggga(x5)
MULT288_IN_GA(x1, x2)  =  MULT288_IN_GA(x1)

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

(10) UsableRulesProof (EQUIVALENT transformation)

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

(11) Obligation:

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

MULT288_IN_GA(s(T725), s(s(s(s(s(s(s(T727)))))))) → MULT288_IN_GA(T725, T727)

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

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

(12) PiDPToQDPProof (SOUND transformation)

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

(13) Obligation:

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

MULT288_IN_GA(s(T725)) → MULT288_IN_GA(T725)

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

(14) 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:

  • MULT288_IN_GA(s(T725)) → MULT288_IN_GA(T725)
    The graph contains the following edges 1 > 1

(15) YES

(16) Obligation:

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

MULT235_IN_GA(s(T597), s(s(s(s(s(s(T599))))))) → MULT235_IN_GA(T597, T599)

The TRS R consists of the following rules:

times1_in_gga(0, T15, 0) → times1_out_gga(0, T15, 0)
times1_in_gga(s(T28), T29, T31) → U20_gga(T28, T29, T31, mult12_in_gga(T28, T29, T31))
mult12_in_gga(0, 0, 0) → mult12_out_gga(0, 0, 0)
mult12_in_gga(s(T51), 0, T54) → U9_gga(T51, T54, mult22_in_ga(T51, T54))
mult22_in_ga(0, 0) → mult22_out_ga(0, 0)
mult22_in_ga(s(T63), T65) → U1_ga(T63, T65, mult22_in_ga(T63, T65))
U1_ga(T63, T65, mult22_out_ga(T63, T65)) → mult22_out_ga(s(T63), T65)
U9_gga(T51, T54, mult22_out_ga(T51, T54)) → mult12_out_gga(s(T51), 0, T54)
mult12_in_gga(0, s(0), s(0)) → mult12_out_gga(0, s(0), s(0))
mult12_in_gga(s(T99), s(0), s(T102)) → U10_gga(T99, T102, mult45_in_ga(T99, T102))
mult45_in_ga(0, s(0)) → mult45_out_ga(0, s(0))
mult45_in_ga(s(T122), s(T124)) → U2_ga(T122, T124, mult45_in_ga(T122, T124))
U2_ga(T122, T124, mult45_out_ga(T122, T124)) → mult45_out_ga(s(T122), s(T124))
U10_gga(T99, T102, mult45_out_ga(T99, T102)) → mult12_out_gga(s(T99), s(0), s(T102))
mult12_in_gga(0, s(s(0)), s(s(0))) → mult12_out_gga(0, s(s(0)), s(s(0)))
mult12_in_gga(s(T161), s(s(0)), s(s(T164))) → U11_gga(T161, T164, mult73_in_ga(T161, T164))
mult73_in_ga(0, s(s(0))) → mult73_out_ga(0, s(s(0)))
mult73_in_ga(s(T195), s(s(T197))) → U3_ga(T195, T197, mult73_in_ga(T195, T197))
U3_ga(T195, T197, mult73_out_ga(T195, T197)) → mult73_out_ga(s(T195), s(s(T197)))
U11_gga(T161, T164, mult73_out_ga(T161, T164)) → mult12_out_gga(s(T161), s(s(0)), s(s(T164)))
mult12_in_gga(0, s(s(s(0))), s(s(s(0)))) → mult12_out_gga(0, s(s(s(0))), s(s(s(0))))
mult12_in_gga(s(T234), s(s(s(0))), s(s(s(T237)))) → U12_gga(T234, T237, mult106_in_ga(T234, T237))
mult106_in_ga(0, s(s(s(0)))) → mult106_out_ga(0, s(s(s(0))))
mult106_in_ga(s(T279), s(s(s(T281)))) → U4_ga(T279, T281, mult106_in_ga(T279, T281))
U4_ga(T279, T281, mult106_out_ga(T279, T281)) → mult106_out_ga(s(T279), s(s(s(T281))))
U12_gga(T234, T237, mult106_out_ga(T234, T237)) → mult12_out_gga(s(T234), s(s(s(0))), s(s(s(T237))))
mult12_in_gga(0, s(s(s(s(0)))), s(s(s(s(0))))) → mult12_out_gga(0, s(s(s(s(0)))), s(s(s(s(0)))))
mult12_in_gga(s(T318), s(s(s(s(0)))), s(s(s(s(T321))))) → U13_gga(T318, T321, mult144_in_ga(T318, T321))
mult144_in_ga(0, s(s(s(s(0))))) → mult144_out_ga(0, s(s(s(s(0)))))
mult144_in_ga(s(T374), s(s(s(s(T376))))) → U5_ga(T374, T376, mult144_in_ga(T374, T376))
U5_ga(T374, T376, mult144_out_ga(T374, T376)) → mult144_out_ga(s(T374), s(s(s(s(T376)))))
U13_gga(T318, T321, mult144_out_ga(T318, T321)) → mult12_out_gga(s(T318), s(s(s(s(0)))), s(s(s(s(T321)))))
mult12_in_gga(0, s(s(s(s(s(0))))), s(s(s(s(s(0)))))) → mult12_out_gga(0, s(s(s(s(s(0))))), s(s(s(s(s(0))))))
mult12_in_gga(s(T413), s(s(s(s(s(0))))), s(s(s(s(s(T416)))))) → U14_gga(T413, T416, mult187_in_ga(T413, T416))
mult187_in_ga(0, s(s(s(s(s(0)))))) → mult187_out_ga(0, s(s(s(s(s(0))))))
mult187_in_ga(s(T480), s(s(s(s(s(T482)))))) → U6_ga(T480, T482, mult187_in_ga(T480, T482))
U6_ga(T480, T482, mult187_out_ga(T480, T482)) → mult187_out_ga(s(T480), s(s(s(s(s(T482))))))
U14_gga(T413, T416, mult187_out_ga(T413, T416)) → mult12_out_gga(s(T413), s(s(s(s(s(0))))), s(s(s(s(s(T416))))))
mult12_in_gga(0, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(0))))))) → mult12_out_gga(0, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(0)))))))
mult12_in_gga(s(T519), s(s(s(s(s(s(0)))))), s(s(s(s(s(s(T522))))))) → U15_gga(T519, T522, mult235_in_ga(T519, T522))
mult235_in_ga(0, s(s(s(s(s(s(0))))))) → mult235_out_ga(0, s(s(s(s(s(s(0)))))))
mult235_in_ga(s(T597), s(s(s(s(s(s(T599))))))) → U7_ga(T597, T599, mult235_in_ga(T597, T599))
U7_ga(T597, T599, mult235_out_ga(T597, T599)) → mult235_out_ga(s(T597), s(s(s(s(s(s(T599)))))))
U15_gga(T519, T522, mult235_out_ga(T519, T522)) → mult12_out_gga(s(T519), s(s(s(s(s(s(0)))))), s(s(s(s(s(s(T522)))))))
mult12_in_gga(0, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(0)))))))) → mult12_out_gga(0, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(0))))))))
mult12_in_gga(s(T636), s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(T639)))))))) → U16_gga(T636, T639, mult288_in_ga(T636, T639))
mult288_in_ga(0, s(s(s(s(s(s(s(0)))))))) → mult288_out_ga(0, s(s(s(s(s(s(s(0))))))))
mult288_in_ga(s(T725), s(s(s(s(s(s(s(T727)))))))) → U8_ga(T725, T727, mult288_in_ga(T725, T727))
U8_ga(T725, T727, mult288_out_ga(T725, T727)) → mult288_out_ga(s(T725), s(s(s(s(s(s(s(T727))))))))
U16_gga(T636, T639, mult288_out_ga(T636, T639)) → mult12_out_gga(s(T636), s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(T639))))))))
mult12_in_gga(T740, s(s(s(s(s(s(s(s(T742)))))))), s(s(s(s(s(s(s(s(T744))))))))) → U17_gga(T740, T742, T744, mult338_in_ggga(T740, s(s(s(s(s(s(s(T742))))))), T742, T744))
mult338_in_ggga(0, T754, 0, 0) → mult338_out_ggga(0, T754, 0, 0)
mult338_in_ggga(s(T767), T768, 0, T770) → U18_ggga(T767, T768, T770, mult12_in_gga(T767, s(T768), T770))
U18_ggga(T767, T768, T770, mult12_out_gga(T767, s(T768), T770)) → mult338_out_ggga(s(T767), T768, 0, T770)
mult338_in_ggga(T786, T787, s(T788), s(T790)) → U19_ggga(T786, T787, T788, T790, mult338_in_ggga(T786, T787, T788, T790))
U19_ggga(T786, T787, T788, T790, mult338_out_ggga(T786, T787, T788, T790)) → mult338_out_ggga(T786, T787, s(T788), s(T790))
U17_gga(T740, T742, T744, mult338_out_ggga(T740, s(s(s(s(s(s(s(T742))))))), T742, T744)) → mult12_out_gga(T740, s(s(s(s(s(s(s(s(T742)))))))), s(s(s(s(s(s(s(s(T744)))))))))
U20_gga(T28, T29, T31, mult12_out_gga(T28, T29, T31)) → times1_out_gga(s(T28), T29, T31)

The argument filtering Pi contains the following mapping:
times1_in_gga(x1, x2, x3)  =  times1_in_gga(x1, x2)
0  =  0
times1_out_gga(x1, x2, x3)  =  times1_out_gga(x3)
s(x1)  =  s(x1)
U20_gga(x1, x2, x3, x4)  =  U20_gga(x4)
mult12_in_gga(x1, x2, x3)  =  mult12_in_gga(x1, x2)
mult12_out_gga(x1, x2, x3)  =  mult12_out_gga(x3)
U9_gga(x1, x2, x3)  =  U9_gga(x3)
mult22_in_ga(x1, x2)  =  mult22_in_ga(x1)
mult22_out_ga(x1, x2)  =  mult22_out_ga(x2)
U1_ga(x1, x2, x3)  =  U1_ga(x3)
U10_gga(x1, x2, x3)  =  U10_gga(x3)
mult45_in_ga(x1, x2)  =  mult45_in_ga(x1)
mult45_out_ga(x1, x2)  =  mult45_out_ga(x2)
U2_ga(x1, x2, x3)  =  U2_ga(x3)
U11_gga(x1, x2, x3)  =  U11_gga(x3)
mult73_in_ga(x1, x2)  =  mult73_in_ga(x1)
mult73_out_ga(x1, x2)  =  mult73_out_ga(x2)
U3_ga(x1, x2, x3)  =  U3_ga(x3)
U12_gga(x1, x2, x3)  =  U12_gga(x3)
mult106_in_ga(x1, x2)  =  mult106_in_ga(x1)
mult106_out_ga(x1, x2)  =  mult106_out_ga(x2)
U4_ga(x1, x2, x3)  =  U4_ga(x3)
U13_gga(x1, x2, x3)  =  U13_gga(x3)
mult144_in_ga(x1, x2)  =  mult144_in_ga(x1)
mult144_out_ga(x1, x2)  =  mult144_out_ga(x2)
U5_ga(x1, x2, x3)  =  U5_ga(x3)
U14_gga(x1, x2, x3)  =  U14_gga(x3)
mult187_in_ga(x1, x2)  =  mult187_in_ga(x1)
mult187_out_ga(x1, x2)  =  mult187_out_ga(x2)
U6_ga(x1, x2, x3)  =  U6_ga(x3)
U15_gga(x1, x2, x3)  =  U15_gga(x3)
mult235_in_ga(x1, x2)  =  mult235_in_ga(x1)
mult235_out_ga(x1, x2)  =  mult235_out_ga(x2)
U7_ga(x1, x2, x3)  =  U7_ga(x3)
U16_gga(x1, x2, x3)  =  U16_gga(x3)
mult288_in_ga(x1, x2)  =  mult288_in_ga(x1)
mult288_out_ga(x1, x2)  =  mult288_out_ga(x2)
U8_ga(x1, x2, x3)  =  U8_ga(x3)
U17_gga(x1, x2, x3, x4)  =  U17_gga(x4)
mult338_in_ggga(x1, x2, x3, x4)  =  mult338_in_ggga(x1, x2, x3)
mult338_out_ggga(x1, x2, x3, x4)  =  mult338_out_ggga(x4)
U18_ggga(x1, x2, x3, x4)  =  U18_ggga(x4)
U19_ggga(x1, x2, x3, x4, x5)  =  U19_ggga(x5)
MULT235_IN_GA(x1, x2)  =  MULT235_IN_GA(x1)

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

(17) UsableRulesProof (EQUIVALENT transformation)

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

(18) Obligation:

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

MULT235_IN_GA(s(T597), s(s(s(s(s(s(T599))))))) → MULT235_IN_GA(T597, T599)

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

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

(19) PiDPToQDPProof (SOUND transformation)

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

(20) Obligation:

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

MULT235_IN_GA(s(T597)) → MULT235_IN_GA(T597)

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

(21) 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:

  • MULT235_IN_GA(s(T597)) → MULT235_IN_GA(T597)
    The graph contains the following edges 1 > 1

(22) YES

(23) Obligation:

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

MULT187_IN_GA(s(T480), s(s(s(s(s(T482)))))) → MULT187_IN_GA(T480, T482)

The TRS R consists of the following rules:

times1_in_gga(0, T15, 0) → times1_out_gga(0, T15, 0)
times1_in_gga(s(T28), T29, T31) → U20_gga(T28, T29, T31, mult12_in_gga(T28, T29, T31))
mult12_in_gga(0, 0, 0) → mult12_out_gga(0, 0, 0)
mult12_in_gga(s(T51), 0, T54) → U9_gga(T51, T54, mult22_in_ga(T51, T54))
mult22_in_ga(0, 0) → mult22_out_ga(0, 0)
mult22_in_ga(s(T63), T65) → U1_ga(T63, T65, mult22_in_ga(T63, T65))
U1_ga(T63, T65, mult22_out_ga(T63, T65)) → mult22_out_ga(s(T63), T65)
U9_gga(T51, T54, mult22_out_ga(T51, T54)) → mult12_out_gga(s(T51), 0, T54)
mult12_in_gga(0, s(0), s(0)) → mult12_out_gga(0, s(0), s(0))
mult12_in_gga(s(T99), s(0), s(T102)) → U10_gga(T99, T102, mult45_in_ga(T99, T102))
mult45_in_ga(0, s(0)) → mult45_out_ga(0, s(0))
mult45_in_ga(s(T122), s(T124)) → U2_ga(T122, T124, mult45_in_ga(T122, T124))
U2_ga(T122, T124, mult45_out_ga(T122, T124)) → mult45_out_ga(s(T122), s(T124))
U10_gga(T99, T102, mult45_out_ga(T99, T102)) → mult12_out_gga(s(T99), s(0), s(T102))
mult12_in_gga(0, s(s(0)), s(s(0))) → mult12_out_gga(0, s(s(0)), s(s(0)))
mult12_in_gga(s(T161), s(s(0)), s(s(T164))) → U11_gga(T161, T164, mult73_in_ga(T161, T164))
mult73_in_ga(0, s(s(0))) → mult73_out_ga(0, s(s(0)))
mult73_in_ga(s(T195), s(s(T197))) → U3_ga(T195, T197, mult73_in_ga(T195, T197))
U3_ga(T195, T197, mult73_out_ga(T195, T197)) → mult73_out_ga(s(T195), s(s(T197)))
U11_gga(T161, T164, mult73_out_ga(T161, T164)) → mult12_out_gga(s(T161), s(s(0)), s(s(T164)))
mult12_in_gga(0, s(s(s(0))), s(s(s(0)))) → mult12_out_gga(0, s(s(s(0))), s(s(s(0))))
mult12_in_gga(s(T234), s(s(s(0))), s(s(s(T237)))) → U12_gga(T234, T237, mult106_in_ga(T234, T237))
mult106_in_ga(0, s(s(s(0)))) → mult106_out_ga(0, s(s(s(0))))
mult106_in_ga(s(T279), s(s(s(T281)))) → U4_ga(T279, T281, mult106_in_ga(T279, T281))
U4_ga(T279, T281, mult106_out_ga(T279, T281)) → mult106_out_ga(s(T279), s(s(s(T281))))
U12_gga(T234, T237, mult106_out_ga(T234, T237)) → mult12_out_gga(s(T234), s(s(s(0))), s(s(s(T237))))
mult12_in_gga(0, s(s(s(s(0)))), s(s(s(s(0))))) → mult12_out_gga(0, s(s(s(s(0)))), s(s(s(s(0)))))
mult12_in_gga(s(T318), s(s(s(s(0)))), s(s(s(s(T321))))) → U13_gga(T318, T321, mult144_in_ga(T318, T321))
mult144_in_ga(0, s(s(s(s(0))))) → mult144_out_ga(0, s(s(s(s(0)))))
mult144_in_ga(s(T374), s(s(s(s(T376))))) → U5_ga(T374, T376, mult144_in_ga(T374, T376))
U5_ga(T374, T376, mult144_out_ga(T374, T376)) → mult144_out_ga(s(T374), s(s(s(s(T376)))))
U13_gga(T318, T321, mult144_out_ga(T318, T321)) → mult12_out_gga(s(T318), s(s(s(s(0)))), s(s(s(s(T321)))))
mult12_in_gga(0, s(s(s(s(s(0))))), s(s(s(s(s(0)))))) → mult12_out_gga(0, s(s(s(s(s(0))))), s(s(s(s(s(0))))))
mult12_in_gga(s(T413), s(s(s(s(s(0))))), s(s(s(s(s(T416)))))) → U14_gga(T413, T416, mult187_in_ga(T413, T416))
mult187_in_ga(0, s(s(s(s(s(0)))))) → mult187_out_ga(0, s(s(s(s(s(0))))))
mult187_in_ga(s(T480), s(s(s(s(s(T482)))))) → U6_ga(T480, T482, mult187_in_ga(T480, T482))
U6_ga(T480, T482, mult187_out_ga(T480, T482)) → mult187_out_ga(s(T480), s(s(s(s(s(T482))))))
U14_gga(T413, T416, mult187_out_ga(T413, T416)) → mult12_out_gga(s(T413), s(s(s(s(s(0))))), s(s(s(s(s(T416))))))
mult12_in_gga(0, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(0))))))) → mult12_out_gga(0, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(0)))))))
mult12_in_gga(s(T519), s(s(s(s(s(s(0)))))), s(s(s(s(s(s(T522))))))) → U15_gga(T519, T522, mult235_in_ga(T519, T522))
mult235_in_ga(0, s(s(s(s(s(s(0))))))) → mult235_out_ga(0, s(s(s(s(s(s(0)))))))
mult235_in_ga(s(T597), s(s(s(s(s(s(T599))))))) → U7_ga(T597, T599, mult235_in_ga(T597, T599))
U7_ga(T597, T599, mult235_out_ga(T597, T599)) → mult235_out_ga(s(T597), s(s(s(s(s(s(T599)))))))
U15_gga(T519, T522, mult235_out_ga(T519, T522)) → mult12_out_gga(s(T519), s(s(s(s(s(s(0)))))), s(s(s(s(s(s(T522)))))))
mult12_in_gga(0, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(0)))))))) → mult12_out_gga(0, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(0))))))))
mult12_in_gga(s(T636), s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(T639)))))))) → U16_gga(T636, T639, mult288_in_ga(T636, T639))
mult288_in_ga(0, s(s(s(s(s(s(s(0)))))))) → mult288_out_ga(0, s(s(s(s(s(s(s(0))))))))
mult288_in_ga(s(T725), s(s(s(s(s(s(s(T727)))))))) → U8_ga(T725, T727, mult288_in_ga(T725, T727))
U8_ga(T725, T727, mult288_out_ga(T725, T727)) → mult288_out_ga(s(T725), s(s(s(s(s(s(s(T727))))))))
U16_gga(T636, T639, mult288_out_ga(T636, T639)) → mult12_out_gga(s(T636), s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(T639))))))))
mult12_in_gga(T740, s(s(s(s(s(s(s(s(T742)))))))), s(s(s(s(s(s(s(s(T744))))))))) → U17_gga(T740, T742, T744, mult338_in_ggga(T740, s(s(s(s(s(s(s(T742))))))), T742, T744))
mult338_in_ggga(0, T754, 0, 0) → mult338_out_ggga(0, T754, 0, 0)
mult338_in_ggga(s(T767), T768, 0, T770) → U18_ggga(T767, T768, T770, mult12_in_gga(T767, s(T768), T770))
U18_ggga(T767, T768, T770, mult12_out_gga(T767, s(T768), T770)) → mult338_out_ggga(s(T767), T768, 0, T770)
mult338_in_ggga(T786, T787, s(T788), s(T790)) → U19_ggga(T786, T787, T788, T790, mult338_in_ggga(T786, T787, T788, T790))
U19_ggga(T786, T787, T788, T790, mult338_out_ggga(T786, T787, T788, T790)) → mult338_out_ggga(T786, T787, s(T788), s(T790))
U17_gga(T740, T742, T744, mult338_out_ggga(T740, s(s(s(s(s(s(s(T742))))))), T742, T744)) → mult12_out_gga(T740, s(s(s(s(s(s(s(s(T742)))))))), s(s(s(s(s(s(s(s(T744)))))))))
U20_gga(T28, T29, T31, mult12_out_gga(T28, T29, T31)) → times1_out_gga(s(T28), T29, T31)

The argument filtering Pi contains the following mapping:
times1_in_gga(x1, x2, x3)  =  times1_in_gga(x1, x2)
0  =  0
times1_out_gga(x1, x2, x3)  =  times1_out_gga(x3)
s(x1)  =  s(x1)
U20_gga(x1, x2, x3, x4)  =  U20_gga(x4)
mult12_in_gga(x1, x2, x3)  =  mult12_in_gga(x1, x2)
mult12_out_gga(x1, x2, x3)  =  mult12_out_gga(x3)
U9_gga(x1, x2, x3)  =  U9_gga(x3)
mult22_in_ga(x1, x2)  =  mult22_in_ga(x1)
mult22_out_ga(x1, x2)  =  mult22_out_ga(x2)
U1_ga(x1, x2, x3)  =  U1_ga(x3)
U10_gga(x1, x2, x3)  =  U10_gga(x3)
mult45_in_ga(x1, x2)  =  mult45_in_ga(x1)
mult45_out_ga(x1, x2)  =  mult45_out_ga(x2)
U2_ga(x1, x2, x3)  =  U2_ga(x3)
U11_gga(x1, x2, x3)  =  U11_gga(x3)
mult73_in_ga(x1, x2)  =  mult73_in_ga(x1)
mult73_out_ga(x1, x2)  =  mult73_out_ga(x2)
U3_ga(x1, x2, x3)  =  U3_ga(x3)
U12_gga(x1, x2, x3)  =  U12_gga(x3)
mult106_in_ga(x1, x2)  =  mult106_in_ga(x1)
mult106_out_ga(x1, x2)  =  mult106_out_ga(x2)
U4_ga(x1, x2, x3)  =  U4_ga(x3)
U13_gga(x1, x2, x3)  =  U13_gga(x3)
mult144_in_ga(x1, x2)  =  mult144_in_ga(x1)
mult144_out_ga(x1, x2)  =  mult144_out_ga(x2)
U5_ga(x1, x2, x3)  =  U5_ga(x3)
U14_gga(x1, x2, x3)  =  U14_gga(x3)
mult187_in_ga(x1, x2)  =  mult187_in_ga(x1)
mult187_out_ga(x1, x2)  =  mult187_out_ga(x2)
U6_ga(x1, x2, x3)  =  U6_ga(x3)
U15_gga(x1, x2, x3)  =  U15_gga(x3)
mult235_in_ga(x1, x2)  =  mult235_in_ga(x1)
mult235_out_ga(x1, x2)  =  mult235_out_ga(x2)
U7_ga(x1, x2, x3)  =  U7_ga(x3)
U16_gga(x1, x2, x3)  =  U16_gga(x3)
mult288_in_ga(x1, x2)  =  mult288_in_ga(x1)
mult288_out_ga(x1, x2)  =  mult288_out_ga(x2)
U8_ga(x1, x2, x3)  =  U8_ga(x3)
U17_gga(x1, x2, x3, x4)  =  U17_gga(x4)
mult338_in_ggga(x1, x2, x3, x4)  =  mult338_in_ggga(x1, x2, x3)
mult338_out_ggga(x1, x2, x3, x4)  =  mult338_out_ggga(x4)
U18_ggga(x1, x2, x3, x4)  =  U18_ggga(x4)
U19_ggga(x1, x2, x3, x4, x5)  =  U19_ggga(x5)
MULT187_IN_GA(x1, x2)  =  MULT187_IN_GA(x1)

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

(24) UsableRulesProof (EQUIVALENT transformation)

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

(25) Obligation:

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

MULT187_IN_GA(s(T480), s(s(s(s(s(T482)))))) → MULT187_IN_GA(T480, T482)

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

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

(26) PiDPToQDPProof (SOUND transformation)

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

(27) Obligation:

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

MULT187_IN_GA(s(T480)) → MULT187_IN_GA(T480)

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

(28) 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:

  • MULT187_IN_GA(s(T480)) → MULT187_IN_GA(T480)
    The graph contains the following edges 1 > 1

(29) YES

(30) Obligation:

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

MULT144_IN_GA(s(T374), s(s(s(s(T376))))) → MULT144_IN_GA(T374, T376)

The TRS R consists of the following rules:

times1_in_gga(0, T15, 0) → times1_out_gga(0, T15, 0)
times1_in_gga(s(T28), T29, T31) → U20_gga(T28, T29, T31, mult12_in_gga(T28, T29, T31))
mult12_in_gga(0, 0, 0) → mult12_out_gga(0, 0, 0)
mult12_in_gga(s(T51), 0, T54) → U9_gga(T51, T54, mult22_in_ga(T51, T54))
mult22_in_ga(0, 0) → mult22_out_ga(0, 0)
mult22_in_ga(s(T63), T65) → U1_ga(T63, T65, mult22_in_ga(T63, T65))
U1_ga(T63, T65, mult22_out_ga(T63, T65)) → mult22_out_ga(s(T63), T65)
U9_gga(T51, T54, mult22_out_ga(T51, T54)) → mult12_out_gga(s(T51), 0, T54)
mult12_in_gga(0, s(0), s(0)) → mult12_out_gga(0, s(0), s(0))
mult12_in_gga(s(T99), s(0), s(T102)) → U10_gga(T99, T102, mult45_in_ga(T99, T102))
mult45_in_ga(0, s(0)) → mult45_out_ga(0, s(0))
mult45_in_ga(s(T122), s(T124)) → U2_ga(T122, T124, mult45_in_ga(T122, T124))
U2_ga(T122, T124, mult45_out_ga(T122, T124)) → mult45_out_ga(s(T122), s(T124))
U10_gga(T99, T102, mult45_out_ga(T99, T102)) → mult12_out_gga(s(T99), s(0), s(T102))
mult12_in_gga(0, s(s(0)), s(s(0))) → mult12_out_gga(0, s(s(0)), s(s(0)))
mult12_in_gga(s(T161), s(s(0)), s(s(T164))) → U11_gga(T161, T164, mult73_in_ga(T161, T164))
mult73_in_ga(0, s(s(0))) → mult73_out_ga(0, s(s(0)))
mult73_in_ga(s(T195), s(s(T197))) → U3_ga(T195, T197, mult73_in_ga(T195, T197))
U3_ga(T195, T197, mult73_out_ga(T195, T197)) → mult73_out_ga(s(T195), s(s(T197)))
U11_gga(T161, T164, mult73_out_ga(T161, T164)) → mult12_out_gga(s(T161), s(s(0)), s(s(T164)))
mult12_in_gga(0, s(s(s(0))), s(s(s(0)))) → mult12_out_gga(0, s(s(s(0))), s(s(s(0))))
mult12_in_gga(s(T234), s(s(s(0))), s(s(s(T237)))) → U12_gga(T234, T237, mult106_in_ga(T234, T237))
mult106_in_ga(0, s(s(s(0)))) → mult106_out_ga(0, s(s(s(0))))
mult106_in_ga(s(T279), s(s(s(T281)))) → U4_ga(T279, T281, mult106_in_ga(T279, T281))
U4_ga(T279, T281, mult106_out_ga(T279, T281)) → mult106_out_ga(s(T279), s(s(s(T281))))
U12_gga(T234, T237, mult106_out_ga(T234, T237)) → mult12_out_gga(s(T234), s(s(s(0))), s(s(s(T237))))
mult12_in_gga(0, s(s(s(s(0)))), s(s(s(s(0))))) → mult12_out_gga(0, s(s(s(s(0)))), s(s(s(s(0)))))
mult12_in_gga(s(T318), s(s(s(s(0)))), s(s(s(s(T321))))) → U13_gga(T318, T321, mult144_in_ga(T318, T321))
mult144_in_ga(0, s(s(s(s(0))))) → mult144_out_ga(0, s(s(s(s(0)))))
mult144_in_ga(s(T374), s(s(s(s(T376))))) → U5_ga(T374, T376, mult144_in_ga(T374, T376))
U5_ga(T374, T376, mult144_out_ga(T374, T376)) → mult144_out_ga(s(T374), s(s(s(s(T376)))))
U13_gga(T318, T321, mult144_out_ga(T318, T321)) → mult12_out_gga(s(T318), s(s(s(s(0)))), s(s(s(s(T321)))))
mult12_in_gga(0, s(s(s(s(s(0))))), s(s(s(s(s(0)))))) → mult12_out_gga(0, s(s(s(s(s(0))))), s(s(s(s(s(0))))))
mult12_in_gga(s(T413), s(s(s(s(s(0))))), s(s(s(s(s(T416)))))) → U14_gga(T413, T416, mult187_in_ga(T413, T416))
mult187_in_ga(0, s(s(s(s(s(0)))))) → mult187_out_ga(0, s(s(s(s(s(0))))))
mult187_in_ga(s(T480), s(s(s(s(s(T482)))))) → U6_ga(T480, T482, mult187_in_ga(T480, T482))
U6_ga(T480, T482, mult187_out_ga(T480, T482)) → mult187_out_ga(s(T480), s(s(s(s(s(T482))))))
U14_gga(T413, T416, mult187_out_ga(T413, T416)) → mult12_out_gga(s(T413), s(s(s(s(s(0))))), s(s(s(s(s(T416))))))
mult12_in_gga(0, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(0))))))) → mult12_out_gga(0, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(0)))))))
mult12_in_gga(s(T519), s(s(s(s(s(s(0)))))), s(s(s(s(s(s(T522))))))) → U15_gga(T519, T522, mult235_in_ga(T519, T522))
mult235_in_ga(0, s(s(s(s(s(s(0))))))) → mult235_out_ga(0, s(s(s(s(s(s(0)))))))
mult235_in_ga(s(T597), s(s(s(s(s(s(T599))))))) → U7_ga(T597, T599, mult235_in_ga(T597, T599))
U7_ga(T597, T599, mult235_out_ga(T597, T599)) → mult235_out_ga(s(T597), s(s(s(s(s(s(T599)))))))
U15_gga(T519, T522, mult235_out_ga(T519, T522)) → mult12_out_gga(s(T519), s(s(s(s(s(s(0)))))), s(s(s(s(s(s(T522)))))))
mult12_in_gga(0, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(0)))))))) → mult12_out_gga(0, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(0))))))))
mult12_in_gga(s(T636), s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(T639)))))))) → U16_gga(T636, T639, mult288_in_ga(T636, T639))
mult288_in_ga(0, s(s(s(s(s(s(s(0)))))))) → mult288_out_ga(0, s(s(s(s(s(s(s(0))))))))
mult288_in_ga(s(T725), s(s(s(s(s(s(s(T727)))))))) → U8_ga(T725, T727, mult288_in_ga(T725, T727))
U8_ga(T725, T727, mult288_out_ga(T725, T727)) → mult288_out_ga(s(T725), s(s(s(s(s(s(s(T727))))))))
U16_gga(T636, T639, mult288_out_ga(T636, T639)) → mult12_out_gga(s(T636), s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(T639))))))))
mult12_in_gga(T740, s(s(s(s(s(s(s(s(T742)))))))), s(s(s(s(s(s(s(s(T744))))))))) → U17_gga(T740, T742, T744, mult338_in_ggga(T740, s(s(s(s(s(s(s(T742))))))), T742, T744))
mult338_in_ggga(0, T754, 0, 0) → mult338_out_ggga(0, T754, 0, 0)
mult338_in_ggga(s(T767), T768, 0, T770) → U18_ggga(T767, T768, T770, mult12_in_gga(T767, s(T768), T770))
U18_ggga(T767, T768, T770, mult12_out_gga(T767, s(T768), T770)) → mult338_out_ggga(s(T767), T768, 0, T770)
mult338_in_ggga(T786, T787, s(T788), s(T790)) → U19_ggga(T786, T787, T788, T790, mult338_in_ggga(T786, T787, T788, T790))
U19_ggga(T786, T787, T788, T790, mult338_out_ggga(T786, T787, T788, T790)) → mult338_out_ggga(T786, T787, s(T788), s(T790))
U17_gga(T740, T742, T744, mult338_out_ggga(T740, s(s(s(s(s(s(s(T742))))))), T742, T744)) → mult12_out_gga(T740, s(s(s(s(s(s(s(s(T742)))))))), s(s(s(s(s(s(s(s(T744)))))))))
U20_gga(T28, T29, T31, mult12_out_gga(T28, T29, T31)) → times1_out_gga(s(T28), T29, T31)

The argument filtering Pi contains the following mapping:
times1_in_gga(x1, x2, x3)  =  times1_in_gga(x1, x2)
0  =  0
times1_out_gga(x1, x2, x3)  =  times1_out_gga(x3)
s(x1)  =  s(x1)
U20_gga(x1, x2, x3, x4)  =  U20_gga(x4)
mult12_in_gga(x1, x2, x3)  =  mult12_in_gga(x1, x2)
mult12_out_gga(x1, x2, x3)  =  mult12_out_gga(x3)
U9_gga(x1, x2, x3)  =  U9_gga(x3)
mult22_in_ga(x1, x2)  =  mult22_in_ga(x1)
mult22_out_ga(x1, x2)  =  mult22_out_ga(x2)
U1_ga(x1, x2, x3)  =  U1_ga(x3)
U10_gga(x1, x2, x3)  =  U10_gga(x3)
mult45_in_ga(x1, x2)  =  mult45_in_ga(x1)
mult45_out_ga(x1, x2)  =  mult45_out_ga(x2)
U2_ga(x1, x2, x3)  =  U2_ga(x3)
U11_gga(x1, x2, x3)  =  U11_gga(x3)
mult73_in_ga(x1, x2)  =  mult73_in_ga(x1)
mult73_out_ga(x1, x2)  =  mult73_out_ga(x2)
U3_ga(x1, x2, x3)  =  U3_ga(x3)
U12_gga(x1, x2, x3)  =  U12_gga(x3)
mult106_in_ga(x1, x2)  =  mult106_in_ga(x1)
mult106_out_ga(x1, x2)  =  mult106_out_ga(x2)
U4_ga(x1, x2, x3)  =  U4_ga(x3)
U13_gga(x1, x2, x3)  =  U13_gga(x3)
mult144_in_ga(x1, x2)  =  mult144_in_ga(x1)
mult144_out_ga(x1, x2)  =  mult144_out_ga(x2)
U5_ga(x1, x2, x3)  =  U5_ga(x3)
U14_gga(x1, x2, x3)  =  U14_gga(x3)
mult187_in_ga(x1, x2)  =  mult187_in_ga(x1)
mult187_out_ga(x1, x2)  =  mult187_out_ga(x2)
U6_ga(x1, x2, x3)  =  U6_ga(x3)
U15_gga(x1, x2, x3)  =  U15_gga(x3)
mult235_in_ga(x1, x2)  =  mult235_in_ga(x1)
mult235_out_ga(x1, x2)  =  mult235_out_ga(x2)
U7_ga(x1, x2, x3)  =  U7_ga(x3)
U16_gga(x1, x2, x3)  =  U16_gga(x3)
mult288_in_ga(x1, x2)  =  mult288_in_ga(x1)
mult288_out_ga(x1, x2)  =  mult288_out_ga(x2)
U8_ga(x1, x2, x3)  =  U8_ga(x3)
U17_gga(x1, x2, x3, x4)  =  U17_gga(x4)
mult338_in_ggga(x1, x2, x3, x4)  =  mult338_in_ggga(x1, x2, x3)
mult338_out_ggga(x1, x2, x3, x4)  =  mult338_out_ggga(x4)
U18_ggga(x1, x2, x3, x4)  =  U18_ggga(x4)
U19_ggga(x1, x2, x3, x4, x5)  =  U19_ggga(x5)
MULT144_IN_GA(x1, x2)  =  MULT144_IN_GA(x1)

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

(31) UsableRulesProof (EQUIVALENT transformation)

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

(32) Obligation:

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

MULT144_IN_GA(s(T374), s(s(s(s(T376))))) → MULT144_IN_GA(T374, T376)

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

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

(33) PiDPToQDPProof (SOUND transformation)

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

(34) Obligation:

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

MULT144_IN_GA(s(T374)) → MULT144_IN_GA(T374)

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

(35) 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:

  • MULT144_IN_GA(s(T374)) → MULT144_IN_GA(T374)
    The graph contains the following edges 1 > 1

(36) YES

(37) Obligation:

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

MULT106_IN_GA(s(T279), s(s(s(T281)))) → MULT106_IN_GA(T279, T281)

The TRS R consists of the following rules:

times1_in_gga(0, T15, 0) → times1_out_gga(0, T15, 0)
times1_in_gga(s(T28), T29, T31) → U20_gga(T28, T29, T31, mult12_in_gga(T28, T29, T31))
mult12_in_gga(0, 0, 0) → mult12_out_gga(0, 0, 0)
mult12_in_gga(s(T51), 0, T54) → U9_gga(T51, T54, mult22_in_ga(T51, T54))
mult22_in_ga(0, 0) → mult22_out_ga(0, 0)
mult22_in_ga(s(T63), T65) → U1_ga(T63, T65, mult22_in_ga(T63, T65))
U1_ga(T63, T65, mult22_out_ga(T63, T65)) → mult22_out_ga(s(T63), T65)
U9_gga(T51, T54, mult22_out_ga(T51, T54)) → mult12_out_gga(s(T51), 0, T54)
mult12_in_gga(0, s(0), s(0)) → mult12_out_gga(0, s(0), s(0))
mult12_in_gga(s(T99), s(0), s(T102)) → U10_gga(T99, T102, mult45_in_ga(T99, T102))
mult45_in_ga(0, s(0)) → mult45_out_ga(0, s(0))
mult45_in_ga(s(T122), s(T124)) → U2_ga(T122, T124, mult45_in_ga(T122, T124))
U2_ga(T122, T124, mult45_out_ga(T122, T124)) → mult45_out_ga(s(T122), s(T124))
U10_gga(T99, T102, mult45_out_ga(T99, T102)) → mult12_out_gga(s(T99), s(0), s(T102))
mult12_in_gga(0, s(s(0)), s(s(0))) → mult12_out_gga(0, s(s(0)), s(s(0)))
mult12_in_gga(s(T161), s(s(0)), s(s(T164))) → U11_gga(T161, T164, mult73_in_ga(T161, T164))
mult73_in_ga(0, s(s(0))) → mult73_out_ga(0, s(s(0)))
mult73_in_ga(s(T195), s(s(T197))) → U3_ga(T195, T197, mult73_in_ga(T195, T197))
U3_ga(T195, T197, mult73_out_ga(T195, T197)) → mult73_out_ga(s(T195), s(s(T197)))
U11_gga(T161, T164, mult73_out_ga(T161, T164)) → mult12_out_gga(s(T161), s(s(0)), s(s(T164)))
mult12_in_gga(0, s(s(s(0))), s(s(s(0)))) → mult12_out_gga(0, s(s(s(0))), s(s(s(0))))
mult12_in_gga(s(T234), s(s(s(0))), s(s(s(T237)))) → U12_gga(T234, T237, mult106_in_ga(T234, T237))
mult106_in_ga(0, s(s(s(0)))) → mult106_out_ga(0, s(s(s(0))))
mult106_in_ga(s(T279), s(s(s(T281)))) → U4_ga(T279, T281, mult106_in_ga(T279, T281))
U4_ga(T279, T281, mult106_out_ga(T279, T281)) → mult106_out_ga(s(T279), s(s(s(T281))))
U12_gga(T234, T237, mult106_out_ga(T234, T237)) → mult12_out_gga(s(T234), s(s(s(0))), s(s(s(T237))))
mult12_in_gga(0, s(s(s(s(0)))), s(s(s(s(0))))) → mult12_out_gga(0, s(s(s(s(0)))), s(s(s(s(0)))))
mult12_in_gga(s(T318), s(s(s(s(0)))), s(s(s(s(T321))))) → U13_gga(T318, T321, mult144_in_ga(T318, T321))
mult144_in_ga(0, s(s(s(s(0))))) → mult144_out_ga(0, s(s(s(s(0)))))
mult144_in_ga(s(T374), s(s(s(s(T376))))) → U5_ga(T374, T376, mult144_in_ga(T374, T376))
U5_ga(T374, T376, mult144_out_ga(T374, T376)) → mult144_out_ga(s(T374), s(s(s(s(T376)))))
U13_gga(T318, T321, mult144_out_ga(T318, T321)) → mult12_out_gga(s(T318), s(s(s(s(0)))), s(s(s(s(T321)))))
mult12_in_gga(0, s(s(s(s(s(0))))), s(s(s(s(s(0)))))) → mult12_out_gga(0, s(s(s(s(s(0))))), s(s(s(s(s(0))))))
mult12_in_gga(s(T413), s(s(s(s(s(0))))), s(s(s(s(s(T416)))))) → U14_gga(T413, T416, mult187_in_ga(T413, T416))
mult187_in_ga(0, s(s(s(s(s(0)))))) → mult187_out_ga(0, s(s(s(s(s(0))))))
mult187_in_ga(s(T480), s(s(s(s(s(T482)))))) → U6_ga(T480, T482, mult187_in_ga(T480, T482))
U6_ga(T480, T482, mult187_out_ga(T480, T482)) → mult187_out_ga(s(T480), s(s(s(s(s(T482))))))
U14_gga(T413, T416, mult187_out_ga(T413, T416)) → mult12_out_gga(s(T413), s(s(s(s(s(0))))), s(s(s(s(s(T416))))))
mult12_in_gga(0, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(0))))))) → mult12_out_gga(0, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(0)))))))
mult12_in_gga(s(T519), s(s(s(s(s(s(0)))))), s(s(s(s(s(s(T522))))))) → U15_gga(T519, T522, mult235_in_ga(T519, T522))
mult235_in_ga(0, s(s(s(s(s(s(0))))))) → mult235_out_ga(0, s(s(s(s(s(s(0)))))))
mult235_in_ga(s(T597), s(s(s(s(s(s(T599))))))) → U7_ga(T597, T599, mult235_in_ga(T597, T599))
U7_ga(T597, T599, mult235_out_ga(T597, T599)) → mult235_out_ga(s(T597), s(s(s(s(s(s(T599)))))))
U15_gga(T519, T522, mult235_out_ga(T519, T522)) → mult12_out_gga(s(T519), s(s(s(s(s(s(0)))))), s(s(s(s(s(s(T522)))))))
mult12_in_gga(0, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(0)))))))) → mult12_out_gga(0, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(0))))))))
mult12_in_gga(s(T636), s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(T639)))))))) → U16_gga(T636, T639, mult288_in_ga(T636, T639))
mult288_in_ga(0, s(s(s(s(s(s(s(0)))))))) → mult288_out_ga(0, s(s(s(s(s(s(s(0))))))))
mult288_in_ga(s(T725), s(s(s(s(s(s(s(T727)))))))) → U8_ga(T725, T727, mult288_in_ga(T725, T727))
U8_ga(T725, T727, mult288_out_ga(T725, T727)) → mult288_out_ga(s(T725), s(s(s(s(s(s(s(T727))))))))
U16_gga(T636, T639, mult288_out_ga(T636, T639)) → mult12_out_gga(s(T636), s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(T639))))))))
mult12_in_gga(T740, s(s(s(s(s(s(s(s(T742)))))))), s(s(s(s(s(s(s(s(T744))))))))) → U17_gga(T740, T742, T744, mult338_in_ggga(T740, s(s(s(s(s(s(s(T742))))))), T742, T744))
mult338_in_ggga(0, T754, 0, 0) → mult338_out_ggga(0, T754, 0, 0)
mult338_in_ggga(s(T767), T768, 0, T770) → U18_ggga(T767, T768, T770, mult12_in_gga(T767, s(T768), T770))
U18_ggga(T767, T768, T770, mult12_out_gga(T767, s(T768), T770)) → mult338_out_ggga(s(T767), T768, 0, T770)
mult338_in_ggga(T786, T787, s(T788), s(T790)) → U19_ggga(T786, T787, T788, T790, mult338_in_ggga(T786, T787, T788, T790))
U19_ggga(T786, T787, T788, T790, mult338_out_ggga(T786, T787, T788, T790)) → mult338_out_ggga(T786, T787, s(T788), s(T790))
U17_gga(T740, T742, T744, mult338_out_ggga(T740, s(s(s(s(s(s(s(T742))))))), T742, T744)) → mult12_out_gga(T740, s(s(s(s(s(s(s(s(T742)))))))), s(s(s(s(s(s(s(s(T744)))))))))
U20_gga(T28, T29, T31, mult12_out_gga(T28, T29, T31)) → times1_out_gga(s(T28), T29, T31)

The argument filtering Pi contains the following mapping:
times1_in_gga(x1, x2, x3)  =  times1_in_gga(x1, x2)
0  =  0
times1_out_gga(x1, x2, x3)  =  times1_out_gga(x3)
s(x1)  =  s(x1)
U20_gga(x1, x2, x3, x4)  =  U20_gga(x4)
mult12_in_gga(x1, x2, x3)  =  mult12_in_gga(x1, x2)
mult12_out_gga(x1, x2, x3)  =  mult12_out_gga(x3)
U9_gga(x1, x2, x3)  =  U9_gga(x3)
mult22_in_ga(x1, x2)  =  mult22_in_ga(x1)
mult22_out_ga(x1, x2)  =  mult22_out_ga(x2)
U1_ga(x1, x2, x3)  =  U1_ga(x3)
U10_gga(x1, x2, x3)  =  U10_gga(x3)
mult45_in_ga(x1, x2)  =  mult45_in_ga(x1)
mult45_out_ga(x1, x2)  =  mult45_out_ga(x2)
U2_ga(x1, x2, x3)  =  U2_ga(x3)
U11_gga(x1, x2, x3)  =  U11_gga(x3)
mult73_in_ga(x1, x2)  =  mult73_in_ga(x1)
mult73_out_ga(x1, x2)  =  mult73_out_ga(x2)
U3_ga(x1, x2, x3)  =  U3_ga(x3)
U12_gga(x1, x2, x3)  =  U12_gga(x3)
mult106_in_ga(x1, x2)  =  mult106_in_ga(x1)
mult106_out_ga(x1, x2)  =  mult106_out_ga(x2)
U4_ga(x1, x2, x3)  =  U4_ga(x3)
U13_gga(x1, x2, x3)  =  U13_gga(x3)
mult144_in_ga(x1, x2)  =  mult144_in_ga(x1)
mult144_out_ga(x1, x2)  =  mult144_out_ga(x2)
U5_ga(x1, x2, x3)  =  U5_ga(x3)
U14_gga(x1, x2, x3)  =  U14_gga(x3)
mult187_in_ga(x1, x2)  =  mult187_in_ga(x1)
mult187_out_ga(x1, x2)  =  mult187_out_ga(x2)
U6_ga(x1, x2, x3)  =  U6_ga(x3)
U15_gga(x1, x2, x3)  =  U15_gga(x3)
mult235_in_ga(x1, x2)  =  mult235_in_ga(x1)
mult235_out_ga(x1, x2)  =  mult235_out_ga(x2)
U7_ga(x1, x2, x3)  =  U7_ga(x3)
U16_gga(x1, x2, x3)  =  U16_gga(x3)
mult288_in_ga(x1, x2)  =  mult288_in_ga(x1)
mult288_out_ga(x1, x2)  =  mult288_out_ga(x2)
U8_ga(x1, x2, x3)  =  U8_ga(x3)
U17_gga(x1, x2, x3, x4)  =  U17_gga(x4)
mult338_in_ggga(x1, x2, x3, x4)  =  mult338_in_ggga(x1, x2, x3)
mult338_out_ggga(x1, x2, x3, x4)  =  mult338_out_ggga(x4)
U18_ggga(x1, x2, x3, x4)  =  U18_ggga(x4)
U19_ggga(x1, x2, x3, x4, x5)  =  U19_ggga(x5)
MULT106_IN_GA(x1, x2)  =  MULT106_IN_GA(x1)

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

(38) UsableRulesProof (EQUIVALENT transformation)

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

(39) Obligation:

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

MULT106_IN_GA(s(T279), s(s(s(T281)))) → MULT106_IN_GA(T279, T281)

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

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

(40) PiDPToQDPProof (SOUND transformation)

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

(41) Obligation:

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

MULT106_IN_GA(s(T279)) → MULT106_IN_GA(T279)

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

(42) 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:

  • MULT106_IN_GA(s(T279)) → MULT106_IN_GA(T279)
    The graph contains the following edges 1 > 1

(43) YES

(44) Obligation:

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

MULT73_IN_GA(s(T195), s(s(T197))) → MULT73_IN_GA(T195, T197)

The TRS R consists of the following rules:

times1_in_gga(0, T15, 0) → times1_out_gga(0, T15, 0)
times1_in_gga(s(T28), T29, T31) → U20_gga(T28, T29, T31, mult12_in_gga(T28, T29, T31))
mult12_in_gga(0, 0, 0) → mult12_out_gga(0, 0, 0)
mult12_in_gga(s(T51), 0, T54) → U9_gga(T51, T54, mult22_in_ga(T51, T54))
mult22_in_ga(0, 0) → mult22_out_ga(0, 0)
mult22_in_ga(s(T63), T65) → U1_ga(T63, T65, mult22_in_ga(T63, T65))
U1_ga(T63, T65, mult22_out_ga(T63, T65)) → mult22_out_ga(s(T63), T65)
U9_gga(T51, T54, mult22_out_ga(T51, T54)) → mult12_out_gga(s(T51), 0, T54)
mult12_in_gga(0, s(0), s(0)) → mult12_out_gga(0, s(0), s(0))
mult12_in_gga(s(T99), s(0), s(T102)) → U10_gga(T99, T102, mult45_in_ga(T99, T102))
mult45_in_ga(0, s(0)) → mult45_out_ga(0, s(0))
mult45_in_ga(s(T122), s(T124)) → U2_ga(T122, T124, mult45_in_ga(T122, T124))
U2_ga(T122, T124, mult45_out_ga(T122, T124)) → mult45_out_ga(s(T122), s(T124))
U10_gga(T99, T102, mult45_out_ga(T99, T102)) → mult12_out_gga(s(T99), s(0), s(T102))
mult12_in_gga(0, s(s(0)), s(s(0))) → mult12_out_gga(0, s(s(0)), s(s(0)))
mult12_in_gga(s(T161), s(s(0)), s(s(T164))) → U11_gga(T161, T164, mult73_in_ga(T161, T164))
mult73_in_ga(0, s(s(0))) → mult73_out_ga(0, s(s(0)))
mult73_in_ga(s(T195), s(s(T197))) → U3_ga(T195, T197, mult73_in_ga(T195, T197))
U3_ga(T195, T197, mult73_out_ga(T195, T197)) → mult73_out_ga(s(T195), s(s(T197)))
U11_gga(T161, T164, mult73_out_ga(T161, T164)) → mult12_out_gga(s(T161), s(s(0)), s(s(T164)))
mult12_in_gga(0, s(s(s(0))), s(s(s(0)))) → mult12_out_gga(0, s(s(s(0))), s(s(s(0))))
mult12_in_gga(s(T234), s(s(s(0))), s(s(s(T237)))) → U12_gga(T234, T237, mult106_in_ga(T234, T237))
mult106_in_ga(0, s(s(s(0)))) → mult106_out_ga(0, s(s(s(0))))
mult106_in_ga(s(T279), s(s(s(T281)))) → U4_ga(T279, T281, mult106_in_ga(T279, T281))
U4_ga(T279, T281, mult106_out_ga(T279, T281)) → mult106_out_ga(s(T279), s(s(s(T281))))
U12_gga(T234, T237, mult106_out_ga(T234, T237)) → mult12_out_gga(s(T234), s(s(s(0))), s(s(s(T237))))
mult12_in_gga(0, s(s(s(s(0)))), s(s(s(s(0))))) → mult12_out_gga(0, s(s(s(s(0)))), s(s(s(s(0)))))
mult12_in_gga(s(T318), s(s(s(s(0)))), s(s(s(s(T321))))) → U13_gga(T318, T321, mult144_in_ga(T318, T321))
mult144_in_ga(0, s(s(s(s(0))))) → mult144_out_ga(0, s(s(s(s(0)))))
mult144_in_ga(s(T374), s(s(s(s(T376))))) → U5_ga(T374, T376, mult144_in_ga(T374, T376))
U5_ga(T374, T376, mult144_out_ga(T374, T376)) → mult144_out_ga(s(T374), s(s(s(s(T376)))))
U13_gga(T318, T321, mult144_out_ga(T318, T321)) → mult12_out_gga(s(T318), s(s(s(s(0)))), s(s(s(s(T321)))))
mult12_in_gga(0, s(s(s(s(s(0))))), s(s(s(s(s(0)))))) → mult12_out_gga(0, s(s(s(s(s(0))))), s(s(s(s(s(0))))))
mult12_in_gga(s(T413), s(s(s(s(s(0))))), s(s(s(s(s(T416)))))) → U14_gga(T413, T416, mult187_in_ga(T413, T416))
mult187_in_ga(0, s(s(s(s(s(0)))))) → mult187_out_ga(0, s(s(s(s(s(0))))))
mult187_in_ga(s(T480), s(s(s(s(s(T482)))))) → U6_ga(T480, T482, mult187_in_ga(T480, T482))
U6_ga(T480, T482, mult187_out_ga(T480, T482)) → mult187_out_ga(s(T480), s(s(s(s(s(T482))))))
U14_gga(T413, T416, mult187_out_ga(T413, T416)) → mult12_out_gga(s(T413), s(s(s(s(s(0))))), s(s(s(s(s(T416))))))
mult12_in_gga(0, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(0))))))) → mult12_out_gga(0, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(0)))))))
mult12_in_gga(s(T519), s(s(s(s(s(s(0)))))), s(s(s(s(s(s(T522))))))) → U15_gga(T519, T522, mult235_in_ga(T519, T522))
mult235_in_ga(0, s(s(s(s(s(s(0))))))) → mult235_out_ga(0, s(s(s(s(s(s(0)))))))
mult235_in_ga(s(T597), s(s(s(s(s(s(T599))))))) → U7_ga(T597, T599, mult235_in_ga(T597, T599))
U7_ga(T597, T599, mult235_out_ga(T597, T599)) → mult235_out_ga(s(T597), s(s(s(s(s(s(T599)))))))
U15_gga(T519, T522, mult235_out_ga(T519, T522)) → mult12_out_gga(s(T519), s(s(s(s(s(s(0)))))), s(s(s(s(s(s(T522)))))))
mult12_in_gga(0, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(0)))))))) → mult12_out_gga(0, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(0))))))))
mult12_in_gga(s(T636), s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(T639)))))))) → U16_gga(T636, T639, mult288_in_ga(T636, T639))
mult288_in_ga(0, s(s(s(s(s(s(s(0)))))))) → mult288_out_ga(0, s(s(s(s(s(s(s(0))))))))
mult288_in_ga(s(T725), s(s(s(s(s(s(s(T727)))))))) → U8_ga(T725, T727, mult288_in_ga(T725, T727))
U8_ga(T725, T727, mult288_out_ga(T725, T727)) → mult288_out_ga(s(T725), s(s(s(s(s(s(s(T727))))))))
U16_gga(T636, T639, mult288_out_ga(T636, T639)) → mult12_out_gga(s(T636), s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(T639))))))))
mult12_in_gga(T740, s(s(s(s(s(s(s(s(T742)))))))), s(s(s(s(s(s(s(s(T744))))))))) → U17_gga(T740, T742, T744, mult338_in_ggga(T740, s(s(s(s(s(s(s(T742))))))), T742, T744))
mult338_in_ggga(0, T754, 0, 0) → mult338_out_ggga(0, T754, 0, 0)
mult338_in_ggga(s(T767), T768, 0, T770) → U18_ggga(T767, T768, T770, mult12_in_gga(T767, s(T768), T770))
U18_ggga(T767, T768, T770, mult12_out_gga(T767, s(T768), T770)) → mult338_out_ggga(s(T767), T768, 0, T770)
mult338_in_ggga(T786, T787, s(T788), s(T790)) → U19_ggga(T786, T787, T788, T790, mult338_in_ggga(T786, T787, T788, T790))
U19_ggga(T786, T787, T788, T790, mult338_out_ggga(T786, T787, T788, T790)) → mult338_out_ggga(T786, T787, s(T788), s(T790))
U17_gga(T740, T742, T744, mult338_out_ggga(T740, s(s(s(s(s(s(s(T742))))))), T742, T744)) → mult12_out_gga(T740, s(s(s(s(s(s(s(s(T742)))))))), s(s(s(s(s(s(s(s(T744)))))))))
U20_gga(T28, T29, T31, mult12_out_gga(T28, T29, T31)) → times1_out_gga(s(T28), T29, T31)

The argument filtering Pi contains the following mapping:
times1_in_gga(x1, x2, x3)  =  times1_in_gga(x1, x2)
0  =  0
times1_out_gga(x1, x2, x3)  =  times1_out_gga(x3)
s(x1)  =  s(x1)
U20_gga(x1, x2, x3, x4)  =  U20_gga(x4)
mult12_in_gga(x1, x2, x3)  =  mult12_in_gga(x1, x2)
mult12_out_gga(x1, x2, x3)  =  mult12_out_gga(x3)
U9_gga(x1, x2, x3)  =  U9_gga(x3)
mult22_in_ga(x1, x2)  =  mult22_in_ga(x1)
mult22_out_ga(x1, x2)  =  mult22_out_ga(x2)
U1_ga(x1, x2, x3)  =  U1_ga(x3)
U10_gga(x1, x2, x3)  =  U10_gga(x3)
mult45_in_ga(x1, x2)  =  mult45_in_ga(x1)
mult45_out_ga(x1, x2)  =  mult45_out_ga(x2)
U2_ga(x1, x2, x3)  =  U2_ga(x3)
U11_gga(x1, x2, x3)  =  U11_gga(x3)
mult73_in_ga(x1, x2)  =  mult73_in_ga(x1)
mult73_out_ga(x1, x2)  =  mult73_out_ga(x2)
U3_ga(x1, x2, x3)  =  U3_ga(x3)
U12_gga(x1, x2, x3)  =  U12_gga(x3)
mult106_in_ga(x1, x2)  =  mult106_in_ga(x1)
mult106_out_ga(x1, x2)  =  mult106_out_ga(x2)
U4_ga(x1, x2, x3)  =  U4_ga(x3)
U13_gga(x1, x2, x3)  =  U13_gga(x3)
mult144_in_ga(x1, x2)  =  mult144_in_ga(x1)
mult144_out_ga(x1, x2)  =  mult144_out_ga(x2)
U5_ga(x1, x2, x3)  =  U5_ga(x3)
U14_gga(x1, x2, x3)  =  U14_gga(x3)
mult187_in_ga(x1, x2)  =  mult187_in_ga(x1)
mult187_out_ga(x1, x2)  =  mult187_out_ga(x2)
U6_ga(x1, x2, x3)  =  U6_ga(x3)
U15_gga(x1, x2, x3)  =  U15_gga(x3)
mult235_in_ga(x1, x2)  =  mult235_in_ga(x1)
mult235_out_ga(x1, x2)  =  mult235_out_ga(x2)
U7_ga(x1, x2, x3)  =  U7_ga(x3)
U16_gga(x1, x2, x3)  =  U16_gga(x3)
mult288_in_ga(x1, x2)  =  mult288_in_ga(x1)
mult288_out_ga(x1, x2)  =  mult288_out_ga(x2)
U8_ga(x1, x2, x3)  =  U8_ga(x3)
U17_gga(x1, x2, x3, x4)  =  U17_gga(x4)
mult338_in_ggga(x1, x2, x3, x4)  =  mult338_in_ggga(x1, x2, x3)
mult338_out_ggga(x1, x2, x3, x4)  =  mult338_out_ggga(x4)
U18_ggga(x1, x2, x3, x4)  =  U18_ggga(x4)
U19_ggga(x1, x2, x3, x4, x5)  =  U19_ggga(x5)
MULT73_IN_GA(x1, x2)  =  MULT73_IN_GA(x1)

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

(45) UsableRulesProof (EQUIVALENT transformation)

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

(46) Obligation:

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

MULT73_IN_GA(s(T195), s(s(T197))) → MULT73_IN_GA(T195, T197)

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

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

(47) PiDPToQDPProof (SOUND transformation)

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

(48) Obligation:

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

MULT73_IN_GA(s(T195)) → MULT73_IN_GA(T195)

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

(49) 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:

  • MULT73_IN_GA(s(T195)) → MULT73_IN_GA(T195)
    The graph contains the following edges 1 > 1

(50) YES

(51) Obligation:

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

MULT45_IN_GA(s(T122), s(T124)) → MULT45_IN_GA(T122, T124)

The TRS R consists of the following rules:

times1_in_gga(0, T15, 0) → times1_out_gga(0, T15, 0)
times1_in_gga(s(T28), T29, T31) → U20_gga(T28, T29, T31, mult12_in_gga(T28, T29, T31))
mult12_in_gga(0, 0, 0) → mult12_out_gga(0, 0, 0)
mult12_in_gga(s(T51), 0, T54) → U9_gga(T51, T54, mult22_in_ga(T51, T54))
mult22_in_ga(0, 0) → mult22_out_ga(0, 0)
mult22_in_ga(s(T63), T65) → U1_ga(T63, T65, mult22_in_ga(T63, T65))
U1_ga(T63, T65, mult22_out_ga(T63, T65)) → mult22_out_ga(s(T63), T65)
U9_gga(T51, T54, mult22_out_ga(T51, T54)) → mult12_out_gga(s(T51), 0, T54)
mult12_in_gga(0, s(0), s(0)) → mult12_out_gga(0, s(0), s(0))
mult12_in_gga(s(T99), s(0), s(T102)) → U10_gga(T99, T102, mult45_in_ga(T99, T102))
mult45_in_ga(0, s(0)) → mult45_out_ga(0, s(0))
mult45_in_ga(s(T122), s(T124)) → U2_ga(T122, T124, mult45_in_ga(T122, T124))
U2_ga(T122, T124, mult45_out_ga(T122, T124)) → mult45_out_ga(s(T122), s(T124))
U10_gga(T99, T102, mult45_out_ga(T99, T102)) → mult12_out_gga(s(T99), s(0), s(T102))
mult12_in_gga(0, s(s(0)), s(s(0))) → mult12_out_gga(0, s(s(0)), s(s(0)))
mult12_in_gga(s(T161), s(s(0)), s(s(T164))) → U11_gga(T161, T164, mult73_in_ga(T161, T164))
mult73_in_ga(0, s(s(0))) → mult73_out_ga(0, s(s(0)))
mult73_in_ga(s(T195), s(s(T197))) → U3_ga(T195, T197, mult73_in_ga(T195, T197))
U3_ga(T195, T197, mult73_out_ga(T195, T197)) → mult73_out_ga(s(T195), s(s(T197)))
U11_gga(T161, T164, mult73_out_ga(T161, T164)) → mult12_out_gga(s(T161), s(s(0)), s(s(T164)))
mult12_in_gga(0, s(s(s(0))), s(s(s(0)))) → mult12_out_gga(0, s(s(s(0))), s(s(s(0))))
mult12_in_gga(s(T234), s(s(s(0))), s(s(s(T237)))) → U12_gga(T234, T237, mult106_in_ga(T234, T237))
mult106_in_ga(0, s(s(s(0)))) → mult106_out_ga(0, s(s(s(0))))
mult106_in_ga(s(T279), s(s(s(T281)))) → U4_ga(T279, T281, mult106_in_ga(T279, T281))
U4_ga(T279, T281, mult106_out_ga(T279, T281)) → mult106_out_ga(s(T279), s(s(s(T281))))
U12_gga(T234, T237, mult106_out_ga(T234, T237)) → mult12_out_gga(s(T234), s(s(s(0))), s(s(s(T237))))
mult12_in_gga(0, s(s(s(s(0)))), s(s(s(s(0))))) → mult12_out_gga(0, s(s(s(s(0)))), s(s(s(s(0)))))
mult12_in_gga(s(T318), s(s(s(s(0)))), s(s(s(s(T321))))) → U13_gga(T318, T321, mult144_in_ga(T318, T321))
mult144_in_ga(0, s(s(s(s(0))))) → mult144_out_ga(0, s(s(s(s(0)))))
mult144_in_ga(s(T374), s(s(s(s(T376))))) → U5_ga(T374, T376, mult144_in_ga(T374, T376))
U5_ga(T374, T376, mult144_out_ga(T374, T376)) → mult144_out_ga(s(T374), s(s(s(s(T376)))))
U13_gga(T318, T321, mult144_out_ga(T318, T321)) → mult12_out_gga(s(T318), s(s(s(s(0)))), s(s(s(s(T321)))))
mult12_in_gga(0, s(s(s(s(s(0))))), s(s(s(s(s(0)))))) → mult12_out_gga(0, s(s(s(s(s(0))))), s(s(s(s(s(0))))))
mult12_in_gga(s(T413), s(s(s(s(s(0))))), s(s(s(s(s(T416)))))) → U14_gga(T413, T416, mult187_in_ga(T413, T416))
mult187_in_ga(0, s(s(s(s(s(0)))))) → mult187_out_ga(0, s(s(s(s(s(0))))))
mult187_in_ga(s(T480), s(s(s(s(s(T482)))))) → U6_ga(T480, T482, mult187_in_ga(T480, T482))
U6_ga(T480, T482, mult187_out_ga(T480, T482)) → mult187_out_ga(s(T480), s(s(s(s(s(T482))))))
U14_gga(T413, T416, mult187_out_ga(T413, T416)) → mult12_out_gga(s(T413), s(s(s(s(s(0))))), s(s(s(s(s(T416))))))
mult12_in_gga(0, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(0))))))) → mult12_out_gga(0, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(0)))))))
mult12_in_gga(s(T519), s(s(s(s(s(s(0)))))), s(s(s(s(s(s(T522))))))) → U15_gga(T519, T522, mult235_in_ga(T519, T522))
mult235_in_ga(0, s(s(s(s(s(s(0))))))) → mult235_out_ga(0, s(s(s(s(s(s(0)))))))
mult235_in_ga(s(T597), s(s(s(s(s(s(T599))))))) → U7_ga(T597, T599, mult235_in_ga(T597, T599))
U7_ga(T597, T599, mult235_out_ga(T597, T599)) → mult235_out_ga(s(T597), s(s(s(s(s(s(T599)))))))
U15_gga(T519, T522, mult235_out_ga(T519, T522)) → mult12_out_gga(s(T519), s(s(s(s(s(s(0)))))), s(s(s(s(s(s(T522)))))))
mult12_in_gga(0, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(0)))))))) → mult12_out_gga(0, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(0))))))))
mult12_in_gga(s(T636), s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(T639)))))))) → U16_gga(T636, T639, mult288_in_ga(T636, T639))
mult288_in_ga(0, s(s(s(s(s(s(s(0)))))))) → mult288_out_ga(0, s(s(s(s(s(s(s(0))))))))
mult288_in_ga(s(T725), s(s(s(s(s(s(s(T727)))))))) → U8_ga(T725, T727, mult288_in_ga(T725, T727))
U8_ga(T725, T727, mult288_out_ga(T725, T727)) → mult288_out_ga(s(T725), s(s(s(s(s(s(s(T727))))))))
U16_gga(T636, T639, mult288_out_ga(T636, T639)) → mult12_out_gga(s(T636), s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(T639))))))))
mult12_in_gga(T740, s(s(s(s(s(s(s(s(T742)))))))), s(s(s(s(s(s(s(s(T744))))))))) → U17_gga(T740, T742, T744, mult338_in_ggga(T740, s(s(s(s(s(s(s(T742))))))), T742, T744))
mult338_in_ggga(0, T754, 0, 0) → mult338_out_ggga(0, T754, 0, 0)
mult338_in_ggga(s(T767), T768, 0, T770) → U18_ggga(T767, T768, T770, mult12_in_gga(T767, s(T768), T770))
U18_ggga(T767, T768, T770, mult12_out_gga(T767, s(T768), T770)) → mult338_out_ggga(s(T767), T768, 0, T770)
mult338_in_ggga(T786, T787, s(T788), s(T790)) → U19_ggga(T786, T787, T788, T790, mult338_in_ggga(T786, T787, T788, T790))
U19_ggga(T786, T787, T788, T790, mult338_out_ggga(T786, T787, T788, T790)) → mult338_out_ggga(T786, T787, s(T788), s(T790))
U17_gga(T740, T742, T744, mult338_out_ggga(T740, s(s(s(s(s(s(s(T742))))))), T742, T744)) → mult12_out_gga(T740, s(s(s(s(s(s(s(s(T742)))))))), s(s(s(s(s(s(s(s(T744)))))))))
U20_gga(T28, T29, T31, mult12_out_gga(T28, T29, T31)) → times1_out_gga(s(T28), T29, T31)

The argument filtering Pi contains the following mapping:
times1_in_gga(x1, x2, x3)  =  times1_in_gga(x1, x2)
0  =  0
times1_out_gga(x1, x2, x3)  =  times1_out_gga(x3)
s(x1)  =  s(x1)
U20_gga(x1, x2, x3, x4)  =  U20_gga(x4)
mult12_in_gga(x1, x2, x3)  =  mult12_in_gga(x1, x2)
mult12_out_gga(x1, x2, x3)  =  mult12_out_gga(x3)
U9_gga(x1, x2, x3)  =  U9_gga(x3)
mult22_in_ga(x1, x2)  =  mult22_in_ga(x1)
mult22_out_ga(x1, x2)  =  mult22_out_ga(x2)
U1_ga(x1, x2, x3)  =  U1_ga(x3)
U10_gga(x1, x2, x3)  =  U10_gga(x3)
mult45_in_ga(x1, x2)  =  mult45_in_ga(x1)
mult45_out_ga(x1, x2)  =  mult45_out_ga(x2)
U2_ga(x1, x2, x3)  =  U2_ga(x3)
U11_gga(x1, x2, x3)  =  U11_gga(x3)
mult73_in_ga(x1, x2)  =  mult73_in_ga(x1)
mult73_out_ga(x1, x2)  =  mult73_out_ga(x2)
U3_ga(x1, x2, x3)  =  U3_ga(x3)
U12_gga(x1, x2, x3)  =  U12_gga(x3)
mult106_in_ga(x1, x2)  =  mult106_in_ga(x1)
mult106_out_ga(x1, x2)  =  mult106_out_ga(x2)
U4_ga(x1, x2, x3)  =  U4_ga(x3)
U13_gga(x1, x2, x3)  =  U13_gga(x3)
mult144_in_ga(x1, x2)  =  mult144_in_ga(x1)
mult144_out_ga(x1, x2)  =  mult144_out_ga(x2)
U5_ga(x1, x2, x3)  =  U5_ga(x3)
U14_gga(x1, x2, x3)  =  U14_gga(x3)
mult187_in_ga(x1, x2)  =  mult187_in_ga(x1)
mult187_out_ga(x1, x2)  =  mult187_out_ga(x2)
U6_ga(x1, x2, x3)  =  U6_ga(x3)
U15_gga(x1, x2, x3)  =  U15_gga(x3)
mult235_in_ga(x1, x2)  =  mult235_in_ga(x1)
mult235_out_ga(x1, x2)  =  mult235_out_ga(x2)
U7_ga(x1, x2, x3)  =  U7_ga(x3)
U16_gga(x1, x2, x3)  =  U16_gga(x3)
mult288_in_ga(x1, x2)  =  mult288_in_ga(x1)
mult288_out_ga(x1, x2)  =  mult288_out_ga(x2)
U8_ga(x1, x2, x3)  =  U8_ga(x3)
U17_gga(x1, x2, x3, x4)  =  U17_gga(x4)
mult338_in_ggga(x1, x2, x3, x4)  =  mult338_in_ggga(x1, x2, x3)
mult338_out_ggga(x1, x2, x3, x4)  =  mult338_out_ggga(x4)
U18_ggga(x1, x2, x3, x4)  =  U18_ggga(x4)
U19_ggga(x1, x2, x3, x4, x5)  =  U19_ggga(x5)
MULT45_IN_GA(x1, x2)  =  MULT45_IN_GA(x1)

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

(52) UsableRulesProof (EQUIVALENT transformation)

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

(53) Obligation:

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

MULT45_IN_GA(s(T122), s(T124)) → MULT45_IN_GA(T122, T124)

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

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

(54) PiDPToQDPProof (SOUND transformation)

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

(55) Obligation:

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

MULT45_IN_GA(s(T122)) → MULT45_IN_GA(T122)

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

(56) 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:

  • MULT45_IN_GA(s(T122)) → MULT45_IN_GA(T122)
    The graph contains the following edges 1 > 1

(57) YES

(58) Obligation:

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

MULT12_IN_GGA(T740, s(s(s(s(s(s(s(s(T742)))))))), s(s(s(s(s(s(s(s(T744))))))))) → MULT338_IN_GGGA(T740, s(s(s(s(s(s(s(T742))))))), T742, T744)
MULT338_IN_GGGA(s(T767), T768, 0, T770) → MULT12_IN_GGA(T767, s(T768), T770)
MULT338_IN_GGGA(T786, T787, s(T788), s(T790)) → MULT338_IN_GGGA(T786, T787, T788, T790)

The TRS R consists of the following rules:

times1_in_gga(0, T15, 0) → times1_out_gga(0, T15, 0)
times1_in_gga(s(T28), T29, T31) → U20_gga(T28, T29, T31, mult12_in_gga(T28, T29, T31))
mult12_in_gga(0, 0, 0) → mult12_out_gga(0, 0, 0)
mult12_in_gga(s(T51), 0, T54) → U9_gga(T51, T54, mult22_in_ga(T51, T54))
mult22_in_ga(0, 0) → mult22_out_ga(0, 0)
mult22_in_ga(s(T63), T65) → U1_ga(T63, T65, mult22_in_ga(T63, T65))
U1_ga(T63, T65, mult22_out_ga(T63, T65)) → mult22_out_ga(s(T63), T65)
U9_gga(T51, T54, mult22_out_ga(T51, T54)) → mult12_out_gga(s(T51), 0, T54)
mult12_in_gga(0, s(0), s(0)) → mult12_out_gga(0, s(0), s(0))
mult12_in_gga(s(T99), s(0), s(T102)) → U10_gga(T99, T102, mult45_in_ga(T99, T102))
mult45_in_ga(0, s(0)) → mult45_out_ga(0, s(0))
mult45_in_ga(s(T122), s(T124)) → U2_ga(T122, T124, mult45_in_ga(T122, T124))
U2_ga(T122, T124, mult45_out_ga(T122, T124)) → mult45_out_ga(s(T122), s(T124))
U10_gga(T99, T102, mult45_out_ga(T99, T102)) → mult12_out_gga(s(T99), s(0), s(T102))
mult12_in_gga(0, s(s(0)), s(s(0))) → mult12_out_gga(0, s(s(0)), s(s(0)))
mult12_in_gga(s(T161), s(s(0)), s(s(T164))) → U11_gga(T161, T164, mult73_in_ga(T161, T164))
mult73_in_ga(0, s(s(0))) → mult73_out_ga(0, s(s(0)))
mult73_in_ga(s(T195), s(s(T197))) → U3_ga(T195, T197, mult73_in_ga(T195, T197))
U3_ga(T195, T197, mult73_out_ga(T195, T197)) → mult73_out_ga(s(T195), s(s(T197)))
U11_gga(T161, T164, mult73_out_ga(T161, T164)) → mult12_out_gga(s(T161), s(s(0)), s(s(T164)))
mult12_in_gga(0, s(s(s(0))), s(s(s(0)))) → mult12_out_gga(0, s(s(s(0))), s(s(s(0))))
mult12_in_gga(s(T234), s(s(s(0))), s(s(s(T237)))) → U12_gga(T234, T237, mult106_in_ga(T234, T237))
mult106_in_ga(0, s(s(s(0)))) → mult106_out_ga(0, s(s(s(0))))
mult106_in_ga(s(T279), s(s(s(T281)))) → U4_ga(T279, T281, mult106_in_ga(T279, T281))
U4_ga(T279, T281, mult106_out_ga(T279, T281)) → mult106_out_ga(s(T279), s(s(s(T281))))
U12_gga(T234, T237, mult106_out_ga(T234, T237)) → mult12_out_gga(s(T234), s(s(s(0))), s(s(s(T237))))
mult12_in_gga(0, s(s(s(s(0)))), s(s(s(s(0))))) → mult12_out_gga(0, s(s(s(s(0)))), s(s(s(s(0)))))
mult12_in_gga(s(T318), s(s(s(s(0)))), s(s(s(s(T321))))) → U13_gga(T318, T321, mult144_in_ga(T318, T321))
mult144_in_ga(0, s(s(s(s(0))))) → mult144_out_ga(0, s(s(s(s(0)))))
mult144_in_ga(s(T374), s(s(s(s(T376))))) → U5_ga(T374, T376, mult144_in_ga(T374, T376))
U5_ga(T374, T376, mult144_out_ga(T374, T376)) → mult144_out_ga(s(T374), s(s(s(s(T376)))))
U13_gga(T318, T321, mult144_out_ga(T318, T321)) → mult12_out_gga(s(T318), s(s(s(s(0)))), s(s(s(s(T321)))))
mult12_in_gga(0, s(s(s(s(s(0))))), s(s(s(s(s(0)))))) → mult12_out_gga(0, s(s(s(s(s(0))))), s(s(s(s(s(0))))))
mult12_in_gga(s(T413), s(s(s(s(s(0))))), s(s(s(s(s(T416)))))) → U14_gga(T413, T416, mult187_in_ga(T413, T416))
mult187_in_ga(0, s(s(s(s(s(0)))))) → mult187_out_ga(0, s(s(s(s(s(0))))))
mult187_in_ga(s(T480), s(s(s(s(s(T482)))))) → U6_ga(T480, T482, mult187_in_ga(T480, T482))
U6_ga(T480, T482, mult187_out_ga(T480, T482)) → mult187_out_ga(s(T480), s(s(s(s(s(T482))))))
U14_gga(T413, T416, mult187_out_ga(T413, T416)) → mult12_out_gga(s(T413), s(s(s(s(s(0))))), s(s(s(s(s(T416))))))
mult12_in_gga(0, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(0))))))) → mult12_out_gga(0, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(0)))))))
mult12_in_gga(s(T519), s(s(s(s(s(s(0)))))), s(s(s(s(s(s(T522))))))) → U15_gga(T519, T522, mult235_in_ga(T519, T522))
mult235_in_ga(0, s(s(s(s(s(s(0))))))) → mult235_out_ga(0, s(s(s(s(s(s(0)))))))
mult235_in_ga(s(T597), s(s(s(s(s(s(T599))))))) → U7_ga(T597, T599, mult235_in_ga(T597, T599))
U7_ga(T597, T599, mult235_out_ga(T597, T599)) → mult235_out_ga(s(T597), s(s(s(s(s(s(T599)))))))
U15_gga(T519, T522, mult235_out_ga(T519, T522)) → mult12_out_gga(s(T519), s(s(s(s(s(s(0)))))), s(s(s(s(s(s(T522)))))))
mult12_in_gga(0, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(0)))))))) → mult12_out_gga(0, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(0))))))))
mult12_in_gga(s(T636), s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(T639)))))))) → U16_gga(T636, T639, mult288_in_ga(T636, T639))
mult288_in_ga(0, s(s(s(s(s(s(s(0)))))))) → mult288_out_ga(0, s(s(s(s(s(s(s(0))))))))
mult288_in_ga(s(T725), s(s(s(s(s(s(s(T727)))))))) → U8_ga(T725, T727, mult288_in_ga(T725, T727))
U8_ga(T725, T727, mult288_out_ga(T725, T727)) → mult288_out_ga(s(T725), s(s(s(s(s(s(s(T727))))))))
U16_gga(T636, T639, mult288_out_ga(T636, T639)) → mult12_out_gga(s(T636), s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(T639))))))))
mult12_in_gga(T740, s(s(s(s(s(s(s(s(T742)))))))), s(s(s(s(s(s(s(s(T744))))))))) → U17_gga(T740, T742, T744, mult338_in_ggga(T740, s(s(s(s(s(s(s(T742))))))), T742, T744))
mult338_in_ggga(0, T754, 0, 0) → mult338_out_ggga(0, T754, 0, 0)
mult338_in_ggga(s(T767), T768, 0, T770) → U18_ggga(T767, T768, T770, mult12_in_gga(T767, s(T768), T770))
U18_ggga(T767, T768, T770, mult12_out_gga(T767, s(T768), T770)) → mult338_out_ggga(s(T767), T768, 0, T770)
mult338_in_ggga(T786, T787, s(T788), s(T790)) → U19_ggga(T786, T787, T788, T790, mult338_in_ggga(T786, T787, T788, T790))
U19_ggga(T786, T787, T788, T790, mult338_out_ggga(T786, T787, T788, T790)) → mult338_out_ggga(T786, T787, s(T788), s(T790))
U17_gga(T740, T742, T744, mult338_out_ggga(T740, s(s(s(s(s(s(s(T742))))))), T742, T744)) → mult12_out_gga(T740, s(s(s(s(s(s(s(s(T742)))))))), s(s(s(s(s(s(s(s(T744)))))))))
U20_gga(T28, T29, T31, mult12_out_gga(T28, T29, T31)) → times1_out_gga(s(T28), T29, T31)

The argument filtering Pi contains the following mapping:
times1_in_gga(x1, x2, x3)  =  times1_in_gga(x1, x2)
0  =  0
times1_out_gga(x1, x2, x3)  =  times1_out_gga(x3)
s(x1)  =  s(x1)
U20_gga(x1, x2, x3, x4)  =  U20_gga(x4)
mult12_in_gga(x1, x2, x3)  =  mult12_in_gga(x1, x2)
mult12_out_gga(x1, x2, x3)  =  mult12_out_gga(x3)
U9_gga(x1, x2, x3)  =  U9_gga(x3)
mult22_in_ga(x1, x2)  =  mult22_in_ga(x1)
mult22_out_ga(x1, x2)  =  mult22_out_ga(x2)
U1_ga(x1, x2, x3)  =  U1_ga(x3)
U10_gga(x1, x2, x3)  =  U10_gga(x3)
mult45_in_ga(x1, x2)  =  mult45_in_ga(x1)
mult45_out_ga(x1, x2)  =  mult45_out_ga(x2)
U2_ga(x1, x2, x3)  =  U2_ga(x3)
U11_gga(x1, x2, x3)  =  U11_gga(x3)
mult73_in_ga(x1, x2)  =  mult73_in_ga(x1)
mult73_out_ga(x1, x2)  =  mult73_out_ga(x2)
U3_ga(x1, x2, x3)  =  U3_ga(x3)
U12_gga(x1, x2, x3)  =  U12_gga(x3)
mult106_in_ga(x1, x2)  =  mult106_in_ga(x1)
mult106_out_ga(x1, x2)  =  mult106_out_ga(x2)
U4_ga(x1, x2, x3)  =  U4_ga(x3)
U13_gga(x1, x2, x3)  =  U13_gga(x3)
mult144_in_ga(x1, x2)  =  mult144_in_ga(x1)
mult144_out_ga(x1, x2)  =  mult144_out_ga(x2)
U5_ga(x1, x2, x3)  =  U5_ga(x3)
U14_gga(x1, x2, x3)  =  U14_gga(x3)
mult187_in_ga(x1, x2)  =  mult187_in_ga(x1)
mult187_out_ga(x1, x2)  =  mult187_out_ga(x2)
U6_ga(x1, x2, x3)  =  U6_ga(x3)
U15_gga(x1, x2, x3)  =  U15_gga(x3)
mult235_in_ga(x1, x2)  =  mult235_in_ga(x1)
mult235_out_ga(x1, x2)  =  mult235_out_ga(x2)
U7_ga(x1, x2, x3)  =  U7_ga(x3)
U16_gga(x1, x2, x3)  =  U16_gga(x3)
mult288_in_ga(x1, x2)  =  mult288_in_ga(x1)
mult288_out_ga(x1, x2)  =  mult288_out_ga(x2)
U8_ga(x1, x2, x3)  =  U8_ga(x3)
U17_gga(x1, x2, x3, x4)  =  U17_gga(x4)
mult338_in_ggga(x1, x2, x3, x4)  =  mult338_in_ggga(x1, x2, x3)
mult338_out_ggga(x1, x2, x3, x4)  =  mult338_out_ggga(x4)
U18_ggga(x1, x2, x3, x4)  =  U18_ggga(x4)
U19_ggga(x1, x2, x3, x4, x5)  =  U19_ggga(x5)
MULT12_IN_GGA(x1, x2, x3)  =  MULT12_IN_GGA(x1, x2)
MULT338_IN_GGGA(x1, x2, x3, x4)  =  MULT338_IN_GGGA(x1, x2, x3)

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

(59) UsableRulesProof (EQUIVALENT transformation)

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

(60) Obligation:

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

MULT12_IN_GGA(T740, s(s(s(s(s(s(s(s(T742)))))))), s(s(s(s(s(s(s(s(T744))))))))) → MULT338_IN_GGGA(T740, s(s(s(s(s(s(s(T742))))))), T742, T744)
MULT338_IN_GGGA(s(T767), T768, 0, T770) → MULT12_IN_GGA(T767, s(T768), T770)
MULT338_IN_GGGA(T786, T787, s(T788), s(T790)) → MULT338_IN_GGGA(T786, T787, T788, T790)

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

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

(61) PiDPToQDPProof (SOUND transformation)

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

(62) Obligation:

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

MULT12_IN_GGA(T740, s(s(s(s(s(s(s(s(T742))))))))) → MULT338_IN_GGGA(T740, s(s(s(s(s(s(s(T742))))))), T742)
MULT338_IN_GGGA(s(T767), T768, 0) → MULT12_IN_GGA(T767, s(T768))
MULT338_IN_GGGA(T786, T787, s(T788)) → MULT338_IN_GGGA(T786, T787, T788)

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

(63) 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:

  • MULT338_IN_GGGA(s(T767), T768, 0) → MULT12_IN_GGA(T767, s(T768))
    The graph contains the following edges 1 > 1

  • MULT338_IN_GGGA(T786, T787, s(T788)) → MULT338_IN_GGGA(T786, T787, T788)
    The graph contains the following edges 1 >= 1, 2 >= 2, 3 > 3

  • MULT12_IN_GGA(T740, s(s(s(s(s(s(s(s(T742))))))))) → MULT338_IN_GGGA(T740, s(s(s(s(s(s(s(T742))))))), T742)
    The graph contains the following edges 1 >= 1, 2 > 2, 2 > 3

(64) YES

(65) Obligation:

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

MULT22_IN_GA(s(T63), T65) → MULT22_IN_GA(T63, T65)

The TRS R consists of the following rules:

times1_in_gga(0, T15, 0) → times1_out_gga(0, T15, 0)
times1_in_gga(s(T28), T29, T31) → U20_gga(T28, T29, T31, mult12_in_gga(T28, T29, T31))
mult12_in_gga(0, 0, 0) → mult12_out_gga(0, 0, 0)
mult12_in_gga(s(T51), 0, T54) → U9_gga(T51, T54, mult22_in_ga(T51, T54))
mult22_in_ga(0, 0) → mult22_out_ga(0, 0)
mult22_in_ga(s(T63), T65) → U1_ga(T63, T65, mult22_in_ga(T63, T65))
U1_ga(T63, T65, mult22_out_ga(T63, T65)) → mult22_out_ga(s(T63), T65)
U9_gga(T51, T54, mult22_out_ga(T51, T54)) → mult12_out_gga(s(T51), 0, T54)
mult12_in_gga(0, s(0), s(0)) → mult12_out_gga(0, s(0), s(0))
mult12_in_gga(s(T99), s(0), s(T102)) → U10_gga(T99, T102, mult45_in_ga(T99, T102))
mult45_in_ga(0, s(0)) → mult45_out_ga(0, s(0))
mult45_in_ga(s(T122), s(T124)) → U2_ga(T122, T124, mult45_in_ga(T122, T124))
U2_ga(T122, T124, mult45_out_ga(T122, T124)) → mult45_out_ga(s(T122), s(T124))
U10_gga(T99, T102, mult45_out_ga(T99, T102)) → mult12_out_gga(s(T99), s(0), s(T102))
mult12_in_gga(0, s(s(0)), s(s(0))) → mult12_out_gga(0, s(s(0)), s(s(0)))
mult12_in_gga(s(T161), s(s(0)), s(s(T164))) → U11_gga(T161, T164, mult73_in_ga(T161, T164))
mult73_in_ga(0, s(s(0))) → mult73_out_ga(0, s(s(0)))
mult73_in_ga(s(T195), s(s(T197))) → U3_ga(T195, T197, mult73_in_ga(T195, T197))
U3_ga(T195, T197, mult73_out_ga(T195, T197)) → mult73_out_ga(s(T195), s(s(T197)))
U11_gga(T161, T164, mult73_out_ga(T161, T164)) → mult12_out_gga(s(T161), s(s(0)), s(s(T164)))
mult12_in_gga(0, s(s(s(0))), s(s(s(0)))) → mult12_out_gga(0, s(s(s(0))), s(s(s(0))))
mult12_in_gga(s(T234), s(s(s(0))), s(s(s(T237)))) → U12_gga(T234, T237, mult106_in_ga(T234, T237))
mult106_in_ga(0, s(s(s(0)))) → mult106_out_ga(0, s(s(s(0))))
mult106_in_ga(s(T279), s(s(s(T281)))) → U4_ga(T279, T281, mult106_in_ga(T279, T281))
U4_ga(T279, T281, mult106_out_ga(T279, T281)) → mult106_out_ga(s(T279), s(s(s(T281))))
U12_gga(T234, T237, mult106_out_ga(T234, T237)) → mult12_out_gga(s(T234), s(s(s(0))), s(s(s(T237))))
mult12_in_gga(0, s(s(s(s(0)))), s(s(s(s(0))))) → mult12_out_gga(0, s(s(s(s(0)))), s(s(s(s(0)))))
mult12_in_gga(s(T318), s(s(s(s(0)))), s(s(s(s(T321))))) → U13_gga(T318, T321, mult144_in_ga(T318, T321))
mult144_in_ga(0, s(s(s(s(0))))) → mult144_out_ga(0, s(s(s(s(0)))))
mult144_in_ga(s(T374), s(s(s(s(T376))))) → U5_ga(T374, T376, mult144_in_ga(T374, T376))
U5_ga(T374, T376, mult144_out_ga(T374, T376)) → mult144_out_ga(s(T374), s(s(s(s(T376)))))
U13_gga(T318, T321, mult144_out_ga(T318, T321)) → mult12_out_gga(s(T318), s(s(s(s(0)))), s(s(s(s(T321)))))
mult12_in_gga(0, s(s(s(s(s(0))))), s(s(s(s(s(0)))))) → mult12_out_gga(0, s(s(s(s(s(0))))), s(s(s(s(s(0))))))
mult12_in_gga(s(T413), s(s(s(s(s(0))))), s(s(s(s(s(T416)))))) → U14_gga(T413, T416, mult187_in_ga(T413, T416))
mult187_in_ga(0, s(s(s(s(s(0)))))) → mult187_out_ga(0, s(s(s(s(s(0))))))
mult187_in_ga(s(T480), s(s(s(s(s(T482)))))) → U6_ga(T480, T482, mult187_in_ga(T480, T482))
U6_ga(T480, T482, mult187_out_ga(T480, T482)) → mult187_out_ga(s(T480), s(s(s(s(s(T482))))))
U14_gga(T413, T416, mult187_out_ga(T413, T416)) → mult12_out_gga(s(T413), s(s(s(s(s(0))))), s(s(s(s(s(T416))))))
mult12_in_gga(0, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(0))))))) → mult12_out_gga(0, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(0)))))))
mult12_in_gga(s(T519), s(s(s(s(s(s(0)))))), s(s(s(s(s(s(T522))))))) → U15_gga(T519, T522, mult235_in_ga(T519, T522))
mult235_in_ga(0, s(s(s(s(s(s(0))))))) → mult235_out_ga(0, s(s(s(s(s(s(0)))))))
mult235_in_ga(s(T597), s(s(s(s(s(s(T599))))))) → U7_ga(T597, T599, mult235_in_ga(T597, T599))
U7_ga(T597, T599, mult235_out_ga(T597, T599)) → mult235_out_ga(s(T597), s(s(s(s(s(s(T599)))))))
U15_gga(T519, T522, mult235_out_ga(T519, T522)) → mult12_out_gga(s(T519), s(s(s(s(s(s(0)))))), s(s(s(s(s(s(T522)))))))
mult12_in_gga(0, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(0)))))))) → mult12_out_gga(0, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(0))))))))
mult12_in_gga(s(T636), s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(T639)))))))) → U16_gga(T636, T639, mult288_in_ga(T636, T639))
mult288_in_ga(0, s(s(s(s(s(s(s(0)))))))) → mult288_out_ga(0, s(s(s(s(s(s(s(0))))))))
mult288_in_ga(s(T725), s(s(s(s(s(s(s(T727)))))))) → U8_ga(T725, T727, mult288_in_ga(T725, T727))
U8_ga(T725, T727, mult288_out_ga(T725, T727)) → mult288_out_ga(s(T725), s(s(s(s(s(s(s(T727))))))))
U16_gga(T636, T639, mult288_out_ga(T636, T639)) → mult12_out_gga(s(T636), s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(T639))))))))
mult12_in_gga(T740, s(s(s(s(s(s(s(s(T742)))))))), s(s(s(s(s(s(s(s(T744))))))))) → U17_gga(T740, T742, T744, mult338_in_ggga(T740, s(s(s(s(s(s(s(T742))))))), T742, T744))
mult338_in_ggga(0, T754, 0, 0) → mult338_out_ggga(0, T754, 0, 0)
mult338_in_ggga(s(T767), T768, 0, T770) → U18_ggga(T767, T768, T770, mult12_in_gga(T767, s(T768), T770))
U18_ggga(T767, T768, T770, mult12_out_gga(T767, s(T768), T770)) → mult338_out_ggga(s(T767), T768, 0, T770)
mult338_in_ggga(T786, T787, s(T788), s(T790)) → U19_ggga(T786, T787, T788, T790, mult338_in_ggga(T786, T787, T788, T790))
U19_ggga(T786, T787, T788, T790, mult338_out_ggga(T786, T787, T788, T790)) → mult338_out_ggga(T786, T787, s(T788), s(T790))
U17_gga(T740, T742, T744, mult338_out_ggga(T740, s(s(s(s(s(s(s(T742))))))), T742, T744)) → mult12_out_gga(T740, s(s(s(s(s(s(s(s(T742)))))))), s(s(s(s(s(s(s(s(T744)))))))))
U20_gga(T28, T29, T31, mult12_out_gga(T28, T29, T31)) → times1_out_gga(s(T28), T29, T31)

The argument filtering Pi contains the following mapping:
times1_in_gga(x1, x2, x3)  =  times1_in_gga(x1, x2)
0  =  0
times1_out_gga(x1, x2, x3)  =  times1_out_gga(x3)
s(x1)  =  s(x1)
U20_gga(x1, x2, x3, x4)  =  U20_gga(x4)
mult12_in_gga(x1, x2, x3)  =  mult12_in_gga(x1, x2)
mult12_out_gga(x1, x2, x3)  =  mult12_out_gga(x3)
U9_gga(x1, x2, x3)  =  U9_gga(x3)
mult22_in_ga(x1, x2)  =  mult22_in_ga(x1)
mult22_out_ga(x1, x2)  =  mult22_out_ga(x2)
U1_ga(x1, x2, x3)  =  U1_ga(x3)
U10_gga(x1, x2, x3)  =  U10_gga(x3)
mult45_in_ga(x1, x2)  =  mult45_in_ga(x1)
mult45_out_ga(x1, x2)  =  mult45_out_ga(x2)
U2_ga(x1, x2, x3)  =  U2_ga(x3)
U11_gga(x1, x2, x3)  =  U11_gga(x3)
mult73_in_ga(x1, x2)  =  mult73_in_ga(x1)
mult73_out_ga(x1, x2)  =  mult73_out_ga(x2)
U3_ga(x1, x2, x3)  =  U3_ga(x3)
U12_gga(x1, x2, x3)  =  U12_gga(x3)
mult106_in_ga(x1, x2)  =  mult106_in_ga(x1)
mult106_out_ga(x1, x2)  =  mult106_out_ga(x2)
U4_ga(x1, x2, x3)  =  U4_ga(x3)
U13_gga(x1, x2, x3)  =  U13_gga(x3)
mult144_in_ga(x1, x2)  =  mult144_in_ga(x1)
mult144_out_ga(x1, x2)  =  mult144_out_ga(x2)
U5_ga(x1, x2, x3)  =  U5_ga(x3)
U14_gga(x1, x2, x3)  =  U14_gga(x3)
mult187_in_ga(x1, x2)  =  mult187_in_ga(x1)
mult187_out_ga(x1, x2)  =  mult187_out_ga(x2)
U6_ga(x1, x2, x3)  =  U6_ga(x3)
U15_gga(x1, x2, x3)  =  U15_gga(x3)
mult235_in_ga(x1, x2)  =  mult235_in_ga(x1)
mult235_out_ga(x1, x2)  =  mult235_out_ga(x2)
U7_ga(x1, x2, x3)  =  U7_ga(x3)
U16_gga(x1, x2, x3)  =  U16_gga(x3)
mult288_in_ga(x1, x2)  =  mult288_in_ga(x1)
mult288_out_ga(x1, x2)  =  mult288_out_ga(x2)
U8_ga(x1, x2, x3)  =  U8_ga(x3)
U17_gga(x1, x2, x3, x4)  =  U17_gga(x4)
mult338_in_ggga(x1, x2, x3, x4)  =  mult338_in_ggga(x1, x2, x3)
mult338_out_ggga(x1, x2, x3, x4)  =  mult338_out_ggga(x4)
U18_ggga(x1, x2, x3, x4)  =  U18_ggga(x4)
U19_ggga(x1, x2, x3, x4, x5)  =  U19_ggga(x5)
MULT22_IN_GA(x1, x2)  =  MULT22_IN_GA(x1)

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

(66) UsableRulesProof (EQUIVALENT transformation)

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

(67) Obligation:

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

MULT22_IN_GA(s(T63), T65) → MULT22_IN_GA(T63, T65)

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

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

(68) PiDPToQDPProof (SOUND transformation)

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

(69) Obligation:

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

MULT22_IN_GA(s(T63)) → MULT22_IN_GA(T63)

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

(70) 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:

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

(71) YES