Left Termination proof of /tmp/tmph00vR

Left Termination of the query pattern
mergesort(g,a)
w.r.t. the given Prolog program could successfully be proven:

0 Prolog

↳1 PrologToPiTRSViaGraphTransformerProof (⇒, 226 ms)

↳2 PiTRS

↳3 DependencyPairsProof (⇔, 355 ms)

↳4 PiDP

↳5 DependencyGraphProof (⇔, 0 ms)

↳6 AND

    ↳7 PiDP

        ↳8 UsableRulesProof (⇔, 0 ms)

        ↳9 PiDP

        ↳10 PiDPToQDPProof (⇒, 29 ms)

        ↳11 QDP

        ↳12 QDPSizeChangeProof (⇔, 0 ms)

        ↳13 YES

    ↳14 PiDP

        ↳15 UsableRulesProof (⇔, 0 ms)

        ↳16 PiDP

        ↳17 PiDPToQDPProof (⇒, 0 ms)

        ↳18 QDP

        ↳19 QDPSizeChangeProof (⇔, 0 ms)

        ↳20 YES

    ↳21 PiDP

        ↳22 UsableRulesProof (⇔, 0 ms)

        ↳23 PiDP

        ↳24 PiDPToQDPProof (⇒, 0 ms)

        ↳25 QDP

        ↳26 Rewriting (⇔, 45 ms)

        ↳27 QDP

        ↳28 Rewriting (⇔, 0 ms)

        ↳29 QDP

        ↳30 QDPOrderProof (⇔, 1674 ms)

        ↳31 QDP

        ↳32 DependencyGraphProof (⇔, 0 ms)

        ↳33 TRUE

    ↳34 PiDP

        ↳35 UsableRulesProof (⇔, 0 ms)

        ↳36 PiDP

        ↳37 PiDPToQDPProof (⇒, 0 ms)

        ↳38 QDP

        ↳39 Rewriting (⇔, 0 ms)

        ↳40 QDP

        ↳41 UsableRulesProof (⇔, 0 ms)

        ↳42 QDP

        ↳43 QReductionProof (⇔, 0 ms)

        ↳44 QDP

        ↳45 QDPOrderProof (⇔, 53 ms)

        ↳46 QDP

        ↳47 DependencyGraphProof (⇔, 0 ms)

        ↳48 TRUE

(0) Obligation:

Clauses:

mergesort([], []).
mergesort(.(X, []), .(X, [])).
mergesort(.(X, .(Y, Xs)), Ys) :- ','(split(.(X, .(Y, Xs)), X1s, X2s), ','(mergesort(X1s, Y1s), ','(mergesort(X2s, Y2s), merge(Y1s, Y2s, Ys)))).
split([], [], []).
split(.(X, Xs), .(X, Ys), Zs) :- split(Xs, Zs, Ys).
merge([], Xs, Xs).
merge(Xs, [], Xs).
merge(.(X, Xs), .(Y, Ys), .(X, Zs)) :- ','(=(X, Y), merge(.(X, Xs), Ys, Zs)).

Query: mergesort(g,a)

(1) PrologToPiTRSViaGraphTransformerProof (SOUND transformation)

Transformed Prolog program to (Pi-)TRS.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
2 [label="A: mergesort(T1, T2)\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
4 [label="4: mergesort(T1, T2), SCOPE: 1, CLAUSE: 0 | mergesort(T1, T2), SCOPE: 1, CLAUSE: 1 | mergesort(T1, T2), SCOPE: 1, CLAUSE: 2\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
9 [label="9: true | mergesort([], T2), SCOPE: 1, CLAUSE: 1 | mergesort([], T2), SCOPE: 1, CLAUSE: 2\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
13 [label="13: mergesort(T1, T2), SCOPE: 1, CLAUSE: 1 | mergesort(T1, T2), SCOPE: 1, CLAUSE: 2\n\nT1 is ground\nmergesort(T1, T2) !=? mergesort([], [])", fontsize=16, style=filled, fillcolor=lightyellow];
16 [label="16: mergesort([], T2), SCOPE: 1, CLAUSE: 1 | mergesort([], T2), SCOPE: 1, CLAUSE: 2\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
18 [label="18: mergesort([], T2), SCOPE: 1, CLAUSE: 2\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
23 [label="23: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
28 [label="28: true | mergesort(.(T4, []), T2), SCOPE: 1, CLAUSE: 2\n\nT4 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
29 [label="29: mergesort(T1, T2), SCOPE: 1, CLAUSE: 2\n\nT1 is ground\nX7 is free\nmergesort(T1, T2) !=? mergesort([], [])\nmergesort(T1, T2) !=? mergesort(.(X7, []), .(X7, []))", fontsize=16, style=filled, fillcolor=lightyellow];
31 [label="31: mergesort(.(T4, []), T2), SCOPE: 1, CLAUSE: 2\n\nT4 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
34 [label="34: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
37 [label="37: ','(split(.(T10, .(T11, T12)), X20, X21), ','(mergesort(X20, X22), ','(mergesort(X21, X23), merge(X22, X23, T14))))\n\nT10 is ground\nT11 is ground\nT12 is ground\nX20 is free\nX21 is free\nX22 is free\nX23 is free", fontsize=16, style=filled, fillcolor=lightyellow];
38 [label="38: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
39 [label="39: ','(split(.(T10, .(T11, T12)), X20, X21), ','(mergesort(X20, X22), ','(mergesort(X21, X23), merge(X22, X23, T14)))), SCOPE: 2, CLAUSE: 3 | ','(split(.(T10, .(T11, T12)), X20, X21), ','(mergesort(X20, X22), ','(mergesort(X21, X23), merge(X22, X23, T14)))), SCOPE: 2, CLAUSE: 4\n\nT10 is ground\nT11 is ground\nT12 is ground\nX20 is free\nX21 is free\nX22 is free\nX23 is free", fontsize=16, style=filled, fillcolor=lightyellow];
40 [label="40: ','(split(.(T10, .(T11, T12)), X20, X21), ','(mergesort(X20, X22), ','(mergesort(X21, X23), merge(X22, X23, T14)))), SCOPE: 2, CLAUSE: 4\n\nT10 is ground\nT11 is ground\nT12 is ground\nX20 is free\nX21 is free\nX22 is free\nX23 is free", fontsize=16, style=filled, fillcolor=lightyellow];
47 [label="B: ','(split(.(T22, T23), X41, X40), ','(mergesort(.(T21, X40), X22), ','(mergesort(X41, X23), merge(X22, X23, T14))))\n\nT21 is ground\nT22 is ground\nT23 is ground\nX22 is free\nX23 is free\nX40 is free\nX41 is free", fontsize=16, style=filled, fillcolor=lightyellow];
48 [label="D: split(.(T22, T23), X41, X40)\n\nT22 is ground\nT23 is ground\nX40 is free\nX41 is free", fontsize=16, style=filled, fillcolor=lightyellow];
49 [label="I: ','(mergesort(.(T21, T25), X22), ','(mergesort(T24, X23), merge(X22, X23, T14)))\n\nT21 is ground\nT24 is ground\nT25 is ground\nX22 is free\nX23 is free", fontsize=16, style=filled, fillcolor=lightyellow];
51 [label="51: split(.(T22, T23), X41, X40), SCOPE: 3, CLAUSE: 3 | split(.(T22, T23), X41, X40), SCOPE: 3, CLAUSE: 4\n\nT22 is ground\nT23 is ground\nX40 is free\nX41 is free", fontsize=16, style=filled, fillcolor=lightyellow];
53 [label="53: split(.(T22, T23), X41, X40), SCOPE: 3, CLAUSE: 4\n\nT22 is ground\nT23 is ground\nX40 is free\nX41 is free", fontsize=16, style=filled, fillcolor=lightyellow];
59 [label="C: split(T31, X59, X58)\n\nT31 is ground\nX58 is free\nX59 is free", fontsize=16, style=filled, fillcolor=lightyellow];
60 [label="60: split(T31, X59, X58), SCOPE: 4, CLAUSE: 3 | split(T31, X59, X58), SCOPE: 4, CLAUSE: 4\n\nT31 is ground\nX58 is free\nX59 is free", fontsize=16, style=filled, fillcolor=lightyellow];
61 [label="61: split(T31, X59, X58), SCOPE: 4, CLAUSE: 3\n\nT31 is ground\nX58 is free\nX59 is free", fontsize=16, style=filled, fillcolor=lightyellow];
62 [label="62: split(T31, X59, X58), SCOPE: 4, CLAUSE: 4\n\nT31 is ground\nX58 is free\nX59 is free", fontsize=16, style=filled, fillcolor=lightyellow];
63 [label="63: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
64 [label="64: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
65 [label="65: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
73 [label="73: split(T37, X77, X76)\n\nT37 is ground\nX76 is free\nX77 is free", fontsize=16, style=filled, fillcolor=lightyellow];
74 [label="74: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
75 [label="75: mergesort(.(T21, T25), X22)\n\nT21 is ground\nT25 is ground\nX22 is free", fontsize=16, style=filled, fillcolor=lightyellow];
76 [label="J: ','(mergesort(T24, X23), merge(T38, X23, T14))\n\nT24 is ground\nT38 is ground\nX23 is free", fontsize=16, style=filled, fillcolor=lightyellow];
82 [label="E: mergesort(T24, X23)\n\nT24 is ground\nX23 is free", fontsize=16, style=filled, fillcolor=lightyellow];
83 [label="G: merge(T38, T39, T14)\n\nT38 is ground\nT39 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
84 [label="84: mergesort(T24, X23), SCOPE: 5, CLAUSE: 0 | mergesort(T24, X23), SCOPE: 5, CLAUSE: 1 | mergesort(T24, X23), SCOPE: 5, CLAUSE: 2\n\nT24 is ground\nX23 is free", fontsize=16, style=filled, fillcolor=lightyellow];
87 [label="87: mergesort(T24, X23), SCOPE: 5, CLAUSE: 0\n\nT24 is ground\nX23 is free", fontsize=16, style=filled, fillcolor=lightyellow];
88 [label="88: mergesort(T24, X23), SCOPE: 5, CLAUSE: 1 | mergesort(T24, X23), SCOPE: 5, CLAUSE: 2\n\nT24 is ground\nX23 is free", fontsize=16, style=filled, fillcolor=lightyellow];
89 [label="89: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
90 [label="90: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
91 [label="91: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
94 [label="94: mergesort(T24, X23), SCOPE: 5, CLAUSE: 1\n\nT24 is ground\nX23 is free", fontsize=16, style=filled, fillcolor=lightyellow];
95 [label="95: mergesort(T24, X23), SCOPE: 5, CLAUSE: 2\n\nT24 is ground\nX23 is free", fontsize=16, style=filled, fillcolor=lightyellow];
99 [label="99: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
102 [label="102: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
104 [label="104: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
110 [label="F: ','(split(.(T51, .(T52, T53)), X101, X102), ','(mergesort(X101, X103), ','(mergesort(X102, X104), merge(X103, X104, X105))))\n\nT51 is ground\nT52 is ground\nT53 is ground\nX105 is free\nX101 is free\nX102 is free\nX103 is free\nX104 is free", fontsize=16, style=filled, fillcolor=lightyellow];
111 [label="111: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
115 [label="115: split(.(T51, .(T52, T53)), X101, X102)\n\nT51 is ground\nT52 is ground\nT53 is ground\nX101 is free\nX102 is free", fontsize=16, style=filled, fillcolor=lightyellow];
117 [label="K: ','(mergesort(T54, X103), ','(mergesort(T55, X104), merge(X103, X104, X105)))\n\nT54 is ground\nT55 is ground\nX105 is free\nX103 is free\nX104 is free", fontsize=16, style=filled, fillcolor=lightyellow];
125 [label="125: mergesort(T54, X103)\n\nT54 is ground\nX103 is free", fontsize=16, style=filled, fillcolor=lightyellow];
127 [label="L: ','(mergesort(T55, X104), merge(T56, X104, X105))\n\nT55 is ground\nT56 is ground\nX105 is free\nX104 is free", fontsize=16, style=filled, fillcolor=lightyellow];
131 [label="131: mergesort(T55, X104)\n\nT55 is ground\nX104 is free", fontsize=16, style=filled, fillcolor=lightyellow];
132 [label="H: merge(T56, T57, X105)\n\nT56 is ground\nT57 is ground\nX105 is free", fontsize=16, style=filled, fillcolor=lightyellow];
141 [label="141: merge(T56, T57, X105), SCOPE: 6, CLAUSE: 5 | merge(T56, T57, X105), SCOPE: 6, CLAUSE: 6 | merge(T56, T57, X105), SCOPE: 6, CLAUSE: 7\n\nT56 is ground\nT57 is ground\nX105 is free", fontsize=16, style=filled, fillcolor=lightyellow];
145 [label="145: merge(T56, T57, X105), SCOPE: 6, CLAUSE: 5\n\nT56 is ground\nT57 is ground\nX105 is free", fontsize=16, style=filled, fillcolor=lightyellow];
146 [label="146: merge(T56, T57, X105), SCOPE: 6, CLAUSE: 6 | merge(T56, T57, X105), SCOPE: 6, CLAUSE: 7\n\nT56 is ground\nT57 is ground\nX105 is free", fontsize=16, style=filled, fillcolor=lightyellow];
147 [label="147: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
148 [label="148: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
149 [label="149: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
150 [label="150: merge(T56, T57, X105), SCOPE: 6, CLAUSE: 6\n\nT56 is ground\nT57 is ground\nX105 is free", fontsize=16, style=filled, fillcolor=lightyellow];
151 [label="151: merge(T56, T57, X105), SCOPE: 6, CLAUSE: 7\n\nT56 is ground\nT57 is ground\nX105 is free", fontsize=16, style=filled, fillcolor=lightyellow];
153 [label="153: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
155 [label="155: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
156 [label="156: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
161 [label="161: ','(=(T78, T80), merge(.(T78, T79), T81, X135))\n\nT78 is ground\nT79 is ground\nT80 is ground\nT81 is ground\nX135 is free", fontsize=16, style=filled, fillcolor=lightyellow];
162 [label="162: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
163 [label="163: merge(.(T83, T79), T81, X135)\n\nT79 is ground\nT81 is ground\nT83 is ground\nX135 is free", fontsize=16, style=filled, fillcolor=lightyellow];
164 [label="164: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
169 [label="169: merge(T38, T39, T14), SCOPE: 7, CLAUSE: 5 | merge(T38, T39, T14), SCOPE: 7, CLAUSE: 6 | merge(T38, T39, T14), SCOPE: 7, CLAUSE: 7\n\nT38 is ground\nT39 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
194 [label="194: merge(T38, T39, T14), SCOPE: 7, CLAUSE: 5\n\nT38 is ground\nT39 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
195 [label="195: merge(T38, T39, T14), SCOPE: 7, CLAUSE: 6 | merge(T38, T39, T14), SCOPE: 7, CLAUSE: 7\n\nT38 is ground\nT39 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
200 [label="200: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
201 [label="201: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
202 [label="202: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
204 [label="204: merge(T38, T39, T14), SCOPE: 7, CLAUSE: 6\n\nT38 is ground\nT39 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
206 [label="206: merge(T38, T39, T14), SCOPE: 7, CLAUSE: 7\n\nT38 is ground\nT39 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
209 [label="209: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
210 [label="210: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
211 [label="211: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
225 [label="225: ','(=(T106, T108), merge(.(T106, T107), T109, T111))\n\nT106 is ground\nT107 is ground\nT108 is ground\nT109 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
226 [label="226: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
227 [label="227: merge(.(T113, T107), T109, T111)\n\nT107 is ground\nT109 is ground\nT113 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
228 [label="228: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
229 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
2 -> 229 [arrowhead = none ];
229 -> 4;

230 [label="EVAL with clause\nmergesort([], []).\nand substitutionT1 -> [],\nT2 -> []", fontsize=14, style = filled, fillcolor = lightblue];
4 -> 230 [arrowhead = none ];
230 -> 9;

231 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
4 -> 231 [arrowhead = none ];
231 -> 13;

232 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
9 -> 232 [arrowhead = none ];
232 -> 16;

233 [label="EVAL with clause\nmergesort(.(X7, []), .(X7, [])).\nand substitutionX7 -> T4,\nT1 -> .(T4, []),\nT2 -> .(T4, [])", fontsize=14, style = filled, fillcolor = lightblue];
13 -> 233 [arrowhead = none ];
233 -> 28;

234 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
13 -> 234 [arrowhead = none ];
234 -> 29;

235 [label="BACKTRACK\nfor clause: mergesort(.(X, []), .(X, []))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
16 -> 235 [arrowhead = none ];
235 -> 18;

236 [label="BACKTRACK\nfor clause: mergesort(.(X, .(Y, Xs)), Ys) :- ','(split(.(X, .(Y, Xs)), X1s, X2s), ','(mergesort(X1s, Y1s), ','(mergesort(X2s, Y2s), merge(Y1s, Y2s, Ys))))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
18 -> 236 [arrowhead = none ];
236 -> 23;

237 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
28 -> 237 [arrowhead = none ];
237 -> 31;

238 [label="EVAL with clause\nmergesort(.(X16, .(X17, X18)), X19) :- ','(split(.(X16, .(X17, X18)), X20, X21), ','(mergesort(X20, X22), ','(mergesort(X21, X23), merge(X22, X23, X19)))).\nand substitutionX16 -> T10,\nX17 -> T11,\nX18 -> T12,\nT1 -> .(T10, .(T11, T12)),\nT2 -> T14,\nX19 -> T14,\nT13 -> T14", fontsize=14, style = filled, fillcolor = lightblue];
29 -> 238 [arrowhead = none ];
238 -> 37;

239 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
29 -> 239 [arrowhead = none ];
239 -> 38;

240 [label="BACKTRACK\nfor clause: mergesort(.(X, .(Y, Xs)), Ys) :- ','(split(.(X, .(Y, Xs)), X1s, X2s), ','(mergesort(X1s, Y1s), ','(mergesort(X2s, Y2s), merge(Y1s, Y2s, Ys))))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
31 -> 240 [arrowhead = none ];
240 -> 34;

241 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
37 -> 241 [arrowhead = none ];
241 -> 39;

242 [label="BACKTRACK\nfor clause: split([], [], [])because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
39 -> 242 [arrowhead = none ];
242 -> 40;

243 [label="ONLY EVAL with clause\nsplit(.(X36, X37), .(X36, X38), X39) :- split(X37, X39, X38).\nand substitutionT10 -> T21,\nX36 -> T21,\nT11 -> T22,\nT12 -> T23,\nX37 -> .(T22, T23),\nX38 -> X40,\nX20 -> .(T21, X40),\nX21 -> X41,\nX39 -> X41", fontsize=14, style = filled, fillcolor = lightblue];
40 -> 243 [arrowhead = none ];
243 -> 47;

244 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
47 -> 244 [arrowhead = none ];
244 -> 48;

245 [label="SPLIT 2\nnew knowledge:\nT22 is ground\nT23 is ground\nT24 is ground\nT25 is ground\nreplacements:X41 -> T24,\nX40 -> T25", fontsize=14, style = filled, fillcolor = violet];
47 -> 245 [arrowhead = none ];
245 -> 49;

246 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
48 -> 246 [arrowhead = none ];
246 -> 51;

247 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
49 -> 247 [arrowhead = none ];
247 -> 75;

248 [label="SPLIT 2\nnew knowledge:\nT21 is ground\nT25 is ground\nT38 is ground\nreplacements:X22 -> T38", fontsize=14, style = filled, fillcolor = violet];
49 -> 248 [arrowhead = none ];
248 -> 76;

249 [label="BACKTRACK\nfor clause: split([], [], [])because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
51 -> 249 [arrowhead = none ];
249 -> 53;

250 [label="ONLY EVAL with clause\nsplit(.(X54, X55), .(X54, X56), X57) :- split(X55, X57, X56).\nand substitutionT22 -> T30,\nX54 -> T30,\nT23 -> T31,\nX55 -> T31,\nX56 -> X58,\nX41 -> .(T30, X58),\nX40 -> X59,\nX57 -> X59", fontsize=14, style = filled, fillcolor = lightblue];
53 -> 250 [arrowhead = none ];
250 -> 59;

251 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
59 -> 251 [arrowhead = none ];
251 -> 60;

252 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
60 -> 252 [arrowhead = none ];
252 -> 61;

253 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
60 -> 253 [arrowhead = none ];
253 -> 62;

254 [label="EVAL with clause\nsplit([], [], []).\nand substitutionT31 -> [],\nX59 -> [],\nX58 -> []", fontsize=14, style = filled, fillcolor = lightblue];
61 -> 254 [arrowhead = none ];
254 -> 63;

255 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
61 -> 255 [arrowhead = none ];
255 -> 64;

256 [label="EVAL with clause\nsplit(.(X72, X73), .(X72, X74), X75) :- split(X73, X75, X74).\nand substitutionX72 -> T36,\nX73 -> T37,\nT31 -> .(T36, T37),\nX74 -> X76,\nX59 -> .(T36, X76),\nX58 -> X77,\nX75 -> X77", fontsize=14, style = filled, fillcolor = lightblue];
62 -> 256 [arrowhead = none ];
256 -> 73;

257 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
62 -> 257 [arrowhead = none ];
257 -> 74;

258 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
63 -> 258 [arrowhead = none ];
258 -> 65;

259 [label="INSTANCE with matching:\nT31 -> T37\nX59 -> X77\nX58 -> X76", fontsize=14, style = filled, fillcolor = lightgrey];
73 -> 259 [arrowhead = none , style=dashed];
259 -> 59[style=dashed];

260 [label="INSTANCE with matching:\nT1 -> .(T21, T25)\nT2 -> X22", fontsize=14, style = filled, fillcolor = lightgrey];
75 -> 260 [arrowhead = none , style=dashed];
260 -> 2[style=dashed];

261 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
76 -> 261 [arrowhead = none ];
261 -> 82;

262 [label="SPLIT 2\nnew knowledge:\nT24 is ground\nT39 is ground\nreplacements:X23 -> T39", fontsize=14, style = filled, fillcolor = violet];
76 -> 262 [arrowhead = none ];
262 -> 83;

263 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
82 -> 263 [arrowhead = none ];
263 -> 84;

264 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
83 -> 264 [arrowhead = none ];
264 -> 169;

265 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
84 -> 265 [arrowhead = none ];
265 -> 87;

266 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
84 -> 266 [arrowhead = none ];
266 -> 88;

267 [label="EVAL with clause\nmergesort([], []).\nand substitutionT24 -> [],\nX23 -> []", fontsize=14, style = filled, fillcolor = lightblue];
87 -> 267 [arrowhead = none ];
267 -> 89;

268 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
87 -> 268 [arrowhead = none ];
268 -> 90;

269 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
88 -> 269 [arrowhead = none ];
269 -> 94;

270 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
88 -> 270 [arrowhead = none ];
270 -> 95;

271 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
89 -> 271 [arrowhead = none ];
271 -> 91;

272 [label="EVAL with clause\nmergesort(.(X82, []), .(X82, [])).\nand substitutionX82 -> T44,\nT24 -> .(T44, []),\nX23 -> .(T44, [])", fontsize=14, style = filled, fillcolor = lightblue];
94 -> 272 [arrowhead = none ];
272 -> 99;

273 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
94 -> 273 [arrowhead = none ];
273 -> 102;

274 [label="EVAL with clause\nmergesort(.(X97, .(X98, X99)), X100) :- ','(split(.(X97, .(X98, X99)), X101, X102), ','(mergesort(X101, X103), ','(mergesort(X102, X104), merge(X103, X104, X100)))).\nand substitutionX97 -> T51,\nX98 -> T52,\nX99 -> T53,\nT24 -> .(T51, .(T52, T53)),\nX23 -> X105,\nX100 -> X105", fontsize=14, style = filled, fillcolor = lightblue];
95 -> 274 [arrowhead = none ];
274 -> 110;

275 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
95 -> 275 [arrowhead = none ];
275 -> 111;

276 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
99 -> 276 [arrowhead = none ];
276 -> 104;

277 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
110 -> 277 [arrowhead = none ];
277 -> 115;

278 [label="SPLIT 2\nnew knowledge:\nT51 is ground\nT52 is ground\nT53 is ground\nT54 is ground\nT55 is ground\nreplacements:X101 -> T54,\nX102 -> T55", fontsize=14, style = filled, fillcolor = violet];
110 -> 278 [arrowhead = none ];
278 -> 117;

279 [label="INSTANCE with matching:\nT22 -> T51\nT23 -> .(T52, T53)\nX41 -> X101\nX40 -> X102", fontsize=14, style = filled, fillcolor = lightgrey];
115 -> 279 [arrowhead = none , style=dashed];
279 -> 48[style=dashed];

280 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
117 -> 280 [arrowhead = none ];
280 -> 125;

281 [label="SPLIT 2\nnew knowledge:\nT54 is ground\nT56 is ground\nreplacements:X103 -> T56", fontsize=14, style = filled, fillcolor = violet];
117 -> 281 [arrowhead = none ];
281 -> 127;

282 [label="INSTANCE with matching:\nT24 -> T54\nX23 -> X103", fontsize=14, style = filled, fillcolor = lightgrey];
125 -> 282 [arrowhead = none , style=dashed];
282 -> 82[style=dashed];

283 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
127 -> 283 [arrowhead = none ];
283 -> 131;

284 [label="SPLIT 2\nnew knowledge:\nT55 is ground\nT57 is ground\nreplacements:X104 -> T57", fontsize=14, style = filled, fillcolor = violet];
127 -> 284 [arrowhead = none ];
284 -> 132;

285 [label="INSTANCE with matching:\nT24 -> T55\nX23 -> X104", fontsize=14, style = filled, fillcolor = lightgrey];
131 -> 285 [arrowhead = none , style=dashed];
285 -> 82[style=dashed];

286 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
132 -> 286 [arrowhead = none ];
286 -> 141;

287 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
141 -> 287 [arrowhead = none ];
287 -> 145;

288 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
141 -> 288 [arrowhead = none ];
288 -> 146;

289 [label="EVAL with clause\nmerge([], X112, X112).\nand substitutionT56 -> [],\nT57 -> T64,\nX112 -> T64,\nX105 -> T64", fontsize=14, style = filled, fillcolor = lightblue];
145 -> 289 [arrowhead = none ];
289 -> 147;

290 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
145 -> 290 [arrowhead = none ];
290 -> 148;

291 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
146 -> 291 [arrowhead = none ];
291 -> 150;

292 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
146 -> 292 [arrowhead = none ];
292 -> 151;

293 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
147 -> 293 [arrowhead = none ];
293 -> 149;

294 [label="EVAL with clause\nmerge(X117, [], X117).\nand substitutionT56 -> T69,\nX117 -> T69,\nT57 -> [],\nX105 -> T69", fontsize=14, style = filled, fillcolor = lightblue];
150 -> 294 [arrowhead = none ];
294 -> 153;

295 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
150 -> 295 [arrowhead = none ];
295 -> 155;

296 [label="EVAL with clause\nmerge(.(X130, X131), .(X132, X133), .(X130, X134)) :- ','(=(X130, X132), merge(.(X130, X131), X133, X134)).\nand substitutionX130 -> T78,\nX131 -> T79,\nT56 -> .(T78, T79),\nX132 -> T80,\nX133 -> T81,\nT57 -> .(T80, T81),\nX134 -> X135,\nX105 -> .(T78, X135)", fontsize=14, style = filled, fillcolor = lightblue];
151 -> 296 [arrowhead = none ];
296 -> 161;

297 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
151 -> 297 [arrowhead = none ];
297 -> 162;

298 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
153 -> 298 [arrowhead = none ];
298 -> 156;

299 [label="UNIFY CASE with substitutionT78 -> T83,\nT80 -> T83", fontsize=14, style = filled, fillcolor = lightblue];
161 -> 299 [arrowhead = none ];
299 -> 163;

300 [label="UNIFY-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
161 -> 300 [arrowhead = none ];
300 -> 164;

301 [label="INSTANCE with matching:\nT38 -> .(T83, T79)\nT39 -> T81\nT14 -> X135", fontsize=14, style = filled, fillcolor = lightgrey];
163 -> 301 [arrowhead = none , style=dashed];
301 -> 83[style=dashed];

302 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
169 -> 302 [arrowhead = none ];
302 -> 194;

303 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
169 -> 303 [arrowhead = none ];
303 -> 195;

304 [label="EVAL with clause\nmerge([], X144, X144).\nand substitutionT38 -> [],\nT39 -> T90,\nX144 -> T90,\nT14 -> T90", fontsize=14, style = filled, fillcolor = lightblue];
194 -> 304 [arrowhead = none ];
304 -> 200;

305 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
194 -> 305 [arrowhead = none ];
305 -> 201;

306 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
195 -> 306 [arrowhead = none ];
306 -> 204;

307 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
195 -> 307 [arrowhead = none ];
307 -> 206;

308 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
200 -> 308 [arrowhead = none ];
308 -> 202;

309 [label="EVAL with clause\nmerge(X149, [], X149).\nand substitutionT38 -> T95,\nX149 -> T95,\nT39 -> [],\nT14 -> T95", fontsize=14, style = filled, fillcolor = lightblue];
204 -> 309 [arrowhead = none ];
309 -> 209;

310 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
204 -> 310 [arrowhead = none ];
310 -> 210;

311 [label="EVAL with clause\nmerge(.(X160, X161), .(X162, X163), .(X160, X164)) :- ','(=(X160, X162), merge(.(X160, X161), X163, X164)).\nand substitutionX160 -> T106,\nX161 -> T107,\nT38 -> .(T106, T107),\nX162 -> T108,\nX163 -> T109,\nT39 -> .(T108, T109),\nX164 -> T111,\nT14 -> .(T106, T111),\nT110 -> T111", fontsize=14, style = filled, fillcolor = lightblue];
206 -> 311 [arrowhead = none ];
311 -> 225;

312 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
206 -> 312 [arrowhead = none ];
312 -> 226;

313 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
209 -> 313 [arrowhead = none ];
313 -> 211;

314 [label="UNIFY CASE with substitutionT106 -> T113,\nT108 -> T113", fontsize=14, style = filled, fillcolor = lightblue];
225 -> 314 [arrowhead = none ];
314 -> 227;

315 [label="UNIFY-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
225 -> 315 [arrowhead = none ];
315 -> 228;

316 [label="INSTANCE with matching:\nT38 -> .(T113, T107)\nT39 -> T109\nT14 -> T111", fontsize=14, style = filled, fillcolor = lightgrey];
227 -> 316 [arrowhead = none , style=dashed];
316 -> 83[style=dashed];

}

(2) Obligation:

Pi-finite rewrite system:
The TRS R consists of the following rules:

mergesortA_in_ga([], []) → mergesortA_out_ga([], [])
mergesortA_in_ga(.(T4, []), .(T4, [])) → mergesortA_out_ga(.(T4, []), .(T4, []))
mergesortA_in_ga(.(T21, .(T22, T23)), T14) → U1_ga(T21, T22, T23, T14, pB_in_ggaagaaa(T22, T23, X41, X40, T21, X22, X23, T14))
pB_in_ggaagaaa(T22, T23, T24, T25, T21, X22, X23, T14) → U7_ggaagaaa(T22, T23, T24, T25, T21, X22, X23, T14, splitD_in_ggaa(T22, T23, T24, T25))
splitD_in_ggaa(T30, T31, .(T30, X58), X59) → U3_ggaa(T30, T31, X58, X59, splitC_in_gaa(T31, X59, X58))
splitC_in_gaa([], [], []) → splitC_out_gaa([], [], [])
splitC_in_gaa(.(T36, T37), .(T36, X76), X77) → U2_gaa(T36, T37, X76, X77, splitC_in_gaa(T37, X77, X76))
U2_gaa(T36, T37, X76, X77, splitC_out_gaa(T37, X77, X76)) → splitC_out_gaa(.(T36, T37), .(T36, X76), X77)
U3_ggaa(T30, T31, X58, X59, splitC_out_gaa(T31, X59, X58)) → splitD_out_ggaa(T30, T31, .(T30, X58), X59)
U7_ggaagaaa(T22, T23, T24, T25, T21, X22, X23, T14, splitD_out_ggaa(T22, T23, T24, T25)) → U8_ggaagaaa(T22, T23, T24, T25, T21, X22, X23, T14, pI_in_ggagaa(T21, T25, X22, T24, X23, T14))
pI_in_ggagaa(T21, T25, T38, T24, X23, T14) → U9_ggagaa(T21, T25, T38, T24, X23, T14, mergesortA_in_ga(.(T21, T25), T38))
U9_ggagaa(T21, T25, T38, T24, X23, T14, mergesortA_out_ga(.(T21, T25), T38)) → U10_ggagaa(T21, T25, T38, T24, X23, T14, pJ_in_gaga(T24, X23, T38, T14))
pJ_in_gaga(T24, T39, T38, T14) → U11_gaga(T24, T39, T38, T14, mergesortE_in_ga(T24, T39))
mergesortE_in_ga([], []) → mergesortE_out_ga([], [])
mergesortE_in_ga(.(T44, []), .(T44, [])) → mergesortE_out_ga(.(T44, []), .(T44, []))
mergesortE_in_ga(.(T51, .(T52, T53)), X105) → U4_ga(T51, T52, T53, X105, pF_in_gggaaaaa(T51, T52, T53, X101, X102, X103, X104, X105))
pF_in_gggaaaaa(T51, T52, T53, T54, T55, X103, X104, X105) → U13_gggaaaaa(T51, T52, T53, T54, T55, X103, X104, X105, splitD_in_ggaa(T51, .(T52, T53), T54, T55))
U13_gggaaaaa(T51, T52, T53, T54, T55, X103, X104, X105, splitD_out_ggaa(T51, .(T52, T53), T54, T55)) → U14_gggaaaaa(T51, T52, T53, T54, T55, X103, X104, X105, pK_in_gagaa(T54, X103, T55, X104, X105))
pK_in_gagaa(T54, T56, T55, X104, X105) → U15_gagaa(T54, T56, T55, X104, X105, mergesortE_in_ga(T54, T56))
U15_gagaa(T54, T56, T55, X104, X105, mergesortE_out_ga(T54, T56)) → U16_gagaa(T54, T56, T55, X104, X105, pL_in_gaga(T55, X104, T56, X105))
pL_in_gaga(T55, T57, T56, X105) → U17_gaga(T55, T57, T56, X105, mergesortE_in_ga(T55, T57))
U17_gaga(T55, T57, T56, X105, mergesortE_out_ga(T55, T57)) → U18_gaga(T55, T57, T56, X105, mergeH_in_gga(T56, T57, X105))
mergeH_in_gga([], T64, T64) → mergeH_out_gga([], T64, T64)
mergeH_in_gga(T69, [], T69) → mergeH_out_gga(T69, [], T69)
mergeH_in_gga(.(T83, T79), .(T83, T81), .(T83, X135)) → U6_gga(T83, T79, T81, X135, mergeG_in_gga(.(T83, T79), T81, X135))
mergeG_in_gga([], T90, T90) → mergeG_out_gga([], T90, T90)
mergeG_in_gga(T95, [], T95) → mergeG_out_gga(T95, [], T95)
mergeG_in_gga(.(T113, T107), .(T113, T109), .(T113, T111)) → U5_gga(T113, T107, T109, T111, mergeG_in_gga(.(T113, T107), T109, T111))
U5_gga(T113, T107, T109, T111, mergeG_out_gga(.(T113, T107), T109, T111)) → mergeG_out_gga(.(T113, T107), .(T113, T109), .(T113, T111))
U6_gga(T83, T79, T81, X135, mergeG_out_gga(.(T83, T79), T81, X135)) → mergeH_out_gga(.(T83, T79), .(T83, T81), .(T83, X135))
U18_gaga(T55, T57, T56, X105, mergeH_out_gga(T56, T57, X105)) → pL_out_gaga(T55, T57, T56, X105)
U16_gagaa(T54, T56, T55, X104, X105, pL_out_gaga(T55, X104, T56, X105)) → pK_out_gagaa(T54, T56, T55, X104, X105)
U14_gggaaaaa(T51, T52, T53, T54, T55, X103, X104, X105, pK_out_gagaa(T54, X103, T55, X104, X105)) → pF_out_gggaaaaa(T51, T52, T53, T54, T55, X103, X104, X105)
U4_ga(T51, T52, T53, X105, pF_out_gggaaaaa(T51, T52, T53, X101, X102, X103, X104, X105)) → mergesortE_out_ga(.(T51, .(T52, T53)), X105)
U11_gaga(T24, T39, T38, T14, mergesortE_out_ga(T24, T39)) → U12_gaga(T24, T39, T38, T14, mergeG_in_gga(T38, T39, T14))
U12_gaga(T24, T39, T38, T14, mergeG_out_gga(T38, T39, T14)) → pJ_out_gaga(T24, T39, T38, T14)
U10_ggagaa(T21, T25, T38, T24, X23, T14, pJ_out_gaga(T24, X23, T38, T14)) → pI_out_ggagaa(T21, T25, T38, T24, X23, T14)
U8_ggaagaaa(T22, T23, T24, T25, T21, X22, X23, T14, pI_out_ggagaa(T21, T25, X22, T24, X23, T14)) → pB_out_ggaagaaa(T22, T23, T24, T25, T21, X22, X23, T14)
U1_ga(T21, T22, T23, T14, pB_out_ggaagaaa(T22, T23, X41, X40, T21, X22, X23, T14)) → mergesortA_out_ga(.(T21, .(T22, T23)), T14)

(3) DependencyPairsProof (EQUIVALENT transformation)

Using Dependency Pairs [AG00,LOPSTR] we result in the following initial DP problem:
Pi DP problem:
The TRS P consists of the following rules:

MERGESORTA_IN_GA(.(T21, .(T22, T23)), T14) → U1_GA(T21, T22, T23, T14, pB_in_ggaagaaa(T22, T23, X41, X40, T21, X22, X23, T14))
MERGESORTA_IN_GA(.(T21, .(T22, T23)), T14) → PB_IN_GGAAGAAA(T22, T23, X41, X40, T21, X22, X23, T14)
PB_IN_GGAAGAAA(T22, T23, T24, T25, T21, X22, X23, T14) → U7_GGAAGAAA(T22, T23, T24, T25, T21, X22, X23, T14, splitD_in_ggaa(T22, T23, T24, T25))
PB_IN_GGAAGAAA(T22, T23, T24, T25, T21, X22, X23, T14) → SPLITD_IN_GGAA(T22, T23, T24, T25)
SPLITD_IN_GGAA(T30, T31, .(T30, X58), X59) → U3_GGAA(T30, T31, X58, X59, splitC_in_gaa(T31, X59, X58))
SPLITD_IN_GGAA(T30, T31, .(T30, X58), X59) → SPLITC_IN_GAA(T31, X59, X58)
SPLITC_IN_GAA(.(T36, T37), .(T36, X76), X77) → U2_GAA(T36, T37, X76, X77, splitC_in_gaa(T37, X77, X76))
SPLITC_IN_GAA(.(T36, T37), .(T36, X76), X77) → SPLITC_IN_GAA(T37, X77, X76)
U7_GGAAGAAA(T22, T23, T24, T25, T21, X22, X23, T14, splitD_out_ggaa(T22, T23, T24, T25)) → U8_GGAAGAAA(T22, T23, T24, T25, T21, X22, X23, T14, pI_in_ggagaa(T21, T25, X22, T24, X23, T14))
U7_GGAAGAAA(T22, T23, T24, T25, T21, X22, X23, T14, splitD_out_ggaa(T22, T23, T24, T25)) → PI_IN_GGAGAA(T21, T25, X22, T24, X23, T14)
PI_IN_GGAGAA(T21, T25, T38, T24, X23, T14) → U9_GGAGAA(T21, T25, T38, T24, X23, T14, mergesortA_in_ga(.(T21, T25), T38))
PI_IN_GGAGAA(T21, T25, T38, T24, X23, T14) → MERGESORTA_IN_GA(.(T21, T25), T38)
U9_GGAGAA(T21, T25, T38, T24, X23, T14, mergesortA_out_ga(.(T21, T25), T38)) → U10_GGAGAA(T21, T25, T38, T24, X23, T14, pJ_in_gaga(T24, X23, T38, T14))
U9_GGAGAA(T21, T25, T38, T24, X23, T14, mergesortA_out_ga(.(T21, T25), T38)) → PJ_IN_GAGA(T24, X23, T38, T14)
PJ_IN_GAGA(T24, T39, T38, T14) → U11_GAGA(T24, T39, T38, T14, mergesortE_in_ga(T24, T39))
PJ_IN_GAGA(T24, T39, T38, T14) → MERGESORTE_IN_GA(T24, T39)
MERGESORTE_IN_GA(.(T51, .(T52, T53)), X105) → U4_GA(T51, T52, T53, X105, pF_in_gggaaaaa(T51, T52, T53, X101, X102, X103, X104, X105))
MERGESORTE_IN_GA(.(T51, .(T52, T53)), X105) → PF_IN_GGGAAAAA(T51, T52, T53, X101, X102, X103, X104, X105)
PF_IN_GGGAAAAA(T51, T52, T53, T54, T55, X103, X104, X105) → U13_GGGAAAAA(T51, T52, T53, T54, T55, X103, X104, X105, splitD_in_ggaa(T51, .(T52, T53), T54, T55))
PF_IN_GGGAAAAA(T51, T52, T53, T54, T55, X103, X104, X105) → SPLITD_IN_GGAA(T51, .(T52, T53), T54, T55)
U13_GGGAAAAA(T51, T52, T53, T54, T55, X103, X104, X105, splitD_out_ggaa(T51, .(T52, T53), T54, T55)) → U14_GGGAAAAA(T51, T52, T53, T54, T55, X103, X104, X105, pK_in_gagaa(T54, X103, T55, X104, X105))
U13_GGGAAAAA(T51, T52, T53, T54, T55, X103, X104, X105, splitD_out_ggaa(T51, .(T52, T53), T54, T55)) → PK_IN_GAGAA(T54, X103, T55, X104, X105)
PK_IN_GAGAA(T54, T56, T55, X104, X105) → U15_GAGAA(T54, T56, T55, X104, X105, mergesortE_in_ga(T54, T56))
PK_IN_GAGAA(T54, T56, T55, X104, X105) → MERGESORTE_IN_GA(T54, T56)
U15_GAGAA(T54, T56, T55, X104, X105, mergesortE_out_ga(T54, T56)) → U16_GAGAA(T54, T56, T55, X104, X105, pL_in_gaga(T55, X104, T56, X105))
U15_GAGAA(T54, T56, T55, X104, X105, mergesortE_out_ga(T54, T56)) → PL_IN_GAGA(T55, X104, T56, X105)
PL_IN_GAGA(T55, T57, T56, X105) → U17_GAGA(T55, T57, T56, X105, mergesortE_in_ga(T55, T57))
PL_IN_GAGA(T55, T57, T56, X105) → MERGESORTE_IN_GA(T55, T57)
U17_GAGA(T55, T57, T56, X105, mergesortE_out_ga(T55, T57)) → U18_GAGA(T55, T57, T56, X105, mergeH_in_gga(T56, T57, X105))
U17_GAGA(T55, T57, T56, X105, mergesortE_out_ga(T55, T57)) → MERGEH_IN_GGA(T56, T57, X105)
MERGEH_IN_GGA(.(T83, T79), .(T83, T81), .(T83, X135)) → U6_GGA(T83, T79, T81, X135, mergeG_in_gga(.(T83, T79), T81, X135))
MERGEH_IN_GGA(.(T83, T79), .(T83, T81), .(T83, X135)) → MERGEG_IN_GGA(.(T83, T79), T81, X135)
MERGEG_IN_GGA(.(T113, T107), .(T113, T109), .(T113, T111)) → U5_GGA(T113, T107, T109, T111, mergeG_in_gga(.(T113, T107), T109, T111))
MERGEG_IN_GGA(.(T113, T107), .(T113, T109), .(T113, T111)) → MERGEG_IN_GGA(.(T113, T107), T109, T111)
U11_GAGA(T24, T39, T38, T14, mergesortE_out_ga(T24, T39)) → U12_GAGA(T24, T39, T38, T14, mergeG_in_gga(T38, T39, T14))
U11_GAGA(T24, T39, T38, T14, mergesortE_out_ga(T24, T39)) → MERGEG_IN_GGA(T38, T39, T14)

The TRS R consists of the following rules:

mergesortA_in_ga([], []) → mergesortA_out_ga([], [])
mergesortA_in_ga(.(T4, []), .(T4, [])) → mergesortA_out_ga(.(T4, []), .(T4, []))
mergesortA_in_ga(.(T21, .(T22, T23)), T14) → U1_ga(T21, T22, T23, T14, pB_in_ggaagaaa(T22, T23, X41, X40, T21, X22, X23, T14))
pB_in_ggaagaaa(T22, T23, T24, T25, T21, X22, X23, T14) → U7_ggaagaaa(T22, T23, T24, T25, T21, X22, X23, T14, splitD_in_ggaa(T22, T23, T24, T25))
splitD_in_ggaa(T30, T31, .(T30, X58), X59) → U3_ggaa(T30, T31, X58, X59, splitC_in_gaa(T31, X59, X58))
splitC_in_gaa([], [], []) → splitC_out_gaa([], [], [])
splitC_in_gaa(.(T36, T37), .(T36, X76), X77) → U2_gaa(T36, T37, X76, X77, splitC_in_gaa(T37, X77, X76))
U2_gaa(T36, T37, X76, X77, splitC_out_gaa(T37, X77, X76)) → splitC_out_gaa(.(T36, T37), .(T36, X76), X77)
U3_ggaa(T30, T31, X58, X59, splitC_out_gaa(T31, X59, X58)) → splitD_out_ggaa(T30, T31, .(T30, X58), X59)
U7_ggaagaaa(T22, T23, T24, T25, T21, X22, X23, T14, splitD_out_ggaa(T22, T23, T24, T25)) → U8_ggaagaaa(T22, T23, T24, T25, T21, X22, X23, T14, pI_in_ggagaa(T21, T25, X22, T24, X23, T14))
pI_in_ggagaa(T21, T25, T38, T24, X23, T14) → U9_ggagaa(T21, T25, T38, T24, X23, T14, mergesortA_in_ga(.(T21, T25), T38))
U9_ggagaa(T21, T25, T38, T24, X23, T14, mergesortA_out_ga(.(T21, T25), T38)) → U10_ggagaa(T21, T25, T38, T24, X23, T14, pJ_in_gaga(T24, X23, T38, T14))
pJ_in_gaga(T24, T39, T38, T14) → U11_gaga(T24, T39, T38, T14, mergesortE_in_ga(T24, T39))
mergesortE_in_ga([], []) → mergesortE_out_ga([], [])
mergesortE_in_ga(.(T44, []), .(T44, [])) → mergesortE_out_ga(.(T44, []), .(T44, []))
mergesortE_in_ga(.(T51, .(T52, T53)), X105) → U4_ga(T51, T52, T53, X105, pF_in_gggaaaaa(T51, T52, T53, X101, X102, X103, X104, X105))
pF_in_gggaaaaa(T51, T52, T53, T54, T55, X103, X104, X105) → U13_gggaaaaa(T51, T52, T53, T54, T55, X103, X104, X105, splitD_in_ggaa(T51, .(T52, T53), T54, T55))
U13_gggaaaaa(T51, T52, T53, T54, T55, X103, X104, X105, splitD_out_ggaa(T51, .(T52, T53), T54, T55)) → U14_gggaaaaa(T51, T52, T53, T54, T55, X103, X104, X105, pK_in_gagaa(T54, X103, T55, X104, X105))
pK_in_gagaa(T54, T56, T55, X104, X105) → U15_gagaa(T54, T56, T55, X104, X105, mergesortE_in_ga(T54, T56))
U15_gagaa(T54, T56, T55, X104, X105, mergesortE_out_ga(T54, T56)) → U16_gagaa(T54, T56, T55, X104, X105, pL_in_gaga(T55, X104, T56, X105))
pL_in_gaga(T55, T57, T56, X105) → U17_gaga(T55, T57, T56, X105, mergesortE_in_ga(T55, T57))
U17_gaga(T55, T57, T56, X105, mergesortE_out_ga(T55, T57)) → U18_gaga(T55, T57, T56, X105, mergeH_in_gga(T56, T57, X105))
mergeH_in_gga([], T64, T64) → mergeH_out_gga([], T64, T64)
mergeH_in_gga(T69, [], T69) → mergeH_out_gga(T69, [], T69)
mergeH_in_gga(.(T83, T79), .(T83, T81), .(T83, X135)) → U6_gga(T83, T79, T81, X135, mergeG_in_gga(.(T83, T79), T81, X135))
mergeG_in_gga([], T90, T90) → mergeG_out_gga([], T90, T90)
mergeG_in_gga(T95, [], T95) → mergeG_out_gga(T95, [], T95)
mergeG_in_gga(.(T113, T107), .(T113, T109), .(T113, T111)) → U5_gga(T113, T107, T109, T111, mergeG_in_gga(.(T113, T107), T109, T111))
U5_gga(T113, T107, T109, T111, mergeG_out_gga(.(T113, T107), T109, T111)) → mergeG_out_gga(.(T113, T107), .(T113, T109), .(T113, T111))
U6_gga(T83, T79, T81, X135, mergeG_out_gga(.(T83, T79), T81, X135)) → mergeH_out_gga(.(T83, T79), .(T83, T81), .(T83, X135))
U18_gaga(T55, T57, T56, X105, mergeH_out_gga(T56, T57, X105)) → pL_out_gaga(T55, T57, T56, X105)
U16_gagaa(T54, T56, T55, X104, X105, pL_out_gaga(T55, X104, T56, X105)) → pK_out_gagaa(T54, T56, T55, X104, X105)
U14_gggaaaaa(T51, T52, T53, T54, T55, X103, X104, X105, pK_out_gagaa(T54, X103, T55, X104, X105)) → pF_out_gggaaaaa(T51, T52, T53, T54, T55, X103, X104, X105)
U4_ga(T51, T52, T53, X105, pF_out_gggaaaaa(T51, T52, T53, X101, X102, X103, X104, X105)) → mergesortE_out_ga(.(T51, .(T52, T53)), X105)
U11_gaga(T24, T39, T38, T14, mergesortE_out_ga(T24, T39)) → U12_gaga(T24, T39, T38, T14, mergeG_in_gga(T38, T39, T14))
U12_gaga(T24, T39, T38, T14, mergeG_out_gga(T38, T39, T14)) → pJ_out_gaga(T24, T39, T38, T14)
U10_ggagaa(T21, T25, T38, T24, X23, T14, pJ_out_gaga(T24, X23, T38, T14)) → pI_out_ggagaa(T21, T25, T38, T24, X23, T14)
U8_ggaagaaa(T22, T23, T24, T25, T21, X22, X23, T14, pI_out_ggagaa(T21, T25, X22, T24, X23, T14)) → pB_out_ggaagaaa(T22, T23, T24, T25, T21, X22, X23, T14)
U1_ga(T21, T22, T23, T14, pB_out_ggaagaaa(T22, T23, X41, X40, T21, X22, X23, T14)) → mergesortA_out_ga(.(T21, .(T22, T23)), T14)

The argument filtering Pi contains the following mapping:
mergesortA_in_ga(x1, x2) = mergesortA_in_ga(x1)
[] = []
mergesortA_out_ga(x1, x2) = mergesortA_out_ga(x1, x2)
.(x1, x2) = .(x1, x2)
U1_ga(x1, x2, x3, x4, x5) = U1_ga(x1, x2, x3, x5)
pB_in_ggaagaaa(x1, x2, x3, x4, x5, x6, x7, x8) = pB_in_ggaagaaa(x1, x2, x5)
U7_ggaagaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9) = U7_ggaagaaa(x1, x2, x5, x9)
splitD_in_ggaa(x1, x2, x3, x4) = splitD_in_ggaa(x1, x2)
U3_ggaa(x1, x2, x3, x4, x5) = U3_ggaa(x1, x2, x5)
splitC_in_gaa(x1, x2, x3) = splitC_in_gaa(x1)
splitC_out_gaa(x1, x2, x3) = splitC_out_gaa(x1, x2, x3)
U2_gaa(x1, x2, x3, x4, x5) = U2_gaa(x1, x2, x5)
splitD_out_ggaa(x1, x2, x3, x4) = splitD_out_ggaa(x1, x2, x3, x4)
U8_ggaagaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9) = U8_ggaagaaa(x1, x2, x3, x4, x5, x9)
pI_in_ggagaa(x1, x2, x3, x4, x5, x6) = pI_in_ggagaa(x1, x2, x4)
U9_ggagaa(x1, x2, x3, x4, x5, x6, x7) = U9_ggagaa(x1, x2, x4, x7)
U10_ggagaa(x1, x2, x3, x4, x5, x6, x7) = U10_ggagaa(x1, x2, x3, x4, x7)
pJ_in_gaga(x1, x2, x3, x4) = pJ_in_gaga(x1, x3)
U11_gaga(x1, x2, x3, x4, x5) = U11_gaga(x1, x3, x5)
mergesortE_in_ga(x1, x2) = mergesortE_in_ga(x1)
mergesortE_out_ga(x1, x2) = mergesortE_out_ga(x1, x2)
U4_ga(x1, x2, x3, x4, x5) = U4_ga(x1, x2, x3, x5)
pF_in_gggaaaaa(x1, x2, x3, x4, x5, x6, x7, x8) = pF_in_gggaaaaa(x1, x2, x3)
U13_gggaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9) = U13_gggaaaaa(x1, x2, x3, x9)
U14_gggaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9) = U14_gggaaaaa(x1, x2, x3, x4, x5, x9)
pK_in_gagaa(x1, x2, x3, x4, x5) = pK_in_gagaa(x1, x3)
U15_gagaa(x1, x2, x3, x4, x5, x6) = U15_gagaa(x1, x3, x6)
U16_gagaa(x1, x2, x3, x4, x5, x6) = U16_gagaa(x1, x2, x3, x6)
pL_in_gaga(x1, x2, x3, x4) = pL_in_gaga(x1, x3)
U17_gaga(x1, x2, x3, x4, x5) = U17_gaga(x1, x3, x5)
U18_gaga(x1, x2, x3, x4, x5) = U18_gaga(x1, x2, x3, x5)
mergeH_in_gga(x1, x2, x3) = mergeH_in_gga(x1, x2)
mergeH_out_gga(x1, x2, x3) = mergeH_out_gga(x1, x2, x3)
U6_gga(x1, x2, x3, x4, x5) = U6_gga(x1, x2, x3, x5)
mergeG_in_gga(x1, x2, x3) = mergeG_in_gga(x1, x2)
mergeG_out_gga(x1, x2, x3) = mergeG_out_gga(x1, x2, x3)
U5_gga(x1, x2, x3, x4, x5) = U5_gga(x1, x2, x3, x5)
pL_out_gaga(x1, x2, x3, x4) = pL_out_gaga(x1, x2, x3, x4)
pK_out_gagaa(x1, x2, x3, x4, x5) = pK_out_gagaa(x1, x2, x3, x4, x5)
pF_out_gggaaaaa(x1, x2, x3, x4, x5, x6, x7, x8) = pF_out_gggaaaaa(x1, x2, x3, x4, x5, x6, x7, x8)
U12_gaga(x1, x2, x3, x4, x5) = U12_gaga(x1, x2, x3, x5)
pJ_out_gaga(x1, x2, x3, x4) = pJ_out_gaga(x1, x2, x3, x4)
pI_out_ggagaa(x1, x2, x3, x4, x5, x6) = pI_out_ggagaa(x1, x2, x3, x4, x5, x6)
pB_out_ggaagaaa(x1, x2, x3, x4, x5, x6, x7, x8) = pB_out_ggaagaaa(x1, x2, x3, x4, x5, x6, x7, x8)
MERGESORTA_IN_GA(x1, x2) = MERGESORTA_IN_GA(x1)
U1_GA(x1, x2, x3, x4, x5) = U1_GA(x1, x2, x3, x5)
PB_IN_GGAAGAAA(x1, x2, x3, x4, x5, x6, x7, x8) = PB_IN_GGAAGAAA(x1, x2, x5)
U7_GGAAGAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9) = U7_GGAAGAAA(x1, x2, x5, x9)
SPLITD_IN_GGAA(x1, x2, x3, x4) = SPLITD_IN_GGAA(x1, x2)
U3_GGAA(x1, x2, x3, x4, x5) = U3_GGAA(x1, x2, x5)
SPLITC_IN_GAA(x1, x2, x3) = SPLITC_IN_GAA(x1)
U2_GAA(x1, x2, x3, x4, x5) = U2_GAA(x1, x2, x5)
U8_GGAAGAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9) = U8_GGAAGAAA(x1, x2, x3, x4, x5, x9)
PI_IN_GGAGAA(x1, x2, x3, x4, x5, x6) = PI_IN_GGAGAA(x1, x2, x4)
U9_GGAGAA(x1, x2, x3, x4, x5, x6, x7) = U9_GGAGAA(x1, x2, x4, x7)
U10_GGAGAA(x1, x2, x3, x4, x5, x6, x7) = U10_GGAGAA(x1, x2, x3, x4, x7)
PJ_IN_GAGA(x1, x2, x3, x4) = PJ_IN_GAGA(x1, x3)
U11_GAGA(x1, x2, x3, x4, x5) = U11_GAGA(x1, x3, x5)
MERGESORTE_IN_GA(x1, x2) = MERGESORTE_IN_GA(x1)
U4_GA(x1, x2, x3, x4, x5) = U4_GA(x1, x2, x3, x5)
PF_IN_GGGAAAAA(x1, x2, x3, x4, x5, x6, x7, x8) = PF_IN_GGGAAAAA(x1, x2, x3)
U13_GGGAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9) = U13_GGGAAAAA(x1, x2, x3, x9)
U14_GGGAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9) = U14_GGGAAAAA(x1, x2, x3, x4, x5, x9)
PK_IN_GAGAA(x1, x2, x3, x4, x5) = PK_IN_GAGAA(x1, x3)
U15_GAGAA(x1, x2, x3, x4, x5, x6) = U15_GAGAA(x1, x3, x6)
U16_GAGAA(x1, x2, x3, x4, x5, x6) = U16_GAGAA(x1, x2, x3, x6)
PL_IN_GAGA(x1, x2, x3, x4) = PL_IN_GAGA(x1, x3)
U17_GAGA(x1, x2, x3, x4, x5) = U17_GAGA(x1, x3, x5)
U18_GAGA(x1, x2, x3, x4, x5) = U18_GAGA(x1, x2, x3, x5)
MERGEH_IN_GGA(x1, x2, x3) = MERGEH_IN_GGA(x1, x2)
U6_GGA(x1, x2, x3, x4, x5) = U6_GGA(x1, x2, x3, x5)
MERGEG_IN_GGA(x1, x2, x3) = MERGEG_IN_GGA(x1, x2)
U5_GGA(x1, x2, x3, x4, x5) = U5_GGA(x1, x2, x3, x5)
U12_GAGA(x1, x2, x3, x4, x5) = U12_GAGA(x1, x2, x3, x5)

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

(4) Obligation:

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

MERGESORTA_IN_GA(.(T21, .(T22, T23)), T14) → U1_GA(T21, T22, T23, T14, pB_in_ggaagaaa(T22, T23, X41, X40, T21, X22, X23, T14))
MERGESORTA_IN_GA(.(T21, .(T22, T23)), T14) → PB_IN_GGAAGAAA(T22, T23, X41, X40, T21, X22, X23, T14)
PB_IN_GGAAGAAA(T22, T23, T24, T25, T21, X22, X23, T14) → U7_GGAAGAAA(T22, T23, T24, T25, T21, X22, X23, T14, splitD_in_ggaa(T22, T23, T24, T25))
PB_IN_GGAAGAAA(T22, T23, T24, T25, T21, X22, X23, T14) → SPLITD_IN_GGAA(T22, T23, T24, T25)
SPLITD_IN_GGAA(T30, T31, .(T30, X58), X59) → U3_GGAA(T30, T31, X58, X59, splitC_in_gaa(T31, X59, X58))
SPLITD_IN_GGAA(T30, T31, .(T30, X58), X59) → SPLITC_IN_GAA(T31, X59, X58)
SPLITC_IN_GAA(.(T36, T37), .(T36, X76), X77) → U2_GAA(T36, T37, X76, X77, splitC_in_gaa(T37, X77, X76))
SPLITC_IN_GAA(.(T36, T37), .(T36, X76), X77) → SPLITC_IN_GAA(T37, X77, X76)
U7_GGAAGAAA(T22, T23, T24, T25, T21, X22, X23, T14, splitD_out_ggaa(T22, T23, T24, T25)) → U8_GGAAGAAA(T22, T23, T24, T25, T21, X22, X23, T14, pI_in_ggagaa(T21, T25, X22, T24, X23, T14))
U7_GGAAGAAA(T22, T23, T24, T25, T21, X22, X23, T14, splitD_out_ggaa(T22, T23, T24, T25)) → PI_IN_GGAGAA(T21, T25, X22, T24, X23, T14)
PI_IN_GGAGAA(T21, T25, T38, T24, X23, T14) → U9_GGAGAA(T21, T25, T38, T24, X23, T14, mergesortA_in_ga(.(T21, T25), T38))
PI_IN_GGAGAA(T21, T25, T38, T24, X23, T14) → MERGESORTA_IN_GA(.(T21, T25), T38)
U9_GGAGAA(T21, T25, T38, T24, X23, T14, mergesortA_out_ga(.(T21, T25), T38)) → U10_GGAGAA(T21, T25, T38, T24, X23, T14, pJ_in_gaga(T24, X23, T38, T14))
U9_GGAGAA(T21, T25, T38, T24, X23, T14, mergesortA_out_ga(.(T21, T25), T38)) → PJ_IN_GAGA(T24, X23, T38, T14)
PJ_IN_GAGA(T24, T39, T38, T14) → U11_GAGA(T24, T39, T38, T14, mergesortE_in_ga(T24, T39))
PJ_IN_GAGA(T24, T39, T38, T14) → MERGESORTE_IN_GA(T24, T39)
MERGESORTE_IN_GA(.(T51, .(T52, T53)), X105) → U4_GA(T51, T52, T53, X105, pF_in_gggaaaaa(T51, T52, T53, X101, X102, X103, X104, X105))
MERGESORTE_IN_GA(.(T51, .(T52, T53)), X105) → PF_IN_GGGAAAAA(T51, T52, T53, X101, X102, X103, X104, X105)
PF_IN_GGGAAAAA(T51, T52, T53, T54, T55, X103, X104, X105) → U13_GGGAAAAA(T51, T52, T53, T54, T55, X103, X104, X105, splitD_in_ggaa(T51, .(T52, T53), T54, T55))
PF_IN_GGGAAAAA(T51, T52, T53, T54, T55, X103, X104, X105) → SPLITD_IN_GGAA(T51, .(T52, T53), T54, T55)
U13_GGGAAAAA(T51, T52, T53, T54, T55, X103, X104, X105, splitD_out_ggaa(T51, .(T52, T53), T54, T55)) → U14_GGGAAAAA(T51, T52, T53, T54, T55, X103, X104, X105, pK_in_gagaa(T54, X103, T55, X104, X105))
U13_GGGAAAAA(T51, T52, T53, T54, T55, X103, X104, X105, splitD_out_ggaa(T51, .(T52, T53), T54, T55)) → PK_IN_GAGAA(T54, X103, T55, X104, X105)
PK_IN_GAGAA(T54, T56, T55, X104, X105) → U15_GAGAA(T54, T56, T55, X104, X105, mergesortE_in_ga(T54, T56))
PK_IN_GAGAA(T54, T56, T55, X104, X105) → MERGESORTE_IN_GA(T54, T56)
U15_GAGAA(T54, T56, T55, X104, X105, mergesortE_out_ga(T54, T56)) → U16_GAGAA(T54, T56, T55, X104, X105, pL_in_gaga(T55, X104, T56, X105))
U15_GAGAA(T54, T56, T55, X104, X105, mergesortE_out_ga(T54, T56)) → PL_IN_GAGA(T55, X104, T56, X105)
PL_IN_GAGA(T55, T57, T56, X105) → U17_GAGA(T55, T57, T56, X105, mergesortE_in_ga(T55, T57))
PL_IN_GAGA(T55, T57, T56, X105) → MERGESORTE_IN_GA(T55, T57)
U17_GAGA(T55, T57, T56, X105, mergesortE_out_ga(T55, T57)) → U18_GAGA(T55, T57, T56, X105, mergeH_in_gga(T56, T57, X105))
U17_GAGA(T55, T57, T56, X105, mergesortE_out_ga(T55, T57)) → MERGEH_IN_GGA(T56, T57, X105)
MERGEH_IN_GGA(.(T83, T79), .(T83, T81), .(T83, X135)) → U6_GGA(T83, T79, T81, X135, mergeG_in_gga(.(T83, T79), T81, X135))
MERGEH_IN_GGA(.(T83, T79), .(T83, T81), .(T83, X135)) → MERGEG_IN_GGA(.(T83, T79), T81, X135)
MERGEG_IN_GGA(.(T113, T107), .(T113, T109), .(T113, T111)) → U5_GGA(T113, T107, T109, T111, mergeG_in_gga(.(T113, T107), T109, T111))
MERGEG_IN_GGA(.(T113, T107), .(T113, T109), .(T113, T111)) → MERGEG_IN_GGA(.(T113, T107), T109, T111)
U11_GAGA(T24, T39, T38, T14, mergesortE_out_ga(T24, T39)) → U12_GAGA(T24, T39, T38, T14, mergeG_in_gga(T38, T39, T14))
U11_GAGA(T24, T39, T38, T14, mergesortE_out_ga(T24, T39)) → MERGEG_IN_GGA(T38, T39, T14)

The TRS R consists of the following rules:

mergesortA_in_ga([], []) → mergesortA_out_ga([], [])
mergesortA_in_ga(.(T4, []), .(T4, [])) → mergesortA_out_ga(.(T4, []), .(T4, []))
mergesortA_in_ga(.(T21, .(T22, T23)), T14) → U1_ga(T21, T22, T23, T14, pB_in_ggaagaaa(T22, T23, X41, X40, T21, X22, X23, T14))
pB_in_ggaagaaa(T22, T23, T24, T25, T21, X22, X23, T14) → U7_ggaagaaa(T22, T23, T24, T25, T21, X22, X23, T14, splitD_in_ggaa(T22, T23, T24, T25))
splitD_in_ggaa(T30, T31, .(T30, X58), X59) → U3_ggaa(T30, T31, X58, X59, splitC_in_gaa(T31, X59, X58))
splitC_in_gaa([], [], []) → splitC_out_gaa([], [], [])
splitC_in_gaa(.(T36, T37), .(T36, X76), X77) → U2_gaa(T36, T37, X76, X77, splitC_in_gaa(T37, X77, X76))
U2_gaa(T36, T37, X76, X77, splitC_out_gaa(T37, X77, X76)) → splitC_out_gaa(.(T36, T37), .(T36, X76), X77)
U3_ggaa(T30, T31, X58, X59, splitC_out_gaa(T31, X59, X58)) → splitD_out_ggaa(T30, T31, .(T30, X58), X59)
U7_ggaagaaa(T22, T23, T24, T25, T21, X22, X23, T14, splitD_out_ggaa(T22, T23, T24, T25)) → U8_ggaagaaa(T22, T23, T24, T25, T21, X22, X23, T14, pI_in_ggagaa(T21, T25, X22, T24, X23, T14))
pI_in_ggagaa(T21, T25, T38, T24, X23, T14) → U9_ggagaa(T21, T25, T38, T24, X23, T14, mergesortA_in_ga(.(T21, T25), T38))
U9_ggagaa(T21, T25, T38, T24, X23, T14, mergesortA_out_ga(.(T21, T25), T38)) → U10_ggagaa(T21, T25, T38, T24, X23, T14, pJ_in_gaga(T24, X23, T38, T14))
pJ_in_gaga(T24, T39, T38, T14) → U11_gaga(T24, T39, T38, T14, mergesortE_in_ga(T24, T39))
mergesortE_in_ga([], []) → mergesortE_out_ga([], [])
mergesortE_in_ga(.(T44, []), .(T44, [])) → mergesortE_out_ga(.(T44, []), .(T44, []))
mergesortE_in_ga(.(T51, .(T52, T53)), X105) → U4_ga(T51, T52, T53, X105, pF_in_gggaaaaa(T51, T52, T53, X101, X102, X103, X104, X105))
pF_in_gggaaaaa(T51, T52, T53, T54, T55, X103, X104, X105) → U13_gggaaaaa(T51, T52, T53, T54, T55, X103, X104, X105, splitD_in_ggaa(T51, .(T52, T53), T54, T55))
U13_gggaaaaa(T51, T52, T53, T54, T55, X103, X104, X105, splitD_out_ggaa(T51, .(T52, T53), T54, T55)) → U14_gggaaaaa(T51, T52, T53, T54, T55, X103, X104, X105, pK_in_gagaa(T54, X103, T55, X104, X105))
pK_in_gagaa(T54, T56, T55, X104, X105) → U15_gagaa(T54, T56, T55, X104, X105, mergesortE_in_ga(T54, T56))
U15_gagaa(T54, T56, T55, X104, X105, mergesortE_out_ga(T54, T56)) → U16_gagaa(T54, T56, T55, X104, X105, pL_in_gaga(T55, X104, T56, X105))
pL_in_gaga(T55, T57, T56, X105) → U17_gaga(T55, T57, T56, X105, mergesortE_in_ga(T55, T57))
U17_gaga(T55, T57, T56, X105, mergesortE_out_ga(T55, T57)) → U18_gaga(T55, T57, T56, X105, mergeH_in_gga(T56, T57, X105))
mergeH_in_gga([], T64, T64) → mergeH_out_gga([], T64, T64)
mergeH_in_gga(T69, [], T69) → mergeH_out_gga(T69, [], T69)
mergeH_in_gga(.(T83, T79), .(T83, T81), .(T83, X135)) → U6_gga(T83, T79, T81, X135, mergeG_in_gga(.(T83, T79), T81, X135))
mergeG_in_gga([], T90, T90) → mergeG_out_gga([], T90, T90)
mergeG_in_gga(T95, [], T95) → mergeG_out_gga(T95, [], T95)
mergeG_in_gga(.(T113, T107), .(T113, T109), .(T113, T111)) → U5_gga(T113, T107, T109, T111, mergeG_in_gga(.(T113, T107), T109, T111))
U5_gga(T113, T107, T109, T111, mergeG_out_gga(.(T113, T107), T109, T111)) → mergeG_out_gga(.(T113, T107), .(T113, T109), .(T113, T111))
U6_gga(T83, T79, T81, X135, mergeG_out_gga(.(T83, T79), T81, X135)) → mergeH_out_gga(.(T83, T79), .(T83, T81), .(T83, X135))
U18_gaga(T55, T57, T56, X105, mergeH_out_gga(T56, T57, X105)) → pL_out_gaga(T55, T57, T56, X105)
U16_gagaa(T54, T56, T55, X104, X105, pL_out_gaga(T55, X104, T56, X105)) → pK_out_gagaa(T54, T56, T55, X104, X105)
U14_gggaaaaa(T51, T52, T53, T54, T55, X103, X104, X105, pK_out_gagaa(T54, X103, T55, X104, X105)) → pF_out_gggaaaaa(T51, T52, T53, T54, T55, X103, X104, X105)
U4_ga(T51, T52, T53, X105, pF_out_gggaaaaa(T51, T52, T53, X101, X102, X103, X104, X105)) → mergesortE_out_ga(.(T51, .(T52, T53)), X105)
U11_gaga(T24, T39, T38, T14, mergesortE_out_ga(T24, T39)) → U12_gaga(T24, T39, T38, T14, mergeG_in_gga(T38, T39, T14))
U12_gaga(T24, T39, T38, T14, mergeG_out_gga(T38, T39, T14)) → pJ_out_gaga(T24, T39, T38, T14)
U10_ggagaa(T21, T25, T38, T24, X23, T14, pJ_out_gaga(T24, X23, T38, T14)) → pI_out_ggagaa(T21, T25, T38, T24, X23, T14)
U8_ggaagaaa(T22, T23, T24, T25, T21, X22, X23, T14, pI_out_ggagaa(T21, T25, X22, T24, X23, T14)) → pB_out_ggaagaaa(T22, T23, T24, T25, T21, X22, X23, T14)
U1_ga(T21, T22, T23, T14, pB_out_ggaagaaa(T22, T23, X41, X40, T21, X22, X23, T14)) → mergesortA_out_ga(.(T21, .(T22, T23)), T14)

(5) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 4 SCCs with 23 less nodes.

(6) Complex Obligation (AND)

(7) Obligation:

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

MERGEG_IN_GGA(.(T113, T107), .(T113, T109), .(T113, T111)) → MERGEG_IN_GGA(.(T113, T107), T109, T111)

The TRS R consists of the following rules:

mergesortA_in_ga([], []) → mergesortA_out_ga([], [])
mergesortA_in_ga(.(T4, []), .(T4, [])) → mergesortA_out_ga(.(T4, []), .(T4, []))
mergesortA_in_ga(.(T21, .(T22, T23)), T14) → U1_ga(T21, T22, T23, T14, pB_in_ggaagaaa(T22, T23, X41, X40, T21, X22, X23, T14))
pB_in_ggaagaaa(T22, T23, T24, T25, T21, X22, X23, T14) → U7_ggaagaaa(T22, T23, T24, T25, T21, X22, X23, T14, splitD_in_ggaa(T22, T23, T24, T25))
splitD_in_ggaa(T30, T31, .(T30, X58), X59) → U3_ggaa(T30, T31, X58, X59, splitC_in_gaa(T31, X59, X58))
splitC_in_gaa([], [], []) → splitC_out_gaa([], [], [])
splitC_in_gaa(.(T36, T37), .(T36, X76), X77) → U2_gaa(T36, T37, X76, X77, splitC_in_gaa(T37, X77, X76))
U2_gaa(T36, T37, X76, X77, splitC_out_gaa(T37, X77, X76)) → splitC_out_gaa(.(T36, T37), .(T36, X76), X77)
U3_ggaa(T30, T31, X58, X59, splitC_out_gaa(T31, X59, X58)) → splitD_out_ggaa(T30, T31, .(T30, X58), X59)
U7_ggaagaaa(T22, T23, T24, T25, T21, X22, X23, T14, splitD_out_ggaa(T22, T23, T24, T25)) → U8_ggaagaaa(T22, T23, T24, T25, T21, X22, X23, T14, pI_in_ggagaa(T21, T25, X22, T24, X23, T14))
pI_in_ggagaa(T21, T25, T38, T24, X23, T14) → U9_ggagaa(T21, T25, T38, T24, X23, T14, mergesortA_in_ga(.(T21, T25), T38))
U9_ggagaa(T21, T25, T38, T24, X23, T14, mergesortA_out_ga(.(T21, T25), T38)) → U10_ggagaa(T21, T25, T38, T24, X23, T14, pJ_in_gaga(T24, X23, T38, T14))
pJ_in_gaga(T24, T39, T38, T14) → U11_gaga(T24, T39, T38, T14, mergesortE_in_ga(T24, T39))
mergesortE_in_ga([], []) → mergesortE_out_ga([], [])
mergesortE_in_ga(.(T44, []), .(T44, [])) → mergesortE_out_ga(.(T44, []), .(T44, []))
mergesortE_in_ga(.(T51, .(T52, T53)), X105) → U4_ga(T51, T52, T53, X105, pF_in_gggaaaaa(T51, T52, T53, X101, X102, X103, X104, X105))
pF_in_gggaaaaa(T51, T52, T53, T54, T55, X103, X104, X105) → U13_gggaaaaa(T51, T52, T53, T54, T55, X103, X104, X105, splitD_in_ggaa(T51, .(T52, T53), T54, T55))
U13_gggaaaaa(T51, T52, T53, T54, T55, X103, X104, X105, splitD_out_ggaa(T51, .(T52, T53), T54, T55)) → U14_gggaaaaa(T51, T52, T53, T54, T55, X103, X104, X105, pK_in_gagaa(T54, X103, T55, X104, X105))
pK_in_gagaa(T54, T56, T55, X104, X105) → U15_gagaa(T54, T56, T55, X104, X105, mergesortE_in_ga(T54, T56))
U15_gagaa(T54, T56, T55, X104, X105, mergesortE_out_ga(T54, T56)) → U16_gagaa(T54, T56, T55, X104, X105, pL_in_gaga(T55, X104, T56, X105))
pL_in_gaga(T55, T57, T56, X105) → U17_gaga(T55, T57, T56, X105, mergesortE_in_ga(T55, T57))
U17_gaga(T55, T57, T56, X105, mergesortE_out_ga(T55, T57)) → U18_gaga(T55, T57, T56, X105, mergeH_in_gga(T56, T57, X105))
mergeH_in_gga([], T64, T64) → mergeH_out_gga([], T64, T64)
mergeH_in_gga(T69, [], T69) → mergeH_out_gga(T69, [], T69)
mergeH_in_gga(.(T83, T79), .(T83, T81), .(T83, X135)) → U6_gga(T83, T79, T81, X135, mergeG_in_gga(.(T83, T79), T81, X135))
mergeG_in_gga([], T90, T90) → mergeG_out_gga([], T90, T90)
mergeG_in_gga(T95, [], T95) → mergeG_out_gga(T95, [], T95)
mergeG_in_gga(.(T113, T107), .(T113, T109), .(T113, T111)) → U5_gga(T113, T107, T109, T111, mergeG_in_gga(.(T113, T107), T109, T111))
U5_gga(T113, T107, T109, T111, mergeG_out_gga(.(T113, T107), T109, T111)) → mergeG_out_gga(.(T113, T107), .(T113, T109), .(T113, T111))
U6_gga(T83, T79, T81, X135, mergeG_out_gga(.(T83, T79), T81, X135)) → mergeH_out_gga(.(T83, T79), .(T83, T81), .(T83, X135))
U18_gaga(T55, T57, T56, X105, mergeH_out_gga(T56, T57, X105)) → pL_out_gaga(T55, T57, T56, X105)
U16_gagaa(T54, T56, T55, X104, X105, pL_out_gaga(T55, X104, T56, X105)) → pK_out_gagaa(T54, T56, T55, X104, X105)
U14_gggaaaaa(T51, T52, T53, T54, T55, X103, X104, X105, pK_out_gagaa(T54, X103, T55, X104, X105)) → pF_out_gggaaaaa(T51, T52, T53, T54, T55, X103, X104, X105)
U4_ga(T51, T52, T53, X105, pF_out_gggaaaaa(T51, T52, T53, X101, X102, X103, X104, X105)) → mergesortE_out_ga(.(T51, .(T52, T53)), X105)
U11_gaga(T24, T39, T38, T14, mergesortE_out_ga(T24, T39)) → U12_gaga(T24, T39, T38, T14, mergeG_in_gga(T38, T39, T14))
U12_gaga(T24, T39, T38, T14, mergeG_out_gga(T38, T39, T14)) → pJ_out_gaga(T24, T39, T38, T14)
U10_ggagaa(T21, T25, T38, T24, X23, T14, pJ_out_gaga(T24, X23, T38, T14)) → pI_out_ggagaa(T21, T25, T38, T24, X23, T14)
U8_ggaagaaa(T22, T23, T24, T25, T21, X22, X23, T14, pI_out_ggagaa(T21, T25, X22, T24, X23, T14)) → pB_out_ggaagaaa(T22, T23, T24, T25, T21, X22, X23, T14)
U1_ga(T21, T22, T23, T14, pB_out_ggaagaaa(T22, T23, X41, X40, T21, X22, X23, T14)) → mergesortA_out_ga(.(T21, .(T22, T23)), T14)

(8) UsableRulesProof (EQUIVALENT transformation)

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

(9) Obligation:

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

MERGEG_IN_GGA(.(T113, T107), .(T113, T109), .(T113, T111)) → MERGEG_IN_GGA(.(T113, T107), T109, T111)

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

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

(10) PiDPToQDPProof (SOUND transformation)

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

(11) Obligation:

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

MERGEG_IN_GGA(.(T113, T107), .(T113, T109)) → MERGEG_IN_GGA(.(T113, T107), T109)

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

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

MERGEG_IN_GGA(.(T113, T107), .(T113, T109)) → MERGEG_IN_GGA(.(T113, T107), T109)
The graph contains the following edges 1 >= 1, 2 > 2

(13) YES

(14) Obligation:

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

SPLITC_IN_GAA(.(T36, T37), .(T36, X76), X77) → SPLITC_IN_GAA(T37, X77, X76)

The TRS R consists of the following rules:

mergesortA_in_ga([], []) → mergesortA_out_ga([], [])
mergesortA_in_ga(.(T4, []), .(T4, [])) → mergesortA_out_ga(.(T4, []), .(T4, []))
mergesortA_in_ga(.(T21, .(T22, T23)), T14) → U1_ga(T21, T22, T23, T14, pB_in_ggaagaaa(T22, T23, X41, X40, T21, X22, X23, T14))
pB_in_ggaagaaa(T22, T23, T24, T25, T21, X22, X23, T14) → U7_ggaagaaa(T22, T23, T24, T25, T21, X22, X23, T14, splitD_in_ggaa(T22, T23, T24, T25))
splitD_in_ggaa(T30, T31, .(T30, X58), X59) → U3_ggaa(T30, T31, X58, X59, splitC_in_gaa(T31, X59, X58))
splitC_in_gaa([], [], []) → splitC_out_gaa([], [], [])
splitC_in_gaa(.(T36, T37), .(T36, X76), X77) → U2_gaa(T36, T37, X76, X77, splitC_in_gaa(T37, X77, X76))
U2_gaa(T36, T37, X76, X77, splitC_out_gaa(T37, X77, X76)) → splitC_out_gaa(.(T36, T37), .(T36, X76), X77)
U3_ggaa(T30, T31, X58, X59, splitC_out_gaa(T31, X59, X58)) → splitD_out_ggaa(T30, T31, .(T30, X58), X59)
U7_ggaagaaa(T22, T23, T24, T25, T21, X22, X23, T14, splitD_out_ggaa(T22, T23, T24, T25)) → U8_ggaagaaa(T22, T23, T24, T25, T21, X22, X23, T14, pI_in_ggagaa(T21, T25, X22, T24, X23, T14))
pI_in_ggagaa(T21, T25, T38, T24, X23, T14) → U9_ggagaa(T21, T25, T38, T24, X23, T14, mergesortA_in_ga(.(T21, T25), T38))
U9_ggagaa(T21, T25, T38, T24, X23, T14, mergesortA_out_ga(.(T21, T25), T38)) → U10_ggagaa(T21, T25, T38, T24, X23, T14, pJ_in_gaga(T24, X23, T38, T14))
pJ_in_gaga(T24, T39, T38, T14) → U11_gaga(T24, T39, T38, T14, mergesortE_in_ga(T24, T39))
mergesortE_in_ga([], []) → mergesortE_out_ga([], [])
mergesortE_in_ga(.(T44, []), .(T44, [])) → mergesortE_out_ga(.(T44, []), .(T44, []))
mergesortE_in_ga(.(T51, .(T52, T53)), X105) → U4_ga(T51, T52, T53, X105, pF_in_gggaaaaa(T51, T52, T53, X101, X102, X103, X104, X105))
pF_in_gggaaaaa(T51, T52, T53, T54, T55, X103, X104, X105) → U13_gggaaaaa(T51, T52, T53, T54, T55, X103, X104, X105, splitD_in_ggaa(T51, .(T52, T53), T54, T55))
U13_gggaaaaa(T51, T52, T53, T54, T55, X103, X104, X105, splitD_out_ggaa(T51, .(T52, T53), T54, T55)) → U14_gggaaaaa(T51, T52, T53, T54, T55, X103, X104, X105, pK_in_gagaa(T54, X103, T55, X104, X105))
pK_in_gagaa(T54, T56, T55, X104, X105) → U15_gagaa(T54, T56, T55, X104, X105, mergesortE_in_ga(T54, T56))
U15_gagaa(T54, T56, T55, X104, X105, mergesortE_out_ga(T54, T56)) → U16_gagaa(T54, T56, T55, X104, X105, pL_in_gaga(T55, X104, T56, X105))
pL_in_gaga(T55, T57, T56, X105) → U17_gaga(T55, T57, T56, X105, mergesortE_in_ga(T55, T57))
U17_gaga(T55, T57, T56, X105, mergesortE_out_ga(T55, T57)) → U18_gaga(T55, T57, T56, X105, mergeH_in_gga(T56, T57, X105))
mergeH_in_gga([], T64, T64) → mergeH_out_gga([], T64, T64)
mergeH_in_gga(T69, [], T69) → mergeH_out_gga(T69, [], T69)
mergeH_in_gga(.(T83, T79), .(T83, T81), .(T83, X135)) → U6_gga(T83, T79, T81, X135, mergeG_in_gga(.(T83, T79), T81, X135))
mergeG_in_gga([], T90, T90) → mergeG_out_gga([], T90, T90)
mergeG_in_gga(T95, [], T95) → mergeG_out_gga(T95, [], T95)
mergeG_in_gga(.(T113, T107), .(T113, T109), .(T113, T111)) → U5_gga(T113, T107, T109, T111, mergeG_in_gga(.(T113, T107), T109, T111))
U5_gga(T113, T107, T109, T111, mergeG_out_gga(.(T113, T107), T109, T111)) → mergeG_out_gga(.(T113, T107), .(T113, T109), .(T113, T111))
U6_gga(T83, T79, T81, X135, mergeG_out_gga(.(T83, T79), T81, X135)) → mergeH_out_gga(.(T83, T79), .(T83, T81), .(T83, X135))
U18_gaga(T55, T57, T56, X105, mergeH_out_gga(T56, T57, X105)) → pL_out_gaga(T55, T57, T56, X105)
U16_gagaa(T54, T56, T55, X104, X105, pL_out_gaga(T55, X104, T56, X105)) → pK_out_gagaa(T54, T56, T55, X104, X105)
U14_gggaaaaa(T51, T52, T53, T54, T55, X103, X104, X105, pK_out_gagaa(T54, X103, T55, X104, X105)) → pF_out_gggaaaaa(T51, T52, T53, T54, T55, X103, X104, X105)
U4_ga(T51, T52, T53, X105, pF_out_gggaaaaa(T51, T52, T53, X101, X102, X103, X104, X105)) → mergesortE_out_ga(.(T51, .(T52, T53)), X105)
U11_gaga(T24, T39, T38, T14, mergesortE_out_ga(T24, T39)) → U12_gaga(T24, T39, T38, T14, mergeG_in_gga(T38, T39, T14))
U12_gaga(T24, T39, T38, T14, mergeG_out_gga(T38, T39, T14)) → pJ_out_gaga(T24, T39, T38, T14)
U10_ggagaa(T21, T25, T38, T24, X23, T14, pJ_out_gaga(T24, X23, T38, T14)) → pI_out_ggagaa(T21, T25, T38, T24, X23, T14)
U8_ggaagaaa(T22, T23, T24, T25, T21, X22, X23, T14, pI_out_ggagaa(T21, T25, X22, T24, X23, T14)) → pB_out_ggaagaaa(T22, T23, T24, T25, T21, X22, X23, T14)
U1_ga(T21, T22, T23, T14, pB_out_ggaagaaa(T22, T23, X41, X40, T21, X22, X23, T14)) → mergesortA_out_ga(.(T21, .(T22, T23)), T14)

(15) UsableRulesProof (EQUIVALENT transformation)

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

(16) Obligation:

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

SPLITC_IN_GAA(.(T36, T37), .(T36, X76), X77) → SPLITC_IN_GAA(T37, X77, X76)

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

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

(17) PiDPToQDPProof (SOUND transformation)

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

(18) Obligation:

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

SPLITC_IN_GAA(.(T36, T37)) → SPLITC_IN_GAA(T37)

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

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

SPLITC_IN_GAA(.(T36, T37)) → SPLITC_IN_GAA(T37)
The graph contains the following edges 1 > 1

(20) YES

(21) Obligation:

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

PF_IN_GGGAAAAA(T51, T52, T53, T54, T55, X103, X104, X105) → U13_GGGAAAAA(T51, T52, T53, T54, T55, X103, X104, X105, splitD_in_ggaa(T51, .(T52, T53), T54, T55))
U13_GGGAAAAA(T51, T52, T53, T54, T55, X103, X104, X105, splitD_out_ggaa(T51, .(T52, T53), T54, T55)) → PK_IN_GAGAA(T54, X103, T55, X104, X105)
PK_IN_GAGAA(T54, T56, T55, X104, X105) → U15_GAGAA(T54, T56, T55, X104, X105, mergesortE_in_ga(T54, T56))
U15_GAGAA(T54, T56, T55, X104, X105, mergesortE_out_ga(T54, T56)) → PL_IN_GAGA(T55, X104, T56, X105)
PL_IN_GAGA(T55, T57, T56, X105) → MERGESORTE_IN_GA(T55, T57)
MERGESORTE_IN_GA(.(T51, .(T52, T53)), X105) → PF_IN_GGGAAAAA(T51, T52, T53, X101, X102, X103, X104, X105)
PK_IN_GAGAA(T54, T56, T55, X104, X105) → MERGESORTE_IN_GA(T54, T56)

The TRS R consists of the following rules:

mergesortA_in_ga([], []) → mergesortA_out_ga([], [])
mergesortA_in_ga(.(T4, []), .(T4, [])) → mergesortA_out_ga(.(T4, []), .(T4, []))
mergesortA_in_ga(.(T21, .(T22, T23)), T14) → U1_ga(T21, T22, T23, T14, pB_in_ggaagaaa(T22, T23, X41, X40, T21, X22, X23, T14))
pB_in_ggaagaaa(T22, T23, T24, T25, T21, X22, X23, T14) → U7_ggaagaaa(T22, T23, T24, T25, T21, X22, X23, T14, splitD_in_ggaa(T22, T23, T24, T25))
splitD_in_ggaa(T30, T31, .(T30, X58), X59) → U3_ggaa(T30, T31, X58, X59, splitC_in_gaa(T31, X59, X58))
splitC_in_gaa([], [], []) → splitC_out_gaa([], [], [])
splitC_in_gaa(.(T36, T37), .(T36, X76), X77) → U2_gaa(T36, T37, X76, X77, splitC_in_gaa(T37, X77, X76))
U2_gaa(T36, T37, X76, X77, splitC_out_gaa(T37, X77, X76)) → splitC_out_gaa(.(T36, T37), .(T36, X76), X77)
U3_ggaa(T30, T31, X58, X59, splitC_out_gaa(T31, X59, X58)) → splitD_out_ggaa(T30, T31, .(T30, X58), X59)
U7_ggaagaaa(T22, T23, T24, T25, T21, X22, X23, T14, splitD_out_ggaa(T22, T23, T24, T25)) → U8_ggaagaaa(T22, T23, T24, T25, T21, X22, X23, T14, pI_in_ggagaa(T21, T25, X22, T24, X23, T14))
pI_in_ggagaa(T21, T25, T38, T24, X23, T14) → U9_ggagaa(T21, T25, T38, T24, X23, T14, mergesortA_in_ga(.(T21, T25), T38))
U9_ggagaa(T21, T25, T38, T24, X23, T14, mergesortA_out_ga(.(T21, T25), T38)) → U10_ggagaa(T21, T25, T38, T24, X23, T14, pJ_in_gaga(T24, X23, T38, T14))
pJ_in_gaga(T24, T39, T38, T14) → U11_gaga(T24, T39, T38, T14, mergesortE_in_ga(T24, T39))
mergesortE_in_ga([], []) → mergesortE_out_ga([], [])
mergesortE_in_ga(.(T44, []), .(T44, [])) → mergesortE_out_ga(.(T44, []), .(T44, []))
mergesortE_in_ga(.(T51, .(T52, T53)), X105) → U4_ga(T51, T52, T53, X105, pF_in_gggaaaaa(T51, T52, T53, X101, X102, X103, X104, X105))
pF_in_gggaaaaa(T51, T52, T53, T54, T55, X103, X104, X105) → U13_gggaaaaa(T51, T52, T53, T54, T55, X103, X104, X105, splitD_in_ggaa(T51, .(T52, T53), T54, T55))
U13_gggaaaaa(T51, T52, T53, T54, T55, X103, X104, X105, splitD_out_ggaa(T51, .(T52, T53), T54, T55)) → U14_gggaaaaa(T51, T52, T53, T54, T55, X103, X104, X105, pK_in_gagaa(T54, X103, T55, X104, X105))
pK_in_gagaa(T54, T56, T55, X104, X105) → U15_gagaa(T54, T56, T55, X104, X105, mergesortE_in_ga(T54, T56))
U15_gagaa(T54, T56, T55, X104, X105, mergesortE_out_ga(T54, T56)) → U16_gagaa(T54, T56, T55, X104, X105, pL_in_gaga(T55, X104, T56, X105))
pL_in_gaga(T55, T57, T56, X105) → U17_gaga(T55, T57, T56, X105, mergesortE_in_ga(T55, T57))
U17_gaga(T55, T57, T56, X105, mergesortE_out_ga(T55, T57)) → U18_gaga(T55, T57, T56, X105, mergeH_in_gga(T56, T57, X105))
mergeH_in_gga([], T64, T64) → mergeH_out_gga([], T64, T64)
mergeH_in_gga(T69, [], T69) → mergeH_out_gga(T69, [], T69)
mergeH_in_gga(.(T83, T79), .(T83, T81), .(T83, X135)) → U6_gga(T83, T79, T81, X135, mergeG_in_gga(.(T83, T79), T81, X135))
mergeG_in_gga([], T90, T90) → mergeG_out_gga([], T90, T90)
mergeG_in_gga(T95, [], T95) → mergeG_out_gga(T95, [], T95)
mergeG_in_gga(.(T113, T107), .(T113, T109), .(T113, T111)) → U5_gga(T113, T107, T109, T111, mergeG_in_gga(.(T113, T107), T109, T111))
U5_gga(T113, T107, T109, T111, mergeG_out_gga(.(T113, T107), T109, T111)) → mergeG_out_gga(.(T113, T107), .(T113, T109), .(T113, T111))
U6_gga(T83, T79, T81, X135, mergeG_out_gga(.(T83, T79), T81, X135)) → mergeH_out_gga(.(T83, T79), .(T83, T81), .(T83, X135))
U18_gaga(T55, T57, T56, X105, mergeH_out_gga(T56, T57, X105)) → pL_out_gaga(T55, T57, T56, X105)
U16_gagaa(T54, T56, T55, X104, X105, pL_out_gaga(T55, X104, T56, X105)) → pK_out_gagaa(T54, T56, T55, X104, X105)
U14_gggaaaaa(T51, T52, T53, T54, T55, X103, X104, X105, pK_out_gagaa(T54, X103, T55, X104, X105)) → pF_out_gggaaaaa(T51, T52, T53, T54, T55, X103, X104, X105)
U4_ga(T51, T52, T53, X105, pF_out_gggaaaaa(T51, T52, T53, X101, X102, X103, X104, X105)) → mergesortE_out_ga(.(T51, .(T52, T53)), X105)
U11_gaga(T24, T39, T38, T14, mergesortE_out_ga(T24, T39)) → U12_gaga(T24, T39, T38, T14, mergeG_in_gga(T38, T39, T14))
U12_gaga(T24, T39, T38, T14, mergeG_out_gga(T38, T39, T14)) → pJ_out_gaga(T24, T39, T38, T14)
U10_ggagaa(T21, T25, T38, T24, X23, T14, pJ_out_gaga(T24, X23, T38, T14)) → pI_out_ggagaa(T21, T25, T38, T24, X23, T14)
U8_ggaagaaa(T22, T23, T24, T25, T21, X22, X23, T14, pI_out_ggagaa(T21, T25, X22, T24, X23, T14)) → pB_out_ggaagaaa(T22, T23, T24, T25, T21, X22, X23, T14)
U1_ga(T21, T22, T23, T14, pB_out_ggaagaaa(T22, T23, X41, X40, T21, X22, X23, T14)) → mergesortA_out_ga(.(T21, .(T22, T23)), T14)

(22) UsableRulesProof (EQUIVALENT transformation)

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

(23) Obligation:

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

PF_IN_GGGAAAAA(T51, T52, T53, T54, T55, X103, X104, X105) → U13_GGGAAAAA(T51, T52, T53, T54, T55, X103, X104, X105, splitD_in_ggaa(T51, .(T52, T53), T54, T55))
U13_GGGAAAAA(T51, T52, T53, T54, T55, X103, X104, X105, splitD_out_ggaa(T51, .(T52, T53), T54, T55)) → PK_IN_GAGAA(T54, X103, T55, X104, X105)
PK_IN_GAGAA(T54, T56, T55, X104, X105) → U15_GAGAA(T54, T56, T55, X104, X105, mergesortE_in_ga(T54, T56))
U15_GAGAA(T54, T56, T55, X104, X105, mergesortE_out_ga(T54, T56)) → PL_IN_GAGA(T55, X104, T56, X105)
PL_IN_GAGA(T55, T57, T56, X105) → MERGESORTE_IN_GA(T55, T57)
MERGESORTE_IN_GA(.(T51, .(T52, T53)), X105) → PF_IN_GGGAAAAA(T51, T52, T53, X101, X102, X103, X104, X105)
PK_IN_GAGAA(T54, T56, T55, X104, X105) → MERGESORTE_IN_GA(T54, T56)

The TRS R consists of the following rules:

splitD_in_ggaa(T30, T31, .(T30, X58), X59) → U3_ggaa(T30, T31, X58, X59, splitC_in_gaa(T31, X59, X58))
mergesortE_in_ga([], []) → mergesortE_out_ga([], [])
mergesortE_in_ga(.(T44, []), .(T44, [])) → mergesortE_out_ga(.(T44, []), .(T44, []))
mergesortE_in_ga(.(T51, .(T52, T53)), X105) → U4_ga(T51, T52, T53, X105, pF_in_gggaaaaa(T51, T52, T53, X101, X102, X103, X104, X105))
U3_ggaa(T30, T31, X58, X59, splitC_out_gaa(T31, X59, X58)) → splitD_out_ggaa(T30, T31, .(T30, X58), X59)
U4_ga(T51, T52, T53, X105, pF_out_gggaaaaa(T51, T52, T53, X101, X102, X103, X104, X105)) → mergesortE_out_ga(.(T51, .(T52, T53)), X105)
splitC_in_gaa([], [], []) → splitC_out_gaa([], [], [])
splitC_in_gaa(.(T36, T37), .(T36, X76), X77) → U2_gaa(T36, T37, X76, X77, splitC_in_gaa(T37, X77, X76))
pF_in_gggaaaaa(T51, T52, T53, T54, T55, X103, X104, X105) → U13_gggaaaaa(T51, T52, T53, T54, T55, X103, X104, X105, splitD_in_ggaa(T51, .(T52, T53), T54, T55))
U2_gaa(T36, T37, X76, X77, splitC_out_gaa(T37, X77, X76)) → splitC_out_gaa(.(T36, T37), .(T36, X76), X77)
U13_gggaaaaa(T51, T52, T53, T54, T55, X103, X104, X105, splitD_out_ggaa(T51, .(T52, T53), T54, T55)) → U14_gggaaaaa(T51, T52, T53, T54, T55, X103, X104, X105, pK_in_gagaa(T54, X103, T55, X104, X105))
U14_gggaaaaa(T51, T52, T53, T54, T55, X103, X104, X105, pK_out_gagaa(T54, X103, T55, X104, X105)) → pF_out_gggaaaaa(T51, T52, T53, T54, T55, X103, X104, X105)
pK_in_gagaa(T54, T56, T55, X104, X105) → U15_gagaa(T54, T56, T55, X104, X105, mergesortE_in_ga(T54, T56))
U15_gagaa(T54, T56, T55, X104, X105, mergesortE_out_ga(T54, T56)) → U16_gagaa(T54, T56, T55, X104, X105, pL_in_gaga(T55, X104, T56, X105))
U16_gagaa(T54, T56, T55, X104, X105, pL_out_gaga(T55, X104, T56, X105)) → pK_out_gagaa(T54, T56, T55, X104, X105)
pL_in_gaga(T55, T57, T56, X105) → U17_gaga(T55, T57, T56, X105, mergesortE_in_ga(T55, T57))
U17_gaga(T55, T57, T56, X105, mergesortE_out_ga(T55, T57)) → U18_gaga(T55, T57, T56, X105, mergeH_in_gga(T56, T57, X105))
U18_gaga(T55, T57, T56, X105, mergeH_out_gga(T56, T57, X105)) → pL_out_gaga(T55, T57, T56, X105)
mergeH_in_gga([], T64, T64) → mergeH_out_gga([], T64, T64)
mergeH_in_gga(T69, [], T69) → mergeH_out_gga(T69, [], T69)
mergeH_in_gga(.(T83, T79), .(T83, T81), .(T83, X135)) → U6_gga(T83, T79, T81, X135, mergeG_in_gga(.(T83, T79), T81, X135))
U6_gga(T83, T79, T81, X135, mergeG_out_gga(.(T83, T79), T81, X135)) → mergeH_out_gga(.(T83, T79), .(T83, T81), .(T83, X135))
mergeG_in_gga(T95, [], T95) → mergeG_out_gga(T95, [], T95)
mergeG_in_gga(.(T113, T107), .(T113, T109), .(T113, T111)) → U5_gga(T113, T107, T109, T111, mergeG_in_gga(.(T113, T107), T109, T111))
U5_gga(T113, T107, T109, T111, mergeG_out_gga(.(T113, T107), T109, T111)) → mergeG_out_gga(.(T113, T107), .(T113, T109), .(T113, T111))

The argument filtering Pi contains the following mapping:
[] = []
.(x1, x2) = .(x1, x2)
splitD_in_ggaa(x1, x2, x3, x4) = splitD_in_ggaa(x1, x2)
U3_ggaa(x1, x2, x3, x4, x5) = U3_ggaa(x1, x2, x5)
splitC_in_gaa(x1, x2, x3) = splitC_in_gaa(x1)
splitC_out_gaa(x1, x2, x3) = splitC_out_gaa(x1, x2, x3)
U2_gaa(x1, x2, x3, x4, x5) = U2_gaa(x1, x2, x5)
splitD_out_ggaa(x1, x2, x3, x4) = splitD_out_ggaa(x1, x2, x3, x4)
mergesortE_in_ga(x1, x2) = mergesortE_in_ga(x1)
mergesortE_out_ga(x1, x2) = mergesortE_out_ga(x1, x2)
U4_ga(x1, x2, x3, x4, x5) = U4_ga(x1, x2, x3, x5)
pF_in_gggaaaaa(x1, x2, x3, x4, x5, x6, x7, x8) = pF_in_gggaaaaa(x1, x2, x3)
U13_gggaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9) = U13_gggaaaaa(x1, x2, x3, x9)
U14_gggaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9) = U14_gggaaaaa(x1, x2, x3, x4, x5, x9)
pK_in_gagaa(x1, x2, x3, x4, x5) = pK_in_gagaa(x1, x3)
U15_gagaa(x1, x2, x3, x4, x5, x6) = U15_gagaa(x1, x3, x6)
U16_gagaa(x1, x2, x3, x4, x5, x6) = U16_gagaa(x1, x2, x3, x6)
pL_in_gaga(x1, x2, x3, x4) = pL_in_gaga(x1, x3)
U17_gaga(x1, x2, x3, x4, x5) = U17_gaga(x1, x3, x5)
U18_gaga(x1, x2, x3, x4, x5) = U18_gaga(x1, x2, x3, x5)
mergeH_in_gga(x1, x2, x3) = mergeH_in_gga(x1, x2)
mergeH_out_gga(x1, x2, x3) = mergeH_out_gga(x1, x2, x3)
U6_gga(x1, x2, x3, x4, x5) = U6_gga(x1, x2, x3, x5)
mergeG_in_gga(x1, x2, x3) = mergeG_in_gga(x1, x2)
mergeG_out_gga(x1, x2, x3) = mergeG_out_gga(x1, x2, x3)
U5_gga(x1, x2, x3, x4, x5) = U5_gga(x1, x2, x3, x5)
pL_out_gaga(x1, x2, x3, x4) = pL_out_gaga(x1, x2, x3, x4)
pK_out_gagaa(x1, x2, x3, x4, x5) = pK_out_gagaa(x1, x2, x3, x4, x5)
pF_out_gggaaaaa(x1, x2, x3, x4, x5, x6, x7, x8) = pF_out_gggaaaaa(x1, x2, x3, x4, x5, x6, x7, x8)
MERGESORTE_IN_GA(x1, x2) = MERGESORTE_IN_GA(x1)
PF_IN_GGGAAAAA(x1, x2, x3, x4, x5, x6, x7, x8) = PF_IN_GGGAAAAA(x1, x2, x3)
U13_GGGAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9) = U13_GGGAAAAA(x1, x2, x3, x9)
PK_IN_GAGAA(x1, x2, x3, x4, x5) = PK_IN_GAGAA(x1, x3)
U15_GAGAA(x1, x2, x3, x4, x5, x6) = U15_GAGAA(x1, x3, x6)
PL_IN_GAGA(x1, x2, x3, x4) = PL_IN_GAGA(x1, x3)

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

(24) PiDPToQDPProof (SOUND transformation)

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

(25) Obligation:

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

PF_IN_GGGAAAAA(T51, T52, T53) → U13_GGGAAAAA(T51, T52, T53, splitD_in_ggaa(T51, .(T52, T53)))
U13_GGGAAAAA(T51, T52, T53, splitD_out_ggaa(T51, .(T52, T53), T54, T55)) → PK_IN_GAGAA(T54, T55)
PK_IN_GAGAA(T54, T55) → U15_GAGAA(T54, T55, mergesortE_in_ga(T54))
U15_GAGAA(T54, T55, mergesortE_out_ga(T54, T56)) → PL_IN_GAGA(T55, T56)
PL_IN_GAGA(T55, T56) → MERGESORTE_IN_GA(T55)
MERGESORTE_IN_GA(.(T51, .(T52, T53))) → PF_IN_GGGAAAAA(T51, T52, T53)
PK_IN_GAGAA(T54, T55) → MERGESORTE_IN_GA(T54)

The TRS R consists of the following rules:

splitD_in_ggaa(T30, T31) → U3_ggaa(T30, T31, splitC_in_gaa(T31))
mergesortE_in_ga([]) → mergesortE_out_ga([], [])
mergesortE_in_ga(.(T44, [])) → mergesortE_out_ga(.(T44, []), .(T44, []))
mergesortE_in_ga(.(T51, .(T52, T53))) → U4_ga(T51, T52, T53, pF_in_gggaaaaa(T51, T52, T53))
U3_ggaa(T30, T31, splitC_out_gaa(T31, X59, X58)) → splitD_out_ggaa(T30, T31, .(T30, X58), X59)
U4_ga(T51, T52, T53, pF_out_gggaaaaa(T51, T52, T53, X101, X102, X103, X104, X105)) → mergesortE_out_ga(.(T51, .(T52, T53)), X105)
splitC_in_gaa([]) → splitC_out_gaa([], [], [])
splitC_in_gaa(.(T36, T37)) → U2_gaa(T36, T37, splitC_in_gaa(T37))
pF_in_gggaaaaa(T51, T52, T53) → U13_gggaaaaa(T51, T52, T53, splitD_in_ggaa(T51, .(T52, T53)))
U2_gaa(T36, T37, splitC_out_gaa(T37, X77, X76)) → splitC_out_gaa(.(T36, T37), .(T36, X76), X77)
U13_gggaaaaa(T51, T52, T53, splitD_out_ggaa(T51, .(T52, T53), T54, T55)) → U14_gggaaaaa(T51, T52, T53, T54, T55, pK_in_gagaa(T54, T55))
U14_gggaaaaa(T51, T52, T53, T54, T55, pK_out_gagaa(T54, X103, T55, X104, X105)) → pF_out_gggaaaaa(T51, T52, T53, T54, T55, X103, X104, X105)
pK_in_gagaa(T54, T55) → U15_gagaa(T54, T55, mergesortE_in_ga(T54))
U15_gagaa(T54, T55, mergesortE_out_ga(T54, T56)) → U16_gagaa(T54, T56, T55, pL_in_gaga(T55, T56))
U16_gagaa(T54, T56, T55, pL_out_gaga(T55, X104, T56, X105)) → pK_out_gagaa(T54, T56, T55, X104, X105)
pL_in_gaga(T55, T56) → U17_gaga(T55, T56, mergesortE_in_ga(T55))
U17_gaga(T55, T56, mergesortE_out_ga(T55, T57)) → U18_gaga(T55, T57, T56, mergeH_in_gga(T56, T57))
U18_gaga(T55, T57, T56, mergeH_out_gga(T56, T57, X105)) → pL_out_gaga(T55, T57, T56, X105)
mergeH_in_gga([], T64) → mergeH_out_gga([], T64, T64)
mergeH_in_gga(T69, []) → mergeH_out_gga(T69, [], T69)
mergeH_in_gga(.(T83, T79), .(T83, T81)) → U6_gga(T83, T79, T81, mergeG_in_gga(.(T83, T79), T81))
U6_gga(T83, T79, T81, mergeG_out_gga(.(T83, T79), T81, X135)) → mergeH_out_gga(.(T83, T79), .(T83, T81), .(T83, X135))
mergeG_in_gga(T95, []) → mergeG_out_gga(T95, [], T95)
mergeG_in_gga(.(T113, T107), .(T113, T109)) → U5_gga(T113, T107, T109, mergeG_in_gga(.(T113, T107), T109))
U5_gga(T113, T107, T109, mergeG_out_gga(.(T113, T107), T109, T111)) → mergeG_out_gga(.(T113, T107), .(T113, T109), .(T113, T111))

The set Q consists of the following terms:

splitD_in_ggaa(x0, x1)
mergesortE_in_ga(x0)
U3_ggaa(x0, x1, x2)
U4_ga(x0, x1, x2, x3)
splitC_in_gaa(x0)
pF_in_gggaaaaa(x0, x1, x2)
U2_gaa(x0, x1, x2)
U13_gggaaaaa(x0, x1, x2, x3)
U14_gggaaaaa(x0, x1, x2, x3, x4, x5)
pK_in_gagaa(x0, x1)
U15_gagaa(x0, x1, x2)
U16_gagaa(x0, x1, x2, x3)
pL_in_gaga(x0, x1)
U17_gaga(x0, x1, x2)
U18_gaga(x0, x1, x2, x3)
mergeH_in_gga(x0, x1)
U6_gga(x0, x1, x2, x3)
mergeG_in_gga(x0, x1)
U5_gga(x0, x1, x2, x3)

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

(26) Rewriting (EQUIVALENT transformation)

By rewriting [LPAR04] the rule PF_IN_GGGAAAAA(T51, T52, T53) → U13_GGGAAAAA(T51, T52, T53, splitD_in_ggaa(T51, .(T52, T53))) at position [3] we obtained the following new rules [LPAR04]:

PF_IN_GGGAAAAA(T51, T52, T53) → U13_GGGAAAAA(T51, T52, T53, U3_ggaa(T51, .(T52, T53), splitC_in_gaa(.(T52, T53))))

(27) Obligation:

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

U13_GGGAAAAA(T51, T52, T53, splitD_out_ggaa(T51, .(T52, T53), T54, T55)) → PK_IN_GAGAA(T54, T55)
PK_IN_GAGAA(T54, T55) → U15_GAGAA(T54, T55, mergesortE_in_ga(T54))
U15_GAGAA(T54, T55, mergesortE_out_ga(T54, T56)) → PL_IN_GAGA(T55, T56)
PL_IN_GAGA(T55, T56) → MERGESORTE_IN_GA(T55)
MERGESORTE_IN_GA(.(T51, .(T52, T53))) → PF_IN_GGGAAAAA(T51, T52, T53)
PK_IN_GAGAA(T54, T55) → MERGESORTE_IN_GA(T54)
PF_IN_GGGAAAAA(T51, T52, T53) → U13_GGGAAAAA(T51, T52, T53, U3_ggaa(T51, .(T52, T53), splitC_in_gaa(.(T52, T53))))

The TRS R consists of the following rules:

splitD_in_ggaa(T30, T31) → U3_ggaa(T30, T31, splitC_in_gaa(T31))
mergesortE_in_ga([]) → mergesortE_out_ga([], [])
mergesortE_in_ga(.(T44, [])) → mergesortE_out_ga(.(T44, []), .(T44, []))
mergesortE_in_ga(.(T51, .(T52, T53))) → U4_ga(T51, T52, T53, pF_in_gggaaaaa(T51, T52, T53))
U3_ggaa(T30, T31, splitC_out_gaa(T31, X59, X58)) → splitD_out_ggaa(T30, T31, .(T30, X58), X59)
U4_ga(T51, T52, T53, pF_out_gggaaaaa(T51, T52, T53, X101, X102, X103, X104, X105)) → mergesortE_out_ga(.(T51, .(T52, T53)), X105)
splitC_in_gaa([]) → splitC_out_gaa([], [], [])
splitC_in_gaa(.(T36, T37)) → U2_gaa(T36, T37, splitC_in_gaa(T37))
pF_in_gggaaaaa(T51, T52, T53) → U13_gggaaaaa(T51, T52, T53, splitD_in_ggaa(T51, .(T52, T53)))
U2_gaa(T36, T37, splitC_out_gaa(T37, X77, X76)) → splitC_out_gaa(.(T36, T37), .(T36, X76), X77)
U13_gggaaaaa(T51, T52, T53, splitD_out_ggaa(T51, .(T52, T53), T54, T55)) → U14_gggaaaaa(T51, T52, T53, T54, T55, pK_in_gagaa(T54, T55))
U14_gggaaaaa(T51, T52, T53, T54, T55, pK_out_gagaa(T54, X103, T55, X104, X105)) → pF_out_gggaaaaa(T51, T52, T53, T54, T55, X103, X104, X105)
pK_in_gagaa(T54, T55) → U15_gagaa(T54, T55, mergesortE_in_ga(T54))
U15_gagaa(T54, T55, mergesortE_out_ga(T54, T56)) → U16_gagaa(T54, T56, T55, pL_in_gaga(T55, T56))
U16_gagaa(T54, T56, T55, pL_out_gaga(T55, X104, T56, X105)) → pK_out_gagaa(T54, T56, T55, X104, X105)
pL_in_gaga(T55, T56) → U17_gaga(T55, T56, mergesortE_in_ga(T55))
U17_gaga(T55, T56, mergesortE_out_ga(T55, T57)) → U18_gaga(T55, T57, T56, mergeH_in_gga(T56, T57))
U18_gaga(T55, T57, T56, mergeH_out_gga(T56, T57, X105)) → pL_out_gaga(T55, T57, T56, X105)
mergeH_in_gga([], T64) → mergeH_out_gga([], T64, T64)
mergeH_in_gga(T69, []) → mergeH_out_gga(T69, [], T69)
mergeH_in_gga(.(T83, T79), .(T83, T81)) → U6_gga(T83, T79, T81, mergeG_in_gga(.(T83, T79), T81))
U6_gga(T83, T79, T81, mergeG_out_gga(.(T83, T79), T81, X135)) → mergeH_out_gga(.(T83, T79), .(T83, T81), .(T83, X135))
mergeG_in_gga(T95, []) → mergeG_out_gga(T95, [], T95)
mergeG_in_gga(.(T113, T107), .(T113, T109)) → U5_gga(T113, T107, T109, mergeG_in_gga(.(T113, T107), T109))
U5_gga(T113, T107, T109, mergeG_out_gga(.(T113, T107), T109, T111)) → mergeG_out_gga(.(T113, T107), .(T113, T109), .(T113, T111))

The set Q consists of the following terms:

splitD_in_ggaa(x0, x1)
mergesortE_in_ga(x0)
U3_ggaa(x0, x1, x2)
U4_ga(x0, x1, x2, x3)
splitC_in_gaa(x0)
pF_in_gggaaaaa(x0, x1, x2)
U2_gaa(x0, x1, x2)
U13_gggaaaaa(x0, x1, x2, x3)
U14_gggaaaaa(x0, x1, x2, x3, x4, x5)
pK_in_gagaa(x0, x1)
U15_gagaa(x0, x1, x2)
U16_gagaa(x0, x1, x2, x3)
pL_in_gaga(x0, x1)
U17_gaga(x0, x1, x2)
U18_gaga(x0, x1, x2, x3)
mergeH_in_gga(x0, x1)
U6_gga(x0, x1, x2, x3)
mergeG_in_gga(x0, x1)
U5_gga(x0, x1, x2, x3)

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

(28) Rewriting (EQUIVALENT transformation)

By rewriting [LPAR04] the rule PF_IN_GGGAAAAA(T51, T52, T53) → U13_GGGAAAAA(T51, T52, T53, U3_ggaa(T51, .(T52, T53), splitC_in_gaa(.(T52, T53)))) at position [3,2] we obtained the following new rules [LPAR04]:

PF_IN_GGGAAAAA(T51, T52, T53) → U13_GGGAAAAA(T51, T52, T53, U3_ggaa(T51, .(T52, T53), U2_gaa(T52, T53, splitC_in_gaa(T53))))

(29) Obligation:

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

U13_GGGAAAAA(T51, T52, T53, splitD_out_ggaa(T51, .(T52, T53), T54, T55)) → PK_IN_GAGAA(T54, T55)
PK_IN_GAGAA(T54, T55) → U15_GAGAA(T54, T55, mergesortE_in_ga(T54))
U15_GAGAA(T54, T55, mergesortE_out_ga(T54, T56)) → PL_IN_GAGA(T55, T56)
PL_IN_GAGA(T55, T56) → MERGESORTE_IN_GA(T55)
MERGESORTE_IN_GA(.(T51, .(T52, T53))) → PF_IN_GGGAAAAA(T51, T52, T53)
PK_IN_GAGAA(T54, T55) → MERGESORTE_IN_GA(T54)
PF_IN_GGGAAAAA(T51, T52, T53) → U13_GGGAAAAA(T51, T52, T53, U3_ggaa(T51, .(T52, T53), U2_gaa(T52, T53, splitC_in_gaa(T53))))

The TRS R consists of the following rules:

splitD_in_ggaa(T30, T31) → U3_ggaa(T30, T31, splitC_in_gaa(T31))
mergesortE_in_ga([]) → mergesortE_out_ga([], [])
mergesortE_in_ga(.(T44, [])) → mergesortE_out_ga(.(T44, []), .(T44, []))
mergesortE_in_ga(.(T51, .(T52, T53))) → U4_ga(T51, T52, T53, pF_in_gggaaaaa(T51, T52, T53))
U3_ggaa(T30, T31, splitC_out_gaa(T31, X59, X58)) → splitD_out_ggaa(T30, T31, .(T30, X58), X59)
U4_ga(T51, T52, T53, pF_out_gggaaaaa(T51, T52, T53, X101, X102, X103, X104, X105)) → mergesortE_out_ga(.(T51, .(T52, T53)), X105)
splitC_in_gaa([]) → splitC_out_gaa([], [], [])
splitC_in_gaa(.(T36, T37)) → U2_gaa(T36, T37, splitC_in_gaa(T37))
pF_in_gggaaaaa(T51, T52, T53) → U13_gggaaaaa(T51, T52, T53, splitD_in_ggaa(T51, .(T52, T53)))
U2_gaa(T36, T37, splitC_out_gaa(T37, X77, X76)) → splitC_out_gaa(.(T36, T37), .(T36, X76), X77)
U13_gggaaaaa(T51, T52, T53, splitD_out_ggaa(T51, .(T52, T53), T54, T55)) → U14_gggaaaaa(T51, T52, T53, T54, T55, pK_in_gagaa(T54, T55))
U14_gggaaaaa(T51, T52, T53, T54, T55, pK_out_gagaa(T54, X103, T55, X104, X105)) → pF_out_gggaaaaa(T51, T52, T53, T54, T55, X103, X104, X105)
pK_in_gagaa(T54, T55) → U15_gagaa(T54, T55, mergesortE_in_ga(T54))
U15_gagaa(T54, T55, mergesortE_out_ga(T54, T56)) → U16_gagaa(T54, T56, T55, pL_in_gaga(T55, T56))
U16_gagaa(T54, T56, T55, pL_out_gaga(T55, X104, T56, X105)) → pK_out_gagaa(T54, T56, T55, X104, X105)
pL_in_gaga(T55, T56) → U17_gaga(T55, T56, mergesortE_in_ga(T55))
U17_gaga(T55, T56, mergesortE_out_ga(T55, T57)) → U18_gaga(T55, T57, T56, mergeH_in_gga(T56, T57))
U18_gaga(T55, T57, T56, mergeH_out_gga(T56, T57, X105)) → pL_out_gaga(T55, T57, T56, X105)
mergeH_in_gga([], T64) → mergeH_out_gga([], T64, T64)
mergeH_in_gga(T69, []) → mergeH_out_gga(T69, [], T69)
mergeH_in_gga(.(T83, T79), .(T83, T81)) → U6_gga(T83, T79, T81, mergeG_in_gga(.(T83, T79), T81))
U6_gga(T83, T79, T81, mergeG_out_gga(.(T83, T79), T81, X135)) → mergeH_out_gga(.(T83, T79), .(T83, T81), .(T83, X135))
mergeG_in_gga(T95, []) → mergeG_out_gga(T95, [], T95)
mergeG_in_gga(.(T113, T107), .(T113, T109)) → U5_gga(T113, T107, T109, mergeG_in_gga(.(T113, T107), T109))
U5_gga(T113, T107, T109, mergeG_out_gga(.(T113, T107), T109, T111)) → mergeG_out_gga(.(T113, T107), .(T113, T109), .(T113, T111))

The set Q consists of the following terms:

splitD_in_ggaa(x0, x1)
mergesortE_in_ga(x0)
U3_ggaa(x0, x1, x2)
U4_ga(x0, x1, x2, x3)
splitC_in_gaa(x0)
pF_in_gggaaaaa(x0, x1, x2)
U2_gaa(x0, x1, x2)
U13_gggaaaaa(x0, x1, x2, x3)
U14_gggaaaaa(x0, x1, x2, x3, x4, x5)
pK_in_gagaa(x0, x1)
U15_gagaa(x0, x1, x2)
U16_gagaa(x0, x1, x2, x3)
pL_in_gaga(x0, x1)
U17_gaga(x0, x1, x2)
U18_gaga(x0, x1, x2, x3)
mergeH_in_gga(x0, x1)
U6_gga(x0, x1, x2, x3)
mergeG_in_gga(x0, x1)
U5_gga(x0, x1, x2, x3)

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

(30) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04,JAR06].

The following pairs can be oriented strictly and are deleted.

MERGESORTE_IN_GA(.(T51, .(T52, T53))) → PF_IN_GGGAAAAA(T51, T52, T53)

The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial Order [NEGPOLO,POLO] with Interpretation:

POL( U15_GAGAA(x₁, ..., x₃) ) = x₂

POL( mergesortE_in_ga(x₁) ) = 0

POL( [] ) = 0

POL( mergesortE_out_ga(x₁, x₂) ) = max{0, 2x₁ + x₂ - 2}

POL( .(x₁, x₂) ) = x₁ + 2x₂ + 1

POL( U4_ga(x₁, ..., x₄) ) = 2x₁ + x₂

POL( pF_in_gggaaaaa(x₁, ..., x₃) ) = 2x₁ + 2x₂ + x₃ + 1

POL( U13_GGGAAAAA(x₁, ..., x₄) ) = x₄ + 1

POL( U2_gaa(x₁, ..., x₃) ) = max{0, x₁ + 2x₃ - 1}

POL( U3_ggaa(x₁, ..., x₃) ) = max{0, x₁ + x₃ - 2}

POL( U13_gggaaaaa(x₁, ..., x₄) ) = x₂ + x₃ + 1

POL( splitC_in_gaa(x₁) ) = x₁ + 2

POL( splitC_out_gaa(x₁, ..., x₃) ) = x₂ + 2x₃ + 2

POL( splitD_out_ggaa(x₁, ..., x₄) ) = max{0, x₃ + x₄ - 1}

POL( U14_gggaaaaa(x₁, ..., x₆) ) = x₁ + 2x₂ + 2x₄ + x₅

POL( pK_in_gagaa(x₁, x₂) ) = 2x₂ + 2

POL( pK_out_gagaa(x₁, ..., x₅) ) = 2x₁ + x₃ + x₄ + x₅ + 1

POL( pF_out_gggaaaaa(x₁, ..., x₈) ) = 2x₁ + 2x₂ + 2x₃ + x₄ + 2x₅ + x₆ + 2x₇ + 2x₈ + 2

POL( U15_gagaa(x₁, ..., x₃) ) = x₁ + 2

POL( splitD_in_ggaa(x₁, x₂) ) = x₂ + 2

POL( U16_gagaa(x₁, ..., x₄) ) = max{0, 2x₄ - 1}

POL( pL_in_gaga(x₁, x₂) ) = 2x₁ + x₂ + 1

POL( pL_out_gaga(x₁, ..., x₄) ) = 0

POL( U17_gaga(x₁, ..., x₃) ) = max{0, x₁ + 2x₂ - 1}

POL( U18_gaga(x₁, ..., x₄) ) = max{0, -1}

POL( mergeH_in_gga(x₁, x₂) ) = 1

POL( mergeH_out_gga(x₁, ..., x₃) ) = x₂ + 2

POL( U6_gga(x₁, ..., x₄) ) = x₁ + x₂ + 2x₃ + 2

POL( mergeG_in_gga(x₁, x₂) ) = max{0, -2}

POL( mergeG_out_gga(x₁, ..., x₃) ) = 2x₃ + 1

POL( U5_gga(x₁, ..., x₄) ) = 2x₁ + 2x₃ + 2

POL( PK_IN_GAGAA(x₁, x₂) ) = x₁ + x₂

POL( PL_IN_GAGA(x₁, x₂) ) = x₁

POL( MERGESORTE_IN_GA(x₁) ) = x₁

POL( PF_IN_GGGAAAAA(x₁, ..., x₃) ) = x₁ + 2x₂ + 2x₃ + 2

The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:

splitC_in_gaa([]) → splitC_out_gaa([], [], [])
splitC_in_gaa(.(T36, T37)) → U2_gaa(T36, T37, splitC_in_gaa(T37))
U2_gaa(T36, T37, splitC_out_gaa(T37, X77, X76)) → splitC_out_gaa(.(T36, T37), .(T36, X76), X77)
U3_ggaa(T30, T31, splitC_out_gaa(T31, X59, X58)) → splitD_out_ggaa(T30, T31, .(T30, X58), X59)

(31) Obligation:

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

U13_GGGAAAAA(T51, T52, T53, splitD_out_ggaa(T51, .(T52, T53), T54, T55)) → PK_IN_GAGAA(T54, T55)
PK_IN_GAGAA(T54, T55) → U15_GAGAA(T54, T55, mergesortE_in_ga(T54))
U15_GAGAA(T54, T55, mergesortE_out_ga(T54, T56)) → PL_IN_GAGA(T55, T56)
PL_IN_GAGA(T55, T56) → MERGESORTE_IN_GA(T55)
PK_IN_GAGAA(T54, T55) → MERGESORTE_IN_GA(T54)
PF_IN_GGGAAAAA(T51, T52, T53) → U13_GGGAAAAA(T51, T52, T53, U3_ggaa(T51, .(T52, T53), U2_gaa(T52, T53, splitC_in_gaa(T53))))

The TRS R consists of the following rules:

splitD_in_ggaa(T30, T31) → U3_ggaa(T30, T31, splitC_in_gaa(T31))
mergesortE_in_ga([]) → mergesortE_out_ga([], [])
mergesortE_in_ga(.(T44, [])) → mergesortE_out_ga(.(T44, []), .(T44, []))
mergesortE_in_ga(.(T51, .(T52, T53))) → U4_ga(T51, T52, T53, pF_in_gggaaaaa(T51, T52, T53))
U3_ggaa(T30, T31, splitC_out_gaa(T31, X59, X58)) → splitD_out_ggaa(T30, T31, .(T30, X58), X59)
U4_ga(T51, T52, T53, pF_out_gggaaaaa(T51, T52, T53, X101, X102, X103, X104, X105)) → mergesortE_out_ga(.(T51, .(T52, T53)), X105)
splitC_in_gaa([]) → splitC_out_gaa([], [], [])
splitC_in_gaa(.(T36, T37)) → U2_gaa(T36, T37, splitC_in_gaa(T37))
pF_in_gggaaaaa(T51, T52, T53) → U13_gggaaaaa(T51, T52, T53, splitD_in_ggaa(T51, .(T52, T53)))
U2_gaa(T36, T37, splitC_out_gaa(T37, X77, X76)) → splitC_out_gaa(.(T36, T37), .(T36, X76), X77)
U13_gggaaaaa(T51, T52, T53, splitD_out_ggaa(T51, .(T52, T53), T54, T55)) → U14_gggaaaaa(T51, T52, T53, T54, T55, pK_in_gagaa(T54, T55))
U14_gggaaaaa(T51, T52, T53, T54, T55, pK_out_gagaa(T54, X103, T55, X104, X105)) → pF_out_gggaaaaa(T51, T52, T53, T54, T55, X103, X104, X105)
pK_in_gagaa(T54, T55) → U15_gagaa(T54, T55, mergesortE_in_ga(T54))
U15_gagaa(T54, T55, mergesortE_out_ga(T54, T56)) → U16_gagaa(T54, T56, T55, pL_in_gaga(T55, T56))
U16_gagaa(T54, T56, T55, pL_out_gaga(T55, X104, T56, X105)) → pK_out_gagaa(T54, T56, T55, X104, X105)
pL_in_gaga(T55, T56) → U17_gaga(T55, T56, mergesortE_in_ga(T55))
U17_gaga(T55, T56, mergesortE_out_ga(T55, T57)) → U18_gaga(T55, T57, T56, mergeH_in_gga(T56, T57))
U18_gaga(T55, T57, T56, mergeH_out_gga(T56, T57, X105)) → pL_out_gaga(T55, T57, T56, X105)
mergeH_in_gga([], T64) → mergeH_out_gga([], T64, T64)
mergeH_in_gga(T69, []) → mergeH_out_gga(T69, [], T69)
mergeH_in_gga(.(T83, T79), .(T83, T81)) → U6_gga(T83, T79, T81, mergeG_in_gga(.(T83, T79), T81))
U6_gga(T83, T79, T81, mergeG_out_gga(.(T83, T79), T81, X135)) → mergeH_out_gga(.(T83, T79), .(T83, T81), .(T83, X135))
mergeG_in_gga(T95, []) → mergeG_out_gga(T95, [], T95)
mergeG_in_gga(.(T113, T107), .(T113, T109)) → U5_gga(T113, T107, T109, mergeG_in_gga(.(T113, T107), T109))
U5_gga(T113, T107, T109, mergeG_out_gga(.(T113, T107), T109, T111)) → mergeG_out_gga(.(T113, T107), .(T113, T109), .(T113, T111))

The set Q consists of the following terms:

splitD_in_ggaa(x0, x1)
mergesortE_in_ga(x0)
U3_ggaa(x0, x1, x2)
U4_ga(x0, x1, x2, x3)
splitC_in_gaa(x0)
pF_in_gggaaaaa(x0, x1, x2)
U2_gaa(x0, x1, x2)
U13_gggaaaaa(x0, x1, x2, x3)
U14_gggaaaaa(x0, x1, x2, x3, x4, x5)
pK_in_gagaa(x0, x1)
U15_gagaa(x0, x1, x2)
U16_gagaa(x0, x1, x2, x3)
pL_in_gaga(x0, x1)
U17_gaga(x0, x1, x2)
U18_gaga(x0, x1, x2, x3)
mergeH_in_gga(x0, x1)
U6_gga(x0, x1, x2, x3)
mergeG_in_gga(x0, x1)
U5_gga(x0, x1, x2, x3)

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

(32) DependencyGraphProof (EQUIVALENT transformation)

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

(33) TRUE

(34) Obligation:

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

MERGESORTA_IN_GA(.(T21, .(T22, T23)), T14) → PB_IN_GGAAGAAA(T22, T23, X41, X40, T21, X22, X23, T14)
PB_IN_GGAAGAAA(T22, T23, T24, T25, T21, X22, X23, T14) → U7_GGAAGAAA(T22, T23, T24, T25, T21, X22, X23, T14, splitD_in_ggaa(T22, T23, T24, T25))
U7_GGAAGAAA(T22, T23, T24, T25, T21, X22, X23, T14, splitD_out_ggaa(T22, T23, T24, T25)) → PI_IN_GGAGAA(T21, T25, X22, T24, X23, T14)
PI_IN_GGAGAA(T21, T25, T38, T24, X23, T14) → MERGESORTA_IN_GA(.(T21, T25), T38)

The TRS R consists of the following rules:

mergesortA_in_ga([], []) → mergesortA_out_ga([], [])
mergesortA_in_ga(.(T4, []), .(T4, [])) → mergesortA_out_ga(.(T4, []), .(T4, []))
mergesortA_in_ga(.(T21, .(T22, T23)), T14) → U1_ga(T21, T22, T23, T14, pB_in_ggaagaaa(T22, T23, X41, X40, T21, X22, X23, T14))
pB_in_ggaagaaa(T22, T23, T24, T25, T21, X22, X23, T14) → U7_ggaagaaa(T22, T23, T24, T25, T21, X22, X23, T14, splitD_in_ggaa(T22, T23, T24, T25))
splitD_in_ggaa(T30, T31, .(T30, X58), X59) → U3_ggaa(T30, T31, X58, X59, splitC_in_gaa(T31, X59, X58))
splitC_in_gaa([], [], []) → splitC_out_gaa([], [], [])
splitC_in_gaa(.(T36, T37), .(T36, X76), X77) → U2_gaa(T36, T37, X76, X77, splitC_in_gaa(T37, X77, X76))
U2_gaa(T36, T37, X76, X77, splitC_out_gaa(T37, X77, X76)) → splitC_out_gaa(.(T36, T37), .(T36, X76), X77)
U3_ggaa(T30, T31, X58, X59, splitC_out_gaa(T31, X59, X58)) → splitD_out_ggaa(T30, T31, .(T30, X58), X59)
U7_ggaagaaa(T22, T23, T24, T25, T21, X22, X23, T14, splitD_out_ggaa(T22, T23, T24, T25)) → U8_ggaagaaa(T22, T23, T24, T25, T21, X22, X23, T14, pI_in_ggagaa(T21, T25, X22, T24, X23, T14))
pI_in_ggagaa(T21, T25, T38, T24, X23, T14) → U9_ggagaa(T21, T25, T38, T24, X23, T14, mergesortA_in_ga(.(T21, T25), T38))
U9_ggagaa(T21, T25, T38, T24, X23, T14, mergesortA_out_ga(.(T21, T25), T38)) → U10_ggagaa(T21, T25, T38, T24, X23, T14, pJ_in_gaga(T24, X23, T38, T14))
pJ_in_gaga(T24, T39, T38, T14) → U11_gaga(T24, T39, T38, T14, mergesortE_in_ga(T24, T39))
mergesortE_in_ga([], []) → mergesortE_out_ga([], [])
mergesortE_in_ga(.(T44, []), .(T44, [])) → mergesortE_out_ga(.(T44, []), .(T44, []))
mergesortE_in_ga(.(T51, .(T52, T53)), X105) → U4_ga(T51, T52, T53, X105, pF_in_gggaaaaa(T51, T52, T53, X101, X102, X103, X104, X105))
pF_in_gggaaaaa(T51, T52, T53, T54, T55, X103, X104, X105) → U13_gggaaaaa(T51, T52, T53, T54, T55, X103, X104, X105, splitD_in_ggaa(T51, .(T52, T53), T54, T55))
U13_gggaaaaa(T51, T52, T53, T54, T55, X103, X104, X105, splitD_out_ggaa(T51, .(T52, T53), T54, T55)) → U14_gggaaaaa(T51, T52, T53, T54, T55, X103, X104, X105, pK_in_gagaa(T54, X103, T55, X104, X105))
pK_in_gagaa(T54, T56, T55, X104, X105) → U15_gagaa(T54, T56, T55, X104, X105, mergesortE_in_ga(T54, T56))
U15_gagaa(T54, T56, T55, X104, X105, mergesortE_out_ga(T54, T56)) → U16_gagaa(T54, T56, T55, X104, X105, pL_in_gaga(T55, X104, T56, X105))
pL_in_gaga(T55, T57, T56, X105) → U17_gaga(T55, T57, T56, X105, mergesortE_in_ga(T55, T57))
U17_gaga(T55, T57, T56, X105, mergesortE_out_ga(T55, T57)) → U18_gaga(T55, T57, T56, X105, mergeH_in_gga(T56, T57, X105))
mergeH_in_gga([], T64, T64) → mergeH_out_gga([], T64, T64)
mergeH_in_gga(T69, [], T69) → mergeH_out_gga(T69, [], T69)
mergeH_in_gga(.(T83, T79), .(T83, T81), .(T83, X135)) → U6_gga(T83, T79, T81, X135, mergeG_in_gga(.(T83, T79), T81, X135))
mergeG_in_gga([], T90, T90) → mergeG_out_gga([], T90, T90)
mergeG_in_gga(T95, [], T95) → mergeG_out_gga(T95, [], T95)
mergeG_in_gga(.(T113, T107), .(T113, T109), .(T113, T111)) → U5_gga(T113, T107, T109, T111, mergeG_in_gga(.(T113, T107), T109, T111))
U5_gga(T113, T107, T109, T111, mergeG_out_gga(.(T113, T107), T109, T111)) → mergeG_out_gga(.(T113, T107), .(T113, T109), .(T113, T111))
U6_gga(T83, T79, T81, X135, mergeG_out_gga(.(T83, T79), T81, X135)) → mergeH_out_gga(.(T83, T79), .(T83, T81), .(T83, X135))
U18_gaga(T55, T57, T56, X105, mergeH_out_gga(T56, T57, X105)) → pL_out_gaga(T55, T57, T56, X105)
U16_gagaa(T54, T56, T55, X104, X105, pL_out_gaga(T55, X104, T56, X105)) → pK_out_gagaa(T54, T56, T55, X104, X105)
U14_gggaaaaa(T51, T52, T53, T54, T55, X103, X104, X105, pK_out_gagaa(T54, X103, T55, X104, X105)) → pF_out_gggaaaaa(T51, T52, T53, T54, T55, X103, X104, X105)
U4_ga(T51, T52, T53, X105, pF_out_gggaaaaa(T51, T52, T53, X101, X102, X103, X104, X105)) → mergesortE_out_ga(.(T51, .(T52, T53)), X105)
U11_gaga(T24, T39, T38, T14, mergesortE_out_ga(T24, T39)) → U12_gaga(T24, T39, T38, T14, mergeG_in_gga(T38, T39, T14))
U12_gaga(T24, T39, T38, T14, mergeG_out_gga(T38, T39, T14)) → pJ_out_gaga(T24, T39, T38, T14)
U10_ggagaa(T21, T25, T38, T24, X23, T14, pJ_out_gaga(T24, X23, T38, T14)) → pI_out_ggagaa(T21, T25, T38, T24, X23, T14)
U8_ggaagaaa(T22, T23, T24, T25, T21, X22, X23, T14, pI_out_ggagaa(T21, T25, X22, T24, X23, T14)) → pB_out_ggaagaaa(T22, T23, T24, T25, T21, X22, X23, T14)
U1_ga(T21, T22, T23, T14, pB_out_ggaagaaa(T22, T23, X41, X40, T21, X22, X23, T14)) → mergesortA_out_ga(.(T21, .(T22, T23)), T14)

(35) UsableRulesProof (EQUIVALENT transformation)

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

(36) Obligation:

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

MERGESORTA_IN_GA(.(T21, .(T22, T23)), T14) → PB_IN_GGAAGAAA(T22, T23, X41, X40, T21, X22, X23, T14)
PB_IN_GGAAGAAA(T22, T23, T24, T25, T21, X22, X23, T14) → U7_GGAAGAAA(T22, T23, T24, T25, T21, X22, X23, T14, splitD_in_ggaa(T22, T23, T24, T25))
U7_GGAAGAAA(T22, T23, T24, T25, T21, X22, X23, T14, splitD_out_ggaa(T22, T23, T24, T25)) → PI_IN_GGAGAA(T21, T25, X22, T24, X23, T14)
PI_IN_GGAGAA(T21, T25, T38, T24, X23, T14) → MERGESORTA_IN_GA(.(T21, T25), T38)

The TRS R consists of the following rules:

splitD_in_ggaa(T30, T31, .(T30, X58), X59) → U3_ggaa(T30, T31, X58, X59, splitC_in_gaa(T31, X59, X58))
U3_ggaa(T30, T31, X58, X59, splitC_out_gaa(T31, X59, X58)) → splitD_out_ggaa(T30, T31, .(T30, X58), X59)
splitC_in_gaa([], [], []) → splitC_out_gaa([], [], [])
splitC_in_gaa(.(T36, T37), .(T36, X76), X77) → U2_gaa(T36, T37, X76, X77, splitC_in_gaa(T37, X77, X76))
U2_gaa(T36, T37, X76, X77, splitC_out_gaa(T37, X77, X76)) → splitC_out_gaa(.(T36, T37), .(T36, X76), X77)

(37) PiDPToQDPProof (SOUND transformation)

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

(38) Obligation:

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

MERGESORTA_IN_GA(.(T21, .(T22, T23))) → PB_IN_GGAAGAAA(T22, T23, T21)
PB_IN_GGAAGAAA(T22, T23, T21) → U7_GGAAGAAA(T22, T23, T21, splitD_in_ggaa(T22, T23))
U7_GGAAGAAA(T22, T23, T21, splitD_out_ggaa(T22, T23, T24, T25)) → PI_IN_GGAGAA(T21, T25, T24)
PI_IN_GGAGAA(T21, T25, T24) → MERGESORTA_IN_GA(.(T21, T25))

The TRS R consists of the following rules:

splitD_in_ggaa(T30, T31) → U3_ggaa(T30, T31, splitC_in_gaa(T31))
U3_ggaa(T30, T31, splitC_out_gaa(T31, X59, X58)) → splitD_out_ggaa(T30, T31, .(T30, X58), X59)
splitC_in_gaa([]) → splitC_out_gaa([], [], [])
splitC_in_gaa(.(T36, T37)) → U2_gaa(T36, T37, splitC_in_gaa(T37))
U2_gaa(T36, T37, splitC_out_gaa(T37, X77, X76)) → splitC_out_gaa(.(T36, T37), .(T36, X76), X77)

The set Q consists of the following terms:

splitD_in_ggaa(x0, x1)
U3_ggaa(x0, x1, x2)
splitC_in_gaa(x0)
U2_gaa(x0, x1, x2)

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

(39) Rewriting (EQUIVALENT transformation)

By rewriting [LPAR04] the rule PB_IN_GGAAGAAA(T22, T23, T21) → U7_GGAAGAAA(T22, T23, T21, splitD_in_ggaa(T22, T23)) at position [3] we obtained the following new rules [LPAR04]:

PB_IN_GGAAGAAA(T22, T23, T21) → U7_GGAAGAAA(T22, T23, T21, U3_ggaa(T22, T23, splitC_in_gaa(T23)))

(40) Obligation:

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

MERGESORTA_IN_GA(.(T21, .(T22, T23))) → PB_IN_GGAAGAAA(T22, T23, T21)
U7_GGAAGAAA(T22, T23, T21, splitD_out_ggaa(T22, T23, T24, T25)) → PI_IN_GGAGAA(T21, T25, T24)
PI_IN_GGAGAA(T21, T25, T24) → MERGESORTA_IN_GA(.(T21, T25))
PB_IN_GGAAGAAA(T22, T23, T21) → U7_GGAAGAAA(T22, T23, T21, U3_ggaa(T22, T23, splitC_in_gaa(T23)))

The TRS R consists of the following rules:

splitD_in_ggaa(T30, T31) → U3_ggaa(T30, T31, splitC_in_gaa(T31))
U3_ggaa(T30, T31, splitC_out_gaa(T31, X59, X58)) → splitD_out_ggaa(T30, T31, .(T30, X58), X59)
splitC_in_gaa([]) → splitC_out_gaa([], [], [])
splitC_in_gaa(.(T36, T37)) → U2_gaa(T36, T37, splitC_in_gaa(T37))
U2_gaa(T36, T37, splitC_out_gaa(T37, X77, X76)) → splitC_out_gaa(.(T36, T37), .(T36, X76), X77)

The set Q consists of the following terms:

splitD_in_ggaa(x0, x1)
U3_ggaa(x0, x1, x2)
splitC_in_gaa(x0)
U2_gaa(x0, x1, x2)

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

(41) UsableRulesProof (EQUIVALENT transformation)

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

(42) Obligation:

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

MERGESORTA_IN_GA(.(T21, .(T22, T23))) → PB_IN_GGAAGAAA(T22, T23, T21)
U7_GGAAGAAA(T22, T23, T21, splitD_out_ggaa(T22, T23, T24, T25)) → PI_IN_GGAGAA(T21, T25, T24)
PI_IN_GGAGAA(T21, T25, T24) → MERGESORTA_IN_GA(.(T21, T25))
PB_IN_GGAAGAAA(T22, T23, T21) → U7_GGAAGAAA(T22, T23, T21, U3_ggaa(T22, T23, splitC_in_gaa(T23)))

The TRS R consists of the following rules:

splitC_in_gaa([]) → splitC_out_gaa([], [], [])
splitC_in_gaa(.(T36, T37)) → U2_gaa(T36, T37, splitC_in_gaa(T37))
U3_ggaa(T30, T31, splitC_out_gaa(T31, X59, X58)) → splitD_out_ggaa(T30, T31, .(T30, X58), X59)
U2_gaa(T36, T37, splitC_out_gaa(T37, X77, X76)) → splitC_out_gaa(.(T36, T37), .(T36, X76), X77)

The set Q consists of the following terms:

splitD_in_ggaa(x0, x1)
U3_ggaa(x0, x1, x2)
splitC_in_gaa(x0)
U2_gaa(x0, x1, x2)

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

(43) QReductionProof (EQUIVALENT transformation)

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

splitD_in_ggaa(x0, x1)

(44) Obligation:

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

MERGESORTA_IN_GA(.(T21, .(T22, T23))) → PB_IN_GGAAGAAA(T22, T23, T21)
U7_GGAAGAAA(T22, T23, T21, splitD_out_ggaa(T22, T23, T24, T25)) → PI_IN_GGAGAA(T21, T25, T24)
PI_IN_GGAGAA(T21, T25, T24) → MERGESORTA_IN_GA(.(T21, T25))
PB_IN_GGAAGAAA(T22, T23, T21) → U7_GGAAGAAA(T22, T23, T21, U3_ggaa(T22, T23, splitC_in_gaa(T23)))

The TRS R consists of the following rules:

splitC_in_gaa([]) → splitC_out_gaa([], [], [])
splitC_in_gaa(.(T36, T37)) → U2_gaa(T36, T37, splitC_in_gaa(T37))
U3_ggaa(T30, T31, splitC_out_gaa(T31, X59, X58)) → splitD_out_ggaa(T30, T31, .(T30, X58), X59)
U2_gaa(T36, T37, splitC_out_gaa(T37, X77, X76)) → splitC_out_gaa(.(T36, T37), .(T36, X76), X77)

The set Q consists of the following terms:

U3_ggaa(x0, x1, x2)
splitC_in_gaa(x0)
U2_gaa(x0, x1, x2)

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

(45) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04,JAR06].

The following pairs can be oriented strictly and are deleted.

MERGESORTA_IN_GA(.(T21, .(T22, T23))) → PB_IN_GGAAGAAA(T22, T23, T21)

The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial interpretation [POLO]:

POL(.(x₁, x₂)) = 1 + x₂
POL(MERGESORTA_IN_GA(x₁)) = x₁
POL(PB_IN_GGAAGAAA(x₁, x₂, x₃)) = 1 + x₂
POL(PI_IN_GGAGAA(x₁, x₂, x₃)) = 1 + x₂
POL(U2_gaa(x₁, x₂, x₃)) = 1 + x₃
POL(U3_ggaa(x₁, x₂, x₃)) = x₃
POL(U7_GGAAGAAA(x₁, x₂, x₃, x₄)) = x₄
POL([]) = 0
POL(splitC_in_gaa(x₁)) = 1 + x₁
POL(splitC_out_gaa(x₁, x₂, x₃)) = 1 + x₂ + x₃
POL(splitD_out_ggaa(x₁, x₂, x₃, x₄)) = 1 + x₄

The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:

splitC_in_gaa([]) → splitC_out_gaa([], [], [])
splitC_in_gaa(.(T36, T37)) → U2_gaa(T36, T37, splitC_in_gaa(T37))
U3_ggaa(T30, T31, splitC_out_gaa(T31, X59, X58)) → splitD_out_ggaa(T30, T31, .(T30, X58), X59)
U2_gaa(T36, T37, splitC_out_gaa(T37, X77, X76)) → splitC_out_gaa(.(T36, T37), .(T36, X76), X77)

(46) Obligation:

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

U7_GGAAGAAA(T22, T23, T21, splitD_out_ggaa(T22, T23, T24, T25)) → PI_IN_GGAGAA(T21, T25, T24)
PI_IN_GGAGAA(T21, T25, T24) → MERGESORTA_IN_GA(.(T21, T25))
PB_IN_GGAAGAAA(T22, T23, T21) → U7_GGAAGAAA(T22, T23, T21, U3_ggaa(T22, T23, splitC_in_gaa(T23)))

The TRS R consists of the following rules:

splitC_in_gaa([]) → splitC_out_gaa([], [], [])
splitC_in_gaa(.(T36, T37)) → U2_gaa(T36, T37, splitC_in_gaa(T37))
U3_ggaa(T30, T31, splitC_out_gaa(T31, X59, X58)) → splitD_out_ggaa(T30, T31, .(T30, X58), X59)
U2_gaa(T36, T37, splitC_out_gaa(T37, X77, X76)) → splitC_out_gaa(.(T36, T37), .(T36, X76), X77)

The set Q consists of the following terms:

U3_ggaa(x0, x1, x2)
splitC_in_gaa(x0)
U2_gaa(x0, x1, x2)

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

(47) DependencyGraphProof (EQUIVALENT transformation)

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

(0) Obligation:

(1) PrologToPiTRSViaGraphTransformerProof (SOUND transformation)

(2) Obligation:

(3) DependencyPairsProof (EQUIVALENT transformation)

(4) Obligation:

(5) DependencyGraphProof (EQUIVALENT transformation)

(6) Complex Obligation (AND)

(7) Obligation:

(8) UsableRulesProof (EQUIVALENT transformation)

(9) Obligation:

(10) PiDPToQDPProof (SOUND transformation)

(11) Obligation:

(12) QDPSizeChangeProof (EQUIVALENT transformation)

(13) YES

(14) Obligation:

(15) UsableRulesProof (EQUIVALENT transformation)

(16) Obligation:

(17) PiDPToQDPProof (SOUND transformation)

(18) Obligation:

(19) QDPSizeChangeProof (EQUIVALENT transformation)

(20) YES

(21) Obligation:

(22) UsableRulesProof (EQUIVALENT transformation)

(23) Obligation:

(24) PiDPToQDPProof (SOUND transformation)

(25) Obligation:

(26) Rewriting (EQUIVALENT transformation)

(27) Obligation:

(28) Rewriting (EQUIVALENT transformation)

(29) Obligation:

(30) QDPOrderProof (EQUIVALENT transformation)

(31) Obligation:

(32) DependencyGraphProof (EQUIVALENT transformation)

(33) TRUE

(34) Obligation:

(35) UsableRulesProof (EQUIVALENT transformation)

(36) Obligation:

(37) PiDPToQDPProof (SOUND transformation)

(38) Obligation:

(39) Rewriting (EQUIVALENT transformation)

(40) Obligation:

(41) UsableRulesProof (EQUIVALENT transformation)

(42) Obligation:

(43) QReductionProof (EQUIVALENT transformation)

(44) Obligation:

(45) QDPOrderProof (EQUIVALENT transformation)

(46) Obligation:

(47) DependencyGraphProof (EQUIVALENT transformation)

(48) TRUE