Left Termination proof of /tmp/tmpy8UPky/btappend.pl

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

0 Prolog

↳1 PrologToPiTRSViaGraphTransformerProof (⇒, 372 ms)

↳2 PiTRS

↳3 DependencyPairsProof (⇔, 310 ms)

↳4 PiDP

↳5 DependencyGraphProof (⇔, 18 ms)

↳6 AND

    ↳7 PiDP

        ↳8 UsableRulesProof (⇔, 0 ms)

        ↳9 PiDP

        ↳10 PiDPToQDPProof (⇒, 0 ms)

        ↳11 QDP

        ↳12 QDPSizeChangeProof (⇔, 0 ms)

        ↳13 YES

    ↳14 PiDP

        ↳15 UsableRulesProof (⇔, 0 ms)

        ↳16 PiDP

        ↳17 PiDPToQDPProof (⇒, 0 ms)

        ↳18 QDP

        ↳19 QDPSizeChangeProof (⇔, 0 ms)

        ↳20 YES

(0) Obligation:

Clauses:

tappend(nil, T, T).
tappend(node(nil, X, T2), T1, node(T1, X, T2)).
tappend(node(T1, X, nil), T2, node(T1, X, T2)).
tappend(node(T1, X, T2), T3, node(U, X, T2)) :- tappend(T1, T3, U).
tappend(node(T1, X, T2), T3, node(T1, X, U)) :- tappend(T2, T3, U).
s2t(s(X), node(T, Y, T)) :- s2t(X, T).
s2t(s(X), node(nil, Y, T)) :- s2t(X, T).
s2t(s(X), node(T, Y, nil)) :- s2t(X, T).
s2t(s(X), node(nil, Y, nil)).
s2t(0, nil).
goal(X) :- ','(s2t(X, T1), tappend(T1, T2, T3)).

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(T4)\n\nT4 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
3 [label="3: goal(T4), SCOPE: 1, CLAUSE: 10\n\nT4 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
8 [label="8: ','(s2t(T6, X3), tappend(X3, X4, X5))\n\nT6 is ground\nX3 is free\nX4 is free\nX5 is free", fontsize=16, style=filled, fillcolor=lightyellow];
10 [label="10: ','(s2t(T6, X3), tappend(X3, X4, X5)), SCOPE: 2, CLAUSE: 5 | ','(s2t(T6, X3), tappend(X3, X4, X5)), SCOPE: 2, CLAUSE: 6 | ','(s2t(T6, X3), tappend(X3, X4, X5)), SCOPE: 2, CLAUSE: 7 | ','(s2t(T6, X3), tappend(X3, X4, X5)), SCOPE: 2, CLAUSE: 8 | ','(s2t(T6, X3), tappend(X3, X4, X5)), SCOPE: 2, CLAUSE: 9\n\nT6 is ground\nX3 is free\nX4 is free\nX5 is free", fontsize=16, style=filled, fillcolor=lightyellow];
13 [label="13: ','(s2t(T6, X3), tappend(X3, X4, X5)), SCOPE: 2, CLAUSE: 5\n\nT6 is ground\nX3 is free\nX4 is free\nX5 is free", fontsize=16, style=filled, fillcolor=lightyellow];
14 [label="14: ','(s2t(T6, X3), tappend(X3, X4, X5)), SCOPE: 2, CLAUSE: 6 | ','(s2t(T6, X3), tappend(X3, X4, X5)), SCOPE: 2, CLAUSE: 7 | ','(s2t(T6, X3), tappend(X3, X4, X5)), SCOPE: 2, CLAUSE: 8 | ','(s2t(T6, X3), tappend(X3, X4, X5)), SCOPE: 2, CLAUSE: 9\n\nT6 is ground\nX3 is free\nX4 is free\nX5 is free", fontsize=16, style=filled, fillcolor=lightyellow];
18 [label="B: ','(s2t(T11, X29), tappend(node(X29, X30, X29), X4, X5))\n\nT11 is ground\nX4 is free\nX5 is free\nX29 is free\nX30 is free", fontsize=16, style=filled, fillcolor=lightyellow];
19 [label="19: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
21 [label="F: s2t(T11, X29)\n\nT11 is ground\nX29 is free", fontsize=16, style=filled, fillcolor=lightyellow];
22 [label="G: tappend(node(T13, X30, T13), X4, X5)\n\nX4 is free\nX5 is free\nX30 is free", fontsize=16, style=filled, fillcolor=lightyellow];
25 [label="25: s2t(T11, X29), SCOPE: 3, CLAUSE: 5 | s2t(T11, X29), SCOPE: 3, CLAUSE: 6 | s2t(T11, X29), SCOPE: 3, CLAUSE: 7 | s2t(T11, X29), SCOPE: 3, CLAUSE: 8 | s2t(T11, X29), SCOPE: 3, CLAUSE: 9\n\nT11 is ground\nX29 is free", fontsize=16, style=filled, fillcolor=lightyellow];
28 [label="28: s2t(T11, X29), SCOPE: 3, CLAUSE: 5\n\nT11 is ground\nX29 is free", fontsize=16, style=filled, fillcolor=lightyellow];
29 [label="29: s2t(T11, X29), SCOPE: 3, CLAUSE: 6 | s2t(T11, X29), SCOPE: 3, CLAUSE: 7 | s2t(T11, X29), SCOPE: 3, CLAUSE: 8 | s2t(T11, X29), SCOPE: 3, CLAUSE: 9\n\nT11 is ground\nX29 is free", fontsize=16, style=filled, fillcolor=lightyellow];
32 [label="32: s2t(T19, X64)\n\nT19 is ground\nX64 is free", fontsize=16, style=filled, fillcolor=lightyellow];
33 [label="33: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
37 [label="37: s2t(T11, X29), SCOPE: 3, CLAUSE: 6\n\nT11 is ground\nX29 is free", fontsize=16, style=filled, fillcolor=lightyellow];
38 [label="38: s2t(T11, X29), SCOPE: 3, CLAUSE: 7 | s2t(T11, X29), SCOPE: 3, CLAUSE: 8 | s2t(T11, X29), SCOPE: 3, CLAUSE: 9\n\nT11 is ground\nX29 is free", fontsize=16, style=filled, fillcolor=lightyellow];
39 [label="39: s2t(T25, X95)\n\nT25 is ground\nX95 is free", fontsize=16, style=filled, fillcolor=lightyellow];
42 [label="42: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
46 [label="46: s2t(T11, X29), SCOPE: 3, CLAUSE: 7\n\nT11 is ground\nX29 is free", fontsize=16, style=filled, fillcolor=lightyellow];
47 [label="47: s2t(T11, X29), SCOPE: 3, CLAUSE: 8 | s2t(T11, X29), SCOPE: 3, CLAUSE: 9\n\nT11 is ground\nX29 is free", fontsize=16, style=filled, fillcolor=lightyellow];
49 [label="49: s2t(T31, X124)\n\nT31 is ground\nX124 is free", fontsize=16, style=filled, fillcolor=lightyellow];
50 [label="50: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
53 [label="53: s2t(T11, X29), SCOPE: 3, CLAUSE: 8\n\nT11 is ground\nX29 is free", fontsize=16, style=filled, fillcolor=lightyellow];
54 [label="54: s2t(T11, X29), SCOPE: 3, CLAUSE: 9\n\nT11 is ground\nX29 is free", fontsize=16, style=filled, fillcolor=lightyellow];
58 [label="58: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
59 [label="59: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
60 [label="60: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
61 [label="61: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
62 [label="62: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
65 [label="65: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
66 [label="66: tappend(node(T13, X30, T13), X4, X5), SCOPE: 4, CLAUSE: 0 | tappend(node(T13, X30, T13), X4, X5), SCOPE: 4, CLAUSE: 1 | tappend(node(T13, X30, T13), X4, X5), SCOPE: 4, CLAUSE: 2 | tappend(node(T13, X30, T13), X4, X5), SCOPE: 4, CLAUSE: 3 | tappend(node(T13, X30, T13), X4, X5), SCOPE: 4, CLAUSE: 4\n\nX4 is free\nX5 is free\nX30 is free", fontsize=16, style=filled, fillcolor=lightyellow];
67 [label="67: tappend(node(T13, X30, T13), X4, X5), SCOPE: 4, CLAUSE: 1 | tappend(node(T13, X30, T13), X4, X5), SCOPE: 4, CLAUSE: 2 | tappend(node(T13, X30, T13), X4, X5), SCOPE: 4, CLAUSE: 3 | tappend(node(T13, X30, T13), X4, X5), SCOPE: 4, CLAUSE: 4\n\nX4 is free\nX5 is free\nX30 is free", fontsize=16, style=filled, fillcolor=lightyellow];
71 [label="71: tappend(node(T13, X30, T13), X4, X5), SCOPE: 4, CLAUSE: 1\n\nX4 is free\nX5 is free\nX30 is free", fontsize=16, style=filled, fillcolor=lightyellow];
72 [label="72: tappend(node(T13, X30, T13), X4, X5), SCOPE: 4, CLAUSE: 2 | tappend(node(T13, X30, T13), X4, X5), SCOPE: 4, CLAUSE: 3 | tappend(node(T13, X30, T13), X4, X5), SCOPE: 4, CLAUSE: 4\n\nX4 is free\nX5 is free\nX30 is free", fontsize=16, style=filled, fillcolor=lightyellow];
75 [label="75: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
76 [label="76: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
77 [label="77: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
78 [label="78: tappend(node(T13, X30, T13), X4, X5), SCOPE: 4, CLAUSE: 2\n\nX4 is free\nX5 is free\nX30 is free", fontsize=16, style=filled, fillcolor=lightyellow];
79 [label="79: tappend(node(T13, X30, T13), X4, X5), SCOPE: 4, CLAUSE: 3 | tappend(node(T13, X30, T13), X4, X5), SCOPE: 4, CLAUSE: 4\n\nX4 is free\nX5 is free\nX30 is free", fontsize=16, style=filled, fillcolor=lightyellow];
90 [label="90: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
92 [label="92: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
93 [label="93: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
99 [label="99: tappend(node(T13, X30, T13), X4, X5), SCOPE: 4, CLAUSE: 3\n\nX4 is free\nX5 is free\nX30 is free", fontsize=16, style=filled, fillcolor=lightyellow];
100 [label="100: tappend(node(T13, X30, T13), X4, X5), SCOPE: 4, CLAUSE: 4\n\nX4 is free\nX5 is free\nX30 is free", fontsize=16, style=filled, fillcolor=lightyellow];
109 [label="E: tappend(T50, X245, X246)\n\nX245 is free\nX246 is free", fontsize=16, style=filled, fillcolor=lightyellow];
114 [label="114: tappend(T50, X245, X246), SCOPE: 5, CLAUSE: 0 | tappend(T50, X245, X246), SCOPE: 5, CLAUSE: 1 | tappend(T50, X245, X246), SCOPE: 5, CLAUSE: 2 | tappend(T50, X245, X246), SCOPE: 5, CLAUSE: 3 | tappend(T50, X245, X246), SCOPE: 5, CLAUSE: 4\n\nX245 is free\nX246 is free", fontsize=16, style=filled, fillcolor=lightyellow];
115 [label="115: tappend(T50, X245, X246), SCOPE: 5, CLAUSE: 0\n\nX245 is free\nX246 is free", fontsize=16, style=filled, fillcolor=lightyellow];
116 [label="116: tappend(T50, X245, X246), SCOPE: 5, CLAUSE: 1 | tappend(T50, X245, X246), SCOPE: 5, CLAUSE: 2 | tappend(T50, X245, X246), SCOPE: 5, CLAUSE: 3 | tappend(T50, X245, X246), SCOPE: 5, CLAUSE: 4\n\nX245 is free\nX246 is free", fontsize=16, style=filled, fillcolor=lightyellow];
118 [label="118: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
121 [label="121: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
122 [label="122: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
125 [label="125: tappend(T50, X245, X246), SCOPE: 5, CLAUSE: 1\n\nX245 is free\nX246 is free", fontsize=16, style=filled, fillcolor=lightyellow];
126 [label="126: tappend(T50, X245, X246), SCOPE: 5, CLAUSE: 2 | tappend(T50, X245, X246), SCOPE: 5, CLAUSE: 3 | tappend(T50, X245, X246), SCOPE: 5, CLAUSE: 4\n\nX245 is free\nX246 is free", fontsize=16, style=filled, fillcolor=lightyellow];
130 [label="130: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
131 [label="131: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
132 [label="132: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
135 [label="135: tappend(T50, X245, X246), SCOPE: 5, CLAUSE: 2\n\nX245 is free\nX246 is free", fontsize=16, style=filled, fillcolor=lightyellow];
136 [label="136: tappend(T50, X245, X246), SCOPE: 5, CLAUSE: 3 | tappend(T50, X245, X246), SCOPE: 5, CLAUSE: 4\n\nX245 is free\nX246 is free", fontsize=16, style=filled, fillcolor=lightyellow];
140 [label="140: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
141 [label="141: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
142 [label="142: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
145 [label="145: tappend(T50, X245, X246), SCOPE: 5, CLAUSE: 3\n\nX245 is free\nX246 is free", fontsize=16, style=filled, fillcolor=lightyellow];
146 [label="146: tappend(T50, X245, X246), SCOPE: 5, CLAUSE: 4\n\nX245 is free\nX246 is free", fontsize=16, style=filled, fillcolor=lightyellow];
147 [label="147: tappend(T86, X334, X335)\n\nX334 is free\nX335 is free", fontsize=16, style=filled, fillcolor=lightyellow];
148 [label="148: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
156 [label="156: tappend(T96, X359, X360)\n\nX359 is free\nX360 is free", fontsize=16, style=filled, fillcolor=lightyellow];
157 [label="157: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
160 [label="160: tappend(T101, X391, X392)\n\nX391 is free\nX392 is free", fontsize=16, style=filled, fillcolor=lightyellow];
163 [label="163: ','(s2t(T6, X3), tappend(X3, X4, X5)), SCOPE: 2, CLAUSE: 6\n\nT6 is ground\nX3 is free\nX4 is free\nX5 is free", fontsize=16, style=filled, fillcolor=lightyellow];
164 [label="164: ','(s2t(T6, X3), tappend(X3, X4, X5)), SCOPE: 2, CLAUSE: 7 | ','(s2t(T6, X3), tappend(X3, X4, X5)), SCOPE: 2, CLAUSE: 8 | ','(s2t(T6, X3), tappend(X3, X4, X5)), SCOPE: 2, CLAUSE: 9\n\nT6 is ground\nX3 is free\nX4 is free\nX5 is free", fontsize=16, style=filled, fillcolor=lightyellow];
165 [label="C: ','(s2t(T106, X421), tappend(node(nil, X420, X421), X4, X5))\n\nT106 is ground\nX4 is free\nX5 is free\nX420 is free\nX421 is free", fontsize=16, style=filled, fillcolor=lightyellow];
166 [label="166: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
169 [label="169: s2t(T106, X421)\n\nT106 is ground\nX421 is free", fontsize=16, style=filled, fillcolor=lightyellow];
170 [label="170: tappend(node(nil, X420, T108), X4, X5)\n\nX4 is free\nX5 is free\nX420 is free", fontsize=16, style=filled, fillcolor=lightyellow];
178 [label="178: ','(s2t(T6, X3), tappend(X3, X4, X5)), SCOPE: 2, CLAUSE: 7\n\nT6 is ground\nX3 is free\nX4 is free\nX5 is free", fontsize=16, style=filled, fillcolor=lightyellow];
179 [label="179: ','(s2t(T6, X3), tappend(X3, X4, X5)), SCOPE: 2, CLAUSE: 8 | ','(s2t(T6, X3), tappend(X3, X4, X5)), SCOPE: 2, CLAUSE: 9\n\nT6 is ground\nX3 is free\nX4 is free\nX5 is free", fontsize=16, style=filled, fillcolor=lightyellow];
185 [label="D: ','(s2t(T114, X457), tappend(node(X457, X458, nil), X4, X5))\n\nT114 is ground\nX4 is free\nX5 is free\nX457 is free\nX458 is free", fontsize=16, style=filled, fillcolor=lightyellow];
186 [label="186: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
190 [label="190: s2t(T114, X457)\n\nT114 is ground\nX457 is free", fontsize=16, style=filled, fillcolor=lightyellow];
191 [label="191: tappend(node(T116, X458, nil), X4, X5)\n\nX4 is free\nX5 is free\nX458 is free", fontsize=16, style=filled, fillcolor=lightyellow];
194 [label="194: ','(s2t(T6, X3), tappend(X3, X4, X5)), SCOPE: 2, CLAUSE: 8\n\nT6 is ground\nX3 is free\nX4 is free\nX5 is free", fontsize=16, style=filled, fillcolor=lightyellow];
195 [label="195: ','(s2t(T6, X3), tappend(X3, X4, X5)), SCOPE: 2, CLAUSE: 9\n\nT6 is ground\nX3 is free\nX4 is free\nX5 is free", fontsize=16, style=filled, fillcolor=lightyellow];
198 [label="198: tappend(node(nil, X485, nil), X4, X5)\n\nX4 is free\nX5 is free\nX485 is free", fontsize=16, style=filled, fillcolor=lightyellow];
199 [label="199: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
200 [label="200: tappend(nil, X4, X5)\n\nX4 is free\nX5 is free", fontsize=16, style=filled, fillcolor=lightyellow];
201 [label="201: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
202 [label="202: tappend(nil, X4, X5), SCOPE: 6, CLAUSE: 0 | tappend(nil, X4, X5), SCOPE: 6, CLAUSE: 1 | tappend(nil, X4, X5), SCOPE: 6, CLAUSE: 2 | tappend(nil, X4, X5), SCOPE: 6, CLAUSE: 3 | tappend(nil, X4, X5), SCOPE: 6, CLAUSE: 4\n\nX4 is free\nX5 is free", fontsize=16, style=filled, fillcolor=lightyellow];
203 [label="203: tappend(nil, X4, X5), SCOPE: 6, CLAUSE: 0\n\nX4 is free\nX5 is free", fontsize=16, style=filled, fillcolor=lightyellow];
204 [label="204: tappend(nil, X4, X5), SCOPE: 6, CLAUSE: 1 | tappend(nil, X4, X5), SCOPE: 6, CLAUSE: 2 | tappend(nil, X4, X5), SCOPE: 6, CLAUSE: 3 | tappend(nil, X4, X5), SCOPE: 6, CLAUSE: 4\n\nX4 is free\nX5 is free", fontsize=16, style=filled, fillcolor=lightyellow];
205 [label="205: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
206 [label="206: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
209 [label="209: tappend(nil, X4, X5), SCOPE: 6, CLAUSE: 2 | tappend(nil, X4, X5), SCOPE: 6, CLAUSE: 3 | tappend(nil, X4, X5), SCOPE: 6, CLAUSE: 4\n\nX4 is free\nX5 is free", fontsize=16, style=filled, fillcolor=lightyellow];
210 [label="210: tappend(nil, X4, X5), SCOPE: 6, CLAUSE: 3 | tappend(nil, X4, X5), SCOPE: 6, CLAUSE: 4\n\nX4 is free\nX5 is free", fontsize=16, style=filled, fillcolor=lightyellow];
212 [label="212: tappend(nil, X4, X5), SCOPE: 6, CLAUSE: 4\n\nX4 is free\nX5 is free", fontsize=16, style=filled, fillcolor=lightyellow];
213 [label="213: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
214 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
2 -> 214 [arrowhead = none ];
214 -> 3;

215 [label="ONLY EVAL with clause\ngoal(X2) :- ','(s2t(X2, X3), tappend(X3, X4, X5)).\nand substitutionT4 -> T6,\nX2 -> T6", fontsize=14, style = filled, fillcolor = lightblue];
3 -> 215 [arrowhead = none ];
215 -> 8;

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

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

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

219 [label="EVAL with clause\ns2t(s(X26), node(X27, X28, X27)) :- s2t(X26, X27).\nand substitutionX26 -> T11,\nT6 -> s(T11),\nX27 -> X29,\nX28 -> X30,\nX3 -> node(X29, X30, X29)", fontsize=14, style = filled, fillcolor = lightblue];
13 -> 219 [arrowhead = none ];
219 -> 18;

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

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

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

223 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
18 -> 223 [arrowhead = none ];
223 -> 21;

224 [label="SPLIT 2\nnew knowledge:\nT11 is ground\nreplacements:X29 -> T13", fontsize=14, style = filled, fillcolor = violet];
18 -> 224 [arrowhead = none ];
224 -> 22;

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

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

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

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

229 [label="EVAL with clause\ns2t(s(X61), node(X62, X63, X62)) :- s2t(X61, X62).\nand substitutionX61 -> T19,\nT11 -> s(T19),\nX62 -> X64,\nX63 -> X65,\nX29 -> node(X64, X65, X64)", fontsize=14, style = filled, fillcolor = lightblue];
28 -> 229 [arrowhead = none ];
229 -> 32;

230 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
28 -> 230 [arrowhead = none ];
230 -> 33;

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

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

233 [label="INSTANCE with matching:\nT11 -> T19\nX29 -> X64", fontsize=14, style = filled, fillcolor = lightgrey];
32 -> 233 [arrowhead = none , style=dashed];
233 -> 21[style=dashed];

234 [label="EVAL with clause\ns2t(s(X91), node(nil, X92, X93)) :- s2t(X91, X93).\nand substitutionX91 -> T25,\nT11 -> s(T25),\nX92 -> X94,\nX93 -> X95,\nX29 -> node(nil, X94, X95)", fontsize=14, style = filled, fillcolor = lightblue];
37 -> 234 [arrowhead = none ];
234 -> 39;

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

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

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

238 [label="INSTANCE with matching:\nT11 -> T25\nX29 -> X95", fontsize=14, style = filled, fillcolor = lightgrey];
39 -> 238 [arrowhead = none , style=dashed];
238 -> 21[style=dashed];

239 [label="EVAL with clause\ns2t(s(X121), node(X122, X123, nil)) :- s2t(X121, X122).\nand substitutionX121 -> T31,\nT11 -> s(T31),\nX122 -> X124,\nX123 -> X125,\nX29 -> node(X124, X125, nil)", fontsize=14, style = filled, fillcolor = lightblue];
46 -> 239 [arrowhead = none ];
239 -> 49;

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

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

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

243 [label="INSTANCE with matching:\nT11 -> T31\nX29 -> X124", fontsize=14, style = filled, fillcolor = lightgrey];
49 -> 243 [arrowhead = none , style=dashed];
243 -> 21[style=dashed];

244 [label="EVAL with clause\ns2t(s(X143), node(nil, X144, nil)).\nand substitutionX143 -> T37,\nT11 -> s(T37),\nX144 -> X145,\nX29 -> node(nil, X145, nil)", fontsize=14, style = filled, fillcolor = lightblue];
53 -> 244 [arrowhead = none ];
244 -> 58;

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

246 [label="EVAL with clause\ns2t(0, nil).\nand substitutionT11 -> 0,\nX29 -> nil", fontsize=14, style = filled, fillcolor = lightblue];
54 -> 246 [arrowhead = none ];
246 -> 61;

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

248 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
58 -> 248 [arrowhead = none ];
248 -> 60;

249 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
61 -> 249 [arrowhead = none ];
249 -> 65;

250 [label="BACKTRACK\nfor clause: tappend(nil, T, T)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
66 -> 250 [arrowhead = none ];
250 -> 67;

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

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

253 [label="EVAL with clause\ntappend(node(nil, X169, X170), X171, node(X171, X169, X170)).\nand substitutionT13 -> nil,\nX30 -> X172,\nX169 -> X172,\nX170 -> nil,\nX4 -> X173,\nX171 -> X173,\nX5 -> node(X173, X172, nil)", fontsize=14, style = filled, fillcolor = lightblue];
71 -> 253 [arrowhead = none ];
253 -> 75;

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

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

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

257 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
75 -> 257 [arrowhead = none ];
257 -> 77;

258 [label="EVAL with clause\ntappend(node(X194, X195, nil), X196, node(X194, X195, X196)).\nand substitutionT13 -> nil,\nX194 -> nil,\nX30 -> X197,\nX195 -> X197,\nT42 -> nil,\nX4 -> X198,\nX196 -> X198,\nX5 -> node(nil, X197, X198)", fontsize=14, style = filled, fillcolor = lightblue];
78 -> 258 [arrowhead = none ];
258 -> 90;

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

260 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
79 -> 260 [arrowhead = none ];
260 -> 99;

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

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

263 [label="ONLY EVAL with clause\ntappend(node(X239, X240, X241), X242, node(X243, X240, X241)) :- tappend(X239, X242, X243).\nand substitutionT13 -> T50,\nX239 -> T50,\nX30 -> X244,\nX240 -> X244,\nX241 -> T50,\nX4 -> X245,\nX242 -> X245,\nX243 -> X246,\nX5 -> node(X246, X244, T50),\nT49 -> T50", fontsize=14, style = filled, fillcolor = lightblue];
99 -> 263 [arrowhead = none ];
263 -> 109;

264 [label="ONLY EVAL with clause\ntappend(node(X385, X386, X387), X388, node(X385, X386, X389)) :- tappend(X387, X388, X389).\nand substitutionT13 -> T101,\nX385 -> T101,\nX30 -> X390,\nX386 -> X390,\nX387 -> T101,\nX4 -> X391,\nX388 -> X391,\nX389 -> X392,\nX5 -> node(T101, X390, X392),\nT100 -> T101", fontsize=14, style = filled, fillcolor = lightblue];
100 -> 264 [arrowhead = none ];
264 -> 160;

265 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
109 -> 265 [arrowhead = none ];
265 -> 114;

266 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
114 -> 266 [arrowhead = none ];
266 -> 115;

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

268 [label="EVAL with clause\ntappend(nil, X259, X259).\nand substitutionT50 -> nil,\nX245 -> X260,\nX259 -> X260,\nX246 -> X260", fontsize=14, style = filled, fillcolor = lightblue];
115 -> 268 [arrowhead = none ];
268 -> 118;

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

270 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
116 -> 270 [arrowhead = none ];
270 -> 125;

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

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

273 [label="EVAL with clause\ntappend(node(nil, X277, X278), X279, node(X279, X277, X278)).\nand substitutionX277 -> T59,\nX278 -> T60,\nT50 -> node(nil, T59, T60),\nX245 -> X280,\nX279 -> X280,\nX246 -> node(X280, T59, T60)", fontsize=14, style = filled, fillcolor = lightblue];
125 -> 273 [arrowhead = none ];
273 -> 130;

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

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

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

277 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
130 -> 277 [arrowhead = none ];
277 -> 132;

278 [label="EVAL with clause\ntappend(node(X297, X298, nil), X299, node(X297, X298, X299)).\nand substitutionX297 -> T69,\nX298 -> T70,\nT50 -> node(T69, T70, nil),\nX245 -> X300,\nX299 -> X300,\nX246 -> node(T69, T70, X300)", fontsize=14, style = filled, fillcolor = lightblue];
135 -> 278 [arrowhead = none ];
278 -> 140;

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

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

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

282 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
140 -> 282 [arrowhead = none ];
282 -> 142;

283 [label="EVAL with clause\ntappend(node(X329, X330, X331), X332, node(X333, X330, X331)) :- tappend(X329, X332, X333).\nand substitutionX329 -> T86,\nX330 -> T84,\nX331 -> T85,\nT50 -> node(T86, T84, T85),\nX245 -> X334,\nX332 -> X334,\nX333 -> X335,\nX246 -> node(X335, T84, T85),\nT83 -> T86", fontsize=14, style = filled, fillcolor = lightblue];
145 -> 283 [arrowhead = none ];
283 -> 147;

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

285 [label="EVAL with clause\ntappend(node(X354, X355, X356), X357, node(X354, X355, X358)) :- tappend(X356, X357, X358).\nand substitutionX354 -> T93,\nX355 -> T94,\nX356 -> T96,\nT50 -> node(T93, T94, T96),\nX245 -> X359,\nX357 -> X359,\nX358 -> X360,\nX246 -> node(T93, T94, X360),\nT95 -> T96", fontsize=14, style = filled, fillcolor = lightblue];
146 -> 285 [arrowhead = none ];
285 -> 156;

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

287 [label="INSTANCE with matching:\nT50 -> T86\nX245 -> X334\nX246 -> X335", fontsize=14, style = filled, fillcolor = lightgrey];
147 -> 287 [arrowhead = none , style=dashed];
287 -> 109[style=dashed];

288 [label="INSTANCE with matching:\nT50 -> T96\nX245 -> X359\nX246 -> X360", fontsize=14, style = filled, fillcolor = lightgrey];
156 -> 288 [arrowhead = none , style=dashed];
288 -> 109[style=dashed];

289 [label="INSTANCE with matching:\nT50 -> T101\nX245 -> X391\nX246 -> X392", fontsize=14, style = filled, fillcolor = lightgrey];
160 -> 289 [arrowhead = none , style=dashed];
289 -> 109[style=dashed];

290 [label="EVAL with clause\ns2t(s(X417), node(nil, X418, X419)) :- s2t(X417, X419).\nand substitutionX417 -> T106,\nT6 -> s(T106),\nX418 -> X420,\nX419 -> X421,\nX3 -> node(nil, X420, X421)", fontsize=14, style = filled, fillcolor = lightblue];
163 -> 290 [arrowhead = none ];
290 -> 165;

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

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

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

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

295 [label="SPLIT 2\nnew knowledge:\nT106 is ground\nreplacements:X421 -> T108", fontsize=14, style = filled, fillcolor = violet];
165 -> 295 [arrowhead = none ];
295 -> 170;

296 [label="INSTANCE with matching:\nT11 -> T106\nX29 -> X421", fontsize=14, style = filled, fillcolor = lightgrey];
169 -> 296 [arrowhead = none , style=dashed];
296 -> 21[style=dashed];

297 [label="INSTANCE with matching:\nT50 -> node(nil, X420, T108)\nX245 -> X4\nX246 -> X5", fontsize=14, style = filled, fillcolor = lightgrey];
170 -> 297 [arrowhead = none , style=dashed];
297 -> 109[style=dashed];

298 [label="EVAL with clause\ns2t(s(X454), node(X455, X456, nil)) :- s2t(X454, X455).\nand substitutionX454 -> T114,\nT6 -> s(T114),\nX455 -> X457,\nX456 -> X458,\nX3 -> node(X457, X458, nil)", fontsize=14, style = filled, fillcolor = lightblue];
178 -> 298 [arrowhead = none ];
298 -> 185;

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

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

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

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

303 [label="SPLIT 2\nnew knowledge:\nT114 is ground\nreplacements:X457 -> T116", fontsize=14, style = filled, fillcolor = violet];
185 -> 303 [arrowhead = none ];
303 -> 191;

304 [label="INSTANCE with matching:\nT11 -> T114\nX29 -> X457", fontsize=14, style = filled, fillcolor = lightgrey];
190 -> 304 [arrowhead = none , style=dashed];
304 -> 21[style=dashed];

305 [label="INSTANCE with matching:\nT50 -> node(T116, X458, nil)\nX245 -> X4\nX246 -> X5", fontsize=14, style = filled, fillcolor = lightgrey];
191 -> 305 [arrowhead = none , style=dashed];
305 -> 109[style=dashed];

306 [label="EVAL with clause\ns2t(s(X483), node(nil, X484, nil)).\nand substitutionX483 -> T122,\nT6 -> s(T122),\nX484 -> X485,\nX3 -> node(nil, X485, nil)", fontsize=14, style = filled, fillcolor = lightblue];
194 -> 306 [arrowhead = none ];
306 -> 198;

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

308 [label="EVAL with clause\ns2t(0, nil).\nand substitutionT6 -> 0,\nX3 -> nil", fontsize=14, style = filled, fillcolor = lightblue];
195 -> 308 [arrowhead = none ];
308 -> 200;

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

310 [label="INSTANCE with matching:\nT50 -> node(nil, X485, nil)\nX245 -> X4\nX246 -> X5", fontsize=14, style = filled, fillcolor = lightgrey];
198 -> 310 [arrowhead = none , style=dashed];
310 -> 109[style=dashed];

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

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

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

314 [label="ONLY EVAL with clause\ntappend(nil, X498, X498).\nand substitutionX4 -> X499,\nX498 -> X499,\nX5 -> X499", fontsize=14, style = filled, fillcolor = lightblue];
203 -> 314 [arrowhead = none ];
314 -> 205;

315 [label="BACKTRACK\nfor clause: tappend(node(nil, X, T2), T1, node(T1, X, T2))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
204 -> 315 [arrowhead = none ];
315 -> 209;

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

317 [label="BACKTRACK\nfor clause: tappend(node(T1, X, nil), T2, node(T1, X, T2))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
209 -> 317 [arrowhead = none ];
317 -> 210;

318 [label="BACKTRACK\nfor clause: tappend(node(T1, X, T2), T3, node(U, X, T2)) :- tappend(T1, T3, U)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
210 -> 318 [arrowhead = none ];
318 -> 212;

319 [label="BACKTRACK\nfor clause: tappend(node(T1, X, T2), T3, node(T1, X, U)) :- tappend(T2, T3, U)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
212 -> 319 [arrowhead = none ];
319 -> 213;

}

(2) Obligation:

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

goalA_in_g(s(T11)) → U1_g(T11, pB_in_gaaaa(T11, X29, X30, X4, X5))
pB_in_gaaaa(T11, T13, X30, X4, X5) → U12_gaaaa(T11, T13, X30, X4, X5, s2tF_in_ga(T11, T13))
s2tF_in_ga(s(T19), node(X64, X65, X64)) → U5_ga(T19, X64, X65, s2tF_in_ga(T19, X64))
s2tF_in_ga(s(T25), node(nil, X94, X95)) → U6_ga(T25, X94, X95, s2tF_in_ga(T25, X95))
s2tF_in_ga(s(T31), node(X124, X125, nil)) → U7_ga(T31, X124, X125, s2tF_in_ga(T31, X124))
s2tF_in_ga(s(T37), node(nil, X145, nil)) → s2tF_out_ga(s(T37), node(nil, X145, nil))
s2tF_in_ga(0, nil) → s2tF_out_ga(0, nil)
U7_ga(T31, X124, X125, s2tF_out_ga(T31, X124)) → s2tF_out_ga(s(T31), node(X124, X125, nil))
U6_ga(T25, X94, X95, s2tF_out_ga(T25, X95)) → s2tF_out_ga(s(T25), node(nil, X94, X95))
U5_ga(T19, X64, X65, s2tF_out_ga(T19, X64)) → s2tF_out_ga(s(T19), node(X64, X65, X64))
U12_gaaaa(T11, T13, X30, X4, X5, s2tF_out_ga(T11, T13)) → U13_gaaaa(T11, T13, X30, X4, X5, tappendG_in_gaaa(T13, X30, X4, X5))
tappendG_in_gaaa(nil, X172, X173, node(X173, X172, nil)) → tappendG_out_gaaa(nil, X172, X173, node(X173, X172, nil))
tappendG_in_gaaa(nil, X197, X198, node(nil, X197, X198)) → tappendG_out_gaaa(nil, X197, X198, node(nil, X197, X198))
tappendG_in_gaaa(T50, X244, X245, node(X246, X244, T50)) → U10_gaaa(T50, X244, X245, X246, tappendE_in_gaa(T50, X245, X246))
tappendE_in_gaa(nil, X260, X260) → tappendE_out_gaa(nil, X260, X260)
tappendE_in_gaa(node(nil, T59, T60), X280, node(X280, T59, T60)) → tappendE_out_gaa(node(nil, T59, T60), X280, node(X280, T59, T60))
tappendE_in_gaa(node(T69, T70, nil), X300, node(T69, T70, X300)) → tappendE_out_gaa(node(T69, T70, nil), X300, node(T69, T70, X300))
tappendE_in_gaa(node(T86, T84, T85), X334, node(X335, T84, T85)) → U8_gaa(T86, T84, T85, X334, X335, tappendE_in_gaa(T86, X334, X335))
tappendE_in_gaa(node(T93, T94, T96), X359, node(T93, T94, X360)) → U9_gaa(T93, T94, T96, X359, X360, tappendE_in_gaa(T96, X359, X360))
U9_gaa(T93, T94, T96, X359, X360, tappendE_out_gaa(T96, X359, X360)) → tappendE_out_gaa(node(T93, T94, T96), X359, node(T93, T94, X360))
U8_gaa(T86, T84, T85, X334, X335, tappendE_out_gaa(T86, X334, X335)) → tappendE_out_gaa(node(T86, T84, T85), X334, node(X335, T84, T85))
U10_gaaa(T50, X244, X245, X246, tappendE_out_gaa(T50, X245, X246)) → tappendG_out_gaaa(T50, X244, X245, node(X246, X244, T50))
tappendG_in_gaaa(T101, X390, X391, node(T101, X390, X392)) → U11_gaaa(T101, X390, X391, X392, tappendE_in_gaa(T101, X391, X392))
U11_gaaa(T101, X390, X391, X392, tappendE_out_gaa(T101, X391, X392)) → tappendG_out_gaaa(T101, X390, X391, node(T101, X390, X392))
U13_gaaaa(T11, T13, X30, X4, X5, tappendG_out_gaaa(T13, X30, X4, X5)) → pB_out_gaaaa(T11, T13, X30, X4, X5)
U1_g(T11, pB_out_gaaaa(T11, X29, X30, X4, X5)) → goalA_out_g(s(T11))
goalA_in_g(s(T106)) → U2_g(T106, pC_in_gaaaa(T106, X421, X420, X4, X5))
pC_in_gaaaa(T106, T108, X420, X4, X5) → U14_gaaaa(T106, T108, X420, X4, X5, s2tF_in_ga(T106, T108))
U14_gaaaa(T106, T108, X420, X4, X5, s2tF_out_ga(T106, T108)) → U15_gaaaa(T106, T108, X420, X4, X5, tappendE_in_gaa(node(nil, X420, T108), X4, X5))
U15_gaaaa(T106, T108, X420, X4, X5, tappendE_out_gaa(node(nil, X420, T108), X4, X5)) → pC_out_gaaaa(T106, T108, X420, X4, X5)
U2_g(T106, pC_out_gaaaa(T106, X421, X420, X4, X5)) → goalA_out_g(s(T106))
goalA_in_g(s(T114)) → U3_g(T114, pD_in_gaaaa(T114, X457, X458, X4, X5))
pD_in_gaaaa(T114, T116, X458, X4, X5) → U16_gaaaa(T114, T116, X458, X4, X5, s2tF_in_ga(T114, T116))
U16_gaaaa(T114, T116, X458, X4, X5, s2tF_out_ga(T114, T116)) → U17_gaaaa(T114, T116, X458, X4, X5, tappendE_in_gaa(node(T116, X458, nil), X4, X5))
U17_gaaaa(T114, T116, X458, X4, X5, tappendE_out_gaa(node(T116, X458, nil), X4, X5)) → pD_out_gaaaa(T114, T116, X458, X4, X5)
U3_g(T114, pD_out_gaaaa(T114, X457, X458, X4, X5)) → goalA_out_g(s(T114))
goalA_in_g(s(T122)) → U4_g(T122, tappendE_in_gaa(node(nil, X485, nil), X4, X5))
U4_g(T122, tappendE_out_gaa(node(nil, X485, nil), X4, X5)) → goalA_out_g(s(T122))
goalA_in_g(0) → goalA_out_g(0)

(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(s(T11)) → U1_G(T11, pB_in_gaaaa(T11, X29, X30, X4, X5))
GOALA_IN_G(s(T11)) → PB_IN_GAAAA(T11, X29, X30, X4, X5)
PB_IN_GAAAA(T11, T13, X30, X4, X5) → U12_GAAAA(T11, T13, X30, X4, X5, s2tF_in_ga(T11, T13))
PB_IN_GAAAA(T11, T13, X30, X4, X5) → S2TF_IN_GA(T11, T13)
S2TF_IN_GA(s(T19), node(X64, X65, X64)) → U5_GA(T19, X64, X65, s2tF_in_ga(T19, X64))
S2TF_IN_GA(s(T19), node(X64, X65, X64)) → S2TF_IN_GA(T19, X64)
S2TF_IN_GA(s(T25), node(nil, X94, X95)) → U6_GA(T25, X94, X95, s2tF_in_ga(T25, X95))
S2TF_IN_GA(s(T25), node(nil, X94, X95)) → S2TF_IN_GA(T25, X95)
S2TF_IN_GA(s(T31), node(X124, X125, nil)) → U7_GA(T31, X124, X125, s2tF_in_ga(T31, X124))
S2TF_IN_GA(s(T31), node(X124, X125, nil)) → S2TF_IN_GA(T31, X124)
U12_GAAAA(T11, T13, X30, X4, X5, s2tF_out_ga(T11, T13)) → U13_GAAAA(T11, T13, X30, X4, X5, tappendG_in_gaaa(T13, X30, X4, X5))
U12_GAAAA(T11, T13, X30, X4, X5, s2tF_out_ga(T11, T13)) → TAPPENDG_IN_GAAA(T13, X30, X4, X5)
TAPPENDG_IN_GAAA(T50, X244, X245, node(X246, X244, T50)) → U10_GAAA(T50, X244, X245, X246, tappendE_in_gaa(T50, X245, X246))
TAPPENDG_IN_GAAA(T50, X244, X245, node(X246, X244, T50)) → TAPPENDE_IN_GAA(T50, X245, X246)
TAPPENDE_IN_GAA(node(T86, T84, T85), X334, node(X335, T84, T85)) → U8_GAA(T86, T84, T85, X334, X335, tappendE_in_gaa(T86, X334, X335))
TAPPENDE_IN_GAA(node(T86, T84, T85), X334, node(X335, T84, T85)) → TAPPENDE_IN_GAA(T86, X334, X335)
TAPPENDE_IN_GAA(node(T93, T94, T96), X359, node(T93, T94, X360)) → U9_GAA(T93, T94, T96, X359, X360, tappendE_in_gaa(T96, X359, X360))
TAPPENDE_IN_GAA(node(T93, T94, T96), X359, node(T93, T94, X360)) → TAPPENDE_IN_GAA(T96, X359, X360)
TAPPENDG_IN_GAAA(T101, X390, X391, node(T101, X390, X392)) → U11_GAAA(T101, X390, X391, X392, tappendE_in_gaa(T101, X391, X392))
TAPPENDG_IN_GAAA(T101, X390, X391, node(T101, X390, X392)) → TAPPENDE_IN_GAA(T101, X391, X392)
GOALA_IN_G(s(T106)) → U2_G(T106, pC_in_gaaaa(T106, X421, X420, X4, X5))
GOALA_IN_G(s(T106)) → PC_IN_GAAAA(T106, X421, X420, X4, X5)
PC_IN_GAAAA(T106, T108, X420, X4, X5) → U14_GAAAA(T106, T108, X420, X4, X5, s2tF_in_ga(T106, T108))
PC_IN_GAAAA(T106, T108, X420, X4, X5) → S2TF_IN_GA(T106, T108)
U14_GAAAA(T106, T108, X420, X4, X5, s2tF_out_ga(T106, T108)) → U15_GAAAA(T106, T108, X420, X4, X5, tappendE_in_gaa(node(nil, X420, T108), X4, X5))
U14_GAAAA(T106, T108, X420, X4, X5, s2tF_out_ga(T106, T108)) → TAPPENDE_IN_GAA(node(nil, X420, T108), X4, X5)
GOALA_IN_G(s(T114)) → U3_G(T114, pD_in_gaaaa(T114, X457, X458, X4, X5))
GOALA_IN_G(s(T114)) → PD_IN_GAAAA(T114, X457, X458, X4, X5)
PD_IN_GAAAA(T114, T116, X458, X4, X5) → U16_GAAAA(T114, T116, X458, X4, X5, s2tF_in_ga(T114, T116))
PD_IN_GAAAA(T114, T116, X458, X4, X5) → S2TF_IN_GA(T114, T116)
U16_GAAAA(T114, T116, X458, X4, X5, s2tF_out_ga(T114, T116)) → U17_GAAAA(T114, T116, X458, X4, X5, tappendE_in_gaa(node(T116, X458, nil), X4, X5))
U16_GAAAA(T114, T116, X458, X4, X5, s2tF_out_ga(T114, T116)) → TAPPENDE_IN_GAA(node(T116, X458, nil), X4, X5)
GOALA_IN_G(s(T122)) → U4_G(T122, tappendE_in_gaa(node(nil, X485, nil), X4, X5))
GOALA_IN_G(s(T122)) → TAPPENDE_IN_GAA(node(nil, X485, nil), X4, X5)

The TRS R consists of the following rules:

goalA_in_g(s(T11)) → U1_g(T11, pB_in_gaaaa(T11, X29, X30, X4, X5))
pB_in_gaaaa(T11, T13, X30, X4, X5) → U12_gaaaa(T11, T13, X30, X4, X5, s2tF_in_ga(T11, T13))
s2tF_in_ga(s(T19), node(X64, X65, X64)) → U5_ga(T19, X64, X65, s2tF_in_ga(T19, X64))
s2tF_in_ga(s(T25), node(nil, X94, X95)) → U6_ga(T25, X94, X95, s2tF_in_ga(T25, X95))
s2tF_in_ga(s(T31), node(X124, X125, nil)) → U7_ga(T31, X124, X125, s2tF_in_ga(T31, X124))
s2tF_in_ga(s(T37), node(nil, X145, nil)) → s2tF_out_ga(s(T37), node(nil, X145, nil))
s2tF_in_ga(0, nil) → s2tF_out_ga(0, nil)
U7_ga(T31, X124, X125, s2tF_out_ga(T31, X124)) → s2tF_out_ga(s(T31), node(X124, X125, nil))
U6_ga(T25, X94, X95, s2tF_out_ga(T25, X95)) → s2tF_out_ga(s(T25), node(nil, X94, X95))
U5_ga(T19, X64, X65, s2tF_out_ga(T19, X64)) → s2tF_out_ga(s(T19), node(X64, X65, X64))
U12_gaaaa(T11, T13, X30, X4, X5, s2tF_out_ga(T11, T13)) → U13_gaaaa(T11, T13, X30, X4, X5, tappendG_in_gaaa(T13, X30, X4, X5))
tappendG_in_gaaa(nil, X172, X173, node(X173, X172, nil)) → tappendG_out_gaaa(nil, X172, X173, node(X173, X172, nil))
tappendG_in_gaaa(nil, X197, X198, node(nil, X197, X198)) → tappendG_out_gaaa(nil, X197, X198, node(nil, X197, X198))
tappendG_in_gaaa(T50, X244, X245, node(X246, X244, T50)) → U10_gaaa(T50, X244, X245, X246, tappendE_in_gaa(T50, X245, X246))
tappendE_in_gaa(nil, X260, X260) → tappendE_out_gaa(nil, X260, X260)
tappendE_in_gaa(node(nil, T59, T60), X280, node(X280, T59, T60)) → tappendE_out_gaa(node(nil, T59, T60), X280, node(X280, T59, T60))
tappendE_in_gaa(node(T69, T70, nil), X300, node(T69, T70, X300)) → tappendE_out_gaa(node(T69, T70, nil), X300, node(T69, T70, X300))
tappendE_in_gaa(node(T86, T84, T85), X334, node(X335, T84, T85)) → U8_gaa(T86, T84, T85, X334, X335, tappendE_in_gaa(T86, X334, X335))
tappendE_in_gaa(node(T93, T94, T96), X359, node(T93, T94, X360)) → U9_gaa(T93, T94, T96, X359, X360, tappendE_in_gaa(T96, X359, X360))
U9_gaa(T93, T94, T96, X359, X360, tappendE_out_gaa(T96, X359, X360)) → tappendE_out_gaa(node(T93, T94, T96), X359, node(T93, T94, X360))
U8_gaa(T86, T84, T85, X334, X335, tappendE_out_gaa(T86, X334, X335)) → tappendE_out_gaa(node(T86, T84, T85), X334, node(X335, T84, T85))
U10_gaaa(T50, X244, X245, X246, tappendE_out_gaa(T50, X245, X246)) → tappendG_out_gaaa(T50, X244, X245, node(X246, X244, T50))
tappendG_in_gaaa(T101, X390, X391, node(T101, X390, X392)) → U11_gaaa(T101, X390, X391, X392, tappendE_in_gaa(T101, X391, X392))
U11_gaaa(T101, X390, X391, X392, tappendE_out_gaa(T101, X391, X392)) → tappendG_out_gaaa(T101, X390, X391, node(T101, X390, X392))
U13_gaaaa(T11, T13, X30, X4, X5, tappendG_out_gaaa(T13, X30, X4, X5)) → pB_out_gaaaa(T11, T13, X30, X4, X5)
U1_g(T11, pB_out_gaaaa(T11, X29, X30, X4, X5)) → goalA_out_g(s(T11))
goalA_in_g(s(T106)) → U2_g(T106, pC_in_gaaaa(T106, X421, X420, X4, X5))
pC_in_gaaaa(T106, T108, X420, X4, X5) → U14_gaaaa(T106, T108, X420, X4, X5, s2tF_in_ga(T106, T108))
U14_gaaaa(T106, T108, X420, X4, X5, s2tF_out_ga(T106, T108)) → U15_gaaaa(T106, T108, X420, X4, X5, tappendE_in_gaa(node(nil, X420, T108), X4, X5))
U15_gaaaa(T106, T108, X420, X4, X5, tappendE_out_gaa(node(nil, X420, T108), X4, X5)) → pC_out_gaaaa(T106, T108, X420, X4, X5)
U2_g(T106, pC_out_gaaaa(T106, X421, X420, X4, X5)) → goalA_out_g(s(T106))
goalA_in_g(s(T114)) → U3_g(T114, pD_in_gaaaa(T114, X457, X458, X4, X5))
pD_in_gaaaa(T114, T116, X458, X4, X5) → U16_gaaaa(T114, T116, X458, X4, X5, s2tF_in_ga(T114, T116))
U16_gaaaa(T114, T116, X458, X4, X5, s2tF_out_ga(T114, T116)) → U17_gaaaa(T114, T116, X458, X4, X5, tappendE_in_gaa(node(T116, X458, nil), X4, X5))
U17_gaaaa(T114, T116, X458, X4, X5, tappendE_out_gaa(node(T116, X458, nil), X4, X5)) → pD_out_gaaaa(T114, T116, X458, X4, X5)
U3_g(T114, pD_out_gaaaa(T114, X457, X458, X4, X5)) → goalA_out_g(s(T114))
goalA_in_g(s(T122)) → U4_g(T122, tappendE_in_gaa(node(nil, X485, nil), X4, X5))
U4_g(T122, tappendE_out_gaa(node(nil, X485, nil), X4, X5)) → goalA_out_g(s(T122))
goalA_in_g(0) → goalA_out_g(0)

The argument filtering Pi contains the following mapping:
goalA_in_g(x1) = goalA_in_g(x1)
s(x1) = s(x1)
U1_g(x1, x2) = U1_g(x1, x2)
pB_in_gaaaa(x1, x2, x3, x4, x5) = pB_in_gaaaa(x1)
U12_gaaaa(x1, x2, x3, x4, x5, x6) = U12_gaaaa(x1, x6)
s2tF_in_ga(x1, x2) = s2tF_in_ga(x1)
U5_ga(x1, x2, x3, x4) = U5_ga(x1, x4)
U6_ga(x1, x2, x3, x4) = U6_ga(x1, x4)
U7_ga(x1, x2, x3, x4) = U7_ga(x1, x4)
s2tF_out_ga(x1, x2) = s2tF_out_ga(x1, x2)
node(x1, x2, x3) = node(x1, x3)
0 = 0
U13_gaaaa(x1, x2, x3, x4, x5, x6) = U13_gaaaa(x1, x2, x6)
tappendG_in_gaaa(x1, x2, x3, x4) = tappendG_in_gaaa(x1)
nil = nil
tappendG_out_gaaa(x1, x2, x3, x4) = tappendG_out_gaaa(x1)
U10_gaaa(x1, x2, x3, x4, x5) = U10_gaaa(x1, x5)
tappendE_in_gaa(x1, x2, x3) = tappendE_in_gaa(x1)
tappendE_out_gaa(x1, x2, x3) = tappendE_out_gaa(x1)
U8_gaa(x1, x2, x3, x4, x5, x6) = U8_gaa(x1, x3, x6)
U9_gaa(x1, x2, x3, x4, x5, x6) = U9_gaa(x1, x3, x6)
U11_gaaa(x1, x2, x3, x4, x5) = U11_gaaa(x1, x5)
pB_out_gaaaa(x1, x2, x3, x4, x5) = pB_out_gaaaa(x1, x2)
goalA_out_g(x1) = goalA_out_g(x1)
U2_g(x1, x2) = U2_g(x1, x2)
pC_in_gaaaa(x1, x2, x3, x4, x5) = pC_in_gaaaa(x1)
U14_gaaaa(x1, x2, x3, x4, x5, x6) = U14_gaaaa(x1, x6)
U15_gaaaa(x1, x2, x3, x4, x5, x6) = U15_gaaaa(x1, x2, x6)
pC_out_gaaaa(x1, x2, x3, x4, x5) = pC_out_gaaaa(x1, x2)
U3_g(x1, x2) = U3_g(x1, x2)
pD_in_gaaaa(x1, x2, x3, x4, x5) = pD_in_gaaaa(x1)
U16_gaaaa(x1, x2, x3, x4, x5, x6) = U16_gaaaa(x1, x6)
U17_gaaaa(x1, x2, x3, x4, x5, x6) = U17_gaaaa(x1, x2, x6)
pD_out_gaaaa(x1, x2, x3, x4, x5) = pD_out_gaaaa(x1, x2)
U4_g(x1, x2) = U4_g(x1, x2)
GOALA_IN_G(x1) = GOALA_IN_G(x1)
U1_G(x1, x2) = U1_G(x1, x2)
PB_IN_GAAAA(x1, x2, x3, x4, x5) = PB_IN_GAAAA(x1)
U12_GAAAA(x1, x2, x3, x4, x5, x6) = U12_GAAAA(x1, x6)
S2TF_IN_GA(x1, x2) = S2TF_IN_GA(x1)
U5_GA(x1, x2, x3, x4) = U5_GA(x1, x4)
U6_GA(x1, x2, x3, x4) = U6_GA(x1, x4)
U7_GA(x1, x2, x3, x4) = U7_GA(x1, x4)
U13_GAAAA(x1, x2, x3, x4, x5, x6) = U13_GAAAA(x1, x2, x6)
TAPPENDG_IN_GAAA(x1, x2, x3, x4) = TAPPENDG_IN_GAAA(x1)
U10_GAAA(x1, x2, x3, x4, x5) = U10_GAAA(x1, x5)
TAPPENDE_IN_GAA(x1, x2, x3) = TAPPENDE_IN_GAA(x1)
U8_GAA(x1, x2, x3, x4, x5, x6) = U8_GAA(x1, x3, x6)
U9_GAA(x1, x2, x3, x4, x5, x6) = U9_GAA(x1, x3, x6)
U11_GAAA(x1, x2, x3, x4, x5) = U11_GAAA(x1, x5)
U2_G(x1, x2) = U2_G(x1, x2)
PC_IN_GAAAA(x1, x2, x3, x4, x5) = PC_IN_GAAAA(x1)
U14_GAAAA(x1, x2, x3, x4, x5, x6) = U14_GAAAA(x1, x6)
U15_GAAAA(x1, x2, x3, x4, x5, x6) = U15_GAAAA(x1, x2, x6)
U3_G(x1, x2) = U3_G(x1, x2)
PD_IN_GAAAA(x1, x2, x3, x4, x5) = PD_IN_GAAAA(x1)
U16_GAAAA(x1, x2, x3, x4, x5, x6) = U16_GAAAA(x1, x6)
U17_GAAAA(x1, x2, x3, x4, x5, x6) = U17_GAAAA(x1, x2, x6)
U4_G(x1, x2) = U4_G(x1, x2)

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(s(T11)) → U1_G(T11, pB_in_gaaaa(T11, X29, X30, X4, X5))
GOALA_IN_G(s(T11)) → PB_IN_GAAAA(T11, X29, X30, X4, X5)
PB_IN_GAAAA(T11, T13, X30, X4, X5) → U12_GAAAA(T11, T13, X30, X4, X5, s2tF_in_ga(T11, T13))
PB_IN_GAAAA(T11, T13, X30, X4, X5) → S2TF_IN_GA(T11, T13)
S2TF_IN_GA(s(T19), node(X64, X65, X64)) → U5_GA(T19, X64, X65, s2tF_in_ga(T19, X64))
S2TF_IN_GA(s(T19), node(X64, X65, X64)) → S2TF_IN_GA(T19, X64)
S2TF_IN_GA(s(T25), node(nil, X94, X95)) → U6_GA(T25, X94, X95, s2tF_in_ga(T25, X95))
S2TF_IN_GA(s(T25), node(nil, X94, X95)) → S2TF_IN_GA(T25, X95)
S2TF_IN_GA(s(T31), node(X124, X125, nil)) → U7_GA(T31, X124, X125, s2tF_in_ga(T31, X124))
S2TF_IN_GA(s(T31), node(X124, X125, nil)) → S2TF_IN_GA(T31, X124)
U12_GAAAA(T11, T13, X30, X4, X5, s2tF_out_ga(T11, T13)) → U13_GAAAA(T11, T13, X30, X4, X5, tappendG_in_gaaa(T13, X30, X4, X5))
U12_GAAAA(T11, T13, X30, X4, X5, s2tF_out_ga(T11, T13)) → TAPPENDG_IN_GAAA(T13, X30, X4, X5)
TAPPENDG_IN_GAAA(T50, X244, X245, node(X246, X244, T50)) → U10_GAAA(T50, X244, X245, X246, tappendE_in_gaa(T50, X245, X246))
TAPPENDG_IN_GAAA(T50, X244, X245, node(X246, X244, T50)) → TAPPENDE_IN_GAA(T50, X245, X246)
TAPPENDE_IN_GAA(node(T86, T84, T85), X334, node(X335, T84, T85)) → U8_GAA(T86, T84, T85, X334, X335, tappendE_in_gaa(T86, X334, X335))
TAPPENDE_IN_GAA(node(T86, T84, T85), X334, node(X335, T84, T85)) → TAPPENDE_IN_GAA(T86, X334, X335)
TAPPENDE_IN_GAA(node(T93, T94, T96), X359, node(T93, T94, X360)) → U9_GAA(T93, T94, T96, X359, X360, tappendE_in_gaa(T96, X359, X360))
TAPPENDE_IN_GAA(node(T93, T94, T96), X359, node(T93, T94, X360)) → TAPPENDE_IN_GAA(T96, X359, X360)
TAPPENDG_IN_GAAA(T101, X390, X391, node(T101, X390, X392)) → U11_GAAA(T101, X390, X391, X392, tappendE_in_gaa(T101, X391, X392))
TAPPENDG_IN_GAAA(T101, X390, X391, node(T101, X390, X392)) → TAPPENDE_IN_GAA(T101, X391, X392)
GOALA_IN_G(s(T106)) → U2_G(T106, pC_in_gaaaa(T106, X421, X420, X4, X5))
GOALA_IN_G(s(T106)) → PC_IN_GAAAA(T106, X421, X420, X4, X5)
PC_IN_GAAAA(T106, T108, X420, X4, X5) → U14_GAAAA(T106, T108, X420, X4, X5, s2tF_in_ga(T106, T108))
PC_IN_GAAAA(T106, T108, X420, X4, X5) → S2TF_IN_GA(T106, T108)
U14_GAAAA(T106, T108, X420, X4, X5, s2tF_out_ga(T106, T108)) → U15_GAAAA(T106, T108, X420, X4, X5, tappendE_in_gaa(node(nil, X420, T108), X4, X5))
U14_GAAAA(T106, T108, X420, X4, X5, s2tF_out_ga(T106, T108)) → TAPPENDE_IN_GAA(node(nil, X420, T108), X4, X5)
GOALA_IN_G(s(T114)) → U3_G(T114, pD_in_gaaaa(T114, X457, X458, X4, X5))
GOALA_IN_G(s(T114)) → PD_IN_GAAAA(T114, X457, X458, X4, X5)
PD_IN_GAAAA(T114, T116, X458, X4, X5) → U16_GAAAA(T114, T116, X458, X4, X5, s2tF_in_ga(T114, T116))
PD_IN_GAAAA(T114, T116, X458, X4, X5) → S2TF_IN_GA(T114, T116)
U16_GAAAA(T114, T116, X458, X4, X5, s2tF_out_ga(T114, T116)) → U17_GAAAA(T114, T116, X458, X4, X5, tappendE_in_gaa(node(T116, X458, nil), X4, X5))
U16_GAAAA(T114, T116, X458, X4, X5, s2tF_out_ga(T114, T116)) → TAPPENDE_IN_GAA(node(T116, X458, nil), X4, X5)
GOALA_IN_G(s(T122)) → U4_G(T122, tappendE_in_gaa(node(nil, X485, nil), X4, X5))
GOALA_IN_G(s(T122)) → TAPPENDE_IN_GAA(node(nil, X485, nil), X4, X5)

The TRS R consists of the following rules:

goalA_in_g(s(T11)) → U1_g(T11, pB_in_gaaaa(T11, X29, X30, X4, X5))
pB_in_gaaaa(T11, T13, X30, X4, X5) → U12_gaaaa(T11, T13, X30, X4, X5, s2tF_in_ga(T11, T13))
s2tF_in_ga(s(T19), node(X64, X65, X64)) → U5_ga(T19, X64, X65, s2tF_in_ga(T19, X64))
s2tF_in_ga(s(T25), node(nil, X94, X95)) → U6_ga(T25, X94, X95, s2tF_in_ga(T25, X95))
s2tF_in_ga(s(T31), node(X124, X125, nil)) → U7_ga(T31, X124, X125, s2tF_in_ga(T31, X124))
s2tF_in_ga(s(T37), node(nil, X145, nil)) → s2tF_out_ga(s(T37), node(nil, X145, nil))
s2tF_in_ga(0, nil) → s2tF_out_ga(0, nil)
U7_ga(T31, X124, X125, s2tF_out_ga(T31, X124)) → s2tF_out_ga(s(T31), node(X124, X125, nil))
U6_ga(T25, X94, X95, s2tF_out_ga(T25, X95)) → s2tF_out_ga(s(T25), node(nil, X94, X95))
U5_ga(T19, X64, X65, s2tF_out_ga(T19, X64)) → s2tF_out_ga(s(T19), node(X64, X65, X64))
U12_gaaaa(T11, T13, X30, X4, X5, s2tF_out_ga(T11, T13)) → U13_gaaaa(T11, T13, X30, X4, X5, tappendG_in_gaaa(T13, X30, X4, X5))
tappendG_in_gaaa(nil, X172, X173, node(X173, X172, nil)) → tappendG_out_gaaa(nil, X172, X173, node(X173, X172, nil))
tappendG_in_gaaa(nil, X197, X198, node(nil, X197, X198)) → tappendG_out_gaaa(nil, X197, X198, node(nil, X197, X198))
tappendG_in_gaaa(T50, X244, X245, node(X246, X244, T50)) → U10_gaaa(T50, X244, X245, X246, tappendE_in_gaa(T50, X245, X246))
tappendE_in_gaa(nil, X260, X260) → tappendE_out_gaa(nil, X260, X260)
tappendE_in_gaa(node(nil, T59, T60), X280, node(X280, T59, T60)) → tappendE_out_gaa(node(nil, T59, T60), X280, node(X280, T59, T60))
tappendE_in_gaa(node(T69, T70, nil), X300, node(T69, T70, X300)) → tappendE_out_gaa(node(T69, T70, nil), X300, node(T69, T70, X300))
tappendE_in_gaa(node(T86, T84, T85), X334, node(X335, T84, T85)) → U8_gaa(T86, T84, T85, X334, X335, tappendE_in_gaa(T86, X334, X335))
tappendE_in_gaa(node(T93, T94, T96), X359, node(T93, T94, X360)) → U9_gaa(T93, T94, T96, X359, X360, tappendE_in_gaa(T96, X359, X360))
U9_gaa(T93, T94, T96, X359, X360, tappendE_out_gaa(T96, X359, X360)) → tappendE_out_gaa(node(T93, T94, T96), X359, node(T93, T94, X360))
U8_gaa(T86, T84, T85, X334, X335, tappendE_out_gaa(T86, X334, X335)) → tappendE_out_gaa(node(T86, T84, T85), X334, node(X335, T84, T85))
U10_gaaa(T50, X244, X245, X246, tappendE_out_gaa(T50, X245, X246)) → tappendG_out_gaaa(T50, X244, X245, node(X246, X244, T50))
tappendG_in_gaaa(T101, X390, X391, node(T101, X390, X392)) → U11_gaaa(T101, X390, X391, X392, tappendE_in_gaa(T101, X391, X392))
U11_gaaa(T101, X390, X391, X392, tappendE_out_gaa(T101, X391, X392)) → tappendG_out_gaaa(T101, X390, X391, node(T101, X390, X392))
U13_gaaaa(T11, T13, X30, X4, X5, tappendG_out_gaaa(T13, X30, X4, X5)) → pB_out_gaaaa(T11, T13, X30, X4, X5)
U1_g(T11, pB_out_gaaaa(T11, X29, X30, X4, X5)) → goalA_out_g(s(T11))
goalA_in_g(s(T106)) → U2_g(T106, pC_in_gaaaa(T106, X421, X420, X4, X5))
pC_in_gaaaa(T106, T108, X420, X4, X5) → U14_gaaaa(T106, T108, X420, X4, X5, s2tF_in_ga(T106, T108))
U14_gaaaa(T106, T108, X420, X4, X5, s2tF_out_ga(T106, T108)) → U15_gaaaa(T106, T108, X420, X4, X5, tappendE_in_gaa(node(nil, X420, T108), X4, X5))
U15_gaaaa(T106, T108, X420, X4, X5, tappendE_out_gaa(node(nil, X420, T108), X4, X5)) → pC_out_gaaaa(T106, T108, X420, X4, X5)
U2_g(T106, pC_out_gaaaa(T106, X421, X420, X4, X5)) → goalA_out_g(s(T106))
goalA_in_g(s(T114)) → U3_g(T114, pD_in_gaaaa(T114, X457, X458, X4, X5))
pD_in_gaaaa(T114, T116, X458, X4, X5) → U16_gaaaa(T114, T116, X458, X4, X5, s2tF_in_ga(T114, T116))
U16_gaaaa(T114, T116, X458, X4, X5, s2tF_out_ga(T114, T116)) → U17_gaaaa(T114, T116, X458, X4, X5, tappendE_in_gaa(node(T116, X458, nil), X4, X5))
U17_gaaaa(T114, T116, X458, X4, X5, tappendE_out_gaa(node(T116, X458, nil), X4, X5)) → pD_out_gaaaa(T114, T116, X458, X4, X5)
U3_g(T114, pD_out_gaaaa(T114, X457, X458, X4, X5)) → goalA_out_g(s(T114))
goalA_in_g(s(T122)) → U4_g(T122, tappendE_in_gaa(node(nil, X485, nil), X4, X5))
U4_g(T122, tappendE_out_gaa(node(nil, X485, nil), X4, X5)) → goalA_out_g(s(T122))
goalA_in_g(0) → goalA_out_g(0)

(5) DependencyGraphProof (EQUIVALENT transformation)

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

(6) Complex Obligation (AND)

(7) Obligation:

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

TAPPENDE_IN_GAA(node(T93, T94, T96), X359, node(T93, T94, X360)) → TAPPENDE_IN_GAA(T96, X359, X360)
TAPPENDE_IN_GAA(node(T86, T84, T85), X334, node(X335, T84, T85)) → TAPPENDE_IN_GAA(T86, X334, X335)

The TRS R consists of the following rules:

goalA_in_g(s(T11)) → U1_g(T11, pB_in_gaaaa(T11, X29, X30, X4, X5))
pB_in_gaaaa(T11, T13, X30, X4, X5) → U12_gaaaa(T11, T13, X30, X4, X5, s2tF_in_ga(T11, T13))
s2tF_in_ga(s(T19), node(X64, X65, X64)) → U5_ga(T19, X64, X65, s2tF_in_ga(T19, X64))
s2tF_in_ga(s(T25), node(nil, X94, X95)) → U6_ga(T25, X94, X95, s2tF_in_ga(T25, X95))
s2tF_in_ga(s(T31), node(X124, X125, nil)) → U7_ga(T31, X124, X125, s2tF_in_ga(T31, X124))
s2tF_in_ga(s(T37), node(nil, X145, nil)) → s2tF_out_ga(s(T37), node(nil, X145, nil))
s2tF_in_ga(0, nil) → s2tF_out_ga(0, nil)
U7_ga(T31, X124, X125, s2tF_out_ga(T31, X124)) → s2tF_out_ga(s(T31), node(X124, X125, nil))
U6_ga(T25, X94, X95, s2tF_out_ga(T25, X95)) → s2tF_out_ga(s(T25), node(nil, X94, X95))
U5_ga(T19, X64, X65, s2tF_out_ga(T19, X64)) → s2tF_out_ga(s(T19), node(X64, X65, X64))
U12_gaaaa(T11, T13, X30, X4, X5, s2tF_out_ga(T11, T13)) → U13_gaaaa(T11, T13, X30, X4, X5, tappendG_in_gaaa(T13, X30, X4, X5))
tappendG_in_gaaa(nil, X172, X173, node(X173, X172, nil)) → tappendG_out_gaaa(nil, X172, X173, node(X173, X172, nil))
tappendG_in_gaaa(nil, X197, X198, node(nil, X197, X198)) → tappendG_out_gaaa(nil, X197, X198, node(nil, X197, X198))
tappendG_in_gaaa(T50, X244, X245, node(X246, X244, T50)) → U10_gaaa(T50, X244, X245, X246, tappendE_in_gaa(T50, X245, X246))
tappendE_in_gaa(nil, X260, X260) → tappendE_out_gaa(nil, X260, X260)
tappendE_in_gaa(node(nil, T59, T60), X280, node(X280, T59, T60)) → tappendE_out_gaa(node(nil, T59, T60), X280, node(X280, T59, T60))
tappendE_in_gaa(node(T69, T70, nil), X300, node(T69, T70, X300)) → tappendE_out_gaa(node(T69, T70, nil), X300, node(T69, T70, X300))
tappendE_in_gaa(node(T86, T84, T85), X334, node(X335, T84, T85)) → U8_gaa(T86, T84, T85, X334, X335, tappendE_in_gaa(T86, X334, X335))
tappendE_in_gaa(node(T93, T94, T96), X359, node(T93, T94, X360)) → U9_gaa(T93, T94, T96, X359, X360, tappendE_in_gaa(T96, X359, X360))
U9_gaa(T93, T94, T96, X359, X360, tappendE_out_gaa(T96, X359, X360)) → tappendE_out_gaa(node(T93, T94, T96), X359, node(T93, T94, X360))
U8_gaa(T86, T84, T85, X334, X335, tappendE_out_gaa(T86, X334, X335)) → tappendE_out_gaa(node(T86, T84, T85), X334, node(X335, T84, T85))
U10_gaaa(T50, X244, X245, X246, tappendE_out_gaa(T50, X245, X246)) → tappendG_out_gaaa(T50, X244, X245, node(X246, X244, T50))
tappendG_in_gaaa(T101, X390, X391, node(T101, X390, X392)) → U11_gaaa(T101, X390, X391, X392, tappendE_in_gaa(T101, X391, X392))
U11_gaaa(T101, X390, X391, X392, tappendE_out_gaa(T101, X391, X392)) → tappendG_out_gaaa(T101, X390, X391, node(T101, X390, X392))
U13_gaaaa(T11, T13, X30, X4, X5, tappendG_out_gaaa(T13, X30, X4, X5)) → pB_out_gaaaa(T11, T13, X30, X4, X5)
U1_g(T11, pB_out_gaaaa(T11, X29, X30, X4, X5)) → goalA_out_g(s(T11))
goalA_in_g(s(T106)) → U2_g(T106, pC_in_gaaaa(T106, X421, X420, X4, X5))
pC_in_gaaaa(T106, T108, X420, X4, X5) → U14_gaaaa(T106, T108, X420, X4, X5, s2tF_in_ga(T106, T108))
U14_gaaaa(T106, T108, X420, X4, X5, s2tF_out_ga(T106, T108)) → U15_gaaaa(T106, T108, X420, X4, X5, tappendE_in_gaa(node(nil, X420, T108), X4, X5))
U15_gaaaa(T106, T108, X420, X4, X5, tappendE_out_gaa(node(nil, X420, T108), X4, X5)) → pC_out_gaaaa(T106, T108, X420, X4, X5)
U2_g(T106, pC_out_gaaaa(T106, X421, X420, X4, X5)) → goalA_out_g(s(T106))
goalA_in_g(s(T114)) → U3_g(T114, pD_in_gaaaa(T114, X457, X458, X4, X5))
pD_in_gaaaa(T114, T116, X458, X4, X5) → U16_gaaaa(T114, T116, X458, X4, X5, s2tF_in_ga(T114, T116))
U16_gaaaa(T114, T116, X458, X4, X5, s2tF_out_ga(T114, T116)) → U17_gaaaa(T114, T116, X458, X4, X5, tappendE_in_gaa(node(T116, X458, nil), X4, X5))
U17_gaaaa(T114, T116, X458, X4, X5, tappendE_out_gaa(node(T116, X458, nil), X4, X5)) → pD_out_gaaaa(T114, T116, X458, X4, X5)
U3_g(T114, pD_out_gaaaa(T114, X457, X458, X4, X5)) → goalA_out_g(s(T114))
goalA_in_g(s(T122)) → U4_g(T122, tappendE_in_gaa(node(nil, X485, nil), X4, X5))
U4_g(T122, tappendE_out_gaa(node(nil, X485, nil), X4, X5)) → goalA_out_g(s(T122))
goalA_in_g(0) → goalA_out_g(0)

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

TAPPENDE_IN_GAA(node(T93, T94, T96), X359, node(T93, T94, X360)) → TAPPENDE_IN_GAA(T96, X359, X360)
TAPPENDE_IN_GAA(node(T86, T84, T85), X334, node(X335, T84, T85)) → TAPPENDE_IN_GAA(T86, X334, X335)

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

TAPPENDE_IN_GAA(node(T93, T96)) → TAPPENDE_IN_GAA(T96)
TAPPENDE_IN_GAA(node(T86, T85)) → TAPPENDE_IN_GAA(T86)

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:

TAPPENDE_IN_GAA(node(T93, T96)) → TAPPENDE_IN_GAA(T96)
The graph contains the following edges 1 > 1
TAPPENDE_IN_GAA(node(T86, T85)) → TAPPENDE_IN_GAA(T86)
The graph contains the following edges 1 > 1

(13) YES

(14) Obligation:

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

S2TF_IN_GA(s(T25), node(nil, X94, X95)) → S2TF_IN_GA(T25, X95)
S2TF_IN_GA(s(T19), node(X64, X65, X64)) → S2TF_IN_GA(T19, X64)
S2TF_IN_GA(s(T31), node(X124, X125, nil)) → S2TF_IN_GA(T31, X124)

The TRS R consists of the following rules:

goalA_in_g(s(T11)) → U1_g(T11, pB_in_gaaaa(T11, X29, X30, X4, X5))
pB_in_gaaaa(T11, T13, X30, X4, X5) → U12_gaaaa(T11, T13, X30, X4, X5, s2tF_in_ga(T11, T13))
s2tF_in_ga(s(T19), node(X64, X65, X64)) → U5_ga(T19, X64, X65, s2tF_in_ga(T19, X64))
s2tF_in_ga(s(T25), node(nil, X94, X95)) → U6_ga(T25, X94, X95, s2tF_in_ga(T25, X95))
s2tF_in_ga(s(T31), node(X124, X125, nil)) → U7_ga(T31, X124, X125, s2tF_in_ga(T31, X124))
s2tF_in_ga(s(T37), node(nil, X145, nil)) → s2tF_out_ga(s(T37), node(nil, X145, nil))
s2tF_in_ga(0, nil) → s2tF_out_ga(0, nil)
U7_ga(T31, X124, X125, s2tF_out_ga(T31, X124)) → s2tF_out_ga(s(T31), node(X124, X125, nil))
U6_ga(T25, X94, X95, s2tF_out_ga(T25, X95)) → s2tF_out_ga(s(T25), node(nil, X94, X95))
U5_ga(T19, X64, X65, s2tF_out_ga(T19, X64)) → s2tF_out_ga(s(T19), node(X64, X65, X64))
U12_gaaaa(T11, T13, X30, X4, X5, s2tF_out_ga(T11, T13)) → U13_gaaaa(T11, T13, X30, X4, X5, tappendG_in_gaaa(T13, X30, X4, X5))
tappendG_in_gaaa(nil, X172, X173, node(X173, X172, nil)) → tappendG_out_gaaa(nil, X172, X173, node(X173, X172, nil))
tappendG_in_gaaa(nil, X197, X198, node(nil, X197, X198)) → tappendG_out_gaaa(nil, X197, X198, node(nil, X197, X198))
tappendG_in_gaaa(T50, X244, X245, node(X246, X244, T50)) → U10_gaaa(T50, X244, X245, X246, tappendE_in_gaa(T50, X245, X246))
tappendE_in_gaa(nil, X260, X260) → tappendE_out_gaa(nil, X260, X260)
tappendE_in_gaa(node(nil, T59, T60), X280, node(X280, T59, T60)) → tappendE_out_gaa(node(nil, T59, T60), X280, node(X280, T59, T60))
tappendE_in_gaa(node(T69, T70, nil), X300, node(T69, T70, X300)) → tappendE_out_gaa(node(T69, T70, nil), X300, node(T69, T70, X300))
tappendE_in_gaa(node(T86, T84, T85), X334, node(X335, T84, T85)) → U8_gaa(T86, T84, T85, X334, X335, tappendE_in_gaa(T86, X334, X335))
tappendE_in_gaa(node(T93, T94, T96), X359, node(T93, T94, X360)) → U9_gaa(T93, T94, T96, X359, X360, tappendE_in_gaa(T96, X359, X360))
U9_gaa(T93, T94, T96, X359, X360, tappendE_out_gaa(T96, X359, X360)) → tappendE_out_gaa(node(T93, T94, T96), X359, node(T93, T94, X360))
U8_gaa(T86, T84, T85, X334, X335, tappendE_out_gaa(T86, X334, X335)) → tappendE_out_gaa(node(T86, T84, T85), X334, node(X335, T84, T85))
U10_gaaa(T50, X244, X245, X246, tappendE_out_gaa(T50, X245, X246)) → tappendG_out_gaaa(T50, X244, X245, node(X246, X244, T50))
tappendG_in_gaaa(T101, X390, X391, node(T101, X390, X392)) → U11_gaaa(T101, X390, X391, X392, tappendE_in_gaa(T101, X391, X392))
U11_gaaa(T101, X390, X391, X392, tappendE_out_gaa(T101, X391, X392)) → tappendG_out_gaaa(T101, X390, X391, node(T101, X390, X392))
U13_gaaaa(T11, T13, X30, X4, X5, tappendG_out_gaaa(T13, X30, X4, X5)) → pB_out_gaaaa(T11, T13, X30, X4, X5)
U1_g(T11, pB_out_gaaaa(T11, X29, X30, X4, X5)) → goalA_out_g(s(T11))
goalA_in_g(s(T106)) → U2_g(T106, pC_in_gaaaa(T106, X421, X420, X4, X5))
pC_in_gaaaa(T106, T108, X420, X4, X5) → U14_gaaaa(T106, T108, X420, X4, X5, s2tF_in_ga(T106, T108))
U14_gaaaa(T106, T108, X420, X4, X5, s2tF_out_ga(T106, T108)) → U15_gaaaa(T106, T108, X420, X4, X5, tappendE_in_gaa(node(nil, X420, T108), X4, X5))
U15_gaaaa(T106, T108, X420, X4, X5, tappendE_out_gaa(node(nil, X420, T108), X4, X5)) → pC_out_gaaaa(T106, T108, X420, X4, X5)
U2_g(T106, pC_out_gaaaa(T106, X421, X420, X4, X5)) → goalA_out_g(s(T106))
goalA_in_g(s(T114)) → U3_g(T114, pD_in_gaaaa(T114, X457, X458, X4, X5))
pD_in_gaaaa(T114, T116, X458, X4, X5) → U16_gaaaa(T114, T116, X458, X4, X5, s2tF_in_ga(T114, T116))
U16_gaaaa(T114, T116, X458, X4, X5, s2tF_out_ga(T114, T116)) → U17_gaaaa(T114, T116, X458, X4, X5, tappendE_in_gaa(node(T116, X458, nil), X4, X5))
U17_gaaaa(T114, T116, X458, X4, X5, tappendE_out_gaa(node(T116, X458, nil), X4, X5)) → pD_out_gaaaa(T114, T116, X458, X4, X5)
U3_g(T114, pD_out_gaaaa(T114, X457, X458, X4, X5)) → goalA_out_g(s(T114))
goalA_in_g(s(T122)) → U4_g(T122, tappendE_in_gaa(node(nil, X485, nil), X4, X5))
U4_g(T122, tappendE_out_gaa(node(nil, X485, nil), X4, X5)) → goalA_out_g(s(T122))
goalA_in_g(0) → goalA_out_g(0)

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

S2TF_IN_GA(s(T25), node(nil, X94, X95)) → S2TF_IN_GA(T25, X95)
S2TF_IN_GA(s(T19), node(X64, X65, X64)) → S2TF_IN_GA(T19, X64)
S2TF_IN_GA(s(T31), node(X124, X125, nil)) → S2TF_IN_GA(T31, X124)

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

S2TF_IN_GA(s(T25)) → S2TF_IN_GA(T25)

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:

S2TF_IN_GA(s(T25)) → S2TF_IN_GA(T25)
The graph contains the following edges 1 > 1

(0) Obligation:

(1) PrologToPiTRSViaGraphTransformerProof (SOUND transformation)

(2) Obligation:

(3) DependencyPairsProof (EQUIVALENT transformation)

(4) Obligation:

(5) DependencyGraphProof (EQUIVALENT transformation)

(6) Complex Obligation (AND)

(7) Obligation:

(8) UsableRulesProof (EQUIVALENT transformation)

(9) Obligation:

(10) PiDPToQDPProof (SOUND transformation)

(11) Obligation:

(12) QDPSizeChangeProof (EQUIVALENT transformation)

(13) YES

(14) Obligation:

(15) UsableRulesProof (EQUIVALENT transformation)

(16) Obligation:

(17) PiDPToQDPProof (SOUND transformation)

(18) Obligation:

(19) QDPSizeChangeProof (EQUIVALENT transformation)

(20) YES