(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