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

(0) Obligation:

Clauses:

m(X, 0, Z) :- ','(!, =(Z, X)).
m(0, Y, Z) :- ','(!, =(Z, 0)).
m(X, Y, Z) :- ','(p(X, A), ','(p(Y, B), m(A, B, Z))).
p(0, 0).
p(s(0), 0).
p(s(s(X)), s(Y)) :- p(s(X), Y).
=(X, X).

Query: m(g,g,a)

(1) BuiltinConflictTransformerProof (EQUIVALENT transformation)

Renamed defined predicates conflicting with built-in predicates [PROLOG].

(2) Obligation:

Clauses:

m(X, 0, Z) :- ','(!, user_defined_=(Z, X)).
m(0, Y, Z) :- ','(!, user_defined_=(Z, 0)).
m(X, Y, Z) :- ','(p(X, A), ','(p(Y, B), m(A, B, Z))).
p(0, 0).
p(s(0), 0).
p(s(s(X)), s(Y)) :- p(s(X), Y).
user_defined_=(X, X).

Query: m(g,g,a)

(3) PrologToPiTRSViaGraphTransformerProof (SOUND transformation)

Transformed Prolog program to (Pi-)TRS.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
2 [label="A: m(T1, T2, T3)\n\nT1 is ground\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
6 [label="6: m(T1, T2, T3), SCOPE: 1, CLAUSE: 0 | m(T1, T2, T3), SCOPE: 1, CLAUSE: 1 | m(T1, T2, T3), SCOPE: 1, CLAUSE: 2\n\nT1 is ground\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
9 [label="9: ','(!_1, user_defined_=(T8, T6)) | m(T6, 0, T3), SCOPE: 1, CLAUSE: 1 | m(T6, 0, T3), SCOPE: 1, CLAUSE: 2\n\nT6 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
11 [label="11: m(T1, T2, T3), SCOPE: 1, CLAUSE: 1 | m(T1, T2, T3), SCOPE: 1, CLAUSE: 2\n\nT1 is ground\nT2 is ground\nX3 is free\nX4 is free\nm(T1, T2, T3) !=? m(X3, 0, X4)", fontsize=16, style=filled, fillcolor=lightyellow];
14 [label="14: user_defined_=(T8, T6)\n\nT6 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
17 [label="17: user_defined_=(T8, T6), SCOPE: 2, CLAUSE: 6\n\nT6 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
20 [label="20: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
24 [label="24: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
25 [label="25: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
28 [label="28: ','(!_1, user_defined_=(T16, 0)) | m(0, T14, T3), SCOPE: 1, CLAUSE: 2\n\nT14 is ground\nX3 is free\nX4 is free\nm(0, T14, T3) !=? m(X3, 0, X4)", fontsize=16, style=filled, fillcolor=lightyellow];
32 [label="32: m(T1, T2, T3), SCOPE: 1, CLAUSE: 2\n\nT1 is ground\nT2 is ground\nX3 is free\nX4 is free\nX10 is free\nX11 is free\nm(T1, T2, T3) !=? m(X3, 0, X4)\nm(T1, T2, T3) !=? m(0, X10, X11)", fontsize=16, style=filled, fillcolor=lightyellow];
34 [label="34: user_defined_=(T16, 0)\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
36 [label="36: user_defined_=(T16, 0), SCOPE: 3, CLAUSE: 6\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
41 [label="41: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
44 [label="44: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
45 [label="45: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
50 [label="50: ','(p(T23, X21), ','(p(T24, X22), m(X21, X22, T26)))\n\nT23 is ground\nT24 is ground\nX3 is free\nX4 is free\nX10 is free\nX11 is free\nX21 is free\nX22 is free\nm(T23, T24, T3) !=? m(X3, 0, X4)\nm(T23, T24, T3) !=? m(0, X10, X11)", fontsize=16, style=filled, fillcolor=lightyellow];
52 [label="52: ','(p(T23, X21), ','(p(T24, X22), m(X21, X22, T26))), SCOPE: 4, CLAUSE: 3 | ','(p(T23, X21), ','(p(T24, X22), m(X21, X22, T26))), SCOPE: 4, CLAUSE: 4 | ','(p(T23, X21), ','(p(T24, X22), m(X21, X22, T26))), SCOPE: 4, CLAUSE: 5\n\nT23 is ground\nT24 is ground\nX3 is free\nX4 is free\nX10 is free\nX11 is free\nX21 is free\nX22 is free\nm(T23, T24, T3) !=? m(X3, 0, X4)\nm(T23, T24, T3) !=? m(0, X10, X11)", fontsize=16, style=filled, fillcolor=lightyellow];
54 [label="54: ','(p(T23, X21), ','(p(T24, X22), m(X21, X22, T26))), SCOPE: 4, CLAUSE: 4 | ','(p(T23, X21), ','(p(T24, X22), m(X21, X22, T26))), SCOPE: 4, CLAUSE: 5\n\nT23 is ground\nT24 is ground\nX3 is free\nX4 is free\nX10 is free\nX11 is free\nX21 is free\nX22 is free\nm(T23, T24, T3) !=? m(X3, 0, X4)\nm(T23, T24, T3) !=? m(0, X10, X11)", fontsize=16, style=filled, fillcolor=lightyellow];
56 [label="56: ','(p(T23, X21), ','(p(T24, X22), m(X21, X22, T26))), SCOPE: 4, CLAUSE: 4\n\nT23 is ground\nT24 is ground\nX3 is free\nX4 is free\nX10 is free\nX11 is free\nX21 is free\nX22 is free\nm(T23, T24, T3) !=? m(X3, 0, X4)\nm(T23, T24, T3) !=? m(0, X10, X11)", fontsize=16, style=filled, fillcolor=lightyellow];
58 [label="58: ','(p(T23, X21), ','(p(T24, X22), m(X21, X22, T26))), SCOPE: 4, CLAUSE: 5\n\nT23 is ground\nT24 is ground\nX3 is free\nX4 is free\nX10 is free\nX11 is free\nX21 is free\nX22 is free\nm(T23, T24, T3) !=? m(X3, 0, X4)\nm(T23, T24, T3) !=? m(0, X10, X11)", fontsize=16, style=filled, fillcolor=lightyellow];
61 [label="B: ','(p(T24, X22), m(0, X22, T26))\n\nT24 is ground\nX3 is free\nX4 is free\nX22 is free\nm(s(0), T24, T3) !=? m(X3, 0, X4)", fontsize=16, style=filled, fillcolor=lightyellow];
63 [label="63: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
65 [label="E: p(T24, X22)\n\nT24 is ground\nX3 is free\nX4 is free\nX22 is free\nm(s(0), T24, T3) !=? m(X3, 0, X4)", fontsize=16, style=filled, fillcolor=lightyellow];
66 [label="F: m(0, T27, T26)\n\nT27 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
71 [label="71: p(T24, X22), SCOPE: 5, CLAUSE: 3 | p(T24, X22), SCOPE: 5, CLAUSE: 4 | p(T24, X22), SCOPE: 5, CLAUSE: 5\n\nT24 is ground\nX3 is free\nX4 is free\nX22 is free\nm(s(0), T24, T3) !=? m(X3, 0, X4)", fontsize=16, style=filled, fillcolor=lightyellow];
74 [label="74: p(T24, X22), SCOPE: 5, CLAUSE: 4 | p(T24, X22), SCOPE: 5, CLAUSE: 5\n\nT24 is ground\nX3 is free\nX4 is free\nX22 is free\nm(s(0), T24, T3) !=? m(X3, 0, X4)", fontsize=16, style=filled, fillcolor=lightyellow];
77 [label="77: p(T24, X22), SCOPE: 5, CLAUSE: 4\n\nT24 is ground\nX3 is free\nX4 is free\nX22 is free\nm(s(0), T24, T3) !=? m(X3, 0, X4)", fontsize=16, style=filled, fillcolor=lightyellow];
79 [label="79: p(T24, X22), SCOPE: 5, CLAUSE: 5\n\nT24 is ground\nX3 is free\nX4 is free\nX22 is free\nm(s(0), T24, T3) !=? m(X3, 0, X4)", fontsize=16, style=filled, fillcolor=lightyellow];
82 [label="82: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
84 [label="84: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
85 [label="85: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
90 [label="D: p(s(T30), X31)\n\nT30 is ground\nX31 is free", fontsize=16, style=filled, fillcolor=lightyellow];
92 [label="92: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
99 [label="99: p(s(T30), X31), SCOPE: 6, CLAUSE: 3 | p(s(T30), X31), SCOPE: 6, CLAUSE: 4 | p(s(T30), X31), SCOPE: 6, CLAUSE: 5\n\nT30 is ground\nX31 is free", fontsize=16, style=filled, fillcolor=lightyellow];
100 [label="100: p(s(T30), X31), SCOPE: 6, CLAUSE: 4 | p(s(T30), X31), SCOPE: 6, CLAUSE: 5\n\nT30 is ground\nX31 is free", fontsize=16, style=filled, fillcolor=lightyellow];
102 [label="102: p(s(T30), X31), SCOPE: 6, CLAUSE: 4\n\nT30 is ground\nX31 is free", fontsize=16, style=filled, fillcolor=lightyellow];
103 [label="103: p(s(T30), X31), SCOPE: 6, CLAUSE: 5\n\nT30 is ground\nX31 is free", fontsize=16, style=filled, fillcolor=lightyellow];
106 [label="106: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
107 [label="107: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
108 [label="108: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
111 [label="111: p(s(T33), X40)\n\nT33 is ground\nX40 is free", fontsize=16, style=filled, fillcolor=lightyellow];
112 [label="112: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
113 [label="113: m(0, T27, T26), SCOPE: 7, CLAUSE: 0 | m(0, T27, T26), SCOPE: 7, CLAUSE: 1 | m(0, T27, T26), SCOPE: 7, CLAUSE: 2\n\nT27 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
117 [label="117: ','(!_7, user_defined_=(T38, 0)) | m(0, 0, T26), SCOPE: 7, CLAUSE: 1 | m(0, 0, T26), SCOPE: 7, CLAUSE: 2\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
120 [label="120: m(0, T27, T26), SCOPE: 7, CLAUSE: 1 | m(0, T27, T26), SCOPE: 7, CLAUSE: 2\n\nT27 is ground\nX47 is free\nX48 is free\nm(0, T27, T26) !=? m(X47, 0, X48)", fontsize=16, style=filled, fillcolor=lightyellow];
122 [label="122: user_defined_=(T38, 0)\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
124 [label="124: user_defined_=(T38, 0), SCOPE: 8, CLAUSE: 6\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
129 [label="129: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
131 [label="131: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
132 [label="132: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
141 [label="141: ','(!_7, user_defined_=(T49, 0)) | m(0, T47, T26), SCOPE: 7, CLAUSE: 2\n\nT47 is ground\nX47 is free\nX48 is free\nm(0, T47, T26) !=? m(X47, 0, X48)", fontsize=16, style=filled, fillcolor=lightyellow];
142 [label="142: user_defined_=(T49, 0)\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
143 [label="143: user_defined_=(T49, 0), SCOPE: 9, CLAUSE: 6\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
149 [label="149: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
150 [label="150: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
151 [label="151: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
161 [label="C: ','(p(s(T55), X69), ','(p(T24, X22), m(s(X69), X22, T26)))\n\nT24 is ground\nT55 is ground\nX3 is free\nX4 is free\nX22 is free\nX69 is free\nm(s(s(T55)), T24, T3) !=? m(X3, 0, X4)", fontsize=16, style=filled, fillcolor=lightyellow];
162 [label="162: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
167 [label="167: p(s(T55), X69)\n\nT24 is ground\nT55 is ground\nX3 is free\nX4 is free\nX69 is free\nm(s(s(T55)), T24, T3) !=? m(X3, 0, X4)", fontsize=16, style=filled, fillcolor=lightyellow];
169 [label="H: ','(p(T24, X22), m(s(T56), X22, T26))\n\nT24 is ground\nT55 is ground\nT56 is ground\nX3 is free\nX4 is free\nX22 is free\nm(s(s(T55)), T24, T3) !=? m(X3, 0, X4)", fontsize=16, style=filled, fillcolor=lightyellow];
178 [label="G: p(T24, X22)\n\nT24 is ground\nT55 is ground\nX3 is free\nX4 is free\nX22 is free\nm(s(s(T55)), T24, T3) !=? m(X3, 0, X4)", fontsize=16, style=filled, fillcolor=lightyellow];
180 [label="180: m(s(T56), T57, T26)\n\nT56 is ground\nT57 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
185 [label="185: p(T24, X22), SCOPE: 10, CLAUSE: 3 | p(T24, X22), SCOPE: 10, CLAUSE: 4 | p(T24, X22), SCOPE: 10, CLAUSE: 5\n\nT24 is ground\nT55 is ground\nX3 is free\nX4 is free\nX22 is free\nm(s(s(T55)), T24, T3) !=? m(X3, 0, X4)", fontsize=16, style=filled, fillcolor=lightyellow];
190 [label="190: p(T24, X22), SCOPE: 10, CLAUSE: 4 | p(T24, X22), SCOPE: 10, CLAUSE: 5\n\nT24 is ground\nT55 is ground\nX3 is free\nX4 is free\nX22 is free\nm(s(s(T55)), T24, T3) !=? m(X3, 0, X4)", fontsize=16, style=filled, fillcolor=lightyellow];
191 [label="191: p(T24, X22), SCOPE: 10, CLAUSE: 4\n\nT24 is ground\nT55 is ground\nX3 is free\nX4 is free\nX22 is free\nm(s(s(T55)), T24, T3) !=? m(X3, 0, X4)", fontsize=16, style=filled, fillcolor=lightyellow];
192 [label="192: p(T24, X22), SCOPE: 10, CLAUSE: 5\n\nT24 is ground\nT55 is ground\nX3 is free\nX4 is free\nX22 is free\nm(s(s(T55)), T24, T3) !=? m(X3, 0, X4)", 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];
205 [label="205: p(s(T60), X78)\n\nT60 is ground\nX78 is free", fontsize=16, style=filled, fillcolor=lightyellow];
206 [label="206: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
207 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
2 -> 207 [arrowhead = none ];
207 -> 6;

208 [label="EVAL with clause\nm(X3, 0, X4) :- ','(!_1, user_defined_=(X4, X3)).\nand substitutionT1 -> T6,\nX3 -> T6,\nT2 -> 0,\nT3 -> T8,\nX4 -> T8,\nT7 -> T8", fontsize=14, style = filled, fillcolor = lightblue];
6 -> 208 [arrowhead = none ];
208 -> 9;

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

210 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
9 -> 210 [arrowhead = none ];
210 -> 14;

211 [label="EVAL with clause\nm(0, X10, X11) :- ','(!_1, user_defined_=(X11, 0)).\nand substitutionT1 -> 0,\nT2 -> T14,\nX10 -> T14,\nT3 -> T16,\nX11 -> T16,\nT15 -> T16", fontsize=14, style = filled, fillcolor = lightblue];
11 -> 211 [arrowhead = none ];
211 -> 28;

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

213 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
14 -> 213 [arrowhead = none ];
213 -> 17;

214 [label="EVAL with clause\nuser_defined_=(X7, X7).\nand substitutionT8 -> T11,\nX7 -> T11,\nT6 -> T11", fontsize=14, style = filled, fillcolor = lightblue];
17 -> 214 [arrowhead = none ];
214 -> 20;

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

216 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
20 -> 216 [arrowhead = none ];
216 -> 25;

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

218 [label="ONLY EVAL with clause\nm(X18, X19, X20) :- ','(p(X18, X21), ','(p(X19, X22), m(X21, X22, X20))).\nand substitutionT1 -> T23,\nX18 -> T23,\nT2 -> T24,\nX19 -> T24,\nT3 -> T26,\nX20 -> T26,\nT25 -> T26", fontsize=14, style = filled, fillcolor = lightblue];
32 -> 218 [arrowhead = none ];
218 -> 50;

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

220 [label="EVAL with clause\nuser_defined_=(X14, X14).\nand substitutionT16 -> 0,\nX14 -> 0,\nT19 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
36 -> 220 [arrowhead = none ];
220 -> 41;

221 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
36 -> 221 [arrowhead = none ];
221 -> 44;

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

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

224 [label="BACKTRACK\nfor clause: p(0, 0)\nwith clash: (m(T23, T24, T3), m(0, X10, X11))", fontsize=14, style = filled, fillcolor = lightgreen];
52 -> 224 [arrowhead = none ];
224 -> 54;

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

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

227 [label="EVAL with clause\np(s(0), 0).\nand substitutionT23 -> s(0),\nX21 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
56 -> 227 [arrowhead = none ];
227 -> 61;

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

229 [label="EVAL with clause\np(s(s(X67)), s(X68)) :- p(s(X67), X68).\nand substitutionX67 -> T55,\nT23 -> s(s(T55)),\nX68 -> X69,\nX21 -> s(X69)", fontsize=14, style = filled, fillcolor = lightblue];
58 -> 229 [arrowhead = none ];
229 -> 161;

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

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

232 [label="SPLIT 2\nnew knowledge:\nT24 is ground\nT27 is ground\nreplacements:X22 -> T27", fontsize=14, style = filled, fillcolor = violet];
61 -> 232 [arrowhead = none ];
232 -> 66;

233 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
65 -> 233 [arrowhead = none ];
233 -> 71;

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

235 [label="BACKTRACK\nfor clause: p(0, 0)\nwith clash: (m(s(0), T24, T3), m(X3, 0, X4))", fontsize=14, style = filled, fillcolor = lightgreen];
71 -> 235 [arrowhead = none ];
235 -> 74;

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

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

238 [label="EVAL with clause\np(s(0), 0).\nand substitutionT24 -> s(0),\nX22 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
77 -> 238 [arrowhead = none ];
238 -> 82;

239 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
77 -> 239 [arrowhead = none ];
239 -> 84;

240 [label="EVAL with clause\np(s(s(X29)), s(X30)) :- p(s(X29), X30).\nand substitutionX29 -> T30,\nT24 -> s(s(T30)),\nX30 -> X31,\nX22 -> s(X31)", fontsize=14, style = filled, fillcolor = lightblue];
79 -> 240 [arrowhead = none ];
240 -> 90;

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

242 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
82 -> 242 [arrowhead = none ];
242 -> 85;

243 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
90 -> 243 [arrowhead = none ];
243 -> 99;

244 [label="BACKTRACK\nfor clause: p(0, 0)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
99 -> 244 [arrowhead = none ];
244 -> 100;

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

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

247 [label="EVAL with clause\np(s(0), 0).\nand substitutionT30 -> 0,\nX31 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
102 -> 247 [arrowhead = none ];
247 -> 106;

248 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
102 -> 248 [arrowhead = none ];
248 -> 107;

249 [label="EVAL with clause\np(s(s(X38)), s(X39)) :- p(s(X38), X39).\nand substitutionX38 -> T33,\nT30 -> s(T33),\nX39 -> X40,\nX31 -> s(X40)", fontsize=14, style = filled, fillcolor = lightblue];
103 -> 249 [arrowhead = none ];
249 -> 111;

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

251 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
106 -> 251 [arrowhead = none ];
251 -> 108;

252 [label="INSTANCE with matching:\nT30 -> T33\nX31 -> X40", fontsize=14, style = filled, fillcolor = lightgrey];
111 -> 252 [arrowhead = none , style=dashed];
252 -> 90[style=dashed];

253 [label="EVAL with clause\nm(X47, 0, X48) :- ','(!_7, user_defined_=(X48, X47)).\nand substitutionX47 -> 0,\nT27 -> 0,\nT26 -> T38,\nX48 -> T38,\nT37 -> T38", fontsize=14, style = filled, fillcolor = lightblue];
113 -> 253 [arrowhead = none ];
253 -> 117;

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

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

256 [label="ONLY EVAL with clause\nm(0, X56, X57) :- ','(!_7, user_defined_=(X57, 0)).\nand substitutionT27 -> T47,\nX56 -> T47,\nT26 -> T49,\nX57 -> T49,\nT48 -> T49", fontsize=14, style = filled, fillcolor = lightblue];
120 -> 256 [arrowhead = none ];
256 -> 141;

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

258 [label="EVAL with clause\nuser_defined_=(X51, X51).\nand substitutionT38 -> 0,\nX51 -> 0,\nT41 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
124 -> 258 [arrowhead = none ];
258 -> 129;

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

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

261 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
141 -> 261 [arrowhead = none ];
261 -> 142;

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

263 [label="EVAL with clause\nuser_defined_=(X60, X60).\nand substitutionT49 -> 0,\nX60 -> 0,\nT52 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
143 -> 263 [arrowhead = none ];
263 -> 149;

264 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
143 -> 264 [arrowhead = none ];
264 -> 150;

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

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

267 [label="SPLIT 2\nnew knowledge:\nT55 is ground\nT56 is ground\nreplacements:X69 -> T56", fontsize=14, style = filled, fillcolor = violet];
161 -> 267 [arrowhead = none ];
267 -> 169;

268 [label="INSTANCE with matching:\nT30 -> T55\nX31 -> X69", fontsize=14, style = filled, fillcolor = lightgrey];
167 -> 268 [arrowhead = none , style=dashed];
268 -> 90[style=dashed];

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

270 [label="SPLIT 2\nnew knowledge:\nT24 is ground\nT57 is ground\nreplacements:X22 -> T57", fontsize=14, style = filled, fillcolor = violet];
169 -> 270 [arrowhead = none ];
270 -> 180;

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

272 [label="INSTANCE with matching:\nT1 -> s(T56)\nT2 -> T57\nT3 -> T26", fontsize=14, style = filled, fillcolor = lightgrey];
180 -> 272 [arrowhead = none , style=dashed];
272 -> 2[style=dashed];

273 [label="BACKTRACK\nfor clause: p(0, 0)\nwith clash: (m(s(s(T55)), T24, T3), m(X3, 0, X4))", fontsize=14, style = filled, fillcolor = lightgreen];
185 -> 273 [arrowhead = none ];
273 -> 190;

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

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

276 [label="EVAL with clause\np(s(0), 0).\nand substitutionT24 -> s(0),\nX22 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
191 -> 276 [arrowhead = none ];
276 -> 193;

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

278 [label="EVAL with clause\np(s(s(X76)), s(X77)) :- p(s(X76), X77).\nand substitutionX76 -> T60,\nT24 -> s(s(T60)),\nX77 -> X78,\nX22 -> s(X78)", fontsize=14, style = filled, fillcolor = lightblue];
192 -> 278 [arrowhead = none ];
278 -> 205;

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

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

281 [label="INSTANCE with matching:\nT30 -> T60\nX31 -> X78", fontsize=14, style = filled, fillcolor = lightgrey];
205 -> 281 [arrowhead = none , style=dashed];
281 -> 90[style=dashed];

}

(4) Obligation:

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

mA_in_gga(T11, 0, T11) → mA_out_gga(T11, 0, T11)
mA_in_gga(0, T14, 0) → mA_out_gga(0, T14, 0)
mA_in_gga(s(0), T24, T26) → U1_gga(T24, T26, pB_in_gaa(T24, X22, T26))
pB_in_gaa(T24, T27, T26) → U6_gaa(T24, T27, T26, pE_in_ga(T24, T27))
pE_in_ga(s(0), 0) → pE_out_ga(s(0), 0)
pE_in_ga(s(s(T30)), s(X31)) → U4_ga(T30, X31, pD_in_ga(T30, X31))
pD_in_ga(0, 0) → pD_out_ga(0, 0)
pD_in_ga(s(T33), s(X40)) → U3_ga(T33, X40, pD_in_ga(T33, X40))
U3_ga(T33, X40, pD_out_ga(T33, X40)) → pD_out_ga(s(T33), s(X40))
U4_ga(T30, X31, pD_out_ga(T30, X31)) → pE_out_ga(s(s(T30)), s(X31))
U6_gaa(T24, T27, T26, pE_out_ga(T24, T27)) → U7_gaa(T24, T27, T26, mF_in_ga(T27, T26))
mF_in_ga(0, 0) → mF_out_ga(0, 0)
mF_in_ga(T47, 0) → mF_out_ga(T47, 0)
U7_gaa(T24, T27, T26, mF_out_ga(T27, T26)) → pB_out_gaa(T24, T27, T26)
U1_gga(T24, T26, pB_out_gaa(T24, X22, T26)) → mA_out_gga(s(0), T24, T26)
mA_in_gga(s(s(T55)), T24, T26) → U2_gga(T55, T24, T26, pC_in_gagaa(T55, X69, T24, X22, T26))
pC_in_gagaa(T55, T56, T24, X22, T26) → U8_gagaa(T55, T56, T24, X22, T26, pD_in_ga(T55, T56))
U8_gagaa(T55, T56, T24, X22, T26, pD_out_ga(T55, T56)) → U9_gagaa(T55, T56, T24, X22, T26, pH_in_gaga(T24, X22, T56, T26))
pH_in_gaga(T24, T57, T56, T26) → U10_gaga(T24, T57, T56, T26, pG_in_ga(T24, T57))
pG_in_ga(s(0), 0) → pG_out_ga(s(0), 0)
pG_in_ga(s(s(T60)), s(X78)) → U5_ga(T60, X78, pD_in_ga(T60, X78))
U5_ga(T60, X78, pD_out_ga(T60, X78)) → pG_out_ga(s(s(T60)), s(X78))
U10_gaga(T24, T57, T56, T26, pG_out_ga(T24, T57)) → U11_gaga(T24, T57, T56, T26, mA_in_gga(s(T56), T57, T26))
U11_gaga(T24, T57, T56, T26, mA_out_gga(s(T56), T57, T26)) → pH_out_gaga(T24, T57, T56, T26)
U9_gagaa(T55, T56, T24, X22, T26, pH_out_gaga(T24, X22, T56, T26)) → pC_out_gagaa(T55, T56, T24, X22, T26)
U2_gga(T55, T24, T26, pC_out_gagaa(T55, X69, T24, X22, T26)) → mA_out_gga(s(s(T55)), T24, T26)

The argument filtering Pi contains the following mapping:
mA_in_gga(x1, x2, x3)  =  mA_in_gga(x1, x2)
0  =  0
mA_out_gga(x1, x2, x3)  =  mA_out_gga(x1, x2, x3)
s(x1)  =  s(x1)
U1_gga(x1, x2, x3)  =  U1_gga(x1, x3)
pB_in_gaa(x1, x2, x3)  =  pB_in_gaa(x1)
U6_gaa(x1, x2, x3, x4)  =  U6_gaa(x1, x4)
pE_in_ga(x1, x2)  =  pE_in_ga(x1)
pE_out_ga(x1, x2)  =  pE_out_ga(x1, x2)
U4_ga(x1, x2, x3)  =  U4_ga(x1, x3)
pD_in_ga(x1, x2)  =  pD_in_ga(x1)
pD_out_ga(x1, x2)  =  pD_out_ga(x1, x2)
U3_ga(x1, x2, x3)  =  U3_ga(x1, x3)
U7_gaa(x1, x2, x3, x4)  =  U7_gaa(x1, x2, x4)
mF_in_ga(x1, x2)  =  mF_in_ga(x1)
mF_out_ga(x1, x2)  =  mF_out_ga(x1, x2)
pB_out_gaa(x1, x2, x3)  =  pB_out_gaa(x1, x2, x3)
U2_gga(x1, x2, x3, x4)  =  U2_gga(x1, x2, x4)
pC_in_gagaa(x1, x2, x3, x4, x5)  =  pC_in_gagaa(x1, x3)
U8_gagaa(x1, x2, x3, x4, x5, x6)  =  U8_gagaa(x1, x3, x6)
U9_gagaa(x1, x2, x3, x4, x5, x6)  =  U9_gagaa(x1, x2, x3, x6)
pH_in_gaga(x1, x2, x3, x4)  =  pH_in_gaga(x1, x3)
U10_gaga(x1, x2, x3, x4, x5)  =  U10_gaga(x1, x3, x5)
pG_in_ga(x1, x2)  =  pG_in_ga(x1)
pG_out_ga(x1, x2)  =  pG_out_ga(x1, x2)
U5_ga(x1, x2, x3)  =  U5_ga(x1, x3)
U11_gaga(x1, x2, x3, x4, x5)  =  U11_gaga(x1, x2, x3, x5)
pH_out_gaga(x1, x2, x3, x4)  =  pH_out_gaga(x1, x2, x3, x4)
pC_out_gagaa(x1, x2, x3, x4, x5)  =  pC_out_gagaa(x1, x2, x3, x4, x5)

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

MA_IN_GGA(s(0), T24, T26) → U1_GGA(T24, T26, pB_in_gaa(T24, X22, T26))
MA_IN_GGA(s(0), T24, T26) → PB_IN_GAA(T24, X22, T26)
PB_IN_GAA(T24, T27, T26) → U6_GAA(T24, T27, T26, pE_in_ga(T24, T27))
PB_IN_GAA(T24, T27, T26) → PE_IN_GA(T24, T27)
PE_IN_GA(s(s(T30)), s(X31)) → U4_GA(T30, X31, pD_in_ga(T30, X31))
PE_IN_GA(s(s(T30)), s(X31)) → PD_IN_GA(T30, X31)
PD_IN_GA(s(T33), s(X40)) → U3_GA(T33, X40, pD_in_ga(T33, X40))
PD_IN_GA(s(T33), s(X40)) → PD_IN_GA(T33, X40)
U6_GAA(T24, T27, T26, pE_out_ga(T24, T27)) → U7_GAA(T24, T27, T26, mF_in_ga(T27, T26))
U6_GAA(T24, T27, T26, pE_out_ga(T24, T27)) → MF_IN_GA(T27, T26)
MA_IN_GGA(s(s(T55)), T24, T26) → U2_GGA(T55, T24, T26, pC_in_gagaa(T55, X69, T24, X22, T26))
MA_IN_GGA(s(s(T55)), T24, T26) → PC_IN_GAGAA(T55, X69, T24, X22, T26)
PC_IN_GAGAA(T55, T56, T24, X22, T26) → U8_GAGAA(T55, T56, T24, X22, T26, pD_in_ga(T55, T56))
PC_IN_GAGAA(T55, T56, T24, X22, T26) → PD_IN_GA(T55, T56)
U8_GAGAA(T55, T56, T24, X22, T26, pD_out_ga(T55, T56)) → U9_GAGAA(T55, T56, T24, X22, T26, pH_in_gaga(T24, X22, T56, T26))
U8_GAGAA(T55, T56, T24, X22, T26, pD_out_ga(T55, T56)) → PH_IN_GAGA(T24, X22, T56, T26)
PH_IN_GAGA(T24, T57, T56, T26) → U10_GAGA(T24, T57, T56, T26, pG_in_ga(T24, T57))
PH_IN_GAGA(T24, T57, T56, T26) → PG_IN_GA(T24, T57)
PG_IN_GA(s(s(T60)), s(X78)) → U5_GA(T60, X78, pD_in_ga(T60, X78))
PG_IN_GA(s(s(T60)), s(X78)) → PD_IN_GA(T60, X78)
U10_GAGA(T24, T57, T56, T26, pG_out_ga(T24, T57)) → U11_GAGA(T24, T57, T56, T26, mA_in_gga(s(T56), T57, T26))
U10_GAGA(T24, T57, T56, T26, pG_out_ga(T24, T57)) → MA_IN_GGA(s(T56), T57, T26)

The TRS R consists of the following rules:

mA_in_gga(T11, 0, T11) → mA_out_gga(T11, 0, T11)
mA_in_gga(0, T14, 0) → mA_out_gga(0, T14, 0)
mA_in_gga(s(0), T24, T26) → U1_gga(T24, T26, pB_in_gaa(T24, X22, T26))
pB_in_gaa(T24, T27, T26) → U6_gaa(T24, T27, T26, pE_in_ga(T24, T27))
pE_in_ga(s(0), 0) → pE_out_ga(s(0), 0)
pE_in_ga(s(s(T30)), s(X31)) → U4_ga(T30, X31, pD_in_ga(T30, X31))
pD_in_ga(0, 0) → pD_out_ga(0, 0)
pD_in_ga(s(T33), s(X40)) → U3_ga(T33, X40, pD_in_ga(T33, X40))
U3_ga(T33, X40, pD_out_ga(T33, X40)) → pD_out_ga(s(T33), s(X40))
U4_ga(T30, X31, pD_out_ga(T30, X31)) → pE_out_ga(s(s(T30)), s(X31))
U6_gaa(T24, T27, T26, pE_out_ga(T24, T27)) → U7_gaa(T24, T27, T26, mF_in_ga(T27, T26))
mF_in_ga(0, 0) → mF_out_ga(0, 0)
mF_in_ga(T47, 0) → mF_out_ga(T47, 0)
U7_gaa(T24, T27, T26, mF_out_ga(T27, T26)) → pB_out_gaa(T24, T27, T26)
U1_gga(T24, T26, pB_out_gaa(T24, X22, T26)) → mA_out_gga(s(0), T24, T26)
mA_in_gga(s(s(T55)), T24, T26) → U2_gga(T55, T24, T26, pC_in_gagaa(T55, X69, T24, X22, T26))
pC_in_gagaa(T55, T56, T24, X22, T26) → U8_gagaa(T55, T56, T24, X22, T26, pD_in_ga(T55, T56))
U8_gagaa(T55, T56, T24, X22, T26, pD_out_ga(T55, T56)) → U9_gagaa(T55, T56, T24, X22, T26, pH_in_gaga(T24, X22, T56, T26))
pH_in_gaga(T24, T57, T56, T26) → U10_gaga(T24, T57, T56, T26, pG_in_ga(T24, T57))
pG_in_ga(s(0), 0) → pG_out_ga(s(0), 0)
pG_in_ga(s(s(T60)), s(X78)) → U5_ga(T60, X78, pD_in_ga(T60, X78))
U5_ga(T60, X78, pD_out_ga(T60, X78)) → pG_out_ga(s(s(T60)), s(X78))
U10_gaga(T24, T57, T56, T26, pG_out_ga(T24, T57)) → U11_gaga(T24, T57, T56, T26, mA_in_gga(s(T56), T57, T26))
U11_gaga(T24, T57, T56, T26, mA_out_gga(s(T56), T57, T26)) → pH_out_gaga(T24, T57, T56, T26)
U9_gagaa(T55, T56, T24, X22, T26, pH_out_gaga(T24, X22, T56, T26)) → pC_out_gagaa(T55, T56, T24, X22, T26)
U2_gga(T55, T24, T26, pC_out_gagaa(T55, X69, T24, X22, T26)) → mA_out_gga(s(s(T55)), T24, T26)

The argument filtering Pi contains the following mapping:
mA_in_gga(x1, x2, x3)  =  mA_in_gga(x1, x2)
0  =  0
mA_out_gga(x1, x2, x3)  =  mA_out_gga(x1, x2, x3)
s(x1)  =  s(x1)
U1_gga(x1, x2, x3)  =  U1_gga(x1, x3)
pB_in_gaa(x1, x2, x3)  =  pB_in_gaa(x1)
U6_gaa(x1, x2, x3, x4)  =  U6_gaa(x1, x4)
pE_in_ga(x1, x2)  =  pE_in_ga(x1)
pE_out_ga(x1, x2)  =  pE_out_ga(x1, x2)
U4_ga(x1, x2, x3)  =  U4_ga(x1, x3)
pD_in_ga(x1, x2)  =  pD_in_ga(x1)
pD_out_ga(x1, x2)  =  pD_out_ga(x1, x2)
U3_ga(x1, x2, x3)  =  U3_ga(x1, x3)
U7_gaa(x1, x2, x3, x4)  =  U7_gaa(x1, x2, x4)
mF_in_ga(x1, x2)  =  mF_in_ga(x1)
mF_out_ga(x1, x2)  =  mF_out_ga(x1, x2)
pB_out_gaa(x1, x2, x3)  =  pB_out_gaa(x1, x2, x3)
U2_gga(x1, x2, x3, x4)  =  U2_gga(x1, x2, x4)
pC_in_gagaa(x1, x2, x3, x4, x5)  =  pC_in_gagaa(x1, x3)
U8_gagaa(x1, x2, x3, x4, x5, x6)  =  U8_gagaa(x1, x3, x6)
U9_gagaa(x1, x2, x3, x4, x5, x6)  =  U9_gagaa(x1, x2, x3, x6)
pH_in_gaga(x1, x2, x3, x4)  =  pH_in_gaga(x1, x3)
U10_gaga(x1, x2, x3, x4, x5)  =  U10_gaga(x1, x3, x5)
pG_in_ga(x1, x2)  =  pG_in_ga(x1)
pG_out_ga(x1, x2)  =  pG_out_ga(x1, x2)
U5_ga(x1, x2, x3)  =  U5_ga(x1, x3)
U11_gaga(x1, x2, x3, x4, x5)  =  U11_gaga(x1, x2, x3, x5)
pH_out_gaga(x1, x2, x3, x4)  =  pH_out_gaga(x1, x2, x3, x4)
pC_out_gagaa(x1, x2, x3, x4, x5)  =  pC_out_gagaa(x1, x2, x3, x4, x5)
MA_IN_GGA(x1, x2, x3)  =  MA_IN_GGA(x1, x2)
U1_GGA(x1, x2, x3)  =  U1_GGA(x1, x3)
PB_IN_GAA(x1, x2, x3)  =  PB_IN_GAA(x1)
U6_GAA(x1, x2, x3, x4)  =  U6_GAA(x1, x4)
PE_IN_GA(x1, x2)  =  PE_IN_GA(x1)
U4_GA(x1, x2, x3)  =  U4_GA(x1, x3)
PD_IN_GA(x1, x2)  =  PD_IN_GA(x1)
U3_GA(x1, x2, x3)  =  U3_GA(x1, x3)
U7_GAA(x1, x2, x3, x4)  =  U7_GAA(x1, x2, x4)
MF_IN_GA(x1, x2)  =  MF_IN_GA(x1)
U2_GGA(x1, x2, x3, x4)  =  U2_GGA(x1, x2, x4)
PC_IN_GAGAA(x1, x2, x3, x4, x5)  =  PC_IN_GAGAA(x1, x3)
U8_GAGAA(x1, x2, x3, x4, x5, x6)  =  U8_GAGAA(x1, x3, x6)
U9_GAGAA(x1, x2, x3, x4, x5, x6)  =  U9_GAGAA(x1, x2, x3, x6)
PH_IN_GAGA(x1, x2, x3, x4)  =  PH_IN_GAGA(x1, x3)
U10_GAGA(x1, x2, x3, x4, x5)  =  U10_GAGA(x1, x3, x5)
PG_IN_GA(x1, x2)  =  PG_IN_GA(x1)
U5_GA(x1, x2, x3)  =  U5_GA(x1, x3)
U11_GAGA(x1, x2, x3, x4, x5)  =  U11_GAGA(x1, x2, x3, x5)

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

(6) Obligation:

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

MA_IN_GGA(s(0), T24, T26) → U1_GGA(T24, T26, pB_in_gaa(T24, X22, T26))
MA_IN_GGA(s(0), T24, T26) → PB_IN_GAA(T24, X22, T26)
PB_IN_GAA(T24, T27, T26) → U6_GAA(T24, T27, T26, pE_in_ga(T24, T27))
PB_IN_GAA(T24, T27, T26) → PE_IN_GA(T24, T27)
PE_IN_GA(s(s(T30)), s(X31)) → U4_GA(T30, X31, pD_in_ga(T30, X31))
PE_IN_GA(s(s(T30)), s(X31)) → PD_IN_GA(T30, X31)
PD_IN_GA(s(T33), s(X40)) → U3_GA(T33, X40, pD_in_ga(T33, X40))
PD_IN_GA(s(T33), s(X40)) → PD_IN_GA(T33, X40)
U6_GAA(T24, T27, T26, pE_out_ga(T24, T27)) → U7_GAA(T24, T27, T26, mF_in_ga(T27, T26))
U6_GAA(T24, T27, T26, pE_out_ga(T24, T27)) → MF_IN_GA(T27, T26)
MA_IN_GGA(s(s(T55)), T24, T26) → U2_GGA(T55, T24, T26, pC_in_gagaa(T55, X69, T24, X22, T26))
MA_IN_GGA(s(s(T55)), T24, T26) → PC_IN_GAGAA(T55, X69, T24, X22, T26)
PC_IN_GAGAA(T55, T56, T24, X22, T26) → U8_GAGAA(T55, T56, T24, X22, T26, pD_in_ga(T55, T56))
PC_IN_GAGAA(T55, T56, T24, X22, T26) → PD_IN_GA(T55, T56)
U8_GAGAA(T55, T56, T24, X22, T26, pD_out_ga(T55, T56)) → U9_GAGAA(T55, T56, T24, X22, T26, pH_in_gaga(T24, X22, T56, T26))
U8_GAGAA(T55, T56, T24, X22, T26, pD_out_ga(T55, T56)) → PH_IN_GAGA(T24, X22, T56, T26)
PH_IN_GAGA(T24, T57, T56, T26) → U10_GAGA(T24, T57, T56, T26, pG_in_ga(T24, T57))
PH_IN_GAGA(T24, T57, T56, T26) → PG_IN_GA(T24, T57)
PG_IN_GA(s(s(T60)), s(X78)) → U5_GA(T60, X78, pD_in_ga(T60, X78))
PG_IN_GA(s(s(T60)), s(X78)) → PD_IN_GA(T60, X78)
U10_GAGA(T24, T57, T56, T26, pG_out_ga(T24, T57)) → U11_GAGA(T24, T57, T56, T26, mA_in_gga(s(T56), T57, T26))
U10_GAGA(T24, T57, T56, T26, pG_out_ga(T24, T57)) → MA_IN_GGA(s(T56), T57, T26)

The TRS R consists of the following rules:

mA_in_gga(T11, 0, T11) → mA_out_gga(T11, 0, T11)
mA_in_gga(0, T14, 0) → mA_out_gga(0, T14, 0)
mA_in_gga(s(0), T24, T26) → U1_gga(T24, T26, pB_in_gaa(T24, X22, T26))
pB_in_gaa(T24, T27, T26) → U6_gaa(T24, T27, T26, pE_in_ga(T24, T27))
pE_in_ga(s(0), 0) → pE_out_ga(s(0), 0)
pE_in_ga(s(s(T30)), s(X31)) → U4_ga(T30, X31, pD_in_ga(T30, X31))
pD_in_ga(0, 0) → pD_out_ga(0, 0)
pD_in_ga(s(T33), s(X40)) → U3_ga(T33, X40, pD_in_ga(T33, X40))
U3_ga(T33, X40, pD_out_ga(T33, X40)) → pD_out_ga(s(T33), s(X40))
U4_ga(T30, X31, pD_out_ga(T30, X31)) → pE_out_ga(s(s(T30)), s(X31))
U6_gaa(T24, T27, T26, pE_out_ga(T24, T27)) → U7_gaa(T24, T27, T26, mF_in_ga(T27, T26))
mF_in_ga(0, 0) → mF_out_ga(0, 0)
mF_in_ga(T47, 0) → mF_out_ga(T47, 0)
U7_gaa(T24, T27, T26, mF_out_ga(T27, T26)) → pB_out_gaa(T24, T27, T26)
U1_gga(T24, T26, pB_out_gaa(T24, X22, T26)) → mA_out_gga(s(0), T24, T26)
mA_in_gga(s(s(T55)), T24, T26) → U2_gga(T55, T24, T26, pC_in_gagaa(T55, X69, T24, X22, T26))
pC_in_gagaa(T55, T56, T24, X22, T26) → U8_gagaa(T55, T56, T24, X22, T26, pD_in_ga(T55, T56))
U8_gagaa(T55, T56, T24, X22, T26, pD_out_ga(T55, T56)) → U9_gagaa(T55, T56, T24, X22, T26, pH_in_gaga(T24, X22, T56, T26))
pH_in_gaga(T24, T57, T56, T26) → U10_gaga(T24, T57, T56, T26, pG_in_ga(T24, T57))
pG_in_ga(s(0), 0) → pG_out_ga(s(0), 0)
pG_in_ga(s(s(T60)), s(X78)) → U5_ga(T60, X78, pD_in_ga(T60, X78))
U5_ga(T60, X78, pD_out_ga(T60, X78)) → pG_out_ga(s(s(T60)), s(X78))
U10_gaga(T24, T57, T56, T26, pG_out_ga(T24, T57)) → U11_gaga(T24, T57, T56, T26, mA_in_gga(s(T56), T57, T26))
U11_gaga(T24, T57, T56, T26, mA_out_gga(s(T56), T57, T26)) → pH_out_gaga(T24, T57, T56, T26)
U9_gagaa(T55, T56, T24, X22, T26, pH_out_gaga(T24, X22, T56, T26)) → pC_out_gagaa(T55, T56, T24, X22, T26)
U2_gga(T55, T24, T26, pC_out_gagaa(T55, X69, T24, X22, T26)) → mA_out_gga(s(s(T55)), T24, T26)

The argument filtering Pi contains the following mapping:
mA_in_gga(x1, x2, x3)  =  mA_in_gga(x1, x2)
0  =  0
mA_out_gga(x1, x2, x3)  =  mA_out_gga(x1, x2, x3)
s(x1)  =  s(x1)
U1_gga(x1, x2, x3)  =  U1_gga(x1, x3)
pB_in_gaa(x1, x2, x3)  =  pB_in_gaa(x1)
U6_gaa(x1, x2, x3, x4)  =  U6_gaa(x1, x4)
pE_in_ga(x1, x2)  =  pE_in_ga(x1)
pE_out_ga(x1, x2)  =  pE_out_ga(x1, x2)
U4_ga(x1, x2, x3)  =  U4_ga(x1, x3)
pD_in_ga(x1, x2)  =  pD_in_ga(x1)
pD_out_ga(x1, x2)  =  pD_out_ga(x1, x2)
U3_ga(x1, x2, x3)  =  U3_ga(x1, x3)
U7_gaa(x1, x2, x3, x4)  =  U7_gaa(x1, x2, x4)
mF_in_ga(x1, x2)  =  mF_in_ga(x1)
mF_out_ga(x1, x2)  =  mF_out_ga(x1, x2)
pB_out_gaa(x1, x2, x3)  =  pB_out_gaa(x1, x2, x3)
U2_gga(x1, x2, x3, x4)  =  U2_gga(x1, x2, x4)
pC_in_gagaa(x1, x2, x3, x4, x5)  =  pC_in_gagaa(x1, x3)
U8_gagaa(x1, x2, x3, x4, x5, x6)  =  U8_gagaa(x1, x3, x6)
U9_gagaa(x1, x2, x3, x4, x5, x6)  =  U9_gagaa(x1, x2, x3, x6)
pH_in_gaga(x1, x2, x3, x4)  =  pH_in_gaga(x1, x3)
U10_gaga(x1, x2, x3, x4, x5)  =  U10_gaga(x1, x3, x5)
pG_in_ga(x1, x2)  =  pG_in_ga(x1)
pG_out_ga(x1, x2)  =  pG_out_ga(x1, x2)
U5_ga(x1, x2, x3)  =  U5_ga(x1, x3)
U11_gaga(x1, x2, x3, x4, x5)  =  U11_gaga(x1, x2, x3, x5)
pH_out_gaga(x1, x2, x3, x4)  =  pH_out_gaga(x1, x2, x3, x4)
pC_out_gagaa(x1, x2, x3, x4, x5)  =  pC_out_gagaa(x1, x2, x3, x4, x5)
MA_IN_GGA(x1, x2, x3)  =  MA_IN_GGA(x1, x2)
U1_GGA(x1, x2, x3)  =  U1_GGA(x1, x3)
PB_IN_GAA(x1, x2, x3)  =  PB_IN_GAA(x1)
U6_GAA(x1, x2, x3, x4)  =  U6_GAA(x1, x4)
PE_IN_GA(x1, x2)  =  PE_IN_GA(x1)
U4_GA(x1, x2, x3)  =  U4_GA(x1, x3)
PD_IN_GA(x1, x2)  =  PD_IN_GA(x1)
U3_GA(x1, x2, x3)  =  U3_GA(x1, x3)
U7_GAA(x1, x2, x3, x4)  =  U7_GAA(x1, x2, x4)
MF_IN_GA(x1, x2)  =  MF_IN_GA(x1)
U2_GGA(x1, x2, x3, x4)  =  U2_GGA(x1, x2, x4)
PC_IN_GAGAA(x1, x2, x3, x4, x5)  =  PC_IN_GAGAA(x1, x3)
U8_GAGAA(x1, x2, x3, x4, x5, x6)  =  U8_GAGAA(x1, x3, x6)
U9_GAGAA(x1, x2, x3, x4, x5, x6)  =  U9_GAGAA(x1, x2, x3, x6)
PH_IN_GAGA(x1, x2, x3, x4)  =  PH_IN_GAGA(x1, x3)
U10_GAGA(x1, x2, x3, x4, x5)  =  U10_GAGA(x1, x3, x5)
PG_IN_GA(x1, x2)  =  PG_IN_GA(x1)
U5_GA(x1, x2, x3)  =  U5_GA(x1, x3)
U11_GAGA(x1, x2, x3, x4, x5)  =  U11_GAGA(x1, x2, x3, x5)

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

(7) DependencyGraphProof (EQUIVALENT transformation)

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

(8) Complex Obligation (AND)

(9) Obligation:

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

PD_IN_GA(s(T33), s(X40)) → PD_IN_GA(T33, X40)

The TRS R consists of the following rules:

mA_in_gga(T11, 0, T11) → mA_out_gga(T11, 0, T11)
mA_in_gga(0, T14, 0) → mA_out_gga(0, T14, 0)
mA_in_gga(s(0), T24, T26) → U1_gga(T24, T26, pB_in_gaa(T24, X22, T26))
pB_in_gaa(T24, T27, T26) → U6_gaa(T24, T27, T26, pE_in_ga(T24, T27))
pE_in_ga(s(0), 0) → pE_out_ga(s(0), 0)
pE_in_ga(s(s(T30)), s(X31)) → U4_ga(T30, X31, pD_in_ga(T30, X31))
pD_in_ga(0, 0) → pD_out_ga(0, 0)
pD_in_ga(s(T33), s(X40)) → U3_ga(T33, X40, pD_in_ga(T33, X40))
U3_ga(T33, X40, pD_out_ga(T33, X40)) → pD_out_ga(s(T33), s(X40))
U4_ga(T30, X31, pD_out_ga(T30, X31)) → pE_out_ga(s(s(T30)), s(X31))
U6_gaa(T24, T27, T26, pE_out_ga(T24, T27)) → U7_gaa(T24, T27, T26, mF_in_ga(T27, T26))
mF_in_ga(0, 0) → mF_out_ga(0, 0)
mF_in_ga(T47, 0) → mF_out_ga(T47, 0)
U7_gaa(T24, T27, T26, mF_out_ga(T27, T26)) → pB_out_gaa(T24, T27, T26)
U1_gga(T24, T26, pB_out_gaa(T24, X22, T26)) → mA_out_gga(s(0), T24, T26)
mA_in_gga(s(s(T55)), T24, T26) → U2_gga(T55, T24, T26, pC_in_gagaa(T55, X69, T24, X22, T26))
pC_in_gagaa(T55, T56, T24, X22, T26) → U8_gagaa(T55, T56, T24, X22, T26, pD_in_ga(T55, T56))
U8_gagaa(T55, T56, T24, X22, T26, pD_out_ga(T55, T56)) → U9_gagaa(T55, T56, T24, X22, T26, pH_in_gaga(T24, X22, T56, T26))
pH_in_gaga(T24, T57, T56, T26) → U10_gaga(T24, T57, T56, T26, pG_in_ga(T24, T57))
pG_in_ga(s(0), 0) → pG_out_ga(s(0), 0)
pG_in_ga(s(s(T60)), s(X78)) → U5_ga(T60, X78, pD_in_ga(T60, X78))
U5_ga(T60, X78, pD_out_ga(T60, X78)) → pG_out_ga(s(s(T60)), s(X78))
U10_gaga(T24, T57, T56, T26, pG_out_ga(T24, T57)) → U11_gaga(T24, T57, T56, T26, mA_in_gga(s(T56), T57, T26))
U11_gaga(T24, T57, T56, T26, mA_out_gga(s(T56), T57, T26)) → pH_out_gaga(T24, T57, T56, T26)
U9_gagaa(T55, T56, T24, X22, T26, pH_out_gaga(T24, X22, T56, T26)) → pC_out_gagaa(T55, T56, T24, X22, T26)
U2_gga(T55, T24, T26, pC_out_gagaa(T55, X69, T24, X22, T26)) → mA_out_gga(s(s(T55)), T24, T26)

The argument filtering Pi contains the following mapping:
mA_in_gga(x1, x2, x3)  =  mA_in_gga(x1, x2)
0  =  0
mA_out_gga(x1, x2, x3)  =  mA_out_gga(x1, x2, x3)
s(x1)  =  s(x1)
U1_gga(x1, x2, x3)  =  U1_gga(x1, x3)
pB_in_gaa(x1, x2, x3)  =  pB_in_gaa(x1)
U6_gaa(x1, x2, x3, x4)  =  U6_gaa(x1, x4)
pE_in_ga(x1, x2)  =  pE_in_ga(x1)
pE_out_ga(x1, x2)  =  pE_out_ga(x1, x2)
U4_ga(x1, x2, x3)  =  U4_ga(x1, x3)
pD_in_ga(x1, x2)  =  pD_in_ga(x1)
pD_out_ga(x1, x2)  =  pD_out_ga(x1, x2)
U3_ga(x1, x2, x3)  =  U3_ga(x1, x3)
U7_gaa(x1, x2, x3, x4)  =  U7_gaa(x1, x2, x4)
mF_in_ga(x1, x2)  =  mF_in_ga(x1)
mF_out_ga(x1, x2)  =  mF_out_ga(x1, x2)
pB_out_gaa(x1, x2, x3)  =  pB_out_gaa(x1, x2, x3)
U2_gga(x1, x2, x3, x4)  =  U2_gga(x1, x2, x4)
pC_in_gagaa(x1, x2, x3, x4, x5)  =  pC_in_gagaa(x1, x3)
U8_gagaa(x1, x2, x3, x4, x5, x6)  =  U8_gagaa(x1, x3, x6)
U9_gagaa(x1, x2, x3, x4, x5, x6)  =  U9_gagaa(x1, x2, x3, x6)
pH_in_gaga(x1, x2, x3, x4)  =  pH_in_gaga(x1, x3)
U10_gaga(x1, x2, x3, x4, x5)  =  U10_gaga(x1, x3, x5)
pG_in_ga(x1, x2)  =  pG_in_ga(x1)
pG_out_ga(x1, x2)  =  pG_out_ga(x1, x2)
U5_ga(x1, x2, x3)  =  U5_ga(x1, x3)
U11_gaga(x1, x2, x3, x4, x5)  =  U11_gaga(x1, x2, x3, x5)
pH_out_gaga(x1, x2, x3, x4)  =  pH_out_gaga(x1, x2, x3, x4)
pC_out_gagaa(x1, x2, x3, x4, x5)  =  pC_out_gagaa(x1, x2, x3, x4, x5)
PD_IN_GA(x1, x2)  =  PD_IN_GA(x1)

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

(10) UsableRulesProof (EQUIVALENT transformation)

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

(11) Obligation:

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

PD_IN_GA(s(T33), s(X40)) → PD_IN_GA(T33, X40)

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

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

(12) PiDPToQDPProof (SOUND transformation)

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

(13) Obligation:

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

PD_IN_GA(s(T33)) → PD_IN_GA(T33)

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

(14) 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_GA(s(T33)) → PD_IN_GA(T33)
  The graph contains the following edges 1 > 1

(15) YES

(16) Obligation:

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

MA_IN_GGA(s(s(T55)), T24, T26) → PC_IN_GAGAA(T55, X69, T24, X22, T26)
PC_IN_GAGAA(T55, T56, T24, X22, T26) → U8_GAGAA(T55, T56, T24, X22, T26, pD_in_ga(T55, T56))
U8_GAGAA(T55, T56, T24, X22, T26, pD_out_ga(T55, T56)) → PH_IN_GAGA(T24, X22, T56, T26)
PH_IN_GAGA(T24, T57, T56, T26) → U10_GAGA(T24, T57, T56, T26, pG_in_ga(T24, T57))
U10_GAGA(T24, T57, T56, T26, pG_out_ga(T24, T57)) → MA_IN_GGA(s(T56), T57, T26)

The TRS R consists of the following rules:

mA_in_gga(T11, 0, T11) → mA_out_gga(T11, 0, T11)
mA_in_gga(0, T14, 0) → mA_out_gga(0, T14, 0)
mA_in_gga(s(0), T24, T26) → U1_gga(T24, T26, pB_in_gaa(T24, X22, T26))
pB_in_gaa(T24, T27, T26) → U6_gaa(T24, T27, T26, pE_in_ga(T24, T27))
pE_in_ga(s(0), 0) → pE_out_ga(s(0), 0)
pE_in_ga(s(s(T30)), s(X31)) → U4_ga(T30, X31, pD_in_ga(T30, X31))
pD_in_ga(0, 0) → pD_out_ga(0, 0)
pD_in_ga(s(T33), s(X40)) → U3_ga(T33, X40, pD_in_ga(T33, X40))
U3_ga(T33, X40, pD_out_ga(T33, X40)) → pD_out_ga(s(T33), s(X40))
U4_ga(T30, X31, pD_out_ga(T30, X31)) → pE_out_ga(s(s(T30)), s(X31))
U6_gaa(T24, T27, T26, pE_out_ga(T24, T27)) → U7_gaa(T24, T27, T26, mF_in_ga(T27, T26))
mF_in_ga(0, 0) → mF_out_ga(0, 0)
mF_in_ga(T47, 0) → mF_out_ga(T47, 0)
U7_gaa(T24, T27, T26, mF_out_ga(T27, T26)) → pB_out_gaa(T24, T27, T26)
U1_gga(T24, T26, pB_out_gaa(T24, X22, T26)) → mA_out_gga(s(0), T24, T26)
mA_in_gga(s(s(T55)), T24, T26) → U2_gga(T55, T24, T26, pC_in_gagaa(T55, X69, T24, X22, T26))
pC_in_gagaa(T55, T56, T24, X22, T26) → U8_gagaa(T55, T56, T24, X22, T26, pD_in_ga(T55, T56))
U8_gagaa(T55, T56, T24, X22, T26, pD_out_ga(T55, T56)) → U9_gagaa(T55, T56, T24, X22, T26, pH_in_gaga(T24, X22, T56, T26))
pH_in_gaga(T24, T57, T56, T26) → U10_gaga(T24, T57, T56, T26, pG_in_ga(T24, T57))
pG_in_ga(s(0), 0) → pG_out_ga(s(0), 0)
pG_in_ga(s(s(T60)), s(X78)) → U5_ga(T60, X78, pD_in_ga(T60, X78))
U5_ga(T60, X78, pD_out_ga(T60, X78)) → pG_out_ga(s(s(T60)), s(X78))
U10_gaga(T24, T57, T56, T26, pG_out_ga(T24, T57)) → U11_gaga(T24, T57, T56, T26, mA_in_gga(s(T56), T57, T26))
U11_gaga(T24, T57, T56, T26, mA_out_gga(s(T56), T57, T26)) → pH_out_gaga(T24, T57, T56, T26)
U9_gagaa(T55, T56, T24, X22, T26, pH_out_gaga(T24, X22, T56, T26)) → pC_out_gagaa(T55, T56, T24, X22, T26)
U2_gga(T55, T24, T26, pC_out_gagaa(T55, X69, T24, X22, T26)) → mA_out_gga(s(s(T55)), T24, T26)

The argument filtering Pi contains the following mapping:
mA_in_gga(x1, x2, x3)  =  mA_in_gga(x1, x2)
0  =  0
mA_out_gga(x1, x2, x3)  =  mA_out_gga(x1, x2, x3)
s(x1)  =  s(x1)
U1_gga(x1, x2, x3)  =  U1_gga(x1, x3)
pB_in_gaa(x1, x2, x3)  =  pB_in_gaa(x1)
U6_gaa(x1, x2, x3, x4)  =  U6_gaa(x1, x4)
pE_in_ga(x1, x2)  =  pE_in_ga(x1)
pE_out_ga(x1, x2)  =  pE_out_ga(x1, x2)
U4_ga(x1, x2, x3)  =  U4_ga(x1, x3)
pD_in_ga(x1, x2)  =  pD_in_ga(x1)
pD_out_ga(x1, x2)  =  pD_out_ga(x1, x2)
U3_ga(x1, x2, x3)  =  U3_ga(x1, x3)
U7_gaa(x1, x2, x3, x4)  =  U7_gaa(x1, x2, x4)
mF_in_ga(x1, x2)  =  mF_in_ga(x1)
mF_out_ga(x1, x2)  =  mF_out_ga(x1, x2)
pB_out_gaa(x1, x2, x3)  =  pB_out_gaa(x1, x2, x3)
U2_gga(x1, x2, x3, x4)  =  U2_gga(x1, x2, x4)
pC_in_gagaa(x1, x2, x3, x4, x5)  =  pC_in_gagaa(x1, x3)
U8_gagaa(x1, x2, x3, x4, x5, x6)  =  U8_gagaa(x1, x3, x6)
U9_gagaa(x1, x2, x3, x4, x5, x6)  =  U9_gagaa(x1, x2, x3, x6)
pH_in_gaga(x1, x2, x3, x4)  =  pH_in_gaga(x1, x3)
U10_gaga(x1, x2, x3, x4, x5)  =  U10_gaga(x1, x3, x5)
pG_in_ga(x1, x2)  =  pG_in_ga(x1)
pG_out_ga(x1, x2)  =  pG_out_ga(x1, x2)
U5_ga(x1, x2, x3)  =  U5_ga(x1, x3)
U11_gaga(x1, x2, x3, x4, x5)  =  U11_gaga(x1, x2, x3, x5)
pH_out_gaga(x1, x2, x3, x4)  =  pH_out_gaga(x1, x2, x3, x4)
pC_out_gagaa(x1, x2, x3, x4, x5)  =  pC_out_gagaa(x1, x2, x3, x4, x5)
MA_IN_GGA(x1, x2, x3)  =  MA_IN_GGA(x1, x2)
PC_IN_GAGAA(x1, x2, x3, x4, x5)  =  PC_IN_GAGAA(x1, x3)
U8_GAGAA(x1, x2, x3, x4, x5, x6)  =  U8_GAGAA(x1, x3, x6)
PH_IN_GAGA(x1, x2, x3, x4)  =  PH_IN_GAGA(x1, x3)
U10_GAGA(x1, x2, x3, x4, x5)  =  U10_GAGA(x1, x3, x5)

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

(17) UsableRulesProof (EQUIVALENT transformation)

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

(18) Obligation:

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

MA_IN_GGA(s(s(T55)), T24, T26) → PC_IN_GAGAA(T55, X69, T24, X22, T26)
PC_IN_GAGAA(T55, T56, T24, X22, T26) → U8_GAGAA(T55, T56, T24, X22, T26, pD_in_ga(T55, T56))
U8_GAGAA(T55, T56, T24, X22, T26, pD_out_ga(T55, T56)) → PH_IN_GAGA(T24, X22, T56, T26)
PH_IN_GAGA(T24, T57, T56, T26) → U10_GAGA(T24, T57, T56, T26, pG_in_ga(T24, T57))
U10_GAGA(T24, T57, T56, T26, pG_out_ga(T24, T57)) → MA_IN_GGA(s(T56), T57, T26)

The TRS R consists of the following rules:

pD_in_ga(0, 0) → pD_out_ga(0, 0)
pD_in_ga(s(T33), s(X40)) → U3_ga(T33, X40, pD_in_ga(T33, X40))
pG_in_ga(s(0), 0) → pG_out_ga(s(0), 0)
pG_in_ga(s(s(T60)), s(X78)) → U5_ga(T60, X78, pD_in_ga(T60, X78))
U3_ga(T33, X40, pD_out_ga(T33, X40)) → pD_out_ga(s(T33), s(X40))
U5_ga(T60, X78, pD_out_ga(T60, X78)) → pG_out_ga(s(s(T60)), s(X78))

The argument filtering Pi contains the following mapping:
0  =  0
s(x1)  =  s(x1)
pD_in_ga(x1, x2)  =  pD_in_ga(x1)
pD_out_ga(x1, x2)  =  pD_out_ga(x1, x2)
U3_ga(x1, x2, x3)  =  U3_ga(x1, x3)
pG_in_ga(x1, x2)  =  pG_in_ga(x1)
pG_out_ga(x1, x2)  =  pG_out_ga(x1, x2)
U5_ga(x1, x2, x3)  =  U5_ga(x1, x3)
MA_IN_GGA(x1, x2, x3)  =  MA_IN_GGA(x1, x2)
PC_IN_GAGAA(x1, x2, x3, x4, x5)  =  PC_IN_GAGAA(x1, x3)
U8_GAGAA(x1, x2, x3, x4, x5, x6)  =  U8_GAGAA(x1, x3, x6)
PH_IN_GAGA(x1, x2, x3, x4)  =  PH_IN_GAGA(x1, x3)
U10_GAGA(x1, x2, x3, x4, x5)  =  U10_GAGA(x1, x3, x5)

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

(19) PiDPToQDPProof (SOUND transformation)

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

(20) Obligation:

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

MA_IN_GGA(s(s(T55)), T24) → PC_IN_GAGAA(T55, T24)
PC_IN_GAGAA(T55, T24) → U8_GAGAA(T55, T24, pD_in_ga(T55))
U8_GAGAA(T55, T24, pD_out_ga(T55, T56)) → PH_IN_GAGA(T24, T56)
PH_IN_GAGA(T24, T56) → U10_GAGA(T24, T56, pG_in_ga(T24))
U10_GAGA(T24, T56, pG_out_ga(T24, T57)) → MA_IN_GGA(s(T56), T57)

The TRS R consists of the following rules:

pD_in_ga(0) → pD_out_ga(0, 0)
pD_in_ga(s(T33)) → U3_ga(T33, pD_in_ga(T33))
pG_in_ga(s(0)) → pG_out_ga(s(0), 0)
pG_in_ga(s(s(T60))) → U5_ga(T60, pD_in_ga(T60))
U3_ga(T33, pD_out_ga(T33, X40)) → pD_out_ga(s(T33), s(X40))
U5_ga(T60, pD_out_ga(T60, X78)) → pG_out_ga(s(s(T60)), s(X78))

The set Q consists of the following terms:

pD_in_ga(x0)
pG_in_ga(x0)
U3_ga(x0, x1)
U5_ga(x0, x1)

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

(21) QDPOrderProof (EQUIVALENT transformation)

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

The following pairs can be oriented strictly and are deleted.

MA_IN_GGA(s(s(T55)), T24) → PC_IN_GAGAA(T55, T24)

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

POL(0) = 0   
POL(MA_IN_GGA(x₁, x₂)) = x₁   
POL(PC_IN_GAGAA(x₁, x₂)) = 1 + x₁   
POL(PH_IN_GAGA(x₁, x₂)) = 1 + x₂   
POL(U10_GAGA(x₁, x₂, x₃)) = 1 + x₂   
POL(U3_ga(x₁, x₂)) = 1 + x₂   
POL(U5_ga(x₁, x₂)) = 0   
POL(U8_GAGAA(x₁, x₂, x₃)) = 1 + x₃   
POL(pD_in_ga(x₁)) = x₁   
POL(pD_out_ga(x₁, x₂)) = x₂   
POL(pG_in_ga(x₁)) = 0   
POL(pG_out_ga(x₁, x₂)) = 0   
POL(s(x₁)) = 1 + x₁   

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

pD_in_ga(0) → pD_out_ga(0, 0)
pD_in_ga(s(T33)) → U3_ga(T33, pD_in_ga(T33))
U3_ga(T33, pD_out_ga(T33, X40)) → pD_out_ga(s(T33), s(X40))

(22) Obligation:

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

PC_IN_GAGAA(T55, T24) → U8_GAGAA(T55, T24, pD_in_ga(T55))
U8_GAGAA(T55, T24, pD_out_ga(T55, T56)) → PH_IN_GAGA(T24, T56)
PH_IN_GAGA(T24, T56) → U10_GAGA(T24, T56, pG_in_ga(T24))
U10_GAGA(T24, T56, pG_out_ga(T24, T57)) → MA_IN_GGA(s(T56), T57)

The TRS R consists of the following rules:

pD_in_ga(0) → pD_out_ga(0, 0)
pD_in_ga(s(T33)) → U3_ga(T33, pD_in_ga(T33))
pG_in_ga(s(0)) → pG_out_ga(s(0), 0)
pG_in_ga(s(s(T60))) → U5_ga(T60, pD_in_ga(T60))
U3_ga(T33, pD_out_ga(T33, X40)) → pD_out_ga(s(T33), s(X40))
U5_ga(T60, pD_out_ga(T60, X78)) → pG_out_ga(s(s(T60)), s(X78))

The set Q consists of the following terms:

pD_in_ga(x0)
pG_in_ga(x0)
U3_ga(x0, x1)
U5_ga(x0, x1)

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

(23) DependencyGraphProof (EQUIVALENT transformation)

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

(24) TRUE