Left Termination proof of /tmp/tmpGlflJB/binary3.pl

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

0 Prolog

↳1 PrologToPiTRSViaGraphTransformerProof (⇒, 572 ms)

↳2 PiTRS

↳3 DependencyPairsProof (⇔, 1852 ms)

↳4 PiDP

↳5 DependencyGraphProof (⇔, 39 ms)

↳6 AND

    ↳7 PiDP

        ↳8 UsableRulesProof (⇔, 0 ms)

        ↳9 PiDP

        ↳10 PiDPToQDPProof (⇔, 0 ms)

        ↳11 QDP

        ↳12 QDPSizeChangeProof (⇔, 0 ms)

        ↳13 YES

    ↳14 PiDP

        ↳15 UsableRulesProof (⇔, 0 ms)

        ↳16 PiDP

        ↳17 PiDPToQDPProof (⇒, 0 ms)

        ↳18 QDP

        ↳19 QDPSizeChangeProof (⇔, 0 ms)

        ↳20 YES

    ↳21 PiDP

        ↳22 UsableRulesProof (⇔, 0 ms)

        ↳23 PiDP

        ↳24 PiDPToQDPProof (⇒, 0 ms)

        ↳25 QDP

        ↳26 QDPSizeChangeProof (⇔, 0 ms)

        ↳27 YES

    ↳28 PiDP

        ↳29 UsableRulesProof (⇔, 0 ms)

        ↳30 PiDP

        ↳31 PiDPToQDPProof (⇒, 0 ms)

        ↳32 QDP

        ↳33 QDPSizeChangeProof (⇔, 0 ms)

        ↳34 YES

    ↳35 PiDP

        ↳36 UsableRulesProof (⇔, 0 ms)

        ↳37 PiDP

        ↳38 PiDPToQDPProof (⇒, 0 ms)

        ↳39 QDP

        ↳40 QDPSizeChangeProof (⇔, 0 ms)

        ↳41 YES

(0) Obligation:

Clauses:

add(b, b, b).
add(X, b, X) :- binaryZ(X).
add(b, Y, Y) :- binaryZ(Y).
add(X, Y, Z) :- addz(X, Y, Z).
addx(one(X), b, one(X)) :- binary(X).
addx(zero(X), b, zero(X)) :- binaryZ(X).
addx(X, Y, Z) :- addz(X, Y, Z).
addy(b, one(Y), one(Y)) :- binary(Y).
addy(b, zero(Y), zero(Y)) :- binaryZ(Y).
addy(X, Y, Z) :- addz(X, Y, Z).
addz(zero(X), zero(Y), zero(Z)) :- addz(X, Y, Z).
addz(zero(X), one(Y), one(Z)) :- addx(X, Y, Z).
addz(one(X), zero(Y), one(Z)) :- addy(X, Y, Z).
addz(one(X), one(Y), zero(Z)) :- addc(X, Y, Z).
addc(b, b, one(b)).
addc(X, b, Z) :- succZ(X, Z).
addc(b, Y, Z) :- succZ(Y, Z).
addc(X, Y, Z) :- addC(X, Y, Z).
addX(zero(X), b, one(X)) :- binaryZ(X).
addX(one(X), b, zero(Z)) :- succ(X, Z).
addX(X, Y, Z) :- addC(X, Y, Z).
addY(b, zero(Y), one(Y)) :- binaryZ(Y).
addY(b, one(Y), zero(Z)) :- succ(Y, Z).
addY(X, Y, Z) :- addC(X, Y, Z).
addC(zero(X), zero(Y), one(Z)) :- addz(X, Y, Z).
addC(zero(X), one(Y), zero(Z)) :- addX(X, Y, Z).
addC(one(X), zero(Y), zero(Z)) :- addY(X, Y, Z).
addC(one(X), one(Y), one(Z)) :- addc(X, Y, Z).
binary(b).
binary(zero(X)) :- binaryZ(X).
binary(one(X)) :- binary(X).
binaryZ(zero(X)) :- binaryZ(X).
binaryZ(one(X)) :- binary(X).
succ(b, one(b)).
succ(zero(X), one(X)) :- binaryZ(X).
succ(one(X), zero(Z)) :- succ(X, Z).
succZ(zero(X), one(X)) :- binaryZ(X).
succZ(one(X), zero(Z)) :- succ(X, Z).
times(one(b), X, X).
times(zero(R), S, zero(RS)) :- times(R, S, RS).
times(one(R), S, RSS) :- ','(times(R, S, RS), add(S, zero(RS), RSS)).

Query: times(g,g,a)

(1) PrologToPiTRSViaGraphTransformerProof (SOUND transformation)

Transformed Prolog program to (Pi-)TRS.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
3 [label="A: times(T1, T2, T3)\n\nT1 is ground\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
5 [label="5: times(T1, T2, T3), SCOPE: 1, CLAUSE: 38 | times(T1, T2, T3), SCOPE: 1, CLAUSE: 39 | times(T1, T2, T3), SCOPE: 1, CLAUSE: 40\n\nT1 is ground\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
9 [label="9: true | times(one(b), T5, T3), SCOPE: 1, CLAUSE: 39 | times(one(b), T5, T3), SCOPE: 1, CLAUSE: 40\n\nT5 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
14 [label="14: times(T1, T2, T3), SCOPE: 1, CLAUSE: 39 | times(T1, T2, T3), SCOPE: 1, CLAUSE: 40\n\nT1 is ground\nT2 is ground\nX2 is free\ntimes(T1, T2, T3) !=? times(one(b), X2, X2)", fontsize=16, style=filled, fillcolor=lightyellow];
16 [label="16: times(one(b), T5, T3), SCOPE: 1, CLAUSE: 39 | times(one(b), T5, T3), SCOPE: 1, CLAUSE: 40\n\nT5 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
19 [label="19: times(one(b), T5, T3), SCOPE: 1, CLAUSE: 40\n\nT5 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
32 [label="32: ','(times(b, T8, X12), add(T8, zero(X12), T10))\n\nT8 is ground\nX12 is free", fontsize=16, style=filled, fillcolor=lightyellow];
35 [label="35: ','(times(b, T8, X12), add(T8, zero(X12), T10)), SCOPE: 2, CLAUSE: 38 | ','(times(b, T8, X12), add(T8, zero(X12), T10)), SCOPE: 2, CLAUSE: 39 | ','(times(b, T8, X12), add(T8, zero(X12), T10)), SCOPE: 2, CLAUSE: 40\n\nT8 is ground\nX12 is free", fontsize=16, style=filled, fillcolor=lightyellow];
36 [label="36: ','(times(b, T8, X12), add(T8, zero(X12), T10)), SCOPE: 2, CLAUSE: 39 | ','(times(b, T8, X12), add(T8, zero(X12), T10)), SCOPE: 2, CLAUSE: 40\n\nT8 is ground\nX12 is free", fontsize=16, style=filled, fillcolor=lightyellow];
37 [label="37: ','(times(b, T8, X12), add(T8, zero(X12), T10)), SCOPE: 2, CLAUSE: 40\n\nT8 is ground\nX12 is free", fontsize=16, style=filled, fillcolor=lightyellow];
39 [label="39: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
42 [label="42: times(T14, T15, T17) | times(zero(T14), T15, T3), SCOPE: 1, CLAUSE: 40\n\nT14 is ground\nT15 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
49 [label="49: times(T1, T2, T3), SCOPE: 1, CLAUSE: 40\n\nT1 is ground\nT2 is ground\nX2 is free\nX23 is free\nX24 is free\nX25 is free\ntimes(T1, T2, T3) !=? times(one(b), X2, X2)\ntimes(T1, T2, T3) !=? times(zero(X23), X24, zero(X25))", fontsize=16, style=filled, fillcolor=lightyellow];
50 [label="50: times(T14, T15, T17), SCOPE: 3, CLAUSE: 38 | times(T14, T15, T17), SCOPE: 3, CLAUSE: 39 | times(T14, T15, T17), SCOPE: 3, CLAUSE: 40 | ?_3 | times(zero(T14), T15, T3), SCOPE: 1, CLAUSE: 40\n\nT14 is ground\nT15 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
51 [label="51: times(T14, T15, T17), SCOPE: 3, CLAUSE: 38\n\nT14 is ground\nT15 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
53 [label="53: times(T14, T15, T17), SCOPE: 3, CLAUSE: 39 | times(T14, T15, T17), SCOPE: 3, CLAUSE: 40 | ?_3 | times(zero(T14), T15, T3), SCOPE: 1, CLAUSE: 40\n\nT14 is ground\nT15 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
55 [label="55: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
56 [label="56: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
57 [label="57: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
62 [label="62: times(T14, T15, T17), SCOPE: 3, CLAUSE: 39\n\nT14 is ground\nT15 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
63 [label="63: times(T14, T15, T17), SCOPE: 3, CLAUSE: 40 | ?_3 | times(zero(T14), T15, T3), SCOPE: 1, CLAUSE: 40\n\nT14 is ground\nT15 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
64 [label="64: times(T35, T36, T38)\n\nT35 is ground\nT36 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
65 [label="65: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
81 [label="81: times(T14, T15, T17), SCOPE: 3, CLAUSE: 40\n\nT14 is ground\nT15 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
82 [label="82: ?_3 | times(zero(T14), T15, T3), SCOPE: 1, CLAUSE: 40\n\nT14 is ground\nT15 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
83 [label="B: ','(times(T53, T54, X65), add(T54, zero(X65), T56))\n\nT53 is ground\nT54 is ground\nX65 is free", fontsize=16, style=filled, fillcolor=lightyellow];
84 [label="84: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
96 [label="F: times(T53, T54, X65)\n\nT53 is ground\nT54 is ground\nX65 is free", fontsize=16, style=filled, fillcolor=lightyellow];
97 [label="C: add(T54, zero(T59), T56)\n\nT54 is ground\nT59 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
106 [label="106: times(T53, T54, X65), SCOPE: 4, CLAUSE: 38 | times(T53, T54, X65), SCOPE: 4, CLAUSE: 39 | times(T53, T54, X65), SCOPE: 4, CLAUSE: 40\n\nT53 is ground\nT54 is ground\nX65 is free", fontsize=16, style=filled, fillcolor=lightyellow];
110 [label="110: times(T53, T54, X65), SCOPE: 4, CLAUSE: 38\n\nT53 is ground\nT54 is ground\nX65 is free", fontsize=16, style=filled, fillcolor=lightyellow];
112 [label="112: times(T53, T54, X65), SCOPE: 4, CLAUSE: 39 | times(T53, T54, X65), SCOPE: 4, CLAUSE: 40\n\nT53 is ground\nT54 is ground\nX65 is free", fontsize=16, style=filled, fillcolor=lightyellow];
116 [label="116: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
117 [label="117: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
118 [label="118: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
121 [label="121: times(T53, T54, X65), SCOPE: 4, CLAUSE: 39\n\nT53 is ground\nT54 is ground\nX65 is free", fontsize=16, style=filled, fillcolor=lightyellow];
122 [label="122: times(T53, T54, X65), SCOPE: 4, CLAUSE: 40\n\nT53 is ground\nT54 is ground\nX65 is free", fontsize=16, style=filled, fillcolor=lightyellow];
131 [label="131: times(T75, T76, X94)\n\nT75 is ground\nT76 is ground\nX94 is free", fontsize=16, style=filled, fillcolor=lightyellow];
132 [label="132: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
176 [label="G: ','(times(T83, T84, X109), add(T84, zero(X109), X110))\n\nT83 is ground\nT84 is ground\nX110 is free\nX109 is free", fontsize=16, style=filled, fillcolor=lightyellow];
177 [label="177: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
187 [label="187: times(T83, T84, X109)\n\nT83 is ground\nT84 is ground\nX109 is free", fontsize=16, style=filled, fillcolor=lightyellow];
188 [label="188: add(T84, zero(T87), X110)\n\nT84 is ground\nT87 is ground\nX110 is free", fontsize=16, style=filled, fillcolor=lightyellow];
191 [label="191: add(T54, zero(T59), T56), SCOPE: 5, CLAUSE: 0 | add(T54, zero(T59), T56), SCOPE: 5, CLAUSE: 1 | add(T54, zero(T59), T56), SCOPE: 5, CLAUSE: 2 | add(T54, zero(T59), T56), SCOPE: 5, CLAUSE: 3\n\nT54 is ground\nT59 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
192 [label="192: add(T54, zero(T59), T56), SCOPE: 5, CLAUSE: 1 | add(T54, zero(T59), T56), SCOPE: 5, CLAUSE: 2 | add(T54, zero(T59), T56), SCOPE: 5, CLAUSE: 3\n\nT54 is ground\nT59 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
193 [label="193: add(T54, zero(T59), T56), SCOPE: 5, CLAUSE: 2 | add(T54, zero(T59), T56), SCOPE: 5, CLAUSE: 3\n\nT54 is ground\nT59 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
196 [label="196: add(T54, zero(T59), T56), SCOPE: 5, CLAUSE: 2\n\nT54 is ground\nT59 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
197 [label="197: add(T54, zero(T59), T56), SCOPE: 5, CLAUSE: 3\n\nT54 is ground\nT59 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
198 [label="198: binaryZ(zero(T95))\n\nT95 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
200 [label="200: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
202 [label="202: binaryZ(zero(T95)), SCOPE: 6, CLAUSE: 31 | binaryZ(zero(T95)), SCOPE: 6, CLAUSE: 32\n\nT95 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
204 [label="204: binaryZ(zero(T95)), SCOPE: 6, CLAUSE: 31\n\nT95 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
205 [label="205: binaryZ(zero(T95)), SCOPE: 6, CLAUSE: 32\n\nT95 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
208 [label="H: binaryZ(T103)\n\nT103 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
211 [label="211: binaryZ(T103), SCOPE: 7, CLAUSE: 31 | binaryZ(T103), SCOPE: 7, CLAUSE: 32\n\nT103 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
212 [label="212: binaryZ(T103), SCOPE: 7, CLAUSE: 31\n\nT103 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
213 [label="213: binaryZ(T103), SCOPE: 7, CLAUSE: 32\n\nT103 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
214 [label="214: binaryZ(T109)\n\nT109 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
215 [label="215: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
218 [label="K: binary(T113)\n\nT113 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
219 [label="219: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
221 [label="221: binary(T113), SCOPE: 8, CLAUSE: 28 | binary(T113), SCOPE: 8, CLAUSE: 29 | binary(T113), SCOPE: 8, CLAUSE: 30\n\nT113 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
222 [label="222: binary(T113), SCOPE: 8, CLAUSE: 28\n\nT113 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
223 [label="223: binary(T113), SCOPE: 8, CLAUSE: 29 | binary(T113), SCOPE: 8, CLAUSE: 30\n\nT113 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
226 [label="226: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
227 [label="227: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
228 [label="228: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
229 [label="229: binary(T113), SCOPE: 8, CLAUSE: 29\n\nT113 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
230 [label="230: binary(T113), SCOPE: 8, CLAUSE: 30\n\nT113 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
232 [label="232: binaryZ(T118)\n\nT118 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
234 [label="234: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
235 [label="235: binary(T122)\n\nT122 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
236 [label="236: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
239 [label="239: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
244 [label="244: addz(T133, zero(T134), T136)\n\nT133 is ground\nT134 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
246 [label="246: addz(T133, zero(T134), T136), SCOPE: 9, CLAUSE: 10 | addz(T133, zero(T134), T136), SCOPE: 9, CLAUSE: 11 | addz(T133, zero(T134), T136), SCOPE: 9, CLAUSE: 12 | addz(T133, zero(T134), T136), SCOPE: 9, CLAUSE: 13\n\nT133 is ground\nT134 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
248 [label="248: addz(T133, zero(T134), T136), SCOPE: 9, CLAUSE: 10\n\nT133 is ground\nT134 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
249 [label="249: addz(T133, zero(T134), T136), SCOPE: 9, CLAUSE: 11 | addz(T133, zero(T134), T136), SCOPE: 9, CLAUSE: 12 | addz(T133, zero(T134), T136), SCOPE: 9, CLAUSE: 13\n\nT133 is ground\nT134 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
253 [label="I: addz(T152, T153, T155)\n\nT152 is ground\nT153 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
254 [label="254: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
255 [label="255: addz(T152, T153, T155), SCOPE: 10, CLAUSE: 10 | addz(T152, T153, T155), SCOPE: 10, CLAUSE: 11 | addz(T152, T153, T155), SCOPE: 10, CLAUSE: 12 | addz(T152, T153, T155), SCOPE: 10, CLAUSE: 13\n\nT152 is ground\nT153 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
258 [label="258: addz(T152, T153, T155), SCOPE: 10, CLAUSE: 10\n\nT152 is ground\nT153 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
259 [label="259: addz(T152, T153, T155), SCOPE: 10, CLAUSE: 11 | addz(T152, T153, T155), SCOPE: 10, CLAUSE: 12 | addz(T152, T153, T155), SCOPE: 10, CLAUSE: 13\n\nT152 is ground\nT153 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
265 [label="265: addz(T171, T172, T174)\n\nT171 is ground\nT172 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
266 [label="266: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
272 [label="272: addz(T152, T153, T155), SCOPE: 10, CLAUSE: 11\n\nT152 is ground\nT153 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
274 [label="274: addz(T152, T153, T155), SCOPE: 10, CLAUSE: 12 | addz(T152, T153, T155), SCOPE: 10, CLAUSE: 13\n\nT152 is ground\nT153 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
276 [label="276: addx(T190, T191, T193)\n\nT190 is ground\nT191 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
279 [label="279: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
282 [label="282: addx(T190, T191, T193), SCOPE: 11, CLAUSE: 4 | addx(T190, T191, T193), SCOPE: 11, CLAUSE: 5 | addx(T190, T191, T193), SCOPE: 11, CLAUSE: 6\n\nT190 is ground\nT191 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
285 [label="285: addx(T190, T191, T193), SCOPE: 11, CLAUSE: 4\n\nT190 is ground\nT191 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
286 [label="286: addx(T190, T191, T193), SCOPE: 11, CLAUSE: 5 | addx(T190, T191, T193), SCOPE: 11, CLAUSE: 6\n\nT190 is ground\nT191 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
289 [label="289: binary(T199)\n\nT199 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
290 [label="290: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
291 [label="291: addx(T190, T191, T193), SCOPE: 11, CLAUSE: 5\n\nT190 is ground\nT191 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
292 [label="292: addx(T190, T191, T193), SCOPE: 11, CLAUSE: 6\n\nT190 is ground\nT191 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
294 [label="294: binaryZ(T204)\n\nT204 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
295 [label="295: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
298 [label="298: addz(T216, T217, T219)\n\nT216 is ground\nT217 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
319 [label="319: addz(T152, T153, T155), SCOPE: 10, CLAUSE: 12\n\nT152 is ground\nT153 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
320 [label="320: addz(T152, T153, T155), SCOPE: 10, CLAUSE: 13\n\nT152 is ground\nT153 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
328 [label="J: addy(T235, T236, T238)\n\nT235 is ground\nT236 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
330 [label="330: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
332 [label="332: addy(T235, T236, T238), SCOPE: 12, CLAUSE: 7 | addy(T235, T236, T238), SCOPE: 12, CLAUSE: 8 | addy(T235, T236, T238), SCOPE: 12, CLAUSE: 9\n\nT235 is ground\nT236 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
333 [label="333: addy(T235, T236, T238), SCOPE: 12, CLAUSE: 7\n\nT235 is ground\nT236 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
334 [label="334: addy(T235, T236, T238), SCOPE: 12, CLAUSE: 8 | addy(T235, T236, T238), SCOPE: 12, CLAUSE: 9\n\nT235 is ground\nT236 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
336 [label="336: binary(T244)\n\nT244 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
337 [label="337: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
338 [label="338: addy(T235, T236, T238), SCOPE: 12, CLAUSE: 8\n\nT235 is ground\nT236 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
339 [label="339: addy(T235, T236, T238), SCOPE: 12, CLAUSE: 9\n\nT235 is ground\nT236 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
340 [label="340: binaryZ(T249)\n\nT249 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
341 [label="341: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
356 [label="356: addz(T261, T262, T264)\n\nT261 is ground\nT262 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
370 [label="L: addc(T274, T275, T277)\n\nT274 is ground\nT275 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
371 [label="371: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
376 [label="376: addc(T274, T275, T277), SCOPE: 13, CLAUSE: 14 | addc(T274, T275, T277), SCOPE: 13, CLAUSE: 15 | addc(T274, T275, T277), SCOPE: 13, CLAUSE: 16 | addc(T274, T275, T277), SCOPE: 13, CLAUSE: 17\n\nT274 is ground\nT275 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
377 [label="377: addc(T274, T275, T277), SCOPE: 13, CLAUSE: 14\n\nT274 is ground\nT275 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
378 [label="378: addc(T274, T275, T277), SCOPE: 13, CLAUSE: 15 | addc(T274, T275, T277), SCOPE: 13, CLAUSE: 16 | addc(T274, T275, T277), SCOPE: 13, CLAUSE: 17\n\nT274 is ground\nT275 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
379 [label="379: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
380 [label="380: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
381 [label="381: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
384 [label="384: addc(T274, T275, T277), SCOPE: 13, CLAUSE: 15\n\nT274 is ground\nT275 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
385 [label="385: addc(T274, T275, T277), SCOPE: 13, CLAUSE: 16 | addc(T274, T275, T277), SCOPE: 13, CLAUSE: 17\n\nT274 is ground\nT275 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
388 [label="N: succZ(T286, T288)\n\nT286 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
389 [label="389: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
402 [label="402: succZ(T286, T288), SCOPE: 14, CLAUSE: 36 | succZ(T286, T288), SCOPE: 14, CLAUSE: 37\n\nT286 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
403 [label="403: succZ(T286, T288), SCOPE: 14, CLAUSE: 36\n\nT286 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
404 [label="404: succZ(T286, T288), SCOPE: 14, CLAUSE: 37\n\nT286 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
405 [label="405: binaryZ(T294)\n\nT294 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
406 [label="406: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
410 [label="M: succ(T300, T302)\n\nT300 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
411 [label="411: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
416 [label="416: succ(T300, T302), SCOPE: 15, CLAUSE: 33 | succ(T300, T302), SCOPE: 15, CLAUSE: 34 | succ(T300, T302), SCOPE: 15, CLAUSE: 35\n\nT300 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
418 [label="418: succ(T300, T302), SCOPE: 15, CLAUSE: 33\n\nT300 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
419 [label="419: succ(T300, T302), SCOPE: 15, CLAUSE: 34 | succ(T300, T302), SCOPE: 15, CLAUSE: 35\n\nT300 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
420 [label="420: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
421 [label="421: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
422 [label="422: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
423 [label="423: succ(T300, T302), SCOPE: 15, CLAUSE: 34\n\nT300 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
424 [label="424: succ(T300, T302), SCOPE: 15, CLAUSE: 35\n\nT300 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
427 [label="427: binaryZ(T307)\n\nT307 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
428 [label="428: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
432 [label="432: succ(T313, T315)\n\nT313 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
433 [label="433: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
438 [label="438: addc(T274, T275, T277), SCOPE: 13, CLAUSE: 16\n\nT274 is ground\nT275 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
439 [label="439: addc(T274, T275, T277), SCOPE: 13, CLAUSE: 17\n\nT274 is ground\nT275 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
441 [label="441: succZ(T324, T326)\n\nT324 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
442 [label="442: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
453 [label="O: addC(T338, T339, T341)\n\nT338 is ground\nT339 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
455 [label="455: addC(T338, T339, T341), SCOPE: 16, CLAUSE: 24 | addC(T338, T339, T341), SCOPE: 16, CLAUSE: 25 | addC(T338, T339, T341), SCOPE: 16, CLAUSE: 26 | addC(T338, T339, T341), SCOPE: 16, CLAUSE: 27\n\nT338 is ground\nT339 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
460 [label="460: addC(T338, T339, T341), SCOPE: 16, CLAUSE: 24\n\nT338 is ground\nT339 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
462 [label="462: addC(T338, T339, T341), SCOPE: 16, CLAUSE: 25 | addC(T338, T339, T341), SCOPE: 16, CLAUSE: 26 | addC(T338, T339, T341), SCOPE: 16, CLAUSE: 27\n\nT338 is ground\nT339 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
469 [label="469: addz(T357, T358, T360)\n\nT357 is ground\nT358 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
470 [label="470: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
475 [label="475: addC(T338, T339, T341), SCOPE: 16, CLAUSE: 25\n\nT338 is ground\nT339 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
476 [label="476: addC(T338, T339, T341), SCOPE: 16, CLAUSE: 26 | addC(T338, T339, T341), SCOPE: 16, CLAUSE: 27\n\nT338 is ground\nT339 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
478 [label="478: addX(T376, T377, T379)\n\nT376 is ground\nT377 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
479 [label="479: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
482 [label="482: addX(T376, T377, T379), SCOPE: 17, CLAUSE: 18 | addX(T376, T377, T379), SCOPE: 17, CLAUSE: 19 | addX(T376, T377, T379), SCOPE: 17, CLAUSE: 20\n\nT376 is ground\nT377 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
484 [label="484: addX(T376, T377, T379), SCOPE: 17, CLAUSE: 18\n\nT376 is ground\nT377 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
485 [label="485: addX(T376, T377, T379), SCOPE: 17, CLAUSE: 19 | addX(T376, T377, T379), SCOPE: 17, CLAUSE: 20\n\nT376 is ground\nT377 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
488 [label="488: binaryZ(T385)\n\nT385 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
489 [label="489: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
495 [label="495: addX(T376, T377, T379), SCOPE: 17, CLAUSE: 19\n\nT376 is ground\nT377 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
496 [label="496: addX(T376, T377, T379), SCOPE: 17, CLAUSE: 20\n\nT376 is ground\nT377 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
501 [label="501: succ(T395, T397)\n\nT395 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
502 [label="502: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
512 [label="512: addC(T408, T409, T411)\n\nT408 is ground\nT409 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
518 [label="518: addC(T338, T339, T341), SCOPE: 16, CLAUSE: 26\n\nT338 is ground\nT339 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
519 [label="519: addC(T338, T339, T341), SCOPE: 16, CLAUSE: 27\n\nT338 is ground\nT339 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
520 [label="520: addY(T427, T428, T430)\n\nT427 is ground\nT428 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
521 [label="521: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
523 [label="523: addY(T427, T428, T430), SCOPE: 18, CLAUSE: 21 | addY(T427, T428, T430), SCOPE: 18, CLAUSE: 22 | addY(T427, T428, T430), SCOPE: 18, CLAUSE: 23\n\nT427 is ground\nT428 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
526 [label="526: addY(T427, T428, T430), SCOPE: 18, CLAUSE: 21\n\nT427 is ground\nT428 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
527 [label="527: addY(T427, T428, T430), SCOPE: 18, CLAUSE: 22 | addY(T427, T428, T430), SCOPE: 18, CLAUSE: 23\n\nT427 is ground\nT428 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
529 [label="529: binaryZ(T436)\n\nT436 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
530 [label="530: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
535 [label="535: addY(T427, T428, T430), SCOPE: 18, CLAUSE: 22\n\nT427 is ground\nT428 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
536 [label="536: addY(T427, T428, T430), SCOPE: 18, CLAUSE: 23\n\nT427 is ground\nT428 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
540 [label="540: succ(T446, T448)\n\nT446 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
543 [label="543: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
550 [label="550: addC(T459, T460, T462)\n\nT459 is ground\nT460 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
558 [label="558: addc(T472, T473, T475)\n\nT472 is ground\nT473 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
559 [label="559: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
560 [label="560: addz(T133, zero(T134), T136), SCOPE: 9, CLAUSE: 12 | addz(T133, zero(T134), T136), SCOPE: 9, CLAUSE: 13\n\nT133 is ground\nT134 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
563 [label="563: addz(T133, zero(T134), T136), SCOPE: 9, CLAUSE: 12\n\nT133 is ground\nT134 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
564 [label="564: addz(T133, zero(T134), T136), SCOPE: 9, CLAUSE: 13\n\nT133 is ground\nT134 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
567 [label="567: addy(T489, T490, T492)\n\nT489 is ground\nT490 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
568 [label="568: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
569 [label="569: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
570 [label="570: times(zero(T14), T15, T3), SCOPE: 1, CLAUSE: 40\n\nT14 is ground\nT15 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
572 [label="572: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
574 [label="574: ','(times(T498, T499, X506), add(T499, zero(X506), T501))\n\nT498 is ground\nT499 is ground\nX2 is free\nX506 is free\ntimes(one(T498), T499, T3) !=? times(one(b), X2, X2)", fontsize=16, style=filled, fillcolor=lightyellow];
575 [label="575: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
576 [label="576: ','(times(T498, T499, X506), add(T499, zero(X506), T501)), SCOPE: 19, CLAUSE: 38 | ','(times(T498, T499, X506), add(T499, zero(X506), T501)), SCOPE: 19, CLAUSE: 39 | ','(times(T498, T499, X506), add(T499, zero(X506), T501)), SCOPE: 19, CLAUSE: 40\n\nT498 is ground\nT499 is ground\nX2 is free\nX506 is free\ntimes(one(T498), T499, T3) !=? times(one(b), X2, X2)", fontsize=16, style=filled, fillcolor=lightyellow];
577 [label="577: ','(times(T498, T499, X506), add(T499, zero(X506), T501)), SCOPE: 19, CLAUSE: 38\n\nT498 is ground\nT499 is ground\nX2 is free\nX506 is free\ntimes(one(T498), T499, T3) !=? times(one(b), X2, X2)", fontsize=16, style=filled, fillcolor=lightyellow];
578 [label="578: ','(times(T498, T499, X506), add(T499, zero(X506), T501)), SCOPE: 19, CLAUSE: 39 | ','(times(T498, T499, X506), add(T499, zero(X506), T501)), SCOPE: 19, CLAUSE: 40\n\nT498 is ground\nT499 is ground\nX2 is free\nX506 is free\ntimes(one(T498), T499, T3) !=? times(one(b), X2, X2)", fontsize=16, style=filled, fillcolor=lightyellow];
579 [label="579: add(T506, zero(T506), T501)\n\nT506 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
580 [label="580: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
583 [label="583: ','(times(T498, T499, X506), add(T499, zero(X506), T501)), SCOPE: 19, CLAUSE: 39\n\nT498 is ground\nT499 is ground\nX2 is free\nX506 is free\ntimes(one(T498), T499, T3) !=? times(one(b), X2, X2)", fontsize=16, style=filled, fillcolor=lightyellow];
584 [label="584: ','(times(T498, T499, X506), add(T499, zero(X506), T501)), SCOPE: 19, CLAUSE: 40\n\nT498 is ground\nT499 is ground\nX2 is free\nX506 is free\ntimes(one(T498), T499, T3) !=? times(one(b), X2, X2)", fontsize=16, style=filled, fillcolor=lightyellow];
587 [label="D: ','(times(T515, T516, X531), add(T516, zero(zero(X531)), T501))\n\nT515 is ground\nT516 is ground\nX531 is free", fontsize=16, style=filled, fillcolor=lightyellow];
588 [label="588: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
591 [label="591: times(T515, T516, X531)\n\nT515 is ground\nT516 is ground\nX531 is free", fontsize=16, style=filled, fillcolor=lightyellow];
592 [label="592: add(T516, zero(zero(T519)), T501)\n\nT516 is ground\nT519 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
593 [label="E: ','(','(times(T526, T527, X548), add(T527, zero(X548), X549)), add(T527, zero(X549), T501))\n\nT526 is ground\nT527 is ground\nX549 is free\nX548 is free", fontsize=16, style=filled, fillcolor=lightyellow];
594 [label="594: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
595 [label="595: times(T526, T527, X548)\n\nT526 is ground\nT527 is ground\nX548 is free", fontsize=16, style=filled, fillcolor=lightyellow];
596 [label="P: ','(add(T527, zero(T530), X549), add(T527, zero(X549), T501))\n\nT527 is ground\nT530 is ground\nX549 is free", fontsize=16, style=filled, fillcolor=lightyellow];
597 [label="597: add(T527, zero(T530), X549)\n\nT527 is ground\nT530 is ground\nX549 is free", fontsize=16, style=filled, fillcolor=lightyellow];
598 [label="598: add(T527, zero(T533), T501)\n\nT527 is ground\nT533 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
599 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
3 -> 599 [arrowhead = none ];
599 -> 5;

600 [label="EVAL with clause\ntimes(one(b), X2, X2).\nand substitutionT1 -> one(b),\nT2 -> T5,\nX2 -> T5,\nT3 -> T5", fontsize=14, style = filled, fillcolor = lightblue];
5 -> 600 [arrowhead = none ];
600 -> 9;

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

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

603 [label="EVAL with clause\ntimes(zero(X23), X24, zero(X25)) :- times(X23, X24, X25).\nand substitutionX23 -> T14,\nT1 -> zero(T14),\nT2 -> T15,\nX24 -> T15,\nX25 -> T17,\nT3 -> zero(T17),\nT16 -> T17", fontsize=14, style = filled, fillcolor = lightblue];
14 -> 603 [arrowhead = none ];
603 -> 42;

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

605 [label="BACKTRACK\nfor clause: times(zero(R), S, zero(RS)) :- times(R, S, RS)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
16 -> 605 [arrowhead = none ];
605 -> 19;

606 [label="ONLY EVAL with clause\ntimes(one(X9), X10, X11) :- ','(times(X9, X10, X12), add(X10, zero(X12), X11)).\nand substitutionX9 -> b,\nT5 -> T8,\nX10 -> T8,\nT3 -> T10,\nX11 -> T10,\nT9 -> T10", fontsize=14, style = filled, fillcolor = lightblue];
19 -> 606 [arrowhead = none ];
606 -> 32;

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

608 [label="BACKTRACK\nfor clause: times(one(b), X, X)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
35 -> 608 [arrowhead = none ];
608 -> 36;

609 [label="BACKTRACK\nfor clause: times(zero(R), S, zero(RS)) :- times(R, S, RS)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
36 -> 609 [arrowhead = none ];
609 -> 37;

610 [label="BACKTRACK\nfor clause: times(one(R), S, RSS) :- ','(times(R, S, RS), add(S, zero(RS), RSS))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
37 -> 610 [arrowhead = none ];
610 -> 39;

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

612 [label="EVAL with clause\ntimes(one(X503), X504, X505) :- ','(times(X503, X504, X506), add(X504, zero(X506), X505)).\nand substitutionX503 -> T498,\nT1 -> one(T498),\nT2 -> T499,\nX504 -> T499,\nT3 -> T501,\nX505 -> T501,\nT500 -> T501", fontsize=14, style = filled, fillcolor = lightblue];
49 -> 612 [arrowhead = none ];
612 -> 574;

613 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
49 -> 613 [arrowhead = none ];
613 -> 575;

614 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
50 -> 614 [arrowhead = none ];
614 -> 51;

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

616 [label="EVAL with clause\ntimes(one(b), X30, X30).\nand substitutionT14 -> one(b),\nT15 -> T22,\nX30 -> T22,\nT17 -> T22", fontsize=14, style = filled, fillcolor = lightblue];
51 -> 616 [arrowhead = none ];
616 -> 55;

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

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

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

620 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
55 -> 620 [arrowhead = none ];
620 -> 57;

621 [label="EVAL with clause\ntimes(zero(X43), X44, zero(X45)) :- times(X43, X44, X45).\nand substitutionX43 -> T35,\nT14 -> zero(T35),\nT15 -> T36,\nX44 -> T36,\nX45 -> T38,\nT17 -> zero(T38),\nT37 -> T38", fontsize=14, style = filled, fillcolor = lightblue];
62 -> 621 [arrowhead = none ];
621 -> 64;

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

623 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
63 -> 623 [arrowhead = none ];
623 -> 81;

624 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
63 -> 624 [arrowhead = none ];
624 -> 82;

625 [label="INSTANCE with matching:\nT1 -> T35\nT2 -> T36\nT3 -> T38", fontsize=14, style = filled, fillcolor = lightgrey];
64 -> 625 [arrowhead = none , style=dashed];
625 -> 3[style=dashed];

626 [label="EVAL with clause\ntimes(one(X62), X63, X64) :- ','(times(X62, X63, X65), add(X63, zero(X65), X64)).\nand substitutionX62 -> T53,\nT14 -> one(T53),\nT15 -> T54,\nX63 -> T54,\nT17 -> T56,\nX64 -> T56,\nT55 -> T56", fontsize=14, style = filled, fillcolor = lightblue];
81 -> 626 [arrowhead = none ];
626 -> 83;

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

628 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
82 -> 628 [arrowhead = none ];
628 -> 570;

629 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
83 -> 629 [arrowhead = none ];
629 -> 96;

630 [label="SPLIT 2\nnew knowledge:\nT53 is ground\nT54 is ground\nT59 is ground\nreplacements:X65 -> T59", fontsize=14, style = filled, fillcolor = violet];
83 -> 630 [arrowhead = none ];
630 -> 97;

631 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
96 -> 631 [arrowhead = none ];
631 -> 106;

632 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
97 -> 632 [arrowhead = none ];
632 -> 191;

633 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
106 -> 633 [arrowhead = none ];
633 -> 110;

634 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
106 -> 634 [arrowhead = none ];
634 -> 112;

635 [label="EVAL with clause\ntimes(one(b), X74, X74).\nand substitutionT53 -> one(b),\nT54 -> T66,\nX74 -> T66,\nX65 -> T66", fontsize=14, style = filled, fillcolor = lightblue];
110 -> 635 [arrowhead = none ];
635 -> 116;

636 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
110 -> 636 [arrowhead = none ];
636 -> 117;

637 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
112 -> 637 [arrowhead = none ];
637 -> 121;

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

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

640 [label="EVAL with clause\ntimes(zero(X91), X92, zero(X93)) :- times(X91, X92, X93).\nand substitutionX91 -> T75,\nT53 -> zero(T75),\nT54 -> T76,\nX92 -> T76,\nX93 -> X94,\nX65 -> zero(X94)", fontsize=14, style = filled, fillcolor = lightblue];
121 -> 640 [arrowhead = none ];
640 -> 131;

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

642 [label="EVAL with clause\ntimes(one(X106), X107, X108) :- ','(times(X106, X107, X109), add(X107, zero(X109), X108)).\nand substitutionX106 -> T83,\nT53 -> one(T83),\nT54 -> T84,\nX107 -> T84,\nX65 -> X110,\nX108 -> X110", fontsize=14, style = filled, fillcolor = lightblue];
122 -> 642 [arrowhead = none ];
642 -> 176;

643 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
122 -> 643 [arrowhead = none ];
643 -> 177;

644 [label="INSTANCE with matching:\nT53 -> T75\nT54 -> T76\nX65 -> X94", fontsize=14, style = filled, fillcolor = lightgrey];
131 -> 644 [arrowhead = none , style=dashed];
644 -> 96[style=dashed];

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

646 [label="SPLIT 2\nnew knowledge:\nT83 is ground\nT84 is ground\nT87 is ground\nreplacements:X109 -> T87", fontsize=14, style = filled, fillcolor = violet];
176 -> 646 [arrowhead = none ];
646 -> 188;

647 [label="INSTANCE with matching:\nT53 -> T83\nT54 -> T84\nX65 -> X109", fontsize=14, style = filled, fillcolor = lightgrey];
187 -> 647 [arrowhead = none , style=dashed];
647 -> 96[style=dashed];

648 [label="INSTANCE with matching:\nT54 -> T84\nT59 -> T87\nT56 -> X110", fontsize=14, style = filled, fillcolor = lightgrey];
188 -> 648 [arrowhead = none , style=dashed];
648 -> 97[style=dashed];

649 [label="BACKTRACK\nfor clause: add(b, b, b)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
191 -> 649 [arrowhead = none ];
649 -> 192;

650 [label="BACKTRACK\nfor clause: add(X, b, X) :- binaryZ(X)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
192 -> 650 [arrowhead = none ];
650 -> 193;

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

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

653 [label="EVAL with clause\nadd(b, X120, X120) :- binaryZ(X120).\nand substitutionT54 -> b,\nT59 -> T95,\nX120 -> zero(T95),\nT56 -> zero(T95)", fontsize=14, style = filled, fillcolor = lightblue];
196 -> 653 [arrowhead = none ];
653 -> 198;

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

655 [label="ONLY EVAL with clause\nadd(X158, X159, X160) :- addz(X158, X159, X160).\nand substitutionT54 -> T133,\nX158 -> T133,\nT59 -> T134,\nX159 -> zero(T134),\nT56 -> T136,\nX160 -> T136,\nT135 -> T136", fontsize=14, style = filled, fillcolor = lightblue];
197 -> 655 [arrowhead = none ];
655 -> 244;

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

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

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

659 [label="ONLY EVAL with clause\nbinaryZ(zero(X128)) :- binaryZ(X128).\nand substitutionT95 -> T103,\nX128 -> T103", fontsize=14, style = filled, fillcolor = lightblue];
204 -> 659 [arrowhead = none ];
659 -> 208;

660 [label="BACKTRACK\nfor clause: binaryZ(one(X)) :- binary(X)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
205 -> 660 [arrowhead = none ];
660 -> 239;

661 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
208 -> 661 [arrowhead = none ];
661 -> 211;

662 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
211 -> 662 [arrowhead = none ];
662 -> 212;

663 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
211 -> 663 [arrowhead = none ];
663 -> 213;

664 [label="EVAL with clause\nbinaryZ(zero(X134)) :- binaryZ(X134).\nand substitutionX134 -> T109,\nT103 -> zero(T109)", fontsize=14, style = filled, fillcolor = lightblue];
212 -> 664 [arrowhead = none ];
664 -> 214;

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

666 [label="EVAL with clause\nbinaryZ(one(X138)) :- binary(X138).\nand substitutionX138 -> T113,\nT103 -> one(T113)", fontsize=14, style = filled, fillcolor = lightblue];
213 -> 666 [arrowhead = none ];
666 -> 218;

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

668 [label="INSTANCE with matching:\nT103 -> T109", fontsize=14, style = filled, fillcolor = lightgrey];
214 -> 668 [arrowhead = none , style=dashed];
668 -> 208[style=dashed];

669 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
218 -> 669 [arrowhead = none ];
669 -> 221;

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

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

672 [label="EVAL with clause\nbinary(b).\nand substitutionT113 -> b", fontsize=14, style = filled, fillcolor = lightblue];
222 -> 672 [arrowhead = none ];
672 -> 226;

673 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
222 -> 673 [arrowhead = none ];
673 -> 227;

674 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
223 -> 674 [arrowhead = none ];
674 -> 229;

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

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

677 [label="EVAL with clause\nbinary(zero(X143)) :- binaryZ(X143).\nand substitutionX143 -> T118,\nT113 -> zero(T118)", fontsize=14, style = filled, fillcolor = lightblue];
229 -> 677 [arrowhead = none ];
677 -> 232;

678 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
229 -> 678 [arrowhead = none ];
678 -> 234;

679 [label="EVAL with clause\nbinary(one(X147)) :- binary(X147).\nand substitutionX147 -> T122,\nT113 -> one(T122)", fontsize=14, style = filled, fillcolor = lightblue];
230 -> 679 [arrowhead = none ];
679 -> 235;

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

681 [label="INSTANCE with matching:\nT103 -> T118", fontsize=14, style = filled, fillcolor = lightgrey];
232 -> 681 [arrowhead = none , style=dashed];
681 -> 208[style=dashed];

682 [label="INSTANCE with matching:\nT113 -> T122", fontsize=14, style = filled, fillcolor = lightgrey];
235 -> 682 [arrowhead = none , style=dashed];
682 -> 218[style=dashed];

683 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
244 -> 683 [arrowhead = none ];
683 -> 246;

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

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

686 [label="EVAL with clause\naddz(zero(X176), zero(X177), zero(X178)) :- addz(X176, X177, X178).\nand substitutionX176 -> T152,\nT133 -> zero(T152),\nT134 -> T153,\nX177 -> T153,\nX178 -> T155,\nT136 -> zero(T155),\nT154 -> T155", fontsize=14, style = filled, fillcolor = lightblue];
248 -> 686 [arrowhead = none ];
686 -> 253;

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

688 [label="BACKTRACK\nfor clause: addz(zero(X), one(Y), one(Z)) :- addx(X, Y, Z)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
249 -> 688 [arrowhead = none ];
688 -> 560;

689 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
253 -> 689 [arrowhead = none ];
689 -> 255;

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

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

692 [label="EVAL with clause\naddz(zero(X194), zero(X195), zero(X196)) :- addz(X194, X195, X196).\nand substitutionX194 -> T171,\nT152 -> zero(T171),\nX195 -> T172,\nT153 -> zero(T172),\nX196 -> T174,\nT155 -> zero(T174),\nT173 -> T174", fontsize=14, style = filled, fillcolor = lightblue];
258 -> 692 [arrowhead = none ];
692 -> 265;

693 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
258 -> 693 [arrowhead = none ];
693 -> 266;

694 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
259 -> 694 [arrowhead = none ];
694 -> 272;

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

696 [label="INSTANCE with matching:\nT152 -> T171\nT153 -> T172\nT155 -> T174", fontsize=14, style = filled, fillcolor = lightgrey];
265 -> 696 [arrowhead = none , style=dashed];
696 -> 253[style=dashed];

697 [label="EVAL with clause\naddz(zero(X212), one(X213), one(X214)) :- addx(X212, X213, X214).\nand substitutionX212 -> T190,\nT152 -> zero(T190),\nX213 -> T191,\nT153 -> one(T191),\nX214 -> T193,\nT155 -> one(T193),\nT192 -> T193", fontsize=14, style = filled, fillcolor = lightblue];
272 -> 697 [arrowhead = none ];
697 -> 276;

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

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

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

701 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
276 -> 701 [arrowhead = none ];
701 -> 282;

702 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
282 -> 702 [arrowhead = none ];
702 -> 285;

703 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
282 -> 703 [arrowhead = none ];
703 -> 286;

704 [label="EVAL with clause\naddx(one(X220), b, one(X220)) :- binary(X220).\nand substitutionX220 -> T199,\nT190 -> one(T199),\nT191 -> b,\nT193 -> one(T199)", fontsize=14, style = filled, fillcolor = lightblue];
285 -> 704 [arrowhead = none ];
704 -> 289;

705 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
285 -> 705 [arrowhead = none ];
705 -> 290;

706 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
286 -> 706 [arrowhead = none ];
706 -> 291;

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

708 [label="INSTANCE with matching:\nT113 -> T199", fontsize=14, style = filled, fillcolor = lightgrey];
289 -> 708 [arrowhead = none , style=dashed];
708 -> 218[style=dashed];

709 [label="EVAL with clause\naddx(zero(X225), b, zero(X225)) :- binaryZ(X225).\nand substitutionX225 -> T204,\nT190 -> zero(T204),\nT191 -> b,\nT193 -> zero(T204)", fontsize=14, style = filled, fillcolor = lightblue];
291 -> 709 [arrowhead = none ];
709 -> 294;

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

711 [label="ONLY EVAL with clause\naddx(X236, X237, X238) :- addz(X236, X237, X238).\nand substitutionT190 -> T216,\nX236 -> T216,\nT191 -> T217,\nX237 -> T217,\nT193 -> T219,\nX238 -> T219,\nT218 -> T219", fontsize=14, style = filled, fillcolor = lightblue];
292 -> 711 [arrowhead = none ];
711 -> 298;

712 [label="INSTANCE with matching:\nT103 -> T204", fontsize=14, style = filled, fillcolor = lightgrey];
294 -> 712 [arrowhead = none , style=dashed];
712 -> 208[style=dashed];

713 [label="INSTANCE with matching:\nT152 -> T216\nT153 -> T217\nT155 -> T219", fontsize=14, style = filled, fillcolor = lightgrey];
298 -> 713 [arrowhead = none , style=dashed];
713 -> 253[style=dashed];

714 [label="EVAL with clause\naddz(one(X254), zero(X255), one(X256)) :- addy(X254, X255, X256).\nand substitutionX254 -> T235,\nT152 -> one(T235),\nX255 -> T236,\nT153 -> zero(T236),\nX256 -> T238,\nT155 -> one(T238),\nT237 -> T238", fontsize=14, style = filled, fillcolor = lightblue];
319 -> 714 [arrowhead = none ];
714 -> 328;

715 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
319 -> 715 [arrowhead = none ];
715 -> 330;

716 [label="EVAL with clause\naddz(one(X290), one(X291), zero(X292)) :- addc(X290, X291, X292).\nand substitutionX290 -> T274,\nT152 -> one(T274),\nX291 -> T275,\nT153 -> one(T275),\nX292 -> T277,\nT155 -> zero(T277),\nT276 -> T277", fontsize=14, style = filled, fillcolor = lightblue];
320 -> 716 [arrowhead = none ];
716 -> 370;

717 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
320 -> 717 [arrowhead = none ];
717 -> 371;

718 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
328 -> 718 [arrowhead = none ];
718 -> 332;

719 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
332 -> 719 [arrowhead = none ];
719 -> 333;

720 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
332 -> 720 [arrowhead = none ];
720 -> 334;

721 [label="EVAL with clause\naddy(b, one(X262), one(X262)) :- binary(X262).\nand substitutionT235 -> b,\nX262 -> T244,\nT236 -> one(T244),\nT238 -> one(T244)", fontsize=14, style = filled, fillcolor = lightblue];
333 -> 721 [arrowhead = none ];
721 -> 336;

722 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
333 -> 722 [arrowhead = none ];
722 -> 337;

723 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
334 -> 723 [arrowhead = none ];
723 -> 338;

724 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
334 -> 724 [arrowhead = none ];
724 -> 339;

725 [label="INSTANCE with matching:\nT113 -> T244", fontsize=14, style = filled, fillcolor = lightgrey];
336 -> 725 [arrowhead = none , style=dashed];
725 -> 218[style=dashed];

726 [label="EVAL with clause\naddy(b, zero(X267), zero(X267)) :- binaryZ(X267).\nand substitutionT235 -> b,\nX267 -> T249,\nT236 -> zero(T249),\nT238 -> zero(T249)", fontsize=14, style = filled, fillcolor = lightblue];
338 -> 726 [arrowhead = none ];
726 -> 340;

727 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
338 -> 727 [arrowhead = none ];
727 -> 341;

728 [label="ONLY EVAL with clause\naddy(X278, X279, X280) :- addz(X278, X279, X280).\nand substitutionT235 -> T261,\nX278 -> T261,\nT236 -> T262,\nX279 -> T262,\nT238 -> T264,\nX280 -> T264,\nT263 -> T264", fontsize=14, style = filled, fillcolor = lightblue];
339 -> 728 [arrowhead = none ];
728 -> 356;

729 [label="INSTANCE with matching:\nT103 -> T249", fontsize=14, style = filled, fillcolor = lightgrey];
340 -> 729 [arrowhead = none , style=dashed];
729 -> 208[style=dashed];

730 [label="INSTANCE with matching:\nT152 -> T261\nT153 -> T262\nT155 -> T264", fontsize=14, style = filled, fillcolor = lightgrey];
356 -> 730 [arrowhead = none , style=dashed];
730 -> 253[style=dashed];

731 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
370 -> 731 [arrowhead = none ];
731 -> 376;

732 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
376 -> 732 [arrowhead = none ];
732 -> 377;

733 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
376 -> 733 [arrowhead = none ];
733 -> 378;

734 [label="EVAL with clause\naddc(b, b, one(b)).\nand substitutionT274 -> b,\nT275 -> b,\nT277 -> one(b)", fontsize=14, style = filled, fillcolor = lightblue];
377 -> 734 [arrowhead = none ];
734 -> 379;

735 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
377 -> 735 [arrowhead = none ];
735 -> 380;

736 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
378 -> 736 [arrowhead = none ];
736 -> 384;

737 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
378 -> 737 [arrowhead = none ];
737 -> 385;

738 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
379 -> 738 [arrowhead = none ];
738 -> 381;

739 [label="EVAL with clause\naddc(X301, b, X302) :- succZ(X301, X302).\nand substitutionT274 -> T286,\nX301 -> T286,\nT275 -> b,\nT277 -> T288,\nX302 -> T288,\nT287 -> T288", fontsize=14, style = filled, fillcolor = lightblue];
384 -> 739 [arrowhead = none ];
739 -> 388;

740 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
384 -> 740 [arrowhead = none ];
740 -> 389;

741 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
385 -> 741 [arrowhead = none ];
741 -> 438;

742 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
385 -> 742 [arrowhead = none ];
742 -> 439;

743 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
388 -> 743 [arrowhead = none ];
743 -> 402;

744 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
402 -> 744 [arrowhead = none ];
744 -> 403;

745 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
402 -> 745 [arrowhead = none ];
745 -> 404;

746 [label="EVAL with clause\nsuccZ(zero(X308), one(X308)) :- binaryZ(X308).\nand substitutionX308 -> T294,\nT286 -> zero(T294),\nT288 -> one(T294)", fontsize=14, style = filled, fillcolor = lightblue];
403 -> 746 [arrowhead = none ];
746 -> 405;

747 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
403 -> 747 [arrowhead = none ];
747 -> 406;

748 [label="EVAL with clause\nsuccZ(one(X314), zero(X315)) :- succ(X314, X315).\nand substitutionX314 -> T300,\nT286 -> one(T300),\nX315 -> T302,\nT288 -> zero(T302),\nT301 -> T302", fontsize=14, style = filled, fillcolor = lightblue];
404 -> 748 [arrowhead = none ];
748 -> 410;

749 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
404 -> 749 [arrowhead = none ];
749 -> 411;

750 [label="INSTANCE with matching:\nT103 -> T294", fontsize=14, style = filled, fillcolor = lightgrey];
405 -> 750 [arrowhead = none , style=dashed];
750 -> 208[style=dashed];

751 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
410 -> 751 [arrowhead = none ];
751 -> 416;

752 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
416 -> 752 [arrowhead = none ];
752 -> 418;

753 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
416 -> 753 [arrowhead = none ];
753 -> 419;

754 [label="EVAL with clause\nsucc(b, one(b)).\nand substitutionT300 -> b,\nT302 -> one(b)", fontsize=14, style = filled, fillcolor = lightblue];
418 -> 754 [arrowhead = none ];
754 -> 420;

755 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
418 -> 755 [arrowhead = none ];
755 -> 421;

756 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
419 -> 756 [arrowhead = none ];
756 -> 423;

757 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
419 -> 757 [arrowhead = none ];
757 -> 424;

758 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
420 -> 758 [arrowhead = none ];
758 -> 422;

759 [label="EVAL with clause\nsucc(zero(X320), one(X320)) :- binaryZ(X320).\nand substitutionX320 -> T307,\nT300 -> zero(T307),\nT302 -> one(T307)", fontsize=14, style = filled, fillcolor = lightblue];
423 -> 759 [arrowhead = none ];
759 -> 427;

760 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
423 -> 760 [arrowhead = none ];
760 -> 428;

761 [label="EVAL with clause\nsucc(one(X326), zero(X327)) :- succ(X326, X327).\nand substitutionX326 -> T313,\nT300 -> one(T313),\nX327 -> T315,\nT302 -> zero(T315),\nT314 -> T315", fontsize=14, style = filled, fillcolor = lightblue];
424 -> 761 [arrowhead = none ];
761 -> 432;

762 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
424 -> 762 [arrowhead = none ];
762 -> 433;

763 [label="INSTANCE with matching:\nT103 -> T307", fontsize=14, style = filled, fillcolor = lightgrey];
427 -> 763 [arrowhead = none , style=dashed];
763 -> 208[style=dashed];

764 [label="INSTANCE with matching:\nT300 -> T313\nT302 -> T315", fontsize=14, style = filled, fillcolor = lightgrey];
432 -> 764 [arrowhead = none , style=dashed];
764 -> 410[style=dashed];

765 [label="EVAL with clause\naddc(b, X336, X337) :- succZ(X336, X337).\nand substitutionT274 -> b,\nT275 -> T324,\nX336 -> T324,\nT277 -> T326,\nX337 -> T326,\nT325 -> T326", fontsize=14, style = filled, fillcolor = lightblue];
438 -> 765 [arrowhead = none ];
765 -> 441;

766 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
438 -> 766 [arrowhead = none ];
766 -> 442;

767 [label="ONLY EVAL with clause\naddc(X348, X349, X350) :- addC(X348, X349, X350).\nand substitutionT274 -> T338,\nX348 -> T338,\nT275 -> T339,\nX349 -> T339,\nT277 -> T341,\nX350 -> T341,\nT340 -> T341", fontsize=14, style = filled, fillcolor = lightblue];
439 -> 767 [arrowhead = none ];
767 -> 453;

768 [label="INSTANCE with matching:\nT286 -> T324\nT288 -> T326", fontsize=14, style = filled, fillcolor = lightgrey];
441 -> 768 [arrowhead = none , style=dashed];
768 -> 388[style=dashed];

769 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
453 -> 769 [arrowhead = none ];
769 -> 455;

770 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
455 -> 770 [arrowhead = none ];
770 -> 460;

771 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
455 -> 771 [arrowhead = none ];
771 -> 462;

772 [label="EVAL with clause\naddC(zero(X366), zero(X367), one(X368)) :- addz(X366, X367, X368).\nand substitutionX366 -> T357,\nT338 -> zero(T357),\nX367 -> T358,\nT339 -> zero(T358),\nX368 -> T360,\nT341 -> one(T360),\nT359 -> T360", fontsize=14, style = filled, fillcolor = lightblue];
460 -> 772 [arrowhead = none ];
772 -> 469;

773 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
460 -> 773 [arrowhead = none ];
773 -> 470;

774 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
462 -> 774 [arrowhead = none ];
774 -> 475;

775 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
462 -> 775 [arrowhead = none ];
775 -> 476;

776 [label="INSTANCE with matching:\nT152 -> T357\nT153 -> T358\nT155 -> T360", fontsize=14, style = filled, fillcolor = lightgrey];
469 -> 776 [arrowhead = none , style=dashed];
776 -> 253[style=dashed];

777 [label="EVAL with clause\naddC(zero(X384), one(X385), zero(X386)) :- addX(X384, X385, X386).\nand substitutionX384 -> T376,\nT338 -> zero(T376),\nX385 -> T377,\nT339 -> one(T377),\nX386 -> T379,\nT341 -> zero(T379),\nT378 -> T379", fontsize=14, style = filled, fillcolor = lightblue];
475 -> 777 [arrowhead = none ];
777 -> 478;

778 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
475 -> 778 [arrowhead = none ];
778 -> 479;

779 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
476 -> 779 [arrowhead = none ];
779 -> 518;

780 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
476 -> 780 [arrowhead = none ];
780 -> 519;

781 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
478 -> 781 [arrowhead = none ];
781 -> 482;

782 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
482 -> 782 [arrowhead = none ];
782 -> 484;

783 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
482 -> 783 [arrowhead = none ];
783 -> 485;

784 [label="EVAL with clause\naddX(zero(X392), b, one(X392)) :- binaryZ(X392).\nand substitutionX392 -> T385,\nT376 -> zero(T385),\nT377 -> b,\nT379 -> one(T385)", fontsize=14, style = filled, fillcolor = lightblue];
484 -> 784 [arrowhead = none ];
784 -> 488;

785 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
484 -> 785 [arrowhead = none ];
785 -> 489;

786 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
485 -> 786 [arrowhead = none ];
786 -> 495;

787 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
485 -> 787 [arrowhead = none ];
787 -> 496;

788 [label="INSTANCE with matching:\nT103 -> T385", fontsize=14, style = filled, fillcolor = lightgrey];
488 -> 788 [arrowhead = none , style=dashed];
788 -> 208[style=dashed];

789 [label="EVAL with clause\naddX(one(X402), b, zero(X403)) :- succ(X402, X403).\nand substitutionX402 -> T395,\nT376 -> one(T395),\nT377 -> b,\nX403 -> T397,\nT379 -> zero(T397),\nT396 -> T397", fontsize=14, style = filled, fillcolor = lightblue];
495 -> 789 [arrowhead = none ];
789 -> 501;

790 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
495 -> 790 [arrowhead = none ];
790 -> 502;

791 [label="ONLY EVAL with clause\naddX(X413, X414, X415) :- addC(X413, X414, X415).\nand substitutionT376 -> T408,\nX413 -> T408,\nT377 -> T409,\nX414 -> T409,\nT379 -> T411,\nX415 -> T411,\nT410 -> T411", fontsize=14, style = filled, fillcolor = lightblue];
496 -> 791 [arrowhead = none ];
791 -> 512;

792 [label="INSTANCE with matching:\nT300 -> T395\nT302 -> T397", fontsize=14, style = filled, fillcolor = lightgrey];
501 -> 792 [arrowhead = none , style=dashed];
792 -> 410[style=dashed];

793 [label="INSTANCE with matching:\nT338 -> T408\nT339 -> T409\nT341 -> T411", fontsize=14, style = filled, fillcolor = lightgrey];
512 -> 793 [arrowhead = none , style=dashed];
793 -> 453[style=dashed];

794 [label="EVAL with clause\naddC(one(X431), zero(X432), zero(X433)) :- addY(X431, X432, X433).\nand substitutionX431 -> T427,\nT338 -> one(T427),\nX432 -> T428,\nT339 -> zero(T428),\nX433 -> T430,\nT341 -> zero(T430),\nT429 -> T430", fontsize=14, style = filled, fillcolor = lightblue];
518 -> 794 [arrowhead = none ];
794 -> 520;

795 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
518 -> 795 [arrowhead = none ];
795 -> 521;

796 [label="EVAL with clause\naddC(one(X472), one(X473), one(X474)) :- addc(X472, X473, X474).\nand substitutionX472 -> T472,\nT338 -> one(T472),\nX473 -> T473,\nT339 -> one(T473),\nX474 -> T475,\nT341 -> one(T475),\nT474 -> T475", fontsize=14, style = filled, fillcolor = lightblue];
519 -> 796 [arrowhead = none ];
796 -> 558;

797 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
519 -> 797 [arrowhead = none ];
797 -> 559;

798 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
520 -> 798 [arrowhead = none ];
798 -> 523;

799 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
523 -> 799 [arrowhead = none ];
799 -> 526;

800 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
523 -> 800 [arrowhead = none ];
800 -> 527;

801 [label="EVAL with clause\naddY(b, zero(X439), one(X439)) :- binaryZ(X439).\nand substitutionT427 -> b,\nX439 -> T436,\nT428 -> zero(T436),\nT430 -> one(T436)", fontsize=14, style = filled, fillcolor = lightblue];
526 -> 801 [arrowhead = none ];
801 -> 529;

802 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
526 -> 802 [arrowhead = none ];
802 -> 530;

803 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
527 -> 803 [arrowhead = none ];
803 -> 535;

804 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
527 -> 804 [arrowhead = none ];
804 -> 536;

805 [label="INSTANCE with matching:\nT103 -> T436", fontsize=14, style = filled, fillcolor = lightgrey];
529 -> 805 [arrowhead = none , style=dashed];
805 -> 208[style=dashed];

806 [label="EVAL with clause\naddY(b, one(X449), zero(X450)) :- succ(X449, X450).\nand substitutionT427 -> b,\nX449 -> T446,\nT428 -> one(T446),\nX450 -> T448,\nT430 -> zero(T448),\nT447 -> T448", fontsize=14, style = filled, fillcolor = lightblue];
535 -> 806 [arrowhead = none ];
806 -> 540;

807 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
535 -> 807 [arrowhead = none ];
807 -> 543;

808 [label="ONLY EVAL with clause\naddY(X460, X461, X462) :- addC(X460, X461, X462).\nand substitutionT427 -> T459,\nX460 -> T459,\nT428 -> T460,\nX461 -> T460,\nT430 -> T462,\nX462 -> T462,\nT461 -> T462", fontsize=14, style = filled, fillcolor = lightblue];
536 -> 808 [arrowhead = none ];
808 -> 550;

809 [label="INSTANCE with matching:\nT300 -> T446\nT302 -> T448", fontsize=14, style = filled, fillcolor = lightgrey];
540 -> 809 [arrowhead = none , style=dashed];
809 -> 410[style=dashed];

810 [label="INSTANCE with matching:\nT338 -> T459\nT339 -> T460\nT341 -> T462", fontsize=14, style = filled, fillcolor = lightgrey];
550 -> 810 [arrowhead = none , style=dashed];
810 -> 453[style=dashed];

811 [label="INSTANCE with matching:\nT274 -> T472\nT275 -> T473\nT277 -> T475", fontsize=14, style = filled, fillcolor = lightgrey];
558 -> 811 [arrowhead = none , style=dashed];
811 -> 370[style=dashed];

812 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
560 -> 812 [arrowhead = none ];
812 -> 563;

813 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
560 -> 813 [arrowhead = none ];
813 -> 564;

814 [label="EVAL with clause\naddz(one(X490), zero(X491), one(X492)) :- addy(X490, X491, X492).\nand substitutionX490 -> T489,\nT133 -> one(T489),\nT134 -> T490,\nX491 -> T490,\nX492 -> T492,\nT136 -> one(T492),\nT491 -> T492", fontsize=14, style = filled, fillcolor = lightblue];
563 -> 814 [arrowhead = none ];
814 -> 567;

815 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
563 -> 815 [arrowhead = none ];
815 -> 568;

816 [label="BACKTRACK\nfor clause: addz(one(X), one(Y), zero(Z)) :- addc(X, Y, Z)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
564 -> 816 [arrowhead = none ];
816 -> 569;

817 [label="INSTANCE with matching:\nT235 -> T489\nT236 -> T490\nT238 -> T492", fontsize=14, style = filled, fillcolor = lightgrey];
567 -> 817 [arrowhead = none , style=dashed];
817 -> 328[style=dashed];

818 [label="BACKTRACK\nfor clause: times(one(R), S, RSS) :- ','(times(R, S, RS), add(S, zero(RS), RSS))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
570 -> 818 [arrowhead = none ];
818 -> 572;

819 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
574 -> 819 [arrowhead = none ];
819 -> 576;

820 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
576 -> 820 [arrowhead = none ];
820 -> 577;

821 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
576 -> 821 [arrowhead = none ];
821 -> 578;

822 [label="EVAL with clause\ntimes(one(b), X511, X511).\nand substitutionT498 -> one(b),\nT499 -> T506,\nX511 -> T506,\nX506 -> T506", fontsize=14, style = filled, fillcolor = lightblue];
577 -> 822 [arrowhead = none ];
822 -> 579;

823 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
577 -> 823 [arrowhead = none ];
823 -> 580;

824 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
578 -> 824 [arrowhead = none ];
824 -> 583;

825 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
578 -> 825 [arrowhead = none ];
825 -> 584;

826 [label="INSTANCE with matching:\nT54 -> T506\nT59 -> T506\nT56 -> T501", fontsize=14, style = filled, fillcolor = lightgrey];
579 -> 826 [arrowhead = none , style=dashed];
826 -> 97[style=dashed];

827 [label="EVAL with clause\ntimes(zero(X528), X529, zero(X530)) :- times(X528, X529, X530).\nand substitutionX528 -> T515,\nT498 -> zero(T515),\nT499 -> T516,\nX529 -> T516,\nX530 -> X531,\nX506 -> zero(X531)", fontsize=14, style = filled, fillcolor = lightblue];
583 -> 827 [arrowhead = none ];
827 -> 587;

828 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
583 -> 828 [arrowhead = none ];
828 -> 588;

829 [label="EVAL with clause\ntimes(one(X545), X546, X547) :- ','(times(X545, X546, X548), add(X546, zero(X548), X547)).\nand substitutionX545 -> T526,\nT498 -> one(T526),\nT499 -> T527,\nX546 -> T527,\nX506 -> X549,\nX547 -> X549", fontsize=14, style = filled, fillcolor = lightblue];
584 -> 829 [arrowhead = none ];
829 -> 593;

830 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
584 -> 830 [arrowhead = none ];
830 -> 594;

831 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
587 -> 831 [arrowhead = none ];
831 -> 591;

832 [label="SPLIT 2\nnew knowledge:\nT515 is ground\nT516 is ground\nT519 is ground\nreplacements:X531 -> T519", fontsize=14, style = filled, fillcolor = violet];
587 -> 832 [arrowhead = none ];
832 -> 592;

833 [label="INSTANCE with matching:\nT53 -> T515\nT54 -> T516\nX65 -> X531", fontsize=14, style = filled, fillcolor = lightgrey];
591 -> 833 [arrowhead = none , style=dashed];
833 -> 96[style=dashed];

834 [label="INSTANCE with matching:\nT54 -> T516\nT59 -> zero(T519)\nT56 -> T501", fontsize=14, style = filled, fillcolor = lightgrey];
592 -> 834 [arrowhead = none , style=dashed];
834 -> 97[style=dashed];

835 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
593 -> 835 [arrowhead = none ];
835 -> 595;

836 [label="SPLIT 2\nnew knowledge:\nT526 is ground\nT527 is ground\nT530 is ground\nreplacements:X548 -> T530", fontsize=14, style = filled, fillcolor = violet];
593 -> 836 [arrowhead = none ];
836 -> 596;

837 [label="INSTANCE with matching:\nT53 -> T526\nT54 -> T527\nX65 -> X548", fontsize=14, style = filled, fillcolor = lightgrey];
595 -> 837 [arrowhead = none , style=dashed];
837 -> 96[style=dashed];

838 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
596 -> 838 [arrowhead = none ];
838 -> 597;

839 [label="SPLIT 2\nnew knowledge:\nT527 is ground\nT530 is ground\nT533 is ground\nreplacements:X549 -> T533", fontsize=14, style = filled, fillcolor = violet];
596 -> 839 [arrowhead = none ];
839 -> 598;

840 [label="INSTANCE with matching:\nT54 -> T527\nT59 -> T530\nT56 -> X549", fontsize=14, style = filled, fillcolor = lightgrey];
597 -> 840 [arrowhead = none , style=dashed];
840 -> 97[style=dashed];

841 [label="INSTANCE with matching:\nT54 -> T527\nT59 -> T533\nT56 -> T501", fontsize=14, style = filled, fillcolor = lightgrey];
598 -> 841 [arrowhead = none , style=dashed];
841 -> 97[style=dashed];

}

(2) Obligation:

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

timesA_in_gga(one(b), T5, T5) → timesA_out_gga(one(b), T5, T5)
timesA_in_gga(zero(one(b)), T22, zero(T22)) → timesA_out_gga(zero(one(b)), T22, zero(T22))
timesA_in_gga(zero(zero(T35)), T36, zero(zero(T38))) → U1_gga(T35, T36, T38, timesA_in_gga(T35, T36, T38))
timesA_in_gga(zero(one(T53)), T54, zero(T56)) → U2_gga(T53, T54, T56, pB_in_ggaa(T53, T54, X65, T56))
pB_in_ggaa(T53, T54, T59, T56) → U39_ggaa(T53, T54, T59, T56, timesF_in_gga(T53, T54, T59))
timesF_in_gga(one(b), T66, T66) → timesF_out_gga(one(b), T66, T66)
timesF_in_gga(zero(T75), T76, zero(X94)) → U6_gga(T75, T76, X94, timesF_in_gga(T75, T76, X94))
timesF_in_gga(one(T83), T84, X110) → U7_gga(T83, T84, X110, pG_in_ggaa(T83, T84, X109, X110))
pG_in_ggaa(T83, T84, T87, X110) → U41_ggaa(T83, T84, T87, X110, timesF_in_gga(T83, T84, T87))
U41_ggaa(T83, T84, T87, X110, timesF_out_gga(T83, T84, T87)) → U42_ggaa(T83, T84, T87, X110, addC1_in_gga(T84, T87, X110))
addC1_in_gga(b, T103, zero(T103)) → U8_gga(T103, binaryZH_in_g(T103))
binaryZH_in_g(zero(T109)) → U11_g(T109, binaryZH_in_g(T109))
binaryZH_in_g(one(T113)) → U12_g(T113, binaryK_in_g(T113))
binaryK_in_g(b) → binaryK_out_g(b)
binaryK_in_g(zero(T118)) → U13_g(T118, binaryZH_in_g(T118))
U13_g(T118, binaryZH_out_g(T118)) → binaryK_out_g(zero(T118))
binaryK_in_g(one(T122)) → U14_g(T122, binaryK_in_g(T122))
U14_g(T122, binaryK_out_g(T122)) → binaryK_out_g(one(T122))
U12_g(T113, binaryK_out_g(T113)) → binaryZH_out_g(one(T113))
U11_g(T109, binaryZH_out_g(T109)) → binaryZH_out_g(zero(T109))
U8_gga(T103, binaryZH_out_g(T103)) → addC1_out_gga(b, T103, zero(T103))
addC1_in_gga(zero(T152), T153, zero(T155)) → U9_gga(T152, T153, T155, addzI_in_gga(T152, T153, T155))
addzI_in_gga(zero(T171), zero(T172), zero(T174)) → U15_gga(T171, T172, T174, addzI_in_gga(T171, T172, T174))
addzI_in_gga(zero(one(T199)), one(b), one(one(T199))) → U16_gga(T199, binaryK_in_g(T199))
U16_gga(T199, binaryK_out_g(T199)) → addzI_out_gga(zero(one(T199)), one(b), one(one(T199)))
addzI_in_gga(zero(zero(T204)), one(b), one(zero(T204))) → U17_gga(T204, binaryZH_in_g(T204))
U17_gga(T204, binaryZH_out_g(T204)) → addzI_out_gga(zero(zero(T204)), one(b), one(zero(T204)))
addzI_in_gga(zero(T216), one(T217), one(T219)) → U18_gga(T216, T217, T219, addzI_in_gga(T216, T217, T219))
addzI_in_gga(one(T235), zero(T236), one(T238)) → U19_gga(T235, T236, T238, addyJ_in_gga(T235, T236, T238))
addyJ_in_gga(b, one(T244), one(T244)) → U36_gga(T244, binaryK_in_g(T244))
U36_gga(T244, binaryK_out_g(T244)) → addyJ_out_gga(b, one(T244), one(T244))
addyJ_in_gga(b, zero(T249), zero(T249)) → U37_gga(T249, binaryZH_in_g(T249))
U37_gga(T249, binaryZH_out_g(T249)) → addyJ_out_gga(b, zero(T249), zero(T249))
addyJ_in_gga(T261, T262, T264) → U38_gga(T261, T262, T264, addzI_in_gga(T261, T262, T264))
addzI_in_gga(one(T274), one(T275), zero(T277)) → U20_gga(T274, T275, T277, addcL_in_gga(T274, T275, T277))
addcL_in_gga(b, b, one(b)) → addcL_out_gga(b, b, one(b))
addcL_in_gga(T286, b, T288) → U33_gga(T286, T288, succZN_in_ga(T286, T288))
succZN_in_ga(zero(T294), one(T294)) → U23_ga(T294, binaryZH_in_g(T294))
U23_ga(T294, binaryZH_out_g(T294)) → succZN_out_ga(zero(T294), one(T294))
succZN_in_ga(one(T300), zero(T302)) → U24_ga(T300, T302, succM_in_ga(T300, T302))
succM_in_ga(b, one(b)) → succM_out_ga(b, one(b))
succM_in_ga(zero(T307), one(T307)) → U21_ga(T307, binaryZH_in_g(T307))
U21_ga(T307, binaryZH_out_g(T307)) → succM_out_ga(zero(T307), one(T307))
succM_in_ga(one(T313), zero(T315)) → U22_ga(T313, T315, succM_in_ga(T313, T315))
U22_ga(T313, T315, succM_out_ga(T313, T315)) → succM_out_ga(one(T313), zero(T315))
U24_ga(T300, T302, succM_out_ga(T300, T302)) → succZN_out_ga(one(T300), zero(T302))
U33_gga(T286, T288, succZN_out_ga(T286, T288)) → addcL_out_gga(T286, b, T288)
addcL_in_gga(b, T324, T326) → U34_gga(T324, T326, succZN_in_ga(T324, T326))
U34_gga(T324, T326, succZN_out_ga(T324, T326)) → addcL_out_gga(b, T324, T326)
addcL_in_gga(T338, T339, T341) → U35_gga(T338, T339, T341, addCO_in_gga(T338, T339, T341))
addCO_in_gga(zero(T357), zero(T358), one(T360)) → U25_gga(T357, T358, T360, addzI_in_gga(T357, T358, T360))
U25_gga(T357, T358, T360, addzI_out_gga(T357, T358, T360)) → addCO_out_gga(zero(T357), zero(T358), one(T360))
addCO_in_gga(zero(zero(T385)), one(b), zero(one(T385))) → U26_gga(T385, binaryZH_in_g(T385))
U26_gga(T385, binaryZH_out_g(T385)) → addCO_out_gga(zero(zero(T385)), one(b), zero(one(T385)))
addCO_in_gga(zero(one(T395)), one(b), zero(zero(T397))) → U27_gga(T395, T397, succM_in_ga(T395, T397))
U27_gga(T395, T397, succM_out_ga(T395, T397)) → addCO_out_gga(zero(one(T395)), one(b), zero(zero(T397)))
addCO_in_gga(zero(T408), one(T409), zero(T411)) → U28_gga(T408, T409, T411, addCO_in_gga(T408, T409, T411))
addCO_in_gga(one(b), zero(zero(T436)), zero(one(T436))) → U29_gga(T436, binaryZH_in_g(T436))
U29_gga(T436, binaryZH_out_g(T436)) → addCO_out_gga(one(b), zero(zero(T436)), zero(one(T436)))
addCO_in_gga(one(b), zero(one(T446)), zero(zero(T448))) → U30_gga(T446, T448, succM_in_ga(T446, T448))
U30_gga(T446, T448, succM_out_ga(T446, T448)) → addCO_out_gga(one(b), zero(one(T446)), zero(zero(T448)))
addCO_in_gga(one(T459), zero(T460), zero(T462)) → U31_gga(T459, T460, T462, addCO_in_gga(T459, T460, T462))
addCO_in_gga(one(T472), one(T473), one(T475)) → U32_gga(T472, T473, T475, addcL_in_gga(T472, T473, T475))
U32_gga(T472, T473, T475, addcL_out_gga(T472, T473, T475)) → addCO_out_gga(one(T472), one(T473), one(T475))
U31_gga(T459, T460, T462, addCO_out_gga(T459, T460, T462)) → addCO_out_gga(one(T459), zero(T460), zero(T462))
U28_gga(T408, T409, T411, addCO_out_gga(T408, T409, T411)) → addCO_out_gga(zero(T408), one(T409), zero(T411))
U35_gga(T338, T339, T341, addCO_out_gga(T338, T339, T341)) → addcL_out_gga(T338, T339, T341)
U20_gga(T274, T275, T277, addcL_out_gga(T274, T275, T277)) → addzI_out_gga(one(T274), one(T275), zero(T277))
U38_gga(T261, T262, T264, addzI_out_gga(T261, T262, T264)) → addyJ_out_gga(T261, T262, T264)
U19_gga(T235, T236, T238, addyJ_out_gga(T235, T236, T238)) → addzI_out_gga(one(T235), zero(T236), one(T238))
U18_gga(T216, T217, T219, addzI_out_gga(T216, T217, T219)) → addzI_out_gga(zero(T216), one(T217), one(T219))
U15_gga(T171, T172, T174, addzI_out_gga(T171, T172, T174)) → addzI_out_gga(zero(T171), zero(T172), zero(T174))
U9_gga(T152, T153, T155, addzI_out_gga(T152, T153, T155)) → addC1_out_gga(zero(T152), T153, zero(T155))
addC1_in_gga(one(T489), T490, one(T492)) → U10_gga(T489, T490, T492, addyJ_in_gga(T489, T490, T492))
U10_gga(T489, T490, T492, addyJ_out_gga(T489, T490, T492)) → addC1_out_gga(one(T489), T490, one(T492))
U42_ggaa(T83, T84, T87, X110, addC1_out_gga(T84, T87, X110)) → pG_out_ggaa(T83, T84, T87, X110)
U7_gga(T83, T84, X110, pG_out_ggaa(T83, T84, X109, X110)) → timesF_out_gga(one(T83), T84, X110)
U6_gga(T75, T76, X94, timesF_out_gga(T75, T76, X94)) → timesF_out_gga(zero(T75), T76, zero(X94))
U39_ggaa(T53, T54, T59, T56, timesF_out_gga(T53, T54, T59)) → U40_ggaa(T53, T54, T59, T56, addC1_in_gga(T54, T59, T56))
U40_ggaa(T53, T54, T59, T56, addC1_out_gga(T54, T59, T56)) → pB_out_ggaa(T53, T54, T59, T56)
U2_gga(T53, T54, T56, pB_out_ggaa(T53, T54, X65, T56)) → timesA_out_gga(zero(one(T53)), T54, zero(T56))
timesA_in_gga(one(one(b)), T506, T501) → U3_gga(T506, T501, addC1_in_gga(T506, T506, T501))
U3_gga(T506, T501, addC1_out_gga(T506, T506, T501)) → timesA_out_gga(one(one(b)), T506, T501)
timesA_in_gga(one(zero(T515)), T516, T501) → U4_gga(T515, T516, T501, pD_in_ggaa(T515, T516, X531, T501))
pD_in_ggaa(T515, T516, T519, T501) → U43_ggaa(T515, T516, T519, T501, timesF_in_gga(T515, T516, T519))
U43_ggaa(T515, T516, T519, T501, timesF_out_gga(T515, T516, T519)) → U44_ggaa(T515, T516, T519, T501, addC1_in_gga(T516, zero(T519), T501))
U44_ggaa(T515, T516, T519, T501, addC1_out_gga(T516, zero(T519), T501)) → pD_out_ggaa(T515, T516, T519, T501)
U4_gga(T515, T516, T501, pD_out_ggaa(T515, T516, X531, T501)) → timesA_out_gga(one(zero(T515)), T516, T501)
timesA_in_gga(one(one(T526)), T527, T501) → U5_gga(T526, T527, T501, pE_in_ggaaa(T526, T527, X548, X549, T501))
pE_in_ggaaa(T526, T527, T530, X549, T501) → U45_ggaaa(T526, T527, T530, X549, T501, timesF_in_gga(T526, T527, T530))
U45_ggaaa(T526, T527, T530, X549, T501, timesF_out_gga(T526, T527, T530)) → U46_ggaaa(T526, T527, T530, X549, T501, pP_in_ggaa(T527, T530, X549, T501))
pP_in_ggaa(T527, T530, T533, T501) → U47_ggaa(T527, T530, T533, T501, addC1_in_gga(T527, T530, T533))
U47_ggaa(T527, T530, T533, T501, addC1_out_gga(T527, T530, T533)) → U48_ggaa(T527, T530, T533, T501, addC1_in_gga(T527, T533, T501))
U48_ggaa(T527, T530, T533, T501, addC1_out_gga(T527, T533, T501)) → pP_out_ggaa(T527, T530, T533, T501)
U46_ggaaa(T526, T527, T530, X549, T501, pP_out_ggaa(T527, T530, X549, T501)) → pE_out_ggaaa(T526, T527, T530, X549, T501)
U5_gga(T526, T527, T501, pE_out_ggaaa(T526, T527, X548, X549, T501)) → timesA_out_gga(one(one(T526)), T527, T501)
U1_gga(T35, T36, T38, timesA_out_gga(T35, T36, T38)) → timesA_out_gga(zero(zero(T35)), T36, zero(zero(T38)))

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

TIMESA_IN_GGA(zero(zero(T35)), T36, zero(zero(T38))) → U1_GGA(T35, T36, T38, timesA_in_gga(T35, T36, T38))
TIMESA_IN_GGA(zero(zero(T35)), T36, zero(zero(T38))) → TIMESA_IN_GGA(T35, T36, T38)
TIMESA_IN_GGA(zero(one(T53)), T54, zero(T56)) → U2_GGA(T53, T54, T56, pB_in_ggaa(T53, T54, X65, T56))
TIMESA_IN_GGA(zero(one(T53)), T54, zero(T56)) → PB_IN_GGAA(T53, T54, X65, T56)
PB_IN_GGAA(T53, T54, T59, T56) → U39_GGAA(T53, T54, T59, T56, timesF_in_gga(T53, T54, T59))
PB_IN_GGAA(T53, T54, T59, T56) → TIMESF_IN_GGA(T53, T54, T59)
TIMESF_IN_GGA(zero(T75), T76, zero(X94)) → U6_GGA(T75, T76, X94, timesF_in_gga(T75, T76, X94))
TIMESF_IN_GGA(zero(T75), T76, zero(X94)) → TIMESF_IN_GGA(T75, T76, X94)
TIMESF_IN_GGA(one(T83), T84, X110) → U7_GGA(T83, T84, X110, pG_in_ggaa(T83, T84, X109, X110))
TIMESF_IN_GGA(one(T83), T84, X110) → PG_IN_GGAA(T83, T84, X109, X110)
PG_IN_GGAA(T83, T84, T87, X110) → U41_GGAA(T83, T84, T87, X110, timesF_in_gga(T83, T84, T87))
PG_IN_GGAA(T83, T84, T87, X110) → TIMESF_IN_GGA(T83, T84, T87)
U41_GGAA(T83, T84, T87, X110, timesF_out_gga(T83, T84, T87)) → U42_GGAA(T83, T84, T87, X110, addC1_in_gga(T84, T87, X110))
U41_GGAA(T83, T84, T87, X110, timesF_out_gga(T83, T84, T87)) → ADDC1_IN_GGA(T84, T87, X110)
ADDC1_IN_GGA(b, T103, zero(T103)) → U8_GGA(T103, binaryZH_in_g(T103))
ADDC1_IN_GGA(b, T103, zero(T103)) → BINARYZH_IN_G(T103)
BINARYZH_IN_G(zero(T109)) → U11_G(T109, binaryZH_in_g(T109))
BINARYZH_IN_G(zero(T109)) → BINARYZH_IN_G(T109)
BINARYZH_IN_G(one(T113)) → U12_G(T113, binaryK_in_g(T113))
BINARYZH_IN_G(one(T113)) → BINARYK_IN_G(T113)
BINARYK_IN_G(zero(T118)) → U13_G(T118, binaryZH_in_g(T118))
BINARYK_IN_G(zero(T118)) → BINARYZH_IN_G(T118)
BINARYK_IN_G(one(T122)) → U14_G(T122, binaryK_in_g(T122))
BINARYK_IN_G(one(T122)) → BINARYK_IN_G(T122)
ADDC1_IN_GGA(zero(T152), T153, zero(T155)) → U9_GGA(T152, T153, T155, addzI_in_gga(T152, T153, T155))
ADDC1_IN_GGA(zero(T152), T153, zero(T155)) → ADDZI_IN_GGA(T152, T153, T155)
ADDZI_IN_GGA(zero(T171), zero(T172), zero(T174)) → U15_GGA(T171, T172, T174, addzI_in_gga(T171, T172, T174))
ADDZI_IN_GGA(zero(T171), zero(T172), zero(T174)) → ADDZI_IN_GGA(T171, T172, T174)
ADDZI_IN_GGA(zero(one(T199)), one(b), one(one(T199))) → U16_GGA(T199, binaryK_in_g(T199))
ADDZI_IN_GGA(zero(one(T199)), one(b), one(one(T199))) → BINARYK_IN_G(T199)
ADDZI_IN_GGA(zero(zero(T204)), one(b), one(zero(T204))) → U17_GGA(T204, binaryZH_in_g(T204))
ADDZI_IN_GGA(zero(zero(T204)), one(b), one(zero(T204))) → BINARYZH_IN_G(T204)
ADDZI_IN_GGA(zero(T216), one(T217), one(T219)) → U18_GGA(T216, T217, T219, addzI_in_gga(T216, T217, T219))
ADDZI_IN_GGA(zero(T216), one(T217), one(T219)) → ADDZI_IN_GGA(T216, T217, T219)
ADDZI_IN_GGA(one(T235), zero(T236), one(T238)) → U19_GGA(T235, T236, T238, addyJ_in_gga(T235, T236, T238))
ADDZI_IN_GGA(one(T235), zero(T236), one(T238)) → ADDYJ_IN_GGA(T235, T236, T238)
ADDYJ_IN_GGA(b, one(T244), one(T244)) → U36_GGA(T244, binaryK_in_g(T244))
ADDYJ_IN_GGA(b, one(T244), one(T244)) → BINARYK_IN_G(T244)
ADDYJ_IN_GGA(b, zero(T249), zero(T249)) → U37_GGA(T249, binaryZH_in_g(T249))
ADDYJ_IN_GGA(b, zero(T249), zero(T249)) → BINARYZH_IN_G(T249)
ADDYJ_IN_GGA(T261, T262, T264) → U38_GGA(T261, T262, T264, addzI_in_gga(T261, T262, T264))
ADDYJ_IN_GGA(T261, T262, T264) → ADDZI_IN_GGA(T261, T262, T264)
ADDZI_IN_GGA(one(T274), one(T275), zero(T277)) → U20_GGA(T274, T275, T277, addcL_in_gga(T274, T275, T277))
ADDZI_IN_GGA(one(T274), one(T275), zero(T277)) → ADDCL_IN_GGA(T274, T275, T277)
ADDCL_IN_GGA(T286, b, T288) → U33_GGA(T286, T288, succZN_in_ga(T286, T288))
ADDCL_IN_GGA(T286, b, T288) → SUCCZN_IN_GA(T286, T288)
SUCCZN_IN_GA(zero(T294), one(T294)) → U23_GA(T294, binaryZH_in_g(T294))
SUCCZN_IN_GA(zero(T294), one(T294)) → BINARYZH_IN_G(T294)
SUCCZN_IN_GA(one(T300), zero(T302)) → U24_GA(T300, T302, succM_in_ga(T300, T302))
SUCCZN_IN_GA(one(T300), zero(T302)) → SUCCM_IN_GA(T300, T302)
SUCCM_IN_GA(zero(T307), one(T307)) → U21_GA(T307, binaryZH_in_g(T307))
SUCCM_IN_GA(zero(T307), one(T307)) → BINARYZH_IN_G(T307)
SUCCM_IN_GA(one(T313), zero(T315)) → U22_GA(T313, T315, succM_in_ga(T313, T315))
SUCCM_IN_GA(one(T313), zero(T315)) → SUCCM_IN_GA(T313, T315)
ADDCL_IN_GGA(b, T324, T326) → U34_GGA(T324, T326, succZN_in_ga(T324, T326))
ADDCL_IN_GGA(b, T324, T326) → SUCCZN_IN_GA(T324, T326)
ADDCL_IN_GGA(T338, T339, T341) → U35_GGA(T338, T339, T341, addCO_in_gga(T338, T339, T341))
ADDCL_IN_GGA(T338, T339, T341) → ADDCO_IN_GGA(T338, T339, T341)
ADDCO_IN_GGA(zero(T357), zero(T358), one(T360)) → U25_GGA(T357, T358, T360, addzI_in_gga(T357, T358, T360))
ADDCO_IN_GGA(zero(T357), zero(T358), one(T360)) → ADDZI_IN_GGA(T357, T358, T360)
ADDCO_IN_GGA(zero(zero(T385)), one(b), zero(one(T385))) → U26_GGA(T385, binaryZH_in_g(T385))
ADDCO_IN_GGA(zero(zero(T385)), one(b), zero(one(T385))) → BINARYZH_IN_G(T385)
ADDCO_IN_GGA(zero(one(T395)), one(b), zero(zero(T397))) → U27_GGA(T395, T397, succM_in_ga(T395, T397))
ADDCO_IN_GGA(zero(one(T395)), one(b), zero(zero(T397))) → SUCCM_IN_GA(T395, T397)
ADDCO_IN_GGA(zero(T408), one(T409), zero(T411)) → U28_GGA(T408, T409, T411, addCO_in_gga(T408, T409, T411))
ADDCO_IN_GGA(zero(T408), one(T409), zero(T411)) → ADDCO_IN_GGA(T408, T409, T411)
ADDCO_IN_GGA(one(b), zero(zero(T436)), zero(one(T436))) → U29_GGA(T436, binaryZH_in_g(T436))
ADDCO_IN_GGA(one(b), zero(zero(T436)), zero(one(T436))) → BINARYZH_IN_G(T436)
ADDCO_IN_GGA(one(b), zero(one(T446)), zero(zero(T448))) → U30_GGA(T446, T448, succM_in_ga(T446, T448))
ADDCO_IN_GGA(one(b), zero(one(T446)), zero(zero(T448))) → SUCCM_IN_GA(T446, T448)
ADDCO_IN_GGA(one(T459), zero(T460), zero(T462)) → U31_GGA(T459, T460, T462, addCO_in_gga(T459, T460, T462))
ADDCO_IN_GGA(one(T459), zero(T460), zero(T462)) → ADDCO_IN_GGA(T459, T460, T462)
ADDCO_IN_GGA(one(T472), one(T473), one(T475)) → U32_GGA(T472, T473, T475, addcL_in_gga(T472, T473, T475))
ADDCO_IN_GGA(one(T472), one(T473), one(T475)) → ADDCL_IN_GGA(T472, T473, T475)
ADDC1_IN_GGA(one(T489), T490, one(T492)) → U10_GGA(T489, T490, T492, addyJ_in_gga(T489, T490, T492))
ADDC1_IN_GGA(one(T489), T490, one(T492)) → ADDYJ_IN_GGA(T489, T490, T492)
U39_GGAA(T53, T54, T59, T56, timesF_out_gga(T53, T54, T59)) → U40_GGAA(T53, T54, T59, T56, addC1_in_gga(T54, T59, T56))
U39_GGAA(T53, T54, T59, T56, timesF_out_gga(T53, T54, T59)) → ADDC1_IN_GGA(T54, T59, T56)
TIMESA_IN_GGA(one(one(b)), T506, T501) → U3_GGA(T506, T501, addC1_in_gga(T506, T506, T501))
TIMESA_IN_GGA(one(one(b)), T506, T501) → ADDC1_IN_GGA(T506, T506, T501)
TIMESA_IN_GGA(one(zero(T515)), T516, T501) → U4_GGA(T515, T516, T501, pD_in_ggaa(T515, T516, X531, T501))
TIMESA_IN_GGA(one(zero(T515)), T516, T501) → PD_IN_GGAA(T515, T516, X531, T501)
PD_IN_GGAA(T515, T516, T519, T501) → U43_GGAA(T515, T516, T519, T501, timesF_in_gga(T515, T516, T519))
PD_IN_GGAA(T515, T516, T519, T501) → TIMESF_IN_GGA(T515, T516, T519)
U43_GGAA(T515, T516, T519, T501, timesF_out_gga(T515, T516, T519)) → U44_GGAA(T515, T516, T519, T501, addC1_in_gga(T516, zero(T519), T501))
U43_GGAA(T515, T516, T519, T501, timesF_out_gga(T515, T516, T519)) → ADDC1_IN_GGA(T516, zero(T519), T501)
TIMESA_IN_GGA(one(one(T526)), T527, T501) → U5_GGA(T526, T527, T501, pE_in_ggaaa(T526, T527, X548, X549, T501))
TIMESA_IN_GGA(one(one(T526)), T527, T501) → PE_IN_GGAAA(T526, T527, X548, X549, T501)
PE_IN_GGAAA(T526, T527, T530, X549, T501) → U45_GGAAA(T526, T527, T530, X549, T501, timesF_in_gga(T526, T527, T530))
PE_IN_GGAAA(T526, T527, T530, X549, T501) → TIMESF_IN_GGA(T526, T527, T530)
U45_GGAAA(T526, T527, T530, X549, T501, timesF_out_gga(T526, T527, T530)) → U46_GGAAA(T526, T527, T530, X549, T501, pP_in_ggaa(T527, T530, X549, T501))
U45_GGAAA(T526, T527, T530, X549, T501, timesF_out_gga(T526, T527, T530)) → PP_IN_GGAA(T527, T530, X549, T501)
PP_IN_GGAA(T527, T530, T533, T501) → U47_GGAA(T527, T530, T533, T501, addC1_in_gga(T527, T530, T533))
PP_IN_GGAA(T527, T530, T533, T501) → ADDC1_IN_GGA(T527, T530, T533)
U47_GGAA(T527, T530, T533, T501, addC1_out_gga(T527, T530, T533)) → U48_GGAA(T527, T530, T533, T501, addC1_in_gga(T527, T533, T501))
U47_GGAA(T527, T530, T533, T501, addC1_out_gga(T527, T530, T533)) → ADDC1_IN_GGA(T527, T533, T501)

The TRS R consists of the following rules:

timesA_in_gga(one(b), T5, T5) → timesA_out_gga(one(b), T5, T5)
timesA_in_gga(zero(one(b)), T22, zero(T22)) → timesA_out_gga(zero(one(b)), T22, zero(T22))
timesA_in_gga(zero(zero(T35)), T36, zero(zero(T38))) → U1_gga(T35, T36, T38, timesA_in_gga(T35, T36, T38))
timesA_in_gga(zero(one(T53)), T54, zero(T56)) → U2_gga(T53, T54, T56, pB_in_ggaa(T53, T54, X65, T56))
pB_in_ggaa(T53, T54, T59, T56) → U39_ggaa(T53, T54, T59, T56, timesF_in_gga(T53, T54, T59))
timesF_in_gga(one(b), T66, T66) → timesF_out_gga(one(b), T66, T66)
timesF_in_gga(zero(T75), T76, zero(X94)) → U6_gga(T75, T76, X94, timesF_in_gga(T75, T76, X94))
timesF_in_gga(one(T83), T84, X110) → U7_gga(T83, T84, X110, pG_in_ggaa(T83, T84, X109, X110))
pG_in_ggaa(T83, T84, T87, X110) → U41_ggaa(T83, T84, T87, X110, timesF_in_gga(T83, T84, T87))
U41_ggaa(T83, T84, T87, X110, timesF_out_gga(T83, T84, T87)) → U42_ggaa(T83, T84, T87, X110, addC1_in_gga(T84, T87, X110))
addC1_in_gga(b, T103, zero(T103)) → U8_gga(T103, binaryZH_in_g(T103))
binaryZH_in_g(zero(T109)) → U11_g(T109, binaryZH_in_g(T109))
binaryZH_in_g(one(T113)) → U12_g(T113, binaryK_in_g(T113))
binaryK_in_g(b) → binaryK_out_g(b)
binaryK_in_g(zero(T118)) → U13_g(T118, binaryZH_in_g(T118))
U13_g(T118, binaryZH_out_g(T118)) → binaryK_out_g(zero(T118))
binaryK_in_g(one(T122)) → U14_g(T122, binaryK_in_g(T122))
U14_g(T122, binaryK_out_g(T122)) → binaryK_out_g(one(T122))
U12_g(T113, binaryK_out_g(T113)) → binaryZH_out_g(one(T113))
U11_g(T109, binaryZH_out_g(T109)) → binaryZH_out_g(zero(T109))
U8_gga(T103, binaryZH_out_g(T103)) → addC1_out_gga(b, T103, zero(T103))
addC1_in_gga(zero(T152), T153, zero(T155)) → U9_gga(T152, T153, T155, addzI_in_gga(T152, T153, T155))
addzI_in_gga(zero(T171), zero(T172), zero(T174)) → U15_gga(T171, T172, T174, addzI_in_gga(T171, T172, T174))
addzI_in_gga(zero(one(T199)), one(b), one(one(T199))) → U16_gga(T199, binaryK_in_g(T199))
U16_gga(T199, binaryK_out_g(T199)) → addzI_out_gga(zero(one(T199)), one(b), one(one(T199)))
addzI_in_gga(zero(zero(T204)), one(b), one(zero(T204))) → U17_gga(T204, binaryZH_in_g(T204))
U17_gga(T204, binaryZH_out_g(T204)) → addzI_out_gga(zero(zero(T204)), one(b), one(zero(T204)))
addzI_in_gga(zero(T216), one(T217), one(T219)) → U18_gga(T216, T217, T219, addzI_in_gga(T216, T217, T219))
addzI_in_gga(one(T235), zero(T236), one(T238)) → U19_gga(T235, T236, T238, addyJ_in_gga(T235, T236, T238))
addyJ_in_gga(b, one(T244), one(T244)) → U36_gga(T244, binaryK_in_g(T244))
U36_gga(T244, binaryK_out_g(T244)) → addyJ_out_gga(b, one(T244), one(T244))
addyJ_in_gga(b, zero(T249), zero(T249)) → U37_gga(T249, binaryZH_in_g(T249))
U37_gga(T249, binaryZH_out_g(T249)) → addyJ_out_gga(b, zero(T249), zero(T249))
addyJ_in_gga(T261, T262, T264) → U38_gga(T261, T262, T264, addzI_in_gga(T261, T262, T264))
addzI_in_gga(one(T274), one(T275), zero(T277)) → U20_gga(T274, T275, T277, addcL_in_gga(T274, T275, T277))
addcL_in_gga(b, b, one(b)) → addcL_out_gga(b, b, one(b))
addcL_in_gga(T286, b, T288) → U33_gga(T286, T288, succZN_in_ga(T286, T288))
succZN_in_ga(zero(T294), one(T294)) → U23_ga(T294, binaryZH_in_g(T294))
U23_ga(T294, binaryZH_out_g(T294)) → succZN_out_ga(zero(T294), one(T294))
succZN_in_ga(one(T300), zero(T302)) → U24_ga(T300, T302, succM_in_ga(T300, T302))
succM_in_ga(b, one(b)) → succM_out_ga(b, one(b))
succM_in_ga(zero(T307), one(T307)) → U21_ga(T307, binaryZH_in_g(T307))
U21_ga(T307, binaryZH_out_g(T307)) → succM_out_ga(zero(T307), one(T307))
succM_in_ga(one(T313), zero(T315)) → U22_ga(T313, T315, succM_in_ga(T313, T315))
U22_ga(T313, T315, succM_out_ga(T313, T315)) → succM_out_ga(one(T313), zero(T315))
U24_ga(T300, T302, succM_out_ga(T300, T302)) → succZN_out_ga(one(T300), zero(T302))
U33_gga(T286, T288, succZN_out_ga(T286, T288)) → addcL_out_gga(T286, b, T288)
addcL_in_gga(b, T324, T326) → U34_gga(T324, T326, succZN_in_ga(T324, T326))
U34_gga(T324, T326, succZN_out_ga(T324, T326)) → addcL_out_gga(b, T324, T326)
addcL_in_gga(T338, T339, T341) → U35_gga(T338, T339, T341, addCO_in_gga(T338, T339, T341))
addCO_in_gga(zero(T357), zero(T358), one(T360)) → U25_gga(T357, T358, T360, addzI_in_gga(T357, T358, T360))
U25_gga(T357, T358, T360, addzI_out_gga(T357, T358, T360)) → addCO_out_gga(zero(T357), zero(T358), one(T360))
addCO_in_gga(zero(zero(T385)), one(b), zero(one(T385))) → U26_gga(T385, binaryZH_in_g(T385))
U26_gga(T385, binaryZH_out_g(T385)) → addCO_out_gga(zero(zero(T385)), one(b), zero(one(T385)))
addCO_in_gga(zero(one(T395)), one(b), zero(zero(T397))) → U27_gga(T395, T397, succM_in_ga(T395, T397))
U27_gga(T395, T397, succM_out_ga(T395, T397)) → addCO_out_gga(zero(one(T395)), one(b), zero(zero(T397)))
addCO_in_gga(zero(T408), one(T409), zero(T411)) → U28_gga(T408, T409, T411, addCO_in_gga(T408, T409, T411))
addCO_in_gga(one(b), zero(zero(T436)), zero(one(T436))) → U29_gga(T436, binaryZH_in_g(T436))
U29_gga(T436, binaryZH_out_g(T436)) → addCO_out_gga(one(b), zero(zero(T436)), zero(one(T436)))
addCO_in_gga(one(b), zero(one(T446)), zero(zero(T448))) → U30_gga(T446, T448, succM_in_ga(T446, T448))
U30_gga(T446, T448, succM_out_ga(T446, T448)) → addCO_out_gga(one(b), zero(one(T446)), zero(zero(T448)))
addCO_in_gga(one(T459), zero(T460), zero(T462)) → U31_gga(T459, T460, T462, addCO_in_gga(T459, T460, T462))
addCO_in_gga(one(T472), one(T473), one(T475)) → U32_gga(T472, T473, T475, addcL_in_gga(T472, T473, T475))
U32_gga(T472, T473, T475, addcL_out_gga(T472, T473, T475)) → addCO_out_gga(one(T472), one(T473), one(T475))
U31_gga(T459, T460, T462, addCO_out_gga(T459, T460, T462)) → addCO_out_gga(one(T459), zero(T460), zero(T462))
U28_gga(T408, T409, T411, addCO_out_gga(T408, T409, T411)) → addCO_out_gga(zero(T408), one(T409), zero(T411))
U35_gga(T338, T339, T341, addCO_out_gga(T338, T339, T341)) → addcL_out_gga(T338, T339, T341)
U20_gga(T274, T275, T277, addcL_out_gga(T274, T275, T277)) → addzI_out_gga(one(T274), one(T275), zero(T277))
U38_gga(T261, T262, T264, addzI_out_gga(T261, T262, T264)) → addyJ_out_gga(T261, T262, T264)
U19_gga(T235, T236, T238, addyJ_out_gga(T235, T236, T238)) → addzI_out_gga(one(T235), zero(T236), one(T238))
U18_gga(T216, T217, T219, addzI_out_gga(T216, T217, T219)) → addzI_out_gga(zero(T216), one(T217), one(T219))
U15_gga(T171, T172, T174, addzI_out_gga(T171, T172, T174)) → addzI_out_gga(zero(T171), zero(T172), zero(T174))
U9_gga(T152, T153, T155, addzI_out_gga(T152, T153, T155)) → addC1_out_gga(zero(T152), T153, zero(T155))
addC1_in_gga(one(T489), T490, one(T492)) → U10_gga(T489, T490, T492, addyJ_in_gga(T489, T490, T492))
U10_gga(T489, T490, T492, addyJ_out_gga(T489, T490, T492)) → addC1_out_gga(one(T489), T490, one(T492))
U42_ggaa(T83, T84, T87, X110, addC1_out_gga(T84, T87, X110)) → pG_out_ggaa(T83, T84, T87, X110)
U7_gga(T83, T84, X110, pG_out_ggaa(T83, T84, X109, X110)) → timesF_out_gga(one(T83), T84, X110)
U6_gga(T75, T76, X94, timesF_out_gga(T75, T76, X94)) → timesF_out_gga(zero(T75), T76, zero(X94))
U39_ggaa(T53, T54, T59, T56, timesF_out_gga(T53, T54, T59)) → U40_ggaa(T53, T54, T59, T56, addC1_in_gga(T54, T59, T56))
U40_ggaa(T53, T54, T59, T56, addC1_out_gga(T54, T59, T56)) → pB_out_ggaa(T53, T54, T59, T56)
U2_gga(T53, T54, T56, pB_out_ggaa(T53, T54, X65, T56)) → timesA_out_gga(zero(one(T53)), T54, zero(T56))
timesA_in_gga(one(one(b)), T506, T501) → U3_gga(T506, T501, addC1_in_gga(T506, T506, T501))
U3_gga(T506, T501, addC1_out_gga(T506, T506, T501)) → timesA_out_gga(one(one(b)), T506, T501)
timesA_in_gga(one(zero(T515)), T516, T501) → U4_gga(T515, T516, T501, pD_in_ggaa(T515, T516, X531, T501))
pD_in_ggaa(T515, T516, T519, T501) → U43_ggaa(T515, T516, T519, T501, timesF_in_gga(T515, T516, T519))
U43_ggaa(T515, T516, T519, T501, timesF_out_gga(T515, T516, T519)) → U44_ggaa(T515, T516, T519, T501, addC1_in_gga(T516, zero(T519), T501))
U44_ggaa(T515, T516, T519, T501, addC1_out_gga(T516, zero(T519), T501)) → pD_out_ggaa(T515, T516, T519, T501)
U4_gga(T515, T516, T501, pD_out_ggaa(T515, T516, X531, T501)) → timesA_out_gga(one(zero(T515)), T516, T501)
timesA_in_gga(one(one(T526)), T527, T501) → U5_gga(T526, T527, T501, pE_in_ggaaa(T526, T527, X548, X549, T501))
pE_in_ggaaa(T526, T527, T530, X549, T501) → U45_ggaaa(T526, T527, T530, X549, T501, timesF_in_gga(T526, T527, T530))
U45_ggaaa(T526, T527, T530, X549, T501, timesF_out_gga(T526, T527, T530)) → U46_ggaaa(T526, T527, T530, X549, T501, pP_in_ggaa(T527, T530, X549, T501))
pP_in_ggaa(T527, T530, T533, T501) → U47_ggaa(T527, T530, T533, T501, addC1_in_gga(T527, T530, T533))
U47_ggaa(T527, T530, T533, T501, addC1_out_gga(T527, T530, T533)) → U48_ggaa(T527, T530, T533, T501, addC1_in_gga(T527, T533, T501))
U48_ggaa(T527, T530, T533, T501, addC1_out_gga(T527, T533, T501)) → pP_out_ggaa(T527, T530, T533, T501)
U46_ggaaa(T526, T527, T530, X549, T501, pP_out_ggaa(T527, T530, X549, T501)) → pE_out_ggaaa(T526, T527, T530, X549, T501)
U5_gga(T526, T527, T501, pE_out_ggaaa(T526, T527, X548, X549, T501)) → timesA_out_gga(one(one(T526)), T527, T501)
U1_gga(T35, T36, T38, timesA_out_gga(T35, T36, T38)) → timesA_out_gga(zero(zero(T35)), T36, zero(zero(T38)))

The argument filtering Pi contains the following mapping:
timesA_in_gga(x1, x2, x3) = timesA_in_gga(x1, x2)
one(x1) = one(x1)
b = b
timesA_out_gga(x1, x2, x3) = timesA_out_gga(x1, x2, x3)
zero(x1) = zero(x1)
U1_gga(x1, x2, x3, x4) = U1_gga(x1, x2, x4)
U2_gga(x1, x2, x3, x4) = U2_gga(x1, x2, x4)
pB_in_ggaa(x1, x2, x3, x4) = pB_in_ggaa(x1, x2)
U39_ggaa(x1, x2, x3, x4, x5) = U39_ggaa(x1, x2, x5)
timesF_in_gga(x1, x2, x3) = timesF_in_gga(x1, x2)
timesF_out_gga(x1, x2, x3) = timesF_out_gga(x1, x2, x3)
U6_gga(x1, x2, x3, x4) = U6_gga(x1, x2, x4)
U7_gga(x1, x2, x3, x4) = U7_gga(x1, x2, x4)
pG_in_ggaa(x1, x2, x3, x4) = pG_in_ggaa(x1, x2)
U41_ggaa(x1, x2, x3, x4, x5) = U41_ggaa(x1, x2, x5)
U42_ggaa(x1, x2, x3, x4, x5) = U42_ggaa(x1, x2, x3, x5)
addC1_in_gga(x1, x2, x3) = addC1_in_gga(x1, x2)
U8_gga(x1, x2) = U8_gga(x1, x2)
binaryZH_in_g(x1) = binaryZH_in_g(x1)
U11_g(x1, x2) = U11_g(x1, x2)
U12_g(x1, x2) = U12_g(x1, x2)
binaryK_in_g(x1) = binaryK_in_g(x1)
binaryK_out_g(x1) = binaryK_out_g(x1)
U13_g(x1, x2) = U13_g(x1, x2)
binaryZH_out_g(x1) = binaryZH_out_g(x1)
U14_g(x1, x2) = U14_g(x1, x2)
addC1_out_gga(x1, x2, x3) = addC1_out_gga(x1, x2, x3)
U9_gga(x1, x2, x3, x4) = U9_gga(x1, x2, x4)
addzI_in_gga(x1, x2, x3) = addzI_in_gga(x1, x2)
U15_gga(x1, x2, x3, x4) = U15_gga(x1, x2, x4)
U16_gga(x1, x2) = U16_gga(x1, x2)
addzI_out_gga(x1, x2, x3) = addzI_out_gga(x1, x2, x3)
U17_gga(x1, x2) = U17_gga(x1, x2)
U18_gga(x1, x2, x3, x4) = U18_gga(x1, x2, x4)
U19_gga(x1, x2, x3, x4) = U19_gga(x1, x2, x4)
addyJ_in_gga(x1, x2, x3) = addyJ_in_gga(x1, x2)
U36_gga(x1, x2) = U36_gga(x1, x2)
addyJ_out_gga(x1, x2, x3) = addyJ_out_gga(x1, x2, x3)
U37_gga(x1, x2) = U37_gga(x1, x2)
U38_gga(x1, x2, x3, x4) = U38_gga(x1, x2, x4)
U20_gga(x1, x2, x3, x4) = U20_gga(x1, x2, x4)
addcL_in_gga(x1, x2, x3) = addcL_in_gga(x1, x2)
addcL_out_gga(x1, x2, x3) = addcL_out_gga(x1, x2, x3)
U33_gga(x1, x2, x3) = U33_gga(x1, x3)
succZN_in_ga(x1, x2) = succZN_in_ga(x1)
U23_ga(x1, x2) = U23_ga(x1, x2)
succZN_out_ga(x1, x2) = succZN_out_ga(x1, x2)
U24_ga(x1, x2, x3) = U24_ga(x1, x3)
succM_in_ga(x1, x2) = succM_in_ga(x1)
succM_out_ga(x1, x2) = succM_out_ga(x1, x2)
U21_ga(x1, x2) = U21_ga(x1, x2)
U22_ga(x1, x2, x3) = U22_ga(x1, x3)
U34_gga(x1, x2, x3) = U34_gga(x1, x3)
U35_gga(x1, x2, x3, x4) = U35_gga(x1, x2, x4)
addCO_in_gga(x1, x2, x3) = addCO_in_gga(x1, x2)
U25_gga(x1, x2, x3, x4) = U25_gga(x1, x2, x4)
addCO_out_gga(x1, x2, x3) = addCO_out_gga(x1, x2, x3)
U26_gga(x1, x2) = U26_gga(x1, x2)
U27_gga(x1, x2, x3) = U27_gga(x1, x3)
U28_gga(x1, x2, x3, x4) = U28_gga(x1, x2, x4)
U29_gga(x1, x2) = U29_gga(x1, x2)
U30_gga(x1, x2, x3) = U30_gga(x1, x3)
U31_gga(x1, x2, x3, x4) = U31_gga(x1, x2, x4)
U32_gga(x1, x2, x3, x4) = U32_gga(x1, x2, x4)
U10_gga(x1, x2, x3, x4) = U10_gga(x1, x2, x4)
pG_out_ggaa(x1, x2, x3, x4) = pG_out_ggaa(x1, x2, x3, x4)
U40_ggaa(x1, x2, x3, x4, x5) = U40_ggaa(x1, x2, x3, x5)
pB_out_ggaa(x1, x2, x3, x4) = pB_out_ggaa(x1, x2, x3, x4)
U3_gga(x1, x2, x3) = U3_gga(x1, x3)
U4_gga(x1, x2, x3, x4) = U4_gga(x1, x2, x4)
pD_in_ggaa(x1, x2, x3, x4) = pD_in_ggaa(x1, x2)
U43_ggaa(x1, x2, x3, x4, x5) = U43_ggaa(x1, x2, x5)
U44_ggaa(x1, x2, x3, x4, x5) = U44_ggaa(x1, x2, x3, x5)
pD_out_ggaa(x1, x2, x3, x4) = pD_out_ggaa(x1, x2, x3, x4)
U5_gga(x1, x2, x3, x4) = U5_gga(x1, x2, x4)
pE_in_ggaaa(x1, x2, x3, x4, x5) = pE_in_ggaaa(x1, x2)
U45_ggaaa(x1, x2, x3, x4, x5, x6) = U45_ggaaa(x1, x2, x6)
U46_ggaaa(x1, x2, x3, x4, x5, x6) = U46_ggaaa(x1, x2, x3, x6)
pP_in_ggaa(x1, x2, x3, x4) = pP_in_ggaa(x1, x2)
U47_ggaa(x1, x2, x3, x4, x5) = U47_ggaa(x1, x2, x5)
U48_ggaa(x1, x2, x3, x4, x5) = U48_ggaa(x1, x2, x3, x5)
pP_out_ggaa(x1, x2, x3, x4) = pP_out_ggaa(x1, x2, x3, x4)
pE_out_ggaaa(x1, x2, x3, x4, x5) = pE_out_ggaaa(x1, x2, x3, x4, x5)
TIMESA_IN_GGA(x1, x2, x3) = TIMESA_IN_GGA(x1, x2)
U1_GGA(x1, x2, x3, x4) = U1_GGA(x1, x2, x4)
U2_GGA(x1, x2, x3, x4) = U2_GGA(x1, x2, x4)
PB_IN_GGAA(x1, x2, x3, x4) = PB_IN_GGAA(x1, x2)
U39_GGAA(x1, x2, x3, x4, x5) = U39_GGAA(x1, x2, x5)
TIMESF_IN_GGA(x1, x2, x3) = TIMESF_IN_GGA(x1, x2)
U6_GGA(x1, x2, x3, x4) = U6_GGA(x1, x2, x4)
U7_GGA(x1, x2, x3, x4) = U7_GGA(x1, x2, x4)
PG_IN_GGAA(x1, x2, x3, x4) = PG_IN_GGAA(x1, x2)
U41_GGAA(x1, x2, x3, x4, x5) = U41_GGAA(x1, x2, x5)
U42_GGAA(x1, x2, x3, x4, x5) = U42_GGAA(x1, x2, x3, x5)
ADDC1_IN_GGA(x1, x2, x3) = ADDC1_IN_GGA(x1, x2)
U8_GGA(x1, x2) = U8_GGA(x1, x2)
BINARYZH_IN_G(x1) = BINARYZH_IN_G(x1)
U11_G(x1, x2) = U11_G(x1, x2)
U12_G(x1, x2) = U12_G(x1, x2)
BINARYK_IN_G(x1) = BINARYK_IN_G(x1)
U13_G(x1, x2) = U13_G(x1, x2)
U14_G(x1, x2) = U14_G(x1, x2)
U9_GGA(x1, x2, x3, x4) = U9_GGA(x1, x2, x4)
ADDZI_IN_GGA(x1, x2, x3) = ADDZI_IN_GGA(x1, x2)
U15_GGA(x1, x2, x3, x4) = U15_GGA(x1, x2, x4)
U16_GGA(x1, x2) = U16_GGA(x1, x2)
U17_GGA(x1, x2) = U17_GGA(x1, x2)
U18_GGA(x1, x2, x3, x4) = U18_GGA(x1, x2, x4)
U19_GGA(x1, x2, x3, x4) = U19_GGA(x1, x2, x4)
ADDYJ_IN_GGA(x1, x2, x3) = ADDYJ_IN_GGA(x1, x2)
U36_GGA(x1, x2) = U36_GGA(x1, x2)
U37_GGA(x1, x2) = U37_GGA(x1, x2)
U38_GGA(x1, x2, x3, x4) = U38_GGA(x1, x2, x4)
U20_GGA(x1, x2, x3, x4) = U20_GGA(x1, x2, x4)
ADDCL_IN_GGA(x1, x2, x3) = ADDCL_IN_GGA(x1, x2)
U33_GGA(x1, x2, x3) = U33_GGA(x1, x3)
SUCCZN_IN_GA(x1, x2) = SUCCZN_IN_GA(x1)
U23_GA(x1, x2) = U23_GA(x1, x2)
U24_GA(x1, x2, x3) = U24_GA(x1, x3)
SUCCM_IN_GA(x1, x2) = SUCCM_IN_GA(x1)
U21_GA(x1, x2) = U21_GA(x1, x2)
U22_GA(x1, x2, x3) = U22_GA(x1, x3)
U34_GGA(x1, x2, x3) = U34_GGA(x1, x3)
U35_GGA(x1, x2, x3, x4) = U35_GGA(x1, x2, x4)
ADDCO_IN_GGA(x1, x2, x3) = ADDCO_IN_GGA(x1, x2)
U25_GGA(x1, x2, x3, x4) = U25_GGA(x1, x2, x4)
U26_GGA(x1, x2) = U26_GGA(x1, x2)
U27_GGA(x1, x2, x3) = U27_GGA(x1, x3)
U28_GGA(x1, x2, x3, x4) = U28_GGA(x1, x2, x4)
U29_GGA(x1, x2) = U29_GGA(x1, x2)
U30_GGA(x1, x2, x3) = U30_GGA(x1, x3)
U31_GGA(x1, x2, x3, x4) = U31_GGA(x1, x2, x4)
U32_GGA(x1, x2, x3, x4) = U32_GGA(x1, x2, x4)
U10_GGA(x1, x2, x3, x4) = U10_GGA(x1, x2, x4)
U40_GGAA(x1, x2, x3, x4, x5) = U40_GGAA(x1, x2, x3, x5)
U3_GGA(x1, x2, x3) = U3_GGA(x1, x3)
U4_GGA(x1, x2, x3, x4) = U4_GGA(x1, x2, x4)
PD_IN_GGAA(x1, x2, x3, x4) = PD_IN_GGAA(x1, x2)
U43_GGAA(x1, x2, x3, x4, x5) = U43_GGAA(x1, x2, x5)
U44_GGAA(x1, x2, x3, x4, x5) = U44_GGAA(x1, x2, x3, x5)
U5_GGA(x1, x2, x3, x4) = U5_GGA(x1, x2, x4)
PE_IN_GGAAA(x1, x2, x3, x4, x5) = PE_IN_GGAAA(x1, x2)
U45_GGAAA(x1, x2, x3, x4, x5, x6) = U45_GGAAA(x1, x2, x6)
U46_GGAAA(x1, x2, x3, x4, x5, x6) = U46_GGAAA(x1, x2, x3, x6)
PP_IN_GGAA(x1, x2, x3, x4) = PP_IN_GGAA(x1, x2)
U47_GGAA(x1, x2, x3, x4, x5) = U47_GGAA(x1, x2, x5)
U48_GGAA(x1, x2, x3, x4, x5) = U48_GGAA(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:

TIMESA_IN_GGA(zero(zero(T35)), T36, zero(zero(T38))) → U1_GGA(T35, T36, T38, timesA_in_gga(T35, T36, T38))
TIMESA_IN_GGA(zero(zero(T35)), T36, zero(zero(T38))) → TIMESA_IN_GGA(T35, T36, T38)
TIMESA_IN_GGA(zero(one(T53)), T54, zero(T56)) → U2_GGA(T53, T54, T56, pB_in_ggaa(T53, T54, X65, T56))
TIMESA_IN_GGA(zero(one(T53)), T54, zero(T56)) → PB_IN_GGAA(T53, T54, X65, T56)
PB_IN_GGAA(T53, T54, T59, T56) → U39_GGAA(T53, T54, T59, T56, timesF_in_gga(T53, T54, T59))
PB_IN_GGAA(T53, T54, T59, T56) → TIMESF_IN_GGA(T53, T54, T59)
TIMESF_IN_GGA(zero(T75), T76, zero(X94)) → U6_GGA(T75, T76, X94, timesF_in_gga(T75, T76, X94))
TIMESF_IN_GGA(zero(T75), T76, zero(X94)) → TIMESF_IN_GGA(T75, T76, X94)
TIMESF_IN_GGA(one(T83), T84, X110) → U7_GGA(T83, T84, X110, pG_in_ggaa(T83, T84, X109, X110))
TIMESF_IN_GGA(one(T83), T84, X110) → PG_IN_GGAA(T83, T84, X109, X110)
PG_IN_GGAA(T83, T84, T87, X110) → U41_GGAA(T83, T84, T87, X110, timesF_in_gga(T83, T84, T87))
PG_IN_GGAA(T83, T84, T87, X110) → TIMESF_IN_GGA(T83, T84, T87)
U41_GGAA(T83, T84, T87, X110, timesF_out_gga(T83, T84, T87)) → U42_GGAA(T83, T84, T87, X110, addC1_in_gga(T84, T87, X110))
U41_GGAA(T83, T84, T87, X110, timesF_out_gga(T83, T84, T87)) → ADDC1_IN_GGA(T84, T87, X110)
ADDC1_IN_GGA(b, T103, zero(T103)) → U8_GGA(T103, binaryZH_in_g(T103))
ADDC1_IN_GGA(b, T103, zero(T103)) → BINARYZH_IN_G(T103)
BINARYZH_IN_G(zero(T109)) → U11_G(T109, binaryZH_in_g(T109))
BINARYZH_IN_G(zero(T109)) → BINARYZH_IN_G(T109)
BINARYZH_IN_G(one(T113)) → U12_G(T113, binaryK_in_g(T113))
BINARYZH_IN_G(one(T113)) → BINARYK_IN_G(T113)
BINARYK_IN_G(zero(T118)) → U13_G(T118, binaryZH_in_g(T118))
BINARYK_IN_G(zero(T118)) → BINARYZH_IN_G(T118)
BINARYK_IN_G(one(T122)) → U14_G(T122, binaryK_in_g(T122))
BINARYK_IN_G(one(T122)) → BINARYK_IN_G(T122)
ADDC1_IN_GGA(zero(T152), T153, zero(T155)) → U9_GGA(T152, T153, T155, addzI_in_gga(T152, T153, T155))
ADDC1_IN_GGA(zero(T152), T153, zero(T155)) → ADDZI_IN_GGA(T152, T153, T155)
ADDZI_IN_GGA(zero(T171), zero(T172), zero(T174)) → U15_GGA(T171, T172, T174, addzI_in_gga(T171, T172, T174))
ADDZI_IN_GGA(zero(T171), zero(T172), zero(T174)) → ADDZI_IN_GGA(T171, T172, T174)
ADDZI_IN_GGA(zero(one(T199)), one(b), one(one(T199))) → U16_GGA(T199, binaryK_in_g(T199))
ADDZI_IN_GGA(zero(one(T199)), one(b), one(one(T199))) → BINARYK_IN_G(T199)
ADDZI_IN_GGA(zero(zero(T204)), one(b), one(zero(T204))) → U17_GGA(T204, binaryZH_in_g(T204))
ADDZI_IN_GGA(zero(zero(T204)), one(b), one(zero(T204))) → BINARYZH_IN_G(T204)
ADDZI_IN_GGA(zero(T216), one(T217), one(T219)) → U18_GGA(T216, T217, T219, addzI_in_gga(T216, T217, T219))
ADDZI_IN_GGA(zero(T216), one(T217), one(T219)) → ADDZI_IN_GGA(T216, T217, T219)
ADDZI_IN_GGA(one(T235), zero(T236), one(T238)) → U19_GGA(T235, T236, T238, addyJ_in_gga(T235, T236, T238))
ADDZI_IN_GGA(one(T235), zero(T236), one(T238)) → ADDYJ_IN_GGA(T235, T236, T238)
ADDYJ_IN_GGA(b, one(T244), one(T244)) → U36_GGA(T244, binaryK_in_g(T244))
ADDYJ_IN_GGA(b, one(T244), one(T244)) → BINARYK_IN_G(T244)
ADDYJ_IN_GGA(b, zero(T249), zero(T249)) → U37_GGA(T249, binaryZH_in_g(T249))
ADDYJ_IN_GGA(b, zero(T249), zero(T249)) → BINARYZH_IN_G(T249)
ADDYJ_IN_GGA(T261, T262, T264) → U38_GGA(T261, T262, T264, addzI_in_gga(T261, T262, T264))
ADDYJ_IN_GGA(T261, T262, T264) → ADDZI_IN_GGA(T261, T262, T264)
ADDZI_IN_GGA(one(T274), one(T275), zero(T277)) → U20_GGA(T274, T275, T277, addcL_in_gga(T274, T275, T277))
ADDZI_IN_GGA(one(T274), one(T275), zero(T277)) → ADDCL_IN_GGA(T274, T275, T277)
ADDCL_IN_GGA(T286, b, T288) → U33_GGA(T286, T288, succZN_in_ga(T286, T288))
ADDCL_IN_GGA(T286, b, T288) → SUCCZN_IN_GA(T286, T288)
SUCCZN_IN_GA(zero(T294), one(T294)) → U23_GA(T294, binaryZH_in_g(T294))
SUCCZN_IN_GA(zero(T294), one(T294)) → BINARYZH_IN_G(T294)
SUCCZN_IN_GA(one(T300), zero(T302)) → U24_GA(T300, T302, succM_in_ga(T300, T302))
SUCCZN_IN_GA(one(T300), zero(T302)) → SUCCM_IN_GA(T300, T302)
SUCCM_IN_GA(zero(T307), one(T307)) → U21_GA(T307, binaryZH_in_g(T307))
SUCCM_IN_GA(zero(T307), one(T307)) → BINARYZH_IN_G(T307)
SUCCM_IN_GA(one(T313), zero(T315)) → U22_GA(T313, T315, succM_in_ga(T313, T315))
SUCCM_IN_GA(one(T313), zero(T315)) → SUCCM_IN_GA(T313, T315)
ADDCL_IN_GGA(b, T324, T326) → U34_GGA(T324, T326, succZN_in_ga(T324, T326))
ADDCL_IN_GGA(b, T324, T326) → SUCCZN_IN_GA(T324, T326)
ADDCL_IN_GGA(T338, T339, T341) → U35_GGA(T338, T339, T341, addCO_in_gga(T338, T339, T341))
ADDCL_IN_GGA(T338, T339, T341) → ADDCO_IN_GGA(T338, T339, T341)
ADDCO_IN_GGA(zero(T357), zero(T358), one(T360)) → U25_GGA(T357, T358, T360, addzI_in_gga(T357, T358, T360))
ADDCO_IN_GGA(zero(T357), zero(T358), one(T360)) → ADDZI_IN_GGA(T357, T358, T360)
ADDCO_IN_GGA(zero(zero(T385)), one(b), zero(one(T385))) → U26_GGA(T385, binaryZH_in_g(T385))
ADDCO_IN_GGA(zero(zero(T385)), one(b), zero(one(T385))) → BINARYZH_IN_G(T385)
ADDCO_IN_GGA(zero(one(T395)), one(b), zero(zero(T397))) → U27_GGA(T395, T397, succM_in_ga(T395, T397))
ADDCO_IN_GGA(zero(one(T395)), one(b), zero(zero(T397))) → SUCCM_IN_GA(T395, T397)
ADDCO_IN_GGA(zero(T408), one(T409), zero(T411)) → U28_GGA(T408, T409, T411, addCO_in_gga(T408, T409, T411))
ADDCO_IN_GGA(zero(T408), one(T409), zero(T411)) → ADDCO_IN_GGA(T408, T409, T411)
ADDCO_IN_GGA(one(b), zero(zero(T436)), zero(one(T436))) → U29_GGA(T436, binaryZH_in_g(T436))
ADDCO_IN_GGA(one(b), zero(zero(T436)), zero(one(T436))) → BINARYZH_IN_G(T436)
ADDCO_IN_GGA(one(b), zero(one(T446)), zero(zero(T448))) → U30_GGA(T446, T448, succM_in_ga(T446, T448))
ADDCO_IN_GGA(one(b), zero(one(T446)), zero(zero(T448))) → SUCCM_IN_GA(T446, T448)
ADDCO_IN_GGA(one(T459), zero(T460), zero(T462)) → U31_GGA(T459, T460, T462, addCO_in_gga(T459, T460, T462))
ADDCO_IN_GGA(one(T459), zero(T460), zero(T462)) → ADDCO_IN_GGA(T459, T460, T462)
ADDCO_IN_GGA(one(T472), one(T473), one(T475)) → U32_GGA(T472, T473, T475, addcL_in_gga(T472, T473, T475))
ADDCO_IN_GGA(one(T472), one(T473), one(T475)) → ADDCL_IN_GGA(T472, T473, T475)
ADDC1_IN_GGA(one(T489), T490, one(T492)) → U10_GGA(T489, T490, T492, addyJ_in_gga(T489, T490, T492))
ADDC1_IN_GGA(one(T489), T490, one(T492)) → ADDYJ_IN_GGA(T489, T490, T492)
U39_GGAA(T53, T54, T59, T56, timesF_out_gga(T53, T54, T59)) → U40_GGAA(T53, T54, T59, T56, addC1_in_gga(T54, T59, T56))
U39_GGAA(T53, T54, T59, T56, timesF_out_gga(T53, T54, T59)) → ADDC1_IN_GGA(T54, T59, T56)
TIMESA_IN_GGA(one(one(b)), T506, T501) → U3_GGA(T506, T501, addC1_in_gga(T506, T506, T501))
TIMESA_IN_GGA(one(one(b)), T506, T501) → ADDC1_IN_GGA(T506, T506, T501)
TIMESA_IN_GGA(one(zero(T515)), T516, T501) → U4_GGA(T515, T516, T501, pD_in_ggaa(T515, T516, X531, T501))
TIMESA_IN_GGA(one(zero(T515)), T516, T501) → PD_IN_GGAA(T515, T516, X531, T501)
PD_IN_GGAA(T515, T516, T519, T501) → U43_GGAA(T515, T516, T519, T501, timesF_in_gga(T515, T516, T519))
PD_IN_GGAA(T515, T516, T519, T501) → TIMESF_IN_GGA(T515, T516, T519)
U43_GGAA(T515, T516, T519, T501, timesF_out_gga(T515, T516, T519)) → U44_GGAA(T515, T516, T519, T501, addC1_in_gga(T516, zero(T519), T501))
U43_GGAA(T515, T516, T519, T501, timesF_out_gga(T515, T516, T519)) → ADDC1_IN_GGA(T516, zero(T519), T501)
TIMESA_IN_GGA(one(one(T526)), T527, T501) → U5_GGA(T526, T527, T501, pE_in_ggaaa(T526, T527, X548, X549, T501))
TIMESA_IN_GGA(one(one(T526)), T527, T501) → PE_IN_GGAAA(T526, T527, X548, X549, T501)
PE_IN_GGAAA(T526, T527, T530, X549, T501) → U45_GGAAA(T526, T527, T530, X549, T501, timesF_in_gga(T526, T527, T530))
PE_IN_GGAAA(T526, T527, T530, X549, T501) → TIMESF_IN_GGA(T526, T527, T530)
U45_GGAAA(T526, T527, T530, X549, T501, timesF_out_gga(T526, T527, T530)) → U46_GGAAA(T526, T527, T530, X549, T501, pP_in_ggaa(T527, T530, X549, T501))
U45_GGAAA(T526, T527, T530, X549, T501, timesF_out_gga(T526, T527, T530)) → PP_IN_GGAA(T527, T530, X549, T501)
PP_IN_GGAA(T527, T530, T533, T501) → U47_GGAA(T527, T530, T533, T501, addC1_in_gga(T527, T530, T533))
PP_IN_GGAA(T527, T530, T533, T501) → ADDC1_IN_GGA(T527, T530, T533)
U47_GGAA(T527, T530, T533, T501, addC1_out_gga(T527, T530, T533)) → U48_GGAA(T527, T530, T533, T501, addC1_in_gga(T527, T533, T501))
U47_GGAA(T527, T530, T533, T501, addC1_out_gga(T527, T530, T533)) → ADDC1_IN_GGA(T527, T533, T501)

The TRS R consists of the following rules:

timesA_in_gga(one(b), T5, T5) → timesA_out_gga(one(b), T5, T5)
timesA_in_gga(zero(one(b)), T22, zero(T22)) → timesA_out_gga(zero(one(b)), T22, zero(T22))
timesA_in_gga(zero(zero(T35)), T36, zero(zero(T38))) → U1_gga(T35, T36, T38, timesA_in_gga(T35, T36, T38))
timesA_in_gga(zero(one(T53)), T54, zero(T56)) → U2_gga(T53, T54, T56, pB_in_ggaa(T53, T54, X65, T56))
pB_in_ggaa(T53, T54, T59, T56) → U39_ggaa(T53, T54, T59, T56, timesF_in_gga(T53, T54, T59))
timesF_in_gga(one(b), T66, T66) → timesF_out_gga(one(b), T66, T66)
timesF_in_gga(zero(T75), T76, zero(X94)) → U6_gga(T75, T76, X94, timesF_in_gga(T75, T76, X94))
timesF_in_gga(one(T83), T84, X110) → U7_gga(T83, T84, X110, pG_in_ggaa(T83, T84, X109, X110))
pG_in_ggaa(T83, T84, T87, X110) → U41_ggaa(T83, T84, T87, X110, timesF_in_gga(T83, T84, T87))
U41_ggaa(T83, T84, T87, X110, timesF_out_gga(T83, T84, T87)) → U42_ggaa(T83, T84, T87, X110, addC1_in_gga(T84, T87, X110))
addC1_in_gga(b, T103, zero(T103)) → U8_gga(T103, binaryZH_in_g(T103))
binaryZH_in_g(zero(T109)) → U11_g(T109, binaryZH_in_g(T109))
binaryZH_in_g(one(T113)) → U12_g(T113, binaryK_in_g(T113))
binaryK_in_g(b) → binaryK_out_g(b)
binaryK_in_g(zero(T118)) → U13_g(T118, binaryZH_in_g(T118))
U13_g(T118, binaryZH_out_g(T118)) → binaryK_out_g(zero(T118))
binaryK_in_g(one(T122)) → U14_g(T122, binaryK_in_g(T122))
U14_g(T122, binaryK_out_g(T122)) → binaryK_out_g(one(T122))
U12_g(T113, binaryK_out_g(T113)) → binaryZH_out_g(one(T113))
U11_g(T109, binaryZH_out_g(T109)) → binaryZH_out_g(zero(T109))
U8_gga(T103, binaryZH_out_g(T103)) → addC1_out_gga(b, T103, zero(T103))
addC1_in_gga(zero(T152), T153, zero(T155)) → U9_gga(T152, T153, T155, addzI_in_gga(T152, T153, T155))
addzI_in_gga(zero(T171), zero(T172), zero(T174)) → U15_gga(T171, T172, T174, addzI_in_gga(T171, T172, T174))
addzI_in_gga(zero(one(T199)), one(b), one(one(T199))) → U16_gga(T199, binaryK_in_g(T199))
U16_gga(T199, binaryK_out_g(T199)) → addzI_out_gga(zero(one(T199)), one(b), one(one(T199)))
addzI_in_gga(zero(zero(T204)), one(b), one(zero(T204))) → U17_gga(T204, binaryZH_in_g(T204))
U17_gga(T204, binaryZH_out_g(T204)) → addzI_out_gga(zero(zero(T204)), one(b), one(zero(T204)))
addzI_in_gga(zero(T216), one(T217), one(T219)) → U18_gga(T216, T217, T219, addzI_in_gga(T216, T217, T219))
addzI_in_gga(one(T235), zero(T236), one(T238)) → U19_gga(T235, T236, T238, addyJ_in_gga(T235, T236, T238))
addyJ_in_gga(b, one(T244), one(T244)) → U36_gga(T244, binaryK_in_g(T244))
U36_gga(T244, binaryK_out_g(T244)) → addyJ_out_gga(b, one(T244), one(T244))
addyJ_in_gga(b, zero(T249), zero(T249)) → U37_gga(T249, binaryZH_in_g(T249))
U37_gga(T249, binaryZH_out_g(T249)) → addyJ_out_gga(b, zero(T249), zero(T249))
addyJ_in_gga(T261, T262, T264) → U38_gga(T261, T262, T264, addzI_in_gga(T261, T262, T264))
addzI_in_gga(one(T274), one(T275), zero(T277)) → U20_gga(T274, T275, T277, addcL_in_gga(T274, T275, T277))
addcL_in_gga(b, b, one(b)) → addcL_out_gga(b, b, one(b))
addcL_in_gga(T286, b, T288) → U33_gga(T286, T288, succZN_in_ga(T286, T288))
succZN_in_ga(zero(T294), one(T294)) → U23_ga(T294, binaryZH_in_g(T294))
U23_ga(T294, binaryZH_out_g(T294)) → succZN_out_ga(zero(T294), one(T294))
succZN_in_ga(one(T300), zero(T302)) → U24_ga(T300, T302, succM_in_ga(T300, T302))
succM_in_ga(b, one(b)) → succM_out_ga(b, one(b))
succM_in_ga(zero(T307), one(T307)) → U21_ga(T307, binaryZH_in_g(T307))
U21_ga(T307, binaryZH_out_g(T307)) → succM_out_ga(zero(T307), one(T307))
succM_in_ga(one(T313), zero(T315)) → U22_ga(T313, T315, succM_in_ga(T313, T315))
U22_ga(T313, T315, succM_out_ga(T313, T315)) → succM_out_ga(one(T313), zero(T315))
U24_ga(T300, T302, succM_out_ga(T300, T302)) → succZN_out_ga(one(T300), zero(T302))
U33_gga(T286, T288, succZN_out_ga(T286, T288)) → addcL_out_gga(T286, b, T288)
addcL_in_gga(b, T324, T326) → U34_gga(T324, T326, succZN_in_ga(T324, T326))
U34_gga(T324, T326, succZN_out_ga(T324, T326)) → addcL_out_gga(b, T324, T326)
addcL_in_gga(T338, T339, T341) → U35_gga(T338, T339, T341, addCO_in_gga(T338, T339, T341))
addCO_in_gga(zero(T357), zero(T358), one(T360)) → U25_gga(T357, T358, T360, addzI_in_gga(T357, T358, T360))
U25_gga(T357, T358, T360, addzI_out_gga(T357, T358, T360)) → addCO_out_gga(zero(T357), zero(T358), one(T360))
addCO_in_gga(zero(zero(T385)), one(b), zero(one(T385))) → U26_gga(T385, binaryZH_in_g(T385))
U26_gga(T385, binaryZH_out_g(T385)) → addCO_out_gga(zero(zero(T385)), one(b), zero(one(T385)))
addCO_in_gga(zero(one(T395)), one(b), zero(zero(T397))) → U27_gga(T395, T397, succM_in_ga(T395, T397))
U27_gga(T395, T397, succM_out_ga(T395, T397)) → addCO_out_gga(zero(one(T395)), one(b), zero(zero(T397)))
addCO_in_gga(zero(T408), one(T409), zero(T411)) → U28_gga(T408, T409, T411, addCO_in_gga(T408, T409, T411))
addCO_in_gga(one(b), zero(zero(T436)), zero(one(T436))) → U29_gga(T436, binaryZH_in_g(T436))
U29_gga(T436, binaryZH_out_g(T436)) → addCO_out_gga(one(b), zero(zero(T436)), zero(one(T436)))
addCO_in_gga(one(b), zero(one(T446)), zero(zero(T448))) → U30_gga(T446, T448, succM_in_ga(T446, T448))
U30_gga(T446, T448, succM_out_ga(T446, T448)) → addCO_out_gga(one(b), zero(one(T446)), zero(zero(T448)))
addCO_in_gga(one(T459), zero(T460), zero(T462)) → U31_gga(T459, T460, T462, addCO_in_gga(T459, T460, T462))
addCO_in_gga(one(T472), one(T473), one(T475)) → U32_gga(T472, T473, T475, addcL_in_gga(T472, T473, T475))
U32_gga(T472, T473, T475, addcL_out_gga(T472, T473, T475)) → addCO_out_gga(one(T472), one(T473), one(T475))
U31_gga(T459, T460, T462, addCO_out_gga(T459, T460, T462)) → addCO_out_gga(one(T459), zero(T460), zero(T462))
U28_gga(T408, T409, T411, addCO_out_gga(T408, T409, T411)) → addCO_out_gga(zero(T408), one(T409), zero(T411))
U35_gga(T338, T339, T341, addCO_out_gga(T338, T339, T341)) → addcL_out_gga(T338, T339, T341)
U20_gga(T274, T275, T277, addcL_out_gga(T274, T275, T277)) → addzI_out_gga(one(T274), one(T275), zero(T277))
U38_gga(T261, T262, T264, addzI_out_gga(T261, T262, T264)) → addyJ_out_gga(T261, T262, T264)
U19_gga(T235, T236, T238, addyJ_out_gga(T235, T236, T238)) → addzI_out_gga(one(T235), zero(T236), one(T238))
U18_gga(T216, T217, T219, addzI_out_gga(T216, T217, T219)) → addzI_out_gga(zero(T216), one(T217), one(T219))
U15_gga(T171, T172, T174, addzI_out_gga(T171, T172, T174)) → addzI_out_gga(zero(T171), zero(T172), zero(T174))
U9_gga(T152, T153, T155, addzI_out_gga(T152, T153, T155)) → addC1_out_gga(zero(T152), T153, zero(T155))
addC1_in_gga(one(T489), T490, one(T492)) → U10_gga(T489, T490, T492, addyJ_in_gga(T489, T490, T492))
U10_gga(T489, T490, T492, addyJ_out_gga(T489, T490, T492)) → addC1_out_gga(one(T489), T490, one(T492))
U42_ggaa(T83, T84, T87, X110, addC1_out_gga(T84, T87, X110)) → pG_out_ggaa(T83, T84, T87, X110)
U7_gga(T83, T84, X110, pG_out_ggaa(T83, T84, X109, X110)) → timesF_out_gga(one(T83), T84, X110)
U6_gga(T75, T76, X94, timesF_out_gga(T75, T76, X94)) → timesF_out_gga(zero(T75), T76, zero(X94))
U39_ggaa(T53, T54, T59, T56, timesF_out_gga(T53, T54, T59)) → U40_ggaa(T53, T54, T59, T56, addC1_in_gga(T54, T59, T56))
U40_ggaa(T53, T54, T59, T56, addC1_out_gga(T54, T59, T56)) → pB_out_ggaa(T53, T54, T59, T56)
U2_gga(T53, T54, T56, pB_out_ggaa(T53, T54, X65, T56)) → timesA_out_gga(zero(one(T53)), T54, zero(T56))
timesA_in_gga(one(one(b)), T506, T501) → U3_gga(T506, T501, addC1_in_gga(T506, T506, T501))
U3_gga(T506, T501, addC1_out_gga(T506, T506, T501)) → timesA_out_gga(one(one(b)), T506, T501)
timesA_in_gga(one(zero(T515)), T516, T501) → U4_gga(T515, T516, T501, pD_in_ggaa(T515, T516, X531, T501))
pD_in_ggaa(T515, T516, T519, T501) → U43_ggaa(T515, T516, T519, T501, timesF_in_gga(T515, T516, T519))
U43_ggaa(T515, T516, T519, T501, timesF_out_gga(T515, T516, T519)) → U44_ggaa(T515, T516, T519, T501, addC1_in_gga(T516, zero(T519), T501))
U44_ggaa(T515, T516, T519, T501, addC1_out_gga(T516, zero(T519), T501)) → pD_out_ggaa(T515, T516, T519, T501)
U4_gga(T515, T516, T501, pD_out_ggaa(T515, T516, X531, T501)) → timesA_out_gga(one(zero(T515)), T516, T501)
timesA_in_gga(one(one(T526)), T527, T501) → U5_gga(T526, T527, T501, pE_in_ggaaa(T526, T527, X548, X549, T501))
pE_in_ggaaa(T526, T527, T530, X549, T501) → U45_ggaaa(T526, T527, T530, X549, T501, timesF_in_gga(T526, T527, T530))
U45_ggaaa(T526, T527, T530, X549, T501, timesF_out_gga(T526, T527, T530)) → U46_ggaaa(T526, T527, T530, X549, T501, pP_in_ggaa(T527, T530, X549, T501))
pP_in_ggaa(T527, T530, T533, T501) → U47_ggaa(T527, T530, T533, T501, addC1_in_gga(T527, T530, T533))
U47_ggaa(T527, T530, T533, T501, addC1_out_gga(T527, T530, T533)) → U48_ggaa(T527, T530, T533, T501, addC1_in_gga(T527, T533, T501))
U48_ggaa(T527, T530, T533, T501, addC1_out_gga(T527, T533, T501)) → pP_out_ggaa(T527, T530, T533, T501)
U46_ggaaa(T526, T527, T530, X549, T501, pP_out_ggaa(T527, T530, X549, T501)) → pE_out_ggaaa(T526, T527, T530, X549, T501)
U5_gga(T526, T527, T501, pE_out_ggaaa(T526, T527, X548, X549, T501)) → timesA_out_gga(one(one(T526)), T527, T501)
U1_gga(T35, T36, T38, timesA_out_gga(T35, T36, T38)) → timesA_out_gga(zero(zero(T35)), T36, zero(zero(T38)))

(5) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 5 SCCs with 77 less nodes.

(6) Complex Obligation (AND)

(7) Obligation:

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

BINARYZH_IN_G(one(T113)) → BINARYK_IN_G(T113)
BINARYK_IN_G(zero(T118)) → BINARYZH_IN_G(T118)
BINARYZH_IN_G(zero(T109)) → BINARYZH_IN_G(T109)
BINARYK_IN_G(one(T122)) → BINARYK_IN_G(T122)

The TRS R consists of the following rules:

timesA_in_gga(one(b), T5, T5) → timesA_out_gga(one(b), T5, T5)
timesA_in_gga(zero(one(b)), T22, zero(T22)) → timesA_out_gga(zero(one(b)), T22, zero(T22))
timesA_in_gga(zero(zero(T35)), T36, zero(zero(T38))) → U1_gga(T35, T36, T38, timesA_in_gga(T35, T36, T38))
timesA_in_gga(zero(one(T53)), T54, zero(T56)) → U2_gga(T53, T54, T56, pB_in_ggaa(T53, T54, X65, T56))
pB_in_ggaa(T53, T54, T59, T56) → U39_ggaa(T53, T54, T59, T56, timesF_in_gga(T53, T54, T59))
timesF_in_gga(one(b), T66, T66) → timesF_out_gga(one(b), T66, T66)
timesF_in_gga(zero(T75), T76, zero(X94)) → U6_gga(T75, T76, X94, timesF_in_gga(T75, T76, X94))
timesF_in_gga(one(T83), T84, X110) → U7_gga(T83, T84, X110, pG_in_ggaa(T83, T84, X109, X110))
pG_in_ggaa(T83, T84, T87, X110) → U41_ggaa(T83, T84, T87, X110, timesF_in_gga(T83, T84, T87))
U41_ggaa(T83, T84, T87, X110, timesF_out_gga(T83, T84, T87)) → U42_ggaa(T83, T84, T87, X110, addC1_in_gga(T84, T87, X110))
addC1_in_gga(b, T103, zero(T103)) → U8_gga(T103, binaryZH_in_g(T103))
binaryZH_in_g(zero(T109)) → U11_g(T109, binaryZH_in_g(T109))
binaryZH_in_g(one(T113)) → U12_g(T113, binaryK_in_g(T113))
binaryK_in_g(b) → binaryK_out_g(b)
binaryK_in_g(zero(T118)) → U13_g(T118, binaryZH_in_g(T118))
U13_g(T118, binaryZH_out_g(T118)) → binaryK_out_g(zero(T118))
binaryK_in_g(one(T122)) → U14_g(T122, binaryK_in_g(T122))
U14_g(T122, binaryK_out_g(T122)) → binaryK_out_g(one(T122))
U12_g(T113, binaryK_out_g(T113)) → binaryZH_out_g(one(T113))
U11_g(T109, binaryZH_out_g(T109)) → binaryZH_out_g(zero(T109))
U8_gga(T103, binaryZH_out_g(T103)) → addC1_out_gga(b, T103, zero(T103))
addC1_in_gga(zero(T152), T153, zero(T155)) → U9_gga(T152, T153, T155, addzI_in_gga(T152, T153, T155))
addzI_in_gga(zero(T171), zero(T172), zero(T174)) → U15_gga(T171, T172, T174, addzI_in_gga(T171, T172, T174))
addzI_in_gga(zero(one(T199)), one(b), one(one(T199))) → U16_gga(T199, binaryK_in_g(T199))
U16_gga(T199, binaryK_out_g(T199)) → addzI_out_gga(zero(one(T199)), one(b), one(one(T199)))
addzI_in_gga(zero(zero(T204)), one(b), one(zero(T204))) → U17_gga(T204, binaryZH_in_g(T204))
U17_gga(T204, binaryZH_out_g(T204)) → addzI_out_gga(zero(zero(T204)), one(b), one(zero(T204)))
addzI_in_gga(zero(T216), one(T217), one(T219)) → U18_gga(T216, T217, T219, addzI_in_gga(T216, T217, T219))
addzI_in_gga(one(T235), zero(T236), one(T238)) → U19_gga(T235, T236, T238, addyJ_in_gga(T235, T236, T238))
addyJ_in_gga(b, one(T244), one(T244)) → U36_gga(T244, binaryK_in_g(T244))
U36_gga(T244, binaryK_out_g(T244)) → addyJ_out_gga(b, one(T244), one(T244))
addyJ_in_gga(b, zero(T249), zero(T249)) → U37_gga(T249, binaryZH_in_g(T249))
U37_gga(T249, binaryZH_out_g(T249)) → addyJ_out_gga(b, zero(T249), zero(T249))
addyJ_in_gga(T261, T262, T264) → U38_gga(T261, T262, T264, addzI_in_gga(T261, T262, T264))
addzI_in_gga(one(T274), one(T275), zero(T277)) → U20_gga(T274, T275, T277, addcL_in_gga(T274, T275, T277))
addcL_in_gga(b, b, one(b)) → addcL_out_gga(b, b, one(b))
addcL_in_gga(T286, b, T288) → U33_gga(T286, T288, succZN_in_ga(T286, T288))
succZN_in_ga(zero(T294), one(T294)) → U23_ga(T294, binaryZH_in_g(T294))
U23_ga(T294, binaryZH_out_g(T294)) → succZN_out_ga(zero(T294), one(T294))
succZN_in_ga(one(T300), zero(T302)) → U24_ga(T300, T302, succM_in_ga(T300, T302))
succM_in_ga(b, one(b)) → succM_out_ga(b, one(b))
succM_in_ga(zero(T307), one(T307)) → U21_ga(T307, binaryZH_in_g(T307))
U21_ga(T307, binaryZH_out_g(T307)) → succM_out_ga(zero(T307), one(T307))
succM_in_ga(one(T313), zero(T315)) → U22_ga(T313, T315, succM_in_ga(T313, T315))
U22_ga(T313, T315, succM_out_ga(T313, T315)) → succM_out_ga(one(T313), zero(T315))
U24_ga(T300, T302, succM_out_ga(T300, T302)) → succZN_out_ga(one(T300), zero(T302))
U33_gga(T286, T288, succZN_out_ga(T286, T288)) → addcL_out_gga(T286, b, T288)
addcL_in_gga(b, T324, T326) → U34_gga(T324, T326, succZN_in_ga(T324, T326))
U34_gga(T324, T326, succZN_out_ga(T324, T326)) → addcL_out_gga(b, T324, T326)
addcL_in_gga(T338, T339, T341) → U35_gga(T338, T339, T341, addCO_in_gga(T338, T339, T341))
addCO_in_gga(zero(T357), zero(T358), one(T360)) → U25_gga(T357, T358, T360, addzI_in_gga(T357, T358, T360))
U25_gga(T357, T358, T360, addzI_out_gga(T357, T358, T360)) → addCO_out_gga(zero(T357), zero(T358), one(T360))
addCO_in_gga(zero(zero(T385)), one(b), zero(one(T385))) → U26_gga(T385, binaryZH_in_g(T385))
U26_gga(T385, binaryZH_out_g(T385)) → addCO_out_gga(zero(zero(T385)), one(b), zero(one(T385)))
addCO_in_gga(zero(one(T395)), one(b), zero(zero(T397))) → U27_gga(T395, T397, succM_in_ga(T395, T397))
U27_gga(T395, T397, succM_out_ga(T395, T397)) → addCO_out_gga(zero(one(T395)), one(b), zero(zero(T397)))
addCO_in_gga(zero(T408), one(T409), zero(T411)) → U28_gga(T408, T409, T411, addCO_in_gga(T408, T409, T411))
addCO_in_gga(one(b), zero(zero(T436)), zero(one(T436))) → U29_gga(T436, binaryZH_in_g(T436))
U29_gga(T436, binaryZH_out_g(T436)) → addCO_out_gga(one(b), zero(zero(T436)), zero(one(T436)))
addCO_in_gga(one(b), zero(one(T446)), zero(zero(T448))) → U30_gga(T446, T448, succM_in_ga(T446, T448))
U30_gga(T446, T448, succM_out_ga(T446, T448)) → addCO_out_gga(one(b), zero(one(T446)), zero(zero(T448)))
addCO_in_gga(one(T459), zero(T460), zero(T462)) → U31_gga(T459, T460, T462, addCO_in_gga(T459, T460, T462))
addCO_in_gga(one(T472), one(T473), one(T475)) → U32_gga(T472, T473, T475, addcL_in_gga(T472, T473, T475))
U32_gga(T472, T473, T475, addcL_out_gga(T472, T473, T475)) → addCO_out_gga(one(T472), one(T473), one(T475))
U31_gga(T459, T460, T462, addCO_out_gga(T459, T460, T462)) → addCO_out_gga(one(T459), zero(T460), zero(T462))
U28_gga(T408, T409, T411, addCO_out_gga(T408, T409, T411)) → addCO_out_gga(zero(T408), one(T409), zero(T411))
U35_gga(T338, T339, T341, addCO_out_gga(T338, T339, T341)) → addcL_out_gga(T338, T339, T341)
U20_gga(T274, T275, T277, addcL_out_gga(T274, T275, T277)) → addzI_out_gga(one(T274), one(T275), zero(T277))
U38_gga(T261, T262, T264, addzI_out_gga(T261, T262, T264)) → addyJ_out_gga(T261, T262, T264)
U19_gga(T235, T236, T238, addyJ_out_gga(T235, T236, T238)) → addzI_out_gga(one(T235), zero(T236), one(T238))
U18_gga(T216, T217, T219, addzI_out_gga(T216, T217, T219)) → addzI_out_gga(zero(T216), one(T217), one(T219))
U15_gga(T171, T172, T174, addzI_out_gga(T171, T172, T174)) → addzI_out_gga(zero(T171), zero(T172), zero(T174))
U9_gga(T152, T153, T155, addzI_out_gga(T152, T153, T155)) → addC1_out_gga(zero(T152), T153, zero(T155))
addC1_in_gga(one(T489), T490, one(T492)) → U10_gga(T489, T490, T492, addyJ_in_gga(T489, T490, T492))
U10_gga(T489, T490, T492, addyJ_out_gga(T489, T490, T492)) → addC1_out_gga(one(T489), T490, one(T492))
U42_ggaa(T83, T84, T87, X110, addC1_out_gga(T84, T87, X110)) → pG_out_ggaa(T83, T84, T87, X110)
U7_gga(T83, T84, X110, pG_out_ggaa(T83, T84, X109, X110)) → timesF_out_gga(one(T83), T84, X110)
U6_gga(T75, T76, X94, timesF_out_gga(T75, T76, X94)) → timesF_out_gga(zero(T75), T76, zero(X94))
U39_ggaa(T53, T54, T59, T56, timesF_out_gga(T53, T54, T59)) → U40_ggaa(T53, T54, T59, T56, addC1_in_gga(T54, T59, T56))
U40_ggaa(T53, T54, T59, T56, addC1_out_gga(T54, T59, T56)) → pB_out_ggaa(T53, T54, T59, T56)
U2_gga(T53, T54, T56, pB_out_ggaa(T53, T54, X65, T56)) → timesA_out_gga(zero(one(T53)), T54, zero(T56))
timesA_in_gga(one(one(b)), T506, T501) → U3_gga(T506, T501, addC1_in_gga(T506, T506, T501))
U3_gga(T506, T501, addC1_out_gga(T506, T506, T501)) → timesA_out_gga(one(one(b)), T506, T501)
timesA_in_gga(one(zero(T515)), T516, T501) → U4_gga(T515, T516, T501, pD_in_ggaa(T515, T516, X531, T501))
pD_in_ggaa(T515, T516, T519, T501) → U43_ggaa(T515, T516, T519, T501, timesF_in_gga(T515, T516, T519))
U43_ggaa(T515, T516, T519, T501, timesF_out_gga(T515, T516, T519)) → U44_ggaa(T515, T516, T519, T501, addC1_in_gga(T516, zero(T519), T501))
U44_ggaa(T515, T516, T519, T501, addC1_out_gga(T516, zero(T519), T501)) → pD_out_ggaa(T515, T516, T519, T501)
U4_gga(T515, T516, T501, pD_out_ggaa(T515, T516, X531, T501)) → timesA_out_gga(one(zero(T515)), T516, T501)
timesA_in_gga(one(one(T526)), T527, T501) → U5_gga(T526, T527, T501, pE_in_ggaaa(T526, T527, X548, X549, T501))
pE_in_ggaaa(T526, T527, T530, X549, T501) → U45_ggaaa(T526, T527, T530, X549, T501, timesF_in_gga(T526, T527, T530))
U45_ggaaa(T526, T527, T530, X549, T501, timesF_out_gga(T526, T527, T530)) → U46_ggaaa(T526, T527, T530, X549, T501, pP_in_ggaa(T527, T530, X549, T501))
pP_in_ggaa(T527, T530, T533, T501) → U47_ggaa(T527, T530, T533, T501, addC1_in_gga(T527, T530, T533))
U47_ggaa(T527, T530, T533, T501, addC1_out_gga(T527, T530, T533)) → U48_ggaa(T527, T530, T533, T501, addC1_in_gga(T527, T533, T501))
U48_ggaa(T527, T530, T533, T501, addC1_out_gga(T527, T533, T501)) → pP_out_ggaa(T527, T530, T533, T501)
U46_ggaaa(T526, T527, T530, X549, T501, pP_out_ggaa(T527, T530, X549, T501)) → pE_out_ggaaa(T526, T527, T530, X549, T501)
U5_gga(T526, T527, T501, pE_out_ggaaa(T526, T527, X548, X549, T501)) → timesA_out_gga(one(one(T526)), T527, T501)
U1_gga(T35, T36, T38, timesA_out_gga(T35, T36, T38)) → timesA_out_gga(zero(zero(T35)), T36, zero(zero(T38)))

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

BINARYZH_IN_G(one(T113)) → BINARYK_IN_G(T113)
BINARYK_IN_G(zero(T118)) → BINARYZH_IN_G(T118)
BINARYZH_IN_G(zero(T109)) → BINARYZH_IN_G(T109)
BINARYK_IN_G(one(T122)) → BINARYK_IN_G(T122)

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

(10) PiDPToQDPProof (EQUIVALENT 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:

BINARYZH_IN_G(one(T113)) → BINARYK_IN_G(T113)
BINARYK_IN_G(zero(T118)) → BINARYZH_IN_G(T118)
BINARYZH_IN_G(zero(T109)) → BINARYZH_IN_G(T109)
BINARYK_IN_G(one(T122)) → BINARYK_IN_G(T122)

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:

BINARYK_IN_G(zero(T118)) → BINARYZH_IN_G(T118)
The graph contains the following edges 1 > 1
BINARYK_IN_G(one(T122)) → BINARYK_IN_G(T122)
The graph contains the following edges 1 > 1
BINARYZH_IN_G(zero(T109)) → BINARYZH_IN_G(T109)
The graph contains the following edges 1 > 1
BINARYZH_IN_G(one(T113)) → BINARYK_IN_G(T113)
The graph contains the following edges 1 > 1

(13) YES

(14) Obligation:

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

SUCCM_IN_GA(one(T313), zero(T315)) → SUCCM_IN_GA(T313, T315)

The TRS R consists of the following rules:

timesA_in_gga(one(b), T5, T5) → timesA_out_gga(one(b), T5, T5)
timesA_in_gga(zero(one(b)), T22, zero(T22)) → timesA_out_gga(zero(one(b)), T22, zero(T22))
timesA_in_gga(zero(zero(T35)), T36, zero(zero(T38))) → U1_gga(T35, T36, T38, timesA_in_gga(T35, T36, T38))
timesA_in_gga(zero(one(T53)), T54, zero(T56)) → U2_gga(T53, T54, T56, pB_in_ggaa(T53, T54, X65, T56))
pB_in_ggaa(T53, T54, T59, T56) → U39_ggaa(T53, T54, T59, T56, timesF_in_gga(T53, T54, T59))
timesF_in_gga(one(b), T66, T66) → timesF_out_gga(one(b), T66, T66)
timesF_in_gga(zero(T75), T76, zero(X94)) → U6_gga(T75, T76, X94, timesF_in_gga(T75, T76, X94))
timesF_in_gga(one(T83), T84, X110) → U7_gga(T83, T84, X110, pG_in_ggaa(T83, T84, X109, X110))
pG_in_ggaa(T83, T84, T87, X110) → U41_ggaa(T83, T84, T87, X110, timesF_in_gga(T83, T84, T87))
U41_ggaa(T83, T84, T87, X110, timesF_out_gga(T83, T84, T87)) → U42_ggaa(T83, T84, T87, X110, addC1_in_gga(T84, T87, X110))
addC1_in_gga(b, T103, zero(T103)) → U8_gga(T103, binaryZH_in_g(T103))
binaryZH_in_g(zero(T109)) → U11_g(T109, binaryZH_in_g(T109))
binaryZH_in_g(one(T113)) → U12_g(T113, binaryK_in_g(T113))
binaryK_in_g(b) → binaryK_out_g(b)
binaryK_in_g(zero(T118)) → U13_g(T118, binaryZH_in_g(T118))
U13_g(T118, binaryZH_out_g(T118)) → binaryK_out_g(zero(T118))
binaryK_in_g(one(T122)) → U14_g(T122, binaryK_in_g(T122))
U14_g(T122, binaryK_out_g(T122)) → binaryK_out_g(one(T122))
U12_g(T113, binaryK_out_g(T113)) → binaryZH_out_g(one(T113))
U11_g(T109, binaryZH_out_g(T109)) → binaryZH_out_g(zero(T109))
U8_gga(T103, binaryZH_out_g(T103)) → addC1_out_gga(b, T103, zero(T103))
addC1_in_gga(zero(T152), T153, zero(T155)) → U9_gga(T152, T153, T155, addzI_in_gga(T152, T153, T155))
addzI_in_gga(zero(T171), zero(T172), zero(T174)) → U15_gga(T171, T172, T174, addzI_in_gga(T171, T172, T174))
addzI_in_gga(zero(one(T199)), one(b), one(one(T199))) → U16_gga(T199, binaryK_in_g(T199))
U16_gga(T199, binaryK_out_g(T199)) → addzI_out_gga(zero(one(T199)), one(b), one(one(T199)))
addzI_in_gga(zero(zero(T204)), one(b), one(zero(T204))) → U17_gga(T204, binaryZH_in_g(T204))
U17_gga(T204, binaryZH_out_g(T204)) → addzI_out_gga(zero(zero(T204)), one(b), one(zero(T204)))
addzI_in_gga(zero(T216), one(T217), one(T219)) → U18_gga(T216, T217, T219, addzI_in_gga(T216, T217, T219))
addzI_in_gga(one(T235), zero(T236), one(T238)) → U19_gga(T235, T236, T238, addyJ_in_gga(T235, T236, T238))
addyJ_in_gga(b, one(T244), one(T244)) → U36_gga(T244, binaryK_in_g(T244))
U36_gga(T244, binaryK_out_g(T244)) → addyJ_out_gga(b, one(T244), one(T244))
addyJ_in_gga(b, zero(T249), zero(T249)) → U37_gga(T249, binaryZH_in_g(T249))
U37_gga(T249, binaryZH_out_g(T249)) → addyJ_out_gga(b, zero(T249), zero(T249))
addyJ_in_gga(T261, T262, T264) → U38_gga(T261, T262, T264, addzI_in_gga(T261, T262, T264))
addzI_in_gga(one(T274), one(T275), zero(T277)) → U20_gga(T274, T275, T277, addcL_in_gga(T274, T275, T277))
addcL_in_gga(b, b, one(b)) → addcL_out_gga(b, b, one(b))
addcL_in_gga(T286, b, T288) → U33_gga(T286, T288, succZN_in_ga(T286, T288))
succZN_in_ga(zero(T294), one(T294)) → U23_ga(T294, binaryZH_in_g(T294))
U23_ga(T294, binaryZH_out_g(T294)) → succZN_out_ga(zero(T294), one(T294))
succZN_in_ga(one(T300), zero(T302)) → U24_ga(T300, T302, succM_in_ga(T300, T302))
succM_in_ga(b, one(b)) → succM_out_ga(b, one(b))
succM_in_ga(zero(T307), one(T307)) → U21_ga(T307, binaryZH_in_g(T307))
U21_ga(T307, binaryZH_out_g(T307)) → succM_out_ga(zero(T307), one(T307))
succM_in_ga(one(T313), zero(T315)) → U22_ga(T313, T315, succM_in_ga(T313, T315))
U22_ga(T313, T315, succM_out_ga(T313, T315)) → succM_out_ga(one(T313), zero(T315))
U24_ga(T300, T302, succM_out_ga(T300, T302)) → succZN_out_ga(one(T300), zero(T302))
U33_gga(T286, T288, succZN_out_ga(T286, T288)) → addcL_out_gga(T286, b, T288)
addcL_in_gga(b, T324, T326) → U34_gga(T324, T326, succZN_in_ga(T324, T326))
U34_gga(T324, T326, succZN_out_ga(T324, T326)) → addcL_out_gga(b, T324, T326)
addcL_in_gga(T338, T339, T341) → U35_gga(T338, T339, T341, addCO_in_gga(T338, T339, T341))
addCO_in_gga(zero(T357), zero(T358), one(T360)) → U25_gga(T357, T358, T360, addzI_in_gga(T357, T358, T360))
U25_gga(T357, T358, T360, addzI_out_gga(T357, T358, T360)) → addCO_out_gga(zero(T357), zero(T358), one(T360))
addCO_in_gga(zero(zero(T385)), one(b), zero(one(T385))) → U26_gga(T385, binaryZH_in_g(T385))
U26_gga(T385, binaryZH_out_g(T385)) → addCO_out_gga(zero(zero(T385)), one(b), zero(one(T385)))
addCO_in_gga(zero(one(T395)), one(b), zero(zero(T397))) → U27_gga(T395, T397, succM_in_ga(T395, T397))
U27_gga(T395, T397, succM_out_ga(T395, T397)) → addCO_out_gga(zero(one(T395)), one(b), zero(zero(T397)))
addCO_in_gga(zero(T408), one(T409), zero(T411)) → U28_gga(T408, T409, T411, addCO_in_gga(T408, T409, T411))
addCO_in_gga(one(b), zero(zero(T436)), zero(one(T436))) → U29_gga(T436, binaryZH_in_g(T436))
U29_gga(T436, binaryZH_out_g(T436)) → addCO_out_gga(one(b), zero(zero(T436)), zero(one(T436)))
addCO_in_gga(one(b), zero(one(T446)), zero(zero(T448))) → U30_gga(T446, T448, succM_in_ga(T446, T448))
U30_gga(T446, T448, succM_out_ga(T446, T448)) → addCO_out_gga(one(b), zero(one(T446)), zero(zero(T448)))
addCO_in_gga(one(T459), zero(T460), zero(T462)) → U31_gga(T459, T460, T462, addCO_in_gga(T459, T460, T462))
addCO_in_gga(one(T472), one(T473), one(T475)) → U32_gga(T472, T473, T475, addcL_in_gga(T472, T473, T475))
U32_gga(T472, T473, T475, addcL_out_gga(T472, T473, T475)) → addCO_out_gga(one(T472), one(T473), one(T475))
U31_gga(T459, T460, T462, addCO_out_gga(T459, T460, T462)) → addCO_out_gga(one(T459), zero(T460), zero(T462))
U28_gga(T408, T409, T411, addCO_out_gga(T408, T409, T411)) → addCO_out_gga(zero(T408), one(T409), zero(T411))
U35_gga(T338, T339, T341, addCO_out_gga(T338, T339, T341)) → addcL_out_gga(T338, T339, T341)
U20_gga(T274, T275, T277, addcL_out_gga(T274, T275, T277)) → addzI_out_gga(one(T274), one(T275), zero(T277))
U38_gga(T261, T262, T264, addzI_out_gga(T261, T262, T264)) → addyJ_out_gga(T261, T262, T264)
U19_gga(T235, T236, T238, addyJ_out_gga(T235, T236, T238)) → addzI_out_gga(one(T235), zero(T236), one(T238))
U18_gga(T216, T217, T219, addzI_out_gga(T216, T217, T219)) → addzI_out_gga(zero(T216), one(T217), one(T219))
U15_gga(T171, T172, T174, addzI_out_gga(T171, T172, T174)) → addzI_out_gga(zero(T171), zero(T172), zero(T174))
U9_gga(T152, T153, T155, addzI_out_gga(T152, T153, T155)) → addC1_out_gga(zero(T152), T153, zero(T155))
addC1_in_gga(one(T489), T490, one(T492)) → U10_gga(T489, T490, T492, addyJ_in_gga(T489, T490, T492))
U10_gga(T489, T490, T492, addyJ_out_gga(T489, T490, T492)) → addC1_out_gga(one(T489), T490, one(T492))
U42_ggaa(T83, T84, T87, X110, addC1_out_gga(T84, T87, X110)) → pG_out_ggaa(T83, T84, T87, X110)
U7_gga(T83, T84, X110, pG_out_ggaa(T83, T84, X109, X110)) → timesF_out_gga(one(T83), T84, X110)
U6_gga(T75, T76, X94, timesF_out_gga(T75, T76, X94)) → timesF_out_gga(zero(T75), T76, zero(X94))
U39_ggaa(T53, T54, T59, T56, timesF_out_gga(T53, T54, T59)) → U40_ggaa(T53, T54, T59, T56, addC1_in_gga(T54, T59, T56))
U40_ggaa(T53, T54, T59, T56, addC1_out_gga(T54, T59, T56)) → pB_out_ggaa(T53, T54, T59, T56)
U2_gga(T53, T54, T56, pB_out_ggaa(T53, T54, X65, T56)) → timesA_out_gga(zero(one(T53)), T54, zero(T56))
timesA_in_gga(one(one(b)), T506, T501) → U3_gga(T506, T501, addC1_in_gga(T506, T506, T501))
U3_gga(T506, T501, addC1_out_gga(T506, T506, T501)) → timesA_out_gga(one(one(b)), T506, T501)
timesA_in_gga(one(zero(T515)), T516, T501) → U4_gga(T515, T516, T501, pD_in_ggaa(T515, T516, X531, T501))
pD_in_ggaa(T515, T516, T519, T501) → U43_ggaa(T515, T516, T519, T501, timesF_in_gga(T515, T516, T519))
U43_ggaa(T515, T516, T519, T501, timesF_out_gga(T515, T516, T519)) → U44_ggaa(T515, T516, T519, T501, addC1_in_gga(T516, zero(T519), T501))
U44_ggaa(T515, T516, T519, T501, addC1_out_gga(T516, zero(T519), T501)) → pD_out_ggaa(T515, T516, T519, T501)
U4_gga(T515, T516, T501, pD_out_ggaa(T515, T516, X531, T501)) → timesA_out_gga(one(zero(T515)), T516, T501)
timesA_in_gga(one(one(T526)), T527, T501) → U5_gga(T526, T527, T501, pE_in_ggaaa(T526, T527, X548, X549, T501))
pE_in_ggaaa(T526, T527, T530, X549, T501) → U45_ggaaa(T526, T527, T530, X549, T501, timesF_in_gga(T526, T527, T530))
U45_ggaaa(T526, T527, T530, X549, T501, timesF_out_gga(T526, T527, T530)) → U46_ggaaa(T526, T527, T530, X549, T501, pP_in_ggaa(T527, T530, X549, T501))
pP_in_ggaa(T527, T530, T533, T501) → U47_ggaa(T527, T530, T533, T501, addC1_in_gga(T527, T530, T533))
U47_ggaa(T527, T530, T533, T501, addC1_out_gga(T527, T530, T533)) → U48_ggaa(T527, T530, T533, T501, addC1_in_gga(T527, T533, T501))
U48_ggaa(T527, T530, T533, T501, addC1_out_gga(T527, T533, T501)) → pP_out_ggaa(T527, T530, T533, T501)
U46_ggaaa(T526, T527, T530, X549, T501, pP_out_ggaa(T527, T530, X549, T501)) → pE_out_ggaaa(T526, T527, T530, X549, T501)
U5_gga(T526, T527, T501, pE_out_ggaaa(T526, T527, X548, X549, T501)) → timesA_out_gga(one(one(T526)), T527, T501)
U1_gga(T35, T36, T38, timesA_out_gga(T35, T36, T38)) → timesA_out_gga(zero(zero(T35)), T36, zero(zero(T38)))

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

SUCCM_IN_GA(one(T313), zero(T315)) → SUCCM_IN_GA(T313, T315)

R is empty.
The argument filtering Pi contains the following mapping:
one(x1) = one(x1)
zero(x1) = zero(x1)
SUCCM_IN_GA(x1, x2) = SUCCM_IN_GA(x1)

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

(17) PiDPToQDPProof (SOUND transformation)

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

(18) Obligation:

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

SUCCM_IN_GA(one(T313)) → SUCCM_IN_GA(T313)

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:

SUCCM_IN_GA(one(T313)) → SUCCM_IN_GA(T313)
The graph contains the following edges 1 > 1

(20) YES

(21) Obligation:

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

ADDZI_IN_GGA(zero(T216), one(T217), one(T219)) → ADDZI_IN_GGA(T216, T217, T219)
ADDZI_IN_GGA(zero(T171), zero(T172), zero(T174)) → ADDZI_IN_GGA(T171, T172, T174)
ADDZI_IN_GGA(one(T235), zero(T236), one(T238)) → ADDYJ_IN_GGA(T235, T236, T238)
ADDYJ_IN_GGA(T261, T262, T264) → ADDZI_IN_GGA(T261, T262, T264)
ADDZI_IN_GGA(one(T274), one(T275), zero(T277)) → ADDCL_IN_GGA(T274, T275, T277)
ADDCL_IN_GGA(T338, T339, T341) → ADDCO_IN_GGA(T338, T339, T341)
ADDCO_IN_GGA(zero(T357), zero(T358), one(T360)) → ADDZI_IN_GGA(T357, T358, T360)
ADDCO_IN_GGA(zero(T408), one(T409), zero(T411)) → ADDCO_IN_GGA(T408, T409, T411)
ADDCO_IN_GGA(one(T459), zero(T460), zero(T462)) → ADDCO_IN_GGA(T459, T460, T462)
ADDCO_IN_GGA(one(T472), one(T473), one(T475)) → ADDCL_IN_GGA(T472, T473, T475)

The TRS R consists of the following rules:

timesA_in_gga(one(b), T5, T5) → timesA_out_gga(one(b), T5, T5)
timesA_in_gga(zero(one(b)), T22, zero(T22)) → timesA_out_gga(zero(one(b)), T22, zero(T22))
timesA_in_gga(zero(zero(T35)), T36, zero(zero(T38))) → U1_gga(T35, T36, T38, timesA_in_gga(T35, T36, T38))
timesA_in_gga(zero(one(T53)), T54, zero(T56)) → U2_gga(T53, T54, T56, pB_in_ggaa(T53, T54, X65, T56))
pB_in_ggaa(T53, T54, T59, T56) → U39_ggaa(T53, T54, T59, T56, timesF_in_gga(T53, T54, T59))
timesF_in_gga(one(b), T66, T66) → timesF_out_gga(one(b), T66, T66)
timesF_in_gga(zero(T75), T76, zero(X94)) → U6_gga(T75, T76, X94, timesF_in_gga(T75, T76, X94))
timesF_in_gga(one(T83), T84, X110) → U7_gga(T83, T84, X110, pG_in_ggaa(T83, T84, X109, X110))
pG_in_ggaa(T83, T84, T87, X110) → U41_ggaa(T83, T84, T87, X110, timesF_in_gga(T83, T84, T87))
U41_ggaa(T83, T84, T87, X110, timesF_out_gga(T83, T84, T87)) → U42_ggaa(T83, T84, T87, X110, addC1_in_gga(T84, T87, X110))
addC1_in_gga(b, T103, zero(T103)) → U8_gga(T103, binaryZH_in_g(T103))
binaryZH_in_g(zero(T109)) → U11_g(T109, binaryZH_in_g(T109))
binaryZH_in_g(one(T113)) → U12_g(T113, binaryK_in_g(T113))
binaryK_in_g(b) → binaryK_out_g(b)
binaryK_in_g(zero(T118)) → U13_g(T118, binaryZH_in_g(T118))
U13_g(T118, binaryZH_out_g(T118)) → binaryK_out_g(zero(T118))
binaryK_in_g(one(T122)) → U14_g(T122, binaryK_in_g(T122))
U14_g(T122, binaryK_out_g(T122)) → binaryK_out_g(one(T122))
U12_g(T113, binaryK_out_g(T113)) → binaryZH_out_g(one(T113))
U11_g(T109, binaryZH_out_g(T109)) → binaryZH_out_g(zero(T109))
U8_gga(T103, binaryZH_out_g(T103)) → addC1_out_gga(b, T103, zero(T103))
addC1_in_gga(zero(T152), T153, zero(T155)) → U9_gga(T152, T153, T155, addzI_in_gga(T152, T153, T155))
addzI_in_gga(zero(T171), zero(T172), zero(T174)) → U15_gga(T171, T172, T174, addzI_in_gga(T171, T172, T174))
addzI_in_gga(zero(one(T199)), one(b), one(one(T199))) → U16_gga(T199, binaryK_in_g(T199))
U16_gga(T199, binaryK_out_g(T199)) → addzI_out_gga(zero(one(T199)), one(b), one(one(T199)))
addzI_in_gga(zero(zero(T204)), one(b), one(zero(T204))) → U17_gga(T204, binaryZH_in_g(T204))
U17_gga(T204, binaryZH_out_g(T204)) → addzI_out_gga(zero(zero(T204)), one(b), one(zero(T204)))
addzI_in_gga(zero(T216), one(T217), one(T219)) → U18_gga(T216, T217, T219, addzI_in_gga(T216, T217, T219))
addzI_in_gga(one(T235), zero(T236), one(T238)) → U19_gga(T235, T236, T238, addyJ_in_gga(T235, T236, T238))
addyJ_in_gga(b, one(T244), one(T244)) → U36_gga(T244, binaryK_in_g(T244))
U36_gga(T244, binaryK_out_g(T244)) → addyJ_out_gga(b, one(T244), one(T244))
addyJ_in_gga(b, zero(T249), zero(T249)) → U37_gga(T249, binaryZH_in_g(T249))
U37_gga(T249, binaryZH_out_g(T249)) → addyJ_out_gga(b, zero(T249), zero(T249))
addyJ_in_gga(T261, T262, T264) → U38_gga(T261, T262, T264, addzI_in_gga(T261, T262, T264))
addzI_in_gga(one(T274), one(T275), zero(T277)) → U20_gga(T274, T275, T277, addcL_in_gga(T274, T275, T277))
addcL_in_gga(b, b, one(b)) → addcL_out_gga(b, b, one(b))
addcL_in_gga(T286, b, T288) → U33_gga(T286, T288, succZN_in_ga(T286, T288))
succZN_in_ga(zero(T294), one(T294)) → U23_ga(T294, binaryZH_in_g(T294))
U23_ga(T294, binaryZH_out_g(T294)) → succZN_out_ga(zero(T294), one(T294))
succZN_in_ga(one(T300), zero(T302)) → U24_ga(T300, T302, succM_in_ga(T300, T302))
succM_in_ga(b, one(b)) → succM_out_ga(b, one(b))
succM_in_ga(zero(T307), one(T307)) → U21_ga(T307, binaryZH_in_g(T307))
U21_ga(T307, binaryZH_out_g(T307)) → succM_out_ga(zero(T307), one(T307))
succM_in_ga(one(T313), zero(T315)) → U22_ga(T313, T315, succM_in_ga(T313, T315))
U22_ga(T313, T315, succM_out_ga(T313, T315)) → succM_out_ga(one(T313), zero(T315))
U24_ga(T300, T302, succM_out_ga(T300, T302)) → succZN_out_ga(one(T300), zero(T302))
U33_gga(T286, T288, succZN_out_ga(T286, T288)) → addcL_out_gga(T286, b, T288)
addcL_in_gga(b, T324, T326) → U34_gga(T324, T326, succZN_in_ga(T324, T326))
U34_gga(T324, T326, succZN_out_ga(T324, T326)) → addcL_out_gga(b, T324, T326)
addcL_in_gga(T338, T339, T341) → U35_gga(T338, T339, T341, addCO_in_gga(T338, T339, T341))
addCO_in_gga(zero(T357), zero(T358), one(T360)) → U25_gga(T357, T358, T360, addzI_in_gga(T357, T358, T360))
U25_gga(T357, T358, T360, addzI_out_gga(T357, T358, T360)) → addCO_out_gga(zero(T357), zero(T358), one(T360))
addCO_in_gga(zero(zero(T385)), one(b), zero(one(T385))) → U26_gga(T385, binaryZH_in_g(T385))
U26_gga(T385, binaryZH_out_g(T385)) → addCO_out_gga(zero(zero(T385)), one(b), zero(one(T385)))
addCO_in_gga(zero(one(T395)), one(b), zero(zero(T397))) → U27_gga(T395, T397, succM_in_ga(T395, T397))
U27_gga(T395, T397, succM_out_ga(T395, T397)) → addCO_out_gga(zero(one(T395)), one(b), zero(zero(T397)))
addCO_in_gga(zero(T408), one(T409), zero(T411)) → U28_gga(T408, T409, T411, addCO_in_gga(T408, T409, T411))
addCO_in_gga(one(b), zero(zero(T436)), zero(one(T436))) → U29_gga(T436, binaryZH_in_g(T436))
U29_gga(T436, binaryZH_out_g(T436)) → addCO_out_gga(one(b), zero(zero(T436)), zero(one(T436)))
addCO_in_gga(one(b), zero(one(T446)), zero(zero(T448))) → U30_gga(T446, T448, succM_in_ga(T446, T448))
U30_gga(T446, T448, succM_out_ga(T446, T448)) → addCO_out_gga(one(b), zero(one(T446)), zero(zero(T448)))
addCO_in_gga(one(T459), zero(T460), zero(T462)) → U31_gga(T459, T460, T462, addCO_in_gga(T459, T460, T462))
addCO_in_gga(one(T472), one(T473), one(T475)) → U32_gga(T472, T473, T475, addcL_in_gga(T472, T473, T475))
U32_gga(T472, T473, T475, addcL_out_gga(T472, T473, T475)) → addCO_out_gga(one(T472), one(T473), one(T475))
U31_gga(T459, T460, T462, addCO_out_gga(T459, T460, T462)) → addCO_out_gga(one(T459), zero(T460), zero(T462))
U28_gga(T408, T409, T411, addCO_out_gga(T408, T409, T411)) → addCO_out_gga(zero(T408), one(T409), zero(T411))
U35_gga(T338, T339, T341, addCO_out_gga(T338, T339, T341)) → addcL_out_gga(T338, T339, T341)
U20_gga(T274, T275, T277, addcL_out_gga(T274, T275, T277)) → addzI_out_gga(one(T274), one(T275), zero(T277))
U38_gga(T261, T262, T264, addzI_out_gga(T261, T262, T264)) → addyJ_out_gga(T261, T262, T264)
U19_gga(T235, T236, T238, addyJ_out_gga(T235, T236, T238)) → addzI_out_gga(one(T235), zero(T236), one(T238))
U18_gga(T216, T217, T219, addzI_out_gga(T216, T217, T219)) → addzI_out_gga(zero(T216), one(T217), one(T219))
U15_gga(T171, T172, T174, addzI_out_gga(T171, T172, T174)) → addzI_out_gga(zero(T171), zero(T172), zero(T174))
U9_gga(T152, T153, T155, addzI_out_gga(T152, T153, T155)) → addC1_out_gga(zero(T152), T153, zero(T155))
addC1_in_gga(one(T489), T490, one(T492)) → U10_gga(T489, T490, T492, addyJ_in_gga(T489, T490, T492))
U10_gga(T489, T490, T492, addyJ_out_gga(T489, T490, T492)) → addC1_out_gga(one(T489), T490, one(T492))
U42_ggaa(T83, T84, T87, X110, addC1_out_gga(T84, T87, X110)) → pG_out_ggaa(T83, T84, T87, X110)
U7_gga(T83, T84, X110, pG_out_ggaa(T83, T84, X109, X110)) → timesF_out_gga(one(T83), T84, X110)
U6_gga(T75, T76, X94, timesF_out_gga(T75, T76, X94)) → timesF_out_gga(zero(T75), T76, zero(X94))
U39_ggaa(T53, T54, T59, T56, timesF_out_gga(T53, T54, T59)) → U40_ggaa(T53, T54, T59, T56, addC1_in_gga(T54, T59, T56))
U40_ggaa(T53, T54, T59, T56, addC1_out_gga(T54, T59, T56)) → pB_out_ggaa(T53, T54, T59, T56)
U2_gga(T53, T54, T56, pB_out_ggaa(T53, T54, X65, T56)) → timesA_out_gga(zero(one(T53)), T54, zero(T56))
timesA_in_gga(one(one(b)), T506, T501) → U3_gga(T506, T501, addC1_in_gga(T506, T506, T501))
U3_gga(T506, T501, addC1_out_gga(T506, T506, T501)) → timesA_out_gga(one(one(b)), T506, T501)
timesA_in_gga(one(zero(T515)), T516, T501) → U4_gga(T515, T516, T501, pD_in_ggaa(T515, T516, X531, T501))
pD_in_ggaa(T515, T516, T519, T501) → U43_ggaa(T515, T516, T519, T501, timesF_in_gga(T515, T516, T519))
U43_ggaa(T515, T516, T519, T501, timesF_out_gga(T515, T516, T519)) → U44_ggaa(T515, T516, T519, T501, addC1_in_gga(T516, zero(T519), T501))
U44_ggaa(T515, T516, T519, T501, addC1_out_gga(T516, zero(T519), T501)) → pD_out_ggaa(T515, T516, T519, T501)
U4_gga(T515, T516, T501, pD_out_ggaa(T515, T516, X531, T501)) → timesA_out_gga(one(zero(T515)), T516, T501)
timesA_in_gga(one(one(T526)), T527, T501) → U5_gga(T526, T527, T501, pE_in_ggaaa(T526, T527, X548, X549, T501))
pE_in_ggaaa(T526, T527, T530, X549, T501) → U45_ggaaa(T526, T527, T530, X549, T501, timesF_in_gga(T526, T527, T530))
U45_ggaaa(T526, T527, T530, X549, T501, timesF_out_gga(T526, T527, T530)) → U46_ggaaa(T526, T527, T530, X549, T501, pP_in_ggaa(T527, T530, X549, T501))
pP_in_ggaa(T527, T530, T533, T501) → U47_ggaa(T527, T530, T533, T501, addC1_in_gga(T527, T530, T533))
U47_ggaa(T527, T530, T533, T501, addC1_out_gga(T527, T530, T533)) → U48_ggaa(T527, T530, T533, T501, addC1_in_gga(T527, T533, T501))
U48_ggaa(T527, T530, T533, T501, addC1_out_gga(T527, T533, T501)) → pP_out_ggaa(T527, T530, T533, T501)
U46_ggaaa(T526, T527, T530, X549, T501, pP_out_ggaa(T527, T530, X549, T501)) → pE_out_ggaaa(T526, T527, T530, X549, T501)
U5_gga(T526, T527, T501, pE_out_ggaaa(T526, T527, X548, X549, T501)) → timesA_out_gga(one(one(T526)), T527, T501)
U1_gga(T35, T36, T38, timesA_out_gga(T35, T36, T38)) → timesA_out_gga(zero(zero(T35)), T36, zero(zero(T38)))

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

ADDZI_IN_GGA(zero(T216), one(T217), one(T219)) → ADDZI_IN_GGA(T216, T217, T219)
ADDZI_IN_GGA(zero(T171), zero(T172), zero(T174)) → ADDZI_IN_GGA(T171, T172, T174)
ADDZI_IN_GGA(one(T235), zero(T236), one(T238)) → ADDYJ_IN_GGA(T235, T236, T238)
ADDYJ_IN_GGA(T261, T262, T264) → ADDZI_IN_GGA(T261, T262, T264)
ADDZI_IN_GGA(one(T274), one(T275), zero(T277)) → ADDCL_IN_GGA(T274, T275, T277)
ADDCL_IN_GGA(T338, T339, T341) → ADDCO_IN_GGA(T338, T339, T341)
ADDCO_IN_GGA(zero(T357), zero(T358), one(T360)) → ADDZI_IN_GGA(T357, T358, T360)
ADDCO_IN_GGA(zero(T408), one(T409), zero(T411)) → ADDCO_IN_GGA(T408, T409, T411)
ADDCO_IN_GGA(one(T459), zero(T460), zero(T462)) → ADDCO_IN_GGA(T459, T460, T462)
ADDCO_IN_GGA(one(T472), one(T473), one(T475)) → ADDCL_IN_GGA(T472, T473, T475)

R is empty.
The argument filtering Pi contains the following mapping:
one(x1) = one(x1)
zero(x1) = zero(x1)
ADDZI_IN_GGA(x1, x2, x3) = ADDZI_IN_GGA(x1, x2)
ADDYJ_IN_GGA(x1, x2, x3) = ADDYJ_IN_GGA(x1, x2)
ADDCL_IN_GGA(x1, x2, x3) = ADDCL_IN_GGA(x1, x2)
ADDCO_IN_GGA(x1, x2, x3) = ADDCO_IN_GGA(x1, x2)

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:

ADDZI_IN_GGA(zero(T216), one(T217)) → ADDZI_IN_GGA(T216, T217)
ADDZI_IN_GGA(zero(T171), zero(T172)) → ADDZI_IN_GGA(T171, T172)
ADDZI_IN_GGA(one(T235), zero(T236)) → ADDYJ_IN_GGA(T235, T236)
ADDYJ_IN_GGA(T261, T262) → ADDZI_IN_GGA(T261, T262)
ADDZI_IN_GGA(one(T274), one(T275)) → ADDCL_IN_GGA(T274, T275)
ADDCL_IN_GGA(T338, T339) → ADDCO_IN_GGA(T338, T339)
ADDCO_IN_GGA(zero(T357), zero(T358)) → ADDZI_IN_GGA(T357, T358)
ADDCO_IN_GGA(zero(T408), one(T409)) → ADDCO_IN_GGA(T408, T409)
ADDCO_IN_GGA(one(T459), zero(T460)) → ADDCO_IN_GGA(T459, T460)
ADDCO_IN_GGA(one(T472), one(T473)) → ADDCL_IN_GGA(T472, T473)

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

(26) QDPSizeChangeProof (EQUIVALENT transformation)

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

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

ADDYJ_IN_GGA(T261, T262) → ADDZI_IN_GGA(T261, T262)
The graph contains the following edges 1 >= 1, 2 >= 2
ADDCO_IN_GGA(zero(T357), zero(T358)) → ADDZI_IN_GGA(T357, T358)
The graph contains the following edges 1 > 1, 2 > 2
ADDZI_IN_GGA(one(T235), zero(T236)) → ADDYJ_IN_GGA(T235, T236)
The graph contains the following edges 1 > 1, 2 > 2
ADDZI_IN_GGA(one(T274), one(T275)) → ADDCL_IN_GGA(T274, T275)
The graph contains the following edges 1 > 1, 2 > 2
ADDCL_IN_GGA(T338, T339) → ADDCO_IN_GGA(T338, T339)
The graph contains the following edges 1 >= 1, 2 >= 2
ADDCO_IN_GGA(one(T472), one(T473)) → ADDCL_IN_GGA(T472, T473)
The graph contains the following edges 1 > 1, 2 > 2
ADDZI_IN_GGA(zero(T216), one(T217)) → ADDZI_IN_GGA(T216, T217)
The graph contains the following edges 1 > 1, 2 > 2
ADDZI_IN_GGA(zero(T171), zero(T172)) → ADDZI_IN_GGA(T171, T172)
The graph contains the following edges 1 > 1, 2 > 2
ADDCO_IN_GGA(zero(T408), one(T409)) → ADDCO_IN_GGA(T408, T409)
The graph contains the following edges 1 > 1, 2 > 2
ADDCO_IN_GGA(one(T459), zero(T460)) → ADDCO_IN_GGA(T459, T460)
The graph contains the following edges 1 > 1, 2 > 2

(27) YES

(28) Obligation:

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

TIMESF_IN_GGA(one(T83), T84, X110) → PG_IN_GGAA(T83, T84, X109, X110)
PG_IN_GGAA(T83, T84, T87, X110) → TIMESF_IN_GGA(T83, T84, T87)
TIMESF_IN_GGA(zero(T75), T76, zero(X94)) → TIMESF_IN_GGA(T75, T76, X94)

The TRS R consists of the following rules:

timesA_in_gga(one(b), T5, T5) → timesA_out_gga(one(b), T5, T5)
timesA_in_gga(zero(one(b)), T22, zero(T22)) → timesA_out_gga(zero(one(b)), T22, zero(T22))
timesA_in_gga(zero(zero(T35)), T36, zero(zero(T38))) → U1_gga(T35, T36, T38, timesA_in_gga(T35, T36, T38))
timesA_in_gga(zero(one(T53)), T54, zero(T56)) → U2_gga(T53, T54, T56, pB_in_ggaa(T53, T54, X65, T56))
pB_in_ggaa(T53, T54, T59, T56) → U39_ggaa(T53, T54, T59, T56, timesF_in_gga(T53, T54, T59))
timesF_in_gga(one(b), T66, T66) → timesF_out_gga(one(b), T66, T66)
timesF_in_gga(zero(T75), T76, zero(X94)) → U6_gga(T75, T76, X94, timesF_in_gga(T75, T76, X94))
timesF_in_gga(one(T83), T84, X110) → U7_gga(T83, T84, X110, pG_in_ggaa(T83, T84, X109, X110))
pG_in_ggaa(T83, T84, T87, X110) → U41_ggaa(T83, T84, T87, X110, timesF_in_gga(T83, T84, T87))
U41_ggaa(T83, T84, T87, X110, timesF_out_gga(T83, T84, T87)) → U42_ggaa(T83, T84, T87, X110, addC1_in_gga(T84, T87, X110))
addC1_in_gga(b, T103, zero(T103)) → U8_gga(T103, binaryZH_in_g(T103))
binaryZH_in_g(zero(T109)) → U11_g(T109, binaryZH_in_g(T109))
binaryZH_in_g(one(T113)) → U12_g(T113, binaryK_in_g(T113))
binaryK_in_g(b) → binaryK_out_g(b)
binaryK_in_g(zero(T118)) → U13_g(T118, binaryZH_in_g(T118))
U13_g(T118, binaryZH_out_g(T118)) → binaryK_out_g(zero(T118))
binaryK_in_g(one(T122)) → U14_g(T122, binaryK_in_g(T122))
U14_g(T122, binaryK_out_g(T122)) → binaryK_out_g(one(T122))
U12_g(T113, binaryK_out_g(T113)) → binaryZH_out_g(one(T113))
U11_g(T109, binaryZH_out_g(T109)) → binaryZH_out_g(zero(T109))
U8_gga(T103, binaryZH_out_g(T103)) → addC1_out_gga(b, T103, zero(T103))
addC1_in_gga(zero(T152), T153, zero(T155)) → U9_gga(T152, T153, T155, addzI_in_gga(T152, T153, T155))
addzI_in_gga(zero(T171), zero(T172), zero(T174)) → U15_gga(T171, T172, T174, addzI_in_gga(T171, T172, T174))
addzI_in_gga(zero(one(T199)), one(b), one(one(T199))) → U16_gga(T199, binaryK_in_g(T199))
U16_gga(T199, binaryK_out_g(T199)) → addzI_out_gga(zero(one(T199)), one(b), one(one(T199)))
addzI_in_gga(zero(zero(T204)), one(b), one(zero(T204))) → U17_gga(T204, binaryZH_in_g(T204))
U17_gga(T204, binaryZH_out_g(T204)) → addzI_out_gga(zero(zero(T204)), one(b), one(zero(T204)))
addzI_in_gga(zero(T216), one(T217), one(T219)) → U18_gga(T216, T217, T219, addzI_in_gga(T216, T217, T219))
addzI_in_gga(one(T235), zero(T236), one(T238)) → U19_gga(T235, T236, T238, addyJ_in_gga(T235, T236, T238))
addyJ_in_gga(b, one(T244), one(T244)) → U36_gga(T244, binaryK_in_g(T244))
U36_gga(T244, binaryK_out_g(T244)) → addyJ_out_gga(b, one(T244), one(T244))
addyJ_in_gga(b, zero(T249), zero(T249)) → U37_gga(T249, binaryZH_in_g(T249))
U37_gga(T249, binaryZH_out_g(T249)) → addyJ_out_gga(b, zero(T249), zero(T249))
addyJ_in_gga(T261, T262, T264) → U38_gga(T261, T262, T264, addzI_in_gga(T261, T262, T264))
addzI_in_gga(one(T274), one(T275), zero(T277)) → U20_gga(T274, T275, T277, addcL_in_gga(T274, T275, T277))
addcL_in_gga(b, b, one(b)) → addcL_out_gga(b, b, one(b))
addcL_in_gga(T286, b, T288) → U33_gga(T286, T288, succZN_in_ga(T286, T288))
succZN_in_ga(zero(T294), one(T294)) → U23_ga(T294, binaryZH_in_g(T294))
U23_ga(T294, binaryZH_out_g(T294)) → succZN_out_ga(zero(T294), one(T294))
succZN_in_ga(one(T300), zero(T302)) → U24_ga(T300, T302, succM_in_ga(T300, T302))
succM_in_ga(b, one(b)) → succM_out_ga(b, one(b))
succM_in_ga(zero(T307), one(T307)) → U21_ga(T307, binaryZH_in_g(T307))
U21_ga(T307, binaryZH_out_g(T307)) → succM_out_ga(zero(T307), one(T307))
succM_in_ga(one(T313), zero(T315)) → U22_ga(T313, T315, succM_in_ga(T313, T315))
U22_ga(T313, T315, succM_out_ga(T313, T315)) → succM_out_ga(one(T313), zero(T315))
U24_ga(T300, T302, succM_out_ga(T300, T302)) → succZN_out_ga(one(T300), zero(T302))
U33_gga(T286, T288, succZN_out_ga(T286, T288)) → addcL_out_gga(T286, b, T288)
addcL_in_gga(b, T324, T326) → U34_gga(T324, T326, succZN_in_ga(T324, T326))
U34_gga(T324, T326, succZN_out_ga(T324, T326)) → addcL_out_gga(b, T324, T326)
addcL_in_gga(T338, T339, T341) → U35_gga(T338, T339, T341, addCO_in_gga(T338, T339, T341))
addCO_in_gga(zero(T357), zero(T358), one(T360)) → U25_gga(T357, T358, T360, addzI_in_gga(T357, T358, T360))
U25_gga(T357, T358, T360, addzI_out_gga(T357, T358, T360)) → addCO_out_gga(zero(T357), zero(T358), one(T360))
addCO_in_gga(zero(zero(T385)), one(b), zero(one(T385))) → U26_gga(T385, binaryZH_in_g(T385))
U26_gga(T385, binaryZH_out_g(T385)) → addCO_out_gga(zero(zero(T385)), one(b), zero(one(T385)))
addCO_in_gga(zero(one(T395)), one(b), zero(zero(T397))) → U27_gga(T395, T397, succM_in_ga(T395, T397))
U27_gga(T395, T397, succM_out_ga(T395, T397)) → addCO_out_gga(zero(one(T395)), one(b), zero(zero(T397)))
addCO_in_gga(zero(T408), one(T409), zero(T411)) → U28_gga(T408, T409, T411, addCO_in_gga(T408, T409, T411))
addCO_in_gga(one(b), zero(zero(T436)), zero(one(T436))) → U29_gga(T436, binaryZH_in_g(T436))
U29_gga(T436, binaryZH_out_g(T436)) → addCO_out_gga(one(b), zero(zero(T436)), zero(one(T436)))
addCO_in_gga(one(b), zero(one(T446)), zero(zero(T448))) → U30_gga(T446, T448, succM_in_ga(T446, T448))
U30_gga(T446, T448, succM_out_ga(T446, T448)) → addCO_out_gga(one(b), zero(one(T446)), zero(zero(T448)))
addCO_in_gga(one(T459), zero(T460), zero(T462)) → U31_gga(T459, T460, T462, addCO_in_gga(T459, T460, T462))
addCO_in_gga(one(T472), one(T473), one(T475)) → U32_gga(T472, T473, T475, addcL_in_gga(T472, T473, T475))
U32_gga(T472, T473, T475, addcL_out_gga(T472, T473, T475)) → addCO_out_gga(one(T472), one(T473), one(T475))
U31_gga(T459, T460, T462, addCO_out_gga(T459, T460, T462)) → addCO_out_gga(one(T459), zero(T460), zero(T462))
U28_gga(T408, T409, T411, addCO_out_gga(T408, T409, T411)) → addCO_out_gga(zero(T408), one(T409), zero(T411))
U35_gga(T338, T339, T341, addCO_out_gga(T338, T339, T341)) → addcL_out_gga(T338, T339, T341)
U20_gga(T274, T275, T277, addcL_out_gga(T274, T275, T277)) → addzI_out_gga(one(T274), one(T275), zero(T277))
U38_gga(T261, T262, T264, addzI_out_gga(T261, T262, T264)) → addyJ_out_gga(T261, T262, T264)
U19_gga(T235, T236, T238, addyJ_out_gga(T235, T236, T238)) → addzI_out_gga(one(T235), zero(T236), one(T238))
U18_gga(T216, T217, T219, addzI_out_gga(T216, T217, T219)) → addzI_out_gga(zero(T216), one(T217), one(T219))
U15_gga(T171, T172, T174, addzI_out_gga(T171, T172, T174)) → addzI_out_gga(zero(T171), zero(T172), zero(T174))
U9_gga(T152, T153, T155, addzI_out_gga(T152, T153, T155)) → addC1_out_gga(zero(T152), T153, zero(T155))
addC1_in_gga(one(T489), T490, one(T492)) → U10_gga(T489, T490, T492, addyJ_in_gga(T489, T490, T492))
U10_gga(T489, T490, T492, addyJ_out_gga(T489, T490, T492)) → addC1_out_gga(one(T489), T490, one(T492))
U42_ggaa(T83, T84, T87, X110, addC1_out_gga(T84, T87, X110)) → pG_out_ggaa(T83, T84, T87, X110)
U7_gga(T83, T84, X110, pG_out_ggaa(T83, T84, X109, X110)) → timesF_out_gga(one(T83), T84, X110)
U6_gga(T75, T76, X94, timesF_out_gga(T75, T76, X94)) → timesF_out_gga(zero(T75), T76, zero(X94))
U39_ggaa(T53, T54, T59, T56, timesF_out_gga(T53, T54, T59)) → U40_ggaa(T53, T54, T59, T56, addC1_in_gga(T54, T59, T56))
U40_ggaa(T53, T54, T59, T56, addC1_out_gga(T54, T59, T56)) → pB_out_ggaa(T53, T54, T59, T56)
U2_gga(T53, T54, T56, pB_out_ggaa(T53, T54, X65, T56)) → timesA_out_gga(zero(one(T53)), T54, zero(T56))
timesA_in_gga(one(one(b)), T506, T501) → U3_gga(T506, T501, addC1_in_gga(T506, T506, T501))
U3_gga(T506, T501, addC1_out_gga(T506, T506, T501)) → timesA_out_gga(one(one(b)), T506, T501)
timesA_in_gga(one(zero(T515)), T516, T501) → U4_gga(T515, T516, T501, pD_in_ggaa(T515, T516, X531, T501))
pD_in_ggaa(T515, T516, T519, T501) → U43_ggaa(T515, T516, T519, T501, timesF_in_gga(T515, T516, T519))
U43_ggaa(T515, T516, T519, T501, timesF_out_gga(T515, T516, T519)) → U44_ggaa(T515, T516, T519, T501, addC1_in_gga(T516, zero(T519), T501))
U44_ggaa(T515, T516, T519, T501, addC1_out_gga(T516, zero(T519), T501)) → pD_out_ggaa(T515, T516, T519, T501)
U4_gga(T515, T516, T501, pD_out_ggaa(T515, T516, X531, T501)) → timesA_out_gga(one(zero(T515)), T516, T501)
timesA_in_gga(one(one(T526)), T527, T501) → U5_gga(T526, T527, T501, pE_in_ggaaa(T526, T527, X548, X549, T501))
pE_in_ggaaa(T526, T527, T530, X549, T501) → U45_ggaaa(T526, T527, T530, X549, T501, timesF_in_gga(T526, T527, T530))
U45_ggaaa(T526, T527, T530, X549, T501, timesF_out_gga(T526, T527, T530)) → U46_ggaaa(T526, T527, T530, X549, T501, pP_in_ggaa(T527, T530, X549, T501))
pP_in_ggaa(T527, T530, T533, T501) → U47_ggaa(T527, T530, T533, T501, addC1_in_gga(T527, T530, T533))
U47_ggaa(T527, T530, T533, T501, addC1_out_gga(T527, T530, T533)) → U48_ggaa(T527, T530, T533, T501, addC1_in_gga(T527, T533, T501))
U48_ggaa(T527, T530, T533, T501, addC1_out_gga(T527, T533, T501)) → pP_out_ggaa(T527, T530, T533, T501)
U46_ggaaa(T526, T527, T530, X549, T501, pP_out_ggaa(T527, T530, X549, T501)) → pE_out_ggaaa(T526, T527, T530, X549, T501)
U5_gga(T526, T527, T501, pE_out_ggaaa(T526, T527, X548, X549, T501)) → timesA_out_gga(one(one(T526)), T527, T501)
U1_gga(T35, T36, T38, timesA_out_gga(T35, T36, T38)) → timesA_out_gga(zero(zero(T35)), T36, zero(zero(T38)))

(29) UsableRulesProof (EQUIVALENT transformation)

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

(30) Obligation:

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

TIMESF_IN_GGA(one(T83), T84, X110) → PG_IN_GGAA(T83, T84, X109, X110)
PG_IN_GGAA(T83, T84, T87, X110) → TIMESF_IN_GGA(T83, T84, T87)
TIMESF_IN_GGA(zero(T75), T76, zero(X94)) → TIMESF_IN_GGA(T75, T76, X94)

R is empty.
The argument filtering Pi contains the following mapping:
one(x1) = one(x1)
zero(x1) = zero(x1)
TIMESF_IN_GGA(x1, x2, x3) = TIMESF_IN_GGA(x1, x2)
PG_IN_GGAA(x1, x2, x3, x4) = PG_IN_GGAA(x1, x2)

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

(31) PiDPToQDPProof (SOUND transformation)

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

(32) Obligation:

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

TIMESF_IN_GGA(one(T83), T84) → PG_IN_GGAA(T83, T84)
PG_IN_GGAA(T83, T84) → TIMESF_IN_GGA(T83, T84)
TIMESF_IN_GGA(zero(T75), T76) → TIMESF_IN_GGA(T75, T76)

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

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

PG_IN_GGAA(T83, T84) → TIMESF_IN_GGA(T83, T84)
The graph contains the following edges 1 >= 1, 2 >= 2
TIMESF_IN_GGA(zero(T75), T76) → TIMESF_IN_GGA(T75, T76)
The graph contains the following edges 1 > 1, 2 >= 2
TIMESF_IN_GGA(one(T83), T84) → PG_IN_GGAA(T83, T84)
The graph contains the following edges 1 > 1, 2 >= 2

(34) YES

(35) Obligation:

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

TIMESA_IN_GGA(zero(zero(T35)), T36, zero(zero(T38))) → TIMESA_IN_GGA(T35, T36, T38)

The TRS R consists of the following rules:

timesA_in_gga(one(b), T5, T5) → timesA_out_gga(one(b), T5, T5)
timesA_in_gga(zero(one(b)), T22, zero(T22)) → timesA_out_gga(zero(one(b)), T22, zero(T22))
timesA_in_gga(zero(zero(T35)), T36, zero(zero(T38))) → U1_gga(T35, T36, T38, timesA_in_gga(T35, T36, T38))
timesA_in_gga(zero(one(T53)), T54, zero(T56)) → U2_gga(T53, T54, T56, pB_in_ggaa(T53, T54, X65, T56))
pB_in_ggaa(T53, T54, T59, T56) → U39_ggaa(T53, T54, T59, T56, timesF_in_gga(T53, T54, T59))
timesF_in_gga(one(b), T66, T66) → timesF_out_gga(one(b), T66, T66)
timesF_in_gga(zero(T75), T76, zero(X94)) → U6_gga(T75, T76, X94, timesF_in_gga(T75, T76, X94))
timesF_in_gga(one(T83), T84, X110) → U7_gga(T83, T84, X110, pG_in_ggaa(T83, T84, X109, X110))
pG_in_ggaa(T83, T84, T87, X110) → U41_ggaa(T83, T84, T87, X110, timesF_in_gga(T83, T84, T87))
U41_ggaa(T83, T84, T87, X110, timesF_out_gga(T83, T84, T87)) → U42_ggaa(T83, T84, T87, X110, addC1_in_gga(T84, T87, X110))
addC1_in_gga(b, T103, zero(T103)) → U8_gga(T103, binaryZH_in_g(T103))
binaryZH_in_g(zero(T109)) → U11_g(T109, binaryZH_in_g(T109))
binaryZH_in_g(one(T113)) → U12_g(T113, binaryK_in_g(T113))
binaryK_in_g(b) → binaryK_out_g(b)
binaryK_in_g(zero(T118)) → U13_g(T118, binaryZH_in_g(T118))
U13_g(T118, binaryZH_out_g(T118)) → binaryK_out_g(zero(T118))
binaryK_in_g(one(T122)) → U14_g(T122, binaryK_in_g(T122))
U14_g(T122, binaryK_out_g(T122)) → binaryK_out_g(one(T122))
U12_g(T113, binaryK_out_g(T113)) → binaryZH_out_g(one(T113))
U11_g(T109, binaryZH_out_g(T109)) → binaryZH_out_g(zero(T109))
U8_gga(T103, binaryZH_out_g(T103)) → addC1_out_gga(b, T103, zero(T103))
addC1_in_gga(zero(T152), T153, zero(T155)) → U9_gga(T152, T153, T155, addzI_in_gga(T152, T153, T155))
addzI_in_gga(zero(T171), zero(T172), zero(T174)) → U15_gga(T171, T172, T174, addzI_in_gga(T171, T172, T174))
addzI_in_gga(zero(one(T199)), one(b), one(one(T199))) → U16_gga(T199, binaryK_in_g(T199))
U16_gga(T199, binaryK_out_g(T199)) → addzI_out_gga(zero(one(T199)), one(b), one(one(T199)))
addzI_in_gga(zero(zero(T204)), one(b), one(zero(T204))) → U17_gga(T204, binaryZH_in_g(T204))
U17_gga(T204, binaryZH_out_g(T204)) → addzI_out_gga(zero(zero(T204)), one(b), one(zero(T204)))
addzI_in_gga(zero(T216), one(T217), one(T219)) → U18_gga(T216, T217, T219, addzI_in_gga(T216, T217, T219))
addzI_in_gga(one(T235), zero(T236), one(T238)) → U19_gga(T235, T236, T238, addyJ_in_gga(T235, T236, T238))
addyJ_in_gga(b, one(T244), one(T244)) → U36_gga(T244, binaryK_in_g(T244))
U36_gga(T244, binaryK_out_g(T244)) → addyJ_out_gga(b, one(T244), one(T244))
addyJ_in_gga(b, zero(T249), zero(T249)) → U37_gga(T249, binaryZH_in_g(T249))
U37_gga(T249, binaryZH_out_g(T249)) → addyJ_out_gga(b, zero(T249), zero(T249))
addyJ_in_gga(T261, T262, T264) → U38_gga(T261, T262, T264, addzI_in_gga(T261, T262, T264))
addzI_in_gga(one(T274), one(T275), zero(T277)) → U20_gga(T274, T275, T277, addcL_in_gga(T274, T275, T277))
addcL_in_gga(b, b, one(b)) → addcL_out_gga(b, b, one(b))
addcL_in_gga(T286, b, T288) → U33_gga(T286, T288, succZN_in_ga(T286, T288))
succZN_in_ga(zero(T294), one(T294)) → U23_ga(T294, binaryZH_in_g(T294))
U23_ga(T294, binaryZH_out_g(T294)) → succZN_out_ga(zero(T294), one(T294))
succZN_in_ga(one(T300), zero(T302)) → U24_ga(T300, T302, succM_in_ga(T300, T302))
succM_in_ga(b, one(b)) → succM_out_ga(b, one(b))
succM_in_ga(zero(T307), one(T307)) → U21_ga(T307, binaryZH_in_g(T307))
U21_ga(T307, binaryZH_out_g(T307)) → succM_out_ga(zero(T307), one(T307))
succM_in_ga(one(T313), zero(T315)) → U22_ga(T313, T315, succM_in_ga(T313, T315))
U22_ga(T313, T315, succM_out_ga(T313, T315)) → succM_out_ga(one(T313), zero(T315))
U24_ga(T300, T302, succM_out_ga(T300, T302)) → succZN_out_ga(one(T300), zero(T302))
U33_gga(T286, T288, succZN_out_ga(T286, T288)) → addcL_out_gga(T286, b, T288)
addcL_in_gga(b, T324, T326) → U34_gga(T324, T326, succZN_in_ga(T324, T326))
U34_gga(T324, T326, succZN_out_ga(T324, T326)) → addcL_out_gga(b, T324, T326)
addcL_in_gga(T338, T339, T341) → U35_gga(T338, T339, T341, addCO_in_gga(T338, T339, T341))
addCO_in_gga(zero(T357), zero(T358), one(T360)) → U25_gga(T357, T358, T360, addzI_in_gga(T357, T358, T360))
U25_gga(T357, T358, T360, addzI_out_gga(T357, T358, T360)) → addCO_out_gga(zero(T357), zero(T358), one(T360))
addCO_in_gga(zero(zero(T385)), one(b), zero(one(T385))) → U26_gga(T385, binaryZH_in_g(T385))
U26_gga(T385, binaryZH_out_g(T385)) → addCO_out_gga(zero(zero(T385)), one(b), zero(one(T385)))
addCO_in_gga(zero(one(T395)), one(b), zero(zero(T397))) → U27_gga(T395, T397, succM_in_ga(T395, T397))
U27_gga(T395, T397, succM_out_ga(T395, T397)) → addCO_out_gga(zero(one(T395)), one(b), zero(zero(T397)))
addCO_in_gga(zero(T408), one(T409), zero(T411)) → U28_gga(T408, T409, T411, addCO_in_gga(T408, T409, T411))
addCO_in_gga(one(b), zero(zero(T436)), zero(one(T436))) → U29_gga(T436, binaryZH_in_g(T436))
U29_gga(T436, binaryZH_out_g(T436)) → addCO_out_gga(one(b), zero(zero(T436)), zero(one(T436)))
addCO_in_gga(one(b), zero(one(T446)), zero(zero(T448))) → U30_gga(T446, T448, succM_in_ga(T446, T448))
U30_gga(T446, T448, succM_out_ga(T446, T448)) → addCO_out_gga(one(b), zero(one(T446)), zero(zero(T448)))
addCO_in_gga(one(T459), zero(T460), zero(T462)) → U31_gga(T459, T460, T462, addCO_in_gga(T459, T460, T462))
addCO_in_gga(one(T472), one(T473), one(T475)) → U32_gga(T472, T473, T475, addcL_in_gga(T472, T473, T475))
U32_gga(T472, T473, T475, addcL_out_gga(T472, T473, T475)) → addCO_out_gga(one(T472), one(T473), one(T475))
U31_gga(T459, T460, T462, addCO_out_gga(T459, T460, T462)) → addCO_out_gga(one(T459), zero(T460), zero(T462))
U28_gga(T408, T409, T411, addCO_out_gga(T408, T409, T411)) → addCO_out_gga(zero(T408), one(T409), zero(T411))
U35_gga(T338, T339, T341, addCO_out_gga(T338, T339, T341)) → addcL_out_gga(T338, T339, T341)
U20_gga(T274, T275, T277, addcL_out_gga(T274, T275, T277)) → addzI_out_gga(one(T274), one(T275), zero(T277))
U38_gga(T261, T262, T264, addzI_out_gga(T261, T262, T264)) → addyJ_out_gga(T261, T262, T264)
U19_gga(T235, T236, T238, addyJ_out_gga(T235, T236, T238)) → addzI_out_gga(one(T235), zero(T236), one(T238))
U18_gga(T216, T217, T219, addzI_out_gga(T216, T217, T219)) → addzI_out_gga(zero(T216), one(T217), one(T219))
U15_gga(T171, T172, T174, addzI_out_gga(T171, T172, T174)) → addzI_out_gga(zero(T171), zero(T172), zero(T174))
U9_gga(T152, T153, T155, addzI_out_gga(T152, T153, T155)) → addC1_out_gga(zero(T152), T153, zero(T155))
addC1_in_gga(one(T489), T490, one(T492)) → U10_gga(T489, T490, T492, addyJ_in_gga(T489, T490, T492))
U10_gga(T489, T490, T492, addyJ_out_gga(T489, T490, T492)) → addC1_out_gga(one(T489), T490, one(T492))
U42_ggaa(T83, T84, T87, X110, addC1_out_gga(T84, T87, X110)) → pG_out_ggaa(T83, T84, T87, X110)
U7_gga(T83, T84, X110, pG_out_ggaa(T83, T84, X109, X110)) → timesF_out_gga(one(T83), T84, X110)
U6_gga(T75, T76, X94, timesF_out_gga(T75, T76, X94)) → timesF_out_gga(zero(T75), T76, zero(X94))
U39_ggaa(T53, T54, T59, T56, timesF_out_gga(T53, T54, T59)) → U40_ggaa(T53, T54, T59, T56, addC1_in_gga(T54, T59, T56))
U40_ggaa(T53, T54, T59, T56, addC1_out_gga(T54, T59, T56)) → pB_out_ggaa(T53, T54, T59, T56)
U2_gga(T53, T54, T56, pB_out_ggaa(T53, T54, X65, T56)) → timesA_out_gga(zero(one(T53)), T54, zero(T56))
timesA_in_gga(one(one(b)), T506, T501) → U3_gga(T506, T501, addC1_in_gga(T506, T506, T501))
U3_gga(T506, T501, addC1_out_gga(T506, T506, T501)) → timesA_out_gga(one(one(b)), T506, T501)
timesA_in_gga(one(zero(T515)), T516, T501) → U4_gga(T515, T516, T501, pD_in_ggaa(T515, T516, X531, T501))
pD_in_ggaa(T515, T516, T519, T501) → U43_ggaa(T515, T516, T519, T501, timesF_in_gga(T515, T516, T519))
U43_ggaa(T515, T516, T519, T501, timesF_out_gga(T515, T516, T519)) → U44_ggaa(T515, T516, T519, T501, addC1_in_gga(T516, zero(T519), T501))
U44_ggaa(T515, T516, T519, T501, addC1_out_gga(T516, zero(T519), T501)) → pD_out_ggaa(T515, T516, T519, T501)
U4_gga(T515, T516, T501, pD_out_ggaa(T515, T516, X531, T501)) → timesA_out_gga(one(zero(T515)), T516, T501)
timesA_in_gga(one(one(T526)), T527, T501) → U5_gga(T526, T527, T501, pE_in_ggaaa(T526, T527, X548, X549, T501))
pE_in_ggaaa(T526, T527, T530, X549, T501) → U45_ggaaa(T526, T527, T530, X549, T501, timesF_in_gga(T526, T527, T530))
U45_ggaaa(T526, T527, T530, X549, T501, timesF_out_gga(T526, T527, T530)) → U46_ggaaa(T526, T527, T530, X549, T501, pP_in_ggaa(T527, T530, X549, T501))
pP_in_ggaa(T527, T530, T533, T501) → U47_ggaa(T527, T530, T533, T501, addC1_in_gga(T527, T530, T533))
U47_ggaa(T527, T530, T533, T501, addC1_out_gga(T527, T530, T533)) → U48_ggaa(T527, T530, T533, T501, addC1_in_gga(T527, T533, T501))
U48_ggaa(T527, T530, T533, T501, addC1_out_gga(T527, T533, T501)) → pP_out_ggaa(T527, T530, T533, T501)
U46_ggaaa(T526, T527, T530, X549, T501, pP_out_ggaa(T527, T530, X549, T501)) → pE_out_ggaaa(T526, T527, T530, X549, T501)
U5_gga(T526, T527, T501, pE_out_ggaaa(T526, T527, X548, X549, T501)) → timesA_out_gga(one(one(T526)), T527, T501)
U1_gga(T35, T36, T38, timesA_out_gga(T35, T36, T38)) → timesA_out_gga(zero(zero(T35)), T36, zero(zero(T38)))

(36) UsableRulesProof (EQUIVALENT transformation)

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

(37) Obligation:

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

TIMESA_IN_GGA(zero(zero(T35)), T36, zero(zero(T38))) → TIMESA_IN_GGA(T35, T36, T38)

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

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

(38) PiDPToQDPProof (SOUND transformation)

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

(39) Obligation:

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

TIMESA_IN_GGA(zero(zero(T35)), T36) → TIMESA_IN_GGA(T35, T36)

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

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

TIMESA_IN_GGA(zero(zero(T35)), T36) → TIMESA_IN_GGA(T35, T36)
The graph contains the following edges 1 > 1, 2 >= 2

(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 (EQUIVALENT 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) QDPSizeChangeProof (EQUIVALENT transformation)

(27) YES

(28) Obligation:

(29) UsableRulesProof (EQUIVALENT transformation)

(30) Obligation:

(31) PiDPToQDPProof (SOUND transformation)

(32) Obligation:

(33) QDPSizeChangeProof (EQUIVALENT transformation)

(34) YES

(35) Obligation:

(36) UsableRulesProof (EQUIVALENT transformation)

(37) Obligation:

(38) PiDPToQDPProof (SOUND transformation)

(39) Obligation:

(40) QDPSizeChangeProof (EQUIVALENT transformation)

(41) YES