Left Termination proof of /tmp/tmpRBLAiF/divremain.pl

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

0 Prolog

↳1 PrologToPrologProblemTransformerProof (⇐)

↳2 Prolog

↳3 PrologToPiTRSProof (⇐)

↳4 PiTRS

↳5 DependencyPairsProof (⇔)

↳6 PiDP

↳7 DependencyGraphProof (⇔)

↳8 AND

    ↳9 PiDP

        ↳10 UsableRulesProof (⇔)

            ↳11 PiDP

                ↳12 PiDPToQDPProof (⇐)

                    ↳13 QDP

                        ↳14 QDPSizeChangeProof (⇔)

                            ↳15 TRUE

    ↳16 PiDP

        ↳17 UsableRulesProof (⇔)

            ↳18 PiDP

                ↳19 PiDPToQDPProof (⇐)

                    ↳20 QDP

                        ↳21 QDPSizeChangeProof (⇔)

                            ↳22 TRUE

    ↳23 PiDP

        ↳24 UsableRulesProof (⇔)

            ↳25 PiDP

                ↳26 PiDPToQDPProof (⇐)

                    ↳27 QDP

                        ↳28 QDPSizeChangeProof (⇔)

                            ↳29 TRUE

    ↳30 PiDP

        ↳31 UsableRulesProof (⇔)

            ↳32 PiDP

                ↳33 PiDPToQDPProof (⇐)

                    ↳34 QDP

                        ↳35 QDPSizeChangeProof (⇔)

                            ↳36 TRUE

    ↳37 PiDP

        ↳38 UsableRulesProof (⇔)

            ↳39 PiDP

                ↳40 PiDPToQDPProof (⇐)

                    ↳41 QDP

                        ↳42 QDPSizeChangeProof (⇔)

                            ↳43 TRUE

    ↳44 PiDP

        ↳45 UsableRulesProof (⇔)

            ↳46 PiDP

                ↳47 PiDPToQDPProof (⇐)

                    ↳48 QDP

                        ↳49 QDPSizeChangeProof (⇔)

                            ↳50 TRUE

    ↳51 PiDP

        ↳52 UsableRulesProof (⇔)

            ↳53 PiDP

                ↳54 PiDPToQDPProof (⇐)

                    ↳55 QDP

                        ↳56 QDPSizeChangeProof (⇔)

                            ↳57 TRUE

    ↳58 PiDP

        ↳59 UsableRulesProof (⇔)

            ↳60 PiDP

                ↳61 PiDPToQDPProof (⇐)

                    ↳62 QDP

                        ↳63 QDPSizeChangeProof (⇔)

                            ↳64 TRUE

    ↳65 PiDP

        ↳66 UsableRulesProof (⇔)

            ↳67 PiDP

                ↳68 PiDPToQDPProof (⇐)

                    ↳69 QDP

                        ↳70 MRRProof (⇔)

                            ↳71 QDP

                                ↳72 PisEmptyProof (⇔)

                                    ↳73 TRUE

(0) Obligation:

Clauses:

div(X1, 0, X2, X3) :- ','(!, failure(a)).
div(0, X4, Z, R) :- ','(!, ','(eq(Z, 0), eq(R, 0))).
div(X, Y, s(Z), R) :- ','(minus(X, Y, U), ','(!, div(U, Y, Z, R))).
div(X, X5, X6, X).
minus(X, 0, X).
minus(s(X), s(Y), Z) :- minus(X, Y, Z).
failure(b).
eq(X, X).

Queries:

div(g,g,a,a).

(1) PrologToPrologProblemTransformerProof (SOUND transformation)

Built Prolog problem from termination graph.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
1 [label="1: div(T1, T2, T3, T4)\n\nT1 is ground\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
2 [label="2: div(T1, T2, T3, T4), SCOPE: 1, CLAUSE: 0 | div(T1, T2, T3, T4), SCOPE: 1, CLAUSE: 1 | div(T1, T2, T3, T4), SCOPE: 1, CLAUSE: 2 | div(T1, T2, T3, T4), SCOPE: 1, CLAUSE: 3 | ?_1\n\nT1 is ground\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
3 [label="3: ','(!_1, failure(a)) | div(T5, 0, T3, T4), SCOPE: 1, CLAUSE: 1 | div(T5, 0, T3, T4), SCOPE: 1, CLAUSE: 2 | div(T5, 0, T3, T4), SCOPE: 1, CLAUSE: 3 | ?_1\n\nT5 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
4 [label="4: div(T1, T2, T3, T4), SCOPE: 1, CLAUSE: 1 | div(T1, T2, T3, T4), SCOPE: 1, CLAUSE: 2 | div(T1, T2, T3, T4), SCOPE: 1, CLAUSE: 3 | ?_1\n\nT1 is ground\nT2 is ground\nX10 is free; \nX11 is free; \nX12 is free; \ndiv(T1, T2, T3, T4) !=? div(X10, 0, X11, X12)", fontsize=16, style=filled, fillcolor=lightyellow];
5 [label="5: failure(a)\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
6 [label="6: failure(a), SCOPE: 2, CLAUSE: 6\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
7 [label="7: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
8 [label="8: ','(!_1, ','(eq(T11, 0), eq(T12, 0))) | div(0, T8, T3, T4), SCOPE: 1, CLAUSE: 2 | div(0, T8, T3, T4), SCOPE: 1, CLAUSE: 3 | ?_1\n\nT8 is ground\nX10 is free; \nX11 is free; \nX12 is free; \ndiv(0, T8, T3, T4) !=? div(X10, 0, X11, X12)", fontsize=16, style=filled, fillcolor=lightyellow];
9 [label="9: div(T1, T2, T3, T4), SCOPE: 1, CLAUSE: 2 | div(T1, T2, T3, T4), SCOPE: 1, CLAUSE: 3 | ?_1\n\nT1 is ground\nT2 is ground\nX10 is free; \nX11 is free; \nX12 is free; \nX16 is free; \nX17 is free; \nX18 is free; \ndiv(T1, T2, T3, T4) !=? div(X10, 0, X11, X12)\ndiv(T1, T2, T3, T4) !=? div(0, X16, X17, X18)", fontsize=16, style=filled, fillcolor=lightyellow];
10 [label="10: ','(eq(T11, 0), eq(T12, 0))\n\nX10 is free\nX11 is free; \nX12 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
11 [label="11: ','(eq(T11, 0), eq(T12, 0)), SCOPE: 3, CLAUSE: 7\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
12 [label="12: eq(T14, 0)\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
13 [label="13: \n\nX20 is free", fontsize=16, style=filled, fillcolor=lightyellow];
14 [label="14: eq(T14, 0), SCOPE: 4, CLAUSE: 7\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
15 [label="15: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
16 [label="16: \n\nX22 is free", fontsize=16, style=filled, fillcolor=lightyellow];
17 [label="17: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
18 [label="18: ','(minus(T16, T17, X31), ','(!_1, div(X31, T17, T20, T21))) | div(T16, T17, T3, T4), SCOPE: 1, CLAUSE: 3 | ?_1\n\nT16 is ground\nT17 is ground\nX10 is free; \nX11 is free; \nX12 is free; \nX16 is free; \nX17 is free; \nX18 is free; \nX31 is free; \ndiv(T16, T17, T3, T4) !=? div(X10, 0, X11, X12)\ndiv(T16, T17, T3, T4) !=? div(0, X16, X17, X18)", fontsize=16, style=filled, fillcolor=lightyellow];
19 [label="19: div(T1, T2, T3, T4), SCOPE: 1, CLAUSE: 3\n\nT1 is ground\nT2 is ground\nX10 is free; \nX11 is free; \nX12 is free; \nX16 is free; \nX17 is free; \nX18 is free; \nX27 is free; \nX28 is free; \nX29 is free; \nX30 is free; \ndiv(T1, T2, T3, T4) !=? div(X10, 0, X11, X12)\ndiv(T1, T2, T3, T4) !=? div(0, X16, X17, X18)\ndiv(T1, T2, T3, T4) !=? div(X27, X28, s(X29), X30)", fontsize=16, style=filled, fillcolor=lightyellow];
20 [label="20: ','(minus(T16, T17, X31), ','(!_1, div(X31, T17, T20, T21))), SCOPE: 5, CLAUSE: 4 | ','(minus(T16, T17, X31), ','(!_1, div(X31, T17, T20, T21))), SCOPE: 5, CLAUSE: 5 | div(T16, T17, T3, T4), SCOPE: 1, CLAUSE: 3 | ?_1\n\nT16 is ground\nT17 is ground\nX10 is free; \nX11 is free; \nX12 is free; \nX16 is free; \nX17 is free; \nX18 is free; \nX31 is free; \ndiv(T16, T17, T3, T4) !=? div(X10, 0, X11, X12)\ndiv(T16, T17, T3, T4) !=? div(0, X16, X17, X18)", fontsize=16, style=filled, fillcolor=lightyellow];
21 [label="21: ','(minus(T16, T17, X31), ','(!_1, div(X31, T17, T20, T21))), SCOPE: 5, CLAUSE: 5 | div(T16, T17, T3, T4), SCOPE: 1, CLAUSE: 3 | ?_1\n\nT16 is ground\nT17 is ground\nX10 is free; \nX11 is free; \nX12 is free; \nX16 is free; \nX17 is free; \nX18 is free; \nX31 is free; \nX33 is free; \ndiv(T16, T17, T3, T4) !=? div(X10, 0, X11, X12)\ndiv(T16, T17, T3, T4) !=? div(0, X16, X17, X18)\nminus(T16, T17, X31) !=? minus(X33, 0, X33)", fontsize=16, style=filled, fillcolor=lightyellow];
22 [label="22: ','(minus(T22, T23, X40), ','(!_1, div(X40, s(T23), T20, T21))) | div(s(T22), s(T23), T3, T4), SCOPE: 1, CLAUSE: 3 | ?_1\n\nT22 is ground\nT23 is ground\nX10 is free; \nX11 is free; \nX12 is free; \nX16 is free; \nX17 is free; \nX18 is free; \nX31 is free; \nX33 is free; \nX40 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
23 [label="23: div(T16, T17, T3, T4), SCOPE: 1, CLAUSE: 3\n\nT16 is ground\nT17 is ground\nX10 is free; \nX11 is free; \nX12 is free; \nX16 is free; \nX17 is free; \nX18 is free; \nX31 is free; \nX33 is free; \nX37 is free; \nX38 is free; \nX39 is free; \ndiv(T16, T17, T3, T4) !=? div(X10, 0, X11, X12)\ndiv(T16, T17, T3, T4) !=? div(0, X16, X17, X18)\nminus(T16, T17, X31) !=? minus(X33, 0, X33)\nminus(T16, T17, X31) !=? minus(s(X37), s(X38), X39)", fontsize=16, style=filled, fillcolor=lightyellow];
24 [label="24: ','(minus(T22, T23, X40), ','(!_1, div(X40, s(T23), T20, T21))), SCOPE: 6, CLAUSE: 4 | ','(minus(T22, T23, X40), ','(!_1, div(X40, s(T23), T20, T21))), SCOPE: 6, CLAUSE: 5 | div(s(T22), s(T23), T3, T4), SCOPE: 1, CLAUSE: 3 | ?_1\n\nT22 is ground\nT23 is ground\nX40 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
25 [label="25: ','(!_1, div(T24, s(0), T20, T21)) | ','(minus(T24, 0, X40), ','(!_1, div(X40, s(0), T20, T21))), SCOPE: 6, CLAUSE: 5 | div(s(T24), s(0), T3, T4), SCOPE: 1, CLAUSE: 3 | ?_1\n\nT24 is ground\nX40 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
26 [label="26: ','(minus(T22, T23, X40), ','(!_1, div(X40, s(T23), T20, T21))), SCOPE: 6, CLAUSE: 5 | div(s(T22), s(T23), T3, T4), SCOPE: 1, CLAUSE: 3 | ?_1\n\nT22 is ground\nT23 is ground\nX40 is free; \nX42 is free; \nminus(T22, T23, X40) !=? minus(X42, 0, X42)", fontsize=16, style=filled, fillcolor=lightyellow];
27 [label="27: div(T24, s(0), T20, T21)\n\nT24 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
28 [label="28: ','(minus(T25, T26, X49), ','(!_1, div(X49, s(s(T26)), T20, T21))) | div(s(s(T25)), s(s(T26)), T3, T4), SCOPE: 1, CLAUSE: 3 | ?_1\n\nT25 is ground\nT26 is ground\nX40 is free; \nX42 is free; \nX49 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
29 [label="29: div(s(T22), s(T23), T3, T4), SCOPE: 1, CLAUSE: 3\n\nT22 is ground\nT23 is ground\nX40 is free; \nX42 is free; \nX46 is free; \nX47 is free; \nX48 is free; \nminus(T22, T23, X40) !=? minus(X42, 0, X42)\nminus(T22, T23, X40) !=? minus(s(X46), s(X47), X48)", fontsize=16, style=filled, fillcolor=lightyellow];
30 [label="30: ','(minus(T25, T26, X49), ','(!_1, div(X49, s(s(T26)), T20, T21))), SCOPE: 7, CLAUSE: 4 | ','(minus(T25, T26, X49), ','(!_1, div(X49, s(s(T26)), T20, T21))), SCOPE: 7, CLAUSE: 5 | div(s(s(T25)), s(s(T26)), T3, T4), SCOPE: 1, CLAUSE: 3 | ?_1\n\nT25 is ground\nT26 is ground\nX49 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
31 [label="31: ','(!_1, div(T27, s(s(0)), T20, T21)) | ','(minus(T27, 0, X49), ','(!_1, div(X49, s(s(0)), T20, T21))), SCOPE: 7, CLAUSE: 5 | div(s(s(T27)), s(s(0)), T3, T4), SCOPE: 1, CLAUSE: 3 | ?_1\n\nT27 is ground\nX49 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
32 [label="32: ','(minus(T25, T26, X49), ','(!_1, div(X49, s(s(T26)), T20, T21))), SCOPE: 7, CLAUSE: 5 | div(s(s(T25)), s(s(T26)), T3, T4), SCOPE: 1, CLAUSE: 3 | ?_1\n\nT25 is ground\nT26 is ground\nX49 is free; \nX51 is free; \nminus(T25, T26, X49) !=? minus(X51, 0, X51)", fontsize=16, style=filled, fillcolor=lightyellow];
33 [label="33: div(T27, s(s(0)), T20, T21)\n\nT27 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
34 [label="34: ','(minus(T28, T29, X58), ','(!_1, div(X58, s(s(s(T29))), T20, T21))) | div(s(s(s(T28))), s(s(s(T29))), T3, T4), SCOPE: 1, CLAUSE: 3 | ?_1\n\nT28 is ground\nT29 is ground\nX49 is free; \nX51 is free; \nX58 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
35 [label="35: div(s(s(T25)), s(s(T26)), T3, T4), SCOPE: 1, CLAUSE: 3\n\nT25 is ground\nT26 is ground\nX49 is free; \nX51 is free; \nX55 is free; \nX56 is free; \nX57 is free; \nminus(T25, T26, X49) !=? minus(X51, 0, X51)\nminus(T25, T26, X49) !=? minus(s(X55), s(X56), X57)", fontsize=16, style=filled, fillcolor=lightyellow];
36 [label="36: ','(minus(T28, T29, X58), ','(!_1, div(X58, s(s(s(T29))), T20, T21))), SCOPE: 8, CLAUSE: 4 | ','(minus(T28, T29, X58), ','(!_1, div(X58, s(s(s(T29))), T20, T21))), SCOPE: 8, CLAUSE: 5 | div(s(s(s(T28))), s(s(s(T29))), T3, T4), SCOPE: 1, CLAUSE: 3 | ?_1\n\nT28 is ground\nT29 is ground\nX58 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
37 [label="37: ','(!_1, div(T30, s(s(s(0))), T20, T21)) | ','(minus(T30, 0, X58), ','(!_1, div(X58, s(s(s(0))), T20, T21))), SCOPE: 8, CLAUSE: 5 | div(s(s(s(T30))), s(s(s(0))), T3, T4), SCOPE: 1, CLAUSE: 3 | ?_1\n\nT30 is ground\nX58 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
38 [label="38: ','(minus(T28, T29, X58), ','(!_1, div(X58, s(s(s(T29))), T20, T21))), SCOPE: 8, CLAUSE: 5 | div(s(s(s(T28))), s(s(s(T29))), T3, T4), SCOPE: 1, CLAUSE: 3 | ?_1\n\nT28 is ground\nT29 is ground\nX58 is free; \nX60 is free; \nminus(T28, T29, X58) !=? minus(X60, 0, X60)", fontsize=16, style=filled, fillcolor=lightyellow];
39 [label="39: div(T30, s(s(s(0))), T20, T21)\n\nT30 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
40 [label="40: ','(minus(T31, T32, X67), ','(!_1, div(X67, s(s(s(s(T32)))), T20, T21))) | div(s(s(s(s(T31)))), s(s(s(s(T32)))), T3, T4), SCOPE: 1, CLAUSE: 3 | ?_1\n\nT31 is ground\nT32 is ground\nX58 is free; \nX60 is free; \nX67 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
41 [label="41: div(s(s(s(T28))), s(s(s(T29))), T3, T4), SCOPE: 1, CLAUSE: 3\n\nT28 is ground\nT29 is ground\nX58 is free; \nX60 is free; \nX64 is free; \nX65 is free; \nX66 is free; \nminus(T28, T29, X58) !=? minus(X60, 0, X60)\nminus(T28, T29, X58) !=? minus(s(X64), s(X65), X66)", fontsize=16, style=filled, fillcolor=lightyellow];
42 [label="42: ','(minus(T31, T32, X67), ','(!_1, div(X67, s(s(s(s(T32)))), T20, T21))), SCOPE: 9, CLAUSE: 4 | ','(minus(T31, T32, X67), ','(!_1, div(X67, s(s(s(s(T32)))), T20, T21))), SCOPE: 9, CLAUSE: 5 | div(s(s(s(s(T31)))), s(s(s(s(T32)))), T3, T4), SCOPE: 1, CLAUSE: 3 | ?_1\n\nT31 is ground\nT32 is ground\nX67 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
43 [label="43: ','(!_1, div(T33, s(s(s(s(0)))), T20, T21)) | ','(minus(T33, 0, X67), ','(!_1, div(X67, s(s(s(s(0)))), T20, T21))), SCOPE: 9, CLAUSE: 5 | div(s(s(s(s(T33)))), s(s(s(s(0)))), T3, T4), SCOPE: 1, CLAUSE: 3 | ?_1\n\nT33 is ground\nX67 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
44 [label="44: ','(minus(T31, T32, X67), ','(!_1, div(X67, s(s(s(s(T32)))), T20, T21))), SCOPE: 9, CLAUSE: 5 | div(s(s(s(s(T31)))), s(s(s(s(T32)))), T3, T4), SCOPE: 1, CLAUSE: 3 | ?_1\n\nT31 is ground\nT32 is ground\nX67 is free; \nX69 is free; \nminus(T31, T32, X67) !=? minus(X69, 0, X69)", fontsize=16, style=filled, fillcolor=lightyellow];
45 [label="45: div(T33, s(s(s(s(0)))), T20, T21)\n\nT33 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
46 [label="46: ','(minus(T34, T35, X76), ','(!_1, div(X76, s(s(s(s(s(T35))))), T20, T21))) | div(s(s(s(s(s(T34))))), s(s(s(s(s(T35))))), T3, T4), SCOPE: 1, CLAUSE: 3 | ?_1\n\nT34 is ground\nT35 is ground\nX67 is free; \nX69 is free; \nX76 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
47 [label="47: div(s(s(s(s(T31)))), s(s(s(s(T32)))), T3, T4), SCOPE: 1, CLAUSE: 3\n\nT31 is ground\nT32 is ground\nX67 is free; \nX69 is free; \nX73 is free; \nX74 is free; \nX75 is free; \nminus(T31, T32, X67) !=? minus(X69, 0, X69)\nminus(T31, T32, X67) !=? minus(s(X73), s(X74), X75)", fontsize=16, style=filled, fillcolor=lightyellow];
48 [label="48: ','(minus(T34, T35, X76), ','(!_1, div(X76, s(s(s(s(s(T35))))), T20, T21))), SCOPE: 10, CLAUSE: 4 | ','(minus(T34, T35, X76), ','(!_1, div(X76, s(s(s(s(s(T35))))), T20, T21))), SCOPE: 10, CLAUSE: 5 | div(s(s(s(s(s(T34))))), s(s(s(s(s(T35))))), T3, T4), SCOPE: 1, CLAUSE: 3 | ?_1\n\nT34 is ground\nT35 is ground\nX76 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
49 [label="49: ','(!_1, div(T36, s(s(s(s(s(0))))), T20, T21)) | ','(minus(T36, 0, X76), ','(!_1, div(X76, s(s(s(s(s(0))))), T20, T21))), SCOPE: 10, CLAUSE: 5 | div(s(s(s(s(s(T36))))), s(s(s(s(s(0))))), T3, T4), SCOPE: 1, CLAUSE: 3 | ?_1\n\nT36 is ground\nX76 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
50 [label="50: ','(minus(T34, T35, X76), ','(!_1, div(X76, s(s(s(s(s(T35))))), T20, T21))), SCOPE: 10, CLAUSE: 5 | div(s(s(s(s(s(T34))))), s(s(s(s(s(T35))))), T3, T4), SCOPE: 1, CLAUSE: 3 | ?_1\n\nT34 is ground\nT35 is ground\nX76 is free; \nX78 is free; \nminus(T34, T35, X76) !=? minus(X78, 0, X78)", fontsize=16, style=filled, fillcolor=lightyellow];
51 [label="51: div(T36, s(s(s(s(s(0))))), T20, T21)\n\nT36 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
52 [label="52: ','(minus(T37, T38, X85), ','(!_1, div(X85, s(s(s(s(s(s(T38)))))), T20, T21))) | div(s(s(s(s(s(s(T37)))))), s(s(s(s(s(s(T38)))))), T3, T4), SCOPE: 1, CLAUSE: 3 | ?_1\n\nT37 is ground\nT38 is ground\nX76 is free; \nX78 is free; \nX85 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
53 [label="53: div(s(s(s(s(s(T34))))), s(s(s(s(s(T35))))), T3, T4), SCOPE: 1, CLAUSE: 3\n\nT34 is ground\nT35 is ground\nX76 is free; \nX78 is free; \nX82 is free; \nX83 is free; \nX84 is free; \nminus(T34, T35, X76) !=? minus(X78, 0, X78)\nminus(T34, T35, X76) !=? minus(s(X82), s(X83), X84)", fontsize=16, style=filled, fillcolor=lightyellow];
54 [label="54: ','(minus(T37, T38, X85), ','(!_1, div(X85, s(s(s(s(s(s(T38)))))), T20, T21))), SCOPE: 11, CLAUSE: 4 | ','(minus(T37, T38, X85), ','(!_1, div(X85, s(s(s(s(s(s(T38)))))), T20, T21))), SCOPE: 11, CLAUSE: 5 | div(s(s(s(s(s(s(T37)))))), s(s(s(s(s(s(T38)))))), T3, T4), SCOPE: 1, CLAUSE: 3 | ?_1\n\nT37 is ground\nT38 is ground\nX85 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
55 [label="55: ','(!_1, div(T39, s(s(s(s(s(s(0)))))), T20, T21)) | ','(minus(T39, 0, X85), ','(!_1, div(X85, s(s(s(s(s(s(0)))))), T20, T21))), SCOPE: 11, CLAUSE: 5 | div(s(s(s(s(s(s(T39)))))), s(s(s(s(s(s(0)))))), T3, T4), SCOPE: 1, CLAUSE: 3 | ?_1\n\nT39 is ground\nX85 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
56 [label="56: ','(minus(T37, T38, X85), ','(!_1, div(X85, s(s(s(s(s(s(T38)))))), T20, T21))), SCOPE: 11, CLAUSE: 5 | div(s(s(s(s(s(s(T37)))))), s(s(s(s(s(s(T38)))))), T3, T4), SCOPE: 1, CLAUSE: 3 | ?_1\n\nT37 is ground\nT38 is ground\nX85 is free; \nX87 is free; \nminus(T37, T38, X85) !=? minus(X87, 0, X87)", fontsize=16, style=filled, fillcolor=lightyellow];
57 [label="57: div(T39, s(s(s(s(s(s(0)))))), T20, T21)\n\nT39 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
58 [label="58: ','(minus(T40, T41, X94), ','(!_1, div(X94, s(s(s(s(s(s(s(T41))))))), T20, T21))) | div(s(s(s(s(s(s(s(T40))))))), s(s(s(s(s(s(s(T41))))))), T3, T4), SCOPE: 1, CLAUSE: 3 | ?_1\n\nT40 is ground\nT41 is ground\nX85 is free; \nX87 is free; \nX94 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
59 [label="59: div(s(s(s(s(s(s(T37)))))), s(s(s(s(s(s(T38)))))), T3, T4), SCOPE: 1, CLAUSE: 3\n\nT37 is ground\nT38 is ground\nX85 is free; \nX87 is free; \nX91 is free; \nX92 is free; \nX93 is free; \nminus(T37, T38, X85) !=? minus(X87, 0, X87)\nminus(T37, T38, X85) !=? minus(s(X91), s(X92), X93)", fontsize=16, style=filled, fillcolor=lightyellow];
60 [label="60: ','(minus(T40, T41, X94), ','(!_1, div(X94, s(T42), T20, T21)))\n\nT40 is ground\nT41 is ground\nT42 is ground\nX94 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
61 [label="61: minus(T40, T41, X94)\n\nT40 is ground\nT41 is ground\nX94 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
62 [label="62: ','(!_1, div(T43, s(T42), T20, T21))\n\nT42 is ground\nT43 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
63 [label="63: minus(T40, T41, X94), SCOPE: 12, CLAUSE: 4 | minus(T40, T41, X94), SCOPE: 12, CLAUSE: 5\n\nT40 is ground\nT41 is ground\nX94 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
64 [label="64: minus(T40, T41, X94), SCOPE: 12, CLAUSE: 4\n\nT40 is ground\nT41 is ground\nX94 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
65 [label="65: minus(T40, T41, X94), SCOPE: 12, CLAUSE: 5\n\nT40 is ground\nT41 is ground\nX94 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
66 [label="66: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
67 [label="67: \n\nX94 is free\nX97 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
68 [label="68: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
69 [label="69: minus(T45, T46, X104)\n\nT45 is ground\nT46 is ground\nX104 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
70 [label="70: \n\nX94 is free\nX101 is free; \nX102 is free; \nX103 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
71 [label="71: div(T43, s(T42), T20, T21)\n\nT42 is ground\nT43 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
72 [label="72: true\n\nX85 is free\nX87 is free; \nX91 is free; \nX92 is free; \nX93 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
73 [label="73: \n\nX85 is free\nX87 is free; \nX91 is free; \nX92 is free; \nX93 is free; \nX108 is free; \nX109 is free; \nX110 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
74 [label="74: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
75 [label="75: true\n\nX76 is free\nX78 is free; \nX82 is free; \nX83 is free; \nX84 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
76 [label="76: \n\nX76 is free\nX78 is free; \nX82 is free; \nX83 is free; \nX84 is free; \nX114 is free; \nX115 is free; \nX116 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
77 [label="77: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
78 [label="78: true\n\nX67 is free\nX69 is free; \nX73 is free; \nX74 is free; \nX75 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
79 [label="79: \n\nX67 is free\nX69 is free; \nX73 is free; \nX74 is free; \nX75 is free; \nX120 is free; \nX121 is free; \nX122 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
80 [label="80: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
81 [label="81: true\n\nX58 is free\nX60 is free; \nX64 is free; \nX65 is free; \nX66 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
82 [label="82: \n\nX58 is free\nX60 is free; \nX64 is free; \nX65 is free; \nX66 is free; \nX126 is free; \nX127 is free; \nX128 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
83 [label="83: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
84 [label="84: true\n\nX49 is free\nX51 is free; \nX55 is free; \nX56 is free; \nX57 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
85 [label="85: \n\nX49 is free\nX51 is free; \nX55 is free; \nX56 is free; \nX57 is free; \nX132 is free; \nX133 is free; \nX134 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
86 [label="86: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
87 [label="87: true\n\nX40 is free\nX42 is free; \nX46 is free; \nX47 is free; \nX48 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
88 [label="88: \n\nX40 is free\nX42 is free; \nX46 is free; \nX47 is free; \nX48 is free; \nX138 is free; \nX139 is free; \nX140 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
89 [label="89: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
90 [label="90: true\n\nX10 is free\nX11 is free; \nX12 is free; \nX16 is free; \nX17 is free; \nX18 is free; \nX31 is free; \nX33 is free; \nX37 is free; \nX38 is free; \nX39 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
91 [label="91: \n\nX10 is free\nX11 is free; \nX12 is free; \nX16 is free; \nX17 is free; \nX18 is free; \nX31 is free; \nX33 is free; \nX37 is free; \nX38 is free; \nX39 is free; \nX144 is free; \nX145 is free; \nX146 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
92 [label="92: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
93 [label="93: true\n\nX10 is free\nX11 is free; \nX12 is free; \nX16 is free; \nX17 is free; \nX18 is free; \nX27 is free; \nX28 is free; \nX29 is free; \nX30 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
94 [label="94: \n\nX10 is free\nX11 is free; \nX12 is free; \nX16 is free; \nX17 is free; \nX18 is free; \nX27 is free; \nX28 is free; \nX29 is free; \nX30 is free; \nX150 is free; \nX151 is free; \nX152 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
95 [label="95: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
96 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
1 -> 96 [arrowhead = none ];
96 -> 2;

97 [label="EVAL with clause\ndiv(X10, 0, X11, X12) :- ','(!, failure(a)).\nand substitution\nT1 -> T5\nX10 -> T5\nT2 -> 0\nT3 -> T6\nX11 -> T6\nT4 -> T7\nX12 -> T7", fontsize=14, style = filled, fillcolor = lightblue];
2 -> 97 [arrowhead = none ];
97 -> 3;

98 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
2 -> 98 [arrowhead = none ];
98 -> 4;

99 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
3 -> 99 [arrowhead = none ];
99 -> 5;

100 [label="EVAL with clause\ndiv(0, X16, X17, X18) :- ','(!, ','(eq(X17, 0), eq(X18, 0))).\nand substitution\nT1 -> 0\nT2 -> T8\nX16 -> T8\nT3 -> T11\nX17 -> T11\nT4 -> T12\nX18 -> T12\nT9 -> T11\nT10 -> T12", fontsize=14, style = filled, fillcolor = lightblue];
4 -> 100 [arrowhead = none ];
100 -> 8;

101 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
4 -> 101 [arrowhead = none ];
101 -> 9;

102 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
5 -> 102 [arrowhead = none ];
102 -> 6;

103 [label="BACKTRACK\nfor clause: failure(b)because of non-unification", fontsize=14, style = filled, fillcolor = white];
6 -> 103 [arrowhead = none ];
103 -> 7;

104 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
8 -> 104 [arrowhead = none ];
104 -> 10;

105 [label="EVAL with clause\ndiv(X27, X28, s(X29), X30) :- ','(minus(X27, X28, X31), ','(!, div(X31, X28, X29, X30))).\nand substitution\nT1 -> T16\nX27 -> T16\nT2 -> T17\nX28 -> T17\nX29 -> T20\nT3 -> s(T20)\nT4 -> T21\nX30 -> T21\nT18 -> T20\nT19 -> T21", fontsize=14, style = filled, fillcolor = lightblue];
9 -> 105 [arrowhead = none ];
105 -> 18;

106 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
9 -> 106 [arrowhead = none ];
106 -> 19;

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

108 [label="EVAL with clause\neq(X20, X20).\nand substitution\nT11 -> 0\nX20 -> 0\nT13 -> 0\nT12 -> T14", fontsize=14, style = filled, fillcolor = lightblue];
11 -> 108 [arrowhead = none ];
108 -> 12;

109 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
11 -> 109 [arrowhead = none ];
109 -> 13;

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

111 [label="EVAL with clause\neq(X22, X22).\nand substitution\nT14 -> 0\nX22 -> 0\nT15 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
14 -> 111 [arrowhead = none ];
111 -> 15;

112 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
14 -> 112 [arrowhead = none ];
112 -> 16;

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

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

115 [label="EVAL with clause\ndiv(X150, X151, X152, X150).\nand substitution\nT1 -> T68\nX150 -> T68\nT2 -> T69\nX151 -> T69\nT3 -> T70\nX152 -> T70\nT4 -> T68", fontsize=14, style = filled, fillcolor = lightblue];
19 -> 115 [arrowhead = none ];
115 -> 93;

116 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
19 -> 116 [arrowhead = none ];
116 -> 94;

117 [label="BACKTRACK\nfor clause: minus(X, 0, X)\nwith clash: (div(T16, T17, T3, T4), div(X10, 0, X11, X12))", fontsize=14, style = filled, fillcolor = white];
20 -> 117 [arrowhead = none ];
117 -> 21;

118 [label="EVAL with clause\nminus(s(X37), s(X38), X39) :- minus(X37, X38, X39).\nand substitution\nX37 -> T22\nT16 -> s(T22)\nX38 -> T23\nT17 -> s(T23)\nX31 -> X40\nX39 -> X40", fontsize=14, style = filled, fillcolor = lightblue];
21 -> 118 [arrowhead = none ];
118 -> 22;

119 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
21 -> 119 [arrowhead = none ];
119 -> 23;

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

121 [label="EVAL with clause\ndiv(X144, X145, X146, X144).\nand substitution\nT16 -> T65\nX144 -> T65\nT17 -> T66\nX145 -> T66\nT3 -> T67\nX146 -> T67\nT4 -> T65", fontsize=14, style = filled, fillcolor = lightblue];
23 -> 121 [arrowhead = none ];
121 -> 90;

122 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
23 -> 122 [arrowhead = none ];
122 -> 91;

123 [label="EVAL with clause\nminus(X42, 0, X42).\nand substitution\nT22 -> T24\nX42 -> T24\nT23 -> 0\nX40 -> T24", fontsize=14, style = filled, fillcolor = lightblue];
24 -> 123 [arrowhead = none ];
123 -> 25;

124 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
24 -> 124 [arrowhead = none ];
124 -> 26;

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

126 [label="EVAL with clause\nminus(s(X46), s(X47), X48) :- minus(X46, X47, X48).\nand substitution\nX46 -> T25\nT22 -> s(T25)\nX47 -> T26\nT23 -> s(T26)\nX40 -> X49\nX48 -> X49", fontsize=14, style = filled, fillcolor = lightblue];
26 -> 126 [arrowhead = none ];
126 -> 28;

127 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
26 -> 127 [arrowhead = none ];
127 -> 29;

128 [label="INSTANCE with matching:\nT1 -> T24\nT2 -> s(0)\nT3 -> T20\nT4 -> T21", fontsize=14, style = filled, fillcolor = lightgrey];
27 -> 128 [arrowhead = none , style=dashed];
128 -> 1[style=dashed];

129 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
28 -> 129 [arrowhead = none ];
129 -> 30;

130 [label="EVAL with clause\ndiv(X138, X139, X140, X138).\nand substitution\nT22 -> T62\nX138 -> s(T62)\nT23 -> T63\nX139 -> s(T63)\nT3 -> T64\nX140 -> T64\nT4 -> s(T62)", fontsize=14, style = filled, fillcolor = lightblue];
29 -> 130 [arrowhead = none ];
130 -> 87;

131 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
29 -> 131 [arrowhead = none ];
131 -> 88;

132 [label="EVAL with clause\nminus(X51, 0, X51).\nand substitution\nT25 -> T27\nX51 -> T27\nT26 -> 0\nX49 -> T27", fontsize=14, style = filled, fillcolor = lightblue];
30 -> 132 [arrowhead = none ];
132 -> 31;

133 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
30 -> 133 [arrowhead = none ];
133 -> 32;

134 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
31 -> 134 [arrowhead = none ];
134 -> 33;

135 [label="EVAL with clause\nminus(s(X55), s(X56), X57) :- minus(X55, X56, X57).\nand substitution\nX55 -> T28\nT25 -> s(T28)\nX56 -> T29\nT26 -> s(T29)\nX49 -> X58\nX57 -> X58", fontsize=14, style = filled, fillcolor = lightblue];
32 -> 135 [arrowhead = none ];
135 -> 34;

136 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
32 -> 136 [arrowhead = none ];
136 -> 35;

137 [label="INSTANCE with matching:\nT1 -> T27\nT2 -> s(s(0))\nT3 -> T20\nT4 -> T21", fontsize=14, style = filled, fillcolor = lightgrey];
33 -> 137 [arrowhead = none , style=dashed];
137 -> 1[style=dashed];

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

139 [label="EVAL with clause\ndiv(X132, X133, X134, X132).\nand substitution\nT25 -> T59\nX132 -> s(s(T59))\nT26 -> T60\nX133 -> s(s(T60))\nT3 -> T61\nX134 -> T61\nT4 -> s(s(T59))", fontsize=14, style = filled, fillcolor = lightblue];
35 -> 139 [arrowhead = none ];
139 -> 84;

140 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
35 -> 140 [arrowhead = none ];
140 -> 85;

141 [label="EVAL with clause\nminus(X60, 0, X60).\nand substitution\nT28 -> T30\nX60 -> T30\nT29 -> 0\nX58 -> T30", fontsize=14, style = filled, fillcolor = lightblue];
36 -> 141 [arrowhead = none ];
141 -> 37;

142 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
36 -> 142 [arrowhead = none ];
142 -> 38;

143 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
37 -> 143 [arrowhead = none ];
143 -> 39;

144 [label="EVAL with clause\nminus(s(X64), s(X65), X66) :- minus(X64, X65, X66).\nand substitution\nX64 -> T31\nT28 -> s(T31)\nX65 -> T32\nT29 -> s(T32)\nX58 -> X67\nX66 -> X67", fontsize=14, style = filled, fillcolor = lightblue];
38 -> 144 [arrowhead = none ];
144 -> 40;

145 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
38 -> 145 [arrowhead = none ];
145 -> 41;

146 [label="INSTANCE with matching:\nT1 -> T30\nT2 -> s(s(s(0)))\nT3 -> T20\nT4 -> T21", fontsize=14, style = filled, fillcolor = lightgrey];
39 -> 146 [arrowhead = none , style=dashed];
146 -> 1[style=dashed];

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

148 [label="EVAL with clause\ndiv(X126, X127, X128, X126).\nand substitution\nT28 -> T56\nX126 -> s(s(s(T56)))\nT29 -> T57\nX127 -> s(s(s(T57)))\nT3 -> T58\nX128 -> T58\nT4 -> s(s(s(T56)))", fontsize=14, style = filled, fillcolor = lightblue];
41 -> 148 [arrowhead = none ];
148 -> 81;

149 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
41 -> 149 [arrowhead = none ];
149 -> 82;

150 [label="EVAL with clause\nminus(X69, 0, X69).\nand substitution\nT31 -> T33\nX69 -> T33\nT32 -> 0\nX67 -> T33", fontsize=14, style = filled, fillcolor = lightblue];
42 -> 150 [arrowhead = none ];
150 -> 43;

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

152 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
43 -> 152 [arrowhead = none ];
152 -> 45;

153 [label="EVAL with clause\nminus(s(X73), s(X74), X75) :- minus(X73, X74, X75).\nand substitution\nX73 -> T34\nT31 -> s(T34)\nX74 -> T35\nT32 -> s(T35)\nX67 -> X76\nX75 -> X76", fontsize=14, style = filled, fillcolor = lightblue];
44 -> 153 [arrowhead = none ];
153 -> 46;

154 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
44 -> 154 [arrowhead = none ];
154 -> 47;

155 [label="INSTANCE with matching:\nT1 -> T33\nT2 -> s(s(s(s(0))))\nT3 -> T20\nT4 -> T21", fontsize=14, style = filled, fillcolor = lightgrey];
45 -> 155 [arrowhead = none , style=dashed];
155 -> 1[style=dashed];

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

157 [label="EVAL with clause\ndiv(X120, X121, X122, X120).\nand substitution\nT31 -> T53\nX120 -> s(s(s(s(T53))))\nT32 -> T54\nX121 -> s(s(s(s(T54))))\nT3 -> T55\nX122 -> T55\nT4 -> s(s(s(s(T53))))", fontsize=14, style = filled, fillcolor = lightblue];
47 -> 157 [arrowhead = none ];
157 -> 78;

158 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
47 -> 158 [arrowhead = none ];
158 -> 79;

159 [label="EVAL with clause\nminus(X78, 0, X78).\nand substitution\nT34 -> T36\nX78 -> T36\nT35 -> 0\nX76 -> T36", fontsize=14, style = filled, fillcolor = lightblue];
48 -> 159 [arrowhead = none ];
159 -> 49;

160 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
48 -> 160 [arrowhead = none ];
160 -> 50;

161 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
49 -> 161 [arrowhead = none ];
161 -> 51;

162 [label="EVAL with clause\nminus(s(X82), s(X83), X84) :- minus(X82, X83, X84).\nand substitution\nX82 -> T37\nT34 -> s(T37)\nX83 -> T38\nT35 -> s(T38)\nX76 -> X85\nX84 -> X85", fontsize=14, style = filled, fillcolor = lightblue];
50 -> 162 [arrowhead = none ];
162 -> 52;

163 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
50 -> 163 [arrowhead = none ];
163 -> 53;

164 [label="INSTANCE with matching:\nT1 -> T36\nT2 -> s(s(s(s(s(0)))))\nT3 -> T20\nT4 -> T21", fontsize=14, style = filled, fillcolor = lightgrey];
51 -> 164 [arrowhead = none , style=dashed];
164 -> 1[style=dashed];

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

166 [label="EVAL with clause\ndiv(X114, X115, X116, X114).\nand substitution\nT34 -> T50\nX114 -> s(s(s(s(s(T50)))))\nT35 -> T51\nX115 -> s(s(s(s(s(T51)))))\nT3 -> T52\nX116 -> T52\nT4 -> s(s(s(s(s(T50)))))", fontsize=14, style = filled, fillcolor = lightblue];
53 -> 166 [arrowhead = none ];
166 -> 75;

167 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
53 -> 167 [arrowhead = none ];
167 -> 76;

168 [label="EVAL with clause\nminus(X87, 0, X87).\nand substitution\nT37 -> T39\nX87 -> T39\nT38 -> 0\nX85 -> T39", fontsize=14, style = filled, fillcolor = lightblue];
54 -> 168 [arrowhead = none ];
168 -> 55;

169 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
54 -> 169 [arrowhead = none ];
169 -> 56;

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

171 [label="EVAL with clause\nminus(s(X91), s(X92), X93) :- minus(X91, X92, X93).\nand substitution\nX91 -> T40\nT37 -> s(T40)\nX92 -> T41\nT38 -> s(T41)\nX85 -> X94\nX93 -> X94", fontsize=14, style = filled, fillcolor = lightblue];
56 -> 171 [arrowhead = none ];
171 -> 58;

172 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
56 -> 172 [arrowhead = none ];
172 -> 59;

173 [label="INSTANCE with matching:\nT1 -> T39\nT2 -> s(s(s(s(s(s(0))))))\nT3 -> T20\nT4 -> T21", fontsize=14, style = filled, fillcolor = lightgrey];
57 -> 173 [arrowhead = none , style=dashed];
173 -> 1[style=dashed];

174 [label="GENERALIZATION\nT42 <-- s(s(s(s(s(s(T41))))))\n\nNew Knowledge:\nT42 is ground", fontsize=14, style = filled, fillcolor = violet];
58 -> 174 [arrowhead = none ];
174 -> 60;

175 [label="EVAL with clause\ndiv(X108, X109, X110, X108).\nand substitution\nT37 -> T47\nX108 -> s(s(s(s(s(s(T47))))))\nT38 -> T48\nX109 -> s(s(s(s(s(s(T48))))))\nT3 -> T49\nX110 -> T49\nT4 -> s(s(s(s(s(s(T47))))))", fontsize=14, style = filled, fillcolor = lightblue];
59 -> 175 [arrowhead = none ];
175 -> 72;

176 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
59 -> 176 [arrowhead = none ];
176 -> 73;

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

178 [label="SPLIT 2\nnew knowledge:\nT43 is ground\nreplacements:\nX94 -> T43", fontsize=14, style = filled, fillcolor = violet];
60 -> 178 [arrowhead = none ];
178 -> 62;

179 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
61 -> 179 [arrowhead = none ];
179 -> 63;

180 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
62 -> 180 [arrowhead = none ];
180 -> 71;

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

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

183 [label="EVAL with clause\nminus(X97, 0, X97).\nand substitution\nT40 -> T44\nX97 -> T44\nT41 -> 0\nX94 -> T44", fontsize=14, style = filled, fillcolor = lightblue];
64 -> 183 [arrowhead = none ];
183 -> 66;

184 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
64 -> 184 [arrowhead = none ];
184 -> 67;

185 [label="EVAL with clause\nminus(s(X101), s(X102), X103) :- minus(X101, X102, X103).\nand substitution\nX101 -> T45\nT40 -> s(T45)\nX102 -> T46\nT41 -> s(T46)\nX94 -> X104\nX103 -> X104", fontsize=14, style = filled, fillcolor = lightblue];
65 -> 185 [arrowhead = none ];
185 -> 69;

186 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
65 -> 186 [arrowhead = none ];
186 -> 70;

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

188 [label="INSTANCE with matching:\nT40 -> T45\nT41 -> T46\nX94 -> X104", fontsize=14, style = filled, fillcolor = lightgrey];
69 -> 188 [arrowhead = none , style=dashed];
188 -> 61[style=dashed];

189 [label="INSTANCE with matching:\nT1 -> T43\nT2 -> s(T42)\nT3 -> T20\nT4 -> T21", fontsize=14, style = filled, fillcolor = lightgrey];
71 -> 189 [arrowhead = none , style=dashed];
189 -> 1[style=dashed];

190 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
72 -> 190 [arrowhead = none ];
190 -> 74;

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

192 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
78 -> 192 [arrowhead = none ];
192 -> 80;

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

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

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

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

197 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
93 -> 197 [arrowhead = none ];
197 -> 95;

}

(2) Obligation:

Clauses:

div1(0, T8, 0, 0).
div1(s(T24), s(0), s(T20), T21) :- div1(T24, s(0), T20, T21).
div1(s(s(T27)), s(s(0)), s(T20), T21) :- div1(T27, s(s(0)), T20, T21).
div1(s(s(s(T30))), s(s(s(0))), s(T20), T21) :- div1(T30, s(s(s(0))), T20, T21).
div1(s(s(s(s(T33)))), s(s(s(s(0)))), s(T20), T21) :- div1(T33, s(s(s(s(0)))), T20, T21).
div1(s(s(s(s(s(T36))))), s(s(s(s(s(0))))), s(T20), T21) :- div1(T36, s(s(s(s(s(0))))), T20, T21).
div1(s(s(s(s(s(s(T39)))))), s(s(s(s(s(s(0)))))), s(T20), T21) :- div1(T39, s(s(s(s(s(s(0)))))), T20, T21).
div1(s(s(s(s(s(s(s(T40))))))), s(s(s(s(s(s(s(T41))))))), s(T20), T21) :- minus61(T40, T41, X94).
div1(s(s(s(s(s(s(s(T40))))))), s(s(s(s(s(s(s(T41))))))), s(T20), T21) :- ','(minus61(T40, T41, T43), div1(T43, s(T42), T20, T21)).
div1(s(s(s(s(s(s(T47)))))), s(s(s(s(s(s(T48)))))), T49, s(s(s(s(s(s(T47))))))).
div1(s(s(s(s(s(T50))))), s(s(s(s(s(T51))))), T52, s(s(s(s(s(T50)))))).
div1(s(s(s(s(T53)))), s(s(s(s(T54)))), T55, s(s(s(s(T53))))).
div1(s(s(s(T56))), s(s(s(T57))), T58, s(s(s(T56)))).
div1(s(s(T59)), s(s(T60)), T61, s(s(T59))).
div1(s(T62), s(T63), T64, s(T62)).
div1(T65, T66, T67, T65).
div1(T68, T69, T70, T68).
minus61(T44, 0, T44).
minus61(s(T45), s(T46), X104) :- minus61(T45, T46, X104).

Queries:

div1(g,g,a,a).

(3) PrologToPiTRSProof (SOUND transformation)

We use the technique of [LOPSTR]. With regard to the inferred argument filtering the predicates were used in the following modes:
div1_in: (b,b,f,f) (b,f,f,f)
minus61_in: (b,b,f) (b,f,f)
Transforming Prolog into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:

div1_in_ggaa(0, T8, 0, 0) → div1_out_ggaa(0, T8, 0, 0)
div1_in_ggaa(s(T24), s(0), s(T20), T21) → U1_ggaa(T24, T20, T21, div1_in_ggaa(T24, s(0), T20, T21))
div1_in_ggaa(s(s(T27)), s(s(0)), s(T20), T21) → U2_ggaa(T27, T20, T21, div1_in_ggaa(T27, s(s(0)), T20, T21))
div1_in_ggaa(s(s(s(T30))), s(s(s(0))), s(T20), T21) → U3_ggaa(T30, T20, T21, div1_in_ggaa(T30, s(s(s(0))), T20, T21))
div1_in_ggaa(s(s(s(s(T33)))), s(s(s(s(0)))), s(T20), T21) → U4_ggaa(T33, T20, T21, div1_in_ggaa(T33, s(s(s(s(0)))), T20, T21))
div1_in_ggaa(s(s(s(s(s(T36))))), s(s(s(s(s(0))))), s(T20), T21) → U5_ggaa(T36, T20, T21, div1_in_ggaa(T36, s(s(s(s(s(0))))), T20, T21))
div1_in_ggaa(s(s(s(s(s(s(T39)))))), s(s(s(s(s(s(0)))))), s(T20), T21) → U6_ggaa(T39, T20, T21, div1_in_ggaa(T39, s(s(s(s(s(s(0)))))), T20, T21))
div1_in_ggaa(s(s(s(s(s(s(s(T40))))))), s(s(s(s(s(s(s(T41))))))), s(T20), T21) → U7_ggaa(T40, T41, T20, T21, minus61_in_gga(T40, T41, X94))
minus61_in_gga(T44, 0, T44) → minus61_out_gga(T44, 0, T44)
minus61_in_gga(s(T45), s(T46), X104) → U10_gga(T45, T46, X104, minus61_in_gga(T45, T46, X104))
U10_gga(T45, T46, X104, minus61_out_gga(T45, T46, X104)) → minus61_out_gga(s(T45), s(T46), X104)
U7_ggaa(T40, T41, T20, T21, minus61_out_gga(T40, T41, X94)) → div1_out_ggaa(s(s(s(s(s(s(s(T40))))))), s(s(s(s(s(s(s(T41))))))), s(T20), T21)
div1_in_ggaa(s(s(s(s(s(s(s(T40))))))), s(s(s(s(s(s(s(T41))))))), s(T20), T21) → U8_ggaa(T40, T41, T20, T21, minus61_in_gga(T40, T41, T43))
U8_ggaa(T40, T41, T20, T21, minus61_out_gga(T40, T41, T43)) → U9_ggaa(T40, T41, T20, T21, div1_in_gaaa(T43, s(T42), T20, T21))
div1_in_gaaa(0, T8, 0, 0) → div1_out_gaaa(0, T8, 0, 0)
div1_in_gaaa(s(T24), s(0), s(T20), T21) → U1_gaaa(T24, T20, T21, div1_in_ggaa(T24, s(0), T20, T21))
div1_in_ggaa(s(s(s(s(s(s(T47)))))), s(s(s(s(s(s(T48)))))), T49, s(s(s(s(s(s(T47))))))) → div1_out_ggaa(s(s(s(s(s(s(T47)))))), s(s(s(s(s(s(T48)))))), T49, s(s(s(s(s(s(T47)))))))
div1_in_ggaa(s(s(s(s(s(T50))))), s(s(s(s(s(T51))))), T52, s(s(s(s(s(T50)))))) → div1_out_ggaa(s(s(s(s(s(T50))))), s(s(s(s(s(T51))))), T52, s(s(s(s(s(T50))))))
div1_in_ggaa(s(s(s(s(T53)))), s(s(s(s(T54)))), T55, s(s(s(s(T53))))) → div1_out_ggaa(s(s(s(s(T53)))), s(s(s(s(T54)))), T55, s(s(s(s(T53)))))
div1_in_ggaa(s(s(s(T56))), s(s(s(T57))), T58, s(s(s(T56)))) → div1_out_ggaa(s(s(s(T56))), s(s(s(T57))), T58, s(s(s(T56))))
div1_in_ggaa(s(s(T59)), s(s(T60)), T61, s(s(T59))) → div1_out_ggaa(s(s(T59)), s(s(T60)), T61, s(s(T59)))
div1_in_ggaa(s(T62), s(T63), T64, s(T62)) → div1_out_ggaa(s(T62), s(T63), T64, s(T62))
div1_in_ggaa(T65, T66, T67, T65) → div1_out_ggaa(T65, T66, T67, T65)
U1_gaaa(T24, T20, T21, div1_out_ggaa(T24, s(0), T20, T21)) → div1_out_gaaa(s(T24), s(0), s(T20), T21)
div1_in_gaaa(s(s(T27)), s(s(0)), s(T20), T21) → U2_gaaa(T27, T20, T21, div1_in_ggaa(T27, s(s(0)), T20, T21))
U2_gaaa(T27, T20, T21, div1_out_ggaa(T27, s(s(0)), T20, T21)) → div1_out_gaaa(s(s(T27)), s(s(0)), s(T20), T21)
div1_in_gaaa(s(s(s(T30))), s(s(s(0))), s(T20), T21) → U3_gaaa(T30, T20, T21, div1_in_ggaa(T30, s(s(s(0))), T20, T21))
U3_gaaa(T30, T20, T21, div1_out_ggaa(T30, s(s(s(0))), T20, T21)) → div1_out_gaaa(s(s(s(T30))), s(s(s(0))), s(T20), T21)
div1_in_gaaa(s(s(s(s(T33)))), s(s(s(s(0)))), s(T20), T21) → U4_gaaa(T33, T20, T21, div1_in_ggaa(T33, s(s(s(s(0)))), T20, T21))
U4_gaaa(T33, T20, T21, div1_out_ggaa(T33, s(s(s(s(0)))), T20, T21)) → div1_out_gaaa(s(s(s(s(T33)))), s(s(s(s(0)))), s(T20), T21)
div1_in_gaaa(s(s(s(s(s(T36))))), s(s(s(s(s(0))))), s(T20), T21) → U5_gaaa(T36, T20, T21, div1_in_ggaa(T36, s(s(s(s(s(0))))), T20, T21))
U5_gaaa(T36, T20, T21, div1_out_ggaa(T36, s(s(s(s(s(0))))), T20, T21)) → div1_out_gaaa(s(s(s(s(s(T36))))), s(s(s(s(s(0))))), s(T20), T21)
div1_in_gaaa(s(s(s(s(s(s(T39)))))), s(s(s(s(s(s(0)))))), s(T20), T21) → U6_gaaa(T39, T20, T21, div1_in_ggaa(T39, s(s(s(s(s(s(0)))))), T20, T21))
U6_gaaa(T39, T20, T21, div1_out_ggaa(T39, s(s(s(s(s(s(0)))))), T20, T21)) → div1_out_gaaa(s(s(s(s(s(s(T39)))))), s(s(s(s(s(s(0)))))), s(T20), T21)
div1_in_gaaa(s(s(s(s(s(s(s(T40))))))), s(s(s(s(s(s(s(T41))))))), s(T20), T21) → U7_gaaa(T40, T41, T20, T21, minus61_in_gaa(T40, T41, X94))
minus61_in_gaa(T44, 0, T44) → minus61_out_gaa(T44, 0, T44)
minus61_in_gaa(s(T45), s(T46), X104) → U10_gaa(T45, T46, X104, minus61_in_gaa(T45, T46, X104))
U10_gaa(T45, T46, X104, minus61_out_gaa(T45, T46, X104)) → minus61_out_gaa(s(T45), s(T46), X104)
U7_gaaa(T40, T41, T20, T21, minus61_out_gaa(T40, T41, X94)) → div1_out_gaaa(s(s(s(s(s(s(s(T40))))))), s(s(s(s(s(s(s(T41))))))), s(T20), T21)
div1_in_gaaa(s(s(s(s(s(s(s(T40))))))), s(s(s(s(s(s(s(T41))))))), s(T20), T21) → U8_gaaa(T40, T41, T20, T21, minus61_in_gaa(T40, T41, T43))
U8_gaaa(T40, T41, T20, T21, minus61_out_gaa(T40, T41, T43)) → U9_gaaa(T40, T41, T20, T21, div1_in_gaaa(T43, s(T42), T20, T21))
div1_in_gaaa(s(s(s(s(s(s(T47)))))), s(s(s(s(s(s(T48)))))), T49, s(s(s(s(s(s(T47))))))) → div1_out_gaaa(s(s(s(s(s(s(T47)))))), s(s(s(s(s(s(T48)))))), T49, s(s(s(s(s(s(T47)))))))
div1_in_gaaa(s(s(s(s(s(T50))))), s(s(s(s(s(T51))))), T52, s(s(s(s(s(T50)))))) → div1_out_gaaa(s(s(s(s(s(T50))))), s(s(s(s(s(T51))))), T52, s(s(s(s(s(T50))))))
div1_in_gaaa(s(s(s(s(T53)))), s(s(s(s(T54)))), T55, s(s(s(s(T53))))) → div1_out_gaaa(s(s(s(s(T53)))), s(s(s(s(T54)))), T55, s(s(s(s(T53)))))
div1_in_gaaa(s(s(s(T56))), s(s(s(T57))), T58, s(s(s(T56)))) → div1_out_gaaa(s(s(s(T56))), s(s(s(T57))), T58, s(s(s(T56))))
div1_in_gaaa(s(s(T59)), s(s(T60)), T61, s(s(T59))) → div1_out_gaaa(s(s(T59)), s(s(T60)), T61, s(s(T59)))
div1_in_gaaa(s(T62), s(T63), T64, s(T62)) → div1_out_gaaa(s(T62), s(T63), T64, s(T62))
div1_in_gaaa(T65, T66, T67, T65) → div1_out_gaaa(T65, T66, T67, T65)
U9_gaaa(T40, T41, T20, T21, div1_out_gaaa(T43, s(T42), T20, T21)) → div1_out_gaaa(s(s(s(s(s(s(s(T40))))))), s(s(s(s(s(s(s(T41))))))), s(T20), T21)
U9_ggaa(T40, T41, T20, T21, div1_out_gaaa(T43, s(T42), T20, T21)) → div1_out_ggaa(s(s(s(s(s(s(s(T40))))))), s(s(s(s(s(s(s(T41))))))), s(T20), T21)
U6_ggaa(T39, T20, T21, div1_out_ggaa(T39, s(s(s(s(s(s(0)))))), T20, T21)) → div1_out_ggaa(s(s(s(s(s(s(T39)))))), s(s(s(s(s(s(0)))))), s(T20), T21)
U5_ggaa(T36, T20, T21, div1_out_ggaa(T36, s(s(s(s(s(0))))), T20, T21)) → div1_out_ggaa(s(s(s(s(s(T36))))), s(s(s(s(s(0))))), s(T20), T21)
U4_ggaa(T33, T20, T21, div1_out_ggaa(T33, s(s(s(s(0)))), T20, T21)) → div1_out_ggaa(s(s(s(s(T33)))), s(s(s(s(0)))), s(T20), T21)
U3_ggaa(T30, T20, T21, div1_out_ggaa(T30, s(s(s(0))), T20, T21)) → div1_out_ggaa(s(s(s(T30))), s(s(s(0))), s(T20), T21)
U2_ggaa(T27, T20, T21, div1_out_ggaa(T27, s(s(0)), T20, T21)) → div1_out_ggaa(s(s(T27)), s(s(0)), s(T20), T21)
U1_ggaa(T24, T20, T21, div1_out_ggaa(T24, s(0), T20, T21)) → div1_out_ggaa(s(T24), s(0), s(T20), T21)

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog

(4) Obligation:

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

div1_in_ggaa(0, T8, 0, 0) → div1_out_ggaa(0, T8, 0, 0)
div1_in_ggaa(s(T24), s(0), s(T20), T21) → U1_ggaa(T24, T20, T21, div1_in_ggaa(T24, s(0), T20, T21))
div1_in_ggaa(s(s(T27)), s(s(0)), s(T20), T21) → U2_ggaa(T27, T20, T21, div1_in_ggaa(T27, s(s(0)), T20, T21))
div1_in_ggaa(s(s(s(T30))), s(s(s(0))), s(T20), T21) → U3_ggaa(T30, T20, T21, div1_in_ggaa(T30, s(s(s(0))), T20, T21))
div1_in_ggaa(s(s(s(s(T33)))), s(s(s(s(0)))), s(T20), T21) → U4_ggaa(T33, T20, T21, div1_in_ggaa(T33, s(s(s(s(0)))), T20, T21))
div1_in_ggaa(s(s(s(s(s(T36))))), s(s(s(s(s(0))))), s(T20), T21) → U5_ggaa(T36, T20, T21, div1_in_ggaa(T36, s(s(s(s(s(0))))), T20, T21))
div1_in_ggaa(s(s(s(s(s(s(T39)))))), s(s(s(s(s(s(0)))))), s(T20), T21) → U6_ggaa(T39, T20, T21, div1_in_ggaa(T39, s(s(s(s(s(s(0)))))), T20, T21))
div1_in_ggaa(s(s(s(s(s(s(s(T40))))))), s(s(s(s(s(s(s(T41))))))), s(T20), T21) → U7_ggaa(T40, T41, T20, T21, minus61_in_gga(T40, T41, X94))
minus61_in_gga(T44, 0, T44) → minus61_out_gga(T44, 0, T44)
minus61_in_gga(s(T45), s(T46), X104) → U10_gga(T45, T46, X104, minus61_in_gga(T45, T46, X104))
U10_gga(T45, T46, X104, minus61_out_gga(T45, T46, X104)) → minus61_out_gga(s(T45), s(T46), X104)
U7_ggaa(T40, T41, T20, T21, minus61_out_gga(T40, T41, X94)) → div1_out_ggaa(s(s(s(s(s(s(s(T40))))))), s(s(s(s(s(s(s(T41))))))), s(T20), T21)
div1_in_ggaa(s(s(s(s(s(s(s(T40))))))), s(s(s(s(s(s(s(T41))))))), s(T20), T21) → U8_ggaa(T40, T41, T20, T21, minus61_in_gga(T40, T41, T43))
U8_ggaa(T40, T41, T20, T21, minus61_out_gga(T40, T41, T43)) → U9_ggaa(T40, T41, T20, T21, div1_in_gaaa(T43, s(T42), T20, T21))
div1_in_gaaa(0, T8, 0, 0) → div1_out_gaaa(0, T8, 0, 0)
div1_in_gaaa(s(T24), s(0), s(T20), T21) → U1_gaaa(T24, T20, T21, div1_in_ggaa(T24, s(0), T20, T21))
div1_in_ggaa(s(s(s(s(s(s(T47)))))), s(s(s(s(s(s(T48)))))), T49, s(s(s(s(s(s(T47))))))) → div1_out_ggaa(s(s(s(s(s(s(T47)))))), s(s(s(s(s(s(T48)))))), T49, s(s(s(s(s(s(T47)))))))
div1_in_ggaa(s(s(s(s(s(T50))))), s(s(s(s(s(T51))))), T52, s(s(s(s(s(T50)))))) → div1_out_ggaa(s(s(s(s(s(T50))))), s(s(s(s(s(T51))))), T52, s(s(s(s(s(T50))))))
div1_in_ggaa(s(s(s(s(T53)))), s(s(s(s(T54)))), T55, s(s(s(s(T53))))) → div1_out_ggaa(s(s(s(s(T53)))), s(s(s(s(T54)))), T55, s(s(s(s(T53)))))
div1_in_ggaa(s(s(s(T56))), s(s(s(T57))), T58, s(s(s(T56)))) → div1_out_ggaa(s(s(s(T56))), s(s(s(T57))), T58, s(s(s(T56))))
div1_in_ggaa(s(s(T59)), s(s(T60)), T61, s(s(T59))) → div1_out_ggaa(s(s(T59)), s(s(T60)), T61, s(s(T59)))
div1_in_ggaa(s(T62), s(T63), T64, s(T62)) → div1_out_ggaa(s(T62), s(T63), T64, s(T62))
div1_in_ggaa(T65, T66, T67, T65) → div1_out_ggaa(T65, T66, T67, T65)
U1_gaaa(T24, T20, T21, div1_out_ggaa(T24, s(0), T20, T21)) → div1_out_gaaa(s(T24), s(0), s(T20), T21)
div1_in_gaaa(s(s(T27)), s(s(0)), s(T20), T21) → U2_gaaa(T27, T20, T21, div1_in_ggaa(T27, s(s(0)), T20, T21))
U2_gaaa(T27, T20, T21, div1_out_ggaa(T27, s(s(0)), T20, T21)) → div1_out_gaaa(s(s(T27)), s(s(0)), s(T20), T21)
div1_in_gaaa(s(s(s(T30))), s(s(s(0))), s(T20), T21) → U3_gaaa(T30, T20, T21, div1_in_ggaa(T30, s(s(s(0))), T20, T21))
U3_gaaa(T30, T20, T21, div1_out_ggaa(T30, s(s(s(0))), T20, T21)) → div1_out_gaaa(s(s(s(T30))), s(s(s(0))), s(T20), T21)
div1_in_gaaa(s(s(s(s(T33)))), s(s(s(s(0)))), s(T20), T21) → U4_gaaa(T33, T20, T21, div1_in_ggaa(T33, s(s(s(s(0)))), T20, T21))
U4_gaaa(T33, T20, T21, div1_out_ggaa(T33, s(s(s(s(0)))), T20, T21)) → div1_out_gaaa(s(s(s(s(T33)))), s(s(s(s(0)))), s(T20), T21)
div1_in_gaaa(s(s(s(s(s(T36))))), s(s(s(s(s(0))))), s(T20), T21) → U5_gaaa(T36, T20, T21, div1_in_ggaa(T36, s(s(s(s(s(0))))), T20, T21))
U5_gaaa(T36, T20, T21, div1_out_ggaa(T36, s(s(s(s(s(0))))), T20, T21)) → div1_out_gaaa(s(s(s(s(s(T36))))), s(s(s(s(s(0))))), s(T20), T21)
div1_in_gaaa(s(s(s(s(s(s(T39)))))), s(s(s(s(s(s(0)))))), s(T20), T21) → U6_gaaa(T39, T20, T21, div1_in_ggaa(T39, s(s(s(s(s(s(0)))))), T20, T21))
U6_gaaa(T39, T20, T21, div1_out_ggaa(T39, s(s(s(s(s(s(0)))))), T20, T21)) → div1_out_gaaa(s(s(s(s(s(s(T39)))))), s(s(s(s(s(s(0)))))), s(T20), T21)
div1_in_gaaa(s(s(s(s(s(s(s(T40))))))), s(s(s(s(s(s(s(T41))))))), s(T20), T21) → U7_gaaa(T40, T41, T20, T21, minus61_in_gaa(T40, T41, X94))
minus61_in_gaa(T44, 0, T44) → minus61_out_gaa(T44, 0, T44)
minus61_in_gaa(s(T45), s(T46), X104) → U10_gaa(T45, T46, X104, minus61_in_gaa(T45, T46, X104))
U10_gaa(T45, T46, X104, minus61_out_gaa(T45, T46, X104)) → minus61_out_gaa(s(T45), s(T46), X104)
U7_gaaa(T40, T41, T20, T21, minus61_out_gaa(T40, T41, X94)) → div1_out_gaaa(s(s(s(s(s(s(s(T40))))))), s(s(s(s(s(s(s(T41))))))), s(T20), T21)
div1_in_gaaa(s(s(s(s(s(s(s(T40))))))), s(s(s(s(s(s(s(T41))))))), s(T20), T21) → U8_gaaa(T40, T41, T20, T21, minus61_in_gaa(T40, T41, T43))
U8_gaaa(T40, T41, T20, T21, minus61_out_gaa(T40, T41, T43)) → U9_gaaa(T40, T41, T20, T21, div1_in_gaaa(T43, s(T42), T20, T21))
div1_in_gaaa(s(s(s(s(s(s(T47)))))), s(s(s(s(s(s(T48)))))), T49, s(s(s(s(s(s(T47))))))) → div1_out_gaaa(s(s(s(s(s(s(T47)))))), s(s(s(s(s(s(T48)))))), T49, s(s(s(s(s(s(T47)))))))
div1_in_gaaa(s(s(s(s(s(T50))))), s(s(s(s(s(T51))))), T52, s(s(s(s(s(T50)))))) → div1_out_gaaa(s(s(s(s(s(T50))))), s(s(s(s(s(T51))))), T52, s(s(s(s(s(T50))))))
div1_in_gaaa(s(s(s(s(T53)))), s(s(s(s(T54)))), T55, s(s(s(s(T53))))) → div1_out_gaaa(s(s(s(s(T53)))), s(s(s(s(T54)))), T55, s(s(s(s(T53)))))
div1_in_gaaa(s(s(s(T56))), s(s(s(T57))), T58, s(s(s(T56)))) → div1_out_gaaa(s(s(s(T56))), s(s(s(T57))), T58, s(s(s(T56))))
div1_in_gaaa(s(s(T59)), s(s(T60)), T61, s(s(T59))) → div1_out_gaaa(s(s(T59)), s(s(T60)), T61, s(s(T59)))
div1_in_gaaa(s(T62), s(T63), T64, s(T62)) → div1_out_gaaa(s(T62), s(T63), T64, s(T62))
div1_in_gaaa(T65, T66, T67, T65) → div1_out_gaaa(T65, T66, T67, T65)
U9_gaaa(T40, T41, T20, T21, div1_out_gaaa(T43, s(T42), T20, T21)) → div1_out_gaaa(s(s(s(s(s(s(s(T40))))))), s(s(s(s(s(s(s(T41))))))), s(T20), T21)
U9_ggaa(T40, T41, T20, T21, div1_out_gaaa(T43, s(T42), T20, T21)) → div1_out_ggaa(s(s(s(s(s(s(s(T40))))))), s(s(s(s(s(s(s(T41))))))), s(T20), T21)
U6_ggaa(T39, T20, T21, div1_out_ggaa(T39, s(s(s(s(s(s(0)))))), T20, T21)) → div1_out_ggaa(s(s(s(s(s(s(T39)))))), s(s(s(s(s(s(0)))))), s(T20), T21)
U5_ggaa(T36, T20, T21, div1_out_ggaa(T36, s(s(s(s(s(0))))), T20, T21)) → div1_out_ggaa(s(s(s(s(s(T36))))), s(s(s(s(s(0))))), s(T20), T21)
U4_ggaa(T33, T20, T21, div1_out_ggaa(T33, s(s(s(s(0)))), T20, T21)) → div1_out_ggaa(s(s(s(s(T33)))), s(s(s(s(0)))), s(T20), T21)
U3_ggaa(T30, T20, T21, div1_out_ggaa(T30, s(s(s(0))), T20, T21)) → div1_out_ggaa(s(s(s(T30))), s(s(s(0))), s(T20), T21)
U2_ggaa(T27, T20, T21, div1_out_ggaa(T27, s(s(0)), T20, T21)) → div1_out_ggaa(s(s(T27)), s(s(0)), s(T20), T21)
U1_ggaa(T24, T20, T21, div1_out_ggaa(T24, s(0), T20, T21)) → div1_out_ggaa(s(T24), s(0), s(T20), T21)

(5) DependencyPairsProof (EQUIVALENT transformation)

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

DIV1_IN_GGAA(s(T24), s(0), s(T20), T21) → U1_GGAA(T24, T20, T21, div1_in_ggaa(T24, s(0), T20, T21))
DIV1_IN_GGAA(s(T24), s(0), s(T20), T21) → DIV1_IN_GGAA(T24, s(0), T20, T21)
DIV1_IN_GGAA(s(s(T27)), s(s(0)), s(T20), T21) → U2_GGAA(T27, T20, T21, div1_in_ggaa(T27, s(s(0)), T20, T21))
DIV1_IN_GGAA(s(s(T27)), s(s(0)), s(T20), T21) → DIV1_IN_GGAA(T27, s(s(0)), T20, T21)
DIV1_IN_GGAA(s(s(s(T30))), s(s(s(0))), s(T20), T21) → U3_GGAA(T30, T20, T21, div1_in_ggaa(T30, s(s(s(0))), T20, T21))
DIV1_IN_GGAA(s(s(s(T30))), s(s(s(0))), s(T20), T21) → DIV1_IN_GGAA(T30, s(s(s(0))), T20, T21)
DIV1_IN_GGAA(s(s(s(s(T33)))), s(s(s(s(0)))), s(T20), T21) → U4_GGAA(T33, T20, T21, div1_in_ggaa(T33, s(s(s(s(0)))), T20, T21))
DIV1_IN_GGAA(s(s(s(s(T33)))), s(s(s(s(0)))), s(T20), T21) → DIV1_IN_GGAA(T33, s(s(s(s(0)))), T20, T21)
DIV1_IN_GGAA(s(s(s(s(s(T36))))), s(s(s(s(s(0))))), s(T20), T21) → U5_GGAA(T36, T20, T21, div1_in_ggaa(T36, s(s(s(s(s(0))))), T20, T21))
DIV1_IN_GGAA(s(s(s(s(s(T36))))), s(s(s(s(s(0))))), s(T20), T21) → DIV1_IN_GGAA(T36, s(s(s(s(s(0))))), T20, T21)
DIV1_IN_GGAA(s(s(s(s(s(s(T39)))))), s(s(s(s(s(s(0)))))), s(T20), T21) → U6_GGAA(T39, T20, T21, div1_in_ggaa(T39, s(s(s(s(s(s(0)))))), T20, T21))
DIV1_IN_GGAA(s(s(s(s(s(s(T39)))))), s(s(s(s(s(s(0)))))), s(T20), T21) → DIV1_IN_GGAA(T39, s(s(s(s(s(s(0)))))), T20, T21)
DIV1_IN_GGAA(s(s(s(s(s(s(s(T40))))))), s(s(s(s(s(s(s(T41))))))), s(T20), T21) → U7_GGAA(T40, T41, T20, T21, minus61_in_gga(T40, T41, X94))
DIV1_IN_GGAA(s(s(s(s(s(s(s(T40))))))), s(s(s(s(s(s(s(T41))))))), s(T20), T21) → MINUS61_IN_GGA(T40, T41, X94)
MINUS61_IN_GGA(s(T45), s(T46), X104) → U10_GGA(T45, T46, X104, minus61_in_gga(T45, T46, X104))
MINUS61_IN_GGA(s(T45), s(T46), X104) → MINUS61_IN_GGA(T45, T46, X104)
DIV1_IN_GGAA(s(s(s(s(s(s(s(T40))))))), s(s(s(s(s(s(s(T41))))))), s(T20), T21) → U8_GGAA(T40, T41, T20, T21, minus61_in_gga(T40, T41, T43))
U8_GGAA(T40, T41, T20, T21, minus61_out_gga(T40, T41, T43)) → U9_GGAA(T40, T41, T20, T21, div1_in_gaaa(T43, s(T42), T20, T21))
U8_GGAA(T40, T41, T20, T21, minus61_out_gga(T40, T41, T43)) → DIV1_IN_GAAA(T43, s(T42), T20, T21)
DIV1_IN_GAAA(s(T24), s(0), s(T20), T21) → U1_GAAA(T24, T20, T21, div1_in_ggaa(T24, s(0), T20, T21))
DIV1_IN_GAAA(s(T24), s(0), s(T20), T21) → DIV1_IN_GGAA(T24, s(0), T20, T21)
DIV1_IN_GAAA(s(s(T27)), s(s(0)), s(T20), T21) → U2_GAAA(T27, T20, T21, div1_in_ggaa(T27, s(s(0)), T20, T21))
DIV1_IN_GAAA(s(s(T27)), s(s(0)), s(T20), T21) → DIV1_IN_GGAA(T27, s(s(0)), T20, T21)
DIV1_IN_GAAA(s(s(s(T30))), s(s(s(0))), s(T20), T21) → U3_GAAA(T30, T20, T21, div1_in_ggaa(T30, s(s(s(0))), T20, T21))
DIV1_IN_GAAA(s(s(s(T30))), s(s(s(0))), s(T20), T21) → DIV1_IN_GGAA(T30, s(s(s(0))), T20, T21)
DIV1_IN_GAAA(s(s(s(s(T33)))), s(s(s(s(0)))), s(T20), T21) → U4_GAAA(T33, T20, T21, div1_in_ggaa(T33, s(s(s(s(0)))), T20, T21))
DIV1_IN_GAAA(s(s(s(s(T33)))), s(s(s(s(0)))), s(T20), T21) → DIV1_IN_GGAA(T33, s(s(s(s(0)))), T20, T21)
DIV1_IN_GAAA(s(s(s(s(s(T36))))), s(s(s(s(s(0))))), s(T20), T21) → U5_GAAA(T36, T20, T21, div1_in_ggaa(T36, s(s(s(s(s(0))))), T20, T21))
DIV1_IN_GAAA(s(s(s(s(s(T36))))), s(s(s(s(s(0))))), s(T20), T21) → DIV1_IN_GGAA(T36, s(s(s(s(s(0))))), T20, T21)
DIV1_IN_GAAA(s(s(s(s(s(s(T39)))))), s(s(s(s(s(s(0)))))), s(T20), T21) → U6_GAAA(T39, T20, T21, div1_in_ggaa(T39, s(s(s(s(s(s(0)))))), T20, T21))
DIV1_IN_GAAA(s(s(s(s(s(s(T39)))))), s(s(s(s(s(s(0)))))), s(T20), T21) → DIV1_IN_GGAA(T39, s(s(s(s(s(s(0)))))), T20, T21)
DIV1_IN_GAAA(s(s(s(s(s(s(s(T40))))))), s(s(s(s(s(s(s(T41))))))), s(T20), T21) → U7_GAAA(T40, T41, T20, T21, minus61_in_gaa(T40, T41, X94))
DIV1_IN_GAAA(s(s(s(s(s(s(s(T40))))))), s(s(s(s(s(s(s(T41))))))), s(T20), T21) → MINUS61_IN_GAA(T40, T41, X94)
MINUS61_IN_GAA(s(T45), s(T46), X104) → U10_GAA(T45, T46, X104, minus61_in_gaa(T45, T46, X104))
MINUS61_IN_GAA(s(T45), s(T46), X104) → MINUS61_IN_GAA(T45, T46, X104)
DIV1_IN_GAAA(s(s(s(s(s(s(s(T40))))))), s(s(s(s(s(s(s(T41))))))), s(T20), T21) → U8_GAAA(T40, T41, T20, T21, minus61_in_gaa(T40, T41, T43))
U8_GAAA(T40, T41, T20, T21, minus61_out_gaa(T40, T41, T43)) → U9_GAAA(T40, T41, T20, T21, div1_in_gaaa(T43, s(T42), T20, T21))
U8_GAAA(T40, T41, T20, T21, minus61_out_gaa(T40, T41, T43)) → DIV1_IN_GAAA(T43, s(T42), T20, T21)

The TRS R consists of the following rules:

div1_in_ggaa(0, T8, 0, 0) → div1_out_ggaa(0, T8, 0, 0)
div1_in_ggaa(s(T24), s(0), s(T20), T21) → U1_ggaa(T24, T20, T21, div1_in_ggaa(T24, s(0), T20, T21))
div1_in_ggaa(s(s(T27)), s(s(0)), s(T20), T21) → U2_ggaa(T27, T20, T21, div1_in_ggaa(T27, s(s(0)), T20, T21))
div1_in_ggaa(s(s(s(T30))), s(s(s(0))), s(T20), T21) → U3_ggaa(T30, T20, T21, div1_in_ggaa(T30, s(s(s(0))), T20, T21))
div1_in_ggaa(s(s(s(s(T33)))), s(s(s(s(0)))), s(T20), T21) → U4_ggaa(T33, T20, T21, div1_in_ggaa(T33, s(s(s(s(0)))), T20, T21))
div1_in_ggaa(s(s(s(s(s(T36))))), s(s(s(s(s(0))))), s(T20), T21) → U5_ggaa(T36, T20, T21, div1_in_ggaa(T36, s(s(s(s(s(0))))), T20, T21))
div1_in_ggaa(s(s(s(s(s(s(T39)))))), s(s(s(s(s(s(0)))))), s(T20), T21) → U6_ggaa(T39, T20, T21, div1_in_ggaa(T39, s(s(s(s(s(s(0)))))), T20, T21))
div1_in_ggaa(s(s(s(s(s(s(s(T40))))))), s(s(s(s(s(s(s(T41))))))), s(T20), T21) → U7_ggaa(T40, T41, T20, T21, minus61_in_gga(T40, T41, X94))
minus61_in_gga(T44, 0, T44) → minus61_out_gga(T44, 0, T44)
minus61_in_gga(s(T45), s(T46), X104) → U10_gga(T45, T46, X104, minus61_in_gga(T45, T46, X104))
U10_gga(T45, T46, X104, minus61_out_gga(T45, T46, X104)) → minus61_out_gga(s(T45), s(T46), X104)
U7_ggaa(T40, T41, T20, T21, minus61_out_gga(T40, T41, X94)) → div1_out_ggaa(s(s(s(s(s(s(s(T40))))))), s(s(s(s(s(s(s(T41))))))), s(T20), T21)
div1_in_ggaa(s(s(s(s(s(s(s(T40))))))), s(s(s(s(s(s(s(T41))))))), s(T20), T21) → U8_ggaa(T40, T41, T20, T21, minus61_in_gga(T40, T41, T43))
U8_ggaa(T40, T41, T20, T21, minus61_out_gga(T40, T41, T43)) → U9_ggaa(T40, T41, T20, T21, div1_in_gaaa(T43, s(T42), T20, T21))
div1_in_gaaa(0, T8, 0, 0) → div1_out_gaaa(0, T8, 0, 0)
div1_in_gaaa(s(T24), s(0), s(T20), T21) → U1_gaaa(T24, T20, T21, div1_in_ggaa(T24, s(0), T20, T21))
div1_in_ggaa(s(s(s(s(s(s(T47)))))), s(s(s(s(s(s(T48)))))), T49, s(s(s(s(s(s(T47))))))) → div1_out_ggaa(s(s(s(s(s(s(T47)))))), s(s(s(s(s(s(T48)))))), T49, s(s(s(s(s(s(T47)))))))
div1_in_ggaa(s(s(s(s(s(T50))))), s(s(s(s(s(T51))))), T52, s(s(s(s(s(T50)))))) → div1_out_ggaa(s(s(s(s(s(T50))))), s(s(s(s(s(T51))))), T52, s(s(s(s(s(T50))))))
div1_in_ggaa(s(s(s(s(T53)))), s(s(s(s(T54)))), T55, s(s(s(s(T53))))) → div1_out_ggaa(s(s(s(s(T53)))), s(s(s(s(T54)))), T55, s(s(s(s(T53)))))
div1_in_ggaa(s(s(s(T56))), s(s(s(T57))), T58, s(s(s(T56)))) → div1_out_ggaa(s(s(s(T56))), s(s(s(T57))), T58, s(s(s(T56))))
div1_in_ggaa(s(s(T59)), s(s(T60)), T61, s(s(T59))) → div1_out_ggaa(s(s(T59)), s(s(T60)), T61, s(s(T59)))
div1_in_ggaa(s(T62), s(T63), T64, s(T62)) → div1_out_ggaa(s(T62), s(T63), T64, s(T62))
div1_in_ggaa(T65, T66, T67, T65) → div1_out_ggaa(T65, T66, T67, T65)
U1_gaaa(T24, T20, T21, div1_out_ggaa(T24, s(0), T20, T21)) → div1_out_gaaa(s(T24), s(0), s(T20), T21)
div1_in_gaaa(s(s(T27)), s(s(0)), s(T20), T21) → U2_gaaa(T27, T20, T21, div1_in_ggaa(T27, s(s(0)), T20, T21))
U2_gaaa(T27, T20, T21, div1_out_ggaa(T27, s(s(0)), T20, T21)) → div1_out_gaaa(s(s(T27)), s(s(0)), s(T20), T21)
div1_in_gaaa(s(s(s(T30))), s(s(s(0))), s(T20), T21) → U3_gaaa(T30, T20, T21, div1_in_ggaa(T30, s(s(s(0))), T20, T21))
U3_gaaa(T30, T20, T21, div1_out_ggaa(T30, s(s(s(0))), T20, T21)) → div1_out_gaaa(s(s(s(T30))), s(s(s(0))), s(T20), T21)
div1_in_gaaa(s(s(s(s(T33)))), s(s(s(s(0)))), s(T20), T21) → U4_gaaa(T33, T20, T21, div1_in_ggaa(T33, s(s(s(s(0)))), T20, T21))
U4_gaaa(T33, T20, T21, div1_out_ggaa(T33, s(s(s(s(0)))), T20, T21)) → div1_out_gaaa(s(s(s(s(T33)))), s(s(s(s(0)))), s(T20), T21)
div1_in_gaaa(s(s(s(s(s(T36))))), s(s(s(s(s(0))))), s(T20), T21) → U5_gaaa(T36, T20, T21, div1_in_ggaa(T36, s(s(s(s(s(0))))), T20, T21))
U5_gaaa(T36, T20, T21, div1_out_ggaa(T36, s(s(s(s(s(0))))), T20, T21)) → div1_out_gaaa(s(s(s(s(s(T36))))), s(s(s(s(s(0))))), s(T20), T21)
div1_in_gaaa(s(s(s(s(s(s(T39)))))), s(s(s(s(s(s(0)))))), s(T20), T21) → U6_gaaa(T39, T20, T21, div1_in_ggaa(T39, s(s(s(s(s(s(0)))))), T20, T21))
U6_gaaa(T39, T20, T21, div1_out_ggaa(T39, s(s(s(s(s(s(0)))))), T20, T21)) → div1_out_gaaa(s(s(s(s(s(s(T39)))))), s(s(s(s(s(s(0)))))), s(T20), T21)
div1_in_gaaa(s(s(s(s(s(s(s(T40))))))), s(s(s(s(s(s(s(T41))))))), s(T20), T21) → U7_gaaa(T40, T41, T20, T21, minus61_in_gaa(T40, T41, X94))
minus61_in_gaa(T44, 0, T44) → minus61_out_gaa(T44, 0, T44)
minus61_in_gaa(s(T45), s(T46), X104) → U10_gaa(T45, T46, X104, minus61_in_gaa(T45, T46, X104))
U10_gaa(T45, T46, X104, minus61_out_gaa(T45, T46, X104)) → minus61_out_gaa(s(T45), s(T46), X104)
U7_gaaa(T40, T41, T20, T21, minus61_out_gaa(T40, T41, X94)) → div1_out_gaaa(s(s(s(s(s(s(s(T40))))))), s(s(s(s(s(s(s(T41))))))), s(T20), T21)
div1_in_gaaa(s(s(s(s(s(s(s(T40))))))), s(s(s(s(s(s(s(T41))))))), s(T20), T21) → U8_gaaa(T40, T41, T20, T21, minus61_in_gaa(T40, T41, T43))
U8_gaaa(T40, T41, T20, T21, minus61_out_gaa(T40, T41, T43)) → U9_gaaa(T40, T41, T20, T21, div1_in_gaaa(T43, s(T42), T20, T21))
div1_in_gaaa(s(s(s(s(s(s(T47)))))), s(s(s(s(s(s(T48)))))), T49, s(s(s(s(s(s(T47))))))) → div1_out_gaaa(s(s(s(s(s(s(T47)))))), s(s(s(s(s(s(T48)))))), T49, s(s(s(s(s(s(T47)))))))
div1_in_gaaa(s(s(s(s(s(T50))))), s(s(s(s(s(T51))))), T52, s(s(s(s(s(T50)))))) → div1_out_gaaa(s(s(s(s(s(T50))))), s(s(s(s(s(T51))))), T52, s(s(s(s(s(T50))))))
div1_in_gaaa(s(s(s(s(T53)))), s(s(s(s(T54)))), T55, s(s(s(s(T53))))) → div1_out_gaaa(s(s(s(s(T53)))), s(s(s(s(T54)))), T55, s(s(s(s(T53)))))
div1_in_gaaa(s(s(s(T56))), s(s(s(T57))), T58, s(s(s(T56)))) → div1_out_gaaa(s(s(s(T56))), s(s(s(T57))), T58, s(s(s(T56))))
div1_in_gaaa(s(s(T59)), s(s(T60)), T61, s(s(T59))) → div1_out_gaaa(s(s(T59)), s(s(T60)), T61, s(s(T59)))
div1_in_gaaa(s(T62), s(T63), T64, s(T62)) → div1_out_gaaa(s(T62), s(T63), T64, s(T62))
div1_in_gaaa(T65, T66, T67, T65) → div1_out_gaaa(T65, T66, T67, T65)
U9_gaaa(T40, T41, T20, T21, div1_out_gaaa(T43, s(T42), T20, T21)) → div1_out_gaaa(s(s(s(s(s(s(s(T40))))))), s(s(s(s(s(s(s(T41))))))), s(T20), T21)
U9_ggaa(T40, T41, T20, T21, div1_out_gaaa(T43, s(T42), T20, T21)) → div1_out_ggaa(s(s(s(s(s(s(s(T40))))))), s(s(s(s(s(s(s(T41))))))), s(T20), T21)
U6_ggaa(T39, T20, T21, div1_out_ggaa(T39, s(s(s(s(s(s(0)))))), T20, T21)) → div1_out_ggaa(s(s(s(s(s(s(T39)))))), s(s(s(s(s(s(0)))))), s(T20), T21)
U5_ggaa(T36, T20, T21, div1_out_ggaa(T36, s(s(s(s(s(0))))), T20, T21)) → div1_out_ggaa(s(s(s(s(s(T36))))), s(s(s(s(s(0))))), s(T20), T21)
U4_ggaa(T33, T20, T21, div1_out_ggaa(T33, s(s(s(s(0)))), T20, T21)) → div1_out_ggaa(s(s(s(s(T33)))), s(s(s(s(0)))), s(T20), T21)
U3_ggaa(T30, T20, T21, div1_out_ggaa(T30, s(s(s(0))), T20, T21)) → div1_out_ggaa(s(s(s(T30))), s(s(s(0))), s(T20), T21)
U2_ggaa(T27, T20, T21, div1_out_ggaa(T27, s(s(0)), T20, T21)) → div1_out_ggaa(s(s(T27)), s(s(0)), s(T20), T21)
U1_ggaa(T24, T20, T21, div1_out_ggaa(T24, s(0), T20, T21)) → div1_out_ggaa(s(T24), s(0), s(T20), T21)

The argument filtering Pi contains the following mapping:
div1_in_ggaa(x1, x2, x3, x4) = div1_in_ggaa(x1, x2)
0 = 0
div1_out_ggaa(x1, x2, x3, x4) = div1_out_ggaa
s(x1) = s(x1)
U1_ggaa(x1, x2, x3, x4) = U1_ggaa(x4)
U2_ggaa(x1, x2, x3, x4) = U2_ggaa(x4)
U3_ggaa(x1, x2, x3, x4) = U3_ggaa(x4)
U4_ggaa(x1, x2, x3, x4) = U4_ggaa(x4)
U5_ggaa(x1, x2, x3, x4) = U5_ggaa(x4)
U6_ggaa(x1, x2, x3, x4) = U6_ggaa(x4)
U7_ggaa(x1, x2, x3, x4, x5) = U7_ggaa(x5)
minus61_in_gga(x1, x2, x3) = minus61_in_gga(x1, x2)
minus61_out_gga(x1, x2, x3) = minus61_out_gga(x3)
U10_gga(x1, x2, x3, x4) = U10_gga(x4)
U8_ggaa(x1, x2, x3, x4, x5) = U8_ggaa(x5)
U9_ggaa(x1, x2, x3, x4, x5) = U9_ggaa(x5)
div1_in_gaaa(x1, x2, x3, x4) = div1_in_gaaa(x1)
div1_out_gaaa(x1, x2, x3, x4) = div1_out_gaaa
U1_gaaa(x1, x2, x3, x4) = U1_gaaa(x4)
U2_gaaa(x1, x2, x3, x4) = U2_gaaa(x4)
U3_gaaa(x1, x2, x3, x4) = U3_gaaa(x4)
U4_gaaa(x1, x2, x3, x4) = U4_gaaa(x4)
U5_gaaa(x1, x2, x3, x4) = U5_gaaa(x4)
U6_gaaa(x1, x2, x3, x4) = U6_gaaa(x4)
U7_gaaa(x1, x2, x3, x4, x5) = U7_gaaa(x5)
minus61_in_gaa(x1, x2, x3) = minus61_in_gaa(x1)
minus61_out_gaa(x1, x2, x3) = minus61_out_gaa(x2, x3)
U10_gaa(x1, x2, x3, x4) = U10_gaa(x4)
U8_gaaa(x1, x2, x3, x4, x5) = U8_gaaa(x5)
U9_gaaa(x1, x2, x3, x4, x5) = U9_gaaa(x5)
DIV1_IN_GGAA(x1, x2, x3, x4) = DIV1_IN_GGAA(x1, x2)
U1_GGAA(x1, x2, x3, x4) = U1_GGAA(x4)
U2_GGAA(x1, x2, x3, x4) = U2_GGAA(x4)
U3_GGAA(x1, x2, x3, x4) = U3_GGAA(x4)
U4_GGAA(x1, x2, x3, x4) = U4_GGAA(x4)
U5_GGAA(x1, x2, x3, x4) = U5_GGAA(x4)
U6_GGAA(x1, x2, x3, x4) = U6_GGAA(x4)
U7_GGAA(x1, x2, x3, x4, x5) = U7_GGAA(x5)
MINUS61_IN_GGA(x1, x2, x3) = MINUS61_IN_GGA(x1, x2)
U10_GGA(x1, x2, x3, x4) = U10_GGA(x4)
U8_GGAA(x1, x2, x3, x4, x5) = U8_GGAA(x5)
U9_GGAA(x1, x2, x3, x4, x5) = U9_GGAA(x5)
DIV1_IN_GAAA(x1, x2, x3, x4) = DIV1_IN_GAAA(x1)
U1_GAAA(x1, x2, x3, x4) = U1_GAAA(x4)
U2_GAAA(x1, x2, x3, x4) = U2_GAAA(x4)
U3_GAAA(x1, x2, x3, x4) = U3_GAAA(x4)
U4_GAAA(x1, x2, x3, x4) = U4_GAAA(x4)
U5_GAAA(x1, x2, x3, x4) = U5_GAAA(x4)
U6_GAAA(x1, x2, x3, x4) = U6_GAAA(x4)
U7_GAAA(x1, x2, x3, x4, x5) = U7_GAAA(x5)
MINUS61_IN_GAA(x1, x2, x3) = MINUS61_IN_GAA(x1)
U10_GAA(x1, x2, x3, x4) = U10_GAA(x4)
U8_GAAA(x1, x2, x3, x4, x5) = U8_GAAA(x5)
U9_GAAA(x1, x2, x3, x4, x5) = U9_GAAA(x5)

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

(6) Obligation:

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

DIV1_IN_GGAA(s(T24), s(0), s(T20), T21) → U1_GGAA(T24, T20, T21, div1_in_ggaa(T24, s(0), T20, T21))
DIV1_IN_GGAA(s(T24), s(0), s(T20), T21) → DIV1_IN_GGAA(T24, s(0), T20, T21)
DIV1_IN_GGAA(s(s(T27)), s(s(0)), s(T20), T21) → U2_GGAA(T27, T20, T21, div1_in_ggaa(T27, s(s(0)), T20, T21))
DIV1_IN_GGAA(s(s(T27)), s(s(0)), s(T20), T21) → DIV1_IN_GGAA(T27, s(s(0)), T20, T21)
DIV1_IN_GGAA(s(s(s(T30))), s(s(s(0))), s(T20), T21) → U3_GGAA(T30, T20, T21, div1_in_ggaa(T30, s(s(s(0))), T20, T21))
DIV1_IN_GGAA(s(s(s(T30))), s(s(s(0))), s(T20), T21) → DIV1_IN_GGAA(T30, s(s(s(0))), T20, T21)
DIV1_IN_GGAA(s(s(s(s(T33)))), s(s(s(s(0)))), s(T20), T21) → U4_GGAA(T33, T20, T21, div1_in_ggaa(T33, s(s(s(s(0)))), T20, T21))
DIV1_IN_GGAA(s(s(s(s(T33)))), s(s(s(s(0)))), s(T20), T21) → DIV1_IN_GGAA(T33, s(s(s(s(0)))), T20, T21)
DIV1_IN_GGAA(s(s(s(s(s(T36))))), s(s(s(s(s(0))))), s(T20), T21) → U5_GGAA(T36, T20, T21, div1_in_ggaa(T36, s(s(s(s(s(0))))), T20, T21))
DIV1_IN_GGAA(s(s(s(s(s(T36))))), s(s(s(s(s(0))))), s(T20), T21) → DIV1_IN_GGAA(T36, s(s(s(s(s(0))))), T20, T21)
DIV1_IN_GGAA(s(s(s(s(s(s(T39)))))), s(s(s(s(s(s(0)))))), s(T20), T21) → U6_GGAA(T39, T20, T21, div1_in_ggaa(T39, s(s(s(s(s(s(0)))))), T20, T21))
DIV1_IN_GGAA(s(s(s(s(s(s(T39)))))), s(s(s(s(s(s(0)))))), s(T20), T21) → DIV1_IN_GGAA(T39, s(s(s(s(s(s(0)))))), T20, T21)
DIV1_IN_GGAA(s(s(s(s(s(s(s(T40))))))), s(s(s(s(s(s(s(T41))))))), s(T20), T21) → U7_GGAA(T40, T41, T20, T21, minus61_in_gga(T40, T41, X94))
DIV1_IN_GGAA(s(s(s(s(s(s(s(T40))))))), s(s(s(s(s(s(s(T41))))))), s(T20), T21) → MINUS61_IN_GGA(T40, T41, X94)
MINUS61_IN_GGA(s(T45), s(T46), X104) → U10_GGA(T45, T46, X104, minus61_in_gga(T45, T46, X104))
MINUS61_IN_GGA(s(T45), s(T46), X104) → MINUS61_IN_GGA(T45, T46, X104)
DIV1_IN_GGAA(s(s(s(s(s(s(s(T40))))))), s(s(s(s(s(s(s(T41))))))), s(T20), T21) → U8_GGAA(T40, T41, T20, T21, minus61_in_gga(T40, T41, T43))
U8_GGAA(T40, T41, T20, T21, minus61_out_gga(T40, T41, T43)) → U9_GGAA(T40, T41, T20, T21, div1_in_gaaa(T43, s(T42), T20, T21))
U8_GGAA(T40, T41, T20, T21, minus61_out_gga(T40, T41, T43)) → DIV1_IN_GAAA(T43, s(T42), T20, T21)
DIV1_IN_GAAA(s(T24), s(0), s(T20), T21) → U1_GAAA(T24, T20, T21, div1_in_ggaa(T24, s(0), T20, T21))
DIV1_IN_GAAA(s(T24), s(0), s(T20), T21) → DIV1_IN_GGAA(T24, s(0), T20, T21)
DIV1_IN_GAAA(s(s(T27)), s(s(0)), s(T20), T21) → U2_GAAA(T27, T20, T21, div1_in_ggaa(T27, s(s(0)), T20, T21))
DIV1_IN_GAAA(s(s(T27)), s(s(0)), s(T20), T21) → DIV1_IN_GGAA(T27, s(s(0)), T20, T21)
DIV1_IN_GAAA(s(s(s(T30))), s(s(s(0))), s(T20), T21) → U3_GAAA(T30, T20, T21, div1_in_ggaa(T30, s(s(s(0))), T20, T21))
DIV1_IN_GAAA(s(s(s(T30))), s(s(s(0))), s(T20), T21) → DIV1_IN_GGAA(T30, s(s(s(0))), T20, T21)
DIV1_IN_GAAA(s(s(s(s(T33)))), s(s(s(s(0)))), s(T20), T21) → U4_GAAA(T33, T20, T21, div1_in_ggaa(T33, s(s(s(s(0)))), T20, T21))
DIV1_IN_GAAA(s(s(s(s(T33)))), s(s(s(s(0)))), s(T20), T21) → DIV1_IN_GGAA(T33, s(s(s(s(0)))), T20, T21)
DIV1_IN_GAAA(s(s(s(s(s(T36))))), s(s(s(s(s(0))))), s(T20), T21) → U5_GAAA(T36, T20, T21, div1_in_ggaa(T36, s(s(s(s(s(0))))), T20, T21))
DIV1_IN_GAAA(s(s(s(s(s(T36))))), s(s(s(s(s(0))))), s(T20), T21) → DIV1_IN_GGAA(T36, s(s(s(s(s(0))))), T20, T21)
DIV1_IN_GAAA(s(s(s(s(s(s(T39)))))), s(s(s(s(s(s(0)))))), s(T20), T21) → U6_GAAA(T39, T20, T21, div1_in_ggaa(T39, s(s(s(s(s(s(0)))))), T20, T21))
DIV1_IN_GAAA(s(s(s(s(s(s(T39)))))), s(s(s(s(s(s(0)))))), s(T20), T21) → DIV1_IN_GGAA(T39, s(s(s(s(s(s(0)))))), T20, T21)
DIV1_IN_GAAA(s(s(s(s(s(s(s(T40))))))), s(s(s(s(s(s(s(T41))))))), s(T20), T21) → U7_GAAA(T40, T41, T20, T21, minus61_in_gaa(T40, T41, X94))
DIV1_IN_GAAA(s(s(s(s(s(s(s(T40))))))), s(s(s(s(s(s(s(T41))))))), s(T20), T21) → MINUS61_IN_GAA(T40, T41, X94)
MINUS61_IN_GAA(s(T45), s(T46), X104) → U10_GAA(T45, T46, X104, minus61_in_gaa(T45, T46, X104))
MINUS61_IN_GAA(s(T45), s(T46), X104) → MINUS61_IN_GAA(T45, T46, X104)
DIV1_IN_GAAA(s(s(s(s(s(s(s(T40))))))), s(s(s(s(s(s(s(T41))))))), s(T20), T21) → U8_GAAA(T40, T41, T20, T21, minus61_in_gaa(T40, T41, T43))
U8_GAAA(T40, T41, T20, T21, minus61_out_gaa(T40, T41, T43)) → U9_GAAA(T40, T41, T20, T21, div1_in_gaaa(T43, s(T42), T20, T21))
U8_GAAA(T40, T41, T20, T21, minus61_out_gaa(T40, T41, T43)) → DIV1_IN_GAAA(T43, s(T42), T20, T21)

The TRS R consists of the following rules:

div1_in_ggaa(0, T8, 0, 0) → div1_out_ggaa(0, T8, 0, 0)
div1_in_ggaa(s(T24), s(0), s(T20), T21) → U1_ggaa(T24, T20, T21, div1_in_ggaa(T24, s(0), T20, T21))
div1_in_ggaa(s(s(T27)), s(s(0)), s(T20), T21) → U2_ggaa(T27, T20, T21, div1_in_ggaa(T27, s(s(0)), T20, T21))
div1_in_ggaa(s(s(s(T30))), s(s(s(0))), s(T20), T21) → U3_ggaa(T30, T20, T21, div1_in_ggaa(T30, s(s(s(0))), T20, T21))
div1_in_ggaa(s(s(s(s(T33)))), s(s(s(s(0)))), s(T20), T21) → U4_ggaa(T33, T20, T21, div1_in_ggaa(T33, s(s(s(s(0)))), T20, T21))
div1_in_ggaa(s(s(s(s(s(T36))))), s(s(s(s(s(0))))), s(T20), T21) → U5_ggaa(T36, T20, T21, div1_in_ggaa(T36, s(s(s(s(s(0))))), T20, T21))
div1_in_ggaa(s(s(s(s(s(s(T39)))))), s(s(s(s(s(s(0)))))), s(T20), T21) → U6_ggaa(T39, T20, T21, div1_in_ggaa(T39, s(s(s(s(s(s(0)))))), T20, T21))
div1_in_ggaa(s(s(s(s(s(s(s(T40))))))), s(s(s(s(s(s(s(T41))))))), s(T20), T21) → U7_ggaa(T40, T41, T20, T21, minus61_in_gga(T40, T41, X94))
minus61_in_gga(T44, 0, T44) → minus61_out_gga(T44, 0, T44)
minus61_in_gga(s(T45), s(T46), X104) → U10_gga(T45, T46, X104, minus61_in_gga(T45, T46, X104))
U10_gga(T45, T46, X104, minus61_out_gga(T45, T46, X104)) → minus61_out_gga(s(T45), s(T46), X104)
U7_ggaa(T40, T41, T20, T21, minus61_out_gga(T40, T41, X94)) → div1_out_ggaa(s(s(s(s(s(s(s(T40))))))), s(s(s(s(s(s(s(T41))))))), s(T20), T21)
div1_in_ggaa(s(s(s(s(s(s(s(T40))))))), s(s(s(s(s(s(s(T41))))))), s(T20), T21) → U8_ggaa(T40, T41, T20, T21, minus61_in_gga(T40, T41, T43))
U8_ggaa(T40, T41, T20, T21, minus61_out_gga(T40, T41, T43)) → U9_ggaa(T40, T41, T20, T21, div1_in_gaaa(T43, s(T42), T20, T21))
div1_in_gaaa(0, T8, 0, 0) → div1_out_gaaa(0, T8, 0, 0)
div1_in_gaaa(s(T24), s(0), s(T20), T21) → U1_gaaa(T24, T20, T21, div1_in_ggaa(T24, s(0), T20, T21))
div1_in_ggaa(s(s(s(s(s(s(T47)))))), s(s(s(s(s(s(T48)))))), T49, s(s(s(s(s(s(T47))))))) → div1_out_ggaa(s(s(s(s(s(s(T47)))))), s(s(s(s(s(s(T48)))))), T49, s(s(s(s(s(s(T47)))))))
div1_in_ggaa(s(s(s(s(s(T50))))), s(s(s(s(s(T51))))), T52, s(s(s(s(s(T50)))))) → div1_out_ggaa(s(s(s(s(s(T50))))), s(s(s(s(s(T51))))), T52, s(s(s(s(s(T50))))))
div1_in_ggaa(s(s(s(s(T53)))), s(s(s(s(T54)))), T55, s(s(s(s(T53))))) → div1_out_ggaa(s(s(s(s(T53)))), s(s(s(s(T54)))), T55, s(s(s(s(T53)))))
div1_in_ggaa(s(s(s(T56))), s(s(s(T57))), T58, s(s(s(T56)))) → div1_out_ggaa(s(s(s(T56))), s(s(s(T57))), T58, s(s(s(T56))))
div1_in_ggaa(s(s(T59)), s(s(T60)), T61, s(s(T59))) → div1_out_ggaa(s(s(T59)), s(s(T60)), T61, s(s(T59)))
div1_in_ggaa(s(T62), s(T63), T64, s(T62)) → div1_out_ggaa(s(T62), s(T63), T64, s(T62))
div1_in_ggaa(T65, T66, T67, T65) → div1_out_ggaa(T65, T66, T67, T65)
U1_gaaa(T24, T20, T21, div1_out_ggaa(T24, s(0), T20, T21)) → div1_out_gaaa(s(T24), s(0), s(T20), T21)
div1_in_gaaa(s(s(T27)), s(s(0)), s(T20), T21) → U2_gaaa(T27, T20, T21, div1_in_ggaa(T27, s(s(0)), T20, T21))
U2_gaaa(T27, T20, T21, div1_out_ggaa(T27, s(s(0)), T20, T21)) → div1_out_gaaa(s(s(T27)), s(s(0)), s(T20), T21)
div1_in_gaaa(s(s(s(T30))), s(s(s(0))), s(T20), T21) → U3_gaaa(T30, T20, T21, div1_in_ggaa(T30, s(s(s(0))), T20, T21))
U3_gaaa(T30, T20, T21, div1_out_ggaa(T30, s(s(s(0))), T20, T21)) → div1_out_gaaa(s(s(s(T30))), s(s(s(0))), s(T20), T21)
div1_in_gaaa(s(s(s(s(T33)))), s(s(s(s(0)))), s(T20), T21) → U4_gaaa(T33, T20, T21, div1_in_ggaa(T33, s(s(s(s(0)))), T20, T21))
U4_gaaa(T33, T20, T21, div1_out_ggaa(T33, s(s(s(s(0)))), T20, T21)) → div1_out_gaaa(s(s(s(s(T33)))), s(s(s(s(0)))), s(T20), T21)
div1_in_gaaa(s(s(s(s(s(T36))))), s(s(s(s(s(0))))), s(T20), T21) → U5_gaaa(T36, T20, T21, div1_in_ggaa(T36, s(s(s(s(s(0))))), T20, T21))
U5_gaaa(T36, T20, T21, div1_out_ggaa(T36, s(s(s(s(s(0))))), T20, T21)) → div1_out_gaaa(s(s(s(s(s(T36))))), s(s(s(s(s(0))))), s(T20), T21)
div1_in_gaaa(s(s(s(s(s(s(T39)))))), s(s(s(s(s(s(0)))))), s(T20), T21) → U6_gaaa(T39, T20, T21, div1_in_ggaa(T39, s(s(s(s(s(s(0)))))), T20, T21))
U6_gaaa(T39, T20, T21, div1_out_ggaa(T39, s(s(s(s(s(s(0)))))), T20, T21)) → div1_out_gaaa(s(s(s(s(s(s(T39)))))), s(s(s(s(s(s(0)))))), s(T20), T21)
div1_in_gaaa(s(s(s(s(s(s(s(T40))))))), s(s(s(s(s(s(s(T41))))))), s(T20), T21) → U7_gaaa(T40, T41, T20, T21, minus61_in_gaa(T40, T41, X94))
minus61_in_gaa(T44, 0, T44) → minus61_out_gaa(T44, 0, T44)
minus61_in_gaa(s(T45), s(T46), X104) → U10_gaa(T45, T46, X104, minus61_in_gaa(T45, T46, X104))
U10_gaa(T45, T46, X104, minus61_out_gaa(T45, T46, X104)) → minus61_out_gaa(s(T45), s(T46), X104)
U7_gaaa(T40, T41, T20, T21, minus61_out_gaa(T40, T41, X94)) → div1_out_gaaa(s(s(s(s(s(s(s(T40))))))), s(s(s(s(s(s(s(T41))))))), s(T20), T21)
div1_in_gaaa(s(s(s(s(s(s(s(T40))))))), s(s(s(s(s(s(s(T41))))))), s(T20), T21) → U8_gaaa(T40, T41, T20, T21, minus61_in_gaa(T40, T41, T43))
U8_gaaa(T40, T41, T20, T21, minus61_out_gaa(T40, T41, T43)) → U9_gaaa(T40, T41, T20, T21, div1_in_gaaa(T43, s(T42), T20, T21))
div1_in_gaaa(s(s(s(s(s(s(T47)))))), s(s(s(s(s(s(T48)))))), T49, s(s(s(s(s(s(T47))))))) → div1_out_gaaa(s(s(s(s(s(s(T47)))))), s(s(s(s(s(s(T48)))))), T49, s(s(s(s(s(s(T47)))))))
div1_in_gaaa(s(s(s(s(s(T50))))), s(s(s(s(s(T51))))), T52, s(s(s(s(s(T50)))))) → div1_out_gaaa(s(s(s(s(s(T50))))), s(s(s(s(s(T51))))), T52, s(s(s(s(s(T50))))))
div1_in_gaaa(s(s(s(s(T53)))), s(s(s(s(T54)))), T55, s(s(s(s(T53))))) → div1_out_gaaa(s(s(s(s(T53)))), s(s(s(s(T54)))), T55, s(s(s(s(T53)))))
div1_in_gaaa(s(s(s(T56))), s(s(s(T57))), T58, s(s(s(T56)))) → div1_out_gaaa(s(s(s(T56))), s(s(s(T57))), T58, s(s(s(T56))))
div1_in_gaaa(s(s(T59)), s(s(T60)), T61, s(s(T59))) → div1_out_gaaa(s(s(T59)), s(s(T60)), T61, s(s(T59)))
div1_in_gaaa(s(T62), s(T63), T64, s(T62)) → div1_out_gaaa(s(T62), s(T63), T64, s(T62))
div1_in_gaaa(T65, T66, T67, T65) → div1_out_gaaa(T65, T66, T67, T65)
U9_gaaa(T40, T41, T20, T21, div1_out_gaaa(T43, s(T42), T20, T21)) → div1_out_gaaa(s(s(s(s(s(s(s(T40))))))), s(s(s(s(s(s(s(T41))))))), s(T20), T21)
U9_ggaa(T40, T41, T20, T21, div1_out_gaaa(T43, s(T42), T20, T21)) → div1_out_ggaa(s(s(s(s(s(s(s(T40))))))), s(s(s(s(s(s(s(T41))))))), s(T20), T21)
U6_ggaa(T39, T20, T21, div1_out_ggaa(T39, s(s(s(s(s(s(0)))))), T20, T21)) → div1_out_ggaa(s(s(s(s(s(s(T39)))))), s(s(s(s(s(s(0)))))), s(T20), T21)
U5_ggaa(T36, T20, T21, div1_out_ggaa(T36, s(s(s(s(s(0))))), T20, T21)) → div1_out_ggaa(s(s(s(s(s(T36))))), s(s(s(s(s(0))))), s(T20), T21)
U4_ggaa(T33, T20, T21, div1_out_ggaa(T33, s(s(s(s(0)))), T20, T21)) → div1_out_ggaa(s(s(s(s(T33)))), s(s(s(s(0)))), s(T20), T21)
U3_ggaa(T30, T20, T21, div1_out_ggaa(T30, s(s(s(0))), T20, T21)) → div1_out_ggaa(s(s(s(T30))), s(s(s(0))), s(T20), T21)
U2_ggaa(T27, T20, T21, div1_out_ggaa(T27, s(s(0)), T20, T21)) → div1_out_ggaa(s(s(T27)), s(s(0)), s(T20), T21)
U1_ggaa(T24, T20, T21, div1_out_ggaa(T24, s(0), T20, T21)) → div1_out_ggaa(s(T24), s(0), s(T20), T21)

(7) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 9 SCCs with 28 less nodes.

(8) Complex Obligation (AND)

(9) Obligation:

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

MINUS61_IN_GAA(s(T45), s(T46), X104) → MINUS61_IN_GAA(T45, T46, X104)

The TRS R consists of the following rules:

div1_in_ggaa(0, T8, 0, 0) → div1_out_ggaa(0, T8, 0, 0)
div1_in_ggaa(s(T24), s(0), s(T20), T21) → U1_ggaa(T24, T20, T21, div1_in_ggaa(T24, s(0), T20, T21))
div1_in_ggaa(s(s(T27)), s(s(0)), s(T20), T21) → U2_ggaa(T27, T20, T21, div1_in_ggaa(T27, s(s(0)), T20, T21))
div1_in_ggaa(s(s(s(T30))), s(s(s(0))), s(T20), T21) → U3_ggaa(T30, T20, T21, div1_in_ggaa(T30, s(s(s(0))), T20, T21))
div1_in_ggaa(s(s(s(s(T33)))), s(s(s(s(0)))), s(T20), T21) → U4_ggaa(T33, T20, T21, div1_in_ggaa(T33, s(s(s(s(0)))), T20, T21))
div1_in_ggaa(s(s(s(s(s(T36))))), s(s(s(s(s(0))))), s(T20), T21) → U5_ggaa(T36, T20, T21, div1_in_ggaa(T36, s(s(s(s(s(0))))), T20, T21))
div1_in_ggaa(s(s(s(s(s(s(T39)))))), s(s(s(s(s(s(0)))))), s(T20), T21) → U6_ggaa(T39, T20, T21, div1_in_ggaa(T39, s(s(s(s(s(s(0)))))), T20, T21))
div1_in_ggaa(s(s(s(s(s(s(s(T40))))))), s(s(s(s(s(s(s(T41))))))), s(T20), T21) → U7_ggaa(T40, T41, T20, T21, minus61_in_gga(T40, T41, X94))
minus61_in_gga(T44, 0, T44) → minus61_out_gga(T44, 0, T44)
minus61_in_gga(s(T45), s(T46), X104) → U10_gga(T45, T46, X104, minus61_in_gga(T45, T46, X104))
U10_gga(T45, T46, X104, minus61_out_gga(T45, T46, X104)) → minus61_out_gga(s(T45), s(T46), X104)
U7_ggaa(T40, T41, T20, T21, minus61_out_gga(T40, T41, X94)) → div1_out_ggaa(s(s(s(s(s(s(s(T40))))))), s(s(s(s(s(s(s(T41))))))), s(T20), T21)
div1_in_ggaa(s(s(s(s(s(s(s(T40))))))), s(s(s(s(s(s(s(T41))))))), s(T20), T21) → U8_ggaa(T40, T41, T20, T21, minus61_in_gga(T40, T41, T43))
U8_ggaa(T40, T41, T20, T21, minus61_out_gga(T40, T41, T43)) → U9_ggaa(T40, T41, T20, T21, div1_in_gaaa(T43, s(T42), T20, T21))
div1_in_gaaa(0, T8, 0, 0) → div1_out_gaaa(0, T8, 0, 0)
div1_in_gaaa(s(T24), s(0), s(T20), T21) → U1_gaaa(T24, T20, T21, div1_in_ggaa(T24, s(0), T20, T21))
div1_in_ggaa(s(s(s(s(s(s(T47)))))), s(s(s(s(s(s(T48)))))), T49, s(s(s(s(s(s(T47))))))) → div1_out_ggaa(s(s(s(s(s(s(T47)))))), s(s(s(s(s(s(T48)))))), T49, s(s(s(s(s(s(T47)))))))
div1_in_ggaa(s(s(s(s(s(T50))))), s(s(s(s(s(T51))))), T52, s(s(s(s(s(T50)))))) → div1_out_ggaa(s(s(s(s(s(T50))))), s(s(s(s(s(T51))))), T52, s(s(s(s(s(T50))))))
div1_in_ggaa(s(s(s(s(T53)))), s(s(s(s(T54)))), T55, s(s(s(s(T53))))) → div1_out_ggaa(s(s(s(s(T53)))), s(s(s(s(T54)))), T55, s(s(s(s(T53)))))
div1_in_ggaa(s(s(s(T56))), s(s(s(T57))), T58, s(s(s(T56)))) → div1_out_ggaa(s(s(s(T56))), s(s(s(T57))), T58, s(s(s(T56))))
div1_in_ggaa(s(s(T59)), s(s(T60)), T61, s(s(T59))) → div1_out_ggaa(s(s(T59)), s(s(T60)), T61, s(s(T59)))
div1_in_ggaa(s(T62), s(T63), T64, s(T62)) → div1_out_ggaa(s(T62), s(T63), T64, s(T62))
div1_in_ggaa(T65, T66, T67, T65) → div1_out_ggaa(T65, T66, T67, T65)
U1_gaaa(T24, T20, T21, div1_out_ggaa(T24, s(0), T20, T21)) → div1_out_gaaa(s(T24), s(0), s(T20), T21)
div1_in_gaaa(s(s(T27)), s(s(0)), s(T20), T21) → U2_gaaa(T27, T20, T21, div1_in_ggaa(T27, s(s(0)), T20, T21))
U2_gaaa(T27, T20, T21, div1_out_ggaa(T27, s(s(0)), T20, T21)) → div1_out_gaaa(s(s(T27)), s(s(0)), s(T20), T21)
div1_in_gaaa(s(s(s(T30))), s(s(s(0))), s(T20), T21) → U3_gaaa(T30, T20, T21, div1_in_ggaa(T30, s(s(s(0))), T20, T21))
U3_gaaa(T30, T20, T21, div1_out_ggaa(T30, s(s(s(0))), T20, T21)) → div1_out_gaaa(s(s(s(T30))), s(s(s(0))), s(T20), T21)
div1_in_gaaa(s(s(s(s(T33)))), s(s(s(s(0)))), s(T20), T21) → U4_gaaa(T33, T20, T21, div1_in_ggaa(T33, s(s(s(s(0)))), T20, T21))
U4_gaaa(T33, T20, T21, div1_out_ggaa(T33, s(s(s(s(0)))), T20, T21)) → div1_out_gaaa(s(s(s(s(T33)))), s(s(s(s(0)))), s(T20), T21)
div1_in_gaaa(s(s(s(s(s(T36))))), s(s(s(s(s(0))))), s(T20), T21) → U5_gaaa(T36, T20, T21, div1_in_ggaa(T36, s(s(s(s(s(0))))), T20, T21))
U5_gaaa(T36, T20, T21, div1_out_ggaa(T36, s(s(s(s(s(0))))), T20, T21)) → div1_out_gaaa(s(s(s(s(s(T36))))), s(s(s(s(s(0))))), s(T20), T21)
div1_in_gaaa(s(s(s(s(s(s(T39)))))), s(s(s(s(s(s(0)))))), s(T20), T21) → U6_gaaa(T39, T20, T21, div1_in_ggaa(T39, s(s(s(s(s(s(0)))))), T20, T21))
U6_gaaa(T39, T20, T21, div1_out_ggaa(T39, s(s(s(s(s(s(0)))))), T20, T21)) → div1_out_gaaa(s(s(s(s(s(s(T39)))))), s(s(s(s(s(s(0)))))), s(T20), T21)
div1_in_gaaa(s(s(s(s(s(s(s(T40))))))), s(s(s(s(s(s(s(T41))))))), s(T20), T21) → U7_gaaa(T40, T41, T20, T21, minus61_in_gaa(T40, T41, X94))
minus61_in_gaa(T44, 0, T44) → minus61_out_gaa(T44, 0, T44)
minus61_in_gaa(s(T45), s(T46), X104) → U10_gaa(T45, T46, X104, minus61_in_gaa(T45, T46, X104))
U10_gaa(T45, T46, X104, minus61_out_gaa(T45, T46, X104)) → minus61_out_gaa(s(T45), s(T46), X104)
U7_gaaa(T40, T41, T20, T21, minus61_out_gaa(T40, T41, X94)) → div1_out_gaaa(s(s(s(s(s(s(s(T40))))))), s(s(s(s(s(s(s(T41))))))), s(T20), T21)
div1_in_gaaa(s(s(s(s(s(s(s(T40))))))), s(s(s(s(s(s(s(T41))))))), s(T20), T21) → U8_gaaa(T40, T41, T20, T21, minus61_in_gaa(T40, T41, T43))
U8_gaaa(T40, T41, T20, T21, minus61_out_gaa(T40, T41, T43)) → U9_gaaa(T40, T41, T20, T21, div1_in_gaaa(T43, s(T42), T20, T21))
div1_in_gaaa(s(s(s(s(s(s(T47)))))), s(s(s(s(s(s(T48)))))), T49, s(s(s(s(s(s(T47))))))) → div1_out_gaaa(s(s(s(s(s(s(T47)))))), s(s(s(s(s(s(T48)))))), T49, s(s(s(s(s(s(T47)))))))
div1_in_gaaa(s(s(s(s(s(T50))))), s(s(s(s(s(T51))))), T52, s(s(s(s(s(T50)))))) → div1_out_gaaa(s(s(s(s(s(T50))))), s(s(s(s(s(T51))))), T52, s(s(s(s(s(T50))))))
div1_in_gaaa(s(s(s(s(T53)))), s(s(s(s(T54)))), T55, s(s(s(s(T53))))) → div1_out_gaaa(s(s(s(s(T53)))), s(s(s(s(T54)))), T55, s(s(s(s(T53)))))
div1_in_gaaa(s(s(s(T56))), s(s(s(T57))), T58, s(s(s(T56)))) → div1_out_gaaa(s(s(s(T56))), s(s(s(T57))), T58, s(s(s(T56))))
div1_in_gaaa(s(s(T59)), s(s(T60)), T61, s(s(T59))) → div1_out_gaaa(s(s(T59)), s(s(T60)), T61, s(s(T59)))
div1_in_gaaa(s(T62), s(T63), T64, s(T62)) → div1_out_gaaa(s(T62), s(T63), T64, s(T62))
div1_in_gaaa(T65, T66, T67, T65) → div1_out_gaaa(T65, T66, T67, T65)
U9_gaaa(T40, T41, T20, T21, div1_out_gaaa(T43, s(T42), T20, T21)) → div1_out_gaaa(s(s(s(s(s(s(s(T40))))))), s(s(s(s(s(s(s(T41))))))), s(T20), T21)
U9_ggaa(T40, T41, T20, T21, div1_out_gaaa(T43, s(T42), T20, T21)) → div1_out_ggaa(s(s(s(s(s(s(s(T40))))))), s(s(s(s(s(s(s(T41))))))), s(T20), T21)
U6_ggaa(T39, T20, T21, div1_out_ggaa(T39, s(s(s(s(s(s(0)))))), T20, T21)) → div1_out_ggaa(s(s(s(s(s(s(T39)))))), s(s(s(s(s(s(0)))))), s(T20), T21)
U5_ggaa(T36, T20, T21, div1_out_ggaa(T36, s(s(s(s(s(0))))), T20, T21)) → div1_out_ggaa(s(s(s(s(s(T36))))), s(s(s(s(s(0))))), s(T20), T21)
U4_ggaa(T33, T20, T21, div1_out_ggaa(T33, s(s(s(s(0)))), T20, T21)) → div1_out_ggaa(s(s(s(s(T33)))), s(s(s(s(0)))), s(T20), T21)
U3_ggaa(T30, T20, T21, div1_out_ggaa(T30, s(s(s(0))), T20, T21)) → div1_out_ggaa(s(s(s(T30))), s(s(s(0))), s(T20), T21)
U2_ggaa(T27, T20, T21, div1_out_ggaa(T27, s(s(0)), T20, T21)) → div1_out_ggaa(s(s(T27)), s(s(0)), s(T20), T21)
U1_ggaa(T24, T20, T21, div1_out_ggaa(T24, s(0), T20, T21)) → div1_out_ggaa(s(T24), s(0), s(T20), T21)

(10) UsableRulesProof (EQUIVALENT transformation)

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

(11) Obligation:

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

MINUS61_IN_GAA(s(T45), s(T46), X104) → MINUS61_IN_GAA(T45, T46, X104)

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

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

(12) PiDPToQDPProof (SOUND transformation)

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

(13) Obligation:

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

MINUS61_IN_GAA(s(T45)) → MINUS61_IN_GAA(T45)

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

(14) QDPSizeChangeProof (EQUIVALENT transformation)

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

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

MINUS61_IN_GAA(s(T45)) → MINUS61_IN_GAA(T45)
The graph contains the following edges 1 > 1

(15) TRUE

(16) Obligation:

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

MINUS61_IN_GGA(s(T45), s(T46), X104) → MINUS61_IN_GGA(T45, T46, X104)

The TRS R consists of the following rules:

div1_in_ggaa(0, T8, 0, 0) → div1_out_ggaa(0, T8, 0, 0)
div1_in_ggaa(s(T24), s(0), s(T20), T21) → U1_ggaa(T24, T20, T21, div1_in_ggaa(T24, s(0), T20, T21))
div1_in_ggaa(s(s(T27)), s(s(0)), s(T20), T21) → U2_ggaa(T27, T20, T21, div1_in_ggaa(T27, s(s(0)), T20, T21))
div1_in_ggaa(s(s(s(T30))), s(s(s(0))), s(T20), T21) → U3_ggaa(T30, T20, T21, div1_in_ggaa(T30, s(s(s(0))), T20, T21))
div1_in_ggaa(s(s(s(s(T33)))), s(s(s(s(0)))), s(T20), T21) → U4_ggaa(T33, T20, T21, div1_in_ggaa(T33, s(s(s(s(0)))), T20, T21))
div1_in_ggaa(s(s(s(s(s(T36))))), s(s(s(s(s(0))))), s(T20), T21) → U5_ggaa(T36, T20, T21, div1_in_ggaa(T36, s(s(s(s(s(0))))), T20, T21))
div1_in_ggaa(s(s(s(s(s(s(T39)))))), s(s(s(s(s(s(0)))))), s(T20), T21) → U6_ggaa(T39, T20, T21, div1_in_ggaa(T39, s(s(s(s(s(s(0)))))), T20, T21))
div1_in_ggaa(s(s(s(s(s(s(s(T40))))))), s(s(s(s(s(s(s(T41))))))), s(T20), T21) → U7_ggaa(T40, T41, T20, T21, minus61_in_gga(T40, T41, X94))
minus61_in_gga(T44, 0, T44) → minus61_out_gga(T44, 0, T44)
minus61_in_gga(s(T45), s(T46), X104) → U10_gga(T45, T46, X104, minus61_in_gga(T45, T46, X104))
U10_gga(T45, T46, X104, minus61_out_gga(T45, T46, X104)) → minus61_out_gga(s(T45), s(T46), X104)
U7_ggaa(T40, T41, T20, T21, minus61_out_gga(T40, T41, X94)) → div1_out_ggaa(s(s(s(s(s(s(s(T40))))))), s(s(s(s(s(s(s(T41))))))), s(T20), T21)
div1_in_ggaa(s(s(s(s(s(s(s(T40))))))), s(s(s(s(s(s(s(T41))))))), s(T20), T21) → U8_ggaa(T40, T41, T20, T21, minus61_in_gga(T40, T41, T43))
U8_ggaa(T40, T41, T20, T21, minus61_out_gga(T40, T41, T43)) → U9_ggaa(T40, T41, T20, T21, div1_in_gaaa(T43, s(T42), T20, T21))
div1_in_gaaa(0, T8, 0, 0) → div1_out_gaaa(0, T8, 0, 0)
div1_in_gaaa(s(T24), s(0), s(T20), T21) → U1_gaaa(T24, T20, T21, div1_in_ggaa(T24, s(0), T20, T21))
div1_in_ggaa(s(s(s(s(s(s(T47)))))), s(s(s(s(s(s(T48)))))), T49, s(s(s(s(s(s(T47))))))) → div1_out_ggaa(s(s(s(s(s(s(T47)))))), s(s(s(s(s(s(T48)))))), T49, s(s(s(s(s(s(T47)))))))
div1_in_ggaa(s(s(s(s(s(T50))))), s(s(s(s(s(T51))))), T52, s(s(s(s(s(T50)))))) → div1_out_ggaa(s(s(s(s(s(T50))))), s(s(s(s(s(T51))))), T52, s(s(s(s(s(T50))))))
div1_in_ggaa(s(s(s(s(T53)))), s(s(s(s(T54)))), T55, s(s(s(s(T53))))) → div1_out_ggaa(s(s(s(s(T53)))), s(s(s(s(T54)))), T55, s(s(s(s(T53)))))
div1_in_ggaa(s(s(s(T56))), s(s(s(T57))), T58, s(s(s(T56)))) → div1_out_ggaa(s(s(s(T56))), s(s(s(T57))), T58, s(s(s(T56))))
div1_in_ggaa(s(s(T59)), s(s(T60)), T61, s(s(T59))) → div1_out_ggaa(s(s(T59)), s(s(T60)), T61, s(s(T59)))
div1_in_ggaa(s(T62), s(T63), T64, s(T62)) → div1_out_ggaa(s(T62), s(T63), T64, s(T62))
div1_in_ggaa(T65, T66, T67, T65) → div1_out_ggaa(T65, T66, T67, T65)
U1_gaaa(T24, T20, T21, div1_out_ggaa(T24, s(0), T20, T21)) → div1_out_gaaa(s(T24), s(0), s(T20), T21)
div1_in_gaaa(s(s(T27)), s(s(0)), s(T20), T21) → U2_gaaa(T27, T20, T21, div1_in_ggaa(T27, s(s(0)), T20, T21))
U2_gaaa(T27, T20, T21, div1_out_ggaa(T27, s(s(0)), T20, T21)) → div1_out_gaaa(s(s(T27)), s(s(0)), s(T20), T21)
div1_in_gaaa(s(s(s(T30))), s(s(s(0))), s(T20), T21) → U3_gaaa(T30, T20, T21, div1_in_ggaa(T30, s(s(s(0))), T20, T21))
U3_gaaa(T30, T20, T21, div1_out_ggaa(T30, s(s(s(0))), T20, T21)) → div1_out_gaaa(s(s(s(T30))), s(s(s(0))), s(T20), T21)
div1_in_gaaa(s(s(s(s(T33)))), s(s(s(s(0)))), s(T20), T21) → U4_gaaa(T33, T20, T21, div1_in_ggaa(T33, s(s(s(s(0)))), T20, T21))
U4_gaaa(T33, T20, T21, div1_out_ggaa(T33, s(s(s(s(0)))), T20, T21)) → div1_out_gaaa(s(s(s(s(T33)))), s(s(s(s(0)))), s(T20), T21)
div1_in_gaaa(s(s(s(s(s(T36))))), s(s(s(s(s(0))))), s(T20), T21) → U5_gaaa(T36, T20, T21, div1_in_ggaa(T36, s(s(s(s(s(0))))), T20, T21))
U5_gaaa(T36, T20, T21, div1_out_ggaa(T36, s(s(s(s(s(0))))), T20, T21)) → div1_out_gaaa(s(s(s(s(s(T36))))), s(s(s(s(s(0))))), s(T20), T21)
div1_in_gaaa(s(s(s(s(s(s(T39)))))), s(s(s(s(s(s(0)))))), s(T20), T21) → U6_gaaa(T39, T20, T21, div1_in_ggaa(T39, s(s(s(s(s(s(0)))))), T20, T21))
U6_gaaa(T39, T20, T21, div1_out_ggaa(T39, s(s(s(s(s(s(0)))))), T20, T21)) → div1_out_gaaa(s(s(s(s(s(s(T39)))))), s(s(s(s(s(s(0)))))), s(T20), T21)
div1_in_gaaa(s(s(s(s(s(s(s(T40))))))), s(s(s(s(s(s(s(T41))))))), s(T20), T21) → U7_gaaa(T40, T41, T20, T21, minus61_in_gaa(T40, T41, X94))
minus61_in_gaa(T44, 0, T44) → minus61_out_gaa(T44, 0, T44)
minus61_in_gaa(s(T45), s(T46), X104) → U10_gaa(T45, T46, X104, minus61_in_gaa(T45, T46, X104))
U10_gaa(T45, T46, X104, minus61_out_gaa(T45, T46, X104)) → minus61_out_gaa(s(T45), s(T46), X104)
U7_gaaa(T40, T41, T20, T21, minus61_out_gaa(T40, T41, X94)) → div1_out_gaaa(s(s(s(s(s(s(s(T40))))))), s(s(s(s(s(s(s(T41))))))), s(T20), T21)
div1_in_gaaa(s(s(s(s(s(s(s(T40))))))), s(s(s(s(s(s(s(T41))))))), s(T20), T21) → U8_gaaa(T40, T41, T20, T21, minus61_in_gaa(T40, T41, T43))
U8_gaaa(T40, T41, T20, T21, minus61_out_gaa(T40, T41, T43)) → U9_gaaa(T40, T41, T20, T21, div1_in_gaaa(T43, s(T42), T20, T21))
div1_in_gaaa(s(s(s(s(s(s(T47)))))), s(s(s(s(s(s(T48)))))), T49, s(s(s(s(s(s(T47))))))) → div1_out_gaaa(s(s(s(s(s(s(T47)))))), s(s(s(s(s(s(T48)))))), T49, s(s(s(s(s(s(T47)))))))
div1_in_gaaa(s(s(s(s(s(T50))))), s(s(s(s(s(T51))))), T52, s(s(s(s(s(T50)))))) → div1_out_gaaa(s(s(s(s(s(T50))))), s(s(s(s(s(T51))))), T52, s(s(s(s(s(T50))))))
div1_in_gaaa(s(s(s(s(T53)))), s(s(s(s(T54)))), T55, s(s(s(s(T53))))) → div1_out_gaaa(s(s(s(s(T53)))), s(s(s(s(T54)))), T55, s(s(s(s(T53)))))
div1_in_gaaa(s(s(s(T56))), s(s(s(T57))), T58, s(s(s(T56)))) → div1_out_gaaa(s(s(s(T56))), s(s(s(T57))), T58, s(s(s(T56))))
div1_in_gaaa(s(s(T59)), s(s(T60)), T61, s(s(T59))) → div1_out_gaaa(s(s(T59)), s(s(T60)), T61, s(s(T59)))
div1_in_gaaa(s(T62), s(T63), T64, s(T62)) → div1_out_gaaa(s(T62), s(T63), T64, s(T62))
div1_in_gaaa(T65, T66, T67, T65) → div1_out_gaaa(T65, T66, T67, T65)
U9_gaaa(T40, T41, T20, T21, div1_out_gaaa(T43, s(T42), T20, T21)) → div1_out_gaaa(s(s(s(s(s(s(s(T40))))))), s(s(s(s(s(s(s(T41))))))), s(T20), T21)
U9_ggaa(T40, T41, T20, T21, div1_out_gaaa(T43, s(T42), T20, T21)) → div1_out_ggaa(s(s(s(s(s(s(s(T40))))))), s(s(s(s(s(s(s(T41))))))), s(T20), T21)
U6_ggaa(T39, T20, T21, div1_out_ggaa(T39, s(s(s(s(s(s(0)))))), T20, T21)) → div1_out_ggaa(s(s(s(s(s(s(T39)))))), s(s(s(s(s(s(0)))))), s(T20), T21)
U5_ggaa(T36, T20, T21, div1_out_ggaa(T36, s(s(s(s(s(0))))), T20, T21)) → div1_out_ggaa(s(s(s(s(s(T36))))), s(s(s(s(s(0))))), s(T20), T21)
U4_ggaa(T33, T20, T21, div1_out_ggaa(T33, s(s(s(s(0)))), T20, T21)) → div1_out_ggaa(s(s(s(s(T33)))), s(s(s(s(0)))), s(T20), T21)
U3_ggaa(T30, T20, T21, div1_out_ggaa(T30, s(s(s(0))), T20, T21)) → div1_out_ggaa(s(s(s(T30))), s(s(s(0))), s(T20), T21)
U2_ggaa(T27, T20, T21, div1_out_ggaa(T27, s(s(0)), T20, T21)) → div1_out_ggaa(s(s(T27)), s(s(0)), s(T20), T21)
U1_ggaa(T24, T20, T21, div1_out_ggaa(T24, s(0), T20, T21)) → div1_out_ggaa(s(T24), s(0), s(T20), T21)

(17) UsableRulesProof (EQUIVALENT transformation)

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

(18) Obligation:

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

MINUS61_IN_GGA(s(T45), s(T46), X104) → MINUS61_IN_GGA(T45, T46, X104)

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

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

(19) PiDPToQDPProof (SOUND transformation)

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

(20) Obligation:

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

MINUS61_IN_GGA(s(T45), s(T46)) → MINUS61_IN_GGA(T45, T46)

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

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

MINUS61_IN_GGA(s(T45), s(T46)) → MINUS61_IN_GGA(T45, T46)
The graph contains the following edges 1 > 1, 2 > 2

(22) TRUE

(23) Obligation:

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

DIV1_IN_GGAA(s(s(s(s(s(s(T39)))))), s(s(s(s(s(s(0)))))), s(T20), T21) → DIV1_IN_GGAA(T39, s(s(s(s(s(s(0)))))), T20, T21)

The TRS R consists of the following rules:

div1_in_ggaa(0, T8, 0, 0) → div1_out_ggaa(0, T8, 0, 0)
div1_in_ggaa(s(T24), s(0), s(T20), T21) → U1_ggaa(T24, T20, T21, div1_in_ggaa(T24, s(0), T20, T21))
div1_in_ggaa(s(s(T27)), s(s(0)), s(T20), T21) → U2_ggaa(T27, T20, T21, div1_in_ggaa(T27, s(s(0)), T20, T21))
div1_in_ggaa(s(s(s(T30))), s(s(s(0))), s(T20), T21) → U3_ggaa(T30, T20, T21, div1_in_ggaa(T30, s(s(s(0))), T20, T21))
div1_in_ggaa(s(s(s(s(T33)))), s(s(s(s(0)))), s(T20), T21) → U4_ggaa(T33, T20, T21, div1_in_ggaa(T33, s(s(s(s(0)))), T20, T21))
div1_in_ggaa(s(s(s(s(s(T36))))), s(s(s(s(s(0))))), s(T20), T21) → U5_ggaa(T36, T20, T21, div1_in_ggaa(T36, s(s(s(s(s(0))))), T20, T21))
div1_in_ggaa(s(s(s(s(s(s(T39)))))), s(s(s(s(s(s(0)))))), s(T20), T21) → U6_ggaa(T39, T20, T21, div1_in_ggaa(T39, s(s(s(s(s(s(0)))))), T20, T21))
div1_in_ggaa(s(s(s(s(s(s(s(T40))))))), s(s(s(s(s(s(s(T41))))))), s(T20), T21) → U7_ggaa(T40, T41, T20, T21, minus61_in_gga(T40, T41, X94))
minus61_in_gga(T44, 0, T44) → minus61_out_gga(T44, 0, T44)
minus61_in_gga(s(T45), s(T46), X104) → U10_gga(T45, T46, X104, minus61_in_gga(T45, T46, X104))
U10_gga(T45, T46, X104, minus61_out_gga(T45, T46, X104)) → minus61_out_gga(s(T45), s(T46), X104)
U7_ggaa(T40, T41, T20, T21, minus61_out_gga(T40, T41, X94)) → div1_out_ggaa(s(s(s(s(s(s(s(T40))))))), s(s(s(s(s(s(s(T41))))))), s(T20), T21)
div1_in_ggaa(s(s(s(s(s(s(s(T40))))))), s(s(s(s(s(s(s(T41))))))), s(T20), T21) → U8_ggaa(T40, T41, T20, T21, minus61_in_gga(T40, T41, T43))
U8_ggaa(T40, T41, T20, T21, minus61_out_gga(T40, T41, T43)) → U9_ggaa(T40, T41, T20, T21, div1_in_gaaa(T43, s(T42), T20, T21))
div1_in_gaaa(0, T8, 0, 0) → div1_out_gaaa(0, T8, 0, 0)
div1_in_gaaa(s(T24), s(0), s(T20), T21) → U1_gaaa(T24, T20, T21, div1_in_ggaa(T24, s(0), T20, T21))
div1_in_ggaa(s(s(s(s(s(s(T47)))))), s(s(s(s(s(s(T48)))))), T49, s(s(s(s(s(s(T47))))))) → div1_out_ggaa(s(s(s(s(s(s(T47)))))), s(s(s(s(s(s(T48)))))), T49, s(s(s(s(s(s(T47)))))))
div1_in_ggaa(s(s(s(s(s(T50))))), s(s(s(s(s(T51))))), T52, s(s(s(s(s(T50)))))) → div1_out_ggaa(s(s(s(s(s(T50))))), s(s(s(s(s(T51))))), T52, s(s(s(s(s(T50))))))
div1_in_ggaa(s(s(s(s(T53)))), s(s(s(s(T54)))), T55, s(s(s(s(T53))))) → div1_out_ggaa(s(s(s(s(T53)))), s(s(s(s(T54)))), T55, s(s(s(s(T53)))))
div1_in_ggaa(s(s(s(T56))), s(s(s(T57))), T58, s(s(s(T56)))) → div1_out_ggaa(s(s(s(T56))), s(s(s(T57))), T58, s(s(s(T56))))
div1_in_ggaa(s(s(T59)), s(s(T60)), T61, s(s(T59))) → div1_out_ggaa(s(s(T59)), s(s(T60)), T61, s(s(T59)))
div1_in_ggaa(s(T62), s(T63), T64, s(T62)) → div1_out_ggaa(s(T62), s(T63), T64, s(T62))
div1_in_ggaa(T65, T66, T67, T65) → div1_out_ggaa(T65, T66, T67, T65)
U1_gaaa(T24, T20, T21, div1_out_ggaa(T24, s(0), T20, T21)) → div1_out_gaaa(s(T24), s(0), s(T20), T21)
div1_in_gaaa(s(s(T27)), s(s(0)), s(T20), T21) → U2_gaaa(T27, T20, T21, div1_in_ggaa(T27, s(s(0)), T20, T21))
U2_gaaa(T27, T20, T21, div1_out_ggaa(T27, s(s(0)), T20, T21)) → div1_out_gaaa(s(s(T27)), s(s(0)), s(T20), T21)
div1_in_gaaa(s(s(s(T30))), s(s(s(0))), s(T20), T21) → U3_gaaa(T30, T20, T21, div1_in_ggaa(T30, s(s(s(0))), T20, T21))
U3_gaaa(T30, T20, T21, div1_out_ggaa(T30, s(s(s(0))), T20, T21)) → div1_out_gaaa(s(s(s(T30))), s(s(s(0))), s(T20), T21)
div1_in_gaaa(s(s(s(s(T33)))), s(s(s(s(0)))), s(T20), T21) → U4_gaaa(T33, T20, T21, div1_in_ggaa(T33, s(s(s(s(0)))), T20, T21))
U4_gaaa(T33, T20, T21, div1_out_ggaa(T33, s(s(s(s(0)))), T20, T21)) → div1_out_gaaa(s(s(s(s(T33)))), s(s(s(s(0)))), s(T20), T21)
div1_in_gaaa(s(s(s(s(s(T36))))), s(s(s(s(s(0))))), s(T20), T21) → U5_gaaa(T36, T20, T21, div1_in_ggaa(T36, s(s(s(s(s(0))))), T20, T21))
U5_gaaa(T36, T20, T21, div1_out_ggaa(T36, s(s(s(s(s(0))))), T20, T21)) → div1_out_gaaa(s(s(s(s(s(T36))))), s(s(s(s(s(0))))), s(T20), T21)
div1_in_gaaa(s(s(s(s(s(s(T39)))))), s(s(s(s(s(s(0)))))), s(T20), T21) → U6_gaaa(T39, T20, T21, div1_in_ggaa(T39, s(s(s(s(s(s(0)))))), T20, T21))
U6_gaaa(T39, T20, T21, div1_out_ggaa(T39, s(s(s(s(s(s(0)))))), T20, T21)) → div1_out_gaaa(s(s(s(s(s(s(T39)))))), s(s(s(s(s(s(0)))))), s(T20), T21)
div1_in_gaaa(s(s(s(s(s(s(s(T40))))))), s(s(s(s(s(s(s(T41))))))), s(T20), T21) → U7_gaaa(T40, T41, T20, T21, minus61_in_gaa(T40, T41, X94))
minus61_in_gaa(T44, 0, T44) → minus61_out_gaa(T44, 0, T44)
minus61_in_gaa(s(T45), s(T46), X104) → U10_gaa(T45, T46, X104, minus61_in_gaa(T45, T46, X104))
U10_gaa(T45, T46, X104, minus61_out_gaa(T45, T46, X104)) → minus61_out_gaa(s(T45), s(T46), X104)
U7_gaaa(T40, T41, T20, T21, minus61_out_gaa(T40, T41, X94)) → div1_out_gaaa(s(s(s(s(s(s(s(T40))))))), s(s(s(s(s(s(s(T41))))))), s(T20), T21)
div1_in_gaaa(s(s(s(s(s(s(s(T40))))))), s(s(s(s(s(s(s(T41))))))), s(T20), T21) → U8_gaaa(T40, T41, T20, T21, minus61_in_gaa(T40, T41, T43))
U8_gaaa(T40, T41, T20, T21, minus61_out_gaa(T40, T41, T43)) → U9_gaaa(T40, T41, T20, T21, div1_in_gaaa(T43, s(T42), T20, T21))
div1_in_gaaa(s(s(s(s(s(s(T47)))))), s(s(s(s(s(s(T48)))))), T49, s(s(s(s(s(s(T47))))))) → div1_out_gaaa(s(s(s(s(s(s(T47)))))), s(s(s(s(s(s(T48)))))), T49, s(s(s(s(s(s(T47)))))))
div1_in_gaaa(s(s(s(s(s(T50))))), s(s(s(s(s(T51))))), T52, s(s(s(s(s(T50)))))) → div1_out_gaaa(s(s(s(s(s(T50))))), s(s(s(s(s(T51))))), T52, s(s(s(s(s(T50))))))
div1_in_gaaa(s(s(s(s(T53)))), s(s(s(s(T54)))), T55, s(s(s(s(T53))))) → div1_out_gaaa(s(s(s(s(T53)))), s(s(s(s(T54)))), T55, s(s(s(s(T53)))))
div1_in_gaaa(s(s(s(T56))), s(s(s(T57))), T58, s(s(s(T56)))) → div1_out_gaaa(s(s(s(T56))), s(s(s(T57))), T58, s(s(s(T56))))
div1_in_gaaa(s(s(T59)), s(s(T60)), T61, s(s(T59))) → div1_out_gaaa(s(s(T59)), s(s(T60)), T61, s(s(T59)))
div1_in_gaaa(s(T62), s(T63), T64, s(T62)) → div1_out_gaaa(s(T62), s(T63), T64, s(T62))
div1_in_gaaa(T65, T66, T67, T65) → div1_out_gaaa(T65, T66, T67, T65)
U9_gaaa(T40, T41, T20, T21, div1_out_gaaa(T43, s(T42), T20, T21)) → div1_out_gaaa(s(s(s(s(s(s(s(T40))))))), s(s(s(s(s(s(s(T41))))))), s(T20), T21)
U9_ggaa(T40, T41, T20, T21, div1_out_gaaa(T43, s(T42), T20, T21)) → div1_out_ggaa(s(s(s(s(s(s(s(T40))))))), s(s(s(s(s(s(s(T41))))))), s(T20), T21)
U6_ggaa(T39, T20, T21, div1_out_ggaa(T39, s(s(s(s(s(s(0)))))), T20, T21)) → div1_out_ggaa(s(s(s(s(s(s(T39)))))), s(s(s(s(s(s(0)))))), s(T20), T21)
U5_ggaa(T36, T20, T21, div1_out_ggaa(T36, s(s(s(s(s(0))))), T20, T21)) → div1_out_ggaa(s(s(s(s(s(T36))))), s(s(s(s(s(0))))), s(T20), T21)
U4_ggaa(T33, T20, T21, div1_out_ggaa(T33, s(s(s(s(0)))), T20, T21)) → div1_out_ggaa(s(s(s(s(T33)))), s(s(s(s(0)))), s(T20), T21)
U3_ggaa(T30, T20, T21, div1_out_ggaa(T30, s(s(s(0))), T20, T21)) → div1_out_ggaa(s(s(s(T30))), s(s(s(0))), s(T20), T21)
U2_ggaa(T27, T20, T21, div1_out_ggaa(T27, s(s(0)), T20, T21)) → div1_out_ggaa(s(s(T27)), s(s(0)), s(T20), T21)
U1_ggaa(T24, T20, T21, div1_out_ggaa(T24, s(0), T20, T21)) → div1_out_ggaa(s(T24), s(0), s(T20), T21)

(24) UsableRulesProof (EQUIVALENT transformation)

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

(25) Obligation:

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

DIV1_IN_GGAA(s(s(s(s(s(s(T39)))))), s(s(s(s(s(s(0)))))), s(T20), T21) → DIV1_IN_GGAA(T39, s(s(s(s(s(s(0)))))), T20, T21)

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

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

(26) PiDPToQDPProof (SOUND transformation)

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

(27) Obligation:

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

DIV1_IN_GGAA(s(s(s(s(s(s(T39)))))), s(s(s(s(s(s(0))))))) → DIV1_IN_GGAA(T39, s(s(s(s(s(s(0)))))))

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

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

DIV1_IN_GGAA(s(s(s(s(s(s(T39)))))), s(s(s(s(s(s(0))))))) → DIV1_IN_GGAA(T39, s(s(s(s(s(s(0)))))))
The graph contains the following edges 1 > 1, 2 >= 2

(29) TRUE

(30) Obligation:

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

DIV1_IN_GGAA(s(s(s(s(s(T36))))), s(s(s(s(s(0))))), s(T20), T21) → DIV1_IN_GGAA(T36, s(s(s(s(s(0))))), T20, T21)

The TRS R consists of the following rules:

div1_in_ggaa(0, T8, 0, 0) → div1_out_ggaa(0, T8, 0, 0)
div1_in_ggaa(s(T24), s(0), s(T20), T21) → U1_ggaa(T24, T20, T21, div1_in_ggaa(T24, s(0), T20, T21))
div1_in_ggaa(s(s(T27)), s(s(0)), s(T20), T21) → U2_ggaa(T27, T20, T21, div1_in_ggaa(T27, s(s(0)), T20, T21))
div1_in_ggaa(s(s(s(T30))), s(s(s(0))), s(T20), T21) → U3_ggaa(T30, T20, T21, div1_in_ggaa(T30, s(s(s(0))), T20, T21))
div1_in_ggaa(s(s(s(s(T33)))), s(s(s(s(0)))), s(T20), T21) → U4_ggaa(T33, T20, T21, div1_in_ggaa(T33, s(s(s(s(0)))), T20, T21))
div1_in_ggaa(s(s(s(s(s(T36))))), s(s(s(s(s(0))))), s(T20), T21) → U5_ggaa(T36, T20, T21, div1_in_ggaa(T36, s(s(s(s(s(0))))), T20, T21))
div1_in_ggaa(s(s(s(s(s(s(T39)))))), s(s(s(s(s(s(0)))))), s(T20), T21) → U6_ggaa(T39, T20, T21, div1_in_ggaa(T39, s(s(s(s(s(s(0)))))), T20, T21))
div1_in_ggaa(s(s(s(s(s(s(s(T40))))))), s(s(s(s(s(s(s(T41))))))), s(T20), T21) → U7_ggaa(T40, T41, T20, T21, minus61_in_gga(T40, T41, X94))
minus61_in_gga(T44, 0, T44) → minus61_out_gga(T44, 0, T44)
minus61_in_gga(s(T45), s(T46), X104) → U10_gga(T45, T46, X104, minus61_in_gga(T45, T46, X104))
U10_gga(T45, T46, X104, minus61_out_gga(T45, T46, X104)) → minus61_out_gga(s(T45), s(T46), X104)
U7_ggaa(T40, T41, T20, T21, minus61_out_gga(T40, T41, X94)) → div1_out_ggaa(s(s(s(s(s(s(s(T40))))))), s(s(s(s(s(s(s(T41))))))), s(T20), T21)
div1_in_ggaa(s(s(s(s(s(s(s(T40))))))), s(s(s(s(s(s(s(T41))))))), s(T20), T21) → U8_ggaa(T40, T41, T20, T21, minus61_in_gga(T40, T41, T43))
U8_ggaa(T40, T41, T20, T21, minus61_out_gga(T40, T41, T43)) → U9_ggaa(T40, T41, T20, T21, div1_in_gaaa(T43, s(T42), T20, T21))
div1_in_gaaa(0, T8, 0, 0) → div1_out_gaaa(0, T8, 0, 0)
div1_in_gaaa(s(T24), s(0), s(T20), T21) → U1_gaaa(T24, T20, T21, div1_in_ggaa(T24, s(0), T20, T21))
div1_in_ggaa(s(s(s(s(s(s(T47)))))), s(s(s(s(s(s(T48)))))), T49, s(s(s(s(s(s(T47))))))) → div1_out_ggaa(s(s(s(s(s(s(T47)))))), s(s(s(s(s(s(T48)))))), T49, s(s(s(s(s(s(T47)))))))
div1_in_ggaa(s(s(s(s(s(T50))))), s(s(s(s(s(T51))))), T52, s(s(s(s(s(T50)))))) → div1_out_ggaa(s(s(s(s(s(T50))))), s(s(s(s(s(T51))))), T52, s(s(s(s(s(T50))))))
div1_in_ggaa(s(s(s(s(T53)))), s(s(s(s(T54)))), T55, s(s(s(s(T53))))) → div1_out_ggaa(s(s(s(s(T53)))), s(s(s(s(T54)))), T55, s(s(s(s(T53)))))
div1_in_ggaa(s(s(s(T56))), s(s(s(T57))), T58, s(s(s(T56)))) → div1_out_ggaa(s(s(s(T56))), s(s(s(T57))), T58, s(s(s(T56))))
div1_in_ggaa(s(s(T59)), s(s(T60)), T61, s(s(T59))) → div1_out_ggaa(s(s(T59)), s(s(T60)), T61, s(s(T59)))
div1_in_ggaa(s(T62), s(T63), T64, s(T62)) → div1_out_ggaa(s(T62), s(T63), T64, s(T62))
div1_in_ggaa(T65, T66, T67, T65) → div1_out_ggaa(T65, T66, T67, T65)
U1_gaaa(T24, T20, T21, div1_out_ggaa(T24, s(0), T20, T21)) → div1_out_gaaa(s(T24), s(0), s(T20), T21)
div1_in_gaaa(s(s(T27)), s(s(0)), s(T20), T21) → U2_gaaa(T27, T20, T21, div1_in_ggaa(T27, s(s(0)), T20, T21))
U2_gaaa(T27, T20, T21, div1_out_ggaa(T27, s(s(0)), T20, T21)) → div1_out_gaaa(s(s(T27)), s(s(0)), s(T20), T21)
div1_in_gaaa(s(s(s(T30))), s(s(s(0))), s(T20), T21) → U3_gaaa(T30, T20, T21, div1_in_ggaa(T30, s(s(s(0))), T20, T21))
U3_gaaa(T30, T20, T21, div1_out_ggaa(T30, s(s(s(0))), T20, T21)) → div1_out_gaaa(s(s(s(T30))), s(s(s(0))), s(T20), T21)
div1_in_gaaa(s(s(s(s(T33)))), s(s(s(s(0)))), s(T20), T21) → U4_gaaa(T33, T20, T21, div1_in_ggaa(T33, s(s(s(s(0)))), T20, T21))
U4_gaaa(T33, T20, T21, div1_out_ggaa(T33, s(s(s(s(0)))), T20, T21)) → div1_out_gaaa(s(s(s(s(T33)))), s(s(s(s(0)))), s(T20), T21)
div1_in_gaaa(s(s(s(s(s(T36))))), s(s(s(s(s(0))))), s(T20), T21) → U5_gaaa(T36, T20, T21, div1_in_ggaa(T36, s(s(s(s(s(0))))), T20, T21))
U5_gaaa(T36, T20, T21, div1_out_ggaa(T36, s(s(s(s(s(0))))), T20, T21)) → div1_out_gaaa(s(s(s(s(s(T36))))), s(s(s(s(s(0))))), s(T20), T21)
div1_in_gaaa(s(s(s(s(s(s(T39)))))), s(s(s(s(s(s(0)))))), s(T20), T21) → U6_gaaa(T39, T20, T21, div1_in_ggaa(T39, s(s(s(s(s(s(0)))))), T20, T21))
U6_gaaa(T39, T20, T21, div1_out_ggaa(T39, s(s(s(s(s(s(0)))))), T20, T21)) → div1_out_gaaa(s(s(s(s(s(s(T39)))))), s(s(s(s(s(s(0)))))), s(T20), T21)
div1_in_gaaa(s(s(s(s(s(s(s(T40))))))), s(s(s(s(s(s(s(T41))))))), s(T20), T21) → U7_gaaa(T40, T41, T20, T21, minus61_in_gaa(T40, T41, X94))
minus61_in_gaa(T44, 0, T44) → minus61_out_gaa(T44, 0, T44)
minus61_in_gaa(s(T45), s(T46), X104) → U10_gaa(T45, T46, X104, minus61_in_gaa(T45, T46, X104))
U10_gaa(T45, T46, X104, minus61_out_gaa(T45, T46, X104)) → minus61_out_gaa(s(T45), s(T46), X104)
U7_gaaa(T40, T41, T20, T21, minus61_out_gaa(T40, T41, X94)) → div1_out_gaaa(s(s(s(s(s(s(s(T40))))))), s(s(s(s(s(s(s(T41))))))), s(T20), T21)
div1_in_gaaa(s(s(s(s(s(s(s(T40))))))), s(s(s(s(s(s(s(T41))))))), s(T20), T21) → U8_gaaa(T40, T41, T20, T21, minus61_in_gaa(T40, T41, T43))
U8_gaaa(T40, T41, T20, T21, minus61_out_gaa(T40, T41, T43)) → U9_gaaa(T40, T41, T20, T21, div1_in_gaaa(T43, s(T42), T20, T21))
div1_in_gaaa(s(s(s(s(s(s(T47)))))), s(s(s(s(s(s(T48)))))), T49, s(s(s(s(s(s(T47))))))) → div1_out_gaaa(s(s(s(s(s(s(T47)))))), s(s(s(s(s(s(T48)))))), T49, s(s(s(s(s(s(T47)))))))
div1_in_gaaa(s(s(s(s(s(T50))))), s(s(s(s(s(T51))))), T52, s(s(s(s(s(T50)))))) → div1_out_gaaa(s(s(s(s(s(T50))))), s(s(s(s(s(T51))))), T52, s(s(s(s(s(T50))))))
div1_in_gaaa(s(s(s(s(T53)))), s(s(s(s(T54)))), T55, s(s(s(s(T53))))) → div1_out_gaaa(s(s(s(s(T53)))), s(s(s(s(T54)))), T55, s(s(s(s(T53)))))
div1_in_gaaa(s(s(s(T56))), s(s(s(T57))), T58, s(s(s(T56)))) → div1_out_gaaa(s(s(s(T56))), s(s(s(T57))), T58, s(s(s(T56))))
div1_in_gaaa(s(s(T59)), s(s(T60)), T61, s(s(T59))) → div1_out_gaaa(s(s(T59)), s(s(T60)), T61, s(s(T59)))
div1_in_gaaa(s(T62), s(T63), T64, s(T62)) → div1_out_gaaa(s(T62), s(T63), T64, s(T62))
div1_in_gaaa(T65, T66, T67, T65) → div1_out_gaaa(T65, T66, T67, T65)
U9_gaaa(T40, T41, T20, T21, div1_out_gaaa(T43, s(T42), T20, T21)) → div1_out_gaaa(s(s(s(s(s(s(s(T40))))))), s(s(s(s(s(s(s(T41))))))), s(T20), T21)
U9_ggaa(T40, T41, T20, T21, div1_out_gaaa(T43, s(T42), T20, T21)) → div1_out_ggaa(s(s(s(s(s(s(s(T40))))))), s(s(s(s(s(s(s(T41))))))), s(T20), T21)
U6_ggaa(T39, T20, T21, div1_out_ggaa(T39, s(s(s(s(s(s(0)))))), T20, T21)) → div1_out_ggaa(s(s(s(s(s(s(T39)))))), s(s(s(s(s(s(0)))))), s(T20), T21)
U5_ggaa(T36, T20, T21, div1_out_ggaa(T36, s(s(s(s(s(0))))), T20, T21)) → div1_out_ggaa(s(s(s(s(s(T36))))), s(s(s(s(s(0))))), s(T20), T21)
U4_ggaa(T33, T20, T21, div1_out_ggaa(T33, s(s(s(s(0)))), T20, T21)) → div1_out_ggaa(s(s(s(s(T33)))), s(s(s(s(0)))), s(T20), T21)
U3_ggaa(T30, T20, T21, div1_out_ggaa(T30, s(s(s(0))), T20, T21)) → div1_out_ggaa(s(s(s(T30))), s(s(s(0))), s(T20), T21)
U2_ggaa(T27, T20, T21, div1_out_ggaa(T27, s(s(0)), T20, T21)) → div1_out_ggaa(s(s(T27)), s(s(0)), s(T20), T21)
U1_ggaa(T24, T20, T21, div1_out_ggaa(T24, s(0), T20, T21)) → div1_out_ggaa(s(T24), s(0), s(T20), T21)

(31) UsableRulesProof (EQUIVALENT transformation)

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

(32) Obligation:

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

DIV1_IN_GGAA(s(s(s(s(s(T36))))), s(s(s(s(s(0))))), s(T20), T21) → DIV1_IN_GGAA(T36, s(s(s(s(s(0))))), T20, T21)

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

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

(33) PiDPToQDPProof (SOUND transformation)

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

(34) Obligation:

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

DIV1_IN_GGAA(s(s(s(s(s(T36))))), s(s(s(s(s(0)))))) → DIV1_IN_GGAA(T36, s(s(s(s(s(0))))))

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

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

DIV1_IN_GGAA(s(s(s(s(s(T36))))), s(s(s(s(s(0)))))) → DIV1_IN_GGAA(T36, s(s(s(s(s(0))))))
The graph contains the following edges 1 > 1, 2 >= 2

(36) TRUE

(37) Obligation:

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

DIV1_IN_GGAA(s(s(s(s(T33)))), s(s(s(s(0)))), s(T20), T21) → DIV1_IN_GGAA(T33, s(s(s(s(0)))), T20, T21)

The TRS R consists of the following rules:

div1_in_ggaa(0, T8, 0, 0) → div1_out_ggaa(0, T8, 0, 0)
div1_in_ggaa(s(T24), s(0), s(T20), T21) → U1_ggaa(T24, T20, T21, div1_in_ggaa(T24, s(0), T20, T21))
div1_in_ggaa(s(s(T27)), s(s(0)), s(T20), T21) → U2_ggaa(T27, T20, T21, div1_in_ggaa(T27, s(s(0)), T20, T21))
div1_in_ggaa(s(s(s(T30))), s(s(s(0))), s(T20), T21) → U3_ggaa(T30, T20, T21, div1_in_ggaa(T30, s(s(s(0))), T20, T21))
div1_in_ggaa(s(s(s(s(T33)))), s(s(s(s(0)))), s(T20), T21) → U4_ggaa(T33, T20, T21, div1_in_ggaa(T33, s(s(s(s(0)))), T20, T21))
div1_in_ggaa(s(s(s(s(s(T36))))), s(s(s(s(s(0))))), s(T20), T21) → U5_ggaa(T36, T20, T21, div1_in_ggaa(T36, s(s(s(s(s(0))))), T20, T21))
div1_in_ggaa(s(s(s(s(s(s(T39)))))), s(s(s(s(s(s(0)))))), s(T20), T21) → U6_ggaa(T39, T20, T21, div1_in_ggaa(T39, s(s(s(s(s(s(0)))))), T20, T21))
div1_in_ggaa(s(s(s(s(s(s(s(T40))))))), s(s(s(s(s(s(s(T41))))))), s(T20), T21) → U7_ggaa(T40, T41, T20, T21, minus61_in_gga(T40, T41, X94))
minus61_in_gga(T44, 0, T44) → minus61_out_gga(T44, 0, T44)
minus61_in_gga(s(T45), s(T46), X104) → U10_gga(T45, T46, X104, minus61_in_gga(T45, T46, X104))
U10_gga(T45, T46, X104, minus61_out_gga(T45, T46, X104)) → minus61_out_gga(s(T45), s(T46), X104)
U7_ggaa(T40, T41, T20, T21, minus61_out_gga(T40, T41, X94)) → div1_out_ggaa(s(s(s(s(s(s(s(T40))))))), s(s(s(s(s(s(s(T41))))))), s(T20), T21)
div1_in_ggaa(s(s(s(s(s(s(s(T40))))))), s(s(s(s(s(s(s(T41))))))), s(T20), T21) → U8_ggaa(T40, T41, T20, T21, minus61_in_gga(T40, T41, T43))
U8_ggaa(T40, T41, T20, T21, minus61_out_gga(T40, T41, T43)) → U9_ggaa(T40, T41, T20, T21, div1_in_gaaa(T43, s(T42), T20, T21))
div1_in_gaaa(0, T8, 0, 0) → div1_out_gaaa(0, T8, 0, 0)
div1_in_gaaa(s(T24), s(0), s(T20), T21) → U1_gaaa(T24, T20, T21, div1_in_ggaa(T24, s(0), T20, T21))
div1_in_ggaa(s(s(s(s(s(s(T47)))))), s(s(s(s(s(s(T48)))))), T49, s(s(s(s(s(s(T47))))))) → div1_out_ggaa(s(s(s(s(s(s(T47)))))), s(s(s(s(s(s(T48)))))), T49, s(s(s(s(s(s(T47)))))))
div1_in_ggaa(s(s(s(s(s(T50))))), s(s(s(s(s(T51))))), T52, s(s(s(s(s(T50)))))) → div1_out_ggaa(s(s(s(s(s(T50))))), s(s(s(s(s(T51))))), T52, s(s(s(s(s(T50))))))
div1_in_ggaa(s(s(s(s(T53)))), s(s(s(s(T54)))), T55, s(s(s(s(T53))))) → div1_out_ggaa(s(s(s(s(T53)))), s(s(s(s(T54)))), T55, s(s(s(s(T53)))))
div1_in_ggaa(s(s(s(T56))), s(s(s(T57))), T58, s(s(s(T56)))) → div1_out_ggaa(s(s(s(T56))), s(s(s(T57))), T58, s(s(s(T56))))
div1_in_ggaa(s(s(T59)), s(s(T60)), T61, s(s(T59))) → div1_out_ggaa(s(s(T59)), s(s(T60)), T61, s(s(T59)))
div1_in_ggaa(s(T62), s(T63), T64, s(T62)) → div1_out_ggaa(s(T62), s(T63), T64, s(T62))
div1_in_ggaa(T65, T66, T67, T65) → div1_out_ggaa(T65, T66, T67, T65)
U1_gaaa(T24, T20, T21, div1_out_ggaa(T24, s(0), T20, T21)) → div1_out_gaaa(s(T24), s(0), s(T20), T21)
div1_in_gaaa(s(s(T27)), s(s(0)), s(T20), T21) → U2_gaaa(T27, T20, T21, div1_in_ggaa(T27, s(s(0)), T20, T21))
U2_gaaa(T27, T20, T21, div1_out_ggaa(T27, s(s(0)), T20, T21)) → div1_out_gaaa(s(s(T27)), s(s(0)), s(T20), T21)
div1_in_gaaa(s(s(s(T30))), s(s(s(0))), s(T20), T21) → U3_gaaa(T30, T20, T21, div1_in_ggaa(T30, s(s(s(0))), T20, T21))
U3_gaaa(T30, T20, T21, div1_out_ggaa(T30, s(s(s(0))), T20, T21)) → div1_out_gaaa(s(s(s(T30))), s(s(s(0))), s(T20), T21)
div1_in_gaaa(s(s(s(s(T33)))), s(s(s(s(0)))), s(T20), T21) → U4_gaaa(T33, T20, T21, div1_in_ggaa(T33, s(s(s(s(0)))), T20, T21))
U4_gaaa(T33, T20, T21, div1_out_ggaa(T33, s(s(s(s(0)))), T20, T21)) → div1_out_gaaa(s(s(s(s(T33)))), s(s(s(s(0)))), s(T20), T21)
div1_in_gaaa(s(s(s(s(s(T36))))), s(s(s(s(s(0))))), s(T20), T21) → U5_gaaa(T36, T20, T21, div1_in_ggaa(T36, s(s(s(s(s(0))))), T20, T21))
U5_gaaa(T36, T20, T21, div1_out_ggaa(T36, s(s(s(s(s(0))))), T20, T21)) → div1_out_gaaa(s(s(s(s(s(T36))))), s(s(s(s(s(0))))), s(T20), T21)
div1_in_gaaa(s(s(s(s(s(s(T39)))))), s(s(s(s(s(s(0)))))), s(T20), T21) → U6_gaaa(T39, T20, T21, div1_in_ggaa(T39, s(s(s(s(s(s(0)))))), T20, T21))
U6_gaaa(T39, T20, T21, div1_out_ggaa(T39, s(s(s(s(s(s(0)))))), T20, T21)) → div1_out_gaaa(s(s(s(s(s(s(T39)))))), s(s(s(s(s(s(0)))))), s(T20), T21)
div1_in_gaaa(s(s(s(s(s(s(s(T40))))))), s(s(s(s(s(s(s(T41))))))), s(T20), T21) → U7_gaaa(T40, T41, T20, T21, minus61_in_gaa(T40, T41, X94))
minus61_in_gaa(T44, 0, T44) → minus61_out_gaa(T44, 0, T44)
minus61_in_gaa(s(T45), s(T46), X104) → U10_gaa(T45, T46, X104, minus61_in_gaa(T45, T46, X104))
U10_gaa(T45, T46, X104, minus61_out_gaa(T45, T46, X104)) → minus61_out_gaa(s(T45), s(T46), X104)
U7_gaaa(T40, T41, T20, T21, minus61_out_gaa(T40, T41, X94)) → div1_out_gaaa(s(s(s(s(s(s(s(T40))))))), s(s(s(s(s(s(s(T41))))))), s(T20), T21)
div1_in_gaaa(s(s(s(s(s(s(s(T40))))))), s(s(s(s(s(s(s(T41))))))), s(T20), T21) → U8_gaaa(T40, T41, T20, T21, minus61_in_gaa(T40, T41, T43))
U8_gaaa(T40, T41, T20, T21, minus61_out_gaa(T40, T41, T43)) → U9_gaaa(T40, T41, T20, T21, div1_in_gaaa(T43, s(T42), T20, T21))
div1_in_gaaa(s(s(s(s(s(s(T47)))))), s(s(s(s(s(s(T48)))))), T49, s(s(s(s(s(s(T47))))))) → div1_out_gaaa(s(s(s(s(s(s(T47)))))), s(s(s(s(s(s(T48)))))), T49, s(s(s(s(s(s(T47)))))))
div1_in_gaaa(s(s(s(s(s(T50))))), s(s(s(s(s(T51))))), T52, s(s(s(s(s(T50)))))) → div1_out_gaaa(s(s(s(s(s(T50))))), s(s(s(s(s(T51))))), T52, s(s(s(s(s(T50))))))
div1_in_gaaa(s(s(s(s(T53)))), s(s(s(s(T54)))), T55, s(s(s(s(T53))))) → div1_out_gaaa(s(s(s(s(T53)))), s(s(s(s(T54)))), T55, s(s(s(s(T53)))))
div1_in_gaaa(s(s(s(T56))), s(s(s(T57))), T58, s(s(s(T56)))) → div1_out_gaaa(s(s(s(T56))), s(s(s(T57))), T58, s(s(s(T56))))
div1_in_gaaa(s(s(T59)), s(s(T60)), T61, s(s(T59))) → div1_out_gaaa(s(s(T59)), s(s(T60)), T61, s(s(T59)))
div1_in_gaaa(s(T62), s(T63), T64, s(T62)) → div1_out_gaaa(s(T62), s(T63), T64, s(T62))
div1_in_gaaa(T65, T66, T67, T65) → div1_out_gaaa(T65, T66, T67, T65)
U9_gaaa(T40, T41, T20, T21, div1_out_gaaa(T43, s(T42), T20, T21)) → div1_out_gaaa(s(s(s(s(s(s(s(T40))))))), s(s(s(s(s(s(s(T41))))))), s(T20), T21)
U9_ggaa(T40, T41, T20, T21, div1_out_gaaa(T43, s(T42), T20, T21)) → div1_out_ggaa(s(s(s(s(s(s(s(T40))))))), s(s(s(s(s(s(s(T41))))))), s(T20), T21)
U6_ggaa(T39, T20, T21, div1_out_ggaa(T39, s(s(s(s(s(s(0)))))), T20, T21)) → div1_out_ggaa(s(s(s(s(s(s(T39)))))), s(s(s(s(s(s(0)))))), s(T20), T21)
U5_ggaa(T36, T20, T21, div1_out_ggaa(T36, s(s(s(s(s(0))))), T20, T21)) → div1_out_ggaa(s(s(s(s(s(T36))))), s(s(s(s(s(0))))), s(T20), T21)
U4_ggaa(T33, T20, T21, div1_out_ggaa(T33, s(s(s(s(0)))), T20, T21)) → div1_out_ggaa(s(s(s(s(T33)))), s(s(s(s(0)))), s(T20), T21)
U3_ggaa(T30, T20, T21, div1_out_ggaa(T30, s(s(s(0))), T20, T21)) → div1_out_ggaa(s(s(s(T30))), s(s(s(0))), s(T20), T21)
U2_ggaa(T27, T20, T21, div1_out_ggaa(T27, s(s(0)), T20, T21)) → div1_out_ggaa(s(s(T27)), s(s(0)), s(T20), T21)
U1_ggaa(T24, T20, T21, div1_out_ggaa(T24, s(0), T20, T21)) → div1_out_ggaa(s(T24), s(0), s(T20), T21)

(38) UsableRulesProof (EQUIVALENT transformation)

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

(39) Obligation:

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

DIV1_IN_GGAA(s(s(s(s(T33)))), s(s(s(s(0)))), s(T20), T21) → DIV1_IN_GGAA(T33, s(s(s(s(0)))), T20, T21)

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

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

(40) PiDPToQDPProof (SOUND transformation)

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

(41) Obligation:

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

DIV1_IN_GGAA(s(s(s(s(T33)))), s(s(s(s(0))))) → DIV1_IN_GGAA(T33, s(s(s(s(0)))))

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

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

DIV1_IN_GGAA(s(s(s(s(T33)))), s(s(s(s(0))))) → DIV1_IN_GGAA(T33, s(s(s(s(0)))))
The graph contains the following edges 1 > 1, 2 >= 2

(43) TRUE

(44) Obligation:

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

DIV1_IN_GGAA(s(s(s(T30))), s(s(s(0))), s(T20), T21) → DIV1_IN_GGAA(T30, s(s(s(0))), T20, T21)

The TRS R consists of the following rules:

div1_in_ggaa(0, T8, 0, 0) → div1_out_ggaa(0, T8, 0, 0)
div1_in_ggaa(s(T24), s(0), s(T20), T21) → U1_ggaa(T24, T20, T21, div1_in_ggaa(T24, s(0), T20, T21))
div1_in_ggaa(s(s(T27)), s(s(0)), s(T20), T21) → U2_ggaa(T27, T20, T21, div1_in_ggaa(T27, s(s(0)), T20, T21))
div1_in_ggaa(s(s(s(T30))), s(s(s(0))), s(T20), T21) → U3_ggaa(T30, T20, T21, div1_in_ggaa(T30, s(s(s(0))), T20, T21))
div1_in_ggaa(s(s(s(s(T33)))), s(s(s(s(0)))), s(T20), T21) → U4_ggaa(T33, T20, T21, div1_in_ggaa(T33, s(s(s(s(0)))), T20, T21))
div1_in_ggaa(s(s(s(s(s(T36))))), s(s(s(s(s(0))))), s(T20), T21) → U5_ggaa(T36, T20, T21, div1_in_ggaa(T36, s(s(s(s(s(0))))), T20, T21))
div1_in_ggaa(s(s(s(s(s(s(T39)))))), s(s(s(s(s(s(0)))))), s(T20), T21) → U6_ggaa(T39, T20, T21, div1_in_ggaa(T39, s(s(s(s(s(s(0)))))), T20, T21))
div1_in_ggaa(s(s(s(s(s(s(s(T40))))))), s(s(s(s(s(s(s(T41))))))), s(T20), T21) → U7_ggaa(T40, T41, T20, T21, minus61_in_gga(T40, T41, X94))
minus61_in_gga(T44, 0, T44) → minus61_out_gga(T44, 0, T44)
minus61_in_gga(s(T45), s(T46), X104) → U10_gga(T45, T46, X104, minus61_in_gga(T45, T46, X104))
U10_gga(T45, T46, X104, minus61_out_gga(T45, T46, X104)) → minus61_out_gga(s(T45), s(T46), X104)
U7_ggaa(T40, T41, T20, T21, minus61_out_gga(T40, T41, X94)) → div1_out_ggaa(s(s(s(s(s(s(s(T40))))))), s(s(s(s(s(s(s(T41))))))), s(T20), T21)
div1_in_ggaa(s(s(s(s(s(s(s(T40))))))), s(s(s(s(s(s(s(T41))))))), s(T20), T21) → U8_ggaa(T40, T41, T20, T21, minus61_in_gga(T40, T41, T43))
U8_ggaa(T40, T41, T20, T21, minus61_out_gga(T40, T41, T43)) → U9_ggaa(T40, T41, T20, T21, div1_in_gaaa(T43, s(T42), T20, T21))
div1_in_gaaa(0, T8, 0, 0) → div1_out_gaaa(0, T8, 0, 0)
div1_in_gaaa(s(T24), s(0), s(T20), T21) → U1_gaaa(T24, T20, T21, div1_in_ggaa(T24, s(0), T20, T21))
div1_in_ggaa(s(s(s(s(s(s(T47)))))), s(s(s(s(s(s(T48)))))), T49, s(s(s(s(s(s(T47))))))) → div1_out_ggaa(s(s(s(s(s(s(T47)))))), s(s(s(s(s(s(T48)))))), T49, s(s(s(s(s(s(T47)))))))
div1_in_ggaa(s(s(s(s(s(T50))))), s(s(s(s(s(T51))))), T52, s(s(s(s(s(T50)))))) → div1_out_ggaa(s(s(s(s(s(T50))))), s(s(s(s(s(T51))))), T52, s(s(s(s(s(T50))))))
div1_in_ggaa(s(s(s(s(T53)))), s(s(s(s(T54)))), T55, s(s(s(s(T53))))) → div1_out_ggaa(s(s(s(s(T53)))), s(s(s(s(T54)))), T55, s(s(s(s(T53)))))
div1_in_ggaa(s(s(s(T56))), s(s(s(T57))), T58, s(s(s(T56)))) → div1_out_ggaa(s(s(s(T56))), s(s(s(T57))), T58, s(s(s(T56))))
div1_in_ggaa(s(s(T59)), s(s(T60)), T61, s(s(T59))) → div1_out_ggaa(s(s(T59)), s(s(T60)), T61, s(s(T59)))
div1_in_ggaa(s(T62), s(T63), T64, s(T62)) → div1_out_ggaa(s(T62), s(T63), T64, s(T62))
div1_in_ggaa(T65, T66, T67, T65) → div1_out_ggaa(T65, T66, T67, T65)
U1_gaaa(T24, T20, T21, div1_out_ggaa(T24, s(0), T20, T21)) → div1_out_gaaa(s(T24), s(0), s(T20), T21)
div1_in_gaaa(s(s(T27)), s(s(0)), s(T20), T21) → U2_gaaa(T27, T20, T21, div1_in_ggaa(T27, s(s(0)), T20, T21))
U2_gaaa(T27, T20, T21, div1_out_ggaa(T27, s(s(0)), T20, T21)) → div1_out_gaaa(s(s(T27)), s(s(0)), s(T20), T21)
div1_in_gaaa(s(s(s(T30))), s(s(s(0))), s(T20), T21) → U3_gaaa(T30, T20, T21, div1_in_ggaa(T30, s(s(s(0))), T20, T21))
U3_gaaa(T30, T20, T21, div1_out_ggaa(T30, s(s(s(0))), T20, T21)) → div1_out_gaaa(s(s(s(T30))), s(s(s(0))), s(T20), T21)
div1_in_gaaa(s(s(s(s(T33)))), s(s(s(s(0)))), s(T20), T21) → U4_gaaa(T33, T20, T21, div1_in_ggaa(T33, s(s(s(s(0)))), T20, T21))
U4_gaaa(T33, T20, T21, div1_out_ggaa(T33, s(s(s(s(0)))), T20, T21)) → div1_out_gaaa(s(s(s(s(T33)))), s(s(s(s(0)))), s(T20), T21)
div1_in_gaaa(s(s(s(s(s(T36))))), s(s(s(s(s(0))))), s(T20), T21) → U5_gaaa(T36, T20, T21, div1_in_ggaa(T36, s(s(s(s(s(0))))), T20, T21))
U5_gaaa(T36, T20, T21, div1_out_ggaa(T36, s(s(s(s(s(0))))), T20, T21)) → div1_out_gaaa(s(s(s(s(s(T36))))), s(s(s(s(s(0))))), s(T20), T21)
div1_in_gaaa(s(s(s(s(s(s(T39)))))), s(s(s(s(s(s(0)))))), s(T20), T21) → U6_gaaa(T39, T20, T21, div1_in_ggaa(T39, s(s(s(s(s(s(0)))))), T20, T21))
U6_gaaa(T39, T20, T21, div1_out_ggaa(T39, s(s(s(s(s(s(0)))))), T20, T21)) → div1_out_gaaa(s(s(s(s(s(s(T39)))))), s(s(s(s(s(s(0)))))), s(T20), T21)
div1_in_gaaa(s(s(s(s(s(s(s(T40))))))), s(s(s(s(s(s(s(T41))))))), s(T20), T21) → U7_gaaa(T40, T41, T20, T21, minus61_in_gaa(T40, T41, X94))
minus61_in_gaa(T44, 0, T44) → minus61_out_gaa(T44, 0, T44)
minus61_in_gaa(s(T45), s(T46), X104) → U10_gaa(T45, T46, X104, minus61_in_gaa(T45, T46, X104))
U10_gaa(T45, T46, X104, minus61_out_gaa(T45, T46, X104)) → minus61_out_gaa(s(T45), s(T46), X104)
U7_gaaa(T40, T41, T20, T21, minus61_out_gaa(T40, T41, X94)) → div1_out_gaaa(s(s(s(s(s(s(s(T40))))))), s(s(s(s(s(s(s(T41))))))), s(T20), T21)
div1_in_gaaa(s(s(s(s(s(s(s(T40))))))), s(s(s(s(s(s(s(T41))))))), s(T20), T21) → U8_gaaa(T40, T41, T20, T21, minus61_in_gaa(T40, T41, T43))
U8_gaaa(T40, T41, T20, T21, minus61_out_gaa(T40, T41, T43)) → U9_gaaa(T40, T41, T20, T21, div1_in_gaaa(T43, s(T42), T20, T21))
div1_in_gaaa(s(s(s(s(s(s(T47)))))), s(s(s(s(s(s(T48)))))), T49, s(s(s(s(s(s(T47))))))) → div1_out_gaaa(s(s(s(s(s(s(T47)))))), s(s(s(s(s(s(T48)))))), T49, s(s(s(s(s(s(T47)))))))
div1_in_gaaa(s(s(s(s(s(T50))))), s(s(s(s(s(T51))))), T52, s(s(s(s(s(T50)))))) → div1_out_gaaa(s(s(s(s(s(T50))))), s(s(s(s(s(T51))))), T52, s(s(s(s(s(T50))))))
div1_in_gaaa(s(s(s(s(T53)))), s(s(s(s(T54)))), T55, s(s(s(s(T53))))) → div1_out_gaaa(s(s(s(s(T53)))), s(s(s(s(T54)))), T55, s(s(s(s(T53)))))
div1_in_gaaa(s(s(s(T56))), s(s(s(T57))), T58, s(s(s(T56)))) → div1_out_gaaa(s(s(s(T56))), s(s(s(T57))), T58, s(s(s(T56))))
div1_in_gaaa(s(s(T59)), s(s(T60)), T61, s(s(T59))) → div1_out_gaaa(s(s(T59)), s(s(T60)), T61, s(s(T59)))
div1_in_gaaa(s(T62), s(T63), T64, s(T62)) → div1_out_gaaa(s(T62), s(T63), T64, s(T62))
div1_in_gaaa(T65, T66, T67, T65) → div1_out_gaaa(T65, T66, T67, T65)
U9_gaaa(T40, T41, T20, T21, div1_out_gaaa(T43, s(T42), T20, T21)) → div1_out_gaaa(s(s(s(s(s(s(s(T40))))))), s(s(s(s(s(s(s(T41))))))), s(T20), T21)
U9_ggaa(T40, T41, T20, T21, div1_out_gaaa(T43, s(T42), T20, T21)) → div1_out_ggaa(s(s(s(s(s(s(s(T40))))))), s(s(s(s(s(s(s(T41))))))), s(T20), T21)
U6_ggaa(T39, T20, T21, div1_out_ggaa(T39, s(s(s(s(s(s(0)))))), T20, T21)) → div1_out_ggaa(s(s(s(s(s(s(T39)))))), s(s(s(s(s(s(0)))))), s(T20), T21)
U5_ggaa(T36, T20, T21, div1_out_ggaa(T36, s(s(s(s(s(0))))), T20, T21)) → div1_out_ggaa(s(s(s(s(s(T36))))), s(s(s(s(s(0))))), s(T20), T21)
U4_ggaa(T33, T20, T21, div1_out_ggaa(T33, s(s(s(s(0)))), T20, T21)) → div1_out_ggaa(s(s(s(s(T33)))), s(s(s(s(0)))), s(T20), T21)
U3_ggaa(T30, T20, T21, div1_out_ggaa(T30, s(s(s(0))), T20, T21)) → div1_out_ggaa(s(s(s(T30))), s(s(s(0))), s(T20), T21)
U2_ggaa(T27, T20, T21, div1_out_ggaa(T27, s(s(0)), T20, T21)) → div1_out_ggaa(s(s(T27)), s(s(0)), s(T20), T21)
U1_ggaa(T24, T20, T21, div1_out_ggaa(T24, s(0), T20, T21)) → div1_out_ggaa(s(T24), s(0), s(T20), T21)

(45) UsableRulesProof (EQUIVALENT transformation)

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

(46) Obligation:

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

DIV1_IN_GGAA(s(s(s(T30))), s(s(s(0))), s(T20), T21) → DIV1_IN_GGAA(T30, s(s(s(0))), T20, T21)

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

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

(47) PiDPToQDPProof (SOUND transformation)

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

(48) Obligation:

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

DIV1_IN_GGAA(s(s(s(T30))), s(s(s(0)))) → DIV1_IN_GGAA(T30, s(s(s(0))))

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

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

DIV1_IN_GGAA(s(s(s(T30))), s(s(s(0)))) → DIV1_IN_GGAA(T30, s(s(s(0))))
The graph contains the following edges 1 > 1, 2 >= 2

(50) TRUE

(51) Obligation:

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

DIV1_IN_GGAA(s(s(T27)), s(s(0)), s(T20), T21) → DIV1_IN_GGAA(T27, s(s(0)), T20, T21)

The TRS R consists of the following rules:

div1_in_ggaa(0, T8, 0, 0) → div1_out_ggaa(0, T8, 0, 0)
div1_in_ggaa(s(T24), s(0), s(T20), T21) → U1_ggaa(T24, T20, T21, div1_in_ggaa(T24, s(0), T20, T21))
div1_in_ggaa(s(s(T27)), s(s(0)), s(T20), T21) → U2_ggaa(T27, T20, T21, div1_in_ggaa(T27, s(s(0)), T20, T21))
div1_in_ggaa(s(s(s(T30))), s(s(s(0))), s(T20), T21) → U3_ggaa(T30, T20, T21, div1_in_ggaa(T30, s(s(s(0))), T20, T21))
div1_in_ggaa(s(s(s(s(T33)))), s(s(s(s(0)))), s(T20), T21) → U4_ggaa(T33, T20, T21, div1_in_ggaa(T33, s(s(s(s(0)))), T20, T21))
div1_in_ggaa(s(s(s(s(s(T36))))), s(s(s(s(s(0))))), s(T20), T21) → U5_ggaa(T36, T20, T21, div1_in_ggaa(T36, s(s(s(s(s(0))))), T20, T21))
div1_in_ggaa(s(s(s(s(s(s(T39)))))), s(s(s(s(s(s(0)))))), s(T20), T21) → U6_ggaa(T39, T20, T21, div1_in_ggaa(T39, s(s(s(s(s(s(0)))))), T20, T21))
div1_in_ggaa(s(s(s(s(s(s(s(T40))))))), s(s(s(s(s(s(s(T41))))))), s(T20), T21) → U7_ggaa(T40, T41, T20, T21, minus61_in_gga(T40, T41, X94))
minus61_in_gga(T44, 0, T44) → minus61_out_gga(T44, 0, T44)
minus61_in_gga(s(T45), s(T46), X104) → U10_gga(T45, T46, X104, minus61_in_gga(T45, T46, X104))
U10_gga(T45, T46, X104, minus61_out_gga(T45, T46, X104)) → minus61_out_gga(s(T45), s(T46), X104)
U7_ggaa(T40, T41, T20, T21, minus61_out_gga(T40, T41, X94)) → div1_out_ggaa(s(s(s(s(s(s(s(T40))))))), s(s(s(s(s(s(s(T41))))))), s(T20), T21)
div1_in_ggaa(s(s(s(s(s(s(s(T40))))))), s(s(s(s(s(s(s(T41))))))), s(T20), T21) → U8_ggaa(T40, T41, T20, T21, minus61_in_gga(T40, T41, T43))
U8_ggaa(T40, T41, T20, T21, minus61_out_gga(T40, T41, T43)) → U9_ggaa(T40, T41, T20, T21, div1_in_gaaa(T43, s(T42), T20, T21))
div1_in_gaaa(0, T8, 0, 0) → div1_out_gaaa(0, T8, 0, 0)
div1_in_gaaa(s(T24), s(0), s(T20), T21) → U1_gaaa(T24, T20, T21, div1_in_ggaa(T24, s(0), T20, T21))
div1_in_ggaa(s(s(s(s(s(s(T47)))))), s(s(s(s(s(s(T48)))))), T49, s(s(s(s(s(s(T47))))))) → div1_out_ggaa(s(s(s(s(s(s(T47)))))), s(s(s(s(s(s(T48)))))), T49, s(s(s(s(s(s(T47)))))))
div1_in_ggaa(s(s(s(s(s(T50))))), s(s(s(s(s(T51))))), T52, s(s(s(s(s(T50)))))) → div1_out_ggaa(s(s(s(s(s(T50))))), s(s(s(s(s(T51))))), T52, s(s(s(s(s(T50))))))
div1_in_ggaa(s(s(s(s(T53)))), s(s(s(s(T54)))), T55, s(s(s(s(T53))))) → div1_out_ggaa(s(s(s(s(T53)))), s(s(s(s(T54)))), T55, s(s(s(s(T53)))))
div1_in_ggaa(s(s(s(T56))), s(s(s(T57))), T58, s(s(s(T56)))) → div1_out_ggaa(s(s(s(T56))), s(s(s(T57))), T58, s(s(s(T56))))
div1_in_ggaa(s(s(T59)), s(s(T60)), T61, s(s(T59))) → div1_out_ggaa(s(s(T59)), s(s(T60)), T61, s(s(T59)))
div1_in_ggaa(s(T62), s(T63), T64, s(T62)) → div1_out_ggaa(s(T62), s(T63), T64, s(T62))
div1_in_ggaa(T65, T66, T67, T65) → div1_out_ggaa(T65, T66, T67, T65)
U1_gaaa(T24, T20, T21, div1_out_ggaa(T24, s(0), T20, T21)) → div1_out_gaaa(s(T24), s(0), s(T20), T21)
div1_in_gaaa(s(s(T27)), s(s(0)), s(T20), T21) → U2_gaaa(T27, T20, T21, div1_in_ggaa(T27, s(s(0)), T20, T21))
U2_gaaa(T27, T20, T21, div1_out_ggaa(T27, s(s(0)), T20, T21)) → div1_out_gaaa(s(s(T27)), s(s(0)), s(T20), T21)
div1_in_gaaa(s(s(s(T30))), s(s(s(0))), s(T20), T21) → U3_gaaa(T30, T20, T21, div1_in_ggaa(T30, s(s(s(0))), T20, T21))
U3_gaaa(T30, T20, T21, div1_out_ggaa(T30, s(s(s(0))), T20, T21)) → div1_out_gaaa(s(s(s(T30))), s(s(s(0))), s(T20), T21)
div1_in_gaaa(s(s(s(s(T33)))), s(s(s(s(0)))), s(T20), T21) → U4_gaaa(T33, T20, T21, div1_in_ggaa(T33, s(s(s(s(0)))), T20, T21))
U4_gaaa(T33, T20, T21, div1_out_ggaa(T33, s(s(s(s(0)))), T20, T21)) → div1_out_gaaa(s(s(s(s(T33)))), s(s(s(s(0)))), s(T20), T21)
div1_in_gaaa(s(s(s(s(s(T36))))), s(s(s(s(s(0))))), s(T20), T21) → U5_gaaa(T36, T20, T21, div1_in_ggaa(T36, s(s(s(s(s(0))))), T20, T21))
U5_gaaa(T36, T20, T21, div1_out_ggaa(T36, s(s(s(s(s(0))))), T20, T21)) → div1_out_gaaa(s(s(s(s(s(T36))))), s(s(s(s(s(0))))), s(T20), T21)
div1_in_gaaa(s(s(s(s(s(s(T39)))))), s(s(s(s(s(s(0)))))), s(T20), T21) → U6_gaaa(T39, T20, T21, div1_in_ggaa(T39, s(s(s(s(s(s(0)))))), T20, T21))
U6_gaaa(T39, T20, T21, div1_out_ggaa(T39, s(s(s(s(s(s(0)))))), T20, T21)) → div1_out_gaaa(s(s(s(s(s(s(T39)))))), s(s(s(s(s(s(0)))))), s(T20), T21)
div1_in_gaaa(s(s(s(s(s(s(s(T40))))))), s(s(s(s(s(s(s(T41))))))), s(T20), T21) → U7_gaaa(T40, T41, T20, T21, minus61_in_gaa(T40, T41, X94))
minus61_in_gaa(T44, 0, T44) → minus61_out_gaa(T44, 0, T44)
minus61_in_gaa(s(T45), s(T46), X104) → U10_gaa(T45, T46, X104, minus61_in_gaa(T45, T46, X104))
U10_gaa(T45, T46, X104, minus61_out_gaa(T45, T46, X104)) → minus61_out_gaa(s(T45), s(T46), X104)
U7_gaaa(T40, T41, T20, T21, minus61_out_gaa(T40, T41, X94)) → div1_out_gaaa(s(s(s(s(s(s(s(T40))))))), s(s(s(s(s(s(s(T41))))))), s(T20), T21)
div1_in_gaaa(s(s(s(s(s(s(s(T40))))))), s(s(s(s(s(s(s(T41))))))), s(T20), T21) → U8_gaaa(T40, T41, T20, T21, minus61_in_gaa(T40, T41, T43))
U8_gaaa(T40, T41, T20, T21, minus61_out_gaa(T40, T41, T43)) → U9_gaaa(T40, T41, T20, T21, div1_in_gaaa(T43, s(T42), T20, T21))
div1_in_gaaa(s(s(s(s(s(s(T47)))))), s(s(s(s(s(s(T48)))))), T49, s(s(s(s(s(s(T47))))))) → div1_out_gaaa(s(s(s(s(s(s(T47)))))), s(s(s(s(s(s(T48)))))), T49, s(s(s(s(s(s(T47)))))))
div1_in_gaaa(s(s(s(s(s(T50))))), s(s(s(s(s(T51))))), T52, s(s(s(s(s(T50)))))) → div1_out_gaaa(s(s(s(s(s(T50))))), s(s(s(s(s(T51))))), T52, s(s(s(s(s(T50))))))
div1_in_gaaa(s(s(s(s(T53)))), s(s(s(s(T54)))), T55, s(s(s(s(T53))))) → div1_out_gaaa(s(s(s(s(T53)))), s(s(s(s(T54)))), T55, s(s(s(s(T53)))))
div1_in_gaaa(s(s(s(T56))), s(s(s(T57))), T58, s(s(s(T56)))) → div1_out_gaaa(s(s(s(T56))), s(s(s(T57))), T58, s(s(s(T56))))
div1_in_gaaa(s(s(T59)), s(s(T60)), T61, s(s(T59))) → div1_out_gaaa(s(s(T59)), s(s(T60)), T61, s(s(T59)))
div1_in_gaaa(s(T62), s(T63), T64, s(T62)) → div1_out_gaaa(s(T62), s(T63), T64, s(T62))
div1_in_gaaa(T65, T66, T67, T65) → div1_out_gaaa(T65, T66, T67, T65)
U9_gaaa(T40, T41, T20, T21, div1_out_gaaa(T43, s(T42), T20, T21)) → div1_out_gaaa(s(s(s(s(s(s(s(T40))))))), s(s(s(s(s(s(s(T41))))))), s(T20), T21)
U9_ggaa(T40, T41, T20, T21, div1_out_gaaa(T43, s(T42), T20, T21)) → div1_out_ggaa(s(s(s(s(s(s(s(T40))))))), s(s(s(s(s(s(s(T41))))))), s(T20), T21)
U6_ggaa(T39, T20, T21, div1_out_ggaa(T39, s(s(s(s(s(s(0)))))), T20, T21)) → div1_out_ggaa(s(s(s(s(s(s(T39)))))), s(s(s(s(s(s(0)))))), s(T20), T21)
U5_ggaa(T36, T20, T21, div1_out_ggaa(T36, s(s(s(s(s(0))))), T20, T21)) → div1_out_ggaa(s(s(s(s(s(T36))))), s(s(s(s(s(0))))), s(T20), T21)
U4_ggaa(T33, T20, T21, div1_out_ggaa(T33, s(s(s(s(0)))), T20, T21)) → div1_out_ggaa(s(s(s(s(T33)))), s(s(s(s(0)))), s(T20), T21)
U3_ggaa(T30, T20, T21, div1_out_ggaa(T30, s(s(s(0))), T20, T21)) → div1_out_ggaa(s(s(s(T30))), s(s(s(0))), s(T20), T21)
U2_ggaa(T27, T20, T21, div1_out_ggaa(T27, s(s(0)), T20, T21)) → div1_out_ggaa(s(s(T27)), s(s(0)), s(T20), T21)
U1_ggaa(T24, T20, T21, div1_out_ggaa(T24, s(0), T20, T21)) → div1_out_ggaa(s(T24), s(0), s(T20), T21)

(52) UsableRulesProof (EQUIVALENT transformation)

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

(53) Obligation:

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

DIV1_IN_GGAA(s(s(T27)), s(s(0)), s(T20), T21) → DIV1_IN_GGAA(T27, s(s(0)), T20, T21)

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

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

(54) PiDPToQDPProof (SOUND transformation)

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

(55) Obligation:

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

DIV1_IN_GGAA(s(s(T27)), s(s(0))) → DIV1_IN_GGAA(T27, s(s(0)))

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

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

DIV1_IN_GGAA(s(s(T27)), s(s(0))) → DIV1_IN_GGAA(T27, s(s(0)))
The graph contains the following edges 1 > 1, 2 >= 2

(57) TRUE

(58) Obligation:

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

DIV1_IN_GGAA(s(T24), s(0), s(T20), T21) → DIV1_IN_GGAA(T24, s(0), T20, T21)

The TRS R consists of the following rules:

div1_in_ggaa(0, T8, 0, 0) → div1_out_ggaa(0, T8, 0, 0)
div1_in_ggaa(s(T24), s(0), s(T20), T21) → U1_ggaa(T24, T20, T21, div1_in_ggaa(T24, s(0), T20, T21))
div1_in_ggaa(s(s(T27)), s(s(0)), s(T20), T21) → U2_ggaa(T27, T20, T21, div1_in_ggaa(T27, s(s(0)), T20, T21))
div1_in_ggaa(s(s(s(T30))), s(s(s(0))), s(T20), T21) → U3_ggaa(T30, T20, T21, div1_in_ggaa(T30, s(s(s(0))), T20, T21))
div1_in_ggaa(s(s(s(s(T33)))), s(s(s(s(0)))), s(T20), T21) → U4_ggaa(T33, T20, T21, div1_in_ggaa(T33, s(s(s(s(0)))), T20, T21))
div1_in_ggaa(s(s(s(s(s(T36))))), s(s(s(s(s(0))))), s(T20), T21) → U5_ggaa(T36, T20, T21, div1_in_ggaa(T36, s(s(s(s(s(0))))), T20, T21))
div1_in_ggaa(s(s(s(s(s(s(T39)))))), s(s(s(s(s(s(0)))))), s(T20), T21) → U6_ggaa(T39, T20, T21, div1_in_ggaa(T39, s(s(s(s(s(s(0)))))), T20, T21))
div1_in_ggaa(s(s(s(s(s(s(s(T40))))))), s(s(s(s(s(s(s(T41))))))), s(T20), T21) → U7_ggaa(T40, T41, T20, T21, minus61_in_gga(T40, T41, X94))
minus61_in_gga(T44, 0, T44) → minus61_out_gga(T44, 0, T44)
minus61_in_gga(s(T45), s(T46), X104) → U10_gga(T45, T46, X104, minus61_in_gga(T45, T46, X104))
U10_gga(T45, T46, X104, minus61_out_gga(T45, T46, X104)) → minus61_out_gga(s(T45), s(T46), X104)
U7_ggaa(T40, T41, T20, T21, minus61_out_gga(T40, T41, X94)) → div1_out_ggaa(s(s(s(s(s(s(s(T40))))))), s(s(s(s(s(s(s(T41))))))), s(T20), T21)
div1_in_ggaa(s(s(s(s(s(s(s(T40))))))), s(s(s(s(s(s(s(T41))))))), s(T20), T21) → U8_ggaa(T40, T41, T20, T21, minus61_in_gga(T40, T41, T43))
U8_ggaa(T40, T41, T20, T21, minus61_out_gga(T40, T41, T43)) → U9_ggaa(T40, T41, T20, T21, div1_in_gaaa(T43, s(T42), T20, T21))
div1_in_gaaa(0, T8, 0, 0) → div1_out_gaaa(0, T8, 0, 0)
div1_in_gaaa(s(T24), s(0), s(T20), T21) → U1_gaaa(T24, T20, T21, div1_in_ggaa(T24, s(0), T20, T21))
div1_in_ggaa(s(s(s(s(s(s(T47)))))), s(s(s(s(s(s(T48)))))), T49, s(s(s(s(s(s(T47))))))) → div1_out_ggaa(s(s(s(s(s(s(T47)))))), s(s(s(s(s(s(T48)))))), T49, s(s(s(s(s(s(T47)))))))
div1_in_ggaa(s(s(s(s(s(T50))))), s(s(s(s(s(T51))))), T52, s(s(s(s(s(T50)))))) → div1_out_ggaa(s(s(s(s(s(T50))))), s(s(s(s(s(T51))))), T52, s(s(s(s(s(T50))))))
div1_in_ggaa(s(s(s(s(T53)))), s(s(s(s(T54)))), T55, s(s(s(s(T53))))) → div1_out_ggaa(s(s(s(s(T53)))), s(s(s(s(T54)))), T55, s(s(s(s(T53)))))
div1_in_ggaa(s(s(s(T56))), s(s(s(T57))), T58, s(s(s(T56)))) → div1_out_ggaa(s(s(s(T56))), s(s(s(T57))), T58, s(s(s(T56))))
div1_in_ggaa(s(s(T59)), s(s(T60)), T61, s(s(T59))) → div1_out_ggaa(s(s(T59)), s(s(T60)), T61, s(s(T59)))
div1_in_ggaa(s(T62), s(T63), T64, s(T62)) → div1_out_ggaa(s(T62), s(T63), T64, s(T62))
div1_in_ggaa(T65, T66, T67, T65) → div1_out_ggaa(T65, T66, T67, T65)
U1_gaaa(T24, T20, T21, div1_out_ggaa(T24, s(0), T20, T21)) → div1_out_gaaa(s(T24), s(0), s(T20), T21)
div1_in_gaaa(s(s(T27)), s(s(0)), s(T20), T21) → U2_gaaa(T27, T20, T21, div1_in_ggaa(T27, s(s(0)), T20, T21))
U2_gaaa(T27, T20, T21, div1_out_ggaa(T27, s(s(0)), T20, T21)) → div1_out_gaaa(s(s(T27)), s(s(0)), s(T20), T21)
div1_in_gaaa(s(s(s(T30))), s(s(s(0))), s(T20), T21) → U3_gaaa(T30, T20, T21, div1_in_ggaa(T30, s(s(s(0))), T20, T21))
U3_gaaa(T30, T20, T21, div1_out_ggaa(T30, s(s(s(0))), T20, T21)) → div1_out_gaaa(s(s(s(T30))), s(s(s(0))), s(T20), T21)
div1_in_gaaa(s(s(s(s(T33)))), s(s(s(s(0)))), s(T20), T21) → U4_gaaa(T33, T20, T21, div1_in_ggaa(T33, s(s(s(s(0)))), T20, T21))
U4_gaaa(T33, T20, T21, div1_out_ggaa(T33, s(s(s(s(0)))), T20, T21)) → div1_out_gaaa(s(s(s(s(T33)))), s(s(s(s(0)))), s(T20), T21)
div1_in_gaaa(s(s(s(s(s(T36))))), s(s(s(s(s(0))))), s(T20), T21) → U5_gaaa(T36, T20, T21, div1_in_ggaa(T36, s(s(s(s(s(0))))), T20, T21))
U5_gaaa(T36, T20, T21, div1_out_ggaa(T36, s(s(s(s(s(0))))), T20, T21)) → div1_out_gaaa(s(s(s(s(s(T36))))), s(s(s(s(s(0))))), s(T20), T21)
div1_in_gaaa(s(s(s(s(s(s(T39)))))), s(s(s(s(s(s(0)))))), s(T20), T21) → U6_gaaa(T39, T20, T21, div1_in_ggaa(T39, s(s(s(s(s(s(0)))))), T20, T21))
U6_gaaa(T39, T20, T21, div1_out_ggaa(T39, s(s(s(s(s(s(0)))))), T20, T21)) → div1_out_gaaa(s(s(s(s(s(s(T39)))))), s(s(s(s(s(s(0)))))), s(T20), T21)
div1_in_gaaa(s(s(s(s(s(s(s(T40))))))), s(s(s(s(s(s(s(T41))))))), s(T20), T21) → U7_gaaa(T40, T41, T20, T21, minus61_in_gaa(T40, T41, X94))
minus61_in_gaa(T44, 0, T44) → minus61_out_gaa(T44, 0, T44)
minus61_in_gaa(s(T45), s(T46), X104) → U10_gaa(T45, T46, X104, minus61_in_gaa(T45, T46, X104))
U10_gaa(T45, T46, X104, minus61_out_gaa(T45, T46, X104)) → minus61_out_gaa(s(T45), s(T46), X104)
U7_gaaa(T40, T41, T20, T21, minus61_out_gaa(T40, T41, X94)) → div1_out_gaaa(s(s(s(s(s(s(s(T40))))))), s(s(s(s(s(s(s(T41))))))), s(T20), T21)
div1_in_gaaa(s(s(s(s(s(s(s(T40))))))), s(s(s(s(s(s(s(T41))))))), s(T20), T21) → U8_gaaa(T40, T41, T20, T21, minus61_in_gaa(T40, T41, T43))
U8_gaaa(T40, T41, T20, T21, minus61_out_gaa(T40, T41, T43)) → U9_gaaa(T40, T41, T20, T21, div1_in_gaaa(T43, s(T42), T20, T21))
div1_in_gaaa(s(s(s(s(s(s(T47)))))), s(s(s(s(s(s(T48)))))), T49, s(s(s(s(s(s(T47))))))) → div1_out_gaaa(s(s(s(s(s(s(T47)))))), s(s(s(s(s(s(T48)))))), T49, s(s(s(s(s(s(T47)))))))
div1_in_gaaa(s(s(s(s(s(T50))))), s(s(s(s(s(T51))))), T52, s(s(s(s(s(T50)))))) → div1_out_gaaa(s(s(s(s(s(T50))))), s(s(s(s(s(T51))))), T52, s(s(s(s(s(T50))))))
div1_in_gaaa(s(s(s(s(T53)))), s(s(s(s(T54)))), T55, s(s(s(s(T53))))) → div1_out_gaaa(s(s(s(s(T53)))), s(s(s(s(T54)))), T55, s(s(s(s(T53)))))
div1_in_gaaa(s(s(s(T56))), s(s(s(T57))), T58, s(s(s(T56)))) → div1_out_gaaa(s(s(s(T56))), s(s(s(T57))), T58, s(s(s(T56))))
div1_in_gaaa(s(s(T59)), s(s(T60)), T61, s(s(T59))) → div1_out_gaaa(s(s(T59)), s(s(T60)), T61, s(s(T59)))
div1_in_gaaa(s(T62), s(T63), T64, s(T62)) → div1_out_gaaa(s(T62), s(T63), T64, s(T62))
div1_in_gaaa(T65, T66, T67, T65) → div1_out_gaaa(T65, T66, T67, T65)
U9_gaaa(T40, T41, T20, T21, div1_out_gaaa(T43, s(T42), T20, T21)) → div1_out_gaaa(s(s(s(s(s(s(s(T40))))))), s(s(s(s(s(s(s(T41))))))), s(T20), T21)
U9_ggaa(T40, T41, T20, T21, div1_out_gaaa(T43, s(T42), T20, T21)) → div1_out_ggaa(s(s(s(s(s(s(s(T40))))))), s(s(s(s(s(s(s(T41))))))), s(T20), T21)
U6_ggaa(T39, T20, T21, div1_out_ggaa(T39, s(s(s(s(s(s(0)))))), T20, T21)) → div1_out_ggaa(s(s(s(s(s(s(T39)))))), s(s(s(s(s(s(0)))))), s(T20), T21)
U5_ggaa(T36, T20, T21, div1_out_ggaa(T36, s(s(s(s(s(0))))), T20, T21)) → div1_out_ggaa(s(s(s(s(s(T36))))), s(s(s(s(s(0))))), s(T20), T21)
U4_ggaa(T33, T20, T21, div1_out_ggaa(T33, s(s(s(s(0)))), T20, T21)) → div1_out_ggaa(s(s(s(s(T33)))), s(s(s(s(0)))), s(T20), T21)
U3_ggaa(T30, T20, T21, div1_out_ggaa(T30, s(s(s(0))), T20, T21)) → div1_out_ggaa(s(s(s(T30))), s(s(s(0))), s(T20), T21)
U2_ggaa(T27, T20, T21, div1_out_ggaa(T27, s(s(0)), T20, T21)) → div1_out_ggaa(s(s(T27)), s(s(0)), s(T20), T21)
U1_ggaa(T24, T20, T21, div1_out_ggaa(T24, s(0), T20, T21)) → div1_out_ggaa(s(T24), s(0), s(T20), T21)

(59) UsableRulesProof (EQUIVALENT transformation)

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

(60) Obligation:

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

DIV1_IN_GGAA(s(T24), s(0), s(T20), T21) → DIV1_IN_GGAA(T24, s(0), T20, T21)

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

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

(61) PiDPToQDPProof (SOUND transformation)

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

(62) Obligation:

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

DIV1_IN_GGAA(s(T24), s(0)) → DIV1_IN_GGAA(T24, s(0))

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

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

DIV1_IN_GGAA(s(T24), s(0)) → DIV1_IN_GGAA(T24, s(0))
The graph contains the following edges 1 > 1, 2 >= 2

(64) TRUE

(65) Obligation:

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

DIV1_IN_GAAA(s(s(s(s(s(s(s(T40))))))), s(s(s(s(s(s(s(T41))))))), s(T20), T21) → U8_GAAA(T40, T41, T20, T21, minus61_in_gaa(T40, T41, T43))
U8_GAAA(T40, T41, T20, T21, minus61_out_gaa(T40, T41, T43)) → DIV1_IN_GAAA(T43, s(T42), T20, T21)

The TRS R consists of the following rules:

div1_in_ggaa(0, T8, 0, 0) → div1_out_ggaa(0, T8, 0, 0)
div1_in_ggaa(s(T24), s(0), s(T20), T21) → U1_ggaa(T24, T20, T21, div1_in_ggaa(T24, s(0), T20, T21))
div1_in_ggaa(s(s(T27)), s(s(0)), s(T20), T21) → U2_ggaa(T27, T20, T21, div1_in_ggaa(T27, s(s(0)), T20, T21))
div1_in_ggaa(s(s(s(T30))), s(s(s(0))), s(T20), T21) → U3_ggaa(T30, T20, T21, div1_in_ggaa(T30, s(s(s(0))), T20, T21))
div1_in_ggaa(s(s(s(s(T33)))), s(s(s(s(0)))), s(T20), T21) → U4_ggaa(T33, T20, T21, div1_in_ggaa(T33, s(s(s(s(0)))), T20, T21))
div1_in_ggaa(s(s(s(s(s(T36))))), s(s(s(s(s(0))))), s(T20), T21) → U5_ggaa(T36, T20, T21, div1_in_ggaa(T36, s(s(s(s(s(0))))), T20, T21))
div1_in_ggaa(s(s(s(s(s(s(T39)))))), s(s(s(s(s(s(0)))))), s(T20), T21) → U6_ggaa(T39, T20, T21, div1_in_ggaa(T39, s(s(s(s(s(s(0)))))), T20, T21))
div1_in_ggaa(s(s(s(s(s(s(s(T40))))))), s(s(s(s(s(s(s(T41))))))), s(T20), T21) → U7_ggaa(T40, T41, T20, T21, minus61_in_gga(T40, T41, X94))
minus61_in_gga(T44, 0, T44) → minus61_out_gga(T44, 0, T44)
minus61_in_gga(s(T45), s(T46), X104) → U10_gga(T45, T46, X104, minus61_in_gga(T45, T46, X104))
U10_gga(T45, T46, X104, minus61_out_gga(T45, T46, X104)) → minus61_out_gga(s(T45), s(T46), X104)
U7_ggaa(T40, T41, T20, T21, minus61_out_gga(T40, T41, X94)) → div1_out_ggaa(s(s(s(s(s(s(s(T40))))))), s(s(s(s(s(s(s(T41))))))), s(T20), T21)
div1_in_ggaa(s(s(s(s(s(s(s(T40))))))), s(s(s(s(s(s(s(T41))))))), s(T20), T21) → U8_ggaa(T40, T41, T20, T21, minus61_in_gga(T40, T41, T43))
U8_ggaa(T40, T41, T20, T21, minus61_out_gga(T40, T41, T43)) → U9_ggaa(T40, T41, T20, T21, div1_in_gaaa(T43, s(T42), T20, T21))
div1_in_gaaa(0, T8, 0, 0) → div1_out_gaaa(0, T8, 0, 0)
div1_in_gaaa(s(T24), s(0), s(T20), T21) → U1_gaaa(T24, T20, T21, div1_in_ggaa(T24, s(0), T20, T21))
div1_in_ggaa(s(s(s(s(s(s(T47)))))), s(s(s(s(s(s(T48)))))), T49, s(s(s(s(s(s(T47))))))) → div1_out_ggaa(s(s(s(s(s(s(T47)))))), s(s(s(s(s(s(T48)))))), T49, s(s(s(s(s(s(T47)))))))
div1_in_ggaa(s(s(s(s(s(T50))))), s(s(s(s(s(T51))))), T52, s(s(s(s(s(T50)))))) → div1_out_ggaa(s(s(s(s(s(T50))))), s(s(s(s(s(T51))))), T52, s(s(s(s(s(T50))))))
div1_in_ggaa(s(s(s(s(T53)))), s(s(s(s(T54)))), T55, s(s(s(s(T53))))) → div1_out_ggaa(s(s(s(s(T53)))), s(s(s(s(T54)))), T55, s(s(s(s(T53)))))
div1_in_ggaa(s(s(s(T56))), s(s(s(T57))), T58, s(s(s(T56)))) → div1_out_ggaa(s(s(s(T56))), s(s(s(T57))), T58, s(s(s(T56))))
div1_in_ggaa(s(s(T59)), s(s(T60)), T61, s(s(T59))) → div1_out_ggaa(s(s(T59)), s(s(T60)), T61, s(s(T59)))
div1_in_ggaa(s(T62), s(T63), T64, s(T62)) → div1_out_ggaa(s(T62), s(T63), T64, s(T62))
div1_in_ggaa(T65, T66, T67, T65) → div1_out_ggaa(T65, T66, T67, T65)
U1_gaaa(T24, T20, T21, div1_out_ggaa(T24, s(0), T20, T21)) → div1_out_gaaa(s(T24), s(0), s(T20), T21)
div1_in_gaaa(s(s(T27)), s(s(0)), s(T20), T21) → U2_gaaa(T27, T20, T21, div1_in_ggaa(T27, s(s(0)), T20, T21))
U2_gaaa(T27, T20, T21, div1_out_ggaa(T27, s(s(0)), T20, T21)) → div1_out_gaaa(s(s(T27)), s(s(0)), s(T20), T21)
div1_in_gaaa(s(s(s(T30))), s(s(s(0))), s(T20), T21) → U3_gaaa(T30, T20, T21, div1_in_ggaa(T30, s(s(s(0))), T20, T21))
U3_gaaa(T30, T20, T21, div1_out_ggaa(T30, s(s(s(0))), T20, T21)) → div1_out_gaaa(s(s(s(T30))), s(s(s(0))), s(T20), T21)
div1_in_gaaa(s(s(s(s(T33)))), s(s(s(s(0)))), s(T20), T21) → U4_gaaa(T33, T20, T21, div1_in_ggaa(T33, s(s(s(s(0)))), T20, T21))
U4_gaaa(T33, T20, T21, div1_out_ggaa(T33, s(s(s(s(0)))), T20, T21)) → div1_out_gaaa(s(s(s(s(T33)))), s(s(s(s(0)))), s(T20), T21)
div1_in_gaaa(s(s(s(s(s(T36))))), s(s(s(s(s(0))))), s(T20), T21) → U5_gaaa(T36, T20, T21, div1_in_ggaa(T36, s(s(s(s(s(0))))), T20, T21))
U5_gaaa(T36, T20, T21, div1_out_ggaa(T36, s(s(s(s(s(0))))), T20, T21)) → div1_out_gaaa(s(s(s(s(s(T36))))), s(s(s(s(s(0))))), s(T20), T21)
div1_in_gaaa(s(s(s(s(s(s(T39)))))), s(s(s(s(s(s(0)))))), s(T20), T21) → U6_gaaa(T39, T20, T21, div1_in_ggaa(T39, s(s(s(s(s(s(0)))))), T20, T21))
U6_gaaa(T39, T20, T21, div1_out_ggaa(T39, s(s(s(s(s(s(0)))))), T20, T21)) → div1_out_gaaa(s(s(s(s(s(s(T39)))))), s(s(s(s(s(s(0)))))), s(T20), T21)
div1_in_gaaa(s(s(s(s(s(s(s(T40))))))), s(s(s(s(s(s(s(T41))))))), s(T20), T21) → U7_gaaa(T40, T41, T20, T21, minus61_in_gaa(T40, T41, X94))
minus61_in_gaa(T44, 0, T44) → minus61_out_gaa(T44, 0, T44)
minus61_in_gaa(s(T45), s(T46), X104) → U10_gaa(T45, T46, X104, minus61_in_gaa(T45, T46, X104))
U10_gaa(T45, T46, X104, minus61_out_gaa(T45, T46, X104)) → minus61_out_gaa(s(T45), s(T46), X104)
U7_gaaa(T40, T41, T20, T21, minus61_out_gaa(T40, T41, X94)) → div1_out_gaaa(s(s(s(s(s(s(s(T40))))))), s(s(s(s(s(s(s(T41))))))), s(T20), T21)
div1_in_gaaa(s(s(s(s(s(s(s(T40))))))), s(s(s(s(s(s(s(T41))))))), s(T20), T21) → U8_gaaa(T40, T41, T20, T21, minus61_in_gaa(T40, T41, T43))
U8_gaaa(T40, T41, T20, T21, minus61_out_gaa(T40, T41, T43)) → U9_gaaa(T40, T41, T20, T21, div1_in_gaaa(T43, s(T42), T20, T21))
div1_in_gaaa(s(s(s(s(s(s(T47)))))), s(s(s(s(s(s(T48)))))), T49, s(s(s(s(s(s(T47))))))) → div1_out_gaaa(s(s(s(s(s(s(T47)))))), s(s(s(s(s(s(T48)))))), T49, s(s(s(s(s(s(T47)))))))
div1_in_gaaa(s(s(s(s(s(T50))))), s(s(s(s(s(T51))))), T52, s(s(s(s(s(T50)))))) → div1_out_gaaa(s(s(s(s(s(T50))))), s(s(s(s(s(T51))))), T52, s(s(s(s(s(T50))))))
div1_in_gaaa(s(s(s(s(T53)))), s(s(s(s(T54)))), T55, s(s(s(s(T53))))) → div1_out_gaaa(s(s(s(s(T53)))), s(s(s(s(T54)))), T55, s(s(s(s(T53)))))
div1_in_gaaa(s(s(s(T56))), s(s(s(T57))), T58, s(s(s(T56)))) → div1_out_gaaa(s(s(s(T56))), s(s(s(T57))), T58, s(s(s(T56))))
div1_in_gaaa(s(s(T59)), s(s(T60)), T61, s(s(T59))) → div1_out_gaaa(s(s(T59)), s(s(T60)), T61, s(s(T59)))
div1_in_gaaa(s(T62), s(T63), T64, s(T62)) → div1_out_gaaa(s(T62), s(T63), T64, s(T62))
div1_in_gaaa(T65, T66, T67, T65) → div1_out_gaaa(T65, T66, T67, T65)
U9_gaaa(T40, T41, T20, T21, div1_out_gaaa(T43, s(T42), T20, T21)) → div1_out_gaaa(s(s(s(s(s(s(s(T40))))))), s(s(s(s(s(s(s(T41))))))), s(T20), T21)
U9_ggaa(T40, T41, T20, T21, div1_out_gaaa(T43, s(T42), T20, T21)) → div1_out_ggaa(s(s(s(s(s(s(s(T40))))))), s(s(s(s(s(s(s(T41))))))), s(T20), T21)
U6_ggaa(T39, T20, T21, div1_out_ggaa(T39, s(s(s(s(s(s(0)))))), T20, T21)) → div1_out_ggaa(s(s(s(s(s(s(T39)))))), s(s(s(s(s(s(0)))))), s(T20), T21)
U5_ggaa(T36, T20, T21, div1_out_ggaa(T36, s(s(s(s(s(0))))), T20, T21)) → div1_out_ggaa(s(s(s(s(s(T36))))), s(s(s(s(s(0))))), s(T20), T21)
U4_ggaa(T33, T20, T21, div1_out_ggaa(T33, s(s(s(s(0)))), T20, T21)) → div1_out_ggaa(s(s(s(s(T33)))), s(s(s(s(0)))), s(T20), T21)
U3_ggaa(T30, T20, T21, div1_out_ggaa(T30, s(s(s(0))), T20, T21)) → div1_out_ggaa(s(s(s(T30))), s(s(s(0))), s(T20), T21)
U2_ggaa(T27, T20, T21, div1_out_ggaa(T27, s(s(0)), T20, T21)) → div1_out_ggaa(s(s(T27)), s(s(0)), s(T20), T21)
U1_ggaa(T24, T20, T21, div1_out_ggaa(T24, s(0), T20, T21)) → div1_out_ggaa(s(T24), s(0), s(T20), T21)

(66) UsableRulesProof (EQUIVALENT transformation)

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

(67) Obligation:

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

DIV1_IN_GAAA(s(s(s(s(s(s(s(T40))))))), s(s(s(s(s(s(s(T41))))))), s(T20), T21) → U8_GAAA(T40, T41, T20, T21, minus61_in_gaa(T40, T41, T43))
U8_GAAA(T40, T41, T20, T21, minus61_out_gaa(T40, T41, T43)) → DIV1_IN_GAAA(T43, s(T42), T20, T21)

The TRS R consists of the following rules:

minus61_in_gaa(T44, 0, T44) → minus61_out_gaa(T44, 0, T44)
minus61_in_gaa(s(T45), s(T46), X104) → U10_gaa(T45, T46, X104, minus61_in_gaa(T45, T46, X104))
U10_gaa(T45, T46, X104, minus61_out_gaa(T45, T46, X104)) → minus61_out_gaa(s(T45), s(T46), X104)

The argument filtering Pi contains the following mapping:
0 = 0
s(x1) = s(x1)
minus61_in_gaa(x1, x2, x3) = minus61_in_gaa(x1)
minus61_out_gaa(x1, x2, x3) = minus61_out_gaa(x2, x3)
U10_gaa(x1, x2, x3, x4) = U10_gaa(x4)
DIV1_IN_GAAA(x1, x2, x3, x4) = DIV1_IN_GAAA(x1)
U8_GAAA(x1, x2, x3, x4, x5) = U8_GAAA(x5)

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

(68) PiDPToQDPProof (SOUND transformation)

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

(69) Obligation:

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

DIV1_IN_GAAA(s(s(s(s(s(s(s(T40)))))))) → U8_GAAA(minus61_in_gaa(T40))
U8_GAAA(minus61_out_gaa(T41, T43)) → DIV1_IN_GAAA(T43)

The TRS R consists of the following rules:

minus61_in_gaa(T44) → minus61_out_gaa(0, T44)
minus61_in_gaa(s(T45)) → U10_gaa(minus61_in_gaa(T45))
U10_gaa(minus61_out_gaa(T46, X104)) → minus61_out_gaa(s(T46), X104)

The set Q consists of the following terms:

minus61_in_gaa(x0)
U10_gaa(x0)

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

(70) MRRProof (EQUIVALENT transformation)

By using the rule removal processor [LPAR04] with the following ordering, at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented.
Strictly oriented dependency pairs:

DIV1_IN_GAAA(s(s(s(s(s(s(s(T40)))))))) → U8_GAAA(minus61_in_gaa(T40))
U8_GAAA(minus61_out_gaa(T41, T43)) → DIV1_IN_GAAA(T43)

Strictly oriented rules of the TRS R:

minus61_in_gaa(T44) → minus61_out_gaa(0, T44)

Used ordering: Polynomial interpretation [POLO]:

POL(0) = 0
POL(DIV1_IN_GAAA(x₁)) = x₁
POL(U10_gaa(x₁)) = 1 + x₁
POL(U8_GAAA(x₁)) = x₁
POL(minus61_in_gaa(x₁)) = 2 + x₁
POL(minus61_out_gaa(x₁, x₂)) = 1 + x₁ + x₂
POL(s(x₁)) = 1 + x₁

(71) Obligation:

Q DP problem:
P is empty.
The TRS R consists of the following rules:

minus61_in_gaa(s(T45)) → U10_gaa(minus61_in_gaa(T45))
U10_gaa(minus61_out_gaa(T46, X104)) → minus61_out_gaa(s(T46), X104)

The set Q consists of the following terms:

minus61_in_gaa(x0)
U10_gaa(x0)

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

(72) PisEmptyProof (EQUIVALENT transformation)

The TRS P is empty. Hence, there is no (P,Q,R) chain.

(0) Obligation:

(1) PrologToPrologProblemTransformerProof (SOUND transformation)

(2) Obligation:

(3) PrologToPiTRSProof (SOUND transformation)

(4) Obligation:

(5) DependencyPairsProof (EQUIVALENT transformation)

(6) Obligation:

(7) DependencyGraphProof (EQUIVALENT transformation)

(8) Complex Obligation (AND)

(9) Obligation:

(10) UsableRulesProof (EQUIVALENT transformation)

(11) Obligation:

(12) PiDPToQDPProof (SOUND transformation)

(13) Obligation:

(14) QDPSizeChangeProof (EQUIVALENT transformation)

(15) TRUE

(16) Obligation:

(17) UsableRulesProof (EQUIVALENT transformation)

(18) Obligation:

(19) PiDPToQDPProof (SOUND transformation)

(20) Obligation:

(21) QDPSizeChangeProof (EQUIVALENT transformation)

(22) TRUE

(23) Obligation:

(24) UsableRulesProof (EQUIVALENT transformation)

(25) Obligation:

(26) PiDPToQDPProof (SOUND transformation)

(27) Obligation:

(28) QDPSizeChangeProof (EQUIVALENT transformation)

(29) TRUE

(30) Obligation:

(31) UsableRulesProof (EQUIVALENT transformation)

(32) Obligation:

(33) PiDPToQDPProof (SOUND transformation)

(34) Obligation:

(35) QDPSizeChangeProof (EQUIVALENT transformation)

(36) TRUE

(37) Obligation:

(38) UsableRulesProof (EQUIVALENT transformation)

(39) Obligation:

(40) PiDPToQDPProof (SOUND transformation)

(41) Obligation:

(42) QDPSizeChangeProof (EQUIVALENT transformation)

(43) TRUE

(44) Obligation:

(45) UsableRulesProof (EQUIVALENT transformation)

(46) Obligation:

(47) PiDPToQDPProof (SOUND transformation)

(48) Obligation:

(49) QDPSizeChangeProof (EQUIVALENT transformation)

(50) TRUE

(51) Obligation:

(52) UsableRulesProof (EQUIVALENT transformation)

(53) Obligation:

(54) PiDPToQDPProof (SOUND transformation)

(55) Obligation:

(56) QDPSizeChangeProof (EQUIVALENT transformation)

(57) TRUE

(58) Obligation:

(59) UsableRulesProof (EQUIVALENT transformation)

(60) Obligation:

(61) PiDPToQDPProof (SOUND transformation)

(62) Obligation:

(63) QDPSizeChangeProof (EQUIVALENT transformation)

(64) TRUE

(65) Obligation:

(66) UsableRulesProof (EQUIVALENT transformation)

(67) Obligation:

(68) PiDPToQDPProof (SOUND transformation)

(69) Obligation:

(70) MRRProof (EQUIVALENT transformation)

(71) Obligation:

(72) PisEmptyProof (EQUIVALENT transformation)

(73) TRUE