(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