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

(0) Obligation:

Clauses:

goal(X) :- ','(s2l(X, Xs), append(Xs, X1, X2)).
append([], Y, Z) :- ','(!, eq(Y, Z)).
append(X, Y, .(H, Z)) :- ','(head(X, H), ','(tail(X, T), append(T, Y, Z))).
s2l(0, L) :- ','(!, eq(L, [])).
s2l(X, .(X3, Xs)) :- ','(p(X, P), s2l(P, Xs)).
head([], X4).
head(.(H, X5), H).
tail([], []).
tail(.(X6, Xs), Xs).
p(0, 0).
p(s(X), X).
eq(X, X).

Query: goal(g)

(1) PrologToPiTRSViaGraphTransformerProof (SOUND transformation)

Transformed Prolog program to (Pi-)TRS.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
2 [label="A: goal(T1)\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
5 [label="5: goal(T1), SCOPE: 1, CLAUSE: 0\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
8 [label="8: ','(s2l(T3, X9), append(X9, X10, X11))\n\nT3 is ground\nX9 is free\nX10 is free\nX11 is free", fontsize=16, style=filled, fillcolor=lightyellow];
11 [label="11: ','(s2l(T3, X9), append(X9, X10, X11)), SCOPE: 2, CLAUSE: 3 | ','(s2l(T3, X9), append(X9, X10, X11)), SCOPE: 2, CLAUSE: 4\n\nT3 is ground\nX9 is free\nX10 is free\nX11 is free", fontsize=16, style=filled, fillcolor=lightyellow];
13 [label="13: ','(','(!_2, eq(X17, [])), append(X17, X10, X11)) | ','(s2l(0, X9), append(X9, X10, X11)), SCOPE: 2, CLAUSE: 4\n\nX9 is free\nX10 is free\nX11 is free\nX17 is free", fontsize=16, style=filled, fillcolor=lightyellow];
15 [label="15: ','(s2l(T3, X9), append(X9, X10, X11)), SCOPE: 2, CLAUSE: 4\n\nT3 is ground\nX9 is free\nX10 is free\nX11 is free\nX16 is free\ns2l(T3, X9) !=? s2l(0, X16)", fontsize=16, style=filled, fillcolor=lightyellow];
16 [label="16: ','(eq(X17, []), append(X17, X10, X11))\n\nX10 is free\nX11 is free\nX17 is free", fontsize=16, style=filled, fillcolor=lightyellow];
19 [label="19: ','(eq(X17, []), append(X17, X10, X11)), SCOPE: 3, CLAUSE: 11\n\nX10 is free\nX11 is free\nX17 is free", fontsize=16, style=filled, fillcolor=lightyellow];
24 [label="B: append([], X10, X11)\n\nX10 is free\nX11 is free", fontsize=16, style=filled, fillcolor=lightyellow];
29 [label="29: append([], X10, X11), SCOPE: 4, CLAUSE: 1 | append([], X10, X11), SCOPE: 4, CLAUSE: 2\n\nX10 is free\nX11 is free", fontsize=16, style=filled, fillcolor=lightyellow];
33 [label="33: ','(!_4, eq(X46, X47)) | append([], X10, X11), SCOPE: 4, CLAUSE: 2\n\nX10 is free\nX11 is free\nX46 is free\nX47 is free", fontsize=16, style=filled, fillcolor=lightyellow];
34 [label="34: eq(X46, X47)\n\nX46 is free\nX47 is free", fontsize=16, style=filled, fillcolor=lightyellow];
35 [label="35: eq(X46, X47), SCOPE: 5, CLAUSE: 11\n\nX46 is free\nX47 is free", fontsize=16, style=filled, fillcolor=lightyellow];
44 [label="44: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
45 [label="45: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
49 [label="49: ','(','(p(T6, X70), s2l(X70, X72)), append(.(X71, X72), X10, X11))\n\nT6 is ground\nX9 is free\nX10 is free\nX11 is free\nX16 is free\nX71 is free\nX72 is free\nX70 is free\ns2l(T6, X9) !=? s2l(0, X16)", fontsize=16, style=filled, fillcolor=lightyellow];
52 [label="52: ','(','(p(T6, X70), s2l(X70, X72)), append(.(X71, X72), X10, X11)), SCOPE: 6, CLAUSE: 9 | ','(','(p(T6, X70), s2l(X70, X72)), append(.(X71, X72), X10, X11)), SCOPE: 6, CLAUSE: 10\n\nT6 is ground\nX9 is free\nX10 is free\nX11 is free\nX16 is free\nX71 is free\nX72 is free\nX70 is free\ns2l(T6, X9) !=? s2l(0, X16)", fontsize=16, style=filled, fillcolor=lightyellow];
53 [label="53: ','(','(p(T6, X70), s2l(X70, X72)), append(.(X71, X72), X10, X11)), SCOPE: 6, CLAUSE: 10\n\nT6 is ground\nX9 is free\nX10 is free\nX11 is free\nX16 is free\nX71 is free\nX72 is free\nX70 is free\ns2l(T6, X9) !=? s2l(0, X16)", fontsize=16, style=filled, fillcolor=lightyellow];
56 [label="C: ','(s2l(T9, X72), append(.(X71, X72), X10, X11))\n\nT9 is ground\nX10 is free\nX11 is free\nX71 is free\nX72 is free", fontsize=16, style=filled, fillcolor=lightyellow];
57 [label="57: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
61 [label="D: s2l(T9, X72)\n\nT9 is ground\nX72 is free", fontsize=16, style=filled, fillcolor=lightyellow];
62 [label="F: append(.(X71, T10), X10, X11)\n\nX10 is free\nX11 is free\nX71 is free", fontsize=16, style=filled, fillcolor=lightyellow];
63 [label="63: s2l(T9, X72), SCOPE: 7, CLAUSE: 3 | s2l(T9, X72), SCOPE: 7, CLAUSE: 4\n\nT9 is ground\nX72 is free", fontsize=16, style=filled, fillcolor=lightyellow];
64 [label="64: ','(!_7, eq(X87, [])) | s2l(0, X72), SCOPE: 7, CLAUSE: 4\n\nX72 is free\nX87 is free", fontsize=16, style=filled, fillcolor=lightyellow];
65 [label="65: s2l(T9, X72), SCOPE: 7, CLAUSE: 4\n\nT9 is ground\nX72 is free\nX86 is free\ns2l(T9, X72) !=? s2l(0, X86)", fontsize=16, style=filled, fillcolor=lightyellow];
67 [label="67: eq(X87, [])\n\nX87 is free", fontsize=16, style=filled, fillcolor=lightyellow];
68 [label="68: eq(X87, []), SCOPE: 8, CLAUSE: 11\n\nX87 is free", fontsize=16, style=filled, fillcolor=lightyellow];
72 [label="72: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
73 [label="73: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
83 [label="83: ','(p(T13, X110), s2l(X110, X112))\n\nT13 is ground\nX72 is free\nX86 is free\nX112 is free\nX110 is free\ns2l(T13, X72) !=? s2l(0, X86)", fontsize=16, style=filled, fillcolor=lightyellow];
84 [label="84: ','(p(T13, X110), s2l(X110, X112)), SCOPE: 9, CLAUSE: 9 | ','(p(T13, X110), s2l(X110, X112)), SCOPE: 9, CLAUSE: 10\n\nT13 is ground\nX72 is free\nX86 is free\nX112 is free\nX110 is free\ns2l(T13, X72) !=? s2l(0, X86)", fontsize=16, style=filled, fillcolor=lightyellow];
85 [label="85: ','(p(T13, X110), s2l(X110, X112)), SCOPE: 9, CLAUSE: 10\n\nT13 is ground\nX72 is free\nX86 is free\nX112 is free\nX110 is free\ns2l(T13, X72) !=? s2l(0, X86)", fontsize=16, style=filled, fillcolor=lightyellow];
86 [label="86: s2l(T16, X112)\n\nT16 is ground\nX112 is free", fontsize=16, style=filled, fillcolor=lightyellow];
87 [label="87: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
91 [label="91: append(.(X71, T10), X10, X11), SCOPE: 10, CLAUSE: 1 | append(.(X71, T10), X10, X11), SCOPE: 10, CLAUSE: 2\n\nX10 is free\nX11 is free\nX71 is free", fontsize=16, style=filled, fillcolor=lightyellow];
92 [label="92: append(.(X71, T10), X10, X11), SCOPE: 10, CLAUSE: 2\n\nX10 is free\nX11 is free\nX71 is free", fontsize=16, style=filled, fillcolor=lightyellow];
97 [label="97: ','(head(.(X150, T21), X152), ','(tail(.(X150, T21), X149), append(X149, X151, X153)))\n\nX150 is free\nX151 is free\nX152 is free\nX153 is free\nX149 is free", fontsize=16, style=filled, fillcolor=lightyellow];
98 [label="98: ','(head(.(X150, T21), X152), ','(tail(.(X150, T21), X149), append(X149, X151, X153))), SCOPE: 11, CLAUSE: 5 | ','(head(.(X150, T21), X152), ','(tail(.(X150, T21), X149), append(X149, X151, X153))), SCOPE: 11, CLAUSE: 6\n\nX150 is free\nX151 is free\nX152 is free\nX153 is free\nX149 is free", fontsize=16, style=filled, fillcolor=lightyellow];
99 [label="99: ','(head(.(X150, T21), X152), ','(tail(.(X150, T21), X149), append(X149, X151, X153))), SCOPE: 11, CLAUSE: 6\n\nX150 is free\nX151 is free\nX152 is free\nX153 is free\nX149 is free", fontsize=16, style=filled, fillcolor=lightyellow];
107 [label="107: ','(tail(.(X171, T26), X149), append(X149, X151, X153))\n\nX151 is free\nX153 is free\nX149 is free\nX171 is free", fontsize=16, style=filled, fillcolor=lightyellow];
108 [label="108: ','(tail(.(X171, T26), X149), append(X149, X151, X153)), SCOPE: 12, CLAUSE: 7 | ','(tail(.(X171, T26), X149), append(X149, X151, X153)), SCOPE: 12, CLAUSE: 8\n\nX151 is free\nX153 is free\nX149 is free\nX171 is free", fontsize=16, style=filled, fillcolor=lightyellow];
110 [label="110: ','(tail(.(X171, T26), X149), append(X149, X151, X153)), SCOPE: 12, CLAUSE: 8\n\nX151 is free\nX153 is free\nX149 is free\nX171 is free", fontsize=16, style=filled, fillcolor=lightyellow];
118 [label="E: append(T31, X151, X153)\n\nX151 is free\nX153 is free", fontsize=16, style=filled, fillcolor=lightyellow];
119 [label="119: append(T31, X151, X153), SCOPE: 13, CLAUSE: 1 | append(T31, X151, X153), SCOPE: 13, CLAUSE: 2\n\nX151 is free\nX153 is free", fontsize=16, style=filled, fillcolor=lightyellow];
122 [label="122: ','(!_13, eq(X203, X204)) | append(T31, X151, X153), SCOPE: 13, CLAUSE: 2\n\nX151 is free\nX153 is free\nX203 is free\nX204 is free", fontsize=16, style=filled, fillcolor=lightyellow];
123 [label="123: append(T31, X151, X153), SCOPE: 13, CLAUSE: 2\n\nX151 is free\nX153 is free\nX201 is free\nX202 is free\nappend(T31, X151, X153) !=? append([], X201, X202)", fontsize=16, style=filled, fillcolor=lightyellow];
124 [label="124: eq(X203, X204)\n\nX203 is free\nX204 is free", fontsize=16, style=filled, fillcolor=lightyellow];
125 [label="125: eq(X203, X204), SCOPE: 14, CLAUSE: 11\n\nX203 is free\nX204 is free", fontsize=16, style=filled, fillcolor=lightyellow];
129 [label="129: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
131 [label="131: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
142 [label="142: ','(head(T36, X236), ','(tail(T36, X234), append(X234, X235, X237)))\n\nX235 is free\nX236 is free\nX237 is free\nX234 is free", fontsize=16, style=filled, fillcolor=lightyellow];
143 [label="143: ','(head(T36, X236), ','(tail(T36, X234), append(X234, X235, X237))), SCOPE: 15, CLAUSE: 5 | ','(head(T36, X236), ','(tail(T36, X234), append(X234, X235, X237))), SCOPE: 15, CLAUSE: 6\n\nX235 is free\nX236 is free\nX237 is free\nX234 is free", fontsize=16, style=filled, fillcolor=lightyellow];
145 [label="145: ','(head(T36, X236), ','(tail(T36, X234), append(X234, X235, X237))), SCOPE: 15, CLAUSE: 5\n\nX235 is free\nX236 is free\nX237 is free\nX234 is free", fontsize=16, style=filled, fillcolor=lightyellow];
146 [label="146: ','(head(T36, X236), ','(tail(T36, X234), append(X234, X235, X237))), SCOPE: 15, CLAUSE: 6\n\nX235 is free\nX236 is free\nX237 is free\nX234 is free", fontsize=16, style=filled, fillcolor=lightyellow];
149 [label="149: ','(tail([], X234), append(X234, X235, X237))\n\nX235 is free\nX237 is free\nX234 is free", fontsize=16, style=filled, fillcolor=lightyellow];
151 [label="151: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
152 [label="152: ','(tail([], X234), append(X234, X235, X237)), SCOPE: 16, CLAUSE: 7 | ','(tail([], X234), append(X234, X235, X237)), SCOPE: 16, CLAUSE: 8\n\nX235 is free\nX237 is free\nX234 is free", fontsize=16, style=filled, fillcolor=lightyellow];
157 [label="157: ','(tail([], X234), append(X234, X235, X237)), SCOPE: 16, CLAUSE: 7\n\nX235 is free\nX237 is free\nX234 is free", fontsize=16, style=filled, fillcolor=lightyellow];
158 [label="158: ','(tail([], X234), append(X234, X235, X237)), SCOPE: 16, CLAUSE: 8\n\nX235 is free\nX237 is free\nX234 is free", fontsize=16, style=filled, fillcolor=lightyellow];
162 [label="162: append([], X235, X237)\n\nX235 is free\nX237 is free", fontsize=16, style=filled, fillcolor=lightyellow];
165 [label="165: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
168 [label="168: ','(tail(.(T43, T44), X234), append(X234, X235, X237))\n\nX235 is free\nX237 is free\nX234 is free", fontsize=16, style=filled, fillcolor=lightyellow];
169 [label="169: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
171 [label="171: ','(tail(.(T43, T44), X234), append(X234, X235, X237)), SCOPE: 17, CLAUSE: 7 | ','(tail(.(T43, T44), X234), append(X234, X235, X237)), SCOPE: 17, CLAUSE: 8\n\nX235 is free\nX237 is free\nX234 is free", fontsize=16, style=filled, fillcolor=lightyellow];
172 [label="172: ','(tail(.(T43, T44), X234), append(X234, X235, X237)), SCOPE: 17, CLAUSE: 8\n\nX235 is free\nX237 is free\nX234 is free", fontsize=16, style=filled, fillcolor=lightyellow];
177 [label="177: append(T52, X235, X237)\n\nX235 is free\nX237 is free", fontsize=16, style=filled, fillcolor=lightyellow];
178 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
2 -> 178 [arrowhead = none ];
178 -> 5;

179 [label="ONLY EVAL with clause\ngoal(X8) :- ','(s2l(X8, X9), append(X9, X10, X11)).\nand substitutionT1 -> T3,\nX8 -> T3", fontsize=14, style = filled, fillcolor = lightblue];
5 -> 179 [arrowhead = none ];
179 -> 8;

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

181 [label="EVAL with clause\ns2l(0, X16) :- ','(!_2, eq(X16, [])).\nand substitutionT3 -> 0,\nX9 -> X17,\nX16 -> X17", fontsize=14, style = filled, fillcolor = lightblue];
11 -> 181 [arrowhead = none ];
181 -> 13;

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

183 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
13 -> 183 [arrowhead = none ];
183 -> 16;

184 [label="ONLY EVAL with clause\ns2l(X67, .(X68, X69)) :- ','(p(X67, X70), s2l(X70, X69)).\nand substitutionT3 -> T6,\nX67 -> T6,\nX68 -> X71,\nX69 -> X72,\nX9 -> .(X71, X72)", fontsize=14, style = filled, fillcolor = lightblue];
15 -> 184 [arrowhead = none ];
184 -> 49;

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

186 [label="ONLY EVAL with clause\neq(X30, X30).\nand substitutionX17 -> [],\nX30 -> [],\nX31 -> []", fontsize=14, style = filled, fillcolor = lightblue];
19 -> 186 [arrowhead = none ];
186 -> 24;

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

188 [label="ONLY EVAL with clause\nappend([], X44, X45) :- ','(!_4, eq(X44, X45)).\nand substitutionX10 -> X46,\nX44 -> X46,\nX11 -> X47,\nX45 -> X47", fontsize=14, style = filled, fillcolor = lightblue];
29 -> 188 [arrowhead = none ];
188 -> 33;

189 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
33 -> 189 [arrowhead = none ];
189 -> 34;

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

191 [label="ONLY EVAL with clause\neq(X52, X52).\nand substitutionX46 -> X53,\nX52 -> X53,\nX47 -> X53", fontsize=14, style = filled, fillcolor = lightblue];
35 -> 191 [arrowhead = none ];
191 -> 44;

192 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
44 -> 192 [arrowhead = none ];
192 -> 45;

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

194 [label="BACKTRACK\nfor clause: p(0, 0)\nwith clash: (s2l(T6, X9), s2l(0, X16))", fontsize=14, style = filled, fillcolor = lightgreen];
52 -> 194 [arrowhead = none ];
194 -> 53;

195 [label="EVAL with clause\np(s(X77), X77).\nand substitutionX77 -> T9,\nT6 -> s(T9),\nX70 -> T9", fontsize=14, style = filled, fillcolor = lightblue];
53 -> 195 [arrowhead = none ];
195 -> 56;

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

197 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
56 -> 197 [arrowhead = none ];
197 -> 61;

198 [label="SPLIT 2\nnew knowledge:\nT9 is ground\nreplacements:X72 -> T10", fontsize=14, style = filled, fillcolor = violet];
56 -> 198 [arrowhead = none ];
198 -> 62;

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

200 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
62 -> 200 [arrowhead = none ];
200 -> 91;

201 [label="EVAL with clause\ns2l(0, X86) :- ','(!_7, eq(X86, [])).\nand substitutionT9 -> 0,\nX72 -> X87,\nX86 -> X87", fontsize=14, style = filled, fillcolor = lightblue];
63 -> 201 [arrowhead = none ];
201 -> 64;

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

203 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
64 -> 203 [arrowhead = none ];
203 -> 67;

204 [label="ONLY EVAL with clause\ns2l(X107, .(X108, X109)) :- ','(p(X107, X110), s2l(X110, X109)).\nand substitutionT9 -> T13,\nX107 -> T13,\nX108 -> X111,\nX109 -> X112,\nX72 -> .(X111, X112)", fontsize=14, style = filled, fillcolor = lightblue];
65 -> 204 [arrowhead = none ];
204 -> 83;

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

206 [label="ONLY EVAL with clause\neq(X92, X92).\nand substitutionX87 -> [],\nX92 -> [],\nX93 -> []", fontsize=14, style = filled, fillcolor = lightblue];
68 -> 206 [arrowhead = none ];
206 -> 72;

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

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

209 [label="BACKTRACK\nfor clause: p(0, 0)\nwith clash: (s2l(T13, X72), s2l(0, X86))", fontsize=14, style = filled, fillcolor = lightgreen];
84 -> 209 [arrowhead = none ];
209 -> 85;

210 [label="EVAL with clause\np(s(X117), X117).\nand substitutionX117 -> T16,\nT13 -> s(T16),\nX110 -> T16", fontsize=14, style = filled, fillcolor = lightblue];
85 -> 210 [arrowhead = none ];
210 -> 86;

211 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
85 -> 211 [arrowhead = none ];
211 -> 87;

212 [label="INSTANCE with matching:\nT9 -> T16\nX72 -> X112", fontsize=14, style = filled, fillcolor = lightgrey];
86 -> 212 [arrowhead = none , style=dashed];
212 -> 61[style=dashed];

213 [label="BACKTRACK\nfor clause: append([], Y, Z) :- ','(!, eq(Y, Z))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
91 -> 213 [arrowhead = none ];
213 -> 92;

214 [label="ONLY EVAL with clause\nappend(X145, X146, .(X147, X148)) :- ','(head(X145, X147), ','(tail(X145, X149), append(X149, X146, X148))).\nand substitutionX71 -> X150,\nT10 -> T21,\nX145 -> .(X150, T21),\nX10 -> X151,\nX146 -> X151,\nX147 -> X152,\nX148 -> X153,\nX11 -> .(X152, X153),\nT20 -> T21", fontsize=14, style = filled, fillcolor = lightblue];
92 -> 214 [arrowhead = none ];
214 -> 97;

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

216 [label="BACKTRACK\nfor clause: head([], X4)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
98 -> 216 [arrowhead = none ];
216 -> 99;

217 [label="ONLY EVAL with clause\nhead(.(X169, X170), X169).\nand substitutionX150 -> X171,\nX169 -> X171,\nT21 -> T26,\nX170 -> T26,\nX152 -> X171,\nT25 -> T26", fontsize=14, style = filled, fillcolor = lightblue];
99 -> 217 [arrowhead = none ];
217 -> 107;

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

219 [label="BACKTRACK\nfor clause: tail([], [])because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
108 -> 219 [arrowhead = none ];
219 -> 110;

220 [label="ONLY EVAL with clause\ntail(.(X186, X187), X187).\nand substitutionX171 -> X188,\nX186 -> X188,\nT26 -> T31,\nX187 -> T31,\nX149 -> T31,\nT30 -> T31", fontsize=14, style = filled, fillcolor = lightblue];
110 -> 220 [arrowhead = none ];
220 -> 118;

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

222 [label="EVAL with clause\nappend([], X201, X202) :- ','(!_13, eq(X201, X202)).\nand substitutionT31 -> [],\nX151 -> X203,\nX201 -> X203,\nX153 -> X204,\nX202 -> X204", fontsize=14, style = filled, fillcolor = lightblue];
119 -> 222 [arrowhead = none ];
222 -> 122;

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

224 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
122 -> 224 [arrowhead = none ];
224 -> 124;

225 [label="ONLY EVAL with clause\nappend(X230, X231, .(X232, X233)) :- ','(head(X230, X232), ','(tail(X230, X234), append(X234, X231, X233))).\nand substitutionT31 -> T36,\nX230 -> T36,\nX151 -> X235,\nX231 -> X235,\nX232 -> X236,\nX233 -> X237,\nX153 -> .(X236, X237),\nT35 -> T36", fontsize=14, style = filled, fillcolor = lightblue];
123 -> 225 [arrowhead = none ];
225 -> 142;

226 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
124 -> 226 [arrowhead = none ];
226 -> 125;

227 [label="ONLY EVAL with clause\neq(X209, X209).\nand substitutionX203 -> X210,\nX209 -> X210,\nX204 -> X210", fontsize=14, style = filled, fillcolor = lightblue];
125 -> 227 [arrowhead = none ];
227 -> 129;

228 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
129 -> 228 [arrowhead = none ];
228 -> 131;

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

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

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

232 [label="EVAL with clause\nhead([], X250).\nand substitutionT36 -> [],\nX236 -> X251,\nX250 -> X251", fontsize=14, style = filled, fillcolor = lightblue];
145 -> 232 [arrowhead = none ];
232 -> 149;

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

234 [label="EVAL with clause\nhead(.(X274, X275), X274).\nand substitutionX274 -> T43,\nX275 -> T44,\nT36 -> .(T43, T44),\nX236 -> T43,\nT41 -> T43,\nT42 -> T44", fontsize=14, style = filled, fillcolor = lightblue];
146 -> 234 [arrowhead = none ];
234 -> 168;

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

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

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

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

239 [label="ONLY EVAL with clause\ntail([], []).\nand substitutionX234 -> []", fontsize=14, style = filled, fillcolor = lightblue];
157 -> 239 [arrowhead = none ];
239 -> 162;

240 [label="BACKTRACK\nfor clause: tail(.(X6, Xs), Xs)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
158 -> 240 [arrowhead = none ];
240 -> 165;

241 [label="INSTANCE with matching:\nX10 -> X235\nX11 -> X237", fontsize=14, style = filled, fillcolor = lightgrey];
162 -> 241 [arrowhead = none , style=dashed];
241 -> 24[style=dashed];

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

243 [label="BACKTRACK\nfor clause: tail([], [])because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
171 -> 243 [arrowhead = none ];
243 -> 172;

244 [label="ONLY EVAL with clause\ntail(.(X288, X289), X289).\nand substitutionT43 -> T50,\nX288 -> T50,\nT44 -> T52,\nX289 -> T52,\nX234 -> T52,\nT51 -> T52", fontsize=14, style = filled, fillcolor = lightblue];
172 -> 244 [arrowhead = none ];
244 -> 177;

245 [label="INSTANCE with matching:\nT31 -> T52\nX151 -> X235\nX153 -> X237", fontsize=14, style = filled, fillcolor = lightgrey];
177 -> 245 [arrowhead = none , style=dashed];
245 -> 118[style=dashed];

}

(2) Obligation:

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

goalA_in_g(0) → U1_g(appendB_in_aa(X10, X11))
appendB_in_aa(X53, X53) → appendB_out_aa(X53, X53)
U1_g(appendB_out_aa(X10, X11)) → goalA_out_g(0)
goalA_in_g(s(T9)) → U2_g(T9, pC_in_gaaaa(T9, X72, X71, X10, X11))
pC_in_gaaaa(T9, T10, X71, X10, X11) → U7_gaaaa(T9, T10, X71, X10, X11, s2lD_in_ga(T9, T10))
s2lD_in_ga(0, []) → s2lD_out_ga(0, [])
s2lD_in_ga(s(T16), .(X111, X112)) → U3_ga(T16, X111, X112, s2lD_in_ga(T16, X112))
U3_ga(T16, X111, X112, s2lD_out_ga(T16, X112)) → s2lD_out_ga(s(T16), .(X111, X112))
U7_gaaaa(T9, T10, X71, X10, X11, s2lD_out_ga(T9, T10)) → U8_gaaaa(T9, T10, X71, X10, X11, appendF_in_agaa(X71, T10, X10, X11))
appendF_in_agaa(X188, T31, X151, .(X188, X153)) → U6_agaa(X188, T31, X151, X153, appendE_in_gaa(T31, X151, X153))
appendE_in_gaa([], X210, X210) → appendE_out_gaa([], X210, X210)
appendE_in_gaa([], X235, .(X251, X237)) → U4_gaa(X235, X251, X237, appendB_in_aa(X235, X237))
U4_gaa(X235, X251, X237, appendB_out_aa(X235, X237)) → appendE_out_gaa([], X235, .(X251, X237))
appendE_in_gaa(.(T50, T52), X235, .(T50, X237)) → U5_gaa(T50, T52, X235, X237, appendE_in_gaa(T52, X235, X237))
U5_gaa(T50, T52, X235, X237, appendE_out_gaa(T52, X235, X237)) → appendE_out_gaa(.(T50, T52), X235, .(T50, X237))
U6_agaa(X188, T31, X151, X153, appendE_out_gaa(T31, X151, X153)) → appendF_out_agaa(X188, T31, X151, .(X188, X153))
U8_gaaaa(T9, T10, X71, X10, X11, appendF_out_agaa(X71, T10, X10, X11)) → pC_out_gaaaa(T9, T10, X71, X10, X11)
U2_g(T9, pC_out_gaaaa(T9, X72, X71, X10, X11)) → goalA_out_g(s(T9))

The argument filtering Pi contains the following mapping:
goalA_in_g(x1)  =  goalA_in_g(x1)
0  =  0
U1_g(x1)  =  U1_g(x1)
appendB_in_aa(x1, x2)  =  appendB_in_aa
appendB_out_aa(x1, x2)  =  appendB_out_aa
goalA_out_g(x1)  =  goalA_out_g(x1)
s(x1)  =  s(x1)
U2_g(x1, x2)  =  U2_g(x1, x2)
pC_in_gaaaa(x1, x2, x3, x4, x5)  =  pC_in_gaaaa(x1)
U7_gaaaa(x1, x2, x3, x4, x5, x6)  =  U7_gaaaa(x1, x6)
s2lD_in_ga(x1, x2)  =  s2lD_in_ga(x1)
s2lD_out_ga(x1, x2)  =  s2lD_out_ga(x1, x2)
U3_ga(x1, x2, x3, x4)  =  U3_ga(x1, x4)
.(x1, x2)  =  .(x2)
U8_gaaaa(x1, x2, x3, x4, x5, x6)  =  U8_gaaaa(x1, x2, x6)
appendF_in_agaa(x1, x2, x3, x4)  =  appendF_in_agaa(x2)
U6_agaa(x1, x2, x3, x4, x5)  =  U6_agaa(x2, x5)
appendE_in_gaa(x1, x2, x3)  =  appendE_in_gaa(x1)
[]  =  []
appendE_out_gaa(x1, x2, x3)  =  appendE_out_gaa(x1)
U4_gaa(x1, x2, x3, x4)  =  U4_gaa(x4)
U5_gaa(x1, x2, x3, x4, x5)  =  U5_gaa(x2, x5)
appendF_out_agaa(x1, x2, x3, x4)  =  appendF_out_agaa(x2)
pC_out_gaaaa(x1, x2, x3, x4, x5)  =  pC_out_gaaaa(x1, x2)

(3) DependencyPairsProof (EQUIVALENT transformation)

Using Dependency Pairs [AG00,LOPSTR] we result in the following initial DP problem:
Pi DP problem:
The TRS P consists of the following rules:

GOALA_IN_G(0) → U1_G(appendB_in_aa(X10, X11))
GOALA_IN_G(0) → APPENDB_IN_AA(X10, X11)
GOALA_IN_G(s(T9)) → U2_G(T9, pC_in_gaaaa(T9, X72, X71, X10, X11))
GOALA_IN_G(s(T9)) → PC_IN_GAAAA(T9, X72, X71, X10, X11)
PC_IN_GAAAA(T9, T10, X71, X10, X11) → U7_GAAAA(T9, T10, X71, X10, X11, s2lD_in_ga(T9, T10))
PC_IN_GAAAA(T9, T10, X71, X10, X11) → S2LD_IN_GA(T9, T10)
S2LD_IN_GA(s(T16), .(X111, X112)) → U3_GA(T16, X111, X112, s2lD_in_ga(T16, X112))
S2LD_IN_GA(s(T16), .(X111, X112)) → S2LD_IN_GA(T16, X112)
U7_GAAAA(T9, T10, X71, X10, X11, s2lD_out_ga(T9, T10)) → U8_GAAAA(T9, T10, X71, X10, X11, appendF_in_agaa(X71, T10, X10, X11))
U7_GAAAA(T9, T10, X71, X10, X11, s2lD_out_ga(T9, T10)) → APPENDF_IN_AGAA(X71, T10, X10, X11)
APPENDF_IN_AGAA(X188, T31, X151, .(X188, X153)) → U6_AGAA(X188, T31, X151, X153, appendE_in_gaa(T31, X151, X153))
APPENDF_IN_AGAA(X188, T31, X151, .(X188, X153)) → APPENDE_IN_GAA(T31, X151, X153)
APPENDE_IN_GAA([], X235, .(X251, X237)) → U4_GAA(X235, X251, X237, appendB_in_aa(X235, X237))
APPENDE_IN_GAA([], X235, .(X251, X237)) → APPENDB_IN_AA(X235, X237)
APPENDE_IN_GAA(.(T50, T52), X235, .(T50, X237)) → U5_GAA(T50, T52, X235, X237, appendE_in_gaa(T52, X235, X237))
APPENDE_IN_GAA(.(T50, T52), X235, .(T50, X237)) → APPENDE_IN_GAA(T52, X235, X237)

The TRS R consists of the following rules:

goalA_in_g(0) → U1_g(appendB_in_aa(X10, X11))
appendB_in_aa(X53, X53) → appendB_out_aa(X53, X53)
U1_g(appendB_out_aa(X10, X11)) → goalA_out_g(0)
goalA_in_g(s(T9)) → U2_g(T9, pC_in_gaaaa(T9, X72, X71, X10, X11))
pC_in_gaaaa(T9, T10, X71, X10, X11) → U7_gaaaa(T9, T10, X71, X10, X11, s2lD_in_ga(T9, T10))
s2lD_in_ga(0, []) → s2lD_out_ga(0, [])
s2lD_in_ga(s(T16), .(X111, X112)) → U3_ga(T16, X111, X112, s2lD_in_ga(T16, X112))
U3_ga(T16, X111, X112, s2lD_out_ga(T16, X112)) → s2lD_out_ga(s(T16), .(X111, X112))
U7_gaaaa(T9, T10, X71, X10, X11, s2lD_out_ga(T9, T10)) → U8_gaaaa(T9, T10, X71, X10, X11, appendF_in_agaa(X71, T10, X10, X11))
appendF_in_agaa(X188, T31, X151, .(X188, X153)) → U6_agaa(X188, T31, X151, X153, appendE_in_gaa(T31, X151, X153))
appendE_in_gaa([], X210, X210) → appendE_out_gaa([], X210, X210)
appendE_in_gaa([], X235, .(X251, X237)) → U4_gaa(X235, X251, X237, appendB_in_aa(X235, X237))
U4_gaa(X235, X251, X237, appendB_out_aa(X235, X237)) → appendE_out_gaa([], X235, .(X251, X237))
appendE_in_gaa(.(T50, T52), X235, .(T50, X237)) → U5_gaa(T50, T52, X235, X237, appendE_in_gaa(T52, X235, X237))
U5_gaa(T50, T52, X235, X237, appendE_out_gaa(T52, X235, X237)) → appendE_out_gaa(.(T50, T52), X235, .(T50, X237))
U6_agaa(X188, T31, X151, X153, appendE_out_gaa(T31, X151, X153)) → appendF_out_agaa(X188, T31, X151, .(X188, X153))
U8_gaaaa(T9, T10, X71, X10, X11, appendF_out_agaa(X71, T10, X10, X11)) → pC_out_gaaaa(T9, T10, X71, X10, X11)
U2_g(T9, pC_out_gaaaa(T9, X72, X71, X10, X11)) → goalA_out_g(s(T9))

The argument filtering Pi contains the following mapping:
goalA_in_g(x1)  =  goalA_in_g(x1)
0  =  0
U1_g(x1)  =  U1_g(x1)
appendB_in_aa(x1, x2)  =  appendB_in_aa
appendB_out_aa(x1, x2)  =  appendB_out_aa
goalA_out_g(x1)  =  goalA_out_g(x1)
s(x1)  =  s(x1)
U2_g(x1, x2)  =  U2_g(x1, x2)
pC_in_gaaaa(x1, x2, x3, x4, x5)  =  pC_in_gaaaa(x1)
U7_gaaaa(x1, x2, x3, x4, x5, x6)  =  U7_gaaaa(x1, x6)
s2lD_in_ga(x1, x2)  =  s2lD_in_ga(x1)
s2lD_out_ga(x1, x2)  =  s2lD_out_ga(x1, x2)
U3_ga(x1, x2, x3, x4)  =  U3_ga(x1, x4)
.(x1, x2)  =  .(x2)
U8_gaaaa(x1, x2, x3, x4, x5, x6)  =  U8_gaaaa(x1, x2, x6)
appendF_in_agaa(x1, x2, x3, x4)  =  appendF_in_agaa(x2)
U6_agaa(x1, x2, x3, x4, x5)  =  U6_agaa(x2, x5)
appendE_in_gaa(x1, x2, x3)  =  appendE_in_gaa(x1)
[]  =  []
appendE_out_gaa(x1, x2, x3)  =  appendE_out_gaa(x1)
U4_gaa(x1, x2, x3, x4)  =  U4_gaa(x4)
U5_gaa(x1, x2, x3, x4, x5)  =  U5_gaa(x2, x5)
appendF_out_agaa(x1, x2, x3, x4)  =  appendF_out_agaa(x2)
pC_out_gaaaa(x1, x2, x3, x4, x5)  =  pC_out_gaaaa(x1, x2)
GOALA_IN_G(x1)  =  GOALA_IN_G(x1)
U1_G(x1)  =  U1_G(x1)
APPENDB_IN_AA(x1, x2)  =  APPENDB_IN_AA
U2_G(x1, x2)  =  U2_G(x1, x2)
PC_IN_GAAAA(x1, x2, x3, x4, x5)  =  PC_IN_GAAAA(x1)
U7_GAAAA(x1, x2, x3, x4, x5, x6)  =  U7_GAAAA(x1, x6)
S2LD_IN_GA(x1, x2)  =  S2LD_IN_GA(x1)
U3_GA(x1, x2, x3, x4)  =  U3_GA(x1, x4)
U8_GAAAA(x1, x2, x3, x4, x5, x6)  =  U8_GAAAA(x1, x2, x6)
APPENDF_IN_AGAA(x1, x2, x3, x4)  =  APPENDF_IN_AGAA(x2)
U6_AGAA(x1, x2, x3, x4, x5)  =  U6_AGAA(x2, x5)
APPENDE_IN_GAA(x1, x2, x3)  =  APPENDE_IN_GAA(x1)
U4_GAA(x1, x2, x3, x4)  =  U4_GAA(x4)
U5_GAA(x1, x2, x3, x4, x5)  =  U5_GAA(x2, x5)

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

(4) Obligation:

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

GOALA_IN_G(0) → U1_G(appendB_in_aa(X10, X11))
GOALA_IN_G(0) → APPENDB_IN_AA(X10, X11)
GOALA_IN_G(s(T9)) → U2_G(T9, pC_in_gaaaa(T9, X72, X71, X10, X11))
GOALA_IN_G(s(T9)) → PC_IN_GAAAA(T9, X72, X71, X10, X11)
PC_IN_GAAAA(T9, T10, X71, X10, X11) → U7_GAAAA(T9, T10, X71, X10, X11, s2lD_in_ga(T9, T10))
PC_IN_GAAAA(T9, T10, X71, X10, X11) → S2LD_IN_GA(T9, T10)
S2LD_IN_GA(s(T16), .(X111, X112)) → U3_GA(T16, X111, X112, s2lD_in_ga(T16, X112))
S2LD_IN_GA(s(T16), .(X111, X112)) → S2LD_IN_GA(T16, X112)
U7_GAAAA(T9, T10, X71, X10, X11, s2lD_out_ga(T9, T10)) → U8_GAAAA(T9, T10, X71, X10, X11, appendF_in_agaa(X71, T10, X10, X11))
U7_GAAAA(T9, T10, X71, X10, X11, s2lD_out_ga(T9, T10)) → APPENDF_IN_AGAA(X71, T10, X10, X11)
APPENDF_IN_AGAA(X188, T31, X151, .(X188, X153)) → U6_AGAA(X188, T31, X151, X153, appendE_in_gaa(T31, X151, X153))
APPENDF_IN_AGAA(X188, T31, X151, .(X188, X153)) → APPENDE_IN_GAA(T31, X151, X153)
APPENDE_IN_GAA([], X235, .(X251, X237)) → U4_GAA(X235, X251, X237, appendB_in_aa(X235, X237))
APPENDE_IN_GAA([], X235, .(X251, X237)) → APPENDB_IN_AA(X235, X237)
APPENDE_IN_GAA(.(T50, T52), X235, .(T50, X237)) → U5_GAA(T50, T52, X235, X237, appendE_in_gaa(T52, X235, X237))
APPENDE_IN_GAA(.(T50, T52), X235, .(T50, X237)) → APPENDE_IN_GAA(T52, X235, X237)

The TRS R consists of the following rules:

goalA_in_g(0) → U1_g(appendB_in_aa(X10, X11))
appendB_in_aa(X53, X53) → appendB_out_aa(X53, X53)
U1_g(appendB_out_aa(X10, X11)) → goalA_out_g(0)
goalA_in_g(s(T9)) → U2_g(T9, pC_in_gaaaa(T9, X72, X71, X10, X11))
pC_in_gaaaa(T9, T10, X71, X10, X11) → U7_gaaaa(T9, T10, X71, X10, X11, s2lD_in_ga(T9, T10))
s2lD_in_ga(0, []) → s2lD_out_ga(0, [])
s2lD_in_ga(s(T16), .(X111, X112)) → U3_ga(T16, X111, X112, s2lD_in_ga(T16, X112))
U3_ga(T16, X111, X112, s2lD_out_ga(T16, X112)) → s2lD_out_ga(s(T16), .(X111, X112))
U7_gaaaa(T9, T10, X71, X10, X11, s2lD_out_ga(T9, T10)) → U8_gaaaa(T9, T10, X71, X10, X11, appendF_in_agaa(X71, T10, X10, X11))
appendF_in_agaa(X188, T31, X151, .(X188, X153)) → U6_agaa(X188, T31, X151, X153, appendE_in_gaa(T31, X151, X153))
appendE_in_gaa([], X210, X210) → appendE_out_gaa([], X210, X210)
appendE_in_gaa([], X235, .(X251, X237)) → U4_gaa(X235, X251, X237, appendB_in_aa(X235, X237))
U4_gaa(X235, X251, X237, appendB_out_aa(X235, X237)) → appendE_out_gaa([], X235, .(X251, X237))
appendE_in_gaa(.(T50, T52), X235, .(T50, X237)) → U5_gaa(T50, T52, X235, X237, appendE_in_gaa(T52, X235, X237))
U5_gaa(T50, T52, X235, X237, appendE_out_gaa(T52, X235, X237)) → appendE_out_gaa(.(T50, T52), X235, .(T50, X237))
U6_agaa(X188, T31, X151, X153, appendE_out_gaa(T31, X151, X153)) → appendF_out_agaa(X188, T31, X151, .(X188, X153))
U8_gaaaa(T9, T10, X71, X10, X11, appendF_out_agaa(X71, T10, X10, X11)) → pC_out_gaaaa(T9, T10, X71, X10, X11)
U2_g(T9, pC_out_gaaaa(T9, X72, X71, X10, X11)) → goalA_out_g(s(T9))

The argument filtering Pi contains the following mapping:
goalA_in_g(x1)  =  goalA_in_g(x1)
0  =  0
U1_g(x1)  =  U1_g(x1)
appendB_in_aa(x1, x2)  =  appendB_in_aa
appendB_out_aa(x1, x2)  =  appendB_out_aa
goalA_out_g(x1)  =  goalA_out_g(x1)
s(x1)  =  s(x1)
U2_g(x1, x2)  =  U2_g(x1, x2)
pC_in_gaaaa(x1, x2, x3, x4, x5)  =  pC_in_gaaaa(x1)
U7_gaaaa(x1, x2, x3, x4, x5, x6)  =  U7_gaaaa(x1, x6)
s2lD_in_ga(x1, x2)  =  s2lD_in_ga(x1)
s2lD_out_ga(x1, x2)  =  s2lD_out_ga(x1, x2)
U3_ga(x1, x2, x3, x4)  =  U3_ga(x1, x4)
.(x1, x2)  =  .(x2)
U8_gaaaa(x1, x2, x3, x4, x5, x6)  =  U8_gaaaa(x1, x2, x6)
appendF_in_agaa(x1, x2, x3, x4)  =  appendF_in_agaa(x2)
U6_agaa(x1, x2, x3, x4, x5)  =  U6_agaa(x2, x5)
appendE_in_gaa(x1, x2, x3)  =  appendE_in_gaa(x1)
[]  =  []
appendE_out_gaa(x1, x2, x3)  =  appendE_out_gaa(x1)
U4_gaa(x1, x2, x3, x4)  =  U4_gaa(x4)
U5_gaa(x1, x2, x3, x4, x5)  =  U5_gaa(x2, x5)
appendF_out_agaa(x1, x2, x3, x4)  =  appendF_out_agaa(x2)
pC_out_gaaaa(x1, x2, x3, x4, x5)  =  pC_out_gaaaa(x1, x2)
GOALA_IN_G(x1)  =  GOALA_IN_G(x1)
U1_G(x1)  =  U1_G(x1)
APPENDB_IN_AA(x1, x2)  =  APPENDB_IN_AA
U2_G(x1, x2)  =  U2_G(x1, x2)
PC_IN_GAAAA(x1, x2, x3, x4, x5)  =  PC_IN_GAAAA(x1)
U7_GAAAA(x1, x2, x3, x4, x5, x6)  =  U7_GAAAA(x1, x6)
S2LD_IN_GA(x1, x2)  =  S2LD_IN_GA(x1)
U3_GA(x1, x2, x3, x4)  =  U3_GA(x1, x4)
U8_GAAAA(x1, x2, x3, x4, x5, x6)  =  U8_GAAAA(x1, x2, x6)
APPENDF_IN_AGAA(x1, x2, x3, x4)  =  APPENDF_IN_AGAA(x2)
U6_AGAA(x1, x2, x3, x4, x5)  =  U6_AGAA(x2, x5)
APPENDE_IN_GAA(x1, x2, x3)  =  APPENDE_IN_GAA(x1)
U4_GAA(x1, x2, x3, x4)  =  U4_GAA(x4)
U5_GAA(x1, x2, x3, x4, x5)  =  U5_GAA(x2, x5)

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

(5) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 2 SCCs with 14 less nodes.

(6) Complex Obligation (AND)

(7) Obligation:

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

APPENDE_IN_GAA(.(T50, T52), X235, .(T50, X237)) → APPENDE_IN_GAA(T52, X235, X237)

The TRS R consists of the following rules:

goalA_in_g(0) → U1_g(appendB_in_aa(X10, X11))
appendB_in_aa(X53, X53) → appendB_out_aa(X53, X53)
U1_g(appendB_out_aa(X10, X11)) → goalA_out_g(0)
goalA_in_g(s(T9)) → U2_g(T9, pC_in_gaaaa(T9, X72, X71, X10, X11))
pC_in_gaaaa(T9, T10, X71, X10, X11) → U7_gaaaa(T9, T10, X71, X10, X11, s2lD_in_ga(T9, T10))
s2lD_in_ga(0, []) → s2lD_out_ga(0, [])
s2lD_in_ga(s(T16), .(X111, X112)) → U3_ga(T16, X111, X112, s2lD_in_ga(T16, X112))
U3_ga(T16, X111, X112, s2lD_out_ga(T16, X112)) → s2lD_out_ga(s(T16), .(X111, X112))
U7_gaaaa(T9, T10, X71, X10, X11, s2lD_out_ga(T9, T10)) → U8_gaaaa(T9, T10, X71, X10, X11, appendF_in_agaa(X71, T10, X10, X11))
appendF_in_agaa(X188, T31, X151, .(X188, X153)) → U6_agaa(X188, T31, X151, X153, appendE_in_gaa(T31, X151, X153))
appendE_in_gaa([], X210, X210) → appendE_out_gaa([], X210, X210)
appendE_in_gaa([], X235, .(X251, X237)) → U4_gaa(X235, X251, X237, appendB_in_aa(X235, X237))
U4_gaa(X235, X251, X237, appendB_out_aa(X235, X237)) → appendE_out_gaa([], X235, .(X251, X237))
appendE_in_gaa(.(T50, T52), X235, .(T50, X237)) → U5_gaa(T50, T52, X235, X237, appendE_in_gaa(T52, X235, X237))
U5_gaa(T50, T52, X235, X237, appendE_out_gaa(T52, X235, X237)) → appendE_out_gaa(.(T50, T52), X235, .(T50, X237))
U6_agaa(X188, T31, X151, X153, appendE_out_gaa(T31, X151, X153)) → appendF_out_agaa(X188, T31, X151, .(X188, X153))
U8_gaaaa(T9, T10, X71, X10, X11, appendF_out_agaa(X71, T10, X10, X11)) → pC_out_gaaaa(T9, T10, X71, X10, X11)
U2_g(T9, pC_out_gaaaa(T9, X72, X71, X10, X11)) → goalA_out_g(s(T9))

The argument filtering Pi contains the following mapping:
goalA_in_g(x1)  =  goalA_in_g(x1)
0  =  0
U1_g(x1)  =  U1_g(x1)
appendB_in_aa(x1, x2)  =  appendB_in_aa
appendB_out_aa(x1, x2)  =  appendB_out_aa
goalA_out_g(x1)  =  goalA_out_g(x1)
s(x1)  =  s(x1)
U2_g(x1, x2)  =  U2_g(x1, x2)
pC_in_gaaaa(x1, x2, x3, x4, x5)  =  pC_in_gaaaa(x1)
U7_gaaaa(x1, x2, x3, x4, x5, x6)  =  U7_gaaaa(x1, x6)
s2lD_in_ga(x1, x2)  =  s2lD_in_ga(x1)
s2lD_out_ga(x1, x2)  =  s2lD_out_ga(x1, x2)
U3_ga(x1, x2, x3, x4)  =  U3_ga(x1, x4)
.(x1, x2)  =  .(x2)
U8_gaaaa(x1, x2, x3, x4, x5, x6)  =  U8_gaaaa(x1, x2, x6)
appendF_in_agaa(x1, x2, x3, x4)  =  appendF_in_agaa(x2)
U6_agaa(x1, x2, x3, x4, x5)  =  U6_agaa(x2, x5)
appendE_in_gaa(x1, x2, x3)  =  appendE_in_gaa(x1)
[]  =  []
appendE_out_gaa(x1, x2, x3)  =  appendE_out_gaa(x1)
U4_gaa(x1, x2, x3, x4)  =  U4_gaa(x4)
U5_gaa(x1, x2, x3, x4, x5)  =  U5_gaa(x2, x5)
appendF_out_agaa(x1, x2, x3, x4)  =  appendF_out_agaa(x2)
pC_out_gaaaa(x1, x2, x3, x4, x5)  =  pC_out_gaaaa(x1, x2)
APPENDE_IN_GAA(x1, x2, x3)  =  APPENDE_IN_GAA(x1)

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

(8) UsableRulesProof (EQUIVALENT transformation)

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

(9) Obligation:

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

APPENDE_IN_GAA(.(T50, T52), X235, .(T50, X237)) → APPENDE_IN_GAA(T52, X235, X237)

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

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

(10) PiDPToQDPProof (SOUND transformation)

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

(11) Obligation:

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

APPENDE_IN_GAA(.(T52)) → APPENDE_IN_GAA(T52)

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:

• APPENDE_IN_GAA(.(T52)) → APPENDE_IN_GAA(T52)
  The graph contains the following edges 1 > 1

(13) YES

(14) Obligation:

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

S2LD_IN_GA(s(T16), .(X111, X112)) → S2LD_IN_GA(T16, X112)

The TRS R consists of the following rules:

goalA_in_g(0) → U1_g(appendB_in_aa(X10, X11))
appendB_in_aa(X53, X53) → appendB_out_aa(X53, X53)
U1_g(appendB_out_aa(X10, X11)) → goalA_out_g(0)
goalA_in_g(s(T9)) → U2_g(T9, pC_in_gaaaa(T9, X72, X71, X10, X11))
pC_in_gaaaa(T9, T10, X71, X10, X11) → U7_gaaaa(T9, T10, X71, X10, X11, s2lD_in_ga(T9, T10))
s2lD_in_ga(0, []) → s2lD_out_ga(0, [])
s2lD_in_ga(s(T16), .(X111, X112)) → U3_ga(T16, X111, X112, s2lD_in_ga(T16, X112))
U3_ga(T16, X111, X112, s2lD_out_ga(T16, X112)) → s2lD_out_ga(s(T16), .(X111, X112))
U7_gaaaa(T9, T10, X71, X10, X11, s2lD_out_ga(T9, T10)) → U8_gaaaa(T9, T10, X71, X10, X11, appendF_in_agaa(X71, T10, X10, X11))
appendF_in_agaa(X188, T31, X151, .(X188, X153)) → U6_agaa(X188, T31, X151, X153, appendE_in_gaa(T31, X151, X153))
appendE_in_gaa([], X210, X210) → appendE_out_gaa([], X210, X210)
appendE_in_gaa([], X235, .(X251, X237)) → U4_gaa(X235, X251, X237, appendB_in_aa(X235, X237))
U4_gaa(X235, X251, X237, appendB_out_aa(X235, X237)) → appendE_out_gaa([], X235, .(X251, X237))
appendE_in_gaa(.(T50, T52), X235, .(T50, X237)) → U5_gaa(T50, T52, X235, X237, appendE_in_gaa(T52, X235, X237))
U5_gaa(T50, T52, X235, X237, appendE_out_gaa(T52, X235, X237)) → appendE_out_gaa(.(T50, T52), X235, .(T50, X237))
U6_agaa(X188, T31, X151, X153, appendE_out_gaa(T31, X151, X153)) → appendF_out_agaa(X188, T31, X151, .(X188, X153))
U8_gaaaa(T9, T10, X71, X10, X11, appendF_out_agaa(X71, T10, X10, X11)) → pC_out_gaaaa(T9, T10, X71, X10, X11)
U2_g(T9, pC_out_gaaaa(T9, X72, X71, X10, X11)) → goalA_out_g(s(T9))

The argument filtering Pi contains the following mapping:
goalA_in_g(x1)  =  goalA_in_g(x1)
0  =  0
U1_g(x1)  =  U1_g(x1)
appendB_in_aa(x1, x2)  =  appendB_in_aa
appendB_out_aa(x1, x2)  =  appendB_out_aa
goalA_out_g(x1)  =  goalA_out_g(x1)
s(x1)  =  s(x1)
U2_g(x1, x2)  =  U2_g(x1, x2)
pC_in_gaaaa(x1, x2, x3, x4, x5)  =  pC_in_gaaaa(x1)
U7_gaaaa(x1, x2, x3, x4, x5, x6)  =  U7_gaaaa(x1, x6)
s2lD_in_ga(x1, x2)  =  s2lD_in_ga(x1)
s2lD_out_ga(x1, x2)  =  s2lD_out_ga(x1, x2)
U3_ga(x1, x2, x3, x4)  =  U3_ga(x1, x4)
.(x1, x2)  =  .(x2)
U8_gaaaa(x1, x2, x3, x4, x5, x6)  =  U8_gaaaa(x1, x2, x6)
appendF_in_agaa(x1, x2, x3, x4)  =  appendF_in_agaa(x2)
U6_agaa(x1, x2, x3, x4, x5)  =  U6_agaa(x2, x5)
appendE_in_gaa(x1, x2, x3)  =  appendE_in_gaa(x1)
[]  =  []
appendE_out_gaa(x1, x2, x3)  =  appendE_out_gaa(x1)
U4_gaa(x1, x2, x3, x4)  =  U4_gaa(x4)
U5_gaa(x1, x2, x3, x4, x5)  =  U5_gaa(x2, x5)
appendF_out_agaa(x1, x2, x3, x4)  =  appendF_out_agaa(x2)
pC_out_gaaaa(x1, x2, x3, x4, x5)  =  pC_out_gaaaa(x1, x2)
S2LD_IN_GA(x1, x2)  =  S2LD_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:

S2LD_IN_GA(s(T16), .(X111, X112)) → S2LD_IN_GA(T16, X112)

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

S2LD_IN_GA(s(T16)) → S2LD_IN_GA(T16)

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:

• S2LD_IN_GA(s(T16)) → S2LD_IN_GA(T16)
  The graph contains the following edges 1 > 1

(20) YES