(0) Obligation:

Clauses:

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

Queries:

div(g,g,a).

(1) PrologToDTProblemTransformerProof (SOUND transformation)

Built DT problem from termination graph.

(2) Obligation:

Triples:

quot52(s(T111), s(T113)) :- quot52(T111, T113).
quot157(s(s(T239)), s(T241)) :- quot157(T239, T241).
quot297(s(s(s(T385))), s(T387)) :- quot297(T385, T387).
quot472(s(s(s(s(T549)))), s(T551)) :- quot472(T549, T551).
quot682(s(s(s(s(s(T731))))), s(T733)) :- quot682(T731, T733).
quot927(s(s(s(s(s(s(T931)))))), s(T933)) :- quot927(T931, T933).
quot1207(s(s(s(s(s(s(s(T1149))))))), s(T1151)) :- quot1207(T1149, T1151).
quot3(s(T78), s(0), s(T80)) :- quot52(T78, T80).
quot3(s(s(T188)), s(s(0)), s(T190)) :- quot157(T188, T190).
quot3(s(s(s(T316))), s(s(s(0))), s(T318)) :- quot297(T316, T318).
quot3(s(s(s(s(T462)))), s(s(s(s(0)))), s(T464)) :- quot472(T462, T464).
quot3(s(s(s(s(s(T626))))), s(s(s(s(s(0))))), s(T628)) :- quot682(T626, T628).
quot3(s(s(s(s(s(s(T808)))))), s(s(s(s(s(s(0)))))), s(T810)) :- quot927(T808, T810).
quot3(s(s(s(s(s(s(s(T1008))))))), s(s(s(s(s(s(s(0))))))), s(T1010)) :- quot1207(T1008, T1010).
quot3(s(s(s(s(s(s(s(s(T1205)))))))), s(s(s(s(s(s(s(s(T1210)))))))), T1178) :- quot1514(T1205, T1210, s(s(s(s(s(s(s(T1210))))))), T1178).
quot1514(T1240, 0, T1241, s(T1243)) :- quot3(T1240, s(T1241), T1243).
quot1514(s(T1290), s(T1295), T1259, T1261) :- quot1514(T1290, T1295, T1259, T1261).
div1(T7, T8, T10) :- quot3(T7, T8, T10).

Clauses:

quotc52(0, 0).
quotc52(s(T111), s(T113)) :- quotc52(T111, T113).
quotc157(0, 0).
quotc157(s(0), 0).
quotc157(s(s(T239)), s(T241)) :- quotc157(T239, T241).
quotc297(0, 0).
quotc297(s(0), 0).
quotc297(s(s(0)), 0).
quotc297(s(s(s(T385))), s(T387)) :- quotc297(T385, T387).
quotc472(0, 0).
quotc472(s(0), 0).
quotc472(s(s(0)), 0).
quotc472(s(s(s(0))), 0).
quotc472(s(s(s(s(T549)))), s(T551)) :- quotc472(T549, T551).
quotc682(0, 0).
quotc682(s(0), 0).
quotc682(s(s(0)), 0).
quotc682(s(s(s(0))), 0).
quotc682(s(s(s(s(0)))), 0).
quotc682(s(s(s(s(s(T731))))), s(T733)) :- quotc682(T731, T733).
quotc927(0, 0).
quotc927(s(0), 0).
quotc927(s(s(0)), 0).
quotc927(s(s(s(0))), 0).
quotc927(s(s(s(s(0)))), 0).
quotc927(s(s(s(s(s(0))))), 0).
quotc927(s(s(s(s(s(s(T931)))))), s(T933)) :- quotc927(T931, T933).
quotc1207(0, 0).
quotc1207(s(0), 0).
quotc1207(s(s(0)), 0).
quotc1207(s(s(s(0))), 0).
quotc1207(s(s(s(s(0)))), 0).
quotc1207(s(s(s(s(s(0))))), 0).
quotc1207(s(s(s(s(s(s(0)))))), 0).
quotc1207(s(s(s(s(s(s(s(T1149))))))), s(T1151)) :- quotc1207(T1149, T1151).
quotc3(0, s(T15), 0).
quotc3(s(0), s(s(T69)), 0).
quotc3(s(T78), s(0), s(T80)) :- quotc52(T78, T80).
quotc3(s(s(0)), s(s(s(T179))), 0).
quotc3(s(s(T188)), s(s(0)), s(T190)) :- quotc157(T188, T190).
quotc3(s(s(s(0))), s(s(s(s(T307)))), 0).
quotc3(s(s(s(T316))), s(s(s(0))), s(T318)) :- quotc297(T316, T318).
quotc3(s(s(s(s(0)))), s(s(s(s(s(T453))))), 0).
quotc3(s(s(s(s(T462)))), s(s(s(s(0)))), s(T464)) :- quotc472(T462, T464).
quotc3(s(s(s(s(s(0))))), s(s(s(s(s(s(T617)))))), 0).
quotc3(s(s(s(s(s(T626))))), s(s(s(s(s(0))))), s(T628)) :- quotc682(T626, T628).
quotc3(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T799))))))), 0).
quotc3(s(s(s(s(s(s(T808)))))), s(s(s(s(s(s(0)))))), s(T810)) :- quotc927(T808, T810).
quotc3(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(T999)))))))), 0).
quotc3(s(s(s(s(s(s(s(T1008))))))), s(s(s(s(s(s(s(0))))))), s(T1010)) :- quotc1207(T1008, T1010).
quotc3(s(s(s(s(s(s(s(s(T1205)))))))), s(s(s(s(s(s(s(s(T1210)))))))), T1178) :- quotc1514(T1205, T1210, s(s(s(s(s(s(s(T1210))))))), T1178).
quotc1514(0, s(T1226), T1227, 0).
quotc1514(T1240, 0, T1241, s(T1243)) :- quotc3(T1240, s(T1241), T1243).
quotc1514(s(T1290), s(T1295), T1259, T1261) :- quotc1514(T1290, T1295, T1259, T1261).

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,f)
quot157_in: (b,f)
quot297_in: (b,f)
quot472_in: (b,f)
quot682_in: (b,f)
quot927_in: (b,f)
quot1207_in: (b,f)
quot1514_in: (b,b,b,f)
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) → U18_GGA(T7, T8, T10, quot3_in_gga(T7, T8, T10))
DIV1_IN_GGA(T7, T8, T10) → QUOT3_IN_GGA(T7, T8, T10)
QUOT3_IN_GGA(s(T78), s(0), s(T80)) → U8_GGA(T78, T80, quot52_in_ga(T78, T80))
QUOT3_IN_GGA(s(T78), s(0), s(T80)) → QUOT52_IN_GA(T78, T80)
QUOT52_IN_GA(s(T111), s(T113)) → U1_GA(T111, T113, quot52_in_ga(T111, T113))
QUOT52_IN_GA(s(T111), s(T113)) → QUOT52_IN_GA(T111, T113)
QUOT3_IN_GGA(s(s(T188)), s(s(0)), s(T190)) → U9_GGA(T188, T190, quot157_in_ga(T188, T190))
QUOT3_IN_GGA(s(s(T188)), s(s(0)), s(T190)) → QUOT157_IN_GA(T188, T190)
QUOT157_IN_GA(s(s(T239)), s(T241)) → U2_GA(T239, T241, quot157_in_ga(T239, T241))
QUOT157_IN_GA(s(s(T239)), s(T241)) → QUOT157_IN_GA(T239, T241)
QUOT3_IN_GGA(s(s(s(T316))), s(s(s(0))), s(T318)) → U10_GGA(T316, T318, quot297_in_ga(T316, T318))
QUOT3_IN_GGA(s(s(s(T316))), s(s(s(0))), s(T318)) → QUOT297_IN_GA(T316, T318)
QUOT297_IN_GA(s(s(s(T385))), s(T387)) → U3_GA(T385, T387, quot297_in_ga(T385, T387))
QUOT297_IN_GA(s(s(s(T385))), s(T387)) → QUOT297_IN_GA(T385, T387)
QUOT3_IN_GGA(s(s(s(s(T462)))), s(s(s(s(0)))), s(T464)) → U11_GGA(T462, T464, quot472_in_ga(T462, T464))
QUOT3_IN_GGA(s(s(s(s(T462)))), s(s(s(s(0)))), s(T464)) → QUOT472_IN_GA(T462, T464)
QUOT472_IN_GA(s(s(s(s(T549)))), s(T551)) → U4_GA(T549, T551, quot472_in_ga(T549, T551))
QUOT472_IN_GA(s(s(s(s(T549)))), s(T551)) → QUOT472_IN_GA(T549, T551)
QUOT3_IN_GGA(s(s(s(s(s(T626))))), s(s(s(s(s(0))))), s(T628)) → U12_GGA(T626, T628, quot682_in_ga(T626, T628))
QUOT3_IN_GGA(s(s(s(s(s(T626))))), s(s(s(s(s(0))))), s(T628)) → QUOT682_IN_GA(T626, T628)
QUOT682_IN_GA(s(s(s(s(s(T731))))), s(T733)) → U5_GA(T731, T733, quot682_in_ga(T731, T733))
QUOT682_IN_GA(s(s(s(s(s(T731))))), s(T733)) → QUOT682_IN_GA(T731, T733)
QUOT3_IN_GGA(s(s(s(s(s(s(T808)))))), s(s(s(s(s(s(0)))))), s(T810)) → U13_GGA(T808, T810, quot927_in_ga(T808, T810))
QUOT3_IN_GGA(s(s(s(s(s(s(T808)))))), s(s(s(s(s(s(0)))))), s(T810)) → QUOT927_IN_GA(T808, T810)
QUOT927_IN_GA(s(s(s(s(s(s(T931)))))), s(T933)) → U6_GA(T931, T933, quot927_in_ga(T931, T933))
QUOT927_IN_GA(s(s(s(s(s(s(T931)))))), s(T933)) → QUOT927_IN_GA(T931, T933)
QUOT3_IN_GGA(s(s(s(s(s(s(s(T1008))))))), s(s(s(s(s(s(s(0))))))), s(T1010)) → U14_GGA(T1008, T1010, quot1207_in_ga(T1008, T1010))
QUOT3_IN_GGA(s(s(s(s(s(s(s(T1008))))))), s(s(s(s(s(s(s(0))))))), s(T1010)) → QUOT1207_IN_GA(T1008, T1010)
QUOT1207_IN_GA(s(s(s(s(s(s(s(T1149))))))), s(T1151)) → U7_GA(T1149, T1151, quot1207_in_ga(T1149, T1151))
QUOT1207_IN_GA(s(s(s(s(s(s(s(T1149))))))), s(T1151)) → QUOT1207_IN_GA(T1149, T1151)
QUOT3_IN_GGA(s(s(s(s(s(s(s(s(T1205)))))))), s(s(s(s(s(s(s(s(T1210)))))))), T1178) → U15_GGA(T1205, T1210, T1178, quot1514_in_ggga(T1205, T1210, s(s(s(s(s(s(s(T1210))))))), T1178))
QUOT3_IN_GGA(s(s(s(s(s(s(s(s(T1205)))))))), s(s(s(s(s(s(s(s(T1210)))))))), T1178) → QUOT1514_IN_GGGA(T1205, T1210, s(s(s(s(s(s(s(T1210))))))), T1178)
QUOT1514_IN_GGGA(T1240, 0, T1241, s(T1243)) → U16_GGGA(T1240, T1241, T1243, quot3_in_gga(T1240, s(T1241), T1243))
QUOT1514_IN_GGGA(T1240, 0, T1241, s(T1243)) → QUOT3_IN_GGA(T1240, s(T1241), T1243)
QUOT1514_IN_GGGA(s(T1290), s(T1295), T1259, T1261) → U17_GGGA(T1290, T1295, T1259, T1261, quot1514_in_ggga(T1290, T1295, T1259, T1261))
QUOT1514_IN_GGGA(s(T1290), s(T1295), T1259, T1261) → QUOT1514_IN_GGGA(T1290, T1295, T1259, T1261)

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_ga(x1, x2)  =  quot52_in_ga(x1)
quot157_in_ga(x1, x2)  =  quot157_in_ga(x1)
quot297_in_ga(x1, x2)  =  quot297_in_ga(x1)
quot472_in_ga(x1, x2)  =  quot472_in_ga(x1)
quot682_in_ga(x1, x2)  =  quot682_in_ga(x1)
quot927_in_ga(x1, x2)  =  quot927_in_ga(x1)
quot1207_in_ga(x1, x2)  =  quot1207_in_ga(x1)
quot1514_in_ggga(x1, x2, x3, x4)  =  quot1514_in_ggga(x1, x2, x3)
DIV1_IN_GGA(x1, x2, x3)  =  DIV1_IN_GGA(x1, x2)
U18_GGA(x1, x2, x3, x4)  =  U18_GGA(x1, x2, x4)
QUOT3_IN_GGA(x1, x2, x3)  =  QUOT3_IN_GGA(x1, x2)
U8_GGA(x1, x2, x3)  =  U8_GGA(x1, x3)
QUOT52_IN_GA(x1, x2)  =  QUOT52_IN_GA(x1)
U1_GA(x1, x2, x3)  =  U1_GA(x1, x3)
U9_GGA(x1, x2, x3)  =  U9_GGA(x1, x3)
QUOT157_IN_GA(x1, x2)  =  QUOT157_IN_GA(x1)
U2_GA(x1, x2, x3)  =  U2_GA(x1, x3)
U10_GGA(x1, x2, x3)  =  U10_GGA(x1, x3)
QUOT297_IN_GA(x1, x2)  =  QUOT297_IN_GA(x1)
U3_GA(x1, x2, x3)  =  U3_GA(x1, x3)
U11_GGA(x1, x2, x3)  =  U11_GGA(x1, x3)
QUOT472_IN_GA(x1, x2)  =  QUOT472_IN_GA(x1)
U4_GA(x1, x2, x3)  =  U4_GA(x1, x3)
U12_GGA(x1, x2, x3)  =  U12_GGA(x1, x3)
QUOT682_IN_GA(x1, x2)  =  QUOT682_IN_GA(x1)
U5_GA(x1, x2, x3)  =  U5_GA(x1, x3)
U13_GGA(x1, x2, x3)  =  U13_GGA(x1, x3)
QUOT927_IN_GA(x1, x2)  =  QUOT927_IN_GA(x1)
U6_GA(x1, x2, x3)  =  U6_GA(x1, x3)
U14_GGA(x1, x2, x3)  =  U14_GGA(x1, x3)
QUOT1207_IN_GA(x1, x2)  =  QUOT1207_IN_GA(x1)
U7_GA(x1, x2, x3)  =  U7_GA(x1, x3)
U15_GGA(x1, x2, x3, x4)  =  U15_GGA(x1, x2, x4)
QUOT1514_IN_GGGA(x1, x2, x3, x4)  =  QUOT1514_IN_GGGA(x1, x2, x3)
U16_GGGA(x1, x2, x3, x4)  =  U16_GGGA(x1, x2, x4)
U17_GGGA(x1, x2, x3, x4, x5)  =  U17_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) → U18_GGA(T7, T8, T10, quot3_in_gga(T7, T8, T10))
DIV1_IN_GGA(T7, T8, T10) → QUOT3_IN_GGA(T7, T8, T10)
QUOT3_IN_GGA(s(T78), s(0), s(T80)) → U8_GGA(T78, T80, quot52_in_ga(T78, T80))
QUOT3_IN_GGA(s(T78), s(0), s(T80)) → QUOT52_IN_GA(T78, T80)
QUOT52_IN_GA(s(T111), s(T113)) → U1_GA(T111, T113, quot52_in_ga(T111, T113))
QUOT52_IN_GA(s(T111), s(T113)) → QUOT52_IN_GA(T111, T113)
QUOT3_IN_GGA(s(s(T188)), s(s(0)), s(T190)) → U9_GGA(T188, T190, quot157_in_ga(T188, T190))
QUOT3_IN_GGA(s(s(T188)), s(s(0)), s(T190)) → QUOT157_IN_GA(T188, T190)
QUOT157_IN_GA(s(s(T239)), s(T241)) → U2_GA(T239, T241, quot157_in_ga(T239, T241))
QUOT157_IN_GA(s(s(T239)), s(T241)) → QUOT157_IN_GA(T239, T241)
QUOT3_IN_GGA(s(s(s(T316))), s(s(s(0))), s(T318)) → U10_GGA(T316, T318, quot297_in_ga(T316, T318))
QUOT3_IN_GGA(s(s(s(T316))), s(s(s(0))), s(T318)) → QUOT297_IN_GA(T316, T318)
QUOT297_IN_GA(s(s(s(T385))), s(T387)) → U3_GA(T385, T387, quot297_in_ga(T385, T387))
QUOT297_IN_GA(s(s(s(T385))), s(T387)) → QUOT297_IN_GA(T385, T387)
QUOT3_IN_GGA(s(s(s(s(T462)))), s(s(s(s(0)))), s(T464)) → U11_GGA(T462, T464, quot472_in_ga(T462, T464))
QUOT3_IN_GGA(s(s(s(s(T462)))), s(s(s(s(0)))), s(T464)) → QUOT472_IN_GA(T462, T464)
QUOT472_IN_GA(s(s(s(s(T549)))), s(T551)) → U4_GA(T549, T551, quot472_in_ga(T549, T551))
QUOT472_IN_GA(s(s(s(s(T549)))), s(T551)) → QUOT472_IN_GA(T549, T551)
QUOT3_IN_GGA(s(s(s(s(s(T626))))), s(s(s(s(s(0))))), s(T628)) → U12_GGA(T626, T628, quot682_in_ga(T626, T628))
QUOT3_IN_GGA(s(s(s(s(s(T626))))), s(s(s(s(s(0))))), s(T628)) → QUOT682_IN_GA(T626, T628)
QUOT682_IN_GA(s(s(s(s(s(T731))))), s(T733)) → U5_GA(T731, T733, quot682_in_ga(T731, T733))
QUOT682_IN_GA(s(s(s(s(s(T731))))), s(T733)) → QUOT682_IN_GA(T731, T733)
QUOT3_IN_GGA(s(s(s(s(s(s(T808)))))), s(s(s(s(s(s(0)))))), s(T810)) → U13_GGA(T808, T810, quot927_in_ga(T808, T810))
QUOT3_IN_GGA(s(s(s(s(s(s(T808)))))), s(s(s(s(s(s(0)))))), s(T810)) → QUOT927_IN_GA(T808, T810)
QUOT927_IN_GA(s(s(s(s(s(s(T931)))))), s(T933)) → U6_GA(T931, T933, quot927_in_ga(T931, T933))
QUOT927_IN_GA(s(s(s(s(s(s(T931)))))), s(T933)) → QUOT927_IN_GA(T931, T933)
QUOT3_IN_GGA(s(s(s(s(s(s(s(T1008))))))), s(s(s(s(s(s(s(0))))))), s(T1010)) → U14_GGA(T1008, T1010, quot1207_in_ga(T1008, T1010))
QUOT3_IN_GGA(s(s(s(s(s(s(s(T1008))))))), s(s(s(s(s(s(s(0))))))), s(T1010)) → QUOT1207_IN_GA(T1008, T1010)
QUOT1207_IN_GA(s(s(s(s(s(s(s(T1149))))))), s(T1151)) → U7_GA(T1149, T1151, quot1207_in_ga(T1149, T1151))
QUOT1207_IN_GA(s(s(s(s(s(s(s(T1149))))))), s(T1151)) → QUOT1207_IN_GA(T1149, T1151)
QUOT3_IN_GGA(s(s(s(s(s(s(s(s(T1205)))))))), s(s(s(s(s(s(s(s(T1210)))))))), T1178) → U15_GGA(T1205, T1210, T1178, quot1514_in_ggga(T1205, T1210, s(s(s(s(s(s(s(T1210))))))), T1178))
QUOT3_IN_GGA(s(s(s(s(s(s(s(s(T1205)))))))), s(s(s(s(s(s(s(s(T1210)))))))), T1178) → QUOT1514_IN_GGGA(T1205, T1210, s(s(s(s(s(s(s(T1210))))))), T1178)
QUOT1514_IN_GGGA(T1240, 0, T1241, s(T1243)) → U16_GGGA(T1240, T1241, T1243, quot3_in_gga(T1240, s(T1241), T1243))
QUOT1514_IN_GGGA(T1240, 0, T1241, s(T1243)) → QUOT3_IN_GGA(T1240, s(T1241), T1243)
QUOT1514_IN_GGGA(s(T1290), s(T1295), T1259, T1261) → U17_GGGA(T1290, T1295, T1259, T1261, quot1514_in_ggga(T1290, T1295, T1259, T1261))
QUOT1514_IN_GGGA(s(T1290), s(T1295), T1259, T1261) → QUOT1514_IN_GGGA(T1290, T1295, T1259, T1261)

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_ga(x1, x2)  =  quot52_in_ga(x1)
quot157_in_ga(x1, x2)  =  quot157_in_ga(x1)
quot297_in_ga(x1, x2)  =  quot297_in_ga(x1)
quot472_in_ga(x1, x2)  =  quot472_in_ga(x1)
quot682_in_ga(x1, x2)  =  quot682_in_ga(x1)
quot927_in_ga(x1, x2)  =  quot927_in_ga(x1)
quot1207_in_ga(x1, x2)  =  quot1207_in_ga(x1)
quot1514_in_ggga(x1, x2, x3, x4)  =  quot1514_in_ggga(x1, x2, x3)
DIV1_IN_GGA(x1, x2, x3)  =  DIV1_IN_GGA(x1, x2)
U18_GGA(x1, x2, x3, x4)  =  U18_GGA(x1, x2, x4)
QUOT3_IN_GGA(x1, x2, x3)  =  QUOT3_IN_GGA(x1, x2)
U8_GGA(x1, x2, x3)  =  U8_GGA(x1, x3)
QUOT52_IN_GA(x1, x2)  =  QUOT52_IN_GA(x1)
U1_GA(x1, x2, x3)  =  U1_GA(x1, x3)
U9_GGA(x1, x2, x3)  =  U9_GGA(x1, x3)
QUOT157_IN_GA(x1, x2)  =  QUOT157_IN_GA(x1)
U2_GA(x1, x2, x3)  =  U2_GA(x1, x3)
U10_GGA(x1, x2, x3)  =  U10_GGA(x1, x3)
QUOT297_IN_GA(x1, x2)  =  QUOT297_IN_GA(x1)
U3_GA(x1, x2, x3)  =  U3_GA(x1, x3)
U11_GGA(x1, x2, x3)  =  U11_GGA(x1, x3)
QUOT472_IN_GA(x1, x2)  =  QUOT472_IN_GA(x1)
U4_GA(x1, x2, x3)  =  U4_GA(x1, x3)
U12_GGA(x1, x2, x3)  =  U12_GGA(x1, x3)
QUOT682_IN_GA(x1, x2)  =  QUOT682_IN_GA(x1)
U5_GA(x1, x2, x3)  =  U5_GA(x1, x3)
U13_GGA(x1, x2, x3)  =  U13_GGA(x1, x3)
QUOT927_IN_GA(x1, x2)  =  QUOT927_IN_GA(x1)
U6_GA(x1, x2, x3)  =  U6_GA(x1, x3)
U14_GGA(x1, x2, x3)  =  U14_GGA(x1, x3)
QUOT1207_IN_GA(x1, x2)  =  QUOT1207_IN_GA(x1)
U7_GA(x1, x2, x3)  =  U7_GA(x1, x3)
U15_GGA(x1, x2, x3, x4)  =  U15_GGA(x1, x2, x4)
QUOT1514_IN_GGGA(x1, x2, x3, x4)  =  QUOT1514_IN_GGGA(x1, x2, x3)
U16_GGGA(x1, x2, x3, x4)  =  U16_GGGA(x1, x2, x4)
U17_GGGA(x1, x2, x3, x4, x5)  =  U17_GGGA(x1, x2, x3, x5)

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

(5) DependencyGraphProof (EQUIVALENT transformation)

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

(6) Complex Obligation (AND)

(7) Obligation:

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

QUOT1207_IN_GA(s(s(s(s(s(s(s(T1149))))))), s(T1151)) → QUOT1207_IN_GA(T1149, T1151)

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

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

(8) PiDPToQDPProof (SOUND 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:

QUOT1207_IN_GA(s(s(s(s(s(s(s(T1149)))))))) → QUOT1207_IN_GA(T1149)

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:

  • QUOT1207_IN_GA(s(s(s(s(s(s(s(T1149)))))))) → QUOT1207_IN_GA(T1149)
    The graph contains the following edges 1 > 1

(11) YES

(12) Obligation:

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

QUOT927_IN_GA(s(s(s(s(s(s(T931)))))), s(T933)) → QUOT927_IN_GA(T931, T933)

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

QUOT927_IN_GA(s(s(s(s(s(s(T931))))))) → QUOT927_IN_GA(T931)

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:

  • QUOT927_IN_GA(s(s(s(s(s(s(T931))))))) → QUOT927_IN_GA(T931)
    The graph contains the following edges 1 > 1

(16) YES

(17) Obligation:

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

QUOT682_IN_GA(s(s(s(s(s(T731))))), s(T733)) → QUOT682_IN_GA(T731, T733)

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

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

(18) PiDPToQDPProof (SOUND 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:

QUOT682_IN_GA(s(s(s(s(s(T731)))))) → QUOT682_IN_GA(T731)

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:

  • QUOT682_IN_GA(s(s(s(s(s(T731)))))) → QUOT682_IN_GA(T731)
    The graph contains the following edges 1 > 1

(21) YES

(22) Obligation:

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

QUOT472_IN_GA(s(s(s(s(T549)))), s(T551)) → QUOT472_IN_GA(T549, T551)

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

QUOT472_IN_GA(s(s(s(s(T549))))) → QUOT472_IN_GA(T549)

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:

  • QUOT472_IN_GA(s(s(s(s(T549))))) → QUOT472_IN_GA(T549)
    The graph contains the following edges 1 > 1

(26) YES

(27) Obligation:

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

QUOT297_IN_GA(s(s(s(T385))), s(T387)) → QUOT297_IN_GA(T385, T387)

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

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

(28) PiDPToQDPProof (SOUND 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:

QUOT297_IN_GA(s(s(s(T385)))) → QUOT297_IN_GA(T385)

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:

  • QUOT297_IN_GA(s(s(s(T385)))) → QUOT297_IN_GA(T385)
    The graph contains the following edges 1 > 1

(31) YES

(32) Obligation:

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

QUOT157_IN_GA(s(s(T239)), s(T241)) → QUOT157_IN_GA(T239, T241)

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

QUOT157_IN_GA(s(s(T239))) → QUOT157_IN_GA(T239)

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:

  • QUOT157_IN_GA(s(s(T239))) → QUOT157_IN_GA(T239)
    The graph contains the following edges 1 > 1

(36) YES

(37) Obligation:

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

QUOT52_IN_GA(s(T111), s(T113)) → QUOT52_IN_GA(T111, T113)

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

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

(38) PiDPToQDPProof (SOUND transformation)

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

(39) Obligation:

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

QUOT52_IN_GA(s(T111)) → QUOT52_IN_GA(T111)

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:

  • QUOT52_IN_GA(s(T111)) → QUOT52_IN_GA(T111)
    The graph contains the following edges 1 > 1

(41) YES

(42) Obligation:

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

QUOT3_IN_GGA(s(s(s(s(s(s(s(s(T1205)))))))), s(s(s(s(s(s(s(s(T1210)))))))), T1178) → QUOT1514_IN_GGGA(T1205, T1210, s(s(s(s(s(s(s(T1210))))))), T1178)
QUOT1514_IN_GGGA(T1240, 0, T1241, s(T1243)) → QUOT3_IN_GGA(T1240, s(T1241), T1243)
QUOT1514_IN_GGGA(s(T1290), s(T1295), T1259, T1261) → QUOT1514_IN_GGGA(T1290, T1295, T1259, T1261)

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)
QUOT1514_IN_GGGA(x1, x2, x3, x4)  =  QUOT1514_IN_GGGA(x1, x2, x3)

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:

QUOT3_IN_GGA(s(s(s(s(s(s(s(s(T1205)))))))), s(s(s(s(s(s(s(s(T1210))))))))) → QUOT1514_IN_GGGA(T1205, T1210, s(s(s(s(s(s(s(T1210))))))))
QUOT1514_IN_GGGA(T1240, 0, T1241) → QUOT3_IN_GGA(T1240, s(T1241))
QUOT1514_IN_GGGA(s(T1290), s(T1295), T1259) → QUOT1514_IN_GGGA(T1290, T1295, T1259)

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:

  • QUOT1514_IN_GGGA(T1240, 0, T1241) → QUOT3_IN_GGA(T1240, s(T1241))
    The graph contains the following edges 1 >= 1

  • QUOT1514_IN_GGGA(s(T1290), s(T1295), T1259) → QUOT1514_IN_GGGA(T1290, T1295, T1259)
    The graph contains the following edges 1 > 1, 2 > 2, 3 >= 3

  • QUOT3_IN_GGA(s(s(s(s(s(s(s(s(T1205)))))))), s(s(s(s(s(s(s(s(T1210))))))))) → QUOT1514_IN_GGGA(T1205, T1210, s(s(s(s(s(s(s(T1210))))))))
    The graph contains the following edges 1 > 1, 2 > 2, 2 > 3

(46) YES