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

(0) Obligation:

Clauses:

p(0, 0).
p(s(X), X).
le(0, Y, true).
le(s(X), 0, false).
le(s(X), s(Y), B) :- le(X, Y, B).
minus(X, Y, Z) :- ','(le(X, Y, B), if(B, X, Y, Z)).
if(true, X, Y, 0).
if(false, X, Y, s(Z)) :- ','(p(X, X1), minus(X1, Y, Z)).

Query: minus(g,a,a)

(1) PrologToPiTRSViaGraphTransformerProof (SOUND transformation)

Transformed Prolog program to (Pi-)TRS.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
2 [label="A: minus(T1, T2, T3)\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
4 [label="4: minus(T1, T2, T3), SCOPE: 1, CLAUSE: 5\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
7 [label="7: ','(le(T7, T10, X8), if(X8, T7, T10, T11))\n\nT7 is ground\nX8 is free", fontsize=16, style=filled, fillcolor=lightyellow];
10 [label="10: ','(le(T7, T10, X8), if(X8, T7, T10, T11)), SCOPE: 2, CLAUSE: 2 | ','(le(T7, T10, X8), if(X8, T7, T10, T11)), SCOPE: 2, CLAUSE: 3 | ','(le(T7, T10, X8), if(X8, T7, T10, T11)), SCOPE: 2, CLAUSE: 4\n\nT7 is ground\nX8 is free", fontsize=16, style=filled, fillcolor=lightyellow];
11 [label="11: ','(le(T7, T10, X8), if(X8, T7, T10, T11)), SCOPE: 2, CLAUSE: 2\n\nT7 is ground\nX8 is free", fontsize=16, style=filled, fillcolor=lightyellow];
13 [label="13: ','(le(T7, T10, X8), if(X8, T7, T10, T11)), SCOPE: 2, CLAUSE: 3 | ','(le(T7, T10, X8), if(X8, T7, T10, T11)), SCOPE: 2, CLAUSE: 4\n\nT7 is ground\nX8 is free", fontsize=16, style=filled, fillcolor=lightyellow];
17 [label="17: if(true, 0, T17, T18)\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
19 [label="19: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
21 [label="21: if(true, 0, T17, T18), SCOPE: 3, CLAUSE: 6 | if(true, 0, T17, T18), SCOPE: 3, CLAUSE: 7\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
25 [label="25: if(true, 0, T17, T18), SCOPE: 3, CLAUSE: 6\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
27 [label="27: if(true, 0, T17, T18), SCOPE: 3, CLAUSE: 7\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
29 [label="29: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
32 [label="32: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
33 [label="33: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
37 [label="37: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
41 [label="41: ','(le(T7, T10, X8), if(X8, T7, T10, T11)), SCOPE: 2, CLAUSE: 3\n\nT7 is ground\nX8 is free", fontsize=16, style=filled, fillcolor=lightyellow];
43 [label="43: ','(le(T7, T10, X8), if(X8, T7, T10, T11)), SCOPE: 2, CLAUSE: 4\n\nT7 is ground\nX8 is free", fontsize=16, style=filled, fillcolor=lightyellow];
45 [label="45: if(false, s(T30), 0, T31)\n\nT30 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
49 [label="49: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
52 [label="52: if(false, s(T30), 0, T31), SCOPE: 4, CLAUSE: 6 | if(false, s(T30), 0, T31), SCOPE: 4, CLAUSE: 7\n\nT30 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
55 [label="55: if(false, s(T30), 0, T31), SCOPE: 4, CLAUSE: 7\n\nT30 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
60 [label="60: ','(p(s(T36), X52), minus(X52, 0, T38))\n\nT36 is ground\nX52 is free", fontsize=16, style=filled, fillcolor=lightyellow];
63 [label="63: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
67 [label="67: ','(p(s(T36), X52), minus(X52, 0, T38)), SCOPE: 5, CLAUSE: 0 | ','(p(s(T36), X52), minus(X52, 0, T38)), SCOPE: 5, CLAUSE: 1\n\nT36 is ground\nX52 is free", fontsize=16, style=filled, fillcolor=lightyellow];
68 [label="68: ','(p(s(T36), X52), minus(X52, 0, T38)), SCOPE: 5, CLAUSE: 1\n\nT36 is ground\nX52 is free", fontsize=16, style=filled, fillcolor=lightyellow];
71 [label="B: minus(T44, 0, T38)\n\nT44 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
73 [label="73: minus(T44, 0, T38), SCOPE: 6, CLAUSE: 5\n\nT44 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
80 [label="F: ','(le(T52, 0, X81), if(X81, T52, 0, T54))\n\nT52 is ground\nX81 is free", fontsize=16, style=filled, fillcolor=lightyellow];
83 [label="H: le(T52, 0, X81)\n\nT52 is ground\nX81 is free", fontsize=16, style=filled, fillcolor=lightyellow];
84 [label="I: if(T55, T52, 0, T54)\n\nT52 is ground\nT55 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
88 [label="88: le(T52, 0, X81), SCOPE: 7, CLAUSE: 2 | le(T52, 0, X81), SCOPE: 7, CLAUSE: 3 | le(T52, 0, X81), SCOPE: 7, CLAUSE: 4\n\nT52 is ground\nX81 is free", fontsize=16, style=filled, fillcolor=lightyellow];
91 [label="91: le(T52, 0, X81), SCOPE: 7, CLAUSE: 2\n\nT52 is ground\nX81 is free", fontsize=16, style=filled, fillcolor=lightyellow];
92 [label="92: le(T52, 0, X81), SCOPE: 7, CLAUSE: 3 | le(T52, 0, X81), SCOPE: 7, CLAUSE: 4\n\nT52 is ground\nX81 is free", fontsize=16, style=filled, fillcolor=lightyellow];
96 [label="96: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
97 [label="97: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
98 [label="98: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
101 [label="101: le(T52, 0, X81), SCOPE: 7, CLAUSE: 3\n\nT52 is ground\nX81 is free", fontsize=16, style=filled, fillcolor=lightyellow];
102 [label="102: le(T52, 0, X81), SCOPE: 7, CLAUSE: 4\n\nT52 is ground\nX81 is free", fontsize=16, style=filled, fillcolor=lightyellow];
106 [label="106: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
107 [label="107: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
109 [label="109: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
110 [label="110: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
112 [label="112: if(T55, T52, 0, T54), SCOPE: 8, CLAUSE: 6 | if(T55, T52, 0, T54), SCOPE: 8, CLAUSE: 7\n\nT52 is ground\nT55 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
115 [label="115: if(T55, T52, 0, T54), SCOPE: 8, CLAUSE: 6\n\nT52 is ground\nT55 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
116 [label="116: if(T55, T52, 0, T54), SCOPE: 8, CLAUSE: 7\n\nT52 is ground\nT55 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
123 [label="123: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
124 [label="124: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
125 [label="125: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
131 [label="131: ','(p(T73, X123), minus(X123, 0, T75))\n\nT73 is ground\nX123 is free", fontsize=16, style=filled, fillcolor=lightyellow];
132 [label="132: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
137 [label="137: ','(p(T73, X123), minus(X123, 0, T75)), SCOPE: 9, CLAUSE: 0 | ','(p(T73, X123), minus(X123, 0, T75)), SCOPE: 9, CLAUSE: 1\n\nT73 is ground\nX123 is free", fontsize=16, style=filled, fillcolor=lightyellow];
139 [label="139: ','(p(T73, X123), minus(X123, 0, T75)), SCOPE: 9, CLAUSE: 0\n\nT73 is ground\nX123 is free", fontsize=16, style=filled, fillcolor=lightyellow];
140 [label="140: ','(p(T73, X123), minus(X123, 0, T75)), SCOPE: 9, CLAUSE: 1\n\nT73 is ground\nX123 is free", fontsize=16, style=filled, fillcolor=lightyellow];
141 [label="D: minus(0, 0, T75)\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
142 [label="142: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
144 [label="144: minus(0, 0, T75), SCOPE: 10, CLAUSE: 5\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
146 [label="E: ','(le(0, 0, X148), if(X148, 0, 0, T82))\n\nX148 is free", fontsize=16, style=filled, fillcolor=lightyellow];
149 [label="J: le(0, 0, X148)\n\nX148 is free", fontsize=16, style=filled, fillcolor=lightyellow];
151 [label="K: if(T83, 0, 0, T82)\n\nT83 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
155 [label="155: le(0, 0, X148), SCOPE: 11, CLAUSE: 2 | le(0, 0, X148), SCOPE: 11, CLAUSE: 3 | le(0, 0, X148), SCOPE: 11, CLAUSE: 4\n\nX148 is free", fontsize=16, style=filled, fillcolor=lightyellow];
158 [label="158: le(0, 0, X148), SCOPE: 11, CLAUSE: 2\n\nX148 is free", fontsize=16, style=filled, fillcolor=lightyellow];
159 [label="159: le(0, 0, X148), SCOPE: 11, CLAUSE: 3 | le(0, 0, X148), SCOPE: 11, CLAUSE: 4\n\nX148 is free", fontsize=16, style=filled, fillcolor=lightyellow];
164 [label="164: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
165 [label="165: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
166 [label="166: le(0, 0, X148), SCOPE: 11, CLAUSE: 4\n\nX148 is free", fontsize=16, style=filled, fillcolor=lightyellow];
167 [label="167: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
174 [label="174: if(T83, 0, 0, T82), SCOPE: 12, CLAUSE: 6 | if(T83, 0, 0, T82), SCOPE: 12, CLAUSE: 7\n\nT83 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
180 [label="180: if(T83, 0, 0, T82), SCOPE: 12, CLAUSE: 6\n\nT83 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
182 [label="182: if(T83, 0, 0, T82), SCOPE: 12, CLAUSE: 7\n\nT83 is ground", 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];
190 [label="190: ','(p(0, X188), minus(X188, 0, T87))\n\nX188 is free", fontsize=16, style=filled, fillcolor=lightyellow];
191 [label="191: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
194 [label="194: ','(p(0, X188), minus(X188, 0, T87)), SCOPE: 13, CLAUSE: 0 | ','(p(0, X188), minus(X188, 0, T87)), SCOPE: 13, CLAUSE: 1\n\nX188 is free", fontsize=16, style=filled, fillcolor=lightyellow];
196 [label="196: ','(p(0, X188), minus(X188, 0, T87)), SCOPE: 13, CLAUSE: 0\n\nX188 is free", fontsize=16, style=filled, fillcolor=lightyellow];
197 [label="197: ','(p(0, X188), minus(X188, 0, T87)), SCOPE: 13, CLAUSE: 1\n\nX188 is free", fontsize=16, style=filled, fillcolor=lightyellow];
198 [label="198: minus(0, 0, T87)\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
202 [label="202: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
203 [label="203: minus(T94, 0, T75)\n\nT94 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
204 [label="204: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
213 [label="C: ','(le(T101, T103, X225), if(X225, s(T101), s(T103), T104))\n\nT101 is ground\nX225 is free", fontsize=16, style=filled, fillcolor=lightyellow];
214 [label="214: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
218 [label="G: le(T101, T103, X225)\n\nT101 is ground\nX225 is free", fontsize=16, style=filled, fillcolor=lightyellow];
219 [label="L: if(T107, s(T101), s(T108), T109)\n\nT101 is ground\nT107 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
223 [label="223: le(T101, T103, X225), SCOPE: 14, CLAUSE: 2 | le(T101, T103, X225), SCOPE: 14, CLAUSE: 3 | le(T101, T103, X225), SCOPE: 14, CLAUSE: 4\n\nT101 is ground\nX225 is free", fontsize=16, style=filled, fillcolor=lightyellow];
226 [label="226: le(T101, T103, X225), SCOPE: 14, CLAUSE: 2\n\nT101 is ground\nX225 is free", fontsize=16, style=filled, fillcolor=lightyellow];
227 [label="227: le(T101, T103, X225), SCOPE: 14, CLAUSE: 3 | le(T101, T103, X225), SCOPE: 14, CLAUSE: 4\n\nT101 is ground\nX225 is free", fontsize=16, style=filled, fillcolor=lightyellow];
232 [label="232: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
233 [label="233: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
235 [label="235: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
239 [label="239: le(T101, T103, X225), SCOPE: 14, CLAUSE: 3\n\nT101 is ground\nX225 is free", fontsize=16, style=filled, fillcolor=lightyellow];
240 [label="240: le(T101, T103, X225), SCOPE: 14, CLAUSE: 4\n\nT101 is ground\nX225 is free", fontsize=16, style=filled, fillcolor=lightyellow];
243 [label="243: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
244 [label="244: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
245 [label="245: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
250 [label="250: le(T126, T128, X251)\n\nT126 is ground\nX251 is free", fontsize=16, style=filled, fillcolor=lightyellow];
251 [label="251: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
255 [label="255: if(T107, s(T101), s(T108), T109), SCOPE: 15, CLAUSE: 6 | if(T107, s(T101), s(T108), T109), SCOPE: 15, CLAUSE: 7\n\nT101 is ground\nT107 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
260 [label="260: if(T107, s(T101), s(T108), T109), SCOPE: 15, CLAUSE: 6\n\nT101 is ground\nT107 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
261 [label="261: if(T107, s(T101), s(T108), T109), SCOPE: 15, CLAUSE: 7\n\nT101 is ground\nT107 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
263 [label="263: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
264 [label="264: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
265 [label="265: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
270 [label="270: ','(p(s(T151), X278), minus(X278, s(T155), T154))\n\nT151 is ground\nX278 is free", fontsize=16, style=filled, fillcolor=lightyellow];
271 [label="271: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
273 [label="273: ','(p(s(T151), X278), minus(X278, s(T155), T154)), SCOPE: 16, CLAUSE: 0 | ','(p(s(T151), X278), minus(X278, s(T155), T154)), SCOPE: 16, CLAUSE: 1\n\nT151 is ground\nX278 is free", fontsize=16, style=filled, fillcolor=lightyellow];
274 [label="274: ','(p(s(T151), X278), minus(X278, s(T155), T154)), SCOPE: 16, CLAUSE: 1\n\nT151 is ground\nX278 is free", fontsize=16, style=filled, fillcolor=lightyellow];
275 [label="275: minus(T163, s(T155), T154)\n\nT163 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
276 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
2 -> 276 [arrowhead = none ];
276 -> 4;

277 [label="ONLY EVAL with clause\nminus(X5, X6, X7) :- ','(le(X5, X6, X8), if(X8, X5, X6, X7)).\nand substitutionT1 -> T7,\nX5 -> T7,\nT2 -> T10,\nX6 -> T10,\nT3 -> T11,\nX7 -> T11,\nT8 -> T10,\nT9 -> T11", fontsize=14, style = filled, fillcolor = lightblue];
4 -> 277 [arrowhead = none ];
277 -> 7;

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

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

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

281 [label="EVAL with clause\nle(0, X13, true).\nand substitutionT7 -> 0,\nT10 -> T17,\nX13 -> T17,\nX8 -> true,\nT16 -> T17,\nT11 -> T18", fontsize=14, style = filled, fillcolor = lightblue];
11 -> 281 [arrowhead = none ];
281 -> 17;

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

283 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
13 -> 283 [arrowhead = none ];
283 -> 41;

284 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
13 -> 284 [arrowhead = none ];
284 -> 43;

285 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
17 -> 285 [arrowhead = none ];
285 -> 21;

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

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

288 [label="EVAL with clause\nif(true, X26, X27, 0).\nand substitutionX26 -> 0,\nT17 -> T25,\nX27 -> T25,\nT18 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
25 -> 288 [arrowhead = none ];
288 -> 29;

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

290 [label="BACKTRACK\nfor clause: if(false, X, Y, s(Z)) :- ','(p(X, X1), minus(X1, Y, Z))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
27 -> 290 [arrowhead = none ];
290 -> 37;

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

292 [label="EVAL with clause\nle(s(X35), 0, false).\nand substitutionX35 -> T30,\nT7 -> s(T30),\nT10 -> 0,\nX8 -> false,\nT11 -> T31", fontsize=14, style = filled, fillcolor = lightblue];
41 -> 292 [arrowhead = none ];
292 -> 45;

293 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
41 -> 293 [arrowhead = none ];
293 -> 49;

294 [label="EVAL with clause\nle(s(X222), s(X223), X224) :- le(X222, X223, X224).\nand substitutionX222 -> T101,\nT7 -> s(T101),\nX223 -> T103,\nT10 -> s(T103),\nX8 -> X225,\nX224 -> X225,\nT102 -> T103,\nT11 -> T104", fontsize=14, style = filled, fillcolor = lightblue];
43 -> 294 [arrowhead = none ];
294 -> 213;

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

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

297 [label="BACKTRACK\nfor clause: if(true, X, Y, 0)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
52 -> 297 [arrowhead = none ];
297 -> 55;

298 [label="EVAL with clause\nif(false, X49, X50, s(X51)) :- ','(p(X49, X52), minus(X52, X50, X51)).\nand substitutionT30 -> T36,\nX49 -> s(T36),\nX50 -> 0,\nX51 -> T38,\nT31 -> s(T38),\nT37 -> T38", fontsize=14, style = filled, fillcolor = lightblue];
55 -> 298 [arrowhead = none ];
298 -> 60;

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

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

301 [label="BACKTRACK\nfor clause: p(0, 0)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
67 -> 301 [arrowhead = none ];
301 -> 68;

302 [label="ONLY EVAL with clause\np(s(X64), X64).\nand substitutionT36 -> T44,\nX64 -> T44,\nX52 -> T44", fontsize=14, style = filled, fillcolor = lightblue];
68 -> 302 [arrowhead = none ];
302 -> 71;

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

304 [label="ONLY EVAL with clause\nminus(X78, X79, X80) :- ','(le(X78, X79, X81), if(X81, X78, X79, X80)).\nand substitutionT44 -> T52,\nX78 -> T52,\nX79 -> 0,\nT38 -> T54,\nX80 -> T54,\nT53 -> T54", fontsize=14, style = filled, fillcolor = lightblue];
73 -> 304 [arrowhead = none ];
304 -> 80;

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

306 [label="SPLIT 2\nnew knowledge:\nT52 is ground\nT55 is ground\nreplacements:X81 -> T55", fontsize=14, style = filled, fillcolor = violet];
80 -> 306 [arrowhead = none ];
306 -> 84;

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

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

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

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

311 [label="EVAL with clause\nle(0, X90, true).\nand substitutionT52 -> 0,\nX90 -> 0,\nX81 -> true", fontsize=14, style = filled, fillcolor = lightblue];
91 -> 311 [arrowhead = none ];
311 -> 96;

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

313 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
92 -> 313 [arrowhead = none ];
313 -> 101;

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

315 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
96 -> 315 [arrowhead = none ];
315 -> 98;

316 [label="EVAL with clause\nle(s(X95), 0, false).\nand substitutionX95 -> T60,\nT52 -> s(T60),\nX81 -> false", fontsize=14, style = filled, fillcolor = lightblue];
101 -> 316 [arrowhead = none ];
316 -> 106;

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

318 [label="BACKTRACK\nfor clause: le(s(X), s(Y), B) :- le(X, Y, B)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
102 -> 318 [arrowhead = none ];
318 -> 110;

319 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
106 -> 319 [arrowhead = none ];
319 -> 109;

320 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
112 -> 320 [arrowhead = none ];
320 -> 115;

321 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
112 -> 321 [arrowhead = none ];
321 -> 116;

322 [label="EVAL with clause\nif(true, X111, X112, 0).\nand substitutionT55 -> true,\nT52 -> T68,\nX111 -> T68,\nX112 -> 0,\nT54 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
115 -> 322 [arrowhead = none ];
322 -> 123;

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

324 [label="EVAL with clause\nif(false, X120, X121, s(X122)) :- ','(p(X120, X123), minus(X123, X121, X122)).\nand substitutionT55 -> false,\nT52 -> T73,\nX120 -> T73,\nX121 -> 0,\nX122 -> T75,\nT54 -> s(T75),\nT74 -> T75", fontsize=14, style = filled, fillcolor = lightblue];
116 -> 324 [arrowhead = none ];
324 -> 131;

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

326 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
123 -> 326 [arrowhead = none ];
326 -> 125;

327 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
131 -> 327 [arrowhead = none ];
327 -> 137;

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

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

330 [label="EVAL with clause\np(0, 0).\nand substitutionT73 -> 0,\nX123 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
139 -> 330 [arrowhead = none ];
330 -> 141;

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

332 [label="EVAL with clause\np(s(X209), X209).\nand substitutionX209 -> T94,\nT73 -> s(T94),\nX123 -> T94", fontsize=14, style = filled, fillcolor = lightblue];
140 -> 332 [arrowhead = none ];
332 -> 203;

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

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

335 [label="ONLY EVAL with clause\nminus(X145, X146, X147) :- ','(le(X145, X146, X148), if(X148, X145, X146, X147)).\nand substitutionX145 -> 0,\nX146 -> 0,\nT75 -> T82,\nX147 -> T82,\nT81 -> T82", fontsize=14, style = filled, fillcolor = lightblue];
144 -> 335 [arrowhead = none ];
335 -> 146;

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

337 [label="SPLIT 2\nnew knowledge:\nT83 is ground\nreplacements:X148 -> T83", fontsize=14, style = filled, fillcolor = violet];
146 -> 337 [arrowhead = none ];
337 -> 151;

338 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
149 -> 338 [arrowhead = none ];
338 -> 155;

339 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
151 -> 339 [arrowhead = none ];
339 -> 174;

340 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
155 -> 340 [arrowhead = none ];
340 -> 158;

341 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
155 -> 341 [arrowhead = none ];
341 -> 159;

342 [label="ONLY EVAL with clause\nle(0, X159, true).\nand substitutionX159 -> 0,\nX148 -> true", fontsize=14, style = filled, fillcolor = lightblue];
158 -> 342 [arrowhead = none ];
342 -> 164;

343 [label="BACKTRACK\nfor clause: le(s(X), 0, false)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
159 -> 343 [arrowhead = none ];
343 -> 166;

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

345 [label="BACKTRACK\nfor clause: le(s(X), s(Y), B) :- le(X, Y, B)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
166 -> 345 [arrowhead = none ];
345 -> 167;

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

347 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
174 -> 347 [arrowhead = none ];
347 -> 182;

348 [label="EVAL with clause\nif(true, X176, X177, 0).\nand substitutionT83 -> true,\nX176 -> 0,\nX177 -> 0,\nT82 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
180 -> 348 [arrowhead = none ];
348 -> 184;

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

350 [label="EVAL with clause\nif(false, X185, X186, s(X187)) :- ','(p(X185, X188), minus(X188, X186, X187)).\nand substitutionT83 -> false,\nX185 -> 0,\nX186 -> 0,\nX187 -> T87,\nT82 -> s(T87),\nT86 -> T87", fontsize=14, style = filled, fillcolor = lightblue];
182 -> 350 [arrowhead = none ];
350 -> 190;

351 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
182 -> 351 [arrowhead = none ];
351 -> 191;

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

353 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
190 -> 353 [arrowhead = none ];
353 -> 194;

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

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

356 [label="ONLY EVAL with clause\np(0, 0).\nand substitutionX188 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
196 -> 356 [arrowhead = none ];
356 -> 198;

357 [label="BACKTRACK\nfor clause: p(s(X), X)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
197 -> 357 [arrowhead = none ];
357 -> 202;

358 [label="INSTANCE with matching:\nT75 -> T87", fontsize=14, style = filled, fillcolor = lightgrey];
198 -> 358 [arrowhead = none , style=dashed];
358 -> 141[style=dashed];

359 [label="INSTANCE with matching:\nT44 -> T94\nT38 -> T75", fontsize=14, style = filled, fillcolor = lightgrey];
203 -> 359 [arrowhead = none , style=dashed];
359 -> 71[style=dashed];

360 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
213 -> 360 [arrowhead = none ];
360 -> 218;

361 [label="SPLIT 2\nnew knowledge:\nT101 is ground\nT107 is ground\nreplacements:X225 -> T107,\nT103 -> T108,\nT104 -> T109", fontsize=14, style = filled, fillcolor = violet];
213 -> 361 [arrowhead = none ];
361 -> 219;

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

363 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
219 -> 363 [arrowhead = none ];
363 -> 255;

364 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
223 -> 364 [arrowhead = none ];
364 -> 226;

365 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
223 -> 365 [arrowhead = none ];
365 -> 227;

366 [label="EVAL with clause\nle(0, X234, true).\nand substitutionT101 -> 0,\nT103 -> T116,\nX234 -> T116,\nX225 -> true", fontsize=14, style = filled, fillcolor = lightblue];
226 -> 366 [arrowhead = none ];
366 -> 232;

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

368 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
227 -> 368 [arrowhead = none ];
368 -> 239;

369 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
227 -> 369 [arrowhead = none ];
369 -> 240;

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

371 [label="EVAL with clause\nle(s(X239), 0, false).\nand substitutionX239 -> T121,\nT101 -> s(T121),\nT103 -> 0,\nX225 -> false", fontsize=14, style = filled, fillcolor = lightblue];
239 -> 371 [arrowhead = none ];
371 -> 243;

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

373 [label="EVAL with clause\nle(s(X248), s(X249), X250) :- le(X248, X249, X250).\nand substitutionX248 -> T126,\nT101 -> s(T126),\nX249 -> T128,\nT103 -> s(T128),\nX225 -> X251,\nX250 -> X251,\nT127 -> T128", fontsize=14, style = filled, fillcolor = lightblue];
240 -> 373 [arrowhead = none ];
373 -> 250;

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

375 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
243 -> 375 [arrowhead = none ];
375 -> 245;

376 [label="INSTANCE with matching:\nT101 -> T126\nT103 -> T128\nX225 -> X251", fontsize=14, style = filled, fillcolor = lightgrey];
250 -> 376 [arrowhead = none , style=dashed];
376 -> 218[style=dashed];

377 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
255 -> 377 [arrowhead = none ];
377 -> 260;

378 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
255 -> 378 [arrowhead = none ];
378 -> 261;

379 [label="EVAL with clause\nif(true, X266, X267, 0).\nand substitutionT107 -> true,\nT101 -> T143,\nX266 -> s(T143),\nT108 -> T144,\nX267 -> s(T144),\nT109 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
260 -> 379 [arrowhead = none ];
379 -> 263;

380 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
260 -> 380 [arrowhead = none ];
380 -> 264;

381 [label="EVAL with clause\nif(false, X275, X276, s(X277)) :- ','(p(X275, X278), minus(X278, X276, X277)).\nand substitutionT107 -> false,\nT101 -> T151,\nX275 -> s(T151),\nT108 -> T155,\nX276 -> s(T155),\nX277 -> T154,\nT109 -> s(T154),\nT153 -> T154,\nT152 -> T155", fontsize=14, style = filled, fillcolor = lightblue];
261 -> 381 [arrowhead = none ];
381 -> 270;

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

383 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
263 -> 383 [arrowhead = none ];
383 -> 265;

384 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
270 -> 384 [arrowhead = none ];
384 -> 273;

385 [label="BACKTRACK\nfor clause: p(0, 0)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
273 -> 385 [arrowhead = none ];
385 -> 274;

386 [label="ONLY EVAL with clause\np(s(X290), X290).\nand substitutionT151 -> T163,\nX290 -> T163,\nX278 -> T163", fontsize=14, style = filled, fillcolor = lightblue];
274 -> 386 [arrowhead = none ];
386 -> 275;

387 [label="INSTANCE with matching:\nT1 -> T163\nT2 -> s(T155)\nT3 -> T154", fontsize=14, style = filled, fillcolor = lightgrey];
275 -> 387 [arrowhead = none , style=dashed];
387 -> 2[style=dashed];

}

(2) Obligation:

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

minusA_in_gaa(0, T25, 0) → minusA_out_gaa(0, T25, 0)
minusA_in_gaa(s(T44), 0, s(T38)) → U1_gaa(T44, T38, minusB_in_ga(T44, T38))
minusB_in_ga(T52, T54) → U4_ga(T52, T54, pF_in_gaa(T52, X81, T54))
pF_in_gaa(T52, T55, T54) → U10_gaa(T52, T55, T54, leH_in_ga(T52, T55))
leH_in_ga(0, true) → leH_out_ga(0, true)
leH_in_ga(s(T60), false) → leH_out_ga(s(T60), false)
U10_gaa(T52, T55, T54, leH_out_ga(T52, T55)) → U11_gaa(T52, T55, T54, ifI_in_gga(T55, T52, T54))
ifI_in_gga(true, T68, 0) → ifI_out_gga(true, T68, 0)
ifI_in_gga(false, 0, s(T75)) → U6_gga(T75, minusD_in_a(T75))
minusD_in_a(T82) → U3_a(T82, pE_in_aa(X148, T82))
pE_in_aa(T83, T82) → U12_aa(T83, T82, leJ_in_a(T83))
leJ_in_a(true) → leJ_out_a(true)
U12_aa(T83, T82, leJ_out_a(T83)) → U13_aa(T83, T82, ifK_in_ga(T83, T82))
ifK_in_ga(true, 0) → ifK_out_ga(true, 0)
ifK_in_ga(false, s(T87)) → U8_ga(T87, minusD_in_a(T87))
U8_ga(T87, minusD_out_a(T87)) → ifK_out_ga(false, s(T87))
U13_aa(T83, T82, ifK_out_ga(T83, T82)) → pE_out_aa(T83, T82)
U3_a(T82, pE_out_aa(X148, T82)) → minusD_out_a(T82)
U6_gga(T75, minusD_out_a(T75)) → ifI_out_gga(false, 0, s(T75))
ifI_in_gga(false, s(T94), s(T75)) → U7_gga(T94, T75, minusB_in_ga(T94, T75))
U7_gga(T94, T75, minusB_out_ga(T94, T75)) → ifI_out_gga(false, s(T94), s(T75))
U11_gaa(T52, T55, T54, ifI_out_gga(T55, T52, T54)) → pF_out_gaa(T52, T55, T54)
U4_ga(T52, T54, pF_out_gaa(T52, X81, T54)) → minusB_out_ga(T52, T54)
U1_gaa(T44, T38, minusB_out_ga(T44, T38)) → minusA_out_gaa(s(T44), 0, s(T38))
minusA_in_gaa(s(T101), s(T103), T104) → U2_gaa(T101, T103, T104, pC_in_gaaa(T101, T103, X225, T104))
pC_in_gaaa(T101, T108, T107, T109) → U14_gaaa(T101, T108, T107, T109, leG_in_gaa(T101, T108, T107))
leG_in_gaa(0, T116, true) → leG_out_gaa(0, T116, true)
leG_in_gaa(s(T121), 0, false) → leG_out_gaa(s(T121), 0, false)
leG_in_gaa(s(T126), s(T128), X251) → U5_gaa(T126, T128, X251, leG_in_gaa(T126, T128, X251))
U5_gaa(T126, T128, X251, leG_out_gaa(T126, T128, X251)) → leG_out_gaa(s(T126), s(T128), X251)
U14_gaaa(T101, T108, T107, T109, leG_out_gaa(T101, T108, T107)) → U15_gaaa(T101, T108, T107, T109, ifL_in_ggaa(T107, T101, T108, T109))
ifL_in_ggaa(true, T143, T144, 0) → ifL_out_ggaa(true, T143, T144, 0)
ifL_in_ggaa(false, T163, T155, s(T154)) → U9_ggaa(T163, T155, T154, minusA_in_gaa(T163, s(T155), T154))
U9_ggaa(T163, T155, T154, minusA_out_gaa(T163, s(T155), T154)) → ifL_out_ggaa(false, T163, T155, s(T154))
U15_gaaa(T101, T108, T107, T109, ifL_out_ggaa(T107, T101, T108, T109)) → pC_out_gaaa(T101, T108, T107, T109)
U2_gaa(T101, T103, T104, pC_out_gaaa(T101, T103, X225, T104)) → minusA_out_gaa(s(T101), s(T103), T104)

The argument filtering Pi contains the following mapping:
minusA_in_gaa(x1, x2, x3)  =  minusA_in_gaa(x1)
0  =  0
minusA_out_gaa(x1, x2, x3)  =  minusA_out_gaa(x1, x3)
s(x1)  =  s(x1)
U1_gaa(x1, x2, x3)  =  U1_gaa(x1, x3)
minusB_in_ga(x1, x2)  =  minusB_in_ga(x1)
U4_ga(x1, x2, x3)  =  U4_ga(x1, x3)
pF_in_gaa(x1, x2, x3)  =  pF_in_gaa(x1)
U10_gaa(x1, x2, x3, x4)  =  U10_gaa(x1, x4)
leH_in_ga(x1, x2)  =  leH_in_ga(x1)
leH_out_ga(x1, x2)  =  leH_out_ga(x1, x2)
U11_gaa(x1, x2, x3, x4)  =  U11_gaa(x1, x2, x4)
ifI_in_gga(x1, x2, x3)  =  ifI_in_gga(x1, x2)
true  =  true
ifI_out_gga(x1, x2, x3)  =  ifI_out_gga(x1, x2, x3)
false  =  false
U6_gga(x1, x2)  =  U6_gga(x2)
minusD_in_a(x1)  =  minusD_in_a
U3_a(x1, x2)  =  U3_a(x2)
pE_in_aa(x1, x2)  =  pE_in_aa
U12_aa(x1, x2, x3)  =  U12_aa(x3)
leJ_in_a(x1)  =  leJ_in_a
leJ_out_a(x1)  =  leJ_out_a(x1)
U13_aa(x1, x2, x3)  =  U13_aa(x1, x3)
ifK_in_ga(x1, x2)  =  ifK_in_ga(x1)
ifK_out_ga(x1, x2)  =  ifK_out_ga(x1, x2)
U8_ga(x1, x2)  =  U8_ga(x2)
minusD_out_a(x1)  =  minusD_out_a(x1)
pE_out_aa(x1, x2)  =  pE_out_aa(x1, x2)
U7_gga(x1, x2, x3)  =  U7_gga(x1, x3)
minusB_out_ga(x1, x2)  =  minusB_out_ga(x1, x2)
pF_out_gaa(x1, x2, x3)  =  pF_out_gaa(x1, x2, x3)
U2_gaa(x1, x2, x3, x4)  =  U2_gaa(x1, x4)
pC_in_gaaa(x1, x2, x3, x4)  =  pC_in_gaaa(x1)
U14_gaaa(x1, x2, x3, x4, x5)  =  U14_gaaa(x1, x5)
leG_in_gaa(x1, x2, x3)  =  leG_in_gaa(x1)
leG_out_gaa(x1, x2, x3)  =  leG_out_gaa(x1, x3)
U5_gaa(x1, x2, x3, x4)  =  U5_gaa(x1, x4)
U15_gaaa(x1, x2, x3, x4, x5)  =  U15_gaaa(x1, x3, x5)
ifL_in_ggaa(x1, x2, x3, x4)  =  ifL_in_ggaa(x1, x2)
ifL_out_ggaa(x1, x2, x3, x4)  =  ifL_out_ggaa(x1, x2, x4)
U9_ggaa(x1, x2, x3, x4)  =  U9_ggaa(x1, x4)
pC_out_gaaa(x1, x2, x3, x4)  =  pC_out_gaaa(x1, x3, x4)

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

MINUSA_IN_GAA(s(T44), 0, s(T38)) → U1_GAA(T44, T38, minusB_in_ga(T44, T38))
MINUSA_IN_GAA(s(T44), 0, s(T38)) → MINUSB_IN_GA(T44, T38)
MINUSB_IN_GA(T52, T54) → U4_GA(T52, T54, pF_in_gaa(T52, X81, T54))
MINUSB_IN_GA(T52, T54) → PF_IN_GAA(T52, X81, T54)
PF_IN_GAA(T52, T55, T54) → U10_GAA(T52, T55, T54, leH_in_ga(T52, T55))
PF_IN_GAA(T52, T55, T54) → LEH_IN_GA(T52, T55)
U10_GAA(T52, T55, T54, leH_out_ga(T52, T55)) → U11_GAA(T52, T55, T54, ifI_in_gga(T55, T52, T54))
U10_GAA(T52, T55, T54, leH_out_ga(T52, T55)) → IFI_IN_GGA(T55, T52, T54)
IFI_IN_GGA(false, 0, s(T75)) → U6_GGA(T75, minusD_in_a(T75))
IFI_IN_GGA(false, 0, s(T75)) → MINUSD_IN_A(T75)
MINUSD_IN_A(T82) → U3_A(T82, pE_in_aa(X148, T82))
MINUSD_IN_A(T82) → PE_IN_AA(X148, T82)
PE_IN_AA(T83, T82) → U12_AA(T83, T82, leJ_in_a(T83))
PE_IN_AA(T83, T82) → LEJ_IN_A(T83)
U12_AA(T83, T82, leJ_out_a(T83)) → U13_AA(T83, T82, ifK_in_ga(T83, T82))
U12_AA(T83, T82, leJ_out_a(T83)) → IFK_IN_GA(T83, T82)
IFK_IN_GA(false, s(T87)) → U8_GA(T87, minusD_in_a(T87))
IFK_IN_GA(false, s(T87)) → MINUSD_IN_A(T87)
IFI_IN_GGA(false, s(T94), s(T75)) → U7_GGA(T94, T75, minusB_in_ga(T94, T75))
IFI_IN_GGA(false, s(T94), s(T75)) → MINUSB_IN_GA(T94, T75)
MINUSA_IN_GAA(s(T101), s(T103), T104) → U2_GAA(T101, T103, T104, pC_in_gaaa(T101, T103, X225, T104))
MINUSA_IN_GAA(s(T101), s(T103), T104) → PC_IN_GAAA(T101, T103, X225, T104)
PC_IN_GAAA(T101, T108, T107, T109) → U14_GAAA(T101, T108, T107, T109, leG_in_gaa(T101, T108, T107))
PC_IN_GAAA(T101, T108, T107, T109) → LEG_IN_GAA(T101, T108, T107)
LEG_IN_GAA(s(T126), s(T128), X251) → U5_GAA(T126, T128, X251, leG_in_gaa(T126, T128, X251))
LEG_IN_GAA(s(T126), s(T128), X251) → LEG_IN_GAA(T126, T128, X251)
U14_GAAA(T101, T108, T107, T109, leG_out_gaa(T101, T108, T107)) → U15_GAAA(T101, T108, T107, T109, ifL_in_ggaa(T107, T101, T108, T109))
U14_GAAA(T101, T108, T107, T109, leG_out_gaa(T101, T108, T107)) → IFL_IN_GGAA(T107, T101, T108, T109)
IFL_IN_GGAA(false, T163, T155, s(T154)) → U9_GGAA(T163, T155, T154, minusA_in_gaa(T163, s(T155), T154))
IFL_IN_GGAA(false, T163, T155, s(T154)) → MINUSA_IN_GAA(T163, s(T155), T154)

The TRS R consists of the following rules:

minusA_in_gaa(0, T25, 0) → minusA_out_gaa(0, T25, 0)
minusA_in_gaa(s(T44), 0, s(T38)) → U1_gaa(T44, T38, minusB_in_ga(T44, T38))
minusB_in_ga(T52, T54) → U4_ga(T52, T54, pF_in_gaa(T52, X81, T54))
pF_in_gaa(T52, T55, T54) → U10_gaa(T52, T55, T54, leH_in_ga(T52, T55))
leH_in_ga(0, true) → leH_out_ga(0, true)
leH_in_ga(s(T60), false) → leH_out_ga(s(T60), false)
U10_gaa(T52, T55, T54, leH_out_ga(T52, T55)) → U11_gaa(T52, T55, T54, ifI_in_gga(T55, T52, T54))
ifI_in_gga(true, T68, 0) → ifI_out_gga(true, T68, 0)
ifI_in_gga(false, 0, s(T75)) → U6_gga(T75, minusD_in_a(T75))
minusD_in_a(T82) → U3_a(T82, pE_in_aa(X148, T82))
pE_in_aa(T83, T82) → U12_aa(T83, T82, leJ_in_a(T83))
leJ_in_a(true) → leJ_out_a(true)
U12_aa(T83, T82, leJ_out_a(T83)) → U13_aa(T83, T82, ifK_in_ga(T83, T82))
ifK_in_ga(true, 0) → ifK_out_ga(true, 0)
ifK_in_ga(false, s(T87)) → U8_ga(T87, minusD_in_a(T87))
U8_ga(T87, minusD_out_a(T87)) → ifK_out_ga(false, s(T87))
U13_aa(T83, T82, ifK_out_ga(T83, T82)) → pE_out_aa(T83, T82)
U3_a(T82, pE_out_aa(X148, T82)) → minusD_out_a(T82)
U6_gga(T75, minusD_out_a(T75)) → ifI_out_gga(false, 0, s(T75))
ifI_in_gga(false, s(T94), s(T75)) → U7_gga(T94, T75, minusB_in_ga(T94, T75))
U7_gga(T94, T75, minusB_out_ga(T94, T75)) → ifI_out_gga(false, s(T94), s(T75))
U11_gaa(T52, T55, T54, ifI_out_gga(T55, T52, T54)) → pF_out_gaa(T52, T55, T54)
U4_ga(T52, T54, pF_out_gaa(T52, X81, T54)) → minusB_out_ga(T52, T54)
U1_gaa(T44, T38, minusB_out_ga(T44, T38)) → minusA_out_gaa(s(T44), 0, s(T38))
minusA_in_gaa(s(T101), s(T103), T104) → U2_gaa(T101, T103, T104, pC_in_gaaa(T101, T103, X225, T104))
pC_in_gaaa(T101, T108, T107, T109) → U14_gaaa(T101, T108, T107, T109, leG_in_gaa(T101, T108, T107))
leG_in_gaa(0, T116, true) → leG_out_gaa(0, T116, true)
leG_in_gaa(s(T121), 0, false) → leG_out_gaa(s(T121), 0, false)
leG_in_gaa(s(T126), s(T128), X251) → U5_gaa(T126, T128, X251, leG_in_gaa(T126, T128, X251))
U5_gaa(T126, T128, X251, leG_out_gaa(T126, T128, X251)) → leG_out_gaa(s(T126), s(T128), X251)
U14_gaaa(T101, T108, T107, T109, leG_out_gaa(T101, T108, T107)) → U15_gaaa(T101, T108, T107, T109, ifL_in_ggaa(T107, T101, T108, T109))
ifL_in_ggaa(true, T143, T144, 0) → ifL_out_ggaa(true, T143, T144, 0)
ifL_in_ggaa(false, T163, T155, s(T154)) → U9_ggaa(T163, T155, T154, minusA_in_gaa(T163, s(T155), T154))
U9_ggaa(T163, T155, T154, minusA_out_gaa(T163, s(T155), T154)) → ifL_out_ggaa(false, T163, T155, s(T154))
U15_gaaa(T101, T108, T107, T109, ifL_out_ggaa(T107, T101, T108, T109)) → pC_out_gaaa(T101, T108, T107, T109)
U2_gaa(T101, T103, T104, pC_out_gaaa(T101, T103, X225, T104)) → minusA_out_gaa(s(T101), s(T103), T104)

The argument filtering Pi contains the following mapping:
minusA_in_gaa(x1, x2, x3)  =  minusA_in_gaa(x1)
0  =  0
minusA_out_gaa(x1, x2, x3)  =  minusA_out_gaa(x1, x3)
s(x1)  =  s(x1)
U1_gaa(x1, x2, x3)  =  U1_gaa(x1, x3)
minusB_in_ga(x1, x2)  =  minusB_in_ga(x1)
U4_ga(x1, x2, x3)  =  U4_ga(x1, x3)
pF_in_gaa(x1, x2, x3)  =  pF_in_gaa(x1)
U10_gaa(x1, x2, x3, x4)  =  U10_gaa(x1, x4)
leH_in_ga(x1, x2)  =  leH_in_ga(x1)
leH_out_ga(x1, x2)  =  leH_out_ga(x1, x2)
U11_gaa(x1, x2, x3, x4)  =  U11_gaa(x1, x2, x4)
ifI_in_gga(x1, x2, x3)  =  ifI_in_gga(x1, x2)
true  =  true
ifI_out_gga(x1, x2, x3)  =  ifI_out_gga(x1, x2, x3)
false  =  false
U6_gga(x1, x2)  =  U6_gga(x2)
minusD_in_a(x1)  =  minusD_in_a
U3_a(x1, x2)  =  U3_a(x2)
pE_in_aa(x1, x2)  =  pE_in_aa
U12_aa(x1, x2, x3)  =  U12_aa(x3)
leJ_in_a(x1)  =  leJ_in_a
leJ_out_a(x1)  =  leJ_out_a(x1)
U13_aa(x1, x2, x3)  =  U13_aa(x1, x3)
ifK_in_ga(x1, x2)  =  ifK_in_ga(x1)
ifK_out_ga(x1, x2)  =  ifK_out_ga(x1, x2)
U8_ga(x1, x2)  =  U8_ga(x2)
minusD_out_a(x1)  =  minusD_out_a(x1)
pE_out_aa(x1, x2)  =  pE_out_aa(x1, x2)
U7_gga(x1, x2, x3)  =  U7_gga(x1, x3)
minusB_out_ga(x1, x2)  =  minusB_out_ga(x1, x2)
pF_out_gaa(x1, x2, x3)  =  pF_out_gaa(x1, x2, x3)
U2_gaa(x1, x2, x3, x4)  =  U2_gaa(x1, x4)
pC_in_gaaa(x1, x2, x3, x4)  =  pC_in_gaaa(x1)
U14_gaaa(x1, x2, x3, x4, x5)  =  U14_gaaa(x1, x5)
leG_in_gaa(x1, x2, x3)  =  leG_in_gaa(x1)
leG_out_gaa(x1, x2, x3)  =  leG_out_gaa(x1, x3)
U5_gaa(x1, x2, x3, x4)  =  U5_gaa(x1, x4)
U15_gaaa(x1, x2, x3, x4, x5)  =  U15_gaaa(x1, x3, x5)
ifL_in_ggaa(x1, x2, x3, x4)  =  ifL_in_ggaa(x1, x2)
ifL_out_ggaa(x1, x2, x3, x4)  =  ifL_out_ggaa(x1, x2, x4)
U9_ggaa(x1, x2, x3, x4)  =  U9_ggaa(x1, x4)
pC_out_gaaa(x1, x2, x3, x4)  =  pC_out_gaaa(x1, x3, x4)
MINUSA_IN_GAA(x1, x2, x3)  =  MINUSA_IN_GAA(x1)
U1_GAA(x1, x2, x3)  =  U1_GAA(x1, x3)
MINUSB_IN_GA(x1, x2)  =  MINUSB_IN_GA(x1)
U4_GA(x1, x2, x3)  =  U4_GA(x1, x3)
PF_IN_GAA(x1, x2, x3)  =  PF_IN_GAA(x1)
U10_GAA(x1, x2, x3, x4)  =  U10_GAA(x1, x4)
LEH_IN_GA(x1, x2)  =  LEH_IN_GA(x1)
U11_GAA(x1, x2, x3, x4)  =  U11_GAA(x1, x2, x4)
IFI_IN_GGA(x1, x2, x3)  =  IFI_IN_GGA(x1, x2)
U6_GGA(x1, x2)  =  U6_GGA(x2)
MINUSD_IN_A(x1)  =  MINUSD_IN_A
U3_A(x1, x2)  =  U3_A(x2)
PE_IN_AA(x1, x2)  =  PE_IN_AA
U12_AA(x1, x2, x3)  =  U12_AA(x3)
LEJ_IN_A(x1)  =  LEJ_IN_A
U13_AA(x1, x2, x3)  =  U13_AA(x1, x3)
IFK_IN_GA(x1, x2)  =  IFK_IN_GA(x1)
U8_GA(x1, x2)  =  U8_GA(x2)
U7_GGA(x1, x2, x3)  =  U7_GGA(x1, x3)
U2_GAA(x1, x2, x3, x4)  =  U2_GAA(x1, x4)
PC_IN_GAAA(x1, x2, x3, x4)  =  PC_IN_GAAA(x1)
U14_GAAA(x1, x2, x3, x4, x5)  =  U14_GAAA(x1, x5)
LEG_IN_GAA(x1, x2, x3)  =  LEG_IN_GAA(x1)
U5_GAA(x1, x2, x3, x4)  =  U5_GAA(x1, x4)
U15_GAAA(x1, x2, x3, x4, x5)  =  U15_GAAA(x1, x3, x5)
IFL_IN_GGAA(x1, x2, x3, x4)  =  IFL_IN_GGAA(x1, x2)
U9_GGAA(x1, x2, x3, x4)  =  U9_GGAA(x1, x4)

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

(4) Obligation:

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

MINUSA_IN_GAA(s(T44), 0, s(T38)) → U1_GAA(T44, T38, minusB_in_ga(T44, T38))
MINUSA_IN_GAA(s(T44), 0, s(T38)) → MINUSB_IN_GA(T44, T38)
MINUSB_IN_GA(T52, T54) → U4_GA(T52, T54, pF_in_gaa(T52, X81, T54))
MINUSB_IN_GA(T52, T54) → PF_IN_GAA(T52, X81, T54)
PF_IN_GAA(T52, T55, T54) → U10_GAA(T52, T55, T54, leH_in_ga(T52, T55))
PF_IN_GAA(T52, T55, T54) → LEH_IN_GA(T52, T55)
U10_GAA(T52, T55, T54, leH_out_ga(T52, T55)) → U11_GAA(T52, T55, T54, ifI_in_gga(T55, T52, T54))
U10_GAA(T52, T55, T54, leH_out_ga(T52, T55)) → IFI_IN_GGA(T55, T52, T54)
IFI_IN_GGA(false, 0, s(T75)) → U6_GGA(T75, minusD_in_a(T75))
IFI_IN_GGA(false, 0, s(T75)) → MINUSD_IN_A(T75)
MINUSD_IN_A(T82) → U3_A(T82, pE_in_aa(X148, T82))
MINUSD_IN_A(T82) → PE_IN_AA(X148, T82)
PE_IN_AA(T83, T82) → U12_AA(T83, T82, leJ_in_a(T83))
PE_IN_AA(T83, T82) → LEJ_IN_A(T83)
U12_AA(T83, T82, leJ_out_a(T83)) → U13_AA(T83, T82, ifK_in_ga(T83, T82))
U12_AA(T83, T82, leJ_out_a(T83)) → IFK_IN_GA(T83, T82)
IFK_IN_GA(false, s(T87)) → U8_GA(T87, minusD_in_a(T87))
IFK_IN_GA(false, s(T87)) → MINUSD_IN_A(T87)
IFI_IN_GGA(false, s(T94), s(T75)) → U7_GGA(T94, T75, minusB_in_ga(T94, T75))
IFI_IN_GGA(false, s(T94), s(T75)) → MINUSB_IN_GA(T94, T75)
MINUSA_IN_GAA(s(T101), s(T103), T104) → U2_GAA(T101, T103, T104, pC_in_gaaa(T101, T103, X225, T104))
MINUSA_IN_GAA(s(T101), s(T103), T104) → PC_IN_GAAA(T101, T103, X225, T104)
PC_IN_GAAA(T101, T108, T107, T109) → U14_GAAA(T101, T108, T107, T109, leG_in_gaa(T101, T108, T107))
PC_IN_GAAA(T101, T108, T107, T109) → LEG_IN_GAA(T101, T108, T107)
LEG_IN_GAA(s(T126), s(T128), X251) → U5_GAA(T126, T128, X251, leG_in_gaa(T126, T128, X251))
LEG_IN_GAA(s(T126), s(T128), X251) → LEG_IN_GAA(T126, T128, X251)
U14_GAAA(T101, T108, T107, T109, leG_out_gaa(T101, T108, T107)) → U15_GAAA(T101, T108, T107, T109, ifL_in_ggaa(T107, T101, T108, T109))
U14_GAAA(T101, T108, T107, T109, leG_out_gaa(T101, T108, T107)) → IFL_IN_GGAA(T107, T101, T108, T109)
IFL_IN_GGAA(false, T163, T155, s(T154)) → U9_GGAA(T163, T155, T154, minusA_in_gaa(T163, s(T155), T154))
IFL_IN_GGAA(false, T163, T155, s(T154)) → MINUSA_IN_GAA(T163, s(T155), T154)

The TRS R consists of the following rules:

minusA_in_gaa(0, T25, 0) → minusA_out_gaa(0, T25, 0)
minusA_in_gaa(s(T44), 0, s(T38)) → U1_gaa(T44, T38, minusB_in_ga(T44, T38))
minusB_in_ga(T52, T54) → U4_ga(T52, T54, pF_in_gaa(T52, X81, T54))
pF_in_gaa(T52, T55, T54) → U10_gaa(T52, T55, T54, leH_in_ga(T52, T55))
leH_in_ga(0, true) → leH_out_ga(0, true)
leH_in_ga(s(T60), false) → leH_out_ga(s(T60), false)
U10_gaa(T52, T55, T54, leH_out_ga(T52, T55)) → U11_gaa(T52, T55, T54, ifI_in_gga(T55, T52, T54))
ifI_in_gga(true, T68, 0) → ifI_out_gga(true, T68, 0)
ifI_in_gga(false, 0, s(T75)) → U6_gga(T75, minusD_in_a(T75))
minusD_in_a(T82) → U3_a(T82, pE_in_aa(X148, T82))
pE_in_aa(T83, T82) → U12_aa(T83, T82, leJ_in_a(T83))
leJ_in_a(true) → leJ_out_a(true)
U12_aa(T83, T82, leJ_out_a(T83)) → U13_aa(T83, T82, ifK_in_ga(T83, T82))
ifK_in_ga(true, 0) → ifK_out_ga(true, 0)
ifK_in_ga(false, s(T87)) → U8_ga(T87, minusD_in_a(T87))
U8_ga(T87, minusD_out_a(T87)) → ifK_out_ga(false, s(T87))
U13_aa(T83, T82, ifK_out_ga(T83, T82)) → pE_out_aa(T83, T82)
U3_a(T82, pE_out_aa(X148, T82)) → minusD_out_a(T82)
U6_gga(T75, minusD_out_a(T75)) → ifI_out_gga(false, 0, s(T75))
ifI_in_gga(false, s(T94), s(T75)) → U7_gga(T94, T75, minusB_in_ga(T94, T75))
U7_gga(T94, T75, minusB_out_ga(T94, T75)) → ifI_out_gga(false, s(T94), s(T75))
U11_gaa(T52, T55, T54, ifI_out_gga(T55, T52, T54)) → pF_out_gaa(T52, T55, T54)
U4_ga(T52, T54, pF_out_gaa(T52, X81, T54)) → minusB_out_ga(T52, T54)
U1_gaa(T44, T38, minusB_out_ga(T44, T38)) → minusA_out_gaa(s(T44), 0, s(T38))
minusA_in_gaa(s(T101), s(T103), T104) → U2_gaa(T101, T103, T104, pC_in_gaaa(T101, T103, X225, T104))
pC_in_gaaa(T101, T108, T107, T109) → U14_gaaa(T101, T108, T107, T109, leG_in_gaa(T101, T108, T107))
leG_in_gaa(0, T116, true) → leG_out_gaa(0, T116, true)
leG_in_gaa(s(T121), 0, false) → leG_out_gaa(s(T121), 0, false)
leG_in_gaa(s(T126), s(T128), X251) → U5_gaa(T126, T128, X251, leG_in_gaa(T126, T128, X251))
U5_gaa(T126, T128, X251, leG_out_gaa(T126, T128, X251)) → leG_out_gaa(s(T126), s(T128), X251)
U14_gaaa(T101, T108, T107, T109, leG_out_gaa(T101, T108, T107)) → U15_gaaa(T101, T108, T107, T109, ifL_in_ggaa(T107, T101, T108, T109))
ifL_in_ggaa(true, T143, T144, 0) → ifL_out_ggaa(true, T143, T144, 0)
ifL_in_ggaa(false, T163, T155, s(T154)) → U9_ggaa(T163, T155, T154, minusA_in_gaa(T163, s(T155), T154))
U9_ggaa(T163, T155, T154, minusA_out_gaa(T163, s(T155), T154)) → ifL_out_ggaa(false, T163, T155, s(T154))
U15_gaaa(T101, T108, T107, T109, ifL_out_ggaa(T107, T101, T108, T109)) → pC_out_gaaa(T101, T108, T107, T109)
U2_gaa(T101, T103, T104, pC_out_gaaa(T101, T103, X225, T104)) → minusA_out_gaa(s(T101), s(T103), T104)

The argument filtering Pi contains the following mapping:
minusA_in_gaa(x1, x2, x3)  =  minusA_in_gaa(x1)
0  =  0
minusA_out_gaa(x1, x2, x3)  =  minusA_out_gaa(x1, x3)
s(x1)  =  s(x1)
U1_gaa(x1, x2, x3)  =  U1_gaa(x1, x3)
minusB_in_ga(x1, x2)  =  minusB_in_ga(x1)
U4_ga(x1, x2, x3)  =  U4_ga(x1, x3)
pF_in_gaa(x1, x2, x3)  =  pF_in_gaa(x1)
U10_gaa(x1, x2, x3, x4)  =  U10_gaa(x1, x4)
leH_in_ga(x1, x2)  =  leH_in_ga(x1)
leH_out_ga(x1, x2)  =  leH_out_ga(x1, x2)
U11_gaa(x1, x2, x3, x4)  =  U11_gaa(x1, x2, x4)
ifI_in_gga(x1, x2, x3)  =  ifI_in_gga(x1, x2)
true  =  true
ifI_out_gga(x1, x2, x3)  =  ifI_out_gga(x1, x2, x3)
false  =  false
U6_gga(x1, x2)  =  U6_gga(x2)
minusD_in_a(x1)  =  minusD_in_a
U3_a(x1, x2)  =  U3_a(x2)
pE_in_aa(x1, x2)  =  pE_in_aa
U12_aa(x1, x2, x3)  =  U12_aa(x3)
leJ_in_a(x1)  =  leJ_in_a
leJ_out_a(x1)  =  leJ_out_a(x1)
U13_aa(x1, x2, x3)  =  U13_aa(x1, x3)
ifK_in_ga(x1, x2)  =  ifK_in_ga(x1)
ifK_out_ga(x1, x2)  =  ifK_out_ga(x1, x2)
U8_ga(x1, x2)  =  U8_ga(x2)
minusD_out_a(x1)  =  minusD_out_a(x1)
pE_out_aa(x1, x2)  =  pE_out_aa(x1, x2)
U7_gga(x1, x2, x3)  =  U7_gga(x1, x3)
minusB_out_ga(x1, x2)  =  minusB_out_ga(x1, x2)
pF_out_gaa(x1, x2, x3)  =  pF_out_gaa(x1, x2, x3)
U2_gaa(x1, x2, x3, x4)  =  U2_gaa(x1, x4)
pC_in_gaaa(x1, x2, x3, x4)  =  pC_in_gaaa(x1)
U14_gaaa(x1, x2, x3, x4, x5)  =  U14_gaaa(x1, x5)
leG_in_gaa(x1, x2, x3)  =  leG_in_gaa(x1)
leG_out_gaa(x1, x2, x3)  =  leG_out_gaa(x1, x3)
U5_gaa(x1, x2, x3, x4)  =  U5_gaa(x1, x4)
U15_gaaa(x1, x2, x3, x4, x5)  =  U15_gaaa(x1, x3, x5)
ifL_in_ggaa(x1, x2, x3, x4)  =  ifL_in_ggaa(x1, x2)
ifL_out_ggaa(x1, x2, x3, x4)  =  ifL_out_ggaa(x1, x2, x4)
U9_ggaa(x1, x2, x3, x4)  =  U9_ggaa(x1, x4)
pC_out_gaaa(x1, x2, x3, x4)  =  pC_out_gaaa(x1, x3, x4)
MINUSA_IN_GAA(x1, x2, x3)  =  MINUSA_IN_GAA(x1)
U1_GAA(x1, x2, x3)  =  U1_GAA(x1, x3)
MINUSB_IN_GA(x1, x2)  =  MINUSB_IN_GA(x1)
U4_GA(x1, x2, x3)  =  U4_GA(x1, x3)
PF_IN_GAA(x1, x2, x3)  =  PF_IN_GAA(x1)
U10_GAA(x1, x2, x3, x4)  =  U10_GAA(x1, x4)
LEH_IN_GA(x1, x2)  =  LEH_IN_GA(x1)
U11_GAA(x1, x2, x3, x4)  =  U11_GAA(x1, x2, x4)
IFI_IN_GGA(x1, x2, x3)  =  IFI_IN_GGA(x1, x2)
U6_GGA(x1, x2)  =  U6_GGA(x2)
MINUSD_IN_A(x1)  =  MINUSD_IN_A
U3_A(x1, x2)  =  U3_A(x2)
PE_IN_AA(x1, x2)  =  PE_IN_AA
U12_AA(x1, x2, x3)  =  U12_AA(x3)
LEJ_IN_A(x1)  =  LEJ_IN_A
U13_AA(x1, x2, x3)  =  U13_AA(x1, x3)
IFK_IN_GA(x1, x2)  =  IFK_IN_GA(x1)
U8_GA(x1, x2)  =  U8_GA(x2)
U7_GGA(x1, x2, x3)  =  U7_GGA(x1, x3)
U2_GAA(x1, x2, x3, x4)  =  U2_GAA(x1, x4)
PC_IN_GAAA(x1, x2, x3, x4)  =  PC_IN_GAAA(x1)
U14_GAAA(x1, x2, x3, x4, x5)  =  U14_GAAA(x1, x5)
LEG_IN_GAA(x1, x2, x3)  =  LEG_IN_GAA(x1)
U5_GAA(x1, x2, x3, x4)  =  U5_GAA(x1, x4)
U15_GAAA(x1, x2, x3, x4, x5)  =  U15_GAAA(x1, x3, x5)
IFL_IN_GGAA(x1, x2, x3, x4)  =  IFL_IN_GGAA(x1, x2)
U9_GGAA(x1, x2, x3, x4)  =  U9_GGAA(x1, x4)

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

(5) DependencyGraphProof (EQUIVALENT transformation)

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

(6) Complex Obligation (AND)

(7) Obligation:

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

LEG_IN_GAA(s(T126), s(T128), X251) → LEG_IN_GAA(T126, T128, X251)

The TRS R consists of the following rules:

minusA_in_gaa(0, T25, 0) → minusA_out_gaa(0, T25, 0)
minusA_in_gaa(s(T44), 0, s(T38)) → U1_gaa(T44, T38, minusB_in_ga(T44, T38))
minusB_in_ga(T52, T54) → U4_ga(T52, T54, pF_in_gaa(T52, X81, T54))
pF_in_gaa(T52, T55, T54) → U10_gaa(T52, T55, T54, leH_in_ga(T52, T55))
leH_in_ga(0, true) → leH_out_ga(0, true)
leH_in_ga(s(T60), false) → leH_out_ga(s(T60), false)
U10_gaa(T52, T55, T54, leH_out_ga(T52, T55)) → U11_gaa(T52, T55, T54, ifI_in_gga(T55, T52, T54))
ifI_in_gga(true, T68, 0) → ifI_out_gga(true, T68, 0)
ifI_in_gga(false, 0, s(T75)) → U6_gga(T75, minusD_in_a(T75))
minusD_in_a(T82) → U3_a(T82, pE_in_aa(X148, T82))
pE_in_aa(T83, T82) → U12_aa(T83, T82, leJ_in_a(T83))
leJ_in_a(true) → leJ_out_a(true)
U12_aa(T83, T82, leJ_out_a(T83)) → U13_aa(T83, T82, ifK_in_ga(T83, T82))
ifK_in_ga(true, 0) → ifK_out_ga(true, 0)
ifK_in_ga(false, s(T87)) → U8_ga(T87, minusD_in_a(T87))
U8_ga(T87, minusD_out_a(T87)) → ifK_out_ga(false, s(T87))
U13_aa(T83, T82, ifK_out_ga(T83, T82)) → pE_out_aa(T83, T82)
U3_a(T82, pE_out_aa(X148, T82)) → minusD_out_a(T82)
U6_gga(T75, minusD_out_a(T75)) → ifI_out_gga(false, 0, s(T75))
ifI_in_gga(false, s(T94), s(T75)) → U7_gga(T94, T75, minusB_in_ga(T94, T75))
U7_gga(T94, T75, minusB_out_ga(T94, T75)) → ifI_out_gga(false, s(T94), s(T75))
U11_gaa(T52, T55, T54, ifI_out_gga(T55, T52, T54)) → pF_out_gaa(T52, T55, T54)
U4_ga(T52, T54, pF_out_gaa(T52, X81, T54)) → minusB_out_ga(T52, T54)
U1_gaa(T44, T38, minusB_out_ga(T44, T38)) → minusA_out_gaa(s(T44), 0, s(T38))
minusA_in_gaa(s(T101), s(T103), T104) → U2_gaa(T101, T103, T104, pC_in_gaaa(T101, T103, X225, T104))
pC_in_gaaa(T101, T108, T107, T109) → U14_gaaa(T101, T108, T107, T109, leG_in_gaa(T101, T108, T107))
leG_in_gaa(0, T116, true) → leG_out_gaa(0, T116, true)
leG_in_gaa(s(T121), 0, false) → leG_out_gaa(s(T121), 0, false)
leG_in_gaa(s(T126), s(T128), X251) → U5_gaa(T126, T128, X251, leG_in_gaa(T126, T128, X251))
U5_gaa(T126, T128, X251, leG_out_gaa(T126, T128, X251)) → leG_out_gaa(s(T126), s(T128), X251)
U14_gaaa(T101, T108, T107, T109, leG_out_gaa(T101, T108, T107)) → U15_gaaa(T101, T108, T107, T109, ifL_in_ggaa(T107, T101, T108, T109))
ifL_in_ggaa(true, T143, T144, 0) → ifL_out_ggaa(true, T143, T144, 0)
ifL_in_ggaa(false, T163, T155, s(T154)) → U9_ggaa(T163, T155, T154, minusA_in_gaa(T163, s(T155), T154))
U9_ggaa(T163, T155, T154, minusA_out_gaa(T163, s(T155), T154)) → ifL_out_ggaa(false, T163, T155, s(T154))
U15_gaaa(T101, T108, T107, T109, ifL_out_ggaa(T107, T101, T108, T109)) → pC_out_gaaa(T101, T108, T107, T109)
U2_gaa(T101, T103, T104, pC_out_gaaa(T101, T103, X225, T104)) → minusA_out_gaa(s(T101), s(T103), T104)

The argument filtering Pi contains the following mapping:
minusA_in_gaa(x1, x2, x3)  =  minusA_in_gaa(x1)
0  =  0
minusA_out_gaa(x1, x2, x3)  =  minusA_out_gaa(x1, x3)
s(x1)  =  s(x1)
U1_gaa(x1, x2, x3)  =  U1_gaa(x1, x3)
minusB_in_ga(x1, x2)  =  minusB_in_ga(x1)
U4_ga(x1, x2, x3)  =  U4_ga(x1, x3)
pF_in_gaa(x1, x2, x3)  =  pF_in_gaa(x1)
U10_gaa(x1, x2, x3, x4)  =  U10_gaa(x1, x4)
leH_in_ga(x1, x2)  =  leH_in_ga(x1)
leH_out_ga(x1, x2)  =  leH_out_ga(x1, x2)
U11_gaa(x1, x2, x3, x4)  =  U11_gaa(x1, x2, x4)
ifI_in_gga(x1, x2, x3)  =  ifI_in_gga(x1, x2)
true  =  true
ifI_out_gga(x1, x2, x3)  =  ifI_out_gga(x1, x2, x3)
false  =  false
U6_gga(x1, x2)  =  U6_gga(x2)
minusD_in_a(x1)  =  minusD_in_a
U3_a(x1, x2)  =  U3_a(x2)
pE_in_aa(x1, x2)  =  pE_in_aa
U12_aa(x1, x2, x3)  =  U12_aa(x3)
leJ_in_a(x1)  =  leJ_in_a
leJ_out_a(x1)  =  leJ_out_a(x1)
U13_aa(x1, x2, x3)  =  U13_aa(x1, x3)
ifK_in_ga(x1, x2)  =  ifK_in_ga(x1)
ifK_out_ga(x1, x2)  =  ifK_out_ga(x1, x2)
U8_ga(x1, x2)  =  U8_ga(x2)
minusD_out_a(x1)  =  minusD_out_a(x1)
pE_out_aa(x1, x2)  =  pE_out_aa(x1, x2)
U7_gga(x1, x2, x3)  =  U7_gga(x1, x3)
minusB_out_ga(x1, x2)  =  minusB_out_ga(x1, x2)
pF_out_gaa(x1, x2, x3)  =  pF_out_gaa(x1, x2, x3)
U2_gaa(x1, x2, x3, x4)  =  U2_gaa(x1, x4)
pC_in_gaaa(x1, x2, x3, x4)  =  pC_in_gaaa(x1)
U14_gaaa(x1, x2, x3, x4, x5)  =  U14_gaaa(x1, x5)
leG_in_gaa(x1, x2, x3)  =  leG_in_gaa(x1)
leG_out_gaa(x1, x2, x3)  =  leG_out_gaa(x1, x3)
U5_gaa(x1, x2, x3, x4)  =  U5_gaa(x1, x4)
U15_gaaa(x1, x2, x3, x4, x5)  =  U15_gaaa(x1, x3, x5)
ifL_in_ggaa(x1, x2, x3, x4)  =  ifL_in_ggaa(x1, x2)
ifL_out_ggaa(x1, x2, x3, x4)  =  ifL_out_ggaa(x1, x2, x4)
U9_ggaa(x1, x2, x3, x4)  =  U9_ggaa(x1, x4)
pC_out_gaaa(x1, x2, x3, x4)  =  pC_out_gaaa(x1, x3, x4)
LEG_IN_GAA(x1, x2, x3)  =  LEG_IN_GAA(x1)

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

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

LEG_IN_GAA(s(T126), s(T128), X251) → LEG_IN_GAA(T126, T128, X251)

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

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

(10) PiDPToQDPProof (SOUND transformation)

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

(11) Obligation:

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

LEG_IN_GAA(s(T126)) → LEG_IN_GAA(T126)

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:

• LEG_IN_GAA(s(T126)) → LEG_IN_GAA(T126)
  The graph contains the following edges 1 > 1

(13) YES

(14) Obligation:

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

MINUSA_IN_GAA(s(T101), s(T103), T104) → PC_IN_GAAA(T101, T103, X225, T104)
PC_IN_GAAA(T101, T108, T107, T109) → U14_GAAA(T101, T108, T107, T109, leG_in_gaa(T101, T108, T107))
U14_GAAA(T101, T108, T107, T109, leG_out_gaa(T101, T108, T107)) → IFL_IN_GGAA(T107, T101, T108, T109)
IFL_IN_GGAA(false, T163, T155, s(T154)) → MINUSA_IN_GAA(T163, s(T155), T154)

The TRS R consists of the following rules:

minusA_in_gaa(0, T25, 0) → minusA_out_gaa(0, T25, 0)
minusA_in_gaa(s(T44), 0, s(T38)) → U1_gaa(T44, T38, minusB_in_ga(T44, T38))
minusB_in_ga(T52, T54) → U4_ga(T52, T54, pF_in_gaa(T52, X81, T54))
pF_in_gaa(T52, T55, T54) → U10_gaa(T52, T55, T54, leH_in_ga(T52, T55))
leH_in_ga(0, true) → leH_out_ga(0, true)
leH_in_ga(s(T60), false) → leH_out_ga(s(T60), false)
U10_gaa(T52, T55, T54, leH_out_ga(T52, T55)) → U11_gaa(T52, T55, T54, ifI_in_gga(T55, T52, T54))
ifI_in_gga(true, T68, 0) → ifI_out_gga(true, T68, 0)
ifI_in_gga(false, 0, s(T75)) → U6_gga(T75, minusD_in_a(T75))
minusD_in_a(T82) → U3_a(T82, pE_in_aa(X148, T82))
pE_in_aa(T83, T82) → U12_aa(T83, T82, leJ_in_a(T83))
leJ_in_a(true) → leJ_out_a(true)
U12_aa(T83, T82, leJ_out_a(T83)) → U13_aa(T83, T82, ifK_in_ga(T83, T82))
ifK_in_ga(true, 0) → ifK_out_ga(true, 0)
ifK_in_ga(false, s(T87)) → U8_ga(T87, minusD_in_a(T87))
U8_ga(T87, minusD_out_a(T87)) → ifK_out_ga(false, s(T87))
U13_aa(T83, T82, ifK_out_ga(T83, T82)) → pE_out_aa(T83, T82)
U3_a(T82, pE_out_aa(X148, T82)) → minusD_out_a(T82)
U6_gga(T75, minusD_out_a(T75)) → ifI_out_gga(false, 0, s(T75))
ifI_in_gga(false, s(T94), s(T75)) → U7_gga(T94, T75, minusB_in_ga(T94, T75))
U7_gga(T94, T75, minusB_out_ga(T94, T75)) → ifI_out_gga(false, s(T94), s(T75))
U11_gaa(T52, T55, T54, ifI_out_gga(T55, T52, T54)) → pF_out_gaa(T52, T55, T54)
U4_ga(T52, T54, pF_out_gaa(T52, X81, T54)) → minusB_out_ga(T52, T54)
U1_gaa(T44, T38, minusB_out_ga(T44, T38)) → minusA_out_gaa(s(T44), 0, s(T38))
minusA_in_gaa(s(T101), s(T103), T104) → U2_gaa(T101, T103, T104, pC_in_gaaa(T101, T103, X225, T104))
pC_in_gaaa(T101, T108, T107, T109) → U14_gaaa(T101, T108, T107, T109, leG_in_gaa(T101, T108, T107))
leG_in_gaa(0, T116, true) → leG_out_gaa(0, T116, true)
leG_in_gaa(s(T121), 0, false) → leG_out_gaa(s(T121), 0, false)
leG_in_gaa(s(T126), s(T128), X251) → U5_gaa(T126, T128, X251, leG_in_gaa(T126, T128, X251))
U5_gaa(T126, T128, X251, leG_out_gaa(T126, T128, X251)) → leG_out_gaa(s(T126), s(T128), X251)
U14_gaaa(T101, T108, T107, T109, leG_out_gaa(T101, T108, T107)) → U15_gaaa(T101, T108, T107, T109, ifL_in_ggaa(T107, T101, T108, T109))
ifL_in_ggaa(true, T143, T144, 0) → ifL_out_ggaa(true, T143, T144, 0)
ifL_in_ggaa(false, T163, T155, s(T154)) → U9_ggaa(T163, T155, T154, minusA_in_gaa(T163, s(T155), T154))
U9_ggaa(T163, T155, T154, minusA_out_gaa(T163, s(T155), T154)) → ifL_out_ggaa(false, T163, T155, s(T154))
U15_gaaa(T101, T108, T107, T109, ifL_out_ggaa(T107, T101, T108, T109)) → pC_out_gaaa(T101, T108, T107, T109)
U2_gaa(T101, T103, T104, pC_out_gaaa(T101, T103, X225, T104)) → minusA_out_gaa(s(T101), s(T103), T104)

The argument filtering Pi contains the following mapping:
minusA_in_gaa(x1, x2, x3)  =  minusA_in_gaa(x1)
0  =  0
minusA_out_gaa(x1, x2, x3)  =  minusA_out_gaa(x1, x3)
s(x1)  =  s(x1)
U1_gaa(x1, x2, x3)  =  U1_gaa(x1, x3)
minusB_in_ga(x1, x2)  =  minusB_in_ga(x1)
U4_ga(x1, x2, x3)  =  U4_ga(x1, x3)
pF_in_gaa(x1, x2, x3)  =  pF_in_gaa(x1)
U10_gaa(x1, x2, x3, x4)  =  U10_gaa(x1, x4)
leH_in_ga(x1, x2)  =  leH_in_ga(x1)
leH_out_ga(x1, x2)  =  leH_out_ga(x1, x2)
U11_gaa(x1, x2, x3, x4)  =  U11_gaa(x1, x2, x4)
ifI_in_gga(x1, x2, x3)  =  ifI_in_gga(x1, x2)
true  =  true
ifI_out_gga(x1, x2, x3)  =  ifI_out_gga(x1, x2, x3)
false  =  false
U6_gga(x1, x2)  =  U6_gga(x2)
minusD_in_a(x1)  =  minusD_in_a
U3_a(x1, x2)  =  U3_a(x2)
pE_in_aa(x1, x2)  =  pE_in_aa
U12_aa(x1, x2, x3)  =  U12_aa(x3)
leJ_in_a(x1)  =  leJ_in_a
leJ_out_a(x1)  =  leJ_out_a(x1)
U13_aa(x1, x2, x3)  =  U13_aa(x1, x3)
ifK_in_ga(x1, x2)  =  ifK_in_ga(x1)
ifK_out_ga(x1, x2)  =  ifK_out_ga(x1, x2)
U8_ga(x1, x2)  =  U8_ga(x2)
minusD_out_a(x1)  =  minusD_out_a(x1)
pE_out_aa(x1, x2)  =  pE_out_aa(x1, x2)
U7_gga(x1, x2, x3)  =  U7_gga(x1, x3)
minusB_out_ga(x1, x2)  =  minusB_out_ga(x1, x2)
pF_out_gaa(x1, x2, x3)  =  pF_out_gaa(x1, x2, x3)
U2_gaa(x1, x2, x3, x4)  =  U2_gaa(x1, x4)
pC_in_gaaa(x1, x2, x3, x4)  =  pC_in_gaaa(x1)
U14_gaaa(x1, x2, x3, x4, x5)  =  U14_gaaa(x1, x5)
leG_in_gaa(x1, x2, x3)  =  leG_in_gaa(x1)
leG_out_gaa(x1, x2, x3)  =  leG_out_gaa(x1, x3)
U5_gaa(x1, x2, x3, x4)  =  U5_gaa(x1, x4)
U15_gaaa(x1, x2, x3, x4, x5)  =  U15_gaaa(x1, x3, x5)
ifL_in_ggaa(x1, x2, x3, x4)  =  ifL_in_ggaa(x1, x2)
ifL_out_ggaa(x1, x2, x3, x4)  =  ifL_out_ggaa(x1, x2, x4)
U9_ggaa(x1, x2, x3, x4)  =  U9_ggaa(x1, x4)
pC_out_gaaa(x1, x2, x3, x4)  =  pC_out_gaaa(x1, x3, x4)
MINUSA_IN_GAA(x1, x2, x3)  =  MINUSA_IN_GAA(x1)
PC_IN_GAAA(x1, x2, x3, x4)  =  PC_IN_GAAA(x1)
U14_GAAA(x1, x2, x3, x4, x5)  =  U14_GAAA(x1, x5)
IFL_IN_GGAA(x1, x2, x3, x4)  =  IFL_IN_GGAA(x1, x2)

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

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

MINUSA_IN_GAA(s(T101), s(T103), T104) → PC_IN_GAAA(T101, T103, X225, T104)
PC_IN_GAAA(T101, T108, T107, T109) → U14_GAAA(T101, T108, T107, T109, leG_in_gaa(T101, T108, T107))
U14_GAAA(T101, T108, T107, T109, leG_out_gaa(T101, T108, T107)) → IFL_IN_GGAA(T107, T101, T108, T109)
IFL_IN_GGAA(false, T163, T155, s(T154)) → MINUSA_IN_GAA(T163, s(T155), T154)

The TRS R consists of the following rules:

leG_in_gaa(0, T116, true) → leG_out_gaa(0, T116, true)
leG_in_gaa(s(T121), 0, false) → leG_out_gaa(s(T121), 0, false)
leG_in_gaa(s(T126), s(T128), X251) → U5_gaa(T126, T128, X251, leG_in_gaa(T126, T128, X251))
U5_gaa(T126, T128, X251, leG_out_gaa(T126, T128, X251)) → leG_out_gaa(s(T126), s(T128), X251)

The argument filtering Pi contains the following mapping:
0  =  0
s(x1)  =  s(x1)
true  =  true
false  =  false
leG_in_gaa(x1, x2, x3)  =  leG_in_gaa(x1)
leG_out_gaa(x1, x2, x3)  =  leG_out_gaa(x1, x3)
U5_gaa(x1, x2, x3, x4)  =  U5_gaa(x1, x4)
MINUSA_IN_GAA(x1, x2, x3)  =  MINUSA_IN_GAA(x1)
PC_IN_GAAA(x1, x2, x3, x4)  =  PC_IN_GAAA(x1)
U14_GAAA(x1, x2, x3, x4, x5)  =  U14_GAAA(x1, x5)
IFL_IN_GGAA(x1, x2, x3, x4)  =  IFL_IN_GGAA(x1, x2)

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

(17) PiDPToQDPProof (SOUND transformation)

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

(18) Obligation:

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

MINUSA_IN_GAA(s(T101)) → PC_IN_GAAA(T101)
PC_IN_GAAA(T101) → U14_GAAA(T101, leG_in_gaa(T101))
U14_GAAA(T101, leG_out_gaa(T101, T107)) → IFL_IN_GGAA(T107, T101)
IFL_IN_GGAA(false, T163) → MINUSA_IN_GAA(T163)

The TRS R consists of the following rules:

leG_in_gaa(0) → leG_out_gaa(0, true)
leG_in_gaa(s(T121)) → leG_out_gaa(s(T121), false)
leG_in_gaa(s(T126)) → U5_gaa(T126, leG_in_gaa(T126))
U5_gaa(T126, leG_out_gaa(T126, X251)) → leG_out_gaa(s(T126), X251)

The set Q consists of the following terms:

leG_in_gaa(x0)
U5_gaa(x0, x1)

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:

• PC_IN_GAAA(T101) → U14_GAAA(T101, leG_in_gaa(T101))
  The graph contains the following edges 1 >= 1

• IFL_IN_GGAA(false, T163) → MINUSA_IN_GAA(T163)
  The graph contains the following edges 2 >= 1

• U14_GAAA(T101, leG_out_gaa(T101, T107)) → IFL_IN_GGAA(T107, T101)
  The graph contains the following edges 2 > 1, 1 >= 2, 2 > 2

• MINUSA_IN_GAA(s(T101)) → PC_IN_GAAA(T101)
  The graph contains the following edges 1 > 1

(20) YES

(21) Obligation:

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

MINUSD_IN_A(T82) → PE_IN_AA(X148, T82)
PE_IN_AA(T83, T82) → U12_AA(T83, T82, leJ_in_a(T83))
U12_AA(T83, T82, leJ_out_a(T83)) → IFK_IN_GA(T83, T82)
IFK_IN_GA(false, s(T87)) → MINUSD_IN_A(T87)

The TRS R consists of the following rules:

minusA_in_gaa(0, T25, 0) → minusA_out_gaa(0, T25, 0)
minusA_in_gaa(s(T44), 0, s(T38)) → U1_gaa(T44, T38, minusB_in_ga(T44, T38))
minusB_in_ga(T52, T54) → U4_ga(T52, T54, pF_in_gaa(T52, X81, T54))
pF_in_gaa(T52, T55, T54) → U10_gaa(T52, T55, T54, leH_in_ga(T52, T55))
leH_in_ga(0, true) → leH_out_ga(0, true)
leH_in_ga(s(T60), false) → leH_out_ga(s(T60), false)
U10_gaa(T52, T55, T54, leH_out_ga(T52, T55)) → U11_gaa(T52, T55, T54, ifI_in_gga(T55, T52, T54))
ifI_in_gga(true, T68, 0) → ifI_out_gga(true, T68, 0)
ifI_in_gga(false, 0, s(T75)) → U6_gga(T75, minusD_in_a(T75))
minusD_in_a(T82) → U3_a(T82, pE_in_aa(X148, T82))
pE_in_aa(T83, T82) → U12_aa(T83, T82, leJ_in_a(T83))
leJ_in_a(true) → leJ_out_a(true)
U12_aa(T83, T82, leJ_out_a(T83)) → U13_aa(T83, T82, ifK_in_ga(T83, T82))
ifK_in_ga(true, 0) → ifK_out_ga(true, 0)
ifK_in_ga(false, s(T87)) → U8_ga(T87, minusD_in_a(T87))
U8_ga(T87, minusD_out_a(T87)) → ifK_out_ga(false, s(T87))
U13_aa(T83, T82, ifK_out_ga(T83, T82)) → pE_out_aa(T83, T82)
U3_a(T82, pE_out_aa(X148, T82)) → minusD_out_a(T82)
U6_gga(T75, minusD_out_a(T75)) → ifI_out_gga(false, 0, s(T75))
ifI_in_gga(false, s(T94), s(T75)) → U7_gga(T94, T75, minusB_in_ga(T94, T75))
U7_gga(T94, T75, minusB_out_ga(T94, T75)) → ifI_out_gga(false, s(T94), s(T75))
U11_gaa(T52, T55, T54, ifI_out_gga(T55, T52, T54)) → pF_out_gaa(T52, T55, T54)
U4_ga(T52, T54, pF_out_gaa(T52, X81, T54)) → minusB_out_ga(T52, T54)
U1_gaa(T44, T38, minusB_out_ga(T44, T38)) → minusA_out_gaa(s(T44), 0, s(T38))
minusA_in_gaa(s(T101), s(T103), T104) → U2_gaa(T101, T103, T104, pC_in_gaaa(T101, T103, X225, T104))
pC_in_gaaa(T101, T108, T107, T109) → U14_gaaa(T101, T108, T107, T109, leG_in_gaa(T101, T108, T107))
leG_in_gaa(0, T116, true) → leG_out_gaa(0, T116, true)
leG_in_gaa(s(T121), 0, false) → leG_out_gaa(s(T121), 0, false)
leG_in_gaa(s(T126), s(T128), X251) → U5_gaa(T126, T128, X251, leG_in_gaa(T126, T128, X251))
U5_gaa(T126, T128, X251, leG_out_gaa(T126, T128, X251)) → leG_out_gaa(s(T126), s(T128), X251)
U14_gaaa(T101, T108, T107, T109, leG_out_gaa(T101, T108, T107)) → U15_gaaa(T101, T108, T107, T109, ifL_in_ggaa(T107, T101, T108, T109))
ifL_in_ggaa(true, T143, T144, 0) → ifL_out_ggaa(true, T143, T144, 0)
ifL_in_ggaa(false, T163, T155, s(T154)) → U9_ggaa(T163, T155, T154, minusA_in_gaa(T163, s(T155), T154))
U9_ggaa(T163, T155, T154, minusA_out_gaa(T163, s(T155), T154)) → ifL_out_ggaa(false, T163, T155, s(T154))
U15_gaaa(T101, T108, T107, T109, ifL_out_ggaa(T107, T101, T108, T109)) → pC_out_gaaa(T101, T108, T107, T109)
U2_gaa(T101, T103, T104, pC_out_gaaa(T101, T103, X225, T104)) → minusA_out_gaa(s(T101), s(T103), T104)

The argument filtering Pi contains the following mapping:
minusA_in_gaa(x1, x2, x3)  =  minusA_in_gaa(x1)
0  =  0
minusA_out_gaa(x1, x2, x3)  =  minusA_out_gaa(x1, x3)
s(x1)  =  s(x1)
U1_gaa(x1, x2, x3)  =  U1_gaa(x1, x3)
minusB_in_ga(x1, x2)  =  minusB_in_ga(x1)
U4_ga(x1, x2, x3)  =  U4_ga(x1, x3)
pF_in_gaa(x1, x2, x3)  =  pF_in_gaa(x1)
U10_gaa(x1, x2, x3, x4)  =  U10_gaa(x1, x4)
leH_in_ga(x1, x2)  =  leH_in_ga(x1)
leH_out_ga(x1, x2)  =  leH_out_ga(x1, x2)
U11_gaa(x1, x2, x3, x4)  =  U11_gaa(x1, x2, x4)
ifI_in_gga(x1, x2, x3)  =  ifI_in_gga(x1, x2)
true  =  true
ifI_out_gga(x1, x2, x3)  =  ifI_out_gga(x1, x2, x3)
false  =  false
U6_gga(x1, x2)  =  U6_gga(x2)
minusD_in_a(x1)  =  minusD_in_a
U3_a(x1, x2)  =  U3_a(x2)
pE_in_aa(x1, x2)  =  pE_in_aa
U12_aa(x1, x2, x3)  =  U12_aa(x3)
leJ_in_a(x1)  =  leJ_in_a
leJ_out_a(x1)  =  leJ_out_a(x1)
U13_aa(x1, x2, x3)  =  U13_aa(x1, x3)
ifK_in_ga(x1, x2)  =  ifK_in_ga(x1)
ifK_out_ga(x1, x2)  =  ifK_out_ga(x1, x2)
U8_ga(x1, x2)  =  U8_ga(x2)
minusD_out_a(x1)  =  minusD_out_a(x1)
pE_out_aa(x1, x2)  =  pE_out_aa(x1, x2)
U7_gga(x1, x2, x3)  =  U7_gga(x1, x3)
minusB_out_ga(x1, x2)  =  minusB_out_ga(x1, x2)
pF_out_gaa(x1, x2, x3)  =  pF_out_gaa(x1, x2, x3)
U2_gaa(x1, x2, x3, x4)  =  U2_gaa(x1, x4)
pC_in_gaaa(x1, x2, x3, x4)  =  pC_in_gaaa(x1)
U14_gaaa(x1, x2, x3, x4, x5)  =  U14_gaaa(x1, x5)
leG_in_gaa(x1, x2, x3)  =  leG_in_gaa(x1)
leG_out_gaa(x1, x2, x3)  =  leG_out_gaa(x1, x3)
U5_gaa(x1, x2, x3, x4)  =  U5_gaa(x1, x4)
U15_gaaa(x1, x2, x3, x4, x5)  =  U15_gaaa(x1, x3, x5)
ifL_in_ggaa(x1, x2, x3, x4)  =  ifL_in_ggaa(x1, x2)
ifL_out_ggaa(x1, x2, x3, x4)  =  ifL_out_ggaa(x1, x2, x4)
U9_ggaa(x1, x2, x3, x4)  =  U9_ggaa(x1, x4)
pC_out_gaaa(x1, x2, x3, x4)  =  pC_out_gaaa(x1, x3, x4)
MINUSD_IN_A(x1)  =  MINUSD_IN_A
PE_IN_AA(x1, x2)  =  PE_IN_AA
U12_AA(x1, x2, x3)  =  U12_AA(x3)
IFK_IN_GA(x1, x2)  =  IFK_IN_GA(x1)

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

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

MINUSD_IN_A(T82) → PE_IN_AA(X148, T82)
PE_IN_AA(T83, T82) → U12_AA(T83, T82, leJ_in_a(T83))
U12_AA(T83, T82, leJ_out_a(T83)) → IFK_IN_GA(T83, T82)
IFK_IN_GA(false, s(T87)) → MINUSD_IN_A(T87)

The TRS R consists of the following rules:

leJ_in_a(true) → leJ_out_a(true)

The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
true  =  true
false  =  false
leJ_in_a(x1)  =  leJ_in_a
leJ_out_a(x1)  =  leJ_out_a(x1)
MINUSD_IN_A(x1)  =  MINUSD_IN_A
PE_IN_AA(x1, x2)  =  PE_IN_AA
U12_AA(x1, x2, x3)  =  U12_AA(x3)
IFK_IN_GA(x1, x2)  =  IFK_IN_GA(x1)

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:

MINUSD_IN_A → PE_IN_AA
PE_IN_AA → U12_AA(leJ_in_a)
U12_AA(leJ_out_a(T83)) → IFK_IN_GA(T83)
IFK_IN_GA(false) → MINUSD_IN_A

The TRS R consists of the following rules:

leJ_in_a → leJ_out_a(true)

The set Q consists of the following terms:

leJ_in_a

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

(26) UsableRulesReductionPairsProof (EQUIVALENT transformation)

By using the usable rules with reduction pair processor [LPAR04] with a polynomial ordering [POLO], all dependency pairs and the corresponding usable rules [FROCOS05] can be oriented non-strictly. All non-usable rules are removed, and those dependency pairs and usable rules that have been oriented strictly or contain non-usable symbols in their left-hand side are removed as well.

The following dependency pairs can be deleted:

MINUSD_IN_A → PE_IN_AA
PE_IN_AA → U12_AA(leJ_in_a)
IFK_IN_GA(false) → MINUSD_IN_A

No rules are removed from R.

Used ordering: POLO with Polynomial interpretation [POLO]:

POL(IFK_IN_GA(x₁)) = x₁   
POL(MINUSD_IN_A) = 2   
POL(PE_IN_AA) = 1   
POL(U12_AA(x₁)) = 2·x₁   
POL(false) = 2   
POL(leJ_in_a) = 0   
POL(leJ_out_a(x₁)) = x₁   
POL(true) = 0   

(27) Obligation:

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

U12_AA(leJ_out_a(T83)) → IFK_IN_GA(T83)

The TRS R consists of the following rules:

leJ_in_a → leJ_out_a(true)

The set Q consists of the following terms:

leJ_in_a

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 1 less node.

(29) TRUE

(30) Obligation:

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

MINUSB_IN_GA(T52, T54) → PF_IN_GAA(T52, X81, T54)
PF_IN_GAA(T52, T55, T54) → U10_GAA(T52, T55, T54, leH_in_ga(T52, T55))
U10_GAA(T52, T55, T54, leH_out_ga(T52, T55)) → IFI_IN_GGA(T55, T52, T54)
IFI_IN_GGA(false, s(T94), s(T75)) → MINUSB_IN_GA(T94, T75)

The TRS R consists of the following rules:

minusA_in_gaa(0, T25, 0) → minusA_out_gaa(0, T25, 0)
minusA_in_gaa(s(T44), 0, s(T38)) → U1_gaa(T44, T38, minusB_in_ga(T44, T38))
minusB_in_ga(T52, T54) → U4_ga(T52, T54, pF_in_gaa(T52, X81, T54))
pF_in_gaa(T52, T55, T54) → U10_gaa(T52, T55, T54, leH_in_ga(T52, T55))
leH_in_ga(0, true) → leH_out_ga(0, true)
leH_in_ga(s(T60), false) → leH_out_ga(s(T60), false)
U10_gaa(T52, T55, T54, leH_out_ga(T52, T55)) → U11_gaa(T52, T55, T54, ifI_in_gga(T55, T52, T54))
ifI_in_gga(true, T68, 0) → ifI_out_gga(true, T68, 0)
ifI_in_gga(false, 0, s(T75)) → U6_gga(T75, minusD_in_a(T75))
minusD_in_a(T82) → U3_a(T82, pE_in_aa(X148, T82))
pE_in_aa(T83, T82) → U12_aa(T83, T82, leJ_in_a(T83))
leJ_in_a(true) → leJ_out_a(true)
U12_aa(T83, T82, leJ_out_a(T83)) → U13_aa(T83, T82, ifK_in_ga(T83, T82))
ifK_in_ga(true, 0) → ifK_out_ga(true, 0)
ifK_in_ga(false, s(T87)) → U8_ga(T87, minusD_in_a(T87))
U8_ga(T87, minusD_out_a(T87)) → ifK_out_ga(false, s(T87))
U13_aa(T83, T82, ifK_out_ga(T83, T82)) → pE_out_aa(T83, T82)
U3_a(T82, pE_out_aa(X148, T82)) → minusD_out_a(T82)
U6_gga(T75, minusD_out_a(T75)) → ifI_out_gga(false, 0, s(T75))
ifI_in_gga(false, s(T94), s(T75)) → U7_gga(T94, T75, minusB_in_ga(T94, T75))
U7_gga(T94, T75, minusB_out_ga(T94, T75)) → ifI_out_gga(false, s(T94), s(T75))
U11_gaa(T52, T55, T54, ifI_out_gga(T55, T52, T54)) → pF_out_gaa(T52, T55, T54)
U4_ga(T52, T54, pF_out_gaa(T52, X81, T54)) → minusB_out_ga(T52, T54)
U1_gaa(T44, T38, minusB_out_ga(T44, T38)) → minusA_out_gaa(s(T44), 0, s(T38))
minusA_in_gaa(s(T101), s(T103), T104) → U2_gaa(T101, T103, T104, pC_in_gaaa(T101, T103, X225, T104))
pC_in_gaaa(T101, T108, T107, T109) → U14_gaaa(T101, T108, T107, T109, leG_in_gaa(T101, T108, T107))
leG_in_gaa(0, T116, true) → leG_out_gaa(0, T116, true)
leG_in_gaa(s(T121), 0, false) → leG_out_gaa(s(T121), 0, false)
leG_in_gaa(s(T126), s(T128), X251) → U5_gaa(T126, T128, X251, leG_in_gaa(T126, T128, X251))
U5_gaa(T126, T128, X251, leG_out_gaa(T126, T128, X251)) → leG_out_gaa(s(T126), s(T128), X251)
U14_gaaa(T101, T108, T107, T109, leG_out_gaa(T101, T108, T107)) → U15_gaaa(T101, T108, T107, T109, ifL_in_ggaa(T107, T101, T108, T109))
ifL_in_ggaa(true, T143, T144, 0) → ifL_out_ggaa(true, T143, T144, 0)
ifL_in_ggaa(false, T163, T155, s(T154)) → U9_ggaa(T163, T155, T154, minusA_in_gaa(T163, s(T155), T154))
U9_ggaa(T163, T155, T154, minusA_out_gaa(T163, s(T155), T154)) → ifL_out_ggaa(false, T163, T155, s(T154))
U15_gaaa(T101, T108, T107, T109, ifL_out_ggaa(T107, T101, T108, T109)) → pC_out_gaaa(T101, T108, T107, T109)
U2_gaa(T101, T103, T104, pC_out_gaaa(T101, T103, X225, T104)) → minusA_out_gaa(s(T101), s(T103), T104)

The argument filtering Pi contains the following mapping:
minusA_in_gaa(x1, x2, x3)  =  minusA_in_gaa(x1)
0  =  0
minusA_out_gaa(x1, x2, x3)  =  minusA_out_gaa(x1, x3)
s(x1)  =  s(x1)
U1_gaa(x1, x2, x3)  =  U1_gaa(x1, x3)
minusB_in_ga(x1, x2)  =  minusB_in_ga(x1)
U4_ga(x1, x2, x3)  =  U4_ga(x1, x3)
pF_in_gaa(x1, x2, x3)  =  pF_in_gaa(x1)
U10_gaa(x1, x2, x3, x4)  =  U10_gaa(x1, x4)
leH_in_ga(x1, x2)  =  leH_in_ga(x1)
leH_out_ga(x1, x2)  =  leH_out_ga(x1, x2)
U11_gaa(x1, x2, x3, x4)  =  U11_gaa(x1, x2, x4)
ifI_in_gga(x1, x2, x3)  =  ifI_in_gga(x1, x2)
true  =  true
ifI_out_gga(x1, x2, x3)  =  ifI_out_gga(x1, x2, x3)
false  =  false
U6_gga(x1, x2)  =  U6_gga(x2)
minusD_in_a(x1)  =  minusD_in_a
U3_a(x1, x2)  =  U3_a(x2)
pE_in_aa(x1, x2)  =  pE_in_aa
U12_aa(x1, x2, x3)  =  U12_aa(x3)
leJ_in_a(x1)  =  leJ_in_a
leJ_out_a(x1)  =  leJ_out_a(x1)
U13_aa(x1, x2, x3)  =  U13_aa(x1, x3)
ifK_in_ga(x1, x2)  =  ifK_in_ga(x1)
ifK_out_ga(x1, x2)  =  ifK_out_ga(x1, x2)
U8_ga(x1, x2)  =  U8_ga(x2)
minusD_out_a(x1)  =  minusD_out_a(x1)
pE_out_aa(x1, x2)  =  pE_out_aa(x1, x2)
U7_gga(x1, x2, x3)  =  U7_gga(x1, x3)
minusB_out_ga(x1, x2)  =  minusB_out_ga(x1, x2)
pF_out_gaa(x1, x2, x3)  =  pF_out_gaa(x1, x2, x3)
U2_gaa(x1, x2, x3, x4)  =  U2_gaa(x1, x4)
pC_in_gaaa(x1, x2, x3, x4)  =  pC_in_gaaa(x1)
U14_gaaa(x1, x2, x3, x4, x5)  =  U14_gaaa(x1, x5)
leG_in_gaa(x1, x2, x3)  =  leG_in_gaa(x1)
leG_out_gaa(x1, x2, x3)  =  leG_out_gaa(x1, x3)
U5_gaa(x1, x2, x3, x4)  =  U5_gaa(x1, x4)
U15_gaaa(x1, x2, x3, x4, x5)  =  U15_gaaa(x1, x3, x5)
ifL_in_ggaa(x1, x2, x3, x4)  =  ifL_in_ggaa(x1, x2)
ifL_out_ggaa(x1, x2, x3, x4)  =  ifL_out_ggaa(x1, x2, x4)
U9_ggaa(x1, x2, x3, x4)  =  U9_ggaa(x1, x4)
pC_out_gaaa(x1, x2, x3, x4)  =  pC_out_gaaa(x1, x3, x4)
MINUSB_IN_GA(x1, x2)  =  MINUSB_IN_GA(x1)
PF_IN_GAA(x1, x2, x3)  =  PF_IN_GAA(x1)
U10_GAA(x1, x2, x3, x4)  =  U10_GAA(x1, x4)
IFI_IN_GGA(x1, x2, x3)  =  IFI_IN_GGA(x1, x2)

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

(31) UsableRulesProof (EQUIVALENT transformation)

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

(32) Obligation:

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

MINUSB_IN_GA(T52, T54) → PF_IN_GAA(T52, X81, T54)
PF_IN_GAA(T52, T55, T54) → U10_GAA(T52, T55, T54, leH_in_ga(T52, T55))
U10_GAA(T52, T55, T54, leH_out_ga(T52, T55)) → IFI_IN_GGA(T55, T52, T54)
IFI_IN_GGA(false, s(T94), s(T75)) → MINUSB_IN_GA(T94, T75)

The TRS R consists of the following rules:

leH_in_ga(0, true) → leH_out_ga(0, true)
leH_in_ga(s(T60), false) → leH_out_ga(s(T60), false)

The argument filtering Pi contains the following mapping:
0  =  0
s(x1)  =  s(x1)
leH_in_ga(x1, x2)  =  leH_in_ga(x1)
leH_out_ga(x1, x2)  =  leH_out_ga(x1, x2)
true  =  true
false  =  false
MINUSB_IN_GA(x1, x2)  =  MINUSB_IN_GA(x1)
PF_IN_GAA(x1, x2, x3)  =  PF_IN_GAA(x1)
U10_GAA(x1, x2, x3, x4)  =  U10_GAA(x1, x4)
IFI_IN_GGA(x1, x2, x3)  =  IFI_IN_GGA(x1, x2)

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:

MINUSB_IN_GA(T52) → PF_IN_GAA(T52)
PF_IN_GAA(T52) → U10_GAA(T52, leH_in_ga(T52))
U10_GAA(T52, leH_out_ga(T52, T55)) → IFI_IN_GGA(T55, T52)
IFI_IN_GGA(false, s(T94)) → MINUSB_IN_GA(T94)

The TRS R consists of the following rules:

leH_in_ga(0) → leH_out_ga(0, true)
leH_in_ga(s(T60)) → leH_out_ga(s(T60), false)

The set Q consists of the following terms:

leH_in_ga(x0)

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:

• PF_IN_GAA(T52) → U10_GAA(T52, leH_in_ga(T52))
  The graph contains the following edges 1 >= 1

• IFI_IN_GGA(false, s(T94)) → MINUSB_IN_GA(T94)
  The graph contains the following edges 2 > 1

• U10_GAA(T52, leH_out_ga(T52, T55)) → IFI_IN_GGA(T55, T52)
  The graph contains the following edges 2 > 1, 1 >= 2, 2 > 2

• MINUSB_IN_GA(T52) → PF_IN_GAA(T52)
  The graph contains the following edges 1 >= 1

(36) YES