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

(0) Obligation:

Clauses:

isNat(s(X)) :- isNat(X).
isNat(0).
notEq(s(X), s(Y)) :- notEq(X, Y).
notEq(s(X), 0).
notEq(0, s(X)).
lt(s(X), s(Y)) :- lt(X, Y).
lt(0, s(Y)).
gt(s(X), s(Y)) :- gt(X, Y).
gt(s(X), 0).
le(s(X), s(Y)) :- le(X, Y).
le(0, s(Y)).
le(0, 0).
even(s(X)) :- odd(X).
even(0).
odd(s(X)) :- even(X).
odd(s(0)).
add(s(X), Y, s(Z)) :- add(X, Y, Z).
add(0, X, X).
mult(s(X), Y, R) :- ','(mult(X, Y, Z), add(Y, Z, R)).
mult(0, Y, 0).
factorial(s(X), R) :- ','(factorial(X, Y), mult(s(X), Y, R)).
factorial(0, s(0)).

Query: factorial(g,a)

(1) PrologToPiTRSViaGraphTransformerProof (SOUND transformation)

Transformed Prolog program to (Pi-)TRS.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
3 [label="A: factorial(T1, T2)\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
5 [label="5: factorial(T1, T2), SCOPE: 1, CLAUSE: 20 | factorial(T1, T2), SCOPE: 1, CLAUSE: 21\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
10 [label="10: ','(factorial(T5, X5), mult(s(T5), X5, T7)) | factorial(s(T5), T2), SCOPE: 1, CLAUSE: 21\n\nT5 is ground\nX5 is free", fontsize=16, style=filled, fillcolor=lightyellow];
12 [label="12: factorial(T1, T2), SCOPE: 1, CLAUSE: 21\n\nT1 is ground\nX3 is free\nX4 is free\nfactorial(T1, T2) !=? factorial(s(X3), X4)", fontsize=16, style=filled, fillcolor=lightyellow];
16 [label="16: ','(factorial(T5, X5), mult(s(T5), X5, T7)), SCOPE: 2, CLAUSE: 20 | ','(factorial(T5, X5), mult(s(T5), X5, T7)), SCOPE: 2, CLAUSE: 21 | ?_2 | factorial(s(T5), T2), SCOPE: 1, CLAUSE: 21\n\nT5 is ground\nX5 is free", fontsize=16, style=filled, fillcolor=lightyellow];
19 [label="19: ','(factorial(T5, X5), mult(s(T5), X5, T7)), SCOPE: 2, CLAUSE: 20\n\nT5 is ground\nX5 is free", fontsize=16, style=filled, fillcolor=lightyellow];
20 [label="20: ','(factorial(T5, X5), mult(s(T5), X5, T7)), SCOPE: 2, CLAUSE: 21 | ?_2 | factorial(s(T5), T2), SCOPE: 1, CLAUSE: 21\n\nT5 is ground\nX5 is free", fontsize=16, style=filled, fillcolor=lightyellow];
23 [label="B: ','(','(factorial(T12, X22), mult(s(T12), X22, X23)), mult(s(s(T12)), X23, T7))\n\nT12 is ground\nX23 is free\nX22 is free", fontsize=16, style=filled, fillcolor=lightyellow];
24 [label="24: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
34 [label="D: factorial(T12, X22)\n\nT12 is ground\nX22 is free", fontsize=16, style=filled, fillcolor=lightyellow];
35 [label="O: ','(mult(s(T12), T14, X23), mult(s(s(T12)), X23, T7))\n\nT12 is ground\nT14 is ground\nX23 is free", fontsize=16, style=filled, fillcolor=lightyellow];
38 [label="38: factorial(T12, X22), SCOPE: 3, CLAUSE: 20 | factorial(T12, X22), SCOPE: 3, CLAUSE: 21\n\nT12 is ground\nX22 is free", fontsize=16, style=filled, fillcolor=lightyellow];
45 [label="45: factorial(T12, X22), SCOPE: 3, CLAUSE: 20\n\nT12 is ground\nX22 is free", fontsize=16, style=filled, fillcolor=lightyellow];
46 [label="46: factorial(T12, X22), SCOPE: 3, CLAUSE: 21\n\nT12 is ground\nX22 is free", fontsize=16, style=filled, fillcolor=lightyellow];
49 [label="E: ','(factorial(T20, X48), mult(s(T20), X48, X49))\n\nT20 is ground\nX49 is free\nX48 is free", fontsize=16, style=filled, fillcolor=lightyellow];
50 [label="50: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
51 [label="51: factorial(T20, X48)\n\nT20 is ground\nX48 is free", fontsize=16, style=filled, fillcolor=lightyellow];
52 [label="G: mult(s(T20), T22, X49)\n\nT20 is ground\nT22 is ground\nX49 is free", fontsize=16, style=filled, fillcolor=lightyellow];
60 [label="60: mult(s(T20), T22, X49), SCOPE: 4, CLAUSE: 18 | mult(s(T20), T22, X49), SCOPE: 4, CLAUSE: 19\n\nT20 is ground\nT22 is ground\nX49 is free", fontsize=16, style=filled, fillcolor=lightyellow];
67 [label="67: mult(s(T20), T22, X49), SCOPE: 4, CLAUSE: 18\n\nT20 is ground\nT22 is ground\nX49 is free", fontsize=16, style=filled, fillcolor=lightyellow];
68 [label="68: mult(s(T20), T22, X49), SCOPE: 4, CLAUSE: 19\n\nT20 is ground\nT22 is ground\nX49 is free", fontsize=16, style=filled, fillcolor=lightyellow];
72 [label="H: ','(mult(T38, T39, X94), add(T39, X94, X95))\n\nT38 is ground\nT39 is ground\nX95 is free\nX94 is free", fontsize=16, style=filled, fillcolor=lightyellow];
86 [label="L: mult(T38, T39, X94)\n\nT38 is ground\nT39 is ground\nX94 is free", fontsize=16, style=filled, fillcolor=lightyellow];
88 [label="F: add(T39, T42, X95)\n\nT39 is ground\nT42 is ground\nX95 is free", fontsize=16, style=filled, fillcolor=lightyellow];
92 [label="92: mult(T38, T39, X94), SCOPE: 5, CLAUSE: 18 | mult(T38, T39, X94), SCOPE: 5, CLAUSE: 19\n\nT38 is ground\nT39 is ground\nX94 is free", fontsize=16, style=filled, fillcolor=lightyellow];
95 [label="95: mult(T38, T39, X94), SCOPE: 5, CLAUSE: 18\n\nT38 is ground\nT39 is ground\nX94 is free", fontsize=16, style=filled, fillcolor=lightyellow];
97 [label="97: mult(T38, T39, X94), SCOPE: 5, CLAUSE: 19\n\nT38 is ground\nT39 is ground\nX94 is free", fontsize=16, style=filled, fillcolor=lightyellow];
105 [label="105: ','(mult(T53, T54, X127), add(T54, X127, X128))\n\nT53 is ground\nT54 is ground\nX128 is free\nX127 is free", fontsize=16, style=filled, fillcolor=lightyellow];
107 [label="107: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
112 [label="112: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
113 [label="113: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
114 [label="114: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
118 [label="118: add(T39, T42, X95), SCOPE: 6, CLAUSE: 16 | add(T39, T42, X95), SCOPE: 6, CLAUSE: 17\n\nT39 is ground\nT42 is ground\nX95 is free", fontsize=16, style=filled, fillcolor=lightyellow];
132 [label="132: add(T39, T42, X95), SCOPE: 6, CLAUSE: 16\n\nT39 is ground\nT42 is ground\nX95 is free", fontsize=16, style=filled, fillcolor=lightyellow];
133 [label="133: add(T39, T42, X95), SCOPE: 6, CLAUSE: 17\n\nT39 is ground\nT42 is ground\nX95 is free", fontsize=16, style=filled, fillcolor=lightyellow];
138 [label="138: add(T70, T71, X160)\n\nT70 is ground\nT71 is ground\nX160 is free", fontsize=16, style=filled, fillcolor=lightyellow];
139 [label="139: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
143 [label="143: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
145 [label="145: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
147 [label="147: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
148 [label="148: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
152 [label="152: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
153 [label="153: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
154 [label="154: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
162 [label="162: mult(s(T12), T14, X23)\n\nT12 is ground\nT14 is ground\nX23 is free", fontsize=16, style=filled, fillcolor=lightyellow];
163 [label="J: mult(s(s(T12)), T79, T7)\n\nT12 is ground\nT79 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
167 [label="167: mult(s(s(T12)), T79, T7), SCOPE: 7, CLAUSE: 18 | mult(s(s(T12)), T79, T7), SCOPE: 7, CLAUSE: 19\n\nT12 is ground\nT79 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
185 [label="185: mult(s(s(T12)), T79, T7), SCOPE: 7, CLAUSE: 18\n\nT12 is ground\nT79 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
186 [label="186: mult(s(s(T12)), T79, T7), SCOPE: 7, CLAUSE: 19\n\nT12 is ground\nT79 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
192 [label="K: ','(mult(s(T103), T104, X210), add(T104, X210, T106))\n\nT103 is ground\nT104 is ground\nX210 is free", fontsize=16, style=filled, fillcolor=lightyellow];
195 [label="195: mult(s(T103), T104, X210)\n\nT103 is ground\nT104 is ground\nX210 is free", fontsize=16, style=filled, fillcolor=lightyellow];
196 [label="I: add(T104, T109, T106)\n\nT104 is ground\nT109 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
204 [label="204: add(T104, T109, T106), SCOPE: 8, CLAUSE: 16 | add(T104, T109, T106), SCOPE: 8, CLAUSE: 17\n\nT104 is ground\nT109 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
205 [label="205: add(T104, T109, T106), SCOPE: 8, CLAUSE: 16\n\nT104 is ground\nT109 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
206 [label="206: add(T104, T109, T106), SCOPE: 8, CLAUSE: 17\n\nT104 is ground\nT109 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
207 [label="207: add(T127, T128, T130)\n\nT127 is ground\nT128 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
208 [label="208: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
209 [label="209: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
210 [label="210: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
211 [label="211: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
212 [label="212: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
213 [label="213: ','(factorial(T5, X5), mult(s(T5), X5, T7)), SCOPE: 2, CLAUSE: 21\n\nT5 is ground\nX5 is free", fontsize=16, style=filled, fillcolor=lightyellow];
214 [label="214: ?_2 | factorial(s(T5), T2), SCOPE: 1, CLAUSE: 21\n\nT5 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
215 [label="215: mult(s(0), s(0), T7)\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
216 [label="216: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
217 [label="217: mult(s(0), s(0), T7), SCOPE: 9, CLAUSE: 18 | mult(s(0), s(0), T7), SCOPE: 9, CLAUSE: 19\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
218 [label="218: mult(s(0), s(0), T7), SCOPE: 9, CLAUSE: 18\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
219 [label="219: mult(s(0), s(0), T7), SCOPE: 9, CLAUSE: 19\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
220 [label="C: ','(mult(0, s(0), X275), add(s(0), X275, T145))\n\nX275 is free", fontsize=16, style=filled, fillcolor=lightyellow];
221 [label="M: mult(0, s(0), X275)\n\nX275 is free", fontsize=16, style=filled, fillcolor=lightyellow];
222 [label="N: add(s(0), T146, T145)\n\nT146 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
223 [label="223: mult(0, s(0), X275), SCOPE: 10, CLAUSE: 18 | mult(0, s(0), X275), SCOPE: 10, CLAUSE: 19\n\nX275 is free", fontsize=16, style=filled, fillcolor=lightyellow];
224 [label="224: mult(0, s(0), X275), SCOPE: 10, CLAUSE: 19\n\nX275 is free", fontsize=16, style=filled, fillcolor=lightyellow];
225 [label="225: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
226 [label="226: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
227 [label="227: add(s(0), T146, T145), SCOPE: 11, CLAUSE: 16 | add(s(0), T146, T145), SCOPE: 11, CLAUSE: 17\n\nT146 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
228 [label="228: add(s(0), T146, T145), SCOPE: 11, CLAUSE: 16\n\nT146 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
229 [label="229: add(s(0), T146, T145), SCOPE: 11, CLAUSE: 17\n\nT146 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
230 [label="230: add(0, T157, T159)\n\nT157 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
231 [label="231: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
232 [label="232: add(0, T157, T159), SCOPE: 12, CLAUSE: 16 | add(0, T157, T159), SCOPE: 12, CLAUSE: 17\n\nT157 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
233 [label="233: add(0, T157, T159), SCOPE: 12, CLAUSE: 17\n\nT157 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
234 [label="234: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
235 [label="235: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
236 [label="236: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
237 [label="237: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
238 [label="238: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
239 [label="239: factorial(s(T5), T2), SCOPE: 1, CLAUSE: 21\n\nT5 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
240 [label="240: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
241 [label="241: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
242 [label="242: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
243 [label="243: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
244 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
3 -> 244 [arrowhead = none ];
244 -> 5;

245 [label="EVAL with clause\nfactorial(s(X3), X4) :- ','(factorial(X3, X5), mult(s(X3), X5, X4)).\nand substitutionX3 -> T5,\nT1 -> s(T5),\nT2 -> T7,\nX4 -> T7,\nT6 -> T7", fontsize=14, style = filled, fillcolor = lightblue];
5 -> 245 [arrowhead = none ];
245 -> 10;

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

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

248 [label="EVAL with clause\nfactorial(0, s(0)).\nand substitutionT1 -> 0,\nT2 -> s(0)", fontsize=14, style = filled, fillcolor = lightblue];
12 -> 248 [arrowhead = none ];
248 -> 241;

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

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

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

252 [label="EVAL with clause\nfactorial(s(X20), X21) :- ','(factorial(X20, X22), mult(s(X20), X22, X21)).\nand substitutionX20 -> T12,\nT5 -> s(T12),\nX5 -> X23,\nX21 -> X23", fontsize=14, style = filled, fillcolor = lightblue];
19 -> 252 [arrowhead = none ];
252 -> 23;

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

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

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

256 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
23 -> 256 [arrowhead = none ];
256 -> 34;

257 [label="SPLIT 2\nnew knowledge:\nT12 is ground\nT14 is ground\nreplacements:X22 -> T14", fontsize=14, style = filled, fillcolor = violet];
23 -> 257 [arrowhead = none ];
257 -> 35;

258 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
34 -> 258 [arrowhead = none ];
258 -> 38;

259 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
35 -> 259 [arrowhead = none ];
259 -> 162;

260 [label="SPLIT 2\nnew knowledge:\nT12 is ground\nT14 is ground\nT79 is ground\nreplacements:X23 -> T79", fontsize=14, style = filled, fillcolor = violet];
35 -> 260 [arrowhead = none ];
260 -> 163;

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

262 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
38 -> 262 [arrowhead = none ];
262 -> 46;

263 [label="EVAL with clause\nfactorial(s(X46), X47) :- ','(factorial(X46, X48), mult(s(X46), X48, X47)).\nand substitutionX46 -> T20,\nT12 -> s(T20),\nX22 -> X49,\nX47 -> X49", fontsize=14, style = filled, fillcolor = lightblue];
45 -> 263 [arrowhead = none ];
263 -> 49;

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

265 [label="EVAL with clause\nfactorial(0, s(0)).\nand substitutionT12 -> 0,\nX22 -> s(0)", fontsize=14, style = filled, fillcolor = lightblue];
46 -> 265 [arrowhead = none ];
265 -> 152;

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

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

268 [label="SPLIT 2\nnew knowledge:\nT20 is ground\nT22 is ground\nreplacements:X48 -> T22", fontsize=14, style = filled, fillcolor = violet];
49 -> 268 [arrowhead = none ];
268 -> 52;

269 [label="INSTANCE with matching:\nT12 -> T20\nX22 -> X48", fontsize=14, style = filled, fillcolor = lightgrey];
51 -> 269 [arrowhead = none , style=dashed];
269 -> 34[style=dashed];

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

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

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

273 [label="ONLY EVAL with clause\nmult(s(X91), X92, X93) :- ','(mult(X91, X92, X94), add(X92, X94, X93)).\nand substitutionT20 -> T38,\nX91 -> T38,\nT22 -> T39,\nX92 -> T39,\nX49 -> X95,\nX93 -> X95", fontsize=14, style = filled, fillcolor = lightblue];
67 -> 273 [arrowhead = none ];
273 -> 72;

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

275 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
72 -> 275 [arrowhead = none ];
275 -> 86;

276 [label="SPLIT 2\nnew knowledge:\nT38 is ground\nT39 is ground\nT42 is ground\nreplacements:X94 -> T42", fontsize=14, style = filled, fillcolor = violet];
72 -> 276 [arrowhead = none ];
276 -> 88;

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

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

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

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

281 [label="EVAL with clause\nmult(s(X124), X125, X126) :- ','(mult(X124, X125, X127), add(X125, X127, X126)).\nand substitutionX124 -> T53,\nT38 -> s(T53),\nT39 -> T54,\nX125 -> T54,\nX94 -> X128,\nX126 -> X128", fontsize=14, style = filled, fillcolor = lightblue];
95 -> 281 [arrowhead = none ];
281 -> 105;

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

283 [label="EVAL with clause\nmult(0, X136, 0).\nand substitutionT38 -> 0,\nT39 -> T59,\nX136 -> T59,\nX94 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
97 -> 283 [arrowhead = none ];
283 -> 112;

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

285 [label="INSTANCE with matching:\nT38 -> T53\nT39 -> T54\nX94 -> X127\nX95 -> X128", fontsize=14, style = filled, fillcolor = lightgrey];
105 -> 285 [arrowhead = none , style=dashed];
285 -> 72[style=dashed];

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

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

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

289 [label="EVAL with clause\nadd(s(X157), X158, s(X159)) :- add(X157, X158, X159).\nand substitutionX157 -> T70,\nT39 -> s(T70),\nT42 -> T71,\nX158 -> T71,\nX159 -> X160,\nX95 -> s(X160)", fontsize=14, style = filled, fillcolor = lightblue];
132 -> 289 [arrowhead = none ];
289 -> 138;

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

291 [label="EVAL with clause\nadd(0, X167, X167).\nand substitutionT39 -> 0,\nT42 -> T76,\nX167 -> T76,\nX95 -> T76", fontsize=14, style = filled, fillcolor = lightblue];
133 -> 291 [arrowhead = none ];
291 -> 143;

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

293 [label="INSTANCE with matching:\nT39 -> T70\nT42 -> T71\nX95 -> X160", fontsize=14, style = filled, fillcolor = lightgrey];
138 -> 293 [arrowhead = none , style=dashed];
293 -> 88[style=dashed];

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

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

296 [label="INSTANCE with matching:\nT20 -> T12\nT22 -> T14\nX49 -> X23", fontsize=14, style = filled, fillcolor = lightgrey];
162 -> 296 [arrowhead = none , style=dashed];
296 -> 52[style=dashed];

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

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

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

300 [label="ONLY EVAL with clause\nmult(s(X207), X208, X209) :- ','(mult(X207, X208, X210), add(X208, X210, X209)).\nand substitutionT12 -> T103,\nX207 -> s(T103),\nT79 -> T104,\nX208 -> T104,\nT7 -> T106,\nX209 -> T106,\nT105 -> T106", fontsize=14, style = filled, fillcolor = lightblue];
185 -> 300 [arrowhead = none ];
300 -> 192;

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

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

303 [label="SPLIT 2\nnew knowledge:\nT103 is ground\nT104 is ground\nT109 is ground\nreplacements:X210 -> T109", fontsize=14, style = filled, fillcolor = violet];
192 -> 303 [arrowhead = none ];
303 -> 196;

304 [label="INSTANCE with matching:\nT20 -> T103\nT22 -> T104\nX49 -> X210", fontsize=14, style = filled, fillcolor = lightgrey];
195 -> 304 [arrowhead = none , style=dashed];
304 -> 52[style=dashed];

305 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
196 -> 305 [arrowhead = none ];
305 -> 204;

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

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

308 [label="EVAL with clause\nadd(s(X236), X237, s(X238)) :- add(X236, X237, X238).\nand substitutionX236 -> T127,\nT104 -> s(T127),\nT109 -> T128,\nX237 -> T128,\nX238 -> T130,\nT106 -> s(T130),\nT129 -> T130", fontsize=14, style = filled, fillcolor = lightblue];
205 -> 308 [arrowhead = none ];
308 -> 207;

309 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
205 -> 309 [arrowhead = none ];
309 -> 208;

310 [label="EVAL with clause\nadd(0, X244, X244).\nand substitutionT104 -> 0,\nT109 -> T136,\nX244 -> T136,\nT106 -> T136", fontsize=14, style = filled, fillcolor = lightblue];
206 -> 310 [arrowhead = none ];
310 -> 209;

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

312 [label="INSTANCE with matching:\nT104 -> T127\nT109 -> T128\nT106 -> T130", fontsize=14, style = filled, fillcolor = lightgrey];
207 -> 312 [arrowhead = none , style=dashed];
312 -> 196[style=dashed];

313 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
209 -> 313 [arrowhead = none ];
313 -> 211;

314 [label="EVAL with clause\nfactorial(0, s(0)).\nand substitutionT5 -> 0,\nX5 -> s(0)", fontsize=14, style = filled, fillcolor = lightblue];
213 -> 314 [arrowhead = none ];
314 -> 215;

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

316 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
214 -> 316 [arrowhead = none ];
316 -> 239;

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

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

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

320 [label="ONLY EVAL with clause\nmult(s(X272), X273, X274) :- ','(mult(X272, X273, X275), add(X273, X275, X274)).\nand substitutionX272 -> 0,\nX273 -> s(0),\nT7 -> T145,\nX274 -> T145,\nT144 -> T145", fontsize=14, style = filled, fillcolor = lightblue];
218 -> 320 [arrowhead = none ];
320 -> 220;

321 [label="BACKTRACK\nfor clause: mult(0, Y, 0)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
219 -> 321 [arrowhead = none ];
321 -> 238;

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

323 [label="SPLIT 2\nnew knowledge:\nT146 is ground\nreplacements:X275 -> T146", fontsize=14, style = filled, fillcolor = violet];
220 -> 323 [arrowhead = none ];
323 -> 222;

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

325 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
222 -> 325 [arrowhead = none ];
325 -> 227;

326 [label="BACKTRACK\nfor clause: mult(s(X), Y, R) :- ','(mult(X, Y, Z), add(Y, Z, R))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
223 -> 326 [arrowhead = none ];
326 -> 224;

327 [label="ONLY EVAL with clause\nmult(0, X289, 0).\nand substitutionX289 -> s(0),\nX275 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
224 -> 327 [arrowhead = none ];
327 -> 225;

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

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

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

331 [label="EVAL with clause\nadd(s(X305), X306, s(X307)) :- add(X305, X306, X307).\nand substitutionX305 -> 0,\nT146 -> T157,\nX306 -> T157,\nX307 -> T159,\nT145 -> s(T159),\nT158 -> T159", fontsize=14, style = filled, fillcolor = lightblue];
228 -> 331 [arrowhead = none ];
331 -> 230;

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

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

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

335 [label="BACKTRACK\nfor clause: add(s(X), Y, s(Z)) :- add(X, Y, Z)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
232 -> 335 [arrowhead = none ];
335 -> 233;

336 [label="EVAL with clause\nadd(0, X316, X316).\nand substitutionT157 -> T162,\nX316 -> T162,\nT159 -> T162", fontsize=14, style = filled, fillcolor = lightblue];
233 -> 336 [arrowhead = none ];
336 -> 234;

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

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

339 [label="BACKTRACK\nfor clause: factorial(0, s(0))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
239 -> 339 [arrowhead = none ];
339 -> 240;

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

}

(2) Obligation:

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

factorialA_in_ga(s(s(T12)), T7) → U1_ga(T12, T7, pB_in_gaaa(T12, X22, X23, T7))
pB_in_gaaa(T12, T14, X23, T7) → U9_gaaa(T12, T14, X23, T7, factorialD_in_ga(T12, T14))
factorialD_in_ga(s(T20), X49) → U3_ga(T20, X49, pE_in_gaa(T20, X48, X49))
pE_in_gaa(T20, T22, X49) → U13_gaa(T20, T22, X49, factorialD_in_ga(T20, T22))
factorialD_in_ga(0, s(0)) → factorialD_out_ga(0, s(0))
U13_gaa(T20, T22, X49, factorialD_out_ga(T20, T22)) → U14_gaa(T20, T22, X49, multG_in_gga(T20, T22, X49))
multG_in_gga(T38, T39, X95) → U5_gga(T38, T39, X95, pH_in_ggaa(T38, T39, X94, X95))
pH_in_ggaa(T38, T39, T42, X95) → U15_ggaa(T38, T39, T42, X95, multL_in_gga(T38, T39, T42))
multL_in_gga(s(T53), T54, X128) → U8_gga(T53, T54, X128, pH_in_ggaa(T53, T54, X127, X128))
U8_gga(T53, T54, X128, pH_out_ggaa(T53, T54, X127, X128)) → multL_out_gga(s(T53), T54, X128)
multL_in_gga(0, T59, 0) → multL_out_gga(0, T59, 0)
U15_ggaa(T38, T39, T42, X95, multL_out_gga(T38, T39, T42)) → U16_ggaa(T38, T39, T42, X95, addF_in_gga(T39, T42, X95))
addF_in_gga(s(T70), T71, s(X160)) → U4_gga(T70, T71, X160, addF_in_gga(T70, T71, X160))
addF_in_gga(0, T76, T76) → addF_out_gga(0, T76, T76)
U4_gga(T70, T71, X160, addF_out_gga(T70, T71, X160)) → addF_out_gga(s(T70), T71, s(X160))
U16_ggaa(T38, T39, T42, X95, addF_out_gga(T39, T42, X95)) → pH_out_ggaa(T38, T39, T42, X95)
U5_gga(T38, T39, X95, pH_out_ggaa(T38, T39, X94, X95)) → multG_out_gga(T38, T39, X95)
U14_gaa(T20, T22, X49, multG_out_gga(T20, T22, X49)) → pE_out_gaa(T20, T22, X49)
U3_ga(T20, X49, pE_out_gaa(T20, X48, X49)) → factorialD_out_ga(s(T20), X49)
U9_gaaa(T12, T14, X23, T7, factorialD_out_ga(T12, T14)) → U10_gaaa(T12, T14, X23, T7, pO_in_ggaa(T12, T14, X23, T7))
pO_in_ggaa(T12, T14, T79, T7) → U11_ggaa(T12, T14, T79, T7, multG_in_gga(T12, T14, T79))
U11_ggaa(T12, T14, T79, T7, multG_out_gga(T12, T14, T79)) → U12_ggaa(T12, T14, T79, T7, multJ_in_gga(T12, T79, T7))
multJ_in_gga(T103, T104, T106) → U7_gga(T103, T104, T106, pK_in_ggaa(T103, T104, X210, T106))
pK_in_ggaa(T103, T104, T109, T106) → U17_ggaa(T103, T104, T109, T106, multG_in_gga(T103, T104, T109))
U17_ggaa(T103, T104, T109, T106, multG_out_gga(T103, T104, T109)) → U18_ggaa(T103, T104, T109, T106, addI_in_gga(T104, T109, T106))
addI_in_gga(s(T127), T128, s(T130)) → U6_gga(T127, T128, T130, addI_in_gga(T127, T128, T130))
addI_in_gga(0, T136, T136) → addI_out_gga(0, T136, T136)
U6_gga(T127, T128, T130, addI_out_gga(T127, T128, T130)) → addI_out_gga(s(T127), T128, s(T130))
U18_ggaa(T103, T104, T109, T106, addI_out_gga(T104, T109, T106)) → pK_out_ggaa(T103, T104, T109, T106)
U7_gga(T103, T104, T106, pK_out_ggaa(T103, T104, X210, T106)) → multJ_out_gga(T103, T104, T106)
U12_ggaa(T12, T14, T79, T7, multJ_out_gga(T12, T79, T7)) → pO_out_ggaa(T12, T14, T79, T7)
U10_gaaa(T12, T14, X23, T7, pO_out_ggaa(T12, T14, X23, T7)) → pB_out_gaaa(T12, T14, X23, T7)
U1_ga(T12, T7, pB_out_gaaa(T12, X22, X23, T7)) → factorialA_out_ga(s(s(T12)), T7)
factorialA_in_ga(s(0), T145) → U2_ga(T145, pC_in_aa(X275, T145))
pC_in_aa(T146, T145) → U19_aa(T146, T145, multM_in_a(T146))
multM_in_a(0) → multM_out_a(0)
U19_aa(T146, T145, multM_out_a(T146)) → U20_aa(T146, T145, addN_in_ga(T146, T145))
addN_in_ga(T162, s(T162)) → addN_out_ga(T162, s(T162))
U20_aa(T146, T145, addN_out_ga(T146, T145)) → pC_out_aa(T146, T145)
U2_ga(T145, pC_out_aa(X275, T145)) → factorialA_out_ga(s(0), T145)
factorialA_in_ga(0, s(0)) → factorialA_out_ga(0, s(0))

The argument filtering Pi contains the following mapping:
factorialA_in_ga(x1, x2)  =  factorialA_in_ga(x1)
s(x1)  =  s(x1)
U1_ga(x1, x2, x3)  =  U1_ga(x1, x3)
pB_in_gaaa(x1, x2, x3, x4)  =  pB_in_gaaa(x1)
U9_gaaa(x1, x2, x3, x4, x5)  =  U9_gaaa(x1, x5)
factorialD_in_ga(x1, x2)  =  factorialD_in_ga(x1)
U3_ga(x1, x2, x3)  =  U3_ga(x1, x3)
pE_in_gaa(x1, x2, x3)  =  pE_in_gaa(x1)
U13_gaa(x1, x2, x3, x4)  =  U13_gaa(x1, x4)
0  =  0
factorialD_out_ga(x1, x2)  =  factorialD_out_ga(x1, x2)
U14_gaa(x1, x2, x3, x4)  =  U14_gaa(x1, x2, x4)
multG_in_gga(x1, x2, x3)  =  multG_in_gga(x1, x2)
U5_gga(x1, x2, x3, x4)  =  U5_gga(x1, x2, x4)
pH_in_ggaa(x1, x2, x3, x4)  =  pH_in_ggaa(x1, x2)
U15_ggaa(x1, x2, x3, x4, x5)  =  U15_ggaa(x1, x2, x5)
multL_in_gga(x1, x2, x3)  =  multL_in_gga(x1, x2)
U8_gga(x1, x2, x3, x4)  =  U8_gga(x1, x2, x4)
pH_out_ggaa(x1, x2, x3, x4)  =  pH_out_ggaa(x1, x2, x3, x4)
multL_out_gga(x1, x2, x3)  =  multL_out_gga(x1, x2, x3)
U16_ggaa(x1, x2, x3, x4, x5)  =  U16_ggaa(x1, x2, x3, x5)
addF_in_gga(x1, x2, x3)  =  addF_in_gga(x1, x2)
U4_gga(x1, x2, x3, x4)  =  U4_gga(x1, x2, x4)
addF_out_gga(x1, x2, x3)  =  addF_out_gga(x1, x2, x3)
multG_out_gga(x1, x2, x3)  =  multG_out_gga(x1, x2, x3)
pE_out_gaa(x1, x2, x3)  =  pE_out_gaa(x1, x2, x3)
U10_gaaa(x1, x2, x3, x4, x5)  =  U10_gaaa(x1, x2, x5)
pO_in_ggaa(x1, x2, x3, x4)  =  pO_in_ggaa(x1, x2)
U11_ggaa(x1, x2, x3, x4, x5)  =  U11_ggaa(x1, x2, x5)
U12_ggaa(x1, x2, x3, x4, x5)  =  U12_ggaa(x1, x2, x3, x5)
multJ_in_gga(x1, x2, x3)  =  multJ_in_gga(x1, x2)
U7_gga(x1, x2, x3, x4)  =  U7_gga(x1, x2, x4)
pK_in_ggaa(x1, x2, x3, x4)  =  pK_in_ggaa(x1, x2)
U17_ggaa(x1, x2, x3, x4, x5)  =  U17_ggaa(x1, x2, x5)
U18_ggaa(x1, x2, x3, x4, x5)  =  U18_ggaa(x1, x2, x3, x5)
addI_in_gga(x1, x2, x3)  =  addI_in_gga(x1, x2)
U6_gga(x1, x2, x3, x4)  =  U6_gga(x1, x2, x4)
addI_out_gga(x1, x2, x3)  =  addI_out_gga(x1, x2, x3)
pK_out_ggaa(x1, x2, x3, x4)  =  pK_out_ggaa(x1, x2, x3, x4)
multJ_out_gga(x1, x2, x3)  =  multJ_out_gga(x1, x2, x3)
pO_out_ggaa(x1, x2, x3, x4)  =  pO_out_ggaa(x1, x2, x3, x4)
pB_out_gaaa(x1, x2, x3, x4)  =  pB_out_gaaa(x1, x2, x3, x4)
factorialA_out_ga(x1, x2)  =  factorialA_out_ga(x1, x2)
U2_ga(x1, x2)  =  U2_ga(x2)
pC_in_aa(x1, x2)  =  pC_in_aa
U19_aa(x1, x2, x3)  =  U19_aa(x3)
multM_in_a(x1)  =  multM_in_a
multM_out_a(x1)  =  multM_out_a(x1)
U20_aa(x1, x2, x3)  =  U20_aa(x1, x3)
addN_in_ga(x1, x2)  =  addN_in_ga(x1)
addN_out_ga(x1, x2)  =  addN_out_ga(x1, x2)
pC_out_aa(x1, x2)  =  pC_out_aa(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:

FACTORIALA_IN_GA(s(s(T12)), T7) → U1_GA(T12, T7, pB_in_gaaa(T12, X22, X23, T7))
FACTORIALA_IN_GA(s(s(T12)), T7) → PB_IN_GAAA(T12, X22, X23, T7)
PB_IN_GAAA(T12, T14, X23, T7) → U9_GAAA(T12, T14, X23, T7, factorialD_in_ga(T12, T14))
PB_IN_GAAA(T12, T14, X23, T7) → FACTORIALD_IN_GA(T12, T14)
FACTORIALD_IN_GA(s(T20), X49) → U3_GA(T20, X49, pE_in_gaa(T20, X48, X49))
FACTORIALD_IN_GA(s(T20), X49) → PE_IN_GAA(T20, X48, X49)
PE_IN_GAA(T20, T22, X49) → U13_GAA(T20, T22, X49, factorialD_in_ga(T20, T22))
PE_IN_GAA(T20, T22, X49) → FACTORIALD_IN_GA(T20, T22)
U13_GAA(T20, T22, X49, factorialD_out_ga(T20, T22)) → U14_GAA(T20, T22, X49, multG_in_gga(T20, T22, X49))
U13_GAA(T20, T22, X49, factorialD_out_ga(T20, T22)) → MULTG_IN_GGA(T20, T22, X49)
MULTG_IN_GGA(T38, T39, X95) → U5_GGA(T38, T39, X95, pH_in_ggaa(T38, T39, X94, X95))
MULTG_IN_GGA(T38, T39, X95) → PH_IN_GGAA(T38, T39, X94, X95)
PH_IN_GGAA(T38, T39, T42, X95) → U15_GGAA(T38, T39, T42, X95, multL_in_gga(T38, T39, T42))
PH_IN_GGAA(T38, T39, T42, X95) → MULTL_IN_GGA(T38, T39, T42)
MULTL_IN_GGA(s(T53), T54, X128) → U8_GGA(T53, T54, X128, pH_in_ggaa(T53, T54, X127, X128))
MULTL_IN_GGA(s(T53), T54, X128) → PH_IN_GGAA(T53, T54, X127, X128)
U15_GGAA(T38, T39, T42, X95, multL_out_gga(T38, T39, T42)) → U16_GGAA(T38, T39, T42, X95, addF_in_gga(T39, T42, X95))
U15_GGAA(T38, T39, T42, X95, multL_out_gga(T38, T39, T42)) → ADDF_IN_GGA(T39, T42, X95)
ADDF_IN_GGA(s(T70), T71, s(X160)) → U4_GGA(T70, T71, X160, addF_in_gga(T70, T71, X160))
ADDF_IN_GGA(s(T70), T71, s(X160)) → ADDF_IN_GGA(T70, T71, X160)
U9_GAAA(T12, T14, X23, T7, factorialD_out_ga(T12, T14)) → U10_GAAA(T12, T14, X23, T7, pO_in_ggaa(T12, T14, X23, T7))
U9_GAAA(T12, T14, X23, T7, factorialD_out_ga(T12, T14)) → PO_IN_GGAA(T12, T14, X23, T7)
PO_IN_GGAA(T12, T14, T79, T7) → U11_GGAA(T12, T14, T79, T7, multG_in_gga(T12, T14, T79))
PO_IN_GGAA(T12, T14, T79, T7) → MULTG_IN_GGA(T12, T14, T79)
U11_GGAA(T12, T14, T79, T7, multG_out_gga(T12, T14, T79)) → U12_GGAA(T12, T14, T79, T7, multJ_in_gga(T12, T79, T7))
U11_GGAA(T12, T14, T79, T7, multG_out_gga(T12, T14, T79)) → MULTJ_IN_GGA(T12, T79, T7)
MULTJ_IN_GGA(T103, T104, T106) → U7_GGA(T103, T104, T106, pK_in_ggaa(T103, T104, X210, T106))
MULTJ_IN_GGA(T103, T104, T106) → PK_IN_GGAA(T103, T104, X210, T106)
PK_IN_GGAA(T103, T104, T109, T106) → U17_GGAA(T103, T104, T109, T106, multG_in_gga(T103, T104, T109))
PK_IN_GGAA(T103, T104, T109, T106) → MULTG_IN_GGA(T103, T104, T109)
U17_GGAA(T103, T104, T109, T106, multG_out_gga(T103, T104, T109)) → U18_GGAA(T103, T104, T109, T106, addI_in_gga(T104, T109, T106))
U17_GGAA(T103, T104, T109, T106, multG_out_gga(T103, T104, T109)) → ADDI_IN_GGA(T104, T109, T106)
ADDI_IN_GGA(s(T127), T128, s(T130)) → U6_GGA(T127, T128, T130, addI_in_gga(T127, T128, T130))
ADDI_IN_GGA(s(T127), T128, s(T130)) → ADDI_IN_GGA(T127, T128, T130)
FACTORIALA_IN_GA(s(0), T145) → U2_GA(T145, pC_in_aa(X275, T145))
FACTORIALA_IN_GA(s(0), T145) → PC_IN_AA(X275, T145)
PC_IN_AA(T146, T145) → U19_AA(T146, T145, multM_in_a(T146))
PC_IN_AA(T146, T145) → MULTM_IN_A(T146)
U19_AA(T146, T145, multM_out_a(T146)) → U20_AA(T146, T145, addN_in_ga(T146, T145))
U19_AA(T146, T145, multM_out_a(T146)) → ADDN_IN_GA(T146, T145)

The TRS R consists of the following rules:

factorialA_in_ga(s(s(T12)), T7) → U1_ga(T12, T7, pB_in_gaaa(T12, X22, X23, T7))
pB_in_gaaa(T12, T14, X23, T7) → U9_gaaa(T12, T14, X23, T7, factorialD_in_ga(T12, T14))
factorialD_in_ga(s(T20), X49) → U3_ga(T20, X49, pE_in_gaa(T20, X48, X49))
pE_in_gaa(T20, T22, X49) → U13_gaa(T20, T22, X49, factorialD_in_ga(T20, T22))
factorialD_in_ga(0, s(0)) → factorialD_out_ga(0, s(0))
U13_gaa(T20, T22, X49, factorialD_out_ga(T20, T22)) → U14_gaa(T20, T22, X49, multG_in_gga(T20, T22, X49))
multG_in_gga(T38, T39, X95) → U5_gga(T38, T39, X95, pH_in_ggaa(T38, T39, X94, X95))
pH_in_ggaa(T38, T39, T42, X95) → U15_ggaa(T38, T39, T42, X95, multL_in_gga(T38, T39, T42))
multL_in_gga(s(T53), T54, X128) → U8_gga(T53, T54, X128, pH_in_ggaa(T53, T54, X127, X128))
U8_gga(T53, T54, X128, pH_out_ggaa(T53, T54, X127, X128)) → multL_out_gga(s(T53), T54, X128)
multL_in_gga(0, T59, 0) → multL_out_gga(0, T59, 0)
U15_ggaa(T38, T39, T42, X95, multL_out_gga(T38, T39, T42)) → U16_ggaa(T38, T39, T42, X95, addF_in_gga(T39, T42, X95))
addF_in_gga(s(T70), T71, s(X160)) → U4_gga(T70, T71, X160, addF_in_gga(T70, T71, X160))
addF_in_gga(0, T76, T76) → addF_out_gga(0, T76, T76)
U4_gga(T70, T71, X160, addF_out_gga(T70, T71, X160)) → addF_out_gga(s(T70), T71, s(X160))
U16_ggaa(T38, T39, T42, X95, addF_out_gga(T39, T42, X95)) → pH_out_ggaa(T38, T39, T42, X95)
U5_gga(T38, T39, X95, pH_out_ggaa(T38, T39, X94, X95)) → multG_out_gga(T38, T39, X95)
U14_gaa(T20, T22, X49, multG_out_gga(T20, T22, X49)) → pE_out_gaa(T20, T22, X49)
U3_ga(T20, X49, pE_out_gaa(T20, X48, X49)) → factorialD_out_ga(s(T20), X49)
U9_gaaa(T12, T14, X23, T7, factorialD_out_ga(T12, T14)) → U10_gaaa(T12, T14, X23, T7, pO_in_ggaa(T12, T14, X23, T7))
pO_in_ggaa(T12, T14, T79, T7) → U11_ggaa(T12, T14, T79, T7, multG_in_gga(T12, T14, T79))
U11_ggaa(T12, T14, T79, T7, multG_out_gga(T12, T14, T79)) → U12_ggaa(T12, T14, T79, T7, multJ_in_gga(T12, T79, T7))
multJ_in_gga(T103, T104, T106) → U7_gga(T103, T104, T106, pK_in_ggaa(T103, T104, X210, T106))
pK_in_ggaa(T103, T104, T109, T106) → U17_ggaa(T103, T104, T109, T106, multG_in_gga(T103, T104, T109))
U17_ggaa(T103, T104, T109, T106, multG_out_gga(T103, T104, T109)) → U18_ggaa(T103, T104, T109, T106, addI_in_gga(T104, T109, T106))
addI_in_gga(s(T127), T128, s(T130)) → U6_gga(T127, T128, T130, addI_in_gga(T127, T128, T130))
addI_in_gga(0, T136, T136) → addI_out_gga(0, T136, T136)
U6_gga(T127, T128, T130, addI_out_gga(T127, T128, T130)) → addI_out_gga(s(T127), T128, s(T130))
U18_ggaa(T103, T104, T109, T106, addI_out_gga(T104, T109, T106)) → pK_out_ggaa(T103, T104, T109, T106)
U7_gga(T103, T104, T106, pK_out_ggaa(T103, T104, X210, T106)) → multJ_out_gga(T103, T104, T106)
U12_ggaa(T12, T14, T79, T7, multJ_out_gga(T12, T79, T7)) → pO_out_ggaa(T12, T14, T79, T7)
U10_gaaa(T12, T14, X23, T7, pO_out_ggaa(T12, T14, X23, T7)) → pB_out_gaaa(T12, T14, X23, T7)
U1_ga(T12, T7, pB_out_gaaa(T12, X22, X23, T7)) → factorialA_out_ga(s(s(T12)), T7)
factorialA_in_ga(s(0), T145) → U2_ga(T145, pC_in_aa(X275, T145))
pC_in_aa(T146, T145) → U19_aa(T146, T145, multM_in_a(T146))
multM_in_a(0) → multM_out_a(0)
U19_aa(T146, T145, multM_out_a(T146)) → U20_aa(T146, T145, addN_in_ga(T146, T145))
addN_in_ga(T162, s(T162)) → addN_out_ga(T162, s(T162))
U20_aa(T146, T145, addN_out_ga(T146, T145)) → pC_out_aa(T146, T145)
U2_ga(T145, pC_out_aa(X275, T145)) → factorialA_out_ga(s(0), T145)
factorialA_in_ga(0, s(0)) → factorialA_out_ga(0, s(0))

The argument filtering Pi contains the following mapping:
factorialA_in_ga(x1, x2)  =  factorialA_in_ga(x1)
s(x1)  =  s(x1)
U1_ga(x1, x2, x3)  =  U1_ga(x1, x3)
pB_in_gaaa(x1, x2, x3, x4)  =  pB_in_gaaa(x1)
U9_gaaa(x1, x2, x3, x4, x5)  =  U9_gaaa(x1, x5)
factorialD_in_ga(x1, x2)  =  factorialD_in_ga(x1)
U3_ga(x1, x2, x3)  =  U3_ga(x1, x3)
pE_in_gaa(x1, x2, x3)  =  pE_in_gaa(x1)
U13_gaa(x1, x2, x3, x4)  =  U13_gaa(x1, x4)
0  =  0
factorialD_out_ga(x1, x2)  =  factorialD_out_ga(x1, x2)
U14_gaa(x1, x2, x3, x4)  =  U14_gaa(x1, x2, x4)
multG_in_gga(x1, x2, x3)  =  multG_in_gga(x1, x2)
U5_gga(x1, x2, x3, x4)  =  U5_gga(x1, x2, x4)
pH_in_ggaa(x1, x2, x3, x4)  =  pH_in_ggaa(x1, x2)
U15_ggaa(x1, x2, x3, x4, x5)  =  U15_ggaa(x1, x2, x5)
multL_in_gga(x1, x2, x3)  =  multL_in_gga(x1, x2)
U8_gga(x1, x2, x3, x4)  =  U8_gga(x1, x2, x4)
pH_out_ggaa(x1, x2, x3, x4)  =  pH_out_ggaa(x1, x2, x3, x4)
multL_out_gga(x1, x2, x3)  =  multL_out_gga(x1, x2, x3)
U16_ggaa(x1, x2, x3, x4, x5)  =  U16_ggaa(x1, x2, x3, x5)
addF_in_gga(x1, x2, x3)  =  addF_in_gga(x1, x2)
U4_gga(x1, x2, x3, x4)  =  U4_gga(x1, x2, x4)
addF_out_gga(x1, x2, x3)  =  addF_out_gga(x1, x2, x3)
multG_out_gga(x1, x2, x3)  =  multG_out_gga(x1, x2, x3)
pE_out_gaa(x1, x2, x3)  =  pE_out_gaa(x1, x2, x3)
U10_gaaa(x1, x2, x3, x4, x5)  =  U10_gaaa(x1, x2, x5)
pO_in_ggaa(x1, x2, x3, x4)  =  pO_in_ggaa(x1, x2)
U11_ggaa(x1, x2, x3, x4, x5)  =  U11_ggaa(x1, x2, x5)
U12_ggaa(x1, x2, x3, x4, x5)  =  U12_ggaa(x1, x2, x3, x5)
multJ_in_gga(x1, x2, x3)  =  multJ_in_gga(x1, x2)
U7_gga(x1, x2, x3, x4)  =  U7_gga(x1, x2, x4)
pK_in_ggaa(x1, x2, x3, x4)  =  pK_in_ggaa(x1, x2)
U17_ggaa(x1, x2, x3, x4, x5)  =  U17_ggaa(x1, x2, x5)
U18_ggaa(x1, x2, x3, x4, x5)  =  U18_ggaa(x1, x2, x3, x5)
addI_in_gga(x1, x2, x3)  =  addI_in_gga(x1, x2)
U6_gga(x1, x2, x3, x4)  =  U6_gga(x1, x2, x4)
addI_out_gga(x1, x2, x3)  =  addI_out_gga(x1, x2, x3)
pK_out_ggaa(x1, x2, x3, x4)  =  pK_out_ggaa(x1, x2, x3, x4)
multJ_out_gga(x1, x2, x3)  =  multJ_out_gga(x1, x2, x3)
pO_out_ggaa(x1, x2, x3, x4)  =  pO_out_ggaa(x1, x2, x3, x4)
pB_out_gaaa(x1, x2, x3, x4)  =  pB_out_gaaa(x1, x2, x3, x4)
factorialA_out_ga(x1, x2)  =  factorialA_out_ga(x1, x2)
U2_ga(x1, x2)  =  U2_ga(x2)
pC_in_aa(x1, x2)  =  pC_in_aa
U19_aa(x1, x2, x3)  =  U19_aa(x3)
multM_in_a(x1)  =  multM_in_a
multM_out_a(x1)  =  multM_out_a(x1)
U20_aa(x1, x2, x3)  =  U20_aa(x1, x3)
addN_in_ga(x1, x2)  =  addN_in_ga(x1)
addN_out_ga(x1, x2)  =  addN_out_ga(x1, x2)
pC_out_aa(x1, x2)  =  pC_out_aa(x1, x2)
FACTORIALA_IN_GA(x1, x2)  =  FACTORIALA_IN_GA(x1)
U1_GA(x1, x2, x3)  =  U1_GA(x1, x3)
PB_IN_GAAA(x1, x2, x3, x4)  =  PB_IN_GAAA(x1)
U9_GAAA(x1, x2, x3, x4, x5)  =  U9_GAAA(x1, x5)
FACTORIALD_IN_GA(x1, x2)  =  FACTORIALD_IN_GA(x1)
U3_GA(x1, x2, x3)  =  U3_GA(x1, x3)
PE_IN_GAA(x1, x2, x3)  =  PE_IN_GAA(x1)
U13_GAA(x1, x2, x3, x4)  =  U13_GAA(x1, x4)
U14_GAA(x1, x2, x3, x4)  =  U14_GAA(x1, x2, x4)
MULTG_IN_GGA(x1, x2, x3)  =  MULTG_IN_GGA(x1, x2)
U5_GGA(x1, x2, x3, x4)  =  U5_GGA(x1, x2, x4)
PH_IN_GGAA(x1, x2, x3, x4)  =  PH_IN_GGAA(x1, x2)
U15_GGAA(x1, x2, x3, x4, x5)  =  U15_GGAA(x1, x2, x5)
MULTL_IN_GGA(x1, x2, x3)  =  MULTL_IN_GGA(x1, x2)
U8_GGA(x1, x2, x3, x4)  =  U8_GGA(x1, x2, x4)
U16_GGAA(x1, x2, x3, x4, x5)  =  U16_GGAA(x1, x2, x3, x5)
ADDF_IN_GGA(x1, x2, x3)  =  ADDF_IN_GGA(x1, x2)
U4_GGA(x1, x2, x3, x4)  =  U4_GGA(x1, x2, x4)
U10_GAAA(x1, x2, x3, x4, x5)  =  U10_GAAA(x1, x2, x5)
PO_IN_GGAA(x1, x2, x3, x4)  =  PO_IN_GGAA(x1, x2)
U11_GGAA(x1, x2, x3, x4, x5)  =  U11_GGAA(x1, x2, x5)
U12_GGAA(x1, x2, x3, x4, x5)  =  U12_GGAA(x1, x2, x3, x5)
MULTJ_IN_GGA(x1, x2, x3)  =  MULTJ_IN_GGA(x1, x2)
U7_GGA(x1, x2, x3, x4)  =  U7_GGA(x1, x2, x4)
PK_IN_GGAA(x1, x2, x3, x4)  =  PK_IN_GGAA(x1, x2)
U17_GGAA(x1, x2, x3, x4, x5)  =  U17_GGAA(x1, x2, x5)
U18_GGAA(x1, x2, x3, x4, x5)  =  U18_GGAA(x1, x2, x3, x5)
ADDI_IN_GGA(x1, x2, x3)  =  ADDI_IN_GGA(x1, x2)
U6_GGA(x1, x2, x3, x4)  =  U6_GGA(x1, x2, x4)
U2_GA(x1, x2)  =  U2_GA(x2)
PC_IN_AA(x1, x2)  =  PC_IN_AA
U19_AA(x1, x2, x3)  =  U19_AA(x3)
MULTM_IN_A(x1)  =  MULTM_IN_A
U20_AA(x1, x2, x3)  =  U20_AA(x1, x3)
ADDN_IN_GA(x1, x2)  =  ADDN_IN_GA(x1)

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

(4) Obligation:

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

FACTORIALA_IN_GA(s(s(T12)), T7) → U1_GA(T12, T7, pB_in_gaaa(T12, X22, X23, T7))
FACTORIALA_IN_GA(s(s(T12)), T7) → PB_IN_GAAA(T12, X22, X23, T7)
PB_IN_GAAA(T12, T14, X23, T7) → U9_GAAA(T12, T14, X23, T7, factorialD_in_ga(T12, T14))
PB_IN_GAAA(T12, T14, X23, T7) → FACTORIALD_IN_GA(T12, T14)
FACTORIALD_IN_GA(s(T20), X49) → U3_GA(T20, X49, pE_in_gaa(T20, X48, X49))
FACTORIALD_IN_GA(s(T20), X49) → PE_IN_GAA(T20, X48, X49)
PE_IN_GAA(T20, T22, X49) → U13_GAA(T20, T22, X49, factorialD_in_ga(T20, T22))
PE_IN_GAA(T20, T22, X49) → FACTORIALD_IN_GA(T20, T22)
U13_GAA(T20, T22, X49, factorialD_out_ga(T20, T22)) → U14_GAA(T20, T22, X49, multG_in_gga(T20, T22, X49))
U13_GAA(T20, T22, X49, factorialD_out_ga(T20, T22)) → MULTG_IN_GGA(T20, T22, X49)
MULTG_IN_GGA(T38, T39, X95) → U5_GGA(T38, T39, X95, pH_in_ggaa(T38, T39, X94, X95))
MULTG_IN_GGA(T38, T39, X95) → PH_IN_GGAA(T38, T39, X94, X95)
PH_IN_GGAA(T38, T39, T42, X95) → U15_GGAA(T38, T39, T42, X95, multL_in_gga(T38, T39, T42))
PH_IN_GGAA(T38, T39, T42, X95) → MULTL_IN_GGA(T38, T39, T42)
MULTL_IN_GGA(s(T53), T54, X128) → U8_GGA(T53, T54, X128, pH_in_ggaa(T53, T54, X127, X128))
MULTL_IN_GGA(s(T53), T54, X128) → PH_IN_GGAA(T53, T54, X127, X128)
U15_GGAA(T38, T39, T42, X95, multL_out_gga(T38, T39, T42)) → U16_GGAA(T38, T39, T42, X95, addF_in_gga(T39, T42, X95))
U15_GGAA(T38, T39, T42, X95, multL_out_gga(T38, T39, T42)) → ADDF_IN_GGA(T39, T42, X95)
ADDF_IN_GGA(s(T70), T71, s(X160)) → U4_GGA(T70, T71, X160, addF_in_gga(T70, T71, X160))
ADDF_IN_GGA(s(T70), T71, s(X160)) → ADDF_IN_GGA(T70, T71, X160)
U9_GAAA(T12, T14, X23, T7, factorialD_out_ga(T12, T14)) → U10_GAAA(T12, T14, X23, T7, pO_in_ggaa(T12, T14, X23, T7))
U9_GAAA(T12, T14, X23, T7, factorialD_out_ga(T12, T14)) → PO_IN_GGAA(T12, T14, X23, T7)
PO_IN_GGAA(T12, T14, T79, T7) → U11_GGAA(T12, T14, T79, T7, multG_in_gga(T12, T14, T79))
PO_IN_GGAA(T12, T14, T79, T7) → MULTG_IN_GGA(T12, T14, T79)
U11_GGAA(T12, T14, T79, T7, multG_out_gga(T12, T14, T79)) → U12_GGAA(T12, T14, T79, T7, multJ_in_gga(T12, T79, T7))
U11_GGAA(T12, T14, T79, T7, multG_out_gga(T12, T14, T79)) → MULTJ_IN_GGA(T12, T79, T7)
MULTJ_IN_GGA(T103, T104, T106) → U7_GGA(T103, T104, T106, pK_in_ggaa(T103, T104, X210, T106))
MULTJ_IN_GGA(T103, T104, T106) → PK_IN_GGAA(T103, T104, X210, T106)
PK_IN_GGAA(T103, T104, T109, T106) → U17_GGAA(T103, T104, T109, T106, multG_in_gga(T103, T104, T109))
PK_IN_GGAA(T103, T104, T109, T106) → MULTG_IN_GGA(T103, T104, T109)
U17_GGAA(T103, T104, T109, T106, multG_out_gga(T103, T104, T109)) → U18_GGAA(T103, T104, T109, T106, addI_in_gga(T104, T109, T106))
U17_GGAA(T103, T104, T109, T106, multG_out_gga(T103, T104, T109)) → ADDI_IN_GGA(T104, T109, T106)
ADDI_IN_GGA(s(T127), T128, s(T130)) → U6_GGA(T127, T128, T130, addI_in_gga(T127, T128, T130))
ADDI_IN_GGA(s(T127), T128, s(T130)) → ADDI_IN_GGA(T127, T128, T130)
FACTORIALA_IN_GA(s(0), T145) → U2_GA(T145, pC_in_aa(X275, T145))
FACTORIALA_IN_GA(s(0), T145) → PC_IN_AA(X275, T145)
PC_IN_AA(T146, T145) → U19_AA(T146, T145, multM_in_a(T146))
PC_IN_AA(T146, T145) → MULTM_IN_A(T146)
U19_AA(T146, T145, multM_out_a(T146)) → U20_AA(T146, T145, addN_in_ga(T146, T145))
U19_AA(T146, T145, multM_out_a(T146)) → ADDN_IN_GA(T146, T145)

The TRS R consists of the following rules:

factorialA_in_ga(s(s(T12)), T7) → U1_ga(T12, T7, pB_in_gaaa(T12, X22, X23, T7))
pB_in_gaaa(T12, T14, X23, T7) → U9_gaaa(T12, T14, X23, T7, factorialD_in_ga(T12, T14))
factorialD_in_ga(s(T20), X49) → U3_ga(T20, X49, pE_in_gaa(T20, X48, X49))
pE_in_gaa(T20, T22, X49) → U13_gaa(T20, T22, X49, factorialD_in_ga(T20, T22))
factorialD_in_ga(0, s(0)) → factorialD_out_ga(0, s(0))
U13_gaa(T20, T22, X49, factorialD_out_ga(T20, T22)) → U14_gaa(T20, T22, X49, multG_in_gga(T20, T22, X49))
multG_in_gga(T38, T39, X95) → U5_gga(T38, T39, X95, pH_in_ggaa(T38, T39, X94, X95))
pH_in_ggaa(T38, T39, T42, X95) → U15_ggaa(T38, T39, T42, X95, multL_in_gga(T38, T39, T42))
multL_in_gga(s(T53), T54, X128) → U8_gga(T53, T54, X128, pH_in_ggaa(T53, T54, X127, X128))
U8_gga(T53, T54, X128, pH_out_ggaa(T53, T54, X127, X128)) → multL_out_gga(s(T53), T54, X128)
multL_in_gga(0, T59, 0) → multL_out_gga(0, T59, 0)
U15_ggaa(T38, T39, T42, X95, multL_out_gga(T38, T39, T42)) → U16_ggaa(T38, T39, T42, X95, addF_in_gga(T39, T42, X95))
addF_in_gga(s(T70), T71, s(X160)) → U4_gga(T70, T71, X160, addF_in_gga(T70, T71, X160))
addF_in_gga(0, T76, T76) → addF_out_gga(0, T76, T76)
U4_gga(T70, T71, X160, addF_out_gga(T70, T71, X160)) → addF_out_gga(s(T70), T71, s(X160))
U16_ggaa(T38, T39, T42, X95, addF_out_gga(T39, T42, X95)) → pH_out_ggaa(T38, T39, T42, X95)
U5_gga(T38, T39, X95, pH_out_ggaa(T38, T39, X94, X95)) → multG_out_gga(T38, T39, X95)
U14_gaa(T20, T22, X49, multG_out_gga(T20, T22, X49)) → pE_out_gaa(T20, T22, X49)
U3_ga(T20, X49, pE_out_gaa(T20, X48, X49)) → factorialD_out_ga(s(T20), X49)
U9_gaaa(T12, T14, X23, T7, factorialD_out_ga(T12, T14)) → U10_gaaa(T12, T14, X23, T7, pO_in_ggaa(T12, T14, X23, T7))
pO_in_ggaa(T12, T14, T79, T7) → U11_ggaa(T12, T14, T79, T7, multG_in_gga(T12, T14, T79))
U11_ggaa(T12, T14, T79, T7, multG_out_gga(T12, T14, T79)) → U12_ggaa(T12, T14, T79, T7, multJ_in_gga(T12, T79, T7))
multJ_in_gga(T103, T104, T106) → U7_gga(T103, T104, T106, pK_in_ggaa(T103, T104, X210, T106))
pK_in_ggaa(T103, T104, T109, T106) → U17_ggaa(T103, T104, T109, T106, multG_in_gga(T103, T104, T109))
U17_ggaa(T103, T104, T109, T106, multG_out_gga(T103, T104, T109)) → U18_ggaa(T103, T104, T109, T106, addI_in_gga(T104, T109, T106))
addI_in_gga(s(T127), T128, s(T130)) → U6_gga(T127, T128, T130, addI_in_gga(T127, T128, T130))
addI_in_gga(0, T136, T136) → addI_out_gga(0, T136, T136)
U6_gga(T127, T128, T130, addI_out_gga(T127, T128, T130)) → addI_out_gga(s(T127), T128, s(T130))
U18_ggaa(T103, T104, T109, T106, addI_out_gga(T104, T109, T106)) → pK_out_ggaa(T103, T104, T109, T106)
U7_gga(T103, T104, T106, pK_out_ggaa(T103, T104, X210, T106)) → multJ_out_gga(T103, T104, T106)
U12_ggaa(T12, T14, T79, T7, multJ_out_gga(T12, T79, T7)) → pO_out_ggaa(T12, T14, T79, T7)
U10_gaaa(T12, T14, X23, T7, pO_out_ggaa(T12, T14, X23, T7)) → pB_out_gaaa(T12, T14, X23, T7)
U1_ga(T12, T7, pB_out_gaaa(T12, X22, X23, T7)) → factorialA_out_ga(s(s(T12)), T7)
factorialA_in_ga(s(0), T145) → U2_ga(T145, pC_in_aa(X275, T145))
pC_in_aa(T146, T145) → U19_aa(T146, T145, multM_in_a(T146))
multM_in_a(0) → multM_out_a(0)
U19_aa(T146, T145, multM_out_a(T146)) → U20_aa(T146, T145, addN_in_ga(T146, T145))
addN_in_ga(T162, s(T162)) → addN_out_ga(T162, s(T162))
U20_aa(T146, T145, addN_out_ga(T146, T145)) → pC_out_aa(T146, T145)
U2_ga(T145, pC_out_aa(X275, T145)) → factorialA_out_ga(s(0), T145)
factorialA_in_ga(0, s(0)) → factorialA_out_ga(0, s(0))

The argument filtering Pi contains the following mapping:
factorialA_in_ga(x1, x2)  =  factorialA_in_ga(x1)
s(x1)  =  s(x1)
U1_ga(x1, x2, x3)  =  U1_ga(x1, x3)
pB_in_gaaa(x1, x2, x3, x4)  =  pB_in_gaaa(x1)
U9_gaaa(x1, x2, x3, x4, x5)  =  U9_gaaa(x1, x5)
factorialD_in_ga(x1, x2)  =  factorialD_in_ga(x1)
U3_ga(x1, x2, x3)  =  U3_ga(x1, x3)
pE_in_gaa(x1, x2, x3)  =  pE_in_gaa(x1)
U13_gaa(x1, x2, x3, x4)  =  U13_gaa(x1, x4)
0  =  0
factorialD_out_ga(x1, x2)  =  factorialD_out_ga(x1, x2)
U14_gaa(x1, x2, x3, x4)  =  U14_gaa(x1, x2, x4)
multG_in_gga(x1, x2, x3)  =  multG_in_gga(x1, x2)
U5_gga(x1, x2, x3, x4)  =  U5_gga(x1, x2, x4)
pH_in_ggaa(x1, x2, x3, x4)  =  pH_in_ggaa(x1, x2)
U15_ggaa(x1, x2, x3, x4, x5)  =  U15_ggaa(x1, x2, x5)
multL_in_gga(x1, x2, x3)  =  multL_in_gga(x1, x2)
U8_gga(x1, x2, x3, x4)  =  U8_gga(x1, x2, x4)
pH_out_ggaa(x1, x2, x3, x4)  =  pH_out_ggaa(x1, x2, x3, x4)
multL_out_gga(x1, x2, x3)  =  multL_out_gga(x1, x2, x3)
U16_ggaa(x1, x2, x3, x4, x5)  =  U16_ggaa(x1, x2, x3, x5)
addF_in_gga(x1, x2, x3)  =  addF_in_gga(x1, x2)
U4_gga(x1, x2, x3, x4)  =  U4_gga(x1, x2, x4)
addF_out_gga(x1, x2, x3)  =  addF_out_gga(x1, x2, x3)
multG_out_gga(x1, x2, x3)  =  multG_out_gga(x1, x2, x3)
pE_out_gaa(x1, x2, x3)  =  pE_out_gaa(x1, x2, x3)
U10_gaaa(x1, x2, x3, x4, x5)  =  U10_gaaa(x1, x2, x5)
pO_in_ggaa(x1, x2, x3, x4)  =  pO_in_ggaa(x1, x2)
U11_ggaa(x1, x2, x3, x4, x5)  =  U11_ggaa(x1, x2, x5)
U12_ggaa(x1, x2, x3, x4, x5)  =  U12_ggaa(x1, x2, x3, x5)
multJ_in_gga(x1, x2, x3)  =  multJ_in_gga(x1, x2)
U7_gga(x1, x2, x3, x4)  =  U7_gga(x1, x2, x4)
pK_in_ggaa(x1, x2, x3, x4)  =  pK_in_ggaa(x1, x2)
U17_ggaa(x1, x2, x3, x4, x5)  =  U17_ggaa(x1, x2, x5)
U18_ggaa(x1, x2, x3, x4, x5)  =  U18_ggaa(x1, x2, x3, x5)
addI_in_gga(x1, x2, x3)  =  addI_in_gga(x1, x2)
U6_gga(x1, x2, x3, x4)  =  U6_gga(x1, x2, x4)
addI_out_gga(x1, x2, x3)  =  addI_out_gga(x1, x2, x3)
pK_out_ggaa(x1, x2, x3, x4)  =  pK_out_ggaa(x1, x2, x3, x4)
multJ_out_gga(x1, x2, x3)  =  multJ_out_gga(x1, x2, x3)
pO_out_ggaa(x1, x2, x3, x4)  =  pO_out_ggaa(x1, x2, x3, x4)
pB_out_gaaa(x1, x2, x3, x4)  =  pB_out_gaaa(x1, x2, x3, x4)
factorialA_out_ga(x1, x2)  =  factorialA_out_ga(x1, x2)
U2_ga(x1, x2)  =  U2_ga(x2)
pC_in_aa(x1, x2)  =  pC_in_aa
U19_aa(x1, x2, x3)  =  U19_aa(x3)
multM_in_a(x1)  =  multM_in_a
multM_out_a(x1)  =  multM_out_a(x1)
U20_aa(x1, x2, x3)  =  U20_aa(x1, x3)
addN_in_ga(x1, x2)  =  addN_in_ga(x1)
addN_out_ga(x1, x2)  =  addN_out_ga(x1, x2)
pC_out_aa(x1, x2)  =  pC_out_aa(x1, x2)
FACTORIALA_IN_GA(x1, x2)  =  FACTORIALA_IN_GA(x1)
U1_GA(x1, x2, x3)  =  U1_GA(x1, x3)
PB_IN_GAAA(x1, x2, x3, x4)  =  PB_IN_GAAA(x1)
U9_GAAA(x1, x2, x3, x4, x5)  =  U9_GAAA(x1, x5)
FACTORIALD_IN_GA(x1, x2)  =  FACTORIALD_IN_GA(x1)
U3_GA(x1, x2, x3)  =  U3_GA(x1, x3)
PE_IN_GAA(x1, x2, x3)  =  PE_IN_GAA(x1)
U13_GAA(x1, x2, x3, x4)  =  U13_GAA(x1, x4)
U14_GAA(x1, x2, x3, x4)  =  U14_GAA(x1, x2, x4)
MULTG_IN_GGA(x1, x2, x3)  =  MULTG_IN_GGA(x1, x2)
U5_GGA(x1, x2, x3, x4)  =  U5_GGA(x1, x2, x4)
PH_IN_GGAA(x1, x2, x3, x4)  =  PH_IN_GGAA(x1, x2)
U15_GGAA(x1, x2, x3, x4, x5)  =  U15_GGAA(x1, x2, x5)
MULTL_IN_GGA(x1, x2, x3)  =  MULTL_IN_GGA(x1, x2)
U8_GGA(x1, x2, x3, x4)  =  U8_GGA(x1, x2, x4)
U16_GGAA(x1, x2, x3, x4, x5)  =  U16_GGAA(x1, x2, x3, x5)
ADDF_IN_GGA(x1, x2, x3)  =  ADDF_IN_GGA(x1, x2)
U4_GGA(x1, x2, x3, x4)  =  U4_GGA(x1, x2, x4)
U10_GAAA(x1, x2, x3, x4, x5)  =  U10_GAAA(x1, x2, x5)
PO_IN_GGAA(x1, x2, x3, x4)  =  PO_IN_GGAA(x1, x2)
U11_GGAA(x1, x2, x3, x4, x5)  =  U11_GGAA(x1, x2, x5)
U12_GGAA(x1, x2, x3, x4, x5)  =  U12_GGAA(x1, x2, x3, x5)
MULTJ_IN_GGA(x1, x2, x3)  =  MULTJ_IN_GGA(x1, x2)
U7_GGA(x1, x2, x3, x4)  =  U7_GGA(x1, x2, x4)
PK_IN_GGAA(x1, x2, x3, x4)  =  PK_IN_GGAA(x1, x2)
U17_GGAA(x1, x2, x3, x4, x5)  =  U17_GGAA(x1, x2, x5)
U18_GGAA(x1, x2, x3, x4, x5)  =  U18_GGAA(x1, x2, x3, x5)
ADDI_IN_GGA(x1, x2, x3)  =  ADDI_IN_GGA(x1, x2)
U6_GGA(x1, x2, x3, x4)  =  U6_GGA(x1, x2, x4)
U2_GA(x1, x2)  =  U2_GA(x2)
PC_IN_AA(x1, x2)  =  PC_IN_AA
U19_AA(x1, x2, x3)  =  U19_AA(x3)
MULTM_IN_A(x1)  =  MULTM_IN_A
U20_AA(x1, x2, x3)  =  U20_AA(x1, x3)
ADDN_IN_GA(x1, x2)  =  ADDN_IN_GA(x1)

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

(5) DependencyGraphProof (EQUIVALENT transformation)

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

(6) Complex Obligation (AND)

(7) Obligation:

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

ADDI_IN_GGA(s(T127), T128, s(T130)) → ADDI_IN_GGA(T127, T128, T130)

The TRS R consists of the following rules:

factorialA_in_ga(s(s(T12)), T7) → U1_ga(T12, T7, pB_in_gaaa(T12, X22, X23, T7))
pB_in_gaaa(T12, T14, X23, T7) → U9_gaaa(T12, T14, X23, T7, factorialD_in_ga(T12, T14))
factorialD_in_ga(s(T20), X49) → U3_ga(T20, X49, pE_in_gaa(T20, X48, X49))
pE_in_gaa(T20, T22, X49) → U13_gaa(T20, T22, X49, factorialD_in_ga(T20, T22))
factorialD_in_ga(0, s(0)) → factorialD_out_ga(0, s(0))
U13_gaa(T20, T22, X49, factorialD_out_ga(T20, T22)) → U14_gaa(T20, T22, X49, multG_in_gga(T20, T22, X49))
multG_in_gga(T38, T39, X95) → U5_gga(T38, T39, X95, pH_in_ggaa(T38, T39, X94, X95))
pH_in_ggaa(T38, T39, T42, X95) → U15_ggaa(T38, T39, T42, X95, multL_in_gga(T38, T39, T42))
multL_in_gga(s(T53), T54, X128) → U8_gga(T53, T54, X128, pH_in_ggaa(T53, T54, X127, X128))
U8_gga(T53, T54, X128, pH_out_ggaa(T53, T54, X127, X128)) → multL_out_gga(s(T53), T54, X128)
multL_in_gga(0, T59, 0) → multL_out_gga(0, T59, 0)
U15_ggaa(T38, T39, T42, X95, multL_out_gga(T38, T39, T42)) → U16_ggaa(T38, T39, T42, X95, addF_in_gga(T39, T42, X95))
addF_in_gga(s(T70), T71, s(X160)) → U4_gga(T70, T71, X160, addF_in_gga(T70, T71, X160))
addF_in_gga(0, T76, T76) → addF_out_gga(0, T76, T76)
U4_gga(T70, T71, X160, addF_out_gga(T70, T71, X160)) → addF_out_gga(s(T70), T71, s(X160))
U16_ggaa(T38, T39, T42, X95, addF_out_gga(T39, T42, X95)) → pH_out_ggaa(T38, T39, T42, X95)
U5_gga(T38, T39, X95, pH_out_ggaa(T38, T39, X94, X95)) → multG_out_gga(T38, T39, X95)
U14_gaa(T20, T22, X49, multG_out_gga(T20, T22, X49)) → pE_out_gaa(T20, T22, X49)
U3_ga(T20, X49, pE_out_gaa(T20, X48, X49)) → factorialD_out_ga(s(T20), X49)
U9_gaaa(T12, T14, X23, T7, factorialD_out_ga(T12, T14)) → U10_gaaa(T12, T14, X23, T7, pO_in_ggaa(T12, T14, X23, T7))
pO_in_ggaa(T12, T14, T79, T7) → U11_ggaa(T12, T14, T79, T7, multG_in_gga(T12, T14, T79))
U11_ggaa(T12, T14, T79, T7, multG_out_gga(T12, T14, T79)) → U12_ggaa(T12, T14, T79, T7, multJ_in_gga(T12, T79, T7))
multJ_in_gga(T103, T104, T106) → U7_gga(T103, T104, T106, pK_in_ggaa(T103, T104, X210, T106))
pK_in_ggaa(T103, T104, T109, T106) → U17_ggaa(T103, T104, T109, T106, multG_in_gga(T103, T104, T109))
U17_ggaa(T103, T104, T109, T106, multG_out_gga(T103, T104, T109)) → U18_ggaa(T103, T104, T109, T106, addI_in_gga(T104, T109, T106))
addI_in_gga(s(T127), T128, s(T130)) → U6_gga(T127, T128, T130, addI_in_gga(T127, T128, T130))
addI_in_gga(0, T136, T136) → addI_out_gga(0, T136, T136)
U6_gga(T127, T128, T130, addI_out_gga(T127, T128, T130)) → addI_out_gga(s(T127), T128, s(T130))
U18_ggaa(T103, T104, T109, T106, addI_out_gga(T104, T109, T106)) → pK_out_ggaa(T103, T104, T109, T106)
U7_gga(T103, T104, T106, pK_out_ggaa(T103, T104, X210, T106)) → multJ_out_gga(T103, T104, T106)
U12_ggaa(T12, T14, T79, T7, multJ_out_gga(T12, T79, T7)) → pO_out_ggaa(T12, T14, T79, T7)
U10_gaaa(T12, T14, X23, T7, pO_out_ggaa(T12, T14, X23, T7)) → pB_out_gaaa(T12, T14, X23, T7)
U1_ga(T12, T7, pB_out_gaaa(T12, X22, X23, T7)) → factorialA_out_ga(s(s(T12)), T7)
factorialA_in_ga(s(0), T145) → U2_ga(T145, pC_in_aa(X275, T145))
pC_in_aa(T146, T145) → U19_aa(T146, T145, multM_in_a(T146))
multM_in_a(0) → multM_out_a(0)
U19_aa(T146, T145, multM_out_a(T146)) → U20_aa(T146, T145, addN_in_ga(T146, T145))
addN_in_ga(T162, s(T162)) → addN_out_ga(T162, s(T162))
U20_aa(T146, T145, addN_out_ga(T146, T145)) → pC_out_aa(T146, T145)
U2_ga(T145, pC_out_aa(X275, T145)) → factorialA_out_ga(s(0), T145)
factorialA_in_ga(0, s(0)) → factorialA_out_ga(0, s(0))

The argument filtering Pi contains the following mapping:
factorialA_in_ga(x1, x2)  =  factorialA_in_ga(x1)
s(x1)  =  s(x1)
U1_ga(x1, x2, x3)  =  U1_ga(x1, x3)
pB_in_gaaa(x1, x2, x3, x4)  =  pB_in_gaaa(x1)
U9_gaaa(x1, x2, x3, x4, x5)  =  U9_gaaa(x1, x5)
factorialD_in_ga(x1, x2)  =  factorialD_in_ga(x1)
U3_ga(x1, x2, x3)  =  U3_ga(x1, x3)
pE_in_gaa(x1, x2, x3)  =  pE_in_gaa(x1)
U13_gaa(x1, x2, x3, x4)  =  U13_gaa(x1, x4)
0  =  0
factorialD_out_ga(x1, x2)  =  factorialD_out_ga(x1, x2)
U14_gaa(x1, x2, x3, x4)  =  U14_gaa(x1, x2, x4)
multG_in_gga(x1, x2, x3)  =  multG_in_gga(x1, x2)
U5_gga(x1, x2, x3, x4)  =  U5_gga(x1, x2, x4)
pH_in_ggaa(x1, x2, x3, x4)  =  pH_in_ggaa(x1, x2)
U15_ggaa(x1, x2, x3, x4, x5)  =  U15_ggaa(x1, x2, x5)
multL_in_gga(x1, x2, x3)  =  multL_in_gga(x1, x2)
U8_gga(x1, x2, x3, x4)  =  U8_gga(x1, x2, x4)
pH_out_ggaa(x1, x2, x3, x4)  =  pH_out_ggaa(x1, x2, x3, x4)
multL_out_gga(x1, x2, x3)  =  multL_out_gga(x1, x2, x3)
U16_ggaa(x1, x2, x3, x4, x5)  =  U16_ggaa(x1, x2, x3, x5)
addF_in_gga(x1, x2, x3)  =  addF_in_gga(x1, x2)
U4_gga(x1, x2, x3, x4)  =  U4_gga(x1, x2, x4)
addF_out_gga(x1, x2, x3)  =  addF_out_gga(x1, x2, x3)
multG_out_gga(x1, x2, x3)  =  multG_out_gga(x1, x2, x3)
pE_out_gaa(x1, x2, x3)  =  pE_out_gaa(x1, x2, x3)
U10_gaaa(x1, x2, x3, x4, x5)  =  U10_gaaa(x1, x2, x5)
pO_in_ggaa(x1, x2, x3, x4)  =  pO_in_ggaa(x1, x2)
U11_ggaa(x1, x2, x3, x4, x5)  =  U11_ggaa(x1, x2, x5)
U12_ggaa(x1, x2, x3, x4, x5)  =  U12_ggaa(x1, x2, x3, x5)
multJ_in_gga(x1, x2, x3)  =  multJ_in_gga(x1, x2)
U7_gga(x1, x2, x3, x4)  =  U7_gga(x1, x2, x4)
pK_in_ggaa(x1, x2, x3, x4)  =  pK_in_ggaa(x1, x2)
U17_ggaa(x1, x2, x3, x4, x5)  =  U17_ggaa(x1, x2, x5)
U18_ggaa(x1, x2, x3, x4, x5)  =  U18_ggaa(x1, x2, x3, x5)
addI_in_gga(x1, x2, x3)  =  addI_in_gga(x1, x2)
U6_gga(x1, x2, x3, x4)  =  U6_gga(x1, x2, x4)
addI_out_gga(x1, x2, x3)  =  addI_out_gga(x1, x2, x3)
pK_out_ggaa(x1, x2, x3, x4)  =  pK_out_ggaa(x1, x2, x3, x4)
multJ_out_gga(x1, x2, x3)  =  multJ_out_gga(x1, x2, x3)
pO_out_ggaa(x1, x2, x3, x4)  =  pO_out_ggaa(x1, x2, x3, x4)
pB_out_gaaa(x1, x2, x3, x4)  =  pB_out_gaaa(x1, x2, x3, x4)
factorialA_out_ga(x1, x2)  =  factorialA_out_ga(x1, x2)
U2_ga(x1, x2)  =  U2_ga(x2)
pC_in_aa(x1, x2)  =  pC_in_aa
U19_aa(x1, x2, x3)  =  U19_aa(x3)
multM_in_a(x1)  =  multM_in_a
multM_out_a(x1)  =  multM_out_a(x1)
U20_aa(x1, x2, x3)  =  U20_aa(x1, x3)
addN_in_ga(x1, x2)  =  addN_in_ga(x1)
addN_out_ga(x1, x2)  =  addN_out_ga(x1, x2)
pC_out_aa(x1, x2)  =  pC_out_aa(x1, x2)
ADDI_IN_GGA(x1, x2, x3)  =  ADDI_IN_GGA(x1, x2)

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:

ADDI_IN_GGA(s(T127), T128, s(T130)) → ADDI_IN_GGA(T127, T128, T130)

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

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:

ADDI_IN_GGA(s(T127), T128) → ADDI_IN_GGA(T127, T128)

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:

• ADDI_IN_GGA(s(T127), T128) → ADDI_IN_GGA(T127, T128)
  The graph contains the following edges 1 > 1, 2 >= 2

(13) YES

(14) Obligation:

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

ADDF_IN_GGA(s(T70), T71, s(X160)) → ADDF_IN_GGA(T70, T71, X160)

The TRS R consists of the following rules:

factorialA_in_ga(s(s(T12)), T7) → U1_ga(T12, T7, pB_in_gaaa(T12, X22, X23, T7))
pB_in_gaaa(T12, T14, X23, T7) → U9_gaaa(T12, T14, X23, T7, factorialD_in_ga(T12, T14))
factorialD_in_ga(s(T20), X49) → U3_ga(T20, X49, pE_in_gaa(T20, X48, X49))
pE_in_gaa(T20, T22, X49) → U13_gaa(T20, T22, X49, factorialD_in_ga(T20, T22))
factorialD_in_ga(0, s(0)) → factorialD_out_ga(0, s(0))
U13_gaa(T20, T22, X49, factorialD_out_ga(T20, T22)) → U14_gaa(T20, T22, X49, multG_in_gga(T20, T22, X49))
multG_in_gga(T38, T39, X95) → U5_gga(T38, T39, X95, pH_in_ggaa(T38, T39, X94, X95))
pH_in_ggaa(T38, T39, T42, X95) → U15_ggaa(T38, T39, T42, X95, multL_in_gga(T38, T39, T42))
multL_in_gga(s(T53), T54, X128) → U8_gga(T53, T54, X128, pH_in_ggaa(T53, T54, X127, X128))
U8_gga(T53, T54, X128, pH_out_ggaa(T53, T54, X127, X128)) → multL_out_gga(s(T53), T54, X128)
multL_in_gga(0, T59, 0) → multL_out_gga(0, T59, 0)
U15_ggaa(T38, T39, T42, X95, multL_out_gga(T38, T39, T42)) → U16_ggaa(T38, T39, T42, X95, addF_in_gga(T39, T42, X95))
addF_in_gga(s(T70), T71, s(X160)) → U4_gga(T70, T71, X160, addF_in_gga(T70, T71, X160))
addF_in_gga(0, T76, T76) → addF_out_gga(0, T76, T76)
U4_gga(T70, T71, X160, addF_out_gga(T70, T71, X160)) → addF_out_gga(s(T70), T71, s(X160))
U16_ggaa(T38, T39, T42, X95, addF_out_gga(T39, T42, X95)) → pH_out_ggaa(T38, T39, T42, X95)
U5_gga(T38, T39, X95, pH_out_ggaa(T38, T39, X94, X95)) → multG_out_gga(T38, T39, X95)
U14_gaa(T20, T22, X49, multG_out_gga(T20, T22, X49)) → pE_out_gaa(T20, T22, X49)
U3_ga(T20, X49, pE_out_gaa(T20, X48, X49)) → factorialD_out_ga(s(T20), X49)
U9_gaaa(T12, T14, X23, T7, factorialD_out_ga(T12, T14)) → U10_gaaa(T12, T14, X23, T7, pO_in_ggaa(T12, T14, X23, T7))
pO_in_ggaa(T12, T14, T79, T7) → U11_ggaa(T12, T14, T79, T7, multG_in_gga(T12, T14, T79))
U11_ggaa(T12, T14, T79, T7, multG_out_gga(T12, T14, T79)) → U12_ggaa(T12, T14, T79, T7, multJ_in_gga(T12, T79, T7))
multJ_in_gga(T103, T104, T106) → U7_gga(T103, T104, T106, pK_in_ggaa(T103, T104, X210, T106))
pK_in_ggaa(T103, T104, T109, T106) → U17_ggaa(T103, T104, T109, T106, multG_in_gga(T103, T104, T109))
U17_ggaa(T103, T104, T109, T106, multG_out_gga(T103, T104, T109)) → U18_ggaa(T103, T104, T109, T106, addI_in_gga(T104, T109, T106))
addI_in_gga(s(T127), T128, s(T130)) → U6_gga(T127, T128, T130, addI_in_gga(T127, T128, T130))
addI_in_gga(0, T136, T136) → addI_out_gga(0, T136, T136)
U6_gga(T127, T128, T130, addI_out_gga(T127, T128, T130)) → addI_out_gga(s(T127), T128, s(T130))
U18_ggaa(T103, T104, T109, T106, addI_out_gga(T104, T109, T106)) → pK_out_ggaa(T103, T104, T109, T106)
U7_gga(T103, T104, T106, pK_out_ggaa(T103, T104, X210, T106)) → multJ_out_gga(T103, T104, T106)
U12_ggaa(T12, T14, T79, T7, multJ_out_gga(T12, T79, T7)) → pO_out_ggaa(T12, T14, T79, T7)
U10_gaaa(T12, T14, X23, T7, pO_out_ggaa(T12, T14, X23, T7)) → pB_out_gaaa(T12, T14, X23, T7)
U1_ga(T12, T7, pB_out_gaaa(T12, X22, X23, T7)) → factorialA_out_ga(s(s(T12)), T7)
factorialA_in_ga(s(0), T145) → U2_ga(T145, pC_in_aa(X275, T145))
pC_in_aa(T146, T145) → U19_aa(T146, T145, multM_in_a(T146))
multM_in_a(0) → multM_out_a(0)
U19_aa(T146, T145, multM_out_a(T146)) → U20_aa(T146, T145, addN_in_ga(T146, T145))
addN_in_ga(T162, s(T162)) → addN_out_ga(T162, s(T162))
U20_aa(T146, T145, addN_out_ga(T146, T145)) → pC_out_aa(T146, T145)
U2_ga(T145, pC_out_aa(X275, T145)) → factorialA_out_ga(s(0), T145)
factorialA_in_ga(0, s(0)) → factorialA_out_ga(0, s(0))

The argument filtering Pi contains the following mapping:
factorialA_in_ga(x1, x2)  =  factorialA_in_ga(x1)
s(x1)  =  s(x1)
U1_ga(x1, x2, x3)  =  U1_ga(x1, x3)
pB_in_gaaa(x1, x2, x3, x4)  =  pB_in_gaaa(x1)
U9_gaaa(x1, x2, x3, x4, x5)  =  U9_gaaa(x1, x5)
factorialD_in_ga(x1, x2)  =  factorialD_in_ga(x1)
U3_ga(x1, x2, x3)  =  U3_ga(x1, x3)
pE_in_gaa(x1, x2, x3)  =  pE_in_gaa(x1)
U13_gaa(x1, x2, x3, x4)  =  U13_gaa(x1, x4)
0  =  0
factorialD_out_ga(x1, x2)  =  factorialD_out_ga(x1, x2)
U14_gaa(x1, x2, x3, x4)  =  U14_gaa(x1, x2, x4)
multG_in_gga(x1, x2, x3)  =  multG_in_gga(x1, x2)
U5_gga(x1, x2, x3, x4)  =  U5_gga(x1, x2, x4)
pH_in_ggaa(x1, x2, x3, x4)  =  pH_in_ggaa(x1, x2)
U15_ggaa(x1, x2, x3, x4, x5)  =  U15_ggaa(x1, x2, x5)
multL_in_gga(x1, x2, x3)  =  multL_in_gga(x1, x2)
U8_gga(x1, x2, x3, x4)  =  U8_gga(x1, x2, x4)
pH_out_ggaa(x1, x2, x3, x4)  =  pH_out_ggaa(x1, x2, x3, x4)
multL_out_gga(x1, x2, x3)  =  multL_out_gga(x1, x2, x3)
U16_ggaa(x1, x2, x3, x4, x5)  =  U16_ggaa(x1, x2, x3, x5)
addF_in_gga(x1, x2, x3)  =  addF_in_gga(x1, x2)
U4_gga(x1, x2, x3, x4)  =  U4_gga(x1, x2, x4)
addF_out_gga(x1, x2, x3)  =  addF_out_gga(x1, x2, x3)
multG_out_gga(x1, x2, x3)  =  multG_out_gga(x1, x2, x3)
pE_out_gaa(x1, x2, x3)  =  pE_out_gaa(x1, x2, x3)
U10_gaaa(x1, x2, x3, x4, x5)  =  U10_gaaa(x1, x2, x5)
pO_in_ggaa(x1, x2, x3, x4)  =  pO_in_ggaa(x1, x2)
U11_ggaa(x1, x2, x3, x4, x5)  =  U11_ggaa(x1, x2, x5)
U12_ggaa(x1, x2, x3, x4, x5)  =  U12_ggaa(x1, x2, x3, x5)
multJ_in_gga(x1, x2, x3)  =  multJ_in_gga(x1, x2)
U7_gga(x1, x2, x3, x4)  =  U7_gga(x1, x2, x4)
pK_in_ggaa(x1, x2, x3, x4)  =  pK_in_ggaa(x1, x2)
U17_ggaa(x1, x2, x3, x4, x5)  =  U17_ggaa(x1, x2, x5)
U18_ggaa(x1, x2, x3, x4, x5)  =  U18_ggaa(x1, x2, x3, x5)
addI_in_gga(x1, x2, x3)  =  addI_in_gga(x1, x2)
U6_gga(x1, x2, x3, x4)  =  U6_gga(x1, x2, x4)
addI_out_gga(x1, x2, x3)  =  addI_out_gga(x1, x2, x3)
pK_out_ggaa(x1, x2, x3, x4)  =  pK_out_ggaa(x1, x2, x3, x4)
multJ_out_gga(x1, x2, x3)  =  multJ_out_gga(x1, x2, x3)
pO_out_ggaa(x1, x2, x3, x4)  =  pO_out_ggaa(x1, x2, x3, x4)
pB_out_gaaa(x1, x2, x3, x4)  =  pB_out_gaaa(x1, x2, x3, x4)
factorialA_out_ga(x1, x2)  =  factorialA_out_ga(x1, x2)
U2_ga(x1, x2)  =  U2_ga(x2)
pC_in_aa(x1, x2)  =  pC_in_aa
U19_aa(x1, x2, x3)  =  U19_aa(x3)
multM_in_a(x1)  =  multM_in_a
multM_out_a(x1)  =  multM_out_a(x1)
U20_aa(x1, x2, x3)  =  U20_aa(x1, x3)
addN_in_ga(x1, x2)  =  addN_in_ga(x1)
addN_out_ga(x1, x2)  =  addN_out_ga(x1, x2)
pC_out_aa(x1, x2)  =  pC_out_aa(x1, x2)
ADDF_IN_GGA(x1, x2, x3)  =  ADDF_IN_GGA(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:

ADDF_IN_GGA(s(T70), T71, s(X160)) → ADDF_IN_GGA(T70, T71, X160)

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

ADDF_IN_GGA(s(T70), T71) → ADDF_IN_GGA(T70, T71)

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:

• ADDF_IN_GGA(s(T70), T71) → ADDF_IN_GGA(T70, T71)
  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:

PH_IN_GGAA(T38, T39, T42, X95) → MULTL_IN_GGA(T38, T39, T42)
MULTL_IN_GGA(s(T53), T54, X128) → PH_IN_GGAA(T53, T54, X127, X128)

The TRS R consists of the following rules:

factorialA_in_ga(s(s(T12)), T7) → U1_ga(T12, T7, pB_in_gaaa(T12, X22, X23, T7))
pB_in_gaaa(T12, T14, X23, T7) → U9_gaaa(T12, T14, X23, T7, factorialD_in_ga(T12, T14))
factorialD_in_ga(s(T20), X49) → U3_ga(T20, X49, pE_in_gaa(T20, X48, X49))
pE_in_gaa(T20, T22, X49) → U13_gaa(T20, T22, X49, factorialD_in_ga(T20, T22))
factorialD_in_ga(0, s(0)) → factorialD_out_ga(0, s(0))
U13_gaa(T20, T22, X49, factorialD_out_ga(T20, T22)) → U14_gaa(T20, T22, X49, multG_in_gga(T20, T22, X49))
multG_in_gga(T38, T39, X95) → U5_gga(T38, T39, X95, pH_in_ggaa(T38, T39, X94, X95))
pH_in_ggaa(T38, T39, T42, X95) → U15_ggaa(T38, T39, T42, X95, multL_in_gga(T38, T39, T42))
multL_in_gga(s(T53), T54, X128) → U8_gga(T53, T54, X128, pH_in_ggaa(T53, T54, X127, X128))
U8_gga(T53, T54, X128, pH_out_ggaa(T53, T54, X127, X128)) → multL_out_gga(s(T53), T54, X128)
multL_in_gga(0, T59, 0) → multL_out_gga(0, T59, 0)
U15_ggaa(T38, T39, T42, X95, multL_out_gga(T38, T39, T42)) → U16_ggaa(T38, T39, T42, X95, addF_in_gga(T39, T42, X95))
addF_in_gga(s(T70), T71, s(X160)) → U4_gga(T70, T71, X160, addF_in_gga(T70, T71, X160))
addF_in_gga(0, T76, T76) → addF_out_gga(0, T76, T76)
U4_gga(T70, T71, X160, addF_out_gga(T70, T71, X160)) → addF_out_gga(s(T70), T71, s(X160))
U16_ggaa(T38, T39, T42, X95, addF_out_gga(T39, T42, X95)) → pH_out_ggaa(T38, T39, T42, X95)
U5_gga(T38, T39, X95, pH_out_ggaa(T38, T39, X94, X95)) → multG_out_gga(T38, T39, X95)
U14_gaa(T20, T22, X49, multG_out_gga(T20, T22, X49)) → pE_out_gaa(T20, T22, X49)
U3_ga(T20, X49, pE_out_gaa(T20, X48, X49)) → factorialD_out_ga(s(T20), X49)
U9_gaaa(T12, T14, X23, T7, factorialD_out_ga(T12, T14)) → U10_gaaa(T12, T14, X23, T7, pO_in_ggaa(T12, T14, X23, T7))
pO_in_ggaa(T12, T14, T79, T7) → U11_ggaa(T12, T14, T79, T7, multG_in_gga(T12, T14, T79))
U11_ggaa(T12, T14, T79, T7, multG_out_gga(T12, T14, T79)) → U12_ggaa(T12, T14, T79, T7, multJ_in_gga(T12, T79, T7))
multJ_in_gga(T103, T104, T106) → U7_gga(T103, T104, T106, pK_in_ggaa(T103, T104, X210, T106))
pK_in_ggaa(T103, T104, T109, T106) → U17_ggaa(T103, T104, T109, T106, multG_in_gga(T103, T104, T109))
U17_ggaa(T103, T104, T109, T106, multG_out_gga(T103, T104, T109)) → U18_ggaa(T103, T104, T109, T106, addI_in_gga(T104, T109, T106))
addI_in_gga(s(T127), T128, s(T130)) → U6_gga(T127, T128, T130, addI_in_gga(T127, T128, T130))
addI_in_gga(0, T136, T136) → addI_out_gga(0, T136, T136)
U6_gga(T127, T128, T130, addI_out_gga(T127, T128, T130)) → addI_out_gga(s(T127), T128, s(T130))
U18_ggaa(T103, T104, T109, T106, addI_out_gga(T104, T109, T106)) → pK_out_ggaa(T103, T104, T109, T106)
U7_gga(T103, T104, T106, pK_out_ggaa(T103, T104, X210, T106)) → multJ_out_gga(T103, T104, T106)
U12_ggaa(T12, T14, T79, T7, multJ_out_gga(T12, T79, T7)) → pO_out_ggaa(T12, T14, T79, T7)
U10_gaaa(T12, T14, X23, T7, pO_out_ggaa(T12, T14, X23, T7)) → pB_out_gaaa(T12, T14, X23, T7)
U1_ga(T12, T7, pB_out_gaaa(T12, X22, X23, T7)) → factorialA_out_ga(s(s(T12)), T7)
factorialA_in_ga(s(0), T145) → U2_ga(T145, pC_in_aa(X275, T145))
pC_in_aa(T146, T145) → U19_aa(T146, T145, multM_in_a(T146))
multM_in_a(0) → multM_out_a(0)
U19_aa(T146, T145, multM_out_a(T146)) → U20_aa(T146, T145, addN_in_ga(T146, T145))
addN_in_ga(T162, s(T162)) → addN_out_ga(T162, s(T162))
U20_aa(T146, T145, addN_out_ga(T146, T145)) → pC_out_aa(T146, T145)
U2_ga(T145, pC_out_aa(X275, T145)) → factorialA_out_ga(s(0), T145)
factorialA_in_ga(0, s(0)) → factorialA_out_ga(0, s(0))

The argument filtering Pi contains the following mapping:
factorialA_in_ga(x1, x2)  =  factorialA_in_ga(x1)
s(x1)  =  s(x1)
U1_ga(x1, x2, x3)  =  U1_ga(x1, x3)
pB_in_gaaa(x1, x2, x3, x4)  =  pB_in_gaaa(x1)
U9_gaaa(x1, x2, x3, x4, x5)  =  U9_gaaa(x1, x5)
factorialD_in_ga(x1, x2)  =  factorialD_in_ga(x1)
U3_ga(x1, x2, x3)  =  U3_ga(x1, x3)
pE_in_gaa(x1, x2, x3)  =  pE_in_gaa(x1)
U13_gaa(x1, x2, x3, x4)  =  U13_gaa(x1, x4)
0  =  0
factorialD_out_ga(x1, x2)  =  factorialD_out_ga(x1, x2)
U14_gaa(x1, x2, x3, x4)  =  U14_gaa(x1, x2, x4)
multG_in_gga(x1, x2, x3)  =  multG_in_gga(x1, x2)
U5_gga(x1, x2, x3, x4)  =  U5_gga(x1, x2, x4)
pH_in_ggaa(x1, x2, x3, x4)  =  pH_in_ggaa(x1, x2)
U15_ggaa(x1, x2, x3, x4, x5)  =  U15_ggaa(x1, x2, x5)
multL_in_gga(x1, x2, x3)  =  multL_in_gga(x1, x2)
U8_gga(x1, x2, x3, x4)  =  U8_gga(x1, x2, x4)
pH_out_ggaa(x1, x2, x3, x4)  =  pH_out_ggaa(x1, x2, x3, x4)
multL_out_gga(x1, x2, x3)  =  multL_out_gga(x1, x2, x3)
U16_ggaa(x1, x2, x3, x4, x5)  =  U16_ggaa(x1, x2, x3, x5)
addF_in_gga(x1, x2, x3)  =  addF_in_gga(x1, x2)
U4_gga(x1, x2, x3, x4)  =  U4_gga(x1, x2, x4)
addF_out_gga(x1, x2, x3)  =  addF_out_gga(x1, x2, x3)
multG_out_gga(x1, x2, x3)  =  multG_out_gga(x1, x2, x3)
pE_out_gaa(x1, x2, x3)  =  pE_out_gaa(x1, x2, x3)
U10_gaaa(x1, x2, x3, x4, x5)  =  U10_gaaa(x1, x2, x5)
pO_in_ggaa(x1, x2, x3, x4)  =  pO_in_ggaa(x1, x2)
U11_ggaa(x1, x2, x3, x4, x5)  =  U11_ggaa(x1, x2, x5)
U12_ggaa(x1, x2, x3, x4, x5)  =  U12_ggaa(x1, x2, x3, x5)
multJ_in_gga(x1, x2, x3)  =  multJ_in_gga(x1, x2)
U7_gga(x1, x2, x3, x4)  =  U7_gga(x1, x2, x4)
pK_in_ggaa(x1, x2, x3, x4)  =  pK_in_ggaa(x1, x2)
U17_ggaa(x1, x2, x3, x4, x5)  =  U17_ggaa(x1, x2, x5)
U18_ggaa(x1, x2, x3, x4, x5)  =  U18_ggaa(x1, x2, x3, x5)
addI_in_gga(x1, x2, x3)  =  addI_in_gga(x1, x2)
U6_gga(x1, x2, x3, x4)  =  U6_gga(x1, x2, x4)
addI_out_gga(x1, x2, x3)  =  addI_out_gga(x1, x2, x3)
pK_out_ggaa(x1, x2, x3, x4)  =  pK_out_ggaa(x1, x2, x3, x4)
multJ_out_gga(x1, x2, x3)  =  multJ_out_gga(x1, x2, x3)
pO_out_ggaa(x1, x2, x3, x4)  =  pO_out_ggaa(x1, x2, x3, x4)
pB_out_gaaa(x1, x2, x3, x4)  =  pB_out_gaaa(x1, x2, x3, x4)
factorialA_out_ga(x1, x2)  =  factorialA_out_ga(x1, x2)
U2_ga(x1, x2)  =  U2_ga(x2)
pC_in_aa(x1, x2)  =  pC_in_aa
U19_aa(x1, x2, x3)  =  U19_aa(x3)
multM_in_a(x1)  =  multM_in_a
multM_out_a(x1)  =  multM_out_a(x1)
U20_aa(x1, x2, x3)  =  U20_aa(x1, x3)
addN_in_ga(x1, x2)  =  addN_in_ga(x1)
addN_out_ga(x1, x2)  =  addN_out_ga(x1, x2)
pC_out_aa(x1, x2)  =  pC_out_aa(x1, x2)
PH_IN_GGAA(x1, x2, x3, x4)  =  PH_IN_GGAA(x1, x2)
MULTL_IN_GGA(x1, x2, x3)  =  MULTL_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:

PH_IN_GGAA(T38, T39, T42, X95) → MULTL_IN_GGA(T38, T39, T42)
MULTL_IN_GGA(s(T53), T54, X128) → PH_IN_GGAA(T53, T54, X127, X128)

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

PH_IN_GGAA(T38, T39) → MULTL_IN_GGA(T38, T39)
MULTL_IN_GGA(s(T53), T54) → PH_IN_GGAA(T53, T54)

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:

• MULTL_IN_GGA(s(T53), T54) → PH_IN_GGAA(T53, T54)
  The graph contains the following edges 1 > 1, 2 >= 2

• PH_IN_GGAA(T38, T39) → MULTL_IN_GGA(T38, T39)
  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:

FACTORIALD_IN_GA(s(T20), X49) → PE_IN_GAA(T20, X48, X49)
PE_IN_GAA(T20, T22, X49) → FACTORIALD_IN_GA(T20, T22)

The TRS R consists of the following rules:

factorialA_in_ga(s(s(T12)), T7) → U1_ga(T12, T7, pB_in_gaaa(T12, X22, X23, T7))
pB_in_gaaa(T12, T14, X23, T7) → U9_gaaa(T12, T14, X23, T7, factorialD_in_ga(T12, T14))
factorialD_in_ga(s(T20), X49) → U3_ga(T20, X49, pE_in_gaa(T20, X48, X49))
pE_in_gaa(T20, T22, X49) → U13_gaa(T20, T22, X49, factorialD_in_ga(T20, T22))
factorialD_in_ga(0, s(0)) → factorialD_out_ga(0, s(0))
U13_gaa(T20, T22, X49, factorialD_out_ga(T20, T22)) → U14_gaa(T20, T22, X49, multG_in_gga(T20, T22, X49))
multG_in_gga(T38, T39, X95) → U5_gga(T38, T39, X95, pH_in_ggaa(T38, T39, X94, X95))
pH_in_ggaa(T38, T39, T42, X95) → U15_ggaa(T38, T39, T42, X95, multL_in_gga(T38, T39, T42))
multL_in_gga(s(T53), T54, X128) → U8_gga(T53, T54, X128, pH_in_ggaa(T53, T54, X127, X128))
U8_gga(T53, T54, X128, pH_out_ggaa(T53, T54, X127, X128)) → multL_out_gga(s(T53), T54, X128)
multL_in_gga(0, T59, 0) → multL_out_gga(0, T59, 0)
U15_ggaa(T38, T39, T42, X95, multL_out_gga(T38, T39, T42)) → U16_ggaa(T38, T39, T42, X95, addF_in_gga(T39, T42, X95))
addF_in_gga(s(T70), T71, s(X160)) → U4_gga(T70, T71, X160, addF_in_gga(T70, T71, X160))
addF_in_gga(0, T76, T76) → addF_out_gga(0, T76, T76)
U4_gga(T70, T71, X160, addF_out_gga(T70, T71, X160)) → addF_out_gga(s(T70), T71, s(X160))
U16_ggaa(T38, T39, T42, X95, addF_out_gga(T39, T42, X95)) → pH_out_ggaa(T38, T39, T42, X95)
U5_gga(T38, T39, X95, pH_out_ggaa(T38, T39, X94, X95)) → multG_out_gga(T38, T39, X95)
U14_gaa(T20, T22, X49, multG_out_gga(T20, T22, X49)) → pE_out_gaa(T20, T22, X49)
U3_ga(T20, X49, pE_out_gaa(T20, X48, X49)) → factorialD_out_ga(s(T20), X49)
U9_gaaa(T12, T14, X23, T7, factorialD_out_ga(T12, T14)) → U10_gaaa(T12, T14, X23, T7, pO_in_ggaa(T12, T14, X23, T7))
pO_in_ggaa(T12, T14, T79, T7) → U11_ggaa(T12, T14, T79, T7, multG_in_gga(T12, T14, T79))
U11_ggaa(T12, T14, T79, T7, multG_out_gga(T12, T14, T79)) → U12_ggaa(T12, T14, T79, T7, multJ_in_gga(T12, T79, T7))
multJ_in_gga(T103, T104, T106) → U7_gga(T103, T104, T106, pK_in_ggaa(T103, T104, X210, T106))
pK_in_ggaa(T103, T104, T109, T106) → U17_ggaa(T103, T104, T109, T106, multG_in_gga(T103, T104, T109))
U17_ggaa(T103, T104, T109, T106, multG_out_gga(T103, T104, T109)) → U18_ggaa(T103, T104, T109, T106, addI_in_gga(T104, T109, T106))
addI_in_gga(s(T127), T128, s(T130)) → U6_gga(T127, T128, T130, addI_in_gga(T127, T128, T130))
addI_in_gga(0, T136, T136) → addI_out_gga(0, T136, T136)
U6_gga(T127, T128, T130, addI_out_gga(T127, T128, T130)) → addI_out_gga(s(T127), T128, s(T130))
U18_ggaa(T103, T104, T109, T106, addI_out_gga(T104, T109, T106)) → pK_out_ggaa(T103, T104, T109, T106)
U7_gga(T103, T104, T106, pK_out_ggaa(T103, T104, X210, T106)) → multJ_out_gga(T103, T104, T106)
U12_ggaa(T12, T14, T79, T7, multJ_out_gga(T12, T79, T7)) → pO_out_ggaa(T12, T14, T79, T7)
U10_gaaa(T12, T14, X23, T7, pO_out_ggaa(T12, T14, X23, T7)) → pB_out_gaaa(T12, T14, X23, T7)
U1_ga(T12, T7, pB_out_gaaa(T12, X22, X23, T7)) → factorialA_out_ga(s(s(T12)), T7)
factorialA_in_ga(s(0), T145) → U2_ga(T145, pC_in_aa(X275, T145))
pC_in_aa(T146, T145) → U19_aa(T146, T145, multM_in_a(T146))
multM_in_a(0) → multM_out_a(0)
U19_aa(T146, T145, multM_out_a(T146)) → U20_aa(T146, T145, addN_in_ga(T146, T145))
addN_in_ga(T162, s(T162)) → addN_out_ga(T162, s(T162))
U20_aa(T146, T145, addN_out_ga(T146, T145)) → pC_out_aa(T146, T145)
U2_ga(T145, pC_out_aa(X275, T145)) → factorialA_out_ga(s(0), T145)
factorialA_in_ga(0, s(0)) → factorialA_out_ga(0, s(0))

The argument filtering Pi contains the following mapping:
factorialA_in_ga(x1, x2)  =  factorialA_in_ga(x1)
s(x1)  =  s(x1)
U1_ga(x1, x2, x3)  =  U1_ga(x1, x3)
pB_in_gaaa(x1, x2, x3, x4)  =  pB_in_gaaa(x1)
U9_gaaa(x1, x2, x3, x4, x5)  =  U9_gaaa(x1, x5)
factorialD_in_ga(x1, x2)  =  factorialD_in_ga(x1)
U3_ga(x1, x2, x3)  =  U3_ga(x1, x3)
pE_in_gaa(x1, x2, x3)  =  pE_in_gaa(x1)
U13_gaa(x1, x2, x3, x4)  =  U13_gaa(x1, x4)
0  =  0
factorialD_out_ga(x1, x2)  =  factorialD_out_ga(x1, x2)
U14_gaa(x1, x2, x3, x4)  =  U14_gaa(x1, x2, x4)
multG_in_gga(x1, x2, x3)  =  multG_in_gga(x1, x2)
U5_gga(x1, x2, x3, x4)  =  U5_gga(x1, x2, x4)
pH_in_ggaa(x1, x2, x3, x4)  =  pH_in_ggaa(x1, x2)
U15_ggaa(x1, x2, x3, x4, x5)  =  U15_ggaa(x1, x2, x5)
multL_in_gga(x1, x2, x3)  =  multL_in_gga(x1, x2)
U8_gga(x1, x2, x3, x4)  =  U8_gga(x1, x2, x4)
pH_out_ggaa(x1, x2, x3, x4)  =  pH_out_ggaa(x1, x2, x3, x4)
multL_out_gga(x1, x2, x3)  =  multL_out_gga(x1, x2, x3)
U16_ggaa(x1, x2, x3, x4, x5)  =  U16_ggaa(x1, x2, x3, x5)
addF_in_gga(x1, x2, x3)  =  addF_in_gga(x1, x2)
U4_gga(x1, x2, x3, x4)  =  U4_gga(x1, x2, x4)
addF_out_gga(x1, x2, x3)  =  addF_out_gga(x1, x2, x3)
multG_out_gga(x1, x2, x3)  =  multG_out_gga(x1, x2, x3)
pE_out_gaa(x1, x2, x3)  =  pE_out_gaa(x1, x2, x3)
U10_gaaa(x1, x2, x3, x4, x5)  =  U10_gaaa(x1, x2, x5)
pO_in_ggaa(x1, x2, x3, x4)  =  pO_in_ggaa(x1, x2)
U11_ggaa(x1, x2, x3, x4, x5)  =  U11_ggaa(x1, x2, x5)
U12_ggaa(x1, x2, x3, x4, x5)  =  U12_ggaa(x1, x2, x3, x5)
multJ_in_gga(x1, x2, x3)  =  multJ_in_gga(x1, x2)
U7_gga(x1, x2, x3, x4)  =  U7_gga(x1, x2, x4)
pK_in_ggaa(x1, x2, x3, x4)  =  pK_in_ggaa(x1, x2)
U17_ggaa(x1, x2, x3, x4, x5)  =  U17_ggaa(x1, x2, x5)
U18_ggaa(x1, x2, x3, x4, x5)  =  U18_ggaa(x1, x2, x3, x5)
addI_in_gga(x1, x2, x3)  =  addI_in_gga(x1, x2)
U6_gga(x1, x2, x3, x4)  =  U6_gga(x1, x2, x4)
addI_out_gga(x1, x2, x3)  =  addI_out_gga(x1, x2, x3)
pK_out_ggaa(x1, x2, x3, x4)  =  pK_out_ggaa(x1, x2, x3, x4)
multJ_out_gga(x1, x2, x3)  =  multJ_out_gga(x1, x2, x3)
pO_out_ggaa(x1, x2, x3, x4)  =  pO_out_ggaa(x1, x2, x3, x4)
pB_out_gaaa(x1, x2, x3, x4)  =  pB_out_gaaa(x1, x2, x3, x4)
factorialA_out_ga(x1, x2)  =  factorialA_out_ga(x1, x2)
U2_ga(x1, x2)  =  U2_ga(x2)
pC_in_aa(x1, x2)  =  pC_in_aa
U19_aa(x1, x2, x3)  =  U19_aa(x3)
multM_in_a(x1)  =  multM_in_a
multM_out_a(x1)  =  multM_out_a(x1)
U20_aa(x1, x2, x3)  =  U20_aa(x1, x3)
addN_in_ga(x1, x2)  =  addN_in_ga(x1)
addN_out_ga(x1, x2)  =  addN_out_ga(x1, x2)
pC_out_aa(x1, x2)  =  pC_out_aa(x1, x2)
FACTORIALD_IN_GA(x1, x2)  =  FACTORIALD_IN_GA(x1)
PE_IN_GAA(x1, x2, x3)  =  PE_IN_GAA(x1)

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:

FACTORIALD_IN_GA(s(T20), X49) → PE_IN_GAA(T20, X48, X49)
PE_IN_GAA(T20, T22, X49) → FACTORIALD_IN_GA(T20, T22)

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

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:

FACTORIALD_IN_GA(s(T20)) → PE_IN_GAA(T20)
PE_IN_GAA(T20) → FACTORIALD_IN_GA(T20)

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

(33) QDPSizeChangeProof (EQUIVALENT transformation)

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

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

• PE_IN_GAA(T20) → FACTORIALD_IN_GA(T20)
  The graph contains the following edges 1 >= 1

• FACTORIALD_IN_GA(s(T20)) → PE_IN_GAA(T20)
  The graph contains the following edges 1 > 1

(34) YES