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

(0) Obligation:

Clauses:

intlist([], []).
intlist(.(X, XS), .(s(X), YS)) :- intlist(XS, YS).
int(0, 0, .(0, [])).
int(0, s(Y), .(0, XS)) :- int(s(0), s(Y), XS).
int(s(X), 0, []).
int(s(X), s(Y), XS) :- ','(int(X, Y, ZS), intlist(ZS, XS)).

Query: int(g,g,a)

(1) PrologToPiTRSViaGraphTransformerProof (SOUND transformation)

Transformed Prolog program to (Pi-)TRS.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
3 [label="A: int(T1, T2, T3)\n\nT1 is ground\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
5 [label="5: int(T1, T2, T3), SCOPE: 1, CLAUSE: 2 | int(T1, T2, T3), SCOPE: 1, CLAUSE: 3 | int(T1, T2, T3), SCOPE: 1, CLAUSE: 4 | int(T1, T2, T3), SCOPE: 1, CLAUSE: 5\n\nT1 is ground\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
11 [label="11: true | int(0, 0, T3), SCOPE: 1, CLAUSE: 3 | int(0, 0, T3), SCOPE: 1, CLAUSE: 4 | int(0, 0, T3), SCOPE: 1, CLAUSE: 5\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
14 [label="14: int(T1, T2, T3), SCOPE: 1, CLAUSE: 3 | int(T1, T2, T3), SCOPE: 1, CLAUSE: 4 | int(T1, T2, T3), SCOPE: 1, CLAUSE: 5\n\nT1 is ground\nT2 is ground\nint(T1, T2, T3) !=? int(0, 0, .(0, []))", fontsize=16, style=filled, fillcolor=lightyellow];
17 [label="17: int(0, 0, T3), SCOPE: 1, CLAUSE: 3 | int(0, 0, T3), SCOPE: 1, CLAUSE: 4 | int(0, 0, T3), SCOPE: 1, CLAUSE: 5\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
19 [label="19: int(0, 0, T3), SCOPE: 1, CLAUSE: 4 | int(0, 0, T3), SCOPE: 1, CLAUSE: 5\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
23 [label="23: int(0, 0, T3), SCOPE: 1, CLAUSE: 5\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
25 [label="25: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
27 [label="27: int(s(0), s(T6), T8) | int(0, s(T6), T3), SCOPE: 1, CLAUSE: 4 | int(0, s(T6), T3), SCOPE: 1, CLAUSE: 5\n\nT6 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
29 [label="29: int(T1, T2, T3), SCOPE: 1, CLAUSE: 4 | int(T1, T2, T3), SCOPE: 1, CLAUSE: 5\n\nT1 is ground\nT2 is ground\nX9 is free\nX10 is free\nint(T1, T2, T3) !=? int(0, 0, .(0, []))\nint(T1, T2, T3) !=? int(0, s(X9), .(0, X10))", fontsize=16, style=filled, fillcolor=lightyellow];
33 [label="33: int(s(0), s(T6), T8), SCOPE: 2, CLAUSE: 2 | int(s(0), s(T6), T8), SCOPE: 2, CLAUSE: 3 | int(s(0), s(T6), T8), SCOPE: 2, CLAUSE: 4 | int(s(0), s(T6), T8), SCOPE: 2, CLAUSE: 5 | ?_2 | int(0, s(T6), T3), SCOPE: 1, CLAUSE: 4 | int(0, s(T6), T3), SCOPE: 1, CLAUSE: 5\n\nT6 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
35 [label="35: int(s(0), s(T6), T8), SCOPE: 2, CLAUSE: 3 | int(s(0), s(T6), T8), SCOPE: 2, CLAUSE: 4 | int(s(0), s(T6), T8), SCOPE: 2, CLAUSE: 5 | ?_2 | int(0, s(T6), T3), SCOPE: 1, CLAUSE: 4 | int(0, s(T6), T3), SCOPE: 1, CLAUSE: 5\n\nT6 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
36 [label="36: int(s(0), s(T6), T8), SCOPE: 2, CLAUSE: 4 | int(s(0), s(T6), T8), SCOPE: 2, CLAUSE: 5 | ?_2 | int(0, s(T6), T3), SCOPE: 1, CLAUSE: 4 | int(0, s(T6), T3), SCOPE: 1, CLAUSE: 5\n\nT6 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
37 [label="37: int(s(0), s(T6), T8), SCOPE: 2, CLAUSE: 5 | ?_2 | int(0, s(T6), T3), SCOPE: 1, CLAUSE: 4 | int(0, s(T6), T3), SCOPE: 1, CLAUSE: 5\n\nT6 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
40 [label="40: int(s(0), s(T6), T8), SCOPE: 2, CLAUSE: 5\n\nT6 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
41 [label="41: ?_2 | int(0, s(T6), T3), SCOPE: 1, CLAUSE: 4 | int(0, s(T6), T3), SCOPE: 1, CLAUSE: 5\n\nT6 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
45 [label="B: ','(int(0, T19, X31), intlist(X31, T21))\n\nT19 is ground\nX31 is free", fontsize=16, style=filled, fillcolor=lightyellow];
50 [label="50: int(0, T19, X31)\n\nT19 is ground\nX31 is free", fontsize=16, style=filled, fillcolor=lightyellow];
51 [label="F: intlist(T22, T21)\n\nT22 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
63 [label="63: intlist(T22, T21), SCOPE: 3, CLAUSE: 0 | intlist(T22, T21), SCOPE: 3, CLAUSE: 1\n\nT22 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
66 [label="66: intlist(T22, T21), SCOPE: 3, CLAUSE: 0\n\nT22 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
67 [label="67: intlist(T22, T21), SCOPE: 3, CLAUSE: 1\n\nT22 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
70 [label="70: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
71 [label="71: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
73 [label="73: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
82 [label="82: intlist(T30, T32)\n\nT30 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
83 [label="83: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
90 [label="90: int(0, s(T6), T3), SCOPE: 1, CLAUSE: 4 | int(0, s(T6), T3), SCOPE: 1, CLAUSE: 5\n\nT6 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
91 [label="91: int(0, s(T6), T3), SCOPE: 1, CLAUSE: 5\n\nT6 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
92 [label="92: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
94 [label="94: true | int(s(T34), 0, T3), SCOPE: 1, CLAUSE: 5\n\nT34 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
103 [label="103: int(T1, T2, T3), SCOPE: 1, CLAUSE: 5\n\nT1 is ground\nT2 is ground\nX9 is free\nX10 is free\nX46 is free\nint(T1, T2, T3) !=? int(0, 0, .(0, []))\nint(T1, T2, T3) !=? int(0, s(X9), .(0, X10))\nint(T1, T2, T3) !=? int(s(X46), 0, [])", fontsize=16, style=filled, fillcolor=lightyellow];
104 [label="104: int(s(T34), 0, T3), SCOPE: 1, CLAUSE: 5\n\nT34 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
106 [label="106: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
115 [label="115: ','(int(T39, T40, X56), intlist(X56, T42))\n\nT39 is ground\nT40 is ground\nX56 is free", fontsize=16, style=filled, fillcolor=lightyellow];
118 [label="118: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
119 [label="119: ','(int(T39, T40, X56), intlist(X56, T42)), SCOPE: 4, CLAUSE: 2 | ','(int(T39, T40, X56), intlist(X56, T42)), SCOPE: 4, CLAUSE: 3 | ','(int(T39, T40, X56), intlist(X56, T42)), SCOPE: 4, CLAUSE: 4 | ','(int(T39, T40, X56), intlist(X56, T42)), SCOPE: 4, CLAUSE: 5\n\nT39 is ground\nT40 is ground\nX56 is free", fontsize=16, style=filled, fillcolor=lightyellow];
140 [label="140: ','(int(T39, T40, X56), intlist(X56, T42)), SCOPE: 4, CLAUSE: 2\n\nT39 is ground\nT40 is ground\nX56 is free", fontsize=16, style=filled, fillcolor=lightyellow];
141 [label="141: ','(int(T39, T40, X56), intlist(X56, T42)), SCOPE: 4, CLAUSE: 3 | ','(int(T39, T40, X56), intlist(X56, T42)), SCOPE: 4, CLAUSE: 4 | ','(int(T39, T40, X56), intlist(X56, T42)), SCOPE: 4, CLAUSE: 5\n\nT39 is ground\nT40 is ground\nX56 is free", fontsize=16, style=filled, fillcolor=lightyellow];
142 [label="142: intlist(.(0, []), T42)\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
144 [label="144: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
146 [label="146: intlist(.(0, []), T42), SCOPE: 5, CLAUSE: 0 | intlist(.(0, []), T42), SCOPE: 5, CLAUSE: 1\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
147 [label="147: intlist(.(0, []), T42), SCOPE: 5, CLAUSE: 1\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
148 [label="C: intlist([], T46)\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
149 [label="149: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
150 [label="150: intlist([], T46), SCOPE: 6, CLAUSE: 0 | intlist([], T46), SCOPE: 6, CLAUSE: 1\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
151 [label="151: intlist([], T46), SCOPE: 6, CLAUSE: 0\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
152 [label="152: intlist([], T46), SCOPE: 6, CLAUSE: 1\n\n", 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];
156 [label="156: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
157 [label="157: ','(int(T39, T40, X56), intlist(X56, T42)), SCOPE: 4, CLAUSE: 3\n\nT39 is ground\nT40 is ground\nX56 is free", fontsize=16, style=filled, fillcolor=lightyellow];
158 [label="158: ','(int(T39, T40, X56), intlist(X56, T42)), SCOPE: 4, CLAUSE: 4 | ','(int(T39, T40, X56), intlist(X56, T42)), SCOPE: 4, CLAUSE: 5\n\nT39 is ground\nT40 is ground\nX56 is free", fontsize=16, style=filled, fillcolor=lightyellow];
159 [label="D: ','(int(s(0), s(T51), X83), intlist(.(0, X83), T42))\n\nT51 is ground\nX83 is free", fontsize=16, style=filled, fillcolor=lightyellow];
160 [label="160: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
161 [label="161: int(s(0), s(T51), X83)\n\nT51 is ground\nX83 is free", fontsize=16, style=filled, fillcolor=lightyellow];
162 [label="162: intlist(.(0, T52), T42)\n\nT52 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
163 [label="163: ','(int(T39, T40, X56), intlist(X56, T42)), SCOPE: 4, CLAUSE: 4\n\nT39 is ground\nT40 is ground\nX56 is free", fontsize=16, style=filled, fillcolor=lightyellow];
164 [label="164: ','(int(T39, T40, X56), intlist(X56, T42)), SCOPE: 4, CLAUSE: 5\n\nT39 is ground\nT40 is ground\nX56 is free", fontsize=16, style=filled, fillcolor=lightyellow];
165 [label="165: intlist([], T42)\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
166 [label="166: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
167 [label="E: ','(','(int(T62, T63, X101), intlist(X101, X102)), intlist(X102, T42))\n\nT62 is ground\nT63 is ground\nX102 is free\nX101 is free", fontsize=16, style=filled, fillcolor=lightyellow];
168 [label="168: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
169 [label="169: int(T62, T63, X101)\n\nT62 is ground\nT63 is ground\nX101 is free", fontsize=16, style=filled, fillcolor=lightyellow];
170 [label="H: ','(intlist(T64, X102), intlist(X102, T42))\n\nT64 is ground\nX102 is free", fontsize=16, style=filled, fillcolor=lightyellow];
171 [label="G: intlist(T64, X102)\n\nT64 is ground\nX102 is free", fontsize=16, style=filled, fillcolor=lightyellow];
172 [label="172: intlist(T65, T42)\n\nT65 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
173 [label="173: intlist(T64, X102), SCOPE: 7, CLAUSE: 0 | intlist(T64, X102), SCOPE: 7, CLAUSE: 1\n\nT64 is ground\nX102 is free", fontsize=16, style=filled, fillcolor=lightyellow];
174 [label="174: intlist(T64, X102), SCOPE: 7, CLAUSE: 0\n\nT64 is ground\nX102 is free", fontsize=16, style=filled, fillcolor=lightyellow];
175 [label="175: intlist(T64, X102), SCOPE: 7, CLAUSE: 1\n\nT64 is ground\nX102 is free", fontsize=16, style=filled, fillcolor=lightyellow];
176 [label="176: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
177 [label="177: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
178 [label="178: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
179 [label="179: intlist(T71, X114)\n\nT71 is ground\nX114 is free", fontsize=16, style=filled, fillcolor=lightyellow];
180 [label="180: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
181 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
3 -> 181 [arrowhead = none ];
181 -> 5;

182 [label="EVAL with clause\nint(0, 0, .(0, [])).\nand substitutionT1 -> 0,\nT2 -> 0,\nT3 -> .(0, [])", fontsize=14, style = filled, fillcolor = lightblue];
5 -> 182 [arrowhead = none ];
182 -> 11;

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

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

185 [label="EVAL with clause\nint(0, s(X9), .(0, X10)) :- int(s(0), s(X9), X10).\nand substitutionT1 -> 0,\nX9 -> T6,\nT2 -> s(T6),\nX10 -> T8,\nT3 -> .(0, T8),\nT7 -> T8", fontsize=14, style = filled, fillcolor = lightblue];
14 -> 185 [arrowhead = none ];
185 -> 27;

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

187 [label="BACKTRACK\nfor clause: int(0, s(Y), .(0, XS)) :- int(s(0), s(Y), XS)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
17 -> 187 [arrowhead = none ];
187 -> 19;

188 [label="BACKTRACK\nfor clause: int(s(X), 0, [])because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
19 -> 188 [arrowhead = none ];
188 -> 23;

189 [label="BACKTRACK\nfor clause: int(s(X), s(Y), XS) :- ','(int(X, Y, ZS), intlist(ZS, XS))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
23 -> 189 [arrowhead = none ];
189 -> 25;

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

191 [label="EVAL with clause\nint(s(X46), 0, []).\nand substitutionX46 -> T34,\nT1 -> s(T34),\nT2 -> 0,\nT3 -> []", fontsize=14, style = filled, fillcolor = lightblue];
29 -> 191 [arrowhead = none ];
191 -> 94;

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

193 [label="BACKTRACK\nfor clause: int(0, 0, .(0, []))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
33 -> 193 [arrowhead = none ];
193 -> 35;

194 [label="BACKTRACK\nfor clause: int(0, s(Y), .(0, XS)) :- int(s(0), s(Y), XS)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
35 -> 194 [arrowhead = none ];
194 -> 36;

195 [label="BACKTRACK\nfor clause: int(s(X), 0, [])because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
36 -> 195 [arrowhead = none ];
195 -> 37;

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

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

198 [label="ONLY EVAL with clause\nint(s(X28), s(X29), X30) :- ','(int(X28, X29, X31), intlist(X31, X30)).\nand substitutionX28 -> 0,\nT6 -> T19,\nX29 -> T19,\nT8 -> T21,\nX30 -> T21,\nT20 -> T21", fontsize=14, style = filled, fillcolor = lightblue];
40 -> 198 [arrowhead = none ];
198 -> 45;

199 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
41 -> 199 [arrowhead = none ];
199 -> 90;

200 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
45 -> 200 [arrowhead = none ];
200 -> 50;

201 [label="SPLIT 2\nnew knowledge:\nT19 is ground\nT22 is ground\nreplacements:X31 -> T22", fontsize=14, style = filled, fillcolor = violet];
45 -> 201 [arrowhead = none ];
201 -> 51;

202 [label="INSTANCE with matching:\nT1 -> 0\nT2 -> T19\nT3 -> X31", fontsize=14, style = filled, fillcolor = lightgrey];
50 -> 202 [arrowhead = none , style=dashed];
202 -> 3[style=dashed];

203 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
51 -> 203 [arrowhead = none ];
203 -> 63;

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

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

206 [label="EVAL with clause\nintlist([], []).\nand substitutionT22 -> [],\nT21 -> []", fontsize=14, style = filled, fillcolor = lightblue];
66 -> 206 [arrowhead = none ];
206 -> 70;

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

208 [label="EVAL with clause\nintlist(.(X38, X39), .(s(X38), X40)) :- intlist(X39, X40).\nand substitutionX38 -> T29,\nX39 -> T30,\nT22 -> .(T29, T30),\nX40 -> T32,\nT21 -> .(s(T29), T32),\nT31 -> T32", fontsize=14, style = filled, fillcolor = lightblue];
67 -> 208 [arrowhead = none ];
208 -> 82;

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

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

211 [label="INSTANCE with matching:\nT22 -> T30\nT21 -> T32", fontsize=14, style = filled, fillcolor = lightgrey];
82 -> 211 [arrowhead = none , style=dashed];
211 -> 51[style=dashed];

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

213 [label="BACKTRACK\nfor clause: int(s(X), s(Y), XS) :- ','(int(X, Y, ZS), intlist(ZS, XS))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
91 -> 213 [arrowhead = none ];
213 -> 92;

214 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
94 -> 214 [arrowhead = none ];
214 -> 104;

215 [label="EVAL with clause\nint(s(X53), s(X54), X55) :- ','(int(X53, X54, X56), intlist(X56, X55)).\nand substitutionX53 -> T39,\nT1 -> s(T39),\nX54 -> T40,\nT2 -> s(T40),\nT3 -> T42,\nX55 -> T42,\nT41 -> T42", fontsize=14, style = filled, fillcolor = lightblue];
103 -> 215 [arrowhead = none ];
215 -> 115;

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

217 [label="BACKTRACK\nfor clause: int(s(X), s(Y), XS) :- ','(int(X, Y, ZS), intlist(ZS, XS))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
104 -> 217 [arrowhead = none ];
217 -> 106;

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

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

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

221 [label="EVAL with clause\nint(0, 0, .(0, [])).\nand substitutionT39 -> 0,\nT40 -> 0,\nX56 -> .(0, [])", fontsize=14, style = filled, fillcolor = lightblue];
140 -> 221 [arrowhead = none ];
221 -> 142;

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

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

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

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

226 [label="BACKTRACK\nfor clause: intlist([], [])because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
146 -> 226 [arrowhead = none ];
226 -> 147;

227 [label="EVAL with clause\nintlist(.(X63, X64), .(s(X63), X65)) :- intlist(X64, X65).\nand substitutionX63 -> 0,\nX64 -> [],\nX65 -> T46,\nT42 -> .(s(0), T46),\nT45 -> T46", fontsize=14, style = filled, fillcolor = lightblue];
147 -> 227 [arrowhead = none ];
227 -> 148;

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

229 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
148 -> 229 [arrowhead = none ];
229 -> 150;

230 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
150 -> 230 [arrowhead = none ];
230 -> 151;

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

232 [label="EVAL with clause\nintlist([], []).\nand substitutionT46 -> []", fontsize=14, style = filled, fillcolor = lightblue];
151 -> 232 [arrowhead = none ];
232 -> 153;

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

234 [label="BACKTRACK\nfor clause: intlist(.(X, XS), .(s(X), YS)) :- intlist(XS, YS)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
152 -> 234 [arrowhead = none ];
234 -> 156;

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

236 [label="EVAL with clause\nint(0, s(X81), .(0, X82)) :- int(s(0), s(X81), X82).\nand substitutionT39 -> 0,\nX81 -> T51,\nT40 -> s(T51),\nX82 -> X83,\nX56 -> .(0, X83)", fontsize=14, style = filled, fillcolor = lightblue];
157 -> 236 [arrowhead = none ];
236 -> 159;

237 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
157 -> 237 [arrowhead = none ];
237 -> 160;

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

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

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

241 [label="SPLIT 2\nnew knowledge:\nT51 is ground\nT52 is ground\nreplacements:X83 -> T52", fontsize=14, style = filled, fillcolor = violet];
159 -> 241 [arrowhead = none ];
241 -> 162;

242 [label="INSTANCE with matching:\nT1 -> s(0)\nT2 -> s(T51)\nT3 -> X83", fontsize=14, style = filled, fillcolor = lightgrey];
161 -> 242 [arrowhead = none , style=dashed];
242 -> 3[style=dashed];

243 [label="INSTANCE with matching:\nT22 -> .(0, T52)\nT21 -> T42", fontsize=14, style = filled, fillcolor = lightgrey];
162 -> 243 [arrowhead = none , style=dashed];
243 -> 51[style=dashed];

244 [label="EVAL with clause\nint(s(X88), 0, []).\nand substitutionX88 -> T57,\nT39 -> s(T57),\nT40 -> 0,\nX56 -> []", fontsize=14, style = filled, fillcolor = lightblue];
163 -> 244 [arrowhead = none ];
244 -> 165;

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

246 [label="EVAL with clause\nint(s(X98), s(X99), X100) :- ','(int(X98, X99, X101), intlist(X101, X100)).\nand substitutionX98 -> T62,\nT39 -> s(T62),\nX99 -> T63,\nT40 -> s(T63),\nX56 -> X102,\nX100 -> X102", fontsize=14, style = filled, fillcolor = lightblue];
164 -> 246 [arrowhead = none ];
246 -> 167;

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

248 [label="INSTANCE with matching:\nT46 -> T42", fontsize=14, style = filled, fillcolor = lightgrey];
165 -> 248 [arrowhead = none , style=dashed];
248 -> 148[style=dashed];

249 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
167 -> 249 [arrowhead = none ];
249 -> 169;

250 [label="SPLIT 2\nnew knowledge:\nT62 is ground\nT63 is ground\nT64 is ground\nreplacements:X101 -> T64", fontsize=14, style = filled, fillcolor = violet];
167 -> 250 [arrowhead = none ];
250 -> 170;

251 [label="INSTANCE with matching:\nT1 -> T62\nT2 -> T63\nT3 -> X101", fontsize=14, style = filled, fillcolor = lightgrey];
169 -> 251 [arrowhead = none , style=dashed];
251 -> 3[style=dashed];

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

253 [label="SPLIT 2\nnew knowledge:\nT64 is ground\nT65 is ground\nreplacements:X102 -> T65", fontsize=14, style = filled, fillcolor = violet];
170 -> 253 [arrowhead = none ];
253 -> 172;

254 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
171 -> 254 [arrowhead = none ];
254 -> 173;

255 [label="INSTANCE with matching:\nT22 -> T65\nT21 -> T42", fontsize=14, style = filled, fillcolor = lightgrey];
172 -> 255 [arrowhead = none , style=dashed];
255 -> 51[style=dashed];

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

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

258 [label="EVAL with clause\nintlist([], []).\nand substitutionT64 -> [],\nX102 -> []", fontsize=14, style = filled, fillcolor = lightblue];
174 -> 258 [arrowhead = none ];
258 -> 176;

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

260 [label="EVAL with clause\nintlist(.(X111, X112), .(s(X111), X113)) :- intlist(X112, X113).\nand substitutionX111 -> T70,\nX112 -> T71,\nT64 -> .(T70, T71),\nX113 -> X114,\nX102 -> .(s(T70), X114)", fontsize=14, style = filled, fillcolor = lightblue];
175 -> 260 [arrowhead = none ];
260 -> 179;

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

262 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
176 -> 262 [arrowhead = none ];
262 -> 178;

263 [label="INSTANCE with matching:\nT64 -> T71\nX102 -> X114", fontsize=14, style = filled, fillcolor = lightgrey];
179 -> 263 [arrowhead = none , style=dashed];
263 -> 171[style=dashed];

}

(2) Obligation:

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

intA_in_gga(0, 0, .(0, [])) → intA_out_gga(0, 0, .(0, []))
intA_in_gga(0, s(T19), .(0, T21)) → U1_gga(T19, T21, pB_in_gaa(T19, X31, T21))
pB_in_gaa(T19, T22, T21) → U8_gaa(T19, T22, T21, intA_in_gga(0, T19, T22))
intA_in_gga(s(T34), 0, []) → intA_out_gga(s(T34), 0, [])
intA_in_gga(s(0), s(0), .(s(0), T46)) → U2_gga(T46, intlistC_in_a(T46))
intlistC_in_a([]) → intlistC_out_a([])
U2_gga(T46, intlistC_out_a(T46)) → intA_out_gga(s(0), s(0), .(s(0), T46))
intA_in_gga(s(0), s(s(T51)), T42) → U3_gga(T51, T42, pD_in_gaa(T51, X83, T42))
pD_in_gaa(T51, T52, T42) → U10_gaa(T51, T52, T42, intA_in_gga(s(0), s(T51), T52))
intA_in_gga(s(s(T57)), s(0), T42) → U4_gga(T57, T42, intlistC_in_a(T42))
U4_gga(T57, T42, intlistC_out_a(T42)) → intA_out_gga(s(s(T57)), s(0), T42)
intA_in_gga(s(s(T62)), s(s(T63)), T42) → U5_gga(T62, T63, T42, pE_in_ggaaa(T62, T63, X101, X102, T42))
pE_in_ggaaa(T62, T63, T64, X102, T42) → U12_ggaaa(T62, T63, T64, X102, T42, intA_in_gga(T62, T63, T64))
U12_ggaaa(T62, T63, T64, X102, T42, intA_out_gga(T62, T63, T64)) → U13_ggaaa(T62, T63, T64, X102, T42, pH_in_gaa(T64, X102, T42))
pH_in_gaa(T64, T65, T42) → U14_gaa(T64, T65, T42, intlistG_in_ga(T64, T65))
intlistG_in_ga([], []) → intlistG_out_ga([], [])
intlistG_in_ga(.(T70, T71), .(s(T70), X114)) → U7_ga(T70, T71, X114, intlistG_in_ga(T71, X114))
U7_ga(T70, T71, X114, intlistG_out_ga(T71, X114)) → intlistG_out_ga(.(T70, T71), .(s(T70), X114))
U14_gaa(T64, T65, T42, intlistG_out_ga(T64, T65)) → U15_gaa(T64, T65, T42, intlistF_in_ga(T65, T42))
intlistF_in_ga([], []) → intlistF_out_ga([], [])
intlistF_in_ga(.(T29, T30), .(s(T29), T32)) → U6_ga(T29, T30, T32, intlistF_in_ga(T30, T32))
U6_ga(T29, T30, T32, intlistF_out_ga(T30, T32)) → intlistF_out_ga(.(T29, T30), .(s(T29), T32))
U15_gaa(T64, T65, T42, intlistF_out_ga(T65, T42)) → pH_out_gaa(T64, T65, T42)
U13_ggaaa(T62, T63, T64, X102, T42, pH_out_gaa(T64, X102, T42)) → pE_out_ggaaa(T62, T63, T64, X102, T42)
U5_gga(T62, T63, T42, pE_out_ggaaa(T62, T63, X101, X102, T42)) → intA_out_gga(s(s(T62)), s(s(T63)), T42)
U10_gaa(T51, T52, T42, intA_out_gga(s(0), s(T51), T52)) → U11_gaa(T51, T52, T42, intlistF_in_ga(.(0, T52), T42))
U11_gaa(T51, T52, T42, intlistF_out_ga(.(0, T52), T42)) → pD_out_gaa(T51, T52, T42)
U3_gga(T51, T42, pD_out_gaa(T51, X83, T42)) → intA_out_gga(s(0), s(s(T51)), T42)
U8_gaa(T19, T22, T21, intA_out_gga(0, T19, T22)) → U9_gaa(T19, T22, T21, intlistF_in_ga(T22, T21))
U9_gaa(T19, T22, T21, intlistF_out_ga(T22, T21)) → pB_out_gaa(T19, T22, T21)
U1_gga(T19, T21, pB_out_gaa(T19, X31, T21)) → intA_out_gga(0, s(T19), .(0, T21))

The argument filtering Pi contains the following mapping:
intA_in_gga(x1, x2, x3)  =  intA_in_gga(x1, x2)
0  =  0
intA_out_gga(x1, x2, x3)  =  intA_out_gga(x1, x2, x3)
s(x1)  =  s(x1)
U1_gga(x1, x2, x3)  =  U1_gga(x1, x3)
pB_in_gaa(x1, x2, x3)  =  pB_in_gaa(x1)
U8_gaa(x1, x2, x3, x4)  =  U8_gaa(x1, x4)
U2_gga(x1, x2)  =  U2_gga(x2)
intlistC_in_a(x1)  =  intlistC_in_a
intlistC_out_a(x1)  =  intlistC_out_a(x1)
U3_gga(x1, x2, x3)  =  U3_gga(x1, x3)
pD_in_gaa(x1, x2, x3)  =  pD_in_gaa(x1)
U10_gaa(x1, x2, x3, x4)  =  U10_gaa(x1, x4)
U4_gga(x1, x2, x3)  =  U4_gga(x1, x3)
U5_gga(x1, x2, x3, x4)  =  U5_gga(x1, x2, x4)
pE_in_ggaaa(x1, x2, x3, x4, x5)  =  pE_in_ggaaa(x1, x2)
U12_ggaaa(x1, x2, x3, x4, x5, x6)  =  U12_ggaaa(x1, x2, x6)
U13_ggaaa(x1, x2, x3, x4, x5, x6)  =  U13_ggaaa(x1, x2, x3, x6)
pH_in_gaa(x1, x2, x3)  =  pH_in_gaa(x1)
U14_gaa(x1, x2, x3, x4)  =  U14_gaa(x1, x4)
intlistG_in_ga(x1, x2)  =  intlistG_in_ga(x1)
[]  =  []
intlistG_out_ga(x1, x2)  =  intlistG_out_ga(x1, x2)
.(x1, x2)  =  .(x1, x2)
U7_ga(x1, x2, x3, x4)  =  U7_ga(x1, x2, x4)
U15_gaa(x1, x2, x3, x4)  =  U15_gaa(x1, x2, x4)
intlistF_in_ga(x1, x2)  =  intlistF_in_ga(x1)
intlistF_out_ga(x1, x2)  =  intlistF_out_ga(x1, x2)
U6_ga(x1, x2, x3, x4)  =  U6_ga(x1, x2, x4)
pH_out_gaa(x1, x2, x3)  =  pH_out_gaa(x1, x2, x3)
pE_out_ggaaa(x1, x2, x3, x4, x5)  =  pE_out_ggaaa(x1, x2, x3, x4, x5)
U11_gaa(x1, x2, x3, x4)  =  U11_gaa(x1, x2, x4)
pD_out_gaa(x1, x2, x3)  =  pD_out_gaa(x1, x2, x3)
U9_gaa(x1, x2, x3, x4)  =  U9_gaa(x1, x2, x4)
pB_out_gaa(x1, x2, x3)  =  pB_out_gaa(x1, x2, x3)

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

INTA_IN_GGA(0, s(T19), .(0, T21)) → U1_GGA(T19, T21, pB_in_gaa(T19, X31, T21))
INTA_IN_GGA(0, s(T19), .(0, T21)) → PB_IN_GAA(T19, X31, T21)
PB_IN_GAA(T19, T22, T21) → U8_GAA(T19, T22, T21, intA_in_gga(0, T19, T22))
PB_IN_GAA(T19, T22, T21) → INTA_IN_GGA(0, T19, T22)
INTA_IN_GGA(s(0), s(0), .(s(0), T46)) → U2_GGA(T46, intlistC_in_a(T46))
INTA_IN_GGA(s(0), s(0), .(s(0), T46)) → INTLISTC_IN_A(T46)
INTA_IN_GGA(s(0), s(s(T51)), T42) → U3_GGA(T51, T42, pD_in_gaa(T51, X83, T42))
INTA_IN_GGA(s(0), s(s(T51)), T42) → PD_IN_GAA(T51, X83, T42)
PD_IN_GAA(T51, T52, T42) → U10_GAA(T51, T52, T42, intA_in_gga(s(0), s(T51), T52))
PD_IN_GAA(T51, T52, T42) → INTA_IN_GGA(s(0), s(T51), T52)
INTA_IN_GGA(s(s(T57)), s(0), T42) → U4_GGA(T57, T42, intlistC_in_a(T42))
INTA_IN_GGA(s(s(T57)), s(0), T42) → INTLISTC_IN_A(T42)
INTA_IN_GGA(s(s(T62)), s(s(T63)), T42) → U5_GGA(T62, T63, T42, pE_in_ggaaa(T62, T63, X101, X102, T42))
INTA_IN_GGA(s(s(T62)), s(s(T63)), T42) → PE_IN_GGAAA(T62, T63, X101, X102, T42)
PE_IN_GGAAA(T62, T63, T64, X102, T42) → U12_GGAAA(T62, T63, T64, X102, T42, intA_in_gga(T62, T63, T64))
PE_IN_GGAAA(T62, T63, T64, X102, T42) → INTA_IN_GGA(T62, T63, T64)
U12_GGAAA(T62, T63, T64, X102, T42, intA_out_gga(T62, T63, T64)) → U13_GGAAA(T62, T63, T64, X102, T42, pH_in_gaa(T64, X102, T42))
U12_GGAAA(T62, T63, T64, X102, T42, intA_out_gga(T62, T63, T64)) → PH_IN_GAA(T64, X102, T42)
PH_IN_GAA(T64, T65, T42) → U14_GAA(T64, T65, T42, intlistG_in_ga(T64, T65))
PH_IN_GAA(T64, T65, T42) → INTLISTG_IN_GA(T64, T65)
INTLISTG_IN_GA(.(T70, T71), .(s(T70), X114)) → U7_GA(T70, T71, X114, intlistG_in_ga(T71, X114))
INTLISTG_IN_GA(.(T70, T71), .(s(T70), X114)) → INTLISTG_IN_GA(T71, X114)
U14_GAA(T64, T65, T42, intlistG_out_ga(T64, T65)) → U15_GAA(T64, T65, T42, intlistF_in_ga(T65, T42))
U14_GAA(T64, T65, T42, intlistG_out_ga(T64, T65)) → INTLISTF_IN_GA(T65, T42)
INTLISTF_IN_GA(.(T29, T30), .(s(T29), T32)) → U6_GA(T29, T30, T32, intlistF_in_ga(T30, T32))
INTLISTF_IN_GA(.(T29, T30), .(s(T29), T32)) → INTLISTF_IN_GA(T30, T32)
U10_GAA(T51, T52, T42, intA_out_gga(s(0), s(T51), T52)) → U11_GAA(T51, T52, T42, intlistF_in_ga(.(0, T52), T42))
U10_GAA(T51, T52, T42, intA_out_gga(s(0), s(T51), T52)) → INTLISTF_IN_GA(.(0, T52), T42)
U8_GAA(T19, T22, T21, intA_out_gga(0, T19, T22)) → U9_GAA(T19, T22, T21, intlistF_in_ga(T22, T21))
U8_GAA(T19, T22, T21, intA_out_gga(0, T19, T22)) → INTLISTF_IN_GA(T22, T21)

The TRS R consists of the following rules:

intA_in_gga(0, 0, .(0, [])) → intA_out_gga(0, 0, .(0, []))
intA_in_gga(0, s(T19), .(0, T21)) → U1_gga(T19, T21, pB_in_gaa(T19, X31, T21))
pB_in_gaa(T19, T22, T21) → U8_gaa(T19, T22, T21, intA_in_gga(0, T19, T22))
intA_in_gga(s(T34), 0, []) → intA_out_gga(s(T34), 0, [])
intA_in_gga(s(0), s(0), .(s(0), T46)) → U2_gga(T46, intlistC_in_a(T46))
intlistC_in_a([]) → intlistC_out_a([])
U2_gga(T46, intlistC_out_a(T46)) → intA_out_gga(s(0), s(0), .(s(0), T46))
intA_in_gga(s(0), s(s(T51)), T42) → U3_gga(T51, T42, pD_in_gaa(T51, X83, T42))
pD_in_gaa(T51, T52, T42) → U10_gaa(T51, T52, T42, intA_in_gga(s(0), s(T51), T52))
intA_in_gga(s(s(T57)), s(0), T42) → U4_gga(T57, T42, intlistC_in_a(T42))
U4_gga(T57, T42, intlistC_out_a(T42)) → intA_out_gga(s(s(T57)), s(0), T42)
intA_in_gga(s(s(T62)), s(s(T63)), T42) → U5_gga(T62, T63, T42, pE_in_ggaaa(T62, T63, X101, X102, T42))
pE_in_ggaaa(T62, T63, T64, X102, T42) → U12_ggaaa(T62, T63, T64, X102, T42, intA_in_gga(T62, T63, T64))
U12_ggaaa(T62, T63, T64, X102, T42, intA_out_gga(T62, T63, T64)) → U13_ggaaa(T62, T63, T64, X102, T42, pH_in_gaa(T64, X102, T42))
pH_in_gaa(T64, T65, T42) → U14_gaa(T64, T65, T42, intlistG_in_ga(T64, T65))
intlistG_in_ga([], []) → intlistG_out_ga([], [])
intlistG_in_ga(.(T70, T71), .(s(T70), X114)) → U7_ga(T70, T71, X114, intlistG_in_ga(T71, X114))
U7_ga(T70, T71, X114, intlistG_out_ga(T71, X114)) → intlistG_out_ga(.(T70, T71), .(s(T70), X114))
U14_gaa(T64, T65, T42, intlistG_out_ga(T64, T65)) → U15_gaa(T64, T65, T42, intlistF_in_ga(T65, T42))
intlistF_in_ga([], []) → intlistF_out_ga([], [])
intlistF_in_ga(.(T29, T30), .(s(T29), T32)) → U6_ga(T29, T30, T32, intlistF_in_ga(T30, T32))
U6_ga(T29, T30, T32, intlistF_out_ga(T30, T32)) → intlistF_out_ga(.(T29, T30), .(s(T29), T32))
U15_gaa(T64, T65, T42, intlistF_out_ga(T65, T42)) → pH_out_gaa(T64, T65, T42)
U13_ggaaa(T62, T63, T64, X102, T42, pH_out_gaa(T64, X102, T42)) → pE_out_ggaaa(T62, T63, T64, X102, T42)
U5_gga(T62, T63, T42, pE_out_ggaaa(T62, T63, X101, X102, T42)) → intA_out_gga(s(s(T62)), s(s(T63)), T42)
U10_gaa(T51, T52, T42, intA_out_gga(s(0), s(T51), T52)) → U11_gaa(T51, T52, T42, intlistF_in_ga(.(0, T52), T42))
U11_gaa(T51, T52, T42, intlistF_out_ga(.(0, T52), T42)) → pD_out_gaa(T51, T52, T42)
U3_gga(T51, T42, pD_out_gaa(T51, X83, T42)) → intA_out_gga(s(0), s(s(T51)), T42)
U8_gaa(T19, T22, T21, intA_out_gga(0, T19, T22)) → U9_gaa(T19, T22, T21, intlistF_in_ga(T22, T21))
U9_gaa(T19, T22, T21, intlistF_out_ga(T22, T21)) → pB_out_gaa(T19, T22, T21)
U1_gga(T19, T21, pB_out_gaa(T19, X31, T21)) → intA_out_gga(0, s(T19), .(0, T21))

The argument filtering Pi contains the following mapping:
intA_in_gga(x1, x2, x3)  =  intA_in_gga(x1, x2)
0  =  0
intA_out_gga(x1, x2, x3)  =  intA_out_gga(x1, x2, x3)
s(x1)  =  s(x1)
U1_gga(x1, x2, x3)  =  U1_gga(x1, x3)
pB_in_gaa(x1, x2, x3)  =  pB_in_gaa(x1)
U8_gaa(x1, x2, x3, x4)  =  U8_gaa(x1, x4)
U2_gga(x1, x2)  =  U2_gga(x2)
intlistC_in_a(x1)  =  intlistC_in_a
intlistC_out_a(x1)  =  intlistC_out_a(x1)
U3_gga(x1, x2, x3)  =  U3_gga(x1, x3)
pD_in_gaa(x1, x2, x3)  =  pD_in_gaa(x1)
U10_gaa(x1, x2, x3, x4)  =  U10_gaa(x1, x4)
U4_gga(x1, x2, x3)  =  U4_gga(x1, x3)
U5_gga(x1, x2, x3, x4)  =  U5_gga(x1, x2, x4)
pE_in_ggaaa(x1, x2, x3, x4, x5)  =  pE_in_ggaaa(x1, x2)
U12_ggaaa(x1, x2, x3, x4, x5, x6)  =  U12_ggaaa(x1, x2, x6)
U13_ggaaa(x1, x2, x3, x4, x5, x6)  =  U13_ggaaa(x1, x2, x3, x6)
pH_in_gaa(x1, x2, x3)  =  pH_in_gaa(x1)
U14_gaa(x1, x2, x3, x4)  =  U14_gaa(x1, x4)
intlistG_in_ga(x1, x2)  =  intlistG_in_ga(x1)
[]  =  []
intlistG_out_ga(x1, x2)  =  intlistG_out_ga(x1, x2)
.(x1, x2)  =  .(x1, x2)
U7_ga(x1, x2, x3, x4)  =  U7_ga(x1, x2, x4)
U15_gaa(x1, x2, x3, x4)  =  U15_gaa(x1, x2, x4)
intlistF_in_ga(x1, x2)  =  intlistF_in_ga(x1)
intlistF_out_ga(x1, x2)  =  intlistF_out_ga(x1, x2)
U6_ga(x1, x2, x3, x4)  =  U6_ga(x1, x2, x4)
pH_out_gaa(x1, x2, x3)  =  pH_out_gaa(x1, x2, x3)
pE_out_ggaaa(x1, x2, x3, x4, x5)  =  pE_out_ggaaa(x1, x2, x3, x4, x5)
U11_gaa(x1, x2, x3, x4)  =  U11_gaa(x1, x2, x4)
pD_out_gaa(x1, x2, x3)  =  pD_out_gaa(x1, x2, x3)
U9_gaa(x1, x2, x3, x4)  =  U9_gaa(x1, x2, x4)
pB_out_gaa(x1, x2, x3)  =  pB_out_gaa(x1, x2, x3)
INTA_IN_GGA(x1, x2, x3)  =  INTA_IN_GGA(x1, x2)
U1_GGA(x1, x2, x3)  =  U1_GGA(x1, x3)
PB_IN_GAA(x1, x2, x3)  =  PB_IN_GAA(x1)
U8_GAA(x1, x2, x3, x4)  =  U8_GAA(x1, x4)
U2_GGA(x1, x2)  =  U2_GGA(x2)
INTLISTC_IN_A(x1)  =  INTLISTC_IN_A
U3_GGA(x1, x2, x3)  =  U3_GGA(x1, x3)
PD_IN_GAA(x1, x2, x3)  =  PD_IN_GAA(x1)
U10_GAA(x1, x2, x3, x4)  =  U10_GAA(x1, x4)
U4_GGA(x1, x2, x3)  =  U4_GGA(x1, x3)
U5_GGA(x1, x2, x3, x4)  =  U5_GGA(x1, x2, x4)
PE_IN_GGAAA(x1, x2, x3, x4, x5)  =  PE_IN_GGAAA(x1, x2)
U12_GGAAA(x1, x2, x3, x4, x5, x6)  =  U12_GGAAA(x1, x2, x6)
U13_GGAAA(x1, x2, x3, x4, x5, x6)  =  U13_GGAAA(x1, x2, x3, x6)
PH_IN_GAA(x1, x2, x3)  =  PH_IN_GAA(x1)
U14_GAA(x1, x2, x3, x4)  =  U14_GAA(x1, x4)
INTLISTG_IN_GA(x1, x2)  =  INTLISTG_IN_GA(x1)
U7_GA(x1, x2, x3, x4)  =  U7_GA(x1, x2, x4)
U15_GAA(x1, x2, x3, x4)  =  U15_GAA(x1, x2, x4)
INTLISTF_IN_GA(x1, x2)  =  INTLISTF_IN_GA(x1)
U6_GA(x1, x2, x3, x4)  =  U6_GA(x1, x2, x4)
U11_GAA(x1, x2, x3, x4)  =  U11_GAA(x1, x2, x4)
U9_GAA(x1, x2, x3, x4)  =  U9_GAA(x1, x2, x4)

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

(4) Obligation:

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

INTA_IN_GGA(0, s(T19), .(0, T21)) → U1_GGA(T19, T21, pB_in_gaa(T19, X31, T21))
INTA_IN_GGA(0, s(T19), .(0, T21)) → PB_IN_GAA(T19, X31, T21)
PB_IN_GAA(T19, T22, T21) → U8_GAA(T19, T22, T21, intA_in_gga(0, T19, T22))
PB_IN_GAA(T19, T22, T21) → INTA_IN_GGA(0, T19, T22)
INTA_IN_GGA(s(0), s(0), .(s(0), T46)) → U2_GGA(T46, intlistC_in_a(T46))
INTA_IN_GGA(s(0), s(0), .(s(0), T46)) → INTLISTC_IN_A(T46)
INTA_IN_GGA(s(0), s(s(T51)), T42) → U3_GGA(T51, T42, pD_in_gaa(T51, X83, T42))
INTA_IN_GGA(s(0), s(s(T51)), T42) → PD_IN_GAA(T51, X83, T42)
PD_IN_GAA(T51, T52, T42) → U10_GAA(T51, T52, T42, intA_in_gga(s(0), s(T51), T52))
PD_IN_GAA(T51, T52, T42) → INTA_IN_GGA(s(0), s(T51), T52)
INTA_IN_GGA(s(s(T57)), s(0), T42) → U4_GGA(T57, T42, intlistC_in_a(T42))
INTA_IN_GGA(s(s(T57)), s(0), T42) → INTLISTC_IN_A(T42)
INTA_IN_GGA(s(s(T62)), s(s(T63)), T42) → U5_GGA(T62, T63, T42, pE_in_ggaaa(T62, T63, X101, X102, T42))
INTA_IN_GGA(s(s(T62)), s(s(T63)), T42) → PE_IN_GGAAA(T62, T63, X101, X102, T42)
PE_IN_GGAAA(T62, T63, T64, X102, T42) → U12_GGAAA(T62, T63, T64, X102, T42, intA_in_gga(T62, T63, T64))
PE_IN_GGAAA(T62, T63, T64, X102, T42) → INTA_IN_GGA(T62, T63, T64)
U12_GGAAA(T62, T63, T64, X102, T42, intA_out_gga(T62, T63, T64)) → U13_GGAAA(T62, T63, T64, X102, T42, pH_in_gaa(T64, X102, T42))
U12_GGAAA(T62, T63, T64, X102, T42, intA_out_gga(T62, T63, T64)) → PH_IN_GAA(T64, X102, T42)
PH_IN_GAA(T64, T65, T42) → U14_GAA(T64, T65, T42, intlistG_in_ga(T64, T65))
PH_IN_GAA(T64, T65, T42) → INTLISTG_IN_GA(T64, T65)
INTLISTG_IN_GA(.(T70, T71), .(s(T70), X114)) → U7_GA(T70, T71, X114, intlistG_in_ga(T71, X114))
INTLISTG_IN_GA(.(T70, T71), .(s(T70), X114)) → INTLISTG_IN_GA(T71, X114)
U14_GAA(T64, T65, T42, intlistG_out_ga(T64, T65)) → U15_GAA(T64, T65, T42, intlistF_in_ga(T65, T42))
U14_GAA(T64, T65, T42, intlistG_out_ga(T64, T65)) → INTLISTF_IN_GA(T65, T42)
INTLISTF_IN_GA(.(T29, T30), .(s(T29), T32)) → U6_GA(T29, T30, T32, intlistF_in_ga(T30, T32))
INTLISTF_IN_GA(.(T29, T30), .(s(T29), T32)) → INTLISTF_IN_GA(T30, T32)
U10_GAA(T51, T52, T42, intA_out_gga(s(0), s(T51), T52)) → U11_GAA(T51, T52, T42, intlistF_in_ga(.(0, T52), T42))
U10_GAA(T51, T52, T42, intA_out_gga(s(0), s(T51), T52)) → INTLISTF_IN_GA(.(0, T52), T42)
U8_GAA(T19, T22, T21, intA_out_gga(0, T19, T22)) → U9_GAA(T19, T22, T21, intlistF_in_ga(T22, T21))
U8_GAA(T19, T22, T21, intA_out_gga(0, T19, T22)) → INTLISTF_IN_GA(T22, T21)

The TRS R consists of the following rules:

intA_in_gga(0, 0, .(0, [])) → intA_out_gga(0, 0, .(0, []))
intA_in_gga(0, s(T19), .(0, T21)) → U1_gga(T19, T21, pB_in_gaa(T19, X31, T21))
pB_in_gaa(T19, T22, T21) → U8_gaa(T19, T22, T21, intA_in_gga(0, T19, T22))
intA_in_gga(s(T34), 0, []) → intA_out_gga(s(T34), 0, [])
intA_in_gga(s(0), s(0), .(s(0), T46)) → U2_gga(T46, intlistC_in_a(T46))
intlistC_in_a([]) → intlistC_out_a([])
U2_gga(T46, intlistC_out_a(T46)) → intA_out_gga(s(0), s(0), .(s(0), T46))
intA_in_gga(s(0), s(s(T51)), T42) → U3_gga(T51, T42, pD_in_gaa(T51, X83, T42))
pD_in_gaa(T51, T52, T42) → U10_gaa(T51, T52, T42, intA_in_gga(s(0), s(T51), T52))
intA_in_gga(s(s(T57)), s(0), T42) → U4_gga(T57, T42, intlistC_in_a(T42))
U4_gga(T57, T42, intlistC_out_a(T42)) → intA_out_gga(s(s(T57)), s(0), T42)
intA_in_gga(s(s(T62)), s(s(T63)), T42) → U5_gga(T62, T63, T42, pE_in_ggaaa(T62, T63, X101, X102, T42))
pE_in_ggaaa(T62, T63, T64, X102, T42) → U12_ggaaa(T62, T63, T64, X102, T42, intA_in_gga(T62, T63, T64))
U12_ggaaa(T62, T63, T64, X102, T42, intA_out_gga(T62, T63, T64)) → U13_ggaaa(T62, T63, T64, X102, T42, pH_in_gaa(T64, X102, T42))
pH_in_gaa(T64, T65, T42) → U14_gaa(T64, T65, T42, intlistG_in_ga(T64, T65))
intlistG_in_ga([], []) → intlistG_out_ga([], [])
intlistG_in_ga(.(T70, T71), .(s(T70), X114)) → U7_ga(T70, T71, X114, intlistG_in_ga(T71, X114))
U7_ga(T70, T71, X114, intlistG_out_ga(T71, X114)) → intlistG_out_ga(.(T70, T71), .(s(T70), X114))
U14_gaa(T64, T65, T42, intlistG_out_ga(T64, T65)) → U15_gaa(T64, T65, T42, intlistF_in_ga(T65, T42))
intlistF_in_ga([], []) → intlistF_out_ga([], [])
intlistF_in_ga(.(T29, T30), .(s(T29), T32)) → U6_ga(T29, T30, T32, intlistF_in_ga(T30, T32))
U6_ga(T29, T30, T32, intlistF_out_ga(T30, T32)) → intlistF_out_ga(.(T29, T30), .(s(T29), T32))
U15_gaa(T64, T65, T42, intlistF_out_ga(T65, T42)) → pH_out_gaa(T64, T65, T42)
U13_ggaaa(T62, T63, T64, X102, T42, pH_out_gaa(T64, X102, T42)) → pE_out_ggaaa(T62, T63, T64, X102, T42)
U5_gga(T62, T63, T42, pE_out_ggaaa(T62, T63, X101, X102, T42)) → intA_out_gga(s(s(T62)), s(s(T63)), T42)
U10_gaa(T51, T52, T42, intA_out_gga(s(0), s(T51), T52)) → U11_gaa(T51, T52, T42, intlistF_in_ga(.(0, T52), T42))
U11_gaa(T51, T52, T42, intlistF_out_ga(.(0, T52), T42)) → pD_out_gaa(T51, T52, T42)
U3_gga(T51, T42, pD_out_gaa(T51, X83, T42)) → intA_out_gga(s(0), s(s(T51)), T42)
U8_gaa(T19, T22, T21, intA_out_gga(0, T19, T22)) → U9_gaa(T19, T22, T21, intlistF_in_ga(T22, T21))
U9_gaa(T19, T22, T21, intlistF_out_ga(T22, T21)) → pB_out_gaa(T19, T22, T21)
U1_gga(T19, T21, pB_out_gaa(T19, X31, T21)) → intA_out_gga(0, s(T19), .(0, T21))

The argument filtering Pi contains the following mapping:
intA_in_gga(x1, x2, x3)  =  intA_in_gga(x1, x2)
0  =  0
intA_out_gga(x1, x2, x3)  =  intA_out_gga(x1, x2, x3)
s(x1)  =  s(x1)
U1_gga(x1, x2, x3)  =  U1_gga(x1, x3)
pB_in_gaa(x1, x2, x3)  =  pB_in_gaa(x1)
U8_gaa(x1, x2, x3, x4)  =  U8_gaa(x1, x4)
U2_gga(x1, x2)  =  U2_gga(x2)
intlistC_in_a(x1)  =  intlistC_in_a
intlistC_out_a(x1)  =  intlistC_out_a(x1)
U3_gga(x1, x2, x3)  =  U3_gga(x1, x3)
pD_in_gaa(x1, x2, x3)  =  pD_in_gaa(x1)
U10_gaa(x1, x2, x3, x4)  =  U10_gaa(x1, x4)
U4_gga(x1, x2, x3)  =  U4_gga(x1, x3)
U5_gga(x1, x2, x3, x4)  =  U5_gga(x1, x2, x4)
pE_in_ggaaa(x1, x2, x3, x4, x5)  =  pE_in_ggaaa(x1, x2)
U12_ggaaa(x1, x2, x3, x4, x5, x6)  =  U12_ggaaa(x1, x2, x6)
U13_ggaaa(x1, x2, x3, x4, x5, x6)  =  U13_ggaaa(x1, x2, x3, x6)
pH_in_gaa(x1, x2, x3)  =  pH_in_gaa(x1)
U14_gaa(x1, x2, x3, x4)  =  U14_gaa(x1, x4)
intlistG_in_ga(x1, x2)  =  intlistG_in_ga(x1)
[]  =  []
intlistG_out_ga(x1, x2)  =  intlistG_out_ga(x1, x2)
.(x1, x2)  =  .(x1, x2)
U7_ga(x1, x2, x3, x4)  =  U7_ga(x1, x2, x4)
U15_gaa(x1, x2, x3, x4)  =  U15_gaa(x1, x2, x4)
intlistF_in_ga(x1, x2)  =  intlistF_in_ga(x1)
intlistF_out_ga(x1, x2)  =  intlistF_out_ga(x1, x2)
U6_ga(x1, x2, x3, x4)  =  U6_ga(x1, x2, x4)
pH_out_gaa(x1, x2, x3)  =  pH_out_gaa(x1, x2, x3)
pE_out_ggaaa(x1, x2, x3, x4, x5)  =  pE_out_ggaaa(x1, x2, x3, x4, x5)
U11_gaa(x1, x2, x3, x4)  =  U11_gaa(x1, x2, x4)
pD_out_gaa(x1, x2, x3)  =  pD_out_gaa(x1, x2, x3)
U9_gaa(x1, x2, x3, x4)  =  U9_gaa(x1, x2, x4)
pB_out_gaa(x1, x2, x3)  =  pB_out_gaa(x1, x2, x3)
INTA_IN_GGA(x1, x2, x3)  =  INTA_IN_GGA(x1, x2)
U1_GGA(x1, x2, x3)  =  U1_GGA(x1, x3)
PB_IN_GAA(x1, x2, x3)  =  PB_IN_GAA(x1)
U8_GAA(x1, x2, x3, x4)  =  U8_GAA(x1, x4)
U2_GGA(x1, x2)  =  U2_GGA(x2)
INTLISTC_IN_A(x1)  =  INTLISTC_IN_A
U3_GGA(x1, x2, x3)  =  U3_GGA(x1, x3)
PD_IN_GAA(x1, x2, x3)  =  PD_IN_GAA(x1)
U10_GAA(x1, x2, x3, x4)  =  U10_GAA(x1, x4)
U4_GGA(x1, x2, x3)  =  U4_GGA(x1, x3)
U5_GGA(x1, x2, x3, x4)  =  U5_GGA(x1, x2, x4)
PE_IN_GGAAA(x1, x2, x3, x4, x5)  =  PE_IN_GGAAA(x1, x2)
U12_GGAAA(x1, x2, x3, x4, x5, x6)  =  U12_GGAAA(x1, x2, x6)
U13_GGAAA(x1, x2, x3, x4, x5, x6)  =  U13_GGAAA(x1, x2, x3, x6)
PH_IN_GAA(x1, x2, x3)  =  PH_IN_GAA(x1)
U14_GAA(x1, x2, x3, x4)  =  U14_GAA(x1, x4)
INTLISTG_IN_GA(x1, x2)  =  INTLISTG_IN_GA(x1)
U7_GA(x1, x2, x3, x4)  =  U7_GA(x1, x2, x4)
U15_GAA(x1, x2, x3, x4)  =  U15_GAA(x1, x2, x4)
INTLISTF_IN_GA(x1, x2)  =  INTLISTF_IN_GA(x1)
U6_GA(x1, x2, x3, x4)  =  U6_GA(x1, x2, x4)
U11_GAA(x1, x2, x3, x4)  =  U11_GAA(x1, x2, x4)
U9_GAA(x1, x2, x3, x4)  =  U9_GAA(x1, x2, x4)

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

(5) DependencyGraphProof (EQUIVALENT transformation)

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

(6) Complex Obligation (AND)

(7) Obligation:

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

INTLISTF_IN_GA(.(T29, T30), .(s(T29), T32)) → INTLISTF_IN_GA(T30, T32)

The TRS R consists of the following rules:

intA_in_gga(0, 0, .(0, [])) → intA_out_gga(0, 0, .(0, []))
intA_in_gga(0, s(T19), .(0, T21)) → U1_gga(T19, T21, pB_in_gaa(T19, X31, T21))
pB_in_gaa(T19, T22, T21) → U8_gaa(T19, T22, T21, intA_in_gga(0, T19, T22))
intA_in_gga(s(T34), 0, []) → intA_out_gga(s(T34), 0, [])
intA_in_gga(s(0), s(0), .(s(0), T46)) → U2_gga(T46, intlistC_in_a(T46))
intlistC_in_a([]) → intlistC_out_a([])
U2_gga(T46, intlistC_out_a(T46)) → intA_out_gga(s(0), s(0), .(s(0), T46))
intA_in_gga(s(0), s(s(T51)), T42) → U3_gga(T51, T42, pD_in_gaa(T51, X83, T42))
pD_in_gaa(T51, T52, T42) → U10_gaa(T51, T52, T42, intA_in_gga(s(0), s(T51), T52))
intA_in_gga(s(s(T57)), s(0), T42) → U4_gga(T57, T42, intlistC_in_a(T42))
U4_gga(T57, T42, intlistC_out_a(T42)) → intA_out_gga(s(s(T57)), s(0), T42)
intA_in_gga(s(s(T62)), s(s(T63)), T42) → U5_gga(T62, T63, T42, pE_in_ggaaa(T62, T63, X101, X102, T42))
pE_in_ggaaa(T62, T63, T64, X102, T42) → U12_ggaaa(T62, T63, T64, X102, T42, intA_in_gga(T62, T63, T64))
U12_ggaaa(T62, T63, T64, X102, T42, intA_out_gga(T62, T63, T64)) → U13_ggaaa(T62, T63, T64, X102, T42, pH_in_gaa(T64, X102, T42))
pH_in_gaa(T64, T65, T42) → U14_gaa(T64, T65, T42, intlistG_in_ga(T64, T65))
intlistG_in_ga([], []) → intlistG_out_ga([], [])
intlistG_in_ga(.(T70, T71), .(s(T70), X114)) → U7_ga(T70, T71, X114, intlistG_in_ga(T71, X114))
U7_ga(T70, T71, X114, intlistG_out_ga(T71, X114)) → intlistG_out_ga(.(T70, T71), .(s(T70), X114))
U14_gaa(T64, T65, T42, intlistG_out_ga(T64, T65)) → U15_gaa(T64, T65, T42, intlistF_in_ga(T65, T42))
intlistF_in_ga([], []) → intlistF_out_ga([], [])
intlistF_in_ga(.(T29, T30), .(s(T29), T32)) → U6_ga(T29, T30, T32, intlistF_in_ga(T30, T32))
U6_ga(T29, T30, T32, intlistF_out_ga(T30, T32)) → intlistF_out_ga(.(T29, T30), .(s(T29), T32))
U15_gaa(T64, T65, T42, intlistF_out_ga(T65, T42)) → pH_out_gaa(T64, T65, T42)
U13_ggaaa(T62, T63, T64, X102, T42, pH_out_gaa(T64, X102, T42)) → pE_out_ggaaa(T62, T63, T64, X102, T42)
U5_gga(T62, T63, T42, pE_out_ggaaa(T62, T63, X101, X102, T42)) → intA_out_gga(s(s(T62)), s(s(T63)), T42)
U10_gaa(T51, T52, T42, intA_out_gga(s(0), s(T51), T52)) → U11_gaa(T51, T52, T42, intlistF_in_ga(.(0, T52), T42))
U11_gaa(T51, T52, T42, intlistF_out_ga(.(0, T52), T42)) → pD_out_gaa(T51, T52, T42)
U3_gga(T51, T42, pD_out_gaa(T51, X83, T42)) → intA_out_gga(s(0), s(s(T51)), T42)
U8_gaa(T19, T22, T21, intA_out_gga(0, T19, T22)) → U9_gaa(T19, T22, T21, intlistF_in_ga(T22, T21))
U9_gaa(T19, T22, T21, intlistF_out_ga(T22, T21)) → pB_out_gaa(T19, T22, T21)
U1_gga(T19, T21, pB_out_gaa(T19, X31, T21)) → intA_out_gga(0, s(T19), .(0, T21))

The argument filtering Pi contains the following mapping:
intA_in_gga(x1, x2, x3)  =  intA_in_gga(x1, x2)
0  =  0
intA_out_gga(x1, x2, x3)  =  intA_out_gga(x1, x2, x3)
s(x1)  =  s(x1)
U1_gga(x1, x2, x3)  =  U1_gga(x1, x3)
pB_in_gaa(x1, x2, x3)  =  pB_in_gaa(x1)
U8_gaa(x1, x2, x3, x4)  =  U8_gaa(x1, x4)
U2_gga(x1, x2)  =  U2_gga(x2)
intlistC_in_a(x1)  =  intlistC_in_a
intlistC_out_a(x1)  =  intlistC_out_a(x1)
U3_gga(x1, x2, x3)  =  U3_gga(x1, x3)
pD_in_gaa(x1, x2, x3)  =  pD_in_gaa(x1)
U10_gaa(x1, x2, x3, x4)  =  U10_gaa(x1, x4)
U4_gga(x1, x2, x3)  =  U4_gga(x1, x3)
U5_gga(x1, x2, x3, x4)  =  U5_gga(x1, x2, x4)
pE_in_ggaaa(x1, x2, x3, x4, x5)  =  pE_in_ggaaa(x1, x2)
U12_ggaaa(x1, x2, x3, x4, x5, x6)  =  U12_ggaaa(x1, x2, x6)
U13_ggaaa(x1, x2, x3, x4, x5, x6)  =  U13_ggaaa(x1, x2, x3, x6)
pH_in_gaa(x1, x2, x3)  =  pH_in_gaa(x1)
U14_gaa(x1, x2, x3, x4)  =  U14_gaa(x1, x4)
intlistG_in_ga(x1, x2)  =  intlistG_in_ga(x1)
[]  =  []
intlistG_out_ga(x1, x2)  =  intlistG_out_ga(x1, x2)
.(x1, x2)  =  .(x1, x2)
U7_ga(x1, x2, x3, x4)  =  U7_ga(x1, x2, x4)
U15_gaa(x1, x2, x3, x4)  =  U15_gaa(x1, x2, x4)
intlistF_in_ga(x1, x2)  =  intlistF_in_ga(x1)
intlistF_out_ga(x1, x2)  =  intlistF_out_ga(x1, x2)
U6_ga(x1, x2, x3, x4)  =  U6_ga(x1, x2, x4)
pH_out_gaa(x1, x2, x3)  =  pH_out_gaa(x1, x2, x3)
pE_out_ggaaa(x1, x2, x3, x4, x5)  =  pE_out_ggaaa(x1, x2, x3, x4, x5)
U11_gaa(x1, x2, x3, x4)  =  U11_gaa(x1, x2, x4)
pD_out_gaa(x1, x2, x3)  =  pD_out_gaa(x1, x2, x3)
U9_gaa(x1, x2, x3, x4)  =  U9_gaa(x1, x2, x4)
pB_out_gaa(x1, x2, x3)  =  pB_out_gaa(x1, x2, x3)
INTLISTF_IN_GA(x1, x2)  =  INTLISTF_IN_GA(x1)

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

(8) UsableRulesProof (EQUIVALENT transformation)

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

(9) Obligation:

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

INTLISTF_IN_GA(.(T29, T30), .(s(T29), T32)) → INTLISTF_IN_GA(T30, T32)

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

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

(10) PiDPToQDPProof (SOUND transformation)

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

(11) Obligation:

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

INTLISTF_IN_GA(.(T29, T30)) → INTLISTF_IN_GA(T30)

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:

• INTLISTF_IN_GA(.(T29, T30)) → INTLISTF_IN_GA(T30)
  The graph contains the following edges 1 > 1

(13) YES

(14) Obligation:

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

INTLISTG_IN_GA(.(T70, T71), .(s(T70), X114)) → INTLISTG_IN_GA(T71, X114)

The TRS R consists of the following rules:

intA_in_gga(0, 0, .(0, [])) → intA_out_gga(0, 0, .(0, []))
intA_in_gga(0, s(T19), .(0, T21)) → U1_gga(T19, T21, pB_in_gaa(T19, X31, T21))
pB_in_gaa(T19, T22, T21) → U8_gaa(T19, T22, T21, intA_in_gga(0, T19, T22))
intA_in_gga(s(T34), 0, []) → intA_out_gga(s(T34), 0, [])
intA_in_gga(s(0), s(0), .(s(0), T46)) → U2_gga(T46, intlistC_in_a(T46))
intlistC_in_a([]) → intlistC_out_a([])
U2_gga(T46, intlistC_out_a(T46)) → intA_out_gga(s(0), s(0), .(s(0), T46))
intA_in_gga(s(0), s(s(T51)), T42) → U3_gga(T51, T42, pD_in_gaa(T51, X83, T42))
pD_in_gaa(T51, T52, T42) → U10_gaa(T51, T52, T42, intA_in_gga(s(0), s(T51), T52))
intA_in_gga(s(s(T57)), s(0), T42) → U4_gga(T57, T42, intlistC_in_a(T42))
U4_gga(T57, T42, intlistC_out_a(T42)) → intA_out_gga(s(s(T57)), s(0), T42)
intA_in_gga(s(s(T62)), s(s(T63)), T42) → U5_gga(T62, T63, T42, pE_in_ggaaa(T62, T63, X101, X102, T42))
pE_in_ggaaa(T62, T63, T64, X102, T42) → U12_ggaaa(T62, T63, T64, X102, T42, intA_in_gga(T62, T63, T64))
U12_ggaaa(T62, T63, T64, X102, T42, intA_out_gga(T62, T63, T64)) → U13_ggaaa(T62, T63, T64, X102, T42, pH_in_gaa(T64, X102, T42))
pH_in_gaa(T64, T65, T42) → U14_gaa(T64, T65, T42, intlistG_in_ga(T64, T65))
intlistG_in_ga([], []) → intlistG_out_ga([], [])
intlistG_in_ga(.(T70, T71), .(s(T70), X114)) → U7_ga(T70, T71, X114, intlistG_in_ga(T71, X114))
U7_ga(T70, T71, X114, intlistG_out_ga(T71, X114)) → intlistG_out_ga(.(T70, T71), .(s(T70), X114))
U14_gaa(T64, T65, T42, intlistG_out_ga(T64, T65)) → U15_gaa(T64, T65, T42, intlistF_in_ga(T65, T42))
intlistF_in_ga([], []) → intlistF_out_ga([], [])
intlistF_in_ga(.(T29, T30), .(s(T29), T32)) → U6_ga(T29, T30, T32, intlistF_in_ga(T30, T32))
U6_ga(T29, T30, T32, intlistF_out_ga(T30, T32)) → intlistF_out_ga(.(T29, T30), .(s(T29), T32))
U15_gaa(T64, T65, T42, intlistF_out_ga(T65, T42)) → pH_out_gaa(T64, T65, T42)
U13_ggaaa(T62, T63, T64, X102, T42, pH_out_gaa(T64, X102, T42)) → pE_out_ggaaa(T62, T63, T64, X102, T42)
U5_gga(T62, T63, T42, pE_out_ggaaa(T62, T63, X101, X102, T42)) → intA_out_gga(s(s(T62)), s(s(T63)), T42)
U10_gaa(T51, T52, T42, intA_out_gga(s(0), s(T51), T52)) → U11_gaa(T51, T52, T42, intlistF_in_ga(.(0, T52), T42))
U11_gaa(T51, T52, T42, intlistF_out_ga(.(0, T52), T42)) → pD_out_gaa(T51, T52, T42)
U3_gga(T51, T42, pD_out_gaa(T51, X83, T42)) → intA_out_gga(s(0), s(s(T51)), T42)
U8_gaa(T19, T22, T21, intA_out_gga(0, T19, T22)) → U9_gaa(T19, T22, T21, intlistF_in_ga(T22, T21))
U9_gaa(T19, T22, T21, intlistF_out_ga(T22, T21)) → pB_out_gaa(T19, T22, T21)
U1_gga(T19, T21, pB_out_gaa(T19, X31, T21)) → intA_out_gga(0, s(T19), .(0, T21))

The argument filtering Pi contains the following mapping:
intA_in_gga(x1, x2, x3)  =  intA_in_gga(x1, x2)
0  =  0
intA_out_gga(x1, x2, x3)  =  intA_out_gga(x1, x2, x3)
s(x1)  =  s(x1)
U1_gga(x1, x2, x3)  =  U1_gga(x1, x3)
pB_in_gaa(x1, x2, x3)  =  pB_in_gaa(x1)
U8_gaa(x1, x2, x3, x4)  =  U8_gaa(x1, x4)
U2_gga(x1, x2)  =  U2_gga(x2)
intlistC_in_a(x1)  =  intlistC_in_a
intlistC_out_a(x1)  =  intlistC_out_a(x1)
U3_gga(x1, x2, x3)  =  U3_gga(x1, x3)
pD_in_gaa(x1, x2, x3)  =  pD_in_gaa(x1)
U10_gaa(x1, x2, x3, x4)  =  U10_gaa(x1, x4)
U4_gga(x1, x2, x3)  =  U4_gga(x1, x3)
U5_gga(x1, x2, x3, x4)  =  U5_gga(x1, x2, x4)
pE_in_ggaaa(x1, x2, x3, x4, x5)  =  pE_in_ggaaa(x1, x2)
U12_ggaaa(x1, x2, x3, x4, x5, x6)  =  U12_ggaaa(x1, x2, x6)
U13_ggaaa(x1, x2, x3, x4, x5, x6)  =  U13_ggaaa(x1, x2, x3, x6)
pH_in_gaa(x1, x2, x3)  =  pH_in_gaa(x1)
U14_gaa(x1, x2, x3, x4)  =  U14_gaa(x1, x4)
intlistG_in_ga(x1, x2)  =  intlistG_in_ga(x1)
[]  =  []
intlistG_out_ga(x1, x2)  =  intlistG_out_ga(x1, x2)
.(x1, x2)  =  .(x1, x2)
U7_ga(x1, x2, x3, x4)  =  U7_ga(x1, x2, x4)
U15_gaa(x1, x2, x3, x4)  =  U15_gaa(x1, x2, x4)
intlistF_in_ga(x1, x2)  =  intlistF_in_ga(x1)
intlistF_out_ga(x1, x2)  =  intlistF_out_ga(x1, x2)
U6_ga(x1, x2, x3, x4)  =  U6_ga(x1, x2, x4)
pH_out_gaa(x1, x2, x3)  =  pH_out_gaa(x1, x2, x3)
pE_out_ggaaa(x1, x2, x3, x4, x5)  =  pE_out_ggaaa(x1, x2, x3, x4, x5)
U11_gaa(x1, x2, x3, x4)  =  U11_gaa(x1, x2, x4)
pD_out_gaa(x1, x2, x3)  =  pD_out_gaa(x1, x2, x3)
U9_gaa(x1, x2, x3, x4)  =  U9_gaa(x1, x2, x4)
pB_out_gaa(x1, x2, x3)  =  pB_out_gaa(x1, x2, x3)
INTLISTG_IN_GA(x1, x2)  =  INTLISTG_IN_GA(x1)

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:

INTLISTG_IN_GA(.(T70, T71), .(s(T70), X114)) → INTLISTG_IN_GA(T71, X114)

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

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:

INTLISTG_IN_GA(.(T70, T71)) → INTLISTG_IN_GA(T71)

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

(19) QDPSizeChangeProof (EQUIVALENT transformation)

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

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

• INTLISTG_IN_GA(.(T70, T71)) → INTLISTG_IN_GA(T71)
  The graph contains the following edges 1 > 1

(20) YES

(21) Obligation:

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

INTA_IN_GGA(s(0), s(s(T51)), T42) → PD_IN_GAA(T51, X83, T42)
PD_IN_GAA(T51, T52, T42) → INTA_IN_GGA(s(0), s(T51), T52)

The TRS R consists of the following rules:

intA_in_gga(0, 0, .(0, [])) → intA_out_gga(0, 0, .(0, []))
intA_in_gga(0, s(T19), .(0, T21)) → U1_gga(T19, T21, pB_in_gaa(T19, X31, T21))
pB_in_gaa(T19, T22, T21) → U8_gaa(T19, T22, T21, intA_in_gga(0, T19, T22))
intA_in_gga(s(T34), 0, []) → intA_out_gga(s(T34), 0, [])
intA_in_gga(s(0), s(0), .(s(0), T46)) → U2_gga(T46, intlistC_in_a(T46))
intlistC_in_a([]) → intlistC_out_a([])
U2_gga(T46, intlistC_out_a(T46)) → intA_out_gga(s(0), s(0), .(s(0), T46))
intA_in_gga(s(0), s(s(T51)), T42) → U3_gga(T51, T42, pD_in_gaa(T51, X83, T42))
pD_in_gaa(T51, T52, T42) → U10_gaa(T51, T52, T42, intA_in_gga(s(0), s(T51), T52))
intA_in_gga(s(s(T57)), s(0), T42) → U4_gga(T57, T42, intlistC_in_a(T42))
U4_gga(T57, T42, intlistC_out_a(T42)) → intA_out_gga(s(s(T57)), s(0), T42)
intA_in_gga(s(s(T62)), s(s(T63)), T42) → U5_gga(T62, T63, T42, pE_in_ggaaa(T62, T63, X101, X102, T42))
pE_in_ggaaa(T62, T63, T64, X102, T42) → U12_ggaaa(T62, T63, T64, X102, T42, intA_in_gga(T62, T63, T64))
U12_ggaaa(T62, T63, T64, X102, T42, intA_out_gga(T62, T63, T64)) → U13_ggaaa(T62, T63, T64, X102, T42, pH_in_gaa(T64, X102, T42))
pH_in_gaa(T64, T65, T42) → U14_gaa(T64, T65, T42, intlistG_in_ga(T64, T65))
intlistG_in_ga([], []) → intlistG_out_ga([], [])
intlistG_in_ga(.(T70, T71), .(s(T70), X114)) → U7_ga(T70, T71, X114, intlistG_in_ga(T71, X114))
U7_ga(T70, T71, X114, intlistG_out_ga(T71, X114)) → intlistG_out_ga(.(T70, T71), .(s(T70), X114))
U14_gaa(T64, T65, T42, intlistG_out_ga(T64, T65)) → U15_gaa(T64, T65, T42, intlistF_in_ga(T65, T42))
intlistF_in_ga([], []) → intlistF_out_ga([], [])
intlistF_in_ga(.(T29, T30), .(s(T29), T32)) → U6_ga(T29, T30, T32, intlistF_in_ga(T30, T32))
U6_ga(T29, T30, T32, intlistF_out_ga(T30, T32)) → intlistF_out_ga(.(T29, T30), .(s(T29), T32))
U15_gaa(T64, T65, T42, intlistF_out_ga(T65, T42)) → pH_out_gaa(T64, T65, T42)
U13_ggaaa(T62, T63, T64, X102, T42, pH_out_gaa(T64, X102, T42)) → pE_out_ggaaa(T62, T63, T64, X102, T42)
U5_gga(T62, T63, T42, pE_out_ggaaa(T62, T63, X101, X102, T42)) → intA_out_gga(s(s(T62)), s(s(T63)), T42)
U10_gaa(T51, T52, T42, intA_out_gga(s(0), s(T51), T52)) → U11_gaa(T51, T52, T42, intlistF_in_ga(.(0, T52), T42))
U11_gaa(T51, T52, T42, intlistF_out_ga(.(0, T52), T42)) → pD_out_gaa(T51, T52, T42)
U3_gga(T51, T42, pD_out_gaa(T51, X83, T42)) → intA_out_gga(s(0), s(s(T51)), T42)
U8_gaa(T19, T22, T21, intA_out_gga(0, T19, T22)) → U9_gaa(T19, T22, T21, intlistF_in_ga(T22, T21))
U9_gaa(T19, T22, T21, intlistF_out_ga(T22, T21)) → pB_out_gaa(T19, T22, T21)
U1_gga(T19, T21, pB_out_gaa(T19, X31, T21)) → intA_out_gga(0, s(T19), .(0, T21))

The argument filtering Pi contains the following mapping:
intA_in_gga(x1, x2, x3)  =  intA_in_gga(x1, x2)
0  =  0
intA_out_gga(x1, x2, x3)  =  intA_out_gga(x1, x2, x3)
s(x1)  =  s(x1)
U1_gga(x1, x2, x3)  =  U1_gga(x1, x3)
pB_in_gaa(x1, x2, x3)  =  pB_in_gaa(x1)
U8_gaa(x1, x2, x3, x4)  =  U8_gaa(x1, x4)
U2_gga(x1, x2)  =  U2_gga(x2)
intlistC_in_a(x1)  =  intlistC_in_a
intlistC_out_a(x1)  =  intlistC_out_a(x1)
U3_gga(x1, x2, x3)  =  U3_gga(x1, x3)
pD_in_gaa(x1, x2, x3)  =  pD_in_gaa(x1)
U10_gaa(x1, x2, x3, x4)  =  U10_gaa(x1, x4)
U4_gga(x1, x2, x3)  =  U4_gga(x1, x3)
U5_gga(x1, x2, x3, x4)  =  U5_gga(x1, x2, x4)
pE_in_ggaaa(x1, x2, x3, x4, x5)  =  pE_in_ggaaa(x1, x2)
U12_ggaaa(x1, x2, x3, x4, x5, x6)  =  U12_ggaaa(x1, x2, x6)
U13_ggaaa(x1, x2, x3, x4, x5, x6)  =  U13_ggaaa(x1, x2, x3, x6)
pH_in_gaa(x1, x2, x3)  =  pH_in_gaa(x1)
U14_gaa(x1, x2, x3, x4)  =  U14_gaa(x1, x4)
intlistG_in_ga(x1, x2)  =  intlistG_in_ga(x1)
[]  =  []
intlistG_out_ga(x1, x2)  =  intlistG_out_ga(x1, x2)
.(x1, x2)  =  .(x1, x2)
U7_ga(x1, x2, x3, x4)  =  U7_ga(x1, x2, x4)
U15_gaa(x1, x2, x3, x4)  =  U15_gaa(x1, x2, x4)
intlistF_in_ga(x1, x2)  =  intlistF_in_ga(x1)
intlistF_out_ga(x1, x2)  =  intlistF_out_ga(x1, x2)
U6_ga(x1, x2, x3, x4)  =  U6_ga(x1, x2, x4)
pH_out_gaa(x1, x2, x3)  =  pH_out_gaa(x1, x2, x3)
pE_out_ggaaa(x1, x2, x3, x4, x5)  =  pE_out_ggaaa(x1, x2, x3, x4, x5)
U11_gaa(x1, x2, x3, x4)  =  U11_gaa(x1, x2, x4)
pD_out_gaa(x1, x2, x3)  =  pD_out_gaa(x1, x2, x3)
U9_gaa(x1, x2, x3, x4)  =  U9_gaa(x1, x2, x4)
pB_out_gaa(x1, x2, x3)  =  pB_out_gaa(x1, x2, x3)
INTA_IN_GGA(x1, x2, x3)  =  INTA_IN_GGA(x1, x2)
PD_IN_GAA(x1, x2, x3)  =  PD_IN_GAA(x1)

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

(22) UsableRulesProof (EQUIVALENT transformation)

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

(23) Obligation:

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

INTA_IN_GGA(s(0), s(s(T51)), T42) → PD_IN_GAA(T51, X83, T42)
PD_IN_GAA(T51, T52, T42) → INTA_IN_GGA(s(0), s(T51), T52)

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

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

(24) PiDPToQDPProof (SOUND transformation)

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

(25) Obligation:

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

INTA_IN_GGA(s(0), s(s(T51))) → PD_IN_GAA(T51)
PD_IN_GAA(T51) → INTA_IN_GGA(s(0), s(T51))

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

(26) MRRProof (EQUIVALENT transformation)

By using the rule removal processor [LPAR04] with the following ordering, at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented.
Strictly oriented dependency pairs:

INTA_IN_GGA(s(0), s(s(T51))) → PD_IN_GAA(T51)

Used ordering: Polynomial interpretation [POLO]:

POL(0) = 0   
POL(INTA_IN_GGA(x₁, x₂)) = x₁ + x₂   
POL(PD_IN_GAA(x₁)) = 2 + 2·x₁   
POL(s(x₁)) = 1 + 2·x₁   

(27) Obligation:

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

PD_IN_GAA(T51) → INTA_IN_GGA(s(0), s(T51))

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

(28) DependencyGraphProof (EQUIVALENT transformation)

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

(29) TRUE

(30) Obligation:

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

INTA_IN_GGA(0, s(T19), .(0, T21)) → PB_IN_GAA(T19, X31, T21)
PB_IN_GAA(T19, T22, T21) → INTA_IN_GGA(0, T19, T22)

The TRS R consists of the following rules:

intA_in_gga(0, 0, .(0, [])) → intA_out_gga(0, 0, .(0, []))
intA_in_gga(0, s(T19), .(0, T21)) → U1_gga(T19, T21, pB_in_gaa(T19, X31, T21))
pB_in_gaa(T19, T22, T21) → U8_gaa(T19, T22, T21, intA_in_gga(0, T19, T22))
intA_in_gga(s(T34), 0, []) → intA_out_gga(s(T34), 0, [])
intA_in_gga(s(0), s(0), .(s(0), T46)) → U2_gga(T46, intlistC_in_a(T46))
intlistC_in_a([]) → intlistC_out_a([])
U2_gga(T46, intlistC_out_a(T46)) → intA_out_gga(s(0), s(0), .(s(0), T46))
intA_in_gga(s(0), s(s(T51)), T42) → U3_gga(T51, T42, pD_in_gaa(T51, X83, T42))
pD_in_gaa(T51, T52, T42) → U10_gaa(T51, T52, T42, intA_in_gga(s(0), s(T51), T52))
intA_in_gga(s(s(T57)), s(0), T42) → U4_gga(T57, T42, intlistC_in_a(T42))
U4_gga(T57, T42, intlistC_out_a(T42)) → intA_out_gga(s(s(T57)), s(0), T42)
intA_in_gga(s(s(T62)), s(s(T63)), T42) → U5_gga(T62, T63, T42, pE_in_ggaaa(T62, T63, X101, X102, T42))
pE_in_ggaaa(T62, T63, T64, X102, T42) → U12_ggaaa(T62, T63, T64, X102, T42, intA_in_gga(T62, T63, T64))
U12_ggaaa(T62, T63, T64, X102, T42, intA_out_gga(T62, T63, T64)) → U13_ggaaa(T62, T63, T64, X102, T42, pH_in_gaa(T64, X102, T42))
pH_in_gaa(T64, T65, T42) → U14_gaa(T64, T65, T42, intlistG_in_ga(T64, T65))
intlistG_in_ga([], []) → intlistG_out_ga([], [])
intlistG_in_ga(.(T70, T71), .(s(T70), X114)) → U7_ga(T70, T71, X114, intlistG_in_ga(T71, X114))
U7_ga(T70, T71, X114, intlistG_out_ga(T71, X114)) → intlistG_out_ga(.(T70, T71), .(s(T70), X114))
U14_gaa(T64, T65, T42, intlistG_out_ga(T64, T65)) → U15_gaa(T64, T65, T42, intlistF_in_ga(T65, T42))
intlistF_in_ga([], []) → intlistF_out_ga([], [])
intlistF_in_ga(.(T29, T30), .(s(T29), T32)) → U6_ga(T29, T30, T32, intlistF_in_ga(T30, T32))
U6_ga(T29, T30, T32, intlistF_out_ga(T30, T32)) → intlistF_out_ga(.(T29, T30), .(s(T29), T32))
U15_gaa(T64, T65, T42, intlistF_out_ga(T65, T42)) → pH_out_gaa(T64, T65, T42)
U13_ggaaa(T62, T63, T64, X102, T42, pH_out_gaa(T64, X102, T42)) → pE_out_ggaaa(T62, T63, T64, X102, T42)
U5_gga(T62, T63, T42, pE_out_ggaaa(T62, T63, X101, X102, T42)) → intA_out_gga(s(s(T62)), s(s(T63)), T42)
U10_gaa(T51, T52, T42, intA_out_gga(s(0), s(T51), T52)) → U11_gaa(T51, T52, T42, intlistF_in_ga(.(0, T52), T42))
U11_gaa(T51, T52, T42, intlistF_out_ga(.(0, T52), T42)) → pD_out_gaa(T51, T52, T42)
U3_gga(T51, T42, pD_out_gaa(T51, X83, T42)) → intA_out_gga(s(0), s(s(T51)), T42)
U8_gaa(T19, T22, T21, intA_out_gga(0, T19, T22)) → U9_gaa(T19, T22, T21, intlistF_in_ga(T22, T21))
U9_gaa(T19, T22, T21, intlistF_out_ga(T22, T21)) → pB_out_gaa(T19, T22, T21)
U1_gga(T19, T21, pB_out_gaa(T19, X31, T21)) → intA_out_gga(0, s(T19), .(0, T21))

The argument filtering Pi contains the following mapping:
intA_in_gga(x1, x2, x3)  =  intA_in_gga(x1, x2)
0  =  0
intA_out_gga(x1, x2, x3)  =  intA_out_gga(x1, x2, x3)
s(x1)  =  s(x1)
U1_gga(x1, x2, x3)  =  U1_gga(x1, x3)
pB_in_gaa(x1, x2, x3)  =  pB_in_gaa(x1)
U8_gaa(x1, x2, x3, x4)  =  U8_gaa(x1, x4)
U2_gga(x1, x2)  =  U2_gga(x2)
intlistC_in_a(x1)  =  intlistC_in_a
intlistC_out_a(x1)  =  intlistC_out_a(x1)
U3_gga(x1, x2, x3)  =  U3_gga(x1, x3)
pD_in_gaa(x1, x2, x3)  =  pD_in_gaa(x1)
U10_gaa(x1, x2, x3, x4)  =  U10_gaa(x1, x4)
U4_gga(x1, x2, x3)  =  U4_gga(x1, x3)
U5_gga(x1, x2, x3, x4)  =  U5_gga(x1, x2, x4)
pE_in_ggaaa(x1, x2, x3, x4, x5)  =  pE_in_ggaaa(x1, x2)
U12_ggaaa(x1, x2, x3, x4, x5, x6)  =  U12_ggaaa(x1, x2, x6)
U13_ggaaa(x1, x2, x3, x4, x5, x6)  =  U13_ggaaa(x1, x2, x3, x6)
pH_in_gaa(x1, x2, x3)  =  pH_in_gaa(x1)
U14_gaa(x1, x2, x3, x4)  =  U14_gaa(x1, x4)
intlistG_in_ga(x1, x2)  =  intlistG_in_ga(x1)
[]  =  []
intlistG_out_ga(x1, x2)  =  intlistG_out_ga(x1, x2)
.(x1, x2)  =  .(x1, x2)
U7_ga(x1, x2, x3, x4)  =  U7_ga(x1, x2, x4)
U15_gaa(x1, x2, x3, x4)  =  U15_gaa(x1, x2, x4)
intlistF_in_ga(x1, x2)  =  intlistF_in_ga(x1)
intlistF_out_ga(x1, x2)  =  intlistF_out_ga(x1, x2)
U6_ga(x1, x2, x3, x4)  =  U6_ga(x1, x2, x4)
pH_out_gaa(x1, x2, x3)  =  pH_out_gaa(x1, x2, x3)
pE_out_ggaaa(x1, x2, x3, x4, x5)  =  pE_out_ggaaa(x1, x2, x3, x4, x5)
U11_gaa(x1, x2, x3, x4)  =  U11_gaa(x1, x2, x4)
pD_out_gaa(x1, x2, x3)  =  pD_out_gaa(x1, x2, x3)
U9_gaa(x1, x2, x3, x4)  =  U9_gaa(x1, x2, x4)
pB_out_gaa(x1, x2, x3)  =  pB_out_gaa(x1, x2, x3)
INTA_IN_GGA(x1, x2, x3)  =  INTA_IN_GGA(x1, x2)
PB_IN_GAA(x1, x2, x3)  =  PB_IN_GAA(x1)

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

(31) UsableRulesProof (EQUIVALENT transformation)

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

(32) Obligation:

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

INTA_IN_GGA(0, s(T19), .(0, T21)) → PB_IN_GAA(T19, X31, T21)
PB_IN_GAA(T19, T22, T21) → INTA_IN_GGA(0, T19, T22)

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

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

(33) PiDPToQDPProof (SOUND transformation)

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

(34) Obligation:

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

INTA_IN_GGA(0, s(T19)) → PB_IN_GAA(T19)
PB_IN_GAA(T19) → INTA_IN_GGA(0, T19)

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

(35) QDPSizeChangeProof (EQUIVALENT transformation)

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

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

• PB_IN_GAA(T19) → INTA_IN_GGA(0, T19)
  The graph contains the following edges 1 >= 2

• INTA_IN_GGA(0, s(T19)) → PB_IN_GAA(T19)
  The graph contains the following edges 2 > 1

(36) YES

(37) Obligation:

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

INTA_IN_GGA(s(s(T62)), s(s(T63)), T42) → PE_IN_GGAAA(T62, T63, X101, X102, T42)
PE_IN_GGAAA(T62, T63, T64, X102, T42) → INTA_IN_GGA(T62, T63, T64)

The TRS R consists of the following rules:

intA_in_gga(0, 0, .(0, [])) → intA_out_gga(0, 0, .(0, []))
intA_in_gga(0, s(T19), .(0, T21)) → U1_gga(T19, T21, pB_in_gaa(T19, X31, T21))
pB_in_gaa(T19, T22, T21) → U8_gaa(T19, T22, T21, intA_in_gga(0, T19, T22))
intA_in_gga(s(T34), 0, []) → intA_out_gga(s(T34), 0, [])
intA_in_gga(s(0), s(0), .(s(0), T46)) → U2_gga(T46, intlistC_in_a(T46))
intlistC_in_a([]) → intlistC_out_a([])
U2_gga(T46, intlistC_out_a(T46)) → intA_out_gga(s(0), s(0), .(s(0), T46))
intA_in_gga(s(0), s(s(T51)), T42) → U3_gga(T51, T42, pD_in_gaa(T51, X83, T42))
pD_in_gaa(T51, T52, T42) → U10_gaa(T51, T52, T42, intA_in_gga(s(0), s(T51), T52))
intA_in_gga(s(s(T57)), s(0), T42) → U4_gga(T57, T42, intlistC_in_a(T42))
U4_gga(T57, T42, intlistC_out_a(T42)) → intA_out_gga(s(s(T57)), s(0), T42)
intA_in_gga(s(s(T62)), s(s(T63)), T42) → U5_gga(T62, T63, T42, pE_in_ggaaa(T62, T63, X101, X102, T42))
pE_in_ggaaa(T62, T63, T64, X102, T42) → U12_ggaaa(T62, T63, T64, X102, T42, intA_in_gga(T62, T63, T64))
U12_ggaaa(T62, T63, T64, X102, T42, intA_out_gga(T62, T63, T64)) → U13_ggaaa(T62, T63, T64, X102, T42, pH_in_gaa(T64, X102, T42))
pH_in_gaa(T64, T65, T42) → U14_gaa(T64, T65, T42, intlistG_in_ga(T64, T65))
intlistG_in_ga([], []) → intlistG_out_ga([], [])
intlistG_in_ga(.(T70, T71), .(s(T70), X114)) → U7_ga(T70, T71, X114, intlistG_in_ga(T71, X114))
U7_ga(T70, T71, X114, intlistG_out_ga(T71, X114)) → intlistG_out_ga(.(T70, T71), .(s(T70), X114))
U14_gaa(T64, T65, T42, intlistG_out_ga(T64, T65)) → U15_gaa(T64, T65, T42, intlistF_in_ga(T65, T42))
intlistF_in_ga([], []) → intlistF_out_ga([], [])
intlistF_in_ga(.(T29, T30), .(s(T29), T32)) → U6_ga(T29, T30, T32, intlistF_in_ga(T30, T32))
U6_ga(T29, T30, T32, intlistF_out_ga(T30, T32)) → intlistF_out_ga(.(T29, T30), .(s(T29), T32))
U15_gaa(T64, T65, T42, intlistF_out_ga(T65, T42)) → pH_out_gaa(T64, T65, T42)
U13_ggaaa(T62, T63, T64, X102, T42, pH_out_gaa(T64, X102, T42)) → pE_out_ggaaa(T62, T63, T64, X102, T42)
U5_gga(T62, T63, T42, pE_out_ggaaa(T62, T63, X101, X102, T42)) → intA_out_gga(s(s(T62)), s(s(T63)), T42)
U10_gaa(T51, T52, T42, intA_out_gga(s(0), s(T51), T52)) → U11_gaa(T51, T52, T42, intlistF_in_ga(.(0, T52), T42))
U11_gaa(T51, T52, T42, intlistF_out_ga(.(0, T52), T42)) → pD_out_gaa(T51, T52, T42)
U3_gga(T51, T42, pD_out_gaa(T51, X83, T42)) → intA_out_gga(s(0), s(s(T51)), T42)
U8_gaa(T19, T22, T21, intA_out_gga(0, T19, T22)) → U9_gaa(T19, T22, T21, intlistF_in_ga(T22, T21))
U9_gaa(T19, T22, T21, intlistF_out_ga(T22, T21)) → pB_out_gaa(T19, T22, T21)
U1_gga(T19, T21, pB_out_gaa(T19, X31, T21)) → intA_out_gga(0, s(T19), .(0, T21))

The argument filtering Pi contains the following mapping:
intA_in_gga(x1, x2, x3)  =  intA_in_gga(x1, x2)
0  =  0
intA_out_gga(x1, x2, x3)  =  intA_out_gga(x1, x2, x3)
s(x1)  =  s(x1)
U1_gga(x1, x2, x3)  =  U1_gga(x1, x3)
pB_in_gaa(x1, x2, x3)  =  pB_in_gaa(x1)
U8_gaa(x1, x2, x3, x4)  =  U8_gaa(x1, x4)
U2_gga(x1, x2)  =  U2_gga(x2)
intlistC_in_a(x1)  =  intlistC_in_a
intlistC_out_a(x1)  =  intlistC_out_a(x1)
U3_gga(x1, x2, x3)  =  U3_gga(x1, x3)
pD_in_gaa(x1, x2, x3)  =  pD_in_gaa(x1)
U10_gaa(x1, x2, x3, x4)  =  U10_gaa(x1, x4)
U4_gga(x1, x2, x3)  =  U4_gga(x1, x3)
U5_gga(x1, x2, x3, x4)  =  U5_gga(x1, x2, x4)
pE_in_ggaaa(x1, x2, x3, x4, x5)  =  pE_in_ggaaa(x1, x2)
U12_ggaaa(x1, x2, x3, x4, x5, x6)  =  U12_ggaaa(x1, x2, x6)
U13_ggaaa(x1, x2, x3, x4, x5, x6)  =  U13_ggaaa(x1, x2, x3, x6)
pH_in_gaa(x1, x2, x3)  =  pH_in_gaa(x1)
U14_gaa(x1, x2, x3, x4)  =  U14_gaa(x1, x4)
intlistG_in_ga(x1, x2)  =  intlistG_in_ga(x1)
[]  =  []
intlistG_out_ga(x1, x2)  =  intlistG_out_ga(x1, x2)
.(x1, x2)  =  .(x1, x2)
U7_ga(x1, x2, x3, x4)  =  U7_ga(x1, x2, x4)
U15_gaa(x1, x2, x3, x4)  =  U15_gaa(x1, x2, x4)
intlistF_in_ga(x1, x2)  =  intlistF_in_ga(x1)
intlistF_out_ga(x1, x2)  =  intlistF_out_ga(x1, x2)
U6_ga(x1, x2, x3, x4)  =  U6_ga(x1, x2, x4)
pH_out_gaa(x1, x2, x3)  =  pH_out_gaa(x1, x2, x3)
pE_out_ggaaa(x1, x2, x3, x4, x5)  =  pE_out_ggaaa(x1, x2, x3, x4, x5)
U11_gaa(x1, x2, x3, x4)  =  U11_gaa(x1, x2, x4)
pD_out_gaa(x1, x2, x3)  =  pD_out_gaa(x1, x2, x3)
U9_gaa(x1, x2, x3, x4)  =  U9_gaa(x1, x2, x4)
pB_out_gaa(x1, x2, x3)  =  pB_out_gaa(x1, x2, x3)
INTA_IN_GGA(x1, x2, x3)  =  INTA_IN_GGA(x1, x2)
PE_IN_GGAAA(x1, x2, x3, x4, x5)  =  PE_IN_GGAAA(x1, x2)

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

(38) UsableRulesProof (EQUIVALENT transformation)

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

(39) Obligation:

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

INTA_IN_GGA(s(s(T62)), s(s(T63)), T42) → PE_IN_GGAAA(T62, T63, X101, X102, T42)
PE_IN_GGAAA(T62, T63, T64, X102, T42) → INTA_IN_GGA(T62, T63, T64)

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

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

(40) PiDPToQDPProof (SOUND transformation)

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

(41) Obligation:

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

INTA_IN_GGA(s(s(T62)), s(s(T63))) → PE_IN_GGAAA(T62, T63)
PE_IN_GGAAA(T62, T63) → INTA_IN_GGA(T62, T63)

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

(42) QDPSizeChangeProof (EQUIVALENT transformation)

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

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

• PE_IN_GGAAA(T62, T63) → INTA_IN_GGA(T62, T63)
  The graph contains the following edges 1 >= 1, 2 >= 2

• INTA_IN_GGA(s(s(T62)), s(s(T63))) → PE_IN_GGAAA(T62, T63)
  The graph contains the following edges 1 > 1, 2 > 2

(43) YES