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

(0) Obligation:

Clauses:

perm([], []).
perm(.(X, L), Z) :- ','(perm(L, Y), insert(X, Y, Z)).
insert(X, [], .(X, [])).
insert(X, L, .(X, L)).
insert(X, .(H, L1), .(H, L2)) :- insert(X, L1, L2).

Query: perm(g,a)

(1) PrologToPiTRSViaGraphTransformerProof (SOUND transformation)

Transformed Prolog program to (Pi-)TRS.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
3 [label="A: perm(T1, T2)\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
5 [label="5: perm(T1, T2), SCOPE: 1, CLAUSE: 0 | perm(T1, T2), SCOPE: 1, CLAUSE: 1\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
10 [label="10: true | perm([], T2), SCOPE: 1, CLAUSE: 1\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
14 [label="14: perm(T1, T2), SCOPE: 1, CLAUSE: 1\n\nT1 is ground\nperm(T1, T2) !=? perm([], [])", fontsize=16, style=filled, fillcolor=lightyellow];
17 [label="17: perm([], T2), SCOPE: 1, CLAUSE: 1\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
19 [label="19: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
23 [label="23: ','(perm(T7, X10), insert(T6, X10, T9))\n\nT6 is ground\nT7 is ground\nX10 is free", fontsize=16, style=filled, fillcolor=lightyellow];
25 [label="25: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
27 [label="27: ','(perm(T7, X10), insert(T6, X10, T9)), SCOPE: 2, CLAUSE: 0 | ','(perm(T7, X10), insert(T6, X10, T9)), SCOPE: 2, CLAUSE: 1\n\nT6 is ground\nT7 is ground\nX10 is free", fontsize=16, style=filled, fillcolor=lightyellow];
30 [label="30: ','(perm(T7, X10), insert(T6, X10, T9)), SCOPE: 2, CLAUSE: 0\n\nT6 is ground\nT7 is ground\nX10 is free", fontsize=16, style=filled, fillcolor=lightyellow];
31 [label="31: ','(perm(T7, X10), insert(T6, X10, T9)), SCOPE: 2, CLAUSE: 1\n\nT6 is ground\nT7 is ground\nX10 is free", fontsize=16, style=filled, fillcolor=lightyellow];
34 [label="34: insert(T6, [], T9)\n\nT6 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
35 [label="35: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
37 [label="37: insert(T6, [], T9), SCOPE: 3, CLAUSE: 2 | insert(T6, [], T9), SCOPE: 3, CLAUSE: 3 | insert(T6, [], T9), SCOPE: 3, CLAUSE: 4\n\nT6 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
39 [label="39: insert(T6, [], T9), SCOPE: 3, CLAUSE: 2\n\nT6 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
41 [label="41: insert(T6, [], T9), SCOPE: 3, CLAUSE: 3 | insert(T6, [], T9), SCOPE: 3, CLAUSE: 4\n\nT6 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
46 [label="46: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
48 [label="48: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
49 [label="49: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
54 [label="54: insert(T6, [], T9), SCOPE: 3, CLAUSE: 3\n\nT6 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
56 [label="56: insert(T6, [], T9), SCOPE: 3, CLAUSE: 4\n\nT6 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
63 [label="63: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
65 [label="65: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
66 [label="66: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
68 [label="68: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
72 [label="B: ','(','(perm(T28, X44), insert(T27, X44, X45)), insert(T6, X45, T9))\n\nT6 is ground\nT27 is ground\nT28 is ground\nX45 is free\nX44 is free", fontsize=16, style=filled, fillcolor=lightyellow];
73 [label="73: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
77 [label="C: perm(T28, X44)\n\nT28 is ground\nX44 is free", fontsize=16, style=filled, fillcolor=lightyellow];
78 [label="G: ','(insert(T27, T29, X45), insert(T6, X45, T9))\n\nT6 is ground\nT27 is ground\nT29 is ground\nX45 is free", fontsize=16, style=filled, fillcolor=lightyellow];
84 [label="84: perm(T28, X44), SCOPE: 4, CLAUSE: 0 | perm(T28, X44), SCOPE: 4, CLAUSE: 1\n\nT28 is ground\nX44 is free", fontsize=16, style=filled, fillcolor=lightyellow];
85 [label="85: perm(T28, X44), SCOPE: 4, CLAUSE: 0\n\nT28 is ground\nX44 is free", fontsize=16, style=filled, fillcolor=lightyellow];
86 [label="86: perm(T28, X44), SCOPE: 4, CLAUSE: 1\n\nT28 is ground\nX44 is free", fontsize=16, style=filled, fillcolor=lightyellow];
87 [label="87: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
88 [label="88: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
89 [label="89: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
94 [label="D: ','(perm(T35, X58), insert(T34, X58, X59))\n\nT34 is ground\nT35 is ground\nX59 is free\nX58 is free", fontsize=16, style=filled, fillcolor=lightyellow];
95 [label="95: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
99 [label="99: perm(T35, X58)\n\nT35 is ground\nX58 is free", fontsize=16, style=filled, fillcolor=lightyellow];
100 [label="E: insert(T34, T36, X59)\n\nT34 is ground\nT36 is ground\nX59 is free", fontsize=16, style=filled, fillcolor=lightyellow];
108 [label="108: insert(T34, T36, X59), SCOPE: 5, CLAUSE: 2 | insert(T34, T36, X59), SCOPE: 5, CLAUSE: 3 | insert(T34, T36, X59), SCOPE: 5, CLAUSE: 4\n\nT34 is ground\nT36 is ground\nX59 is free", fontsize=16, style=filled, fillcolor=lightyellow];
113 [label="113: insert(T34, T36, X59), SCOPE: 5, CLAUSE: 2\n\nT34 is ground\nT36 is ground\nX59 is free", fontsize=16, style=filled, fillcolor=lightyellow];
114 [label="114: insert(T34, T36, X59), SCOPE: 5, CLAUSE: 3 | insert(T34, T36, X59), SCOPE: 5, CLAUSE: 4\n\nT34 is ground\nT36 is ground\nX59 is free", fontsize=16, style=filled, fillcolor=lightyellow];
117 [label="117: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
120 [label="120: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
121 [label="121: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
122 [label="122: insert(T34, T36, X59), SCOPE: 5, CLAUSE: 3\n\nT34 is ground\nT36 is ground\nX59 is free", fontsize=16, style=filled, fillcolor=lightyellow];
123 [label="123: insert(T34, T36, X59), SCOPE: 5, CLAUSE: 4\n\nT34 is ground\nT36 is ground\nX59 is free", fontsize=16, style=filled, fillcolor=lightyellow];
126 [label="126: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
127 [label="127: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
132 [label="132: insert(T60, T62, X91)\n\nT60 is ground\nT62 is ground\nX91 is free", fontsize=16, style=filled, fillcolor=lightyellow];
133 [label="133: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
138 [label="138: insert(T27, T29, X45)\n\nT27 is ground\nT29 is ground\nX45 is free", fontsize=16, style=filled, fillcolor=lightyellow];
139 [label="F: insert(T6, T67, T9)\n\nT6 is ground\nT67 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
142 [label="142: insert(T6, T67, T9), SCOPE: 6, CLAUSE: 2 | insert(T6, T67, T9), SCOPE: 6, CLAUSE: 3 | insert(T6, T67, T9), SCOPE: 6, CLAUSE: 4\n\nT6 is ground\nT67 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
144 [label="144: insert(T6, T67, T9), SCOPE: 6, CLAUSE: 2\n\nT6 is ground\nT67 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
145 [label="145: insert(T6, T67, T9), SCOPE: 6, CLAUSE: 3 | insert(T6, T67, T9), SCOPE: 6, CLAUSE: 4\n\nT6 is ground\nT67 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
149 [label="149: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
151 [label="151: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
153 [label="153: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
154 [label="154: insert(T6, T67, T9), SCOPE: 6, CLAUSE: 3\n\nT6 is ground\nT67 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
155 [label="155: insert(T6, T67, T9), SCOPE: 6, CLAUSE: 4\n\nT6 is ground\nT67 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
162 [label="162: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
163 [label="163: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
165 [label="165: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
172 [label="172: insert(T95, T97, T99)\n\nT95 is ground\nT97 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
173 [label="173: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
174 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
3 -> 174 [arrowhead = none ];
174 -> 5;

175 [label="EVAL with clause\nperm([], []).\nand substitutionT1 -> [],\nT2 -> []", fontsize=14, style = filled, fillcolor = lightblue];
5 -> 175 [arrowhead = none ];
175 -> 10;

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

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

178 [label="EVAL with clause\nperm(.(X7, X8), X9) :- ','(perm(X8, X10), insert(X7, X10, X9)).\nand substitutionX7 -> T6,\nX8 -> T7,\nT1 -> .(T6, T7),\nT2 -> T9,\nX9 -> T9,\nT8 -> T9", fontsize=14, style = filled, fillcolor = lightblue];
14 -> 178 [arrowhead = none ];
178 -> 23;

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

180 [label="BACKTRACK\nfor clause: perm(.(X, L), Z) :- ','(perm(L, Y), insert(X, Y, Z))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
17 -> 180 [arrowhead = none ];
180 -> 19;

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

182 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
27 -> 182 [arrowhead = none ];
182 -> 30;

183 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
27 -> 183 [arrowhead = none ];
183 -> 31;

184 [label="EVAL with clause\nperm([], []).\nand substitutionT7 -> [],\nX10 -> []", fontsize=14, style = filled, fillcolor = lightblue];
30 -> 184 [arrowhead = none ];
184 -> 34;

185 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
30 -> 185 [arrowhead = none ];
185 -> 35;

186 [label="EVAL with clause\nperm(.(X41, X42), X43) :- ','(perm(X42, X44), insert(X41, X44, X43)).\nand substitutionX41 -> T27,\nX42 -> T28,\nT7 -> .(T27, T28),\nX10 -> X45,\nX43 -> X45", fontsize=14, style = filled, fillcolor = lightblue];
31 -> 186 [arrowhead = none ];
186 -> 72;

187 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
31 -> 187 [arrowhead = none ];
187 -> 73;

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

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

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

191 [label="EVAL with clause\ninsert(X17, [], .(X17, [])).\nand substitutionT6 -> T16,\nX17 -> T16,\nT9 -> .(T16, [])", fontsize=14, style = filled, fillcolor = lightblue];
39 -> 191 [arrowhead = none ];
191 -> 46;

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

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

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

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

196 [label="EVAL with clause\ninsert(X26, X27, .(X26, X27)).\nand substitutionT6 -> T21,\nX26 -> T21,\nX27 -> [],\nT9 -> .(T21, [])", fontsize=14, style = filled, fillcolor = lightblue];
54 -> 196 [arrowhead = none ];
196 -> 63;

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

198 [label="BACKTRACK\nfor clause: insert(X, .(H, L1), .(H, L2)) :- insert(X, L1, L2)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
56 -> 198 [arrowhead = none ];
198 -> 68;

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

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

201 [label="SPLIT 2\nnew knowledge:\nT28 is ground\nT29 is ground\nreplacements:X44 -> T29", fontsize=14, style = filled, fillcolor = violet];
72 -> 201 [arrowhead = none ];
201 -> 78;

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

203 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
78 -> 203 [arrowhead = none ];
203 -> 138;

204 [label="SPLIT 2\nnew knowledge:\nT27 is ground\nT29 is ground\nT67 is ground\nreplacements:X45 -> T67", fontsize=14, style = filled, fillcolor = violet];
78 -> 204 [arrowhead = none ];
204 -> 139;

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

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

207 [label="EVAL with clause\nperm([], []).\nand substitutionT28 -> [],\nX44 -> []", fontsize=14, style = filled, fillcolor = lightblue];
85 -> 207 [arrowhead = none ];
207 -> 87;

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

209 [label="EVAL with clause\nperm(.(X55, X56), X57) :- ','(perm(X56, X58), insert(X55, X58, X57)).\nand substitutionX55 -> T34,\nX56 -> T35,\nT28 -> .(T34, T35),\nX44 -> X59,\nX57 -> X59", fontsize=14, style = filled, fillcolor = lightblue];
86 -> 209 [arrowhead = none ];
209 -> 94;

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

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

212 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
94 -> 212 [arrowhead = none ];
212 -> 99;

213 [label="SPLIT 2\nnew knowledge:\nT35 is ground\nT36 is ground\nreplacements:X58 -> T36", fontsize=14, style = filled, fillcolor = violet];
94 -> 213 [arrowhead = none ];
213 -> 100;

214 [label="INSTANCE with matching:\nT28 -> T35\nX44 -> X58", fontsize=14, style = filled, fillcolor = lightgrey];
99 -> 214 [arrowhead = none , style=dashed];
214 -> 77[style=dashed];

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

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

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

218 [label="EVAL with clause\ninsert(X66, [], .(X66, [])).\nand substitutionT34 -> T43,\nX66 -> T43,\nT36 -> [],\nX59 -> .(T43, [])", fontsize=14, style = filled, fillcolor = lightblue];
113 -> 218 [arrowhead = none ];
218 -> 117;

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

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

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

222 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
117 -> 222 [arrowhead = none ];
222 -> 121;

223 [label="ONLY EVAL with clause\ninsert(X75, X76, .(X75, X76)).\nand substitutionT34 -> T52,\nX75 -> T52,\nT36 -> T53,\nX76 -> T53,\nX59 -> .(T52, T53)", fontsize=14, style = filled, fillcolor = lightblue];
122 -> 223 [arrowhead = none ];
223 -> 126;

224 [label="EVAL with clause\ninsert(X87, .(X88, X89), .(X88, X90)) :- insert(X87, X89, X90).\nand substitutionT34 -> T60,\nX87 -> T60,\nX88 -> T61,\nX89 -> T62,\nT36 -> .(T61, T62),\nX90 -> X91,\nX59 -> .(T61, X91)", fontsize=14, style = filled, fillcolor = lightblue];
123 -> 224 [arrowhead = none ];
224 -> 132;

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

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

227 [label="INSTANCE with matching:\nT34 -> T60\nT36 -> T62\nX59 -> X91", fontsize=14, style = filled, fillcolor = lightgrey];
132 -> 227 [arrowhead = none , style=dashed];
227 -> 100[style=dashed];

228 [label="INSTANCE with matching:\nT34 -> T27\nT36 -> T29\nX59 -> X45", fontsize=14, style = filled, fillcolor = lightgrey];
138 -> 228 [arrowhead = none , style=dashed];
228 -> 100[style=dashed];

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

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

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

232 [label="EVAL with clause\ninsert(X104, [], .(X104, [])).\nand substitutionT6 -> T76,\nX104 -> T76,\nT67 -> [],\nT9 -> .(T76, [])", fontsize=14, style = filled, fillcolor = lightblue];
144 -> 232 [arrowhead = none ];
232 -> 149;

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

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

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

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

237 [label="EVAL with clause\ninsert(X113, X114, .(X113, X114)).\nand substitutionT6 -> T85,\nX113 -> T85,\nT67 -> T86,\nX114 -> T86,\nT9 -> .(T85, T86)", fontsize=14, style = filled, fillcolor = lightblue];
154 -> 237 [arrowhead = none ];
237 -> 162;

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

239 [label="EVAL with clause\ninsert(X123, .(X124, X125), .(X124, X126)) :- insert(X123, X125, X126).\nand substitutionT6 -> T95,\nX123 -> T95,\nX124 -> T96,\nX125 -> T97,\nT67 -> .(T96, T97),\nX126 -> T99,\nT9 -> .(T96, T99),\nT98 -> T99", fontsize=14, style = filled, fillcolor = lightblue];
155 -> 239 [arrowhead = none ];
239 -> 172;

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

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

242 [label="INSTANCE with matching:\nT6 -> T95\nT67 -> T97\nT9 -> T99", fontsize=14, style = filled, fillcolor = lightgrey];
172 -> 242 [arrowhead = none , style=dashed];
242 -> 139[style=dashed];

}

(2) Obligation:

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

permA_in_ga([], []) → permA_out_ga([], [])
permA_in_ga(.(T16, []), .(T16, [])) → permA_out_ga(.(T16, []), .(T16, []))
permA_in_ga(.(T6, .(T27, T28)), T9) → U1_ga(T6, T27, T28, T9, pB_in_gagaga(T28, X44, T27, X45, T6, T9))
pB_in_gagaga(T28, T29, T27, X45, T6, T9) → U5_gagaga(T28, T29, T27, X45, T6, T9, permC_in_ga(T28, T29))
permC_in_ga([], []) → permC_out_ga([], [])
permC_in_ga(.(T34, T35), X59) → U2_ga(T34, T35, X59, pD_in_gaga(T35, X58, T34, X59))
pD_in_gaga(T35, T36, T34, X59) → U9_gaga(T35, T36, T34, X59, permC_in_ga(T35, T36))
U9_gaga(T35, T36, T34, X59, permC_out_ga(T35, T36)) → U10_gaga(T35, T36, T34, X59, insertE_in_gga(T34, T36, X59))
insertE_in_gga(T43, [], .(T43, [])) → insertE_out_gga(T43, [], .(T43, []))
insertE_in_gga(T52, T53, .(T52, T53)) → insertE_out_gga(T52, T53, .(T52, T53))
insertE_in_gga(T60, .(T61, T62), .(T61, X91)) → U3_gga(T60, T61, T62, X91, insertE_in_gga(T60, T62, X91))
U3_gga(T60, T61, T62, X91, insertE_out_gga(T60, T62, X91)) → insertE_out_gga(T60, .(T61, T62), .(T61, X91))
U10_gaga(T35, T36, T34, X59, insertE_out_gga(T34, T36, X59)) → pD_out_gaga(T35, T36, T34, X59)
U2_ga(T34, T35, X59, pD_out_gaga(T35, X58, T34, X59)) → permC_out_ga(.(T34, T35), X59)
U5_gagaga(T28, T29, T27, X45, T6, T9, permC_out_ga(T28, T29)) → U6_gagaga(T28, T29, T27, X45, T6, T9, pG_in_ggaga(T27, T29, X45, T6, T9))
pG_in_ggaga(T27, T29, T67, T6, T9) → U7_ggaga(T27, T29, T67, T6, T9, insertE_in_gga(T27, T29, T67))
U7_ggaga(T27, T29, T67, T6, T9, insertE_out_gga(T27, T29, T67)) → U8_ggaga(T27, T29, T67, T6, T9, insertF_in_gga(T6, T67, T9))
insertF_in_gga(T76, [], .(T76, [])) → insertF_out_gga(T76, [], .(T76, []))
insertF_in_gga(T85, T86, .(T85, T86)) → insertF_out_gga(T85, T86, .(T85, T86))
insertF_in_gga(T95, .(T96, T97), .(T96, T99)) → U4_gga(T95, T96, T97, T99, insertF_in_gga(T95, T97, T99))
U4_gga(T95, T96, T97, T99, insertF_out_gga(T95, T97, T99)) → insertF_out_gga(T95, .(T96, T97), .(T96, T99))
U8_ggaga(T27, T29, T67, T6, T9, insertF_out_gga(T6, T67, T9)) → pG_out_ggaga(T27, T29, T67, T6, T9)
U6_gagaga(T28, T29, T27, X45, T6, T9, pG_out_ggaga(T27, T29, X45, T6, T9)) → pB_out_gagaga(T28, T29, T27, X45, T6, T9)
U1_ga(T6, T27, T28, T9, pB_out_gagaga(T28, X44, T27, X45, T6, T9)) → permA_out_ga(.(T6, .(T27, T28)), T9)

The argument filtering Pi contains the following mapping:
permA_in_ga(x1, x2)  =  permA_in_ga(x1)
[]  =  []
permA_out_ga(x1, x2)  =  permA_out_ga(x1, x2)
.(x1, x2)  =  .(x1, x2)
U1_ga(x1, x2, x3, x4, x5)  =  U1_ga(x1, x2, x3, x5)
pB_in_gagaga(x1, x2, x3, x4, x5, x6)  =  pB_in_gagaga(x1, x3, x5)
U5_gagaga(x1, x2, x3, x4, x5, x6, x7)  =  U5_gagaga(x1, x3, x5, x7)
permC_in_ga(x1, x2)  =  permC_in_ga(x1)
permC_out_ga(x1, x2)  =  permC_out_ga(x1, x2)
U2_ga(x1, x2, x3, x4)  =  U2_ga(x1, x2, x4)
pD_in_gaga(x1, x2, x3, x4)  =  pD_in_gaga(x1, x3)
U9_gaga(x1, x2, x3, x4, x5)  =  U9_gaga(x1, x3, x5)
U10_gaga(x1, x2, x3, x4, x5)  =  U10_gaga(x1, x2, x3, x5)
insertE_in_gga(x1, x2, x3)  =  insertE_in_gga(x1, x2)
insertE_out_gga(x1, x2, x3)  =  insertE_out_gga(x1, x2, x3)
U3_gga(x1, x2, x3, x4, x5)  =  U3_gga(x1, x2, x3, x5)
pD_out_gaga(x1, x2, x3, x4)  =  pD_out_gaga(x1, x2, x3, x4)
U6_gagaga(x1, x2, x3, x4, x5, x6, x7)  =  U6_gagaga(x1, x2, x3, x5, x7)
pG_in_ggaga(x1, x2, x3, x4, x5)  =  pG_in_ggaga(x1, x2, x4)
U7_ggaga(x1, x2, x3, x4, x5, x6)  =  U7_ggaga(x1, x2, x4, x6)
U8_ggaga(x1, x2, x3, x4, x5, x6)  =  U8_ggaga(x1, x2, x3, x4, x6)
insertF_in_gga(x1, x2, x3)  =  insertF_in_gga(x1, x2)
insertF_out_gga(x1, x2, x3)  =  insertF_out_gga(x1, x2, x3)
U4_gga(x1, x2, x3, x4, x5)  =  U4_gga(x1, x2, x3, x5)
pG_out_ggaga(x1, x2, x3, x4, x5)  =  pG_out_ggaga(x1, x2, x3, x4, x5)
pB_out_gagaga(x1, x2, x3, x4, x5, x6)  =  pB_out_gagaga(x1, x2, x3, x4, x5, x6)

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

PERMA_IN_GA(.(T6, .(T27, T28)), T9) → U1_GA(T6, T27, T28, T9, pB_in_gagaga(T28, X44, T27, X45, T6, T9))
PERMA_IN_GA(.(T6, .(T27, T28)), T9) → PB_IN_GAGAGA(T28, X44, T27, X45, T6, T9)
PB_IN_GAGAGA(T28, T29, T27, X45, T6, T9) → U5_GAGAGA(T28, T29, T27, X45, T6, T9, permC_in_ga(T28, T29))
PB_IN_GAGAGA(T28, T29, T27, X45, T6, T9) → PERMC_IN_GA(T28, T29)
PERMC_IN_GA(.(T34, T35), X59) → U2_GA(T34, T35, X59, pD_in_gaga(T35, X58, T34, X59))
PERMC_IN_GA(.(T34, T35), X59) → PD_IN_GAGA(T35, X58, T34, X59)
PD_IN_GAGA(T35, T36, T34, X59) → U9_GAGA(T35, T36, T34, X59, permC_in_ga(T35, T36))
PD_IN_GAGA(T35, T36, T34, X59) → PERMC_IN_GA(T35, T36)
U9_GAGA(T35, T36, T34, X59, permC_out_ga(T35, T36)) → U10_GAGA(T35, T36, T34, X59, insertE_in_gga(T34, T36, X59))
U9_GAGA(T35, T36, T34, X59, permC_out_ga(T35, T36)) → INSERTE_IN_GGA(T34, T36, X59)
INSERTE_IN_GGA(T60, .(T61, T62), .(T61, X91)) → U3_GGA(T60, T61, T62, X91, insertE_in_gga(T60, T62, X91))
INSERTE_IN_GGA(T60, .(T61, T62), .(T61, X91)) → INSERTE_IN_GGA(T60, T62, X91)
U5_GAGAGA(T28, T29, T27, X45, T6, T9, permC_out_ga(T28, T29)) → U6_GAGAGA(T28, T29, T27, X45, T6, T9, pG_in_ggaga(T27, T29, X45, T6, T9))
U5_GAGAGA(T28, T29, T27, X45, T6, T9, permC_out_ga(T28, T29)) → PG_IN_GGAGA(T27, T29, X45, T6, T9)
PG_IN_GGAGA(T27, T29, T67, T6, T9) → U7_GGAGA(T27, T29, T67, T6, T9, insertE_in_gga(T27, T29, T67))
PG_IN_GGAGA(T27, T29, T67, T6, T9) → INSERTE_IN_GGA(T27, T29, T67)
U7_GGAGA(T27, T29, T67, T6, T9, insertE_out_gga(T27, T29, T67)) → U8_GGAGA(T27, T29, T67, T6, T9, insertF_in_gga(T6, T67, T9))
U7_GGAGA(T27, T29, T67, T6, T9, insertE_out_gga(T27, T29, T67)) → INSERTF_IN_GGA(T6, T67, T9)
INSERTF_IN_GGA(T95, .(T96, T97), .(T96, T99)) → U4_GGA(T95, T96, T97, T99, insertF_in_gga(T95, T97, T99))
INSERTF_IN_GGA(T95, .(T96, T97), .(T96, T99)) → INSERTF_IN_GGA(T95, T97, T99)

The TRS R consists of the following rules:

permA_in_ga([], []) → permA_out_ga([], [])
permA_in_ga(.(T16, []), .(T16, [])) → permA_out_ga(.(T16, []), .(T16, []))
permA_in_ga(.(T6, .(T27, T28)), T9) → U1_ga(T6, T27, T28, T9, pB_in_gagaga(T28, X44, T27, X45, T6, T9))
pB_in_gagaga(T28, T29, T27, X45, T6, T9) → U5_gagaga(T28, T29, T27, X45, T6, T9, permC_in_ga(T28, T29))
permC_in_ga([], []) → permC_out_ga([], [])
permC_in_ga(.(T34, T35), X59) → U2_ga(T34, T35, X59, pD_in_gaga(T35, X58, T34, X59))
pD_in_gaga(T35, T36, T34, X59) → U9_gaga(T35, T36, T34, X59, permC_in_ga(T35, T36))
U9_gaga(T35, T36, T34, X59, permC_out_ga(T35, T36)) → U10_gaga(T35, T36, T34, X59, insertE_in_gga(T34, T36, X59))
insertE_in_gga(T43, [], .(T43, [])) → insertE_out_gga(T43, [], .(T43, []))
insertE_in_gga(T52, T53, .(T52, T53)) → insertE_out_gga(T52, T53, .(T52, T53))
insertE_in_gga(T60, .(T61, T62), .(T61, X91)) → U3_gga(T60, T61, T62, X91, insertE_in_gga(T60, T62, X91))
U3_gga(T60, T61, T62, X91, insertE_out_gga(T60, T62, X91)) → insertE_out_gga(T60, .(T61, T62), .(T61, X91))
U10_gaga(T35, T36, T34, X59, insertE_out_gga(T34, T36, X59)) → pD_out_gaga(T35, T36, T34, X59)
U2_ga(T34, T35, X59, pD_out_gaga(T35, X58, T34, X59)) → permC_out_ga(.(T34, T35), X59)
U5_gagaga(T28, T29, T27, X45, T6, T9, permC_out_ga(T28, T29)) → U6_gagaga(T28, T29, T27, X45, T6, T9, pG_in_ggaga(T27, T29, X45, T6, T9))
pG_in_ggaga(T27, T29, T67, T6, T9) → U7_ggaga(T27, T29, T67, T6, T9, insertE_in_gga(T27, T29, T67))
U7_ggaga(T27, T29, T67, T6, T9, insertE_out_gga(T27, T29, T67)) → U8_ggaga(T27, T29, T67, T6, T9, insertF_in_gga(T6, T67, T9))
insertF_in_gga(T76, [], .(T76, [])) → insertF_out_gga(T76, [], .(T76, []))
insertF_in_gga(T85, T86, .(T85, T86)) → insertF_out_gga(T85, T86, .(T85, T86))
insertF_in_gga(T95, .(T96, T97), .(T96, T99)) → U4_gga(T95, T96, T97, T99, insertF_in_gga(T95, T97, T99))
U4_gga(T95, T96, T97, T99, insertF_out_gga(T95, T97, T99)) → insertF_out_gga(T95, .(T96, T97), .(T96, T99))
U8_ggaga(T27, T29, T67, T6, T9, insertF_out_gga(T6, T67, T9)) → pG_out_ggaga(T27, T29, T67, T6, T9)
U6_gagaga(T28, T29, T27, X45, T6, T9, pG_out_ggaga(T27, T29, X45, T6, T9)) → pB_out_gagaga(T28, T29, T27, X45, T6, T9)
U1_ga(T6, T27, T28, T9, pB_out_gagaga(T28, X44, T27, X45, T6, T9)) → permA_out_ga(.(T6, .(T27, T28)), T9)

The argument filtering Pi contains the following mapping:
permA_in_ga(x1, x2)  =  permA_in_ga(x1)
[]  =  []
permA_out_ga(x1, x2)  =  permA_out_ga(x1, x2)
.(x1, x2)  =  .(x1, x2)
U1_ga(x1, x2, x3, x4, x5)  =  U1_ga(x1, x2, x3, x5)
pB_in_gagaga(x1, x2, x3, x4, x5, x6)  =  pB_in_gagaga(x1, x3, x5)
U5_gagaga(x1, x2, x3, x4, x5, x6, x7)  =  U5_gagaga(x1, x3, x5, x7)
permC_in_ga(x1, x2)  =  permC_in_ga(x1)
permC_out_ga(x1, x2)  =  permC_out_ga(x1, x2)
U2_ga(x1, x2, x3, x4)  =  U2_ga(x1, x2, x4)
pD_in_gaga(x1, x2, x3, x4)  =  pD_in_gaga(x1, x3)
U9_gaga(x1, x2, x3, x4, x5)  =  U9_gaga(x1, x3, x5)
U10_gaga(x1, x2, x3, x4, x5)  =  U10_gaga(x1, x2, x3, x5)
insertE_in_gga(x1, x2, x3)  =  insertE_in_gga(x1, x2)
insertE_out_gga(x1, x2, x3)  =  insertE_out_gga(x1, x2, x3)
U3_gga(x1, x2, x3, x4, x5)  =  U3_gga(x1, x2, x3, x5)
pD_out_gaga(x1, x2, x3, x4)  =  pD_out_gaga(x1, x2, x3, x4)
U6_gagaga(x1, x2, x3, x4, x5, x6, x7)  =  U6_gagaga(x1, x2, x3, x5, x7)
pG_in_ggaga(x1, x2, x3, x4, x5)  =  pG_in_ggaga(x1, x2, x4)
U7_ggaga(x1, x2, x3, x4, x5, x6)  =  U7_ggaga(x1, x2, x4, x6)
U8_ggaga(x1, x2, x3, x4, x5, x6)  =  U8_ggaga(x1, x2, x3, x4, x6)
insertF_in_gga(x1, x2, x3)  =  insertF_in_gga(x1, x2)
insertF_out_gga(x1, x2, x3)  =  insertF_out_gga(x1, x2, x3)
U4_gga(x1, x2, x3, x4, x5)  =  U4_gga(x1, x2, x3, x5)
pG_out_ggaga(x1, x2, x3, x4, x5)  =  pG_out_ggaga(x1, x2, x3, x4, x5)
pB_out_gagaga(x1, x2, x3, x4, x5, x6)  =  pB_out_gagaga(x1, x2, x3, x4, x5, x6)
PERMA_IN_GA(x1, x2)  =  PERMA_IN_GA(x1)
U1_GA(x1, x2, x3, x4, x5)  =  U1_GA(x1, x2, x3, x5)
PB_IN_GAGAGA(x1, x2, x3, x4, x5, x6)  =  PB_IN_GAGAGA(x1, x3, x5)
U5_GAGAGA(x1, x2, x3, x4, x5, x6, x7)  =  U5_GAGAGA(x1, x3, x5, x7)
PERMC_IN_GA(x1, x2)  =  PERMC_IN_GA(x1)
U2_GA(x1, x2, x3, x4)  =  U2_GA(x1, x2, x4)
PD_IN_GAGA(x1, x2, x3, x4)  =  PD_IN_GAGA(x1, x3)
U9_GAGA(x1, x2, x3, x4, x5)  =  U9_GAGA(x1, x3, x5)
U10_GAGA(x1, x2, x3, x4, x5)  =  U10_GAGA(x1, x2, x3, x5)
INSERTE_IN_GGA(x1, x2, x3)  =  INSERTE_IN_GGA(x1, x2)
U3_GGA(x1, x2, x3, x4, x5)  =  U3_GGA(x1, x2, x3, x5)
U6_GAGAGA(x1, x2, x3, x4, x5, x6, x7)  =  U6_GAGAGA(x1, x2, x3, x5, x7)
PG_IN_GGAGA(x1, x2, x3, x4, x5)  =  PG_IN_GGAGA(x1, x2, x4)
U7_GGAGA(x1, x2, x3, x4, x5, x6)  =  U7_GGAGA(x1, x2, x4, x6)
U8_GGAGA(x1, x2, x3, x4, x5, x6)  =  U8_GGAGA(x1, x2, x3, x4, x6)
INSERTF_IN_GGA(x1, x2, x3)  =  INSERTF_IN_GGA(x1, x2)
U4_GGA(x1, x2, x3, x4, x5)  =  U4_GGA(x1, x2, x3, x5)

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

(4) Obligation:

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

PERMA_IN_GA(.(T6, .(T27, T28)), T9) → U1_GA(T6, T27, T28, T9, pB_in_gagaga(T28, X44, T27, X45, T6, T9))
PERMA_IN_GA(.(T6, .(T27, T28)), T9) → PB_IN_GAGAGA(T28, X44, T27, X45, T6, T9)
PB_IN_GAGAGA(T28, T29, T27, X45, T6, T9) → U5_GAGAGA(T28, T29, T27, X45, T6, T9, permC_in_ga(T28, T29))
PB_IN_GAGAGA(T28, T29, T27, X45, T6, T9) → PERMC_IN_GA(T28, T29)
PERMC_IN_GA(.(T34, T35), X59) → U2_GA(T34, T35, X59, pD_in_gaga(T35, X58, T34, X59))
PERMC_IN_GA(.(T34, T35), X59) → PD_IN_GAGA(T35, X58, T34, X59)
PD_IN_GAGA(T35, T36, T34, X59) → U9_GAGA(T35, T36, T34, X59, permC_in_ga(T35, T36))
PD_IN_GAGA(T35, T36, T34, X59) → PERMC_IN_GA(T35, T36)
U9_GAGA(T35, T36, T34, X59, permC_out_ga(T35, T36)) → U10_GAGA(T35, T36, T34, X59, insertE_in_gga(T34, T36, X59))
U9_GAGA(T35, T36, T34, X59, permC_out_ga(T35, T36)) → INSERTE_IN_GGA(T34, T36, X59)
INSERTE_IN_GGA(T60, .(T61, T62), .(T61, X91)) → U3_GGA(T60, T61, T62, X91, insertE_in_gga(T60, T62, X91))
INSERTE_IN_GGA(T60, .(T61, T62), .(T61, X91)) → INSERTE_IN_GGA(T60, T62, X91)
U5_GAGAGA(T28, T29, T27, X45, T6, T9, permC_out_ga(T28, T29)) → U6_GAGAGA(T28, T29, T27, X45, T6, T9, pG_in_ggaga(T27, T29, X45, T6, T9))
U5_GAGAGA(T28, T29, T27, X45, T6, T9, permC_out_ga(T28, T29)) → PG_IN_GGAGA(T27, T29, X45, T6, T9)
PG_IN_GGAGA(T27, T29, T67, T6, T9) → U7_GGAGA(T27, T29, T67, T6, T9, insertE_in_gga(T27, T29, T67))
PG_IN_GGAGA(T27, T29, T67, T6, T9) → INSERTE_IN_GGA(T27, T29, T67)
U7_GGAGA(T27, T29, T67, T6, T9, insertE_out_gga(T27, T29, T67)) → U8_GGAGA(T27, T29, T67, T6, T9, insertF_in_gga(T6, T67, T9))
U7_GGAGA(T27, T29, T67, T6, T9, insertE_out_gga(T27, T29, T67)) → INSERTF_IN_GGA(T6, T67, T9)
INSERTF_IN_GGA(T95, .(T96, T97), .(T96, T99)) → U4_GGA(T95, T96, T97, T99, insertF_in_gga(T95, T97, T99))
INSERTF_IN_GGA(T95, .(T96, T97), .(T96, T99)) → INSERTF_IN_GGA(T95, T97, T99)

The TRS R consists of the following rules:

permA_in_ga([], []) → permA_out_ga([], [])
permA_in_ga(.(T16, []), .(T16, [])) → permA_out_ga(.(T16, []), .(T16, []))
permA_in_ga(.(T6, .(T27, T28)), T9) → U1_ga(T6, T27, T28, T9, pB_in_gagaga(T28, X44, T27, X45, T6, T9))
pB_in_gagaga(T28, T29, T27, X45, T6, T9) → U5_gagaga(T28, T29, T27, X45, T6, T9, permC_in_ga(T28, T29))
permC_in_ga([], []) → permC_out_ga([], [])
permC_in_ga(.(T34, T35), X59) → U2_ga(T34, T35, X59, pD_in_gaga(T35, X58, T34, X59))
pD_in_gaga(T35, T36, T34, X59) → U9_gaga(T35, T36, T34, X59, permC_in_ga(T35, T36))
U9_gaga(T35, T36, T34, X59, permC_out_ga(T35, T36)) → U10_gaga(T35, T36, T34, X59, insertE_in_gga(T34, T36, X59))
insertE_in_gga(T43, [], .(T43, [])) → insertE_out_gga(T43, [], .(T43, []))
insertE_in_gga(T52, T53, .(T52, T53)) → insertE_out_gga(T52, T53, .(T52, T53))
insertE_in_gga(T60, .(T61, T62), .(T61, X91)) → U3_gga(T60, T61, T62, X91, insertE_in_gga(T60, T62, X91))
U3_gga(T60, T61, T62, X91, insertE_out_gga(T60, T62, X91)) → insertE_out_gga(T60, .(T61, T62), .(T61, X91))
U10_gaga(T35, T36, T34, X59, insertE_out_gga(T34, T36, X59)) → pD_out_gaga(T35, T36, T34, X59)
U2_ga(T34, T35, X59, pD_out_gaga(T35, X58, T34, X59)) → permC_out_ga(.(T34, T35), X59)
U5_gagaga(T28, T29, T27, X45, T6, T9, permC_out_ga(T28, T29)) → U6_gagaga(T28, T29, T27, X45, T6, T9, pG_in_ggaga(T27, T29, X45, T6, T9))
pG_in_ggaga(T27, T29, T67, T6, T9) → U7_ggaga(T27, T29, T67, T6, T9, insertE_in_gga(T27, T29, T67))
U7_ggaga(T27, T29, T67, T6, T9, insertE_out_gga(T27, T29, T67)) → U8_ggaga(T27, T29, T67, T6, T9, insertF_in_gga(T6, T67, T9))
insertF_in_gga(T76, [], .(T76, [])) → insertF_out_gga(T76, [], .(T76, []))
insertF_in_gga(T85, T86, .(T85, T86)) → insertF_out_gga(T85, T86, .(T85, T86))
insertF_in_gga(T95, .(T96, T97), .(T96, T99)) → U4_gga(T95, T96, T97, T99, insertF_in_gga(T95, T97, T99))
U4_gga(T95, T96, T97, T99, insertF_out_gga(T95, T97, T99)) → insertF_out_gga(T95, .(T96, T97), .(T96, T99))
U8_ggaga(T27, T29, T67, T6, T9, insertF_out_gga(T6, T67, T9)) → pG_out_ggaga(T27, T29, T67, T6, T9)
U6_gagaga(T28, T29, T27, X45, T6, T9, pG_out_ggaga(T27, T29, X45, T6, T9)) → pB_out_gagaga(T28, T29, T27, X45, T6, T9)
U1_ga(T6, T27, T28, T9, pB_out_gagaga(T28, X44, T27, X45, T6, T9)) → permA_out_ga(.(T6, .(T27, T28)), T9)

The argument filtering Pi contains the following mapping:
permA_in_ga(x1, x2)  =  permA_in_ga(x1)
[]  =  []
permA_out_ga(x1, x2)  =  permA_out_ga(x1, x2)
.(x1, x2)  =  .(x1, x2)
U1_ga(x1, x2, x3, x4, x5)  =  U1_ga(x1, x2, x3, x5)
pB_in_gagaga(x1, x2, x3, x4, x5, x6)  =  pB_in_gagaga(x1, x3, x5)
U5_gagaga(x1, x2, x3, x4, x5, x6, x7)  =  U5_gagaga(x1, x3, x5, x7)
permC_in_ga(x1, x2)  =  permC_in_ga(x1)
permC_out_ga(x1, x2)  =  permC_out_ga(x1, x2)
U2_ga(x1, x2, x3, x4)  =  U2_ga(x1, x2, x4)
pD_in_gaga(x1, x2, x3, x4)  =  pD_in_gaga(x1, x3)
U9_gaga(x1, x2, x3, x4, x5)  =  U9_gaga(x1, x3, x5)
U10_gaga(x1, x2, x3, x4, x5)  =  U10_gaga(x1, x2, x3, x5)
insertE_in_gga(x1, x2, x3)  =  insertE_in_gga(x1, x2)
insertE_out_gga(x1, x2, x3)  =  insertE_out_gga(x1, x2, x3)
U3_gga(x1, x2, x3, x4, x5)  =  U3_gga(x1, x2, x3, x5)
pD_out_gaga(x1, x2, x3, x4)  =  pD_out_gaga(x1, x2, x3, x4)
U6_gagaga(x1, x2, x3, x4, x5, x6, x7)  =  U6_gagaga(x1, x2, x3, x5, x7)
pG_in_ggaga(x1, x2, x3, x4, x5)  =  pG_in_ggaga(x1, x2, x4)
U7_ggaga(x1, x2, x3, x4, x5, x6)  =  U7_ggaga(x1, x2, x4, x6)
U8_ggaga(x1, x2, x3, x4, x5, x6)  =  U8_ggaga(x1, x2, x3, x4, x6)
insertF_in_gga(x1, x2, x3)  =  insertF_in_gga(x1, x2)
insertF_out_gga(x1, x2, x3)  =  insertF_out_gga(x1, x2, x3)
U4_gga(x1, x2, x3, x4, x5)  =  U4_gga(x1, x2, x3, x5)
pG_out_ggaga(x1, x2, x3, x4, x5)  =  pG_out_ggaga(x1, x2, x3, x4, x5)
pB_out_gagaga(x1, x2, x3, x4, x5, x6)  =  pB_out_gagaga(x1, x2, x3, x4, x5, x6)
PERMA_IN_GA(x1, x2)  =  PERMA_IN_GA(x1)
U1_GA(x1, x2, x3, x4, x5)  =  U1_GA(x1, x2, x3, x5)
PB_IN_GAGAGA(x1, x2, x3, x4, x5, x6)  =  PB_IN_GAGAGA(x1, x3, x5)
U5_GAGAGA(x1, x2, x3, x4, x5, x6, x7)  =  U5_GAGAGA(x1, x3, x5, x7)
PERMC_IN_GA(x1, x2)  =  PERMC_IN_GA(x1)
U2_GA(x1, x2, x3, x4)  =  U2_GA(x1, x2, x4)
PD_IN_GAGA(x1, x2, x3, x4)  =  PD_IN_GAGA(x1, x3)
U9_GAGA(x1, x2, x3, x4, x5)  =  U9_GAGA(x1, x3, x5)
U10_GAGA(x1, x2, x3, x4, x5)  =  U10_GAGA(x1, x2, x3, x5)
INSERTE_IN_GGA(x1, x2, x3)  =  INSERTE_IN_GGA(x1, x2)
U3_GGA(x1, x2, x3, x4, x5)  =  U3_GGA(x1, x2, x3, x5)
U6_GAGAGA(x1, x2, x3, x4, x5, x6, x7)  =  U6_GAGAGA(x1, x2, x3, x5, x7)
PG_IN_GGAGA(x1, x2, x3, x4, x5)  =  PG_IN_GGAGA(x1, x2, x4)
U7_GGAGA(x1, x2, x3, x4, x5, x6)  =  U7_GGAGA(x1, x2, x4, x6)
U8_GGAGA(x1, x2, x3, x4, x5, x6)  =  U8_GGAGA(x1, x2, x3, x4, x6)
INSERTF_IN_GGA(x1, x2, x3)  =  INSERTF_IN_GGA(x1, x2)
U4_GGA(x1, x2, x3, x4, x5)  =  U4_GGA(x1, x2, x3, x5)

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

(5) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 3 SCCs with 16 less nodes.

(6) Complex Obligation (AND)

(7) Obligation:

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

INSERTF_IN_GGA(T95, .(T96, T97), .(T96, T99)) → INSERTF_IN_GGA(T95, T97, T99)

The TRS R consists of the following rules:

permA_in_ga([], []) → permA_out_ga([], [])
permA_in_ga(.(T16, []), .(T16, [])) → permA_out_ga(.(T16, []), .(T16, []))
permA_in_ga(.(T6, .(T27, T28)), T9) → U1_ga(T6, T27, T28, T9, pB_in_gagaga(T28, X44, T27, X45, T6, T9))
pB_in_gagaga(T28, T29, T27, X45, T6, T9) → U5_gagaga(T28, T29, T27, X45, T6, T9, permC_in_ga(T28, T29))
permC_in_ga([], []) → permC_out_ga([], [])
permC_in_ga(.(T34, T35), X59) → U2_ga(T34, T35, X59, pD_in_gaga(T35, X58, T34, X59))
pD_in_gaga(T35, T36, T34, X59) → U9_gaga(T35, T36, T34, X59, permC_in_ga(T35, T36))
U9_gaga(T35, T36, T34, X59, permC_out_ga(T35, T36)) → U10_gaga(T35, T36, T34, X59, insertE_in_gga(T34, T36, X59))
insertE_in_gga(T43, [], .(T43, [])) → insertE_out_gga(T43, [], .(T43, []))
insertE_in_gga(T52, T53, .(T52, T53)) → insertE_out_gga(T52, T53, .(T52, T53))
insertE_in_gga(T60, .(T61, T62), .(T61, X91)) → U3_gga(T60, T61, T62, X91, insertE_in_gga(T60, T62, X91))
U3_gga(T60, T61, T62, X91, insertE_out_gga(T60, T62, X91)) → insertE_out_gga(T60, .(T61, T62), .(T61, X91))
U10_gaga(T35, T36, T34, X59, insertE_out_gga(T34, T36, X59)) → pD_out_gaga(T35, T36, T34, X59)
U2_ga(T34, T35, X59, pD_out_gaga(T35, X58, T34, X59)) → permC_out_ga(.(T34, T35), X59)
U5_gagaga(T28, T29, T27, X45, T6, T9, permC_out_ga(T28, T29)) → U6_gagaga(T28, T29, T27, X45, T6, T9, pG_in_ggaga(T27, T29, X45, T6, T9))
pG_in_ggaga(T27, T29, T67, T6, T9) → U7_ggaga(T27, T29, T67, T6, T9, insertE_in_gga(T27, T29, T67))
U7_ggaga(T27, T29, T67, T6, T9, insertE_out_gga(T27, T29, T67)) → U8_ggaga(T27, T29, T67, T6, T9, insertF_in_gga(T6, T67, T9))
insertF_in_gga(T76, [], .(T76, [])) → insertF_out_gga(T76, [], .(T76, []))
insertF_in_gga(T85, T86, .(T85, T86)) → insertF_out_gga(T85, T86, .(T85, T86))
insertF_in_gga(T95, .(T96, T97), .(T96, T99)) → U4_gga(T95, T96, T97, T99, insertF_in_gga(T95, T97, T99))
U4_gga(T95, T96, T97, T99, insertF_out_gga(T95, T97, T99)) → insertF_out_gga(T95, .(T96, T97), .(T96, T99))
U8_ggaga(T27, T29, T67, T6, T9, insertF_out_gga(T6, T67, T9)) → pG_out_ggaga(T27, T29, T67, T6, T9)
U6_gagaga(T28, T29, T27, X45, T6, T9, pG_out_ggaga(T27, T29, X45, T6, T9)) → pB_out_gagaga(T28, T29, T27, X45, T6, T9)
U1_ga(T6, T27, T28, T9, pB_out_gagaga(T28, X44, T27, X45, T6, T9)) → permA_out_ga(.(T6, .(T27, T28)), T9)

The argument filtering Pi contains the following mapping:
permA_in_ga(x1, x2)  =  permA_in_ga(x1)
[]  =  []
permA_out_ga(x1, x2)  =  permA_out_ga(x1, x2)
.(x1, x2)  =  .(x1, x2)
U1_ga(x1, x2, x3, x4, x5)  =  U1_ga(x1, x2, x3, x5)
pB_in_gagaga(x1, x2, x3, x4, x5, x6)  =  pB_in_gagaga(x1, x3, x5)
U5_gagaga(x1, x2, x3, x4, x5, x6, x7)  =  U5_gagaga(x1, x3, x5, x7)
permC_in_ga(x1, x2)  =  permC_in_ga(x1)
permC_out_ga(x1, x2)  =  permC_out_ga(x1, x2)
U2_ga(x1, x2, x3, x4)  =  U2_ga(x1, x2, x4)
pD_in_gaga(x1, x2, x3, x4)  =  pD_in_gaga(x1, x3)
U9_gaga(x1, x2, x3, x4, x5)  =  U9_gaga(x1, x3, x5)
U10_gaga(x1, x2, x3, x4, x5)  =  U10_gaga(x1, x2, x3, x5)
insertE_in_gga(x1, x2, x3)  =  insertE_in_gga(x1, x2)
insertE_out_gga(x1, x2, x3)  =  insertE_out_gga(x1, x2, x3)
U3_gga(x1, x2, x3, x4, x5)  =  U3_gga(x1, x2, x3, x5)
pD_out_gaga(x1, x2, x3, x4)  =  pD_out_gaga(x1, x2, x3, x4)
U6_gagaga(x1, x2, x3, x4, x5, x6, x7)  =  U6_gagaga(x1, x2, x3, x5, x7)
pG_in_ggaga(x1, x2, x3, x4, x5)  =  pG_in_ggaga(x1, x2, x4)
U7_ggaga(x1, x2, x3, x4, x5, x6)  =  U7_ggaga(x1, x2, x4, x6)
U8_ggaga(x1, x2, x3, x4, x5, x6)  =  U8_ggaga(x1, x2, x3, x4, x6)
insertF_in_gga(x1, x2, x3)  =  insertF_in_gga(x1, x2)
insertF_out_gga(x1, x2, x3)  =  insertF_out_gga(x1, x2, x3)
U4_gga(x1, x2, x3, x4, x5)  =  U4_gga(x1, x2, x3, x5)
pG_out_ggaga(x1, x2, x3, x4, x5)  =  pG_out_ggaga(x1, x2, x3, x4, x5)
pB_out_gagaga(x1, x2, x3, x4, x5, x6)  =  pB_out_gagaga(x1, x2, x3, x4, x5, x6)
INSERTF_IN_GGA(x1, x2, x3)  =  INSERTF_IN_GGA(x1, x2)

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

(8) UsableRulesProof (EQUIVALENT transformation)

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

(9) Obligation:

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

INSERTF_IN_GGA(T95, .(T96, T97), .(T96, T99)) → INSERTF_IN_GGA(T95, T97, T99)

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

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

(10) PiDPToQDPProof (SOUND transformation)

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

(11) Obligation:

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

INSERTF_IN_GGA(T95, .(T96, T97)) → INSERTF_IN_GGA(T95, T97)

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:

• INSERTF_IN_GGA(T95, .(T96, T97)) → INSERTF_IN_GGA(T95, T97)
  The graph contains the following edges 1 >= 1, 2 > 2

(13) YES

(14) Obligation:

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

INSERTE_IN_GGA(T60, .(T61, T62), .(T61, X91)) → INSERTE_IN_GGA(T60, T62, X91)

The TRS R consists of the following rules:

permA_in_ga([], []) → permA_out_ga([], [])
permA_in_ga(.(T16, []), .(T16, [])) → permA_out_ga(.(T16, []), .(T16, []))
permA_in_ga(.(T6, .(T27, T28)), T9) → U1_ga(T6, T27, T28, T9, pB_in_gagaga(T28, X44, T27, X45, T6, T9))
pB_in_gagaga(T28, T29, T27, X45, T6, T9) → U5_gagaga(T28, T29, T27, X45, T6, T9, permC_in_ga(T28, T29))
permC_in_ga([], []) → permC_out_ga([], [])
permC_in_ga(.(T34, T35), X59) → U2_ga(T34, T35, X59, pD_in_gaga(T35, X58, T34, X59))
pD_in_gaga(T35, T36, T34, X59) → U9_gaga(T35, T36, T34, X59, permC_in_ga(T35, T36))
U9_gaga(T35, T36, T34, X59, permC_out_ga(T35, T36)) → U10_gaga(T35, T36, T34, X59, insertE_in_gga(T34, T36, X59))
insertE_in_gga(T43, [], .(T43, [])) → insertE_out_gga(T43, [], .(T43, []))
insertE_in_gga(T52, T53, .(T52, T53)) → insertE_out_gga(T52, T53, .(T52, T53))
insertE_in_gga(T60, .(T61, T62), .(T61, X91)) → U3_gga(T60, T61, T62, X91, insertE_in_gga(T60, T62, X91))
U3_gga(T60, T61, T62, X91, insertE_out_gga(T60, T62, X91)) → insertE_out_gga(T60, .(T61, T62), .(T61, X91))
U10_gaga(T35, T36, T34, X59, insertE_out_gga(T34, T36, X59)) → pD_out_gaga(T35, T36, T34, X59)
U2_ga(T34, T35, X59, pD_out_gaga(T35, X58, T34, X59)) → permC_out_ga(.(T34, T35), X59)
U5_gagaga(T28, T29, T27, X45, T6, T9, permC_out_ga(T28, T29)) → U6_gagaga(T28, T29, T27, X45, T6, T9, pG_in_ggaga(T27, T29, X45, T6, T9))
pG_in_ggaga(T27, T29, T67, T6, T9) → U7_ggaga(T27, T29, T67, T6, T9, insertE_in_gga(T27, T29, T67))
U7_ggaga(T27, T29, T67, T6, T9, insertE_out_gga(T27, T29, T67)) → U8_ggaga(T27, T29, T67, T6, T9, insertF_in_gga(T6, T67, T9))
insertF_in_gga(T76, [], .(T76, [])) → insertF_out_gga(T76, [], .(T76, []))
insertF_in_gga(T85, T86, .(T85, T86)) → insertF_out_gga(T85, T86, .(T85, T86))
insertF_in_gga(T95, .(T96, T97), .(T96, T99)) → U4_gga(T95, T96, T97, T99, insertF_in_gga(T95, T97, T99))
U4_gga(T95, T96, T97, T99, insertF_out_gga(T95, T97, T99)) → insertF_out_gga(T95, .(T96, T97), .(T96, T99))
U8_ggaga(T27, T29, T67, T6, T9, insertF_out_gga(T6, T67, T9)) → pG_out_ggaga(T27, T29, T67, T6, T9)
U6_gagaga(T28, T29, T27, X45, T6, T9, pG_out_ggaga(T27, T29, X45, T6, T9)) → pB_out_gagaga(T28, T29, T27, X45, T6, T9)
U1_ga(T6, T27, T28, T9, pB_out_gagaga(T28, X44, T27, X45, T6, T9)) → permA_out_ga(.(T6, .(T27, T28)), T9)

The argument filtering Pi contains the following mapping:
permA_in_ga(x1, x2)  =  permA_in_ga(x1)
[]  =  []
permA_out_ga(x1, x2)  =  permA_out_ga(x1, x2)
.(x1, x2)  =  .(x1, x2)
U1_ga(x1, x2, x3, x4, x5)  =  U1_ga(x1, x2, x3, x5)
pB_in_gagaga(x1, x2, x3, x4, x5, x6)  =  pB_in_gagaga(x1, x3, x5)
U5_gagaga(x1, x2, x3, x4, x5, x6, x7)  =  U5_gagaga(x1, x3, x5, x7)
permC_in_ga(x1, x2)  =  permC_in_ga(x1)
permC_out_ga(x1, x2)  =  permC_out_ga(x1, x2)
U2_ga(x1, x2, x3, x4)  =  U2_ga(x1, x2, x4)
pD_in_gaga(x1, x2, x3, x4)  =  pD_in_gaga(x1, x3)
U9_gaga(x1, x2, x3, x4, x5)  =  U9_gaga(x1, x3, x5)
U10_gaga(x1, x2, x3, x4, x5)  =  U10_gaga(x1, x2, x3, x5)
insertE_in_gga(x1, x2, x3)  =  insertE_in_gga(x1, x2)
insertE_out_gga(x1, x2, x3)  =  insertE_out_gga(x1, x2, x3)
U3_gga(x1, x2, x3, x4, x5)  =  U3_gga(x1, x2, x3, x5)
pD_out_gaga(x1, x2, x3, x4)  =  pD_out_gaga(x1, x2, x3, x4)
U6_gagaga(x1, x2, x3, x4, x5, x6, x7)  =  U6_gagaga(x1, x2, x3, x5, x7)
pG_in_ggaga(x1, x2, x3, x4, x5)  =  pG_in_ggaga(x1, x2, x4)
U7_ggaga(x1, x2, x3, x4, x5, x6)  =  U7_ggaga(x1, x2, x4, x6)
U8_ggaga(x1, x2, x3, x4, x5, x6)  =  U8_ggaga(x1, x2, x3, x4, x6)
insertF_in_gga(x1, x2, x3)  =  insertF_in_gga(x1, x2)
insertF_out_gga(x1, x2, x3)  =  insertF_out_gga(x1, x2, x3)
U4_gga(x1, x2, x3, x4, x5)  =  U4_gga(x1, x2, x3, x5)
pG_out_ggaga(x1, x2, x3, x4, x5)  =  pG_out_ggaga(x1, x2, x3, x4, x5)
pB_out_gagaga(x1, x2, x3, x4, x5, x6)  =  pB_out_gagaga(x1, x2, x3, x4, x5, x6)
INSERTE_IN_GGA(x1, x2, x3)  =  INSERTE_IN_GGA(x1, x2)

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

(15) UsableRulesProof (EQUIVALENT transformation)

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

(16) Obligation:

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

INSERTE_IN_GGA(T60, .(T61, T62), .(T61, X91)) → INSERTE_IN_GGA(T60, T62, X91)

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

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

(17) PiDPToQDPProof (SOUND transformation)

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

(18) Obligation:

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

INSERTE_IN_GGA(T60, .(T61, T62)) → INSERTE_IN_GGA(T60, T62)

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:

• INSERTE_IN_GGA(T60, .(T61, T62)) → INSERTE_IN_GGA(T60, T62)
  The graph contains the following edges 1 >= 1, 2 > 2

(20) YES

(21) Obligation:

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

PERMC_IN_GA(.(T34, T35), X59) → PD_IN_GAGA(T35, X58, T34, X59)
PD_IN_GAGA(T35, T36, T34, X59) → PERMC_IN_GA(T35, T36)

The TRS R consists of the following rules:

permA_in_ga([], []) → permA_out_ga([], [])
permA_in_ga(.(T16, []), .(T16, [])) → permA_out_ga(.(T16, []), .(T16, []))
permA_in_ga(.(T6, .(T27, T28)), T9) → U1_ga(T6, T27, T28, T9, pB_in_gagaga(T28, X44, T27, X45, T6, T9))
pB_in_gagaga(T28, T29, T27, X45, T6, T9) → U5_gagaga(T28, T29, T27, X45, T6, T9, permC_in_ga(T28, T29))
permC_in_ga([], []) → permC_out_ga([], [])
permC_in_ga(.(T34, T35), X59) → U2_ga(T34, T35, X59, pD_in_gaga(T35, X58, T34, X59))
pD_in_gaga(T35, T36, T34, X59) → U9_gaga(T35, T36, T34, X59, permC_in_ga(T35, T36))
U9_gaga(T35, T36, T34, X59, permC_out_ga(T35, T36)) → U10_gaga(T35, T36, T34, X59, insertE_in_gga(T34, T36, X59))
insertE_in_gga(T43, [], .(T43, [])) → insertE_out_gga(T43, [], .(T43, []))
insertE_in_gga(T52, T53, .(T52, T53)) → insertE_out_gga(T52, T53, .(T52, T53))
insertE_in_gga(T60, .(T61, T62), .(T61, X91)) → U3_gga(T60, T61, T62, X91, insertE_in_gga(T60, T62, X91))
U3_gga(T60, T61, T62, X91, insertE_out_gga(T60, T62, X91)) → insertE_out_gga(T60, .(T61, T62), .(T61, X91))
U10_gaga(T35, T36, T34, X59, insertE_out_gga(T34, T36, X59)) → pD_out_gaga(T35, T36, T34, X59)
U2_ga(T34, T35, X59, pD_out_gaga(T35, X58, T34, X59)) → permC_out_ga(.(T34, T35), X59)
U5_gagaga(T28, T29, T27, X45, T6, T9, permC_out_ga(T28, T29)) → U6_gagaga(T28, T29, T27, X45, T6, T9, pG_in_ggaga(T27, T29, X45, T6, T9))
pG_in_ggaga(T27, T29, T67, T6, T9) → U7_ggaga(T27, T29, T67, T6, T9, insertE_in_gga(T27, T29, T67))
U7_ggaga(T27, T29, T67, T6, T9, insertE_out_gga(T27, T29, T67)) → U8_ggaga(T27, T29, T67, T6, T9, insertF_in_gga(T6, T67, T9))
insertF_in_gga(T76, [], .(T76, [])) → insertF_out_gga(T76, [], .(T76, []))
insertF_in_gga(T85, T86, .(T85, T86)) → insertF_out_gga(T85, T86, .(T85, T86))
insertF_in_gga(T95, .(T96, T97), .(T96, T99)) → U4_gga(T95, T96, T97, T99, insertF_in_gga(T95, T97, T99))
U4_gga(T95, T96, T97, T99, insertF_out_gga(T95, T97, T99)) → insertF_out_gga(T95, .(T96, T97), .(T96, T99))
U8_ggaga(T27, T29, T67, T6, T9, insertF_out_gga(T6, T67, T9)) → pG_out_ggaga(T27, T29, T67, T6, T9)
U6_gagaga(T28, T29, T27, X45, T6, T9, pG_out_ggaga(T27, T29, X45, T6, T9)) → pB_out_gagaga(T28, T29, T27, X45, T6, T9)
U1_ga(T6, T27, T28, T9, pB_out_gagaga(T28, X44, T27, X45, T6, T9)) → permA_out_ga(.(T6, .(T27, T28)), T9)

The argument filtering Pi contains the following mapping:
permA_in_ga(x1, x2)  =  permA_in_ga(x1)
[]  =  []
permA_out_ga(x1, x2)  =  permA_out_ga(x1, x2)
.(x1, x2)  =  .(x1, x2)
U1_ga(x1, x2, x3, x4, x5)  =  U1_ga(x1, x2, x3, x5)
pB_in_gagaga(x1, x2, x3, x4, x5, x6)  =  pB_in_gagaga(x1, x3, x5)
U5_gagaga(x1, x2, x3, x4, x5, x6, x7)  =  U5_gagaga(x1, x3, x5, x7)
permC_in_ga(x1, x2)  =  permC_in_ga(x1)
permC_out_ga(x1, x2)  =  permC_out_ga(x1, x2)
U2_ga(x1, x2, x3, x4)  =  U2_ga(x1, x2, x4)
pD_in_gaga(x1, x2, x3, x4)  =  pD_in_gaga(x1, x3)
U9_gaga(x1, x2, x3, x4, x5)  =  U9_gaga(x1, x3, x5)
U10_gaga(x1, x2, x3, x4, x5)  =  U10_gaga(x1, x2, x3, x5)
insertE_in_gga(x1, x2, x3)  =  insertE_in_gga(x1, x2)
insertE_out_gga(x1, x2, x3)  =  insertE_out_gga(x1, x2, x3)
U3_gga(x1, x2, x3, x4, x5)  =  U3_gga(x1, x2, x3, x5)
pD_out_gaga(x1, x2, x3, x4)  =  pD_out_gaga(x1, x2, x3, x4)
U6_gagaga(x1, x2, x3, x4, x5, x6, x7)  =  U6_gagaga(x1, x2, x3, x5, x7)
pG_in_ggaga(x1, x2, x3, x4, x5)  =  pG_in_ggaga(x1, x2, x4)
U7_ggaga(x1, x2, x3, x4, x5, x6)  =  U7_ggaga(x1, x2, x4, x6)
U8_ggaga(x1, x2, x3, x4, x5, x6)  =  U8_ggaga(x1, x2, x3, x4, x6)
insertF_in_gga(x1, x2, x3)  =  insertF_in_gga(x1, x2)
insertF_out_gga(x1, x2, x3)  =  insertF_out_gga(x1, x2, x3)
U4_gga(x1, x2, x3, x4, x5)  =  U4_gga(x1, x2, x3, x5)
pG_out_ggaga(x1, x2, x3, x4, x5)  =  pG_out_ggaga(x1, x2, x3, x4, x5)
pB_out_gagaga(x1, x2, x3, x4, x5, x6)  =  pB_out_gagaga(x1, x2, x3, x4, x5, x6)
PERMC_IN_GA(x1, x2)  =  PERMC_IN_GA(x1)
PD_IN_GAGA(x1, x2, x3, x4)  =  PD_IN_GAGA(x1, x3)

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

(22) UsableRulesProof (EQUIVALENT transformation)

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

(23) Obligation:

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

PERMC_IN_GA(.(T34, T35), X59) → PD_IN_GAGA(T35, X58, T34, X59)
PD_IN_GAGA(T35, T36, T34, X59) → PERMC_IN_GA(T35, T36)

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

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

(24) PiDPToQDPProof (SOUND transformation)

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

(25) Obligation:

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

PERMC_IN_GA(.(T34, T35)) → PD_IN_GAGA(T35, T34)
PD_IN_GAGA(T35, T34) → PERMC_IN_GA(T35)

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

(26) QDPSizeChangeProof (EQUIVALENT transformation)

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

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

• PD_IN_GAGA(T35, T34) → PERMC_IN_GA(T35)
  The graph contains the following edges 1 >= 1

• PERMC_IN_GA(.(T34, T35)) → PD_IN_GAGA(T35, T34)
  The graph contains the following edges 1 > 1, 1 > 2

(27) YES