(0) Obligation:

Clauses:

qs([], []).
qs(.(X, Xs), Ys) :- ','(part(X, Xs, Littles, Bigs), ','(qs(Littles, Ls), ','(qs(Bigs, Bs), app(Ls, .(X, Bs), Ys)))).
part(X, .(Y, Xs), .(Y, Ls), Bs) :- ','(less(X, Y), part(X, Xs, Ls, Bs)).
part(X, .(Y, Xs), Ls, .(Y, Bs)) :- part(X, Xs, Ls, Bs).
part(X1, [], [], []).
app([], X, X).
app(.(X, Xs), Ys, .(X, Zs)) :- app(Xs, Ys, Zs).
less(0, s(X2)).
less(s(X), s(Y)) :- less(X, Y).

Queries:

qs(a,g).

(1) PrologToDTProblemTransformerProof (SOUND transformation)

Built DT problem from termination graph.

(2) Obligation:

Triples:

less13(s(T45), s(T46)) :- less13(T45, T46).
part23(T70, .(T73, T74), .(T73, X123), X124) :- less13(T70, T73).
part23(T70, .(T73, T77), .(T73, X123), X124) :- ','(lessc13(T70, T73), part23(T70, T77, X123, X124)).
part23(T95, .(T96, T98), X174, .(T96, X175)) :- part23(T95, T98, X174, X175).
part44(T148, .(T149, T150), .(T149, X282), X283) :- less13(T148, T149).
part44(T153, .(T149, T154), .(T149, X282), X283) :- ','(lessc13(T153, T149), part23(T153, T154, X282, X283)).
part44(T175, .(T173, T176), X333, .(T173, X334)) :- part44(T175, T176, X333, X334).
p43(T122, T123, X230, X231, X232, X233, X234) :- part44(T122, T123, X230, X231).
p43(T129, T123, T127, T128, X232, X233, X234) :- ','(partc44(T129, T123, T127, T128), qs60(T127, X232)).
p43(T185, T123, T127, T184, T183, X233, X234) :- ','(partc44(T185, T123, T127, T184), ','(qsc60(T127, T183), qs60(T184, X233))).
p43(T199, T123, T127, T184, T198, T197, X234) :- ','(partc44(T199, T123, T127, T184), ','(qsc60(T127, T198), ','(qsc60(T184, T197), app71(T198, T199, T197, X234)))).
qs60(.(T192, T193), X370) :- p43(T192, T193, X366, X367, X368, X369, X370).
app71(.(T222, T226), T227, T228, .(T222, X403)) :- app71(T226, T227, T228, X403).
qs39(T122, T123, X234) :- p43(T122, T123, X230, X231, X232, X233, X234).
app131(.(T433, T438), T435, T439, .(T433, T437)) :- app131(T438, T435, T439, T437).
app157(.(T542, T547), T548, T549, .(T542, T546)) :- app157(T547, T548, T549, T546).
qs1(.(T24, .(T25, T26)), []) :- less13(T24, T25).
qs1(.(T29, .(T31, T30)), []) :- ','(lessc13(T29, T31), part23(T29, T30, X49, X50)).
qs1(.(T29, .(T54, T30)), []) :- ','(lessc13(T29, T54), ','(partc23(T29, T30, T52, T53), qs39(T54, T52, X11))).
qs1(.(T29, .(T54, T30)), []) :- ','(lessc13(T29, T54), ','(partc23(T29, T30, T52, T108), ','(qsc39(T54, T52, T107), qs60(T108, X12)))).
qs1(.(T264, .(T266, T265)), []) :- part44(T264, T265, X454, X455).
qs1(.(T273, .(T272, T265)), []) :- ','(partc44(T273, T265, T270, T271), qs60(T270, X11)).
qs1(.(T280, .(T278, T265)), []) :- ','(partc44(T280, T265, T270, T279), ','(qsc60(T270, T277), qs39(T278, T279, X12))).
qs1(.(T285, .(T278, T265)), []) :- ','(partc44(T285, T265, T270, T279), ','(qsc60(T270, T284), ','(qsc39(T278, T279, T283), app94(T284, T285, T283)))).
qs1(.(T305, []), []) :- qs100(X11).
qs1(.(T305, []), []) :- ','(qsc100(T309), qs100(X12)).
qs1(.(T305, []), []) :- ','(qsc100(T309), ','(qsc100(T315), app94(T309, T305, T315))).
qs1(.(T347, .(T348, T349)), T329) :- less13(T347, T348).
qs1(.(T352, .(T354, T353)), T329) :- ','(lessc13(T352, T354), part23(T352, T353, X581, X582)).
qs1(.(T352, .(T363, T353)), T329) :- ','(lessc13(T352, T363), ','(partc23(T352, T353, T361, T362), qs39(T363, T361, X543))).
qs1(.(T352, .(T363, T353)), T329) :- ','(lessc13(T352, T363), ','(partc23(T352, T353, T361, T371), ','(qsc39(T363, T361, T370), qs60(T371, X544)))).
qs1(.(T404, .(T363, T353)), .(T402, T406)) :- ','(lessc13(T404, T363), ','(partc23(T404, T353, T361, T371), ','(qsc39(T363, T361, .(T402, T407)), ','(qsc60(T371, T408), app131(T407, T404, T408, T406))))).
qs1(.(T459, .(T461, T460)), T329) :- part44(T459, T460, X705, X706).
qs1(.(T468, .(T467, T460)), T329) :- ','(partc44(T468, T460, T465, T466), qs60(T465, X543)).
qs1(.(T476, .(T474, T460)), T329) :- ','(partc44(T476, T460, T465, T475), ','(qsc60(T465, T473), qs39(T474, T475, X544))).
qs1(.(T516, .(T474, T460)), .(T510, T514)) :- ','(partc44(T516, T460, T465, T475), ','(qsc60(T465, .(T510, T515)), ','(qsc39(T474, T475, T517), app157(T515, T516, T517, T514)))).
qs1(.(T557, []), T329) :- qs100(X543).
qs1(.(T557, []), T329) :- ','(qsc100(T560), qs100(X544)).
qs1(.(T557, []), T329) :- ','(qsc100(T560), ','(qsc100(T563), app157(T560, T557, T563, T329))).

Clauses:

lessc13(0, s(T38)).
lessc13(s(T45), s(T46)) :- lessc13(T45, T46).
partc23(T70, .(T73, T77), .(T73, X123), X124) :- ','(lessc13(T70, T73), partc23(T70, T77, X123, X124)).
partc23(T95, .(T96, T98), X174, .(T96, X175)) :- partc23(T95, T98, X174, X175).
partc23(T104, [], [], []).
partc44(T153, .(T149, T154), .(T149, X282), X283) :- ','(lessc13(T153, T149), partc23(T153, T154, X282, X283)).
partc44(T175, .(T173, T176), X333, .(T173, X334)) :- partc44(T175, T176, X333, X334).
partc44(T182, [], [], []).
qc43(T199, T123, T127, T184, T198, T197, X234) :- ','(partc44(T199, T123, T127, T184), ','(qsc60(T127, T198), ','(qsc60(T184, T197), appc71(T198, T199, T197, X234)))).
qsc60([], []).
qsc60(.(T192, T193), X370) :- qc43(T192, T193, X366, X367, X368, X369, X370).
appc71([], T212, T213, .(T212, T213)).
appc71(.(T222, T226), T227, T228, .(T222, X403)) :- appc71(T226, T227, T228, X403).
qsc39(T122, T123, X234) :- qc43(T122, T123, X230, X231, X232, X233, X234).
qsc100([]).
appc131([], T421, T422, .(T421, T422)).
appc131(.(T433, T438), T435, T439, .(T433, T437)) :- appc131(T438, T435, T439, T437).
appc157([], T530, T531, .(T530, T531)).
appc157(.(T542, T547), T548, T549, .(T542, T546)) :- appc157(T547, T548, T549, T546).

Afs:

qs1(x1, x2)  =  qs1(x2)

(3) UndefinedPredicateInTriplesTransformerProof (SOUND transformation)

Deleted triples and predicates having undefined goals [UNKNOWN].

(4) Obligation:

Triples:

less13(s(T45), s(T46)) :- less13(T45, T46).
part23(T70, .(T73, T74), .(T73, X123), X124) :- less13(T70, T73).
part23(T70, .(T73, T77), .(T73, X123), X124) :- ','(lessc13(T70, T73), part23(T70, T77, X123, X124)).
part23(T95, .(T96, T98), X174, .(T96, X175)) :- part23(T95, T98, X174, X175).
part44(T148, .(T149, T150), .(T149, X282), X283) :- less13(T148, T149).
part44(T153, .(T149, T154), .(T149, X282), X283) :- ','(lessc13(T153, T149), part23(T153, T154, X282, X283)).
part44(T175, .(T173, T176), X333, .(T173, X334)) :- part44(T175, T176, X333, X334).
p43(T122, T123, X230, X231, X232, X233, X234) :- part44(T122, T123, X230, X231).
p43(T129, T123, T127, T128, X232, X233, X234) :- ','(partc44(T129, T123, T127, T128), qs60(T127, X232)).
p43(T185, T123, T127, T184, T183, X233, X234) :- ','(partc44(T185, T123, T127, T184), ','(qsc60(T127, T183), qs60(T184, X233))).
p43(T199, T123, T127, T184, T198, T197, X234) :- ','(partc44(T199, T123, T127, T184), ','(qsc60(T127, T198), ','(qsc60(T184, T197), app71(T198, T199, T197, X234)))).
qs60(.(T192, T193), X370) :- p43(T192, T193, X366, X367, X368, X369, X370).
app71(.(T222, T226), T227, T228, .(T222, X403)) :- app71(T226, T227, T228, X403).
qs39(T122, T123, X234) :- p43(T122, T123, X230, X231, X232, X233, X234).
app131(.(T433, T438), T435, T439, .(T433, T437)) :- app131(T438, T435, T439, T437).
app157(.(T542, T547), T548, T549, .(T542, T546)) :- app157(T547, T548, T549, T546).
qs1(.(T24, .(T25, T26)), []) :- less13(T24, T25).
qs1(.(T29, .(T31, T30)), []) :- ','(lessc13(T29, T31), part23(T29, T30, X49, X50)).
qs1(.(T29, .(T54, T30)), []) :- ','(lessc13(T29, T54), ','(partc23(T29, T30, T52, T53), qs39(T54, T52, X11))).
qs1(.(T29, .(T54, T30)), []) :- ','(lessc13(T29, T54), ','(partc23(T29, T30, T52, T108), ','(qsc39(T54, T52, T107), qs60(T108, X12)))).
qs1(.(T264, .(T266, T265)), []) :- part44(T264, T265, X454, X455).
qs1(.(T273, .(T272, T265)), []) :- ','(partc44(T273, T265, T270, T271), qs60(T270, X11)).
qs1(.(T280, .(T278, T265)), []) :- ','(partc44(T280, T265, T270, T279), ','(qsc60(T270, T277), qs39(T278, T279, X12))).
qs1(.(T347, .(T348, T349)), T329) :- less13(T347, T348).
qs1(.(T352, .(T354, T353)), T329) :- ','(lessc13(T352, T354), part23(T352, T353, X581, X582)).
qs1(.(T352, .(T363, T353)), T329) :- ','(lessc13(T352, T363), ','(partc23(T352, T353, T361, T362), qs39(T363, T361, X543))).
qs1(.(T352, .(T363, T353)), T329) :- ','(lessc13(T352, T363), ','(partc23(T352, T353, T361, T371), ','(qsc39(T363, T361, T370), qs60(T371, X544)))).
qs1(.(T404, .(T363, T353)), .(T402, T406)) :- ','(lessc13(T404, T363), ','(partc23(T404, T353, T361, T371), ','(qsc39(T363, T361, .(T402, T407)), ','(qsc60(T371, T408), app131(T407, T404, T408, T406))))).
qs1(.(T459, .(T461, T460)), T329) :- part44(T459, T460, X705, X706).
qs1(.(T468, .(T467, T460)), T329) :- ','(partc44(T468, T460, T465, T466), qs60(T465, X543)).
qs1(.(T476, .(T474, T460)), T329) :- ','(partc44(T476, T460, T465, T475), ','(qsc60(T465, T473), qs39(T474, T475, X544))).
qs1(.(T516, .(T474, T460)), .(T510, T514)) :- ','(partc44(T516, T460, T465, T475), ','(qsc60(T465, .(T510, T515)), ','(qsc39(T474, T475, T517), app157(T515, T516, T517, T514)))).
qs1(.(T557, []), T329) :- ','(qsc100(T560), ','(qsc100(T563), app157(T560, T557, T563, T329))).

Clauses:

lessc13(0, s(T38)).
lessc13(s(T45), s(T46)) :- lessc13(T45, T46).
partc23(T70, .(T73, T77), .(T73, X123), X124) :- ','(lessc13(T70, T73), partc23(T70, T77, X123, X124)).
partc23(T95, .(T96, T98), X174, .(T96, X175)) :- partc23(T95, T98, X174, X175).
partc23(T104, [], [], []).
partc44(T153, .(T149, T154), .(T149, X282), X283) :- ','(lessc13(T153, T149), partc23(T153, T154, X282, X283)).
partc44(T175, .(T173, T176), X333, .(T173, X334)) :- partc44(T175, T176, X333, X334).
partc44(T182, [], [], []).
qc43(T199, T123, T127, T184, T198, T197, X234) :- ','(partc44(T199, T123, T127, T184), ','(qsc60(T127, T198), ','(qsc60(T184, T197), appc71(T198, T199, T197, X234)))).
qsc60([], []).
qsc60(.(T192, T193), X370) :- qc43(T192, T193, X366, X367, X368, X369, X370).
appc71([], T212, T213, .(T212, T213)).
appc71(.(T222, T226), T227, T228, .(T222, X403)) :- appc71(T226, T227, T228, X403).
qsc39(T122, T123, X234) :- qc43(T122, T123, X230, X231, X232, X233, X234).
qsc100([]).
appc131([], T421, T422, .(T421, T422)).
appc131(.(T433, T438), T435, T439, .(T433, T437)) :- appc131(T438, T435, T439, T437).
appc157([], T530, T531, .(T530, T531)).
appc157(.(T542, T547), T548, T549, .(T542, T546)) :- appc157(T547, T548, T549, T546).

Afs:

qs1(x1, x2)  =  qs1(x2)

(5) TriplesToPiDPProof (SOUND transformation)

We use the technique of [LOPSTR]. With regard to the inferred argument filtering the predicates were used in the following modes:
qs1_in: (f,b)
less13_in: (f,f) (b,f)
lessc13_in: (f,f) (b,f)
part23_in: (b,f,f,f)
partc23_in: (b,f,f,f)
qs39_in: (f,f,f)
p43_in: (f,f,f,f,f,f,f)
part44_in: (f,f,f,f)
partc44_in: (f,f,f,f)
qs60_in: (f,f)
qsc60_in: (f,f)
qc43_in: (f,f,f,f,f,f,f)
appc71_in: (f,f,f,f)
app71_in: (f,f,f,f)
qsc39_in: (f,f,f)
app131_in: (f,b,f,b)
app157_in: (f,f,f,b) (b,f,b,b)
Transforming TRIPLES into the following Term Rewriting System:
Pi DP problem:
The TRS P consists of the following rules:

QS1_IN_AG(.(T24, .(T25, T26)), []) → U25_AG(T24, T25, T26, less13_in_aa(T24, T25))
QS1_IN_AG(.(T24, .(T25, T26)), []) → LESS13_IN_AA(T24, T25)
LESS13_IN_AA(s(T45), s(T46)) → U1_AA(T45, T46, less13_in_aa(T45, T46))
LESS13_IN_AA(s(T45), s(T46)) → LESS13_IN_AA(T45, T46)
QS1_IN_AG(.(T29, .(T31, T30)), []) → U26_AG(T29, T31, T30, lessc13_in_aa(T29, T31))
U26_AG(T29, T31, T30, lessc13_out_aa(T29, T31)) → U27_AG(T29, T31, T30, part23_in_gaaa(T29, T30, X49, X50))
U26_AG(T29, T31, T30, lessc13_out_aa(T29, T31)) → PART23_IN_GAAA(T29, T30, X49, X50)
PART23_IN_GAAA(T70, .(T73, T74), .(T73, X123), X124) → U2_GAAA(T70, T73, T74, X123, X124, less13_in_ga(T70, T73))
PART23_IN_GAAA(T70, .(T73, T74), .(T73, X123), X124) → LESS13_IN_GA(T70, T73)
LESS13_IN_GA(s(T45), s(T46)) → U1_GA(T45, T46, less13_in_ga(T45, T46))
LESS13_IN_GA(s(T45), s(T46)) → LESS13_IN_GA(T45, T46)
PART23_IN_GAAA(T70, .(T73, T77), .(T73, X123), X124) → U3_GAAA(T70, T73, T77, X123, X124, lessc13_in_ga(T70, T73))
U3_GAAA(T70, T73, T77, X123, X124, lessc13_out_ga(T70, T73)) → U4_GAAA(T70, T73, T77, X123, X124, part23_in_gaaa(T70, T77, X123, X124))
U3_GAAA(T70, T73, T77, X123, X124, lessc13_out_ga(T70, T73)) → PART23_IN_GAAA(T70, T77, X123, X124)
PART23_IN_GAAA(T95, .(T96, T98), X174, .(T96, X175)) → U5_GAAA(T95, T96, T98, X174, X175, part23_in_gaaa(T95, T98, X174, X175))
PART23_IN_GAAA(T95, .(T96, T98), X174, .(T96, X175)) → PART23_IN_GAAA(T95, T98, X174, X175)
QS1_IN_AG(.(T29, .(T54, T30)), []) → U28_AG(T29, T54, T30, lessc13_in_aa(T29, T54))
U28_AG(T29, T54, T30, lessc13_out_aa(T29, T54)) → U29_AG(T29, T54, T30, partc23_in_gaaa(T29, T30, T52, T53))
U29_AG(T29, T54, T30, partc23_out_gaaa(T29, T30, T52, T53)) → U30_AG(T29, T54, T30, qs39_in_aaa(T54, T52, X11))
U29_AG(T29, T54, T30, partc23_out_gaaa(T29, T30, T52, T53)) → QS39_IN_AAA(T54, T52, X11)
QS39_IN_AAA(T122, T123, X234) → U22_AAA(T122, T123, X234, p43_in_aaaaaaa(T122, T123, X230, X231, X232, X233, X234))
QS39_IN_AAA(T122, T123, X234) → P43_IN_AAAAAAA(T122, T123, X230, X231, X232, X233, X234)
P43_IN_AAAAAAA(T122, T123, X230, X231, X232, X233, X234) → U10_AAAAAAA(T122, T123, X230, X231, X232, X233, X234, part44_in_aaaa(T122, T123, X230, X231))
P43_IN_AAAAAAA(T122, T123, X230, X231, X232, X233, X234) → PART44_IN_AAAA(T122, T123, X230, X231)
PART44_IN_AAAA(T148, .(T149, T150), .(T149, X282), X283) → U6_AAAA(T148, T149, T150, X282, X283, less13_in_aa(T148, T149))
PART44_IN_AAAA(T148, .(T149, T150), .(T149, X282), X283) → LESS13_IN_AA(T148, T149)
PART44_IN_AAAA(T153, .(T149, T154), .(T149, X282), X283) → U7_AAAA(T153, T149, T154, X282, X283, lessc13_in_aa(T153, T149))
U7_AAAA(T153, T149, T154, X282, X283, lessc13_out_aa(T153, T149)) → U8_AAAA(T153, T149, T154, X282, X283, part23_in_gaaa(T153, T154, X282, X283))
U7_AAAA(T153, T149, T154, X282, X283, lessc13_out_aa(T153, T149)) → PART23_IN_GAAA(T153, T154, X282, X283)
PART44_IN_AAAA(T175, .(T173, T176), X333, .(T173, X334)) → U9_AAAA(T175, T173, T176, X333, X334, part44_in_aaaa(T175, T176, X333, X334))
PART44_IN_AAAA(T175, .(T173, T176), X333, .(T173, X334)) → PART44_IN_AAAA(T175, T176, X333, X334)
P43_IN_AAAAAAA(T129, T123, T127, T128, X232, X233, X234) → U11_AAAAAAA(T129, T123, T127, T128, X232, X233, X234, partc44_in_aaaa(T129, T123, T127, T128))
U11_AAAAAAA(T129, T123, T127, T128, X232, X233, X234, partc44_out_aaaa(T129, T123, T127, T128)) → U12_AAAAAAA(T129, T123, T127, T128, X232, X233, X234, qs60_in_aa(T127, X232))
U11_AAAAAAA(T129, T123, T127, T128, X232, X233, X234, partc44_out_aaaa(T129, T123, T127, T128)) → QS60_IN_AA(T127, X232)
QS60_IN_AA(.(T192, T193), X370) → U20_AA(T192, T193, X370, p43_in_aaaaaaa(T192, T193, X366, X367, X368, X369, X370))
QS60_IN_AA(.(T192, T193), X370) → P43_IN_AAAAAAA(T192, T193, X366, X367, X368, X369, X370)
P43_IN_AAAAAAA(T185, T123, T127, T184, T183, X233, X234) → U13_AAAAAAA(T185, T123, T127, T184, T183, X233, X234, partc44_in_aaaa(T185, T123, T127, T184))
U13_AAAAAAA(T185, T123, T127, T184, T183, X233, X234, partc44_out_aaaa(T185, T123, T127, T184)) → U14_AAAAAAA(T185, T123, T127, T184, T183, X233, X234, qsc60_in_aa(T127, T183))
U14_AAAAAAA(T185, T123, T127, T184, T183, X233, X234, qsc60_out_aa(T127, T183)) → U15_AAAAAAA(T185, T123, T127, T184, T183, X233, X234, qs60_in_aa(T184, X233))
U14_AAAAAAA(T185, T123, T127, T184, T183, X233, X234, qsc60_out_aa(T127, T183)) → QS60_IN_AA(T184, X233)
P43_IN_AAAAAAA(T199, T123, T127, T184, T198, T197, X234) → U16_AAAAAAA(T199, T123, T127, T184, T198, T197, X234, partc44_in_aaaa(T199, T123, T127, T184))
U16_AAAAAAA(T199, T123, T127, T184, T198, T197, X234, partc44_out_aaaa(T199, T123, T127, T184)) → U17_AAAAAAA(T199, T123, T127, T184, T198, T197, X234, qsc60_in_aa(T127, T198))
U17_AAAAAAA(T199, T123, T127, T184, T198, T197, X234, qsc60_out_aa(T127, T198)) → U18_AAAAAAA(T199, T123, T127, T184, T198, T197, X234, qsc60_in_aa(T184, T197))
U18_AAAAAAA(T199, T123, T127, T184, T198, T197, X234, qsc60_out_aa(T184, T197)) → U19_AAAAAAA(T199, T123, T127, T184, T198, T197, X234, app71_in_aaaa(T198, T199, T197, X234))
U18_AAAAAAA(T199, T123, T127, T184, T198, T197, X234, qsc60_out_aa(T184, T197)) → APP71_IN_AAAA(T198, T199, T197, X234)
APP71_IN_AAAA(.(T222, T226), T227, T228, .(T222, X403)) → U21_AAAA(T222, T226, T227, T228, X403, app71_in_aaaa(T226, T227, T228, X403))
APP71_IN_AAAA(.(T222, T226), T227, T228, .(T222, X403)) → APP71_IN_AAAA(T226, T227, T228, X403)
U28_AG(T29, T54, T30, lessc13_out_aa(T29, T54)) → U31_AG(T29, T54, T30, partc23_in_gaaa(T29, T30, T52, T108))
U31_AG(T29, T54, T30, partc23_out_gaaa(T29, T30, T52, T108)) → U32_AG(T29, T54, T30, T108, qsc39_in_aaa(T54, T52, T107))
U32_AG(T29, T54, T30, T108, qsc39_out_aaa(T54, T52, T107)) → U33_AG(T29, T54, T30, qs60_in_aa(T108, X12))
U32_AG(T29, T54, T30, T108, qsc39_out_aaa(T54, T52, T107)) → QS60_IN_AA(T108, X12)
QS1_IN_AG(.(T264, .(T266, T265)), []) → U34_AG(T264, T266, T265, part44_in_aaaa(T264, T265, X454, X455))
QS1_IN_AG(.(T264, .(T266, T265)), []) → PART44_IN_AAAA(T264, T265, X454, X455)
QS1_IN_AG(.(T273, .(T272, T265)), []) → U35_AG(T273, T272, T265, partc44_in_aaaa(T273, T265, T270, T271))
U35_AG(T273, T272, T265, partc44_out_aaaa(T273, T265, T270, T271)) → U36_AG(T273, T272, T265, qs60_in_aa(T270, X11))
U35_AG(T273, T272, T265, partc44_out_aaaa(T273, T265, T270, T271)) → QS60_IN_AA(T270, X11)
QS1_IN_AG(.(T280, .(T278, T265)), []) → U37_AG(T280, T278, T265, partc44_in_aaaa(T280, T265, T270, T279))
U37_AG(T280, T278, T265, partc44_out_aaaa(T280, T265, T270, T279)) → U38_AG(T280, T278, T265, T279, qsc60_in_aa(T270, T277))
U38_AG(T280, T278, T265, T279, qsc60_out_aa(T270, T277)) → U39_AG(T280, T278, T265, qs39_in_aaa(T278, T279, X12))
U38_AG(T280, T278, T265, T279, qsc60_out_aa(T270, T277)) → QS39_IN_AAA(T278, T279, X12)
QS1_IN_AG(.(T347, .(T348, T349)), T329) → U40_AG(T347, T348, T349, T329, less13_in_aa(T347, T348))
QS1_IN_AG(.(T347, .(T348, T349)), T329) → LESS13_IN_AA(T347, T348)
QS1_IN_AG(.(T352, .(T354, T353)), T329) → U41_AG(T352, T354, T353, T329, lessc13_in_aa(T352, T354))
U41_AG(T352, T354, T353, T329, lessc13_out_aa(T352, T354)) → U42_AG(T352, T354, T353, T329, part23_in_gaaa(T352, T353, X581, X582))
U41_AG(T352, T354, T353, T329, lessc13_out_aa(T352, T354)) → PART23_IN_GAAA(T352, T353, X581, X582)
QS1_IN_AG(.(T352, .(T363, T353)), T329) → U43_AG(T352, T363, T353, T329, lessc13_in_aa(T352, T363))
U43_AG(T352, T363, T353, T329, lessc13_out_aa(T352, T363)) → U44_AG(T352, T363, T353, T329, partc23_in_gaaa(T352, T353, T361, T362))
U44_AG(T352, T363, T353, T329, partc23_out_gaaa(T352, T353, T361, T362)) → U45_AG(T352, T363, T353, T329, qs39_in_aaa(T363, T361, X543))
U44_AG(T352, T363, T353, T329, partc23_out_gaaa(T352, T353, T361, T362)) → QS39_IN_AAA(T363, T361, X543)
U43_AG(T352, T363, T353, T329, lessc13_out_aa(T352, T363)) → U46_AG(T352, T363, T353, T329, partc23_in_gaaa(T352, T353, T361, T371))
U46_AG(T352, T363, T353, T329, partc23_out_gaaa(T352, T353, T361, T371)) → U47_AG(T352, T363, T353, T329, T371, qsc39_in_aaa(T363, T361, T370))
U47_AG(T352, T363, T353, T329, T371, qsc39_out_aaa(T363, T361, T370)) → U48_AG(T352, T363, T353, T329, qs60_in_aa(T371, X544))
U47_AG(T352, T363, T353, T329, T371, qsc39_out_aaa(T363, T361, T370)) → QS60_IN_AA(T371, X544)
QS1_IN_AG(.(T404, .(T363, T353)), .(T402, T406)) → U49_AG(T404, T363, T353, T402, T406, lessc13_in_aa(T404, T363))
U49_AG(T404, T363, T353, T402, T406, lessc13_out_aa(T404, T363)) → U50_AG(T404, T363, T353, T402, T406, partc23_in_gaaa(T404, T353, T361, T371))
U50_AG(T404, T363, T353, T402, T406, partc23_out_gaaa(T404, T353, T361, T371)) → U51_AG(T404, T363, T353, T402, T406, T371, qsc39_in_aaa(T363, T361, .(T402, T407)))
U51_AG(T404, T363, T353, T402, T406, T371, qsc39_out_aaa(T363, T361, .(T402, T407))) → U52_AG(T404, T363, T353, T402, T406, T407, qsc60_in_aa(T371, T408))
U52_AG(T404, T363, T353, T402, T406, T407, qsc60_out_aa(T371, T408)) → U53_AG(T404, T363, T353, T402, T406, app131_in_agag(T407, T404, T408, T406))
U52_AG(T404, T363, T353, T402, T406, T407, qsc60_out_aa(T371, T408)) → APP131_IN_AGAG(T407, T404, T408, T406)
APP131_IN_AGAG(.(T433, T438), T435, T439, .(T433, T437)) → U23_AGAG(T433, T438, T435, T439, T437, app131_in_agag(T438, T435, T439, T437))
APP131_IN_AGAG(.(T433, T438), T435, T439, .(T433, T437)) → APP131_IN_AGAG(T438, T435, T439, T437)
QS1_IN_AG(.(T459, .(T461, T460)), T329) → U54_AG(T459, T461, T460, T329, part44_in_aaaa(T459, T460, X705, X706))
QS1_IN_AG(.(T459, .(T461, T460)), T329) → PART44_IN_AAAA(T459, T460, X705, X706)
QS1_IN_AG(.(T468, .(T467, T460)), T329) → U55_AG(T468, T467, T460, T329, partc44_in_aaaa(T468, T460, T465, T466))
U55_AG(T468, T467, T460, T329, partc44_out_aaaa(T468, T460, T465, T466)) → U56_AG(T468, T467, T460, T329, qs60_in_aa(T465, X543))
U55_AG(T468, T467, T460, T329, partc44_out_aaaa(T468, T460, T465, T466)) → QS60_IN_AA(T465, X543)
QS1_IN_AG(.(T476, .(T474, T460)), T329) → U57_AG(T476, T474, T460, T329, partc44_in_aaaa(T476, T460, T465, T475))
U57_AG(T476, T474, T460, T329, partc44_out_aaaa(T476, T460, T465, T475)) → U58_AG(T476, T474, T460, T329, T475, qsc60_in_aa(T465, T473))
U58_AG(T476, T474, T460, T329, T475, qsc60_out_aa(T465, T473)) → U59_AG(T476, T474, T460, T329, qs39_in_aaa(T474, T475, X544))
U58_AG(T476, T474, T460, T329, T475, qsc60_out_aa(T465, T473)) → QS39_IN_AAA(T474, T475, X544)
QS1_IN_AG(.(T516, .(T474, T460)), .(T510, T514)) → U60_AG(T516, T474, T460, T510, T514, partc44_in_aaaa(T516, T460, T465, T475))
U60_AG(T516, T474, T460, T510, T514, partc44_out_aaaa(T516, T460, T465, T475)) → U61_AG(T516, T474, T460, T510, T514, T475, qsc60_in_aa(T465, .(T510, T515)))
U61_AG(T516, T474, T460, T510, T514, T475, qsc60_out_aa(T465, .(T510, T515))) → U62_AG(T516, T474, T460, T510, T514, T515, qsc39_in_aaa(T474, T475, T517))
U62_AG(T516, T474, T460, T510, T514, T515, qsc39_out_aaa(T474, T475, T517)) → U63_AG(T516, T474, T460, T510, T514, app157_in_aaag(T515, T516, T517, T514))
U62_AG(T516, T474, T460, T510, T514, T515, qsc39_out_aaa(T474, T475, T517)) → APP157_IN_AAAG(T515, T516, T517, T514)
APP157_IN_AAAG(.(T542, T547), T548, T549, .(T542, T546)) → U24_AAAG(T542, T547, T548, T549, T546, app157_in_aaag(T547, T548, T549, T546))
APP157_IN_AAAG(.(T542, T547), T548, T549, .(T542, T546)) → APP157_IN_AAAG(T547, T548, T549, T546)
QS1_IN_AG(.(T557, []), T329) → U64_AG(T557, T329, qsc100_in_a(T560))
U64_AG(T557, T329, qsc100_out_a(T560)) → U65_AG(T557, T329, T560, qsc100_in_a(T563))
U65_AG(T557, T329, T560, qsc100_out_a(T563)) → U66_AG(T557, T329, app157_in_gagg(T560, T557, T563, T329))
U65_AG(T557, T329, T560, qsc100_out_a(T563)) → APP157_IN_GAGG(T560, T557, T563, T329)
APP157_IN_GAGG(.(T542, T547), T548, T549, .(T542, T546)) → U24_GAGG(T542, T547, T548, T549, T546, app157_in_gagg(T547, T548, T549, T546))
APP157_IN_GAGG(.(T542, T547), T548, T549, .(T542, T546)) → APP157_IN_GAGG(T547, T548, T549, T546)

The TRS R consists of the following rules:

lessc13_in_aa(0, s(T38)) → lessc13_out_aa(0, s(T38))
lessc13_in_aa(s(T45), s(T46)) → U68_aa(T45, T46, lessc13_in_aa(T45, T46))
U68_aa(T45, T46, lessc13_out_aa(T45, T46)) → lessc13_out_aa(s(T45), s(T46))
lessc13_in_ga(0, s(T38)) → lessc13_out_ga(0, s(T38))
lessc13_in_ga(s(T45), s(T46)) → U68_ga(T45, T46, lessc13_in_ga(T45, T46))
U68_ga(T45, T46, lessc13_out_ga(T45, T46)) → lessc13_out_ga(s(T45), s(T46))
partc23_in_gaaa(T70, .(T73, T77), .(T73, X123), X124) → U69_gaaa(T70, T73, T77, X123, X124, lessc13_in_ga(T70, T73))
U69_gaaa(T70, T73, T77, X123, X124, lessc13_out_ga(T70, T73)) → U70_gaaa(T70, T73, T77, X123, X124, partc23_in_gaaa(T70, T77, X123, X124))
partc23_in_gaaa(T95, .(T96, T98), X174, .(T96, X175)) → U71_gaaa(T95, T96, T98, X174, X175, partc23_in_gaaa(T95, T98, X174, X175))
partc23_in_gaaa(T104, [], [], []) → partc23_out_gaaa(T104, [], [], [])
U71_gaaa(T95, T96, T98, X174, X175, partc23_out_gaaa(T95, T98, X174, X175)) → partc23_out_gaaa(T95, .(T96, T98), X174, .(T96, X175))
U70_gaaa(T70, T73, T77, X123, X124, partc23_out_gaaa(T70, T77, X123, X124)) → partc23_out_gaaa(T70, .(T73, T77), .(T73, X123), X124)
partc44_in_aaaa(T153, .(T149, T154), .(T149, X282), X283) → U72_aaaa(T153, T149, T154, X282, X283, lessc13_in_aa(T153, T149))
U72_aaaa(T153, T149, T154, X282, X283, lessc13_out_aa(T153, T149)) → U73_aaaa(T153, T149, T154, X282, X283, partc23_in_gaaa(T153, T154, X282, X283))
U73_aaaa(T153, T149, T154, X282, X283, partc23_out_gaaa(T153, T154, X282, X283)) → partc44_out_aaaa(T153, .(T149, T154), .(T149, X282), X283)
partc44_in_aaaa(T175, .(T173, T176), X333, .(T173, X334)) → U74_aaaa(T175, T173, T176, X333, X334, partc44_in_aaaa(T175, T176, X333, X334))
partc44_in_aaaa(T182, [], [], []) → partc44_out_aaaa(T182, [], [], [])
U74_aaaa(T175, T173, T176, X333, X334, partc44_out_aaaa(T175, T176, X333, X334)) → partc44_out_aaaa(T175, .(T173, T176), X333, .(T173, X334))
qsc60_in_aa([], []) → qsc60_out_aa([], [])
qsc60_in_aa(.(T192, T193), X370) → U79_aa(T192, T193, X370, qc43_in_aaaaaaa(T192, T193, X366, X367, X368, X369, X370))
qc43_in_aaaaaaa(T199, T123, T127, T184, T198, T197, X234) → U75_aaaaaaa(T199, T123, T127, T184, T198, T197, X234, partc44_in_aaaa(T199, T123, T127, T184))
U75_aaaaaaa(T199, T123, T127, T184, T198, T197, X234, partc44_out_aaaa(T199, T123, T127, T184)) → U76_aaaaaaa(T199, T123, T127, T184, T198, T197, X234, qsc60_in_aa(T127, T198))
U76_aaaaaaa(T199, T123, T127, T184, T198, T197, X234, qsc60_out_aa(T127, T198)) → U77_aaaaaaa(T199, T123, T127, T184, T198, T197, X234, qsc60_in_aa(T184, T197))
U77_aaaaaaa(T199, T123, T127, T184, T198, T197, X234, qsc60_out_aa(T184, T197)) → U78_aaaaaaa(T199, T123, T127, T184, T198, T197, X234, appc71_in_aaaa(T198, T199, T197, X234))
appc71_in_aaaa([], T212, T213, .(T212, T213)) → appc71_out_aaaa([], T212, T213, .(T212, T213))
appc71_in_aaaa(.(T222, T226), T227, T228, .(T222, X403)) → U80_aaaa(T222, T226, T227, T228, X403, appc71_in_aaaa(T226, T227, T228, X403))
U80_aaaa(T222, T226, T227, T228, X403, appc71_out_aaaa(T226, T227, T228, X403)) → appc71_out_aaaa(.(T222, T226), T227, T228, .(T222, X403))
U78_aaaaaaa(T199, T123, T127, T184, T198, T197, X234, appc71_out_aaaa(T198, T199, T197, X234)) → qc43_out_aaaaaaa(T199, T123, T127, T184, T198, T197, X234)
U79_aa(T192, T193, X370, qc43_out_aaaaaaa(T192, T193, X366, X367, X368, X369, X370)) → qsc60_out_aa(.(T192, T193), X370)
qsc39_in_aaa(T122, T123, X234) → U81_aaa(T122, T123, X234, qc43_in_aaaaaaa(T122, T123, X230, X231, X232, X233, X234))
U81_aaa(T122, T123, X234, qc43_out_aaaaaaa(T122, T123, X230, X231, X232, X233, X234)) → qsc39_out_aaa(T122, T123, X234)
qsc100_in_a([]) → qsc100_out_a([])

The argument filtering Pi contains the following mapping:
[]  =  []
less13_in_aa(x1, x2)  =  less13_in_aa
lessc13_in_aa(x1, x2)  =  lessc13_in_aa
lessc13_out_aa(x1, x2)  =  lessc13_out_aa(x1)
U68_aa(x1, x2, x3)  =  U68_aa(x3)
part23_in_gaaa(x1, x2, x3, x4)  =  part23_in_gaaa(x1)
less13_in_ga(x1, x2)  =  less13_in_ga(x1)
s(x1)  =  s(x1)
lessc13_in_ga(x1, x2)  =  lessc13_in_ga(x1)
0  =  0
lessc13_out_ga(x1, x2)  =  lessc13_out_ga(x1)
U68_ga(x1, x2, x3)  =  U68_ga(x1, x3)
partc23_in_gaaa(x1, x2, x3, x4)  =  partc23_in_gaaa(x1)
U69_gaaa(x1, x2, x3, x4, x5, x6)  =  U69_gaaa(x1, x6)
U70_gaaa(x1, x2, x3, x4, x5, x6)  =  U70_gaaa(x1, x6)
U71_gaaa(x1, x2, x3, x4, x5, x6)  =  U71_gaaa(x1, x6)
partc23_out_gaaa(x1, x2, x3, x4)  =  partc23_out_gaaa(x1)
qs39_in_aaa(x1, x2, x3)  =  qs39_in_aaa
p43_in_aaaaaaa(x1, x2, x3, x4, x5, x6, x7)  =  p43_in_aaaaaaa
part44_in_aaaa(x1, x2, x3, x4)  =  part44_in_aaaa
partc44_in_aaaa(x1, x2, x3, x4)  =  partc44_in_aaaa
U72_aaaa(x1, x2, x3, x4, x5, x6)  =  U72_aaaa(x6)
U73_aaaa(x1, x2, x3, x4, x5, x6)  =  U73_aaaa(x6)
partc44_out_aaaa(x1, x2, x3, x4)  =  partc44_out_aaaa
U74_aaaa(x1, x2, x3, x4, x5, x6)  =  U74_aaaa(x6)
qs60_in_aa(x1, x2)  =  qs60_in_aa
qsc60_in_aa(x1, x2)  =  qsc60_in_aa
qsc60_out_aa(x1, x2)  =  qsc60_out_aa
U79_aa(x1, x2, x3, x4)  =  U79_aa(x4)
qc43_in_aaaaaaa(x1, x2, x3, x4, x5, x6, x7)  =  qc43_in_aaaaaaa
U75_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  U75_aaaaaaa(x8)
U76_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  U76_aaaaaaa(x8)
U77_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  U77_aaaaaaa(x8)
U78_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  U78_aaaaaaa(x8)
.(x1, x2)  =  .(x1, x2)
qc43_out_aaaaaaa(x1, x2, x3, x4, x5, x6, x7)  =  qc43_out_aaaaaaa
appc71_in_aaaa(x1, x2, x3, x4)  =  appc71_in_aaaa
appc71_out_aaaa(x1, x2, x3, x4)  =  appc71_out_aaaa
U80_aaaa(x1, x2, x3, x4, x5, x6)  =  U80_aaaa(x6)
app71_in_aaaa(x1, x2, x3, x4)  =  app71_in_aaaa
qsc39_in_aaa(x1, x2, x3)  =  qsc39_in_aaa
U81_aaa(x1, x2, x3, x4)  =  U81_aaa(x4)
qsc39_out_aaa(x1, x2, x3)  =  qsc39_out_aaa
app131_in_agag(x1, x2, x3, x4)  =  app131_in_agag(x2, x4)
app157_in_aaag(x1, x2, x3, x4)  =  app157_in_aaag(x4)
qsc100_in_a(x1)  =  qsc100_in_a
qsc100_out_a(x1)  =  qsc100_out_a(x1)
app157_in_gagg(x1, x2, x3, x4)  =  app157_in_gagg(x1, x3, x4)
QS1_IN_AG(x1, x2)  =  QS1_IN_AG(x2)
U25_AG(x1, x2, x3, x4)  =  U25_AG(x4)
LESS13_IN_AA(x1, x2)  =  LESS13_IN_AA
U1_AA(x1, x2, x3)  =  U1_AA(x3)
U26_AG(x1, x2, x3, x4)  =  U26_AG(x4)
U27_AG(x1, x2, x3, x4)  =  U27_AG(x4)
PART23_IN_GAAA(x1, x2, x3, x4)  =  PART23_IN_GAAA(x1)
U2_GAAA(x1, x2, x3, x4, x5, x6)  =  U2_GAAA(x1, x6)
LESS13_IN_GA(x1, x2)  =  LESS13_IN_GA(x1)
U1_GA(x1, x2, x3)  =  U1_GA(x1, x3)
U3_GAAA(x1, x2, x3, x4, x5, x6)  =  U3_GAAA(x1, x6)
U4_GAAA(x1, x2, x3, x4, x5, x6)  =  U4_GAAA(x1, x6)
U5_GAAA(x1, x2, x3, x4, x5, x6)  =  U5_GAAA(x1, x6)
U28_AG(x1, x2, x3, x4)  =  U28_AG(x4)
U29_AG(x1, x2, x3, x4)  =  U29_AG(x4)
U30_AG(x1, x2, x3, x4)  =  U30_AG(x4)
QS39_IN_AAA(x1, x2, x3)  =  QS39_IN_AAA
U22_AAA(x1, x2, x3, x4)  =  U22_AAA(x4)
P43_IN_AAAAAAA(x1, x2, x3, x4, x5, x6, x7)  =  P43_IN_AAAAAAA
U10_AAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8)  =  U10_AAAAAAA(x8)
PART44_IN_AAAA(x1, x2, x3, x4)  =  PART44_IN_AAAA
U6_AAAA(x1, x2, x3, x4, x5, x6)  =  U6_AAAA(x6)
U7_AAAA(x1, x2, x3, x4, x5, x6)  =  U7_AAAA(x6)
U8_AAAA(x1, x2, x3, x4, x5, x6)  =  U8_AAAA(x1, x6)
U9_AAAA(x1, x2, x3, x4, x5, x6)  =  U9_AAAA(x6)
U11_AAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8)  =  U11_AAAAAAA(x8)
U12_AAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8)  =  U12_AAAAAAA(x8)
QS60_IN_AA(x1, x2)  =  QS60_IN_AA
U20_AA(x1, x2, x3, x4)  =  U20_AA(x4)
U13_AAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8)  =  U13_AAAAAAA(x8)
U14_AAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8)  =  U14_AAAAAAA(x8)
U15_AAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8)  =  U15_AAAAAAA(x8)
U16_AAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8)  =  U16_AAAAAAA(x8)
U17_AAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8)  =  U17_AAAAAAA(x8)
U18_AAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8)  =  U18_AAAAAAA(x8)
U19_AAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8)  =  U19_AAAAAAA(x8)
APP71_IN_AAAA(x1, x2, x3, x4)  =  APP71_IN_AAAA
U21_AAAA(x1, x2, x3, x4, x5, x6)  =  U21_AAAA(x6)
U31_AG(x1, x2, x3, x4)  =  U31_AG(x4)
U32_AG(x1, x2, x3, x4, x5)  =  U32_AG(x5)
U33_AG(x1, x2, x3, x4)  =  U33_AG(x4)
U34_AG(x1, x2, x3, x4)  =  U34_AG(x4)
U35_AG(x1, x2, x3, x4)  =  U35_AG(x4)
U36_AG(x1, x2, x3, x4)  =  U36_AG(x4)
U37_AG(x1, x2, x3, x4)  =  U37_AG(x4)
U38_AG(x1, x2, x3, x4, x5)  =  U38_AG(x5)
U39_AG(x1, x2, x3, x4)  =  U39_AG(x4)
U40_AG(x1, x2, x3, x4, x5)  =  U40_AG(x4, x5)
U41_AG(x1, x2, x3, x4, x5)  =  U41_AG(x4, x5)
U42_AG(x1, x2, x3, x4, x5)  =  U42_AG(x4, x5)
U43_AG(x1, x2, x3, x4, x5)  =  U43_AG(x4, x5)
U44_AG(x1, x2, x3, x4, x5)  =  U44_AG(x4, x5)
U45_AG(x1, x2, x3, x4, x5)  =  U45_AG(x4, x5)
U46_AG(x1, x2, x3, x4, x5)  =  U46_AG(x4, x5)
U47_AG(x1, x2, x3, x4, x5, x6)  =  U47_AG(x4, x6)
U48_AG(x1, x2, x3, x4, x5)  =  U48_AG(x4, x5)
U49_AG(x1, x2, x3, x4, x5, x6)  =  U49_AG(x4, x5, x6)
U50_AG(x1, x2, x3, x4, x5, x6)  =  U50_AG(x1, x4, x5, x6)
U51_AG(x1, x2, x3, x4, x5, x6, x7)  =  U51_AG(x1, x4, x5, x7)
U52_AG(x1, x2, x3, x4, x5, x6, x7)  =  U52_AG(x1, x4, x5, x7)
U53_AG(x1, x2, x3, x4, x5, x6)  =  U53_AG(x4, x5, x6)
APP131_IN_AGAG(x1, x2, x3, x4)  =  APP131_IN_AGAG(x2, x4)
U23_AGAG(x1, x2, x3, x4, x5, x6)  =  U23_AGAG(x1, x3, x5, x6)
U54_AG(x1, x2, x3, x4, x5)  =  U54_AG(x4, x5)
U55_AG(x1, x2, x3, x4, x5)  =  U55_AG(x4, x5)
U56_AG(x1, x2, x3, x4, x5)  =  U56_AG(x4, x5)
U57_AG(x1, x2, x3, x4, x5)  =  U57_AG(x4, x5)
U58_AG(x1, x2, x3, x4, x5, x6)  =  U58_AG(x4, x6)
U59_AG(x1, x2, x3, x4, x5)  =  U59_AG(x4, x5)
U60_AG(x1, x2, x3, x4, x5, x6)  =  U60_AG(x4, x5, x6)
U61_AG(x1, x2, x3, x4, x5, x6, x7)  =  U61_AG(x4, x5, x7)
U62_AG(x1, x2, x3, x4, x5, x6, x7)  =  U62_AG(x4, x5, x7)
U63_AG(x1, x2, x3, x4, x5, x6)  =  U63_AG(x4, x5, x6)
APP157_IN_AAAG(x1, x2, x3, x4)  =  APP157_IN_AAAG(x4)
U24_AAAG(x1, x2, x3, x4, x5, x6)  =  U24_AAAG(x1, x5, x6)
U64_AG(x1, x2, x3)  =  U64_AG(x2, x3)
U65_AG(x1, x2, x3, x4)  =  U65_AG(x2, x3, x4)
U66_AG(x1, x2, x3)  =  U66_AG(x2, x3)
APP157_IN_GAGG(x1, x2, x3, x4)  =  APP157_IN_GAGG(x1, x3, x4)
U24_GAGG(x1, x2, x3, x4, x5, x6)  =  U24_GAGG(x1, x2, x4, x5, x6)

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

Infinitary Constructor Rewriting Termination of PiDP implies Termination of TRIPLES

(6) Obligation:

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

QS1_IN_AG(.(T24, .(T25, T26)), []) → U25_AG(T24, T25, T26, less13_in_aa(T24, T25))
QS1_IN_AG(.(T24, .(T25, T26)), []) → LESS13_IN_AA(T24, T25)
LESS13_IN_AA(s(T45), s(T46)) → U1_AA(T45, T46, less13_in_aa(T45, T46))
LESS13_IN_AA(s(T45), s(T46)) → LESS13_IN_AA(T45, T46)
QS1_IN_AG(.(T29, .(T31, T30)), []) → U26_AG(T29, T31, T30, lessc13_in_aa(T29, T31))
U26_AG(T29, T31, T30, lessc13_out_aa(T29, T31)) → U27_AG(T29, T31, T30, part23_in_gaaa(T29, T30, X49, X50))
U26_AG(T29, T31, T30, lessc13_out_aa(T29, T31)) → PART23_IN_GAAA(T29, T30, X49, X50)
PART23_IN_GAAA(T70, .(T73, T74), .(T73, X123), X124) → U2_GAAA(T70, T73, T74, X123, X124, less13_in_ga(T70, T73))
PART23_IN_GAAA(T70, .(T73, T74), .(T73, X123), X124) → LESS13_IN_GA(T70, T73)
LESS13_IN_GA(s(T45), s(T46)) → U1_GA(T45, T46, less13_in_ga(T45, T46))
LESS13_IN_GA(s(T45), s(T46)) → LESS13_IN_GA(T45, T46)
PART23_IN_GAAA(T70, .(T73, T77), .(T73, X123), X124) → U3_GAAA(T70, T73, T77, X123, X124, lessc13_in_ga(T70, T73))
U3_GAAA(T70, T73, T77, X123, X124, lessc13_out_ga(T70, T73)) → U4_GAAA(T70, T73, T77, X123, X124, part23_in_gaaa(T70, T77, X123, X124))
U3_GAAA(T70, T73, T77, X123, X124, lessc13_out_ga(T70, T73)) → PART23_IN_GAAA(T70, T77, X123, X124)
PART23_IN_GAAA(T95, .(T96, T98), X174, .(T96, X175)) → U5_GAAA(T95, T96, T98, X174, X175, part23_in_gaaa(T95, T98, X174, X175))
PART23_IN_GAAA(T95, .(T96, T98), X174, .(T96, X175)) → PART23_IN_GAAA(T95, T98, X174, X175)
QS1_IN_AG(.(T29, .(T54, T30)), []) → U28_AG(T29, T54, T30, lessc13_in_aa(T29, T54))
U28_AG(T29, T54, T30, lessc13_out_aa(T29, T54)) → U29_AG(T29, T54, T30, partc23_in_gaaa(T29, T30, T52, T53))
U29_AG(T29, T54, T30, partc23_out_gaaa(T29, T30, T52, T53)) → U30_AG(T29, T54, T30, qs39_in_aaa(T54, T52, X11))
U29_AG(T29, T54, T30, partc23_out_gaaa(T29, T30, T52, T53)) → QS39_IN_AAA(T54, T52, X11)
QS39_IN_AAA(T122, T123, X234) → U22_AAA(T122, T123, X234, p43_in_aaaaaaa(T122, T123, X230, X231, X232, X233, X234))
QS39_IN_AAA(T122, T123, X234) → P43_IN_AAAAAAA(T122, T123, X230, X231, X232, X233, X234)
P43_IN_AAAAAAA(T122, T123, X230, X231, X232, X233, X234) → U10_AAAAAAA(T122, T123, X230, X231, X232, X233, X234, part44_in_aaaa(T122, T123, X230, X231))
P43_IN_AAAAAAA(T122, T123, X230, X231, X232, X233, X234) → PART44_IN_AAAA(T122, T123, X230, X231)
PART44_IN_AAAA(T148, .(T149, T150), .(T149, X282), X283) → U6_AAAA(T148, T149, T150, X282, X283, less13_in_aa(T148, T149))
PART44_IN_AAAA(T148, .(T149, T150), .(T149, X282), X283) → LESS13_IN_AA(T148, T149)
PART44_IN_AAAA(T153, .(T149, T154), .(T149, X282), X283) → U7_AAAA(T153, T149, T154, X282, X283, lessc13_in_aa(T153, T149))
U7_AAAA(T153, T149, T154, X282, X283, lessc13_out_aa(T153, T149)) → U8_AAAA(T153, T149, T154, X282, X283, part23_in_gaaa(T153, T154, X282, X283))
U7_AAAA(T153, T149, T154, X282, X283, lessc13_out_aa(T153, T149)) → PART23_IN_GAAA(T153, T154, X282, X283)
PART44_IN_AAAA(T175, .(T173, T176), X333, .(T173, X334)) → U9_AAAA(T175, T173, T176, X333, X334, part44_in_aaaa(T175, T176, X333, X334))
PART44_IN_AAAA(T175, .(T173, T176), X333, .(T173, X334)) → PART44_IN_AAAA(T175, T176, X333, X334)
P43_IN_AAAAAAA(T129, T123, T127, T128, X232, X233, X234) → U11_AAAAAAA(T129, T123, T127, T128, X232, X233, X234, partc44_in_aaaa(T129, T123, T127, T128))
U11_AAAAAAA(T129, T123, T127, T128, X232, X233, X234, partc44_out_aaaa(T129, T123, T127, T128)) → U12_AAAAAAA(T129, T123, T127, T128, X232, X233, X234, qs60_in_aa(T127, X232))
U11_AAAAAAA(T129, T123, T127, T128, X232, X233, X234, partc44_out_aaaa(T129, T123, T127, T128)) → QS60_IN_AA(T127, X232)
QS60_IN_AA(.(T192, T193), X370) → U20_AA(T192, T193, X370, p43_in_aaaaaaa(T192, T193, X366, X367, X368, X369, X370))
QS60_IN_AA(.(T192, T193), X370) → P43_IN_AAAAAAA(T192, T193, X366, X367, X368, X369, X370)
P43_IN_AAAAAAA(T185, T123, T127, T184, T183, X233, X234) → U13_AAAAAAA(T185, T123, T127, T184, T183, X233, X234, partc44_in_aaaa(T185, T123, T127, T184))
U13_AAAAAAA(T185, T123, T127, T184, T183, X233, X234, partc44_out_aaaa(T185, T123, T127, T184)) → U14_AAAAAAA(T185, T123, T127, T184, T183, X233, X234, qsc60_in_aa(T127, T183))
U14_AAAAAAA(T185, T123, T127, T184, T183, X233, X234, qsc60_out_aa(T127, T183)) → U15_AAAAAAA(T185, T123, T127, T184, T183, X233, X234, qs60_in_aa(T184, X233))
U14_AAAAAAA(T185, T123, T127, T184, T183, X233, X234, qsc60_out_aa(T127, T183)) → QS60_IN_AA(T184, X233)
P43_IN_AAAAAAA(T199, T123, T127, T184, T198, T197, X234) → U16_AAAAAAA(T199, T123, T127, T184, T198, T197, X234, partc44_in_aaaa(T199, T123, T127, T184))
U16_AAAAAAA(T199, T123, T127, T184, T198, T197, X234, partc44_out_aaaa(T199, T123, T127, T184)) → U17_AAAAAAA(T199, T123, T127, T184, T198, T197, X234, qsc60_in_aa(T127, T198))
U17_AAAAAAA(T199, T123, T127, T184, T198, T197, X234, qsc60_out_aa(T127, T198)) → U18_AAAAAAA(T199, T123, T127, T184, T198, T197, X234, qsc60_in_aa(T184, T197))
U18_AAAAAAA(T199, T123, T127, T184, T198, T197, X234, qsc60_out_aa(T184, T197)) → U19_AAAAAAA(T199, T123, T127, T184, T198, T197, X234, app71_in_aaaa(T198, T199, T197, X234))
U18_AAAAAAA(T199, T123, T127, T184, T198, T197, X234, qsc60_out_aa(T184, T197)) → APP71_IN_AAAA(T198, T199, T197, X234)
APP71_IN_AAAA(.(T222, T226), T227, T228, .(T222, X403)) → U21_AAAA(T222, T226, T227, T228, X403, app71_in_aaaa(T226, T227, T228, X403))
APP71_IN_AAAA(.(T222, T226), T227, T228, .(T222, X403)) → APP71_IN_AAAA(T226, T227, T228, X403)
U28_AG(T29, T54, T30, lessc13_out_aa(T29, T54)) → U31_AG(T29, T54, T30, partc23_in_gaaa(T29, T30, T52, T108))
U31_AG(T29, T54, T30, partc23_out_gaaa(T29, T30, T52, T108)) → U32_AG(T29, T54, T30, T108, qsc39_in_aaa(T54, T52, T107))
U32_AG(T29, T54, T30, T108, qsc39_out_aaa(T54, T52, T107)) → U33_AG(T29, T54, T30, qs60_in_aa(T108, X12))
U32_AG(T29, T54, T30, T108, qsc39_out_aaa(T54, T52, T107)) → QS60_IN_AA(T108, X12)
QS1_IN_AG(.(T264, .(T266, T265)), []) → U34_AG(T264, T266, T265, part44_in_aaaa(T264, T265, X454, X455))
QS1_IN_AG(.(T264, .(T266, T265)), []) → PART44_IN_AAAA(T264, T265, X454, X455)
QS1_IN_AG(.(T273, .(T272, T265)), []) → U35_AG(T273, T272, T265, partc44_in_aaaa(T273, T265, T270, T271))
U35_AG(T273, T272, T265, partc44_out_aaaa(T273, T265, T270, T271)) → U36_AG(T273, T272, T265, qs60_in_aa(T270, X11))
U35_AG(T273, T272, T265, partc44_out_aaaa(T273, T265, T270, T271)) → QS60_IN_AA(T270, X11)
QS1_IN_AG(.(T280, .(T278, T265)), []) → U37_AG(T280, T278, T265, partc44_in_aaaa(T280, T265, T270, T279))
U37_AG(T280, T278, T265, partc44_out_aaaa(T280, T265, T270, T279)) → U38_AG(T280, T278, T265, T279, qsc60_in_aa(T270, T277))
U38_AG(T280, T278, T265, T279, qsc60_out_aa(T270, T277)) → U39_AG(T280, T278, T265, qs39_in_aaa(T278, T279, X12))
U38_AG(T280, T278, T265, T279, qsc60_out_aa(T270, T277)) → QS39_IN_AAA(T278, T279, X12)
QS1_IN_AG(.(T347, .(T348, T349)), T329) → U40_AG(T347, T348, T349, T329, less13_in_aa(T347, T348))
QS1_IN_AG(.(T347, .(T348, T349)), T329) → LESS13_IN_AA(T347, T348)
QS1_IN_AG(.(T352, .(T354, T353)), T329) → U41_AG(T352, T354, T353, T329, lessc13_in_aa(T352, T354))
U41_AG(T352, T354, T353, T329, lessc13_out_aa(T352, T354)) → U42_AG(T352, T354, T353, T329, part23_in_gaaa(T352, T353, X581, X582))
U41_AG(T352, T354, T353, T329, lessc13_out_aa(T352, T354)) → PART23_IN_GAAA(T352, T353, X581, X582)
QS1_IN_AG(.(T352, .(T363, T353)), T329) → U43_AG(T352, T363, T353, T329, lessc13_in_aa(T352, T363))
U43_AG(T352, T363, T353, T329, lessc13_out_aa(T352, T363)) → U44_AG(T352, T363, T353, T329, partc23_in_gaaa(T352, T353, T361, T362))
U44_AG(T352, T363, T353, T329, partc23_out_gaaa(T352, T353, T361, T362)) → U45_AG(T352, T363, T353, T329, qs39_in_aaa(T363, T361, X543))
U44_AG(T352, T363, T353, T329, partc23_out_gaaa(T352, T353, T361, T362)) → QS39_IN_AAA(T363, T361, X543)
U43_AG(T352, T363, T353, T329, lessc13_out_aa(T352, T363)) → U46_AG(T352, T363, T353, T329, partc23_in_gaaa(T352, T353, T361, T371))
U46_AG(T352, T363, T353, T329, partc23_out_gaaa(T352, T353, T361, T371)) → U47_AG(T352, T363, T353, T329, T371, qsc39_in_aaa(T363, T361, T370))
U47_AG(T352, T363, T353, T329, T371, qsc39_out_aaa(T363, T361, T370)) → U48_AG(T352, T363, T353, T329, qs60_in_aa(T371, X544))
U47_AG(T352, T363, T353, T329, T371, qsc39_out_aaa(T363, T361, T370)) → QS60_IN_AA(T371, X544)
QS1_IN_AG(.(T404, .(T363, T353)), .(T402, T406)) → U49_AG(T404, T363, T353, T402, T406, lessc13_in_aa(T404, T363))
U49_AG(T404, T363, T353, T402, T406, lessc13_out_aa(T404, T363)) → U50_AG(T404, T363, T353, T402, T406, partc23_in_gaaa(T404, T353, T361, T371))
U50_AG(T404, T363, T353, T402, T406, partc23_out_gaaa(T404, T353, T361, T371)) → U51_AG(T404, T363, T353, T402, T406, T371, qsc39_in_aaa(T363, T361, .(T402, T407)))
U51_AG(T404, T363, T353, T402, T406, T371, qsc39_out_aaa(T363, T361, .(T402, T407))) → U52_AG(T404, T363, T353, T402, T406, T407, qsc60_in_aa(T371, T408))
U52_AG(T404, T363, T353, T402, T406, T407, qsc60_out_aa(T371, T408)) → U53_AG(T404, T363, T353, T402, T406, app131_in_agag(T407, T404, T408, T406))
U52_AG(T404, T363, T353, T402, T406, T407, qsc60_out_aa(T371, T408)) → APP131_IN_AGAG(T407, T404, T408, T406)
APP131_IN_AGAG(.(T433, T438), T435, T439, .(T433, T437)) → U23_AGAG(T433, T438, T435, T439, T437, app131_in_agag(T438, T435, T439, T437))
APP131_IN_AGAG(.(T433, T438), T435, T439, .(T433, T437)) → APP131_IN_AGAG(T438, T435, T439, T437)
QS1_IN_AG(.(T459, .(T461, T460)), T329) → U54_AG(T459, T461, T460, T329, part44_in_aaaa(T459, T460, X705, X706))
QS1_IN_AG(.(T459, .(T461, T460)), T329) → PART44_IN_AAAA(T459, T460, X705, X706)
QS1_IN_AG(.(T468, .(T467, T460)), T329) → U55_AG(T468, T467, T460, T329, partc44_in_aaaa(T468, T460, T465, T466))
U55_AG(T468, T467, T460, T329, partc44_out_aaaa(T468, T460, T465, T466)) → U56_AG(T468, T467, T460, T329, qs60_in_aa(T465, X543))
U55_AG(T468, T467, T460, T329, partc44_out_aaaa(T468, T460, T465, T466)) → QS60_IN_AA(T465, X543)
QS1_IN_AG(.(T476, .(T474, T460)), T329) → U57_AG(T476, T474, T460, T329, partc44_in_aaaa(T476, T460, T465, T475))
U57_AG(T476, T474, T460, T329, partc44_out_aaaa(T476, T460, T465, T475)) → U58_AG(T476, T474, T460, T329, T475, qsc60_in_aa(T465, T473))
U58_AG(T476, T474, T460, T329, T475, qsc60_out_aa(T465, T473)) → U59_AG(T476, T474, T460, T329, qs39_in_aaa(T474, T475, X544))
U58_AG(T476, T474, T460, T329, T475, qsc60_out_aa(T465, T473)) → QS39_IN_AAA(T474, T475, X544)
QS1_IN_AG(.(T516, .(T474, T460)), .(T510, T514)) → U60_AG(T516, T474, T460, T510, T514, partc44_in_aaaa(T516, T460, T465, T475))
U60_AG(T516, T474, T460, T510, T514, partc44_out_aaaa(T516, T460, T465, T475)) → U61_AG(T516, T474, T460, T510, T514, T475, qsc60_in_aa(T465, .(T510, T515)))
U61_AG(T516, T474, T460, T510, T514, T475, qsc60_out_aa(T465, .(T510, T515))) → U62_AG(T516, T474, T460, T510, T514, T515, qsc39_in_aaa(T474, T475, T517))
U62_AG(T516, T474, T460, T510, T514, T515, qsc39_out_aaa(T474, T475, T517)) → U63_AG(T516, T474, T460, T510, T514, app157_in_aaag(T515, T516, T517, T514))
U62_AG(T516, T474, T460, T510, T514, T515, qsc39_out_aaa(T474, T475, T517)) → APP157_IN_AAAG(T515, T516, T517, T514)
APP157_IN_AAAG(.(T542, T547), T548, T549, .(T542, T546)) → U24_AAAG(T542, T547, T548, T549, T546, app157_in_aaag(T547, T548, T549, T546))
APP157_IN_AAAG(.(T542, T547), T548, T549, .(T542, T546)) → APP157_IN_AAAG(T547, T548, T549, T546)
QS1_IN_AG(.(T557, []), T329) → U64_AG(T557, T329, qsc100_in_a(T560))
U64_AG(T557, T329, qsc100_out_a(T560)) → U65_AG(T557, T329, T560, qsc100_in_a(T563))
U65_AG(T557, T329, T560, qsc100_out_a(T563)) → U66_AG(T557, T329, app157_in_gagg(T560, T557, T563, T329))
U65_AG(T557, T329, T560, qsc100_out_a(T563)) → APP157_IN_GAGG(T560, T557, T563, T329)
APP157_IN_GAGG(.(T542, T547), T548, T549, .(T542, T546)) → U24_GAGG(T542, T547, T548, T549, T546, app157_in_gagg(T547, T548, T549, T546))
APP157_IN_GAGG(.(T542, T547), T548, T549, .(T542, T546)) → APP157_IN_GAGG(T547, T548, T549, T546)

The TRS R consists of the following rules:

lessc13_in_aa(0, s(T38)) → lessc13_out_aa(0, s(T38))
lessc13_in_aa(s(T45), s(T46)) → U68_aa(T45, T46, lessc13_in_aa(T45, T46))
U68_aa(T45, T46, lessc13_out_aa(T45, T46)) → lessc13_out_aa(s(T45), s(T46))
lessc13_in_ga(0, s(T38)) → lessc13_out_ga(0, s(T38))
lessc13_in_ga(s(T45), s(T46)) → U68_ga(T45, T46, lessc13_in_ga(T45, T46))
U68_ga(T45, T46, lessc13_out_ga(T45, T46)) → lessc13_out_ga(s(T45), s(T46))
partc23_in_gaaa(T70, .(T73, T77), .(T73, X123), X124) → U69_gaaa(T70, T73, T77, X123, X124, lessc13_in_ga(T70, T73))
U69_gaaa(T70, T73, T77, X123, X124, lessc13_out_ga(T70, T73)) → U70_gaaa(T70, T73, T77, X123, X124, partc23_in_gaaa(T70, T77, X123, X124))
partc23_in_gaaa(T95, .(T96, T98), X174, .(T96, X175)) → U71_gaaa(T95, T96, T98, X174, X175, partc23_in_gaaa(T95, T98, X174, X175))
partc23_in_gaaa(T104, [], [], []) → partc23_out_gaaa(T104, [], [], [])
U71_gaaa(T95, T96, T98, X174, X175, partc23_out_gaaa(T95, T98, X174, X175)) → partc23_out_gaaa(T95, .(T96, T98), X174, .(T96, X175))
U70_gaaa(T70, T73, T77, X123, X124, partc23_out_gaaa(T70, T77, X123, X124)) → partc23_out_gaaa(T70, .(T73, T77), .(T73, X123), X124)
partc44_in_aaaa(T153, .(T149, T154), .(T149, X282), X283) → U72_aaaa(T153, T149, T154, X282, X283, lessc13_in_aa(T153, T149))
U72_aaaa(T153, T149, T154, X282, X283, lessc13_out_aa(T153, T149)) → U73_aaaa(T153, T149, T154, X282, X283, partc23_in_gaaa(T153, T154, X282, X283))
U73_aaaa(T153, T149, T154, X282, X283, partc23_out_gaaa(T153, T154, X282, X283)) → partc44_out_aaaa(T153, .(T149, T154), .(T149, X282), X283)
partc44_in_aaaa(T175, .(T173, T176), X333, .(T173, X334)) → U74_aaaa(T175, T173, T176, X333, X334, partc44_in_aaaa(T175, T176, X333, X334))
partc44_in_aaaa(T182, [], [], []) → partc44_out_aaaa(T182, [], [], [])
U74_aaaa(T175, T173, T176, X333, X334, partc44_out_aaaa(T175, T176, X333, X334)) → partc44_out_aaaa(T175, .(T173, T176), X333, .(T173, X334))
qsc60_in_aa([], []) → qsc60_out_aa([], [])
qsc60_in_aa(.(T192, T193), X370) → U79_aa(T192, T193, X370, qc43_in_aaaaaaa(T192, T193, X366, X367, X368, X369, X370))
qc43_in_aaaaaaa(T199, T123, T127, T184, T198, T197, X234) → U75_aaaaaaa(T199, T123, T127, T184, T198, T197, X234, partc44_in_aaaa(T199, T123, T127, T184))
U75_aaaaaaa(T199, T123, T127, T184, T198, T197, X234, partc44_out_aaaa(T199, T123, T127, T184)) → U76_aaaaaaa(T199, T123, T127, T184, T198, T197, X234, qsc60_in_aa(T127, T198))
U76_aaaaaaa(T199, T123, T127, T184, T198, T197, X234, qsc60_out_aa(T127, T198)) → U77_aaaaaaa(T199, T123, T127, T184, T198, T197, X234, qsc60_in_aa(T184, T197))
U77_aaaaaaa(T199, T123, T127, T184, T198, T197, X234, qsc60_out_aa(T184, T197)) → U78_aaaaaaa(T199, T123, T127, T184, T198, T197, X234, appc71_in_aaaa(T198, T199, T197, X234))
appc71_in_aaaa([], T212, T213, .(T212, T213)) → appc71_out_aaaa([], T212, T213, .(T212, T213))
appc71_in_aaaa(.(T222, T226), T227, T228, .(T222, X403)) → U80_aaaa(T222, T226, T227, T228, X403, appc71_in_aaaa(T226, T227, T228, X403))
U80_aaaa(T222, T226, T227, T228, X403, appc71_out_aaaa(T226, T227, T228, X403)) → appc71_out_aaaa(.(T222, T226), T227, T228, .(T222, X403))
U78_aaaaaaa(T199, T123, T127, T184, T198, T197, X234, appc71_out_aaaa(T198, T199, T197, X234)) → qc43_out_aaaaaaa(T199, T123, T127, T184, T198, T197, X234)
U79_aa(T192, T193, X370, qc43_out_aaaaaaa(T192, T193, X366, X367, X368, X369, X370)) → qsc60_out_aa(.(T192, T193), X370)
qsc39_in_aaa(T122, T123, X234) → U81_aaa(T122, T123, X234, qc43_in_aaaaaaa(T122, T123, X230, X231, X232, X233, X234))
U81_aaa(T122, T123, X234, qc43_out_aaaaaaa(T122, T123, X230, X231, X232, X233, X234)) → qsc39_out_aaa(T122, T123, X234)
qsc100_in_a([]) → qsc100_out_a([])

The argument filtering Pi contains the following mapping:
[]  =  []
less13_in_aa(x1, x2)  =  less13_in_aa
lessc13_in_aa(x1, x2)  =  lessc13_in_aa
lessc13_out_aa(x1, x2)  =  lessc13_out_aa(x1)
U68_aa(x1, x2, x3)  =  U68_aa(x3)
part23_in_gaaa(x1, x2, x3, x4)  =  part23_in_gaaa(x1)
less13_in_ga(x1, x2)  =  less13_in_ga(x1)
s(x1)  =  s(x1)
lessc13_in_ga(x1, x2)  =  lessc13_in_ga(x1)
0  =  0
lessc13_out_ga(x1, x2)  =  lessc13_out_ga(x1)
U68_ga(x1, x2, x3)  =  U68_ga(x1, x3)
partc23_in_gaaa(x1, x2, x3, x4)  =  partc23_in_gaaa(x1)
U69_gaaa(x1, x2, x3, x4, x5, x6)  =  U69_gaaa(x1, x6)
U70_gaaa(x1, x2, x3, x4, x5, x6)  =  U70_gaaa(x1, x6)
U71_gaaa(x1, x2, x3, x4, x5, x6)  =  U71_gaaa(x1, x6)
partc23_out_gaaa(x1, x2, x3, x4)  =  partc23_out_gaaa(x1)
qs39_in_aaa(x1, x2, x3)  =  qs39_in_aaa
p43_in_aaaaaaa(x1, x2, x3, x4, x5, x6, x7)  =  p43_in_aaaaaaa
part44_in_aaaa(x1, x2, x3, x4)  =  part44_in_aaaa
partc44_in_aaaa(x1, x2, x3, x4)  =  partc44_in_aaaa
U72_aaaa(x1, x2, x3, x4, x5, x6)  =  U72_aaaa(x6)
U73_aaaa(x1, x2, x3, x4, x5, x6)  =  U73_aaaa(x6)
partc44_out_aaaa(x1, x2, x3, x4)  =  partc44_out_aaaa
U74_aaaa(x1, x2, x3, x4, x5, x6)  =  U74_aaaa(x6)
qs60_in_aa(x1, x2)  =  qs60_in_aa
qsc60_in_aa(x1, x2)  =  qsc60_in_aa
qsc60_out_aa(x1, x2)  =  qsc60_out_aa
U79_aa(x1, x2, x3, x4)  =  U79_aa(x4)
qc43_in_aaaaaaa(x1, x2, x3, x4, x5, x6, x7)  =  qc43_in_aaaaaaa
U75_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  U75_aaaaaaa(x8)
U76_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  U76_aaaaaaa(x8)
U77_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  U77_aaaaaaa(x8)
U78_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  U78_aaaaaaa(x8)
.(x1, x2)  =  .(x1, x2)
qc43_out_aaaaaaa(x1, x2, x3, x4, x5, x6, x7)  =  qc43_out_aaaaaaa
appc71_in_aaaa(x1, x2, x3, x4)  =  appc71_in_aaaa
appc71_out_aaaa(x1, x2, x3, x4)  =  appc71_out_aaaa
U80_aaaa(x1, x2, x3, x4, x5, x6)  =  U80_aaaa(x6)
app71_in_aaaa(x1, x2, x3, x4)  =  app71_in_aaaa
qsc39_in_aaa(x1, x2, x3)  =  qsc39_in_aaa
U81_aaa(x1, x2, x3, x4)  =  U81_aaa(x4)
qsc39_out_aaa(x1, x2, x3)  =  qsc39_out_aaa
app131_in_agag(x1, x2, x3, x4)  =  app131_in_agag(x2, x4)
app157_in_aaag(x1, x2, x3, x4)  =  app157_in_aaag(x4)
qsc100_in_a(x1)  =  qsc100_in_a
qsc100_out_a(x1)  =  qsc100_out_a(x1)
app157_in_gagg(x1, x2, x3, x4)  =  app157_in_gagg(x1, x3, x4)
QS1_IN_AG(x1, x2)  =  QS1_IN_AG(x2)
U25_AG(x1, x2, x3, x4)  =  U25_AG(x4)
LESS13_IN_AA(x1, x2)  =  LESS13_IN_AA
U1_AA(x1, x2, x3)  =  U1_AA(x3)
U26_AG(x1, x2, x3, x4)  =  U26_AG(x4)
U27_AG(x1, x2, x3, x4)  =  U27_AG(x4)
PART23_IN_GAAA(x1, x2, x3, x4)  =  PART23_IN_GAAA(x1)
U2_GAAA(x1, x2, x3, x4, x5, x6)  =  U2_GAAA(x1, x6)
LESS13_IN_GA(x1, x2)  =  LESS13_IN_GA(x1)
U1_GA(x1, x2, x3)  =  U1_GA(x1, x3)
U3_GAAA(x1, x2, x3, x4, x5, x6)  =  U3_GAAA(x1, x6)
U4_GAAA(x1, x2, x3, x4, x5, x6)  =  U4_GAAA(x1, x6)
U5_GAAA(x1, x2, x3, x4, x5, x6)  =  U5_GAAA(x1, x6)
U28_AG(x1, x2, x3, x4)  =  U28_AG(x4)
U29_AG(x1, x2, x3, x4)  =  U29_AG(x4)
U30_AG(x1, x2, x3, x4)  =  U30_AG(x4)
QS39_IN_AAA(x1, x2, x3)  =  QS39_IN_AAA
U22_AAA(x1, x2, x3, x4)  =  U22_AAA(x4)
P43_IN_AAAAAAA(x1, x2, x3, x4, x5, x6, x7)  =  P43_IN_AAAAAAA
U10_AAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8)  =  U10_AAAAAAA(x8)
PART44_IN_AAAA(x1, x2, x3, x4)  =  PART44_IN_AAAA
U6_AAAA(x1, x2, x3, x4, x5, x6)  =  U6_AAAA(x6)
U7_AAAA(x1, x2, x3, x4, x5, x6)  =  U7_AAAA(x6)
U8_AAAA(x1, x2, x3, x4, x5, x6)  =  U8_AAAA(x1, x6)
U9_AAAA(x1, x2, x3, x4, x5, x6)  =  U9_AAAA(x6)
U11_AAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8)  =  U11_AAAAAAA(x8)
U12_AAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8)  =  U12_AAAAAAA(x8)
QS60_IN_AA(x1, x2)  =  QS60_IN_AA
U20_AA(x1, x2, x3, x4)  =  U20_AA(x4)
U13_AAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8)  =  U13_AAAAAAA(x8)
U14_AAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8)  =  U14_AAAAAAA(x8)
U15_AAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8)  =  U15_AAAAAAA(x8)
U16_AAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8)  =  U16_AAAAAAA(x8)
U17_AAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8)  =  U17_AAAAAAA(x8)
U18_AAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8)  =  U18_AAAAAAA(x8)
U19_AAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8)  =  U19_AAAAAAA(x8)
APP71_IN_AAAA(x1, x2, x3, x4)  =  APP71_IN_AAAA
U21_AAAA(x1, x2, x3, x4, x5, x6)  =  U21_AAAA(x6)
U31_AG(x1, x2, x3, x4)  =  U31_AG(x4)
U32_AG(x1, x2, x3, x4, x5)  =  U32_AG(x5)
U33_AG(x1, x2, x3, x4)  =  U33_AG(x4)
U34_AG(x1, x2, x3, x4)  =  U34_AG(x4)
U35_AG(x1, x2, x3, x4)  =  U35_AG(x4)
U36_AG(x1, x2, x3, x4)  =  U36_AG(x4)
U37_AG(x1, x2, x3, x4)  =  U37_AG(x4)
U38_AG(x1, x2, x3, x4, x5)  =  U38_AG(x5)
U39_AG(x1, x2, x3, x4)  =  U39_AG(x4)
U40_AG(x1, x2, x3, x4, x5)  =  U40_AG(x4, x5)
U41_AG(x1, x2, x3, x4, x5)  =  U41_AG(x4, x5)
U42_AG(x1, x2, x3, x4, x5)  =  U42_AG(x4, x5)
U43_AG(x1, x2, x3, x4, x5)  =  U43_AG(x4, x5)
U44_AG(x1, x2, x3, x4, x5)  =  U44_AG(x4, x5)
U45_AG(x1, x2, x3, x4, x5)  =  U45_AG(x4, x5)
U46_AG(x1, x2, x3, x4, x5)  =  U46_AG(x4, x5)
U47_AG(x1, x2, x3, x4, x5, x6)  =  U47_AG(x4, x6)
U48_AG(x1, x2, x3, x4, x5)  =  U48_AG(x4, x5)
U49_AG(x1, x2, x3, x4, x5, x6)  =  U49_AG(x4, x5, x6)
U50_AG(x1, x2, x3, x4, x5, x6)  =  U50_AG(x1, x4, x5, x6)
U51_AG(x1, x2, x3, x4, x5, x6, x7)  =  U51_AG(x1, x4, x5, x7)
U52_AG(x1, x2, x3, x4, x5, x6, x7)  =  U52_AG(x1, x4, x5, x7)
U53_AG(x1, x2, x3, x4, x5, x6)  =  U53_AG(x4, x5, x6)
APP131_IN_AGAG(x1, x2, x3, x4)  =  APP131_IN_AGAG(x2, x4)
U23_AGAG(x1, x2, x3, x4, x5, x6)  =  U23_AGAG(x1, x3, x5, x6)
U54_AG(x1, x2, x3, x4, x5)  =  U54_AG(x4, x5)
U55_AG(x1, x2, x3, x4, x5)  =  U55_AG(x4, x5)
U56_AG(x1, x2, x3, x4, x5)  =  U56_AG(x4, x5)
U57_AG(x1, x2, x3, x4, x5)  =  U57_AG(x4, x5)
U58_AG(x1, x2, x3, x4, x5, x6)  =  U58_AG(x4, x6)
U59_AG(x1, x2, x3, x4, x5)  =  U59_AG(x4, x5)
U60_AG(x1, x2, x3, x4, x5, x6)  =  U60_AG(x4, x5, x6)
U61_AG(x1, x2, x3, x4, x5, x6, x7)  =  U61_AG(x4, x5, x7)
U62_AG(x1, x2, x3, x4, x5, x6, x7)  =  U62_AG(x4, x5, x7)
U63_AG(x1, x2, x3, x4, x5, x6)  =  U63_AG(x4, x5, x6)
APP157_IN_AAAG(x1, x2, x3, x4)  =  APP157_IN_AAAG(x4)
U24_AAAG(x1, x2, x3, x4, x5, x6)  =  U24_AAAG(x1, x5, x6)
U64_AG(x1, x2, x3)  =  U64_AG(x2, x3)
U65_AG(x1, x2, x3, x4)  =  U65_AG(x2, x3, x4)
U66_AG(x1, x2, x3)  =  U66_AG(x2, x3)
APP157_IN_GAGG(x1, x2, x3, x4)  =  APP157_IN_GAGG(x1, x3, x4)
U24_GAGG(x1, x2, x3, x4, x5, x6)  =  U24_GAGG(x1, x2, x4, x5, x6)

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

(7) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 9 SCCs with 87 less nodes.

(8) Complex Obligation (AND)

(9) Obligation:

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

APP157_IN_GAGG(.(T542, T547), T548, T549, .(T542, T546)) → APP157_IN_GAGG(T547, T548, T549, T546)

The TRS R consists of the following rules:

lessc13_in_aa(0, s(T38)) → lessc13_out_aa(0, s(T38))
lessc13_in_aa(s(T45), s(T46)) → U68_aa(T45, T46, lessc13_in_aa(T45, T46))
U68_aa(T45, T46, lessc13_out_aa(T45, T46)) → lessc13_out_aa(s(T45), s(T46))
lessc13_in_ga(0, s(T38)) → lessc13_out_ga(0, s(T38))
lessc13_in_ga(s(T45), s(T46)) → U68_ga(T45, T46, lessc13_in_ga(T45, T46))
U68_ga(T45, T46, lessc13_out_ga(T45, T46)) → lessc13_out_ga(s(T45), s(T46))
partc23_in_gaaa(T70, .(T73, T77), .(T73, X123), X124) → U69_gaaa(T70, T73, T77, X123, X124, lessc13_in_ga(T70, T73))
U69_gaaa(T70, T73, T77, X123, X124, lessc13_out_ga(T70, T73)) → U70_gaaa(T70, T73, T77, X123, X124, partc23_in_gaaa(T70, T77, X123, X124))
partc23_in_gaaa(T95, .(T96, T98), X174, .(T96, X175)) → U71_gaaa(T95, T96, T98, X174, X175, partc23_in_gaaa(T95, T98, X174, X175))
partc23_in_gaaa(T104, [], [], []) → partc23_out_gaaa(T104, [], [], [])
U71_gaaa(T95, T96, T98, X174, X175, partc23_out_gaaa(T95, T98, X174, X175)) → partc23_out_gaaa(T95, .(T96, T98), X174, .(T96, X175))
U70_gaaa(T70, T73, T77, X123, X124, partc23_out_gaaa(T70, T77, X123, X124)) → partc23_out_gaaa(T70, .(T73, T77), .(T73, X123), X124)
partc44_in_aaaa(T153, .(T149, T154), .(T149, X282), X283) → U72_aaaa(T153, T149, T154, X282, X283, lessc13_in_aa(T153, T149))
U72_aaaa(T153, T149, T154, X282, X283, lessc13_out_aa(T153, T149)) → U73_aaaa(T153, T149, T154, X282, X283, partc23_in_gaaa(T153, T154, X282, X283))
U73_aaaa(T153, T149, T154, X282, X283, partc23_out_gaaa(T153, T154, X282, X283)) → partc44_out_aaaa(T153, .(T149, T154), .(T149, X282), X283)
partc44_in_aaaa(T175, .(T173, T176), X333, .(T173, X334)) → U74_aaaa(T175, T173, T176, X333, X334, partc44_in_aaaa(T175, T176, X333, X334))
partc44_in_aaaa(T182, [], [], []) → partc44_out_aaaa(T182, [], [], [])
U74_aaaa(T175, T173, T176, X333, X334, partc44_out_aaaa(T175, T176, X333, X334)) → partc44_out_aaaa(T175, .(T173, T176), X333, .(T173, X334))
qsc60_in_aa([], []) → qsc60_out_aa([], [])
qsc60_in_aa(.(T192, T193), X370) → U79_aa(T192, T193, X370, qc43_in_aaaaaaa(T192, T193, X366, X367, X368, X369, X370))
qc43_in_aaaaaaa(T199, T123, T127, T184, T198, T197, X234) → U75_aaaaaaa(T199, T123, T127, T184, T198, T197, X234, partc44_in_aaaa(T199, T123, T127, T184))
U75_aaaaaaa(T199, T123, T127, T184, T198, T197, X234, partc44_out_aaaa(T199, T123, T127, T184)) → U76_aaaaaaa(T199, T123, T127, T184, T198, T197, X234, qsc60_in_aa(T127, T198))
U76_aaaaaaa(T199, T123, T127, T184, T198, T197, X234, qsc60_out_aa(T127, T198)) → U77_aaaaaaa(T199, T123, T127, T184, T198, T197, X234, qsc60_in_aa(T184, T197))
U77_aaaaaaa(T199, T123, T127, T184, T198, T197, X234, qsc60_out_aa(T184, T197)) → U78_aaaaaaa(T199, T123, T127, T184, T198, T197, X234, appc71_in_aaaa(T198, T199, T197, X234))
appc71_in_aaaa([], T212, T213, .(T212, T213)) → appc71_out_aaaa([], T212, T213, .(T212, T213))
appc71_in_aaaa(.(T222, T226), T227, T228, .(T222, X403)) → U80_aaaa(T222, T226, T227, T228, X403, appc71_in_aaaa(T226, T227, T228, X403))
U80_aaaa(T222, T226, T227, T228, X403, appc71_out_aaaa(T226, T227, T228, X403)) → appc71_out_aaaa(.(T222, T226), T227, T228, .(T222, X403))
U78_aaaaaaa(T199, T123, T127, T184, T198, T197, X234, appc71_out_aaaa(T198, T199, T197, X234)) → qc43_out_aaaaaaa(T199, T123, T127, T184, T198, T197, X234)
U79_aa(T192, T193, X370, qc43_out_aaaaaaa(T192, T193, X366, X367, X368, X369, X370)) → qsc60_out_aa(.(T192, T193), X370)
qsc39_in_aaa(T122, T123, X234) → U81_aaa(T122, T123, X234, qc43_in_aaaaaaa(T122, T123, X230, X231, X232, X233, X234))
U81_aaa(T122, T123, X234, qc43_out_aaaaaaa(T122, T123, X230, X231, X232, X233, X234)) → qsc39_out_aaa(T122, T123, X234)
qsc100_in_a([]) → qsc100_out_a([])

The argument filtering Pi contains the following mapping:
[]  =  []
lessc13_in_aa(x1, x2)  =  lessc13_in_aa
lessc13_out_aa(x1, x2)  =  lessc13_out_aa(x1)
U68_aa(x1, x2, x3)  =  U68_aa(x3)
s(x1)  =  s(x1)
lessc13_in_ga(x1, x2)  =  lessc13_in_ga(x1)
0  =  0
lessc13_out_ga(x1, x2)  =  lessc13_out_ga(x1)
U68_ga(x1, x2, x3)  =  U68_ga(x1, x3)
partc23_in_gaaa(x1, x2, x3, x4)  =  partc23_in_gaaa(x1)
U69_gaaa(x1, x2, x3, x4, x5, x6)  =  U69_gaaa(x1, x6)
U70_gaaa(x1, x2, x3, x4, x5, x6)  =  U70_gaaa(x1, x6)
U71_gaaa(x1, x2, x3, x4, x5, x6)  =  U71_gaaa(x1, x6)
partc23_out_gaaa(x1, x2, x3, x4)  =  partc23_out_gaaa(x1)
partc44_in_aaaa(x1, x2, x3, x4)  =  partc44_in_aaaa
U72_aaaa(x1, x2, x3, x4, x5, x6)  =  U72_aaaa(x6)
U73_aaaa(x1, x2, x3, x4, x5, x6)  =  U73_aaaa(x6)
partc44_out_aaaa(x1, x2, x3, x4)  =  partc44_out_aaaa
U74_aaaa(x1, x2, x3, x4, x5, x6)  =  U74_aaaa(x6)
qsc60_in_aa(x1, x2)  =  qsc60_in_aa
qsc60_out_aa(x1, x2)  =  qsc60_out_aa
U79_aa(x1, x2, x3, x4)  =  U79_aa(x4)
qc43_in_aaaaaaa(x1, x2, x3, x4, x5, x6, x7)  =  qc43_in_aaaaaaa
U75_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  U75_aaaaaaa(x8)
U76_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  U76_aaaaaaa(x8)
U77_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  U77_aaaaaaa(x8)
U78_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  U78_aaaaaaa(x8)
.(x1, x2)  =  .(x1, x2)
qc43_out_aaaaaaa(x1, x2, x3, x4, x5, x6, x7)  =  qc43_out_aaaaaaa
appc71_in_aaaa(x1, x2, x3, x4)  =  appc71_in_aaaa
appc71_out_aaaa(x1, x2, x3, x4)  =  appc71_out_aaaa
U80_aaaa(x1, x2, x3, x4, x5, x6)  =  U80_aaaa(x6)
qsc39_in_aaa(x1, x2, x3)  =  qsc39_in_aaa
U81_aaa(x1, x2, x3, x4)  =  U81_aaa(x4)
qsc39_out_aaa(x1, x2, x3)  =  qsc39_out_aaa
qsc100_in_a(x1)  =  qsc100_in_a
qsc100_out_a(x1)  =  qsc100_out_a(x1)
APP157_IN_GAGG(x1, x2, x3, x4)  =  APP157_IN_GAGG(x1, x3, x4)

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

(10) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(11) Obligation:

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

APP157_IN_GAGG(.(T542, T547), T548, T549, .(T542, T546)) → APP157_IN_GAGG(T547, T548, T549, T546)

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

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

(12) PiDPToQDPProof (SOUND transformation)

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

(13) Obligation:

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

APP157_IN_GAGG(.(T542, T547), T549, .(T542, T546)) → APP157_IN_GAGG(T547, T549, T546)

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

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

  • APP157_IN_GAGG(.(T542, T547), T549, .(T542, T546)) → APP157_IN_GAGG(T547, T549, T546)
    The graph contains the following edges 1 > 1, 2 >= 2, 3 > 3

(15) YES

(16) Obligation:

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

APP157_IN_AAAG(.(T542, T547), T548, T549, .(T542, T546)) → APP157_IN_AAAG(T547, T548, T549, T546)

The TRS R consists of the following rules:

lessc13_in_aa(0, s(T38)) → lessc13_out_aa(0, s(T38))
lessc13_in_aa(s(T45), s(T46)) → U68_aa(T45, T46, lessc13_in_aa(T45, T46))
U68_aa(T45, T46, lessc13_out_aa(T45, T46)) → lessc13_out_aa(s(T45), s(T46))
lessc13_in_ga(0, s(T38)) → lessc13_out_ga(0, s(T38))
lessc13_in_ga(s(T45), s(T46)) → U68_ga(T45, T46, lessc13_in_ga(T45, T46))
U68_ga(T45, T46, lessc13_out_ga(T45, T46)) → lessc13_out_ga(s(T45), s(T46))
partc23_in_gaaa(T70, .(T73, T77), .(T73, X123), X124) → U69_gaaa(T70, T73, T77, X123, X124, lessc13_in_ga(T70, T73))
U69_gaaa(T70, T73, T77, X123, X124, lessc13_out_ga(T70, T73)) → U70_gaaa(T70, T73, T77, X123, X124, partc23_in_gaaa(T70, T77, X123, X124))
partc23_in_gaaa(T95, .(T96, T98), X174, .(T96, X175)) → U71_gaaa(T95, T96, T98, X174, X175, partc23_in_gaaa(T95, T98, X174, X175))
partc23_in_gaaa(T104, [], [], []) → partc23_out_gaaa(T104, [], [], [])
U71_gaaa(T95, T96, T98, X174, X175, partc23_out_gaaa(T95, T98, X174, X175)) → partc23_out_gaaa(T95, .(T96, T98), X174, .(T96, X175))
U70_gaaa(T70, T73, T77, X123, X124, partc23_out_gaaa(T70, T77, X123, X124)) → partc23_out_gaaa(T70, .(T73, T77), .(T73, X123), X124)
partc44_in_aaaa(T153, .(T149, T154), .(T149, X282), X283) → U72_aaaa(T153, T149, T154, X282, X283, lessc13_in_aa(T153, T149))
U72_aaaa(T153, T149, T154, X282, X283, lessc13_out_aa(T153, T149)) → U73_aaaa(T153, T149, T154, X282, X283, partc23_in_gaaa(T153, T154, X282, X283))
U73_aaaa(T153, T149, T154, X282, X283, partc23_out_gaaa(T153, T154, X282, X283)) → partc44_out_aaaa(T153, .(T149, T154), .(T149, X282), X283)
partc44_in_aaaa(T175, .(T173, T176), X333, .(T173, X334)) → U74_aaaa(T175, T173, T176, X333, X334, partc44_in_aaaa(T175, T176, X333, X334))
partc44_in_aaaa(T182, [], [], []) → partc44_out_aaaa(T182, [], [], [])
U74_aaaa(T175, T173, T176, X333, X334, partc44_out_aaaa(T175, T176, X333, X334)) → partc44_out_aaaa(T175, .(T173, T176), X333, .(T173, X334))
qsc60_in_aa([], []) → qsc60_out_aa([], [])
qsc60_in_aa(.(T192, T193), X370) → U79_aa(T192, T193, X370, qc43_in_aaaaaaa(T192, T193, X366, X367, X368, X369, X370))
qc43_in_aaaaaaa(T199, T123, T127, T184, T198, T197, X234) → U75_aaaaaaa(T199, T123, T127, T184, T198, T197, X234, partc44_in_aaaa(T199, T123, T127, T184))
U75_aaaaaaa(T199, T123, T127, T184, T198, T197, X234, partc44_out_aaaa(T199, T123, T127, T184)) → U76_aaaaaaa(T199, T123, T127, T184, T198, T197, X234, qsc60_in_aa(T127, T198))
U76_aaaaaaa(T199, T123, T127, T184, T198, T197, X234, qsc60_out_aa(T127, T198)) → U77_aaaaaaa(T199, T123, T127, T184, T198, T197, X234, qsc60_in_aa(T184, T197))
U77_aaaaaaa(T199, T123, T127, T184, T198, T197, X234, qsc60_out_aa(T184, T197)) → U78_aaaaaaa(T199, T123, T127, T184, T198, T197, X234, appc71_in_aaaa(T198, T199, T197, X234))
appc71_in_aaaa([], T212, T213, .(T212, T213)) → appc71_out_aaaa([], T212, T213, .(T212, T213))
appc71_in_aaaa(.(T222, T226), T227, T228, .(T222, X403)) → U80_aaaa(T222, T226, T227, T228, X403, appc71_in_aaaa(T226, T227, T228, X403))
U80_aaaa(T222, T226, T227, T228, X403, appc71_out_aaaa(T226, T227, T228, X403)) → appc71_out_aaaa(.(T222, T226), T227, T228, .(T222, X403))
U78_aaaaaaa(T199, T123, T127, T184, T198, T197, X234, appc71_out_aaaa(T198, T199, T197, X234)) → qc43_out_aaaaaaa(T199, T123, T127, T184, T198, T197, X234)
U79_aa(T192, T193, X370, qc43_out_aaaaaaa(T192, T193, X366, X367, X368, X369, X370)) → qsc60_out_aa(.(T192, T193), X370)
qsc39_in_aaa(T122, T123, X234) → U81_aaa(T122, T123, X234, qc43_in_aaaaaaa(T122, T123, X230, X231, X232, X233, X234))
U81_aaa(T122, T123, X234, qc43_out_aaaaaaa(T122, T123, X230, X231, X232, X233, X234)) → qsc39_out_aaa(T122, T123, X234)
qsc100_in_a([]) → qsc100_out_a([])

The argument filtering Pi contains the following mapping:
[]  =  []
lessc13_in_aa(x1, x2)  =  lessc13_in_aa
lessc13_out_aa(x1, x2)  =  lessc13_out_aa(x1)
U68_aa(x1, x2, x3)  =  U68_aa(x3)
s(x1)  =  s(x1)
lessc13_in_ga(x1, x2)  =  lessc13_in_ga(x1)
0  =  0
lessc13_out_ga(x1, x2)  =  lessc13_out_ga(x1)
U68_ga(x1, x2, x3)  =  U68_ga(x1, x3)
partc23_in_gaaa(x1, x2, x3, x4)  =  partc23_in_gaaa(x1)
U69_gaaa(x1, x2, x3, x4, x5, x6)  =  U69_gaaa(x1, x6)
U70_gaaa(x1, x2, x3, x4, x5, x6)  =  U70_gaaa(x1, x6)
U71_gaaa(x1, x2, x3, x4, x5, x6)  =  U71_gaaa(x1, x6)
partc23_out_gaaa(x1, x2, x3, x4)  =  partc23_out_gaaa(x1)
partc44_in_aaaa(x1, x2, x3, x4)  =  partc44_in_aaaa
U72_aaaa(x1, x2, x3, x4, x5, x6)  =  U72_aaaa(x6)
U73_aaaa(x1, x2, x3, x4, x5, x6)  =  U73_aaaa(x6)
partc44_out_aaaa(x1, x2, x3, x4)  =  partc44_out_aaaa
U74_aaaa(x1, x2, x3, x4, x5, x6)  =  U74_aaaa(x6)
qsc60_in_aa(x1, x2)  =  qsc60_in_aa
qsc60_out_aa(x1, x2)  =  qsc60_out_aa
U79_aa(x1, x2, x3, x4)  =  U79_aa(x4)
qc43_in_aaaaaaa(x1, x2, x3, x4, x5, x6, x7)  =  qc43_in_aaaaaaa
U75_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  U75_aaaaaaa(x8)
U76_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  U76_aaaaaaa(x8)
U77_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  U77_aaaaaaa(x8)
U78_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  U78_aaaaaaa(x8)
.(x1, x2)  =  .(x1, x2)
qc43_out_aaaaaaa(x1, x2, x3, x4, x5, x6, x7)  =  qc43_out_aaaaaaa
appc71_in_aaaa(x1, x2, x3, x4)  =  appc71_in_aaaa
appc71_out_aaaa(x1, x2, x3, x4)  =  appc71_out_aaaa
U80_aaaa(x1, x2, x3, x4, x5, x6)  =  U80_aaaa(x6)
qsc39_in_aaa(x1, x2, x3)  =  qsc39_in_aaa
U81_aaa(x1, x2, x3, x4)  =  U81_aaa(x4)
qsc39_out_aaa(x1, x2, x3)  =  qsc39_out_aaa
qsc100_in_a(x1)  =  qsc100_in_a
qsc100_out_a(x1)  =  qsc100_out_a(x1)
APP157_IN_AAAG(x1, x2, x3, x4)  =  APP157_IN_AAAG(x4)

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

(17) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(18) Obligation:

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

APP157_IN_AAAG(.(T542, T547), T548, T549, .(T542, T546)) → APP157_IN_AAAG(T547, T548, T549, T546)

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

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

(19) PiDPToQDPProof (SOUND transformation)

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

(20) Obligation:

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

APP157_IN_AAAG(.(T542, T546)) → APP157_IN_AAAG(T546)

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

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

  • APP157_IN_AAAG(.(T542, T546)) → APP157_IN_AAAG(T546)
    The graph contains the following edges 1 > 1

(22) YES

(23) Obligation:

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

APP131_IN_AGAG(.(T433, T438), T435, T439, .(T433, T437)) → APP131_IN_AGAG(T438, T435, T439, T437)

The TRS R consists of the following rules:

lessc13_in_aa(0, s(T38)) → lessc13_out_aa(0, s(T38))
lessc13_in_aa(s(T45), s(T46)) → U68_aa(T45, T46, lessc13_in_aa(T45, T46))
U68_aa(T45, T46, lessc13_out_aa(T45, T46)) → lessc13_out_aa(s(T45), s(T46))
lessc13_in_ga(0, s(T38)) → lessc13_out_ga(0, s(T38))
lessc13_in_ga(s(T45), s(T46)) → U68_ga(T45, T46, lessc13_in_ga(T45, T46))
U68_ga(T45, T46, lessc13_out_ga(T45, T46)) → lessc13_out_ga(s(T45), s(T46))
partc23_in_gaaa(T70, .(T73, T77), .(T73, X123), X124) → U69_gaaa(T70, T73, T77, X123, X124, lessc13_in_ga(T70, T73))
U69_gaaa(T70, T73, T77, X123, X124, lessc13_out_ga(T70, T73)) → U70_gaaa(T70, T73, T77, X123, X124, partc23_in_gaaa(T70, T77, X123, X124))
partc23_in_gaaa(T95, .(T96, T98), X174, .(T96, X175)) → U71_gaaa(T95, T96, T98, X174, X175, partc23_in_gaaa(T95, T98, X174, X175))
partc23_in_gaaa(T104, [], [], []) → partc23_out_gaaa(T104, [], [], [])
U71_gaaa(T95, T96, T98, X174, X175, partc23_out_gaaa(T95, T98, X174, X175)) → partc23_out_gaaa(T95, .(T96, T98), X174, .(T96, X175))
U70_gaaa(T70, T73, T77, X123, X124, partc23_out_gaaa(T70, T77, X123, X124)) → partc23_out_gaaa(T70, .(T73, T77), .(T73, X123), X124)
partc44_in_aaaa(T153, .(T149, T154), .(T149, X282), X283) → U72_aaaa(T153, T149, T154, X282, X283, lessc13_in_aa(T153, T149))
U72_aaaa(T153, T149, T154, X282, X283, lessc13_out_aa(T153, T149)) → U73_aaaa(T153, T149, T154, X282, X283, partc23_in_gaaa(T153, T154, X282, X283))
U73_aaaa(T153, T149, T154, X282, X283, partc23_out_gaaa(T153, T154, X282, X283)) → partc44_out_aaaa(T153, .(T149, T154), .(T149, X282), X283)
partc44_in_aaaa(T175, .(T173, T176), X333, .(T173, X334)) → U74_aaaa(T175, T173, T176, X333, X334, partc44_in_aaaa(T175, T176, X333, X334))
partc44_in_aaaa(T182, [], [], []) → partc44_out_aaaa(T182, [], [], [])
U74_aaaa(T175, T173, T176, X333, X334, partc44_out_aaaa(T175, T176, X333, X334)) → partc44_out_aaaa(T175, .(T173, T176), X333, .(T173, X334))
qsc60_in_aa([], []) → qsc60_out_aa([], [])
qsc60_in_aa(.(T192, T193), X370) → U79_aa(T192, T193, X370, qc43_in_aaaaaaa(T192, T193, X366, X367, X368, X369, X370))
qc43_in_aaaaaaa(T199, T123, T127, T184, T198, T197, X234) → U75_aaaaaaa(T199, T123, T127, T184, T198, T197, X234, partc44_in_aaaa(T199, T123, T127, T184))
U75_aaaaaaa(T199, T123, T127, T184, T198, T197, X234, partc44_out_aaaa(T199, T123, T127, T184)) → U76_aaaaaaa(T199, T123, T127, T184, T198, T197, X234, qsc60_in_aa(T127, T198))
U76_aaaaaaa(T199, T123, T127, T184, T198, T197, X234, qsc60_out_aa(T127, T198)) → U77_aaaaaaa(T199, T123, T127, T184, T198, T197, X234, qsc60_in_aa(T184, T197))
U77_aaaaaaa(T199, T123, T127, T184, T198, T197, X234, qsc60_out_aa(T184, T197)) → U78_aaaaaaa(T199, T123, T127, T184, T198, T197, X234, appc71_in_aaaa(T198, T199, T197, X234))
appc71_in_aaaa([], T212, T213, .(T212, T213)) → appc71_out_aaaa([], T212, T213, .(T212, T213))
appc71_in_aaaa(.(T222, T226), T227, T228, .(T222, X403)) → U80_aaaa(T222, T226, T227, T228, X403, appc71_in_aaaa(T226, T227, T228, X403))
U80_aaaa(T222, T226, T227, T228, X403, appc71_out_aaaa(T226, T227, T228, X403)) → appc71_out_aaaa(.(T222, T226), T227, T228, .(T222, X403))
U78_aaaaaaa(T199, T123, T127, T184, T198, T197, X234, appc71_out_aaaa(T198, T199, T197, X234)) → qc43_out_aaaaaaa(T199, T123, T127, T184, T198, T197, X234)
U79_aa(T192, T193, X370, qc43_out_aaaaaaa(T192, T193, X366, X367, X368, X369, X370)) → qsc60_out_aa(.(T192, T193), X370)
qsc39_in_aaa(T122, T123, X234) → U81_aaa(T122, T123, X234, qc43_in_aaaaaaa(T122, T123, X230, X231, X232, X233, X234))
U81_aaa(T122, T123, X234, qc43_out_aaaaaaa(T122, T123, X230, X231, X232, X233, X234)) → qsc39_out_aaa(T122, T123, X234)
qsc100_in_a([]) → qsc100_out_a([])

The argument filtering Pi contains the following mapping:
[]  =  []
lessc13_in_aa(x1, x2)  =  lessc13_in_aa
lessc13_out_aa(x1, x2)  =  lessc13_out_aa(x1)
U68_aa(x1, x2, x3)  =  U68_aa(x3)
s(x1)  =  s(x1)
lessc13_in_ga(x1, x2)  =  lessc13_in_ga(x1)
0  =  0
lessc13_out_ga(x1, x2)  =  lessc13_out_ga(x1)
U68_ga(x1, x2, x3)  =  U68_ga(x1, x3)
partc23_in_gaaa(x1, x2, x3, x4)  =  partc23_in_gaaa(x1)
U69_gaaa(x1, x2, x3, x4, x5, x6)  =  U69_gaaa(x1, x6)
U70_gaaa(x1, x2, x3, x4, x5, x6)  =  U70_gaaa(x1, x6)
U71_gaaa(x1, x2, x3, x4, x5, x6)  =  U71_gaaa(x1, x6)
partc23_out_gaaa(x1, x2, x3, x4)  =  partc23_out_gaaa(x1)
partc44_in_aaaa(x1, x2, x3, x4)  =  partc44_in_aaaa
U72_aaaa(x1, x2, x3, x4, x5, x6)  =  U72_aaaa(x6)
U73_aaaa(x1, x2, x3, x4, x5, x6)  =  U73_aaaa(x6)
partc44_out_aaaa(x1, x2, x3, x4)  =  partc44_out_aaaa
U74_aaaa(x1, x2, x3, x4, x5, x6)  =  U74_aaaa(x6)
qsc60_in_aa(x1, x2)  =  qsc60_in_aa
qsc60_out_aa(x1, x2)  =  qsc60_out_aa
U79_aa(x1, x2, x3, x4)  =  U79_aa(x4)
qc43_in_aaaaaaa(x1, x2, x3, x4, x5, x6, x7)  =  qc43_in_aaaaaaa
U75_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  U75_aaaaaaa(x8)
U76_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  U76_aaaaaaa(x8)
U77_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  U77_aaaaaaa(x8)
U78_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  U78_aaaaaaa(x8)
.(x1, x2)  =  .(x1, x2)
qc43_out_aaaaaaa(x1, x2, x3, x4, x5, x6, x7)  =  qc43_out_aaaaaaa
appc71_in_aaaa(x1, x2, x3, x4)  =  appc71_in_aaaa
appc71_out_aaaa(x1, x2, x3, x4)  =  appc71_out_aaaa
U80_aaaa(x1, x2, x3, x4, x5, x6)  =  U80_aaaa(x6)
qsc39_in_aaa(x1, x2, x3)  =  qsc39_in_aaa
U81_aaa(x1, x2, x3, x4)  =  U81_aaa(x4)
qsc39_out_aaa(x1, x2, x3)  =  qsc39_out_aaa
qsc100_in_a(x1)  =  qsc100_in_a
qsc100_out_a(x1)  =  qsc100_out_a(x1)
APP131_IN_AGAG(x1, x2, x3, x4)  =  APP131_IN_AGAG(x2, x4)

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

(24) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(25) Obligation:

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

APP131_IN_AGAG(.(T433, T438), T435, T439, .(T433, T437)) → APP131_IN_AGAG(T438, T435, T439, T437)

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

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

(26) PiDPToQDPProof (SOUND transformation)

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

(27) Obligation:

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

APP131_IN_AGAG(T435, .(T433, T437)) → APP131_IN_AGAG(T435, T437)

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

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

  • APP131_IN_AGAG(T435, .(T433, T437)) → APP131_IN_AGAG(T435, T437)
    The graph contains the following edges 1 >= 1, 2 > 2

(29) YES

(30) Obligation:

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

APP71_IN_AAAA(.(T222, T226), T227, T228, .(T222, X403)) → APP71_IN_AAAA(T226, T227, T228, X403)

The TRS R consists of the following rules:

lessc13_in_aa(0, s(T38)) → lessc13_out_aa(0, s(T38))
lessc13_in_aa(s(T45), s(T46)) → U68_aa(T45, T46, lessc13_in_aa(T45, T46))
U68_aa(T45, T46, lessc13_out_aa(T45, T46)) → lessc13_out_aa(s(T45), s(T46))
lessc13_in_ga(0, s(T38)) → lessc13_out_ga(0, s(T38))
lessc13_in_ga(s(T45), s(T46)) → U68_ga(T45, T46, lessc13_in_ga(T45, T46))
U68_ga(T45, T46, lessc13_out_ga(T45, T46)) → lessc13_out_ga(s(T45), s(T46))
partc23_in_gaaa(T70, .(T73, T77), .(T73, X123), X124) → U69_gaaa(T70, T73, T77, X123, X124, lessc13_in_ga(T70, T73))
U69_gaaa(T70, T73, T77, X123, X124, lessc13_out_ga(T70, T73)) → U70_gaaa(T70, T73, T77, X123, X124, partc23_in_gaaa(T70, T77, X123, X124))
partc23_in_gaaa(T95, .(T96, T98), X174, .(T96, X175)) → U71_gaaa(T95, T96, T98, X174, X175, partc23_in_gaaa(T95, T98, X174, X175))
partc23_in_gaaa(T104, [], [], []) → partc23_out_gaaa(T104, [], [], [])
U71_gaaa(T95, T96, T98, X174, X175, partc23_out_gaaa(T95, T98, X174, X175)) → partc23_out_gaaa(T95, .(T96, T98), X174, .(T96, X175))
U70_gaaa(T70, T73, T77, X123, X124, partc23_out_gaaa(T70, T77, X123, X124)) → partc23_out_gaaa(T70, .(T73, T77), .(T73, X123), X124)
partc44_in_aaaa(T153, .(T149, T154), .(T149, X282), X283) → U72_aaaa(T153, T149, T154, X282, X283, lessc13_in_aa(T153, T149))
U72_aaaa(T153, T149, T154, X282, X283, lessc13_out_aa(T153, T149)) → U73_aaaa(T153, T149, T154, X282, X283, partc23_in_gaaa(T153, T154, X282, X283))
U73_aaaa(T153, T149, T154, X282, X283, partc23_out_gaaa(T153, T154, X282, X283)) → partc44_out_aaaa(T153, .(T149, T154), .(T149, X282), X283)
partc44_in_aaaa(T175, .(T173, T176), X333, .(T173, X334)) → U74_aaaa(T175, T173, T176, X333, X334, partc44_in_aaaa(T175, T176, X333, X334))
partc44_in_aaaa(T182, [], [], []) → partc44_out_aaaa(T182, [], [], [])
U74_aaaa(T175, T173, T176, X333, X334, partc44_out_aaaa(T175, T176, X333, X334)) → partc44_out_aaaa(T175, .(T173, T176), X333, .(T173, X334))
qsc60_in_aa([], []) → qsc60_out_aa([], [])
qsc60_in_aa(.(T192, T193), X370) → U79_aa(T192, T193, X370, qc43_in_aaaaaaa(T192, T193, X366, X367, X368, X369, X370))
qc43_in_aaaaaaa(T199, T123, T127, T184, T198, T197, X234) → U75_aaaaaaa(T199, T123, T127, T184, T198, T197, X234, partc44_in_aaaa(T199, T123, T127, T184))
U75_aaaaaaa(T199, T123, T127, T184, T198, T197, X234, partc44_out_aaaa(T199, T123, T127, T184)) → U76_aaaaaaa(T199, T123, T127, T184, T198, T197, X234, qsc60_in_aa(T127, T198))
U76_aaaaaaa(T199, T123, T127, T184, T198, T197, X234, qsc60_out_aa(T127, T198)) → U77_aaaaaaa(T199, T123, T127, T184, T198, T197, X234, qsc60_in_aa(T184, T197))
U77_aaaaaaa(T199, T123, T127, T184, T198, T197, X234, qsc60_out_aa(T184, T197)) → U78_aaaaaaa(T199, T123, T127, T184, T198, T197, X234, appc71_in_aaaa(T198, T199, T197, X234))
appc71_in_aaaa([], T212, T213, .(T212, T213)) → appc71_out_aaaa([], T212, T213, .(T212, T213))
appc71_in_aaaa(.(T222, T226), T227, T228, .(T222, X403)) → U80_aaaa(T222, T226, T227, T228, X403, appc71_in_aaaa(T226, T227, T228, X403))
U80_aaaa(T222, T226, T227, T228, X403, appc71_out_aaaa(T226, T227, T228, X403)) → appc71_out_aaaa(.(T222, T226), T227, T228, .(T222, X403))
U78_aaaaaaa(T199, T123, T127, T184, T198, T197, X234, appc71_out_aaaa(T198, T199, T197, X234)) → qc43_out_aaaaaaa(T199, T123, T127, T184, T198, T197, X234)
U79_aa(T192, T193, X370, qc43_out_aaaaaaa(T192, T193, X366, X367, X368, X369, X370)) → qsc60_out_aa(.(T192, T193), X370)
qsc39_in_aaa(T122, T123, X234) → U81_aaa(T122, T123, X234, qc43_in_aaaaaaa(T122, T123, X230, X231, X232, X233, X234))
U81_aaa(T122, T123, X234, qc43_out_aaaaaaa(T122, T123, X230, X231, X232, X233, X234)) → qsc39_out_aaa(T122, T123, X234)
qsc100_in_a([]) → qsc100_out_a([])

The argument filtering Pi contains the following mapping:
[]  =  []
lessc13_in_aa(x1, x2)  =  lessc13_in_aa
lessc13_out_aa(x1, x2)  =  lessc13_out_aa(x1)
U68_aa(x1, x2, x3)  =  U68_aa(x3)
s(x1)  =  s(x1)
lessc13_in_ga(x1, x2)  =  lessc13_in_ga(x1)
0  =  0
lessc13_out_ga(x1, x2)  =  lessc13_out_ga(x1)
U68_ga(x1, x2, x3)  =  U68_ga(x1, x3)
partc23_in_gaaa(x1, x2, x3, x4)  =  partc23_in_gaaa(x1)
U69_gaaa(x1, x2, x3, x4, x5, x6)  =  U69_gaaa(x1, x6)
U70_gaaa(x1, x2, x3, x4, x5, x6)  =  U70_gaaa(x1, x6)
U71_gaaa(x1, x2, x3, x4, x5, x6)  =  U71_gaaa(x1, x6)
partc23_out_gaaa(x1, x2, x3, x4)  =  partc23_out_gaaa(x1)
partc44_in_aaaa(x1, x2, x3, x4)  =  partc44_in_aaaa
U72_aaaa(x1, x2, x3, x4, x5, x6)  =  U72_aaaa(x6)
U73_aaaa(x1, x2, x3, x4, x5, x6)  =  U73_aaaa(x6)
partc44_out_aaaa(x1, x2, x3, x4)  =  partc44_out_aaaa
U74_aaaa(x1, x2, x3, x4, x5, x6)  =  U74_aaaa(x6)
qsc60_in_aa(x1, x2)  =  qsc60_in_aa
qsc60_out_aa(x1, x2)  =  qsc60_out_aa
U79_aa(x1, x2, x3, x4)  =  U79_aa(x4)
qc43_in_aaaaaaa(x1, x2, x3, x4, x5, x6, x7)  =  qc43_in_aaaaaaa
U75_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  U75_aaaaaaa(x8)
U76_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  U76_aaaaaaa(x8)
U77_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  U77_aaaaaaa(x8)
U78_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  U78_aaaaaaa(x8)
.(x1, x2)  =  .(x1, x2)
qc43_out_aaaaaaa(x1, x2, x3, x4, x5, x6, x7)  =  qc43_out_aaaaaaa
appc71_in_aaaa(x1, x2, x3, x4)  =  appc71_in_aaaa
appc71_out_aaaa(x1, x2, x3, x4)  =  appc71_out_aaaa
U80_aaaa(x1, x2, x3, x4, x5, x6)  =  U80_aaaa(x6)
qsc39_in_aaa(x1, x2, x3)  =  qsc39_in_aaa
U81_aaa(x1, x2, x3, x4)  =  U81_aaa(x4)
qsc39_out_aaa(x1, x2, x3)  =  qsc39_out_aaa
qsc100_in_a(x1)  =  qsc100_in_a
qsc100_out_a(x1)  =  qsc100_out_a(x1)
APP71_IN_AAAA(x1, x2, x3, x4)  =  APP71_IN_AAAA

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

(31) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(32) Obligation:

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

APP71_IN_AAAA(.(T222, T226), T227, T228, .(T222, X403)) → APP71_IN_AAAA(T226, T227, T228, X403)

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

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:

APP71_IN_AAAAAPP71_IN_AAAA

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

(35) NonTerminationProof (EQUIVALENT transformation)

We used the non-termination processor [FROCOS05] to show that the DP problem is infinite.
Found a loop by semiunifying a rule from P directly.

s = APP71_IN_AAAA evaluates to t =APP71_IN_AAAA

Thus s starts an infinite chain as s semiunifies with t with the following substitutions:
  • Matcher: [ ]
  • Semiunifier: [ ]




Rewriting sequence

The DP semiunifies directly so there is only one rewrite step from APP71_IN_AAAA to APP71_IN_AAAA.



(36) NO

(37) Obligation:

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

LESS13_IN_GA(s(T45), s(T46)) → LESS13_IN_GA(T45, T46)

The TRS R consists of the following rules:

lessc13_in_aa(0, s(T38)) → lessc13_out_aa(0, s(T38))
lessc13_in_aa(s(T45), s(T46)) → U68_aa(T45, T46, lessc13_in_aa(T45, T46))
U68_aa(T45, T46, lessc13_out_aa(T45, T46)) → lessc13_out_aa(s(T45), s(T46))
lessc13_in_ga(0, s(T38)) → lessc13_out_ga(0, s(T38))
lessc13_in_ga(s(T45), s(T46)) → U68_ga(T45, T46, lessc13_in_ga(T45, T46))
U68_ga(T45, T46, lessc13_out_ga(T45, T46)) → lessc13_out_ga(s(T45), s(T46))
partc23_in_gaaa(T70, .(T73, T77), .(T73, X123), X124) → U69_gaaa(T70, T73, T77, X123, X124, lessc13_in_ga(T70, T73))
U69_gaaa(T70, T73, T77, X123, X124, lessc13_out_ga(T70, T73)) → U70_gaaa(T70, T73, T77, X123, X124, partc23_in_gaaa(T70, T77, X123, X124))
partc23_in_gaaa(T95, .(T96, T98), X174, .(T96, X175)) → U71_gaaa(T95, T96, T98, X174, X175, partc23_in_gaaa(T95, T98, X174, X175))
partc23_in_gaaa(T104, [], [], []) → partc23_out_gaaa(T104, [], [], [])
U71_gaaa(T95, T96, T98, X174, X175, partc23_out_gaaa(T95, T98, X174, X175)) → partc23_out_gaaa(T95, .(T96, T98), X174, .(T96, X175))
U70_gaaa(T70, T73, T77, X123, X124, partc23_out_gaaa(T70, T77, X123, X124)) → partc23_out_gaaa(T70, .(T73, T77), .(T73, X123), X124)
partc44_in_aaaa(T153, .(T149, T154), .(T149, X282), X283) → U72_aaaa(T153, T149, T154, X282, X283, lessc13_in_aa(T153, T149))
U72_aaaa(T153, T149, T154, X282, X283, lessc13_out_aa(T153, T149)) → U73_aaaa(T153, T149, T154, X282, X283, partc23_in_gaaa(T153, T154, X282, X283))
U73_aaaa(T153, T149, T154, X282, X283, partc23_out_gaaa(T153, T154, X282, X283)) → partc44_out_aaaa(T153, .(T149, T154), .(T149, X282), X283)
partc44_in_aaaa(T175, .(T173, T176), X333, .(T173, X334)) → U74_aaaa(T175, T173, T176, X333, X334, partc44_in_aaaa(T175, T176, X333, X334))
partc44_in_aaaa(T182, [], [], []) → partc44_out_aaaa(T182, [], [], [])
U74_aaaa(T175, T173, T176, X333, X334, partc44_out_aaaa(T175, T176, X333, X334)) → partc44_out_aaaa(T175, .(T173, T176), X333, .(T173, X334))
qsc60_in_aa([], []) → qsc60_out_aa([], [])
qsc60_in_aa(.(T192, T193), X370) → U79_aa(T192, T193, X370, qc43_in_aaaaaaa(T192, T193, X366, X367, X368, X369, X370))
qc43_in_aaaaaaa(T199, T123, T127, T184, T198, T197, X234) → U75_aaaaaaa(T199, T123, T127, T184, T198, T197, X234, partc44_in_aaaa(T199, T123, T127, T184))
U75_aaaaaaa(T199, T123, T127, T184, T198, T197, X234, partc44_out_aaaa(T199, T123, T127, T184)) → U76_aaaaaaa(T199, T123, T127, T184, T198, T197, X234, qsc60_in_aa(T127, T198))
U76_aaaaaaa(T199, T123, T127, T184, T198, T197, X234, qsc60_out_aa(T127, T198)) → U77_aaaaaaa(T199, T123, T127, T184, T198, T197, X234, qsc60_in_aa(T184, T197))
U77_aaaaaaa(T199, T123, T127, T184, T198, T197, X234, qsc60_out_aa(T184, T197)) → U78_aaaaaaa(T199, T123, T127, T184, T198, T197, X234, appc71_in_aaaa(T198, T199, T197, X234))
appc71_in_aaaa([], T212, T213, .(T212, T213)) → appc71_out_aaaa([], T212, T213, .(T212, T213))
appc71_in_aaaa(.(T222, T226), T227, T228, .(T222, X403)) → U80_aaaa(T222, T226, T227, T228, X403, appc71_in_aaaa(T226, T227, T228, X403))
U80_aaaa(T222, T226, T227, T228, X403, appc71_out_aaaa(T226, T227, T228, X403)) → appc71_out_aaaa(.(T222, T226), T227, T228, .(T222, X403))
U78_aaaaaaa(T199, T123, T127, T184, T198, T197, X234, appc71_out_aaaa(T198, T199, T197, X234)) → qc43_out_aaaaaaa(T199, T123, T127, T184, T198, T197, X234)
U79_aa(T192, T193, X370, qc43_out_aaaaaaa(T192, T193, X366, X367, X368, X369, X370)) → qsc60_out_aa(.(T192, T193), X370)
qsc39_in_aaa(T122, T123, X234) → U81_aaa(T122, T123, X234, qc43_in_aaaaaaa(T122, T123, X230, X231, X232, X233, X234))
U81_aaa(T122, T123, X234, qc43_out_aaaaaaa(T122, T123, X230, X231, X232, X233, X234)) → qsc39_out_aaa(T122, T123, X234)
qsc100_in_a([]) → qsc100_out_a([])

The argument filtering Pi contains the following mapping:
[]  =  []
lessc13_in_aa(x1, x2)  =  lessc13_in_aa
lessc13_out_aa(x1, x2)  =  lessc13_out_aa(x1)
U68_aa(x1, x2, x3)  =  U68_aa(x3)
s(x1)  =  s(x1)
lessc13_in_ga(x1, x2)  =  lessc13_in_ga(x1)
0  =  0
lessc13_out_ga(x1, x2)  =  lessc13_out_ga(x1)
U68_ga(x1, x2, x3)  =  U68_ga(x1, x3)
partc23_in_gaaa(x1, x2, x3, x4)  =  partc23_in_gaaa(x1)
U69_gaaa(x1, x2, x3, x4, x5, x6)  =  U69_gaaa(x1, x6)
U70_gaaa(x1, x2, x3, x4, x5, x6)  =  U70_gaaa(x1, x6)
U71_gaaa(x1, x2, x3, x4, x5, x6)  =  U71_gaaa(x1, x6)
partc23_out_gaaa(x1, x2, x3, x4)  =  partc23_out_gaaa(x1)
partc44_in_aaaa(x1, x2, x3, x4)  =  partc44_in_aaaa
U72_aaaa(x1, x2, x3, x4, x5, x6)  =  U72_aaaa(x6)
U73_aaaa(x1, x2, x3, x4, x5, x6)  =  U73_aaaa(x6)
partc44_out_aaaa(x1, x2, x3, x4)  =  partc44_out_aaaa
U74_aaaa(x1, x2, x3, x4, x5, x6)  =  U74_aaaa(x6)
qsc60_in_aa(x1, x2)  =  qsc60_in_aa
qsc60_out_aa(x1, x2)  =  qsc60_out_aa
U79_aa(x1, x2, x3, x4)  =  U79_aa(x4)
qc43_in_aaaaaaa(x1, x2, x3, x4, x5, x6, x7)  =  qc43_in_aaaaaaa
U75_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  U75_aaaaaaa(x8)
U76_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  U76_aaaaaaa(x8)
U77_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  U77_aaaaaaa(x8)
U78_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  U78_aaaaaaa(x8)
.(x1, x2)  =  .(x1, x2)
qc43_out_aaaaaaa(x1, x2, x3, x4, x5, x6, x7)  =  qc43_out_aaaaaaa
appc71_in_aaaa(x1, x2, x3, x4)  =  appc71_in_aaaa
appc71_out_aaaa(x1, x2, x3, x4)  =  appc71_out_aaaa
U80_aaaa(x1, x2, x3, x4, x5, x6)  =  U80_aaaa(x6)
qsc39_in_aaa(x1, x2, x3)  =  qsc39_in_aaa
U81_aaa(x1, x2, x3, x4)  =  U81_aaa(x4)
qsc39_out_aaa(x1, x2, x3)  =  qsc39_out_aaa
qsc100_in_a(x1)  =  qsc100_in_a
qsc100_out_a(x1)  =  qsc100_out_a(x1)
LESS13_IN_GA(x1, x2)  =  LESS13_IN_GA(x1)

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

(38) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(39) Obligation:

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

LESS13_IN_GA(s(T45), s(T46)) → LESS13_IN_GA(T45, T46)

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

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

(40) PiDPToQDPProof (SOUND transformation)

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

(41) Obligation:

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

LESS13_IN_GA(s(T45)) → LESS13_IN_GA(T45)

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

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

  • LESS13_IN_GA(s(T45)) → LESS13_IN_GA(T45)
    The graph contains the following edges 1 > 1

(43) YES

(44) Obligation:

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

PART23_IN_GAAA(T70, .(T73, T77), .(T73, X123), X124) → U3_GAAA(T70, T73, T77, X123, X124, lessc13_in_ga(T70, T73))
U3_GAAA(T70, T73, T77, X123, X124, lessc13_out_ga(T70, T73)) → PART23_IN_GAAA(T70, T77, X123, X124)
PART23_IN_GAAA(T95, .(T96, T98), X174, .(T96, X175)) → PART23_IN_GAAA(T95, T98, X174, X175)

The TRS R consists of the following rules:

lessc13_in_aa(0, s(T38)) → lessc13_out_aa(0, s(T38))
lessc13_in_aa(s(T45), s(T46)) → U68_aa(T45, T46, lessc13_in_aa(T45, T46))
U68_aa(T45, T46, lessc13_out_aa(T45, T46)) → lessc13_out_aa(s(T45), s(T46))
lessc13_in_ga(0, s(T38)) → lessc13_out_ga(0, s(T38))
lessc13_in_ga(s(T45), s(T46)) → U68_ga(T45, T46, lessc13_in_ga(T45, T46))
U68_ga(T45, T46, lessc13_out_ga(T45, T46)) → lessc13_out_ga(s(T45), s(T46))
partc23_in_gaaa(T70, .(T73, T77), .(T73, X123), X124) → U69_gaaa(T70, T73, T77, X123, X124, lessc13_in_ga(T70, T73))
U69_gaaa(T70, T73, T77, X123, X124, lessc13_out_ga(T70, T73)) → U70_gaaa(T70, T73, T77, X123, X124, partc23_in_gaaa(T70, T77, X123, X124))
partc23_in_gaaa(T95, .(T96, T98), X174, .(T96, X175)) → U71_gaaa(T95, T96, T98, X174, X175, partc23_in_gaaa(T95, T98, X174, X175))
partc23_in_gaaa(T104, [], [], []) → partc23_out_gaaa(T104, [], [], [])
U71_gaaa(T95, T96, T98, X174, X175, partc23_out_gaaa(T95, T98, X174, X175)) → partc23_out_gaaa(T95, .(T96, T98), X174, .(T96, X175))
U70_gaaa(T70, T73, T77, X123, X124, partc23_out_gaaa(T70, T77, X123, X124)) → partc23_out_gaaa(T70, .(T73, T77), .(T73, X123), X124)
partc44_in_aaaa(T153, .(T149, T154), .(T149, X282), X283) → U72_aaaa(T153, T149, T154, X282, X283, lessc13_in_aa(T153, T149))
U72_aaaa(T153, T149, T154, X282, X283, lessc13_out_aa(T153, T149)) → U73_aaaa(T153, T149, T154, X282, X283, partc23_in_gaaa(T153, T154, X282, X283))
U73_aaaa(T153, T149, T154, X282, X283, partc23_out_gaaa(T153, T154, X282, X283)) → partc44_out_aaaa(T153, .(T149, T154), .(T149, X282), X283)
partc44_in_aaaa(T175, .(T173, T176), X333, .(T173, X334)) → U74_aaaa(T175, T173, T176, X333, X334, partc44_in_aaaa(T175, T176, X333, X334))
partc44_in_aaaa(T182, [], [], []) → partc44_out_aaaa(T182, [], [], [])
U74_aaaa(T175, T173, T176, X333, X334, partc44_out_aaaa(T175, T176, X333, X334)) → partc44_out_aaaa(T175, .(T173, T176), X333, .(T173, X334))
qsc60_in_aa([], []) → qsc60_out_aa([], [])
qsc60_in_aa(.(T192, T193), X370) → U79_aa(T192, T193, X370, qc43_in_aaaaaaa(T192, T193, X366, X367, X368, X369, X370))
qc43_in_aaaaaaa(T199, T123, T127, T184, T198, T197, X234) → U75_aaaaaaa(T199, T123, T127, T184, T198, T197, X234, partc44_in_aaaa(T199, T123, T127, T184))
U75_aaaaaaa(T199, T123, T127, T184, T198, T197, X234, partc44_out_aaaa(T199, T123, T127, T184)) → U76_aaaaaaa(T199, T123, T127, T184, T198, T197, X234, qsc60_in_aa(T127, T198))
U76_aaaaaaa(T199, T123, T127, T184, T198, T197, X234, qsc60_out_aa(T127, T198)) → U77_aaaaaaa(T199, T123, T127, T184, T198, T197, X234, qsc60_in_aa(T184, T197))
U77_aaaaaaa(T199, T123, T127, T184, T198, T197, X234, qsc60_out_aa(T184, T197)) → U78_aaaaaaa(T199, T123, T127, T184, T198, T197, X234, appc71_in_aaaa(T198, T199, T197, X234))
appc71_in_aaaa([], T212, T213, .(T212, T213)) → appc71_out_aaaa([], T212, T213, .(T212, T213))
appc71_in_aaaa(.(T222, T226), T227, T228, .(T222, X403)) → U80_aaaa(T222, T226, T227, T228, X403, appc71_in_aaaa(T226, T227, T228, X403))
U80_aaaa(T222, T226, T227, T228, X403, appc71_out_aaaa(T226, T227, T228, X403)) → appc71_out_aaaa(.(T222, T226), T227, T228, .(T222, X403))
U78_aaaaaaa(T199, T123, T127, T184, T198, T197, X234, appc71_out_aaaa(T198, T199, T197, X234)) → qc43_out_aaaaaaa(T199, T123, T127, T184, T198, T197, X234)
U79_aa(T192, T193, X370, qc43_out_aaaaaaa(T192, T193, X366, X367, X368, X369, X370)) → qsc60_out_aa(.(T192, T193), X370)
qsc39_in_aaa(T122, T123, X234) → U81_aaa(T122, T123, X234, qc43_in_aaaaaaa(T122, T123, X230, X231, X232, X233, X234))
U81_aaa(T122, T123, X234, qc43_out_aaaaaaa(T122, T123, X230, X231, X232, X233, X234)) → qsc39_out_aaa(T122, T123, X234)
qsc100_in_a([]) → qsc100_out_a([])

The argument filtering Pi contains the following mapping:
[]  =  []
lessc13_in_aa(x1, x2)  =  lessc13_in_aa
lessc13_out_aa(x1, x2)  =  lessc13_out_aa(x1)
U68_aa(x1, x2, x3)  =  U68_aa(x3)
s(x1)  =  s(x1)
lessc13_in_ga(x1, x2)  =  lessc13_in_ga(x1)
0  =  0
lessc13_out_ga(x1, x2)  =  lessc13_out_ga(x1)
U68_ga(x1, x2, x3)  =  U68_ga(x1, x3)
partc23_in_gaaa(x1, x2, x3, x4)  =  partc23_in_gaaa(x1)
U69_gaaa(x1, x2, x3, x4, x5, x6)  =  U69_gaaa(x1, x6)
U70_gaaa(x1, x2, x3, x4, x5, x6)  =  U70_gaaa(x1, x6)
U71_gaaa(x1, x2, x3, x4, x5, x6)  =  U71_gaaa(x1, x6)
partc23_out_gaaa(x1, x2, x3, x4)  =  partc23_out_gaaa(x1)
partc44_in_aaaa(x1, x2, x3, x4)  =  partc44_in_aaaa
U72_aaaa(x1, x2, x3, x4, x5, x6)  =  U72_aaaa(x6)
U73_aaaa(x1, x2, x3, x4, x5, x6)  =  U73_aaaa(x6)
partc44_out_aaaa(x1, x2, x3, x4)  =  partc44_out_aaaa
U74_aaaa(x1, x2, x3, x4, x5, x6)  =  U74_aaaa(x6)
qsc60_in_aa(x1, x2)  =  qsc60_in_aa
qsc60_out_aa(x1, x2)  =  qsc60_out_aa
U79_aa(x1, x2, x3, x4)  =  U79_aa(x4)
qc43_in_aaaaaaa(x1, x2, x3, x4, x5, x6, x7)  =  qc43_in_aaaaaaa
U75_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  U75_aaaaaaa(x8)
U76_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  U76_aaaaaaa(x8)
U77_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  U77_aaaaaaa(x8)
U78_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  U78_aaaaaaa(x8)
.(x1, x2)  =  .(x1, x2)
qc43_out_aaaaaaa(x1, x2, x3, x4, x5, x6, x7)  =  qc43_out_aaaaaaa
appc71_in_aaaa(x1, x2, x3, x4)  =  appc71_in_aaaa
appc71_out_aaaa(x1, x2, x3, x4)  =  appc71_out_aaaa
U80_aaaa(x1, x2, x3, x4, x5, x6)  =  U80_aaaa(x6)
qsc39_in_aaa(x1, x2, x3)  =  qsc39_in_aaa
U81_aaa(x1, x2, x3, x4)  =  U81_aaa(x4)
qsc39_out_aaa(x1, x2, x3)  =  qsc39_out_aaa
qsc100_in_a(x1)  =  qsc100_in_a
qsc100_out_a(x1)  =  qsc100_out_a(x1)
PART23_IN_GAAA(x1, x2, x3, x4)  =  PART23_IN_GAAA(x1)
U3_GAAA(x1, x2, x3, x4, x5, x6)  =  U3_GAAA(x1, x6)

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

(45) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(46) Obligation:

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

PART23_IN_GAAA(T70, .(T73, T77), .(T73, X123), X124) → U3_GAAA(T70, T73, T77, X123, X124, lessc13_in_ga(T70, T73))
U3_GAAA(T70, T73, T77, X123, X124, lessc13_out_ga(T70, T73)) → PART23_IN_GAAA(T70, T77, X123, X124)
PART23_IN_GAAA(T95, .(T96, T98), X174, .(T96, X175)) → PART23_IN_GAAA(T95, T98, X174, X175)

The TRS R consists of the following rules:

lessc13_in_ga(0, s(T38)) → lessc13_out_ga(0, s(T38))
lessc13_in_ga(s(T45), s(T46)) → U68_ga(T45, T46, lessc13_in_ga(T45, T46))
U68_ga(T45, T46, lessc13_out_ga(T45, T46)) → lessc13_out_ga(s(T45), s(T46))

The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
lessc13_in_ga(x1, x2)  =  lessc13_in_ga(x1)
0  =  0
lessc13_out_ga(x1, x2)  =  lessc13_out_ga(x1)
U68_ga(x1, x2, x3)  =  U68_ga(x1, x3)
.(x1, x2)  =  .(x1, x2)
PART23_IN_GAAA(x1, x2, x3, x4)  =  PART23_IN_GAAA(x1)
U3_GAAA(x1, x2, x3, x4, x5, x6)  =  U3_GAAA(x1, x6)

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

(47) PiDPToQDPProof (SOUND transformation)

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

(48) Obligation:

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

PART23_IN_GAAA(T70) → U3_GAAA(T70, lessc13_in_ga(T70))
U3_GAAA(T70, lessc13_out_ga(T70)) → PART23_IN_GAAA(T70)
PART23_IN_GAAA(T95) → PART23_IN_GAAA(T95)

The TRS R consists of the following rules:

lessc13_in_ga(0) → lessc13_out_ga(0)
lessc13_in_ga(s(T45)) → U68_ga(T45, lessc13_in_ga(T45))
U68_ga(T45, lessc13_out_ga(T45)) → lessc13_out_ga(s(T45))

The set Q consists of the following terms:

lessc13_in_ga(x0)
U68_ga(x0, x1)

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

(49) Narrowing (SOUND transformation)

By narrowing [LPAR04] the rule PART23_IN_GAAA(T70) → U3_GAAA(T70, lessc13_in_ga(T70)) at position [1] we obtained the following new rules [LPAR04]:

PART23_IN_GAAA(0) → U3_GAAA(0, lessc13_out_ga(0))
PART23_IN_GAAA(s(x0)) → U3_GAAA(s(x0), U68_ga(x0, lessc13_in_ga(x0)))

(50) Obligation:

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

U3_GAAA(T70, lessc13_out_ga(T70)) → PART23_IN_GAAA(T70)
PART23_IN_GAAA(T95) → PART23_IN_GAAA(T95)
PART23_IN_GAAA(0) → U3_GAAA(0, lessc13_out_ga(0))
PART23_IN_GAAA(s(x0)) → U3_GAAA(s(x0), U68_ga(x0, lessc13_in_ga(x0)))

The TRS R consists of the following rules:

lessc13_in_ga(0) → lessc13_out_ga(0)
lessc13_in_ga(s(T45)) → U68_ga(T45, lessc13_in_ga(T45))
U68_ga(T45, lessc13_out_ga(T45)) → lessc13_out_ga(s(T45))

The set Q consists of the following terms:

lessc13_in_ga(x0)
U68_ga(x0, x1)

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

(51) Instantiation (EQUIVALENT transformation)

By instantiating [LPAR04] the rule U3_GAAA(T70, lessc13_out_ga(T70)) → PART23_IN_GAAA(T70) we obtained the following new rules [LPAR04]:

U3_GAAA(0, lessc13_out_ga(0)) → PART23_IN_GAAA(0)
U3_GAAA(s(z0), lessc13_out_ga(s(z0))) → PART23_IN_GAAA(s(z0))

(52) Obligation:

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

PART23_IN_GAAA(T95) → PART23_IN_GAAA(T95)
PART23_IN_GAAA(0) → U3_GAAA(0, lessc13_out_ga(0))
PART23_IN_GAAA(s(x0)) → U3_GAAA(s(x0), U68_ga(x0, lessc13_in_ga(x0)))
U3_GAAA(0, lessc13_out_ga(0)) → PART23_IN_GAAA(0)
U3_GAAA(s(z0), lessc13_out_ga(s(z0))) → PART23_IN_GAAA(s(z0))

The TRS R consists of the following rules:

lessc13_in_ga(0) → lessc13_out_ga(0)
lessc13_in_ga(s(T45)) → U68_ga(T45, lessc13_in_ga(T45))
U68_ga(T45, lessc13_out_ga(T45)) → lessc13_out_ga(s(T45))

The set Q consists of the following terms:

lessc13_in_ga(x0)
U68_ga(x0, x1)

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

(53) NonTerminationProof (EQUIVALENT transformation)

We used the non-termination processor [FROCOS05] to show that the DP problem is infinite.
Found a loop by semiunifying a rule from P directly.

s = PART23_IN_GAAA(T95) evaluates to t =PART23_IN_GAAA(T95)

Thus s starts an infinite chain as s semiunifies with t with the following substitutions:
  • Semiunifier: [ ]
  • Matcher: [ ]




Rewriting sequence

The DP semiunifies directly so there is only one rewrite step from PART23_IN_GAAA(T95) to PART23_IN_GAAA(T95).



(54) NO

(55) Obligation:

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

LESS13_IN_AA(s(T45), s(T46)) → LESS13_IN_AA(T45, T46)

The TRS R consists of the following rules:

lessc13_in_aa(0, s(T38)) → lessc13_out_aa(0, s(T38))
lessc13_in_aa(s(T45), s(T46)) → U68_aa(T45, T46, lessc13_in_aa(T45, T46))
U68_aa(T45, T46, lessc13_out_aa(T45, T46)) → lessc13_out_aa(s(T45), s(T46))
lessc13_in_ga(0, s(T38)) → lessc13_out_ga(0, s(T38))
lessc13_in_ga(s(T45), s(T46)) → U68_ga(T45, T46, lessc13_in_ga(T45, T46))
U68_ga(T45, T46, lessc13_out_ga(T45, T46)) → lessc13_out_ga(s(T45), s(T46))
partc23_in_gaaa(T70, .(T73, T77), .(T73, X123), X124) → U69_gaaa(T70, T73, T77, X123, X124, lessc13_in_ga(T70, T73))
U69_gaaa(T70, T73, T77, X123, X124, lessc13_out_ga(T70, T73)) → U70_gaaa(T70, T73, T77, X123, X124, partc23_in_gaaa(T70, T77, X123, X124))
partc23_in_gaaa(T95, .(T96, T98), X174, .(T96, X175)) → U71_gaaa(T95, T96, T98, X174, X175, partc23_in_gaaa(T95, T98, X174, X175))
partc23_in_gaaa(T104, [], [], []) → partc23_out_gaaa(T104, [], [], [])
U71_gaaa(T95, T96, T98, X174, X175, partc23_out_gaaa(T95, T98, X174, X175)) → partc23_out_gaaa(T95, .(T96, T98), X174, .(T96, X175))
U70_gaaa(T70, T73, T77, X123, X124, partc23_out_gaaa(T70, T77, X123, X124)) → partc23_out_gaaa(T70, .(T73, T77), .(T73, X123), X124)
partc44_in_aaaa(T153, .(T149, T154), .(T149, X282), X283) → U72_aaaa(T153, T149, T154, X282, X283, lessc13_in_aa(T153, T149))
U72_aaaa(T153, T149, T154, X282, X283, lessc13_out_aa(T153, T149)) → U73_aaaa(T153, T149, T154, X282, X283, partc23_in_gaaa(T153, T154, X282, X283))
U73_aaaa(T153, T149, T154, X282, X283, partc23_out_gaaa(T153, T154, X282, X283)) → partc44_out_aaaa(T153, .(T149, T154), .(T149, X282), X283)
partc44_in_aaaa(T175, .(T173, T176), X333, .(T173, X334)) → U74_aaaa(T175, T173, T176, X333, X334, partc44_in_aaaa(T175, T176, X333, X334))
partc44_in_aaaa(T182, [], [], []) → partc44_out_aaaa(T182, [], [], [])
U74_aaaa(T175, T173, T176, X333, X334, partc44_out_aaaa(T175, T176, X333, X334)) → partc44_out_aaaa(T175, .(T173, T176), X333, .(T173, X334))
qsc60_in_aa([], []) → qsc60_out_aa([], [])
qsc60_in_aa(.(T192, T193), X370) → U79_aa(T192, T193, X370, qc43_in_aaaaaaa(T192, T193, X366, X367, X368, X369, X370))
qc43_in_aaaaaaa(T199, T123, T127, T184, T198, T197, X234) → U75_aaaaaaa(T199, T123, T127, T184, T198, T197, X234, partc44_in_aaaa(T199, T123, T127, T184))
U75_aaaaaaa(T199, T123, T127, T184, T198, T197, X234, partc44_out_aaaa(T199, T123, T127, T184)) → U76_aaaaaaa(T199, T123, T127, T184, T198, T197, X234, qsc60_in_aa(T127, T198))
U76_aaaaaaa(T199, T123, T127, T184, T198, T197, X234, qsc60_out_aa(T127, T198)) → U77_aaaaaaa(T199, T123, T127, T184, T198, T197, X234, qsc60_in_aa(T184, T197))
U77_aaaaaaa(T199, T123, T127, T184, T198, T197, X234, qsc60_out_aa(T184, T197)) → U78_aaaaaaa(T199, T123, T127, T184, T198, T197, X234, appc71_in_aaaa(T198, T199, T197, X234))
appc71_in_aaaa([], T212, T213, .(T212, T213)) → appc71_out_aaaa([], T212, T213, .(T212, T213))
appc71_in_aaaa(.(T222, T226), T227, T228, .(T222, X403)) → U80_aaaa(T222, T226, T227, T228, X403, appc71_in_aaaa(T226, T227, T228, X403))
U80_aaaa(T222, T226, T227, T228, X403, appc71_out_aaaa(T226, T227, T228, X403)) → appc71_out_aaaa(.(T222, T226), T227, T228, .(T222, X403))
U78_aaaaaaa(T199, T123, T127, T184, T198, T197, X234, appc71_out_aaaa(T198, T199, T197, X234)) → qc43_out_aaaaaaa(T199, T123, T127, T184, T198, T197, X234)
U79_aa(T192, T193, X370, qc43_out_aaaaaaa(T192, T193, X366, X367, X368, X369, X370)) → qsc60_out_aa(.(T192, T193), X370)
qsc39_in_aaa(T122, T123, X234) → U81_aaa(T122, T123, X234, qc43_in_aaaaaaa(T122, T123, X230, X231, X232, X233, X234))
U81_aaa(T122, T123, X234, qc43_out_aaaaaaa(T122, T123, X230, X231, X232, X233, X234)) → qsc39_out_aaa(T122, T123, X234)
qsc100_in_a([]) → qsc100_out_a([])

The argument filtering Pi contains the following mapping:
[]  =  []
lessc13_in_aa(x1, x2)  =  lessc13_in_aa
lessc13_out_aa(x1, x2)  =  lessc13_out_aa(x1)
U68_aa(x1, x2, x3)  =  U68_aa(x3)
s(x1)  =  s(x1)
lessc13_in_ga(x1, x2)  =  lessc13_in_ga(x1)
0  =  0
lessc13_out_ga(x1, x2)  =  lessc13_out_ga(x1)
U68_ga(x1, x2, x3)  =  U68_ga(x1, x3)
partc23_in_gaaa(x1, x2, x3, x4)  =  partc23_in_gaaa(x1)
U69_gaaa(x1, x2, x3, x4, x5, x6)  =  U69_gaaa(x1, x6)
U70_gaaa(x1, x2, x3, x4, x5, x6)  =  U70_gaaa(x1, x6)
U71_gaaa(x1, x2, x3, x4, x5, x6)  =  U71_gaaa(x1, x6)
partc23_out_gaaa(x1, x2, x3, x4)  =  partc23_out_gaaa(x1)
partc44_in_aaaa(x1, x2, x3, x4)  =  partc44_in_aaaa
U72_aaaa(x1, x2, x3, x4, x5, x6)  =  U72_aaaa(x6)
U73_aaaa(x1, x2, x3, x4, x5, x6)  =  U73_aaaa(x6)
partc44_out_aaaa(x1, x2, x3, x4)  =  partc44_out_aaaa
U74_aaaa(x1, x2, x3, x4, x5, x6)  =  U74_aaaa(x6)
qsc60_in_aa(x1, x2)  =  qsc60_in_aa
qsc60_out_aa(x1, x2)  =  qsc60_out_aa
U79_aa(x1, x2, x3, x4)  =  U79_aa(x4)
qc43_in_aaaaaaa(x1, x2, x3, x4, x5, x6, x7)  =  qc43_in_aaaaaaa
U75_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  U75_aaaaaaa(x8)
U76_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  U76_aaaaaaa(x8)
U77_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  U77_aaaaaaa(x8)
U78_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  U78_aaaaaaa(x8)
.(x1, x2)  =  .(x1, x2)
qc43_out_aaaaaaa(x1, x2, x3, x4, x5, x6, x7)  =  qc43_out_aaaaaaa
appc71_in_aaaa(x1, x2, x3, x4)  =  appc71_in_aaaa
appc71_out_aaaa(x1, x2, x3, x4)  =  appc71_out_aaaa
U80_aaaa(x1, x2, x3, x4, x5, x6)  =  U80_aaaa(x6)
qsc39_in_aaa(x1, x2, x3)  =  qsc39_in_aaa
U81_aaa(x1, x2, x3, x4)  =  U81_aaa(x4)
qsc39_out_aaa(x1, x2, x3)  =  qsc39_out_aaa
qsc100_in_a(x1)  =  qsc100_in_a
qsc100_out_a(x1)  =  qsc100_out_a(x1)
LESS13_IN_AA(x1, x2)  =  LESS13_IN_AA

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

(56) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(57) Obligation:

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

LESS13_IN_AA(s(T45), s(T46)) → LESS13_IN_AA(T45, T46)

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

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

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

LESS13_IN_AALESS13_IN_AA

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

(60) NonTerminationProof (EQUIVALENT transformation)

We used the non-termination processor [FROCOS05] to show that the DP problem is infinite.
Found a loop by semiunifying a rule from P directly.

s = LESS13_IN_AA evaluates to t =LESS13_IN_AA

Thus s starts an infinite chain as s semiunifies with t with the following substitutions:
  • Matcher: [ ]
  • Semiunifier: [ ]




Rewriting sequence

The DP semiunifies directly so there is only one rewrite step from LESS13_IN_AA to LESS13_IN_AA.



(61) NO

(62) Obligation:

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

PART44_IN_AAAA(T175, .(T173, T176), X333, .(T173, X334)) → PART44_IN_AAAA(T175, T176, X333, X334)

The TRS R consists of the following rules:

lessc13_in_aa(0, s(T38)) → lessc13_out_aa(0, s(T38))
lessc13_in_aa(s(T45), s(T46)) → U68_aa(T45, T46, lessc13_in_aa(T45, T46))
U68_aa(T45, T46, lessc13_out_aa(T45, T46)) → lessc13_out_aa(s(T45), s(T46))
lessc13_in_ga(0, s(T38)) → lessc13_out_ga(0, s(T38))
lessc13_in_ga(s(T45), s(T46)) → U68_ga(T45, T46, lessc13_in_ga(T45, T46))
U68_ga(T45, T46, lessc13_out_ga(T45, T46)) → lessc13_out_ga(s(T45), s(T46))
partc23_in_gaaa(T70, .(T73, T77), .(T73, X123), X124) → U69_gaaa(T70, T73, T77, X123, X124, lessc13_in_ga(T70, T73))
U69_gaaa(T70, T73, T77, X123, X124, lessc13_out_ga(T70, T73)) → U70_gaaa(T70, T73, T77, X123, X124, partc23_in_gaaa(T70, T77, X123, X124))
partc23_in_gaaa(T95, .(T96, T98), X174, .(T96, X175)) → U71_gaaa(T95, T96, T98, X174, X175, partc23_in_gaaa(T95, T98, X174, X175))
partc23_in_gaaa(T104, [], [], []) → partc23_out_gaaa(T104, [], [], [])
U71_gaaa(T95, T96, T98, X174, X175, partc23_out_gaaa(T95, T98, X174, X175)) → partc23_out_gaaa(T95, .(T96, T98), X174, .(T96, X175))
U70_gaaa(T70, T73, T77, X123, X124, partc23_out_gaaa(T70, T77, X123, X124)) → partc23_out_gaaa(T70, .(T73, T77), .(T73, X123), X124)
partc44_in_aaaa(T153, .(T149, T154), .(T149, X282), X283) → U72_aaaa(T153, T149, T154, X282, X283, lessc13_in_aa(T153, T149))
U72_aaaa(T153, T149, T154, X282, X283, lessc13_out_aa(T153, T149)) → U73_aaaa(T153, T149, T154, X282, X283, partc23_in_gaaa(T153, T154, X282, X283))
U73_aaaa(T153, T149, T154, X282, X283, partc23_out_gaaa(T153, T154, X282, X283)) → partc44_out_aaaa(T153, .(T149, T154), .(T149, X282), X283)
partc44_in_aaaa(T175, .(T173, T176), X333, .(T173, X334)) → U74_aaaa(T175, T173, T176, X333, X334, partc44_in_aaaa(T175, T176, X333, X334))
partc44_in_aaaa(T182, [], [], []) → partc44_out_aaaa(T182, [], [], [])
U74_aaaa(T175, T173, T176, X333, X334, partc44_out_aaaa(T175, T176, X333, X334)) → partc44_out_aaaa(T175, .(T173, T176), X333, .(T173, X334))
qsc60_in_aa([], []) → qsc60_out_aa([], [])
qsc60_in_aa(.(T192, T193), X370) → U79_aa(T192, T193, X370, qc43_in_aaaaaaa(T192, T193, X366, X367, X368, X369, X370))
qc43_in_aaaaaaa(T199, T123, T127, T184, T198, T197, X234) → U75_aaaaaaa(T199, T123, T127, T184, T198, T197, X234, partc44_in_aaaa(T199, T123, T127, T184))
U75_aaaaaaa(T199, T123, T127, T184, T198, T197, X234, partc44_out_aaaa(T199, T123, T127, T184)) → U76_aaaaaaa(T199, T123, T127, T184, T198, T197, X234, qsc60_in_aa(T127, T198))
U76_aaaaaaa(T199, T123, T127, T184, T198, T197, X234, qsc60_out_aa(T127, T198)) → U77_aaaaaaa(T199, T123, T127, T184, T198, T197, X234, qsc60_in_aa(T184, T197))
U77_aaaaaaa(T199, T123, T127, T184, T198, T197, X234, qsc60_out_aa(T184, T197)) → U78_aaaaaaa(T199, T123, T127, T184, T198, T197, X234, appc71_in_aaaa(T198, T199, T197, X234))
appc71_in_aaaa([], T212, T213, .(T212, T213)) → appc71_out_aaaa([], T212, T213, .(T212, T213))
appc71_in_aaaa(.(T222, T226), T227, T228, .(T222, X403)) → U80_aaaa(T222, T226, T227, T228, X403, appc71_in_aaaa(T226, T227, T228, X403))
U80_aaaa(T222, T226, T227, T228, X403, appc71_out_aaaa(T226, T227, T228, X403)) → appc71_out_aaaa(.(T222, T226), T227, T228, .(T222, X403))
U78_aaaaaaa(T199, T123, T127, T184, T198, T197, X234, appc71_out_aaaa(T198, T199, T197, X234)) → qc43_out_aaaaaaa(T199, T123, T127, T184, T198, T197, X234)
U79_aa(T192, T193, X370, qc43_out_aaaaaaa(T192, T193, X366, X367, X368, X369, X370)) → qsc60_out_aa(.(T192, T193), X370)
qsc39_in_aaa(T122, T123, X234) → U81_aaa(T122, T123, X234, qc43_in_aaaaaaa(T122, T123, X230, X231, X232, X233, X234))
U81_aaa(T122, T123, X234, qc43_out_aaaaaaa(T122, T123, X230, X231, X232, X233, X234)) → qsc39_out_aaa(T122, T123, X234)
qsc100_in_a([]) → qsc100_out_a([])

The argument filtering Pi contains the following mapping:
[]  =  []
lessc13_in_aa(x1, x2)  =  lessc13_in_aa
lessc13_out_aa(x1, x2)  =  lessc13_out_aa(x1)
U68_aa(x1, x2, x3)  =  U68_aa(x3)
s(x1)  =  s(x1)
lessc13_in_ga(x1, x2)  =  lessc13_in_ga(x1)
0  =  0
lessc13_out_ga(x1, x2)  =  lessc13_out_ga(x1)
U68_ga(x1, x2, x3)  =  U68_ga(x1, x3)
partc23_in_gaaa(x1, x2, x3, x4)  =  partc23_in_gaaa(x1)
U69_gaaa(x1, x2, x3, x4, x5, x6)  =  U69_gaaa(x1, x6)
U70_gaaa(x1, x2, x3, x4, x5, x6)  =  U70_gaaa(x1, x6)
U71_gaaa(x1, x2, x3, x4, x5, x6)  =  U71_gaaa(x1, x6)
partc23_out_gaaa(x1, x2, x3, x4)  =  partc23_out_gaaa(x1)
partc44_in_aaaa(x1, x2, x3, x4)  =  partc44_in_aaaa
U72_aaaa(x1, x2, x3, x4, x5, x6)  =  U72_aaaa(x6)
U73_aaaa(x1, x2, x3, x4, x5, x6)  =  U73_aaaa(x6)
partc44_out_aaaa(x1, x2, x3, x4)  =  partc44_out_aaaa
U74_aaaa(x1, x2, x3, x4, x5, x6)  =  U74_aaaa(x6)
qsc60_in_aa(x1, x2)  =  qsc60_in_aa
qsc60_out_aa(x1, x2)  =  qsc60_out_aa
U79_aa(x1, x2, x3, x4)  =  U79_aa(x4)
qc43_in_aaaaaaa(x1, x2, x3, x4, x5, x6, x7)  =  qc43_in_aaaaaaa
U75_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  U75_aaaaaaa(x8)
U76_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  U76_aaaaaaa(x8)
U77_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  U77_aaaaaaa(x8)
U78_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  U78_aaaaaaa(x8)
.(x1, x2)  =  .(x1, x2)
qc43_out_aaaaaaa(x1, x2, x3, x4, x5, x6, x7)  =  qc43_out_aaaaaaa
appc71_in_aaaa(x1, x2, x3, x4)  =  appc71_in_aaaa
appc71_out_aaaa(x1, x2, x3, x4)  =  appc71_out_aaaa
U80_aaaa(x1, x2, x3, x4, x5, x6)  =  U80_aaaa(x6)
qsc39_in_aaa(x1, x2, x3)  =  qsc39_in_aaa
U81_aaa(x1, x2, x3, x4)  =  U81_aaa(x4)
qsc39_out_aaa(x1, x2, x3)  =  qsc39_out_aaa
qsc100_in_a(x1)  =  qsc100_in_a
qsc100_out_a(x1)  =  qsc100_out_a(x1)
PART44_IN_AAAA(x1, x2, x3, x4)  =  PART44_IN_AAAA

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

(63) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(64) Obligation:

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

PART44_IN_AAAA(T175, .(T173, T176), X333, .(T173, X334)) → PART44_IN_AAAA(T175, T176, X333, X334)

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

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

(65) PiDPToQDPProof (SOUND transformation)

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

(66) Obligation:

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

PART44_IN_AAAAPART44_IN_AAAA

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

(67) NonTerminationProof (EQUIVALENT transformation)

We used the non-termination processor [FROCOS05] to show that the DP problem is infinite.
Found a loop by semiunifying a rule from P directly.

s = PART44_IN_AAAA evaluates to t =PART44_IN_AAAA

Thus s starts an infinite chain as s semiunifies with t with the following substitutions:
  • Semiunifier: [ ]
  • Matcher: [ ]




Rewriting sequence

The DP semiunifies directly so there is only one rewrite step from PART44_IN_AAAA to PART44_IN_AAAA.



(68) NO

(69) Obligation:

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

P43_IN_AAAAAAA(T129, T123, T127, T128, X232, X233, X234) → U11_AAAAAAA(T129, T123, T127, T128, X232, X233, X234, partc44_in_aaaa(T129, T123, T127, T128))
U11_AAAAAAA(T129, T123, T127, T128, X232, X233, X234, partc44_out_aaaa(T129, T123, T127, T128)) → QS60_IN_AA(T127, X232)
QS60_IN_AA(.(T192, T193), X370) → P43_IN_AAAAAAA(T192, T193, X366, X367, X368, X369, X370)
P43_IN_AAAAAAA(T185, T123, T127, T184, T183, X233, X234) → U13_AAAAAAA(T185, T123, T127, T184, T183, X233, X234, partc44_in_aaaa(T185, T123, T127, T184))
U13_AAAAAAA(T185, T123, T127, T184, T183, X233, X234, partc44_out_aaaa(T185, T123, T127, T184)) → U14_AAAAAAA(T185, T123, T127, T184, T183, X233, X234, qsc60_in_aa(T127, T183))
U14_AAAAAAA(T185, T123, T127, T184, T183, X233, X234, qsc60_out_aa(T127, T183)) → QS60_IN_AA(T184, X233)

The TRS R consists of the following rules:

lessc13_in_aa(0, s(T38)) → lessc13_out_aa(0, s(T38))
lessc13_in_aa(s(T45), s(T46)) → U68_aa(T45, T46, lessc13_in_aa(T45, T46))
U68_aa(T45, T46, lessc13_out_aa(T45, T46)) → lessc13_out_aa(s(T45), s(T46))
lessc13_in_ga(0, s(T38)) → lessc13_out_ga(0, s(T38))
lessc13_in_ga(s(T45), s(T46)) → U68_ga(T45, T46, lessc13_in_ga(T45, T46))
U68_ga(T45, T46, lessc13_out_ga(T45, T46)) → lessc13_out_ga(s(T45), s(T46))
partc23_in_gaaa(T70, .(T73, T77), .(T73, X123), X124) → U69_gaaa(T70, T73, T77, X123, X124, lessc13_in_ga(T70, T73))
U69_gaaa(T70, T73, T77, X123, X124, lessc13_out_ga(T70, T73)) → U70_gaaa(T70, T73, T77, X123, X124, partc23_in_gaaa(T70, T77, X123, X124))
partc23_in_gaaa(T95, .(T96, T98), X174, .(T96, X175)) → U71_gaaa(T95, T96, T98, X174, X175, partc23_in_gaaa(T95, T98, X174, X175))
partc23_in_gaaa(T104, [], [], []) → partc23_out_gaaa(T104, [], [], [])
U71_gaaa(T95, T96, T98, X174, X175, partc23_out_gaaa(T95, T98, X174, X175)) → partc23_out_gaaa(T95, .(T96, T98), X174, .(T96, X175))
U70_gaaa(T70, T73, T77, X123, X124, partc23_out_gaaa(T70, T77, X123, X124)) → partc23_out_gaaa(T70, .(T73, T77), .(T73, X123), X124)
partc44_in_aaaa(T153, .(T149, T154), .(T149, X282), X283) → U72_aaaa(T153, T149, T154, X282, X283, lessc13_in_aa(T153, T149))
U72_aaaa(T153, T149, T154, X282, X283, lessc13_out_aa(T153, T149)) → U73_aaaa(T153, T149, T154, X282, X283, partc23_in_gaaa(T153, T154, X282, X283))
U73_aaaa(T153, T149, T154, X282, X283, partc23_out_gaaa(T153, T154, X282, X283)) → partc44_out_aaaa(T153, .(T149, T154), .(T149, X282), X283)
partc44_in_aaaa(T175, .(T173, T176), X333, .(T173, X334)) → U74_aaaa(T175, T173, T176, X333, X334, partc44_in_aaaa(T175, T176, X333, X334))
partc44_in_aaaa(T182, [], [], []) → partc44_out_aaaa(T182, [], [], [])
U74_aaaa(T175, T173, T176, X333, X334, partc44_out_aaaa(T175, T176, X333, X334)) → partc44_out_aaaa(T175, .(T173, T176), X333, .(T173, X334))
qsc60_in_aa([], []) → qsc60_out_aa([], [])
qsc60_in_aa(.(T192, T193), X370) → U79_aa(T192, T193, X370, qc43_in_aaaaaaa(T192, T193, X366, X367, X368, X369, X370))
qc43_in_aaaaaaa(T199, T123, T127, T184, T198, T197, X234) → U75_aaaaaaa(T199, T123, T127, T184, T198, T197, X234, partc44_in_aaaa(T199, T123, T127, T184))
U75_aaaaaaa(T199, T123, T127, T184, T198, T197, X234, partc44_out_aaaa(T199, T123, T127, T184)) → U76_aaaaaaa(T199, T123, T127, T184, T198, T197, X234, qsc60_in_aa(T127, T198))
U76_aaaaaaa(T199, T123, T127, T184, T198, T197, X234, qsc60_out_aa(T127, T198)) → U77_aaaaaaa(T199, T123, T127, T184, T198, T197, X234, qsc60_in_aa(T184, T197))
U77_aaaaaaa(T199, T123, T127, T184, T198, T197, X234, qsc60_out_aa(T184, T197)) → U78_aaaaaaa(T199, T123, T127, T184, T198, T197, X234, appc71_in_aaaa(T198, T199, T197, X234))
appc71_in_aaaa([], T212, T213, .(T212, T213)) → appc71_out_aaaa([], T212, T213, .(T212, T213))
appc71_in_aaaa(.(T222, T226), T227, T228, .(T222, X403)) → U80_aaaa(T222, T226, T227, T228, X403, appc71_in_aaaa(T226, T227, T228, X403))
U80_aaaa(T222, T226, T227, T228, X403, appc71_out_aaaa(T226, T227, T228, X403)) → appc71_out_aaaa(.(T222, T226), T227, T228, .(T222, X403))
U78_aaaaaaa(T199, T123, T127, T184, T198, T197, X234, appc71_out_aaaa(T198, T199, T197, X234)) → qc43_out_aaaaaaa(T199, T123, T127, T184, T198, T197, X234)
U79_aa(T192, T193, X370, qc43_out_aaaaaaa(T192, T193, X366, X367, X368, X369, X370)) → qsc60_out_aa(.(T192, T193), X370)
qsc39_in_aaa(T122, T123, X234) → U81_aaa(T122, T123, X234, qc43_in_aaaaaaa(T122, T123, X230, X231, X232, X233, X234))
U81_aaa(T122, T123, X234, qc43_out_aaaaaaa(T122, T123, X230, X231, X232, X233, X234)) → qsc39_out_aaa(T122, T123, X234)
qsc100_in_a([]) → qsc100_out_a([])

The argument filtering Pi contains the following mapping:
[]  =  []
lessc13_in_aa(x1, x2)  =  lessc13_in_aa
lessc13_out_aa(x1, x2)  =  lessc13_out_aa(x1)
U68_aa(x1, x2, x3)  =  U68_aa(x3)
s(x1)  =  s(x1)
lessc13_in_ga(x1, x2)  =  lessc13_in_ga(x1)
0  =  0
lessc13_out_ga(x1, x2)  =  lessc13_out_ga(x1)
U68_ga(x1, x2, x3)  =  U68_ga(x1, x3)
partc23_in_gaaa(x1, x2, x3, x4)  =  partc23_in_gaaa(x1)
U69_gaaa(x1, x2, x3, x4, x5, x6)  =  U69_gaaa(x1, x6)
U70_gaaa(x1, x2, x3, x4, x5, x6)  =  U70_gaaa(x1, x6)
U71_gaaa(x1, x2, x3, x4, x5, x6)  =  U71_gaaa(x1, x6)
partc23_out_gaaa(x1, x2, x3, x4)  =  partc23_out_gaaa(x1)
partc44_in_aaaa(x1, x2, x3, x4)  =  partc44_in_aaaa
U72_aaaa(x1, x2, x3, x4, x5, x6)  =  U72_aaaa(x6)
U73_aaaa(x1, x2, x3, x4, x5, x6)  =  U73_aaaa(x6)
partc44_out_aaaa(x1, x2, x3, x4)  =  partc44_out_aaaa
U74_aaaa(x1, x2, x3, x4, x5, x6)  =  U74_aaaa(x6)
qsc60_in_aa(x1, x2)  =  qsc60_in_aa
qsc60_out_aa(x1, x2)  =  qsc60_out_aa
U79_aa(x1, x2, x3, x4)  =  U79_aa(x4)
qc43_in_aaaaaaa(x1, x2, x3, x4, x5, x6, x7)  =  qc43_in_aaaaaaa
U75_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  U75_aaaaaaa(x8)
U76_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  U76_aaaaaaa(x8)
U77_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  U77_aaaaaaa(x8)
U78_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  U78_aaaaaaa(x8)
.(x1, x2)  =  .(x1, x2)
qc43_out_aaaaaaa(x1, x2, x3, x4, x5, x6, x7)  =  qc43_out_aaaaaaa
appc71_in_aaaa(x1, x2, x3, x4)  =  appc71_in_aaaa
appc71_out_aaaa(x1, x2, x3, x4)  =  appc71_out_aaaa
U80_aaaa(x1, x2, x3, x4, x5, x6)  =  U80_aaaa(x6)
qsc39_in_aaa(x1, x2, x3)  =  qsc39_in_aaa
U81_aaa(x1, x2, x3, x4)  =  U81_aaa(x4)
qsc39_out_aaa(x1, x2, x3)  =  qsc39_out_aaa
qsc100_in_a(x1)  =  qsc100_in_a
qsc100_out_a(x1)  =  qsc100_out_a(x1)
P43_IN_AAAAAAA(x1, x2, x3, x4, x5, x6, x7)  =  P43_IN_AAAAAAA
U11_AAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8)  =  U11_AAAAAAA(x8)
QS60_IN_AA(x1, x2)  =  QS60_IN_AA
U13_AAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8)  =  U13_AAAAAAA(x8)
U14_AAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8)  =  U14_AAAAAAA(x8)

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

(70) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(71) Obligation:

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

P43_IN_AAAAAAA(T129, T123, T127, T128, X232, X233, X234) → U11_AAAAAAA(T129, T123, T127, T128, X232, X233, X234, partc44_in_aaaa(T129, T123, T127, T128))
U11_AAAAAAA(T129, T123, T127, T128, X232, X233, X234, partc44_out_aaaa(T129, T123, T127, T128)) → QS60_IN_AA(T127, X232)
QS60_IN_AA(.(T192, T193), X370) → P43_IN_AAAAAAA(T192, T193, X366, X367, X368, X369, X370)
P43_IN_AAAAAAA(T185, T123, T127, T184, T183, X233, X234) → U13_AAAAAAA(T185, T123, T127, T184, T183, X233, X234, partc44_in_aaaa(T185, T123, T127, T184))
U13_AAAAAAA(T185, T123, T127, T184, T183, X233, X234, partc44_out_aaaa(T185, T123, T127, T184)) → U14_AAAAAAA(T185, T123, T127, T184, T183, X233, X234, qsc60_in_aa(T127, T183))
U14_AAAAAAA(T185, T123, T127, T184, T183, X233, X234, qsc60_out_aa(T127, T183)) → QS60_IN_AA(T184, X233)

The TRS R consists of the following rules:

partc44_in_aaaa(T153, .(T149, T154), .(T149, X282), X283) → U72_aaaa(T153, T149, T154, X282, X283, lessc13_in_aa(T153, T149))
partc44_in_aaaa(T175, .(T173, T176), X333, .(T173, X334)) → U74_aaaa(T175, T173, T176, X333, X334, partc44_in_aaaa(T175, T176, X333, X334))
partc44_in_aaaa(T182, [], [], []) → partc44_out_aaaa(T182, [], [], [])
qsc60_in_aa([], []) → qsc60_out_aa([], [])
qsc60_in_aa(.(T192, T193), X370) → U79_aa(T192, T193, X370, qc43_in_aaaaaaa(T192, T193, X366, X367, X368, X369, X370))
U72_aaaa(T153, T149, T154, X282, X283, lessc13_out_aa(T153, T149)) → U73_aaaa(T153, T149, T154, X282, X283, partc23_in_gaaa(T153, T154, X282, X283))
U74_aaaa(T175, T173, T176, X333, X334, partc44_out_aaaa(T175, T176, X333, X334)) → partc44_out_aaaa(T175, .(T173, T176), X333, .(T173, X334))
U79_aa(T192, T193, X370, qc43_out_aaaaaaa(T192, T193, X366, X367, X368, X369, X370)) → qsc60_out_aa(.(T192, T193), X370)
lessc13_in_aa(0, s(T38)) → lessc13_out_aa(0, s(T38))
lessc13_in_aa(s(T45), s(T46)) → U68_aa(T45, T46, lessc13_in_aa(T45, T46))
U73_aaaa(T153, T149, T154, X282, X283, partc23_out_gaaa(T153, T154, X282, X283)) → partc44_out_aaaa(T153, .(T149, T154), .(T149, X282), X283)
qc43_in_aaaaaaa(T199, T123, T127, T184, T198, T197, X234) → U75_aaaaaaa(T199, T123, T127, T184, T198, T197, X234, partc44_in_aaaa(T199, T123, T127, T184))
U68_aa(T45, T46, lessc13_out_aa(T45, T46)) → lessc13_out_aa(s(T45), s(T46))
partc23_in_gaaa(T70, .(T73, T77), .(T73, X123), X124) → U69_gaaa(T70, T73, T77, X123, X124, lessc13_in_ga(T70, T73))
partc23_in_gaaa(T95, .(T96, T98), X174, .(T96, X175)) → U71_gaaa(T95, T96, T98, X174, X175, partc23_in_gaaa(T95, T98, X174, X175))
partc23_in_gaaa(T104, [], [], []) → partc23_out_gaaa(T104, [], [], [])
U75_aaaaaaa(T199, T123, T127, T184, T198, T197, X234, partc44_out_aaaa(T199, T123, T127, T184)) → U76_aaaaaaa(T199, T123, T127, T184, T198, T197, X234, qsc60_in_aa(T127, T198))
U69_gaaa(T70, T73, T77, X123, X124, lessc13_out_ga(T70, T73)) → U70_gaaa(T70, T73, T77, X123, X124, partc23_in_gaaa(T70, T77, X123, X124))
U71_gaaa(T95, T96, T98, X174, X175, partc23_out_gaaa(T95, T98, X174, X175)) → partc23_out_gaaa(T95, .(T96, T98), X174, .(T96, X175))
U76_aaaaaaa(T199, T123, T127, T184, T198, T197, X234, qsc60_out_aa(T127, T198)) → U77_aaaaaaa(T199, T123, T127, T184, T198, T197, X234, qsc60_in_aa(T184, T197))
lessc13_in_ga(0, s(T38)) → lessc13_out_ga(0, s(T38))
lessc13_in_ga(s(T45), s(T46)) → U68_ga(T45, T46, lessc13_in_ga(T45, T46))
U70_gaaa(T70, T73, T77, X123, X124, partc23_out_gaaa(T70, T77, X123, X124)) → partc23_out_gaaa(T70, .(T73, T77), .(T73, X123), X124)
U77_aaaaaaa(T199, T123, T127, T184, T198, T197, X234, qsc60_out_aa(T184, T197)) → U78_aaaaaaa(T199, T123, T127, T184, T198, T197, X234, appc71_in_aaaa(T198, T199, T197, X234))
U68_ga(T45, T46, lessc13_out_ga(T45, T46)) → lessc13_out_ga(s(T45), s(T46))
U78_aaaaaaa(T199, T123, T127, T184, T198, T197, X234, appc71_out_aaaa(T198, T199, T197, X234)) → qc43_out_aaaaaaa(T199, T123, T127, T184, T198, T197, X234)
appc71_in_aaaa([], T212, T213, .(T212, T213)) → appc71_out_aaaa([], T212, T213, .(T212, T213))
appc71_in_aaaa(.(T222, T226), T227, T228, .(T222, X403)) → U80_aaaa(T222, T226, T227, T228, X403, appc71_in_aaaa(T226, T227, T228, X403))
U80_aaaa(T222, T226, T227, T228, X403, appc71_out_aaaa(T226, T227, T228, X403)) → appc71_out_aaaa(.(T222, T226), T227, T228, .(T222, X403))

The argument filtering Pi contains the following mapping:
[]  =  []
lessc13_in_aa(x1, x2)  =  lessc13_in_aa
lessc13_out_aa(x1, x2)  =  lessc13_out_aa(x1)
U68_aa(x1, x2, x3)  =  U68_aa(x3)
s(x1)  =  s(x1)
lessc13_in_ga(x1, x2)  =  lessc13_in_ga(x1)
0  =  0
lessc13_out_ga(x1, x2)  =  lessc13_out_ga(x1)
U68_ga(x1, x2, x3)  =  U68_ga(x1, x3)
partc23_in_gaaa(x1, x2, x3, x4)  =  partc23_in_gaaa(x1)
U69_gaaa(x1, x2, x3, x4, x5, x6)  =  U69_gaaa(x1, x6)
U70_gaaa(x1, x2, x3, x4, x5, x6)  =  U70_gaaa(x1, x6)
U71_gaaa(x1, x2, x3, x4, x5, x6)  =  U71_gaaa(x1, x6)
partc23_out_gaaa(x1, x2, x3, x4)  =  partc23_out_gaaa(x1)
partc44_in_aaaa(x1, x2, x3, x4)  =  partc44_in_aaaa
U72_aaaa(x1, x2, x3, x4, x5, x6)  =  U72_aaaa(x6)
U73_aaaa(x1, x2, x3, x4, x5, x6)  =  U73_aaaa(x6)
partc44_out_aaaa(x1, x2, x3, x4)  =  partc44_out_aaaa
U74_aaaa(x1, x2, x3, x4, x5, x6)  =  U74_aaaa(x6)
qsc60_in_aa(x1, x2)  =  qsc60_in_aa
qsc60_out_aa(x1, x2)  =  qsc60_out_aa
U79_aa(x1, x2, x3, x4)  =  U79_aa(x4)
qc43_in_aaaaaaa(x1, x2, x3, x4, x5, x6, x7)  =  qc43_in_aaaaaaa
U75_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  U75_aaaaaaa(x8)
U76_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  U76_aaaaaaa(x8)
U77_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  U77_aaaaaaa(x8)
U78_aaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  U78_aaaaaaa(x8)
.(x1, x2)  =  .(x1, x2)
qc43_out_aaaaaaa(x1, x2, x3, x4, x5, x6, x7)  =  qc43_out_aaaaaaa
appc71_in_aaaa(x1, x2, x3, x4)  =  appc71_in_aaaa
appc71_out_aaaa(x1, x2, x3, x4)  =  appc71_out_aaaa
U80_aaaa(x1, x2, x3, x4, x5, x6)  =  U80_aaaa(x6)
P43_IN_AAAAAAA(x1, x2, x3, x4, x5, x6, x7)  =  P43_IN_AAAAAAA
U11_AAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8)  =  U11_AAAAAAA(x8)
QS60_IN_AA(x1, x2)  =  QS60_IN_AA
U13_AAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8)  =  U13_AAAAAAA(x8)
U14_AAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8)  =  U14_AAAAAAA(x8)

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

(72) PiDPToQDPProof (SOUND transformation)

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

(73) Obligation:

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

P43_IN_AAAAAAAU11_AAAAAAA(partc44_in_aaaa)
U11_AAAAAAA(partc44_out_aaaa) → QS60_IN_AA
QS60_IN_AAP43_IN_AAAAAAA
P43_IN_AAAAAAAU13_AAAAAAA(partc44_in_aaaa)
U13_AAAAAAA(partc44_out_aaaa) → U14_AAAAAAA(qsc60_in_aa)
U14_AAAAAAA(qsc60_out_aa) → QS60_IN_AA

The TRS R consists of the following rules:

partc44_in_aaaaU72_aaaa(lessc13_in_aa)
partc44_in_aaaaU74_aaaa(partc44_in_aaaa)
partc44_in_aaaapartc44_out_aaaa
qsc60_in_aaqsc60_out_aa
qsc60_in_aaU79_aa(qc43_in_aaaaaaa)
U72_aaaa(lessc13_out_aa(T153)) → U73_aaaa(partc23_in_gaaa(T153))
U74_aaaa(partc44_out_aaaa) → partc44_out_aaaa
U79_aa(qc43_out_aaaaaaa) → qsc60_out_aa
lessc13_in_aalessc13_out_aa(0)
lessc13_in_aaU68_aa(lessc13_in_aa)
U73_aaaa(partc23_out_gaaa(T153)) → partc44_out_aaaa
qc43_in_aaaaaaaU75_aaaaaaa(partc44_in_aaaa)
U68_aa(lessc13_out_aa(T45)) → lessc13_out_aa(s(T45))
partc23_in_gaaa(T70) → U69_gaaa(T70, lessc13_in_ga(T70))
partc23_in_gaaa(T95) → U71_gaaa(T95, partc23_in_gaaa(T95))
partc23_in_gaaa(T104) → partc23_out_gaaa(T104)
U75_aaaaaaa(partc44_out_aaaa) → U76_aaaaaaa(qsc60_in_aa)
U69_gaaa(T70, lessc13_out_ga(T70)) → U70_gaaa(T70, partc23_in_gaaa(T70))
U71_gaaa(T95, partc23_out_gaaa(T95)) → partc23_out_gaaa(T95)
U76_aaaaaaa(qsc60_out_aa) → U77_aaaaaaa(qsc60_in_aa)
lessc13_in_ga(0) → lessc13_out_ga(0)
lessc13_in_ga(s(T45)) → U68_ga(T45, lessc13_in_ga(T45))
U70_gaaa(T70, partc23_out_gaaa(T70)) → partc23_out_gaaa(T70)
U77_aaaaaaa(qsc60_out_aa) → U78_aaaaaaa(appc71_in_aaaa)
U68_ga(T45, lessc13_out_ga(T45)) → lessc13_out_ga(s(T45))
U78_aaaaaaa(appc71_out_aaaa) → qc43_out_aaaaaaa
appc71_in_aaaaappc71_out_aaaa
appc71_in_aaaaU80_aaaa(appc71_in_aaaa)
U80_aaaa(appc71_out_aaaa) → appc71_out_aaaa

The set Q consists of the following terms:

partc44_in_aaaa
qsc60_in_aa
U72_aaaa(x0)
U74_aaaa(x0)
U79_aa(x0)
lessc13_in_aa
U73_aaaa(x0)
qc43_in_aaaaaaa
U68_aa(x0)
partc23_in_gaaa(x0)
U75_aaaaaaa(x0)
U69_gaaa(x0, x1)
U71_gaaa(x0, x1)
U76_aaaaaaa(x0)
lessc13_in_ga(x0)
U70_gaaa(x0, x1)
U77_aaaaaaa(x0)
U68_ga(x0, x1)
U78_aaaaaaa(x0)
appc71_in_aaaa
U80_aaaa(x0)

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

(74) Narrowing (SOUND transformation)

By narrowing [LPAR04] the rule P43_IN_AAAAAAAU11_AAAAAAA(partc44_in_aaaa) at position [0] we obtained the following new rules [LPAR04]:

P43_IN_AAAAAAAU11_AAAAAAA(U72_aaaa(lessc13_in_aa))
P43_IN_AAAAAAAU11_AAAAAAA(U74_aaaa(partc44_in_aaaa))
P43_IN_AAAAAAAU11_AAAAAAA(partc44_out_aaaa)

(75) Obligation:

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

U11_AAAAAAA(partc44_out_aaaa) → QS60_IN_AA
QS60_IN_AAP43_IN_AAAAAAA
P43_IN_AAAAAAAU13_AAAAAAA(partc44_in_aaaa)
U13_AAAAAAA(partc44_out_aaaa) → U14_AAAAAAA(qsc60_in_aa)
U14_AAAAAAA(qsc60_out_aa) → QS60_IN_AA
P43_IN_AAAAAAAU11_AAAAAAA(U72_aaaa(lessc13_in_aa))
P43_IN_AAAAAAAU11_AAAAAAA(U74_aaaa(partc44_in_aaaa))
P43_IN_AAAAAAAU11_AAAAAAA(partc44_out_aaaa)

The TRS R consists of the following rules:

partc44_in_aaaaU72_aaaa(lessc13_in_aa)
partc44_in_aaaaU74_aaaa(partc44_in_aaaa)
partc44_in_aaaapartc44_out_aaaa
qsc60_in_aaqsc60_out_aa
qsc60_in_aaU79_aa(qc43_in_aaaaaaa)
U72_aaaa(lessc13_out_aa(T153)) → U73_aaaa(partc23_in_gaaa(T153))
U74_aaaa(partc44_out_aaaa) → partc44_out_aaaa
U79_aa(qc43_out_aaaaaaa) → qsc60_out_aa
lessc13_in_aalessc13_out_aa(0)
lessc13_in_aaU68_aa(lessc13_in_aa)
U73_aaaa(partc23_out_gaaa(T153)) → partc44_out_aaaa
qc43_in_aaaaaaaU75_aaaaaaa(partc44_in_aaaa)
U68_aa(lessc13_out_aa(T45)) → lessc13_out_aa(s(T45))
partc23_in_gaaa(T70) → U69_gaaa(T70, lessc13_in_ga(T70))
partc23_in_gaaa(T95) → U71_gaaa(T95, partc23_in_gaaa(T95))
partc23_in_gaaa(T104) → partc23_out_gaaa(T104)
U75_aaaaaaa(partc44_out_aaaa) → U76_aaaaaaa(qsc60_in_aa)
U69_gaaa(T70, lessc13_out_ga(T70)) → U70_gaaa(T70, partc23_in_gaaa(T70))
U71_gaaa(T95, partc23_out_gaaa(T95)) → partc23_out_gaaa(T95)
U76_aaaaaaa(qsc60_out_aa) → U77_aaaaaaa(qsc60_in_aa)
lessc13_in_ga(0) → lessc13_out_ga(0)
lessc13_in_ga(s(T45)) → U68_ga(T45, lessc13_in_ga(T45))
U70_gaaa(T70, partc23_out_gaaa(T70)) → partc23_out_gaaa(T70)
U77_aaaaaaa(qsc60_out_aa) → U78_aaaaaaa(appc71_in_aaaa)
U68_ga(T45, lessc13_out_ga(T45)) → lessc13_out_ga(s(T45))
U78_aaaaaaa(appc71_out_aaaa) → qc43_out_aaaaaaa
appc71_in_aaaaappc71_out_aaaa
appc71_in_aaaaU80_aaaa(appc71_in_aaaa)
U80_aaaa(appc71_out_aaaa) → appc71_out_aaaa

The set Q consists of the following terms:

partc44_in_aaaa
qsc60_in_aa
U72_aaaa(x0)
U74_aaaa(x0)
U79_aa(x0)
lessc13_in_aa
U73_aaaa(x0)
qc43_in_aaaaaaa
U68_aa(x0)
partc23_in_gaaa(x0)
U75_aaaaaaa(x0)
U69_gaaa(x0, x1)
U71_gaaa(x0, x1)
U76_aaaaaaa(x0)
lessc13_in_ga(x0)
U70_gaaa(x0, x1)
U77_aaaaaaa(x0)
U68_ga(x0, x1)
U78_aaaaaaa(x0)
appc71_in_aaaa
U80_aaaa(x0)

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

(76) Narrowing (SOUND transformation)

By narrowing [LPAR04] the rule P43_IN_AAAAAAAU13_AAAAAAA(partc44_in_aaaa) at position [0] we obtained the following new rules [LPAR04]:

P43_IN_AAAAAAAU13_AAAAAAA(U72_aaaa(lessc13_in_aa))
P43_IN_AAAAAAAU13_AAAAAAA(U74_aaaa(partc44_in_aaaa))
P43_IN_AAAAAAAU13_AAAAAAA(partc44_out_aaaa)

(77) Obligation:

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

U11_AAAAAAA(partc44_out_aaaa) → QS60_IN_AA
QS60_IN_AAP43_IN_AAAAAAA
U13_AAAAAAA(partc44_out_aaaa) → U14_AAAAAAA(qsc60_in_aa)
U14_AAAAAAA(qsc60_out_aa) → QS60_IN_AA
P43_IN_AAAAAAAU11_AAAAAAA(U72_aaaa(lessc13_in_aa))
P43_IN_AAAAAAAU11_AAAAAAA(U74_aaaa(partc44_in_aaaa))
P43_IN_AAAAAAAU11_AAAAAAA(partc44_out_aaaa)
P43_IN_AAAAAAAU13_AAAAAAA(U72_aaaa(lessc13_in_aa))
P43_IN_AAAAAAAU13_AAAAAAA(U74_aaaa(partc44_in_aaaa))
P43_IN_AAAAAAAU13_AAAAAAA(partc44_out_aaaa)

The TRS R consists of the following rules:

partc44_in_aaaaU72_aaaa(lessc13_in_aa)
partc44_in_aaaaU74_aaaa(partc44_in_aaaa)
partc44_in_aaaapartc44_out_aaaa
qsc60_in_aaqsc60_out_aa
qsc60_in_aaU79_aa(qc43_in_aaaaaaa)
U72_aaaa(lessc13_out_aa(T153)) → U73_aaaa(partc23_in_gaaa(T153))
U74_aaaa(partc44_out_aaaa) → partc44_out_aaaa
U79_aa(qc43_out_aaaaaaa) → qsc60_out_aa
lessc13_in_aalessc13_out_aa(0)
lessc13_in_aaU68_aa(lessc13_in_aa)
U73_aaaa(partc23_out_gaaa(T153)) → partc44_out_aaaa
qc43_in_aaaaaaaU75_aaaaaaa(partc44_in_aaaa)
U68_aa(lessc13_out_aa(T45)) → lessc13_out_aa(s(T45))
partc23_in_gaaa(T70) → U69_gaaa(T70, lessc13_in_ga(T70))
partc23_in_gaaa(T95) → U71_gaaa(T95, partc23_in_gaaa(T95))
partc23_in_gaaa(T104) → partc23_out_gaaa(T104)
U75_aaaaaaa(partc44_out_aaaa) → U76_aaaaaaa(qsc60_in_aa)
U69_gaaa(T70, lessc13_out_ga(T70)) → U70_gaaa(T70, partc23_in_gaaa(T70))
U71_gaaa(T95, partc23_out_gaaa(T95)) → partc23_out_gaaa(T95)
U76_aaaaaaa(qsc60_out_aa) → U77_aaaaaaa(qsc60_in_aa)
lessc13_in_ga(0) → lessc13_out_ga(0)
lessc13_in_ga(s(T45)) → U68_ga(T45, lessc13_in_ga(T45))
U70_gaaa(T70, partc23_out_gaaa(T70)) → partc23_out_gaaa(T70)
U77_aaaaaaa(qsc60_out_aa) → U78_aaaaaaa(appc71_in_aaaa)
U68_ga(T45, lessc13_out_ga(T45)) → lessc13_out_ga(s(T45))
U78_aaaaaaa(appc71_out_aaaa) → qc43_out_aaaaaaa
appc71_in_aaaaappc71_out_aaaa
appc71_in_aaaaU80_aaaa(appc71_in_aaaa)
U80_aaaa(appc71_out_aaaa) → appc71_out_aaaa

The set Q consists of the following terms:

partc44_in_aaaa
qsc60_in_aa
U72_aaaa(x0)
U74_aaaa(x0)
U79_aa(x0)
lessc13_in_aa
U73_aaaa(x0)
qc43_in_aaaaaaa
U68_aa(x0)
partc23_in_gaaa(x0)
U75_aaaaaaa(x0)
U69_gaaa(x0, x1)
U71_gaaa(x0, x1)
U76_aaaaaaa(x0)
lessc13_in_ga(x0)
U70_gaaa(x0, x1)
U77_aaaaaaa(x0)
U68_ga(x0, x1)
U78_aaaaaaa(x0)
appc71_in_aaaa
U80_aaaa(x0)

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

(78) Narrowing (SOUND transformation)

By narrowing [LPAR04] the rule U13_AAAAAAA(partc44_out_aaaa) → U14_AAAAAAA(qsc60_in_aa) at position [0] we obtained the following new rules [LPAR04]:

U13_AAAAAAA(partc44_out_aaaa) → U14_AAAAAAA(qsc60_out_aa)
U13_AAAAAAA(partc44_out_aaaa) → U14_AAAAAAA(U79_aa(qc43_in_aaaaaaa))

(79) Obligation:

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

U11_AAAAAAA(partc44_out_aaaa) → QS60_IN_AA
QS60_IN_AAP43_IN_AAAAAAA
U14_AAAAAAA(qsc60_out_aa) → QS60_IN_AA
P43_IN_AAAAAAAU11_AAAAAAA(U72_aaaa(lessc13_in_aa))
P43_IN_AAAAAAAU11_AAAAAAA(U74_aaaa(partc44_in_aaaa))
P43_IN_AAAAAAAU11_AAAAAAA(partc44_out_aaaa)
P43_IN_AAAAAAAU13_AAAAAAA(U72_aaaa(lessc13_in_aa))
P43_IN_AAAAAAAU13_AAAAAAA(U74_aaaa(partc44_in_aaaa))
P43_IN_AAAAAAAU13_AAAAAAA(partc44_out_aaaa)
U13_AAAAAAA(partc44_out_aaaa) → U14_AAAAAAA(qsc60_out_aa)
U13_AAAAAAA(partc44_out_aaaa) → U14_AAAAAAA(U79_aa(qc43_in_aaaaaaa))

The TRS R consists of the following rules:

partc44_in_aaaaU72_aaaa(lessc13_in_aa)
partc44_in_aaaaU74_aaaa(partc44_in_aaaa)
partc44_in_aaaapartc44_out_aaaa
qsc60_in_aaqsc60_out_aa
qsc60_in_aaU79_aa(qc43_in_aaaaaaa)
U72_aaaa(lessc13_out_aa(T153)) → U73_aaaa(partc23_in_gaaa(T153))
U74_aaaa(partc44_out_aaaa) → partc44_out_aaaa
U79_aa(qc43_out_aaaaaaa) → qsc60_out_aa
lessc13_in_aalessc13_out_aa(0)
lessc13_in_aaU68_aa(lessc13_in_aa)
U73_aaaa(partc23_out_gaaa(T153)) → partc44_out_aaaa
qc43_in_aaaaaaaU75_aaaaaaa(partc44_in_aaaa)
U68_aa(lessc13_out_aa(T45)) → lessc13_out_aa(s(T45))
partc23_in_gaaa(T70) → U69_gaaa(T70, lessc13_in_ga(T70))
partc23_in_gaaa(T95) → U71_gaaa(T95, partc23_in_gaaa(T95))
partc23_in_gaaa(T104) → partc23_out_gaaa(T104)
U75_aaaaaaa(partc44_out_aaaa) → U76_aaaaaaa(qsc60_in_aa)
U69_gaaa(T70, lessc13_out_ga(T70)) → U70_gaaa(T70, partc23_in_gaaa(T70))
U71_gaaa(T95, partc23_out_gaaa(T95)) → partc23_out_gaaa(T95)
U76_aaaaaaa(qsc60_out_aa) → U77_aaaaaaa(qsc60_in_aa)
lessc13_in_ga(0) → lessc13_out_ga(0)
lessc13_in_ga(s(T45)) → U68_ga(T45, lessc13_in_ga(T45))
U70_gaaa(T70, partc23_out_gaaa(T70)) → partc23_out_gaaa(T70)
U77_aaaaaaa(qsc60_out_aa) → U78_aaaaaaa(appc71_in_aaaa)
U68_ga(T45, lessc13_out_ga(T45)) → lessc13_out_ga(s(T45))
U78_aaaaaaa(appc71_out_aaaa) → qc43_out_aaaaaaa
appc71_in_aaaaappc71_out_aaaa
appc71_in_aaaaU80_aaaa(appc71_in_aaaa)
U80_aaaa(appc71_out_aaaa) → appc71_out_aaaa

The set Q consists of the following terms:

partc44_in_aaaa
qsc60_in_aa
U72_aaaa(x0)
U74_aaaa(x0)
U79_aa(x0)
lessc13_in_aa
U73_aaaa(x0)
qc43_in_aaaaaaa
U68_aa(x0)
partc23_in_gaaa(x0)
U75_aaaaaaa(x0)
U69_gaaa(x0, x1)
U71_gaaa(x0, x1)
U76_aaaaaaa(x0)
lessc13_in_ga(x0)
U70_gaaa(x0, x1)
U77_aaaaaaa(x0)
U68_ga(x0, x1)
U78_aaaaaaa(x0)
appc71_in_aaaa
U80_aaaa(x0)

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

(80) NonTerminationProof (EQUIVALENT transformation)

We used the non-termination processor [FROCOS05] to show that the DP problem is infinite.
Found a loop by narrowing to the left:

s = QS60_IN_AA evaluates to t =QS60_IN_AA

Thus s starts an infinite chain as s semiunifies with t with the following substitutions:
  • Semiunifier: [ ]
  • Matcher: [ ]




Rewriting sequence

QS60_IN_AAP43_IN_AAAAAAA
with rule QS60_IN_AAP43_IN_AAAAAAA at position [] and matcher [ ]

P43_IN_AAAAAAAU11_AAAAAAA(partc44_out_aaaa)
with rule P43_IN_AAAAAAAU11_AAAAAAA(partc44_out_aaaa) at position [] and matcher [ ]

U11_AAAAAAA(partc44_out_aaaa)QS60_IN_AA
with rule U11_AAAAAAA(partc44_out_aaaa) → QS60_IN_AA

Now applying the matcher to the start term leads to a term which is equal to the last term in the rewriting sequence


All these steps are and every following step will be a correct step w.r.t to Q.



(81) NO