Left Termination proof of /tmp/tmp7TbLoH/pl8.2.1a.pl

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

0 Prolog

↳1 PrologToPiTRSViaGraphTransformerProof (⇒, 266 ms)

↳2 PiTRS

↳3 DependencyPairsProof (⇔, 499 ms)

↳4 PiDP

↳5 DependencyGraphProof (⇔, 27 ms)

↳6 AND

    ↳7 PiDP

        ↳8 UsableRulesProof (⇔, 0 ms)

        ↳9 PiDP

        ↳10 PiDPToQDPProof (⇒, 0 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 QDPSizeChangeProof (⇔, 0 ms)

        ↳27 YES

    ↳28 PiDP

        ↳29 UsableRulesProof (⇔, 0 ms)

        ↳30 PiDP

        ↳31 PiDPToQDPProof (⇒, 0 ms)

        ↳32 QDP

        ↳33 MRRProof (⇔, 107 ms)

        ↳34 QDP

        ↳35 DependencyGraphProof (⇔, 0 ms)

        ↳36 TRUE

    ↳37 PiDP

        ↳38 UsableRulesProof (⇔, 0 ms)

        ↳39 PiDP

        ↳40 PiDPToQDPProof (⇒, 23 ms)

        ↳41 QDP

        ↳42 QDPOrderProof (⇔, 1338 ms)

        ↳43 QDP

        ↳44 DependencyGraphProof (⇔, 0 ms)

        ↳45 TRUE

(0) Obligation:

Clauses:

mergesort([], []).
mergesort(.(E, []), .(E, [])).
mergesort(.(E, .(F, U)), V) :- ','(split(U, L2, L1), ','(mergesort(.(E, L2), X), ','(mergesort(.(F, L1), Z), merge(X, Z, V)))).
merge(X, [], X).
merge([], X, X).
merge(.(A, X), .(B, Y), .(A, Z)) :- ','(le(A, B), merge(X, .(B, Y), Z)).
merge(.(A, X), .(B, Y), .(B, Z)) :- ','(gt(A, B), merge(.(A, X), Y, Z)).
split([], [], []).
split(.(E, U), .(E, V), W) :- split(U, W, V).
gt(s(X), s(Y)) :- gt(X, Y).
gt(s(X), 0).
le(s(X), s(Y)) :- le(X, Y).
le(0, s(Y)).
le(0, 0).

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];
6 [label="6: 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];
13 [label="13: true | mergesort([], T2), SCOPE: 1, CLAUSE: 1 | mergesort([], T2), SCOPE: 1, CLAUSE: 2\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
15 [label="15: 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];
26 [label="26: mergesort([], T2), SCOPE: 1, CLAUSE: 2\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
28 [label="28: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
31 [label="31: true | mergesort(.(T4, []), T2), SCOPE: 1, CLAUSE: 2\n\nT4 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
32 [label="32: 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];
33 [label="33: 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];
48 [label="48: ','(split(T12, X20, X21), ','(mergesort(.(T10, X20), X22), ','(mergesort(.(T11, 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];
55 [label="55: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
60 [label="60: ','(split(T12, X20, X21), ','(mergesort(.(T10, X20), X22), ','(mergesort(.(T11, X21), X23), merge(X22, X23, T14)))), SCOPE: 2, CLAUSE: 7 | ','(split(T12, X20, X21), ','(mergesort(.(T10, X20), X22), ','(mergesort(.(T11, X21), X23), merge(X22, X23, T14)))), SCOPE: 2, CLAUSE: 8\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];
61 [label="61: ','(split(T12, X20, X21), ','(mergesort(.(T10, X20), X22), ','(mergesort(.(T11, X21), X23), merge(X22, X23, T14)))), SCOPE: 2, CLAUSE: 7\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];
62 [label="62: ','(split(T12, X20, X21), ','(mergesort(.(T10, X20), X22), ','(mergesort(.(T11, X21), X23), merge(X22, X23, T14)))), SCOPE: 2, CLAUSE: 8\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];
68 [label="B: ','(mergesort(.(T10, []), X22), ','(mergesort(.(T11, []), X23), merge(X22, X23, T14)))\n\nT10 is ground\nT11 is ground\nX22 is free\nX23 is free", fontsize=16, style=filled, fillcolor=lightyellow];
69 [label="69: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
73 [label="D: mergesort(.(T10, []), X22)\n\nT10 is ground\nX22 is free", fontsize=16, style=filled, fillcolor=lightyellow];
75 [label="K: ','(mergesort(.(T11, []), X23), merge(T15, X23, T14))\n\nT11 is ground\nT15 is ground\nX23 is free", fontsize=16, style=filled, fillcolor=lightyellow];
76 [label="76: mergesort(.(T10, []), X22), SCOPE: 3, CLAUSE: 0 | mergesort(.(T10, []), X22), SCOPE: 3, CLAUSE: 1 | mergesort(.(T10, []), X22), SCOPE: 3, CLAUSE: 2\n\nT10 is ground\nX22 is free", fontsize=16, style=filled, fillcolor=lightyellow];
77 [label="77: mergesort(.(T10, []), X22), SCOPE: 3, CLAUSE: 1 | mergesort(.(T10, []), X22), SCOPE: 3, CLAUSE: 2\n\nT10 is ground\nX22 is free", fontsize=16, style=filled, fillcolor=lightyellow];
80 [label="80: mergesort(.(T10, []), X22), SCOPE: 3, CLAUSE: 1\n\nT10 is ground\nX22 is free", fontsize=16, style=filled, fillcolor=lightyellow];
82 [label="82: mergesort(.(T10, []), X22), SCOPE: 3, CLAUSE: 2\n\nT10 is ground\nX22 is free", fontsize=16, style=filled, fillcolor=lightyellow];
86 [label="86: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
89 [label="89: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
90 [label="90: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
99 [label="99: mergesort(.(T11, []), X23)\n\nT11 is ground\nX23 is free", fontsize=16, style=filled, fillcolor=lightyellow];
100 [label="E: merge(T15, T22, T14)\n\nT15 is ground\nT22 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
104 [label="104: merge(T15, T22, T14), SCOPE: 4, CLAUSE: 3 | merge(T15, T22, T14), SCOPE: 4, CLAUSE: 4 | merge(T15, T22, T14), SCOPE: 4, CLAUSE: 5 | merge(T15, T22, T14), SCOPE: 4, CLAUSE: 6\n\nT15 is ground\nT22 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
107 [label="107: merge(T15, T22, T14), SCOPE: 4, CLAUSE: 3\n\nT15 is ground\nT22 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
108 [label="108: merge(T15, T22, T14), SCOPE: 4, CLAUSE: 4 | merge(T15, T22, T14), SCOPE: 4, CLAUSE: 5 | merge(T15, T22, T14), SCOPE: 4, CLAUSE: 6\n\nT15 is ground\nT22 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
114 [label="114: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
115 [label="115: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
116 [label="116: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
117 [label="117: merge(T15, T22, T14), SCOPE: 4, CLAUSE: 4\n\nT15 is ground\nT22 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
118 [label="118: merge(T15, T22, T14), SCOPE: 4, CLAUSE: 5 | merge(T15, T22, T14), SCOPE: 4, CLAUSE: 6\n\nT15 is ground\nT22 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
119 [label="119: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
120 [label="120: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
121 [label="121: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
124 [label="124: merge(T15, T22, T14), SCOPE: 4, CLAUSE: 5\n\nT15 is ground\nT22 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
125 [label="125: merge(T15, T22, T14), SCOPE: 4, CLAUSE: 6\n\nT15 is ground\nT22 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
135 [label="F: ','(le(T55, T57), merge(T56, .(T57, T58), T60))\n\nT55 is ground\nT56 is ground\nT57 is ground\nT58 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
136 [label="136: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
139 [label="H: le(T55, T57)\n\nT55 is ground\nT57 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
140 [label="140: merge(T56, .(T57, T58), T60)\n\nT56 is ground\nT57 is ground\nT58 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
144 [label="144: le(T55, T57), SCOPE: 5, CLAUSE: 11 | le(T55, T57), SCOPE: 5, CLAUSE: 12 | le(T55, T57), SCOPE: 5, CLAUSE: 13\n\nT55 is ground\nT57 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
146 [label="146: le(T55, T57), SCOPE: 5, CLAUSE: 11\n\nT55 is ground\nT57 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
149 [label="149: le(T55, T57), SCOPE: 5, CLAUSE: 12 | le(T55, T57), SCOPE: 5, CLAUSE: 13\n\nT55 is ground\nT57 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
157 [label="157: le(T73, T74)\n\nT73 is ground\nT74 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
159 [label="159: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
161 [label="161: le(T55, T57), SCOPE: 5, CLAUSE: 12\n\nT55 is ground\nT57 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
162 [label="162: le(T55, T57), SCOPE: 5, CLAUSE: 13\n\nT55 is ground\nT57 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
165 [label="165: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
166 [label="166: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
167 [label="167: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
168 [label="168: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
170 [label="170: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
171 [label="171: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
181 [label="G: ','(gt(T94, T96), merge(.(T94, T95), T97, T99))\n\nT94 is ground\nT95 is ground\nT96 is ground\nT97 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
183 [label="183: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
188 [label="I: gt(T94, T96)\n\nT94 is ground\nT96 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
189 [label="189: merge(.(T94, T95), T97, T99)\n\nT94 is ground\nT95 is ground\nT97 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
192 [label="192: gt(T94, T96), SCOPE: 6, CLAUSE: 9 | gt(T94, T96), SCOPE: 6, CLAUSE: 10\n\nT94 is ground\nT96 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
196 [label="196: gt(T94, T96), SCOPE: 6, CLAUSE: 9\n\nT94 is ground\nT96 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
197 [label="197: gt(T94, T96), SCOPE: 6, CLAUSE: 10\n\nT94 is ground\nT96 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
208 [label="208: gt(T112, T113)\n\nT112 is ground\nT113 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
209 [label="209: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
212 [label="212: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
213 [label="213: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
214 [label="214: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
223 [label="C: ','(split(T128, X146, X145), ','(mergesort(.(T10, .(T127, X145)), X22), ','(mergesort(.(T11, X146), X23), merge(X22, X23, T14))))\n\nT10 is ground\nT11 is ground\nT127 is ground\nT128 is ground\nX22 is free\nX23 is free\nX145 is free\nX146 is free", fontsize=16, style=filled, fillcolor=lightyellow];
224 [label="224: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
231 [label="J: split(T128, X146, X145)\n\nT128 is ground\nX145 is free\nX146 is free", fontsize=16, style=filled, fillcolor=lightyellow];
232 [label="L: ','(mergesort(.(T10, .(T127, T130)), X22), ','(mergesort(.(T11, T129), X23), merge(X22, X23, T14)))\n\nT10 is ground\nT11 is ground\nT127 is ground\nT129 is ground\nT130 is ground\nX22 is free\nX23 is free", fontsize=16, style=filled, fillcolor=lightyellow];
233 [label="233: split(T128, X146, X145), SCOPE: 7, CLAUSE: 7 | split(T128, X146, X145), SCOPE: 7, CLAUSE: 8\n\nT128 is ground\nX145 is free\nX146 is free", fontsize=16, style=filled, fillcolor=lightyellow];
234 [label="234: split(T128, X146, X145), SCOPE: 7, CLAUSE: 7\n\nT128 is ground\nX145 is free\nX146 is free", fontsize=16, style=filled, fillcolor=lightyellow];
235 [label="235: split(T128, X146, X145), SCOPE: 7, CLAUSE: 8\n\nT128 is ground\nX145 is free\nX146 is free", fontsize=16, style=filled, fillcolor=lightyellow];
236 [label="236: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
237 [label="237: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
238 [label="238: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
239 [label="239: split(T136, X164, X163)\n\nT136 is ground\nX163 is free\nX164 is free", fontsize=16, style=filled, fillcolor=lightyellow];
240 [label="240: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
241 [label="241: mergesort(.(T10, .(T127, T130)), X22)\n\nT10 is ground\nT127 is ground\nT130 is ground\nX22 is free", fontsize=16, style=filled, fillcolor=lightyellow];
242 [label="M: ','(mergesort(.(T11, T129), X23), merge(T137, X23, T14))\n\nT11 is ground\nT129 is ground\nT137 is ground\nX23 is free", fontsize=16, style=filled, fillcolor=lightyellow];
243 [label="243: mergesort(.(T11, T129), X23)\n\nT11 is ground\nT129 is ground\nX23 is free", fontsize=16, style=filled, fillcolor=lightyellow];
244 [label="244: merge(T137, T138, T14)\n\nT137 is ground\nT138 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
245 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
2 -> 245 [arrowhead = none ];
245 -> 6;

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

247 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
6 -> 247 [arrowhead = none ];
247 -> 15;

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

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

250 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
15 -> 250 [arrowhead = none ];
250 -> 32;

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

252 [label="BACKTRACK\nfor clause: mergesort(.(E, .(F, U)), V) :- ','(split(U, L2, L1), ','(mergesort(.(E, L2), X), ','(mergesort(.(F, L1), Z), merge(X, Z, V))))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
26 -> 252 [arrowhead = none ];
252 -> 28;

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

254 [label="EVAL with clause\nmergesort(.(X16, .(X17, X18)), X19) :- ','(split(X18, X20, X21), ','(mergesort(.(X16, X20), X22), ','(mergesort(.(X17, 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];
32 -> 254 [arrowhead = none ];
254 -> 48;

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

256 [label="BACKTRACK\nfor clause: mergesort(.(E, .(F, U)), V) :- ','(split(U, L2, L1), ','(mergesort(.(E, L2), X), ','(mergesort(.(F, L1), Z), merge(X, Z, V))))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
33 -> 256 [arrowhead = none ];
256 -> 34;

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

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

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

260 [label="EVAL with clause\nsplit([], [], []).\nand substitutionT12 -> [],\nX20 -> [],\nX21 -> []", fontsize=14, style = filled, fillcolor = lightblue];
61 -> 260 [arrowhead = none ];
260 -> 68;

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

262 [label="EVAL with clause\nsplit(.(X141, X142), .(X141, X143), X144) :- split(X142, X144, X143).\nand substitutionX141 -> T127,\nX142 -> T128,\nT12 -> .(T127, T128),\nX143 -> X145,\nX20 -> .(T127, X145),\nX21 -> X146,\nX144 -> X146", fontsize=14, style = filled, fillcolor = lightblue];
62 -> 262 [arrowhead = none ];
262 -> 223;

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

264 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
68 -> 264 [arrowhead = none ];
264 -> 73;

265 [label="SPLIT 2\nnew knowledge:\nT10 is ground\nT15 is ground\nreplacements:X22 -> T15", fontsize=14, style = filled, fillcolor = violet];
68 -> 265 [arrowhead = none ];
265 -> 75;

266 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
73 -> 266 [arrowhead = none ];
266 -> 76;

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

268 [label="SPLIT 2\nnew knowledge:\nT11 is ground\nT22 is ground\nreplacements:X23 -> T22", fontsize=14, style = filled, fillcolor = violet];
75 -> 268 [arrowhead = none ];
268 -> 100;

269 [label="BACKTRACK\nfor clause: mergesort([], [])because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
76 -> 269 [arrowhead = none ];
269 -> 77;

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

271 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
77 -> 271 [arrowhead = none ];
271 -> 82;

272 [label="ONLY EVAL with clause\nmergesort(.(X28, []), .(X28, [])).\nand substitutionT10 -> T20,\nX28 -> T20,\nX22 -> .(T20, [])", fontsize=14, style = filled, fillcolor = lightblue];
80 -> 272 [arrowhead = none ];
272 -> 86;

273 [label="BACKTRACK\nfor clause: mergesort(.(E, .(F, U)), V) :- ','(split(U, L2, L1), ','(mergesort(.(E, L2), X), ','(mergesort(.(F, L1), Z), merge(X, Z, V))))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
82 -> 273 [arrowhead = none ];
273 -> 90;

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

275 [label="INSTANCE with matching:\nT10 -> T11\nX22 -> X23", fontsize=14, style = filled, fillcolor = lightgrey];
99 -> 275 [arrowhead = none , style=dashed];
275 -> 73[style=dashed];

276 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
100 -> 276 [arrowhead = none ];
276 -> 104;

277 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
104 -> 277 [arrowhead = none ];
277 -> 107;

278 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
104 -> 278 [arrowhead = none ];
278 -> 108;

279 [label="EVAL with clause\nmerge(X39, [], X39).\nand substitutionT15 -> T29,\nX39 -> T29,\nT22 -> [],\nT14 -> T29", fontsize=14, style = filled, fillcolor = lightblue];
107 -> 279 [arrowhead = none ];
279 -> 114;

280 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
107 -> 280 [arrowhead = none ];
280 -> 115;

281 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
108 -> 281 [arrowhead = none ];
281 -> 117;

282 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
108 -> 282 [arrowhead = none ];
282 -> 118;

283 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
114 -> 283 [arrowhead = none ];
283 -> 116;

284 [label="EVAL with clause\nmerge([], X44, X44).\nand substitutionT15 -> [],\nT22 -> T34,\nX44 -> T34,\nT14 -> T34", fontsize=14, style = filled, fillcolor = lightblue];
117 -> 284 [arrowhead = none ];
284 -> 119;

285 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
117 -> 285 [arrowhead = none ];
285 -> 120;

286 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
118 -> 286 [arrowhead = none ];
286 -> 124;

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

288 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
119 -> 288 [arrowhead = none ];
288 -> 121;

289 [label="EVAL with clause\nmerge(.(X65, X66), .(X67, X68), .(X65, X69)) :- ','(le(X65, X67), merge(X66, .(X67, X68), X69)).\nand substitutionX65 -> T55,\nX66 -> T56,\nT15 -> .(T55, T56),\nX67 -> T57,\nX68 -> T58,\nT22 -> .(T57, T58),\nX69 -> T60,\nT14 -> .(T55, T60),\nT59 -> T60", fontsize=14, style = filled, fillcolor = lightblue];
124 -> 289 [arrowhead = none ];
289 -> 135;

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

291 [label="EVAL with clause\nmerge(.(X103, X104), .(X105, X106), .(X105, X107)) :- ','(gt(X103, X105), merge(.(X103, X104), X106, X107)).\nand substitutionX103 -> T94,\nX104 -> T95,\nT15 -> .(T94, T95),\nX105 -> T96,\nX106 -> T97,\nT22 -> .(T96, T97),\nX107 -> T99,\nT14 -> .(T96, T99),\nT98 -> T99", fontsize=14, style = filled, fillcolor = lightblue];
125 -> 291 [arrowhead = none ];
291 -> 181;

292 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
125 -> 292 [arrowhead = none ];
292 -> 183;

293 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
135 -> 293 [arrowhead = none ];
293 -> 139;

294 [label="SPLIT 2\nnew knowledge:\nT55 is ground\nT57 is ground", fontsize=14, style = filled, fillcolor = violet];
135 -> 294 [arrowhead = none ];
294 -> 140;

295 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
139 -> 295 [arrowhead = none ];
295 -> 144;

296 [label="INSTANCE with matching:\nT15 -> T56\nT22 -> .(T57, T58)\nT14 -> T60", fontsize=14, style = filled, fillcolor = lightgrey];
140 -> 296 [arrowhead = none , style=dashed];
296 -> 100[style=dashed];

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

298 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
144 -> 298 [arrowhead = none ];
298 -> 149;

299 [label="EVAL with clause\nle(s(X82), s(X83)) :- le(X82, X83).\nand substitutionX82 -> T73,\nT55 -> s(T73),\nX83 -> T74,\nT57 -> s(T74)", fontsize=14, style = filled, fillcolor = lightblue];
146 -> 299 [arrowhead = none ];
299 -> 157;

300 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
146 -> 300 [arrowhead = none ];
300 -> 159;

301 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
149 -> 301 [arrowhead = none ];
301 -> 161;

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

303 [label="INSTANCE with matching:\nT55 -> T73\nT57 -> T74", fontsize=14, style = filled, fillcolor = lightgrey];
157 -> 303 [arrowhead = none , style=dashed];
303 -> 139[style=dashed];

304 [label="EVAL with clause\nle(0, s(X90)).\nand substitutionT55 -> 0,\nX90 -> T81,\nT57 -> s(T81)", fontsize=14, style = filled, fillcolor = lightblue];
161 -> 304 [arrowhead = none ];
304 -> 165;

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

306 [label="EVAL with clause\nle(0, 0).\nand substitutionT55 -> 0,\nT57 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
162 -> 306 [arrowhead = none ];
306 -> 168;

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

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

309 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
168 -> 309 [arrowhead = none ];
309 -> 171;

310 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
181 -> 310 [arrowhead = none ];
310 -> 188;

311 [label="SPLIT 2\nnew knowledge:\nT94 is ground\nT96 is ground", fontsize=14, style = filled, fillcolor = violet];
181 -> 311 [arrowhead = none ];
311 -> 189;

312 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
188 -> 312 [arrowhead = none ];
312 -> 192;

313 [label="INSTANCE with matching:\nT15 -> .(T94, T95)\nT22 -> T97\nT14 -> T99", fontsize=14, style = filled, fillcolor = lightgrey];
189 -> 313 [arrowhead = none , style=dashed];
313 -> 100[style=dashed];

314 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
192 -> 314 [arrowhead = none ];
314 -> 196;

315 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
192 -> 315 [arrowhead = none ];
315 -> 197;

316 [label="EVAL with clause\ngt(s(X120), s(X121)) :- gt(X120, X121).\nand substitutionX120 -> T112,\nT94 -> s(T112),\nX121 -> T113,\nT96 -> s(T113)", fontsize=14, style = filled, fillcolor = lightblue];
196 -> 316 [arrowhead = none ];
316 -> 208;

317 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
196 -> 317 [arrowhead = none ];
317 -> 209;

318 [label="EVAL with clause\ngt(s(X126), 0).\nand substitutionX126 -> T118,\nT94 -> s(T118),\nT96 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
197 -> 318 [arrowhead = none ];
318 -> 212;

319 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
197 -> 319 [arrowhead = none ];
319 -> 213;

320 [label="INSTANCE with matching:\nT94 -> T112\nT96 -> T113", fontsize=14, style = filled, fillcolor = lightgrey];
208 -> 320 [arrowhead = none , style=dashed];
320 -> 188[style=dashed];

321 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
212 -> 321 [arrowhead = none ];
321 -> 214;

322 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
223 -> 322 [arrowhead = none ];
322 -> 231;

323 [label="SPLIT 2\nnew knowledge:\nT128 is ground\nT129 is ground\nT130 is ground\nreplacements:X146 -> T129,\nX145 -> T130", fontsize=14, style = filled, fillcolor = violet];
223 -> 323 [arrowhead = none ];
323 -> 232;

324 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
231 -> 324 [arrowhead = none ];
324 -> 233;

325 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
232 -> 325 [arrowhead = none ];
325 -> 241;

326 [label="SPLIT 2\nnew knowledge:\nT10 is ground\nT127 is ground\nT130 is ground\nT137 is ground\nreplacements:X22 -> T137", fontsize=14, style = filled, fillcolor = violet];
232 -> 326 [arrowhead = none ];
326 -> 242;

327 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
233 -> 327 [arrowhead = none ];
327 -> 234;

328 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
233 -> 328 [arrowhead = none ];
328 -> 235;

329 [label="EVAL with clause\nsplit([], [], []).\nand substitutionT128 -> [],\nX146 -> [],\nX145 -> []", fontsize=14, style = filled, fillcolor = lightblue];
234 -> 329 [arrowhead = none ];
329 -> 236;

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

331 [label="EVAL with clause\nsplit(.(X159, X160), .(X159, X161), X162) :- split(X160, X162, X161).\nand substitutionX159 -> T135,\nX160 -> T136,\nT128 -> .(T135, T136),\nX161 -> X163,\nX146 -> .(T135, X163),\nX145 -> X164,\nX162 -> X164", fontsize=14, style = filled, fillcolor = lightblue];
235 -> 331 [arrowhead = none ];
331 -> 239;

332 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
235 -> 332 [arrowhead = none ];
332 -> 240;

333 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
236 -> 333 [arrowhead = none ];
333 -> 238;

334 [label="INSTANCE with matching:\nT128 -> T136\nX146 -> X164\nX145 -> X163", fontsize=14, style = filled, fillcolor = lightgrey];
239 -> 334 [arrowhead = none , style=dashed];
334 -> 231[style=dashed];

335 [label="INSTANCE with matching:\nT1 -> .(T10, .(T127, T130))\nT2 -> X22", fontsize=14, style = filled, fillcolor = lightgrey];
241 -> 335 [arrowhead = none , style=dashed];
335 -> 2[style=dashed];

336 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
242 -> 336 [arrowhead = none ];
336 -> 243;

337 [label="SPLIT 2\nnew knowledge:\nT11 is ground\nT129 is ground\nT138 is ground\nreplacements:X23 -> T138", fontsize=14, style = filled, fillcolor = violet];
242 -> 337 [arrowhead = none ];
337 -> 244;

338 [label="INSTANCE with matching:\nT1 -> .(T11, T129)\nT2 -> X23", fontsize=14, style = filled, fillcolor = lightgrey];
243 -> 338 [arrowhead = none , style=dashed];
338 -> 2[style=dashed];

339 [label="INSTANCE with matching:\nT15 -> T137\nT22 -> T138", fontsize=14, style = filled, fillcolor = lightgrey];
244 -> 339 [arrowhead = none , style=dashed];
339 -> 100[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(.(T10, .(T11, [])), T14) → U1_ga(T10, T11, T14, pB_in_gagaa(T10, X22, T11, X23, T14))
pB_in_gagaa(T10, T15, T11, X23, T14) → U8_gagaa(T10, T15, T11, X23, T14, mergesortD_in_ga(T10, T15))
mergesortD_in_ga(T20, .(T20, [])) → mergesortD_out_ga(T20, .(T20, []))
U8_gagaa(T10, T15, T11, X23, T14, mergesortD_out_ga(T10, T15)) → U9_gagaa(T10, T15, T11, X23, T14, pK_in_gaga(T11, X23, T15, T14))
pK_in_gaga(T11, T22, T15, T14) → U10_gaga(T11, T22, T15, T14, mergesortD_in_ga(T11, T22))
U10_gaga(T11, T22, T15, T14, mergesortD_out_ga(T11, T22)) → U11_gaga(T11, T22, T15, T14, mergeE_in_gga(T15, T22, T14))
mergeE_in_gga(T29, [], T29) → mergeE_out_gga(T29, [], T29)
mergeE_in_gga([], T34, T34) → mergeE_out_gga([], T34, T34)
mergeE_in_gga(.(T55, T56), .(T57, T58), .(T55, T60)) → U3_gga(T55, T56, T57, T58, T60, pF_in_gggga(T55, T57, T56, T58, T60))
pF_in_gggga(T55, T57, T56, T58, T60) → U12_gggga(T55, T57, T56, T58, T60, leH_in_gg(T55, T57))
leH_in_gg(s(T73), s(T74)) → U5_gg(T73, T74, leH_in_gg(T73, T74))
leH_in_gg(0, s(T81)) → leH_out_gg(0, s(T81))
leH_in_gg(0, 0) → leH_out_gg(0, 0)
U5_gg(T73, T74, leH_out_gg(T73, T74)) → leH_out_gg(s(T73), s(T74))
U12_gggga(T55, T57, T56, T58, T60, leH_out_gg(T55, T57)) → U13_gggga(T55, T57, T56, T58, T60, mergeE_in_gga(T56, .(T57, T58), T60))
mergeE_in_gga(.(T94, T95), .(T96, T97), .(T96, T99)) → U4_gga(T94, T95, T96, T97, T99, pG_in_gggga(T94, T96, T95, T97, T99))
pG_in_gggga(T94, T96, T95, T97, T99) → U14_gggga(T94, T96, T95, T97, T99, gtI_in_gg(T94, T96))
gtI_in_gg(s(T112), s(T113)) → U6_gg(T112, T113, gtI_in_gg(T112, T113))
gtI_in_gg(s(T118), 0) → gtI_out_gg(s(T118), 0)
U6_gg(T112, T113, gtI_out_gg(T112, T113)) → gtI_out_gg(s(T112), s(T113))
U14_gggga(T94, T96, T95, T97, T99, gtI_out_gg(T94, T96)) → U15_gggga(T94, T96, T95, T97, T99, mergeE_in_gga(.(T94, T95), T97, T99))
U15_gggga(T94, T96, T95, T97, T99, mergeE_out_gga(.(T94, T95), T97, T99)) → pG_out_gggga(T94, T96, T95, T97, T99)
U4_gga(T94, T95, T96, T97, T99, pG_out_gggga(T94, T96, T95, T97, T99)) → mergeE_out_gga(.(T94, T95), .(T96, T97), .(T96, T99))
U13_gggga(T55, T57, T56, T58, T60, mergeE_out_gga(T56, .(T57, T58), T60)) → pF_out_gggga(T55, T57, T56, T58, T60)
U3_gga(T55, T56, T57, T58, T60, pF_out_gggga(T55, T57, T56, T58, T60)) → mergeE_out_gga(.(T55, T56), .(T57, T58), .(T55, T60))
U11_gaga(T11, T22, T15, T14, mergeE_out_gga(T15, T22, T14)) → pK_out_gaga(T11, T22, T15, T14)
U9_gagaa(T10, T15, T11, X23, T14, pK_out_gaga(T11, X23, T15, T14)) → pB_out_gagaa(T10, T15, T11, X23, T14)
U1_ga(T10, T11, T14, pB_out_gagaa(T10, X22, T11, X23, T14)) → mergesortA_out_ga(.(T10, .(T11, [])), T14)
mergesortA_in_ga(.(T10, .(T11, .(T127, T128))), T14) → U2_ga(T10, T11, T127, T128, T14, pC_in_gaaggagaa(T128, X146, X145, T10, T127, X22, T11, X23, T14))
pC_in_gaaggagaa(T128, T129, T130, T10, T127, X22, T11, X23, T14) → U16_gaaggagaa(T128, T129, T130, T10, T127, X22, T11, X23, T14, splitJ_in_gaa(T128, T129, T130))
splitJ_in_gaa([], [], []) → splitJ_out_gaa([], [], [])
splitJ_in_gaa(.(T135, T136), .(T135, X163), X164) → U7_gaa(T135, T136, X163, X164, splitJ_in_gaa(T136, X164, X163))
U7_gaa(T135, T136, X163, X164, splitJ_out_gaa(T136, X164, X163)) → splitJ_out_gaa(.(T135, T136), .(T135, X163), X164)
U16_gaaggagaa(T128, T129, T130, T10, T127, X22, T11, X23, T14, splitJ_out_gaa(T128, T129, T130)) → U17_gaaggagaa(T128, T129, T130, T10, T127, X22, T11, X23, T14, pL_in_gggaggaa(T10, T127, T130, X22, T11, T129, X23, T14))
pL_in_gggaggaa(T10, T127, T130, T137, T11, T129, X23, T14) → U18_gggaggaa(T10, T127, T130, T137, T11, T129, X23, T14, mergesortA_in_ga(.(T10, .(T127, T130)), T137))
U18_gggaggaa(T10, T127, T130, T137, T11, T129, X23, T14, mergesortA_out_ga(.(T10, .(T127, T130)), T137)) → U19_gggaggaa(T10, T127, T130, T137, T11, T129, X23, T14, pM_in_ggaga(T11, T129, X23, T137, T14))
pM_in_ggaga(T11, T129, T138, T137, T14) → U20_ggaga(T11, T129, T138, T137, T14, mergesortA_in_ga(.(T11, T129), T138))
U20_ggaga(T11, T129, T138, T137, T14, mergesortA_out_ga(.(T11, T129), T138)) → U21_ggaga(T11, T129, T138, T137, T14, mergeE_in_gga(T137, T138, T14))
U21_ggaga(T11, T129, T138, T137, T14, mergeE_out_gga(T137, T138, T14)) → pM_out_ggaga(T11, T129, T138, T137, T14)
U19_gggaggaa(T10, T127, T130, T137, T11, T129, X23, T14, pM_out_ggaga(T11, T129, X23, T137, T14)) → pL_out_gggaggaa(T10, T127, T130, T137, T11, T129, X23, T14)
U17_gaaggagaa(T128, T129, T130, T10, T127, X22, T11, X23, T14, pL_out_gggaggaa(T10, T127, T130, X22, T11, T129, X23, T14)) → pC_out_gaaggagaa(T128, T129, T130, T10, T127, X22, T11, X23, T14)
U2_ga(T10, T11, T127, T128, T14, pC_out_gaaggagaa(T128, X146, X145, T10, T127, X22, T11, X23, T14)) → mergesortA_out_ga(.(T10, .(T11, .(T127, T128))), 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(.(T10, .(T11, [])), T14) → U1_GA(T10, T11, T14, pB_in_gagaa(T10, X22, T11, X23, T14))
MERGESORTA_IN_GA(.(T10, .(T11, [])), T14) → PB_IN_GAGAA(T10, X22, T11, X23, T14)
PB_IN_GAGAA(T10, T15, T11, X23, T14) → U8_GAGAA(T10, T15, T11, X23, T14, mergesortD_in_ga(T10, T15))
PB_IN_GAGAA(T10, T15, T11, X23, T14) → MERGESORTD_IN_GA(T10, T15)
U8_GAGAA(T10, T15, T11, X23, T14, mergesortD_out_ga(T10, T15)) → U9_GAGAA(T10, T15, T11, X23, T14, pK_in_gaga(T11, X23, T15, T14))
U8_GAGAA(T10, T15, T11, X23, T14, mergesortD_out_ga(T10, T15)) → PK_IN_GAGA(T11, X23, T15, T14)
PK_IN_GAGA(T11, T22, T15, T14) → U10_GAGA(T11, T22, T15, T14, mergesortD_in_ga(T11, T22))
PK_IN_GAGA(T11, T22, T15, T14) → MERGESORTD_IN_GA(T11, T22)
U10_GAGA(T11, T22, T15, T14, mergesortD_out_ga(T11, T22)) → U11_GAGA(T11, T22, T15, T14, mergeE_in_gga(T15, T22, T14))
U10_GAGA(T11, T22, T15, T14, mergesortD_out_ga(T11, T22)) → MERGEE_IN_GGA(T15, T22, T14)
MERGEE_IN_GGA(.(T55, T56), .(T57, T58), .(T55, T60)) → U3_GGA(T55, T56, T57, T58, T60, pF_in_gggga(T55, T57, T56, T58, T60))
MERGEE_IN_GGA(.(T55, T56), .(T57, T58), .(T55, T60)) → PF_IN_GGGGA(T55, T57, T56, T58, T60)
PF_IN_GGGGA(T55, T57, T56, T58, T60) → U12_GGGGA(T55, T57, T56, T58, T60, leH_in_gg(T55, T57))
PF_IN_GGGGA(T55, T57, T56, T58, T60) → LEH_IN_GG(T55, T57)
LEH_IN_GG(s(T73), s(T74)) → U5_GG(T73, T74, leH_in_gg(T73, T74))
LEH_IN_GG(s(T73), s(T74)) → LEH_IN_GG(T73, T74)
U12_GGGGA(T55, T57, T56, T58, T60, leH_out_gg(T55, T57)) → U13_GGGGA(T55, T57, T56, T58, T60, mergeE_in_gga(T56, .(T57, T58), T60))
U12_GGGGA(T55, T57, T56, T58, T60, leH_out_gg(T55, T57)) → MERGEE_IN_GGA(T56, .(T57, T58), T60)
MERGEE_IN_GGA(.(T94, T95), .(T96, T97), .(T96, T99)) → U4_GGA(T94, T95, T96, T97, T99, pG_in_gggga(T94, T96, T95, T97, T99))
MERGEE_IN_GGA(.(T94, T95), .(T96, T97), .(T96, T99)) → PG_IN_GGGGA(T94, T96, T95, T97, T99)
PG_IN_GGGGA(T94, T96, T95, T97, T99) → U14_GGGGA(T94, T96, T95, T97, T99, gtI_in_gg(T94, T96))
PG_IN_GGGGA(T94, T96, T95, T97, T99) → GTI_IN_GG(T94, T96)
GTI_IN_GG(s(T112), s(T113)) → U6_GG(T112, T113, gtI_in_gg(T112, T113))
GTI_IN_GG(s(T112), s(T113)) → GTI_IN_GG(T112, T113)
U14_GGGGA(T94, T96, T95, T97, T99, gtI_out_gg(T94, T96)) → U15_GGGGA(T94, T96, T95, T97, T99, mergeE_in_gga(.(T94, T95), T97, T99))
U14_GGGGA(T94, T96, T95, T97, T99, gtI_out_gg(T94, T96)) → MERGEE_IN_GGA(.(T94, T95), T97, T99)
MERGESORTA_IN_GA(.(T10, .(T11, .(T127, T128))), T14) → U2_GA(T10, T11, T127, T128, T14, pC_in_gaaggagaa(T128, X146, X145, T10, T127, X22, T11, X23, T14))
MERGESORTA_IN_GA(.(T10, .(T11, .(T127, T128))), T14) → PC_IN_GAAGGAGAA(T128, X146, X145, T10, T127, X22, T11, X23, T14)
PC_IN_GAAGGAGAA(T128, T129, T130, T10, T127, X22, T11, X23, T14) → U16_GAAGGAGAA(T128, T129, T130, T10, T127, X22, T11, X23, T14, splitJ_in_gaa(T128, T129, T130))
PC_IN_GAAGGAGAA(T128, T129, T130, T10, T127, X22, T11, X23, T14) → SPLITJ_IN_GAA(T128, T129, T130)
SPLITJ_IN_GAA(.(T135, T136), .(T135, X163), X164) → U7_GAA(T135, T136, X163, X164, splitJ_in_gaa(T136, X164, X163))
SPLITJ_IN_GAA(.(T135, T136), .(T135, X163), X164) → SPLITJ_IN_GAA(T136, X164, X163)
U16_GAAGGAGAA(T128, T129, T130, T10, T127, X22, T11, X23, T14, splitJ_out_gaa(T128, T129, T130)) → U17_GAAGGAGAA(T128, T129, T130, T10, T127, X22, T11, X23, T14, pL_in_gggaggaa(T10, T127, T130, X22, T11, T129, X23, T14))
U16_GAAGGAGAA(T128, T129, T130, T10, T127, X22, T11, X23, T14, splitJ_out_gaa(T128, T129, T130)) → PL_IN_GGGAGGAA(T10, T127, T130, X22, T11, T129, X23, T14)
PL_IN_GGGAGGAA(T10, T127, T130, T137, T11, T129, X23, T14) → U18_GGGAGGAA(T10, T127, T130, T137, T11, T129, X23, T14, mergesortA_in_ga(.(T10, .(T127, T130)), T137))
PL_IN_GGGAGGAA(T10, T127, T130, T137, T11, T129, X23, T14) → MERGESORTA_IN_GA(.(T10, .(T127, T130)), T137)
U18_GGGAGGAA(T10, T127, T130, T137, T11, T129, X23, T14, mergesortA_out_ga(.(T10, .(T127, T130)), T137)) → U19_GGGAGGAA(T10, T127, T130, T137, T11, T129, X23, T14, pM_in_ggaga(T11, T129, X23, T137, T14))
U18_GGGAGGAA(T10, T127, T130, T137, T11, T129, X23, T14, mergesortA_out_ga(.(T10, .(T127, T130)), T137)) → PM_IN_GGAGA(T11, T129, X23, T137, T14)
PM_IN_GGAGA(T11, T129, T138, T137, T14) → U20_GGAGA(T11, T129, T138, T137, T14, mergesortA_in_ga(.(T11, T129), T138))
PM_IN_GGAGA(T11, T129, T138, T137, T14) → MERGESORTA_IN_GA(.(T11, T129), T138)
U20_GGAGA(T11, T129, T138, T137, T14, mergesortA_out_ga(.(T11, T129), T138)) → U21_GGAGA(T11, T129, T138, T137, T14, mergeE_in_gga(T137, T138, T14))
U20_GGAGA(T11, T129, T138, T137, T14, mergesortA_out_ga(.(T11, T129), T138)) → MERGEE_IN_GGA(T137, T138, 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(.(T10, .(T11, [])), T14) → U1_ga(T10, T11, T14, pB_in_gagaa(T10, X22, T11, X23, T14))
pB_in_gagaa(T10, T15, T11, X23, T14) → U8_gagaa(T10, T15, T11, X23, T14, mergesortD_in_ga(T10, T15))
mergesortD_in_ga(T20, .(T20, [])) → mergesortD_out_ga(T20, .(T20, []))
U8_gagaa(T10, T15, T11, X23, T14, mergesortD_out_ga(T10, T15)) → U9_gagaa(T10, T15, T11, X23, T14, pK_in_gaga(T11, X23, T15, T14))
pK_in_gaga(T11, T22, T15, T14) → U10_gaga(T11, T22, T15, T14, mergesortD_in_ga(T11, T22))
U10_gaga(T11, T22, T15, T14, mergesortD_out_ga(T11, T22)) → U11_gaga(T11, T22, T15, T14, mergeE_in_gga(T15, T22, T14))
mergeE_in_gga(T29, [], T29) → mergeE_out_gga(T29, [], T29)
mergeE_in_gga([], T34, T34) → mergeE_out_gga([], T34, T34)
mergeE_in_gga(.(T55, T56), .(T57, T58), .(T55, T60)) → U3_gga(T55, T56, T57, T58, T60, pF_in_gggga(T55, T57, T56, T58, T60))
pF_in_gggga(T55, T57, T56, T58, T60) → U12_gggga(T55, T57, T56, T58, T60, leH_in_gg(T55, T57))
leH_in_gg(s(T73), s(T74)) → U5_gg(T73, T74, leH_in_gg(T73, T74))
leH_in_gg(0, s(T81)) → leH_out_gg(0, s(T81))
leH_in_gg(0, 0) → leH_out_gg(0, 0)
U5_gg(T73, T74, leH_out_gg(T73, T74)) → leH_out_gg(s(T73), s(T74))
U12_gggga(T55, T57, T56, T58, T60, leH_out_gg(T55, T57)) → U13_gggga(T55, T57, T56, T58, T60, mergeE_in_gga(T56, .(T57, T58), T60))
mergeE_in_gga(.(T94, T95), .(T96, T97), .(T96, T99)) → U4_gga(T94, T95, T96, T97, T99, pG_in_gggga(T94, T96, T95, T97, T99))
pG_in_gggga(T94, T96, T95, T97, T99) → U14_gggga(T94, T96, T95, T97, T99, gtI_in_gg(T94, T96))
gtI_in_gg(s(T112), s(T113)) → U6_gg(T112, T113, gtI_in_gg(T112, T113))
gtI_in_gg(s(T118), 0) → gtI_out_gg(s(T118), 0)
U6_gg(T112, T113, gtI_out_gg(T112, T113)) → gtI_out_gg(s(T112), s(T113))
U14_gggga(T94, T96, T95, T97, T99, gtI_out_gg(T94, T96)) → U15_gggga(T94, T96, T95, T97, T99, mergeE_in_gga(.(T94, T95), T97, T99))
U15_gggga(T94, T96, T95, T97, T99, mergeE_out_gga(.(T94, T95), T97, T99)) → pG_out_gggga(T94, T96, T95, T97, T99)
U4_gga(T94, T95, T96, T97, T99, pG_out_gggga(T94, T96, T95, T97, T99)) → mergeE_out_gga(.(T94, T95), .(T96, T97), .(T96, T99))
U13_gggga(T55, T57, T56, T58, T60, mergeE_out_gga(T56, .(T57, T58), T60)) → pF_out_gggga(T55, T57, T56, T58, T60)
U3_gga(T55, T56, T57, T58, T60, pF_out_gggga(T55, T57, T56, T58, T60)) → mergeE_out_gga(.(T55, T56), .(T57, T58), .(T55, T60))
U11_gaga(T11, T22, T15, T14, mergeE_out_gga(T15, T22, T14)) → pK_out_gaga(T11, T22, T15, T14)
U9_gagaa(T10, T15, T11, X23, T14, pK_out_gaga(T11, X23, T15, T14)) → pB_out_gagaa(T10, T15, T11, X23, T14)
U1_ga(T10, T11, T14, pB_out_gagaa(T10, X22, T11, X23, T14)) → mergesortA_out_ga(.(T10, .(T11, [])), T14)
mergesortA_in_ga(.(T10, .(T11, .(T127, T128))), T14) → U2_ga(T10, T11, T127, T128, T14, pC_in_gaaggagaa(T128, X146, X145, T10, T127, X22, T11, X23, T14))
pC_in_gaaggagaa(T128, T129, T130, T10, T127, X22, T11, X23, T14) → U16_gaaggagaa(T128, T129, T130, T10, T127, X22, T11, X23, T14, splitJ_in_gaa(T128, T129, T130))
splitJ_in_gaa([], [], []) → splitJ_out_gaa([], [], [])
splitJ_in_gaa(.(T135, T136), .(T135, X163), X164) → U7_gaa(T135, T136, X163, X164, splitJ_in_gaa(T136, X164, X163))
U7_gaa(T135, T136, X163, X164, splitJ_out_gaa(T136, X164, X163)) → splitJ_out_gaa(.(T135, T136), .(T135, X163), X164)
U16_gaaggagaa(T128, T129, T130, T10, T127, X22, T11, X23, T14, splitJ_out_gaa(T128, T129, T130)) → U17_gaaggagaa(T128, T129, T130, T10, T127, X22, T11, X23, T14, pL_in_gggaggaa(T10, T127, T130, X22, T11, T129, X23, T14))
pL_in_gggaggaa(T10, T127, T130, T137, T11, T129, X23, T14) → U18_gggaggaa(T10, T127, T130, T137, T11, T129, X23, T14, mergesortA_in_ga(.(T10, .(T127, T130)), T137))
U18_gggaggaa(T10, T127, T130, T137, T11, T129, X23, T14, mergesortA_out_ga(.(T10, .(T127, T130)), T137)) → U19_gggaggaa(T10, T127, T130, T137, T11, T129, X23, T14, pM_in_ggaga(T11, T129, X23, T137, T14))
pM_in_ggaga(T11, T129, T138, T137, T14) → U20_ggaga(T11, T129, T138, T137, T14, mergesortA_in_ga(.(T11, T129), T138))
U20_ggaga(T11, T129, T138, T137, T14, mergesortA_out_ga(.(T11, T129), T138)) → U21_ggaga(T11, T129, T138, T137, T14, mergeE_in_gga(T137, T138, T14))
U21_ggaga(T11, T129, T138, T137, T14, mergeE_out_gga(T137, T138, T14)) → pM_out_ggaga(T11, T129, T138, T137, T14)
U19_gggaggaa(T10, T127, T130, T137, T11, T129, X23, T14, pM_out_ggaga(T11, T129, X23, T137, T14)) → pL_out_gggaggaa(T10, T127, T130, T137, T11, T129, X23, T14)
U17_gaaggagaa(T128, T129, T130, T10, T127, X22, T11, X23, T14, pL_out_gggaggaa(T10, T127, T130, X22, T11, T129, X23, T14)) → pC_out_gaaggagaa(T128, T129, T130, T10, T127, X22, T11, X23, T14)
U2_ga(T10, T11, T127, T128, T14, pC_out_gaaggagaa(T128, X146, X145, T10, T127, X22, T11, X23, T14)) → mergesortA_out_ga(.(T10, .(T11, .(T127, T128))), 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) = U1_ga(x1, x2, x4)
pB_in_gagaa(x1, x2, x3, x4, x5) = pB_in_gagaa(x1, x3)
U8_gagaa(x1, x2, x3, x4, x5, x6) = U8_gagaa(x1, x3, x6)
mergesortD_in_ga(x1, x2) = mergesortD_in_ga(x1)
mergesortD_out_ga(x1, x2) = mergesortD_out_ga(x1, x2)
U9_gagaa(x1, x2, x3, x4, x5, x6) = U9_gagaa(x1, x2, x3, x6)
pK_in_gaga(x1, x2, x3, x4) = pK_in_gaga(x1, x3)
U10_gaga(x1, x2, x3, x4, x5) = U10_gaga(x1, x3, x5)
U11_gaga(x1, x2, x3, x4, x5) = U11_gaga(x1, x2, x3, x5)
mergeE_in_gga(x1, x2, x3) = mergeE_in_gga(x1, x2)
mergeE_out_gga(x1, x2, x3) = mergeE_out_gga(x1, x2, x3)
U3_gga(x1, x2, x3, x4, x5, x6) = U3_gga(x1, x2, x3, x4, x6)
pF_in_gggga(x1, x2, x3, x4, x5) = pF_in_gggga(x1, x2, x3, x4)
U12_gggga(x1, x2, x3, x4, x5, x6) = U12_gggga(x1, x2, x3, x4, x6)
leH_in_gg(x1, x2) = leH_in_gg(x1, x2)
s(x1) = s(x1)
U5_gg(x1, x2, x3) = U5_gg(x1, x2, x3)
0 = 0
leH_out_gg(x1, x2) = leH_out_gg(x1, x2)
U13_gggga(x1, x2, x3, x4, x5, x6) = U13_gggga(x1, x2, x3, x4, x6)
U4_gga(x1, x2, x3, x4, x5, x6) = U4_gga(x1, x2, x3, x4, x6)
pG_in_gggga(x1, x2, x3, x4, x5) = pG_in_gggga(x1, x2, x3, x4)
U14_gggga(x1, x2, x3, x4, x5, x6) = U14_gggga(x1, x2, x3, x4, x6)
gtI_in_gg(x1, x2) = gtI_in_gg(x1, x2)
U6_gg(x1, x2, x3) = U6_gg(x1, x2, x3)
gtI_out_gg(x1, x2) = gtI_out_gg(x1, x2)
U15_gggga(x1, x2, x3, x4, x5, x6) = U15_gggga(x1, x2, x3, x4, x6)
pG_out_gggga(x1, x2, x3, x4, x5) = pG_out_gggga(x1, x2, x3, x4, x5)
pF_out_gggga(x1, x2, x3, x4, x5) = pF_out_gggga(x1, x2, x3, x4, x5)
pK_out_gaga(x1, x2, x3, x4) = pK_out_gaga(x1, x2, x3, x4)
pB_out_gagaa(x1, x2, x3, x4, x5) = pB_out_gagaa(x1, x2, x3, x4, x5)
U2_ga(x1, x2, x3, x4, x5, x6) = U2_ga(x1, x2, x3, x4, x6)
pC_in_gaaggagaa(x1, x2, x3, x4, x5, x6, x7, x8, x9) = pC_in_gaaggagaa(x1, x4, x5, x7)
U16_gaaggagaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10) = U16_gaaggagaa(x1, x4, x5, x7, x10)
splitJ_in_gaa(x1, x2, x3) = splitJ_in_gaa(x1)
splitJ_out_gaa(x1, x2, x3) = splitJ_out_gaa(x1, x2, x3)
U7_gaa(x1, x2, x3, x4, x5) = U7_gaa(x1, x2, x5)
U17_gaaggagaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10) = U17_gaaggagaa(x1, x2, x3, x4, x5, x7, x10)
pL_in_gggaggaa(x1, x2, x3, x4, x5, x6, x7, x8) = pL_in_gggaggaa(x1, x2, x3, x5, x6)
U18_gggaggaa(x1, x2, x3, x4, x5, x6, x7, x8, x9) = U18_gggaggaa(x1, x2, x3, x5, x6, x9)
U19_gggaggaa(x1, x2, x3, x4, x5, x6, x7, x8, x9) = U19_gggaggaa(x1, x2, x3, x4, x5, x6, x9)
pM_in_ggaga(x1, x2, x3, x4, x5) = pM_in_ggaga(x1, x2, x4)
U20_ggaga(x1, x2, x3, x4, x5, x6) = U20_ggaga(x1, x2, x4, x6)
U21_ggaga(x1, x2, x3, x4, x5, x6) = U21_ggaga(x1, x2, x3, x4, x6)
pM_out_ggaga(x1, x2, x3, x4, x5) = pM_out_ggaga(x1, x2, x3, x4, x5)
pL_out_gggaggaa(x1, x2, x3, x4, x5, x6, x7, x8) = pL_out_gggaggaa(x1, x2, x3, x4, x5, x6, x7, x8)
pC_out_gaaggagaa(x1, x2, x3, x4, x5, x6, x7, x8, x9) = pC_out_gaaggagaa(x1, x2, x3, x4, x5, x6, x7, x8, x9)
MERGESORTA_IN_GA(x1, x2) = MERGESORTA_IN_GA(x1)
U1_GA(x1, x2, x3, x4) = U1_GA(x1, x2, x4)
PB_IN_GAGAA(x1, x2, x3, x4, x5) = PB_IN_GAGAA(x1, x3)
U8_GAGAA(x1, x2, x3, x4, x5, x6) = U8_GAGAA(x1, x3, x6)
MERGESORTD_IN_GA(x1, x2) = MERGESORTD_IN_GA(x1)
U9_GAGAA(x1, x2, x3, x4, x5, x6) = U9_GAGAA(x1, x2, x3, x6)
PK_IN_GAGA(x1, x2, x3, x4) = PK_IN_GAGA(x1, x3)
U10_GAGA(x1, x2, x3, x4, x5) = U10_GAGA(x1, x3, x5)
U11_GAGA(x1, x2, x3, x4, x5) = U11_GAGA(x1, x2, x3, x5)
MERGEE_IN_GGA(x1, x2, x3) = MERGEE_IN_GGA(x1, x2)
U3_GGA(x1, x2, x3, x4, x5, x6) = U3_GGA(x1, x2, x3, x4, x6)
PF_IN_GGGGA(x1, x2, x3, x4, x5) = PF_IN_GGGGA(x1, x2, x3, x4)
U12_GGGGA(x1, x2, x3, x4, x5, x6) = U12_GGGGA(x1, x2, x3, x4, x6)
LEH_IN_GG(x1, x2) = LEH_IN_GG(x1, x2)
U5_GG(x1, x2, x3) = U5_GG(x1, x2, x3)
U13_GGGGA(x1, x2, x3, x4, x5, x6) = U13_GGGGA(x1, x2, x3, x4, x6)
U4_GGA(x1, x2, x3, x4, x5, x6) = U4_GGA(x1, x2, x3, x4, x6)
PG_IN_GGGGA(x1, x2, x3, x4, x5) = PG_IN_GGGGA(x1, x2, x3, x4)
U14_GGGGA(x1, x2, x3, x4, x5, x6) = U14_GGGGA(x1, x2, x3, x4, x6)
GTI_IN_GG(x1, x2) = GTI_IN_GG(x1, x2)
U6_GG(x1, x2, x3) = U6_GG(x1, x2, x3)
U15_GGGGA(x1, x2, x3, x4, x5, x6) = U15_GGGGA(x1, x2, x3, x4, x6)
U2_GA(x1, x2, x3, x4, x5, x6) = U2_GA(x1, x2, x3, x4, x6)
PC_IN_GAAGGAGAA(x1, x2, x3, x4, x5, x6, x7, x8, x9) = PC_IN_GAAGGAGAA(x1, x4, x5, x7)
U16_GAAGGAGAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10) = U16_GAAGGAGAA(x1, x4, x5, x7, x10)
SPLITJ_IN_GAA(x1, x2, x3) = SPLITJ_IN_GAA(x1)
U7_GAA(x1, x2, x3, x4, x5) = U7_GAA(x1, x2, x5)
U17_GAAGGAGAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10) = U17_GAAGGAGAA(x1, x2, x3, x4, x5, x7, x10)
PL_IN_GGGAGGAA(x1, x2, x3, x4, x5, x6, x7, x8) = PL_IN_GGGAGGAA(x1, x2, x3, x5, x6)
U18_GGGAGGAA(x1, x2, x3, x4, x5, x6, x7, x8, x9) = U18_GGGAGGAA(x1, x2, x3, x5, x6, x9)
U19_GGGAGGAA(x1, x2, x3, x4, x5, x6, x7, x8, x9) = U19_GGGAGGAA(x1, x2, x3, x4, x5, x6, x9)
PM_IN_GGAGA(x1, x2, x3, x4, x5) = PM_IN_GGAGA(x1, x2, x4)
U20_GGAGA(x1, x2, x3, x4, x5, x6) = U20_GGAGA(x1, x2, x4, x6)
U21_GGAGA(x1, x2, x3, x4, x5, x6) = U21_GGAGA(x1, x2, x3, x4, x6)

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(.(T10, .(T11, [])), T14) → U1_GA(T10, T11, T14, pB_in_gagaa(T10, X22, T11, X23, T14))
MERGESORTA_IN_GA(.(T10, .(T11, [])), T14) → PB_IN_GAGAA(T10, X22, T11, X23, T14)
PB_IN_GAGAA(T10, T15, T11, X23, T14) → U8_GAGAA(T10, T15, T11, X23, T14, mergesortD_in_ga(T10, T15))
PB_IN_GAGAA(T10, T15, T11, X23, T14) → MERGESORTD_IN_GA(T10, T15)
U8_GAGAA(T10, T15, T11, X23, T14, mergesortD_out_ga(T10, T15)) → U9_GAGAA(T10, T15, T11, X23, T14, pK_in_gaga(T11, X23, T15, T14))
U8_GAGAA(T10, T15, T11, X23, T14, mergesortD_out_ga(T10, T15)) → PK_IN_GAGA(T11, X23, T15, T14)
PK_IN_GAGA(T11, T22, T15, T14) → U10_GAGA(T11, T22, T15, T14, mergesortD_in_ga(T11, T22))
PK_IN_GAGA(T11, T22, T15, T14) → MERGESORTD_IN_GA(T11, T22)
U10_GAGA(T11, T22, T15, T14, mergesortD_out_ga(T11, T22)) → U11_GAGA(T11, T22, T15, T14, mergeE_in_gga(T15, T22, T14))
U10_GAGA(T11, T22, T15, T14, mergesortD_out_ga(T11, T22)) → MERGEE_IN_GGA(T15, T22, T14)
MERGEE_IN_GGA(.(T55, T56), .(T57, T58), .(T55, T60)) → U3_GGA(T55, T56, T57, T58, T60, pF_in_gggga(T55, T57, T56, T58, T60))
MERGEE_IN_GGA(.(T55, T56), .(T57, T58), .(T55, T60)) → PF_IN_GGGGA(T55, T57, T56, T58, T60)
PF_IN_GGGGA(T55, T57, T56, T58, T60) → U12_GGGGA(T55, T57, T56, T58, T60, leH_in_gg(T55, T57))
PF_IN_GGGGA(T55, T57, T56, T58, T60) → LEH_IN_GG(T55, T57)
LEH_IN_GG(s(T73), s(T74)) → U5_GG(T73, T74, leH_in_gg(T73, T74))
LEH_IN_GG(s(T73), s(T74)) → LEH_IN_GG(T73, T74)
U12_GGGGA(T55, T57, T56, T58, T60, leH_out_gg(T55, T57)) → U13_GGGGA(T55, T57, T56, T58, T60, mergeE_in_gga(T56, .(T57, T58), T60))
U12_GGGGA(T55, T57, T56, T58, T60, leH_out_gg(T55, T57)) → MERGEE_IN_GGA(T56, .(T57, T58), T60)
MERGEE_IN_GGA(.(T94, T95), .(T96, T97), .(T96, T99)) → U4_GGA(T94, T95, T96, T97, T99, pG_in_gggga(T94, T96, T95, T97, T99))
MERGEE_IN_GGA(.(T94, T95), .(T96, T97), .(T96, T99)) → PG_IN_GGGGA(T94, T96, T95, T97, T99)
PG_IN_GGGGA(T94, T96, T95, T97, T99) → U14_GGGGA(T94, T96, T95, T97, T99, gtI_in_gg(T94, T96))
PG_IN_GGGGA(T94, T96, T95, T97, T99) → GTI_IN_GG(T94, T96)
GTI_IN_GG(s(T112), s(T113)) → U6_GG(T112, T113, gtI_in_gg(T112, T113))
GTI_IN_GG(s(T112), s(T113)) → GTI_IN_GG(T112, T113)
U14_GGGGA(T94, T96, T95, T97, T99, gtI_out_gg(T94, T96)) → U15_GGGGA(T94, T96, T95, T97, T99, mergeE_in_gga(.(T94, T95), T97, T99))
U14_GGGGA(T94, T96, T95, T97, T99, gtI_out_gg(T94, T96)) → MERGEE_IN_GGA(.(T94, T95), T97, T99)
MERGESORTA_IN_GA(.(T10, .(T11, .(T127, T128))), T14) → U2_GA(T10, T11, T127, T128, T14, pC_in_gaaggagaa(T128, X146, X145, T10, T127, X22, T11, X23, T14))
MERGESORTA_IN_GA(.(T10, .(T11, .(T127, T128))), T14) → PC_IN_GAAGGAGAA(T128, X146, X145, T10, T127, X22, T11, X23, T14)
PC_IN_GAAGGAGAA(T128, T129, T130, T10, T127, X22, T11, X23, T14) → U16_GAAGGAGAA(T128, T129, T130, T10, T127, X22, T11, X23, T14, splitJ_in_gaa(T128, T129, T130))
PC_IN_GAAGGAGAA(T128, T129, T130, T10, T127, X22, T11, X23, T14) → SPLITJ_IN_GAA(T128, T129, T130)
SPLITJ_IN_GAA(.(T135, T136), .(T135, X163), X164) → U7_GAA(T135, T136, X163, X164, splitJ_in_gaa(T136, X164, X163))
SPLITJ_IN_GAA(.(T135, T136), .(T135, X163), X164) → SPLITJ_IN_GAA(T136, X164, X163)
U16_GAAGGAGAA(T128, T129, T130, T10, T127, X22, T11, X23, T14, splitJ_out_gaa(T128, T129, T130)) → U17_GAAGGAGAA(T128, T129, T130, T10, T127, X22, T11, X23, T14, pL_in_gggaggaa(T10, T127, T130, X22, T11, T129, X23, T14))
U16_GAAGGAGAA(T128, T129, T130, T10, T127, X22, T11, X23, T14, splitJ_out_gaa(T128, T129, T130)) → PL_IN_GGGAGGAA(T10, T127, T130, X22, T11, T129, X23, T14)
PL_IN_GGGAGGAA(T10, T127, T130, T137, T11, T129, X23, T14) → U18_GGGAGGAA(T10, T127, T130, T137, T11, T129, X23, T14, mergesortA_in_ga(.(T10, .(T127, T130)), T137))
PL_IN_GGGAGGAA(T10, T127, T130, T137, T11, T129, X23, T14) → MERGESORTA_IN_GA(.(T10, .(T127, T130)), T137)
U18_GGGAGGAA(T10, T127, T130, T137, T11, T129, X23, T14, mergesortA_out_ga(.(T10, .(T127, T130)), T137)) → U19_GGGAGGAA(T10, T127, T130, T137, T11, T129, X23, T14, pM_in_ggaga(T11, T129, X23, T137, T14))
U18_GGGAGGAA(T10, T127, T130, T137, T11, T129, X23, T14, mergesortA_out_ga(.(T10, .(T127, T130)), T137)) → PM_IN_GGAGA(T11, T129, X23, T137, T14)
PM_IN_GGAGA(T11, T129, T138, T137, T14) → U20_GGAGA(T11, T129, T138, T137, T14, mergesortA_in_ga(.(T11, T129), T138))
PM_IN_GGAGA(T11, T129, T138, T137, T14) → MERGESORTA_IN_GA(.(T11, T129), T138)
U20_GGAGA(T11, T129, T138, T137, T14, mergesortA_out_ga(.(T11, T129), T138)) → U21_GGAGA(T11, T129, T138, T137, T14, mergeE_in_gga(T137, T138, T14))
U20_GGAGA(T11, T129, T138, T137, T14, mergesortA_out_ga(.(T11, T129), T138)) → MERGEE_IN_GGA(T137, T138, 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(.(T10, .(T11, [])), T14) → U1_ga(T10, T11, T14, pB_in_gagaa(T10, X22, T11, X23, T14))
pB_in_gagaa(T10, T15, T11, X23, T14) → U8_gagaa(T10, T15, T11, X23, T14, mergesortD_in_ga(T10, T15))
mergesortD_in_ga(T20, .(T20, [])) → mergesortD_out_ga(T20, .(T20, []))
U8_gagaa(T10, T15, T11, X23, T14, mergesortD_out_ga(T10, T15)) → U9_gagaa(T10, T15, T11, X23, T14, pK_in_gaga(T11, X23, T15, T14))
pK_in_gaga(T11, T22, T15, T14) → U10_gaga(T11, T22, T15, T14, mergesortD_in_ga(T11, T22))
U10_gaga(T11, T22, T15, T14, mergesortD_out_ga(T11, T22)) → U11_gaga(T11, T22, T15, T14, mergeE_in_gga(T15, T22, T14))
mergeE_in_gga(T29, [], T29) → mergeE_out_gga(T29, [], T29)
mergeE_in_gga([], T34, T34) → mergeE_out_gga([], T34, T34)
mergeE_in_gga(.(T55, T56), .(T57, T58), .(T55, T60)) → U3_gga(T55, T56, T57, T58, T60, pF_in_gggga(T55, T57, T56, T58, T60))
pF_in_gggga(T55, T57, T56, T58, T60) → U12_gggga(T55, T57, T56, T58, T60, leH_in_gg(T55, T57))
leH_in_gg(s(T73), s(T74)) → U5_gg(T73, T74, leH_in_gg(T73, T74))
leH_in_gg(0, s(T81)) → leH_out_gg(0, s(T81))
leH_in_gg(0, 0) → leH_out_gg(0, 0)
U5_gg(T73, T74, leH_out_gg(T73, T74)) → leH_out_gg(s(T73), s(T74))
U12_gggga(T55, T57, T56, T58, T60, leH_out_gg(T55, T57)) → U13_gggga(T55, T57, T56, T58, T60, mergeE_in_gga(T56, .(T57, T58), T60))
mergeE_in_gga(.(T94, T95), .(T96, T97), .(T96, T99)) → U4_gga(T94, T95, T96, T97, T99, pG_in_gggga(T94, T96, T95, T97, T99))
pG_in_gggga(T94, T96, T95, T97, T99) → U14_gggga(T94, T96, T95, T97, T99, gtI_in_gg(T94, T96))
gtI_in_gg(s(T112), s(T113)) → U6_gg(T112, T113, gtI_in_gg(T112, T113))
gtI_in_gg(s(T118), 0) → gtI_out_gg(s(T118), 0)
U6_gg(T112, T113, gtI_out_gg(T112, T113)) → gtI_out_gg(s(T112), s(T113))
U14_gggga(T94, T96, T95, T97, T99, gtI_out_gg(T94, T96)) → U15_gggga(T94, T96, T95, T97, T99, mergeE_in_gga(.(T94, T95), T97, T99))
U15_gggga(T94, T96, T95, T97, T99, mergeE_out_gga(.(T94, T95), T97, T99)) → pG_out_gggga(T94, T96, T95, T97, T99)
U4_gga(T94, T95, T96, T97, T99, pG_out_gggga(T94, T96, T95, T97, T99)) → mergeE_out_gga(.(T94, T95), .(T96, T97), .(T96, T99))
U13_gggga(T55, T57, T56, T58, T60, mergeE_out_gga(T56, .(T57, T58), T60)) → pF_out_gggga(T55, T57, T56, T58, T60)
U3_gga(T55, T56, T57, T58, T60, pF_out_gggga(T55, T57, T56, T58, T60)) → mergeE_out_gga(.(T55, T56), .(T57, T58), .(T55, T60))
U11_gaga(T11, T22, T15, T14, mergeE_out_gga(T15, T22, T14)) → pK_out_gaga(T11, T22, T15, T14)
U9_gagaa(T10, T15, T11, X23, T14, pK_out_gaga(T11, X23, T15, T14)) → pB_out_gagaa(T10, T15, T11, X23, T14)
U1_ga(T10, T11, T14, pB_out_gagaa(T10, X22, T11, X23, T14)) → mergesortA_out_ga(.(T10, .(T11, [])), T14)
mergesortA_in_ga(.(T10, .(T11, .(T127, T128))), T14) → U2_ga(T10, T11, T127, T128, T14, pC_in_gaaggagaa(T128, X146, X145, T10, T127, X22, T11, X23, T14))
pC_in_gaaggagaa(T128, T129, T130, T10, T127, X22, T11, X23, T14) → U16_gaaggagaa(T128, T129, T130, T10, T127, X22, T11, X23, T14, splitJ_in_gaa(T128, T129, T130))
splitJ_in_gaa([], [], []) → splitJ_out_gaa([], [], [])
splitJ_in_gaa(.(T135, T136), .(T135, X163), X164) → U7_gaa(T135, T136, X163, X164, splitJ_in_gaa(T136, X164, X163))
U7_gaa(T135, T136, X163, X164, splitJ_out_gaa(T136, X164, X163)) → splitJ_out_gaa(.(T135, T136), .(T135, X163), X164)
U16_gaaggagaa(T128, T129, T130, T10, T127, X22, T11, X23, T14, splitJ_out_gaa(T128, T129, T130)) → U17_gaaggagaa(T128, T129, T130, T10, T127, X22, T11, X23, T14, pL_in_gggaggaa(T10, T127, T130, X22, T11, T129, X23, T14))
pL_in_gggaggaa(T10, T127, T130, T137, T11, T129, X23, T14) → U18_gggaggaa(T10, T127, T130, T137, T11, T129, X23, T14, mergesortA_in_ga(.(T10, .(T127, T130)), T137))
U18_gggaggaa(T10, T127, T130, T137, T11, T129, X23, T14, mergesortA_out_ga(.(T10, .(T127, T130)), T137)) → U19_gggaggaa(T10, T127, T130, T137, T11, T129, X23, T14, pM_in_ggaga(T11, T129, X23, T137, T14))
pM_in_ggaga(T11, T129, T138, T137, T14) → U20_ggaga(T11, T129, T138, T137, T14, mergesortA_in_ga(.(T11, T129), T138))
U20_ggaga(T11, T129, T138, T137, T14, mergesortA_out_ga(.(T11, T129), T138)) → U21_ggaga(T11, T129, T138, T137, T14, mergeE_in_gga(T137, T138, T14))
U21_ggaga(T11, T129, T138, T137, T14, mergeE_out_gga(T137, T138, T14)) → pM_out_ggaga(T11, T129, T138, T137, T14)
U19_gggaggaa(T10, T127, T130, T137, T11, T129, X23, T14, pM_out_ggaga(T11, T129, X23, T137, T14)) → pL_out_gggaggaa(T10, T127, T130, T137, T11, T129, X23, T14)
U17_gaaggagaa(T128, T129, T130, T10, T127, X22, T11, X23, T14, pL_out_gggaggaa(T10, T127, T130, X22, T11, T129, X23, T14)) → pC_out_gaaggagaa(T128, T129, T130, T10, T127, X22, T11, X23, T14)
U2_ga(T10, T11, T127, T128, T14, pC_out_gaaggagaa(T128, X146, X145, T10, T127, X22, T11, X23, T14)) → mergesortA_out_ga(.(T10, .(T11, .(T127, T128))), T14)

(5) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 5 SCCs with 26 less nodes.

(6) Complex Obligation (AND)

(7) Obligation:

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

SPLITJ_IN_GAA(.(T135, T136), .(T135, X163), X164) → SPLITJ_IN_GAA(T136, X164, X163)

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(.(T10, .(T11, [])), T14) → U1_ga(T10, T11, T14, pB_in_gagaa(T10, X22, T11, X23, T14))
pB_in_gagaa(T10, T15, T11, X23, T14) → U8_gagaa(T10, T15, T11, X23, T14, mergesortD_in_ga(T10, T15))
mergesortD_in_ga(T20, .(T20, [])) → mergesortD_out_ga(T20, .(T20, []))
U8_gagaa(T10, T15, T11, X23, T14, mergesortD_out_ga(T10, T15)) → U9_gagaa(T10, T15, T11, X23, T14, pK_in_gaga(T11, X23, T15, T14))
pK_in_gaga(T11, T22, T15, T14) → U10_gaga(T11, T22, T15, T14, mergesortD_in_ga(T11, T22))
U10_gaga(T11, T22, T15, T14, mergesortD_out_ga(T11, T22)) → U11_gaga(T11, T22, T15, T14, mergeE_in_gga(T15, T22, T14))
mergeE_in_gga(T29, [], T29) → mergeE_out_gga(T29, [], T29)
mergeE_in_gga([], T34, T34) → mergeE_out_gga([], T34, T34)
mergeE_in_gga(.(T55, T56), .(T57, T58), .(T55, T60)) → U3_gga(T55, T56, T57, T58, T60, pF_in_gggga(T55, T57, T56, T58, T60))
pF_in_gggga(T55, T57, T56, T58, T60) → U12_gggga(T55, T57, T56, T58, T60, leH_in_gg(T55, T57))
leH_in_gg(s(T73), s(T74)) → U5_gg(T73, T74, leH_in_gg(T73, T74))
leH_in_gg(0, s(T81)) → leH_out_gg(0, s(T81))
leH_in_gg(0, 0) → leH_out_gg(0, 0)
U5_gg(T73, T74, leH_out_gg(T73, T74)) → leH_out_gg(s(T73), s(T74))
U12_gggga(T55, T57, T56, T58, T60, leH_out_gg(T55, T57)) → U13_gggga(T55, T57, T56, T58, T60, mergeE_in_gga(T56, .(T57, T58), T60))
mergeE_in_gga(.(T94, T95), .(T96, T97), .(T96, T99)) → U4_gga(T94, T95, T96, T97, T99, pG_in_gggga(T94, T96, T95, T97, T99))
pG_in_gggga(T94, T96, T95, T97, T99) → U14_gggga(T94, T96, T95, T97, T99, gtI_in_gg(T94, T96))
gtI_in_gg(s(T112), s(T113)) → U6_gg(T112, T113, gtI_in_gg(T112, T113))
gtI_in_gg(s(T118), 0) → gtI_out_gg(s(T118), 0)
U6_gg(T112, T113, gtI_out_gg(T112, T113)) → gtI_out_gg(s(T112), s(T113))
U14_gggga(T94, T96, T95, T97, T99, gtI_out_gg(T94, T96)) → U15_gggga(T94, T96, T95, T97, T99, mergeE_in_gga(.(T94, T95), T97, T99))
U15_gggga(T94, T96, T95, T97, T99, mergeE_out_gga(.(T94, T95), T97, T99)) → pG_out_gggga(T94, T96, T95, T97, T99)
U4_gga(T94, T95, T96, T97, T99, pG_out_gggga(T94, T96, T95, T97, T99)) → mergeE_out_gga(.(T94, T95), .(T96, T97), .(T96, T99))
U13_gggga(T55, T57, T56, T58, T60, mergeE_out_gga(T56, .(T57, T58), T60)) → pF_out_gggga(T55, T57, T56, T58, T60)
U3_gga(T55, T56, T57, T58, T60, pF_out_gggga(T55, T57, T56, T58, T60)) → mergeE_out_gga(.(T55, T56), .(T57, T58), .(T55, T60))
U11_gaga(T11, T22, T15, T14, mergeE_out_gga(T15, T22, T14)) → pK_out_gaga(T11, T22, T15, T14)
U9_gagaa(T10, T15, T11, X23, T14, pK_out_gaga(T11, X23, T15, T14)) → pB_out_gagaa(T10, T15, T11, X23, T14)
U1_ga(T10, T11, T14, pB_out_gagaa(T10, X22, T11, X23, T14)) → mergesortA_out_ga(.(T10, .(T11, [])), T14)
mergesortA_in_ga(.(T10, .(T11, .(T127, T128))), T14) → U2_ga(T10, T11, T127, T128, T14, pC_in_gaaggagaa(T128, X146, X145, T10, T127, X22, T11, X23, T14))
pC_in_gaaggagaa(T128, T129, T130, T10, T127, X22, T11, X23, T14) → U16_gaaggagaa(T128, T129, T130, T10, T127, X22, T11, X23, T14, splitJ_in_gaa(T128, T129, T130))
splitJ_in_gaa([], [], []) → splitJ_out_gaa([], [], [])
splitJ_in_gaa(.(T135, T136), .(T135, X163), X164) → U7_gaa(T135, T136, X163, X164, splitJ_in_gaa(T136, X164, X163))
U7_gaa(T135, T136, X163, X164, splitJ_out_gaa(T136, X164, X163)) → splitJ_out_gaa(.(T135, T136), .(T135, X163), X164)
U16_gaaggagaa(T128, T129, T130, T10, T127, X22, T11, X23, T14, splitJ_out_gaa(T128, T129, T130)) → U17_gaaggagaa(T128, T129, T130, T10, T127, X22, T11, X23, T14, pL_in_gggaggaa(T10, T127, T130, X22, T11, T129, X23, T14))
pL_in_gggaggaa(T10, T127, T130, T137, T11, T129, X23, T14) → U18_gggaggaa(T10, T127, T130, T137, T11, T129, X23, T14, mergesortA_in_ga(.(T10, .(T127, T130)), T137))
U18_gggaggaa(T10, T127, T130, T137, T11, T129, X23, T14, mergesortA_out_ga(.(T10, .(T127, T130)), T137)) → U19_gggaggaa(T10, T127, T130, T137, T11, T129, X23, T14, pM_in_ggaga(T11, T129, X23, T137, T14))
pM_in_ggaga(T11, T129, T138, T137, T14) → U20_ggaga(T11, T129, T138, T137, T14, mergesortA_in_ga(.(T11, T129), T138))
U20_ggaga(T11, T129, T138, T137, T14, mergesortA_out_ga(.(T11, T129), T138)) → U21_ggaga(T11, T129, T138, T137, T14, mergeE_in_gga(T137, T138, T14))
U21_ggaga(T11, T129, T138, T137, T14, mergeE_out_gga(T137, T138, T14)) → pM_out_ggaga(T11, T129, T138, T137, T14)
U19_gggaggaa(T10, T127, T130, T137, T11, T129, X23, T14, pM_out_ggaga(T11, T129, X23, T137, T14)) → pL_out_gggaggaa(T10, T127, T130, T137, T11, T129, X23, T14)
U17_gaaggagaa(T128, T129, T130, T10, T127, X22, T11, X23, T14, pL_out_gggaggaa(T10, T127, T130, X22, T11, T129, X23, T14)) → pC_out_gaaggagaa(T128, T129, T130, T10, T127, X22, T11, X23, T14)
U2_ga(T10, T11, T127, T128, T14, pC_out_gaaggagaa(T128, X146, X145, T10, T127, X22, T11, X23, T14)) → mergesortA_out_ga(.(T10, .(T11, .(T127, T128))), 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:

SPLITJ_IN_GAA(.(T135, T136), .(T135, X163), X164) → SPLITJ_IN_GAA(T136, X164, X163)

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

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:

SPLITJ_IN_GAA(.(T135, T136)) → SPLITJ_IN_GAA(T136)

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:

SPLITJ_IN_GAA(.(T135, T136)) → SPLITJ_IN_GAA(T136)
The graph contains the following edges 1 > 1

(13) YES

(14) Obligation:

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

GTI_IN_GG(s(T112), s(T113)) → GTI_IN_GG(T112, T113)

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(.(T10, .(T11, [])), T14) → U1_ga(T10, T11, T14, pB_in_gagaa(T10, X22, T11, X23, T14))
pB_in_gagaa(T10, T15, T11, X23, T14) → U8_gagaa(T10, T15, T11, X23, T14, mergesortD_in_ga(T10, T15))
mergesortD_in_ga(T20, .(T20, [])) → mergesortD_out_ga(T20, .(T20, []))
U8_gagaa(T10, T15, T11, X23, T14, mergesortD_out_ga(T10, T15)) → U9_gagaa(T10, T15, T11, X23, T14, pK_in_gaga(T11, X23, T15, T14))
pK_in_gaga(T11, T22, T15, T14) → U10_gaga(T11, T22, T15, T14, mergesortD_in_ga(T11, T22))
U10_gaga(T11, T22, T15, T14, mergesortD_out_ga(T11, T22)) → U11_gaga(T11, T22, T15, T14, mergeE_in_gga(T15, T22, T14))
mergeE_in_gga(T29, [], T29) → mergeE_out_gga(T29, [], T29)
mergeE_in_gga([], T34, T34) → mergeE_out_gga([], T34, T34)
mergeE_in_gga(.(T55, T56), .(T57, T58), .(T55, T60)) → U3_gga(T55, T56, T57, T58, T60, pF_in_gggga(T55, T57, T56, T58, T60))
pF_in_gggga(T55, T57, T56, T58, T60) → U12_gggga(T55, T57, T56, T58, T60, leH_in_gg(T55, T57))
leH_in_gg(s(T73), s(T74)) → U5_gg(T73, T74, leH_in_gg(T73, T74))
leH_in_gg(0, s(T81)) → leH_out_gg(0, s(T81))
leH_in_gg(0, 0) → leH_out_gg(0, 0)
U5_gg(T73, T74, leH_out_gg(T73, T74)) → leH_out_gg(s(T73), s(T74))
U12_gggga(T55, T57, T56, T58, T60, leH_out_gg(T55, T57)) → U13_gggga(T55, T57, T56, T58, T60, mergeE_in_gga(T56, .(T57, T58), T60))
mergeE_in_gga(.(T94, T95), .(T96, T97), .(T96, T99)) → U4_gga(T94, T95, T96, T97, T99, pG_in_gggga(T94, T96, T95, T97, T99))
pG_in_gggga(T94, T96, T95, T97, T99) → U14_gggga(T94, T96, T95, T97, T99, gtI_in_gg(T94, T96))
gtI_in_gg(s(T112), s(T113)) → U6_gg(T112, T113, gtI_in_gg(T112, T113))
gtI_in_gg(s(T118), 0) → gtI_out_gg(s(T118), 0)
U6_gg(T112, T113, gtI_out_gg(T112, T113)) → gtI_out_gg(s(T112), s(T113))
U14_gggga(T94, T96, T95, T97, T99, gtI_out_gg(T94, T96)) → U15_gggga(T94, T96, T95, T97, T99, mergeE_in_gga(.(T94, T95), T97, T99))
U15_gggga(T94, T96, T95, T97, T99, mergeE_out_gga(.(T94, T95), T97, T99)) → pG_out_gggga(T94, T96, T95, T97, T99)
U4_gga(T94, T95, T96, T97, T99, pG_out_gggga(T94, T96, T95, T97, T99)) → mergeE_out_gga(.(T94, T95), .(T96, T97), .(T96, T99))
U13_gggga(T55, T57, T56, T58, T60, mergeE_out_gga(T56, .(T57, T58), T60)) → pF_out_gggga(T55, T57, T56, T58, T60)
U3_gga(T55, T56, T57, T58, T60, pF_out_gggga(T55, T57, T56, T58, T60)) → mergeE_out_gga(.(T55, T56), .(T57, T58), .(T55, T60))
U11_gaga(T11, T22, T15, T14, mergeE_out_gga(T15, T22, T14)) → pK_out_gaga(T11, T22, T15, T14)
U9_gagaa(T10, T15, T11, X23, T14, pK_out_gaga(T11, X23, T15, T14)) → pB_out_gagaa(T10, T15, T11, X23, T14)
U1_ga(T10, T11, T14, pB_out_gagaa(T10, X22, T11, X23, T14)) → mergesortA_out_ga(.(T10, .(T11, [])), T14)
mergesortA_in_ga(.(T10, .(T11, .(T127, T128))), T14) → U2_ga(T10, T11, T127, T128, T14, pC_in_gaaggagaa(T128, X146, X145, T10, T127, X22, T11, X23, T14))
pC_in_gaaggagaa(T128, T129, T130, T10, T127, X22, T11, X23, T14) → U16_gaaggagaa(T128, T129, T130, T10, T127, X22, T11, X23, T14, splitJ_in_gaa(T128, T129, T130))
splitJ_in_gaa([], [], []) → splitJ_out_gaa([], [], [])
splitJ_in_gaa(.(T135, T136), .(T135, X163), X164) → U7_gaa(T135, T136, X163, X164, splitJ_in_gaa(T136, X164, X163))
U7_gaa(T135, T136, X163, X164, splitJ_out_gaa(T136, X164, X163)) → splitJ_out_gaa(.(T135, T136), .(T135, X163), X164)
U16_gaaggagaa(T128, T129, T130, T10, T127, X22, T11, X23, T14, splitJ_out_gaa(T128, T129, T130)) → U17_gaaggagaa(T128, T129, T130, T10, T127, X22, T11, X23, T14, pL_in_gggaggaa(T10, T127, T130, X22, T11, T129, X23, T14))
pL_in_gggaggaa(T10, T127, T130, T137, T11, T129, X23, T14) → U18_gggaggaa(T10, T127, T130, T137, T11, T129, X23, T14, mergesortA_in_ga(.(T10, .(T127, T130)), T137))
U18_gggaggaa(T10, T127, T130, T137, T11, T129, X23, T14, mergesortA_out_ga(.(T10, .(T127, T130)), T137)) → U19_gggaggaa(T10, T127, T130, T137, T11, T129, X23, T14, pM_in_ggaga(T11, T129, X23, T137, T14))
pM_in_ggaga(T11, T129, T138, T137, T14) → U20_ggaga(T11, T129, T138, T137, T14, mergesortA_in_ga(.(T11, T129), T138))
U20_ggaga(T11, T129, T138, T137, T14, mergesortA_out_ga(.(T11, T129), T138)) → U21_ggaga(T11, T129, T138, T137, T14, mergeE_in_gga(T137, T138, T14))
U21_ggaga(T11, T129, T138, T137, T14, mergeE_out_gga(T137, T138, T14)) → pM_out_ggaga(T11, T129, T138, T137, T14)
U19_gggaggaa(T10, T127, T130, T137, T11, T129, X23, T14, pM_out_ggaga(T11, T129, X23, T137, T14)) → pL_out_gggaggaa(T10, T127, T130, T137, T11, T129, X23, T14)
U17_gaaggagaa(T128, T129, T130, T10, T127, X22, T11, X23, T14, pL_out_gggaggaa(T10, T127, T130, X22, T11, T129, X23, T14)) → pC_out_gaaggagaa(T128, T129, T130, T10, T127, X22, T11, X23, T14)
U2_ga(T10, T11, T127, T128, T14, pC_out_gaaggagaa(T128, X146, X145, T10, T127, X22, T11, X23, T14)) → mergesortA_out_ga(.(T10, .(T11, .(T127, T128))), 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:

GTI_IN_GG(s(T112), s(T113)) → GTI_IN_GG(T112, T113)

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

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

GTI_IN_GG(s(T112), s(T113)) → GTI_IN_GG(T112, T113)

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:

GTI_IN_GG(s(T112), s(T113)) → GTI_IN_GG(T112, T113)
The graph contains the following edges 1 > 1, 2 > 2

(20) YES

(21) Obligation:

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

LEH_IN_GG(s(T73), s(T74)) → LEH_IN_GG(T73, T74)

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(.(T10, .(T11, [])), T14) → U1_ga(T10, T11, T14, pB_in_gagaa(T10, X22, T11, X23, T14))
pB_in_gagaa(T10, T15, T11, X23, T14) → U8_gagaa(T10, T15, T11, X23, T14, mergesortD_in_ga(T10, T15))
mergesortD_in_ga(T20, .(T20, [])) → mergesortD_out_ga(T20, .(T20, []))
U8_gagaa(T10, T15, T11, X23, T14, mergesortD_out_ga(T10, T15)) → U9_gagaa(T10, T15, T11, X23, T14, pK_in_gaga(T11, X23, T15, T14))
pK_in_gaga(T11, T22, T15, T14) → U10_gaga(T11, T22, T15, T14, mergesortD_in_ga(T11, T22))
U10_gaga(T11, T22, T15, T14, mergesortD_out_ga(T11, T22)) → U11_gaga(T11, T22, T15, T14, mergeE_in_gga(T15, T22, T14))
mergeE_in_gga(T29, [], T29) → mergeE_out_gga(T29, [], T29)
mergeE_in_gga([], T34, T34) → mergeE_out_gga([], T34, T34)
mergeE_in_gga(.(T55, T56), .(T57, T58), .(T55, T60)) → U3_gga(T55, T56, T57, T58, T60, pF_in_gggga(T55, T57, T56, T58, T60))
pF_in_gggga(T55, T57, T56, T58, T60) → U12_gggga(T55, T57, T56, T58, T60, leH_in_gg(T55, T57))
leH_in_gg(s(T73), s(T74)) → U5_gg(T73, T74, leH_in_gg(T73, T74))
leH_in_gg(0, s(T81)) → leH_out_gg(0, s(T81))
leH_in_gg(0, 0) → leH_out_gg(0, 0)
U5_gg(T73, T74, leH_out_gg(T73, T74)) → leH_out_gg(s(T73), s(T74))
U12_gggga(T55, T57, T56, T58, T60, leH_out_gg(T55, T57)) → U13_gggga(T55, T57, T56, T58, T60, mergeE_in_gga(T56, .(T57, T58), T60))
mergeE_in_gga(.(T94, T95), .(T96, T97), .(T96, T99)) → U4_gga(T94, T95, T96, T97, T99, pG_in_gggga(T94, T96, T95, T97, T99))
pG_in_gggga(T94, T96, T95, T97, T99) → U14_gggga(T94, T96, T95, T97, T99, gtI_in_gg(T94, T96))
gtI_in_gg(s(T112), s(T113)) → U6_gg(T112, T113, gtI_in_gg(T112, T113))
gtI_in_gg(s(T118), 0) → gtI_out_gg(s(T118), 0)
U6_gg(T112, T113, gtI_out_gg(T112, T113)) → gtI_out_gg(s(T112), s(T113))
U14_gggga(T94, T96, T95, T97, T99, gtI_out_gg(T94, T96)) → U15_gggga(T94, T96, T95, T97, T99, mergeE_in_gga(.(T94, T95), T97, T99))
U15_gggga(T94, T96, T95, T97, T99, mergeE_out_gga(.(T94, T95), T97, T99)) → pG_out_gggga(T94, T96, T95, T97, T99)
U4_gga(T94, T95, T96, T97, T99, pG_out_gggga(T94, T96, T95, T97, T99)) → mergeE_out_gga(.(T94, T95), .(T96, T97), .(T96, T99))
U13_gggga(T55, T57, T56, T58, T60, mergeE_out_gga(T56, .(T57, T58), T60)) → pF_out_gggga(T55, T57, T56, T58, T60)
U3_gga(T55, T56, T57, T58, T60, pF_out_gggga(T55, T57, T56, T58, T60)) → mergeE_out_gga(.(T55, T56), .(T57, T58), .(T55, T60))
U11_gaga(T11, T22, T15, T14, mergeE_out_gga(T15, T22, T14)) → pK_out_gaga(T11, T22, T15, T14)
U9_gagaa(T10, T15, T11, X23, T14, pK_out_gaga(T11, X23, T15, T14)) → pB_out_gagaa(T10, T15, T11, X23, T14)
U1_ga(T10, T11, T14, pB_out_gagaa(T10, X22, T11, X23, T14)) → mergesortA_out_ga(.(T10, .(T11, [])), T14)
mergesortA_in_ga(.(T10, .(T11, .(T127, T128))), T14) → U2_ga(T10, T11, T127, T128, T14, pC_in_gaaggagaa(T128, X146, X145, T10, T127, X22, T11, X23, T14))
pC_in_gaaggagaa(T128, T129, T130, T10, T127, X22, T11, X23, T14) → U16_gaaggagaa(T128, T129, T130, T10, T127, X22, T11, X23, T14, splitJ_in_gaa(T128, T129, T130))
splitJ_in_gaa([], [], []) → splitJ_out_gaa([], [], [])
splitJ_in_gaa(.(T135, T136), .(T135, X163), X164) → U7_gaa(T135, T136, X163, X164, splitJ_in_gaa(T136, X164, X163))
U7_gaa(T135, T136, X163, X164, splitJ_out_gaa(T136, X164, X163)) → splitJ_out_gaa(.(T135, T136), .(T135, X163), X164)
U16_gaaggagaa(T128, T129, T130, T10, T127, X22, T11, X23, T14, splitJ_out_gaa(T128, T129, T130)) → U17_gaaggagaa(T128, T129, T130, T10, T127, X22, T11, X23, T14, pL_in_gggaggaa(T10, T127, T130, X22, T11, T129, X23, T14))
pL_in_gggaggaa(T10, T127, T130, T137, T11, T129, X23, T14) → U18_gggaggaa(T10, T127, T130, T137, T11, T129, X23, T14, mergesortA_in_ga(.(T10, .(T127, T130)), T137))
U18_gggaggaa(T10, T127, T130, T137, T11, T129, X23, T14, mergesortA_out_ga(.(T10, .(T127, T130)), T137)) → U19_gggaggaa(T10, T127, T130, T137, T11, T129, X23, T14, pM_in_ggaga(T11, T129, X23, T137, T14))
pM_in_ggaga(T11, T129, T138, T137, T14) → U20_ggaga(T11, T129, T138, T137, T14, mergesortA_in_ga(.(T11, T129), T138))
U20_ggaga(T11, T129, T138, T137, T14, mergesortA_out_ga(.(T11, T129), T138)) → U21_ggaga(T11, T129, T138, T137, T14, mergeE_in_gga(T137, T138, T14))
U21_ggaga(T11, T129, T138, T137, T14, mergeE_out_gga(T137, T138, T14)) → pM_out_ggaga(T11, T129, T138, T137, T14)
U19_gggaggaa(T10, T127, T130, T137, T11, T129, X23, T14, pM_out_ggaga(T11, T129, X23, T137, T14)) → pL_out_gggaggaa(T10, T127, T130, T137, T11, T129, X23, T14)
U17_gaaggagaa(T128, T129, T130, T10, T127, X22, T11, X23, T14, pL_out_gggaggaa(T10, T127, T130, X22, T11, T129, X23, T14)) → pC_out_gaaggagaa(T128, T129, T130, T10, T127, X22, T11, X23, T14)
U2_ga(T10, T11, T127, T128, T14, pC_out_gaaggagaa(T128, X146, X145, T10, T127, X22, T11, X23, T14)) → mergesortA_out_ga(.(T10, .(T11, .(T127, T128))), 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:

LEH_IN_GG(s(T73), s(T74)) → LEH_IN_GG(T73, T74)

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

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

LEH_IN_GG(s(T73), s(T74)) → LEH_IN_GG(T73, T74)

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

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

LEH_IN_GG(s(T73), s(T74)) → LEH_IN_GG(T73, T74)
The graph contains the following edges 1 > 1, 2 > 2

(27) YES

(28) Obligation:

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

MERGEE_IN_GGA(.(T55, T56), .(T57, T58), .(T55, T60)) → PF_IN_GGGGA(T55, T57, T56, T58, T60)
PF_IN_GGGGA(T55, T57, T56, T58, T60) → U12_GGGGA(T55, T57, T56, T58, T60, leH_in_gg(T55, T57))
U12_GGGGA(T55, T57, T56, T58, T60, leH_out_gg(T55, T57)) → MERGEE_IN_GGA(T56, .(T57, T58), T60)
MERGEE_IN_GGA(.(T94, T95), .(T96, T97), .(T96, T99)) → PG_IN_GGGGA(T94, T96, T95, T97, T99)
PG_IN_GGGGA(T94, T96, T95, T97, T99) → U14_GGGGA(T94, T96, T95, T97, T99, gtI_in_gg(T94, T96))
U14_GGGGA(T94, T96, T95, T97, T99, gtI_out_gg(T94, T96)) → MERGEE_IN_GGA(.(T94, T95), T97, T99)

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(.(T10, .(T11, [])), T14) → U1_ga(T10, T11, T14, pB_in_gagaa(T10, X22, T11, X23, T14))
pB_in_gagaa(T10, T15, T11, X23, T14) → U8_gagaa(T10, T15, T11, X23, T14, mergesortD_in_ga(T10, T15))
mergesortD_in_ga(T20, .(T20, [])) → mergesortD_out_ga(T20, .(T20, []))
U8_gagaa(T10, T15, T11, X23, T14, mergesortD_out_ga(T10, T15)) → U9_gagaa(T10, T15, T11, X23, T14, pK_in_gaga(T11, X23, T15, T14))
pK_in_gaga(T11, T22, T15, T14) → U10_gaga(T11, T22, T15, T14, mergesortD_in_ga(T11, T22))
U10_gaga(T11, T22, T15, T14, mergesortD_out_ga(T11, T22)) → U11_gaga(T11, T22, T15, T14, mergeE_in_gga(T15, T22, T14))
mergeE_in_gga(T29, [], T29) → mergeE_out_gga(T29, [], T29)
mergeE_in_gga([], T34, T34) → mergeE_out_gga([], T34, T34)
mergeE_in_gga(.(T55, T56), .(T57, T58), .(T55, T60)) → U3_gga(T55, T56, T57, T58, T60, pF_in_gggga(T55, T57, T56, T58, T60))
pF_in_gggga(T55, T57, T56, T58, T60) → U12_gggga(T55, T57, T56, T58, T60, leH_in_gg(T55, T57))
leH_in_gg(s(T73), s(T74)) → U5_gg(T73, T74, leH_in_gg(T73, T74))
leH_in_gg(0, s(T81)) → leH_out_gg(0, s(T81))
leH_in_gg(0, 0) → leH_out_gg(0, 0)
U5_gg(T73, T74, leH_out_gg(T73, T74)) → leH_out_gg(s(T73), s(T74))
U12_gggga(T55, T57, T56, T58, T60, leH_out_gg(T55, T57)) → U13_gggga(T55, T57, T56, T58, T60, mergeE_in_gga(T56, .(T57, T58), T60))
mergeE_in_gga(.(T94, T95), .(T96, T97), .(T96, T99)) → U4_gga(T94, T95, T96, T97, T99, pG_in_gggga(T94, T96, T95, T97, T99))
pG_in_gggga(T94, T96, T95, T97, T99) → U14_gggga(T94, T96, T95, T97, T99, gtI_in_gg(T94, T96))
gtI_in_gg(s(T112), s(T113)) → U6_gg(T112, T113, gtI_in_gg(T112, T113))
gtI_in_gg(s(T118), 0) → gtI_out_gg(s(T118), 0)
U6_gg(T112, T113, gtI_out_gg(T112, T113)) → gtI_out_gg(s(T112), s(T113))
U14_gggga(T94, T96, T95, T97, T99, gtI_out_gg(T94, T96)) → U15_gggga(T94, T96, T95, T97, T99, mergeE_in_gga(.(T94, T95), T97, T99))
U15_gggga(T94, T96, T95, T97, T99, mergeE_out_gga(.(T94, T95), T97, T99)) → pG_out_gggga(T94, T96, T95, T97, T99)
U4_gga(T94, T95, T96, T97, T99, pG_out_gggga(T94, T96, T95, T97, T99)) → mergeE_out_gga(.(T94, T95), .(T96, T97), .(T96, T99))
U13_gggga(T55, T57, T56, T58, T60, mergeE_out_gga(T56, .(T57, T58), T60)) → pF_out_gggga(T55, T57, T56, T58, T60)
U3_gga(T55, T56, T57, T58, T60, pF_out_gggga(T55, T57, T56, T58, T60)) → mergeE_out_gga(.(T55, T56), .(T57, T58), .(T55, T60))
U11_gaga(T11, T22, T15, T14, mergeE_out_gga(T15, T22, T14)) → pK_out_gaga(T11, T22, T15, T14)
U9_gagaa(T10, T15, T11, X23, T14, pK_out_gaga(T11, X23, T15, T14)) → pB_out_gagaa(T10, T15, T11, X23, T14)
U1_ga(T10, T11, T14, pB_out_gagaa(T10, X22, T11, X23, T14)) → mergesortA_out_ga(.(T10, .(T11, [])), T14)
mergesortA_in_ga(.(T10, .(T11, .(T127, T128))), T14) → U2_ga(T10, T11, T127, T128, T14, pC_in_gaaggagaa(T128, X146, X145, T10, T127, X22, T11, X23, T14))
pC_in_gaaggagaa(T128, T129, T130, T10, T127, X22, T11, X23, T14) → U16_gaaggagaa(T128, T129, T130, T10, T127, X22, T11, X23, T14, splitJ_in_gaa(T128, T129, T130))
splitJ_in_gaa([], [], []) → splitJ_out_gaa([], [], [])
splitJ_in_gaa(.(T135, T136), .(T135, X163), X164) → U7_gaa(T135, T136, X163, X164, splitJ_in_gaa(T136, X164, X163))
U7_gaa(T135, T136, X163, X164, splitJ_out_gaa(T136, X164, X163)) → splitJ_out_gaa(.(T135, T136), .(T135, X163), X164)
U16_gaaggagaa(T128, T129, T130, T10, T127, X22, T11, X23, T14, splitJ_out_gaa(T128, T129, T130)) → U17_gaaggagaa(T128, T129, T130, T10, T127, X22, T11, X23, T14, pL_in_gggaggaa(T10, T127, T130, X22, T11, T129, X23, T14))
pL_in_gggaggaa(T10, T127, T130, T137, T11, T129, X23, T14) → U18_gggaggaa(T10, T127, T130, T137, T11, T129, X23, T14, mergesortA_in_ga(.(T10, .(T127, T130)), T137))
U18_gggaggaa(T10, T127, T130, T137, T11, T129, X23, T14, mergesortA_out_ga(.(T10, .(T127, T130)), T137)) → U19_gggaggaa(T10, T127, T130, T137, T11, T129, X23, T14, pM_in_ggaga(T11, T129, X23, T137, T14))
pM_in_ggaga(T11, T129, T138, T137, T14) → U20_ggaga(T11, T129, T138, T137, T14, mergesortA_in_ga(.(T11, T129), T138))
U20_ggaga(T11, T129, T138, T137, T14, mergesortA_out_ga(.(T11, T129), T138)) → U21_ggaga(T11, T129, T138, T137, T14, mergeE_in_gga(T137, T138, T14))
U21_ggaga(T11, T129, T138, T137, T14, mergeE_out_gga(T137, T138, T14)) → pM_out_ggaga(T11, T129, T138, T137, T14)
U19_gggaggaa(T10, T127, T130, T137, T11, T129, X23, T14, pM_out_ggaga(T11, T129, X23, T137, T14)) → pL_out_gggaggaa(T10, T127, T130, T137, T11, T129, X23, T14)
U17_gaaggagaa(T128, T129, T130, T10, T127, X22, T11, X23, T14, pL_out_gggaggaa(T10, T127, T130, X22, T11, T129, X23, T14)) → pC_out_gaaggagaa(T128, T129, T130, T10, T127, X22, T11, X23, T14)
U2_ga(T10, T11, T127, T128, T14, pC_out_gaaggagaa(T128, X146, X145, T10, T127, X22, T11, X23, T14)) → mergesortA_out_ga(.(T10, .(T11, .(T127, T128))), T14)

(29) UsableRulesProof (EQUIVALENT transformation)

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

(30) Obligation:

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

MERGEE_IN_GGA(.(T55, T56), .(T57, T58), .(T55, T60)) → PF_IN_GGGGA(T55, T57, T56, T58, T60)
PF_IN_GGGGA(T55, T57, T56, T58, T60) → U12_GGGGA(T55, T57, T56, T58, T60, leH_in_gg(T55, T57))
U12_GGGGA(T55, T57, T56, T58, T60, leH_out_gg(T55, T57)) → MERGEE_IN_GGA(T56, .(T57, T58), T60)
MERGEE_IN_GGA(.(T94, T95), .(T96, T97), .(T96, T99)) → PG_IN_GGGGA(T94, T96, T95, T97, T99)
PG_IN_GGGGA(T94, T96, T95, T97, T99) → U14_GGGGA(T94, T96, T95, T97, T99, gtI_in_gg(T94, T96))
U14_GGGGA(T94, T96, T95, T97, T99, gtI_out_gg(T94, T96)) → MERGEE_IN_GGA(.(T94, T95), T97, T99)

The TRS R consists of the following rules:

leH_in_gg(s(T73), s(T74)) → U5_gg(T73, T74, leH_in_gg(T73, T74))
leH_in_gg(0, s(T81)) → leH_out_gg(0, s(T81))
leH_in_gg(0, 0) → leH_out_gg(0, 0)
gtI_in_gg(s(T112), s(T113)) → U6_gg(T112, T113, gtI_in_gg(T112, T113))
gtI_in_gg(s(T118), 0) → gtI_out_gg(s(T118), 0)
U5_gg(T73, T74, leH_out_gg(T73, T74)) → leH_out_gg(s(T73), s(T74))
U6_gg(T112, T113, gtI_out_gg(T112, T113)) → gtI_out_gg(s(T112), s(T113))

The argument filtering Pi contains the following mapping:
.(x1, x2) = .(x1, x2)
leH_in_gg(x1, x2) = leH_in_gg(x1, x2)
s(x1) = s(x1)
U5_gg(x1, x2, x3) = U5_gg(x1, x2, x3)
0 = 0
leH_out_gg(x1, x2) = leH_out_gg(x1, x2)
gtI_in_gg(x1, x2) = gtI_in_gg(x1, x2)
U6_gg(x1, x2, x3) = U6_gg(x1, x2, x3)
gtI_out_gg(x1, x2) = gtI_out_gg(x1, x2)
MERGEE_IN_GGA(x1, x2, x3) = MERGEE_IN_GGA(x1, x2)
PF_IN_GGGGA(x1, x2, x3, x4, x5) = PF_IN_GGGGA(x1, x2, x3, x4)
U12_GGGGA(x1, x2, x3, x4, x5, x6) = U12_GGGGA(x1, x2, x3, x4, x6)
PG_IN_GGGGA(x1, x2, x3, x4, x5) = PG_IN_GGGGA(x1, x2, x3, x4)
U14_GGGGA(x1, x2, x3, x4, x5, x6) = U14_GGGGA(x1, x2, x3, x4, x6)

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

(31) PiDPToQDPProof (SOUND transformation)

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

(32) Obligation:

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

MERGEE_IN_GGA(.(T55, T56), .(T57, T58)) → PF_IN_GGGGA(T55, T57, T56, T58)
PF_IN_GGGGA(T55, T57, T56, T58) → U12_GGGGA(T55, T57, T56, T58, leH_in_gg(T55, T57))
U12_GGGGA(T55, T57, T56, T58, leH_out_gg(T55, T57)) → MERGEE_IN_GGA(T56, .(T57, T58))
MERGEE_IN_GGA(.(T94, T95), .(T96, T97)) → PG_IN_GGGGA(T94, T96, T95, T97)
PG_IN_GGGGA(T94, T96, T95, T97) → U14_GGGGA(T94, T96, T95, T97, gtI_in_gg(T94, T96))
U14_GGGGA(T94, T96, T95, T97, gtI_out_gg(T94, T96)) → MERGEE_IN_GGA(.(T94, T95), T97)

The TRS R consists of the following rules:

leH_in_gg(s(T73), s(T74)) → U5_gg(T73, T74, leH_in_gg(T73, T74))
leH_in_gg(0, s(T81)) → leH_out_gg(0, s(T81))
leH_in_gg(0, 0) → leH_out_gg(0, 0)
gtI_in_gg(s(T112), s(T113)) → U6_gg(T112, T113, gtI_in_gg(T112, T113))
gtI_in_gg(s(T118), 0) → gtI_out_gg(s(T118), 0)
U5_gg(T73, T74, leH_out_gg(T73, T74)) → leH_out_gg(s(T73), s(T74))
U6_gg(T112, T113, gtI_out_gg(T112, T113)) → gtI_out_gg(s(T112), s(T113))

The set Q consists of the following terms:

leH_in_gg(x0, x1)
gtI_in_gg(x0, x1)
U5_gg(x0, x1, x2)
U6_gg(x0, x1, x2)

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

(33) MRRProof (EQUIVALENT transformation)

By using the rule removal processor [LPAR04] with the following ordering, at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented.
Strictly oriented dependency pairs:

MERGEE_IN_GGA(.(T55, T56), .(T57, T58)) → PF_IN_GGGGA(T55, T57, T56, T58)
MERGEE_IN_GGA(.(T94, T95), .(T96, T97)) → PG_IN_GGGGA(T94, T96, T95, T97)

Used ordering: Polynomial interpretation [POLO]:

POL(.(x₁, x₂)) = 1 + 2·x₁ + 2·x₂
POL(0) = 0
POL(MERGEE_IN_GGA(x₁, x₂)) = x₁ + x₂
POL(PF_IN_GGGGA(x₁, x₂, x₃, x₄)) = 1 + 2·x₁ + 2·x₂ + 2·x₃ + 2·x₄
POL(PG_IN_GGGGA(x₁, x₂, x₃, x₄)) = 1 + 2·x₁ + 2·x₂ + 2·x₃ + 2·x₄
POL(U12_GGGGA(x₁, x₂, x₃, x₄, x₅)) = 1 + x₁ + x₂ + 2·x₃ + 2·x₄ + x₅
POL(U14_GGGGA(x₁, x₂, x₃, x₄, x₅)) = 1 + x₁ + x₂ + 2·x₃ + x₄ + x₅
POL(U5_gg(x₁, x₂, x₃)) = x₁ + x₂ + x₃
POL(U6_gg(x₁, x₂, x₃)) = x₁ + x₂ + x₃
POL(gtI_in_gg(x₁, x₂)) = x₁ + x₂
POL(gtI_out_gg(x₁, x₂)) = x₁ + x₂
POL(leH_in_gg(x₁, x₂)) = x₁ + x₂
POL(leH_out_gg(x₁, x₂)) = x₁ + x₂
POL(s(x₁)) = 2·x₁

(34) Obligation:

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

PF_IN_GGGGA(T55, T57, T56, T58) → U12_GGGGA(T55, T57, T56, T58, leH_in_gg(T55, T57))
U12_GGGGA(T55, T57, T56, T58, leH_out_gg(T55, T57)) → MERGEE_IN_GGA(T56, .(T57, T58))
PG_IN_GGGGA(T94, T96, T95, T97) → U14_GGGGA(T94, T96, T95, T97, gtI_in_gg(T94, T96))
U14_GGGGA(T94, T96, T95, T97, gtI_out_gg(T94, T96)) → MERGEE_IN_GGA(.(T94, T95), T97)

The TRS R consists of the following rules:

leH_in_gg(s(T73), s(T74)) → U5_gg(T73, T74, leH_in_gg(T73, T74))
leH_in_gg(0, s(T81)) → leH_out_gg(0, s(T81))
leH_in_gg(0, 0) → leH_out_gg(0, 0)
gtI_in_gg(s(T112), s(T113)) → U6_gg(T112, T113, gtI_in_gg(T112, T113))
gtI_in_gg(s(T118), 0) → gtI_out_gg(s(T118), 0)
U5_gg(T73, T74, leH_out_gg(T73, T74)) → leH_out_gg(s(T73), s(T74))
U6_gg(T112, T113, gtI_out_gg(T112, T113)) → gtI_out_gg(s(T112), s(T113))

The set Q consists of the following terms:

leH_in_gg(x0, x1)
gtI_in_gg(x0, x1)
U5_gg(x0, x1, x2)
U6_gg(x0, x1, x2)

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

(35) DependencyGraphProof (EQUIVALENT transformation)

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

(36) TRUE

(37) Obligation:

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

MERGESORTA_IN_GA(.(T10, .(T11, .(T127, T128))), T14) → PC_IN_GAAGGAGAA(T128, X146, X145, T10, T127, X22, T11, X23, T14)
PC_IN_GAAGGAGAA(T128, T129, T130, T10, T127, X22, T11, X23, T14) → U16_GAAGGAGAA(T128, T129, T130, T10, T127, X22, T11, X23, T14, splitJ_in_gaa(T128, T129, T130))
U16_GAAGGAGAA(T128, T129, T130, T10, T127, X22, T11, X23, T14, splitJ_out_gaa(T128, T129, T130)) → PL_IN_GGGAGGAA(T10, T127, T130, X22, T11, T129, X23, T14)
PL_IN_GGGAGGAA(T10, T127, T130, T137, T11, T129, X23, T14) → U18_GGGAGGAA(T10, T127, T130, T137, T11, T129, X23, T14, mergesortA_in_ga(.(T10, .(T127, T130)), T137))
U18_GGGAGGAA(T10, T127, T130, T137, T11, T129, X23, T14, mergesortA_out_ga(.(T10, .(T127, T130)), T137)) → PM_IN_GGAGA(T11, T129, X23, T137, T14)
PM_IN_GGAGA(T11, T129, T138, T137, T14) → MERGESORTA_IN_GA(.(T11, T129), T138)
PL_IN_GGGAGGAA(T10, T127, T130, T137, T11, T129, X23, T14) → MERGESORTA_IN_GA(.(T10, .(T127, T130)), T137)

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(.(T10, .(T11, [])), T14) → U1_ga(T10, T11, T14, pB_in_gagaa(T10, X22, T11, X23, T14))
pB_in_gagaa(T10, T15, T11, X23, T14) → U8_gagaa(T10, T15, T11, X23, T14, mergesortD_in_ga(T10, T15))
mergesortD_in_ga(T20, .(T20, [])) → mergesortD_out_ga(T20, .(T20, []))
U8_gagaa(T10, T15, T11, X23, T14, mergesortD_out_ga(T10, T15)) → U9_gagaa(T10, T15, T11, X23, T14, pK_in_gaga(T11, X23, T15, T14))
pK_in_gaga(T11, T22, T15, T14) → U10_gaga(T11, T22, T15, T14, mergesortD_in_ga(T11, T22))
U10_gaga(T11, T22, T15, T14, mergesortD_out_ga(T11, T22)) → U11_gaga(T11, T22, T15, T14, mergeE_in_gga(T15, T22, T14))
mergeE_in_gga(T29, [], T29) → mergeE_out_gga(T29, [], T29)
mergeE_in_gga([], T34, T34) → mergeE_out_gga([], T34, T34)
mergeE_in_gga(.(T55, T56), .(T57, T58), .(T55, T60)) → U3_gga(T55, T56, T57, T58, T60, pF_in_gggga(T55, T57, T56, T58, T60))
pF_in_gggga(T55, T57, T56, T58, T60) → U12_gggga(T55, T57, T56, T58, T60, leH_in_gg(T55, T57))
leH_in_gg(s(T73), s(T74)) → U5_gg(T73, T74, leH_in_gg(T73, T74))
leH_in_gg(0, s(T81)) → leH_out_gg(0, s(T81))
leH_in_gg(0, 0) → leH_out_gg(0, 0)
U5_gg(T73, T74, leH_out_gg(T73, T74)) → leH_out_gg(s(T73), s(T74))
U12_gggga(T55, T57, T56, T58, T60, leH_out_gg(T55, T57)) → U13_gggga(T55, T57, T56, T58, T60, mergeE_in_gga(T56, .(T57, T58), T60))
mergeE_in_gga(.(T94, T95), .(T96, T97), .(T96, T99)) → U4_gga(T94, T95, T96, T97, T99, pG_in_gggga(T94, T96, T95, T97, T99))
pG_in_gggga(T94, T96, T95, T97, T99) → U14_gggga(T94, T96, T95, T97, T99, gtI_in_gg(T94, T96))
gtI_in_gg(s(T112), s(T113)) → U6_gg(T112, T113, gtI_in_gg(T112, T113))
gtI_in_gg(s(T118), 0) → gtI_out_gg(s(T118), 0)
U6_gg(T112, T113, gtI_out_gg(T112, T113)) → gtI_out_gg(s(T112), s(T113))
U14_gggga(T94, T96, T95, T97, T99, gtI_out_gg(T94, T96)) → U15_gggga(T94, T96, T95, T97, T99, mergeE_in_gga(.(T94, T95), T97, T99))
U15_gggga(T94, T96, T95, T97, T99, mergeE_out_gga(.(T94, T95), T97, T99)) → pG_out_gggga(T94, T96, T95, T97, T99)
U4_gga(T94, T95, T96, T97, T99, pG_out_gggga(T94, T96, T95, T97, T99)) → mergeE_out_gga(.(T94, T95), .(T96, T97), .(T96, T99))
U13_gggga(T55, T57, T56, T58, T60, mergeE_out_gga(T56, .(T57, T58), T60)) → pF_out_gggga(T55, T57, T56, T58, T60)
U3_gga(T55, T56, T57, T58, T60, pF_out_gggga(T55, T57, T56, T58, T60)) → mergeE_out_gga(.(T55, T56), .(T57, T58), .(T55, T60))
U11_gaga(T11, T22, T15, T14, mergeE_out_gga(T15, T22, T14)) → pK_out_gaga(T11, T22, T15, T14)
U9_gagaa(T10, T15, T11, X23, T14, pK_out_gaga(T11, X23, T15, T14)) → pB_out_gagaa(T10, T15, T11, X23, T14)
U1_ga(T10, T11, T14, pB_out_gagaa(T10, X22, T11, X23, T14)) → mergesortA_out_ga(.(T10, .(T11, [])), T14)
mergesortA_in_ga(.(T10, .(T11, .(T127, T128))), T14) → U2_ga(T10, T11, T127, T128, T14, pC_in_gaaggagaa(T128, X146, X145, T10, T127, X22, T11, X23, T14))
pC_in_gaaggagaa(T128, T129, T130, T10, T127, X22, T11, X23, T14) → U16_gaaggagaa(T128, T129, T130, T10, T127, X22, T11, X23, T14, splitJ_in_gaa(T128, T129, T130))
splitJ_in_gaa([], [], []) → splitJ_out_gaa([], [], [])
splitJ_in_gaa(.(T135, T136), .(T135, X163), X164) → U7_gaa(T135, T136, X163, X164, splitJ_in_gaa(T136, X164, X163))
U7_gaa(T135, T136, X163, X164, splitJ_out_gaa(T136, X164, X163)) → splitJ_out_gaa(.(T135, T136), .(T135, X163), X164)
U16_gaaggagaa(T128, T129, T130, T10, T127, X22, T11, X23, T14, splitJ_out_gaa(T128, T129, T130)) → U17_gaaggagaa(T128, T129, T130, T10, T127, X22, T11, X23, T14, pL_in_gggaggaa(T10, T127, T130, X22, T11, T129, X23, T14))
pL_in_gggaggaa(T10, T127, T130, T137, T11, T129, X23, T14) → U18_gggaggaa(T10, T127, T130, T137, T11, T129, X23, T14, mergesortA_in_ga(.(T10, .(T127, T130)), T137))
U18_gggaggaa(T10, T127, T130, T137, T11, T129, X23, T14, mergesortA_out_ga(.(T10, .(T127, T130)), T137)) → U19_gggaggaa(T10, T127, T130, T137, T11, T129, X23, T14, pM_in_ggaga(T11, T129, X23, T137, T14))
pM_in_ggaga(T11, T129, T138, T137, T14) → U20_ggaga(T11, T129, T138, T137, T14, mergesortA_in_ga(.(T11, T129), T138))
U20_ggaga(T11, T129, T138, T137, T14, mergesortA_out_ga(.(T11, T129), T138)) → U21_ggaga(T11, T129, T138, T137, T14, mergeE_in_gga(T137, T138, T14))
U21_ggaga(T11, T129, T138, T137, T14, mergeE_out_gga(T137, T138, T14)) → pM_out_ggaga(T11, T129, T138, T137, T14)
U19_gggaggaa(T10, T127, T130, T137, T11, T129, X23, T14, pM_out_ggaga(T11, T129, X23, T137, T14)) → pL_out_gggaggaa(T10, T127, T130, T137, T11, T129, X23, T14)
U17_gaaggagaa(T128, T129, T130, T10, T127, X22, T11, X23, T14, pL_out_gggaggaa(T10, T127, T130, X22, T11, T129, X23, T14)) → pC_out_gaaggagaa(T128, T129, T130, T10, T127, X22, T11, X23, T14)
U2_ga(T10, T11, T127, T128, T14, pC_out_gaaggagaa(T128, X146, X145, T10, T127, X22, T11, X23, T14)) → mergesortA_out_ga(.(T10, .(T11, .(T127, T128))), T14)

(38) UsableRulesProof (EQUIVALENT transformation)

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

(39) Obligation:

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

MERGESORTA_IN_GA(.(T10, .(T11, .(T127, T128))), T14) → PC_IN_GAAGGAGAA(T128, X146, X145, T10, T127, X22, T11, X23, T14)
PC_IN_GAAGGAGAA(T128, T129, T130, T10, T127, X22, T11, X23, T14) → U16_GAAGGAGAA(T128, T129, T130, T10, T127, X22, T11, X23, T14, splitJ_in_gaa(T128, T129, T130))
U16_GAAGGAGAA(T128, T129, T130, T10, T127, X22, T11, X23, T14, splitJ_out_gaa(T128, T129, T130)) → PL_IN_GGGAGGAA(T10, T127, T130, X22, T11, T129, X23, T14)
PL_IN_GGGAGGAA(T10, T127, T130, T137, T11, T129, X23, T14) → U18_GGGAGGAA(T10, T127, T130, T137, T11, T129, X23, T14, mergesortA_in_ga(.(T10, .(T127, T130)), T137))
U18_GGGAGGAA(T10, T127, T130, T137, T11, T129, X23, T14, mergesortA_out_ga(.(T10, .(T127, T130)), T137)) → PM_IN_GGAGA(T11, T129, X23, T137, T14)
PM_IN_GGAGA(T11, T129, T138, T137, T14) → MERGESORTA_IN_GA(.(T11, T129), T138)
PL_IN_GGGAGGAA(T10, T127, T130, T137, T11, T129, X23, T14) → MERGESORTA_IN_GA(.(T10, .(T127, T130)), T137)

The TRS R consists of the following rules:

splitJ_in_gaa([], [], []) → splitJ_out_gaa([], [], [])
splitJ_in_gaa(.(T135, T136), .(T135, X163), X164) → U7_gaa(T135, T136, X163, X164, splitJ_in_gaa(T136, X164, X163))
mergesortA_in_ga(.(T10, .(T11, [])), T14) → U1_ga(T10, T11, T14, pB_in_gagaa(T10, X22, T11, X23, T14))
mergesortA_in_ga(.(T10, .(T11, .(T127, T128))), T14) → U2_ga(T10, T11, T127, T128, T14, pC_in_gaaggagaa(T128, X146, X145, T10, T127, X22, T11, X23, T14))
U7_gaa(T135, T136, X163, X164, splitJ_out_gaa(T136, X164, X163)) → splitJ_out_gaa(.(T135, T136), .(T135, X163), X164)
U1_ga(T10, T11, T14, pB_out_gagaa(T10, X22, T11, X23, T14)) → mergesortA_out_ga(.(T10, .(T11, [])), T14)
U2_ga(T10, T11, T127, T128, T14, pC_out_gaaggagaa(T128, X146, X145, T10, T127, X22, T11, X23, T14)) → mergesortA_out_ga(.(T10, .(T11, .(T127, T128))), T14)
pB_in_gagaa(T10, T15, T11, X23, T14) → U8_gagaa(T10, T15, T11, X23, T14, mergesortD_in_ga(T10, T15))
pC_in_gaaggagaa(T128, T129, T130, T10, T127, X22, T11, X23, T14) → U16_gaaggagaa(T128, T129, T130, T10, T127, X22, T11, X23, T14, splitJ_in_gaa(T128, T129, T130))
U8_gagaa(T10, T15, T11, X23, T14, mergesortD_out_ga(T10, T15)) → U9_gagaa(T10, T15, T11, X23, T14, pK_in_gaga(T11, X23, T15, T14))
U16_gaaggagaa(T128, T129, T130, T10, T127, X22, T11, X23, T14, splitJ_out_gaa(T128, T129, T130)) → U17_gaaggagaa(T128, T129, T130, T10, T127, X22, T11, X23, T14, pL_in_gggaggaa(T10, T127, T130, X22, T11, T129, X23, T14))
mergesortD_in_ga(T20, .(T20, [])) → mergesortD_out_ga(T20, .(T20, []))
U9_gagaa(T10, T15, T11, X23, T14, pK_out_gaga(T11, X23, T15, T14)) → pB_out_gagaa(T10, T15, T11, X23, T14)
U17_gaaggagaa(T128, T129, T130, T10, T127, X22, T11, X23, T14, pL_out_gggaggaa(T10, T127, T130, X22, T11, T129, X23, T14)) → pC_out_gaaggagaa(T128, T129, T130, T10, T127, X22, T11, X23, T14)
pK_in_gaga(T11, T22, T15, T14) → U10_gaga(T11, T22, T15, T14, mergesortD_in_ga(T11, T22))
pL_in_gggaggaa(T10, T127, T130, T137, T11, T129, X23, T14) → U18_gggaggaa(T10, T127, T130, T137, T11, T129, X23, T14, mergesortA_in_ga(.(T10, .(T127, T130)), T137))
U10_gaga(T11, T22, T15, T14, mergesortD_out_ga(T11, T22)) → U11_gaga(T11, T22, T15, T14, mergeE_in_gga(T15, T22, T14))
U18_gggaggaa(T10, T127, T130, T137, T11, T129, X23, T14, mergesortA_out_ga(.(T10, .(T127, T130)), T137)) → U19_gggaggaa(T10, T127, T130, T137, T11, T129, X23, T14, pM_in_ggaga(T11, T129, X23, T137, T14))
U11_gaga(T11, T22, T15, T14, mergeE_out_gga(T15, T22, T14)) → pK_out_gaga(T11, T22, T15, T14)
U19_gggaggaa(T10, T127, T130, T137, T11, T129, X23, T14, pM_out_ggaga(T11, T129, X23, T137, T14)) → pL_out_gggaggaa(T10, T127, T130, T137, T11, T129, X23, T14)
mergeE_in_gga(T29, [], T29) → mergeE_out_gga(T29, [], T29)
mergeE_in_gga([], T34, T34) → mergeE_out_gga([], T34, T34)
mergeE_in_gga(.(T55, T56), .(T57, T58), .(T55, T60)) → U3_gga(T55, T56, T57, T58, T60, pF_in_gggga(T55, T57, T56, T58, T60))
mergeE_in_gga(.(T94, T95), .(T96, T97), .(T96, T99)) → U4_gga(T94, T95, T96, T97, T99, pG_in_gggga(T94, T96, T95, T97, T99))
pM_in_ggaga(T11, T129, T138, T137, T14) → U20_ggaga(T11, T129, T138, T137, T14, mergesortA_in_ga(.(T11, T129), T138))
U3_gga(T55, T56, T57, T58, T60, pF_out_gggga(T55, T57, T56, T58, T60)) → mergeE_out_gga(.(T55, T56), .(T57, T58), .(T55, T60))
U4_gga(T94, T95, T96, T97, T99, pG_out_gggga(T94, T96, T95, T97, T99)) → mergeE_out_gga(.(T94, T95), .(T96, T97), .(T96, T99))
U20_ggaga(T11, T129, T138, T137, T14, mergesortA_out_ga(.(T11, T129), T138)) → U21_ggaga(T11, T129, T138, T137, T14, mergeE_in_gga(T137, T138, T14))
pF_in_gggga(T55, T57, T56, T58, T60) → U12_gggga(T55, T57, T56, T58, T60, leH_in_gg(T55, T57))
pG_in_gggga(T94, T96, T95, T97, T99) → U14_gggga(T94, T96, T95, T97, T99, gtI_in_gg(T94, T96))
mergesortA_in_ga(.(T4, []), .(T4, [])) → mergesortA_out_ga(.(T4, []), .(T4, []))
U21_ggaga(T11, T129, T138, T137, T14, mergeE_out_gga(T137, T138, T14)) → pM_out_ggaga(T11, T129, T138, T137, T14)
U12_gggga(T55, T57, T56, T58, T60, leH_out_gg(T55, T57)) → U13_gggga(T55, T57, T56, T58, T60, mergeE_in_gga(T56, .(T57, T58), T60))
U14_gggga(T94, T96, T95, T97, T99, gtI_out_gg(T94, T96)) → U15_gggga(T94, T96, T95, T97, T99, mergeE_in_gga(.(T94, T95), T97, T99))
leH_in_gg(s(T73), s(T74)) → U5_gg(T73, T74, leH_in_gg(T73, T74))
leH_in_gg(0, s(T81)) → leH_out_gg(0, s(T81))
leH_in_gg(0, 0) → leH_out_gg(0, 0)
U13_gggga(T55, T57, T56, T58, T60, mergeE_out_gga(T56, .(T57, T58), T60)) → pF_out_gggga(T55, T57, T56, T58, T60)
gtI_in_gg(s(T112), s(T113)) → U6_gg(T112, T113, gtI_in_gg(T112, T113))
gtI_in_gg(s(T118), 0) → gtI_out_gg(s(T118), 0)
U15_gggga(T94, T96, T95, T97, T99, mergeE_out_gga(.(T94, T95), T97, T99)) → pG_out_gggga(T94, T96, T95, T97, T99)
U5_gg(T73, T74, leH_out_gg(T73, T74)) → leH_out_gg(s(T73), s(T74))
U6_gg(T112, T113, gtI_out_gg(T112, T113)) → gtI_out_gg(s(T112), s(T113))

(40) PiDPToQDPProof (SOUND transformation)

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

(41) Obligation:

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

MERGESORTA_IN_GA(.(T10, .(T11, .(T127, T128)))) → PC_IN_GAAGGAGAA(T128, T10, T127, T11)
PC_IN_GAAGGAGAA(T128, T10, T127, T11) → U16_GAAGGAGAA(T128, T10, T127, T11, splitJ_in_gaa(T128))
U16_GAAGGAGAA(T128, T10, T127, T11, splitJ_out_gaa(T128, T129, T130)) → PL_IN_GGGAGGAA(T10, T127, T130, T11, T129)
PL_IN_GGGAGGAA(T10, T127, T130, T11, T129) → U18_GGGAGGAA(T10, T127, T130, T11, T129, mergesortA_in_ga(.(T10, .(T127, T130))))
U18_GGGAGGAA(T10, T127, T130, T11, T129, mergesortA_out_ga(.(T10, .(T127, T130)), T137)) → PM_IN_GGAGA(T11, T129, T137)
PM_IN_GGAGA(T11, T129, T137) → MERGESORTA_IN_GA(.(T11, T129))
PL_IN_GGGAGGAA(T10, T127, T130, T11, T129) → MERGESORTA_IN_GA(.(T10, .(T127, T130)))

The TRS R consists of the following rules:

splitJ_in_gaa([]) → splitJ_out_gaa([], [], [])
splitJ_in_gaa(.(T135, T136)) → U7_gaa(T135, T136, splitJ_in_gaa(T136))
mergesortA_in_ga(.(T10, .(T11, []))) → U1_ga(T10, T11, pB_in_gagaa(T10, T11))
mergesortA_in_ga(.(T10, .(T11, .(T127, T128)))) → U2_ga(T10, T11, T127, T128, pC_in_gaaggagaa(T128, T10, T127, T11))
U7_gaa(T135, T136, splitJ_out_gaa(T136, X164, X163)) → splitJ_out_gaa(.(T135, T136), .(T135, X163), X164)
U1_ga(T10, T11, pB_out_gagaa(T10, X22, T11, X23, T14)) → mergesortA_out_ga(.(T10, .(T11, [])), T14)
U2_ga(T10, T11, T127, T128, pC_out_gaaggagaa(T128, X146, X145, T10, T127, X22, T11, X23, T14)) → mergesortA_out_ga(.(T10, .(T11, .(T127, T128))), T14)
pB_in_gagaa(T10, T11) → U8_gagaa(T10, T11, mergesortD_in_ga(T10))
pC_in_gaaggagaa(T128, T10, T127, T11) → U16_gaaggagaa(T128, T10, T127, T11, splitJ_in_gaa(T128))
U8_gagaa(T10, T11, mergesortD_out_ga(T10, T15)) → U9_gagaa(T10, T15, T11, pK_in_gaga(T11, T15))
U16_gaaggagaa(T128, T10, T127, T11, splitJ_out_gaa(T128, T129, T130)) → U17_gaaggagaa(T128, T129, T130, T10, T127, T11, pL_in_gggaggaa(T10, T127, T130, T11, T129))
mergesortD_in_ga(T20) → mergesortD_out_ga(T20, .(T20, []))
U9_gagaa(T10, T15, T11, pK_out_gaga(T11, X23, T15, T14)) → pB_out_gagaa(T10, T15, T11, X23, T14)
U17_gaaggagaa(T128, T129, T130, T10, T127, T11, pL_out_gggaggaa(T10, T127, T130, X22, T11, T129, X23, T14)) → pC_out_gaaggagaa(T128, T129, T130, T10, T127, X22, T11, X23, T14)
pK_in_gaga(T11, T15) → U10_gaga(T11, T15, mergesortD_in_ga(T11))
pL_in_gggaggaa(T10, T127, T130, T11, T129) → U18_gggaggaa(T10, T127, T130, T11, T129, mergesortA_in_ga(.(T10, .(T127, T130))))
U10_gaga(T11, T15, mergesortD_out_ga(T11, T22)) → U11_gaga(T11, T22, T15, mergeE_in_gga(T15, T22))
U18_gggaggaa(T10, T127, T130, T11, T129, mergesortA_out_ga(.(T10, .(T127, T130)), T137)) → U19_gggaggaa(T10, T127, T130, T137, T11, T129, pM_in_ggaga(T11, T129, T137))
U11_gaga(T11, T22, T15, mergeE_out_gga(T15, T22, T14)) → pK_out_gaga(T11, T22, T15, T14)
U19_gggaggaa(T10, T127, T130, T137, T11, T129, pM_out_ggaga(T11, T129, X23, T137, T14)) → pL_out_gggaggaa(T10, T127, T130, T137, T11, T129, X23, T14)
mergeE_in_gga(T29, []) → mergeE_out_gga(T29, [], T29)
mergeE_in_gga([], T34) → mergeE_out_gga([], T34, T34)
mergeE_in_gga(.(T55, T56), .(T57, T58)) → U3_gga(T55, T56, T57, T58, pF_in_gggga(T55, T57, T56, T58))
mergeE_in_gga(.(T94, T95), .(T96, T97)) → U4_gga(T94, T95, T96, T97, pG_in_gggga(T94, T96, T95, T97))
pM_in_ggaga(T11, T129, T137) → U20_ggaga(T11, T129, T137, mergesortA_in_ga(.(T11, T129)))
U3_gga(T55, T56, T57, T58, pF_out_gggga(T55, T57, T56, T58, T60)) → mergeE_out_gga(.(T55, T56), .(T57, T58), .(T55, T60))
U4_gga(T94, T95, T96, T97, pG_out_gggga(T94, T96, T95, T97, T99)) → mergeE_out_gga(.(T94, T95), .(T96, T97), .(T96, T99))
U20_ggaga(T11, T129, T137, mergesortA_out_ga(.(T11, T129), T138)) → U21_ggaga(T11, T129, T138, T137, mergeE_in_gga(T137, T138))
pF_in_gggga(T55, T57, T56, T58) → U12_gggga(T55, T57, T56, T58, leH_in_gg(T55, T57))
pG_in_gggga(T94, T96, T95, T97) → U14_gggga(T94, T96, T95, T97, gtI_in_gg(T94, T96))
mergesortA_in_ga(.(T4, [])) → mergesortA_out_ga(.(T4, []), .(T4, []))
U21_ggaga(T11, T129, T138, T137, mergeE_out_gga(T137, T138, T14)) → pM_out_ggaga(T11, T129, T138, T137, T14)
U12_gggga(T55, T57, T56, T58, leH_out_gg(T55, T57)) → U13_gggga(T55, T57, T56, T58, mergeE_in_gga(T56, .(T57, T58)))
U14_gggga(T94, T96, T95, T97, gtI_out_gg(T94, T96)) → U15_gggga(T94, T96, T95, T97, mergeE_in_gga(.(T94, T95), T97))
leH_in_gg(s(T73), s(T74)) → U5_gg(T73, T74, leH_in_gg(T73, T74))
leH_in_gg(0, s(T81)) → leH_out_gg(0, s(T81))
leH_in_gg(0, 0) → leH_out_gg(0, 0)
U13_gggga(T55, T57, T56, T58, mergeE_out_gga(T56, .(T57, T58), T60)) → pF_out_gggga(T55, T57, T56, T58, T60)
gtI_in_gg(s(T112), s(T113)) → U6_gg(T112, T113, gtI_in_gg(T112, T113))
gtI_in_gg(s(T118), 0) → gtI_out_gg(s(T118), 0)
U15_gggga(T94, T96, T95, T97, mergeE_out_gga(.(T94, T95), T97, T99)) → pG_out_gggga(T94, T96, T95, T97, T99)
U5_gg(T73, T74, leH_out_gg(T73, T74)) → leH_out_gg(s(T73), s(T74))
U6_gg(T112, T113, gtI_out_gg(T112, T113)) → gtI_out_gg(s(T112), s(T113))

The set Q consists of the following terms:

splitJ_in_gaa(x0)
mergesortA_in_ga(x0)
U7_gaa(x0, x1, x2)
U1_ga(x0, x1, x2)
U2_ga(x0, x1, x2, x3, x4)
pB_in_gagaa(x0, x1)
pC_in_gaaggagaa(x0, x1, x2, x3)
U8_gagaa(x0, x1, x2)
U16_gaaggagaa(x0, x1, x2, x3, x4)
mergesortD_in_ga(x0)
U9_gagaa(x0, x1, x2, x3)
U17_gaaggagaa(x0, x1, x2, x3, x4, x5, x6)
pK_in_gaga(x0, x1)
pL_in_gggaggaa(x0, x1, x2, x3, x4)
U10_gaga(x0, x1, x2)
U18_gggaggaa(x0, x1, x2, x3, x4, x5)
U11_gaga(x0, x1, x2, x3)
U19_gggaggaa(x0, x1, x2, x3, x4, x5, x6)
mergeE_in_gga(x0, x1)
pM_in_ggaga(x0, x1, x2)
U3_gga(x0, x1, x2, x3, x4)
U4_gga(x0, x1, x2, x3, x4)
U20_ggaga(x0, x1, x2, x3)
pF_in_gggga(x0, x1, x2, x3)
pG_in_gggga(x0, x1, x2, x3)
U21_ggaga(x0, x1, x2, x3, x4)
U12_gggga(x0, x1, x2, x3, x4)
U14_gggga(x0, x1, x2, x3, x4)
leH_in_gg(x0, x1)
U13_gggga(x0, x1, x2, x3, x4)
gtI_in_gg(x0, x1)
U15_gggga(x0, x1, x2, x3, x4)
U5_gg(x0, x1, x2)
U6_gg(x0, x1, x2)

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

(42) QDPOrderProof (EQUIVALENT transformation)

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

The following pairs can be oriented strictly and are deleted.

MERGESORTA_IN_GA(.(T10, .(T11, .(T127, T128)))) → PC_IN_GAAGGAGAA(T128, T10, T127, T11)
PL_IN_GGGAGGAA(T10, T127, T130, T11, T129) → U18_GGGAGGAA(T10, T127, T130, T11, T129, mergesortA_in_ga(.(T10, .(T127, T130))))
U18_GGGAGGAA(T10, T127, T130, T11, T129, mergesortA_out_ga(.(T10, .(T127, T130)), T137)) → PM_IN_GGAGA(T11, T129, T137)

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

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

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

POL( U18_GGGAGGAA(x₁, ..., x₆) ) = x₁ + 2x₂ + x₃ + 2x₄ + 2x₅ + 1

POL( splitJ_in_gaa(x₁) ) = 2x₁ + 1

POL( [] ) = 0

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

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

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

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

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

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

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

POL( pC_in_gaaggagaa(x₁, ..., x₄) ) = 2x₁

POL( U17_gaaggagaa(x₁, ..., x₇) ) = max{0, 2x₁ + x₄ + x₅ - 2}

POL( pL_in_gggaggaa(x₁, ..., x₅) ) = 2x₁ + 1

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

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

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

POL( mergesortA_out_ga(x₁, x₂) ) = max{0, x₁ + x₂ - 1}

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

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

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

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

POL( U21_ggaga(x₁, ..., x₅) ) = max{0, x₁ + 2x₂ - 2}

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

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

POL( mergesortD_in_ga(x₁) ) = 2

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

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

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

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

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

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

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

POL( mergeE_out_gga(x₁, ..., x₃) ) = 2

POL( U3_gga(x₁, ..., x₅) ) = x₂ + 1

POL( pF_in_gggga(x₁, ..., x₄) ) = x₁ + 2x₄ + 1

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

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

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

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

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

POL( s(x₁) ) = 2x₁

POL( U5_gg(x₁, ..., x₃) ) = max{0, -1}

POL( 0 ) = 0

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

POL( U13_gggga(x₁, ..., x₅) ) = max{0, x₂ + 2x₅ - 2}

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

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

POL( gtI_in_gg(x₁, x₂) ) = 0

POL( U6_gg(x₁, ..., x₃) ) = max{0, -1}

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

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

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

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

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

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

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

splitJ_in_gaa([]) → splitJ_out_gaa([], [], [])
splitJ_in_gaa(.(T135, T136)) → U7_gaa(T135, T136, splitJ_in_gaa(T136))
U7_gaa(T135, T136, splitJ_out_gaa(T136, X164, X163)) → splitJ_out_gaa(.(T135, T136), .(T135, X163), X164)

(43) Obligation:

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

PC_IN_GAAGGAGAA(T128, T10, T127, T11) → U16_GAAGGAGAA(T128, T10, T127, T11, splitJ_in_gaa(T128))
U16_GAAGGAGAA(T128, T10, T127, T11, splitJ_out_gaa(T128, T129, T130)) → PL_IN_GGGAGGAA(T10, T127, T130, T11, T129)
PM_IN_GGAGA(T11, T129, T137) → MERGESORTA_IN_GA(.(T11, T129))
PL_IN_GGGAGGAA(T10, T127, T130, T11, T129) → MERGESORTA_IN_GA(.(T10, .(T127, T130)))

The TRS R consists of the following rules:

splitJ_in_gaa([]) → splitJ_out_gaa([], [], [])
splitJ_in_gaa(.(T135, T136)) → U7_gaa(T135, T136, splitJ_in_gaa(T136))
mergesortA_in_ga(.(T10, .(T11, []))) → U1_ga(T10, T11, pB_in_gagaa(T10, T11))
mergesortA_in_ga(.(T10, .(T11, .(T127, T128)))) → U2_ga(T10, T11, T127, T128, pC_in_gaaggagaa(T128, T10, T127, T11))
U7_gaa(T135, T136, splitJ_out_gaa(T136, X164, X163)) → splitJ_out_gaa(.(T135, T136), .(T135, X163), X164)
U1_ga(T10, T11, pB_out_gagaa(T10, X22, T11, X23, T14)) → mergesortA_out_ga(.(T10, .(T11, [])), T14)
U2_ga(T10, T11, T127, T128, pC_out_gaaggagaa(T128, X146, X145, T10, T127, X22, T11, X23, T14)) → mergesortA_out_ga(.(T10, .(T11, .(T127, T128))), T14)
pB_in_gagaa(T10, T11) → U8_gagaa(T10, T11, mergesortD_in_ga(T10))
pC_in_gaaggagaa(T128, T10, T127, T11) → U16_gaaggagaa(T128, T10, T127, T11, splitJ_in_gaa(T128))
U8_gagaa(T10, T11, mergesortD_out_ga(T10, T15)) → U9_gagaa(T10, T15, T11, pK_in_gaga(T11, T15))
U16_gaaggagaa(T128, T10, T127, T11, splitJ_out_gaa(T128, T129, T130)) → U17_gaaggagaa(T128, T129, T130, T10, T127, T11, pL_in_gggaggaa(T10, T127, T130, T11, T129))
mergesortD_in_ga(T20) → mergesortD_out_ga(T20, .(T20, []))
U9_gagaa(T10, T15, T11, pK_out_gaga(T11, X23, T15, T14)) → pB_out_gagaa(T10, T15, T11, X23, T14)
U17_gaaggagaa(T128, T129, T130, T10, T127, T11, pL_out_gggaggaa(T10, T127, T130, X22, T11, T129, X23, T14)) → pC_out_gaaggagaa(T128, T129, T130, T10, T127, X22, T11, X23, T14)
pK_in_gaga(T11, T15) → U10_gaga(T11, T15, mergesortD_in_ga(T11))
pL_in_gggaggaa(T10, T127, T130, T11, T129) → U18_gggaggaa(T10, T127, T130, T11, T129, mergesortA_in_ga(.(T10, .(T127, T130))))
U10_gaga(T11, T15, mergesortD_out_ga(T11, T22)) → U11_gaga(T11, T22, T15, mergeE_in_gga(T15, T22))
U18_gggaggaa(T10, T127, T130, T11, T129, mergesortA_out_ga(.(T10, .(T127, T130)), T137)) → U19_gggaggaa(T10, T127, T130, T137, T11, T129, pM_in_ggaga(T11, T129, T137))
U11_gaga(T11, T22, T15, mergeE_out_gga(T15, T22, T14)) → pK_out_gaga(T11, T22, T15, T14)
U19_gggaggaa(T10, T127, T130, T137, T11, T129, pM_out_ggaga(T11, T129, X23, T137, T14)) → pL_out_gggaggaa(T10, T127, T130, T137, T11, T129, X23, T14)
mergeE_in_gga(T29, []) → mergeE_out_gga(T29, [], T29)
mergeE_in_gga([], T34) → mergeE_out_gga([], T34, T34)
mergeE_in_gga(.(T55, T56), .(T57, T58)) → U3_gga(T55, T56, T57, T58, pF_in_gggga(T55, T57, T56, T58))
mergeE_in_gga(.(T94, T95), .(T96, T97)) → U4_gga(T94, T95, T96, T97, pG_in_gggga(T94, T96, T95, T97))
pM_in_ggaga(T11, T129, T137) → U20_ggaga(T11, T129, T137, mergesortA_in_ga(.(T11, T129)))
U3_gga(T55, T56, T57, T58, pF_out_gggga(T55, T57, T56, T58, T60)) → mergeE_out_gga(.(T55, T56), .(T57, T58), .(T55, T60))
U4_gga(T94, T95, T96, T97, pG_out_gggga(T94, T96, T95, T97, T99)) → mergeE_out_gga(.(T94, T95), .(T96, T97), .(T96, T99))
U20_ggaga(T11, T129, T137, mergesortA_out_ga(.(T11, T129), T138)) → U21_ggaga(T11, T129, T138, T137, mergeE_in_gga(T137, T138))
pF_in_gggga(T55, T57, T56, T58) → U12_gggga(T55, T57, T56, T58, leH_in_gg(T55, T57))
pG_in_gggga(T94, T96, T95, T97) → U14_gggga(T94, T96, T95, T97, gtI_in_gg(T94, T96))
mergesortA_in_ga(.(T4, [])) → mergesortA_out_ga(.(T4, []), .(T4, []))
U21_ggaga(T11, T129, T138, T137, mergeE_out_gga(T137, T138, T14)) → pM_out_ggaga(T11, T129, T138, T137, T14)
U12_gggga(T55, T57, T56, T58, leH_out_gg(T55, T57)) → U13_gggga(T55, T57, T56, T58, mergeE_in_gga(T56, .(T57, T58)))
U14_gggga(T94, T96, T95, T97, gtI_out_gg(T94, T96)) → U15_gggga(T94, T96, T95, T97, mergeE_in_gga(.(T94, T95), T97))
leH_in_gg(s(T73), s(T74)) → U5_gg(T73, T74, leH_in_gg(T73, T74))
leH_in_gg(0, s(T81)) → leH_out_gg(0, s(T81))
leH_in_gg(0, 0) → leH_out_gg(0, 0)
U13_gggga(T55, T57, T56, T58, mergeE_out_gga(T56, .(T57, T58), T60)) → pF_out_gggga(T55, T57, T56, T58, T60)
gtI_in_gg(s(T112), s(T113)) → U6_gg(T112, T113, gtI_in_gg(T112, T113))
gtI_in_gg(s(T118), 0) → gtI_out_gg(s(T118), 0)
U15_gggga(T94, T96, T95, T97, mergeE_out_gga(.(T94, T95), T97, T99)) → pG_out_gggga(T94, T96, T95, T97, T99)
U5_gg(T73, T74, leH_out_gg(T73, T74)) → leH_out_gg(s(T73), s(T74))
U6_gg(T112, T113, gtI_out_gg(T112, T113)) → gtI_out_gg(s(T112), s(T113))

The set Q consists of the following terms:

splitJ_in_gaa(x0)
mergesortA_in_ga(x0)
U7_gaa(x0, x1, x2)
U1_ga(x0, x1, x2)
U2_ga(x0, x1, x2, x3, x4)
pB_in_gagaa(x0, x1)
pC_in_gaaggagaa(x0, x1, x2, x3)
U8_gagaa(x0, x1, x2)
U16_gaaggagaa(x0, x1, x2, x3, x4)
mergesortD_in_ga(x0)
U9_gagaa(x0, x1, x2, x3)
U17_gaaggagaa(x0, x1, x2, x3, x4, x5, x6)
pK_in_gaga(x0, x1)
pL_in_gggaggaa(x0, x1, x2, x3, x4)
U10_gaga(x0, x1, x2)
U18_gggaggaa(x0, x1, x2, x3, x4, x5)
U11_gaga(x0, x1, x2, x3)
U19_gggaggaa(x0, x1, x2, x3, x4, x5, x6)
mergeE_in_gga(x0, x1)
pM_in_ggaga(x0, x1, x2)
U3_gga(x0, x1, x2, x3, x4)
U4_gga(x0, x1, x2, x3, x4)
U20_ggaga(x0, x1, x2, x3)
pF_in_gggga(x0, x1, x2, x3)
pG_in_gggga(x0, x1, x2, x3)
U21_ggaga(x0, x1, x2, x3, x4)
U12_gggga(x0, x1, x2, x3, x4)
U14_gggga(x0, x1, x2, x3, x4)
leH_in_gg(x0, x1)
U13_gggga(x0, x1, x2, x3, x4)
gtI_in_gg(x0, x1)
U15_gggga(x0, x1, x2, x3, x4)
U5_gg(x0, x1, x2)
U6_gg(x0, x1, x2)

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

(44) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 4 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 (EQUIVALENT transformation)

(18) Obligation:

(19) QDPSizeChangeProof (EQUIVALENT transformation)

(20) YES

(21) Obligation:

(22) UsableRulesProof (EQUIVALENT transformation)

(23) Obligation:

(24) PiDPToQDPProof (EQUIVALENT transformation)

(25) Obligation:

(26) QDPSizeChangeProof (EQUIVALENT transformation)

(27) YES

(28) Obligation:

(29) UsableRulesProof (EQUIVALENT transformation)

(30) Obligation:

(31) PiDPToQDPProof (SOUND transformation)

(32) Obligation:

(33) MRRProof (EQUIVALENT transformation)

(34) Obligation:

(35) DependencyGraphProof (EQUIVALENT transformation)

(36) TRUE

(37) Obligation:

(38) UsableRulesProof (EQUIVALENT transformation)

(39) Obligation:

(40) PiDPToQDPProof (SOUND transformation)

(41) Obligation:

(42) QDPOrderProof (EQUIVALENT transformation)

(43) Obligation:

(44) DependencyGraphProof (EQUIVALENT transformation)

(45) TRUE