(0) Obligation:

Clauses:

div(X, Y, Z) :- quot(X, Y, Y, Z).
quot(0, s(Y), s(Z), 0).
quot(X, 0, s(Z), s(U)) :- quot(X, s(Z), s(Z), U).
quot(X, Y, Z, U) :- ','(no(zero(X)), ','(no(zero(Y)), ','(p(X, Px), ','(p(Y, Py), quot(Px, Py, Z, U))))).
p(0, 0).
p(s(X), X).
zero(0).
no(X) :- ','(X, ','(!, failure(a))).
no(X1).
failure(b).

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(T68)), 0) → quotB_out_gga(s(0), s(s(T68)), 0)
quotB_in_gga(s(T77), s(0), s(T79)) → U11_gga(T77, T79, quotC_in_ga(T77, T79))
quotC_in_ga(0, 0) → quotC_out_ga(0, 0)
quotC_in_ga(s(T106), s(T108)) → U2_ga(T106, T108, quotC_in_ga(T106, T108))
U2_ga(T106, T108, quotC_out_ga(T106, T108)) → quotC_out_ga(s(T106), s(T108))
U11_gga(T77, T79, quotC_out_ga(T77, T79)) → quotB_out_gga(s(T77), s(0), s(T79))
quotB_in_gga(s(s(0)), s(s(s(T174))), 0) → quotB_out_gga(s(s(0)), s(s(s(T174))), 0)
quotB_in_gga(s(s(T183)), s(s(0)), s(T185)) → U12_gga(T183, T185, quotD_in_ga(T183, T185))
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(T230)), s(T232)) → U3_ga(T230, T232, quotD_in_ga(T230, T232))
U3_ga(T230, T232, quotD_out_ga(T230, T232)) → quotD_out_ga(s(s(T230)), s(T232))
U12_gga(T183, T185, quotD_out_ga(T183, T185)) → quotB_out_gga(s(s(T183)), s(s(0)), s(T185))
quotB_in_gga(s(s(s(0))), s(s(s(s(T298)))), 0) → quotB_out_gga(s(s(s(0))), s(s(s(s(T298)))), 0)
quotB_in_gga(s(s(s(T307))), s(s(s(0))), s(T309)) → U13_gga(T307, T309, quotE_in_ga(T307, T309))
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(T372))), s(T374)) → U4_ga(T372, T374, quotE_in_ga(T372, T374))
U4_ga(T372, T374, quotE_out_ga(T372, T374)) → quotE_out_ga(s(s(s(T372))), s(T374))
U13_gga(T307, T309, quotE_out_ga(T307, T309)) → quotB_out_gga(s(s(s(T307))), s(s(s(0))), s(T309))
quotB_in_gga(s(s(s(s(0)))), s(s(s(s(s(T440))))), 0) → quotB_out_gga(s(s(s(s(0)))), s(s(s(s(s(T440))))), 0)
quotB_in_gga(s(s(s(s(T449)))), s(s(s(s(0)))), s(T451)) → U14_gga(T449, T451, quotF_in_ga(T449, T451))
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(T532)))), s(T534)) → U5_ga(T532, T534, quotF_in_ga(T532, T534))
U5_ga(T532, T534, quotF_out_ga(T532, T534)) → quotF_out_ga(s(s(s(s(T532)))), s(T534))
U14_gga(T449, T451, quotF_out_ga(T449, T451)) → quotB_out_gga(s(s(s(s(T449)))), s(s(s(s(0)))), s(T451))
quotB_in_gga(s(s(s(s(s(0))))), s(s(s(s(s(s(T600)))))), 0) → quotB_out_gga(s(s(s(s(s(0))))), s(s(s(s(s(s(T600)))))), 0)
quotB_in_gga(s(s(s(s(s(T609))))), s(s(s(s(s(0))))), s(T611)) → U15_gga(T609, T611, quotG_in_ga(T609, T611))
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(0)))), 0) → quotG_out_ga(s(s(s(s(0)))), 0)
quotG_in_ga(s(s(s(s(s(T710))))), s(T712)) → U6_ga(T710, T712, quotG_in_ga(T710, T712))
U6_ga(T710, T712, quotG_out_ga(T710, T712)) → quotG_out_ga(s(s(s(s(s(T710))))), s(T712))
U15_gga(T609, T611, quotG_out_ga(T609, T611)) → quotB_out_gga(s(s(s(s(s(T609))))), s(s(s(s(s(0))))), s(T611))
quotB_in_gga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T778))))))), 0) → quotB_out_gga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T778))))))), 0)
quotB_in_gga(s(s(s(s(s(s(T787)))))), s(s(s(s(s(s(0)))))), s(T789)) → U16_gga(T787, T789, quotH_in_ga(T787, T789))
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(0))), 0) → quotH_out_ga(s(s(s(0))), 0)
quotH_in_ga(s(s(s(s(0)))), 0) → quotH_out_ga(s(s(s(s(0)))), 0)
quotH_in_ga(s(s(s(s(s(0))))), 0) → quotH_out_ga(s(s(s(s(s(0))))), 0)
quotH_in_ga(s(s(s(s(s(s(T906)))))), s(T908)) → U7_ga(T906, T908, quotH_in_ga(T906, T908))
U7_ga(T906, T908, quotH_out_ga(T906, T908)) → quotH_out_ga(s(s(s(s(s(s(T906)))))), s(T908))
U16_gga(T787, T789, quotH_out_ga(T787, T789)) → quotB_out_gga(s(s(s(s(s(s(T787)))))), s(s(s(s(s(s(0)))))), s(T789))
quotB_in_gga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(T974)))))))), 0) → quotB_out_gga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(T974)))))))), 0)
quotB_in_gga(s(s(s(s(s(s(s(T983))))))), s(s(s(s(s(s(s(0))))))), s(T985)) → U17_gga(T983, T985, quotI_in_ga(T983, T985))
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(0)), 0) → quotI_out_ga(s(s(0)), 0)
quotI_in_ga(s(s(s(0))), 0) → quotI_out_ga(s(s(s(0))), 0)
quotI_in_ga(s(s(s(s(0)))), 0) → quotI_out_ga(s(s(s(s(0)))), 0)
quotI_in_ga(s(s(s(s(s(0))))), 0) → quotI_out_ga(s(s(s(s(s(0))))), 0)
quotI_in_ga(s(s(s(s(s(s(0)))))), 0) → quotI_out_ga(s(s(s(s(s(s(0)))))), 0)
quotI_in_ga(s(s(s(s(s(s(s(T1120))))))), s(T1122)) → U8_ga(T1120, T1122, quotI_in_ga(T1120, T1122))
U8_ga(T1120, T1122, quotI_out_ga(T1120, T1122)) → quotI_out_ga(s(s(s(s(s(s(s(T1120))))))), s(T1122))
U17_gga(T983, T985, quotI_out_ga(T983, T985)) → quotB_out_gga(s(s(s(s(s(s(s(T983))))))), s(s(s(s(s(s(s(0))))))), s(T985))
quotB_in_gga(s(s(s(s(s(s(s(s(T1176)))))))), s(s(s(s(s(s(s(s(T1181)))))))), T1149) → U18_gga(T1176, T1181, T1149, quotJ_in_ggga(T1176, T1181, s(s(s(s(s(s(s(T1181))))))), T1149))
quotJ_in_ggga(0, s(T1197), T1198, 0) → quotJ_out_ggga(0, s(T1197), T1198, 0)
quotJ_in_ggga(T1211, 0, T1212, s(T1214)) → U9_ggga(T1211, T1212, T1214, quotB_in_gga(T1211, s(T1212), T1214))
U9_ggga(T1211, T1212, T1214, quotB_out_gga(T1211, s(T1212), T1214)) → quotJ_out_ggga(T1211, 0, T1212, s(T1214))
quotJ_in_ggga(s(T1261), s(T1266), T1230, T1232) → U10_ggga(T1261, T1266, T1230, T1232, quotJ_in_ggga(T1261, T1266, T1230, T1232))
U10_ggga(T1261, T1266, T1230, T1232, quotJ_out_ggga(T1261, T1266, T1230, T1232)) → quotJ_out_ggga(s(T1261), s(T1266), T1230, T1232)
U18_gga(T1176, T1181, T1149, quotJ_out_ggga(T1176, T1181, s(s(s(s(s(s(s(T1181))))))), T1149)) → quotB_out_gga(s(s(s(s(s(s(s(s(T1176)))))))), s(s(s(s(s(s(s(s(T1181)))))))), T1149)
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)
U11_gga(x1, x2, x3)  =  U11_gga(x1, x3)
quotC_in_ga(x1, x2)  =  quotC_in_ga(x1)
quotC_out_ga(x1, x2)  =  quotC_out_ga(x1, x2)
U2_ga(x1, x2, x3)  =  U2_ga(x1, x3)
U12_gga(x1, x2, x3)  =  U12_gga(x1, x3)
quotD_in_ga(x1, x2)  =  quotD_in_ga(x1)
quotD_out_ga(x1, x2)  =  quotD_out_ga(x1, x2)
U3_ga(x1, x2, x3)  =  U3_ga(x1, x3)
U13_gga(x1, x2, x3)  =  U13_gga(x1, x3)
quotE_in_ga(x1, x2)  =  quotE_in_ga(x1)
quotE_out_ga(x1, x2)  =  quotE_out_ga(x1, x2)
U4_ga(x1, x2, x3)  =  U4_ga(x1, x3)
U14_gga(x1, x2, x3)  =  U14_gga(x1, x3)
quotF_in_ga(x1, x2)  =  quotF_in_ga(x1)
quotF_out_ga(x1, x2)  =  quotF_out_ga(x1, x2)
U5_ga(x1, x2, x3)  =  U5_ga(x1, x3)
U15_gga(x1, x2, x3)  =  U15_gga(x1, x3)
quotG_in_ga(x1, x2)  =  quotG_in_ga(x1)
quotG_out_ga(x1, x2)  =  quotG_out_ga(x1, x2)
U6_ga(x1, x2, x3)  =  U6_ga(x1, x3)
U16_gga(x1, x2, x3)  =  U16_gga(x1, x3)
quotH_in_ga(x1, x2)  =  quotH_in_ga(x1)
quotH_out_ga(x1, x2)  =  quotH_out_ga(x1, x2)
U7_ga(x1, x2, x3)  =  U7_ga(x1, x3)
U17_gga(x1, x2, x3)  =  U17_gga(x1, x3)
quotI_in_ga(x1, x2)  =  quotI_in_ga(x1)
quotI_out_ga(x1, x2)  =  quotI_out_ga(x1, x2)
U8_ga(x1, x2, x3)  =  U8_ga(x1, x3)
U18_gga(x1, x2, x3, x4)  =  U18_gga(x1, x2, x4)
quotJ_in_ggga(x1, x2, x3, x4)  =  quotJ_in_ggga(x1, x2, x3)
quotJ_out_ggga(x1, x2, x3, x4)  =  quotJ_out_ggga(x1, x2, x3, x4)
U9_ggga(x1, x2, x3, x4)  =  U9_ggga(x1, x2, x4)
U10_ggga(x1, x2, x3, x4, x5)  =  U10_ggga(x1, x2, x3, x5)
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(T77), s(0), s(T79)) → U11_GGA(T77, T79, quotC_in_ga(T77, T79))
QUOTB_IN_GGA(s(T77), s(0), s(T79)) → QUOTC_IN_GA(T77, T79)
QUOTC_IN_GA(s(T106), s(T108)) → U2_GA(T106, T108, quotC_in_ga(T106, T108))
QUOTC_IN_GA(s(T106), s(T108)) → QUOTC_IN_GA(T106, T108)
QUOTB_IN_GGA(s(s(T183)), s(s(0)), s(T185)) → U12_GGA(T183, T185, quotD_in_ga(T183, T185))
QUOTB_IN_GGA(s(s(T183)), s(s(0)), s(T185)) → QUOTD_IN_GA(T183, T185)
QUOTD_IN_GA(s(s(T230)), s(T232)) → U3_GA(T230, T232, quotD_in_ga(T230, T232))
QUOTD_IN_GA(s(s(T230)), s(T232)) → QUOTD_IN_GA(T230, T232)
QUOTB_IN_GGA(s(s(s(T307))), s(s(s(0))), s(T309)) → U13_GGA(T307, T309, quotE_in_ga(T307, T309))
QUOTB_IN_GGA(s(s(s(T307))), s(s(s(0))), s(T309)) → QUOTE_IN_GA(T307, T309)
QUOTE_IN_GA(s(s(s(T372))), s(T374)) → U4_GA(T372, T374, quotE_in_ga(T372, T374))
QUOTE_IN_GA(s(s(s(T372))), s(T374)) → QUOTE_IN_GA(T372, T374)
QUOTB_IN_GGA(s(s(s(s(T449)))), s(s(s(s(0)))), s(T451)) → U14_GGA(T449, T451, quotF_in_ga(T449, T451))
QUOTB_IN_GGA(s(s(s(s(T449)))), s(s(s(s(0)))), s(T451)) → QUOTF_IN_GA(T449, T451)
QUOTF_IN_GA(s(s(s(s(T532)))), s(T534)) → U5_GA(T532, T534, quotF_in_ga(T532, T534))
QUOTF_IN_GA(s(s(s(s(T532)))), s(T534)) → QUOTF_IN_GA(T532, T534)
QUOTB_IN_GGA(s(s(s(s(s(T609))))), s(s(s(s(s(0))))), s(T611)) → U15_GGA(T609, T611, quotG_in_ga(T609, T611))
QUOTB_IN_GGA(s(s(s(s(s(T609))))), s(s(s(s(s(0))))), s(T611)) → QUOTG_IN_GA(T609, T611)
QUOTG_IN_GA(s(s(s(s(s(T710))))), s(T712)) → U6_GA(T710, T712, quotG_in_ga(T710, T712))
QUOTG_IN_GA(s(s(s(s(s(T710))))), s(T712)) → QUOTG_IN_GA(T710, T712)
QUOTB_IN_GGA(s(s(s(s(s(s(T787)))))), s(s(s(s(s(s(0)))))), s(T789)) → U16_GGA(T787, T789, quotH_in_ga(T787, T789))
QUOTB_IN_GGA(s(s(s(s(s(s(T787)))))), s(s(s(s(s(s(0)))))), s(T789)) → QUOTH_IN_GA(T787, T789)
QUOTH_IN_GA(s(s(s(s(s(s(T906)))))), s(T908)) → U7_GA(T906, T908, quotH_in_ga(T906, T908))
QUOTH_IN_GA(s(s(s(s(s(s(T906)))))), s(T908)) → QUOTH_IN_GA(T906, T908)
QUOTB_IN_GGA(s(s(s(s(s(s(s(T983))))))), s(s(s(s(s(s(s(0))))))), s(T985)) → U17_GGA(T983, T985, quotI_in_ga(T983, T985))
QUOTB_IN_GGA(s(s(s(s(s(s(s(T983))))))), s(s(s(s(s(s(s(0))))))), s(T985)) → QUOTI_IN_GA(T983, T985)
QUOTI_IN_GA(s(s(s(s(s(s(s(T1120))))))), s(T1122)) → U8_GA(T1120, T1122, quotI_in_ga(T1120, T1122))
QUOTI_IN_GA(s(s(s(s(s(s(s(T1120))))))), s(T1122)) → QUOTI_IN_GA(T1120, T1122)
QUOTB_IN_GGA(s(s(s(s(s(s(s(s(T1176)))))))), s(s(s(s(s(s(s(s(T1181)))))))), T1149) → U18_GGA(T1176, T1181, T1149, quotJ_in_ggga(T1176, T1181, s(s(s(s(s(s(s(T1181))))))), T1149))
QUOTB_IN_GGA(s(s(s(s(s(s(s(s(T1176)))))))), s(s(s(s(s(s(s(s(T1181)))))))), T1149) → QUOTJ_IN_GGGA(T1176, T1181, s(s(s(s(s(s(s(T1181))))))), T1149)
QUOTJ_IN_GGGA(T1211, 0, T1212, s(T1214)) → U9_GGGA(T1211, T1212, T1214, quotB_in_gga(T1211, s(T1212), T1214))
QUOTJ_IN_GGGA(T1211, 0, T1212, s(T1214)) → QUOTB_IN_GGA(T1211, s(T1212), T1214)
QUOTJ_IN_GGGA(s(T1261), s(T1266), T1230, T1232) → U10_GGGA(T1261, T1266, T1230, T1232, quotJ_in_ggga(T1261, T1266, T1230, T1232))
QUOTJ_IN_GGGA(s(T1261), s(T1266), T1230, T1232) → QUOTJ_IN_GGGA(T1261, T1266, T1230, T1232)

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(T68)), 0) → quotB_out_gga(s(0), s(s(T68)), 0)
quotB_in_gga(s(T77), s(0), s(T79)) → U11_gga(T77, T79, quotC_in_ga(T77, T79))
quotC_in_ga(0, 0) → quotC_out_ga(0, 0)
quotC_in_ga(s(T106), s(T108)) → U2_ga(T106, T108, quotC_in_ga(T106, T108))
U2_ga(T106, T108, quotC_out_ga(T106, T108)) → quotC_out_ga(s(T106), s(T108))
U11_gga(T77, T79, quotC_out_ga(T77, T79)) → quotB_out_gga(s(T77), s(0), s(T79))
quotB_in_gga(s(s(0)), s(s(s(T174))), 0) → quotB_out_gga(s(s(0)), s(s(s(T174))), 0)
quotB_in_gga(s(s(T183)), s(s(0)), s(T185)) → U12_gga(T183, T185, quotD_in_ga(T183, T185))
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(T230)), s(T232)) → U3_ga(T230, T232, quotD_in_ga(T230, T232))
U3_ga(T230, T232, quotD_out_ga(T230, T232)) → quotD_out_ga(s(s(T230)), s(T232))
U12_gga(T183, T185, quotD_out_ga(T183, T185)) → quotB_out_gga(s(s(T183)), s(s(0)), s(T185))
quotB_in_gga(s(s(s(0))), s(s(s(s(T298)))), 0) → quotB_out_gga(s(s(s(0))), s(s(s(s(T298)))), 0)
quotB_in_gga(s(s(s(T307))), s(s(s(0))), s(T309)) → U13_gga(T307, T309, quotE_in_ga(T307, T309))
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(T372))), s(T374)) → U4_ga(T372, T374, quotE_in_ga(T372, T374))
U4_ga(T372, T374, quotE_out_ga(T372, T374)) → quotE_out_ga(s(s(s(T372))), s(T374))
U13_gga(T307, T309, quotE_out_ga(T307, T309)) → quotB_out_gga(s(s(s(T307))), s(s(s(0))), s(T309))
quotB_in_gga(s(s(s(s(0)))), s(s(s(s(s(T440))))), 0) → quotB_out_gga(s(s(s(s(0)))), s(s(s(s(s(T440))))), 0)
quotB_in_gga(s(s(s(s(T449)))), s(s(s(s(0)))), s(T451)) → U14_gga(T449, T451, quotF_in_ga(T449, T451))
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(T532)))), s(T534)) → U5_ga(T532, T534, quotF_in_ga(T532, T534))
U5_ga(T532, T534, quotF_out_ga(T532, T534)) → quotF_out_ga(s(s(s(s(T532)))), s(T534))
U14_gga(T449, T451, quotF_out_ga(T449, T451)) → quotB_out_gga(s(s(s(s(T449)))), s(s(s(s(0)))), s(T451))
quotB_in_gga(s(s(s(s(s(0))))), s(s(s(s(s(s(T600)))))), 0) → quotB_out_gga(s(s(s(s(s(0))))), s(s(s(s(s(s(T600)))))), 0)
quotB_in_gga(s(s(s(s(s(T609))))), s(s(s(s(s(0))))), s(T611)) → U15_gga(T609, T611, quotG_in_ga(T609, T611))
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(0)))), 0) → quotG_out_ga(s(s(s(s(0)))), 0)
quotG_in_ga(s(s(s(s(s(T710))))), s(T712)) → U6_ga(T710, T712, quotG_in_ga(T710, T712))
U6_ga(T710, T712, quotG_out_ga(T710, T712)) → quotG_out_ga(s(s(s(s(s(T710))))), s(T712))
U15_gga(T609, T611, quotG_out_ga(T609, T611)) → quotB_out_gga(s(s(s(s(s(T609))))), s(s(s(s(s(0))))), s(T611))
quotB_in_gga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T778))))))), 0) → quotB_out_gga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T778))))))), 0)
quotB_in_gga(s(s(s(s(s(s(T787)))))), s(s(s(s(s(s(0)))))), s(T789)) → U16_gga(T787, T789, quotH_in_ga(T787, T789))
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(0))), 0) → quotH_out_ga(s(s(s(0))), 0)
quotH_in_ga(s(s(s(s(0)))), 0) → quotH_out_ga(s(s(s(s(0)))), 0)
quotH_in_ga(s(s(s(s(s(0))))), 0) → quotH_out_ga(s(s(s(s(s(0))))), 0)
quotH_in_ga(s(s(s(s(s(s(T906)))))), s(T908)) → U7_ga(T906, T908, quotH_in_ga(T906, T908))
U7_ga(T906, T908, quotH_out_ga(T906, T908)) → quotH_out_ga(s(s(s(s(s(s(T906)))))), s(T908))
U16_gga(T787, T789, quotH_out_ga(T787, T789)) → quotB_out_gga(s(s(s(s(s(s(T787)))))), s(s(s(s(s(s(0)))))), s(T789))
quotB_in_gga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(T974)))))))), 0) → quotB_out_gga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(T974)))))))), 0)
quotB_in_gga(s(s(s(s(s(s(s(T983))))))), s(s(s(s(s(s(s(0))))))), s(T985)) → U17_gga(T983, T985, quotI_in_ga(T983, T985))
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(0)), 0) → quotI_out_ga(s(s(0)), 0)
quotI_in_ga(s(s(s(0))), 0) → quotI_out_ga(s(s(s(0))), 0)
quotI_in_ga(s(s(s(s(0)))), 0) → quotI_out_ga(s(s(s(s(0)))), 0)
quotI_in_ga(s(s(s(s(s(0))))), 0) → quotI_out_ga(s(s(s(s(s(0))))), 0)
quotI_in_ga(s(s(s(s(s(s(0)))))), 0) → quotI_out_ga(s(s(s(s(s(s(0)))))), 0)
quotI_in_ga(s(s(s(s(s(s(s(T1120))))))), s(T1122)) → U8_ga(T1120, T1122, quotI_in_ga(T1120, T1122))
U8_ga(T1120, T1122, quotI_out_ga(T1120, T1122)) → quotI_out_ga(s(s(s(s(s(s(s(T1120))))))), s(T1122))
U17_gga(T983, T985, quotI_out_ga(T983, T985)) → quotB_out_gga(s(s(s(s(s(s(s(T983))))))), s(s(s(s(s(s(s(0))))))), s(T985))
quotB_in_gga(s(s(s(s(s(s(s(s(T1176)))))))), s(s(s(s(s(s(s(s(T1181)))))))), T1149) → U18_gga(T1176, T1181, T1149, quotJ_in_ggga(T1176, T1181, s(s(s(s(s(s(s(T1181))))))), T1149))
quotJ_in_ggga(0, s(T1197), T1198, 0) → quotJ_out_ggga(0, s(T1197), T1198, 0)
quotJ_in_ggga(T1211, 0, T1212, s(T1214)) → U9_ggga(T1211, T1212, T1214, quotB_in_gga(T1211, s(T1212), T1214))
U9_ggga(T1211, T1212, T1214, quotB_out_gga(T1211, s(T1212), T1214)) → quotJ_out_ggga(T1211, 0, T1212, s(T1214))
quotJ_in_ggga(s(T1261), s(T1266), T1230, T1232) → U10_ggga(T1261, T1266, T1230, T1232, quotJ_in_ggga(T1261, T1266, T1230, T1232))
U10_ggga(T1261, T1266, T1230, T1232, quotJ_out_ggga(T1261, T1266, T1230, T1232)) → quotJ_out_ggga(s(T1261), s(T1266), T1230, T1232)
U18_gga(T1176, T1181, T1149, quotJ_out_ggga(T1176, T1181, s(s(s(s(s(s(s(T1181))))))), T1149)) → quotB_out_gga(s(s(s(s(s(s(s(s(T1176)))))))), s(s(s(s(s(s(s(s(T1181)))))))), T1149)
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)
U11_gga(x1, x2, x3)  =  U11_gga(x1, x3)
quotC_in_ga(x1, x2)  =  quotC_in_ga(x1)
quotC_out_ga(x1, x2)  =  quotC_out_ga(x1, x2)
U2_ga(x1, x2, x3)  =  U2_ga(x1, x3)
U12_gga(x1, x2, x3)  =  U12_gga(x1, x3)
quotD_in_ga(x1, x2)  =  quotD_in_ga(x1)
quotD_out_ga(x1, x2)  =  quotD_out_ga(x1, x2)
U3_ga(x1, x2, x3)  =  U3_ga(x1, x3)
U13_gga(x1, x2, x3)  =  U13_gga(x1, x3)
quotE_in_ga(x1, x2)  =  quotE_in_ga(x1)
quotE_out_ga(x1, x2)  =  quotE_out_ga(x1, x2)
U4_ga(x1, x2, x3)  =  U4_ga(x1, x3)
U14_gga(x1, x2, x3)  =  U14_gga(x1, x3)
quotF_in_ga(x1, x2)  =  quotF_in_ga(x1)
quotF_out_ga(x1, x2)  =  quotF_out_ga(x1, x2)
U5_ga(x1, x2, x3)  =  U5_ga(x1, x3)
U15_gga(x1, x2, x3)  =  U15_gga(x1, x3)
quotG_in_ga(x1, x2)  =  quotG_in_ga(x1)
quotG_out_ga(x1, x2)  =  quotG_out_ga(x1, x2)
U6_ga(x1, x2, x3)  =  U6_ga(x1, x3)
U16_gga(x1, x2, x3)  =  U16_gga(x1, x3)
quotH_in_ga(x1, x2)  =  quotH_in_ga(x1)
quotH_out_ga(x1, x2)  =  quotH_out_ga(x1, x2)
U7_ga(x1, x2, x3)  =  U7_ga(x1, x3)
U17_gga(x1, x2, x3)  =  U17_gga(x1, x3)
quotI_in_ga(x1, x2)  =  quotI_in_ga(x1)
quotI_out_ga(x1, x2)  =  quotI_out_ga(x1, x2)
U8_ga(x1, x2, x3)  =  U8_ga(x1, x3)
U18_gga(x1, x2, x3, x4)  =  U18_gga(x1, x2, x4)
quotJ_in_ggga(x1, x2, x3, x4)  =  quotJ_in_ggga(x1, x2, x3)
quotJ_out_ggga(x1, x2, x3, x4)  =  quotJ_out_ggga(x1, x2, x3, x4)
U9_ggga(x1, x2, x3, x4)  =  U9_ggga(x1, x2, x4)
U10_ggga(x1, x2, x3, x4, x5)  =  U10_ggga(x1, x2, x3, x5)
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)
U11_GGA(x1, x2, x3)  =  U11_GGA(x1, x3)
QUOTC_IN_GA(x1, x2)  =  QUOTC_IN_GA(x1)
U2_GA(x1, x2, x3)  =  U2_GA(x1, x3)
U12_GGA(x1, x2, x3)  =  U12_GGA(x1, x3)
QUOTD_IN_GA(x1, x2)  =  QUOTD_IN_GA(x1)
U3_GA(x1, x2, x3)  =  U3_GA(x1, x3)
U13_GGA(x1, x2, x3)  =  U13_GGA(x1, x3)
QUOTE_IN_GA(x1, x2)  =  QUOTE_IN_GA(x1)
U4_GA(x1, x2, x3)  =  U4_GA(x1, x3)
U14_GGA(x1, x2, x3)  =  U14_GGA(x1, x3)
QUOTF_IN_GA(x1, x2)  =  QUOTF_IN_GA(x1)
U5_GA(x1, x2, x3)  =  U5_GA(x1, x3)
U15_GGA(x1, x2, x3)  =  U15_GGA(x1, x3)
QUOTG_IN_GA(x1, x2)  =  QUOTG_IN_GA(x1)
U6_GA(x1, x2, x3)  =  U6_GA(x1, x3)
U16_GGA(x1, x2, x3)  =  U16_GGA(x1, x3)
QUOTH_IN_GA(x1, x2)  =  QUOTH_IN_GA(x1)
U7_GA(x1, x2, x3)  =  U7_GA(x1, x3)
U17_GGA(x1, x2, x3)  =  U17_GGA(x1, x3)
QUOTI_IN_GA(x1, x2)  =  QUOTI_IN_GA(x1)
U8_GA(x1, x2, x3)  =  U8_GA(x1, x3)
U18_GGA(x1, x2, x3, x4)  =  U18_GGA(x1, x2, x4)
QUOTJ_IN_GGGA(x1, x2, x3, x4)  =  QUOTJ_IN_GGGA(x1, x2, x3)
U9_GGGA(x1, x2, x3, x4)  =  U9_GGGA(x1, x2, x4)
U10_GGGA(x1, x2, x3, x4, x5)  =  U10_GGGA(x1, x2, x3, x5)

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

(4) Obligation:

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

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(T77), s(0), s(T79)) → U11_GGA(T77, T79, quotC_in_ga(T77, T79))
QUOTB_IN_GGA(s(T77), s(0), s(T79)) → QUOTC_IN_GA(T77, T79)
QUOTC_IN_GA(s(T106), s(T108)) → U2_GA(T106, T108, quotC_in_ga(T106, T108))
QUOTC_IN_GA(s(T106), s(T108)) → QUOTC_IN_GA(T106, T108)
QUOTB_IN_GGA(s(s(T183)), s(s(0)), s(T185)) → U12_GGA(T183, T185, quotD_in_ga(T183, T185))
QUOTB_IN_GGA(s(s(T183)), s(s(0)), s(T185)) → QUOTD_IN_GA(T183, T185)
QUOTD_IN_GA(s(s(T230)), s(T232)) → U3_GA(T230, T232, quotD_in_ga(T230, T232))
QUOTD_IN_GA(s(s(T230)), s(T232)) → QUOTD_IN_GA(T230, T232)
QUOTB_IN_GGA(s(s(s(T307))), s(s(s(0))), s(T309)) → U13_GGA(T307, T309, quotE_in_ga(T307, T309))
QUOTB_IN_GGA(s(s(s(T307))), s(s(s(0))), s(T309)) → QUOTE_IN_GA(T307, T309)
QUOTE_IN_GA(s(s(s(T372))), s(T374)) → U4_GA(T372, T374, quotE_in_ga(T372, T374))
QUOTE_IN_GA(s(s(s(T372))), s(T374)) → QUOTE_IN_GA(T372, T374)
QUOTB_IN_GGA(s(s(s(s(T449)))), s(s(s(s(0)))), s(T451)) → U14_GGA(T449, T451, quotF_in_ga(T449, T451))
QUOTB_IN_GGA(s(s(s(s(T449)))), s(s(s(s(0)))), s(T451)) → QUOTF_IN_GA(T449, T451)
QUOTF_IN_GA(s(s(s(s(T532)))), s(T534)) → U5_GA(T532, T534, quotF_in_ga(T532, T534))
QUOTF_IN_GA(s(s(s(s(T532)))), s(T534)) → QUOTF_IN_GA(T532, T534)
QUOTB_IN_GGA(s(s(s(s(s(T609))))), s(s(s(s(s(0))))), s(T611)) → U15_GGA(T609, T611, quotG_in_ga(T609, T611))
QUOTB_IN_GGA(s(s(s(s(s(T609))))), s(s(s(s(s(0))))), s(T611)) → QUOTG_IN_GA(T609, T611)
QUOTG_IN_GA(s(s(s(s(s(T710))))), s(T712)) → U6_GA(T710, T712, quotG_in_ga(T710, T712))
QUOTG_IN_GA(s(s(s(s(s(T710))))), s(T712)) → QUOTG_IN_GA(T710, T712)
QUOTB_IN_GGA(s(s(s(s(s(s(T787)))))), s(s(s(s(s(s(0)))))), s(T789)) → U16_GGA(T787, T789, quotH_in_ga(T787, T789))
QUOTB_IN_GGA(s(s(s(s(s(s(T787)))))), s(s(s(s(s(s(0)))))), s(T789)) → QUOTH_IN_GA(T787, T789)
QUOTH_IN_GA(s(s(s(s(s(s(T906)))))), s(T908)) → U7_GA(T906, T908, quotH_in_ga(T906, T908))
QUOTH_IN_GA(s(s(s(s(s(s(T906)))))), s(T908)) → QUOTH_IN_GA(T906, T908)
QUOTB_IN_GGA(s(s(s(s(s(s(s(T983))))))), s(s(s(s(s(s(s(0))))))), s(T985)) → U17_GGA(T983, T985, quotI_in_ga(T983, T985))
QUOTB_IN_GGA(s(s(s(s(s(s(s(T983))))))), s(s(s(s(s(s(s(0))))))), s(T985)) → QUOTI_IN_GA(T983, T985)
QUOTI_IN_GA(s(s(s(s(s(s(s(T1120))))))), s(T1122)) → U8_GA(T1120, T1122, quotI_in_ga(T1120, T1122))
QUOTI_IN_GA(s(s(s(s(s(s(s(T1120))))))), s(T1122)) → QUOTI_IN_GA(T1120, T1122)
QUOTB_IN_GGA(s(s(s(s(s(s(s(s(T1176)))))))), s(s(s(s(s(s(s(s(T1181)))))))), T1149) → U18_GGA(T1176, T1181, T1149, quotJ_in_ggga(T1176, T1181, s(s(s(s(s(s(s(T1181))))))), T1149))
QUOTB_IN_GGA(s(s(s(s(s(s(s(s(T1176)))))))), s(s(s(s(s(s(s(s(T1181)))))))), T1149) → QUOTJ_IN_GGGA(T1176, T1181, s(s(s(s(s(s(s(T1181))))))), T1149)
QUOTJ_IN_GGGA(T1211, 0, T1212, s(T1214)) → U9_GGGA(T1211, T1212, T1214, quotB_in_gga(T1211, s(T1212), T1214))
QUOTJ_IN_GGGA(T1211, 0, T1212, s(T1214)) → QUOTB_IN_GGA(T1211, s(T1212), T1214)
QUOTJ_IN_GGGA(s(T1261), s(T1266), T1230, T1232) → U10_GGGA(T1261, T1266, T1230, T1232, quotJ_in_ggga(T1261, T1266, T1230, T1232))
QUOTJ_IN_GGGA(s(T1261), s(T1266), T1230, T1232) → QUOTJ_IN_GGGA(T1261, T1266, T1230, T1232)

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(T68)), 0) → quotB_out_gga(s(0), s(s(T68)), 0)
quotB_in_gga(s(T77), s(0), s(T79)) → U11_gga(T77, T79, quotC_in_ga(T77, T79))
quotC_in_ga(0, 0) → quotC_out_ga(0, 0)
quotC_in_ga(s(T106), s(T108)) → U2_ga(T106, T108, quotC_in_ga(T106, T108))
U2_ga(T106, T108, quotC_out_ga(T106, T108)) → quotC_out_ga(s(T106), s(T108))
U11_gga(T77, T79, quotC_out_ga(T77, T79)) → quotB_out_gga(s(T77), s(0), s(T79))
quotB_in_gga(s(s(0)), s(s(s(T174))), 0) → quotB_out_gga(s(s(0)), s(s(s(T174))), 0)
quotB_in_gga(s(s(T183)), s(s(0)), s(T185)) → U12_gga(T183, T185, quotD_in_ga(T183, T185))
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(T230)), s(T232)) → U3_ga(T230, T232, quotD_in_ga(T230, T232))
U3_ga(T230, T232, quotD_out_ga(T230, T232)) → quotD_out_ga(s(s(T230)), s(T232))
U12_gga(T183, T185, quotD_out_ga(T183, T185)) → quotB_out_gga(s(s(T183)), s(s(0)), s(T185))
quotB_in_gga(s(s(s(0))), s(s(s(s(T298)))), 0) → quotB_out_gga(s(s(s(0))), s(s(s(s(T298)))), 0)
quotB_in_gga(s(s(s(T307))), s(s(s(0))), s(T309)) → U13_gga(T307, T309, quotE_in_ga(T307, T309))
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(T372))), s(T374)) → U4_ga(T372, T374, quotE_in_ga(T372, T374))
U4_ga(T372, T374, quotE_out_ga(T372, T374)) → quotE_out_ga(s(s(s(T372))), s(T374))
U13_gga(T307, T309, quotE_out_ga(T307, T309)) → quotB_out_gga(s(s(s(T307))), s(s(s(0))), s(T309))
quotB_in_gga(s(s(s(s(0)))), s(s(s(s(s(T440))))), 0) → quotB_out_gga(s(s(s(s(0)))), s(s(s(s(s(T440))))), 0)
quotB_in_gga(s(s(s(s(T449)))), s(s(s(s(0)))), s(T451)) → U14_gga(T449, T451, quotF_in_ga(T449, T451))
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(T532)))), s(T534)) → U5_ga(T532, T534, quotF_in_ga(T532, T534))
U5_ga(T532, T534, quotF_out_ga(T532, T534)) → quotF_out_ga(s(s(s(s(T532)))), s(T534))
U14_gga(T449, T451, quotF_out_ga(T449, T451)) → quotB_out_gga(s(s(s(s(T449)))), s(s(s(s(0)))), s(T451))
quotB_in_gga(s(s(s(s(s(0))))), s(s(s(s(s(s(T600)))))), 0) → quotB_out_gga(s(s(s(s(s(0))))), s(s(s(s(s(s(T600)))))), 0)
quotB_in_gga(s(s(s(s(s(T609))))), s(s(s(s(s(0))))), s(T611)) → U15_gga(T609, T611, quotG_in_ga(T609, T611))
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(0)))), 0) → quotG_out_ga(s(s(s(s(0)))), 0)
quotG_in_ga(s(s(s(s(s(T710))))), s(T712)) → U6_ga(T710, T712, quotG_in_ga(T710, T712))
U6_ga(T710, T712, quotG_out_ga(T710, T712)) → quotG_out_ga(s(s(s(s(s(T710))))), s(T712))
U15_gga(T609, T611, quotG_out_ga(T609, T611)) → quotB_out_gga(s(s(s(s(s(T609))))), s(s(s(s(s(0))))), s(T611))
quotB_in_gga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T778))))))), 0) → quotB_out_gga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T778))))))), 0)
quotB_in_gga(s(s(s(s(s(s(T787)))))), s(s(s(s(s(s(0)))))), s(T789)) → U16_gga(T787, T789, quotH_in_ga(T787, T789))
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(0))), 0) → quotH_out_ga(s(s(s(0))), 0)
quotH_in_ga(s(s(s(s(0)))), 0) → quotH_out_ga(s(s(s(s(0)))), 0)
quotH_in_ga(s(s(s(s(s(0))))), 0) → quotH_out_ga(s(s(s(s(s(0))))), 0)
quotH_in_ga(s(s(s(s(s(s(T906)))))), s(T908)) → U7_ga(T906, T908, quotH_in_ga(T906, T908))
U7_ga(T906, T908, quotH_out_ga(T906, T908)) → quotH_out_ga(s(s(s(s(s(s(T906)))))), s(T908))
U16_gga(T787, T789, quotH_out_ga(T787, T789)) → quotB_out_gga(s(s(s(s(s(s(T787)))))), s(s(s(s(s(s(0)))))), s(T789))
quotB_in_gga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(T974)))))))), 0) → quotB_out_gga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(T974)))))))), 0)
quotB_in_gga(s(s(s(s(s(s(s(T983))))))), s(s(s(s(s(s(s(0))))))), s(T985)) → U17_gga(T983, T985, quotI_in_ga(T983, T985))
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(0)), 0) → quotI_out_ga(s(s(0)), 0)
quotI_in_ga(s(s(s(0))), 0) → quotI_out_ga(s(s(s(0))), 0)
quotI_in_ga(s(s(s(s(0)))), 0) → quotI_out_ga(s(s(s(s(0)))), 0)
quotI_in_ga(s(s(s(s(s(0))))), 0) → quotI_out_ga(s(s(s(s(s(0))))), 0)
quotI_in_ga(s(s(s(s(s(s(0)))))), 0) → quotI_out_ga(s(s(s(s(s(s(0)))))), 0)
quotI_in_ga(s(s(s(s(s(s(s(T1120))))))), s(T1122)) → U8_ga(T1120, T1122, quotI_in_ga(T1120, T1122))
U8_ga(T1120, T1122, quotI_out_ga(T1120, T1122)) → quotI_out_ga(s(s(s(s(s(s(s(T1120))))))), s(T1122))
U17_gga(T983, T985, quotI_out_ga(T983, T985)) → quotB_out_gga(s(s(s(s(s(s(s(T983))))))), s(s(s(s(s(s(s(0))))))), s(T985))
quotB_in_gga(s(s(s(s(s(s(s(s(T1176)))))))), s(s(s(s(s(s(s(s(T1181)))))))), T1149) → U18_gga(T1176, T1181, T1149, quotJ_in_ggga(T1176, T1181, s(s(s(s(s(s(s(T1181))))))), T1149))
quotJ_in_ggga(0, s(T1197), T1198, 0) → quotJ_out_ggga(0, s(T1197), T1198, 0)
quotJ_in_ggga(T1211, 0, T1212, s(T1214)) → U9_ggga(T1211, T1212, T1214, quotB_in_gga(T1211, s(T1212), T1214))
U9_ggga(T1211, T1212, T1214, quotB_out_gga(T1211, s(T1212), T1214)) → quotJ_out_ggga(T1211, 0, T1212, s(T1214))
quotJ_in_ggga(s(T1261), s(T1266), T1230, T1232) → U10_ggga(T1261, T1266, T1230, T1232, quotJ_in_ggga(T1261, T1266, T1230, T1232))
U10_ggga(T1261, T1266, T1230, T1232, quotJ_out_ggga(T1261, T1266, T1230, T1232)) → quotJ_out_ggga(s(T1261), s(T1266), T1230, T1232)
U18_gga(T1176, T1181, T1149, quotJ_out_ggga(T1176, T1181, s(s(s(s(s(s(s(T1181))))))), T1149)) → quotB_out_gga(s(s(s(s(s(s(s(s(T1176)))))))), s(s(s(s(s(s(s(s(T1181)))))))), T1149)
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)
U11_gga(x1, x2, x3)  =  U11_gga(x1, x3)
quotC_in_ga(x1, x2)  =  quotC_in_ga(x1)
quotC_out_ga(x1, x2)  =  quotC_out_ga(x1, x2)
U2_ga(x1, x2, x3)  =  U2_ga(x1, x3)
U12_gga(x1, x2, x3)  =  U12_gga(x1, x3)
quotD_in_ga(x1, x2)  =  quotD_in_ga(x1)
quotD_out_ga(x1, x2)  =  quotD_out_ga(x1, x2)
U3_ga(x1, x2, x3)  =  U3_ga(x1, x3)
U13_gga(x1, x2, x3)  =  U13_gga(x1, x3)
quotE_in_ga(x1, x2)  =  quotE_in_ga(x1)
quotE_out_ga(x1, x2)  =  quotE_out_ga(x1, x2)
U4_ga(x1, x2, x3)  =  U4_ga(x1, x3)
U14_gga(x1, x2, x3)  =  U14_gga(x1, x3)
quotF_in_ga(x1, x2)  =  quotF_in_ga(x1)
quotF_out_ga(x1, x2)  =  quotF_out_ga(x1, x2)
U5_ga(x1, x2, x3)  =  U5_ga(x1, x3)
U15_gga(x1, x2, x3)  =  U15_gga(x1, x3)
quotG_in_ga(x1, x2)  =  quotG_in_ga(x1)
quotG_out_ga(x1, x2)  =  quotG_out_ga(x1, x2)
U6_ga(x1, x2, x3)  =  U6_ga(x1, x3)
U16_gga(x1, x2, x3)  =  U16_gga(x1, x3)
quotH_in_ga(x1, x2)  =  quotH_in_ga(x1)
quotH_out_ga(x1, x2)  =  quotH_out_ga(x1, x2)
U7_ga(x1, x2, x3)  =  U7_ga(x1, x3)
U17_gga(x1, x2, x3)  =  U17_gga(x1, x3)
quotI_in_ga(x1, x2)  =  quotI_in_ga(x1)
quotI_out_ga(x1, x2)  =  quotI_out_ga(x1, x2)
U8_ga(x1, x2, x3)  =  U8_ga(x1, x3)
U18_gga(x1, x2, x3, x4)  =  U18_gga(x1, x2, x4)
quotJ_in_ggga(x1, x2, x3, x4)  =  quotJ_in_ggga(x1, x2, x3)
quotJ_out_ggga(x1, x2, x3, x4)  =  quotJ_out_ggga(x1, x2, x3, x4)
U9_ggga(x1, x2, x3, x4)  =  U9_ggga(x1, x2, x4)
U10_ggga(x1, x2, x3, x4, x5)  =  U10_ggga(x1, x2, x3, x5)
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)
U11_GGA(x1, x2, x3)  =  U11_GGA(x1, x3)
QUOTC_IN_GA(x1, x2)  =  QUOTC_IN_GA(x1)
U2_GA(x1, x2, x3)  =  U2_GA(x1, x3)
U12_GGA(x1, x2, x3)  =  U12_GGA(x1, x3)
QUOTD_IN_GA(x1, x2)  =  QUOTD_IN_GA(x1)
U3_GA(x1, x2, x3)  =  U3_GA(x1, x3)
U13_GGA(x1, x2, x3)  =  U13_GGA(x1, x3)
QUOTE_IN_GA(x1, x2)  =  QUOTE_IN_GA(x1)
U4_GA(x1, x2, x3)  =  U4_GA(x1, x3)
U14_GGA(x1, x2, x3)  =  U14_GGA(x1, x3)
QUOTF_IN_GA(x1, x2)  =  QUOTF_IN_GA(x1)
U5_GA(x1, x2, x3)  =  U5_GA(x1, x3)
U15_GGA(x1, x2, x3)  =  U15_GGA(x1, x3)
QUOTG_IN_GA(x1, x2)  =  QUOTG_IN_GA(x1)
U6_GA(x1, x2, x3)  =  U6_GA(x1, x3)
U16_GGA(x1, x2, x3)  =  U16_GGA(x1, x3)
QUOTH_IN_GA(x1, x2)  =  QUOTH_IN_GA(x1)
U7_GA(x1, x2, x3)  =  U7_GA(x1, x3)
U17_GGA(x1, x2, x3)  =  U17_GGA(x1, x3)
QUOTI_IN_GA(x1, x2)  =  QUOTI_IN_GA(x1)
U8_GA(x1, x2, x3)  =  U8_GA(x1, x3)
U18_GGA(x1, x2, x3, x4)  =  U18_GGA(x1, x2, x4)
QUOTJ_IN_GGGA(x1, x2, x3, x4)  =  QUOTJ_IN_GGGA(x1, x2, x3)
U9_GGGA(x1, x2, x3, x4)  =  U9_GGGA(x1, x2, x4)
U10_GGGA(x1, x2, x3, x4, x5)  =  U10_GGGA(x1, x2, x3, x5)

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

(5) DependencyGraphProof (EQUIVALENT transformation)

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

(6) Complex Obligation (AND)

(7) Obligation:

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

QUOTI_IN_GA(s(s(s(s(s(s(s(T1120))))))), s(T1122)) → QUOTI_IN_GA(T1120, T1122)

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(T68)), 0) → quotB_out_gga(s(0), s(s(T68)), 0)
quotB_in_gga(s(T77), s(0), s(T79)) → U11_gga(T77, T79, quotC_in_ga(T77, T79))
quotC_in_ga(0, 0) → quotC_out_ga(0, 0)
quotC_in_ga(s(T106), s(T108)) → U2_ga(T106, T108, quotC_in_ga(T106, T108))
U2_ga(T106, T108, quotC_out_ga(T106, T108)) → quotC_out_ga(s(T106), s(T108))
U11_gga(T77, T79, quotC_out_ga(T77, T79)) → quotB_out_gga(s(T77), s(0), s(T79))
quotB_in_gga(s(s(0)), s(s(s(T174))), 0) → quotB_out_gga(s(s(0)), s(s(s(T174))), 0)
quotB_in_gga(s(s(T183)), s(s(0)), s(T185)) → U12_gga(T183, T185, quotD_in_ga(T183, T185))
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(T230)), s(T232)) → U3_ga(T230, T232, quotD_in_ga(T230, T232))
U3_ga(T230, T232, quotD_out_ga(T230, T232)) → quotD_out_ga(s(s(T230)), s(T232))
U12_gga(T183, T185, quotD_out_ga(T183, T185)) → quotB_out_gga(s(s(T183)), s(s(0)), s(T185))
quotB_in_gga(s(s(s(0))), s(s(s(s(T298)))), 0) → quotB_out_gga(s(s(s(0))), s(s(s(s(T298)))), 0)
quotB_in_gga(s(s(s(T307))), s(s(s(0))), s(T309)) → U13_gga(T307, T309, quotE_in_ga(T307, T309))
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(T372))), s(T374)) → U4_ga(T372, T374, quotE_in_ga(T372, T374))
U4_ga(T372, T374, quotE_out_ga(T372, T374)) → quotE_out_ga(s(s(s(T372))), s(T374))
U13_gga(T307, T309, quotE_out_ga(T307, T309)) → quotB_out_gga(s(s(s(T307))), s(s(s(0))), s(T309))
quotB_in_gga(s(s(s(s(0)))), s(s(s(s(s(T440))))), 0) → quotB_out_gga(s(s(s(s(0)))), s(s(s(s(s(T440))))), 0)
quotB_in_gga(s(s(s(s(T449)))), s(s(s(s(0)))), s(T451)) → U14_gga(T449, T451, quotF_in_ga(T449, T451))
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(T532)))), s(T534)) → U5_ga(T532, T534, quotF_in_ga(T532, T534))
U5_ga(T532, T534, quotF_out_ga(T532, T534)) → quotF_out_ga(s(s(s(s(T532)))), s(T534))
U14_gga(T449, T451, quotF_out_ga(T449, T451)) → quotB_out_gga(s(s(s(s(T449)))), s(s(s(s(0)))), s(T451))
quotB_in_gga(s(s(s(s(s(0))))), s(s(s(s(s(s(T600)))))), 0) → quotB_out_gga(s(s(s(s(s(0))))), s(s(s(s(s(s(T600)))))), 0)
quotB_in_gga(s(s(s(s(s(T609))))), s(s(s(s(s(0))))), s(T611)) → U15_gga(T609, T611, quotG_in_ga(T609, T611))
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(0)))), 0) → quotG_out_ga(s(s(s(s(0)))), 0)
quotG_in_ga(s(s(s(s(s(T710))))), s(T712)) → U6_ga(T710, T712, quotG_in_ga(T710, T712))
U6_ga(T710, T712, quotG_out_ga(T710, T712)) → quotG_out_ga(s(s(s(s(s(T710))))), s(T712))
U15_gga(T609, T611, quotG_out_ga(T609, T611)) → quotB_out_gga(s(s(s(s(s(T609))))), s(s(s(s(s(0))))), s(T611))
quotB_in_gga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T778))))))), 0) → quotB_out_gga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T778))))))), 0)
quotB_in_gga(s(s(s(s(s(s(T787)))))), s(s(s(s(s(s(0)))))), s(T789)) → U16_gga(T787, T789, quotH_in_ga(T787, T789))
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(0))), 0) → quotH_out_ga(s(s(s(0))), 0)
quotH_in_ga(s(s(s(s(0)))), 0) → quotH_out_ga(s(s(s(s(0)))), 0)
quotH_in_ga(s(s(s(s(s(0))))), 0) → quotH_out_ga(s(s(s(s(s(0))))), 0)
quotH_in_ga(s(s(s(s(s(s(T906)))))), s(T908)) → U7_ga(T906, T908, quotH_in_ga(T906, T908))
U7_ga(T906, T908, quotH_out_ga(T906, T908)) → quotH_out_ga(s(s(s(s(s(s(T906)))))), s(T908))
U16_gga(T787, T789, quotH_out_ga(T787, T789)) → quotB_out_gga(s(s(s(s(s(s(T787)))))), s(s(s(s(s(s(0)))))), s(T789))
quotB_in_gga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(T974)))))))), 0) → quotB_out_gga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(T974)))))))), 0)
quotB_in_gga(s(s(s(s(s(s(s(T983))))))), s(s(s(s(s(s(s(0))))))), s(T985)) → U17_gga(T983, T985, quotI_in_ga(T983, T985))
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(0)), 0) → quotI_out_ga(s(s(0)), 0)
quotI_in_ga(s(s(s(0))), 0) → quotI_out_ga(s(s(s(0))), 0)
quotI_in_ga(s(s(s(s(0)))), 0) → quotI_out_ga(s(s(s(s(0)))), 0)
quotI_in_ga(s(s(s(s(s(0))))), 0) → quotI_out_ga(s(s(s(s(s(0))))), 0)
quotI_in_ga(s(s(s(s(s(s(0)))))), 0) → quotI_out_ga(s(s(s(s(s(s(0)))))), 0)
quotI_in_ga(s(s(s(s(s(s(s(T1120))))))), s(T1122)) → U8_ga(T1120, T1122, quotI_in_ga(T1120, T1122))
U8_ga(T1120, T1122, quotI_out_ga(T1120, T1122)) → quotI_out_ga(s(s(s(s(s(s(s(T1120))))))), s(T1122))
U17_gga(T983, T985, quotI_out_ga(T983, T985)) → quotB_out_gga(s(s(s(s(s(s(s(T983))))))), s(s(s(s(s(s(s(0))))))), s(T985))
quotB_in_gga(s(s(s(s(s(s(s(s(T1176)))))))), s(s(s(s(s(s(s(s(T1181)))))))), T1149) → U18_gga(T1176, T1181, T1149, quotJ_in_ggga(T1176, T1181, s(s(s(s(s(s(s(T1181))))))), T1149))
quotJ_in_ggga(0, s(T1197), T1198, 0) → quotJ_out_ggga(0, s(T1197), T1198, 0)
quotJ_in_ggga(T1211, 0, T1212, s(T1214)) → U9_ggga(T1211, T1212, T1214, quotB_in_gga(T1211, s(T1212), T1214))
U9_ggga(T1211, T1212, T1214, quotB_out_gga(T1211, s(T1212), T1214)) → quotJ_out_ggga(T1211, 0, T1212, s(T1214))
quotJ_in_ggga(s(T1261), s(T1266), T1230, T1232) → U10_ggga(T1261, T1266, T1230, T1232, quotJ_in_ggga(T1261, T1266, T1230, T1232))
U10_ggga(T1261, T1266, T1230, T1232, quotJ_out_ggga(T1261, T1266, T1230, T1232)) → quotJ_out_ggga(s(T1261), s(T1266), T1230, T1232)
U18_gga(T1176, T1181, T1149, quotJ_out_ggga(T1176, T1181, s(s(s(s(s(s(s(T1181))))))), T1149)) → quotB_out_gga(s(s(s(s(s(s(s(s(T1176)))))))), s(s(s(s(s(s(s(s(T1181)))))))), T1149)
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)
U11_gga(x1, x2, x3)  =  U11_gga(x1, x3)
quotC_in_ga(x1, x2)  =  quotC_in_ga(x1)
quotC_out_ga(x1, x2)  =  quotC_out_ga(x1, x2)
U2_ga(x1, x2, x3)  =  U2_ga(x1, x3)
U12_gga(x1, x2, x3)  =  U12_gga(x1, x3)
quotD_in_ga(x1, x2)  =  quotD_in_ga(x1)
quotD_out_ga(x1, x2)  =  quotD_out_ga(x1, x2)
U3_ga(x1, x2, x3)  =  U3_ga(x1, x3)
U13_gga(x1, x2, x3)  =  U13_gga(x1, x3)
quotE_in_ga(x1, x2)  =  quotE_in_ga(x1)
quotE_out_ga(x1, x2)  =  quotE_out_ga(x1, x2)
U4_ga(x1, x2, x3)  =  U4_ga(x1, x3)
U14_gga(x1, x2, x3)  =  U14_gga(x1, x3)
quotF_in_ga(x1, x2)  =  quotF_in_ga(x1)
quotF_out_ga(x1, x2)  =  quotF_out_ga(x1, x2)
U5_ga(x1, x2, x3)  =  U5_ga(x1, x3)
U15_gga(x1, x2, x3)  =  U15_gga(x1, x3)
quotG_in_ga(x1, x2)  =  quotG_in_ga(x1)
quotG_out_ga(x1, x2)  =  quotG_out_ga(x1, x2)
U6_ga(x1, x2, x3)  =  U6_ga(x1, x3)
U16_gga(x1, x2, x3)  =  U16_gga(x1, x3)
quotH_in_ga(x1, x2)  =  quotH_in_ga(x1)
quotH_out_ga(x1, x2)  =  quotH_out_ga(x1, x2)
U7_ga(x1, x2, x3)  =  U7_ga(x1, x3)
U17_gga(x1, x2, x3)  =  U17_gga(x1, x3)
quotI_in_ga(x1, x2)  =  quotI_in_ga(x1)
quotI_out_ga(x1, x2)  =  quotI_out_ga(x1, x2)
U8_ga(x1, x2, x3)  =  U8_ga(x1, x3)
U18_gga(x1, x2, x3, x4)  =  U18_gga(x1, x2, x4)
quotJ_in_ggga(x1, x2, x3, x4)  =  quotJ_in_ggga(x1, x2, x3)
quotJ_out_ggga(x1, x2, x3, x4)  =  quotJ_out_ggga(x1, x2, x3, x4)
U9_ggga(x1, x2, x3, x4)  =  U9_ggga(x1, x2, x4)
U10_ggga(x1, x2, x3, x4, x5)  =  U10_ggga(x1, x2, x3, x5)
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

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

QUOTI_IN_GA(s(s(s(s(s(s(s(T1120))))))), s(T1122)) → QUOTI_IN_GA(T1120, T1122)

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

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

QUOTI_IN_GA(s(s(s(s(s(s(s(T1120)))))))) → QUOTI_IN_GA(T1120)

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:

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

(13) YES

(14) Obligation:

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

QUOTH_IN_GA(s(s(s(s(s(s(T906)))))), s(T908)) → QUOTH_IN_GA(T906, T908)

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(T68)), 0) → quotB_out_gga(s(0), s(s(T68)), 0)
quotB_in_gga(s(T77), s(0), s(T79)) → U11_gga(T77, T79, quotC_in_ga(T77, T79))
quotC_in_ga(0, 0) → quotC_out_ga(0, 0)
quotC_in_ga(s(T106), s(T108)) → U2_ga(T106, T108, quotC_in_ga(T106, T108))
U2_ga(T106, T108, quotC_out_ga(T106, T108)) → quotC_out_ga(s(T106), s(T108))
U11_gga(T77, T79, quotC_out_ga(T77, T79)) → quotB_out_gga(s(T77), s(0), s(T79))
quotB_in_gga(s(s(0)), s(s(s(T174))), 0) → quotB_out_gga(s(s(0)), s(s(s(T174))), 0)
quotB_in_gga(s(s(T183)), s(s(0)), s(T185)) → U12_gga(T183, T185, quotD_in_ga(T183, T185))
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(T230)), s(T232)) → U3_ga(T230, T232, quotD_in_ga(T230, T232))
U3_ga(T230, T232, quotD_out_ga(T230, T232)) → quotD_out_ga(s(s(T230)), s(T232))
U12_gga(T183, T185, quotD_out_ga(T183, T185)) → quotB_out_gga(s(s(T183)), s(s(0)), s(T185))
quotB_in_gga(s(s(s(0))), s(s(s(s(T298)))), 0) → quotB_out_gga(s(s(s(0))), s(s(s(s(T298)))), 0)
quotB_in_gga(s(s(s(T307))), s(s(s(0))), s(T309)) → U13_gga(T307, T309, quotE_in_ga(T307, T309))
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(T372))), s(T374)) → U4_ga(T372, T374, quotE_in_ga(T372, T374))
U4_ga(T372, T374, quotE_out_ga(T372, T374)) → quotE_out_ga(s(s(s(T372))), s(T374))
U13_gga(T307, T309, quotE_out_ga(T307, T309)) → quotB_out_gga(s(s(s(T307))), s(s(s(0))), s(T309))
quotB_in_gga(s(s(s(s(0)))), s(s(s(s(s(T440))))), 0) → quotB_out_gga(s(s(s(s(0)))), s(s(s(s(s(T440))))), 0)
quotB_in_gga(s(s(s(s(T449)))), s(s(s(s(0)))), s(T451)) → U14_gga(T449, T451, quotF_in_ga(T449, T451))
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(T532)))), s(T534)) → U5_ga(T532, T534, quotF_in_ga(T532, T534))
U5_ga(T532, T534, quotF_out_ga(T532, T534)) → quotF_out_ga(s(s(s(s(T532)))), s(T534))
U14_gga(T449, T451, quotF_out_ga(T449, T451)) → quotB_out_gga(s(s(s(s(T449)))), s(s(s(s(0)))), s(T451))
quotB_in_gga(s(s(s(s(s(0))))), s(s(s(s(s(s(T600)))))), 0) → quotB_out_gga(s(s(s(s(s(0))))), s(s(s(s(s(s(T600)))))), 0)
quotB_in_gga(s(s(s(s(s(T609))))), s(s(s(s(s(0))))), s(T611)) → U15_gga(T609, T611, quotG_in_ga(T609, T611))
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(0)))), 0) → quotG_out_ga(s(s(s(s(0)))), 0)
quotG_in_ga(s(s(s(s(s(T710))))), s(T712)) → U6_ga(T710, T712, quotG_in_ga(T710, T712))
U6_ga(T710, T712, quotG_out_ga(T710, T712)) → quotG_out_ga(s(s(s(s(s(T710))))), s(T712))
U15_gga(T609, T611, quotG_out_ga(T609, T611)) → quotB_out_gga(s(s(s(s(s(T609))))), s(s(s(s(s(0))))), s(T611))
quotB_in_gga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T778))))))), 0) → quotB_out_gga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T778))))))), 0)
quotB_in_gga(s(s(s(s(s(s(T787)))))), s(s(s(s(s(s(0)))))), s(T789)) → U16_gga(T787, T789, quotH_in_ga(T787, T789))
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(0))), 0) → quotH_out_ga(s(s(s(0))), 0)
quotH_in_ga(s(s(s(s(0)))), 0) → quotH_out_ga(s(s(s(s(0)))), 0)
quotH_in_ga(s(s(s(s(s(0))))), 0) → quotH_out_ga(s(s(s(s(s(0))))), 0)
quotH_in_ga(s(s(s(s(s(s(T906)))))), s(T908)) → U7_ga(T906, T908, quotH_in_ga(T906, T908))
U7_ga(T906, T908, quotH_out_ga(T906, T908)) → quotH_out_ga(s(s(s(s(s(s(T906)))))), s(T908))
U16_gga(T787, T789, quotH_out_ga(T787, T789)) → quotB_out_gga(s(s(s(s(s(s(T787)))))), s(s(s(s(s(s(0)))))), s(T789))
quotB_in_gga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(T974)))))))), 0) → quotB_out_gga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(T974)))))))), 0)
quotB_in_gga(s(s(s(s(s(s(s(T983))))))), s(s(s(s(s(s(s(0))))))), s(T985)) → U17_gga(T983, T985, quotI_in_ga(T983, T985))
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(0)), 0) → quotI_out_ga(s(s(0)), 0)
quotI_in_ga(s(s(s(0))), 0) → quotI_out_ga(s(s(s(0))), 0)
quotI_in_ga(s(s(s(s(0)))), 0) → quotI_out_ga(s(s(s(s(0)))), 0)
quotI_in_ga(s(s(s(s(s(0))))), 0) → quotI_out_ga(s(s(s(s(s(0))))), 0)
quotI_in_ga(s(s(s(s(s(s(0)))))), 0) → quotI_out_ga(s(s(s(s(s(s(0)))))), 0)
quotI_in_ga(s(s(s(s(s(s(s(T1120))))))), s(T1122)) → U8_ga(T1120, T1122, quotI_in_ga(T1120, T1122))
U8_ga(T1120, T1122, quotI_out_ga(T1120, T1122)) → quotI_out_ga(s(s(s(s(s(s(s(T1120))))))), s(T1122))
U17_gga(T983, T985, quotI_out_ga(T983, T985)) → quotB_out_gga(s(s(s(s(s(s(s(T983))))))), s(s(s(s(s(s(s(0))))))), s(T985))
quotB_in_gga(s(s(s(s(s(s(s(s(T1176)))))))), s(s(s(s(s(s(s(s(T1181)))))))), T1149) → U18_gga(T1176, T1181, T1149, quotJ_in_ggga(T1176, T1181, s(s(s(s(s(s(s(T1181))))))), T1149))
quotJ_in_ggga(0, s(T1197), T1198, 0) → quotJ_out_ggga(0, s(T1197), T1198, 0)
quotJ_in_ggga(T1211, 0, T1212, s(T1214)) → U9_ggga(T1211, T1212, T1214, quotB_in_gga(T1211, s(T1212), T1214))
U9_ggga(T1211, T1212, T1214, quotB_out_gga(T1211, s(T1212), T1214)) → quotJ_out_ggga(T1211, 0, T1212, s(T1214))
quotJ_in_ggga(s(T1261), s(T1266), T1230, T1232) → U10_ggga(T1261, T1266, T1230, T1232, quotJ_in_ggga(T1261, T1266, T1230, T1232))
U10_ggga(T1261, T1266, T1230, T1232, quotJ_out_ggga(T1261, T1266, T1230, T1232)) → quotJ_out_ggga(s(T1261), s(T1266), T1230, T1232)
U18_gga(T1176, T1181, T1149, quotJ_out_ggga(T1176, T1181, s(s(s(s(s(s(s(T1181))))))), T1149)) → quotB_out_gga(s(s(s(s(s(s(s(s(T1176)))))))), s(s(s(s(s(s(s(s(T1181)))))))), T1149)
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)
U11_gga(x1, x2, x3)  =  U11_gga(x1, x3)
quotC_in_ga(x1, x2)  =  quotC_in_ga(x1)
quotC_out_ga(x1, x2)  =  quotC_out_ga(x1, x2)
U2_ga(x1, x2, x3)  =  U2_ga(x1, x3)
U12_gga(x1, x2, x3)  =  U12_gga(x1, x3)
quotD_in_ga(x1, x2)  =  quotD_in_ga(x1)
quotD_out_ga(x1, x2)  =  quotD_out_ga(x1, x2)
U3_ga(x1, x2, x3)  =  U3_ga(x1, x3)
U13_gga(x1, x2, x3)  =  U13_gga(x1, x3)
quotE_in_ga(x1, x2)  =  quotE_in_ga(x1)
quotE_out_ga(x1, x2)  =  quotE_out_ga(x1, x2)
U4_ga(x1, x2, x3)  =  U4_ga(x1, x3)
U14_gga(x1, x2, x3)  =  U14_gga(x1, x3)
quotF_in_ga(x1, x2)  =  quotF_in_ga(x1)
quotF_out_ga(x1, x2)  =  quotF_out_ga(x1, x2)
U5_ga(x1, x2, x3)  =  U5_ga(x1, x3)
U15_gga(x1, x2, x3)  =  U15_gga(x1, x3)
quotG_in_ga(x1, x2)  =  quotG_in_ga(x1)
quotG_out_ga(x1, x2)  =  quotG_out_ga(x1, x2)
U6_ga(x1, x2, x3)  =  U6_ga(x1, x3)
U16_gga(x1, x2, x3)  =  U16_gga(x1, x3)
quotH_in_ga(x1, x2)  =  quotH_in_ga(x1)
quotH_out_ga(x1, x2)  =  quotH_out_ga(x1, x2)
U7_ga(x1, x2, x3)  =  U7_ga(x1, x3)
U17_gga(x1, x2, x3)  =  U17_gga(x1, x3)
quotI_in_ga(x1, x2)  =  quotI_in_ga(x1)
quotI_out_ga(x1, x2)  =  quotI_out_ga(x1, x2)
U8_ga(x1, x2, x3)  =  U8_ga(x1, x3)
U18_gga(x1, x2, x3, x4)  =  U18_gga(x1, x2, x4)
quotJ_in_ggga(x1, x2, x3, x4)  =  quotJ_in_ggga(x1, x2, x3)
quotJ_out_ggga(x1, x2, x3, x4)  =  quotJ_out_ggga(x1, x2, x3, x4)
U9_ggga(x1, x2, x3, x4)  =  U9_ggga(x1, x2, x4)
U10_ggga(x1, x2, x3, x4, x5)  =  U10_ggga(x1, x2, x3, x5)
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

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

QUOTH_IN_GA(s(s(s(s(s(s(T906)))))), s(T908)) → QUOTH_IN_GA(T906, T908)

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

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

QUOTH_IN_GA(s(s(s(s(s(s(T906))))))) → QUOTH_IN_GA(T906)

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:

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

(20) YES

(21) Obligation:

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

QUOTG_IN_GA(s(s(s(s(s(T710))))), s(T712)) → QUOTG_IN_GA(T710, T712)

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(T68)), 0) → quotB_out_gga(s(0), s(s(T68)), 0)
quotB_in_gga(s(T77), s(0), s(T79)) → U11_gga(T77, T79, quotC_in_ga(T77, T79))
quotC_in_ga(0, 0) → quotC_out_ga(0, 0)
quotC_in_ga(s(T106), s(T108)) → U2_ga(T106, T108, quotC_in_ga(T106, T108))
U2_ga(T106, T108, quotC_out_ga(T106, T108)) → quotC_out_ga(s(T106), s(T108))
U11_gga(T77, T79, quotC_out_ga(T77, T79)) → quotB_out_gga(s(T77), s(0), s(T79))
quotB_in_gga(s(s(0)), s(s(s(T174))), 0) → quotB_out_gga(s(s(0)), s(s(s(T174))), 0)
quotB_in_gga(s(s(T183)), s(s(0)), s(T185)) → U12_gga(T183, T185, quotD_in_ga(T183, T185))
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(T230)), s(T232)) → U3_ga(T230, T232, quotD_in_ga(T230, T232))
U3_ga(T230, T232, quotD_out_ga(T230, T232)) → quotD_out_ga(s(s(T230)), s(T232))
U12_gga(T183, T185, quotD_out_ga(T183, T185)) → quotB_out_gga(s(s(T183)), s(s(0)), s(T185))
quotB_in_gga(s(s(s(0))), s(s(s(s(T298)))), 0) → quotB_out_gga(s(s(s(0))), s(s(s(s(T298)))), 0)
quotB_in_gga(s(s(s(T307))), s(s(s(0))), s(T309)) → U13_gga(T307, T309, quotE_in_ga(T307, T309))
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(T372))), s(T374)) → U4_ga(T372, T374, quotE_in_ga(T372, T374))
U4_ga(T372, T374, quotE_out_ga(T372, T374)) → quotE_out_ga(s(s(s(T372))), s(T374))
U13_gga(T307, T309, quotE_out_ga(T307, T309)) → quotB_out_gga(s(s(s(T307))), s(s(s(0))), s(T309))
quotB_in_gga(s(s(s(s(0)))), s(s(s(s(s(T440))))), 0) → quotB_out_gga(s(s(s(s(0)))), s(s(s(s(s(T440))))), 0)
quotB_in_gga(s(s(s(s(T449)))), s(s(s(s(0)))), s(T451)) → U14_gga(T449, T451, quotF_in_ga(T449, T451))
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(T532)))), s(T534)) → U5_ga(T532, T534, quotF_in_ga(T532, T534))
U5_ga(T532, T534, quotF_out_ga(T532, T534)) → quotF_out_ga(s(s(s(s(T532)))), s(T534))
U14_gga(T449, T451, quotF_out_ga(T449, T451)) → quotB_out_gga(s(s(s(s(T449)))), s(s(s(s(0)))), s(T451))
quotB_in_gga(s(s(s(s(s(0))))), s(s(s(s(s(s(T600)))))), 0) → quotB_out_gga(s(s(s(s(s(0))))), s(s(s(s(s(s(T600)))))), 0)
quotB_in_gga(s(s(s(s(s(T609))))), s(s(s(s(s(0))))), s(T611)) → U15_gga(T609, T611, quotG_in_ga(T609, T611))
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(0)))), 0) → quotG_out_ga(s(s(s(s(0)))), 0)
quotG_in_ga(s(s(s(s(s(T710))))), s(T712)) → U6_ga(T710, T712, quotG_in_ga(T710, T712))
U6_ga(T710, T712, quotG_out_ga(T710, T712)) → quotG_out_ga(s(s(s(s(s(T710))))), s(T712))
U15_gga(T609, T611, quotG_out_ga(T609, T611)) → quotB_out_gga(s(s(s(s(s(T609))))), s(s(s(s(s(0))))), s(T611))
quotB_in_gga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T778))))))), 0) → quotB_out_gga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T778))))))), 0)
quotB_in_gga(s(s(s(s(s(s(T787)))))), s(s(s(s(s(s(0)))))), s(T789)) → U16_gga(T787, T789, quotH_in_ga(T787, T789))
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(0))), 0) → quotH_out_ga(s(s(s(0))), 0)
quotH_in_ga(s(s(s(s(0)))), 0) → quotH_out_ga(s(s(s(s(0)))), 0)
quotH_in_ga(s(s(s(s(s(0))))), 0) → quotH_out_ga(s(s(s(s(s(0))))), 0)
quotH_in_ga(s(s(s(s(s(s(T906)))))), s(T908)) → U7_ga(T906, T908, quotH_in_ga(T906, T908))
U7_ga(T906, T908, quotH_out_ga(T906, T908)) → quotH_out_ga(s(s(s(s(s(s(T906)))))), s(T908))
U16_gga(T787, T789, quotH_out_ga(T787, T789)) → quotB_out_gga(s(s(s(s(s(s(T787)))))), s(s(s(s(s(s(0)))))), s(T789))
quotB_in_gga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(T974)))))))), 0) → quotB_out_gga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(T974)))))))), 0)
quotB_in_gga(s(s(s(s(s(s(s(T983))))))), s(s(s(s(s(s(s(0))))))), s(T985)) → U17_gga(T983, T985, quotI_in_ga(T983, T985))
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(0)), 0) → quotI_out_ga(s(s(0)), 0)
quotI_in_ga(s(s(s(0))), 0) → quotI_out_ga(s(s(s(0))), 0)
quotI_in_ga(s(s(s(s(0)))), 0) → quotI_out_ga(s(s(s(s(0)))), 0)
quotI_in_ga(s(s(s(s(s(0))))), 0) → quotI_out_ga(s(s(s(s(s(0))))), 0)
quotI_in_ga(s(s(s(s(s(s(0)))))), 0) → quotI_out_ga(s(s(s(s(s(s(0)))))), 0)
quotI_in_ga(s(s(s(s(s(s(s(T1120))))))), s(T1122)) → U8_ga(T1120, T1122, quotI_in_ga(T1120, T1122))
U8_ga(T1120, T1122, quotI_out_ga(T1120, T1122)) → quotI_out_ga(s(s(s(s(s(s(s(T1120))))))), s(T1122))
U17_gga(T983, T985, quotI_out_ga(T983, T985)) → quotB_out_gga(s(s(s(s(s(s(s(T983))))))), s(s(s(s(s(s(s(0))))))), s(T985))
quotB_in_gga(s(s(s(s(s(s(s(s(T1176)))))))), s(s(s(s(s(s(s(s(T1181)))))))), T1149) → U18_gga(T1176, T1181, T1149, quotJ_in_ggga(T1176, T1181, s(s(s(s(s(s(s(T1181))))))), T1149))
quotJ_in_ggga(0, s(T1197), T1198, 0) → quotJ_out_ggga(0, s(T1197), T1198, 0)
quotJ_in_ggga(T1211, 0, T1212, s(T1214)) → U9_ggga(T1211, T1212, T1214, quotB_in_gga(T1211, s(T1212), T1214))
U9_ggga(T1211, T1212, T1214, quotB_out_gga(T1211, s(T1212), T1214)) → quotJ_out_ggga(T1211, 0, T1212, s(T1214))
quotJ_in_ggga(s(T1261), s(T1266), T1230, T1232) → U10_ggga(T1261, T1266, T1230, T1232, quotJ_in_ggga(T1261, T1266, T1230, T1232))
U10_ggga(T1261, T1266, T1230, T1232, quotJ_out_ggga(T1261, T1266, T1230, T1232)) → quotJ_out_ggga(s(T1261), s(T1266), T1230, T1232)
U18_gga(T1176, T1181, T1149, quotJ_out_ggga(T1176, T1181, s(s(s(s(s(s(s(T1181))))))), T1149)) → quotB_out_gga(s(s(s(s(s(s(s(s(T1176)))))))), s(s(s(s(s(s(s(s(T1181)))))))), T1149)
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)
U11_gga(x1, x2, x3)  =  U11_gga(x1, x3)
quotC_in_ga(x1, x2)  =  quotC_in_ga(x1)
quotC_out_ga(x1, x2)  =  quotC_out_ga(x1, x2)
U2_ga(x1, x2, x3)  =  U2_ga(x1, x3)
U12_gga(x1, x2, x3)  =  U12_gga(x1, x3)
quotD_in_ga(x1, x2)  =  quotD_in_ga(x1)
quotD_out_ga(x1, x2)  =  quotD_out_ga(x1, x2)
U3_ga(x1, x2, x3)  =  U3_ga(x1, x3)
U13_gga(x1, x2, x3)  =  U13_gga(x1, x3)
quotE_in_ga(x1, x2)  =  quotE_in_ga(x1)
quotE_out_ga(x1, x2)  =  quotE_out_ga(x1, x2)
U4_ga(x1, x2, x3)  =  U4_ga(x1, x3)
U14_gga(x1, x2, x3)  =  U14_gga(x1, x3)
quotF_in_ga(x1, x2)  =  quotF_in_ga(x1)
quotF_out_ga(x1, x2)  =  quotF_out_ga(x1, x2)
U5_ga(x1, x2, x3)  =  U5_ga(x1, x3)
U15_gga(x1, x2, x3)  =  U15_gga(x1, x3)
quotG_in_ga(x1, x2)  =  quotG_in_ga(x1)
quotG_out_ga(x1, x2)  =  quotG_out_ga(x1, x2)
U6_ga(x1, x2, x3)  =  U6_ga(x1, x3)
U16_gga(x1, x2, x3)  =  U16_gga(x1, x3)
quotH_in_ga(x1, x2)  =  quotH_in_ga(x1)
quotH_out_ga(x1, x2)  =  quotH_out_ga(x1, x2)
U7_ga(x1, x2, x3)  =  U7_ga(x1, x3)
U17_gga(x1, x2, x3)  =  U17_gga(x1, x3)
quotI_in_ga(x1, x2)  =  quotI_in_ga(x1)
quotI_out_ga(x1, x2)  =  quotI_out_ga(x1, x2)
U8_ga(x1, x2, x3)  =  U8_ga(x1, x3)
U18_gga(x1, x2, x3, x4)  =  U18_gga(x1, x2, x4)
quotJ_in_ggga(x1, x2, x3, x4)  =  quotJ_in_ggga(x1, x2, x3)
quotJ_out_ggga(x1, x2, x3, x4)  =  quotJ_out_ggga(x1, x2, x3, x4)
U9_ggga(x1, x2, x3, x4)  =  U9_ggga(x1, x2, x4)
U10_ggga(x1, x2, x3, x4, x5)  =  U10_ggga(x1, x2, x3, x5)
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

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

QUOTG_IN_GA(s(s(s(s(s(T710))))), s(T712)) → QUOTG_IN_GA(T710, T712)

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

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

QUOTG_IN_GA(s(s(s(s(s(T710)))))) → QUOTG_IN_GA(T710)

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:

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

(27) YES

(28) Obligation:

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

QUOTF_IN_GA(s(s(s(s(T532)))), s(T534)) → QUOTF_IN_GA(T532, T534)

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(T68)), 0) → quotB_out_gga(s(0), s(s(T68)), 0)
quotB_in_gga(s(T77), s(0), s(T79)) → U11_gga(T77, T79, quotC_in_ga(T77, T79))
quotC_in_ga(0, 0) → quotC_out_ga(0, 0)
quotC_in_ga(s(T106), s(T108)) → U2_ga(T106, T108, quotC_in_ga(T106, T108))
U2_ga(T106, T108, quotC_out_ga(T106, T108)) → quotC_out_ga(s(T106), s(T108))
U11_gga(T77, T79, quotC_out_ga(T77, T79)) → quotB_out_gga(s(T77), s(0), s(T79))
quotB_in_gga(s(s(0)), s(s(s(T174))), 0) → quotB_out_gga(s(s(0)), s(s(s(T174))), 0)
quotB_in_gga(s(s(T183)), s(s(0)), s(T185)) → U12_gga(T183, T185, quotD_in_ga(T183, T185))
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(T230)), s(T232)) → U3_ga(T230, T232, quotD_in_ga(T230, T232))
U3_ga(T230, T232, quotD_out_ga(T230, T232)) → quotD_out_ga(s(s(T230)), s(T232))
U12_gga(T183, T185, quotD_out_ga(T183, T185)) → quotB_out_gga(s(s(T183)), s(s(0)), s(T185))
quotB_in_gga(s(s(s(0))), s(s(s(s(T298)))), 0) → quotB_out_gga(s(s(s(0))), s(s(s(s(T298)))), 0)
quotB_in_gga(s(s(s(T307))), s(s(s(0))), s(T309)) → U13_gga(T307, T309, quotE_in_ga(T307, T309))
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(T372))), s(T374)) → U4_ga(T372, T374, quotE_in_ga(T372, T374))
U4_ga(T372, T374, quotE_out_ga(T372, T374)) → quotE_out_ga(s(s(s(T372))), s(T374))
U13_gga(T307, T309, quotE_out_ga(T307, T309)) → quotB_out_gga(s(s(s(T307))), s(s(s(0))), s(T309))
quotB_in_gga(s(s(s(s(0)))), s(s(s(s(s(T440))))), 0) → quotB_out_gga(s(s(s(s(0)))), s(s(s(s(s(T440))))), 0)
quotB_in_gga(s(s(s(s(T449)))), s(s(s(s(0)))), s(T451)) → U14_gga(T449, T451, quotF_in_ga(T449, T451))
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(T532)))), s(T534)) → U5_ga(T532, T534, quotF_in_ga(T532, T534))
U5_ga(T532, T534, quotF_out_ga(T532, T534)) → quotF_out_ga(s(s(s(s(T532)))), s(T534))
U14_gga(T449, T451, quotF_out_ga(T449, T451)) → quotB_out_gga(s(s(s(s(T449)))), s(s(s(s(0)))), s(T451))
quotB_in_gga(s(s(s(s(s(0))))), s(s(s(s(s(s(T600)))))), 0) → quotB_out_gga(s(s(s(s(s(0))))), s(s(s(s(s(s(T600)))))), 0)
quotB_in_gga(s(s(s(s(s(T609))))), s(s(s(s(s(0))))), s(T611)) → U15_gga(T609, T611, quotG_in_ga(T609, T611))
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(0)))), 0) → quotG_out_ga(s(s(s(s(0)))), 0)
quotG_in_ga(s(s(s(s(s(T710))))), s(T712)) → U6_ga(T710, T712, quotG_in_ga(T710, T712))
U6_ga(T710, T712, quotG_out_ga(T710, T712)) → quotG_out_ga(s(s(s(s(s(T710))))), s(T712))
U15_gga(T609, T611, quotG_out_ga(T609, T611)) → quotB_out_gga(s(s(s(s(s(T609))))), s(s(s(s(s(0))))), s(T611))
quotB_in_gga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T778))))))), 0) → quotB_out_gga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T778))))))), 0)
quotB_in_gga(s(s(s(s(s(s(T787)))))), s(s(s(s(s(s(0)))))), s(T789)) → U16_gga(T787, T789, quotH_in_ga(T787, T789))
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(0))), 0) → quotH_out_ga(s(s(s(0))), 0)
quotH_in_ga(s(s(s(s(0)))), 0) → quotH_out_ga(s(s(s(s(0)))), 0)
quotH_in_ga(s(s(s(s(s(0))))), 0) → quotH_out_ga(s(s(s(s(s(0))))), 0)
quotH_in_ga(s(s(s(s(s(s(T906)))))), s(T908)) → U7_ga(T906, T908, quotH_in_ga(T906, T908))
U7_ga(T906, T908, quotH_out_ga(T906, T908)) → quotH_out_ga(s(s(s(s(s(s(T906)))))), s(T908))
U16_gga(T787, T789, quotH_out_ga(T787, T789)) → quotB_out_gga(s(s(s(s(s(s(T787)))))), s(s(s(s(s(s(0)))))), s(T789))
quotB_in_gga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(T974)))))))), 0) → quotB_out_gga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(T974)))))))), 0)
quotB_in_gga(s(s(s(s(s(s(s(T983))))))), s(s(s(s(s(s(s(0))))))), s(T985)) → U17_gga(T983, T985, quotI_in_ga(T983, T985))
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(0)), 0) → quotI_out_ga(s(s(0)), 0)
quotI_in_ga(s(s(s(0))), 0) → quotI_out_ga(s(s(s(0))), 0)
quotI_in_ga(s(s(s(s(0)))), 0) → quotI_out_ga(s(s(s(s(0)))), 0)
quotI_in_ga(s(s(s(s(s(0))))), 0) → quotI_out_ga(s(s(s(s(s(0))))), 0)
quotI_in_ga(s(s(s(s(s(s(0)))))), 0) → quotI_out_ga(s(s(s(s(s(s(0)))))), 0)
quotI_in_ga(s(s(s(s(s(s(s(T1120))))))), s(T1122)) → U8_ga(T1120, T1122, quotI_in_ga(T1120, T1122))
U8_ga(T1120, T1122, quotI_out_ga(T1120, T1122)) → quotI_out_ga(s(s(s(s(s(s(s(T1120))))))), s(T1122))
U17_gga(T983, T985, quotI_out_ga(T983, T985)) → quotB_out_gga(s(s(s(s(s(s(s(T983))))))), s(s(s(s(s(s(s(0))))))), s(T985))
quotB_in_gga(s(s(s(s(s(s(s(s(T1176)))))))), s(s(s(s(s(s(s(s(T1181)))))))), T1149) → U18_gga(T1176, T1181, T1149, quotJ_in_ggga(T1176, T1181, s(s(s(s(s(s(s(T1181))))))), T1149))
quotJ_in_ggga(0, s(T1197), T1198, 0) → quotJ_out_ggga(0, s(T1197), T1198, 0)
quotJ_in_ggga(T1211, 0, T1212, s(T1214)) → U9_ggga(T1211, T1212, T1214, quotB_in_gga(T1211, s(T1212), T1214))
U9_ggga(T1211, T1212, T1214, quotB_out_gga(T1211, s(T1212), T1214)) → quotJ_out_ggga(T1211, 0, T1212, s(T1214))
quotJ_in_ggga(s(T1261), s(T1266), T1230, T1232) → U10_ggga(T1261, T1266, T1230, T1232, quotJ_in_ggga(T1261, T1266, T1230, T1232))
U10_ggga(T1261, T1266, T1230, T1232, quotJ_out_ggga(T1261, T1266, T1230, T1232)) → quotJ_out_ggga(s(T1261), s(T1266), T1230, T1232)
U18_gga(T1176, T1181, T1149, quotJ_out_ggga(T1176, T1181, s(s(s(s(s(s(s(T1181))))))), T1149)) → quotB_out_gga(s(s(s(s(s(s(s(s(T1176)))))))), s(s(s(s(s(s(s(s(T1181)))))))), T1149)
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)
U11_gga(x1, x2, x3)  =  U11_gga(x1, x3)
quotC_in_ga(x1, x2)  =  quotC_in_ga(x1)
quotC_out_ga(x1, x2)  =  quotC_out_ga(x1, x2)
U2_ga(x1, x2, x3)  =  U2_ga(x1, x3)
U12_gga(x1, x2, x3)  =  U12_gga(x1, x3)
quotD_in_ga(x1, x2)  =  quotD_in_ga(x1)
quotD_out_ga(x1, x2)  =  quotD_out_ga(x1, x2)
U3_ga(x1, x2, x3)  =  U3_ga(x1, x3)
U13_gga(x1, x2, x3)  =  U13_gga(x1, x3)
quotE_in_ga(x1, x2)  =  quotE_in_ga(x1)
quotE_out_ga(x1, x2)  =  quotE_out_ga(x1, x2)
U4_ga(x1, x2, x3)  =  U4_ga(x1, x3)
U14_gga(x1, x2, x3)  =  U14_gga(x1, x3)
quotF_in_ga(x1, x2)  =  quotF_in_ga(x1)
quotF_out_ga(x1, x2)  =  quotF_out_ga(x1, x2)
U5_ga(x1, x2, x3)  =  U5_ga(x1, x3)
U15_gga(x1, x2, x3)  =  U15_gga(x1, x3)
quotG_in_ga(x1, x2)  =  quotG_in_ga(x1)
quotG_out_ga(x1, x2)  =  quotG_out_ga(x1, x2)
U6_ga(x1, x2, x3)  =  U6_ga(x1, x3)
U16_gga(x1, x2, x3)  =  U16_gga(x1, x3)
quotH_in_ga(x1, x2)  =  quotH_in_ga(x1)
quotH_out_ga(x1, x2)  =  quotH_out_ga(x1, x2)
U7_ga(x1, x2, x3)  =  U7_ga(x1, x3)
U17_gga(x1, x2, x3)  =  U17_gga(x1, x3)
quotI_in_ga(x1, x2)  =  quotI_in_ga(x1)
quotI_out_ga(x1, x2)  =  quotI_out_ga(x1, x2)
U8_ga(x1, x2, x3)  =  U8_ga(x1, x3)
U18_gga(x1, x2, x3, x4)  =  U18_gga(x1, x2, x4)
quotJ_in_ggga(x1, x2, x3, x4)  =  quotJ_in_ggga(x1, x2, x3)
quotJ_out_ggga(x1, x2, x3, x4)  =  quotJ_out_ggga(x1, x2, x3, x4)
U9_ggga(x1, x2, x3, x4)  =  U9_ggga(x1, x2, x4)
U10_ggga(x1, x2, x3, x4, x5)  =  U10_ggga(x1, x2, x3, x5)
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

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

QUOTF_IN_GA(s(s(s(s(T532)))), s(T534)) → QUOTF_IN_GA(T532, T534)

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

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

QUOTF_IN_GA(s(s(s(s(T532))))) → QUOTF_IN_GA(T532)

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:

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

(34) YES

(35) Obligation:

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

QUOTE_IN_GA(s(s(s(T372))), s(T374)) → QUOTE_IN_GA(T372, T374)

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(T68)), 0) → quotB_out_gga(s(0), s(s(T68)), 0)
quotB_in_gga(s(T77), s(0), s(T79)) → U11_gga(T77, T79, quotC_in_ga(T77, T79))
quotC_in_ga(0, 0) → quotC_out_ga(0, 0)
quotC_in_ga(s(T106), s(T108)) → U2_ga(T106, T108, quotC_in_ga(T106, T108))
U2_ga(T106, T108, quotC_out_ga(T106, T108)) → quotC_out_ga(s(T106), s(T108))
U11_gga(T77, T79, quotC_out_ga(T77, T79)) → quotB_out_gga(s(T77), s(0), s(T79))
quotB_in_gga(s(s(0)), s(s(s(T174))), 0) → quotB_out_gga(s(s(0)), s(s(s(T174))), 0)
quotB_in_gga(s(s(T183)), s(s(0)), s(T185)) → U12_gga(T183, T185, quotD_in_ga(T183, T185))
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(T230)), s(T232)) → U3_ga(T230, T232, quotD_in_ga(T230, T232))
U3_ga(T230, T232, quotD_out_ga(T230, T232)) → quotD_out_ga(s(s(T230)), s(T232))
U12_gga(T183, T185, quotD_out_ga(T183, T185)) → quotB_out_gga(s(s(T183)), s(s(0)), s(T185))
quotB_in_gga(s(s(s(0))), s(s(s(s(T298)))), 0) → quotB_out_gga(s(s(s(0))), s(s(s(s(T298)))), 0)
quotB_in_gga(s(s(s(T307))), s(s(s(0))), s(T309)) → U13_gga(T307, T309, quotE_in_ga(T307, T309))
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(T372))), s(T374)) → U4_ga(T372, T374, quotE_in_ga(T372, T374))
U4_ga(T372, T374, quotE_out_ga(T372, T374)) → quotE_out_ga(s(s(s(T372))), s(T374))
U13_gga(T307, T309, quotE_out_ga(T307, T309)) → quotB_out_gga(s(s(s(T307))), s(s(s(0))), s(T309))
quotB_in_gga(s(s(s(s(0)))), s(s(s(s(s(T440))))), 0) → quotB_out_gga(s(s(s(s(0)))), s(s(s(s(s(T440))))), 0)
quotB_in_gga(s(s(s(s(T449)))), s(s(s(s(0)))), s(T451)) → U14_gga(T449, T451, quotF_in_ga(T449, T451))
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(T532)))), s(T534)) → U5_ga(T532, T534, quotF_in_ga(T532, T534))
U5_ga(T532, T534, quotF_out_ga(T532, T534)) → quotF_out_ga(s(s(s(s(T532)))), s(T534))
U14_gga(T449, T451, quotF_out_ga(T449, T451)) → quotB_out_gga(s(s(s(s(T449)))), s(s(s(s(0)))), s(T451))
quotB_in_gga(s(s(s(s(s(0))))), s(s(s(s(s(s(T600)))))), 0) → quotB_out_gga(s(s(s(s(s(0))))), s(s(s(s(s(s(T600)))))), 0)
quotB_in_gga(s(s(s(s(s(T609))))), s(s(s(s(s(0))))), s(T611)) → U15_gga(T609, T611, quotG_in_ga(T609, T611))
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(0)))), 0) → quotG_out_ga(s(s(s(s(0)))), 0)
quotG_in_ga(s(s(s(s(s(T710))))), s(T712)) → U6_ga(T710, T712, quotG_in_ga(T710, T712))
U6_ga(T710, T712, quotG_out_ga(T710, T712)) → quotG_out_ga(s(s(s(s(s(T710))))), s(T712))
U15_gga(T609, T611, quotG_out_ga(T609, T611)) → quotB_out_gga(s(s(s(s(s(T609))))), s(s(s(s(s(0))))), s(T611))
quotB_in_gga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T778))))))), 0) → quotB_out_gga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T778))))))), 0)
quotB_in_gga(s(s(s(s(s(s(T787)))))), s(s(s(s(s(s(0)))))), s(T789)) → U16_gga(T787, T789, quotH_in_ga(T787, T789))
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(0))), 0) → quotH_out_ga(s(s(s(0))), 0)
quotH_in_ga(s(s(s(s(0)))), 0) → quotH_out_ga(s(s(s(s(0)))), 0)
quotH_in_ga(s(s(s(s(s(0))))), 0) → quotH_out_ga(s(s(s(s(s(0))))), 0)
quotH_in_ga(s(s(s(s(s(s(T906)))))), s(T908)) → U7_ga(T906, T908, quotH_in_ga(T906, T908))
U7_ga(T906, T908, quotH_out_ga(T906, T908)) → quotH_out_ga(s(s(s(s(s(s(T906)))))), s(T908))
U16_gga(T787, T789, quotH_out_ga(T787, T789)) → quotB_out_gga(s(s(s(s(s(s(T787)))))), s(s(s(s(s(s(0)))))), s(T789))
quotB_in_gga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(T974)))))))), 0) → quotB_out_gga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(T974)))))))), 0)
quotB_in_gga(s(s(s(s(s(s(s(T983))))))), s(s(s(s(s(s(s(0))))))), s(T985)) → U17_gga(T983, T985, quotI_in_ga(T983, T985))
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(0)), 0) → quotI_out_ga(s(s(0)), 0)
quotI_in_ga(s(s(s(0))), 0) → quotI_out_ga(s(s(s(0))), 0)
quotI_in_ga(s(s(s(s(0)))), 0) → quotI_out_ga(s(s(s(s(0)))), 0)
quotI_in_ga(s(s(s(s(s(0))))), 0) → quotI_out_ga(s(s(s(s(s(0))))), 0)
quotI_in_ga(s(s(s(s(s(s(0)))))), 0) → quotI_out_ga(s(s(s(s(s(s(0)))))), 0)
quotI_in_ga(s(s(s(s(s(s(s(T1120))))))), s(T1122)) → U8_ga(T1120, T1122, quotI_in_ga(T1120, T1122))
U8_ga(T1120, T1122, quotI_out_ga(T1120, T1122)) → quotI_out_ga(s(s(s(s(s(s(s(T1120))))))), s(T1122))
U17_gga(T983, T985, quotI_out_ga(T983, T985)) → quotB_out_gga(s(s(s(s(s(s(s(T983))))))), s(s(s(s(s(s(s(0))))))), s(T985))
quotB_in_gga(s(s(s(s(s(s(s(s(T1176)))))))), s(s(s(s(s(s(s(s(T1181)))))))), T1149) → U18_gga(T1176, T1181, T1149, quotJ_in_ggga(T1176, T1181, s(s(s(s(s(s(s(T1181))))))), T1149))
quotJ_in_ggga(0, s(T1197), T1198, 0) → quotJ_out_ggga(0, s(T1197), T1198, 0)
quotJ_in_ggga(T1211, 0, T1212, s(T1214)) → U9_ggga(T1211, T1212, T1214, quotB_in_gga(T1211, s(T1212), T1214))
U9_ggga(T1211, T1212, T1214, quotB_out_gga(T1211, s(T1212), T1214)) → quotJ_out_ggga(T1211, 0, T1212, s(T1214))
quotJ_in_ggga(s(T1261), s(T1266), T1230, T1232) → U10_ggga(T1261, T1266, T1230, T1232, quotJ_in_ggga(T1261, T1266, T1230, T1232))
U10_ggga(T1261, T1266, T1230, T1232, quotJ_out_ggga(T1261, T1266, T1230, T1232)) → quotJ_out_ggga(s(T1261), s(T1266), T1230, T1232)
U18_gga(T1176, T1181, T1149, quotJ_out_ggga(T1176, T1181, s(s(s(s(s(s(s(T1181))))))), T1149)) → quotB_out_gga(s(s(s(s(s(s(s(s(T1176)))))))), s(s(s(s(s(s(s(s(T1181)))))))), T1149)
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)
U11_gga(x1, x2, x3)  =  U11_gga(x1, x3)
quotC_in_ga(x1, x2)  =  quotC_in_ga(x1)
quotC_out_ga(x1, x2)  =  quotC_out_ga(x1, x2)
U2_ga(x1, x2, x3)  =  U2_ga(x1, x3)
U12_gga(x1, x2, x3)  =  U12_gga(x1, x3)
quotD_in_ga(x1, x2)  =  quotD_in_ga(x1)
quotD_out_ga(x1, x2)  =  quotD_out_ga(x1, x2)
U3_ga(x1, x2, x3)  =  U3_ga(x1, x3)
U13_gga(x1, x2, x3)  =  U13_gga(x1, x3)
quotE_in_ga(x1, x2)  =  quotE_in_ga(x1)
quotE_out_ga(x1, x2)  =  quotE_out_ga(x1, x2)
U4_ga(x1, x2, x3)  =  U4_ga(x1, x3)
U14_gga(x1, x2, x3)  =  U14_gga(x1, x3)
quotF_in_ga(x1, x2)  =  quotF_in_ga(x1)
quotF_out_ga(x1, x2)  =  quotF_out_ga(x1, x2)
U5_ga(x1, x2, x3)  =  U5_ga(x1, x3)
U15_gga(x1, x2, x3)  =  U15_gga(x1, x3)
quotG_in_ga(x1, x2)  =  quotG_in_ga(x1)
quotG_out_ga(x1, x2)  =  quotG_out_ga(x1, x2)
U6_ga(x1, x2, x3)  =  U6_ga(x1, x3)
U16_gga(x1, x2, x3)  =  U16_gga(x1, x3)
quotH_in_ga(x1, x2)  =  quotH_in_ga(x1)
quotH_out_ga(x1, x2)  =  quotH_out_ga(x1, x2)
U7_ga(x1, x2, x3)  =  U7_ga(x1, x3)
U17_gga(x1, x2, x3)  =  U17_gga(x1, x3)
quotI_in_ga(x1, x2)  =  quotI_in_ga(x1)
quotI_out_ga(x1, x2)  =  quotI_out_ga(x1, x2)
U8_ga(x1, x2, x3)  =  U8_ga(x1, x3)
U18_gga(x1, x2, x3, x4)  =  U18_gga(x1, x2, x4)
quotJ_in_ggga(x1, x2, x3, x4)  =  quotJ_in_ggga(x1, x2, x3)
quotJ_out_ggga(x1, x2, x3, x4)  =  quotJ_out_ggga(x1, x2, x3, x4)
U9_ggga(x1, x2, x3, x4)  =  U9_ggga(x1, x2, x4)
U10_ggga(x1, x2, x3, x4, x5)  =  U10_ggga(x1, x2, x3, x5)
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

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

QUOTE_IN_GA(s(s(s(T372))), s(T374)) → QUOTE_IN_GA(T372, T374)

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

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

QUOTE_IN_GA(s(s(s(T372)))) → QUOTE_IN_GA(T372)

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:

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

(41) YES

(42) Obligation:

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

QUOTD_IN_GA(s(s(T230)), s(T232)) → QUOTD_IN_GA(T230, T232)

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(T68)), 0) → quotB_out_gga(s(0), s(s(T68)), 0)
quotB_in_gga(s(T77), s(0), s(T79)) → U11_gga(T77, T79, quotC_in_ga(T77, T79))
quotC_in_ga(0, 0) → quotC_out_ga(0, 0)
quotC_in_ga(s(T106), s(T108)) → U2_ga(T106, T108, quotC_in_ga(T106, T108))
U2_ga(T106, T108, quotC_out_ga(T106, T108)) → quotC_out_ga(s(T106), s(T108))
U11_gga(T77, T79, quotC_out_ga(T77, T79)) → quotB_out_gga(s(T77), s(0), s(T79))
quotB_in_gga(s(s(0)), s(s(s(T174))), 0) → quotB_out_gga(s(s(0)), s(s(s(T174))), 0)
quotB_in_gga(s(s(T183)), s(s(0)), s(T185)) → U12_gga(T183, T185, quotD_in_ga(T183, T185))
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(T230)), s(T232)) → U3_ga(T230, T232, quotD_in_ga(T230, T232))
U3_ga(T230, T232, quotD_out_ga(T230, T232)) → quotD_out_ga(s(s(T230)), s(T232))
U12_gga(T183, T185, quotD_out_ga(T183, T185)) → quotB_out_gga(s(s(T183)), s(s(0)), s(T185))
quotB_in_gga(s(s(s(0))), s(s(s(s(T298)))), 0) → quotB_out_gga(s(s(s(0))), s(s(s(s(T298)))), 0)
quotB_in_gga(s(s(s(T307))), s(s(s(0))), s(T309)) → U13_gga(T307, T309, quotE_in_ga(T307, T309))
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(T372))), s(T374)) → U4_ga(T372, T374, quotE_in_ga(T372, T374))
U4_ga(T372, T374, quotE_out_ga(T372, T374)) → quotE_out_ga(s(s(s(T372))), s(T374))
U13_gga(T307, T309, quotE_out_ga(T307, T309)) → quotB_out_gga(s(s(s(T307))), s(s(s(0))), s(T309))
quotB_in_gga(s(s(s(s(0)))), s(s(s(s(s(T440))))), 0) → quotB_out_gga(s(s(s(s(0)))), s(s(s(s(s(T440))))), 0)
quotB_in_gga(s(s(s(s(T449)))), s(s(s(s(0)))), s(T451)) → U14_gga(T449, T451, quotF_in_ga(T449, T451))
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(T532)))), s(T534)) → U5_ga(T532, T534, quotF_in_ga(T532, T534))
U5_ga(T532, T534, quotF_out_ga(T532, T534)) → quotF_out_ga(s(s(s(s(T532)))), s(T534))
U14_gga(T449, T451, quotF_out_ga(T449, T451)) → quotB_out_gga(s(s(s(s(T449)))), s(s(s(s(0)))), s(T451))
quotB_in_gga(s(s(s(s(s(0))))), s(s(s(s(s(s(T600)))))), 0) → quotB_out_gga(s(s(s(s(s(0))))), s(s(s(s(s(s(T600)))))), 0)
quotB_in_gga(s(s(s(s(s(T609))))), s(s(s(s(s(0))))), s(T611)) → U15_gga(T609, T611, quotG_in_ga(T609, T611))
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(0)))), 0) → quotG_out_ga(s(s(s(s(0)))), 0)
quotG_in_ga(s(s(s(s(s(T710))))), s(T712)) → U6_ga(T710, T712, quotG_in_ga(T710, T712))
U6_ga(T710, T712, quotG_out_ga(T710, T712)) → quotG_out_ga(s(s(s(s(s(T710))))), s(T712))
U15_gga(T609, T611, quotG_out_ga(T609, T611)) → quotB_out_gga(s(s(s(s(s(T609))))), s(s(s(s(s(0))))), s(T611))
quotB_in_gga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T778))))))), 0) → quotB_out_gga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T778))))))), 0)
quotB_in_gga(s(s(s(s(s(s(T787)))))), s(s(s(s(s(s(0)))))), s(T789)) → U16_gga(T787, T789, quotH_in_ga(T787, T789))
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(0))), 0) → quotH_out_ga(s(s(s(0))), 0)
quotH_in_ga(s(s(s(s(0)))), 0) → quotH_out_ga(s(s(s(s(0)))), 0)
quotH_in_ga(s(s(s(s(s(0))))), 0) → quotH_out_ga(s(s(s(s(s(0))))), 0)
quotH_in_ga(s(s(s(s(s(s(T906)))))), s(T908)) → U7_ga(T906, T908, quotH_in_ga(T906, T908))
U7_ga(T906, T908, quotH_out_ga(T906, T908)) → quotH_out_ga(s(s(s(s(s(s(T906)))))), s(T908))
U16_gga(T787, T789, quotH_out_ga(T787, T789)) → quotB_out_gga(s(s(s(s(s(s(T787)))))), s(s(s(s(s(s(0)))))), s(T789))
quotB_in_gga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(T974)))))))), 0) → quotB_out_gga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(T974)))))))), 0)
quotB_in_gga(s(s(s(s(s(s(s(T983))))))), s(s(s(s(s(s(s(0))))))), s(T985)) → U17_gga(T983, T985, quotI_in_ga(T983, T985))
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(0)), 0) → quotI_out_ga(s(s(0)), 0)
quotI_in_ga(s(s(s(0))), 0) → quotI_out_ga(s(s(s(0))), 0)
quotI_in_ga(s(s(s(s(0)))), 0) → quotI_out_ga(s(s(s(s(0)))), 0)
quotI_in_ga(s(s(s(s(s(0))))), 0) → quotI_out_ga(s(s(s(s(s(0))))), 0)
quotI_in_ga(s(s(s(s(s(s(0)))))), 0) → quotI_out_ga(s(s(s(s(s(s(0)))))), 0)
quotI_in_ga(s(s(s(s(s(s(s(T1120))))))), s(T1122)) → U8_ga(T1120, T1122, quotI_in_ga(T1120, T1122))
U8_ga(T1120, T1122, quotI_out_ga(T1120, T1122)) → quotI_out_ga(s(s(s(s(s(s(s(T1120))))))), s(T1122))
U17_gga(T983, T985, quotI_out_ga(T983, T985)) → quotB_out_gga(s(s(s(s(s(s(s(T983))))))), s(s(s(s(s(s(s(0))))))), s(T985))
quotB_in_gga(s(s(s(s(s(s(s(s(T1176)))))))), s(s(s(s(s(s(s(s(T1181)))))))), T1149) → U18_gga(T1176, T1181, T1149, quotJ_in_ggga(T1176, T1181, s(s(s(s(s(s(s(T1181))))))), T1149))
quotJ_in_ggga(0, s(T1197), T1198, 0) → quotJ_out_ggga(0, s(T1197), T1198, 0)
quotJ_in_ggga(T1211, 0, T1212, s(T1214)) → U9_ggga(T1211, T1212, T1214, quotB_in_gga(T1211, s(T1212), T1214))
U9_ggga(T1211, T1212, T1214, quotB_out_gga(T1211, s(T1212), T1214)) → quotJ_out_ggga(T1211, 0, T1212, s(T1214))
quotJ_in_ggga(s(T1261), s(T1266), T1230, T1232) → U10_ggga(T1261, T1266, T1230, T1232, quotJ_in_ggga(T1261, T1266, T1230, T1232))
U10_ggga(T1261, T1266, T1230, T1232, quotJ_out_ggga(T1261, T1266, T1230, T1232)) → quotJ_out_ggga(s(T1261), s(T1266), T1230, T1232)
U18_gga(T1176, T1181, T1149, quotJ_out_ggga(T1176, T1181, s(s(s(s(s(s(s(T1181))))))), T1149)) → quotB_out_gga(s(s(s(s(s(s(s(s(T1176)))))))), s(s(s(s(s(s(s(s(T1181)))))))), T1149)
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)
U11_gga(x1, x2, x3)  =  U11_gga(x1, x3)
quotC_in_ga(x1, x2)  =  quotC_in_ga(x1)
quotC_out_ga(x1, x2)  =  quotC_out_ga(x1, x2)
U2_ga(x1, x2, x3)  =  U2_ga(x1, x3)
U12_gga(x1, x2, x3)  =  U12_gga(x1, x3)
quotD_in_ga(x1, x2)  =  quotD_in_ga(x1)
quotD_out_ga(x1, x2)  =  quotD_out_ga(x1, x2)
U3_ga(x1, x2, x3)  =  U3_ga(x1, x3)
U13_gga(x1, x2, x3)  =  U13_gga(x1, x3)
quotE_in_ga(x1, x2)  =  quotE_in_ga(x1)
quotE_out_ga(x1, x2)  =  quotE_out_ga(x1, x2)
U4_ga(x1, x2, x3)  =  U4_ga(x1, x3)
U14_gga(x1, x2, x3)  =  U14_gga(x1, x3)
quotF_in_ga(x1, x2)  =  quotF_in_ga(x1)
quotF_out_ga(x1, x2)  =  quotF_out_ga(x1, x2)
U5_ga(x1, x2, x3)  =  U5_ga(x1, x3)
U15_gga(x1, x2, x3)  =  U15_gga(x1, x3)
quotG_in_ga(x1, x2)  =  quotG_in_ga(x1)
quotG_out_ga(x1, x2)  =  quotG_out_ga(x1, x2)
U6_ga(x1, x2, x3)  =  U6_ga(x1, x3)
U16_gga(x1, x2, x3)  =  U16_gga(x1, x3)
quotH_in_ga(x1, x2)  =  quotH_in_ga(x1)
quotH_out_ga(x1, x2)  =  quotH_out_ga(x1, x2)
U7_ga(x1, x2, x3)  =  U7_ga(x1, x3)
U17_gga(x1, x2, x3)  =  U17_gga(x1, x3)
quotI_in_ga(x1, x2)  =  quotI_in_ga(x1)
quotI_out_ga(x1, x2)  =  quotI_out_ga(x1, x2)
U8_ga(x1, x2, x3)  =  U8_ga(x1, x3)
U18_gga(x1, x2, x3, x4)  =  U18_gga(x1, x2, x4)
quotJ_in_ggga(x1, x2, x3, x4)  =  quotJ_in_ggga(x1, x2, x3)
quotJ_out_ggga(x1, x2, x3, x4)  =  quotJ_out_ggga(x1, x2, x3, x4)
U9_ggga(x1, x2, x3, x4)  =  U9_ggga(x1, x2, x4)
U10_ggga(x1, x2, x3, x4, x5)  =  U10_ggga(x1, x2, x3, x5)
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

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

QUOTD_IN_GA(s(s(T230)), s(T232)) → QUOTD_IN_GA(T230, T232)

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

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

QUOTD_IN_GA(s(s(T230))) → QUOTD_IN_GA(T230)

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:

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

(48) YES

(49) Obligation:

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

QUOTC_IN_GA(s(T106), s(T108)) → QUOTC_IN_GA(T106, T108)

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(T68)), 0) → quotB_out_gga(s(0), s(s(T68)), 0)
quotB_in_gga(s(T77), s(0), s(T79)) → U11_gga(T77, T79, quotC_in_ga(T77, T79))
quotC_in_ga(0, 0) → quotC_out_ga(0, 0)
quotC_in_ga(s(T106), s(T108)) → U2_ga(T106, T108, quotC_in_ga(T106, T108))
U2_ga(T106, T108, quotC_out_ga(T106, T108)) → quotC_out_ga(s(T106), s(T108))
U11_gga(T77, T79, quotC_out_ga(T77, T79)) → quotB_out_gga(s(T77), s(0), s(T79))
quotB_in_gga(s(s(0)), s(s(s(T174))), 0) → quotB_out_gga(s(s(0)), s(s(s(T174))), 0)
quotB_in_gga(s(s(T183)), s(s(0)), s(T185)) → U12_gga(T183, T185, quotD_in_ga(T183, T185))
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(T230)), s(T232)) → U3_ga(T230, T232, quotD_in_ga(T230, T232))
U3_ga(T230, T232, quotD_out_ga(T230, T232)) → quotD_out_ga(s(s(T230)), s(T232))
U12_gga(T183, T185, quotD_out_ga(T183, T185)) → quotB_out_gga(s(s(T183)), s(s(0)), s(T185))
quotB_in_gga(s(s(s(0))), s(s(s(s(T298)))), 0) → quotB_out_gga(s(s(s(0))), s(s(s(s(T298)))), 0)
quotB_in_gga(s(s(s(T307))), s(s(s(0))), s(T309)) → U13_gga(T307, T309, quotE_in_ga(T307, T309))
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(T372))), s(T374)) → U4_ga(T372, T374, quotE_in_ga(T372, T374))
U4_ga(T372, T374, quotE_out_ga(T372, T374)) → quotE_out_ga(s(s(s(T372))), s(T374))
U13_gga(T307, T309, quotE_out_ga(T307, T309)) → quotB_out_gga(s(s(s(T307))), s(s(s(0))), s(T309))
quotB_in_gga(s(s(s(s(0)))), s(s(s(s(s(T440))))), 0) → quotB_out_gga(s(s(s(s(0)))), s(s(s(s(s(T440))))), 0)
quotB_in_gga(s(s(s(s(T449)))), s(s(s(s(0)))), s(T451)) → U14_gga(T449, T451, quotF_in_ga(T449, T451))
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(T532)))), s(T534)) → U5_ga(T532, T534, quotF_in_ga(T532, T534))
U5_ga(T532, T534, quotF_out_ga(T532, T534)) → quotF_out_ga(s(s(s(s(T532)))), s(T534))
U14_gga(T449, T451, quotF_out_ga(T449, T451)) → quotB_out_gga(s(s(s(s(T449)))), s(s(s(s(0)))), s(T451))
quotB_in_gga(s(s(s(s(s(0))))), s(s(s(s(s(s(T600)))))), 0) → quotB_out_gga(s(s(s(s(s(0))))), s(s(s(s(s(s(T600)))))), 0)
quotB_in_gga(s(s(s(s(s(T609))))), s(s(s(s(s(0))))), s(T611)) → U15_gga(T609, T611, quotG_in_ga(T609, T611))
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(0)))), 0) → quotG_out_ga(s(s(s(s(0)))), 0)
quotG_in_ga(s(s(s(s(s(T710))))), s(T712)) → U6_ga(T710, T712, quotG_in_ga(T710, T712))
U6_ga(T710, T712, quotG_out_ga(T710, T712)) → quotG_out_ga(s(s(s(s(s(T710))))), s(T712))
U15_gga(T609, T611, quotG_out_ga(T609, T611)) → quotB_out_gga(s(s(s(s(s(T609))))), s(s(s(s(s(0))))), s(T611))
quotB_in_gga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T778))))))), 0) → quotB_out_gga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T778))))))), 0)
quotB_in_gga(s(s(s(s(s(s(T787)))))), s(s(s(s(s(s(0)))))), s(T789)) → U16_gga(T787, T789, quotH_in_ga(T787, T789))
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(0))), 0) → quotH_out_ga(s(s(s(0))), 0)
quotH_in_ga(s(s(s(s(0)))), 0) → quotH_out_ga(s(s(s(s(0)))), 0)
quotH_in_ga(s(s(s(s(s(0))))), 0) → quotH_out_ga(s(s(s(s(s(0))))), 0)
quotH_in_ga(s(s(s(s(s(s(T906)))))), s(T908)) → U7_ga(T906, T908, quotH_in_ga(T906, T908))
U7_ga(T906, T908, quotH_out_ga(T906, T908)) → quotH_out_ga(s(s(s(s(s(s(T906)))))), s(T908))
U16_gga(T787, T789, quotH_out_ga(T787, T789)) → quotB_out_gga(s(s(s(s(s(s(T787)))))), s(s(s(s(s(s(0)))))), s(T789))
quotB_in_gga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(T974)))))))), 0) → quotB_out_gga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(T974)))))))), 0)
quotB_in_gga(s(s(s(s(s(s(s(T983))))))), s(s(s(s(s(s(s(0))))))), s(T985)) → U17_gga(T983, T985, quotI_in_ga(T983, T985))
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(0)), 0) → quotI_out_ga(s(s(0)), 0)
quotI_in_ga(s(s(s(0))), 0) → quotI_out_ga(s(s(s(0))), 0)
quotI_in_ga(s(s(s(s(0)))), 0) → quotI_out_ga(s(s(s(s(0)))), 0)
quotI_in_ga(s(s(s(s(s(0))))), 0) → quotI_out_ga(s(s(s(s(s(0))))), 0)
quotI_in_ga(s(s(s(s(s(s(0)))))), 0) → quotI_out_ga(s(s(s(s(s(s(0)))))), 0)
quotI_in_ga(s(s(s(s(s(s(s(T1120))))))), s(T1122)) → U8_ga(T1120, T1122, quotI_in_ga(T1120, T1122))
U8_ga(T1120, T1122, quotI_out_ga(T1120, T1122)) → quotI_out_ga(s(s(s(s(s(s(s(T1120))))))), s(T1122))
U17_gga(T983, T985, quotI_out_ga(T983, T985)) → quotB_out_gga(s(s(s(s(s(s(s(T983))))))), s(s(s(s(s(s(s(0))))))), s(T985))
quotB_in_gga(s(s(s(s(s(s(s(s(T1176)))))))), s(s(s(s(s(s(s(s(T1181)))))))), T1149) → U18_gga(T1176, T1181, T1149, quotJ_in_ggga(T1176, T1181, s(s(s(s(s(s(s(T1181))))))), T1149))
quotJ_in_ggga(0, s(T1197), T1198, 0) → quotJ_out_ggga(0, s(T1197), T1198, 0)
quotJ_in_ggga(T1211, 0, T1212, s(T1214)) → U9_ggga(T1211, T1212, T1214, quotB_in_gga(T1211, s(T1212), T1214))
U9_ggga(T1211, T1212, T1214, quotB_out_gga(T1211, s(T1212), T1214)) → quotJ_out_ggga(T1211, 0, T1212, s(T1214))
quotJ_in_ggga(s(T1261), s(T1266), T1230, T1232) → U10_ggga(T1261, T1266, T1230, T1232, quotJ_in_ggga(T1261, T1266, T1230, T1232))
U10_ggga(T1261, T1266, T1230, T1232, quotJ_out_ggga(T1261, T1266, T1230, T1232)) → quotJ_out_ggga(s(T1261), s(T1266), T1230, T1232)
U18_gga(T1176, T1181, T1149, quotJ_out_ggga(T1176, T1181, s(s(s(s(s(s(s(T1181))))))), T1149)) → quotB_out_gga(s(s(s(s(s(s(s(s(T1176)))))))), s(s(s(s(s(s(s(s(T1181)))))))), T1149)
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)
U11_gga(x1, x2, x3)  =  U11_gga(x1, x3)
quotC_in_ga(x1, x2)  =  quotC_in_ga(x1)
quotC_out_ga(x1, x2)  =  quotC_out_ga(x1, x2)
U2_ga(x1, x2, x3)  =  U2_ga(x1, x3)
U12_gga(x1, x2, x3)  =  U12_gga(x1, x3)
quotD_in_ga(x1, x2)  =  quotD_in_ga(x1)
quotD_out_ga(x1, x2)  =  quotD_out_ga(x1, x2)
U3_ga(x1, x2, x3)  =  U3_ga(x1, x3)
U13_gga(x1, x2, x3)  =  U13_gga(x1, x3)
quotE_in_ga(x1, x2)  =  quotE_in_ga(x1)
quotE_out_ga(x1, x2)  =  quotE_out_ga(x1, x2)
U4_ga(x1, x2, x3)  =  U4_ga(x1, x3)
U14_gga(x1, x2, x3)  =  U14_gga(x1, x3)
quotF_in_ga(x1, x2)  =  quotF_in_ga(x1)
quotF_out_ga(x1, x2)  =  quotF_out_ga(x1, x2)
U5_ga(x1, x2, x3)  =  U5_ga(x1, x3)
U15_gga(x1, x2, x3)  =  U15_gga(x1, x3)
quotG_in_ga(x1, x2)  =  quotG_in_ga(x1)
quotG_out_ga(x1, x2)  =  quotG_out_ga(x1, x2)
U6_ga(x1, x2, x3)  =  U6_ga(x1, x3)
U16_gga(x1, x2, x3)  =  U16_gga(x1, x3)
quotH_in_ga(x1, x2)  =  quotH_in_ga(x1)
quotH_out_ga(x1, x2)  =  quotH_out_ga(x1, x2)
U7_ga(x1, x2, x3)  =  U7_ga(x1, x3)
U17_gga(x1, x2, x3)  =  U17_gga(x1, x3)
quotI_in_ga(x1, x2)  =  quotI_in_ga(x1)
quotI_out_ga(x1, x2)  =  quotI_out_ga(x1, x2)
U8_ga(x1, x2, x3)  =  U8_ga(x1, x3)
U18_gga(x1, x2, x3, x4)  =  U18_gga(x1, x2, x4)
quotJ_in_ggga(x1, x2, x3, x4)  =  quotJ_in_ggga(x1, x2, x3)
quotJ_out_ggga(x1, x2, x3, x4)  =  quotJ_out_ggga(x1, x2, x3, x4)
U9_ggga(x1, x2, x3, x4)  =  U9_ggga(x1, x2, x4)
U10_ggga(x1, x2, x3, x4, x5)  =  U10_ggga(x1, x2, x3, x5)
divA_out_gga(x1, x2, x3)  =  divA_out_gga(x1, x2, x3)
QUOTC_IN_GA(x1, x2)  =  QUOTC_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:

QUOTC_IN_GA(s(T106), s(T108)) → QUOTC_IN_GA(T106, T108)

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

QUOTC_IN_GA(s(T106)) → QUOTC_IN_GA(T106)

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:

  • QUOTC_IN_GA(s(T106)) → QUOTC_IN_GA(T106)
    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(T1176)))))))), s(s(s(s(s(s(s(s(T1181)))))))), T1149) → QUOTJ_IN_GGGA(T1176, T1181, s(s(s(s(s(s(s(T1181))))))), T1149)
QUOTJ_IN_GGGA(T1211, 0, T1212, s(T1214)) → QUOTB_IN_GGA(T1211, s(T1212), T1214)
QUOTJ_IN_GGGA(s(T1261), s(T1266), T1230, T1232) → QUOTJ_IN_GGGA(T1261, T1266, T1230, T1232)

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(T68)), 0) → quotB_out_gga(s(0), s(s(T68)), 0)
quotB_in_gga(s(T77), s(0), s(T79)) → U11_gga(T77, T79, quotC_in_ga(T77, T79))
quotC_in_ga(0, 0) → quotC_out_ga(0, 0)
quotC_in_ga(s(T106), s(T108)) → U2_ga(T106, T108, quotC_in_ga(T106, T108))
U2_ga(T106, T108, quotC_out_ga(T106, T108)) → quotC_out_ga(s(T106), s(T108))
U11_gga(T77, T79, quotC_out_ga(T77, T79)) → quotB_out_gga(s(T77), s(0), s(T79))
quotB_in_gga(s(s(0)), s(s(s(T174))), 0) → quotB_out_gga(s(s(0)), s(s(s(T174))), 0)
quotB_in_gga(s(s(T183)), s(s(0)), s(T185)) → U12_gga(T183, T185, quotD_in_ga(T183, T185))
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(T230)), s(T232)) → U3_ga(T230, T232, quotD_in_ga(T230, T232))
U3_ga(T230, T232, quotD_out_ga(T230, T232)) → quotD_out_ga(s(s(T230)), s(T232))
U12_gga(T183, T185, quotD_out_ga(T183, T185)) → quotB_out_gga(s(s(T183)), s(s(0)), s(T185))
quotB_in_gga(s(s(s(0))), s(s(s(s(T298)))), 0) → quotB_out_gga(s(s(s(0))), s(s(s(s(T298)))), 0)
quotB_in_gga(s(s(s(T307))), s(s(s(0))), s(T309)) → U13_gga(T307, T309, quotE_in_ga(T307, T309))
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(T372))), s(T374)) → U4_ga(T372, T374, quotE_in_ga(T372, T374))
U4_ga(T372, T374, quotE_out_ga(T372, T374)) → quotE_out_ga(s(s(s(T372))), s(T374))
U13_gga(T307, T309, quotE_out_ga(T307, T309)) → quotB_out_gga(s(s(s(T307))), s(s(s(0))), s(T309))
quotB_in_gga(s(s(s(s(0)))), s(s(s(s(s(T440))))), 0) → quotB_out_gga(s(s(s(s(0)))), s(s(s(s(s(T440))))), 0)
quotB_in_gga(s(s(s(s(T449)))), s(s(s(s(0)))), s(T451)) → U14_gga(T449, T451, quotF_in_ga(T449, T451))
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(T532)))), s(T534)) → U5_ga(T532, T534, quotF_in_ga(T532, T534))
U5_ga(T532, T534, quotF_out_ga(T532, T534)) → quotF_out_ga(s(s(s(s(T532)))), s(T534))
U14_gga(T449, T451, quotF_out_ga(T449, T451)) → quotB_out_gga(s(s(s(s(T449)))), s(s(s(s(0)))), s(T451))
quotB_in_gga(s(s(s(s(s(0))))), s(s(s(s(s(s(T600)))))), 0) → quotB_out_gga(s(s(s(s(s(0))))), s(s(s(s(s(s(T600)))))), 0)
quotB_in_gga(s(s(s(s(s(T609))))), s(s(s(s(s(0))))), s(T611)) → U15_gga(T609, T611, quotG_in_ga(T609, T611))
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(0)))), 0) → quotG_out_ga(s(s(s(s(0)))), 0)
quotG_in_ga(s(s(s(s(s(T710))))), s(T712)) → U6_ga(T710, T712, quotG_in_ga(T710, T712))
U6_ga(T710, T712, quotG_out_ga(T710, T712)) → quotG_out_ga(s(s(s(s(s(T710))))), s(T712))
U15_gga(T609, T611, quotG_out_ga(T609, T611)) → quotB_out_gga(s(s(s(s(s(T609))))), s(s(s(s(s(0))))), s(T611))
quotB_in_gga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T778))))))), 0) → quotB_out_gga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T778))))))), 0)
quotB_in_gga(s(s(s(s(s(s(T787)))))), s(s(s(s(s(s(0)))))), s(T789)) → U16_gga(T787, T789, quotH_in_ga(T787, T789))
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(0))), 0) → quotH_out_ga(s(s(s(0))), 0)
quotH_in_ga(s(s(s(s(0)))), 0) → quotH_out_ga(s(s(s(s(0)))), 0)
quotH_in_ga(s(s(s(s(s(0))))), 0) → quotH_out_ga(s(s(s(s(s(0))))), 0)
quotH_in_ga(s(s(s(s(s(s(T906)))))), s(T908)) → U7_ga(T906, T908, quotH_in_ga(T906, T908))
U7_ga(T906, T908, quotH_out_ga(T906, T908)) → quotH_out_ga(s(s(s(s(s(s(T906)))))), s(T908))
U16_gga(T787, T789, quotH_out_ga(T787, T789)) → quotB_out_gga(s(s(s(s(s(s(T787)))))), s(s(s(s(s(s(0)))))), s(T789))
quotB_in_gga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(T974)))))))), 0) → quotB_out_gga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(T974)))))))), 0)
quotB_in_gga(s(s(s(s(s(s(s(T983))))))), s(s(s(s(s(s(s(0))))))), s(T985)) → U17_gga(T983, T985, quotI_in_ga(T983, T985))
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(0)), 0) → quotI_out_ga(s(s(0)), 0)
quotI_in_ga(s(s(s(0))), 0) → quotI_out_ga(s(s(s(0))), 0)
quotI_in_ga(s(s(s(s(0)))), 0) → quotI_out_ga(s(s(s(s(0)))), 0)
quotI_in_ga(s(s(s(s(s(0))))), 0) → quotI_out_ga(s(s(s(s(s(0))))), 0)
quotI_in_ga(s(s(s(s(s(s(0)))))), 0) → quotI_out_ga(s(s(s(s(s(s(0)))))), 0)
quotI_in_ga(s(s(s(s(s(s(s(T1120))))))), s(T1122)) → U8_ga(T1120, T1122, quotI_in_ga(T1120, T1122))
U8_ga(T1120, T1122, quotI_out_ga(T1120, T1122)) → quotI_out_ga(s(s(s(s(s(s(s(T1120))))))), s(T1122))
U17_gga(T983, T985, quotI_out_ga(T983, T985)) → quotB_out_gga(s(s(s(s(s(s(s(T983))))))), s(s(s(s(s(s(s(0))))))), s(T985))
quotB_in_gga(s(s(s(s(s(s(s(s(T1176)))))))), s(s(s(s(s(s(s(s(T1181)))))))), T1149) → U18_gga(T1176, T1181, T1149, quotJ_in_ggga(T1176, T1181, s(s(s(s(s(s(s(T1181))))))), T1149))
quotJ_in_ggga(0, s(T1197), T1198, 0) → quotJ_out_ggga(0, s(T1197), T1198, 0)
quotJ_in_ggga(T1211, 0, T1212, s(T1214)) → U9_ggga(T1211, T1212, T1214, quotB_in_gga(T1211, s(T1212), T1214))
U9_ggga(T1211, T1212, T1214, quotB_out_gga(T1211, s(T1212), T1214)) → quotJ_out_ggga(T1211, 0, T1212, s(T1214))
quotJ_in_ggga(s(T1261), s(T1266), T1230, T1232) → U10_ggga(T1261, T1266, T1230, T1232, quotJ_in_ggga(T1261, T1266, T1230, T1232))
U10_ggga(T1261, T1266, T1230, T1232, quotJ_out_ggga(T1261, T1266, T1230, T1232)) → quotJ_out_ggga(s(T1261), s(T1266), T1230, T1232)
U18_gga(T1176, T1181, T1149, quotJ_out_ggga(T1176, T1181, s(s(s(s(s(s(s(T1181))))))), T1149)) → quotB_out_gga(s(s(s(s(s(s(s(s(T1176)))))))), s(s(s(s(s(s(s(s(T1181)))))))), T1149)
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)
U11_gga(x1, x2, x3)  =  U11_gga(x1, x3)
quotC_in_ga(x1, x2)  =  quotC_in_ga(x1)
quotC_out_ga(x1, x2)  =  quotC_out_ga(x1, x2)
U2_ga(x1, x2, x3)  =  U2_ga(x1, x3)
U12_gga(x1, x2, x3)  =  U12_gga(x1, x3)
quotD_in_ga(x1, x2)  =  quotD_in_ga(x1)
quotD_out_ga(x1, x2)  =  quotD_out_ga(x1, x2)
U3_ga(x1, x2, x3)  =  U3_ga(x1, x3)
U13_gga(x1, x2, x3)  =  U13_gga(x1, x3)
quotE_in_ga(x1, x2)  =  quotE_in_ga(x1)
quotE_out_ga(x1, x2)  =  quotE_out_ga(x1, x2)
U4_ga(x1, x2, x3)  =  U4_ga(x1, x3)
U14_gga(x1, x2, x3)  =  U14_gga(x1, x3)
quotF_in_ga(x1, x2)  =  quotF_in_ga(x1)
quotF_out_ga(x1, x2)  =  quotF_out_ga(x1, x2)
U5_ga(x1, x2, x3)  =  U5_ga(x1, x3)
U15_gga(x1, x2, x3)  =  U15_gga(x1, x3)
quotG_in_ga(x1, x2)  =  quotG_in_ga(x1)
quotG_out_ga(x1, x2)  =  quotG_out_ga(x1, x2)
U6_ga(x1, x2, x3)  =  U6_ga(x1, x3)
U16_gga(x1, x2, x3)  =  U16_gga(x1, x3)
quotH_in_ga(x1, x2)  =  quotH_in_ga(x1)
quotH_out_ga(x1, x2)  =  quotH_out_ga(x1, x2)
U7_ga(x1, x2, x3)  =  U7_ga(x1, x3)
U17_gga(x1, x2, x3)  =  U17_gga(x1, x3)
quotI_in_ga(x1, x2)  =  quotI_in_ga(x1)
quotI_out_ga(x1, x2)  =  quotI_out_ga(x1, x2)
U8_ga(x1, x2, x3)  =  U8_ga(x1, x3)
U18_gga(x1, x2, x3, x4)  =  U18_gga(x1, x2, x4)
quotJ_in_ggga(x1, x2, x3, x4)  =  quotJ_in_ggga(x1, x2, x3)
quotJ_out_ggga(x1, x2, x3, x4)  =  quotJ_out_ggga(x1, x2, x3, x4)
U9_ggga(x1, x2, x3, x4)  =  U9_ggga(x1, x2, x4)
U10_ggga(x1, x2, x3, x4, x5)  =  U10_ggga(x1, x2, x3, x5)
divA_out_gga(x1, x2, x3)  =  divA_out_gga(x1, x2, x3)
QUOTB_IN_GGA(x1, x2, x3)  =  QUOTB_IN_GGA(x1, x2)
QUOTJ_IN_GGGA(x1, x2, x3, x4)  =  QUOTJ_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(T1176)))))))), s(s(s(s(s(s(s(s(T1181)))))))), T1149) → QUOTJ_IN_GGGA(T1176, T1181, s(s(s(s(s(s(s(T1181))))))), T1149)
QUOTJ_IN_GGGA(T1211, 0, T1212, s(T1214)) → QUOTB_IN_GGA(T1211, s(T1212), T1214)
QUOTJ_IN_GGGA(s(T1261), s(T1266), T1230, T1232) → QUOTJ_IN_GGGA(T1261, T1266, T1230, T1232)

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)
QUOTJ_IN_GGGA(x1, x2, x3, x4)  =  QUOTJ_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(T1176)))))))), s(s(s(s(s(s(s(s(T1181))))))))) → QUOTJ_IN_GGGA(T1176, T1181, s(s(s(s(s(s(s(T1181))))))))
QUOTJ_IN_GGGA(T1211, 0, T1212) → QUOTB_IN_GGA(T1211, s(T1212))
QUOTJ_IN_GGGA(s(T1261), s(T1266), T1230) → QUOTJ_IN_GGGA(T1261, T1266, T1230)

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:

  • QUOTJ_IN_GGGA(T1211, 0, T1212) → QUOTB_IN_GGA(T1211, s(T1212))
    The graph contains the following edges 1 >= 1

  • QUOTJ_IN_GGGA(s(T1261), s(T1266), T1230) → QUOTJ_IN_GGGA(T1261, T1266, T1230)
    The graph contains the following edges 1 > 1, 2 > 2, 3 >= 3

  • QUOTB_IN_GGA(s(s(s(s(s(s(s(s(T1176)))))))), s(s(s(s(s(s(s(s(T1181))))))))) → QUOTJ_IN_GGGA(T1176, T1181, s(s(s(s(s(s(s(T1181))))))))
    The graph contains the following edges 1 > 1, 2 > 2, 2 > 3

(62) YES