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

Query: div(g,g,a)

(1) PrologToPiTRSViaGraphTransformerProof (SOUND transformation)

Transformed Prolog program to (Pi-)TRS.

(2) Obligation:

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

divA_in_gga(T7, T8, T10) → U1_gga(T7, T8, T10, quotB_in_gga(T7, T8, T10))
quotB_in_gga(0, s(T15), 0) → quotB_out_gga(0, s(T15), 0)
quotB_in_gga(s(0), s(s(T38)), 0) → quotB_out_gga(s(0), s(s(T38)), 0)
quotB_in_gga(s(s(0)), s(s(s(T61))), 0) → quotB_out_gga(s(s(0)), s(s(s(T61))), 0)
quotB_in_gga(s(s(s(0))), s(s(s(s(T84)))), 0) → quotB_out_gga(s(s(s(0))), s(s(s(s(T84)))), 0)
quotB_in_gga(s(s(s(s(0)))), s(s(s(s(s(T107))))), 0) → quotB_out_gga(s(s(s(s(0)))), s(s(s(s(s(T107))))), 0)
quotB_in_gga(s(s(s(s(s(0))))), s(s(s(s(s(s(T130)))))), 0) → quotB_out_gga(s(s(s(s(s(0))))), s(s(s(s(s(s(T130)))))), 0)
quotB_in_gga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T153))))))), 0) → quotB_out_gga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T153))))))), 0)
quotB_in_gga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(T176)))))))), 0) → quotB_out_gga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(T176)))))))), 0)
quotB_in_gga(s(s(s(s(s(s(s(s(T189)))))))), s(s(s(s(s(s(s(s(T190)))))))), T192) → U4_gga(T189, T190, T192, quotC_in_ggga(T189, T190, s(s(s(s(s(s(s(T190))))))), T192))
quotC_in_ggga(0, s(T208), T209, 0) → quotC_out_ggga(0, s(T208), T209, 0)
quotC_in_ggga(s(T226), s(T227), T228, T230) → U2_ggga(T226, T227, T228, T230, quotC_in_ggga(T226, T227, T228, T230))
quotC_in_ggga(T241, 0, T242, s(T244)) → U3_ggga(T241, T242, T244, quotB_in_gga(T241, s(T242), T244))
quotB_in_gga(s(s(s(s(s(s(s(T251))))))), s(s(s(s(s(s(s(0))))))), s(T253)) → U5_gga(T251, T253, quotD_in_ga(T251, T253))
quotD_in_ga(0, 0) → quotD_out_ga(0, 0)
quotD_in_ga(s(0), 0) → quotD_out_ga(s(0), 0)
quotD_in_ga(s(s(0)), 0) → quotD_out_ga(s(s(0)), 0)
quotD_in_ga(s(s(s(0))), 0) → quotD_out_ga(s(s(s(0))), 0)
quotD_in_ga(s(s(s(s(0)))), 0) → quotD_out_ga(s(s(s(s(0)))), 0)
quotD_in_ga(s(s(s(s(s(0))))), 0) → quotD_out_ga(s(s(s(s(s(0))))), 0)
quotD_in_ga(s(s(s(s(s(s(0)))))), 0) → quotD_out_ga(s(s(s(s(s(s(0)))))), 0)
quotD_in_ga(s(s(s(s(s(s(s(T336))))))), s(T338)) → U12_ga(T336, T338, quotD_in_ga(T336, T338))
U12_ga(T336, T338, quotD_out_ga(T336, T338)) → quotD_out_ga(s(s(s(s(s(s(s(T336))))))), s(T338))
U5_gga(T251, T253, quotD_out_ga(T251, T253)) → quotB_out_gga(s(s(s(s(s(s(s(T251))))))), s(s(s(s(s(s(s(0))))))), s(T253))
quotB_in_gga(s(s(s(s(s(s(T350)))))), s(s(s(s(s(s(0)))))), s(T352)) → U6_gga(T350, T352, quotE_in_ga(T350, T352))
quotE_in_ga(0, 0) → quotE_out_ga(0, 0)
quotE_in_ga(s(0), 0) → quotE_out_ga(s(0), 0)
quotE_in_ga(s(s(0)), 0) → quotE_out_ga(s(s(0)), 0)
quotE_in_ga(s(s(s(0))), 0) → quotE_out_ga(s(s(s(0))), 0)
quotE_in_ga(s(s(s(s(0)))), 0) → quotE_out_ga(s(s(s(s(0)))), 0)
quotE_in_ga(s(s(s(s(s(0))))), 0) → quotE_out_ga(s(s(s(s(s(0))))), 0)
quotE_in_ga(s(s(s(s(s(s(T424)))))), s(T426)) → U13_ga(T424, T426, quotE_in_ga(T424, T426))
U13_ga(T424, T426, quotE_out_ga(T424, T426)) → quotE_out_ga(s(s(s(s(s(s(T424)))))), s(T426))
U6_gga(T350, T352, quotE_out_ga(T350, T352)) → quotB_out_gga(s(s(s(s(s(s(T350)))))), s(s(s(s(s(s(0)))))), s(T352))
quotB_in_gga(s(s(s(s(s(T437))))), s(s(s(s(s(0))))), s(T439)) → U7_gga(T437, T439, quotF_in_ga(T437, T439))
quotF_in_ga(0, 0) → quotF_out_ga(0, 0)
quotF_in_ga(s(0), 0) → quotF_out_ga(s(0), 0)
quotF_in_ga(s(s(0)), 0) → quotF_out_ga(s(s(0)), 0)
quotF_in_ga(s(s(s(0))), 0) → quotF_out_ga(s(s(s(0))), 0)
quotF_in_ga(s(s(s(s(0)))), 0) → quotF_out_ga(s(s(s(s(0)))), 0)
quotF_in_ga(s(s(s(s(s(T500))))), s(T502)) → U14_ga(T500, T502, quotF_in_ga(T500, T502))
U14_ga(T500, T502, quotF_out_ga(T500, T502)) → quotF_out_ga(s(s(s(s(s(T500))))), s(T502))
U7_gga(T437, T439, quotF_out_ga(T437, T439)) → quotB_out_gga(s(s(s(s(s(T437))))), s(s(s(s(s(0))))), s(T439))
quotB_in_gga(s(s(s(s(T512)))), s(s(s(s(0)))), s(T514)) → U8_gga(T512, T514, quotG_in_ga(T512, T514))
quotG_in_ga(0, 0) → quotG_out_ga(0, 0)
quotG_in_ga(s(0), 0) → quotG_out_ga(s(0), 0)
quotG_in_ga(s(s(0)), 0) → quotG_out_ga(s(s(0)), 0)
quotG_in_ga(s(s(s(0))), 0) → quotG_out_ga(s(s(s(0))), 0)
quotG_in_ga(s(s(s(s(T564)))), s(T566)) → U15_ga(T564, T566, quotG_in_ga(T564, T566))
U15_ga(T564, T566, quotG_out_ga(T564, T566)) → quotG_out_ga(s(s(s(s(T564)))), s(T566))
U8_gga(T512, T514, quotG_out_ga(T512, T514)) → quotB_out_gga(s(s(s(s(T512)))), s(s(s(s(0)))), s(T514))
quotB_in_gga(s(s(s(T575))), s(s(s(0))), s(T577)) → U9_gga(T575, T577, quotH_in_ga(T575, T577))
quotH_in_ga(0, 0) → quotH_out_ga(0, 0)
quotH_in_ga(s(0), 0) → quotH_out_ga(s(0), 0)
quotH_in_ga(s(s(0)), 0) → quotH_out_ga(s(s(0)), 0)
quotH_in_ga(s(s(s(T616))), s(T618)) → U16_ga(T616, T618, quotH_in_ga(T616, T618))
U16_ga(T616, T618, quotH_out_ga(T616, T618)) → quotH_out_ga(s(s(s(T616))), s(T618))
U9_gga(T575, T577, quotH_out_ga(T575, T577)) → quotB_out_gga(s(s(s(T575))), s(s(s(0))), s(T577))
quotB_in_gga(s(s(T626)), s(s(0)), s(T628)) → U10_gga(T626, T628, quotI_in_ga(T626, T628))
quotI_in_ga(0, 0) → quotI_out_ga(0, 0)
quotI_in_ga(s(0), 0) → quotI_out_ga(s(0), 0)
quotI_in_ga(s(s(T656)), s(T658)) → U17_ga(T656, T658, quotI_in_ga(T656, T658))
U17_ga(T656, T658, quotI_out_ga(T656, T658)) → quotI_out_ga(s(s(T656)), s(T658))
U10_gga(T626, T628, quotI_out_ga(T626, T628)) → quotB_out_gga(s(s(T626)), s(s(0)), s(T628))
quotB_in_gga(s(T665), s(0), s(T667)) → U11_gga(T665, T667, quotJ_in_ga(T665, T667))
quotJ_in_ga(0, 0) → quotJ_out_ga(0, 0)
quotJ_in_ga(s(T684), s(T686)) → U18_ga(T684, T686, quotJ_in_ga(T684, T686))
U18_ga(T684, T686, quotJ_out_ga(T684, T686)) → quotJ_out_ga(s(T684), s(T686))
U11_gga(T665, T667, quotJ_out_ga(T665, T667)) → quotB_out_gga(s(T665), s(0), s(T667))
U3_ggga(T241, T242, T244, quotB_out_gga(T241, s(T242), T244)) → quotC_out_ggga(T241, 0, T242, s(T244))
U2_ggga(T226, T227, T228, T230, quotC_out_ggga(T226, T227, T228, T230)) → quotC_out_ggga(s(T226), s(T227), T228, T230)
U4_gga(T189, T190, T192, quotC_out_ggga(T189, T190, s(s(s(s(s(s(s(T190))))))), T192)) → quotB_out_gga(s(s(s(s(s(s(s(s(T189)))))))), s(s(s(s(s(s(s(s(T190)))))))), T192)
U1_gga(T7, T8, T10, quotB_out_gga(T7, T8, T10)) → divA_out_gga(T7, T8, T10)

The argument filtering Pi contains the following mapping:
divA_in_gga(x1, x2, x3)  =  divA_in_gga(x1, x2)
U1_gga(x1, x2, x3, x4)  =  U1_gga(x1, x2, x4)
quotB_in_gga(x1, x2, x3)  =  quotB_in_gga(x1, x2)
0  =  0
s(x1)  =  s(x1)
quotB_out_gga(x1, x2, x3)  =  quotB_out_gga(x1, x2, x3)
U4_gga(x1, x2, x3, x4)  =  U4_gga(x1, x2, x4)
quotC_in_ggga(x1, x2, x3, x4)  =  quotC_in_ggga(x1, x2, x3)
quotC_out_ggga(x1, x2, x3, x4)  =  quotC_out_ggga(x1, x2, x3, x4)
U2_ggga(x1, x2, x3, x4, x5)  =  U2_ggga(x1, x2, x3, x5)
U3_ggga(x1, x2, x3, x4)  =  U3_ggga(x1, x2, x4)
U5_gga(x1, x2, x3)  =  U5_gga(x1, x3)
quotD_in_ga(x1, x2)  =  quotD_in_ga(x1)
quotD_out_ga(x1, x2)  =  quotD_out_ga(x1, x2)
U12_ga(x1, x2, x3)  =  U12_ga(x1, x3)
U6_gga(x1, x2, x3)  =  U6_gga(x1, x3)
quotE_in_ga(x1, x2)  =  quotE_in_ga(x1)
quotE_out_ga(x1, x2)  =  quotE_out_ga(x1, x2)
U13_ga(x1, x2, x3)  =  U13_ga(x1, x3)
U7_gga(x1, x2, x3)  =  U7_gga(x1, x3)
quotF_in_ga(x1, x2)  =  quotF_in_ga(x1)
quotF_out_ga(x1, x2)  =  quotF_out_ga(x1, x2)
U14_ga(x1, x2, x3)  =  U14_ga(x1, x3)
U8_gga(x1, x2, x3)  =  U8_gga(x1, x3)
quotG_in_ga(x1, x2)  =  quotG_in_ga(x1)
quotG_out_ga(x1, x2)  =  quotG_out_ga(x1, x2)
U15_ga(x1, x2, x3)  =  U15_ga(x1, x3)
U9_gga(x1, x2, x3)  =  U9_gga(x1, x3)
quotH_in_ga(x1, x2)  =  quotH_in_ga(x1)
quotH_out_ga(x1, x2)  =  quotH_out_ga(x1, x2)
U16_ga(x1, x2, x3)  =  U16_ga(x1, x3)
U10_gga(x1, x2, x3)  =  U10_gga(x1, x3)
quotI_in_ga(x1, x2)  =  quotI_in_ga(x1)
quotI_out_ga(x1, x2)  =  quotI_out_ga(x1, x2)
U17_ga(x1, x2, x3)  =  U17_ga(x1, x3)
U11_gga(x1, x2, x3)  =  U11_gga(x1, x3)
quotJ_in_ga(x1, x2)  =  quotJ_in_ga(x1)
quotJ_out_ga(x1, x2)  =  quotJ_out_ga(x1, x2)
U18_ga(x1, x2, x3)  =  U18_ga(x1, x3)
divA_out_gga(x1, x2, x3)  =  divA_out_gga(x1, x2, x3)

(3) DependencyPairsProof (EQUIVALENT transformation)

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

DIVA_IN_GGA(T7, T8, T10) → U1_GGA(T7, T8, T10, quotB_in_gga(T7, T8, T10))
DIVA_IN_GGA(T7, T8, T10) → QUOTB_IN_GGA(T7, T8, T10)
QUOTB_IN_GGA(s(s(s(s(s(s(s(s(T189)))))))), s(s(s(s(s(s(s(s(T190)))))))), T192) → U4_GGA(T189, T190, T192, quotC_in_ggga(T189, T190, s(s(s(s(s(s(s(T190))))))), T192))
QUOTB_IN_GGA(s(s(s(s(s(s(s(s(T189)))))))), s(s(s(s(s(s(s(s(T190)))))))), T192) → QUOTC_IN_GGGA(T189, T190, s(s(s(s(s(s(s(T190))))))), T192)
QUOTC_IN_GGGA(s(T226), s(T227), T228, T230) → U2_GGGA(T226, T227, T228, T230, quotC_in_ggga(T226, T227, T228, T230))
QUOTC_IN_GGGA(s(T226), s(T227), T228, T230) → QUOTC_IN_GGGA(T226, T227, T228, T230)
QUOTC_IN_GGGA(T241, 0, T242, s(T244)) → U3_GGGA(T241, T242, T244, quotB_in_gga(T241, s(T242), T244))
QUOTC_IN_GGGA(T241, 0, T242, s(T244)) → QUOTB_IN_GGA(T241, s(T242), T244)
QUOTB_IN_GGA(s(s(s(s(s(s(s(T251))))))), s(s(s(s(s(s(s(0))))))), s(T253)) → U5_GGA(T251, T253, quotD_in_ga(T251, T253))
QUOTB_IN_GGA(s(s(s(s(s(s(s(T251))))))), s(s(s(s(s(s(s(0))))))), s(T253)) → QUOTD_IN_GA(T251, T253)
QUOTD_IN_GA(s(s(s(s(s(s(s(T336))))))), s(T338)) → U12_GA(T336, T338, quotD_in_ga(T336, T338))
QUOTD_IN_GA(s(s(s(s(s(s(s(T336))))))), s(T338)) → QUOTD_IN_GA(T336, T338)
QUOTB_IN_GGA(s(s(s(s(s(s(T350)))))), s(s(s(s(s(s(0)))))), s(T352)) → U6_GGA(T350, T352, quotE_in_ga(T350, T352))
QUOTB_IN_GGA(s(s(s(s(s(s(T350)))))), s(s(s(s(s(s(0)))))), s(T352)) → QUOTE_IN_GA(T350, T352)
QUOTE_IN_GA(s(s(s(s(s(s(T424)))))), s(T426)) → U13_GA(T424, T426, quotE_in_ga(T424, T426))
QUOTE_IN_GA(s(s(s(s(s(s(T424)))))), s(T426)) → QUOTE_IN_GA(T424, T426)
QUOTB_IN_GGA(s(s(s(s(s(T437))))), s(s(s(s(s(0))))), s(T439)) → U7_GGA(T437, T439, quotF_in_ga(T437, T439))
QUOTB_IN_GGA(s(s(s(s(s(T437))))), s(s(s(s(s(0))))), s(T439)) → QUOTF_IN_GA(T437, T439)
QUOTF_IN_GA(s(s(s(s(s(T500))))), s(T502)) → U14_GA(T500, T502, quotF_in_ga(T500, T502))
QUOTF_IN_GA(s(s(s(s(s(T500))))), s(T502)) → QUOTF_IN_GA(T500, T502)
QUOTB_IN_GGA(s(s(s(s(T512)))), s(s(s(s(0)))), s(T514)) → U8_GGA(T512, T514, quotG_in_ga(T512, T514))
QUOTB_IN_GGA(s(s(s(s(T512)))), s(s(s(s(0)))), s(T514)) → QUOTG_IN_GA(T512, T514)
QUOTG_IN_GA(s(s(s(s(T564)))), s(T566)) → U15_GA(T564, T566, quotG_in_ga(T564, T566))
QUOTG_IN_GA(s(s(s(s(T564)))), s(T566)) → QUOTG_IN_GA(T564, T566)
QUOTB_IN_GGA(s(s(s(T575))), s(s(s(0))), s(T577)) → U9_GGA(T575, T577, quotH_in_ga(T575, T577))
QUOTB_IN_GGA(s(s(s(T575))), s(s(s(0))), s(T577)) → QUOTH_IN_GA(T575, T577)
QUOTH_IN_GA(s(s(s(T616))), s(T618)) → U16_GA(T616, T618, quotH_in_ga(T616, T618))
QUOTH_IN_GA(s(s(s(T616))), s(T618)) → QUOTH_IN_GA(T616, T618)
QUOTB_IN_GGA(s(s(T626)), s(s(0)), s(T628)) → U10_GGA(T626, T628, quotI_in_ga(T626, T628))
QUOTB_IN_GGA(s(s(T626)), s(s(0)), s(T628)) → QUOTI_IN_GA(T626, T628)
QUOTI_IN_GA(s(s(T656)), s(T658)) → U17_GA(T656, T658, quotI_in_ga(T656, T658))
QUOTI_IN_GA(s(s(T656)), s(T658)) → QUOTI_IN_GA(T656, T658)
QUOTB_IN_GGA(s(T665), s(0), s(T667)) → U11_GGA(T665, T667, quotJ_in_ga(T665, T667))
QUOTB_IN_GGA(s(T665), s(0), s(T667)) → QUOTJ_IN_GA(T665, T667)
QUOTJ_IN_GA(s(T684), s(T686)) → U18_GA(T684, T686, quotJ_in_ga(T684, T686))
QUOTJ_IN_GA(s(T684), s(T686)) → QUOTJ_IN_GA(T684, T686)

The TRS R consists of the following rules:

divA_in_gga(T7, T8, T10) → U1_gga(T7, T8, T10, quotB_in_gga(T7, T8, T10))
quotB_in_gga(0, s(T15), 0) → quotB_out_gga(0, s(T15), 0)
quotB_in_gga(s(0), s(s(T38)), 0) → quotB_out_gga(s(0), s(s(T38)), 0)
quotB_in_gga(s(s(0)), s(s(s(T61))), 0) → quotB_out_gga(s(s(0)), s(s(s(T61))), 0)
quotB_in_gga(s(s(s(0))), s(s(s(s(T84)))), 0) → quotB_out_gga(s(s(s(0))), s(s(s(s(T84)))), 0)
quotB_in_gga(s(s(s(s(0)))), s(s(s(s(s(T107))))), 0) → quotB_out_gga(s(s(s(s(0)))), s(s(s(s(s(T107))))), 0)
quotB_in_gga(s(s(s(s(s(0))))), s(s(s(s(s(s(T130)))))), 0) → quotB_out_gga(s(s(s(s(s(0))))), s(s(s(s(s(s(T130)))))), 0)
quotB_in_gga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T153))))))), 0) → quotB_out_gga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T153))))))), 0)
quotB_in_gga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(T176)))))))), 0) → quotB_out_gga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(T176)))))))), 0)
quotB_in_gga(s(s(s(s(s(s(s(s(T189)))))))), s(s(s(s(s(s(s(s(T190)))))))), T192) → U4_gga(T189, T190, T192, quotC_in_ggga(T189, T190, s(s(s(s(s(s(s(T190))))))), T192))
quotC_in_ggga(0, s(T208), T209, 0) → quotC_out_ggga(0, s(T208), T209, 0)
quotC_in_ggga(s(T226), s(T227), T228, T230) → U2_ggga(T226, T227, T228, T230, quotC_in_ggga(T226, T227, T228, T230))
quotC_in_ggga(T241, 0, T242, s(T244)) → U3_ggga(T241, T242, T244, quotB_in_gga(T241, s(T242), T244))
quotB_in_gga(s(s(s(s(s(s(s(T251))))))), s(s(s(s(s(s(s(0))))))), s(T253)) → U5_gga(T251, T253, quotD_in_ga(T251, T253))
quotD_in_ga(0, 0) → quotD_out_ga(0, 0)
quotD_in_ga(s(0), 0) → quotD_out_ga(s(0), 0)
quotD_in_ga(s(s(0)), 0) → quotD_out_ga(s(s(0)), 0)
quotD_in_ga(s(s(s(0))), 0) → quotD_out_ga(s(s(s(0))), 0)
quotD_in_ga(s(s(s(s(0)))), 0) → quotD_out_ga(s(s(s(s(0)))), 0)
quotD_in_ga(s(s(s(s(s(0))))), 0) → quotD_out_ga(s(s(s(s(s(0))))), 0)
quotD_in_ga(s(s(s(s(s(s(0)))))), 0) → quotD_out_ga(s(s(s(s(s(s(0)))))), 0)
quotD_in_ga(s(s(s(s(s(s(s(T336))))))), s(T338)) → U12_ga(T336, T338, quotD_in_ga(T336, T338))
U12_ga(T336, T338, quotD_out_ga(T336, T338)) → quotD_out_ga(s(s(s(s(s(s(s(T336))))))), s(T338))
U5_gga(T251, T253, quotD_out_ga(T251, T253)) → quotB_out_gga(s(s(s(s(s(s(s(T251))))))), s(s(s(s(s(s(s(0))))))), s(T253))
quotB_in_gga(s(s(s(s(s(s(T350)))))), s(s(s(s(s(s(0)))))), s(T352)) → U6_gga(T350, T352, quotE_in_ga(T350, T352))
quotE_in_ga(0, 0) → quotE_out_ga(0, 0)
quotE_in_ga(s(0), 0) → quotE_out_ga(s(0), 0)
quotE_in_ga(s(s(0)), 0) → quotE_out_ga(s(s(0)), 0)
quotE_in_ga(s(s(s(0))), 0) → quotE_out_ga(s(s(s(0))), 0)
quotE_in_ga(s(s(s(s(0)))), 0) → quotE_out_ga(s(s(s(s(0)))), 0)
quotE_in_ga(s(s(s(s(s(0))))), 0) → quotE_out_ga(s(s(s(s(s(0))))), 0)
quotE_in_ga(s(s(s(s(s(s(T424)))))), s(T426)) → U13_ga(T424, T426, quotE_in_ga(T424, T426))
U13_ga(T424, T426, quotE_out_ga(T424, T426)) → quotE_out_ga(s(s(s(s(s(s(T424)))))), s(T426))
U6_gga(T350, T352, quotE_out_ga(T350, T352)) → quotB_out_gga(s(s(s(s(s(s(T350)))))), s(s(s(s(s(s(0)))))), s(T352))
quotB_in_gga(s(s(s(s(s(T437))))), s(s(s(s(s(0))))), s(T439)) → U7_gga(T437, T439, quotF_in_ga(T437, T439))
quotF_in_ga(0, 0) → quotF_out_ga(0, 0)
quotF_in_ga(s(0), 0) → quotF_out_ga(s(0), 0)
quotF_in_ga(s(s(0)), 0) → quotF_out_ga(s(s(0)), 0)
quotF_in_ga(s(s(s(0))), 0) → quotF_out_ga(s(s(s(0))), 0)
quotF_in_ga(s(s(s(s(0)))), 0) → quotF_out_ga(s(s(s(s(0)))), 0)
quotF_in_ga(s(s(s(s(s(T500))))), s(T502)) → U14_ga(T500, T502, quotF_in_ga(T500, T502))
U14_ga(T500, T502, quotF_out_ga(T500, T502)) → quotF_out_ga(s(s(s(s(s(T500))))), s(T502))
U7_gga(T437, T439, quotF_out_ga(T437, T439)) → quotB_out_gga(s(s(s(s(s(T437))))), s(s(s(s(s(0))))), s(T439))
quotB_in_gga(s(s(s(s(T512)))), s(s(s(s(0)))), s(T514)) → U8_gga(T512, T514, quotG_in_ga(T512, T514))
quotG_in_ga(0, 0) → quotG_out_ga(0, 0)
quotG_in_ga(s(0), 0) → quotG_out_ga(s(0), 0)
quotG_in_ga(s(s(0)), 0) → quotG_out_ga(s(s(0)), 0)
quotG_in_ga(s(s(s(0))), 0) → quotG_out_ga(s(s(s(0))), 0)
quotG_in_ga(s(s(s(s(T564)))), s(T566)) → U15_ga(T564, T566, quotG_in_ga(T564, T566))
U15_ga(T564, T566, quotG_out_ga(T564, T566)) → quotG_out_ga(s(s(s(s(T564)))), s(T566))
U8_gga(T512, T514, quotG_out_ga(T512, T514)) → quotB_out_gga(s(s(s(s(T512)))), s(s(s(s(0)))), s(T514))
quotB_in_gga(s(s(s(T575))), s(s(s(0))), s(T577)) → U9_gga(T575, T577, quotH_in_ga(T575, T577))
quotH_in_ga(0, 0) → quotH_out_ga(0, 0)
quotH_in_ga(s(0), 0) → quotH_out_ga(s(0), 0)
quotH_in_ga(s(s(0)), 0) → quotH_out_ga(s(s(0)), 0)
quotH_in_ga(s(s(s(T616))), s(T618)) → U16_ga(T616, T618, quotH_in_ga(T616, T618))
U16_ga(T616, T618, quotH_out_ga(T616, T618)) → quotH_out_ga(s(s(s(T616))), s(T618))
U9_gga(T575, T577, quotH_out_ga(T575, T577)) → quotB_out_gga(s(s(s(T575))), s(s(s(0))), s(T577))
quotB_in_gga(s(s(T626)), s(s(0)), s(T628)) → U10_gga(T626, T628, quotI_in_ga(T626, T628))
quotI_in_ga(0, 0) → quotI_out_ga(0, 0)
quotI_in_ga(s(0), 0) → quotI_out_ga(s(0), 0)
quotI_in_ga(s(s(T656)), s(T658)) → U17_ga(T656, T658, quotI_in_ga(T656, T658))
U17_ga(T656, T658, quotI_out_ga(T656, T658)) → quotI_out_ga(s(s(T656)), s(T658))
U10_gga(T626, T628, quotI_out_ga(T626, T628)) → quotB_out_gga(s(s(T626)), s(s(0)), s(T628))
quotB_in_gga(s(T665), s(0), s(T667)) → U11_gga(T665, T667, quotJ_in_ga(T665, T667))
quotJ_in_ga(0, 0) → quotJ_out_ga(0, 0)
quotJ_in_ga(s(T684), s(T686)) → U18_ga(T684, T686, quotJ_in_ga(T684, T686))
U18_ga(T684, T686, quotJ_out_ga(T684, T686)) → quotJ_out_ga(s(T684), s(T686))
U11_gga(T665, T667, quotJ_out_ga(T665, T667)) → quotB_out_gga(s(T665), s(0), s(T667))
U3_ggga(T241, T242, T244, quotB_out_gga(T241, s(T242), T244)) → quotC_out_ggga(T241, 0, T242, s(T244))
U2_ggga(T226, T227, T228, T230, quotC_out_ggga(T226, T227, T228, T230)) → quotC_out_ggga(s(T226), s(T227), T228, T230)
U4_gga(T189, T190, T192, quotC_out_ggga(T189, T190, s(s(s(s(s(s(s(T190))))))), T192)) → quotB_out_gga(s(s(s(s(s(s(s(s(T189)))))))), s(s(s(s(s(s(s(s(T190)))))))), T192)
U1_gga(T7, T8, T10, quotB_out_gga(T7, T8, T10)) → divA_out_gga(T7, T8, T10)

The argument filtering Pi contains the following mapping:
divA_in_gga(x1, x2, x3)  =  divA_in_gga(x1, x2)
U1_gga(x1, x2, x3, x4)  =  U1_gga(x1, x2, x4)
quotB_in_gga(x1, x2, x3)  =  quotB_in_gga(x1, x2)
0  =  0
s(x1)  =  s(x1)
quotB_out_gga(x1, x2, x3)  =  quotB_out_gga(x1, x2, x3)
U4_gga(x1, x2, x3, x4)  =  U4_gga(x1, x2, x4)
quotC_in_ggga(x1, x2, x3, x4)  =  quotC_in_ggga(x1, x2, x3)
quotC_out_ggga(x1, x2, x3, x4)  =  quotC_out_ggga(x1, x2, x3, x4)
U2_ggga(x1, x2, x3, x4, x5)  =  U2_ggga(x1, x2, x3, x5)
U3_ggga(x1, x2, x3, x4)  =  U3_ggga(x1, x2, x4)
U5_gga(x1, x2, x3)  =  U5_gga(x1, x3)
quotD_in_ga(x1, x2)  =  quotD_in_ga(x1)
quotD_out_ga(x1, x2)  =  quotD_out_ga(x1, x2)
U12_ga(x1, x2, x3)  =  U12_ga(x1, x3)
U6_gga(x1, x2, x3)  =  U6_gga(x1, x3)
quotE_in_ga(x1, x2)  =  quotE_in_ga(x1)
quotE_out_ga(x1, x2)  =  quotE_out_ga(x1, x2)
U13_ga(x1, x2, x3)  =  U13_ga(x1, x3)
U7_gga(x1, x2, x3)  =  U7_gga(x1, x3)
quotF_in_ga(x1, x2)  =  quotF_in_ga(x1)
quotF_out_ga(x1, x2)  =  quotF_out_ga(x1, x2)
U14_ga(x1, x2, x3)  =  U14_ga(x1, x3)
U8_gga(x1, x2, x3)  =  U8_gga(x1, x3)
quotG_in_ga(x1, x2)  =  quotG_in_ga(x1)
quotG_out_ga(x1, x2)  =  quotG_out_ga(x1, x2)
U15_ga(x1, x2, x3)  =  U15_ga(x1, x3)
U9_gga(x1, x2, x3)  =  U9_gga(x1, x3)
quotH_in_ga(x1, x2)  =  quotH_in_ga(x1)
quotH_out_ga(x1, x2)  =  quotH_out_ga(x1, x2)
U16_ga(x1, x2, x3)  =  U16_ga(x1, x3)
U10_gga(x1, x2, x3)  =  U10_gga(x1, x3)
quotI_in_ga(x1, x2)  =  quotI_in_ga(x1)
quotI_out_ga(x1, x2)  =  quotI_out_ga(x1, x2)
U17_ga(x1, x2, x3)  =  U17_ga(x1, x3)
U11_gga(x1, x2, x3)  =  U11_gga(x1, x3)
quotJ_in_ga(x1, x2)  =  quotJ_in_ga(x1)
quotJ_out_ga(x1, x2)  =  quotJ_out_ga(x1, x2)
U18_ga(x1, x2, x3)  =  U18_ga(x1, x3)
divA_out_gga(x1, x2, x3)  =  divA_out_gga(x1, x2, x3)
DIVA_IN_GGA(x1, x2, x3)  =  DIVA_IN_GGA(x1, x2)
U1_GGA(x1, x2, x3, x4)  =  U1_GGA(x1, x2, x4)
QUOTB_IN_GGA(x1, x2, x3)  =  QUOTB_IN_GGA(x1, x2)
U4_GGA(x1, x2, x3, x4)  =  U4_GGA(x1, x2, x4)
QUOTC_IN_GGGA(x1, x2, x3, x4)  =  QUOTC_IN_GGGA(x1, x2, x3)
U2_GGGA(x1, x2, x3, x4, x5)  =  U2_GGGA(x1, x2, x3, x5)
U3_GGGA(x1, x2, x3, x4)  =  U3_GGGA(x1, x2, x4)
U5_GGA(x1, x2, x3)  =  U5_GGA(x1, x3)
QUOTD_IN_GA(x1, x2)  =  QUOTD_IN_GA(x1)
U12_GA(x1, x2, x3)  =  U12_GA(x1, x3)
U6_GGA(x1, x2, x3)  =  U6_GGA(x1, x3)
QUOTE_IN_GA(x1, x2)  =  QUOTE_IN_GA(x1)
U13_GA(x1, x2, x3)  =  U13_GA(x1, x3)
U7_GGA(x1, x2, x3)  =  U7_GGA(x1, x3)
QUOTF_IN_GA(x1, x2)  =  QUOTF_IN_GA(x1)
U14_GA(x1, x2, x3)  =  U14_GA(x1, x3)
U8_GGA(x1, x2, x3)  =  U8_GGA(x1, x3)
QUOTG_IN_GA(x1, x2)  =  QUOTG_IN_GA(x1)
U15_GA(x1, x2, x3)  =  U15_GA(x1, x3)
U9_GGA(x1, x2, x3)  =  U9_GGA(x1, x3)
QUOTH_IN_GA(x1, x2)  =  QUOTH_IN_GA(x1)
U16_GA(x1, x2, x3)  =  U16_GA(x1, x3)
U10_GGA(x1, x2, x3)  =  U10_GGA(x1, x3)
QUOTI_IN_GA(x1, x2)  =  QUOTI_IN_GA(x1)
U17_GA(x1, x2, x3)  =  U17_GA(x1, x3)
U11_GGA(x1, x2, x3)  =  U11_GGA(x1, x3)
QUOTJ_IN_GA(x1, x2)  =  QUOTJ_IN_GA(x1)
U18_GA(x1, x2, x3)  =  U18_GA(x1, x3)

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

(4) Obligation:

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

DIVA_IN_GGA(T7, T8, T10) → U1_GGA(T7, T8, T10, quotB_in_gga(T7, T8, T10))
DIVA_IN_GGA(T7, T8, T10) → QUOTB_IN_GGA(T7, T8, T10)
QUOTB_IN_GGA(s(s(s(s(s(s(s(s(T189)))))))), s(s(s(s(s(s(s(s(T190)))))))), T192) → U4_GGA(T189, T190, T192, quotC_in_ggga(T189, T190, s(s(s(s(s(s(s(T190))))))), T192))
QUOTB_IN_GGA(s(s(s(s(s(s(s(s(T189)))))))), s(s(s(s(s(s(s(s(T190)))))))), T192) → QUOTC_IN_GGGA(T189, T190, s(s(s(s(s(s(s(T190))))))), T192)
QUOTC_IN_GGGA(s(T226), s(T227), T228, T230) → U2_GGGA(T226, T227, T228, T230, quotC_in_ggga(T226, T227, T228, T230))
QUOTC_IN_GGGA(s(T226), s(T227), T228, T230) → QUOTC_IN_GGGA(T226, T227, T228, T230)
QUOTC_IN_GGGA(T241, 0, T242, s(T244)) → U3_GGGA(T241, T242, T244, quotB_in_gga(T241, s(T242), T244))
QUOTC_IN_GGGA(T241, 0, T242, s(T244)) → QUOTB_IN_GGA(T241, s(T242), T244)
QUOTB_IN_GGA(s(s(s(s(s(s(s(T251))))))), s(s(s(s(s(s(s(0))))))), s(T253)) → U5_GGA(T251, T253, quotD_in_ga(T251, T253))
QUOTB_IN_GGA(s(s(s(s(s(s(s(T251))))))), s(s(s(s(s(s(s(0))))))), s(T253)) → QUOTD_IN_GA(T251, T253)
QUOTD_IN_GA(s(s(s(s(s(s(s(T336))))))), s(T338)) → U12_GA(T336, T338, quotD_in_ga(T336, T338))
QUOTD_IN_GA(s(s(s(s(s(s(s(T336))))))), s(T338)) → QUOTD_IN_GA(T336, T338)
QUOTB_IN_GGA(s(s(s(s(s(s(T350)))))), s(s(s(s(s(s(0)))))), s(T352)) → U6_GGA(T350, T352, quotE_in_ga(T350, T352))
QUOTB_IN_GGA(s(s(s(s(s(s(T350)))))), s(s(s(s(s(s(0)))))), s(T352)) → QUOTE_IN_GA(T350, T352)
QUOTE_IN_GA(s(s(s(s(s(s(T424)))))), s(T426)) → U13_GA(T424, T426, quotE_in_ga(T424, T426))
QUOTE_IN_GA(s(s(s(s(s(s(T424)))))), s(T426)) → QUOTE_IN_GA(T424, T426)
QUOTB_IN_GGA(s(s(s(s(s(T437))))), s(s(s(s(s(0))))), s(T439)) → U7_GGA(T437, T439, quotF_in_ga(T437, T439))
QUOTB_IN_GGA(s(s(s(s(s(T437))))), s(s(s(s(s(0))))), s(T439)) → QUOTF_IN_GA(T437, T439)
QUOTF_IN_GA(s(s(s(s(s(T500))))), s(T502)) → U14_GA(T500, T502, quotF_in_ga(T500, T502))
QUOTF_IN_GA(s(s(s(s(s(T500))))), s(T502)) → QUOTF_IN_GA(T500, T502)
QUOTB_IN_GGA(s(s(s(s(T512)))), s(s(s(s(0)))), s(T514)) → U8_GGA(T512, T514, quotG_in_ga(T512, T514))
QUOTB_IN_GGA(s(s(s(s(T512)))), s(s(s(s(0)))), s(T514)) → QUOTG_IN_GA(T512, T514)
QUOTG_IN_GA(s(s(s(s(T564)))), s(T566)) → U15_GA(T564, T566, quotG_in_ga(T564, T566))
QUOTG_IN_GA(s(s(s(s(T564)))), s(T566)) → QUOTG_IN_GA(T564, T566)
QUOTB_IN_GGA(s(s(s(T575))), s(s(s(0))), s(T577)) → U9_GGA(T575, T577, quotH_in_ga(T575, T577))
QUOTB_IN_GGA(s(s(s(T575))), s(s(s(0))), s(T577)) → QUOTH_IN_GA(T575, T577)
QUOTH_IN_GA(s(s(s(T616))), s(T618)) → U16_GA(T616, T618, quotH_in_ga(T616, T618))
QUOTH_IN_GA(s(s(s(T616))), s(T618)) → QUOTH_IN_GA(T616, T618)
QUOTB_IN_GGA(s(s(T626)), s(s(0)), s(T628)) → U10_GGA(T626, T628, quotI_in_ga(T626, T628))
QUOTB_IN_GGA(s(s(T626)), s(s(0)), s(T628)) → QUOTI_IN_GA(T626, T628)
QUOTI_IN_GA(s(s(T656)), s(T658)) → U17_GA(T656, T658, quotI_in_ga(T656, T658))
QUOTI_IN_GA(s(s(T656)), s(T658)) → QUOTI_IN_GA(T656, T658)
QUOTB_IN_GGA(s(T665), s(0), s(T667)) → U11_GGA(T665, T667, quotJ_in_ga(T665, T667))
QUOTB_IN_GGA(s(T665), s(0), s(T667)) → QUOTJ_IN_GA(T665, T667)
QUOTJ_IN_GA(s(T684), s(T686)) → U18_GA(T684, T686, quotJ_in_ga(T684, T686))
QUOTJ_IN_GA(s(T684), s(T686)) → QUOTJ_IN_GA(T684, T686)

The TRS R consists of the following rules:

divA_in_gga(T7, T8, T10) → U1_gga(T7, T8, T10, quotB_in_gga(T7, T8, T10))
quotB_in_gga(0, s(T15), 0) → quotB_out_gga(0, s(T15), 0)
quotB_in_gga(s(0), s(s(T38)), 0) → quotB_out_gga(s(0), s(s(T38)), 0)
quotB_in_gga(s(s(0)), s(s(s(T61))), 0) → quotB_out_gga(s(s(0)), s(s(s(T61))), 0)
quotB_in_gga(s(s(s(0))), s(s(s(s(T84)))), 0) → quotB_out_gga(s(s(s(0))), s(s(s(s(T84)))), 0)
quotB_in_gga(s(s(s(s(0)))), s(s(s(s(s(T107))))), 0) → quotB_out_gga(s(s(s(s(0)))), s(s(s(s(s(T107))))), 0)
quotB_in_gga(s(s(s(s(s(0))))), s(s(s(s(s(s(T130)))))), 0) → quotB_out_gga(s(s(s(s(s(0))))), s(s(s(s(s(s(T130)))))), 0)
quotB_in_gga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T153))))))), 0) → quotB_out_gga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T153))))))), 0)
quotB_in_gga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(T176)))))))), 0) → quotB_out_gga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(T176)))))))), 0)
quotB_in_gga(s(s(s(s(s(s(s(s(T189)))))))), s(s(s(s(s(s(s(s(T190)))))))), T192) → U4_gga(T189, T190, T192, quotC_in_ggga(T189, T190, s(s(s(s(s(s(s(T190))))))), T192))
quotC_in_ggga(0, s(T208), T209, 0) → quotC_out_ggga(0, s(T208), T209, 0)
quotC_in_ggga(s(T226), s(T227), T228, T230) → U2_ggga(T226, T227, T228, T230, quotC_in_ggga(T226, T227, T228, T230))
quotC_in_ggga(T241, 0, T242, s(T244)) → U3_ggga(T241, T242, T244, quotB_in_gga(T241, s(T242), T244))
quotB_in_gga(s(s(s(s(s(s(s(T251))))))), s(s(s(s(s(s(s(0))))))), s(T253)) → U5_gga(T251, T253, quotD_in_ga(T251, T253))
quotD_in_ga(0, 0) → quotD_out_ga(0, 0)
quotD_in_ga(s(0), 0) → quotD_out_ga(s(0), 0)
quotD_in_ga(s(s(0)), 0) → quotD_out_ga(s(s(0)), 0)
quotD_in_ga(s(s(s(0))), 0) → quotD_out_ga(s(s(s(0))), 0)
quotD_in_ga(s(s(s(s(0)))), 0) → quotD_out_ga(s(s(s(s(0)))), 0)
quotD_in_ga(s(s(s(s(s(0))))), 0) → quotD_out_ga(s(s(s(s(s(0))))), 0)
quotD_in_ga(s(s(s(s(s(s(0)))))), 0) → quotD_out_ga(s(s(s(s(s(s(0)))))), 0)
quotD_in_ga(s(s(s(s(s(s(s(T336))))))), s(T338)) → U12_ga(T336, T338, quotD_in_ga(T336, T338))
U12_ga(T336, T338, quotD_out_ga(T336, T338)) → quotD_out_ga(s(s(s(s(s(s(s(T336))))))), s(T338))
U5_gga(T251, T253, quotD_out_ga(T251, T253)) → quotB_out_gga(s(s(s(s(s(s(s(T251))))))), s(s(s(s(s(s(s(0))))))), s(T253))
quotB_in_gga(s(s(s(s(s(s(T350)))))), s(s(s(s(s(s(0)))))), s(T352)) → U6_gga(T350, T352, quotE_in_ga(T350, T352))
quotE_in_ga(0, 0) → quotE_out_ga(0, 0)
quotE_in_ga(s(0), 0) → quotE_out_ga(s(0), 0)
quotE_in_ga(s(s(0)), 0) → quotE_out_ga(s(s(0)), 0)
quotE_in_ga(s(s(s(0))), 0) → quotE_out_ga(s(s(s(0))), 0)
quotE_in_ga(s(s(s(s(0)))), 0) → quotE_out_ga(s(s(s(s(0)))), 0)
quotE_in_ga(s(s(s(s(s(0))))), 0) → quotE_out_ga(s(s(s(s(s(0))))), 0)
quotE_in_ga(s(s(s(s(s(s(T424)))))), s(T426)) → U13_ga(T424, T426, quotE_in_ga(T424, T426))
U13_ga(T424, T426, quotE_out_ga(T424, T426)) → quotE_out_ga(s(s(s(s(s(s(T424)))))), s(T426))
U6_gga(T350, T352, quotE_out_ga(T350, T352)) → quotB_out_gga(s(s(s(s(s(s(T350)))))), s(s(s(s(s(s(0)))))), s(T352))
quotB_in_gga(s(s(s(s(s(T437))))), s(s(s(s(s(0))))), s(T439)) → U7_gga(T437, T439, quotF_in_ga(T437, T439))
quotF_in_ga(0, 0) → quotF_out_ga(0, 0)
quotF_in_ga(s(0), 0) → quotF_out_ga(s(0), 0)
quotF_in_ga(s(s(0)), 0) → quotF_out_ga(s(s(0)), 0)
quotF_in_ga(s(s(s(0))), 0) → quotF_out_ga(s(s(s(0))), 0)
quotF_in_ga(s(s(s(s(0)))), 0) → quotF_out_ga(s(s(s(s(0)))), 0)
quotF_in_ga(s(s(s(s(s(T500))))), s(T502)) → U14_ga(T500, T502, quotF_in_ga(T500, T502))
U14_ga(T500, T502, quotF_out_ga(T500, T502)) → quotF_out_ga(s(s(s(s(s(T500))))), s(T502))
U7_gga(T437, T439, quotF_out_ga(T437, T439)) → quotB_out_gga(s(s(s(s(s(T437))))), s(s(s(s(s(0))))), s(T439))
quotB_in_gga(s(s(s(s(T512)))), s(s(s(s(0)))), s(T514)) → U8_gga(T512, T514, quotG_in_ga(T512, T514))
quotG_in_ga(0, 0) → quotG_out_ga(0, 0)
quotG_in_ga(s(0), 0) → quotG_out_ga(s(0), 0)
quotG_in_ga(s(s(0)), 0) → quotG_out_ga(s(s(0)), 0)
quotG_in_ga(s(s(s(0))), 0) → quotG_out_ga(s(s(s(0))), 0)
quotG_in_ga(s(s(s(s(T564)))), s(T566)) → U15_ga(T564, T566, quotG_in_ga(T564, T566))
U15_ga(T564, T566, quotG_out_ga(T564, T566)) → quotG_out_ga(s(s(s(s(T564)))), s(T566))
U8_gga(T512, T514, quotG_out_ga(T512, T514)) → quotB_out_gga(s(s(s(s(T512)))), s(s(s(s(0)))), s(T514))
quotB_in_gga(s(s(s(T575))), s(s(s(0))), s(T577)) → U9_gga(T575, T577, quotH_in_ga(T575, T577))
quotH_in_ga(0, 0) → quotH_out_ga(0, 0)
quotH_in_ga(s(0), 0) → quotH_out_ga(s(0), 0)
quotH_in_ga(s(s(0)), 0) → quotH_out_ga(s(s(0)), 0)
quotH_in_ga(s(s(s(T616))), s(T618)) → U16_ga(T616, T618, quotH_in_ga(T616, T618))
U16_ga(T616, T618, quotH_out_ga(T616, T618)) → quotH_out_ga(s(s(s(T616))), s(T618))
U9_gga(T575, T577, quotH_out_ga(T575, T577)) → quotB_out_gga(s(s(s(T575))), s(s(s(0))), s(T577))
quotB_in_gga(s(s(T626)), s(s(0)), s(T628)) → U10_gga(T626, T628, quotI_in_ga(T626, T628))
quotI_in_ga(0, 0) → quotI_out_ga(0, 0)
quotI_in_ga(s(0), 0) → quotI_out_ga(s(0), 0)
quotI_in_ga(s(s(T656)), s(T658)) → U17_ga(T656, T658, quotI_in_ga(T656, T658))
U17_ga(T656, T658, quotI_out_ga(T656, T658)) → quotI_out_ga(s(s(T656)), s(T658))
U10_gga(T626, T628, quotI_out_ga(T626, T628)) → quotB_out_gga(s(s(T626)), s(s(0)), s(T628))
quotB_in_gga(s(T665), s(0), s(T667)) → U11_gga(T665, T667, quotJ_in_ga(T665, T667))
quotJ_in_ga(0, 0) → quotJ_out_ga(0, 0)
quotJ_in_ga(s(T684), s(T686)) → U18_ga(T684, T686, quotJ_in_ga(T684, T686))
U18_ga(T684, T686, quotJ_out_ga(T684, T686)) → quotJ_out_ga(s(T684), s(T686))
U11_gga(T665, T667, quotJ_out_ga(T665, T667)) → quotB_out_gga(s(T665), s(0), s(T667))
U3_ggga(T241, T242, T244, quotB_out_gga(T241, s(T242), T244)) → quotC_out_ggga(T241, 0, T242, s(T244))
U2_ggga(T226, T227, T228, T230, quotC_out_ggga(T226, T227, T228, T230)) → quotC_out_ggga(s(T226), s(T227), T228, T230)
U4_gga(T189, T190, T192, quotC_out_ggga(T189, T190, s(s(s(s(s(s(s(T190))))))), T192)) → quotB_out_gga(s(s(s(s(s(s(s(s(T189)))))))), s(s(s(s(s(s(s(s(T190)))))))), T192)
U1_gga(T7, T8, T10, quotB_out_gga(T7, T8, T10)) → divA_out_gga(T7, T8, T10)

The argument filtering Pi contains the following mapping:
divA_in_gga(x1, x2, x3)  =  divA_in_gga(x1, x2)
U1_gga(x1, x2, x3, x4)  =  U1_gga(x1, x2, x4)
quotB_in_gga(x1, x2, x3)  =  quotB_in_gga(x1, x2)
0  =  0
s(x1)  =  s(x1)
quotB_out_gga(x1, x2, x3)  =  quotB_out_gga(x1, x2, x3)
U4_gga(x1, x2, x3, x4)  =  U4_gga(x1, x2, x4)
quotC_in_ggga(x1, x2, x3, x4)  =  quotC_in_ggga(x1, x2, x3)
quotC_out_ggga(x1, x2, x3, x4)  =  quotC_out_ggga(x1, x2, x3, x4)
U2_ggga(x1, x2, x3, x4, x5)  =  U2_ggga(x1, x2, x3, x5)
U3_ggga(x1, x2, x3, x4)  =  U3_ggga(x1, x2, x4)
U5_gga(x1, x2, x3)  =  U5_gga(x1, x3)
quotD_in_ga(x1, x2)  =  quotD_in_ga(x1)
quotD_out_ga(x1, x2)  =  quotD_out_ga(x1, x2)
U12_ga(x1, x2, x3)  =  U12_ga(x1, x3)
U6_gga(x1, x2, x3)  =  U6_gga(x1, x3)
quotE_in_ga(x1, x2)  =  quotE_in_ga(x1)
quotE_out_ga(x1, x2)  =  quotE_out_ga(x1, x2)
U13_ga(x1, x2, x3)  =  U13_ga(x1, x3)
U7_gga(x1, x2, x3)  =  U7_gga(x1, x3)
quotF_in_ga(x1, x2)  =  quotF_in_ga(x1)
quotF_out_ga(x1, x2)  =  quotF_out_ga(x1, x2)
U14_ga(x1, x2, x3)  =  U14_ga(x1, x3)
U8_gga(x1, x2, x3)  =  U8_gga(x1, x3)
quotG_in_ga(x1, x2)  =  quotG_in_ga(x1)
quotG_out_ga(x1, x2)  =  quotG_out_ga(x1, x2)
U15_ga(x1, x2, x3)  =  U15_ga(x1, x3)
U9_gga(x1, x2, x3)  =  U9_gga(x1, x3)
quotH_in_ga(x1, x2)  =  quotH_in_ga(x1)
quotH_out_ga(x1, x2)  =  quotH_out_ga(x1, x2)
U16_ga(x1, x2, x3)  =  U16_ga(x1, x3)
U10_gga(x1, x2, x3)  =  U10_gga(x1, x3)
quotI_in_ga(x1, x2)  =  quotI_in_ga(x1)
quotI_out_ga(x1, x2)  =  quotI_out_ga(x1, x2)
U17_ga(x1, x2, x3)  =  U17_ga(x1, x3)
U11_gga(x1, x2, x3)  =  U11_gga(x1, x3)
quotJ_in_ga(x1, x2)  =  quotJ_in_ga(x1)
quotJ_out_ga(x1, x2)  =  quotJ_out_ga(x1, x2)
U18_ga(x1, x2, x3)  =  U18_ga(x1, x3)
divA_out_gga(x1, x2, x3)  =  divA_out_gga(x1, x2, x3)
DIVA_IN_GGA(x1, x2, x3)  =  DIVA_IN_GGA(x1, x2)
U1_GGA(x1, x2, x3, x4)  =  U1_GGA(x1, x2, x4)
QUOTB_IN_GGA(x1, x2, x3)  =  QUOTB_IN_GGA(x1, x2)
U4_GGA(x1, x2, x3, x4)  =  U4_GGA(x1, x2, x4)
QUOTC_IN_GGGA(x1, x2, x3, x4)  =  QUOTC_IN_GGGA(x1, x2, x3)
U2_GGGA(x1, x2, x3, x4, x5)  =  U2_GGGA(x1, x2, x3, x5)
U3_GGGA(x1, x2, x3, x4)  =  U3_GGGA(x1, x2, x4)
U5_GGA(x1, x2, x3)  =  U5_GGA(x1, x3)
QUOTD_IN_GA(x1, x2)  =  QUOTD_IN_GA(x1)
U12_GA(x1, x2, x3)  =  U12_GA(x1, x3)
U6_GGA(x1, x2, x3)  =  U6_GGA(x1, x3)
QUOTE_IN_GA(x1, x2)  =  QUOTE_IN_GA(x1)
U13_GA(x1, x2, x3)  =  U13_GA(x1, x3)
U7_GGA(x1, x2, x3)  =  U7_GGA(x1, x3)
QUOTF_IN_GA(x1, x2)  =  QUOTF_IN_GA(x1)
U14_GA(x1, x2, x3)  =  U14_GA(x1, x3)
U8_GGA(x1, x2, x3)  =  U8_GGA(x1, x3)
QUOTG_IN_GA(x1, x2)  =  QUOTG_IN_GA(x1)
U15_GA(x1, x2, x3)  =  U15_GA(x1, x3)
U9_GGA(x1, x2, x3)  =  U9_GGA(x1, x3)
QUOTH_IN_GA(x1, x2)  =  QUOTH_IN_GA(x1)
U16_GA(x1, x2, x3)  =  U16_GA(x1, x3)
U10_GGA(x1, x2, x3)  =  U10_GGA(x1, x3)
QUOTI_IN_GA(x1, x2)  =  QUOTI_IN_GA(x1)
U17_GA(x1, x2, x3)  =  U17_GA(x1, x3)
U11_GGA(x1, x2, x3)  =  U11_GGA(x1, x3)
QUOTJ_IN_GA(x1, x2)  =  QUOTJ_IN_GA(x1)
U18_GA(x1, x2, x3)  =  U18_GA(x1, x3)

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

(5) DependencyGraphProof (EQUIVALENT transformation)

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

(6) Complex Obligation (AND)

(7) Obligation:

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

QUOTJ_IN_GA(s(T684), s(T686)) → QUOTJ_IN_GA(T684, T686)

The TRS R consists of the following rules:

divA_in_gga(T7, T8, T10) → U1_gga(T7, T8, T10, quotB_in_gga(T7, T8, T10))
quotB_in_gga(0, s(T15), 0) → quotB_out_gga(0, s(T15), 0)
quotB_in_gga(s(0), s(s(T38)), 0) → quotB_out_gga(s(0), s(s(T38)), 0)
quotB_in_gga(s(s(0)), s(s(s(T61))), 0) → quotB_out_gga(s(s(0)), s(s(s(T61))), 0)
quotB_in_gga(s(s(s(0))), s(s(s(s(T84)))), 0) → quotB_out_gga(s(s(s(0))), s(s(s(s(T84)))), 0)
quotB_in_gga(s(s(s(s(0)))), s(s(s(s(s(T107))))), 0) → quotB_out_gga(s(s(s(s(0)))), s(s(s(s(s(T107))))), 0)
quotB_in_gga(s(s(s(s(s(0))))), s(s(s(s(s(s(T130)))))), 0) → quotB_out_gga(s(s(s(s(s(0))))), s(s(s(s(s(s(T130)))))), 0)
quotB_in_gga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T153))))))), 0) → quotB_out_gga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T153))))))), 0)
quotB_in_gga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(T176)))))))), 0) → quotB_out_gga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(T176)))))))), 0)
quotB_in_gga(s(s(s(s(s(s(s(s(T189)))))))), s(s(s(s(s(s(s(s(T190)))))))), T192) → U4_gga(T189, T190, T192, quotC_in_ggga(T189, T190, s(s(s(s(s(s(s(T190))))))), T192))
quotC_in_ggga(0, s(T208), T209, 0) → quotC_out_ggga(0, s(T208), T209, 0)
quotC_in_ggga(s(T226), s(T227), T228, T230) → U2_ggga(T226, T227, T228, T230, quotC_in_ggga(T226, T227, T228, T230))
quotC_in_ggga(T241, 0, T242, s(T244)) → U3_ggga(T241, T242, T244, quotB_in_gga(T241, s(T242), T244))
quotB_in_gga(s(s(s(s(s(s(s(T251))))))), s(s(s(s(s(s(s(0))))))), s(T253)) → U5_gga(T251, T253, quotD_in_ga(T251, T253))
quotD_in_ga(0, 0) → quotD_out_ga(0, 0)
quotD_in_ga(s(0), 0) → quotD_out_ga(s(0), 0)
quotD_in_ga(s(s(0)), 0) → quotD_out_ga(s(s(0)), 0)
quotD_in_ga(s(s(s(0))), 0) → quotD_out_ga(s(s(s(0))), 0)
quotD_in_ga(s(s(s(s(0)))), 0) → quotD_out_ga(s(s(s(s(0)))), 0)
quotD_in_ga(s(s(s(s(s(0))))), 0) → quotD_out_ga(s(s(s(s(s(0))))), 0)
quotD_in_ga(s(s(s(s(s(s(0)))))), 0) → quotD_out_ga(s(s(s(s(s(s(0)))))), 0)
quotD_in_ga(s(s(s(s(s(s(s(T336))))))), s(T338)) → U12_ga(T336, T338, quotD_in_ga(T336, T338))
U12_ga(T336, T338, quotD_out_ga(T336, T338)) → quotD_out_ga(s(s(s(s(s(s(s(T336))))))), s(T338))
U5_gga(T251, T253, quotD_out_ga(T251, T253)) → quotB_out_gga(s(s(s(s(s(s(s(T251))))))), s(s(s(s(s(s(s(0))))))), s(T253))
quotB_in_gga(s(s(s(s(s(s(T350)))))), s(s(s(s(s(s(0)))))), s(T352)) → U6_gga(T350, T352, quotE_in_ga(T350, T352))
quotE_in_ga(0, 0) → quotE_out_ga(0, 0)
quotE_in_ga(s(0), 0) → quotE_out_ga(s(0), 0)
quotE_in_ga(s(s(0)), 0) → quotE_out_ga(s(s(0)), 0)
quotE_in_ga(s(s(s(0))), 0) → quotE_out_ga(s(s(s(0))), 0)
quotE_in_ga(s(s(s(s(0)))), 0) → quotE_out_ga(s(s(s(s(0)))), 0)
quotE_in_ga(s(s(s(s(s(0))))), 0) → quotE_out_ga(s(s(s(s(s(0))))), 0)
quotE_in_ga(s(s(s(s(s(s(T424)))))), s(T426)) → U13_ga(T424, T426, quotE_in_ga(T424, T426))
U13_ga(T424, T426, quotE_out_ga(T424, T426)) → quotE_out_ga(s(s(s(s(s(s(T424)))))), s(T426))
U6_gga(T350, T352, quotE_out_ga(T350, T352)) → quotB_out_gga(s(s(s(s(s(s(T350)))))), s(s(s(s(s(s(0)))))), s(T352))
quotB_in_gga(s(s(s(s(s(T437))))), s(s(s(s(s(0))))), s(T439)) → U7_gga(T437, T439, quotF_in_ga(T437, T439))
quotF_in_ga(0, 0) → quotF_out_ga(0, 0)
quotF_in_ga(s(0), 0) → quotF_out_ga(s(0), 0)
quotF_in_ga(s(s(0)), 0) → quotF_out_ga(s(s(0)), 0)
quotF_in_ga(s(s(s(0))), 0) → quotF_out_ga(s(s(s(0))), 0)
quotF_in_ga(s(s(s(s(0)))), 0) → quotF_out_ga(s(s(s(s(0)))), 0)
quotF_in_ga(s(s(s(s(s(T500))))), s(T502)) → U14_ga(T500, T502, quotF_in_ga(T500, T502))
U14_ga(T500, T502, quotF_out_ga(T500, T502)) → quotF_out_ga(s(s(s(s(s(T500))))), s(T502))
U7_gga(T437, T439, quotF_out_ga(T437, T439)) → quotB_out_gga(s(s(s(s(s(T437))))), s(s(s(s(s(0))))), s(T439))
quotB_in_gga(s(s(s(s(T512)))), s(s(s(s(0)))), s(T514)) → U8_gga(T512, T514, quotG_in_ga(T512, T514))
quotG_in_ga(0, 0) → quotG_out_ga(0, 0)
quotG_in_ga(s(0), 0) → quotG_out_ga(s(0), 0)
quotG_in_ga(s(s(0)), 0) → quotG_out_ga(s(s(0)), 0)
quotG_in_ga(s(s(s(0))), 0) → quotG_out_ga(s(s(s(0))), 0)
quotG_in_ga(s(s(s(s(T564)))), s(T566)) → U15_ga(T564, T566, quotG_in_ga(T564, T566))
U15_ga(T564, T566, quotG_out_ga(T564, T566)) → quotG_out_ga(s(s(s(s(T564)))), s(T566))
U8_gga(T512, T514, quotG_out_ga(T512, T514)) → quotB_out_gga(s(s(s(s(T512)))), s(s(s(s(0)))), s(T514))
quotB_in_gga(s(s(s(T575))), s(s(s(0))), s(T577)) → U9_gga(T575, T577, quotH_in_ga(T575, T577))
quotH_in_ga(0, 0) → quotH_out_ga(0, 0)
quotH_in_ga(s(0), 0) → quotH_out_ga(s(0), 0)
quotH_in_ga(s(s(0)), 0) → quotH_out_ga(s(s(0)), 0)
quotH_in_ga(s(s(s(T616))), s(T618)) → U16_ga(T616, T618, quotH_in_ga(T616, T618))
U16_ga(T616, T618, quotH_out_ga(T616, T618)) → quotH_out_ga(s(s(s(T616))), s(T618))
U9_gga(T575, T577, quotH_out_ga(T575, T577)) → quotB_out_gga(s(s(s(T575))), s(s(s(0))), s(T577))
quotB_in_gga(s(s(T626)), s(s(0)), s(T628)) → U10_gga(T626, T628, quotI_in_ga(T626, T628))
quotI_in_ga(0, 0) → quotI_out_ga(0, 0)
quotI_in_ga(s(0), 0) → quotI_out_ga(s(0), 0)
quotI_in_ga(s(s(T656)), s(T658)) → U17_ga(T656, T658, quotI_in_ga(T656, T658))
U17_ga(T656, T658, quotI_out_ga(T656, T658)) → quotI_out_ga(s(s(T656)), s(T658))
U10_gga(T626, T628, quotI_out_ga(T626, T628)) → quotB_out_gga(s(s(T626)), s(s(0)), s(T628))
quotB_in_gga(s(T665), s(0), s(T667)) → U11_gga(T665, T667, quotJ_in_ga(T665, T667))
quotJ_in_ga(0, 0) → quotJ_out_ga(0, 0)
quotJ_in_ga(s(T684), s(T686)) → U18_ga(T684, T686, quotJ_in_ga(T684, T686))
U18_ga(T684, T686, quotJ_out_ga(T684, T686)) → quotJ_out_ga(s(T684), s(T686))
U11_gga(T665, T667, quotJ_out_ga(T665, T667)) → quotB_out_gga(s(T665), s(0), s(T667))
U3_ggga(T241, T242, T244, quotB_out_gga(T241, s(T242), T244)) → quotC_out_ggga(T241, 0, T242, s(T244))
U2_ggga(T226, T227, T228, T230, quotC_out_ggga(T226, T227, T228, T230)) → quotC_out_ggga(s(T226), s(T227), T228, T230)
U4_gga(T189, T190, T192, quotC_out_ggga(T189, T190, s(s(s(s(s(s(s(T190))))))), T192)) → quotB_out_gga(s(s(s(s(s(s(s(s(T189)))))))), s(s(s(s(s(s(s(s(T190)))))))), T192)
U1_gga(T7, T8, T10, quotB_out_gga(T7, T8, T10)) → divA_out_gga(T7, T8, T10)

The argument filtering Pi contains the following mapping:
divA_in_gga(x1, x2, x3)  =  divA_in_gga(x1, x2)
U1_gga(x1, x2, x3, x4)  =  U1_gga(x1, x2, x4)
quotB_in_gga(x1, x2, x3)  =  quotB_in_gga(x1, x2)
0  =  0
s(x1)  =  s(x1)
quotB_out_gga(x1, x2, x3)  =  quotB_out_gga(x1, x2, x3)
U4_gga(x1, x2, x3, x4)  =  U4_gga(x1, x2, x4)
quotC_in_ggga(x1, x2, x3, x4)  =  quotC_in_ggga(x1, x2, x3)
quotC_out_ggga(x1, x2, x3, x4)  =  quotC_out_ggga(x1, x2, x3, x4)
U2_ggga(x1, x2, x3, x4, x5)  =  U2_ggga(x1, x2, x3, x5)
U3_ggga(x1, x2, x3, x4)  =  U3_ggga(x1, x2, x4)
U5_gga(x1, x2, x3)  =  U5_gga(x1, x3)
quotD_in_ga(x1, x2)  =  quotD_in_ga(x1)
quotD_out_ga(x1, x2)  =  quotD_out_ga(x1, x2)
U12_ga(x1, x2, x3)  =  U12_ga(x1, x3)
U6_gga(x1, x2, x3)  =  U6_gga(x1, x3)
quotE_in_ga(x1, x2)  =  quotE_in_ga(x1)
quotE_out_ga(x1, x2)  =  quotE_out_ga(x1, x2)
U13_ga(x1, x2, x3)  =  U13_ga(x1, x3)
U7_gga(x1, x2, x3)  =  U7_gga(x1, x3)
quotF_in_ga(x1, x2)  =  quotF_in_ga(x1)
quotF_out_ga(x1, x2)  =  quotF_out_ga(x1, x2)
U14_ga(x1, x2, x3)  =  U14_ga(x1, x3)
U8_gga(x1, x2, x3)  =  U8_gga(x1, x3)
quotG_in_ga(x1, x2)  =  quotG_in_ga(x1)
quotG_out_ga(x1, x2)  =  quotG_out_ga(x1, x2)
U15_ga(x1, x2, x3)  =  U15_ga(x1, x3)
U9_gga(x1, x2, x3)  =  U9_gga(x1, x3)
quotH_in_ga(x1, x2)  =  quotH_in_ga(x1)
quotH_out_ga(x1, x2)  =  quotH_out_ga(x1, x2)
U16_ga(x1, x2, x3)  =  U16_ga(x1, x3)
U10_gga(x1, x2, x3)  =  U10_gga(x1, x3)
quotI_in_ga(x1, x2)  =  quotI_in_ga(x1)
quotI_out_ga(x1, x2)  =  quotI_out_ga(x1, x2)
U17_ga(x1, x2, x3)  =  U17_ga(x1, x3)
U11_gga(x1, x2, x3)  =  U11_gga(x1, x3)
quotJ_in_ga(x1, x2)  =  quotJ_in_ga(x1)
quotJ_out_ga(x1, x2)  =  quotJ_out_ga(x1, x2)
U18_ga(x1, x2, x3)  =  U18_ga(x1, x3)
divA_out_gga(x1, x2, x3)  =  divA_out_gga(x1, x2, x3)
QUOTJ_IN_GA(x1, x2)  =  QUOTJ_IN_GA(x1)

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

(8) UsableRulesProof (EQUIVALENT transformation)

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

(9) Obligation:

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

QUOTJ_IN_GA(s(T684), s(T686)) → QUOTJ_IN_GA(T684, T686)

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

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

(10) PiDPToQDPProof (SOUND transformation)

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

(11) Obligation:

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

QUOTJ_IN_GA(s(T684)) → QUOTJ_IN_GA(T684)

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

(12) QDPSizeChangeProof (EQUIVALENT transformation)

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

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

  • QUOTJ_IN_GA(s(T684)) → QUOTJ_IN_GA(T684)
    The graph contains the following edges 1 > 1

(13) YES

(14) Obligation:

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

QUOTI_IN_GA(s(s(T656)), s(T658)) → QUOTI_IN_GA(T656, T658)

The TRS R consists of the following rules:

divA_in_gga(T7, T8, T10) → U1_gga(T7, T8, T10, quotB_in_gga(T7, T8, T10))
quotB_in_gga(0, s(T15), 0) → quotB_out_gga(0, s(T15), 0)
quotB_in_gga(s(0), s(s(T38)), 0) → quotB_out_gga(s(0), s(s(T38)), 0)
quotB_in_gga(s(s(0)), s(s(s(T61))), 0) → quotB_out_gga(s(s(0)), s(s(s(T61))), 0)
quotB_in_gga(s(s(s(0))), s(s(s(s(T84)))), 0) → quotB_out_gga(s(s(s(0))), s(s(s(s(T84)))), 0)
quotB_in_gga(s(s(s(s(0)))), s(s(s(s(s(T107))))), 0) → quotB_out_gga(s(s(s(s(0)))), s(s(s(s(s(T107))))), 0)
quotB_in_gga(s(s(s(s(s(0))))), s(s(s(s(s(s(T130)))))), 0) → quotB_out_gga(s(s(s(s(s(0))))), s(s(s(s(s(s(T130)))))), 0)
quotB_in_gga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T153))))))), 0) → quotB_out_gga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T153))))))), 0)
quotB_in_gga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(T176)))))))), 0) → quotB_out_gga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(T176)))))))), 0)
quotB_in_gga(s(s(s(s(s(s(s(s(T189)))))))), s(s(s(s(s(s(s(s(T190)))))))), T192) → U4_gga(T189, T190, T192, quotC_in_ggga(T189, T190, s(s(s(s(s(s(s(T190))))))), T192))
quotC_in_ggga(0, s(T208), T209, 0) → quotC_out_ggga(0, s(T208), T209, 0)
quotC_in_ggga(s(T226), s(T227), T228, T230) → U2_ggga(T226, T227, T228, T230, quotC_in_ggga(T226, T227, T228, T230))
quotC_in_ggga(T241, 0, T242, s(T244)) → U3_ggga(T241, T242, T244, quotB_in_gga(T241, s(T242), T244))
quotB_in_gga(s(s(s(s(s(s(s(T251))))))), s(s(s(s(s(s(s(0))))))), s(T253)) → U5_gga(T251, T253, quotD_in_ga(T251, T253))
quotD_in_ga(0, 0) → quotD_out_ga(0, 0)
quotD_in_ga(s(0), 0) → quotD_out_ga(s(0), 0)
quotD_in_ga(s(s(0)), 0) → quotD_out_ga(s(s(0)), 0)
quotD_in_ga(s(s(s(0))), 0) → quotD_out_ga(s(s(s(0))), 0)
quotD_in_ga(s(s(s(s(0)))), 0) → quotD_out_ga(s(s(s(s(0)))), 0)
quotD_in_ga(s(s(s(s(s(0))))), 0) → quotD_out_ga(s(s(s(s(s(0))))), 0)
quotD_in_ga(s(s(s(s(s(s(0)))))), 0) → quotD_out_ga(s(s(s(s(s(s(0)))))), 0)
quotD_in_ga(s(s(s(s(s(s(s(T336))))))), s(T338)) → U12_ga(T336, T338, quotD_in_ga(T336, T338))
U12_ga(T336, T338, quotD_out_ga(T336, T338)) → quotD_out_ga(s(s(s(s(s(s(s(T336))))))), s(T338))
U5_gga(T251, T253, quotD_out_ga(T251, T253)) → quotB_out_gga(s(s(s(s(s(s(s(T251))))))), s(s(s(s(s(s(s(0))))))), s(T253))
quotB_in_gga(s(s(s(s(s(s(T350)))))), s(s(s(s(s(s(0)))))), s(T352)) → U6_gga(T350, T352, quotE_in_ga(T350, T352))
quotE_in_ga(0, 0) → quotE_out_ga(0, 0)
quotE_in_ga(s(0), 0) → quotE_out_ga(s(0), 0)
quotE_in_ga(s(s(0)), 0) → quotE_out_ga(s(s(0)), 0)
quotE_in_ga(s(s(s(0))), 0) → quotE_out_ga(s(s(s(0))), 0)
quotE_in_ga(s(s(s(s(0)))), 0) → quotE_out_ga(s(s(s(s(0)))), 0)
quotE_in_ga(s(s(s(s(s(0))))), 0) → quotE_out_ga(s(s(s(s(s(0))))), 0)
quotE_in_ga(s(s(s(s(s(s(T424)))))), s(T426)) → U13_ga(T424, T426, quotE_in_ga(T424, T426))
U13_ga(T424, T426, quotE_out_ga(T424, T426)) → quotE_out_ga(s(s(s(s(s(s(T424)))))), s(T426))
U6_gga(T350, T352, quotE_out_ga(T350, T352)) → quotB_out_gga(s(s(s(s(s(s(T350)))))), s(s(s(s(s(s(0)))))), s(T352))
quotB_in_gga(s(s(s(s(s(T437))))), s(s(s(s(s(0))))), s(T439)) → U7_gga(T437, T439, quotF_in_ga(T437, T439))
quotF_in_ga(0, 0) → quotF_out_ga(0, 0)
quotF_in_ga(s(0), 0) → quotF_out_ga(s(0), 0)
quotF_in_ga(s(s(0)), 0) → quotF_out_ga(s(s(0)), 0)
quotF_in_ga(s(s(s(0))), 0) → quotF_out_ga(s(s(s(0))), 0)
quotF_in_ga(s(s(s(s(0)))), 0) → quotF_out_ga(s(s(s(s(0)))), 0)
quotF_in_ga(s(s(s(s(s(T500))))), s(T502)) → U14_ga(T500, T502, quotF_in_ga(T500, T502))
U14_ga(T500, T502, quotF_out_ga(T500, T502)) → quotF_out_ga(s(s(s(s(s(T500))))), s(T502))
U7_gga(T437, T439, quotF_out_ga(T437, T439)) → quotB_out_gga(s(s(s(s(s(T437))))), s(s(s(s(s(0))))), s(T439))
quotB_in_gga(s(s(s(s(T512)))), s(s(s(s(0)))), s(T514)) → U8_gga(T512, T514, quotG_in_ga(T512, T514))
quotG_in_ga(0, 0) → quotG_out_ga(0, 0)
quotG_in_ga(s(0), 0) → quotG_out_ga(s(0), 0)
quotG_in_ga(s(s(0)), 0) → quotG_out_ga(s(s(0)), 0)
quotG_in_ga(s(s(s(0))), 0) → quotG_out_ga(s(s(s(0))), 0)
quotG_in_ga(s(s(s(s(T564)))), s(T566)) → U15_ga(T564, T566, quotG_in_ga(T564, T566))
U15_ga(T564, T566, quotG_out_ga(T564, T566)) → quotG_out_ga(s(s(s(s(T564)))), s(T566))
U8_gga(T512, T514, quotG_out_ga(T512, T514)) → quotB_out_gga(s(s(s(s(T512)))), s(s(s(s(0)))), s(T514))
quotB_in_gga(s(s(s(T575))), s(s(s(0))), s(T577)) → U9_gga(T575, T577, quotH_in_ga(T575, T577))
quotH_in_ga(0, 0) → quotH_out_ga(0, 0)
quotH_in_ga(s(0), 0) → quotH_out_ga(s(0), 0)
quotH_in_ga(s(s(0)), 0) → quotH_out_ga(s(s(0)), 0)
quotH_in_ga(s(s(s(T616))), s(T618)) → U16_ga(T616, T618, quotH_in_ga(T616, T618))
U16_ga(T616, T618, quotH_out_ga(T616, T618)) → quotH_out_ga(s(s(s(T616))), s(T618))
U9_gga(T575, T577, quotH_out_ga(T575, T577)) → quotB_out_gga(s(s(s(T575))), s(s(s(0))), s(T577))
quotB_in_gga(s(s(T626)), s(s(0)), s(T628)) → U10_gga(T626, T628, quotI_in_ga(T626, T628))
quotI_in_ga(0, 0) → quotI_out_ga(0, 0)
quotI_in_ga(s(0), 0) → quotI_out_ga(s(0), 0)
quotI_in_ga(s(s(T656)), s(T658)) → U17_ga(T656, T658, quotI_in_ga(T656, T658))
U17_ga(T656, T658, quotI_out_ga(T656, T658)) → quotI_out_ga(s(s(T656)), s(T658))
U10_gga(T626, T628, quotI_out_ga(T626, T628)) → quotB_out_gga(s(s(T626)), s(s(0)), s(T628))
quotB_in_gga(s(T665), s(0), s(T667)) → U11_gga(T665, T667, quotJ_in_ga(T665, T667))
quotJ_in_ga(0, 0) → quotJ_out_ga(0, 0)
quotJ_in_ga(s(T684), s(T686)) → U18_ga(T684, T686, quotJ_in_ga(T684, T686))
U18_ga(T684, T686, quotJ_out_ga(T684, T686)) → quotJ_out_ga(s(T684), s(T686))
U11_gga(T665, T667, quotJ_out_ga(T665, T667)) → quotB_out_gga(s(T665), s(0), s(T667))
U3_ggga(T241, T242, T244, quotB_out_gga(T241, s(T242), T244)) → quotC_out_ggga(T241, 0, T242, s(T244))
U2_ggga(T226, T227, T228, T230, quotC_out_ggga(T226, T227, T228, T230)) → quotC_out_ggga(s(T226), s(T227), T228, T230)
U4_gga(T189, T190, T192, quotC_out_ggga(T189, T190, s(s(s(s(s(s(s(T190))))))), T192)) → quotB_out_gga(s(s(s(s(s(s(s(s(T189)))))))), s(s(s(s(s(s(s(s(T190)))))))), T192)
U1_gga(T7, T8, T10, quotB_out_gga(T7, T8, T10)) → divA_out_gga(T7, T8, T10)

The argument filtering Pi contains the following mapping:
divA_in_gga(x1, x2, x3)  =  divA_in_gga(x1, x2)
U1_gga(x1, x2, x3, x4)  =  U1_gga(x1, x2, x4)
quotB_in_gga(x1, x2, x3)  =  quotB_in_gga(x1, x2)
0  =  0
s(x1)  =  s(x1)
quotB_out_gga(x1, x2, x3)  =  quotB_out_gga(x1, x2, x3)
U4_gga(x1, x2, x3, x4)  =  U4_gga(x1, x2, x4)
quotC_in_ggga(x1, x2, x3, x4)  =  quotC_in_ggga(x1, x2, x3)
quotC_out_ggga(x1, x2, x3, x4)  =  quotC_out_ggga(x1, x2, x3, x4)
U2_ggga(x1, x2, x3, x4, x5)  =  U2_ggga(x1, x2, x3, x5)
U3_ggga(x1, x2, x3, x4)  =  U3_ggga(x1, x2, x4)
U5_gga(x1, x2, x3)  =  U5_gga(x1, x3)
quotD_in_ga(x1, x2)  =  quotD_in_ga(x1)
quotD_out_ga(x1, x2)  =  quotD_out_ga(x1, x2)
U12_ga(x1, x2, x3)  =  U12_ga(x1, x3)
U6_gga(x1, x2, x3)  =  U6_gga(x1, x3)
quotE_in_ga(x1, x2)  =  quotE_in_ga(x1)
quotE_out_ga(x1, x2)  =  quotE_out_ga(x1, x2)
U13_ga(x1, x2, x3)  =  U13_ga(x1, x3)
U7_gga(x1, x2, x3)  =  U7_gga(x1, x3)
quotF_in_ga(x1, x2)  =  quotF_in_ga(x1)
quotF_out_ga(x1, x2)  =  quotF_out_ga(x1, x2)
U14_ga(x1, x2, x3)  =  U14_ga(x1, x3)
U8_gga(x1, x2, x3)  =  U8_gga(x1, x3)
quotG_in_ga(x1, x2)  =  quotG_in_ga(x1)
quotG_out_ga(x1, x2)  =  quotG_out_ga(x1, x2)
U15_ga(x1, x2, x3)  =  U15_ga(x1, x3)
U9_gga(x1, x2, x3)  =  U9_gga(x1, x3)
quotH_in_ga(x1, x2)  =  quotH_in_ga(x1)
quotH_out_ga(x1, x2)  =  quotH_out_ga(x1, x2)
U16_ga(x1, x2, x3)  =  U16_ga(x1, x3)
U10_gga(x1, x2, x3)  =  U10_gga(x1, x3)
quotI_in_ga(x1, x2)  =  quotI_in_ga(x1)
quotI_out_ga(x1, x2)  =  quotI_out_ga(x1, x2)
U17_ga(x1, x2, x3)  =  U17_ga(x1, x3)
U11_gga(x1, x2, x3)  =  U11_gga(x1, x3)
quotJ_in_ga(x1, x2)  =  quotJ_in_ga(x1)
quotJ_out_ga(x1, x2)  =  quotJ_out_ga(x1, x2)
U18_ga(x1, x2, x3)  =  U18_ga(x1, x3)
divA_out_gga(x1, x2, x3)  =  divA_out_gga(x1, x2, x3)
QUOTI_IN_GA(x1, x2)  =  QUOTI_IN_GA(x1)

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

(15) UsableRulesProof (EQUIVALENT transformation)

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

(16) Obligation:

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

QUOTI_IN_GA(s(s(T656)), s(T658)) → QUOTI_IN_GA(T656, T658)

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

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

(17) PiDPToQDPProof (SOUND transformation)

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

(18) Obligation:

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

QUOTI_IN_GA(s(s(T656))) → QUOTI_IN_GA(T656)

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

(19) QDPSizeChangeProof (EQUIVALENT transformation)

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

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

  • QUOTI_IN_GA(s(s(T656))) → QUOTI_IN_GA(T656)
    The graph contains the following edges 1 > 1

(20) YES

(21) Obligation:

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

QUOTH_IN_GA(s(s(s(T616))), s(T618)) → QUOTH_IN_GA(T616, T618)

The TRS R consists of the following rules:

divA_in_gga(T7, T8, T10) → U1_gga(T7, T8, T10, quotB_in_gga(T7, T8, T10))
quotB_in_gga(0, s(T15), 0) → quotB_out_gga(0, s(T15), 0)
quotB_in_gga(s(0), s(s(T38)), 0) → quotB_out_gga(s(0), s(s(T38)), 0)
quotB_in_gga(s(s(0)), s(s(s(T61))), 0) → quotB_out_gga(s(s(0)), s(s(s(T61))), 0)
quotB_in_gga(s(s(s(0))), s(s(s(s(T84)))), 0) → quotB_out_gga(s(s(s(0))), s(s(s(s(T84)))), 0)
quotB_in_gga(s(s(s(s(0)))), s(s(s(s(s(T107))))), 0) → quotB_out_gga(s(s(s(s(0)))), s(s(s(s(s(T107))))), 0)
quotB_in_gga(s(s(s(s(s(0))))), s(s(s(s(s(s(T130)))))), 0) → quotB_out_gga(s(s(s(s(s(0))))), s(s(s(s(s(s(T130)))))), 0)
quotB_in_gga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T153))))))), 0) → quotB_out_gga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T153))))))), 0)
quotB_in_gga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(T176)))))))), 0) → quotB_out_gga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(T176)))))))), 0)
quotB_in_gga(s(s(s(s(s(s(s(s(T189)))))))), s(s(s(s(s(s(s(s(T190)))))))), T192) → U4_gga(T189, T190, T192, quotC_in_ggga(T189, T190, s(s(s(s(s(s(s(T190))))))), T192))
quotC_in_ggga(0, s(T208), T209, 0) → quotC_out_ggga(0, s(T208), T209, 0)
quotC_in_ggga(s(T226), s(T227), T228, T230) → U2_ggga(T226, T227, T228, T230, quotC_in_ggga(T226, T227, T228, T230))
quotC_in_ggga(T241, 0, T242, s(T244)) → U3_ggga(T241, T242, T244, quotB_in_gga(T241, s(T242), T244))
quotB_in_gga(s(s(s(s(s(s(s(T251))))))), s(s(s(s(s(s(s(0))))))), s(T253)) → U5_gga(T251, T253, quotD_in_ga(T251, T253))
quotD_in_ga(0, 0) → quotD_out_ga(0, 0)
quotD_in_ga(s(0), 0) → quotD_out_ga(s(0), 0)
quotD_in_ga(s(s(0)), 0) → quotD_out_ga(s(s(0)), 0)
quotD_in_ga(s(s(s(0))), 0) → quotD_out_ga(s(s(s(0))), 0)
quotD_in_ga(s(s(s(s(0)))), 0) → quotD_out_ga(s(s(s(s(0)))), 0)
quotD_in_ga(s(s(s(s(s(0))))), 0) → quotD_out_ga(s(s(s(s(s(0))))), 0)
quotD_in_ga(s(s(s(s(s(s(0)))))), 0) → quotD_out_ga(s(s(s(s(s(s(0)))))), 0)
quotD_in_ga(s(s(s(s(s(s(s(T336))))))), s(T338)) → U12_ga(T336, T338, quotD_in_ga(T336, T338))
U12_ga(T336, T338, quotD_out_ga(T336, T338)) → quotD_out_ga(s(s(s(s(s(s(s(T336))))))), s(T338))
U5_gga(T251, T253, quotD_out_ga(T251, T253)) → quotB_out_gga(s(s(s(s(s(s(s(T251))))))), s(s(s(s(s(s(s(0))))))), s(T253))
quotB_in_gga(s(s(s(s(s(s(T350)))))), s(s(s(s(s(s(0)))))), s(T352)) → U6_gga(T350, T352, quotE_in_ga(T350, T352))
quotE_in_ga(0, 0) → quotE_out_ga(0, 0)
quotE_in_ga(s(0), 0) → quotE_out_ga(s(0), 0)
quotE_in_ga(s(s(0)), 0) → quotE_out_ga(s(s(0)), 0)
quotE_in_ga(s(s(s(0))), 0) → quotE_out_ga(s(s(s(0))), 0)
quotE_in_ga(s(s(s(s(0)))), 0) → quotE_out_ga(s(s(s(s(0)))), 0)
quotE_in_ga(s(s(s(s(s(0))))), 0) → quotE_out_ga(s(s(s(s(s(0))))), 0)
quotE_in_ga(s(s(s(s(s(s(T424)))))), s(T426)) → U13_ga(T424, T426, quotE_in_ga(T424, T426))
U13_ga(T424, T426, quotE_out_ga(T424, T426)) → quotE_out_ga(s(s(s(s(s(s(T424)))))), s(T426))
U6_gga(T350, T352, quotE_out_ga(T350, T352)) → quotB_out_gga(s(s(s(s(s(s(T350)))))), s(s(s(s(s(s(0)))))), s(T352))
quotB_in_gga(s(s(s(s(s(T437))))), s(s(s(s(s(0))))), s(T439)) → U7_gga(T437, T439, quotF_in_ga(T437, T439))
quotF_in_ga(0, 0) → quotF_out_ga(0, 0)
quotF_in_ga(s(0), 0) → quotF_out_ga(s(0), 0)
quotF_in_ga(s(s(0)), 0) → quotF_out_ga(s(s(0)), 0)
quotF_in_ga(s(s(s(0))), 0) → quotF_out_ga(s(s(s(0))), 0)
quotF_in_ga(s(s(s(s(0)))), 0) → quotF_out_ga(s(s(s(s(0)))), 0)
quotF_in_ga(s(s(s(s(s(T500))))), s(T502)) → U14_ga(T500, T502, quotF_in_ga(T500, T502))
U14_ga(T500, T502, quotF_out_ga(T500, T502)) → quotF_out_ga(s(s(s(s(s(T500))))), s(T502))
U7_gga(T437, T439, quotF_out_ga(T437, T439)) → quotB_out_gga(s(s(s(s(s(T437))))), s(s(s(s(s(0))))), s(T439))
quotB_in_gga(s(s(s(s(T512)))), s(s(s(s(0)))), s(T514)) → U8_gga(T512, T514, quotG_in_ga(T512, T514))
quotG_in_ga(0, 0) → quotG_out_ga(0, 0)
quotG_in_ga(s(0), 0) → quotG_out_ga(s(0), 0)
quotG_in_ga(s(s(0)), 0) → quotG_out_ga(s(s(0)), 0)
quotG_in_ga(s(s(s(0))), 0) → quotG_out_ga(s(s(s(0))), 0)
quotG_in_ga(s(s(s(s(T564)))), s(T566)) → U15_ga(T564, T566, quotG_in_ga(T564, T566))
U15_ga(T564, T566, quotG_out_ga(T564, T566)) → quotG_out_ga(s(s(s(s(T564)))), s(T566))
U8_gga(T512, T514, quotG_out_ga(T512, T514)) → quotB_out_gga(s(s(s(s(T512)))), s(s(s(s(0)))), s(T514))
quotB_in_gga(s(s(s(T575))), s(s(s(0))), s(T577)) → U9_gga(T575, T577, quotH_in_ga(T575, T577))
quotH_in_ga(0, 0) → quotH_out_ga(0, 0)
quotH_in_ga(s(0), 0) → quotH_out_ga(s(0), 0)
quotH_in_ga(s(s(0)), 0) → quotH_out_ga(s(s(0)), 0)
quotH_in_ga(s(s(s(T616))), s(T618)) → U16_ga(T616, T618, quotH_in_ga(T616, T618))
U16_ga(T616, T618, quotH_out_ga(T616, T618)) → quotH_out_ga(s(s(s(T616))), s(T618))
U9_gga(T575, T577, quotH_out_ga(T575, T577)) → quotB_out_gga(s(s(s(T575))), s(s(s(0))), s(T577))
quotB_in_gga(s(s(T626)), s(s(0)), s(T628)) → U10_gga(T626, T628, quotI_in_ga(T626, T628))
quotI_in_ga(0, 0) → quotI_out_ga(0, 0)
quotI_in_ga(s(0), 0) → quotI_out_ga(s(0), 0)
quotI_in_ga(s(s(T656)), s(T658)) → U17_ga(T656, T658, quotI_in_ga(T656, T658))
U17_ga(T656, T658, quotI_out_ga(T656, T658)) → quotI_out_ga(s(s(T656)), s(T658))
U10_gga(T626, T628, quotI_out_ga(T626, T628)) → quotB_out_gga(s(s(T626)), s(s(0)), s(T628))
quotB_in_gga(s(T665), s(0), s(T667)) → U11_gga(T665, T667, quotJ_in_ga(T665, T667))
quotJ_in_ga(0, 0) → quotJ_out_ga(0, 0)
quotJ_in_ga(s(T684), s(T686)) → U18_ga(T684, T686, quotJ_in_ga(T684, T686))
U18_ga(T684, T686, quotJ_out_ga(T684, T686)) → quotJ_out_ga(s(T684), s(T686))
U11_gga(T665, T667, quotJ_out_ga(T665, T667)) → quotB_out_gga(s(T665), s(0), s(T667))
U3_ggga(T241, T242, T244, quotB_out_gga(T241, s(T242), T244)) → quotC_out_ggga(T241, 0, T242, s(T244))
U2_ggga(T226, T227, T228, T230, quotC_out_ggga(T226, T227, T228, T230)) → quotC_out_ggga(s(T226), s(T227), T228, T230)
U4_gga(T189, T190, T192, quotC_out_ggga(T189, T190, s(s(s(s(s(s(s(T190))))))), T192)) → quotB_out_gga(s(s(s(s(s(s(s(s(T189)))))))), s(s(s(s(s(s(s(s(T190)))))))), T192)
U1_gga(T7, T8, T10, quotB_out_gga(T7, T8, T10)) → divA_out_gga(T7, T8, T10)

The argument filtering Pi contains the following mapping:
divA_in_gga(x1, x2, x3)  =  divA_in_gga(x1, x2)
U1_gga(x1, x2, x3, x4)  =  U1_gga(x1, x2, x4)
quotB_in_gga(x1, x2, x3)  =  quotB_in_gga(x1, x2)
0  =  0
s(x1)  =  s(x1)
quotB_out_gga(x1, x2, x3)  =  quotB_out_gga(x1, x2, x3)
U4_gga(x1, x2, x3, x4)  =  U4_gga(x1, x2, x4)
quotC_in_ggga(x1, x2, x3, x4)  =  quotC_in_ggga(x1, x2, x3)
quotC_out_ggga(x1, x2, x3, x4)  =  quotC_out_ggga(x1, x2, x3, x4)
U2_ggga(x1, x2, x3, x4, x5)  =  U2_ggga(x1, x2, x3, x5)
U3_ggga(x1, x2, x3, x4)  =  U3_ggga(x1, x2, x4)
U5_gga(x1, x2, x3)  =  U5_gga(x1, x3)
quotD_in_ga(x1, x2)  =  quotD_in_ga(x1)
quotD_out_ga(x1, x2)  =  quotD_out_ga(x1, x2)
U12_ga(x1, x2, x3)  =  U12_ga(x1, x3)
U6_gga(x1, x2, x3)  =  U6_gga(x1, x3)
quotE_in_ga(x1, x2)  =  quotE_in_ga(x1)
quotE_out_ga(x1, x2)  =  quotE_out_ga(x1, x2)
U13_ga(x1, x2, x3)  =  U13_ga(x1, x3)
U7_gga(x1, x2, x3)  =  U7_gga(x1, x3)
quotF_in_ga(x1, x2)  =  quotF_in_ga(x1)
quotF_out_ga(x1, x2)  =  quotF_out_ga(x1, x2)
U14_ga(x1, x2, x3)  =  U14_ga(x1, x3)
U8_gga(x1, x2, x3)  =  U8_gga(x1, x3)
quotG_in_ga(x1, x2)  =  quotG_in_ga(x1)
quotG_out_ga(x1, x2)  =  quotG_out_ga(x1, x2)
U15_ga(x1, x2, x3)  =  U15_ga(x1, x3)
U9_gga(x1, x2, x3)  =  U9_gga(x1, x3)
quotH_in_ga(x1, x2)  =  quotH_in_ga(x1)
quotH_out_ga(x1, x2)  =  quotH_out_ga(x1, x2)
U16_ga(x1, x2, x3)  =  U16_ga(x1, x3)
U10_gga(x1, x2, x3)  =  U10_gga(x1, x3)
quotI_in_ga(x1, x2)  =  quotI_in_ga(x1)
quotI_out_ga(x1, x2)  =  quotI_out_ga(x1, x2)
U17_ga(x1, x2, x3)  =  U17_ga(x1, x3)
U11_gga(x1, x2, x3)  =  U11_gga(x1, x3)
quotJ_in_ga(x1, x2)  =  quotJ_in_ga(x1)
quotJ_out_ga(x1, x2)  =  quotJ_out_ga(x1, x2)
U18_ga(x1, x2, x3)  =  U18_ga(x1, x3)
divA_out_gga(x1, x2, x3)  =  divA_out_gga(x1, x2, x3)
QUOTH_IN_GA(x1, x2)  =  QUOTH_IN_GA(x1)

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

(22) UsableRulesProof (EQUIVALENT transformation)

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

(23) Obligation:

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

QUOTH_IN_GA(s(s(s(T616))), s(T618)) → QUOTH_IN_GA(T616, T618)

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

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

(24) PiDPToQDPProof (SOUND transformation)

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

(25) Obligation:

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

QUOTH_IN_GA(s(s(s(T616)))) → QUOTH_IN_GA(T616)

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

(26) QDPSizeChangeProof (EQUIVALENT transformation)

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

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

  • QUOTH_IN_GA(s(s(s(T616)))) → QUOTH_IN_GA(T616)
    The graph contains the following edges 1 > 1

(27) YES

(28) Obligation:

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

QUOTG_IN_GA(s(s(s(s(T564)))), s(T566)) → QUOTG_IN_GA(T564, T566)

The TRS R consists of the following rules:

divA_in_gga(T7, T8, T10) → U1_gga(T7, T8, T10, quotB_in_gga(T7, T8, T10))
quotB_in_gga(0, s(T15), 0) → quotB_out_gga(0, s(T15), 0)
quotB_in_gga(s(0), s(s(T38)), 0) → quotB_out_gga(s(0), s(s(T38)), 0)
quotB_in_gga(s(s(0)), s(s(s(T61))), 0) → quotB_out_gga(s(s(0)), s(s(s(T61))), 0)
quotB_in_gga(s(s(s(0))), s(s(s(s(T84)))), 0) → quotB_out_gga(s(s(s(0))), s(s(s(s(T84)))), 0)
quotB_in_gga(s(s(s(s(0)))), s(s(s(s(s(T107))))), 0) → quotB_out_gga(s(s(s(s(0)))), s(s(s(s(s(T107))))), 0)
quotB_in_gga(s(s(s(s(s(0))))), s(s(s(s(s(s(T130)))))), 0) → quotB_out_gga(s(s(s(s(s(0))))), s(s(s(s(s(s(T130)))))), 0)
quotB_in_gga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T153))))))), 0) → quotB_out_gga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T153))))))), 0)
quotB_in_gga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(T176)))))))), 0) → quotB_out_gga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(T176)))))))), 0)
quotB_in_gga(s(s(s(s(s(s(s(s(T189)))))))), s(s(s(s(s(s(s(s(T190)))))))), T192) → U4_gga(T189, T190, T192, quotC_in_ggga(T189, T190, s(s(s(s(s(s(s(T190))))))), T192))
quotC_in_ggga(0, s(T208), T209, 0) → quotC_out_ggga(0, s(T208), T209, 0)
quotC_in_ggga(s(T226), s(T227), T228, T230) → U2_ggga(T226, T227, T228, T230, quotC_in_ggga(T226, T227, T228, T230))
quotC_in_ggga(T241, 0, T242, s(T244)) → U3_ggga(T241, T242, T244, quotB_in_gga(T241, s(T242), T244))
quotB_in_gga(s(s(s(s(s(s(s(T251))))))), s(s(s(s(s(s(s(0))))))), s(T253)) → U5_gga(T251, T253, quotD_in_ga(T251, T253))
quotD_in_ga(0, 0) → quotD_out_ga(0, 0)
quotD_in_ga(s(0), 0) → quotD_out_ga(s(0), 0)
quotD_in_ga(s(s(0)), 0) → quotD_out_ga(s(s(0)), 0)
quotD_in_ga(s(s(s(0))), 0) → quotD_out_ga(s(s(s(0))), 0)
quotD_in_ga(s(s(s(s(0)))), 0) → quotD_out_ga(s(s(s(s(0)))), 0)
quotD_in_ga(s(s(s(s(s(0))))), 0) → quotD_out_ga(s(s(s(s(s(0))))), 0)
quotD_in_ga(s(s(s(s(s(s(0)))))), 0) → quotD_out_ga(s(s(s(s(s(s(0)))))), 0)
quotD_in_ga(s(s(s(s(s(s(s(T336))))))), s(T338)) → U12_ga(T336, T338, quotD_in_ga(T336, T338))
U12_ga(T336, T338, quotD_out_ga(T336, T338)) → quotD_out_ga(s(s(s(s(s(s(s(T336))))))), s(T338))
U5_gga(T251, T253, quotD_out_ga(T251, T253)) → quotB_out_gga(s(s(s(s(s(s(s(T251))))))), s(s(s(s(s(s(s(0))))))), s(T253))
quotB_in_gga(s(s(s(s(s(s(T350)))))), s(s(s(s(s(s(0)))))), s(T352)) → U6_gga(T350, T352, quotE_in_ga(T350, T352))
quotE_in_ga(0, 0) → quotE_out_ga(0, 0)
quotE_in_ga(s(0), 0) → quotE_out_ga(s(0), 0)
quotE_in_ga(s(s(0)), 0) → quotE_out_ga(s(s(0)), 0)
quotE_in_ga(s(s(s(0))), 0) → quotE_out_ga(s(s(s(0))), 0)
quotE_in_ga(s(s(s(s(0)))), 0) → quotE_out_ga(s(s(s(s(0)))), 0)
quotE_in_ga(s(s(s(s(s(0))))), 0) → quotE_out_ga(s(s(s(s(s(0))))), 0)
quotE_in_ga(s(s(s(s(s(s(T424)))))), s(T426)) → U13_ga(T424, T426, quotE_in_ga(T424, T426))
U13_ga(T424, T426, quotE_out_ga(T424, T426)) → quotE_out_ga(s(s(s(s(s(s(T424)))))), s(T426))
U6_gga(T350, T352, quotE_out_ga(T350, T352)) → quotB_out_gga(s(s(s(s(s(s(T350)))))), s(s(s(s(s(s(0)))))), s(T352))
quotB_in_gga(s(s(s(s(s(T437))))), s(s(s(s(s(0))))), s(T439)) → U7_gga(T437, T439, quotF_in_ga(T437, T439))
quotF_in_ga(0, 0) → quotF_out_ga(0, 0)
quotF_in_ga(s(0), 0) → quotF_out_ga(s(0), 0)
quotF_in_ga(s(s(0)), 0) → quotF_out_ga(s(s(0)), 0)
quotF_in_ga(s(s(s(0))), 0) → quotF_out_ga(s(s(s(0))), 0)
quotF_in_ga(s(s(s(s(0)))), 0) → quotF_out_ga(s(s(s(s(0)))), 0)
quotF_in_ga(s(s(s(s(s(T500))))), s(T502)) → U14_ga(T500, T502, quotF_in_ga(T500, T502))
U14_ga(T500, T502, quotF_out_ga(T500, T502)) → quotF_out_ga(s(s(s(s(s(T500))))), s(T502))
U7_gga(T437, T439, quotF_out_ga(T437, T439)) → quotB_out_gga(s(s(s(s(s(T437))))), s(s(s(s(s(0))))), s(T439))
quotB_in_gga(s(s(s(s(T512)))), s(s(s(s(0)))), s(T514)) → U8_gga(T512, T514, quotG_in_ga(T512, T514))
quotG_in_ga(0, 0) → quotG_out_ga(0, 0)
quotG_in_ga(s(0), 0) → quotG_out_ga(s(0), 0)
quotG_in_ga(s(s(0)), 0) → quotG_out_ga(s(s(0)), 0)
quotG_in_ga(s(s(s(0))), 0) → quotG_out_ga(s(s(s(0))), 0)
quotG_in_ga(s(s(s(s(T564)))), s(T566)) → U15_ga(T564, T566, quotG_in_ga(T564, T566))
U15_ga(T564, T566, quotG_out_ga(T564, T566)) → quotG_out_ga(s(s(s(s(T564)))), s(T566))
U8_gga(T512, T514, quotG_out_ga(T512, T514)) → quotB_out_gga(s(s(s(s(T512)))), s(s(s(s(0)))), s(T514))
quotB_in_gga(s(s(s(T575))), s(s(s(0))), s(T577)) → U9_gga(T575, T577, quotH_in_ga(T575, T577))
quotH_in_ga(0, 0) → quotH_out_ga(0, 0)
quotH_in_ga(s(0), 0) → quotH_out_ga(s(0), 0)
quotH_in_ga(s(s(0)), 0) → quotH_out_ga(s(s(0)), 0)
quotH_in_ga(s(s(s(T616))), s(T618)) → U16_ga(T616, T618, quotH_in_ga(T616, T618))
U16_ga(T616, T618, quotH_out_ga(T616, T618)) → quotH_out_ga(s(s(s(T616))), s(T618))
U9_gga(T575, T577, quotH_out_ga(T575, T577)) → quotB_out_gga(s(s(s(T575))), s(s(s(0))), s(T577))
quotB_in_gga(s(s(T626)), s(s(0)), s(T628)) → U10_gga(T626, T628, quotI_in_ga(T626, T628))
quotI_in_ga(0, 0) → quotI_out_ga(0, 0)
quotI_in_ga(s(0), 0) → quotI_out_ga(s(0), 0)
quotI_in_ga(s(s(T656)), s(T658)) → U17_ga(T656, T658, quotI_in_ga(T656, T658))
U17_ga(T656, T658, quotI_out_ga(T656, T658)) → quotI_out_ga(s(s(T656)), s(T658))
U10_gga(T626, T628, quotI_out_ga(T626, T628)) → quotB_out_gga(s(s(T626)), s(s(0)), s(T628))
quotB_in_gga(s(T665), s(0), s(T667)) → U11_gga(T665, T667, quotJ_in_ga(T665, T667))
quotJ_in_ga(0, 0) → quotJ_out_ga(0, 0)
quotJ_in_ga(s(T684), s(T686)) → U18_ga(T684, T686, quotJ_in_ga(T684, T686))
U18_ga(T684, T686, quotJ_out_ga(T684, T686)) → quotJ_out_ga(s(T684), s(T686))
U11_gga(T665, T667, quotJ_out_ga(T665, T667)) → quotB_out_gga(s(T665), s(0), s(T667))
U3_ggga(T241, T242, T244, quotB_out_gga(T241, s(T242), T244)) → quotC_out_ggga(T241, 0, T242, s(T244))
U2_ggga(T226, T227, T228, T230, quotC_out_ggga(T226, T227, T228, T230)) → quotC_out_ggga(s(T226), s(T227), T228, T230)
U4_gga(T189, T190, T192, quotC_out_ggga(T189, T190, s(s(s(s(s(s(s(T190))))))), T192)) → quotB_out_gga(s(s(s(s(s(s(s(s(T189)))))))), s(s(s(s(s(s(s(s(T190)))))))), T192)
U1_gga(T7, T8, T10, quotB_out_gga(T7, T8, T10)) → divA_out_gga(T7, T8, T10)

The argument filtering Pi contains the following mapping:
divA_in_gga(x1, x2, x3)  =  divA_in_gga(x1, x2)
U1_gga(x1, x2, x3, x4)  =  U1_gga(x1, x2, x4)
quotB_in_gga(x1, x2, x3)  =  quotB_in_gga(x1, x2)
0  =  0
s(x1)  =  s(x1)
quotB_out_gga(x1, x2, x3)  =  quotB_out_gga(x1, x2, x3)
U4_gga(x1, x2, x3, x4)  =  U4_gga(x1, x2, x4)
quotC_in_ggga(x1, x2, x3, x4)  =  quotC_in_ggga(x1, x2, x3)
quotC_out_ggga(x1, x2, x3, x4)  =  quotC_out_ggga(x1, x2, x3, x4)
U2_ggga(x1, x2, x3, x4, x5)  =  U2_ggga(x1, x2, x3, x5)
U3_ggga(x1, x2, x3, x4)  =  U3_ggga(x1, x2, x4)
U5_gga(x1, x2, x3)  =  U5_gga(x1, x3)
quotD_in_ga(x1, x2)  =  quotD_in_ga(x1)
quotD_out_ga(x1, x2)  =  quotD_out_ga(x1, x2)
U12_ga(x1, x2, x3)  =  U12_ga(x1, x3)
U6_gga(x1, x2, x3)  =  U6_gga(x1, x3)
quotE_in_ga(x1, x2)  =  quotE_in_ga(x1)
quotE_out_ga(x1, x2)  =  quotE_out_ga(x1, x2)
U13_ga(x1, x2, x3)  =  U13_ga(x1, x3)
U7_gga(x1, x2, x3)  =  U7_gga(x1, x3)
quotF_in_ga(x1, x2)  =  quotF_in_ga(x1)
quotF_out_ga(x1, x2)  =  quotF_out_ga(x1, x2)
U14_ga(x1, x2, x3)  =  U14_ga(x1, x3)
U8_gga(x1, x2, x3)  =  U8_gga(x1, x3)
quotG_in_ga(x1, x2)  =  quotG_in_ga(x1)
quotG_out_ga(x1, x2)  =  quotG_out_ga(x1, x2)
U15_ga(x1, x2, x3)  =  U15_ga(x1, x3)
U9_gga(x1, x2, x3)  =  U9_gga(x1, x3)
quotH_in_ga(x1, x2)  =  quotH_in_ga(x1)
quotH_out_ga(x1, x2)  =  quotH_out_ga(x1, x2)
U16_ga(x1, x2, x3)  =  U16_ga(x1, x3)
U10_gga(x1, x2, x3)  =  U10_gga(x1, x3)
quotI_in_ga(x1, x2)  =  quotI_in_ga(x1)
quotI_out_ga(x1, x2)  =  quotI_out_ga(x1, x2)
U17_ga(x1, x2, x3)  =  U17_ga(x1, x3)
U11_gga(x1, x2, x3)  =  U11_gga(x1, x3)
quotJ_in_ga(x1, x2)  =  quotJ_in_ga(x1)
quotJ_out_ga(x1, x2)  =  quotJ_out_ga(x1, x2)
U18_ga(x1, x2, x3)  =  U18_ga(x1, x3)
divA_out_gga(x1, x2, x3)  =  divA_out_gga(x1, x2, x3)
QUOTG_IN_GA(x1, x2)  =  QUOTG_IN_GA(x1)

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

(29) UsableRulesProof (EQUIVALENT transformation)

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

(30) Obligation:

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

QUOTG_IN_GA(s(s(s(s(T564)))), s(T566)) → QUOTG_IN_GA(T564, T566)

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

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

(31) PiDPToQDPProof (SOUND transformation)

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

(32) Obligation:

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

QUOTG_IN_GA(s(s(s(s(T564))))) → QUOTG_IN_GA(T564)

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

(33) QDPSizeChangeProof (EQUIVALENT transformation)

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

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

  • QUOTG_IN_GA(s(s(s(s(T564))))) → QUOTG_IN_GA(T564)
    The graph contains the following edges 1 > 1

(34) YES

(35) Obligation:

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

QUOTF_IN_GA(s(s(s(s(s(T500))))), s(T502)) → QUOTF_IN_GA(T500, T502)

The TRS R consists of the following rules:

divA_in_gga(T7, T8, T10) → U1_gga(T7, T8, T10, quotB_in_gga(T7, T8, T10))
quotB_in_gga(0, s(T15), 0) → quotB_out_gga(0, s(T15), 0)
quotB_in_gga(s(0), s(s(T38)), 0) → quotB_out_gga(s(0), s(s(T38)), 0)
quotB_in_gga(s(s(0)), s(s(s(T61))), 0) → quotB_out_gga(s(s(0)), s(s(s(T61))), 0)
quotB_in_gga(s(s(s(0))), s(s(s(s(T84)))), 0) → quotB_out_gga(s(s(s(0))), s(s(s(s(T84)))), 0)
quotB_in_gga(s(s(s(s(0)))), s(s(s(s(s(T107))))), 0) → quotB_out_gga(s(s(s(s(0)))), s(s(s(s(s(T107))))), 0)
quotB_in_gga(s(s(s(s(s(0))))), s(s(s(s(s(s(T130)))))), 0) → quotB_out_gga(s(s(s(s(s(0))))), s(s(s(s(s(s(T130)))))), 0)
quotB_in_gga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T153))))))), 0) → quotB_out_gga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T153))))))), 0)
quotB_in_gga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(T176)))))))), 0) → quotB_out_gga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(T176)))))))), 0)
quotB_in_gga(s(s(s(s(s(s(s(s(T189)))))))), s(s(s(s(s(s(s(s(T190)))))))), T192) → U4_gga(T189, T190, T192, quotC_in_ggga(T189, T190, s(s(s(s(s(s(s(T190))))))), T192))
quotC_in_ggga(0, s(T208), T209, 0) → quotC_out_ggga(0, s(T208), T209, 0)
quotC_in_ggga(s(T226), s(T227), T228, T230) → U2_ggga(T226, T227, T228, T230, quotC_in_ggga(T226, T227, T228, T230))
quotC_in_ggga(T241, 0, T242, s(T244)) → U3_ggga(T241, T242, T244, quotB_in_gga(T241, s(T242), T244))
quotB_in_gga(s(s(s(s(s(s(s(T251))))))), s(s(s(s(s(s(s(0))))))), s(T253)) → U5_gga(T251, T253, quotD_in_ga(T251, T253))
quotD_in_ga(0, 0) → quotD_out_ga(0, 0)
quotD_in_ga(s(0), 0) → quotD_out_ga(s(0), 0)
quotD_in_ga(s(s(0)), 0) → quotD_out_ga(s(s(0)), 0)
quotD_in_ga(s(s(s(0))), 0) → quotD_out_ga(s(s(s(0))), 0)
quotD_in_ga(s(s(s(s(0)))), 0) → quotD_out_ga(s(s(s(s(0)))), 0)
quotD_in_ga(s(s(s(s(s(0))))), 0) → quotD_out_ga(s(s(s(s(s(0))))), 0)
quotD_in_ga(s(s(s(s(s(s(0)))))), 0) → quotD_out_ga(s(s(s(s(s(s(0)))))), 0)
quotD_in_ga(s(s(s(s(s(s(s(T336))))))), s(T338)) → U12_ga(T336, T338, quotD_in_ga(T336, T338))
U12_ga(T336, T338, quotD_out_ga(T336, T338)) → quotD_out_ga(s(s(s(s(s(s(s(T336))))))), s(T338))
U5_gga(T251, T253, quotD_out_ga(T251, T253)) → quotB_out_gga(s(s(s(s(s(s(s(T251))))))), s(s(s(s(s(s(s(0))))))), s(T253))
quotB_in_gga(s(s(s(s(s(s(T350)))))), s(s(s(s(s(s(0)))))), s(T352)) → U6_gga(T350, T352, quotE_in_ga(T350, T352))
quotE_in_ga(0, 0) → quotE_out_ga(0, 0)
quotE_in_ga(s(0), 0) → quotE_out_ga(s(0), 0)
quotE_in_ga(s(s(0)), 0) → quotE_out_ga(s(s(0)), 0)
quotE_in_ga(s(s(s(0))), 0) → quotE_out_ga(s(s(s(0))), 0)
quotE_in_ga(s(s(s(s(0)))), 0) → quotE_out_ga(s(s(s(s(0)))), 0)
quotE_in_ga(s(s(s(s(s(0))))), 0) → quotE_out_ga(s(s(s(s(s(0))))), 0)
quotE_in_ga(s(s(s(s(s(s(T424)))))), s(T426)) → U13_ga(T424, T426, quotE_in_ga(T424, T426))
U13_ga(T424, T426, quotE_out_ga(T424, T426)) → quotE_out_ga(s(s(s(s(s(s(T424)))))), s(T426))
U6_gga(T350, T352, quotE_out_ga(T350, T352)) → quotB_out_gga(s(s(s(s(s(s(T350)))))), s(s(s(s(s(s(0)))))), s(T352))
quotB_in_gga(s(s(s(s(s(T437))))), s(s(s(s(s(0))))), s(T439)) → U7_gga(T437, T439, quotF_in_ga(T437, T439))
quotF_in_ga(0, 0) → quotF_out_ga(0, 0)
quotF_in_ga(s(0), 0) → quotF_out_ga(s(0), 0)
quotF_in_ga(s(s(0)), 0) → quotF_out_ga(s(s(0)), 0)
quotF_in_ga(s(s(s(0))), 0) → quotF_out_ga(s(s(s(0))), 0)
quotF_in_ga(s(s(s(s(0)))), 0) → quotF_out_ga(s(s(s(s(0)))), 0)
quotF_in_ga(s(s(s(s(s(T500))))), s(T502)) → U14_ga(T500, T502, quotF_in_ga(T500, T502))
U14_ga(T500, T502, quotF_out_ga(T500, T502)) → quotF_out_ga(s(s(s(s(s(T500))))), s(T502))
U7_gga(T437, T439, quotF_out_ga(T437, T439)) → quotB_out_gga(s(s(s(s(s(T437))))), s(s(s(s(s(0))))), s(T439))
quotB_in_gga(s(s(s(s(T512)))), s(s(s(s(0)))), s(T514)) → U8_gga(T512, T514, quotG_in_ga(T512, T514))
quotG_in_ga(0, 0) → quotG_out_ga(0, 0)
quotG_in_ga(s(0), 0) → quotG_out_ga(s(0), 0)
quotG_in_ga(s(s(0)), 0) → quotG_out_ga(s(s(0)), 0)
quotG_in_ga(s(s(s(0))), 0) → quotG_out_ga(s(s(s(0))), 0)
quotG_in_ga(s(s(s(s(T564)))), s(T566)) → U15_ga(T564, T566, quotG_in_ga(T564, T566))
U15_ga(T564, T566, quotG_out_ga(T564, T566)) → quotG_out_ga(s(s(s(s(T564)))), s(T566))
U8_gga(T512, T514, quotG_out_ga(T512, T514)) → quotB_out_gga(s(s(s(s(T512)))), s(s(s(s(0)))), s(T514))
quotB_in_gga(s(s(s(T575))), s(s(s(0))), s(T577)) → U9_gga(T575, T577, quotH_in_ga(T575, T577))
quotH_in_ga(0, 0) → quotH_out_ga(0, 0)
quotH_in_ga(s(0), 0) → quotH_out_ga(s(0), 0)
quotH_in_ga(s(s(0)), 0) → quotH_out_ga(s(s(0)), 0)
quotH_in_ga(s(s(s(T616))), s(T618)) → U16_ga(T616, T618, quotH_in_ga(T616, T618))
U16_ga(T616, T618, quotH_out_ga(T616, T618)) → quotH_out_ga(s(s(s(T616))), s(T618))
U9_gga(T575, T577, quotH_out_ga(T575, T577)) → quotB_out_gga(s(s(s(T575))), s(s(s(0))), s(T577))
quotB_in_gga(s(s(T626)), s(s(0)), s(T628)) → U10_gga(T626, T628, quotI_in_ga(T626, T628))
quotI_in_ga(0, 0) → quotI_out_ga(0, 0)
quotI_in_ga(s(0), 0) → quotI_out_ga(s(0), 0)
quotI_in_ga(s(s(T656)), s(T658)) → U17_ga(T656, T658, quotI_in_ga(T656, T658))
U17_ga(T656, T658, quotI_out_ga(T656, T658)) → quotI_out_ga(s(s(T656)), s(T658))
U10_gga(T626, T628, quotI_out_ga(T626, T628)) → quotB_out_gga(s(s(T626)), s(s(0)), s(T628))
quotB_in_gga(s(T665), s(0), s(T667)) → U11_gga(T665, T667, quotJ_in_ga(T665, T667))
quotJ_in_ga(0, 0) → quotJ_out_ga(0, 0)
quotJ_in_ga(s(T684), s(T686)) → U18_ga(T684, T686, quotJ_in_ga(T684, T686))
U18_ga(T684, T686, quotJ_out_ga(T684, T686)) → quotJ_out_ga(s(T684), s(T686))
U11_gga(T665, T667, quotJ_out_ga(T665, T667)) → quotB_out_gga(s(T665), s(0), s(T667))
U3_ggga(T241, T242, T244, quotB_out_gga(T241, s(T242), T244)) → quotC_out_ggga(T241, 0, T242, s(T244))
U2_ggga(T226, T227, T228, T230, quotC_out_ggga(T226, T227, T228, T230)) → quotC_out_ggga(s(T226), s(T227), T228, T230)
U4_gga(T189, T190, T192, quotC_out_ggga(T189, T190, s(s(s(s(s(s(s(T190))))))), T192)) → quotB_out_gga(s(s(s(s(s(s(s(s(T189)))))))), s(s(s(s(s(s(s(s(T190)))))))), T192)
U1_gga(T7, T8, T10, quotB_out_gga(T7, T8, T10)) → divA_out_gga(T7, T8, T10)

The argument filtering Pi contains the following mapping:
divA_in_gga(x1, x2, x3)  =  divA_in_gga(x1, x2)
U1_gga(x1, x2, x3, x4)  =  U1_gga(x1, x2, x4)
quotB_in_gga(x1, x2, x3)  =  quotB_in_gga(x1, x2)
0  =  0
s(x1)  =  s(x1)
quotB_out_gga(x1, x2, x3)  =  quotB_out_gga(x1, x2, x3)
U4_gga(x1, x2, x3, x4)  =  U4_gga(x1, x2, x4)
quotC_in_ggga(x1, x2, x3, x4)  =  quotC_in_ggga(x1, x2, x3)
quotC_out_ggga(x1, x2, x3, x4)  =  quotC_out_ggga(x1, x2, x3, x4)
U2_ggga(x1, x2, x3, x4, x5)  =  U2_ggga(x1, x2, x3, x5)
U3_ggga(x1, x2, x3, x4)  =  U3_ggga(x1, x2, x4)
U5_gga(x1, x2, x3)  =  U5_gga(x1, x3)
quotD_in_ga(x1, x2)  =  quotD_in_ga(x1)
quotD_out_ga(x1, x2)  =  quotD_out_ga(x1, x2)
U12_ga(x1, x2, x3)  =  U12_ga(x1, x3)
U6_gga(x1, x2, x3)  =  U6_gga(x1, x3)
quotE_in_ga(x1, x2)  =  quotE_in_ga(x1)
quotE_out_ga(x1, x2)  =  quotE_out_ga(x1, x2)
U13_ga(x1, x2, x3)  =  U13_ga(x1, x3)
U7_gga(x1, x2, x3)  =  U7_gga(x1, x3)
quotF_in_ga(x1, x2)  =  quotF_in_ga(x1)
quotF_out_ga(x1, x2)  =  quotF_out_ga(x1, x2)
U14_ga(x1, x2, x3)  =  U14_ga(x1, x3)
U8_gga(x1, x2, x3)  =  U8_gga(x1, x3)
quotG_in_ga(x1, x2)  =  quotG_in_ga(x1)
quotG_out_ga(x1, x2)  =  quotG_out_ga(x1, x2)
U15_ga(x1, x2, x3)  =  U15_ga(x1, x3)
U9_gga(x1, x2, x3)  =  U9_gga(x1, x3)
quotH_in_ga(x1, x2)  =  quotH_in_ga(x1)
quotH_out_ga(x1, x2)  =  quotH_out_ga(x1, x2)
U16_ga(x1, x2, x3)  =  U16_ga(x1, x3)
U10_gga(x1, x2, x3)  =  U10_gga(x1, x3)
quotI_in_ga(x1, x2)  =  quotI_in_ga(x1)
quotI_out_ga(x1, x2)  =  quotI_out_ga(x1, x2)
U17_ga(x1, x2, x3)  =  U17_ga(x1, x3)
U11_gga(x1, x2, x3)  =  U11_gga(x1, x3)
quotJ_in_ga(x1, x2)  =  quotJ_in_ga(x1)
quotJ_out_ga(x1, x2)  =  quotJ_out_ga(x1, x2)
U18_ga(x1, x2, x3)  =  U18_ga(x1, x3)
divA_out_gga(x1, x2, x3)  =  divA_out_gga(x1, x2, x3)
QUOTF_IN_GA(x1, x2)  =  QUOTF_IN_GA(x1)

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

(36) UsableRulesProof (EQUIVALENT transformation)

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

(37) Obligation:

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

QUOTF_IN_GA(s(s(s(s(s(T500))))), s(T502)) → QUOTF_IN_GA(T500, T502)

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

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

(38) PiDPToQDPProof (SOUND transformation)

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

(39) Obligation:

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

QUOTF_IN_GA(s(s(s(s(s(T500)))))) → QUOTF_IN_GA(T500)

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

(40) QDPSizeChangeProof (EQUIVALENT transformation)

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

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

  • QUOTF_IN_GA(s(s(s(s(s(T500)))))) → QUOTF_IN_GA(T500)
    The graph contains the following edges 1 > 1

(41) YES

(42) Obligation:

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

QUOTE_IN_GA(s(s(s(s(s(s(T424)))))), s(T426)) → QUOTE_IN_GA(T424, T426)

The TRS R consists of the following rules:

divA_in_gga(T7, T8, T10) → U1_gga(T7, T8, T10, quotB_in_gga(T7, T8, T10))
quotB_in_gga(0, s(T15), 0) → quotB_out_gga(0, s(T15), 0)
quotB_in_gga(s(0), s(s(T38)), 0) → quotB_out_gga(s(0), s(s(T38)), 0)
quotB_in_gga(s(s(0)), s(s(s(T61))), 0) → quotB_out_gga(s(s(0)), s(s(s(T61))), 0)
quotB_in_gga(s(s(s(0))), s(s(s(s(T84)))), 0) → quotB_out_gga(s(s(s(0))), s(s(s(s(T84)))), 0)
quotB_in_gga(s(s(s(s(0)))), s(s(s(s(s(T107))))), 0) → quotB_out_gga(s(s(s(s(0)))), s(s(s(s(s(T107))))), 0)
quotB_in_gga(s(s(s(s(s(0))))), s(s(s(s(s(s(T130)))))), 0) → quotB_out_gga(s(s(s(s(s(0))))), s(s(s(s(s(s(T130)))))), 0)
quotB_in_gga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T153))))))), 0) → quotB_out_gga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T153))))))), 0)
quotB_in_gga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(T176)))))))), 0) → quotB_out_gga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(T176)))))))), 0)
quotB_in_gga(s(s(s(s(s(s(s(s(T189)))))))), s(s(s(s(s(s(s(s(T190)))))))), T192) → U4_gga(T189, T190, T192, quotC_in_ggga(T189, T190, s(s(s(s(s(s(s(T190))))))), T192))
quotC_in_ggga(0, s(T208), T209, 0) → quotC_out_ggga(0, s(T208), T209, 0)
quotC_in_ggga(s(T226), s(T227), T228, T230) → U2_ggga(T226, T227, T228, T230, quotC_in_ggga(T226, T227, T228, T230))
quotC_in_ggga(T241, 0, T242, s(T244)) → U3_ggga(T241, T242, T244, quotB_in_gga(T241, s(T242), T244))
quotB_in_gga(s(s(s(s(s(s(s(T251))))))), s(s(s(s(s(s(s(0))))))), s(T253)) → U5_gga(T251, T253, quotD_in_ga(T251, T253))
quotD_in_ga(0, 0) → quotD_out_ga(0, 0)
quotD_in_ga(s(0), 0) → quotD_out_ga(s(0), 0)
quotD_in_ga(s(s(0)), 0) → quotD_out_ga(s(s(0)), 0)
quotD_in_ga(s(s(s(0))), 0) → quotD_out_ga(s(s(s(0))), 0)
quotD_in_ga(s(s(s(s(0)))), 0) → quotD_out_ga(s(s(s(s(0)))), 0)
quotD_in_ga(s(s(s(s(s(0))))), 0) → quotD_out_ga(s(s(s(s(s(0))))), 0)
quotD_in_ga(s(s(s(s(s(s(0)))))), 0) → quotD_out_ga(s(s(s(s(s(s(0)))))), 0)
quotD_in_ga(s(s(s(s(s(s(s(T336))))))), s(T338)) → U12_ga(T336, T338, quotD_in_ga(T336, T338))
U12_ga(T336, T338, quotD_out_ga(T336, T338)) → quotD_out_ga(s(s(s(s(s(s(s(T336))))))), s(T338))
U5_gga(T251, T253, quotD_out_ga(T251, T253)) → quotB_out_gga(s(s(s(s(s(s(s(T251))))))), s(s(s(s(s(s(s(0))))))), s(T253))
quotB_in_gga(s(s(s(s(s(s(T350)))))), s(s(s(s(s(s(0)))))), s(T352)) → U6_gga(T350, T352, quotE_in_ga(T350, T352))
quotE_in_ga(0, 0) → quotE_out_ga(0, 0)
quotE_in_ga(s(0), 0) → quotE_out_ga(s(0), 0)
quotE_in_ga(s(s(0)), 0) → quotE_out_ga(s(s(0)), 0)
quotE_in_ga(s(s(s(0))), 0) → quotE_out_ga(s(s(s(0))), 0)
quotE_in_ga(s(s(s(s(0)))), 0) → quotE_out_ga(s(s(s(s(0)))), 0)
quotE_in_ga(s(s(s(s(s(0))))), 0) → quotE_out_ga(s(s(s(s(s(0))))), 0)
quotE_in_ga(s(s(s(s(s(s(T424)))))), s(T426)) → U13_ga(T424, T426, quotE_in_ga(T424, T426))
U13_ga(T424, T426, quotE_out_ga(T424, T426)) → quotE_out_ga(s(s(s(s(s(s(T424)))))), s(T426))
U6_gga(T350, T352, quotE_out_ga(T350, T352)) → quotB_out_gga(s(s(s(s(s(s(T350)))))), s(s(s(s(s(s(0)))))), s(T352))
quotB_in_gga(s(s(s(s(s(T437))))), s(s(s(s(s(0))))), s(T439)) → U7_gga(T437, T439, quotF_in_ga(T437, T439))
quotF_in_ga(0, 0) → quotF_out_ga(0, 0)
quotF_in_ga(s(0), 0) → quotF_out_ga(s(0), 0)
quotF_in_ga(s(s(0)), 0) → quotF_out_ga(s(s(0)), 0)
quotF_in_ga(s(s(s(0))), 0) → quotF_out_ga(s(s(s(0))), 0)
quotF_in_ga(s(s(s(s(0)))), 0) → quotF_out_ga(s(s(s(s(0)))), 0)
quotF_in_ga(s(s(s(s(s(T500))))), s(T502)) → U14_ga(T500, T502, quotF_in_ga(T500, T502))
U14_ga(T500, T502, quotF_out_ga(T500, T502)) → quotF_out_ga(s(s(s(s(s(T500))))), s(T502))
U7_gga(T437, T439, quotF_out_ga(T437, T439)) → quotB_out_gga(s(s(s(s(s(T437))))), s(s(s(s(s(0))))), s(T439))
quotB_in_gga(s(s(s(s(T512)))), s(s(s(s(0)))), s(T514)) → U8_gga(T512, T514, quotG_in_ga(T512, T514))
quotG_in_ga(0, 0) → quotG_out_ga(0, 0)
quotG_in_ga(s(0), 0) → quotG_out_ga(s(0), 0)
quotG_in_ga(s(s(0)), 0) → quotG_out_ga(s(s(0)), 0)
quotG_in_ga(s(s(s(0))), 0) → quotG_out_ga(s(s(s(0))), 0)
quotG_in_ga(s(s(s(s(T564)))), s(T566)) → U15_ga(T564, T566, quotG_in_ga(T564, T566))
U15_ga(T564, T566, quotG_out_ga(T564, T566)) → quotG_out_ga(s(s(s(s(T564)))), s(T566))
U8_gga(T512, T514, quotG_out_ga(T512, T514)) → quotB_out_gga(s(s(s(s(T512)))), s(s(s(s(0)))), s(T514))
quotB_in_gga(s(s(s(T575))), s(s(s(0))), s(T577)) → U9_gga(T575, T577, quotH_in_ga(T575, T577))
quotH_in_ga(0, 0) → quotH_out_ga(0, 0)
quotH_in_ga(s(0), 0) → quotH_out_ga(s(0), 0)
quotH_in_ga(s(s(0)), 0) → quotH_out_ga(s(s(0)), 0)
quotH_in_ga(s(s(s(T616))), s(T618)) → U16_ga(T616, T618, quotH_in_ga(T616, T618))
U16_ga(T616, T618, quotH_out_ga(T616, T618)) → quotH_out_ga(s(s(s(T616))), s(T618))
U9_gga(T575, T577, quotH_out_ga(T575, T577)) → quotB_out_gga(s(s(s(T575))), s(s(s(0))), s(T577))
quotB_in_gga(s(s(T626)), s(s(0)), s(T628)) → U10_gga(T626, T628, quotI_in_ga(T626, T628))
quotI_in_ga(0, 0) → quotI_out_ga(0, 0)
quotI_in_ga(s(0), 0) → quotI_out_ga(s(0), 0)
quotI_in_ga(s(s(T656)), s(T658)) → U17_ga(T656, T658, quotI_in_ga(T656, T658))
U17_ga(T656, T658, quotI_out_ga(T656, T658)) → quotI_out_ga(s(s(T656)), s(T658))
U10_gga(T626, T628, quotI_out_ga(T626, T628)) → quotB_out_gga(s(s(T626)), s(s(0)), s(T628))
quotB_in_gga(s(T665), s(0), s(T667)) → U11_gga(T665, T667, quotJ_in_ga(T665, T667))
quotJ_in_ga(0, 0) → quotJ_out_ga(0, 0)
quotJ_in_ga(s(T684), s(T686)) → U18_ga(T684, T686, quotJ_in_ga(T684, T686))
U18_ga(T684, T686, quotJ_out_ga(T684, T686)) → quotJ_out_ga(s(T684), s(T686))
U11_gga(T665, T667, quotJ_out_ga(T665, T667)) → quotB_out_gga(s(T665), s(0), s(T667))
U3_ggga(T241, T242, T244, quotB_out_gga(T241, s(T242), T244)) → quotC_out_ggga(T241, 0, T242, s(T244))
U2_ggga(T226, T227, T228, T230, quotC_out_ggga(T226, T227, T228, T230)) → quotC_out_ggga(s(T226), s(T227), T228, T230)
U4_gga(T189, T190, T192, quotC_out_ggga(T189, T190, s(s(s(s(s(s(s(T190))))))), T192)) → quotB_out_gga(s(s(s(s(s(s(s(s(T189)))))))), s(s(s(s(s(s(s(s(T190)))))))), T192)
U1_gga(T7, T8, T10, quotB_out_gga(T7, T8, T10)) → divA_out_gga(T7, T8, T10)

The argument filtering Pi contains the following mapping:
divA_in_gga(x1, x2, x3)  =  divA_in_gga(x1, x2)
U1_gga(x1, x2, x3, x4)  =  U1_gga(x1, x2, x4)
quotB_in_gga(x1, x2, x3)  =  quotB_in_gga(x1, x2)
0  =  0
s(x1)  =  s(x1)
quotB_out_gga(x1, x2, x3)  =  quotB_out_gga(x1, x2, x3)
U4_gga(x1, x2, x3, x4)  =  U4_gga(x1, x2, x4)
quotC_in_ggga(x1, x2, x3, x4)  =  quotC_in_ggga(x1, x2, x3)
quotC_out_ggga(x1, x2, x3, x4)  =  quotC_out_ggga(x1, x2, x3, x4)
U2_ggga(x1, x2, x3, x4, x5)  =  U2_ggga(x1, x2, x3, x5)
U3_ggga(x1, x2, x3, x4)  =  U3_ggga(x1, x2, x4)
U5_gga(x1, x2, x3)  =  U5_gga(x1, x3)
quotD_in_ga(x1, x2)  =  quotD_in_ga(x1)
quotD_out_ga(x1, x2)  =  quotD_out_ga(x1, x2)
U12_ga(x1, x2, x3)  =  U12_ga(x1, x3)
U6_gga(x1, x2, x3)  =  U6_gga(x1, x3)
quotE_in_ga(x1, x2)  =  quotE_in_ga(x1)
quotE_out_ga(x1, x2)  =  quotE_out_ga(x1, x2)
U13_ga(x1, x2, x3)  =  U13_ga(x1, x3)
U7_gga(x1, x2, x3)  =  U7_gga(x1, x3)
quotF_in_ga(x1, x2)  =  quotF_in_ga(x1)
quotF_out_ga(x1, x2)  =  quotF_out_ga(x1, x2)
U14_ga(x1, x2, x3)  =  U14_ga(x1, x3)
U8_gga(x1, x2, x3)  =  U8_gga(x1, x3)
quotG_in_ga(x1, x2)  =  quotG_in_ga(x1)
quotG_out_ga(x1, x2)  =  quotG_out_ga(x1, x2)
U15_ga(x1, x2, x3)  =  U15_ga(x1, x3)
U9_gga(x1, x2, x3)  =  U9_gga(x1, x3)
quotH_in_ga(x1, x2)  =  quotH_in_ga(x1)
quotH_out_ga(x1, x2)  =  quotH_out_ga(x1, x2)
U16_ga(x1, x2, x3)  =  U16_ga(x1, x3)
U10_gga(x1, x2, x3)  =  U10_gga(x1, x3)
quotI_in_ga(x1, x2)  =  quotI_in_ga(x1)
quotI_out_ga(x1, x2)  =  quotI_out_ga(x1, x2)
U17_ga(x1, x2, x3)  =  U17_ga(x1, x3)
U11_gga(x1, x2, x3)  =  U11_gga(x1, x3)
quotJ_in_ga(x1, x2)  =  quotJ_in_ga(x1)
quotJ_out_ga(x1, x2)  =  quotJ_out_ga(x1, x2)
U18_ga(x1, x2, x3)  =  U18_ga(x1, x3)
divA_out_gga(x1, x2, x3)  =  divA_out_gga(x1, x2, x3)
QUOTE_IN_GA(x1, x2)  =  QUOTE_IN_GA(x1)

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

(43) UsableRulesProof (EQUIVALENT transformation)

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

(44) Obligation:

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

QUOTE_IN_GA(s(s(s(s(s(s(T424)))))), s(T426)) → QUOTE_IN_GA(T424, T426)

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

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

(45) PiDPToQDPProof (SOUND transformation)

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

(46) Obligation:

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

QUOTE_IN_GA(s(s(s(s(s(s(T424))))))) → QUOTE_IN_GA(T424)

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

(47) QDPSizeChangeProof (EQUIVALENT transformation)

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

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

  • QUOTE_IN_GA(s(s(s(s(s(s(T424))))))) → QUOTE_IN_GA(T424)
    The graph contains the following edges 1 > 1

(48) YES

(49) Obligation:

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

QUOTD_IN_GA(s(s(s(s(s(s(s(T336))))))), s(T338)) → QUOTD_IN_GA(T336, T338)

The TRS R consists of the following rules:

divA_in_gga(T7, T8, T10) → U1_gga(T7, T8, T10, quotB_in_gga(T7, T8, T10))
quotB_in_gga(0, s(T15), 0) → quotB_out_gga(0, s(T15), 0)
quotB_in_gga(s(0), s(s(T38)), 0) → quotB_out_gga(s(0), s(s(T38)), 0)
quotB_in_gga(s(s(0)), s(s(s(T61))), 0) → quotB_out_gga(s(s(0)), s(s(s(T61))), 0)
quotB_in_gga(s(s(s(0))), s(s(s(s(T84)))), 0) → quotB_out_gga(s(s(s(0))), s(s(s(s(T84)))), 0)
quotB_in_gga(s(s(s(s(0)))), s(s(s(s(s(T107))))), 0) → quotB_out_gga(s(s(s(s(0)))), s(s(s(s(s(T107))))), 0)
quotB_in_gga(s(s(s(s(s(0))))), s(s(s(s(s(s(T130)))))), 0) → quotB_out_gga(s(s(s(s(s(0))))), s(s(s(s(s(s(T130)))))), 0)
quotB_in_gga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T153))))))), 0) → quotB_out_gga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T153))))))), 0)
quotB_in_gga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(T176)))))))), 0) → quotB_out_gga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(T176)))))))), 0)
quotB_in_gga(s(s(s(s(s(s(s(s(T189)))))))), s(s(s(s(s(s(s(s(T190)))))))), T192) → U4_gga(T189, T190, T192, quotC_in_ggga(T189, T190, s(s(s(s(s(s(s(T190))))))), T192))
quotC_in_ggga(0, s(T208), T209, 0) → quotC_out_ggga(0, s(T208), T209, 0)
quotC_in_ggga(s(T226), s(T227), T228, T230) → U2_ggga(T226, T227, T228, T230, quotC_in_ggga(T226, T227, T228, T230))
quotC_in_ggga(T241, 0, T242, s(T244)) → U3_ggga(T241, T242, T244, quotB_in_gga(T241, s(T242), T244))
quotB_in_gga(s(s(s(s(s(s(s(T251))))))), s(s(s(s(s(s(s(0))))))), s(T253)) → U5_gga(T251, T253, quotD_in_ga(T251, T253))
quotD_in_ga(0, 0) → quotD_out_ga(0, 0)
quotD_in_ga(s(0), 0) → quotD_out_ga(s(0), 0)
quotD_in_ga(s(s(0)), 0) → quotD_out_ga(s(s(0)), 0)
quotD_in_ga(s(s(s(0))), 0) → quotD_out_ga(s(s(s(0))), 0)
quotD_in_ga(s(s(s(s(0)))), 0) → quotD_out_ga(s(s(s(s(0)))), 0)
quotD_in_ga(s(s(s(s(s(0))))), 0) → quotD_out_ga(s(s(s(s(s(0))))), 0)
quotD_in_ga(s(s(s(s(s(s(0)))))), 0) → quotD_out_ga(s(s(s(s(s(s(0)))))), 0)
quotD_in_ga(s(s(s(s(s(s(s(T336))))))), s(T338)) → U12_ga(T336, T338, quotD_in_ga(T336, T338))
U12_ga(T336, T338, quotD_out_ga(T336, T338)) → quotD_out_ga(s(s(s(s(s(s(s(T336))))))), s(T338))
U5_gga(T251, T253, quotD_out_ga(T251, T253)) → quotB_out_gga(s(s(s(s(s(s(s(T251))))))), s(s(s(s(s(s(s(0))))))), s(T253))
quotB_in_gga(s(s(s(s(s(s(T350)))))), s(s(s(s(s(s(0)))))), s(T352)) → U6_gga(T350, T352, quotE_in_ga(T350, T352))
quotE_in_ga(0, 0) → quotE_out_ga(0, 0)
quotE_in_ga(s(0), 0) → quotE_out_ga(s(0), 0)
quotE_in_ga(s(s(0)), 0) → quotE_out_ga(s(s(0)), 0)
quotE_in_ga(s(s(s(0))), 0) → quotE_out_ga(s(s(s(0))), 0)
quotE_in_ga(s(s(s(s(0)))), 0) → quotE_out_ga(s(s(s(s(0)))), 0)
quotE_in_ga(s(s(s(s(s(0))))), 0) → quotE_out_ga(s(s(s(s(s(0))))), 0)
quotE_in_ga(s(s(s(s(s(s(T424)))))), s(T426)) → U13_ga(T424, T426, quotE_in_ga(T424, T426))
U13_ga(T424, T426, quotE_out_ga(T424, T426)) → quotE_out_ga(s(s(s(s(s(s(T424)))))), s(T426))
U6_gga(T350, T352, quotE_out_ga(T350, T352)) → quotB_out_gga(s(s(s(s(s(s(T350)))))), s(s(s(s(s(s(0)))))), s(T352))
quotB_in_gga(s(s(s(s(s(T437))))), s(s(s(s(s(0))))), s(T439)) → U7_gga(T437, T439, quotF_in_ga(T437, T439))
quotF_in_ga(0, 0) → quotF_out_ga(0, 0)
quotF_in_ga(s(0), 0) → quotF_out_ga(s(0), 0)
quotF_in_ga(s(s(0)), 0) → quotF_out_ga(s(s(0)), 0)
quotF_in_ga(s(s(s(0))), 0) → quotF_out_ga(s(s(s(0))), 0)
quotF_in_ga(s(s(s(s(0)))), 0) → quotF_out_ga(s(s(s(s(0)))), 0)
quotF_in_ga(s(s(s(s(s(T500))))), s(T502)) → U14_ga(T500, T502, quotF_in_ga(T500, T502))
U14_ga(T500, T502, quotF_out_ga(T500, T502)) → quotF_out_ga(s(s(s(s(s(T500))))), s(T502))
U7_gga(T437, T439, quotF_out_ga(T437, T439)) → quotB_out_gga(s(s(s(s(s(T437))))), s(s(s(s(s(0))))), s(T439))
quotB_in_gga(s(s(s(s(T512)))), s(s(s(s(0)))), s(T514)) → U8_gga(T512, T514, quotG_in_ga(T512, T514))
quotG_in_ga(0, 0) → quotG_out_ga(0, 0)
quotG_in_ga(s(0), 0) → quotG_out_ga(s(0), 0)
quotG_in_ga(s(s(0)), 0) → quotG_out_ga(s(s(0)), 0)
quotG_in_ga(s(s(s(0))), 0) → quotG_out_ga(s(s(s(0))), 0)
quotG_in_ga(s(s(s(s(T564)))), s(T566)) → U15_ga(T564, T566, quotG_in_ga(T564, T566))
U15_ga(T564, T566, quotG_out_ga(T564, T566)) → quotG_out_ga(s(s(s(s(T564)))), s(T566))
U8_gga(T512, T514, quotG_out_ga(T512, T514)) → quotB_out_gga(s(s(s(s(T512)))), s(s(s(s(0)))), s(T514))
quotB_in_gga(s(s(s(T575))), s(s(s(0))), s(T577)) → U9_gga(T575, T577, quotH_in_ga(T575, T577))
quotH_in_ga(0, 0) → quotH_out_ga(0, 0)
quotH_in_ga(s(0), 0) → quotH_out_ga(s(0), 0)
quotH_in_ga(s(s(0)), 0) → quotH_out_ga(s(s(0)), 0)
quotH_in_ga(s(s(s(T616))), s(T618)) → U16_ga(T616, T618, quotH_in_ga(T616, T618))
U16_ga(T616, T618, quotH_out_ga(T616, T618)) → quotH_out_ga(s(s(s(T616))), s(T618))
U9_gga(T575, T577, quotH_out_ga(T575, T577)) → quotB_out_gga(s(s(s(T575))), s(s(s(0))), s(T577))
quotB_in_gga(s(s(T626)), s(s(0)), s(T628)) → U10_gga(T626, T628, quotI_in_ga(T626, T628))
quotI_in_ga(0, 0) → quotI_out_ga(0, 0)
quotI_in_ga(s(0), 0) → quotI_out_ga(s(0), 0)
quotI_in_ga(s(s(T656)), s(T658)) → U17_ga(T656, T658, quotI_in_ga(T656, T658))
U17_ga(T656, T658, quotI_out_ga(T656, T658)) → quotI_out_ga(s(s(T656)), s(T658))
U10_gga(T626, T628, quotI_out_ga(T626, T628)) → quotB_out_gga(s(s(T626)), s(s(0)), s(T628))
quotB_in_gga(s(T665), s(0), s(T667)) → U11_gga(T665, T667, quotJ_in_ga(T665, T667))
quotJ_in_ga(0, 0) → quotJ_out_ga(0, 0)
quotJ_in_ga(s(T684), s(T686)) → U18_ga(T684, T686, quotJ_in_ga(T684, T686))
U18_ga(T684, T686, quotJ_out_ga(T684, T686)) → quotJ_out_ga(s(T684), s(T686))
U11_gga(T665, T667, quotJ_out_ga(T665, T667)) → quotB_out_gga(s(T665), s(0), s(T667))
U3_ggga(T241, T242, T244, quotB_out_gga(T241, s(T242), T244)) → quotC_out_ggga(T241, 0, T242, s(T244))
U2_ggga(T226, T227, T228, T230, quotC_out_ggga(T226, T227, T228, T230)) → quotC_out_ggga(s(T226), s(T227), T228, T230)
U4_gga(T189, T190, T192, quotC_out_ggga(T189, T190, s(s(s(s(s(s(s(T190))))))), T192)) → quotB_out_gga(s(s(s(s(s(s(s(s(T189)))))))), s(s(s(s(s(s(s(s(T190)))))))), T192)
U1_gga(T7, T8, T10, quotB_out_gga(T7, T8, T10)) → divA_out_gga(T7, T8, T10)

The argument filtering Pi contains the following mapping:
divA_in_gga(x1, x2, x3)  =  divA_in_gga(x1, x2)
U1_gga(x1, x2, x3, x4)  =  U1_gga(x1, x2, x4)
quotB_in_gga(x1, x2, x3)  =  quotB_in_gga(x1, x2)
0  =  0
s(x1)  =  s(x1)
quotB_out_gga(x1, x2, x3)  =  quotB_out_gga(x1, x2, x3)
U4_gga(x1, x2, x3, x4)  =  U4_gga(x1, x2, x4)
quotC_in_ggga(x1, x2, x3, x4)  =  quotC_in_ggga(x1, x2, x3)
quotC_out_ggga(x1, x2, x3, x4)  =  quotC_out_ggga(x1, x2, x3, x4)
U2_ggga(x1, x2, x3, x4, x5)  =  U2_ggga(x1, x2, x3, x5)
U3_ggga(x1, x2, x3, x4)  =  U3_ggga(x1, x2, x4)
U5_gga(x1, x2, x3)  =  U5_gga(x1, x3)
quotD_in_ga(x1, x2)  =  quotD_in_ga(x1)
quotD_out_ga(x1, x2)  =  quotD_out_ga(x1, x2)
U12_ga(x1, x2, x3)  =  U12_ga(x1, x3)
U6_gga(x1, x2, x3)  =  U6_gga(x1, x3)
quotE_in_ga(x1, x2)  =  quotE_in_ga(x1)
quotE_out_ga(x1, x2)  =  quotE_out_ga(x1, x2)
U13_ga(x1, x2, x3)  =  U13_ga(x1, x3)
U7_gga(x1, x2, x3)  =  U7_gga(x1, x3)
quotF_in_ga(x1, x2)  =  quotF_in_ga(x1)
quotF_out_ga(x1, x2)  =  quotF_out_ga(x1, x2)
U14_ga(x1, x2, x3)  =  U14_ga(x1, x3)
U8_gga(x1, x2, x3)  =  U8_gga(x1, x3)
quotG_in_ga(x1, x2)  =  quotG_in_ga(x1)
quotG_out_ga(x1, x2)  =  quotG_out_ga(x1, x2)
U15_ga(x1, x2, x3)  =  U15_ga(x1, x3)
U9_gga(x1, x2, x3)  =  U9_gga(x1, x3)
quotH_in_ga(x1, x2)  =  quotH_in_ga(x1)
quotH_out_ga(x1, x2)  =  quotH_out_ga(x1, x2)
U16_ga(x1, x2, x3)  =  U16_ga(x1, x3)
U10_gga(x1, x2, x3)  =  U10_gga(x1, x3)
quotI_in_ga(x1, x2)  =  quotI_in_ga(x1)
quotI_out_ga(x1, x2)  =  quotI_out_ga(x1, x2)
U17_ga(x1, x2, x3)  =  U17_ga(x1, x3)
U11_gga(x1, x2, x3)  =  U11_gga(x1, x3)
quotJ_in_ga(x1, x2)  =  quotJ_in_ga(x1)
quotJ_out_ga(x1, x2)  =  quotJ_out_ga(x1, x2)
U18_ga(x1, x2, x3)  =  U18_ga(x1, x3)
divA_out_gga(x1, x2, x3)  =  divA_out_gga(x1, x2, x3)
QUOTD_IN_GA(x1, x2)  =  QUOTD_IN_GA(x1)

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

(50) UsableRulesProof (EQUIVALENT transformation)

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

(51) Obligation:

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

QUOTD_IN_GA(s(s(s(s(s(s(s(T336))))))), s(T338)) → QUOTD_IN_GA(T336, T338)

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

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

(52) PiDPToQDPProof (SOUND transformation)

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

(53) Obligation:

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

QUOTD_IN_GA(s(s(s(s(s(s(s(T336)))))))) → QUOTD_IN_GA(T336)

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

(54) QDPSizeChangeProof (EQUIVALENT transformation)

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

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

  • QUOTD_IN_GA(s(s(s(s(s(s(s(T336)))))))) → QUOTD_IN_GA(T336)
    The graph contains the following edges 1 > 1

(55) YES

(56) Obligation:

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

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

The TRS R consists of the following rules:

divA_in_gga(T7, T8, T10) → U1_gga(T7, T8, T10, quotB_in_gga(T7, T8, T10))
quotB_in_gga(0, s(T15), 0) → quotB_out_gga(0, s(T15), 0)
quotB_in_gga(s(0), s(s(T38)), 0) → quotB_out_gga(s(0), s(s(T38)), 0)
quotB_in_gga(s(s(0)), s(s(s(T61))), 0) → quotB_out_gga(s(s(0)), s(s(s(T61))), 0)
quotB_in_gga(s(s(s(0))), s(s(s(s(T84)))), 0) → quotB_out_gga(s(s(s(0))), s(s(s(s(T84)))), 0)
quotB_in_gga(s(s(s(s(0)))), s(s(s(s(s(T107))))), 0) → quotB_out_gga(s(s(s(s(0)))), s(s(s(s(s(T107))))), 0)
quotB_in_gga(s(s(s(s(s(0))))), s(s(s(s(s(s(T130)))))), 0) → quotB_out_gga(s(s(s(s(s(0))))), s(s(s(s(s(s(T130)))))), 0)
quotB_in_gga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T153))))))), 0) → quotB_out_gga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T153))))))), 0)
quotB_in_gga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(T176)))))))), 0) → quotB_out_gga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(T176)))))))), 0)
quotB_in_gga(s(s(s(s(s(s(s(s(T189)))))))), s(s(s(s(s(s(s(s(T190)))))))), T192) → U4_gga(T189, T190, T192, quotC_in_ggga(T189, T190, s(s(s(s(s(s(s(T190))))))), T192))
quotC_in_ggga(0, s(T208), T209, 0) → quotC_out_ggga(0, s(T208), T209, 0)
quotC_in_ggga(s(T226), s(T227), T228, T230) → U2_ggga(T226, T227, T228, T230, quotC_in_ggga(T226, T227, T228, T230))
quotC_in_ggga(T241, 0, T242, s(T244)) → U3_ggga(T241, T242, T244, quotB_in_gga(T241, s(T242), T244))
quotB_in_gga(s(s(s(s(s(s(s(T251))))))), s(s(s(s(s(s(s(0))))))), s(T253)) → U5_gga(T251, T253, quotD_in_ga(T251, T253))
quotD_in_ga(0, 0) → quotD_out_ga(0, 0)
quotD_in_ga(s(0), 0) → quotD_out_ga(s(0), 0)
quotD_in_ga(s(s(0)), 0) → quotD_out_ga(s(s(0)), 0)
quotD_in_ga(s(s(s(0))), 0) → quotD_out_ga(s(s(s(0))), 0)
quotD_in_ga(s(s(s(s(0)))), 0) → quotD_out_ga(s(s(s(s(0)))), 0)
quotD_in_ga(s(s(s(s(s(0))))), 0) → quotD_out_ga(s(s(s(s(s(0))))), 0)
quotD_in_ga(s(s(s(s(s(s(0)))))), 0) → quotD_out_ga(s(s(s(s(s(s(0)))))), 0)
quotD_in_ga(s(s(s(s(s(s(s(T336))))))), s(T338)) → U12_ga(T336, T338, quotD_in_ga(T336, T338))
U12_ga(T336, T338, quotD_out_ga(T336, T338)) → quotD_out_ga(s(s(s(s(s(s(s(T336))))))), s(T338))
U5_gga(T251, T253, quotD_out_ga(T251, T253)) → quotB_out_gga(s(s(s(s(s(s(s(T251))))))), s(s(s(s(s(s(s(0))))))), s(T253))
quotB_in_gga(s(s(s(s(s(s(T350)))))), s(s(s(s(s(s(0)))))), s(T352)) → U6_gga(T350, T352, quotE_in_ga(T350, T352))
quotE_in_ga(0, 0) → quotE_out_ga(0, 0)
quotE_in_ga(s(0), 0) → quotE_out_ga(s(0), 0)
quotE_in_ga(s(s(0)), 0) → quotE_out_ga(s(s(0)), 0)
quotE_in_ga(s(s(s(0))), 0) → quotE_out_ga(s(s(s(0))), 0)
quotE_in_ga(s(s(s(s(0)))), 0) → quotE_out_ga(s(s(s(s(0)))), 0)
quotE_in_ga(s(s(s(s(s(0))))), 0) → quotE_out_ga(s(s(s(s(s(0))))), 0)
quotE_in_ga(s(s(s(s(s(s(T424)))))), s(T426)) → U13_ga(T424, T426, quotE_in_ga(T424, T426))
U13_ga(T424, T426, quotE_out_ga(T424, T426)) → quotE_out_ga(s(s(s(s(s(s(T424)))))), s(T426))
U6_gga(T350, T352, quotE_out_ga(T350, T352)) → quotB_out_gga(s(s(s(s(s(s(T350)))))), s(s(s(s(s(s(0)))))), s(T352))
quotB_in_gga(s(s(s(s(s(T437))))), s(s(s(s(s(0))))), s(T439)) → U7_gga(T437, T439, quotF_in_ga(T437, T439))
quotF_in_ga(0, 0) → quotF_out_ga(0, 0)
quotF_in_ga(s(0), 0) → quotF_out_ga(s(0), 0)
quotF_in_ga(s(s(0)), 0) → quotF_out_ga(s(s(0)), 0)
quotF_in_ga(s(s(s(0))), 0) → quotF_out_ga(s(s(s(0))), 0)
quotF_in_ga(s(s(s(s(0)))), 0) → quotF_out_ga(s(s(s(s(0)))), 0)
quotF_in_ga(s(s(s(s(s(T500))))), s(T502)) → U14_ga(T500, T502, quotF_in_ga(T500, T502))
U14_ga(T500, T502, quotF_out_ga(T500, T502)) → quotF_out_ga(s(s(s(s(s(T500))))), s(T502))
U7_gga(T437, T439, quotF_out_ga(T437, T439)) → quotB_out_gga(s(s(s(s(s(T437))))), s(s(s(s(s(0))))), s(T439))
quotB_in_gga(s(s(s(s(T512)))), s(s(s(s(0)))), s(T514)) → U8_gga(T512, T514, quotG_in_ga(T512, T514))
quotG_in_ga(0, 0) → quotG_out_ga(0, 0)
quotG_in_ga(s(0), 0) → quotG_out_ga(s(0), 0)
quotG_in_ga(s(s(0)), 0) → quotG_out_ga(s(s(0)), 0)
quotG_in_ga(s(s(s(0))), 0) → quotG_out_ga(s(s(s(0))), 0)
quotG_in_ga(s(s(s(s(T564)))), s(T566)) → U15_ga(T564, T566, quotG_in_ga(T564, T566))
U15_ga(T564, T566, quotG_out_ga(T564, T566)) → quotG_out_ga(s(s(s(s(T564)))), s(T566))
U8_gga(T512, T514, quotG_out_ga(T512, T514)) → quotB_out_gga(s(s(s(s(T512)))), s(s(s(s(0)))), s(T514))
quotB_in_gga(s(s(s(T575))), s(s(s(0))), s(T577)) → U9_gga(T575, T577, quotH_in_ga(T575, T577))
quotH_in_ga(0, 0) → quotH_out_ga(0, 0)
quotH_in_ga(s(0), 0) → quotH_out_ga(s(0), 0)
quotH_in_ga(s(s(0)), 0) → quotH_out_ga(s(s(0)), 0)
quotH_in_ga(s(s(s(T616))), s(T618)) → U16_ga(T616, T618, quotH_in_ga(T616, T618))
U16_ga(T616, T618, quotH_out_ga(T616, T618)) → quotH_out_ga(s(s(s(T616))), s(T618))
U9_gga(T575, T577, quotH_out_ga(T575, T577)) → quotB_out_gga(s(s(s(T575))), s(s(s(0))), s(T577))
quotB_in_gga(s(s(T626)), s(s(0)), s(T628)) → U10_gga(T626, T628, quotI_in_ga(T626, T628))
quotI_in_ga(0, 0) → quotI_out_ga(0, 0)
quotI_in_ga(s(0), 0) → quotI_out_ga(s(0), 0)
quotI_in_ga(s(s(T656)), s(T658)) → U17_ga(T656, T658, quotI_in_ga(T656, T658))
U17_ga(T656, T658, quotI_out_ga(T656, T658)) → quotI_out_ga(s(s(T656)), s(T658))
U10_gga(T626, T628, quotI_out_ga(T626, T628)) → quotB_out_gga(s(s(T626)), s(s(0)), s(T628))
quotB_in_gga(s(T665), s(0), s(T667)) → U11_gga(T665, T667, quotJ_in_ga(T665, T667))
quotJ_in_ga(0, 0) → quotJ_out_ga(0, 0)
quotJ_in_ga(s(T684), s(T686)) → U18_ga(T684, T686, quotJ_in_ga(T684, T686))
U18_ga(T684, T686, quotJ_out_ga(T684, T686)) → quotJ_out_ga(s(T684), s(T686))
U11_gga(T665, T667, quotJ_out_ga(T665, T667)) → quotB_out_gga(s(T665), s(0), s(T667))
U3_ggga(T241, T242, T244, quotB_out_gga(T241, s(T242), T244)) → quotC_out_ggga(T241, 0, T242, s(T244))
U2_ggga(T226, T227, T228, T230, quotC_out_ggga(T226, T227, T228, T230)) → quotC_out_ggga(s(T226), s(T227), T228, T230)
U4_gga(T189, T190, T192, quotC_out_ggga(T189, T190, s(s(s(s(s(s(s(T190))))))), T192)) → quotB_out_gga(s(s(s(s(s(s(s(s(T189)))))))), s(s(s(s(s(s(s(s(T190)))))))), T192)
U1_gga(T7, T8, T10, quotB_out_gga(T7, T8, T10)) → divA_out_gga(T7, T8, T10)

The argument filtering Pi contains the following mapping:
divA_in_gga(x1, x2, x3)  =  divA_in_gga(x1, x2)
U1_gga(x1, x2, x3, x4)  =  U1_gga(x1, x2, x4)
quotB_in_gga(x1, x2, x3)  =  quotB_in_gga(x1, x2)
0  =  0
s(x1)  =  s(x1)
quotB_out_gga(x1, x2, x3)  =  quotB_out_gga(x1, x2, x3)
U4_gga(x1, x2, x3, x4)  =  U4_gga(x1, x2, x4)
quotC_in_ggga(x1, x2, x3, x4)  =  quotC_in_ggga(x1, x2, x3)
quotC_out_ggga(x1, x2, x3, x4)  =  quotC_out_ggga(x1, x2, x3, x4)
U2_ggga(x1, x2, x3, x4, x5)  =  U2_ggga(x1, x2, x3, x5)
U3_ggga(x1, x2, x3, x4)  =  U3_ggga(x1, x2, x4)
U5_gga(x1, x2, x3)  =  U5_gga(x1, x3)
quotD_in_ga(x1, x2)  =  quotD_in_ga(x1)
quotD_out_ga(x1, x2)  =  quotD_out_ga(x1, x2)
U12_ga(x1, x2, x3)  =  U12_ga(x1, x3)
U6_gga(x1, x2, x3)  =  U6_gga(x1, x3)
quotE_in_ga(x1, x2)  =  quotE_in_ga(x1)
quotE_out_ga(x1, x2)  =  quotE_out_ga(x1, x2)
U13_ga(x1, x2, x3)  =  U13_ga(x1, x3)
U7_gga(x1, x2, x3)  =  U7_gga(x1, x3)
quotF_in_ga(x1, x2)  =  quotF_in_ga(x1)
quotF_out_ga(x1, x2)  =  quotF_out_ga(x1, x2)
U14_ga(x1, x2, x3)  =  U14_ga(x1, x3)
U8_gga(x1, x2, x3)  =  U8_gga(x1, x3)
quotG_in_ga(x1, x2)  =  quotG_in_ga(x1)
quotG_out_ga(x1, x2)  =  quotG_out_ga(x1, x2)
U15_ga(x1, x2, x3)  =  U15_ga(x1, x3)
U9_gga(x1, x2, x3)  =  U9_gga(x1, x3)
quotH_in_ga(x1, x2)  =  quotH_in_ga(x1)
quotH_out_ga(x1, x2)  =  quotH_out_ga(x1, x2)
U16_ga(x1, x2, x3)  =  U16_ga(x1, x3)
U10_gga(x1, x2, x3)  =  U10_gga(x1, x3)
quotI_in_ga(x1, x2)  =  quotI_in_ga(x1)
quotI_out_ga(x1, x2)  =  quotI_out_ga(x1, x2)
U17_ga(x1, x2, x3)  =  U17_ga(x1, x3)
U11_gga(x1, x2, x3)  =  U11_gga(x1, x3)
quotJ_in_ga(x1, x2)  =  quotJ_in_ga(x1)
quotJ_out_ga(x1, x2)  =  quotJ_out_ga(x1, x2)
U18_ga(x1, x2, x3)  =  U18_ga(x1, x3)
divA_out_gga(x1, x2, x3)  =  divA_out_gga(x1, x2, x3)
QUOTB_IN_GGA(x1, x2, x3)  =  QUOTB_IN_GGA(x1, x2)
QUOTC_IN_GGGA(x1, x2, x3, x4)  =  QUOTC_IN_GGGA(x1, x2, x3)

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

(57) UsableRulesProof (EQUIVALENT transformation)

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

(58) Obligation:

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

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

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

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

(59) PiDPToQDPProof (SOUND transformation)

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

(60) Obligation:

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

QUOTB_IN_GGA(s(s(s(s(s(s(s(s(T189)))))))), s(s(s(s(s(s(s(s(T190))))))))) → QUOTC_IN_GGGA(T189, T190, s(s(s(s(s(s(s(T190))))))))
QUOTC_IN_GGGA(s(T226), s(T227), T228) → QUOTC_IN_GGGA(T226, T227, T228)
QUOTC_IN_GGGA(T241, 0, T242) → QUOTB_IN_GGA(T241, s(T242))

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

(61) QDPSizeChangeProof (EQUIVALENT transformation)

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

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

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

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

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

(62) YES