Left Termination proof of /tmp/tmp0FZYM7/rev.pl

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

0 Prolog

↳1 PrologToPiTRSViaGraphTransformerProof (⇒, 193 ms)

↳2 PiTRS

↳3 DependencyPairsProof (⇔, 324 ms)

↳4 PiDP

↳5 DependencyGraphProof (⇔, 0 ms)

↳6 AND

    ↳7 PiDP

        ↳8 UsableRulesProof (⇔, 0 ms)

        ↳9 PiDP

        ↳10 PiDPToQDPProof (⇒, 18 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

    ↳21 PiDP

        ↳22 UsableRulesProof (⇔, 0 ms)

        ↳23 PiDP

        ↳24 PiDPToQDPProof (⇒, 40 ms)

        ↳25 QDP

        ↳26 QDPOrderProof (⇔, 541 ms)

        ↳27 QDP

        ↳28 DependencyGraphProof (⇔, 0 ms)

        ↳29 TRUE

(0) Obligation:

Clauses:

rev([], []).
rev(.(X, XS), .(Y, YS)) :- ','(rev1(X, XS, Y), rev2(X, XS, YS)).
rev1(X, [], X).
rev1(X, .(Y, YS), Z) :- rev1(Y, YS, Z).
rev2(X, [], []).
rev2(X, .(Y, YS), ZS) :- ','(rev2(Y, YS, US), ','(rev(US, VS), rev(.(X, VS), ZS))).

Query: rev(g,a)

(1) PrologToPiTRSViaGraphTransformerProof (SOUND transformation)

Transformed Prolog program to (Pi-)TRS.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
1 [label="A: rev(T1, T2)\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
5 [label="5: rev(T1, T2), SCOPE: 1, CLAUSE: 0 | rev(T1, T2), SCOPE: 1, CLAUSE: 1\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
9 [label="9: true | rev([], T2), SCOPE: 1, CLAUSE: 1\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
12 [label="12: rev(T1, T2), SCOPE: 1, CLAUSE: 1\n\nT1 is ground\nrev(T1, T2) !=? rev([], [])", fontsize=16, style=filled, fillcolor=lightyellow];
16 [label="16: rev([], T2), SCOPE: 1, CLAUSE: 1\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
18 [label="18: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
22 [label="22: ','(rev1(T7, T8, T11), rev2(T7, T8, T12))\n\nT7 is ground\nT8 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
24 [label="24: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
26 [label="26: ','(rev1(T7, T8, T11), rev2(T7, T8, T12)), SCOPE: 2, CLAUSE: 2 | ','(rev1(T7, T8, T11), rev2(T7, T8, T12)), SCOPE: 2, CLAUSE: 3\n\nT7 is ground\nT8 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
28 [label="28: ','(rev1(T7, T8, T11), rev2(T7, T8, T12)), SCOPE: 2, CLAUSE: 2\n\nT7 is ground\nT8 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
29 [label="29: ','(rev1(T7, T8, T11), rev2(T7, T8, T12)), SCOPE: 2, CLAUSE: 3\n\nT7 is ground\nT8 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
32 [label="32: rev2(T17, [], T18)\n\nT17 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
33 [label="33: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
39 [label="39: rev2(T17, [], T18), SCOPE: 3, CLAUSE: 4 | rev2(T17, [], T18), SCOPE: 3, CLAUSE: 5\n\nT17 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
40 [label="40: rev2(T17, [], T18), SCOPE: 3, CLAUSE: 4\n\nT17 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
41 [label="41: rev2(T17, [], T18), SCOPE: 3, CLAUSE: 5\n\nT17 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
44 [label="44: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
46 [label="46: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
47 [label="47: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
51 [label="51: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
65 [label="B: ','(rev1(T36, T37, T39), rev2(T35, .(T36, T37), T40))\n\nT35 is ground\nT36 is ground\nT37 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
67 [label="67: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
78 [label="C: rev1(T36, T37, T39)\n\nT36 is ground\nT37 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
79 [label="I: rev2(T35, .(T36, T37), T43)\n\nT35 is ground\nT36 is ground\nT37 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
80 [label="80: rev1(T36, T37, T39), SCOPE: 4, CLAUSE: 2 | rev1(T36, T37, T39), SCOPE: 4, CLAUSE: 3\n\nT36 is ground\nT37 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
85 [label="85: rev1(T36, T37, T39), SCOPE: 4, CLAUSE: 2\n\nT36 is ground\nT37 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
86 [label="86: rev1(T36, T37, T39), SCOPE: 4, CLAUSE: 3\n\nT36 is ground\nT37 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
97 [label="97: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
98 [label="98: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
99 [label="99: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
107 [label="107: rev1(T60, T61, T63)\n\nT60 is ground\nT61 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
108 [label="108: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
115 [label="115: rev2(T35, .(T36, T37), T43), SCOPE: 5, CLAUSE: 4 | rev2(T35, .(T36, T37), T43), SCOPE: 5, CLAUSE: 5\n\nT35 is ground\nT36 is ground\nT37 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
118 [label="118: rev2(T35, .(T36, T37), T43), SCOPE: 5, CLAUSE: 5\n\nT35 is ground\nT36 is ground\nT37 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
133 [label="J: ','(rev2(T81, T82, X83), ','(rev(X83, X84), rev(.(T80, X84), T84)))\n\nT80 is ground\nT81 is ground\nT82 is ground\nX83 is free\nX84 is free", fontsize=16, style=filled, fillcolor=lightyellow];
150 [label="D: rev2(T81, T82, X83)\n\nT81 is ground\nT82 is ground\nX83 is free", fontsize=16, style=filled, fillcolor=lightyellow];
151 [label="K: ','(rev(T87, X84), rev(.(T80, X84), T84))\n\nT80 is ground\nT87 is ground\nX84 is free", fontsize=16, style=filled, fillcolor=lightyellow];
154 [label="154: rev2(T81, T82, X83), SCOPE: 6, CLAUSE: 4 | rev2(T81, T82, X83), SCOPE: 6, CLAUSE: 5\n\nT81 is ground\nT82 is ground\nX83 is free", fontsize=16, style=filled, fillcolor=lightyellow];
155 [label="155: rev2(T81, T82, X83), SCOPE: 6, CLAUSE: 4\n\nT81 is ground\nT82 is ground\nX83 is free", fontsize=16, style=filled, fillcolor=lightyellow];
156 [label="156: rev2(T81, T82, X83), SCOPE: 6, CLAUSE: 5\n\nT81 is ground\nT82 is ground\nX83 is free", fontsize=16, style=filled, fillcolor=lightyellow];
157 [label="157: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
168 [label="168: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
169 [label="169: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
170 [label="E: ','(rev2(T102, T103, X110), ','(rev(X110, X111), rev(.(T101, X111), X112)))\n\nT101 is ground\nT102 is ground\nT103 is ground\nX112 is free\nX110 is free\nX111 is free", fontsize=16, style=filled, fillcolor=lightyellow];
171 [label="171: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
174 [label="174: rev2(T102, T103, X110)\n\nT102 is ground\nT103 is ground\nX110 is free", fontsize=16, style=filled, fillcolor=lightyellow];
175 [label="L: ','(rev(T106, X111), rev(.(T101, X111), X112))\n\nT101 is ground\nT106 is ground\nX112 is free\nX111 is free", fontsize=16, style=filled, fillcolor=lightyellow];
176 [label="G: rev(T106, X111)\n\nT106 is ground\nX111 is free", fontsize=16, style=filled, fillcolor=lightyellow];
177 [label="177: rev(.(T101, T109), X112)\n\nT101 is ground\nT109 is ground\nX112 is free", fontsize=16, style=filled, fillcolor=lightyellow];
178 [label="178: rev(T106, X111), SCOPE: 7, CLAUSE: 0 | rev(T106, X111), SCOPE: 7, CLAUSE: 1\n\nT106 is ground\nX111 is free", fontsize=16, style=filled, fillcolor=lightyellow];
179 [label="179: rev(T106, X111), SCOPE: 7, CLAUSE: 0\n\nT106 is ground\nX111 is free", fontsize=16, style=filled, fillcolor=lightyellow];
180 [label="180: rev(T106, X111), SCOPE: 7, CLAUSE: 1\n\nT106 is ground\nX111 is free", fontsize=16, style=filled, fillcolor=lightyellow];
181 [label="181: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
182 [label="182: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
183 [label="183: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
186 [label="H: ','(rev1(T114, T115, X133), rev2(T114, T115, X134))\n\nT114 is ground\nT115 is ground\nX133 is free\nX134 is free", fontsize=16, style=filled, fillcolor=lightyellow];
187 [label="187: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
188 [label="F: rev1(T114, T115, X133)\n\nT114 is ground\nT115 is ground\nX133 is free", fontsize=16, style=filled, fillcolor=lightyellow];
189 [label="189: rev2(T114, T115, X134)\n\nT114 is ground\nT115 is ground\nX134 is free", fontsize=16, style=filled, fillcolor=lightyellow];
190 [label="190: rev1(T114, T115, X133), SCOPE: 8, CLAUSE: 2 | rev1(T114, T115, X133), SCOPE: 8, CLAUSE: 3\n\nT114 is ground\nT115 is ground\nX133 is free", fontsize=16, style=filled, fillcolor=lightyellow];
191 [label="191: rev1(T114, T115, X133), SCOPE: 8, CLAUSE: 2\n\nT114 is ground\nT115 is ground\nX133 is free", fontsize=16, style=filled, fillcolor=lightyellow];
192 [label="192: rev1(T114, T115, X133), SCOPE: 8, CLAUSE: 3\n\nT114 is ground\nT115 is ground\nX133 is free", fontsize=16, style=filled, fillcolor=lightyellow];
193 [label="193: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
194 [label="194: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
195 [label="195: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
196 [label="196: rev1(T133, T134, X158)\n\nT133 is ground\nT134 is ground\nX158 is free", fontsize=16, style=filled, fillcolor=lightyellow];
197 [label="197: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
198 [label="198: rev(T87, X84)\n\nT87 is ground\nX84 is free", fontsize=16, style=filled, fillcolor=lightyellow];
199 [label="199: rev(.(T80, T139), T84)\n\nT80 is ground\nT139 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
200 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
1 -> 200 [arrowhead = none ];
200 -> 5;

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

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

203 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
9 -> 203 [arrowhead = none ];
203 -> 16;

204 [label="EVAL with clause\nrev(.(X9, X10), .(X11, X12)) :- ','(rev1(X9, X10, X11), rev2(X9, X10, X12)).\nand substitutionX9 -> T7,\nX10 -> T8,\nT1 -> .(T7, T8),\nX11 -> T11,\nX12 -> T12,\nT2 -> .(T11, T12),\nT9 -> T11,\nT10 -> T12", fontsize=14, style = filled, fillcolor = lightblue];
12 -> 204 [arrowhead = none ];
204 -> 22;

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

206 [label="BACKTRACK\nfor clause: rev(.(X, XS), .(Y, YS)) :- ','(rev1(X, XS, Y), rev2(X, XS, YS))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
16 -> 206 [arrowhead = none ];
206 -> 18;

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

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

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

210 [label="EVAL with clause\nrev1(X17, [], X17).\nand substitutionT7 -> T17,\nX17 -> T17,\nT8 -> [],\nT11 -> T17,\nT12 -> T18", fontsize=14, style = filled, fillcolor = lightblue];
28 -> 210 [arrowhead = none ];
210 -> 32;

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

212 [label="EVAL with clause\nrev1(X37, .(X38, X39), X40) :- rev1(X38, X39, X40).\nand substitutionT7 -> T35,\nX37 -> T35,\nX38 -> T36,\nX39 -> T37,\nT8 -> .(T36, T37),\nT11 -> T39,\nX40 -> T39,\nT38 -> T39,\nT12 -> T40", fontsize=14, style = filled, fillcolor = lightblue];
29 -> 212 [arrowhead = none ];
212 -> 65;

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

214 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
32 -> 214 [arrowhead = none ];
214 -> 39;

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

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

217 [label="EVAL with clause\nrev2(X24, [], []).\nand substitutionT17 -> T25,\nX24 -> T25,\nT18 -> []", fontsize=14, style = filled, fillcolor = lightblue];
40 -> 217 [arrowhead = none ];
217 -> 44;

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

219 [label="BACKTRACK\nfor clause: rev2(X, .(Y, YS), ZS) :- ','(rev2(Y, YS, US), ','(rev(US, VS), rev(.(X, VS), ZS)))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
41 -> 219 [arrowhead = none ];
219 -> 51;

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

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

222 [label="SPLIT 2\nnew knowledge:\nT36 is ground\nT37 is ground\nT39 is ground\nreplacements:T40 -> T43", fontsize=14, style = filled, fillcolor = violet];
65 -> 222 [arrowhead = none ];
222 -> 79;

223 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
78 -> 223 [arrowhead = none ];
223 -> 80;

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

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

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

227 [label="EVAL with clause\nrev1(X49, [], X49).\nand substitutionT36 -> T50,\nX49 -> T50,\nT37 -> [],\nT39 -> T50", fontsize=14, style = filled, fillcolor = lightblue];
85 -> 227 [arrowhead = none ];
227 -> 97;

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

229 [label="EVAL with clause\nrev1(X58, .(X59, X60), X61) :- rev1(X59, X60, X61).\nand substitutionT36 -> T59,\nX58 -> T59,\nX59 -> T60,\nX60 -> T61,\nT37 -> .(T60, T61),\nT39 -> T63,\nX61 -> T63,\nT62 -> T63", fontsize=14, style = filled, fillcolor = lightblue];
86 -> 229 [arrowhead = none ];
229 -> 107;

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

231 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
97 -> 231 [arrowhead = none ];
231 -> 99;

232 [label="INSTANCE with matching:\nT36 -> T60\nT37 -> T61\nT39 -> T63", fontsize=14, style = filled, fillcolor = lightgrey];
107 -> 232 [arrowhead = none , style=dashed];
232 -> 78[style=dashed];

233 [label="BACKTRACK\nfor clause: rev2(X, [], [])because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
115 -> 233 [arrowhead = none ];
233 -> 118;

234 [label="ONLY EVAL with clause\nrev2(X79, .(X80, X81), X82) :- ','(rev2(X80, X81, X83), ','(rev(X83, X84), rev(.(X79, X84), X82))).\nand substitutionT35 -> T80,\nX79 -> T80,\nT36 -> T81,\nX80 -> T81,\nT37 -> T82,\nX81 -> T82,\nT43 -> T84,\nX82 -> T84,\nT83 -> T84", fontsize=14, style = filled, fillcolor = lightblue];
118 -> 234 [arrowhead = none ];
234 -> 133;

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

236 [label="SPLIT 2\nnew knowledge:\nT81 is ground\nT82 is ground\nT87 is ground\nreplacements:X83 -> T87", fontsize=14, style = filled, fillcolor = violet];
133 -> 236 [arrowhead = none ];
236 -> 151;

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

238 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
151 -> 238 [arrowhead = none ];
238 -> 198;

239 [label="SPLIT 2\nnew knowledge:\nT87 is ground\nT139 is ground\nreplacements:X84 -> T139", fontsize=14, style = filled, fillcolor = violet];
151 -> 239 [arrowhead = none ];
239 -> 199;

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

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

242 [label="EVAL with clause\nrev2(X93, [], []).\nand substitutionT81 -> T94,\nX93 -> T94,\nT82 -> [],\nX83 -> []", fontsize=14, style = filled, fillcolor = lightblue];
155 -> 242 [arrowhead = none ];
242 -> 157;

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

244 [label="EVAL with clause\nrev2(X106, .(X107, X108), X109) :- ','(rev2(X107, X108, X110), ','(rev(X110, X111), rev(.(X106, X111), X109))).\nand substitutionT81 -> T101,\nX106 -> T101,\nX107 -> T102,\nX108 -> T103,\nT82 -> .(T102, T103),\nX83 -> X112,\nX109 -> X112", fontsize=14, style = filled, fillcolor = lightblue];
156 -> 244 [arrowhead = none ];
244 -> 170;

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

246 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
157 -> 246 [arrowhead = none ];
246 -> 169;

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

248 [label="SPLIT 2\nnew knowledge:\nT102 is ground\nT103 is ground\nT106 is ground\nreplacements:X110 -> T106", fontsize=14, style = filled, fillcolor = violet];
170 -> 248 [arrowhead = none ];
248 -> 175;

249 [label="INSTANCE with matching:\nT81 -> T102\nT82 -> T103\nX83 -> X110", fontsize=14, style = filled, fillcolor = lightgrey];
174 -> 249 [arrowhead = none , style=dashed];
249 -> 150[style=dashed];

250 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
175 -> 250 [arrowhead = none ];
250 -> 176;

251 [label="SPLIT 2\nnew knowledge:\nT106 is ground\nT109 is ground\nreplacements:X111 -> T109", fontsize=14, style = filled, fillcolor = violet];
175 -> 251 [arrowhead = none ];
251 -> 177;

252 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
176 -> 252 [arrowhead = none ];
252 -> 178;

253 [label="INSTANCE with matching:\nT1 -> .(T101, T109)\nT2 -> X112", fontsize=14, style = filled, fillcolor = lightgrey];
177 -> 253 [arrowhead = none , style=dashed];
253 -> 1[style=dashed];

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

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

256 [label="EVAL with clause\nrev([], []).\nand substitutionT106 -> [],\nX111 -> []", fontsize=14, style = filled, fillcolor = lightblue];
179 -> 256 [arrowhead = none ];
256 -> 181;

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

258 [label="EVAL with clause\nrev(.(X129, X130), .(X131, X132)) :- ','(rev1(X129, X130, X131), rev2(X129, X130, X132)).\nand substitutionX129 -> T114,\nX130 -> T115,\nT106 -> .(T114, T115),\nX131 -> X133,\nX132 -> X134,\nX111 -> .(X133, X134)", fontsize=14, style = filled, fillcolor = lightblue];
180 -> 258 [arrowhead = none ];
258 -> 186;

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

260 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
181 -> 260 [arrowhead = none ];
260 -> 183;

261 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
186 -> 261 [arrowhead = none ];
261 -> 188;

262 [label="SPLIT 2\nnew knowledge:\nT114 is ground\nT115 is ground\nT118 is ground\nreplacements:X133 -> T118", fontsize=14, style = filled, fillcolor = violet];
186 -> 262 [arrowhead = none ];
262 -> 189;

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

264 [label="INSTANCE with matching:\nT81 -> T114\nT82 -> T115\nX83 -> X134", fontsize=14, style = filled, fillcolor = lightgrey];
189 -> 264 [arrowhead = none , style=dashed];
264 -> 150[style=dashed];

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

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

267 [label="EVAL with clause\nrev1(X143, [], X143).\nand substitutionT114 -> T125,\nX143 -> T125,\nT115 -> [],\nX133 -> T125", fontsize=14, style = filled, fillcolor = lightblue];
191 -> 267 [arrowhead = none ];
267 -> 193;

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

269 [label="EVAL with clause\nrev1(X154, .(X155, X156), X157) :- rev1(X155, X156, X157).\nand substitutionT114 -> T132,\nX154 -> T132,\nX155 -> T133,\nX156 -> T134,\nT115 -> .(T133, T134),\nX133 -> X158,\nX157 -> X158", fontsize=14, style = filled, fillcolor = lightblue];
192 -> 269 [arrowhead = none ];
269 -> 196;

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

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

272 [label="INSTANCE with matching:\nT114 -> T133\nT115 -> T134\nX133 -> X158", fontsize=14, style = filled, fillcolor = lightgrey];
196 -> 272 [arrowhead = none , style=dashed];
272 -> 188[style=dashed];

273 [label="INSTANCE with matching:\nT106 -> T87\nX111 -> X84", fontsize=14, style = filled, fillcolor = lightgrey];
198 -> 273 [arrowhead = none , style=dashed];
273 -> 176[style=dashed];

274 [label="INSTANCE with matching:\nT1 -> .(T80, T139)\nT2 -> T84", fontsize=14, style = filled, fillcolor = lightgrey];
199 -> 274 [arrowhead = none , style=dashed];
274 -> 1[style=dashed];

}

(2) Obligation:

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

revA_in_ga([], []) → revA_out_ga([], [])
revA_in_ga(.(T25, []), .(T25, [])) → revA_out_ga(.(T25, []), .(T25, []))
revA_in_ga(.(T35, .(T36, T37)), .(T39, T40)) → U1_ga(T35, T36, T37, T39, T40, pB_in_ggaga(T36, T37, T39, T35, T40))
pB_in_ggaga(T36, T37, T39, T35, T43) → U7_ggaga(T36, T37, T39, T35, T43, rev1C_in_gga(T36, T37, T39))
rev1C_in_gga(T50, [], T50) → rev1C_out_gga(T50, [], T50)
rev1C_in_gga(T59, .(T60, T61), T63) → U2_gga(T59, T60, T61, T63, rev1C_in_gga(T60, T61, T63))
U2_gga(T59, T60, T61, T63, rev1C_out_gga(T60, T61, T63)) → rev1C_out_gga(T59, .(T60, T61), T63)
U7_ggaga(T36, T37, T39, T35, T43, rev1C_out_gga(T36, T37, T39)) → U8_ggaga(T36, T37, T39, T35, T43, rev2I_in_ggga(T35, T36, T37, T43))
rev2I_in_ggga(T80, T81, T82, T84) → U6_ggga(T80, T81, T82, T84, pJ_in_ggaaga(T81, T82, X83, X84, T80, T84))
pJ_in_ggaaga(T81, T82, T87, X84, T80, T84) → U9_ggaaga(T81, T82, T87, X84, T80, T84, rev2D_in_gga(T81, T82, T87))
rev2D_in_gga(T94, [], []) → rev2D_out_gga(T94, [], [])
rev2D_in_gga(T101, .(T102, T103), X112) → U3_gga(T101, T102, T103, X112, pE_in_ggaaga(T102, T103, X110, X111, T101, X112))
pE_in_ggaaga(T102, T103, T106, X111, T101, X112) → U13_ggaaga(T102, T103, T106, X111, T101, X112, rev2D_in_gga(T102, T103, T106))
U13_ggaaga(T102, T103, T106, X111, T101, X112, rev2D_out_gga(T102, T103, T106)) → U14_ggaaga(T102, T103, T106, X111, T101, X112, pL_in_gaga(T106, X111, T101, X112))
pL_in_gaga(T106, T109, T101, X112) → U15_gaga(T106, T109, T101, X112, revG_in_ga(T106, T109))
revG_in_ga([], []) → revG_out_ga([], [])
revG_in_ga(.(T114, T115), .(X133, X134)) → U5_ga(T114, T115, X133, X134, pH_in_ggaa(T114, T115, X133, X134))
pH_in_ggaa(T114, T115, T118, X134) → U17_ggaa(T114, T115, T118, X134, rev1F_in_gga(T114, T115, T118))
rev1F_in_gga(T125, [], T125) → rev1F_out_gga(T125, [], T125)
rev1F_in_gga(T132, .(T133, T134), X158) → U4_gga(T132, T133, T134, X158, rev1F_in_gga(T133, T134, X158))
U4_gga(T132, T133, T134, X158, rev1F_out_gga(T133, T134, X158)) → rev1F_out_gga(T132, .(T133, T134), X158)
U17_ggaa(T114, T115, T118, X134, rev1F_out_gga(T114, T115, T118)) → U18_ggaa(T114, T115, T118, X134, rev2D_in_gga(T114, T115, X134))
U18_ggaa(T114, T115, T118, X134, rev2D_out_gga(T114, T115, X134)) → pH_out_ggaa(T114, T115, T118, X134)
U5_ga(T114, T115, X133, X134, pH_out_ggaa(T114, T115, X133, X134)) → revG_out_ga(.(T114, T115), .(X133, X134))
U15_gaga(T106, T109, T101, X112, revG_out_ga(T106, T109)) → U16_gaga(T106, T109, T101, X112, revA_in_ga(.(T101, T109), X112))
U16_gaga(T106, T109, T101, X112, revA_out_ga(.(T101, T109), X112)) → pL_out_gaga(T106, T109, T101, X112)
U14_ggaaga(T102, T103, T106, X111, T101, X112, pL_out_gaga(T106, X111, T101, X112)) → pE_out_ggaaga(T102, T103, T106, X111, T101, X112)
U3_gga(T101, T102, T103, X112, pE_out_ggaaga(T102, T103, X110, X111, T101, X112)) → rev2D_out_gga(T101, .(T102, T103), X112)
U9_ggaaga(T81, T82, T87, X84, T80, T84, rev2D_out_gga(T81, T82, T87)) → U10_ggaaga(T81, T82, T87, X84, T80, T84, pK_in_gaga(T87, X84, T80, T84))
pK_in_gaga(T87, T139, T80, T84) → U11_gaga(T87, T139, T80, T84, revG_in_ga(T87, T139))
U11_gaga(T87, T139, T80, T84, revG_out_ga(T87, T139)) → U12_gaga(T87, T139, T80, T84, revA_in_ga(.(T80, T139), T84))
U12_gaga(T87, T139, T80, T84, revA_out_ga(.(T80, T139), T84)) → pK_out_gaga(T87, T139, T80, T84)
U10_ggaaga(T81, T82, T87, X84, T80, T84, pK_out_gaga(T87, X84, T80, T84)) → pJ_out_ggaaga(T81, T82, T87, X84, T80, T84)
U6_ggga(T80, T81, T82, T84, pJ_out_ggaaga(T81, T82, X83, X84, T80, T84)) → rev2I_out_ggga(T80, T81, T82, T84)
U8_ggaga(T36, T37, T39, T35, T43, rev2I_out_ggga(T35, T36, T37, T43)) → pB_out_ggaga(T36, T37, T39, T35, T43)
U1_ga(T35, T36, T37, T39, T40, pB_out_ggaga(T36, T37, T39, T35, T40)) → revA_out_ga(.(T35, .(T36, T37)), .(T39, T40))

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

REVA_IN_GA(.(T35, .(T36, T37)), .(T39, T40)) → U1_GA(T35, T36, T37, T39, T40, pB_in_ggaga(T36, T37, T39, T35, T40))
REVA_IN_GA(.(T35, .(T36, T37)), .(T39, T40)) → PB_IN_GGAGA(T36, T37, T39, T35, T40)
PB_IN_GGAGA(T36, T37, T39, T35, T43) → U7_GGAGA(T36, T37, T39, T35, T43, rev1C_in_gga(T36, T37, T39))
PB_IN_GGAGA(T36, T37, T39, T35, T43) → REV1C_IN_GGA(T36, T37, T39)
REV1C_IN_GGA(T59, .(T60, T61), T63) → U2_GGA(T59, T60, T61, T63, rev1C_in_gga(T60, T61, T63))
REV1C_IN_GGA(T59, .(T60, T61), T63) → REV1C_IN_GGA(T60, T61, T63)
U7_GGAGA(T36, T37, T39, T35, T43, rev1C_out_gga(T36, T37, T39)) → U8_GGAGA(T36, T37, T39, T35, T43, rev2I_in_ggga(T35, T36, T37, T43))
U7_GGAGA(T36, T37, T39, T35, T43, rev1C_out_gga(T36, T37, T39)) → REV2I_IN_GGGA(T35, T36, T37, T43)
REV2I_IN_GGGA(T80, T81, T82, T84) → U6_GGGA(T80, T81, T82, T84, pJ_in_ggaaga(T81, T82, X83, X84, T80, T84))
REV2I_IN_GGGA(T80, T81, T82, T84) → PJ_IN_GGAAGA(T81, T82, X83, X84, T80, T84)
PJ_IN_GGAAGA(T81, T82, T87, X84, T80, T84) → U9_GGAAGA(T81, T82, T87, X84, T80, T84, rev2D_in_gga(T81, T82, T87))
PJ_IN_GGAAGA(T81, T82, T87, X84, T80, T84) → REV2D_IN_GGA(T81, T82, T87)
REV2D_IN_GGA(T101, .(T102, T103), X112) → U3_GGA(T101, T102, T103, X112, pE_in_ggaaga(T102, T103, X110, X111, T101, X112))
REV2D_IN_GGA(T101, .(T102, T103), X112) → PE_IN_GGAAGA(T102, T103, X110, X111, T101, X112)
PE_IN_GGAAGA(T102, T103, T106, X111, T101, X112) → U13_GGAAGA(T102, T103, T106, X111, T101, X112, rev2D_in_gga(T102, T103, T106))
PE_IN_GGAAGA(T102, T103, T106, X111, T101, X112) → REV2D_IN_GGA(T102, T103, T106)
U13_GGAAGA(T102, T103, T106, X111, T101, X112, rev2D_out_gga(T102, T103, T106)) → U14_GGAAGA(T102, T103, T106, X111, T101, X112, pL_in_gaga(T106, X111, T101, X112))
U13_GGAAGA(T102, T103, T106, X111, T101, X112, rev2D_out_gga(T102, T103, T106)) → PL_IN_GAGA(T106, X111, T101, X112)
PL_IN_GAGA(T106, T109, T101, X112) → U15_GAGA(T106, T109, T101, X112, revG_in_ga(T106, T109))
PL_IN_GAGA(T106, T109, T101, X112) → REVG_IN_GA(T106, T109)
REVG_IN_GA(.(T114, T115), .(X133, X134)) → U5_GA(T114, T115, X133, X134, pH_in_ggaa(T114, T115, X133, X134))
REVG_IN_GA(.(T114, T115), .(X133, X134)) → PH_IN_GGAA(T114, T115, X133, X134)
PH_IN_GGAA(T114, T115, T118, X134) → U17_GGAA(T114, T115, T118, X134, rev1F_in_gga(T114, T115, T118))
PH_IN_GGAA(T114, T115, T118, X134) → REV1F_IN_GGA(T114, T115, T118)
REV1F_IN_GGA(T132, .(T133, T134), X158) → U4_GGA(T132, T133, T134, X158, rev1F_in_gga(T133, T134, X158))
REV1F_IN_GGA(T132, .(T133, T134), X158) → REV1F_IN_GGA(T133, T134, X158)
U17_GGAA(T114, T115, T118, X134, rev1F_out_gga(T114, T115, T118)) → U18_GGAA(T114, T115, T118, X134, rev2D_in_gga(T114, T115, X134))
U17_GGAA(T114, T115, T118, X134, rev1F_out_gga(T114, T115, T118)) → REV2D_IN_GGA(T114, T115, X134)
U15_GAGA(T106, T109, T101, X112, revG_out_ga(T106, T109)) → U16_GAGA(T106, T109, T101, X112, revA_in_ga(.(T101, T109), X112))
U15_GAGA(T106, T109, T101, X112, revG_out_ga(T106, T109)) → REVA_IN_GA(.(T101, T109), X112)
U9_GGAAGA(T81, T82, T87, X84, T80, T84, rev2D_out_gga(T81, T82, T87)) → U10_GGAAGA(T81, T82, T87, X84, T80, T84, pK_in_gaga(T87, X84, T80, T84))
U9_GGAAGA(T81, T82, T87, X84, T80, T84, rev2D_out_gga(T81, T82, T87)) → PK_IN_GAGA(T87, X84, T80, T84)
PK_IN_GAGA(T87, T139, T80, T84) → U11_GAGA(T87, T139, T80, T84, revG_in_ga(T87, T139))
PK_IN_GAGA(T87, T139, T80, T84) → REVG_IN_GA(T87, T139)
U11_GAGA(T87, T139, T80, T84, revG_out_ga(T87, T139)) → U12_GAGA(T87, T139, T80, T84, revA_in_ga(.(T80, T139), T84))
U11_GAGA(T87, T139, T80, T84, revG_out_ga(T87, T139)) → REVA_IN_GA(.(T80, T139), T84)

The TRS R consists of the following rules:

revA_in_ga([], []) → revA_out_ga([], [])
revA_in_ga(.(T25, []), .(T25, [])) → revA_out_ga(.(T25, []), .(T25, []))
revA_in_ga(.(T35, .(T36, T37)), .(T39, T40)) → U1_ga(T35, T36, T37, T39, T40, pB_in_ggaga(T36, T37, T39, T35, T40))
pB_in_ggaga(T36, T37, T39, T35, T43) → U7_ggaga(T36, T37, T39, T35, T43, rev1C_in_gga(T36, T37, T39))
rev1C_in_gga(T50, [], T50) → rev1C_out_gga(T50, [], T50)
rev1C_in_gga(T59, .(T60, T61), T63) → U2_gga(T59, T60, T61, T63, rev1C_in_gga(T60, T61, T63))
U2_gga(T59, T60, T61, T63, rev1C_out_gga(T60, T61, T63)) → rev1C_out_gga(T59, .(T60, T61), T63)
U7_ggaga(T36, T37, T39, T35, T43, rev1C_out_gga(T36, T37, T39)) → U8_ggaga(T36, T37, T39, T35, T43, rev2I_in_ggga(T35, T36, T37, T43))
rev2I_in_ggga(T80, T81, T82, T84) → U6_ggga(T80, T81, T82, T84, pJ_in_ggaaga(T81, T82, X83, X84, T80, T84))
pJ_in_ggaaga(T81, T82, T87, X84, T80, T84) → U9_ggaaga(T81, T82, T87, X84, T80, T84, rev2D_in_gga(T81, T82, T87))
rev2D_in_gga(T94, [], []) → rev2D_out_gga(T94, [], [])
rev2D_in_gga(T101, .(T102, T103), X112) → U3_gga(T101, T102, T103, X112, pE_in_ggaaga(T102, T103, X110, X111, T101, X112))
pE_in_ggaaga(T102, T103, T106, X111, T101, X112) → U13_ggaaga(T102, T103, T106, X111, T101, X112, rev2D_in_gga(T102, T103, T106))
U13_ggaaga(T102, T103, T106, X111, T101, X112, rev2D_out_gga(T102, T103, T106)) → U14_ggaaga(T102, T103, T106, X111, T101, X112, pL_in_gaga(T106, X111, T101, X112))
pL_in_gaga(T106, T109, T101, X112) → U15_gaga(T106, T109, T101, X112, revG_in_ga(T106, T109))
revG_in_ga([], []) → revG_out_ga([], [])
revG_in_ga(.(T114, T115), .(X133, X134)) → U5_ga(T114, T115, X133, X134, pH_in_ggaa(T114, T115, X133, X134))
pH_in_ggaa(T114, T115, T118, X134) → U17_ggaa(T114, T115, T118, X134, rev1F_in_gga(T114, T115, T118))
rev1F_in_gga(T125, [], T125) → rev1F_out_gga(T125, [], T125)
rev1F_in_gga(T132, .(T133, T134), X158) → U4_gga(T132, T133, T134, X158, rev1F_in_gga(T133, T134, X158))
U4_gga(T132, T133, T134, X158, rev1F_out_gga(T133, T134, X158)) → rev1F_out_gga(T132, .(T133, T134), X158)
U17_ggaa(T114, T115, T118, X134, rev1F_out_gga(T114, T115, T118)) → U18_ggaa(T114, T115, T118, X134, rev2D_in_gga(T114, T115, X134))
U18_ggaa(T114, T115, T118, X134, rev2D_out_gga(T114, T115, X134)) → pH_out_ggaa(T114, T115, T118, X134)
U5_ga(T114, T115, X133, X134, pH_out_ggaa(T114, T115, X133, X134)) → revG_out_ga(.(T114, T115), .(X133, X134))
U15_gaga(T106, T109, T101, X112, revG_out_ga(T106, T109)) → U16_gaga(T106, T109, T101, X112, revA_in_ga(.(T101, T109), X112))
U16_gaga(T106, T109, T101, X112, revA_out_ga(.(T101, T109), X112)) → pL_out_gaga(T106, T109, T101, X112)
U14_ggaaga(T102, T103, T106, X111, T101, X112, pL_out_gaga(T106, X111, T101, X112)) → pE_out_ggaaga(T102, T103, T106, X111, T101, X112)
U3_gga(T101, T102, T103, X112, pE_out_ggaaga(T102, T103, X110, X111, T101, X112)) → rev2D_out_gga(T101, .(T102, T103), X112)
U9_ggaaga(T81, T82, T87, X84, T80, T84, rev2D_out_gga(T81, T82, T87)) → U10_ggaaga(T81, T82, T87, X84, T80, T84, pK_in_gaga(T87, X84, T80, T84))
pK_in_gaga(T87, T139, T80, T84) → U11_gaga(T87, T139, T80, T84, revG_in_ga(T87, T139))
U11_gaga(T87, T139, T80, T84, revG_out_ga(T87, T139)) → U12_gaga(T87, T139, T80, T84, revA_in_ga(.(T80, T139), T84))
U12_gaga(T87, T139, T80, T84, revA_out_ga(.(T80, T139), T84)) → pK_out_gaga(T87, T139, T80, T84)
U10_ggaaga(T81, T82, T87, X84, T80, T84, pK_out_gaga(T87, X84, T80, T84)) → pJ_out_ggaaga(T81, T82, T87, X84, T80, T84)
U6_ggga(T80, T81, T82, T84, pJ_out_ggaaga(T81, T82, X83, X84, T80, T84)) → rev2I_out_ggga(T80, T81, T82, T84)
U8_ggaga(T36, T37, T39, T35, T43, rev2I_out_ggga(T35, T36, T37, T43)) → pB_out_ggaga(T36, T37, T39, T35, T43)
U1_ga(T35, T36, T37, T39, T40, pB_out_ggaga(T36, T37, T39, T35, T40)) → revA_out_ga(.(T35, .(T36, T37)), .(T39, T40))

The argument filtering Pi contains the following mapping:
revA_in_ga(x1, x2) = revA_in_ga(x1)
[] = []
revA_out_ga(x1, x2) = revA_out_ga(x1, x2)
.(x1, x2) = .(x1, x2)
U1_ga(x1, x2, x3, x4, x5, x6) = U1_ga(x1, x2, x3, x6)
pB_in_ggaga(x1, x2, x3, x4, x5) = pB_in_ggaga(x1, x2, x4)
U7_ggaga(x1, x2, x3, x4, x5, x6) = U7_ggaga(x1, x2, x4, x6)
rev1C_in_gga(x1, x2, x3) = rev1C_in_gga(x1, x2)
rev1C_out_gga(x1, x2, x3) = rev1C_out_gga(x1, x2, x3)
U2_gga(x1, x2, x3, x4, x5) = U2_gga(x1, x2, x3, x5)
U8_ggaga(x1, x2, x3, x4, x5, x6) = U8_ggaga(x1, x2, x3, x4, x6)
rev2I_in_ggga(x1, x2, x3, x4) = rev2I_in_ggga(x1, x2, x3)
U6_ggga(x1, x2, x3, x4, x5) = U6_ggga(x1, x2, x3, x5)
pJ_in_ggaaga(x1, x2, x3, x4, x5, x6) = pJ_in_ggaaga(x1, x2, x5)
U9_ggaaga(x1, x2, x3, x4, x5, x6, x7) = U9_ggaaga(x1, x2, x5, x7)
rev2D_in_gga(x1, x2, x3) = rev2D_in_gga(x1, x2)
rev2D_out_gga(x1, x2, x3) = rev2D_out_gga(x1, x2, x3)
U3_gga(x1, x2, x3, x4, x5) = U3_gga(x1, x2, x3, x5)
pE_in_ggaaga(x1, x2, x3, x4, x5, x6) = pE_in_ggaaga(x1, x2, x5)
U13_ggaaga(x1, x2, x3, x4, x5, x6, x7) = U13_ggaaga(x1, x2, x5, x7)
U14_ggaaga(x1, x2, x3, x4, x5, x6, x7) = U14_ggaaga(x1, x2, x3, x5, x7)
pL_in_gaga(x1, x2, x3, x4) = pL_in_gaga(x1, x3)
U15_gaga(x1, x2, x3, x4, x5) = U15_gaga(x1, x3, x5)
revG_in_ga(x1, x2) = revG_in_ga(x1)
revG_out_ga(x1, x2) = revG_out_ga(x1, x2)
U5_ga(x1, x2, x3, x4, x5) = U5_ga(x1, x2, x5)
pH_in_ggaa(x1, x2, x3, x4) = pH_in_ggaa(x1, x2)
U17_ggaa(x1, x2, x3, x4, x5) = U17_ggaa(x1, x2, x5)
rev1F_in_gga(x1, x2, x3) = rev1F_in_gga(x1, x2)
rev1F_out_gga(x1, x2, x3) = rev1F_out_gga(x1, x2, x3)
U4_gga(x1, x2, x3, x4, x5) = U4_gga(x1, x2, x3, x5)
U18_ggaa(x1, x2, x3, x4, x5) = U18_ggaa(x1, x2, x3, x5)
pH_out_ggaa(x1, x2, x3, x4) = pH_out_ggaa(x1, x2, x3, x4)
U16_gaga(x1, x2, x3, x4, x5) = U16_gaga(x1, x2, x3, x5)
pL_out_gaga(x1, x2, x3, x4) = pL_out_gaga(x1, x2, x3, x4)
pE_out_ggaaga(x1, x2, x3, x4, x5, x6) = pE_out_ggaaga(x1, x2, x3, x4, x5, x6)
U10_ggaaga(x1, x2, x3, x4, x5, x6, x7) = U10_ggaaga(x1, x2, x3, x5, x7)
pK_in_gaga(x1, x2, x3, x4) = pK_in_gaga(x1, x3)
U11_gaga(x1, x2, x3, x4, x5) = U11_gaga(x1, x3, x5)
U12_gaga(x1, x2, x3, x4, x5) = U12_gaga(x1, x2, x3, x5)
pK_out_gaga(x1, x2, x3, x4) = pK_out_gaga(x1, x2, x3, x4)
pJ_out_ggaaga(x1, x2, x3, x4, x5, x6) = pJ_out_ggaaga(x1, x2, x3, x4, x5, x6)
rev2I_out_ggga(x1, x2, x3, x4) = rev2I_out_ggga(x1, x2, x3, x4)
pB_out_ggaga(x1, x2, x3, x4, x5) = pB_out_ggaga(x1, x2, x3, x4, x5)
REVA_IN_GA(x1, x2) = REVA_IN_GA(x1)
U1_GA(x1, x2, x3, x4, x5, x6) = U1_GA(x1, x2, x3, x6)
PB_IN_GGAGA(x1, x2, x3, x4, x5) = PB_IN_GGAGA(x1, x2, x4)
U7_GGAGA(x1, x2, x3, x4, x5, x6) = U7_GGAGA(x1, x2, x4, x6)
REV1C_IN_GGA(x1, x2, x3) = REV1C_IN_GGA(x1, x2)
U2_GGA(x1, x2, x3, x4, x5) = U2_GGA(x1, x2, x3, x5)
U8_GGAGA(x1, x2, x3, x4, x5, x6) = U8_GGAGA(x1, x2, x3, x4, x6)
REV2I_IN_GGGA(x1, x2, x3, x4) = REV2I_IN_GGGA(x1, x2, x3)
U6_GGGA(x1, x2, x3, x4, x5) = U6_GGGA(x1, x2, x3, x5)
PJ_IN_GGAAGA(x1, x2, x3, x4, x5, x6) = PJ_IN_GGAAGA(x1, x2, x5)
U9_GGAAGA(x1, x2, x3, x4, x5, x6, x7) = U9_GGAAGA(x1, x2, x5, x7)
REV2D_IN_GGA(x1, x2, x3) = REV2D_IN_GGA(x1, x2)
U3_GGA(x1, x2, x3, x4, x5) = U3_GGA(x1, x2, x3, x5)
PE_IN_GGAAGA(x1, x2, x3, x4, x5, x6) = PE_IN_GGAAGA(x1, x2, x5)
U13_GGAAGA(x1, x2, x3, x4, x5, x6, x7) = U13_GGAAGA(x1, x2, x5, x7)
U14_GGAAGA(x1, x2, x3, x4, x5, x6, x7) = U14_GGAAGA(x1, x2, x3, x5, x7)
PL_IN_GAGA(x1, x2, x3, x4) = PL_IN_GAGA(x1, x3)
U15_GAGA(x1, x2, x3, x4, x5) = U15_GAGA(x1, x3, x5)
REVG_IN_GA(x1, x2) = REVG_IN_GA(x1)
U5_GA(x1, x2, x3, x4, x5) = U5_GA(x1, x2, x5)
PH_IN_GGAA(x1, x2, x3, x4) = PH_IN_GGAA(x1, x2)
U17_GGAA(x1, x2, x3, x4, x5) = U17_GGAA(x1, x2, x5)
REV1F_IN_GGA(x1, x2, x3) = REV1F_IN_GGA(x1, x2)
U4_GGA(x1, x2, x3, x4, x5) = U4_GGA(x1, x2, x3, x5)
U18_GGAA(x1, x2, x3, x4, x5) = U18_GGAA(x1, x2, x3, x5)
U16_GAGA(x1, x2, x3, x4, x5) = U16_GAGA(x1, x2, x3, x5)
U10_GGAAGA(x1, x2, x3, x4, x5, x6, x7) = U10_GGAAGA(x1, x2, x3, x5, x7)
PK_IN_GAGA(x1, x2, x3, x4) = PK_IN_GAGA(x1, x3)
U11_GAGA(x1, x2, x3, x4, x5) = U11_GAGA(x1, x3, x5)
U12_GAGA(x1, x2, x3, x4, x5) = U12_GAGA(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:

REVA_IN_GA(.(T35, .(T36, T37)), .(T39, T40)) → U1_GA(T35, T36, T37, T39, T40, pB_in_ggaga(T36, T37, T39, T35, T40))
REVA_IN_GA(.(T35, .(T36, T37)), .(T39, T40)) → PB_IN_GGAGA(T36, T37, T39, T35, T40)
PB_IN_GGAGA(T36, T37, T39, T35, T43) → U7_GGAGA(T36, T37, T39, T35, T43, rev1C_in_gga(T36, T37, T39))
PB_IN_GGAGA(T36, T37, T39, T35, T43) → REV1C_IN_GGA(T36, T37, T39)
REV1C_IN_GGA(T59, .(T60, T61), T63) → U2_GGA(T59, T60, T61, T63, rev1C_in_gga(T60, T61, T63))
REV1C_IN_GGA(T59, .(T60, T61), T63) → REV1C_IN_GGA(T60, T61, T63)
U7_GGAGA(T36, T37, T39, T35, T43, rev1C_out_gga(T36, T37, T39)) → U8_GGAGA(T36, T37, T39, T35, T43, rev2I_in_ggga(T35, T36, T37, T43))
U7_GGAGA(T36, T37, T39, T35, T43, rev1C_out_gga(T36, T37, T39)) → REV2I_IN_GGGA(T35, T36, T37, T43)
REV2I_IN_GGGA(T80, T81, T82, T84) → U6_GGGA(T80, T81, T82, T84, pJ_in_ggaaga(T81, T82, X83, X84, T80, T84))
REV2I_IN_GGGA(T80, T81, T82, T84) → PJ_IN_GGAAGA(T81, T82, X83, X84, T80, T84)
PJ_IN_GGAAGA(T81, T82, T87, X84, T80, T84) → U9_GGAAGA(T81, T82, T87, X84, T80, T84, rev2D_in_gga(T81, T82, T87))
PJ_IN_GGAAGA(T81, T82, T87, X84, T80, T84) → REV2D_IN_GGA(T81, T82, T87)
REV2D_IN_GGA(T101, .(T102, T103), X112) → U3_GGA(T101, T102, T103, X112, pE_in_ggaaga(T102, T103, X110, X111, T101, X112))
REV2D_IN_GGA(T101, .(T102, T103), X112) → PE_IN_GGAAGA(T102, T103, X110, X111, T101, X112)
PE_IN_GGAAGA(T102, T103, T106, X111, T101, X112) → U13_GGAAGA(T102, T103, T106, X111, T101, X112, rev2D_in_gga(T102, T103, T106))
PE_IN_GGAAGA(T102, T103, T106, X111, T101, X112) → REV2D_IN_GGA(T102, T103, T106)
U13_GGAAGA(T102, T103, T106, X111, T101, X112, rev2D_out_gga(T102, T103, T106)) → U14_GGAAGA(T102, T103, T106, X111, T101, X112, pL_in_gaga(T106, X111, T101, X112))
U13_GGAAGA(T102, T103, T106, X111, T101, X112, rev2D_out_gga(T102, T103, T106)) → PL_IN_GAGA(T106, X111, T101, X112)
PL_IN_GAGA(T106, T109, T101, X112) → U15_GAGA(T106, T109, T101, X112, revG_in_ga(T106, T109))
PL_IN_GAGA(T106, T109, T101, X112) → REVG_IN_GA(T106, T109)
REVG_IN_GA(.(T114, T115), .(X133, X134)) → U5_GA(T114, T115, X133, X134, pH_in_ggaa(T114, T115, X133, X134))
REVG_IN_GA(.(T114, T115), .(X133, X134)) → PH_IN_GGAA(T114, T115, X133, X134)
PH_IN_GGAA(T114, T115, T118, X134) → U17_GGAA(T114, T115, T118, X134, rev1F_in_gga(T114, T115, T118))
PH_IN_GGAA(T114, T115, T118, X134) → REV1F_IN_GGA(T114, T115, T118)
REV1F_IN_GGA(T132, .(T133, T134), X158) → U4_GGA(T132, T133, T134, X158, rev1F_in_gga(T133, T134, X158))
REV1F_IN_GGA(T132, .(T133, T134), X158) → REV1F_IN_GGA(T133, T134, X158)
U17_GGAA(T114, T115, T118, X134, rev1F_out_gga(T114, T115, T118)) → U18_GGAA(T114, T115, T118, X134, rev2D_in_gga(T114, T115, X134))
U17_GGAA(T114, T115, T118, X134, rev1F_out_gga(T114, T115, T118)) → REV2D_IN_GGA(T114, T115, X134)
U15_GAGA(T106, T109, T101, X112, revG_out_ga(T106, T109)) → U16_GAGA(T106, T109, T101, X112, revA_in_ga(.(T101, T109), X112))
U15_GAGA(T106, T109, T101, X112, revG_out_ga(T106, T109)) → REVA_IN_GA(.(T101, T109), X112)
U9_GGAAGA(T81, T82, T87, X84, T80, T84, rev2D_out_gga(T81, T82, T87)) → U10_GGAAGA(T81, T82, T87, X84, T80, T84, pK_in_gaga(T87, X84, T80, T84))
U9_GGAAGA(T81, T82, T87, X84, T80, T84, rev2D_out_gga(T81, T82, T87)) → PK_IN_GAGA(T87, X84, T80, T84)
PK_IN_GAGA(T87, T139, T80, T84) → U11_GAGA(T87, T139, T80, T84, revG_in_ga(T87, T139))
PK_IN_GAGA(T87, T139, T80, T84) → REVG_IN_GA(T87, T139)
U11_GAGA(T87, T139, T80, T84, revG_out_ga(T87, T139)) → U12_GAGA(T87, T139, T80, T84, revA_in_ga(.(T80, T139), T84))
U11_GAGA(T87, T139, T80, T84, revG_out_ga(T87, T139)) → REVA_IN_GA(.(T80, T139), T84)

The TRS R consists of the following rules:

revA_in_ga([], []) → revA_out_ga([], [])
revA_in_ga(.(T25, []), .(T25, [])) → revA_out_ga(.(T25, []), .(T25, []))
revA_in_ga(.(T35, .(T36, T37)), .(T39, T40)) → U1_ga(T35, T36, T37, T39, T40, pB_in_ggaga(T36, T37, T39, T35, T40))
pB_in_ggaga(T36, T37, T39, T35, T43) → U7_ggaga(T36, T37, T39, T35, T43, rev1C_in_gga(T36, T37, T39))
rev1C_in_gga(T50, [], T50) → rev1C_out_gga(T50, [], T50)
rev1C_in_gga(T59, .(T60, T61), T63) → U2_gga(T59, T60, T61, T63, rev1C_in_gga(T60, T61, T63))
U2_gga(T59, T60, T61, T63, rev1C_out_gga(T60, T61, T63)) → rev1C_out_gga(T59, .(T60, T61), T63)
U7_ggaga(T36, T37, T39, T35, T43, rev1C_out_gga(T36, T37, T39)) → U8_ggaga(T36, T37, T39, T35, T43, rev2I_in_ggga(T35, T36, T37, T43))
rev2I_in_ggga(T80, T81, T82, T84) → U6_ggga(T80, T81, T82, T84, pJ_in_ggaaga(T81, T82, X83, X84, T80, T84))
pJ_in_ggaaga(T81, T82, T87, X84, T80, T84) → U9_ggaaga(T81, T82, T87, X84, T80, T84, rev2D_in_gga(T81, T82, T87))
rev2D_in_gga(T94, [], []) → rev2D_out_gga(T94, [], [])
rev2D_in_gga(T101, .(T102, T103), X112) → U3_gga(T101, T102, T103, X112, pE_in_ggaaga(T102, T103, X110, X111, T101, X112))
pE_in_ggaaga(T102, T103, T106, X111, T101, X112) → U13_ggaaga(T102, T103, T106, X111, T101, X112, rev2D_in_gga(T102, T103, T106))
U13_ggaaga(T102, T103, T106, X111, T101, X112, rev2D_out_gga(T102, T103, T106)) → U14_ggaaga(T102, T103, T106, X111, T101, X112, pL_in_gaga(T106, X111, T101, X112))
pL_in_gaga(T106, T109, T101, X112) → U15_gaga(T106, T109, T101, X112, revG_in_ga(T106, T109))
revG_in_ga([], []) → revG_out_ga([], [])
revG_in_ga(.(T114, T115), .(X133, X134)) → U5_ga(T114, T115, X133, X134, pH_in_ggaa(T114, T115, X133, X134))
pH_in_ggaa(T114, T115, T118, X134) → U17_ggaa(T114, T115, T118, X134, rev1F_in_gga(T114, T115, T118))
rev1F_in_gga(T125, [], T125) → rev1F_out_gga(T125, [], T125)
rev1F_in_gga(T132, .(T133, T134), X158) → U4_gga(T132, T133, T134, X158, rev1F_in_gga(T133, T134, X158))
U4_gga(T132, T133, T134, X158, rev1F_out_gga(T133, T134, X158)) → rev1F_out_gga(T132, .(T133, T134), X158)
U17_ggaa(T114, T115, T118, X134, rev1F_out_gga(T114, T115, T118)) → U18_ggaa(T114, T115, T118, X134, rev2D_in_gga(T114, T115, X134))
U18_ggaa(T114, T115, T118, X134, rev2D_out_gga(T114, T115, X134)) → pH_out_ggaa(T114, T115, T118, X134)
U5_ga(T114, T115, X133, X134, pH_out_ggaa(T114, T115, X133, X134)) → revG_out_ga(.(T114, T115), .(X133, X134))
U15_gaga(T106, T109, T101, X112, revG_out_ga(T106, T109)) → U16_gaga(T106, T109, T101, X112, revA_in_ga(.(T101, T109), X112))
U16_gaga(T106, T109, T101, X112, revA_out_ga(.(T101, T109), X112)) → pL_out_gaga(T106, T109, T101, X112)
U14_ggaaga(T102, T103, T106, X111, T101, X112, pL_out_gaga(T106, X111, T101, X112)) → pE_out_ggaaga(T102, T103, T106, X111, T101, X112)
U3_gga(T101, T102, T103, X112, pE_out_ggaaga(T102, T103, X110, X111, T101, X112)) → rev2D_out_gga(T101, .(T102, T103), X112)
U9_ggaaga(T81, T82, T87, X84, T80, T84, rev2D_out_gga(T81, T82, T87)) → U10_ggaaga(T81, T82, T87, X84, T80, T84, pK_in_gaga(T87, X84, T80, T84))
pK_in_gaga(T87, T139, T80, T84) → U11_gaga(T87, T139, T80, T84, revG_in_ga(T87, T139))
U11_gaga(T87, T139, T80, T84, revG_out_ga(T87, T139)) → U12_gaga(T87, T139, T80, T84, revA_in_ga(.(T80, T139), T84))
U12_gaga(T87, T139, T80, T84, revA_out_ga(.(T80, T139), T84)) → pK_out_gaga(T87, T139, T80, T84)
U10_ggaaga(T81, T82, T87, X84, T80, T84, pK_out_gaga(T87, X84, T80, T84)) → pJ_out_ggaaga(T81, T82, T87, X84, T80, T84)
U6_ggga(T80, T81, T82, T84, pJ_out_ggaaga(T81, T82, X83, X84, T80, T84)) → rev2I_out_ggga(T80, T81, T82, T84)
U8_ggaga(T36, T37, T39, T35, T43, rev2I_out_ggga(T35, T36, T37, T43)) → pB_out_ggaga(T36, T37, T39, T35, T43)
U1_ga(T35, T36, T37, T39, T40, pB_out_ggaga(T36, T37, T39, T35, T40)) → revA_out_ga(.(T35, .(T36, T37)), .(T39, T40))

(5) DependencyGraphProof (EQUIVALENT transformation)

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

(6) Complex Obligation (AND)

(7) Obligation:

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

REV1F_IN_GGA(T132, .(T133, T134), X158) → REV1F_IN_GGA(T133, T134, X158)

The TRS R consists of the following rules:

revA_in_ga([], []) → revA_out_ga([], [])
revA_in_ga(.(T25, []), .(T25, [])) → revA_out_ga(.(T25, []), .(T25, []))
revA_in_ga(.(T35, .(T36, T37)), .(T39, T40)) → U1_ga(T35, T36, T37, T39, T40, pB_in_ggaga(T36, T37, T39, T35, T40))
pB_in_ggaga(T36, T37, T39, T35, T43) → U7_ggaga(T36, T37, T39, T35, T43, rev1C_in_gga(T36, T37, T39))
rev1C_in_gga(T50, [], T50) → rev1C_out_gga(T50, [], T50)
rev1C_in_gga(T59, .(T60, T61), T63) → U2_gga(T59, T60, T61, T63, rev1C_in_gga(T60, T61, T63))
U2_gga(T59, T60, T61, T63, rev1C_out_gga(T60, T61, T63)) → rev1C_out_gga(T59, .(T60, T61), T63)
U7_ggaga(T36, T37, T39, T35, T43, rev1C_out_gga(T36, T37, T39)) → U8_ggaga(T36, T37, T39, T35, T43, rev2I_in_ggga(T35, T36, T37, T43))
rev2I_in_ggga(T80, T81, T82, T84) → U6_ggga(T80, T81, T82, T84, pJ_in_ggaaga(T81, T82, X83, X84, T80, T84))
pJ_in_ggaaga(T81, T82, T87, X84, T80, T84) → U9_ggaaga(T81, T82, T87, X84, T80, T84, rev2D_in_gga(T81, T82, T87))
rev2D_in_gga(T94, [], []) → rev2D_out_gga(T94, [], [])
rev2D_in_gga(T101, .(T102, T103), X112) → U3_gga(T101, T102, T103, X112, pE_in_ggaaga(T102, T103, X110, X111, T101, X112))
pE_in_ggaaga(T102, T103, T106, X111, T101, X112) → U13_ggaaga(T102, T103, T106, X111, T101, X112, rev2D_in_gga(T102, T103, T106))
U13_ggaaga(T102, T103, T106, X111, T101, X112, rev2D_out_gga(T102, T103, T106)) → U14_ggaaga(T102, T103, T106, X111, T101, X112, pL_in_gaga(T106, X111, T101, X112))
pL_in_gaga(T106, T109, T101, X112) → U15_gaga(T106, T109, T101, X112, revG_in_ga(T106, T109))
revG_in_ga([], []) → revG_out_ga([], [])
revG_in_ga(.(T114, T115), .(X133, X134)) → U5_ga(T114, T115, X133, X134, pH_in_ggaa(T114, T115, X133, X134))
pH_in_ggaa(T114, T115, T118, X134) → U17_ggaa(T114, T115, T118, X134, rev1F_in_gga(T114, T115, T118))
rev1F_in_gga(T125, [], T125) → rev1F_out_gga(T125, [], T125)
rev1F_in_gga(T132, .(T133, T134), X158) → U4_gga(T132, T133, T134, X158, rev1F_in_gga(T133, T134, X158))
U4_gga(T132, T133, T134, X158, rev1F_out_gga(T133, T134, X158)) → rev1F_out_gga(T132, .(T133, T134), X158)
U17_ggaa(T114, T115, T118, X134, rev1F_out_gga(T114, T115, T118)) → U18_ggaa(T114, T115, T118, X134, rev2D_in_gga(T114, T115, X134))
U18_ggaa(T114, T115, T118, X134, rev2D_out_gga(T114, T115, X134)) → pH_out_ggaa(T114, T115, T118, X134)
U5_ga(T114, T115, X133, X134, pH_out_ggaa(T114, T115, X133, X134)) → revG_out_ga(.(T114, T115), .(X133, X134))
U15_gaga(T106, T109, T101, X112, revG_out_ga(T106, T109)) → U16_gaga(T106, T109, T101, X112, revA_in_ga(.(T101, T109), X112))
U16_gaga(T106, T109, T101, X112, revA_out_ga(.(T101, T109), X112)) → pL_out_gaga(T106, T109, T101, X112)
U14_ggaaga(T102, T103, T106, X111, T101, X112, pL_out_gaga(T106, X111, T101, X112)) → pE_out_ggaaga(T102, T103, T106, X111, T101, X112)
U3_gga(T101, T102, T103, X112, pE_out_ggaaga(T102, T103, X110, X111, T101, X112)) → rev2D_out_gga(T101, .(T102, T103), X112)
U9_ggaaga(T81, T82, T87, X84, T80, T84, rev2D_out_gga(T81, T82, T87)) → U10_ggaaga(T81, T82, T87, X84, T80, T84, pK_in_gaga(T87, X84, T80, T84))
pK_in_gaga(T87, T139, T80, T84) → U11_gaga(T87, T139, T80, T84, revG_in_ga(T87, T139))
U11_gaga(T87, T139, T80, T84, revG_out_ga(T87, T139)) → U12_gaga(T87, T139, T80, T84, revA_in_ga(.(T80, T139), T84))
U12_gaga(T87, T139, T80, T84, revA_out_ga(.(T80, T139), T84)) → pK_out_gaga(T87, T139, T80, T84)
U10_ggaaga(T81, T82, T87, X84, T80, T84, pK_out_gaga(T87, X84, T80, T84)) → pJ_out_ggaaga(T81, T82, T87, X84, T80, T84)
U6_ggga(T80, T81, T82, T84, pJ_out_ggaaga(T81, T82, X83, X84, T80, T84)) → rev2I_out_ggga(T80, T81, T82, T84)
U8_ggaga(T36, T37, T39, T35, T43, rev2I_out_ggga(T35, T36, T37, T43)) → pB_out_ggaga(T36, T37, T39, T35, T43)
U1_ga(T35, T36, T37, T39, T40, pB_out_ggaga(T36, T37, T39, T35, T40)) → revA_out_ga(.(T35, .(T36, T37)), .(T39, T40))

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

REV1F_IN_GGA(T132, .(T133, T134), X158) → REV1F_IN_GGA(T133, T134, X158)

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

REV1F_IN_GGA(T132, .(T133, T134)) → REV1F_IN_GGA(T133, T134)

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:

REV1F_IN_GGA(T132, .(T133, T134)) → REV1F_IN_GGA(T133, T134)
The graph contains the following edges 2 > 1, 2 > 2

(13) YES

(14) Obligation:

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

REV1C_IN_GGA(T59, .(T60, T61), T63) → REV1C_IN_GGA(T60, T61, T63)

The TRS R consists of the following rules:

revA_in_ga([], []) → revA_out_ga([], [])
revA_in_ga(.(T25, []), .(T25, [])) → revA_out_ga(.(T25, []), .(T25, []))
revA_in_ga(.(T35, .(T36, T37)), .(T39, T40)) → U1_ga(T35, T36, T37, T39, T40, pB_in_ggaga(T36, T37, T39, T35, T40))
pB_in_ggaga(T36, T37, T39, T35, T43) → U7_ggaga(T36, T37, T39, T35, T43, rev1C_in_gga(T36, T37, T39))
rev1C_in_gga(T50, [], T50) → rev1C_out_gga(T50, [], T50)
rev1C_in_gga(T59, .(T60, T61), T63) → U2_gga(T59, T60, T61, T63, rev1C_in_gga(T60, T61, T63))
U2_gga(T59, T60, T61, T63, rev1C_out_gga(T60, T61, T63)) → rev1C_out_gga(T59, .(T60, T61), T63)
U7_ggaga(T36, T37, T39, T35, T43, rev1C_out_gga(T36, T37, T39)) → U8_ggaga(T36, T37, T39, T35, T43, rev2I_in_ggga(T35, T36, T37, T43))
rev2I_in_ggga(T80, T81, T82, T84) → U6_ggga(T80, T81, T82, T84, pJ_in_ggaaga(T81, T82, X83, X84, T80, T84))
pJ_in_ggaaga(T81, T82, T87, X84, T80, T84) → U9_ggaaga(T81, T82, T87, X84, T80, T84, rev2D_in_gga(T81, T82, T87))
rev2D_in_gga(T94, [], []) → rev2D_out_gga(T94, [], [])
rev2D_in_gga(T101, .(T102, T103), X112) → U3_gga(T101, T102, T103, X112, pE_in_ggaaga(T102, T103, X110, X111, T101, X112))
pE_in_ggaaga(T102, T103, T106, X111, T101, X112) → U13_ggaaga(T102, T103, T106, X111, T101, X112, rev2D_in_gga(T102, T103, T106))
U13_ggaaga(T102, T103, T106, X111, T101, X112, rev2D_out_gga(T102, T103, T106)) → U14_ggaaga(T102, T103, T106, X111, T101, X112, pL_in_gaga(T106, X111, T101, X112))
pL_in_gaga(T106, T109, T101, X112) → U15_gaga(T106, T109, T101, X112, revG_in_ga(T106, T109))
revG_in_ga([], []) → revG_out_ga([], [])
revG_in_ga(.(T114, T115), .(X133, X134)) → U5_ga(T114, T115, X133, X134, pH_in_ggaa(T114, T115, X133, X134))
pH_in_ggaa(T114, T115, T118, X134) → U17_ggaa(T114, T115, T118, X134, rev1F_in_gga(T114, T115, T118))
rev1F_in_gga(T125, [], T125) → rev1F_out_gga(T125, [], T125)
rev1F_in_gga(T132, .(T133, T134), X158) → U4_gga(T132, T133, T134, X158, rev1F_in_gga(T133, T134, X158))
U4_gga(T132, T133, T134, X158, rev1F_out_gga(T133, T134, X158)) → rev1F_out_gga(T132, .(T133, T134), X158)
U17_ggaa(T114, T115, T118, X134, rev1F_out_gga(T114, T115, T118)) → U18_ggaa(T114, T115, T118, X134, rev2D_in_gga(T114, T115, X134))
U18_ggaa(T114, T115, T118, X134, rev2D_out_gga(T114, T115, X134)) → pH_out_ggaa(T114, T115, T118, X134)
U5_ga(T114, T115, X133, X134, pH_out_ggaa(T114, T115, X133, X134)) → revG_out_ga(.(T114, T115), .(X133, X134))
U15_gaga(T106, T109, T101, X112, revG_out_ga(T106, T109)) → U16_gaga(T106, T109, T101, X112, revA_in_ga(.(T101, T109), X112))
U16_gaga(T106, T109, T101, X112, revA_out_ga(.(T101, T109), X112)) → pL_out_gaga(T106, T109, T101, X112)
U14_ggaaga(T102, T103, T106, X111, T101, X112, pL_out_gaga(T106, X111, T101, X112)) → pE_out_ggaaga(T102, T103, T106, X111, T101, X112)
U3_gga(T101, T102, T103, X112, pE_out_ggaaga(T102, T103, X110, X111, T101, X112)) → rev2D_out_gga(T101, .(T102, T103), X112)
U9_ggaaga(T81, T82, T87, X84, T80, T84, rev2D_out_gga(T81, T82, T87)) → U10_ggaaga(T81, T82, T87, X84, T80, T84, pK_in_gaga(T87, X84, T80, T84))
pK_in_gaga(T87, T139, T80, T84) → U11_gaga(T87, T139, T80, T84, revG_in_ga(T87, T139))
U11_gaga(T87, T139, T80, T84, revG_out_ga(T87, T139)) → U12_gaga(T87, T139, T80, T84, revA_in_ga(.(T80, T139), T84))
U12_gaga(T87, T139, T80, T84, revA_out_ga(.(T80, T139), T84)) → pK_out_gaga(T87, T139, T80, T84)
U10_ggaaga(T81, T82, T87, X84, T80, T84, pK_out_gaga(T87, X84, T80, T84)) → pJ_out_ggaaga(T81, T82, T87, X84, T80, T84)
U6_ggga(T80, T81, T82, T84, pJ_out_ggaaga(T81, T82, X83, X84, T80, T84)) → rev2I_out_ggga(T80, T81, T82, T84)
U8_ggaga(T36, T37, T39, T35, T43, rev2I_out_ggga(T35, T36, T37, T43)) → pB_out_ggaga(T36, T37, T39, T35, T43)
U1_ga(T35, T36, T37, T39, T40, pB_out_ggaga(T36, T37, T39, T35, T40)) → revA_out_ga(.(T35, .(T36, T37)), .(T39, T40))

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

REV1C_IN_GGA(T59, .(T60, T61), T63) → REV1C_IN_GGA(T60, T61, T63)

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

REV1C_IN_GGA(T59, .(T60, T61)) → REV1C_IN_GGA(T60, T61)

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:

REV1C_IN_GGA(T59, .(T60, T61)) → REV1C_IN_GGA(T60, T61)
The graph contains the following edges 2 > 1, 2 > 2

(20) YES

(21) Obligation:

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

REVA_IN_GA(.(T35, .(T36, T37)), .(T39, T40)) → PB_IN_GGAGA(T36, T37, T39, T35, T40)
PB_IN_GGAGA(T36, T37, T39, T35, T43) → U7_GGAGA(T36, T37, T39, T35, T43, rev1C_in_gga(T36, T37, T39))
U7_GGAGA(T36, T37, T39, T35, T43, rev1C_out_gga(T36, T37, T39)) → REV2I_IN_GGGA(T35, T36, T37, T43)
REV2I_IN_GGGA(T80, T81, T82, T84) → PJ_IN_GGAAGA(T81, T82, X83, X84, T80, T84)
PJ_IN_GGAAGA(T81, T82, T87, X84, T80, T84) → U9_GGAAGA(T81, T82, T87, X84, T80, T84, rev2D_in_gga(T81, T82, T87))
U9_GGAAGA(T81, T82, T87, X84, T80, T84, rev2D_out_gga(T81, T82, T87)) → PK_IN_GAGA(T87, X84, T80, T84)
PK_IN_GAGA(T87, T139, T80, T84) → U11_GAGA(T87, T139, T80, T84, revG_in_ga(T87, T139))
U11_GAGA(T87, T139, T80, T84, revG_out_ga(T87, T139)) → REVA_IN_GA(.(T80, T139), T84)
PK_IN_GAGA(T87, T139, T80, T84) → REVG_IN_GA(T87, T139)
REVG_IN_GA(.(T114, T115), .(X133, X134)) → PH_IN_GGAA(T114, T115, X133, X134)
PH_IN_GGAA(T114, T115, T118, X134) → U17_GGAA(T114, T115, T118, X134, rev1F_in_gga(T114, T115, T118))
U17_GGAA(T114, T115, T118, X134, rev1F_out_gga(T114, T115, T118)) → REV2D_IN_GGA(T114, T115, X134)
REV2D_IN_GGA(T101, .(T102, T103), X112) → PE_IN_GGAAGA(T102, T103, X110, X111, T101, X112)
PE_IN_GGAAGA(T102, T103, T106, X111, T101, X112) → U13_GGAAGA(T102, T103, T106, X111, T101, X112, rev2D_in_gga(T102, T103, T106))
U13_GGAAGA(T102, T103, T106, X111, T101, X112, rev2D_out_gga(T102, T103, T106)) → PL_IN_GAGA(T106, X111, T101, X112)
PL_IN_GAGA(T106, T109, T101, X112) → U15_GAGA(T106, T109, T101, X112, revG_in_ga(T106, T109))
U15_GAGA(T106, T109, T101, X112, revG_out_ga(T106, T109)) → REVA_IN_GA(.(T101, T109), X112)
PL_IN_GAGA(T106, T109, T101, X112) → REVG_IN_GA(T106, T109)
PE_IN_GGAAGA(T102, T103, T106, X111, T101, X112) → REV2D_IN_GGA(T102, T103, T106)
PJ_IN_GGAAGA(T81, T82, T87, X84, T80, T84) → REV2D_IN_GGA(T81, T82, T87)

The TRS R consists of the following rules:

revA_in_ga([], []) → revA_out_ga([], [])
revA_in_ga(.(T25, []), .(T25, [])) → revA_out_ga(.(T25, []), .(T25, []))
revA_in_ga(.(T35, .(T36, T37)), .(T39, T40)) → U1_ga(T35, T36, T37, T39, T40, pB_in_ggaga(T36, T37, T39, T35, T40))
pB_in_ggaga(T36, T37, T39, T35, T43) → U7_ggaga(T36, T37, T39, T35, T43, rev1C_in_gga(T36, T37, T39))
rev1C_in_gga(T50, [], T50) → rev1C_out_gga(T50, [], T50)
rev1C_in_gga(T59, .(T60, T61), T63) → U2_gga(T59, T60, T61, T63, rev1C_in_gga(T60, T61, T63))
U2_gga(T59, T60, T61, T63, rev1C_out_gga(T60, T61, T63)) → rev1C_out_gga(T59, .(T60, T61), T63)
U7_ggaga(T36, T37, T39, T35, T43, rev1C_out_gga(T36, T37, T39)) → U8_ggaga(T36, T37, T39, T35, T43, rev2I_in_ggga(T35, T36, T37, T43))
rev2I_in_ggga(T80, T81, T82, T84) → U6_ggga(T80, T81, T82, T84, pJ_in_ggaaga(T81, T82, X83, X84, T80, T84))
pJ_in_ggaaga(T81, T82, T87, X84, T80, T84) → U9_ggaaga(T81, T82, T87, X84, T80, T84, rev2D_in_gga(T81, T82, T87))
rev2D_in_gga(T94, [], []) → rev2D_out_gga(T94, [], [])
rev2D_in_gga(T101, .(T102, T103), X112) → U3_gga(T101, T102, T103, X112, pE_in_ggaaga(T102, T103, X110, X111, T101, X112))
pE_in_ggaaga(T102, T103, T106, X111, T101, X112) → U13_ggaaga(T102, T103, T106, X111, T101, X112, rev2D_in_gga(T102, T103, T106))
U13_ggaaga(T102, T103, T106, X111, T101, X112, rev2D_out_gga(T102, T103, T106)) → U14_ggaaga(T102, T103, T106, X111, T101, X112, pL_in_gaga(T106, X111, T101, X112))
pL_in_gaga(T106, T109, T101, X112) → U15_gaga(T106, T109, T101, X112, revG_in_ga(T106, T109))
revG_in_ga([], []) → revG_out_ga([], [])
revG_in_ga(.(T114, T115), .(X133, X134)) → U5_ga(T114, T115, X133, X134, pH_in_ggaa(T114, T115, X133, X134))
pH_in_ggaa(T114, T115, T118, X134) → U17_ggaa(T114, T115, T118, X134, rev1F_in_gga(T114, T115, T118))
rev1F_in_gga(T125, [], T125) → rev1F_out_gga(T125, [], T125)
rev1F_in_gga(T132, .(T133, T134), X158) → U4_gga(T132, T133, T134, X158, rev1F_in_gga(T133, T134, X158))
U4_gga(T132, T133, T134, X158, rev1F_out_gga(T133, T134, X158)) → rev1F_out_gga(T132, .(T133, T134), X158)
U17_ggaa(T114, T115, T118, X134, rev1F_out_gga(T114, T115, T118)) → U18_ggaa(T114, T115, T118, X134, rev2D_in_gga(T114, T115, X134))
U18_ggaa(T114, T115, T118, X134, rev2D_out_gga(T114, T115, X134)) → pH_out_ggaa(T114, T115, T118, X134)
U5_ga(T114, T115, X133, X134, pH_out_ggaa(T114, T115, X133, X134)) → revG_out_ga(.(T114, T115), .(X133, X134))
U15_gaga(T106, T109, T101, X112, revG_out_ga(T106, T109)) → U16_gaga(T106, T109, T101, X112, revA_in_ga(.(T101, T109), X112))
U16_gaga(T106, T109, T101, X112, revA_out_ga(.(T101, T109), X112)) → pL_out_gaga(T106, T109, T101, X112)
U14_ggaaga(T102, T103, T106, X111, T101, X112, pL_out_gaga(T106, X111, T101, X112)) → pE_out_ggaaga(T102, T103, T106, X111, T101, X112)
U3_gga(T101, T102, T103, X112, pE_out_ggaaga(T102, T103, X110, X111, T101, X112)) → rev2D_out_gga(T101, .(T102, T103), X112)
U9_ggaaga(T81, T82, T87, X84, T80, T84, rev2D_out_gga(T81, T82, T87)) → U10_ggaaga(T81, T82, T87, X84, T80, T84, pK_in_gaga(T87, X84, T80, T84))
pK_in_gaga(T87, T139, T80, T84) → U11_gaga(T87, T139, T80, T84, revG_in_ga(T87, T139))
U11_gaga(T87, T139, T80, T84, revG_out_ga(T87, T139)) → U12_gaga(T87, T139, T80, T84, revA_in_ga(.(T80, T139), T84))
U12_gaga(T87, T139, T80, T84, revA_out_ga(.(T80, T139), T84)) → pK_out_gaga(T87, T139, T80, T84)
U10_ggaaga(T81, T82, T87, X84, T80, T84, pK_out_gaga(T87, X84, T80, T84)) → pJ_out_ggaaga(T81, T82, T87, X84, T80, T84)
U6_ggga(T80, T81, T82, T84, pJ_out_ggaaga(T81, T82, X83, X84, T80, T84)) → rev2I_out_ggga(T80, T81, T82, T84)
U8_ggaga(T36, T37, T39, T35, T43, rev2I_out_ggga(T35, T36, T37, T43)) → pB_out_ggaga(T36, T37, T39, T35, T43)
U1_ga(T35, T36, T37, T39, T40, pB_out_ggaga(T36, T37, T39, T35, T40)) → revA_out_ga(.(T35, .(T36, T37)), .(T39, T40))

The argument filtering Pi contains the following mapping:
revA_in_ga(x1, x2) = revA_in_ga(x1)
[] = []
revA_out_ga(x1, x2) = revA_out_ga(x1, x2)
.(x1, x2) = .(x1, x2)
U1_ga(x1, x2, x3, x4, x5, x6) = U1_ga(x1, x2, x3, x6)
pB_in_ggaga(x1, x2, x3, x4, x5) = pB_in_ggaga(x1, x2, x4)
U7_ggaga(x1, x2, x3, x4, x5, x6) = U7_ggaga(x1, x2, x4, x6)
rev1C_in_gga(x1, x2, x3) = rev1C_in_gga(x1, x2)
rev1C_out_gga(x1, x2, x3) = rev1C_out_gga(x1, x2, x3)
U2_gga(x1, x2, x3, x4, x5) = U2_gga(x1, x2, x3, x5)
U8_ggaga(x1, x2, x3, x4, x5, x6) = U8_ggaga(x1, x2, x3, x4, x6)
rev2I_in_ggga(x1, x2, x3, x4) = rev2I_in_ggga(x1, x2, x3)
U6_ggga(x1, x2, x3, x4, x5) = U6_ggga(x1, x2, x3, x5)
pJ_in_ggaaga(x1, x2, x3, x4, x5, x6) = pJ_in_ggaaga(x1, x2, x5)
U9_ggaaga(x1, x2, x3, x4, x5, x6, x7) = U9_ggaaga(x1, x2, x5, x7)
rev2D_in_gga(x1, x2, x3) = rev2D_in_gga(x1, x2)
rev2D_out_gga(x1, x2, x3) = rev2D_out_gga(x1, x2, x3)
U3_gga(x1, x2, x3, x4, x5) = U3_gga(x1, x2, x3, x5)
pE_in_ggaaga(x1, x2, x3, x4, x5, x6) = pE_in_ggaaga(x1, x2, x5)
U13_ggaaga(x1, x2, x3, x4, x5, x6, x7) = U13_ggaaga(x1, x2, x5, x7)
U14_ggaaga(x1, x2, x3, x4, x5, x6, x7) = U14_ggaaga(x1, x2, x3, x5, x7)
pL_in_gaga(x1, x2, x3, x4) = pL_in_gaga(x1, x3)
U15_gaga(x1, x2, x3, x4, x5) = U15_gaga(x1, x3, x5)
revG_in_ga(x1, x2) = revG_in_ga(x1)
revG_out_ga(x1, x2) = revG_out_ga(x1, x2)
U5_ga(x1, x2, x3, x4, x5) = U5_ga(x1, x2, x5)
pH_in_ggaa(x1, x2, x3, x4) = pH_in_ggaa(x1, x2)
U17_ggaa(x1, x2, x3, x4, x5) = U17_ggaa(x1, x2, x5)
rev1F_in_gga(x1, x2, x3) = rev1F_in_gga(x1, x2)
rev1F_out_gga(x1, x2, x3) = rev1F_out_gga(x1, x2, x3)
U4_gga(x1, x2, x3, x4, x5) = U4_gga(x1, x2, x3, x5)
U18_ggaa(x1, x2, x3, x4, x5) = U18_ggaa(x1, x2, x3, x5)
pH_out_ggaa(x1, x2, x3, x4) = pH_out_ggaa(x1, x2, x3, x4)
U16_gaga(x1, x2, x3, x4, x5) = U16_gaga(x1, x2, x3, x5)
pL_out_gaga(x1, x2, x3, x4) = pL_out_gaga(x1, x2, x3, x4)
pE_out_ggaaga(x1, x2, x3, x4, x5, x6) = pE_out_ggaaga(x1, x2, x3, x4, x5, x6)
U10_ggaaga(x1, x2, x3, x4, x5, x6, x7) = U10_ggaaga(x1, x2, x3, x5, x7)
pK_in_gaga(x1, x2, x3, x4) = pK_in_gaga(x1, x3)
U11_gaga(x1, x2, x3, x4, x5) = U11_gaga(x1, x3, x5)
U12_gaga(x1, x2, x3, x4, x5) = U12_gaga(x1, x2, x3, x5)
pK_out_gaga(x1, x2, x3, x4) = pK_out_gaga(x1, x2, x3, x4)
pJ_out_ggaaga(x1, x2, x3, x4, x5, x6) = pJ_out_ggaaga(x1, x2, x3, x4, x5, x6)
rev2I_out_ggga(x1, x2, x3, x4) = rev2I_out_ggga(x1, x2, x3, x4)
pB_out_ggaga(x1, x2, x3, x4, x5) = pB_out_ggaga(x1, x2, x3, x4, x5)
REVA_IN_GA(x1, x2) = REVA_IN_GA(x1)
PB_IN_GGAGA(x1, x2, x3, x4, x5) = PB_IN_GGAGA(x1, x2, x4)
U7_GGAGA(x1, x2, x3, x4, x5, x6) = U7_GGAGA(x1, x2, x4, x6)
REV2I_IN_GGGA(x1, x2, x3, x4) = REV2I_IN_GGGA(x1, x2, x3)
PJ_IN_GGAAGA(x1, x2, x3, x4, x5, x6) = PJ_IN_GGAAGA(x1, x2, x5)
U9_GGAAGA(x1, x2, x3, x4, x5, x6, x7) = U9_GGAAGA(x1, x2, x5, x7)
REV2D_IN_GGA(x1, x2, x3) = REV2D_IN_GGA(x1, x2)
PE_IN_GGAAGA(x1, x2, x3, x4, x5, x6) = PE_IN_GGAAGA(x1, x2, x5)
U13_GGAAGA(x1, x2, x3, x4, x5, x6, x7) = U13_GGAAGA(x1, x2, x5, x7)
PL_IN_GAGA(x1, x2, x3, x4) = PL_IN_GAGA(x1, x3)
U15_GAGA(x1, x2, x3, x4, x5) = U15_GAGA(x1, x3, x5)
REVG_IN_GA(x1, x2) = REVG_IN_GA(x1)
PH_IN_GGAA(x1, x2, x3, x4) = PH_IN_GGAA(x1, x2)
U17_GGAA(x1, x2, x3, x4, x5) = U17_GGAA(x1, x2, x5)
PK_IN_GAGA(x1, x2, x3, x4) = PK_IN_GAGA(x1, x3)
U11_GAGA(x1, x2, x3, x4, x5) = U11_GAGA(x1, x3, x5)

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:

REVA_IN_GA(.(T35, .(T36, T37)), .(T39, T40)) → PB_IN_GGAGA(T36, T37, T39, T35, T40)
PB_IN_GGAGA(T36, T37, T39, T35, T43) → U7_GGAGA(T36, T37, T39, T35, T43, rev1C_in_gga(T36, T37, T39))
U7_GGAGA(T36, T37, T39, T35, T43, rev1C_out_gga(T36, T37, T39)) → REV2I_IN_GGGA(T35, T36, T37, T43)
REV2I_IN_GGGA(T80, T81, T82, T84) → PJ_IN_GGAAGA(T81, T82, X83, X84, T80, T84)
PJ_IN_GGAAGA(T81, T82, T87, X84, T80, T84) → U9_GGAAGA(T81, T82, T87, X84, T80, T84, rev2D_in_gga(T81, T82, T87))
U9_GGAAGA(T81, T82, T87, X84, T80, T84, rev2D_out_gga(T81, T82, T87)) → PK_IN_GAGA(T87, X84, T80, T84)
PK_IN_GAGA(T87, T139, T80, T84) → U11_GAGA(T87, T139, T80, T84, revG_in_ga(T87, T139))
U11_GAGA(T87, T139, T80, T84, revG_out_ga(T87, T139)) → REVA_IN_GA(.(T80, T139), T84)
PK_IN_GAGA(T87, T139, T80, T84) → REVG_IN_GA(T87, T139)
REVG_IN_GA(.(T114, T115), .(X133, X134)) → PH_IN_GGAA(T114, T115, X133, X134)
PH_IN_GGAA(T114, T115, T118, X134) → U17_GGAA(T114, T115, T118, X134, rev1F_in_gga(T114, T115, T118))
U17_GGAA(T114, T115, T118, X134, rev1F_out_gga(T114, T115, T118)) → REV2D_IN_GGA(T114, T115, X134)
REV2D_IN_GGA(T101, .(T102, T103), X112) → PE_IN_GGAAGA(T102, T103, X110, X111, T101, X112)
PE_IN_GGAAGA(T102, T103, T106, X111, T101, X112) → U13_GGAAGA(T102, T103, T106, X111, T101, X112, rev2D_in_gga(T102, T103, T106))
U13_GGAAGA(T102, T103, T106, X111, T101, X112, rev2D_out_gga(T102, T103, T106)) → PL_IN_GAGA(T106, X111, T101, X112)
PL_IN_GAGA(T106, T109, T101, X112) → U15_GAGA(T106, T109, T101, X112, revG_in_ga(T106, T109))
U15_GAGA(T106, T109, T101, X112, revG_out_ga(T106, T109)) → REVA_IN_GA(.(T101, T109), X112)
PL_IN_GAGA(T106, T109, T101, X112) → REVG_IN_GA(T106, T109)
PE_IN_GGAAGA(T102, T103, T106, X111, T101, X112) → REV2D_IN_GGA(T102, T103, T106)
PJ_IN_GGAAGA(T81, T82, T87, X84, T80, T84) → REV2D_IN_GGA(T81, T82, T87)

The TRS R consists of the following rules:

rev1C_in_gga(T50, [], T50) → rev1C_out_gga(T50, [], T50)
rev1C_in_gga(T59, .(T60, T61), T63) → U2_gga(T59, T60, T61, T63, rev1C_in_gga(T60, T61, T63))
rev2D_in_gga(T94, [], []) → rev2D_out_gga(T94, [], [])
rev2D_in_gga(T101, .(T102, T103), X112) → U3_gga(T101, T102, T103, X112, pE_in_ggaaga(T102, T103, X110, X111, T101, X112))
revG_in_ga([], []) → revG_out_ga([], [])
revG_in_ga(.(T114, T115), .(X133, X134)) → U5_ga(T114, T115, X133, X134, pH_in_ggaa(T114, T115, X133, X134))
rev1F_in_gga(T125, [], T125) → rev1F_out_gga(T125, [], T125)
rev1F_in_gga(T132, .(T133, T134), X158) → U4_gga(T132, T133, T134, X158, rev1F_in_gga(T133, T134, X158))
U2_gga(T59, T60, T61, T63, rev1C_out_gga(T60, T61, T63)) → rev1C_out_gga(T59, .(T60, T61), T63)
U3_gga(T101, T102, T103, X112, pE_out_ggaaga(T102, T103, X110, X111, T101, X112)) → rev2D_out_gga(T101, .(T102, T103), X112)
U5_ga(T114, T115, X133, X134, pH_out_ggaa(T114, T115, X133, X134)) → revG_out_ga(.(T114, T115), .(X133, X134))
U4_gga(T132, T133, T134, X158, rev1F_out_gga(T133, T134, X158)) → rev1F_out_gga(T132, .(T133, T134), X158)
pE_in_ggaaga(T102, T103, T106, X111, T101, X112) → U13_ggaaga(T102, T103, T106, X111, T101, X112, rev2D_in_gga(T102, T103, T106))
pH_in_ggaa(T114, T115, T118, X134) → U17_ggaa(T114, T115, T118, X134, rev1F_in_gga(T114, T115, T118))
U13_ggaaga(T102, T103, T106, X111, T101, X112, rev2D_out_gga(T102, T103, T106)) → U14_ggaaga(T102, T103, T106, X111, T101, X112, pL_in_gaga(T106, X111, T101, X112))
U17_ggaa(T114, T115, T118, X134, rev1F_out_gga(T114, T115, T118)) → U18_ggaa(T114, T115, T118, X134, rev2D_in_gga(T114, T115, X134))
U14_ggaaga(T102, T103, T106, X111, T101, X112, pL_out_gaga(T106, X111, T101, X112)) → pE_out_ggaaga(T102, T103, T106, X111, T101, X112)
U18_ggaa(T114, T115, T118, X134, rev2D_out_gga(T114, T115, X134)) → pH_out_ggaa(T114, T115, T118, X134)
pL_in_gaga(T106, T109, T101, X112) → U15_gaga(T106, T109, T101, X112, revG_in_ga(T106, T109))
U15_gaga(T106, T109, T101, X112, revG_out_ga(T106, T109)) → U16_gaga(T106, T109, T101, X112, revA_in_ga(.(T101, T109), X112))
U16_gaga(T106, T109, T101, X112, revA_out_ga(.(T101, T109), X112)) → pL_out_gaga(T106, T109, T101, X112)
revA_in_ga(.(T25, []), .(T25, [])) → revA_out_ga(.(T25, []), .(T25, []))
revA_in_ga(.(T35, .(T36, T37)), .(T39, T40)) → U1_ga(T35, T36, T37, T39, T40, pB_in_ggaga(T36, T37, T39, T35, T40))
U1_ga(T35, T36, T37, T39, T40, pB_out_ggaga(T36, T37, T39, T35, T40)) → revA_out_ga(.(T35, .(T36, T37)), .(T39, T40))
pB_in_ggaga(T36, T37, T39, T35, T43) → U7_ggaga(T36, T37, T39, T35, T43, rev1C_in_gga(T36, T37, T39))
U7_ggaga(T36, T37, T39, T35, T43, rev1C_out_gga(T36, T37, T39)) → U8_ggaga(T36, T37, T39, T35, T43, rev2I_in_ggga(T35, T36, T37, T43))
U8_ggaga(T36, T37, T39, T35, T43, rev2I_out_ggga(T35, T36, T37, T43)) → pB_out_ggaga(T36, T37, T39, T35, T43)
rev2I_in_ggga(T80, T81, T82, T84) → U6_ggga(T80, T81, T82, T84, pJ_in_ggaaga(T81, T82, X83, X84, T80, T84))
U6_ggga(T80, T81, T82, T84, pJ_out_ggaaga(T81, T82, X83, X84, T80, T84)) → rev2I_out_ggga(T80, T81, T82, T84)
pJ_in_ggaaga(T81, T82, T87, X84, T80, T84) → U9_ggaaga(T81, T82, T87, X84, T80, T84, rev2D_in_gga(T81, T82, T87))
U9_ggaaga(T81, T82, T87, X84, T80, T84, rev2D_out_gga(T81, T82, T87)) → U10_ggaaga(T81, T82, T87, X84, T80, T84, pK_in_gaga(T87, X84, T80, T84))
U10_ggaaga(T81, T82, T87, X84, T80, T84, pK_out_gaga(T87, X84, T80, T84)) → pJ_out_ggaaga(T81, T82, T87, X84, T80, T84)
pK_in_gaga(T87, T139, T80, T84) → U11_gaga(T87, T139, T80, T84, revG_in_ga(T87, T139))
U11_gaga(T87, T139, T80, T84, revG_out_ga(T87, T139)) → U12_gaga(T87, T139, T80, T84, revA_in_ga(.(T80, T139), T84))
U12_gaga(T87, T139, T80, T84, revA_out_ga(.(T80, T139), T84)) → pK_out_gaga(T87, T139, T80, T84)

The argument filtering Pi contains the following mapping:
revA_in_ga(x1, x2) = revA_in_ga(x1)
[] = []
revA_out_ga(x1, x2) = revA_out_ga(x1, x2)
.(x1, x2) = .(x1, x2)
U1_ga(x1, x2, x3, x4, x5, x6) = U1_ga(x1, x2, x3, x6)
pB_in_ggaga(x1, x2, x3, x4, x5) = pB_in_ggaga(x1, x2, x4)
U7_ggaga(x1, x2, x3, x4, x5, x6) = U7_ggaga(x1, x2, x4, x6)
rev1C_in_gga(x1, x2, x3) = rev1C_in_gga(x1, x2)
rev1C_out_gga(x1, x2, x3) = rev1C_out_gga(x1, x2, x3)
U2_gga(x1, x2, x3, x4, x5) = U2_gga(x1, x2, x3, x5)
U8_ggaga(x1, x2, x3, x4, x5, x6) = U8_ggaga(x1, x2, x3, x4, x6)
rev2I_in_ggga(x1, x2, x3, x4) = rev2I_in_ggga(x1, x2, x3)
U6_ggga(x1, x2, x3, x4, x5) = U6_ggga(x1, x2, x3, x5)
pJ_in_ggaaga(x1, x2, x3, x4, x5, x6) = pJ_in_ggaaga(x1, x2, x5)
U9_ggaaga(x1, x2, x3, x4, x5, x6, x7) = U9_ggaaga(x1, x2, x5, x7)
rev2D_in_gga(x1, x2, x3) = rev2D_in_gga(x1, x2)
rev2D_out_gga(x1, x2, x3) = rev2D_out_gga(x1, x2, x3)
U3_gga(x1, x2, x3, x4, x5) = U3_gga(x1, x2, x3, x5)
pE_in_ggaaga(x1, x2, x3, x4, x5, x6) = pE_in_ggaaga(x1, x2, x5)
U13_ggaaga(x1, x2, x3, x4, x5, x6, x7) = U13_ggaaga(x1, x2, x5, x7)
U14_ggaaga(x1, x2, x3, x4, x5, x6, x7) = U14_ggaaga(x1, x2, x3, x5, x7)
pL_in_gaga(x1, x2, x3, x4) = pL_in_gaga(x1, x3)
U15_gaga(x1, x2, x3, x4, x5) = U15_gaga(x1, x3, x5)
revG_in_ga(x1, x2) = revG_in_ga(x1)
revG_out_ga(x1, x2) = revG_out_ga(x1, x2)
U5_ga(x1, x2, x3, x4, x5) = U5_ga(x1, x2, x5)
pH_in_ggaa(x1, x2, x3, x4) = pH_in_ggaa(x1, x2)
U17_ggaa(x1, x2, x3, x4, x5) = U17_ggaa(x1, x2, x5)
rev1F_in_gga(x1, x2, x3) = rev1F_in_gga(x1, x2)
rev1F_out_gga(x1, x2, x3) = rev1F_out_gga(x1, x2, x3)
U4_gga(x1, x2, x3, x4, x5) = U4_gga(x1, x2, x3, x5)
U18_ggaa(x1, x2, x3, x4, x5) = U18_ggaa(x1, x2, x3, x5)
pH_out_ggaa(x1, x2, x3, x4) = pH_out_ggaa(x1, x2, x3, x4)
U16_gaga(x1, x2, x3, x4, x5) = U16_gaga(x1, x2, x3, x5)
pL_out_gaga(x1, x2, x3, x4) = pL_out_gaga(x1, x2, x3, x4)
pE_out_ggaaga(x1, x2, x3, x4, x5, x6) = pE_out_ggaaga(x1, x2, x3, x4, x5, x6)
U10_ggaaga(x1, x2, x3, x4, x5, x6, x7) = U10_ggaaga(x1, x2, x3, x5, x7)
pK_in_gaga(x1, x2, x3, x4) = pK_in_gaga(x1, x3)
U11_gaga(x1, x2, x3, x4, x5) = U11_gaga(x1, x3, x5)
U12_gaga(x1, x2, x3, x4, x5) = U12_gaga(x1, x2, x3, x5)
pK_out_gaga(x1, x2, x3, x4) = pK_out_gaga(x1, x2, x3, x4)
pJ_out_ggaaga(x1, x2, x3, x4, x5, x6) = pJ_out_ggaaga(x1, x2, x3, x4, x5, x6)
rev2I_out_ggga(x1, x2, x3, x4) = rev2I_out_ggga(x1, x2, x3, x4)
pB_out_ggaga(x1, x2, x3, x4, x5) = pB_out_ggaga(x1, x2, x3, x4, x5)
REVA_IN_GA(x1, x2) = REVA_IN_GA(x1)
PB_IN_GGAGA(x1, x2, x3, x4, x5) = PB_IN_GGAGA(x1, x2, x4)
U7_GGAGA(x1, x2, x3, x4, x5, x6) = U7_GGAGA(x1, x2, x4, x6)
REV2I_IN_GGGA(x1, x2, x3, x4) = REV2I_IN_GGGA(x1, x2, x3)
PJ_IN_GGAAGA(x1, x2, x3, x4, x5, x6) = PJ_IN_GGAAGA(x1, x2, x5)
U9_GGAAGA(x1, x2, x3, x4, x5, x6, x7) = U9_GGAAGA(x1, x2, x5, x7)
REV2D_IN_GGA(x1, x2, x3) = REV2D_IN_GGA(x1, x2)
PE_IN_GGAAGA(x1, x2, x3, x4, x5, x6) = PE_IN_GGAAGA(x1, x2, x5)
U13_GGAAGA(x1, x2, x3, x4, x5, x6, x7) = U13_GGAAGA(x1, x2, x5, x7)
PL_IN_GAGA(x1, x2, x3, x4) = PL_IN_GAGA(x1, x3)
U15_GAGA(x1, x2, x3, x4, x5) = U15_GAGA(x1, x3, x5)
REVG_IN_GA(x1, x2) = REVG_IN_GA(x1)
PH_IN_GGAA(x1, x2, x3, x4) = PH_IN_GGAA(x1, x2)
U17_GGAA(x1, x2, x3, x4, x5) = U17_GGAA(x1, x2, x5)
PK_IN_GAGA(x1, x2, x3, x4) = PK_IN_GAGA(x1, x3)
U11_GAGA(x1, x2, x3, x4, x5) = U11_GAGA(x1, x3, x5)

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:

REVA_IN_GA(.(T35, .(T36, T37))) → PB_IN_GGAGA(T36, T37, T35)
PB_IN_GGAGA(T36, T37, T35) → U7_GGAGA(T36, T37, T35, rev1C_in_gga(T36, T37))
U7_GGAGA(T36, T37, T35, rev1C_out_gga(T36, T37, T39)) → REV2I_IN_GGGA(T35, T36, T37)
REV2I_IN_GGGA(T80, T81, T82) → PJ_IN_GGAAGA(T81, T82, T80)
PJ_IN_GGAAGA(T81, T82, T80) → U9_GGAAGA(T81, T82, T80, rev2D_in_gga(T81, T82))
U9_GGAAGA(T81, T82, T80, rev2D_out_gga(T81, T82, T87)) → PK_IN_GAGA(T87, T80)
PK_IN_GAGA(T87, T80) → U11_GAGA(T87, T80, revG_in_ga(T87))
U11_GAGA(T87, T80, revG_out_ga(T87, T139)) → REVA_IN_GA(.(T80, T139))
PK_IN_GAGA(T87, T80) → REVG_IN_GA(T87)
REVG_IN_GA(.(T114, T115)) → PH_IN_GGAA(T114, T115)
PH_IN_GGAA(T114, T115) → U17_GGAA(T114, T115, rev1F_in_gga(T114, T115))
U17_GGAA(T114, T115, rev1F_out_gga(T114, T115, T118)) → REV2D_IN_GGA(T114, T115)
REV2D_IN_GGA(T101, .(T102, T103)) → PE_IN_GGAAGA(T102, T103, T101)
PE_IN_GGAAGA(T102, T103, T101) → U13_GGAAGA(T102, T103, T101, rev2D_in_gga(T102, T103))
U13_GGAAGA(T102, T103, T101, rev2D_out_gga(T102, T103, T106)) → PL_IN_GAGA(T106, T101)
PL_IN_GAGA(T106, T101) → U15_GAGA(T106, T101, revG_in_ga(T106))
U15_GAGA(T106, T101, revG_out_ga(T106, T109)) → REVA_IN_GA(.(T101, T109))
PL_IN_GAGA(T106, T101) → REVG_IN_GA(T106)
PE_IN_GGAAGA(T102, T103, T101) → REV2D_IN_GGA(T102, T103)
PJ_IN_GGAAGA(T81, T82, T80) → REV2D_IN_GGA(T81, T82)

The TRS R consists of the following rules:

rev1C_in_gga(T50, []) → rev1C_out_gga(T50, [], T50)
rev1C_in_gga(T59, .(T60, T61)) → U2_gga(T59, T60, T61, rev1C_in_gga(T60, T61))
rev2D_in_gga(T94, []) → rev2D_out_gga(T94, [], [])
rev2D_in_gga(T101, .(T102, T103)) → U3_gga(T101, T102, T103, pE_in_ggaaga(T102, T103, T101))
revG_in_ga([]) → revG_out_ga([], [])
revG_in_ga(.(T114, T115)) → U5_ga(T114, T115, pH_in_ggaa(T114, T115))
rev1F_in_gga(T125, []) → rev1F_out_gga(T125, [], T125)
rev1F_in_gga(T132, .(T133, T134)) → U4_gga(T132, T133, T134, rev1F_in_gga(T133, T134))
U2_gga(T59, T60, T61, rev1C_out_gga(T60, T61, T63)) → rev1C_out_gga(T59, .(T60, T61), T63)
U3_gga(T101, T102, T103, pE_out_ggaaga(T102, T103, X110, X111, T101, X112)) → rev2D_out_gga(T101, .(T102, T103), X112)
U5_ga(T114, T115, pH_out_ggaa(T114, T115, X133, X134)) → revG_out_ga(.(T114, T115), .(X133, X134))
U4_gga(T132, T133, T134, rev1F_out_gga(T133, T134, X158)) → rev1F_out_gga(T132, .(T133, T134), X158)
pE_in_ggaaga(T102, T103, T101) → U13_ggaaga(T102, T103, T101, rev2D_in_gga(T102, T103))
pH_in_ggaa(T114, T115) → U17_ggaa(T114, T115, rev1F_in_gga(T114, T115))
U13_ggaaga(T102, T103, T101, rev2D_out_gga(T102, T103, T106)) → U14_ggaaga(T102, T103, T106, T101, pL_in_gaga(T106, T101))
U17_ggaa(T114, T115, rev1F_out_gga(T114, T115, T118)) → U18_ggaa(T114, T115, T118, rev2D_in_gga(T114, T115))
U14_ggaaga(T102, T103, T106, T101, pL_out_gaga(T106, X111, T101, X112)) → pE_out_ggaaga(T102, T103, T106, X111, T101, X112)
U18_ggaa(T114, T115, T118, rev2D_out_gga(T114, T115, X134)) → pH_out_ggaa(T114, T115, T118, X134)
pL_in_gaga(T106, T101) → U15_gaga(T106, T101, revG_in_ga(T106))
U15_gaga(T106, T101, revG_out_ga(T106, T109)) → U16_gaga(T106, T109, T101, revA_in_ga(.(T101, T109)))
U16_gaga(T106, T109, T101, revA_out_ga(.(T101, T109), X112)) → pL_out_gaga(T106, T109, T101, X112)
revA_in_ga(.(T25, [])) → revA_out_ga(.(T25, []), .(T25, []))
revA_in_ga(.(T35, .(T36, T37))) → U1_ga(T35, T36, T37, pB_in_ggaga(T36, T37, T35))
U1_ga(T35, T36, T37, pB_out_ggaga(T36, T37, T39, T35, T40)) → revA_out_ga(.(T35, .(T36, T37)), .(T39, T40))
pB_in_ggaga(T36, T37, T35) → U7_ggaga(T36, T37, T35, rev1C_in_gga(T36, T37))
U7_ggaga(T36, T37, T35, rev1C_out_gga(T36, T37, T39)) → U8_ggaga(T36, T37, T39, T35, rev2I_in_ggga(T35, T36, T37))
U8_ggaga(T36, T37, T39, T35, rev2I_out_ggga(T35, T36, T37, T43)) → pB_out_ggaga(T36, T37, T39, T35, T43)
rev2I_in_ggga(T80, T81, T82) → U6_ggga(T80, T81, T82, pJ_in_ggaaga(T81, T82, T80))
U6_ggga(T80, T81, T82, pJ_out_ggaaga(T81, T82, X83, X84, T80, T84)) → rev2I_out_ggga(T80, T81, T82, T84)
pJ_in_ggaaga(T81, T82, T80) → U9_ggaaga(T81, T82, T80, rev2D_in_gga(T81, T82))
U9_ggaaga(T81, T82, T80, rev2D_out_gga(T81, T82, T87)) → U10_ggaaga(T81, T82, T87, T80, pK_in_gaga(T87, T80))
U10_ggaaga(T81, T82, T87, T80, pK_out_gaga(T87, X84, T80, T84)) → pJ_out_ggaaga(T81, T82, T87, X84, T80, T84)
pK_in_gaga(T87, T80) → U11_gaga(T87, T80, revG_in_ga(T87))
U11_gaga(T87, T80, revG_out_ga(T87, T139)) → U12_gaga(T87, T139, T80, revA_in_ga(.(T80, T139)))
U12_gaga(T87, T139, T80, revA_out_ga(.(T80, T139), T84)) → pK_out_gaga(T87, T139, T80, T84)

The set Q consists of the following terms:

rev1C_in_gga(x0, x1)
rev2D_in_gga(x0, x1)
revG_in_ga(x0)
rev1F_in_gga(x0, x1)
U2_gga(x0, x1, x2, x3)
U3_gga(x0, x1, x2, x3)
U5_ga(x0, x1, x2)
U4_gga(x0, x1, x2, x3)
pE_in_ggaaga(x0, x1, x2)
pH_in_ggaa(x0, x1)
U13_ggaaga(x0, x1, x2, x3)
U17_ggaa(x0, x1, x2)
U14_ggaaga(x0, x1, x2, x3, x4)
U18_ggaa(x0, x1, x2, x3)
pL_in_gaga(x0, x1)
U15_gaga(x0, x1, x2)
U16_gaga(x0, x1, x2, x3)
revA_in_ga(x0)
U1_ga(x0, x1, x2, x3)
pB_in_ggaga(x0, x1, x2)
U7_ggaga(x0, x1, x2, x3)
U8_ggaga(x0, x1, x2, x3, x4)
rev2I_in_ggga(x0, x1, x2)
U6_ggga(x0, x1, x2, x3)
pJ_in_ggaaga(x0, x1, x2)
U9_ggaaga(x0, x1, x2, x3)
U10_ggaaga(x0, x1, x2, x3, x4)
pK_in_gaga(x0, x1)
U11_gaga(x0, x1, x2)
U12_gaga(x0, x1, x2, x3)

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

(26) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04,JAR06].

The following pairs can be oriented strictly and are deleted.

REVA_IN_GA(.(T35, .(T36, T37))) → PB_IN_GGAGA(T36, T37, T35)
PK_IN_GAGA(T87, T80) → REVG_IN_GA(T87)
U17_GGAA(T114, T115, rev1F_out_gga(T114, T115, T118)) → REV2D_IN_GGA(T114, T115)
PL_IN_GAGA(T106, T101) → REVG_IN_GA(T106)
PE_IN_GGAAGA(T102, T103, T101) → REV2D_IN_GGA(T102, T103)
PJ_IN_GGAAGA(T81, T82, T80) → REV2D_IN_GGA(T81, T82)

The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial interpretation [POLO]:

POL(.(x₁, x₂)) = 1 + x₂
POL(PB_IN_GGAGA(x₁, x₂, x₃)) = 1 + x₂
POL(PE_IN_GGAAGA(x₁, x₂, x₃)) = 1 + x₂
POL(PH_IN_GGAA(x₁, x₂)) = 1 + x₂
POL(PJ_IN_GGAAGA(x₁, x₂, x₃)) = 1 + x₂
POL(PK_IN_GAGA(x₁, x₂)) = 1 + x₁
POL(PL_IN_GAGA(x₁, x₂)) = 1 + x₁
POL(REV2D_IN_GGA(x₁, x₂)) = x₂
POL(REV2I_IN_GGGA(x₁, x₂, x₃)) = 1 + x₃
POL(REVA_IN_GA(x₁)) = x₁
POL(REVG_IN_GA(x₁)) = x₁
POL(U10_ggaaga(x₁, x₂, x₃, x₄, x₅)) = x₅
POL(U11_GAGA(x₁, x₂, x₃)) = 1 + x₃
POL(U11_gaga(x₁, x₂, x₃)) = 1 + x₃
POL(U12_gaga(x₁, x₂, x₃, x₄)) = x₄
POL(U13_GGAAGA(x₁, x₂, x₃, x₄)) = 1 + x₄
POL(U13_ggaaga(x₁, x₂, x₃, x₄)) = 1 + x₄
POL(U14_ggaaga(x₁, x₂, x₃, x₄, x₅)) = x₅
POL(U15_GAGA(x₁, x₂, x₃)) = 1 + x₃
POL(U15_gaga(x₁, x₂, x₃)) = 1 + x₃
POL(U16_gaga(x₁, x₂, x₃, x₄)) = x₄
POL(U17_GGAA(x₁, x₂, x₃)) = 1 + x₂
POL(U17_ggaa(x₁, x₂, x₃)) = x₂
POL(U18_ggaa(x₁, x₂, x₃, x₄)) = x₄
POL(U1_ga(x₁, x₂, x₃, x₄)) = 1 + x₄
POL(U2_gga(x₁, x₂, x₃, x₄)) = 0
POL(U3_gga(x₁, x₂, x₃, x₄)) = x₄
POL(U4_gga(x₁, x₂, x₃, x₄)) = 0
POL(U5_ga(x₁, x₂, x₃)) = 1 + x₃
POL(U6_ggga(x₁, x₂, x₃, x₄)) = x₄
POL(U7_GGAGA(x₁, x₂, x₃, x₄)) = 1 + x₂
POL(U7_ggaga(x₁, x₂, x₃, x₄)) = 1 + x₂
POL(U8_ggaga(x₁, x₂, x₃, x₄, x₅)) = x₅
POL(U9_GGAAGA(x₁, x₂, x₃, x₄)) = 1 + x₄
POL(U9_ggaaga(x₁, x₂, x₃, x₄)) = 1 + x₄
POL([]) = 0
POL(pB_in_ggaga(x₁, x₂, x₃)) = 1 + x₂
POL(pB_out_ggaga(x₁, x₂, x₃, x₄, x₅)) = x₅
POL(pE_in_ggaaga(x₁, x₂, x₃)) = 1 + x₂
POL(pE_out_ggaaga(x₁, x₂, x₃, x₄, x₅, x₆)) = x₆
POL(pH_in_ggaa(x₁, x₂)) = x₂
POL(pH_out_ggaa(x₁, x₂, x₃, x₄)) = x₄
POL(pJ_in_ggaaga(x₁, x₂, x₃)) = 1 + x₂
POL(pJ_out_ggaaga(x₁, x₂, x₃, x₄, x₅, x₆)) = x₆
POL(pK_in_gaga(x₁, x₂)) = 1 + x₁
POL(pK_out_gaga(x₁, x₂, x₃, x₄)) = x₄
POL(pL_in_gaga(x₁, x₂)) = 1 + x₁
POL(pL_out_gaga(x₁, x₂, x₃, x₄)) = x₄
POL(rev1C_in_gga(x₁, x₂)) = 0
POL(rev1C_out_gga(x₁, x₂, x₃)) = 0
POL(rev1F_in_gga(x₁, x₂)) = 0
POL(rev1F_out_gga(x₁, x₂, x₃)) = 0
POL(rev2D_in_gga(x₁, x₂)) = x₂
POL(rev2D_out_gga(x₁, x₂, x₃)) = x₃
POL(rev2I_in_ggga(x₁, x₂, x₃)) = 1 + x₃
POL(rev2I_out_ggga(x₁, x₂, x₃, x₄)) = x₄
POL(revA_in_ga(x₁)) = x₁
POL(revA_out_ga(x₁, x₂)) = x₂
POL(revG_in_ga(x₁)) = x₁
POL(revG_out_ga(x₁, x₂)) = x₂

The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:

rev2D_in_gga(T94, []) → rev2D_out_gga(T94, [], [])
rev2D_in_gga(T101, .(T102, T103)) → U3_gga(T101, T102, T103, pE_in_ggaaga(T102, T103, T101))
revG_in_ga([]) → revG_out_ga([], [])
revG_in_ga(.(T114, T115)) → U5_ga(T114, T115, pH_in_ggaa(T114, T115))
U7_ggaga(T36, T37, T35, rev1C_out_gga(T36, T37, T39)) → U8_ggaga(T36, T37, T39, T35, rev2I_in_ggga(T35, T36, T37))
U8_ggaga(T36, T37, T39, T35, rev2I_out_ggga(T35, T36, T37, T43)) → pB_out_ggaga(T36, T37, T39, T35, T43)
rev2I_in_ggga(T80, T81, T82) → U6_ggga(T80, T81, T82, pJ_in_ggaaga(T81, T82, T80))
U6_ggga(T80, T81, T82, pJ_out_ggaaga(T81, T82, X83, X84, T80, T84)) → rev2I_out_ggga(T80, T81, T82, T84)
pJ_in_ggaaga(T81, T82, T80) → U9_ggaaga(T81, T82, T80, rev2D_in_gga(T81, T82))
U3_gga(T101, T102, T103, pE_out_ggaaga(T102, T103, X110, X111, T101, X112)) → rev2D_out_gga(T101, .(T102, T103), X112)
pE_in_ggaaga(T102, T103, T101) → U13_ggaaga(T102, T103, T101, rev2D_in_gga(T102, T103))
U13_ggaaga(T102, T103, T101, rev2D_out_gga(T102, T103, T106)) → U14_ggaaga(T102, T103, T106, T101, pL_in_gaga(T106, T101))
U14_ggaaga(T102, T103, T106, T101, pL_out_gaga(T106, X111, T101, X112)) → pE_out_ggaaga(T102, T103, T106, X111, T101, X112)
pL_in_gaga(T106, T101) → U15_gaga(T106, T101, revG_in_ga(T106))
U5_ga(T114, T115, pH_out_ggaa(T114, T115, X133, X134)) → revG_out_ga(.(T114, T115), .(X133, X134))
pH_in_ggaa(T114, T115) → U17_ggaa(T114, T115, rev1F_in_gga(T114, T115))
U17_ggaa(T114, T115, rev1F_out_gga(T114, T115, T118)) → U18_ggaa(T114, T115, T118, rev2D_in_gga(T114, T115))
U18_ggaa(T114, T115, T118, rev2D_out_gga(T114, T115, X134)) → pH_out_ggaa(T114, T115, T118, X134)
U15_gaga(T106, T101, revG_out_ga(T106, T109)) → U16_gaga(T106, T109, T101, revA_in_ga(.(T101, T109)))
revA_in_ga(.(T25, [])) → revA_out_ga(.(T25, []), .(T25, []))
U16_gaga(T106, T109, T101, revA_out_ga(.(T101, T109), X112)) → pL_out_gaga(T106, T109, T101, X112)
revA_in_ga(.(T35, .(T36, T37))) → U1_ga(T35, T36, T37, pB_in_ggaga(T36, T37, T35))
U1_ga(T35, T36, T37, pB_out_ggaga(T36, T37, T39, T35, T40)) → revA_out_ga(.(T35, .(T36, T37)), .(T39, T40))
pB_in_ggaga(T36, T37, T35) → U7_ggaga(T36, T37, T35, rev1C_in_gga(T36, T37))
U9_ggaaga(T81, T82, T80, rev2D_out_gga(T81, T82, T87)) → U10_ggaaga(T81, T82, T87, T80, pK_in_gaga(T87, T80))
U10_ggaaga(T81, T82, T87, T80, pK_out_gaga(T87, X84, T80, T84)) → pJ_out_ggaaga(T81, T82, T87, X84, T80, T84)
pK_in_gaga(T87, T80) → U11_gaga(T87, T80, revG_in_ga(T87))
U11_gaga(T87, T80, revG_out_ga(T87, T139)) → U12_gaga(T87, T139, T80, revA_in_ga(.(T80, T139)))
U12_gaga(T87, T139, T80, revA_out_ga(.(T80, T139), T84)) → pK_out_gaga(T87, T139, T80, T84)

(27) Obligation:

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

PB_IN_GGAGA(T36, T37, T35) → U7_GGAGA(T36, T37, T35, rev1C_in_gga(T36, T37))
U7_GGAGA(T36, T37, T35, rev1C_out_gga(T36, T37, T39)) → REV2I_IN_GGGA(T35, T36, T37)
REV2I_IN_GGGA(T80, T81, T82) → PJ_IN_GGAAGA(T81, T82, T80)
PJ_IN_GGAAGA(T81, T82, T80) → U9_GGAAGA(T81, T82, T80, rev2D_in_gga(T81, T82))
U9_GGAAGA(T81, T82, T80, rev2D_out_gga(T81, T82, T87)) → PK_IN_GAGA(T87, T80)
PK_IN_GAGA(T87, T80) → U11_GAGA(T87, T80, revG_in_ga(T87))
U11_GAGA(T87, T80, revG_out_ga(T87, T139)) → REVA_IN_GA(.(T80, T139))
REVG_IN_GA(.(T114, T115)) → PH_IN_GGAA(T114, T115)
PH_IN_GGAA(T114, T115) → U17_GGAA(T114, T115, rev1F_in_gga(T114, T115))
REV2D_IN_GGA(T101, .(T102, T103)) → PE_IN_GGAAGA(T102, T103, T101)
PE_IN_GGAAGA(T102, T103, T101) → U13_GGAAGA(T102, T103, T101, rev2D_in_gga(T102, T103))
U13_GGAAGA(T102, T103, T101, rev2D_out_gga(T102, T103, T106)) → PL_IN_GAGA(T106, T101)
PL_IN_GAGA(T106, T101) → U15_GAGA(T106, T101, revG_in_ga(T106))
U15_GAGA(T106, T101, revG_out_ga(T106, T109)) → REVA_IN_GA(.(T101, T109))

The TRS R consists of the following rules:

rev1C_in_gga(T50, []) → rev1C_out_gga(T50, [], T50)
rev1C_in_gga(T59, .(T60, T61)) → U2_gga(T59, T60, T61, rev1C_in_gga(T60, T61))
rev2D_in_gga(T94, []) → rev2D_out_gga(T94, [], [])
rev2D_in_gga(T101, .(T102, T103)) → U3_gga(T101, T102, T103, pE_in_ggaaga(T102, T103, T101))
revG_in_ga([]) → revG_out_ga([], [])
revG_in_ga(.(T114, T115)) → U5_ga(T114, T115, pH_in_ggaa(T114, T115))
rev1F_in_gga(T125, []) → rev1F_out_gga(T125, [], T125)
rev1F_in_gga(T132, .(T133, T134)) → U4_gga(T132, T133, T134, rev1F_in_gga(T133, T134))
U2_gga(T59, T60, T61, rev1C_out_gga(T60, T61, T63)) → rev1C_out_gga(T59, .(T60, T61), T63)
U3_gga(T101, T102, T103, pE_out_ggaaga(T102, T103, X110, X111, T101, X112)) → rev2D_out_gga(T101, .(T102, T103), X112)
U5_ga(T114, T115, pH_out_ggaa(T114, T115, X133, X134)) → revG_out_ga(.(T114, T115), .(X133, X134))
U4_gga(T132, T133, T134, rev1F_out_gga(T133, T134, X158)) → rev1F_out_gga(T132, .(T133, T134), X158)
pE_in_ggaaga(T102, T103, T101) → U13_ggaaga(T102, T103, T101, rev2D_in_gga(T102, T103))
pH_in_ggaa(T114, T115) → U17_ggaa(T114, T115, rev1F_in_gga(T114, T115))
U13_ggaaga(T102, T103, T101, rev2D_out_gga(T102, T103, T106)) → U14_ggaaga(T102, T103, T106, T101, pL_in_gaga(T106, T101))
U17_ggaa(T114, T115, rev1F_out_gga(T114, T115, T118)) → U18_ggaa(T114, T115, T118, rev2D_in_gga(T114, T115))
U14_ggaaga(T102, T103, T106, T101, pL_out_gaga(T106, X111, T101, X112)) → pE_out_ggaaga(T102, T103, T106, X111, T101, X112)
U18_ggaa(T114, T115, T118, rev2D_out_gga(T114, T115, X134)) → pH_out_ggaa(T114, T115, T118, X134)
pL_in_gaga(T106, T101) → U15_gaga(T106, T101, revG_in_ga(T106))
U15_gaga(T106, T101, revG_out_ga(T106, T109)) → U16_gaga(T106, T109, T101, revA_in_ga(.(T101, T109)))
U16_gaga(T106, T109, T101, revA_out_ga(.(T101, T109), X112)) → pL_out_gaga(T106, T109, T101, X112)
revA_in_ga(.(T25, [])) → revA_out_ga(.(T25, []), .(T25, []))
revA_in_ga(.(T35, .(T36, T37))) → U1_ga(T35, T36, T37, pB_in_ggaga(T36, T37, T35))
U1_ga(T35, T36, T37, pB_out_ggaga(T36, T37, T39, T35, T40)) → revA_out_ga(.(T35, .(T36, T37)), .(T39, T40))
pB_in_ggaga(T36, T37, T35) → U7_ggaga(T36, T37, T35, rev1C_in_gga(T36, T37))
U7_ggaga(T36, T37, T35, rev1C_out_gga(T36, T37, T39)) → U8_ggaga(T36, T37, T39, T35, rev2I_in_ggga(T35, T36, T37))
U8_ggaga(T36, T37, T39, T35, rev2I_out_ggga(T35, T36, T37, T43)) → pB_out_ggaga(T36, T37, T39, T35, T43)
rev2I_in_ggga(T80, T81, T82) → U6_ggga(T80, T81, T82, pJ_in_ggaaga(T81, T82, T80))
U6_ggga(T80, T81, T82, pJ_out_ggaaga(T81, T82, X83, X84, T80, T84)) → rev2I_out_ggga(T80, T81, T82, T84)
pJ_in_ggaaga(T81, T82, T80) → U9_ggaaga(T81, T82, T80, rev2D_in_gga(T81, T82))
U9_ggaaga(T81, T82, T80, rev2D_out_gga(T81, T82, T87)) → U10_ggaaga(T81, T82, T87, T80, pK_in_gaga(T87, T80))
U10_ggaaga(T81, T82, T87, T80, pK_out_gaga(T87, X84, T80, T84)) → pJ_out_ggaaga(T81, T82, T87, X84, T80, T84)
pK_in_gaga(T87, T80) → U11_gaga(T87, T80, revG_in_ga(T87))
U11_gaga(T87, T80, revG_out_ga(T87, T139)) → U12_gaga(T87, T139, T80, revA_in_ga(.(T80, T139)))
U12_gaga(T87, T139, T80, revA_out_ga(.(T80, T139), T84)) → pK_out_gaga(T87, T139, T80, T84)

The set Q consists of the following terms:

rev1C_in_gga(x0, x1)
rev2D_in_gga(x0, x1)
revG_in_ga(x0)
rev1F_in_gga(x0, x1)
U2_gga(x0, x1, x2, x3)
U3_gga(x0, x1, x2, x3)
U5_ga(x0, x1, x2)
U4_gga(x0, x1, x2, x3)
pE_in_ggaaga(x0, x1, x2)
pH_in_ggaa(x0, x1)
U13_ggaaga(x0, x1, x2, x3)
U17_ggaa(x0, x1, x2)
U14_ggaaga(x0, x1, x2, x3, x4)
U18_ggaa(x0, x1, x2, x3)
pL_in_gaga(x0, x1)
U15_gaga(x0, x1, x2)
U16_gaga(x0, x1, x2, x3)
revA_in_ga(x0)
U1_ga(x0, x1, x2, x3)
pB_in_ggaga(x0, x1, x2)
U7_ggaga(x0, x1, x2, x3)
U8_ggaga(x0, x1, x2, x3, x4)
rev2I_in_ggga(x0, x1, x2)
U6_ggga(x0, x1, x2, x3)
pJ_in_ggaaga(x0, x1, x2)
U9_ggaaga(x0, x1, x2, x3)
U10_ggaaga(x0, x1, x2, x3, x4)
pK_in_gaga(x0, x1)
U11_gaga(x0, x1, x2)
U12_gaga(x0, x1, x2, x3)

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

(28) DependencyGraphProof (EQUIVALENT transformation)

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

(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

(21) Obligation:

(22) UsableRulesProof (EQUIVALENT transformation)

(23) Obligation:

(24) PiDPToQDPProof (SOUND transformation)

(25) Obligation:

(26) QDPOrderProof (EQUIVALENT transformation)

(27) Obligation:

(28) DependencyGraphProof (EQUIVALENT transformation)

(29) TRUE