(0) Obligation:

Clauses:

div(X, Y, Z) :- quot(X, Y, Y, Z).
quot(0, s(Y), s(Z), 0).
quot(s(X), s(Y), Z, U) :- quot(X, Y, Z, U).
quot(X, 0, s(Z), s(U)) :- quot(X, s(Z), s(Z), U).

Queries:

div(g,g,a).

(1) PrologToPrologProblemTransformerProof (SOUND transformation)

Built Prolog problem from termination graph.

(2) Obligation:

Clauses:

quot84(0, s(T208), T209, 0).
quot84(s(T226), s(T227), T228, T230) :- quot84(T226, T227, T228, T230).
quot84(T241, 0, T242, s(T244)) :- quot3(T241, s(T242), T244).
quot3(0, s(T15), 0).
quot3(s(0), s(s(T38)), 0).
quot3(s(s(0)), s(s(s(T61))), 0).
quot3(s(s(s(0))), s(s(s(s(T84)))), 0).
quot3(s(s(s(s(0)))), s(s(s(s(s(T107))))), 0).
quot3(s(s(s(s(s(0))))), s(s(s(s(s(s(T130)))))), 0).
quot3(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T153))))))), 0).
quot3(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(T176)))))))), 0).
quot3(s(s(s(s(s(s(s(s(T189)))))))), s(s(s(s(s(s(s(s(T190)))))))), T192) :- quot84(T189, T190, s(s(s(s(s(s(s(T190))))))), T192).
quot3(s(s(s(s(s(s(s(T251))))))), s(s(s(s(s(s(s(0))))))), s(T253)) :- quot97(T251, T253).
quot3(s(s(s(s(s(s(T353)))))), s(s(s(s(s(s(0)))))), s(T355)) :- quot181(T353, T355).
quot3(s(s(s(s(s(T443))))), s(s(s(s(s(0))))), s(T445)) :- quot254(T443, T445).
quot3(s(s(s(s(T521)))), s(s(s(s(0)))), s(T523)) :- quot316(T521, T523).
quot3(s(s(s(T587))), s(s(s(0))), s(T589)) :- quot367(T587, T589).
quot3(s(s(T641)), s(s(0)), s(T643)) :- quot407(T641, T643).
quot3(s(T683), s(0), s(T685)) :- quot436(T683, T685).
quot97(0, 0).
quot97(s(0), 0).
quot97(s(s(0)), 0).
quot97(s(s(s(0))), 0).
quot97(s(s(s(s(0)))), 0).
quot97(s(s(s(s(s(0))))), 0).
quot97(s(s(s(s(s(s(0)))))), 0).
quot97(s(s(s(s(s(s(s(T339))))))), s(T341)) :- quot97(T339, T341).
quot181(0, 0).
quot181(s(0), 0).
quot181(s(s(0)), 0).
quot181(s(s(s(0))), 0).
quot181(s(s(s(s(0)))), 0).
quot181(s(s(s(s(s(0))))), 0).
quot181(s(s(s(s(s(s(T430)))))), s(T432)) :- quot181(T430, T432).
quot254(0, 0).
quot254(s(0), 0).
quot254(s(s(0)), 0).
quot254(s(s(s(0))), 0).
quot254(s(s(s(s(0)))), 0).
quot254(s(s(s(s(s(T509))))), s(T511)) :- quot254(T509, T511).
quot316(0, 0).
quot316(s(0), 0).
quot316(s(s(0)), 0).
quot316(s(s(s(0))), 0).
quot316(s(s(s(s(T576)))), s(T578)) :- quot316(T576, T578).
quot367(0, 0).
quot367(s(0), 0).
quot367(s(s(0)), 0).
quot367(s(s(s(T631))), s(T633)) :- quot367(T631, T633).
quot407(0, 0).
quot407(s(0), 0).
quot407(s(s(T674)), s(T676)) :- quot407(T674, T676).
quot436(0, 0).
quot436(s(T705), s(T707)) :- quot436(T705, T707).
div1(T7, T8, T10) :- quot3(T7, T8, T10).

Queries:

div1(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:
div1_in: (b,b,f)
quot3_in: (b,b,f)
quot84_in: (b,b,b,f)
quot97_in: (b,f)
quot181_in: (b,f)
quot254_in: (b,f)
quot316_in: (b,f)
quot367_in: (b,f)
quot407_in: (b,f)
quot436_in: (b,f)
Transforming Prolog into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:

div1_in_gga(T7, T8, T10) → U18_gga(T7, T8, T10, quot3_in_gga(T7, T8, T10))
quot3_in_gga(0, s(T15), 0) → quot3_out_gga(0, s(T15), 0)
quot3_in_gga(s(0), s(s(T38)), 0) → quot3_out_gga(s(0), s(s(T38)), 0)
quot3_in_gga(s(s(0)), s(s(s(T61))), 0) → quot3_out_gga(s(s(0)), s(s(s(T61))), 0)
quot3_in_gga(s(s(s(0))), s(s(s(s(T84)))), 0) → quot3_out_gga(s(s(s(0))), s(s(s(s(T84)))), 0)
quot3_in_gga(s(s(s(s(0)))), s(s(s(s(s(T107))))), 0) → quot3_out_gga(s(s(s(s(0)))), s(s(s(s(s(T107))))), 0)
quot3_in_gga(s(s(s(s(s(0))))), s(s(s(s(s(s(T130)))))), 0) → quot3_out_gga(s(s(s(s(s(0))))), s(s(s(s(s(s(T130)))))), 0)
quot3_in_gga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T153))))))), 0) → quot3_out_gga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T153))))))), 0)
quot3_in_gga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(T176)))))))), 0) → quot3_out_gga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(T176)))))))), 0)
quot3_in_gga(s(s(s(s(s(s(s(s(T189)))))))), s(s(s(s(s(s(s(s(T190)))))))), T192) → U3_gga(T189, T190, T192, quot84_in_ggga(T189, T190, s(s(s(s(s(s(s(T190))))))), T192))
quot84_in_ggga(0, s(T208), T209, 0) → quot84_out_ggga(0, s(T208), T209, 0)
quot84_in_ggga(s(T226), s(T227), T228, T230) → U1_ggga(T226, T227, T228, T230, quot84_in_ggga(T226, T227, T228, T230))
quot84_in_ggga(T241, 0, T242, s(T244)) → U2_ggga(T241, T242, T244, quot3_in_gga(T241, s(T242), T244))
quot3_in_gga(s(s(s(s(s(s(s(T251))))))), s(s(s(s(s(s(s(0))))))), s(T253)) → U4_gga(T251, T253, quot97_in_ga(T251, T253))
quot97_in_ga(0, 0) → quot97_out_ga(0, 0)
quot97_in_ga(s(0), 0) → quot97_out_ga(s(0), 0)
quot97_in_ga(s(s(0)), 0) → quot97_out_ga(s(s(0)), 0)
quot97_in_ga(s(s(s(0))), 0) → quot97_out_ga(s(s(s(0))), 0)
quot97_in_ga(s(s(s(s(0)))), 0) → quot97_out_ga(s(s(s(s(0)))), 0)
quot97_in_ga(s(s(s(s(s(0))))), 0) → quot97_out_ga(s(s(s(s(s(0))))), 0)
quot97_in_ga(s(s(s(s(s(s(0)))))), 0) → quot97_out_ga(s(s(s(s(s(s(0)))))), 0)
quot97_in_ga(s(s(s(s(s(s(s(T339))))))), s(T341)) → U11_ga(T339, T341, quot97_in_ga(T339, T341))
U11_ga(T339, T341, quot97_out_ga(T339, T341)) → quot97_out_ga(s(s(s(s(s(s(s(T339))))))), s(T341))
U4_gga(T251, T253, quot97_out_ga(T251, T253)) → quot3_out_gga(s(s(s(s(s(s(s(T251))))))), s(s(s(s(s(s(s(0))))))), s(T253))
quot3_in_gga(s(s(s(s(s(s(T353)))))), s(s(s(s(s(s(0)))))), s(T355)) → U5_gga(T353, T355, quot181_in_ga(T353, T355))
quot181_in_ga(0, 0) → quot181_out_ga(0, 0)
quot181_in_ga(s(0), 0) → quot181_out_ga(s(0), 0)
quot181_in_ga(s(s(0)), 0) → quot181_out_ga(s(s(0)), 0)
quot181_in_ga(s(s(s(0))), 0) → quot181_out_ga(s(s(s(0))), 0)
quot181_in_ga(s(s(s(s(0)))), 0) → quot181_out_ga(s(s(s(s(0)))), 0)
quot181_in_ga(s(s(s(s(s(0))))), 0) → quot181_out_ga(s(s(s(s(s(0))))), 0)
quot181_in_ga(s(s(s(s(s(s(T430)))))), s(T432)) → U12_ga(T430, T432, quot181_in_ga(T430, T432))
U12_ga(T430, T432, quot181_out_ga(T430, T432)) → quot181_out_ga(s(s(s(s(s(s(T430)))))), s(T432))
U5_gga(T353, T355, quot181_out_ga(T353, T355)) → quot3_out_gga(s(s(s(s(s(s(T353)))))), s(s(s(s(s(s(0)))))), s(T355))
quot3_in_gga(s(s(s(s(s(T443))))), s(s(s(s(s(0))))), s(T445)) → U6_gga(T443, T445, quot254_in_ga(T443, T445))
quot254_in_ga(0, 0) → quot254_out_ga(0, 0)
quot254_in_ga(s(0), 0) → quot254_out_ga(s(0), 0)
quot254_in_ga(s(s(0)), 0) → quot254_out_ga(s(s(0)), 0)
quot254_in_ga(s(s(s(0))), 0) → quot254_out_ga(s(s(s(0))), 0)
quot254_in_ga(s(s(s(s(0)))), 0) → quot254_out_ga(s(s(s(s(0)))), 0)
quot254_in_ga(s(s(s(s(s(T509))))), s(T511)) → U13_ga(T509, T511, quot254_in_ga(T509, T511))
U13_ga(T509, T511, quot254_out_ga(T509, T511)) → quot254_out_ga(s(s(s(s(s(T509))))), s(T511))
U6_gga(T443, T445, quot254_out_ga(T443, T445)) → quot3_out_gga(s(s(s(s(s(T443))))), s(s(s(s(s(0))))), s(T445))
quot3_in_gga(s(s(s(s(T521)))), s(s(s(s(0)))), s(T523)) → U7_gga(T521, T523, quot316_in_ga(T521, T523))
quot316_in_ga(0, 0) → quot316_out_ga(0, 0)
quot316_in_ga(s(0), 0) → quot316_out_ga(s(0), 0)
quot316_in_ga(s(s(0)), 0) → quot316_out_ga(s(s(0)), 0)
quot316_in_ga(s(s(s(0))), 0) → quot316_out_ga(s(s(s(0))), 0)
quot316_in_ga(s(s(s(s(T576)))), s(T578)) → U14_ga(T576, T578, quot316_in_ga(T576, T578))
U14_ga(T576, T578, quot316_out_ga(T576, T578)) → quot316_out_ga(s(s(s(s(T576)))), s(T578))
U7_gga(T521, T523, quot316_out_ga(T521, T523)) → quot3_out_gga(s(s(s(s(T521)))), s(s(s(s(0)))), s(T523))
quot3_in_gga(s(s(s(T587))), s(s(s(0))), s(T589)) → U8_gga(T587, T589, quot367_in_ga(T587, T589))
quot367_in_ga(0, 0) → quot367_out_ga(0, 0)
quot367_in_ga(s(0), 0) → quot367_out_ga(s(0), 0)
quot367_in_ga(s(s(0)), 0) → quot367_out_ga(s(s(0)), 0)
quot367_in_ga(s(s(s(T631))), s(T633)) → U15_ga(T631, T633, quot367_in_ga(T631, T633))
U15_ga(T631, T633, quot367_out_ga(T631, T633)) → quot367_out_ga(s(s(s(T631))), s(T633))
U8_gga(T587, T589, quot367_out_ga(T587, T589)) → quot3_out_gga(s(s(s(T587))), s(s(s(0))), s(T589))
quot3_in_gga(s(s(T641)), s(s(0)), s(T643)) → U9_gga(T641, T643, quot407_in_ga(T641, T643))
quot407_in_ga(0, 0) → quot407_out_ga(0, 0)
quot407_in_ga(s(0), 0) → quot407_out_ga(s(0), 0)
quot407_in_ga(s(s(T674)), s(T676)) → U16_ga(T674, T676, quot407_in_ga(T674, T676))
U16_ga(T674, T676, quot407_out_ga(T674, T676)) → quot407_out_ga(s(s(T674)), s(T676))
U9_gga(T641, T643, quot407_out_ga(T641, T643)) → quot3_out_gga(s(s(T641)), s(s(0)), s(T643))
quot3_in_gga(s(T683), s(0), s(T685)) → U10_gga(T683, T685, quot436_in_ga(T683, T685))
quot436_in_ga(0, 0) → quot436_out_ga(0, 0)
quot436_in_ga(s(T705), s(T707)) → U17_ga(T705, T707, quot436_in_ga(T705, T707))
U17_ga(T705, T707, quot436_out_ga(T705, T707)) → quot436_out_ga(s(T705), s(T707))
U10_gga(T683, T685, quot436_out_ga(T683, T685)) → quot3_out_gga(s(T683), s(0), s(T685))
U2_ggga(T241, T242, T244, quot3_out_gga(T241, s(T242), T244)) → quot84_out_ggga(T241, 0, T242, s(T244))
U1_ggga(T226, T227, T228, T230, quot84_out_ggga(T226, T227, T228, T230)) → quot84_out_ggga(s(T226), s(T227), T228, T230)
U3_gga(T189, T190, T192, quot84_out_ggga(T189, T190, s(s(s(s(s(s(s(T190))))))), T192)) → quot3_out_gga(s(s(s(s(s(s(s(s(T189)))))))), s(s(s(s(s(s(s(s(T190)))))))), T192)
U18_gga(T7, T8, T10, quot3_out_gga(T7, T8, T10)) → div1_out_gga(T7, T8, T10)

The argument filtering Pi contains the following mapping:
div1_in_gga(x1, x2, x3)  =  div1_in_gga(x1, x2)
U18_gga(x1, x2, x3, x4)  =  U18_gga(x4)
quot3_in_gga(x1, x2, x3)  =  quot3_in_gga(x1, x2)
0  =  0
s(x1)  =  s(x1)
quot3_out_gga(x1, x2, x3)  =  quot3_out_gga(x3)
U3_gga(x1, x2, x3, x4)  =  U3_gga(x4)
quot84_in_ggga(x1, x2, x3, x4)  =  quot84_in_ggga(x1, x2, x3)
quot84_out_ggga(x1, x2, x3, x4)  =  quot84_out_ggga(x4)
U1_ggga(x1, x2, x3, x4, x5)  =  U1_ggga(x5)
U2_ggga(x1, x2, x3, x4)  =  U2_ggga(x4)
U4_gga(x1, x2, x3)  =  U4_gga(x3)
quot97_in_ga(x1, x2)  =  quot97_in_ga(x1)
quot97_out_ga(x1, x2)  =  quot97_out_ga(x2)
U11_ga(x1, x2, x3)  =  U11_ga(x3)
U5_gga(x1, x2, x3)  =  U5_gga(x3)
quot181_in_ga(x1, x2)  =  quot181_in_ga(x1)
quot181_out_ga(x1, x2)  =  quot181_out_ga(x2)
U12_ga(x1, x2, x3)  =  U12_ga(x3)
U6_gga(x1, x2, x3)  =  U6_gga(x3)
quot254_in_ga(x1, x2)  =  quot254_in_ga(x1)
quot254_out_ga(x1, x2)  =  quot254_out_ga(x2)
U13_ga(x1, x2, x3)  =  U13_ga(x3)
U7_gga(x1, x2, x3)  =  U7_gga(x3)
quot316_in_ga(x1, x2)  =  quot316_in_ga(x1)
quot316_out_ga(x1, x2)  =  quot316_out_ga(x2)
U14_ga(x1, x2, x3)  =  U14_ga(x3)
U8_gga(x1, x2, x3)  =  U8_gga(x3)
quot367_in_ga(x1, x2)  =  quot367_in_ga(x1)
quot367_out_ga(x1, x2)  =  quot367_out_ga(x2)
U15_ga(x1, x2, x3)  =  U15_ga(x3)
U9_gga(x1, x2, x3)  =  U9_gga(x3)
quot407_in_ga(x1, x2)  =  quot407_in_ga(x1)
quot407_out_ga(x1, x2)  =  quot407_out_ga(x2)
U16_ga(x1, x2, x3)  =  U16_ga(x3)
U10_gga(x1, x2, x3)  =  U10_gga(x3)
quot436_in_ga(x1, x2)  =  quot436_in_ga(x1)
quot436_out_ga(x1, x2)  =  quot436_out_ga(x2)
U17_ga(x1, x2, x3)  =  U17_ga(x3)
div1_out_gga(x1, x2, x3)  =  div1_out_gga(x3)

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog

(4) Obligation:

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

div1_in_gga(T7, T8, T10) → U18_gga(T7, T8, T10, quot3_in_gga(T7, T8, T10))
quot3_in_gga(0, s(T15), 0) → quot3_out_gga(0, s(T15), 0)
quot3_in_gga(s(0), s(s(T38)), 0) → quot3_out_gga(s(0), s(s(T38)), 0)
quot3_in_gga(s(s(0)), s(s(s(T61))), 0) → quot3_out_gga(s(s(0)), s(s(s(T61))), 0)
quot3_in_gga(s(s(s(0))), s(s(s(s(T84)))), 0) → quot3_out_gga(s(s(s(0))), s(s(s(s(T84)))), 0)
quot3_in_gga(s(s(s(s(0)))), s(s(s(s(s(T107))))), 0) → quot3_out_gga(s(s(s(s(0)))), s(s(s(s(s(T107))))), 0)
quot3_in_gga(s(s(s(s(s(0))))), s(s(s(s(s(s(T130)))))), 0) → quot3_out_gga(s(s(s(s(s(0))))), s(s(s(s(s(s(T130)))))), 0)
quot3_in_gga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T153))))))), 0) → quot3_out_gga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T153))))))), 0)
quot3_in_gga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(T176)))))))), 0) → quot3_out_gga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(T176)))))))), 0)
quot3_in_gga(s(s(s(s(s(s(s(s(T189)))))))), s(s(s(s(s(s(s(s(T190)))))))), T192) → U3_gga(T189, T190, T192, quot84_in_ggga(T189, T190, s(s(s(s(s(s(s(T190))))))), T192))
quot84_in_ggga(0, s(T208), T209, 0) → quot84_out_ggga(0, s(T208), T209, 0)
quot84_in_ggga(s(T226), s(T227), T228, T230) → U1_ggga(T226, T227, T228, T230, quot84_in_ggga(T226, T227, T228, T230))
quot84_in_ggga(T241, 0, T242, s(T244)) → U2_ggga(T241, T242, T244, quot3_in_gga(T241, s(T242), T244))
quot3_in_gga(s(s(s(s(s(s(s(T251))))))), s(s(s(s(s(s(s(0))))))), s(T253)) → U4_gga(T251, T253, quot97_in_ga(T251, T253))
quot97_in_ga(0, 0) → quot97_out_ga(0, 0)
quot97_in_ga(s(0), 0) → quot97_out_ga(s(0), 0)
quot97_in_ga(s(s(0)), 0) → quot97_out_ga(s(s(0)), 0)
quot97_in_ga(s(s(s(0))), 0) → quot97_out_ga(s(s(s(0))), 0)
quot97_in_ga(s(s(s(s(0)))), 0) → quot97_out_ga(s(s(s(s(0)))), 0)
quot97_in_ga(s(s(s(s(s(0))))), 0) → quot97_out_ga(s(s(s(s(s(0))))), 0)
quot97_in_ga(s(s(s(s(s(s(0)))))), 0) → quot97_out_ga(s(s(s(s(s(s(0)))))), 0)
quot97_in_ga(s(s(s(s(s(s(s(T339))))))), s(T341)) → U11_ga(T339, T341, quot97_in_ga(T339, T341))
U11_ga(T339, T341, quot97_out_ga(T339, T341)) → quot97_out_ga(s(s(s(s(s(s(s(T339))))))), s(T341))
U4_gga(T251, T253, quot97_out_ga(T251, T253)) → quot3_out_gga(s(s(s(s(s(s(s(T251))))))), s(s(s(s(s(s(s(0))))))), s(T253))
quot3_in_gga(s(s(s(s(s(s(T353)))))), s(s(s(s(s(s(0)))))), s(T355)) → U5_gga(T353, T355, quot181_in_ga(T353, T355))
quot181_in_ga(0, 0) → quot181_out_ga(0, 0)
quot181_in_ga(s(0), 0) → quot181_out_ga(s(0), 0)
quot181_in_ga(s(s(0)), 0) → quot181_out_ga(s(s(0)), 0)
quot181_in_ga(s(s(s(0))), 0) → quot181_out_ga(s(s(s(0))), 0)
quot181_in_ga(s(s(s(s(0)))), 0) → quot181_out_ga(s(s(s(s(0)))), 0)
quot181_in_ga(s(s(s(s(s(0))))), 0) → quot181_out_ga(s(s(s(s(s(0))))), 0)
quot181_in_ga(s(s(s(s(s(s(T430)))))), s(T432)) → U12_ga(T430, T432, quot181_in_ga(T430, T432))
U12_ga(T430, T432, quot181_out_ga(T430, T432)) → quot181_out_ga(s(s(s(s(s(s(T430)))))), s(T432))
U5_gga(T353, T355, quot181_out_ga(T353, T355)) → quot3_out_gga(s(s(s(s(s(s(T353)))))), s(s(s(s(s(s(0)))))), s(T355))
quot3_in_gga(s(s(s(s(s(T443))))), s(s(s(s(s(0))))), s(T445)) → U6_gga(T443, T445, quot254_in_ga(T443, T445))
quot254_in_ga(0, 0) → quot254_out_ga(0, 0)
quot254_in_ga(s(0), 0) → quot254_out_ga(s(0), 0)
quot254_in_ga(s(s(0)), 0) → quot254_out_ga(s(s(0)), 0)
quot254_in_ga(s(s(s(0))), 0) → quot254_out_ga(s(s(s(0))), 0)
quot254_in_ga(s(s(s(s(0)))), 0) → quot254_out_ga(s(s(s(s(0)))), 0)
quot254_in_ga(s(s(s(s(s(T509))))), s(T511)) → U13_ga(T509, T511, quot254_in_ga(T509, T511))
U13_ga(T509, T511, quot254_out_ga(T509, T511)) → quot254_out_ga(s(s(s(s(s(T509))))), s(T511))
U6_gga(T443, T445, quot254_out_ga(T443, T445)) → quot3_out_gga(s(s(s(s(s(T443))))), s(s(s(s(s(0))))), s(T445))
quot3_in_gga(s(s(s(s(T521)))), s(s(s(s(0)))), s(T523)) → U7_gga(T521, T523, quot316_in_ga(T521, T523))
quot316_in_ga(0, 0) → quot316_out_ga(0, 0)
quot316_in_ga(s(0), 0) → quot316_out_ga(s(0), 0)
quot316_in_ga(s(s(0)), 0) → quot316_out_ga(s(s(0)), 0)
quot316_in_ga(s(s(s(0))), 0) → quot316_out_ga(s(s(s(0))), 0)
quot316_in_ga(s(s(s(s(T576)))), s(T578)) → U14_ga(T576, T578, quot316_in_ga(T576, T578))
U14_ga(T576, T578, quot316_out_ga(T576, T578)) → quot316_out_ga(s(s(s(s(T576)))), s(T578))
U7_gga(T521, T523, quot316_out_ga(T521, T523)) → quot3_out_gga(s(s(s(s(T521)))), s(s(s(s(0)))), s(T523))
quot3_in_gga(s(s(s(T587))), s(s(s(0))), s(T589)) → U8_gga(T587, T589, quot367_in_ga(T587, T589))
quot367_in_ga(0, 0) → quot367_out_ga(0, 0)
quot367_in_ga(s(0), 0) → quot367_out_ga(s(0), 0)
quot367_in_ga(s(s(0)), 0) → quot367_out_ga(s(s(0)), 0)
quot367_in_ga(s(s(s(T631))), s(T633)) → U15_ga(T631, T633, quot367_in_ga(T631, T633))
U15_ga(T631, T633, quot367_out_ga(T631, T633)) → quot367_out_ga(s(s(s(T631))), s(T633))
U8_gga(T587, T589, quot367_out_ga(T587, T589)) → quot3_out_gga(s(s(s(T587))), s(s(s(0))), s(T589))
quot3_in_gga(s(s(T641)), s(s(0)), s(T643)) → U9_gga(T641, T643, quot407_in_ga(T641, T643))
quot407_in_ga(0, 0) → quot407_out_ga(0, 0)
quot407_in_ga(s(0), 0) → quot407_out_ga(s(0), 0)
quot407_in_ga(s(s(T674)), s(T676)) → U16_ga(T674, T676, quot407_in_ga(T674, T676))
U16_ga(T674, T676, quot407_out_ga(T674, T676)) → quot407_out_ga(s(s(T674)), s(T676))
U9_gga(T641, T643, quot407_out_ga(T641, T643)) → quot3_out_gga(s(s(T641)), s(s(0)), s(T643))
quot3_in_gga(s(T683), s(0), s(T685)) → U10_gga(T683, T685, quot436_in_ga(T683, T685))
quot436_in_ga(0, 0) → quot436_out_ga(0, 0)
quot436_in_ga(s(T705), s(T707)) → U17_ga(T705, T707, quot436_in_ga(T705, T707))
U17_ga(T705, T707, quot436_out_ga(T705, T707)) → quot436_out_ga(s(T705), s(T707))
U10_gga(T683, T685, quot436_out_ga(T683, T685)) → quot3_out_gga(s(T683), s(0), s(T685))
U2_ggga(T241, T242, T244, quot3_out_gga(T241, s(T242), T244)) → quot84_out_ggga(T241, 0, T242, s(T244))
U1_ggga(T226, T227, T228, T230, quot84_out_ggga(T226, T227, T228, T230)) → quot84_out_ggga(s(T226), s(T227), T228, T230)
U3_gga(T189, T190, T192, quot84_out_ggga(T189, T190, s(s(s(s(s(s(s(T190))))))), T192)) → quot3_out_gga(s(s(s(s(s(s(s(s(T189)))))))), s(s(s(s(s(s(s(s(T190)))))))), T192)
U18_gga(T7, T8, T10, quot3_out_gga(T7, T8, T10)) → div1_out_gga(T7, T8, T10)

The argument filtering Pi contains the following mapping:
div1_in_gga(x1, x2, x3)  =  div1_in_gga(x1, x2)
U18_gga(x1, x2, x3, x4)  =  U18_gga(x4)
quot3_in_gga(x1, x2, x3)  =  quot3_in_gga(x1, x2)
0  =  0
s(x1)  =  s(x1)
quot3_out_gga(x1, x2, x3)  =  quot3_out_gga(x3)
U3_gga(x1, x2, x3, x4)  =  U3_gga(x4)
quot84_in_ggga(x1, x2, x3, x4)  =  quot84_in_ggga(x1, x2, x3)
quot84_out_ggga(x1, x2, x3, x4)  =  quot84_out_ggga(x4)
U1_ggga(x1, x2, x3, x4, x5)  =  U1_ggga(x5)
U2_ggga(x1, x2, x3, x4)  =  U2_ggga(x4)
U4_gga(x1, x2, x3)  =  U4_gga(x3)
quot97_in_ga(x1, x2)  =  quot97_in_ga(x1)
quot97_out_ga(x1, x2)  =  quot97_out_ga(x2)
U11_ga(x1, x2, x3)  =  U11_ga(x3)
U5_gga(x1, x2, x3)  =  U5_gga(x3)
quot181_in_ga(x1, x2)  =  quot181_in_ga(x1)
quot181_out_ga(x1, x2)  =  quot181_out_ga(x2)
U12_ga(x1, x2, x3)  =  U12_ga(x3)
U6_gga(x1, x2, x3)  =  U6_gga(x3)
quot254_in_ga(x1, x2)  =  quot254_in_ga(x1)
quot254_out_ga(x1, x2)  =  quot254_out_ga(x2)
U13_ga(x1, x2, x3)  =  U13_ga(x3)
U7_gga(x1, x2, x3)  =  U7_gga(x3)
quot316_in_ga(x1, x2)  =  quot316_in_ga(x1)
quot316_out_ga(x1, x2)  =  quot316_out_ga(x2)
U14_ga(x1, x2, x3)  =  U14_ga(x3)
U8_gga(x1, x2, x3)  =  U8_gga(x3)
quot367_in_ga(x1, x2)  =  quot367_in_ga(x1)
quot367_out_ga(x1, x2)  =  quot367_out_ga(x2)
U15_ga(x1, x2, x3)  =  U15_ga(x3)
U9_gga(x1, x2, x3)  =  U9_gga(x3)
quot407_in_ga(x1, x2)  =  quot407_in_ga(x1)
quot407_out_ga(x1, x2)  =  quot407_out_ga(x2)
U16_ga(x1, x2, x3)  =  U16_ga(x3)
U10_gga(x1, x2, x3)  =  U10_gga(x3)
quot436_in_ga(x1, x2)  =  quot436_in_ga(x1)
quot436_out_ga(x1, x2)  =  quot436_out_ga(x2)
U17_ga(x1, x2, x3)  =  U17_ga(x3)
div1_out_gga(x1, x2, x3)  =  div1_out_gga(x3)

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

DIV1_IN_GGA(T7, T8, T10) → U18_GGA(T7, T8, T10, quot3_in_gga(T7, T8, T10))
DIV1_IN_GGA(T7, T8, T10) → QUOT3_IN_GGA(T7, T8, T10)
QUOT3_IN_GGA(s(s(s(s(s(s(s(s(T189)))))))), s(s(s(s(s(s(s(s(T190)))))))), T192) → U3_GGA(T189, T190, T192, quot84_in_ggga(T189, T190, s(s(s(s(s(s(s(T190))))))), T192))
QUOT3_IN_GGA(s(s(s(s(s(s(s(s(T189)))))))), s(s(s(s(s(s(s(s(T190)))))))), T192) → QUOT84_IN_GGGA(T189, T190, s(s(s(s(s(s(s(T190))))))), T192)
QUOT84_IN_GGGA(s(T226), s(T227), T228, T230) → U1_GGGA(T226, T227, T228, T230, quot84_in_ggga(T226, T227, T228, T230))
QUOT84_IN_GGGA(s(T226), s(T227), T228, T230) → QUOT84_IN_GGGA(T226, T227, T228, T230)
QUOT84_IN_GGGA(T241, 0, T242, s(T244)) → U2_GGGA(T241, T242, T244, quot3_in_gga(T241, s(T242), T244))
QUOT84_IN_GGGA(T241, 0, T242, s(T244)) → QUOT3_IN_GGA(T241, s(T242), T244)
QUOT3_IN_GGA(s(s(s(s(s(s(s(T251))))))), s(s(s(s(s(s(s(0))))))), s(T253)) → U4_GGA(T251, T253, quot97_in_ga(T251, T253))
QUOT3_IN_GGA(s(s(s(s(s(s(s(T251))))))), s(s(s(s(s(s(s(0))))))), s(T253)) → QUOT97_IN_GA(T251, T253)
QUOT97_IN_GA(s(s(s(s(s(s(s(T339))))))), s(T341)) → U11_GA(T339, T341, quot97_in_ga(T339, T341))
QUOT97_IN_GA(s(s(s(s(s(s(s(T339))))))), s(T341)) → QUOT97_IN_GA(T339, T341)
QUOT3_IN_GGA(s(s(s(s(s(s(T353)))))), s(s(s(s(s(s(0)))))), s(T355)) → U5_GGA(T353, T355, quot181_in_ga(T353, T355))
QUOT3_IN_GGA(s(s(s(s(s(s(T353)))))), s(s(s(s(s(s(0)))))), s(T355)) → QUOT181_IN_GA(T353, T355)
QUOT181_IN_GA(s(s(s(s(s(s(T430)))))), s(T432)) → U12_GA(T430, T432, quot181_in_ga(T430, T432))
QUOT181_IN_GA(s(s(s(s(s(s(T430)))))), s(T432)) → QUOT181_IN_GA(T430, T432)
QUOT3_IN_GGA(s(s(s(s(s(T443))))), s(s(s(s(s(0))))), s(T445)) → U6_GGA(T443, T445, quot254_in_ga(T443, T445))
QUOT3_IN_GGA(s(s(s(s(s(T443))))), s(s(s(s(s(0))))), s(T445)) → QUOT254_IN_GA(T443, T445)
QUOT254_IN_GA(s(s(s(s(s(T509))))), s(T511)) → U13_GA(T509, T511, quot254_in_ga(T509, T511))
QUOT254_IN_GA(s(s(s(s(s(T509))))), s(T511)) → QUOT254_IN_GA(T509, T511)
QUOT3_IN_GGA(s(s(s(s(T521)))), s(s(s(s(0)))), s(T523)) → U7_GGA(T521, T523, quot316_in_ga(T521, T523))
QUOT3_IN_GGA(s(s(s(s(T521)))), s(s(s(s(0)))), s(T523)) → QUOT316_IN_GA(T521, T523)
QUOT316_IN_GA(s(s(s(s(T576)))), s(T578)) → U14_GA(T576, T578, quot316_in_ga(T576, T578))
QUOT316_IN_GA(s(s(s(s(T576)))), s(T578)) → QUOT316_IN_GA(T576, T578)
QUOT3_IN_GGA(s(s(s(T587))), s(s(s(0))), s(T589)) → U8_GGA(T587, T589, quot367_in_ga(T587, T589))
QUOT3_IN_GGA(s(s(s(T587))), s(s(s(0))), s(T589)) → QUOT367_IN_GA(T587, T589)
QUOT367_IN_GA(s(s(s(T631))), s(T633)) → U15_GA(T631, T633, quot367_in_ga(T631, T633))
QUOT367_IN_GA(s(s(s(T631))), s(T633)) → QUOT367_IN_GA(T631, T633)
QUOT3_IN_GGA(s(s(T641)), s(s(0)), s(T643)) → U9_GGA(T641, T643, quot407_in_ga(T641, T643))
QUOT3_IN_GGA(s(s(T641)), s(s(0)), s(T643)) → QUOT407_IN_GA(T641, T643)
QUOT407_IN_GA(s(s(T674)), s(T676)) → U16_GA(T674, T676, quot407_in_ga(T674, T676))
QUOT407_IN_GA(s(s(T674)), s(T676)) → QUOT407_IN_GA(T674, T676)
QUOT3_IN_GGA(s(T683), s(0), s(T685)) → U10_GGA(T683, T685, quot436_in_ga(T683, T685))
QUOT3_IN_GGA(s(T683), s(0), s(T685)) → QUOT436_IN_GA(T683, T685)
QUOT436_IN_GA(s(T705), s(T707)) → U17_GA(T705, T707, quot436_in_ga(T705, T707))
QUOT436_IN_GA(s(T705), s(T707)) → QUOT436_IN_GA(T705, T707)

The TRS R consists of the following rules:

div1_in_gga(T7, T8, T10) → U18_gga(T7, T8, T10, quot3_in_gga(T7, T8, T10))
quot3_in_gga(0, s(T15), 0) → quot3_out_gga(0, s(T15), 0)
quot3_in_gga(s(0), s(s(T38)), 0) → quot3_out_gga(s(0), s(s(T38)), 0)
quot3_in_gga(s(s(0)), s(s(s(T61))), 0) → quot3_out_gga(s(s(0)), s(s(s(T61))), 0)
quot3_in_gga(s(s(s(0))), s(s(s(s(T84)))), 0) → quot3_out_gga(s(s(s(0))), s(s(s(s(T84)))), 0)
quot3_in_gga(s(s(s(s(0)))), s(s(s(s(s(T107))))), 0) → quot3_out_gga(s(s(s(s(0)))), s(s(s(s(s(T107))))), 0)
quot3_in_gga(s(s(s(s(s(0))))), s(s(s(s(s(s(T130)))))), 0) → quot3_out_gga(s(s(s(s(s(0))))), s(s(s(s(s(s(T130)))))), 0)
quot3_in_gga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T153))))))), 0) → quot3_out_gga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T153))))))), 0)
quot3_in_gga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(T176)))))))), 0) → quot3_out_gga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(T176)))))))), 0)
quot3_in_gga(s(s(s(s(s(s(s(s(T189)))))))), s(s(s(s(s(s(s(s(T190)))))))), T192) → U3_gga(T189, T190, T192, quot84_in_ggga(T189, T190, s(s(s(s(s(s(s(T190))))))), T192))
quot84_in_ggga(0, s(T208), T209, 0) → quot84_out_ggga(0, s(T208), T209, 0)
quot84_in_ggga(s(T226), s(T227), T228, T230) → U1_ggga(T226, T227, T228, T230, quot84_in_ggga(T226, T227, T228, T230))
quot84_in_ggga(T241, 0, T242, s(T244)) → U2_ggga(T241, T242, T244, quot3_in_gga(T241, s(T242), T244))
quot3_in_gga(s(s(s(s(s(s(s(T251))))))), s(s(s(s(s(s(s(0))))))), s(T253)) → U4_gga(T251, T253, quot97_in_ga(T251, T253))
quot97_in_ga(0, 0) → quot97_out_ga(0, 0)
quot97_in_ga(s(0), 0) → quot97_out_ga(s(0), 0)
quot97_in_ga(s(s(0)), 0) → quot97_out_ga(s(s(0)), 0)
quot97_in_ga(s(s(s(0))), 0) → quot97_out_ga(s(s(s(0))), 0)
quot97_in_ga(s(s(s(s(0)))), 0) → quot97_out_ga(s(s(s(s(0)))), 0)
quot97_in_ga(s(s(s(s(s(0))))), 0) → quot97_out_ga(s(s(s(s(s(0))))), 0)
quot97_in_ga(s(s(s(s(s(s(0)))))), 0) → quot97_out_ga(s(s(s(s(s(s(0)))))), 0)
quot97_in_ga(s(s(s(s(s(s(s(T339))))))), s(T341)) → U11_ga(T339, T341, quot97_in_ga(T339, T341))
U11_ga(T339, T341, quot97_out_ga(T339, T341)) → quot97_out_ga(s(s(s(s(s(s(s(T339))))))), s(T341))
U4_gga(T251, T253, quot97_out_ga(T251, T253)) → quot3_out_gga(s(s(s(s(s(s(s(T251))))))), s(s(s(s(s(s(s(0))))))), s(T253))
quot3_in_gga(s(s(s(s(s(s(T353)))))), s(s(s(s(s(s(0)))))), s(T355)) → U5_gga(T353, T355, quot181_in_ga(T353, T355))
quot181_in_ga(0, 0) → quot181_out_ga(0, 0)
quot181_in_ga(s(0), 0) → quot181_out_ga(s(0), 0)
quot181_in_ga(s(s(0)), 0) → quot181_out_ga(s(s(0)), 0)
quot181_in_ga(s(s(s(0))), 0) → quot181_out_ga(s(s(s(0))), 0)
quot181_in_ga(s(s(s(s(0)))), 0) → quot181_out_ga(s(s(s(s(0)))), 0)
quot181_in_ga(s(s(s(s(s(0))))), 0) → quot181_out_ga(s(s(s(s(s(0))))), 0)
quot181_in_ga(s(s(s(s(s(s(T430)))))), s(T432)) → U12_ga(T430, T432, quot181_in_ga(T430, T432))
U12_ga(T430, T432, quot181_out_ga(T430, T432)) → quot181_out_ga(s(s(s(s(s(s(T430)))))), s(T432))
U5_gga(T353, T355, quot181_out_ga(T353, T355)) → quot3_out_gga(s(s(s(s(s(s(T353)))))), s(s(s(s(s(s(0)))))), s(T355))
quot3_in_gga(s(s(s(s(s(T443))))), s(s(s(s(s(0))))), s(T445)) → U6_gga(T443, T445, quot254_in_ga(T443, T445))
quot254_in_ga(0, 0) → quot254_out_ga(0, 0)
quot254_in_ga(s(0), 0) → quot254_out_ga(s(0), 0)
quot254_in_ga(s(s(0)), 0) → quot254_out_ga(s(s(0)), 0)
quot254_in_ga(s(s(s(0))), 0) → quot254_out_ga(s(s(s(0))), 0)
quot254_in_ga(s(s(s(s(0)))), 0) → quot254_out_ga(s(s(s(s(0)))), 0)
quot254_in_ga(s(s(s(s(s(T509))))), s(T511)) → U13_ga(T509, T511, quot254_in_ga(T509, T511))
U13_ga(T509, T511, quot254_out_ga(T509, T511)) → quot254_out_ga(s(s(s(s(s(T509))))), s(T511))
U6_gga(T443, T445, quot254_out_ga(T443, T445)) → quot3_out_gga(s(s(s(s(s(T443))))), s(s(s(s(s(0))))), s(T445))
quot3_in_gga(s(s(s(s(T521)))), s(s(s(s(0)))), s(T523)) → U7_gga(T521, T523, quot316_in_ga(T521, T523))
quot316_in_ga(0, 0) → quot316_out_ga(0, 0)
quot316_in_ga(s(0), 0) → quot316_out_ga(s(0), 0)
quot316_in_ga(s(s(0)), 0) → quot316_out_ga(s(s(0)), 0)
quot316_in_ga(s(s(s(0))), 0) → quot316_out_ga(s(s(s(0))), 0)
quot316_in_ga(s(s(s(s(T576)))), s(T578)) → U14_ga(T576, T578, quot316_in_ga(T576, T578))
U14_ga(T576, T578, quot316_out_ga(T576, T578)) → quot316_out_ga(s(s(s(s(T576)))), s(T578))
U7_gga(T521, T523, quot316_out_ga(T521, T523)) → quot3_out_gga(s(s(s(s(T521)))), s(s(s(s(0)))), s(T523))
quot3_in_gga(s(s(s(T587))), s(s(s(0))), s(T589)) → U8_gga(T587, T589, quot367_in_ga(T587, T589))
quot367_in_ga(0, 0) → quot367_out_ga(0, 0)
quot367_in_ga(s(0), 0) → quot367_out_ga(s(0), 0)
quot367_in_ga(s(s(0)), 0) → quot367_out_ga(s(s(0)), 0)
quot367_in_ga(s(s(s(T631))), s(T633)) → U15_ga(T631, T633, quot367_in_ga(T631, T633))
U15_ga(T631, T633, quot367_out_ga(T631, T633)) → quot367_out_ga(s(s(s(T631))), s(T633))
U8_gga(T587, T589, quot367_out_ga(T587, T589)) → quot3_out_gga(s(s(s(T587))), s(s(s(0))), s(T589))
quot3_in_gga(s(s(T641)), s(s(0)), s(T643)) → U9_gga(T641, T643, quot407_in_ga(T641, T643))
quot407_in_ga(0, 0) → quot407_out_ga(0, 0)
quot407_in_ga(s(0), 0) → quot407_out_ga(s(0), 0)
quot407_in_ga(s(s(T674)), s(T676)) → U16_ga(T674, T676, quot407_in_ga(T674, T676))
U16_ga(T674, T676, quot407_out_ga(T674, T676)) → quot407_out_ga(s(s(T674)), s(T676))
U9_gga(T641, T643, quot407_out_ga(T641, T643)) → quot3_out_gga(s(s(T641)), s(s(0)), s(T643))
quot3_in_gga(s(T683), s(0), s(T685)) → U10_gga(T683, T685, quot436_in_ga(T683, T685))
quot436_in_ga(0, 0) → quot436_out_ga(0, 0)
quot436_in_ga(s(T705), s(T707)) → U17_ga(T705, T707, quot436_in_ga(T705, T707))
U17_ga(T705, T707, quot436_out_ga(T705, T707)) → quot436_out_ga(s(T705), s(T707))
U10_gga(T683, T685, quot436_out_ga(T683, T685)) → quot3_out_gga(s(T683), s(0), s(T685))
U2_ggga(T241, T242, T244, quot3_out_gga(T241, s(T242), T244)) → quot84_out_ggga(T241, 0, T242, s(T244))
U1_ggga(T226, T227, T228, T230, quot84_out_ggga(T226, T227, T228, T230)) → quot84_out_ggga(s(T226), s(T227), T228, T230)
U3_gga(T189, T190, T192, quot84_out_ggga(T189, T190, s(s(s(s(s(s(s(T190))))))), T192)) → quot3_out_gga(s(s(s(s(s(s(s(s(T189)))))))), s(s(s(s(s(s(s(s(T190)))))))), T192)
U18_gga(T7, T8, T10, quot3_out_gga(T7, T8, T10)) → div1_out_gga(T7, T8, T10)

The argument filtering Pi contains the following mapping:
div1_in_gga(x1, x2, x3)  =  div1_in_gga(x1, x2)
U18_gga(x1, x2, x3, x4)  =  U18_gga(x4)
quot3_in_gga(x1, x2, x3)  =  quot3_in_gga(x1, x2)
0  =  0
s(x1)  =  s(x1)
quot3_out_gga(x1, x2, x3)  =  quot3_out_gga(x3)
U3_gga(x1, x2, x3, x4)  =  U3_gga(x4)
quot84_in_ggga(x1, x2, x3, x4)  =  quot84_in_ggga(x1, x2, x3)
quot84_out_ggga(x1, x2, x3, x4)  =  quot84_out_ggga(x4)
U1_ggga(x1, x2, x3, x4, x5)  =  U1_ggga(x5)
U2_ggga(x1, x2, x3, x4)  =  U2_ggga(x4)
U4_gga(x1, x2, x3)  =  U4_gga(x3)
quot97_in_ga(x1, x2)  =  quot97_in_ga(x1)
quot97_out_ga(x1, x2)  =  quot97_out_ga(x2)
U11_ga(x1, x2, x3)  =  U11_ga(x3)
U5_gga(x1, x2, x3)  =  U5_gga(x3)
quot181_in_ga(x1, x2)  =  quot181_in_ga(x1)
quot181_out_ga(x1, x2)  =  quot181_out_ga(x2)
U12_ga(x1, x2, x3)  =  U12_ga(x3)
U6_gga(x1, x2, x3)  =  U6_gga(x3)
quot254_in_ga(x1, x2)  =  quot254_in_ga(x1)
quot254_out_ga(x1, x2)  =  quot254_out_ga(x2)
U13_ga(x1, x2, x3)  =  U13_ga(x3)
U7_gga(x1, x2, x3)  =  U7_gga(x3)
quot316_in_ga(x1, x2)  =  quot316_in_ga(x1)
quot316_out_ga(x1, x2)  =  quot316_out_ga(x2)
U14_ga(x1, x2, x3)  =  U14_ga(x3)
U8_gga(x1, x2, x3)  =  U8_gga(x3)
quot367_in_ga(x1, x2)  =  quot367_in_ga(x1)
quot367_out_ga(x1, x2)  =  quot367_out_ga(x2)
U15_ga(x1, x2, x3)  =  U15_ga(x3)
U9_gga(x1, x2, x3)  =  U9_gga(x3)
quot407_in_ga(x1, x2)  =  quot407_in_ga(x1)
quot407_out_ga(x1, x2)  =  quot407_out_ga(x2)
U16_ga(x1, x2, x3)  =  U16_ga(x3)
U10_gga(x1, x2, x3)  =  U10_gga(x3)
quot436_in_ga(x1, x2)  =  quot436_in_ga(x1)
quot436_out_ga(x1, x2)  =  quot436_out_ga(x2)
U17_ga(x1, x2, x3)  =  U17_ga(x3)
div1_out_gga(x1, x2, x3)  =  div1_out_gga(x3)
DIV1_IN_GGA(x1, x2, x3)  =  DIV1_IN_GGA(x1, x2)
U18_GGA(x1, x2, x3, x4)  =  U18_GGA(x4)
QUOT3_IN_GGA(x1, x2, x3)  =  QUOT3_IN_GGA(x1, x2)
U3_GGA(x1, x2, x3, x4)  =  U3_GGA(x4)
QUOT84_IN_GGGA(x1, x2, x3, x4)  =  QUOT84_IN_GGGA(x1, x2, x3)
U1_GGGA(x1, x2, x3, x4, x5)  =  U1_GGGA(x5)
U2_GGGA(x1, x2, x3, x4)  =  U2_GGGA(x4)
U4_GGA(x1, x2, x3)  =  U4_GGA(x3)
QUOT97_IN_GA(x1, x2)  =  QUOT97_IN_GA(x1)
U11_GA(x1, x2, x3)  =  U11_GA(x3)
U5_GGA(x1, x2, x3)  =  U5_GGA(x3)
QUOT181_IN_GA(x1, x2)  =  QUOT181_IN_GA(x1)
U12_GA(x1, x2, x3)  =  U12_GA(x3)
U6_GGA(x1, x2, x3)  =  U6_GGA(x3)
QUOT254_IN_GA(x1, x2)  =  QUOT254_IN_GA(x1)
U13_GA(x1, x2, x3)  =  U13_GA(x3)
U7_GGA(x1, x2, x3)  =  U7_GGA(x3)
QUOT316_IN_GA(x1, x2)  =  QUOT316_IN_GA(x1)
U14_GA(x1, x2, x3)  =  U14_GA(x3)
U8_GGA(x1, x2, x3)  =  U8_GGA(x3)
QUOT367_IN_GA(x1, x2)  =  QUOT367_IN_GA(x1)
U15_GA(x1, x2, x3)  =  U15_GA(x3)
U9_GGA(x1, x2, x3)  =  U9_GGA(x3)
QUOT407_IN_GA(x1, x2)  =  QUOT407_IN_GA(x1)
U16_GA(x1, x2, x3)  =  U16_GA(x3)
U10_GGA(x1, x2, x3)  =  U10_GGA(x3)
QUOT436_IN_GA(x1, x2)  =  QUOT436_IN_GA(x1)
U17_GA(x1, x2, x3)  =  U17_GA(x3)

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

(6) Obligation:

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

DIV1_IN_GGA(T7, T8, T10) → U18_GGA(T7, T8, T10, quot3_in_gga(T7, T8, T10))
DIV1_IN_GGA(T7, T8, T10) → QUOT3_IN_GGA(T7, T8, T10)
QUOT3_IN_GGA(s(s(s(s(s(s(s(s(T189)))))))), s(s(s(s(s(s(s(s(T190)))))))), T192) → U3_GGA(T189, T190, T192, quot84_in_ggga(T189, T190, s(s(s(s(s(s(s(T190))))))), T192))
QUOT3_IN_GGA(s(s(s(s(s(s(s(s(T189)))))))), s(s(s(s(s(s(s(s(T190)))))))), T192) → QUOT84_IN_GGGA(T189, T190, s(s(s(s(s(s(s(T190))))))), T192)
QUOT84_IN_GGGA(s(T226), s(T227), T228, T230) → U1_GGGA(T226, T227, T228, T230, quot84_in_ggga(T226, T227, T228, T230))
QUOT84_IN_GGGA(s(T226), s(T227), T228, T230) → QUOT84_IN_GGGA(T226, T227, T228, T230)
QUOT84_IN_GGGA(T241, 0, T242, s(T244)) → U2_GGGA(T241, T242, T244, quot3_in_gga(T241, s(T242), T244))
QUOT84_IN_GGGA(T241, 0, T242, s(T244)) → QUOT3_IN_GGA(T241, s(T242), T244)
QUOT3_IN_GGA(s(s(s(s(s(s(s(T251))))))), s(s(s(s(s(s(s(0))))))), s(T253)) → U4_GGA(T251, T253, quot97_in_ga(T251, T253))
QUOT3_IN_GGA(s(s(s(s(s(s(s(T251))))))), s(s(s(s(s(s(s(0))))))), s(T253)) → QUOT97_IN_GA(T251, T253)
QUOT97_IN_GA(s(s(s(s(s(s(s(T339))))))), s(T341)) → U11_GA(T339, T341, quot97_in_ga(T339, T341))
QUOT97_IN_GA(s(s(s(s(s(s(s(T339))))))), s(T341)) → QUOT97_IN_GA(T339, T341)
QUOT3_IN_GGA(s(s(s(s(s(s(T353)))))), s(s(s(s(s(s(0)))))), s(T355)) → U5_GGA(T353, T355, quot181_in_ga(T353, T355))
QUOT3_IN_GGA(s(s(s(s(s(s(T353)))))), s(s(s(s(s(s(0)))))), s(T355)) → QUOT181_IN_GA(T353, T355)
QUOT181_IN_GA(s(s(s(s(s(s(T430)))))), s(T432)) → U12_GA(T430, T432, quot181_in_ga(T430, T432))
QUOT181_IN_GA(s(s(s(s(s(s(T430)))))), s(T432)) → QUOT181_IN_GA(T430, T432)
QUOT3_IN_GGA(s(s(s(s(s(T443))))), s(s(s(s(s(0))))), s(T445)) → U6_GGA(T443, T445, quot254_in_ga(T443, T445))
QUOT3_IN_GGA(s(s(s(s(s(T443))))), s(s(s(s(s(0))))), s(T445)) → QUOT254_IN_GA(T443, T445)
QUOT254_IN_GA(s(s(s(s(s(T509))))), s(T511)) → U13_GA(T509, T511, quot254_in_ga(T509, T511))
QUOT254_IN_GA(s(s(s(s(s(T509))))), s(T511)) → QUOT254_IN_GA(T509, T511)
QUOT3_IN_GGA(s(s(s(s(T521)))), s(s(s(s(0)))), s(T523)) → U7_GGA(T521, T523, quot316_in_ga(T521, T523))
QUOT3_IN_GGA(s(s(s(s(T521)))), s(s(s(s(0)))), s(T523)) → QUOT316_IN_GA(T521, T523)
QUOT316_IN_GA(s(s(s(s(T576)))), s(T578)) → U14_GA(T576, T578, quot316_in_ga(T576, T578))
QUOT316_IN_GA(s(s(s(s(T576)))), s(T578)) → QUOT316_IN_GA(T576, T578)
QUOT3_IN_GGA(s(s(s(T587))), s(s(s(0))), s(T589)) → U8_GGA(T587, T589, quot367_in_ga(T587, T589))
QUOT3_IN_GGA(s(s(s(T587))), s(s(s(0))), s(T589)) → QUOT367_IN_GA(T587, T589)
QUOT367_IN_GA(s(s(s(T631))), s(T633)) → U15_GA(T631, T633, quot367_in_ga(T631, T633))
QUOT367_IN_GA(s(s(s(T631))), s(T633)) → QUOT367_IN_GA(T631, T633)
QUOT3_IN_GGA(s(s(T641)), s(s(0)), s(T643)) → U9_GGA(T641, T643, quot407_in_ga(T641, T643))
QUOT3_IN_GGA(s(s(T641)), s(s(0)), s(T643)) → QUOT407_IN_GA(T641, T643)
QUOT407_IN_GA(s(s(T674)), s(T676)) → U16_GA(T674, T676, quot407_in_ga(T674, T676))
QUOT407_IN_GA(s(s(T674)), s(T676)) → QUOT407_IN_GA(T674, T676)
QUOT3_IN_GGA(s(T683), s(0), s(T685)) → U10_GGA(T683, T685, quot436_in_ga(T683, T685))
QUOT3_IN_GGA(s(T683), s(0), s(T685)) → QUOT436_IN_GA(T683, T685)
QUOT436_IN_GA(s(T705), s(T707)) → U17_GA(T705, T707, quot436_in_ga(T705, T707))
QUOT436_IN_GA(s(T705), s(T707)) → QUOT436_IN_GA(T705, T707)

The TRS R consists of the following rules:

div1_in_gga(T7, T8, T10) → U18_gga(T7, T8, T10, quot3_in_gga(T7, T8, T10))
quot3_in_gga(0, s(T15), 0) → quot3_out_gga(0, s(T15), 0)
quot3_in_gga(s(0), s(s(T38)), 0) → quot3_out_gga(s(0), s(s(T38)), 0)
quot3_in_gga(s(s(0)), s(s(s(T61))), 0) → quot3_out_gga(s(s(0)), s(s(s(T61))), 0)
quot3_in_gga(s(s(s(0))), s(s(s(s(T84)))), 0) → quot3_out_gga(s(s(s(0))), s(s(s(s(T84)))), 0)
quot3_in_gga(s(s(s(s(0)))), s(s(s(s(s(T107))))), 0) → quot3_out_gga(s(s(s(s(0)))), s(s(s(s(s(T107))))), 0)
quot3_in_gga(s(s(s(s(s(0))))), s(s(s(s(s(s(T130)))))), 0) → quot3_out_gga(s(s(s(s(s(0))))), s(s(s(s(s(s(T130)))))), 0)
quot3_in_gga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T153))))))), 0) → quot3_out_gga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T153))))))), 0)
quot3_in_gga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(T176)))))))), 0) → quot3_out_gga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(T176)))))))), 0)
quot3_in_gga(s(s(s(s(s(s(s(s(T189)))))))), s(s(s(s(s(s(s(s(T190)))))))), T192) → U3_gga(T189, T190, T192, quot84_in_ggga(T189, T190, s(s(s(s(s(s(s(T190))))))), T192))
quot84_in_ggga(0, s(T208), T209, 0) → quot84_out_ggga(0, s(T208), T209, 0)
quot84_in_ggga(s(T226), s(T227), T228, T230) → U1_ggga(T226, T227, T228, T230, quot84_in_ggga(T226, T227, T228, T230))
quot84_in_ggga(T241, 0, T242, s(T244)) → U2_ggga(T241, T242, T244, quot3_in_gga(T241, s(T242), T244))
quot3_in_gga(s(s(s(s(s(s(s(T251))))))), s(s(s(s(s(s(s(0))))))), s(T253)) → U4_gga(T251, T253, quot97_in_ga(T251, T253))
quot97_in_ga(0, 0) → quot97_out_ga(0, 0)
quot97_in_ga(s(0), 0) → quot97_out_ga(s(0), 0)
quot97_in_ga(s(s(0)), 0) → quot97_out_ga(s(s(0)), 0)
quot97_in_ga(s(s(s(0))), 0) → quot97_out_ga(s(s(s(0))), 0)
quot97_in_ga(s(s(s(s(0)))), 0) → quot97_out_ga(s(s(s(s(0)))), 0)
quot97_in_ga(s(s(s(s(s(0))))), 0) → quot97_out_ga(s(s(s(s(s(0))))), 0)
quot97_in_ga(s(s(s(s(s(s(0)))))), 0) → quot97_out_ga(s(s(s(s(s(s(0)))))), 0)
quot97_in_ga(s(s(s(s(s(s(s(T339))))))), s(T341)) → U11_ga(T339, T341, quot97_in_ga(T339, T341))
U11_ga(T339, T341, quot97_out_ga(T339, T341)) → quot97_out_ga(s(s(s(s(s(s(s(T339))))))), s(T341))
U4_gga(T251, T253, quot97_out_ga(T251, T253)) → quot3_out_gga(s(s(s(s(s(s(s(T251))))))), s(s(s(s(s(s(s(0))))))), s(T253))
quot3_in_gga(s(s(s(s(s(s(T353)))))), s(s(s(s(s(s(0)))))), s(T355)) → U5_gga(T353, T355, quot181_in_ga(T353, T355))
quot181_in_ga(0, 0) → quot181_out_ga(0, 0)
quot181_in_ga(s(0), 0) → quot181_out_ga(s(0), 0)
quot181_in_ga(s(s(0)), 0) → quot181_out_ga(s(s(0)), 0)
quot181_in_ga(s(s(s(0))), 0) → quot181_out_ga(s(s(s(0))), 0)
quot181_in_ga(s(s(s(s(0)))), 0) → quot181_out_ga(s(s(s(s(0)))), 0)
quot181_in_ga(s(s(s(s(s(0))))), 0) → quot181_out_ga(s(s(s(s(s(0))))), 0)
quot181_in_ga(s(s(s(s(s(s(T430)))))), s(T432)) → U12_ga(T430, T432, quot181_in_ga(T430, T432))
U12_ga(T430, T432, quot181_out_ga(T430, T432)) → quot181_out_ga(s(s(s(s(s(s(T430)))))), s(T432))
U5_gga(T353, T355, quot181_out_ga(T353, T355)) → quot3_out_gga(s(s(s(s(s(s(T353)))))), s(s(s(s(s(s(0)))))), s(T355))
quot3_in_gga(s(s(s(s(s(T443))))), s(s(s(s(s(0))))), s(T445)) → U6_gga(T443, T445, quot254_in_ga(T443, T445))
quot254_in_ga(0, 0) → quot254_out_ga(0, 0)
quot254_in_ga(s(0), 0) → quot254_out_ga(s(0), 0)
quot254_in_ga(s(s(0)), 0) → quot254_out_ga(s(s(0)), 0)
quot254_in_ga(s(s(s(0))), 0) → quot254_out_ga(s(s(s(0))), 0)
quot254_in_ga(s(s(s(s(0)))), 0) → quot254_out_ga(s(s(s(s(0)))), 0)
quot254_in_ga(s(s(s(s(s(T509))))), s(T511)) → U13_ga(T509, T511, quot254_in_ga(T509, T511))
U13_ga(T509, T511, quot254_out_ga(T509, T511)) → quot254_out_ga(s(s(s(s(s(T509))))), s(T511))
U6_gga(T443, T445, quot254_out_ga(T443, T445)) → quot3_out_gga(s(s(s(s(s(T443))))), s(s(s(s(s(0))))), s(T445))
quot3_in_gga(s(s(s(s(T521)))), s(s(s(s(0)))), s(T523)) → U7_gga(T521, T523, quot316_in_ga(T521, T523))
quot316_in_ga(0, 0) → quot316_out_ga(0, 0)
quot316_in_ga(s(0), 0) → quot316_out_ga(s(0), 0)
quot316_in_ga(s(s(0)), 0) → quot316_out_ga(s(s(0)), 0)
quot316_in_ga(s(s(s(0))), 0) → quot316_out_ga(s(s(s(0))), 0)
quot316_in_ga(s(s(s(s(T576)))), s(T578)) → U14_ga(T576, T578, quot316_in_ga(T576, T578))
U14_ga(T576, T578, quot316_out_ga(T576, T578)) → quot316_out_ga(s(s(s(s(T576)))), s(T578))
U7_gga(T521, T523, quot316_out_ga(T521, T523)) → quot3_out_gga(s(s(s(s(T521)))), s(s(s(s(0)))), s(T523))
quot3_in_gga(s(s(s(T587))), s(s(s(0))), s(T589)) → U8_gga(T587, T589, quot367_in_ga(T587, T589))
quot367_in_ga(0, 0) → quot367_out_ga(0, 0)
quot367_in_ga(s(0), 0) → quot367_out_ga(s(0), 0)
quot367_in_ga(s(s(0)), 0) → quot367_out_ga(s(s(0)), 0)
quot367_in_ga(s(s(s(T631))), s(T633)) → U15_ga(T631, T633, quot367_in_ga(T631, T633))
U15_ga(T631, T633, quot367_out_ga(T631, T633)) → quot367_out_ga(s(s(s(T631))), s(T633))
U8_gga(T587, T589, quot367_out_ga(T587, T589)) → quot3_out_gga(s(s(s(T587))), s(s(s(0))), s(T589))
quot3_in_gga(s(s(T641)), s(s(0)), s(T643)) → U9_gga(T641, T643, quot407_in_ga(T641, T643))
quot407_in_ga(0, 0) → quot407_out_ga(0, 0)
quot407_in_ga(s(0), 0) → quot407_out_ga(s(0), 0)
quot407_in_ga(s(s(T674)), s(T676)) → U16_ga(T674, T676, quot407_in_ga(T674, T676))
U16_ga(T674, T676, quot407_out_ga(T674, T676)) → quot407_out_ga(s(s(T674)), s(T676))
U9_gga(T641, T643, quot407_out_ga(T641, T643)) → quot3_out_gga(s(s(T641)), s(s(0)), s(T643))
quot3_in_gga(s(T683), s(0), s(T685)) → U10_gga(T683, T685, quot436_in_ga(T683, T685))
quot436_in_ga(0, 0) → quot436_out_ga(0, 0)
quot436_in_ga(s(T705), s(T707)) → U17_ga(T705, T707, quot436_in_ga(T705, T707))
U17_ga(T705, T707, quot436_out_ga(T705, T707)) → quot436_out_ga(s(T705), s(T707))
U10_gga(T683, T685, quot436_out_ga(T683, T685)) → quot3_out_gga(s(T683), s(0), s(T685))
U2_ggga(T241, T242, T244, quot3_out_gga(T241, s(T242), T244)) → quot84_out_ggga(T241, 0, T242, s(T244))
U1_ggga(T226, T227, T228, T230, quot84_out_ggga(T226, T227, T228, T230)) → quot84_out_ggga(s(T226), s(T227), T228, T230)
U3_gga(T189, T190, T192, quot84_out_ggga(T189, T190, s(s(s(s(s(s(s(T190))))))), T192)) → quot3_out_gga(s(s(s(s(s(s(s(s(T189)))))))), s(s(s(s(s(s(s(s(T190)))))))), T192)
U18_gga(T7, T8, T10, quot3_out_gga(T7, T8, T10)) → div1_out_gga(T7, T8, T10)

The argument filtering Pi contains the following mapping:
div1_in_gga(x1, x2, x3)  =  div1_in_gga(x1, x2)
U18_gga(x1, x2, x3, x4)  =  U18_gga(x4)
quot3_in_gga(x1, x2, x3)  =  quot3_in_gga(x1, x2)
0  =  0
s(x1)  =  s(x1)
quot3_out_gga(x1, x2, x3)  =  quot3_out_gga(x3)
U3_gga(x1, x2, x3, x4)  =  U3_gga(x4)
quot84_in_ggga(x1, x2, x3, x4)  =  quot84_in_ggga(x1, x2, x3)
quot84_out_ggga(x1, x2, x3, x4)  =  quot84_out_ggga(x4)
U1_ggga(x1, x2, x3, x4, x5)  =  U1_ggga(x5)
U2_ggga(x1, x2, x3, x4)  =  U2_ggga(x4)
U4_gga(x1, x2, x3)  =  U4_gga(x3)
quot97_in_ga(x1, x2)  =  quot97_in_ga(x1)
quot97_out_ga(x1, x2)  =  quot97_out_ga(x2)
U11_ga(x1, x2, x3)  =  U11_ga(x3)
U5_gga(x1, x2, x3)  =  U5_gga(x3)
quot181_in_ga(x1, x2)  =  quot181_in_ga(x1)
quot181_out_ga(x1, x2)  =  quot181_out_ga(x2)
U12_ga(x1, x2, x3)  =  U12_ga(x3)
U6_gga(x1, x2, x3)  =  U6_gga(x3)
quot254_in_ga(x1, x2)  =  quot254_in_ga(x1)
quot254_out_ga(x1, x2)  =  quot254_out_ga(x2)
U13_ga(x1, x2, x3)  =  U13_ga(x3)
U7_gga(x1, x2, x3)  =  U7_gga(x3)
quot316_in_ga(x1, x2)  =  quot316_in_ga(x1)
quot316_out_ga(x1, x2)  =  quot316_out_ga(x2)
U14_ga(x1, x2, x3)  =  U14_ga(x3)
U8_gga(x1, x2, x3)  =  U8_gga(x3)
quot367_in_ga(x1, x2)  =  quot367_in_ga(x1)
quot367_out_ga(x1, x2)  =  quot367_out_ga(x2)
U15_ga(x1, x2, x3)  =  U15_ga(x3)
U9_gga(x1, x2, x3)  =  U9_gga(x3)
quot407_in_ga(x1, x2)  =  quot407_in_ga(x1)
quot407_out_ga(x1, x2)  =  quot407_out_ga(x2)
U16_ga(x1, x2, x3)  =  U16_ga(x3)
U10_gga(x1, x2, x3)  =  U10_gga(x3)
quot436_in_ga(x1, x2)  =  quot436_in_ga(x1)
quot436_out_ga(x1, x2)  =  quot436_out_ga(x2)
U17_ga(x1, x2, x3)  =  U17_ga(x3)
div1_out_gga(x1, x2, x3)  =  div1_out_gga(x3)
DIV1_IN_GGA(x1, x2, x3)  =  DIV1_IN_GGA(x1, x2)
U18_GGA(x1, x2, x3, x4)  =  U18_GGA(x4)
QUOT3_IN_GGA(x1, x2, x3)  =  QUOT3_IN_GGA(x1, x2)
U3_GGA(x1, x2, x3, x4)  =  U3_GGA(x4)
QUOT84_IN_GGGA(x1, x2, x3, x4)  =  QUOT84_IN_GGGA(x1, x2, x3)
U1_GGGA(x1, x2, x3, x4, x5)  =  U1_GGGA(x5)
U2_GGGA(x1, x2, x3, x4)  =  U2_GGGA(x4)
U4_GGA(x1, x2, x3)  =  U4_GGA(x3)
QUOT97_IN_GA(x1, x2)  =  QUOT97_IN_GA(x1)
U11_GA(x1, x2, x3)  =  U11_GA(x3)
U5_GGA(x1, x2, x3)  =  U5_GGA(x3)
QUOT181_IN_GA(x1, x2)  =  QUOT181_IN_GA(x1)
U12_GA(x1, x2, x3)  =  U12_GA(x3)
U6_GGA(x1, x2, x3)  =  U6_GGA(x3)
QUOT254_IN_GA(x1, x2)  =  QUOT254_IN_GA(x1)
U13_GA(x1, x2, x3)  =  U13_GA(x3)
U7_GGA(x1, x2, x3)  =  U7_GGA(x3)
QUOT316_IN_GA(x1, x2)  =  QUOT316_IN_GA(x1)
U14_GA(x1, x2, x3)  =  U14_GA(x3)
U8_GGA(x1, x2, x3)  =  U8_GGA(x3)
QUOT367_IN_GA(x1, x2)  =  QUOT367_IN_GA(x1)
U15_GA(x1, x2, x3)  =  U15_GA(x3)
U9_GGA(x1, x2, x3)  =  U9_GGA(x3)
QUOT407_IN_GA(x1, x2)  =  QUOT407_IN_GA(x1)
U16_GA(x1, x2, x3)  =  U16_GA(x3)
U10_GGA(x1, x2, x3)  =  U10_GGA(x3)
QUOT436_IN_GA(x1, x2)  =  QUOT436_IN_GA(x1)
U17_GA(x1, x2, x3)  =  U17_GA(x3)

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

(7) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 8 SCCs with 26 less nodes.

(8) Complex Obligation (AND)

(9) Obligation:

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

QUOT436_IN_GA(s(T705), s(T707)) → QUOT436_IN_GA(T705, T707)

The TRS R consists of the following rules:

div1_in_gga(T7, T8, T10) → U18_gga(T7, T8, T10, quot3_in_gga(T7, T8, T10))
quot3_in_gga(0, s(T15), 0) → quot3_out_gga(0, s(T15), 0)
quot3_in_gga(s(0), s(s(T38)), 0) → quot3_out_gga(s(0), s(s(T38)), 0)
quot3_in_gga(s(s(0)), s(s(s(T61))), 0) → quot3_out_gga(s(s(0)), s(s(s(T61))), 0)
quot3_in_gga(s(s(s(0))), s(s(s(s(T84)))), 0) → quot3_out_gga(s(s(s(0))), s(s(s(s(T84)))), 0)
quot3_in_gga(s(s(s(s(0)))), s(s(s(s(s(T107))))), 0) → quot3_out_gga(s(s(s(s(0)))), s(s(s(s(s(T107))))), 0)
quot3_in_gga(s(s(s(s(s(0))))), s(s(s(s(s(s(T130)))))), 0) → quot3_out_gga(s(s(s(s(s(0))))), s(s(s(s(s(s(T130)))))), 0)
quot3_in_gga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T153))))))), 0) → quot3_out_gga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T153))))))), 0)
quot3_in_gga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(T176)))))))), 0) → quot3_out_gga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(T176)))))))), 0)
quot3_in_gga(s(s(s(s(s(s(s(s(T189)))))))), s(s(s(s(s(s(s(s(T190)))))))), T192) → U3_gga(T189, T190, T192, quot84_in_ggga(T189, T190, s(s(s(s(s(s(s(T190))))))), T192))
quot84_in_ggga(0, s(T208), T209, 0) → quot84_out_ggga(0, s(T208), T209, 0)
quot84_in_ggga(s(T226), s(T227), T228, T230) → U1_ggga(T226, T227, T228, T230, quot84_in_ggga(T226, T227, T228, T230))
quot84_in_ggga(T241, 0, T242, s(T244)) → U2_ggga(T241, T242, T244, quot3_in_gga(T241, s(T242), T244))
quot3_in_gga(s(s(s(s(s(s(s(T251))))))), s(s(s(s(s(s(s(0))))))), s(T253)) → U4_gga(T251, T253, quot97_in_ga(T251, T253))
quot97_in_ga(0, 0) → quot97_out_ga(0, 0)
quot97_in_ga(s(0), 0) → quot97_out_ga(s(0), 0)
quot97_in_ga(s(s(0)), 0) → quot97_out_ga(s(s(0)), 0)
quot97_in_ga(s(s(s(0))), 0) → quot97_out_ga(s(s(s(0))), 0)
quot97_in_ga(s(s(s(s(0)))), 0) → quot97_out_ga(s(s(s(s(0)))), 0)
quot97_in_ga(s(s(s(s(s(0))))), 0) → quot97_out_ga(s(s(s(s(s(0))))), 0)
quot97_in_ga(s(s(s(s(s(s(0)))))), 0) → quot97_out_ga(s(s(s(s(s(s(0)))))), 0)
quot97_in_ga(s(s(s(s(s(s(s(T339))))))), s(T341)) → U11_ga(T339, T341, quot97_in_ga(T339, T341))
U11_ga(T339, T341, quot97_out_ga(T339, T341)) → quot97_out_ga(s(s(s(s(s(s(s(T339))))))), s(T341))
U4_gga(T251, T253, quot97_out_ga(T251, T253)) → quot3_out_gga(s(s(s(s(s(s(s(T251))))))), s(s(s(s(s(s(s(0))))))), s(T253))
quot3_in_gga(s(s(s(s(s(s(T353)))))), s(s(s(s(s(s(0)))))), s(T355)) → U5_gga(T353, T355, quot181_in_ga(T353, T355))
quot181_in_ga(0, 0) → quot181_out_ga(0, 0)
quot181_in_ga(s(0), 0) → quot181_out_ga(s(0), 0)
quot181_in_ga(s(s(0)), 0) → quot181_out_ga(s(s(0)), 0)
quot181_in_ga(s(s(s(0))), 0) → quot181_out_ga(s(s(s(0))), 0)
quot181_in_ga(s(s(s(s(0)))), 0) → quot181_out_ga(s(s(s(s(0)))), 0)
quot181_in_ga(s(s(s(s(s(0))))), 0) → quot181_out_ga(s(s(s(s(s(0))))), 0)
quot181_in_ga(s(s(s(s(s(s(T430)))))), s(T432)) → U12_ga(T430, T432, quot181_in_ga(T430, T432))
U12_ga(T430, T432, quot181_out_ga(T430, T432)) → quot181_out_ga(s(s(s(s(s(s(T430)))))), s(T432))
U5_gga(T353, T355, quot181_out_ga(T353, T355)) → quot3_out_gga(s(s(s(s(s(s(T353)))))), s(s(s(s(s(s(0)))))), s(T355))
quot3_in_gga(s(s(s(s(s(T443))))), s(s(s(s(s(0))))), s(T445)) → U6_gga(T443, T445, quot254_in_ga(T443, T445))
quot254_in_ga(0, 0) → quot254_out_ga(0, 0)
quot254_in_ga(s(0), 0) → quot254_out_ga(s(0), 0)
quot254_in_ga(s(s(0)), 0) → quot254_out_ga(s(s(0)), 0)
quot254_in_ga(s(s(s(0))), 0) → quot254_out_ga(s(s(s(0))), 0)
quot254_in_ga(s(s(s(s(0)))), 0) → quot254_out_ga(s(s(s(s(0)))), 0)
quot254_in_ga(s(s(s(s(s(T509))))), s(T511)) → U13_ga(T509, T511, quot254_in_ga(T509, T511))
U13_ga(T509, T511, quot254_out_ga(T509, T511)) → quot254_out_ga(s(s(s(s(s(T509))))), s(T511))
U6_gga(T443, T445, quot254_out_ga(T443, T445)) → quot3_out_gga(s(s(s(s(s(T443))))), s(s(s(s(s(0))))), s(T445))
quot3_in_gga(s(s(s(s(T521)))), s(s(s(s(0)))), s(T523)) → U7_gga(T521, T523, quot316_in_ga(T521, T523))
quot316_in_ga(0, 0) → quot316_out_ga(0, 0)
quot316_in_ga(s(0), 0) → quot316_out_ga(s(0), 0)
quot316_in_ga(s(s(0)), 0) → quot316_out_ga(s(s(0)), 0)
quot316_in_ga(s(s(s(0))), 0) → quot316_out_ga(s(s(s(0))), 0)
quot316_in_ga(s(s(s(s(T576)))), s(T578)) → U14_ga(T576, T578, quot316_in_ga(T576, T578))
U14_ga(T576, T578, quot316_out_ga(T576, T578)) → quot316_out_ga(s(s(s(s(T576)))), s(T578))
U7_gga(T521, T523, quot316_out_ga(T521, T523)) → quot3_out_gga(s(s(s(s(T521)))), s(s(s(s(0)))), s(T523))
quot3_in_gga(s(s(s(T587))), s(s(s(0))), s(T589)) → U8_gga(T587, T589, quot367_in_ga(T587, T589))
quot367_in_ga(0, 0) → quot367_out_ga(0, 0)
quot367_in_ga(s(0), 0) → quot367_out_ga(s(0), 0)
quot367_in_ga(s(s(0)), 0) → quot367_out_ga(s(s(0)), 0)
quot367_in_ga(s(s(s(T631))), s(T633)) → U15_ga(T631, T633, quot367_in_ga(T631, T633))
U15_ga(T631, T633, quot367_out_ga(T631, T633)) → quot367_out_ga(s(s(s(T631))), s(T633))
U8_gga(T587, T589, quot367_out_ga(T587, T589)) → quot3_out_gga(s(s(s(T587))), s(s(s(0))), s(T589))
quot3_in_gga(s(s(T641)), s(s(0)), s(T643)) → U9_gga(T641, T643, quot407_in_ga(T641, T643))
quot407_in_ga(0, 0) → quot407_out_ga(0, 0)
quot407_in_ga(s(0), 0) → quot407_out_ga(s(0), 0)
quot407_in_ga(s(s(T674)), s(T676)) → U16_ga(T674, T676, quot407_in_ga(T674, T676))
U16_ga(T674, T676, quot407_out_ga(T674, T676)) → quot407_out_ga(s(s(T674)), s(T676))
U9_gga(T641, T643, quot407_out_ga(T641, T643)) → quot3_out_gga(s(s(T641)), s(s(0)), s(T643))
quot3_in_gga(s(T683), s(0), s(T685)) → U10_gga(T683, T685, quot436_in_ga(T683, T685))
quot436_in_ga(0, 0) → quot436_out_ga(0, 0)
quot436_in_ga(s(T705), s(T707)) → U17_ga(T705, T707, quot436_in_ga(T705, T707))
U17_ga(T705, T707, quot436_out_ga(T705, T707)) → quot436_out_ga(s(T705), s(T707))
U10_gga(T683, T685, quot436_out_ga(T683, T685)) → quot3_out_gga(s(T683), s(0), s(T685))
U2_ggga(T241, T242, T244, quot3_out_gga(T241, s(T242), T244)) → quot84_out_ggga(T241, 0, T242, s(T244))
U1_ggga(T226, T227, T228, T230, quot84_out_ggga(T226, T227, T228, T230)) → quot84_out_ggga(s(T226), s(T227), T228, T230)
U3_gga(T189, T190, T192, quot84_out_ggga(T189, T190, s(s(s(s(s(s(s(T190))))))), T192)) → quot3_out_gga(s(s(s(s(s(s(s(s(T189)))))))), s(s(s(s(s(s(s(s(T190)))))))), T192)
U18_gga(T7, T8, T10, quot3_out_gga(T7, T8, T10)) → div1_out_gga(T7, T8, T10)

The argument filtering Pi contains the following mapping:
div1_in_gga(x1, x2, x3)  =  div1_in_gga(x1, x2)
U18_gga(x1, x2, x3, x4)  =  U18_gga(x4)
quot3_in_gga(x1, x2, x3)  =  quot3_in_gga(x1, x2)
0  =  0
s(x1)  =  s(x1)
quot3_out_gga(x1, x2, x3)  =  quot3_out_gga(x3)
U3_gga(x1, x2, x3, x4)  =  U3_gga(x4)
quot84_in_ggga(x1, x2, x3, x4)  =  quot84_in_ggga(x1, x2, x3)
quot84_out_ggga(x1, x2, x3, x4)  =  quot84_out_ggga(x4)
U1_ggga(x1, x2, x3, x4, x5)  =  U1_ggga(x5)
U2_ggga(x1, x2, x3, x4)  =  U2_ggga(x4)
U4_gga(x1, x2, x3)  =  U4_gga(x3)
quot97_in_ga(x1, x2)  =  quot97_in_ga(x1)
quot97_out_ga(x1, x2)  =  quot97_out_ga(x2)
U11_ga(x1, x2, x3)  =  U11_ga(x3)
U5_gga(x1, x2, x3)  =  U5_gga(x3)
quot181_in_ga(x1, x2)  =  quot181_in_ga(x1)
quot181_out_ga(x1, x2)  =  quot181_out_ga(x2)
U12_ga(x1, x2, x3)  =  U12_ga(x3)
U6_gga(x1, x2, x3)  =  U6_gga(x3)
quot254_in_ga(x1, x2)  =  quot254_in_ga(x1)
quot254_out_ga(x1, x2)  =  quot254_out_ga(x2)
U13_ga(x1, x2, x3)  =  U13_ga(x3)
U7_gga(x1, x2, x3)  =  U7_gga(x3)
quot316_in_ga(x1, x2)  =  quot316_in_ga(x1)
quot316_out_ga(x1, x2)  =  quot316_out_ga(x2)
U14_ga(x1, x2, x3)  =  U14_ga(x3)
U8_gga(x1, x2, x3)  =  U8_gga(x3)
quot367_in_ga(x1, x2)  =  quot367_in_ga(x1)
quot367_out_ga(x1, x2)  =  quot367_out_ga(x2)
U15_ga(x1, x2, x3)  =  U15_ga(x3)
U9_gga(x1, x2, x3)  =  U9_gga(x3)
quot407_in_ga(x1, x2)  =  quot407_in_ga(x1)
quot407_out_ga(x1, x2)  =  quot407_out_ga(x2)
U16_ga(x1, x2, x3)  =  U16_ga(x3)
U10_gga(x1, x2, x3)  =  U10_gga(x3)
quot436_in_ga(x1, x2)  =  quot436_in_ga(x1)
quot436_out_ga(x1, x2)  =  quot436_out_ga(x2)
U17_ga(x1, x2, x3)  =  U17_ga(x3)
div1_out_gga(x1, x2, x3)  =  div1_out_gga(x3)
QUOT436_IN_GA(x1, x2)  =  QUOT436_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:

QUOT436_IN_GA(s(T705), s(T707)) → QUOT436_IN_GA(T705, T707)

R is empty.
The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
QUOT436_IN_GA(x1, x2)  =  QUOT436_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:

QUOT436_IN_GA(s(T705)) → QUOT436_IN_GA(T705)

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:

  • QUOT436_IN_GA(s(T705)) → QUOT436_IN_GA(T705)
    The graph contains the following edges 1 > 1

(15) YES

(16) Obligation:

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

QUOT407_IN_GA(s(s(T674)), s(T676)) → QUOT407_IN_GA(T674, T676)

The TRS R consists of the following rules:

div1_in_gga(T7, T8, T10) → U18_gga(T7, T8, T10, quot3_in_gga(T7, T8, T10))
quot3_in_gga(0, s(T15), 0) → quot3_out_gga(0, s(T15), 0)
quot3_in_gga(s(0), s(s(T38)), 0) → quot3_out_gga(s(0), s(s(T38)), 0)
quot3_in_gga(s(s(0)), s(s(s(T61))), 0) → quot3_out_gga(s(s(0)), s(s(s(T61))), 0)
quot3_in_gga(s(s(s(0))), s(s(s(s(T84)))), 0) → quot3_out_gga(s(s(s(0))), s(s(s(s(T84)))), 0)
quot3_in_gga(s(s(s(s(0)))), s(s(s(s(s(T107))))), 0) → quot3_out_gga(s(s(s(s(0)))), s(s(s(s(s(T107))))), 0)
quot3_in_gga(s(s(s(s(s(0))))), s(s(s(s(s(s(T130)))))), 0) → quot3_out_gga(s(s(s(s(s(0))))), s(s(s(s(s(s(T130)))))), 0)
quot3_in_gga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T153))))))), 0) → quot3_out_gga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T153))))))), 0)
quot3_in_gga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(T176)))))))), 0) → quot3_out_gga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(T176)))))))), 0)
quot3_in_gga(s(s(s(s(s(s(s(s(T189)))))))), s(s(s(s(s(s(s(s(T190)))))))), T192) → U3_gga(T189, T190, T192, quot84_in_ggga(T189, T190, s(s(s(s(s(s(s(T190))))))), T192))
quot84_in_ggga(0, s(T208), T209, 0) → quot84_out_ggga(0, s(T208), T209, 0)
quot84_in_ggga(s(T226), s(T227), T228, T230) → U1_ggga(T226, T227, T228, T230, quot84_in_ggga(T226, T227, T228, T230))
quot84_in_ggga(T241, 0, T242, s(T244)) → U2_ggga(T241, T242, T244, quot3_in_gga(T241, s(T242), T244))
quot3_in_gga(s(s(s(s(s(s(s(T251))))))), s(s(s(s(s(s(s(0))))))), s(T253)) → U4_gga(T251, T253, quot97_in_ga(T251, T253))
quot97_in_ga(0, 0) → quot97_out_ga(0, 0)
quot97_in_ga(s(0), 0) → quot97_out_ga(s(0), 0)
quot97_in_ga(s(s(0)), 0) → quot97_out_ga(s(s(0)), 0)
quot97_in_ga(s(s(s(0))), 0) → quot97_out_ga(s(s(s(0))), 0)
quot97_in_ga(s(s(s(s(0)))), 0) → quot97_out_ga(s(s(s(s(0)))), 0)
quot97_in_ga(s(s(s(s(s(0))))), 0) → quot97_out_ga(s(s(s(s(s(0))))), 0)
quot97_in_ga(s(s(s(s(s(s(0)))))), 0) → quot97_out_ga(s(s(s(s(s(s(0)))))), 0)
quot97_in_ga(s(s(s(s(s(s(s(T339))))))), s(T341)) → U11_ga(T339, T341, quot97_in_ga(T339, T341))
U11_ga(T339, T341, quot97_out_ga(T339, T341)) → quot97_out_ga(s(s(s(s(s(s(s(T339))))))), s(T341))
U4_gga(T251, T253, quot97_out_ga(T251, T253)) → quot3_out_gga(s(s(s(s(s(s(s(T251))))))), s(s(s(s(s(s(s(0))))))), s(T253))
quot3_in_gga(s(s(s(s(s(s(T353)))))), s(s(s(s(s(s(0)))))), s(T355)) → U5_gga(T353, T355, quot181_in_ga(T353, T355))
quot181_in_ga(0, 0) → quot181_out_ga(0, 0)
quot181_in_ga(s(0), 0) → quot181_out_ga(s(0), 0)
quot181_in_ga(s(s(0)), 0) → quot181_out_ga(s(s(0)), 0)
quot181_in_ga(s(s(s(0))), 0) → quot181_out_ga(s(s(s(0))), 0)
quot181_in_ga(s(s(s(s(0)))), 0) → quot181_out_ga(s(s(s(s(0)))), 0)
quot181_in_ga(s(s(s(s(s(0))))), 0) → quot181_out_ga(s(s(s(s(s(0))))), 0)
quot181_in_ga(s(s(s(s(s(s(T430)))))), s(T432)) → U12_ga(T430, T432, quot181_in_ga(T430, T432))
U12_ga(T430, T432, quot181_out_ga(T430, T432)) → quot181_out_ga(s(s(s(s(s(s(T430)))))), s(T432))
U5_gga(T353, T355, quot181_out_ga(T353, T355)) → quot3_out_gga(s(s(s(s(s(s(T353)))))), s(s(s(s(s(s(0)))))), s(T355))
quot3_in_gga(s(s(s(s(s(T443))))), s(s(s(s(s(0))))), s(T445)) → U6_gga(T443, T445, quot254_in_ga(T443, T445))
quot254_in_ga(0, 0) → quot254_out_ga(0, 0)
quot254_in_ga(s(0), 0) → quot254_out_ga(s(0), 0)
quot254_in_ga(s(s(0)), 0) → quot254_out_ga(s(s(0)), 0)
quot254_in_ga(s(s(s(0))), 0) → quot254_out_ga(s(s(s(0))), 0)
quot254_in_ga(s(s(s(s(0)))), 0) → quot254_out_ga(s(s(s(s(0)))), 0)
quot254_in_ga(s(s(s(s(s(T509))))), s(T511)) → U13_ga(T509, T511, quot254_in_ga(T509, T511))
U13_ga(T509, T511, quot254_out_ga(T509, T511)) → quot254_out_ga(s(s(s(s(s(T509))))), s(T511))
U6_gga(T443, T445, quot254_out_ga(T443, T445)) → quot3_out_gga(s(s(s(s(s(T443))))), s(s(s(s(s(0))))), s(T445))
quot3_in_gga(s(s(s(s(T521)))), s(s(s(s(0)))), s(T523)) → U7_gga(T521, T523, quot316_in_ga(T521, T523))
quot316_in_ga(0, 0) → quot316_out_ga(0, 0)
quot316_in_ga(s(0), 0) → quot316_out_ga(s(0), 0)
quot316_in_ga(s(s(0)), 0) → quot316_out_ga(s(s(0)), 0)
quot316_in_ga(s(s(s(0))), 0) → quot316_out_ga(s(s(s(0))), 0)
quot316_in_ga(s(s(s(s(T576)))), s(T578)) → U14_ga(T576, T578, quot316_in_ga(T576, T578))
U14_ga(T576, T578, quot316_out_ga(T576, T578)) → quot316_out_ga(s(s(s(s(T576)))), s(T578))
U7_gga(T521, T523, quot316_out_ga(T521, T523)) → quot3_out_gga(s(s(s(s(T521)))), s(s(s(s(0)))), s(T523))
quot3_in_gga(s(s(s(T587))), s(s(s(0))), s(T589)) → U8_gga(T587, T589, quot367_in_ga(T587, T589))
quot367_in_ga(0, 0) → quot367_out_ga(0, 0)
quot367_in_ga(s(0), 0) → quot367_out_ga(s(0), 0)
quot367_in_ga(s(s(0)), 0) → quot367_out_ga(s(s(0)), 0)
quot367_in_ga(s(s(s(T631))), s(T633)) → U15_ga(T631, T633, quot367_in_ga(T631, T633))
U15_ga(T631, T633, quot367_out_ga(T631, T633)) → quot367_out_ga(s(s(s(T631))), s(T633))
U8_gga(T587, T589, quot367_out_ga(T587, T589)) → quot3_out_gga(s(s(s(T587))), s(s(s(0))), s(T589))
quot3_in_gga(s(s(T641)), s(s(0)), s(T643)) → U9_gga(T641, T643, quot407_in_ga(T641, T643))
quot407_in_ga(0, 0) → quot407_out_ga(0, 0)
quot407_in_ga(s(0), 0) → quot407_out_ga(s(0), 0)
quot407_in_ga(s(s(T674)), s(T676)) → U16_ga(T674, T676, quot407_in_ga(T674, T676))
U16_ga(T674, T676, quot407_out_ga(T674, T676)) → quot407_out_ga(s(s(T674)), s(T676))
U9_gga(T641, T643, quot407_out_ga(T641, T643)) → quot3_out_gga(s(s(T641)), s(s(0)), s(T643))
quot3_in_gga(s(T683), s(0), s(T685)) → U10_gga(T683, T685, quot436_in_ga(T683, T685))
quot436_in_ga(0, 0) → quot436_out_ga(0, 0)
quot436_in_ga(s(T705), s(T707)) → U17_ga(T705, T707, quot436_in_ga(T705, T707))
U17_ga(T705, T707, quot436_out_ga(T705, T707)) → quot436_out_ga(s(T705), s(T707))
U10_gga(T683, T685, quot436_out_ga(T683, T685)) → quot3_out_gga(s(T683), s(0), s(T685))
U2_ggga(T241, T242, T244, quot3_out_gga(T241, s(T242), T244)) → quot84_out_ggga(T241, 0, T242, s(T244))
U1_ggga(T226, T227, T228, T230, quot84_out_ggga(T226, T227, T228, T230)) → quot84_out_ggga(s(T226), s(T227), T228, T230)
U3_gga(T189, T190, T192, quot84_out_ggga(T189, T190, s(s(s(s(s(s(s(T190))))))), T192)) → quot3_out_gga(s(s(s(s(s(s(s(s(T189)))))))), s(s(s(s(s(s(s(s(T190)))))))), T192)
U18_gga(T7, T8, T10, quot3_out_gga(T7, T8, T10)) → div1_out_gga(T7, T8, T10)

The argument filtering Pi contains the following mapping:
div1_in_gga(x1, x2, x3)  =  div1_in_gga(x1, x2)
U18_gga(x1, x2, x3, x4)  =  U18_gga(x4)
quot3_in_gga(x1, x2, x3)  =  quot3_in_gga(x1, x2)
0  =  0
s(x1)  =  s(x1)
quot3_out_gga(x1, x2, x3)  =  quot3_out_gga(x3)
U3_gga(x1, x2, x3, x4)  =  U3_gga(x4)
quot84_in_ggga(x1, x2, x3, x4)  =  quot84_in_ggga(x1, x2, x3)
quot84_out_ggga(x1, x2, x3, x4)  =  quot84_out_ggga(x4)
U1_ggga(x1, x2, x3, x4, x5)  =  U1_ggga(x5)
U2_ggga(x1, x2, x3, x4)  =  U2_ggga(x4)
U4_gga(x1, x2, x3)  =  U4_gga(x3)
quot97_in_ga(x1, x2)  =  quot97_in_ga(x1)
quot97_out_ga(x1, x2)  =  quot97_out_ga(x2)
U11_ga(x1, x2, x3)  =  U11_ga(x3)
U5_gga(x1, x2, x3)  =  U5_gga(x3)
quot181_in_ga(x1, x2)  =  quot181_in_ga(x1)
quot181_out_ga(x1, x2)  =  quot181_out_ga(x2)
U12_ga(x1, x2, x3)  =  U12_ga(x3)
U6_gga(x1, x2, x3)  =  U6_gga(x3)
quot254_in_ga(x1, x2)  =  quot254_in_ga(x1)
quot254_out_ga(x1, x2)  =  quot254_out_ga(x2)
U13_ga(x1, x2, x3)  =  U13_ga(x3)
U7_gga(x1, x2, x3)  =  U7_gga(x3)
quot316_in_ga(x1, x2)  =  quot316_in_ga(x1)
quot316_out_ga(x1, x2)  =  quot316_out_ga(x2)
U14_ga(x1, x2, x3)  =  U14_ga(x3)
U8_gga(x1, x2, x3)  =  U8_gga(x3)
quot367_in_ga(x1, x2)  =  quot367_in_ga(x1)
quot367_out_ga(x1, x2)  =  quot367_out_ga(x2)
U15_ga(x1, x2, x3)  =  U15_ga(x3)
U9_gga(x1, x2, x3)  =  U9_gga(x3)
quot407_in_ga(x1, x2)  =  quot407_in_ga(x1)
quot407_out_ga(x1, x2)  =  quot407_out_ga(x2)
U16_ga(x1, x2, x3)  =  U16_ga(x3)
U10_gga(x1, x2, x3)  =  U10_gga(x3)
quot436_in_ga(x1, x2)  =  quot436_in_ga(x1)
quot436_out_ga(x1, x2)  =  quot436_out_ga(x2)
U17_ga(x1, x2, x3)  =  U17_ga(x3)
div1_out_gga(x1, x2, x3)  =  div1_out_gga(x3)
QUOT407_IN_GA(x1, x2)  =  QUOT407_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:

QUOT407_IN_GA(s(s(T674)), s(T676)) → QUOT407_IN_GA(T674, T676)

R is empty.
The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
QUOT407_IN_GA(x1, x2)  =  QUOT407_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:

QUOT407_IN_GA(s(s(T674))) → QUOT407_IN_GA(T674)

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:

  • QUOT407_IN_GA(s(s(T674))) → QUOT407_IN_GA(T674)
    The graph contains the following edges 1 > 1

(22) YES

(23) Obligation:

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

QUOT367_IN_GA(s(s(s(T631))), s(T633)) → QUOT367_IN_GA(T631, T633)

The TRS R consists of the following rules:

div1_in_gga(T7, T8, T10) → U18_gga(T7, T8, T10, quot3_in_gga(T7, T8, T10))
quot3_in_gga(0, s(T15), 0) → quot3_out_gga(0, s(T15), 0)
quot3_in_gga(s(0), s(s(T38)), 0) → quot3_out_gga(s(0), s(s(T38)), 0)
quot3_in_gga(s(s(0)), s(s(s(T61))), 0) → quot3_out_gga(s(s(0)), s(s(s(T61))), 0)
quot3_in_gga(s(s(s(0))), s(s(s(s(T84)))), 0) → quot3_out_gga(s(s(s(0))), s(s(s(s(T84)))), 0)
quot3_in_gga(s(s(s(s(0)))), s(s(s(s(s(T107))))), 0) → quot3_out_gga(s(s(s(s(0)))), s(s(s(s(s(T107))))), 0)
quot3_in_gga(s(s(s(s(s(0))))), s(s(s(s(s(s(T130)))))), 0) → quot3_out_gga(s(s(s(s(s(0))))), s(s(s(s(s(s(T130)))))), 0)
quot3_in_gga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T153))))))), 0) → quot3_out_gga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T153))))))), 0)
quot3_in_gga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(T176)))))))), 0) → quot3_out_gga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(T176)))))))), 0)
quot3_in_gga(s(s(s(s(s(s(s(s(T189)))))))), s(s(s(s(s(s(s(s(T190)))))))), T192) → U3_gga(T189, T190, T192, quot84_in_ggga(T189, T190, s(s(s(s(s(s(s(T190))))))), T192))
quot84_in_ggga(0, s(T208), T209, 0) → quot84_out_ggga(0, s(T208), T209, 0)
quot84_in_ggga(s(T226), s(T227), T228, T230) → U1_ggga(T226, T227, T228, T230, quot84_in_ggga(T226, T227, T228, T230))
quot84_in_ggga(T241, 0, T242, s(T244)) → U2_ggga(T241, T242, T244, quot3_in_gga(T241, s(T242), T244))
quot3_in_gga(s(s(s(s(s(s(s(T251))))))), s(s(s(s(s(s(s(0))))))), s(T253)) → U4_gga(T251, T253, quot97_in_ga(T251, T253))
quot97_in_ga(0, 0) → quot97_out_ga(0, 0)
quot97_in_ga(s(0), 0) → quot97_out_ga(s(0), 0)
quot97_in_ga(s(s(0)), 0) → quot97_out_ga(s(s(0)), 0)
quot97_in_ga(s(s(s(0))), 0) → quot97_out_ga(s(s(s(0))), 0)
quot97_in_ga(s(s(s(s(0)))), 0) → quot97_out_ga(s(s(s(s(0)))), 0)
quot97_in_ga(s(s(s(s(s(0))))), 0) → quot97_out_ga(s(s(s(s(s(0))))), 0)
quot97_in_ga(s(s(s(s(s(s(0)))))), 0) → quot97_out_ga(s(s(s(s(s(s(0)))))), 0)
quot97_in_ga(s(s(s(s(s(s(s(T339))))))), s(T341)) → U11_ga(T339, T341, quot97_in_ga(T339, T341))
U11_ga(T339, T341, quot97_out_ga(T339, T341)) → quot97_out_ga(s(s(s(s(s(s(s(T339))))))), s(T341))
U4_gga(T251, T253, quot97_out_ga(T251, T253)) → quot3_out_gga(s(s(s(s(s(s(s(T251))))))), s(s(s(s(s(s(s(0))))))), s(T253))
quot3_in_gga(s(s(s(s(s(s(T353)))))), s(s(s(s(s(s(0)))))), s(T355)) → U5_gga(T353, T355, quot181_in_ga(T353, T355))
quot181_in_ga(0, 0) → quot181_out_ga(0, 0)
quot181_in_ga(s(0), 0) → quot181_out_ga(s(0), 0)
quot181_in_ga(s(s(0)), 0) → quot181_out_ga(s(s(0)), 0)
quot181_in_ga(s(s(s(0))), 0) → quot181_out_ga(s(s(s(0))), 0)
quot181_in_ga(s(s(s(s(0)))), 0) → quot181_out_ga(s(s(s(s(0)))), 0)
quot181_in_ga(s(s(s(s(s(0))))), 0) → quot181_out_ga(s(s(s(s(s(0))))), 0)
quot181_in_ga(s(s(s(s(s(s(T430)))))), s(T432)) → U12_ga(T430, T432, quot181_in_ga(T430, T432))
U12_ga(T430, T432, quot181_out_ga(T430, T432)) → quot181_out_ga(s(s(s(s(s(s(T430)))))), s(T432))
U5_gga(T353, T355, quot181_out_ga(T353, T355)) → quot3_out_gga(s(s(s(s(s(s(T353)))))), s(s(s(s(s(s(0)))))), s(T355))
quot3_in_gga(s(s(s(s(s(T443))))), s(s(s(s(s(0))))), s(T445)) → U6_gga(T443, T445, quot254_in_ga(T443, T445))
quot254_in_ga(0, 0) → quot254_out_ga(0, 0)
quot254_in_ga(s(0), 0) → quot254_out_ga(s(0), 0)
quot254_in_ga(s(s(0)), 0) → quot254_out_ga(s(s(0)), 0)
quot254_in_ga(s(s(s(0))), 0) → quot254_out_ga(s(s(s(0))), 0)
quot254_in_ga(s(s(s(s(0)))), 0) → quot254_out_ga(s(s(s(s(0)))), 0)
quot254_in_ga(s(s(s(s(s(T509))))), s(T511)) → U13_ga(T509, T511, quot254_in_ga(T509, T511))
U13_ga(T509, T511, quot254_out_ga(T509, T511)) → quot254_out_ga(s(s(s(s(s(T509))))), s(T511))
U6_gga(T443, T445, quot254_out_ga(T443, T445)) → quot3_out_gga(s(s(s(s(s(T443))))), s(s(s(s(s(0))))), s(T445))
quot3_in_gga(s(s(s(s(T521)))), s(s(s(s(0)))), s(T523)) → U7_gga(T521, T523, quot316_in_ga(T521, T523))
quot316_in_ga(0, 0) → quot316_out_ga(0, 0)
quot316_in_ga(s(0), 0) → quot316_out_ga(s(0), 0)
quot316_in_ga(s(s(0)), 0) → quot316_out_ga(s(s(0)), 0)
quot316_in_ga(s(s(s(0))), 0) → quot316_out_ga(s(s(s(0))), 0)
quot316_in_ga(s(s(s(s(T576)))), s(T578)) → U14_ga(T576, T578, quot316_in_ga(T576, T578))
U14_ga(T576, T578, quot316_out_ga(T576, T578)) → quot316_out_ga(s(s(s(s(T576)))), s(T578))
U7_gga(T521, T523, quot316_out_ga(T521, T523)) → quot3_out_gga(s(s(s(s(T521)))), s(s(s(s(0)))), s(T523))
quot3_in_gga(s(s(s(T587))), s(s(s(0))), s(T589)) → U8_gga(T587, T589, quot367_in_ga(T587, T589))
quot367_in_ga(0, 0) → quot367_out_ga(0, 0)
quot367_in_ga(s(0), 0) → quot367_out_ga(s(0), 0)
quot367_in_ga(s(s(0)), 0) → quot367_out_ga(s(s(0)), 0)
quot367_in_ga(s(s(s(T631))), s(T633)) → U15_ga(T631, T633, quot367_in_ga(T631, T633))
U15_ga(T631, T633, quot367_out_ga(T631, T633)) → quot367_out_ga(s(s(s(T631))), s(T633))
U8_gga(T587, T589, quot367_out_ga(T587, T589)) → quot3_out_gga(s(s(s(T587))), s(s(s(0))), s(T589))
quot3_in_gga(s(s(T641)), s(s(0)), s(T643)) → U9_gga(T641, T643, quot407_in_ga(T641, T643))
quot407_in_ga(0, 0) → quot407_out_ga(0, 0)
quot407_in_ga(s(0), 0) → quot407_out_ga(s(0), 0)
quot407_in_ga(s(s(T674)), s(T676)) → U16_ga(T674, T676, quot407_in_ga(T674, T676))
U16_ga(T674, T676, quot407_out_ga(T674, T676)) → quot407_out_ga(s(s(T674)), s(T676))
U9_gga(T641, T643, quot407_out_ga(T641, T643)) → quot3_out_gga(s(s(T641)), s(s(0)), s(T643))
quot3_in_gga(s(T683), s(0), s(T685)) → U10_gga(T683, T685, quot436_in_ga(T683, T685))
quot436_in_ga(0, 0) → quot436_out_ga(0, 0)
quot436_in_ga(s(T705), s(T707)) → U17_ga(T705, T707, quot436_in_ga(T705, T707))
U17_ga(T705, T707, quot436_out_ga(T705, T707)) → quot436_out_ga(s(T705), s(T707))
U10_gga(T683, T685, quot436_out_ga(T683, T685)) → quot3_out_gga(s(T683), s(0), s(T685))
U2_ggga(T241, T242, T244, quot3_out_gga(T241, s(T242), T244)) → quot84_out_ggga(T241, 0, T242, s(T244))
U1_ggga(T226, T227, T228, T230, quot84_out_ggga(T226, T227, T228, T230)) → quot84_out_ggga(s(T226), s(T227), T228, T230)
U3_gga(T189, T190, T192, quot84_out_ggga(T189, T190, s(s(s(s(s(s(s(T190))))))), T192)) → quot3_out_gga(s(s(s(s(s(s(s(s(T189)))))))), s(s(s(s(s(s(s(s(T190)))))))), T192)
U18_gga(T7, T8, T10, quot3_out_gga(T7, T8, T10)) → div1_out_gga(T7, T8, T10)

The argument filtering Pi contains the following mapping:
div1_in_gga(x1, x2, x3)  =  div1_in_gga(x1, x2)
U18_gga(x1, x2, x3, x4)  =  U18_gga(x4)
quot3_in_gga(x1, x2, x3)  =  quot3_in_gga(x1, x2)
0  =  0
s(x1)  =  s(x1)
quot3_out_gga(x1, x2, x3)  =  quot3_out_gga(x3)
U3_gga(x1, x2, x3, x4)  =  U3_gga(x4)
quot84_in_ggga(x1, x2, x3, x4)  =  quot84_in_ggga(x1, x2, x3)
quot84_out_ggga(x1, x2, x3, x4)  =  quot84_out_ggga(x4)
U1_ggga(x1, x2, x3, x4, x5)  =  U1_ggga(x5)
U2_ggga(x1, x2, x3, x4)  =  U2_ggga(x4)
U4_gga(x1, x2, x3)  =  U4_gga(x3)
quot97_in_ga(x1, x2)  =  quot97_in_ga(x1)
quot97_out_ga(x1, x2)  =  quot97_out_ga(x2)
U11_ga(x1, x2, x3)  =  U11_ga(x3)
U5_gga(x1, x2, x3)  =  U5_gga(x3)
quot181_in_ga(x1, x2)  =  quot181_in_ga(x1)
quot181_out_ga(x1, x2)  =  quot181_out_ga(x2)
U12_ga(x1, x2, x3)  =  U12_ga(x3)
U6_gga(x1, x2, x3)  =  U6_gga(x3)
quot254_in_ga(x1, x2)  =  quot254_in_ga(x1)
quot254_out_ga(x1, x2)  =  quot254_out_ga(x2)
U13_ga(x1, x2, x3)  =  U13_ga(x3)
U7_gga(x1, x2, x3)  =  U7_gga(x3)
quot316_in_ga(x1, x2)  =  quot316_in_ga(x1)
quot316_out_ga(x1, x2)  =  quot316_out_ga(x2)
U14_ga(x1, x2, x3)  =  U14_ga(x3)
U8_gga(x1, x2, x3)  =  U8_gga(x3)
quot367_in_ga(x1, x2)  =  quot367_in_ga(x1)
quot367_out_ga(x1, x2)  =  quot367_out_ga(x2)
U15_ga(x1, x2, x3)  =  U15_ga(x3)
U9_gga(x1, x2, x3)  =  U9_gga(x3)
quot407_in_ga(x1, x2)  =  quot407_in_ga(x1)
quot407_out_ga(x1, x2)  =  quot407_out_ga(x2)
U16_ga(x1, x2, x3)  =  U16_ga(x3)
U10_gga(x1, x2, x3)  =  U10_gga(x3)
quot436_in_ga(x1, x2)  =  quot436_in_ga(x1)
quot436_out_ga(x1, x2)  =  quot436_out_ga(x2)
U17_ga(x1, x2, x3)  =  U17_ga(x3)
div1_out_gga(x1, x2, x3)  =  div1_out_gga(x3)
QUOT367_IN_GA(x1, x2)  =  QUOT367_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:

QUOT367_IN_GA(s(s(s(T631))), s(T633)) → QUOT367_IN_GA(T631, T633)

R is empty.
The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
QUOT367_IN_GA(x1, x2)  =  QUOT367_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:

QUOT367_IN_GA(s(s(s(T631)))) → QUOT367_IN_GA(T631)

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:

  • QUOT367_IN_GA(s(s(s(T631)))) → QUOT367_IN_GA(T631)
    The graph contains the following edges 1 > 1

(29) YES

(30) Obligation:

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

QUOT316_IN_GA(s(s(s(s(T576)))), s(T578)) → QUOT316_IN_GA(T576, T578)

The TRS R consists of the following rules:

div1_in_gga(T7, T8, T10) → U18_gga(T7, T8, T10, quot3_in_gga(T7, T8, T10))
quot3_in_gga(0, s(T15), 0) → quot3_out_gga(0, s(T15), 0)
quot3_in_gga(s(0), s(s(T38)), 0) → quot3_out_gga(s(0), s(s(T38)), 0)
quot3_in_gga(s(s(0)), s(s(s(T61))), 0) → quot3_out_gga(s(s(0)), s(s(s(T61))), 0)
quot3_in_gga(s(s(s(0))), s(s(s(s(T84)))), 0) → quot3_out_gga(s(s(s(0))), s(s(s(s(T84)))), 0)
quot3_in_gga(s(s(s(s(0)))), s(s(s(s(s(T107))))), 0) → quot3_out_gga(s(s(s(s(0)))), s(s(s(s(s(T107))))), 0)
quot3_in_gga(s(s(s(s(s(0))))), s(s(s(s(s(s(T130)))))), 0) → quot3_out_gga(s(s(s(s(s(0))))), s(s(s(s(s(s(T130)))))), 0)
quot3_in_gga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T153))))))), 0) → quot3_out_gga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T153))))))), 0)
quot3_in_gga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(T176)))))))), 0) → quot3_out_gga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(T176)))))))), 0)
quot3_in_gga(s(s(s(s(s(s(s(s(T189)))))))), s(s(s(s(s(s(s(s(T190)))))))), T192) → U3_gga(T189, T190, T192, quot84_in_ggga(T189, T190, s(s(s(s(s(s(s(T190))))))), T192))
quot84_in_ggga(0, s(T208), T209, 0) → quot84_out_ggga(0, s(T208), T209, 0)
quot84_in_ggga(s(T226), s(T227), T228, T230) → U1_ggga(T226, T227, T228, T230, quot84_in_ggga(T226, T227, T228, T230))
quot84_in_ggga(T241, 0, T242, s(T244)) → U2_ggga(T241, T242, T244, quot3_in_gga(T241, s(T242), T244))
quot3_in_gga(s(s(s(s(s(s(s(T251))))))), s(s(s(s(s(s(s(0))))))), s(T253)) → U4_gga(T251, T253, quot97_in_ga(T251, T253))
quot97_in_ga(0, 0) → quot97_out_ga(0, 0)
quot97_in_ga(s(0), 0) → quot97_out_ga(s(0), 0)
quot97_in_ga(s(s(0)), 0) → quot97_out_ga(s(s(0)), 0)
quot97_in_ga(s(s(s(0))), 0) → quot97_out_ga(s(s(s(0))), 0)
quot97_in_ga(s(s(s(s(0)))), 0) → quot97_out_ga(s(s(s(s(0)))), 0)
quot97_in_ga(s(s(s(s(s(0))))), 0) → quot97_out_ga(s(s(s(s(s(0))))), 0)
quot97_in_ga(s(s(s(s(s(s(0)))))), 0) → quot97_out_ga(s(s(s(s(s(s(0)))))), 0)
quot97_in_ga(s(s(s(s(s(s(s(T339))))))), s(T341)) → U11_ga(T339, T341, quot97_in_ga(T339, T341))
U11_ga(T339, T341, quot97_out_ga(T339, T341)) → quot97_out_ga(s(s(s(s(s(s(s(T339))))))), s(T341))
U4_gga(T251, T253, quot97_out_ga(T251, T253)) → quot3_out_gga(s(s(s(s(s(s(s(T251))))))), s(s(s(s(s(s(s(0))))))), s(T253))
quot3_in_gga(s(s(s(s(s(s(T353)))))), s(s(s(s(s(s(0)))))), s(T355)) → U5_gga(T353, T355, quot181_in_ga(T353, T355))
quot181_in_ga(0, 0) → quot181_out_ga(0, 0)
quot181_in_ga(s(0), 0) → quot181_out_ga(s(0), 0)
quot181_in_ga(s(s(0)), 0) → quot181_out_ga(s(s(0)), 0)
quot181_in_ga(s(s(s(0))), 0) → quot181_out_ga(s(s(s(0))), 0)
quot181_in_ga(s(s(s(s(0)))), 0) → quot181_out_ga(s(s(s(s(0)))), 0)
quot181_in_ga(s(s(s(s(s(0))))), 0) → quot181_out_ga(s(s(s(s(s(0))))), 0)
quot181_in_ga(s(s(s(s(s(s(T430)))))), s(T432)) → U12_ga(T430, T432, quot181_in_ga(T430, T432))
U12_ga(T430, T432, quot181_out_ga(T430, T432)) → quot181_out_ga(s(s(s(s(s(s(T430)))))), s(T432))
U5_gga(T353, T355, quot181_out_ga(T353, T355)) → quot3_out_gga(s(s(s(s(s(s(T353)))))), s(s(s(s(s(s(0)))))), s(T355))
quot3_in_gga(s(s(s(s(s(T443))))), s(s(s(s(s(0))))), s(T445)) → U6_gga(T443, T445, quot254_in_ga(T443, T445))
quot254_in_ga(0, 0) → quot254_out_ga(0, 0)
quot254_in_ga(s(0), 0) → quot254_out_ga(s(0), 0)
quot254_in_ga(s(s(0)), 0) → quot254_out_ga(s(s(0)), 0)
quot254_in_ga(s(s(s(0))), 0) → quot254_out_ga(s(s(s(0))), 0)
quot254_in_ga(s(s(s(s(0)))), 0) → quot254_out_ga(s(s(s(s(0)))), 0)
quot254_in_ga(s(s(s(s(s(T509))))), s(T511)) → U13_ga(T509, T511, quot254_in_ga(T509, T511))
U13_ga(T509, T511, quot254_out_ga(T509, T511)) → quot254_out_ga(s(s(s(s(s(T509))))), s(T511))
U6_gga(T443, T445, quot254_out_ga(T443, T445)) → quot3_out_gga(s(s(s(s(s(T443))))), s(s(s(s(s(0))))), s(T445))
quot3_in_gga(s(s(s(s(T521)))), s(s(s(s(0)))), s(T523)) → U7_gga(T521, T523, quot316_in_ga(T521, T523))
quot316_in_ga(0, 0) → quot316_out_ga(0, 0)
quot316_in_ga(s(0), 0) → quot316_out_ga(s(0), 0)
quot316_in_ga(s(s(0)), 0) → quot316_out_ga(s(s(0)), 0)
quot316_in_ga(s(s(s(0))), 0) → quot316_out_ga(s(s(s(0))), 0)
quot316_in_ga(s(s(s(s(T576)))), s(T578)) → U14_ga(T576, T578, quot316_in_ga(T576, T578))
U14_ga(T576, T578, quot316_out_ga(T576, T578)) → quot316_out_ga(s(s(s(s(T576)))), s(T578))
U7_gga(T521, T523, quot316_out_ga(T521, T523)) → quot3_out_gga(s(s(s(s(T521)))), s(s(s(s(0)))), s(T523))
quot3_in_gga(s(s(s(T587))), s(s(s(0))), s(T589)) → U8_gga(T587, T589, quot367_in_ga(T587, T589))
quot367_in_ga(0, 0) → quot367_out_ga(0, 0)
quot367_in_ga(s(0), 0) → quot367_out_ga(s(0), 0)
quot367_in_ga(s(s(0)), 0) → quot367_out_ga(s(s(0)), 0)
quot367_in_ga(s(s(s(T631))), s(T633)) → U15_ga(T631, T633, quot367_in_ga(T631, T633))
U15_ga(T631, T633, quot367_out_ga(T631, T633)) → quot367_out_ga(s(s(s(T631))), s(T633))
U8_gga(T587, T589, quot367_out_ga(T587, T589)) → quot3_out_gga(s(s(s(T587))), s(s(s(0))), s(T589))
quot3_in_gga(s(s(T641)), s(s(0)), s(T643)) → U9_gga(T641, T643, quot407_in_ga(T641, T643))
quot407_in_ga(0, 0) → quot407_out_ga(0, 0)
quot407_in_ga(s(0), 0) → quot407_out_ga(s(0), 0)
quot407_in_ga(s(s(T674)), s(T676)) → U16_ga(T674, T676, quot407_in_ga(T674, T676))
U16_ga(T674, T676, quot407_out_ga(T674, T676)) → quot407_out_ga(s(s(T674)), s(T676))
U9_gga(T641, T643, quot407_out_ga(T641, T643)) → quot3_out_gga(s(s(T641)), s(s(0)), s(T643))
quot3_in_gga(s(T683), s(0), s(T685)) → U10_gga(T683, T685, quot436_in_ga(T683, T685))
quot436_in_ga(0, 0) → quot436_out_ga(0, 0)
quot436_in_ga(s(T705), s(T707)) → U17_ga(T705, T707, quot436_in_ga(T705, T707))
U17_ga(T705, T707, quot436_out_ga(T705, T707)) → quot436_out_ga(s(T705), s(T707))
U10_gga(T683, T685, quot436_out_ga(T683, T685)) → quot3_out_gga(s(T683), s(0), s(T685))
U2_ggga(T241, T242, T244, quot3_out_gga(T241, s(T242), T244)) → quot84_out_ggga(T241, 0, T242, s(T244))
U1_ggga(T226, T227, T228, T230, quot84_out_ggga(T226, T227, T228, T230)) → quot84_out_ggga(s(T226), s(T227), T228, T230)
U3_gga(T189, T190, T192, quot84_out_ggga(T189, T190, s(s(s(s(s(s(s(T190))))))), T192)) → quot3_out_gga(s(s(s(s(s(s(s(s(T189)))))))), s(s(s(s(s(s(s(s(T190)))))))), T192)
U18_gga(T7, T8, T10, quot3_out_gga(T7, T8, T10)) → div1_out_gga(T7, T8, T10)

The argument filtering Pi contains the following mapping:
div1_in_gga(x1, x2, x3)  =  div1_in_gga(x1, x2)
U18_gga(x1, x2, x3, x4)  =  U18_gga(x4)
quot3_in_gga(x1, x2, x3)  =  quot3_in_gga(x1, x2)
0  =  0
s(x1)  =  s(x1)
quot3_out_gga(x1, x2, x3)  =  quot3_out_gga(x3)
U3_gga(x1, x2, x3, x4)  =  U3_gga(x4)
quot84_in_ggga(x1, x2, x3, x4)  =  quot84_in_ggga(x1, x2, x3)
quot84_out_ggga(x1, x2, x3, x4)  =  quot84_out_ggga(x4)
U1_ggga(x1, x2, x3, x4, x5)  =  U1_ggga(x5)
U2_ggga(x1, x2, x3, x4)  =  U2_ggga(x4)
U4_gga(x1, x2, x3)  =  U4_gga(x3)
quot97_in_ga(x1, x2)  =  quot97_in_ga(x1)
quot97_out_ga(x1, x2)  =  quot97_out_ga(x2)
U11_ga(x1, x2, x3)  =  U11_ga(x3)
U5_gga(x1, x2, x3)  =  U5_gga(x3)
quot181_in_ga(x1, x2)  =  quot181_in_ga(x1)
quot181_out_ga(x1, x2)  =  quot181_out_ga(x2)
U12_ga(x1, x2, x3)  =  U12_ga(x3)
U6_gga(x1, x2, x3)  =  U6_gga(x3)
quot254_in_ga(x1, x2)  =  quot254_in_ga(x1)
quot254_out_ga(x1, x2)  =  quot254_out_ga(x2)
U13_ga(x1, x2, x3)  =  U13_ga(x3)
U7_gga(x1, x2, x3)  =  U7_gga(x3)
quot316_in_ga(x1, x2)  =  quot316_in_ga(x1)
quot316_out_ga(x1, x2)  =  quot316_out_ga(x2)
U14_ga(x1, x2, x3)  =  U14_ga(x3)
U8_gga(x1, x2, x3)  =  U8_gga(x3)
quot367_in_ga(x1, x2)  =  quot367_in_ga(x1)
quot367_out_ga(x1, x2)  =  quot367_out_ga(x2)
U15_ga(x1, x2, x3)  =  U15_ga(x3)
U9_gga(x1, x2, x3)  =  U9_gga(x3)
quot407_in_ga(x1, x2)  =  quot407_in_ga(x1)
quot407_out_ga(x1, x2)  =  quot407_out_ga(x2)
U16_ga(x1, x2, x3)  =  U16_ga(x3)
U10_gga(x1, x2, x3)  =  U10_gga(x3)
quot436_in_ga(x1, x2)  =  quot436_in_ga(x1)
quot436_out_ga(x1, x2)  =  quot436_out_ga(x2)
U17_ga(x1, x2, x3)  =  U17_ga(x3)
div1_out_gga(x1, x2, x3)  =  div1_out_gga(x3)
QUOT316_IN_GA(x1, x2)  =  QUOT316_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:

QUOT316_IN_GA(s(s(s(s(T576)))), s(T578)) → QUOT316_IN_GA(T576, T578)

R is empty.
The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
QUOT316_IN_GA(x1, x2)  =  QUOT316_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:

QUOT316_IN_GA(s(s(s(s(T576))))) → QUOT316_IN_GA(T576)

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:

  • QUOT316_IN_GA(s(s(s(s(T576))))) → QUOT316_IN_GA(T576)
    The graph contains the following edges 1 > 1

(36) YES

(37) Obligation:

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

QUOT254_IN_GA(s(s(s(s(s(T509))))), s(T511)) → QUOT254_IN_GA(T509, T511)

The TRS R consists of the following rules:

div1_in_gga(T7, T8, T10) → U18_gga(T7, T8, T10, quot3_in_gga(T7, T8, T10))
quot3_in_gga(0, s(T15), 0) → quot3_out_gga(0, s(T15), 0)
quot3_in_gga(s(0), s(s(T38)), 0) → quot3_out_gga(s(0), s(s(T38)), 0)
quot3_in_gga(s(s(0)), s(s(s(T61))), 0) → quot3_out_gga(s(s(0)), s(s(s(T61))), 0)
quot3_in_gga(s(s(s(0))), s(s(s(s(T84)))), 0) → quot3_out_gga(s(s(s(0))), s(s(s(s(T84)))), 0)
quot3_in_gga(s(s(s(s(0)))), s(s(s(s(s(T107))))), 0) → quot3_out_gga(s(s(s(s(0)))), s(s(s(s(s(T107))))), 0)
quot3_in_gga(s(s(s(s(s(0))))), s(s(s(s(s(s(T130)))))), 0) → quot3_out_gga(s(s(s(s(s(0))))), s(s(s(s(s(s(T130)))))), 0)
quot3_in_gga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T153))))))), 0) → quot3_out_gga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T153))))))), 0)
quot3_in_gga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(T176)))))))), 0) → quot3_out_gga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(T176)))))))), 0)
quot3_in_gga(s(s(s(s(s(s(s(s(T189)))))))), s(s(s(s(s(s(s(s(T190)))))))), T192) → U3_gga(T189, T190, T192, quot84_in_ggga(T189, T190, s(s(s(s(s(s(s(T190))))))), T192))
quot84_in_ggga(0, s(T208), T209, 0) → quot84_out_ggga(0, s(T208), T209, 0)
quot84_in_ggga(s(T226), s(T227), T228, T230) → U1_ggga(T226, T227, T228, T230, quot84_in_ggga(T226, T227, T228, T230))
quot84_in_ggga(T241, 0, T242, s(T244)) → U2_ggga(T241, T242, T244, quot3_in_gga(T241, s(T242), T244))
quot3_in_gga(s(s(s(s(s(s(s(T251))))))), s(s(s(s(s(s(s(0))))))), s(T253)) → U4_gga(T251, T253, quot97_in_ga(T251, T253))
quot97_in_ga(0, 0) → quot97_out_ga(0, 0)
quot97_in_ga(s(0), 0) → quot97_out_ga(s(0), 0)
quot97_in_ga(s(s(0)), 0) → quot97_out_ga(s(s(0)), 0)
quot97_in_ga(s(s(s(0))), 0) → quot97_out_ga(s(s(s(0))), 0)
quot97_in_ga(s(s(s(s(0)))), 0) → quot97_out_ga(s(s(s(s(0)))), 0)
quot97_in_ga(s(s(s(s(s(0))))), 0) → quot97_out_ga(s(s(s(s(s(0))))), 0)
quot97_in_ga(s(s(s(s(s(s(0)))))), 0) → quot97_out_ga(s(s(s(s(s(s(0)))))), 0)
quot97_in_ga(s(s(s(s(s(s(s(T339))))))), s(T341)) → U11_ga(T339, T341, quot97_in_ga(T339, T341))
U11_ga(T339, T341, quot97_out_ga(T339, T341)) → quot97_out_ga(s(s(s(s(s(s(s(T339))))))), s(T341))
U4_gga(T251, T253, quot97_out_ga(T251, T253)) → quot3_out_gga(s(s(s(s(s(s(s(T251))))))), s(s(s(s(s(s(s(0))))))), s(T253))
quot3_in_gga(s(s(s(s(s(s(T353)))))), s(s(s(s(s(s(0)))))), s(T355)) → U5_gga(T353, T355, quot181_in_ga(T353, T355))
quot181_in_ga(0, 0) → quot181_out_ga(0, 0)
quot181_in_ga(s(0), 0) → quot181_out_ga(s(0), 0)
quot181_in_ga(s(s(0)), 0) → quot181_out_ga(s(s(0)), 0)
quot181_in_ga(s(s(s(0))), 0) → quot181_out_ga(s(s(s(0))), 0)
quot181_in_ga(s(s(s(s(0)))), 0) → quot181_out_ga(s(s(s(s(0)))), 0)
quot181_in_ga(s(s(s(s(s(0))))), 0) → quot181_out_ga(s(s(s(s(s(0))))), 0)
quot181_in_ga(s(s(s(s(s(s(T430)))))), s(T432)) → U12_ga(T430, T432, quot181_in_ga(T430, T432))
U12_ga(T430, T432, quot181_out_ga(T430, T432)) → quot181_out_ga(s(s(s(s(s(s(T430)))))), s(T432))
U5_gga(T353, T355, quot181_out_ga(T353, T355)) → quot3_out_gga(s(s(s(s(s(s(T353)))))), s(s(s(s(s(s(0)))))), s(T355))
quot3_in_gga(s(s(s(s(s(T443))))), s(s(s(s(s(0))))), s(T445)) → U6_gga(T443, T445, quot254_in_ga(T443, T445))
quot254_in_ga(0, 0) → quot254_out_ga(0, 0)
quot254_in_ga(s(0), 0) → quot254_out_ga(s(0), 0)
quot254_in_ga(s(s(0)), 0) → quot254_out_ga(s(s(0)), 0)
quot254_in_ga(s(s(s(0))), 0) → quot254_out_ga(s(s(s(0))), 0)
quot254_in_ga(s(s(s(s(0)))), 0) → quot254_out_ga(s(s(s(s(0)))), 0)
quot254_in_ga(s(s(s(s(s(T509))))), s(T511)) → U13_ga(T509, T511, quot254_in_ga(T509, T511))
U13_ga(T509, T511, quot254_out_ga(T509, T511)) → quot254_out_ga(s(s(s(s(s(T509))))), s(T511))
U6_gga(T443, T445, quot254_out_ga(T443, T445)) → quot3_out_gga(s(s(s(s(s(T443))))), s(s(s(s(s(0))))), s(T445))
quot3_in_gga(s(s(s(s(T521)))), s(s(s(s(0)))), s(T523)) → U7_gga(T521, T523, quot316_in_ga(T521, T523))
quot316_in_ga(0, 0) → quot316_out_ga(0, 0)
quot316_in_ga(s(0), 0) → quot316_out_ga(s(0), 0)
quot316_in_ga(s(s(0)), 0) → quot316_out_ga(s(s(0)), 0)
quot316_in_ga(s(s(s(0))), 0) → quot316_out_ga(s(s(s(0))), 0)
quot316_in_ga(s(s(s(s(T576)))), s(T578)) → U14_ga(T576, T578, quot316_in_ga(T576, T578))
U14_ga(T576, T578, quot316_out_ga(T576, T578)) → quot316_out_ga(s(s(s(s(T576)))), s(T578))
U7_gga(T521, T523, quot316_out_ga(T521, T523)) → quot3_out_gga(s(s(s(s(T521)))), s(s(s(s(0)))), s(T523))
quot3_in_gga(s(s(s(T587))), s(s(s(0))), s(T589)) → U8_gga(T587, T589, quot367_in_ga(T587, T589))
quot367_in_ga(0, 0) → quot367_out_ga(0, 0)
quot367_in_ga(s(0), 0) → quot367_out_ga(s(0), 0)
quot367_in_ga(s(s(0)), 0) → quot367_out_ga(s(s(0)), 0)
quot367_in_ga(s(s(s(T631))), s(T633)) → U15_ga(T631, T633, quot367_in_ga(T631, T633))
U15_ga(T631, T633, quot367_out_ga(T631, T633)) → quot367_out_ga(s(s(s(T631))), s(T633))
U8_gga(T587, T589, quot367_out_ga(T587, T589)) → quot3_out_gga(s(s(s(T587))), s(s(s(0))), s(T589))
quot3_in_gga(s(s(T641)), s(s(0)), s(T643)) → U9_gga(T641, T643, quot407_in_ga(T641, T643))
quot407_in_ga(0, 0) → quot407_out_ga(0, 0)
quot407_in_ga(s(0), 0) → quot407_out_ga(s(0), 0)
quot407_in_ga(s(s(T674)), s(T676)) → U16_ga(T674, T676, quot407_in_ga(T674, T676))
U16_ga(T674, T676, quot407_out_ga(T674, T676)) → quot407_out_ga(s(s(T674)), s(T676))
U9_gga(T641, T643, quot407_out_ga(T641, T643)) → quot3_out_gga(s(s(T641)), s(s(0)), s(T643))
quot3_in_gga(s(T683), s(0), s(T685)) → U10_gga(T683, T685, quot436_in_ga(T683, T685))
quot436_in_ga(0, 0) → quot436_out_ga(0, 0)
quot436_in_ga(s(T705), s(T707)) → U17_ga(T705, T707, quot436_in_ga(T705, T707))
U17_ga(T705, T707, quot436_out_ga(T705, T707)) → quot436_out_ga(s(T705), s(T707))
U10_gga(T683, T685, quot436_out_ga(T683, T685)) → quot3_out_gga(s(T683), s(0), s(T685))
U2_ggga(T241, T242, T244, quot3_out_gga(T241, s(T242), T244)) → quot84_out_ggga(T241, 0, T242, s(T244))
U1_ggga(T226, T227, T228, T230, quot84_out_ggga(T226, T227, T228, T230)) → quot84_out_ggga(s(T226), s(T227), T228, T230)
U3_gga(T189, T190, T192, quot84_out_ggga(T189, T190, s(s(s(s(s(s(s(T190))))))), T192)) → quot3_out_gga(s(s(s(s(s(s(s(s(T189)))))))), s(s(s(s(s(s(s(s(T190)))))))), T192)
U18_gga(T7, T8, T10, quot3_out_gga(T7, T8, T10)) → div1_out_gga(T7, T8, T10)

The argument filtering Pi contains the following mapping:
div1_in_gga(x1, x2, x3)  =  div1_in_gga(x1, x2)
U18_gga(x1, x2, x3, x4)  =  U18_gga(x4)
quot3_in_gga(x1, x2, x3)  =  quot3_in_gga(x1, x2)
0  =  0
s(x1)  =  s(x1)
quot3_out_gga(x1, x2, x3)  =  quot3_out_gga(x3)
U3_gga(x1, x2, x3, x4)  =  U3_gga(x4)
quot84_in_ggga(x1, x2, x3, x4)  =  quot84_in_ggga(x1, x2, x3)
quot84_out_ggga(x1, x2, x3, x4)  =  quot84_out_ggga(x4)
U1_ggga(x1, x2, x3, x4, x5)  =  U1_ggga(x5)
U2_ggga(x1, x2, x3, x4)  =  U2_ggga(x4)
U4_gga(x1, x2, x3)  =  U4_gga(x3)
quot97_in_ga(x1, x2)  =  quot97_in_ga(x1)
quot97_out_ga(x1, x2)  =  quot97_out_ga(x2)
U11_ga(x1, x2, x3)  =  U11_ga(x3)
U5_gga(x1, x2, x3)  =  U5_gga(x3)
quot181_in_ga(x1, x2)  =  quot181_in_ga(x1)
quot181_out_ga(x1, x2)  =  quot181_out_ga(x2)
U12_ga(x1, x2, x3)  =  U12_ga(x3)
U6_gga(x1, x2, x3)  =  U6_gga(x3)
quot254_in_ga(x1, x2)  =  quot254_in_ga(x1)
quot254_out_ga(x1, x2)  =  quot254_out_ga(x2)
U13_ga(x1, x2, x3)  =  U13_ga(x3)
U7_gga(x1, x2, x3)  =  U7_gga(x3)
quot316_in_ga(x1, x2)  =  quot316_in_ga(x1)
quot316_out_ga(x1, x2)  =  quot316_out_ga(x2)
U14_ga(x1, x2, x3)  =  U14_ga(x3)
U8_gga(x1, x2, x3)  =  U8_gga(x3)
quot367_in_ga(x1, x2)  =  quot367_in_ga(x1)
quot367_out_ga(x1, x2)  =  quot367_out_ga(x2)
U15_ga(x1, x2, x3)  =  U15_ga(x3)
U9_gga(x1, x2, x3)  =  U9_gga(x3)
quot407_in_ga(x1, x2)  =  quot407_in_ga(x1)
quot407_out_ga(x1, x2)  =  quot407_out_ga(x2)
U16_ga(x1, x2, x3)  =  U16_ga(x3)
U10_gga(x1, x2, x3)  =  U10_gga(x3)
quot436_in_ga(x1, x2)  =  quot436_in_ga(x1)
quot436_out_ga(x1, x2)  =  quot436_out_ga(x2)
U17_ga(x1, x2, x3)  =  U17_ga(x3)
div1_out_gga(x1, x2, x3)  =  div1_out_gga(x3)
QUOT254_IN_GA(x1, x2)  =  QUOT254_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:

QUOT254_IN_GA(s(s(s(s(s(T509))))), s(T511)) → QUOT254_IN_GA(T509, T511)

R is empty.
The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
QUOT254_IN_GA(x1, x2)  =  QUOT254_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:

QUOT254_IN_GA(s(s(s(s(s(T509)))))) → QUOT254_IN_GA(T509)

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:

  • QUOT254_IN_GA(s(s(s(s(s(T509)))))) → QUOT254_IN_GA(T509)
    The graph contains the following edges 1 > 1

(43) YES

(44) Obligation:

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

QUOT181_IN_GA(s(s(s(s(s(s(T430)))))), s(T432)) → QUOT181_IN_GA(T430, T432)

The TRS R consists of the following rules:

div1_in_gga(T7, T8, T10) → U18_gga(T7, T8, T10, quot3_in_gga(T7, T8, T10))
quot3_in_gga(0, s(T15), 0) → quot3_out_gga(0, s(T15), 0)
quot3_in_gga(s(0), s(s(T38)), 0) → quot3_out_gga(s(0), s(s(T38)), 0)
quot3_in_gga(s(s(0)), s(s(s(T61))), 0) → quot3_out_gga(s(s(0)), s(s(s(T61))), 0)
quot3_in_gga(s(s(s(0))), s(s(s(s(T84)))), 0) → quot3_out_gga(s(s(s(0))), s(s(s(s(T84)))), 0)
quot3_in_gga(s(s(s(s(0)))), s(s(s(s(s(T107))))), 0) → quot3_out_gga(s(s(s(s(0)))), s(s(s(s(s(T107))))), 0)
quot3_in_gga(s(s(s(s(s(0))))), s(s(s(s(s(s(T130)))))), 0) → quot3_out_gga(s(s(s(s(s(0))))), s(s(s(s(s(s(T130)))))), 0)
quot3_in_gga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T153))))))), 0) → quot3_out_gga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T153))))))), 0)
quot3_in_gga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(T176)))))))), 0) → quot3_out_gga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(T176)))))))), 0)
quot3_in_gga(s(s(s(s(s(s(s(s(T189)))))))), s(s(s(s(s(s(s(s(T190)))))))), T192) → U3_gga(T189, T190, T192, quot84_in_ggga(T189, T190, s(s(s(s(s(s(s(T190))))))), T192))
quot84_in_ggga(0, s(T208), T209, 0) → quot84_out_ggga(0, s(T208), T209, 0)
quot84_in_ggga(s(T226), s(T227), T228, T230) → U1_ggga(T226, T227, T228, T230, quot84_in_ggga(T226, T227, T228, T230))
quot84_in_ggga(T241, 0, T242, s(T244)) → U2_ggga(T241, T242, T244, quot3_in_gga(T241, s(T242), T244))
quot3_in_gga(s(s(s(s(s(s(s(T251))))))), s(s(s(s(s(s(s(0))))))), s(T253)) → U4_gga(T251, T253, quot97_in_ga(T251, T253))
quot97_in_ga(0, 0) → quot97_out_ga(0, 0)
quot97_in_ga(s(0), 0) → quot97_out_ga(s(0), 0)
quot97_in_ga(s(s(0)), 0) → quot97_out_ga(s(s(0)), 0)
quot97_in_ga(s(s(s(0))), 0) → quot97_out_ga(s(s(s(0))), 0)
quot97_in_ga(s(s(s(s(0)))), 0) → quot97_out_ga(s(s(s(s(0)))), 0)
quot97_in_ga(s(s(s(s(s(0))))), 0) → quot97_out_ga(s(s(s(s(s(0))))), 0)
quot97_in_ga(s(s(s(s(s(s(0)))))), 0) → quot97_out_ga(s(s(s(s(s(s(0)))))), 0)
quot97_in_ga(s(s(s(s(s(s(s(T339))))))), s(T341)) → U11_ga(T339, T341, quot97_in_ga(T339, T341))
U11_ga(T339, T341, quot97_out_ga(T339, T341)) → quot97_out_ga(s(s(s(s(s(s(s(T339))))))), s(T341))
U4_gga(T251, T253, quot97_out_ga(T251, T253)) → quot3_out_gga(s(s(s(s(s(s(s(T251))))))), s(s(s(s(s(s(s(0))))))), s(T253))
quot3_in_gga(s(s(s(s(s(s(T353)))))), s(s(s(s(s(s(0)))))), s(T355)) → U5_gga(T353, T355, quot181_in_ga(T353, T355))
quot181_in_ga(0, 0) → quot181_out_ga(0, 0)
quot181_in_ga(s(0), 0) → quot181_out_ga(s(0), 0)
quot181_in_ga(s(s(0)), 0) → quot181_out_ga(s(s(0)), 0)
quot181_in_ga(s(s(s(0))), 0) → quot181_out_ga(s(s(s(0))), 0)
quot181_in_ga(s(s(s(s(0)))), 0) → quot181_out_ga(s(s(s(s(0)))), 0)
quot181_in_ga(s(s(s(s(s(0))))), 0) → quot181_out_ga(s(s(s(s(s(0))))), 0)
quot181_in_ga(s(s(s(s(s(s(T430)))))), s(T432)) → U12_ga(T430, T432, quot181_in_ga(T430, T432))
U12_ga(T430, T432, quot181_out_ga(T430, T432)) → quot181_out_ga(s(s(s(s(s(s(T430)))))), s(T432))
U5_gga(T353, T355, quot181_out_ga(T353, T355)) → quot3_out_gga(s(s(s(s(s(s(T353)))))), s(s(s(s(s(s(0)))))), s(T355))
quot3_in_gga(s(s(s(s(s(T443))))), s(s(s(s(s(0))))), s(T445)) → U6_gga(T443, T445, quot254_in_ga(T443, T445))
quot254_in_ga(0, 0) → quot254_out_ga(0, 0)
quot254_in_ga(s(0), 0) → quot254_out_ga(s(0), 0)
quot254_in_ga(s(s(0)), 0) → quot254_out_ga(s(s(0)), 0)
quot254_in_ga(s(s(s(0))), 0) → quot254_out_ga(s(s(s(0))), 0)
quot254_in_ga(s(s(s(s(0)))), 0) → quot254_out_ga(s(s(s(s(0)))), 0)
quot254_in_ga(s(s(s(s(s(T509))))), s(T511)) → U13_ga(T509, T511, quot254_in_ga(T509, T511))
U13_ga(T509, T511, quot254_out_ga(T509, T511)) → quot254_out_ga(s(s(s(s(s(T509))))), s(T511))
U6_gga(T443, T445, quot254_out_ga(T443, T445)) → quot3_out_gga(s(s(s(s(s(T443))))), s(s(s(s(s(0))))), s(T445))
quot3_in_gga(s(s(s(s(T521)))), s(s(s(s(0)))), s(T523)) → U7_gga(T521, T523, quot316_in_ga(T521, T523))
quot316_in_ga(0, 0) → quot316_out_ga(0, 0)
quot316_in_ga(s(0), 0) → quot316_out_ga(s(0), 0)
quot316_in_ga(s(s(0)), 0) → quot316_out_ga(s(s(0)), 0)
quot316_in_ga(s(s(s(0))), 0) → quot316_out_ga(s(s(s(0))), 0)
quot316_in_ga(s(s(s(s(T576)))), s(T578)) → U14_ga(T576, T578, quot316_in_ga(T576, T578))
U14_ga(T576, T578, quot316_out_ga(T576, T578)) → quot316_out_ga(s(s(s(s(T576)))), s(T578))
U7_gga(T521, T523, quot316_out_ga(T521, T523)) → quot3_out_gga(s(s(s(s(T521)))), s(s(s(s(0)))), s(T523))
quot3_in_gga(s(s(s(T587))), s(s(s(0))), s(T589)) → U8_gga(T587, T589, quot367_in_ga(T587, T589))
quot367_in_ga(0, 0) → quot367_out_ga(0, 0)
quot367_in_ga(s(0), 0) → quot367_out_ga(s(0), 0)
quot367_in_ga(s(s(0)), 0) → quot367_out_ga(s(s(0)), 0)
quot367_in_ga(s(s(s(T631))), s(T633)) → U15_ga(T631, T633, quot367_in_ga(T631, T633))
U15_ga(T631, T633, quot367_out_ga(T631, T633)) → quot367_out_ga(s(s(s(T631))), s(T633))
U8_gga(T587, T589, quot367_out_ga(T587, T589)) → quot3_out_gga(s(s(s(T587))), s(s(s(0))), s(T589))
quot3_in_gga(s(s(T641)), s(s(0)), s(T643)) → U9_gga(T641, T643, quot407_in_ga(T641, T643))
quot407_in_ga(0, 0) → quot407_out_ga(0, 0)
quot407_in_ga(s(0), 0) → quot407_out_ga(s(0), 0)
quot407_in_ga(s(s(T674)), s(T676)) → U16_ga(T674, T676, quot407_in_ga(T674, T676))
U16_ga(T674, T676, quot407_out_ga(T674, T676)) → quot407_out_ga(s(s(T674)), s(T676))
U9_gga(T641, T643, quot407_out_ga(T641, T643)) → quot3_out_gga(s(s(T641)), s(s(0)), s(T643))
quot3_in_gga(s(T683), s(0), s(T685)) → U10_gga(T683, T685, quot436_in_ga(T683, T685))
quot436_in_ga(0, 0) → quot436_out_ga(0, 0)
quot436_in_ga(s(T705), s(T707)) → U17_ga(T705, T707, quot436_in_ga(T705, T707))
U17_ga(T705, T707, quot436_out_ga(T705, T707)) → quot436_out_ga(s(T705), s(T707))
U10_gga(T683, T685, quot436_out_ga(T683, T685)) → quot3_out_gga(s(T683), s(0), s(T685))
U2_ggga(T241, T242, T244, quot3_out_gga(T241, s(T242), T244)) → quot84_out_ggga(T241, 0, T242, s(T244))
U1_ggga(T226, T227, T228, T230, quot84_out_ggga(T226, T227, T228, T230)) → quot84_out_ggga(s(T226), s(T227), T228, T230)
U3_gga(T189, T190, T192, quot84_out_ggga(T189, T190, s(s(s(s(s(s(s(T190))))))), T192)) → quot3_out_gga(s(s(s(s(s(s(s(s(T189)))))))), s(s(s(s(s(s(s(s(T190)))))))), T192)
U18_gga(T7, T8, T10, quot3_out_gga(T7, T8, T10)) → div1_out_gga(T7, T8, T10)

The argument filtering Pi contains the following mapping:
div1_in_gga(x1, x2, x3)  =  div1_in_gga(x1, x2)
U18_gga(x1, x2, x3, x4)  =  U18_gga(x4)
quot3_in_gga(x1, x2, x3)  =  quot3_in_gga(x1, x2)
0  =  0
s(x1)  =  s(x1)
quot3_out_gga(x1, x2, x3)  =  quot3_out_gga(x3)
U3_gga(x1, x2, x3, x4)  =  U3_gga(x4)
quot84_in_ggga(x1, x2, x3, x4)  =  quot84_in_ggga(x1, x2, x3)
quot84_out_ggga(x1, x2, x3, x4)  =  quot84_out_ggga(x4)
U1_ggga(x1, x2, x3, x4, x5)  =  U1_ggga(x5)
U2_ggga(x1, x2, x3, x4)  =  U2_ggga(x4)
U4_gga(x1, x2, x3)  =  U4_gga(x3)
quot97_in_ga(x1, x2)  =  quot97_in_ga(x1)
quot97_out_ga(x1, x2)  =  quot97_out_ga(x2)
U11_ga(x1, x2, x3)  =  U11_ga(x3)
U5_gga(x1, x2, x3)  =  U5_gga(x3)
quot181_in_ga(x1, x2)  =  quot181_in_ga(x1)
quot181_out_ga(x1, x2)  =  quot181_out_ga(x2)
U12_ga(x1, x2, x3)  =  U12_ga(x3)
U6_gga(x1, x2, x3)  =  U6_gga(x3)
quot254_in_ga(x1, x2)  =  quot254_in_ga(x1)
quot254_out_ga(x1, x2)  =  quot254_out_ga(x2)
U13_ga(x1, x2, x3)  =  U13_ga(x3)
U7_gga(x1, x2, x3)  =  U7_gga(x3)
quot316_in_ga(x1, x2)  =  quot316_in_ga(x1)
quot316_out_ga(x1, x2)  =  quot316_out_ga(x2)
U14_ga(x1, x2, x3)  =  U14_ga(x3)
U8_gga(x1, x2, x3)  =  U8_gga(x3)
quot367_in_ga(x1, x2)  =  quot367_in_ga(x1)
quot367_out_ga(x1, x2)  =  quot367_out_ga(x2)
U15_ga(x1, x2, x3)  =  U15_ga(x3)
U9_gga(x1, x2, x3)  =  U9_gga(x3)
quot407_in_ga(x1, x2)  =  quot407_in_ga(x1)
quot407_out_ga(x1, x2)  =  quot407_out_ga(x2)
U16_ga(x1, x2, x3)  =  U16_ga(x3)
U10_gga(x1, x2, x3)  =  U10_gga(x3)
quot436_in_ga(x1, x2)  =  quot436_in_ga(x1)
quot436_out_ga(x1, x2)  =  quot436_out_ga(x2)
U17_ga(x1, x2, x3)  =  U17_ga(x3)
div1_out_gga(x1, x2, x3)  =  div1_out_gga(x3)
QUOT181_IN_GA(x1, x2)  =  QUOT181_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:

QUOT181_IN_GA(s(s(s(s(s(s(T430)))))), s(T432)) → QUOT181_IN_GA(T430, T432)

R is empty.
The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
QUOT181_IN_GA(x1, x2)  =  QUOT181_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:

QUOT181_IN_GA(s(s(s(s(s(s(T430))))))) → QUOT181_IN_GA(T430)

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:

  • QUOT181_IN_GA(s(s(s(s(s(s(T430))))))) → QUOT181_IN_GA(T430)
    The graph contains the following edges 1 > 1

(50) YES

(51) Obligation:

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

QUOT97_IN_GA(s(s(s(s(s(s(s(T339))))))), s(T341)) → QUOT97_IN_GA(T339, T341)

The TRS R consists of the following rules:

div1_in_gga(T7, T8, T10) → U18_gga(T7, T8, T10, quot3_in_gga(T7, T8, T10))
quot3_in_gga(0, s(T15), 0) → quot3_out_gga(0, s(T15), 0)
quot3_in_gga(s(0), s(s(T38)), 0) → quot3_out_gga(s(0), s(s(T38)), 0)
quot3_in_gga(s(s(0)), s(s(s(T61))), 0) → quot3_out_gga(s(s(0)), s(s(s(T61))), 0)
quot3_in_gga(s(s(s(0))), s(s(s(s(T84)))), 0) → quot3_out_gga(s(s(s(0))), s(s(s(s(T84)))), 0)
quot3_in_gga(s(s(s(s(0)))), s(s(s(s(s(T107))))), 0) → quot3_out_gga(s(s(s(s(0)))), s(s(s(s(s(T107))))), 0)
quot3_in_gga(s(s(s(s(s(0))))), s(s(s(s(s(s(T130)))))), 0) → quot3_out_gga(s(s(s(s(s(0))))), s(s(s(s(s(s(T130)))))), 0)
quot3_in_gga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T153))))))), 0) → quot3_out_gga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T153))))))), 0)
quot3_in_gga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(T176)))))))), 0) → quot3_out_gga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(T176)))))))), 0)
quot3_in_gga(s(s(s(s(s(s(s(s(T189)))))))), s(s(s(s(s(s(s(s(T190)))))))), T192) → U3_gga(T189, T190, T192, quot84_in_ggga(T189, T190, s(s(s(s(s(s(s(T190))))))), T192))
quot84_in_ggga(0, s(T208), T209, 0) → quot84_out_ggga(0, s(T208), T209, 0)
quot84_in_ggga(s(T226), s(T227), T228, T230) → U1_ggga(T226, T227, T228, T230, quot84_in_ggga(T226, T227, T228, T230))
quot84_in_ggga(T241, 0, T242, s(T244)) → U2_ggga(T241, T242, T244, quot3_in_gga(T241, s(T242), T244))
quot3_in_gga(s(s(s(s(s(s(s(T251))))))), s(s(s(s(s(s(s(0))))))), s(T253)) → U4_gga(T251, T253, quot97_in_ga(T251, T253))
quot97_in_ga(0, 0) → quot97_out_ga(0, 0)
quot97_in_ga(s(0), 0) → quot97_out_ga(s(0), 0)
quot97_in_ga(s(s(0)), 0) → quot97_out_ga(s(s(0)), 0)
quot97_in_ga(s(s(s(0))), 0) → quot97_out_ga(s(s(s(0))), 0)
quot97_in_ga(s(s(s(s(0)))), 0) → quot97_out_ga(s(s(s(s(0)))), 0)
quot97_in_ga(s(s(s(s(s(0))))), 0) → quot97_out_ga(s(s(s(s(s(0))))), 0)
quot97_in_ga(s(s(s(s(s(s(0)))))), 0) → quot97_out_ga(s(s(s(s(s(s(0)))))), 0)
quot97_in_ga(s(s(s(s(s(s(s(T339))))))), s(T341)) → U11_ga(T339, T341, quot97_in_ga(T339, T341))
U11_ga(T339, T341, quot97_out_ga(T339, T341)) → quot97_out_ga(s(s(s(s(s(s(s(T339))))))), s(T341))
U4_gga(T251, T253, quot97_out_ga(T251, T253)) → quot3_out_gga(s(s(s(s(s(s(s(T251))))))), s(s(s(s(s(s(s(0))))))), s(T253))
quot3_in_gga(s(s(s(s(s(s(T353)))))), s(s(s(s(s(s(0)))))), s(T355)) → U5_gga(T353, T355, quot181_in_ga(T353, T355))
quot181_in_ga(0, 0) → quot181_out_ga(0, 0)
quot181_in_ga(s(0), 0) → quot181_out_ga(s(0), 0)
quot181_in_ga(s(s(0)), 0) → quot181_out_ga(s(s(0)), 0)
quot181_in_ga(s(s(s(0))), 0) → quot181_out_ga(s(s(s(0))), 0)
quot181_in_ga(s(s(s(s(0)))), 0) → quot181_out_ga(s(s(s(s(0)))), 0)
quot181_in_ga(s(s(s(s(s(0))))), 0) → quot181_out_ga(s(s(s(s(s(0))))), 0)
quot181_in_ga(s(s(s(s(s(s(T430)))))), s(T432)) → U12_ga(T430, T432, quot181_in_ga(T430, T432))
U12_ga(T430, T432, quot181_out_ga(T430, T432)) → quot181_out_ga(s(s(s(s(s(s(T430)))))), s(T432))
U5_gga(T353, T355, quot181_out_ga(T353, T355)) → quot3_out_gga(s(s(s(s(s(s(T353)))))), s(s(s(s(s(s(0)))))), s(T355))
quot3_in_gga(s(s(s(s(s(T443))))), s(s(s(s(s(0))))), s(T445)) → U6_gga(T443, T445, quot254_in_ga(T443, T445))
quot254_in_ga(0, 0) → quot254_out_ga(0, 0)
quot254_in_ga(s(0), 0) → quot254_out_ga(s(0), 0)
quot254_in_ga(s(s(0)), 0) → quot254_out_ga(s(s(0)), 0)
quot254_in_ga(s(s(s(0))), 0) → quot254_out_ga(s(s(s(0))), 0)
quot254_in_ga(s(s(s(s(0)))), 0) → quot254_out_ga(s(s(s(s(0)))), 0)
quot254_in_ga(s(s(s(s(s(T509))))), s(T511)) → U13_ga(T509, T511, quot254_in_ga(T509, T511))
U13_ga(T509, T511, quot254_out_ga(T509, T511)) → quot254_out_ga(s(s(s(s(s(T509))))), s(T511))
U6_gga(T443, T445, quot254_out_ga(T443, T445)) → quot3_out_gga(s(s(s(s(s(T443))))), s(s(s(s(s(0))))), s(T445))
quot3_in_gga(s(s(s(s(T521)))), s(s(s(s(0)))), s(T523)) → U7_gga(T521, T523, quot316_in_ga(T521, T523))
quot316_in_ga(0, 0) → quot316_out_ga(0, 0)
quot316_in_ga(s(0), 0) → quot316_out_ga(s(0), 0)
quot316_in_ga(s(s(0)), 0) → quot316_out_ga(s(s(0)), 0)
quot316_in_ga(s(s(s(0))), 0) → quot316_out_ga(s(s(s(0))), 0)
quot316_in_ga(s(s(s(s(T576)))), s(T578)) → U14_ga(T576, T578, quot316_in_ga(T576, T578))
U14_ga(T576, T578, quot316_out_ga(T576, T578)) → quot316_out_ga(s(s(s(s(T576)))), s(T578))
U7_gga(T521, T523, quot316_out_ga(T521, T523)) → quot3_out_gga(s(s(s(s(T521)))), s(s(s(s(0)))), s(T523))
quot3_in_gga(s(s(s(T587))), s(s(s(0))), s(T589)) → U8_gga(T587, T589, quot367_in_ga(T587, T589))
quot367_in_ga(0, 0) → quot367_out_ga(0, 0)
quot367_in_ga(s(0), 0) → quot367_out_ga(s(0), 0)
quot367_in_ga(s(s(0)), 0) → quot367_out_ga(s(s(0)), 0)
quot367_in_ga(s(s(s(T631))), s(T633)) → U15_ga(T631, T633, quot367_in_ga(T631, T633))
U15_ga(T631, T633, quot367_out_ga(T631, T633)) → quot367_out_ga(s(s(s(T631))), s(T633))
U8_gga(T587, T589, quot367_out_ga(T587, T589)) → quot3_out_gga(s(s(s(T587))), s(s(s(0))), s(T589))
quot3_in_gga(s(s(T641)), s(s(0)), s(T643)) → U9_gga(T641, T643, quot407_in_ga(T641, T643))
quot407_in_ga(0, 0) → quot407_out_ga(0, 0)
quot407_in_ga(s(0), 0) → quot407_out_ga(s(0), 0)
quot407_in_ga(s(s(T674)), s(T676)) → U16_ga(T674, T676, quot407_in_ga(T674, T676))
U16_ga(T674, T676, quot407_out_ga(T674, T676)) → quot407_out_ga(s(s(T674)), s(T676))
U9_gga(T641, T643, quot407_out_ga(T641, T643)) → quot3_out_gga(s(s(T641)), s(s(0)), s(T643))
quot3_in_gga(s(T683), s(0), s(T685)) → U10_gga(T683, T685, quot436_in_ga(T683, T685))
quot436_in_ga(0, 0) → quot436_out_ga(0, 0)
quot436_in_ga(s(T705), s(T707)) → U17_ga(T705, T707, quot436_in_ga(T705, T707))
U17_ga(T705, T707, quot436_out_ga(T705, T707)) → quot436_out_ga(s(T705), s(T707))
U10_gga(T683, T685, quot436_out_ga(T683, T685)) → quot3_out_gga(s(T683), s(0), s(T685))
U2_ggga(T241, T242, T244, quot3_out_gga(T241, s(T242), T244)) → quot84_out_ggga(T241, 0, T242, s(T244))
U1_ggga(T226, T227, T228, T230, quot84_out_ggga(T226, T227, T228, T230)) → quot84_out_ggga(s(T226), s(T227), T228, T230)
U3_gga(T189, T190, T192, quot84_out_ggga(T189, T190, s(s(s(s(s(s(s(T190))))))), T192)) → quot3_out_gga(s(s(s(s(s(s(s(s(T189)))))))), s(s(s(s(s(s(s(s(T190)))))))), T192)
U18_gga(T7, T8, T10, quot3_out_gga(T7, T8, T10)) → div1_out_gga(T7, T8, T10)

The argument filtering Pi contains the following mapping:
div1_in_gga(x1, x2, x3)  =  div1_in_gga(x1, x2)
U18_gga(x1, x2, x3, x4)  =  U18_gga(x4)
quot3_in_gga(x1, x2, x3)  =  quot3_in_gga(x1, x2)
0  =  0
s(x1)  =  s(x1)
quot3_out_gga(x1, x2, x3)  =  quot3_out_gga(x3)
U3_gga(x1, x2, x3, x4)  =  U3_gga(x4)
quot84_in_ggga(x1, x2, x3, x4)  =  quot84_in_ggga(x1, x2, x3)
quot84_out_ggga(x1, x2, x3, x4)  =  quot84_out_ggga(x4)
U1_ggga(x1, x2, x3, x4, x5)  =  U1_ggga(x5)
U2_ggga(x1, x2, x3, x4)  =  U2_ggga(x4)
U4_gga(x1, x2, x3)  =  U4_gga(x3)
quot97_in_ga(x1, x2)  =  quot97_in_ga(x1)
quot97_out_ga(x1, x2)  =  quot97_out_ga(x2)
U11_ga(x1, x2, x3)  =  U11_ga(x3)
U5_gga(x1, x2, x3)  =  U5_gga(x3)
quot181_in_ga(x1, x2)  =  quot181_in_ga(x1)
quot181_out_ga(x1, x2)  =  quot181_out_ga(x2)
U12_ga(x1, x2, x3)  =  U12_ga(x3)
U6_gga(x1, x2, x3)  =  U6_gga(x3)
quot254_in_ga(x1, x2)  =  quot254_in_ga(x1)
quot254_out_ga(x1, x2)  =  quot254_out_ga(x2)
U13_ga(x1, x2, x3)  =  U13_ga(x3)
U7_gga(x1, x2, x3)  =  U7_gga(x3)
quot316_in_ga(x1, x2)  =  quot316_in_ga(x1)
quot316_out_ga(x1, x2)  =  quot316_out_ga(x2)
U14_ga(x1, x2, x3)  =  U14_ga(x3)
U8_gga(x1, x2, x3)  =  U8_gga(x3)
quot367_in_ga(x1, x2)  =  quot367_in_ga(x1)
quot367_out_ga(x1, x2)  =  quot367_out_ga(x2)
U15_ga(x1, x2, x3)  =  U15_ga(x3)
U9_gga(x1, x2, x3)  =  U9_gga(x3)
quot407_in_ga(x1, x2)  =  quot407_in_ga(x1)
quot407_out_ga(x1, x2)  =  quot407_out_ga(x2)
U16_ga(x1, x2, x3)  =  U16_ga(x3)
U10_gga(x1, x2, x3)  =  U10_gga(x3)
quot436_in_ga(x1, x2)  =  quot436_in_ga(x1)
quot436_out_ga(x1, x2)  =  quot436_out_ga(x2)
U17_ga(x1, x2, x3)  =  U17_ga(x3)
div1_out_gga(x1, x2, x3)  =  div1_out_gga(x3)
QUOT97_IN_GA(x1, x2)  =  QUOT97_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:

QUOT97_IN_GA(s(s(s(s(s(s(s(T339))))))), s(T341)) → QUOT97_IN_GA(T339, T341)

R is empty.
The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
QUOT97_IN_GA(x1, x2)  =  QUOT97_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:

QUOT97_IN_GA(s(s(s(s(s(s(s(T339)))))))) → QUOT97_IN_GA(T339)

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:

  • QUOT97_IN_GA(s(s(s(s(s(s(s(T339)))))))) → QUOT97_IN_GA(T339)
    The graph contains the following edges 1 > 1

(57) YES

(58) Obligation:

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

QUOT3_IN_GGA(s(s(s(s(s(s(s(s(T189)))))))), s(s(s(s(s(s(s(s(T190)))))))), T192) → QUOT84_IN_GGGA(T189, T190, s(s(s(s(s(s(s(T190))))))), T192)
QUOT84_IN_GGGA(s(T226), s(T227), T228, T230) → QUOT84_IN_GGGA(T226, T227, T228, T230)
QUOT84_IN_GGGA(T241, 0, T242, s(T244)) → QUOT3_IN_GGA(T241, s(T242), T244)

The TRS R consists of the following rules:

div1_in_gga(T7, T8, T10) → U18_gga(T7, T8, T10, quot3_in_gga(T7, T8, T10))
quot3_in_gga(0, s(T15), 0) → quot3_out_gga(0, s(T15), 0)
quot3_in_gga(s(0), s(s(T38)), 0) → quot3_out_gga(s(0), s(s(T38)), 0)
quot3_in_gga(s(s(0)), s(s(s(T61))), 0) → quot3_out_gga(s(s(0)), s(s(s(T61))), 0)
quot3_in_gga(s(s(s(0))), s(s(s(s(T84)))), 0) → quot3_out_gga(s(s(s(0))), s(s(s(s(T84)))), 0)
quot3_in_gga(s(s(s(s(0)))), s(s(s(s(s(T107))))), 0) → quot3_out_gga(s(s(s(s(0)))), s(s(s(s(s(T107))))), 0)
quot3_in_gga(s(s(s(s(s(0))))), s(s(s(s(s(s(T130)))))), 0) → quot3_out_gga(s(s(s(s(s(0))))), s(s(s(s(s(s(T130)))))), 0)
quot3_in_gga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T153))))))), 0) → quot3_out_gga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T153))))))), 0)
quot3_in_gga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(T176)))))))), 0) → quot3_out_gga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(T176)))))))), 0)
quot3_in_gga(s(s(s(s(s(s(s(s(T189)))))))), s(s(s(s(s(s(s(s(T190)))))))), T192) → U3_gga(T189, T190, T192, quot84_in_ggga(T189, T190, s(s(s(s(s(s(s(T190))))))), T192))
quot84_in_ggga(0, s(T208), T209, 0) → quot84_out_ggga(0, s(T208), T209, 0)
quot84_in_ggga(s(T226), s(T227), T228, T230) → U1_ggga(T226, T227, T228, T230, quot84_in_ggga(T226, T227, T228, T230))
quot84_in_ggga(T241, 0, T242, s(T244)) → U2_ggga(T241, T242, T244, quot3_in_gga(T241, s(T242), T244))
quot3_in_gga(s(s(s(s(s(s(s(T251))))))), s(s(s(s(s(s(s(0))))))), s(T253)) → U4_gga(T251, T253, quot97_in_ga(T251, T253))
quot97_in_ga(0, 0) → quot97_out_ga(0, 0)
quot97_in_ga(s(0), 0) → quot97_out_ga(s(0), 0)
quot97_in_ga(s(s(0)), 0) → quot97_out_ga(s(s(0)), 0)
quot97_in_ga(s(s(s(0))), 0) → quot97_out_ga(s(s(s(0))), 0)
quot97_in_ga(s(s(s(s(0)))), 0) → quot97_out_ga(s(s(s(s(0)))), 0)
quot97_in_ga(s(s(s(s(s(0))))), 0) → quot97_out_ga(s(s(s(s(s(0))))), 0)
quot97_in_ga(s(s(s(s(s(s(0)))))), 0) → quot97_out_ga(s(s(s(s(s(s(0)))))), 0)
quot97_in_ga(s(s(s(s(s(s(s(T339))))))), s(T341)) → U11_ga(T339, T341, quot97_in_ga(T339, T341))
U11_ga(T339, T341, quot97_out_ga(T339, T341)) → quot97_out_ga(s(s(s(s(s(s(s(T339))))))), s(T341))
U4_gga(T251, T253, quot97_out_ga(T251, T253)) → quot3_out_gga(s(s(s(s(s(s(s(T251))))))), s(s(s(s(s(s(s(0))))))), s(T253))
quot3_in_gga(s(s(s(s(s(s(T353)))))), s(s(s(s(s(s(0)))))), s(T355)) → U5_gga(T353, T355, quot181_in_ga(T353, T355))
quot181_in_ga(0, 0) → quot181_out_ga(0, 0)
quot181_in_ga(s(0), 0) → quot181_out_ga(s(0), 0)
quot181_in_ga(s(s(0)), 0) → quot181_out_ga(s(s(0)), 0)
quot181_in_ga(s(s(s(0))), 0) → quot181_out_ga(s(s(s(0))), 0)
quot181_in_ga(s(s(s(s(0)))), 0) → quot181_out_ga(s(s(s(s(0)))), 0)
quot181_in_ga(s(s(s(s(s(0))))), 0) → quot181_out_ga(s(s(s(s(s(0))))), 0)
quot181_in_ga(s(s(s(s(s(s(T430)))))), s(T432)) → U12_ga(T430, T432, quot181_in_ga(T430, T432))
U12_ga(T430, T432, quot181_out_ga(T430, T432)) → quot181_out_ga(s(s(s(s(s(s(T430)))))), s(T432))
U5_gga(T353, T355, quot181_out_ga(T353, T355)) → quot3_out_gga(s(s(s(s(s(s(T353)))))), s(s(s(s(s(s(0)))))), s(T355))
quot3_in_gga(s(s(s(s(s(T443))))), s(s(s(s(s(0))))), s(T445)) → U6_gga(T443, T445, quot254_in_ga(T443, T445))
quot254_in_ga(0, 0) → quot254_out_ga(0, 0)
quot254_in_ga(s(0), 0) → quot254_out_ga(s(0), 0)
quot254_in_ga(s(s(0)), 0) → quot254_out_ga(s(s(0)), 0)
quot254_in_ga(s(s(s(0))), 0) → quot254_out_ga(s(s(s(0))), 0)
quot254_in_ga(s(s(s(s(0)))), 0) → quot254_out_ga(s(s(s(s(0)))), 0)
quot254_in_ga(s(s(s(s(s(T509))))), s(T511)) → U13_ga(T509, T511, quot254_in_ga(T509, T511))
U13_ga(T509, T511, quot254_out_ga(T509, T511)) → quot254_out_ga(s(s(s(s(s(T509))))), s(T511))
U6_gga(T443, T445, quot254_out_ga(T443, T445)) → quot3_out_gga(s(s(s(s(s(T443))))), s(s(s(s(s(0))))), s(T445))
quot3_in_gga(s(s(s(s(T521)))), s(s(s(s(0)))), s(T523)) → U7_gga(T521, T523, quot316_in_ga(T521, T523))
quot316_in_ga(0, 0) → quot316_out_ga(0, 0)
quot316_in_ga(s(0), 0) → quot316_out_ga(s(0), 0)
quot316_in_ga(s(s(0)), 0) → quot316_out_ga(s(s(0)), 0)
quot316_in_ga(s(s(s(0))), 0) → quot316_out_ga(s(s(s(0))), 0)
quot316_in_ga(s(s(s(s(T576)))), s(T578)) → U14_ga(T576, T578, quot316_in_ga(T576, T578))
U14_ga(T576, T578, quot316_out_ga(T576, T578)) → quot316_out_ga(s(s(s(s(T576)))), s(T578))
U7_gga(T521, T523, quot316_out_ga(T521, T523)) → quot3_out_gga(s(s(s(s(T521)))), s(s(s(s(0)))), s(T523))
quot3_in_gga(s(s(s(T587))), s(s(s(0))), s(T589)) → U8_gga(T587, T589, quot367_in_ga(T587, T589))
quot367_in_ga(0, 0) → quot367_out_ga(0, 0)
quot367_in_ga(s(0), 0) → quot367_out_ga(s(0), 0)
quot367_in_ga(s(s(0)), 0) → quot367_out_ga(s(s(0)), 0)
quot367_in_ga(s(s(s(T631))), s(T633)) → U15_ga(T631, T633, quot367_in_ga(T631, T633))
U15_ga(T631, T633, quot367_out_ga(T631, T633)) → quot367_out_ga(s(s(s(T631))), s(T633))
U8_gga(T587, T589, quot367_out_ga(T587, T589)) → quot3_out_gga(s(s(s(T587))), s(s(s(0))), s(T589))
quot3_in_gga(s(s(T641)), s(s(0)), s(T643)) → U9_gga(T641, T643, quot407_in_ga(T641, T643))
quot407_in_ga(0, 0) → quot407_out_ga(0, 0)
quot407_in_ga(s(0), 0) → quot407_out_ga(s(0), 0)
quot407_in_ga(s(s(T674)), s(T676)) → U16_ga(T674, T676, quot407_in_ga(T674, T676))
U16_ga(T674, T676, quot407_out_ga(T674, T676)) → quot407_out_ga(s(s(T674)), s(T676))
U9_gga(T641, T643, quot407_out_ga(T641, T643)) → quot3_out_gga(s(s(T641)), s(s(0)), s(T643))
quot3_in_gga(s(T683), s(0), s(T685)) → U10_gga(T683, T685, quot436_in_ga(T683, T685))
quot436_in_ga(0, 0) → quot436_out_ga(0, 0)
quot436_in_ga(s(T705), s(T707)) → U17_ga(T705, T707, quot436_in_ga(T705, T707))
U17_ga(T705, T707, quot436_out_ga(T705, T707)) → quot436_out_ga(s(T705), s(T707))
U10_gga(T683, T685, quot436_out_ga(T683, T685)) → quot3_out_gga(s(T683), s(0), s(T685))
U2_ggga(T241, T242, T244, quot3_out_gga(T241, s(T242), T244)) → quot84_out_ggga(T241, 0, T242, s(T244))
U1_ggga(T226, T227, T228, T230, quot84_out_ggga(T226, T227, T228, T230)) → quot84_out_ggga(s(T226), s(T227), T228, T230)
U3_gga(T189, T190, T192, quot84_out_ggga(T189, T190, s(s(s(s(s(s(s(T190))))))), T192)) → quot3_out_gga(s(s(s(s(s(s(s(s(T189)))))))), s(s(s(s(s(s(s(s(T190)))))))), T192)
U18_gga(T7, T8, T10, quot3_out_gga(T7, T8, T10)) → div1_out_gga(T7, T8, T10)

The argument filtering Pi contains the following mapping:
div1_in_gga(x1, x2, x3)  =  div1_in_gga(x1, x2)
U18_gga(x1, x2, x3, x4)  =  U18_gga(x4)
quot3_in_gga(x1, x2, x3)  =  quot3_in_gga(x1, x2)
0  =  0
s(x1)  =  s(x1)
quot3_out_gga(x1, x2, x3)  =  quot3_out_gga(x3)
U3_gga(x1, x2, x3, x4)  =  U3_gga(x4)
quot84_in_ggga(x1, x2, x3, x4)  =  quot84_in_ggga(x1, x2, x3)
quot84_out_ggga(x1, x2, x3, x4)  =  quot84_out_ggga(x4)
U1_ggga(x1, x2, x3, x4, x5)  =  U1_ggga(x5)
U2_ggga(x1, x2, x3, x4)  =  U2_ggga(x4)
U4_gga(x1, x2, x3)  =  U4_gga(x3)
quot97_in_ga(x1, x2)  =  quot97_in_ga(x1)
quot97_out_ga(x1, x2)  =  quot97_out_ga(x2)
U11_ga(x1, x2, x3)  =  U11_ga(x3)
U5_gga(x1, x2, x3)  =  U5_gga(x3)
quot181_in_ga(x1, x2)  =  quot181_in_ga(x1)
quot181_out_ga(x1, x2)  =  quot181_out_ga(x2)
U12_ga(x1, x2, x3)  =  U12_ga(x3)
U6_gga(x1, x2, x3)  =  U6_gga(x3)
quot254_in_ga(x1, x2)  =  quot254_in_ga(x1)
quot254_out_ga(x1, x2)  =  quot254_out_ga(x2)
U13_ga(x1, x2, x3)  =  U13_ga(x3)
U7_gga(x1, x2, x3)  =  U7_gga(x3)
quot316_in_ga(x1, x2)  =  quot316_in_ga(x1)
quot316_out_ga(x1, x2)  =  quot316_out_ga(x2)
U14_ga(x1, x2, x3)  =  U14_ga(x3)
U8_gga(x1, x2, x3)  =  U8_gga(x3)
quot367_in_ga(x1, x2)  =  quot367_in_ga(x1)
quot367_out_ga(x1, x2)  =  quot367_out_ga(x2)
U15_ga(x1, x2, x3)  =  U15_ga(x3)
U9_gga(x1, x2, x3)  =  U9_gga(x3)
quot407_in_ga(x1, x2)  =  quot407_in_ga(x1)
quot407_out_ga(x1, x2)  =  quot407_out_ga(x2)
U16_ga(x1, x2, x3)  =  U16_ga(x3)
U10_gga(x1, x2, x3)  =  U10_gga(x3)
quot436_in_ga(x1, x2)  =  quot436_in_ga(x1)
quot436_out_ga(x1, x2)  =  quot436_out_ga(x2)
U17_ga(x1, x2, x3)  =  U17_ga(x3)
div1_out_gga(x1, x2, x3)  =  div1_out_gga(x3)
QUOT3_IN_GGA(x1, x2, x3)  =  QUOT3_IN_GGA(x1, x2)
QUOT84_IN_GGGA(x1, x2, x3, x4)  =  QUOT84_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:

QUOT3_IN_GGA(s(s(s(s(s(s(s(s(T189)))))))), s(s(s(s(s(s(s(s(T190)))))))), T192) → QUOT84_IN_GGGA(T189, T190, s(s(s(s(s(s(s(T190))))))), T192)
QUOT84_IN_GGGA(s(T226), s(T227), T228, T230) → QUOT84_IN_GGGA(T226, T227, T228, T230)
QUOT84_IN_GGGA(T241, 0, T242, s(T244)) → QUOT3_IN_GGA(T241, s(T242), T244)

R is empty.
The argument filtering Pi contains the following mapping:
0  =  0
s(x1)  =  s(x1)
QUOT3_IN_GGA(x1, x2, x3)  =  QUOT3_IN_GGA(x1, x2)
QUOT84_IN_GGGA(x1, x2, x3, x4)  =  QUOT84_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:

QUOT3_IN_GGA(s(s(s(s(s(s(s(s(T189)))))))), s(s(s(s(s(s(s(s(T190))))))))) → QUOT84_IN_GGGA(T189, T190, s(s(s(s(s(s(s(T190))))))))
QUOT84_IN_GGGA(s(T226), s(T227), T228) → QUOT84_IN_GGGA(T226, T227, T228)
QUOT84_IN_GGGA(T241, 0, T242) → QUOT3_IN_GGA(T241, s(T242))

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:

  • QUOT84_IN_GGGA(T241, 0, T242) → QUOT3_IN_GGA(T241, s(T242))
    The graph contains the following edges 1 >= 1

  • QUOT84_IN_GGGA(s(T226), s(T227), T228) → QUOT84_IN_GGGA(T226, T227, T228)
    The graph contains the following edges 1 > 1, 2 > 2, 3 >= 3

  • QUOT3_IN_GGA(s(s(s(s(s(s(s(s(T189)))))))), s(s(s(s(s(s(s(s(T190))))))))) → QUOT84_IN_GGGA(T189, T190, s(s(s(s(s(s(s(T190))))))))
    The graph contains the following edges 1 > 1, 2 > 2, 2 > 3

(64) YES