(0) Obligation:

Clauses:

ms([], []).
ms(.(X, []), .(X, [])).
ms(.(X, .(Y, Xs)), Ys) :- ','(split(.(X, .(Y, Xs)), X1s, X2s), ','(ms(X1s, Y1s), ','(ms(X2s, Y2s), merge(Y1s, Y2s, Ys)))).
split([], [], []).
split(.(X, Xs), .(X, Ys), Zs) :- split(Xs, Zs, Ys).
merge([], Xs, Xs).
merge(Xs, [], Xs).
merge(.(X, Xs), .(Y, Ys), .(X, Zs)) :- ','(less(X, s(Y)), merge(Xs, .(Y, Ys), Zs)).
merge(.(X, Xs), .(Y, Ys), .(Y, Zs)) :- ','(less(Y, X), merge(.(X, Xs), Ys, Zs)).
less(0, s(X1)).
less(s(X), s(Y)) :- less(X, Y).

Queries:

ms(a,g).

(1) PrologToDTProblemTransformerProof (SOUND transformation)

Built DT problem from termination graph.

(2) Obligation:

Triples:

split16(.(T49, T51), .(T49, X89), X90) :- split16(T51, X90, X89).
split12(T42, T44, .(T42, X71), X72) :- split16(T44, X72, X71).
p34(T72, T73, T74, X123, X124, X125, X126, X127) :- split12(T72, .(T73, T74), X123, X124).
p34(T72, T73, T74, T78, T79, X125, X126, X127) :- ','(splitc12(T72, .(T73, T74), T78, T79), ms38(T78, X125)).
p34(T72, T73, T74, T78, T84, T83, X126, X127) :- ','(splitc12(T72, .(T73, T74), T78, T84), ','(msc38(T78, T83), ms38(T84, X126))).
p34(T72, T73, T74, T78, T84, T106, T105, X127) :- ','(splitc12(T72, .(T73, T74), T78, T84), ','(msc38(T78, T106), ','(msc38(T84, T105), merge54(T106, T105, X127)))).
ms38(.(T99, .(T100, T101)), X172) :- p34(T99, T100, T101, X168, X169, X170, X171, X172).
merge54(.(T139, T141), .(T140, T142), .(T139, X226)) :- less70(T139, T140).
merge54(.(T139, T145), .(T146, T147), .(T139, X226)) :- ','(lessc70(T139, T146), merge54(T145, .(T146, T147), X226)).
merge54(.(T197, T199), .(T196, T198), .(T196, X287)) :- less78(T196, T197).
merge54(.(T202, T203), .(T196, T204), .(T196, X287)) :- ','(lessc78(T196, T202), merge54(.(T202, T203), T204, X287)).
less78(s(T176), s(T177)) :- less78(T176, T177).
ms25(T72, .(T73, T74), X127) :- p34(T72, T73, T74, X123, X124, X125, X126, X127).
less70(s(T161), T162) :- less78(T161, T162).
p179(T513, T518, T519, T520, T517) :- less70(T513, T518).
p179(T513, T568, .(T563, T569), T570, .(T563, T567)) :- ','(lessc70(T513, T568), p179(T563, T568, T569, T570, T567)).
p179(T513, T585, .(T588, T590), T589, .(T585, T587)) :- ','(lessc70(T513, T585), p194(T585, T588, T590, T589, T587)).
p194(T585, T588, T590, T589, T587) :- less78(T585, T588).
p194(T585, T632, T638, .(T637, T639), .(T632, T636)) :- ','(lessc78(T585, T632), p179(T632, T637, T638, T639, T636)).
p194(T585, T657, T659, .(T654, T658), .(T654, T656)) :- ','(lessc78(T585, T657), p194(T654, T657, T659, T658, T656)).
ms1(.(T29, .(T27, T28)), []) :- split12(T27, T28, X42, X41).
ms1(.(T34, .(T27, T28)), []) :- ','(splitc12(T27, T28, T32, T33), ms25(T34, T33, X13)).
ms1(.(T34, .(T27, T28)), []) :- ','(splitc12(T27, T28, T55, T33), ','(msc25(T34, T33, T54), ms38(T55, X14))).
ms1(.(T34, .(T27, T28)), []) :- ','(splitc12(T27, T28, T55, T33), ','(msc25(T34, T33, T212), ','(msc38(T55, T211), merge93(T212, T211)))).
ms1(.(T262, .(T260, T261)), .(T242, [])) :- split12(T260, T261, X367, X366).
ms1(.(T267, .(T260, T261)), .(T242, [])) :- ','(splitc12(T260, T261, T265, T266), ms25(T267, T266, X338)).
ms1(.(T267, .(T260, T261)), .(T242, [])) :- ','(splitc12(T260, T261, T273, T266), ','(msc25(T267, T266, T272), ms38(T273, X339))).
ms1(.(T267, .(T260, T261)), .(T318, [])) :- ','(splitc12(T260, T261, T273, T266), ','(msc25(T267, T266, .(T318, T323)), ','(msc38(T273, .(T322, T324)), less70(T318, T322)))).
ms1(.(T267, .(T260, T261)), .(T318, [])) :- ','(splitc12(T260, T261, T273, T266), ','(msc25(T267, T266, .(T318, T327)), ','(msc38(T273, .(T328, T329)), ','(lessc70(T318, T328), merge93(T327, .(T328, T329)))))).
ms1(.(T267, .(T260, T261)), .(T356, [])) :- ','(splitc12(T260, T261, T273, T266), ','(msc25(T267, T266, .(T358, T360)), ','(msc38(T273, .(T356, T359)), less78(T356, T358)))).
ms1(.(T267, .(T260, T261)), .(T356, [])) :- ','(splitc12(T260, T261, T273, T266), ','(msc25(T267, T266, .(T363, T364)), ','(msc38(T273, .(T356, T365)), ','(lessc78(T356, T363), merge93(.(T363, T364), T365))))).
ms1(.(T407, .(T405, T406)), T387) :- split12(T405, T406, X523, X522).
ms1(.(T412, .(T405, T406)), T387) :- ','(splitc12(T405, T406, T410, T411), ms25(T412, T411, X494)).
ms1(.(T412, .(T405, T406)), T387) :- ','(splitc12(T405, T406, T420, T411), ','(msc25(T412, T411, T419), ms38(T420, X495))).
ms1(.(T412, .(T405, T406)), .(T461, T465)) :- ','(splitc12(T405, T406, T420, T411), ','(msc25(T412, T411, .(T461, T467)), ','(msc38(T420, .(T466, T468)), less70(T461, T466)))).
ms1(.(T412, .(T405, T406)), .(T461, .(T513, T517))) :- ','(splitc12(T405, T406, T420, T411), ','(msc25(T412, T411, .(T461, .(T513, T519))), ','(msc38(T420, .(T518, T520)), ','(lessc70(T461, T518), p179(T513, T518, T519, T520, T517))))).
ms1(.(T412, .(T405, T406)), .(T461, .(T674, T676))) :- ','(splitc12(T405, T406, T420, T411), ','(msc25(T412, T411, .(T461, .(T677, T679))), ','(msc38(T420, .(T674, T678)), ','(lessc70(T461, T674), p194(T674, T677, T679, T678, T676))))).
ms1(.(T412, .(T405, T406)), .(T694, T696)) :- ','(splitc12(T405, T406, T420, T411), ','(msc25(T412, T411, .(T697, T699)), ','(msc38(T420, .(T694, T698)), p194(T694, T697, T699, T698, T696)))).

Clauses:

splitc16([], [], []).
splitc16(.(T49, T51), .(T49, X89), X90) :- splitc16(T51, X90, X89).
splitc12(T42, T44, .(T42, X71), X72) :- splitc16(T44, X72, X71).
qc34(T72, T73, T74, T78, T84, T106, T105, X127) :- ','(splitc12(T72, .(T73, T74), T78, T84), ','(msc38(T78, T106), ','(msc38(T84, T105), mergec54(T106, T105, X127)))).
msc38([], []).
msc38(.(T89, []), .(T89, [])).
msc38(.(T99, .(T100, T101)), X172) :- qc34(T99, T100, T101, X168, X169, X170, X171, X172).
mergec54([], T113, T113).
mergec54(T118, [], T118).
mergec54(.(T139, T145), .(T146, T147), .(T139, X226)) :- ','(lessc70(T139, T146), mergec54(T145, .(T146, T147), X226)).
mergec54(.(T202, T203), .(T196, T204), .(T196, X287)) :- ','(lessc78(T196, T202), mergec54(.(T202, T203), T204, X287)).
lessc78(0, s(T169)).
lessc78(s(T176), s(T177)) :- lessc78(T176, T177).
msc25(T62, [], .(T62, [])).
msc25(T72, .(T73, T74), X127) :- qc34(T72, T73, T74, X123, X124, X125, X126, X127).
lessc70(0, T154).
lessc70(s(T161), T162) :- lessc78(T161, T162).
mergec93([], []).
mergec93([], []).
qc179(T513, T540, [], T541, .(T540, T541)) :- lessc70(T513, T540).
qc179(T513, T568, .(T563, T569), T570, .(T563, T567)) :- ','(lessc70(T513, T568), qc179(T563, T568, T569, T570, T567)).
qc179(T513, T585, .(T588, T590), T589, .(T585, T587)) :- ','(lessc70(T513, T585), qc194(T585, T588, T590, T589, T587)).
qc194(T585, T610, T611, [], .(T610, T611)) :- lessc78(T585, T610).
qc194(T585, T632, T638, .(T637, T639), .(T632, T636)) :- ','(lessc78(T585, T632), qc179(T632, T637, T638, T639, T636)).
qc194(T585, T657, T659, .(T654, T658), .(T654, T656)) :- ','(lessc78(T585, T657), qc194(T654, T657, T659, T658, T656)).

Afs:

ms1(x1, x2)  =  ms1(x2)

(3) UndefinedPredicateInTriplesTransformerProof (SOUND transformation)

Deleted triples and predicates having undefined goals [UNKNOWN].

(4) Obligation:

Triples:

split16(.(T49, T51), .(T49, X89), X90) :- split16(T51, X90, X89).
split12(T42, T44, .(T42, X71), X72) :- split16(T44, X72, X71).
p34(T72, T73, T74, X123, X124, X125, X126, X127) :- split12(T72, .(T73, T74), X123, X124).
p34(T72, T73, T74, T78, T79, X125, X126, X127) :- ','(splitc12(T72, .(T73, T74), T78, T79), ms38(T78, X125)).
p34(T72, T73, T74, T78, T84, T83, X126, X127) :- ','(splitc12(T72, .(T73, T74), T78, T84), ','(msc38(T78, T83), ms38(T84, X126))).
p34(T72, T73, T74, T78, T84, T106, T105, X127) :- ','(splitc12(T72, .(T73, T74), T78, T84), ','(msc38(T78, T106), ','(msc38(T84, T105), merge54(T106, T105, X127)))).
ms38(.(T99, .(T100, T101)), X172) :- p34(T99, T100, T101, X168, X169, X170, X171, X172).
merge54(.(T139, T141), .(T140, T142), .(T139, X226)) :- less70(T139, T140).
merge54(.(T139, T145), .(T146, T147), .(T139, X226)) :- ','(lessc70(T139, T146), merge54(T145, .(T146, T147), X226)).
merge54(.(T197, T199), .(T196, T198), .(T196, X287)) :- less78(T196, T197).
merge54(.(T202, T203), .(T196, T204), .(T196, X287)) :- ','(lessc78(T196, T202), merge54(.(T202, T203), T204, X287)).
less78(s(T176), s(T177)) :- less78(T176, T177).
ms25(T72, .(T73, T74), X127) :- p34(T72, T73, T74, X123, X124, X125, X126, X127).
less70(s(T161), T162) :- less78(T161, T162).
p179(T513, T518, T519, T520, T517) :- less70(T513, T518).
p179(T513, T568, .(T563, T569), T570, .(T563, T567)) :- ','(lessc70(T513, T568), p179(T563, T568, T569, T570, T567)).
p179(T513, T585, .(T588, T590), T589, .(T585, T587)) :- ','(lessc70(T513, T585), p194(T585, T588, T590, T589, T587)).
p194(T585, T588, T590, T589, T587) :- less78(T585, T588).
p194(T585, T632, T638, .(T637, T639), .(T632, T636)) :- ','(lessc78(T585, T632), p179(T632, T637, T638, T639, T636)).
p194(T585, T657, T659, .(T654, T658), .(T654, T656)) :- ','(lessc78(T585, T657), p194(T654, T657, T659, T658, T656)).
ms1(.(T29, .(T27, T28)), []) :- split12(T27, T28, X42, X41).
ms1(.(T34, .(T27, T28)), []) :- ','(splitc12(T27, T28, T32, T33), ms25(T34, T33, X13)).
ms1(.(T34, .(T27, T28)), []) :- ','(splitc12(T27, T28, T55, T33), ','(msc25(T34, T33, T54), ms38(T55, X14))).
ms1(.(T262, .(T260, T261)), .(T242, [])) :- split12(T260, T261, X367, X366).
ms1(.(T267, .(T260, T261)), .(T242, [])) :- ','(splitc12(T260, T261, T265, T266), ms25(T267, T266, X338)).
ms1(.(T267, .(T260, T261)), .(T242, [])) :- ','(splitc12(T260, T261, T273, T266), ','(msc25(T267, T266, T272), ms38(T273, X339))).
ms1(.(T267, .(T260, T261)), .(T318, [])) :- ','(splitc12(T260, T261, T273, T266), ','(msc25(T267, T266, .(T318, T323)), ','(msc38(T273, .(T322, T324)), less70(T318, T322)))).
ms1(.(T267, .(T260, T261)), .(T356, [])) :- ','(splitc12(T260, T261, T273, T266), ','(msc25(T267, T266, .(T358, T360)), ','(msc38(T273, .(T356, T359)), less78(T356, T358)))).
ms1(.(T407, .(T405, T406)), T387) :- split12(T405, T406, X523, X522).
ms1(.(T412, .(T405, T406)), T387) :- ','(splitc12(T405, T406, T410, T411), ms25(T412, T411, X494)).
ms1(.(T412, .(T405, T406)), T387) :- ','(splitc12(T405, T406, T420, T411), ','(msc25(T412, T411, T419), ms38(T420, X495))).
ms1(.(T412, .(T405, T406)), .(T461, T465)) :- ','(splitc12(T405, T406, T420, T411), ','(msc25(T412, T411, .(T461, T467)), ','(msc38(T420, .(T466, T468)), less70(T461, T466)))).
ms1(.(T412, .(T405, T406)), .(T461, .(T513, T517))) :- ','(splitc12(T405, T406, T420, T411), ','(msc25(T412, T411, .(T461, .(T513, T519))), ','(msc38(T420, .(T518, T520)), ','(lessc70(T461, T518), p179(T513, T518, T519, T520, T517))))).
ms1(.(T412, .(T405, T406)), .(T461, .(T674, T676))) :- ','(splitc12(T405, T406, T420, T411), ','(msc25(T412, T411, .(T461, .(T677, T679))), ','(msc38(T420, .(T674, T678)), ','(lessc70(T461, T674), p194(T674, T677, T679, T678, T676))))).
ms1(.(T412, .(T405, T406)), .(T694, T696)) :- ','(splitc12(T405, T406, T420, T411), ','(msc25(T412, T411, .(T697, T699)), ','(msc38(T420, .(T694, T698)), p194(T694, T697, T699, T698, T696)))).

Clauses:

splitc16([], [], []).
splitc16(.(T49, T51), .(T49, X89), X90) :- splitc16(T51, X90, X89).
splitc12(T42, T44, .(T42, X71), X72) :- splitc16(T44, X72, X71).
qc34(T72, T73, T74, T78, T84, T106, T105, X127) :- ','(splitc12(T72, .(T73, T74), T78, T84), ','(msc38(T78, T106), ','(msc38(T84, T105), mergec54(T106, T105, X127)))).
msc38([], []).
msc38(.(T89, []), .(T89, [])).
msc38(.(T99, .(T100, T101)), X172) :- qc34(T99, T100, T101, X168, X169, X170, X171, X172).
mergec54([], T113, T113).
mergec54(T118, [], T118).
mergec54(.(T139, T145), .(T146, T147), .(T139, X226)) :- ','(lessc70(T139, T146), mergec54(T145, .(T146, T147), X226)).
mergec54(.(T202, T203), .(T196, T204), .(T196, X287)) :- ','(lessc78(T196, T202), mergec54(.(T202, T203), T204, X287)).
lessc78(0, s(T169)).
lessc78(s(T176), s(T177)) :- lessc78(T176, T177).
msc25(T62, [], .(T62, [])).
msc25(T72, .(T73, T74), X127) :- qc34(T72, T73, T74, X123, X124, X125, X126, X127).
lessc70(0, T154).
lessc70(s(T161), T162) :- lessc78(T161, T162).
mergec93([], []).
mergec93([], []).
qc179(T513, T540, [], T541, .(T540, T541)) :- lessc70(T513, T540).
qc179(T513, T568, .(T563, T569), T570, .(T563, T567)) :- ','(lessc70(T513, T568), qc179(T563, T568, T569, T570, T567)).
qc179(T513, T585, .(T588, T590), T589, .(T585, T587)) :- ','(lessc70(T513, T585), qc194(T585, T588, T590, T589, T587)).
qc194(T585, T610, T611, [], .(T610, T611)) :- lessc78(T585, T610).
qc194(T585, T632, T638, .(T637, T639), .(T632, T636)) :- ','(lessc78(T585, T632), qc179(T632, T637, T638, T639, T636)).
qc194(T585, T657, T659, .(T654, T658), .(T654, T656)) :- ','(lessc78(T585, T657), qc194(T654, T657, T659, T658, T656)).

Afs:

ms1(x1, x2)  =  ms1(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:
ms1_in: (f,b)
split12_in: (f,f,f,f)
split16_in: (f,f,f)
splitc12_in: (f,f,f,f)
splitc16_in: (f,f,f)
ms25_in: (f,f,f)
p34_in: (f,f,f,f,f,f,f,f)
ms38_in: (f,f)
msc38_in: (f,f)
qc34_in: (f,f,f,f,f,f,f,f)
mergec54_in: (f,f,f)
lessc70_in: (f,f) (b,f) (b,b)
lessc78_in: (f,f) (b,f) (b,b)
merge54_in: (f,f,f)
less70_in: (f,f) (b,f)
less78_in: (f,f) (b,f)
msc25_in: (f,f,f)
p179_in: (b,f,f,f,b)
p194_in: (b,f,f,f,b)
Transforming TRIPLES into the following Term Rewriting System:
Pi DP problem:
The TRS P consists of the following rules:

MS1_IN_AG(.(T29, .(T27, T28)), []) → U33_AG(T29, T27, T28, split12_in_aaaa(T27, T28, X42, X41))
MS1_IN_AG(.(T29, .(T27, T28)), []) → SPLIT12_IN_AAAA(T27, T28, X42, X41)
SPLIT12_IN_AAAA(T42, T44, .(T42, X71), X72) → U2_AAAA(T42, T44, X71, X72, split16_in_aaa(T44, X72, X71))
SPLIT12_IN_AAAA(T42, T44, .(T42, X71), X72) → SPLIT16_IN_AAA(T44, X72, X71)
SPLIT16_IN_AAA(.(T49, T51), .(T49, X89), X90) → U1_AAA(T49, T51, X89, X90, split16_in_aaa(T51, X90, X89))
SPLIT16_IN_AAA(.(T49, T51), .(T49, X89), X90) → SPLIT16_IN_AAA(T51, X90, X89)
MS1_IN_AG(.(T34, .(T27, T28)), []) → U34_AG(T34, T27, T28, splitc12_in_aaaa(T27, T28, T32, T33))
U34_AG(T34, T27, T28, splitc12_out_aaaa(T27, T28, T32, T33)) → U35_AG(T34, T27, T28, ms25_in_aaa(T34, T33, X13))
U34_AG(T34, T27, T28, splitc12_out_aaaa(T27, T28, T32, T33)) → MS25_IN_AAA(T34, T33, X13)
MS25_IN_AAA(T72, .(T73, T74), X127) → U21_AAA(T72, T73, T74, X127, p34_in_aaaaaaaa(T72, T73, T74, X123, X124, X125, X126, X127))
MS25_IN_AAA(T72, .(T73, T74), X127) → P34_IN_AAAAAAAA(T72, T73, T74, X123, X124, X125, X126, X127)
P34_IN_AAAAAAAA(T72, T73, T74, X123, X124, X125, X126, X127) → U3_AAAAAAAA(T72, T73, T74, X123, X124, X125, X126, X127, split12_in_aaaa(T72, .(T73, T74), X123, X124))
P34_IN_AAAAAAAA(T72, T73, T74, X123, X124, X125, X126, X127) → SPLIT12_IN_AAAA(T72, .(T73, T74), X123, X124)
P34_IN_AAAAAAAA(T72, T73, T74, T78, T79, X125, X126, X127) → U4_AAAAAAAA(T72, T73, T74, T78, T79, X125, X126, X127, splitc12_in_aaaa(T72, .(T73, T74), T78, T79))
U4_AAAAAAAA(T72, T73, T74, T78, T79, X125, X126, X127, splitc12_out_aaaa(T72, .(T73, T74), T78, T79)) → U5_AAAAAAAA(T72, T73, T74, T78, T79, X125, X126, X127, ms38_in_aa(T78, X125))
U4_AAAAAAAA(T72, T73, T74, T78, T79, X125, X126, X127, splitc12_out_aaaa(T72, .(T73, T74), T78, T79)) → MS38_IN_AA(T78, X125)
MS38_IN_AA(.(T99, .(T100, T101)), X172) → U13_AA(T99, T100, T101, X172, p34_in_aaaaaaaa(T99, T100, T101, X168, X169, X170, X171, X172))
MS38_IN_AA(.(T99, .(T100, T101)), X172) → P34_IN_AAAAAAAA(T99, T100, T101, X168, X169, X170, X171, X172)
P34_IN_AAAAAAAA(T72, T73, T74, T78, T84, T83, X126, X127) → U6_AAAAAAAA(T72, T73, T74, T78, T84, T83, X126, X127, splitc12_in_aaaa(T72, .(T73, T74), T78, T84))
U6_AAAAAAAA(T72, T73, T74, T78, T84, T83, X126, X127, splitc12_out_aaaa(T72, .(T73, T74), T78, T84)) → U7_AAAAAAAA(T72, T73, T74, T78, T84, T83, X126, X127, msc38_in_aa(T78, T83))
U7_AAAAAAAA(T72, T73, T74, T78, T84, T83, X126, X127, msc38_out_aa(T78, T83)) → U8_AAAAAAAA(T72, T73, T74, T78, T84, T83, X126, X127, ms38_in_aa(T84, X126))
U7_AAAAAAAA(T72, T73, T74, T78, T84, T83, X126, X127, msc38_out_aa(T78, T83)) → MS38_IN_AA(T84, X126)
P34_IN_AAAAAAAA(T72, T73, T74, T78, T84, T106, T105, X127) → U9_AAAAAAAA(T72, T73, T74, T78, T84, T106, T105, X127, splitc12_in_aaaa(T72, .(T73, T74), T78, T84))
U9_AAAAAAAA(T72, T73, T74, T78, T84, T106, T105, X127, splitc12_out_aaaa(T72, .(T73, T74), T78, T84)) → U10_AAAAAAAA(T72, T73, T74, T78, T84, T106, T105, X127, msc38_in_aa(T78, T106))
U10_AAAAAAAA(T72, T73, T74, T78, T84, T106, T105, X127, msc38_out_aa(T78, T106)) → U11_AAAAAAAA(T72, T73, T74, T78, T84, T106, T105, X127, msc38_in_aa(T84, T105))
U11_AAAAAAAA(T72, T73, T74, T78, T84, T106, T105, X127, msc38_out_aa(T84, T105)) → U12_AAAAAAAA(T72, T73, T74, T78, T84, T106, T105, X127, merge54_in_aaa(T106, T105, X127))
U11_AAAAAAAA(T72, T73, T74, T78, T84, T106, T105, X127, msc38_out_aa(T84, T105)) → MERGE54_IN_AAA(T106, T105, X127)
MERGE54_IN_AAA(.(T139, T141), .(T140, T142), .(T139, X226)) → U14_AAA(T139, T141, T140, T142, X226, less70_in_aa(T139, T140))
MERGE54_IN_AAA(.(T139, T141), .(T140, T142), .(T139, X226)) → LESS70_IN_AA(T139, T140)
LESS70_IN_AA(s(T161), T162) → U22_AA(T161, T162, less78_in_aa(T161, T162))
LESS70_IN_AA(s(T161), T162) → LESS78_IN_AA(T161, T162)
LESS78_IN_AA(s(T176), s(T177)) → U20_AA(T176, T177, less78_in_aa(T176, T177))
LESS78_IN_AA(s(T176), s(T177)) → LESS78_IN_AA(T176, T177)
MERGE54_IN_AAA(.(T139, T145), .(T146, T147), .(T139, X226)) → U15_AAA(T139, T145, T146, T147, X226, lessc70_in_aa(T139, T146))
U15_AAA(T139, T145, T146, T147, X226, lessc70_out_aa(T139, T146)) → U16_AAA(T139, T145, T146, T147, X226, merge54_in_aaa(T145, .(T146, T147), X226))
U15_AAA(T139, T145, T146, T147, X226, lessc70_out_aa(T139, T146)) → MERGE54_IN_AAA(T145, .(T146, T147), X226)
MERGE54_IN_AAA(.(T197, T199), .(T196, T198), .(T196, X287)) → U17_AAA(T197, T199, T196, T198, X287, less78_in_aa(T196, T197))
MERGE54_IN_AAA(.(T197, T199), .(T196, T198), .(T196, X287)) → LESS78_IN_AA(T196, T197)
MERGE54_IN_AAA(.(T202, T203), .(T196, T204), .(T196, X287)) → U18_AAA(T202, T203, T196, T204, X287, lessc78_in_aa(T196, T202))
U18_AAA(T202, T203, T196, T204, X287, lessc78_out_aa(T196, T202)) → U19_AAA(T202, T203, T196, T204, X287, merge54_in_aaa(.(T202, T203), T204, X287))
U18_AAA(T202, T203, T196, T204, X287, lessc78_out_aa(T196, T202)) → MERGE54_IN_AAA(.(T202, T203), T204, X287)
MS1_IN_AG(.(T34, .(T27, T28)), []) → U36_AG(T34, T27, T28, splitc12_in_aaaa(T27, T28, T55, T33))
U36_AG(T34, T27, T28, splitc12_out_aaaa(T27, T28, T55, T33)) → U37_AG(T34, T27, T28, T55, msc25_in_aaa(T34, T33, T54))
U37_AG(T34, T27, T28, T55, msc25_out_aaa(T34, T33, T54)) → U38_AG(T34, T27, T28, ms38_in_aa(T55, X14))
U37_AG(T34, T27, T28, T55, msc25_out_aaa(T34, T33, T54)) → MS38_IN_AA(T55, X14)
MS1_IN_AG(.(T262, .(T260, T261)), .(T242, [])) → U39_AG(T262, T260, T261, T242, split12_in_aaaa(T260, T261, X367, X366))
MS1_IN_AG(.(T262, .(T260, T261)), .(T242, [])) → SPLIT12_IN_AAAA(T260, T261, X367, X366)
MS1_IN_AG(.(T267, .(T260, T261)), .(T242, [])) → U40_AG(T267, T260, T261, T242, splitc12_in_aaaa(T260, T261, T265, T266))
U40_AG(T267, T260, T261, T242, splitc12_out_aaaa(T260, T261, T265, T266)) → U41_AG(T267, T260, T261, T242, ms25_in_aaa(T267, T266, X338))
U40_AG(T267, T260, T261, T242, splitc12_out_aaaa(T260, T261, T265, T266)) → MS25_IN_AAA(T267, T266, X338)
MS1_IN_AG(.(T267, .(T260, T261)), .(T242, [])) → U42_AG(T267, T260, T261, T242, splitc12_in_aaaa(T260, T261, T273, T266))
U42_AG(T267, T260, T261, T242, splitc12_out_aaaa(T260, T261, T273, T266)) → U43_AG(T267, T260, T261, T242, T273, msc25_in_aaa(T267, T266, T272))
U43_AG(T267, T260, T261, T242, T273, msc25_out_aaa(T267, T266, T272)) → U44_AG(T267, T260, T261, T242, ms38_in_aa(T273, X339))
U43_AG(T267, T260, T261, T242, T273, msc25_out_aaa(T267, T266, T272)) → MS38_IN_AA(T273, X339)
MS1_IN_AG(.(T267, .(T260, T261)), .(T318, [])) → U45_AG(T267, T260, T261, T318, splitc12_in_aaaa(T260, T261, T273, T266))
U45_AG(T267, T260, T261, T318, splitc12_out_aaaa(T260, T261, T273, T266)) → U46_AG(T267, T260, T261, T318, T273, msc25_in_aaa(T267, T266, .(T318, T323)))
U46_AG(T267, T260, T261, T318, T273, msc25_out_aaa(T267, T266, .(T318, T323))) → U47_AG(T267, T260, T261, T318, msc38_in_aa(T273, .(T322, T324)))
U47_AG(T267, T260, T261, T318, msc38_out_aa(T273, .(T322, T324))) → U48_AG(T267, T260, T261, T318, less70_in_ga(T318, T322))
U47_AG(T267, T260, T261, T318, msc38_out_aa(T273, .(T322, T324))) → LESS70_IN_GA(T318, T322)
LESS70_IN_GA(s(T161), T162) → U22_GA(T161, T162, less78_in_ga(T161, T162))
LESS70_IN_GA(s(T161), T162) → LESS78_IN_GA(T161, T162)
LESS78_IN_GA(s(T176), s(T177)) → U20_GA(T176, T177, less78_in_ga(T176, T177))
LESS78_IN_GA(s(T176), s(T177)) → LESS78_IN_GA(T176, T177)
MS1_IN_AG(.(T267, .(T260, T261)), .(T356, [])) → U49_AG(T267, T260, T261, T356, splitc12_in_aaaa(T260, T261, T273, T266))
U49_AG(T267, T260, T261, T356, splitc12_out_aaaa(T260, T261, T273, T266)) → U50_AG(T267, T260, T261, T356, T273, msc25_in_aaa(T267, T266, .(T358, T360)))
U50_AG(T267, T260, T261, T356, T273, msc25_out_aaa(T267, T266, .(T358, T360))) → U51_AG(T267, T260, T261, T356, T358, msc38_in_aa(T273, .(T356, T359)))
U51_AG(T267, T260, T261, T356, T358, msc38_out_aa(T273, .(T356, T359))) → U52_AG(T267, T260, T261, T356, less78_in_ga(T356, T358))
U51_AG(T267, T260, T261, T356, T358, msc38_out_aa(T273, .(T356, T359))) → LESS78_IN_GA(T356, T358)
MS1_IN_AG(.(T407, .(T405, T406)), T387) → U53_AG(T407, T405, T406, T387, split12_in_aaaa(T405, T406, X523, X522))
MS1_IN_AG(.(T407, .(T405, T406)), T387) → SPLIT12_IN_AAAA(T405, T406, X523, X522)
MS1_IN_AG(.(T412, .(T405, T406)), T387) → U54_AG(T412, T405, T406, T387, splitc12_in_aaaa(T405, T406, T410, T411))
U54_AG(T412, T405, T406, T387, splitc12_out_aaaa(T405, T406, T410, T411)) → U55_AG(T412, T405, T406, T387, ms25_in_aaa(T412, T411, X494))
U54_AG(T412, T405, T406, T387, splitc12_out_aaaa(T405, T406, T410, T411)) → MS25_IN_AAA(T412, T411, X494)
MS1_IN_AG(.(T412, .(T405, T406)), T387) → U56_AG(T412, T405, T406, T387, splitc12_in_aaaa(T405, T406, T420, T411))
U56_AG(T412, T405, T406, T387, splitc12_out_aaaa(T405, T406, T420, T411)) → U57_AG(T412, T405, T406, T387, T420, msc25_in_aaa(T412, T411, T419))
U57_AG(T412, T405, T406, T387, T420, msc25_out_aaa(T412, T411, T419)) → U58_AG(T412, T405, T406, T387, ms38_in_aa(T420, X495))
U57_AG(T412, T405, T406, T387, T420, msc25_out_aaa(T412, T411, T419)) → MS38_IN_AA(T420, X495)
MS1_IN_AG(.(T412, .(T405, T406)), .(T461, T465)) → U59_AG(T412, T405, T406, T461, T465, splitc12_in_aaaa(T405, T406, T420, T411))
U59_AG(T412, T405, T406, T461, T465, splitc12_out_aaaa(T405, T406, T420, T411)) → U60_AG(T412, T405, T406, T461, T465, T420, msc25_in_aaa(T412, T411, .(T461, T467)))
U60_AG(T412, T405, T406, T461, T465, T420, msc25_out_aaa(T412, T411, .(T461, T467))) → U61_AG(T412, T405, T406, T461, T465, msc38_in_aa(T420, .(T466, T468)))
U61_AG(T412, T405, T406, T461, T465, msc38_out_aa(T420, .(T466, T468))) → U62_AG(T412, T405, T406, T461, T465, less70_in_ga(T461, T466))
U61_AG(T412, T405, T406, T461, T465, msc38_out_aa(T420, .(T466, T468))) → LESS70_IN_GA(T461, T466)
MS1_IN_AG(.(T412, .(T405, T406)), .(T461, .(T513, T517))) → U63_AG(T412, T405, T406, T461, T513, T517, splitc12_in_aaaa(T405, T406, T420, T411))
U63_AG(T412, T405, T406, T461, T513, T517, splitc12_out_aaaa(T405, T406, T420, T411)) → U64_AG(T412, T405, T406, T461, T513, T517, T420, msc25_in_aaa(T412, T411, .(T461, .(T513, T519))))
U64_AG(T412, T405, T406, T461, T513, T517, T420, msc25_out_aaa(T412, T411, .(T461, .(T513, T519)))) → U65_AG(T412, T405, T406, T461, T513, T517, T519, msc38_in_aa(T420, .(T518, T520)))
U65_AG(T412, T405, T406, T461, T513, T517, T519, msc38_out_aa(T420, .(T518, T520))) → U66_AG(T412, T405, T406, T461, T513, T517, T519, T518, T520, lessc70_in_ga(T461, T518))
U66_AG(T412, T405, T406, T461, T513, T517, T519, T518, T520, lessc70_out_ga(T461, T518)) → U67_AG(T412, T405, T406, T461, T513, T517, p179_in_gaaag(T513, T518, T519, T520, T517))
U66_AG(T412, T405, T406, T461, T513, T517, T519, T518, T520, lessc70_out_ga(T461, T518)) → P179_IN_GAAAG(T513, T518, T519, T520, T517)
P179_IN_GAAAG(T513, T518, T519, T520, T517) → U23_GAAAG(T513, T518, T519, T520, T517, less70_in_ga(T513, T518))
P179_IN_GAAAG(T513, T518, T519, T520, T517) → LESS70_IN_GA(T513, T518)
P179_IN_GAAAG(T513, T568, .(T563, T569), T570, .(T563, T567)) → U24_GAAAG(T513, T568, T563, T569, T570, T567, lessc70_in_ga(T513, T568))
U24_GAAAG(T513, T568, T563, T569, T570, T567, lessc70_out_ga(T513, T568)) → U25_GAAAG(T513, T568, T563, T569, T570, T567, p179_in_gaaag(T563, T568, T569, T570, T567))
U24_GAAAG(T513, T568, T563, T569, T570, T567, lessc70_out_ga(T513, T568)) → P179_IN_GAAAG(T563, T568, T569, T570, T567)
P179_IN_GAAAG(T513, T585, .(T588, T590), T589, .(T585, T587)) → U26_GAAAG(T513, T585, T588, T590, T589, T587, lessc70_in_gg(T513, T585))
U26_GAAAG(T513, T585, T588, T590, T589, T587, lessc70_out_gg(T513, T585)) → U27_GAAAG(T513, T585, T588, T590, T589, T587, p194_in_gaaag(T585, T588, T590, T589, T587))
U26_GAAAG(T513, T585, T588, T590, T589, T587, lessc70_out_gg(T513, T585)) → P194_IN_GAAAG(T585, T588, T590, T589, T587)
P194_IN_GAAAG(T585, T588, T590, T589, T587) → U28_GAAAG(T585, T588, T590, T589, T587, less78_in_ga(T585, T588))
P194_IN_GAAAG(T585, T588, T590, T589, T587) → LESS78_IN_GA(T585, T588)
P194_IN_GAAAG(T585, T632, T638, .(T637, T639), .(T632, T636)) → U29_GAAAG(T585, T632, T638, T637, T639, T636, lessc78_in_gg(T585, T632))
U29_GAAAG(T585, T632, T638, T637, T639, T636, lessc78_out_gg(T585, T632)) → U30_GAAAG(T585, T632, T638, T637, T639, T636, p179_in_gaaag(T632, T637, T638, T639, T636))
U29_GAAAG(T585, T632, T638, T637, T639, T636, lessc78_out_gg(T585, T632)) → P179_IN_GAAAG(T632, T637, T638, T639, T636)
P194_IN_GAAAG(T585, T657, T659, .(T654, T658), .(T654, T656)) → U31_GAAAG(T585, T657, T659, T654, T658, T656, lessc78_in_ga(T585, T657))
U31_GAAAG(T585, T657, T659, T654, T658, T656, lessc78_out_ga(T585, T657)) → U32_GAAAG(T585, T657, T659, T654, T658, T656, p194_in_gaaag(T654, T657, T659, T658, T656))
U31_GAAAG(T585, T657, T659, T654, T658, T656, lessc78_out_ga(T585, T657)) → P194_IN_GAAAG(T654, T657, T659, T658, T656)
MS1_IN_AG(.(T412, .(T405, T406)), .(T461, .(T674, T676))) → U68_AG(T412, T405, T406, T461, T674, T676, splitc12_in_aaaa(T405, T406, T420, T411))
U68_AG(T412, T405, T406, T461, T674, T676, splitc12_out_aaaa(T405, T406, T420, T411)) → U69_AG(T412, T405, T406, T461, T674, T676, T420, msc25_in_aaa(T412, T411, .(T461, .(T677, T679))))
U69_AG(T412, T405, T406, T461, T674, T676, T420, msc25_out_aaa(T412, T411, .(T461, .(T677, T679)))) → U70_AG(T412, T405, T406, T461, T674, T676, T677, T679, msc38_in_aa(T420, .(T674, T678)))
U70_AG(T412, T405, T406, T461, T674, T676, T677, T679, msc38_out_aa(T420, .(T674, T678))) → U71_AG(T412, T405, T406, T461, T674, T676, T677, T679, T678, lessc70_in_gg(T461, T674))
U71_AG(T412, T405, T406, T461, T674, T676, T677, T679, T678, lessc70_out_gg(T461, T674)) → U72_AG(T412, T405, T406, T461, T674, T676, p194_in_gaaag(T674, T677, T679, T678, T676))
U71_AG(T412, T405, T406, T461, T674, T676, T677, T679, T678, lessc70_out_gg(T461, T674)) → P194_IN_GAAAG(T674, T677, T679, T678, T676)
MS1_IN_AG(.(T412, .(T405, T406)), .(T694, T696)) → U73_AG(T412, T405, T406, T694, T696, splitc12_in_aaaa(T405, T406, T420, T411))
U73_AG(T412, T405, T406, T694, T696, splitc12_out_aaaa(T405, T406, T420, T411)) → U74_AG(T412, T405, T406, T694, T696, T420, msc25_in_aaa(T412, T411, .(T697, T699)))
U74_AG(T412, T405, T406, T694, T696, T420, msc25_out_aaa(T412, T411, .(T697, T699))) → U75_AG(T412, T405, T406, T694, T696, T697, T699, msc38_in_aa(T420, .(T694, T698)))
U75_AG(T412, T405, T406, T694, T696, T697, T699, msc38_out_aa(T420, .(T694, T698))) → U76_AG(T412, T405, T406, T694, T696, p194_in_gaaag(T694, T697, T699, T698, T696))
U75_AG(T412, T405, T406, T694, T696, T697, T699, msc38_out_aa(T420, .(T694, T698))) → P194_IN_GAAAG(T694, T697, T699, T698, T696)

The TRS R consists of the following rules:

splitc12_in_aaaa(T42, T44, .(T42, X71), X72) → U79_aaaa(T42, T44, X71, X72, splitc16_in_aaa(T44, X72, X71))
splitc16_in_aaa([], [], []) → splitc16_out_aaa([], [], [])
splitc16_in_aaa(.(T49, T51), .(T49, X89), X90) → U78_aaa(T49, T51, X89, X90, splitc16_in_aaa(T51, X90, X89))
U78_aaa(T49, T51, X89, X90, splitc16_out_aaa(T51, X90, X89)) → splitc16_out_aaa(.(T49, T51), .(T49, X89), X90)
U79_aaaa(T42, T44, X71, X72, splitc16_out_aaa(T44, X72, X71)) → splitc12_out_aaaa(T42, T44, .(T42, X71), X72)
msc38_in_aa([], []) → msc38_out_aa([], [])
msc38_in_aa(.(T89, []), .(T89, [])) → msc38_out_aa(.(T89, []), .(T89, []))
msc38_in_aa(.(T99, .(T100, T101)), X172) → U84_aa(T99, T100, T101, X172, qc34_in_aaaaaaaa(T99, T100, T101, X168, X169, X170, X171, X172))
qc34_in_aaaaaaaa(T72, T73, T74, T78, T84, T106, T105, X127) → U80_aaaaaaaa(T72, T73, T74, T78, T84, T106, T105, X127, splitc12_in_aaaa(T72, .(T73, T74), T78, T84))
U80_aaaaaaaa(T72, T73, T74, T78, T84, T106, T105, X127, splitc12_out_aaaa(T72, .(T73, T74), T78, T84)) → U81_aaaaaaaa(T72, T73, T74, T78, T84, T106, T105, X127, msc38_in_aa(T78, T106))
U81_aaaaaaaa(T72, T73, T74, T78, T84, T106, T105, X127, msc38_out_aa(T78, T106)) → U82_aaaaaaaa(T72, T73, T74, T78, T84, T106, T105, X127, msc38_in_aa(T84, T105))
U82_aaaaaaaa(T72, T73, T74, T78, T84, T106, T105, X127, msc38_out_aa(T84, T105)) → U83_aaaaaaaa(T72, T73, T74, T78, T84, T106, T105, X127, mergec54_in_aaa(T106, T105, X127))
mergec54_in_aaa([], T113, T113) → mergec54_out_aaa([], T113, T113)
mergec54_in_aaa(T118, [], T118) → mergec54_out_aaa(T118, [], T118)
mergec54_in_aaa(.(T139, T145), .(T146, T147), .(T139, X226)) → U85_aaa(T139, T145, T146, T147, X226, lessc70_in_aa(T139, T146))
lessc70_in_aa(0, T154) → lessc70_out_aa(0, T154)
lessc70_in_aa(s(T161), T162) → U91_aa(T161, T162, lessc78_in_aa(T161, T162))
lessc78_in_aa(0, s(T169)) → lessc78_out_aa(0, s(T169))
lessc78_in_aa(s(T176), s(T177)) → U89_aa(T176, T177, lessc78_in_aa(T176, T177))
U89_aa(T176, T177, lessc78_out_aa(T176, T177)) → lessc78_out_aa(s(T176), s(T177))
U91_aa(T161, T162, lessc78_out_aa(T161, T162)) → lessc70_out_aa(s(T161), T162)
U85_aaa(T139, T145, T146, T147, X226, lessc70_out_aa(T139, T146)) → U86_aaa(T139, T145, T146, T147, X226, mergec54_in_aaa(T145, .(T146, T147), X226))
mergec54_in_aaa(.(T202, T203), .(T196, T204), .(T196, X287)) → U87_aaa(T202, T203, T196, T204, X287, lessc78_in_aa(T196, T202))
U87_aaa(T202, T203, T196, T204, X287, lessc78_out_aa(T196, T202)) → U88_aaa(T202, T203, T196, T204, X287, mergec54_in_aaa(.(T202, T203), T204, X287))
U88_aaa(T202, T203, T196, T204, X287, mergec54_out_aaa(.(T202, T203), T204, X287)) → mergec54_out_aaa(.(T202, T203), .(T196, T204), .(T196, X287))
U86_aaa(T139, T145, T146, T147, X226, mergec54_out_aaa(T145, .(T146, T147), X226)) → mergec54_out_aaa(.(T139, T145), .(T146, T147), .(T139, X226))
U83_aaaaaaaa(T72, T73, T74, T78, T84, T106, T105, X127, mergec54_out_aaa(T106, T105, X127)) → qc34_out_aaaaaaaa(T72, T73, T74, T78, T84, T106, T105, X127)
U84_aa(T99, T100, T101, X172, qc34_out_aaaaaaaa(T99, T100, T101, X168, X169, X170, X171, X172)) → msc38_out_aa(.(T99, .(T100, T101)), X172)
msc25_in_aaa(T62, [], .(T62, [])) → msc25_out_aaa(T62, [], .(T62, []))
msc25_in_aaa(T72, .(T73, T74), X127) → U90_aaa(T72, T73, T74, X127, qc34_in_aaaaaaaa(T72, T73, T74, X123, X124, X125, X126, X127))
U90_aaa(T72, T73, T74, X127, qc34_out_aaaaaaaa(T72, T73, T74, X123, X124, X125, X126, X127)) → msc25_out_aaa(T72, .(T73, T74), X127)
lessc70_in_ga(0, T154) → lessc70_out_ga(0, T154)
lessc70_in_ga(s(T161), T162) → U91_ga(T161, T162, lessc78_in_ga(T161, T162))
lessc78_in_ga(0, s(T169)) → lessc78_out_ga(0, s(T169))
lessc78_in_ga(s(T176), s(T177)) → U89_ga(T176, T177, lessc78_in_ga(T176, T177))
U89_ga(T176, T177, lessc78_out_ga(T176, T177)) → lessc78_out_ga(s(T176), s(T177))
U91_ga(T161, T162, lessc78_out_ga(T161, T162)) → lessc70_out_ga(s(T161), T162)
lessc70_in_gg(0, T154) → lessc70_out_gg(0, T154)
lessc70_in_gg(s(T161), T162) → U91_gg(T161, T162, lessc78_in_gg(T161, T162))
lessc78_in_gg(0, s(T169)) → lessc78_out_gg(0, s(T169))
lessc78_in_gg(s(T176), s(T177)) → U89_gg(T176, T177, lessc78_in_gg(T176, T177))
U89_gg(T176, T177, lessc78_out_gg(T176, T177)) → lessc78_out_gg(s(T176), s(T177))
U91_gg(T161, T162, lessc78_out_gg(T161, T162)) → lessc70_out_gg(s(T161), T162)

The argument filtering Pi contains the following mapping:
[]  =  []
split12_in_aaaa(x1, x2, x3, x4)  =  split12_in_aaaa
split16_in_aaa(x1, x2, x3)  =  split16_in_aaa
splitc12_in_aaaa(x1, x2, x3, x4)  =  splitc12_in_aaaa
U79_aaaa(x1, x2, x3, x4, x5)  =  U79_aaaa(x5)
splitc16_in_aaa(x1, x2, x3)  =  splitc16_in_aaa
splitc16_out_aaa(x1, x2, x3)  =  splitc16_out_aaa
U78_aaa(x1, x2, x3, x4, x5)  =  U78_aaa(x5)
splitc12_out_aaaa(x1, x2, x3, x4)  =  splitc12_out_aaaa
ms25_in_aaa(x1, x2, x3)  =  ms25_in_aaa
p34_in_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  p34_in_aaaaaaaa
ms38_in_aa(x1, x2)  =  ms38_in_aa
msc38_in_aa(x1, x2)  =  msc38_in_aa
msc38_out_aa(x1, x2)  =  msc38_out_aa
U84_aa(x1, x2, x3, x4, x5)  =  U84_aa(x5)
qc34_in_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  qc34_in_aaaaaaaa
U80_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U80_aaaaaaaa(x9)
U81_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U81_aaaaaaaa(x9)
U82_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U82_aaaaaaaa(x9)
U83_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U83_aaaaaaaa(x9)
mergec54_in_aaa(x1, x2, x3)  =  mergec54_in_aaa
mergec54_out_aaa(x1, x2, x3)  =  mergec54_out_aaa
U85_aaa(x1, x2, x3, x4, x5, x6)  =  U85_aaa(x6)
lessc70_in_aa(x1, x2)  =  lessc70_in_aa
lessc70_out_aa(x1, x2)  =  lessc70_out_aa(x1)
U91_aa(x1, x2, x3)  =  U91_aa(x3)
lessc78_in_aa(x1, x2)  =  lessc78_in_aa
lessc78_out_aa(x1, x2)  =  lessc78_out_aa(x1)
U89_aa(x1, x2, x3)  =  U89_aa(x3)
U86_aaa(x1, x2, x3, x4, x5, x6)  =  U86_aaa(x6)
U87_aaa(x1, x2, x3, x4, x5, x6)  =  U87_aaa(x6)
U88_aaa(x1, x2, x3, x4, x5, x6)  =  U88_aaa(x6)
qc34_out_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  qc34_out_aaaaaaaa
merge54_in_aaa(x1, x2, x3)  =  merge54_in_aaa
less70_in_aa(x1, x2)  =  less70_in_aa
less78_in_aa(x1, x2)  =  less78_in_aa
msc25_in_aaa(x1, x2, x3)  =  msc25_in_aaa
msc25_out_aaa(x1, x2, x3)  =  msc25_out_aaa
U90_aaa(x1, x2, x3, x4, x5)  =  U90_aaa(x5)
.(x1, x2)  =  .(x1, x2)
less70_in_ga(x1, x2)  =  less70_in_ga(x1)
s(x1)  =  s(x1)
less78_in_ga(x1, x2)  =  less78_in_ga(x1)
lessc70_in_ga(x1, x2)  =  lessc70_in_ga(x1)
0  =  0
lessc70_out_ga(x1, x2)  =  lessc70_out_ga(x1)
U91_ga(x1, x2, x3)  =  U91_ga(x1, x3)
lessc78_in_ga(x1, x2)  =  lessc78_in_ga(x1)
lessc78_out_ga(x1, x2)  =  lessc78_out_ga(x1)
U89_ga(x1, x2, x3)  =  U89_ga(x1, x3)
p179_in_gaaag(x1, x2, x3, x4, x5)  =  p179_in_gaaag(x1, x5)
lessc70_in_gg(x1, x2)  =  lessc70_in_gg(x1, x2)
lessc70_out_gg(x1, x2)  =  lessc70_out_gg(x1, x2)
U91_gg(x1, x2, x3)  =  U91_gg(x1, x2, x3)
lessc78_in_gg(x1, x2)  =  lessc78_in_gg(x1, x2)
lessc78_out_gg(x1, x2)  =  lessc78_out_gg(x1, x2)
U89_gg(x1, x2, x3)  =  U89_gg(x1, x2, x3)
p194_in_gaaag(x1, x2, x3, x4, x5)  =  p194_in_gaaag(x1, x5)
MS1_IN_AG(x1, x2)  =  MS1_IN_AG(x2)
U33_AG(x1, x2, x3, x4)  =  U33_AG(x4)
SPLIT12_IN_AAAA(x1, x2, x3, x4)  =  SPLIT12_IN_AAAA
U2_AAAA(x1, x2, x3, x4, x5)  =  U2_AAAA(x5)
SPLIT16_IN_AAA(x1, x2, x3)  =  SPLIT16_IN_AAA
U1_AAA(x1, x2, x3, x4, x5)  =  U1_AAA(x5)
U34_AG(x1, x2, x3, x4)  =  U34_AG(x4)
U35_AG(x1, x2, x3, x4)  =  U35_AG(x4)
MS25_IN_AAA(x1, x2, x3)  =  MS25_IN_AAA
U21_AAA(x1, x2, x3, x4, x5)  =  U21_AAA(x5)
P34_IN_AAAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8)  =  P34_IN_AAAAAAAA
U3_AAAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U3_AAAAAAAA(x9)
U4_AAAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U4_AAAAAAAA(x9)
U5_AAAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U5_AAAAAAAA(x9)
MS38_IN_AA(x1, x2)  =  MS38_IN_AA
U13_AA(x1, x2, x3, x4, x5)  =  U13_AA(x5)
U6_AAAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U6_AAAAAAAA(x9)
U7_AAAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U7_AAAAAAAA(x9)
U8_AAAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U8_AAAAAAAA(x9)
U9_AAAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U9_AAAAAAAA(x9)
U10_AAAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U10_AAAAAAAA(x9)
U11_AAAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U11_AAAAAAAA(x9)
U12_AAAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U12_AAAAAAAA(x9)
MERGE54_IN_AAA(x1, x2, x3)  =  MERGE54_IN_AAA
U14_AAA(x1, x2, x3, x4, x5, x6)  =  U14_AAA(x6)
LESS70_IN_AA(x1, x2)  =  LESS70_IN_AA
U22_AA(x1, x2, x3)  =  U22_AA(x3)
LESS78_IN_AA(x1, x2)  =  LESS78_IN_AA
U20_AA(x1, x2, x3)  =  U20_AA(x3)
U15_AAA(x1, x2, x3, x4, x5, x6)  =  U15_AAA(x6)
U16_AAA(x1, x2, x3, x4, x5, x6)  =  U16_AAA(x6)
U17_AAA(x1, x2, x3, x4, x5, x6)  =  U17_AAA(x6)
U18_AAA(x1, x2, x3, x4, x5, x6)  =  U18_AAA(x6)
U19_AAA(x1, x2, x3, x4, x5, x6)  =  U19_AAA(x6)
U36_AG(x1, x2, x3, x4)  =  U36_AG(x4)
U37_AG(x1, x2, x3, x4, x5)  =  U37_AG(x5)
U38_AG(x1, x2, x3, x4)  =  U38_AG(x4)
U39_AG(x1, x2, x3, x4, x5)  =  U39_AG(x4, x5)
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, x6)  =  U43_AG(x4, x6)
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, x6)  =  U46_AG(x4, x6)
U47_AG(x1, x2, x3, x4, x5)  =  U47_AG(x4, x5)
U48_AG(x1, x2, x3, x4, x5)  =  U48_AG(x4, x5)
LESS70_IN_GA(x1, x2)  =  LESS70_IN_GA(x1)
U22_GA(x1, x2, x3)  =  U22_GA(x1, x3)
LESS78_IN_GA(x1, x2)  =  LESS78_IN_GA(x1)
U20_GA(x1, x2, x3)  =  U20_GA(x1, x3)
U49_AG(x1, x2, x3, x4, x5)  =  U49_AG(x4, x5)
U50_AG(x1, x2, x3, x4, x5, x6)  =  U50_AG(x4, x6)
U51_AG(x1, x2, x3, x4, x5, x6)  =  U51_AG(x4, x6)
U52_AG(x1, x2, x3, x4, x5)  =  U52_AG(x4, x5)
U53_AG(x1, x2, x3, x4, x5)  =  U53_AG(x4, x5)
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, x6)  =  U57_AG(x4, x6)
U58_AG(x1, x2, x3, x4, x5)  =  U58_AG(x4, x5)
U59_AG(x1, x2, x3, x4, x5, x6)  =  U59_AG(x4, x5, x6)
U60_AG(x1, x2, x3, x4, x5, x6, x7)  =  U60_AG(x4, x5, x7)
U61_AG(x1, x2, x3, x4, x5, x6)  =  U61_AG(x4, x5, x6)
U62_AG(x1, x2, x3, x4, x5, x6)  =  U62_AG(x4, x5, x6)
U63_AG(x1, x2, x3, x4, x5, x6, x7)  =  U63_AG(x4, x5, x6, x7)
U64_AG(x1, x2, x3, x4, x5, x6, x7, x8)  =  U64_AG(x4, x5, x6, x8)
U65_AG(x1, x2, x3, x4, x5, x6, x7, x8)  =  U65_AG(x4, x5, x6, x8)
U66_AG(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  U66_AG(x4, x5, x6, x10)
U67_AG(x1, x2, x3, x4, x5, x6, x7)  =  U67_AG(x4, x5, x6, x7)
P179_IN_GAAAG(x1, x2, x3, x4, x5)  =  P179_IN_GAAAG(x1, x5)
U23_GAAAG(x1, x2, x3, x4, x5, x6)  =  U23_GAAAG(x1, x5, x6)
U24_GAAAG(x1, x2, x3, x4, x5, x6, x7)  =  U24_GAAAG(x1, x3, x6, x7)
U25_GAAAG(x1, x2, x3, x4, x5, x6, x7)  =  U25_GAAAG(x1, x3, x6, x7)
U26_GAAAG(x1, x2, x3, x4, x5, x6, x7)  =  U26_GAAAG(x1, x2, x6, x7)
U27_GAAAG(x1, x2, x3, x4, x5, x6, x7)  =  U27_GAAAG(x1, x2, x6, x7)
P194_IN_GAAAG(x1, x2, x3, x4, x5)  =  P194_IN_GAAAG(x1, x5)
U28_GAAAG(x1, x2, x3, x4, x5, x6)  =  U28_GAAAG(x1, x5, x6)
U29_GAAAG(x1, x2, x3, x4, x5, x6, x7)  =  U29_GAAAG(x1, x2, x6, x7)
U30_GAAAG(x1, x2, x3, x4, x5, x6, x7)  =  U30_GAAAG(x1, x2, x6, x7)
U31_GAAAG(x1, x2, x3, x4, x5, x6, x7)  =  U31_GAAAG(x1, x4, x6, x7)
U32_GAAAG(x1, x2, x3, x4, x5, x6, x7)  =  U32_GAAAG(x1, x4, x6, x7)
U68_AG(x1, x2, x3, x4, x5, x6, x7)  =  U68_AG(x4, x5, x6, x7)
U69_AG(x1, x2, x3, x4, x5, x6, x7, x8)  =  U69_AG(x4, x5, x6, x8)
U70_AG(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U70_AG(x4, x5, x6, x9)
U71_AG(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  U71_AG(x4, x5, x6, x10)
U72_AG(x1, x2, x3, x4, x5, x6, x7)  =  U72_AG(x4, x5, x6, x7)
U73_AG(x1, x2, x3, x4, x5, x6)  =  U73_AG(x4, x5, x6)
U74_AG(x1, x2, x3, x4, x5, x6, x7)  =  U74_AG(x4, x5, x7)
U75_AG(x1, x2, x3, x4, x5, x6, x7, x8)  =  U75_AG(x4, x5, x8)
U76_AG(x1, x2, x3, x4, x5, x6)  =  U76_AG(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:

MS1_IN_AG(.(T29, .(T27, T28)), []) → U33_AG(T29, T27, T28, split12_in_aaaa(T27, T28, X42, X41))
MS1_IN_AG(.(T29, .(T27, T28)), []) → SPLIT12_IN_AAAA(T27, T28, X42, X41)
SPLIT12_IN_AAAA(T42, T44, .(T42, X71), X72) → U2_AAAA(T42, T44, X71, X72, split16_in_aaa(T44, X72, X71))
SPLIT12_IN_AAAA(T42, T44, .(T42, X71), X72) → SPLIT16_IN_AAA(T44, X72, X71)
SPLIT16_IN_AAA(.(T49, T51), .(T49, X89), X90) → U1_AAA(T49, T51, X89, X90, split16_in_aaa(T51, X90, X89))
SPLIT16_IN_AAA(.(T49, T51), .(T49, X89), X90) → SPLIT16_IN_AAA(T51, X90, X89)
MS1_IN_AG(.(T34, .(T27, T28)), []) → U34_AG(T34, T27, T28, splitc12_in_aaaa(T27, T28, T32, T33))
U34_AG(T34, T27, T28, splitc12_out_aaaa(T27, T28, T32, T33)) → U35_AG(T34, T27, T28, ms25_in_aaa(T34, T33, X13))
U34_AG(T34, T27, T28, splitc12_out_aaaa(T27, T28, T32, T33)) → MS25_IN_AAA(T34, T33, X13)
MS25_IN_AAA(T72, .(T73, T74), X127) → U21_AAA(T72, T73, T74, X127, p34_in_aaaaaaaa(T72, T73, T74, X123, X124, X125, X126, X127))
MS25_IN_AAA(T72, .(T73, T74), X127) → P34_IN_AAAAAAAA(T72, T73, T74, X123, X124, X125, X126, X127)
P34_IN_AAAAAAAA(T72, T73, T74, X123, X124, X125, X126, X127) → U3_AAAAAAAA(T72, T73, T74, X123, X124, X125, X126, X127, split12_in_aaaa(T72, .(T73, T74), X123, X124))
P34_IN_AAAAAAAA(T72, T73, T74, X123, X124, X125, X126, X127) → SPLIT12_IN_AAAA(T72, .(T73, T74), X123, X124)
P34_IN_AAAAAAAA(T72, T73, T74, T78, T79, X125, X126, X127) → U4_AAAAAAAA(T72, T73, T74, T78, T79, X125, X126, X127, splitc12_in_aaaa(T72, .(T73, T74), T78, T79))
U4_AAAAAAAA(T72, T73, T74, T78, T79, X125, X126, X127, splitc12_out_aaaa(T72, .(T73, T74), T78, T79)) → U5_AAAAAAAA(T72, T73, T74, T78, T79, X125, X126, X127, ms38_in_aa(T78, X125))
U4_AAAAAAAA(T72, T73, T74, T78, T79, X125, X126, X127, splitc12_out_aaaa(T72, .(T73, T74), T78, T79)) → MS38_IN_AA(T78, X125)
MS38_IN_AA(.(T99, .(T100, T101)), X172) → U13_AA(T99, T100, T101, X172, p34_in_aaaaaaaa(T99, T100, T101, X168, X169, X170, X171, X172))
MS38_IN_AA(.(T99, .(T100, T101)), X172) → P34_IN_AAAAAAAA(T99, T100, T101, X168, X169, X170, X171, X172)
P34_IN_AAAAAAAA(T72, T73, T74, T78, T84, T83, X126, X127) → U6_AAAAAAAA(T72, T73, T74, T78, T84, T83, X126, X127, splitc12_in_aaaa(T72, .(T73, T74), T78, T84))
U6_AAAAAAAA(T72, T73, T74, T78, T84, T83, X126, X127, splitc12_out_aaaa(T72, .(T73, T74), T78, T84)) → U7_AAAAAAAA(T72, T73, T74, T78, T84, T83, X126, X127, msc38_in_aa(T78, T83))
U7_AAAAAAAA(T72, T73, T74, T78, T84, T83, X126, X127, msc38_out_aa(T78, T83)) → U8_AAAAAAAA(T72, T73, T74, T78, T84, T83, X126, X127, ms38_in_aa(T84, X126))
U7_AAAAAAAA(T72, T73, T74, T78, T84, T83, X126, X127, msc38_out_aa(T78, T83)) → MS38_IN_AA(T84, X126)
P34_IN_AAAAAAAA(T72, T73, T74, T78, T84, T106, T105, X127) → U9_AAAAAAAA(T72, T73, T74, T78, T84, T106, T105, X127, splitc12_in_aaaa(T72, .(T73, T74), T78, T84))
U9_AAAAAAAA(T72, T73, T74, T78, T84, T106, T105, X127, splitc12_out_aaaa(T72, .(T73, T74), T78, T84)) → U10_AAAAAAAA(T72, T73, T74, T78, T84, T106, T105, X127, msc38_in_aa(T78, T106))
U10_AAAAAAAA(T72, T73, T74, T78, T84, T106, T105, X127, msc38_out_aa(T78, T106)) → U11_AAAAAAAA(T72, T73, T74, T78, T84, T106, T105, X127, msc38_in_aa(T84, T105))
U11_AAAAAAAA(T72, T73, T74, T78, T84, T106, T105, X127, msc38_out_aa(T84, T105)) → U12_AAAAAAAA(T72, T73, T74, T78, T84, T106, T105, X127, merge54_in_aaa(T106, T105, X127))
U11_AAAAAAAA(T72, T73, T74, T78, T84, T106, T105, X127, msc38_out_aa(T84, T105)) → MERGE54_IN_AAA(T106, T105, X127)
MERGE54_IN_AAA(.(T139, T141), .(T140, T142), .(T139, X226)) → U14_AAA(T139, T141, T140, T142, X226, less70_in_aa(T139, T140))
MERGE54_IN_AAA(.(T139, T141), .(T140, T142), .(T139, X226)) → LESS70_IN_AA(T139, T140)
LESS70_IN_AA(s(T161), T162) → U22_AA(T161, T162, less78_in_aa(T161, T162))
LESS70_IN_AA(s(T161), T162) → LESS78_IN_AA(T161, T162)
LESS78_IN_AA(s(T176), s(T177)) → U20_AA(T176, T177, less78_in_aa(T176, T177))
LESS78_IN_AA(s(T176), s(T177)) → LESS78_IN_AA(T176, T177)
MERGE54_IN_AAA(.(T139, T145), .(T146, T147), .(T139, X226)) → U15_AAA(T139, T145, T146, T147, X226, lessc70_in_aa(T139, T146))
U15_AAA(T139, T145, T146, T147, X226, lessc70_out_aa(T139, T146)) → U16_AAA(T139, T145, T146, T147, X226, merge54_in_aaa(T145, .(T146, T147), X226))
U15_AAA(T139, T145, T146, T147, X226, lessc70_out_aa(T139, T146)) → MERGE54_IN_AAA(T145, .(T146, T147), X226)
MERGE54_IN_AAA(.(T197, T199), .(T196, T198), .(T196, X287)) → U17_AAA(T197, T199, T196, T198, X287, less78_in_aa(T196, T197))
MERGE54_IN_AAA(.(T197, T199), .(T196, T198), .(T196, X287)) → LESS78_IN_AA(T196, T197)
MERGE54_IN_AAA(.(T202, T203), .(T196, T204), .(T196, X287)) → U18_AAA(T202, T203, T196, T204, X287, lessc78_in_aa(T196, T202))
U18_AAA(T202, T203, T196, T204, X287, lessc78_out_aa(T196, T202)) → U19_AAA(T202, T203, T196, T204, X287, merge54_in_aaa(.(T202, T203), T204, X287))
U18_AAA(T202, T203, T196, T204, X287, lessc78_out_aa(T196, T202)) → MERGE54_IN_AAA(.(T202, T203), T204, X287)
MS1_IN_AG(.(T34, .(T27, T28)), []) → U36_AG(T34, T27, T28, splitc12_in_aaaa(T27, T28, T55, T33))
U36_AG(T34, T27, T28, splitc12_out_aaaa(T27, T28, T55, T33)) → U37_AG(T34, T27, T28, T55, msc25_in_aaa(T34, T33, T54))
U37_AG(T34, T27, T28, T55, msc25_out_aaa(T34, T33, T54)) → U38_AG(T34, T27, T28, ms38_in_aa(T55, X14))
U37_AG(T34, T27, T28, T55, msc25_out_aaa(T34, T33, T54)) → MS38_IN_AA(T55, X14)
MS1_IN_AG(.(T262, .(T260, T261)), .(T242, [])) → U39_AG(T262, T260, T261, T242, split12_in_aaaa(T260, T261, X367, X366))
MS1_IN_AG(.(T262, .(T260, T261)), .(T242, [])) → SPLIT12_IN_AAAA(T260, T261, X367, X366)
MS1_IN_AG(.(T267, .(T260, T261)), .(T242, [])) → U40_AG(T267, T260, T261, T242, splitc12_in_aaaa(T260, T261, T265, T266))
U40_AG(T267, T260, T261, T242, splitc12_out_aaaa(T260, T261, T265, T266)) → U41_AG(T267, T260, T261, T242, ms25_in_aaa(T267, T266, X338))
U40_AG(T267, T260, T261, T242, splitc12_out_aaaa(T260, T261, T265, T266)) → MS25_IN_AAA(T267, T266, X338)
MS1_IN_AG(.(T267, .(T260, T261)), .(T242, [])) → U42_AG(T267, T260, T261, T242, splitc12_in_aaaa(T260, T261, T273, T266))
U42_AG(T267, T260, T261, T242, splitc12_out_aaaa(T260, T261, T273, T266)) → U43_AG(T267, T260, T261, T242, T273, msc25_in_aaa(T267, T266, T272))
U43_AG(T267, T260, T261, T242, T273, msc25_out_aaa(T267, T266, T272)) → U44_AG(T267, T260, T261, T242, ms38_in_aa(T273, X339))
U43_AG(T267, T260, T261, T242, T273, msc25_out_aaa(T267, T266, T272)) → MS38_IN_AA(T273, X339)
MS1_IN_AG(.(T267, .(T260, T261)), .(T318, [])) → U45_AG(T267, T260, T261, T318, splitc12_in_aaaa(T260, T261, T273, T266))
U45_AG(T267, T260, T261, T318, splitc12_out_aaaa(T260, T261, T273, T266)) → U46_AG(T267, T260, T261, T318, T273, msc25_in_aaa(T267, T266, .(T318, T323)))
U46_AG(T267, T260, T261, T318, T273, msc25_out_aaa(T267, T266, .(T318, T323))) → U47_AG(T267, T260, T261, T318, msc38_in_aa(T273, .(T322, T324)))
U47_AG(T267, T260, T261, T318, msc38_out_aa(T273, .(T322, T324))) → U48_AG(T267, T260, T261, T318, less70_in_ga(T318, T322))
U47_AG(T267, T260, T261, T318, msc38_out_aa(T273, .(T322, T324))) → LESS70_IN_GA(T318, T322)
LESS70_IN_GA(s(T161), T162) → U22_GA(T161, T162, less78_in_ga(T161, T162))
LESS70_IN_GA(s(T161), T162) → LESS78_IN_GA(T161, T162)
LESS78_IN_GA(s(T176), s(T177)) → U20_GA(T176, T177, less78_in_ga(T176, T177))
LESS78_IN_GA(s(T176), s(T177)) → LESS78_IN_GA(T176, T177)
MS1_IN_AG(.(T267, .(T260, T261)), .(T356, [])) → U49_AG(T267, T260, T261, T356, splitc12_in_aaaa(T260, T261, T273, T266))
U49_AG(T267, T260, T261, T356, splitc12_out_aaaa(T260, T261, T273, T266)) → U50_AG(T267, T260, T261, T356, T273, msc25_in_aaa(T267, T266, .(T358, T360)))
U50_AG(T267, T260, T261, T356, T273, msc25_out_aaa(T267, T266, .(T358, T360))) → U51_AG(T267, T260, T261, T356, T358, msc38_in_aa(T273, .(T356, T359)))
U51_AG(T267, T260, T261, T356, T358, msc38_out_aa(T273, .(T356, T359))) → U52_AG(T267, T260, T261, T356, less78_in_ga(T356, T358))
U51_AG(T267, T260, T261, T356, T358, msc38_out_aa(T273, .(T356, T359))) → LESS78_IN_GA(T356, T358)
MS1_IN_AG(.(T407, .(T405, T406)), T387) → U53_AG(T407, T405, T406, T387, split12_in_aaaa(T405, T406, X523, X522))
MS1_IN_AG(.(T407, .(T405, T406)), T387) → SPLIT12_IN_AAAA(T405, T406, X523, X522)
MS1_IN_AG(.(T412, .(T405, T406)), T387) → U54_AG(T412, T405, T406, T387, splitc12_in_aaaa(T405, T406, T410, T411))
U54_AG(T412, T405, T406, T387, splitc12_out_aaaa(T405, T406, T410, T411)) → U55_AG(T412, T405, T406, T387, ms25_in_aaa(T412, T411, X494))
U54_AG(T412, T405, T406, T387, splitc12_out_aaaa(T405, T406, T410, T411)) → MS25_IN_AAA(T412, T411, X494)
MS1_IN_AG(.(T412, .(T405, T406)), T387) → U56_AG(T412, T405, T406, T387, splitc12_in_aaaa(T405, T406, T420, T411))
U56_AG(T412, T405, T406, T387, splitc12_out_aaaa(T405, T406, T420, T411)) → U57_AG(T412, T405, T406, T387, T420, msc25_in_aaa(T412, T411, T419))
U57_AG(T412, T405, T406, T387, T420, msc25_out_aaa(T412, T411, T419)) → U58_AG(T412, T405, T406, T387, ms38_in_aa(T420, X495))
U57_AG(T412, T405, T406, T387, T420, msc25_out_aaa(T412, T411, T419)) → MS38_IN_AA(T420, X495)
MS1_IN_AG(.(T412, .(T405, T406)), .(T461, T465)) → U59_AG(T412, T405, T406, T461, T465, splitc12_in_aaaa(T405, T406, T420, T411))
U59_AG(T412, T405, T406, T461, T465, splitc12_out_aaaa(T405, T406, T420, T411)) → U60_AG(T412, T405, T406, T461, T465, T420, msc25_in_aaa(T412, T411, .(T461, T467)))
U60_AG(T412, T405, T406, T461, T465, T420, msc25_out_aaa(T412, T411, .(T461, T467))) → U61_AG(T412, T405, T406, T461, T465, msc38_in_aa(T420, .(T466, T468)))
U61_AG(T412, T405, T406, T461, T465, msc38_out_aa(T420, .(T466, T468))) → U62_AG(T412, T405, T406, T461, T465, less70_in_ga(T461, T466))
U61_AG(T412, T405, T406, T461, T465, msc38_out_aa(T420, .(T466, T468))) → LESS70_IN_GA(T461, T466)
MS1_IN_AG(.(T412, .(T405, T406)), .(T461, .(T513, T517))) → U63_AG(T412, T405, T406, T461, T513, T517, splitc12_in_aaaa(T405, T406, T420, T411))
U63_AG(T412, T405, T406, T461, T513, T517, splitc12_out_aaaa(T405, T406, T420, T411)) → U64_AG(T412, T405, T406, T461, T513, T517, T420, msc25_in_aaa(T412, T411, .(T461, .(T513, T519))))
U64_AG(T412, T405, T406, T461, T513, T517, T420, msc25_out_aaa(T412, T411, .(T461, .(T513, T519)))) → U65_AG(T412, T405, T406, T461, T513, T517, T519, msc38_in_aa(T420, .(T518, T520)))
U65_AG(T412, T405, T406, T461, T513, T517, T519, msc38_out_aa(T420, .(T518, T520))) → U66_AG(T412, T405, T406, T461, T513, T517, T519, T518, T520, lessc70_in_ga(T461, T518))
U66_AG(T412, T405, T406, T461, T513, T517, T519, T518, T520, lessc70_out_ga(T461, T518)) → U67_AG(T412, T405, T406, T461, T513, T517, p179_in_gaaag(T513, T518, T519, T520, T517))
U66_AG(T412, T405, T406, T461, T513, T517, T519, T518, T520, lessc70_out_ga(T461, T518)) → P179_IN_GAAAG(T513, T518, T519, T520, T517)
P179_IN_GAAAG(T513, T518, T519, T520, T517) → U23_GAAAG(T513, T518, T519, T520, T517, less70_in_ga(T513, T518))
P179_IN_GAAAG(T513, T518, T519, T520, T517) → LESS70_IN_GA(T513, T518)
P179_IN_GAAAG(T513, T568, .(T563, T569), T570, .(T563, T567)) → U24_GAAAG(T513, T568, T563, T569, T570, T567, lessc70_in_ga(T513, T568))
U24_GAAAG(T513, T568, T563, T569, T570, T567, lessc70_out_ga(T513, T568)) → U25_GAAAG(T513, T568, T563, T569, T570, T567, p179_in_gaaag(T563, T568, T569, T570, T567))
U24_GAAAG(T513, T568, T563, T569, T570, T567, lessc70_out_ga(T513, T568)) → P179_IN_GAAAG(T563, T568, T569, T570, T567)
P179_IN_GAAAG(T513, T585, .(T588, T590), T589, .(T585, T587)) → U26_GAAAG(T513, T585, T588, T590, T589, T587, lessc70_in_gg(T513, T585))
U26_GAAAG(T513, T585, T588, T590, T589, T587, lessc70_out_gg(T513, T585)) → U27_GAAAG(T513, T585, T588, T590, T589, T587, p194_in_gaaag(T585, T588, T590, T589, T587))
U26_GAAAG(T513, T585, T588, T590, T589, T587, lessc70_out_gg(T513, T585)) → P194_IN_GAAAG(T585, T588, T590, T589, T587)
P194_IN_GAAAG(T585, T588, T590, T589, T587) → U28_GAAAG(T585, T588, T590, T589, T587, less78_in_ga(T585, T588))
P194_IN_GAAAG(T585, T588, T590, T589, T587) → LESS78_IN_GA(T585, T588)
P194_IN_GAAAG(T585, T632, T638, .(T637, T639), .(T632, T636)) → U29_GAAAG(T585, T632, T638, T637, T639, T636, lessc78_in_gg(T585, T632))
U29_GAAAG(T585, T632, T638, T637, T639, T636, lessc78_out_gg(T585, T632)) → U30_GAAAG(T585, T632, T638, T637, T639, T636, p179_in_gaaag(T632, T637, T638, T639, T636))
U29_GAAAG(T585, T632, T638, T637, T639, T636, lessc78_out_gg(T585, T632)) → P179_IN_GAAAG(T632, T637, T638, T639, T636)
P194_IN_GAAAG(T585, T657, T659, .(T654, T658), .(T654, T656)) → U31_GAAAG(T585, T657, T659, T654, T658, T656, lessc78_in_ga(T585, T657))
U31_GAAAG(T585, T657, T659, T654, T658, T656, lessc78_out_ga(T585, T657)) → U32_GAAAG(T585, T657, T659, T654, T658, T656, p194_in_gaaag(T654, T657, T659, T658, T656))
U31_GAAAG(T585, T657, T659, T654, T658, T656, lessc78_out_ga(T585, T657)) → P194_IN_GAAAG(T654, T657, T659, T658, T656)
MS1_IN_AG(.(T412, .(T405, T406)), .(T461, .(T674, T676))) → U68_AG(T412, T405, T406, T461, T674, T676, splitc12_in_aaaa(T405, T406, T420, T411))
U68_AG(T412, T405, T406, T461, T674, T676, splitc12_out_aaaa(T405, T406, T420, T411)) → U69_AG(T412, T405, T406, T461, T674, T676, T420, msc25_in_aaa(T412, T411, .(T461, .(T677, T679))))
U69_AG(T412, T405, T406, T461, T674, T676, T420, msc25_out_aaa(T412, T411, .(T461, .(T677, T679)))) → U70_AG(T412, T405, T406, T461, T674, T676, T677, T679, msc38_in_aa(T420, .(T674, T678)))
U70_AG(T412, T405, T406, T461, T674, T676, T677, T679, msc38_out_aa(T420, .(T674, T678))) → U71_AG(T412, T405, T406, T461, T674, T676, T677, T679, T678, lessc70_in_gg(T461, T674))
U71_AG(T412, T405, T406, T461, T674, T676, T677, T679, T678, lessc70_out_gg(T461, T674)) → U72_AG(T412, T405, T406, T461, T674, T676, p194_in_gaaag(T674, T677, T679, T678, T676))
U71_AG(T412, T405, T406, T461, T674, T676, T677, T679, T678, lessc70_out_gg(T461, T674)) → P194_IN_GAAAG(T674, T677, T679, T678, T676)
MS1_IN_AG(.(T412, .(T405, T406)), .(T694, T696)) → U73_AG(T412, T405, T406, T694, T696, splitc12_in_aaaa(T405, T406, T420, T411))
U73_AG(T412, T405, T406, T694, T696, splitc12_out_aaaa(T405, T406, T420, T411)) → U74_AG(T412, T405, T406, T694, T696, T420, msc25_in_aaa(T412, T411, .(T697, T699)))
U74_AG(T412, T405, T406, T694, T696, T420, msc25_out_aaa(T412, T411, .(T697, T699))) → U75_AG(T412, T405, T406, T694, T696, T697, T699, msc38_in_aa(T420, .(T694, T698)))
U75_AG(T412, T405, T406, T694, T696, T697, T699, msc38_out_aa(T420, .(T694, T698))) → U76_AG(T412, T405, T406, T694, T696, p194_in_gaaag(T694, T697, T699, T698, T696))
U75_AG(T412, T405, T406, T694, T696, T697, T699, msc38_out_aa(T420, .(T694, T698))) → P194_IN_GAAAG(T694, T697, T699, T698, T696)

The TRS R consists of the following rules:

splitc12_in_aaaa(T42, T44, .(T42, X71), X72) → U79_aaaa(T42, T44, X71, X72, splitc16_in_aaa(T44, X72, X71))
splitc16_in_aaa([], [], []) → splitc16_out_aaa([], [], [])
splitc16_in_aaa(.(T49, T51), .(T49, X89), X90) → U78_aaa(T49, T51, X89, X90, splitc16_in_aaa(T51, X90, X89))
U78_aaa(T49, T51, X89, X90, splitc16_out_aaa(T51, X90, X89)) → splitc16_out_aaa(.(T49, T51), .(T49, X89), X90)
U79_aaaa(T42, T44, X71, X72, splitc16_out_aaa(T44, X72, X71)) → splitc12_out_aaaa(T42, T44, .(T42, X71), X72)
msc38_in_aa([], []) → msc38_out_aa([], [])
msc38_in_aa(.(T89, []), .(T89, [])) → msc38_out_aa(.(T89, []), .(T89, []))
msc38_in_aa(.(T99, .(T100, T101)), X172) → U84_aa(T99, T100, T101, X172, qc34_in_aaaaaaaa(T99, T100, T101, X168, X169, X170, X171, X172))
qc34_in_aaaaaaaa(T72, T73, T74, T78, T84, T106, T105, X127) → U80_aaaaaaaa(T72, T73, T74, T78, T84, T106, T105, X127, splitc12_in_aaaa(T72, .(T73, T74), T78, T84))
U80_aaaaaaaa(T72, T73, T74, T78, T84, T106, T105, X127, splitc12_out_aaaa(T72, .(T73, T74), T78, T84)) → U81_aaaaaaaa(T72, T73, T74, T78, T84, T106, T105, X127, msc38_in_aa(T78, T106))
U81_aaaaaaaa(T72, T73, T74, T78, T84, T106, T105, X127, msc38_out_aa(T78, T106)) → U82_aaaaaaaa(T72, T73, T74, T78, T84, T106, T105, X127, msc38_in_aa(T84, T105))
U82_aaaaaaaa(T72, T73, T74, T78, T84, T106, T105, X127, msc38_out_aa(T84, T105)) → U83_aaaaaaaa(T72, T73, T74, T78, T84, T106, T105, X127, mergec54_in_aaa(T106, T105, X127))
mergec54_in_aaa([], T113, T113) → mergec54_out_aaa([], T113, T113)
mergec54_in_aaa(T118, [], T118) → mergec54_out_aaa(T118, [], T118)
mergec54_in_aaa(.(T139, T145), .(T146, T147), .(T139, X226)) → U85_aaa(T139, T145, T146, T147, X226, lessc70_in_aa(T139, T146))
lessc70_in_aa(0, T154) → lessc70_out_aa(0, T154)
lessc70_in_aa(s(T161), T162) → U91_aa(T161, T162, lessc78_in_aa(T161, T162))
lessc78_in_aa(0, s(T169)) → lessc78_out_aa(0, s(T169))
lessc78_in_aa(s(T176), s(T177)) → U89_aa(T176, T177, lessc78_in_aa(T176, T177))
U89_aa(T176, T177, lessc78_out_aa(T176, T177)) → lessc78_out_aa(s(T176), s(T177))
U91_aa(T161, T162, lessc78_out_aa(T161, T162)) → lessc70_out_aa(s(T161), T162)
U85_aaa(T139, T145, T146, T147, X226, lessc70_out_aa(T139, T146)) → U86_aaa(T139, T145, T146, T147, X226, mergec54_in_aaa(T145, .(T146, T147), X226))
mergec54_in_aaa(.(T202, T203), .(T196, T204), .(T196, X287)) → U87_aaa(T202, T203, T196, T204, X287, lessc78_in_aa(T196, T202))
U87_aaa(T202, T203, T196, T204, X287, lessc78_out_aa(T196, T202)) → U88_aaa(T202, T203, T196, T204, X287, mergec54_in_aaa(.(T202, T203), T204, X287))
U88_aaa(T202, T203, T196, T204, X287, mergec54_out_aaa(.(T202, T203), T204, X287)) → mergec54_out_aaa(.(T202, T203), .(T196, T204), .(T196, X287))
U86_aaa(T139, T145, T146, T147, X226, mergec54_out_aaa(T145, .(T146, T147), X226)) → mergec54_out_aaa(.(T139, T145), .(T146, T147), .(T139, X226))
U83_aaaaaaaa(T72, T73, T74, T78, T84, T106, T105, X127, mergec54_out_aaa(T106, T105, X127)) → qc34_out_aaaaaaaa(T72, T73, T74, T78, T84, T106, T105, X127)
U84_aa(T99, T100, T101, X172, qc34_out_aaaaaaaa(T99, T100, T101, X168, X169, X170, X171, X172)) → msc38_out_aa(.(T99, .(T100, T101)), X172)
msc25_in_aaa(T62, [], .(T62, [])) → msc25_out_aaa(T62, [], .(T62, []))
msc25_in_aaa(T72, .(T73, T74), X127) → U90_aaa(T72, T73, T74, X127, qc34_in_aaaaaaaa(T72, T73, T74, X123, X124, X125, X126, X127))
U90_aaa(T72, T73, T74, X127, qc34_out_aaaaaaaa(T72, T73, T74, X123, X124, X125, X126, X127)) → msc25_out_aaa(T72, .(T73, T74), X127)
lessc70_in_ga(0, T154) → lessc70_out_ga(0, T154)
lessc70_in_ga(s(T161), T162) → U91_ga(T161, T162, lessc78_in_ga(T161, T162))
lessc78_in_ga(0, s(T169)) → lessc78_out_ga(0, s(T169))
lessc78_in_ga(s(T176), s(T177)) → U89_ga(T176, T177, lessc78_in_ga(T176, T177))
U89_ga(T176, T177, lessc78_out_ga(T176, T177)) → lessc78_out_ga(s(T176), s(T177))
U91_ga(T161, T162, lessc78_out_ga(T161, T162)) → lessc70_out_ga(s(T161), T162)
lessc70_in_gg(0, T154) → lessc70_out_gg(0, T154)
lessc70_in_gg(s(T161), T162) → U91_gg(T161, T162, lessc78_in_gg(T161, T162))
lessc78_in_gg(0, s(T169)) → lessc78_out_gg(0, s(T169))
lessc78_in_gg(s(T176), s(T177)) → U89_gg(T176, T177, lessc78_in_gg(T176, T177))
U89_gg(T176, T177, lessc78_out_gg(T176, T177)) → lessc78_out_gg(s(T176), s(T177))
U91_gg(T161, T162, lessc78_out_gg(T161, T162)) → lessc70_out_gg(s(T161), T162)

The argument filtering Pi contains the following mapping:
[]  =  []
split12_in_aaaa(x1, x2, x3, x4)  =  split12_in_aaaa
split16_in_aaa(x1, x2, x3)  =  split16_in_aaa
splitc12_in_aaaa(x1, x2, x3, x4)  =  splitc12_in_aaaa
U79_aaaa(x1, x2, x3, x4, x5)  =  U79_aaaa(x5)
splitc16_in_aaa(x1, x2, x3)  =  splitc16_in_aaa
splitc16_out_aaa(x1, x2, x3)  =  splitc16_out_aaa
U78_aaa(x1, x2, x3, x4, x5)  =  U78_aaa(x5)
splitc12_out_aaaa(x1, x2, x3, x4)  =  splitc12_out_aaaa
ms25_in_aaa(x1, x2, x3)  =  ms25_in_aaa
p34_in_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  p34_in_aaaaaaaa
ms38_in_aa(x1, x2)  =  ms38_in_aa
msc38_in_aa(x1, x2)  =  msc38_in_aa
msc38_out_aa(x1, x2)  =  msc38_out_aa
U84_aa(x1, x2, x3, x4, x5)  =  U84_aa(x5)
qc34_in_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  qc34_in_aaaaaaaa
U80_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U80_aaaaaaaa(x9)
U81_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U81_aaaaaaaa(x9)
U82_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U82_aaaaaaaa(x9)
U83_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U83_aaaaaaaa(x9)
mergec54_in_aaa(x1, x2, x3)  =  mergec54_in_aaa
mergec54_out_aaa(x1, x2, x3)  =  mergec54_out_aaa
U85_aaa(x1, x2, x3, x4, x5, x6)  =  U85_aaa(x6)
lessc70_in_aa(x1, x2)  =  lessc70_in_aa
lessc70_out_aa(x1, x2)  =  lessc70_out_aa(x1)
U91_aa(x1, x2, x3)  =  U91_aa(x3)
lessc78_in_aa(x1, x2)  =  lessc78_in_aa
lessc78_out_aa(x1, x2)  =  lessc78_out_aa(x1)
U89_aa(x1, x2, x3)  =  U89_aa(x3)
U86_aaa(x1, x2, x3, x4, x5, x6)  =  U86_aaa(x6)
U87_aaa(x1, x2, x3, x4, x5, x6)  =  U87_aaa(x6)
U88_aaa(x1, x2, x3, x4, x5, x6)  =  U88_aaa(x6)
qc34_out_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  qc34_out_aaaaaaaa
merge54_in_aaa(x1, x2, x3)  =  merge54_in_aaa
less70_in_aa(x1, x2)  =  less70_in_aa
less78_in_aa(x1, x2)  =  less78_in_aa
msc25_in_aaa(x1, x2, x3)  =  msc25_in_aaa
msc25_out_aaa(x1, x2, x3)  =  msc25_out_aaa
U90_aaa(x1, x2, x3, x4, x5)  =  U90_aaa(x5)
.(x1, x2)  =  .(x1, x2)
less70_in_ga(x1, x2)  =  less70_in_ga(x1)
s(x1)  =  s(x1)
less78_in_ga(x1, x2)  =  less78_in_ga(x1)
lessc70_in_ga(x1, x2)  =  lessc70_in_ga(x1)
0  =  0
lessc70_out_ga(x1, x2)  =  lessc70_out_ga(x1)
U91_ga(x1, x2, x3)  =  U91_ga(x1, x3)
lessc78_in_ga(x1, x2)  =  lessc78_in_ga(x1)
lessc78_out_ga(x1, x2)  =  lessc78_out_ga(x1)
U89_ga(x1, x2, x3)  =  U89_ga(x1, x3)
p179_in_gaaag(x1, x2, x3, x4, x5)  =  p179_in_gaaag(x1, x5)
lessc70_in_gg(x1, x2)  =  lessc70_in_gg(x1, x2)
lessc70_out_gg(x1, x2)  =  lessc70_out_gg(x1, x2)
U91_gg(x1, x2, x3)  =  U91_gg(x1, x2, x3)
lessc78_in_gg(x1, x2)  =  lessc78_in_gg(x1, x2)
lessc78_out_gg(x1, x2)  =  lessc78_out_gg(x1, x2)
U89_gg(x1, x2, x3)  =  U89_gg(x1, x2, x3)
p194_in_gaaag(x1, x2, x3, x4, x5)  =  p194_in_gaaag(x1, x5)
MS1_IN_AG(x1, x2)  =  MS1_IN_AG(x2)
U33_AG(x1, x2, x3, x4)  =  U33_AG(x4)
SPLIT12_IN_AAAA(x1, x2, x3, x4)  =  SPLIT12_IN_AAAA
U2_AAAA(x1, x2, x3, x4, x5)  =  U2_AAAA(x5)
SPLIT16_IN_AAA(x1, x2, x3)  =  SPLIT16_IN_AAA
U1_AAA(x1, x2, x3, x4, x5)  =  U1_AAA(x5)
U34_AG(x1, x2, x3, x4)  =  U34_AG(x4)
U35_AG(x1, x2, x3, x4)  =  U35_AG(x4)
MS25_IN_AAA(x1, x2, x3)  =  MS25_IN_AAA
U21_AAA(x1, x2, x3, x4, x5)  =  U21_AAA(x5)
P34_IN_AAAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8)  =  P34_IN_AAAAAAAA
U3_AAAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U3_AAAAAAAA(x9)
U4_AAAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U4_AAAAAAAA(x9)
U5_AAAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U5_AAAAAAAA(x9)
MS38_IN_AA(x1, x2)  =  MS38_IN_AA
U13_AA(x1, x2, x3, x4, x5)  =  U13_AA(x5)
U6_AAAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U6_AAAAAAAA(x9)
U7_AAAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U7_AAAAAAAA(x9)
U8_AAAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U8_AAAAAAAA(x9)
U9_AAAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U9_AAAAAAAA(x9)
U10_AAAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U10_AAAAAAAA(x9)
U11_AAAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U11_AAAAAAAA(x9)
U12_AAAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U12_AAAAAAAA(x9)
MERGE54_IN_AAA(x1, x2, x3)  =  MERGE54_IN_AAA
U14_AAA(x1, x2, x3, x4, x5, x6)  =  U14_AAA(x6)
LESS70_IN_AA(x1, x2)  =  LESS70_IN_AA
U22_AA(x1, x2, x3)  =  U22_AA(x3)
LESS78_IN_AA(x1, x2)  =  LESS78_IN_AA
U20_AA(x1, x2, x3)  =  U20_AA(x3)
U15_AAA(x1, x2, x3, x4, x5, x6)  =  U15_AAA(x6)
U16_AAA(x1, x2, x3, x4, x5, x6)  =  U16_AAA(x6)
U17_AAA(x1, x2, x3, x4, x5, x6)  =  U17_AAA(x6)
U18_AAA(x1, x2, x3, x4, x5, x6)  =  U18_AAA(x6)
U19_AAA(x1, x2, x3, x4, x5, x6)  =  U19_AAA(x6)
U36_AG(x1, x2, x3, x4)  =  U36_AG(x4)
U37_AG(x1, x2, x3, x4, x5)  =  U37_AG(x5)
U38_AG(x1, x2, x3, x4)  =  U38_AG(x4)
U39_AG(x1, x2, x3, x4, x5)  =  U39_AG(x4, x5)
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, x6)  =  U43_AG(x4, x6)
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, x6)  =  U46_AG(x4, x6)
U47_AG(x1, x2, x3, x4, x5)  =  U47_AG(x4, x5)
U48_AG(x1, x2, x3, x4, x5)  =  U48_AG(x4, x5)
LESS70_IN_GA(x1, x2)  =  LESS70_IN_GA(x1)
U22_GA(x1, x2, x3)  =  U22_GA(x1, x3)
LESS78_IN_GA(x1, x2)  =  LESS78_IN_GA(x1)
U20_GA(x1, x2, x3)  =  U20_GA(x1, x3)
U49_AG(x1, x2, x3, x4, x5)  =  U49_AG(x4, x5)
U50_AG(x1, x2, x3, x4, x5, x6)  =  U50_AG(x4, x6)
U51_AG(x1, x2, x3, x4, x5, x6)  =  U51_AG(x4, x6)
U52_AG(x1, x2, x3, x4, x5)  =  U52_AG(x4, x5)
U53_AG(x1, x2, x3, x4, x5)  =  U53_AG(x4, x5)
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, x6)  =  U57_AG(x4, x6)
U58_AG(x1, x2, x3, x4, x5)  =  U58_AG(x4, x5)
U59_AG(x1, x2, x3, x4, x5, x6)  =  U59_AG(x4, x5, x6)
U60_AG(x1, x2, x3, x4, x5, x6, x7)  =  U60_AG(x4, x5, x7)
U61_AG(x1, x2, x3, x4, x5, x6)  =  U61_AG(x4, x5, x6)
U62_AG(x1, x2, x3, x4, x5, x6)  =  U62_AG(x4, x5, x6)
U63_AG(x1, x2, x3, x4, x5, x6, x7)  =  U63_AG(x4, x5, x6, x7)
U64_AG(x1, x2, x3, x4, x5, x6, x7, x8)  =  U64_AG(x4, x5, x6, x8)
U65_AG(x1, x2, x3, x4, x5, x6, x7, x8)  =  U65_AG(x4, x5, x6, x8)
U66_AG(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  U66_AG(x4, x5, x6, x10)
U67_AG(x1, x2, x3, x4, x5, x6, x7)  =  U67_AG(x4, x5, x6, x7)
P179_IN_GAAAG(x1, x2, x3, x4, x5)  =  P179_IN_GAAAG(x1, x5)
U23_GAAAG(x1, x2, x3, x4, x5, x6)  =  U23_GAAAG(x1, x5, x6)
U24_GAAAG(x1, x2, x3, x4, x5, x6, x7)  =  U24_GAAAG(x1, x3, x6, x7)
U25_GAAAG(x1, x2, x3, x4, x5, x6, x7)  =  U25_GAAAG(x1, x3, x6, x7)
U26_GAAAG(x1, x2, x3, x4, x5, x6, x7)  =  U26_GAAAG(x1, x2, x6, x7)
U27_GAAAG(x1, x2, x3, x4, x5, x6, x7)  =  U27_GAAAG(x1, x2, x6, x7)
P194_IN_GAAAG(x1, x2, x3, x4, x5)  =  P194_IN_GAAAG(x1, x5)
U28_GAAAG(x1, x2, x3, x4, x5, x6)  =  U28_GAAAG(x1, x5, x6)
U29_GAAAG(x1, x2, x3, x4, x5, x6, x7)  =  U29_GAAAG(x1, x2, x6, x7)
U30_GAAAG(x1, x2, x3, x4, x5, x6, x7)  =  U30_GAAAG(x1, x2, x6, x7)
U31_GAAAG(x1, x2, x3, x4, x5, x6, x7)  =  U31_GAAAG(x1, x4, x6, x7)
U32_GAAAG(x1, x2, x3, x4, x5, x6, x7)  =  U32_GAAAG(x1, x4, x6, x7)
U68_AG(x1, x2, x3, x4, x5, x6, x7)  =  U68_AG(x4, x5, x6, x7)
U69_AG(x1, x2, x3, x4, x5, x6, x7, x8)  =  U69_AG(x4, x5, x6, x8)
U70_AG(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U70_AG(x4, x5, x6, x9)
U71_AG(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  U71_AG(x4, x5, x6, x10)
U72_AG(x1, x2, x3, x4, x5, x6, x7)  =  U72_AG(x4, x5, x6, x7)
U73_AG(x1, x2, x3, x4, x5, x6)  =  U73_AG(x4, x5, x6)
U74_AG(x1, x2, x3, x4, x5, x6, x7)  =  U74_AG(x4, x5, x7)
U75_AG(x1, x2, x3, x4, x5, x6, x7, x8)  =  U75_AG(x4, x5, x8)
U76_AG(x1, x2, x3, x4, x5, x6)  =  U76_AG(x4, x5, x6)

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

(7) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 6 SCCs with 94 less nodes.

(8) Complex Obligation (AND)

(9) Obligation:

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

LESS78_IN_GA(s(T176), s(T177)) → LESS78_IN_GA(T176, T177)

The TRS R consists of the following rules:

splitc12_in_aaaa(T42, T44, .(T42, X71), X72) → U79_aaaa(T42, T44, X71, X72, splitc16_in_aaa(T44, X72, X71))
splitc16_in_aaa([], [], []) → splitc16_out_aaa([], [], [])
splitc16_in_aaa(.(T49, T51), .(T49, X89), X90) → U78_aaa(T49, T51, X89, X90, splitc16_in_aaa(T51, X90, X89))
U78_aaa(T49, T51, X89, X90, splitc16_out_aaa(T51, X90, X89)) → splitc16_out_aaa(.(T49, T51), .(T49, X89), X90)
U79_aaaa(T42, T44, X71, X72, splitc16_out_aaa(T44, X72, X71)) → splitc12_out_aaaa(T42, T44, .(T42, X71), X72)
msc38_in_aa([], []) → msc38_out_aa([], [])
msc38_in_aa(.(T89, []), .(T89, [])) → msc38_out_aa(.(T89, []), .(T89, []))
msc38_in_aa(.(T99, .(T100, T101)), X172) → U84_aa(T99, T100, T101, X172, qc34_in_aaaaaaaa(T99, T100, T101, X168, X169, X170, X171, X172))
qc34_in_aaaaaaaa(T72, T73, T74, T78, T84, T106, T105, X127) → U80_aaaaaaaa(T72, T73, T74, T78, T84, T106, T105, X127, splitc12_in_aaaa(T72, .(T73, T74), T78, T84))
U80_aaaaaaaa(T72, T73, T74, T78, T84, T106, T105, X127, splitc12_out_aaaa(T72, .(T73, T74), T78, T84)) → U81_aaaaaaaa(T72, T73, T74, T78, T84, T106, T105, X127, msc38_in_aa(T78, T106))
U81_aaaaaaaa(T72, T73, T74, T78, T84, T106, T105, X127, msc38_out_aa(T78, T106)) → U82_aaaaaaaa(T72, T73, T74, T78, T84, T106, T105, X127, msc38_in_aa(T84, T105))
U82_aaaaaaaa(T72, T73, T74, T78, T84, T106, T105, X127, msc38_out_aa(T84, T105)) → U83_aaaaaaaa(T72, T73, T74, T78, T84, T106, T105, X127, mergec54_in_aaa(T106, T105, X127))
mergec54_in_aaa([], T113, T113) → mergec54_out_aaa([], T113, T113)
mergec54_in_aaa(T118, [], T118) → mergec54_out_aaa(T118, [], T118)
mergec54_in_aaa(.(T139, T145), .(T146, T147), .(T139, X226)) → U85_aaa(T139, T145, T146, T147, X226, lessc70_in_aa(T139, T146))
lessc70_in_aa(0, T154) → lessc70_out_aa(0, T154)
lessc70_in_aa(s(T161), T162) → U91_aa(T161, T162, lessc78_in_aa(T161, T162))
lessc78_in_aa(0, s(T169)) → lessc78_out_aa(0, s(T169))
lessc78_in_aa(s(T176), s(T177)) → U89_aa(T176, T177, lessc78_in_aa(T176, T177))
U89_aa(T176, T177, lessc78_out_aa(T176, T177)) → lessc78_out_aa(s(T176), s(T177))
U91_aa(T161, T162, lessc78_out_aa(T161, T162)) → lessc70_out_aa(s(T161), T162)
U85_aaa(T139, T145, T146, T147, X226, lessc70_out_aa(T139, T146)) → U86_aaa(T139, T145, T146, T147, X226, mergec54_in_aaa(T145, .(T146, T147), X226))
mergec54_in_aaa(.(T202, T203), .(T196, T204), .(T196, X287)) → U87_aaa(T202, T203, T196, T204, X287, lessc78_in_aa(T196, T202))
U87_aaa(T202, T203, T196, T204, X287, lessc78_out_aa(T196, T202)) → U88_aaa(T202, T203, T196, T204, X287, mergec54_in_aaa(.(T202, T203), T204, X287))
U88_aaa(T202, T203, T196, T204, X287, mergec54_out_aaa(.(T202, T203), T204, X287)) → mergec54_out_aaa(.(T202, T203), .(T196, T204), .(T196, X287))
U86_aaa(T139, T145, T146, T147, X226, mergec54_out_aaa(T145, .(T146, T147), X226)) → mergec54_out_aaa(.(T139, T145), .(T146, T147), .(T139, X226))
U83_aaaaaaaa(T72, T73, T74, T78, T84, T106, T105, X127, mergec54_out_aaa(T106, T105, X127)) → qc34_out_aaaaaaaa(T72, T73, T74, T78, T84, T106, T105, X127)
U84_aa(T99, T100, T101, X172, qc34_out_aaaaaaaa(T99, T100, T101, X168, X169, X170, X171, X172)) → msc38_out_aa(.(T99, .(T100, T101)), X172)
msc25_in_aaa(T62, [], .(T62, [])) → msc25_out_aaa(T62, [], .(T62, []))
msc25_in_aaa(T72, .(T73, T74), X127) → U90_aaa(T72, T73, T74, X127, qc34_in_aaaaaaaa(T72, T73, T74, X123, X124, X125, X126, X127))
U90_aaa(T72, T73, T74, X127, qc34_out_aaaaaaaa(T72, T73, T74, X123, X124, X125, X126, X127)) → msc25_out_aaa(T72, .(T73, T74), X127)
lessc70_in_ga(0, T154) → lessc70_out_ga(0, T154)
lessc70_in_ga(s(T161), T162) → U91_ga(T161, T162, lessc78_in_ga(T161, T162))
lessc78_in_ga(0, s(T169)) → lessc78_out_ga(0, s(T169))
lessc78_in_ga(s(T176), s(T177)) → U89_ga(T176, T177, lessc78_in_ga(T176, T177))
U89_ga(T176, T177, lessc78_out_ga(T176, T177)) → lessc78_out_ga(s(T176), s(T177))
U91_ga(T161, T162, lessc78_out_ga(T161, T162)) → lessc70_out_ga(s(T161), T162)
lessc70_in_gg(0, T154) → lessc70_out_gg(0, T154)
lessc70_in_gg(s(T161), T162) → U91_gg(T161, T162, lessc78_in_gg(T161, T162))
lessc78_in_gg(0, s(T169)) → lessc78_out_gg(0, s(T169))
lessc78_in_gg(s(T176), s(T177)) → U89_gg(T176, T177, lessc78_in_gg(T176, T177))
U89_gg(T176, T177, lessc78_out_gg(T176, T177)) → lessc78_out_gg(s(T176), s(T177))
U91_gg(T161, T162, lessc78_out_gg(T161, T162)) → lessc70_out_gg(s(T161), T162)

The argument filtering Pi contains the following mapping:
[]  =  []
splitc12_in_aaaa(x1, x2, x3, x4)  =  splitc12_in_aaaa
U79_aaaa(x1, x2, x3, x4, x5)  =  U79_aaaa(x5)
splitc16_in_aaa(x1, x2, x3)  =  splitc16_in_aaa
splitc16_out_aaa(x1, x2, x3)  =  splitc16_out_aaa
U78_aaa(x1, x2, x3, x4, x5)  =  U78_aaa(x5)
splitc12_out_aaaa(x1, x2, x3, x4)  =  splitc12_out_aaaa
msc38_in_aa(x1, x2)  =  msc38_in_aa
msc38_out_aa(x1, x2)  =  msc38_out_aa
U84_aa(x1, x2, x3, x4, x5)  =  U84_aa(x5)
qc34_in_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  qc34_in_aaaaaaaa
U80_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U80_aaaaaaaa(x9)
U81_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U81_aaaaaaaa(x9)
U82_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U82_aaaaaaaa(x9)
U83_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U83_aaaaaaaa(x9)
mergec54_in_aaa(x1, x2, x3)  =  mergec54_in_aaa
mergec54_out_aaa(x1, x2, x3)  =  mergec54_out_aaa
U85_aaa(x1, x2, x3, x4, x5, x6)  =  U85_aaa(x6)
lessc70_in_aa(x1, x2)  =  lessc70_in_aa
lessc70_out_aa(x1, x2)  =  lessc70_out_aa(x1)
U91_aa(x1, x2, x3)  =  U91_aa(x3)
lessc78_in_aa(x1, x2)  =  lessc78_in_aa
lessc78_out_aa(x1, x2)  =  lessc78_out_aa(x1)
U89_aa(x1, x2, x3)  =  U89_aa(x3)
U86_aaa(x1, x2, x3, x4, x5, x6)  =  U86_aaa(x6)
U87_aaa(x1, x2, x3, x4, x5, x6)  =  U87_aaa(x6)
U88_aaa(x1, x2, x3, x4, x5, x6)  =  U88_aaa(x6)
qc34_out_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  qc34_out_aaaaaaaa
msc25_in_aaa(x1, x2, x3)  =  msc25_in_aaa
msc25_out_aaa(x1, x2, x3)  =  msc25_out_aaa
U90_aaa(x1, x2, x3, x4, x5)  =  U90_aaa(x5)
.(x1, x2)  =  .(x1, x2)
s(x1)  =  s(x1)
lessc70_in_ga(x1, x2)  =  lessc70_in_ga(x1)
0  =  0
lessc70_out_ga(x1, x2)  =  lessc70_out_ga(x1)
U91_ga(x1, x2, x3)  =  U91_ga(x1, x3)
lessc78_in_ga(x1, x2)  =  lessc78_in_ga(x1)
lessc78_out_ga(x1, x2)  =  lessc78_out_ga(x1)
U89_ga(x1, x2, x3)  =  U89_ga(x1, x3)
lessc70_in_gg(x1, x2)  =  lessc70_in_gg(x1, x2)
lessc70_out_gg(x1, x2)  =  lessc70_out_gg(x1, x2)
U91_gg(x1, x2, x3)  =  U91_gg(x1, x2, x3)
lessc78_in_gg(x1, x2)  =  lessc78_in_gg(x1, x2)
lessc78_out_gg(x1, x2)  =  lessc78_out_gg(x1, x2)
U89_gg(x1, x2, x3)  =  U89_gg(x1, x2, x3)
LESS78_IN_GA(x1, x2)  =  LESS78_IN_GA(x1)

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:

LESS78_IN_GA(s(T176), s(T177)) → LESS78_IN_GA(T176, T177)

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

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:

LESS78_IN_GA(s(T176)) → LESS78_IN_GA(T176)

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:

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

(15) YES

(16) Obligation:

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

P179_IN_GAAAG(T513, T568, .(T563, T569), T570, .(T563, T567)) → U24_GAAAG(T513, T568, T563, T569, T570, T567, lessc70_in_ga(T513, T568))
U24_GAAAG(T513, T568, T563, T569, T570, T567, lessc70_out_ga(T513, T568)) → P179_IN_GAAAG(T563, T568, T569, T570, T567)
P179_IN_GAAAG(T513, T585, .(T588, T590), T589, .(T585, T587)) → U26_GAAAG(T513, T585, T588, T590, T589, T587, lessc70_in_gg(T513, T585))
U26_GAAAG(T513, T585, T588, T590, T589, T587, lessc70_out_gg(T513, T585)) → P194_IN_GAAAG(T585, T588, T590, T589, T587)
P194_IN_GAAAG(T585, T632, T638, .(T637, T639), .(T632, T636)) → U29_GAAAG(T585, T632, T638, T637, T639, T636, lessc78_in_gg(T585, T632))
U29_GAAAG(T585, T632, T638, T637, T639, T636, lessc78_out_gg(T585, T632)) → P179_IN_GAAAG(T632, T637, T638, T639, T636)
P194_IN_GAAAG(T585, T657, T659, .(T654, T658), .(T654, T656)) → U31_GAAAG(T585, T657, T659, T654, T658, T656, lessc78_in_ga(T585, T657))
U31_GAAAG(T585, T657, T659, T654, T658, T656, lessc78_out_ga(T585, T657)) → P194_IN_GAAAG(T654, T657, T659, T658, T656)

The TRS R consists of the following rules:

splitc12_in_aaaa(T42, T44, .(T42, X71), X72) → U79_aaaa(T42, T44, X71, X72, splitc16_in_aaa(T44, X72, X71))
splitc16_in_aaa([], [], []) → splitc16_out_aaa([], [], [])
splitc16_in_aaa(.(T49, T51), .(T49, X89), X90) → U78_aaa(T49, T51, X89, X90, splitc16_in_aaa(T51, X90, X89))
U78_aaa(T49, T51, X89, X90, splitc16_out_aaa(T51, X90, X89)) → splitc16_out_aaa(.(T49, T51), .(T49, X89), X90)
U79_aaaa(T42, T44, X71, X72, splitc16_out_aaa(T44, X72, X71)) → splitc12_out_aaaa(T42, T44, .(T42, X71), X72)
msc38_in_aa([], []) → msc38_out_aa([], [])
msc38_in_aa(.(T89, []), .(T89, [])) → msc38_out_aa(.(T89, []), .(T89, []))
msc38_in_aa(.(T99, .(T100, T101)), X172) → U84_aa(T99, T100, T101, X172, qc34_in_aaaaaaaa(T99, T100, T101, X168, X169, X170, X171, X172))
qc34_in_aaaaaaaa(T72, T73, T74, T78, T84, T106, T105, X127) → U80_aaaaaaaa(T72, T73, T74, T78, T84, T106, T105, X127, splitc12_in_aaaa(T72, .(T73, T74), T78, T84))
U80_aaaaaaaa(T72, T73, T74, T78, T84, T106, T105, X127, splitc12_out_aaaa(T72, .(T73, T74), T78, T84)) → U81_aaaaaaaa(T72, T73, T74, T78, T84, T106, T105, X127, msc38_in_aa(T78, T106))
U81_aaaaaaaa(T72, T73, T74, T78, T84, T106, T105, X127, msc38_out_aa(T78, T106)) → U82_aaaaaaaa(T72, T73, T74, T78, T84, T106, T105, X127, msc38_in_aa(T84, T105))
U82_aaaaaaaa(T72, T73, T74, T78, T84, T106, T105, X127, msc38_out_aa(T84, T105)) → U83_aaaaaaaa(T72, T73, T74, T78, T84, T106, T105, X127, mergec54_in_aaa(T106, T105, X127))
mergec54_in_aaa([], T113, T113) → mergec54_out_aaa([], T113, T113)
mergec54_in_aaa(T118, [], T118) → mergec54_out_aaa(T118, [], T118)
mergec54_in_aaa(.(T139, T145), .(T146, T147), .(T139, X226)) → U85_aaa(T139, T145, T146, T147, X226, lessc70_in_aa(T139, T146))
lessc70_in_aa(0, T154) → lessc70_out_aa(0, T154)
lessc70_in_aa(s(T161), T162) → U91_aa(T161, T162, lessc78_in_aa(T161, T162))
lessc78_in_aa(0, s(T169)) → lessc78_out_aa(0, s(T169))
lessc78_in_aa(s(T176), s(T177)) → U89_aa(T176, T177, lessc78_in_aa(T176, T177))
U89_aa(T176, T177, lessc78_out_aa(T176, T177)) → lessc78_out_aa(s(T176), s(T177))
U91_aa(T161, T162, lessc78_out_aa(T161, T162)) → lessc70_out_aa(s(T161), T162)
U85_aaa(T139, T145, T146, T147, X226, lessc70_out_aa(T139, T146)) → U86_aaa(T139, T145, T146, T147, X226, mergec54_in_aaa(T145, .(T146, T147), X226))
mergec54_in_aaa(.(T202, T203), .(T196, T204), .(T196, X287)) → U87_aaa(T202, T203, T196, T204, X287, lessc78_in_aa(T196, T202))
U87_aaa(T202, T203, T196, T204, X287, lessc78_out_aa(T196, T202)) → U88_aaa(T202, T203, T196, T204, X287, mergec54_in_aaa(.(T202, T203), T204, X287))
U88_aaa(T202, T203, T196, T204, X287, mergec54_out_aaa(.(T202, T203), T204, X287)) → mergec54_out_aaa(.(T202, T203), .(T196, T204), .(T196, X287))
U86_aaa(T139, T145, T146, T147, X226, mergec54_out_aaa(T145, .(T146, T147), X226)) → mergec54_out_aaa(.(T139, T145), .(T146, T147), .(T139, X226))
U83_aaaaaaaa(T72, T73, T74, T78, T84, T106, T105, X127, mergec54_out_aaa(T106, T105, X127)) → qc34_out_aaaaaaaa(T72, T73, T74, T78, T84, T106, T105, X127)
U84_aa(T99, T100, T101, X172, qc34_out_aaaaaaaa(T99, T100, T101, X168, X169, X170, X171, X172)) → msc38_out_aa(.(T99, .(T100, T101)), X172)
msc25_in_aaa(T62, [], .(T62, [])) → msc25_out_aaa(T62, [], .(T62, []))
msc25_in_aaa(T72, .(T73, T74), X127) → U90_aaa(T72, T73, T74, X127, qc34_in_aaaaaaaa(T72, T73, T74, X123, X124, X125, X126, X127))
U90_aaa(T72, T73, T74, X127, qc34_out_aaaaaaaa(T72, T73, T74, X123, X124, X125, X126, X127)) → msc25_out_aaa(T72, .(T73, T74), X127)
lessc70_in_ga(0, T154) → lessc70_out_ga(0, T154)
lessc70_in_ga(s(T161), T162) → U91_ga(T161, T162, lessc78_in_ga(T161, T162))
lessc78_in_ga(0, s(T169)) → lessc78_out_ga(0, s(T169))
lessc78_in_ga(s(T176), s(T177)) → U89_ga(T176, T177, lessc78_in_ga(T176, T177))
U89_ga(T176, T177, lessc78_out_ga(T176, T177)) → lessc78_out_ga(s(T176), s(T177))
U91_ga(T161, T162, lessc78_out_ga(T161, T162)) → lessc70_out_ga(s(T161), T162)
lessc70_in_gg(0, T154) → lessc70_out_gg(0, T154)
lessc70_in_gg(s(T161), T162) → U91_gg(T161, T162, lessc78_in_gg(T161, T162))
lessc78_in_gg(0, s(T169)) → lessc78_out_gg(0, s(T169))
lessc78_in_gg(s(T176), s(T177)) → U89_gg(T176, T177, lessc78_in_gg(T176, T177))
U89_gg(T176, T177, lessc78_out_gg(T176, T177)) → lessc78_out_gg(s(T176), s(T177))
U91_gg(T161, T162, lessc78_out_gg(T161, T162)) → lessc70_out_gg(s(T161), T162)

The argument filtering Pi contains the following mapping:
[]  =  []
splitc12_in_aaaa(x1, x2, x3, x4)  =  splitc12_in_aaaa
U79_aaaa(x1, x2, x3, x4, x5)  =  U79_aaaa(x5)
splitc16_in_aaa(x1, x2, x3)  =  splitc16_in_aaa
splitc16_out_aaa(x1, x2, x3)  =  splitc16_out_aaa
U78_aaa(x1, x2, x3, x4, x5)  =  U78_aaa(x5)
splitc12_out_aaaa(x1, x2, x3, x4)  =  splitc12_out_aaaa
msc38_in_aa(x1, x2)  =  msc38_in_aa
msc38_out_aa(x1, x2)  =  msc38_out_aa
U84_aa(x1, x2, x3, x4, x5)  =  U84_aa(x5)
qc34_in_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  qc34_in_aaaaaaaa
U80_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U80_aaaaaaaa(x9)
U81_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U81_aaaaaaaa(x9)
U82_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U82_aaaaaaaa(x9)
U83_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U83_aaaaaaaa(x9)
mergec54_in_aaa(x1, x2, x3)  =  mergec54_in_aaa
mergec54_out_aaa(x1, x2, x3)  =  mergec54_out_aaa
U85_aaa(x1, x2, x3, x4, x5, x6)  =  U85_aaa(x6)
lessc70_in_aa(x1, x2)  =  lessc70_in_aa
lessc70_out_aa(x1, x2)  =  lessc70_out_aa(x1)
U91_aa(x1, x2, x3)  =  U91_aa(x3)
lessc78_in_aa(x1, x2)  =  lessc78_in_aa
lessc78_out_aa(x1, x2)  =  lessc78_out_aa(x1)
U89_aa(x1, x2, x3)  =  U89_aa(x3)
U86_aaa(x1, x2, x3, x4, x5, x6)  =  U86_aaa(x6)
U87_aaa(x1, x2, x3, x4, x5, x6)  =  U87_aaa(x6)
U88_aaa(x1, x2, x3, x4, x5, x6)  =  U88_aaa(x6)
qc34_out_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  qc34_out_aaaaaaaa
msc25_in_aaa(x1, x2, x3)  =  msc25_in_aaa
msc25_out_aaa(x1, x2, x3)  =  msc25_out_aaa
U90_aaa(x1, x2, x3, x4, x5)  =  U90_aaa(x5)
.(x1, x2)  =  .(x1, x2)
s(x1)  =  s(x1)
lessc70_in_ga(x1, x2)  =  lessc70_in_ga(x1)
0  =  0
lessc70_out_ga(x1, x2)  =  lessc70_out_ga(x1)
U91_ga(x1, x2, x3)  =  U91_ga(x1, x3)
lessc78_in_ga(x1, x2)  =  lessc78_in_ga(x1)
lessc78_out_ga(x1, x2)  =  lessc78_out_ga(x1)
U89_ga(x1, x2, x3)  =  U89_ga(x1, x3)
lessc70_in_gg(x1, x2)  =  lessc70_in_gg(x1, x2)
lessc70_out_gg(x1, x2)  =  lessc70_out_gg(x1, x2)
U91_gg(x1, x2, x3)  =  U91_gg(x1, x2, x3)
lessc78_in_gg(x1, x2)  =  lessc78_in_gg(x1, x2)
lessc78_out_gg(x1, x2)  =  lessc78_out_gg(x1, x2)
U89_gg(x1, x2, x3)  =  U89_gg(x1, x2, x3)
P179_IN_GAAAG(x1, x2, x3, x4, x5)  =  P179_IN_GAAAG(x1, x5)
U24_GAAAG(x1, x2, x3, x4, x5, x6, x7)  =  U24_GAAAG(x1, x3, x6, x7)
U26_GAAAG(x1, x2, x3, x4, x5, x6, x7)  =  U26_GAAAG(x1, x2, x6, x7)
P194_IN_GAAAG(x1, x2, x3, x4, x5)  =  P194_IN_GAAAG(x1, x5)
U29_GAAAG(x1, x2, x3, x4, x5, x6, x7)  =  U29_GAAAG(x1, x2, x6, x7)
U31_GAAAG(x1, x2, x3, x4, x5, x6, x7)  =  U31_GAAAG(x1, x4, x6, x7)

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:

P179_IN_GAAAG(T513, T568, .(T563, T569), T570, .(T563, T567)) → U24_GAAAG(T513, T568, T563, T569, T570, T567, lessc70_in_ga(T513, T568))
U24_GAAAG(T513, T568, T563, T569, T570, T567, lessc70_out_ga(T513, T568)) → P179_IN_GAAAG(T563, T568, T569, T570, T567)
P179_IN_GAAAG(T513, T585, .(T588, T590), T589, .(T585, T587)) → U26_GAAAG(T513, T585, T588, T590, T589, T587, lessc70_in_gg(T513, T585))
U26_GAAAG(T513, T585, T588, T590, T589, T587, lessc70_out_gg(T513, T585)) → P194_IN_GAAAG(T585, T588, T590, T589, T587)
P194_IN_GAAAG(T585, T632, T638, .(T637, T639), .(T632, T636)) → U29_GAAAG(T585, T632, T638, T637, T639, T636, lessc78_in_gg(T585, T632))
U29_GAAAG(T585, T632, T638, T637, T639, T636, lessc78_out_gg(T585, T632)) → P179_IN_GAAAG(T632, T637, T638, T639, T636)
P194_IN_GAAAG(T585, T657, T659, .(T654, T658), .(T654, T656)) → U31_GAAAG(T585, T657, T659, T654, T658, T656, lessc78_in_ga(T585, T657))
U31_GAAAG(T585, T657, T659, T654, T658, T656, lessc78_out_ga(T585, T657)) → P194_IN_GAAAG(T654, T657, T659, T658, T656)

The TRS R consists of the following rules:

lessc70_in_ga(0, T154) → lessc70_out_ga(0, T154)
lessc70_in_ga(s(T161), T162) → U91_ga(T161, T162, lessc78_in_ga(T161, T162))
lessc70_in_gg(0, T154) → lessc70_out_gg(0, T154)
lessc70_in_gg(s(T161), T162) → U91_gg(T161, T162, lessc78_in_gg(T161, T162))
lessc78_in_gg(0, s(T169)) → lessc78_out_gg(0, s(T169))
lessc78_in_gg(s(T176), s(T177)) → U89_gg(T176, T177, lessc78_in_gg(T176, T177))
lessc78_in_ga(0, s(T169)) → lessc78_out_ga(0, s(T169))
lessc78_in_ga(s(T176), s(T177)) → U89_ga(T176, T177, lessc78_in_ga(T176, T177))
U91_ga(T161, T162, lessc78_out_ga(T161, T162)) → lessc70_out_ga(s(T161), T162)
U91_gg(T161, T162, lessc78_out_gg(T161, T162)) → lessc70_out_gg(s(T161), T162)
U89_gg(T176, T177, lessc78_out_gg(T176, T177)) → lessc78_out_gg(s(T176), s(T177))
U89_ga(T176, T177, lessc78_out_ga(T176, T177)) → lessc78_out_ga(s(T176), s(T177))

The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
s(x1)  =  s(x1)
lessc70_in_ga(x1, x2)  =  lessc70_in_ga(x1)
0  =  0
lessc70_out_ga(x1, x2)  =  lessc70_out_ga(x1)
U91_ga(x1, x2, x3)  =  U91_ga(x1, x3)
lessc78_in_ga(x1, x2)  =  lessc78_in_ga(x1)
lessc78_out_ga(x1, x2)  =  lessc78_out_ga(x1)
U89_ga(x1, x2, x3)  =  U89_ga(x1, x3)
lessc70_in_gg(x1, x2)  =  lessc70_in_gg(x1, x2)
lessc70_out_gg(x1, x2)  =  lessc70_out_gg(x1, x2)
U91_gg(x1, x2, x3)  =  U91_gg(x1, x2, x3)
lessc78_in_gg(x1, x2)  =  lessc78_in_gg(x1, x2)
lessc78_out_gg(x1, x2)  =  lessc78_out_gg(x1, x2)
U89_gg(x1, x2, x3)  =  U89_gg(x1, x2, x3)
P179_IN_GAAAG(x1, x2, x3, x4, x5)  =  P179_IN_GAAAG(x1, x5)
U24_GAAAG(x1, x2, x3, x4, x5, x6, x7)  =  U24_GAAAG(x1, x3, x6, x7)
U26_GAAAG(x1, x2, x3, x4, x5, x6, x7)  =  U26_GAAAG(x1, x2, x6, x7)
P194_IN_GAAAG(x1, x2, x3, x4, x5)  =  P194_IN_GAAAG(x1, x5)
U29_GAAAG(x1, x2, x3, x4, x5, x6, x7)  =  U29_GAAAG(x1, x2, x6, x7)
U31_GAAAG(x1, x2, x3, x4, x5, x6, x7)  =  U31_GAAAG(x1, x4, x6, x7)

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:

P179_IN_GAAAG(T513, .(T563, T567)) → U24_GAAAG(T513, T563, T567, lessc70_in_ga(T513))
U24_GAAAG(T513, T563, T567, lessc70_out_ga(T513)) → P179_IN_GAAAG(T563, T567)
P179_IN_GAAAG(T513, .(T585, T587)) → U26_GAAAG(T513, T585, T587, lessc70_in_gg(T513, T585))
U26_GAAAG(T513, T585, T587, lessc70_out_gg(T513, T585)) → P194_IN_GAAAG(T585, T587)
P194_IN_GAAAG(T585, .(T632, T636)) → U29_GAAAG(T585, T632, T636, lessc78_in_gg(T585, T632))
U29_GAAAG(T585, T632, T636, lessc78_out_gg(T585, T632)) → P179_IN_GAAAG(T632, T636)
P194_IN_GAAAG(T585, .(T654, T656)) → U31_GAAAG(T585, T654, T656, lessc78_in_ga(T585))
U31_GAAAG(T585, T654, T656, lessc78_out_ga(T585)) → P194_IN_GAAAG(T654, T656)

The TRS R consists of the following rules:

lessc70_in_ga(0) → lessc70_out_ga(0)
lessc70_in_ga(s(T161)) → U91_ga(T161, lessc78_in_ga(T161))
lessc70_in_gg(0, T154) → lessc70_out_gg(0, T154)
lessc70_in_gg(s(T161), T162) → U91_gg(T161, T162, lessc78_in_gg(T161, T162))
lessc78_in_gg(0, s(T169)) → lessc78_out_gg(0, s(T169))
lessc78_in_gg(s(T176), s(T177)) → U89_gg(T176, T177, lessc78_in_gg(T176, T177))
lessc78_in_ga(0) → lessc78_out_ga(0)
lessc78_in_ga(s(T176)) → U89_ga(T176, lessc78_in_ga(T176))
U91_ga(T161, lessc78_out_ga(T161)) → lessc70_out_ga(s(T161))
U91_gg(T161, T162, lessc78_out_gg(T161, T162)) → lessc70_out_gg(s(T161), T162)
U89_gg(T176, T177, lessc78_out_gg(T176, T177)) → lessc78_out_gg(s(T176), s(T177))
U89_ga(T176, lessc78_out_ga(T176)) → lessc78_out_ga(s(T176))

The set Q consists of the following terms:

lessc70_in_ga(x0)
lessc70_in_gg(x0, x1)
lessc78_in_gg(x0, x1)
lessc78_in_ga(x0)
U91_ga(x0, x1)
U91_gg(x0, x1, x2)
U89_gg(x0, x1, x2)
U89_ga(x0, x1)

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:

  • U24_GAAAG(T513, T563, T567, lessc70_out_ga(T513)) → P179_IN_GAAAG(T563, T567)
    The graph contains the following edges 2 >= 1, 3 >= 2

  • U29_GAAAG(T585, T632, T636, lessc78_out_gg(T585, T632)) → P179_IN_GAAAG(T632, T636)
    The graph contains the following edges 2 >= 1, 4 > 1, 3 >= 2

  • P179_IN_GAAAG(T513, .(T563, T567)) → U24_GAAAG(T513, T563, T567, lessc70_in_ga(T513))
    The graph contains the following edges 1 >= 1, 2 > 2, 2 > 3

  • P179_IN_GAAAG(T513, .(T585, T587)) → U26_GAAAG(T513, T585, T587, lessc70_in_gg(T513, T585))
    The graph contains the following edges 1 >= 1, 2 > 2, 2 > 3

  • U26_GAAAG(T513, T585, T587, lessc70_out_gg(T513, T585)) → P194_IN_GAAAG(T585, T587)
    The graph contains the following edges 2 >= 1, 4 > 1, 3 >= 2

  • U31_GAAAG(T585, T654, T656, lessc78_out_ga(T585)) → P194_IN_GAAAG(T654, T656)
    The graph contains the following edges 2 >= 1, 3 >= 2

  • P194_IN_GAAAG(T585, .(T632, T636)) → U29_GAAAG(T585, T632, T636, lessc78_in_gg(T585, T632))
    The graph contains the following edges 1 >= 1, 2 > 2, 2 > 3

  • P194_IN_GAAAG(T585, .(T654, T656)) → U31_GAAAG(T585, T654, T656, lessc78_in_ga(T585))
    The graph contains the following edges 1 >= 1, 2 > 2, 2 > 3

(22) YES

(23) Obligation:

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

LESS78_IN_AA(s(T176), s(T177)) → LESS78_IN_AA(T176, T177)

The TRS R consists of the following rules:

splitc12_in_aaaa(T42, T44, .(T42, X71), X72) → U79_aaaa(T42, T44, X71, X72, splitc16_in_aaa(T44, X72, X71))
splitc16_in_aaa([], [], []) → splitc16_out_aaa([], [], [])
splitc16_in_aaa(.(T49, T51), .(T49, X89), X90) → U78_aaa(T49, T51, X89, X90, splitc16_in_aaa(T51, X90, X89))
U78_aaa(T49, T51, X89, X90, splitc16_out_aaa(T51, X90, X89)) → splitc16_out_aaa(.(T49, T51), .(T49, X89), X90)
U79_aaaa(T42, T44, X71, X72, splitc16_out_aaa(T44, X72, X71)) → splitc12_out_aaaa(T42, T44, .(T42, X71), X72)
msc38_in_aa([], []) → msc38_out_aa([], [])
msc38_in_aa(.(T89, []), .(T89, [])) → msc38_out_aa(.(T89, []), .(T89, []))
msc38_in_aa(.(T99, .(T100, T101)), X172) → U84_aa(T99, T100, T101, X172, qc34_in_aaaaaaaa(T99, T100, T101, X168, X169, X170, X171, X172))
qc34_in_aaaaaaaa(T72, T73, T74, T78, T84, T106, T105, X127) → U80_aaaaaaaa(T72, T73, T74, T78, T84, T106, T105, X127, splitc12_in_aaaa(T72, .(T73, T74), T78, T84))
U80_aaaaaaaa(T72, T73, T74, T78, T84, T106, T105, X127, splitc12_out_aaaa(T72, .(T73, T74), T78, T84)) → U81_aaaaaaaa(T72, T73, T74, T78, T84, T106, T105, X127, msc38_in_aa(T78, T106))
U81_aaaaaaaa(T72, T73, T74, T78, T84, T106, T105, X127, msc38_out_aa(T78, T106)) → U82_aaaaaaaa(T72, T73, T74, T78, T84, T106, T105, X127, msc38_in_aa(T84, T105))
U82_aaaaaaaa(T72, T73, T74, T78, T84, T106, T105, X127, msc38_out_aa(T84, T105)) → U83_aaaaaaaa(T72, T73, T74, T78, T84, T106, T105, X127, mergec54_in_aaa(T106, T105, X127))
mergec54_in_aaa([], T113, T113) → mergec54_out_aaa([], T113, T113)
mergec54_in_aaa(T118, [], T118) → mergec54_out_aaa(T118, [], T118)
mergec54_in_aaa(.(T139, T145), .(T146, T147), .(T139, X226)) → U85_aaa(T139, T145, T146, T147, X226, lessc70_in_aa(T139, T146))
lessc70_in_aa(0, T154) → lessc70_out_aa(0, T154)
lessc70_in_aa(s(T161), T162) → U91_aa(T161, T162, lessc78_in_aa(T161, T162))
lessc78_in_aa(0, s(T169)) → lessc78_out_aa(0, s(T169))
lessc78_in_aa(s(T176), s(T177)) → U89_aa(T176, T177, lessc78_in_aa(T176, T177))
U89_aa(T176, T177, lessc78_out_aa(T176, T177)) → lessc78_out_aa(s(T176), s(T177))
U91_aa(T161, T162, lessc78_out_aa(T161, T162)) → lessc70_out_aa(s(T161), T162)
U85_aaa(T139, T145, T146, T147, X226, lessc70_out_aa(T139, T146)) → U86_aaa(T139, T145, T146, T147, X226, mergec54_in_aaa(T145, .(T146, T147), X226))
mergec54_in_aaa(.(T202, T203), .(T196, T204), .(T196, X287)) → U87_aaa(T202, T203, T196, T204, X287, lessc78_in_aa(T196, T202))
U87_aaa(T202, T203, T196, T204, X287, lessc78_out_aa(T196, T202)) → U88_aaa(T202, T203, T196, T204, X287, mergec54_in_aaa(.(T202, T203), T204, X287))
U88_aaa(T202, T203, T196, T204, X287, mergec54_out_aaa(.(T202, T203), T204, X287)) → mergec54_out_aaa(.(T202, T203), .(T196, T204), .(T196, X287))
U86_aaa(T139, T145, T146, T147, X226, mergec54_out_aaa(T145, .(T146, T147), X226)) → mergec54_out_aaa(.(T139, T145), .(T146, T147), .(T139, X226))
U83_aaaaaaaa(T72, T73, T74, T78, T84, T106, T105, X127, mergec54_out_aaa(T106, T105, X127)) → qc34_out_aaaaaaaa(T72, T73, T74, T78, T84, T106, T105, X127)
U84_aa(T99, T100, T101, X172, qc34_out_aaaaaaaa(T99, T100, T101, X168, X169, X170, X171, X172)) → msc38_out_aa(.(T99, .(T100, T101)), X172)
msc25_in_aaa(T62, [], .(T62, [])) → msc25_out_aaa(T62, [], .(T62, []))
msc25_in_aaa(T72, .(T73, T74), X127) → U90_aaa(T72, T73, T74, X127, qc34_in_aaaaaaaa(T72, T73, T74, X123, X124, X125, X126, X127))
U90_aaa(T72, T73, T74, X127, qc34_out_aaaaaaaa(T72, T73, T74, X123, X124, X125, X126, X127)) → msc25_out_aaa(T72, .(T73, T74), X127)
lessc70_in_ga(0, T154) → lessc70_out_ga(0, T154)
lessc70_in_ga(s(T161), T162) → U91_ga(T161, T162, lessc78_in_ga(T161, T162))
lessc78_in_ga(0, s(T169)) → lessc78_out_ga(0, s(T169))
lessc78_in_ga(s(T176), s(T177)) → U89_ga(T176, T177, lessc78_in_ga(T176, T177))
U89_ga(T176, T177, lessc78_out_ga(T176, T177)) → lessc78_out_ga(s(T176), s(T177))
U91_ga(T161, T162, lessc78_out_ga(T161, T162)) → lessc70_out_ga(s(T161), T162)
lessc70_in_gg(0, T154) → lessc70_out_gg(0, T154)
lessc70_in_gg(s(T161), T162) → U91_gg(T161, T162, lessc78_in_gg(T161, T162))
lessc78_in_gg(0, s(T169)) → lessc78_out_gg(0, s(T169))
lessc78_in_gg(s(T176), s(T177)) → U89_gg(T176, T177, lessc78_in_gg(T176, T177))
U89_gg(T176, T177, lessc78_out_gg(T176, T177)) → lessc78_out_gg(s(T176), s(T177))
U91_gg(T161, T162, lessc78_out_gg(T161, T162)) → lessc70_out_gg(s(T161), T162)

The argument filtering Pi contains the following mapping:
[]  =  []
splitc12_in_aaaa(x1, x2, x3, x4)  =  splitc12_in_aaaa
U79_aaaa(x1, x2, x3, x4, x5)  =  U79_aaaa(x5)
splitc16_in_aaa(x1, x2, x3)  =  splitc16_in_aaa
splitc16_out_aaa(x1, x2, x3)  =  splitc16_out_aaa
U78_aaa(x1, x2, x3, x4, x5)  =  U78_aaa(x5)
splitc12_out_aaaa(x1, x2, x3, x4)  =  splitc12_out_aaaa
msc38_in_aa(x1, x2)  =  msc38_in_aa
msc38_out_aa(x1, x2)  =  msc38_out_aa
U84_aa(x1, x2, x3, x4, x5)  =  U84_aa(x5)
qc34_in_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  qc34_in_aaaaaaaa
U80_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U80_aaaaaaaa(x9)
U81_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U81_aaaaaaaa(x9)
U82_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U82_aaaaaaaa(x9)
U83_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U83_aaaaaaaa(x9)
mergec54_in_aaa(x1, x2, x3)  =  mergec54_in_aaa
mergec54_out_aaa(x1, x2, x3)  =  mergec54_out_aaa
U85_aaa(x1, x2, x3, x4, x5, x6)  =  U85_aaa(x6)
lessc70_in_aa(x1, x2)  =  lessc70_in_aa
lessc70_out_aa(x1, x2)  =  lessc70_out_aa(x1)
U91_aa(x1, x2, x3)  =  U91_aa(x3)
lessc78_in_aa(x1, x2)  =  lessc78_in_aa
lessc78_out_aa(x1, x2)  =  lessc78_out_aa(x1)
U89_aa(x1, x2, x3)  =  U89_aa(x3)
U86_aaa(x1, x2, x3, x4, x5, x6)  =  U86_aaa(x6)
U87_aaa(x1, x2, x3, x4, x5, x6)  =  U87_aaa(x6)
U88_aaa(x1, x2, x3, x4, x5, x6)  =  U88_aaa(x6)
qc34_out_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  qc34_out_aaaaaaaa
msc25_in_aaa(x1, x2, x3)  =  msc25_in_aaa
msc25_out_aaa(x1, x2, x3)  =  msc25_out_aaa
U90_aaa(x1, x2, x3, x4, x5)  =  U90_aaa(x5)
.(x1, x2)  =  .(x1, x2)
s(x1)  =  s(x1)
lessc70_in_ga(x1, x2)  =  lessc70_in_ga(x1)
0  =  0
lessc70_out_ga(x1, x2)  =  lessc70_out_ga(x1)
U91_ga(x1, x2, x3)  =  U91_ga(x1, x3)
lessc78_in_ga(x1, x2)  =  lessc78_in_ga(x1)
lessc78_out_ga(x1, x2)  =  lessc78_out_ga(x1)
U89_ga(x1, x2, x3)  =  U89_ga(x1, x3)
lessc70_in_gg(x1, x2)  =  lessc70_in_gg(x1, x2)
lessc70_out_gg(x1, x2)  =  lessc70_out_gg(x1, x2)
U91_gg(x1, x2, x3)  =  U91_gg(x1, x2, x3)
lessc78_in_gg(x1, x2)  =  lessc78_in_gg(x1, x2)
lessc78_out_gg(x1, x2)  =  lessc78_out_gg(x1, x2)
U89_gg(x1, x2, x3)  =  U89_gg(x1, x2, x3)
LESS78_IN_AA(x1, x2)  =  LESS78_IN_AA

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:

LESS78_IN_AA(s(T176), s(T177)) → LESS78_IN_AA(T176, T177)

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

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:

LESS78_IN_AALESS78_IN_AA

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

(28) 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 = LESS78_IN_AA evaluates to t =LESS78_IN_AA

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 LESS78_IN_AA to LESS78_IN_AA.



(29) NO

(30) Obligation:

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

MERGE54_IN_AAA(.(T139, T145), .(T146, T147), .(T139, X226)) → U15_AAA(T139, T145, T146, T147, X226, lessc70_in_aa(T139, T146))
U15_AAA(T139, T145, T146, T147, X226, lessc70_out_aa(T139, T146)) → MERGE54_IN_AAA(T145, .(T146, T147), X226)
MERGE54_IN_AAA(.(T202, T203), .(T196, T204), .(T196, X287)) → U18_AAA(T202, T203, T196, T204, X287, lessc78_in_aa(T196, T202))
U18_AAA(T202, T203, T196, T204, X287, lessc78_out_aa(T196, T202)) → MERGE54_IN_AAA(.(T202, T203), T204, X287)

The TRS R consists of the following rules:

splitc12_in_aaaa(T42, T44, .(T42, X71), X72) → U79_aaaa(T42, T44, X71, X72, splitc16_in_aaa(T44, X72, X71))
splitc16_in_aaa([], [], []) → splitc16_out_aaa([], [], [])
splitc16_in_aaa(.(T49, T51), .(T49, X89), X90) → U78_aaa(T49, T51, X89, X90, splitc16_in_aaa(T51, X90, X89))
U78_aaa(T49, T51, X89, X90, splitc16_out_aaa(T51, X90, X89)) → splitc16_out_aaa(.(T49, T51), .(T49, X89), X90)
U79_aaaa(T42, T44, X71, X72, splitc16_out_aaa(T44, X72, X71)) → splitc12_out_aaaa(T42, T44, .(T42, X71), X72)
msc38_in_aa([], []) → msc38_out_aa([], [])
msc38_in_aa(.(T89, []), .(T89, [])) → msc38_out_aa(.(T89, []), .(T89, []))
msc38_in_aa(.(T99, .(T100, T101)), X172) → U84_aa(T99, T100, T101, X172, qc34_in_aaaaaaaa(T99, T100, T101, X168, X169, X170, X171, X172))
qc34_in_aaaaaaaa(T72, T73, T74, T78, T84, T106, T105, X127) → U80_aaaaaaaa(T72, T73, T74, T78, T84, T106, T105, X127, splitc12_in_aaaa(T72, .(T73, T74), T78, T84))
U80_aaaaaaaa(T72, T73, T74, T78, T84, T106, T105, X127, splitc12_out_aaaa(T72, .(T73, T74), T78, T84)) → U81_aaaaaaaa(T72, T73, T74, T78, T84, T106, T105, X127, msc38_in_aa(T78, T106))
U81_aaaaaaaa(T72, T73, T74, T78, T84, T106, T105, X127, msc38_out_aa(T78, T106)) → U82_aaaaaaaa(T72, T73, T74, T78, T84, T106, T105, X127, msc38_in_aa(T84, T105))
U82_aaaaaaaa(T72, T73, T74, T78, T84, T106, T105, X127, msc38_out_aa(T84, T105)) → U83_aaaaaaaa(T72, T73, T74, T78, T84, T106, T105, X127, mergec54_in_aaa(T106, T105, X127))
mergec54_in_aaa([], T113, T113) → mergec54_out_aaa([], T113, T113)
mergec54_in_aaa(T118, [], T118) → mergec54_out_aaa(T118, [], T118)
mergec54_in_aaa(.(T139, T145), .(T146, T147), .(T139, X226)) → U85_aaa(T139, T145, T146, T147, X226, lessc70_in_aa(T139, T146))
lessc70_in_aa(0, T154) → lessc70_out_aa(0, T154)
lessc70_in_aa(s(T161), T162) → U91_aa(T161, T162, lessc78_in_aa(T161, T162))
lessc78_in_aa(0, s(T169)) → lessc78_out_aa(0, s(T169))
lessc78_in_aa(s(T176), s(T177)) → U89_aa(T176, T177, lessc78_in_aa(T176, T177))
U89_aa(T176, T177, lessc78_out_aa(T176, T177)) → lessc78_out_aa(s(T176), s(T177))
U91_aa(T161, T162, lessc78_out_aa(T161, T162)) → lessc70_out_aa(s(T161), T162)
U85_aaa(T139, T145, T146, T147, X226, lessc70_out_aa(T139, T146)) → U86_aaa(T139, T145, T146, T147, X226, mergec54_in_aaa(T145, .(T146, T147), X226))
mergec54_in_aaa(.(T202, T203), .(T196, T204), .(T196, X287)) → U87_aaa(T202, T203, T196, T204, X287, lessc78_in_aa(T196, T202))
U87_aaa(T202, T203, T196, T204, X287, lessc78_out_aa(T196, T202)) → U88_aaa(T202, T203, T196, T204, X287, mergec54_in_aaa(.(T202, T203), T204, X287))
U88_aaa(T202, T203, T196, T204, X287, mergec54_out_aaa(.(T202, T203), T204, X287)) → mergec54_out_aaa(.(T202, T203), .(T196, T204), .(T196, X287))
U86_aaa(T139, T145, T146, T147, X226, mergec54_out_aaa(T145, .(T146, T147), X226)) → mergec54_out_aaa(.(T139, T145), .(T146, T147), .(T139, X226))
U83_aaaaaaaa(T72, T73, T74, T78, T84, T106, T105, X127, mergec54_out_aaa(T106, T105, X127)) → qc34_out_aaaaaaaa(T72, T73, T74, T78, T84, T106, T105, X127)
U84_aa(T99, T100, T101, X172, qc34_out_aaaaaaaa(T99, T100, T101, X168, X169, X170, X171, X172)) → msc38_out_aa(.(T99, .(T100, T101)), X172)
msc25_in_aaa(T62, [], .(T62, [])) → msc25_out_aaa(T62, [], .(T62, []))
msc25_in_aaa(T72, .(T73, T74), X127) → U90_aaa(T72, T73, T74, X127, qc34_in_aaaaaaaa(T72, T73, T74, X123, X124, X125, X126, X127))
U90_aaa(T72, T73, T74, X127, qc34_out_aaaaaaaa(T72, T73, T74, X123, X124, X125, X126, X127)) → msc25_out_aaa(T72, .(T73, T74), X127)
lessc70_in_ga(0, T154) → lessc70_out_ga(0, T154)
lessc70_in_ga(s(T161), T162) → U91_ga(T161, T162, lessc78_in_ga(T161, T162))
lessc78_in_ga(0, s(T169)) → lessc78_out_ga(0, s(T169))
lessc78_in_ga(s(T176), s(T177)) → U89_ga(T176, T177, lessc78_in_ga(T176, T177))
U89_ga(T176, T177, lessc78_out_ga(T176, T177)) → lessc78_out_ga(s(T176), s(T177))
U91_ga(T161, T162, lessc78_out_ga(T161, T162)) → lessc70_out_ga(s(T161), T162)
lessc70_in_gg(0, T154) → lessc70_out_gg(0, T154)
lessc70_in_gg(s(T161), T162) → U91_gg(T161, T162, lessc78_in_gg(T161, T162))
lessc78_in_gg(0, s(T169)) → lessc78_out_gg(0, s(T169))
lessc78_in_gg(s(T176), s(T177)) → U89_gg(T176, T177, lessc78_in_gg(T176, T177))
U89_gg(T176, T177, lessc78_out_gg(T176, T177)) → lessc78_out_gg(s(T176), s(T177))
U91_gg(T161, T162, lessc78_out_gg(T161, T162)) → lessc70_out_gg(s(T161), T162)

The argument filtering Pi contains the following mapping:
[]  =  []
splitc12_in_aaaa(x1, x2, x3, x4)  =  splitc12_in_aaaa
U79_aaaa(x1, x2, x3, x4, x5)  =  U79_aaaa(x5)
splitc16_in_aaa(x1, x2, x3)  =  splitc16_in_aaa
splitc16_out_aaa(x1, x2, x3)  =  splitc16_out_aaa
U78_aaa(x1, x2, x3, x4, x5)  =  U78_aaa(x5)
splitc12_out_aaaa(x1, x2, x3, x4)  =  splitc12_out_aaaa
msc38_in_aa(x1, x2)  =  msc38_in_aa
msc38_out_aa(x1, x2)  =  msc38_out_aa
U84_aa(x1, x2, x3, x4, x5)  =  U84_aa(x5)
qc34_in_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  qc34_in_aaaaaaaa
U80_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U80_aaaaaaaa(x9)
U81_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U81_aaaaaaaa(x9)
U82_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U82_aaaaaaaa(x9)
U83_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U83_aaaaaaaa(x9)
mergec54_in_aaa(x1, x2, x3)  =  mergec54_in_aaa
mergec54_out_aaa(x1, x2, x3)  =  mergec54_out_aaa
U85_aaa(x1, x2, x3, x4, x5, x6)  =  U85_aaa(x6)
lessc70_in_aa(x1, x2)  =  lessc70_in_aa
lessc70_out_aa(x1, x2)  =  lessc70_out_aa(x1)
U91_aa(x1, x2, x3)  =  U91_aa(x3)
lessc78_in_aa(x1, x2)  =  lessc78_in_aa
lessc78_out_aa(x1, x2)  =  lessc78_out_aa(x1)
U89_aa(x1, x2, x3)  =  U89_aa(x3)
U86_aaa(x1, x2, x3, x4, x5, x6)  =  U86_aaa(x6)
U87_aaa(x1, x2, x3, x4, x5, x6)  =  U87_aaa(x6)
U88_aaa(x1, x2, x3, x4, x5, x6)  =  U88_aaa(x6)
qc34_out_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  qc34_out_aaaaaaaa
msc25_in_aaa(x1, x2, x3)  =  msc25_in_aaa
msc25_out_aaa(x1, x2, x3)  =  msc25_out_aaa
U90_aaa(x1, x2, x3, x4, x5)  =  U90_aaa(x5)
.(x1, x2)  =  .(x1, x2)
s(x1)  =  s(x1)
lessc70_in_ga(x1, x2)  =  lessc70_in_ga(x1)
0  =  0
lessc70_out_ga(x1, x2)  =  lessc70_out_ga(x1)
U91_ga(x1, x2, x3)  =  U91_ga(x1, x3)
lessc78_in_ga(x1, x2)  =  lessc78_in_ga(x1)
lessc78_out_ga(x1, x2)  =  lessc78_out_ga(x1)
U89_ga(x1, x2, x3)  =  U89_ga(x1, x3)
lessc70_in_gg(x1, x2)  =  lessc70_in_gg(x1, x2)
lessc70_out_gg(x1, x2)  =  lessc70_out_gg(x1, x2)
U91_gg(x1, x2, x3)  =  U91_gg(x1, x2, x3)
lessc78_in_gg(x1, x2)  =  lessc78_in_gg(x1, x2)
lessc78_out_gg(x1, x2)  =  lessc78_out_gg(x1, x2)
U89_gg(x1, x2, x3)  =  U89_gg(x1, x2, x3)
MERGE54_IN_AAA(x1, x2, x3)  =  MERGE54_IN_AAA
U15_AAA(x1, x2, x3, x4, x5, x6)  =  U15_AAA(x6)
U18_AAA(x1, x2, x3, x4, x5, x6)  =  U18_AAA(x6)

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:

MERGE54_IN_AAA(.(T139, T145), .(T146, T147), .(T139, X226)) → U15_AAA(T139, T145, T146, T147, X226, lessc70_in_aa(T139, T146))
U15_AAA(T139, T145, T146, T147, X226, lessc70_out_aa(T139, T146)) → MERGE54_IN_AAA(T145, .(T146, T147), X226)
MERGE54_IN_AAA(.(T202, T203), .(T196, T204), .(T196, X287)) → U18_AAA(T202, T203, T196, T204, X287, lessc78_in_aa(T196, T202))
U18_AAA(T202, T203, T196, T204, X287, lessc78_out_aa(T196, T202)) → MERGE54_IN_AAA(.(T202, T203), T204, X287)

The TRS R consists of the following rules:

lessc70_in_aa(0, T154) → lessc70_out_aa(0, T154)
lessc70_in_aa(s(T161), T162) → U91_aa(T161, T162, lessc78_in_aa(T161, T162))
lessc78_in_aa(0, s(T169)) → lessc78_out_aa(0, s(T169))
lessc78_in_aa(s(T176), s(T177)) → U89_aa(T176, T177, lessc78_in_aa(T176, T177))
U91_aa(T161, T162, lessc78_out_aa(T161, T162)) → lessc70_out_aa(s(T161), T162)
U89_aa(T176, T177, lessc78_out_aa(T176, T177)) → lessc78_out_aa(s(T176), s(T177))

The argument filtering Pi contains the following mapping:
lessc70_in_aa(x1, x2)  =  lessc70_in_aa
lessc70_out_aa(x1, x2)  =  lessc70_out_aa(x1)
U91_aa(x1, x2, x3)  =  U91_aa(x3)
lessc78_in_aa(x1, x2)  =  lessc78_in_aa
lessc78_out_aa(x1, x2)  =  lessc78_out_aa(x1)
U89_aa(x1, x2, x3)  =  U89_aa(x3)
.(x1, x2)  =  .(x1, x2)
s(x1)  =  s(x1)
0  =  0
MERGE54_IN_AAA(x1, x2, x3)  =  MERGE54_IN_AAA
U15_AAA(x1, x2, x3, x4, x5, x6)  =  U15_AAA(x6)
U18_AAA(x1, x2, x3, x4, x5, x6)  =  U18_AAA(x6)

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:

MERGE54_IN_AAAU15_AAA(lessc70_in_aa)
U15_AAA(lessc70_out_aa(T139)) → MERGE54_IN_AAA
MERGE54_IN_AAAU18_AAA(lessc78_in_aa)
U18_AAA(lessc78_out_aa(T196)) → MERGE54_IN_AAA

The TRS R consists of the following rules:

lessc70_in_aalessc70_out_aa(0)
lessc70_in_aaU91_aa(lessc78_in_aa)
lessc78_in_aalessc78_out_aa(0)
lessc78_in_aaU89_aa(lessc78_in_aa)
U91_aa(lessc78_out_aa(T161)) → lessc70_out_aa(s(T161))
U89_aa(lessc78_out_aa(T176)) → lessc78_out_aa(s(T176))

The set Q consists of the following terms:

lessc70_in_aa
lessc78_in_aa
U91_aa(x0)
U89_aa(x0)

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

(35) Narrowing (SOUND transformation)

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

MERGE54_IN_AAAU15_AAA(lessc70_out_aa(0))
MERGE54_IN_AAAU15_AAA(U91_aa(lessc78_in_aa))

(36) Obligation:

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

U15_AAA(lessc70_out_aa(T139)) → MERGE54_IN_AAA
MERGE54_IN_AAAU18_AAA(lessc78_in_aa)
U18_AAA(lessc78_out_aa(T196)) → MERGE54_IN_AAA
MERGE54_IN_AAAU15_AAA(lessc70_out_aa(0))
MERGE54_IN_AAAU15_AAA(U91_aa(lessc78_in_aa))

The TRS R consists of the following rules:

lessc70_in_aalessc70_out_aa(0)
lessc70_in_aaU91_aa(lessc78_in_aa)
lessc78_in_aalessc78_out_aa(0)
lessc78_in_aaU89_aa(lessc78_in_aa)
U91_aa(lessc78_out_aa(T161)) → lessc70_out_aa(s(T161))
U89_aa(lessc78_out_aa(T176)) → lessc78_out_aa(s(T176))

The set Q consists of the following terms:

lessc70_in_aa
lessc78_in_aa
U91_aa(x0)
U89_aa(x0)

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

(37) UsableRulesProof (EQUIVALENT transformation)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

(38) Obligation:

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

U15_AAA(lessc70_out_aa(T139)) → MERGE54_IN_AAA
MERGE54_IN_AAAU18_AAA(lessc78_in_aa)
U18_AAA(lessc78_out_aa(T196)) → MERGE54_IN_AAA
MERGE54_IN_AAAU15_AAA(lessc70_out_aa(0))
MERGE54_IN_AAAU15_AAA(U91_aa(lessc78_in_aa))

The TRS R consists of the following rules:

lessc78_in_aalessc78_out_aa(0)
lessc78_in_aaU89_aa(lessc78_in_aa)
U91_aa(lessc78_out_aa(T161)) → lessc70_out_aa(s(T161))
U89_aa(lessc78_out_aa(T176)) → lessc78_out_aa(s(T176))

The set Q consists of the following terms:

lessc70_in_aa
lessc78_in_aa
U91_aa(x0)
U89_aa(x0)

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

(39) QReductionProof (EQUIVALENT transformation)

We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

lessc70_in_aa

(40) Obligation:

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

U15_AAA(lessc70_out_aa(T139)) → MERGE54_IN_AAA
MERGE54_IN_AAAU18_AAA(lessc78_in_aa)
U18_AAA(lessc78_out_aa(T196)) → MERGE54_IN_AAA
MERGE54_IN_AAAU15_AAA(lessc70_out_aa(0))
MERGE54_IN_AAAU15_AAA(U91_aa(lessc78_in_aa))

The TRS R consists of the following rules:

lessc78_in_aalessc78_out_aa(0)
lessc78_in_aaU89_aa(lessc78_in_aa)
U91_aa(lessc78_out_aa(T161)) → lessc70_out_aa(s(T161))
U89_aa(lessc78_out_aa(T176)) → lessc78_out_aa(s(T176))

The set Q consists of the following terms:

lessc78_in_aa
U91_aa(x0)
U89_aa(x0)

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

(41) Narrowing (SOUND transformation)

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

MERGE54_IN_AAAU18_AAA(lessc78_out_aa(0))
MERGE54_IN_AAAU18_AAA(U89_aa(lessc78_in_aa))

(42) Obligation:

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

U15_AAA(lessc70_out_aa(T139)) → MERGE54_IN_AAA
U18_AAA(lessc78_out_aa(T196)) → MERGE54_IN_AAA
MERGE54_IN_AAAU15_AAA(lessc70_out_aa(0))
MERGE54_IN_AAAU15_AAA(U91_aa(lessc78_in_aa))
MERGE54_IN_AAAU18_AAA(lessc78_out_aa(0))
MERGE54_IN_AAAU18_AAA(U89_aa(lessc78_in_aa))

The TRS R consists of the following rules:

lessc78_in_aalessc78_out_aa(0)
lessc78_in_aaU89_aa(lessc78_in_aa)
U91_aa(lessc78_out_aa(T161)) → lessc70_out_aa(s(T161))
U89_aa(lessc78_out_aa(T176)) → lessc78_out_aa(s(T176))

The set Q consists of the following terms:

lessc78_in_aa
U91_aa(x0)
U89_aa(x0)

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

(43) 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 = MERGE54_IN_AAA evaluates to t =MERGE54_IN_AAA

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




Rewriting sequence

MERGE54_IN_AAAU15_AAA(lessc70_out_aa(0))
with rule MERGE54_IN_AAAU15_AAA(lessc70_out_aa(0)) at position [] and matcher [ ]

U15_AAA(lessc70_out_aa(0))MERGE54_IN_AAA
with rule U15_AAA(lessc70_out_aa(T139)) → MERGE54_IN_AAA

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.



(44) NO

(45) Obligation:

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

SPLIT16_IN_AAA(.(T49, T51), .(T49, X89), X90) → SPLIT16_IN_AAA(T51, X90, X89)

The TRS R consists of the following rules:

splitc12_in_aaaa(T42, T44, .(T42, X71), X72) → U79_aaaa(T42, T44, X71, X72, splitc16_in_aaa(T44, X72, X71))
splitc16_in_aaa([], [], []) → splitc16_out_aaa([], [], [])
splitc16_in_aaa(.(T49, T51), .(T49, X89), X90) → U78_aaa(T49, T51, X89, X90, splitc16_in_aaa(T51, X90, X89))
U78_aaa(T49, T51, X89, X90, splitc16_out_aaa(T51, X90, X89)) → splitc16_out_aaa(.(T49, T51), .(T49, X89), X90)
U79_aaaa(T42, T44, X71, X72, splitc16_out_aaa(T44, X72, X71)) → splitc12_out_aaaa(T42, T44, .(T42, X71), X72)
msc38_in_aa([], []) → msc38_out_aa([], [])
msc38_in_aa(.(T89, []), .(T89, [])) → msc38_out_aa(.(T89, []), .(T89, []))
msc38_in_aa(.(T99, .(T100, T101)), X172) → U84_aa(T99, T100, T101, X172, qc34_in_aaaaaaaa(T99, T100, T101, X168, X169, X170, X171, X172))
qc34_in_aaaaaaaa(T72, T73, T74, T78, T84, T106, T105, X127) → U80_aaaaaaaa(T72, T73, T74, T78, T84, T106, T105, X127, splitc12_in_aaaa(T72, .(T73, T74), T78, T84))
U80_aaaaaaaa(T72, T73, T74, T78, T84, T106, T105, X127, splitc12_out_aaaa(T72, .(T73, T74), T78, T84)) → U81_aaaaaaaa(T72, T73, T74, T78, T84, T106, T105, X127, msc38_in_aa(T78, T106))
U81_aaaaaaaa(T72, T73, T74, T78, T84, T106, T105, X127, msc38_out_aa(T78, T106)) → U82_aaaaaaaa(T72, T73, T74, T78, T84, T106, T105, X127, msc38_in_aa(T84, T105))
U82_aaaaaaaa(T72, T73, T74, T78, T84, T106, T105, X127, msc38_out_aa(T84, T105)) → U83_aaaaaaaa(T72, T73, T74, T78, T84, T106, T105, X127, mergec54_in_aaa(T106, T105, X127))
mergec54_in_aaa([], T113, T113) → mergec54_out_aaa([], T113, T113)
mergec54_in_aaa(T118, [], T118) → mergec54_out_aaa(T118, [], T118)
mergec54_in_aaa(.(T139, T145), .(T146, T147), .(T139, X226)) → U85_aaa(T139, T145, T146, T147, X226, lessc70_in_aa(T139, T146))
lessc70_in_aa(0, T154) → lessc70_out_aa(0, T154)
lessc70_in_aa(s(T161), T162) → U91_aa(T161, T162, lessc78_in_aa(T161, T162))
lessc78_in_aa(0, s(T169)) → lessc78_out_aa(0, s(T169))
lessc78_in_aa(s(T176), s(T177)) → U89_aa(T176, T177, lessc78_in_aa(T176, T177))
U89_aa(T176, T177, lessc78_out_aa(T176, T177)) → lessc78_out_aa(s(T176), s(T177))
U91_aa(T161, T162, lessc78_out_aa(T161, T162)) → lessc70_out_aa(s(T161), T162)
U85_aaa(T139, T145, T146, T147, X226, lessc70_out_aa(T139, T146)) → U86_aaa(T139, T145, T146, T147, X226, mergec54_in_aaa(T145, .(T146, T147), X226))
mergec54_in_aaa(.(T202, T203), .(T196, T204), .(T196, X287)) → U87_aaa(T202, T203, T196, T204, X287, lessc78_in_aa(T196, T202))
U87_aaa(T202, T203, T196, T204, X287, lessc78_out_aa(T196, T202)) → U88_aaa(T202, T203, T196, T204, X287, mergec54_in_aaa(.(T202, T203), T204, X287))
U88_aaa(T202, T203, T196, T204, X287, mergec54_out_aaa(.(T202, T203), T204, X287)) → mergec54_out_aaa(.(T202, T203), .(T196, T204), .(T196, X287))
U86_aaa(T139, T145, T146, T147, X226, mergec54_out_aaa(T145, .(T146, T147), X226)) → mergec54_out_aaa(.(T139, T145), .(T146, T147), .(T139, X226))
U83_aaaaaaaa(T72, T73, T74, T78, T84, T106, T105, X127, mergec54_out_aaa(T106, T105, X127)) → qc34_out_aaaaaaaa(T72, T73, T74, T78, T84, T106, T105, X127)
U84_aa(T99, T100, T101, X172, qc34_out_aaaaaaaa(T99, T100, T101, X168, X169, X170, X171, X172)) → msc38_out_aa(.(T99, .(T100, T101)), X172)
msc25_in_aaa(T62, [], .(T62, [])) → msc25_out_aaa(T62, [], .(T62, []))
msc25_in_aaa(T72, .(T73, T74), X127) → U90_aaa(T72, T73, T74, X127, qc34_in_aaaaaaaa(T72, T73, T74, X123, X124, X125, X126, X127))
U90_aaa(T72, T73, T74, X127, qc34_out_aaaaaaaa(T72, T73, T74, X123, X124, X125, X126, X127)) → msc25_out_aaa(T72, .(T73, T74), X127)
lessc70_in_ga(0, T154) → lessc70_out_ga(0, T154)
lessc70_in_ga(s(T161), T162) → U91_ga(T161, T162, lessc78_in_ga(T161, T162))
lessc78_in_ga(0, s(T169)) → lessc78_out_ga(0, s(T169))
lessc78_in_ga(s(T176), s(T177)) → U89_ga(T176, T177, lessc78_in_ga(T176, T177))
U89_ga(T176, T177, lessc78_out_ga(T176, T177)) → lessc78_out_ga(s(T176), s(T177))
U91_ga(T161, T162, lessc78_out_ga(T161, T162)) → lessc70_out_ga(s(T161), T162)
lessc70_in_gg(0, T154) → lessc70_out_gg(0, T154)
lessc70_in_gg(s(T161), T162) → U91_gg(T161, T162, lessc78_in_gg(T161, T162))
lessc78_in_gg(0, s(T169)) → lessc78_out_gg(0, s(T169))
lessc78_in_gg(s(T176), s(T177)) → U89_gg(T176, T177, lessc78_in_gg(T176, T177))
U89_gg(T176, T177, lessc78_out_gg(T176, T177)) → lessc78_out_gg(s(T176), s(T177))
U91_gg(T161, T162, lessc78_out_gg(T161, T162)) → lessc70_out_gg(s(T161), T162)

The argument filtering Pi contains the following mapping:
[]  =  []
splitc12_in_aaaa(x1, x2, x3, x4)  =  splitc12_in_aaaa
U79_aaaa(x1, x2, x3, x4, x5)  =  U79_aaaa(x5)
splitc16_in_aaa(x1, x2, x3)  =  splitc16_in_aaa
splitc16_out_aaa(x1, x2, x3)  =  splitc16_out_aaa
U78_aaa(x1, x2, x3, x4, x5)  =  U78_aaa(x5)
splitc12_out_aaaa(x1, x2, x3, x4)  =  splitc12_out_aaaa
msc38_in_aa(x1, x2)  =  msc38_in_aa
msc38_out_aa(x1, x2)  =  msc38_out_aa
U84_aa(x1, x2, x3, x4, x5)  =  U84_aa(x5)
qc34_in_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  qc34_in_aaaaaaaa
U80_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U80_aaaaaaaa(x9)
U81_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U81_aaaaaaaa(x9)
U82_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U82_aaaaaaaa(x9)
U83_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U83_aaaaaaaa(x9)
mergec54_in_aaa(x1, x2, x3)  =  mergec54_in_aaa
mergec54_out_aaa(x1, x2, x3)  =  mergec54_out_aaa
U85_aaa(x1, x2, x3, x4, x5, x6)  =  U85_aaa(x6)
lessc70_in_aa(x1, x2)  =  lessc70_in_aa
lessc70_out_aa(x1, x2)  =  lessc70_out_aa(x1)
U91_aa(x1, x2, x3)  =  U91_aa(x3)
lessc78_in_aa(x1, x2)  =  lessc78_in_aa
lessc78_out_aa(x1, x2)  =  lessc78_out_aa(x1)
U89_aa(x1, x2, x3)  =  U89_aa(x3)
U86_aaa(x1, x2, x3, x4, x5, x6)  =  U86_aaa(x6)
U87_aaa(x1, x2, x3, x4, x5, x6)  =  U87_aaa(x6)
U88_aaa(x1, x2, x3, x4, x5, x6)  =  U88_aaa(x6)
qc34_out_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  qc34_out_aaaaaaaa
msc25_in_aaa(x1, x2, x3)  =  msc25_in_aaa
msc25_out_aaa(x1, x2, x3)  =  msc25_out_aaa
U90_aaa(x1, x2, x3, x4, x5)  =  U90_aaa(x5)
.(x1, x2)  =  .(x1, x2)
s(x1)  =  s(x1)
lessc70_in_ga(x1, x2)  =  lessc70_in_ga(x1)
0  =  0
lessc70_out_ga(x1, x2)  =  lessc70_out_ga(x1)
U91_ga(x1, x2, x3)  =  U91_ga(x1, x3)
lessc78_in_ga(x1, x2)  =  lessc78_in_ga(x1)
lessc78_out_ga(x1, x2)  =  lessc78_out_ga(x1)
U89_ga(x1, x2, x3)  =  U89_ga(x1, x3)
lessc70_in_gg(x1, x2)  =  lessc70_in_gg(x1, x2)
lessc70_out_gg(x1, x2)  =  lessc70_out_gg(x1, x2)
U91_gg(x1, x2, x3)  =  U91_gg(x1, x2, x3)
lessc78_in_gg(x1, x2)  =  lessc78_in_gg(x1, x2)
lessc78_out_gg(x1, x2)  =  lessc78_out_gg(x1, x2)
U89_gg(x1, x2, x3)  =  U89_gg(x1, x2, x3)
SPLIT16_IN_AAA(x1, x2, x3)  =  SPLIT16_IN_AAA

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

(46) UsableRulesProof (EQUIVALENT transformation)

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

(47) Obligation:

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

SPLIT16_IN_AAA(.(T49, T51), .(T49, X89), X90) → SPLIT16_IN_AAA(T51, X90, X89)

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

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

(48) PiDPToQDPProof (SOUND transformation)

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

(49) Obligation:

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

SPLIT16_IN_AAASPLIT16_IN_AAA

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

(50) 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 = SPLIT16_IN_AAA evaluates to t =SPLIT16_IN_AAA

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 SPLIT16_IN_AAA to SPLIT16_IN_AAA.



(51) NO

(52) Obligation:

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

P34_IN_AAAAAAAA(T72, T73, T74, T78, T79, X125, X126, X127) → U4_AAAAAAAA(T72, T73, T74, T78, T79, X125, X126, X127, splitc12_in_aaaa(T72, .(T73, T74), T78, T79))
U4_AAAAAAAA(T72, T73, T74, T78, T79, X125, X126, X127, splitc12_out_aaaa(T72, .(T73, T74), T78, T79)) → MS38_IN_AA(T78, X125)
MS38_IN_AA(.(T99, .(T100, T101)), X172) → P34_IN_AAAAAAAA(T99, T100, T101, X168, X169, X170, X171, X172)
P34_IN_AAAAAAAA(T72, T73, T74, T78, T84, T83, X126, X127) → U6_AAAAAAAA(T72, T73, T74, T78, T84, T83, X126, X127, splitc12_in_aaaa(T72, .(T73, T74), T78, T84))
U6_AAAAAAAA(T72, T73, T74, T78, T84, T83, X126, X127, splitc12_out_aaaa(T72, .(T73, T74), T78, T84)) → U7_AAAAAAAA(T72, T73, T74, T78, T84, T83, X126, X127, msc38_in_aa(T78, T83))
U7_AAAAAAAA(T72, T73, T74, T78, T84, T83, X126, X127, msc38_out_aa(T78, T83)) → MS38_IN_AA(T84, X126)

The TRS R consists of the following rules:

splitc12_in_aaaa(T42, T44, .(T42, X71), X72) → U79_aaaa(T42, T44, X71, X72, splitc16_in_aaa(T44, X72, X71))
splitc16_in_aaa([], [], []) → splitc16_out_aaa([], [], [])
splitc16_in_aaa(.(T49, T51), .(T49, X89), X90) → U78_aaa(T49, T51, X89, X90, splitc16_in_aaa(T51, X90, X89))
U78_aaa(T49, T51, X89, X90, splitc16_out_aaa(T51, X90, X89)) → splitc16_out_aaa(.(T49, T51), .(T49, X89), X90)
U79_aaaa(T42, T44, X71, X72, splitc16_out_aaa(T44, X72, X71)) → splitc12_out_aaaa(T42, T44, .(T42, X71), X72)
msc38_in_aa([], []) → msc38_out_aa([], [])
msc38_in_aa(.(T89, []), .(T89, [])) → msc38_out_aa(.(T89, []), .(T89, []))
msc38_in_aa(.(T99, .(T100, T101)), X172) → U84_aa(T99, T100, T101, X172, qc34_in_aaaaaaaa(T99, T100, T101, X168, X169, X170, X171, X172))
qc34_in_aaaaaaaa(T72, T73, T74, T78, T84, T106, T105, X127) → U80_aaaaaaaa(T72, T73, T74, T78, T84, T106, T105, X127, splitc12_in_aaaa(T72, .(T73, T74), T78, T84))
U80_aaaaaaaa(T72, T73, T74, T78, T84, T106, T105, X127, splitc12_out_aaaa(T72, .(T73, T74), T78, T84)) → U81_aaaaaaaa(T72, T73, T74, T78, T84, T106, T105, X127, msc38_in_aa(T78, T106))
U81_aaaaaaaa(T72, T73, T74, T78, T84, T106, T105, X127, msc38_out_aa(T78, T106)) → U82_aaaaaaaa(T72, T73, T74, T78, T84, T106, T105, X127, msc38_in_aa(T84, T105))
U82_aaaaaaaa(T72, T73, T74, T78, T84, T106, T105, X127, msc38_out_aa(T84, T105)) → U83_aaaaaaaa(T72, T73, T74, T78, T84, T106, T105, X127, mergec54_in_aaa(T106, T105, X127))
mergec54_in_aaa([], T113, T113) → mergec54_out_aaa([], T113, T113)
mergec54_in_aaa(T118, [], T118) → mergec54_out_aaa(T118, [], T118)
mergec54_in_aaa(.(T139, T145), .(T146, T147), .(T139, X226)) → U85_aaa(T139, T145, T146, T147, X226, lessc70_in_aa(T139, T146))
lessc70_in_aa(0, T154) → lessc70_out_aa(0, T154)
lessc70_in_aa(s(T161), T162) → U91_aa(T161, T162, lessc78_in_aa(T161, T162))
lessc78_in_aa(0, s(T169)) → lessc78_out_aa(0, s(T169))
lessc78_in_aa(s(T176), s(T177)) → U89_aa(T176, T177, lessc78_in_aa(T176, T177))
U89_aa(T176, T177, lessc78_out_aa(T176, T177)) → lessc78_out_aa(s(T176), s(T177))
U91_aa(T161, T162, lessc78_out_aa(T161, T162)) → lessc70_out_aa(s(T161), T162)
U85_aaa(T139, T145, T146, T147, X226, lessc70_out_aa(T139, T146)) → U86_aaa(T139, T145, T146, T147, X226, mergec54_in_aaa(T145, .(T146, T147), X226))
mergec54_in_aaa(.(T202, T203), .(T196, T204), .(T196, X287)) → U87_aaa(T202, T203, T196, T204, X287, lessc78_in_aa(T196, T202))
U87_aaa(T202, T203, T196, T204, X287, lessc78_out_aa(T196, T202)) → U88_aaa(T202, T203, T196, T204, X287, mergec54_in_aaa(.(T202, T203), T204, X287))
U88_aaa(T202, T203, T196, T204, X287, mergec54_out_aaa(.(T202, T203), T204, X287)) → mergec54_out_aaa(.(T202, T203), .(T196, T204), .(T196, X287))
U86_aaa(T139, T145, T146, T147, X226, mergec54_out_aaa(T145, .(T146, T147), X226)) → mergec54_out_aaa(.(T139, T145), .(T146, T147), .(T139, X226))
U83_aaaaaaaa(T72, T73, T74, T78, T84, T106, T105, X127, mergec54_out_aaa(T106, T105, X127)) → qc34_out_aaaaaaaa(T72, T73, T74, T78, T84, T106, T105, X127)
U84_aa(T99, T100, T101, X172, qc34_out_aaaaaaaa(T99, T100, T101, X168, X169, X170, X171, X172)) → msc38_out_aa(.(T99, .(T100, T101)), X172)
msc25_in_aaa(T62, [], .(T62, [])) → msc25_out_aaa(T62, [], .(T62, []))
msc25_in_aaa(T72, .(T73, T74), X127) → U90_aaa(T72, T73, T74, X127, qc34_in_aaaaaaaa(T72, T73, T74, X123, X124, X125, X126, X127))
U90_aaa(T72, T73, T74, X127, qc34_out_aaaaaaaa(T72, T73, T74, X123, X124, X125, X126, X127)) → msc25_out_aaa(T72, .(T73, T74), X127)
lessc70_in_ga(0, T154) → lessc70_out_ga(0, T154)
lessc70_in_ga(s(T161), T162) → U91_ga(T161, T162, lessc78_in_ga(T161, T162))
lessc78_in_ga(0, s(T169)) → lessc78_out_ga(0, s(T169))
lessc78_in_ga(s(T176), s(T177)) → U89_ga(T176, T177, lessc78_in_ga(T176, T177))
U89_ga(T176, T177, lessc78_out_ga(T176, T177)) → lessc78_out_ga(s(T176), s(T177))
U91_ga(T161, T162, lessc78_out_ga(T161, T162)) → lessc70_out_ga(s(T161), T162)
lessc70_in_gg(0, T154) → lessc70_out_gg(0, T154)
lessc70_in_gg(s(T161), T162) → U91_gg(T161, T162, lessc78_in_gg(T161, T162))
lessc78_in_gg(0, s(T169)) → lessc78_out_gg(0, s(T169))
lessc78_in_gg(s(T176), s(T177)) → U89_gg(T176, T177, lessc78_in_gg(T176, T177))
U89_gg(T176, T177, lessc78_out_gg(T176, T177)) → lessc78_out_gg(s(T176), s(T177))
U91_gg(T161, T162, lessc78_out_gg(T161, T162)) → lessc70_out_gg(s(T161), T162)

The argument filtering Pi contains the following mapping:
[]  =  []
splitc12_in_aaaa(x1, x2, x3, x4)  =  splitc12_in_aaaa
U79_aaaa(x1, x2, x3, x4, x5)  =  U79_aaaa(x5)
splitc16_in_aaa(x1, x2, x3)  =  splitc16_in_aaa
splitc16_out_aaa(x1, x2, x3)  =  splitc16_out_aaa
U78_aaa(x1, x2, x3, x4, x5)  =  U78_aaa(x5)
splitc12_out_aaaa(x1, x2, x3, x4)  =  splitc12_out_aaaa
msc38_in_aa(x1, x2)  =  msc38_in_aa
msc38_out_aa(x1, x2)  =  msc38_out_aa
U84_aa(x1, x2, x3, x4, x5)  =  U84_aa(x5)
qc34_in_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  qc34_in_aaaaaaaa
U80_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U80_aaaaaaaa(x9)
U81_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U81_aaaaaaaa(x9)
U82_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U82_aaaaaaaa(x9)
U83_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U83_aaaaaaaa(x9)
mergec54_in_aaa(x1, x2, x3)  =  mergec54_in_aaa
mergec54_out_aaa(x1, x2, x3)  =  mergec54_out_aaa
U85_aaa(x1, x2, x3, x4, x5, x6)  =  U85_aaa(x6)
lessc70_in_aa(x1, x2)  =  lessc70_in_aa
lessc70_out_aa(x1, x2)  =  lessc70_out_aa(x1)
U91_aa(x1, x2, x3)  =  U91_aa(x3)
lessc78_in_aa(x1, x2)  =  lessc78_in_aa
lessc78_out_aa(x1, x2)  =  lessc78_out_aa(x1)
U89_aa(x1, x2, x3)  =  U89_aa(x3)
U86_aaa(x1, x2, x3, x4, x5, x6)  =  U86_aaa(x6)
U87_aaa(x1, x2, x3, x4, x5, x6)  =  U87_aaa(x6)
U88_aaa(x1, x2, x3, x4, x5, x6)  =  U88_aaa(x6)
qc34_out_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  qc34_out_aaaaaaaa
msc25_in_aaa(x1, x2, x3)  =  msc25_in_aaa
msc25_out_aaa(x1, x2, x3)  =  msc25_out_aaa
U90_aaa(x1, x2, x3, x4, x5)  =  U90_aaa(x5)
.(x1, x2)  =  .(x1, x2)
s(x1)  =  s(x1)
lessc70_in_ga(x1, x2)  =  lessc70_in_ga(x1)
0  =  0
lessc70_out_ga(x1, x2)  =  lessc70_out_ga(x1)
U91_ga(x1, x2, x3)  =  U91_ga(x1, x3)
lessc78_in_ga(x1, x2)  =  lessc78_in_ga(x1)
lessc78_out_ga(x1, x2)  =  lessc78_out_ga(x1)
U89_ga(x1, x2, x3)  =  U89_ga(x1, x3)
lessc70_in_gg(x1, x2)  =  lessc70_in_gg(x1, x2)
lessc70_out_gg(x1, x2)  =  lessc70_out_gg(x1, x2)
U91_gg(x1, x2, x3)  =  U91_gg(x1, x2, x3)
lessc78_in_gg(x1, x2)  =  lessc78_in_gg(x1, x2)
lessc78_out_gg(x1, x2)  =  lessc78_out_gg(x1, x2)
U89_gg(x1, x2, x3)  =  U89_gg(x1, x2, x3)
P34_IN_AAAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8)  =  P34_IN_AAAAAAAA
U4_AAAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U4_AAAAAAAA(x9)
MS38_IN_AA(x1, x2)  =  MS38_IN_AA
U6_AAAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U6_AAAAAAAA(x9)
U7_AAAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U7_AAAAAAAA(x9)

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

(53) UsableRulesProof (EQUIVALENT transformation)

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

(54) Obligation:

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

P34_IN_AAAAAAAA(T72, T73, T74, T78, T79, X125, X126, X127) → U4_AAAAAAAA(T72, T73, T74, T78, T79, X125, X126, X127, splitc12_in_aaaa(T72, .(T73, T74), T78, T79))
U4_AAAAAAAA(T72, T73, T74, T78, T79, X125, X126, X127, splitc12_out_aaaa(T72, .(T73, T74), T78, T79)) → MS38_IN_AA(T78, X125)
MS38_IN_AA(.(T99, .(T100, T101)), X172) → P34_IN_AAAAAAAA(T99, T100, T101, X168, X169, X170, X171, X172)
P34_IN_AAAAAAAA(T72, T73, T74, T78, T84, T83, X126, X127) → U6_AAAAAAAA(T72, T73, T74, T78, T84, T83, X126, X127, splitc12_in_aaaa(T72, .(T73, T74), T78, T84))
U6_AAAAAAAA(T72, T73, T74, T78, T84, T83, X126, X127, splitc12_out_aaaa(T72, .(T73, T74), T78, T84)) → U7_AAAAAAAA(T72, T73, T74, T78, T84, T83, X126, X127, msc38_in_aa(T78, T83))
U7_AAAAAAAA(T72, T73, T74, T78, T84, T83, X126, X127, msc38_out_aa(T78, T83)) → MS38_IN_AA(T84, X126)

The TRS R consists of the following rules:

splitc12_in_aaaa(T42, T44, .(T42, X71), X72) → U79_aaaa(T42, T44, X71, X72, splitc16_in_aaa(T44, X72, X71))
msc38_in_aa([], []) → msc38_out_aa([], [])
msc38_in_aa(.(T89, []), .(T89, [])) → msc38_out_aa(.(T89, []), .(T89, []))
msc38_in_aa(.(T99, .(T100, T101)), X172) → U84_aa(T99, T100, T101, X172, qc34_in_aaaaaaaa(T99, T100, T101, X168, X169, X170, X171, X172))
U79_aaaa(T42, T44, X71, X72, splitc16_out_aaa(T44, X72, X71)) → splitc12_out_aaaa(T42, T44, .(T42, X71), X72)
U84_aa(T99, T100, T101, X172, qc34_out_aaaaaaaa(T99, T100, T101, X168, X169, X170, X171, X172)) → msc38_out_aa(.(T99, .(T100, T101)), X172)
splitc16_in_aaa([], [], []) → splitc16_out_aaa([], [], [])
splitc16_in_aaa(.(T49, T51), .(T49, X89), X90) → U78_aaa(T49, T51, X89, X90, splitc16_in_aaa(T51, X90, X89))
qc34_in_aaaaaaaa(T72, T73, T74, T78, T84, T106, T105, X127) → U80_aaaaaaaa(T72, T73, T74, T78, T84, T106, T105, X127, splitc12_in_aaaa(T72, .(T73, T74), T78, T84))
U78_aaa(T49, T51, X89, X90, splitc16_out_aaa(T51, X90, X89)) → splitc16_out_aaa(.(T49, T51), .(T49, X89), X90)
U80_aaaaaaaa(T72, T73, T74, T78, T84, T106, T105, X127, splitc12_out_aaaa(T72, .(T73, T74), T78, T84)) → U81_aaaaaaaa(T72, T73, T74, T78, T84, T106, T105, X127, msc38_in_aa(T78, T106))
U81_aaaaaaaa(T72, T73, T74, T78, T84, T106, T105, X127, msc38_out_aa(T78, T106)) → U82_aaaaaaaa(T72, T73, T74, T78, T84, T106, T105, X127, msc38_in_aa(T84, T105))
U82_aaaaaaaa(T72, T73, T74, T78, T84, T106, T105, X127, msc38_out_aa(T84, T105)) → U83_aaaaaaaa(T72, T73, T74, T78, T84, T106, T105, X127, mergec54_in_aaa(T106, T105, X127))
U83_aaaaaaaa(T72, T73, T74, T78, T84, T106, T105, X127, mergec54_out_aaa(T106, T105, X127)) → qc34_out_aaaaaaaa(T72, T73, T74, T78, T84, T106, T105, X127)
mergec54_in_aaa([], T113, T113) → mergec54_out_aaa([], T113, T113)
mergec54_in_aaa(T118, [], T118) → mergec54_out_aaa(T118, [], T118)
mergec54_in_aaa(.(T139, T145), .(T146, T147), .(T139, X226)) → U85_aaa(T139, T145, T146, T147, X226, lessc70_in_aa(T139, T146))
mergec54_in_aaa(.(T202, T203), .(T196, T204), .(T196, X287)) → U87_aaa(T202, T203, T196, T204, X287, lessc78_in_aa(T196, T202))
U85_aaa(T139, T145, T146, T147, X226, lessc70_out_aa(T139, T146)) → U86_aaa(T139, T145, T146, T147, X226, mergec54_in_aaa(T145, .(T146, T147), X226))
U87_aaa(T202, T203, T196, T204, X287, lessc78_out_aa(T196, T202)) → U88_aaa(T202, T203, T196, T204, X287, mergec54_in_aaa(.(T202, T203), T204, X287))
lessc70_in_aa(0, T154) → lessc70_out_aa(0, T154)
lessc70_in_aa(s(T161), T162) → U91_aa(T161, T162, lessc78_in_aa(T161, T162))
U86_aaa(T139, T145, T146, T147, X226, mergec54_out_aaa(T145, .(T146, T147), X226)) → mergec54_out_aaa(.(T139, T145), .(T146, T147), .(T139, X226))
lessc78_in_aa(0, s(T169)) → lessc78_out_aa(0, s(T169))
lessc78_in_aa(s(T176), s(T177)) → U89_aa(T176, T177, lessc78_in_aa(T176, T177))
U88_aaa(T202, T203, T196, T204, X287, mergec54_out_aaa(.(T202, T203), T204, X287)) → mergec54_out_aaa(.(T202, T203), .(T196, T204), .(T196, X287))
U91_aa(T161, T162, lessc78_out_aa(T161, T162)) → lessc70_out_aa(s(T161), T162)
U89_aa(T176, T177, lessc78_out_aa(T176, T177)) → lessc78_out_aa(s(T176), s(T177))

The argument filtering Pi contains the following mapping:
[]  =  []
splitc12_in_aaaa(x1, x2, x3, x4)  =  splitc12_in_aaaa
U79_aaaa(x1, x2, x3, x4, x5)  =  U79_aaaa(x5)
splitc16_in_aaa(x1, x2, x3)  =  splitc16_in_aaa
splitc16_out_aaa(x1, x2, x3)  =  splitc16_out_aaa
U78_aaa(x1, x2, x3, x4, x5)  =  U78_aaa(x5)
splitc12_out_aaaa(x1, x2, x3, x4)  =  splitc12_out_aaaa
msc38_in_aa(x1, x2)  =  msc38_in_aa
msc38_out_aa(x1, x2)  =  msc38_out_aa
U84_aa(x1, x2, x3, x4, x5)  =  U84_aa(x5)
qc34_in_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  qc34_in_aaaaaaaa
U80_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U80_aaaaaaaa(x9)
U81_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U81_aaaaaaaa(x9)
U82_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U82_aaaaaaaa(x9)
U83_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U83_aaaaaaaa(x9)
mergec54_in_aaa(x1, x2, x3)  =  mergec54_in_aaa
mergec54_out_aaa(x1, x2, x3)  =  mergec54_out_aaa
U85_aaa(x1, x2, x3, x4, x5, x6)  =  U85_aaa(x6)
lessc70_in_aa(x1, x2)  =  lessc70_in_aa
lessc70_out_aa(x1, x2)  =  lessc70_out_aa(x1)
U91_aa(x1, x2, x3)  =  U91_aa(x3)
lessc78_in_aa(x1, x2)  =  lessc78_in_aa
lessc78_out_aa(x1, x2)  =  lessc78_out_aa(x1)
U89_aa(x1, x2, x3)  =  U89_aa(x3)
U86_aaa(x1, x2, x3, x4, x5, x6)  =  U86_aaa(x6)
U87_aaa(x1, x2, x3, x4, x5, x6)  =  U87_aaa(x6)
U88_aaa(x1, x2, x3, x4, x5, x6)  =  U88_aaa(x6)
qc34_out_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  qc34_out_aaaaaaaa
.(x1, x2)  =  .(x1, x2)
s(x1)  =  s(x1)
0  =  0
P34_IN_AAAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8)  =  P34_IN_AAAAAAAA
U4_AAAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U4_AAAAAAAA(x9)
MS38_IN_AA(x1, x2)  =  MS38_IN_AA
U6_AAAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U6_AAAAAAAA(x9)
U7_AAAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U7_AAAAAAAA(x9)

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

(55) PiDPToQDPProof (SOUND transformation)

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

(56) Obligation:

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

P34_IN_AAAAAAAAU4_AAAAAAAA(splitc12_in_aaaa)
U4_AAAAAAAA(splitc12_out_aaaa) → MS38_IN_AA
MS38_IN_AAP34_IN_AAAAAAAA
P34_IN_AAAAAAAAU6_AAAAAAAA(splitc12_in_aaaa)
U6_AAAAAAAA(splitc12_out_aaaa) → U7_AAAAAAAA(msc38_in_aa)
U7_AAAAAAAA(msc38_out_aa) → MS38_IN_AA

The TRS R consists of the following rules:

splitc12_in_aaaaU79_aaaa(splitc16_in_aaa)
msc38_in_aamsc38_out_aa
msc38_in_aaU84_aa(qc34_in_aaaaaaaa)
U79_aaaa(splitc16_out_aaa) → splitc12_out_aaaa
U84_aa(qc34_out_aaaaaaaa) → msc38_out_aa
splitc16_in_aaasplitc16_out_aaa
splitc16_in_aaaU78_aaa(splitc16_in_aaa)
qc34_in_aaaaaaaaU80_aaaaaaaa(splitc12_in_aaaa)
U78_aaa(splitc16_out_aaa) → splitc16_out_aaa
U80_aaaaaaaa(splitc12_out_aaaa) → U81_aaaaaaaa(msc38_in_aa)
U81_aaaaaaaa(msc38_out_aa) → U82_aaaaaaaa(msc38_in_aa)
U82_aaaaaaaa(msc38_out_aa) → U83_aaaaaaaa(mergec54_in_aaa)
U83_aaaaaaaa(mergec54_out_aaa) → qc34_out_aaaaaaaa
mergec54_in_aaamergec54_out_aaa
mergec54_in_aaaU85_aaa(lessc70_in_aa)
mergec54_in_aaaU87_aaa(lessc78_in_aa)
U85_aaa(lessc70_out_aa(T139)) → U86_aaa(mergec54_in_aaa)
U87_aaa(lessc78_out_aa(T196)) → U88_aaa(mergec54_in_aaa)
lessc70_in_aalessc70_out_aa(0)
lessc70_in_aaU91_aa(lessc78_in_aa)
U86_aaa(mergec54_out_aaa) → mergec54_out_aaa
lessc78_in_aalessc78_out_aa(0)
lessc78_in_aaU89_aa(lessc78_in_aa)
U88_aaa(mergec54_out_aaa) → mergec54_out_aaa
U91_aa(lessc78_out_aa(T161)) → lessc70_out_aa(s(T161))
U89_aa(lessc78_out_aa(T176)) → lessc78_out_aa(s(T176))

The set Q consists of the following terms:

splitc12_in_aaaa
msc38_in_aa
U79_aaaa(x0)
U84_aa(x0)
splitc16_in_aaa
qc34_in_aaaaaaaa
U78_aaa(x0)
U80_aaaaaaaa(x0)
U81_aaaaaaaa(x0)
U82_aaaaaaaa(x0)
U83_aaaaaaaa(x0)
mergec54_in_aaa
U85_aaa(x0)
U87_aaa(x0)
lessc70_in_aa
U86_aaa(x0)
lessc78_in_aa
U88_aaa(x0)
U91_aa(x0)
U89_aa(x0)

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

(57) Narrowing (SOUND transformation)

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

P34_IN_AAAAAAAAU4_AAAAAAAA(U79_aaaa(splitc16_in_aaa))

(58) Obligation:

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

U4_AAAAAAAA(splitc12_out_aaaa) → MS38_IN_AA
MS38_IN_AAP34_IN_AAAAAAAA
P34_IN_AAAAAAAAU6_AAAAAAAA(splitc12_in_aaaa)
U6_AAAAAAAA(splitc12_out_aaaa) → U7_AAAAAAAA(msc38_in_aa)
U7_AAAAAAAA(msc38_out_aa) → MS38_IN_AA
P34_IN_AAAAAAAAU4_AAAAAAAA(U79_aaaa(splitc16_in_aaa))

The TRS R consists of the following rules:

splitc12_in_aaaaU79_aaaa(splitc16_in_aaa)
msc38_in_aamsc38_out_aa
msc38_in_aaU84_aa(qc34_in_aaaaaaaa)
U79_aaaa(splitc16_out_aaa) → splitc12_out_aaaa
U84_aa(qc34_out_aaaaaaaa) → msc38_out_aa
splitc16_in_aaasplitc16_out_aaa
splitc16_in_aaaU78_aaa(splitc16_in_aaa)
qc34_in_aaaaaaaaU80_aaaaaaaa(splitc12_in_aaaa)
U78_aaa(splitc16_out_aaa) → splitc16_out_aaa
U80_aaaaaaaa(splitc12_out_aaaa) → U81_aaaaaaaa(msc38_in_aa)
U81_aaaaaaaa(msc38_out_aa) → U82_aaaaaaaa(msc38_in_aa)
U82_aaaaaaaa(msc38_out_aa) → U83_aaaaaaaa(mergec54_in_aaa)
U83_aaaaaaaa(mergec54_out_aaa) → qc34_out_aaaaaaaa
mergec54_in_aaamergec54_out_aaa
mergec54_in_aaaU85_aaa(lessc70_in_aa)
mergec54_in_aaaU87_aaa(lessc78_in_aa)
U85_aaa(lessc70_out_aa(T139)) → U86_aaa(mergec54_in_aaa)
U87_aaa(lessc78_out_aa(T196)) → U88_aaa(mergec54_in_aaa)
lessc70_in_aalessc70_out_aa(0)
lessc70_in_aaU91_aa(lessc78_in_aa)
U86_aaa(mergec54_out_aaa) → mergec54_out_aaa
lessc78_in_aalessc78_out_aa(0)
lessc78_in_aaU89_aa(lessc78_in_aa)
U88_aaa(mergec54_out_aaa) → mergec54_out_aaa
U91_aa(lessc78_out_aa(T161)) → lessc70_out_aa(s(T161))
U89_aa(lessc78_out_aa(T176)) → lessc78_out_aa(s(T176))

The set Q consists of the following terms:

splitc12_in_aaaa
msc38_in_aa
U79_aaaa(x0)
U84_aa(x0)
splitc16_in_aaa
qc34_in_aaaaaaaa
U78_aaa(x0)
U80_aaaaaaaa(x0)
U81_aaaaaaaa(x0)
U82_aaaaaaaa(x0)
U83_aaaaaaaa(x0)
mergec54_in_aaa
U85_aaa(x0)
U87_aaa(x0)
lessc70_in_aa
U86_aaa(x0)
lessc78_in_aa
U88_aaa(x0)
U91_aa(x0)
U89_aa(x0)

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

(59) Narrowing (SOUND transformation)

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

P34_IN_AAAAAAAAU6_AAAAAAAA(U79_aaaa(splitc16_in_aaa))

(60) Obligation:

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

U4_AAAAAAAA(splitc12_out_aaaa) → MS38_IN_AA
MS38_IN_AAP34_IN_AAAAAAAA
U6_AAAAAAAA(splitc12_out_aaaa) → U7_AAAAAAAA(msc38_in_aa)
U7_AAAAAAAA(msc38_out_aa) → MS38_IN_AA
P34_IN_AAAAAAAAU4_AAAAAAAA(U79_aaaa(splitc16_in_aaa))
P34_IN_AAAAAAAAU6_AAAAAAAA(U79_aaaa(splitc16_in_aaa))

The TRS R consists of the following rules:

splitc12_in_aaaaU79_aaaa(splitc16_in_aaa)
msc38_in_aamsc38_out_aa
msc38_in_aaU84_aa(qc34_in_aaaaaaaa)
U79_aaaa(splitc16_out_aaa) → splitc12_out_aaaa
U84_aa(qc34_out_aaaaaaaa) → msc38_out_aa
splitc16_in_aaasplitc16_out_aaa
splitc16_in_aaaU78_aaa(splitc16_in_aaa)
qc34_in_aaaaaaaaU80_aaaaaaaa(splitc12_in_aaaa)
U78_aaa(splitc16_out_aaa) → splitc16_out_aaa
U80_aaaaaaaa(splitc12_out_aaaa) → U81_aaaaaaaa(msc38_in_aa)
U81_aaaaaaaa(msc38_out_aa) → U82_aaaaaaaa(msc38_in_aa)
U82_aaaaaaaa(msc38_out_aa) → U83_aaaaaaaa(mergec54_in_aaa)
U83_aaaaaaaa(mergec54_out_aaa) → qc34_out_aaaaaaaa
mergec54_in_aaamergec54_out_aaa
mergec54_in_aaaU85_aaa(lessc70_in_aa)
mergec54_in_aaaU87_aaa(lessc78_in_aa)
U85_aaa(lessc70_out_aa(T139)) → U86_aaa(mergec54_in_aaa)
U87_aaa(lessc78_out_aa(T196)) → U88_aaa(mergec54_in_aaa)
lessc70_in_aalessc70_out_aa(0)
lessc70_in_aaU91_aa(lessc78_in_aa)
U86_aaa(mergec54_out_aaa) → mergec54_out_aaa
lessc78_in_aalessc78_out_aa(0)
lessc78_in_aaU89_aa(lessc78_in_aa)
U88_aaa(mergec54_out_aaa) → mergec54_out_aaa
U91_aa(lessc78_out_aa(T161)) → lessc70_out_aa(s(T161))
U89_aa(lessc78_out_aa(T176)) → lessc78_out_aa(s(T176))

The set Q consists of the following terms:

splitc12_in_aaaa
msc38_in_aa
U79_aaaa(x0)
U84_aa(x0)
splitc16_in_aaa
qc34_in_aaaaaaaa
U78_aaa(x0)
U80_aaaaaaaa(x0)
U81_aaaaaaaa(x0)
U82_aaaaaaaa(x0)
U83_aaaaaaaa(x0)
mergec54_in_aaa
U85_aaa(x0)
U87_aaa(x0)
lessc70_in_aa
U86_aaa(x0)
lessc78_in_aa
U88_aaa(x0)
U91_aa(x0)
U89_aa(x0)

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

(61) Narrowing (SOUND transformation)

By narrowing [LPAR04] the rule U6_AAAAAAAA(splitc12_out_aaaa) → U7_AAAAAAAA(msc38_in_aa) at position [0] we obtained the following new rules [LPAR04]:

U6_AAAAAAAA(splitc12_out_aaaa) → U7_AAAAAAAA(msc38_out_aa)
U6_AAAAAAAA(splitc12_out_aaaa) → U7_AAAAAAAA(U84_aa(qc34_in_aaaaaaaa))

(62) Obligation:

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

U4_AAAAAAAA(splitc12_out_aaaa) → MS38_IN_AA
MS38_IN_AAP34_IN_AAAAAAAA
U7_AAAAAAAA(msc38_out_aa) → MS38_IN_AA
P34_IN_AAAAAAAAU4_AAAAAAAA(U79_aaaa(splitc16_in_aaa))
P34_IN_AAAAAAAAU6_AAAAAAAA(U79_aaaa(splitc16_in_aaa))
U6_AAAAAAAA(splitc12_out_aaaa) → U7_AAAAAAAA(msc38_out_aa)
U6_AAAAAAAA(splitc12_out_aaaa) → U7_AAAAAAAA(U84_aa(qc34_in_aaaaaaaa))

The TRS R consists of the following rules:

splitc12_in_aaaaU79_aaaa(splitc16_in_aaa)
msc38_in_aamsc38_out_aa
msc38_in_aaU84_aa(qc34_in_aaaaaaaa)
U79_aaaa(splitc16_out_aaa) → splitc12_out_aaaa
U84_aa(qc34_out_aaaaaaaa) → msc38_out_aa
splitc16_in_aaasplitc16_out_aaa
splitc16_in_aaaU78_aaa(splitc16_in_aaa)
qc34_in_aaaaaaaaU80_aaaaaaaa(splitc12_in_aaaa)
U78_aaa(splitc16_out_aaa) → splitc16_out_aaa
U80_aaaaaaaa(splitc12_out_aaaa) → U81_aaaaaaaa(msc38_in_aa)
U81_aaaaaaaa(msc38_out_aa) → U82_aaaaaaaa(msc38_in_aa)
U82_aaaaaaaa(msc38_out_aa) → U83_aaaaaaaa(mergec54_in_aaa)
U83_aaaaaaaa(mergec54_out_aaa) → qc34_out_aaaaaaaa
mergec54_in_aaamergec54_out_aaa
mergec54_in_aaaU85_aaa(lessc70_in_aa)
mergec54_in_aaaU87_aaa(lessc78_in_aa)
U85_aaa(lessc70_out_aa(T139)) → U86_aaa(mergec54_in_aaa)
U87_aaa(lessc78_out_aa(T196)) → U88_aaa(mergec54_in_aaa)
lessc70_in_aalessc70_out_aa(0)
lessc70_in_aaU91_aa(lessc78_in_aa)
U86_aaa(mergec54_out_aaa) → mergec54_out_aaa
lessc78_in_aalessc78_out_aa(0)
lessc78_in_aaU89_aa(lessc78_in_aa)
U88_aaa(mergec54_out_aaa) → mergec54_out_aaa
U91_aa(lessc78_out_aa(T161)) → lessc70_out_aa(s(T161))
U89_aa(lessc78_out_aa(T176)) → lessc78_out_aa(s(T176))

The set Q consists of the following terms:

splitc12_in_aaaa
msc38_in_aa
U79_aaaa(x0)
U84_aa(x0)
splitc16_in_aaa
qc34_in_aaaaaaaa
U78_aaa(x0)
U80_aaaaaaaa(x0)
U81_aaaaaaaa(x0)
U82_aaaaaaaa(x0)
U83_aaaaaaaa(x0)
mergec54_in_aaa
U85_aaa(x0)
U87_aaa(x0)
lessc70_in_aa
U86_aaa(x0)
lessc78_in_aa
U88_aaa(x0)
U91_aa(x0)
U89_aa(x0)

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

(63) 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 = U4_AAAAAAAA(U79_aaaa(splitc16_in_aaa)) evaluates to t =U4_AAAAAAAA(U79_aaaa(splitc16_in_aaa))

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




Rewriting sequence

U4_AAAAAAAA(U79_aaaa(splitc16_in_aaa))U4_AAAAAAAA(U79_aaaa(splitc16_out_aaa))
with rule splitc16_in_aaasplitc16_out_aaa at position [0,0] and matcher [ ]

U4_AAAAAAAA(U79_aaaa(splitc16_out_aaa))U4_AAAAAAAA(splitc12_out_aaaa)
with rule U79_aaaa(splitc16_out_aaa) → splitc12_out_aaaa at position [0] and matcher [ ]

U4_AAAAAAAA(splitc12_out_aaaa)MS38_IN_AA
with rule U4_AAAAAAAA(splitc12_out_aaaa) → MS38_IN_AA at position [] and matcher [ ]

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

P34_IN_AAAAAAAAU4_AAAAAAAA(U79_aaaa(splitc16_in_aaa))
with rule P34_IN_AAAAAAAAU4_AAAAAAAA(U79_aaaa(splitc16_in_aaa))

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.



(64) NO