Left Termination proof of /tmp/tmppg4uqH/mergesort

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

0 Prolog

↳1 PrologToPiTRSViaGraphTransformerProof (⇒, 214 ms)

↳2 PiTRS

↳3 DependencyPairsProof (⇔, 286 ms)

↳4 PiDP

↳5 DependencyGraphProof (⇔, 33 ms)

↳6 AND

    ↳7 PiDP

        ↳8 UsableRulesProof (⇔, 0 ms)

        ↳9 PiDP

        ↳10 PiDPToQDPProof (⇔, 13 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 MRRProof (⇔, 266 ms)

        ↳27 QDP

        ↳28 DependencyGraphProof (⇔, 0 ms)

        ↳29 TRUE

    ↳30 PiDP

        ↳31 UsableRulesProof (⇔, 0 ms)

        ↳32 PiDP

        ↳33 PiDPToQDPProof (⇒, 0 ms)

        ↳34 QDP

        ↳35 QDPSizeChangeProof (⇔, 0 ms)

        ↳36 YES

    ↳37 PiDP

        ↳38 UsableRulesProof (⇔, 0 ms)

        ↳39 PiDP

        ↳40 PiDPToQDPProof (⇒, 34 ms)

        ↳41 QDP

        ↳42 QDPOrderProof (⇔, 1093 ms)

        ↳43 QDP

        ↳44 DependencyGraphProof (⇔, 0 ms)

        ↳45 TRUE

(0) Obligation:

Clauses:

mergesort([], []).
mergesort(.(X, []), .(X, [])).
mergesort(.(X, .(Y, L1)), L2) :- ','(split2(.(X, .(Y, L1)), L3, L4), ','(mergesort(L3, L5), ','(mergesort(L4, L6), merge(L5, L6, L2)))).
split(L1, L2, L3) :- split0(L1, L2, L3).
split(L1, L2, L3) :- split1(L1, L2, L3).
split(L1, L2, L3) :- split2(L1, L2, L3).
split0([], [], []).
split1(.(X, []), .(X, []), []).
split2(.(X, .(Y, L1)), .(X, L2), .(Y, L3)) :- split(L1, L2, L3).
merge([], L1, L1).
merge(L1, [], L1).
merge(.(X, L1), .(Y, L2), .(X, L3)) :- ','(le(X, Y), merge(L1, .(Y, L2), L3)).
merge(.(X, L1), .(Y, L2), .(Y, L3)) :- ','(gt(X, Y), merge(.(X, L1), L2, L3)).
gt(s(X), s(Y)) :- gt(X, Y).
gt(s(X), 0).
le(s(X), s(Y)) :- le(X, Y).
le(0, s(Y)).
le(0, 0).

Query: mergesort(g,a)

(1) PrologToPiTRSViaGraphTransformerProof (SOUND transformation)

Transformed Prolog program to (Pi-)TRS.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
1 [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];
23 [label="23: true | mergesort([], T2), SCOPE: 1, CLAUSE: 1 | mergesort([], T2), SCOPE: 1, CLAUSE: 2\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
24 [label="24: 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];
25 [label="25: mergesort([], T2), SCOPE: 1, CLAUSE: 1 | mergesort([], T2), SCOPE: 1, CLAUSE: 2\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
27 [label="27: mergesort([], T2), SCOPE: 1, CLAUSE: 2\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
29 [label="29: \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];
36 [label="36: ','(split2(.(T10, .(T11, T12)), X20, X21), ','(mergesort(X20, X22), ','(mergesort(X21, X23), merge(X22, X23, T14))))\n\nT10 is ground\nT11 is ground\nT12 is ground\nX20 is free\nX21 is free\nX22 is free\nX23 is free", fontsize=16, style=filled, fillcolor=lightyellow];
38 [label="38: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
41 [label="41: ','(split2(.(T10, .(T11, T12)), X20, X21), ','(mergesort(X20, X22), ','(mergesort(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];
43 [label="B: ','(split(T24, X48, X49), ','(mergesort(.(T22, X48), X22), ','(mergesort(.(T23, X49), X23), merge(X22, X23, T14))))\n\nT22 is ground\nT23 is ground\nT24 is ground\nX22 is free\nX23 is free\nX48 is free\nX49 is free", fontsize=16, style=filled, fillcolor=lightyellow];
46 [label="C: split(T24, X48, X49)\n\nT24 is ground\nX48 is free\nX49 is free", fontsize=16, style=filled, fillcolor=lightyellow];
48 [label="I: ','(mergesort(.(T22, T26), X22), ','(mergesort(.(T23, T27), X23), merge(X22, X23, T14)))\n\nT22 is ground\nT23 is ground\nT26 is ground\nT27 is ground\nX22 is free\nX23 is free", fontsize=16, style=filled, fillcolor=lightyellow];
53 [label="53: split(T24, X48, X49), SCOPE: 3, CLAUSE: 3 | split(T24, X48, X49), SCOPE: 3, CLAUSE: 4 | split(T24, X48, X49), SCOPE: 3, CLAUSE: 5\n\nT24 is ground\nX48 is free\nX49 is free", fontsize=16, style=filled, fillcolor=lightyellow];
65 [label="65: split(T24, X48, X49), SCOPE: 3, CLAUSE: 3\n\nT24 is ground\nX48 is free\nX49 is free", fontsize=16, style=filled, fillcolor=lightyellow];
66 [label="66: split(T24, X48, X49), SCOPE: 3, CLAUSE: 4 | split(T24, X48, X49), SCOPE: 3, CLAUSE: 5\n\nT24 is ground\nX48 is free\nX49 is free", fontsize=16, style=filled, fillcolor=lightyellow];
69 [label="69: split0(T33, X83, X84)\n\nT33 is ground\nX83 is free\nX84 is free", fontsize=16, style=filled, fillcolor=lightyellow];
71 [label="71: split0(T33, X83, X84), SCOPE: 4, CLAUSE: 6\n\nT33 is ground\nX83 is free\nX84 is free", fontsize=16, style=filled, fillcolor=lightyellow];
73 [label="73: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
74 [label="74: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
75 [label="75: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
93 [label="93: split(T24, X48, X49), SCOPE: 3, CLAUSE: 4\n\nT24 is ground\nX48 is free\nX49 is free", fontsize=16, style=filled, fillcolor=lightyellow];
94 [label="94: split(T24, X48, X49), SCOPE: 3, CLAUSE: 5\n\nT24 is ground\nX48 is free\nX49 is free", fontsize=16, style=filled, fillcolor=lightyellow];
95 [label="95: split1(T38, X108, X109)\n\nT38 is ground\nX108 is free\nX109 is free", fontsize=16, style=filled, fillcolor=lightyellow];
96 [label="96: split1(T38, X108, X109), SCOPE: 5, CLAUSE: 7\n\nT38 is ground\nX108 is free\nX109 is free", fontsize=16, style=filled, fillcolor=lightyellow];
97 [label="97: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
98 [label="98: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
99 [label="99: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
104 [label="104: split2(T47, X133, X134)\n\nT47 is ground\nX133 is free\nX134 is free", fontsize=16, style=filled, fillcolor=lightyellow];
105 [label="105: split2(T47, X133, X134), SCOPE: 6, CLAUSE: 8\n\nT47 is ground\nX133 is free\nX134 is free", fontsize=16, style=filled, fillcolor=lightyellow];
110 [label="110: split(T59, X161, X162)\n\nT59 is ground\nX161 is free\nX162 is free", fontsize=16, style=filled, fillcolor=lightyellow];
111 [label="111: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
120 [label="120: mergesort(.(T22, T26), X22)\n\nT22 is ground\nT26 is ground\nX22 is free", fontsize=16, style=filled, fillcolor=lightyellow];
122 [label="J: ','(mergesort(.(T23, T27), X23), merge(T61, X23, T14))\n\nT23 is ground\nT27 is ground\nT61 is ground\nX23 is free", fontsize=16, style=filled, fillcolor=lightyellow];
127 [label="127: mergesort(.(T23, T27), X23)\n\nT23 is ground\nT27 is ground\nX23 is free", fontsize=16, style=filled, fillcolor=lightyellow];
128 [label="D: merge(T61, T62, T14)\n\nT61 is ground\nT62 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
129 [label="129: merge(T61, T62, T14), SCOPE: 7, CLAUSE: 9 | merge(T61, T62, T14), SCOPE: 7, CLAUSE: 10 | merge(T61, T62, T14), SCOPE: 7, CLAUSE: 11 | merge(T61, T62, T14), SCOPE: 7, CLAUSE: 12\n\nT61 is ground\nT62 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
132 [label="132: merge(T61, T62, T14), SCOPE: 7, CLAUSE: 9\n\nT61 is ground\nT62 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
133 [label="133: merge(T61, T62, T14), SCOPE: 7, CLAUSE: 10 | merge(T61, T62, T14), SCOPE: 7, CLAUSE: 11 | merge(T61, T62, T14), SCOPE: 7, CLAUSE: 12\n\nT61 is ground\nT62 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
134 [label="134: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
135 [label="135: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
136 [label="136: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
137 [label="137: merge(T61, T62, T14), SCOPE: 7, CLAUSE: 10\n\nT61 is ground\nT62 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
138 [label="138: merge(T61, T62, T14), SCOPE: 7, CLAUSE: 11 | merge(T61, T62, T14), SCOPE: 7, CLAUSE: 12\n\nT61 is ground\nT62 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
141 [label="141: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
142 [label="142: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
143 [label="143: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
147 [label="147: merge(T61, T62, T14), SCOPE: 7, CLAUSE: 11\n\nT61 is ground\nT62 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
148 [label="148: merge(T61, T62, T14), SCOPE: 7, CLAUSE: 12\n\nT61 is ground\nT62 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
159 [label="E: ','(le(T95, T97), merge(T96, .(T97, T98), T100))\n\nT95 is ground\nT96 is ground\nT97 is ground\nT98 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
160 [label="160: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
163 [label="G: le(T95, T97)\n\nT95 is ground\nT97 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
164 [label="164: merge(T96, .(T97, T98), T100)\n\nT96 is ground\nT97 is ground\nT98 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
167 [label="167: le(T95, T97), SCOPE: 8, CLAUSE: 15 | le(T95, T97), SCOPE: 8, CLAUSE: 16 | le(T95, T97), SCOPE: 8, CLAUSE: 17\n\nT95 is ground\nT97 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
168 [label="168: le(T95, T97), SCOPE: 8, CLAUSE: 15\n\nT95 is ground\nT97 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
169 [label="169: le(T95, T97), SCOPE: 8, CLAUSE: 16 | le(T95, T97), SCOPE: 8, CLAUSE: 17\n\nT95 is ground\nT97 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
172 [label="172: le(T113, T114)\n\nT113 is ground\nT114 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
173 [label="173: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
176 [label="176: le(T95, T97), SCOPE: 8, CLAUSE: 16\n\nT95 is ground\nT97 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
177 [label="177: le(T95, T97), SCOPE: 8, CLAUSE: 17\n\nT95 is ground\nT97 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
179 [label="179: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
180 [label="180: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
181 [label="181: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
184 [label="184: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
185 [label="185: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
186 [label="186: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
200 [label="F: ','(gt(T136, T138), merge(.(T136, T137), T139, T141))\n\nT136 is ground\nT137 is ground\nT138 is ground\nT139 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
201 [label="201: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
207 [label="H: gt(T136, T138)\n\nT136 is ground\nT138 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
208 [label="208: merge(.(T136, T137), T139, T141)\n\nT136 is ground\nT137 is ground\nT139 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
211 [label="211: gt(T136, T138), SCOPE: 9, CLAUSE: 13 | gt(T136, T138), SCOPE: 9, CLAUSE: 14\n\nT136 is ground\nT138 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
212 [label="212: gt(T136, T138), SCOPE: 9, CLAUSE: 13\n\nT136 is ground\nT138 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
213 [label="213: gt(T136, T138), SCOPE: 9, CLAUSE: 14\n\nT136 is ground\nT138 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
216 [label="216: gt(T154, T155)\n\nT154 is ground\nT155 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
217 [label="217: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
220 [label="220: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
221 [label="221: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
222 [label="222: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
223 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
1 -> 223 [arrowhead = none ];
223 -> 6;

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

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

226 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
23 -> 226 [arrowhead = none ];
226 -> 25;

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

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

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

230 [label="BACKTRACK\nfor clause: mergesort(.(X, .(Y, L1)), L2) :- ','(split2(.(X, .(Y, L1)), L3, L4), ','(mergesort(L3, L5), ','(mergesort(L4, L6), merge(L5, L6, L2))))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
27 -> 230 [arrowhead = none ];
230 -> 29;

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

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

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

234 [label="BACKTRACK\nfor clause: mergesort(.(X, .(Y, L1)), L2) :- ','(split2(.(X, .(Y, L1)), L3, L4), ','(mergesort(L3, L5), ','(mergesort(L4, L6), merge(L5, L6, L2))))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
33 -> 234 [arrowhead = none ];
234 -> 34;

235 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
36 -> 235 [arrowhead = none ];
235 -> 41;

236 [label="ONLY EVAL with clause\nsplit2(.(X43, .(X44, X45)), .(X43, X46), .(X44, X47)) :- split(X45, X46, X47).\nand substitutionT10 -> T22,\nX43 -> T22,\nT11 -> T23,\nX44 -> T23,\nT12 -> T24,\nX45 -> T24,\nX46 -> X48,\nX20 -> .(T22, X48),\nX47 -> X49,\nX21 -> .(T23, X49)", fontsize=14, style = filled, fillcolor = lightblue];
41 -> 236 [arrowhead = none ];
236 -> 43;

237 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
43 -> 237 [arrowhead = none ];
237 -> 46;

238 [label="SPLIT 2\nnew knowledge:\nT24 is ground\nT26 is ground\nT27 is ground\nreplacements:X48 -> T26,\nX49 -> T27", fontsize=14, style = filled, fillcolor = violet];
43 -> 238 [arrowhead = none ];
238 -> 48;

239 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
46 -> 239 [arrowhead = none ];
239 -> 53;

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

241 [label="SPLIT 2\nnew knowledge:\nT22 is ground\nT26 is ground\nT61 is ground\nreplacements:X22 -> T61", fontsize=14, style = filled, fillcolor = violet];
48 -> 241 [arrowhead = none ];
241 -> 122;

242 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
53 -> 242 [arrowhead = none ];
242 -> 65;

243 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
53 -> 243 [arrowhead = none ];
243 -> 66;

244 [label="ONLY EVAL with clause\nsplit(X80, X81, X82) :- split0(X80, X81, X82).\nand substitutionT24 -> T33,\nX80 -> T33,\nX48 -> X83,\nX81 -> X83,\nX49 -> X84,\nX82 -> X84", fontsize=14, style = filled, fillcolor = lightblue];
65 -> 244 [arrowhead = none ];
244 -> 69;

245 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
66 -> 245 [arrowhead = none ];
245 -> 93;

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

247 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
69 -> 247 [arrowhead = none ];
247 -> 71;

248 [label="EVAL with clause\nsplit0([], [], []).\nand substitutionT33 -> [],\nX83 -> [],\nX84 -> []", fontsize=14, style = filled, fillcolor = lightblue];
71 -> 248 [arrowhead = none ];
248 -> 73;

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

250 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
73 -> 250 [arrowhead = none ];
250 -> 75;

251 [label="ONLY EVAL with clause\nsplit(X105, X106, X107) :- split1(X105, X106, X107).\nand substitutionT24 -> T38,\nX105 -> T38,\nX48 -> X108,\nX106 -> X108,\nX49 -> X109,\nX107 -> X109", fontsize=14, style = filled, fillcolor = lightblue];
93 -> 251 [arrowhead = none ];
251 -> 95;

252 [label="ONLY EVAL with clause\nsplit(X130, X131, X132) :- split2(X130, X131, X132).\nand substitutionT24 -> T47,\nX130 -> T47,\nX48 -> X133,\nX131 -> X133,\nX49 -> X134,\nX132 -> X134", fontsize=14, style = filled, fillcolor = lightblue];
94 -> 252 [arrowhead = none ];
252 -> 104;

253 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
95 -> 253 [arrowhead = none ];
253 -> 96;

254 [label="EVAL with clause\nsplit1(.(X112, []), .(X112, []), []).\nand substitutionX112 -> T41,\nT38 -> .(T41, []),\nX108 -> .(T41, []),\nX109 -> []", fontsize=14, style = filled, fillcolor = lightblue];
96 -> 254 [arrowhead = none ];
254 -> 97;

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

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

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

258 [label="EVAL with clause\nsplit2(.(X156, .(X157, X158)), .(X156, X159), .(X157, X160)) :- split(X158, X159, X160).\nand substitutionX156 -> T57,\nX157 -> T58,\nX158 -> T59,\nT47 -> .(T57, .(T58, T59)),\nX159 -> X161,\nX133 -> .(T57, X161),\nX160 -> X162,\nX134 -> .(T58, X162)", fontsize=14, style = filled, fillcolor = lightblue];
105 -> 258 [arrowhead = none ];
258 -> 110;

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

260 [label="INSTANCE with matching:\nT24 -> T59\nX48 -> X161\nX49 -> X162", fontsize=14, style = filled, fillcolor = lightgrey];
110 -> 260 [arrowhead = none , style=dashed];
260 -> 46[style=dashed];

261 [label="INSTANCE with matching:\nT1 -> .(T22, T26)\nT2 -> X22", fontsize=14, style = filled, fillcolor = lightgrey];
120 -> 261 [arrowhead = none , style=dashed];
261 -> 1[style=dashed];

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

263 [label="SPLIT 2\nnew knowledge:\nT23 is ground\nT27 is ground\nT62 is ground\nreplacements:X23 -> T62", fontsize=14, style = filled, fillcolor = violet];
122 -> 263 [arrowhead = none ];
263 -> 128;

264 [label="INSTANCE with matching:\nT1 -> .(T23, T27)\nT2 -> X23", fontsize=14, style = filled, fillcolor = lightgrey];
127 -> 264 [arrowhead = none , style=dashed];
264 -> 1[style=dashed];

265 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
128 -> 265 [arrowhead = none ];
265 -> 129;

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

267 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
129 -> 267 [arrowhead = none ];
267 -> 133;

268 [label="EVAL with clause\nmerge([], X174, X174).\nand substitutionT61 -> [],\nT62 -> T69,\nX174 -> T69,\nT14 -> T69", fontsize=14, style = filled, fillcolor = lightblue];
132 -> 268 [arrowhead = none ];
268 -> 134;

269 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
132 -> 269 [arrowhead = none ];
269 -> 135;

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

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

272 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
134 -> 272 [arrowhead = none ];
272 -> 136;

273 [label="EVAL with clause\nmerge(X179, [], X179).\nand substitutionT61 -> T74,\nX179 -> T74,\nT62 -> [],\nT14 -> T74", fontsize=14, style = filled, fillcolor = lightblue];
137 -> 273 [arrowhead = none ];
273 -> 141;

274 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
137 -> 274 [arrowhead = none ];
274 -> 142;

275 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
138 -> 275 [arrowhead = none ];
275 -> 147;

276 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
138 -> 276 [arrowhead = none ];
276 -> 148;

277 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
141 -> 277 [arrowhead = none ];
277 -> 143;

278 [label="EVAL with clause\nmerge(.(X200, X201), .(X202, X203), .(X200, X204)) :- ','(le(X200, X202), merge(X201, .(X202, X203), X204)).\nand substitutionX200 -> T95,\nX201 -> T96,\nT61 -> .(T95, T96),\nX202 -> T97,\nX203 -> T98,\nT62 -> .(T97, T98),\nX204 -> T100,\nT14 -> .(T95, T100),\nT99 -> T100", fontsize=14, style = filled, fillcolor = lightblue];
147 -> 278 [arrowhead = none ];
278 -> 159;

279 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
147 -> 279 [arrowhead = none ];
279 -> 160;

280 [label="EVAL with clause\nmerge(.(X238, X239), .(X240, X241), .(X240, X242)) :- ','(gt(X238, X240), merge(.(X238, X239), X241, X242)).\nand substitutionX238 -> T136,\nX239 -> T137,\nT61 -> .(T136, T137),\nX240 -> T138,\nX241 -> T139,\nT62 -> .(T138, T139),\nX242 -> T141,\nT14 -> .(T138, T141),\nT140 -> T141", fontsize=14, style = filled, fillcolor = lightblue];
148 -> 280 [arrowhead = none ];
280 -> 200;

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

282 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
159 -> 282 [arrowhead = none ];
282 -> 163;

283 [label="SPLIT 2\nnew knowledge:\nT95 is ground\nT97 is ground", fontsize=14, style = filled, fillcolor = violet];
159 -> 283 [arrowhead = none ];
283 -> 164;

284 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
163 -> 284 [arrowhead = none ];
284 -> 167;

285 [label="INSTANCE with matching:\nT61 -> T96\nT62 -> .(T97, T98)\nT14 -> T100", fontsize=14, style = filled, fillcolor = lightgrey];
164 -> 285 [arrowhead = none , style=dashed];
285 -> 128[style=dashed];

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

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

288 [label="EVAL with clause\nle(s(X217), s(X218)) :- le(X217, X218).\nand substitutionX217 -> T113,\nT95 -> s(T113),\nX218 -> T114,\nT97 -> s(T114)", fontsize=14, style = filled, fillcolor = lightblue];
168 -> 288 [arrowhead = none ];
288 -> 172;

289 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
168 -> 289 [arrowhead = none ];
289 -> 173;

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

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

292 [label="INSTANCE with matching:\nT95 -> T113\nT97 -> T114", fontsize=14, style = filled, fillcolor = lightgrey];
172 -> 292 [arrowhead = none , style=dashed];
292 -> 163[style=dashed];

293 [label="EVAL with clause\nle(0, s(X225)).\nand substitutionT95 -> 0,\nX225 -> T121,\nT97 -> s(T121)", fontsize=14, style = filled, fillcolor = lightblue];
176 -> 293 [arrowhead = none ];
293 -> 179;

294 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
176 -> 294 [arrowhead = none ];
294 -> 180;

295 [label="EVAL with clause\nle(0, 0).\nand substitutionT95 -> 0,\nT97 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
177 -> 295 [arrowhead = none ];
295 -> 184;

296 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
177 -> 296 [arrowhead = none ];
296 -> 185;

297 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
179 -> 297 [arrowhead = none ];
297 -> 181;

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

299 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
200 -> 299 [arrowhead = none ];
299 -> 207;

300 [label="SPLIT 2\nnew knowledge:\nT136 is ground\nT138 is ground", fontsize=14, style = filled, fillcolor = violet];
200 -> 300 [arrowhead = none ];
300 -> 208;

301 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
207 -> 301 [arrowhead = none ];
301 -> 211;

302 [label="INSTANCE with matching:\nT61 -> .(T136, T137)\nT62 -> T139\nT14 -> T141", fontsize=14, style = filled, fillcolor = lightgrey];
208 -> 302 [arrowhead = none , style=dashed];
302 -> 128[style=dashed];

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

304 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
211 -> 304 [arrowhead = none ];
304 -> 213;

305 [label="EVAL with clause\ngt(s(X255), s(X256)) :- gt(X255, X256).\nand substitutionX255 -> T154,\nT136 -> s(T154),\nX256 -> T155,\nT138 -> s(T155)", fontsize=14, style = filled, fillcolor = lightblue];
212 -> 305 [arrowhead = none ];
305 -> 216;

306 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
212 -> 306 [arrowhead = none ];
306 -> 217;

307 [label="EVAL with clause\ngt(s(X261), 0).\nand substitutionX261 -> T160,\nT136 -> s(T160),\nT138 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
213 -> 307 [arrowhead = none ];
307 -> 220;

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

309 [label="INSTANCE with matching:\nT136 -> T154\nT138 -> T155", fontsize=14, style = filled, fillcolor = lightgrey];
216 -> 309 [arrowhead = none , style=dashed];
309 -> 207[style=dashed];

310 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
220 -> 310 [arrowhead = none ];
310 -> 222;

}

(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(.(T22, .(T23, T24)), T14) → U1_ga(T22, T23, T24, T14, pB_in_gaagagaa(T24, X48, X49, T22, X22, T23, X23, T14))
pB_in_gaagagaa(T24, T26, T27, T22, X22, T23, X23, T14) → U7_gaagagaa(T24, T26, T27, T22, X22, T23, X23, T14, splitC_in_gaa(T24, T26, T27))
splitC_in_gaa([], [], []) → splitC_out_gaa([], [], [])
splitC_in_gaa(.(T41, []), .(T41, []), []) → splitC_out_gaa(.(T41, []), .(T41, []), [])
splitC_in_gaa(.(T57, .(T58, T59)), .(T57, X161), .(T58, X162)) → U2_gaa(T57, T58, T59, X161, X162, splitC_in_gaa(T59, X161, X162))
U2_gaa(T57, T58, T59, X161, X162, splitC_out_gaa(T59, X161, X162)) → splitC_out_gaa(.(T57, .(T58, T59)), .(T57, X161), .(T58, X162))
U7_gaagagaa(T24, T26, T27, T22, X22, T23, X23, T14, splitC_out_gaa(T24, T26, T27)) → U8_gaagagaa(T24, T26, T27, T22, X22, T23, X23, T14, pI_in_ggaggaa(T22, T26, X22, T23, T27, X23, T14))
pI_in_ggaggaa(T22, T26, T61, T23, T27, X23, T14) → U9_ggaggaa(T22, T26, T61, T23, T27, X23, T14, mergesortA_in_ga(.(T22, T26), T61))
U9_ggaggaa(T22, T26, T61, T23, T27, X23, T14, mergesortA_out_ga(.(T22, T26), T61)) → U10_ggaggaa(T22, T26, T61, T23, T27, X23, T14, pJ_in_ggaga(T23, T27, X23, T61, T14))
pJ_in_ggaga(T23, T27, T62, T61, T14) → U11_ggaga(T23, T27, T62, T61, T14, mergesortA_in_ga(.(T23, T27), T62))
U11_ggaga(T23, T27, T62, T61, T14, mergesortA_out_ga(.(T23, T27), T62)) → U12_ggaga(T23, T27, T62, T61, T14, mergeD_in_gga(T61, T62, T14))
mergeD_in_gga([], T69, T69) → mergeD_out_gga([], T69, T69)
mergeD_in_gga(T74, [], T74) → mergeD_out_gga(T74, [], T74)
mergeD_in_gga(.(T95, T96), .(T97, T98), .(T95, T100)) → U3_gga(T95, T96, T97, T98, T100, pE_in_gggga(T95, T97, T96, T98, T100))
pE_in_gggga(T95, T97, T96, T98, T100) → U13_gggga(T95, T97, T96, T98, T100, leG_in_gg(T95, T97))
leG_in_gg(s(T113), s(T114)) → U5_gg(T113, T114, leG_in_gg(T113, T114))
leG_in_gg(0, s(T121)) → leG_out_gg(0, s(T121))
leG_in_gg(0, 0) → leG_out_gg(0, 0)
U5_gg(T113, T114, leG_out_gg(T113, T114)) → leG_out_gg(s(T113), s(T114))
U13_gggga(T95, T97, T96, T98, T100, leG_out_gg(T95, T97)) → U14_gggga(T95, T97, T96, T98, T100, mergeD_in_gga(T96, .(T97, T98), T100))
mergeD_in_gga(.(T136, T137), .(T138, T139), .(T138, T141)) → U4_gga(T136, T137, T138, T139, T141, pF_in_gggga(T136, T138, T137, T139, T141))
pF_in_gggga(T136, T138, T137, T139, T141) → U15_gggga(T136, T138, T137, T139, T141, gtH_in_gg(T136, T138))
gtH_in_gg(s(T154), s(T155)) → U6_gg(T154, T155, gtH_in_gg(T154, T155))
gtH_in_gg(s(T160), 0) → gtH_out_gg(s(T160), 0)
U6_gg(T154, T155, gtH_out_gg(T154, T155)) → gtH_out_gg(s(T154), s(T155))
U15_gggga(T136, T138, T137, T139, T141, gtH_out_gg(T136, T138)) → U16_gggga(T136, T138, T137, T139, T141, mergeD_in_gga(.(T136, T137), T139, T141))
U16_gggga(T136, T138, T137, T139, T141, mergeD_out_gga(.(T136, T137), T139, T141)) → pF_out_gggga(T136, T138, T137, T139, T141)
U4_gga(T136, T137, T138, T139, T141, pF_out_gggga(T136, T138, T137, T139, T141)) → mergeD_out_gga(.(T136, T137), .(T138, T139), .(T138, T141))
U14_gggga(T95, T97, T96, T98, T100, mergeD_out_gga(T96, .(T97, T98), T100)) → pE_out_gggga(T95, T97, T96, T98, T100)
U3_gga(T95, T96, T97, T98, T100, pE_out_gggga(T95, T97, T96, T98, T100)) → mergeD_out_gga(.(T95, T96), .(T97, T98), .(T95, T100))
U12_ggaga(T23, T27, T62, T61, T14, mergeD_out_gga(T61, T62, T14)) → pJ_out_ggaga(T23, T27, T62, T61, T14)
U10_ggaggaa(T22, T26, T61, T23, T27, X23, T14, pJ_out_ggaga(T23, T27, X23, T61, T14)) → pI_out_ggaggaa(T22, T26, T61, T23, T27, X23, T14)
U8_gaagagaa(T24, T26, T27, T22, X22, T23, X23, T14, pI_out_ggaggaa(T22, T26, X22, T23, T27, X23, T14)) → pB_out_gaagagaa(T24, T26, T27, T22, X22, T23, X23, T14)
U1_ga(T22, T23, T24, T14, pB_out_gaagagaa(T24, X48, X49, T22, X22, T23, X23, T14)) → mergesortA_out_ga(.(T22, .(T23, T24)), 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(.(T22, .(T23, T24)), T14) → U1_GA(T22, T23, T24, T14, pB_in_gaagagaa(T24, X48, X49, T22, X22, T23, X23, T14))
MERGESORTA_IN_GA(.(T22, .(T23, T24)), T14) → PB_IN_GAAGAGAA(T24, X48, X49, T22, X22, T23, X23, T14)
PB_IN_GAAGAGAA(T24, T26, T27, T22, X22, T23, X23, T14) → U7_GAAGAGAA(T24, T26, T27, T22, X22, T23, X23, T14, splitC_in_gaa(T24, T26, T27))
PB_IN_GAAGAGAA(T24, T26, T27, T22, X22, T23, X23, T14) → SPLITC_IN_GAA(T24, T26, T27)
SPLITC_IN_GAA(.(T57, .(T58, T59)), .(T57, X161), .(T58, X162)) → U2_GAA(T57, T58, T59, X161, X162, splitC_in_gaa(T59, X161, X162))
SPLITC_IN_GAA(.(T57, .(T58, T59)), .(T57, X161), .(T58, X162)) → SPLITC_IN_GAA(T59, X161, X162)
U7_GAAGAGAA(T24, T26, T27, T22, X22, T23, X23, T14, splitC_out_gaa(T24, T26, T27)) → U8_GAAGAGAA(T24, T26, T27, T22, X22, T23, X23, T14, pI_in_ggaggaa(T22, T26, X22, T23, T27, X23, T14))
U7_GAAGAGAA(T24, T26, T27, T22, X22, T23, X23, T14, splitC_out_gaa(T24, T26, T27)) → PI_IN_GGAGGAA(T22, T26, X22, T23, T27, X23, T14)
PI_IN_GGAGGAA(T22, T26, T61, T23, T27, X23, T14) → U9_GGAGGAA(T22, T26, T61, T23, T27, X23, T14, mergesortA_in_ga(.(T22, T26), T61))
PI_IN_GGAGGAA(T22, T26, T61, T23, T27, X23, T14) → MERGESORTA_IN_GA(.(T22, T26), T61)
U9_GGAGGAA(T22, T26, T61, T23, T27, X23, T14, mergesortA_out_ga(.(T22, T26), T61)) → U10_GGAGGAA(T22, T26, T61, T23, T27, X23, T14, pJ_in_ggaga(T23, T27, X23, T61, T14))
U9_GGAGGAA(T22, T26, T61, T23, T27, X23, T14, mergesortA_out_ga(.(T22, T26), T61)) → PJ_IN_GGAGA(T23, T27, X23, T61, T14)
PJ_IN_GGAGA(T23, T27, T62, T61, T14) → U11_GGAGA(T23, T27, T62, T61, T14, mergesortA_in_ga(.(T23, T27), T62))
PJ_IN_GGAGA(T23, T27, T62, T61, T14) → MERGESORTA_IN_GA(.(T23, T27), T62)
U11_GGAGA(T23, T27, T62, T61, T14, mergesortA_out_ga(.(T23, T27), T62)) → U12_GGAGA(T23, T27, T62, T61, T14, mergeD_in_gga(T61, T62, T14))
U11_GGAGA(T23, T27, T62, T61, T14, mergesortA_out_ga(.(T23, T27), T62)) → MERGED_IN_GGA(T61, T62, T14)
MERGED_IN_GGA(.(T95, T96), .(T97, T98), .(T95, T100)) → U3_GGA(T95, T96, T97, T98, T100, pE_in_gggga(T95, T97, T96, T98, T100))
MERGED_IN_GGA(.(T95, T96), .(T97, T98), .(T95, T100)) → PE_IN_GGGGA(T95, T97, T96, T98, T100)
PE_IN_GGGGA(T95, T97, T96, T98, T100) → U13_GGGGA(T95, T97, T96, T98, T100, leG_in_gg(T95, T97))
PE_IN_GGGGA(T95, T97, T96, T98, T100) → LEG_IN_GG(T95, T97)
LEG_IN_GG(s(T113), s(T114)) → U5_GG(T113, T114, leG_in_gg(T113, T114))
LEG_IN_GG(s(T113), s(T114)) → LEG_IN_GG(T113, T114)
U13_GGGGA(T95, T97, T96, T98, T100, leG_out_gg(T95, T97)) → U14_GGGGA(T95, T97, T96, T98, T100, mergeD_in_gga(T96, .(T97, T98), T100))
U13_GGGGA(T95, T97, T96, T98, T100, leG_out_gg(T95, T97)) → MERGED_IN_GGA(T96, .(T97, T98), T100)
MERGED_IN_GGA(.(T136, T137), .(T138, T139), .(T138, T141)) → U4_GGA(T136, T137, T138, T139, T141, pF_in_gggga(T136, T138, T137, T139, T141))
MERGED_IN_GGA(.(T136, T137), .(T138, T139), .(T138, T141)) → PF_IN_GGGGA(T136, T138, T137, T139, T141)
PF_IN_GGGGA(T136, T138, T137, T139, T141) → U15_GGGGA(T136, T138, T137, T139, T141, gtH_in_gg(T136, T138))
PF_IN_GGGGA(T136, T138, T137, T139, T141) → GTH_IN_GG(T136, T138)
GTH_IN_GG(s(T154), s(T155)) → U6_GG(T154, T155, gtH_in_gg(T154, T155))
GTH_IN_GG(s(T154), s(T155)) → GTH_IN_GG(T154, T155)
U15_GGGGA(T136, T138, T137, T139, T141, gtH_out_gg(T136, T138)) → U16_GGGGA(T136, T138, T137, T139, T141, mergeD_in_gga(.(T136, T137), T139, T141))
U15_GGGGA(T136, T138, T137, T139, T141, gtH_out_gg(T136, T138)) → MERGED_IN_GGA(.(T136, T137), T139, T141)

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(.(T22, .(T23, T24)), T14) → U1_ga(T22, T23, T24, T14, pB_in_gaagagaa(T24, X48, X49, T22, X22, T23, X23, T14))
pB_in_gaagagaa(T24, T26, T27, T22, X22, T23, X23, T14) → U7_gaagagaa(T24, T26, T27, T22, X22, T23, X23, T14, splitC_in_gaa(T24, T26, T27))
splitC_in_gaa([], [], []) → splitC_out_gaa([], [], [])
splitC_in_gaa(.(T41, []), .(T41, []), []) → splitC_out_gaa(.(T41, []), .(T41, []), [])
splitC_in_gaa(.(T57, .(T58, T59)), .(T57, X161), .(T58, X162)) → U2_gaa(T57, T58, T59, X161, X162, splitC_in_gaa(T59, X161, X162))
U2_gaa(T57, T58, T59, X161, X162, splitC_out_gaa(T59, X161, X162)) → splitC_out_gaa(.(T57, .(T58, T59)), .(T57, X161), .(T58, X162))
U7_gaagagaa(T24, T26, T27, T22, X22, T23, X23, T14, splitC_out_gaa(T24, T26, T27)) → U8_gaagagaa(T24, T26, T27, T22, X22, T23, X23, T14, pI_in_ggaggaa(T22, T26, X22, T23, T27, X23, T14))
pI_in_ggaggaa(T22, T26, T61, T23, T27, X23, T14) → U9_ggaggaa(T22, T26, T61, T23, T27, X23, T14, mergesortA_in_ga(.(T22, T26), T61))
U9_ggaggaa(T22, T26, T61, T23, T27, X23, T14, mergesortA_out_ga(.(T22, T26), T61)) → U10_ggaggaa(T22, T26, T61, T23, T27, X23, T14, pJ_in_ggaga(T23, T27, X23, T61, T14))
pJ_in_ggaga(T23, T27, T62, T61, T14) → U11_ggaga(T23, T27, T62, T61, T14, mergesortA_in_ga(.(T23, T27), T62))
U11_ggaga(T23, T27, T62, T61, T14, mergesortA_out_ga(.(T23, T27), T62)) → U12_ggaga(T23, T27, T62, T61, T14, mergeD_in_gga(T61, T62, T14))
mergeD_in_gga([], T69, T69) → mergeD_out_gga([], T69, T69)
mergeD_in_gga(T74, [], T74) → mergeD_out_gga(T74, [], T74)
mergeD_in_gga(.(T95, T96), .(T97, T98), .(T95, T100)) → U3_gga(T95, T96, T97, T98, T100, pE_in_gggga(T95, T97, T96, T98, T100))
pE_in_gggga(T95, T97, T96, T98, T100) → U13_gggga(T95, T97, T96, T98, T100, leG_in_gg(T95, T97))
leG_in_gg(s(T113), s(T114)) → U5_gg(T113, T114, leG_in_gg(T113, T114))
leG_in_gg(0, s(T121)) → leG_out_gg(0, s(T121))
leG_in_gg(0, 0) → leG_out_gg(0, 0)
U5_gg(T113, T114, leG_out_gg(T113, T114)) → leG_out_gg(s(T113), s(T114))
U13_gggga(T95, T97, T96, T98, T100, leG_out_gg(T95, T97)) → U14_gggga(T95, T97, T96, T98, T100, mergeD_in_gga(T96, .(T97, T98), T100))
mergeD_in_gga(.(T136, T137), .(T138, T139), .(T138, T141)) → U4_gga(T136, T137, T138, T139, T141, pF_in_gggga(T136, T138, T137, T139, T141))
pF_in_gggga(T136, T138, T137, T139, T141) → U15_gggga(T136, T138, T137, T139, T141, gtH_in_gg(T136, T138))
gtH_in_gg(s(T154), s(T155)) → U6_gg(T154, T155, gtH_in_gg(T154, T155))
gtH_in_gg(s(T160), 0) → gtH_out_gg(s(T160), 0)
U6_gg(T154, T155, gtH_out_gg(T154, T155)) → gtH_out_gg(s(T154), s(T155))
U15_gggga(T136, T138, T137, T139, T141, gtH_out_gg(T136, T138)) → U16_gggga(T136, T138, T137, T139, T141, mergeD_in_gga(.(T136, T137), T139, T141))
U16_gggga(T136, T138, T137, T139, T141, mergeD_out_gga(.(T136, T137), T139, T141)) → pF_out_gggga(T136, T138, T137, T139, T141)
U4_gga(T136, T137, T138, T139, T141, pF_out_gggga(T136, T138, T137, T139, T141)) → mergeD_out_gga(.(T136, T137), .(T138, T139), .(T138, T141))
U14_gggga(T95, T97, T96, T98, T100, mergeD_out_gga(T96, .(T97, T98), T100)) → pE_out_gggga(T95, T97, T96, T98, T100)
U3_gga(T95, T96, T97, T98, T100, pE_out_gggga(T95, T97, T96, T98, T100)) → mergeD_out_gga(.(T95, T96), .(T97, T98), .(T95, T100))
U12_ggaga(T23, T27, T62, T61, T14, mergeD_out_gga(T61, T62, T14)) → pJ_out_ggaga(T23, T27, T62, T61, T14)
U10_ggaggaa(T22, T26, T61, T23, T27, X23, T14, pJ_out_ggaga(T23, T27, X23, T61, T14)) → pI_out_ggaggaa(T22, T26, T61, T23, T27, X23, T14)
U8_gaagagaa(T24, T26, T27, T22, X22, T23, X23, T14, pI_out_ggaggaa(T22, T26, X22, T23, T27, X23, T14)) → pB_out_gaagagaa(T24, T26, T27, T22, X22, T23, X23, T14)
U1_ga(T22, T23, T24, T14, pB_out_gaagagaa(T24, X48, X49, T22, X22, T23, X23, T14)) → mergesortA_out_ga(.(T22, .(T23, T24)), T14)

The argument filtering Pi contains the following mapping:
mergesortA_in_ga(x1, x2) = mergesortA_in_ga(x1)
[] = []
mergesortA_out_ga(x1, x2) = mergesortA_out_ga(x1, x2)
.(x1, x2) = .(x1, x2)
U1_ga(x1, x2, x3, x4, x5) = U1_ga(x1, x2, x3, x5)
pB_in_gaagagaa(x1, x2, x3, x4, x5, x6, x7, x8) = pB_in_gaagagaa(x1, x4, x6)
U7_gaagagaa(x1, x2, x3, x4, x5, x6, x7, x8, x9) = U7_gaagagaa(x1, x4, x6, x9)
splitC_in_gaa(x1, x2, x3) = splitC_in_gaa(x1)
splitC_out_gaa(x1, x2, x3) = splitC_out_gaa(x1, x2, x3)
U2_gaa(x1, x2, x3, x4, x5, x6) = U2_gaa(x1, x2, x3, x6)
U8_gaagagaa(x1, x2, x3, x4, x5, x6, x7, x8, x9) = U8_gaagagaa(x1, x2, x3, x4, x6, x9)
pI_in_ggaggaa(x1, x2, x3, x4, x5, x6, x7) = pI_in_ggaggaa(x1, x2, x4, x5)
U9_ggaggaa(x1, x2, x3, x4, x5, x6, x7, x8) = U9_ggaggaa(x1, x2, x4, x5, x8)
U10_ggaggaa(x1, x2, x3, x4, x5, x6, x7, x8) = U10_ggaggaa(x1, x2, x3, x4, x5, x8)
pJ_in_ggaga(x1, x2, x3, x4, x5) = pJ_in_ggaga(x1, x2, x4)
U11_ggaga(x1, x2, x3, x4, x5, x6) = U11_ggaga(x1, x2, x4, x6)
U12_ggaga(x1, x2, x3, x4, x5, x6) = U12_ggaga(x1, x2, x3, x4, x6)
mergeD_in_gga(x1, x2, x3) = mergeD_in_gga(x1, x2)
mergeD_out_gga(x1, x2, x3) = mergeD_out_gga(x1, x2, x3)
U3_gga(x1, x2, x3, x4, x5, x6) = U3_gga(x1, x2, x3, x4, x6)
pE_in_gggga(x1, x2, x3, x4, x5) = pE_in_gggga(x1, x2, x3, x4)
U13_gggga(x1, x2, x3, x4, x5, x6) = U13_gggga(x1, x2, x3, x4, x6)
leG_in_gg(x1, x2) = leG_in_gg(x1, x2)
s(x1) = s(x1)
U5_gg(x1, x2, x3) = U5_gg(x1, x2, x3)
0 = 0
leG_out_gg(x1, x2) = leG_out_gg(x1, x2)
U14_gggga(x1, x2, x3, x4, x5, x6) = U14_gggga(x1, x2, x3, x4, x6)
U4_gga(x1, x2, x3, x4, x5, x6) = U4_gga(x1, x2, x3, x4, x6)
pF_in_gggga(x1, x2, x3, x4, x5) = pF_in_gggga(x1, x2, x3, x4)
U15_gggga(x1, x2, x3, x4, x5, x6) = U15_gggga(x1, x2, x3, x4, x6)
gtH_in_gg(x1, x2) = gtH_in_gg(x1, x2)
U6_gg(x1, x2, x3) = U6_gg(x1, x2, x3)
gtH_out_gg(x1, x2) = gtH_out_gg(x1, x2)
U16_gggga(x1, x2, x3, x4, x5, x6) = U16_gggga(x1, x2, x3, x4, x6)
pF_out_gggga(x1, x2, x3, x4, x5) = pF_out_gggga(x1, x2, x3, x4, x5)
pE_out_gggga(x1, x2, x3, x4, x5) = pE_out_gggga(x1, x2, x3, x4, x5)
pJ_out_ggaga(x1, x2, x3, x4, x5) = pJ_out_ggaga(x1, x2, x3, x4, x5)
pI_out_ggaggaa(x1, x2, x3, x4, x5, x6, x7) = pI_out_ggaggaa(x1, x2, x3, x4, x5, x6, x7)
pB_out_gaagagaa(x1, x2, x3, x4, x5, x6, x7, x8) = pB_out_gaagagaa(x1, x2, x3, x4, x5, x6, x7, x8)
MERGESORTA_IN_GA(x1, x2) = MERGESORTA_IN_GA(x1)
U1_GA(x1, x2, x3, x4, x5) = U1_GA(x1, x2, x3, x5)
PB_IN_GAAGAGAA(x1, x2, x3, x4, x5, x6, x7, x8) = PB_IN_GAAGAGAA(x1, x4, x6)
U7_GAAGAGAA(x1, x2, x3, x4, x5, x6, x7, x8, x9) = U7_GAAGAGAA(x1, x4, x6, x9)
SPLITC_IN_GAA(x1, x2, x3) = SPLITC_IN_GAA(x1)
U2_GAA(x1, x2, x3, x4, x5, x6) = U2_GAA(x1, x2, x3, x6)
U8_GAAGAGAA(x1, x2, x3, x4, x5, x6, x7, x8, x9) = U8_GAAGAGAA(x1, x2, x3, x4, x6, x9)
PI_IN_GGAGGAA(x1, x2, x3, x4, x5, x6, x7) = PI_IN_GGAGGAA(x1, x2, x4, x5)
U9_GGAGGAA(x1, x2, x3, x4, x5, x6, x7, x8) = U9_GGAGGAA(x1, x2, x4, x5, x8)
U10_GGAGGAA(x1, x2, x3, x4, x5, x6, x7, x8) = U10_GGAGGAA(x1, x2, x3, x4, x5, x8)
PJ_IN_GGAGA(x1, x2, x3, x4, x5) = PJ_IN_GGAGA(x1, x2, x4)
U11_GGAGA(x1, x2, x3, x4, x5, x6) = U11_GGAGA(x1, x2, x4, x6)
U12_GGAGA(x1, x2, x3, x4, x5, x6) = U12_GGAGA(x1, x2, x3, x4, x6)
MERGED_IN_GGA(x1, x2, x3) = MERGED_IN_GGA(x1, x2)
U3_GGA(x1, x2, x3, x4, x5, x6) = U3_GGA(x1, x2, x3, x4, x6)
PE_IN_GGGGA(x1, x2, x3, x4, x5) = PE_IN_GGGGA(x1, x2, x3, x4)
U13_GGGGA(x1, x2, x3, x4, x5, x6) = U13_GGGGA(x1, x2, x3, x4, x6)
LEG_IN_GG(x1, x2) = LEG_IN_GG(x1, x2)
U5_GG(x1, x2, x3) = U5_GG(x1, x2, x3)
U14_GGGGA(x1, x2, x3, x4, x5, x6) = U14_GGGGA(x1, x2, x3, x4, x6)
U4_GGA(x1, x2, x3, x4, x5, x6) = U4_GGA(x1, x2, x3, x4, x6)
PF_IN_GGGGA(x1, x2, x3, x4, x5) = PF_IN_GGGGA(x1, x2, x3, x4)
U15_GGGGA(x1, x2, x3, x4, x5, x6) = U15_GGGGA(x1, x2, x3, x4, x6)
GTH_IN_GG(x1, x2) = GTH_IN_GG(x1, x2)
U6_GG(x1, x2, x3) = U6_GG(x1, x2, x3)
U16_GGGGA(x1, x2, x3, x4, x5, x6) = U16_GGGGA(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(.(T22, .(T23, T24)), T14) → U1_GA(T22, T23, T24, T14, pB_in_gaagagaa(T24, X48, X49, T22, X22, T23, X23, T14))
MERGESORTA_IN_GA(.(T22, .(T23, T24)), T14) → PB_IN_GAAGAGAA(T24, X48, X49, T22, X22, T23, X23, T14)
PB_IN_GAAGAGAA(T24, T26, T27, T22, X22, T23, X23, T14) → U7_GAAGAGAA(T24, T26, T27, T22, X22, T23, X23, T14, splitC_in_gaa(T24, T26, T27))
PB_IN_GAAGAGAA(T24, T26, T27, T22, X22, T23, X23, T14) → SPLITC_IN_GAA(T24, T26, T27)
SPLITC_IN_GAA(.(T57, .(T58, T59)), .(T57, X161), .(T58, X162)) → U2_GAA(T57, T58, T59, X161, X162, splitC_in_gaa(T59, X161, X162))
SPLITC_IN_GAA(.(T57, .(T58, T59)), .(T57, X161), .(T58, X162)) → SPLITC_IN_GAA(T59, X161, X162)
U7_GAAGAGAA(T24, T26, T27, T22, X22, T23, X23, T14, splitC_out_gaa(T24, T26, T27)) → U8_GAAGAGAA(T24, T26, T27, T22, X22, T23, X23, T14, pI_in_ggaggaa(T22, T26, X22, T23, T27, X23, T14))
U7_GAAGAGAA(T24, T26, T27, T22, X22, T23, X23, T14, splitC_out_gaa(T24, T26, T27)) → PI_IN_GGAGGAA(T22, T26, X22, T23, T27, X23, T14)
PI_IN_GGAGGAA(T22, T26, T61, T23, T27, X23, T14) → U9_GGAGGAA(T22, T26, T61, T23, T27, X23, T14, mergesortA_in_ga(.(T22, T26), T61))
PI_IN_GGAGGAA(T22, T26, T61, T23, T27, X23, T14) → MERGESORTA_IN_GA(.(T22, T26), T61)
U9_GGAGGAA(T22, T26, T61, T23, T27, X23, T14, mergesortA_out_ga(.(T22, T26), T61)) → U10_GGAGGAA(T22, T26, T61, T23, T27, X23, T14, pJ_in_ggaga(T23, T27, X23, T61, T14))
U9_GGAGGAA(T22, T26, T61, T23, T27, X23, T14, mergesortA_out_ga(.(T22, T26), T61)) → PJ_IN_GGAGA(T23, T27, X23, T61, T14)
PJ_IN_GGAGA(T23, T27, T62, T61, T14) → U11_GGAGA(T23, T27, T62, T61, T14, mergesortA_in_ga(.(T23, T27), T62))
PJ_IN_GGAGA(T23, T27, T62, T61, T14) → MERGESORTA_IN_GA(.(T23, T27), T62)
U11_GGAGA(T23, T27, T62, T61, T14, mergesortA_out_ga(.(T23, T27), T62)) → U12_GGAGA(T23, T27, T62, T61, T14, mergeD_in_gga(T61, T62, T14))
U11_GGAGA(T23, T27, T62, T61, T14, mergesortA_out_ga(.(T23, T27), T62)) → MERGED_IN_GGA(T61, T62, T14)
MERGED_IN_GGA(.(T95, T96), .(T97, T98), .(T95, T100)) → U3_GGA(T95, T96, T97, T98, T100, pE_in_gggga(T95, T97, T96, T98, T100))
MERGED_IN_GGA(.(T95, T96), .(T97, T98), .(T95, T100)) → PE_IN_GGGGA(T95, T97, T96, T98, T100)
PE_IN_GGGGA(T95, T97, T96, T98, T100) → U13_GGGGA(T95, T97, T96, T98, T100, leG_in_gg(T95, T97))
PE_IN_GGGGA(T95, T97, T96, T98, T100) → LEG_IN_GG(T95, T97)
LEG_IN_GG(s(T113), s(T114)) → U5_GG(T113, T114, leG_in_gg(T113, T114))
LEG_IN_GG(s(T113), s(T114)) → LEG_IN_GG(T113, T114)
U13_GGGGA(T95, T97, T96, T98, T100, leG_out_gg(T95, T97)) → U14_GGGGA(T95, T97, T96, T98, T100, mergeD_in_gga(T96, .(T97, T98), T100))
U13_GGGGA(T95, T97, T96, T98, T100, leG_out_gg(T95, T97)) → MERGED_IN_GGA(T96, .(T97, T98), T100)
MERGED_IN_GGA(.(T136, T137), .(T138, T139), .(T138, T141)) → U4_GGA(T136, T137, T138, T139, T141, pF_in_gggga(T136, T138, T137, T139, T141))
MERGED_IN_GGA(.(T136, T137), .(T138, T139), .(T138, T141)) → PF_IN_GGGGA(T136, T138, T137, T139, T141)
PF_IN_GGGGA(T136, T138, T137, T139, T141) → U15_GGGGA(T136, T138, T137, T139, T141, gtH_in_gg(T136, T138))
PF_IN_GGGGA(T136, T138, T137, T139, T141) → GTH_IN_GG(T136, T138)
GTH_IN_GG(s(T154), s(T155)) → U6_GG(T154, T155, gtH_in_gg(T154, T155))
GTH_IN_GG(s(T154), s(T155)) → GTH_IN_GG(T154, T155)
U15_GGGGA(T136, T138, T137, T139, T141, gtH_out_gg(T136, T138)) → U16_GGGGA(T136, T138, T137, T139, T141, mergeD_in_gga(.(T136, T137), T139, T141))
U15_GGGGA(T136, T138, T137, T139, T141, gtH_out_gg(T136, T138)) → MERGED_IN_GGA(.(T136, T137), T139, T141)

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(.(T22, .(T23, T24)), T14) → U1_ga(T22, T23, T24, T14, pB_in_gaagagaa(T24, X48, X49, T22, X22, T23, X23, T14))
pB_in_gaagagaa(T24, T26, T27, T22, X22, T23, X23, T14) → U7_gaagagaa(T24, T26, T27, T22, X22, T23, X23, T14, splitC_in_gaa(T24, T26, T27))
splitC_in_gaa([], [], []) → splitC_out_gaa([], [], [])
splitC_in_gaa(.(T41, []), .(T41, []), []) → splitC_out_gaa(.(T41, []), .(T41, []), [])
splitC_in_gaa(.(T57, .(T58, T59)), .(T57, X161), .(T58, X162)) → U2_gaa(T57, T58, T59, X161, X162, splitC_in_gaa(T59, X161, X162))
U2_gaa(T57, T58, T59, X161, X162, splitC_out_gaa(T59, X161, X162)) → splitC_out_gaa(.(T57, .(T58, T59)), .(T57, X161), .(T58, X162))
U7_gaagagaa(T24, T26, T27, T22, X22, T23, X23, T14, splitC_out_gaa(T24, T26, T27)) → U8_gaagagaa(T24, T26, T27, T22, X22, T23, X23, T14, pI_in_ggaggaa(T22, T26, X22, T23, T27, X23, T14))
pI_in_ggaggaa(T22, T26, T61, T23, T27, X23, T14) → U9_ggaggaa(T22, T26, T61, T23, T27, X23, T14, mergesortA_in_ga(.(T22, T26), T61))
U9_ggaggaa(T22, T26, T61, T23, T27, X23, T14, mergesortA_out_ga(.(T22, T26), T61)) → U10_ggaggaa(T22, T26, T61, T23, T27, X23, T14, pJ_in_ggaga(T23, T27, X23, T61, T14))
pJ_in_ggaga(T23, T27, T62, T61, T14) → U11_ggaga(T23, T27, T62, T61, T14, mergesortA_in_ga(.(T23, T27), T62))
U11_ggaga(T23, T27, T62, T61, T14, mergesortA_out_ga(.(T23, T27), T62)) → U12_ggaga(T23, T27, T62, T61, T14, mergeD_in_gga(T61, T62, T14))
mergeD_in_gga([], T69, T69) → mergeD_out_gga([], T69, T69)
mergeD_in_gga(T74, [], T74) → mergeD_out_gga(T74, [], T74)
mergeD_in_gga(.(T95, T96), .(T97, T98), .(T95, T100)) → U3_gga(T95, T96, T97, T98, T100, pE_in_gggga(T95, T97, T96, T98, T100))
pE_in_gggga(T95, T97, T96, T98, T100) → U13_gggga(T95, T97, T96, T98, T100, leG_in_gg(T95, T97))
leG_in_gg(s(T113), s(T114)) → U5_gg(T113, T114, leG_in_gg(T113, T114))
leG_in_gg(0, s(T121)) → leG_out_gg(0, s(T121))
leG_in_gg(0, 0) → leG_out_gg(0, 0)
U5_gg(T113, T114, leG_out_gg(T113, T114)) → leG_out_gg(s(T113), s(T114))
U13_gggga(T95, T97, T96, T98, T100, leG_out_gg(T95, T97)) → U14_gggga(T95, T97, T96, T98, T100, mergeD_in_gga(T96, .(T97, T98), T100))
mergeD_in_gga(.(T136, T137), .(T138, T139), .(T138, T141)) → U4_gga(T136, T137, T138, T139, T141, pF_in_gggga(T136, T138, T137, T139, T141))
pF_in_gggga(T136, T138, T137, T139, T141) → U15_gggga(T136, T138, T137, T139, T141, gtH_in_gg(T136, T138))
gtH_in_gg(s(T154), s(T155)) → U6_gg(T154, T155, gtH_in_gg(T154, T155))
gtH_in_gg(s(T160), 0) → gtH_out_gg(s(T160), 0)
U6_gg(T154, T155, gtH_out_gg(T154, T155)) → gtH_out_gg(s(T154), s(T155))
U15_gggga(T136, T138, T137, T139, T141, gtH_out_gg(T136, T138)) → U16_gggga(T136, T138, T137, T139, T141, mergeD_in_gga(.(T136, T137), T139, T141))
U16_gggga(T136, T138, T137, T139, T141, mergeD_out_gga(.(T136, T137), T139, T141)) → pF_out_gggga(T136, T138, T137, T139, T141)
U4_gga(T136, T137, T138, T139, T141, pF_out_gggga(T136, T138, T137, T139, T141)) → mergeD_out_gga(.(T136, T137), .(T138, T139), .(T138, T141))
U14_gggga(T95, T97, T96, T98, T100, mergeD_out_gga(T96, .(T97, T98), T100)) → pE_out_gggga(T95, T97, T96, T98, T100)
U3_gga(T95, T96, T97, T98, T100, pE_out_gggga(T95, T97, T96, T98, T100)) → mergeD_out_gga(.(T95, T96), .(T97, T98), .(T95, T100))
U12_ggaga(T23, T27, T62, T61, T14, mergeD_out_gga(T61, T62, T14)) → pJ_out_ggaga(T23, T27, T62, T61, T14)
U10_ggaggaa(T22, T26, T61, T23, T27, X23, T14, pJ_out_ggaga(T23, T27, X23, T61, T14)) → pI_out_ggaggaa(T22, T26, T61, T23, T27, X23, T14)
U8_gaagagaa(T24, T26, T27, T22, X22, T23, X23, T14, pI_out_ggaggaa(T22, T26, X22, T23, T27, X23, T14)) → pB_out_gaagagaa(T24, T26, T27, T22, X22, T23, X23, T14)
U1_ga(T22, T23, T24, T14, pB_out_gaagagaa(T24, X48, X49, T22, X22, T23, X23, T14)) → mergesortA_out_ga(.(T22, .(T23, T24)), T14)

(5) DependencyGraphProof (EQUIVALENT transformation)

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

(6) Complex Obligation (AND)

(7) Obligation:

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

GTH_IN_GG(s(T154), s(T155)) → GTH_IN_GG(T154, T155)

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(.(T22, .(T23, T24)), T14) → U1_ga(T22, T23, T24, T14, pB_in_gaagagaa(T24, X48, X49, T22, X22, T23, X23, T14))
pB_in_gaagagaa(T24, T26, T27, T22, X22, T23, X23, T14) → U7_gaagagaa(T24, T26, T27, T22, X22, T23, X23, T14, splitC_in_gaa(T24, T26, T27))
splitC_in_gaa([], [], []) → splitC_out_gaa([], [], [])
splitC_in_gaa(.(T41, []), .(T41, []), []) → splitC_out_gaa(.(T41, []), .(T41, []), [])
splitC_in_gaa(.(T57, .(T58, T59)), .(T57, X161), .(T58, X162)) → U2_gaa(T57, T58, T59, X161, X162, splitC_in_gaa(T59, X161, X162))
U2_gaa(T57, T58, T59, X161, X162, splitC_out_gaa(T59, X161, X162)) → splitC_out_gaa(.(T57, .(T58, T59)), .(T57, X161), .(T58, X162))
U7_gaagagaa(T24, T26, T27, T22, X22, T23, X23, T14, splitC_out_gaa(T24, T26, T27)) → U8_gaagagaa(T24, T26, T27, T22, X22, T23, X23, T14, pI_in_ggaggaa(T22, T26, X22, T23, T27, X23, T14))
pI_in_ggaggaa(T22, T26, T61, T23, T27, X23, T14) → U9_ggaggaa(T22, T26, T61, T23, T27, X23, T14, mergesortA_in_ga(.(T22, T26), T61))
U9_ggaggaa(T22, T26, T61, T23, T27, X23, T14, mergesortA_out_ga(.(T22, T26), T61)) → U10_ggaggaa(T22, T26, T61, T23, T27, X23, T14, pJ_in_ggaga(T23, T27, X23, T61, T14))
pJ_in_ggaga(T23, T27, T62, T61, T14) → U11_ggaga(T23, T27, T62, T61, T14, mergesortA_in_ga(.(T23, T27), T62))
U11_ggaga(T23, T27, T62, T61, T14, mergesortA_out_ga(.(T23, T27), T62)) → U12_ggaga(T23, T27, T62, T61, T14, mergeD_in_gga(T61, T62, T14))
mergeD_in_gga([], T69, T69) → mergeD_out_gga([], T69, T69)
mergeD_in_gga(T74, [], T74) → mergeD_out_gga(T74, [], T74)
mergeD_in_gga(.(T95, T96), .(T97, T98), .(T95, T100)) → U3_gga(T95, T96, T97, T98, T100, pE_in_gggga(T95, T97, T96, T98, T100))
pE_in_gggga(T95, T97, T96, T98, T100) → U13_gggga(T95, T97, T96, T98, T100, leG_in_gg(T95, T97))
leG_in_gg(s(T113), s(T114)) → U5_gg(T113, T114, leG_in_gg(T113, T114))
leG_in_gg(0, s(T121)) → leG_out_gg(0, s(T121))
leG_in_gg(0, 0) → leG_out_gg(0, 0)
U5_gg(T113, T114, leG_out_gg(T113, T114)) → leG_out_gg(s(T113), s(T114))
U13_gggga(T95, T97, T96, T98, T100, leG_out_gg(T95, T97)) → U14_gggga(T95, T97, T96, T98, T100, mergeD_in_gga(T96, .(T97, T98), T100))
mergeD_in_gga(.(T136, T137), .(T138, T139), .(T138, T141)) → U4_gga(T136, T137, T138, T139, T141, pF_in_gggga(T136, T138, T137, T139, T141))
pF_in_gggga(T136, T138, T137, T139, T141) → U15_gggga(T136, T138, T137, T139, T141, gtH_in_gg(T136, T138))
gtH_in_gg(s(T154), s(T155)) → U6_gg(T154, T155, gtH_in_gg(T154, T155))
gtH_in_gg(s(T160), 0) → gtH_out_gg(s(T160), 0)
U6_gg(T154, T155, gtH_out_gg(T154, T155)) → gtH_out_gg(s(T154), s(T155))
U15_gggga(T136, T138, T137, T139, T141, gtH_out_gg(T136, T138)) → U16_gggga(T136, T138, T137, T139, T141, mergeD_in_gga(.(T136, T137), T139, T141))
U16_gggga(T136, T138, T137, T139, T141, mergeD_out_gga(.(T136, T137), T139, T141)) → pF_out_gggga(T136, T138, T137, T139, T141)
U4_gga(T136, T137, T138, T139, T141, pF_out_gggga(T136, T138, T137, T139, T141)) → mergeD_out_gga(.(T136, T137), .(T138, T139), .(T138, T141))
U14_gggga(T95, T97, T96, T98, T100, mergeD_out_gga(T96, .(T97, T98), T100)) → pE_out_gggga(T95, T97, T96, T98, T100)
U3_gga(T95, T96, T97, T98, T100, pE_out_gggga(T95, T97, T96, T98, T100)) → mergeD_out_gga(.(T95, T96), .(T97, T98), .(T95, T100))
U12_ggaga(T23, T27, T62, T61, T14, mergeD_out_gga(T61, T62, T14)) → pJ_out_ggaga(T23, T27, T62, T61, T14)
U10_ggaggaa(T22, T26, T61, T23, T27, X23, T14, pJ_out_ggaga(T23, T27, X23, T61, T14)) → pI_out_ggaggaa(T22, T26, T61, T23, T27, X23, T14)
U8_gaagagaa(T24, T26, T27, T22, X22, T23, X23, T14, pI_out_ggaggaa(T22, T26, X22, T23, T27, X23, T14)) → pB_out_gaagagaa(T24, T26, T27, T22, X22, T23, X23, T14)
U1_ga(T22, T23, T24, T14, pB_out_gaagagaa(T24, X48, X49, T22, X22, T23, X23, T14)) → mergesortA_out_ga(.(T22, .(T23, T24)), 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:

GTH_IN_GG(s(T154), s(T155)) → GTH_IN_GG(T154, T155)

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

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

GTH_IN_GG(s(T154), s(T155)) → GTH_IN_GG(T154, T155)

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:

GTH_IN_GG(s(T154), s(T155)) → GTH_IN_GG(T154, T155)
The graph contains the following edges 1 > 1, 2 > 2

(13) YES

(14) Obligation:

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

LEG_IN_GG(s(T113), s(T114)) → LEG_IN_GG(T113, T114)

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(.(T22, .(T23, T24)), T14) → U1_ga(T22, T23, T24, T14, pB_in_gaagagaa(T24, X48, X49, T22, X22, T23, X23, T14))
pB_in_gaagagaa(T24, T26, T27, T22, X22, T23, X23, T14) → U7_gaagagaa(T24, T26, T27, T22, X22, T23, X23, T14, splitC_in_gaa(T24, T26, T27))
splitC_in_gaa([], [], []) → splitC_out_gaa([], [], [])
splitC_in_gaa(.(T41, []), .(T41, []), []) → splitC_out_gaa(.(T41, []), .(T41, []), [])
splitC_in_gaa(.(T57, .(T58, T59)), .(T57, X161), .(T58, X162)) → U2_gaa(T57, T58, T59, X161, X162, splitC_in_gaa(T59, X161, X162))
U2_gaa(T57, T58, T59, X161, X162, splitC_out_gaa(T59, X161, X162)) → splitC_out_gaa(.(T57, .(T58, T59)), .(T57, X161), .(T58, X162))
U7_gaagagaa(T24, T26, T27, T22, X22, T23, X23, T14, splitC_out_gaa(T24, T26, T27)) → U8_gaagagaa(T24, T26, T27, T22, X22, T23, X23, T14, pI_in_ggaggaa(T22, T26, X22, T23, T27, X23, T14))
pI_in_ggaggaa(T22, T26, T61, T23, T27, X23, T14) → U9_ggaggaa(T22, T26, T61, T23, T27, X23, T14, mergesortA_in_ga(.(T22, T26), T61))
U9_ggaggaa(T22, T26, T61, T23, T27, X23, T14, mergesortA_out_ga(.(T22, T26), T61)) → U10_ggaggaa(T22, T26, T61, T23, T27, X23, T14, pJ_in_ggaga(T23, T27, X23, T61, T14))
pJ_in_ggaga(T23, T27, T62, T61, T14) → U11_ggaga(T23, T27, T62, T61, T14, mergesortA_in_ga(.(T23, T27), T62))
U11_ggaga(T23, T27, T62, T61, T14, mergesortA_out_ga(.(T23, T27), T62)) → U12_ggaga(T23, T27, T62, T61, T14, mergeD_in_gga(T61, T62, T14))
mergeD_in_gga([], T69, T69) → mergeD_out_gga([], T69, T69)
mergeD_in_gga(T74, [], T74) → mergeD_out_gga(T74, [], T74)
mergeD_in_gga(.(T95, T96), .(T97, T98), .(T95, T100)) → U3_gga(T95, T96, T97, T98, T100, pE_in_gggga(T95, T97, T96, T98, T100))
pE_in_gggga(T95, T97, T96, T98, T100) → U13_gggga(T95, T97, T96, T98, T100, leG_in_gg(T95, T97))
leG_in_gg(s(T113), s(T114)) → U5_gg(T113, T114, leG_in_gg(T113, T114))
leG_in_gg(0, s(T121)) → leG_out_gg(0, s(T121))
leG_in_gg(0, 0) → leG_out_gg(0, 0)
U5_gg(T113, T114, leG_out_gg(T113, T114)) → leG_out_gg(s(T113), s(T114))
U13_gggga(T95, T97, T96, T98, T100, leG_out_gg(T95, T97)) → U14_gggga(T95, T97, T96, T98, T100, mergeD_in_gga(T96, .(T97, T98), T100))
mergeD_in_gga(.(T136, T137), .(T138, T139), .(T138, T141)) → U4_gga(T136, T137, T138, T139, T141, pF_in_gggga(T136, T138, T137, T139, T141))
pF_in_gggga(T136, T138, T137, T139, T141) → U15_gggga(T136, T138, T137, T139, T141, gtH_in_gg(T136, T138))
gtH_in_gg(s(T154), s(T155)) → U6_gg(T154, T155, gtH_in_gg(T154, T155))
gtH_in_gg(s(T160), 0) → gtH_out_gg(s(T160), 0)
U6_gg(T154, T155, gtH_out_gg(T154, T155)) → gtH_out_gg(s(T154), s(T155))
U15_gggga(T136, T138, T137, T139, T141, gtH_out_gg(T136, T138)) → U16_gggga(T136, T138, T137, T139, T141, mergeD_in_gga(.(T136, T137), T139, T141))
U16_gggga(T136, T138, T137, T139, T141, mergeD_out_gga(.(T136, T137), T139, T141)) → pF_out_gggga(T136, T138, T137, T139, T141)
U4_gga(T136, T137, T138, T139, T141, pF_out_gggga(T136, T138, T137, T139, T141)) → mergeD_out_gga(.(T136, T137), .(T138, T139), .(T138, T141))
U14_gggga(T95, T97, T96, T98, T100, mergeD_out_gga(T96, .(T97, T98), T100)) → pE_out_gggga(T95, T97, T96, T98, T100)
U3_gga(T95, T96, T97, T98, T100, pE_out_gggga(T95, T97, T96, T98, T100)) → mergeD_out_gga(.(T95, T96), .(T97, T98), .(T95, T100))
U12_ggaga(T23, T27, T62, T61, T14, mergeD_out_gga(T61, T62, T14)) → pJ_out_ggaga(T23, T27, T62, T61, T14)
U10_ggaggaa(T22, T26, T61, T23, T27, X23, T14, pJ_out_ggaga(T23, T27, X23, T61, T14)) → pI_out_ggaggaa(T22, T26, T61, T23, T27, X23, T14)
U8_gaagagaa(T24, T26, T27, T22, X22, T23, X23, T14, pI_out_ggaggaa(T22, T26, X22, T23, T27, X23, T14)) → pB_out_gaagagaa(T24, T26, T27, T22, X22, T23, X23, T14)
U1_ga(T22, T23, T24, T14, pB_out_gaagagaa(T24, X48, X49, T22, X22, T23, X23, T14)) → mergesortA_out_ga(.(T22, .(T23, T24)), 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:

LEG_IN_GG(s(T113), s(T114)) → LEG_IN_GG(T113, T114)

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:

LEG_IN_GG(s(T113), s(T114)) → LEG_IN_GG(T113, T114)

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:

LEG_IN_GG(s(T113), s(T114)) → LEG_IN_GG(T113, T114)
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:

MERGED_IN_GGA(.(T95, T96), .(T97, T98), .(T95, T100)) → PE_IN_GGGGA(T95, T97, T96, T98, T100)
PE_IN_GGGGA(T95, T97, T96, T98, T100) → U13_GGGGA(T95, T97, T96, T98, T100, leG_in_gg(T95, T97))
U13_GGGGA(T95, T97, T96, T98, T100, leG_out_gg(T95, T97)) → MERGED_IN_GGA(T96, .(T97, T98), T100)
MERGED_IN_GGA(.(T136, T137), .(T138, T139), .(T138, T141)) → PF_IN_GGGGA(T136, T138, T137, T139, T141)
PF_IN_GGGGA(T136, T138, T137, T139, T141) → U15_GGGGA(T136, T138, T137, T139, T141, gtH_in_gg(T136, T138))
U15_GGGGA(T136, T138, T137, T139, T141, gtH_out_gg(T136, T138)) → MERGED_IN_GGA(.(T136, T137), T139, T141)

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(.(T22, .(T23, T24)), T14) → U1_ga(T22, T23, T24, T14, pB_in_gaagagaa(T24, X48, X49, T22, X22, T23, X23, T14))
pB_in_gaagagaa(T24, T26, T27, T22, X22, T23, X23, T14) → U7_gaagagaa(T24, T26, T27, T22, X22, T23, X23, T14, splitC_in_gaa(T24, T26, T27))
splitC_in_gaa([], [], []) → splitC_out_gaa([], [], [])
splitC_in_gaa(.(T41, []), .(T41, []), []) → splitC_out_gaa(.(T41, []), .(T41, []), [])
splitC_in_gaa(.(T57, .(T58, T59)), .(T57, X161), .(T58, X162)) → U2_gaa(T57, T58, T59, X161, X162, splitC_in_gaa(T59, X161, X162))
U2_gaa(T57, T58, T59, X161, X162, splitC_out_gaa(T59, X161, X162)) → splitC_out_gaa(.(T57, .(T58, T59)), .(T57, X161), .(T58, X162))
U7_gaagagaa(T24, T26, T27, T22, X22, T23, X23, T14, splitC_out_gaa(T24, T26, T27)) → U8_gaagagaa(T24, T26, T27, T22, X22, T23, X23, T14, pI_in_ggaggaa(T22, T26, X22, T23, T27, X23, T14))
pI_in_ggaggaa(T22, T26, T61, T23, T27, X23, T14) → U9_ggaggaa(T22, T26, T61, T23, T27, X23, T14, mergesortA_in_ga(.(T22, T26), T61))
U9_ggaggaa(T22, T26, T61, T23, T27, X23, T14, mergesortA_out_ga(.(T22, T26), T61)) → U10_ggaggaa(T22, T26, T61, T23, T27, X23, T14, pJ_in_ggaga(T23, T27, X23, T61, T14))
pJ_in_ggaga(T23, T27, T62, T61, T14) → U11_ggaga(T23, T27, T62, T61, T14, mergesortA_in_ga(.(T23, T27), T62))
U11_ggaga(T23, T27, T62, T61, T14, mergesortA_out_ga(.(T23, T27), T62)) → U12_ggaga(T23, T27, T62, T61, T14, mergeD_in_gga(T61, T62, T14))
mergeD_in_gga([], T69, T69) → mergeD_out_gga([], T69, T69)
mergeD_in_gga(T74, [], T74) → mergeD_out_gga(T74, [], T74)
mergeD_in_gga(.(T95, T96), .(T97, T98), .(T95, T100)) → U3_gga(T95, T96, T97, T98, T100, pE_in_gggga(T95, T97, T96, T98, T100))
pE_in_gggga(T95, T97, T96, T98, T100) → U13_gggga(T95, T97, T96, T98, T100, leG_in_gg(T95, T97))
leG_in_gg(s(T113), s(T114)) → U5_gg(T113, T114, leG_in_gg(T113, T114))
leG_in_gg(0, s(T121)) → leG_out_gg(0, s(T121))
leG_in_gg(0, 0) → leG_out_gg(0, 0)
U5_gg(T113, T114, leG_out_gg(T113, T114)) → leG_out_gg(s(T113), s(T114))
U13_gggga(T95, T97, T96, T98, T100, leG_out_gg(T95, T97)) → U14_gggga(T95, T97, T96, T98, T100, mergeD_in_gga(T96, .(T97, T98), T100))
mergeD_in_gga(.(T136, T137), .(T138, T139), .(T138, T141)) → U4_gga(T136, T137, T138, T139, T141, pF_in_gggga(T136, T138, T137, T139, T141))
pF_in_gggga(T136, T138, T137, T139, T141) → U15_gggga(T136, T138, T137, T139, T141, gtH_in_gg(T136, T138))
gtH_in_gg(s(T154), s(T155)) → U6_gg(T154, T155, gtH_in_gg(T154, T155))
gtH_in_gg(s(T160), 0) → gtH_out_gg(s(T160), 0)
U6_gg(T154, T155, gtH_out_gg(T154, T155)) → gtH_out_gg(s(T154), s(T155))
U15_gggga(T136, T138, T137, T139, T141, gtH_out_gg(T136, T138)) → U16_gggga(T136, T138, T137, T139, T141, mergeD_in_gga(.(T136, T137), T139, T141))
U16_gggga(T136, T138, T137, T139, T141, mergeD_out_gga(.(T136, T137), T139, T141)) → pF_out_gggga(T136, T138, T137, T139, T141)
U4_gga(T136, T137, T138, T139, T141, pF_out_gggga(T136, T138, T137, T139, T141)) → mergeD_out_gga(.(T136, T137), .(T138, T139), .(T138, T141))
U14_gggga(T95, T97, T96, T98, T100, mergeD_out_gga(T96, .(T97, T98), T100)) → pE_out_gggga(T95, T97, T96, T98, T100)
U3_gga(T95, T96, T97, T98, T100, pE_out_gggga(T95, T97, T96, T98, T100)) → mergeD_out_gga(.(T95, T96), .(T97, T98), .(T95, T100))
U12_ggaga(T23, T27, T62, T61, T14, mergeD_out_gga(T61, T62, T14)) → pJ_out_ggaga(T23, T27, T62, T61, T14)
U10_ggaggaa(T22, T26, T61, T23, T27, X23, T14, pJ_out_ggaga(T23, T27, X23, T61, T14)) → pI_out_ggaggaa(T22, T26, T61, T23, T27, X23, T14)
U8_gaagagaa(T24, T26, T27, T22, X22, T23, X23, T14, pI_out_ggaggaa(T22, T26, X22, T23, T27, X23, T14)) → pB_out_gaagagaa(T24, T26, T27, T22, X22, T23, X23, T14)
U1_ga(T22, T23, T24, T14, pB_out_gaagagaa(T24, X48, X49, T22, X22, T23, X23, T14)) → mergesortA_out_ga(.(T22, .(T23, T24)), 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:

MERGED_IN_GGA(.(T95, T96), .(T97, T98), .(T95, T100)) → PE_IN_GGGGA(T95, T97, T96, T98, T100)
PE_IN_GGGGA(T95, T97, T96, T98, T100) → U13_GGGGA(T95, T97, T96, T98, T100, leG_in_gg(T95, T97))
U13_GGGGA(T95, T97, T96, T98, T100, leG_out_gg(T95, T97)) → MERGED_IN_GGA(T96, .(T97, T98), T100)
MERGED_IN_GGA(.(T136, T137), .(T138, T139), .(T138, T141)) → PF_IN_GGGGA(T136, T138, T137, T139, T141)
PF_IN_GGGGA(T136, T138, T137, T139, T141) → U15_GGGGA(T136, T138, T137, T139, T141, gtH_in_gg(T136, T138))
U15_GGGGA(T136, T138, T137, T139, T141, gtH_out_gg(T136, T138)) → MERGED_IN_GGA(.(T136, T137), T139, T141)

The TRS R consists of the following rules:

leG_in_gg(s(T113), s(T114)) → U5_gg(T113, T114, leG_in_gg(T113, T114))
leG_in_gg(0, s(T121)) → leG_out_gg(0, s(T121))
leG_in_gg(0, 0) → leG_out_gg(0, 0)
gtH_in_gg(s(T154), s(T155)) → U6_gg(T154, T155, gtH_in_gg(T154, T155))
gtH_in_gg(s(T160), 0) → gtH_out_gg(s(T160), 0)
U5_gg(T113, T114, leG_out_gg(T113, T114)) → leG_out_gg(s(T113), s(T114))
U6_gg(T154, T155, gtH_out_gg(T154, T155)) → gtH_out_gg(s(T154), s(T155))

The argument filtering Pi contains the following mapping:
.(x1, x2) = .(x1, x2)
leG_in_gg(x1, x2) = leG_in_gg(x1, x2)
s(x1) = s(x1)
U5_gg(x1, x2, x3) = U5_gg(x1, x2, x3)
0 = 0
leG_out_gg(x1, x2) = leG_out_gg(x1, x2)
gtH_in_gg(x1, x2) = gtH_in_gg(x1, x2)
U6_gg(x1, x2, x3) = U6_gg(x1, x2, x3)
gtH_out_gg(x1, x2) = gtH_out_gg(x1, x2)
MERGED_IN_GGA(x1, x2, x3) = MERGED_IN_GGA(x1, x2)
PE_IN_GGGGA(x1, x2, x3, x4, x5) = PE_IN_GGGGA(x1, x2, x3, x4)
U13_GGGGA(x1, x2, x3, x4, x5, x6) = U13_GGGGA(x1, x2, x3, x4, x6)
PF_IN_GGGGA(x1, x2, x3, x4, x5) = PF_IN_GGGGA(x1, x2, x3, x4)
U15_GGGGA(x1, x2, x3, x4, x5, x6) = U15_GGGGA(x1, x2, x3, x4, x6)

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

(24) PiDPToQDPProof (SOUND transformation)

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

(25) Obligation:

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

MERGED_IN_GGA(.(T95, T96), .(T97, T98)) → PE_IN_GGGGA(T95, T97, T96, T98)
PE_IN_GGGGA(T95, T97, T96, T98) → U13_GGGGA(T95, T97, T96, T98, leG_in_gg(T95, T97))
U13_GGGGA(T95, T97, T96, T98, leG_out_gg(T95, T97)) → MERGED_IN_GGA(T96, .(T97, T98))
MERGED_IN_GGA(.(T136, T137), .(T138, T139)) → PF_IN_GGGGA(T136, T138, T137, T139)
PF_IN_GGGGA(T136, T138, T137, T139) → U15_GGGGA(T136, T138, T137, T139, gtH_in_gg(T136, T138))
U15_GGGGA(T136, T138, T137, T139, gtH_out_gg(T136, T138)) → MERGED_IN_GGA(.(T136, T137), T139)

The TRS R consists of the following rules:

leG_in_gg(s(T113), s(T114)) → U5_gg(T113, T114, leG_in_gg(T113, T114))
leG_in_gg(0, s(T121)) → leG_out_gg(0, s(T121))
leG_in_gg(0, 0) → leG_out_gg(0, 0)
gtH_in_gg(s(T154), s(T155)) → U6_gg(T154, T155, gtH_in_gg(T154, T155))
gtH_in_gg(s(T160), 0) → gtH_out_gg(s(T160), 0)
U5_gg(T113, T114, leG_out_gg(T113, T114)) → leG_out_gg(s(T113), s(T114))
U6_gg(T154, T155, gtH_out_gg(T154, T155)) → gtH_out_gg(s(T154), s(T155))

The set Q consists of the following terms:

leG_in_gg(x0, x1)
gtH_in_gg(x0, x1)
U5_gg(x0, x1, x2)
U6_gg(x0, x1, x2)

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

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

MERGED_IN_GGA(.(T95, T96), .(T97, T98)) → PE_IN_GGGGA(T95, T97, T96, T98)
MERGED_IN_GGA(.(T136, T137), .(T138, T139)) → PF_IN_GGGGA(T136, T138, T137, T139)

Used ordering: Polynomial interpretation [POLO]:

POL(.(x₁, x₂)) = 1 + 2·x₁ + 2·x₂
POL(0) = 0
POL(MERGED_IN_GGA(x₁, x₂)) = x₁ + x₂
POL(PE_IN_GGGGA(x₁, x₂, x₃, x₄)) = 1 + 2·x₁ + 2·x₂ + 2·x₃ + 2·x₄
POL(PF_IN_GGGGA(x₁, x₂, x₃, x₄)) = 1 + 2·x₁ + 2·x₂ + 2·x₃ + 2·x₄
POL(U13_GGGGA(x₁, x₂, x₃, x₄, x₅)) = 1 + x₁ + x₂ + 2·x₃ + 2·x₄ + x₅
POL(U15_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(gtH_in_gg(x₁, x₂)) = x₁ + x₂
POL(gtH_out_gg(x₁, x₂)) = x₁ + x₂
POL(leG_in_gg(x₁, x₂)) = x₁ + x₂
POL(leG_out_gg(x₁, x₂)) = x₁ + x₂
POL(s(x₁)) = 2·x₁

(27) Obligation:

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

PE_IN_GGGGA(T95, T97, T96, T98) → U13_GGGGA(T95, T97, T96, T98, leG_in_gg(T95, T97))
U13_GGGGA(T95, T97, T96, T98, leG_out_gg(T95, T97)) → MERGED_IN_GGA(T96, .(T97, T98))
PF_IN_GGGGA(T136, T138, T137, T139) → U15_GGGGA(T136, T138, T137, T139, gtH_in_gg(T136, T138))
U15_GGGGA(T136, T138, T137, T139, gtH_out_gg(T136, T138)) → MERGED_IN_GGA(.(T136, T137), T139)

The TRS R consists of the following rules:

leG_in_gg(s(T113), s(T114)) → U5_gg(T113, T114, leG_in_gg(T113, T114))
leG_in_gg(0, s(T121)) → leG_out_gg(0, s(T121))
leG_in_gg(0, 0) → leG_out_gg(0, 0)
gtH_in_gg(s(T154), s(T155)) → U6_gg(T154, T155, gtH_in_gg(T154, T155))
gtH_in_gg(s(T160), 0) → gtH_out_gg(s(T160), 0)
U5_gg(T113, T114, leG_out_gg(T113, T114)) → leG_out_gg(s(T113), s(T114))
U6_gg(T154, T155, gtH_out_gg(T154, T155)) → gtH_out_gg(s(T154), s(T155))

The set Q consists of the following terms:

leG_in_gg(x0, x1)
gtH_in_gg(x0, x1)
U5_gg(x0, x1, x2)
U6_gg(x0, x1, x2)

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

(28) DependencyGraphProof (EQUIVALENT transformation)

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

(29) TRUE

(30) Obligation:

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

SPLITC_IN_GAA(.(T57, .(T58, T59)), .(T57, X161), .(T58, X162)) → SPLITC_IN_GAA(T59, X161, X162)

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(.(T22, .(T23, T24)), T14) → U1_ga(T22, T23, T24, T14, pB_in_gaagagaa(T24, X48, X49, T22, X22, T23, X23, T14))
pB_in_gaagagaa(T24, T26, T27, T22, X22, T23, X23, T14) → U7_gaagagaa(T24, T26, T27, T22, X22, T23, X23, T14, splitC_in_gaa(T24, T26, T27))
splitC_in_gaa([], [], []) → splitC_out_gaa([], [], [])
splitC_in_gaa(.(T41, []), .(T41, []), []) → splitC_out_gaa(.(T41, []), .(T41, []), [])
splitC_in_gaa(.(T57, .(T58, T59)), .(T57, X161), .(T58, X162)) → U2_gaa(T57, T58, T59, X161, X162, splitC_in_gaa(T59, X161, X162))
U2_gaa(T57, T58, T59, X161, X162, splitC_out_gaa(T59, X161, X162)) → splitC_out_gaa(.(T57, .(T58, T59)), .(T57, X161), .(T58, X162))
U7_gaagagaa(T24, T26, T27, T22, X22, T23, X23, T14, splitC_out_gaa(T24, T26, T27)) → U8_gaagagaa(T24, T26, T27, T22, X22, T23, X23, T14, pI_in_ggaggaa(T22, T26, X22, T23, T27, X23, T14))
pI_in_ggaggaa(T22, T26, T61, T23, T27, X23, T14) → U9_ggaggaa(T22, T26, T61, T23, T27, X23, T14, mergesortA_in_ga(.(T22, T26), T61))
U9_ggaggaa(T22, T26, T61, T23, T27, X23, T14, mergesortA_out_ga(.(T22, T26), T61)) → U10_ggaggaa(T22, T26, T61, T23, T27, X23, T14, pJ_in_ggaga(T23, T27, X23, T61, T14))
pJ_in_ggaga(T23, T27, T62, T61, T14) → U11_ggaga(T23, T27, T62, T61, T14, mergesortA_in_ga(.(T23, T27), T62))
U11_ggaga(T23, T27, T62, T61, T14, mergesortA_out_ga(.(T23, T27), T62)) → U12_ggaga(T23, T27, T62, T61, T14, mergeD_in_gga(T61, T62, T14))
mergeD_in_gga([], T69, T69) → mergeD_out_gga([], T69, T69)
mergeD_in_gga(T74, [], T74) → mergeD_out_gga(T74, [], T74)
mergeD_in_gga(.(T95, T96), .(T97, T98), .(T95, T100)) → U3_gga(T95, T96, T97, T98, T100, pE_in_gggga(T95, T97, T96, T98, T100))
pE_in_gggga(T95, T97, T96, T98, T100) → U13_gggga(T95, T97, T96, T98, T100, leG_in_gg(T95, T97))
leG_in_gg(s(T113), s(T114)) → U5_gg(T113, T114, leG_in_gg(T113, T114))
leG_in_gg(0, s(T121)) → leG_out_gg(0, s(T121))
leG_in_gg(0, 0) → leG_out_gg(0, 0)
U5_gg(T113, T114, leG_out_gg(T113, T114)) → leG_out_gg(s(T113), s(T114))
U13_gggga(T95, T97, T96, T98, T100, leG_out_gg(T95, T97)) → U14_gggga(T95, T97, T96, T98, T100, mergeD_in_gga(T96, .(T97, T98), T100))
mergeD_in_gga(.(T136, T137), .(T138, T139), .(T138, T141)) → U4_gga(T136, T137, T138, T139, T141, pF_in_gggga(T136, T138, T137, T139, T141))
pF_in_gggga(T136, T138, T137, T139, T141) → U15_gggga(T136, T138, T137, T139, T141, gtH_in_gg(T136, T138))
gtH_in_gg(s(T154), s(T155)) → U6_gg(T154, T155, gtH_in_gg(T154, T155))
gtH_in_gg(s(T160), 0) → gtH_out_gg(s(T160), 0)
U6_gg(T154, T155, gtH_out_gg(T154, T155)) → gtH_out_gg(s(T154), s(T155))
U15_gggga(T136, T138, T137, T139, T141, gtH_out_gg(T136, T138)) → U16_gggga(T136, T138, T137, T139, T141, mergeD_in_gga(.(T136, T137), T139, T141))
U16_gggga(T136, T138, T137, T139, T141, mergeD_out_gga(.(T136, T137), T139, T141)) → pF_out_gggga(T136, T138, T137, T139, T141)
U4_gga(T136, T137, T138, T139, T141, pF_out_gggga(T136, T138, T137, T139, T141)) → mergeD_out_gga(.(T136, T137), .(T138, T139), .(T138, T141))
U14_gggga(T95, T97, T96, T98, T100, mergeD_out_gga(T96, .(T97, T98), T100)) → pE_out_gggga(T95, T97, T96, T98, T100)
U3_gga(T95, T96, T97, T98, T100, pE_out_gggga(T95, T97, T96, T98, T100)) → mergeD_out_gga(.(T95, T96), .(T97, T98), .(T95, T100))
U12_ggaga(T23, T27, T62, T61, T14, mergeD_out_gga(T61, T62, T14)) → pJ_out_ggaga(T23, T27, T62, T61, T14)
U10_ggaggaa(T22, T26, T61, T23, T27, X23, T14, pJ_out_ggaga(T23, T27, X23, T61, T14)) → pI_out_ggaggaa(T22, T26, T61, T23, T27, X23, T14)
U8_gaagagaa(T24, T26, T27, T22, X22, T23, X23, T14, pI_out_ggaggaa(T22, T26, X22, T23, T27, X23, T14)) → pB_out_gaagagaa(T24, T26, T27, T22, X22, T23, X23, T14)
U1_ga(T22, T23, T24, T14, pB_out_gaagagaa(T24, X48, X49, T22, X22, T23, X23, T14)) → mergesortA_out_ga(.(T22, .(T23, T24)), T14)

(31) UsableRulesProof (EQUIVALENT transformation)

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

(32) Obligation:

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

SPLITC_IN_GAA(.(T57, .(T58, T59)), .(T57, X161), .(T58, X162)) → SPLITC_IN_GAA(T59, X161, X162)

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

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

(33) PiDPToQDPProof (SOUND transformation)

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

(34) Obligation:

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

SPLITC_IN_GAA(.(T57, .(T58, T59))) → SPLITC_IN_GAA(T59)

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

(35) QDPSizeChangeProof (EQUIVALENT transformation)

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

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

SPLITC_IN_GAA(.(T57, .(T58, T59))) → SPLITC_IN_GAA(T59)
The graph contains the following edges 1 > 1

(36) YES

(37) Obligation:

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

MERGESORTA_IN_GA(.(T22, .(T23, T24)), T14) → PB_IN_GAAGAGAA(T24, X48, X49, T22, X22, T23, X23, T14)
PB_IN_GAAGAGAA(T24, T26, T27, T22, X22, T23, X23, T14) → U7_GAAGAGAA(T24, T26, T27, T22, X22, T23, X23, T14, splitC_in_gaa(T24, T26, T27))
U7_GAAGAGAA(T24, T26, T27, T22, X22, T23, X23, T14, splitC_out_gaa(T24, T26, T27)) → PI_IN_GGAGGAA(T22, T26, X22, T23, T27, X23, T14)
PI_IN_GGAGGAA(T22, T26, T61, T23, T27, X23, T14) → U9_GGAGGAA(T22, T26, T61, T23, T27, X23, T14, mergesortA_in_ga(.(T22, T26), T61))
U9_GGAGGAA(T22, T26, T61, T23, T27, X23, T14, mergesortA_out_ga(.(T22, T26), T61)) → PJ_IN_GGAGA(T23, T27, X23, T61, T14)
PJ_IN_GGAGA(T23, T27, T62, T61, T14) → MERGESORTA_IN_GA(.(T23, T27), T62)
PI_IN_GGAGGAA(T22, T26, T61, T23, T27, X23, T14) → MERGESORTA_IN_GA(.(T22, T26), T61)

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(.(T22, .(T23, T24)), T14) → U1_ga(T22, T23, T24, T14, pB_in_gaagagaa(T24, X48, X49, T22, X22, T23, X23, T14))
pB_in_gaagagaa(T24, T26, T27, T22, X22, T23, X23, T14) → U7_gaagagaa(T24, T26, T27, T22, X22, T23, X23, T14, splitC_in_gaa(T24, T26, T27))
splitC_in_gaa([], [], []) → splitC_out_gaa([], [], [])
splitC_in_gaa(.(T41, []), .(T41, []), []) → splitC_out_gaa(.(T41, []), .(T41, []), [])
splitC_in_gaa(.(T57, .(T58, T59)), .(T57, X161), .(T58, X162)) → U2_gaa(T57, T58, T59, X161, X162, splitC_in_gaa(T59, X161, X162))
U2_gaa(T57, T58, T59, X161, X162, splitC_out_gaa(T59, X161, X162)) → splitC_out_gaa(.(T57, .(T58, T59)), .(T57, X161), .(T58, X162))
U7_gaagagaa(T24, T26, T27, T22, X22, T23, X23, T14, splitC_out_gaa(T24, T26, T27)) → U8_gaagagaa(T24, T26, T27, T22, X22, T23, X23, T14, pI_in_ggaggaa(T22, T26, X22, T23, T27, X23, T14))
pI_in_ggaggaa(T22, T26, T61, T23, T27, X23, T14) → U9_ggaggaa(T22, T26, T61, T23, T27, X23, T14, mergesortA_in_ga(.(T22, T26), T61))
U9_ggaggaa(T22, T26, T61, T23, T27, X23, T14, mergesortA_out_ga(.(T22, T26), T61)) → U10_ggaggaa(T22, T26, T61, T23, T27, X23, T14, pJ_in_ggaga(T23, T27, X23, T61, T14))
pJ_in_ggaga(T23, T27, T62, T61, T14) → U11_ggaga(T23, T27, T62, T61, T14, mergesortA_in_ga(.(T23, T27), T62))
U11_ggaga(T23, T27, T62, T61, T14, mergesortA_out_ga(.(T23, T27), T62)) → U12_ggaga(T23, T27, T62, T61, T14, mergeD_in_gga(T61, T62, T14))
mergeD_in_gga([], T69, T69) → mergeD_out_gga([], T69, T69)
mergeD_in_gga(T74, [], T74) → mergeD_out_gga(T74, [], T74)
mergeD_in_gga(.(T95, T96), .(T97, T98), .(T95, T100)) → U3_gga(T95, T96, T97, T98, T100, pE_in_gggga(T95, T97, T96, T98, T100))
pE_in_gggga(T95, T97, T96, T98, T100) → U13_gggga(T95, T97, T96, T98, T100, leG_in_gg(T95, T97))
leG_in_gg(s(T113), s(T114)) → U5_gg(T113, T114, leG_in_gg(T113, T114))
leG_in_gg(0, s(T121)) → leG_out_gg(0, s(T121))
leG_in_gg(0, 0) → leG_out_gg(0, 0)
U5_gg(T113, T114, leG_out_gg(T113, T114)) → leG_out_gg(s(T113), s(T114))
U13_gggga(T95, T97, T96, T98, T100, leG_out_gg(T95, T97)) → U14_gggga(T95, T97, T96, T98, T100, mergeD_in_gga(T96, .(T97, T98), T100))
mergeD_in_gga(.(T136, T137), .(T138, T139), .(T138, T141)) → U4_gga(T136, T137, T138, T139, T141, pF_in_gggga(T136, T138, T137, T139, T141))
pF_in_gggga(T136, T138, T137, T139, T141) → U15_gggga(T136, T138, T137, T139, T141, gtH_in_gg(T136, T138))
gtH_in_gg(s(T154), s(T155)) → U6_gg(T154, T155, gtH_in_gg(T154, T155))
gtH_in_gg(s(T160), 0) → gtH_out_gg(s(T160), 0)
U6_gg(T154, T155, gtH_out_gg(T154, T155)) → gtH_out_gg(s(T154), s(T155))
U15_gggga(T136, T138, T137, T139, T141, gtH_out_gg(T136, T138)) → U16_gggga(T136, T138, T137, T139, T141, mergeD_in_gga(.(T136, T137), T139, T141))
U16_gggga(T136, T138, T137, T139, T141, mergeD_out_gga(.(T136, T137), T139, T141)) → pF_out_gggga(T136, T138, T137, T139, T141)
U4_gga(T136, T137, T138, T139, T141, pF_out_gggga(T136, T138, T137, T139, T141)) → mergeD_out_gga(.(T136, T137), .(T138, T139), .(T138, T141))
U14_gggga(T95, T97, T96, T98, T100, mergeD_out_gga(T96, .(T97, T98), T100)) → pE_out_gggga(T95, T97, T96, T98, T100)
U3_gga(T95, T96, T97, T98, T100, pE_out_gggga(T95, T97, T96, T98, T100)) → mergeD_out_gga(.(T95, T96), .(T97, T98), .(T95, T100))
U12_ggaga(T23, T27, T62, T61, T14, mergeD_out_gga(T61, T62, T14)) → pJ_out_ggaga(T23, T27, T62, T61, T14)
U10_ggaggaa(T22, T26, T61, T23, T27, X23, T14, pJ_out_ggaga(T23, T27, X23, T61, T14)) → pI_out_ggaggaa(T22, T26, T61, T23, T27, X23, T14)
U8_gaagagaa(T24, T26, T27, T22, X22, T23, X23, T14, pI_out_ggaggaa(T22, T26, X22, T23, T27, X23, T14)) → pB_out_gaagagaa(T24, T26, T27, T22, X22, T23, X23, T14)
U1_ga(T22, T23, T24, T14, pB_out_gaagagaa(T24, X48, X49, T22, X22, T23, X23, T14)) → mergesortA_out_ga(.(T22, .(T23, T24)), T14)

The argument filtering Pi contains the following mapping:
mergesortA_in_ga(x1, x2) = mergesortA_in_ga(x1)
[] = []
mergesortA_out_ga(x1, x2) = mergesortA_out_ga(x1, x2)
.(x1, x2) = .(x1, x2)
U1_ga(x1, x2, x3, x4, x5) = U1_ga(x1, x2, x3, x5)
pB_in_gaagagaa(x1, x2, x3, x4, x5, x6, x7, x8) = pB_in_gaagagaa(x1, x4, x6)
U7_gaagagaa(x1, x2, x3, x4, x5, x6, x7, x8, x9) = U7_gaagagaa(x1, x4, x6, x9)
splitC_in_gaa(x1, x2, x3) = splitC_in_gaa(x1)
splitC_out_gaa(x1, x2, x3) = splitC_out_gaa(x1, x2, x3)
U2_gaa(x1, x2, x3, x4, x5, x6) = U2_gaa(x1, x2, x3, x6)
U8_gaagagaa(x1, x2, x3, x4, x5, x6, x7, x8, x9) = U8_gaagagaa(x1, x2, x3, x4, x6, x9)
pI_in_ggaggaa(x1, x2, x3, x4, x5, x6, x7) = pI_in_ggaggaa(x1, x2, x4, x5)
U9_ggaggaa(x1, x2, x3, x4, x5, x6, x7, x8) = U9_ggaggaa(x1, x2, x4, x5, x8)
U10_ggaggaa(x1, x2, x3, x4, x5, x6, x7, x8) = U10_ggaggaa(x1, x2, x3, x4, x5, x8)
pJ_in_ggaga(x1, x2, x3, x4, x5) = pJ_in_ggaga(x1, x2, x4)
U11_ggaga(x1, x2, x3, x4, x5, x6) = U11_ggaga(x1, x2, x4, x6)
U12_ggaga(x1, x2, x3, x4, x5, x6) = U12_ggaga(x1, x2, x3, x4, x6)
mergeD_in_gga(x1, x2, x3) = mergeD_in_gga(x1, x2)
mergeD_out_gga(x1, x2, x3) = mergeD_out_gga(x1, x2, x3)
U3_gga(x1, x2, x3, x4, x5, x6) = U3_gga(x1, x2, x3, x4, x6)
pE_in_gggga(x1, x2, x3, x4, x5) = pE_in_gggga(x1, x2, x3, x4)
U13_gggga(x1, x2, x3, x4, x5, x6) = U13_gggga(x1, x2, x3, x4, x6)
leG_in_gg(x1, x2) = leG_in_gg(x1, x2)
s(x1) = s(x1)
U5_gg(x1, x2, x3) = U5_gg(x1, x2, x3)
0 = 0
leG_out_gg(x1, x2) = leG_out_gg(x1, x2)
U14_gggga(x1, x2, x3, x4, x5, x6) = U14_gggga(x1, x2, x3, x4, x6)
U4_gga(x1, x2, x3, x4, x5, x6) = U4_gga(x1, x2, x3, x4, x6)
pF_in_gggga(x1, x2, x3, x4, x5) = pF_in_gggga(x1, x2, x3, x4)
U15_gggga(x1, x2, x3, x4, x5, x6) = U15_gggga(x1, x2, x3, x4, x6)
gtH_in_gg(x1, x2) = gtH_in_gg(x1, x2)
U6_gg(x1, x2, x3) = U6_gg(x1, x2, x3)
gtH_out_gg(x1, x2) = gtH_out_gg(x1, x2)
U16_gggga(x1, x2, x3, x4, x5, x6) = U16_gggga(x1, x2, x3, x4, x6)
pF_out_gggga(x1, x2, x3, x4, x5) = pF_out_gggga(x1, x2, x3, x4, x5)
pE_out_gggga(x1, x2, x3, x4, x5) = pE_out_gggga(x1, x2, x3, x4, x5)
pJ_out_ggaga(x1, x2, x3, x4, x5) = pJ_out_ggaga(x1, x2, x3, x4, x5)
pI_out_ggaggaa(x1, x2, x3, x4, x5, x6, x7) = pI_out_ggaggaa(x1, x2, x3, x4, x5, x6, x7)
pB_out_gaagagaa(x1, x2, x3, x4, x5, x6, x7, x8) = pB_out_gaagagaa(x1, x2, x3, x4, x5, x6, x7, x8)
MERGESORTA_IN_GA(x1, x2) = MERGESORTA_IN_GA(x1)
PB_IN_GAAGAGAA(x1, x2, x3, x4, x5, x6, x7, x8) = PB_IN_GAAGAGAA(x1, x4, x6)
U7_GAAGAGAA(x1, x2, x3, x4, x5, x6, x7, x8, x9) = U7_GAAGAGAA(x1, x4, x6, x9)
PI_IN_GGAGGAA(x1, x2, x3, x4, x5, x6, x7) = PI_IN_GGAGGAA(x1, x2, x4, x5)
U9_GGAGGAA(x1, x2, x3, x4, x5, x6, x7, x8) = U9_GGAGGAA(x1, x2, x4, x5, x8)
PJ_IN_GGAGA(x1, x2, x3, x4, x5) = PJ_IN_GGAGA(x1, x2, x4)

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

(38) UsableRulesProof (EQUIVALENT transformation)

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

(39) Obligation:

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

MERGESORTA_IN_GA(.(T22, .(T23, T24)), T14) → PB_IN_GAAGAGAA(T24, X48, X49, T22, X22, T23, X23, T14)
PB_IN_GAAGAGAA(T24, T26, T27, T22, X22, T23, X23, T14) → U7_GAAGAGAA(T24, T26, T27, T22, X22, T23, X23, T14, splitC_in_gaa(T24, T26, T27))
U7_GAAGAGAA(T24, T26, T27, T22, X22, T23, X23, T14, splitC_out_gaa(T24, T26, T27)) → PI_IN_GGAGGAA(T22, T26, X22, T23, T27, X23, T14)
PI_IN_GGAGGAA(T22, T26, T61, T23, T27, X23, T14) → U9_GGAGGAA(T22, T26, T61, T23, T27, X23, T14, mergesortA_in_ga(.(T22, T26), T61))
U9_GGAGGAA(T22, T26, T61, T23, T27, X23, T14, mergesortA_out_ga(.(T22, T26), T61)) → PJ_IN_GGAGA(T23, T27, X23, T61, T14)
PJ_IN_GGAGA(T23, T27, T62, T61, T14) → MERGESORTA_IN_GA(.(T23, T27), T62)
PI_IN_GGAGGAA(T22, T26, T61, T23, T27, X23, T14) → MERGESORTA_IN_GA(.(T22, T26), T61)

The TRS R consists of the following rules:

splitC_in_gaa([], [], []) → splitC_out_gaa([], [], [])
splitC_in_gaa(.(T41, []), .(T41, []), []) → splitC_out_gaa(.(T41, []), .(T41, []), [])
splitC_in_gaa(.(T57, .(T58, T59)), .(T57, X161), .(T58, X162)) → U2_gaa(T57, T58, T59, X161, X162, splitC_in_gaa(T59, X161, X162))
mergesortA_in_ga(.(T4, []), .(T4, [])) → mergesortA_out_ga(.(T4, []), .(T4, []))
mergesortA_in_ga(.(T22, .(T23, T24)), T14) → U1_ga(T22, T23, T24, T14, pB_in_gaagagaa(T24, X48, X49, T22, X22, T23, X23, T14))
U2_gaa(T57, T58, T59, X161, X162, splitC_out_gaa(T59, X161, X162)) → splitC_out_gaa(.(T57, .(T58, T59)), .(T57, X161), .(T58, X162))
U1_ga(T22, T23, T24, T14, pB_out_gaagagaa(T24, X48, X49, T22, X22, T23, X23, T14)) → mergesortA_out_ga(.(T22, .(T23, T24)), T14)
pB_in_gaagagaa(T24, T26, T27, T22, X22, T23, X23, T14) → U7_gaagagaa(T24, T26, T27, T22, X22, T23, X23, T14, splitC_in_gaa(T24, T26, T27))
U7_gaagagaa(T24, T26, T27, T22, X22, T23, X23, T14, splitC_out_gaa(T24, T26, T27)) → U8_gaagagaa(T24, T26, T27, T22, X22, T23, X23, T14, pI_in_ggaggaa(T22, T26, X22, T23, T27, X23, T14))
U8_gaagagaa(T24, T26, T27, T22, X22, T23, X23, T14, pI_out_ggaggaa(T22, T26, X22, T23, T27, X23, T14)) → pB_out_gaagagaa(T24, T26, T27, T22, X22, T23, X23, T14)
pI_in_ggaggaa(T22, T26, T61, T23, T27, X23, T14) → U9_ggaggaa(T22, T26, T61, T23, T27, X23, T14, mergesortA_in_ga(.(T22, T26), T61))
U9_ggaggaa(T22, T26, T61, T23, T27, X23, T14, mergesortA_out_ga(.(T22, T26), T61)) → U10_ggaggaa(T22, T26, T61, T23, T27, X23, T14, pJ_in_ggaga(T23, T27, X23, T61, T14))
U10_ggaggaa(T22, T26, T61, T23, T27, X23, T14, pJ_out_ggaga(T23, T27, X23, T61, T14)) → pI_out_ggaggaa(T22, T26, T61, T23, T27, X23, T14)
pJ_in_ggaga(T23, T27, T62, T61, T14) → U11_ggaga(T23, T27, T62, T61, T14, mergesortA_in_ga(.(T23, T27), T62))
U11_ggaga(T23, T27, T62, T61, T14, mergesortA_out_ga(.(T23, T27), T62)) → U12_ggaga(T23, T27, T62, T61, T14, mergeD_in_gga(T61, T62, T14))
U12_ggaga(T23, T27, T62, T61, T14, mergeD_out_gga(T61, T62, T14)) → pJ_out_ggaga(T23, T27, T62, T61, T14)
mergeD_in_gga([], T69, T69) → mergeD_out_gga([], T69, T69)
mergeD_in_gga(T74, [], T74) → mergeD_out_gga(T74, [], T74)
mergeD_in_gga(.(T95, T96), .(T97, T98), .(T95, T100)) → U3_gga(T95, T96, T97, T98, T100, pE_in_gggga(T95, T97, T96, T98, T100))
mergeD_in_gga(.(T136, T137), .(T138, T139), .(T138, T141)) → U4_gga(T136, T137, T138, T139, T141, pF_in_gggga(T136, T138, T137, T139, T141))
U3_gga(T95, T96, T97, T98, T100, pE_out_gggga(T95, T97, T96, T98, T100)) → mergeD_out_gga(.(T95, T96), .(T97, T98), .(T95, T100))
U4_gga(T136, T137, T138, T139, T141, pF_out_gggga(T136, T138, T137, T139, T141)) → mergeD_out_gga(.(T136, T137), .(T138, T139), .(T138, T141))
pE_in_gggga(T95, T97, T96, T98, T100) → U13_gggga(T95, T97, T96, T98, T100, leG_in_gg(T95, T97))
pF_in_gggga(T136, T138, T137, T139, T141) → U15_gggga(T136, T138, T137, T139, T141, gtH_in_gg(T136, T138))
U13_gggga(T95, T97, T96, T98, T100, leG_out_gg(T95, T97)) → U14_gggga(T95, T97, T96, T98, T100, mergeD_in_gga(T96, .(T97, T98), T100))
U15_gggga(T136, T138, T137, T139, T141, gtH_out_gg(T136, T138)) → U16_gggga(T136, T138, T137, T139, T141, mergeD_in_gga(.(T136, T137), T139, T141))
leG_in_gg(s(T113), s(T114)) → U5_gg(T113, T114, leG_in_gg(T113, T114))
leG_in_gg(0, s(T121)) → leG_out_gg(0, s(T121))
leG_in_gg(0, 0) → leG_out_gg(0, 0)
U14_gggga(T95, T97, T96, T98, T100, mergeD_out_gga(T96, .(T97, T98), T100)) → pE_out_gggga(T95, T97, T96, T98, T100)
gtH_in_gg(s(T154), s(T155)) → U6_gg(T154, T155, gtH_in_gg(T154, T155))
gtH_in_gg(s(T160), 0) → gtH_out_gg(s(T160), 0)
U16_gggga(T136, T138, T137, T139, T141, mergeD_out_gga(.(T136, T137), T139, T141)) → pF_out_gggga(T136, T138, T137, T139, T141)
U5_gg(T113, T114, leG_out_gg(T113, T114)) → leG_out_gg(s(T113), s(T114))
U6_gg(T154, T155, gtH_out_gg(T154, T155)) → gtH_out_gg(s(T154), s(T155))

The argument filtering Pi contains the following mapping:
mergesortA_in_ga(x1, x2) = mergesortA_in_ga(x1)
[] = []
mergesortA_out_ga(x1, x2) = mergesortA_out_ga(x1, x2)
.(x1, x2) = .(x1, x2)
U1_ga(x1, x2, x3, x4, x5) = U1_ga(x1, x2, x3, x5)
pB_in_gaagagaa(x1, x2, x3, x4, x5, x6, x7, x8) = pB_in_gaagagaa(x1, x4, x6)
U7_gaagagaa(x1, x2, x3, x4, x5, x6, x7, x8, x9) = U7_gaagagaa(x1, x4, x6, x9)
splitC_in_gaa(x1, x2, x3) = splitC_in_gaa(x1)
splitC_out_gaa(x1, x2, x3) = splitC_out_gaa(x1, x2, x3)
U2_gaa(x1, x2, x3, x4, x5, x6) = U2_gaa(x1, x2, x3, x6)
U8_gaagagaa(x1, x2, x3, x4, x5, x6, x7, x8, x9) = U8_gaagagaa(x1, x2, x3, x4, x6, x9)
pI_in_ggaggaa(x1, x2, x3, x4, x5, x6, x7) = pI_in_ggaggaa(x1, x2, x4, x5)
U9_ggaggaa(x1, x2, x3, x4, x5, x6, x7, x8) = U9_ggaggaa(x1, x2, x4, x5, x8)
U10_ggaggaa(x1, x2, x3, x4, x5, x6, x7, x8) = U10_ggaggaa(x1, x2, x3, x4, x5, x8)
pJ_in_ggaga(x1, x2, x3, x4, x5) = pJ_in_ggaga(x1, x2, x4)
U11_ggaga(x1, x2, x3, x4, x5, x6) = U11_ggaga(x1, x2, x4, x6)
U12_ggaga(x1, x2, x3, x4, x5, x6) = U12_ggaga(x1, x2, x3, x4, x6)
mergeD_in_gga(x1, x2, x3) = mergeD_in_gga(x1, x2)
mergeD_out_gga(x1, x2, x3) = mergeD_out_gga(x1, x2, x3)
U3_gga(x1, x2, x3, x4, x5, x6) = U3_gga(x1, x2, x3, x4, x6)
pE_in_gggga(x1, x2, x3, x4, x5) = pE_in_gggga(x1, x2, x3, x4)
U13_gggga(x1, x2, x3, x4, x5, x6) = U13_gggga(x1, x2, x3, x4, x6)
leG_in_gg(x1, x2) = leG_in_gg(x1, x2)
s(x1) = s(x1)
U5_gg(x1, x2, x3) = U5_gg(x1, x2, x3)
0 = 0
leG_out_gg(x1, x2) = leG_out_gg(x1, x2)
U14_gggga(x1, x2, x3, x4, x5, x6) = U14_gggga(x1, x2, x3, x4, x6)
U4_gga(x1, x2, x3, x4, x5, x6) = U4_gga(x1, x2, x3, x4, x6)
pF_in_gggga(x1, x2, x3, x4, x5) = pF_in_gggga(x1, x2, x3, x4)
U15_gggga(x1, x2, x3, x4, x5, x6) = U15_gggga(x1, x2, x3, x4, x6)
gtH_in_gg(x1, x2) = gtH_in_gg(x1, x2)
U6_gg(x1, x2, x3) = U6_gg(x1, x2, x3)
gtH_out_gg(x1, x2) = gtH_out_gg(x1, x2)
U16_gggga(x1, x2, x3, x4, x5, x6) = U16_gggga(x1, x2, x3, x4, x6)
pF_out_gggga(x1, x2, x3, x4, x5) = pF_out_gggga(x1, x2, x3, x4, x5)
pE_out_gggga(x1, x2, x3, x4, x5) = pE_out_gggga(x1, x2, x3, x4, x5)
pJ_out_ggaga(x1, x2, x3, x4, x5) = pJ_out_ggaga(x1, x2, x3, x4, x5)
pI_out_ggaggaa(x1, x2, x3, x4, x5, x6, x7) = pI_out_ggaggaa(x1, x2, x3, x4, x5, x6, x7)
pB_out_gaagagaa(x1, x2, x3, x4, x5, x6, x7, x8) = pB_out_gaagagaa(x1, x2, x3, x4, x5, x6, x7, x8)
MERGESORTA_IN_GA(x1, x2) = MERGESORTA_IN_GA(x1)
PB_IN_GAAGAGAA(x1, x2, x3, x4, x5, x6, x7, x8) = PB_IN_GAAGAGAA(x1, x4, x6)
U7_GAAGAGAA(x1, x2, x3, x4, x5, x6, x7, x8, x9) = U7_GAAGAGAA(x1, x4, x6, x9)
PI_IN_GGAGGAA(x1, x2, x3, x4, x5, x6, x7) = PI_IN_GGAGGAA(x1, x2, x4, x5)
U9_GGAGGAA(x1, x2, x3, x4, x5, x6, x7, x8) = U9_GGAGGAA(x1, x2, x4, x5, x8)
PJ_IN_GGAGA(x1, x2, x3, x4, x5) = PJ_IN_GGAGA(x1, x2, x4)

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

(40) PiDPToQDPProof (SOUND transformation)

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

(41) Obligation:

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

MERGESORTA_IN_GA(.(T22, .(T23, T24))) → PB_IN_GAAGAGAA(T24, T22, T23)
PB_IN_GAAGAGAA(T24, T22, T23) → U7_GAAGAGAA(T24, T22, T23, splitC_in_gaa(T24))
U7_GAAGAGAA(T24, T22, T23, splitC_out_gaa(T24, T26, T27)) → PI_IN_GGAGGAA(T22, T26, T23, T27)
PI_IN_GGAGGAA(T22, T26, T23, T27) → U9_GGAGGAA(T22, T26, T23, T27, mergesortA_in_ga(.(T22, T26)))
U9_GGAGGAA(T22, T26, T23, T27, mergesortA_out_ga(.(T22, T26), T61)) → PJ_IN_GGAGA(T23, T27, T61)
PJ_IN_GGAGA(T23, T27, T61) → MERGESORTA_IN_GA(.(T23, T27))
PI_IN_GGAGGAA(T22, T26, T23, T27) → MERGESORTA_IN_GA(.(T22, T26))

The TRS R consists of the following rules:

splitC_in_gaa([]) → splitC_out_gaa([], [], [])
splitC_in_gaa(.(T41, [])) → splitC_out_gaa(.(T41, []), .(T41, []), [])
splitC_in_gaa(.(T57, .(T58, T59))) → U2_gaa(T57, T58, T59, splitC_in_gaa(T59))
mergesortA_in_ga(.(T4, [])) → mergesortA_out_ga(.(T4, []), .(T4, []))
mergesortA_in_ga(.(T22, .(T23, T24))) → U1_ga(T22, T23, T24, pB_in_gaagagaa(T24, T22, T23))
U2_gaa(T57, T58, T59, splitC_out_gaa(T59, X161, X162)) → splitC_out_gaa(.(T57, .(T58, T59)), .(T57, X161), .(T58, X162))
U1_ga(T22, T23, T24, pB_out_gaagagaa(T24, X48, X49, T22, X22, T23, X23, T14)) → mergesortA_out_ga(.(T22, .(T23, T24)), T14)
pB_in_gaagagaa(T24, T22, T23) → U7_gaagagaa(T24, T22, T23, splitC_in_gaa(T24))
U7_gaagagaa(T24, T22, T23, splitC_out_gaa(T24, T26, T27)) → U8_gaagagaa(T24, T26, T27, T22, T23, pI_in_ggaggaa(T22, T26, T23, T27))
U8_gaagagaa(T24, T26, T27, T22, T23, pI_out_ggaggaa(T22, T26, X22, T23, T27, X23, T14)) → pB_out_gaagagaa(T24, T26, T27, T22, X22, T23, X23, T14)
pI_in_ggaggaa(T22, T26, T23, T27) → U9_ggaggaa(T22, T26, T23, T27, mergesortA_in_ga(.(T22, T26)))
U9_ggaggaa(T22, T26, T23, T27, mergesortA_out_ga(.(T22, T26), T61)) → U10_ggaggaa(T22, T26, T61, T23, T27, pJ_in_ggaga(T23, T27, T61))
U10_ggaggaa(T22, T26, T61, T23, T27, pJ_out_ggaga(T23, T27, X23, T61, T14)) → pI_out_ggaggaa(T22, T26, T61, T23, T27, X23, T14)
pJ_in_ggaga(T23, T27, T61) → U11_ggaga(T23, T27, T61, mergesortA_in_ga(.(T23, T27)))
U11_ggaga(T23, T27, T61, mergesortA_out_ga(.(T23, T27), T62)) → U12_ggaga(T23, T27, T62, T61, mergeD_in_gga(T61, T62))
U12_ggaga(T23, T27, T62, T61, mergeD_out_gga(T61, T62, T14)) → pJ_out_ggaga(T23, T27, T62, T61, T14)
mergeD_in_gga([], T69) → mergeD_out_gga([], T69, T69)
mergeD_in_gga(T74, []) → mergeD_out_gga(T74, [], T74)
mergeD_in_gga(.(T95, T96), .(T97, T98)) → U3_gga(T95, T96, T97, T98, pE_in_gggga(T95, T97, T96, T98))
mergeD_in_gga(.(T136, T137), .(T138, T139)) → U4_gga(T136, T137, T138, T139, pF_in_gggga(T136, T138, T137, T139))
U3_gga(T95, T96, T97, T98, pE_out_gggga(T95, T97, T96, T98, T100)) → mergeD_out_gga(.(T95, T96), .(T97, T98), .(T95, T100))
U4_gga(T136, T137, T138, T139, pF_out_gggga(T136, T138, T137, T139, T141)) → mergeD_out_gga(.(T136, T137), .(T138, T139), .(T138, T141))
pE_in_gggga(T95, T97, T96, T98) → U13_gggga(T95, T97, T96, T98, leG_in_gg(T95, T97))
pF_in_gggga(T136, T138, T137, T139) → U15_gggga(T136, T138, T137, T139, gtH_in_gg(T136, T138))
U13_gggga(T95, T97, T96, T98, leG_out_gg(T95, T97)) → U14_gggga(T95, T97, T96, T98, mergeD_in_gga(T96, .(T97, T98)))
U15_gggga(T136, T138, T137, T139, gtH_out_gg(T136, T138)) → U16_gggga(T136, T138, T137, T139, mergeD_in_gga(.(T136, T137), T139))
leG_in_gg(s(T113), s(T114)) → U5_gg(T113, T114, leG_in_gg(T113, T114))
leG_in_gg(0, s(T121)) → leG_out_gg(0, s(T121))
leG_in_gg(0, 0) → leG_out_gg(0, 0)
U14_gggga(T95, T97, T96, T98, mergeD_out_gga(T96, .(T97, T98), T100)) → pE_out_gggga(T95, T97, T96, T98, T100)
gtH_in_gg(s(T154), s(T155)) → U6_gg(T154, T155, gtH_in_gg(T154, T155))
gtH_in_gg(s(T160), 0) → gtH_out_gg(s(T160), 0)
U16_gggga(T136, T138, T137, T139, mergeD_out_gga(.(T136, T137), T139, T141)) → pF_out_gggga(T136, T138, T137, T139, T141)
U5_gg(T113, T114, leG_out_gg(T113, T114)) → leG_out_gg(s(T113), s(T114))
U6_gg(T154, T155, gtH_out_gg(T154, T155)) → gtH_out_gg(s(T154), s(T155))

The set Q consists of the following terms:

splitC_in_gaa(x0)
mergesortA_in_ga(x0)
U2_gaa(x0, x1, x2, x3)
U1_ga(x0, x1, x2, x3)
pB_in_gaagagaa(x0, x1, x2)
U7_gaagagaa(x0, x1, x2, x3)
U8_gaagagaa(x0, x1, x2, x3, x4, x5)
pI_in_ggaggaa(x0, x1, x2, x3)
U9_ggaggaa(x0, x1, x2, x3, x4)
U10_ggaggaa(x0, x1, x2, x3, x4, x5)
pJ_in_ggaga(x0, x1, x2)
U11_ggaga(x0, x1, x2, x3)
U12_ggaga(x0, x1, x2, x3, x4)
mergeD_in_gga(x0, x1)
U3_gga(x0, x1, x2, x3, x4)
U4_gga(x0, x1, x2, x3, x4)
pE_in_gggga(x0, x1, x2, x3)
pF_in_gggga(x0, x1, x2, x3)
U13_gggga(x0, x1, x2, x3, x4)
U15_gggga(x0, x1, x2, x3, x4)
leG_in_gg(x0, x1)
U14_gggga(x0, x1, x2, x3, x4)
gtH_in_gg(x0, x1)
U16_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(.(T22, .(T23, T24))) → PB_IN_GAAGAGAA(T24, T22, T23)
PB_IN_GAAGAGAA(T24, T22, T23) → U7_GAAGAGAA(T24, T22, T23, splitC_in_gaa(T24))

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

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

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

POL( U9_GGAGGAA(x₁, ..., x₅) ) = 2x₄

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

POL( [] ) = 0

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

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

POL( U2_gaa(x₁, ..., x₄) ) = 2x₄ + 2

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

POL( mergesortA_out_ga(x₁, x₂) ) = 2

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

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

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

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

POL( pI_out_ggaggaa(x₁, ..., x₇) ) = 2x₃ + 2x₆ + 2x₇ + 2

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

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

POL( U10_ggaggaa(x₁, ..., x₆) ) = x₁ + x₂ + x₃ + x₅ + 2x₆ + 2

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

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

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

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

POL( mergeD_in_gga(x₁, x₂) ) = 2

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

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

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

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

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

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

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

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

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

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

POL( 0 ) = 2

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

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

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

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

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

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

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

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

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

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

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

POL( PJ_IN_GGAGA(x₁, ..., x₃) ) = 2x₂

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

splitC_in_gaa([]) → splitC_out_gaa([], [], [])
splitC_in_gaa(.(T41, [])) → splitC_out_gaa(.(T41, []), .(T41, []), [])
splitC_in_gaa(.(T57, .(T58, T59))) → U2_gaa(T57, T58, T59, splitC_in_gaa(T59))
U2_gaa(T57, T58, T59, splitC_out_gaa(T59, X161, X162)) → splitC_out_gaa(.(T57, .(T58, T59)), .(T57, X161), .(T58, X162))

(43) Obligation:

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

U7_GAAGAGAA(T24, T22, T23, splitC_out_gaa(T24, T26, T27)) → PI_IN_GGAGGAA(T22, T26, T23, T27)
PI_IN_GGAGGAA(T22, T26, T23, T27) → U9_GGAGGAA(T22, T26, T23, T27, mergesortA_in_ga(.(T22, T26)))
U9_GGAGGAA(T22, T26, T23, T27, mergesortA_out_ga(.(T22, T26), T61)) → PJ_IN_GGAGA(T23, T27, T61)
PJ_IN_GGAGA(T23, T27, T61) → MERGESORTA_IN_GA(.(T23, T27))
PI_IN_GGAGGAA(T22, T26, T23, T27) → MERGESORTA_IN_GA(.(T22, T26))

The TRS R consists of the following rules:

splitC_in_gaa([]) → splitC_out_gaa([], [], [])
splitC_in_gaa(.(T41, [])) → splitC_out_gaa(.(T41, []), .(T41, []), [])
splitC_in_gaa(.(T57, .(T58, T59))) → U2_gaa(T57, T58, T59, splitC_in_gaa(T59))
mergesortA_in_ga(.(T4, [])) → mergesortA_out_ga(.(T4, []), .(T4, []))
mergesortA_in_ga(.(T22, .(T23, T24))) → U1_ga(T22, T23, T24, pB_in_gaagagaa(T24, T22, T23))
U2_gaa(T57, T58, T59, splitC_out_gaa(T59, X161, X162)) → splitC_out_gaa(.(T57, .(T58, T59)), .(T57, X161), .(T58, X162))
U1_ga(T22, T23, T24, pB_out_gaagagaa(T24, X48, X49, T22, X22, T23, X23, T14)) → mergesortA_out_ga(.(T22, .(T23, T24)), T14)
pB_in_gaagagaa(T24, T22, T23) → U7_gaagagaa(T24, T22, T23, splitC_in_gaa(T24))
U7_gaagagaa(T24, T22, T23, splitC_out_gaa(T24, T26, T27)) → U8_gaagagaa(T24, T26, T27, T22, T23, pI_in_ggaggaa(T22, T26, T23, T27))
U8_gaagagaa(T24, T26, T27, T22, T23, pI_out_ggaggaa(T22, T26, X22, T23, T27, X23, T14)) → pB_out_gaagagaa(T24, T26, T27, T22, X22, T23, X23, T14)
pI_in_ggaggaa(T22, T26, T23, T27) → U9_ggaggaa(T22, T26, T23, T27, mergesortA_in_ga(.(T22, T26)))
U9_ggaggaa(T22, T26, T23, T27, mergesortA_out_ga(.(T22, T26), T61)) → U10_ggaggaa(T22, T26, T61, T23, T27, pJ_in_ggaga(T23, T27, T61))
U10_ggaggaa(T22, T26, T61, T23, T27, pJ_out_ggaga(T23, T27, X23, T61, T14)) → pI_out_ggaggaa(T22, T26, T61, T23, T27, X23, T14)
pJ_in_ggaga(T23, T27, T61) → U11_ggaga(T23, T27, T61, mergesortA_in_ga(.(T23, T27)))
U11_ggaga(T23, T27, T61, mergesortA_out_ga(.(T23, T27), T62)) → U12_ggaga(T23, T27, T62, T61, mergeD_in_gga(T61, T62))
U12_ggaga(T23, T27, T62, T61, mergeD_out_gga(T61, T62, T14)) → pJ_out_ggaga(T23, T27, T62, T61, T14)
mergeD_in_gga([], T69) → mergeD_out_gga([], T69, T69)
mergeD_in_gga(T74, []) → mergeD_out_gga(T74, [], T74)
mergeD_in_gga(.(T95, T96), .(T97, T98)) → U3_gga(T95, T96, T97, T98, pE_in_gggga(T95, T97, T96, T98))
mergeD_in_gga(.(T136, T137), .(T138, T139)) → U4_gga(T136, T137, T138, T139, pF_in_gggga(T136, T138, T137, T139))
U3_gga(T95, T96, T97, T98, pE_out_gggga(T95, T97, T96, T98, T100)) → mergeD_out_gga(.(T95, T96), .(T97, T98), .(T95, T100))
U4_gga(T136, T137, T138, T139, pF_out_gggga(T136, T138, T137, T139, T141)) → mergeD_out_gga(.(T136, T137), .(T138, T139), .(T138, T141))
pE_in_gggga(T95, T97, T96, T98) → U13_gggga(T95, T97, T96, T98, leG_in_gg(T95, T97))
pF_in_gggga(T136, T138, T137, T139) → U15_gggga(T136, T138, T137, T139, gtH_in_gg(T136, T138))
U13_gggga(T95, T97, T96, T98, leG_out_gg(T95, T97)) → U14_gggga(T95, T97, T96, T98, mergeD_in_gga(T96, .(T97, T98)))
U15_gggga(T136, T138, T137, T139, gtH_out_gg(T136, T138)) → U16_gggga(T136, T138, T137, T139, mergeD_in_gga(.(T136, T137), T139))
leG_in_gg(s(T113), s(T114)) → U5_gg(T113, T114, leG_in_gg(T113, T114))
leG_in_gg(0, s(T121)) → leG_out_gg(0, s(T121))
leG_in_gg(0, 0) → leG_out_gg(0, 0)
U14_gggga(T95, T97, T96, T98, mergeD_out_gga(T96, .(T97, T98), T100)) → pE_out_gggga(T95, T97, T96, T98, T100)
gtH_in_gg(s(T154), s(T155)) → U6_gg(T154, T155, gtH_in_gg(T154, T155))
gtH_in_gg(s(T160), 0) → gtH_out_gg(s(T160), 0)
U16_gggga(T136, T138, T137, T139, mergeD_out_gga(.(T136, T137), T139, T141)) → pF_out_gggga(T136, T138, T137, T139, T141)
U5_gg(T113, T114, leG_out_gg(T113, T114)) → leG_out_gg(s(T113), s(T114))
U6_gg(T154, T155, gtH_out_gg(T154, T155)) → gtH_out_gg(s(T154), s(T155))

The set Q consists of the following terms:

splitC_in_gaa(x0)
mergesortA_in_ga(x0)
U2_gaa(x0, x1, x2, x3)
U1_ga(x0, x1, x2, x3)
pB_in_gaagagaa(x0, x1, x2)
U7_gaagagaa(x0, x1, x2, x3)
U8_gaagagaa(x0, x1, x2, x3, x4, x5)
pI_in_ggaggaa(x0, x1, x2, x3)
U9_ggaggaa(x0, x1, x2, x3, x4)
U10_ggaggaa(x0, x1, x2, x3, x4, x5)
pJ_in_ggaga(x0, x1, x2)
U11_ggaga(x0, x1, x2, x3)
U12_ggaga(x0, x1, x2, x3, x4)
mergeD_in_gga(x0, x1)
U3_gga(x0, x1, x2, x3, x4)
U4_gga(x0, x1, x2, x3, x4)
pE_in_gggga(x0, x1, x2, x3)
pF_in_gggga(x0, x1, x2, x3)
U13_gggga(x0, x1, x2, x3, x4)
U15_gggga(x0, x1, x2, x3, x4)
leG_in_gg(x0, x1)
U14_gggga(x0, x1, x2, x3, x4)
gtH_in_gg(x0, x1)
U16_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 5 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 (EQUIVALENT 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 (SOUND transformation)

(25) Obligation:

(26) MRRProof (EQUIVALENT transformation)

(27) Obligation:

(28) DependencyGraphProof (EQUIVALENT transformation)

(29) TRUE

(30) Obligation:

(31) UsableRulesProof (EQUIVALENT transformation)

(32) Obligation:

(33) PiDPToQDPProof (SOUND transformation)

(34) Obligation:

(35) QDPSizeChangeProof (EQUIVALENT transformation)

(36) YES

(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