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

(0) Obligation:

Clauses:

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

Query: q(g,g)

(1) PrologToPiTRSViaGraphTransformerProof (SOUND transformation)

Transformed Prolog program to (Pi-)TRS.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
3 [label="A: q(T1, T2)\n\nT1 is ground\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
4 [label="4: q(T1, T2), SCOPE: 1, CLAUSE: 0\n\nT1 is ground\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
7 [label="B: m(T5, T6, X5)\n\nT5 is ground\nT6 is ground\nX5 is free", fontsize=16, style=filled, fillcolor=lightyellow];
11 [label="11: m(T5, T6, X5), SCOPE: 2, CLAUSE: 1 | m(T5, T6, X5), SCOPE: 2, CLAUSE: 2 | m(T5, T6, X5), SCOPE: 2, CLAUSE: 3\n\nT5 is ground\nT6 is ground\nX5 is free", fontsize=16, style=filled, fillcolor=lightyellow];
13 [label="13: true | m(T9, 0, X5), SCOPE: 2, CLAUSE: 2 | m(T9, 0, X5), SCOPE: 2, CLAUSE: 3\n\nT9 is ground\nX5 is free", fontsize=16, style=filled, fillcolor=lightyellow];
15 [label="15: m(T5, T6, X5), SCOPE: 2, CLAUSE: 2 | m(T5, T6, X5), SCOPE: 2, CLAUSE: 3\n\nT5 is ground\nT6 is ground\nX5 is free\nX8 is free\nm(T5, T6, X5) !=? m(X8, 0, X8)", fontsize=16, style=filled, fillcolor=lightyellow];
16 [label="16: m(T9, 0, X5), SCOPE: 2, CLAUSE: 2 | m(T9, 0, X5), SCOPE: 2, CLAUSE: 3\n\nT9 is ground\nX5 is free", fontsize=16, style=filled, fillcolor=lightyellow];
21 [label="21: !_2 | m(0, 0, X5), SCOPE: 2, CLAUSE: 3\n\nX5 is free", fontsize=16, style=filled, fillcolor=lightyellow];
25 [label="25: m(T9, 0, X5), SCOPE: 2, CLAUSE: 3\n\nT9 is ground\nX5 is free\nX11 is free\nm(T9, 0, X5) !=? m(0, X11, 0)", fontsize=16, style=filled, fillcolor=lightyellow];
27 [label="27: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
29 [label="29: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
36 [label="36: ','(p(T12, X27), ','(p(0, X28), m(X27, X28, X29)))\n\nT12 is ground\nX5 is free\nX11 is free\nX29 is free\nX27 is free\nX28 is free\nm(T12, 0, X5) !=? m(0, X11, 0)", fontsize=16, style=filled, fillcolor=lightyellow];
40 [label="40: ','(p(T12, X27), ','(p(0, X28), m(X27, X28, X29))), SCOPE: 3, CLAUSE: 4 | ','(p(T12, X27), ','(p(0, X28), m(X27, X28, X29))), SCOPE: 3, CLAUSE: 5\n\nT12 is ground\nX5 is free\nX11 is free\nX29 is free\nX27 is free\nX28 is free\nm(T12, 0, X5) !=? m(0, X11, 0)", fontsize=16, style=filled, fillcolor=lightyellow];
42 [label="42: ','(p(T12, X27), ','(p(0, X28), m(X27, X28, X29))), SCOPE: 3, CLAUSE: 5\n\nT12 is ground\nX5 is free\nX11 is free\nX29 is free\nX27 is free\nX28 is free\nm(T12, 0, X5) !=? m(0, X11, 0)", fontsize=16, style=filled, fillcolor=lightyellow];
43 [label="43: ','(p(0, X28), m(T15, X28, X29))\n\nT15 is ground\nX29 is free\nX28 is free", fontsize=16, style=filled, fillcolor=lightyellow];
44 [label="44: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
47 [label="47: ','(p(0, X28), m(T15, X28, X29)), SCOPE: 4, CLAUSE: 4 | ','(p(0, X28), m(T15, X28, X29)), SCOPE: 4, CLAUSE: 5\n\nT15 is ground\nX29 is free\nX28 is free", fontsize=16, style=filled, fillcolor=lightyellow];
49 [label="49: ','(p(0, X28), m(T15, X28, X29)), SCOPE: 4, CLAUSE: 4\n\nT15 is ground\nX29 is free\nX28 is free", fontsize=16, style=filled, fillcolor=lightyellow];
54 [label="54: ','(p(0, X28), m(T15, X28, X29)), SCOPE: 4, CLAUSE: 5\n\nT15 is ground\nX29 is free\nX28 is free", fontsize=16, style=filled, fillcolor=lightyellow];
59 [label="C: m(T15, 0, X29)\n\nT15 is ground\nX29 is free", fontsize=16, style=filled, fillcolor=lightyellow];
62 [label="62: m(T15, 0, X29), SCOPE: 5, CLAUSE: 1 | m(T15, 0, X29), SCOPE: 5, CLAUSE: 2 | m(T15, 0, X29), SCOPE: 5, CLAUSE: 3\n\nT15 is ground\nX29 is free", fontsize=16, style=filled, fillcolor=lightyellow];
76 [label="76: true | m(T22, 0, X29), SCOPE: 5, CLAUSE: 2 | m(T22, 0, X29), SCOPE: 5, CLAUSE: 3\n\nT22 is ground\nX29 is free", fontsize=16, style=filled, fillcolor=lightyellow];
77 [label="77: m(T22, 0, X29), SCOPE: 5, CLAUSE: 2 | m(T22, 0, X29), SCOPE: 5, CLAUSE: 3\n\nT22 is ground\nX29 is free", fontsize=16, style=filled, fillcolor=lightyellow];
84 [label="84: !_5 | m(0, 0, X29), SCOPE: 5, CLAUSE: 3\n\nX29 is free", fontsize=16, style=filled, fillcolor=lightyellow];
85 [label="85: m(T22, 0, X29), SCOPE: 5, CLAUSE: 3\n\nT22 is ground\nX29 is free\nX44 is free\nm(T22, 0, X29) !=? m(0, X44, 0)", fontsize=16, style=filled, fillcolor=lightyellow];
86 [label="86: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
87 [label="87: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
112 [label="112: ','(p(T25, X60), ','(p(0, X61), m(X60, X61, X62)))\n\nT25 is ground\nX29 is free\nX44 is free\nX62 is free\nX60 is free\nX61 is free\nm(T25, 0, X29) !=? m(0, X44, 0)", fontsize=16, style=filled, fillcolor=lightyellow];
114 [label="114: ','(p(T25, X60), ','(p(0, X61), m(X60, X61, X62))), SCOPE: 6, CLAUSE: 4 | ','(p(T25, X60), ','(p(0, X61), m(X60, X61, X62))), SCOPE: 6, CLAUSE: 5\n\nT25 is ground\nX29 is free\nX44 is free\nX62 is free\nX60 is free\nX61 is free\nm(T25, 0, X29) !=? m(0, X44, 0)", fontsize=16, style=filled, fillcolor=lightyellow];
115 [label="115: ','(p(T25, X60), ','(p(0, X61), m(X60, X61, X62))), SCOPE: 6, CLAUSE: 5\n\nT25 is ground\nX29 is free\nX44 is free\nX62 is free\nX60 is free\nX61 is free\nm(T25, 0, X29) !=? m(0, X44, 0)", fontsize=16, style=filled, fillcolor=lightyellow];
118 [label="118: ','(p(0, X61), m(T28, X61, X62))\n\nT28 is ground\nX62 is free\nX61 is free", fontsize=16, style=filled, fillcolor=lightyellow];
119 [label="119: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
122 [label="122: ','(p(0, X61), m(T28, X61, X62)), SCOPE: 7, CLAUSE: 4 | ','(p(0, X61), m(T28, X61, X62)), SCOPE: 7, CLAUSE: 5\n\nT28 is ground\nX62 is free\nX61 is free", fontsize=16, style=filled, fillcolor=lightyellow];
124 [label="124: ','(p(0, X61), m(T28, X61, X62)), SCOPE: 7, CLAUSE: 4\n\nT28 is ground\nX62 is free\nX61 is free", fontsize=16, style=filled, fillcolor=lightyellow];
126 [label="126: ','(p(0, X61), m(T28, X61, X62)), SCOPE: 7, CLAUSE: 5\n\nT28 is ground\nX62 is free\nX61 is free", fontsize=16, style=filled, fillcolor=lightyellow];
135 [label="135: m(T28, 0, X62)\n\nT28 is ground\nX62 is free", fontsize=16, style=filled, fillcolor=lightyellow];
136 [label="136: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
137 [label="137: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
138 [label="138: !_2 | m(0, T35, X5), SCOPE: 2, CLAUSE: 3\n\nT35 is ground\nX5 is free\nX8 is free\nm(0, T35, X5) !=? m(X8, 0, X8)", fontsize=16, style=filled, fillcolor=lightyellow];
139 [label="139: m(T5, T6, X5), SCOPE: 2, CLAUSE: 3\n\nT5 is ground\nT6 is ground\nX5 is free\nX8 is free\nX76 is free\nm(T5, T6, X5) !=? m(X8, 0, X8)\nm(T5, T6, X5) !=? m(0, X76, 0)", fontsize=16, style=filled, fillcolor=lightyellow];
140 [label="140: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
141 [label="141: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
145 [label="145: ','(p(T40, X92), ','(p(T41, X93), m(X92, X93, X94)))\n\nT40 is ground\nT41 is ground\nX5 is free\nX8 is free\nX76 is free\nX94 is free\nX92 is free\nX93 is free\nm(T40, T41, X5) !=? m(X8, 0, X8)\nm(T40, T41, X5) !=? m(0, X76, 0)", fontsize=16, style=filled, fillcolor=lightyellow];
146 [label="146: ','(p(T40, X92), ','(p(T41, X93), m(X92, X93, X94))), SCOPE: 8, CLAUSE: 4 | ','(p(T40, X92), ','(p(T41, X93), m(X92, X93, X94))), SCOPE: 8, CLAUSE: 5\n\nT40 is ground\nT41 is ground\nX5 is free\nX8 is free\nX76 is free\nX94 is free\nX92 is free\nX93 is free\nm(T40, T41, X5) !=? m(X8, 0, X8)\nm(T40, T41, X5) !=? m(0, X76, 0)", fontsize=16, style=filled, fillcolor=lightyellow];
147 [label="147: ','(p(T40, X92), ','(p(T41, X93), m(X92, X93, X94))), SCOPE: 8, CLAUSE: 5\n\nT40 is ground\nT41 is ground\nX5 is free\nX8 is free\nX76 is free\nX94 is free\nX92 is free\nX93 is free\nm(T40, T41, X5) !=? m(X8, 0, X8)\nm(T40, T41, X5) !=? m(0, X76, 0)", fontsize=16, style=filled, fillcolor=lightyellow];
148 [label="148: ','(p(T41, X93), m(T44, X93, X94))\n\nT41 is ground\nT44 is ground\nX5 is free\nX8 is free\nX94 is free\nX93 is free\nm(s(T44), T41, X5) !=? m(X8, 0, X8)", fontsize=16, style=filled, fillcolor=lightyellow];
149 [label="149: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
150 [label="150: ','(p(T41, X93), m(T44, X93, X94)), SCOPE: 9, CLAUSE: 4 | ','(p(T41, X93), m(T44, X93, X94)), SCOPE: 9, CLAUSE: 5\n\nT41 is ground\nT44 is ground\nX5 is free\nX8 is free\nX94 is free\nX93 is free\nm(s(T44), T41, X5) !=? m(X8, 0, X8)", fontsize=16, style=filled, fillcolor=lightyellow];
151 [label="151: ','(p(T41, X93), m(T44, X93, X94)), SCOPE: 9, CLAUSE: 5\n\nT41 is ground\nT44 is ground\nX5 is free\nX8 is free\nX94 is free\nX93 is free\nm(s(T44), T41, X5) !=? m(X8, 0, X8)", fontsize=16, style=filled, fillcolor=lightyellow];
152 [label="152: m(T44, T48, X94)\n\nT44 is ground\nT48 is ground\nX94 is free", fontsize=16, style=filled, fillcolor=lightyellow];
153 [label="153: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
154 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
3 -> 154 [arrowhead = none ];
154 -> 4;

155 [label="ONLY EVAL with clause\nq(X3, X4) :- m(X3, X4, X5).\nand substitutionT1 -> T5,\nX3 -> T5,\nT2 -> T6,\nX4 -> T6", fontsize=14, style = filled, fillcolor = lightblue];
4 -> 155 [arrowhead = none ];
155 -> 7;

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

157 [label="EVAL with clause\nm(X8, 0, X8).\nand substitutionT5 -> T9,\nX8 -> T9,\nT6 -> 0,\nX5 -> T9", fontsize=14, style = filled, fillcolor = lightblue];
11 -> 157 [arrowhead = none ];
157 -> 13;

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

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

160 [label="EVAL with clause\nm(0, X76, 0) :- !_2.\nand substitutionT5 -> 0,\nT6 -> T35,\nX76 -> T35,\nX5 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
15 -> 160 [arrowhead = none ];
160 -> 138;

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

162 [label="EVAL with clause\nm(0, X11, 0) :- !_2.\nand substitutionT9 -> 0,\nX11 -> 0,\nX5 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
16 -> 162 [arrowhead = none ];
162 -> 21;

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

164 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
21 -> 164 [arrowhead = none ];
164 -> 27;

165 [label="ONLY EVAL with clause\nm(X24, X25, X26) :- ','(p(X24, X27), ','(p(X25, X28), m(X27, X28, X26))).\nand substitutionT9 -> T12,\nX24 -> T12,\nX25 -> 0,\nX5 -> X29,\nX26 -> X29", fontsize=14, style = filled, fillcolor = lightblue];
25 -> 165 [arrowhead = none ];
165 -> 36;

166 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
27 -> 166 [arrowhead = none ];
166 -> 29;

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

168 [label="BACKTRACK\nfor clause: p(0, 0)\nwith clash: (m(T12, 0, X5), m(0, X11, 0))", fontsize=14, style = filled, fillcolor = lightgreen];
40 -> 168 [arrowhead = none ];
168 -> 42;

169 [label="EVAL with clause\np(s(X34), X34).\nand substitutionX34 -> T15,\nT12 -> s(T15),\nX27 -> T15", fontsize=14, style = filled, fillcolor = lightblue];
42 -> 169 [arrowhead = none ];
169 -> 43;

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

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

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

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

174 [label="ONLY EVAL with clause\np(0, 0).\nand substitutionX28 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
49 -> 174 [arrowhead = none ];
174 -> 59;

175 [label="BACKTRACK\nfor clause: p(s(X), X)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
54 -> 175 [arrowhead = none ];
175 -> 137;

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

177 [label="ONLY EVAL with clause\nm(X41, 0, X41).\nand substitutionT15 -> T22,\nX41 -> T22,\nX29 -> T22", fontsize=14, style = filled, fillcolor = lightblue];
62 -> 177 [arrowhead = none ];
177 -> 76;

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

179 [label="EVAL with clause\nm(0, X44, 0) :- !_5.\nand substitutionT22 -> 0,\nX44 -> 0,\nX29 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
77 -> 179 [arrowhead = none ];
179 -> 84;

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

181 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
84 -> 181 [arrowhead = none ];
181 -> 86;

182 [label="ONLY EVAL with clause\nm(X57, X58, X59) :- ','(p(X57, X60), ','(p(X58, X61), m(X60, X61, X59))).\nand substitutionT22 -> T25,\nX57 -> T25,\nX58 -> 0,\nX29 -> X62,\nX59 -> X62", fontsize=14, style = filled, fillcolor = lightblue];
85 -> 182 [arrowhead = none ];
182 -> 112;

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

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

185 [label="BACKTRACK\nfor clause: p(0, 0)\nwith clash: (m(T25, 0, X29), m(0, X44, 0))", fontsize=14, style = filled, fillcolor = lightgreen];
114 -> 185 [arrowhead = none ];
185 -> 115;

186 [label="EVAL with clause\np(s(X67), X67).\nand substitutionX67 -> T28,\nT25 -> s(T28),\nX60 -> T28", fontsize=14, style = filled, fillcolor = lightblue];
115 -> 186 [arrowhead = none ];
186 -> 118;

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

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

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

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

191 [label="ONLY EVAL with clause\np(0, 0).\nand substitutionX61 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
124 -> 191 [arrowhead = none ];
191 -> 135;

192 [label="BACKTRACK\nfor clause: p(s(X), X)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
126 -> 192 [arrowhead = none ];
192 -> 136;

193 [label="INSTANCE with matching:\nT15 -> T28\nX29 -> X62", fontsize=14, style = filled, fillcolor = lightgrey];
135 -> 193 [arrowhead = none , style=dashed];
193 -> 59[style=dashed];

194 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
138 -> 194 [arrowhead = none ];
194 -> 140;

195 [label="ONLY EVAL with clause\nm(X89, X90, X91) :- ','(p(X89, X92), ','(p(X90, X93), m(X92, X93, X91))).\nand substitutionT5 -> T40,\nX89 -> T40,\nT6 -> T41,\nX90 -> T41,\nX5 -> X94,\nX91 -> X94", fontsize=14, style = filled, fillcolor = lightblue];
139 -> 195 [arrowhead = none ];
195 -> 145;

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

197 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
145 -> 197 [arrowhead = none ];
197 -> 146;

198 [label="BACKTRACK\nfor clause: p(0, 0)\nwith clash: (m(T40, T41, X5), m(0, X76, 0))", fontsize=14, style = filled, fillcolor = lightgreen];
146 -> 198 [arrowhead = none ];
198 -> 147;

199 [label="EVAL with clause\np(s(X99), X99).\nand substitutionX99 -> T44,\nT40 -> s(T44),\nX92 -> T44", fontsize=14, style = filled, fillcolor = lightblue];
147 -> 199 [arrowhead = none ];
199 -> 148;

200 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
147 -> 200 [arrowhead = none ];
200 -> 149;

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

202 [label="BACKTRACK\nfor clause: p(0, 0)\nwith clash: (m(s(T44), T41, X5), m(X8, 0, X8))", fontsize=14, style = filled, fillcolor = lightgreen];
150 -> 202 [arrowhead = none ];
202 -> 151;

203 [label="EVAL with clause\np(s(X103), X103).\nand substitutionX103 -> T48,\nT41 -> s(T48),\nX93 -> T48", fontsize=14, style = filled, fillcolor = lightblue];
151 -> 203 [arrowhead = none ];
203 -> 152;

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

205 [label="INSTANCE with matching:\nT5 -> T44\nT6 -> T48\nX5 -> X94", fontsize=14, style = filled, fillcolor = lightgrey];
152 -> 205 [arrowhead = none , style=dashed];
205 -> 7[style=dashed];

}

(2) Obligation:

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

qA_in_gg(T5, T6) → U1_gg(T5, T6, mB_in_gga(T5, T6, X5))
mB_in_gga(T9, 0, T9) → mB_out_gga(T9, 0, T9)
mB_in_gga(0, 0, 0) → mB_out_gga(0, 0, 0)
mB_in_gga(s(T15), 0, X29) → U3_gga(T15, X29, mC_in_ga(T15, X29))
mC_in_ga(T22, T22) → mC_out_ga(T22, T22)
mC_in_ga(0, 0) → mC_out_ga(0, 0)
mC_in_ga(s(T28), X62) → U2_ga(T28, X62, mC_in_ga(T28, X62))
U2_ga(T28, X62, mC_out_ga(T28, X62)) → mC_out_ga(s(T28), X62)
U3_gga(T15, X29, mC_out_ga(T15, X29)) → mB_out_gga(s(T15), 0, X29)
mB_in_gga(0, T35, 0) → mB_out_gga(0, T35, 0)
mB_in_gga(s(T44), s(T48), X94) → U4_gga(T44, T48, X94, mB_in_gga(T44, T48, X94))
U4_gga(T44, T48, X94, mB_out_gga(T44, T48, X94)) → mB_out_gga(s(T44), s(T48), X94)
U1_gg(T5, T6, mB_out_gga(T5, T6, X5)) → qA_out_gg(T5, T6)

The argument filtering Pi contains the following mapping:
qA_in_gg(x1, x2)  =  qA_in_gg(x1, x2)
U1_gg(x1, x2, x3)  =  U1_gg(x1, x2, x3)
mB_in_gga(x1, x2, x3)  =  mB_in_gga(x1, x2)
0  =  0
mB_out_gga(x1, x2, x3)  =  mB_out_gga(x1, x2, x3)
s(x1)  =  s(x1)
U3_gga(x1, x2, x3)  =  U3_gga(x1, x3)
mC_in_ga(x1, x2)  =  mC_in_ga(x1)
mC_out_ga(x1, x2)  =  mC_out_ga(x1, x2)
U2_ga(x1, x2, x3)  =  U2_ga(x1, x3)
U4_gga(x1, x2, x3, x4)  =  U4_gga(x1, x2, x4)
qA_out_gg(x1, x2)  =  qA_out_gg(x1, x2)

(3) DependencyPairsProof (EQUIVALENT transformation)

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

QA_IN_GG(T5, T6) → U1_GG(T5, T6, mB_in_gga(T5, T6, X5))
QA_IN_GG(T5, T6) → MB_IN_GGA(T5, T6, X5)
MB_IN_GGA(s(T15), 0, X29) → U3_GGA(T15, X29, mC_in_ga(T15, X29))
MB_IN_GGA(s(T15), 0, X29) → MC_IN_GA(T15, X29)
MC_IN_GA(s(T28), X62) → U2_GA(T28, X62, mC_in_ga(T28, X62))
MC_IN_GA(s(T28), X62) → MC_IN_GA(T28, X62)
MB_IN_GGA(s(T44), s(T48), X94) → U4_GGA(T44, T48, X94, mB_in_gga(T44, T48, X94))
MB_IN_GGA(s(T44), s(T48), X94) → MB_IN_GGA(T44, T48, X94)

The TRS R consists of the following rules:

qA_in_gg(T5, T6) → U1_gg(T5, T6, mB_in_gga(T5, T6, X5))
mB_in_gga(T9, 0, T9) → mB_out_gga(T9, 0, T9)
mB_in_gga(0, 0, 0) → mB_out_gga(0, 0, 0)
mB_in_gga(s(T15), 0, X29) → U3_gga(T15, X29, mC_in_ga(T15, X29))
mC_in_ga(T22, T22) → mC_out_ga(T22, T22)
mC_in_ga(0, 0) → mC_out_ga(0, 0)
mC_in_ga(s(T28), X62) → U2_ga(T28, X62, mC_in_ga(T28, X62))
U2_ga(T28, X62, mC_out_ga(T28, X62)) → mC_out_ga(s(T28), X62)
U3_gga(T15, X29, mC_out_ga(T15, X29)) → mB_out_gga(s(T15), 0, X29)
mB_in_gga(0, T35, 0) → mB_out_gga(0, T35, 0)
mB_in_gga(s(T44), s(T48), X94) → U4_gga(T44, T48, X94, mB_in_gga(T44, T48, X94))
U4_gga(T44, T48, X94, mB_out_gga(T44, T48, X94)) → mB_out_gga(s(T44), s(T48), X94)
U1_gg(T5, T6, mB_out_gga(T5, T6, X5)) → qA_out_gg(T5, T6)

The argument filtering Pi contains the following mapping:
qA_in_gg(x1, x2)  =  qA_in_gg(x1, x2)
U1_gg(x1, x2, x3)  =  U1_gg(x1, x2, x3)
mB_in_gga(x1, x2, x3)  =  mB_in_gga(x1, x2)
0  =  0
mB_out_gga(x1, x2, x3)  =  mB_out_gga(x1, x2, x3)
s(x1)  =  s(x1)
U3_gga(x1, x2, x3)  =  U3_gga(x1, x3)
mC_in_ga(x1, x2)  =  mC_in_ga(x1)
mC_out_ga(x1, x2)  =  mC_out_ga(x1, x2)
U2_ga(x1, x2, x3)  =  U2_ga(x1, x3)
U4_gga(x1, x2, x3, x4)  =  U4_gga(x1, x2, x4)
qA_out_gg(x1, x2)  =  qA_out_gg(x1, x2)
QA_IN_GG(x1, x2)  =  QA_IN_GG(x1, x2)
U1_GG(x1, x2, x3)  =  U1_GG(x1, x2, x3)
MB_IN_GGA(x1, x2, x3)  =  MB_IN_GGA(x1, x2)
U3_GGA(x1, x2, x3)  =  U3_GGA(x1, x3)
MC_IN_GA(x1, x2)  =  MC_IN_GA(x1)
U2_GA(x1, x2, x3)  =  U2_GA(x1, x3)
U4_GGA(x1, x2, x3, x4)  =  U4_GGA(x1, x2, x4)

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

(4) Obligation:

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

QA_IN_GG(T5, T6) → U1_GG(T5, T6, mB_in_gga(T5, T6, X5))
QA_IN_GG(T5, T6) → MB_IN_GGA(T5, T6, X5)
MB_IN_GGA(s(T15), 0, X29) → U3_GGA(T15, X29, mC_in_ga(T15, X29))
MB_IN_GGA(s(T15), 0, X29) → MC_IN_GA(T15, X29)
MC_IN_GA(s(T28), X62) → U2_GA(T28, X62, mC_in_ga(T28, X62))
MC_IN_GA(s(T28), X62) → MC_IN_GA(T28, X62)
MB_IN_GGA(s(T44), s(T48), X94) → U4_GGA(T44, T48, X94, mB_in_gga(T44, T48, X94))
MB_IN_GGA(s(T44), s(T48), X94) → MB_IN_GGA(T44, T48, X94)

The TRS R consists of the following rules:

qA_in_gg(T5, T6) → U1_gg(T5, T6, mB_in_gga(T5, T6, X5))
mB_in_gga(T9, 0, T9) → mB_out_gga(T9, 0, T9)
mB_in_gga(0, 0, 0) → mB_out_gga(0, 0, 0)
mB_in_gga(s(T15), 0, X29) → U3_gga(T15, X29, mC_in_ga(T15, X29))
mC_in_ga(T22, T22) → mC_out_ga(T22, T22)
mC_in_ga(0, 0) → mC_out_ga(0, 0)
mC_in_ga(s(T28), X62) → U2_ga(T28, X62, mC_in_ga(T28, X62))
U2_ga(T28, X62, mC_out_ga(T28, X62)) → mC_out_ga(s(T28), X62)
U3_gga(T15, X29, mC_out_ga(T15, X29)) → mB_out_gga(s(T15), 0, X29)
mB_in_gga(0, T35, 0) → mB_out_gga(0, T35, 0)
mB_in_gga(s(T44), s(T48), X94) → U4_gga(T44, T48, X94, mB_in_gga(T44, T48, X94))
U4_gga(T44, T48, X94, mB_out_gga(T44, T48, X94)) → mB_out_gga(s(T44), s(T48), X94)
U1_gg(T5, T6, mB_out_gga(T5, T6, X5)) → qA_out_gg(T5, T6)

The argument filtering Pi contains the following mapping:
qA_in_gg(x1, x2)  =  qA_in_gg(x1, x2)
U1_gg(x1, x2, x3)  =  U1_gg(x1, x2, x3)
mB_in_gga(x1, x2, x3)  =  mB_in_gga(x1, x2)
0  =  0
mB_out_gga(x1, x2, x3)  =  mB_out_gga(x1, x2, x3)
s(x1)  =  s(x1)
U3_gga(x1, x2, x3)  =  U3_gga(x1, x3)
mC_in_ga(x1, x2)  =  mC_in_ga(x1)
mC_out_ga(x1, x2)  =  mC_out_ga(x1, x2)
U2_ga(x1, x2, x3)  =  U2_ga(x1, x3)
U4_gga(x1, x2, x3, x4)  =  U4_gga(x1, x2, x4)
qA_out_gg(x1, x2)  =  qA_out_gg(x1, x2)
QA_IN_GG(x1, x2)  =  QA_IN_GG(x1, x2)
U1_GG(x1, x2, x3)  =  U1_GG(x1, x2, x3)
MB_IN_GGA(x1, x2, x3)  =  MB_IN_GGA(x1, x2)
U3_GGA(x1, x2, x3)  =  U3_GGA(x1, x3)
MC_IN_GA(x1, x2)  =  MC_IN_GA(x1)
U2_GA(x1, x2, x3)  =  U2_GA(x1, x3)
U4_GGA(x1, x2, x3, x4)  =  U4_GGA(x1, x2, x4)

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

(5) DependencyGraphProof (EQUIVALENT transformation)

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

(6) Complex Obligation (AND)

(7) Obligation:

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

MC_IN_GA(s(T28), X62) → MC_IN_GA(T28, X62)

The TRS R consists of the following rules:

qA_in_gg(T5, T6) → U1_gg(T5, T6, mB_in_gga(T5, T6, X5))
mB_in_gga(T9, 0, T9) → mB_out_gga(T9, 0, T9)
mB_in_gga(0, 0, 0) → mB_out_gga(0, 0, 0)
mB_in_gga(s(T15), 0, X29) → U3_gga(T15, X29, mC_in_ga(T15, X29))
mC_in_ga(T22, T22) → mC_out_ga(T22, T22)
mC_in_ga(0, 0) → mC_out_ga(0, 0)
mC_in_ga(s(T28), X62) → U2_ga(T28, X62, mC_in_ga(T28, X62))
U2_ga(T28, X62, mC_out_ga(T28, X62)) → mC_out_ga(s(T28), X62)
U3_gga(T15, X29, mC_out_ga(T15, X29)) → mB_out_gga(s(T15), 0, X29)
mB_in_gga(0, T35, 0) → mB_out_gga(0, T35, 0)
mB_in_gga(s(T44), s(T48), X94) → U4_gga(T44, T48, X94, mB_in_gga(T44, T48, X94))
U4_gga(T44, T48, X94, mB_out_gga(T44, T48, X94)) → mB_out_gga(s(T44), s(T48), X94)
U1_gg(T5, T6, mB_out_gga(T5, T6, X5)) → qA_out_gg(T5, T6)

The argument filtering Pi contains the following mapping:
qA_in_gg(x1, x2)  =  qA_in_gg(x1, x2)
U1_gg(x1, x2, x3)  =  U1_gg(x1, x2, x3)
mB_in_gga(x1, x2, x3)  =  mB_in_gga(x1, x2)
0  =  0
mB_out_gga(x1, x2, x3)  =  mB_out_gga(x1, x2, x3)
s(x1)  =  s(x1)
U3_gga(x1, x2, x3)  =  U3_gga(x1, x3)
mC_in_ga(x1, x2)  =  mC_in_ga(x1)
mC_out_ga(x1, x2)  =  mC_out_ga(x1, x2)
U2_ga(x1, x2, x3)  =  U2_ga(x1, x3)
U4_gga(x1, x2, x3, x4)  =  U4_gga(x1, x2, x4)
qA_out_gg(x1, x2)  =  qA_out_gg(x1, x2)
MC_IN_GA(x1, x2)  =  MC_IN_GA(x1)

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

(8) UsableRulesProof (EQUIVALENT transformation)

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

(9) Obligation:

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

MC_IN_GA(s(T28), X62) → MC_IN_GA(T28, X62)

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

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

(10) PiDPToQDPProof (SOUND transformation)

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

(11) Obligation:

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

MC_IN_GA(s(T28)) → MC_IN_GA(T28)

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:

• MC_IN_GA(s(T28)) → MC_IN_GA(T28)
  The graph contains the following edges 1 > 1

(13) YES

(14) Obligation:

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

MB_IN_GGA(s(T44), s(T48), X94) → MB_IN_GGA(T44, T48, X94)

The TRS R consists of the following rules:

qA_in_gg(T5, T6) → U1_gg(T5, T6, mB_in_gga(T5, T6, X5))
mB_in_gga(T9, 0, T9) → mB_out_gga(T9, 0, T9)
mB_in_gga(0, 0, 0) → mB_out_gga(0, 0, 0)
mB_in_gga(s(T15), 0, X29) → U3_gga(T15, X29, mC_in_ga(T15, X29))
mC_in_ga(T22, T22) → mC_out_ga(T22, T22)
mC_in_ga(0, 0) → mC_out_ga(0, 0)
mC_in_ga(s(T28), X62) → U2_ga(T28, X62, mC_in_ga(T28, X62))
U2_ga(T28, X62, mC_out_ga(T28, X62)) → mC_out_ga(s(T28), X62)
U3_gga(T15, X29, mC_out_ga(T15, X29)) → mB_out_gga(s(T15), 0, X29)
mB_in_gga(0, T35, 0) → mB_out_gga(0, T35, 0)
mB_in_gga(s(T44), s(T48), X94) → U4_gga(T44, T48, X94, mB_in_gga(T44, T48, X94))
U4_gga(T44, T48, X94, mB_out_gga(T44, T48, X94)) → mB_out_gga(s(T44), s(T48), X94)
U1_gg(T5, T6, mB_out_gga(T5, T6, X5)) → qA_out_gg(T5, T6)

The argument filtering Pi contains the following mapping:
qA_in_gg(x1, x2)  =  qA_in_gg(x1, x2)
U1_gg(x1, x2, x3)  =  U1_gg(x1, x2, x3)
mB_in_gga(x1, x2, x3)  =  mB_in_gga(x1, x2)
0  =  0
mB_out_gga(x1, x2, x3)  =  mB_out_gga(x1, x2, x3)
s(x1)  =  s(x1)
U3_gga(x1, x2, x3)  =  U3_gga(x1, x3)
mC_in_ga(x1, x2)  =  mC_in_ga(x1)
mC_out_ga(x1, x2)  =  mC_out_ga(x1, x2)
U2_ga(x1, x2, x3)  =  U2_ga(x1, x3)
U4_gga(x1, x2, x3, x4)  =  U4_gga(x1, x2, x4)
qA_out_gg(x1, x2)  =  qA_out_gg(x1, x2)
MB_IN_GGA(x1, x2, x3)  =  MB_IN_GGA(x1, x2)

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

(15) UsableRulesProof (EQUIVALENT transformation)

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

(16) Obligation:

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

MB_IN_GGA(s(T44), s(T48), X94) → MB_IN_GGA(T44, T48, X94)

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

MB_IN_GGA(s(T44), s(T48)) → MB_IN_GGA(T44, T48)

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:

• MB_IN_GGA(s(T44), s(T48)) → MB_IN_GGA(T44, T48)
  The graph contains the following edges 1 > 1, 2 > 2

(20) YES