(0) Obligation:

Clauses:

qsort([], []).
qsort(.(H, L), S) :- ','(split(L, H, A, B), ','(qsort(A, A1), ','(qsort(B, B1), append(A1, .(H, B1), S)))).
split([], Y, [], []).
split(.(X, Xs), Y, .(X, Ls), Bs) :- ','(le(X, Y), split(Xs, Y, Ls, Bs)).
split(.(X, Xs), Y, Ls, .(X, Bs)) :- ','(gt(X, Y), split(Xs, Y, Ls, Bs)).
append([], L, L).
append(.(H, L1), L2, .(H, L3)) :- append(L1, L2, L3).
gt(s(X), s(Y)) :- gt(X, Y).
gt(s(X), 0).
le(s(X), s(Y)) :- le(X, Y).
le(0, s(Y)).
le(0, 0).

Queries:

qsort(g,a).

(1) PrologToDTProblemTransformerProof (SOUND transformation)

Built DT problem from termination graph.

(2) Obligation:

Triples:

append23(.(T45, T46), T47, T48, .(T45, T50)) :- append23(T46, T47, T48, T50).
le36(s(T82), s(T83)) :- le36(T82, T83).
split51(.(T114, T115), T116, .(T114, X167), X168) :- le36(T114, T116).
split51(.(T114, T115), T116, .(T114, X167), X168) :- ','(lec36(T114, T116), split51(T115, T116, X167, X168)).
split51(.(T129, T130), T131, X199, .(T129, X200)) :- gt67(T129, T131).
split51(.(T129, T130), T131, X199, .(T129, X200)) :- ','(gtc67(T129, T131), split51(T130, T131, X199, X200)).
gt67(s(T144), s(T145)) :- gt67(T144, T145).
qsort79(.(T163, T164), X265) :- split51(T164, T163, X261, X262).
qsort79(.(T163, T164), X265) :- ','(splitc51(T164, T163, T167, T168), qsort79(T167, X263)).
qsort79(.(T163, T164), X265) :- ','(splitc51(T164, T163, T167, T168), ','(qsortc79(T167, T171), qsort79(T168, X264))).
qsort79(.(T163, T164), X265) :- ','(splitc51(T164, T163, T167, T168), ','(qsortc79(T167, T171), ','(qsortc79(T168, T172), append94(T171, T163, T172, X265)))).
append94(.(T195, T196), T197, T198, .(T195, X295)) :- append94(T196, T197, T198, X295).
p78(T94, X13, T155, T69, T9) :- qsort79(T94, X13).
p78(T94, T158, T155, T69, T9) :- ','(qsortc79(T94, T158), append23(T155, T69, T158, T9)).
qsort1(.(T14, []), T9) :- qsort14(X12).
qsort1(.(T14, []), T9) :- ','(qsortc14(T17), qsort14(X13)).
qsort1(.(T14, []), T9) :- ','(qsortc14(T17), ','(qsortc14(T20), append23(T17, T14, T20, T9))).
qsort1(.(T69, .(T67, T68)), T9) :- le36(T67, T69).
qsort1(.(T69, .(T67, T68)), T9) :- ','(lec36(T67, T69), split51(T68, T69, X93, X94)).
qsort1(.(T69, .(T67, T68)), T9) :- ','(lec36(T67, T69), ','(splitc51(T68, T69, T93, T94), qsort1(.(T67, T93), X12))).
qsort1(.(T69, .(T67, T68)), T9) :- ','(lec36(T67, T69), ','(splitc51(T68, T69, T93, T94), ','(qsortc1(.(T67, T93), T155), p78(T94, X13, T155, T69, T9)))).
qsort1(.(T215, .(T213, T214)), T9) :- gt67(T213, T215).
qsort1(.(T215, .(T213, T214)), T9) :- ','(gtc67(T213, T215), split51(T214, T215, X323, X324)).
qsort1(.(T215, .(T213, T214)), T9) :- ','(gtc67(T213, T215), ','(splitc51(T214, T215, T222, T223), qsort79(T222, X12))).
qsort1(.(T215, .(T213, T214)), T9) :- ','(gtc67(T213, T215), ','(splitc51(T214, T215, T222, T223), ','(qsortc79(T222, T226), p78(.(T213, T223), X13, T226, T215, T9)))).

Clauses:

qsortc14([]).
appendc23([], T33, T34, .(T33, T34)).
appendc23(.(T45, T46), T47, T48, .(T45, T50)) :- appendc23(T46, T47, T48, T50).
lec36(s(T82), s(T83)) :- lec36(T82, T83).
lec36(0, s(T90)).
lec36(0, 0).
splitc51([], T101, [], []).
splitc51(.(T114, T115), T116, .(T114, X167), X168) :- ','(lec36(T114, T116), splitc51(T115, T116, X167, X168)).
splitc51(.(T129, T130), T131, X199, .(T129, X200)) :- ','(gtc67(T129, T131), splitc51(T130, T131, X199, X200)).
gtc67(s(T144), s(T145)) :- gtc67(T144, T145).
gtc67(s(T150), 0).
qsortc1([], []).
qsortc1(.(T14, []), T9) :- ','(qsortc14(T17), ','(qsortc14(T20), appendc23(T17, T14, T20, T9))).
qsortc1(.(T69, .(T67, T68)), T9) :- ','(lec36(T67, T69), ','(splitc51(T68, T69, T93, T94), ','(qsortc1(.(T67, T93), T155), qc78(T94, X13, T155, T69, T9)))).
qsortc1(.(T215, .(T213, T214)), T9) :- ','(gtc67(T213, T215), ','(splitc51(T214, T215, T222, T223), ','(qsortc79(T222, T226), qc78(.(T213, T223), X13, T226, T215, T9)))).
qsortc79([], []).
qsortc79(.(T163, T164), X265) :- ','(splitc51(T164, T163, T167, T168), ','(qsortc79(T167, T171), ','(qsortc79(T168, T172), appendc94(T171, T163, T172, X265)))).
appendc94([], T185, T186, .(T185, T186)).
appendc94(.(T195, T196), T197, T198, .(T195, X295)) :- appendc94(T196, T197, T198, X295).
qc78(T94, T158, T155, T69, T9) :- ','(qsortc79(T94, T158), appendc23(T155, T69, T158, T9)).

Afs:

qsort1(x1, x2)  =  qsort1(x1)

(3) UndefinedPredicateInTriplesTransformerProof (SOUND transformation)

Deleted triples and predicates having undefined goals [UNKNOWN].

(4) Obligation:

Triples:

append23(.(T45, T46), T47, T48, .(T45, T50)) :- append23(T46, T47, T48, T50).
le36(s(T82), s(T83)) :- le36(T82, T83).
split51(.(T114, T115), T116, .(T114, X167), X168) :- le36(T114, T116).
split51(.(T114, T115), T116, .(T114, X167), X168) :- ','(lec36(T114, T116), split51(T115, T116, X167, X168)).
split51(.(T129, T130), T131, X199, .(T129, X200)) :- gt67(T129, T131).
split51(.(T129, T130), T131, X199, .(T129, X200)) :- ','(gtc67(T129, T131), split51(T130, T131, X199, X200)).
gt67(s(T144), s(T145)) :- gt67(T144, T145).
qsort79(.(T163, T164), X265) :- split51(T164, T163, X261, X262).
qsort79(.(T163, T164), X265) :- ','(splitc51(T164, T163, T167, T168), qsort79(T167, X263)).
qsort79(.(T163, T164), X265) :- ','(splitc51(T164, T163, T167, T168), ','(qsortc79(T167, T171), qsort79(T168, X264))).
qsort79(.(T163, T164), X265) :- ','(splitc51(T164, T163, T167, T168), ','(qsortc79(T167, T171), ','(qsortc79(T168, T172), append94(T171, T163, T172, X265)))).
append94(.(T195, T196), T197, T198, .(T195, X295)) :- append94(T196, T197, T198, X295).
p78(T94, X13, T155, T69, T9) :- qsort79(T94, X13).
p78(T94, T158, T155, T69, T9) :- ','(qsortc79(T94, T158), append23(T155, T69, T158, T9)).
qsort1(.(T14, []), T9) :- ','(qsortc14(T17), ','(qsortc14(T20), append23(T17, T14, T20, T9))).
qsort1(.(T69, .(T67, T68)), T9) :- le36(T67, T69).
qsort1(.(T69, .(T67, T68)), T9) :- ','(lec36(T67, T69), split51(T68, T69, X93, X94)).
qsort1(.(T69, .(T67, T68)), T9) :- ','(lec36(T67, T69), ','(splitc51(T68, T69, T93, T94), qsort1(.(T67, T93), X12))).
qsort1(.(T69, .(T67, T68)), T9) :- ','(lec36(T67, T69), ','(splitc51(T68, T69, T93, T94), ','(qsortc1(.(T67, T93), T155), p78(T94, X13, T155, T69, T9)))).
qsort1(.(T215, .(T213, T214)), T9) :- gt67(T213, T215).
qsort1(.(T215, .(T213, T214)), T9) :- ','(gtc67(T213, T215), split51(T214, T215, X323, X324)).
qsort1(.(T215, .(T213, T214)), T9) :- ','(gtc67(T213, T215), ','(splitc51(T214, T215, T222, T223), qsort79(T222, X12))).
qsort1(.(T215, .(T213, T214)), T9) :- ','(gtc67(T213, T215), ','(splitc51(T214, T215, T222, T223), ','(qsortc79(T222, T226), p78(.(T213, T223), X13, T226, T215, T9)))).

Clauses:

qsortc14([]).
appendc23([], T33, T34, .(T33, T34)).
appendc23(.(T45, T46), T47, T48, .(T45, T50)) :- appendc23(T46, T47, T48, T50).
lec36(s(T82), s(T83)) :- lec36(T82, T83).
lec36(0, s(T90)).
lec36(0, 0).
splitc51([], T101, [], []).
splitc51(.(T114, T115), T116, .(T114, X167), X168) :- ','(lec36(T114, T116), splitc51(T115, T116, X167, X168)).
splitc51(.(T129, T130), T131, X199, .(T129, X200)) :- ','(gtc67(T129, T131), splitc51(T130, T131, X199, X200)).
gtc67(s(T144), s(T145)) :- gtc67(T144, T145).
gtc67(s(T150), 0).
qsortc1([], []).
qsortc1(.(T14, []), T9) :- ','(qsortc14(T17), ','(qsortc14(T20), appendc23(T17, T14, T20, T9))).
qsortc1(.(T69, .(T67, T68)), T9) :- ','(lec36(T67, T69), ','(splitc51(T68, T69, T93, T94), ','(qsortc1(.(T67, T93), T155), qc78(T94, X13, T155, T69, T9)))).
qsortc1(.(T215, .(T213, T214)), T9) :- ','(gtc67(T213, T215), ','(splitc51(T214, T215, T222, T223), ','(qsortc79(T222, T226), qc78(.(T213, T223), X13, T226, T215, T9)))).
qsortc79([], []).
qsortc79(.(T163, T164), X265) :- ','(splitc51(T164, T163, T167, T168), ','(qsortc79(T167, T171), ','(qsortc79(T168, T172), appendc94(T171, T163, T172, X265)))).
appendc94([], T185, T186, .(T185, T186)).
appendc94(.(T195, T196), T197, T198, .(T195, X295)) :- appendc94(T196, T197, T198, X295).
qc78(T94, T158, T155, T69, T9) :- ','(qsortc79(T94, T158), appendc23(T155, T69, T158, T9)).

Afs:

qsort1(x1, x2)  =  qsort1(x1)

(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:
qsort1_in: (b,f)
append23_in: (b,b,b,f)
le36_in: (b,b)
lec36_in: (b,b)
split51_in: (b,b,f,f)
gt67_in: (b,b)
gtc67_in: (b,b)
splitc51_in: (b,b,f,f)
qsort79_in: (b,f)
qsortc79_in: (b,f)
appendc94_in: (b,b,b,f)
append94_in: (b,b,b,f)
p78_in: (b,f,b,b,f)
qsortc1_in: (b,f)
appendc23_in: (b,b,b,f)
qc78_in: (b,f,b,b,f)
Transforming TRIPLES into the following Term Rewriting System:
Pi DP problem:
The TRS P consists of the following rules:

QSORT1_IN_GA(.(T14, []), T9) → U21_GA(T14, T9, qsortc14_in_a(T17))
U21_GA(T14, T9, qsortc14_out_a(T17)) → U22_GA(T14, T9, T17, qsortc14_in_a(T20))
U22_GA(T14, T9, T17, qsortc14_out_a(T20)) → U23_GA(T14, T9, append23_in_ggga(T17, T14, T20, T9))
U22_GA(T14, T9, T17, qsortc14_out_a(T20)) → APPEND23_IN_GGGA(T17, T14, T20, T9)
APPEND23_IN_GGGA(.(T45, T46), T47, T48, .(T45, T50)) → U1_GGGA(T45, T46, T47, T48, T50, append23_in_ggga(T46, T47, T48, T50))
APPEND23_IN_GGGA(.(T45, T46), T47, T48, .(T45, T50)) → APPEND23_IN_GGGA(T46, T47, T48, T50)
QSORT1_IN_GA(.(T69, .(T67, T68)), T9) → U24_GA(T69, T67, T68, T9, le36_in_gg(T67, T69))
QSORT1_IN_GA(.(T69, .(T67, T68)), T9) → LE36_IN_GG(T67, T69)
LE36_IN_GG(s(T82), s(T83)) → U2_GG(T82, T83, le36_in_gg(T82, T83))
LE36_IN_GG(s(T82), s(T83)) → LE36_IN_GG(T82, T83)
QSORT1_IN_GA(.(T69, .(T67, T68)), T9) → U25_GA(T69, T67, T68, T9, lec36_in_gg(T67, T69))
U25_GA(T69, T67, T68, T9, lec36_out_gg(T67, T69)) → U26_GA(T69, T67, T68, T9, split51_in_ggaa(T68, T69, X93, X94))
U25_GA(T69, T67, T68, T9, lec36_out_gg(T67, T69)) → SPLIT51_IN_GGAA(T68, T69, X93, X94)
SPLIT51_IN_GGAA(.(T114, T115), T116, .(T114, X167), X168) → U3_GGAA(T114, T115, T116, X167, X168, le36_in_gg(T114, T116))
SPLIT51_IN_GGAA(.(T114, T115), T116, .(T114, X167), X168) → LE36_IN_GG(T114, T116)
SPLIT51_IN_GGAA(.(T114, T115), T116, .(T114, X167), X168) → U4_GGAA(T114, T115, T116, X167, X168, lec36_in_gg(T114, T116))
U4_GGAA(T114, T115, T116, X167, X168, lec36_out_gg(T114, T116)) → U5_GGAA(T114, T115, T116, X167, X168, split51_in_ggaa(T115, T116, X167, X168))
U4_GGAA(T114, T115, T116, X167, X168, lec36_out_gg(T114, T116)) → SPLIT51_IN_GGAA(T115, T116, X167, X168)
SPLIT51_IN_GGAA(.(T129, T130), T131, X199, .(T129, X200)) → U6_GGAA(T129, T130, T131, X199, X200, gt67_in_gg(T129, T131))
SPLIT51_IN_GGAA(.(T129, T130), T131, X199, .(T129, X200)) → GT67_IN_GG(T129, T131)
GT67_IN_GG(s(T144), s(T145)) → U9_GG(T144, T145, gt67_in_gg(T144, T145))
GT67_IN_GG(s(T144), s(T145)) → GT67_IN_GG(T144, T145)
SPLIT51_IN_GGAA(.(T129, T130), T131, X199, .(T129, X200)) → U7_GGAA(T129, T130, T131, X199, X200, gtc67_in_gg(T129, T131))
U7_GGAA(T129, T130, T131, X199, X200, gtc67_out_gg(T129, T131)) → U8_GGAA(T129, T130, T131, X199, X200, split51_in_ggaa(T130, T131, X199, X200))
U7_GGAA(T129, T130, T131, X199, X200, gtc67_out_gg(T129, T131)) → SPLIT51_IN_GGAA(T130, T131, X199, X200)
U25_GA(T69, T67, T68, T9, lec36_out_gg(T67, T69)) → U27_GA(T69, T67, T68, T9, splitc51_in_ggaa(T68, T69, T93, T94))
U27_GA(T69, T67, T68, T9, splitc51_out_ggaa(T68, T69, T93, T94)) → U28_GA(T69, T67, T68, T9, qsort1_in_ga(.(T67, T93), X12))
U27_GA(T69, T67, T68, T9, splitc51_out_ggaa(T68, T69, T93, T94)) → QSORT1_IN_GA(.(T67, T93), X12)
QSORT1_IN_GA(.(T215, .(T213, T214)), T9) → U31_GA(T215, T213, T214, T9, gt67_in_gg(T213, T215))
QSORT1_IN_GA(.(T215, .(T213, T214)), T9) → GT67_IN_GG(T213, T215)
QSORT1_IN_GA(.(T215, .(T213, T214)), T9) → U32_GA(T215, T213, T214, T9, gtc67_in_gg(T213, T215))
U32_GA(T215, T213, T214, T9, gtc67_out_gg(T213, T215)) → U33_GA(T215, T213, T214, T9, split51_in_ggaa(T214, T215, X323, X324))
U32_GA(T215, T213, T214, T9, gtc67_out_gg(T213, T215)) → SPLIT51_IN_GGAA(T214, T215, X323, X324)
U32_GA(T215, T213, T214, T9, gtc67_out_gg(T213, T215)) → U34_GA(T215, T213, T214, T9, splitc51_in_ggaa(T214, T215, T222, T223))
U34_GA(T215, T213, T214, T9, splitc51_out_ggaa(T214, T215, T222, T223)) → U35_GA(T215, T213, T214, T9, qsort79_in_ga(T222, X12))
U34_GA(T215, T213, T214, T9, splitc51_out_ggaa(T214, T215, T222, T223)) → QSORT79_IN_GA(T222, X12)
QSORT79_IN_GA(.(T163, T164), X265) → U10_GA(T163, T164, X265, split51_in_ggaa(T164, T163, X261, X262))
QSORT79_IN_GA(.(T163, T164), X265) → SPLIT51_IN_GGAA(T164, T163, X261, X262)
QSORT79_IN_GA(.(T163, T164), X265) → U11_GA(T163, T164, X265, splitc51_in_ggaa(T164, T163, T167, T168))
U11_GA(T163, T164, X265, splitc51_out_ggaa(T164, T163, T167, T168)) → U12_GA(T163, T164, X265, qsort79_in_ga(T167, X263))
U11_GA(T163, T164, X265, splitc51_out_ggaa(T164, T163, T167, T168)) → QSORT79_IN_GA(T167, X263)
U11_GA(T163, T164, X265, splitc51_out_ggaa(T164, T163, T167, T168)) → U13_GA(T163, T164, X265, T168, qsortc79_in_ga(T167, T171))
U13_GA(T163, T164, X265, T168, qsortc79_out_ga(T167, T171)) → U14_GA(T163, T164, X265, qsort79_in_ga(T168, X264))
U13_GA(T163, T164, X265, T168, qsortc79_out_ga(T167, T171)) → QSORT79_IN_GA(T168, X264)
U13_GA(T163, T164, X265, T168, qsortc79_out_ga(T167, T171)) → U15_GA(T163, T164, X265, T171, qsortc79_in_ga(T168, T172))
U15_GA(T163, T164, X265, T171, qsortc79_out_ga(T168, T172)) → U16_GA(T163, T164, X265, append94_in_ggga(T171, T163, T172, X265))
U15_GA(T163, T164, X265, T171, qsortc79_out_ga(T168, T172)) → APPEND94_IN_GGGA(T171, T163, T172, X265)
APPEND94_IN_GGGA(.(T195, T196), T197, T198, .(T195, X295)) → U17_GGGA(T195, T196, T197, T198, X295, append94_in_ggga(T196, T197, T198, X295))
APPEND94_IN_GGGA(.(T195, T196), T197, T198, .(T195, X295)) → APPEND94_IN_GGGA(T196, T197, T198, X295)
U34_GA(T215, T213, T214, T9, splitc51_out_ggaa(T214, T215, T222, T223)) → U36_GA(T215, T213, T214, T9, T223, qsortc79_in_ga(T222, T226))
U36_GA(T215, T213, T214, T9, T223, qsortc79_out_ga(T222, T226)) → U37_GA(T215, T213, T214, T9, p78_in_gagga(.(T213, T223), X13, T226, T215, T9))
U36_GA(T215, T213, T214, T9, T223, qsortc79_out_ga(T222, T226)) → P78_IN_GAGGA(.(T213, T223), X13, T226, T215, T9)
P78_IN_GAGGA(T94, X13, T155, T69, T9) → U18_GAGGA(T94, X13, T155, T69, T9, qsort79_in_ga(T94, X13))
P78_IN_GAGGA(T94, X13, T155, T69, T9) → QSORT79_IN_GA(T94, X13)
P78_IN_GAGGA(T94, T158, T155, T69, T9) → U19_GAGGA(T94, T158, T155, T69, T9, qsortc79_in_ga(T94, T158))
U19_GAGGA(T94, T158, T155, T69, T9, qsortc79_out_ga(T94, T158)) → U20_GAGGA(T94, T158, T155, T69, T9, append23_in_ggga(T155, T69, T158, T9))
U19_GAGGA(T94, T158, T155, T69, T9, qsortc79_out_ga(T94, T158)) → APPEND23_IN_GGGA(T155, T69, T158, T9)
U27_GA(T69, T67, T68, T9, splitc51_out_ggaa(T68, T69, T93, T94)) → U29_GA(T69, T67, T68, T9, T94, qsortc1_in_ga(.(T67, T93), T155))
U29_GA(T69, T67, T68, T9, T94, qsortc1_out_ga(.(T67, T93), T155)) → U30_GA(T69, T67, T68, T9, p78_in_gagga(T94, X13, T155, T69, T9))
U29_GA(T69, T67, T68, T9, T94, qsortc1_out_ga(.(T67, T93), T155)) → P78_IN_GAGGA(T94, X13, T155, T69, T9)

The TRS R consists of the following rules:

qsortc14_in_a([]) → qsortc14_out_a([])
lec36_in_gg(s(T82), s(T83)) → U40_gg(T82, T83, lec36_in_gg(T82, T83))
lec36_in_gg(0, s(T90)) → lec36_out_gg(0, s(T90))
lec36_in_gg(0, 0) → lec36_out_gg(0, 0)
U40_gg(T82, T83, lec36_out_gg(T82, T83)) → lec36_out_gg(s(T82), s(T83))
gtc67_in_gg(s(T144), s(T145)) → U45_gg(T144, T145, gtc67_in_gg(T144, T145))
gtc67_in_gg(s(T150), 0) → gtc67_out_gg(s(T150), 0)
U45_gg(T144, T145, gtc67_out_gg(T144, T145)) → gtc67_out_gg(s(T144), s(T145))
splitc51_in_ggaa([], T101, [], []) → splitc51_out_ggaa([], T101, [], [])
splitc51_in_ggaa(.(T114, T115), T116, .(T114, X167), X168) → U41_ggaa(T114, T115, T116, X167, X168, lec36_in_gg(T114, T116))
U41_ggaa(T114, T115, T116, X167, X168, lec36_out_gg(T114, T116)) → U42_ggaa(T114, T115, T116, X167, X168, splitc51_in_ggaa(T115, T116, X167, X168))
splitc51_in_ggaa(.(T129, T130), T131, X199, .(T129, X200)) → U43_ggaa(T129, T130, T131, X199, X200, gtc67_in_gg(T129, T131))
U43_ggaa(T129, T130, T131, X199, X200, gtc67_out_gg(T129, T131)) → U44_ggaa(T129, T130, T131, X199, X200, splitc51_in_ggaa(T130, T131, X199, X200))
U44_ggaa(T129, T130, T131, X199, X200, splitc51_out_ggaa(T130, T131, X199, X200)) → splitc51_out_ggaa(.(T129, T130), T131, X199, .(T129, X200))
U42_ggaa(T114, T115, T116, X167, X168, splitc51_out_ggaa(T115, T116, X167, X168)) → splitc51_out_ggaa(.(T114, T115), T116, .(T114, X167), X168)
qsortc79_in_ga([], []) → qsortc79_out_ga([], [])
qsortc79_in_ga(.(T163, T164), X265) → U57_ga(T163, T164, X265, splitc51_in_ggaa(T164, T163, T167, T168))
U57_ga(T163, T164, X265, splitc51_out_ggaa(T164, T163, T167, T168)) → U58_ga(T163, T164, X265, T168, qsortc79_in_ga(T167, T171))
U58_ga(T163, T164, X265, T168, qsortc79_out_ga(T167, T171)) → U59_ga(T163, T164, X265, T171, qsortc79_in_ga(T168, T172))
U59_ga(T163, T164, X265, T171, qsortc79_out_ga(T168, T172)) → U60_ga(T163, T164, X265, appendc94_in_ggga(T171, T163, T172, X265))
appendc94_in_ggga([], T185, T186, .(T185, T186)) → appendc94_out_ggga([], T185, T186, .(T185, T186))
appendc94_in_ggga(.(T195, T196), T197, T198, .(T195, X295)) → U61_ggga(T195, T196, T197, T198, X295, appendc94_in_ggga(T196, T197, T198, X295))
U61_ggga(T195, T196, T197, T198, X295, appendc94_out_ggga(T196, T197, T198, X295)) → appendc94_out_ggga(.(T195, T196), T197, T198, .(T195, X295))
U60_ga(T163, T164, X265, appendc94_out_ggga(T171, T163, T172, X265)) → qsortc79_out_ga(.(T163, T164), X265)
qsortc1_in_ga([], []) → qsortc1_out_ga([], [])
qsortc1_in_ga(.(T14, []), T9) → U46_ga(T14, T9, qsortc14_in_a(T17))
U46_ga(T14, T9, qsortc14_out_a(T17)) → U47_ga(T14, T9, T17, qsortc14_in_a(T20))
U47_ga(T14, T9, T17, qsortc14_out_a(T20)) → U48_ga(T14, T9, appendc23_in_ggga(T17, T14, T20, T9))
appendc23_in_ggga([], T33, T34, .(T33, T34)) → appendc23_out_ggga([], T33, T34, .(T33, T34))
appendc23_in_ggga(.(T45, T46), T47, T48, .(T45, T50)) → U39_ggga(T45, T46, T47, T48, T50, appendc23_in_ggga(T46, T47, T48, T50))
U39_ggga(T45, T46, T47, T48, T50, appendc23_out_ggga(T46, T47, T48, T50)) → appendc23_out_ggga(.(T45, T46), T47, T48, .(T45, T50))
U48_ga(T14, T9, appendc23_out_ggga(T17, T14, T20, T9)) → qsortc1_out_ga(.(T14, []), T9)
qsortc1_in_ga(.(T69, .(T67, T68)), T9) → U49_ga(T69, T67, T68, T9, lec36_in_gg(T67, T69))
U49_ga(T69, T67, T68, T9, lec36_out_gg(T67, T69)) → U50_ga(T69, T67, T68, T9, splitc51_in_ggaa(T68, T69, T93, T94))
U50_ga(T69, T67, T68, T9, splitc51_out_ggaa(T68, T69, T93, T94)) → U51_ga(T69, T67, T68, T9, T94, qsortc1_in_ga(.(T67, T93), T155))
qsortc1_in_ga(.(T215, .(T213, T214)), T9) → U53_ga(T215, T213, T214, T9, gtc67_in_gg(T213, T215))
U53_ga(T215, T213, T214, T9, gtc67_out_gg(T213, T215)) → U54_ga(T215, T213, T214, T9, splitc51_in_ggaa(T214, T215, T222, T223))
U54_ga(T215, T213, T214, T9, splitc51_out_ggaa(T214, T215, T222, T223)) → U55_ga(T215, T213, T214, T9, T223, qsortc79_in_ga(T222, T226))
U55_ga(T215, T213, T214, T9, T223, qsortc79_out_ga(T222, T226)) → U56_ga(T215, T213, T214, T9, qc78_in_gagga(.(T213, T223), X13, T226, T215, T9))
qc78_in_gagga(T94, T158, T155, T69, T9) → U62_gagga(T94, T158, T155, T69, T9, qsortc79_in_ga(T94, T158))
U62_gagga(T94, T158, T155, T69, T9, qsortc79_out_ga(T94, T158)) → U63_gagga(T94, T158, T155, T69, T9, appendc23_in_ggga(T155, T69, T158, T9))
U63_gagga(T94, T158, T155, T69, T9, appendc23_out_ggga(T155, T69, T158, T9)) → qc78_out_gagga(T94, T158, T155, T69, T9)
U56_ga(T215, T213, T214, T9, qc78_out_gagga(.(T213, T223), X13, T226, T215, T9)) → qsortc1_out_ga(.(T215, .(T213, T214)), T9)
U51_ga(T69, T67, T68, T9, T94, qsortc1_out_ga(.(T67, T93), T155)) → U52_ga(T69, T67, T68, T9, qc78_in_gagga(T94, X13, T155, T69, T9))
U52_ga(T69, T67, T68, T9, qc78_out_gagga(T94, X13, T155, T69, T9)) → qsortc1_out_ga(.(T69, .(T67, T68)), T9)

The argument filtering Pi contains the following mapping:
qsort1_in_ga(x1, x2)  =  qsort1_in_ga(x1)
.(x1, x2)  =  .(x1, x2)
[]  =  []
qsortc14_in_a(x1)  =  qsortc14_in_a
qsortc14_out_a(x1)  =  qsortc14_out_a(x1)
append23_in_ggga(x1, x2, x3, x4)  =  append23_in_ggga(x1, x2, x3)
le36_in_gg(x1, x2)  =  le36_in_gg(x1, x2)
s(x1)  =  s(x1)
lec36_in_gg(x1, x2)  =  lec36_in_gg(x1, x2)
U40_gg(x1, x2, x3)  =  U40_gg(x1, x2, x3)
0  =  0
lec36_out_gg(x1, x2)  =  lec36_out_gg(x1, x2)
split51_in_ggaa(x1, x2, x3, x4)  =  split51_in_ggaa(x1, x2)
gt67_in_gg(x1, x2)  =  gt67_in_gg(x1, x2)
gtc67_in_gg(x1, x2)  =  gtc67_in_gg(x1, x2)
U45_gg(x1, x2, x3)  =  U45_gg(x1, x2, x3)
gtc67_out_gg(x1, x2)  =  gtc67_out_gg(x1, x2)
splitc51_in_ggaa(x1, x2, x3, x4)  =  splitc51_in_ggaa(x1, x2)
splitc51_out_ggaa(x1, x2, x3, x4)  =  splitc51_out_ggaa(x1, x2, x3, x4)
U41_ggaa(x1, x2, x3, x4, x5, x6)  =  U41_ggaa(x1, x2, x3, x6)
U42_ggaa(x1, x2, x3, x4, x5, x6)  =  U42_ggaa(x1, x2, x3, x6)
U43_ggaa(x1, x2, x3, x4, x5, x6)  =  U43_ggaa(x1, x2, x3, x6)
U44_ggaa(x1, x2, x3, x4, x5, x6)  =  U44_ggaa(x1, x2, x3, x6)
qsort79_in_ga(x1, x2)  =  qsort79_in_ga(x1)
qsortc79_in_ga(x1, x2)  =  qsortc79_in_ga(x1)
qsortc79_out_ga(x1, x2)  =  qsortc79_out_ga(x1, x2)
U57_ga(x1, x2, x3, x4)  =  U57_ga(x1, x2, x4)
U58_ga(x1, x2, x3, x4, x5)  =  U58_ga(x1, x2, x4, x5)
U59_ga(x1, x2, x3, x4, x5)  =  U59_ga(x1, x2, x4, x5)
U60_ga(x1, x2, x3, x4)  =  U60_ga(x1, x2, x4)
appendc94_in_ggga(x1, x2, x3, x4)  =  appendc94_in_ggga(x1, x2, x3)
appendc94_out_ggga(x1, x2, x3, x4)  =  appendc94_out_ggga(x1, x2, x3, x4)
U61_ggga(x1, x2, x3, x4, x5, x6)  =  U61_ggga(x1, x2, x3, x4, x6)
append94_in_ggga(x1, x2, x3, x4)  =  append94_in_ggga(x1, x2, x3)
p78_in_gagga(x1, x2, x3, x4, x5)  =  p78_in_gagga(x1, x3, x4)
qsortc1_in_ga(x1, x2)  =  qsortc1_in_ga(x1)
qsortc1_out_ga(x1, x2)  =  qsortc1_out_ga(x1, x2)
U46_ga(x1, x2, x3)  =  U46_ga(x1, x3)
U47_ga(x1, x2, x3, x4)  =  U47_ga(x1, x3, x4)
U48_ga(x1, x2, x3)  =  U48_ga(x1, x3)
appendc23_in_ggga(x1, x2, x3, x4)  =  appendc23_in_ggga(x1, x2, x3)
appendc23_out_ggga(x1, x2, x3, x4)  =  appendc23_out_ggga(x1, x2, x3, x4)
U39_ggga(x1, x2, x3, x4, x5, x6)  =  U39_ggga(x1, x2, x3, x4, x6)
U49_ga(x1, x2, x3, x4, x5)  =  U49_ga(x1, x2, x3, x5)
U50_ga(x1, x2, x3, x4, x5)  =  U50_ga(x1, x2, x3, x5)
U51_ga(x1, x2, x3, x4, x5, x6)  =  U51_ga(x1, x2, x3, x5, x6)
U53_ga(x1, x2, x3, x4, x5)  =  U53_ga(x1, x2, x3, x5)
U54_ga(x1, x2, x3, x4, x5)  =  U54_ga(x1, x2, x3, x5)
U55_ga(x1, x2, x3, x4, x5, x6)  =  U55_ga(x1, x2, x3, x5, x6)
U56_ga(x1, x2, x3, x4, x5)  =  U56_ga(x1, x2, x3, x5)
qc78_in_gagga(x1, x2, x3, x4, x5)  =  qc78_in_gagga(x1, x3, x4)
U62_gagga(x1, x2, x3, x4, x5, x6)  =  U62_gagga(x1, x3, x4, x6)
U63_gagga(x1, x2, x3, x4, x5, x6)  =  U63_gagga(x1, x2, x3, x4, x6)
qc78_out_gagga(x1, x2, x3, x4, x5)  =  qc78_out_gagga(x1, x2, x3, x4, x5)
U52_ga(x1, x2, x3, x4, x5)  =  U52_ga(x1, x2, x3, x5)
QSORT1_IN_GA(x1, x2)  =  QSORT1_IN_GA(x1)
U21_GA(x1, x2, x3)  =  U21_GA(x1, x3)
U22_GA(x1, x2, x3, x4)  =  U22_GA(x1, x3, x4)
U23_GA(x1, x2, x3)  =  U23_GA(x1, x3)
APPEND23_IN_GGGA(x1, x2, x3, x4)  =  APPEND23_IN_GGGA(x1, x2, x3)
U1_GGGA(x1, x2, x3, x4, x5, x6)  =  U1_GGGA(x1, x2, x3, x4, x6)
U24_GA(x1, x2, x3, x4, x5)  =  U24_GA(x1, x2, x3, x5)
LE36_IN_GG(x1, x2)  =  LE36_IN_GG(x1, x2)
U2_GG(x1, x2, x3)  =  U2_GG(x1, x2, x3)
U25_GA(x1, x2, x3, x4, x5)  =  U25_GA(x1, x2, x3, x5)
U26_GA(x1, x2, x3, x4, x5)  =  U26_GA(x1, x2, x3, x5)
SPLIT51_IN_GGAA(x1, x2, x3, x4)  =  SPLIT51_IN_GGAA(x1, x2)
U3_GGAA(x1, x2, x3, x4, x5, x6)  =  U3_GGAA(x1, x2, x3, x6)
U4_GGAA(x1, x2, x3, x4, x5, x6)  =  U4_GGAA(x1, x2, x3, x6)
U5_GGAA(x1, x2, x3, x4, x5, x6)  =  U5_GGAA(x1, x2, x3, x6)
U6_GGAA(x1, x2, x3, x4, x5, x6)  =  U6_GGAA(x1, x2, x3, x6)
GT67_IN_GG(x1, x2)  =  GT67_IN_GG(x1, x2)
U9_GG(x1, x2, x3)  =  U9_GG(x1, x2, x3)
U7_GGAA(x1, x2, x3, x4, x5, x6)  =  U7_GGAA(x1, x2, x3, x6)
U8_GGAA(x1, x2, x3, x4, x5, x6)  =  U8_GGAA(x1, x2, x3, x6)
U27_GA(x1, x2, x3, x4, x5)  =  U27_GA(x1, x2, x3, x5)
U28_GA(x1, x2, x3, x4, x5)  =  U28_GA(x1, x2, x3, x5)
U31_GA(x1, x2, x3, x4, x5)  =  U31_GA(x1, x2, x3, x5)
U32_GA(x1, x2, x3, x4, x5)  =  U32_GA(x1, x2, x3, x5)
U33_GA(x1, x2, x3, x4, x5)  =  U33_GA(x1, x2, x3, x5)
U34_GA(x1, x2, x3, x4, x5)  =  U34_GA(x1, x2, x3, x5)
U35_GA(x1, x2, x3, x4, x5)  =  U35_GA(x1, x2, x3, x5)
QSORT79_IN_GA(x1, x2)  =  QSORT79_IN_GA(x1)
U10_GA(x1, x2, x3, x4)  =  U10_GA(x1, x2, x4)
U11_GA(x1, x2, x3, x4)  =  U11_GA(x1, x2, x4)
U12_GA(x1, x2, x3, x4)  =  U12_GA(x1, x2, x4)
U13_GA(x1, x2, x3, x4, x5)  =  U13_GA(x1, x2, x4, x5)
U14_GA(x1, x2, x3, x4)  =  U14_GA(x1, x2, x4)
U15_GA(x1, x2, x3, x4, x5)  =  U15_GA(x1, x2, x4, x5)
U16_GA(x1, x2, x3, x4)  =  U16_GA(x1, x2, x4)
APPEND94_IN_GGGA(x1, x2, x3, x4)  =  APPEND94_IN_GGGA(x1, x2, x3)
U17_GGGA(x1, x2, x3, x4, x5, x6)  =  U17_GGGA(x1, x2, x3, x4, x6)
U36_GA(x1, x2, x3, x4, x5, x6)  =  U36_GA(x1, x2, x3, x5, x6)
U37_GA(x1, x2, x3, x4, x5)  =  U37_GA(x1, x2, x3, x5)
P78_IN_GAGGA(x1, x2, x3, x4, x5)  =  P78_IN_GAGGA(x1, x3, x4)
U18_GAGGA(x1, x2, x3, x4, x5, x6)  =  U18_GAGGA(x1, x3, x4, x6)
U19_GAGGA(x1, x2, x3, x4, x5, x6)  =  U19_GAGGA(x1, x3, x4, x6)
U20_GAGGA(x1, x2, x3, x4, x5, x6)  =  U20_GAGGA(x1, x3, x4, x6)
U29_GA(x1, x2, x3, x4, x5, x6)  =  U29_GA(x1, x2, x3, x5, x6)
U30_GA(x1, x2, x3, x4, x5)  =  U30_GA(x1, x2, x3, x5)

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:

QSORT1_IN_GA(.(T14, []), T9) → U21_GA(T14, T9, qsortc14_in_a(T17))
U21_GA(T14, T9, qsortc14_out_a(T17)) → U22_GA(T14, T9, T17, qsortc14_in_a(T20))
U22_GA(T14, T9, T17, qsortc14_out_a(T20)) → U23_GA(T14, T9, append23_in_ggga(T17, T14, T20, T9))
U22_GA(T14, T9, T17, qsortc14_out_a(T20)) → APPEND23_IN_GGGA(T17, T14, T20, T9)
APPEND23_IN_GGGA(.(T45, T46), T47, T48, .(T45, T50)) → U1_GGGA(T45, T46, T47, T48, T50, append23_in_ggga(T46, T47, T48, T50))
APPEND23_IN_GGGA(.(T45, T46), T47, T48, .(T45, T50)) → APPEND23_IN_GGGA(T46, T47, T48, T50)
QSORT1_IN_GA(.(T69, .(T67, T68)), T9) → U24_GA(T69, T67, T68, T9, le36_in_gg(T67, T69))
QSORT1_IN_GA(.(T69, .(T67, T68)), T9) → LE36_IN_GG(T67, T69)
LE36_IN_GG(s(T82), s(T83)) → U2_GG(T82, T83, le36_in_gg(T82, T83))
LE36_IN_GG(s(T82), s(T83)) → LE36_IN_GG(T82, T83)
QSORT1_IN_GA(.(T69, .(T67, T68)), T9) → U25_GA(T69, T67, T68, T9, lec36_in_gg(T67, T69))
U25_GA(T69, T67, T68, T9, lec36_out_gg(T67, T69)) → U26_GA(T69, T67, T68, T9, split51_in_ggaa(T68, T69, X93, X94))
U25_GA(T69, T67, T68, T9, lec36_out_gg(T67, T69)) → SPLIT51_IN_GGAA(T68, T69, X93, X94)
SPLIT51_IN_GGAA(.(T114, T115), T116, .(T114, X167), X168) → U3_GGAA(T114, T115, T116, X167, X168, le36_in_gg(T114, T116))
SPLIT51_IN_GGAA(.(T114, T115), T116, .(T114, X167), X168) → LE36_IN_GG(T114, T116)
SPLIT51_IN_GGAA(.(T114, T115), T116, .(T114, X167), X168) → U4_GGAA(T114, T115, T116, X167, X168, lec36_in_gg(T114, T116))
U4_GGAA(T114, T115, T116, X167, X168, lec36_out_gg(T114, T116)) → U5_GGAA(T114, T115, T116, X167, X168, split51_in_ggaa(T115, T116, X167, X168))
U4_GGAA(T114, T115, T116, X167, X168, lec36_out_gg(T114, T116)) → SPLIT51_IN_GGAA(T115, T116, X167, X168)
SPLIT51_IN_GGAA(.(T129, T130), T131, X199, .(T129, X200)) → U6_GGAA(T129, T130, T131, X199, X200, gt67_in_gg(T129, T131))
SPLIT51_IN_GGAA(.(T129, T130), T131, X199, .(T129, X200)) → GT67_IN_GG(T129, T131)
GT67_IN_GG(s(T144), s(T145)) → U9_GG(T144, T145, gt67_in_gg(T144, T145))
GT67_IN_GG(s(T144), s(T145)) → GT67_IN_GG(T144, T145)
SPLIT51_IN_GGAA(.(T129, T130), T131, X199, .(T129, X200)) → U7_GGAA(T129, T130, T131, X199, X200, gtc67_in_gg(T129, T131))
U7_GGAA(T129, T130, T131, X199, X200, gtc67_out_gg(T129, T131)) → U8_GGAA(T129, T130, T131, X199, X200, split51_in_ggaa(T130, T131, X199, X200))
U7_GGAA(T129, T130, T131, X199, X200, gtc67_out_gg(T129, T131)) → SPLIT51_IN_GGAA(T130, T131, X199, X200)
U25_GA(T69, T67, T68, T9, lec36_out_gg(T67, T69)) → U27_GA(T69, T67, T68, T9, splitc51_in_ggaa(T68, T69, T93, T94))
U27_GA(T69, T67, T68, T9, splitc51_out_ggaa(T68, T69, T93, T94)) → U28_GA(T69, T67, T68, T9, qsort1_in_ga(.(T67, T93), X12))
U27_GA(T69, T67, T68, T9, splitc51_out_ggaa(T68, T69, T93, T94)) → QSORT1_IN_GA(.(T67, T93), X12)
QSORT1_IN_GA(.(T215, .(T213, T214)), T9) → U31_GA(T215, T213, T214, T9, gt67_in_gg(T213, T215))
QSORT1_IN_GA(.(T215, .(T213, T214)), T9) → GT67_IN_GG(T213, T215)
QSORT1_IN_GA(.(T215, .(T213, T214)), T9) → U32_GA(T215, T213, T214, T9, gtc67_in_gg(T213, T215))
U32_GA(T215, T213, T214, T9, gtc67_out_gg(T213, T215)) → U33_GA(T215, T213, T214, T9, split51_in_ggaa(T214, T215, X323, X324))
U32_GA(T215, T213, T214, T9, gtc67_out_gg(T213, T215)) → SPLIT51_IN_GGAA(T214, T215, X323, X324)
U32_GA(T215, T213, T214, T9, gtc67_out_gg(T213, T215)) → U34_GA(T215, T213, T214, T9, splitc51_in_ggaa(T214, T215, T222, T223))
U34_GA(T215, T213, T214, T9, splitc51_out_ggaa(T214, T215, T222, T223)) → U35_GA(T215, T213, T214, T9, qsort79_in_ga(T222, X12))
U34_GA(T215, T213, T214, T9, splitc51_out_ggaa(T214, T215, T222, T223)) → QSORT79_IN_GA(T222, X12)
QSORT79_IN_GA(.(T163, T164), X265) → U10_GA(T163, T164, X265, split51_in_ggaa(T164, T163, X261, X262))
QSORT79_IN_GA(.(T163, T164), X265) → SPLIT51_IN_GGAA(T164, T163, X261, X262)
QSORT79_IN_GA(.(T163, T164), X265) → U11_GA(T163, T164, X265, splitc51_in_ggaa(T164, T163, T167, T168))
U11_GA(T163, T164, X265, splitc51_out_ggaa(T164, T163, T167, T168)) → U12_GA(T163, T164, X265, qsort79_in_ga(T167, X263))
U11_GA(T163, T164, X265, splitc51_out_ggaa(T164, T163, T167, T168)) → QSORT79_IN_GA(T167, X263)
U11_GA(T163, T164, X265, splitc51_out_ggaa(T164, T163, T167, T168)) → U13_GA(T163, T164, X265, T168, qsortc79_in_ga(T167, T171))
U13_GA(T163, T164, X265, T168, qsortc79_out_ga(T167, T171)) → U14_GA(T163, T164, X265, qsort79_in_ga(T168, X264))
U13_GA(T163, T164, X265, T168, qsortc79_out_ga(T167, T171)) → QSORT79_IN_GA(T168, X264)
U13_GA(T163, T164, X265, T168, qsortc79_out_ga(T167, T171)) → U15_GA(T163, T164, X265, T171, qsortc79_in_ga(T168, T172))
U15_GA(T163, T164, X265, T171, qsortc79_out_ga(T168, T172)) → U16_GA(T163, T164, X265, append94_in_ggga(T171, T163, T172, X265))
U15_GA(T163, T164, X265, T171, qsortc79_out_ga(T168, T172)) → APPEND94_IN_GGGA(T171, T163, T172, X265)
APPEND94_IN_GGGA(.(T195, T196), T197, T198, .(T195, X295)) → U17_GGGA(T195, T196, T197, T198, X295, append94_in_ggga(T196, T197, T198, X295))
APPEND94_IN_GGGA(.(T195, T196), T197, T198, .(T195, X295)) → APPEND94_IN_GGGA(T196, T197, T198, X295)
U34_GA(T215, T213, T214, T9, splitc51_out_ggaa(T214, T215, T222, T223)) → U36_GA(T215, T213, T214, T9, T223, qsortc79_in_ga(T222, T226))
U36_GA(T215, T213, T214, T9, T223, qsortc79_out_ga(T222, T226)) → U37_GA(T215, T213, T214, T9, p78_in_gagga(.(T213, T223), X13, T226, T215, T9))
U36_GA(T215, T213, T214, T9, T223, qsortc79_out_ga(T222, T226)) → P78_IN_GAGGA(.(T213, T223), X13, T226, T215, T9)
P78_IN_GAGGA(T94, X13, T155, T69, T9) → U18_GAGGA(T94, X13, T155, T69, T9, qsort79_in_ga(T94, X13))
P78_IN_GAGGA(T94, X13, T155, T69, T9) → QSORT79_IN_GA(T94, X13)
P78_IN_GAGGA(T94, T158, T155, T69, T9) → U19_GAGGA(T94, T158, T155, T69, T9, qsortc79_in_ga(T94, T158))
U19_GAGGA(T94, T158, T155, T69, T9, qsortc79_out_ga(T94, T158)) → U20_GAGGA(T94, T158, T155, T69, T9, append23_in_ggga(T155, T69, T158, T9))
U19_GAGGA(T94, T158, T155, T69, T9, qsortc79_out_ga(T94, T158)) → APPEND23_IN_GGGA(T155, T69, T158, T9)
U27_GA(T69, T67, T68, T9, splitc51_out_ggaa(T68, T69, T93, T94)) → U29_GA(T69, T67, T68, T9, T94, qsortc1_in_ga(.(T67, T93), T155))
U29_GA(T69, T67, T68, T9, T94, qsortc1_out_ga(.(T67, T93), T155)) → U30_GA(T69, T67, T68, T9, p78_in_gagga(T94, X13, T155, T69, T9))
U29_GA(T69, T67, T68, T9, T94, qsortc1_out_ga(.(T67, T93), T155)) → P78_IN_GAGGA(T94, X13, T155, T69, T9)

The TRS R consists of the following rules:

qsortc14_in_a([]) → qsortc14_out_a([])
lec36_in_gg(s(T82), s(T83)) → U40_gg(T82, T83, lec36_in_gg(T82, T83))
lec36_in_gg(0, s(T90)) → lec36_out_gg(0, s(T90))
lec36_in_gg(0, 0) → lec36_out_gg(0, 0)
U40_gg(T82, T83, lec36_out_gg(T82, T83)) → lec36_out_gg(s(T82), s(T83))
gtc67_in_gg(s(T144), s(T145)) → U45_gg(T144, T145, gtc67_in_gg(T144, T145))
gtc67_in_gg(s(T150), 0) → gtc67_out_gg(s(T150), 0)
U45_gg(T144, T145, gtc67_out_gg(T144, T145)) → gtc67_out_gg(s(T144), s(T145))
splitc51_in_ggaa([], T101, [], []) → splitc51_out_ggaa([], T101, [], [])
splitc51_in_ggaa(.(T114, T115), T116, .(T114, X167), X168) → U41_ggaa(T114, T115, T116, X167, X168, lec36_in_gg(T114, T116))
U41_ggaa(T114, T115, T116, X167, X168, lec36_out_gg(T114, T116)) → U42_ggaa(T114, T115, T116, X167, X168, splitc51_in_ggaa(T115, T116, X167, X168))
splitc51_in_ggaa(.(T129, T130), T131, X199, .(T129, X200)) → U43_ggaa(T129, T130, T131, X199, X200, gtc67_in_gg(T129, T131))
U43_ggaa(T129, T130, T131, X199, X200, gtc67_out_gg(T129, T131)) → U44_ggaa(T129, T130, T131, X199, X200, splitc51_in_ggaa(T130, T131, X199, X200))
U44_ggaa(T129, T130, T131, X199, X200, splitc51_out_ggaa(T130, T131, X199, X200)) → splitc51_out_ggaa(.(T129, T130), T131, X199, .(T129, X200))
U42_ggaa(T114, T115, T116, X167, X168, splitc51_out_ggaa(T115, T116, X167, X168)) → splitc51_out_ggaa(.(T114, T115), T116, .(T114, X167), X168)
qsortc79_in_ga([], []) → qsortc79_out_ga([], [])
qsortc79_in_ga(.(T163, T164), X265) → U57_ga(T163, T164, X265, splitc51_in_ggaa(T164, T163, T167, T168))
U57_ga(T163, T164, X265, splitc51_out_ggaa(T164, T163, T167, T168)) → U58_ga(T163, T164, X265, T168, qsortc79_in_ga(T167, T171))
U58_ga(T163, T164, X265, T168, qsortc79_out_ga(T167, T171)) → U59_ga(T163, T164, X265, T171, qsortc79_in_ga(T168, T172))
U59_ga(T163, T164, X265, T171, qsortc79_out_ga(T168, T172)) → U60_ga(T163, T164, X265, appendc94_in_ggga(T171, T163, T172, X265))
appendc94_in_ggga([], T185, T186, .(T185, T186)) → appendc94_out_ggga([], T185, T186, .(T185, T186))
appendc94_in_ggga(.(T195, T196), T197, T198, .(T195, X295)) → U61_ggga(T195, T196, T197, T198, X295, appendc94_in_ggga(T196, T197, T198, X295))
U61_ggga(T195, T196, T197, T198, X295, appendc94_out_ggga(T196, T197, T198, X295)) → appendc94_out_ggga(.(T195, T196), T197, T198, .(T195, X295))
U60_ga(T163, T164, X265, appendc94_out_ggga(T171, T163, T172, X265)) → qsortc79_out_ga(.(T163, T164), X265)
qsortc1_in_ga([], []) → qsortc1_out_ga([], [])
qsortc1_in_ga(.(T14, []), T9) → U46_ga(T14, T9, qsortc14_in_a(T17))
U46_ga(T14, T9, qsortc14_out_a(T17)) → U47_ga(T14, T9, T17, qsortc14_in_a(T20))
U47_ga(T14, T9, T17, qsortc14_out_a(T20)) → U48_ga(T14, T9, appendc23_in_ggga(T17, T14, T20, T9))
appendc23_in_ggga([], T33, T34, .(T33, T34)) → appendc23_out_ggga([], T33, T34, .(T33, T34))
appendc23_in_ggga(.(T45, T46), T47, T48, .(T45, T50)) → U39_ggga(T45, T46, T47, T48, T50, appendc23_in_ggga(T46, T47, T48, T50))
U39_ggga(T45, T46, T47, T48, T50, appendc23_out_ggga(T46, T47, T48, T50)) → appendc23_out_ggga(.(T45, T46), T47, T48, .(T45, T50))
U48_ga(T14, T9, appendc23_out_ggga(T17, T14, T20, T9)) → qsortc1_out_ga(.(T14, []), T9)
qsortc1_in_ga(.(T69, .(T67, T68)), T9) → U49_ga(T69, T67, T68, T9, lec36_in_gg(T67, T69))
U49_ga(T69, T67, T68, T9, lec36_out_gg(T67, T69)) → U50_ga(T69, T67, T68, T9, splitc51_in_ggaa(T68, T69, T93, T94))
U50_ga(T69, T67, T68, T9, splitc51_out_ggaa(T68, T69, T93, T94)) → U51_ga(T69, T67, T68, T9, T94, qsortc1_in_ga(.(T67, T93), T155))
qsortc1_in_ga(.(T215, .(T213, T214)), T9) → U53_ga(T215, T213, T214, T9, gtc67_in_gg(T213, T215))
U53_ga(T215, T213, T214, T9, gtc67_out_gg(T213, T215)) → U54_ga(T215, T213, T214, T9, splitc51_in_ggaa(T214, T215, T222, T223))
U54_ga(T215, T213, T214, T9, splitc51_out_ggaa(T214, T215, T222, T223)) → U55_ga(T215, T213, T214, T9, T223, qsortc79_in_ga(T222, T226))
U55_ga(T215, T213, T214, T9, T223, qsortc79_out_ga(T222, T226)) → U56_ga(T215, T213, T214, T9, qc78_in_gagga(.(T213, T223), X13, T226, T215, T9))
qc78_in_gagga(T94, T158, T155, T69, T9) → U62_gagga(T94, T158, T155, T69, T9, qsortc79_in_ga(T94, T158))
U62_gagga(T94, T158, T155, T69, T9, qsortc79_out_ga(T94, T158)) → U63_gagga(T94, T158, T155, T69, T9, appendc23_in_ggga(T155, T69, T158, T9))
U63_gagga(T94, T158, T155, T69, T9, appendc23_out_ggga(T155, T69, T158, T9)) → qc78_out_gagga(T94, T158, T155, T69, T9)
U56_ga(T215, T213, T214, T9, qc78_out_gagga(.(T213, T223), X13, T226, T215, T9)) → qsortc1_out_ga(.(T215, .(T213, T214)), T9)
U51_ga(T69, T67, T68, T9, T94, qsortc1_out_ga(.(T67, T93), T155)) → U52_ga(T69, T67, T68, T9, qc78_in_gagga(T94, X13, T155, T69, T9))
U52_ga(T69, T67, T68, T9, qc78_out_gagga(T94, X13, T155, T69, T9)) → qsortc1_out_ga(.(T69, .(T67, T68)), T9)

The argument filtering Pi contains the following mapping:
qsort1_in_ga(x1, x2)  =  qsort1_in_ga(x1)
.(x1, x2)  =  .(x1, x2)
[]  =  []
qsortc14_in_a(x1)  =  qsortc14_in_a
qsortc14_out_a(x1)  =  qsortc14_out_a(x1)
append23_in_ggga(x1, x2, x3, x4)  =  append23_in_ggga(x1, x2, x3)
le36_in_gg(x1, x2)  =  le36_in_gg(x1, x2)
s(x1)  =  s(x1)
lec36_in_gg(x1, x2)  =  lec36_in_gg(x1, x2)
U40_gg(x1, x2, x3)  =  U40_gg(x1, x2, x3)
0  =  0
lec36_out_gg(x1, x2)  =  lec36_out_gg(x1, x2)
split51_in_ggaa(x1, x2, x3, x4)  =  split51_in_ggaa(x1, x2)
gt67_in_gg(x1, x2)  =  gt67_in_gg(x1, x2)
gtc67_in_gg(x1, x2)  =  gtc67_in_gg(x1, x2)
U45_gg(x1, x2, x3)  =  U45_gg(x1, x2, x3)
gtc67_out_gg(x1, x2)  =  gtc67_out_gg(x1, x2)
splitc51_in_ggaa(x1, x2, x3, x4)  =  splitc51_in_ggaa(x1, x2)
splitc51_out_ggaa(x1, x2, x3, x4)  =  splitc51_out_ggaa(x1, x2, x3, x4)
U41_ggaa(x1, x2, x3, x4, x5, x6)  =  U41_ggaa(x1, x2, x3, x6)
U42_ggaa(x1, x2, x3, x4, x5, x6)  =  U42_ggaa(x1, x2, x3, x6)
U43_ggaa(x1, x2, x3, x4, x5, x6)  =  U43_ggaa(x1, x2, x3, x6)
U44_ggaa(x1, x2, x3, x4, x5, x6)  =  U44_ggaa(x1, x2, x3, x6)
qsort79_in_ga(x1, x2)  =  qsort79_in_ga(x1)
qsortc79_in_ga(x1, x2)  =  qsortc79_in_ga(x1)
qsortc79_out_ga(x1, x2)  =  qsortc79_out_ga(x1, x2)
U57_ga(x1, x2, x3, x4)  =  U57_ga(x1, x2, x4)
U58_ga(x1, x2, x3, x4, x5)  =  U58_ga(x1, x2, x4, x5)
U59_ga(x1, x2, x3, x4, x5)  =  U59_ga(x1, x2, x4, x5)
U60_ga(x1, x2, x3, x4)  =  U60_ga(x1, x2, x4)
appendc94_in_ggga(x1, x2, x3, x4)  =  appendc94_in_ggga(x1, x2, x3)
appendc94_out_ggga(x1, x2, x3, x4)  =  appendc94_out_ggga(x1, x2, x3, x4)
U61_ggga(x1, x2, x3, x4, x5, x6)  =  U61_ggga(x1, x2, x3, x4, x6)
append94_in_ggga(x1, x2, x3, x4)  =  append94_in_ggga(x1, x2, x3)
p78_in_gagga(x1, x2, x3, x4, x5)  =  p78_in_gagga(x1, x3, x4)
qsortc1_in_ga(x1, x2)  =  qsortc1_in_ga(x1)
qsortc1_out_ga(x1, x2)  =  qsortc1_out_ga(x1, x2)
U46_ga(x1, x2, x3)  =  U46_ga(x1, x3)
U47_ga(x1, x2, x3, x4)  =  U47_ga(x1, x3, x4)
U48_ga(x1, x2, x3)  =  U48_ga(x1, x3)
appendc23_in_ggga(x1, x2, x3, x4)  =  appendc23_in_ggga(x1, x2, x3)
appendc23_out_ggga(x1, x2, x3, x4)  =  appendc23_out_ggga(x1, x2, x3, x4)
U39_ggga(x1, x2, x3, x4, x5, x6)  =  U39_ggga(x1, x2, x3, x4, x6)
U49_ga(x1, x2, x3, x4, x5)  =  U49_ga(x1, x2, x3, x5)
U50_ga(x1, x2, x3, x4, x5)  =  U50_ga(x1, x2, x3, x5)
U51_ga(x1, x2, x3, x4, x5, x6)  =  U51_ga(x1, x2, x3, x5, x6)
U53_ga(x1, x2, x3, x4, x5)  =  U53_ga(x1, x2, x3, x5)
U54_ga(x1, x2, x3, x4, x5)  =  U54_ga(x1, x2, x3, x5)
U55_ga(x1, x2, x3, x4, x5, x6)  =  U55_ga(x1, x2, x3, x5, x6)
U56_ga(x1, x2, x3, x4, x5)  =  U56_ga(x1, x2, x3, x5)
qc78_in_gagga(x1, x2, x3, x4, x5)  =  qc78_in_gagga(x1, x3, x4)
U62_gagga(x1, x2, x3, x4, x5, x6)  =  U62_gagga(x1, x3, x4, x6)
U63_gagga(x1, x2, x3, x4, x5, x6)  =  U63_gagga(x1, x2, x3, x4, x6)
qc78_out_gagga(x1, x2, x3, x4, x5)  =  qc78_out_gagga(x1, x2, x3, x4, x5)
U52_ga(x1, x2, x3, x4, x5)  =  U52_ga(x1, x2, x3, x5)
QSORT1_IN_GA(x1, x2)  =  QSORT1_IN_GA(x1)
U21_GA(x1, x2, x3)  =  U21_GA(x1, x3)
U22_GA(x1, x2, x3, x4)  =  U22_GA(x1, x3, x4)
U23_GA(x1, x2, x3)  =  U23_GA(x1, x3)
APPEND23_IN_GGGA(x1, x2, x3, x4)  =  APPEND23_IN_GGGA(x1, x2, x3)
U1_GGGA(x1, x2, x3, x4, x5, x6)  =  U1_GGGA(x1, x2, x3, x4, x6)
U24_GA(x1, x2, x3, x4, x5)  =  U24_GA(x1, x2, x3, x5)
LE36_IN_GG(x1, x2)  =  LE36_IN_GG(x1, x2)
U2_GG(x1, x2, x3)  =  U2_GG(x1, x2, x3)
U25_GA(x1, x2, x3, x4, x5)  =  U25_GA(x1, x2, x3, x5)
U26_GA(x1, x2, x3, x4, x5)  =  U26_GA(x1, x2, x3, x5)
SPLIT51_IN_GGAA(x1, x2, x3, x4)  =  SPLIT51_IN_GGAA(x1, x2)
U3_GGAA(x1, x2, x3, x4, x5, x6)  =  U3_GGAA(x1, x2, x3, x6)
U4_GGAA(x1, x2, x3, x4, x5, x6)  =  U4_GGAA(x1, x2, x3, x6)
U5_GGAA(x1, x2, x3, x4, x5, x6)  =  U5_GGAA(x1, x2, x3, x6)
U6_GGAA(x1, x2, x3, x4, x5, x6)  =  U6_GGAA(x1, x2, x3, x6)
GT67_IN_GG(x1, x2)  =  GT67_IN_GG(x1, x2)
U9_GG(x1, x2, x3)  =  U9_GG(x1, x2, x3)
U7_GGAA(x1, x2, x3, x4, x5, x6)  =  U7_GGAA(x1, x2, x3, x6)
U8_GGAA(x1, x2, x3, x4, x5, x6)  =  U8_GGAA(x1, x2, x3, x6)
U27_GA(x1, x2, x3, x4, x5)  =  U27_GA(x1, x2, x3, x5)
U28_GA(x1, x2, x3, x4, x5)  =  U28_GA(x1, x2, x3, x5)
U31_GA(x1, x2, x3, x4, x5)  =  U31_GA(x1, x2, x3, x5)
U32_GA(x1, x2, x3, x4, x5)  =  U32_GA(x1, x2, x3, x5)
U33_GA(x1, x2, x3, x4, x5)  =  U33_GA(x1, x2, x3, x5)
U34_GA(x1, x2, x3, x4, x5)  =  U34_GA(x1, x2, x3, x5)
U35_GA(x1, x2, x3, x4, x5)  =  U35_GA(x1, x2, x3, x5)
QSORT79_IN_GA(x1, x2)  =  QSORT79_IN_GA(x1)
U10_GA(x1, x2, x3, x4)  =  U10_GA(x1, x2, x4)
U11_GA(x1, x2, x3, x4)  =  U11_GA(x1, x2, x4)
U12_GA(x1, x2, x3, x4)  =  U12_GA(x1, x2, x4)
U13_GA(x1, x2, x3, x4, x5)  =  U13_GA(x1, x2, x4, x5)
U14_GA(x1, x2, x3, x4)  =  U14_GA(x1, x2, x4)
U15_GA(x1, x2, x3, x4, x5)  =  U15_GA(x1, x2, x4, x5)
U16_GA(x1, x2, x3, x4)  =  U16_GA(x1, x2, x4)
APPEND94_IN_GGGA(x1, x2, x3, x4)  =  APPEND94_IN_GGGA(x1, x2, x3)
U17_GGGA(x1, x2, x3, x4, x5, x6)  =  U17_GGGA(x1, x2, x3, x4, x6)
U36_GA(x1, x2, x3, x4, x5, x6)  =  U36_GA(x1, x2, x3, x5, x6)
U37_GA(x1, x2, x3, x4, x5)  =  U37_GA(x1, x2, x3, x5)
P78_IN_GAGGA(x1, x2, x3, x4, x5)  =  P78_IN_GAGGA(x1, x3, x4)
U18_GAGGA(x1, x2, x3, x4, x5, x6)  =  U18_GAGGA(x1, x3, x4, x6)
U19_GAGGA(x1, x2, x3, x4, x5, x6)  =  U19_GAGGA(x1, x3, x4, x6)
U20_GAGGA(x1, x2, x3, x4, x5, x6)  =  U20_GAGGA(x1, x3, x4, x6)
U29_GA(x1, x2, x3, x4, x5, x6)  =  U29_GA(x1, x2, x3, x5, x6)
U30_GA(x1, x2, x3, x4, x5)  =  U30_GA(x1, x2, x3, x5)

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

(7) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 7 SCCs with 45 less nodes.

(8) Complex Obligation (AND)

(9) Obligation:

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

APPEND94_IN_GGGA(.(T195, T196), T197, T198, .(T195, X295)) → APPEND94_IN_GGGA(T196, T197, T198, X295)

The TRS R consists of the following rules:

qsortc14_in_a([]) → qsortc14_out_a([])
lec36_in_gg(s(T82), s(T83)) → U40_gg(T82, T83, lec36_in_gg(T82, T83))
lec36_in_gg(0, s(T90)) → lec36_out_gg(0, s(T90))
lec36_in_gg(0, 0) → lec36_out_gg(0, 0)
U40_gg(T82, T83, lec36_out_gg(T82, T83)) → lec36_out_gg(s(T82), s(T83))
gtc67_in_gg(s(T144), s(T145)) → U45_gg(T144, T145, gtc67_in_gg(T144, T145))
gtc67_in_gg(s(T150), 0) → gtc67_out_gg(s(T150), 0)
U45_gg(T144, T145, gtc67_out_gg(T144, T145)) → gtc67_out_gg(s(T144), s(T145))
splitc51_in_ggaa([], T101, [], []) → splitc51_out_ggaa([], T101, [], [])
splitc51_in_ggaa(.(T114, T115), T116, .(T114, X167), X168) → U41_ggaa(T114, T115, T116, X167, X168, lec36_in_gg(T114, T116))
U41_ggaa(T114, T115, T116, X167, X168, lec36_out_gg(T114, T116)) → U42_ggaa(T114, T115, T116, X167, X168, splitc51_in_ggaa(T115, T116, X167, X168))
splitc51_in_ggaa(.(T129, T130), T131, X199, .(T129, X200)) → U43_ggaa(T129, T130, T131, X199, X200, gtc67_in_gg(T129, T131))
U43_ggaa(T129, T130, T131, X199, X200, gtc67_out_gg(T129, T131)) → U44_ggaa(T129, T130, T131, X199, X200, splitc51_in_ggaa(T130, T131, X199, X200))
U44_ggaa(T129, T130, T131, X199, X200, splitc51_out_ggaa(T130, T131, X199, X200)) → splitc51_out_ggaa(.(T129, T130), T131, X199, .(T129, X200))
U42_ggaa(T114, T115, T116, X167, X168, splitc51_out_ggaa(T115, T116, X167, X168)) → splitc51_out_ggaa(.(T114, T115), T116, .(T114, X167), X168)
qsortc79_in_ga([], []) → qsortc79_out_ga([], [])
qsortc79_in_ga(.(T163, T164), X265) → U57_ga(T163, T164, X265, splitc51_in_ggaa(T164, T163, T167, T168))
U57_ga(T163, T164, X265, splitc51_out_ggaa(T164, T163, T167, T168)) → U58_ga(T163, T164, X265, T168, qsortc79_in_ga(T167, T171))
U58_ga(T163, T164, X265, T168, qsortc79_out_ga(T167, T171)) → U59_ga(T163, T164, X265, T171, qsortc79_in_ga(T168, T172))
U59_ga(T163, T164, X265, T171, qsortc79_out_ga(T168, T172)) → U60_ga(T163, T164, X265, appendc94_in_ggga(T171, T163, T172, X265))
appendc94_in_ggga([], T185, T186, .(T185, T186)) → appendc94_out_ggga([], T185, T186, .(T185, T186))
appendc94_in_ggga(.(T195, T196), T197, T198, .(T195, X295)) → U61_ggga(T195, T196, T197, T198, X295, appendc94_in_ggga(T196, T197, T198, X295))
U61_ggga(T195, T196, T197, T198, X295, appendc94_out_ggga(T196, T197, T198, X295)) → appendc94_out_ggga(.(T195, T196), T197, T198, .(T195, X295))
U60_ga(T163, T164, X265, appendc94_out_ggga(T171, T163, T172, X265)) → qsortc79_out_ga(.(T163, T164), X265)
qsortc1_in_ga([], []) → qsortc1_out_ga([], [])
qsortc1_in_ga(.(T14, []), T9) → U46_ga(T14, T9, qsortc14_in_a(T17))
U46_ga(T14, T9, qsortc14_out_a(T17)) → U47_ga(T14, T9, T17, qsortc14_in_a(T20))
U47_ga(T14, T9, T17, qsortc14_out_a(T20)) → U48_ga(T14, T9, appendc23_in_ggga(T17, T14, T20, T9))
appendc23_in_ggga([], T33, T34, .(T33, T34)) → appendc23_out_ggga([], T33, T34, .(T33, T34))
appendc23_in_ggga(.(T45, T46), T47, T48, .(T45, T50)) → U39_ggga(T45, T46, T47, T48, T50, appendc23_in_ggga(T46, T47, T48, T50))
U39_ggga(T45, T46, T47, T48, T50, appendc23_out_ggga(T46, T47, T48, T50)) → appendc23_out_ggga(.(T45, T46), T47, T48, .(T45, T50))
U48_ga(T14, T9, appendc23_out_ggga(T17, T14, T20, T9)) → qsortc1_out_ga(.(T14, []), T9)
qsortc1_in_ga(.(T69, .(T67, T68)), T9) → U49_ga(T69, T67, T68, T9, lec36_in_gg(T67, T69))
U49_ga(T69, T67, T68, T9, lec36_out_gg(T67, T69)) → U50_ga(T69, T67, T68, T9, splitc51_in_ggaa(T68, T69, T93, T94))
U50_ga(T69, T67, T68, T9, splitc51_out_ggaa(T68, T69, T93, T94)) → U51_ga(T69, T67, T68, T9, T94, qsortc1_in_ga(.(T67, T93), T155))
qsortc1_in_ga(.(T215, .(T213, T214)), T9) → U53_ga(T215, T213, T214, T9, gtc67_in_gg(T213, T215))
U53_ga(T215, T213, T214, T9, gtc67_out_gg(T213, T215)) → U54_ga(T215, T213, T214, T9, splitc51_in_ggaa(T214, T215, T222, T223))
U54_ga(T215, T213, T214, T9, splitc51_out_ggaa(T214, T215, T222, T223)) → U55_ga(T215, T213, T214, T9, T223, qsortc79_in_ga(T222, T226))
U55_ga(T215, T213, T214, T9, T223, qsortc79_out_ga(T222, T226)) → U56_ga(T215, T213, T214, T9, qc78_in_gagga(.(T213, T223), X13, T226, T215, T9))
qc78_in_gagga(T94, T158, T155, T69, T9) → U62_gagga(T94, T158, T155, T69, T9, qsortc79_in_ga(T94, T158))
U62_gagga(T94, T158, T155, T69, T9, qsortc79_out_ga(T94, T158)) → U63_gagga(T94, T158, T155, T69, T9, appendc23_in_ggga(T155, T69, T158, T9))
U63_gagga(T94, T158, T155, T69, T9, appendc23_out_ggga(T155, T69, T158, T9)) → qc78_out_gagga(T94, T158, T155, T69, T9)
U56_ga(T215, T213, T214, T9, qc78_out_gagga(.(T213, T223), X13, T226, T215, T9)) → qsortc1_out_ga(.(T215, .(T213, T214)), T9)
U51_ga(T69, T67, T68, T9, T94, qsortc1_out_ga(.(T67, T93), T155)) → U52_ga(T69, T67, T68, T9, qc78_in_gagga(T94, X13, T155, T69, T9))
U52_ga(T69, T67, T68, T9, qc78_out_gagga(T94, X13, T155, T69, T9)) → qsortc1_out_ga(.(T69, .(T67, T68)), T9)

The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
[]  =  []
qsortc14_in_a(x1)  =  qsortc14_in_a
qsortc14_out_a(x1)  =  qsortc14_out_a(x1)
s(x1)  =  s(x1)
lec36_in_gg(x1, x2)  =  lec36_in_gg(x1, x2)
U40_gg(x1, x2, x3)  =  U40_gg(x1, x2, x3)
0  =  0
lec36_out_gg(x1, x2)  =  lec36_out_gg(x1, x2)
gtc67_in_gg(x1, x2)  =  gtc67_in_gg(x1, x2)
U45_gg(x1, x2, x3)  =  U45_gg(x1, x2, x3)
gtc67_out_gg(x1, x2)  =  gtc67_out_gg(x1, x2)
splitc51_in_ggaa(x1, x2, x3, x4)  =  splitc51_in_ggaa(x1, x2)
splitc51_out_ggaa(x1, x2, x3, x4)  =  splitc51_out_ggaa(x1, x2, x3, x4)
U41_ggaa(x1, x2, x3, x4, x5, x6)  =  U41_ggaa(x1, x2, x3, x6)
U42_ggaa(x1, x2, x3, x4, x5, x6)  =  U42_ggaa(x1, x2, x3, x6)
U43_ggaa(x1, x2, x3, x4, x5, x6)  =  U43_ggaa(x1, x2, x3, x6)
U44_ggaa(x1, x2, x3, x4, x5, x6)  =  U44_ggaa(x1, x2, x3, x6)
qsortc79_in_ga(x1, x2)  =  qsortc79_in_ga(x1)
qsortc79_out_ga(x1, x2)  =  qsortc79_out_ga(x1, x2)
U57_ga(x1, x2, x3, x4)  =  U57_ga(x1, x2, x4)
U58_ga(x1, x2, x3, x4, x5)  =  U58_ga(x1, x2, x4, x5)
U59_ga(x1, x2, x3, x4, x5)  =  U59_ga(x1, x2, x4, x5)
U60_ga(x1, x2, x3, x4)  =  U60_ga(x1, x2, x4)
appendc94_in_ggga(x1, x2, x3, x4)  =  appendc94_in_ggga(x1, x2, x3)
appendc94_out_ggga(x1, x2, x3, x4)  =  appendc94_out_ggga(x1, x2, x3, x4)
U61_ggga(x1, x2, x3, x4, x5, x6)  =  U61_ggga(x1, x2, x3, x4, x6)
qsortc1_in_ga(x1, x2)  =  qsortc1_in_ga(x1)
qsortc1_out_ga(x1, x2)  =  qsortc1_out_ga(x1, x2)
U46_ga(x1, x2, x3)  =  U46_ga(x1, x3)
U47_ga(x1, x2, x3, x4)  =  U47_ga(x1, x3, x4)
U48_ga(x1, x2, x3)  =  U48_ga(x1, x3)
appendc23_in_ggga(x1, x2, x3, x4)  =  appendc23_in_ggga(x1, x2, x3)
appendc23_out_ggga(x1, x2, x3, x4)  =  appendc23_out_ggga(x1, x2, x3, x4)
U39_ggga(x1, x2, x3, x4, x5, x6)  =  U39_ggga(x1, x2, x3, x4, x6)
U49_ga(x1, x2, x3, x4, x5)  =  U49_ga(x1, x2, x3, x5)
U50_ga(x1, x2, x3, x4, x5)  =  U50_ga(x1, x2, x3, x5)
U51_ga(x1, x2, x3, x4, x5, x6)  =  U51_ga(x1, x2, x3, x5, x6)
U53_ga(x1, x2, x3, x4, x5)  =  U53_ga(x1, x2, x3, x5)
U54_ga(x1, x2, x3, x4, x5)  =  U54_ga(x1, x2, x3, x5)
U55_ga(x1, x2, x3, x4, x5, x6)  =  U55_ga(x1, x2, x3, x5, x6)
U56_ga(x1, x2, x3, x4, x5)  =  U56_ga(x1, x2, x3, x5)
qc78_in_gagga(x1, x2, x3, x4, x5)  =  qc78_in_gagga(x1, x3, x4)
U62_gagga(x1, x2, x3, x4, x5, x6)  =  U62_gagga(x1, x3, x4, x6)
U63_gagga(x1, x2, x3, x4, x5, x6)  =  U63_gagga(x1, x2, x3, x4, x6)
qc78_out_gagga(x1, x2, x3, x4, x5)  =  qc78_out_gagga(x1, x2, x3, x4, x5)
U52_ga(x1, x2, x3, x4, x5)  =  U52_ga(x1, x2, x3, x5)
APPEND94_IN_GGGA(x1, x2, x3, x4)  =  APPEND94_IN_GGGA(x1, x2, x3)

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:

APPEND94_IN_GGGA(.(T195, T196), T197, T198, .(T195, X295)) → APPEND94_IN_GGGA(T196, T197, T198, X295)

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

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:

APPEND94_IN_GGGA(.(T195, T196), T197, T198) → APPEND94_IN_GGGA(T196, T197, T198)

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:

  • APPEND94_IN_GGGA(.(T195, T196), T197, T198) → APPEND94_IN_GGGA(T196, T197, T198)
    The graph contains the following edges 1 > 1, 2 >= 2, 3 >= 3

(15) YES

(16) Obligation:

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

GT67_IN_GG(s(T144), s(T145)) → GT67_IN_GG(T144, T145)

The TRS R consists of the following rules:

qsortc14_in_a([]) → qsortc14_out_a([])
lec36_in_gg(s(T82), s(T83)) → U40_gg(T82, T83, lec36_in_gg(T82, T83))
lec36_in_gg(0, s(T90)) → lec36_out_gg(0, s(T90))
lec36_in_gg(0, 0) → lec36_out_gg(0, 0)
U40_gg(T82, T83, lec36_out_gg(T82, T83)) → lec36_out_gg(s(T82), s(T83))
gtc67_in_gg(s(T144), s(T145)) → U45_gg(T144, T145, gtc67_in_gg(T144, T145))
gtc67_in_gg(s(T150), 0) → gtc67_out_gg(s(T150), 0)
U45_gg(T144, T145, gtc67_out_gg(T144, T145)) → gtc67_out_gg(s(T144), s(T145))
splitc51_in_ggaa([], T101, [], []) → splitc51_out_ggaa([], T101, [], [])
splitc51_in_ggaa(.(T114, T115), T116, .(T114, X167), X168) → U41_ggaa(T114, T115, T116, X167, X168, lec36_in_gg(T114, T116))
U41_ggaa(T114, T115, T116, X167, X168, lec36_out_gg(T114, T116)) → U42_ggaa(T114, T115, T116, X167, X168, splitc51_in_ggaa(T115, T116, X167, X168))
splitc51_in_ggaa(.(T129, T130), T131, X199, .(T129, X200)) → U43_ggaa(T129, T130, T131, X199, X200, gtc67_in_gg(T129, T131))
U43_ggaa(T129, T130, T131, X199, X200, gtc67_out_gg(T129, T131)) → U44_ggaa(T129, T130, T131, X199, X200, splitc51_in_ggaa(T130, T131, X199, X200))
U44_ggaa(T129, T130, T131, X199, X200, splitc51_out_ggaa(T130, T131, X199, X200)) → splitc51_out_ggaa(.(T129, T130), T131, X199, .(T129, X200))
U42_ggaa(T114, T115, T116, X167, X168, splitc51_out_ggaa(T115, T116, X167, X168)) → splitc51_out_ggaa(.(T114, T115), T116, .(T114, X167), X168)
qsortc79_in_ga([], []) → qsortc79_out_ga([], [])
qsortc79_in_ga(.(T163, T164), X265) → U57_ga(T163, T164, X265, splitc51_in_ggaa(T164, T163, T167, T168))
U57_ga(T163, T164, X265, splitc51_out_ggaa(T164, T163, T167, T168)) → U58_ga(T163, T164, X265, T168, qsortc79_in_ga(T167, T171))
U58_ga(T163, T164, X265, T168, qsortc79_out_ga(T167, T171)) → U59_ga(T163, T164, X265, T171, qsortc79_in_ga(T168, T172))
U59_ga(T163, T164, X265, T171, qsortc79_out_ga(T168, T172)) → U60_ga(T163, T164, X265, appendc94_in_ggga(T171, T163, T172, X265))
appendc94_in_ggga([], T185, T186, .(T185, T186)) → appendc94_out_ggga([], T185, T186, .(T185, T186))
appendc94_in_ggga(.(T195, T196), T197, T198, .(T195, X295)) → U61_ggga(T195, T196, T197, T198, X295, appendc94_in_ggga(T196, T197, T198, X295))
U61_ggga(T195, T196, T197, T198, X295, appendc94_out_ggga(T196, T197, T198, X295)) → appendc94_out_ggga(.(T195, T196), T197, T198, .(T195, X295))
U60_ga(T163, T164, X265, appendc94_out_ggga(T171, T163, T172, X265)) → qsortc79_out_ga(.(T163, T164), X265)
qsortc1_in_ga([], []) → qsortc1_out_ga([], [])
qsortc1_in_ga(.(T14, []), T9) → U46_ga(T14, T9, qsortc14_in_a(T17))
U46_ga(T14, T9, qsortc14_out_a(T17)) → U47_ga(T14, T9, T17, qsortc14_in_a(T20))
U47_ga(T14, T9, T17, qsortc14_out_a(T20)) → U48_ga(T14, T9, appendc23_in_ggga(T17, T14, T20, T9))
appendc23_in_ggga([], T33, T34, .(T33, T34)) → appendc23_out_ggga([], T33, T34, .(T33, T34))
appendc23_in_ggga(.(T45, T46), T47, T48, .(T45, T50)) → U39_ggga(T45, T46, T47, T48, T50, appendc23_in_ggga(T46, T47, T48, T50))
U39_ggga(T45, T46, T47, T48, T50, appendc23_out_ggga(T46, T47, T48, T50)) → appendc23_out_ggga(.(T45, T46), T47, T48, .(T45, T50))
U48_ga(T14, T9, appendc23_out_ggga(T17, T14, T20, T9)) → qsortc1_out_ga(.(T14, []), T9)
qsortc1_in_ga(.(T69, .(T67, T68)), T9) → U49_ga(T69, T67, T68, T9, lec36_in_gg(T67, T69))
U49_ga(T69, T67, T68, T9, lec36_out_gg(T67, T69)) → U50_ga(T69, T67, T68, T9, splitc51_in_ggaa(T68, T69, T93, T94))
U50_ga(T69, T67, T68, T9, splitc51_out_ggaa(T68, T69, T93, T94)) → U51_ga(T69, T67, T68, T9, T94, qsortc1_in_ga(.(T67, T93), T155))
qsortc1_in_ga(.(T215, .(T213, T214)), T9) → U53_ga(T215, T213, T214, T9, gtc67_in_gg(T213, T215))
U53_ga(T215, T213, T214, T9, gtc67_out_gg(T213, T215)) → U54_ga(T215, T213, T214, T9, splitc51_in_ggaa(T214, T215, T222, T223))
U54_ga(T215, T213, T214, T9, splitc51_out_ggaa(T214, T215, T222, T223)) → U55_ga(T215, T213, T214, T9, T223, qsortc79_in_ga(T222, T226))
U55_ga(T215, T213, T214, T9, T223, qsortc79_out_ga(T222, T226)) → U56_ga(T215, T213, T214, T9, qc78_in_gagga(.(T213, T223), X13, T226, T215, T9))
qc78_in_gagga(T94, T158, T155, T69, T9) → U62_gagga(T94, T158, T155, T69, T9, qsortc79_in_ga(T94, T158))
U62_gagga(T94, T158, T155, T69, T9, qsortc79_out_ga(T94, T158)) → U63_gagga(T94, T158, T155, T69, T9, appendc23_in_ggga(T155, T69, T158, T9))
U63_gagga(T94, T158, T155, T69, T9, appendc23_out_ggga(T155, T69, T158, T9)) → qc78_out_gagga(T94, T158, T155, T69, T9)
U56_ga(T215, T213, T214, T9, qc78_out_gagga(.(T213, T223), X13, T226, T215, T9)) → qsortc1_out_ga(.(T215, .(T213, T214)), T9)
U51_ga(T69, T67, T68, T9, T94, qsortc1_out_ga(.(T67, T93), T155)) → U52_ga(T69, T67, T68, T9, qc78_in_gagga(T94, X13, T155, T69, T9))
U52_ga(T69, T67, T68, T9, qc78_out_gagga(T94, X13, T155, T69, T9)) → qsortc1_out_ga(.(T69, .(T67, T68)), T9)

The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
[]  =  []
qsortc14_in_a(x1)  =  qsortc14_in_a
qsortc14_out_a(x1)  =  qsortc14_out_a(x1)
s(x1)  =  s(x1)
lec36_in_gg(x1, x2)  =  lec36_in_gg(x1, x2)
U40_gg(x1, x2, x3)  =  U40_gg(x1, x2, x3)
0  =  0
lec36_out_gg(x1, x2)  =  lec36_out_gg(x1, x2)
gtc67_in_gg(x1, x2)  =  gtc67_in_gg(x1, x2)
U45_gg(x1, x2, x3)  =  U45_gg(x1, x2, x3)
gtc67_out_gg(x1, x2)  =  gtc67_out_gg(x1, x2)
splitc51_in_ggaa(x1, x2, x3, x4)  =  splitc51_in_ggaa(x1, x2)
splitc51_out_ggaa(x1, x2, x3, x4)  =  splitc51_out_ggaa(x1, x2, x3, x4)
U41_ggaa(x1, x2, x3, x4, x5, x6)  =  U41_ggaa(x1, x2, x3, x6)
U42_ggaa(x1, x2, x3, x4, x5, x6)  =  U42_ggaa(x1, x2, x3, x6)
U43_ggaa(x1, x2, x3, x4, x5, x6)  =  U43_ggaa(x1, x2, x3, x6)
U44_ggaa(x1, x2, x3, x4, x5, x6)  =  U44_ggaa(x1, x2, x3, x6)
qsortc79_in_ga(x1, x2)  =  qsortc79_in_ga(x1)
qsortc79_out_ga(x1, x2)  =  qsortc79_out_ga(x1, x2)
U57_ga(x1, x2, x3, x4)  =  U57_ga(x1, x2, x4)
U58_ga(x1, x2, x3, x4, x5)  =  U58_ga(x1, x2, x4, x5)
U59_ga(x1, x2, x3, x4, x5)  =  U59_ga(x1, x2, x4, x5)
U60_ga(x1, x2, x3, x4)  =  U60_ga(x1, x2, x4)
appendc94_in_ggga(x1, x2, x3, x4)  =  appendc94_in_ggga(x1, x2, x3)
appendc94_out_ggga(x1, x2, x3, x4)  =  appendc94_out_ggga(x1, x2, x3, x4)
U61_ggga(x1, x2, x3, x4, x5, x6)  =  U61_ggga(x1, x2, x3, x4, x6)
qsortc1_in_ga(x1, x2)  =  qsortc1_in_ga(x1)
qsortc1_out_ga(x1, x2)  =  qsortc1_out_ga(x1, x2)
U46_ga(x1, x2, x3)  =  U46_ga(x1, x3)
U47_ga(x1, x2, x3, x4)  =  U47_ga(x1, x3, x4)
U48_ga(x1, x2, x3)  =  U48_ga(x1, x3)
appendc23_in_ggga(x1, x2, x3, x4)  =  appendc23_in_ggga(x1, x2, x3)
appendc23_out_ggga(x1, x2, x3, x4)  =  appendc23_out_ggga(x1, x2, x3, x4)
U39_ggga(x1, x2, x3, x4, x5, x6)  =  U39_ggga(x1, x2, x3, x4, x6)
U49_ga(x1, x2, x3, x4, x5)  =  U49_ga(x1, x2, x3, x5)
U50_ga(x1, x2, x3, x4, x5)  =  U50_ga(x1, x2, x3, x5)
U51_ga(x1, x2, x3, x4, x5, x6)  =  U51_ga(x1, x2, x3, x5, x6)
U53_ga(x1, x2, x3, x4, x5)  =  U53_ga(x1, x2, x3, x5)
U54_ga(x1, x2, x3, x4, x5)  =  U54_ga(x1, x2, x3, x5)
U55_ga(x1, x2, x3, x4, x5, x6)  =  U55_ga(x1, x2, x3, x5, x6)
U56_ga(x1, x2, x3, x4, x5)  =  U56_ga(x1, x2, x3, x5)
qc78_in_gagga(x1, x2, x3, x4, x5)  =  qc78_in_gagga(x1, x3, x4)
U62_gagga(x1, x2, x3, x4, x5, x6)  =  U62_gagga(x1, x3, x4, x6)
U63_gagga(x1, x2, x3, x4, x5, x6)  =  U63_gagga(x1, x2, x3, x4, x6)
qc78_out_gagga(x1, x2, x3, x4, x5)  =  qc78_out_gagga(x1, x2, x3, x4, x5)
U52_ga(x1, x2, x3, x4, x5)  =  U52_ga(x1, x2, x3, x5)
GT67_IN_GG(x1, x2)  =  GT67_IN_GG(x1, x2)

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:

GT67_IN_GG(s(T144), s(T145)) → GT67_IN_GG(T144, T145)

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

(19) PiDPToQDPProof (EQUIVALENT 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:

GT67_IN_GG(s(T144), s(T145)) → GT67_IN_GG(T144, T145)

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

(21) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • GT67_IN_GG(s(T144), s(T145)) → GT67_IN_GG(T144, T145)
    The graph contains the following edges 1 > 1, 2 > 2

(22) YES

(23) Obligation:

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

LE36_IN_GG(s(T82), s(T83)) → LE36_IN_GG(T82, T83)

The TRS R consists of the following rules:

qsortc14_in_a([]) → qsortc14_out_a([])
lec36_in_gg(s(T82), s(T83)) → U40_gg(T82, T83, lec36_in_gg(T82, T83))
lec36_in_gg(0, s(T90)) → lec36_out_gg(0, s(T90))
lec36_in_gg(0, 0) → lec36_out_gg(0, 0)
U40_gg(T82, T83, lec36_out_gg(T82, T83)) → lec36_out_gg(s(T82), s(T83))
gtc67_in_gg(s(T144), s(T145)) → U45_gg(T144, T145, gtc67_in_gg(T144, T145))
gtc67_in_gg(s(T150), 0) → gtc67_out_gg(s(T150), 0)
U45_gg(T144, T145, gtc67_out_gg(T144, T145)) → gtc67_out_gg(s(T144), s(T145))
splitc51_in_ggaa([], T101, [], []) → splitc51_out_ggaa([], T101, [], [])
splitc51_in_ggaa(.(T114, T115), T116, .(T114, X167), X168) → U41_ggaa(T114, T115, T116, X167, X168, lec36_in_gg(T114, T116))
U41_ggaa(T114, T115, T116, X167, X168, lec36_out_gg(T114, T116)) → U42_ggaa(T114, T115, T116, X167, X168, splitc51_in_ggaa(T115, T116, X167, X168))
splitc51_in_ggaa(.(T129, T130), T131, X199, .(T129, X200)) → U43_ggaa(T129, T130, T131, X199, X200, gtc67_in_gg(T129, T131))
U43_ggaa(T129, T130, T131, X199, X200, gtc67_out_gg(T129, T131)) → U44_ggaa(T129, T130, T131, X199, X200, splitc51_in_ggaa(T130, T131, X199, X200))
U44_ggaa(T129, T130, T131, X199, X200, splitc51_out_ggaa(T130, T131, X199, X200)) → splitc51_out_ggaa(.(T129, T130), T131, X199, .(T129, X200))
U42_ggaa(T114, T115, T116, X167, X168, splitc51_out_ggaa(T115, T116, X167, X168)) → splitc51_out_ggaa(.(T114, T115), T116, .(T114, X167), X168)
qsortc79_in_ga([], []) → qsortc79_out_ga([], [])
qsortc79_in_ga(.(T163, T164), X265) → U57_ga(T163, T164, X265, splitc51_in_ggaa(T164, T163, T167, T168))
U57_ga(T163, T164, X265, splitc51_out_ggaa(T164, T163, T167, T168)) → U58_ga(T163, T164, X265, T168, qsortc79_in_ga(T167, T171))
U58_ga(T163, T164, X265, T168, qsortc79_out_ga(T167, T171)) → U59_ga(T163, T164, X265, T171, qsortc79_in_ga(T168, T172))
U59_ga(T163, T164, X265, T171, qsortc79_out_ga(T168, T172)) → U60_ga(T163, T164, X265, appendc94_in_ggga(T171, T163, T172, X265))
appendc94_in_ggga([], T185, T186, .(T185, T186)) → appendc94_out_ggga([], T185, T186, .(T185, T186))
appendc94_in_ggga(.(T195, T196), T197, T198, .(T195, X295)) → U61_ggga(T195, T196, T197, T198, X295, appendc94_in_ggga(T196, T197, T198, X295))
U61_ggga(T195, T196, T197, T198, X295, appendc94_out_ggga(T196, T197, T198, X295)) → appendc94_out_ggga(.(T195, T196), T197, T198, .(T195, X295))
U60_ga(T163, T164, X265, appendc94_out_ggga(T171, T163, T172, X265)) → qsortc79_out_ga(.(T163, T164), X265)
qsortc1_in_ga([], []) → qsortc1_out_ga([], [])
qsortc1_in_ga(.(T14, []), T9) → U46_ga(T14, T9, qsortc14_in_a(T17))
U46_ga(T14, T9, qsortc14_out_a(T17)) → U47_ga(T14, T9, T17, qsortc14_in_a(T20))
U47_ga(T14, T9, T17, qsortc14_out_a(T20)) → U48_ga(T14, T9, appendc23_in_ggga(T17, T14, T20, T9))
appendc23_in_ggga([], T33, T34, .(T33, T34)) → appendc23_out_ggga([], T33, T34, .(T33, T34))
appendc23_in_ggga(.(T45, T46), T47, T48, .(T45, T50)) → U39_ggga(T45, T46, T47, T48, T50, appendc23_in_ggga(T46, T47, T48, T50))
U39_ggga(T45, T46, T47, T48, T50, appendc23_out_ggga(T46, T47, T48, T50)) → appendc23_out_ggga(.(T45, T46), T47, T48, .(T45, T50))
U48_ga(T14, T9, appendc23_out_ggga(T17, T14, T20, T9)) → qsortc1_out_ga(.(T14, []), T9)
qsortc1_in_ga(.(T69, .(T67, T68)), T9) → U49_ga(T69, T67, T68, T9, lec36_in_gg(T67, T69))
U49_ga(T69, T67, T68, T9, lec36_out_gg(T67, T69)) → U50_ga(T69, T67, T68, T9, splitc51_in_ggaa(T68, T69, T93, T94))
U50_ga(T69, T67, T68, T9, splitc51_out_ggaa(T68, T69, T93, T94)) → U51_ga(T69, T67, T68, T9, T94, qsortc1_in_ga(.(T67, T93), T155))
qsortc1_in_ga(.(T215, .(T213, T214)), T9) → U53_ga(T215, T213, T214, T9, gtc67_in_gg(T213, T215))
U53_ga(T215, T213, T214, T9, gtc67_out_gg(T213, T215)) → U54_ga(T215, T213, T214, T9, splitc51_in_ggaa(T214, T215, T222, T223))
U54_ga(T215, T213, T214, T9, splitc51_out_ggaa(T214, T215, T222, T223)) → U55_ga(T215, T213, T214, T9, T223, qsortc79_in_ga(T222, T226))
U55_ga(T215, T213, T214, T9, T223, qsortc79_out_ga(T222, T226)) → U56_ga(T215, T213, T214, T9, qc78_in_gagga(.(T213, T223), X13, T226, T215, T9))
qc78_in_gagga(T94, T158, T155, T69, T9) → U62_gagga(T94, T158, T155, T69, T9, qsortc79_in_ga(T94, T158))
U62_gagga(T94, T158, T155, T69, T9, qsortc79_out_ga(T94, T158)) → U63_gagga(T94, T158, T155, T69, T9, appendc23_in_ggga(T155, T69, T158, T9))
U63_gagga(T94, T158, T155, T69, T9, appendc23_out_ggga(T155, T69, T158, T9)) → qc78_out_gagga(T94, T158, T155, T69, T9)
U56_ga(T215, T213, T214, T9, qc78_out_gagga(.(T213, T223), X13, T226, T215, T9)) → qsortc1_out_ga(.(T215, .(T213, T214)), T9)
U51_ga(T69, T67, T68, T9, T94, qsortc1_out_ga(.(T67, T93), T155)) → U52_ga(T69, T67, T68, T9, qc78_in_gagga(T94, X13, T155, T69, T9))
U52_ga(T69, T67, T68, T9, qc78_out_gagga(T94, X13, T155, T69, T9)) → qsortc1_out_ga(.(T69, .(T67, T68)), T9)

The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
[]  =  []
qsortc14_in_a(x1)  =  qsortc14_in_a
qsortc14_out_a(x1)  =  qsortc14_out_a(x1)
s(x1)  =  s(x1)
lec36_in_gg(x1, x2)  =  lec36_in_gg(x1, x2)
U40_gg(x1, x2, x3)  =  U40_gg(x1, x2, x3)
0  =  0
lec36_out_gg(x1, x2)  =  lec36_out_gg(x1, x2)
gtc67_in_gg(x1, x2)  =  gtc67_in_gg(x1, x2)
U45_gg(x1, x2, x3)  =  U45_gg(x1, x2, x3)
gtc67_out_gg(x1, x2)  =  gtc67_out_gg(x1, x2)
splitc51_in_ggaa(x1, x2, x3, x4)  =  splitc51_in_ggaa(x1, x2)
splitc51_out_ggaa(x1, x2, x3, x4)  =  splitc51_out_ggaa(x1, x2, x3, x4)
U41_ggaa(x1, x2, x3, x4, x5, x6)  =  U41_ggaa(x1, x2, x3, x6)
U42_ggaa(x1, x2, x3, x4, x5, x6)  =  U42_ggaa(x1, x2, x3, x6)
U43_ggaa(x1, x2, x3, x4, x5, x6)  =  U43_ggaa(x1, x2, x3, x6)
U44_ggaa(x1, x2, x3, x4, x5, x6)  =  U44_ggaa(x1, x2, x3, x6)
qsortc79_in_ga(x1, x2)  =  qsortc79_in_ga(x1)
qsortc79_out_ga(x1, x2)  =  qsortc79_out_ga(x1, x2)
U57_ga(x1, x2, x3, x4)  =  U57_ga(x1, x2, x4)
U58_ga(x1, x2, x3, x4, x5)  =  U58_ga(x1, x2, x4, x5)
U59_ga(x1, x2, x3, x4, x5)  =  U59_ga(x1, x2, x4, x5)
U60_ga(x1, x2, x3, x4)  =  U60_ga(x1, x2, x4)
appendc94_in_ggga(x1, x2, x3, x4)  =  appendc94_in_ggga(x1, x2, x3)
appendc94_out_ggga(x1, x2, x3, x4)  =  appendc94_out_ggga(x1, x2, x3, x4)
U61_ggga(x1, x2, x3, x4, x5, x6)  =  U61_ggga(x1, x2, x3, x4, x6)
qsortc1_in_ga(x1, x2)  =  qsortc1_in_ga(x1)
qsortc1_out_ga(x1, x2)  =  qsortc1_out_ga(x1, x2)
U46_ga(x1, x2, x3)  =  U46_ga(x1, x3)
U47_ga(x1, x2, x3, x4)  =  U47_ga(x1, x3, x4)
U48_ga(x1, x2, x3)  =  U48_ga(x1, x3)
appendc23_in_ggga(x1, x2, x3, x4)  =  appendc23_in_ggga(x1, x2, x3)
appendc23_out_ggga(x1, x2, x3, x4)  =  appendc23_out_ggga(x1, x2, x3, x4)
U39_ggga(x1, x2, x3, x4, x5, x6)  =  U39_ggga(x1, x2, x3, x4, x6)
U49_ga(x1, x2, x3, x4, x5)  =  U49_ga(x1, x2, x3, x5)
U50_ga(x1, x2, x3, x4, x5)  =  U50_ga(x1, x2, x3, x5)
U51_ga(x1, x2, x3, x4, x5, x6)  =  U51_ga(x1, x2, x3, x5, x6)
U53_ga(x1, x2, x3, x4, x5)  =  U53_ga(x1, x2, x3, x5)
U54_ga(x1, x2, x3, x4, x5)  =  U54_ga(x1, x2, x3, x5)
U55_ga(x1, x2, x3, x4, x5, x6)  =  U55_ga(x1, x2, x3, x5, x6)
U56_ga(x1, x2, x3, x4, x5)  =  U56_ga(x1, x2, x3, x5)
qc78_in_gagga(x1, x2, x3, x4, x5)  =  qc78_in_gagga(x1, x3, x4)
U62_gagga(x1, x2, x3, x4, x5, x6)  =  U62_gagga(x1, x3, x4, x6)
U63_gagga(x1, x2, x3, x4, x5, x6)  =  U63_gagga(x1, x2, x3, x4, x6)
qc78_out_gagga(x1, x2, x3, x4, x5)  =  qc78_out_gagga(x1, x2, x3, x4, x5)
U52_ga(x1, x2, x3, x4, x5)  =  U52_ga(x1, x2, x3, x5)
LE36_IN_GG(x1, x2)  =  LE36_IN_GG(x1, x2)

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:

LE36_IN_GG(s(T82), s(T83)) → LE36_IN_GG(T82, T83)

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

(26) PiDPToQDPProof (EQUIVALENT 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:

LE36_IN_GG(s(T82), s(T83)) → LE36_IN_GG(T82, T83)

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

(28) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • LE36_IN_GG(s(T82), s(T83)) → LE36_IN_GG(T82, T83)
    The graph contains the following edges 1 > 1, 2 > 2

(29) YES

(30) Obligation:

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

SPLIT51_IN_GGAA(.(T114, T115), T116, .(T114, X167), X168) → U4_GGAA(T114, T115, T116, X167, X168, lec36_in_gg(T114, T116))
U4_GGAA(T114, T115, T116, X167, X168, lec36_out_gg(T114, T116)) → SPLIT51_IN_GGAA(T115, T116, X167, X168)
SPLIT51_IN_GGAA(.(T129, T130), T131, X199, .(T129, X200)) → U7_GGAA(T129, T130, T131, X199, X200, gtc67_in_gg(T129, T131))
U7_GGAA(T129, T130, T131, X199, X200, gtc67_out_gg(T129, T131)) → SPLIT51_IN_GGAA(T130, T131, X199, X200)

The TRS R consists of the following rules:

qsortc14_in_a([]) → qsortc14_out_a([])
lec36_in_gg(s(T82), s(T83)) → U40_gg(T82, T83, lec36_in_gg(T82, T83))
lec36_in_gg(0, s(T90)) → lec36_out_gg(0, s(T90))
lec36_in_gg(0, 0) → lec36_out_gg(0, 0)
U40_gg(T82, T83, lec36_out_gg(T82, T83)) → lec36_out_gg(s(T82), s(T83))
gtc67_in_gg(s(T144), s(T145)) → U45_gg(T144, T145, gtc67_in_gg(T144, T145))
gtc67_in_gg(s(T150), 0) → gtc67_out_gg(s(T150), 0)
U45_gg(T144, T145, gtc67_out_gg(T144, T145)) → gtc67_out_gg(s(T144), s(T145))
splitc51_in_ggaa([], T101, [], []) → splitc51_out_ggaa([], T101, [], [])
splitc51_in_ggaa(.(T114, T115), T116, .(T114, X167), X168) → U41_ggaa(T114, T115, T116, X167, X168, lec36_in_gg(T114, T116))
U41_ggaa(T114, T115, T116, X167, X168, lec36_out_gg(T114, T116)) → U42_ggaa(T114, T115, T116, X167, X168, splitc51_in_ggaa(T115, T116, X167, X168))
splitc51_in_ggaa(.(T129, T130), T131, X199, .(T129, X200)) → U43_ggaa(T129, T130, T131, X199, X200, gtc67_in_gg(T129, T131))
U43_ggaa(T129, T130, T131, X199, X200, gtc67_out_gg(T129, T131)) → U44_ggaa(T129, T130, T131, X199, X200, splitc51_in_ggaa(T130, T131, X199, X200))
U44_ggaa(T129, T130, T131, X199, X200, splitc51_out_ggaa(T130, T131, X199, X200)) → splitc51_out_ggaa(.(T129, T130), T131, X199, .(T129, X200))
U42_ggaa(T114, T115, T116, X167, X168, splitc51_out_ggaa(T115, T116, X167, X168)) → splitc51_out_ggaa(.(T114, T115), T116, .(T114, X167), X168)
qsortc79_in_ga([], []) → qsortc79_out_ga([], [])
qsortc79_in_ga(.(T163, T164), X265) → U57_ga(T163, T164, X265, splitc51_in_ggaa(T164, T163, T167, T168))
U57_ga(T163, T164, X265, splitc51_out_ggaa(T164, T163, T167, T168)) → U58_ga(T163, T164, X265, T168, qsortc79_in_ga(T167, T171))
U58_ga(T163, T164, X265, T168, qsortc79_out_ga(T167, T171)) → U59_ga(T163, T164, X265, T171, qsortc79_in_ga(T168, T172))
U59_ga(T163, T164, X265, T171, qsortc79_out_ga(T168, T172)) → U60_ga(T163, T164, X265, appendc94_in_ggga(T171, T163, T172, X265))
appendc94_in_ggga([], T185, T186, .(T185, T186)) → appendc94_out_ggga([], T185, T186, .(T185, T186))
appendc94_in_ggga(.(T195, T196), T197, T198, .(T195, X295)) → U61_ggga(T195, T196, T197, T198, X295, appendc94_in_ggga(T196, T197, T198, X295))
U61_ggga(T195, T196, T197, T198, X295, appendc94_out_ggga(T196, T197, T198, X295)) → appendc94_out_ggga(.(T195, T196), T197, T198, .(T195, X295))
U60_ga(T163, T164, X265, appendc94_out_ggga(T171, T163, T172, X265)) → qsortc79_out_ga(.(T163, T164), X265)
qsortc1_in_ga([], []) → qsortc1_out_ga([], [])
qsortc1_in_ga(.(T14, []), T9) → U46_ga(T14, T9, qsortc14_in_a(T17))
U46_ga(T14, T9, qsortc14_out_a(T17)) → U47_ga(T14, T9, T17, qsortc14_in_a(T20))
U47_ga(T14, T9, T17, qsortc14_out_a(T20)) → U48_ga(T14, T9, appendc23_in_ggga(T17, T14, T20, T9))
appendc23_in_ggga([], T33, T34, .(T33, T34)) → appendc23_out_ggga([], T33, T34, .(T33, T34))
appendc23_in_ggga(.(T45, T46), T47, T48, .(T45, T50)) → U39_ggga(T45, T46, T47, T48, T50, appendc23_in_ggga(T46, T47, T48, T50))
U39_ggga(T45, T46, T47, T48, T50, appendc23_out_ggga(T46, T47, T48, T50)) → appendc23_out_ggga(.(T45, T46), T47, T48, .(T45, T50))
U48_ga(T14, T9, appendc23_out_ggga(T17, T14, T20, T9)) → qsortc1_out_ga(.(T14, []), T9)
qsortc1_in_ga(.(T69, .(T67, T68)), T9) → U49_ga(T69, T67, T68, T9, lec36_in_gg(T67, T69))
U49_ga(T69, T67, T68, T9, lec36_out_gg(T67, T69)) → U50_ga(T69, T67, T68, T9, splitc51_in_ggaa(T68, T69, T93, T94))
U50_ga(T69, T67, T68, T9, splitc51_out_ggaa(T68, T69, T93, T94)) → U51_ga(T69, T67, T68, T9, T94, qsortc1_in_ga(.(T67, T93), T155))
qsortc1_in_ga(.(T215, .(T213, T214)), T9) → U53_ga(T215, T213, T214, T9, gtc67_in_gg(T213, T215))
U53_ga(T215, T213, T214, T9, gtc67_out_gg(T213, T215)) → U54_ga(T215, T213, T214, T9, splitc51_in_ggaa(T214, T215, T222, T223))
U54_ga(T215, T213, T214, T9, splitc51_out_ggaa(T214, T215, T222, T223)) → U55_ga(T215, T213, T214, T9, T223, qsortc79_in_ga(T222, T226))
U55_ga(T215, T213, T214, T9, T223, qsortc79_out_ga(T222, T226)) → U56_ga(T215, T213, T214, T9, qc78_in_gagga(.(T213, T223), X13, T226, T215, T9))
qc78_in_gagga(T94, T158, T155, T69, T9) → U62_gagga(T94, T158, T155, T69, T9, qsortc79_in_ga(T94, T158))
U62_gagga(T94, T158, T155, T69, T9, qsortc79_out_ga(T94, T158)) → U63_gagga(T94, T158, T155, T69, T9, appendc23_in_ggga(T155, T69, T158, T9))
U63_gagga(T94, T158, T155, T69, T9, appendc23_out_ggga(T155, T69, T158, T9)) → qc78_out_gagga(T94, T158, T155, T69, T9)
U56_ga(T215, T213, T214, T9, qc78_out_gagga(.(T213, T223), X13, T226, T215, T9)) → qsortc1_out_ga(.(T215, .(T213, T214)), T9)
U51_ga(T69, T67, T68, T9, T94, qsortc1_out_ga(.(T67, T93), T155)) → U52_ga(T69, T67, T68, T9, qc78_in_gagga(T94, X13, T155, T69, T9))
U52_ga(T69, T67, T68, T9, qc78_out_gagga(T94, X13, T155, T69, T9)) → qsortc1_out_ga(.(T69, .(T67, T68)), T9)

The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
[]  =  []
qsortc14_in_a(x1)  =  qsortc14_in_a
qsortc14_out_a(x1)  =  qsortc14_out_a(x1)
s(x1)  =  s(x1)
lec36_in_gg(x1, x2)  =  lec36_in_gg(x1, x2)
U40_gg(x1, x2, x3)  =  U40_gg(x1, x2, x3)
0  =  0
lec36_out_gg(x1, x2)  =  lec36_out_gg(x1, x2)
gtc67_in_gg(x1, x2)  =  gtc67_in_gg(x1, x2)
U45_gg(x1, x2, x3)  =  U45_gg(x1, x2, x3)
gtc67_out_gg(x1, x2)  =  gtc67_out_gg(x1, x2)
splitc51_in_ggaa(x1, x2, x3, x4)  =  splitc51_in_ggaa(x1, x2)
splitc51_out_ggaa(x1, x2, x3, x4)  =  splitc51_out_ggaa(x1, x2, x3, x4)
U41_ggaa(x1, x2, x3, x4, x5, x6)  =  U41_ggaa(x1, x2, x3, x6)
U42_ggaa(x1, x2, x3, x4, x5, x6)  =  U42_ggaa(x1, x2, x3, x6)
U43_ggaa(x1, x2, x3, x4, x5, x6)  =  U43_ggaa(x1, x2, x3, x6)
U44_ggaa(x1, x2, x3, x4, x5, x6)  =  U44_ggaa(x1, x2, x3, x6)
qsortc79_in_ga(x1, x2)  =  qsortc79_in_ga(x1)
qsortc79_out_ga(x1, x2)  =  qsortc79_out_ga(x1, x2)
U57_ga(x1, x2, x3, x4)  =  U57_ga(x1, x2, x4)
U58_ga(x1, x2, x3, x4, x5)  =  U58_ga(x1, x2, x4, x5)
U59_ga(x1, x2, x3, x4, x5)  =  U59_ga(x1, x2, x4, x5)
U60_ga(x1, x2, x3, x4)  =  U60_ga(x1, x2, x4)
appendc94_in_ggga(x1, x2, x3, x4)  =  appendc94_in_ggga(x1, x2, x3)
appendc94_out_ggga(x1, x2, x3, x4)  =  appendc94_out_ggga(x1, x2, x3, x4)
U61_ggga(x1, x2, x3, x4, x5, x6)  =  U61_ggga(x1, x2, x3, x4, x6)
qsortc1_in_ga(x1, x2)  =  qsortc1_in_ga(x1)
qsortc1_out_ga(x1, x2)  =  qsortc1_out_ga(x1, x2)
U46_ga(x1, x2, x3)  =  U46_ga(x1, x3)
U47_ga(x1, x2, x3, x4)  =  U47_ga(x1, x3, x4)
U48_ga(x1, x2, x3)  =  U48_ga(x1, x3)
appendc23_in_ggga(x1, x2, x3, x4)  =  appendc23_in_ggga(x1, x2, x3)
appendc23_out_ggga(x1, x2, x3, x4)  =  appendc23_out_ggga(x1, x2, x3, x4)
U39_ggga(x1, x2, x3, x4, x5, x6)  =  U39_ggga(x1, x2, x3, x4, x6)
U49_ga(x1, x2, x3, x4, x5)  =  U49_ga(x1, x2, x3, x5)
U50_ga(x1, x2, x3, x4, x5)  =  U50_ga(x1, x2, x3, x5)
U51_ga(x1, x2, x3, x4, x5, x6)  =  U51_ga(x1, x2, x3, x5, x6)
U53_ga(x1, x2, x3, x4, x5)  =  U53_ga(x1, x2, x3, x5)
U54_ga(x1, x2, x3, x4, x5)  =  U54_ga(x1, x2, x3, x5)
U55_ga(x1, x2, x3, x4, x5, x6)  =  U55_ga(x1, x2, x3, x5, x6)
U56_ga(x1, x2, x3, x4, x5)  =  U56_ga(x1, x2, x3, x5)
qc78_in_gagga(x1, x2, x3, x4, x5)  =  qc78_in_gagga(x1, x3, x4)
U62_gagga(x1, x2, x3, x4, x5, x6)  =  U62_gagga(x1, x3, x4, x6)
U63_gagga(x1, x2, x3, x4, x5, x6)  =  U63_gagga(x1, x2, x3, x4, x6)
qc78_out_gagga(x1, x2, x3, x4, x5)  =  qc78_out_gagga(x1, x2, x3, x4, x5)
U52_ga(x1, x2, x3, x4, x5)  =  U52_ga(x1, x2, x3, x5)
SPLIT51_IN_GGAA(x1, x2, x3, x4)  =  SPLIT51_IN_GGAA(x1, x2)
U4_GGAA(x1, x2, x3, x4, x5, x6)  =  U4_GGAA(x1, x2, x3, x6)
U7_GGAA(x1, x2, x3, x4, x5, x6)  =  U7_GGAA(x1, x2, x3, 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:

SPLIT51_IN_GGAA(.(T114, T115), T116, .(T114, X167), X168) → U4_GGAA(T114, T115, T116, X167, X168, lec36_in_gg(T114, T116))
U4_GGAA(T114, T115, T116, X167, X168, lec36_out_gg(T114, T116)) → SPLIT51_IN_GGAA(T115, T116, X167, X168)
SPLIT51_IN_GGAA(.(T129, T130), T131, X199, .(T129, X200)) → U7_GGAA(T129, T130, T131, X199, X200, gtc67_in_gg(T129, T131))
U7_GGAA(T129, T130, T131, X199, X200, gtc67_out_gg(T129, T131)) → SPLIT51_IN_GGAA(T130, T131, X199, X200)

The TRS R consists of the following rules:

lec36_in_gg(s(T82), s(T83)) → U40_gg(T82, T83, lec36_in_gg(T82, T83))
lec36_in_gg(0, s(T90)) → lec36_out_gg(0, s(T90))
lec36_in_gg(0, 0) → lec36_out_gg(0, 0)
gtc67_in_gg(s(T144), s(T145)) → U45_gg(T144, T145, gtc67_in_gg(T144, T145))
gtc67_in_gg(s(T150), 0) → gtc67_out_gg(s(T150), 0)
U40_gg(T82, T83, lec36_out_gg(T82, T83)) → lec36_out_gg(s(T82), s(T83))
U45_gg(T144, T145, gtc67_out_gg(T144, T145)) → gtc67_out_gg(s(T144), s(T145))

The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
s(x1)  =  s(x1)
lec36_in_gg(x1, x2)  =  lec36_in_gg(x1, x2)
U40_gg(x1, x2, x3)  =  U40_gg(x1, x2, x3)
0  =  0
lec36_out_gg(x1, x2)  =  lec36_out_gg(x1, x2)
gtc67_in_gg(x1, x2)  =  gtc67_in_gg(x1, x2)
U45_gg(x1, x2, x3)  =  U45_gg(x1, x2, x3)
gtc67_out_gg(x1, x2)  =  gtc67_out_gg(x1, x2)
SPLIT51_IN_GGAA(x1, x2, x3, x4)  =  SPLIT51_IN_GGAA(x1, x2)
U4_GGAA(x1, x2, x3, x4, x5, x6)  =  U4_GGAA(x1, x2, x3, x6)
U7_GGAA(x1, x2, x3, x4, x5, x6)  =  U7_GGAA(x1, x2, x3, 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:

SPLIT51_IN_GGAA(.(T114, T115), T116) → U4_GGAA(T114, T115, T116, lec36_in_gg(T114, T116))
U4_GGAA(T114, T115, T116, lec36_out_gg(T114, T116)) → SPLIT51_IN_GGAA(T115, T116)
SPLIT51_IN_GGAA(.(T129, T130), T131) → U7_GGAA(T129, T130, T131, gtc67_in_gg(T129, T131))
U7_GGAA(T129, T130, T131, gtc67_out_gg(T129, T131)) → SPLIT51_IN_GGAA(T130, T131)

The TRS R consists of the following rules:

lec36_in_gg(s(T82), s(T83)) → U40_gg(T82, T83, lec36_in_gg(T82, T83))
lec36_in_gg(0, s(T90)) → lec36_out_gg(0, s(T90))
lec36_in_gg(0, 0) → lec36_out_gg(0, 0)
gtc67_in_gg(s(T144), s(T145)) → U45_gg(T144, T145, gtc67_in_gg(T144, T145))
gtc67_in_gg(s(T150), 0) → gtc67_out_gg(s(T150), 0)
U40_gg(T82, T83, lec36_out_gg(T82, T83)) → lec36_out_gg(s(T82), s(T83))
U45_gg(T144, T145, gtc67_out_gg(T144, T145)) → gtc67_out_gg(s(T144), s(T145))

The set Q consists of the following terms:

lec36_in_gg(x0, x1)
gtc67_in_gg(x0, x1)
U40_gg(x0, x1, x2)
U45_gg(x0, x1, x2)

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

(35) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • U4_GGAA(T114, T115, T116, lec36_out_gg(T114, T116)) → SPLIT51_IN_GGAA(T115, T116)
    The graph contains the following edges 2 >= 1, 3 >= 2, 4 > 2

  • U7_GGAA(T129, T130, T131, gtc67_out_gg(T129, T131)) → SPLIT51_IN_GGAA(T130, T131)
    The graph contains the following edges 2 >= 1, 3 >= 2, 4 > 2

  • SPLIT51_IN_GGAA(.(T114, T115), T116) → U4_GGAA(T114, T115, T116, lec36_in_gg(T114, T116))
    The graph contains the following edges 1 > 1, 1 > 2, 2 >= 3

  • SPLIT51_IN_GGAA(.(T129, T130), T131) → U7_GGAA(T129, T130, T131, gtc67_in_gg(T129, T131))
    The graph contains the following edges 1 > 1, 1 > 2, 2 >= 3

(36) YES

(37) Obligation:

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

QSORT79_IN_GA(.(T163, T164), X265) → U11_GA(T163, T164, X265, splitc51_in_ggaa(T164, T163, T167, T168))
U11_GA(T163, T164, X265, splitc51_out_ggaa(T164, T163, T167, T168)) → QSORT79_IN_GA(T167, X263)
U11_GA(T163, T164, X265, splitc51_out_ggaa(T164, T163, T167, T168)) → U13_GA(T163, T164, X265, T168, qsortc79_in_ga(T167, T171))
U13_GA(T163, T164, X265, T168, qsortc79_out_ga(T167, T171)) → QSORT79_IN_GA(T168, X264)

The TRS R consists of the following rules:

qsortc14_in_a([]) → qsortc14_out_a([])
lec36_in_gg(s(T82), s(T83)) → U40_gg(T82, T83, lec36_in_gg(T82, T83))
lec36_in_gg(0, s(T90)) → lec36_out_gg(0, s(T90))
lec36_in_gg(0, 0) → lec36_out_gg(0, 0)
U40_gg(T82, T83, lec36_out_gg(T82, T83)) → lec36_out_gg(s(T82), s(T83))
gtc67_in_gg(s(T144), s(T145)) → U45_gg(T144, T145, gtc67_in_gg(T144, T145))
gtc67_in_gg(s(T150), 0) → gtc67_out_gg(s(T150), 0)
U45_gg(T144, T145, gtc67_out_gg(T144, T145)) → gtc67_out_gg(s(T144), s(T145))
splitc51_in_ggaa([], T101, [], []) → splitc51_out_ggaa([], T101, [], [])
splitc51_in_ggaa(.(T114, T115), T116, .(T114, X167), X168) → U41_ggaa(T114, T115, T116, X167, X168, lec36_in_gg(T114, T116))
U41_ggaa(T114, T115, T116, X167, X168, lec36_out_gg(T114, T116)) → U42_ggaa(T114, T115, T116, X167, X168, splitc51_in_ggaa(T115, T116, X167, X168))
splitc51_in_ggaa(.(T129, T130), T131, X199, .(T129, X200)) → U43_ggaa(T129, T130, T131, X199, X200, gtc67_in_gg(T129, T131))
U43_ggaa(T129, T130, T131, X199, X200, gtc67_out_gg(T129, T131)) → U44_ggaa(T129, T130, T131, X199, X200, splitc51_in_ggaa(T130, T131, X199, X200))
U44_ggaa(T129, T130, T131, X199, X200, splitc51_out_ggaa(T130, T131, X199, X200)) → splitc51_out_ggaa(.(T129, T130), T131, X199, .(T129, X200))
U42_ggaa(T114, T115, T116, X167, X168, splitc51_out_ggaa(T115, T116, X167, X168)) → splitc51_out_ggaa(.(T114, T115), T116, .(T114, X167), X168)
qsortc79_in_ga([], []) → qsortc79_out_ga([], [])
qsortc79_in_ga(.(T163, T164), X265) → U57_ga(T163, T164, X265, splitc51_in_ggaa(T164, T163, T167, T168))
U57_ga(T163, T164, X265, splitc51_out_ggaa(T164, T163, T167, T168)) → U58_ga(T163, T164, X265, T168, qsortc79_in_ga(T167, T171))
U58_ga(T163, T164, X265, T168, qsortc79_out_ga(T167, T171)) → U59_ga(T163, T164, X265, T171, qsortc79_in_ga(T168, T172))
U59_ga(T163, T164, X265, T171, qsortc79_out_ga(T168, T172)) → U60_ga(T163, T164, X265, appendc94_in_ggga(T171, T163, T172, X265))
appendc94_in_ggga([], T185, T186, .(T185, T186)) → appendc94_out_ggga([], T185, T186, .(T185, T186))
appendc94_in_ggga(.(T195, T196), T197, T198, .(T195, X295)) → U61_ggga(T195, T196, T197, T198, X295, appendc94_in_ggga(T196, T197, T198, X295))
U61_ggga(T195, T196, T197, T198, X295, appendc94_out_ggga(T196, T197, T198, X295)) → appendc94_out_ggga(.(T195, T196), T197, T198, .(T195, X295))
U60_ga(T163, T164, X265, appendc94_out_ggga(T171, T163, T172, X265)) → qsortc79_out_ga(.(T163, T164), X265)
qsortc1_in_ga([], []) → qsortc1_out_ga([], [])
qsortc1_in_ga(.(T14, []), T9) → U46_ga(T14, T9, qsortc14_in_a(T17))
U46_ga(T14, T9, qsortc14_out_a(T17)) → U47_ga(T14, T9, T17, qsortc14_in_a(T20))
U47_ga(T14, T9, T17, qsortc14_out_a(T20)) → U48_ga(T14, T9, appendc23_in_ggga(T17, T14, T20, T9))
appendc23_in_ggga([], T33, T34, .(T33, T34)) → appendc23_out_ggga([], T33, T34, .(T33, T34))
appendc23_in_ggga(.(T45, T46), T47, T48, .(T45, T50)) → U39_ggga(T45, T46, T47, T48, T50, appendc23_in_ggga(T46, T47, T48, T50))
U39_ggga(T45, T46, T47, T48, T50, appendc23_out_ggga(T46, T47, T48, T50)) → appendc23_out_ggga(.(T45, T46), T47, T48, .(T45, T50))
U48_ga(T14, T9, appendc23_out_ggga(T17, T14, T20, T9)) → qsortc1_out_ga(.(T14, []), T9)
qsortc1_in_ga(.(T69, .(T67, T68)), T9) → U49_ga(T69, T67, T68, T9, lec36_in_gg(T67, T69))
U49_ga(T69, T67, T68, T9, lec36_out_gg(T67, T69)) → U50_ga(T69, T67, T68, T9, splitc51_in_ggaa(T68, T69, T93, T94))
U50_ga(T69, T67, T68, T9, splitc51_out_ggaa(T68, T69, T93, T94)) → U51_ga(T69, T67, T68, T9, T94, qsortc1_in_ga(.(T67, T93), T155))
qsortc1_in_ga(.(T215, .(T213, T214)), T9) → U53_ga(T215, T213, T214, T9, gtc67_in_gg(T213, T215))
U53_ga(T215, T213, T214, T9, gtc67_out_gg(T213, T215)) → U54_ga(T215, T213, T214, T9, splitc51_in_ggaa(T214, T215, T222, T223))
U54_ga(T215, T213, T214, T9, splitc51_out_ggaa(T214, T215, T222, T223)) → U55_ga(T215, T213, T214, T9, T223, qsortc79_in_ga(T222, T226))
U55_ga(T215, T213, T214, T9, T223, qsortc79_out_ga(T222, T226)) → U56_ga(T215, T213, T214, T9, qc78_in_gagga(.(T213, T223), X13, T226, T215, T9))
qc78_in_gagga(T94, T158, T155, T69, T9) → U62_gagga(T94, T158, T155, T69, T9, qsortc79_in_ga(T94, T158))
U62_gagga(T94, T158, T155, T69, T9, qsortc79_out_ga(T94, T158)) → U63_gagga(T94, T158, T155, T69, T9, appendc23_in_ggga(T155, T69, T158, T9))
U63_gagga(T94, T158, T155, T69, T9, appendc23_out_ggga(T155, T69, T158, T9)) → qc78_out_gagga(T94, T158, T155, T69, T9)
U56_ga(T215, T213, T214, T9, qc78_out_gagga(.(T213, T223), X13, T226, T215, T9)) → qsortc1_out_ga(.(T215, .(T213, T214)), T9)
U51_ga(T69, T67, T68, T9, T94, qsortc1_out_ga(.(T67, T93), T155)) → U52_ga(T69, T67, T68, T9, qc78_in_gagga(T94, X13, T155, T69, T9))
U52_ga(T69, T67, T68, T9, qc78_out_gagga(T94, X13, T155, T69, T9)) → qsortc1_out_ga(.(T69, .(T67, T68)), T9)

The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
[]  =  []
qsortc14_in_a(x1)  =  qsortc14_in_a
qsortc14_out_a(x1)  =  qsortc14_out_a(x1)
s(x1)  =  s(x1)
lec36_in_gg(x1, x2)  =  lec36_in_gg(x1, x2)
U40_gg(x1, x2, x3)  =  U40_gg(x1, x2, x3)
0  =  0
lec36_out_gg(x1, x2)  =  lec36_out_gg(x1, x2)
gtc67_in_gg(x1, x2)  =  gtc67_in_gg(x1, x2)
U45_gg(x1, x2, x3)  =  U45_gg(x1, x2, x3)
gtc67_out_gg(x1, x2)  =  gtc67_out_gg(x1, x2)
splitc51_in_ggaa(x1, x2, x3, x4)  =  splitc51_in_ggaa(x1, x2)
splitc51_out_ggaa(x1, x2, x3, x4)  =  splitc51_out_ggaa(x1, x2, x3, x4)
U41_ggaa(x1, x2, x3, x4, x5, x6)  =  U41_ggaa(x1, x2, x3, x6)
U42_ggaa(x1, x2, x3, x4, x5, x6)  =  U42_ggaa(x1, x2, x3, x6)
U43_ggaa(x1, x2, x3, x4, x5, x6)  =  U43_ggaa(x1, x2, x3, x6)
U44_ggaa(x1, x2, x3, x4, x5, x6)  =  U44_ggaa(x1, x2, x3, x6)
qsortc79_in_ga(x1, x2)  =  qsortc79_in_ga(x1)
qsortc79_out_ga(x1, x2)  =  qsortc79_out_ga(x1, x2)
U57_ga(x1, x2, x3, x4)  =  U57_ga(x1, x2, x4)
U58_ga(x1, x2, x3, x4, x5)  =  U58_ga(x1, x2, x4, x5)
U59_ga(x1, x2, x3, x4, x5)  =  U59_ga(x1, x2, x4, x5)
U60_ga(x1, x2, x3, x4)  =  U60_ga(x1, x2, x4)
appendc94_in_ggga(x1, x2, x3, x4)  =  appendc94_in_ggga(x1, x2, x3)
appendc94_out_ggga(x1, x2, x3, x4)  =  appendc94_out_ggga(x1, x2, x3, x4)
U61_ggga(x1, x2, x3, x4, x5, x6)  =  U61_ggga(x1, x2, x3, x4, x6)
qsortc1_in_ga(x1, x2)  =  qsortc1_in_ga(x1)
qsortc1_out_ga(x1, x2)  =  qsortc1_out_ga(x1, x2)
U46_ga(x1, x2, x3)  =  U46_ga(x1, x3)
U47_ga(x1, x2, x3, x4)  =  U47_ga(x1, x3, x4)
U48_ga(x1, x2, x3)  =  U48_ga(x1, x3)
appendc23_in_ggga(x1, x2, x3, x4)  =  appendc23_in_ggga(x1, x2, x3)
appendc23_out_ggga(x1, x2, x3, x4)  =  appendc23_out_ggga(x1, x2, x3, x4)
U39_ggga(x1, x2, x3, x4, x5, x6)  =  U39_ggga(x1, x2, x3, x4, x6)
U49_ga(x1, x2, x3, x4, x5)  =  U49_ga(x1, x2, x3, x5)
U50_ga(x1, x2, x3, x4, x5)  =  U50_ga(x1, x2, x3, x5)
U51_ga(x1, x2, x3, x4, x5, x6)  =  U51_ga(x1, x2, x3, x5, x6)
U53_ga(x1, x2, x3, x4, x5)  =  U53_ga(x1, x2, x3, x5)
U54_ga(x1, x2, x3, x4, x5)  =  U54_ga(x1, x2, x3, x5)
U55_ga(x1, x2, x3, x4, x5, x6)  =  U55_ga(x1, x2, x3, x5, x6)
U56_ga(x1, x2, x3, x4, x5)  =  U56_ga(x1, x2, x3, x5)
qc78_in_gagga(x1, x2, x3, x4, x5)  =  qc78_in_gagga(x1, x3, x4)
U62_gagga(x1, x2, x3, x4, x5, x6)  =  U62_gagga(x1, x3, x4, x6)
U63_gagga(x1, x2, x3, x4, x5, x6)  =  U63_gagga(x1, x2, x3, x4, x6)
qc78_out_gagga(x1, x2, x3, x4, x5)  =  qc78_out_gagga(x1, x2, x3, x4, x5)
U52_ga(x1, x2, x3, x4, x5)  =  U52_ga(x1, x2, x3, x5)
QSORT79_IN_GA(x1, x2)  =  QSORT79_IN_GA(x1)
U11_GA(x1, x2, x3, x4)  =  U11_GA(x1, x2, x4)
U13_GA(x1, x2, x3, x4, x5)  =  U13_GA(x1, x2, x4, x5)

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

(38) UsableRulesProof (EQUIVALENT transformation)

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

(39) Obligation:

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

QSORT79_IN_GA(.(T163, T164), X265) → U11_GA(T163, T164, X265, splitc51_in_ggaa(T164, T163, T167, T168))
U11_GA(T163, T164, X265, splitc51_out_ggaa(T164, T163, T167, T168)) → QSORT79_IN_GA(T167, X263)
U11_GA(T163, T164, X265, splitc51_out_ggaa(T164, T163, T167, T168)) → U13_GA(T163, T164, X265, T168, qsortc79_in_ga(T167, T171))
U13_GA(T163, T164, X265, T168, qsortc79_out_ga(T167, T171)) → QSORT79_IN_GA(T168, X264)

The TRS R consists of the following rules:

splitc51_in_ggaa([], T101, [], []) → splitc51_out_ggaa([], T101, [], [])
splitc51_in_ggaa(.(T114, T115), T116, .(T114, X167), X168) → U41_ggaa(T114, T115, T116, X167, X168, lec36_in_gg(T114, T116))
splitc51_in_ggaa(.(T129, T130), T131, X199, .(T129, X200)) → U43_ggaa(T129, T130, T131, X199, X200, gtc67_in_gg(T129, T131))
qsortc79_in_ga([], []) → qsortc79_out_ga([], [])
qsortc79_in_ga(.(T163, T164), X265) → U57_ga(T163, T164, X265, splitc51_in_ggaa(T164, T163, T167, T168))
U41_ggaa(T114, T115, T116, X167, X168, lec36_out_gg(T114, T116)) → U42_ggaa(T114, T115, T116, X167, X168, splitc51_in_ggaa(T115, T116, X167, X168))
U43_ggaa(T129, T130, T131, X199, X200, gtc67_out_gg(T129, T131)) → U44_ggaa(T129, T130, T131, X199, X200, splitc51_in_ggaa(T130, T131, X199, X200))
U57_ga(T163, T164, X265, splitc51_out_ggaa(T164, T163, T167, T168)) → U58_ga(T163, T164, X265, T168, qsortc79_in_ga(T167, T171))
lec36_in_gg(s(T82), s(T83)) → U40_gg(T82, T83, lec36_in_gg(T82, T83))
lec36_in_gg(0, s(T90)) → lec36_out_gg(0, s(T90))
lec36_in_gg(0, 0) → lec36_out_gg(0, 0)
U42_ggaa(T114, T115, T116, X167, X168, splitc51_out_ggaa(T115, T116, X167, X168)) → splitc51_out_ggaa(.(T114, T115), T116, .(T114, X167), X168)
gtc67_in_gg(s(T144), s(T145)) → U45_gg(T144, T145, gtc67_in_gg(T144, T145))
gtc67_in_gg(s(T150), 0) → gtc67_out_gg(s(T150), 0)
U44_ggaa(T129, T130, T131, X199, X200, splitc51_out_ggaa(T130, T131, X199, X200)) → splitc51_out_ggaa(.(T129, T130), T131, X199, .(T129, X200))
U58_ga(T163, T164, X265, T168, qsortc79_out_ga(T167, T171)) → U59_ga(T163, T164, X265, T171, qsortc79_in_ga(T168, T172))
U40_gg(T82, T83, lec36_out_gg(T82, T83)) → lec36_out_gg(s(T82), s(T83))
U45_gg(T144, T145, gtc67_out_gg(T144, T145)) → gtc67_out_gg(s(T144), s(T145))
U59_ga(T163, T164, X265, T171, qsortc79_out_ga(T168, T172)) → U60_ga(T163, T164, X265, appendc94_in_ggga(T171, T163, T172, X265))
U60_ga(T163, T164, X265, appendc94_out_ggga(T171, T163, T172, X265)) → qsortc79_out_ga(.(T163, T164), X265)
appendc94_in_ggga([], T185, T186, .(T185, T186)) → appendc94_out_ggga([], T185, T186, .(T185, T186))
appendc94_in_ggga(.(T195, T196), T197, T198, .(T195, X295)) → U61_ggga(T195, T196, T197, T198, X295, appendc94_in_ggga(T196, T197, T198, X295))
U61_ggga(T195, T196, T197, T198, X295, appendc94_out_ggga(T196, T197, T198, X295)) → appendc94_out_ggga(.(T195, T196), T197, T198, .(T195, X295))

The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
[]  =  []
s(x1)  =  s(x1)
lec36_in_gg(x1, x2)  =  lec36_in_gg(x1, x2)
U40_gg(x1, x2, x3)  =  U40_gg(x1, x2, x3)
0  =  0
lec36_out_gg(x1, x2)  =  lec36_out_gg(x1, x2)
gtc67_in_gg(x1, x2)  =  gtc67_in_gg(x1, x2)
U45_gg(x1, x2, x3)  =  U45_gg(x1, x2, x3)
gtc67_out_gg(x1, x2)  =  gtc67_out_gg(x1, x2)
splitc51_in_ggaa(x1, x2, x3, x4)  =  splitc51_in_ggaa(x1, x2)
splitc51_out_ggaa(x1, x2, x3, x4)  =  splitc51_out_ggaa(x1, x2, x3, x4)
U41_ggaa(x1, x2, x3, x4, x5, x6)  =  U41_ggaa(x1, x2, x3, x6)
U42_ggaa(x1, x2, x3, x4, x5, x6)  =  U42_ggaa(x1, x2, x3, x6)
U43_ggaa(x1, x2, x3, x4, x5, x6)  =  U43_ggaa(x1, x2, x3, x6)
U44_ggaa(x1, x2, x3, x4, x5, x6)  =  U44_ggaa(x1, x2, x3, x6)
qsortc79_in_ga(x1, x2)  =  qsortc79_in_ga(x1)
qsortc79_out_ga(x1, x2)  =  qsortc79_out_ga(x1, x2)
U57_ga(x1, x2, x3, x4)  =  U57_ga(x1, x2, x4)
U58_ga(x1, x2, x3, x4, x5)  =  U58_ga(x1, x2, x4, x5)
U59_ga(x1, x2, x3, x4, x5)  =  U59_ga(x1, x2, x4, x5)
U60_ga(x1, x2, x3, x4)  =  U60_ga(x1, x2, x4)
appendc94_in_ggga(x1, x2, x3, x4)  =  appendc94_in_ggga(x1, x2, x3)
appendc94_out_ggga(x1, x2, x3, x4)  =  appendc94_out_ggga(x1, x2, x3, x4)
U61_ggga(x1, x2, x3, x4, x5, x6)  =  U61_ggga(x1, x2, x3, x4, x6)
QSORT79_IN_GA(x1, x2)  =  QSORT79_IN_GA(x1)
U11_GA(x1, x2, x3, x4)  =  U11_GA(x1, x2, x4)
U13_GA(x1, x2, x3, x4, x5)  =  U13_GA(x1, x2, x4, x5)

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

(40) PiDPToQDPProof (SOUND transformation)

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

(41) Obligation:

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

QSORT79_IN_GA(.(T163, T164)) → U11_GA(T163, T164, splitc51_in_ggaa(T164, T163))
U11_GA(T163, T164, splitc51_out_ggaa(T164, T163, T167, T168)) → QSORT79_IN_GA(T167)
U11_GA(T163, T164, splitc51_out_ggaa(T164, T163, T167, T168)) → U13_GA(T163, T164, T168, qsortc79_in_ga(T167))
U13_GA(T163, T164, T168, qsortc79_out_ga(T167, T171)) → QSORT79_IN_GA(T168)

The TRS R consists of the following rules:

splitc51_in_ggaa([], T101) → splitc51_out_ggaa([], T101, [], [])
splitc51_in_ggaa(.(T114, T115), T116) → U41_ggaa(T114, T115, T116, lec36_in_gg(T114, T116))
splitc51_in_ggaa(.(T129, T130), T131) → U43_ggaa(T129, T130, T131, gtc67_in_gg(T129, T131))
qsortc79_in_ga([]) → qsortc79_out_ga([], [])
qsortc79_in_ga(.(T163, T164)) → U57_ga(T163, T164, splitc51_in_ggaa(T164, T163))
U41_ggaa(T114, T115, T116, lec36_out_gg(T114, T116)) → U42_ggaa(T114, T115, T116, splitc51_in_ggaa(T115, T116))
U43_ggaa(T129, T130, T131, gtc67_out_gg(T129, T131)) → U44_ggaa(T129, T130, T131, splitc51_in_ggaa(T130, T131))
U57_ga(T163, T164, splitc51_out_ggaa(T164, T163, T167, T168)) → U58_ga(T163, T164, T168, qsortc79_in_ga(T167))
lec36_in_gg(s(T82), s(T83)) → U40_gg(T82, T83, lec36_in_gg(T82, T83))
lec36_in_gg(0, s(T90)) → lec36_out_gg(0, s(T90))
lec36_in_gg(0, 0) → lec36_out_gg(0, 0)
U42_ggaa(T114, T115, T116, splitc51_out_ggaa(T115, T116, X167, X168)) → splitc51_out_ggaa(.(T114, T115), T116, .(T114, X167), X168)
gtc67_in_gg(s(T144), s(T145)) → U45_gg(T144, T145, gtc67_in_gg(T144, T145))
gtc67_in_gg(s(T150), 0) → gtc67_out_gg(s(T150), 0)
U44_ggaa(T129, T130, T131, splitc51_out_ggaa(T130, T131, X199, X200)) → splitc51_out_ggaa(.(T129, T130), T131, X199, .(T129, X200))
U58_ga(T163, T164, T168, qsortc79_out_ga(T167, T171)) → U59_ga(T163, T164, T171, qsortc79_in_ga(T168))
U40_gg(T82, T83, lec36_out_gg(T82, T83)) → lec36_out_gg(s(T82), s(T83))
U45_gg(T144, T145, gtc67_out_gg(T144, T145)) → gtc67_out_gg(s(T144), s(T145))
U59_ga(T163, T164, T171, qsortc79_out_ga(T168, T172)) → U60_ga(T163, T164, appendc94_in_ggga(T171, T163, T172))
U60_ga(T163, T164, appendc94_out_ggga(T171, T163, T172, X265)) → qsortc79_out_ga(.(T163, T164), X265)
appendc94_in_ggga([], T185, T186) → appendc94_out_ggga([], T185, T186, .(T185, T186))
appendc94_in_ggga(.(T195, T196), T197, T198) → U61_ggga(T195, T196, T197, T198, appendc94_in_ggga(T196, T197, T198))
U61_ggga(T195, T196, T197, T198, appendc94_out_ggga(T196, T197, T198, X295)) → appendc94_out_ggga(.(T195, T196), T197, T198, .(T195, X295))

The set Q consists of the following terms:

splitc51_in_ggaa(x0, x1)
qsortc79_in_ga(x0)
U41_ggaa(x0, x1, x2, x3)
U43_ggaa(x0, x1, x2, x3)
U57_ga(x0, x1, x2)
lec36_in_gg(x0, x1)
U42_ggaa(x0, x1, x2, x3)
gtc67_in_gg(x0, x1)
U44_ggaa(x0, x1, x2, x3)
U58_ga(x0, x1, x2, x3)
U40_gg(x0, x1, x2)
U45_gg(x0, x1, x2)
U59_ga(x0, x1, x2, x3)
U60_ga(x0, x1, x2)
appendc94_in_ggga(x0, x1, x2)
U61_ggga(x0, x1, x2, x3, x4)

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

(42) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


QSORT79_IN_GA(.(T163, T164)) → U11_GA(T163, T164, splitc51_in_ggaa(T164, T163))
The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial interpretation [POLO]:

POL(.(x1, x2)) = 1 + x2   
POL(0) = 0   
POL(QSORT79_IN_GA(x1)) = x1   
POL(U11_GA(x1, x2, x3)) = x3   
POL(U13_GA(x1, x2, x3, x4)) = x3   
POL(U40_gg(x1, x2, x3)) = 0   
POL(U41_ggaa(x1, x2, x3, x4)) = 1 + x2   
POL(U42_ggaa(x1, x2, x3, x4)) = 1 + x4   
POL(U43_ggaa(x1, x2, x3, x4)) = 1 + x2   
POL(U44_ggaa(x1, x2, x3, x4)) = 1 + x4   
POL(U45_gg(x1, x2, x3)) = 0   
POL(U57_ga(x1, x2, x3)) = 0   
POL(U58_ga(x1, x2, x3, x4)) = 0   
POL(U59_ga(x1, x2, x3, x4)) = 0   
POL(U60_ga(x1, x2, x3)) = 0   
POL(U61_ggga(x1, x2, x3, x4, x5)) = 0   
POL([]) = 0   
POL(appendc94_in_ggga(x1, x2, x3)) = 0   
POL(appendc94_out_ggga(x1, x2, x3, x4)) = 0   
POL(gtc67_in_gg(x1, x2)) = 0   
POL(gtc67_out_gg(x1, x2)) = 0   
POL(lec36_in_gg(x1, x2)) = 0   
POL(lec36_out_gg(x1, x2)) = 0   
POL(qsortc79_in_ga(x1)) = 0   
POL(qsortc79_out_ga(x1, x2)) = 0   
POL(s(x1)) = 0   
POL(splitc51_in_ggaa(x1, x2)) = x1   
POL(splitc51_out_ggaa(x1, x2, x3, x4)) = x3 + x4   

The following usable rules [FROCOS05] were oriented:

splitc51_in_ggaa([], T101) → splitc51_out_ggaa([], T101, [], [])
splitc51_in_ggaa(.(T114, T115), T116) → U41_ggaa(T114, T115, T116, lec36_in_gg(T114, T116))
splitc51_in_ggaa(.(T129, T130), T131) → U43_ggaa(T129, T130, T131, gtc67_in_gg(T129, T131))
U41_ggaa(T114, T115, T116, lec36_out_gg(T114, T116)) → U42_ggaa(T114, T115, T116, splitc51_in_ggaa(T115, T116))
U42_ggaa(T114, T115, T116, splitc51_out_ggaa(T115, T116, X167, X168)) → splitc51_out_ggaa(.(T114, T115), T116, .(T114, X167), X168)
U43_ggaa(T129, T130, T131, gtc67_out_gg(T129, T131)) → U44_ggaa(T129, T130, T131, splitc51_in_ggaa(T130, T131))
U44_ggaa(T129, T130, T131, splitc51_out_ggaa(T130, T131, X199, X200)) → splitc51_out_ggaa(.(T129, T130), T131, X199, .(T129, X200))

(43) Obligation:

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

U11_GA(T163, T164, splitc51_out_ggaa(T164, T163, T167, T168)) → QSORT79_IN_GA(T167)
U11_GA(T163, T164, splitc51_out_ggaa(T164, T163, T167, T168)) → U13_GA(T163, T164, T168, qsortc79_in_ga(T167))
U13_GA(T163, T164, T168, qsortc79_out_ga(T167, T171)) → QSORT79_IN_GA(T168)

The TRS R consists of the following rules:

splitc51_in_ggaa([], T101) → splitc51_out_ggaa([], T101, [], [])
splitc51_in_ggaa(.(T114, T115), T116) → U41_ggaa(T114, T115, T116, lec36_in_gg(T114, T116))
splitc51_in_ggaa(.(T129, T130), T131) → U43_ggaa(T129, T130, T131, gtc67_in_gg(T129, T131))
qsortc79_in_ga([]) → qsortc79_out_ga([], [])
qsortc79_in_ga(.(T163, T164)) → U57_ga(T163, T164, splitc51_in_ggaa(T164, T163))
U41_ggaa(T114, T115, T116, lec36_out_gg(T114, T116)) → U42_ggaa(T114, T115, T116, splitc51_in_ggaa(T115, T116))
U43_ggaa(T129, T130, T131, gtc67_out_gg(T129, T131)) → U44_ggaa(T129, T130, T131, splitc51_in_ggaa(T130, T131))
U57_ga(T163, T164, splitc51_out_ggaa(T164, T163, T167, T168)) → U58_ga(T163, T164, T168, qsortc79_in_ga(T167))
lec36_in_gg(s(T82), s(T83)) → U40_gg(T82, T83, lec36_in_gg(T82, T83))
lec36_in_gg(0, s(T90)) → lec36_out_gg(0, s(T90))
lec36_in_gg(0, 0) → lec36_out_gg(0, 0)
U42_ggaa(T114, T115, T116, splitc51_out_ggaa(T115, T116, X167, X168)) → splitc51_out_ggaa(.(T114, T115), T116, .(T114, X167), X168)
gtc67_in_gg(s(T144), s(T145)) → U45_gg(T144, T145, gtc67_in_gg(T144, T145))
gtc67_in_gg(s(T150), 0) → gtc67_out_gg(s(T150), 0)
U44_ggaa(T129, T130, T131, splitc51_out_ggaa(T130, T131, X199, X200)) → splitc51_out_ggaa(.(T129, T130), T131, X199, .(T129, X200))
U58_ga(T163, T164, T168, qsortc79_out_ga(T167, T171)) → U59_ga(T163, T164, T171, qsortc79_in_ga(T168))
U40_gg(T82, T83, lec36_out_gg(T82, T83)) → lec36_out_gg(s(T82), s(T83))
U45_gg(T144, T145, gtc67_out_gg(T144, T145)) → gtc67_out_gg(s(T144), s(T145))
U59_ga(T163, T164, T171, qsortc79_out_ga(T168, T172)) → U60_ga(T163, T164, appendc94_in_ggga(T171, T163, T172))
U60_ga(T163, T164, appendc94_out_ggga(T171, T163, T172, X265)) → qsortc79_out_ga(.(T163, T164), X265)
appendc94_in_ggga([], T185, T186) → appendc94_out_ggga([], T185, T186, .(T185, T186))
appendc94_in_ggga(.(T195, T196), T197, T198) → U61_ggga(T195, T196, T197, T198, appendc94_in_ggga(T196, T197, T198))
U61_ggga(T195, T196, T197, T198, appendc94_out_ggga(T196, T197, T198, X295)) → appendc94_out_ggga(.(T195, T196), T197, T198, .(T195, X295))

The set Q consists of the following terms:

splitc51_in_ggaa(x0, x1)
qsortc79_in_ga(x0)
U41_ggaa(x0, x1, x2, x3)
U43_ggaa(x0, x1, x2, x3)
U57_ga(x0, x1, x2)
lec36_in_gg(x0, x1)
U42_ggaa(x0, x1, x2, x3)
gtc67_in_gg(x0, x1)
U44_ggaa(x0, x1, x2, x3)
U58_ga(x0, x1, x2, x3)
U40_gg(x0, x1, x2)
U45_gg(x0, x1, x2)
U59_ga(x0, x1, x2, x3)
U60_ga(x0, x1, x2)
appendc94_in_ggga(x0, x1, x2)
U61_ggga(x0, x1, x2, x3, x4)

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

(44) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 3 less nodes.

(45) TRUE

(46) Obligation:

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

APPEND23_IN_GGGA(.(T45, T46), T47, T48, .(T45, T50)) → APPEND23_IN_GGGA(T46, T47, T48, T50)

The TRS R consists of the following rules:

qsortc14_in_a([]) → qsortc14_out_a([])
lec36_in_gg(s(T82), s(T83)) → U40_gg(T82, T83, lec36_in_gg(T82, T83))
lec36_in_gg(0, s(T90)) → lec36_out_gg(0, s(T90))
lec36_in_gg(0, 0) → lec36_out_gg(0, 0)
U40_gg(T82, T83, lec36_out_gg(T82, T83)) → lec36_out_gg(s(T82), s(T83))
gtc67_in_gg(s(T144), s(T145)) → U45_gg(T144, T145, gtc67_in_gg(T144, T145))
gtc67_in_gg(s(T150), 0) → gtc67_out_gg(s(T150), 0)
U45_gg(T144, T145, gtc67_out_gg(T144, T145)) → gtc67_out_gg(s(T144), s(T145))
splitc51_in_ggaa([], T101, [], []) → splitc51_out_ggaa([], T101, [], [])
splitc51_in_ggaa(.(T114, T115), T116, .(T114, X167), X168) → U41_ggaa(T114, T115, T116, X167, X168, lec36_in_gg(T114, T116))
U41_ggaa(T114, T115, T116, X167, X168, lec36_out_gg(T114, T116)) → U42_ggaa(T114, T115, T116, X167, X168, splitc51_in_ggaa(T115, T116, X167, X168))
splitc51_in_ggaa(.(T129, T130), T131, X199, .(T129, X200)) → U43_ggaa(T129, T130, T131, X199, X200, gtc67_in_gg(T129, T131))
U43_ggaa(T129, T130, T131, X199, X200, gtc67_out_gg(T129, T131)) → U44_ggaa(T129, T130, T131, X199, X200, splitc51_in_ggaa(T130, T131, X199, X200))
U44_ggaa(T129, T130, T131, X199, X200, splitc51_out_ggaa(T130, T131, X199, X200)) → splitc51_out_ggaa(.(T129, T130), T131, X199, .(T129, X200))
U42_ggaa(T114, T115, T116, X167, X168, splitc51_out_ggaa(T115, T116, X167, X168)) → splitc51_out_ggaa(.(T114, T115), T116, .(T114, X167), X168)
qsortc79_in_ga([], []) → qsortc79_out_ga([], [])
qsortc79_in_ga(.(T163, T164), X265) → U57_ga(T163, T164, X265, splitc51_in_ggaa(T164, T163, T167, T168))
U57_ga(T163, T164, X265, splitc51_out_ggaa(T164, T163, T167, T168)) → U58_ga(T163, T164, X265, T168, qsortc79_in_ga(T167, T171))
U58_ga(T163, T164, X265, T168, qsortc79_out_ga(T167, T171)) → U59_ga(T163, T164, X265, T171, qsortc79_in_ga(T168, T172))
U59_ga(T163, T164, X265, T171, qsortc79_out_ga(T168, T172)) → U60_ga(T163, T164, X265, appendc94_in_ggga(T171, T163, T172, X265))
appendc94_in_ggga([], T185, T186, .(T185, T186)) → appendc94_out_ggga([], T185, T186, .(T185, T186))
appendc94_in_ggga(.(T195, T196), T197, T198, .(T195, X295)) → U61_ggga(T195, T196, T197, T198, X295, appendc94_in_ggga(T196, T197, T198, X295))
U61_ggga(T195, T196, T197, T198, X295, appendc94_out_ggga(T196, T197, T198, X295)) → appendc94_out_ggga(.(T195, T196), T197, T198, .(T195, X295))
U60_ga(T163, T164, X265, appendc94_out_ggga(T171, T163, T172, X265)) → qsortc79_out_ga(.(T163, T164), X265)
qsortc1_in_ga([], []) → qsortc1_out_ga([], [])
qsortc1_in_ga(.(T14, []), T9) → U46_ga(T14, T9, qsortc14_in_a(T17))
U46_ga(T14, T9, qsortc14_out_a(T17)) → U47_ga(T14, T9, T17, qsortc14_in_a(T20))
U47_ga(T14, T9, T17, qsortc14_out_a(T20)) → U48_ga(T14, T9, appendc23_in_ggga(T17, T14, T20, T9))
appendc23_in_ggga([], T33, T34, .(T33, T34)) → appendc23_out_ggga([], T33, T34, .(T33, T34))
appendc23_in_ggga(.(T45, T46), T47, T48, .(T45, T50)) → U39_ggga(T45, T46, T47, T48, T50, appendc23_in_ggga(T46, T47, T48, T50))
U39_ggga(T45, T46, T47, T48, T50, appendc23_out_ggga(T46, T47, T48, T50)) → appendc23_out_ggga(.(T45, T46), T47, T48, .(T45, T50))
U48_ga(T14, T9, appendc23_out_ggga(T17, T14, T20, T9)) → qsortc1_out_ga(.(T14, []), T9)
qsortc1_in_ga(.(T69, .(T67, T68)), T9) → U49_ga(T69, T67, T68, T9, lec36_in_gg(T67, T69))
U49_ga(T69, T67, T68, T9, lec36_out_gg(T67, T69)) → U50_ga(T69, T67, T68, T9, splitc51_in_ggaa(T68, T69, T93, T94))
U50_ga(T69, T67, T68, T9, splitc51_out_ggaa(T68, T69, T93, T94)) → U51_ga(T69, T67, T68, T9, T94, qsortc1_in_ga(.(T67, T93), T155))
qsortc1_in_ga(.(T215, .(T213, T214)), T9) → U53_ga(T215, T213, T214, T9, gtc67_in_gg(T213, T215))
U53_ga(T215, T213, T214, T9, gtc67_out_gg(T213, T215)) → U54_ga(T215, T213, T214, T9, splitc51_in_ggaa(T214, T215, T222, T223))
U54_ga(T215, T213, T214, T9, splitc51_out_ggaa(T214, T215, T222, T223)) → U55_ga(T215, T213, T214, T9, T223, qsortc79_in_ga(T222, T226))
U55_ga(T215, T213, T214, T9, T223, qsortc79_out_ga(T222, T226)) → U56_ga(T215, T213, T214, T9, qc78_in_gagga(.(T213, T223), X13, T226, T215, T9))
qc78_in_gagga(T94, T158, T155, T69, T9) → U62_gagga(T94, T158, T155, T69, T9, qsortc79_in_ga(T94, T158))
U62_gagga(T94, T158, T155, T69, T9, qsortc79_out_ga(T94, T158)) → U63_gagga(T94, T158, T155, T69, T9, appendc23_in_ggga(T155, T69, T158, T9))
U63_gagga(T94, T158, T155, T69, T9, appendc23_out_ggga(T155, T69, T158, T9)) → qc78_out_gagga(T94, T158, T155, T69, T9)
U56_ga(T215, T213, T214, T9, qc78_out_gagga(.(T213, T223), X13, T226, T215, T9)) → qsortc1_out_ga(.(T215, .(T213, T214)), T9)
U51_ga(T69, T67, T68, T9, T94, qsortc1_out_ga(.(T67, T93), T155)) → U52_ga(T69, T67, T68, T9, qc78_in_gagga(T94, X13, T155, T69, T9))
U52_ga(T69, T67, T68, T9, qc78_out_gagga(T94, X13, T155, T69, T9)) → qsortc1_out_ga(.(T69, .(T67, T68)), T9)

The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
[]  =  []
qsortc14_in_a(x1)  =  qsortc14_in_a
qsortc14_out_a(x1)  =  qsortc14_out_a(x1)
s(x1)  =  s(x1)
lec36_in_gg(x1, x2)  =  lec36_in_gg(x1, x2)
U40_gg(x1, x2, x3)  =  U40_gg(x1, x2, x3)
0  =  0
lec36_out_gg(x1, x2)  =  lec36_out_gg(x1, x2)
gtc67_in_gg(x1, x2)  =  gtc67_in_gg(x1, x2)
U45_gg(x1, x2, x3)  =  U45_gg(x1, x2, x3)
gtc67_out_gg(x1, x2)  =  gtc67_out_gg(x1, x2)
splitc51_in_ggaa(x1, x2, x3, x4)  =  splitc51_in_ggaa(x1, x2)
splitc51_out_ggaa(x1, x2, x3, x4)  =  splitc51_out_ggaa(x1, x2, x3, x4)
U41_ggaa(x1, x2, x3, x4, x5, x6)  =  U41_ggaa(x1, x2, x3, x6)
U42_ggaa(x1, x2, x3, x4, x5, x6)  =  U42_ggaa(x1, x2, x3, x6)
U43_ggaa(x1, x2, x3, x4, x5, x6)  =  U43_ggaa(x1, x2, x3, x6)
U44_ggaa(x1, x2, x3, x4, x5, x6)  =  U44_ggaa(x1, x2, x3, x6)
qsortc79_in_ga(x1, x2)  =  qsortc79_in_ga(x1)
qsortc79_out_ga(x1, x2)  =  qsortc79_out_ga(x1, x2)
U57_ga(x1, x2, x3, x4)  =  U57_ga(x1, x2, x4)
U58_ga(x1, x2, x3, x4, x5)  =  U58_ga(x1, x2, x4, x5)
U59_ga(x1, x2, x3, x4, x5)  =  U59_ga(x1, x2, x4, x5)
U60_ga(x1, x2, x3, x4)  =  U60_ga(x1, x2, x4)
appendc94_in_ggga(x1, x2, x3, x4)  =  appendc94_in_ggga(x1, x2, x3)
appendc94_out_ggga(x1, x2, x3, x4)  =  appendc94_out_ggga(x1, x2, x3, x4)
U61_ggga(x1, x2, x3, x4, x5, x6)  =  U61_ggga(x1, x2, x3, x4, x6)
qsortc1_in_ga(x1, x2)  =  qsortc1_in_ga(x1)
qsortc1_out_ga(x1, x2)  =  qsortc1_out_ga(x1, x2)
U46_ga(x1, x2, x3)  =  U46_ga(x1, x3)
U47_ga(x1, x2, x3, x4)  =  U47_ga(x1, x3, x4)
U48_ga(x1, x2, x3)  =  U48_ga(x1, x3)
appendc23_in_ggga(x1, x2, x3, x4)  =  appendc23_in_ggga(x1, x2, x3)
appendc23_out_ggga(x1, x2, x3, x4)  =  appendc23_out_ggga(x1, x2, x3, x4)
U39_ggga(x1, x2, x3, x4, x5, x6)  =  U39_ggga(x1, x2, x3, x4, x6)
U49_ga(x1, x2, x3, x4, x5)  =  U49_ga(x1, x2, x3, x5)
U50_ga(x1, x2, x3, x4, x5)  =  U50_ga(x1, x2, x3, x5)
U51_ga(x1, x2, x3, x4, x5, x6)  =  U51_ga(x1, x2, x3, x5, x6)
U53_ga(x1, x2, x3, x4, x5)  =  U53_ga(x1, x2, x3, x5)
U54_ga(x1, x2, x3, x4, x5)  =  U54_ga(x1, x2, x3, x5)
U55_ga(x1, x2, x3, x4, x5, x6)  =  U55_ga(x1, x2, x3, x5, x6)
U56_ga(x1, x2, x3, x4, x5)  =  U56_ga(x1, x2, x3, x5)
qc78_in_gagga(x1, x2, x3, x4, x5)  =  qc78_in_gagga(x1, x3, x4)
U62_gagga(x1, x2, x3, x4, x5, x6)  =  U62_gagga(x1, x3, x4, x6)
U63_gagga(x1, x2, x3, x4, x5, x6)  =  U63_gagga(x1, x2, x3, x4, x6)
qc78_out_gagga(x1, x2, x3, x4, x5)  =  qc78_out_gagga(x1, x2, x3, x4, x5)
U52_ga(x1, x2, x3, x4, x5)  =  U52_ga(x1, x2, x3, x5)
APPEND23_IN_GGGA(x1, x2, x3, x4)  =  APPEND23_IN_GGGA(x1, x2, x3)

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

(47) UsableRulesProof (EQUIVALENT transformation)

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

(48) Obligation:

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

APPEND23_IN_GGGA(.(T45, T46), T47, T48, .(T45, T50)) → APPEND23_IN_GGGA(T46, T47, T48, T50)

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

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

(49) PiDPToQDPProof (SOUND transformation)

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

(50) Obligation:

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

APPEND23_IN_GGGA(.(T45, T46), T47, T48) → APPEND23_IN_GGGA(T46, T47, T48)

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

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

  • APPEND23_IN_GGGA(.(T45, T46), T47, T48) → APPEND23_IN_GGGA(T46, T47, T48)
    The graph contains the following edges 1 > 1, 2 >= 2, 3 >= 3

(52) YES

(53) Obligation:

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

QSORT1_IN_GA(.(T69, .(T67, T68)), T9) → U25_GA(T69, T67, T68, T9, lec36_in_gg(T67, T69))
U25_GA(T69, T67, T68, T9, lec36_out_gg(T67, T69)) → U27_GA(T69, T67, T68, T9, splitc51_in_ggaa(T68, T69, T93, T94))
U27_GA(T69, T67, T68, T9, splitc51_out_ggaa(T68, T69, T93, T94)) → QSORT1_IN_GA(.(T67, T93), X12)

The TRS R consists of the following rules:

qsortc14_in_a([]) → qsortc14_out_a([])
lec36_in_gg(s(T82), s(T83)) → U40_gg(T82, T83, lec36_in_gg(T82, T83))
lec36_in_gg(0, s(T90)) → lec36_out_gg(0, s(T90))
lec36_in_gg(0, 0) → lec36_out_gg(0, 0)
U40_gg(T82, T83, lec36_out_gg(T82, T83)) → lec36_out_gg(s(T82), s(T83))
gtc67_in_gg(s(T144), s(T145)) → U45_gg(T144, T145, gtc67_in_gg(T144, T145))
gtc67_in_gg(s(T150), 0) → gtc67_out_gg(s(T150), 0)
U45_gg(T144, T145, gtc67_out_gg(T144, T145)) → gtc67_out_gg(s(T144), s(T145))
splitc51_in_ggaa([], T101, [], []) → splitc51_out_ggaa([], T101, [], [])
splitc51_in_ggaa(.(T114, T115), T116, .(T114, X167), X168) → U41_ggaa(T114, T115, T116, X167, X168, lec36_in_gg(T114, T116))
U41_ggaa(T114, T115, T116, X167, X168, lec36_out_gg(T114, T116)) → U42_ggaa(T114, T115, T116, X167, X168, splitc51_in_ggaa(T115, T116, X167, X168))
splitc51_in_ggaa(.(T129, T130), T131, X199, .(T129, X200)) → U43_ggaa(T129, T130, T131, X199, X200, gtc67_in_gg(T129, T131))
U43_ggaa(T129, T130, T131, X199, X200, gtc67_out_gg(T129, T131)) → U44_ggaa(T129, T130, T131, X199, X200, splitc51_in_ggaa(T130, T131, X199, X200))
U44_ggaa(T129, T130, T131, X199, X200, splitc51_out_ggaa(T130, T131, X199, X200)) → splitc51_out_ggaa(.(T129, T130), T131, X199, .(T129, X200))
U42_ggaa(T114, T115, T116, X167, X168, splitc51_out_ggaa(T115, T116, X167, X168)) → splitc51_out_ggaa(.(T114, T115), T116, .(T114, X167), X168)
qsortc79_in_ga([], []) → qsortc79_out_ga([], [])
qsortc79_in_ga(.(T163, T164), X265) → U57_ga(T163, T164, X265, splitc51_in_ggaa(T164, T163, T167, T168))
U57_ga(T163, T164, X265, splitc51_out_ggaa(T164, T163, T167, T168)) → U58_ga(T163, T164, X265, T168, qsortc79_in_ga(T167, T171))
U58_ga(T163, T164, X265, T168, qsortc79_out_ga(T167, T171)) → U59_ga(T163, T164, X265, T171, qsortc79_in_ga(T168, T172))
U59_ga(T163, T164, X265, T171, qsortc79_out_ga(T168, T172)) → U60_ga(T163, T164, X265, appendc94_in_ggga(T171, T163, T172, X265))
appendc94_in_ggga([], T185, T186, .(T185, T186)) → appendc94_out_ggga([], T185, T186, .(T185, T186))
appendc94_in_ggga(.(T195, T196), T197, T198, .(T195, X295)) → U61_ggga(T195, T196, T197, T198, X295, appendc94_in_ggga(T196, T197, T198, X295))
U61_ggga(T195, T196, T197, T198, X295, appendc94_out_ggga(T196, T197, T198, X295)) → appendc94_out_ggga(.(T195, T196), T197, T198, .(T195, X295))
U60_ga(T163, T164, X265, appendc94_out_ggga(T171, T163, T172, X265)) → qsortc79_out_ga(.(T163, T164), X265)
qsortc1_in_ga([], []) → qsortc1_out_ga([], [])
qsortc1_in_ga(.(T14, []), T9) → U46_ga(T14, T9, qsortc14_in_a(T17))
U46_ga(T14, T9, qsortc14_out_a(T17)) → U47_ga(T14, T9, T17, qsortc14_in_a(T20))
U47_ga(T14, T9, T17, qsortc14_out_a(T20)) → U48_ga(T14, T9, appendc23_in_ggga(T17, T14, T20, T9))
appendc23_in_ggga([], T33, T34, .(T33, T34)) → appendc23_out_ggga([], T33, T34, .(T33, T34))
appendc23_in_ggga(.(T45, T46), T47, T48, .(T45, T50)) → U39_ggga(T45, T46, T47, T48, T50, appendc23_in_ggga(T46, T47, T48, T50))
U39_ggga(T45, T46, T47, T48, T50, appendc23_out_ggga(T46, T47, T48, T50)) → appendc23_out_ggga(.(T45, T46), T47, T48, .(T45, T50))
U48_ga(T14, T9, appendc23_out_ggga(T17, T14, T20, T9)) → qsortc1_out_ga(.(T14, []), T9)
qsortc1_in_ga(.(T69, .(T67, T68)), T9) → U49_ga(T69, T67, T68, T9, lec36_in_gg(T67, T69))
U49_ga(T69, T67, T68, T9, lec36_out_gg(T67, T69)) → U50_ga(T69, T67, T68, T9, splitc51_in_ggaa(T68, T69, T93, T94))
U50_ga(T69, T67, T68, T9, splitc51_out_ggaa(T68, T69, T93, T94)) → U51_ga(T69, T67, T68, T9, T94, qsortc1_in_ga(.(T67, T93), T155))
qsortc1_in_ga(.(T215, .(T213, T214)), T9) → U53_ga(T215, T213, T214, T9, gtc67_in_gg(T213, T215))
U53_ga(T215, T213, T214, T9, gtc67_out_gg(T213, T215)) → U54_ga(T215, T213, T214, T9, splitc51_in_ggaa(T214, T215, T222, T223))
U54_ga(T215, T213, T214, T9, splitc51_out_ggaa(T214, T215, T222, T223)) → U55_ga(T215, T213, T214, T9, T223, qsortc79_in_ga(T222, T226))
U55_ga(T215, T213, T214, T9, T223, qsortc79_out_ga(T222, T226)) → U56_ga(T215, T213, T214, T9, qc78_in_gagga(.(T213, T223), X13, T226, T215, T9))
qc78_in_gagga(T94, T158, T155, T69, T9) → U62_gagga(T94, T158, T155, T69, T9, qsortc79_in_ga(T94, T158))
U62_gagga(T94, T158, T155, T69, T9, qsortc79_out_ga(T94, T158)) → U63_gagga(T94, T158, T155, T69, T9, appendc23_in_ggga(T155, T69, T158, T9))
U63_gagga(T94, T158, T155, T69, T9, appendc23_out_ggga(T155, T69, T158, T9)) → qc78_out_gagga(T94, T158, T155, T69, T9)
U56_ga(T215, T213, T214, T9, qc78_out_gagga(.(T213, T223), X13, T226, T215, T9)) → qsortc1_out_ga(.(T215, .(T213, T214)), T9)
U51_ga(T69, T67, T68, T9, T94, qsortc1_out_ga(.(T67, T93), T155)) → U52_ga(T69, T67, T68, T9, qc78_in_gagga(T94, X13, T155, T69, T9))
U52_ga(T69, T67, T68, T9, qc78_out_gagga(T94, X13, T155, T69, T9)) → qsortc1_out_ga(.(T69, .(T67, T68)), T9)

The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
[]  =  []
qsortc14_in_a(x1)  =  qsortc14_in_a
qsortc14_out_a(x1)  =  qsortc14_out_a(x1)
s(x1)  =  s(x1)
lec36_in_gg(x1, x2)  =  lec36_in_gg(x1, x2)
U40_gg(x1, x2, x3)  =  U40_gg(x1, x2, x3)
0  =  0
lec36_out_gg(x1, x2)  =  lec36_out_gg(x1, x2)
gtc67_in_gg(x1, x2)  =  gtc67_in_gg(x1, x2)
U45_gg(x1, x2, x3)  =  U45_gg(x1, x2, x3)
gtc67_out_gg(x1, x2)  =  gtc67_out_gg(x1, x2)
splitc51_in_ggaa(x1, x2, x3, x4)  =  splitc51_in_ggaa(x1, x2)
splitc51_out_ggaa(x1, x2, x3, x4)  =  splitc51_out_ggaa(x1, x2, x3, x4)
U41_ggaa(x1, x2, x3, x4, x5, x6)  =  U41_ggaa(x1, x2, x3, x6)
U42_ggaa(x1, x2, x3, x4, x5, x6)  =  U42_ggaa(x1, x2, x3, x6)
U43_ggaa(x1, x2, x3, x4, x5, x6)  =  U43_ggaa(x1, x2, x3, x6)
U44_ggaa(x1, x2, x3, x4, x5, x6)  =  U44_ggaa(x1, x2, x3, x6)
qsortc79_in_ga(x1, x2)  =  qsortc79_in_ga(x1)
qsortc79_out_ga(x1, x2)  =  qsortc79_out_ga(x1, x2)
U57_ga(x1, x2, x3, x4)  =  U57_ga(x1, x2, x4)
U58_ga(x1, x2, x3, x4, x5)  =  U58_ga(x1, x2, x4, x5)
U59_ga(x1, x2, x3, x4, x5)  =  U59_ga(x1, x2, x4, x5)
U60_ga(x1, x2, x3, x4)  =  U60_ga(x1, x2, x4)
appendc94_in_ggga(x1, x2, x3, x4)  =  appendc94_in_ggga(x1, x2, x3)
appendc94_out_ggga(x1, x2, x3, x4)  =  appendc94_out_ggga(x1, x2, x3, x4)
U61_ggga(x1, x2, x3, x4, x5, x6)  =  U61_ggga(x1, x2, x3, x4, x6)
qsortc1_in_ga(x1, x2)  =  qsortc1_in_ga(x1)
qsortc1_out_ga(x1, x2)  =  qsortc1_out_ga(x1, x2)
U46_ga(x1, x2, x3)  =  U46_ga(x1, x3)
U47_ga(x1, x2, x3, x4)  =  U47_ga(x1, x3, x4)
U48_ga(x1, x2, x3)  =  U48_ga(x1, x3)
appendc23_in_ggga(x1, x2, x3, x4)  =  appendc23_in_ggga(x1, x2, x3)
appendc23_out_ggga(x1, x2, x3, x4)  =  appendc23_out_ggga(x1, x2, x3, x4)
U39_ggga(x1, x2, x3, x4, x5, x6)  =  U39_ggga(x1, x2, x3, x4, x6)
U49_ga(x1, x2, x3, x4, x5)  =  U49_ga(x1, x2, x3, x5)
U50_ga(x1, x2, x3, x4, x5)  =  U50_ga(x1, x2, x3, x5)
U51_ga(x1, x2, x3, x4, x5, x6)  =  U51_ga(x1, x2, x3, x5, x6)
U53_ga(x1, x2, x3, x4, x5)  =  U53_ga(x1, x2, x3, x5)
U54_ga(x1, x2, x3, x4, x5)  =  U54_ga(x1, x2, x3, x5)
U55_ga(x1, x2, x3, x4, x5, x6)  =  U55_ga(x1, x2, x3, x5, x6)
U56_ga(x1, x2, x3, x4, x5)  =  U56_ga(x1, x2, x3, x5)
qc78_in_gagga(x1, x2, x3, x4, x5)  =  qc78_in_gagga(x1, x3, x4)
U62_gagga(x1, x2, x3, x4, x5, x6)  =  U62_gagga(x1, x3, x4, x6)
U63_gagga(x1, x2, x3, x4, x5, x6)  =  U63_gagga(x1, x2, x3, x4, x6)
qc78_out_gagga(x1, x2, x3, x4, x5)  =  qc78_out_gagga(x1, x2, x3, x4, x5)
U52_ga(x1, x2, x3, x4, x5)  =  U52_ga(x1, x2, x3, x5)
QSORT1_IN_GA(x1, x2)  =  QSORT1_IN_GA(x1)
U25_GA(x1, x2, x3, x4, x5)  =  U25_GA(x1, x2, x3, x5)
U27_GA(x1, x2, x3, x4, x5)  =  U27_GA(x1, x2, x3, x5)

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

(54) UsableRulesProof (EQUIVALENT transformation)

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

(55) Obligation:

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

QSORT1_IN_GA(.(T69, .(T67, T68)), T9) → U25_GA(T69, T67, T68, T9, lec36_in_gg(T67, T69))
U25_GA(T69, T67, T68, T9, lec36_out_gg(T67, T69)) → U27_GA(T69, T67, T68, T9, splitc51_in_ggaa(T68, T69, T93, T94))
U27_GA(T69, T67, T68, T9, splitc51_out_ggaa(T68, T69, T93, T94)) → QSORT1_IN_GA(.(T67, T93), X12)

The TRS R consists of the following rules:

lec36_in_gg(s(T82), s(T83)) → U40_gg(T82, T83, lec36_in_gg(T82, T83))
lec36_in_gg(0, s(T90)) → lec36_out_gg(0, s(T90))
lec36_in_gg(0, 0) → lec36_out_gg(0, 0)
splitc51_in_ggaa([], T101, [], []) → splitc51_out_ggaa([], T101, [], [])
splitc51_in_ggaa(.(T114, T115), T116, .(T114, X167), X168) → U41_ggaa(T114, T115, T116, X167, X168, lec36_in_gg(T114, T116))
splitc51_in_ggaa(.(T129, T130), T131, X199, .(T129, X200)) → U43_ggaa(T129, T130, T131, X199, X200, gtc67_in_gg(T129, T131))
U40_gg(T82, T83, lec36_out_gg(T82, T83)) → lec36_out_gg(s(T82), s(T83))
U41_ggaa(T114, T115, T116, X167, X168, lec36_out_gg(T114, T116)) → U42_ggaa(T114, T115, T116, X167, X168, splitc51_in_ggaa(T115, T116, X167, X168))
U43_ggaa(T129, T130, T131, X199, X200, gtc67_out_gg(T129, T131)) → U44_ggaa(T129, T130, T131, X199, X200, splitc51_in_ggaa(T130, T131, X199, X200))
U42_ggaa(T114, T115, T116, X167, X168, splitc51_out_ggaa(T115, T116, X167, X168)) → splitc51_out_ggaa(.(T114, T115), T116, .(T114, X167), X168)
gtc67_in_gg(s(T144), s(T145)) → U45_gg(T144, T145, gtc67_in_gg(T144, T145))
gtc67_in_gg(s(T150), 0) → gtc67_out_gg(s(T150), 0)
U44_ggaa(T129, T130, T131, X199, X200, splitc51_out_ggaa(T130, T131, X199, X200)) → splitc51_out_ggaa(.(T129, T130), T131, X199, .(T129, X200))
U45_gg(T144, T145, gtc67_out_gg(T144, T145)) → gtc67_out_gg(s(T144), s(T145))

The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
[]  =  []
s(x1)  =  s(x1)
lec36_in_gg(x1, x2)  =  lec36_in_gg(x1, x2)
U40_gg(x1, x2, x3)  =  U40_gg(x1, x2, x3)
0  =  0
lec36_out_gg(x1, x2)  =  lec36_out_gg(x1, x2)
gtc67_in_gg(x1, x2)  =  gtc67_in_gg(x1, x2)
U45_gg(x1, x2, x3)  =  U45_gg(x1, x2, x3)
gtc67_out_gg(x1, x2)  =  gtc67_out_gg(x1, x2)
splitc51_in_ggaa(x1, x2, x3, x4)  =  splitc51_in_ggaa(x1, x2)
splitc51_out_ggaa(x1, x2, x3, x4)  =  splitc51_out_ggaa(x1, x2, x3, x4)
U41_ggaa(x1, x2, x3, x4, x5, x6)  =  U41_ggaa(x1, x2, x3, x6)
U42_ggaa(x1, x2, x3, x4, x5, x6)  =  U42_ggaa(x1, x2, x3, x6)
U43_ggaa(x1, x2, x3, x4, x5, x6)  =  U43_ggaa(x1, x2, x3, x6)
U44_ggaa(x1, x2, x3, x4, x5, x6)  =  U44_ggaa(x1, x2, x3, x6)
QSORT1_IN_GA(x1, x2)  =  QSORT1_IN_GA(x1)
U25_GA(x1, x2, x3, x4, x5)  =  U25_GA(x1, x2, x3, x5)
U27_GA(x1, x2, x3, x4, x5)  =  U27_GA(x1, x2, x3, x5)

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

(56) PiDPToQDPProof (SOUND transformation)

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

(57) Obligation:

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

QSORT1_IN_GA(.(T69, .(T67, T68))) → U25_GA(T69, T67, T68, lec36_in_gg(T67, T69))
U25_GA(T69, T67, T68, lec36_out_gg(T67, T69)) → U27_GA(T69, T67, T68, splitc51_in_ggaa(T68, T69))
U27_GA(T69, T67, T68, splitc51_out_ggaa(T68, T69, T93, T94)) → QSORT1_IN_GA(.(T67, T93))

The TRS R consists of the following rules:

lec36_in_gg(s(T82), s(T83)) → U40_gg(T82, T83, lec36_in_gg(T82, T83))
lec36_in_gg(0, s(T90)) → lec36_out_gg(0, s(T90))
lec36_in_gg(0, 0) → lec36_out_gg(0, 0)
splitc51_in_ggaa([], T101) → splitc51_out_ggaa([], T101, [], [])
splitc51_in_ggaa(.(T114, T115), T116) → U41_ggaa(T114, T115, T116, lec36_in_gg(T114, T116))
splitc51_in_ggaa(.(T129, T130), T131) → U43_ggaa(T129, T130, T131, gtc67_in_gg(T129, T131))
U40_gg(T82, T83, lec36_out_gg(T82, T83)) → lec36_out_gg(s(T82), s(T83))
U41_ggaa(T114, T115, T116, lec36_out_gg(T114, T116)) → U42_ggaa(T114, T115, T116, splitc51_in_ggaa(T115, T116))
U43_ggaa(T129, T130, T131, gtc67_out_gg(T129, T131)) → U44_ggaa(T129, T130, T131, splitc51_in_ggaa(T130, T131))
U42_ggaa(T114, T115, T116, splitc51_out_ggaa(T115, T116, X167, X168)) → splitc51_out_ggaa(.(T114, T115), T116, .(T114, X167), X168)
gtc67_in_gg(s(T144), s(T145)) → U45_gg(T144, T145, gtc67_in_gg(T144, T145))
gtc67_in_gg(s(T150), 0) → gtc67_out_gg(s(T150), 0)
U44_ggaa(T129, T130, T131, splitc51_out_ggaa(T130, T131, X199, X200)) → splitc51_out_ggaa(.(T129, T130), T131, X199, .(T129, X200))
U45_gg(T144, T145, gtc67_out_gg(T144, T145)) → gtc67_out_gg(s(T144), s(T145))

The set Q consists of the following terms:

lec36_in_gg(x0, x1)
splitc51_in_ggaa(x0, x1)
U40_gg(x0, x1, x2)
U41_ggaa(x0, x1, x2, x3)
U43_ggaa(x0, x1, x2, x3)
U42_ggaa(x0, x1, x2, x3)
gtc67_in_gg(x0, x1)
U44_ggaa(x0, x1, x2, x3)
U45_gg(x0, x1, x2)

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

(58) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


QSORT1_IN_GA(.(T69, .(T67, T68))) → U25_GA(T69, T67, T68, lec36_in_gg(T67, T69))
The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial interpretation [POLO]:

POL(.(x1, x2)) = 1 + x2   
POL(0) = 0   
POL(QSORT1_IN_GA(x1)) = x1   
POL(U25_GA(x1, x2, x3, x4)) = 1 + x3   
POL(U27_GA(x1, x2, x3, x4)) = 1 + x4   
POL(U40_gg(x1, x2, x3)) = 0   
POL(U41_ggaa(x1, x2, x3, x4)) = 1 + x2   
POL(U42_ggaa(x1, x2, x3, x4)) = 1 + x4   
POL(U43_ggaa(x1, x2, x3, x4)) = 1 + x2   
POL(U44_ggaa(x1, x2, x3, x4)) = x4   
POL(U45_gg(x1, x2, x3)) = 0   
POL([]) = 0   
POL(gtc67_in_gg(x1, x2)) = 0   
POL(gtc67_out_gg(x1, x2)) = 0   
POL(lec36_in_gg(x1, x2)) = 0   
POL(lec36_out_gg(x1, x2)) = 0   
POL(s(x1)) = 0   
POL(splitc51_in_ggaa(x1, x2)) = x1   
POL(splitc51_out_ggaa(x1, x2, x3, x4)) = x3   

The following usable rules [FROCOS05] were oriented:

splitc51_in_ggaa([], T101) → splitc51_out_ggaa([], T101, [], [])
splitc51_in_ggaa(.(T114, T115), T116) → U41_ggaa(T114, T115, T116, lec36_in_gg(T114, T116))
splitc51_in_ggaa(.(T129, T130), T131) → U43_ggaa(T129, T130, T131, gtc67_in_gg(T129, T131))
U41_ggaa(T114, T115, T116, lec36_out_gg(T114, T116)) → U42_ggaa(T114, T115, T116, splitc51_in_ggaa(T115, T116))
U42_ggaa(T114, T115, T116, splitc51_out_ggaa(T115, T116, X167, X168)) → splitc51_out_ggaa(.(T114, T115), T116, .(T114, X167), X168)
U43_ggaa(T129, T130, T131, gtc67_out_gg(T129, T131)) → U44_ggaa(T129, T130, T131, splitc51_in_ggaa(T130, T131))
U44_ggaa(T129, T130, T131, splitc51_out_ggaa(T130, T131, X199, X200)) → splitc51_out_ggaa(.(T129, T130), T131, X199, .(T129, X200))

(59) Obligation:

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

U25_GA(T69, T67, T68, lec36_out_gg(T67, T69)) → U27_GA(T69, T67, T68, splitc51_in_ggaa(T68, T69))
U27_GA(T69, T67, T68, splitc51_out_ggaa(T68, T69, T93, T94)) → QSORT1_IN_GA(.(T67, T93))

The TRS R consists of the following rules:

lec36_in_gg(s(T82), s(T83)) → U40_gg(T82, T83, lec36_in_gg(T82, T83))
lec36_in_gg(0, s(T90)) → lec36_out_gg(0, s(T90))
lec36_in_gg(0, 0) → lec36_out_gg(0, 0)
splitc51_in_ggaa([], T101) → splitc51_out_ggaa([], T101, [], [])
splitc51_in_ggaa(.(T114, T115), T116) → U41_ggaa(T114, T115, T116, lec36_in_gg(T114, T116))
splitc51_in_ggaa(.(T129, T130), T131) → U43_ggaa(T129, T130, T131, gtc67_in_gg(T129, T131))
U40_gg(T82, T83, lec36_out_gg(T82, T83)) → lec36_out_gg(s(T82), s(T83))
U41_ggaa(T114, T115, T116, lec36_out_gg(T114, T116)) → U42_ggaa(T114, T115, T116, splitc51_in_ggaa(T115, T116))
U43_ggaa(T129, T130, T131, gtc67_out_gg(T129, T131)) → U44_ggaa(T129, T130, T131, splitc51_in_ggaa(T130, T131))
U42_ggaa(T114, T115, T116, splitc51_out_ggaa(T115, T116, X167, X168)) → splitc51_out_ggaa(.(T114, T115), T116, .(T114, X167), X168)
gtc67_in_gg(s(T144), s(T145)) → U45_gg(T144, T145, gtc67_in_gg(T144, T145))
gtc67_in_gg(s(T150), 0) → gtc67_out_gg(s(T150), 0)
U44_ggaa(T129, T130, T131, splitc51_out_ggaa(T130, T131, X199, X200)) → splitc51_out_ggaa(.(T129, T130), T131, X199, .(T129, X200))
U45_gg(T144, T145, gtc67_out_gg(T144, T145)) → gtc67_out_gg(s(T144), s(T145))

The set Q consists of the following terms:

lec36_in_gg(x0, x1)
splitc51_in_ggaa(x0, x1)
U40_gg(x0, x1, x2)
U41_ggaa(x0, x1, x2, x3)
U43_ggaa(x0, x1, x2, x3)
U42_ggaa(x0, x1, x2, x3)
gtc67_in_gg(x0, x1)
U44_ggaa(x0, x1, x2, x3)
U45_gg(x0, x1, x2)

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

(60) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 2 less nodes.

(61) TRUE