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

(0) Obligation:

Clauses:

rem(X, Y, R) :- ','(notZero(Y), ','(sub(X, Y, Z), rem(Z, Y, R))).
rem(X, Y, X) :- ','(notZero(Y), geq(X, Y)).
sub(s(X), s(Y), Z) :- sub(X, Y, Z).
sub(X, 0, X).
notZero(s(X)).
geq(s(X), s(Y)) :- geq(X, Y).
geq(X, 0).

Query: rem(g,a,g)

(1) PrologToPiTRSViaGraphTransformerProof (SOUND transformation)

Transformed Prolog program to (Pi-)TRS.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
1 [label="A: rem(T1, T2, T3)\n\nT1 is ground\nT3 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
5 [label="5: rem(T1, T2, T3), SCOPE: 1, CLAUSE: 0 | rem(T1, T2, T3), SCOPE: 1, CLAUSE: 1\n\nT1 is ground\nT3 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
8 [label="8: ','(notZero(T10), ','(sub(T7, T10, X7), rem(X7, T10, T9))) | rem(T7, T2, T9), SCOPE: 1, CLAUSE: 1\n\nT7 is ground\nT9 is ground\nX7 is free", fontsize=16, style=filled, fillcolor=lightyellow];
12 [label="12: ','(notZero(T10), ','(sub(T7, T10, X7), rem(X7, T10, T9))), SCOPE: 2, CLAUSE: 4 | ?_2 | rem(T7, T2, T9), SCOPE: 1, CLAUSE: 1\n\nT7 is ground\nT9 is ground\nX7 is free", fontsize=16, style=filled, fillcolor=lightyellow];
13 [label="13: ','(notZero(T10), ','(sub(T7, T10, X7), rem(X7, T10, T9))), SCOPE: 2, CLAUSE: 4\n\nT7 is ground\nT9 is ground\nX7 is free", fontsize=16, style=filled, fillcolor=lightyellow];
14 [label="14: ?_2 | rem(T7, T2, T9), SCOPE: 1, CLAUSE: 1\n\nT7 is ground\nT9 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
15 [label="B: ','(sub(T7, s(T16), X7), rem(X7, s(T16), T9))\n\nT7 is ground\nT9 is ground\nX7 is free", fontsize=16, style=filled, fillcolor=lightyellow];
16 [label="16: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
26 [label="I: sub(T7, s(T16), X7)\n\nT7 is ground\nX7 is free", fontsize=16, style=filled, fillcolor=lightyellow];
29 [label="E: rem(T19, s(T20), T9)\n\nT9 is ground\nT20 is ground\nT19 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
33 [label="33: sub(T7, s(T16), X7), SCOPE: 3, CLAUSE: 2 | sub(T7, s(T16), X7), SCOPE: 3, CLAUSE: 3\n\nT7 is ground\nX7 is free", fontsize=16, style=filled, fillcolor=lightyellow];
34 [label="34: sub(T7, s(T16), X7), SCOPE: 3, CLAUSE: 2\n\nT7 is ground\nX7 is free", fontsize=16, style=filled, fillcolor=lightyellow];
35 [label="35: sub(T7, s(T16), X7), SCOPE: 3, CLAUSE: 3\n\nT7 is ground\nX7 is free", fontsize=16, style=filled, fillcolor=lightyellow];
40 [label="D: sub(T31, T33, X40)\n\nT31 is ground\nX40 is free", fontsize=16, style=filled, fillcolor=lightyellow];
41 [label="41: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
45 [label="45: sub(T31, T33, X40), SCOPE: 4, CLAUSE: 2 | sub(T31, T33, X40), SCOPE: 4, CLAUSE: 3\n\nT31 is ground\nX40 is free", fontsize=16, style=filled, fillcolor=lightyellow];
47 [label="47: sub(T31, T33, X40), SCOPE: 4, CLAUSE: 2\n\nT31 is ground\nX40 is free", fontsize=16, style=filled, fillcolor=lightyellow];
48 [label="48: sub(T31, T33, X40), SCOPE: 4, CLAUSE: 3\n\nT31 is ground\nX40 is free", fontsize=16, style=filled, fillcolor=lightyellow];
52 [label="52: sub(T44, T46, X64)\n\nT44 is ground\nX64 is free", fontsize=16, style=filled, fillcolor=lightyellow];
53 [label="53: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
59 [label="59: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
60 [label="60: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
62 [label="62: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
67 [label="67: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
72 [label="72: rem(T19, s(T20), T9), SCOPE: 5, CLAUSE: 0 | rem(T19, s(T20), T9), SCOPE: 5, CLAUSE: 1\n\nT9 is ground\nT20 is ground\nT19 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
75 [label="75: rem(T19, s(T20), T9), SCOPE: 5, CLAUSE: 0\n\nT9 is ground\nT20 is ground\nT19 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
76 [label="76: rem(T19, s(T20), T9), SCOPE: 5, CLAUSE: 1\n\nT9 is ground\nT20 is ground\nT19 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
80 [label="80: ','(notZero(s(T73)), ','(sub(T72, s(T73), X102), rem(X102, s(T73), T74)))\n\nT72 is ground\nT73 is ground\nT74 is ground\nX102 is free", fontsize=16, style=filled, fillcolor=lightyellow];
81 [label="81: ','(notZero(s(T73)), ','(sub(T72, s(T73), X102), rem(X102, s(T73), T74))), SCOPE: 6, CLAUSE: 4\n\nT72 is ground\nT73 is ground\nT74 is ground\nX102 is free", fontsize=16, style=filled, fillcolor=lightyellow];
84 [label="F: ','(sub(T72, s(T81), X102), rem(X102, s(T81), T74))\n\nT72 is ground\nT74 is ground\nT81 is ground\nX102 is free", fontsize=16, style=filled, fillcolor=lightyellow];
88 [label="J: sub(T72, s(T81), X102)\n\nT72 is ground\nT81 is ground\nX102 is free", fontsize=16, style=filled, fillcolor=lightyellow];
89 [label="89: rem(T84, s(T81), T74)\n\nT74 is ground\nT81 is ground\nT84 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
92 [label="92: sub(T72, s(T81), X102), SCOPE: 7, CLAUSE: 2 | sub(T72, s(T81), X102), SCOPE: 7, CLAUSE: 3\n\nT72 is ground\nT81 is ground\nX102 is free", fontsize=16, style=filled, fillcolor=lightyellow];
94 [label="94: sub(T72, s(T81), X102), SCOPE: 7, CLAUSE: 2\n\nT72 is ground\nT81 is ground\nX102 is free", fontsize=16, style=filled, fillcolor=lightyellow];
95 [label="95: sub(T72, s(T81), X102), SCOPE: 7, CLAUSE: 3\n\nT72 is ground\nT81 is ground\nX102 is free", fontsize=16, style=filled, fillcolor=lightyellow];
100 [label="H: sub(T95, T96, X141)\n\nT95 is ground\nT96 is ground\nX141 is free", fontsize=16, style=filled, fillcolor=lightyellow];
101 [label="101: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
104 [label="104: sub(T95, T96, X141), SCOPE: 8, CLAUSE: 2 | sub(T95, T96, X141), SCOPE: 8, CLAUSE: 3\n\nT95 is ground\nT96 is ground\nX141 is free", fontsize=16, style=filled, fillcolor=lightyellow];
106 [label="106: sub(T95, T96, X141), SCOPE: 8, CLAUSE: 2\n\nT95 is ground\nT96 is ground\nX141 is free", fontsize=16, style=filled, fillcolor=lightyellow];
107 [label="107: sub(T95, T96, X141), SCOPE: 8, CLAUSE: 3\n\nT95 is ground\nT96 is ground\nX141 is free", fontsize=16, style=filled, fillcolor=lightyellow];
111 [label="111: sub(T107, T108, X165)\n\nT107 is ground\nT108 is ground\nX165 is free", fontsize=16, style=filled, fillcolor=lightyellow];
112 [label="112: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
115 [label="115: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
118 [label="118: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
119 [label="119: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
120 [label="120: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
126 [label="126: ','(notZero(s(T123)), geq(T122, s(T123)))\n\nT122 is ground\nT123 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
127 [label="127: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
128 [label="128: ','(notZero(s(T123)), geq(T122, s(T123))), SCOPE: 9, CLAUSE: 4\n\nT122 is ground\nT123 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
129 [label="129: geq(T122, s(T130))\n\nT122 is ground\nT130 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
132 [label="132: geq(T122, s(T130)), SCOPE: 10, CLAUSE: 5 | geq(T122, s(T130)), SCOPE: 10, CLAUSE: 6\n\nT122 is ground\nT130 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
134 [label="134: geq(T122, s(T130)), SCOPE: 10, CLAUSE: 5\n\nT122 is ground\nT130 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
135 [label="135: geq(T122, s(T130)), SCOPE: 10, CLAUSE: 6\n\nT122 is ground\nT130 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
138 [label="G: geq(T141, T142)\n\nT141 is ground\nT142 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
139 [label="139: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
142 [label="142: geq(T141, T142), SCOPE: 11, CLAUSE: 5 | geq(T141, T142), SCOPE: 11, CLAUSE: 6\n\nT141 is ground\nT142 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
146 [label="146: geq(T141, T142), SCOPE: 11, CLAUSE: 5\n\nT141 is ground\nT142 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
147 [label="147: geq(T141, T142), SCOPE: 11, CLAUSE: 6\n\nT141 is ground\nT142 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
152 [label="152: geq(T153, T154)\n\nT153 is ground\nT154 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
153 [label="153: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
158 [label="158: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
159 [label="159: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
160 [label="160: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
161 [label="161: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
162 [label="162: rem(T7, T2, T9), SCOPE: 1, CLAUSE: 1\n\nT7 is ground\nT9 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
167 [label="167: ','(notZero(T167), geq(T165, T167))\n\nT165 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
168 [label="168: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
169 [label="169: ','(notZero(T167), geq(T165, T167)), SCOPE: 12, CLAUSE: 4\n\nT165 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
170 [label="170: geq(T165, s(T173))\n\nT165 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
171 [label="171: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
175 [label="175: geq(T165, s(T173)), SCOPE: 13, CLAUSE: 5 | geq(T165, s(T173)), SCOPE: 13, CLAUSE: 6\n\nT165 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
178 [label="178: geq(T165, s(T173)), SCOPE: 13, CLAUSE: 5\n\nT165 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
179 [label="179: geq(T165, s(T173)), SCOPE: 13, CLAUSE: 6\n\nT165 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
185 [label="C: geq(T184, T186)\n\nT184 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
186 [label="186: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
189 [label="189: geq(T184, T186), SCOPE: 14, CLAUSE: 5 | geq(T184, T186), SCOPE: 14, CLAUSE: 6\n\nT184 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
191 [label="191: geq(T184, T186), SCOPE: 14, CLAUSE: 5\n\nT184 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
192 [label="192: geq(T184, T186), SCOPE: 14, CLAUSE: 6\n\nT184 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
197 [label="197: geq(T197, T199)\n\nT197 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
198 [label="198: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
206 [label="206: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
207 [label="207: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
208 [label="208: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
212 [label="212: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
213 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
1 -> 213 [arrowhead = none ];
213 -> 5;

214 [label="ONLY EVAL with clause\nrem(X4, X5, X6) :- ','(notZero(X5), ','(sub(X4, X5, X7), rem(X7, X5, X6))).\nand substitutionT1 -> T7,\nX4 -> T7,\nT2 -> T10,\nX5 -> T10,\nT3 -> T9,\nX6 -> T9,\nT8 -> T10", fontsize=14, style = filled, fillcolor = lightblue];
5 -> 214 [arrowhead = none ];
214 -> 8;

215 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
8 -> 215 [arrowhead = none ];
215 -> 12;

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

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

218 [label="EVAL with clause\nnotZero(s(X12)).\nand substitutionX12 -> T16,\nT10 -> s(T16),\nT15 -> T16", fontsize=14, style = filled, fillcolor = lightblue];
13 -> 218 [arrowhead = none ];
218 -> 15;

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

220 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
14 -> 220 [arrowhead = none ];
220 -> 162;

221 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
15 -> 221 [arrowhead = none ];
221 -> 26;

222 [label="SPLIT 2\nnew knowledge:\nT7 is ground\nT20 is ground\nT19 is ground\nreplacements:X7 -> T19,\nT16 -> T20", fontsize=14, style = filled, fillcolor = violet];
15 -> 222 [arrowhead = none ];
222 -> 29;

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

224 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
29 -> 224 [arrowhead = none ];
224 -> 72;

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

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

227 [label="EVAL with clause\nsub(s(X37), s(X38), X39) :- sub(X37, X38, X39).\nand substitutionX37 -> T31,\nT7 -> s(T31),\nT16 -> T33,\nX38 -> T33,\nX7 -> X40,\nX39 -> X40,\nT32 -> T33", fontsize=14, style = filled, fillcolor = lightblue];
34 -> 227 [arrowhead = none ];
227 -> 40;

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

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

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

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

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

233 [label="EVAL with clause\nsub(s(X61), s(X62), X63) :- sub(X61, X62, X63).\nand substitutionX61 -> T44,\nT31 -> s(T44),\nX62 -> T46,\nT33 -> s(T46),\nX40 -> X64,\nX63 -> X64,\nT45 -> T46", fontsize=14, style = filled, fillcolor = lightblue];
47 -> 233 [arrowhead = none ];
233 -> 52;

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

235 [label="EVAL with clause\nsub(X71, 0, X71).\nand substitutionT31 -> T51,\nX71 -> T51,\nT33 -> 0,\nX40 -> T51", fontsize=14, style = filled, fillcolor = lightblue];
48 -> 235 [arrowhead = none ];
235 -> 59;

236 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
48 -> 236 [arrowhead = none ];
236 -> 60;

237 [label="INSTANCE with matching:\nT31 -> T44\nT33 -> T46\nX40 -> X64", fontsize=14, style = filled, fillcolor = lightgrey];
52 -> 237 [arrowhead = none , style=dashed];
237 -> 40[style=dashed];

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

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

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

241 [label="ONLY EVAL with clause\nrem(X99, X100, X101) :- ','(notZero(X100), ','(sub(X99, X100, X102), rem(X102, X100, X101))).\nand substitutionT19 -> T72,\nX99 -> T72,\nT20 -> T73,\nX100 -> s(T73),\nT9 -> T74,\nX101 -> T74", fontsize=14, style = filled, fillcolor = lightblue];
75 -> 241 [arrowhead = none ];
241 -> 80;

242 [label="EVAL with clause\nrem(X182, X183, X182) :- ','(notZero(X183), geq(X182, X183)).\nand substitutionT19 -> T122,\nX182 -> T122,\nT20 -> T123,\nX183 -> s(T123),\nT9 -> T122", fontsize=14, style = filled, fillcolor = lightblue];
76 -> 242 [arrowhead = none ];
242 -> 126;

243 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
76 -> 243 [arrowhead = none ];
243 -> 127;

244 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
80 -> 244 [arrowhead = none ];
244 -> 81;

245 [label="ONLY EVAL with clause\nnotZero(s(X113)).\nand substitutionT73 -> T81,\nX113 -> T81", fontsize=14, style = filled, fillcolor = lightblue];
81 -> 245 [arrowhead = none ];
245 -> 84;

246 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
84 -> 246 [arrowhead = none ];
246 -> 88;

247 [label="SPLIT 2\nnew knowledge:\nT72 is ground\nT81 is ground\nT84 is ground\nreplacements:X102 -> T84", fontsize=14, style = filled, fillcolor = violet];
84 -> 247 [arrowhead = none ];
247 -> 89;

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

249 [label="INSTANCE with matching:\nT19 -> T84\nT20 -> T81\nT9 -> T74", fontsize=14, style = filled, fillcolor = lightgrey];
89 -> 249 [arrowhead = none , style=dashed];
249 -> 29[style=dashed];

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

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

252 [label="EVAL with clause\nsub(s(X138), s(X139), X140) :- sub(X138, X139, X140).\nand substitutionX138 -> T95,\nT72 -> s(T95),\nT81 -> T96,\nX139 -> T96,\nX102 -> X141,\nX140 -> X141", fontsize=14, style = filled, fillcolor = lightblue];
94 -> 252 [arrowhead = none ];
252 -> 100;

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

254 [label="BACKTRACK\nfor clause: sub(X, 0, X)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
95 -> 254 [arrowhead = none ];
254 -> 120;

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

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

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

258 [label="EVAL with clause\nsub(s(X162), s(X163), X164) :- sub(X162, X163, X164).\nand substitutionX162 -> T107,\nT95 -> s(T107),\nX163 -> T108,\nT96 -> s(T108),\nX141 -> X165,\nX164 -> X165", fontsize=14, style = filled, fillcolor = lightblue];
106 -> 258 [arrowhead = none ];
258 -> 111;

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

260 [label="EVAL with clause\nsub(X172, 0, X172).\nand substitutionT95 -> T113,\nX172 -> T113,\nT96 -> 0,\nX141 -> T113", fontsize=14, style = filled, fillcolor = lightblue];
107 -> 260 [arrowhead = none ];
260 -> 115;

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

262 [label="INSTANCE with matching:\nT95 -> T107\nT96 -> T108\nX141 -> X165", fontsize=14, style = filled, fillcolor = lightgrey];
111 -> 262 [arrowhead = none , style=dashed];
262 -> 100[style=dashed];

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

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

265 [label="ONLY EVAL with clause\nnotZero(s(X190)).\nand substitutionT123 -> T130,\nX190 -> T130", fontsize=14, style = filled, fillcolor = lightblue];
128 -> 265 [arrowhead = none ];
265 -> 129;

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

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

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

269 [label="EVAL with clause\ngeq(s(X201), s(X202)) :- geq(X201, X202).\nand substitutionX201 -> T141,\nT122 -> s(T141),\nT130 -> T142,\nX202 -> T142", fontsize=14, style = filled, fillcolor = lightblue];
134 -> 269 [arrowhead = none ];
269 -> 138;

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

271 [label="BACKTRACK\nfor clause: geq(X, 0)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
135 -> 271 [arrowhead = none ];
271 -> 161;

272 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
138 -> 272 [arrowhead = none ];
272 -> 142;

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

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

275 [label="EVAL with clause\ngeq(s(X213), s(X214)) :- geq(X213, X214).\nand substitutionX213 -> T153,\nT141 -> s(T153),\nX214 -> T154,\nT142 -> s(T154)", fontsize=14, style = filled, fillcolor = lightblue];
146 -> 275 [arrowhead = none ];
275 -> 152;

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

277 [label="EVAL with clause\ngeq(X219, 0).\nand substitutionT141 -> T159,\nX219 -> T159,\nT142 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
147 -> 277 [arrowhead = none ];
277 -> 158;

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

279 [label="INSTANCE with matching:\nT141 -> T153\nT142 -> T154", fontsize=14, style = filled, fillcolor = lightgrey];
152 -> 279 [arrowhead = none , style=dashed];
279 -> 138[style=dashed];

280 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
158 -> 280 [arrowhead = none ];
280 -> 160;

281 [label="EVAL with clause\nrem(X225, X226, X225) :- ','(notZero(X226), geq(X225, X226)).\nand substitutionT7 -> T165,\nX225 -> T165,\nT2 -> T167,\nX226 -> T167,\nT9 -> T165,\nT166 -> T167", fontsize=14, style = filled, fillcolor = lightblue];
162 -> 281 [arrowhead = none ];
281 -> 167;

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

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

284 [label="EVAL with clause\nnotZero(s(X231)).\nand substitutionX231 -> T173,\nT167 -> s(T173),\nT172 -> T173", fontsize=14, style = filled, fillcolor = lightblue];
169 -> 284 [arrowhead = none ];
284 -> 170;

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

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

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

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

289 [label="EVAL with clause\ngeq(s(X242), s(X243)) :- geq(X242, X243).\nand substitutionX242 -> T184,\nT165 -> s(T184),\nT173 -> T186,\nX243 -> T186,\nT185 -> T186", fontsize=14, style = filled, fillcolor = lightblue];
178 -> 289 [arrowhead = none ];
289 -> 185;

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

291 [label="BACKTRACK\nfor clause: geq(X, 0)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
179 -> 291 [arrowhead = none ];
291 -> 212;

292 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
185 -> 292 [arrowhead = none ];
292 -> 189;

293 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
189 -> 293 [arrowhead = none ];
293 -> 191;

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

295 [label="EVAL with clause\ngeq(s(X254), s(X255)) :- geq(X254, X255).\nand substitutionX254 -> T197,\nT184 -> s(T197),\nX255 -> T199,\nT186 -> s(T199),\nT198 -> T199", fontsize=14, style = filled, fillcolor = lightblue];
191 -> 295 [arrowhead = none ];
295 -> 197;

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

297 [label="EVAL with clause\ngeq(X260, 0).\nand substitutionT184 -> T204,\nX260 -> T204,\nT186 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
192 -> 297 [arrowhead = none ];
297 -> 206;

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

299 [label="INSTANCE with matching:\nT184 -> T197\nT186 -> T199", fontsize=14, style = filled, fillcolor = lightgrey];
197 -> 299 [arrowhead = none , style=dashed];
299 -> 185[style=dashed];

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

}

(2) Obligation:

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

remA_in_gag(T7, s(T16), T9) → U1_gag(T7, T16, T9, pB_in_gaag(T7, T16, X7, T9))
pB_in_gaag(T7, T20, T19, T9) → U11_gaag(T7, T20, T19, T9, subI_in_gaa(T7, T20, T19))
subI_in_gaa(s(T31), T33, X40) → U9_gaa(T31, T33, X40, subD_in_gaa(T31, T33, X40))
subD_in_gaa(s(T44), s(T46), X64) → U3_gaa(T44, T46, X64, subD_in_gaa(T44, T46, X64))
subD_in_gaa(T51, 0, T51) → subD_out_gaa(T51, 0, T51)
U3_gaa(T44, T46, X64, subD_out_gaa(T44, T46, X64)) → subD_out_gaa(s(T44), s(T46), X64)
U9_gaa(T31, T33, X40, subD_out_gaa(T31, T33, X40)) → subI_out_gaa(s(T31), T33, X40)
U11_gaag(T7, T20, T19, T9, subI_out_gaa(T7, T20, T19)) → U12_gaag(T7, T20, T19, T9, remE_in_ggg(T19, T20, T9))
remE_in_ggg(T72, T81, T74) → U4_ggg(T72, T81, T74, pF_in_ggag(T72, T81, X102, T74))
pF_in_ggag(T72, T81, T84, T74) → U13_ggag(T72, T81, T84, T74, subJ_in_gga(T72, T81, T84))
subJ_in_gga(s(T95), T96, X141) → U10_gga(T95, T96, X141, subH_in_gga(T95, T96, X141))
subH_in_gga(s(T107), s(T108), X165) → U6_gga(T107, T108, X165, subH_in_gga(T107, T108, X165))
subH_in_gga(T113, 0, T113) → subH_out_gga(T113, 0, T113)
U6_gga(T107, T108, X165, subH_out_gga(T107, T108, X165)) → subH_out_gga(s(T107), s(T108), X165)
U10_gga(T95, T96, X141, subH_out_gga(T95, T96, X141)) → subJ_out_gga(s(T95), T96, X141)
U13_ggag(T72, T81, T84, T74, subJ_out_gga(T72, T81, T84)) → U14_ggag(T72, T81, T84, T74, remE_in_ggg(T84, T81, T74))
remE_in_ggg(s(T141), T142, s(T141)) → U5_ggg(T141, T142, geqG_in_gg(T141, T142))
geqG_in_gg(s(T153), s(T154)) → U7_gg(T153, T154, geqG_in_gg(T153, T154))
geqG_in_gg(T159, 0) → geqG_out_gg(T159, 0)
U7_gg(T153, T154, geqG_out_gg(T153, T154)) → geqG_out_gg(s(T153), s(T154))
U5_ggg(T141, T142, geqG_out_gg(T141, T142)) → remE_out_ggg(s(T141), T142, s(T141))
U14_ggag(T72, T81, T84, T74, remE_out_ggg(T84, T81, T74)) → pF_out_ggag(T72, T81, T84, T74)
U4_ggg(T72, T81, T74, pF_out_ggag(T72, T81, X102, T74)) → remE_out_ggg(T72, T81, T74)
U12_gaag(T7, T20, T19, T9, remE_out_ggg(T19, T20, T9)) → pB_out_gaag(T7, T20, T19, T9)
U1_gag(T7, T16, T9, pB_out_gaag(T7, T16, X7, T9)) → remA_out_gag(T7, s(T16), T9)
remA_in_gag(s(T184), s(T186), s(T184)) → U2_gag(T184, T186, geqC_in_ga(T184, T186))
geqC_in_ga(s(T197), s(T199)) → U8_ga(T197, T199, geqC_in_ga(T197, T199))
geqC_in_ga(T204, 0) → geqC_out_ga(T204, 0)
U8_ga(T197, T199, geqC_out_ga(T197, T199)) → geqC_out_ga(s(T197), s(T199))
U2_gag(T184, T186, geqC_out_ga(T184, T186)) → remA_out_gag(s(T184), s(T186), s(T184))

The argument filtering Pi contains the following mapping:
remA_in_gag(x1, x2, x3)  =  remA_in_gag(x1, x3)
U1_gag(x1, x2, x3, x4)  =  U1_gag(x1, x3, x4)
pB_in_gaag(x1, x2, x3, x4)  =  pB_in_gaag(x1, x4)
U11_gaag(x1, x2, x3, x4, x5)  =  U11_gaag(x1, x4, x5)
subI_in_gaa(x1, x2, x3)  =  subI_in_gaa(x1)
s(x1)  =  s(x1)
U9_gaa(x1, x2, x3, x4)  =  U9_gaa(x1, x4)
subD_in_gaa(x1, x2, x3)  =  subD_in_gaa(x1)
U3_gaa(x1, x2, x3, x4)  =  U3_gaa(x1, x4)
subD_out_gaa(x1, x2, x3)  =  subD_out_gaa(x1, x2, x3)
subI_out_gaa(x1, x2, x3)  =  subI_out_gaa(x1, x2, x3)
U12_gaag(x1, x2, x3, x4, x5)  =  U12_gaag(x1, x2, x3, x4, x5)
remE_in_ggg(x1, x2, x3)  =  remE_in_ggg(x1, x2, x3)
U4_ggg(x1, x2, x3, x4)  =  U4_ggg(x1, x2, x3, x4)
pF_in_ggag(x1, x2, x3, x4)  =  pF_in_ggag(x1, x2, x4)
U13_ggag(x1, x2, x3, x4, x5)  =  U13_ggag(x1, x2, x4, x5)
subJ_in_gga(x1, x2, x3)  =  subJ_in_gga(x1, x2)
U10_gga(x1, x2, x3, x4)  =  U10_gga(x1, x2, x4)
subH_in_gga(x1, x2, x3)  =  subH_in_gga(x1, x2)
U6_gga(x1, x2, x3, x4)  =  U6_gga(x1, x2, x4)
0  =  0
subH_out_gga(x1, x2, x3)  =  subH_out_gga(x1, x2, x3)
subJ_out_gga(x1, x2, x3)  =  subJ_out_gga(x1, x2, x3)
U14_ggag(x1, x2, x3, x4, x5)  =  U14_ggag(x1, x2, x3, x4, x5)
U5_ggg(x1, x2, x3)  =  U5_ggg(x1, x2, x3)
geqG_in_gg(x1, x2)  =  geqG_in_gg(x1, x2)
U7_gg(x1, x2, x3)  =  U7_gg(x1, x2, x3)
geqG_out_gg(x1, x2)  =  geqG_out_gg(x1, x2)
remE_out_ggg(x1, x2, x3)  =  remE_out_ggg(x1, x2, x3)
pF_out_ggag(x1, x2, x3, x4)  =  pF_out_ggag(x1, x2, x3, x4)
pB_out_gaag(x1, x2, x3, x4)  =  pB_out_gaag(x1, x2, x3, x4)
remA_out_gag(x1, x2, x3)  =  remA_out_gag(x1, x2, x3)
U2_gag(x1, x2, x3)  =  U2_gag(x1, x3)
geqC_in_ga(x1, x2)  =  geqC_in_ga(x1)
U8_ga(x1, x2, x3)  =  U8_ga(x1, x3)
geqC_out_ga(x1, x2)  =  geqC_out_ga(x1, x2)

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

REMA_IN_GAG(T7, s(T16), T9) → U1_GAG(T7, T16, T9, pB_in_gaag(T7, T16, X7, T9))
REMA_IN_GAG(T7, s(T16), T9) → PB_IN_GAAG(T7, T16, X7, T9)
PB_IN_GAAG(T7, T20, T19, T9) → U11_GAAG(T7, T20, T19, T9, subI_in_gaa(T7, T20, T19))
PB_IN_GAAG(T7, T20, T19, T9) → SUBI_IN_GAA(T7, T20, T19)
SUBI_IN_GAA(s(T31), T33, X40) → U9_GAA(T31, T33, X40, subD_in_gaa(T31, T33, X40))
SUBI_IN_GAA(s(T31), T33, X40) → SUBD_IN_GAA(T31, T33, X40)
SUBD_IN_GAA(s(T44), s(T46), X64) → U3_GAA(T44, T46, X64, subD_in_gaa(T44, T46, X64))
SUBD_IN_GAA(s(T44), s(T46), X64) → SUBD_IN_GAA(T44, T46, X64)
U11_GAAG(T7, T20, T19, T9, subI_out_gaa(T7, T20, T19)) → U12_GAAG(T7, T20, T19, T9, remE_in_ggg(T19, T20, T9))
U11_GAAG(T7, T20, T19, T9, subI_out_gaa(T7, T20, T19)) → REME_IN_GGG(T19, T20, T9)
REME_IN_GGG(T72, T81, T74) → U4_GGG(T72, T81, T74, pF_in_ggag(T72, T81, X102, T74))
REME_IN_GGG(T72, T81, T74) → PF_IN_GGAG(T72, T81, X102, T74)
PF_IN_GGAG(T72, T81, T84, T74) → U13_GGAG(T72, T81, T84, T74, subJ_in_gga(T72, T81, T84))
PF_IN_GGAG(T72, T81, T84, T74) → SUBJ_IN_GGA(T72, T81, T84)
SUBJ_IN_GGA(s(T95), T96, X141) → U10_GGA(T95, T96, X141, subH_in_gga(T95, T96, X141))
SUBJ_IN_GGA(s(T95), T96, X141) → SUBH_IN_GGA(T95, T96, X141)
SUBH_IN_GGA(s(T107), s(T108), X165) → U6_GGA(T107, T108, X165, subH_in_gga(T107, T108, X165))
SUBH_IN_GGA(s(T107), s(T108), X165) → SUBH_IN_GGA(T107, T108, X165)
U13_GGAG(T72, T81, T84, T74, subJ_out_gga(T72, T81, T84)) → U14_GGAG(T72, T81, T84, T74, remE_in_ggg(T84, T81, T74))
U13_GGAG(T72, T81, T84, T74, subJ_out_gga(T72, T81, T84)) → REME_IN_GGG(T84, T81, T74)
REME_IN_GGG(s(T141), T142, s(T141)) → U5_GGG(T141, T142, geqG_in_gg(T141, T142))
REME_IN_GGG(s(T141), T142, s(T141)) → GEQG_IN_GG(T141, T142)
GEQG_IN_GG(s(T153), s(T154)) → U7_GG(T153, T154, geqG_in_gg(T153, T154))
GEQG_IN_GG(s(T153), s(T154)) → GEQG_IN_GG(T153, T154)
REMA_IN_GAG(s(T184), s(T186), s(T184)) → U2_GAG(T184, T186, geqC_in_ga(T184, T186))
REMA_IN_GAG(s(T184), s(T186), s(T184)) → GEQC_IN_GA(T184, T186)
GEQC_IN_GA(s(T197), s(T199)) → U8_GA(T197, T199, geqC_in_ga(T197, T199))
GEQC_IN_GA(s(T197), s(T199)) → GEQC_IN_GA(T197, T199)

The TRS R consists of the following rules:

remA_in_gag(T7, s(T16), T9) → U1_gag(T7, T16, T9, pB_in_gaag(T7, T16, X7, T9))
pB_in_gaag(T7, T20, T19, T9) → U11_gaag(T7, T20, T19, T9, subI_in_gaa(T7, T20, T19))
subI_in_gaa(s(T31), T33, X40) → U9_gaa(T31, T33, X40, subD_in_gaa(T31, T33, X40))
subD_in_gaa(s(T44), s(T46), X64) → U3_gaa(T44, T46, X64, subD_in_gaa(T44, T46, X64))
subD_in_gaa(T51, 0, T51) → subD_out_gaa(T51, 0, T51)
U3_gaa(T44, T46, X64, subD_out_gaa(T44, T46, X64)) → subD_out_gaa(s(T44), s(T46), X64)
U9_gaa(T31, T33, X40, subD_out_gaa(T31, T33, X40)) → subI_out_gaa(s(T31), T33, X40)
U11_gaag(T7, T20, T19, T9, subI_out_gaa(T7, T20, T19)) → U12_gaag(T7, T20, T19, T9, remE_in_ggg(T19, T20, T9))
remE_in_ggg(T72, T81, T74) → U4_ggg(T72, T81, T74, pF_in_ggag(T72, T81, X102, T74))
pF_in_ggag(T72, T81, T84, T74) → U13_ggag(T72, T81, T84, T74, subJ_in_gga(T72, T81, T84))
subJ_in_gga(s(T95), T96, X141) → U10_gga(T95, T96, X141, subH_in_gga(T95, T96, X141))
subH_in_gga(s(T107), s(T108), X165) → U6_gga(T107, T108, X165, subH_in_gga(T107, T108, X165))
subH_in_gga(T113, 0, T113) → subH_out_gga(T113, 0, T113)
U6_gga(T107, T108, X165, subH_out_gga(T107, T108, X165)) → subH_out_gga(s(T107), s(T108), X165)
U10_gga(T95, T96, X141, subH_out_gga(T95, T96, X141)) → subJ_out_gga(s(T95), T96, X141)
U13_ggag(T72, T81, T84, T74, subJ_out_gga(T72, T81, T84)) → U14_ggag(T72, T81, T84, T74, remE_in_ggg(T84, T81, T74))
remE_in_ggg(s(T141), T142, s(T141)) → U5_ggg(T141, T142, geqG_in_gg(T141, T142))
geqG_in_gg(s(T153), s(T154)) → U7_gg(T153, T154, geqG_in_gg(T153, T154))
geqG_in_gg(T159, 0) → geqG_out_gg(T159, 0)
U7_gg(T153, T154, geqG_out_gg(T153, T154)) → geqG_out_gg(s(T153), s(T154))
U5_ggg(T141, T142, geqG_out_gg(T141, T142)) → remE_out_ggg(s(T141), T142, s(T141))
U14_ggag(T72, T81, T84, T74, remE_out_ggg(T84, T81, T74)) → pF_out_ggag(T72, T81, T84, T74)
U4_ggg(T72, T81, T74, pF_out_ggag(T72, T81, X102, T74)) → remE_out_ggg(T72, T81, T74)
U12_gaag(T7, T20, T19, T9, remE_out_ggg(T19, T20, T9)) → pB_out_gaag(T7, T20, T19, T9)
U1_gag(T7, T16, T9, pB_out_gaag(T7, T16, X7, T9)) → remA_out_gag(T7, s(T16), T9)
remA_in_gag(s(T184), s(T186), s(T184)) → U2_gag(T184, T186, geqC_in_ga(T184, T186))
geqC_in_ga(s(T197), s(T199)) → U8_ga(T197, T199, geqC_in_ga(T197, T199))
geqC_in_ga(T204, 0) → geqC_out_ga(T204, 0)
U8_ga(T197, T199, geqC_out_ga(T197, T199)) → geqC_out_ga(s(T197), s(T199))
U2_gag(T184, T186, geqC_out_ga(T184, T186)) → remA_out_gag(s(T184), s(T186), s(T184))

The argument filtering Pi contains the following mapping:
remA_in_gag(x1, x2, x3)  =  remA_in_gag(x1, x3)
U1_gag(x1, x2, x3, x4)  =  U1_gag(x1, x3, x4)
pB_in_gaag(x1, x2, x3, x4)  =  pB_in_gaag(x1, x4)
U11_gaag(x1, x2, x3, x4, x5)  =  U11_gaag(x1, x4, x5)
subI_in_gaa(x1, x2, x3)  =  subI_in_gaa(x1)
s(x1)  =  s(x1)
U9_gaa(x1, x2, x3, x4)  =  U9_gaa(x1, x4)
subD_in_gaa(x1, x2, x3)  =  subD_in_gaa(x1)
U3_gaa(x1, x2, x3, x4)  =  U3_gaa(x1, x4)
subD_out_gaa(x1, x2, x3)  =  subD_out_gaa(x1, x2, x3)
subI_out_gaa(x1, x2, x3)  =  subI_out_gaa(x1, x2, x3)
U12_gaag(x1, x2, x3, x4, x5)  =  U12_gaag(x1, x2, x3, x4, x5)
remE_in_ggg(x1, x2, x3)  =  remE_in_ggg(x1, x2, x3)
U4_ggg(x1, x2, x3, x4)  =  U4_ggg(x1, x2, x3, x4)
pF_in_ggag(x1, x2, x3, x4)  =  pF_in_ggag(x1, x2, x4)
U13_ggag(x1, x2, x3, x4, x5)  =  U13_ggag(x1, x2, x4, x5)
subJ_in_gga(x1, x2, x3)  =  subJ_in_gga(x1, x2)
U10_gga(x1, x2, x3, x4)  =  U10_gga(x1, x2, x4)
subH_in_gga(x1, x2, x3)  =  subH_in_gga(x1, x2)
U6_gga(x1, x2, x3, x4)  =  U6_gga(x1, x2, x4)
0  =  0
subH_out_gga(x1, x2, x3)  =  subH_out_gga(x1, x2, x3)
subJ_out_gga(x1, x2, x3)  =  subJ_out_gga(x1, x2, x3)
U14_ggag(x1, x2, x3, x4, x5)  =  U14_ggag(x1, x2, x3, x4, x5)
U5_ggg(x1, x2, x3)  =  U5_ggg(x1, x2, x3)
geqG_in_gg(x1, x2)  =  geqG_in_gg(x1, x2)
U7_gg(x1, x2, x3)  =  U7_gg(x1, x2, x3)
geqG_out_gg(x1, x2)  =  geqG_out_gg(x1, x2)
remE_out_ggg(x1, x2, x3)  =  remE_out_ggg(x1, x2, x3)
pF_out_ggag(x1, x2, x3, x4)  =  pF_out_ggag(x1, x2, x3, x4)
pB_out_gaag(x1, x2, x3, x4)  =  pB_out_gaag(x1, x2, x3, x4)
remA_out_gag(x1, x2, x3)  =  remA_out_gag(x1, x2, x3)
U2_gag(x1, x2, x3)  =  U2_gag(x1, x3)
geqC_in_ga(x1, x2)  =  geqC_in_ga(x1)
U8_ga(x1, x2, x3)  =  U8_ga(x1, x3)
geqC_out_ga(x1, x2)  =  geqC_out_ga(x1, x2)
REMA_IN_GAG(x1, x2, x3)  =  REMA_IN_GAG(x1, x3)
U1_GAG(x1, x2, x3, x4)  =  U1_GAG(x1, x3, x4)
PB_IN_GAAG(x1, x2, x3, x4)  =  PB_IN_GAAG(x1, x4)
U11_GAAG(x1, x2, x3, x4, x5)  =  U11_GAAG(x1, x4, x5)
SUBI_IN_GAA(x1, x2, x3)  =  SUBI_IN_GAA(x1)
U9_GAA(x1, x2, x3, x4)  =  U9_GAA(x1, x4)
SUBD_IN_GAA(x1, x2, x3)  =  SUBD_IN_GAA(x1)
U3_GAA(x1, x2, x3, x4)  =  U3_GAA(x1, x4)
U12_GAAG(x1, x2, x3, x4, x5)  =  U12_GAAG(x1, x2, x3, x4, x5)
REME_IN_GGG(x1, x2, x3)  =  REME_IN_GGG(x1, x2, x3)
U4_GGG(x1, x2, x3, x4)  =  U4_GGG(x1, x2, x3, x4)
PF_IN_GGAG(x1, x2, x3, x4)  =  PF_IN_GGAG(x1, x2, x4)
U13_GGAG(x1, x2, x3, x4, x5)  =  U13_GGAG(x1, x2, x4, x5)
SUBJ_IN_GGA(x1, x2, x3)  =  SUBJ_IN_GGA(x1, x2)
U10_GGA(x1, x2, x3, x4)  =  U10_GGA(x1, x2, x4)
SUBH_IN_GGA(x1, x2, x3)  =  SUBH_IN_GGA(x1, x2)
U6_GGA(x1, x2, x3, x4)  =  U6_GGA(x1, x2, x4)
U14_GGAG(x1, x2, x3, x4, x5)  =  U14_GGAG(x1, x2, x3, x4, x5)
U5_GGG(x1, x2, x3)  =  U5_GGG(x1, x2, x3)
GEQG_IN_GG(x1, x2)  =  GEQG_IN_GG(x1, x2)
U7_GG(x1, x2, x3)  =  U7_GG(x1, x2, x3)
U2_GAG(x1, x2, x3)  =  U2_GAG(x1, x3)
GEQC_IN_GA(x1, x2)  =  GEQC_IN_GA(x1)
U8_GA(x1, x2, x3)  =  U8_GA(x1, x3)

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

(4) Obligation:

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

REMA_IN_GAG(T7, s(T16), T9) → U1_GAG(T7, T16, T9, pB_in_gaag(T7, T16, X7, T9))
REMA_IN_GAG(T7, s(T16), T9) → PB_IN_GAAG(T7, T16, X7, T9)
PB_IN_GAAG(T7, T20, T19, T9) → U11_GAAG(T7, T20, T19, T9, subI_in_gaa(T7, T20, T19))
PB_IN_GAAG(T7, T20, T19, T9) → SUBI_IN_GAA(T7, T20, T19)
SUBI_IN_GAA(s(T31), T33, X40) → U9_GAA(T31, T33, X40, subD_in_gaa(T31, T33, X40))
SUBI_IN_GAA(s(T31), T33, X40) → SUBD_IN_GAA(T31, T33, X40)
SUBD_IN_GAA(s(T44), s(T46), X64) → U3_GAA(T44, T46, X64, subD_in_gaa(T44, T46, X64))
SUBD_IN_GAA(s(T44), s(T46), X64) → SUBD_IN_GAA(T44, T46, X64)
U11_GAAG(T7, T20, T19, T9, subI_out_gaa(T7, T20, T19)) → U12_GAAG(T7, T20, T19, T9, remE_in_ggg(T19, T20, T9))
U11_GAAG(T7, T20, T19, T9, subI_out_gaa(T7, T20, T19)) → REME_IN_GGG(T19, T20, T9)
REME_IN_GGG(T72, T81, T74) → U4_GGG(T72, T81, T74, pF_in_ggag(T72, T81, X102, T74))
REME_IN_GGG(T72, T81, T74) → PF_IN_GGAG(T72, T81, X102, T74)
PF_IN_GGAG(T72, T81, T84, T74) → U13_GGAG(T72, T81, T84, T74, subJ_in_gga(T72, T81, T84))
PF_IN_GGAG(T72, T81, T84, T74) → SUBJ_IN_GGA(T72, T81, T84)
SUBJ_IN_GGA(s(T95), T96, X141) → U10_GGA(T95, T96, X141, subH_in_gga(T95, T96, X141))
SUBJ_IN_GGA(s(T95), T96, X141) → SUBH_IN_GGA(T95, T96, X141)
SUBH_IN_GGA(s(T107), s(T108), X165) → U6_GGA(T107, T108, X165, subH_in_gga(T107, T108, X165))
SUBH_IN_GGA(s(T107), s(T108), X165) → SUBH_IN_GGA(T107, T108, X165)
U13_GGAG(T72, T81, T84, T74, subJ_out_gga(T72, T81, T84)) → U14_GGAG(T72, T81, T84, T74, remE_in_ggg(T84, T81, T74))
U13_GGAG(T72, T81, T84, T74, subJ_out_gga(T72, T81, T84)) → REME_IN_GGG(T84, T81, T74)
REME_IN_GGG(s(T141), T142, s(T141)) → U5_GGG(T141, T142, geqG_in_gg(T141, T142))
REME_IN_GGG(s(T141), T142, s(T141)) → GEQG_IN_GG(T141, T142)
GEQG_IN_GG(s(T153), s(T154)) → U7_GG(T153, T154, geqG_in_gg(T153, T154))
GEQG_IN_GG(s(T153), s(T154)) → GEQG_IN_GG(T153, T154)
REMA_IN_GAG(s(T184), s(T186), s(T184)) → U2_GAG(T184, T186, geqC_in_ga(T184, T186))
REMA_IN_GAG(s(T184), s(T186), s(T184)) → GEQC_IN_GA(T184, T186)
GEQC_IN_GA(s(T197), s(T199)) → U8_GA(T197, T199, geqC_in_ga(T197, T199))
GEQC_IN_GA(s(T197), s(T199)) → GEQC_IN_GA(T197, T199)

The TRS R consists of the following rules:

remA_in_gag(T7, s(T16), T9) → U1_gag(T7, T16, T9, pB_in_gaag(T7, T16, X7, T9))
pB_in_gaag(T7, T20, T19, T9) → U11_gaag(T7, T20, T19, T9, subI_in_gaa(T7, T20, T19))
subI_in_gaa(s(T31), T33, X40) → U9_gaa(T31, T33, X40, subD_in_gaa(T31, T33, X40))
subD_in_gaa(s(T44), s(T46), X64) → U3_gaa(T44, T46, X64, subD_in_gaa(T44, T46, X64))
subD_in_gaa(T51, 0, T51) → subD_out_gaa(T51, 0, T51)
U3_gaa(T44, T46, X64, subD_out_gaa(T44, T46, X64)) → subD_out_gaa(s(T44), s(T46), X64)
U9_gaa(T31, T33, X40, subD_out_gaa(T31, T33, X40)) → subI_out_gaa(s(T31), T33, X40)
U11_gaag(T7, T20, T19, T9, subI_out_gaa(T7, T20, T19)) → U12_gaag(T7, T20, T19, T9, remE_in_ggg(T19, T20, T9))
remE_in_ggg(T72, T81, T74) → U4_ggg(T72, T81, T74, pF_in_ggag(T72, T81, X102, T74))
pF_in_ggag(T72, T81, T84, T74) → U13_ggag(T72, T81, T84, T74, subJ_in_gga(T72, T81, T84))
subJ_in_gga(s(T95), T96, X141) → U10_gga(T95, T96, X141, subH_in_gga(T95, T96, X141))
subH_in_gga(s(T107), s(T108), X165) → U6_gga(T107, T108, X165, subH_in_gga(T107, T108, X165))
subH_in_gga(T113, 0, T113) → subH_out_gga(T113, 0, T113)
U6_gga(T107, T108, X165, subH_out_gga(T107, T108, X165)) → subH_out_gga(s(T107), s(T108), X165)
U10_gga(T95, T96, X141, subH_out_gga(T95, T96, X141)) → subJ_out_gga(s(T95), T96, X141)
U13_ggag(T72, T81, T84, T74, subJ_out_gga(T72, T81, T84)) → U14_ggag(T72, T81, T84, T74, remE_in_ggg(T84, T81, T74))
remE_in_ggg(s(T141), T142, s(T141)) → U5_ggg(T141, T142, geqG_in_gg(T141, T142))
geqG_in_gg(s(T153), s(T154)) → U7_gg(T153, T154, geqG_in_gg(T153, T154))
geqG_in_gg(T159, 0) → geqG_out_gg(T159, 0)
U7_gg(T153, T154, geqG_out_gg(T153, T154)) → geqG_out_gg(s(T153), s(T154))
U5_ggg(T141, T142, geqG_out_gg(T141, T142)) → remE_out_ggg(s(T141), T142, s(T141))
U14_ggag(T72, T81, T84, T74, remE_out_ggg(T84, T81, T74)) → pF_out_ggag(T72, T81, T84, T74)
U4_ggg(T72, T81, T74, pF_out_ggag(T72, T81, X102, T74)) → remE_out_ggg(T72, T81, T74)
U12_gaag(T7, T20, T19, T9, remE_out_ggg(T19, T20, T9)) → pB_out_gaag(T7, T20, T19, T9)
U1_gag(T7, T16, T9, pB_out_gaag(T7, T16, X7, T9)) → remA_out_gag(T7, s(T16), T9)
remA_in_gag(s(T184), s(T186), s(T184)) → U2_gag(T184, T186, geqC_in_ga(T184, T186))
geqC_in_ga(s(T197), s(T199)) → U8_ga(T197, T199, geqC_in_ga(T197, T199))
geqC_in_ga(T204, 0) → geqC_out_ga(T204, 0)
U8_ga(T197, T199, geqC_out_ga(T197, T199)) → geqC_out_ga(s(T197), s(T199))
U2_gag(T184, T186, geqC_out_ga(T184, T186)) → remA_out_gag(s(T184), s(T186), s(T184))

The argument filtering Pi contains the following mapping:
remA_in_gag(x1, x2, x3)  =  remA_in_gag(x1, x3)
U1_gag(x1, x2, x3, x4)  =  U1_gag(x1, x3, x4)
pB_in_gaag(x1, x2, x3, x4)  =  pB_in_gaag(x1, x4)
U11_gaag(x1, x2, x3, x4, x5)  =  U11_gaag(x1, x4, x5)
subI_in_gaa(x1, x2, x3)  =  subI_in_gaa(x1)
s(x1)  =  s(x1)
U9_gaa(x1, x2, x3, x4)  =  U9_gaa(x1, x4)
subD_in_gaa(x1, x2, x3)  =  subD_in_gaa(x1)
U3_gaa(x1, x2, x3, x4)  =  U3_gaa(x1, x4)
subD_out_gaa(x1, x2, x3)  =  subD_out_gaa(x1, x2, x3)
subI_out_gaa(x1, x2, x3)  =  subI_out_gaa(x1, x2, x3)
U12_gaag(x1, x2, x3, x4, x5)  =  U12_gaag(x1, x2, x3, x4, x5)
remE_in_ggg(x1, x2, x3)  =  remE_in_ggg(x1, x2, x3)
U4_ggg(x1, x2, x3, x4)  =  U4_ggg(x1, x2, x3, x4)
pF_in_ggag(x1, x2, x3, x4)  =  pF_in_ggag(x1, x2, x4)
U13_ggag(x1, x2, x3, x4, x5)  =  U13_ggag(x1, x2, x4, x5)
subJ_in_gga(x1, x2, x3)  =  subJ_in_gga(x1, x2)
U10_gga(x1, x2, x3, x4)  =  U10_gga(x1, x2, x4)
subH_in_gga(x1, x2, x3)  =  subH_in_gga(x1, x2)
U6_gga(x1, x2, x3, x4)  =  U6_gga(x1, x2, x4)
0  =  0
subH_out_gga(x1, x2, x3)  =  subH_out_gga(x1, x2, x3)
subJ_out_gga(x1, x2, x3)  =  subJ_out_gga(x1, x2, x3)
U14_ggag(x1, x2, x3, x4, x5)  =  U14_ggag(x1, x2, x3, x4, x5)
U5_ggg(x1, x2, x3)  =  U5_ggg(x1, x2, x3)
geqG_in_gg(x1, x2)  =  geqG_in_gg(x1, x2)
U7_gg(x1, x2, x3)  =  U7_gg(x1, x2, x3)
geqG_out_gg(x1, x2)  =  geqG_out_gg(x1, x2)
remE_out_ggg(x1, x2, x3)  =  remE_out_ggg(x1, x2, x3)
pF_out_ggag(x1, x2, x3, x4)  =  pF_out_ggag(x1, x2, x3, x4)
pB_out_gaag(x1, x2, x3, x4)  =  pB_out_gaag(x1, x2, x3, x4)
remA_out_gag(x1, x2, x3)  =  remA_out_gag(x1, x2, x3)
U2_gag(x1, x2, x3)  =  U2_gag(x1, x3)
geqC_in_ga(x1, x2)  =  geqC_in_ga(x1)
U8_ga(x1, x2, x3)  =  U8_ga(x1, x3)
geqC_out_ga(x1, x2)  =  geqC_out_ga(x1, x2)
REMA_IN_GAG(x1, x2, x3)  =  REMA_IN_GAG(x1, x3)
U1_GAG(x1, x2, x3, x4)  =  U1_GAG(x1, x3, x4)
PB_IN_GAAG(x1, x2, x3, x4)  =  PB_IN_GAAG(x1, x4)
U11_GAAG(x1, x2, x3, x4, x5)  =  U11_GAAG(x1, x4, x5)
SUBI_IN_GAA(x1, x2, x3)  =  SUBI_IN_GAA(x1)
U9_GAA(x1, x2, x3, x4)  =  U9_GAA(x1, x4)
SUBD_IN_GAA(x1, x2, x3)  =  SUBD_IN_GAA(x1)
U3_GAA(x1, x2, x3, x4)  =  U3_GAA(x1, x4)
U12_GAAG(x1, x2, x3, x4, x5)  =  U12_GAAG(x1, x2, x3, x4, x5)
REME_IN_GGG(x1, x2, x3)  =  REME_IN_GGG(x1, x2, x3)
U4_GGG(x1, x2, x3, x4)  =  U4_GGG(x1, x2, x3, x4)
PF_IN_GGAG(x1, x2, x3, x4)  =  PF_IN_GGAG(x1, x2, x4)
U13_GGAG(x1, x2, x3, x4, x5)  =  U13_GGAG(x1, x2, x4, x5)
SUBJ_IN_GGA(x1, x2, x3)  =  SUBJ_IN_GGA(x1, x2)
U10_GGA(x1, x2, x3, x4)  =  U10_GGA(x1, x2, x4)
SUBH_IN_GGA(x1, x2, x3)  =  SUBH_IN_GGA(x1, x2)
U6_GGA(x1, x2, x3, x4)  =  U6_GGA(x1, x2, x4)
U14_GGAG(x1, x2, x3, x4, x5)  =  U14_GGAG(x1, x2, x3, x4, x5)
U5_GGG(x1, x2, x3)  =  U5_GGG(x1, x2, x3)
GEQG_IN_GG(x1, x2)  =  GEQG_IN_GG(x1, x2)
U7_GG(x1, x2, x3)  =  U7_GG(x1, x2, x3)
U2_GAG(x1, x2, x3)  =  U2_GAG(x1, x3)
GEQC_IN_GA(x1, x2)  =  GEQC_IN_GA(x1)
U8_GA(x1, x2, x3)  =  U8_GA(x1, x3)

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

(5) DependencyGraphProof (EQUIVALENT transformation)

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

(6) Complex Obligation (AND)

(7) Obligation:

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

GEQC_IN_GA(s(T197), s(T199)) → GEQC_IN_GA(T197, T199)

The TRS R consists of the following rules:

remA_in_gag(T7, s(T16), T9) → U1_gag(T7, T16, T9, pB_in_gaag(T7, T16, X7, T9))
pB_in_gaag(T7, T20, T19, T9) → U11_gaag(T7, T20, T19, T9, subI_in_gaa(T7, T20, T19))
subI_in_gaa(s(T31), T33, X40) → U9_gaa(T31, T33, X40, subD_in_gaa(T31, T33, X40))
subD_in_gaa(s(T44), s(T46), X64) → U3_gaa(T44, T46, X64, subD_in_gaa(T44, T46, X64))
subD_in_gaa(T51, 0, T51) → subD_out_gaa(T51, 0, T51)
U3_gaa(T44, T46, X64, subD_out_gaa(T44, T46, X64)) → subD_out_gaa(s(T44), s(T46), X64)
U9_gaa(T31, T33, X40, subD_out_gaa(T31, T33, X40)) → subI_out_gaa(s(T31), T33, X40)
U11_gaag(T7, T20, T19, T9, subI_out_gaa(T7, T20, T19)) → U12_gaag(T7, T20, T19, T9, remE_in_ggg(T19, T20, T9))
remE_in_ggg(T72, T81, T74) → U4_ggg(T72, T81, T74, pF_in_ggag(T72, T81, X102, T74))
pF_in_ggag(T72, T81, T84, T74) → U13_ggag(T72, T81, T84, T74, subJ_in_gga(T72, T81, T84))
subJ_in_gga(s(T95), T96, X141) → U10_gga(T95, T96, X141, subH_in_gga(T95, T96, X141))
subH_in_gga(s(T107), s(T108), X165) → U6_gga(T107, T108, X165, subH_in_gga(T107, T108, X165))
subH_in_gga(T113, 0, T113) → subH_out_gga(T113, 0, T113)
U6_gga(T107, T108, X165, subH_out_gga(T107, T108, X165)) → subH_out_gga(s(T107), s(T108), X165)
U10_gga(T95, T96, X141, subH_out_gga(T95, T96, X141)) → subJ_out_gga(s(T95), T96, X141)
U13_ggag(T72, T81, T84, T74, subJ_out_gga(T72, T81, T84)) → U14_ggag(T72, T81, T84, T74, remE_in_ggg(T84, T81, T74))
remE_in_ggg(s(T141), T142, s(T141)) → U5_ggg(T141, T142, geqG_in_gg(T141, T142))
geqG_in_gg(s(T153), s(T154)) → U7_gg(T153, T154, geqG_in_gg(T153, T154))
geqG_in_gg(T159, 0) → geqG_out_gg(T159, 0)
U7_gg(T153, T154, geqG_out_gg(T153, T154)) → geqG_out_gg(s(T153), s(T154))
U5_ggg(T141, T142, geqG_out_gg(T141, T142)) → remE_out_ggg(s(T141), T142, s(T141))
U14_ggag(T72, T81, T84, T74, remE_out_ggg(T84, T81, T74)) → pF_out_ggag(T72, T81, T84, T74)
U4_ggg(T72, T81, T74, pF_out_ggag(T72, T81, X102, T74)) → remE_out_ggg(T72, T81, T74)
U12_gaag(T7, T20, T19, T9, remE_out_ggg(T19, T20, T9)) → pB_out_gaag(T7, T20, T19, T9)
U1_gag(T7, T16, T9, pB_out_gaag(T7, T16, X7, T9)) → remA_out_gag(T7, s(T16), T9)
remA_in_gag(s(T184), s(T186), s(T184)) → U2_gag(T184, T186, geqC_in_ga(T184, T186))
geqC_in_ga(s(T197), s(T199)) → U8_ga(T197, T199, geqC_in_ga(T197, T199))
geqC_in_ga(T204, 0) → geqC_out_ga(T204, 0)
U8_ga(T197, T199, geqC_out_ga(T197, T199)) → geqC_out_ga(s(T197), s(T199))
U2_gag(T184, T186, geqC_out_ga(T184, T186)) → remA_out_gag(s(T184), s(T186), s(T184))

The argument filtering Pi contains the following mapping:
remA_in_gag(x1, x2, x3)  =  remA_in_gag(x1, x3)
U1_gag(x1, x2, x3, x4)  =  U1_gag(x1, x3, x4)
pB_in_gaag(x1, x2, x3, x4)  =  pB_in_gaag(x1, x4)
U11_gaag(x1, x2, x3, x4, x5)  =  U11_gaag(x1, x4, x5)
subI_in_gaa(x1, x2, x3)  =  subI_in_gaa(x1)
s(x1)  =  s(x1)
U9_gaa(x1, x2, x3, x4)  =  U9_gaa(x1, x4)
subD_in_gaa(x1, x2, x3)  =  subD_in_gaa(x1)
U3_gaa(x1, x2, x3, x4)  =  U3_gaa(x1, x4)
subD_out_gaa(x1, x2, x3)  =  subD_out_gaa(x1, x2, x3)
subI_out_gaa(x1, x2, x3)  =  subI_out_gaa(x1, x2, x3)
U12_gaag(x1, x2, x3, x4, x5)  =  U12_gaag(x1, x2, x3, x4, x5)
remE_in_ggg(x1, x2, x3)  =  remE_in_ggg(x1, x2, x3)
U4_ggg(x1, x2, x3, x4)  =  U4_ggg(x1, x2, x3, x4)
pF_in_ggag(x1, x2, x3, x4)  =  pF_in_ggag(x1, x2, x4)
U13_ggag(x1, x2, x3, x4, x5)  =  U13_ggag(x1, x2, x4, x5)
subJ_in_gga(x1, x2, x3)  =  subJ_in_gga(x1, x2)
U10_gga(x1, x2, x3, x4)  =  U10_gga(x1, x2, x4)
subH_in_gga(x1, x2, x3)  =  subH_in_gga(x1, x2)
U6_gga(x1, x2, x3, x4)  =  U6_gga(x1, x2, x4)
0  =  0
subH_out_gga(x1, x2, x3)  =  subH_out_gga(x1, x2, x3)
subJ_out_gga(x1, x2, x3)  =  subJ_out_gga(x1, x2, x3)
U14_ggag(x1, x2, x3, x4, x5)  =  U14_ggag(x1, x2, x3, x4, x5)
U5_ggg(x1, x2, x3)  =  U5_ggg(x1, x2, x3)
geqG_in_gg(x1, x2)  =  geqG_in_gg(x1, x2)
U7_gg(x1, x2, x3)  =  U7_gg(x1, x2, x3)
geqG_out_gg(x1, x2)  =  geqG_out_gg(x1, x2)
remE_out_ggg(x1, x2, x3)  =  remE_out_ggg(x1, x2, x3)
pF_out_ggag(x1, x2, x3, x4)  =  pF_out_ggag(x1, x2, x3, x4)
pB_out_gaag(x1, x2, x3, x4)  =  pB_out_gaag(x1, x2, x3, x4)
remA_out_gag(x1, x2, x3)  =  remA_out_gag(x1, x2, x3)
U2_gag(x1, x2, x3)  =  U2_gag(x1, x3)
geqC_in_ga(x1, x2)  =  geqC_in_ga(x1)
U8_ga(x1, x2, x3)  =  U8_ga(x1, x3)
geqC_out_ga(x1, x2)  =  geqC_out_ga(x1, x2)
GEQC_IN_GA(x1, x2)  =  GEQC_IN_GA(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:

GEQC_IN_GA(s(T197), s(T199)) → GEQC_IN_GA(T197, T199)

R is empty.
The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
GEQC_IN_GA(x1, x2)  =  GEQC_IN_GA(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:

GEQC_IN_GA(s(T197)) → GEQC_IN_GA(T197)

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:

• GEQC_IN_GA(s(T197)) → GEQC_IN_GA(T197)
  The graph contains the following edges 1 > 1

(13) YES

(14) Obligation:

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

GEQG_IN_GG(s(T153), s(T154)) → GEQG_IN_GG(T153, T154)

The TRS R consists of the following rules:

remA_in_gag(T7, s(T16), T9) → U1_gag(T7, T16, T9, pB_in_gaag(T7, T16, X7, T9))
pB_in_gaag(T7, T20, T19, T9) → U11_gaag(T7, T20, T19, T9, subI_in_gaa(T7, T20, T19))
subI_in_gaa(s(T31), T33, X40) → U9_gaa(T31, T33, X40, subD_in_gaa(T31, T33, X40))
subD_in_gaa(s(T44), s(T46), X64) → U3_gaa(T44, T46, X64, subD_in_gaa(T44, T46, X64))
subD_in_gaa(T51, 0, T51) → subD_out_gaa(T51, 0, T51)
U3_gaa(T44, T46, X64, subD_out_gaa(T44, T46, X64)) → subD_out_gaa(s(T44), s(T46), X64)
U9_gaa(T31, T33, X40, subD_out_gaa(T31, T33, X40)) → subI_out_gaa(s(T31), T33, X40)
U11_gaag(T7, T20, T19, T9, subI_out_gaa(T7, T20, T19)) → U12_gaag(T7, T20, T19, T9, remE_in_ggg(T19, T20, T9))
remE_in_ggg(T72, T81, T74) → U4_ggg(T72, T81, T74, pF_in_ggag(T72, T81, X102, T74))
pF_in_ggag(T72, T81, T84, T74) → U13_ggag(T72, T81, T84, T74, subJ_in_gga(T72, T81, T84))
subJ_in_gga(s(T95), T96, X141) → U10_gga(T95, T96, X141, subH_in_gga(T95, T96, X141))
subH_in_gga(s(T107), s(T108), X165) → U6_gga(T107, T108, X165, subH_in_gga(T107, T108, X165))
subH_in_gga(T113, 0, T113) → subH_out_gga(T113, 0, T113)
U6_gga(T107, T108, X165, subH_out_gga(T107, T108, X165)) → subH_out_gga(s(T107), s(T108), X165)
U10_gga(T95, T96, X141, subH_out_gga(T95, T96, X141)) → subJ_out_gga(s(T95), T96, X141)
U13_ggag(T72, T81, T84, T74, subJ_out_gga(T72, T81, T84)) → U14_ggag(T72, T81, T84, T74, remE_in_ggg(T84, T81, T74))
remE_in_ggg(s(T141), T142, s(T141)) → U5_ggg(T141, T142, geqG_in_gg(T141, T142))
geqG_in_gg(s(T153), s(T154)) → U7_gg(T153, T154, geqG_in_gg(T153, T154))
geqG_in_gg(T159, 0) → geqG_out_gg(T159, 0)
U7_gg(T153, T154, geqG_out_gg(T153, T154)) → geqG_out_gg(s(T153), s(T154))
U5_ggg(T141, T142, geqG_out_gg(T141, T142)) → remE_out_ggg(s(T141), T142, s(T141))
U14_ggag(T72, T81, T84, T74, remE_out_ggg(T84, T81, T74)) → pF_out_ggag(T72, T81, T84, T74)
U4_ggg(T72, T81, T74, pF_out_ggag(T72, T81, X102, T74)) → remE_out_ggg(T72, T81, T74)
U12_gaag(T7, T20, T19, T9, remE_out_ggg(T19, T20, T9)) → pB_out_gaag(T7, T20, T19, T9)
U1_gag(T7, T16, T9, pB_out_gaag(T7, T16, X7, T9)) → remA_out_gag(T7, s(T16), T9)
remA_in_gag(s(T184), s(T186), s(T184)) → U2_gag(T184, T186, geqC_in_ga(T184, T186))
geqC_in_ga(s(T197), s(T199)) → U8_ga(T197, T199, geqC_in_ga(T197, T199))
geqC_in_ga(T204, 0) → geqC_out_ga(T204, 0)
U8_ga(T197, T199, geqC_out_ga(T197, T199)) → geqC_out_ga(s(T197), s(T199))
U2_gag(T184, T186, geqC_out_ga(T184, T186)) → remA_out_gag(s(T184), s(T186), s(T184))

The argument filtering Pi contains the following mapping:
remA_in_gag(x1, x2, x3)  =  remA_in_gag(x1, x3)
U1_gag(x1, x2, x3, x4)  =  U1_gag(x1, x3, x4)
pB_in_gaag(x1, x2, x3, x4)  =  pB_in_gaag(x1, x4)
U11_gaag(x1, x2, x3, x4, x5)  =  U11_gaag(x1, x4, x5)
subI_in_gaa(x1, x2, x3)  =  subI_in_gaa(x1)
s(x1)  =  s(x1)
U9_gaa(x1, x2, x3, x4)  =  U9_gaa(x1, x4)
subD_in_gaa(x1, x2, x3)  =  subD_in_gaa(x1)
U3_gaa(x1, x2, x3, x4)  =  U3_gaa(x1, x4)
subD_out_gaa(x1, x2, x3)  =  subD_out_gaa(x1, x2, x3)
subI_out_gaa(x1, x2, x3)  =  subI_out_gaa(x1, x2, x3)
U12_gaag(x1, x2, x3, x4, x5)  =  U12_gaag(x1, x2, x3, x4, x5)
remE_in_ggg(x1, x2, x3)  =  remE_in_ggg(x1, x2, x3)
U4_ggg(x1, x2, x3, x4)  =  U4_ggg(x1, x2, x3, x4)
pF_in_ggag(x1, x2, x3, x4)  =  pF_in_ggag(x1, x2, x4)
U13_ggag(x1, x2, x3, x4, x5)  =  U13_ggag(x1, x2, x4, x5)
subJ_in_gga(x1, x2, x3)  =  subJ_in_gga(x1, x2)
U10_gga(x1, x2, x3, x4)  =  U10_gga(x1, x2, x4)
subH_in_gga(x1, x2, x3)  =  subH_in_gga(x1, x2)
U6_gga(x1, x2, x3, x4)  =  U6_gga(x1, x2, x4)
0  =  0
subH_out_gga(x1, x2, x3)  =  subH_out_gga(x1, x2, x3)
subJ_out_gga(x1, x2, x3)  =  subJ_out_gga(x1, x2, x3)
U14_ggag(x1, x2, x3, x4, x5)  =  U14_ggag(x1, x2, x3, x4, x5)
U5_ggg(x1, x2, x3)  =  U5_ggg(x1, x2, x3)
geqG_in_gg(x1, x2)  =  geqG_in_gg(x1, x2)
U7_gg(x1, x2, x3)  =  U7_gg(x1, x2, x3)
geqG_out_gg(x1, x2)  =  geqG_out_gg(x1, x2)
remE_out_ggg(x1, x2, x3)  =  remE_out_ggg(x1, x2, x3)
pF_out_ggag(x1, x2, x3, x4)  =  pF_out_ggag(x1, x2, x3, x4)
pB_out_gaag(x1, x2, x3, x4)  =  pB_out_gaag(x1, x2, x3, x4)
remA_out_gag(x1, x2, x3)  =  remA_out_gag(x1, x2, x3)
U2_gag(x1, x2, x3)  =  U2_gag(x1, x3)
geqC_in_ga(x1, x2)  =  geqC_in_ga(x1)
U8_ga(x1, x2, x3)  =  U8_ga(x1, x3)
geqC_out_ga(x1, x2)  =  geqC_out_ga(x1, x2)
GEQG_IN_GG(x1, x2)  =  GEQG_IN_GG(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:

GEQG_IN_GG(s(T153), s(T154)) → GEQG_IN_GG(T153, T154)

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

(17) PiDPToQDPProof (EQUIVALENT transformation)

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

(18) Obligation:

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

GEQG_IN_GG(s(T153), s(T154)) → GEQG_IN_GG(T153, T154)

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

(19) QDPSizeChangeProof (EQUIVALENT transformation)

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

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

• GEQG_IN_GG(s(T153), s(T154)) → GEQG_IN_GG(T153, T154)
  The graph contains the following edges 1 > 1, 2 > 2

(20) YES

(21) Obligation:

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

SUBH_IN_GGA(s(T107), s(T108), X165) → SUBH_IN_GGA(T107, T108, X165)

The TRS R consists of the following rules:

remA_in_gag(T7, s(T16), T9) → U1_gag(T7, T16, T9, pB_in_gaag(T7, T16, X7, T9))
pB_in_gaag(T7, T20, T19, T9) → U11_gaag(T7, T20, T19, T9, subI_in_gaa(T7, T20, T19))
subI_in_gaa(s(T31), T33, X40) → U9_gaa(T31, T33, X40, subD_in_gaa(T31, T33, X40))
subD_in_gaa(s(T44), s(T46), X64) → U3_gaa(T44, T46, X64, subD_in_gaa(T44, T46, X64))
subD_in_gaa(T51, 0, T51) → subD_out_gaa(T51, 0, T51)
U3_gaa(T44, T46, X64, subD_out_gaa(T44, T46, X64)) → subD_out_gaa(s(T44), s(T46), X64)
U9_gaa(T31, T33, X40, subD_out_gaa(T31, T33, X40)) → subI_out_gaa(s(T31), T33, X40)
U11_gaag(T7, T20, T19, T9, subI_out_gaa(T7, T20, T19)) → U12_gaag(T7, T20, T19, T9, remE_in_ggg(T19, T20, T9))
remE_in_ggg(T72, T81, T74) → U4_ggg(T72, T81, T74, pF_in_ggag(T72, T81, X102, T74))
pF_in_ggag(T72, T81, T84, T74) → U13_ggag(T72, T81, T84, T74, subJ_in_gga(T72, T81, T84))
subJ_in_gga(s(T95), T96, X141) → U10_gga(T95, T96, X141, subH_in_gga(T95, T96, X141))
subH_in_gga(s(T107), s(T108), X165) → U6_gga(T107, T108, X165, subH_in_gga(T107, T108, X165))
subH_in_gga(T113, 0, T113) → subH_out_gga(T113, 0, T113)
U6_gga(T107, T108, X165, subH_out_gga(T107, T108, X165)) → subH_out_gga(s(T107), s(T108), X165)
U10_gga(T95, T96, X141, subH_out_gga(T95, T96, X141)) → subJ_out_gga(s(T95), T96, X141)
U13_ggag(T72, T81, T84, T74, subJ_out_gga(T72, T81, T84)) → U14_ggag(T72, T81, T84, T74, remE_in_ggg(T84, T81, T74))
remE_in_ggg(s(T141), T142, s(T141)) → U5_ggg(T141, T142, geqG_in_gg(T141, T142))
geqG_in_gg(s(T153), s(T154)) → U7_gg(T153, T154, geqG_in_gg(T153, T154))
geqG_in_gg(T159, 0) → geqG_out_gg(T159, 0)
U7_gg(T153, T154, geqG_out_gg(T153, T154)) → geqG_out_gg(s(T153), s(T154))
U5_ggg(T141, T142, geqG_out_gg(T141, T142)) → remE_out_ggg(s(T141), T142, s(T141))
U14_ggag(T72, T81, T84, T74, remE_out_ggg(T84, T81, T74)) → pF_out_ggag(T72, T81, T84, T74)
U4_ggg(T72, T81, T74, pF_out_ggag(T72, T81, X102, T74)) → remE_out_ggg(T72, T81, T74)
U12_gaag(T7, T20, T19, T9, remE_out_ggg(T19, T20, T9)) → pB_out_gaag(T7, T20, T19, T9)
U1_gag(T7, T16, T9, pB_out_gaag(T7, T16, X7, T9)) → remA_out_gag(T7, s(T16), T9)
remA_in_gag(s(T184), s(T186), s(T184)) → U2_gag(T184, T186, geqC_in_ga(T184, T186))
geqC_in_ga(s(T197), s(T199)) → U8_ga(T197, T199, geqC_in_ga(T197, T199))
geqC_in_ga(T204, 0) → geqC_out_ga(T204, 0)
U8_ga(T197, T199, geqC_out_ga(T197, T199)) → geqC_out_ga(s(T197), s(T199))
U2_gag(T184, T186, geqC_out_ga(T184, T186)) → remA_out_gag(s(T184), s(T186), s(T184))

The argument filtering Pi contains the following mapping:
remA_in_gag(x1, x2, x3)  =  remA_in_gag(x1, x3)
U1_gag(x1, x2, x3, x4)  =  U1_gag(x1, x3, x4)
pB_in_gaag(x1, x2, x3, x4)  =  pB_in_gaag(x1, x4)
U11_gaag(x1, x2, x3, x4, x5)  =  U11_gaag(x1, x4, x5)
subI_in_gaa(x1, x2, x3)  =  subI_in_gaa(x1)
s(x1)  =  s(x1)
U9_gaa(x1, x2, x3, x4)  =  U9_gaa(x1, x4)
subD_in_gaa(x1, x2, x3)  =  subD_in_gaa(x1)
U3_gaa(x1, x2, x3, x4)  =  U3_gaa(x1, x4)
subD_out_gaa(x1, x2, x3)  =  subD_out_gaa(x1, x2, x3)
subI_out_gaa(x1, x2, x3)  =  subI_out_gaa(x1, x2, x3)
U12_gaag(x1, x2, x3, x4, x5)  =  U12_gaag(x1, x2, x3, x4, x5)
remE_in_ggg(x1, x2, x3)  =  remE_in_ggg(x1, x2, x3)
U4_ggg(x1, x2, x3, x4)  =  U4_ggg(x1, x2, x3, x4)
pF_in_ggag(x1, x2, x3, x4)  =  pF_in_ggag(x1, x2, x4)
U13_ggag(x1, x2, x3, x4, x5)  =  U13_ggag(x1, x2, x4, x5)
subJ_in_gga(x1, x2, x3)  =  subJ_in_gga(x1, x2)
U10_gga(x1, x2, x3, x4)  =  U10_gga(x1, x2, x4)
subH_in_gga(x1, x2, x3)  =  subH_in_gga(x1, x2)
U6_gga(x1, x2, x3, x4)  =  U6_gga(x1, x2, x4)
0  =  0
subH_out_gga(x1, x2, x3)  =  subH_out_gga(x1, x2, x3)
subJ_out_gga(x1, x2, x3)  =  subJ_out_gga(x1, x2, x3)
U14_ggag(x1, x2, x3, x4, x5)  =  U14_ggag(x1, x2, x3, x4, x5)
U5_ggg(x1, x2, x3)  =  U5_ggg(x1, x2, x3)
geqG_in_gg(x1, x2)  =  geqG_in_gg(x1, x2)
U7_gg(x1, x2, x3)  =  U7_gg(x1, x2, x3)
geqG_out_gg(x1, x2)  =  geqG_out_gg(x1, x2)
remE_out_ggg(x1, x2, x3)  =  remE_out_ggg(x1, x2, x3)
pF_out_ggag(x1, x2, x3, x4)  =  pF_out_ggag(x1, x2, x3, x4)
pB_out_gaag(x1, x2, x3, x4)  =  pB_out_gaag(x1, x2, x3, x4)
remA_out_gag(x1, x2, x3)  =  remA_out_gag(x1, x2, x3)
U2_gag(x1, x2, x3)  =  U2_gag(x1, x3)
geqC_in_ga(x1, x2)  =  geqC_in_ga(x1)
U8_ga(x1, x2, x3)  =  U8_ga(x1, x3)
geqC_out_ga(x1, x2)  =  geqC_out_ga(x1, x2)
SUBH_IN_GGA(x1, x2, x3)  =  SUBH_IN_GGA(x1, x2)

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:

SUBH_IN_GGA(s(T107), s(T108), X165) → SUBH_IN_GGA(T107, T108, X165)

R is empty.
The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
SUBH_IN_GGA(x1, x2, x3)  =  SUBH_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:

SUBH_IN_GGA(s(T107), s(T108)) → SUBH_IN_GGA(T107, T108)

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:

• SUBH_IN_GGA(s(T107), s(T108)) → SUBH_IN_GGA(T107, T108)
  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:

REME_IN_GGG(T72, T81, T74) → PF_IN_GGAG(T72, T81, X102, T74)
PF_IN_GGAG(T72, T81, T84, T74) → U13_GGAG(T72, T81, T84, T74, subJ_in_gga(T72, T81, T84))
U13_GGAG(T72, T81, T84, T74, subJ_out_gga(T72, T81, T84)) → REME_IN_GGG(T84, T81, T74)

The TRS R consists of the following rules:

remA_in_gag(T7, s(T16), T9) → U1_gag(T7, T16, T9, pB_in_gaag(T7, T16, X7, T9))
pB_in_gaag(T7, T20, T19, T9) → U11_gaag(T7, T20, T19, T9, subI_in_gaa(T7, T20, T19))
subI_in_gaa(s(T31), T33, X40) → U9_gaa(T31, T33, X40, subD_in_gaa(T31, T33, X40))
subD_in_gaa(s(T44), s(T46), X64) → U3_gaa(T44, T46, X64, subD_in_gaa(T44, T46, X64))
subD_in_gaa(T51, 0, T51) → subD_out_gaa(T51, 0, T51)
U3_gaa(T44, T46, X64, subD_out_gaa(T44, T46, X64)) → subD_out_gaa(s(T44), s(T46), X64)
U9_gaa(T31, T33, X40, subD_out_gaa(T31, T33, X40)) → subI_out_gaa(s(T31), T33, X40)
U11_gaag(T7, T20, T19, T9, subI_out_gaa(T7, T20, T19)) → U12_gaag(T7, T20, T19, T9, remE_in_ggg(T19, T20, T9))
remE_in_ggg(T72, T81, T74) → U4_ggg(T72, T81, T74, pF_in_ggag(T72, T81, X102, T74))
pF_in_ggag(T72, T81, T84, T74) → U13_ggag(T72, T81, T84, T74, subJ_in_gga(T72, T81, T84))
subJ_in_gga(s(T95), T96, X141) → U10_gga(T95, T96, X141, subH_in_gga(T95, T96, X141))
subH_in_gga(s(T107), s(T108), X165) → U6_gga(T107, T108, X165, subH_in_gga(T107, T108, X165))
subH_in_gga(T113, 0, T113) → subH_out_gga(T113, 0, T113)
U6_gga(T107, T108, X165, subH_out_gga(T107, T108, X165)) → subH_out_gga(s(T107), s(T108), X165)
U10_gga(T95, T96, X141, subH_out_gga(T95, T96, X141)) → subJ_out_gga(s(T95), T96, X141)
U13_ggag(T72, T81, T84, T74, subJ_out_gga(T72, T81, T84)) → U14_ggag(T72, T81, T84, T74, remE_in_ggg(T84, T81, T74))
remE_in_ggg(s(T141), T142, s(T141)) → U5_ggg(T141, T142, geqG_in_gg(T141, T142))
geqG_in_gg(s(T153), s(T154)) → U7_gg(T153, T154, geqG_in_gg(T153, T154))
geqG_in_gg(T159, 0) → geqG_out_gg(T159, 0)
U7_gg(T153, T154, geqG_out_gg(T153, T154)) → geqG_out_gg(s(T153), s(T154))
U5_ggg(T141, T142, geqG_out_gg(T141, T142)) → remE_out_ggg(s(T141), T142, s(T141))
U14_ggag(T72, T81, T84, T74, remE_out_ggg(T84, T81, T74)) → pF_out_ggag(T72, T81, T84, T74)
U4_ggg(T72, T81, T74, pF_out_ggag(T72, T81, X102, T74)) → remE_out_ggg(T72, T81, T74)
U12_gaag(T7, T20, T19, T9, remE_out_ggg(T19, T20, T9)) → pB_out_gaag(T7, T20, T19, T9)
U1_gag(T7, T16, T9, pB_out_gaag(T7, T16, X7, T9)) → remA_out_gag(T7, s(T16), T9)
remA_in_gag(s(T184), s(T186), s(T184)) → U2_gag(T184, T186, geqC_in_ga(T184, T186))
geqC_in_ga(s(T197), s(T199)) → U8_ga(T197, T199, geqC_in_ga(T197, T199))
geqC_in_ga(T204, 0) → geqC_out_ga(T204, 0)
U8_ga(T197, T199, geqC_out_ga(T197, T199)) → geqC_out_ga(s(T197), s(T199))
U2_gag(T184, T186, geqC_out_ga(T184, T186)) → remA_out_gag(s(T184), s(T186), s(T184))

The argument filtering Pi contains the following mapping:
remA_in_gag(x1, x2, x3)  =  remA_in_gag(x1, x3)
U1_gag(x1, x2, x3, x4)  =  U1_gag(x1, x3, x4)
pB_in_gaag(x1, x2, x3, x4)  =  pB_in_gaag(x1, x4)
U11_gaag(x1, x2, x3, x4, x5)  =  U11_gaag(x1, x4, x5)
subI_in_gaa(x1, x2, x3)  =  subI_in_gaa(x1)
s(x1)  =  s(x1)
U9_gaa(x1, x2, x3, x4)  =  U9_gaa(x1, x4)
subD_in_gaa(x1, x2, x3)  =  subD_in_gaa(x1)
U3_gaa(x1, x2, x3, x4)  =  U3_gaa(x1, x4)
subD_out_gaa(x1, x2, x3)  =  subD_out_gaa(x1, x2, x3)
subI_out_gaa(x1, x2, x3)  =  subI_out_gaa(x1, x2, x3)
U12_gaag(x1, x2, x3, x4, x5)  =  U12_gaag(x1, x2, x3, x4, x5)
remE_in_ggg(x1, x2, x3)  =  remE_in_ggg(x1, x2, x3)
U4_ggg(x1, x2, x3, x4)  =  U4_ggg(x1, x2, x3, x4)
pF_in_ggag(x1, x2, x3, x4)  =  pF_in_ggag(x1, x2, x4)
U13_ggag(x1, x2, x3, x4, x5)  =  U13_ggag(x1, x2, x4, x5)
subJ_in_gga(x1, x2, x3)  =  subJ_in_gga(x1, x2)
U10_gga(x1, x2, x3, x4)  =  U10_gga(x1, x2, x4)
subH_in_gga(x1, x2, x3)  =  subH_in_gga(x1, x2)
U6_gga(x1, x2, x3, x4)  =  U6_gga(x1, x2, x4)
0  =  0
subH_out_gga(x1, x2, x3)  =  subH_out_gga(x1, x2, x3)
subJ_out_gga(x1, x2, x3)  =  subJ_out_gga(x1, x2, x3)
U14_ggag(x1, x2, x3, x4, x5)  =  U14_ggag(x1, x2, x3, x4, x5)
U5_ggg(x1, x2, x3)  =  U5_ggg(x1, x2, x3)
geqG_in_gg(x1, x2)  =  geqG_in_gg(x1, x2)
U7_gg(x1, x2, x3)  =  U7_gg(x1, x2, x3)
geqG_out_gg(x1, x2)  =  geqG_out_gg(x1, x2)
remE_out_ggg(x1, x2, x3)  =  remE_out_ggg(x1, x2, x3)
pF_out_ggag(x1, x2, x3, x4)  =  pF_out_ggag(x1, x2, x3, x4)
pB_out_gaag(x1, x2, x3, x4)  =  pB_out_gaag(x1, x2, x3, x4)
remA_out_gag(x1, x2, x3)  =  remA_out_gag(x1, x2, x3)
U2_gag(x1, x2, x3)  =  U2_gag(x1, x3)
geqC_in_ga(x1, x2)  =  geqC_in_ga(x1)
U8_ga(x1, x2, x3)  =  U8_ga(x1, x3)
geqC_out_ga(x1, x2)  =  geqC_out_ga(x1, x2)
REME_IN_GGG(x1, x2, x3)  =  REME_IN_GGG(x1, x2, x3)
PF_IN_GGAG(x1, x2, x3, x4)  =  PF_IN_GGAG(x1, x2, x4)
U13_GGAG(x1, x2, x3, x4, x5)  =  U13_GGAG(x1, x2, x4, x5)

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

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

REME_IN_GGG(T72, T81, T74) → PF_IN_GGAG(T72, T81, X102, T74)
PF_IN_GGAG(T72, T81, T84, T74) → U13_GGAG(T72, T81, T84, T74, subJ_in_gga(T72, T81, T84))
U13_GGAG(T72, T81, T84, T74, subJ_out_gga(T72, T81, T84)) → REME_IN_GGG(T84, T81, T74)

The TRS R consists of the following rules:

subJ_in_gga(s(T95), T96, X141) → U10_gga(T95, T96, X141, subH_in_gga(T95, T96, X141))
U10_gga(T95, T96, X141, subH_out_gga(T95, T96, X141)) → subJ_out_gga(s(T95), T96, X141)
subH_in_gga(s(T107), s(T108), X165) → U6_gga(T107, T108, X165, subH_in_gga(T107, T108, X165))
subH_in_gga(T113, 0, T113) → subH_out_gga(T113, 0, T113)
U6_gga(T107, T108, X165, subH_out_gga(T107, T108, X165)) → subH_out_gga(s(T107), s(T108), X165)

The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
subJ_in_gga(x1, x2, x3)  =  subJ_in_gga(x1, x2)
U10_gga(x1, x2, x3, x4)  =  U10_gga(x1, x2, x4)
subH_in_gga(x1, x2, x3)  =  subH_in_gga(x1, x2)
U6_gga(x1, x2, x3, x4)  =  U6_gga(x1, x2, x4)
0  =  0
subH_out_gga(x1, x2, x3)  =  subH_out_gga(x1, x2, x3)
subJ_out_gga(x1, x2, x3)  =  subJ_out_gga(x1, x2, x3)
REME_IN_GGG(x1, x2, x3)  =  REME_IN_GGG(x1, x2, x3)
PF_IN_GGAG(x1, x2, x3, x4)  =  PF_IN_GGAG(x1, x2, x4)
U13_GGAG(x1, x2, x3, x4, x5)  =  U13_GGAG(x1, x2, x4, x5)

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:

REME_IN_GGG(T72, T81, T74) → PF_IN_GGAG(T72, T81, T74)
PF_IN_GGAG(T72, T81, T74) → U13_GGAG(T72, T81, T74, subJ_in_gga(T72, T81))
U13_GGAG(T72, T81, T74, subJ_out_gga(T72, T81, T84)) → REME_IN_GGG(T84, T81, T74)

The TRS R consists of the following rules:

subJ_in_gga(s(T95), T96) → U10_gga(T95, T96, subH_in_gga(T95, T96))
U10_gga(T95, T96, subH_out_gga(T95, T96, X141)) → subJ_out_gga(s(T95), T96, X141)
subH_in_gga(s(T107), s(T108)) → U6_gga(T107, T108, subH_in_gga(T107, T108))
subH_in_gga(T113, 0) → subH_out_gga(T113, 0, T113)
U6_gga(T107, T108, subH_out_gga(T107, T108, X165)) → subH_out_gga(s(T107), s(T108), X165)

The set Q consists of the following terms:

subJ_in_gga(x0, x1)
U10_gga(x0, x1, x2)
subH_in_gga(x0, x1)
U6_gga(x0, x1, x2)

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

(33) QDPOrderProof (EQUIVALENT transformation)

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

The following pairs can be oriented strictly and are deleted.

PF_IN_GGAG(T72, T81, T74) → U13_GGAG(T72, T81, T74, subJ_in_gga(T72, T81))

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

POL(0) = 0   
POL(PF_IN_GGAG(x₁, x₂, x₃)) = 1 + x₁   
POL(REME_IN_GGG(x₁, x₂, x₃)) = 1 + x₁   
POL(U10_gga(x₁, x₂, x₃)) = 1 + x₃   
POL(U13_GGAG(x₁, x₂, x₃, x₄)) = x₄   
POL(U6_gga(x₁, x₂, x₃)) = 1 + x₃   
POL(s(x₁)) = 1 + x₁   
POL(subH_in_gga(x₁, x₂)) = x₁   
POL(subH_out_gga(x₁, x₂, x₃)) = x₃   
POL(subJ_in_gga(x₁, x₂)) = x₁   
POL(subJ_out_gga(x₁, x₂, x₃)) = 1 + x₃   

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

subJ_in_gga(s(T95), T96) → U10_gga(T95, T96, subH_in_gga(T95, T96))
subH_in_gga(s(T107), s(T108)) → U6_gga(T107, T108, subH_in_gga(T107, T108))
subH_in_gga(T113, 0) → subH_out_gga(T113, 0, T113)
U10_gga(T95, T96, subH_out_gga(T95, T96, X141)) → subJ_out_gga(s(T95), T96, X141)
U6_gga(T107, T108, subH_out_gga(T107, T108, X165)) → subH_out_gga(s(T107), s(T108), X165)

(34) Obligation:

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

REME_IN_GGG(T72, T81, T74) → PF_IN_GGAG(T72, T81, T74)
U13_GGAG(T72, T81, T74, subJ_out_gga(T72, T81, T84)) → REME_IN_GGG(T84, T81, T74)

The TRS R consists of the following rules:

subJ_in_gga(s(T95), T96) → U10_gga(T95, T96, subH_in_gga(T95, T96))
U10_gga(T95, T96, subH_out_gga(T95, T96, X141)) → subJ_out_gga(s(T95), T96, X141)
subH_in_gga(s(T107), s(T108)) → U6_gga(T107, T108, subH_in_gga(T107, T108))
subH_in_gga(T113, 0) → subH_out_gga(T113, 0, T113)
U6_gga(T107, T108, subH_out_gga(T107, T108, X165)) → subH_out_gga(s(T107), s(T108), X165)

The set Q consists of the following terms:

subJ_in_gga(x0, x1)
U10_gga(x0, x1, x2)
subH_in_gga(x0, x1)
U6_gga(x0, x1, x2)

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

(35) DependencyGraphProof (EQUIVALENT transformation)

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

(36) TRUE

(37) Obligation:

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

SUBD_IN_GAA(s(T44), s(T46), X64) → SUBD_IN_GAA(T44, T46, X64)

The TRS R consists of the following rules:

remA_in_gag(T7, s(T16), T9) → U1_gag(T7, T16, T9, pB_in_gaag(T7, T16, X7, T9))
pB_in_gaag(T7, T20, T19, T9) → U11_gaag(T7, T20, T19, T9, subI_in_gaa(T7, T20, T19))
subI_in_gaa(s(T31), T33, X40) → U9_gaa(T31, T33, X40, subD_in_gaa(T31, T33, X40))
subD_in_gaa(s(T44), s(T46), X64) → U3_gaa(T44, T46, X64, subD_in_gaa(T44, T46, X64))
subD_in_gaa(T51, 0, T51) → subD_out_gaa(T51, 0, T51)
U3_gaa(T44, T46, X64, subD_out_gaa(T44, T46, X64)) → subD_out_gaa(s(T44), s(T46), X64)
U9_gaa(T31, T33, X40, subD_out_gaa(T31, T33, X40)) → subI_out_gaa(s(T31), T33, X40)
U11_gaag(T7, T20, T19, T9, subI_out_gaa(T7, T20, T19)) → U12_gaag(T7, T20, T19, T9, remE_in_ggg(T19, T20, T9))
remE_in_ggg(T72, T81, T74) → U4_ggg(T72, T81, T74, pF_in_ggag(T72, T81, X102, T74))
pF_in_ggag(T72, T81, T84, T74) → U13_ggag(T72, T81, T84, T74, subJ_in_gga(T72, T81, T84))
subJ_in_gga(s(T95), T96, X141) → U10_gga(T95, T96, X141, subH_in_gga(T95, T96, X141))
subH_in_gga(s(T107), s(T108), X165) → U6_gga(T107, T108, X165, subH_in_gga(T107, T108, X165))
subH_in_gga(T113, 0, T113) → subH_out_gga(T113, 0, T113)
U6_gga(T107, T108, X165, subH_out_gga(T107, T108, X165)) → subH_out_gga(s(T107), s(T108), X165)
U10_gga(T95, T96, X141, subH_out_gga(T95, T96, X141)) → subJ_out_gga(s(T95), T96, X141)
U13_ggag(T72, T81, T84, T74, subJ_out_gga(T72, T81, T84)) → U14_ggag(T72, T81, T84, T74, remE_in_ggg(T84, T81, T74))
remE_in_ggg(s(T141), T142, s(T141)) → U5_ggg(T141, T142, geqG_in_gg(T141, T142))
geqG_in_gg(s(T153), s(T154)) → U7_gg(T153, T154, geqG_in_gg(T153, T154))
geqG_in_gg(T159, 0) → geqG_out_gg(T159, 0)
U7_gg(T153, T154, geqG_out_gg(T153, T154)) → geqG_out_gg(s(T153), s(T154))
U5_ggg(T141, T142, geqG_out_gg(T141, T142)) → remE_out_ggg(s(T141), T142, s(T141))
U14_ggag(T72, T81, T84, T74, remE_out_ggg(T84, T81, T74)) → pF_out_ggag(T72, T81, T84, T74)
U4_ggg(T72, T81, T74, pF_out_ggag(T72, T81, X102, T74)) → remE_out_ggg(T72, T81, T74)
U12_gaag(T7, T20, T19, T9, remE_out_ggg(T19, T20, T9)) → pB_out_gaag(T7, T20, T19, T9)
U1_gag(T7, T16, T9, pB_out_gaag(T7, T16, X7, T9)) → remA_out_gag(T7, s(T16), T9)
remA_in_gag(s(T184), s(T186), s(T184)) → U2_gag(T184, T186, geqC_in_ga(T184, T186))
geqC_in_ga(s(T197), s(T199)) → U8_ga(T197, T199, geqC_in_ga(T197, T199))
geqC_in_ga(T204, 0) → geqC_out_ga(T204, 0)
U8_ga(T197, T199, geqC_out_ga(T197, T199)) → geqC_out_ga(s(T197), s(T199))
U2_gag(T184, T186, geqC_out_ga(T184, T186)) → remA_out_gag(s(T184), s(T186), s(T184))

The argument filtering Pi contains the following mapping:
remA_in_gag(x1, x2, x3)  =  remA_in_gag(x1, x3)
U1_gag(x1, x2, x3, x4)  =  U1_gag(x1, x3, x4)
pB_in_gaag(x1, x2, x3, x4)  =  pB_in_gaag(x1, x4)
U11_gaag(x1, x2, x3, x4, x5)  =  U11_gaag(x1, x4, x5)
subI_in_gaa(x1, x2, x3)  =  subI_in_gaa(x1)
s(x1)  =  s(x1)
U9_gaa(x1, x2, x3, x4)  =  U9_gaa(x1, x4)
subD_in_gaa(x1, x2, x3)  =  subD_in_gaa(x1)
U3_gaa(x1, x2, x3, x4)  =  U3_gaa(x1, x4)
subD_out_gaa(x1, x2, x3)  =  subD_out_gaa(x1, x2, x3)
subI_out_gaa(x1, x2, x3)  =  subI_out_gaa(x1, x2, x3)
U12_gaag(x1, x2, x3, x4, x5)  =  U12_gaag(x1, x2, x3, x4, x5)
remE_in_ggg(x1, x2, x3)  =  remE_in_ggg(x1, x2, x3)
U4_ggg(x1, x2, x3, x4)  =  U4_ggg(x1, x2, x3, x4)
pF_in_ggag(x1, x2, x3, x4)  =  pF_in_ggag(x1, x2, x4)
U13_ggag(x1, x2, x3, x4, x5)  =  U13_ggag(x1, x2, x4, x5)
subJ_in_gga(x1, x2, x3)  =  subJ_in_gga(x1, x2)
U10_gga(x1, x2, x3, x4)  =  U10_gga(x1, x2, x4)
subH_in_gga(x1, x2, x3)  =  subH_in_gga(x1, x2)
U6_gga(x1, x2, x3, x4)  =  U6_gga(x1, x2, x4)
0  =  0
subH_out_gga(x1, x2, x3)  =  subH_out_gga(x1, x2, x3)
subJ_out_gga(x1, x2, x3)  =  subJ_out_gga(x1, x2, x3)
U14_ggag(x1, x2, x3, x4, x5)  =  U14_ggag(x1, x2, x3, x4, x5)
U5_ggg(x1, x2, x3)  =  U5_ggg(x1, x2, x3)
geqG_in_gg(x1, x2)  =  geqG_in_gg(x1, x2)
U7_gg(x1, x2, x3)  =  U7_gg(x1, x2, x3)
geqG_out_gg(x1, x2)  =  geqG_out_gg(x1, x2)
remE_out_ggg(x1, x2, x3)  =  remE_out_ggg(x1, x2, x3)
pF_out_ggag(x1, x2, x3, x4)  =  pF_out_ggag(x1, x2, x3, x4)
pB_out_gaag(x1, x2, x3, x4)  =  pB_out_gaag(x1, x2, x3, x4)
remA_out_gag(x1, x2, x3)  =  remA_out_gag(x1, x2, x3)
U2_gag(x1, x2, x3)  =  U2_gag(x1, x3)
geqC_in_ga(x1, x2)  =  geqC_in_ga(x1)
U8_ga(x1, x2, x3)  =  U8_ga(x1, x3)
geqC_out_ga(x1, x2)  =  geqC_out_ga(x1, x2)
SUBD_IN_GAA(x1, x2, x3)  =  SUBD_IN_GAA(x1)

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

(38) UsableRulesProof (EQUIVALENT transformation)

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

(39) Obligation:

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

SUBD_IN_GAA(s(T44), s(T46), X64) → SUBD_IN_GAA(T44, T46, X64)

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

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

(40) PiDPToQDPProof (SOUND transformation)

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

(41) Obligation:

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

SUBD_IN_GAA(s(T44)) → SUBD_IN_GAA(T44)

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

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

• SUBD_IN_GAA(s(T44)) → SUBD_IN_GAA(T44)
  The graph contains the following edges 1 > 1

(43) YES