Left Termination proof of /tmp/tmppaQGqh/slowsort-bb.pl

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

0 Prolog

↳1 PrologToPiTRSViaGraphTransformerProof (⇒, 237 ms)

↳2 PiTRS

↳3 DependencyPairsProof (⇔, 356 ms)

↳4 PiDP

↳5 DependencyGraphProof (⇔, 41 ms)

↳6 AND

    ↳7 PiDP

        ↳8 UsableRulesProof (⇔, 0 ms)

        ↳9 PiDP

        ↳10 PiDPToQDPProof (⇔, 24 ms)

        ↳11 QDP

        ↳12 QDPSizeChangeProof (⇔, 0 ms)

        ↳13 YES

    ↳14 PiDP

        ↳15 UsableRulesProof (⇔, 0 ms)

        ↳16 PiDP

        ↳17 PiDPToQDPProof (⇔, 0 ms)

        ↳18 QDP

        ↳19 QDPSizeChangeProof (⇔, 0 ms)

        ↳20 YES

    ↳21 PiDP

        ↳22 UsableRulesProof (⇔, 0 ms)

        ↳23 PiDP

        ↳24 PiDPToQDPProof (⇒, 0 ms)

        ↳25 QDP

        ↳26 QDPSizeChangeProof (⇔, 0 ms)

        ↳27 YES

    ↳28 PiDP

        ↳29 UsableRulesProof (⇔, 0 ms)

        ↳30 PiDP

        ↳31 PiDPToQDPProof (⇒, 0 ms)

        ↳32 QDP

        ↳33 QDPSizeChangeProof (⇔, 0 ms)

        ↳34 YES

    ↳35 PiDP

        ↳36 UsableRulesProof (⇔, 0 ms)

        ↳37 PiDP

        ↳38 PiDPToQDPProof (⇒, 0 ms)

        ↳39 QDP

        ↳40 QDPSizeChangeProof (⇔, 0 ms)

        ↳41 YES

(0) Obligation:

Clauses:

ss(Xs, Ys) :- ','(perm(Xs, Ys), ordered(Ys)).
perm([], []).
perm(Xs, .(X, Ys)) :- ','(app(X1s, .(X, X2s), Xs), ','(app(X1s, X2s, Zs), perm(Zs, Ys))).
app([], X, X).
app(.(X, Xs), Ys, .(X, Zs)) :- app(Xs, Ys, Zs).
ordered([]).
ordered(.(X1, [])).
ordered(.(X, .(Y, Xs))) :- ','(less(X, s(Y)), ordered(.(Y, Xs))).
less(0, s(X2)).
less(s(X), s(Y)) :- less(X, Y).

Query: ss(g,g)

(1) PrologToPiTRSViaGraphTransformerProof (SOUND transformation)

Transformed Prolog program to (Pi-)TRS.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
2 [label="A: ss(T1, T2)\n\nT1 is ground\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
5 [label="5: ss(T1, T2), SCOPE: 1, CLAUSE: 0\n\nT1 is ground\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
7 [label="7: ','(perm(T5, T6), ordered(T6))\n\nT5 is ground\nT6 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
10 [label="10: ','(perm(T5, T6), ordered(T6)), SCOPE: 2, CLAUSE: 1 | ','(perm(T5, T6), ordered(T6)), SCOPE: 2, CLAUSE: 2\n\nT5 is ground\nT6 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
12 [label="12: ','(perm(T5, T6), ordered(T6)), SCOPE: 2, CLAUSE: 1\n\nT5 is ground\nT6 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
14 [label="14: ','(perm(T5, T6), ordered(T6)), SCOPE: 2, CLAUSE: 2\n\nT5 is ground\nT6 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
16 [label="16: ordered([])\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
19 [label="19: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
20 [label="20: ordered([]), SCOPE: 3, CLAUSE: 5 | ordered([]), SCOPE: 3, CLAUSE: 6 | ordered([]), SCOPE: 3, CLAUSE: 7\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
22 [label="22: ordered([]), SCOPE: 3, CLAUSE: 5\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
24 [label="24: ordered([]), SCOPE: 3, CLAUSE: 6 | ordered([]), SCOPE: 3, CLAUSE: 7\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
26 [label="26: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
27 [label="27: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
32 [label="32: ordered([]), SCOPE: 3, CLAUSE: 7\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
34 [label="34: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
42 [label="B: ','(','(app(X23, .(T14, X24), T13), ','(app(X23, X24, X25), perm(X25, T15))), ordered(.(T14, T15)))\n\nT13 is ground\nT14 is ground\nT15 is ground\nX23 is free\nX24 is free\nX25 is free", fontsize=16, style=filled, fillcolor=lightyellow];
43 [label="43: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
48 [label="C: app(X23, .(T14, X24), T13)\n\nT13 is ground\nT14 is ground\nX23 is free\nX24 is free", fontsize=16, style=filled, fillcolor=lightyellow];
49 [label="K: ','(','(app(T20, T21, X25), perm(X25, T15)), ordered(.(T14, T15)))\n\nT14 is ground\nT15 is ground\nT20 is ground\nT21 is ground\nX25 is free", fontsize=16, style=filled, fillcolor=lightyellow];
52 [label="52: app(X23, .(T14, X24), T13), SCOPE: 4, CLAUSE: 3 | app(X23, .(T14, X24), T13), SCOPE: 4, CLAUSE: 4\n\nT13 is ground\nT14 is ground\nX23 is free\nX24 is free", fontsize=16, style=filled, fillcolor=lightyellow];
54 [label="54: app(X23, .(T14, X24), T13), SCOPE: 4, CLAUSE: 3\n\nT13 is ground\nT14 is ground\nX23 is free\nX24 is free", fontsize=16, style=filled, fillcolor=lightyellow];
55 [label="55: app(X23, .(T14, X24), T13), SCOPE: 4, CLAUSE: 4\n\nT13 is ground\nT14 is ground\nX23 is free\nX24 is free", fontsize=16, style=filled, fillcolor=lightyellow];
60 [label="60: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
62 [label="62: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
63 [label="63: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
72 [label="72: app(X63, .(T42, X64), T44)\n\nT42 is ground\nT44 is ground\nX63 is free\nX64 is free", fontsize=16, style=filled, fillcolor=lightyellow];
74 [label="74: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
79 [label="D: app(T20, T21, X25)\n\nT20 is ground\nT21 is ground\nX25 is free", fontsize=16, style=filled, fillcolor=lightyellow];
80 [label="L: ','(perm(T51, T15), ordered(.(T14, T15)))\n\nT14 is ground\nT15 is ground\nT51 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
83 [label="83: app(T20, T21, X25), SCOPE: 5, CLAUSE: 3 | app(T20, T21, X25), SCOPE: 5, CLAUSE: 4\n\nT20 is ground\nT21 is ground\nX25 is free", fontsize=16, style=filled, fillcolor=lightyellow];
84 [label="84: app(T20, T21, X25), SCOPE: 5, CLAUSE: 3\n\nT20 is ground\nT21 is ground\nX25 is free", fontsize=16, style=filled, fillcolor=lightyellow];
85 [label="85: app(T20, T21, X25), SCOPE: 5, CLAUSE: 4\n\nT20 is ground\nT21 is ground\nX25 is free", fontsize=16, style=filled, fillcolor=lightyellow];
86 [label="86: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
88 [label="88: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
90 [label="90: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
99 [label="99: app(T66, T67, X92)\n\nT66 is ground\nT67 is ground\nX92 is free", fontsize=16, style=filled, fillcolor=lightyellow];
102 [label="102: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
104 [label="E: perm(T51, T15)\n\nT15 is ground\nT51 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
106 [label="G: ordered(.(T14, T15))\n\nT14 is ground\nT15 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
108 [label="108: perm(T51, T15), SCOPE: 6, CLAUSE: 1 | perm(T51, T15), SCOPE: 6, CLAUSE: 2\n\nT15 is ground\nT51 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
109 [label="109: perm(T51, T15), SCOPE: 6, CLAUSE: 1\n\nT15 is ground\nT51 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
110 [label="110: perm(T51, T15), SCOPE: 6, CLAUSE: 2\n\nT15 is ground\nT51 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
111 [label="111: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
112 [label="112: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
113 [label="113: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
139 [label="F: ','(app(X107, .(T77, X108), T76), ','(app(X107, X108, X109), perm(X109, T78)))\n\nT76 is ground\nT77 is ground\nT78 is ground\nX107 is free\nX108 is free\nX109 is free", fontsize=16, style=filled, fillcolor=lightyellow];
140 [label="140: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
143 [label="143: app(X107, .(T77, X108), T76)\n\nT76 is ground\nT77 is ground\nX107 is free\nX108 is free", fontsize=16, style=filled, fillcolor=lightyellow];
144 [label="M: ','(app(T83, T84, X109), perm(X109, T78))\n\nT78 is ground\nT83 is ground\nT84 is ground\nX109 is free", fontsize=16, style=filled, fillcolor=lightyellow];
171 [label="171: app(T83, T84, X109)\n\nT83 is ground\nT84 is ground\nX109 is free", fontsize=16, style=filled, fillcolor=lightyellow];
172 [label="172: perm(T91, T78)\n\nT78 is ground\nT91 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
178 [label="178: ordered(.(T14, T15)), SCOPE: 7, CLAUSE: 5 | ordered(.(T14, T15)), SCOPE: 7, CLAUSE: 6 | ordered(.(T14, T15)), SCOPE: 7, CLAUSE: 7\n\nT14 is ground\nT15 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
179 [label="179: ordered(.(T14, T15)), SCOPE: 7, CLAUSE: 6 | ordered(.(T14, T15)), SCOPE: 7, CLAUSE: 7\n\nT14 is ground\nT15 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
180 [label="180: ordered(.(T14, T15)), SCOPE: 7, CLAUSE: 6\n\nT14 is ground\nT15 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
181 [label="181: ordered(.(T14, T15)), SCOPE: 7, CLAUSE: 7\n\nT14 is ground\nT15 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
185 [label="185: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
186 [label="186: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
187 [label="187: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
191 [label="H: ','(less(T105, s(T106)), ordered(.(T106, T107)))\n\nT105 is ground\nT106 is ground\nT107 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
192 [label="192: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
195 [label="J: less(T105, s(T106))\n\nT105 is ground\nT106 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
196 [label="196: ordered(.(T106, T107))\n\nT106 is ground\nT107 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
205 [label="205: less(T105, s(T106)), SCOPE: 8, CLAUSE: 8 | less(T105, s(T106)), SCOPE: 8, CLAUSE: 9\n\nT105 is ground\nT106 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
206 [label="206: less(T105, s(T106)), SCOPE: 8, CLAUSE: 8\n\nT105 is ground\nT106 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
207 [label="207: less(T105, s(T106)), SCOPE: 8, CLAUSE: 9\n\nT105 is ground\nT106 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
208 [label="208: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
209 [label="209: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
210 [label="210: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
211 [label="I: less(T121, T122)\n\nT121 is ground\nT122 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
212 [label="212: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
213 [label="213: less(T121, T122), SCOPE: 9, CLAUSE: 8 | less(T121, T122), SCOPE: 9, CLAUSE: 9\n\nT121 is ground\nT122 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
214 [label="214: less(T121, T122), SCOPE: 9, CLAUSE: 8\n\nT121 is ground\nT122 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
215 [label="215: less(T121, T122), SCOPE: 9, CLAUSE: 9\n\nT121 is ground\nT122 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
216 [label="216: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
217 [label="217: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
218 [label="218: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
219 [label="219: less(T134, T135)\n\nT134 is ground\nT135 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
220 [label="220: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
221 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
2 -> 221 [arrowhead = none ];
221 -> 5;

222 [label="ONLY EVAL with clause\nss(X5, X6) :- ','(perm(X5, X6), ordered(X6)).\nand substitutionT1 -> T5,\nX5 -> T5,\nT2 -> T6,\nX6 -> T6", fontsize=14, style = filled, fillcolor = lightblue];
5 -> 222 [arrowhead = none ];
222 -> 7;

223 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
7 -> 223 [arrowhead = none ];
223 -> 10;

224 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
10 -> 224 [arrowhead = none ];
224 -> 12;

225 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
10 -> 225 [arrowhead = none ];
225 -> 14;

226 [label="EVAL with clause\nperm([], []).\nand substitutionT5 -> [],\nT6 -> []", fontsize=14, style = filled, fillcolor = lightblue];
12 -> 226 [arrowhead = none ];
226 -> 16;

227 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
12 -> 227 [arrowhead = none ];
227 -> 19;

228 [label="EVAL with clause\nperm(X20, .(X21, X22)) :- ','(app(X23, .(X21, X24), X20), ','(app(X23, X24, X25), perm(X25, X22))).\nand substitutionT5 -> T13,\nX20 -> T13,\nX21 -> T14,\nX22 -> T15,\nT6 -> .(T14, T15)", fontsize=14, style = filled, fillcolor = lightblue];
14 -> 228 [arrowhead = none ];
228 -> 42;

229 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
14 -> 229 [arrowhead = none ];
229 -> 43;

230 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
16 -> 230 [arrowhead = none ];
230 -> 20;

231 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
20 -> 231 [arrowhead = none ];
231 -> 22;

232 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
20 -> 232 [arrowhead = none ];
232 -> 24;

233 [label="ONLY EVAL with clause\nordered([]).\nand substitution", fontsize=14, style = filled, fillcolor = lightblue];
22 -> 233 [arrowhead = none ];
233 -> 26;

234 [label="BACKTRACK\nfor clause: ordered(.(X1, []))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
24 -> 234 [arrowhead = none ];
234 -> 32;

235 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
26 -> 235 [arrowhead = none ];
235 -> 27;

236 [label="BACKTRACK\nfor clause: ordered(.(X, .(Y, Xs))) :- ','(less(X, s(Y)), ordered(.(Y, Xs)))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
32 -> 236 [arrowhead = none ];
236 -> 34;

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

238 [label="SPLIT 2\nnew knowledge:\nT20 is ground\nT14 is ground\nT21 is ground\nT13 is ground\nreplacements:X23 -> T20,\nX24 -> T21", fontsize=14, style = filled, fillcolor = violet];
42 -> 238 [arrowhead = none ];
238 -> 49;

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

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

241 [label="SPLIT 2\nnew knowledge:\nT20 is ground\nT21 is ground\nT51 is ground\nreplacements:X25 -> T51", fontsize=14, style = filled, fillcolor = violet];
49 -> 241 [arrowhead = none ];
241 -> 80;

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

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

244 [label="EVAL with clause\napp([], X42, X42).\nand substitutionX23 -> [],\nT14 -> T34,\nX24 -> T35,\nX42 -> .(T34, T35),\nX43 -> T35,\nT13 -> .(T34, T35)", fontsize=14, style = filled, fillcolor = lightblue];
54 -> 244 [arrowhead = none ];
244 -> 60;

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

246 [label="EVAL with clause\napp(.(X58, X59), X60, .(X58, X61)) :- app(X59, X60, X61).\nand substitutionX58 -> T43,\nX59 -> X63,\nX23 -> .(T43, X63),\nT14 -> T42,\nX24 -> X64,\nX60 -> .(T42, X64),\nX62 -> T43,\nX61 -> T44,\nT13 -> .(T43, T44)", fontsize=14, style = filled, fillcolor = lightblue];
55 -> 246 [arrowhead = none ];
246 -> 72;

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

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

249 [label="INSTANCE with matching:\nX23 -> X63\nT14 -> T42\nX24 -> X64\nT13 -> T44", fontsize=14, style = filled, fillcolor = lightgrey];
72 -> 249 [arrowhead = none , style=dashed];
249 -> 48[style=dashed];

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

251 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
80 -> 251 [arrowhead = none ];
251 -> 104;

252 [label="SPLIT 2\nnew knowledge:\nT51 is ground\nT15 is ground", fontsize=14, style = filled, fillcolor = violet];
80 -> 252 [arrowhead = none ];
252 -> 106;

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

254 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
83 -> 254 [arrowhead = none ];
254 -> 85;

255 [label="EVAL with clause\napp([], X77, X77).\nand substitutionT20 -> [],\nT21 -> T58,\nX77 -> T58,\nX25 -> T58", fontsize=14, style = filled, fillcolor = lightblue];
84 -> 255 [arrowhead = none ];
255 -> 86;

256 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
84 -> 256 [arrowhead = none ];
256 -> 88;

257 [label="EVAL with clause\napp(.(X88, X89), X90, .(X88, X91)) :- app(X89, X90, X91).\nand substitutionX88 -> T65,\nX89 -> T66,\nT20 -> .(T65, T66),\nT21 -> T67,\nX90 -> T67,\nX91 -> X92,\nX25 -> .(T65, X92)", fontsize=14, style = filled, fillcolor = lightblue];
85 -> 257 [arrowhead = none ];
257 -> 99;

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

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

260 [label="INSTANCE with matching:\nT20 -> T66\nT21 -> T67\nX25 -> X92", fontsize=14, style = filled, fillcolor = lightgrey];
99 -> 260 [arrowhead = none , style=dashed];
260 -> 79[style=dashed];

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

262 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
106 -> 262 [arrowhead = none ];
262 -> 178;

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

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

265 [label="EVAL with clause\nperm([], []).\nand substitutionT51 -> [],\nT15 -> []", fontsize=14, style = filled, fillcolor = lightblue];
109 -> 265 [arrowhead = none ];
265 -> 111;

266 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
109 -> 266 [arrowhead = none ];
266 -> 112;

267 [label="EVAL with clause\nperm(X104, .(X105, X106)) :- ','(app(X107, .(X105, X108), X104), ','(app(X107, X108, X109), perm(X109, X106))).\nand substitutionT51 -> T76,\nX104 -> T76,\nX105 -> T77,\nX106 -> T78,\nT15 -> .(T77, T78)", fontsize=14, style = filled, fillcolor = lightblue];
110 -> 267 [arrowhead = none ];
267 -> 139;

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

269 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
111 -> 269 [arrowhead = none ];
269 -> 113;

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

271 [label="SPLIT 2\nnew knowledge:\nT83 is ground\nT77 is ground\nT84 is ground\nT76 is ground\nreplacements:X107 -> T83,\nX108 -> T84", fontsize=14, style = filled, fillcolor = violet];
139 -> 271 [arrowhead = none ];
271 -> 144;

272 [label="INSTANCE with matching:\nX23 -> X107\nT14 -> T77\nX24 -> X108\nT13 -> T76", fontsize=14, style = filled, fillcolor = lightgrey];
143 -> 272 [arrowhead = none , style=dashed];
272 -> 48[style=dashed];

273 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
144 -> 273 [arrowhead = none ];
273 -> 171;

274 [label="SPLIT 2\nnew knowledge:\nT83 is ground\nT84 is ground\nT91 is ground\nreplacements:X109 -> T91", fontsize=14, style = filled, fillcolor = violet];
144 -> 274 [arrowhead = none ];
274 -> 172;

275 [label="INSTANCE with matching:\nT20 -> T83\nT21 -> T84\nX25 -> X109", fontsize=14, style = filled, fillcolor = lightgrey];
171 -> 275 [arrowhead = none , style=dashed];
275 -> 79[style=dashed];

276 [label="INSTANCE with matching:\nT51 -> T91\nT15 -> T78", fontsize=14, style = filled, fillcolor = lightgrey];
172 -> 276 [arrowhead = none , style=dashed];
276 -> 104[style=dashed];

277 [label="BACKTRACK\nfor clause: ordered([])because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
178 -> 277 [arrowhead = none ];
277 -> 179;

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

279 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
179 -> 279 [arrowhead = none ];
279 -> 181;

280 [label="EVAL with clause\nordered(.(X126, [])).\nand substitutionT14 -> T98,\nX126 -> T98,\nT15 -> []", fontsize=14, style = filled, fillcolor = lightblue];
180 -> 280 [arrowhead = none ];
280 -> 185;

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

282 [label="EVAL with clause\nordered(.(X133, .(X134, X135))) :- ','(less(X133, s(X134)), ordered(.(X134, X135))).\nand substitutionT14 -> T105,\nX133 -> T105,\nX134 -> T106,\nX135 -> T107,\nT15 -> .(T106, T107)", fontsize=14, style = filled, fillcolor = lightblue];
181 -> 282 [arrowhead = none ];
282 -> 191;

283 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
181 -> 283 [arrowhead = none ];
283 -> 192;

284 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
185 -> 284 [arrowhead = none ];
284 -> 187;

285 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
191 -> 285 [arrowhead = none ];
285 -> 195;

286 [label="SPLIT 2\nnew knowledge:\nT105 is ground\nT106 is ground", fontsize=14, style = filled, fillcolor = violet];
191 -> 286 [arrowhead = none ];
286 -> 196;

287 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
195 -> 287 [arrowhead = none ];
287 -> 205;

288 [label="INSTANCE with matching:\nT14 -> T106\nT15 -> T107", fontsize=14, style = filled, fillcolor = lightgrey];
196 -> 288 [arrowhead = none , style=dashed];
288 -> 106[style=dashed];

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

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

291 [label="EVAL with clause\nless(0, s(X144)).\nand substitutionT105 -> 0,\nT106 -> T116,\nX144 -> T116", fontsize=14, style = filled, fillcolor = lightblue];
206 -> 291 [arrowhead = none ];
291 -> 208;

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

293 [label="EVAL with clause\nless(s(X149), s(X150)) :- less(X149, X150).\nand substitutionX149 -> T121,\nT105 -> s(T121),\nT106 -> T122,\nX150 -> T122", fontsize=14, style = filled, fillcolor = lightblue];
207 -> 293 [arrowhead = none ];
293 -> 211;

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

295 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
208 -> 295 [arrowhead = none ];
295 -> 210;

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

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

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

299 [label="EVAL with clause\nless(0, s(X157)).\nand substitutionT121 -> 0,\nX157 -> T129,\nT122 -> s(T129)", fontsize=14, style = filled, fillcolor = lightblue];
214 -> 299 [arrowhead = none ];
299 -> 216;

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

301 [label="EVAL with clause\nless(s(X162), s(X163)) :- less(X162, X163).\nand substitutionX162 -> T134,\nT121 -> s(T134),\nX163 -> T135,\nT122 -> s(T135)", fontsize=14, style = filled, fillcolor = lightblue];
215 -> 301 [arrowhead = none ];
301 -> 219;

302 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
215 -> 302 [arrowhead = none ];
302 -> 220;

303 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
216 -> 303 [arrowhead = none ];
303 -> 218;

304 [label="INSTANCE with matching:\nT121 -> T134\nT122 -> T135", fontsize=14, style = filled, fillcolor = lightgrey];
219 -> 304 [arrowhead = none , style=dashed];
304 -> 211[style=dashed];

}

(2) Obligation:

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

ssA_in_gg([], []) → ssA_out_gg([], [])
ssA_in_gg(T13, .(T14, T15)) → U1_gg(T13, T14, T15, pB_in_agagag(X23, T14, X24, T13, X25, T15))
pB_in_agagag(T20, T14, T21, T13, X25, T15) → U8_agagag(T20, T14, T21, T13, X25, T15, appC_in_agag(T20, T14, T21, T13))
appC_in_agag([], T34, T35, .(T34, T35)) → appC_out_agag([], T34, T35, .(T34, T35))
appC_in_agag(.(T43, X63), T42, X64, .(T43, T44)) → U2_agag(T43, X63, T42, X64, T44, appC_in_agag(X63, T42, X64, T44))
U2_agag(T43, X63, T42, X64, T44, appC_out_agag(X63, T42, X64, T44)) → appC_out_agag(.(T43, X63), T42, X64, .(T43, T44))
U8_agagag(T20, T14, T21, T13, X25, T15, appC_out_agag(T20, T14, T21, T13)) → U9_agagag(T20, T14, T21, T13, X25, T15, pK_in_ggagg(T20, T21, X25, T15, T14))
pK_in_ggagg(T20, T21, T51, T15, T14) → U10_ggagg(T20, T21, T51, T15, T14, appD_in_gga(T20, T21, T51))
appD_in_gga([], T58, T58) → appD_out_gga([], T58, T58)
appD_in_gga(.(T65, T66), T67, .(T65, X92)) → U3_gga(T65, T66, T67, X92, appD_in_gga(T66, T67, X92))
U3_gga(T65, T66, T67, X92, appD_out_gga(T66, T67, X92)) → appD_out_gga(.(T65, T66), T67, .(T65, X92))
U10_ggagg(T20, T21, T51, T15, T14, appD_out_gga(T20, T21, T51)) → U11_ggagg(T20, T21, T51, T15, T14, pL_in_ggg(T51, T15, T14))
pL_in_ggg(T51, T15, T14) → U12_ggg(T51, T15, T14, permE_in_gg(T51, T15))
permE_in_gg([], []) → permE_out_gg([], [])
permE_in_gg(T76, .(T77, T78)) → U4_gg(T76, T77, T78, pF_in_agagag(X107, T77, X108, T76, X109, T78))
pF_in_agagag(T83, T77, T84, T76, X109, T78) → U14_agagag(T83, T77, T84, T76, X109, T78, appC_in_agag(T83, T77, T84, T76))
U14_agagag(T83, T77, T84, T76, X109, T78, appC_out_agag(T83, T77, T84, T76)) → U15_agagag(T83, T77, T84, T76, X109, T78, pM_in_ggag(T83, T84, X109, T78))
pM_in_ggag(T83, T84, T91, T78) → U16_ggag(T83, T84, T91, T78, appD_in_gga(T83, T84, T91))
U16_ggag(T83, T84, T91, T78, appD_out_gga(T83, T84, T91)) → U17_ggag(T83, T84, T91, T78, permE_in_gg(T91, T78))
U17_ggag(T83, T84, T91, T78, permE_out_gg(T91, T78)) → pM_out_ggag(T83, T84, T91, T78)
U15_agagag(T83, T77, T84, T76, X109, T78, pM_out_ggag(T83, T84, X109, T78)) → pF_out_agagag(T83, T77, T84, T76, X109, T78)
U4_gg(T76, T77, T78, pF_out_agagag(X107, T77, X108, T76, X109, T78)) → permE_out_gg(T76, .(T77, T78))
U12_ggg(T51, T15, T14, permE_out_gg(T51, T15)) → U13_ggg(T51, T15, T14, orderedG_in_gg(T14, T15))
orderedG_in_gg(T98, []) → orderedG_out_gg(T98, [])
orderedG_in_gg(T105, .(T106, T107)) → U5_gg(T105, T106, T107, pH_in_ggg(T105, T106, T107))
pH_in_ggg(T105, T106, T107) → U18_ggg(T105, T106, T107, lessJ_in_gg(T105, T106))
lessJ_in_gg(0, T116) → lessJ_out_gg(0, T116)
lessJ_in_gg(s(T121), T122) → U7_gg(T121, T122, lessI_in_gg(T121, T122))
lessI_in_gg(0, s(T129)) → lessI_out_gg(0, s(T129))
lessI_in_gg(s(T134), s(T135)) → U6_gg(T134, T135, lessI_in_gg(T134, T135))
U6_gg(T134, T135, lessI_out_gg(T134, T135)) → lessI_out_gg(s(T134), s(T135))
U7_gg(T121, T122, lessI_out_gg(T121, T122)) → lessJ_out_gg(s(T121), T122)
U18_ggg(T105, T106, T107, lessJ_out_gg(T105, T106)) → U19_ggg(T105, T106, T107, orderedG_in_gg(T106, T107))
U19_ggg(T105, T106, T107, orderedG_out_gg(T106, T107)) → pH_out_ggg(T105, T106, T107)
U5_gg(T105, T106, T107, pH_out_ggg(T105, T106, T107)) → orderedG_out_gg(T105, .(T106, T107))
U13_ggg(T51, T15, T14, orderedG_out_gg(T14, T15)) → pL_out_ggg(T51, T15, T14)
U11_ggagg(T20, T21, T51, T15, T14, pL_out_ggg(T51, T15, T14)) → pK_out_ggagg(T20, T21, T51, T15, T14)
U9_agagag(T20, T14, T21, T13, X25, T15, pK_out_ggagg(T20, T21, X25, T15, T14)) → pB_out_agagag(T20, T14, T21, T13, X25, T15)
U1_gg(T13, T14, T15, pB_out_agagag(X23, T14, X24, T13, X25, T15)) → ssA_out_gg(T13, .(T14, T15))

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

SSA_IN_GG(T13, .(T14, T15)) → U1_GG(T13, T14, T15, pB_in_agagag(X23, T14, X24, T13, X25, T15))
SSA_IN_GG(T13, .(T14, T15)) → PB_IN_AGAGAG(X23, T14, X24, T13, X25, T15)
PB_IN_AGAGAG(T20, T14, T21, T13, X25, T15) → U8_AGAGAG(T20, T14, T21, T13, X25, T15, appC_in_agag(T20, T14, T21, T13))
PB_IN_AGAGAG(T20, T14, T21, T13, X25, T15) → APPC_IN_AGAG(T20, T14, T21, T13)
APPC_IN_AGAG(.(T43, X63), T42, X64, .(T43, T44)) → U2_AGAG(T43, X63, T42, X64, T44, appC_in_agag(X63, T42, X64, T44))
APPC_IN_AGAG(.(T43, X63), T42, X64, .(T43, T44)) → APPC_IN_AGAG(X63, T42, X64, T44)
U8_AGAGAG(T20, T14, T21, T13, X25, T15, appC_out_agag(T20, T14, T21, T13)) → U9_AGAGAG(T20, T14, T21, T13, X25, T15, pK_in_ggagg(T20, T21, X25, T15, T14))
U8_AGAGAG(T20, T14, T21, T13, X25, T15, appC_out_agag(T20, T14, T21, T13)) → PK_IN_GGAGG(T20, T21, X25, T15, T14)
PK_IN_GGAGG(T20, T21, T51, T15, T14) → U10_GGAGG(T20, T21, T51, T15, T14, appD_in_gga(T20, T21, T51))
PK_IN_GGAGG(T20, T21, T51, T15, T14) → APPD_IN_GGA(T20, T21, T51)
APPD_IN_GGA(.(T65, T66), T67, .(T65, X92)) → U3_GGA(T65, T66, T67, X92, appD_in_gga(T66, T67, X92))
APPD_IN_GGA(.(T65, T66), T67, .(T65, X92)) → APPD_IN_GGA(T66, T67, X92)
U10_GGAGG(T20, T21, T51, T15, T14, appD_out_gga(T20, T21, T51)) → U11_GGAGG(T20, T21, T51, T15, T14, pL_in_ggg(T51, T15, T14))
U10_GGAGG(T20, T21, T51, T15, T14, appD_out_gga(T20, T21, T51)) → PL_IN_GGG(T51, T15, T14)
PL_IN_GGG(T51, T15, T14) → U12_GGG(T51, T15, T14, permE_in_gg(T51, T15))
PL_IN_GGG(T51, T15, T14) → PERME_IN_GG(T51, T15)
PERME_IN_GG(T76, .(T77, T78)) → U4_GG(T76, T77, T78, pF_in_agagag(X107, T77, X108, T76, X109, T78))
PERME_IN_GG(T76, .(T77, T78)) → PF_IN_AGAGAG(X107, T77, X108, T76, X109, T78)
PF_IN_AGAGAG(T83, T77, T84, T76, X109, T78) → U14_AGAGAG(T83, T77, T84, T76, X109, T78, appC_in_agag(T83, T77, T84, T76))
PF_IN_AGAGAG(T83, T77, T84, T76, X109, T78) → APPC_IN_AGAG(T83, T77, T84, T76)
U14_AGAGAG(T83, T77, T84, T76, X109, T78, appC_out_agag(T83, T77, T84, T76)) → U15_AGAGAG(T83, T77, T84, T76, X109, T78, pM_in_ggag(T83, T84, X109, T78))
U14_AGAGAG(T83, T77, T84, T76, X109, T78, appC_out_agag(T83, T77, T84, T76)) → PM_IN_GGAG(T83, T84, X109, T78)
PM_IN_GGAG(T83, T84, T91, T78) → U16_GGAG(T83, T84, T91, T78, appD_in_gga(T83, T84, T91))
PM_IN_GGAG(T83, T84, T91, T78) → APPD_IN_GGA(T83, T84, T91)
U16_GGAG(T83, T84, T91, T78, appD_out_gga(T83, T84, T91)) → U17_GGAG(T83, T84, T91, T78, permE_in_gg(T91, T78))
U16_GGAG(T83, T84, T91, T78, appD_out_gga(T83, T84, T91)) → PERME_IN_GG(T91, T78)
U12_GGG(T51, T15, T14, permE_out_gg(T51, T15)) → U13_GGG(T51, T15, T14, orderedG_in_gg(T14, T15))
U12_GGG(T51, T15, T14, permE_out_gg(T51, T15)) → ORDEREDG_IN_GG(T14, T15)
ORDEREDG_IN_GG(T105, .(T106, T107)) → U5_GG(T105, T106, T107, pH_in_ggg(T105, T106, T107))
ORDEREDG_IN_GG(T105, .(T106, T107)) → PH_IN_GGG(T105, T106, T107)
PH_IN_GGG(T105, T106, T107) → U18_GGG(T105, T106, T107, lessJ_in_gg(T105, T106))
PH_IN_GGG(T105, T106, T107) → LESSJ_IN_GG(T105, T106)
LESSJ_IN_GG(s(T121), T122) → U7_GG(T121, T122, lessI_in_gg(T121, T122))
LESSJ_IN_GG(s(T121), T122) → LESSI_IN_GG(T121, T122)
LESSI_IN_GG(s(T134), s(T135)) → U6_GG(T134, T135, lessI_in_gg(T134, T135))
LESSI_IN_GG(s(T134), s(T135)) → LESSI_IN_GG(T134, T135)
U18_GGG(T105, T106, T107, lessJ_out_gg(T105, T106)) → U19_GGG(T105, T106, T107, orderedG_in_gg(T106, T107))
U18_GGG(T105, T106, T107, lessJ_out_gg(T105, T106)) → ORDEREDG_IN_GG(T106, T107)

The TRS R consists of the following rules:

ssA_in_gg([], []) → ssA_out_gg([], [])
ssA_in_gg(T13, .(T14, T15)) → U1_gg(T13, T14, T15, pB_in_agagag(X23, T14, X24, T13, X25, T15))
pB_in_agagag(T20, T14, T21, T13, X25, T15) → U8_agagag(T20, T14, T21, T13, X25, T15, appC_in_agag(T20, T14, T21, T13))
appC_in_agag([], T34, T35, .(T34, T35)) → appC_out_agag([], T34, T35, .(T34, T35))
appC_in_agag(.(T43, X63), T42, X64, .(T43, T44)) → U2_agag(T43, X63, T42, X64, T44, appC_in_agag(X63, T42, X64, T44))
U2_agag(T43, X63, T42, X64, T44, appC_out_agag(X63, T42, X64, T44)) → appC_out_agag(.(T43, X63), T42, X64, .(T43, T44))
U8_agagag(T20, T14, T21, T13, X25, T15, appC_out_agag(T20, T14, T21, T13)) → U9_agagag(T20, T14, T21, T13, X25, T15, pK_in_ggagg(T20, T21, X25, T15, T14))
pK_in_ggagg(T20, T21, T51, T15, T14) → U10_ggagg(T20, T21, T51, T15, T14, appD_in_gga(T20, T21, T51))
appD_in_gga([], T58, T58) → appD_out_gga([], T58, T58)
appD_in_gga(.(T65, T66), T67, .(T65, X92)) → U3_gga(T65, T66, T67, X92, appD_in_gga(T66, T67, X92))
U3_gga(T65, T66, T67, X92, appD_out_gga(T66, T67, X92)) → appD_out_gga(.(T65, T66), T67, .(T65, X92))
U10_ggagg(T20, T21, T51, T15, T14, appD_out_gga(T20, T21, T51)) → U11_ggagg(T20, T21, T51, T15, T14, pL_in_ggg(T51, T15, T14))
pL_in_ggg(T51, T15, T14) → U12_ggg(T51, T15, T14, permE_in_gg(T51, T15))
permE_in_gg([], []) → permE_out_gg([], [])
permE_in_gg(T76, .(T77, T78)) → U4_gg(T76, T77, T78, pF_in_agagag(X107, T77, X108, T76, X109, T78))
pF_in_agagag(T83, T77, T84, T76, X109, T78) → U14_agagag(T83, T77, T84, T76, X109, T78, appC_in_agag(T83, T77, T84, T76))
U14_agagag(T83, T77, T84, T76, X109, T78, appC_out_agag(T83, T77, T84, T76)) → U15_agagag(T83, T77, T84, T76, X109, T78, pM_in_ggag(T83, T84, X109, T78))
pM_in_ggag(T83, T84, T91, T78) → U16_ggag(T83, T84, T91, T78, appD_in_gga(T83, T84, T91))
U16_ggag(T83, T84, T91, T78, appD_out_gga(T83, T84, T91)) → U17_ggag(T83, T84, T91, T78, permE_in_gg(T91, T78))
U17_ggag(T83, T84, T91, T78, permE_out_gg(T91, T78)) → pM_out_ggag(T83, T84, T91, T78)
U15_agagag(T83, T77, T84, T76, X109, T78, pM_out_ggag(T83, T84, X109, T78)) → pF_out_agagag(T83, T77, T84, T76, X109, T78)
U4_gg(T76, T77, T78, pF_out_agagag(X107, T77, X108, T76, X109, T78)) → permE_out_gg(T76, .(T77, T78))
U12_ggg(T51, T15, T14, permE_out_gg(T51, T15)) → U13_ggg(T51, T15, T14, orderedG_in_gg(T14, T15))
orderedG_in_gg(T98, []) → orderedG_out_gg(T98, [])
orderedG_in_gg(T105, .(T106, T107)) → U5_gg(T105, T106, T107, pH_in_ggg(T105, T106, T107))
pH_in_ggg(T105, T106, T107) → U18_ggg(T105, T106, T107, lessJ_in_gg(T105, T106))
lessJ_in_gg(0, T116) → lessJ_out_gg(0, T116)
lessJ_in_gg(s(T121), T122) → U7_gg(T121, T122, lessI_in_gg(T121, T122))
lessI_in_gg(0, s(T129)) → lessI_out_gg(0, s(T129))
lessI_in_gg(s(T134), s(T135)) → U6_gg(T134, T135, lessI_in_gg(T134, T135))
U6_gg(T134, T135, lessI_out_gg(T134, T135)) → lessI_out_gg(s(T134), s(T135))
U7_gg(T121, T122, lessI_out_gg(T121, T122)) → lessJ_out_gg(s(T121), T122)
U18_ggg(T105, T106, T107, lessJ_out_gg(T105, T106)) → U19_ggg(T105, T106, T107, orderedG_in_gg(T106, T107))
U19_ggg(T105, T106, T107, orderedG_out_gg(T106, T107)) → pH_out_ggg(T105, T106, T107)
U5_gg(T105, T106, T107, pH_out_ggg(T105, T106, T107)) → orderedG_out_gg(T105, .(T106, T107))
U13_ggg(T51, T15, T14, orderedG_out_gg(T14, T15)) → pL_out_ggg(T51, T15, T14)
U11_ggagg(T20, T21, T51, T15, T14, pL_out_ggg(T51, T15, T14)) → pK_out_ggagg(T20, T21, T51, T15, T14)
U9_agagag(T20, T14, T21, T13, X25, T15, pK_out_ggagg(T20, T21, X25, T15, T14)) → pB_out_agagag(T20, T14, T21, T13, X25, T15)
U1_gg(T13, T14, T15, pB_out_agagag(X23, T14, X24, T13, X25, T15)) → ssA_out_gg(T13, .(T14, T15))

The argument filtering Pi contains the following mapping:
ssA_in_gg(x1, x2) = ssA_in_gg(x1, x2)
[] = []
ssA_out_gg(x1, x2) = ssA_out_gg(x1, x2)
.(x1, x2) = .(x1, x2)
U1_gg(x1, x2, x3, x4) = U1_gg(x1, x2, x3, x4)
pB_in_agagag(x1, x2, x3, x4, x5, x6) = pB_in_agagag(x2, x4, x6)
U8_agagag(x1, x2, x3, x4, x5, x6, x7) = U8_agagag(x2, x4, x6, x7)
appC_in_agag(x1, x2, x3, x4) = appC_in_agag(x2, x4)
appC_out_agag(x1, x2, x3, x4) = appC_out_agag(x1, x2, x3, x4)
U2_agag(x1, x2, x3, x4, x5, x6) = U2_agag(x1, x3, x5, x6)
U9_agagag(x1, x2, x3, x4, x5, x6, x7) = U9_agagag(x1, x2, x3, x4, x6, x7)
pK_in_ggagg(x1, x2, x3, x4, x5) = pK_in_ggagg(x1, x2, x4, x5)
U10_ggagg(x1, x2, x3, x4, x5, x6) = U10_ggagg(x1, x2, x4, x5, x6)
appD_in_gga(x1, x2, x3) = appD_in_gga(x1, x2)
appD_out_gga(x1, x2, x3) = appD_out_gga(x1, x2, x3)
U3_gga(x1, x2, x3, x4, x5) = U3_gga(x1, x2, x3, x5)
U11_ggagg(x1, x2, x3, x4, x5, x6) = U11_ggagg(x1, x2, x3, x4, x5, x6)
pL_in_ggg(x1, x2, x3) = pL_in_ggg(x1, x2, x3)
U12_ggg(x1, x2, x3, x4) = U12_ggg(x1, x2, x3, x4)
permE_in_gg(x1, x2) = permE_in_gg(x1, x2)
permE_out_gg(x1, x2) = permE_out_gg(x1, x2)
U4_gg(x1, x2, x3, x4) = U4_gg(x1, x2, x3, x4)
pF_in_agagag(x1, x2, x3, x4, x5, x6) = pF_in_agagag(x2, x4, x6)
U14_agagag(x1, x2, x3, x4, x5, x6, x7) = U14_agagag(x2, x4, x6, x7)
U15_agagag(x1, x2, x3, x4, x5, x6, x7) = U15_agagag(x1, x2, x3, x4, x6, x7)
pM_in_ggag(x1, x2, x3, x4) = pM_in_ggag(x1, x2, x4)
U16_ggag(x1, x2, x3, x4, x5) = U16_ggag(x1, x2, x4, x5)
U17_ggag(x1, x2, x3, x4, x5) = U17_ggag(x1, x2, x3, x4, x5)
pM_out_ggag(x1, x2, x3, x4) = pM_out_ggag(x1, x2, x3, x4)
pF_out_agagag(x1, x2, x3, x4, x5, x6) = pF_out_agagag(x1, x2, x3, x4, x5, x6)
U13_ggg(x1, x2, x3, x4) = U13_ggg(x1, x2, x3, x4)
orderedG_in_gg(x1, x2) = orderedG_in_gg(x1, x2)
orderedG_out_gg(x1, x2) = orderedG_out_gg(x1, x2)
U5_gg(x1, x2, x3, x4) = U5_gg(x1, x2, x3, x4)
pH_in_ggg(x1, x2, x3) = pH_in_ggg(x1, x2, x3)
U18_ggg(x1, x2, x3, x4) = U18_ggg(x1, x2, x3, x4)
lessJ_in_gg(x1, x2) = lessJ_in_gg(x1, x2)
0 = 0
lessJ_out_gg(x1, x2) = lessJ_out_gg(x1, x2)
s(x1) = s(x1)
U7_gg(x1, x2, x3) = U7_gg(x1, x2, x3)
lessI_in_gg(x1, x2) = lessI_in_gg(x1, x2)
lessI_out_gg(x1, x2) = lessI_out_gg(x1, x2)
U6_gg(x1, x2, x3) = U6_gg(x1, x2, x3)
U19_ggg(x1, x2, x3, x4) = U19_ggg(x1, x2, x3, x4)
pH_out_ggg(x1, x2, x3) = pH_out_ggg(x1, x2, x3)
pL_out_ggg(x1, x2, x3) = pL_out_ggg(x1, x2, x3)
pK_out_ggagg(x1, x2, x3, x4, x5) = pK_out_ggagg(x1, x2, x3, x4, x5)
pB_out_agagag(x1, x2, x3, x4, x5, x6) = pB_out_agagag(x1, x2, x3, x4, x5, x6)
SSA_IN_GG(x1, x2) = SSA_IN_GG(x1, x2)
U1_GG(x1, x2, x3, x4) = U1_GG(x1, x2, x3, x4)
PB_IN_AGAGAG(x1, x2, x3, x4, x5, x6) = PB_IN_AGAGAG(x2, x4, x6)
U8_AGAGAG(x1, x2, x3, x4, x5, x6, x7) = U8_AGAGAG(x2, x4, x6, x7)
APPC_IN_AGAG(x1, x2, x3, x4) = APPC_IN_AGAG(x2, x4)
U2_AGAG(x1, x2, x3, x4, x5, x6) = U2_AGAG(x1, x3, x5, x6)
U9_AGAGAG(x1, x2, x3, x4, x5, x6, x7) = U9_AGAGAG(x1, x2, x3, x4, x6, x7)
PK_IN_GGAGG(x1, x2, x3, x4, x5) = PK_IN_GGAGG(x1, x2, x4, x5)
U10_GGAGG(x1, x2, x3, x4, x5, x6) = U10_GGAGG(x1, x2, x4, x5, x6)
APPD_IN_GGA(x1, x2, x3) = APPD_IN_GGA(x1, x2)
U3_GGA(x1, x2, x3, x4, x5) = U3_GGA(x1, x2, x3, x5)
U11_GGAGG(x1, x2, x3, x4, x5, x6) = U11_GGAGG(x1, x2, x3, x4, x5, x6)
PL_IN_GGG(x1, x2, x3) = PL_IN_GGG(x1, x2, x3)
U12_GGG(x1, x2, x3, x4) = U12_GGG(x1, x2, x3, x4)
PERME_IN_GG(x1, x2) = PERME_IN_GG(x1, x2)
U4_GG(x1, x2, x3, x4) = U4_GG(x1, x2, x3, x4)
PF_IN_AGAGAG(x1, x2, x3, x4, x5, x6) = PF_IN_AGAGAG(x2, x4, x6)
U14_AGAGAG(x1, x2, x3, x4, x5, x6, x7) = U14_AGAGAG(x2, x4, x6, x7)
U15_AGAGAG(x1, x2, x3, x4, x5, x6, x7) = U15_AGAGAG(x1, x2, x3, x4, x6, x7)
PM_IN_GGAG(x1, x2, x3, x4) = PM_IN_GGAG(x1, x2, x4)
U16_GGAG(x1, x2, x3, x4, x5) = U16_GGAG(x1, x2, x4, x5)
U17_GGAG(x1, x2, x3, x4, x5) = U17_GGAG(x1, x2, x3, x4, x5)
U13_GGG(x1, x2, x3, x4) = U13_GGG(x1, x2, x3, x4)
ORDEREDG_IN_GG(x1, x2) = ORDEREDG_IN_GG(x1, x2)
U5_GG(x1, x2, x3, x4) = U5_GG(x1, x2, x3, x4)
PH_IN_GGG(x1, x2, x3) = PH_IN_GGG(x1, x2, x3)
U18_GGG(x1, x2, x3, x4) = U18_GGG(x1, x2, x3, x4)
LESSJ_IN_GG(x1, x2) = LESSJ_IN_GG(x1, x2)
U7_GG(x1, x2, x3) = U7_GG(x1, x2, x3)
LESSI_IN_GG(x1, x2) = LESSI_IN_GG(x1, x2)
U6_GG(x1, x2, x3) = U6_GG(x1, x2, x3)
U19_GGG(x1, x2, x3, x4) = U19_GGG(x1, x2, x3, x4)

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

(4) Obligation:

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

SSA_IN_GG(T13, .(T14, T15)) → U1_GG(T13, T14, T15, pB_in_agagag(X23, T14, X24, T13, X25, T15))
SSA_IN_GG(T13, .(T14, T15)) → PB_IN_AGAGAG(X23, T14, X24, T13, X25, T15)
PB_IN_AGAGAG(T20, T14, T21, T13, X25, T15) → U8_AGAGAG(T20, T14, T21, T13, X25, T15, appC_in_agag(T20, T14, T21, T13))
PB_IN_AGAGAG(T20, T14, T21, T13, X25, T15) → APPC_IN_AGAG(T20, T14, T21, T13)
APPC_IN_AGAG(.(T43, X63), T42, X64, .(T43, T44)) → U2_AGAG(T43, X63, T42, X64, T44, appC_in_agag(X63, T42, X64, T44))
APPC_IN_AGAG(.(T43, X63), T42, X64, .(T43, T44)) → APPC_IN_AGAG(X63, T42, X64, T44)
U8_AGAGAG(T20, T14, T21, T13, X25, T15, appC_out_agag(T20, T14, T21, T13)) → U9_AGAGAG(T20, T14, T21, T13, X25, T15, pK_in_ggagg(T20, T21, X25, T15, T14))
U8_AGAGAG(T20, T14, T21, T13, X25, T15, appC_out_agag(T20, T14, T21, T13)) → PK_IN_GGAGG(T20, T21, X25, T15, T14)
PK_IN_GGAGG(T20, T21, T51, T15, T14) → U10_GGAGG(T20, T21, T51, T15, T14, appD_in_gga(T20, T21, T51))
PK_IN_GGAGG(T20, T21, T51, T15, T14) → APPD_IN_GGA(T20, T21, T51)
APPD_IN_GGA(.(T65, T66), T67, .(T65, X92)) → U3_GGA(T65, T66, T67, X92, appD_in_gga(T66, T67, X92))
APPD_IN_GGA(.(T65, T66), T67, .(T65, X92)) → APPD_IN_GGA(T66, T67, X92)
U10_GGAGG(T20, T21, T51, T15, T14, appD_out_gga(T20, T21, T51)) → U11_GGAGG(T20, T21, T51, T15, T14, pL_in_ggg(T51, T15, T14))
U10_GGAGG(T20, T21, T51, T15, T14, appD_out_gga(T20, T21, T51)) → PL_IN_GGG(T51, T15, T14)
PL_IN_GGG(T51, T15, T14) → U12_GGG(T51, T15, T14, permE_in_gg(T51, T15))
PL_IN_GGG(T51, T15, T14) → PERME_IN_GG(T51, T15)
PERME_IN_GG(T76, .(T77, T78)) → U4_GG(T76, T77, T78, pF_in_agagag(X107, T77, X108, T76, X109, T78))
PERME_IN_GG(T76, .(T77, T78)) → PF_IN_AGAGAG(X107, T77, X108, T76, X109, T78)
PF_IN_AGAGAG(T83, T77, T84, T76, X109, T78) → U14_AGAGAG(T83, T77, T84, T76, X109, T78, appC_in_agag(T83, T77, T84, T76))
PF_IN_AGAGAG(T83, T77, T84, T76, X109, T78) → APPC_IN_AGAG(T83, T77, T84, T76)
U14_AGAGAG(T83, T77, T84, T76, X109, T78, appC_out_agag(T83, T77, T84, T76)) → U15_AGAGAG(T83, T77, T84, T76, X109, T78, pM_in_ggag(T83, T84, X109, T78))
U14_AGAGAG(T83, T77, T84, T76, X109, T78, appC_out_agag(T83, T77, T84, T76)) → PM_IN_GGAG(T83, T84, X109, T78)
PM_IN_GGAG(T83, T84, T91, T78) → U16_GGAG(T83, T84, T91, T78, appD_in_gga(T83, T84, T91))
PM_IN_GGAG(T83, T84, T91, T78) → APPD_IN_GGA(T83, T84, T91)
U16_GGAG(T83, T84, T91, T78, appD_out_gga(T83, T84, T91)) → U17_GGAG(T83, T84, T91, T78, permE_in_gg(T91, T78))
U16_GGAG(T83, T84, T91, T78, appD_out_gga(T83, T84, T91)) → PERME_IN_GG(T91, T78)
U12_GGG(T51, T15, T14, permE_out_gg(T51, T15)) → U13_GGG(T51, T15, T14, orderedG_in_gg(T14, T15))
U12_GGG(T51, T15, T14, permE_out_gg(T51, T15)) → ORDEREDG_IN_GG(T14, T15)
ORDEREDG_IN_GG(T105, .(T106, T107)) → U5_GG(T105, T106, T107, pH_in_ggg(T105, T106, T107))
ORDEREDG_IN_GG(T105, .(T106, T107)) → PH_IN_GGG(T105, T106, T107)
PH_IN_GGG(T105, T106, T107) → U18_GGG(T105, T106, T107, lessJ_in_gg(T105, T106))
PH_IN_GGG(T105, T106, T107) → LESSJ_IN_GG(T105, T106)
LESSJ_IN_GG(s(T121), T122) → U7_GG(T121, T122, lessI_in_gg(T121, T122))
LESSJ_IN_GG(s(T121), T122) → LESSI_IN_GG(T121, T122)
LESSI_IN_GG(s(T134), s(T135)) → U6_GG(T134, T135, lessI_in_gg(T134, T135))
LESSI_IN_GG(s(T134), s(T135)) → LESSI_IN_GG(T134, T135)
U18_GGG(T105, T106, T107, lessJ_out_gg(T105, T106)) → U19_GGG(T105, T106, T107, orderedG_in_gg(T106, T107))
U18_GGG(T105, T106, T107, lessJ_out_gg(T105, T106)) → ORDEREDG_IN_GG(T106, T107)

The TRS R consists of the following rules:

ssA_in_gg([], []) → ssA_out_gg([], [])
ssA_in_gg(T13, .(T14, T15)) → U1_gg(T13, T14, T15, pB_in_agagag(X23, T14, X24, T13, X25, T15))
pB_in_agagag(T20, T14, T21, T13, X25, T15) → U8_agagag(T20, T14, T21, T13, X25, T15, appC_in_agag(T20, T14, T21, T13))
appC_in_agag([], T34, T35, .(T34, T35)) → appC_out_agag([], T34, T35, .(T34, T35))
appC_in_agag(.(T43, X63), T42, X64, .(T43, T44)) → U2_agag(T43, X63, T42, X64, T44, appC_in_agag(X63, T42, X64, T44))
U2_agag(T43, X63, T42, X64, T44, appC_out_agag(X63, T42, X64, T44)) → appC_out_agag(.(T43, X63), T42, X64, .(T43, T44))
U8_agagag(T20, T14, T21, T13, X25, T15, appC_out_agag(T20, T14, T21, T13)) → U9_agagag(T20, T14, T21, T13, X25, T15, pK_in_ggagg(T20, T21, X25, T15, T14))
pK_in_ggagg(T20, T21, T51, T15, T14) → U10_ggagg(T20, T21, T51, T15, T14, appD_in_gga(T20, T21, T51))
appD_in_gga([], T58, T58) → appD_out_gga([], T58, T58)
appD_in_gga(.(T65, T66), T67, .(T65, X92)) → U3_gga(T65, T66, T67, X92, appD_in_gga(T66, T67, X92))
U3_gga(T65, T66, T67, X92, appD_out_gga(T66, T67, X92)) → appD_out_gga(.(T65, T66), T67, .(T65, X92))
U10_ggagg(T20, T21, T51, T15, T14, appD_out_gga(T20, T21, T51)) → U11_ggagg(T20, T21, T51, T15, T14, pL_in_ggg(T51, T15, T14))
pL_in_ggg(T51, T15, T14) → U12_ggg(T51, T15, T14, permE_in_gg(T51, T15))
permE_in_gg([], []) → permE_out_gg([], [])
permE_in_gg(T76, .(T77, T78)) → U4_gg(T76, T77, T78, pF_in_agagag(X107, T77, X108, T76, X109, T78))
pF_in_agagag(T83, T77, T84, T76, X109, T78) → U14_agagag(T83, T77, T84, T76, X109, T78, appC_in_agag(T83, T77, T84, T76))
U14_agagag(T83, T77, T84, T76, X109, T78, appC_out_agag(T83, T77, T84, T76)) → U15_agagag(T83, T77, T84, T76, X109, T78, pM_in_ggag(T83, T84, X109, T78))
pM_in_ggag(T83, T84, T91, T78) → U16_ggag(T83, T84, T91, T78, appD_in_gga(T83, T84, T91))
U16_ggag(T83, T84, T91, T78, appD_out_gga(T83, T84, T91)) → U17_ggag(T83, T84, T91, T78, permE_in_gg(T91, T78))
U17_ggag(T83, T84, T91, T78, permE_out_gg(T91, T78)) → pM_out_ggag(T83, T84, T91, T78)
U15_agagag(T83, T77, T84, T76, X109, T78, pM_out_ggag(T83, T84, X109, T78)) → pF_out_agagag(T83, T77, T84, T76, X109, T78)
U4_gg(T76, T77, T78, pF_out_agagag(X107, T77, X108, T76, X109, T78)) → permE_out_gg(T76, .(T77, T78))
U12_ggg(T51, T15, T14, permE_out_gg(T51, T15)) → U13_ggg(T51, T15, T14, orderedG_in_gg(T14, T15))
orderedG_in_gg(T98, []) → orderedG_out_gg(T98, [])
orderedG_in_gg(T105, .(T106, T107)) → U5_gg(T105, T106, T107, pH_in_ggg(T105, T106, T107))
pH_in_ggg(T105, T106, T107) → U18_ggg(T105, T106, T107, lessJ_in_gg(T105, T106))
lessJ_in_gg(0, T116) → lessJ_out_gg(0, T116)
lessJ_in_gg(s(T121), T122) → U7_gg(T121, T122, lessI_in_gg(T121, T122))
lessI_in_gg(0, s(T129)) → lessI_out_gg(0, s(T129))
lessI_in_gg(s(T134), s(T135)) → U6_gg(T134, T135, lessI_in_gg(T134, T135))
U6_gg(T134, T135, lessI_out_gg(T134, T135)) → lessI_out_gg(s(T134), s(T135))
U7_gg(T121, T122, lessI_out_gg(T121, T122)) → lessJ_out_gg(s(T121), T122)
U18_ggg(T105, T106, T107, lessJ_out_gg(T105, T106)) → U19_ggg(T105, T106, T107, orderedG_in_gg(T106, T107))
U19_ggg(T105, T106, T107, orderedG_out_gg(T106, T107)) → pH_out_ggg(T105, T106, T107)
U5_gg(T105, T106, T107, pH_out_ggg(T105, T106, T107)) → orderedG_out_gg(T105, .(T106, T107))
U13_ggg(T51, T15, T14, orderedG_out_gg(T14, T15)) → pL_out_ggg(T51, T15, T14)
U11_ggagg(T20, T21, T51, T15, T14, pL_out_ggg(T51, T15, T14)) → pK_out_ggagg(T20, T21, T51, T15, T14)
U9_agagag(T20, T14, T21, T13, X25, T15, pK_out_ggagg(T20, T21, X25, T15, T14)) → pB_out_agagag(T20, T14, T21, T13, X25, T15)
U1_gg(T13, T14, T15, pB_out_agagag(X23, T14, X24, T13, X25, T15)) → ssA_out_gg(T13, .(T14, T15))

(5) DependencyGraphProof (EQUIVALENT transformation)

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

(6) Complex Obligation (AND)

(7) Obligation:

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

LESSI_IN_GG(s(T134), s(T135)) → LESSI_IN_GG(T134, T135)

The TRS R consists of the following rules:

ssA_in_gg([], []) → ssA_out_gg([], [])
ssA_in_gg(T13, .(T14, T15)) → U1_gg(T13, T14, T15, pB_in_agagag(X23, T14, X24, T13, X25, T15))
pB_in_agagag(T20, T14, T21, T13, X25, T15) → U8_agagag(T20, T14, T21, T13, X25, T15, appC_in_agag(T20, T14, T21, T13))
appC_in_agag([], T34, T35, .(T34, T35)) → appC_out_agag([], T34, T35, .(T34, T35))
appC_in_agag(.(T43, X63), T42, X64, .(T43, T44)) → U2_agag(T43, X63, T42, X64, T44, appC_in_agag(X63, T42, X64, T44))
U2_agag(T43, X63, T42, X64, T44, appC_out_agag(X63, T42, X64, T44)) → appC_out_agag(.(T43, X63), T42, X64, .(T43, T44))
U8_agagag(T20, T14, T21, T13, X25, T15, appC_out_agag(T20, T14, T21, T13)) → U9_agagag(T20, T14, T21, T13, X25, T15, pK_in_ggagg(T20, T21, X25, T15, T14))
pK_in_ggagg(T20, T21, T51, T15, T14) → U10_ggagg(T20, T21, T51, T15, T14, appD_in_gga(T20, T21, T51))
appD_in_gga([], T58, T58) → appD_out_gga([], T58, T58)
appD_in_gga(.(T65, T66), T67, .(T65, X92)) → U3_gga(T65, T66, T67, X92, appD_in_gga(T66, T67, X92))
U3_gga(T65, T66, T67, X92, appD_out_gga(T66, T67, X92)) → appD_out_gga(.(T65, T66), T67, .(T65, X92))
U10_ggagg(T20, T21, T51, T15, T14, appD_out_gga(T20, T21, T51)) → U11_ggagg(T20, T21, T51, T15, T14, pL_in_ggg(T51, T15, T14))
pL_in_ggg(T51, T15, T14) → U12_ggg(T51, T15, T14, permE_in_gg(T51, T15))
permE_in_gg([], []) → permE_out_gg([], [])
permE_in_gg(T76, .(T77, T78)) → U4_gg(T76, T77, T78, pF_in_agagag(X107, T77, X108, T76, X109, T78))
pF_in_agagag(T83, T77, T84, T76, X109, T78) → U14_agagag(T83, T77, T84, T76, X109, T78, appC_in_agag(T83, T77, T84, T76))
U14_agagag(T83, T77, T84, T76, X109, T78, appC_out_agag(T83, T77, T84, T76)) → U15_agagag(T83, T77, T84, T76, X109, T78, pM_in_ggag(T83, T84, X109, T78))
pM_in_ggag(T83, T84, T91, T78) → U16_ggag(T83, T84, T91, T78, appD_in_gga(T83, T84, T91))
U16_ggag(T83, T84, T91, T78, appD_out_gga(T83, T84, T91)) → U17_ggag(T83, T84, T91, T78, permE_in_gg(T91, T78))
U17_ggag(T83, T84, T91, T78, permE_out_gg(T91, T78)) → pM_out_ggag(T83, T84, T91, T78)
U15_agagag(T83, T77, T84, T76, X109, T78, pM_out_ggag(T83, T84, X109, T78)) → pF_out_agagag(T83, T77, T84, T76, X109, T78)
U4_gg(T76, T77, T78, pF_out_agagag(X107, T77, X108, T76, X109, T78)) → permE_out_gg(T76, .(T77, T78))
U12_ggg(T51, T15, T14, permE_out_gg(T51, T15)) → U13_ggg(T51, T15, T14, orderedG_in_gg(T14, T15))
orderedG_in_gg(T98, []) → orderedG_out_gg(T98, [])
orderedG_in_gg(T105, .(T106, T107)) → U5_gg(T105, T106, T107, pH_in_ggg(T105, T106, T107))
pH_in_ggg(T105, T106, T107) → U18_ggg(T105, T106, T107, lessJ_in_gg(T105, T106))
lessJ_in_gg(0, T116) → lessJ_out_gg(0, T116)
lessJ_in_gg(s(T121), T122) → U7_gg(T121, T122, lessI_in_gg(T121, T122))
lessI_in_gg(0, s(T129)) → lessI_out_gg(0, s(T129))
lessI_in_gg(s(T134), s(T135)) → U6_gg(T134, T135, lessI_in_gg(T134, T135))
U6_gg(T134, T135, lessI_out_gg(T134, T135)) → lessI_out_gg(s(T134), s(T135))
U7_gg(T121, T122, lessI_out_gg(T121, T122)) → lessJ_out_gg(s(T121), T122)
U18_ggg(T105, T106, T107, lessJ_out_gg(T105, T106)) → U19_ggg(T105, T106, T107, orderedG_in_gg(T106, T107))
U19_ggg(T105, T106, T107, orderedG_out_gg(T106, T107)) → pH_out_ggg(T105, T106, T107)
U5_gg(T105, T106, T107, pH_out_ggg(T105, T106, T107)) → orderedG_out_gg(T105, .(T106, T107))
U13_ggg(T51, T15, T14, orderedG_out_gg(T14, T15)) → pL_out_ggg(T51, T15, T14)
U11_ggagg(T20, T21, T51, T15, T14, pL_out_ggg(T51, T15, T14)) → pK_out_ggagg(T20, T21, T51, T15, T14)
U9_agagag(T20, T14, T21, T13, X25, T15, pK_out_ggagg(T20, T21, X25, T15, T14)) → pB_out_agagag(T20, T14, T21, T13, X25, T15)
U1_gg(T13, T14, T15, pB_out_agagag(X23, T14, X24, T13, X25, T15)) → ssA_out_gg(T13, .(T14, T15))

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

LESSI_IN_GG(s(T134), s(T135)) → LESSI_IN_GG(T134, T135)

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:

LESSI_IN_GG(s(T134), s(T135)) → LESSI_IN_GG(T134, T135)

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:

LESSI_IN_GG(s(T134), s(T135)) → LESSI_IN_GG(T134, T135)
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:

ORDEREDG_IN_GG(T105, .(T106, T107)) → PH_IN_GGG(T105, T106, T107)
PH_IN_GGG(T105, T106, T107) → U18_GGG(T105, T106, T107, lessJ_in_gg(T105, T106))
U18_GGG(T105, T106, T107, lessJ_out_gg(T105, T106)) → ORDEREDG_IN_GG(T106, T107)

The TRS R consists of the following rules:

ssA_in_gg([], []) → ssA_out_gg([], [])
ssA_in_gg(T13, .(T14, T15)) → U1_gg(T13, T14, T15, pB_in_agagag(X23, T14, X24, T13, X25, T15))
pB_in_agagag(T20, T14, T21, T13, X25, T15) → U8_agagag(T20, T14, T21, T13, X25, T15, appC_in_agag(T20, T14, T21, T13))
appC_in_agag([], T34, T35, .(T34, T35)) → appC_out_agag([], T34, T35, .(T34, T35))
appC_in_agag(.(T43, X63), T42, X64, .(T43, T44)) → U2_agag(T43, X63, T42, X64, T44, appC_in_agag(X63, T42, X64, T44))
U2_agag(T43, X63, T42, X64, T44, appC_out_agag(X63, T42, X64, T44)) → appC_out_agag(.(T43, X63), T42, X64, .(T43, T44))
U8_agagag(T20, T14, T21, T13, X25, T15, appC_out_agag(T20, T14, T21, T13)) → U9_agagag(T20, T14, T21, T13, X25, T15, pK_in_ggagg(T20, T21, X25, T15, T14))
pK_in_ggagg(T20, T21, T51, T15, T14) → U10_ggagg(T20, T21, T51, T15, T14, appD_in_gga(T20, T21, T51))
appD_in_gga([], T58, T58) → appD_out_gga([], T58, T58)
appD_in_gga(.(T65, T66), T67, .(T65, X92)) → U3_gga(T65, T66, T67, X92, appD_in_gga(T66, T67, X92))
U3_gga(T65, T66, T67, X92, appD_out_gga(T66, T67, X92)) → appD_out_gga(.(T65, T66), T67, .(T65, X92))
U10_ggagg(T20, T21, T51, T15, T14, appD_out_gga(T20, T21, T51)) → U11_ggagg(T20, T21, T51, T15, T14, pL_in_ggg(T51, T15, T14))
pL_in_ggg(T51, T15, T14) → U12_ggg(T51, T15, T14, permE_in_gg(T51, T15))
permE_in_gg([], []) → permE_out_gg([], [])
permE_in_gg(T76, .(T77, T78)) → U4_gg(T76, T77, T78, pF_in_agagag(X107, T77, X108, T76, X109, T78))
pF_in_agagag(T83, T77, T84, T76, X109, T78) → U14_agagag(T83, T77, T84, T76, X109, T78, appC_in_agag(T83, T77, T84, T76))
U14_agagag(T83, T77, T84, T76, X109, T78, appC_out_agag(T83, T77, T84, T76)) → U15_agagag(T83, T77, T84, T76, X109, T78, pM_in_ggag(T83, T84, X109, T78))
pM_in_ggag(T83, T84, T91, T78) → U16_ggag(T83, T84, T91, T78, appD_in_gga(T83, T84, T91))
U16_ggag(T83, T84, T91, T78, appD_out_gga(T83, T84, T91)) → U17_ggag(T83, T84, T91, T78, permE_in_gg(T91, T78))
U17_ggag(T83, T84, T91, T78, permE_out_gg(T91, T78)) → pM_out_ggag(T83, T84, T91, T78)
U15_agagag(T83, T77, T84, T76, X109, T78, pM_out_ggag(T83, T84, X109, T78)) → pF_out_agagag(T83, T77, T84, T76, X109, T78)
U4_gg(T76, T77, T78, pF_out_agagag(X107, T77, X108, T76, X109, T78)) → permE_out_gg(T76, .(T77, T78))
U12_ggg(T51, T15, T14, permE_out_gg(T51, T15)) → U13_ggg(T51, T15, T14, orderedG_in_gg(T14, T15))
orderedG_in_gg(T98, []) → orderedG_out_gg(T98, [])
orderedG_in_gg(T105, .(T106, T107)) → U5_gg(T105, T106, T107, pH_in_ggg(T105, T106, T107))
pH_in_ggg(T105, T106, T107) → U18_ggg(T105, T106, T107, lessJ_in_gg(T105, T106))
lessJ_in_gg(0, T116) → lessJ_out_gg(0, T116)
lessJ_in_gg(s(T121), T122) → U7_gg(T121, T122, lessI_in_gg(T121, T122))
lessI_in_gg(0, s(T129)) → lessI_out_gg(0, s(T129))
lessI_in_gg(s(T134), s(T135)) → U6_gg(T134, T135, lessI_in_gg(T134, T135))
U6_gg(T134, T135, lessI_out_gg(T134, T135)) → lessI_out_gg(s(T134), s(T135))
U7_gg(T121, T122, lessI_out_gg(T121, T122)) → lessJ_out_gg(s(T121), T122)
U18_ggg(T105, T106, T107, lessJ_out_gg(T105, T106)) → U19_ggg(T105, T106, T107, orderedG_in_gg(T106, T107))
U19_ggg(T105, T106, T107, orderedG_out_gg(T106, T107)) → pH_out_ggg(T105, T106, T107)
U5_gg(T105, T106, T107, pH_out_ggg(T105, T106, T107)) → orderedG_out_gg(T105, .(T106, T107))
U13_ggg(T51, T15, T14, orderedG_out_gg(T14, T15)) → pL_out_ggg(T51, T15, T14)
U11_ggagg(T20, T21, T51, T15, T14, pL_out_ggg(T51, T15, T14)) → pK_out_ggagg(T20, T21, T51, T15, T14)
U9_agagag(T20, T14, T21, T13, X25, T15, pK_out_ggagg(T20, T21, X25, T15, T14)) → pB_out_agagag(T20, T14, T21, T13, X25, T15)
U1_gg(T13, T14, T15, pB_out_agagag(X23, T14, X24, T13, X25, T15)) → ssA_out_gg(T13, .(T14, T15))

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

ORDEREDG_IN_GG(T105, .(T106, T107)) → PH_IN_GGG(T105, T106, T107)
PH_IN_GGG(T105, T106, T107) → U18_GGG(T105, T106, T107, lessJ_in_gg(T105, T106))
U18_GGG(T105, T106, T107, lessJ_out_gg(T105, T106)) → ORDEREDG_IN_GG(T106, T107)

The TRS R consists of the following rules:

lessJ_in_gg(0, T116) → lessJ_out_gg(0, T116)
lessJ_in_gg(s(T121), T122) → U7_gg(T121, T122, lessI_in_gg(T121, T122))
U7_gg(T121, T122, lessI_out_gg(T121, T122)) → lessJ_out_gg(s(T121), T122)
lessI_in_gg(0, s(T129)) → lessI_out_gg(0, s(T129))
lessI_in_gg(s(T134), s(T135)) → U6_gg(T134, T135, lessI_in_gg(T134, T135))
U6_gg(T134, T135, lessI_out_gg(T134, T135)) → lessI_out_gg(s(T134), s(T135))

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:

ORDEREDG_IN_GG(T105, .(T106, T107)) → PH_IN_GGG(T105, T106, T107)
PH_IN_GGG(T105, T106, T107) → U18_GGG(T105, T106, T107, lessJ_in_gg(T105, T106))
U18_GGG(T105, T106, T107, lessJ_out_gg(T105, T106)) → ORDEREDG_IN_GG(T106, T107)

The TRS R consists of the following rules:

lessJ_in_gg(0, T116) → lessJ_out_gg(0, T116)
lessJ_in_gg(s(T121), T122) → U7_gg(T121, T122, lessI_in_gg(T121, T122))
U7_gg(T121, T122, lessI_out_gg(T121, T122)) → lessJ_out_gg(s(T121), T122)
lessI_in_gg(0, s(T129)) → lessI_out_gg(0, s(T129))
lessI_in_gg(s(T134), s(T135)) → U6_gg(T134, T135, lessI_in_gg(T134, T135))
U6_gg(T134, T135, lessI_out_gg(T134, T135)) → lessI_out_gg(s(T134), s(T135))

The set Q consists of the following terms:

lessJ_in_gg(x0, x1)
U7_gg(x0, x1, x2)
lessI_in_gg(x0, x1)
U6_gg(x0, x1, x2)

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:

PH_IN_GGG(T105, T106, T107) → U18_GGG(T105, T106, T107, lessJ_in_gg(T105, T106))
The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 3
U18_GGG(T105, T106, T107, lessJ_out_gg(T105, T106)) → ORDEREDG_IN_GG(T106, T107)
The graph contains the following edges 2 >= 1, 4 > 1, 3 >= 2
ORDEREDG_IN_GG(T105, .(T106, T107)) → PH_IN_GGG(T105, T106, T107)
The graph contains the following edges 1 >= 1, 2 > 2, 2 > 3

(20) YES

(21) Obligation:

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

APPD_IN_GGA(.(T65, T66), T67, .(T65, X92)) → APPD_IN_GGA(T66, T67, X92)

The TRS R consists of the following rules:

ssA_in_gg([], []) → ssA_out_gg([], [])
ssA_in_gg(T13, .(T14, T15)) → U1_gg(T13, T14, T15, pB_in_agagag(X23, T14, X24, T13, X25, T15))
pB_in_agagag(T20, T14, T21, T13, X25, T15) → U8_agagag(T20, T14, T21, T13, X25, T15, appC_in_agag(T20, T14, T21, T13))
appC_in_agag([], T34, T35, .(T34, T35)) → appC_out_agag([], T34, T35, .(T34, T35))
appC_in_agag(.(T43, X63), T42, X64, .(T43, T44)) → U2_agag(T43, X63, T42, X64, T44, appC_in_agag(X63, T42, X64, T44))
U2_agag(T43, X63, T42, X64, T44, appC_out_agag(X63, T42, X64, T44)) → appC_out_agag(.(T43, X63), T42, X64, .(T43, T44))
U8_agagag(T20, T14, T21, T13, X25, T15, appC_out_agag(T20, T14, T21, T13)) → U9_agagag(T20, T14, T21, T13, X25, T15, pK_in_ggagg(T20, T21, X25, T15, T14))
pK_in_ggagg(T20, T21, T51, T15, T14) → U10_ggagg(T20, T21, T51, T15, T14, appD_in_gga(T20, T21, T51))
appD_in_gga([], T58, T58) → appD_out_gga([], T58, T58)
appD_in_gga(.(T65, T66), T67, .(T65, X92)) → U3_gga(T65, T66, T67, X92, appD_in_gga(T66, T67, X92))
U3_gga(T65, T66, T67, X92, appD_out_gga(T66, T67, X92)) → appD_out_gga(.(T65, T66), T67, .(T65, X92))
U10_ggagg(T20, T21, T51, T15, T14, appD_out_gga(T20, T21, T51)) → U11_ggagg(T20, T21, T51, T15, T14, pL_in_ggg(T51, T15, T14))
pL_in_ggg(T51, T15, T14) → U12_ggg(T51, T15, T14, permE_in_gg(T51, T15))
permE_in_gg([], []) → permE_out_gg([], [])
permE_in_gg(T76, .(T77, T78)) → U4_gg(T76, T77, T78, pF_in_agagag(X107, T77, X108, T76, X109, T78))
pF_in_agagag(T83, T77, T84, T76, X109, T78) → U14_agagag(T83, T77, T84, T76, X109, T78, appC_in_agag(T83, T77, T84, T76))
U14_agagag(T83, T77, T84, T76, X109, T78, appC_out_agag(T83, T77, T84, T76)) → U15_agagag(T83, T77, T84, T76, X109, T78, pM_in_ggag(T83, T84, X109, T78))
pM_in_ggag(T83, T84, T91, T78) → U16_ggag(T83, T84, T91, T78, appD_in_gga(T83, T84, T91))
U16_ggag(T83, T84, T91, T78, appD_out_gga(T83, T84, T91)) → U17_ggag(T83, T84, T91, T78, permE_in_gg(T91, T78))
U17_ggag(T83, T84, T91, T78, permE_out_gg(T91, T78)) → pM_out_ggag(T83, T84, T91, T78)
U15_agagag(T83, T77, T84, T76, X109, T78, pM_out_ggag(T83, T84, X109, T78)) → pF_out_agagag(T83, T77, T84, T76, X109, T78)
U4_gg(T76, T77, T78, pF_out_agagag(X107, T77, X108, T76, X109, T78)) → permE_out_gg(T76, .(T77, T78))
U12_ggg(T51, T15, T14, permE_out_gg(T51, T15)) → U13_ggg(T51, T15, T14, orderedG_in_gg(T14, T15))
orderedG_in_gg(T98, []) → orderedG_out_gg(T98, [])
orderedG_in_gg(T105, .(T106, T107)) → U5_gg(T105, T106, T107, pH_in_ggg(T105, T106, T107))
pH_in_ggg(T105, T106, T107) → U18_ggg(T105, T106, T107, lessJ_in_gg(T105, T106))
lessJ_in_gg(0, T116) → lessJ_out_gg(0, T116)
lessJ_in_gg(s(T121), T122) → U7_gg(T121, T122, lessI_in_gg(T121, T122))
lessI_in_gg(0, s(T129)) → lessI_out_gg(0, s(T129))
lessI_in_gg(s(T134), s(T135)) → U6_gg(T134, T135, lessI_in_gg(T134, T135))
U6_gg(T134, T135, lessI_out_gg(T134, T135)) → lessI_out_gg(s(T134), s(T135))
U7_gg(T121, T122, lessI_out_gg(T121, T122)) → lessJ_out_gg(s(T121), T122)
U18_ggg(T105, T106, T107, lessJ_out_gg(T105, T106)) → U19_ggg(T105, T106, T107, orderedG_in_gg(T106, T107))
U19_ggg(T105, T106, T107, orderedG_out_gg(T106, T107)) → pH_out_ggg(T105, T106, T107)
U5_gg(T105, T106, T107, pH_out_ggg(T105, T106, T107)) → orderedG_out_gg(T105, .(T106, T107))
U13_ggg(T51, T15, T14, orderedG_out_gg(T14, T15)) → pL_out_ggg(T51, T15, T14)
U11_ggagg(T20, T21, T51, T15, T14, pL_out_ggg(T51, T15, T14)) → pK_out_ggagg(T20, T21, T51, T15, T14)
U9_agagag(T20, T14, T21, T13, X25, T15, pK_out_ggagg(T20, T21, X25, T15, T14)) → pB_out_agagag(T20, T14, T21, T13, X25, T15)
U1_gg(T13, T14, T15, pB_out_agagag(X23, T14, X24, T13, X25, T15)) → ssA_out_gg(T13, .(T14, T15))

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

APPD_IN_GGA(.(T65, T66), T67, .(T65, X92)) → APPD_IN_GGA(T66, T67, X92)

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

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:

APPD_IN_GGA(.(T65, T66), T67) → APPD_IN_GGA(T66, T67)

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

(26) QDPSizeChangeProof (EQUIVALENT transformation)

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

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

APPD_IN_GGA(.(T65, T66), T67) → APPD_IN_GGA(T66, T67)
The graph contains the following edges 1 > 1, 2 >= 2

(27) YES

(28) Obligation:

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

APPC_IN_AGAG(.(T43, X63), T42, X64, .(T43, T44)) → APPC_IN_AGAG(X63, T42, X64, T44)

The TRS R consists of the following rules:

ssA_in_gg([], []) → ssA_out_gg([], [])
ssA_in_gg(T13, .(T14, T15)) → U1_gg(T13, T14, T15, pB_in_agagag(X23, T14, X24, T13, X25, T15))
pB_in_agagag(T20, T14, T21, T13, X25, T15) → U8_agagag(T20, T14, T21, T13, X25, T15, appC_in_agag(T20, T14, T21, T13))
appC_in_agag([], T34, T35, .(T34, T35)) → appC_out_agag([], T34, T35, .(T34, T35))
appC_in_agag(.(T43, X63), T42, X64, .(T43, T44)) → U2_agag(T43, X63, T42, X64, T44, appC_in_agag(X63, T42, X64, T44))
U2_agag(T43, X63, T42, X64, T44, appC_out_agag(X63, T42, X64, T44)) → appC_out_agag(.(T43, X63), T42, X64, .(T43, T44))
U8_agagag(T20, T14, T21, T13, X25, T15, appC_out_agag(T20, T14, T21, T13)) → U9_agagag(T20, T14, T21, T13, X25, T15, pK_in_ggagg(T20, T21, X25, T15, T14))
pK_in_ggagg(T20, T21, T51, T15, T14) → U10_ggagg(T20, T21, T51, T15, T14, appD_in_gga(T20, T21, T51))
appD_in_gga([], T58, T58) → appD_out_gga([], T58, T58)
appD_in_gga(.(T65, T66), T67, .(T65, X92)) → U3_gga(T65, T66, T67, X92, appD_in_gga(T66, T67, X92))
U3_gga(T65, T66, T67, X92, appD_out_gga(T66, T67, X92)) → appD_out_gga(.(T65, T66), T67, .(T65, X92))
U10_ggagg(T20, T21, T51, T15, T14, appD_out_gga(T20, T21, T51)) → U11_ggagg(T20, T21, T51, T15, T14, pL_in_ggg(T51, T15, T14))
pL_in_ggg(T51, T15, T14) → U12_ggg(T51, T15, T14, permE_in_gg(T51, T15))
permE_in_gg([], []) → permE_out_gg([], [])
permE_in_gg(T76, .(T77, T78)) → U4_gg(T76, T77, T78, pF_in_agagag(X107, T77, X108, T76, X109, T78))
pF_in_agagag(T83, T77, T84, T76, X109, T78) → U14_agagag(T83, T77, T84, T76, X109, T78, appC_in_agag(T83, T77, T84, T76))
U14_agagag(T83, T77, T84, T76, X109, T78, appC_out_agag(T83, T77, T84, T76)) → U15_agagag(T83, T77, T84, T76, X109, T78, pM_in_ggag(T83, T84, X109, T78))
pM_in_ggag(T83, T84, T91, T78) → U16_ggag(T83, T84, T91, T78, appD_in_gga(T83, T84, T91))
U16_ggag(T83, T84, T91, T78, appD_out_gga(T83, T84, T91)) → U17_ggag(T83, T84, T91, T78, permE_in_gg(T91, T78))
U17_ggag(T83, T84, T91, T78, permE_out_gg(T91, T78)) → pM_out_ggag(T83, T84, T91, T78)
U15_agagag(T83, T77, T84, T76, X109, T78, pM_out_ggag(T83, T84, X109, T78)) → pF_out_agagag(T83, T77, T84, T76, X109, T78)
U4_gg(T76, T77, T78, pF_out_agagag(X107, T77, X108, T76, X109, T78)) → permE_out_gg(T76, .(T77, T78))
U12_ggg(T51, T15, T14, permE_out_gg(T51, T15)) → U13_ggg(T51, T15, T14, orderedG_in_gg(T14, T15))
orderedG_in_gg(T98, []) → orderedG_out_gg(T98, [])
orderedG_in_gg(T105, .(T106, T107)) → U5_gg(T105, T106, T107, pH_in_ggg(T105, T106, T107))
pH_in_ggg(T105, T106, T107) → U18_ggg(T105, T106, T107, lessJ_in_gg(T105, T106))
lessJ_in_gg(0, T116) → lessJ_out_gg(0, T116)
lessJ_in_gg(s(T121), T122) → U7_gg(T121, T122, lessI_in_gg(T121, T122))
lessI_in_gg(0, s(T129)) → lessI_out_gg(0, s(T129))
lessI_in_gg(s(T134), s(T135)) → U6_gg(T134, T135, lessI_in_gg(T134, T135))
U6_gg(T134, T135, lessI_out_gg(T134, T135)) → lessI_out_gg(s(T134), s(T135))
U7_gg(T121, T122, lessI_out_gg(T121, T122)) → lessJ_out_gg(s(T121), T122)
U18_ggg(T105, T106, T107, lessJ_out_gg(T105, T106)) → U19_ggg(T105, T106, T107, orderedG_in_gg(T106, T107))
U19_ggg(T105, T106, T107, orderedG_out_gg(T106, T107)) → pH_out_ggg(T105, T106, T107)
U5_gg(T105, T106, T107, pH_out_ggg(T105, T106, T107)) → orderedG_out_gg(T105, .(T106, T107))
U13_ggg(T51, T15, T14, orderedG_out_gg(T14, T15)) → pL_out_ggg(T51, T15, T14)
U11_ggagg(T20, T21, T51, T15, T14, pL_out_ggg(T51, T15, T14)) → pK_out_ggagg(T20, T21, T51, T15, T14)
U9_agagag(T20, T14, T21, T13, X25, T15, pK_out_ggagg(T20, T21, X25, T15, T14)) → pB_out_agagag(T20, T14, T21, T13, X25, T15)
U1_gg(T13, T14, T15, pB_out_agagag(X23, T14, X24, T13, X25, T15)) → ssA_out_gg(T13, .(T14, T15))

(29) UsableRulesProof (EQUIVALENT transformation)

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

(30) Obligation:

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

APPC_IN_AGAG(.(T43, X63), T42, X64, .(T43, T44)) → APPC_IN_AGAG(X63, T42, X64, T44)

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

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

(31) PiDPToQDPProof (SOUND transformation)

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

(32) Obligation:

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

APPC_IN_AGAG(T42, .(T43, T44)) → APPC_IN_AGAG(T42, T44)

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

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

APPC_IN_AGAG(T42, .(T43, T44)) → APPC_IN_AGAG(T42, T44)
The graph contains the following edges 1 >= 1, 2 > 2

(34) YES

(35) Obligation:

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

PF_IN_AGAGAG(T83, T77, T84, T76, X109, T78) → U14_AGAGAG(T83, T77, T84, T76, X109, T78, appC_in_agag(T83, T77, T84, T76))
U14_AGAGAG(T83, T77, T84, T76, X109, T78, appC_out_agag(T83, T77, T84, T76)) → PM_IN_GGAG(T83, T84, X109, T78)
PM_IN_GGAG(T83, T84, T91, T78) → U16_GGAG(T83, T84, T91, T78, appD_in_gga(T83, T84, T91))
U16_GGAG(T83, T84, T91, T78, appD_out_gga(T83, T84, T91)) → PERME_IN_GG(T91, T78)
PERME_IN_GG(T76, .(T77, T78)) → PF_IN_AGAGAG(X107, T77, X108, T76, X109, T78)

The TRS R consists of the following rules:

ssA_in_gg([], []) → ssA_out_gg([], [])
ssA_in_gg(T13, .(T14, T15)) → U1_gg(T13, T14, T15, pB_in_agagag(X23, T14, X24, T13, X25, T15))
pB_in_agagag(T20, T14, T21, T13, X25, T15) → U8_agagag(T20, T14, T21, T13, X25, T15, appC_in_agag(T20, T14, T21, T13))
appC_in_agag([], T34, T35, .(T34, T35)) → appC_out_agag([], T34, T35, .(T34, T35))
appC_in_agag(.(T43, X63), T42, X64, .(T43, T44)) → U2_agag(T43, X63, T42, X64, T44, appC_in_agag(X63, T42, X64, T44))
U2_agag(T43, X63, T42, X64, T44, appC_out_agag(X63, T42, X64, T44)) → appC_out_agag(.(T43, X63), T42, X64, .(T43, T44))
U8_agagag(T20, T14, T21, T13, X25, T15, appC_out_agag(T20, T14, T21, T13)) → U9_agagag(T20, T14, T21, T13, X25, T15, pK_in_ggagg(T20, T21, X25, T15, T14))
pK_in_ggagg(T20, T21, T51, T15, T14) → U10_ggagg(T20, T21, T51, T15, T14, appD_in_gga(T20, T21, T51))
appD_in_gga([], T58, T58) → appD_out_gga([], T58, T58)
appD_in_gga(.(T65, T66), T67, .(T65, X92)) → U3_gga(T65, T66, T67, X92, appD_in_gga(T66, T67, X92))
U3_gga(T65, T66, T67, X92, appD_out_gga(T66, T67, X92)) → appD_out_gga(.(T65, T66), T67, .(T65, X92))
U10_ggagg(T20, T21, T51, T15, T14, appD_out_gga(T20, T21, T51)) → U11_ggagg(T20, T21, T51, T15, T14, pL_in_ggg(T51, T15, T14))
pL_in_ggg(T51, T15, T14) → U12_ggg(T51, T15, T14, permE_in_gg(T51, T15))
permE_in_gg([], []) → permE_out_gg([], [])
permE_in_gg(T76, .(T77, T78)) → U4_gg(T76, T77, T78, pF_in_agagag(X107, T77, X108, T76, X109, T78))
pF_in_agagag(T83, T77, T84, T76, X109, T78) → U14_agagag(T83, T77, T84, T76, X109, T78, appC_in_agag(T83, T77, T84, T76))
U14_agagag(T83, T77, T84, T76, X109, T78, appC_out_agag(T83, T77, T84, T76)) → U15_agagag(T83, T77, T84, T76, X109, T78, pM_in_ggag(T83, T84, X109, T78))
pM_in_ggag(T83, T84, T91, T78) → U16_ggag(T83, T84, T91, T78, appD_in_gga(T83, T84, T91))
U16_ggag(T83, T84, T91, T78, appD_out_gga(T83, T84, T91)) → U17_ggag(T83, T84, T91, T78, permE_in_gg(T91, T78))
U17_ggag(T83, T84, T91, T78, permE_out_gg(T91, T78)) → pM_out_ggag(T83, T84, T91, T78)
U15_agagag(T83, T77, T84, T76, X109, T78, pM_out_ggag(T83, T84, X109, T78)) → pF_out_agagag(T83, T77, T84, T76, X109, T78)
U4_gg(T76, T77, T78, pF_out_agagag(X107, T77, X108, T76, X109, T78)) → permE_out_gg(T76, .(T77, T78))
U12_ggg(T51, T15, T14, permE_out_gg(T51, T15)) → U13_ggg(T51, T15, T14, orderedG_in_gg(T14, T15))
orderedG_in_gg(T98, []) → orderedG_out_gg(T98, [])
orderedG_in_gg(T105, .(T106, T107)) → U5_gg(T105, T106, T107, pH_in_ggg(T105, T106, T107))
pH_in_ggg(T105, T106, T107) → U18_ggg(T105, T106, T107, lessJ_in_gg(T105, T106))
lessJ_in_gg(0, T116) → lessJ_out_gg(0, T116)
lessJ_in_gg(s(T121), T122) → U7_gg(T121, T122, lessI_in_gg(T121, T122))
lessI_in_gg(0, s(T129)) → lessI_out_gg(0, s(T129))
lessI_in_gg(s(T134), s(T135)) → U6_gg(T134, T135, lessI_in_gg(T134, T135))
U6_gg(T134, T135, lessI_out_gg(T134, T135)) → lessI_out_gg(s(T134), s(T135))
U7_gg(T121, T122, lessI_out_gg(T121, T122)) → lessJ_out_gg(s(T121), T122)
U18_ggg(T105, T106, T107, lessJ_out_gg(T105, T106)) → U19_ggg(T105, T106, T107, orderedG_in_gg(T106, T107))
U19_ggg(T105, T106, T107, orderedG_out_gg(T106, T107)) → pH_out_ggg(T105, T106, T107)
U5_gg(T105, T106, T107, pH_out_ggg(T105, T106, T107)) → orderedG_out_gg(T105, .(T106, T107))
U13_ggg(T51, T15, T14, orderedG_out_gg(T14, T15)) → pL_out_ggg(T51, T15, T14)
U11_ggagg(T20, T21, T51, T15, T14, pL_out_ggg(T51, T15, T14)) → pK_out_ggagg(T20, T21, T51, T15, T14)
U9_agagag(T20, T14, T21, T13, X25, T15, pK_out_ggagg(T20, T21, X25, T15, T14)) → pB_out_agagag(T20, T14, T21, T13, X25, T15)
U1_gg(T13, T14, T15, pB_out_agagag(X23, T14, X24, T13, X25, T15)) → ssA_out_gg(T13, .(T14, T15))

(36) UsableRulesProof (EQUIVALENT transformation)

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

(37) Obligation:

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

PF_IN_AGAGAG(T83, T77, T84, T76, X109, T78) → U14_AGAGAG(T83, T77, T84, T76, X109, T78, appC_in_agag(T83, T77, T84, T76))
U14_AGAGAG(T83, T77, T84, T76, X109, T78, appC_out_agag(T83, T77, T84, T76)) → PM_IN_GGAG(T83, T84, X109, T78)
PM_IN_GGAG(T83, T84, T91, T78) → U16_GGAG(T83, T84, T91, T78, appD_in_gga(T83, T84, T91))
U16_GGAG(T83, T84, T91, T78, appD_out_gga(T83, T84, T91)) → PERME_IN_GG(T91, T78)
PERME_IN_GG(T76, .(T77, T78)) → PF_IN_AGAGAG(X107, T77, X108, T76, X109, T78)

The TRS R consists of the following rules:

appC_in_agag([], T34, T35, .(T34, T35)) → appC_out_agag([], T34, T35, .(T34, T35))
appC_in_agag(.(T43, X63), T42, X64, .(T43, T44)) → U2_agag(T43, X63, T42, X64, T44, appC_in_agag(X63, T42, X64, T44))
appD_in_gga([], T58, T58) → appD_out_gga([], T58, T58)
appD_in_gga(.(T65, T66), T67, .(T65, X92)) → U3_gga(T65, T66, T67, X92, appD_in_gga(T66, T67, X92))
U2_agag(T43, X63, T42, X64, T44, appC_out_agag(X63, T42, X64, T44)) → appC_out_agag(.(T43, X63), T42, X64, .(T43, T44))
U3_gga(T65, T66, T67, X92, appD_out_gga(T66, T67, X92)) → appD_out_gga(.(T65, T66), T67, .(T65, X92))

The argument filtering Pi contains the following mapping:
[] = []
.(x1, x2) = .(x1, x2)
appC_in_agag(x1, x2, x3, x4) = appC_in_agag(x2, x4)
appC_out_agag(x1, x2, x3, x4) = appC_out_agag(x1, x2, x3, x4)
U2_agag(x1, x2, x3, x4, x5, x6) = U2_agag(x1, x3, x5, x6)
appD_in_gga(x1, x2, x3) = appD_in_gga(x1, x2)
appD_out_gga(x1, x2, x3) = appD_out_gga(x1, x2, x3)
U3_gga(x1, x2, x3, x4, x5) = U3_gga(x1, x2, x3, x5)
PERME_IN_GG(x1, x2) = PERME_IN_GG(x1, x2)
PF_IN_AGAGAG(x1, x2, x3, x4, x5, x6) = PF_IN_AGAGAG(x2, x4, x6)
U14_AGAGAG(x1, x2, x3, x4, x5, x6, x7) = U14_AGAGAG(x2, x4, x6, x7)
PM_IN_GGAG(x1, x2, x3, x4) = PM_IN_GGAG(x1, x2, x4)
U16_GGAG(x1, x2, x3, x4, x5) = U16_GGAG(x1, x2, x4, x5)

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

(38) PiDPToQDPProof (SOUND transformation)

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

(39) Obligation:

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

PF_IN_AGAGAG(T77, T76, T78) → U14_AGAGAG(T77, T76, T78, appC_in_agag(T77, T76))
U14_AGAGAG(T77, T76, T78, appC_out_agag(T83, T77, T84, T76)) → PM_IN_GGAG(T83, T84, T78)
PM_IN_GGAG(T83, T84, T78) → U16_GGAG(T83, T84, T78, appD_in_gga(T83, T84))
U16_GGAG(T83, T84, T78, appD_out_gga(T83, T84, T91)) → PERME_IN_GG(T91, T78)
PERME_IN_GG(T76, .(T77, T78)) → PF_IN_AGAGAG(T77, T76, T78)

The TRS R consists of the following rules:

appC_in_agag(T34, .(T34, T35)) → appC_out_agag([], T34, T35, .(T34, T35))
appC_in_agag(T42, .(T43, T44)) → U2_agag(T43, T42, T44, appC_in_agag(T42, T44))
appD_in_gga([], T58) → appD_out_gga([], T58, T58)
appD_in_gga(.(T65, T66), T67) → U3_gga(T65, T66, T67, appD_in_gga(T66, T67))
U2_agag(T43, T42, T44, appC_out_agag(X63, T42, X64, T44)) → appC_out_agag(.(T43, X63), T42, X64, .(T43, T44))
U3_gga(T65, T66, T67, appD_out_gga(T66, T67, X92)) → appD_out_gga(.(T65, T66), T67, .(T65, X92))

The set Q consists of the following terms:

appC_in_agag(x0, x1)
appD_in_gga(x0, x1)
U2_agag(x0, x1, x2, x3)
U3_gga(x0, x1, x2, x3)

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

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

U14_AGAGAG(T77, T76, T78, appC_out_agag(T83, T77, T84, T76)) → PM_IN_GGAG(T83, T84, T78)
The graph contains the following edges 4 > 1, 4 > 2, 3 >= 3
PERME_IN_GG(T76, .(T77, T78)) → PF_IN_AGAGAG(T77, T76, T78)
The graph contains the following edges 2 > 1, 1 >= 2, 2 > 3
PM_IN_GGAG(T83, T84, T78) → U16_GGAG(T83, T84, T78, appD_in_gga(T83, T84))
The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 3
PF_IN_AGAGAG(T77, T76, T78) → U14_AGAGAG(T77, T76, T78, appC_in_agag(T77, T76))
The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 3
U16_GGAG(T83, T84, T78, appD_out_gga(T83, T84, T91)) → PERME_IN_GG(T91, T78)
The graph contains the following edges 4 > 1, 3 >= 2

(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) QDPSizeChangeProof (EQUIVALENT transformation)

(27) YES

(28) Obligation:

(29) UsableRulesProof (EQUIVALENT transformation)

(30) Obligation:

(31) PiDPToQDPProof (SOUND transformation)

(32) Obligation:

(33) QDPSizeChangeProof (EQUIVALENT transformation)

(34) YES

(35) Obligation:

(36) UsableRulesProof (EQUIVALENT transformation)

(37) Obligation:

(38) PiDPToQDPProof (SOUND transformation)

(39) Obligation:

(40) QDPSizeChangeProof (EQUIVALENT transformation)

(41) YES