(0) Obligation:

Clauses:

div(X, Y, Z) :- quot(X, Y, Y, Z).
quot(0, s(Y), s(Z), R) :- ','(!, eq(R, 0)).
quot(X, 0, Z, U) :- ','(!, ','(eq(Z, s(X1)), ','(p(U, P), quot(X, Z, Z, P)))).
quot(s(X), Y, Z, U) :- ','(p(Y, P), quot(X, P, Z, U)).
p(0, 0).
p(s(X), X).
eq(X, X).

Queries:

div(g,g,a).

(1) PrologToDTProblemTransformerProof (SOUND transformation)

Built DT problem from termination graph.

(2) Obligation:

Triples:

quot52(s(T85)) :- quot66(T85).
quot78(s(T108), T110) :- quot93(T108, T110).
quot93(T121, 0) :- quot52(T121).
quot93(T121, s(T127)) :- quot78(T121, T127).
quot134(s(s(T176))) :- quot161(T176).
quot173(s(s(T217)), T219) :- quot202(T217, T219).
quot202(T230, 0) :- quot134(T230).
quot202(T230, s(T236)) :- quot173(T230, T236).
quot243(s(s(s(T289)))) :- quot283(T289).
quot295(s(s(s(T348))), T350) :- quot338(T348, T350).
quot338(T361, 0) :- quot243(T361).
quot338(T361, s(T367)) :- quot295(T361, T367).
quot379(s(s(s(s(T424))))) :- quot432(T424).
quot444(s(s(s(s(T501)))), T503) :- quot501(T501, T503).
quot501(T514, 0) :- quot379(T514).
quot501(T514, s(T520)) :- quot444(T514, T520).
quot542(s(s(s(s(s(T581)))))) :- quot608(T581).
quot620(s(s(s(s(s(T676))))), T678) :- quot691(T676, T678).
quot691(T689, 0) :- quot542(T689).
quot691(T689, s(T695)) :- quot620(T689, T695).
quot732(s(s(s(s(s(s(T760))))))) :- quot811(T760).
quot823(s(s(s(s(s(s(T873)))))), T875) :- quot908(T873, T875).
quot908(T886, 0) :- quot732(T886).
quot908(T886, s(T892)) :- quot823(T886, T892).
quot949(s(s(s(s(s(s(s(T961)))))))) :- quot1041(T961).
quot1053(s(s(s(s(s(s(s(T1092))))))), T1094) :- quot1152(T1092, T1094).
quot1152(T1105, 0) :- quot949(T1105).
quot1152(T1105, s(T1111)) :- quot1053(T1105, T1111).
quot66(T90) :- quot52(T90).
quot161(T181) :- quot134(T181).
quot283(T294) :- quot243(T294).
quot432(T429) :- quot379(T429).
quot608(T586) :- quot542(T586).
quot811(T765) :- quot732(T765).
quot1041(T966) :- quot949(T966).
quot1194(s(T1195), 0) :- quot52(T1195).
quot1194(s(s(T1200)), 0) :- quot66(T1200).
quot1194(s(s(T1215)), s(0)) :- quot134(T1215).
quot1194(s(s(s(T1220))), s(0)) :- quot161(T1220).
quot1194(s(s(s(T1235))), s(s(0))) :- quot243(T1235).
quot1194(s(s(s(s(T1240)))), s(s(0))) :- quot283(T1240).
quot1194(s(s(s(s(T1255)))), s(s(s(0)))) :- quot379(T1255).
quot1194(s(s(s(s(s(T1260))))), s(s(s(0)))) :- quot432(T1260).
quot1194(s(s(s(s(s(T1275))))), s(s(s(s(0))))) :- quot542(T1275).
quot1194(s(s(s(s(s(s(T1280)))))), s(s(s(s(0))))) :- quot608(T1280).
quot1194(s(s(s(s(s(s(T1295)))))), s(s(s(s(s(0)))))) :- quot732(T1295).
quot1194(s(s(s(s(s(s(s(T1300))))))), s(s(s(s(s(0)))))) :- quot811(T1300).
quot1194(s(s(s(s(s(s(s(T1315))))))), s(s(s(s(s(s(0))))))) :- quot949(T1315).
quot1194(s(s(s(s(s(s(s(s(T1320)))))))), s(s(s(s(s(s(0))))))) :- quot1041(T1320).
quot1194(s(s(s(s(s(s(s(s(T1320)))))))), s(s(s(s(s(s(s(T1326)))))))) :- quot1405(T1320, T1326, s(s(s(s(s(s(s(T1326)))))))).
quot1405(T1345, 0, T1351) :- quot1194(T1345, T1351).
quot1405(s(T1372), 0, T1378) :- quot1194(T1372, T1378).
quot1405(s(T1362), s(T1385), T1364) :- quot1405(T1362, T1385, T1364).
quot3(s(T79), s(0), 0) :- quot52(T79).
quot3(s(T79), s(0), s(T94)) :- quot78(T79, T94).
quot3(s(s(T135)), s(0), T138) :- quot93(T135, T138).
quot3(s(s(T166)), s(s(0)), 0) :- quot134(T166).
quot3(s(s(T166)), s(s(0)), s(T185)) :- quot173(T166, T185).
quot3(s(s(s(T244))), s(s(0)), T247) :- quot202(T244, T247).
quot3(s(s(s(T275))), s(s(s(0))), 0) :- quot243(T275).
quot3(s(s(s(T275))), s(s(s(0))), s(T298)) :- quot295(T275, T298).
quot3(s(s(s(s(T375)))), s(s(s(0))), T378) :- quot338(T375, T378).
quot3(s(s(s(s(T406)))), s(s(s(s(0)))), 0) :- quot379(T406).
quot3(s(s(s(s(T406)))), s(s(s(s(0)))), s(T433)) :- quot444(T406, T433).
quot3(s(s(s(s(s(T528))))), s(s(s(s(0)))), T531) :- quot501(T528, T531).
quot3(s(s(s(s(s(T559))))), s(s(s(s(s(0))))), 0) :- quot542(T559).
quot3(s(s(s(s(s(T559))))), s(s(s(s(s(0))))), s(T590)) :- quot620(T559, T590).
quot3(s(s(s(s(s(s(T703)))))), s(s(s(s(s(0))))), T706) :- quot691(T703, T706).
quot3(s(s(s(s(s(s(T734)))))), s(s(s(s(s(s(0)))))), 0) :- quot732(T734).
quot3(s(s(s(s(s(s(T734)))))), s(s(s(s(s(s(0)))))), s(T769)) :- quot823(T734, T769).
quot3(s(s(s(s(s(s(s(T900))))))), s(s(s(s(s(s(0)))))), T903) :- quot908(T900, T903).
quot3(s(s(s(s(s(s(s(T931))))))), s(s(s(s(s(s(s(0))))))), 0) :- quot949(T931).
quot3(s(s(s(s(s(s(s(T931))))))), s(s(s(s(s(s(s(0))))))), s(T970)) :- quot1053(T931, T970).
quot3(s(s(s(s(s(s(s(s(T1119)))))))), s(s(s(s(s(s(s(0))))))), T1122) :- quot1152(T1119, T1122).
quot3(s(s(s(s(s(s(s(s(T1119)))))))), s(s(s(s(s(s(s(s(T1129)))))))), T1122) :- quot1175(T1119, T1129, s(s(s(s(s(s(s(T1129))))))), T1122).
quot1175(T1161, 0, T1169, 0) :- quot1194(T1161, T1169).
quot1175(T1161, 0, T1169, s(T1391)) :- quot3(T1161, s(T1169), T1391).
quot1175(s(T1419), 0, T1427, 0) :- quot1194(T1419, T1427).
quot1175(s(T1419), 0, T1427, s(T1433)) :- quot3(T1419, s(T1427), T1433).
quot1175(s(T1402), s(T1438), T1404, T1406) :- quot1175(T1402, T1438, T1404, T1406).
div1(T7, T8, T10) :- quot3(T7, T8, T10).

Clauses:

quotc52(0).
quotc52(s(T85)) :- quotc66(T85).
quotc78(0, 0).
quotc78(s(T108), T110) :- quotc93(T108, T110).
quotc93(T121, 0) :- quotc52(T121).
quotc93(T121, s(T127)) :- quotc78(T121, T127).
quotc134(0).
quotc134(s(0)).
quotc134(s(s(T176))) :- quotc161(T176).
quotc173(0, 0).
quotc173(s(0), 0).
quotc173(s(s(T217)), T219) :- quotc202(T217, T219).
quotc202(T230, 0) :- quotc134(T230).
quotc202(T230, s(T236)) :- quotc173(T230, T236).
quotc243(0).
quotc243(s(0)).
quotc243(s(s(0))).
quotc243(s(s(s(T289)))) :- quotc283(T289).
quotc295(0, 0).
quotc295(s(0), 0).
quotc295(s(s(0)), 0).
quotc295(s(s(s(T348))), T350) :- quotc338(T348, T350).
quotc338(T361, 0) :- quotc243(T361).
quotc338(T361, s(T367)) :- quotc295(T361, T367).
quotc379(0).
quotc379(s(0)).
quotc379(s(s(0))).
quotc379(s(s(s(0)))).
quotc379(s(s(s(s(T424))))) :- quotc432(T424).
quotc444(0, 0).
quotc444(s(0), 0).
quotc444(s(s(0)), 0).
quotc444(s(s(s(0))), 0).
quotc444(s(s(s(s(T501)))), T503) :- quotc501(T501, T503).
quotc501(T514, 0) :- quotc379(T514).
quotc501(T514, s(T520)) :- quotc444(T514, T520).
quotc542(0).
quotc542(s(0)).
quotc542(s(s(0))).
quotc542(s(s(s(0)))).
quotc542(s(s(s(s(0))))).
quotc542(s(s(s(s(s(T581)))))) :- quotc608(T581).
quotc620(0, 0).
quotc620(s(0), 0).
quotc620(s(s(0)), 0).
quotc620(s(s(s(0))), 0).
quotc620(s(s(s(s(0)))), 0).
quotc620(s(s(s(s(s(T676))))), T678) :- quotc691(T676, T678).
quotc691(T689, 0) :- quotc542(T689).
quotc691(T689, s(T695)) :- quotc620(T689, T695).
quotc732(0).
quotc732(s(0)).
quotc732(s(s(0))).
quotc732(s(s(s(0)))).
quotc732(s(s(s(s(0))))).
quotc732(s(s(s(s(s(0)))))).
quotc732(s(s(s(s(s(s(T760))))))) :- quotc811(T760).
quotc823(0, 0).
quotc823(s(0), 0).
quotc823(s(s(0)), 0).
quotc823(s(s(s(0))), 0).
quotc823(s(s(s(s(0)))), 0).
quotc823(s(s(s(s(s(0))))), 0).
quotc823(s(s(s(s(s(s(T873)))))), T875) :- quotc908(T873, T875).
quotc908(T886, 0) :- quotc732(T886).
quotc908(T886, s(T892)) :- quotc823(T886, T892).
quotc949(0).
quotc949(s(0)).
quotc949(s(s(0))).
quotc949(s(s(s(0)))).
quotc949(s(s(s(s(0))))).
quotc949(s(s(s(s(s(0)))))).
quotc949(s(s(s(s(s(s(0))))))).
quotc949(s(s(s(s(s(s(s(T961)))))))) :- quotc1041(T961).
quotc1053(0, 0).
quotc1053(s(0), 0).
quotc1053(s(s(0)), 0).
quotc1053(s(s(s(0))), 0).
quotc1053(s(s(s(s(0)))), 0).
quotc1053(s(s(s(s(s(0))))), 0).
quotc1053(s(s(s(s(s(s(0)))))), 0).
quotc1053(s(s(s(s(s(s(s(T1092))))))), T1094) :- quotc1152(T1092, T1094).
quotc1152(T1105, 0) :- quotc949(T1105).
quotc1152(T1105, s(T1111)) :- quotc1053(T1105, T1111).
quotc66(T90) :- quotc52(T90).
quotc161(T181) :- quotc134(T181).
quotc283(T294) :- quotc243(T294).
quotc432(T429) :- quotc379(T429).
quotc608(T586) :- quotc542(T586).
quotc811(T765) :- quotc732(T765).
quotc1041(T966) :- quotc949(T966).
quotc1194(0, T1174).
quotc1194(s(0), s(T1190)).
quotc1194(s(T1195), 0) :- quotc52(T1195).
quotc1194(s(s(T1200)), 0) :- quotc66(T1200).
quotc1194(s(s(0)), s(s(T1210))).
quotc1194(s(s(T1215)), s(0)) :- quotc134(T1215).
quotc1194(s(s(s(T1220))), s(0)) :- quotc161(T1220).
quotc1194(s(s(s(0))), s(s(s(T1230)))).
quotc1194(s(s(s(T1235))), s(s(0))) :- quotc243(T1235).
quotc1194(s(s(s(s(T1240)))), s(s(0))) :- quotc283(T1240).
quotc1194(s(s(s(s(0)))), s(s(s(s(T1250))))).
quotc1194(s(s(s(s(T1255)))), s(s(s(0)))) :- quotc379(T1255).
quotc1194(s(s(s(s(s(T1260))))), s(s(s(0)))) :- quotc432(T1260).
quotc1194(s(s(s(s(s(0))))), s(s(s(s(s(T1270)))))).
quotc1194(s(s(s(s(s(T1275))))), s(s(s(s(0))))) :- quotc542(T1275).
quotc1194(s(s(s(s(s(s(T1280)))))), s(s(s(s(0))))) :- quotc608(T1280).
quotc1194(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(T1290))))))).
quotc1194(s(s(s(s(s(s(T1295)))))), s(s(s(s(s(0)))))) :- quotc732(T1295).
quotc1194(s(s(s(s(s(s(s(T1300))))))), s(s(s(s(s(0)))))) :- quotc811(T1300).
quotc1194(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(T1310)))))))).
quotc1194(s(s(s(s(s(s(s(T1315))))))), s(s(s(s(s(s(0))))))) :- quotc949(T1315).
quotc1194(s(s(s(s(s(s(s(s(T1320)))))))), s(s(s(s(s(s(0))))))) :- quotc1041(T1320).
quotc1194(s(s(s(s(s(s(s(s(T1320)))))))), s(s(s(s(s(s(s(T1326)))))))) :- quotc1405(T1320, T1326, s(s(s(s(s(s(s(T1326)))))))).
quotc1405(0, s(T1335), T1336).
quotc1405(T1345, 0, T1351) :- quotc1194(T1345, T1351).
quotc1405(s(T1372), 0, T1378) :- quotc1194(T1372, T1378).
quotc1405(s(T1362), s(T1385), T1364) :- quotc1405(T1362, T1385, T1364).
quotc3(0, s(T15), 0).
quotc3(s(0), s(s(T65)), 0).
quotc3(s(T79), s(0), 0) :- quotc52(T79).
quotc3(s(T79), s(0), s(T94)) :- quotc78(T79, T94).
quotc3(s(s(T135)), s(0), T138) :- quotc93(T135, T138).
quotc3(s(s(0)), s(s(s(T152))), 0).
quotc3(s(s(T166)), s(s(0)), 0) :- quotc134(T166).
quotc3(s(s(T166)), s(s(0)), s(T185)) :- quotc173(T166, T185).
quotc3(s(s(s(T244))), s(s(0)), T247) :- quotc202(T244, T247).
quotc3(s(s(s(0))), s(s(s(s(T261)))), 0).
quotc3(s(s(s(T275))), s(s(s(0))), 0) :- quotc243(T275).
quotc3(s(s(s(T275))), s(s(s(0))), s(T298)) :- quotc295(T275, T298).
quotc3(s(s(s(s(T375)))), s(s(s(0))), T378) :- quotc338(T375, T378).
quotc3(s(s(s(s(0)))), s(s(s(s(s(T392))))), 0).
quotc3(s(s(s(s(T406)))), s(s(s(s(0)))), 0) :- quotc379(T406).
quotc3(s(s(s(s(T406)))), s(s(s(s(0)))), s(T433)) :- quotc444(T406, T433).
quotc3(s(s(s(s(s(T528))))), s(s(s(s(0)))), T531) :- quotc501(T528, T531).
quotc3(s(s(s(s(s(0))))), s(s(s(s(s(s(T545)))))), 0).
quotc3(s(s(s(s(s(T559))))), s(s(s(s(s(0))))), 0) :- quotc542(T559).
quotc3(s(s(s(s(s(T559))))), s(s(s(s(s(0))))), s(T590)) :- quotc620(T559, T590).
quotc3(s(s(s(s(s(s(T703)))))), s(s(s(s(s(0))))), T706) :- quotc691(T703, T706).
quotc3(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T720))))))), 0).
quotc3(s(s(s(s(s(s(T734)))))), s(s(s(s(s(s(0)))))), 0) :- quotc732(T734).
quotc3(s(s(s(s(s(s(T734)))))), s(s(s(s(s(s(0)))))), s(T769)) :- quotc823(T734, T769).
quotc3(s(s(s(s(s(s(s(T900))))))), s(s(s(s(s(s(0)))))), T903) :- quotc908(T900, T903).
quotc3(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(T917)))))))), 0).
quotc3(s(s(s(s(s(s(s(T931))))))), s(s(s(s(s(s(s(0))))))), 0) :- quotc949(T931).
quotc3(s(s(s(s(s(s(s(T931))))))), s(s(s(s(s(s(s(0))))))), s(T970)) :- quotc1053(T931, T970).
quotc3(s(s(s(s(s(s(s(s(T1119)))))))), s(s(s(s(s(s(s(0))))))), T1122) :- quotc1152(T1119, T1122).
quotc3(s(s(s(s(s(s(s(s(T1119)))))))), s(s(s(s(s(s(s(s(T1129)))))))), T1122) :- quotc1175(T1119, T1129, s(s(s(s(s(s(s(T1129))))))), T1122).
quotc1175(0, s(T1142), T1143, 0).
quotc1175(T1161, 0, T1169, 0) :- quotc1194(T1161, T1169).
quotc1175(T1161, 0, T1169, s(T1391)) :- quotc3(T1161, s(T1169), T1391).
quotc1175(s(T1419), 0, T1427, 0) :- quotc1194(T1419, T1427).
quotc1175(s(T1419), 0, T1427, s(T1433)) :- quotc3(T1419, s(T1427), T1433).
quotc1175(s(T1402), s(T1438), T1404, T1406) :- quotc1175(T1402, T1438, T1404, T1406).

Afs:

div1(x1, x2, x3)  =  div1(x1, x2)

(3) TriplesToPiDPProof (SOUND transformation)

We use the technique of [LOPSTR]. With regard to the inferred argument filtering the predicates were used in the following modes:
div1_in: (b,b,f)
quot3_in: (b,b,f)
quot52_in: (b)
quot66_in: (b)
quot78_in: (b,f)
quot93_in: (b,f)
quot134_in: (b)
quot161_in: (b)
quot173_in: (b,f)
quot202_in: (b,f)
quot243_in: (b)
quot283_in: (b)
quot295_in: (b,f)
quot338_in: (b,f)
quot379_in: (b)
quot432_in: (b)
quot444_in: (b,f)
quot501_in: (b,f)
quot542_in: (b)
quot608_in: (b)
quot620_in: (b,f)
quot691_in: (b,f)
quot732_in: (b)
quot811_in: (b)
quot823_in: (b,f)
quot908_in: (b,f)
quot949_in: (b)
quot1041_in: (b)
quot1053_in: (b,f)
quot1152_in: (b,f)
quot1175_in: (b,b,b,f)
quot1194_in: (b,b)
quot1405_in: (b,b,b)
Transforming TRIPLES into the following Term Rewriting System:
Pi DP problem:
The TRS P consists of the following rules:

DIV1_IN_GGA(T7, T8, T10) → U81_GGA(T7, T8, T10, quot3_in_gga(T7, T8, T10))
DIV1_IN_GGA(T7, T8, T10) → QUOT3_IN_GGA(T7, T8, T10)
QUOT3_IN_GGA(s(T79), s(0), 0) → U54_GGA(T79, quot52_in_g(T79))
QUOT3_IN_GGA(s(T79), s(0), 0) → QUOT52_IN_G(T79)
QUOT52_IN_G(s(T85)) → U1_G(T85, quot66_in_g(T85))
QUOT52_IN_G(s(T85)) → QUOT66_IN_G(T85)
QUOT66_IN_G(T90) → U29_G(T90, quot52_in_g(T90))
QUOT66_IN_G(T90) → QUOT52_IN_G(T90)
QUOT3_IN_GGA(s(T79), s(0), s(T94)) → U55_GGA(T79, T94, quot78_in_ga(T79, T94))
QUOT3_IN_GGA(s(T79), s(0), s(T94)) → QUOT78_IN_GA(T79, T94)
QUOT78_IN_GA(s(T108), T110) → U2_GA(T108, T110, quot93_in_ga(T108, T110))
QUOT78_IN_GA(s(T108), T110) → QUOT93_IN_GA(T108, T110)
QUOT93_IN_GA(T121, 0) → U3_GA(T121, quot52_in_g(T121))
QUOT93_IN_GA(T121, 0) → QUOT52_IN_G(T121)
QUOT93_IN_GA(T121, s(T127)) → U4_GA(T121, T127, quot78_in_ga(T121, T127))
QUOT93_IN_GA(T121, s(T127)) → QUOT78_IN_GA(T121, T127)
QUOT3_IN_GGA(s(s(T135)), s(0), T138) → U56_GGA(T135, T138, quot93_in_ga(T135, T138))
QUOT3_IN_GGA(s(s(T135)), s(0), T138) → QUOT93_IN_GA(T135, T138)
QUOT3_IN_GGA(s(s(T166)), s(s(0)), 0) → U57_GGA(T166, quot134_in_g(T166))
QUOT3_IN_GGA(s(s(T166)), s(s(0)), 0) → QUOT134_IN_G(T166)
QUOT134_IN_G(s(s(T176))) → U5_G(T176, quot161_in_g(T176))
QUOT134_IN_G(s(s(T176))) → QUOT161_IN_G(T176)
QUOT161_IN_G(T181) → U30_G(T181, quot134_in_g(T181))
QUOT161_IN_G(T181) → QUOT134_IN_G(T181)
QUOT3_IN_GGA(s(s(T166)), s(s(0)), s(T185)) → U58_GGA(T166, T185, quot173_in_ga(T166, T185))
QUOT3_IN_GGA(s(s(T166)), s(s(0)), s(T185)) → QUOT173_IN_GA(T166, T185)
QUOT173_IN_GA(s(s(T217)), T219) → U6_GA(T217, T219, quot202_in_ga(T217, T219))
QUOT173_IN_GA(s(s(T217)), T219) → QUOT202_IN_GA(T217, T219)
QUOT202_IN_GA(T230, 0) → U7_GA(T230, quot134_in_g(T230))
QUOT202_IN_GA(T230, 0) → QUOT134_IN_G(T230)
QUOT202_IN_GA(T230, s(T236)) → U8_GA(T230, T236, quot173_in_ga(T230, T236))
QUOT202_IN_GA(T230, s(T236)) → QUOT173_IN_GA(T230, T236)
QUOT3_IN_GGA(s(s(s(T244))), s(s(0)), T247) → U59_GGA(T244, T247, quot202_in_ga(T244, T247))
QUOT3_IN_GGA(s(s(s(T244))), s(s(0)), T247) → QUOT202_IN_GA(T244, T247)
QUOT3_IN_GGA(s(s(s(T275))), s(s(s(0))), 0) → U60_GGA(T275, quot243_in_g(T275))
QUOT3_IN_GGA(s(s(s(T275))), s(s(s(0))), 0) → QUOT243_IN_G(T275)
QUOT243_IN_G(s(s(s(T289)))) → U9_G(T289, quot283_in_g(T289))
QUOT243_IN_G(s(s(s(T289)))) → QUOT283_IN_G(T289)
QUOT283_IN_G(T294) → U31_G(T294, quot243_in_g(T294))
QUOT283_IN_G(T294) → QUOT243_IN_G(T294)
QUOT3_IN_GGA(s(s(s(T275))), s(s(s(0))), s(T298)) → U61_GGA(T275, T298, quot295_in_ga(T275, T298))
QUOT3_IN_GGA(s(s(s(T275))), s(s(s(0))), s(T298)) → QUOT295_IN_GA(T275, T298)
QUOT295_IN_GA(s(s(s(T348))), T350) → U10_GA(T348, T350, quot338_in_ga(T348, T350))
QUOT295_IN_GA(s(s(s(T348))), T350) → QUOT338_IN_GA(T348, T350)
QUOT338_IN_GA(T361, 0) → U11_GA(T361, quot243_in_g(T361))
QUOT338_IN_GA(T361, 0) → QUOT243_IN_G(T361)
QUOT338_IN_GA(T361, s(T367)) → U12_GA(T361, T367, quot295_in_ga(T361, T367))
QUOT338_IN_GA(T361, s(T367)) → QUOT295_IN_GA(T361, T367)
QUOT3_IN_GGA(s(s(s(s(T375)))), s(s(s(0))), T378) → U62_GGA(T375, T378, quot338_in_ga(T375, T378))
QUOT3_IN_GGA(s(s(s(s(T375)))), s(s(s(0))), T378) → QUOT338_IN_GA(T375, T378)
QUOT3_IN_GGA(s(s(s(s(T406)))), s(s(s(s(0)))), 0) → U63_GGA(T406, quot379_in_g(T406))
QUOT3_IN_GGA(s(s(s(s(T406)))), s(s(s(s(0)))), 0) → QUOT379_IN_G(T406)
QUOT379_IN_G(s(s(s(s(T424))))) → U13_G(T424, quot432_in_g(T424))
QUOT379_IN_G(s(s(s(s(T424))))) → QUOT432_IN_G(T424)
QUOT432_IN_G(T429) → U32_G(T429, quot379_in_g(T429))
QUOT432_IN_G(T429) → QUOT379_IN_G(T429)
QUOT3_IN_GGA(s(s(s(s(T406)))), s(s(s(s(0)))), s(T433)) → U64_GGA(T406, T433, quot444_in_ga(T406, T433))
QUOT3_IN_GGA(s(s(s(s(T406)))), s(s(s(s(0)))), s(T433)) → QUOT444_IN_GA(T406, T433)
QUOT444_IN_GA(s(s(s(s(T501)))), T503) → U14_GA(T501, T503, quot501_in_ga(T501, T503))
QUOT444_IN_GA(s(s(s(s(T501)))), T503) → QUOT501_IN_GA(T501, T503)
QUOT501_IN_GA(T514, 0) → U15_GA(T514, quot379_in_g(T514))
QUOT501_IN_GA(T514, 0) → QUOT379_IN_G(T514)
QUOT501_IN_GA(T514, s(T520)) → U16_GA(T514, T520, quot444_in_ga(T514, T520))
QUOT501_IN_GA(T514, s(T520)) → QUOT444_IN_GA(T514, T520)
QUOT3_IN_GGA(s(s(s(s(s(T528))))), s(s(s(s(0)))), T531) → U65_GGA(T528, T531, quot501_in_ga(T528, T531))
QUOT3_IN_GGA(s(s(s(s(s(T528))))), s(s(s(s(0)))), T531) → QUOT501_IN_GA(T528, T531)
QUOT3_IN_GGA(s(s(s(s(s(T559))))), s(s(s(s(s(0))))), 0) → U66_GGA(T559, quot542_in_g(T559))
QUOT3_IN_GGA(s(s(s(s(s(T559))))), s(s(s(s(s(0))))), 0) → QUOT542_IN_G(T559)
QUOT542_IN_G(s(s(s(s(s(T581)))))) → U17_G(T581, quot608_in_g(T581))
QUOT542_IN_G(s(s(s(s(s(T581)))))) → QUOT608_IN_G(T581)
QUOT608_IN_G(T586) → U33_G(T586, quot542_in_g(T586))
QUOT608_IN_G(T586) → QUOT542_IN_G(T586)
QUOT3_IN_GGA(s(s(s(s(s(T559))))), s(s(s(s(s(0))))), s(T590)) → U67_GGA(T559, T590, quot620_in_ga(T559, T590))
QUOT3_IN_GGA(s(s(s(s(s(T559))))), s(s(s(s(s(0))))), s(T590)) → QUOT620_IN_GA(T559, T590)
QUOT620_IN_GA(s(s(s(s(s(T676))))), T678) → U18_GA(T676, T678, quot691_in_ga(T676, T678))
QUOT620_IN_GA(s(s(s(s(s(T676))))), T678) → QUOT691_IN_GA(T676, T678)
QUOT691_IN_GA(T689, 0) → U19_GA(T689, quot542_in_g(T689))
QUOT691_IN_GA(T689, 0) → QUOT542_IN_G(T689)
QUOT691_IN_GA(T689, s(T695)) → U20_GA(T689, T695, quot620_in_ga(T689, T695))
QUOT691_IN_GA(T689, s(T695)) → QUOT620_IN_GA(T689, T695)
QUOT3_IN_GGA(s(s(s(s(s(s(T703)))))), s(s(s(s(s(0))))), T706) → U68_GGA(T703, T706, quot691_in_ga(T703, T706))
QUOT3_IN_GGA(s(s(s(s(s(s(T703)))))), s(s(s(s(s(0))))), T706) → QUOT691_IN_GA(T703, T706)
QUOT3_IN_GGA(s(s(s(s(s(s(T734)))))), s(s(s(s(s(s(0)))))), 0) → U69_GGA(T734, quot732_in_g(T734))
QUOT3_IN_GGA(s(s(s(s(s(s(T734)))))), s(s(s(s(s(s(0)))))), 0) → QUOT732_IN_G(T734)
QUOT732_IN_G(s(s(s(s(s(s(T760))))))) → U21_G(T760, quot811_in_g(T760))
QUOT732_IN_G(s(s(s(s(s(s(T760))))))) → QUOT811_IN_G(T760)
QUOT811_IN_G(T765) → U34_G(T765, quot732_in_g(T765))
QUOT811_IN_G(T765) → QUOT732_IN_G(T765)
QUOT3_IN_GGA(s(s(s(s(s(s(T734)))))), s(s(s(s(s(s(0)))))), s(T769)) → U70_GGA(T734, T769, quot823_in_ga(T734, T769))
QUOT3_IN_GGA(s(s(s(s(s(s(T734)))))), s(s(s(s(s(s(0)))))), s(T769)) → QUOT823_IN_GA(T734, T769)
QUOT823_IN_GA(s(s(s(s(s(s(T873)))))), T875) → U22_GA(T873, T875, quot908_in_ga(T873, T875))
QUOT823_IN_GA(s(s(s(s(s(s(T873)))))), T875) → QUOT908_IN_GA(T873, T875)
QUOT908_IN_GA(T886, 0) → U23_GA(T886, quot732_in_g(T886))
QUOT908_IN_GA(T886, 0) → QUOT732_IN_G(T886)
QUOT908_IN_GA(T886, s(T892)) → U24_GA(T886, T892, quot823_in_ga(T886, T892))
QUOT908_IN_GA(T886, s(T892)) → QUOT823_IN_GA(T886, T892)
QUOT3_IN_GGA(s(s(s(s(s(s(s(T900))))))), s(s(s(s(s(s(0)))))), T903) → U71_GGA(T900, T903, quot908_in_ga(T900, T903))
QUOT3_IN_GGA(s(s(s(s(s(s(s(T900))))))), s(s(s(s(s(s(0)))))), T903) → QUOT908_IN_GA(T900, T903)
QUOT3_IN_GGA(s(s(s(s(s(s(s(T931))))))), s(s(s(s(s(s(s(0))))))), 0) → U72_GGA(T931, quot949_in_g(T931))
QUOT3_IN_GGA(s(s(s(s(s(s(s(T931))))))), s(s(s(s(s(s(s(0))))))), 0) → QUOT949_IN_G(T931)
QUOT949_IN_G(s(s(s(s(s(s(s(T961)))))))) → U25_G(T961, quot1041_in_g(T961))
QUOT949_IN_G(s(s(s(s(s(s(s(T961)))))))) → QUOT1041_IN_G(T961)
QUOT1041_IN_G(T966) → U35_G(T966, quot949_in_g(T966))
QUOT1041_IN_G(T966) → QUOT949_IN_G(T966)
QUOT3_IN_GGA(s(s(s(s(s(s(s(T931))))))), s(s(s(s(s(s(s(0))))))), s(T970)) → U73_GGA(T931, T970, quot1053_in_ga(T931, T970))
QUOT3_IN_GGA(s(s(s(s(s(s(s(T931))))))), s(s(s(s(s(s(s(0))))))), s(T970)) → QUOT1053_IN_GA(T931, T970)
QUOT1053_IN_GA(s(s(s(s(s(s(s(T1092))))))), T1094) → U26_GA(T1092, T1094, quot1152_in_ga(T1092, T1094))
QUOT1053_IN_GA(s(s(s(s(s(s(s(T1092))))))), T1094) → QUOT1152_IN_GA(T1092, T1094)
QUOT1152_IN_GA(T1105, 0) → U27_GA(T1105, quot949_in_g(T1105))
QUOT1152_IN_GA(T1105, 0) → QUOT949_IN_G(T1105)
QUOT1152_IN_GA(T1105, s(T1111)) → U28_GA(T1105, T1111, quot1053_in_ga(T1105, T1111))
QUOT1152_IN_GA(T1105, s(T1111)) → QUOT1053_IN_GA(T1105, T1111)
QUOT3_IN_GGA(s(s(s(s(s(s(s(s(T1119)))))))), s(s(s(s(s(s(s(0))))))), T1122) → U74_GGA(T1119, T1122, quot1152_in_ga(T1119, T1122))
QUOT3_IN_GGA(s(s(s(s(s(s(s(s(T1119)))))))), s(s(s(s(s(s(s(0))))))), T1122) → QUOT1152_IN_GA(T1119, T1122)
QUOT3_IN_GGA(s(s(s(s(s(s(s(s(T1119)))))))), s(s(s(s(s(s(s(s(T1129)))))))), T1122) → U75_GGA(T1119, T1129, T1122, quot1175_in_ggga(T1119, T1129, s(s(s(s(s(s(s(T1129))))))), T1122))
QUOT3_IN_GGA(s(s(s(s(s(s(s(s(T1119)))))))), s(s(s(s(s(s(s(s(T1129)))))))), T1122) → QUOT1175_IN_GGGA(T1119, T1129, s(s(s(s(s(s(s(T1129))))))), T1122)
QUOT1175_IN_GGGA(T1161, 0, T1169, 0) → U76_GGGA(T1161, T1169, quot1194_in_gg(T1161, T1169))
QUOT1175_IN_GGGA(T1161, 0, T1169, 0) → QUOT1194_IN_GG(T1161, T1169)
QUOT1194_IN_GG(s(T1195), 0) → U36_GG(T1195, quot52_in_g(T1195))
QUOT1194_IN_GG(s(T1195), 0) → QUOT52_IN_G(T1195)
QUOT1194_IN_GG(s(s(T1200)), 0) → U37_GG(T1200, quot66_in_g(T1200))
QUOT1194_IN_GG(s(s(T1200)), 0) → QUOT66_IN_G(T1200)
QUOT1194_IN_GG(s(s(T1215)), s(0)) → U38_GG(T1215, quot134_in_g(T1215))
QUOT1194_IN_GG(s(s(T1215)), s(0)) → QUOT134_IN_G(T1215)
QUOT1194_IN_GG(s(s(s(T1220))), s(0)) → U39_GG(T1220, quot161_in_g(T1220))
QUOT1194_IN_GG(s(s(s(T1220))), s(0)) → QUOT161_IN_G(T1220)
QUOT1194_IN_GG(s(s(s(T1235))), s(s(0))) → U40_GG(T1235, quot243_in_g(T1235))
QUOT1194_IN_GG(s(s(s(T1235))), s(s(0))) → QUOT243_IN_G(T1235)
QUOT1194_IN_GG(s(s(s(s(T1240)))), s(s(0))) → U41_GG(T1240, quot283_in_g(T1240))
QUOT1194_IN_GG(s(s(s(s(T1240)))), s(s(0))) → QUOT283_IN_G(T1240)
QUOT1194_IN_GG(s(s(s(s(T1255)))), s(s(s(0)))) → U42_GG(T1255, quot379_in_g(T1255))
QUOT1194_IN_GG(s(s(s(s(T1255)))), s(s(s(0)))) → QUOT379_IN_G(T1255)
QUOT1194_IN_GG(s(s(s(s(s(T1260))))), s(s(s(0)))) → U43_GG(T1260, quot432_in_g(T1260))
QUOT1194_IN_GG(s(s(s(s(s(T1260))))), s(s(s(0)))) → QUOT432_IN_G(T1260)
QUOT1194_IN_GG(s(s(s(s(s(T1275))))), s(s(s(s(0))))) → U44_GG(T1275, quot542_in_g(T1275))
QUOT1194_IN_GG(s(s(s(s(s(T1275))))), s(s(s(s(0))))) → QUOT542_IN_G(T1275)
QUOT1194_IN_GG(s(s(s(s(s(s(T1280)))))), s(s(s(s(0))))) → U45_GG(T1280, quot608_in_g(T1280))
QUOT1194_IN_GG(s(s(s(s(s(s(T1280)))))), s(s(s(s(0))))) → QUOT608_IN_G(T1280)
QUOT1194_IN_GG(s(s(s(s(s(s(T1295)))))), s(s(s(s(s(0)))))) → U46_GG(T1295, quot732_in_g(T1295))
QUOT1194_IN_GG(s(s(s(s(s(s(T1295)))))), s(s(s(s(s(0)))))) → QUOT732_IN_G(T1295)
QUOT1194_IN_GG(s(s(s(s(s(s(s(T1300))))))), s(s(s(s(s(0)))))) → U47_GG(T1300, quot811_in_g(T1300))
QUOT1194_IN_GG(s(s(s(s(s(s(s(T1300))))))), s(s(s(s(s(0)))))) → QUOT811_IN_G(T1300)
QUOT1194_IN_GG(s(s(s(s(s(s(s(T1315))))))), s(s(s(s(s(s(0))))))) → U48_GG(T1315, quot949_in_g(T1315))
QUOT1194_IN_GG(s(s(s(s(s(s(s(T1315))))))), s(s(s(s(s(s(0))))))) → QUOT949_IN_G(T1315)
QUOT1194_IN_GG(s(s(s(s(s(s(s(s(T1320)))))))), s(s(s(s(s(s(0))))))) → U49_GG(T1320, quot1041_in_g(T1320))
QUOT1194_IN_GG(s(s(s(s(s(s(s(s(T1320)))))))), s(s(s(s(s(s(0))))))) → QUOT1041_IN_G(T1320)
QUOT1194_IN_GG(s(s(s(s(s(s(s(s(T1320)))))))), s(s(s(s(s(s(s(T1326)))))))) → U50_GG(T1320, T1326, quot1405_in_ggg(T1320, T1326, s(s(s(s(s(s(s(T1326)))))))))
QUOT1194_IN_GG(s(s(s(s(s(s(s(s(T1320)))))))), s(s(s(s(s(s(s(T1326)))))))) → QUOT1405_IN_GGG(T1320, T1326, s(s(s(s(s(s(s(T1326))))))))
QUOT1405_IN_GGG(T1345, 0, T1351) → U51_GGG(T1345, T1351, quot1194_in_gg(T1345, T1351))
QUOT1405_IN_GGG(T1345, 0, T1351) → QUOT1194_IN_GG(T1345, T1351)
QUOT1405_IN_GGG(s(T1372), 0, T1378) → U52_GGG(T1372, T1378, quot1194_in_gg(T1372, T1378))
QUOT1405_IN_GGG(s(T1372), 0, T1378) → QUOT1194_IN_GG(T1372, T1378)
QUOT1405_IN_GGG(s(T1362), s(T1385), T1364) → U53_GGG(T1362, T1385, T1364, quot1405_in_ggg(T1362, T1385, T1364))
QUOT1405_IN_GGG(s(T1362), s(T1385), T1364) → QUOT1405_IN_GGG(T1362, T1385, T1364)
QUOT1175_IN_GGGA(T1161, 0, T1169, s(T1391)) → U77_GGGA(T1161, T1169, T1391, quot3_in_gga(T1161, s(T1169), T1391))
QUOT1175_IN_GGGA(T1161, 0, T1169, s(T1391)) → QUOT3_IN_GGA(T1161, s(T1169), T1391)
QUOT1175_IN_GGGA(s(T1419), 0, T1427, 0) → U78_GGGA(T1419, T1427, quot1194_in_gg(T1419, T1427))
QUOT1175_IN_GGGA(s(T1419), 0, T1427, 0) → QUOT1194_IN_GG(T1419, T1427)
QUOT1175_IN_GGGA(s(T1419), 0, T1427, s(T1433)) → U79_GGGA(T1419, T1427, T1433, quot3_in_gga(T1419, s(T1427), T1433))
QUOT1175_IN_GGGA(s(T1419), 0, T1427, s(T1433)) → QUOT3_IN_GGA(T1419, s(T1427), T1433)
QUOT1175_IN_GGGA(s(T1402), s(T1438), T1404, T1406) → U80_GGGA(T1402, T1438, T1404, T1406, quot1175_in_ggga(T1402, T1438, T1404, T1406))
QUOT1175_IN_GGGA(s(T1402), s(T1438), T1404, T1406) → QUOT1175_IN_GGGA(T1402, T1438, T1404, T1406)

R is empty.
The argument filtering Pi contains the following mapping:
quot3_in_gga(x1, x2, x3)  =  quot3_in_gga(x1, x2)
s(x1)  =  s(x1)
0  =  0
quot52_in_g(x1)  =  quot52_in_g(x1)
quot66_in_g(x1)  =  quot66_in_g(x1)
quot78_in_ga(x1, x2)  =  quot78_in_ga(x1)
quot93_in_ga(x1, x2)  =  quot93_in_ga(x1)
quot134_in_g(x1)  =  quot134_in_g(x1)
quot161_in_g(x1)  =  quot161_in_g(x1)
quot173_in_ga(x1, x2)  =  quot173_in_ga(x1)
quot202_in_ga(x1, x2)  =  quot202_in_ga(x1)
quot243_in_g(x1)  =  quot243_in_g(x1)
quot283_in_g(x1)  =  quot283_in_g(x1)
quot295_in_ga(x1, x2)  =  quot295_in_ga(x1)
quot338_in_ga(x1, x2)  =  quot338_in_ga(x1)
quot379_in_g(x1)  =  quot379_in_g(x1)
quot432_in_g(x1)  =  quot432_in_g(x1)
quot444_in_ga(x1, x2)  =  quot444_in_ga(x1)
quot501_in_ga(x1, x2)  =  quot501_in_ga(x1)
quot542_in_g(x1)  =  quot542_in_g(x1)
quot608_in_g(x1)  =  quot608_in_g(x1)
quot620_in_ga(x1, x2)  =  quot620_in_ga(x1)
quot691_in_ga(x1, x2)  =  quot691_in_ga(x1)
quot732_in_g(x1)  =  quot732_in_g(x1)
quot811_in_g(x1)  =  quot811_in_g(x1)
quot823_in_ga(x1, x2)  =  quot823_in_ga(x1)
quot908_in_ga(x1, x2)  =  quot908_in_ga(x1)
quot949_in_g(x1)  =  quot949_in_g(x1)
quot1041_in_g(x1)  =  quot1041_in_g(x1)
quot1053_in_ga(x1, x2)  =  quot1053_in_ga(x1)
quot1152_in_ga(x1, x2)  =  quot1152_in_ga(x1)
quot1175_in_ggga(x1, x2, x3, x4)  =  quot1175_in_ggga(x1, x2, x3)
quot1194_in_gg(x1, x2)  =  quot1194_in_gg(x1, x2)
quot1405_in_ggg(x1, x2, x3)  =  quot1405_in_ggg(x1, x2, x3)
DIV1_IN_GGA(x1, x2, x3)  =  DIV1_IN_GGA(x1, x2)
U81_GGA(x1, x2, x3, x4)  =  U81_GGA(x1, x2, x4)
QUOT3_IN_GGA(x1, x2, x3)  =  QUOT3_IN_GGA(x1, x2)
U54_GGA(x1, x2)  =  U54_GGA(x1, x2)
QUOT52_IN_G(x1)  =  QUOT52_IN_G(x1)
U1_G(x1, x2)  =  U1_G(x1, x2)
QUOT66_IN_G(x1)  =  QUOT66_IN_G(x1)
U29_G(x1, x2)  =  U29_G(x1, x2)
U55_GGA(x1, x2, x3)  =  U55_GGA(x1, x3)
QUOT78_IN_GA(x1, x2)  =  QUOT78_IN_GA(x1)
U2_GA(x1, x2, x3)  =  U2_GA(x1, x3)
QUOT93_IN_GA(x1, x2)  =  QUOT93_IN_GA(x1)
U3_GA(x1, x2)  =  U3_GA(x1, x2)
U4_GA(x1, x2, x3)  =  U4_GA(x1, x3)
U56_GGA(x1, x2, x3)  =  U56_GGA(x1, x3)
U57_GGA(x1, x2)  =  U57_GGA(x1, x2)
QUOT134_IN_G(x1)  =  QUOT134_IN_G(x1)
U5_G(x1, x2)  =  U5_G(x1, x2)
QUOT161_IN_G(x1)  =  QUOT161_IN_G(x1)
U30_G(x1, x2)  =  U30_G(x1, x2)
U58_GGA(x1, x2, x3)  =  U58_GGA(x1, x3)
QUOT173_IN_GA(x1, x2)  =  QUOT173_IN_GA(x1)
U6_GA(x1, x2, x3)  =  U6_GA(x1, x3)
QUOT202_IN_GA(x1, x2)  =  QUOT202_IN_GA(x1)
U7_GA(x1, x2)  =  U7_GA(x1, x2)
U8_GA(x1, x2, x3)  =  U8_GA(x1, x3)
U59_GGA(x1, x2, x3)  =  U59_GGA(x1, x3)
U60_GGA(x1, x2)  =  U60_GGA(x1, x2)
QUOT243_IN_G(x1)  =  QUOT243_IN_G(x1)
U9_G(x1, x2)  =  U9_G(x1, x2)
QUOT283_IN_G(x1)  =  QUOT283_IN_G(x1)
U31_G(x1, x2)  =  U31_G(x1, x2)
U61_GGA(x1, x2, x3)  =  U61_GGA(x1, x3)
QUOT295_IN_GA(x1, x2)  =  QUOT295_IN_GA(x1)
U10_GA(x1, x2, x3)  =  U10_GA(x1, x3)
QUOT338_IN_GA(x1, x2)  =  QUOT338_IN_GA(x1)
U11_GA(x1, x2)  =  U11_GA(x1, x2)
U12_GA(x1, x2, x3)  =  U12_GA(x1, x3)
U62_GGA(x1, x2, x3)  =  U62_GGA(x1, x3)
U63_GGA(x1, x2)  =  U63_GGA(x1, x2)
QUOT379_IN_G(x1)  =  QUOT379_IN_G(x1)
U13_G(x1, x2)  =  U13_G(x1, x2)
QUOT432_IN_G(x1)  =  QUOT432_IN_G(x1)
U32_G(x1, x2)  =  U32_G(x1, x2)
U64_GGA(x1, x2, x3)  =  U64_GGA(x1, x3)
QUOT444_IN_GA(x1, x2)  =  QUOT444_IN_GA(x1)
U14_GA(x1, x2, x3)  =  U14_GA(x1, x3)
QUOT501_IN_GA(x1, x2)  =  QUOT501_IN_GA(x1)
U15_GA(x1, x2)  =  U15_GA(x1, x2)
U16_GA(x1, x2, x3)  =  U16_GA(x1, x3)
U65_GGA(x1, x2, x3)  =  U65_GGA(x1, x3)
U66_GGA(x1, x2)  =  U66_GGA(x1, x2)
QUOT542_IN_G(x1)  =  QUOT542_IN_G(x1)
U17_G(x1, x2)  =  U17_G(x1, x2)
QUOT608_IN_G(x1)  =  QUOT608_IN_G(x1)
U33_G(x1, x2)  =  U33_G(x1, x2)
U67_GGA(x1, x2, x3)  =  U67_GGA(x1, x3)
QUOT620_IN_GA(x1, x2)  =  QUOT620_IN_GA(x1)
U18_GA(x1, x2, x3)  =  U18_GA(x1, x3)
QUOT691_IN_GA(x1, x2)  =  QUOT691_IN_GA(x1)
U19_GA(x1, x2)  =  U19_GA(x1, x2)
U20_GA(x1, x2, x3)  =  U20_GA(x1, x3)
U68_GGA(x1, x2, x3)  =  U68_GGA(x1, x3)
U69_GGA(x1, x2)  =  U69_GGA(x1, x2)
QUOT732_IN_G(x1)  =  QUOT732_IN_G(x1)
U21_G(x1, x2)  =  U21_G(x1, x2)
QUOT811_IN_G(x1)  =  QUOT811_IN_G(x1)
U34_G(x1, x2)  =  U34_G(x1, x2)
U70_GGA(x1, x2, x3)  =  U70_GGA(x1, x3)
QUOT823_IN_GA(x1, x2)  =  QUOT823_IN_GA(x1)
U22_GA(x1, x2, x3)  =  U22_GA(x1, x3)
QUOT908_IN_GA(x1, x2)  =  QUOT908_IN_GA(x1)
U23_GA(x1, x2)  =  U23_GA(x1, x2)
U24_GA(x1, x2, x3)  =  U24_GA(x1, x3)
U71_GGA(x1, x2, x3)  =  U71_GGA(x1, x3)
U72_GGA(x1, x2)  =  U72_GGA(x1, x2)
QUOT949_IN_G(x1)  =  QUOT949_IN_G(x1)
U25_G(x1, x2)  =  U25_G(x1, x2)
QUOT1041_IN_G(x1)  =  QUOT1041_IN_G(x1)
U35_G(x1, x2)  =  U35_G(x1, x2)
U73_GGA(x1, x2, x3)  =  U73_GGA(x1, x3)
QUOT1053_IN_GA(x1, x2)  =  QUOT1053_IN_GA(x1)
U26_GA(x1, x2, x3)  =  U26_GA(x1, x3)
QUOT1152_IN_GA(x1, x2)  =  QUOT1152_IN_GA(x1)
U27_GA(x1, x2)  =  U27_GA(x1, x2)
U28_GA(x1, x2, x3)  =  U28_GA(x1, x3)
U74_GGA(x1, x2, x3)  =  U74_GGA(x1, x3)
U75_GGA(x1, x2, x3, x4)  =  U75_GGA(x1, x2, x4)
QUOT1175_IN_GGGA(x1, x2, x3, x4)  =  QUOT1175_IN_GGGA(x1, x2, x3)
U76_GGGA(x1, x2, x3)  =  U76_GGGA(x1, x2, x3)
QUOT1194_IN_GG(x1, x2)  =  QUOT1194_IN_GG(x1, x2)
U36_GG(x1, x2)  =  U36_GG(x1, x2)
U37_GG(x1, x2)  =  U37_GG(x1, x2)
U38_GG(x1, x2)  =  U38_GG(x1, x2)
U39_GG(x1, x2)  =  U39_GG(x1, x2)
U40_GG(x1, x2)  =  U40_GG(x1, x2)
U41_GG(x1, x2)  =  U41_GG(x1, x2)
U42_GG(x1, x2)  =  U42_GG(x1, x2)
U43_GG(x1, x2)  =  U43_GG(x1, x2)
U44_GG(x1, x2)  =  U44_GG(x1, x2)
U45_GG(x1, x2)  =  U45_GG(x1, x2)
U46_GG(x1, x2)  =  U46_GG(x1, x2)
U47_GG(x1, x2)  =  U47_GG(x1, x2)
U48_GG(x1, x2)  =  U48_GG(x1, x2)
U49_GG(x1, x2)  =  U49_GG(x1, x2)
U50_GG(x1, x2, x3)  =  U50_GG(x1, x2, x3)
QUOT1405_IN_GGG(x1, x2, x3)  =  QUOT1405_IN_GGG(x1, x2, x3)
U51_GGG(x1, x2, x3)  =  U51_GGG(x1, x2, x3)
U52_GGG(x1, x2, x3)  =  U52_GGG(x1, x2, x3)
U53_GGG(x1, x2, x3, x4)  =  U53_GGG(x1, x2, x3, x4)
U77_GGGA(x1, x2, x3, x4)  =  U77_GGGA(x1, x2, x4)
U78_GGGA(x1, x2, x3)  =  U78_GGGA(x1, x2, x3)
U79_GGGA(x1, x2, x3, x4)  =  U79_GGGA(x1, x2, x4)
U80_GGGA(x1, x2, x3, x4, x5)  =  U80_GGGA(x1, x2, x3, x5)

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

Infinitary Constructor Rewriting Termination of PiDP implies Termination of TRIPLES

(4) Obligation:

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

DIV1_IN_GGA(T7, T8, T10) → U81_GGA(T7, T8, T10, quot3_in_gga(T7, T8, T10))
DIV1_IN_GGA(T7, T8, T10) → QUOT3_IN_GGA(T7, T8, T10)
QUOT3_IN_GGA(s(T79), s(0), 0) → U54_GGA(T79, quot52_in_g(T79))
QUOT3_IN_GGA(s(T79), s(0), 0) → QUOT52_IN_G(T79)
QUOT52_IN_G(s(T85)) → U1_G(T85, quot66_in_g(T85))
QUOT52_IN_G(s(T85)) → QUOT66_IN_G(T85)
QUOT66_IN_G(T90) → U29_G(T90, quot52_in_g(T90))
QUOT66_IN_G(T90) → QUOT52_IN_G(T90)
QUOT3_IN_GGA(s(T79), s(0), s(T94)) → U55_GGA(T79, T94, quot78_in_ga(T79, T94))
QUOT3_IN_GGA(s(T79), s(0), s(T94)) → QUOT78_IN_GA(T79, T94)
QUOT78_IN_GA(s(T108), T110) → U2_GA(T108, T110, quot93_in_ga(T108, T110))
QUOT78_IN_GA(s(T108), T110) → QUOT93_IN_GA(T108, T110)
QUOT93_IN_GA(T121, 0) → U3_GA(T121, quot52_in_g(T121))
QUOT93_IN_GA(T121, 0) → QUOT52_IN_G(T121)
QUOT93_IN_GA(T121, s(T127)) → U4_GA(T121, T127, quot78_in_ga(T121, T127))
QUOT93_IN_GA(T121, s(T127)) → QUOT78_IN_GA(T121, T127)
QUOT3_IN_GGA(s(s(T135)), s(0), T138) → U56_GGA(T135, T138, quot93_in_ga(T135, T138))
QUOT3_IN_GGA(s(s(T135)), s(0), T138) → QUOT93_IN_GA(T135, T138)
QUOT3_IN_GGA(s(s(T166)), s(s(0)), 0) → U57_GGA(T166, quot134_in_g(T166))
QUOT3_IN_GGA(s(s(T166)), s(s(0)), 0) → QUOT134_IN_G(T166)
QUOT134_IN_G(s(s(T176))) → U5_G(T176, quot161_in_g(T176))
QUOT134_IN_G(s(s(T176))) → QUOT161_IN_G(T176)
QUOT161_IN_G(T181) → U30_G(T181, quot134_in_g(T181))
QUOT161_IN_G(T181) → QUOT134_IN_G(T181)
QUOT3_IN_GGA(s(s(T166)), s(s(0)), s(T185)) → U58_GGA(T166, T185, quot173_in_ga(T166, T185))
QUOT3_IN_GGA(s(s(T166)), s(s(0)), s(T185)) → QUOT173_IN_GA(T166, T185)
QUOT173_IN_GA(s(s(T217)), T219) → U6_GA(T217, T219, quot202_in_ga(T217, T219))
QUOT173_IN_GA(s(s(T217)), T219) → QUOT202_IN_GA(T217, T219)
QUOT202_IN_GA(T230, 0) → U7_GA(T230, quot134_in_g(T230))
QUOT202_IN_GA(T230, 0) → QUOT134_IN_G(T230)
QUOT202_IN_GA(T230, s(T236)) → U8_GA(T230, T236, quot173_in_ga(T230, T236))
QUOT202_IN_GA(T230, s(T236)) → QUOT173_IN_GA(T230, T236)
QUOT3_IN_GGA(s(s(s(T244))), s(s(0)), T247) → U59_GGA(T244, T247, quot202_in_ga(T244, T247))
QUOT3_IN_GGA(s(s(s(T244))), s(s(0)), T247) → QUOT202_IN_GA(T244, T247)
QUOT3_IN_GGA(s(s(s(T275))), s(s(s(0))), 0) → U60_GGA(T275, quot243_in_g(T275))
QUOT3_IN_GGA(s(s(s(T275))), s(s(s(0))), 0) → QUOT243_IN_G(T275)
QUOT243_IN_G(s(s(s(T289)))) → U9_G(T289, quot283_in_g(T289))
QUOT243_IN_G(s(s(s(T289)))) → QUOT283_IN_G(T289)
QUOT283_IN_G(T294) → U31_G(T294, quot243_in_g(T294))
QUOT283_IN_G(T294) → QUOT243_IN_G(T294)
QUOT3_IN_GGA(s(s(s(T275))), s(s(s(0))), s(T298)) → U61_GGA(T275, T298, quot295_in_ga(T275, T298))
QUOT3_IN_GGA(s(s(s(T275))), s(s(s(0))), s(T298)) → QUOT295_IN_GA(T275, T298)
QUOT295_IN_GA(s(s(s(T348))), T350) → U10_GA(T348, T350, quot338_in_ga(T348, T350))
QUOT295_IN_GA(s(s(s(T348))), T350) → QUOT338_IN_GA(T348, T350)
QUOT338_IN_GA(T361, 0) → U11_GA(T361, quot243_in_g(T361))
QUOT338_IN_GA(T361, 0) → QUOT243_IN_G(T361)
QUOT338_IN_GA(T361, s(T367)) → U12_GA(T361, T367, quot295_in_ga(T361, T367))
QUOT338_IN_GA(T361, s(T367)) → QUOT295_IN_GA(T361, T367)
QUOT3_IN_GGA(s(s(s(s(T375)))), s(s(s(0))), T378) → U62_GGA(T375, T378, quot338_in_ga(T375, T378))
QUOT3_IN_GGA(s(s(s(s(T375)))), s(s(s(0))), T378) → QUOT338_IN_GA(T375, T378)
QUOT3_IN_GGA(s(s(s(s(T406)))), s(s(s(s(0)))), 0) → U63_GGA(T406, quot379_in_g(T406))
QUOT3_IN_GGA(s(s(s(s(T406)))), s(s(s(s(0)))), 0) → QUOT379_IN_G(T406)
QUOT379_IN_G(s(s(s(s(T424))))) → U13_G(T424, quot432_in_g(T424))
QUOT379_IN_G(s(s(s(s(T424))))) → QUOT432_IN_G(T424)
QUOT432_IN_G(T429) → U32_G(T429, quot379_in_g(T429))
QUOT432_IN_G(T429) → QUOT379_IN_G(T429)
QUOT3_IN_GGA(s(s(s(s(T406)))), s(s(s(s(0)))), s(T433)) → U64_GGA(T406, T433, quot444_in_ga(T406, T433))
QUOT3_IN_GGA(s(s(s(s(T406)))), s(s(s(s(0)))), s(T433)) → QUOT444_IN_GA(T406, T433)
QUOT444_IN_GA(s(s(s(s(T501)))), T503) → U14_GA(T501, T503, quot501_in_ga(T501, T503))
QUOT444_IN_GA(s(s(s(s(T501)))), T503) → QUOT501_IN_GA(T501, T503)
QUOT501_IN_GA(T514, 0) → U15_GA(T514, quot379_in_g(T514))
QUOT501_IN_GA(T514, 0) → QUOT379_IN_G(T514)
QUOT501_IN_GA(T514, s(T520)) → U16_GA(T514, T520, quot444_in_ga(T514, T520))
QUOT501_IN_GA(T514, s(T520)) → QUOT444_IN_GA(T514, T520)
QUOT3_IN_GGA(s(s(s(s(s(T528))))), s(s(s(s(0)))), T531) → U65_GGA(T528, T531, quot501_in_ga(T528, T531))
QUOT3_IN_GGA(s(s(s(s(s(T528))))), s(s(s(s(0)))), T531) → QUOT501_IN_GA(T528, T531)
QUOT3_IN_GGA(s(s(s(s(s(T559))))), s(s(s(s(s(0))))), 0) → U66_GGA(T559, quot542_in_g(T559))
QUOT3_IN_GGA(s(s(s(s(s(T559))))), s(s(s(s(s(0))))), 0) → QUOT542_IN_G(T559)
QUOT542_IN_G(s(s(s(s(s(T581)))))) → U17_G(T581, quot608_in_g(T581))
QUOT542_IN_G(s(s(s(s(s(T581)))))) → QUOT608_IN_G(T581)
QUOT608_IN_G(T586) → U33_G(T586, quot542_in_g(T586))
QUOT608_IN_G(T586) → QUOT542_IN_G(T586)
QUOT3_IN_GGA(s(s(s(s(s(T559))))), s(s(s(s(s(0))))), s(T590)) → U67_GGA(T559, T590, quot620_in_ga(T559, T590))
QUOT3_IN_GGA(s(s(s(s(s(T559))))), s(s(s(s(s(0))))), s(T590)) → QUOT620_IN_GA(T559, T590)
QUOT620_IN_GA(s(s(s(s(s(T676))))), T678) → U18_GA(T676, T678, quot691_in_ga(T676, T678))
QUOT620_IN_GA(s(s(s(s(s(T676))))), T678) → QUOT691_IN_GA(T676, T678)
QUOT691_IN_GA(T689, 0) → U19_GA(T689, quot542_in_g(T689))
QUOT691_IN_GA(T689, 0) → QUOT542_IN_G(T689)
QUOT691_IN_GA(T689, s(T695)) → U20_GA(T689, T695, quot620_in_ga(T689, T695))
QUOT691_IN_GA(T689, s(T695)) → QUOT620_IN_GA(T689, T695)
QUOT3_IN_GGA(s(s(s(s(s(s(T703)))))), s(s(s(s(s(0))))), T706) → U68_GGA(T703, T706, quot691_in_ga(T703, T706))
QUOT3_IN_GGA(s(s(s(s(s(s(T703)))))), s(s(s(s(s(0))))), T706) → QUOT691_IN_GA(T703, T706)
QUOT3_IN_GGA(s(s(s(s(s(s(T734)))))), s(s(s(s(s(s(0)))))), 0) → U69_GGA(T734, quot732_in_g(T734))
QUOT3_IN_GGA(s(s(s(s(s(s(T734)))))), s(s(s(s(s(s(0)))))), 0) → QUOT732_IN_G(T734)
QUOT732_IN_G(s(s(s(s(s(s(T760))))))) → U21_G(T760, quot811_in_g(T760))
QUOT732_IN_G(s(s(s(s(s(s(T760))))))) → QUOT811_IN_G(T760)
QUOT811_IN_G(T765) → U34_G(T765, quot732_in_g(T765))
QUOT811_IN_G(T765) → QUOT732_IN_G(T765)
QUOT3_IN_GGA(s(s(s(s(s(s(T734)))))), s(s(s(s(s(s(0)))))), s(T769)) → U70_GGA(T734, T769, quot823_in_ga(T734, T769))
QUOT3_IN_GGA(s(s(s(s(s(s(T734)))))), s(s(s(s(s(s(0)))))), s(T769)) → QUOT823_IN_GA(T734, T769)
QUOT823_IN_GA(s(s(s(s(s(s(T873)))))), T875) → U22_GA(T873, T875, quot908_in_ga(T873, T875))
QUOT823_IN_GA(s(s(s(s(s(s(T873)))))), T875) → QUOT908_IN_GA(T873, T875)
QUOT908_IN_GA(T886, 0) → U23_GA(T886, quot732_in_g(T886))
QUOT908_IN_GA(T886, 0) → QUOT732_IN_G(T886)
QUOT908_IN_GA(T886, s(T892)) → U24_GA(T886, T892, quot823_in_ga(T886, T892))
QUOT908_IN_GA(T886, s(T892)) → QUOT823_IN_GA(T886, T892)
QUOT3_IN_GGA(s(s(s(s(s(s(s(T900))))))), s(s(s(s(s(s(0)))))), T903) → U71_GGA(T900, T903, quot908_in_ga(T900, T903))
QUOT3_IN_GGA(s(s(s(s(s(s(s(T900))))))), s(s(s(s(s(s(0)))))), T903) → QUOT908_IN_GA(T900, T903)
QUOT3_IN_GGA(s(s(s(s(s(s(s(T931))))))), s(s(s(s(s(s(s(0))))))), 0) → U72_GGA(T931, quot949_in_g(T931))
QUOT3_IN_GGA(s(s(s(s(s(s(s(T931))))))), s(s(s(s(s(s(s(0))))))), 0) → QUOT949_IN_G(T931)
QUOT949_IN_G(s(s(s(s(s(s(s(T961)))))))) → U25_G(T961, quot1041_in_g(T961))
QUOT949_IN_G(s(s(s(s(s(s(s(T961)))))))) → QUOT1041_IN_G(T961)
QUOT1041_IN_G(T966) → U35_G(T966, quot949_in_g(T966))
QUOT1041_IN_G(T966) → QUOT949_IN_G(T966)
QUOT3_IN_GGA(s(s(s(s(s(s(s(T931))))))), s(s(s(s(s(s(s(0))))))), s(T970)) → U73_GGA(T931, T970, quot1053_in_ga(T931, T970))
QUOT3_IN_GGA(s(s(s(s(s(s(s(T931))))))), s(s(s(s(s(s(s(0))))))), s(T970)) → QUOT1053_IN_GA(T931, T970)
QUOT1053_IN_GA(s(s(s(s(s(s(s(T1092))))))), T1094) → U26_GA(T1092, T1094, quot1152_in_ga(T1092, T1094))
QUOT1053_IN_GA(s(s(s(s(s(s(s(T1092))))))), T1094) → QUOT1152_IN_GA(T1092, T1094)
QUOT1152_IN_GA(T1105, 0) → U27_GA(T1105, quot949_in_g(T1105))
QUOT1152_IN_GA(T1105, 0) → QUOT949_IN_G(T1105)
QUOT1152_IN_GA(T1105, s(T1111)) → U28_GA(T1105, T1111, quot1053_in_ga(T1105, T1111))
QUOT1152_IN_GA(T1105, s(T1111)) → QUOT1053_IN_GA(T1105, T1111)
QUOT3_IN_GGA(s(s(s(s(s(s(s(s(T1119)))))))), s(s(s(s(s(s(s(0))))))), T1122) → U74_GGA(T1119, T1122, quot1152_in_ga(T1119, T1122))
QUOT3_IN_GGA(s(s(s(s(s(s(s(s(T1119)))))))), s(s(s(s(s(s(s(0))))))), T1122) → QUOT1152_IN_GA(T1119, T1122)
QUOT3_IN_GGA(s(s(s(s(s(s(s(s(T1119)))))))), s(s(s(s(s(s(s(s(T1129)))))))), T1122) → U75_GGA(T1119, T1129, T1122, quot1175_in_ggga(T1119, T1129, s(s(s(s(s(s(s(T1129))))))), T1122))
QUOT3_IN_GGA(s(s(s(s(s(s(s(s(T1119)))))))), s(s(s(s(s(s(s(s(T1129)))))))), T1122) → QUOT1175_IN_GGGA(T1119, T1129, s(s(s(s(s(s(s(T1129))))))), T1122)
QUOT1175_IN_GGGA(T1161, 0, T1169, 0) → U76_GGGA(T1161, T1169, quot1194_in_gg(T1161, T1169))
QUOT1175_IN_GGGA(T1161, 0, T1169, 0) → QUOT1194_IN_GG(T1161, T1169)
QUOT1194_IN_GG(s(T1195), 0) → U36_GG(T1195, quot52_in_g(T1195))
QUOT1194_IN_GG(s(T1195), 0) → QUOT52_IN_G(T1195)
QUOT1194_IN_GG(s(s(T1200)), 0) → U37_GG(T1200, quot66_in_g(T1200))
QUOT1194_IN_GG(s(s(T1200)), 0) → QUOT66_IN_G(T1200)
QUOT1194_IN_GG(s(s(T1215)), s(0)) → U38_GG(T1215, quot134_in_g(T1215))
QUOT1194_IN_GG(s(s(T1215)), s(0)) → QUOT134_IN_G(T1215)
QUOT1194_IN_GG(s(s(s(T1220))), s(0)) → U39_GG(T1220, quot161_in_g(T1220))
QUOT1194_IN_GG(s(s(s(T1220))), s(0)) → QUOT161_IN_G(T1220)
QUOT1194_IN_GG(s(s(s(T1235))), s(s(0))) → U40_GG(T1235, quot243_in_g(T1235))
QUOT1194_IN_GG(s(s(s(T1235))), s(s(0))) → QUOT243_IN_G(T1235)
QUOT1194_IN_GG(s(s(s(s(T1240)))), s(s(0))) → U41_GG(T1240, quot283_in_g(T1240))
QUOT1194_IN_GG(s(s(s(s(T1240)))), s(s(0))) → QUOT283_IN_G(T1240)
QUOT1194_IN_GG(s(s(s(s(T1255)))), s(s(s(0)))) → U42_GG(T1255, quot379_in_g(T1255))
QUOT1194_IN_GG(s(s(s(s(T1255)))), s(s(s(0)))) → QUOT379_IN_G(T1255)
QUOT1194_IN_GG(s(s(s(s(s(T1260))))), s(s(s(0)))) → U43_GG(T1260, quot432_in_g(T1260))
QUOT1194_IN_GG(s(s(s(s(s(T1260))))), s(s(s(0)))) → QUOT432_IN_G(T1260)
QUOT1194_IN_GG(s(s(s(s(s(T1275))))), s(s(s(s(0))))) → U44_GG(T1275, quot542_in_g(T1275))
QUOT1194_IN_GG(s(s(s(s(s(T1275))))), s(s(s(s(0))))) → QUOT542_IN_G(T1275)
QUOT1194_IN_GG(s(s(s(s(s(s(T1280)))))), s(s(s(s(0))))) → U45_GG(T1280, quot608_in_g(T1280))
QUOT1194_IN_GG(s(s(s(s(s(s(T1280)))))), s(s(s(s(0))))) → QUOT608_IN_G(T1280)
QUOT1194_IN_GG(s(s(s(s(s(s(T1295)))))), s(s(s(s(s(0)))))) → U46_GG(T1295, quot732_in_g(T1295))
QUOT1194_IN_GG(s(s(s(s(s(s(T1295)))))), s(s(s(s(s(0)))))) → QUOT732_IN_G(T1295)
QUOT1194_IN_GG(s(s(s(s(s(s(s(T1300))))))), s(s(s(s(s(0)))))) → U47_GG(T1300, quot811_in_g(T1300))
QUOT1194_IN_GG(s(s(s(s(s(s(s(T1300))))))), s(s(s(s(s(0)))))) → QUOT811_IN_G(T1300)
QUOT1194_IN_GG(s(s(s(s(s(s(s(T1315))))))), s(s(s(s(s(s(0))))))) → U48_GG(T1315, quot949_in_g(T1315))
QUOT1194_IN_GG(s(s(s(s(s(s(s(T1315))))))), s(s(s(s(s(s(0))))))) → QUOT949_IN_G(T1315)
QUOT1194_IN_GG(s(s(s(s(s(s(s(s(T1320)))))))), s(s(s(s(s(s(0))))))) → U49_GG(T1320, quot1041_in_g(T1320))
QUOT1194_IN_GG(s(s(s(s(s(s(s(s(T1320)))))))), s(s(s(s(s(s(0))))))) → QUOT1041_IN_G(T1320)
QUOT1194_IN_GG(s(s(s(s(s(s(s(s(T1320)))))))), s(s(s(s(s(s(s(T1326)))))))) → U50_GG(T1320, T1326, quot1405_in_ggg(T1320, T1326, s(s(s(s(s(s(s(T1326)))))))))
QUOT1194_IN_GG(s(s(s(s(s(s(s(s(T1320)))))))), s(s(s(s(s(s(s(T1326)))))))) → QUOT1405_IN_GGG(T1320, T1326, s(s(s(s(s(s(s(T1326))))))))
QUOT1405_IN_GGG(T1345, 0, T1351) → U51_GGG(T1345, T1351, quot1194_in_gg(T1345, T1351))
QUOT1405_IN_GGG(T1345, 0, T1351) → QUOT1194_IN_GG(T1345, T1351)
QUOT1405_IN_GGG(s(T1372), 0, T1378) → U52_GGG(T1372, T1378, quot1194_in_gg(T1372, T1378))
QUOT1405_IN_GGG(s(T1372), 0, T1378) → QUOT1194_IN_GG(T1372, T1378)
QUOT1405_IN_GGG(s(T1362), s(T1385), T1364) → U53_GGG(T1362, T1385, T1364, quot1405_in_ggg(T1362, T1385, T1364))
QUOT1405_IN_GGG(s(T1362), s(T1385), T1364) → QUOT1405_IN_GGG(T1362, T1385, T1364)
QUOT1175_IN_GGGA(T1161, 0, T1169, s(T1391)) → U77_GGGA(T1161, T1169, T1391, quot3_in_gga(T1161, s(T1169), T1391))
QUOT1175_IN_GGGA(T1161, 0, T1169, s(T1391)) → QUOT3_IN_GGA(T1161, s(T1169), T1391)
QUOT1175_IN_GGGA(s(T1419), 0, T1427, 0) → U78_GGGA(T1419, T1427, quot1194_in_gg(T1419, T1427))
QUOT1175_IN_GGGA(s(T1419), 0, T1427, 0) → QUOT1194_IN_GG(T1419, T1427)
QUOT1175_IN_GGGA(s(T1419), 0, T1427, s(T1433)) → U79_GGGA(T1419, T1427, T1433, quot3_in_gga(T1419, s(T1427), T1433))
QUOT1175_IN_GGGA(s(T1419), 0, T1427, s(T1433)) → QUOT3_IN_GGA(T1419, s(T1427), T1433)
QUOT1175_IN_GGGA(s(T1402), s(T1438), T1404, T1406) → U80_GGGA(T1402, T1438, T1404, T1406, quot1175_in_ggga(T1402, T1438, T1404, T1406))
QUOT1175_IN_GGGA(s(T1402), s(T1438), T1404, T1406) → QUOT1175_IN_GGGA(T1402, T1438, T1404, T1406)

R is empty.
The argument filtering Pi contains the following mapping:
quot3_in_gga(x1, x2, x3)  =  quot3_in_gga(x1, x2)
s(x1)  =  s(x1)
0  =  0
quot52_in_g(x1)  =  quot52_in_g(x1)
quot66_in_g(x1)  =  quot66_in_g(x1)
quot78_in_ga(x1, x2)  =  quot78_in_ga(x1)
quot93_in_ga(x1, x2)  =  quot93_in_ga(x1)
quot134_in_g(x1)  =  quot134_in_g(x1)
quot161_in_g(x1)  =  quot161_in_g(x1)
quot173_in_ga(x1, x2)  =  quot173_in_ga(x1)
quot202_in_ga(x1, x2)  =  quot202_in_ga(x1)
quot243_in_g(x1)  =  quot243_in_g(x1)
quot283_in_g(x1)  =  quot283_in_g(x1)
quot295_in_ga(x1, x2)  =  quot295_in_ga(x1)
quot338_in_ga(x1, x2)  =  quot338_in_ga(x1)
quot379_in_g(x1)  =  quot379_in_g(x1)
quot432_in_g(x1)  =  quot432_in_g(x1)
quot444_in_ga(x1, x2)  =  quot444_in_ga(x1)
quot501_in_ga(x1, x2)  =  quot501_in_ga(x1)
quot542_in_g(x1)  =  quot542_in_g(x1)
quot608_in_g(x1)  =  quot608_in_g(x1)
quot620_in_ga(x1, x2)  =  quot620_in_ga(x1)
quot691_in_ga(x1, x2)  =  quot691_in_ga(x1)
quot732_in_g(x1)  =  quot732_in_g(x1)
quot811_in_g(x1)  =  quot811_in_g(x1)
quot823_in_ga(x1, x2)  =  quot823_in_ga(x1)
quot908_in_ga(x1, x2)  =  quot908_in_ga(x1)
quot949_in_g(x1)  =  quot949_in_g(x1)
quot1041_in_g(x1)  =  quot1041_in_g(x1)
quot1053_in_ga(x1, x2)  =  quot1053_in_ga(x1)
quot1152_in_ga(x1, x2)  =  quot1152_in_ga(x1)
quot1175_in_ggga(x1, x2, x3, x4)  =  quot1175_in_ggga(x1, x2, x3)
quot1194_in_gg(x1, x2)  =  quot1194_in_gg(x1, x2)
quot1405_in_ggg(x1, x2, x3)  =  quot1405_in_ggg(x1, x2, x3)
DIV1_IN_GGA(x1, x2, x3)  =  DIV1_IN_GGA(x1, x2)
U81_GGA(x1, x2, x3, x4)  =  U81_GGA(x1, x2, x4)
QUOT3_IN_GGA(x1, x2, x3)  =  QUOT3_IN_GGA(x1, x2)
U54_GGA(x1, x2)  =  U54_GGA(x1, x2)
QUOT52_IN_G(x1)  =  QUOT52_IN_G(x1)
U1_G(x1, x2)  =  U1_G(x1, x2)
QUOT66_IN_G(x1)  =  QUOT66_IN_G(x1)
U29_G(x1, x2)  =  U29_G(x1, x2)
U55_GGA(x1, x2, x3)  =  U55_GGA(x1, x3)
QUOT78_IN_GA(x1, x2)  =  QUOT78_IN_GA(x1)
U2_GA(x1, x2, x3)  =  U2_GA(x1, x3)
QUOT93_IN_GA(x1, x2)  =  QUOT93_IN_GA(x1)
U3_GA(x1, x2)  =  U3_GA(x1, x2)
U4_GA(x1, x2, x3)  =  U4_GA(x1, x3)
U56_GGA(x1, x2, x3)  =  U56_GGA(x1, x3)
U57_GGA(x1, x2)  =  U57_GGA(x1, x2)
QUOT134_IN_G(x1)  =  QUOT134_IN_G(x1)
U5_G(x1, x2)  =  U5_G(x1, x2)
QUOT161_IN_G(x1)  =  QUOT161_IN_G(x1)
U30_G(x1, x2)  =  U30_G(x1, x2)
U58_GGA(x1, x2, x3)  =  U58_GGA(x1, x3)
QUOT173_IN_GA(x1, x2)  =  QUOT173_IN_GA(x1)
U6_GA(x1, x2, x3)  =  U6_GA(x1, x3)
QUOT202_IN_GA(x1, x2)  =  QUOT202_IN_GA(x1)
U7_GA(x1, x2)  =  U7_GA(x1, x2)
U8_GA(x1, x2, x3)  =  U8_GA(x1, x3)
U59_GGA(x1, x2, x3)  =  U59_GGA(x1, x3)
U60_GGA(x1, x2)  =  U60_GGA(x1, x2)
QUOT243_IN_G(x1)  =  QUOT243_IN_G(x1)
U9_G(x1, x2)  =  U9_G(x1, x2)
QUOT283_IN_G(x1)  =  QUOT283_IN_G(x1)
U31_G(x1, x2)  =  U31_G(x1, x2)
U61_GGA(x1, x2, x3)  =  U61_GGA(x1, x3)
QUOT295_IN_GA(x1, x2)  =  QUOT295_IN_GA(x1)
U10_GA(x1, x2, x3)  =  U10_GA(x1, x3)
QUOT338_IN_GA(x1, x2)  =  QUOT338_IN_GA(x1)
U11_GA(x1, x2)  =  U11_GA(x1, x2)
U12_GA(x1, x2, x3)  =  U12_GA(x1, x3)
U62_GGA(x1, x2, x3)  =  U62_GGA(x1, x3)
U63_GGA(x1, x2)  =  U63_GGA(x1, x2)
QUOT379_IN_G(x1)  =  QUOT379_IN_G(x1)
U13_G(x1, x2)  =  U13_G(x1, x2)
QUOT432_IN_G(x1)  =  QUOT432_IN_G(x1)
U32_G(x1, x2)  =  U32_G(x1, x2)
U64_GGA(x1, x2, x3)  =  U64_GGA(x1, x3)
QUOT444_IN_GA(x1, x2)  =  QUOT444_IN_GA(x1)
U14_GA(x1, x2, x3)  =  U14_GA(x1, x3)
QUOT501_IN_GA(x1, x2)  =  QUOT501_IN_GA(x1)
U15_GA(x1, x2)  =  U15_GA(x1, x2)
U16_GA(x1, x2, x3)  =  U16_GA(x1, x3)
U65_GGA(x1, x2, x3)  =  U65_GGA(x1, x3)
U66_GGA(x1, x2)  =  U66_GGA(x1, x2)
QUOT542_IN_G(x1)  =  QUOT542_IN_G(x1)
U17_G(x1, x2)  =  U17_G(x1, x2)
QUOT608_IN_G(x1)  =  QUOT608_IN_G(x1)
U33_G(x1, x2)  =  U33_G(x1, x2)
U67_GGA(x1, x2, x3)  =  U67_GGA(x1, x3)
QUOT620_IN_GA(x1, x2)  =  QUOT620_IN_GA(x1)
U18_GA(x1, x2, x3)  =  U18_GA(x1, x3)
QUOT691_IN_GA(x1, x2)  =  QUOT691_IN_GA(x1)
U19_GA(x1, x2)  =  U19_GA(x1, x2)
U20_GA(x1, x2, x3)  =  U20_GA(x1, x3)
U68_GGA(x1, x2, x3)  =  U68_GGA(x1, x3)
U69_GGA(x1, x2)  =  U69_GGA(x1, x2)
QUOT732_IN_G(x1)  =  QUOT732_IN_G(x1)
U21_G(x1, x2)  =  U21_G(x1, x2)
QUOT811_IN_G(x1)  =  QUOT811_IN_G(x1)
U34_G(x1, x2)  =  U34_G(x1, x2)
U70_GGA(x1, x2, x3)  =  U70_GGA(x1, x3)
QUOT823_IN_GA(x1, x2)  =  QUOT823_IN_GA(x1)
U22_GA(x1, x2, x3)  =  U22_GA(x1, x3)
QUOT908_IN_GA(x1, x2)  =  QUOT908_IN_GA(x1)
U23_GA(x1, x2)  =  U23_GA(x1, x2)
U24_GA(x1, x2, x3)  =  U24_GA(x1, x3)
U71_GGA(x1, x2, x3)  =  U71_GGA(x1, x3)
U72_GGA(x1, x2)  =  U72_GGA(x1, x2)
QUOT949_IN_G(x1)  =  QUOT949_IN_G(x1)
U25_G(x1, x2)  =  U25_G(x1, x2)
QUOT1041_IN_G(x1)  =  QUOT1041_IN_G(x1)
U35_G(x1, x2)  =  U35_G(x1, x2)
U73_GGA(x1, x2, x3)  =  U73_GGA(x1, x3)
QUOT1053_IN_GA(x1, x2)  =  QUOT1053_IN_GA(x1)
U26_GA(x1, x2, x3)  =  U26_GA(x1, x3)
QUOT1152_IN_GA(x1, x2)  =  QUOT1152_IN_GA(x1)
U27_GA(x1, x2)  =  U27_GA(x1, x2)
U28_GA(x1, x2, x3)  =  U28_GA(x1, x3)
U74_GGA(x1, x2, x3)  =  U74_GGA(x1, x3)
U75_GGA(x1, x2, x3, x4)  =  U75_GGA(x1, x2, x4)
QUOT1175_IN_GGGA(x1, x2, x3, x4)  =  QUOT1175_IN_GGGA(x1, x2, x3)
U76_GGGA(x1, x2, x3)  =  U76_GGGA(x1, x2, x3)
QUOT1194_IN_GG(x1, x2)  =  QUOT1194_IN_GG(x1, x2)
U36_GG(x1, x2)  =  U36_GG(x1, x2)
U37_GG(x1, x2)  =  U37_GG(x1, x2)
U38_GG(x1, x2)  =  U38_GG(x1, x2)
U39_GG(x1, x2)  =  U39_GG(x1, x2)
U40_GG(x1, x2)  =  U40_GG(x1, x2)
U41_GG(x1, x2)  =  U41_GG(x1, x2)
U42_GG(x1, x2)  =  U42_GG(x1, x2)
U43_GG(x1, x2)  =  U43_GG(x1, x2)
U44_GG(x1, x2)  =  U44_GG(x1, x2)
U45_GG(x1, x2)  =  U45_GG(x1, x2)
U46_GG(x1, x2)  =  U46_GG(x1, x2)
U47_GG(x1, x2)  =  U47_GG(x1, x2)
U48_GG(x1, x2)  =  U48_GG(x1, x2)
U49_GG(x1, x2)  =  U49_GG(x1, x2)
U50_GG(x1, x2, x3)  =  U50_GG(x1, x2, x3)
QUOT1405_IN_GGG(x1, x2, x3)  =  QUOT1405_IN_GGG(x1, x2, x3)
U51_GGG(x1, x2, x3)  =  U51_GGG(x1, x2, x3)
U52_GGG(x1, x2, x3)  =  U52_GGG(x1, x2, x3)
U53_GGG(x1, x2, x3, x4)  =  U53_GGG(x1, x2, x3, x4)
U77_GGGA(x1, x2, x3, x4)  =  U77_GGGA(x1, x2, x4)
U78_GGGA(x1, x2, x3)  =  U78_GGGA(x1, x2, x3)
U79_GGGA(x1, x2, x3, x4)  =  U79_GGGA(x1, x2, x4)
U80_GGGA(x1, x2, x3, x4, x5)  =  U80_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 16 SCCs with 126 less nodes.

(6) Complex Obligation (AND)

(7) Obligation:

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

QUOT949_IN_G(s(s(s(s(s(s(s(T961)))))))) → QUOT1041_IN_G(T961)
QUOT1041_IN_G(T966) → QUOT949_IN_G(T966)

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

(8) PiDPToQDPProof (EQUIVALENT transformation)

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

(9) Obligation:

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

QUOT949_IN_G(s(s(s(s(s(s(s(T961)))))))) → QUOT1041_IN_G(T961)
QUOT1041_IN_G(T966) → QUOT949_IN_G(T966)

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

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

  • QUOT1041_IN_G(T966) → QUOT949_IN_G(T966)
    The graph contains the following edges 1 >= 1

  • QUOT949_IN_G(s(s(s(s(s(s(s(T961)))))))) → QUOT1041_IN_G(T961)
    The graph contains the following edges 1 > 1

(11) YES

(12) Obligation:

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

QUOT1152_IN_GA(T1105, s(T1111)) → QUOT1053_IN_GA(T1105, T1111)
QUOT1053_IN_GA(s(s(s(s(s(s(s(T1092))))))), T1094) → QUOT1152_IN_GA(T1092, T1094)

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

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

(13) PiDPToQDPProof (SOUND transformation)

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

(14) Obligation:

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

QUOT1152_IN_GA(T1105) → QUOT1053_IN_GA(T1105)
QUOT1053_IN_GA(s(s(s(s(s(s(s(T1092)))))))) → QUOT1152_IN_GA(T1092)

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

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

  • QUOT1053_IN_GA(s(s(s(s(s(s(s(T1092)))))))) → QUOT1152_IN_GA(T1092)
    The graph contains the following edges 1 > 1

  • QUOT1152_IN_GA(T1105) → QUOT1053_IN_GA(T1105)
    The graph contains the following edges 1 >= 1

(16) YES

(17) Obligation:

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

QUOT732_IN_G(s(s(s(s(s(s(T760))))))) → QUOT811_IN_G(T760)
QUOT811_IN_G(T765) → QUOT732_IN_G(T765)

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

(18) PiDPToQDPProof (EQUIVALENT transformation)

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

(19) Obligation:

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

QUOT732_IN_G(s(s(s(s(s(s(T760))))))) → QUOT811_IN_G(T760)
QUOT811_IN_G(T765) → QUOT732_IN_G(T765)

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

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

  • QUOT811_IN_G(T765) → QUOT732_IN_G(T765)
    The graph contains the following edges 1 >= 1

  • QUOT732_IN_G(s(s(s(s(s(s(T760))))))) → QUOT811_IN_G(T760)
    The graph contains the following edges 1 > 1

(21) YES

(22) Obligation:

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

QUOT908_IN_GA(T886, s(T892)) → QUOT823_IN_GA(T886, T892)
QUOT823_IN_GA(s(s(s(s(s(s(T873)))))), T875) → QUOT908_IN_GA(T873, T875)

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

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

(23) PiDPToQDPProof (SOUND transformation)

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

(24) Obligation:

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

QUOT908_IN_GA(T886) → QUOT823_IN_GA(T886)
QUOT823_IN_GA(s(s(s(s(s(s(T873))))))) → QUOT908_IN_GA(T873)

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

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

  • QUOT823_IN_GA(s(s(s(s(s(s(T873))))))) → QUOT908_IN_GA(T873)
    The graph contains the following edges 1 > 1

  • QUOT908_IN_GA(T886) → QUOT823_IN_GA(T886)
    The graph contains the following edges 1 >= 1

(26) YES

(27) Obligation:

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

QUOT542_IN_G(s(s(s(s(s(T581)))))) → QUOT608_IN_G(T581)
QUOT608_IN_G(T586) → QUOT542_IN_G(T586)

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

(28) PiDPToQDPProof (EQUIVALENT transformation)

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

(29) Obligation:

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

QUOT542_IN_G(s(s(s(s(s(T581)))))) → QUOT608_IN_G(T581)
QUOT608_IN_G(T586) → QUOT542_IN_G(T586)

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

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

  • QUOT608_IN_G(T586) → QUOT542_IN_G(T586)
    The graph contains the following edges 1 >= 1

  • QUOT542_IN_G(s(s(s(s(s(T581)))))) → QUOT608_IN_G(T581)
    The graph contains the following edges 1 > 1

(31) YES

(32) Obligation:

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

QUOT691_IN_GA(T689, s(T695)) → QUOT620_IN_GA(T689, T695)
QUOT620_IN_GA(s(s(s(s(s(T676))))), T678) → QUOT691_IN_GA(T676, T678)

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

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

(33) PiDPToQDPProof (SOUND transformation)

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

(34) Obligation:

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

QUOT691_IN_GA(T689) → QUOT620_IN_GA(T689)
QUOT620_IN_GA(s(s(s(s(s(T676)))))) → QUOT691_IN_GA(T676)

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

(35) QDPSizeChangeProof (EQUIVALENT transformation)

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

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

  • QUOT620_IN_GA(s(s(s(s(s(T676)))))) → QUOT691_IN_GA(T676)
    The graph contains the following edges 1 > 1

  • QUOT691_IN_GA(T689) → QUOT620_IN_GA(T689)
    The graph contains the following edges 1 >= 1

(36) YES

(37) Obligation:

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

QUOT379_IN_G(s(s(s(s(T424))))) → QUOT432_IN_G(T424)
QUOT432_IN_G(T429) → QUOT379_IN_G(T429)

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

(38) PiDPToQDPProof (EQUIVALENT 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:

QUOT379_IN_G(s(s(s(s(T424))))) → QUOT432_IN_G(T424)
QUOT432_IN_G(T429) → QUOT379_IN_G(T429)

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:

  • QUOT432_IN_G(T429) → QUOT379_IN_G(T429)
    The graph contains the following edges 1 >= 1

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

(41) YES

(42) Obligation:

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

QUOT501_IN_GA(T514, s(T520)) → QUOT444_IN_GA(T514, T520)
QUOT444_IN_GA(s(s(s(s(T501)))), T503) → QUOT501_IN_GA(T501, T503)

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

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

(43) PiDPToQDPProof (SOUND transformation)

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

(44) Obligation:

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

QUOT501_IN_GA(T514) → QUOT444_IN_GA(T514)
QUOT444_IN_GA(s(s(s(s(T501))))) → QUOT501_IN_GA(T501)

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

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

  • QUOT444_IN_GA(s(s(s(s(T501))))) → QUOT501_IN_GA(T501)
    The graph contains the following edges 1 > 1

  • QUOT501_IN_GA(T514) → QUOT444_IN_GA(T514)
    The graph contains the following edges 1 >= 1

(46) YES

(47) Obligation:

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

QUOT243_IN_G(s(s(s(T289)))) → QUOT283_IN_G(T289)
QUOT283_IN_G(T294) → QUOT243_IN_G(T294)

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

(48) PiDPToQDPProof (EQUIVALENT transformation)

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

(49) Obligation:

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

QUOT243_IN_G(s(s(s(T289)))) → QUOT283_IN_G(T289)
QUOT283_IN_G(T294) → QUOT243_IN_G(T294)

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

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

  • QUOT283_IN_G(T294) → QUOT243_IN_G(T294)
    The graph contains the following edges 1 >= 1

  • QUOT243_IN_G(s(s(s(T289)))) → QUOT283_IN_G(T289)
    The graph contains the following edges 1 > 1

(51) YES

(52) Obligation:

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

QUOT338_IN_GA(T361, s(T367)) → QUOT295_IN_GA(T361, T367)
QUOT295_IN_GA(s(s(s(T348))), T350) → QUOT338_IN_GA(T348, T350)

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

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

(53) PiDPToQDPProof (SOUND transformation)

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

(54) Obligation:

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

QUOT338_IN_GA(T361) → QUOT295_IN_GA(T361)
QUOT295_IN_GA(s(s(s(T348)))) → QUOT338_IN_GA(T348)

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

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

  • QUOT295_IN_GA(s(s(s(T348)))) → QUOT338_IN_GA(T348)
    The graph contains the following edges 1 > 1

  • QUOT338_IN_GA(T361) → QUOT295_IN_GA(T361)
    The graph contains the following edges 1 >= 1

(56) YES

(57) Obligation:

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

QUOT134_IN_G(s(s(T176))) → QUOT161_IN_G(T176)
QUOT161_IN_G(T181) → QUOT134_IN_G(T181)

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

(58) PiDPToQDPProof (EQUIVALENT transformation)

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

(59) Obligation:

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

QUOT134_IN_G(s(s(T176))) → QUOT161_IN_G(T176)
QUOT161_IN_G(T181) → QUOT134_IN_G(T181)

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

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

  • QUOT161_IN_G(T181) → QUOT134_IN_G(T181)
    The graph contains the following edges 1 >= 1

  • QUOT134_IN_G(s(s(T176))) → QUOT161_IN_G(T176)
    The graph contains the following edges 1 > 1

(61) YES

(62) Obligation:

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

QUOT202_IN_GA(T230, s(T236)) → QUOT173_IN_GA(T230, T236)
QUOT173_IN_GA(s(s(T217)), T219) → QUOT202_IN_GA(T217, T219)

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

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

(63) PiDPToQDPProof (SOUND transformation)

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

(64) Obligation:

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

QUOT202_IN_GA(T230) → QUOT173_IN_GA(T230)
QUOT173_IN_GA(s(s(T217))) → QUOT202_IN_GA(T217)

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

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

  • QUOT173_IN_GA(s(s(T217))) → QUOT202_IN_GA(T217)
    The graph contains the following edges 1 > 1

  • QUOT202_IN_GA(T230) → QUOT173_IN_GA(T230)
    The graph contains the following edges 1 >= 1

(66) YES

(67) Obligation:

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

QUOT52_IN_G(s(T85)) → QUOT66_IN_G(T85)
QUOT66_IN_G(T90) → QUOT52_IN_G(T90)

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

(68) PiDPToQDPProof (EQUIVALENT transformation)

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

(69) Obligation:

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

QUOT52_IN_G(s(T85)) → QUOT66_IN_G(T85)
QUOT66_IN_G(T90) → QUOT52_IN_G(T90)

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

(70) QDPSizeChangeProof (EQUIVALENT transformation)

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

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

  • QUOT66_IN_G(T90) → QUOT52_IN_G(T90)
    The graph contains the following edges 1 >= 1

  • QUOT52_IN_G(s(T85)) → QUOT66_IN_G(T85)
    The graph contains the following edges 1 > 1

(71) YES

(72) Obligation:

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

QUOT1194_IN_GG(s(s(s(s(s(s(s(s(T1320)))))))), s(s(s(s(s(s(s(T1326)))))))) → QUOT1405_IN_GGG(T1320, T1326, s(s(s(s(s(s(s(T1326))))))))
QUOT1405_IN_GGG(T1345, 0, T1351) → QUOT1194_IN_GG(T1345, T1351)
QUOT1405_IN_GGG(s(T1372), 0, T1378) → QUOT1194_IN_GG(T1372, T1378)
QUOT1405_IN_GGG(s(T1362), s(T1385), T1364) → QUOT1405_IN_GGG(T1362, T1385, T1364)

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

(73) PiDPToQDPProof (EQUIVALENT transformation)

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

(74) Obligation:

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

QUOT1194_IN_GG(s(s(s(s(s(s(s(s(T1320)))))))), s(s(s(s(s(s(s(T1326)))))))) → QUOT1405_IN_GGG(T1320, T1326, s(s(s(s(s(s(s(T1326))))))))
QUOT1405_IN_GGG(T1345, 0, T1351) → QUOT1194_IN_GG(T1345, T1351)
QUOT1405_IN_GGG(s(T1372), 0, T1378) → QUOT1194_IN_GG(T1372, T1378)
QUOT1405_IN_GGG(s(T1362), s(T1385), T1364) → QUOT1405_IN_GGG(T1362, T1385, T1364)

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

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

  • QUOT1405_IN_GGG(s(T1362), s(T1385), T1364) → QUOT1405_IN_GGG(T1362, T1385, T1364)
    The graph contains the following edges 1 > 1, 2 > 2, 3 >= 3

  • QUOT1194_IN_GG(s(s(s(s(s(s(s(s(T1320)))))))), s(s(s(s(s(s(s(T1326)))))))) → QUOT1405_IN_GGG(T1320, T1326, s(s(s(s(s(s(s(T1326))))))))
    The graph contains the following edges 1 > 1, 2 > 2, 2 >= 3

  • QUOT1405_IN_GGG(T1345, 0, T1351) → QUOT1194_IN_GG(T1345, T1351)
    The graph contains the following edges 1 >= 1, 3 >= 2

  • QUOT1405_IN_GGG(s(T1372), 0, T1378) → QUOT1194_IN_GG(T1372, T1378)
    The graph contains the following edges 1 > 1, 3 >= 2

(76) YES

(77) Obligation:

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

QUOT93_IN_GA(T121, s(T127)) → QUOT78_IN_GA(T121, T127)
QUOT78_IN_GA(s(T108), T110) → QUOT93_IN_GA(T108, T110)

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

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

(78) PiDPToQDPProof (SOUND transformation)

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

(79) Obligation:

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

QUOT93_IN_GA(T121) → QUOT78_IN_GA(T121)
QUOT78_IN_GA(s(T108)) → QUOT93_IN_GA(T108)

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

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

  • QUOT78_IN_GA(s(T108)) → QUOT93_IN_GA(T108)
    The graph contains the following edges 1 > 1

  • QUOT93_IN_GA(T121) → QUOT78_IN_GA(T121)
    The graph contains the following edges 1 >= 1

(81) YES

(82) Obligation:

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

QUOT3_IN_GGA(s(s(s(s(s(s(s(s(T1119)))))))), s(s(s(s(s(s(s(s(T1129)))))))), T1122) → QUOT1175_IN_GGGA(T1119, T1129, s(s(s(s(s(s(s(T1129))))))), T1122)
QUOT1175_IN_GGGA(T1161, 0, T1169, s(T1391)) → QUOT3_IN_GGA(T1161, s(T1169), T1391)
QUOT1175_IN_GGGA(s(T1419), 0, T1427, s(T1433)) → QUOT3_IN_GGA(T1419, s(T1427), T1433)
QUOT1175_IN_GGGA(s(T1402), s(T1438), T1404, T1406) → QUOT1175_IN_GGGA(T1402, T1438, T1404, T1406)

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

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

(83) PiDPToQDPProof (SOUND transformation)

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

(84) Obligation:

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

QUOT3_IN_GGA(s(s(s(s(s(s(s(s(T1119)))))))), s(s(s(s(s(s(s(s(T1129))))))))) → QUOT1175_IN_GGGA(T1119, T1129, s(s(s(s(s(s(s(T1129))))))))
QUOT1175_IN_GGGA(T1161, 0, T1169) → QUOT3_IN_GGA(T1161, s(T1169))
QUOT1175_IN_GGGA(s(T1419), 0, T1427) → QUOT3_IN_GGA(T1419, s(T1427))
QUOT1175_IN_GGGA(s(T1402), s(T1438), T1404) → QUOT1175_IN_GGGA(T1402, T1438, T1404)

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

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

  • QUOT1175_IN_GGGA(s(T1402), s(T1438), T1404) → QUOT1175_IN_GGGA(T1402, T1438, T1404)
    The graph contains the following edges 1 > 1, 2 > 2, 3 >= 3

  • QUOT3_IN_GGA(s(s(s(s(s(s(s(s(T1119)))))))), s(s(s(s(s(s(s(s(T1129))))))))) → QUOT1175_IN_GGGA(T1119, T1129, s(s(s(s(s(s(s(T1129))))))))
    The graph contains the following edges 1 > 1, 2 > 2, 2 > 3

  • QUOT1175_IN_GGGA(T1161, 0, T1169) → QUOT3_IN_GGA(T1161, s(T1169))
    The graph contains the following edges 1 >= 1

  • QUOT1175_IN_GGGA(s(T1419), 0, T1427) → QUOT3_IN_GGA(T1419, s(T1427))
    The graph contains the following edges 1 > 1

(86) YES