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

(0) Obligation:

Clauses:

convert([], B, 0).
convert(.(0, XS), B, X) :- ','(convert(XS, B, Y), times(Y, B, X)).
convert(.(s(Y), XS), B, s(X)) :- convert(.(Y, XS), B, X).
plus(0, Y, Y).
plus(s(X), Y, s(Z)) :- plus(X, Y, Z).
times(0, Y, 0).
times(s(X), Y, Z) :- ','(times(X, Y, U), plus(Y, U, Z)).

Query: convert(g,g,a)

(1) PrologToPiTRSViaGraphTransformerProof (SOUND transformation)

Transformed Prolog program to (Pi-)TRS.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
3 [label="A: convert(T1, T2, T3)\n\nT1 is ground\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
6 [label="6: convert(T1, T2, T3), SCOPE: 1, CLAUSE: 0 | convert(T1, T2, T3), SCOPE: 1, CLAUSE: 1 | convert(T1, T2, T3), SCOPE: 1, CLAUSE: 2\n\nT1 is ground\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
11 [label="11: true | convert([], T5, T3), SCOPE: 1, CLAUSE: 1 | convert([], T5, T3), SCOPE: 1, CLAUSE: 2\n\nT5 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
12 [label="12: convert(T1, T2, T3), SCOPE: 1, CLAUSE: 1 | convert(T1, T2, T3), SCOPE: 1, CLAUSE: 2\n\nT1 is ground\nT2 is ground\nX2 is free\nconvert(T1, T2, T3) !=? convert([], X2, 0)", fontsize=16, style=filled, fillcolor=lightyellow];
13 [label="13: convert([], T5, T3), SCOPE: 1, CLAUSE: 1 | convert([], T5, T3), SCOPE: 1, CLAUSE: 2\n\nT5 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
14 [label="14: convert([], T5, T3), SCOPE: 1, CLAUSE: 2\n\nT5 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
15 [label="15: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
16 [label="16: ','(convert(T9, T10, X16), times(X16, T10, T12)) | convert(.(0, T9), T10, T3), SCOPE: 1, CLAUSE: 2\n\nT9 is ground\nT10 is ground\nX16 is free", fontsize=16, style=filled, fillcolor=lightyellow];
17 [label="17: convert(T1, T2, T3), SCOPE: 1, CLAUSE: 2\n\nT1 is ground\nT2 is ground\nX2 is free\nX13 is free\nX14 is free\nX15 is free\nconvert(T1, T2, T3) !=? convert([], X2, 0)\nconvert(T1, T2, T3) !=? convert(.(0, X13), X14, X15)", fontsize=16, style=filled, fillcolor=lightyellow];
18 [label="18: ','(convert(T9, T10, X16), times(X16, T10, T12)), SCOPE: 2, CLAUSE: 0 | ','(convert(T9, T10, X16), times(X16, T10, T12)), SCOPE: 2, CLAUSE: 1 | ','(convert(T9, T10, X16), times(X16, T10, T12)), SCOPE: 2, CLAUSE: 2 | ?_2 | convert(.(0, T9), T10, T3), SCOPE: 1, CLAUSE: 2\n\nT9 is ground\nT10 is ground\nX16 is free", fontsize=16, style=filled, fillcolor=lightyellow];
19 [label="19: ','(convert(T9, T10, X16), times(X16, T10, T12)), SCOPE: 2, CLAUSE: 0\n\nT9 is ground\nT10 is ground\nX16 is free", fontsize=16, style=filled, fillcolor=lightyellow];
20 [label="20: ','(convert(T9, T10, X16), times(X16, T10, T12)), SCOPE: 2, CLAUSE: 1 | ','(convert(T9, T10, X16), times(X16, T10, T12)), SCOPE: 2, CLAUSE: 2 | ?_2 | convert(.(0, T9), T10, T3), SCOPE: 1, CLAUSE: 2\n\nT9 is ground\nT10 is ground\nX16 is free", fontsize=16, style=filled, fillcolor=lightyellow];
22 [label="22: times(0, T17, T12)\n\nT17 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
23 [label="23: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
40 [label="40: times(0, T17, T12), SCOPE: 3, CLAUSE: 5 | times(0, T17, T12), SCOPE: 3, CLAUSE: 6\n\nT17 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
42 [label="42: times(0, T17, T12), SCOPE: 3, CLAUSE: 5\n\nT17 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
43 [label="43: times(0, T17, T12), SCOPE: 3, CLAUSE: 6\n\nT17 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
46 [label="46: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
47 [label="47: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
49 [label="49: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
51 [label="51: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
58 [label="58: ','(convert(T9, T10, X16), times(X16, T10, T12)), SCOPE: 2, CLAUSE: 1\n\nT9 is ground\nT10 is ground\nX16 is free", fontsize=16, style=filled, fillcolor=lightyellow];
61 [label="61: ','(convert(T9, T10, X16), times(X16, T10, T12)), SCOPE: 2, CLAUSE: 2 | ?_2 | convert(.(0, T9), T10, T3), SCOPE: 1, CLAUSE: 2\n\nT9 is ground\nT10 is ground\nX16 is free", fontsize=16, style=filled, fillcolor=lightyellow];
82 [label="B: ','(','(convert(T33, T34, X53), times(X53, T34, X54)), times(X54, T34, T12))\n\nT33 is ground\nT34 is ground\nX54 is free\nX53 is free", fontsize=16, style=filled, fillcolor=lightyellow];
83 [label="83: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
89 [label="E: convert(T33, T34, X53)\n\nT33 is ground\nT34 is ground\nX53 is free", fontsize=16, style=filled, fillcolor=lightyellow];
91 [label="M: ','(times(T37, T34, X54), times(X54, T34, T12))\n\nT34 is ground\nT37 is ground\nX54 is free", fontsize=16, style=filled, fillcolor=lightyellow];
94 [label="94: convert(T33, T34, X53), SCOPE: 4, CLAUSE: 0 | convert(T33, T34, X53), SCOPE: 4, CLAUSE: 1 | convert(T33, T34, X53), SCOPE: 4, CLAUSE: 2\n\nT33 is ground\nT34 is ground\nX53 is free", fontsize=16, style=filled, fillcolor=lightyellow];
96 [label="96: convert(T33, T34, X53), SCOPE: 4, CLAUSE: 0\n\nT33 is ground\nT34 is ground\nX53 is free", fontsize=16, style=filled, fillcolor=lightyellow];
98 [label="98: convert(T33, T34, X53), SCOPE: 4, CLAUSE: 1 | convert(T33, T34, X53), SCOPE: 4, CLAUSE: 2\n\nT33 is ground\nT34 is ground\nX53 is free", fontsize=16, style=filled, fillcolor=lightyellow];
114 [label="114: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
116 [label="116: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
118 [label="118: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
121 [label="121: convert(T33, T34, X53), SCOPE: 4, CLAUSE: 1\n\nT33 is ground\nT34 is ground\nX53 is free", fontsize=16, style=filled, fillcolor=lightyellow];
123 [label="123: convert(T33, T34, X53), SCOPE: 4, CLAUSE: 2\n\nT33 is ground\nT34 is ground\nX53 is free", fontsize=16, style=filled, fillcolor=lightyellow];
129 [label="F: ','(convert(T53, T54, X85), times(X85, T54, X86))\n\nT53 is ground\nT54 is ground\nX86 is free\nX85 is free", fontsize=16, style=filled, fillcolor=lightyellow];
132 [label="132: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
136 [label="136: convert(T53, T54, X85)\n\nT53 is ground\nT54 is ground\nX85 is free", fontsize=16, style=filled, fillcolor=lightyellow];
137 [label="G: times(T57, T54, X86)\n\nT54 is ground\nT57 is ground\nX86 is free", fontsize=16, style=filled, fillcolor=lightyellow];
140 [label="140: times(T57, T54, X86), SCOPE: 5, CLAUSE: 5 | times(T57, T54, X86), SCOPE: 5, CLAUSE: 6\n\nT54 is ground\nT57 is ground\nX86 is free", fontsize=16, style=filled, fillcolor=lightyellow];
141 [label="141: times(T57, T54, X86), SCOPE: 5, CLAUSE: 5\n\nT54 is ground\nT57 is ground\nX86 is free", fontsize=16, style=filled, fillcolor=lightyellow];
142 [label="142: times(T57, T54, X86), SCOPE: 5, CLAUSE: 6\n\nT54 is ground\nT57 is ground\nX86 is free", fontsize=16, style=filled, fillcolor=lightyellow];
153 [label="153: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
154 [label="154: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
155 [label="155: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
158 [label="H: ','(times(T71, T72, X110), plus(T72, X110, X111))\n\nT71 is ground\nT72 is ground\nX111 is free\nX110 is free", fontsize=16, style=filled, fillcolor=lightyellow];
159 [label="159: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
160 [label="160: times(T71, T72, X110)\n\nT71 is ground\nT72 is ground\nX110 is free", fontsize=16, style=filled, fillcolor=lightyellow];
161 [label="I: plus(T72, T75, X111)\n\nT72 is ground\nT75 is ground\nX111 is free", fontsize=16, style=filled, fillcolor=lightyellow];
168 [label="168: plus(T72, T75, X111), SCOPE: 6, CLAUSE: 3 | plus(T72, T75, X111), SCOPE: 6, CLAUSE: 4\n\nT72 is ground\nT75 is ground\nX111 is free", fontsize=16, style=filled, fillcolor=lightyellow];
169 [label="169: plus(T72, T75, X111), SCOPE: 6, CLAUSE: 3\n\nT72 is ground\nT75 is ground\nX111 is free", fontsize=16, style=filled, fillcolor=lightyellow];
171 [label="171: plus(T72, T75, X111), SCOPE: 6, CLAUSE: 4\n\nT72 is ground\nT75 is ground\nX111 is free", fontsize=16, style=filled, fillcolor=lightyellow];
173 [label="173: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
174 [label="174: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
175 [label="175: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
178 [label="178: plus(T89, T90, X134)\n\nT89 is ground\nT90 is ground\nX134 is free", fontsize=16, style=filled, fillcolor=lightyellow];
179 [label="179: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
188 [label="188: convert(.(T99, T100), T101, X151)\n\nT99 is ground\nT100 is ground\nT101 is ground\nX151 is free", fontsize=16, style=filled, fillcolor=lightyellow];
189 [label="189: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
194 [label="194: times(T37, T34, X54)\n\nT34 is ground\nT37 is ground\nX54 is free", fontsize=16, style=filled, fillcolor=lightyellow];
195 [label="K: times(T104, T34, T12)\n\nT34 is ground\nT104 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
196 [label="196: times(T104, T34, T12), SCOPE: 7, CLAUSE: 5 | times(T104, T34, T12), SCOPE: 7, CLAUSE: 6\n\nT34 is ground\nT104 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
197 [label="197: times(T104, T34, T12), SCOPE: 7, CLAUSE: 5\n\nT34 is ground\nT104 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
198 [label="198: times(T104, T34, T12), SCOPE: 7, CLAUSE: 6\n\nT34 is ground\nT104 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
199 [label="199: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
200 [label="200: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
201 [label="201: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
204 [label="L: ','(times(T120, T121, X175), plus(T121, X175, T123))\n\nT120 is ground\nT121 is ground\nX175 is free", fontsize=16, style=filled, fillcolor=lightyellow];
205 [label="205: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
206 [label="206: times(T120, T121, X175)\n\nT120 is ground\nT121 is ground\nX175 is free", fontsize=16, style=filled, fillcolor=lightyellow];
207 [label="J: plus(T121, T126, T123)\n\nT121 is ground\nT126 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
213 [label="213: plus(T121, T126, T123), SCOPE: 8, CLAUSE: 3 | plus(T121, T126, T123), SCOPE: 8, CLAUSE: 4\n\nT121 is ground\nT126 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
215 [label="215: plus(T121, T126, T123), SCOPE: 8, CLAUSE: 3\n\nT121 is ground\nT126 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
216 [label="216: plus(T121, T126, T123), SCOPE: 8, CLAUSE: 4\n\nT121 is ground\nT126 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
217 [label="217: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
218 [label="218: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
219 [label="219: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
222 [label="222: plus(T142, T143, T145)\n\nT142 is ground\nT143 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
223 [label="223: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
226 [label="226: ','(convert(T9, T10, X16), times(X16, T10, T12)), SCOPE: 2, CLAUSE: 2\n\nT9 is ground\nT10 is ground\nX16 is free", fontsize=16, style=filled, fillcolor=lightyellow];
227 [label="227: ?_2 | convert(.(0, T9), T10, T3), SCOPE: 1, CLAUSE: 2\n\nT9 is ground\nT10 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
230 [label="C: ','(convert(.(T160, T161), T162, X222), times(s(X222), T162, T12))\n\nT160 is ground\nT161 is ground\nT162 is ground\nX222 is free", fontsize=16, style=filled, fillcolor=lightyellow];
231 [label="231: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
235 [label="235: convert(.(T160, T161), T162, X222)\n\nT160 is ground\nT161 is ground\nT162 is ground\nX222 is free", fontsize=16, style=filled, fillcolor=lightyellow];
236 [label="236: times(s(T163), T162, T12)\n\nT162 is ground\nT163 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
238 [label="238: convert(.(0, T9), T10, T3), SCOPE: 1, CLAUSE: 2\n\nT9 is ground\nT10 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
239 [label="239: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
244 [label="244: convert(.(T168, T169), T170, T172)\n\nT168 is ground\nT169 is ground\nT170 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
245 [label="245: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
246 [label="246: convert(.(T168, T169), T170, T172), SCOPE: 9, CLAUSE: 0 | convert(.(T168, T169), T170, T172), SCOPE: 9, CLAUSE: 1 | convert(.(T168, T169), T170, T172), SCOPE: 9, CLAUSE: 2\n\nT168 is ground\nT169 is ground\nT170 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
247 [label="247: convert(.(T168, T169), T170, T172), SCOPE: 9, CLAUSE: 1 | convert(.(T168, T169), T170, T172), SCOPE: 9, CLAUSE: 2\n\nT168 is ground\nT169 is ground\nT170 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
250 [label="250: convert(.(T168, T169), T170, T172), SCOPE: 9, CLAUSE: 1\n\nT168 is ground\nT169 is ground\nT170 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
251 [label="251: convert(.(T168, T169), T170, T172), SCOPE: 9, CLAUSE: 2\n\nT168 is ground\nT169 is ground\nT170 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
254 [label="D: ','(convert(T185, T186, X259), times(X259, T186, T188))\n\nT185 is ground\nT186 is ground\nX259 is free", fontsize=16, style=filled, fillcolor=lightyellow];
255 [label="255: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
258 [label="258: convert(T185, T186, X259)\n\nT185 is ground\nT186 is ground\nX259 is free", fontsize=16, style=filled, fillcolor=lightyellow];
259 [label="259: times(T191, T186, T188)\n\nT186 is ground\nT191 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
262 [label="262: convert(.(T204, T205), T206, T208)\n\nT204 is ground\nT205 is ground\nT206 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
263 [label="263: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
264 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
3 -> 264 [arrowhead = none ];
264 -> 6;

265 [label="EVAL with clause\nconvert([], X2, 0).\nand substitutionT1 -> [],\nT2 -> T5,\nX2 -> T5,\nT3 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
6 -> 265 [arrowhead = none ];
265 -> 11;

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

267 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
11 -> 267 [arrowhead = none ];
267 -> 13;

268 [label="EVAL with clause\nconvert(.(0, X13), X14, X15) :- ','(convert(X13, X14, X16), times(X16, X14, X15)).\nand substitutionX13 -> T9,\nT1 -> .(0, T9),\nT2 -> T10,\nX14 -> T10,\nT3 -> T12,\nX15 -> T12,\nT11 -> T12", fontsize=14, style = filled, fillcolor = lightblue];
12 -> 268 [arrowhead = none ];
268 -> 16;

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

270 [label="BACKTRACK\nfor clause: convert(.(0, XS), B, X) :- ','(convert(XS, B, Y), times(Y, B, X))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
13 -> 270 [arrowhead = none ];
270 -> 14;

271 [label="BACKTRACK\nfor clause: convert(.(s(Y), XS), B, s(X)) :- convert(.(Y, XS), B, X)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
14 -> 271 [arrowhead = none ];
271 -> 15;

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

273 [label="EVAL with clause\nconvert(.(s(X237), X238), X239, s(X240)) :- convert(.(X237, X238), X239, X240).\nand substitutionX237 -> T168,\nX238 -> T169,\nT1 -> .(s(T168), T169),\nT2 -> T170,\nX239 -> T170,\nX240 -> T172,\nT3 -> s(T172),\nT171 -> T172", fontsize=14, style = filled, fillcolor = lightblue];
17 -> 273 [arrowhead = none ];
273 -> 244;

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

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

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

277 [label="EVAL with clause\nconvert([], X21, 0).\nand substitutionT9 -> [],\nT10 -> T17,\nX21 -> T17,\nX16 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
19 -> 277 [arrowhead = none ];
277 -> 22;

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

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

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

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

282 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
40 -> 282 [arrowhead = none ];
282 -> 42;

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

284 [label="EVAL with clause\ntimes(0, X28, 0).\nand substitutionT17 -> T24,\nX28 -> T24,\nT12 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
42 -> 284 [arrowhead = none ];
284 -> 46;

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

286 [label="BACKTRACK\nfor clause: times(s(X), Y, Z) :- ','(times(X, Y, U), plus(Y, U, Z))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
43 -> 286 [arrowhead = none ];
286 -> 51;

287 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
46 -> 287 [arrowhead = none ];
287 -> 49;

288 [label="EVAL with clause\nconvert(.(0, X50), X51, X52) :- ','(convert(X50, X51, X53), times(X53, X51, X52)).\nand substitutionX50 -> T33,\nT9 -> .(0, T33),\nT10 -> T34,\nX51 -> T34,\nX16 -> X54,\nX52 -> X54", fontsize=14, style = filled, fillcolor = lightblue];
58 -> 288 [arrowhead = none ];
288 -> 82;

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

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

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

292 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
82 -> 292 [arrowhead = none ];
292 -> 89;

293 [label="SPLIT 2\nnew knowledge:\nT33 is ground\nT34 is ground\nT37 is ground\nreplacements:X53 -> T37", fontsize=14, style = filled, fillcolor = violet];
82 -> 293 [arrowhead = none ];
293 -> 91;

294 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
89 -> 294 [arrowhead = none ];
294 -> 94;

295 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
91 -> 295 [arrowhead = none ];
295 -> 194;

296 [label="SPLIT 2\nnew knowledge:\nT37 is ground\nT34 is ground\nT104 is ground\nreplacements:X54 -> T104", fontsize=14, style = filled, fillcolor = violet];
91 -> 296 [arrowhead = none ];
296 -> 195;

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

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

299 [label="EVAL with clause\nconvert([], X63, 0).\nand substitutionT33 -> [],\nT34 -> T44,\nX63 -> T44,\nX53 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
96 -> 299 [arrowhead = none ];
299 -> 114;

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

301 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
98 -> 301 [arrowhead = none ];
301 -> 121;

302 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
98 -> 302 [arrowhead = none ];
302 -> 123;

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

304 [label="EVAL with clause\nconvert(.(0, X82), X83, X84) :- ','(convert(X82, X83, X85), times(X85, X83, X84)).\nand substitutionX82 -> T53,\nT33 -> .(0, T53),\nT34 -> T54,\nX83 -> T54,\nX53 -> X86,\nX84 -> X86", fontsize=14, style = filled, fillcolor = lightblue];
121 -> 304 [arrowhead = none ];
304 -> 129;

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

306 [label="EVAL with clause\nconvert(.(s(X147), X148), X149, s(X150)) :- convert(.(X147, X148), X149, X150).\nand substitutionX147 -> T99,\nX148 -> T100,\nT33 -> .(s(T99), T100),\nT34 -> T101,\nX149 -> T101,\nX150 -> X151,\nX53 -> s(X151)", fontsize=14, style = filled, fillcolor = lightblue];
123 -> 306 [arrowhead = none ];
306 -> 188;

307 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
123 -> 307 [arrowhead = none ];
307 -> 189;

308 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
129 -> 308 [arrowhead = none ];
308 -> 136;

309 [label="SPLIT 2\nnew knowledge:\nT53 is ground\nT54 is ground\nT57 is ground\nreplacements:X85 -> T57", fontsize=14, style = filled, fillcolor = violet];
129 -> 309 [arrowhead = none ];
309 -> 137;

310 [label="INSTANCE with matching:\nT33 -> T53\nT34 -> T54\nX53 -> X85", fontsize=14, style = filled, fillcolor = lightgrey];
136 -> 310 [arrowhead = none , style=dashed];
310 -> 89[style=dashed];

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

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

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

314 [label="EVAL with clause\ntimes(0, X97, 0).\nand substitutionT57 -> 0,\nT54 -> T66,\nX97 -> T66,\nX86 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
141 -> 314 [arrowhead = none ];
314 -> 153;

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

316 [label="EVAL with clause\ntimes(s(X107), X108, X109) :- ','(times(X107, X108, X110), plus(X108, X110, X109)).\nand substitutionX107 -> T71,\nT57 -> s(T71),\nT54 -> T72,\nX108 -> T72,\nX86 -> X111,\nX109 -> X111", fontsize=14, style = filled, fillcolor = lightblue];
142 -> 316 [arrowhead = none ];
316 -> 158;

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

318 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
153 -> 318 [arrowhead = none ];
318 -> 155;

319 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
158 -> 319 [arrowhead = none ];
319 -> 160;

320 [label="SPLIT 2\nnew knowledge:\nT71 is ground\nT72 is ground\nT75 is ground\nreplacements:X110 -> T75", fontsize=14, style = filled, fillcolor = violet];
158 -> 320 [arrowhead = none ];
320 -> 161;

321 [label="INSTANCE with matching:\nT57 -> T71\nT54 -> T72\nX86 -> X110", fontsize=14, style = filled, fillcolor = lightgrey];
160 -> 321 [arrowhead = none , style=dashed];
321 -> 137[style=dashed];

322 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
161 -> 322 [arrowhead = none ];
322 -> 168;

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

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

325 [label="EVAL with clause\nplus(0, X122, X122).\nand substitutionT72 -> 0,\nT75 -> T84,\nX122 -> T84,\nX111 -> T84", fontsize=14, style = filled, fillcolor = lightblue];
169 -> 325 [arrowhead = none ];
325 -> 173;

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

327 [label="EVAL with clause\nplus(s(X131), X132, s(X133)) :- plus(X131, X132, X133).\nand substitutionX131 -> T89,\nT72 -> s(T89),\nT75 -> T90,\nX132 -> T90,\nX133 -> X134,\nX111 -> s(X134)", fontsize=14, style = filled, fillcolor = lightblue];
171 -> 327 [arrowhead = none ];
327 -> 178;

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

329 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
173 -> 329 [arrowhead = none ];
329 -> 175;

330 [label="INSTANCE with matching:\nT72 -> T89\nT75 -> T90\nX111 -> X134", fontsize=14, style = filled, fillcolor = lightgrey];
178 -> 330 [arrowhead = none , style=dashed];
330 -> 161[style=dashed];

331 [label="INSTANCE with matching:\nT1 -> .(T99, T100)\nT2 -> T101\nT3 -> X151", fontsize=14, style = filled, fillcolor = lightgrey];
188 -> 331 [arrowhead = none , style=dashed];
331 -> 3[style=dashed];

332 [label="INSTANCE with matching:\nT57 -> T37\nT54 -> T34\nX86 -> X54", fontsize=14, style = filled, fillcolor = lightgrey];
194 -> 332 [arrowhead = none , style=dashed];
332 -> 137[style=dashed];

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

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

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

336 [label="EVAL with clause\ntimes(0, X164, 0).\nand substitutionT104 -> 0,\nT34 -> T113,\nX164 -> T113,\nT12 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
197 -> 336 [arrowhead = none ];
336 -> 199;

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

338 [label="EVAL with clause\ntimes(s(X172), X173, X174) :- ','(times(X172, X173, X175), plus(X173, X175, X174)).\nand substitutionX172 -> T120,\nT104 -> s(T120),\nT34 -> T121,\nX173 -> T121,\nT12 -> T123,\nX174 -> T123,\nT122 -> T123", fontsize=14, style = filled, fillcolor = lightblue];
198 -> 338 [arrowhead = none ];
338 -> 204;

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

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

341 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
204 -> 341 [arrowhead = none ];
341 -> 206;

342 [label="SPLIT 2\nnew knowledge:\nT120 is ground\nT121 is ground\nT126 is ground\nreplacements:X175 -> T126", fontsize=14, style = filled, fillcolor = violet];
204 -> 342 [arrowhead = none ];
342 -> 207;

343 [label="INSTANCE with matching:\nT57 -> T120\nT54 -> T121\nX86 -> X175", fontsize=14, style = filled, fillcolor = lightgrey];
206 -> 343 [arrowhead = none , style=dashed];
343 -> 137[style=dashed];

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

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

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

347 [label="EVAL with clause\nplus(0, X186, X186).\nand substitutionT121 -> 0,\nT126 -> T135,\nX186 -> T135,\nT123 -> T135", fontsize=14, style = filled, fillcolor = lightblue];
215 -> 347 [arrowhead = none ];
347 -> 217;

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

349 [label="EVAL with clause\nplus(s(X193), X194, s(X195)) :- plus(X193, X194, X195).\nand substitutionX193 -> T142,\nT121 -> s(T142),\nT126 -> T143,\nX194 -> T143,\nX195 -> T145,\nT123 -> s(T145),\nT144 -> T145", fontsize=14, style = filled, fillcolor = lightblue];
216 -> 349 [arrowhead = none ];
349 -> 222;

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

351 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
217 -> 351 [arrowhead = none ];
351 -> 219;

352 [label="INSTANCE with matching:\nT121 -> T142\nT126 -> T143\nT123 -> T145", fontsize=14, style = filled, fillcolor = lightgrey];
222 -> 352 [arrowhead = none , style=dashed];
352 -> 207[style=dashed];

353 [label="EVAL with clause\nconvert(.(s(X218), X219), X220, s(X221)) :- convert(.(X218, X219), X220, X221).\nand substitutionX218 -> T160,\nX219 -> T161,\nT9 -> .(s(T160), T161),\nT10 -> T162,\nX220 -> T162,\nX221 -> X222,\nX16 -> s(X222)", fontsize=14, style = filled, fillcolor = lightblue];
226 -> 353 [arrowhead = none ];
353 -> 230;

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

355 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
227 -> 355 [arrowhead = none ];
355 -> 238;

356 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
230 -> 356 [arrowhead = none ];
356 -> 235;

357 [label="SPLIT 2\nnew knowledge:\nT160 is ground\nT161 is ground\nT162 is ground\nT163 is ground\nreplacements:X222 -> T163", fontsize=14, style = filled, fillcolor = violet];
230 -> 357 [arrowhead = none ];
357 -> 236;

358 [label="INSTANCE with matching:\nT1 -> .(T160, T161)\nT2 -> T162\nT3 -> X222", fontsize=14, style = filled, fillcolor = lightgrey];
235 -> 358 [arrowhead = none , style=dashed];
358 -> 3[style=dashed];

359 [label="INSTANCE with matching:\nT104 -> s(T163)\nT34 -> T162", fontsize=14, style = filled, fillcolor = lightgrey];
236 -> 359 [arrowhead = none , style=dashed];
359 -> 195[style=dashed];

360 [label="BACKTRACK\nfor clause: convert(.(s(Y), XS), B, s(X)) :- convert(.(Y, XS), B, X)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
238 -> 360 [arrowhead = none ];
360 -> 239;

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

362 [label="BACKTRACK\nfor clause: convert([], B, 0)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
246 -> 362 [arrowhead = none ];
362 -> 247;

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

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

365 [label="EVAL with clause\nconvert(.(0, X256), X257, X258) :- ','(convert(X256, X257, X259), times(X259, X257, X258)).\nand substitutionT168 -> 0,\nT169 -> T185,\nX256 -> T185,\nT170 -> T186,\nX257 -> T186,\nT172 -> T188,\nX258 -> T188,\nT187 -> T188", fontsize=14, style = filled, fillcolor = lightblue];
250 -> 365 [arrowhead = none ];
365 -> 254;

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

367 [label="EVAL with clause\nconvert(.(s(X274), X275), X276, s(X277)) :- convert(.(X274, X275), X276, X277).\nand substitutionX274 -> T204,\nT168 -> s(T204),\nT169 -> T205,\nX275 -> T205,\nT170 -> T206,\nX276 -> T206,\nX277 -> T208,\nT172 -> s(T208),\nT207 -> T208", fontsize=14, style = filled, fillcolor = lightblue];
251 -> 367 [arrowhead = none ];
367 -> 262;

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

369 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
254 -> 369 [arrowhead = none ];
369 -> 258;

370 [label="SPLIT 2\nnew knowledge:\nT185 is ground\nT186 is ground\nT191 is ground\nreplacements:X259 -> T191", fontsize=14, style = filled, fillcolor = violet];
254 -> 370 [arrowhead = none ];
370 -> 259;

371 [label="INSTANCE with matching:\nT33 -> T185\nT34 -> T186\nX53 -> X259", fontsize=14, style = filled, fillcolor = lightgrey];
258 -> 371 [arrowhead = none , style=dashed];
371 -> 89[style=dashed];

372 [label="INSTANCE with matching:\nT104 -> T191\nT34 -> T186\nT12 -> T188", fontsize=14, style = filled, fillcolor = lightgrey];
259 -> 372 [arrowhead = none , style=dashed];
372 -> 195[style=dashed];

373 [label="INSTANCE with matching:\nT1 -> .(T204, T205)\nT2 -> T206\nT3 -> T208", fontsize=14, style = filled, fillcolor = lightgrey];
262 -> 373 [arrowhead = none , style=dashed];
373 -> 3[style=dashed];

}

(2) Obligation:

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

convertA_in_gga([], T5, 0) → convertA_out_gga([], T5, 0)
convertA_in_gga(.(0, []), T24, 0) → convertA_out_gga(.(0, []), T24, 0)
convertA_in_gga(.(0, .(0, T33)), T34, T12) → U1_gga(T33, T34, T12, pB_in_ggaaa(T33, T34, X53, X54, T12))
pB_in_ggaaa(T33, T34, T37, X54, T12) → U11_ggaaa(T33, T34, T37, X54, T12, convertE_in_gga(T33, T34, T37))
convertE_in_gga([], T44, 0) → convertE_out_gga([], T44, 0)
convertE_in_gga(.(0, T53), T54, X86) → U5_gga(T53, T54, X86, pF_in_ggaa(T53, T54, X85, X86))
pF_in_ggaa(T53, T54, T57, X86) → U15_ggaa(T53, T54, T57, X86, convertE_in_gga(T53, T54, T57))
convertE_in_gga(.(s(T99), T100), T101, s(X151)) → U6_gga(T99, T100, T101, X151, convertA_in_gga(.(T99, T100), T101, X151))
convertA_in_gga(.(0, .(s(T160), T161)), T162, T12) → U2_gga(T160, T161, T162, T12, pC_in_gggaa(T160, T161, T162, X222, T12))
pC_in_gggaa(T160, T161, T162, T163, T12) → U21_gggaa(T160, T161, T162, T163, T12, convertA_in_gga(.(T160, T161), T162, T163))
convertA_in_gga(.(s(0), T185), T186, s(T188)) → U3_gga(T185, T186, T188, pD_in_ggaa(T185, T186, X259, T188))
pD_in_ggaa(T185, T186, T191, T188) → U23_ggaa(T185, T186, T191, T188, convertE_in_gga(T185, T186, T191))
U23_ggaa(T185, T186, T191, T188, convertE_out_gga(T185, T186, T191)) → U24_ggaa(T185, T186, T191, T188, timesK_in_gga(T191, T186, T188))
timesK_in_gga(0, T113, 0) → timesK_out_gga(0, T113, 0)
timesK_in_gga(s(T120), T121, T123) → U10_gga(T120, T121, T123, pL_in_ggaa(T120, T121, X175, T123))
pL_in_ggaa(T120, T121, T126, T123) → U19_ggaa(T120, T121, T126, T123, timesG_in_gga(T120, T121, T126))
timesG_in_gga(0, T66, 0) → timesG_out_gga(0, T66, 0)
timesG_in_gga(s(T71), T72, X111) → U7_gga(T71, T72, X111, pH_in_ggaa(T71, T72, X110, X111))
pH_in_ggaa(T71, T72, T75, X111) → U17_ggaa(T71, T72, T75, X111, timesG_in_gga(T71, T72, T75))
U17_ggaa(T71, T72, T75, X111, timesG_out_gga(T71, T72, T75)) → U18_ggaa(T71, T72, T75, X111, plusI_in_gga(T72, T75, X111))
plusI_in_gga(0, T84, T84) → plusI_out_gga(0, T84, T84)
plusI_in_gga(s(T89), T90, s(X134)) → U8_gga(T89, T90, X134, plusI_in_gga(T89, T90, X134))
U8_gga(T89, T90, X134, plusI_out_gga(T89, T90, X134)) → plusI_out_gga(s(T89), T90, s(X134))
U18_ggaa(T71, T72, T75, X111, plusI_out_gga(T72, T75, X111)) → pH_out_ggaa(T71, T72, T75, X111)
U7_gga(T71, T72, X111, pH_out_ggaa(T71, T72, X110, X111)) → timesG_out_gga(s(T71), T72, X111)
U19_ggaa(T120, T121, T126, T123, timesG_out_gga(T120, T121, T126)) → U20_ggaa(T120, T121, T126, T123, plusJ_in_gga(T121, T126, T123))
plusJ_in_gga(0, T135, T135) → plusJ_out_gga(0, T135, T135)
plusJ_in_gga(s(T142), T143, s(T145)) → U9_gga(T142, T143, T145, plusJ_in_gga(T142, T143, T145))
U9_gga(T142, T143, T145, plusJ_out_gga(T142, T143, T145)) → plusJ_out_gga(s(T142), T143, s(T145))
U20_ggaa(T120, T121, T126, T123, plusJ_out_gga(T121, T126, T123)) → pL_out_ggaa(T120, T121, T126, T123)
U10_gga(T120, T121, T123, pL_out_ggaa(T120, T121, X175, T123)) → timesK_out_gga(s(T120), T121, T123)
U24_ggaa(T185, T186, T191, T188, timesK_out_gga(T191, T186, T188)) → pD_out_ggaa(T185, T186, T191, T188)
U3_gga(T185, T186, T188, pD_out_ggaa(T185, T186, X259, T188)) → convertA_out_gga(.(s(0), T185), T186, s(T188))
convertA_in_gga(.(s(s(T204)), T205), T206, s(s(T208))) → U4_gga(T204, T205, T206, T208, convertA_in_gga(.(T204, T205), T206, T208))
U4_gga(T204, T205, T206, T208, convertA_out_gga(.(T204, T205), T206, T208)) → convertA_out_gga(.(s(s(T204)), T205), T206, s(s(T208)))
U21_gggaa(T160, T161, T162, T163, T12, convertA_out_gga(.(T160, T161), T162, T163)) → U22_gggaa(T160, T161, T162, T163, T12, timesK_in_gga(s(T163), T162, T12))
U22_gggaa(T160, T161, T162, T163, T12, timesK_out_gga(s(T163), T162, T12)) → pC_out_gggaa(T160, T161, T162, T163, T12)
U2_gga(T160, T161, T162, T12, pC_out_gggaa(T160, T161, T162, X222, T12)) → convertA_out_gga(.(0, .(s(T160), T161)), T162, T12)
U6_gga(T99, T100, T101, X151, convertA_out_gga(.(T99, T100), T101, X151)) → convertE_out_gga(.(s(T99), T100), T101, s(X151))
U15_ggaa(T53, T54, T57, X86, convertE_out_gga(T53, T54, T57)) → U16_ggaa(T53, T54, T57, X86, timesG_in_gga(T57, T54, X86))
U16_ggaa(T53, T54, T57, X86, timesG_out_gga(T57, T54, X86)) → pF_out_ggaa(T53, T54, T57, X86)
U5_gga(T53, T54, X86, pF_out_ggaa(T53, T54, X85, X86)) → convertE_out_gga(.(0, T53), T54, X86)
U11_ggaaa(T33, T34, T37, X54, T12, convertE_out_gga(T33, T34, T37)) → U12_ggaaa(T33, T34, T37, X54, T12, pM_in_ggaa(T37, T34, X54, T12))
pM_in_ggaa(T37, T34, T104, T12) → U13_ggaa(T37, T34, T104, T12, timesG_in_gga(T37, T34, T104))
U13_ggaa(T37, T34, T104, T12, timesG_out_gga(T37, T34, T104)) → U14_ggaa(T37, T34, T104, T12, timesK_in_gga(T104, T34, T12))
U14_ggaa(T37, T34, T104, T12, timesK_out_gga(T104, T34, T12)) → pM_out_ggaa(T37, T34, T104, T12)
U12_ggaaa(T33, T34, T37, X54, T12, pM_out_ggaa(T37, T34, X54, T12)) → pB_out_ggaaa(T33, T34, T37, X54, T12)
U1_gga(T33, T34, T12, pB_out_ggaaa(T33, T34, X53, X54, T12)) → convertA_out_gga(.(0, .(0, T33)), T34, T12)

The argument filtering Pi contains the following mapping:
convertA_in_gga(x1, x2, x3)  =  convertA_in_gga(x1, x2)
[]  =  []
convertA_out_gga(x1, x2, x3)  =  convertA_out_gga(x1, x2, x3)
.(x1, x2)  =  .(x1, x2)
0  =  0
U1_gga(x1, x2, x3, x4)  =  U1_gga(x1, x2, x4)
pB_in_ggaaa(x1, x2, x3, x4, x5)  =  pB_in_ggaaa(x1, x2)
U11_ggaaa(x1, x2, x3, x4, x5, x6)  =  U11_ggaaa(x1, x2, x6)
convertE_in_gga(x1, x2, x3)  =  convertE_in_gga(x1, x2)
convertE_out_gga(x1, x2, x3)  =  convertE_out_gga(x1, x2, x3)
U5_gga(x1, x2, x3, x4)  =  U5_gga(x1, x2, x4)
pF_in_ggaa(x1, x2, x3, x4)  =  pF_in_ggaa(x1, x2)
U15_ggaa(x1, x2, x3, x4, x5)  =  U15_ggaa(x1, x2, x5)
s(x1)  =  s(x1)
U6_gga(x1, x2, x3, x4, x5)  =  U6_gga(x1, x2, x3, x5)
U2_gga(x1, x2, x3, x4, x5)  =  U2_gga(x1, x2, x3, x5)
pC_in_gggaa(x1, x2, x3, x4, x5)  =  pC_in_gggaa(x1, x2, x3)
U21_gggaa(x1, x2, x3, x4, x5, x6)  =  U21_gggaa(x1, x2, x3, x6)
U3_gga(x1, x2, x3, x4)  =  U3_gga(x1, x2, x4)
pD_in_ggaa(x1, x2, x3, x4)  =  pD_in_ggaa(x1, x2)
U23_ggaa(x1, x2, x3, x4, x5)  =  U23_ggaa(x1, x2, x5)
U24_ggaa(x1, x2, x3, x4, x5)  =  U24_ggaa(x1, x2, x3, x5)
timesK_in_gga(x1, x2, x3)  =  timesK_in_gga(x1, x2)
timesK_out_gga(x1, x2, x3)  =  timesK_out_gga(x1, x2, x3)
U10_gga(x1, x2, x3, x4)  =  U10_gga(x1, x2, x4)
pL_in_ggaa(x1, x2, x3, x4)  =  pL_in_ggaa(x1, x2)
U19_ggaa(x1, x2, x3, x4, x5)  =  U19_ggaa(x1, x2, x5)
timesG_in_gga(x1, x2, x3)  =  timesG_in_gga(x1, x2)
timesG_out_gga(x1, x2, x3)  =  timesG_out_gga(x1, x2, x3)
U7_gga(x1, x2, x3, x4)  =  U7_gga(x1, x2, x4)
pH_in_ggaa(x1, x2, x3, x4)  =  pH_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)
plusI_in_gga(x1, x2, x3)  =  plusI_in_gga(x1, x2)
plusI_out_gga(x1, x2, x3)  =  plusI_out_gga(x1, x2, x3)
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)
U20_ggaa(x1, x2, x3, x4, x5)  =  U20_ggaa(x1, x2, x3, x5)
plusJ_in_gga(x1, x2, x3)  =  plusJ_in_gga(x1, x2)
plusJ_out_gga(x1, x2, x3)  =  plusJ_out_gga(x1, x2, x3)
U9_gga(x1, x2, x3, x4)  =  U9_gga(x1, x2, x4)
pL_out_ggaa(x1, x2, x3, x4)  =  pL_out_ggaa(x1, x2, x3, x4)
pD_out_ggaa(x1, x2, x3, x4)  =  pD_out_ggaa(x1, x2, x3, x4)
U4_gga(x1, x2, x3, x4, x5)  =  U4_gga(x1, x2, x3, x5)
U22_gggaa(x1, x2, x3, x4, x5, x6)  =  U22_gggaa(x1, x2, x3, x4, x6)
pC_out_gggaa(x1, x2, x3, x4, x5)  =  pC_out_gggaa(x1, x2, x3, x4, x5)
U16_ggaa(x1, x2, x3, x4, x5)  =  U16_ggaa(x1, x2, x3, x5)
pF_out_ggaa(x1, x2, x3, x4)  =  pF_out_ggaa(x1, x2, x3, x4)
U12_ggaaa(x1, x2, x3, x4, x5, x6)  =  U12_ggaaa(x1, x2, x3, x6)
pM_in_ggaa(x1, x2, x3, x4)  =  pM_in_ggaa(x1, x2)
U13_ggaa(x1, x2, x3, x4, x5)  =  U13_ggaa(x1, x2, x5)
U14_ggaa(x1, x2, x3, x4, x5)  =  U14_ggaa(x1, x2, x3, x5)
pM_out_ggaa(x1, x2, x3, x4)  =  pM_out_ggaa(x1, x2, x3, x4)
pB_out_ggaaa(x1, x2, x3, x4, x5)  =  pB_out_ggaaa(x1, x2, x3, x4, x5)

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

CONVERTA_IN_GGA(.(0, .(0, T33)), T34, T12) → U1_GGA(T33, T34, T12, pB_in_ggaaa(T33, T34, X53, X54, T12))
CONVERTA_IN_GGA(.(0, .(0, T33)), T34, T12) → PB_IN_GGAAA(T33, T34, X53, X54, T12)
PB_IN_GGAAA(T33, T34, T37, X54, T12) → U11_GGAAA(T33, T34, T37, X54, T12, convertE_in_gga(T33, T34, T37))
PB_IN_GGAAA(T33, T34, T37, X54, T12) → CONVERTE_IN_GGA(T33, T34, T37)
CONVERTE_IN_GGA(.(0, T53), T54, X86) → U5_GGA(T53, T54, X86, pF_in_ggaa(T53, T54, X85, X86))
CONVERTE_IN_GGA(.(0, T53), T54, X86) → PF_IN_GGAA(T53, T54, X85, X86)
PF_IN_GGAA(T53, T54, T57, X86) → U15_GGAA(T53, T54, T57, X86, convertE_in_gga(T53, T54, T57))
PF_IN_GGAA(T53, T54, T57, X86) → CONVERTE_IN_GGA(T53, T54, T57)
CONVERTE_IN_GGA(.(s(T99), T100), T101, s(X151)) → U6_GGA(T99, T100, T101, X151, convertA_in_gga(.(T99, T100), T101, X151))
CONVERTE_IN_GGA(.(s(T99), T100), T101, s(X151)) → CONVERTA_IN_GGA(.(T99, T100), T101, X151)
CONVERTA_IN_GGA(.(0, .(s(T160), T161)), T162, T12) → U2_GGA(T160, T161, T162, T12, pC_in_gggaa(T160, T161, T162, X222, T12))
CONVERTA_IN_GGA(.(0, .(s(T160), T161)), T162, T12) → PC_IN_GGGAA(T160, T161, T162, X222, T12)
PC_IN_GGGAA(T160, T161, T162, T163, T12) → U21_GGGAA(T160, T161, T162, T163, T12, convertA_in_gga(.(T160, T161), T162, T163))
PC_IN_GGGAA(T160, T161, T162, T163, T12) → CONVERTA_IN_GGA(.(T160, T161), T162, T163)
CONVERTA_IN_GGA(.(s(0), T185), T186, s(T188)) → U3_GGA(T185, T186, T188, pD_in_ggaa(T185, T186, X259, T188))
CONVERTA_IN_GGA(.(s(0), T185), T186, s(T188)) → PD_IN_GGAA(T185, T186, X259, T188)
PD_IN_GGAA(T185, T186, T191, T188) → U23_GGAA(T185, T186, T191, T188, convertE_in_gga(T185, T186, T191))
PD_IN_GGAA(T185, T186, T191, T188) → CONVERTE_IN_GGA(T185, T186, T191)
U23_GGAA(T185, T186, T191, T188, convertE_out_gga(T185, T186, T191)) → U24_GGAA(T185, T186, T191, T188, timesK_in_gga(T191, T186, T188))
U23_GGAA(T185, T186, T191, T188, convertE_out_gga(T185, T186, T191)) → TIMESK_IN_GGA(T191, T186, T188)
TIMESK_IN_GGA(s(T120), T121, T123) → U10_GGA(T120, T121, T123, pL_in_ggaa(T120, T121, X175, T123))
TIMESK_IN_GGA(s(T120), T121, T123) → PL_IN_GGAA(T120, T121, X175, T123)
PL_IN_GGAA(T120, T121, T126, T123) → U19_GGAA(T120, T121, T126, T123, timesG_in_gga(T120, T121, T126))
PL_IN_GGAA(T120, T121, T126, T123) → TIMESG_IN_GGA(T120, T121, T126)
TIMESG_IN_GGA(s(T71), T72, X111) → U7_GGA(T71, T72, X111, pH_in_ggaa(T71, T72, X110, X111))
TIMESG_IN_GGA(s(T71), T72, X111) → PH_IN_GGAA(T71, T72, X110, X111)
PH_IN_GGAA(T71, T72, T75, X111) → U17_GGAA(T71, T72, T75, X111, timesG_in_gga(T71, T72, T75))
PH_IN_GGAA(T71, T72, T75, X111) → TIMESG_IN_GGA(T71, T72, T75)
U17_GGAA(T71, T72, T75, X111, timesG_out_gga(T71, T72, T75)) → U18_GGAA(T71, T72, T75, X111, plusI_in_gga(T72, T75, X111))
U17_GGAA(T71, T72, T75, X111, timesG_out_gga(T71, T72, T75)) → PLUSI_IN_GGA(T72, T75, X111)
PLUSI_IN_GGA(s(T89), T90, s(X134)) → U8_GGA(T89, T90, X134, plusI_in_gga(T89, T90, X134))
PLUSI_IN_GGA(s(T89), T90, s(X134)) → PLUSI_IN_GGA(T89, T90, X134)
U19_GGAA(T120, T121, T126, T123, timesG_out_gga(T120, T121, T126)) → U20_GGAA(T120, T121, T126, T123, plusJ_in_gga(T121, T126, T123))
U19_GGAA(T120, T121, T126, T123, timesG_out_gga(T120, T121, T126)) → PLUSJ_IN_GGA(T121, T126, T123)
PLUSJ_IN_GGA(s(T142), T143, s(T145)) → U9_GGA(T142, T143, T145, plusJ_in_gga(T142, T143, T145))
PLUSJ_IN_GGA(s(T142), T143, s(T145)) → PLUSJ_IN_GGA(T142, T143, T145)
CONVERTA_IN_GGA(.(s(s(T204)), T205), T206, s(s(T208))) → U4_GGA(T204, T205, T206, T208, convertA_in_gga(.(T204, T205), T206, T208))
CONVERTA_IN_GGA(.(s(s(T204)), T205), T206, s(s(T208))) → CONVERTA_IN_GGA(.(T204, T205), T206, T208)
U21_GGGAA(T160, T161, T162, T163, T12, convertA_out_gga(.(T160, T161), T162, T163)) → U22_GGGAA(T160, T161, T162, T163, T12, timesK_in_gga(s(T163), T162, T12))
U21_GGGAA(T160, T161, T162, T163, T12, convertA_out_gga(.(T160, T161), T162, T163)) → TIMESK_IN_GGA(s(T163), T162, T12)
U15_GGAA(T53, T54, T57, X86, convertE_out_gga(T53, T54, T57)) → U16_GGAA(T53, T54, T57, X86, timesG_in_gga(T57, T54, X86))
U15_GGAA(T53, T54, T57, X86, convertE_out_gga(T53, T54, T57)) → TIMESG_IN_GGA(T57, T54, X86)
U11_GGAAA(T33, T34, T37, X54, T12, convertE_out_gga(T33, T34, T37)) → U12_GGAAA(T33, T34, T37, X54, T12, pM_in_ggaa(T37, T34, X54, T12))
U11_GGAAA(T33, T34, T37, X54, T12, convertE_out_gga(T33, T34, T37)) → PM_IN_GGAA(T37, T34, X54, T12)
PM_IN_GGAA(T37, T34, T104, T12) → U13_GGAA(T37, T34, T104, T12, timesG_in_gga(T37, T34, T104))
PM_IN_GGAA(T37, T34, T104, T12) → TIMESG_IN_GGA(T37, T34, T104)
U13_GGAA(T37, T34, T104, T12, timesG_out_gga(T37, T34, T104)) → U14_GGAA(T37, T34, T104, T12, timesK_in_gga(T104, T34, T12))
U13_GGAA(T37, T34, T104, T12, timesG_out_gga(T37, T34, T104)) → TIMESK_IN_GGA(T104, T34, T12)

The TRS R consists of the following rules:

convertA_in_gga([], T5, 0) → convertA_out_gga([], T5, 0)
convertA_in_gga(.(0, []), T24, 0) → convertA_out_gga(.(0, []), T24, 0)
convertA_in_gga(.(0, .(0, T33)), T34, T12) → U1_gga(T33, T34, T12, pB_in_ggaaa(T33, T34, X53, X54, T12))
pB_in_ggaaa(T33, T34, T37, X54, T12) → U11_ggaaa(T33, T34, T37, X54, T12, convertE_in_gga(T33, T34, T37))
convertE_in_gga([], T44, 0) → convertE_out_gga([], T44, 0)
convertE_in_gga(.(0, T53), T54, X86) → U5_gga(T53, T54, X86, pF_in_ggaa(T53, T54, X85, X86))
pF_in_ggaa(T53, T54, T57, X86) → U15_ggaa(T53, T54, T57, X86, convertE_in_gga(T53, T54, T57))
convertE_in_gga(.(s(T99), T100), T101, s(X151)) → U6_gga(T99, T100, T101, X151, convertA_in_gga(.(T99, T100), T101, X151))
convertA_in_gga(.(0, .(s(T160), T161)), T162, T12) → U2_gga(T160, T161, T162, T12, pC_in_gggaa(T160, T161, T162, X222, T12))
pC_in_gggaa(T160, T161, T162, T163, T12) → U21_gggaa(T160, T161, T162, T163, T12, convertA_in_gga(.(T160, T161), T162, T163))
convertA_in_gga(.(s(0), T185), T186, s(T188)) → U3_gga(T185, T186, T188, pD_in_ggaa(T185, T186, X259, T188))
pD_in_ggaa(T185, T186, T191, T188) → U23_ggaa(T185, T186, T191, T188, convertE_in_gga(T185, T186, T191))
U23_ggaa(T185, T186, T191, T188, convertE_out_gga(T185, T186, T191)) → U24_ggaa(T185, T186, T191, T188, timesK_in_gga(T191, T186, T188))
timesK_in_gga(0, T113, 0) → timesK_out_gga(0, T113, 0)
timesK_in_gga(s(T120), T121, T123) → U10_gga(T120, T121, T123, pL_in_ggaa(T120, T121, X175, T123))
pL_in_ggaa(T120, T121, T126, T123) → U19_ggaa(T120, T121, T126, T123, timesG_in_gga(T120, T121, T126))
timesG_in_gga(0, T66, 0) → timesG_out_gga(0, T66, 0)
timesG_in_gga(s(T71), T72, X111) → U7_gga(T71, T72, X111, pH_in_ggaa(T71, T72, X110, X111))
pH_in_ggaa(T71, T72, T75, X111) → U17_ggaa(T71, T72, T75, X111, timesG_in_gga(T71, T72, T75))
U17_ggaa(T71, T72, T75, X111, timesG_out_gga(T71, T72, T75)) → U18_ggaa(T71, T72, T75, X111, plusI_in_gga(T72, T75, X111))
plusI_in_gga(0, T84, T84) → plusI_out_gga(0, T84, T84)
plusI_in_gga(s(T89), T90, s(X134)) → U8_gga(T89, T90, X134, plusI_in_gga(T89, T90, X134))
U8_gga(T89, T90, X134, plusI_out_gga(T89, T90, X134)) → plusI_out_gga(s(T89), T90, s(X134))
U18_ggaa(T71, T72, T75, X111, plusI_out_gga(T72, T75, X111)) → pH_out_ggaa(T71, T72, T75, X111)
U7_gga(T71, T72, X111, pH_out_ggaa(T71, T72, X110, X111)) → timesG_out_gga(s(T71), T72, X111)
U19_ggaa(T120, T121, T126, T123, timesG_out_gga(T120, T121, T126)) → U20_ggaa(T120, T121, T126, T123, plusJ_in_gga(T121, T126, T123))
plusJ_in_gga(0, T135, T135) → plusJ_out_gga(0, T135, T135)
plusJ_in_gga(s(T142), T143, s(T145)) → U9_gga(T142, T143, T145, plusJ_in_gga(T142, T143, T145))
U9_gga(T142, T143, T145, plusJ_out_gga(T142, T143, T145)) → plusJ_out_gga(s(T142), T143, s(T145))
U20_ggaa(T120, T121, T126, T123, plusJ_out_gga(T121, T126, T123)) → pL_out_ggaa(T120, T121, T126, T123)
U10_gga(T120, T121, T123, pL_out_ggaa(T120, T121, X175, T123)) → timesK_out_gga(s(T120), T121, T123)
U24_ggaa(T185, T186, T191, T188, timesK_out_gga(T191, T186, T188)) → pD_out_ggaa(T185, T186, T191, T188)
U3_gga(T185, T186, T188, pD_out_ggaa(T185, T186, X259, T188)) → convertA_out_gga(.(s(0), T185), T186, s(T188))
convertA_in_gga(.(s(s(T204)), T205), T206, s(s(T208))) → U4_gga(T204, T205, T206, T208, convertA_in_gga(.(T204, T205), T206, T208))
U4_gga(T204, T205, T206, T208, convertA_out_gga(.(T204, T205), T206, T208)) → convertA_out_gga(.(s(s(T204)), T205), T206, s(s(T208)))
U21_gggaa(T160, T161, T162, T163, T12, convertA_out_gga(.(T160, T161), T162, T163)) → U22_gggaa(T160, T161, T162, T163, T12, timesK_in_gga(s(T163), T162, T12))
U22_gggaa(T160, T161, T162, T163, T12, timesK_out_gga(s(T163), T162, T12)) → pC_out_gggaa(T160, T161, T162, T163, T12)
U2_gga(T160, T161, T162, T12, pC_out_gggaa(T160, T161, T162, X222, T12)) → convertA_out_gga(.(0, .(s(T160), T161)), T162, T12)
U6_gga(T99, T100, T101, X151, convertA_out_gga(.(T99, T100), T101, X151)) → convertE_out_gga(.(s(T99), T100), T101, s(X151))
U15_ggaa(T53, T54, T57, X86, convertE_out_gga(T53, T54, T57)) → U16_ggaa(T53, T54, T57, X86, timesG_in_gga(T57, T54, X86))
U16_ggaa(T53, T54, T57, X86, timesG_out_gga(T57, T54, X86)) → pF_out_ggaa(T53, T54, T57, X86)
U5_gga(T53, T54, X86, pF_out_ggaa(T53, T54, X85, X86)) → convertE_out_gga(.(0, T53), T54, X86)
U11_ggaaa(T33, T34, T37, X54, T12, convertE_out_gga(T33, T34, T37)) → U12_ggaaa(T33, T34, T37, X54, T12, pM_in_ggaa(T37, T34, X54, T12))
pM_in_ggaa(T37, T34, T104, T12) → U13_ggaa(T37, T34, T104, T12, timesG_in_gga(T37, T34, T104))
U13_ggaa(T37, T34, T104, T12, timesG_out_gga(T37, T34, T104)) → U14_ggaa(T37, T34, T104, T12, timesK_in_gga(T104, T34, T12))
U14_ggaa(T37, T34, T104, T12, timesK_out_gga(T104, T34, T12)) → pM_out_ggaa(T37, T34, T104, T12)
U12_ggaaa(T33, T34, T37, X54, T12, pM_out_ggaa(T37, T34, X54, T12)) → pB_out_ggaaa(T33, T34, T37, X54, T12)
U1_gga(T33, T34, T12, pB_out_ggaaa(T33, T34, X53, X54, T12)) → convertA_out_gga(.(0, .(0, T33)), T34, T12)

The argument filtering Pi contains the following mapping:
convertA_in_gga(x1, x2, x3)  =  convertA_in_gga(x1, x2)
[]  =  []
convertA_out_gga(x1, x2, x3)  =  convertA_out_gga(x1, x2, x3)
.(x1, x2)  =  .(x1, x2)
0  =  0
U1_gga(x1, x2, x3, x4)  =  U1_gga(x1, x2, x4)
pB_in_ggaaa(x1, x2, x3, x4, x5)  =  pB_in_ggaaa(x1, x2)
U11_ggaaa(x1, x2, x3, x4, x5, x6)  =  U11_ggaaa(x1, x2, x6)
convertE_in_gga(x1, x2, x3)  =  convertE_in_gga(x1, x2)
convertE_out_gga(x1, x2, x3)  =  convertE_out_gga(x1, x2, x3)
U5_gga(x1, x2, x3, x4)  =  U5_gga(x1, x2, x4)
pF_in_ggaa(x1, x2, x3, x4)  =  pF_in_ggaa(x1, x2)
U15_ggaa(x1, x2, x3, x4, x5)  =  U15_ggaa(x1, x2, x5)
s(x1)  =  s(x1)
U6_gga(x1, x2, x3, x4, x5)  =  U6_gga(x1, x2, x3, x5)
U2_gga(x1, x2, x3, x4, x5)  =  U2_gga(x1, x2, x3, x5)
pC_in_gggaa(x1, x2, x3, x4, x5)  =  pC_in_gggaa(x1, x2, x3)
U21_gggaa(x1, x2, x3, x4, x5, x6)  =  U21_gggaa(x1, x2, x3, x6)
U3_gga(x1, x2, x3, x4)  =  U3_gga(x1, x2, x4)
pD_in_ggaa(x1, x2, x3, x4)  =  pD_in_ggaa(x1, x2)
U23_ggaa(x1, x2, x3, x4, x5)  =  U23_ggaa(x1, x2, x5)
U24_ggaa(x1, x2, x3, x4, x5)  =  U24_ggaa(x1, x2, x3, x5)
timesK_in_gga(x1, x2, x3)  =  timesK_in_gga(x1, x2)
timesK_out_gga(x1, x2, x3)  =  timesK_out_gga(x1, x2, x3)
U10_gga(x1, x2, x3, x4)  =  U10_gga(x1, x2, x4)
pL_in_ggaa(x1, x2, x3, x4)  =  pL_in_ggaa(x1, x2)
U19_ggaa(x1, x2, x3, x4, x5)  =  U19_ggaa(x1, x2, x5)
timesG_in_gga(x1, x2, x3)  =  timesG_in_gga(x1, x2)
timesG_out_gga(x1, x2, x3)  =  timesG_out_gga(x1, x2, x3)
U7_gga(x1, x2, x3, x4)  =  U7_gga(x1, x2, x4)
pH_in_ggaa(x1, x2, x3, x4)  =  pH_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)
plusI_in_gga(x1, x2, x3)  =  plusI_in_gga(x1, x2)
plusI_out_gga(x1, x2, x3)  =  plusI_out_gga(x1, x2, x3)
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)
U20_ggaa(x1, x2, x3, x4, x5)  =  U20_ggaa(x1, x2, x3, x5)
plusJ_in_gga(x1, x2, x3)  =  plusJ_in_gga(x1, x2)
plusJ_out_gga(x1, x2, x3)  =  plusJ_out_gga(x1, x2, x3)
U9_gga(x1, x2, x3, x4)  =  U9_gga(x1, x2, x4)
pL_out_ggaa(x1, x2, x3, x4)  =  pL_out_ggaa(x1, x2, x3, x4)
pD_out_ggaa(x1, x2, x3, x4)  =  pD_out_ggaa(x1, x2, x3, x4)
U4_gga(x1, x2, x3, x4, x5)  =  U4_gga(x1, x2, x3, x5)
U22_gggaa(x1, x2, x3, x4, x5, x6)  =  U22_gggaa(x1, x2, x3, x4, x6)
pC_out_gggaa(x1, x2, x3, x4, x5)  =  pC_out_gggaa(x1, x2, x3, x4, x5)
U16_ggaa(x1, x2, x3, x4, x5)  =  U16_ggaa(x1, x2, x3, x5)
pF_out_ggaa(x1, x2, x3, x4)  =  pF_out_ggaa(x1, x2, x3, x4)
U12_ggaaa(x1, x2, x3, x4, x5, x6)  =  U12_ggaaa(x1, x2, x3, x6)
pM_in_ggaa(x1, x2, x3, x4)  =  pM_in_ggaa(x1, x2)
U13_ggaa(x1, x2, x3, x4, x5)  =  U13_ggaa(x1, x2, x5)
U14_ggaa(x1, x2, x3, x4, x5)  =  U14_ggaa(x1, x2, x3, x5)
pM_out_ggaa(x1, x2, x3, x4)  =  pM_out_ggaa(x1, x2, x3, x4)
pB_out_ggaaa(x1, x2, x3, x4, x5)  =  pB_out_ggaaa(x1, x2, x3, x4, x5)
CONVERTA_IN_GGA(x1, x2, x3)  =  CONVERTA_IN_GGA(x1, x2)
U1_GGA(x1, x2, x3, x4)  =  U1_GGA(x1, x2, x4)
PB_IN_GGAAA(x1, x2, x3, x4, x5)  =  PB_IN_GGAAA(x1, x2)
U11_GGAAA(x1, x2, x3, x4, x5, x6)  =  U11_GGAAA(x1, x2, x6)
CONVERTE_IN_GGA(x1, x2, x3)  =  CONVERTE_IN_GGA(x1, x2)
U5_GGA(x1, x2, x3, x4)  =  U5_GGA(x1, x2, x4)
PF_IN_GGAA(x1, x2, x3, x4)  =  PF_IN_GGAA(x1, x2)
U15_GGAA(x1, x2, x3, x4, x5)  =  U15_GGAA(x1, x2, x5)
U6_GGA(x1, x2, x3, x4, x5)  =  U6_GGA(x1, x2, x3, x5)
U2_GGA(x1, x2, x3, x4, x5)  =  U2_GGA(x1, x2, x3, x5)
PC_IN_GGGAA(x1, x2, x3, x4, x5)  =  PC_IN_GGGAA(x1, x2, x3)
U21_GGGAA(x1, x2, x3, x4, x5, x6)  =  U21_GGGAA(x1, x2, x3, x6)
U3_GGA(x1, x2, x3, x4)  =  U3_GGA(x1, x2, x4)
PD_IN_GGAA(x1, x2, x3, x4)  =  PD_IN_GGAA(x1, x2)
U23_GGAA(x1, x2, x3, x4, x5)  =  U23_GGAA(x1, x2, x5)
U24_GGAA(x1, x2, x3, x4, x5)  =  U24_GGAA(x1, x2, x3, x5)
TIMESK_IN_GGA(x1, x2, x3)  =  TIMESK_IN_GGA(x1, x2)
U10_GGA(x1, x2, x3, x4)  =  U10_GGA(x1, x2, x4)
PL_IN_GGAA(x1, x2, x3, x4)  =  PL_IN_GGAA(x1, x2)
U19_GGAA(x1, x2, x3, x4, x5)  =  U19_GGAA(x1, x2, x5)
TIMESG_IN_GGA(x1, x2, x3)  =  TIMESG_IN_GGA(x1, x2)
U7_GGA(x1, x2, x3, x4)  =  U7_GGA(x1, x2, x4)
PH_IN_GGAA(x1, x2, x3, x4)  =  PH_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)
PLUSI_IN_GGA(x1, x2, x3)  =  PLUSI_IN_GGA(x1, x2)
U8_GGA(x1, x2, x3, x4)  =  U8_GGA(x1, x2, x4)
U20_GGAA(x1, x2, x3, x4, x5)  =  U20_GGAA(x1, x2, x3, x5)
PLUSJ_IN_GGA(x1, x2, x3)  =  PLUSJ_IN_GGA(x1, x2)
U9_GGA(x1, x2, x3, x4)  =  U9_GGA(x1, x2, x4)
U4_GGA(x1, x2, x3, x4, x5)  =  U4_GGA(x1, x2, x3, x5)
U22_GGGAA(x1, x2, x3, x4, x5, x6)  =  U22_GGGAA(x1, x2, x3, x4, x6)
U16_GGAA(x1, x2, x3, x4, x5)  =  U16_GGAA(x1, x2, x3, x5)
U12_GGAAA(x1, x2, x3, x4, x5, x6)  =  U12_GGAAA(x1, x2, x3, x6)
PM_IN_GGAA(x1, x2, x3, x4)  =  PM_IN_GGAA(x1, x2)
U13_GGAA(x1, x2, x3, x4, x5)  =  U13_GGAA(x1, x2, x5)
U14_GGAA(x1, x2, x3, x4, x5)  =  U14_GGAA(x1, x2, x3, x5)

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

(4) Obligation:

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

CONVERTA_IN_GGA(.(0, .(0, T33)), T34, T12) → U1_GGA(T33, T34, T12, pB_in_ggaaa(T33, T34, X53, X54, T12))
CONVERTA_IN_GGA(.(0, .(0, T33)), T34, T12) → PB_IN_GGAAA(T33, T34, X53, X54, T12)
PB_IN_GGAAA(T33, T34, T37, X54, T12) → U11_GGAAA(T33, T34, T37, X54, T12, convertE_in_gga(T33, T34, T37))
PB_IN_GGAAA(T33, T34, T37, X54, T12) → CONVERTE_IN_GGA(T33, T34, T37)
CONVERTE_IN_GGA(.(0, T53), T54, X86) → U5_GGA(T53, T54, X86, pF_in_ggaa(T53, T54, X85, X86))
CONVERTE_IN_GGA(.(0, T53), T54, X86) → PF_IN_GGAA(T53, T54, X85, X86)
PF_IN_GGAA(T53, T54, T57, X86) → U15_GGAA(T53, T54, T57, X86, convertE_in_gga(T53, T54, T57))
PF_IN_GGAA(T53, T54, T57, X86) → CONVERTE_IN_GGA(T53, T54, T57)
CONVERTE_IN_GGA(.(s(T99), T100), T101, s(X151)) → U6_GGA(T99, T100, T101, X151, convertA_in_gga(.(T99, T100), T101, X151))
CONVERTE_IN_GGA(.(s(T99), T100), T101, s(X151)) → CONVERTA_IN_GGA(.(T99, T100), T101, X151)
CONVERTA_IN_GGA(.(0, .(s(T160), T161)), T162, T12) → U2_GGA(T160, T161, T162, T12, pC_in_gggaa(T160, T161, T162, X222, T12))
CONVERTA_IN_GGA(.(0, .(s(T160), T161)), T162, T12) → PC_IN_GGGAA(T160, T161, T162, X222, T12)
PC_IN_GGGAA(T160, T161, T162, T163, T12) → U21_GGGAA(T160, T161, T162, T163, T12, convertA_in_gga(.(T160, T161), T162, T163))
PC_IN_GGGAA(T160, T161, T162, T163, T12) → CONVERTA_IN_GGA(.(T160, T161), T162, T163)
CONVERTA_IN_GGA(.(s(0), T185), T186, s(T188)) → U3_GGA(T185, T186, T188, pD_in_ggaa(T185, T186, X259, T188))
CONVERTA_IN_GGA(.(s(0), T185), T186, s(T188)) → PD_IN_GGAA(T185, T186, X259, T188)
PD_IN_GGAA(T185, T186, T191, T188) → U23_GGAA(T185, T186, T191, T188, convertE_in_gga(T185, T186, T191))
PD_IN_GGAA(T185, T186, T191, T188) → CONVERTE_IN_GGA(T185, T186, T191)
U23_GGAA(T185, T186, T191, T188, convertE_out_gga(T185, T186, T191)) → U24_GGAA(T185, T186, T191, T188, timesK_in_gga(T191, T186, T188))
U23_GGAA(T185, T186, T191, T188, convertE_out_gga(T185, T186, T191)) → TIMESK_IN_GGA(T191, T186, T188)
TIMESK_IN_GGA(s(T120), T121, T123) → U10_GGA(T120, T121, T123, pL_in_ggaa(T120, T121, X175, T123))
TIMESK_IN_GGA(s(T120), T121, T123) → PL_IN_GGAA(T120, T121, X175, T123)
PL_IN_GGAA(T120, T121, T126, T123) → U19_GGAA(T120, T121, T126, T123, timesG_in_gga(T120, T121, T126))
PL_IN_GGAA(T120, T121, T126, T123) → TIMESG_IN_GGA(T120, T121, T126)
TIMESG_IN_GGA(s(T71), T72, X111) → U7_GGA(T71, T72, X111, pH_in_ggaa(T71, T72, X110, X111))
TIMESG_IN_GGA(s(T71), T72, X111) → PH_IN_GGAA(T71, T72, X110, X111)
PH_IN_GGAA(T71, T72, T75, X111) → U17_GGAA(T71, T72, T75, X111, timesG_in_gga(T71, T72, T75))
PH_IN_GGAA(T71, T72, T75, X111) → TIMESG_IN_GGA(T71, T72, T75)
U17_GGAA(T71, T72, T75, X111, timesG_out_gga(T71, T72, T75)) → U18_GGAA(T71, T72, T75, X111, plusI_in_gga(T72, T75, X111))
U17_GGAA(T71, T72, T75, X111, timesG_out_gga(T71, T72, T75)) → PLUSI_IN_GGA(T72, T75, X111)
PLUSI_IN_GGA(s(T89), T90, s(X134)) → U8_GGA(T89, T90, X134, plusI_in_gga(T89, T90, X134))
PLUSI_IN_GGA(s(T89), T90, s(X134)) → PLUSI_IN_GGA(T89, T90, X134)
U19_GGAA(T120, T121, T126, T123, timesG_out_gga(T120, T121, T126)) → U20_GGAA(T120, T121, T126, T123, plusJ_in_gga(T121, T126, T123))
U19_GGAA(T120, T121, T126, T123, timesG_out_gga(T120, T121, T126)) → PLUSJ_IN_GGA(T121, T126, T123)
PLUSJ_IN_GGA(s(T142), T143, s(T145)) → U9_GGA(T142, T143, T145, plusJ_in_gga(T142, T143, T145))
PLUSJ_IN_GGA(s(T142), T143, s(T145)) → PLUSJ_IN_GGA(T142, T143, T145)
CONVERTA_IN_GGA(.(s(s(T204)), T205), T206, s(s(T208))) → U4_GGA(T204, T205, T206, T208, convertA_in_gga(.(T204, T205), T206, T208))
CONVERTA_IN_GGA(.(s(s(T204)), T205), T206, s(s(T208))) → CONVERTA_IN_GGA(.(T204, T205), T206, T208)
U21_GGGAA(T160, T161, T162, T163, T12, convertA_out_gga(.(T160, T161), T162, T163)) → U22_GGGAA(T160, T161, T162, T163, T12, timesK_in_gga(s(T163), T162, T12))
U21_GGGAA(T160, T161, T162, T163, T12, convertA_out_gga(.(T160, T161), T162, T163)) → TIMESK_IN_GGA(s(T163), T162, T12)
U15_GGAA(T53, T54, T57, X86, convertE_out_gga(T53, T54, T57)) → U16_GGAA(T53, T54, T57, X86, timesG_in_gga(T57, T54, X86))
U15_GGAA(T53, T54, T57, X86, convertE_out_gga(T53, T54, T57)) → TIMESG_IN_GGA(T57, T54, X86)
U11_GGAAA(T33, T34, T37, X54, T12, convertE_out_gga(T33, T34, T37)) → U12_GGAAA(T33, T34, T37, X54, T12, pM_in_ggaa(T37, T34, X54, T12))
U11_GGAAA(T33, T34, T37, X54, T12, convertE_out_gga(T33, T34, T37)) → PM_IN_GGAA(T37, T34, X54, T12)
PM_IN_GGAA(T37, T34, T104, T12) → U13_GGAA(T37, T34, T104, T12, timesG_in_gga(T37, T34, T104))
PM_IN_GGAA(T37, T34, T104, T12) → TIMESG_IN_GGA(T37, T34, T104)
U13_GGAA(T37, T34, T104, T12, timesG_out_gga(T37, T34, T104)) → U14_GGAA(T37, T34, T104, T12, timesK_in_gga(T104, T34, T12))
U13_GGAA(T37, T34, T104, T12, timesG_out_gga(T37, T34, T104)) → TIMESK_IN_GGA(T104, T34, T12)

The TRS R consists of the following rules:

convertA_in_gga([], T5, 0) → convertA_out_gga([], T5, 0)
convertA_in_gga(.(0, []), T24, 0) → convertA_out_gga(.(0, []), T24, 0)
convertA_in_gga(.(0, .(0, T33)), T34, T12) → U1_gga(T33, T34, T12, pB_in_ggaaa(T33, T34, X53, X54, T12))
pB_in_ggaaa(T33, T34, T37, X54, T12) → U11_ggaaa(T33, T34, T37, X54, T12, convertE_in_gga(T33, T34, T37))
convertE_in_gga([], T44, 0) → convertE_out_gga([], T44, 0)
convertE_in_gga(.(0, T53), T54, X86) → U5_gga(T53, T54, X86, pF_in_ggaa(T53, T54, X85, X86))
pF_in_ggaa(T53, T54, T57, X86) → U15_ggaa(T53, T54, T57, X86, convertE_in_gga(T53, T54, T57))
convertE_in_gga(.(s(T99), T100), T101, s(X151)) → U6_gga(T99, T100, T101, X151, convertA_in_gga(.(T99, T100), T101, X151))
convertA_in_gga(.(0, .(s(T160), T161)), T162, T12) → U2_gga(T160, T161, T162, T12, pC_in_gggaa(T160, T161, T162, X222, T12))
pC_in_gggaa(T160, T161, T162, T163, T12) → U21_gggaa(T160, T161, T162, T163, T12, convertA_in_gga(.(T160, T161), T162, T163))
convertA_in_gga(.(s(0), T185), T186, s(T188)) → U3_gga(T185, T186, T188, pD_in_ggaa(T185, T186, X259, T188))
pD_in_ggaa(T185, T186, T191, T188) → U23_ggaa(T185, T186, T191, T188, convertE_in_gga(T185, T186, T191))
U23_ggaa(T185, T186, T191, T188, convertE_out_gga(T185, T186, T191)) → U24_ggaa(T185, T186, T191, T188, timesK_in_gga(T191, T186, T188))
timesK_in_gga(0, T113, 0) → timesK_out_gga(0, T113, 0)
timesK_in_gga(s(T120), T121, T123) → U10_gga(T120, T121, T123, pL_in_ggaa(T120, T121, X175, T123))
pL_in_ggaa(T120, T121, T126, T123) → U19_ggaa(T120, T121, T126, T123, timesG_in_gga(T120, T121, T126))
timesG_in_gga(0, T66, 0) → timesG_out_gga(0, T66, 0)
timesG_in_gga(s(T71), T72, X111) → U7_gga(T71, T72, X111, pH_in_ggaa(T71, T72, X110, X111))
pH_in_ggaa(T71, T72, T75, X111) → U17_ggaa(T71, T72, T75, X111, timesG_in_gga(T71, T72, T75))
U17_ggaa(T71, T72, T75, X111, timesG_out_gga(T71, T72, T75)) → U18_ggaa(T71, T72, T75, X111, plusI_in_gga(T72, T75, X111))
plusI_in_gga(0, T84, T84) → plusI_out_gga(0, T84, T84)
plusI_in_gga(s(T89), T90, s(X134)) → U8_gga(T89, T90, X134, plusI_in_gga(T89, T90, X134))
U8_gga(T89, T90, X134, plusI_out_gga(T89, T90, X134)) → plusI_out_gga(s(T89), T90, s(X134))
U18_ggaa(T71, T72, T75, X111, plusI_out_gga(T72, T75, X111)) → pH_out_ggaa(T71, T72, T75, X111)
U7_gga(T71, T72, X111, pH_out_ggaa(T71, T72, X110, X111)) → timesG_out_gga(s(T71), T72, X111)
U19_ggaa(T120, T121, T126, T123, timesG_out_gga(T120, T121, T126)) → U20_ggaa(T120, T121, T126, T123, plusJ_in_gga(T121, T126, T123))
plusJ_in_gga(0, T135, T135) → plusJ_out_gga(0, T135, T135)
plusJ_in_gga(s(T142), T143, s(T145)) → U9_gga(T142, T143, T145, plusJ_in_gga(T142, T143, T145))
U9_gga(T142, T143, T145, plusJ_out_gga(T142, T143, T145)) → plusJ_out_gga(s(T142), T143, s(T145))
U20_ggaa(T120, T121, T126, T123, plusJ_out_gga(T121, T126, T123)) → pL_out_ggaa(T120, T121, T126, T123)
U10_gga(T120, T121, T123, pL_out_ggaa(T120, T121, X175, T123)) → timesK_out_gga(s(T120), T121, T123)
U24_ggaa(T185, T186, T191, T188, timesK_out_gga(T191, T186, T188)) → pD_out_ggaa(T185, T186, T191, T188)
U3_gga(T185, T186, T188, pD_out_ggaa(T185, T186, X259, T188)) → convertA_out_gga(.(s(0), T185), T186, s(T188))
convertA_in_gga(.(s(s(T204)), T205), T206, s(s(T208))) → U4_gga(T204, T205, T206, T208, convertA_in_gga(.(T204, T205), T206, T208))
U4_gga(T204, T205, T206, T208, convertA_out_gga(.(T204, T205), T206, T208)) → convertA_out_gga(.(s(s(T204)), T205), T206, s(s(T208)))
U21_gggaa(T160, T161, T162, T163, T12, convertA_out_gga(.(T160, T161), T162, T163)) → U22_gggaa(T160, T161, T162, T163, T12, timesK_in_gga(s(T163), T162, T12))
U22_gggaa(T160, T161, T162, T163, T12, timesK_out_gga(s(T163), T162, T12)) → pC_out_gggaa(T160, T161, T162, T163, T12)
U2_gga(T160, T161, T162, T12, pC_out_gggaa(T160, T161, T162, X222, T12)) → convertA_out_gga(.(0, .(s(T160), T161)), T162, T12)
U6_gga(T99, T100, T101, X151, convertA_out_gga(.(T99, T100), T101, X151)) → convertE_out_gga(.(s(T99), T100), T101, s(X151))
U15_ggaa(T53, T54, T57, X86, convertE_out_gga(T53, T54, T57)) → U16_ggaa(T53, T54, T57, X86, timesG_in_gga(T57, T54, X86))
U16_ggaa(T53, T54, T57, X86, timesG_out_gga(T57, T54, X86)) → pF_out_ggaa(T53, T54, T57, X86)
U5_gga(T53, T54, X86, pF_out_ggaa(T53, T54, X85, X86)) → convertE_out_gga(.(0, T53), T54, X86)
U11_ggaaa(T33, T34, T37, X54, T12, convertE_out_gga(T33, T34, T37)) → U12_ggaaa(T33, T34, T37, X54, T12, pM_in_ggaa(T37, T34, X54, T12))
pM_in_ggaa(T37, T34, T104, T12) → U13_ggaa(T37, T34, T104, T12, timesG_in_gga(T37, T34, T104))
U13_ggaa(T37, T34, T104, T12, timesG_out_gga(T37, T34, T104)) → U14_ggaa(T37, T34, T104, T12, timesK_in_gga(T104, T34, T12))
U14_ggaa(T37, T34, T104, T12, timesK_out_gga(T104, T34, T12)) → pM_out_ggaa(T37, T34, T104, T12)
U12_ggaaa(T33, T34, T37, X54, T12, pM_out_ggaa(T37, T34, X54, T12)) → pB_out_ggaaa(T33, T34, T37, X54, T12)
U1_gga(T33, T34, T12, pB_out_ggaaa(T33, T34, X53, X54, T12)) → convertA_out_gga(.(0, .(0, T33)), T34, T12)

The argument filtering Pi contains the following mapping:
convertA_in_gga(x1, x2, x3)  =  convertA_in_gga(x1, x2)
[]  =  []
convertA_out_gga(x1, x2, x3)  =  convertA_out_gga(x1, x2, x3)
.(x1, x2)  =  .(x1, x2)
0  =  0
U1_gga(x1, x2, x3, x4)  =  U1_gga(x1, x2, x4)
pB_in_ggaaa(x1, x2, x3, x4, x5)  =  pB_in_ggaaa(x1, x2)
U11_ggaaa(x1, x2, x3, x4, x5, x6)  =  U11_ggaaa(x1, x2, x6)
convertE_in_gga(x1, x2, x3)  =  convertE_in_gga(x1, x2)
convertE_out_gga(x1, x2, x3)  =  convertE_out_gga(x1, x2, x3)
U5_gga(x1, x2, x3, x4)  =  U5_gga(x1, x2, x4)
pF_in_ggaa(x1, x2, x3, x4)  =  pF_in_ggaa(x1, x2)
U15_ggaa(x1, x2, x3, x4, x5)  =  U15_ggaa(x1, x2, x5)
s(x1)  =  s(x1)
U6_gga(x1, x2, x3, x4, x5)  =  U6_gga(x1, x2, x3, x5)
U2_gga(x1, x2, x3, x4, x5)  =  U2_gga(x1, x2, x3, x5)
pC_in_gggaa(x1, x2, x3, x4, x5)  =  pC_in_gggaa(x1, x2, x3)
U21_gggaa(x1, x2, x3, x4, x5, x6)  =  U21_gggaa(x1, x2, x3, x6)
U3_gga(x1, x2, x3, x4)  =  U3_gga(x1, x2, x4)
pD_in_ggaa(x1, x2, x3, x4)  =  pD_in_ggaa(x1, x2)
U23_ggaa(x1, x2, x3, x4, x5)  =  U23_ggaa(x1, x2, x5)
U24_ggaa(x1, x2, x3, x4, x5)  =  U24_ggaa(x1, x2, x3, x5)
timesK_in_gga(x1, x2, x3)  =  timesK_in_gga(x1, x2)
timesK_out_gga(x1, x2, x3)  =  timesK_out_gga(x1, x2, x3)
U10_gga(x1, x2, x3, x4)  =  U10_gga(x1, x2, x4)
pL_in_ggaa(x1, x2, x3, x4)  =  pL_in_ggaa(x1, x2)
U19_ggaa(x1, x2, x3, x4, x5)  =  U19_ggaa(x1, x2, x5)
timesG_in_gga(x1, x2, x3)  =  timesG_in_gga(x1, x2)
timesG_out_gga(x1, x2, x3)  =  timesG_out_gga(x1, x2, x3)
U7_gga(x1, x2, x3, x4)  =  U7_gga(x1, x2, x4)
pH_in_ggaa(x1, x2, x3, x4)  =  pH_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)
plusI_in_gga(x1, x2, x3)  =  plusI_in_gga(x1, x2)
plusI_out_gga(x1, x2, x3)  =  plusI_out_gga(x1, x2, x3)
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)
U20_ggaa(x1, x2, x3, x4, x5)  =  U20_ggaa(x1, x2, x3, x5)
plusJ_in_gga(x1, x2, x3)  =  plusJ_in_gga(x1, x2)
plusJ_out_gga(x1, x2, x3)  =  plusJ_out_gga(x1, x2, x3)
U9_gga(x1, x2, x3, x4)  =  U9_gga(x1, x2, x4)
pL_out_ggaa(x1, x2, x3, x4)  =  pL_out_ggaa(x1, x2, x3, x4)
pD_out_ggaa(x1, x2, x3, x4)  =  pD_out_ggaa(x1, x2, x3, x4)
U4_gga(x1, x2, x3, x4, x5)  =  U4_gga(x1, x2, x3, x5)
U22_gggaa(x1, x2, x3, x4, x5, x6)  =  U22_gggaa(x1, x2, x3, x4, x6)
pC_out_gggaa(x1, x2, x3, x4, x5)  =  pC_out_gggaa(x1, x2, x3, x4, x5)
U16_ggaa(x1, x2, x3, x4, x5)  =  U16_ggaa(x1, x2, x3, x5)
pF_out_ggaa(x1, x2, x3, x4)  =  pF_out_ggaa(x1, x2, x3, x4)
U12_ggaaa(x1, x2, x3, x4, x5, x6)  =  U12_ggaaa(x1, x2, x3, x6)
pM_in_ggaa(x1, x2, x3, x4)  =  pM_in_ggaa(x1, x2)
U13_ggaa(x1, x2, x3, x4, x5)  =  U13_ggaa(x1, x2, x5)
U14_ggaa(x1, x2, x3, x4, x5)  =  U14_ggaa(x1, x2, x3, x5)
pM_out_ggaa(x1, x2, x3, x4)  =  pM_out_ggaa(x1, x2, x3, x4)
pB_out_ggaaa(x1, x2, x3, x4, x5)  =  pB_out_ggaaa(x1, x2, x3, x4, x5)
CONVERTA_IN_GGA(x1, x2, x3)  =  CONVERTA_IN_GGA(x1, x2)
U1_GGA(x1, x2, x3, x4)  =  U1_GGA(x1, x2, x4)
PB_IN_GGAAA(x1, x2, x3, x4, x5)  =  PB_IN_GGAAA(x1, x2)
U11_GGAAA(x1, x2, x3, x4, x5, x6)  =  U11_GGAAA(x1, x2, x6)
CONVERTE_IN_GGA(x1, x2, x3)  =  CONVERTE_IN_GGA(x1, x2)
U5_GGA(x1, x2, x3, x4)  =  U5_GGA(x1, x2, x4)
PF_IN_GGAA(x1, x2, x3, x4)  =  PF_IN_GGAA(x1, x2)
U15_GGAA(x1, x2, x3, x4, x5)  =  U15_GGAA(x1, x2, x5)
U6_GGA(x1, x2, x3, x4, x5)  =  U6_GGA(x1, x2, x3, x5)
U2_GGA(x1, x2, x3, x4, x5)  =  U2_GGA(x1, x2, x3, x5)
PC_IN_GGGAA(x1, x2, x3, x4, x5)  =  PC_IN_GGGAA(x1, x2, x3)
U21_GGGAA(x1, x2, x3, x4, x5, x6)  =  U21_GGGAA(x1, x2, x3, x6)
U3_GGA(x1, x2, x3, x4)  =  U3_GGA(x1, x2, x4)
PD_IN_GGAA(x1, x2, x3, x4)  =  PD_IN_GGAA(x1, x2)
U23_GGAA(x1, x2, x3, x4, x5)  =  U23_GGAA(x1, x2, x5)
U24_GGAA(x1, x2, x3, x4, x5)  =  U24_GGAA(x1, x2, x3, x5)
TIMESK_IN_GGA(x1, x2, x3)  =  TIMESK_IN_GGA(x1, x2)
U10_GGA(x1, x2, x3, x4)  =  U10_GGA(x1, x2, x4)
PL_IN_GGAA(x1, x2, x3, x4)  =  PL_IN_GGAA(x1, x2)
U19_GGAA(x1, x2, x3, x4, x5)  =  U19_GGAA(x1, x2, x5)
TIMESG_IN_GGA(x1, x2, x3)  =  TIMESG_IN_GGA(x1, x2)
U7_GGA(x1, x2, x3, x4)  =  U7_GGA(x1, x2, x4)
PH_IN_GGAA(x1, x2, x3, x4)  =  PH_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)
PLUSI_IN_GGA(x1, x2, x3)  =  PLUSI_IN_GGA(x1, x2)
U8_GGA(x1, x2, x3, x4)  =  U8_GGA(x1, x2, x4)
U20_GGAA(x1, x2, x3, x4, x5)  =  U20_GGAA(x1, x2, x3, x5)
PLUSJ_IN_GGA(x1, x2, x3)  =  PLUSJ_IN_GGA(x1, x2)
U9_GGA(x1, x2, x3, x4)  =  U9_GGA(x1, x2, x4)
U4_GGA(x1, x2, x3, x4, x5)  =  U4_GGA(x1, x2, x3, x5)
U22_GGGAA(x1, x2, x3, x4, x5, x6)  =  U22_GGGAA(x1, x2, x3, x4, x6)
U16_GGAA(x1, x2, x3, x4, x5)  =  U16_GGAA(x1, x2, x3, x5)
U12_GGAAA(x1, x2, x3, x4, x5, x6)  =  U12_GGAAA(x1, x2, x3, x6)
PM_IN_GGAA(x1, x2, x3, x4)  =  PM_IN_GGAA(x1, x2)
U13_GGAA(x1, x2, x3, x4, x5)  =  U13_GGAA(x1, x2, x5)
U14_GGAA(x1, x2, x3, x4, x5)  =  U14_GGAA(x1, x2, x3, x5)

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:

PLUSJ_IN_GGA(s(T142), T143, s(T145)) → PLUSJ_IN_GGA(T142, T143, T145)

The TRS R consists of the following rules:

convertA_in_gga([], T5, 0) → convertA_out_gga([], T5, 0)
convertA_in_gga(.(0, []), T24, 0) → convertA_out_gga(.(0, []), T24, 0)
convertA_in_gga(.(0, .(0, T33)), T34, T12) → U1_gga(T33, T34, T12, pB_in_ggaaa(T33, T34, X53, X54, T12))
pB_in_ggaaa(T33, T34, T37, X54, T12) → U11_ggaaa(T33, T34, T37, X54, T12, convertE_in_gga(T33, T34, T37))
convertE_in_gga([], T44, 0) → convertE_out_gga([], T44, 0)
convertE_in_gga(.(0, T53), T54, X86) → U5_gga(T53, T54, X86, pF_in_ggaa(T53, T54, X85, X86))
pF_in_ggaa(T53, T54, T57, X86) → U15_ggaa(T53, T54, T57, X86, convertE_in_gga(T53, T54, T57))
convertE_in_gga(.(s(T99), T100), T101, s(X151)) → U6_gga(T99, T100, T101, X151, convertA_in_gga(.(T99, T100), T101, X151))
convertA_in_gga(.(0, .(s(T160), T161)), T162, T12) → U2_gga(T160, T161, T162, T12, pC_in_gggaa(T160, T161, T162, X222, T12))
pC_in_gggaa(T160, T161, T162, T163, T12) → U21_gggaa(T160, T161, T162, T163, T12, convertA_in_gga(.(T160, T161), T162, T163))
convertA_in_gga(.(s(0), T185), T186, s(T188)) → U3_gga(T185, T186, T188, pD_in_ggaa(T185, T186, X259, T188))
pD_in_ggaa(T185, T186, T191, T188) → U23_ggaa(T185, T186, T191, T188, convertE_in_gga(T185, T186, T191))
U23_ggaa(T185, T186, T191, T188, convertE_out_gga(T185, T186, T191)) → U24_ggaa(T185, T186, T191, T188, timesK_in_gga(T191, T186, T188))
timesK_in_gga(0, T113, 0) → timesK_out_gga(0, T113, 0)
timesK_in_gga(s(T120), T121, T123) → U10_gga(T120, T121, T123, pL_in_ggaa(T120, T121, X175, T123))
pL_in_ggaa(T120, T121, T126, T123) → U19_ggaa(T120, T121, T126, T123, timesG_in_gga(T120, T121, T126))
timesG_in_gga(0, T66, 0) → timesG_out_gga(0, T66, 0)
timesG_in_gga(s(T71), T72, X111) → U7_gga(T71, T72, X111, pH_in_ggaa(T71, T72, X110, X111))
pH_in_ggaa(T71, T72, T75, X111) → U17_ggaa(T71, T72, T75, X111, timesG_in_gga(T71, T72, T75))
U17_ggaa(T71, T72, T75, X111, timesG_out_gga(T71, T72, T75)) → U18_ggaa(T71, T72, T75, X111, plusI_in_gga(T72, T75, X111))
plusI_in_gga(0, T84, T84) → plusI_out_gga(0, T84, T84)
plusI_in_gga(s(T89), T90, s(X134)) → U8_gga(T89, T90, X134, plusI_in_gga(T89, T90, X134))
U8_gga(T89, T90, X134, plusI_out_gga(T89, T90, X134)) → plusI_out_gga(s(T89), T90, s(X134))
U18_ggaa(T71, T72, T75, X111, plusI_out_gga(T72, T75, X111)) → pH_out_ggaa(T71, T72, T75, X111)
U7_gga(T71, T72, X111, pH_out_ggaa(T71, T72, X110, X111)) → timesG_out_gga(s(T71), T72, X111)
U19_ggaa(T120, T121, T126, T123, timesG_out_gga(T120, T121, T126)) → U20_ggaa(T120, T121, T126, T123, plusJ_in_gga(T121, T126, T123))
plusJ_in_gga(0, T135, T135) → plusJ_out_gga(0, T135, T135)
plusJ_in_gga(s(T142), T143, s(T145)) → U9_gga(T142, T143, T145, plusJ_in_gga(T142, T143, T145))
U9_gga(T142, T143, T145, plusJ_out_gga(T142, T143, T145)) → plusJ_out_gga(s(T142), T143, s(T145))
U20_ggaa(T120, T121, T126, T123, plusJ_out_gga(T121, T126, T123)) → pL_out_ggaa(T120, T121, T126, T123)
U10_gga(T120, T121, T123, pL_out_ggaa(T120, T121, X175, T123)) → timesK_out_gga(s(T120), T121, T123)
U24_ggaa(T185, T186, T191, T188, timesK_out_gga(T191, T186, T188)) → pD_out_ggaa(T185, T186, T191, T188)
U3_gga(T185, T186, T188, pD_out_ggaa(T185, T186, X259, T188)) → convertA_out_gga(.(s(0), T185), T186, s(T188))
convertA_in_gga(.(s(s(T204)), T205), T206, s(s(T208))) → U4_gga(T204, T205, T206, T208, convertA_in_gga(.(T204, T205), T206, T208))
U4_gga(T204, T205, T206, T208, convertA_out_gga(.(T204, T205), T206, T208)) → convertA_out_gga(.(s(s(T204)), T205), T206, s(s(T208)))
U21_gggaa(T160, T161, T162, T163, T12, convertA_out_gga(.(T160, T161), T162, T163)) → U22_gggaa(T160, T161, T162, T163, T12, timesK_in_gga(s(T163), T162, T12))
U22_gggaa(T160, T161, T162, T163, T12, timesK_out_gga(s(T163), T162, T12)) → pC_out_gggaa(T160, T161, T162, T163, T12)
U2_gga(T160, T161, T162, T12, pC_out_gggaa(T160, T161, T162, X222, T12)) → convertA_out_gga(.(0, .(s(T160), T161)), T162, T12)
U6_gga(T99, T100, T101, X151, convertA_out_gga(.(T99, T100), T101, X151)) → convertE_out_gga(.(s(T99), T100), T101, s(X151))
U15_ggaa(T53, T54, T57, X86, convertE_out_gga(T53, T54, T57)) → U16_ggaa(T53, T54, T57, X86, timesG_in_gga(T57, T54, X86))
U16_ggaa(T53, T54, T57, X86, timesG_out_gga(T57, T54, X86)) → pF_out_ggaa(T53, T54, T57, X86)
U5_gga(T53, T54, X86, pF_out_ggaa(T53, T54, X85, X86)) → convertE_out_gga(.(0, T53), T54, X86)
U11_ggaaa(T33, T34, T37, X54, T12, convertE_out_gga(T33, T34, T37)) → U12_ggaaa(T33, T34, T37, X54, T12, pM_in_ggaa(T37, T34, X54, T12))
pM_in_ggaa(T37, T34, T104, T12) → U13_ggaa(T37, T34, T104, T12, timesG_in_gga(T37, T34, T104))
U13_ggaa(T37, T34, T104, T12, timesG_out_gga(T37, T34, T104)) → U14_ggaa(T37, T34, T104, T12, timesK_in_gga(T104, T34, T12))
U14_ggaa(T37, T34, T104, T12, timesK_out_gga(T104, T34, T12)) → pM_out_ggaa(T37, T34, T104, T12)
U12_ggaaa(T33, T34, T37, X54, T12, pM_out_ggaa(T37, T34, X54, T12)) → pB_out_ggaaa(T33, T34, T37, X54, T12)
U1_gga(T33, T34, T12, pB_out_ggaaa(T33, T34, X53, X54, T12)) → convertA_out_gga(.(0, .(0, T33)), T34, T12)

The argument filtering Pi contains the following mapping:
convertA_in_gga(x1, x2, x3)  =  convertA_in_gga(x1, x2)
[]  =  []
convertA_out_gga(x1, x2, x3)  =  convertA_out_gga(x1, x2, x3)
.(x1, x2)  =  .(x1, x2)
0  =  0
U1_gga(x1, x2, x3, x4)  =  U1_gga(x1, x2, x4)
pB_in_ggaaa(x1, x2, x3, x4, x5)  =  pB_in_ggaaa(x1, x2)
U11_ggaaa(x1, x2, x3, x4, x5, x6)  =  U11_ggaaa(x1, x2, x6)
convertE_in_gga(x1, x2, x3)  =  convertE_in_gga(x1, x2)
convertE_out_gga(x1, x2, x3)  =  convertE_out_gga(x1, x2, x3)
U5_gga(x1, x2, x3, x4)  =  U5_gga(x1, x2, x4)
pF_in_ggaa(x1, x2, x3, x4)  =  pF_in_ggaa(x1, x2)
U15_ggaa(x1, x2, x3, x4, x5)  =  U15_ggaa(x1, x2, x5)
s(x1)  =  s(x1)
U6_gga(x1, x2, x3, x4, x5)  =  U6_gga(x1, x2, x3, x5)
U2_gga(x1, x2, x3, x4, x5)  =  U2_gga(x1, x2, x3, x5)
pC_in_gggaa(x1, x2, x3, x4, x5)  =  pC_in_gggaa(x1, x2, x3)
U21_gggaa(x1, x2, x3, x4, x5, x6)  =  U21_gggaa(x1, x2, x3, x6)
U3_gga(x1, x2, x3, x4)  =  U3_gga(x1, x2, x4)
pD_in_ggaa(x1, x2, x3, x4)  =  pD_in_ggaa(x1, x2)
U23_ggaa(x1, x2, x3, x4, x5)  =  U23_ggaa(x1, x2, x5)
U24_ggaa(x1, x2, x3, x4, x5)  =  U24_ggaa(x1, x2, x3, x5)
timesK_in_gga(x1, x2, x3)  =  timesK_in_gga(x1, x2)
timesK_out_gga(x1, x2, x3)  =  timesK_out_gga(x1, x2, x3)
U10_gga(x1, x2, x3, x4)  =  U10_gga(x1, x2, x4)
pL_in_ggaa(x1, x2, x3, x4)  =  pL_in_ggaa(x1, x2)
U19_ggaa(x1, x2, x3, x4, x5)  =  U19_ggaa(x1, x2, x5)
timesG_in_gga(x1, x2, x3)  =  timesG_in_gga(x1, x2)
timesG_out_gga(x1, x2, x3)  =  timesG_out_gga(x1, x2, x3)
U7_gga(x1, x2, x3, x4)  =  U7_gga(x1, x2, x4)
pH_in_ggaa(x1, x2, x3, x4)  =  pH_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)
plusI_in_gga(x1, x2, x3)  =  plusI_in_gga(x1, x2)
plusI_out_gga(x1, x2, x3)  =  plusI_out_gga(x1, x2, x3)
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)
U20_ggaa(x1, x2, x3, x4, x5)  =  U20_ggaa(x1, x2, x3, x5)
plusJ_in_gga(x1, x2, x3)  =  plusJ_in_gga(x1, x2)
plusJ_out_gga(x1, x2, x3)  =  plusJ_out_gga(x1, x2, x3)
U9_gga(x1, x2, x3, x4)  =  U9_gga(x1, x2, x4)
pL_out_ggaa(x1, x2, x3, x4)  =  pL_out_ggaa(x1, x2, x3, x4)
pD_out_ggaa(x1, x2, x3, x4)  =  pD_out_ggaa(x1, x2, x3, x4)
U4_gga(x1, x2, x3, x4, x5)  =  U4_gga(x1, x2, x3, x5)
U22_gggaa(x1, x2, x3, x4, x5, x6)  =  U22_gggaa(x1, x2, x3, x4, x6)
pC_out_gggaa(x1, x2, x3, x4, x5)  =  pC_out_gggaa(x1, x2, x3, x4, x5)
U16_ggaa(x1, x2, x3, x4, x5)  =  U16_ggaa(x1, x2, x3, x5)
pF_out_ggaa(x1, x2, x3, x4)  =  pF_out_ggaa(x1, x2, x3, x4)
U12_ggaaa(x1, x2, x3, x4, x5, x6)  =  U12_ggaaa(x1, x2, x3, x6)
pM_in_ggaa(x1, x2, x3, x4)  =  pM_in_ggaa(x1, x2)
U13_ggaa(x1, x2, x3, x4, x5)  =  U13_ggaa(x1, x2, x5)
U14_ggaa(x1, x2, x3, x4, x5)  =  U14_ggaa(x1, x2, x3, x5)
pM_out_ggaa(x1, x2, x3, x4)  =  pM_out_ggaa(x1, x2, x3, x4)
pB_out_ggaaa(x1, x2, x3, x4, x5)  =  pB_out_ggaaa(x1, x2, x3, x4, x5)
PLUSJ_IN_GGA(x1, x2, x3)  =  PLUSJ_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:

PLUSJ_IN_GGA(s(T142), T143, s(T145)) → PLUSJ_IN_GGA(T142, T143, T145)

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

PLUSJ_IN_GGA(s(T142), T143) → PLUSJ_IN_GGA(T142, T143)

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:

• PLUSJ_IN_GGA(s(T142), T143) → PLUSJ_IN_GGA(T142, T143)
  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:

PLUSI_IN_GGA(s(T89), T90, s(X134)) → PLUSI_IN_GGA(T89, T90, X134)

The TRS R consists of the following rules:

convertA_in_gga([], T5, 0) → convertA_out_gga([], T5, 0)
convertA_in_gga(.(0, []), T24, 0) → convertA_out_gga(.(0, []), T24, 0)
convertA_in_gga(.(0, .(0, T33)), T34, T12) → U1_gga(T33, T34, T12, pB_in_ggaaa(T33, T34, X53, X54, T12))
pB_in_ggaaa(T33, T34, T37, X54, T12) → U11_ggaaa(T33, T34, T37, X54, T12, convertE_in_gga(T33, T34, T37))
convertE_in_gga([], T44, 0) → convertE_out_gga([], T44, 0)
convertE_in_gga(.(0, T53), T54, X86) → U5_gga(T53, T54, X86, pF_in_ggaa(T53, T54, X85, X86))
pF_in_ggaa(T53, T54, T57, X86) → U15_ggaa(T53, T54, T57, X86, convertE_in_gga(T53, T54, T57))
convertE_in_gga(.(s(T99), T100), T101, s(X151)) → U6_gga(T99, T100, T101, X151, convertA_in_gga(.(T99, T100), T101, X151))
convertA_in_gga(.(0, .(s(T160), T161)), T162, T12) → U2_gga(T160, T161, T162, T12, pC_in_gggaa(T160, T161, T162, X222, T12))
pC_in_gggaa(T160, T161, T162, T163, T12) → U21_gggaa(T160, T161, T162, T163, T12, convertA_in_gga(.(T160, T161), T162, T163))
convertA_in_gga(.(s(0), T185), T186, s(T188)) → U3_gga(T185, T186, T188, pD_in_ggaa(T185, T186, X259, T188))
pD_in_ggaa(T185, T186, T191, T188) → U23_ggaa(T185, T186, T191, T188, convertE_in_gga(T185, T186, T191))
U23_ggaa(T185, T186, T191, T188, convertE_out_gga(T185, T186, T191)) → U24_ggaa(T185, T186, T191, T188, timesK_in_gga(T191, T186, T188))
timesK_in_gga(0, T113, 0) → timesK_out_gga(0, T113, 0)
timesK_in_gga(s(T120), T121, T123) → U10_gga(T120, T121, T123, pL_in_ggaa(T120, T121, X175, T123))
pL_in_ggaa(T120, T121, T126, T123) → U19_ggaa(T120, T121, T126, T123, timesG_in_gga(T120, T121, T126))
timesG_in_gga(0, T66, 0) → timesG_out_gga(0, T66, 0)
timesG_in_gga(s(T71), T72, X111) → U7_gga(T71, T72, X111, pH_in_ggaa(T71, T72, X110, X111))
pH_in_ggaa(T71, T72, T75, X111) → U17_ggaa(T71, T72, T75, X111, timesG_in_gga(T71, T72, T75))
U17_ggaa(T71, T72, T75, X111, timesG_out_gga(T71, T72, T75)) → U18_ggaa(T71, T72, T75, X111, plusI_in_gga(T72, T75, X111))
plusI_in_gga(0, T84, T84) → plusI_out_gga(0, T84, T84)
plusI_in_gga(s(T89), T90, s(X134)) → U8_gga(T89, T90, X134, plusI_in_gga(T89, T90, X134))
U8_gga(T89, T90, X134, plusI_out_gga(T89, T90, X134)) → plusI_out_gga(s(T89), T90, s(X134))
U18_ggaa(T71, T72, T75, X111, plusI_out_gga(T72, T75, X111)) → pH_out_ggaa(T71, T72, T75, X111)
U7_gga(T71, T72, X111, pH_out_ggaa(T71, T72, X110, X111)) → timesG_out_gga(s(T71), T72, X111)
U19_ggaa(T120, T121, T126, T123, timesG_out_gga(T120, T121, T126)) → U20_ggaa(T120, T121, T126, T123, plusJ_in_gga(T121, T126, T123))
plusJ_in_gga(0, T135, T135) → plusJ_out_gga(0, T135, T135)
plusJ_in_gga(s(T142), T143, s(T145)) → U9_gga(T142, T143, T145, plusJ_in_gga(T142, T143, T145))
U9_gga(T142, T143, T145, plusJ_out_gga(T142, T143, T145)) → plusJ_out_gga(s(T142), T143, s(T145))
U20_ggaa(T120, T121, T126, T123, plusJ_out_gga(T121, T126, T123)) → pL_out_ggaa(T120, T121, T126, T123)
U10_gga(T120, T121, T123, pL_out_ggaa(T120, T121, X175, T123)) → timesK_out_gga(s(T120), T121, T123)
U24_ggaa(T185, T186, T191, T188, timesK_out_gga(T191, T186, T188)) → pD_out_ggaa(T185, T186, T191, T188)
U3_gga(T185, T186, T188, pD_out_ggaa(T185, T186, X259, T188)) → convertA_out_gga(.(s(0), T185), T186, s(T188))
convertA_in_gga(.(s(s(T204)), T205), T206, s(s(T208))) → U4_gga(T204, T205, T206, T208, convertA_in_gga(.(T204, T205), T206, T208))
U4_gga(T204, T205, T206, T208, convertA_out_gga(.(T204, T205), T206, T208)) → convertA_out_gga(.(s(s(T204)), T205), T206, s(s(T208)))
U21_gggaa(T160, T161, T162, T163, T12, convertA_out_gga(.(T160, T161), T162, T163)) → U22_gggaa(T160, T161, T162, T163, T12, timesK_in_gga(s(T163), T162, T12))
U22_gggaa(T160, T161, T162, T163, T12, timesK_out_gga(s(T163), T162, T12)) → pC_out_gggaa(T160, T161, T162, T163, T12)
U2_gga(T160, T161, T162, T12, pC_out_gggaa(T160, T161, T162, X222, T12)) → convertA_out_gga(.(0, .(s(T160), T161)), T162, T12)
U6_gga(T99, T100, T101, X151, convertA_out_gga(.(T99, T100), T101, X151)) → convertE_out_gga(.(s(T99), T100), T101, s(X151))
U15_ggaa(T53, T54, T57, X86, convertE_out_gga(T53, T54, T57)) → U16_ggaa(T53, T54, T57, X86, timesG_in_gga(T57, T54, X86))
U16_ggaa(T53, T54, T57, X86, timesG_out_gga(T57, T54, X86)) → pF_out_ggaa(T53, T54, T57, X86)
U5_gga(T53, T54, X86, pF_out_ggaa(T53, T54, X85, X86)) → convertE_out_gga(.(0, T53), T54, X86)
U11_ggaaa(T33, T34, T37, X54, T12, convertE_out_gga(T33, T34, T37)) → U12_ggaaa(T33, T34, T37, X54, T12, pM_in_ggaa(T37, T34, X54, T12))
pM_in_ggaa(T37, T34, T104, T12) → U13_ggaa(T37, T34, T104, T12, timesG_in_gga(T37, T34, T104))
U13_ggaa(T37, T34, T104, T12, timesG_out_gga(T37, T34, T104)) → U14_ggaa(T37, T34, T104, T12, timesK_in_gga(T104, T34, T12))
U14_ggaa(T37, T34, T104, T12, timesK_out_gga(T104, T34, T12)) → pM_out_ggaa(T37, T34, T104, T12)
U12_ggaaa(T33, T34, T37, X54, T12, pM_out_ggaa(T37, T34, X54, T12)) → pB_out_ggaaa(T33, T34, T37, X54, T12)
U1_gga(T33, T34, T12, pB_out_ggaaa(T33, T34, X53, X54, T12)) → convertA_out_gga(.(0, .(0, T33)), T34, T12)

The argument filtering Pi contains the following mapping:
convertA_in_gga(x1, x2, x3)  =  convertA_in_gga(x1, x2)
[]  =  []
convertA_out_gga(x1, x2, x3)  =  convertA_out_gga(x1, x2, x3)
.(x1, x2)  =  .(x1, x2)
0  =  0
U1_gga(x1, x2, x3, x4)  =  U1_gga(x1, x2, x4)
pB_in_ggaaa(x1, x2, x3, x4, x5)  =  pB_in_ggaaa(x1, x2)
U11_ggaaa(x1, x2, x3, x4, x5, x6)  =  U11_ggaaa(x1, x2, x6)
convertE_in_gga(x1, x2, x3)  =  convertE_in_gga(x1, x2)
convertE_out_gga(x1, x2, x3)  =  convertE_out_gga(x1, x2, x3)
U5_gga(x1, x2, x3, x4)  =  U5_gga(x1, x2, x4)
pF_in_ggaa(x1, x2, x3, x4)  =  pF_in_ggaa(x1, x2)
U15_ggaa(x1, x2, x3, x4, x5)  =  U15_ggaa(x1, x2, x5)
s(x1)  =  s(x1)
U6_gga(x1, x2, x3, x4, x5)  =  U6_gga(x1, x2, x3, x5)
U2_gga(x1, x2, x3, x4, x5)  =  U2_gga(x1, x2, x3, x5)
pC_in_gggaa(x1, x2, x3, x4, x5)  =  pC_in_gggaa(x1, x2, x3)
U21_gggaa(x1, x2, x3, x4, x5, x6)  =  U21_gggaa(x1, x2, x3, x6)
U3_gga(x1, x2, x3, x4)  =  U3_gga(x1, x2, x4)
pD_in_ggaa(x1, x2, x3, x4)  =  pD_in_ggaa(x1, x2)
U23_ggaa(x1, x2, x3, x4, x5)  =  U23_ggaa(x1, x2, x5)
U24_ggaa(x1, x2, x3, x4, x5)  =  U24_ggaa(x1, x2, x3, x5)
timesK_in_gga(x1, x2, x3)  =  timesK_in_gga(x1, x2)
timesK_out_gga(x1, x2, x3)  =  timesK_out_gga(x1, x2, x3)
U10_gga(x1, x2, x3, x4)  =  U10_gga(x1, x2, x4)
pL_in_ggaa(x1, x2, x3, x4)  =  pL_in_ggaa(x1, x2)
U19_ggaa(x1, x2, x3, x4, x5)  =  U19_ggaa(x1, x2, x5)
timesG_in_gga(x1, x2, x3)  =  timesG_in_gga(x1, x2)
timesG_out_gga(x1, x2, x3)  =  timesG_out_gga(x1, x2, x3)
U7_gga(x1, x2, x3, x4)  =  U7_gga(x1, x2, x4)
pH_in_ggaa(x1, x2, x3, x4)  =  pH_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)
plusI_in_gga(x1, x2, x3)  =  plusI_in_gga(x1, x2)
plusI_out_gga(x1, x2, x3)  =  plusI_out_gga(x1, x2, x3)
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)
U20_ggaa(x1, x2, x3, x4, x5)  =  U20_ggaa(x1, x2, x3, x5)
plusJ_in_gga(x1, x2, x3)  =  plusJ_in_gga(x1, x2)
plusJ_out_gga(x1, x2, x3)  =  plusJ_out_gga(x1, x2, x3)
U9_gga(x1, x2, x3, x4)  =  U9_gga(x1, x2, x4)
pL_out_ggaa(x1, x2, x3, x4)  =  pL_out_ggaa(x1, x2, x3, x4)
pD_out_ggaa(x1, x2, x3, x4)  =  pD_out_ggaa(x1, x2, x3, x4)
U4_gga(x1, x2, x3, x4, x5)  =  U4_gga(x1, x2, x3, x5)
U22_gggaa(x1, x2, x3, x4, x5, x6)  =  U22_gggaa(x1, x2, x3, x4, x6)
pC_out_gggaa(x1, x2, x3, x4, x5)  =  pC_out_gggaa(x1, x2, x3, x4, x5)
U16_ggaa(x1, x2, x3, x4, x5)  =  U16_ggaa(x1, x2, x3, x5)
pF_out_ggaa(x1, x2, x3, x4)  =  pF_out_ggaa(x1, x2, x3, x4)
U12_ggaaa(x1, x2, x3, x4, x5, x6)  =  U12_ggaaa(x1, x2, x3, x6)
pM_in_ggaa(x1, x2, x3, x4)  =  pM_in_ggaa(x1, x2)
U13_ggaa(x1, x2, x3, x4, x5)  =  U13_ggaa(x1, x2, x5)
U14_ggaa(x1, x2, x3, x4, x5)  =  U14_ggaa(x1, x2, x3, x5)
pM_out_ggaa(x1, x2, x3, x4)  =  pM_out_ggaa(x1, x2, x3, x4)
pB_out_ggaaa(x1, x2, x3, x4, x5)  =  pB_out_ggaaa(x1, x2, x3, x4, x5)
PLUSI_IN_GGA(x1, x2, x3)  =  PLUSI_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:

PLUSI_IN_GGA(s(T89), T90, s(X134)) → PLUSI_IN_GGA(T89, T90, X134)

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

PLUSI_IN_GGA(s(T89), T90) → PLUSI_IN_GGA(T89, T90)

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:

• PLUSI_IN_GGA(s(T89), T90) → PLUSI_IN_GGA(T89, T90)
  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:

TIMESG_IN_GGA(s(T71), T72, X111) → PH_IN_GGAA(T71, T72, X110, X111)
PH_IN_GGAA(T71, T72, T75, X111) → TIMESG_IN_GGA(T71, T72, T75)

The TRS R consists of the following rules:

convertA_in_gga([], T5, 0) → convertA_out_gga([], T5, 0)
convertA_in_gga(.(0, []), T24, 0) → convertA_out_gga(.(0, []), T24, 0)
convertA_in_gga(.(0, .(0, T33)), T34, T12) → U1_gga(T33, T34, T12, pB_in_ggaaa(T33, T34, X53, X54, T12))
pB_in_ggaaa(T33, T34, T37, X54, T12) → U11_ggaaa(T33, T34, T37, X54, T12, convertE_in_gga(T33, T34, T37))
convertE_in_gga([], T44, 0) → convertE_out_gga([], T44, 0)
convertE_in_gga(.(0, T53), T54, X86) → U5_gga(T53, T54, X86, pF_in_ggaa(T53, T54, X85, X86))
pF_in_ggaa(T53, T54, T57, X86) → U15_ggaa(T53, T54, T57, X86, convertE_in_gga(T53, T54, T57))
convertE_in_gga(.(s(T99), T100), T101, s(X151)) → U6_gga(T99, T100, T101, X151, convertA_in_gga(.(T99, T100), T101, X151))
convertA_in_gga(.(0, .(s(T160), T161)), T162, T12) → U2_gga(T160, T161, T162, T12, pC_in_gggaa(T160, T161, T162, X222, T12))
pC_in_gggaa(T160, T161, T162, T163, T12) → U21_gggaa(T160, T161, T162, T163, T12, convertA_in_gga(.(T160, T161), T162, T163))
convertA_in_gga(.(s(0), T185), T186, s(T188)) → U3_gga(T185, T186, T188, pD_in_ggaa(T185, T186, X259, T188))
pD_in_ggaa(T185, T186, T191, T188) → U23_ggaa(T185, T186, T191, T188, convertE_in_gga(T185, T186, T191))
U23_ggaa(T185, T186, T191, T188, convertE_out_gga(T185, T186, T191)) → U24_ggaa(T185, T186, T191, T188, timesK_in_gga(T191, T186, T188))
timesK_in_gga(0, T113, 0) → timesK_out_gga(0, T113, 0)
timesK_in_gga(s(T120), T121, T123) → U10_gga(T120, T121, T123, pL_in_ggaa(T120, T121, X175, T123))
pL_in_ggaa(T120, T121, T126, T123) → U19_ggaa(T120, T121, T126, T123, timesG_in_gga(T120, T121, T126))
timesG_in_gga(0, T66, 0) → timesG_out_gga(0, T66, 0)
timesG_in_gga(s(T71), T72, X111) → U7_gga(T71, T72, X111, pH_in_ggaa(T71, T72, X110, X111))
pH_in_ggaa(T71, T72, T75, X111) → U17_ggaa(T71, T72, T75, X111, timesG_in_gga(T71, T72, T75))
U17_ggaa(T71, T72, T75, X111, timesG_out_gga(T71, T72, T75)) → U18_ggaa(T71, T72, T75, X111, plusI_in_gga(T72, T75, X111))
plusI_in_gga(0, T84, T84) → plusI_out_gga(0, T84, T84)
plusI_in_gga(s(T89), T90, s(X134)) → U8_gga(T89, T90, X134, plusI_in_gga(T89, T90, X134))
U8_gga(T89, T90, X134, plusI_out_gga(T89, T90, X134)) → plusI_out_gga(s(T89), T90, s(X134))
U18_ggaa(T71, T72, T75, X111, plusI_out_gga(T72, T75, X111)) → pH_out_ggaa(T71, T72, T75, X111)
U7_gga(T71, T72, X111, pH_out_ggaa(T71, T72, X110, X111)) → timesG_out_gga(s(T71), T72, X111)
U19_ggaa(T120, T121, T126, T123, timesG_out_gga(T120, T121, T126)) → U20_ggaa(T120, T121, T126, T123, plusJ_in_gga(T121, T126, T123))
plusJ_in_gga(0, T135, T135) → plusJ_out_gga(0, T135, T135)
plusJ_in_gga(s(T142), T143, s(T145)) → U9_gga(T142, T143, T145, plusJ_in_gga(T142, T143, T145))
U9_gga(T142, T143, T145, plusJ_out_gga(T142, T143, T145)) → plusJ_out_gga(s(T142), T143, s(T145))
U20_ggaa(T120, T121, T126, T123, plusJ_out_gga(T121, T126, T123)) → pL_out_ggaa(T120, T121, T126, T123)
U10_gga(T120, T121, T123, pL_out_ggaa(T120, T121, X175, T123)) → timesK_out_gga(s(T120), T121, T123)
U24_ggaa(T185, T186, T191, T188, timesK_out_gga(T191, T186, T188)) → pD_out_ggaa(T185, T186, T191, T188)
U3_gga(T185, T186, T188, pD_out_ggaa(T185, T186, X259, T188)) → convertA_out_gga(.(s(0), T185), T186, s(T188))
convertA_in_gga(.(s(s(T204)), T205), T206, s(s(T208))) → U4_gga(T204, T205, T206, T208, convertA_in_gga(.(T204, T205), T206, T208))
U4_gga(T204, T205, T206, T208, convertA_out_gga(.(T204, T205), T206, T208)) → convertA_out_gga(.(s(s(T204)), T205), T206, s(s(T208)))
U21_gggaa(T160, T161, T162, T163, T12, convertA_out_gga(.(T160, T161), T162, T163)) → U22_gggaa(T160, T161, T162, T163, T12, timesK_in_gga(s(T163), T162, T12))
U22_gggaa(T160, T161, T162, T163, T12, timesK_out_gga(s(T163), T162, T12)) → pC_out_gggaa(T160, T161, T162, T163, T12)
U2_gga(T160, T161, T162, T12, pC_out_gggaa(T160, T161, T162, X222, T12)) → convertA_out_gga(.(0, .(s(T160), T161)), T162, T12)
U6_gga(T99, T100, T101, X151, convertA_out_gga(.(T99, T100), T101, X151)) → convertE_out_gga(.(s(T99), T100), T101, s(X151))
U15_ggaa(T53, T54, T57, X86, convertE_out_gga(T53, T54, T57)) → U16_ggaa(T53, T54, T57, X86, timesG_in_gga(T57, T54, X86))
U16_ggaa(T53, T54, T57, X86, timesG_out_gga(T57, T54, X86)) → pF_out_ggaa(T53, T54, T57, X86)
U5_gga(T53, T54, X86, pF_out_ggaa(T53, T54, X85, X86)) → convertE_out_gga(.(0, T53), T54, X86)
U11_ggaaa(T33, T34, T37, X54, T12, convertE_out_gga(T33, T34, T37)) → U12_ggaaa(T33, T34, T37, X54, T12, pM_in_ggaa(T37, T34, X54, T12))
pM_in_ggaa(T37, T34, T104, T12) → U13_ggaa(T37, T34, T104, T12, timesG_in_gga(T37, T34, T104))
U13_ggaa(T37, T34, T104, T12, timesG_out_gga(T37, T34, T104)) → U14_ggaa(T37, T34, T104, T12, timesK_in_gga(T104, T34, T12))
U14_ggaa(T37, T34, T104, T12, timesK_out_gga(T104, T34, T12)) → pM_out_ggaa(T37, T34, T104, T12)
U12_ggaaa(T33, T34, T37, X54, T12, pM_out_ggaa(T37, T34, X54, T12)) → pB_out_ggaaa(T33, T34, T37, X54, T12)
U1_gga(T33, T34, T12, pB_out_ggaaa(T33, T34, X53, X54, T12)) → convertA_out_gga(.(0, .(0, T33)), T34, T12)

The argument filtering Pi contains the following mapping:
convertA_in_gga(x1, x2, x3)  =  convertA_in_gga(x1, x2)
[]  =  []
convertA_out_gga(x1, x2, x3)  =  convertA_out_gga(x1, x2, x3)
.(x1, x2)  =  .(x1, x2)
0  =  0
U1_gga(x1, x2, x3, x4)  =  U1_gga(x1, x2, x4)
pB_in_ggaaa(x1, x2, x3, x4, x5)  =  pB_in_ggaaa(x1, x2)
U11_ggaaa(x1, x2, x3, x4, x5, x6)  =  U11_ggaaa(x1, x2, x6)
convertE_in_gga(x1, x2, x3)  =  convertE_in_gga(x1, x2)
convertE_out_gga(x1, x2, x3)  =  convertE_out_gga(x1, x2, x3)
U5_gga(x1, x2, x3, x4)  =  U5_gga(x1, x2, x4)
pF_in_ggaa(x1, x2, x3, x4)  =  pF_in_ggaa(x1, x2)
U15_ggaa(x1, x2, x3, x4, x5)  =  U15_ggaa(x1, x2, x5)
s(x1)  =  s(x1)
U6_gga(x1, x2, x3, x4, x5)  =  U6_gga(x1, x2, x3, x5)
U2_gga(x1, x2, x3, x4, x5)  =  U2_gga(x1, x2, x3, x5)
pC_in_gggaa(x1, x2, x3, x4, x5)  =  pC_in_gggaa(x1, x2, x3)
U21_gggaa(x1, x2, x3, x4, x5, x6)  =  U21_gggaa(x1, x2, x3, x6)
U3_gga(x1, x2, x3, x4)  =  U3_gga(x1, x2, x4)
pD_in_ggaa(x1, x2, x3, x4)  =  pD_in_ggaa(x1, x2)
U23_ggaa(x1, x2, x3, x4, x5)  =  U23_ggaa(x1, x2, x5)
U24_ggaa(x1, x2, x3, x4, x5)  =  U24_ggaa(x1, x2, x3, x5)
timesK_in_gga(x1, x2, x3)  =  timesK_in_gga(x1, x2)
timesK_out_gga(x1, x2, x3)  =  timesK_out_gga(x1, x2, x3)
U10_gga(x1, x2, x3, x4)  =  U10_gga(x1, x2, x4)
pL_in_ggaa(x1, x2, x3, x4)  =  pL_in_ggaa(x1, x2)
U19_ggaa(x1, x2, x3, x4, x5)  =  U19_ggaa(x1, x2, x5)
timesG_in_gga(x1, x2, x3)  =  timesG_in_gga(x1, x2)
timesG_out_gga(x1, x2, x3)  =  timesG_out_gga(x1, x2, x3)
U7_gga(x1, x2, x3, x4)  =  U7_gga(x1, x2, x4)
pH_in_ggaa(x1, x2, x3, x4)  =  pH_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)
plusI_in_gga(x1, x2, x3)  =  plusI_in_gga(x1, x2)
plusI_out_gga(x1, x2, x3)  =  plusI_out_gga(x1, x2, x3)
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)
U20_ggaa(x1, x2, x3, x4, x5)  =  U20_ggaa(x1, x2, x3, x5)
plusJ_in_gga(x1, x2, x3)  =  plusJ_in_gga(x1, x2)
plusJ_out_gga(x1, x2, x3)  =  plusJ_out_gga(x1, x2, x3)
U9_gga(x1, x2, x3, x4)  =  U9_gga(x1, x2, x4)
pL_out_ggaa(x1, x2, x3, x4)  =  pL_out_ggaa(x1, x2, x3, x4)
pD_out_ggaa(x1, x2, x3, x4)  =  pD_out_ggaa(x1, x2, x3, x4)
U4_gga(x1, x2, x3, x4, x5)  =  U4_gga(x1, x2, x3, x5)
U22_gggaa(x1, x2, x3, x4, x5, x6)  =  U22_gggaa(x1, x2, x3, x4, x6)
pC_out_gggaa(x1, x2, x3, x4, x5)  =  pC_out_gggaa(x1, x2, x3, x4, x5)
U16_ggaa(x1, x2, x3, x4, x5)  =  U16_ggaa(x1, x2, x3, x5)
pF_out_ggaa(x1, x2, x3, x4)  =  pF_out_ggaa(x1, x2, x3, x4)
U12_ggaaa(x1, x2, x3, x4, x5, x6)  =  U12_ggaaa(x1, x2, x3, x6)
pM_in_ggaa(x1, x2, x3, x4)  =  pM_in_ggaa(x1, x2)
U13_ggaa(x1, x2, x3, x4, x5)  =  U13_ggaa(x1, x2, x5)
U14_ggaa(x1, x2, x3, x4, x5)  =  U14_ggaa(x1, x2, x3, x5)
pM_out_ggaa(x1, x2, x3, x4)  =  pM_out_ggaa(x1, x2, x3, x4)
pB_out_ggaaa(x1, x2, x3, x4, x5)  =  pB_out_ggaaa(x1, x2, x3, x4, x5)
TIMESG_IN_GGA(x1, x2, x3)  =  TIMESG_IN_GGA(x1, x2)
PH_IN_GGAA(x1, x2, x3, x4)  =  PH_IN_GGAA(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:

TIMESG_IN_GGA(s(T71), T72, X111) → PH_IN_GGAA(T71, T72, X110, X111)
PH_IN_GGAA(T71, T72, T75, X111) → TIMESG_IN_GGA(T71, T72, T75)

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

TIMESG_IN_GGA(s(T71), T72) → PH_IN_GGAA(T71, T72)
PH_IN_GGAA(T71, T72) → TIMESG_IN_GGA(T71, T72)

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:

• PH_IN_GGAA(T71, T72) → TIMESG_IN_GGA(T71, T72)
  The graph contains the following edges 1 >= 1, 2 >= 2

• TIMESG_IN_GGA(s(T71), T72) → PH_IN_GGAA(T71, T72)
  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:

CONVERTA_IN_GGA(.(0, .(0, T33)), T34, T12) → PB_IN_GGAAA(T33, T34, X53, X54, T12)
PB_IN_GGAAA(T33, T34, T37, X54, T12) → CONVERTE_IN_GGA(T33, T34, T37)
CONVERTE_IN_GGA(.(0, T53), T54, X86) → PF_IN_GGAA(T53, T54, X85, X86)
PF_IN_GGAA(T53, T54, T57, X86) → CONVERTE_IN_GGA(T53, T54, T57)
CONVERTE_IN_GGA(.(s(T99), T100), T101, s(X151)) → CONVERTA_IN_GGA(.(T99, T100), T101, X151)
CONVERTA_IN_GGA(.(0, .(s(T160), T161)), T162, T12) → PC_IN_GGGAA(T160, T161, T162, X222, T12)
PC_IN_GGGAA(T160, T161, T162, T163, T12) → CONVERTA_IN_GGA(.(T160, T161), T162, T163)
CONVERTA_IN_GGA(.(s(0), T185), T186, s(T188)) → PD_IN_GGAA(T185, T186, X259, T188)
PD_IN_GGAA(T185, T186, T191, T188) → CONVERTE_IN_GGA(T185, T186, T191)
CONVERTA_IN_GGA(.(s(s(T204)), T205), T206, s(s(T208))) → CONVERTA_IN_GGA(.(T204, T205), T206, T208)

The TRS R consists of the following rules:

convertA_in_gga([], T5, 0) → convertA_out_gga([], T5, 0)
convertA_in_gga(.(0, []), T24, 0) → convertA_out_gga(.(0, []), T24, 0)
convertA_in_gga(.(0, .(0, T33)), T34, T12) → U1_gga(T33, T34, T12, pB_in_ggaaa(T33, T34, X53, X54, T12))
pB_in_ggaaa(T33, T34, T37, X54, T12) → U11_ggaaa(T33, T34, T37, X54, T12, convertE_in_gga(T33, T34, T37))
convertE_in_gga([], T44, 0) → convertE_out_gga([], T44, 0)
convertE_in_gga(.(0, T53), T54, X86) → U5_gga(T53, T54, X86, pF_in_ggaa(T53, T54, X85, X86))
pF_in_ggaa(T53, T54, T57, X86) → U15_ggaa(T53, T54, T57, X86, convertE_in_gga(T53, T54, T57))
convertE_in_gga(.(s(T99), T100), T101, s(X151)) → U6_gga(T99, T100, T101, X151, convertA_in_gga(.(T99, T100), T101, X151))
convertA_in_gga(.(0, .(s(T160), T161)), T162, T12) → U2_gga(T160, T161, T162, T12, pC_in_gggaa(T160, T161, T162, X222, T12))
pC_in_gggaa(T160, T161, T162, T163, T12) → U21_gggaa(T160, T161, T162, T163, T12, convertA_in_gga(.(T160, T161), T162, T163))
convertA_in_gga(.(s(0), T185), T186, s(T188)) → U3_gga(T185, T186, T188, pD_in_ggaa(T185, T186, X259, T188))
pD_in_ggaa(T185, T186, T191, T188) → U23_ggaa(T185, T186, T191, T188, convertE_in_gga(T185, T186, T191))
U23_ggaa(T185, T186, T191, T188, convertE_out_gga(T185, T186, T191)) → U24_ggaa(T185, T186, T191, T188, timesK_in_gga(T191, T186, T188))
timesK_in_gga(0, T113, 0) → timesK_out_gga(0, T113, 0)
timesK_in_gga(s(T120), T121, T123) → U10_gga(T120, T121, T123, pL_in_ggaa(T120, T121, X175, T123))
pL_in_ggaa(T120, T121, T126, T123) → U19_ggaa(T120, T121, T126, T123, timesG_in_gga(T120, T121, T126))
timesG_in_gga(0, T66, 0) → timesG_out_gga(0, T66, 0)
timesG_in_gga(s(T71), T72, X111) → U7_gga(T71, T72, X111, pH_in_ggaa(T71, T72, X110, X111))
pH_in_ggaa(T71, T72, T75, X111) → U17_ggaa(T71, T72, T75, X111, timesG_in_gga(T71, T72, T75))
U17_ggaa(T71, T72, T75, X111, timesG_out_gga(T71, T72, T75)) → U18_ggaa(T71, T72, T75, X111, plusI_in_gga(T72, T75, X111))
plusI_in_gga(0, T84, T84) → plusI_out_gga(0, T84, T84)
plusI_in_gga(s(T89), T90, s(X134)) → U8_gga(T89, T90, X134, plusI_in_gga(T89, T90, X134))
U8_gga(T89, T90, X134, plusI_out_gga(T89, T90, X134)) → plusI_out_gga(s(T89), T90, s(X134))
U18_ggaa(T71, T72, T75, X111, plusI_out_gga(T72, T75, X111)) → pH_out_ggaa(T71, T72, T75, X111)
U7_gga(T71, T72, X111, pH_out_ggaa(T71, T72, X110, X111)) → timesG_out_gga(s(T71), T72, X111)
U19_ggaa(T120, T121, T126, T123, timesG_out_gga(T120, T121, T126)) → U20_ggaa(T120, T121, T126, T123, plusJ_in_gga(T121, T126, T123))
plusJ_in_gga(0, T135, T135) → plusJ_out_gga(0, T135, T135)
plusJ_in_gga(s(T142), T143, s(T145)) → U9_gga(T142, T143, T145, plusJ_in_gga(T142, T143, T145))
U9_gga(T142, T143, T145, plusJ_out_gga(T142, T143, T145)) → plusJ_out_gga(s(T142), T143, s(T145))
U20_ggaa(T120, T121, T126, T123, plusJ_out_gga(T121, T126, T123)) → pL_out_ggaa(T120, T121, T126, T123)
U10_gga(T120, T121, T123, pL_out_ggaa(T120, T121, X175, T123)) → timesK_out_gga(s(T120), T121, T123)
U24_ggaa(T185, T186, T191, T188, timesK_out_gga(T191, T186, T188)) → pD_out_ggaa(T185, T186, T191, T188)
U3_gga(T185, T186, T188, pD_out_ggaa(T185, T186, X259, T188)) → convertA_out_gga(.(s(0), T185), T186, s(T188))
convertA_in_gga(.(s(s(T204)), T205), T206, s(s(T208))) → U4_gga(T204, T205, T206, T208, convertA_in_gga(.(T204, T205), T206, T208))
U4_gga(T204, T205, T206, T208, convertA_out_gga(.(T204, T205), T206, T208)) → convertA_out_gga(.(s(s(T204)), T205), T206, s(s(T208)))
U21_gggaa(T160, T161, T162, T163, T12, convertA_out_gga(.(T160, T161), T162, T163)) → U22_gggaa(T160, T161, T162, T163, T12, timesK_in_gga(s(T163), T162, T12))
U22_gggaa(T160, T161, T162, T163, T12, timesK_out_gga(s(T163), T162, T12)) → pC_out_gggaa(T160, T161, T162, T163, T12)
U2_gga(T160, T161, T162, T12, pC_out_gggaa(T160, T161, T162, X222, T12)) → convertA_out_gga(.(0, .(s(T160), T161)), T162, T12)
U6_gga(T99, T100, T101, X151, convertA_out_gga(.(T99, T100), T101, X151)) → convertE_out_gga(.(s(T99), T100), T101, s(X151))
U15_ggaa(T53, T54, T57, X86, convertE_out_gga(T53, T54, T57)) → U16_ggaa(T53, T54, T57, X86, timesG_in_gga(T57, T54, X86))
U16_ggaa(T53, T54, T57, X86, timesG_out_gga(T57, T54, X86)) → pF_out_ggaa(T53, T54, T57, X86)
U5_gga(T53, T54, X86, pF_out_ggaa(T53, T54, X85, X86)) → convertE_out_gga(.(0, T53), T54, X86)
U11_ggaaa(T33, T34, T37, X54, T12, convertE_out_gga(T33, T34, T37)) → U12_ggaaa(T33, T34, T37, X54, T12, pM_in_ggaa(T37, T34, X54, T12))
pM_in_ggaa(T37, T34, T104, T12) → U13_ggaa(T37, T34, T104, T12, timesG_in_gga(T37, T34, T104))
U13_ggaa(T37, T34, T104, T12, timesG_out_gga(T37, T34, T104)) → U14_ggaa(T37, T34, T104, T12, timesK_in_gga(T104, T34, T12))
U14_ggaa(T37, T34, T104, T12, timesK_out_gga(T104, T34, T12)) → pM_out_ggaa(T37, T34, T104, T12)
U12_ggaaa(T33, T34, T37, X54, T12, pM_out_ggaa(T37, T34, X54, T12)) → pB_out_ggaaa(T33, T34, T37, X54, T12)
U1_gga(T33, T34, T12, pB_out_ggaaa(T33, T34, X53, X54, T12)) → convertA_out_gga(.(0, .(0, T33)), T34, T12)

The argument filtering Pi contains the following mapping:
convertA_in_gga(x1, x2, x3)  =  convertA_in_gga(x1, x2)
[]  =  []
convertA_out_gga(x1, x2, x3)  =  convertA_out_gga(x1, x2, x3)
.(x1, x2)  =  .(x1, x2)
0  =  0
U1_gga(x1, x2, x3, x4)  =  U1_gga(x1, x2, x4)
pB_in_ggaaa(x1, x2, x3, x4, x5)  =  pB_in_ggaaa(x1, x2)
U11_ggaaa(x1, x2, x3, x4, x5, x6)  =  U11_ggaaa(x1, x2, x6)
convertE_in_gga(x1, x2, x3)  =  convertE_in_gga(x1, x2)
convertE_out_gga(x1, x2, x3)  =  convertE_out_gga(x1, x2, x3)
U5_gga(x1, x2, x3, x4)  =  U5_gga(x1, x2, x4)
pF_in_ggaa(x1, x2, x3, x4)  =  pF_in_ggaa(x1, x2)
U15_ggaa(x1, x2, x3, x4, x5)  =  U15_ggaa(x1, x2, x5)
s(x1)  =  s(x1)
U6_gga(x1, x2, x3, x4, x5)  =  U6_gga(x1, x2, x3, x5)
U2_gga(x1, x2, x3, x4, x5)  =  U2_gga(x1, x2, x3, x5)
pC_in_gggaa(x1, x2, x3, x4, x5)  =  pC_in_gggaa(x1, x2, x3)
U21_gggaa(x1, x2, x3, x4, x5, x6)  =  U21_gggaa(x1, x2, x3, x6)
U3_gga(x1, x2, x3, x4)  =  U3_gga(x1, x2, x4)
pD_in_ggaa(x1, x2, x3, x4)  =  pD_in_ggaa(x1, x2)
U23_ggaa(x1, x2, x3, x4, x5)  =  U23_ggaa(x1, x2, x5)
U24_ggaa(x1, x2, x3, x4, x5)  =  U24_ggaa(x1, x2, x3, x5)
timesK_in_gga(x1, x2, x3)  =  timesK_in_gga(x1, x2)
timesK_out_gga(x1, x2, x3)  =  timesK_out_gga(x1, x2, x3)
U10_gga(x1, x2, x3, x4)  =  U10_gga(x1, x2, x4)
pL_in_ggaa(x1, x2, x3, x4)  =  pL_in_ggaa(x1, x2)
U19_ggaa(x1, x2, x3, x4, x5)  =  U19_ggaa(x1, x2, x5)
timesG_in_gga(x1, x2, x3)  =  timesG_in_gga(x1, x2)
timesG_out_gga(x1, x2, x3)  =  timesG_out_gga(x1, x2, x3)
U7_gga(x1, x2, x3, x4)  =  U7_gga(x1, x2, x4)
pH_in_ggaa(x1, x2, x3, x4)  =  pH_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)
plusI_in_gga(x1, x2, x3)  =  plusI_in_gga(x1, x2)
plusI_out_gga(x1, x2, x3)  =  plusI_out_gga(x1, x2, x3)
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)
U20_ggaa(x1, x2, x3, x4, x5)  =  U20_ggaa(x1, x2, x3, x5)
plusJ_in_gga(x1, x2, x3)  =  plusJ_in_gga(x1, x2)
plusJ_out_gga(x1, x2, x3)  =  plusJ_out_gga(x1, x2, x3)
U9_gga(x1, x2, x3, x4)  =  U9_gga(x1, x2, x4)
pL_out_ggaa(x1, x2, x3, x4)  =  pL_out_ggaa(x1, x2, x3, x4)
pD_out_ggaa(x1, x2, x3, x4)  =  pD_out_ggaa(x1, x2, x3, x4)
U4_gga(x1, x2, x3, x4, x5)  =  U4_gga(x1, x2, x3, x5)
U22_gggaa(x1, x2, x3, x4, x5, x6)  =  U22_gggaa(x1, x2, x3, x4, x6)
pC_out_gggaa(x1, x2, x3, x4, x5)  =  pC_out_gggaa(x1, x2, x3, x4, x5)
U16_ggaa(x1, x2, x3, x4, x5)  =  U16_ggaa(x1, x2, x3, x5)
pF_out_ggaa(x1, x2, x3, x4)  =  pF_out_ggaa(x1, x2, x3, x4)
U12_ggaaa(x1, x2, x3, x4, x5, x6)  =  U12_ggaaa(x1, x2, x3, x6)
pM_in_ggaa(x1, x2, x3, x4)  =  pM_in_ggaa(x1, x2)
U13_ggaa(x1, x2, x3, x4, x5)  =  U13_ggaa(x1, x2, x5)
U14_ggaa(x1, x2, x3, x4, x5)  =  U14_ggaa(x1, x2, x3, x5)
pM_out_ggaa(x1, x2, x3, x4)  =  pM_out_ggaa(x1, x2, x3, x4)
pB_out_ggaaa(x1, x2, x3, x4, x5)  =  pB_out_ggaaa(x1, x2, x3, x4, x5)
CONVERTA_IN_GGA(x1, x2, x3)  =  CONVERTA_IN_GGA(x1, x2)
PB_IN_GGAAA(x1, x2, x3, x4, x5)  =  PB_IN_GGAAA(x1, x2)
CONVERTE_IN_GGA(x1, x2, x3)  =  CONVERTE_IN_GGA(x1, x2)
PF_IN_GGAA(x1, x2, x3, x4)  =  PF_IN_GGAA(x1, x2)
PC_IN_GGGAA(x1, x2, x3, x4, x5)  =  PC_IN_GGGAA(x1, x2, x3)
PD_IN_GGAA(x1, x2, x3, x4)  =  PD_IN_GGAA(x1, x2)

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:

CONVERTA_IN_GGA(.(0, .(0, T33)), T34, T12) → PB_IN_GGAAA(T33, T34, X53, X54, T12)
PB_IN_GGAAA(T33, T34, T37, X54, T12) → CONVERTE_IN_GGA(T33, T34, T37)
CONVERTE_IN_GGA(.(0, T53), T54, X86) → PF_IN_GGAA(T53, T54, X85, X86)
PF_IN_GGAA(T53, T54, T57, X86) → CONVERTE_IN_GGA(T53, T54, T57)
CONVERTE_IN_GGA(.(s(T99), T100), T101, s(X151)) → CONVERTA_IN_GGA(.(T99, T100), T101, X151)
CONVERTA_IN_GGA(.(0, .(s(T160), T161)), T162, T12) → PC_IN_GGGAA(T160, T161, T162, X222, T12)
PC_IN_GGGAA(T160, T161, T162, T163, T12) → CONVERTA_IN_GGA(.(T160, T161), T162, T163)
CONVERTA_IN_GGA(.(s(0), T185), T186, s(T188)) → PD_IN_GGAA(T185, T186, X259, T188)
PD_IN_GGAA(T185, T186, T191, T188) → CONVERTE_IN_GGA(T185, T186, T191)
CONVERTA_IN_GGA(.(s(s(T204)), T205), T206, s(s(T208))) → CONVERTA_IN_GGA(.(T204, T205), T206, T208)

R is empty.
The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
0  =  0
s(x1)  =  s(x1)
CONVERTA_IN_GGA(x1, x2, x3)  =  CONVERTA_IN_GGA(x1, x2)
PB_IN_GGAAA(x1, x2, x3, x4, x5)  =  PB_IN_GGAAA(x1, x2)
CONVERTE_IN_GGA(x1, x2, x3)  =  CONVERTE_IN_GGA(x1, x2)
PF_IN_GGAA(x1, x2, x3, x4)  =  PF_IN_GGAA(x1, x2)
PC_IN_GGGAA(x1, x2, x3, x4, x5)  =  PC_IN_GGGAA(x1, x2, x3)
PD_IN_GGAA(x1, x2, x3, x4)  =  PD_IN_GGAA(x1, x2)

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:

CONVERTA_IN_GGA(.(0, .(0, T33)), T34) → PB_IN_GGAAA(T33, T34)
PB_IN_GGAAA(T33, T34) → CONVERTE_IN_GGA(T33, T34)
CONVERTE_IN_GGA(.(0, T53), T54) → PF_IN_GGAA(T53, T54)
PF_IN_GGAA(T53, T54) → CONVERTE_IN_GGA(T53, T54)
CONVERTE_IN_GGA(.(s(T99), T100), T101) → CONVERTA_IN_GGA(.(T99, T100), T101)
CONVERTA_IN_GGA(.(0, .(s(T160), T161)), T162) → PC_IN_GGGAA(T160, T161, T162)
PC_IN_GGGAA(T160, T161, T162) → CONVERTA_IN_GGA(.(T160, T161), T162)
CONVERTA_IN_GGA(.(s(0), T185), T186) → PD_IN_GGAA(T185, T186)
PD_IN_GGAA(T185, T186) → CONVERTE_IN_GGA(T185, T186)
CONVERTA_IN_GGA(.(s(s(T204)), T205), T206) → CONVERTA_IN_GGA(.(T204, T205), T206)

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

(33) UsableRulesReductionPairsProof (EQUIVALENT transformation)

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

The following dependency pairs can be deleted:

CONVERTA_IN_GGA(.(0, .(0, T33)), T34) → PB_IN_GGAAA(T33, T34)
CONVERTE_IN_GGA(.(0, T53), T54) → PF_IN_GGAA(T53, T54)
CONVERTE_IN_GGA(.(s(T99), T100), T101) → CONVERTA_IN_GGA(.(T99, T100), T101)
CONVERTA_IN_GGA(.(0, .(s(T160), T161)), T162) → PC_IN_GGGAA(T160, T161, T162)
CONVERTA_IN_GGA(.(s(0), T185), T186) → PD_IN_GGAA(T185, T186)
CONVERTA_IN_GGA(.(s(s(T204)), T205), T206) → CONVERTA_IN_GGA(.(T204, T205), T206)

No rules are removed from R.

Used ordering: POLO with Polynomial interpretation [POLO]:

POL(.(x₁, x₂)) = 2·x₁ + 2·x₂   
POL(0) = 0   
POL(CONVERTA_IN_GGA(x₁, x₂)) = x₁ + x₂   
POL(CONVERTE_IN_GGA(x₁, x₂)) = x₁ + x₂   
POL(PB_IN_GGAAA(x₁, x₂)) = 2·x₁ + x₂   
POL(PC_IN_GGGAA(x₁, x₂, x₃)) = 2·x₁ + 2·x₂ + x₃   
POL(PD_IN_GGAA(x₁, x₂)) = 2·x₁ + x₂   
POL(PF_IN_GGAA(x₁, x₂)) = 2·x₁ + x₂   
POL(s(x₁)) = x₁   

(34) Obligation:

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

PB_IN_GGAAA(T33, T34) → CONVERTE_IN_GGA(T33, T34)
PF_IN_GGAA(T53, T54) → CONVERTE_IN_GGA(T53, T54)
PC_IN_GGGAA(T160, T161, T162) → CONVERTA_IN_GGA(.(T160, T161), T162)
PD_IN_GGAA(T185, T186) → CONVERTE_IN_GGA(T185, T186)

R is empty.
Q is empty.
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 4 less nodes.

(36) TRUE