Left Termination proof of /tmp/tmpKNSYMZ/fib

Left Termination of the query pattern fib_in_2(g, a) w.r.t. the given Prolog program could not be shown:

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 UsableRulesReductionPairsProof (⇔)

                ↳15 QDP

                ↳16 NonTerminationProof (⇔)

                ↳17 NO

            ↳18 PiDP

                ↳19 UsableRulesProof (⇔)

                ↳20 PiDP

                ↳21 PiDPToQDPProof (⇐)

                ↳22 QDP

                ↳23 NonTerminationProof (⇔)

                ↳24 NO

            ↳25 PiDP

                ↳26 UsableRulesProof (⇔)

                ↳27 PiDP

                ↳28 PiDPToQDPProof (⇐)

                ↳29 QDP

                ↳30 QDPSizeChangeProof (⇔)

                ↳31 YES

            ↳32 PiDP

                ↳33 UsableRulesProof (⇔)

                ↳34 PiDP

                ↳35 PiDPToQDPProof (⇐)

                ↳36 QDP

                ↳37 QDPSizeChangeProof (⇔)

                ↳38 YES

            ↳39 PiDP

                ↳40 UsableRulesProof (⇔)

                ↳41 PiDP

                ↳42 PiDPToQDPProof (⇐)

                ↳43 QDP

                ↳44 QDPSizeChangeProof (⇔)

                ↳45 YES

    ↳46 PrologToPiTRSProof (⇐)

        ↳47 PiTRS

        ↳48 DependencyPairsProof (⇔)

        ↳49 PiDP

        ↳50 DependencyGraphProof (⇔)

        ↳51 AND

            ↳52 PiDP

                ↳53 UsableRulesProof (⇔)

                ↳54 PiDP

                ↳55 PiDPToQDPProof (⇐)

                ↳56 QDP

                ↳57 UsableRulesReductionPairsProof (⇔)

                ↳58 QDP

                ↳59 NonTerminationProof (⇔)

                ↳60 NO

            ↳61 PiDP

                ↳62 UsableRulesProof (⇔)

                ↳63 PiDP

                ↳64 PiDPToQDPProof (⇐)

                ↳65 QDP

                ↳66 NonTerminationProof (⇔)

                ↳67 NO

            ↳68 PiDP

                ↳69 UsableRulesProof (⇔)

                ↳70 PiDP

                ↳71 PiDPToQDPProof (⇐)

                ↳72 QDP

                ↳73 QDPSizeChangeProof (⇔)

                ↳74 YES

            ↳75 PiDP

                ↳76 UsableRulesProof (⇔)

                ↳77 PiDP

                ↳78 PiDPToQDPProof (⇐)

                ↳79 QDP

                ↳80 QDPSizeChangeProof (⇔)

                ↳81 YES

            ↳82 PiDP

                ↳83 UsableRulesProof (⇔)

                ↳84 PiDP

                ↳85 PiDPToQDPProof (⇐)

                ↳86 QDP

                ↳87 QDPSizeChangeProof (⇔)

                ↳88 YES

(0) Obligation:

Clauses:

add(0, 0, 0).
add(s(X), Y, s(N)) :- add(X, Y, N).
add(X, s(Y), s(N)) :- add(X, Y, N).
fib(0, 0).
fib(s(0), s(0)).
fib(s(s(X)), N) :- ','(fib(s(X), N1), ','(fib(X, N2), add(N1, N2, N))).

Queries:

fib(g,a).

(1) PrologToPrologProblemTransformerProof (SOUND transformation)

Built Prolog problem from termination graph.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
1 [label="1: fib(T1, T2)\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
2 [label="2: fib(T1, T2), SCOPE: 1, CLAUSE: 3 | fib(T1, T2), SCOPE: 1, CLAUSE: 4 | fib(T1, T2), SCOPE: 1, CLAUSE: 5\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
3 [label="3: true | fib(0, T2), SCOPE: 1, CLAUSE: 4 | fib(0, T2), SCOPE: 1, CLAUSE: 5\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
4 [label="4: fib(T1, T2), SCOPE: 1, CLAUSE: 4 | fib(T1, T2), SCOPE: 1, CLAUSE: 5\n\nT1 is ground\nfib(T1, T2) !=? fib(0, 0)", fontsize=16, style=filled, fillcolor=lightyellow];
5 [label="5: fib(0, T2), SCOPE: 1, CLAUSE: 4 | fib(0, T2), SCOPE: 1, CLAUSE: 5\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
6 [label="6: fib(0, T2), SCOPE: 1, CLAUSE: 5\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
7 [label="7: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
8 [label="8: true | fib(s(0), T2), SCOPE: 1, CLAUSE: 5\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
9 [label="9: fib(T1, T2), SCOPE: 1, CLAUSE: 5\n\nT1 is ground\nfib(T1, T2) !=? fib(0, 0)\nfib(T1, T2) !=? fib(s(0), s(0))", fontsize=16, style=filled, fillcolor=lightyellow];
10 [label="10: fib(s(0), T2), SCOPE: 1, CLAUSE: 5\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
11 [label="11: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
12 [label="12: ','(fib(s(T5), X9), ','(fib(T5, X10), add(X9, X10, T7)))\n\nT5 is ground\nX9 is free; \nX10 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
13 [label="13: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
14 [label="14: ','(fib(s(T5), X9), ','(fib(T5, X10), add(X9, X10, T7))), SCOPE: 2, CLAUSE: 3 | ','(fib(s(T5), X9), ','(fib(T5, X10), add(X9, X10, T7))), SCOPE: 2, CLAUSE: 4 | ','(fib(s(T5), X9), ','(fib(T5, X10), add(X9, X10, T7))), SCOPE: 2, CLAUSE: 5\n\nT5 is ground\nX9 is free; \nX10 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
15 [label="15: ','(fib(s(T5), X9), ','(fib(T5, X10), add(X9, X10, T7))), SCOPE: 2, CLAUSE: 4 | ','(fib(s(T5), X9), ','(fib(T5, X10), add(X9, X10, T7))), SCOPE: 2, CLAUSE: 5\n\nT5 is ground\nX9 is free; \nX10 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
16 [label="16: ','(fib(s(T5), X9), ','(fib(T5, X10), add(X9, X10, T7))), SCOPE: 2, CLAUSE: 4\n\nT5 is ground\nX9 is free; \nX10 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
17 [label="17: ','(fib(s(T5), X9), ','(fib(T5, X10), add(X9, X10, T7))), SCOPE: 2, CLAUSE: 5\n\nT5 is ground\nX9 is free; \nX10 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
18 [label="18: ','(fib(0, X10), add(s(0), X10, T7))\n\nX10 is free", fontsize=16, style=filled, fillcolor=lightyellow];
19 [label="19: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
20 [label="20: fib(0, X10)\n\nX10 is free", fontsize=16, style=filled, fillcolor=lightyellow];
21 [label="21: add(s(0), T9, T7)\n\nT9 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
22 [label="22: fib(0, X10), SCOPE: 3, CLAUSE: 3 | fib(0, X10), SCOPE: 3, CLAUSE: 4 | fib(0, X10), SCOPE: 3, CLAUSE: 5\n\nX10 is free", fontsize=16, style=filled, fillcolor=lightyellow];
23 [label="23: fib(0, X10), SCOPE: 3, CLAUSE: 3\n\nX10 is free", fontsize=16, style=filled, fillcolor=lightyellow];
24 [label="24: fib(0, X10), SCOPE: 3, CLAUSE: 4 | fib(0, X10), SCOPE: 3, CLAUSE: 5\n\nX10 is free", fontsize=16, style=filled, fillcolor=lightyellow];
25 [label="25: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
26 [label="26: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
27 [label="27: fib(0, X10), SCOPE: 3, CLAUSE: 5\n\nX10 is free", fontsize=16, style=filled, fillcolor=lightyellow];
28 [label="28: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
29 [label="29: add(s(0), T9, T7), SCOPE: 4, CLAUSE: 0 | add(s(0), T9, T7), SCOPE: 4, CLAUSE: 1 | add(s(0), T9, T7), SCOPE: 4, CLAUSE: 2\n\nT9 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
30 [label="30: add(s(0), T9, T7), SCOPE: 4, CLAUSE: 1 | add(s(0), T9, T7), SCOPE: 4, CLAUSE: 2\n\nT9 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
31 [label="31: add(s(0), T9, T7), SCOPE: 4, CLAUSE: 1\n\nT9 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
32 [label="32: add(s(0), T9, T7), SCOPE: 4, CLAUSE: 2\n\nT9 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
33 [label="33: add(0, T20, T22)\n\nT20 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
34 [label="34: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
35 [label="35: add(0, T20, T22), SCOPE: 5, CLAUSE: 0 | add(0, T20, T22), SCOPE: 5, CLAUSE: 1 | add(0, T20, T22), SCOPE: 5, CLAUSE: 2\n\nT20 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
36 [label="36: add(0, T20, T22), SCOPE: 5, CLAUSE: 0\n\nT20 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
37 [label="37: add(0, T20, T22), SCOPE: 5, CLAUSE: 1 | add(0, T20, T22), SCOPE: 5, CLAUSE: 2\n\nT20 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
38 [label="38: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
39 [label="39: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
40 [label="40: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
41 [label="41: add(0, T20, T22), SCOPE: 5, CLAUSE: 2\n\nT20 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
42 [label="42: add(0, T27, T29)\n\nT27 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
43 [label="43: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
44 [label="44: add(s(0), T34, T36)\n\nT34 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
45 [label="45: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
46 [label="46: ','(fib(s(T41), X80), ','(fib(T41, X81), ','(add(X80, X81, X82), ','(fib(s(T41), X10), add(X82, X10, T7)))))\n\nT41 is ground\nX10 is free; \nX82 is free; \nX80 is free; \nX81 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
47 [label="47: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
48 [label="48: fib(s(T41), X80)\n\nT41 is ground\nX80 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
49 [label="49: ','(fib(T41, X81), ','(add(T42, X81, X82), ','(fib(s(T41), X10), add(X82, X10, T7))))\n\nT41 is ground\nT42 is ground\nX10 is free; \nX82 is free; \nX81 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
50 [label="50: fib(s(T41), X80), SCOPE: 6, CLAUSE: 3 | fib(s(T41), X80), SCOPE: 6, CLAUSE: 4 | fib(s(T41), X80), SCOPE: 6, CLAUSE: 5\n\nT41 is ground\nX80 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
51 [label="51: fib(s(T41), X80), SCOPE: 6, CLAUSE: 4 | fib(s(T41), X80), SCOPE: 6, CLAUSE: 5\n\nT41 is ground\nX80 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
52 [label="52: fib(s(T41), X80), SCOPE: 6, CLAUSE: 4\n\nT41 is ground\nX80 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
53 [label="53: fib(s(T41), X80), SCOPE: 6, CLAUSE: 5\n\nT41 is ground\nX80 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
54 [label="54: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
55 [label="55: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
56 [label="56: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
57 [label="57: ','(fib(s(T45), X95), ','(fib(T45, X96), add(X95, X96, X97)))\n\nT45 is ground\nX97 is free; \nX95 is free; \nX96 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
58 [label="58: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
59 [label="59: fib(s(T45), X95)\n\nT45 is ground\nX95 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
60 [label="60: ','(fib(T45, X96), add(T46, X96, X97))\n\nT45 is ground\nT46 is ground\nX97 is free; \nX96 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
61 [label="61: fib(T45, X96)\n\nT45 is ground\nX96 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
62 [label="62: add(T46, T47, X97)\n\nT46 is ground\nT47 is ground\nX97 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
63 [label="63: fib(T45, X96), SCOPE: 7, CLAUSE: 3 | fib(T45, X96), SCOPE: 7, CLAUSE: 4 | fib(T45, X96), SCOPE: 7, CLAUSE: 5\n\nT45 is ground\nX96 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
64 [label="64: fib(T45, X96), SCOPE: 7, CLAUSE: 3\n\nT45 is ground\nX96 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
65 [label="65: fib(T45, X96), SCOPE: 7, CLAUSE: 4 | fib(T45, X96), SCOPE: 7, CLAUSE: 5\n\nT45 is ground\nX96 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
66 [label="66: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
67 [label="67: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
68 [label="68: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
69 [label="69: fib(T45, X96), SCOPE: 7, CLAUSE: 4\n\nT45 is ground\nX96 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
70 [label="70: fib(T45, X96), SCOPE: 7, CLAUSE: 5\n\nT45 is ground\nX96 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
71 [label="71: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
72 [label="72: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
73 [label="73: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
74 [label="74: ','(fib(s(T50), X110), ','(fib(T50, X111), add(X110, X111, X112)))\n\nT50 is ground\nX112 is free; \nX110 is free; \nX111 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
75 [label="75: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
76 [label="76: add(T46, T47, X97), SCOPE: 8, CLAUSE: 0 | add(T46, T47, X97), SCOPE: 8, CLAUSE: 1 | add(T46, T47, X97), SCOPE: 8, CLAUSE: 2\n\nT46 is ground\nT47 is ground\nX97 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
77 [label="77: add(T46, T47, X97), SCOPE: 8, CLAUSE: 0\n\nT46 is ground\nT47 is ground\nX97 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
78 [label="78: add(T46, T47, X97), SCOPE: 8, CLAUSE: 1 | add(T46, T47, X97), SCOPE: 8, CLAUSE: 2\n\nT46 is ground\nT47 is ground\nX97 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
79 [label="79: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
80 [label="80: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
81 [label="81: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
82 [label="82: add(T46, T47, X97), SCOPE: 8, CLAUSE: 1\n\nT46 is ground\nT47 is ground\nX97 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
83 [label="83: add(T46, T47, X97), SCOPE: 8, CLAUSE: 2\n\nT46 is ground\nT47 is ground\nX97 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
84 [label="84: add(T59, T60, X134)\n\nT59 is ground\nT60 is ground\nX134 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
85 [label="85: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
86 [label="86: add(T65, T66, X149)\n\nT65 is ground\nT66 is ground\nX149 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
87 [label="87: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
88 [label="88: fib(T41, X81)\n\nT41 is ground\nX81 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
89 [label="89: ','(add(T42, T67, X82), ','(fib(s(T41), X10), add(X82, X10, T7)))\n\nT41 is ground\nT42 is ground\nT67 is ground\nX10 is free; \nX82 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
90 [label="90: add(T42, T67, X82)\n\nT42 is ground\nT67 is ground\nX82 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
91 [label="91: ','(fib(s(T41), X10), add(T68, X10, T7))\n\nT41 is ground\nT68 is ground\nX10 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
92 [label="92: fib(s(T41), X10)\n\nT41 is ground\nX10 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
93 [label="93: add(T68, T69, T7)\n\nT68 is ground\nT69 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
94 [label="94: add(T68, T69, T7), SCOPE: 9, CLAUSE: 0 | add(T68, T69, T7), SCOPE: 9, CLAUSE: 1 | add(T68, T69, T7), SCOPE: 9, CLAUSE: 2\n\nT68 is ground\nT69 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
95 [label="95: add(T68, T69, T7), SCOPE: 9, CLAUSE: 0\n\nT68 is ground\nT69 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
96 [label="96: add(T68, T69, T7), SCOPE: 9, CLAUSE: 1 | add(T68, T69, T7), SCOPE: 9, CLAUSE: 2\n\nT68 is ground\nT69 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
97 [label="97: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
98 [label="98: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
99 [label="99: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
100 [label="100: add(T68, T69, T7), SCOPE: 9, CLAUSE: 1\n\nT68 is ground\nT69 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
101 [label="101: add(T68, T69, T7), SCOPE: 9, CLAUSE: 2\n\nT68 is ground\nT69 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
102 [label="102: add(T82, T83, T85)\n\nT82 is ground\nT83 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
103 [label="103: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
104 [label="104: add(T92, T93, T95)\n\nT92 is ground\nT93 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
105 [label="105: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
106 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
1 -> 106 [arrowhead = none ];
106 -> 2;

107 [label="EVAL with clause\nfib(0, 0).\nand substitution\nT1 -> 0\nT2 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
2 -> 107 [arrowhead = none ];
107 -> 3;

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

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

110 [label="EVAL with clause\nfib(s(0), s(0)).\nand substitution\nT1 -> s(0)\nT2 -> s(0)", fontsize=14, style = filled, fillcolor = lightblue];
4 -> 110 [arrowhead = none ];
110 -> 8;

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

112 [label="BACKTRACK\nfor clause: fib(s(0), s(0))because of non-unification", fontsize=14, style = filled, fillcolor = white];
5 -> 112 [arrowhead = none ];
112 -> 6;

113 [label="BACKTRACK\nfor clause: fib(s(s(X)), N) :- ','(fib(s(X), N1), ','(fib(X, N2), add(N1, N2, N)))because of non-unification", fontsize=14, style = filled, fillcolor = white];
6 -> 113 [arrowhead = none ];
113 -> 7;

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

115 [label="EVAL with clause\nfib(s(s(X7)), X8) :- ','(fib(s(X7), X9), ','(fib(X7, X10), add(X9, X10, X8))).\nand substitution\nX7 -> T5\nT1 -> s(s(T5))\nT2 -> T7\nX8 -> T7\nT6 -> T7", fontsize=14, style = filled, fillcolor = lightblue];
9 -> 115 [arrowhead = none ];
115 -> 12;

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

117 [label="BACKTRACK\nfor clause: fib(s(s(X)), N) :- ','(fib(s(X), N1), ','(fib(X, N2), add(N1, N2, N)))because of non-unification", fontsize=14, style = filled, fillcolor = white];
10 -> 117 [arrowhead = none ];
117 -> 11;

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

119 [label="BACKTRACK\nfor clause: fib(0, 0)because of non-unification", fontsize=14, style = filled, fillcolor = white];
14 -> 119 [arrowhead = none ];
119 -> 15;

120 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
15 -> 120 [arrowhead = none ];
120 -> 16;

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

122 [label="EVAL with clause\nfib(s(0), s(0)).\nand substitution\nT5 -> 0\nX9 -> s(0)", fontsize=14, style = filled, fillcolor = lightblue];
16 -> 122 [arrowhead = none ];
122 -> 18;

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

124 [label="EVAL with clause\nfib(s(s(X78)), X79) :- ','(fib(s(X78), X80), ','(fib(X78, X81), add(X80, X81, X79))).\nand substitution\nX78 -> T41\nT5 -> s(T41)\nX9 -> X82\nX79 -> X82", fontsize=14, style = filled, fillcolor = lightblue];
17 -> 124 [arrowhead = none ];
124 -> 46;

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

126 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
18 -> 126 [arrowhead = none ];
126 -> 20;

127 [label="SPLIT 2\nnew knowledge:\nT9 is ground\nreplacements:\nX10 -> T9", fontsize=14, style = filled, fillcolor = violet];
18 -> 127 [arrowhead = none ];
127 -> 21;

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

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

130 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
22 -> 130 [arrowhead = none ];
130 -> 23;

131 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
22 -> 131 [arrowhead = none ];
131 -> 24;

132 [label="ONLY EVAL with clause\nfib(0, 0).\nand substitution\nX10 -> 0", fontsize=14, style = filled, fillcolor = white];
23 -> 132 [arrowhead = none ];
132 -> 25;

133 [label="BACKTRACK\nfor clause: fib(s(0), s(0))because of non-unification", fontsize=14, style = filled, fillcolor = white];
24 -> 133 [arrowhead = none ];
133 -> 27;

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

135 [label="BACKTRACK\nfor clause: fib(s(s(X)), N) :- ','(fib(s(X), N1), ','(fib(X, N2), add(N1, N2, N)))because of non-unification", fontsize=14, style = filled, fillcolor = white];
27 -> 135 [arrowhead = none ];
135 -> 28;

136 [label="BACKTRACK\nfor clause: add(0, 0, 0)because of non-unification", fontsize=14, style = filled, fillcolor = white];
29 -> 136 [arrowhead = none ];
136 -> 30;

137 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
30 -> 137 [arrowhead = none ];
137 -> 31;

138 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
30 -> 138 [arrowhead = none ];
138 -> 32;

139 [label="EVAL with clause\nadd(s(X34), X35, s(X36)) :- add(X34, X35, X36).\nand substitution\nX34 -> 0\nT9 -> T20\nX35 -> T20\nX36 -> T22\nT7 -> s(T22)\nT21 -> T22", fontsize=14, style = filled, fillcolor = lightblue];
31 -> 139 [arrowhead = none ];
139 -> 33;

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

141 [label="EVAL with clause\nadd(X61, s(X62), s(X63)) :- add(X61, X62, X63).\nand substitution\nX61 -> s(0)\nX62 -> T34\nT9 -> s(T34)\nX63 -> T36\nT7 -> s(T36)\nT35 -> T36", fontsize=14, style = filled, fillcolor = lightblue];
32 -> 141 [arrowhead = none ];
141 -> 44;

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

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

144 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
35 -> 144 [arrowhead = none ];
144 -> 36;

145 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
35 -> 145 [arrowhead = none ];
145 -> 37;

146 [label="EVAL with clause\nadd(0, 0, 0).\nand substitution\nT20 -> 0\nT22 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
36 -> 146 [arrowhead = none ];
146 -> 38;

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

148 [label="BACKTRACK\nfor clause: add(s(X), Y, s(N)) :- add(X, Y, N)because of non-unification", fontsize=14, style = filled, fillcolor = white];
37 -> 148 [arrowhead = none ];
148 -> 41;

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

150 [label="EVAL with clause\nadd(X49, s(X50), s(X51)) :- add(X49, X50, X51).\nand substitution\nX49 -> 0\nX50 -> T27\nT20 -> s(T27)\nX51 -> T29\nT22 -> s(T29)\nT28 -> T29", fontsize=14, style = filled, fillcolor = lightblue];
41 -> 150 [arrowhead = none ];
150 -> 42;

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

152 [label="INSTANCE with matching:\nT20 -> T27\nT22 -> T29", fontsize=14, style = filled, fillcolor = lightgrey];
42 -> 152 [arrowhead = none , style=dashed];
152 -> 33[style=dashed];

153 [label="INSTANCE with matching:\nT9 -> T34\nT7 -> T36", fontsize=14, style = filled, fillcolor = lightgrey];
44 -> 153 [arrowhead = none , style=dashed];
153 -> 21[style=dashed];

154 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
46 -> 154 [arrowhead = none ];
154 -> 48;

155 [label="SPLIT 2\nnew knowledge:\nT42 is ground\nreplacements:\nX80 -> T42", fontsize=14, style = filled, fillcolor = violet];
46 -> 155 [arrowhead = none ];
155 -> 49;

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

157 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
49 -> 157 [arrowhead = none ];
157 -> 88;

158 [label="SPLIT 2\nnew knowledge:\nT67 is ground\nreplacements:\nX81 -> T67", fontsize=14, style = filled, fillcolor = violet];
49 -> 158 [arrowhead = none ];
158 -> 89;

159 [label="BACKTRACK\nfor clause: fib(0, 0)because of non-unification", fontsize=14, style = filled, fillcolor = white];
50 -> 159 [arrowhead = none ];
159 -> 51;

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

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

162 [label="EVAL with clause\nfib(s(0), s(0)).\nand substitution\nT41 -> 0\nX80 -> s(0)", fontsize=14, style = filled, fillcolor = lightblue];
52 -> 162 [arrowhead = none ];
162 -> 54;

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

164 [label="EVAL with clause\nfib(s(s(X93)), X94) :- ','(fib(s(X93), X95), ','(fib(X93, X96), add(X95, X96, X94))).\nand substitution\nX93 -> T45\nT41 -> s(T45)\nX80 -> X97\nX94 -> X97", fontsize=14, style = filled, fillcolor = lightblue];
53 -> 164 [arrowhead = none ];
164 -> 57;

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

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

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

168 [label="SPLIT 2\nnew knowledge:\nT46 is ground\nreplacements:\nX95 -> T46", fontsize=14, style = filled, fillcolor = violet];
57 -> 168 [arrowhead = none ];
168 -> 60;

169 [label="INSTANCE with matching:\nT41 -> T45\nX80 -> X95", fontsize=14, style = filled, fillcolor = lightgrey];
59 -> 169 [arrowhead = none , style=dashed];
169 -> 48[style=dashed];

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

171 [label="SPLIT 2\nnew knowledge:\nT47 is ground\nreplacements:\nX96 -> T47", fontsize=14, style = filled, fillcolor = violet];
60 -> 171 [arrowhead = none ];
171 -> 62;

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

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

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

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

176 [label="EVAL with clause\nfib(0, 0).\nand substitution\nT45 -> 0\nX96 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
64 -> 176 [arrowhead = none ];
176 -> 66;

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

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

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

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

181 [label="EVAL with clause\nfib(s(0), s(0)).\nand substitution\nT45 -> s(0)\nX96 -> s(0)", fontsize=14, style = filled, fillcolor = lightblue];
69 -> 181 [arrowhead = none ];
181 -> 71;

182 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
69 -> 182 [arrowhead = none ];
182 -> 72;

183 [label="EVAL with clause\nfib(s(s(X108)), X109) :- ','(fib(s(X108), X110), ','(fib(X108, X111), add(X110, X111, X109))).\nand substitution\nX108 -> T50\nT45 -> s(s(T50))\nX96 -> X112\nX109 -> X112", fontsize=14, style = filled, fillcolor = lightblue];
70 -> 183 [arrowhead = none ];
183 -> 74;

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

185 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
71 -> 185 [arrowhead = none ];
185 -> 73;

186 [label="INSTANCE with matching:\nT45 -> T50\nX95 -> X110\nX96 -> X111\nX97 -> X112", fontsize=14, style = filled, fillcolor = lightgrey];
74 -> 186 [arrowhead = none , style=dashed];
186 -> 57[style=dashed];

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

188 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
76 -> 188 [arrowhead = none ];
188 -> 78;

189 [label="EVAL with clause\nadd(0, 0, 0).\nand substitution\nT46 -> 0\nT47 -> 0\nX97 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
77 -> 189 [arrowhead = none ];
189 -> 79;

190 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
77 -> 190 [arrowhead = none ];
190 -> 80;

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

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

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

194 [label="EVAL with clause\nadd(s(X131), X132, s(X133)) :- add(X131, X132, X133).\nand substitution\nX131 -> T59\nT46 -> s(T59)\nT47 -> T60\nX132 -> T60\nX133 -> X134\nX97 -> s(X134)", fontsize=14, style = filled, fillcolor = lightblue];
82 -> 194 [arrowhead = none ];
194 -> 84;

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

196 [label="EVAL with clause\nadd(X146, s(X147), s(X148)) :- add(X146, X147, X148).\nand substitution\nT46 -> T65\nX146 -> T65\nX147 -> T66\nT47 -> s(T66)\nX148 -> X149\nX97 -> s(X149)", fontsize=14, style = filled, fillcolor = lightblue];
83 -> 196 [arrowhead = none ];
196 -> 86;

197 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
83 -> 197 [arrowhead = none ];
197 -> 87;

198 [label="INSTANCE with matching:\nT46 -> T59\nT47 -> T60\nX97 -> X134", fontsize=14, style = filled, fillcolor = lightgrey];
84 -> 198 [arrowhead = none , style=dashed];
198 -> 62[style=dashed];

199 [label="INSTANCE with matching:\nT46 -> T65\nT47 -> T66\nX97 -> X149", fontsize=14, style = filled, fillcolor = lightgrey];
86 -> 199 [arrowhead = none , style=dashed];
199 -> 62[style=dashed];

200 [label="INSTANCE with matching:\nT45 -> T41\nX96 -> X81", fontsize=14, style = filled, fillcolor = lightgrey];
88 -> 200 [arrowhead = none , style=dashed];
200 -> 61[style=dashed];

201 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
89 -> 201 [arrowhead = none ];
201 -> 90;

202 [label="SPLIT 2\nnew knowledge:\nT68 is ground\nreplacements:\nX82 -> T68", fontsize=14, style = filled, fillcolor = violet];
89 -> 202 [arrowhead = none ];
202 -> 91;

203 [label="INSTANCE with matching:\nT46 -> T42\nT47 -> T67\nX97 -> X82", fontsize=14, style = filled, fillcolor = lightgrey];
90 -> 203 [arrowhead = none , style=dashed];
203 -> 62[style=dashed];

204 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
91 -> 204 [arrowhead = none ];
204 -> 92;

205 [label="SPLIT 2\nnew knowledge:\nT69 is ground\nreplacements:\nX10 -> T69", fontsize=14, style = filled, fillcolor = violet];
91 -> 205 [arrowhead = none ];
205 -> 93;

206 [label="INSTANCE with matching:\nX80 -> X10", fontsize=14, style = filled, fillcolor = lightgrey];
92 -> 206 [arrowhead = none , style=dashed];
206 -> 48[style=dashed];

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

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

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

210 [label="EVAL with clause\nadd(0, 0, 0).\nand substitution\nT68 -> 0\nT69 -> 0\nT7 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
95 -> 210 [arrowhead = none ];
210 -> 97;

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

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

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

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

215 [label="EVAL with clause\nadd(s(X165), X166, s(X167)) :- add(X165, X166, X167).\nand substitution\nX165 -> T82\nT68 -> s(T82)\nT69 -> T83\nX166 -> T83\nX167 -> T85\nT7 -> s(T85)\nT84 -> T85", fontsize=14, style = filled, fillcolor = lightblue];
100 -> 215 [arrowhead = none ];
215 -> 102;

216 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
100 -> 216 [arrowhead = none ];
216 -> 103;

217 [label="EVAL with clause\nadd(X177, s(X178), s(X179)) :- add(X177, X178, X179).\nand substitution\nT68 -> T92\nX177 -> T92\nX178 -> T93\nT69 -> s(T93)\nX179 -> T95\nT7 -> s(T95)\nT94 -> T95", fontsize=14, style = filled, fillcolor = lightblue];
101 -> 217 [arrowhead = none ];
217 -> 104;

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

219 [label="INSTANCE with matching:\nT68 -> T82\nT69 -> T83\nT7 -> T85", fontsize=14, style = filled, fillcolor = lightgrey];
102 -> 219 [arrowhead = none , style=dashed];
219 -> 93[style=dashed];

220 [label="INSTANCE with matching:\nT68 -> T92\nT69 -> T93\nT7 -> T95", fontsize=14, style = filled, fillcolor = lightgrey];
104 -> 220 [arrowhead = none , style=dashed];
220 -> 93[style=dashed];

}

(2) Obligation:

Clauses:

add33(0, 0).
add33(s(T27), s(T29)) :- add33(T27, T29).
add21(T20, s(T22)) :- add33(T20, T22).
add21(s(T34), s(T36)) :- add21(T34, T36).
fib48(0, s(0)).
fib48(s(T45), X97) :- p57(T45, X95, X96, X97).
p57(T45, X95, X96, X97) :- fib48(T45, X95).
p57(T45, T46, X96, X97) :- ','(fib48(T45, T46), fib61(T45, X96)).
p57(T45, T46, T47, X97) :- ','(fib48(T45, T46), ','(fib61(T45, T47), add62(T46, T47, X97))).
add62(0, 0, 0).
add62(s(T59), T60, s(X134)) :- add62(T59, T60, X134).
add62(T65, s(T66), s(X149)) :- add62(T65, T66, X149).
fib61(0, 0).
fib61(s(0), s(0)).
fib61(s(s(T50)), X112) :- p57(T50, X110, X111, X112).
add93(0, 0, 0).
add93(s(T82), T83, s(T85)) :- add93(T82, T83, T85).
add93(T92, s(T93), s(T95)) :- add93(T92, T93, T95).
fib20(0).
fib1(0, 0).
fib1(s(0), s(0)).
fib1(s(s(0)), T7) :- fib20(X10).
fib1(s(s(0)), T7) :- ','(fib20(T9), add21(T9, T7)).
fib1(s(s(s(T41))), T7) :- fib48(T41, X80).
fib1(s(s(s(T41))), T7) :- ','(fib48(T41, T42), fib61(T41, X81)).
fib1(s(s(s(T41))), T7) :- ','(fib48(T41, T42), ','(fib61(T41, T67), add62(T42, T67, X82))).
fib1(s(s(s(T41))), T7) :- ','(fib48(T41, T42), ','(fib61(T41, T67), ','(add62(T42, T67, T68), fib48(T41, X10)))).
fib1(s(s(s(T41))), T7) :- ','(fib48(T41, T42), ','(fib61(T41, T67), ','(add62(T42, T67, T68), ','(fib48(T41, T69), add93(T68, T69, T7))))).

Queries:

fib1(g,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:
fib1_in: (b,f)
add21_in: (b,f)
add33_in: (b,f)
fib48_in: (b,f)
p57_in: (b,f,f,f)
fib61_in: (b,f)
add62_in: (f,f,f)
add93_in: (b,f,f)
Transforming Prolog into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:

fib1_in_ga(0, 0) → fib1_out_ga(0, 0)
fib1_in_ga(s(0), s(0)) → fib1_out_ga(s(0), s(0))
fib1_in_ga(s(s(0)), T7) → U16_ga(T7, fib20_in_a(X10))
fib20_in_a(0) → fib20_out_a(0)
U16_ga(T7, fib20_out_a(X10)) → fib1_out_ga(s(s(0)), T7)
fib1_in_ga(s(s(0)), T7) → U17_ga(T7, fib20_in_a(T9))
U17_ga(T7, fib20_out_a(T9)) → U18_ga(T7, add21_in_ga(T9, T7))
add21_in_ga(T20, s(T22)) → U2_ga(T20, T22, add33_in_ga(T20, T22))
add33_in_ga(0, 0) → add33_out_ga(0, 0)
add33_in_ga(s(T27), s(T29)) → U1_ga(T27, T29, add33_in_ga(T27, T29))
U1_ga(T27, T29, add33_out_ga(T27, T29)) → add33_out_ga(s(T27), s(T29))
U2_ga(T20, T22, add33_out_ga(T20, T22)) → add21_out_ga(T20, s(T22))
add21_in_ga(s(T34), s(T36)) → U3_ga(T34, T36, add21_in_ga(T34, T36))
U3_ga(T34, T36, add21_out_ga(T34, T36)) → add21_out_ga(s(T34), s(T36))
U18_ga(T7, add21_out_ga(T9, T7)) → fib1_out_ga(s(s(0)), T7)
fib1_in_ga(s(s(s(T41))), T7) → U19_ga(T41, T7, fib48_in_ga(T41, X80))
fib48_in_ga(0, s(0)) → fib48_out_ga(0, s(0))
fib48_in_ga(s(T45), X97) → U4_ga(T45, X97, p57_in_gaaa(T45, X95, X96, X97))
p57_in_gaaa(T45, X95, X96, X97) → U5_gaaa(T45, X95, X96, X97, fib48_in_ga(T45, X95))
U5_gaaa(T45, X95, X96, X97, fib48_out_ga(T45, X95)) → p57_out_gaaa(T45, X95, X96, X97)
p57_in_gaaa(T45, T46, X96, X97) → U6_gaaa(T45, T46, X96, X97, fib48_in_ga(T45, T46))
U6_gaaa(T45, T46, X96, X97, fib48_out_ga(T45, T46)) → U7_gaaa(T45, T46, X96, X97, fib61_in_ga(T45, X96))
fib61_in_ga(0, 0) → fib61_out_ga(0, 0)
fib61_in_ga(s(0), s(0)) → fib61_out_ga(s(0), s(0))
fib61_in_ga(s(s(T50)), X112) → U13_ga(T50, X112, p57_in_gaaa(T50, X110, X111, X112))
p57_in_gaaa(T45, T46, T47, X97) → U8_gaaa(T45, T46, T47, X97, fib48_in_ga(T45, T46))
U8_gaaa(T45, T46, T47, X97, fib48_out_ga(T45, T46)) → U9_gaaa(T45, T46, T47, X97, fib61_in_ga(T45, T47))
U9_gaaa(T45, T46, T47, X97, fib61_out_ga(T45, T47)) → U10_gaaa(T45, T46, T47, X97, add62_in_aaa(T46, T47, X97))
add62_in_aaa(0, 0, 0) → add62_out_aaa(0, 0, 0)
add62_in_aaa(s(T59), T60, s(X134)) → U11_aaa(T59, T60, X134, add62_in_aaa(T59, T60, X134))
add62_in_aaa(T65, s(T66), s(X149)) → U12_aaa(T65, T66, X149, add62_in_aaa(T65, T66, X149))
U12_aaa(T65, T66, X149, add62_out_aaa(T65, T66, X149)) → add62_out_aaa(T65, s(T66), s(X149))
U11_aaa(T59, T60, X134, add62_out_aaa(T59, T60, X134)) → add62_out_aaa(s(T59), T60, s(X134))
U10_gaaa(T45, T46, T47, X97, add62_out_aaa(T46, T47, X97)) → p57_out_gaaa(T45, T46, T47, X97)
U13_ga(T50, X112, p57_out_gaaa(T50, X110, X111, X112)) → fib61_out_ga(s(s(T50)), X112)
U7_gaaa(T45, T46, X96, X97, fib61_out_ga(T45, X96)) → p57_out_gaaa(T45, T46, X96, X97)
U4_ga(T45, X97, p57_out_gaaa(T45, X95, X96, X97)) → fib48_out_ga(s(T45), X97)
U19_ga(T41, T7, fib48_out_ga(T41, X80)) → fib1_out_ga(s(s(s(T41))), T7)
fib1_in_ga(s(s(s(T41))), T7) → U20_ga(T41, T7, fib48_in_ga(T41, T42))
U20_ga(T41, T7, fib48_out_ga(T41, T42)) → U21_ga(T41, T7, fib61_in_ga(T41, X81))
U21_ga(T41, T7, fib61_out_ga(T41, X81)) → fib1_out_ga(s(s(s(T41))), T7)
U20_ga(T41, T7, fib48_out_ga(T41, T42)) → U22_ga(T41, T7, T42, fib61_in_ga(T41, T67))
U22_ga(T41, T7, T42, fib61_out_ga(T41, T67)) → U23_ga(T41, T7, add62_in_aaa(T42, T67, X82))
U23_ga(T41, T7, add62_out_aaa(T42, T67, X82)) → fib1_out_ga(s(s(s(T41))), T7)
U22_ga(T41, T7, T42, fib61_out_ga(T41, T67)) → U24_ga(T41, T7, add62_in_aaa(T42, T67, T68))
U24_ga(T41, T7, add62_out_aaa(T42, T67, T68)) → U25_ga(T41, T7, fib48_in_ga(T41, X10))
U25_ga(T41, T7, fib48_out_ga(T41, X10)) → fib1_out_ga(s(s(s(T41))), T7)
U24_ga(T41, T7, add62_out_aaa(T42, T67, T68)) → U26_ga(T41, T7, T68, fib48_in_ga(T41, T69))
U26_ga(T41, T7, T68, fib48_out_ga(T41, T69)) → U27_ga(T41, T7, add93_in_gaa(T68, T69, T7))
add93_in_gaa(0, 0, 0) → add93_out_gaa(0, 0, 0)
add93_in_gaa(s(T82), T83, s(T85)) → U14_gaa(T82, T83, T85, add93_in_gaa(T82, T83, T85))
add93_in_gaa(T92, s(T93), s(T95)) → U15_gaa(T92, T93, T95, add93_in_gaa(T92, T93, T95))
U15_gaa(T92, T93, T95, add93_out_gaa(T92, T93, T95)) → add93_out_gaa(T92, s(T93), s(T95))
U14_gaa(T82, T83, T85, add93_out_gaa(T82, T83, T85)) → add93_out_gaa(s(T82), T83, s(T85))
U27_ga(T41, T7, add93_out_gaa(T68, T69, T7)) → fib1_out_ga(s(s(s(T41))), T7)

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog

(4) Obligation:

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

fib1_in_ga(0, 0) → fib1_out_ga(0, 0)
fib1_in_ga(s(0), s(0)) → fib1_out_ga(s(0), s(0))
fib1_in_ga(s(s(0)), T7) → U16_ga(T7, fib20_in_a(X10))
fib20_in_a(0) → fib20_out_a(0)
U16_ga(T7, fib20_out_a(X10)) → fib1_out_ga(s(s(0)), T7)
fib1_in_ga(s(s(0)), T7) → U17_ga(T7, fib20_in_a(T9))
U17_ga(T7, fib20_out_a(T9)) → U18_ga(T7, add21_in_ga(T9, T7))
add21_in_ga(T20, s(T22)) → U2_ga(T20, T22, add33_in_ga(T20, T22))
add33_in_ga(0, 0) → add33_out_ga(0, 0)
add33_in_ga(s(T27), s(T29)) → U1_ga(T27, T29, add33_in_ga(T27, T29))
U1_ga(T27, T29, add33_out_ga(T27, T29)) → add33_out_ga(s(T27), s(T29))
U2_ga(T20, T22, add33_out_ga(T20, T22)) → add21_out_ga(T20, s(T22))
add21_in_ga(s(T34), s(T36)) → U3_ga(T34, T36, add21_in_ga(T34, T36))
U3_ga(T34, T36, add21_out_ga(T34, T36)) → add21_out_ga(s(T34), s(T36))
U18_ga(T7, add21_out_ga(T9, T7)) → fib1_out_ga(s(s(0)), T7)
fib1_in_ga(s(s(s(T41))), T7) → U19_ga(T41, T7, fib48_in_ga(T41, X80))
fib48_in_ga(0, s(0)) → fib48_out_ga(0, s(0))
fib48_in_ga(s(T45), X97) → U4_ga(T45, X97, p57_in_gaaa(T45, X95, X96, X97))
p57_in_gaaa(T45, X95, X96, X97) → U5_gaaa(T45, X95, X96, X97, fib48_in_ga(T45, X95))
U5_gaaa(T45, X95, X96, X97, fib48_out_ga(T45, X95)) → p57_out_gaaa(T45, X95, X96, X97)
p57_in_gaaa(T45, T46, X96, X97) → U6_gaaa(T45, T46, X96, X97, fib48_in_ga(T45, T46))
U6_gaaa(T45, T46, X96, X97, fib48_out_ga(T45, T46)) → U7_gaaa(T45, T46, X96, X97, fib61_in_ga(T45, X96))
fib61_in_ga(0, 0) → fib61_out_ga(0, 0)
fib61_in_ga(s(0), s(0)) → fib61_out_ga(s(0), s(0))
fib61_in_ga(s(s(T50)), X112) → U13_ga(T50, X112, p57_in_gaaa(T50, X110, X111, X112))
p57_in_gaaa(T45, T46, T47, X97) → U8_gaaa(T45, T46, T47, X97, fib48_in_ga(T45, T46))
U8_gaaa(T45, T46, T47, X97, fib48_out_ga(T45, T46)) → U9_gaaa(T45, T46, T47, X97, fib61_in_ga(T45, T47))
U9_gaaa(T45, T46, T47, X97, fib61_out_ga(T45, T47)) → U10_gaaa(T45, T46, T47, X97, add62_in_aaa(T46, T47, X97))
add62_in_aaa(0, 0, 0) → add62_out_aaa(0, 0, 0)
add62_in_aaa(s(T59), T60, s(X134)) → U11_aaa(T59, T60, X134, add62_in_aaa(T59, T60, X134))
add62_in_aaa(T65, s(T66), s(X149)) → U12_aaa(T65, T66, X149, add62_in_aaa(T65, T66, X149))
U12_aaa(T65, T66, X149, add62_out_aaa(T65, T66, X149)) → add62_out_aaa(T65, s(T66), s(X149))
U11_aaa(T59, T60, X134, add62_out_aaa(T59, T60, X134)) → add62_out_aaa(s(T59), T60, s(X134))
U10_gaaa(T45, T46, T47, X97, add62_out_aaa(T46, T47, X97)) → p57_out_gaaa(T45, T46, T47, X97)
U13_ga(T50, X112, p57_out_gaaa(T50, X110, X111, X112)) → fib61_out_ga(s(s(T50)), X112)
U7_gaaa(T45, T46, X96, X97, fib61_out_ga(T45, X96)) → p57_out_gaaa(T45, T46, X96, X97)
U4_ga(T45, X97, p57_out_gaaa(T45, X95, X96, X97)) → fib48_out_ga(s(T45), X97)
U19_ga(T41, T7, fib48_out_ga(T41, X80)) → fib1_out_ga(s(s(s(T41))), T7)
fib1_in_ga(s(s(s(T41))), T7) → U20_ga(T41, T7, fib48_in_ga(T41, T42))
U20_ga(T41, T7, fib48_out_ga(T41, T42)) → U21_ga(T41, T7, fib61_in_ga(T41, X81))
U21_ga(T41, T7, fib61_out_ga(T41, X81)) → fib1_out_ga(s(s(s(T41))), T7)
U20_ga(T41, T7, fib48_out_ga(T41, T42)) → U22_ga(T41, T7, T42, fib61_in_ga(T41, T67))
U22_ga(T41, T7, T42, fib61_out_ga(T41, T67)) → U23_ga(T41, T7, add62_in_aaa(T42, T67, X82))
U23_ga(T41, T7, add62_out_aaa(T42, T67, X82)) → fib1_out_ga(s(s(s(T41))), T7)
U22_ga(T41, T7, T42, fib61_out_ga(T41, T67)) → U24_ga(T41, T7, add62_in_aaa(T42, T67, T68))
U24_ga(T41, T7, add62_out_aaa(T42, T67, T68)) → U25_ga(T41, T7, fib48_in_ga(T41, X10))
U25_ga(T41, T7, fib48_out_ga(T41, X10)) → fib1_out_ga(s(s(s(T41))), T7)
U24_ga(T41, T7, add62_out_aaa(T42, T67, T68)) → U26_ga(T41, T7, T68, fib48_in_ga(T41, T69))
U26_ga(T41, T7, T68, fib48_out_ga(T41, T69)) → U27_ga(T41, T7, add93_in_gaa(T68, T69, T7))
add93_in_gaa(0, 0, 0) → add93_out_gaa(0, 0, 0)
add93_in_gaa(s(T82), T83, s(T85)) → U14_gaa(T82, T83, T85, add93_in_gaa(T82, T83, T85))
add93_in_gaa(T92, s(T93), s(T95)) → U15_gaa(T92, T93, T95, add93_in_gaa(T92, T93, T95))
U15_gaa(T92, T93, T95, add93_out_gaa(T92, T93, T95)) → add93_out_gaa(T92, s(T93), s(T95))
U14_gaa(T82, T83, T85, add93_out_gaa(T82, T83, T85)) → add93_out_gaa(s(T82), T83, s(T85))
U27_ga(T41, T7, add93_out_gaa(T68, T69, T7)) → fib1_out_ga(s(s(s(T41))), T7)

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

FIB1_IN_GA(s(s(0)), T7) → U16_GA(T7, fib20_in_a(X10))
FIB1_IN_GA(s(s(0)), T7) → FIB20_IN_A(X10)
FIB1_IN_GA(s(s(0)), T7) → U17_GA(T7, fib20_in_a(T9))
U17_GA(T7, fib20_out_a(T9)) → U18_GA(T7, add21_in_ga(T9, T7))
U17_GA(T7, fib20_out_a(T9)) → ADD21_IN_GA(T9, T7)
ADD21_IN_GA(T20, s(T22)) → U2_GA(T20, T22, add33_in_ga(T20, T22))
ADD21_IN_GA(T20, s(T22)) → ADD33_IN_GA(T20, T22)
ADD33_IN_GA(s(T27), s(T29)) → U1_GA(T27, T29, add33_in_ga(T27, T29))
ADD33_IN_GA(s(T27), s(T29)) → ADD33_IN_GA(T27, T29)
ADD21_IN_GA(s(T34), s(T36)) → U3_GA(T34, T36, add21_in_ga(T34, T36))
ADD21_IN_GA(s(T34), s(T36)) → ADD21_IN_GA(T34, T36)
FIB1_IN_GA(s(s(s(T41))), T7) → U19_GA(T41, T7, fib48_in_ga(T41, X80))
FIB1_IN_GA(s(s(s(T41))), T7) → FIB48_IN_GA(T41, X80)
FIB48_IN_GA(s(T45), X97) → U4_GA(T45, X97, p57_in_gaaa(T45, X95, X96, X97))
FIB48_IN_GA(s(T45), X97) → P57_IN_GAAA(T45, X95, X96, X97)
P57_IN_GAAA(T45, X95, X96, X97) → U5_GAAA(T45, X95, X96, X97, fib48_in_ga(T45, X95))
P57_IN_GAAA(T45, X95, X96, X97) → FIB48_IN_GA(T45, X95)
P57_IN_GAAA(T45, T46, X96, X97) → U6_GAAA(T45, T46, X96, X97, fib48_in_ga(T45, T46))
U6_GAAA(T45, T46, X96, X97, fib48_out_ga(T45, T46)) → U7_GAAA(T45, T46, X96, X97, fib61_in_ga(T45, X96))
U6_GAAA(T45, T46, X96, X97, fib48_out_ga(T45, T46)) → FIB61_IN_GA(T45, X96)
FIB61_IN_GA(s(s(T50)), X112) → U13_GA(T50, X112, p57_in_gaaa(T50, X110, X111, X112))
FIB61_IN_GA(s(s(T50)), X112) → P57_IN_GAAA(T50, X110, X111, X112)
P57_IN_GAAA(T45, T46, T47, X97) → U8_GAAA(T45, T46, T47, X97, fib48_in_ga(T45, T46))
U8_GAAA(T45, T46, T47, X97, fib48_out_ga(T45, T46)) → U9_GAAA(T45, T46, T47, X97, fib61_in_ga(T45, T47))
U8_GAAA(T45, T46, T47, X97, fib48_out_ga(T45, T46)) → FIB61_IN_GA(T45, T47)
U9_GAAA(T45, T46, T47, X97, fib61_out_ga(T45, T47)) → U10_GAAA(T45, T46, T47, X97, add62_in_aaa(T46, T47, X97))
U9_GAAA(T45, T46, T47, X97, fib61_out_ga(T45, T47)) → ADD62_IN_AAA(T46, T47, X97)
ADD62_IN_AAA(s(T59), T60, s(X134)) → U11_AAA(T59, T60, X134, add62_in_aaa(T59, T60, X134))
ADD62_IN_AAA(s(T59), T60, s(X134)) → ADD62_IN_AAA(T59, T60, X134)
ADD62_IN_AAA(T65, s(T66), s(X149)) → U12_AAA(T65, T66, X149, add62_in_aaa(T65, T66, X149))
ADD62_IN_AAA(T65, s(T66), s(X149)) → ADD62_IN_AAA(T65, T66, X149)
FIB1_IN_GA(s(s(s(T41))), T7) → U20_GA(T41, T7, fib48_in_ga(T41, T42))
U20_GA(T41, T7, fib48_out_ga(T41, T42)) → U21_GA(T41, T7, fib61_in_ga(T41, X81))
U20_GA(T41, T7, fib48_out_ga(T41, T42)) → FIB61_IN_GA(T41, X81)
U20_GA(T41, T7, fib48_out_ga(T41, T42)) → U22_GA(T41, T7, T42, fib61_in_ga(T41, T67))
U22_GA(T41, T7, T42, fib61_out_ga(T41, T67)) → U23_GA(T41, T7, add62_in_aaa(T42, T67, X82))
U22_GA(T41, T7, T42, fib61_out_ga(T41, T67)) → ADD62_IN_AAA(T42, T67, X82)
U22_GA(T41, T7, T42, fib61_out_ga(T41, T67)) → U24_GA(T41, T7, add62_in_aaa(T42, T67, T68))
U24_GA(T41, T7, add62_out_aaa(T42, T67, T68)) → U25_GA(T41, T7, fib48_in_ga(T41, X10))
U24_GA(T41, T7, add62_out_aaa(T42, T67, T68)) → FIB48_IN_GA(T41, X10)
U24_GA(T41, T7, add62_out_aaa(T42, T67, T68)) → U26_GA(T41, T7, T68, fib48_in_ga(T41, T69))
U26_GA(T41, T7, T68, fib48_out_ga(T41, T69)) → U27_GA(T41, T7, add93_in_gaa(T68, T69, T7))
U26_GA(T41, T7, T68, fib48_out_ga(T41, T69)) → ADD93_IN_GAA(T68, T69, T7)
ADD93_IN_GAA(s(T82), T83, s(T85)) → U14_GAA(T82, T83, T85, add93_in_gaa(T82, T83, T85))
ADD93_IN_GAA(s(T82), T83, s(T85)) → ADD93_IN_GAA(T82, T83, T85)
ADD93_IN_GAA(T92, s(T93), s(T95)) → U15_GAA(T92, T93, T95, add93_in_gaa(T92, T93, T95))
ADD93_IN_GAA(T92, s(T93), s(T95)) → ADD93_IN_GAA(T92, T93, T95)

The TRS R consists of the following rules:

fib1_in_ga(0, 0) → fib1_out_ga(0, 0)
fib1_in_ga(s(0), s(0)) → fib1_out_ga(s(0), s(0))
fib1_in_ga(s(s(0)), T7) → U16_ga(T7, fib20_in_a(X10))
fib20_in_a(0) → fib20_out_a(0)
U16_ga(T7, fib20_out_a(X10)) → fib1_out_ga(s(s(0)), T7)
fib1_in_ga(s(s(0)), T7) → U17_ga(T7, fib20_in_a(T9))
U17_ga(T7, fib20_out_a(T9)) → U18_ga(T7, add21_in_ga(T9, T7))
add21_in_ga(T20, s(T22)) → U2_ga(T20, T22, add33_in_ga(T20, T22))
add33_in_ga(0, 0) → add33_out_ga(0, 0)
add33_in_ga(s(T27), s(T29)) → U1_ga(T27, T29, add33_in_ga(T27, T29))
U1_ga(T27, T29, add33_out_ga(T27, T29)) → add33_out_ga(s(T27), s(T29))
U2_ga(T20, T22, add33_out_ga(T20, T22)) → add21_out_ga(T20, s(T22))
add21_in_ga(s(T34), s(T36)) → U3_ga(T34, T36, add21_in_ga(T34, T36))
U3_ga(T34, T36, add21_out_ga(T34, T36)) → add21_out_ga(s(T34), s(T36))
U18_ga(T7, add21_out_ga(T9, T7)) → fib1_out_ga(s(s(0)), T7)
fib1_in_ga(s(s(s(T41))), T7) → U19_ga(T41, T7, fib48_in_ga(T41, X80))
fib48_in_ga(0, s(0)) → fib48_out_ga(0, s(0))
fib48_in_ga(s(T45), X97) → U4_ga(T45, X97, p57_in_gaaa(T45, X95, X96, X97))
p57_in_gaaa(T45, X95, X96, X97) → U5_gaaa(T45, X95, X96, X97, fib48_in_ga(T45, X95))
U5_gaaa(T45, X95, X96, X97, fib48_out_ga(T45, X95)) → p57_out_gaaa(T45, X95, X96, X97)
p57_in_gaaa(T45, T46, X96, X97) → U6_gaaa(T45, T46, X96, X97, fib48_in_ga(T45, T46))
U6_gaaa(T45, T46, X96, X97, fib48_out_ga(T45, T46)) → U7_gaaa(T45, T46, X96, X97, fib61_in_ga(T45, X96))
fib61_in_ga(0, 0) → fib61_out_ga(0, 0)
fib61_in_ga(s(0), s(0)) → fib61_out_ga(s(0), s(0))
fib61_in_ga(s(s(T50)), X112) → U13_ga(T50, X112, p57_in_gaaa(T50, X110, X111, X112))
p57_in_gaaa(T45, T46, T47, X97) → U8_gaaa(T45, T46, T47, X97, fib48_in_ga(T45, T46))
U8_gaaa(T45, T46, T47, X97, fib48_out_ga(T45, T46)) → U9_gaaa(T45, T46, T47, X97, fib61_in_ga(T45, T47))
U9_gaaa(T45, T46, T47, X97, fib61_out_ga(T45, T47)) → U10_gaaa(T45, T46, T47, X97, add62_in_aaa(T46, T47, X97))
add62_in_aaa(0, 0, 0) → add62_out_aaa(0, 0, 0)
add62_in_aaa(s(T59), T60, s(X134)) → U11_aaa(T59, T60, X134, add62_in_aaa(T59, T60, X134))
add62_in_aaa(T65, s(T66), s(X149)) → U12_aaa(T65, T66, X149, add62_in_aaa(T65, T66, X149))
U12_aaa(T65, T66, X149, add62_out_aaa(T65, T66, X149)) → add62_out_aaa(T65, s(T66), s(X149))
U11_aaa(T59, T60, X134, add62_out_aaa(T59, T60, X134)) → add62_out_aaa(s(T59), T60, s(X134))
U10_gaaa(T45, T46, T47, X97, add62_out_aaa(T46, T47, X97)) → p57_out_gaaa(T45, T46, T47, X97)
U13_ga(T50, X112, p57_out_gaaa(T50, X110, X111, X112)) → fib61_out_ga(s(s(T50)), X112)
U7_gaaa(T45, T46, X96, X97, fib61_out_ga(T45, X96)) → p57_out_gaaa(T45, T46, X96, X97)
U4_ga(T45, X97, p57_out_gaaa(T45, X95, X96, X97)) → fib48_out_ga(s(T45), X97)
U19_ga(T41, T7, fib48_out_ga(T41, X80)) → fib1_out_ga(s(s(s(T41))), T7)
fib1_in_ga(s(s(s(T41))), T7) → U20_ga(T41, T7, fib48_in_ga(T41, T42))
U20_ga(T41, T7, fib48_out_ga(T41, T42)) → U21_ga(T41, T7, fib61_in_ga(T41, X81))
U21_ga(T41, T7, fib61_out_ga(T41, X81)) → fib1_out_ga(s(s(s(T41))), T7)
U20_ga(T41, T7, fib48_out_ga(T41, T42)) → U22_ga(T41, T7, T42, fib61_in_ga(T41, T67))
U22_ga(T41, T7, T42, fib61_out_ga(T41, T67)) → U23_ga(T41, T7, add62_in_aaa(T42, T67, X82))
U23_ga(T41, T7, add62_out_aaa(T42, T67, X82)) → fib1_out_ga(s(s(s(T41))), T7)
U22_ga(T41, T7, T42, fib61_out_ga(T41, T67)) → U24_ga(T41, T7, add62_in_aaa(T42, T67, T68))
U24_ga(T41, T7, add62_out_aaa(T42, T67, T68)) → U25_ga(T41, T7, fib48_in_ga(T41, X10))
U25_ga(T41, T7, fib48_out_ga(T41, X10)) → fib1_out_ga(s(s(s(T41))), T7)
U24_ga(T41, T7, add62_out_aaa(T42, T67, T68)) → U26_ga(T41, T7, T68, fib48_in_ga(T41, T69))
U26_ga(T41, T7, T68, fib48_out_ga(T41, T69)) → U27_ga(T41, T7, add93_in_gaa(T68, T69, T7))
add93_in_gaa(0, 0, 0) → add93_out_gaa(0, 0, 0)
add93_in_gaa(s(T82), T83, s(T85)) → U14_gaa(T82, T83, T85, add93_in_gaa(T82, T83, T85))
add93_in_gaa(T92, s(T93), s(T95)) → U15_gaa(T92, T93, T95, add93_in_gaa(T92, T93, T95))
U15_gaa(T92, T93, T95, add93_out_gaa(T92, T93, T95)) → add93_out_gaa(T92, s(T93), s(T95))
U14_gaa(T82, T83, T85, add93_out_gaa(T82, T83, T85)) → add93_out_gaa(s(T82), T83, s(T85))
U27_ga(T41, T7, add93_out_gaa(T68, T69, T7)) → fib1_out_ga(s(s(s(T41))), T7)

The argument filtering Pi contains the following mapping:
fib1_in_ga(x1, x2) = fib1_in_ga(x1)
0 = 0
fib1_out_ga(x1, x2) = fib1_out_ga(x1)
s(x1) = s(x1)
U16_ga(x1, x2) = U16_ga(x2)
fib20_in_a(x1) = fib20_in_a
fib20_out_a(x1) = fib20_out_a(x1)
U17_ga(x1, x2) = U17_ga(x2)
U18_ga(x1, x2) = U18_ga(x2)
add21_in_ga(x1, x2) = add21_in_ga(x1)
U2_ga(x1, x2, x3) = U2_ga(x1, x3)
add33_in_ga(x1, x2) = add33_in_ga(x1)
add33_out_ga(x1, x2) = add33_out_ga(x1, x2)
U1_ga(x1, x2, x3) = U1_ga(x1, x3)
add21_out_ga(x1, x2) = add21_out_ga(x1, x2)
U3_ga(x1, x2, x3) = U3_ga(x1, x3)
U19_ga(x1, x2, x3) = U19_ga(x1, x3)
fib48_in_ga(x1, x2) = fib48_in_ga(x1)
fib48_out_ga(x1, x2) = fib48_out_ga(x1)
U4_ga(x1, x2, x3) = U4_ga(x1, x3)
p57_in_gaaa(x1, x2, x3, x4) = p57_in_gaaa(x1)
U5_gaaa(x1, x2, x3, x4, x5) = U5_gaaa(x1, x5)
p57_out_gaaa(x1, x2, x3, x4) = p57_out_gaaa(x1)
U6_gaaa(x1, x2, x3, x4, x5) = U6_gaaa(x1, x5)
U7_gaaa(x1, x2, x3, x4, x5) = U7_gaaa(x1, x5)
fib61_in_ga(x1, x2) = fib61_in_ga(x1)
fib61_out_ga(x1, x2) = fib61_out_ga(x1)
U13_ga(x1, x2, x3) = U13_ga(x1, x3)
U8_gaaa(x1, x2, x3, x4, x5) = U8_gaaa(x1, x5)
U9_gaaa(x1, x2, x3, x4, x5) = U9_gaaa(x1, x5)
U10_gaaa(x1, x2, x3, x4, x5) = U10_gaaa(x1, x5)
add62_in_aaa(x1, x2, x3) = add62_in_aaa
add62_out_aaa(x1, x2, x3) = add62_out_aaa(x1, x2, x3)
U11_aaa(x1, x2, x3, x4) = U11_aaa(x4)
U12_aaa(x1, x2, x3, x4) = U12_aaa(x4)
U20_ga(x1, x2, x3) = U20_ga(x1, x3)
U21_ga(x1, x2, x3) = U21_ga(x1, x3)
U22_ga(x1, x2, x3, x4) = U22_ga(x1, x4)
U23_ga(x1, x2, x3) = U23_ga(x1, x3)
U24_ga(x1, x2, x3) = U24_ga(x1, x3)
U25_ga(x1, x2, x3) = U25_ga(x1, x3)
U26_ga(x1, x2, x3, x4) = U26_ga(x1, x3, x4)
U27_ga(x1, x2, x3) = U27_ga(x1, x3)
add93_in_gaa(x1, x2, x3) = add93_in_gaa(x1)
add93_out_gaa(x1, x2, x3) = add93_out_gaa(x1, x2, x3)
U14_gaa(x1, x2, x3, x4) = U14_gaa(x1, x4)
U15_gaa(x1, x2, x3, x4) = U15_gaa(x1, x4)
FIB1_IN_GA(x1, x2) = FIB1_IN_GA(x1)
U16_GA(x1, x2) = U16_GA(x2)
FIB20_IN_A(x1) = FIB20_IN_A
U17_GA(x1, x2) = U17_GA(x2)
U18_GA(x1, x2) = U18_GA(x2)
ADD21_IN_GA(x1, x2) = ADD21_IN_GA(x1)
U2_GA(x1, x2, x3) = U2_GA(x1, x3)
ADD33_IN_GA(x1, x2) = ADD33_IN_GA(x1)
U1_GA(x1, x2, x3) = U1_GA(x1, x3)
U3_GA(x1, x2, x3) = U3_GA(x1, x3)
U19_GA(x1, x2, x3) = U19_GA(x1, x3)
FIB48_IN_GA(x1, x2) = FIB48_IN_GA(x1)
U4_GA(x1, x2, x3) = U4_GA(x1, x3)
P57_IN_GAAA(x1, x2, x3, x4) = P57_IN_GAAA(x1)
U5_GAAA(x1, x2, x3, x4, x5) = U5_GAAA(x1, x5)
U6_GAAA(x1, x2, x3, x4, x5) = U6_GAAA(x1, x5)
U7_GAAA(x1, x2, x3, x4, x5) = U7_GAAA(x1, x5)
FIB61_IN_GA(x1, x2) = FIB61_IN_GA(x1)
U13_GA(x1, x2, x3) = U13_GA(x1, x3)
U8_GAAA(x1, x2, x3, x4, x5) = U8_GAAA(x1, x5)
U9_GAAA(x1, x2, x3, x4, x5) = U9_GAAA(x1, x5)
U10_GAAA(x1, x2, x3, x4, x5) = U10_GAAA(x1, x5)
ADD62_IN_AAA(x1, x2, x3) = ADD62_IN_AAA
U11_AAA(x1, x2, x3, x4) = U11_AAA(x4)
U12_AAA(x1, x2, x3, x4) = U12_AAA(x4)
U20_GA(x1, x2, x3) = U20_GA(x1, x3)
U21_GA(x1, x2, x3) = U21_GA(x1, x3)
U22_GA(x1, x2, x3, x4) = U22_GA(x1, x4)
U23_GA(x1, x2, x3) = U23_GA(x1, x3)
U24_GA(x1, x2, x3) = U24_GA(x1, x3)
U25_GA(x1, x2, x3) = U25_GA(x1, x3)
U26_GA(x1, x2, x3, x4) = U26_GA(x1, x3, x4)
U27_GA(x1, x2, x3) = U27_GA(x1, x3)
ADD93_IN_GAA(x1, x2, x3) = ADD93_IN_GAA(x1)
U14_GAA(x1, x2, x3, x4) = U14_GAA(x1, x4)
U15_GAA(x1, x2, x3, x4) = U15_GAA(x1, x4)

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

(6) Obligation:

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

FIB1_IN_GA(s(s(0)), T7) → U16_GA(T7, fib20_in_a(X10))
FIB1_IN_GA(s(s(0)), T7) → FIB20_IN_A(X10)
FIB1_IN_GA(s(s(0)), T7) → U17_GA(T7, fib20_in_a(T9))
U17_GA(T7, fib20_out_a(T9)) → U18_GA(T7, add21_in_ga(T9, T7))
U17_GA(T7, fib20_out_a(T9)) → ADD21_IN_GA(T9, T7)
ADD21_IN_GA(T20, s(T22)) → U2_GA(T20, T22, add33_in_ga(T20, T22))
ADD21_IN_GA(T20, s(T22)) → ADD33_IN_GA(T20, T22)
ADD33_IN_GA(s(T27), s(T29)) → U1_GA(T27, T29, add33_in_ga(T27, T29))
ADD33_IN_GA(s(T27), s(T29)) → ADD33_IN_GA(T27, T29)
ADD21_IN_GA(s(T34), s(T36)) → U3_GA(T34, T36, add21_in_ga(T34, T36))
ADD21_IN_GA(s(T34), s(T36)) → ADD21_IN_GA(T34, T36)
FIB1_IN_GA(s(s(s(T41))), T7) → U19_GA(T41, T7, fib48_in_ga(T41, X80))
FIB1_IN_GA(s(s(s(T41))), T7) → FIB48_IN_GA(T41, X80)
FIB48_IN_GA(s(T45), X97) → U4_GA(T45, X97, p57_in_gaaa(T45, X95, X96, X97))
FIB48_IN_GA(s(T45), X97) → P57_IN_GAAA(T45, X95, X96, X97)
P57_IN_GAAA(T45, X95, X96, X97) → U5_GAAA(T45, X95, X96, X97, fib48_in_ga(T45, X95))
P57_IN_GAAA(T45, X95, X96, X97) → FIB48_IN_GA(T45, X95)
P57_IN_GAAA(T45, T46, X96, X97) → U6_GAAA(T45, T46, X96, X97, fib48_in_ga(T45, T46))
U6_GAAA(T45, T46, X96, X97, fib48_out_ga(T45, T46)) → U7_GAAA(T45, T46, X96, X97, fib61_in_ga(T45, X96))
U6_GAAA(T45, T46, X96, X97, fib48_out_ga(T45, T46)) → FIB61_IN_GA(T45, X96)
FIB61_IN_GA(s(s(T50)), X112) → U13_GA(T50, X112, p57_in_gaaa(T50, X110, X111, X112))
FIB61_IN_GA(s(s(T50)), X112) → P57_IN_GAAA(T50, X110, X111, X112)
P57_IN_GAAA(T45, T46, T47, X97) → U8_GAAA(T45, T46, T47, X97, fib48_in_ga(T45, T46))
U8_GAAA(T45, T46, T47, X97, fib48_out_ga(T45, T46)) → U9_GAAA(T45, T46, T47, X97, fib61_in_ga(T45, T47))
U8_GAAA(T45, T46, T47, X97, fib48_out_ga(T45, T46)) → FIB61_IN_GA(T45, T47)
U9_GAAA(T45, T46, T47, X97, fib61_out_ga(T45, T47)) → U10_GAAA(T45, T46, T47, X97, add62_in_aaa(T46, T47, X97))
U9_GAAA(T45, T46, T47, X97, fib61_out_ga(T45, T47)) → ADD62_IN_AAA(T46, T47, X97)
ADD62_IN_AAA(s(T59), T60, s(X134)) → U11_AAA(T59, T60, X134, add62_in_aaa(T59, T60, X134))
ADD62_IN_AAA(s(T59), T60, s(X134)) → ADD62_IN_AAA(T59, T60, X134)
ADD62_IN_AAA(T65, s(T66), s(X149)) → U12_AAA(T65, T66, X149, add62_in_aaa(T65, T66, X149))
ADD62_IN_AAA(T65, s(T66), s(X149)) → ADD62_IN_AAA(T65, T66, X149)
FIB1_IN_GA(s(s(s(T41))), T7) → U20_GA(T41, T7, fib48_in_ga(T41, T42))
U20_GA(T41, T7, fib48_out_ga(T41, T42)) → U21_GA(T41, T7, fib61_in_ga(T41, X81))
U20_GA(T41, T7, fib48_out_ga(T41, T42)) → FIB61_IN_GA(T41, X81)
U20_GA(T41, T7, fib48_out_ga(T41, T42)) → U22_GA(T41, T7, T42, fib61_in_ga(T41, T67))
U22_GA(T41, T7, T42, fib61_out_ga(T41, T67)) → U23_GA(T41, T7, add62_in_aaa(T42, T67, X82))
U22_GA(T41, T7, T42, fib61_out_ga(T41, T67)) → ADD62_IN_AAA(T42, T67, X82)
U22_GA(T41, T7, T42, fib61_out_ga(T41, T67)) → U24_GA(T41, T7, add62_in_aaa(T42, T67, T68))
U24_GA(T41, T7, add62_out_aaa(T42, T67, T68)) → U25_GA(T41, T7, fib48_in_ga(T41, X10))
U24_GA(T41, T7, add62_out_aaa(T42, T67, T68)) → FIB48_IN_GA(T41, X10)
U24_GA(T41, T7, add62_out_aaa(T42, T67, T68)) → U26_GA(T41, T7, T68, fib48_in_ga(T41, T69))
U26_GA(T41, T7, T68, fib48_out_ga(T41, T69)) → U27_GA(T41, T7, add93_in_gaa(T68, T69, T7))
U26_GA(T41, T7, T68, fib48_out_ga(T41, T69)) → ADD93_IN_GAA(T68, T69, T7)
ADD93_IN_GAA(s(T82), T83, s(T85)) → U14_GAA(T82, T83, T85, add93_in_gaa(T82, T83, T85))
ADD93_IN_GAA(s(T82), T83, s(T85)) → ADD93_IN_GAA(T82, T83, T85)
ADD93_IN_GAA(T92, s(T93), s(T95)) → U15_GAA(T92, T93, T95, add93_in_gaa(T92, T93, T95))
ADD93_IN_GAA(T92, s(T93), s(T95)) → ADD93_IN_GAA(T92, T93, T95)

The TRS R consists of the following rules:

fib1_in_ga(0, 0) → fib1_out_ga(0, 0)
fib1_in_ga(s(0), s(0)) → fib1_out_ga(s(0), s(0))
fib1_in_ga(s(s(0)), T7) → U16_ga(T7, fib20_in_a(X10))
fib20_in_a(0) → fib20_out_a(0)
U16_ga(T7, fib20_out_a(X10)) → fib1_out_ga(s(s(0)), T7)
fib1_in_ga(s(s(0)), T7) → U17_ga(T7, fib20_in_a(T9))
U17_ga(T7, fib20_out_a(T9)) → U18_ga(T7, add21_in_ga(T9, T7))
add21_in_ga(T20, s(T22)) → U2_ga(T20, T22, add33_in_ga(T20, T22))
add33_in_ga(0, 0) → add33_out_ga(0, 0)
add33_in_ga(s(T27), s(T29)) → U1_ga(T27, T29, add33_in_ga(T27, T29))
U1_ga(T27, T29, add33_out_ga(T27, T29)) → add33_out_ga(s(T27), s(T29))
U2_ga(T20, T22, add33_out_ga(T20, T22)) → add21_out_ga(T20, s(T22))
add21_in_ga(s(T34), s(T36)) → U3_ga(T34, T36, add21_in_ga(T34, T36))
U3_ga(T34, T36, add21_out_ga(T34, T36)) → add21_out_ga(s(T34), s(T36))
U18_ga(T7, add21_out_ga(T9, T7)) → fib1_out_ga(s(s(0)), T7)
fib1_in_ga(s(s(s(T41))), T7) → U19_ga(T41, T7, fib48_in_ga(T41, X80))
fib48_in_ga(0, s(0)) → fib48_out_ga(0, s(0))
fib48_in_ga(s(T45), X97) → U4_ga(T45, X97, p57_in_gaaa(T45, X95, X96, X97))
p57_in_gaaa(T45, X95, X96, X97) → U5_gaaa(T45, X95, X96, X97, fib48_in_ga(T45, X95))
U5_gaaa(T45, X95, X96, X97, fib48_out_ga(T45, X95)) → p57_out_gaaa(T45, X95, X96, X97)
p57_in_gaaa(T45, T46, X96, X97) → U6_gaaa(T45, T46, X96, X97, fib48_in_ga(T45, T46))
U6_gaaa(T45, T46, X96, X97, fib48_out_ga(T45, T46)) → U7_gaaa(T45, T46, X96, X97, fib61_in_ga(T45, X96))
fib61_in_ga(0, 0) → fib61_out_ga(0, 0)
fib61_in_ga(s(0), s(0)) → fib61_out_ga(s(0), s(0))
fib61_in_ga(s(s(T50)), X112) → U13_ga(T50, X112, p57_in_gaaa(T50, X110, X111, X112))
p57_in_gaaa(T45, T46, T47, X97) → U8_gaaa(T45, T46, T47, X97, fib48_in_ga(T45, T46))
U8_gaaa(T45, T46, T47, X97, fib48_out_ga(T45, T46)) → U9_gaaa(T45, T46, T47, X97, fib61_in_ga(T45, T47))
U9_gaaa(T45, T46, T47, X97, fib61_out_ga(T45, T47)) → U10_gaaa(T45, T46, T47, X97, add62_in_aaa(T46, T47, X97))
add62_in_aaa(0, 0, 0) → add62_out_aaa(0, 0, 0)
add62_in_aaa(s(T59), T60, s(X134)) → U11_aaa(T59, T60, X134, add62_in_aaa(T59, T60, X134))
add62_in_aaa(T65, s(T66), s(X149)) → U12_aaa(T65, T66, X149, add62_in_aaa(T65, T66, X149))
U12_aaa(T65, T66, X149, add62_out_aaa(T65, T66, X149)) → add62_out_aaa(T65, s(T66), s(X149))
U11_aaa(T59, T60, X134, add62_out_aaa(T59, T60, X134)) → add62_out_aaa(s(T59), T60, s(X134))
U10_gaaa(T45, T46, T47, X97, add62_out_aaa(T46, T47, X97)) → p57_out_gaaa(T45, T46, T47, X97)
U13_ga(T50, X112, p57_out_gaaa(T50, X110, X111, X112)) → fib61_out_ga(s(s(T50)), X112)
U7_gaaa(T45, T46, X96, X97, fib61_out_ga(T45, X96)) → p57_out_gaaa(T45, T46, X96, X97)
U4_ga(T45, X97, p57_out_gaaa(T45, X95, X96, X97)) → fib48_out_ga(s(T45), X97)
U19_ga(T41, T7, fib48_out_ga(T41, X80)) → fib1_out_ga(s(s(s(T41))), T7)
fib1_in_ga(s(s(s(T41))), T7) → U20_ga(T41, T7, fib48_in_ga(T41, T42))
U20_ga(T41, T7, fib48_out_ga(T41, T42)) → U21_ga(T41, T7, fib61_in_ga(T41, X81))
U21_ga(T41, T7, fib61_out_ga(T41, X81)) → fib1_out_ga(s(s(s(T41))), T7)
U20_ga(T41, T7, fib48_out_ga(T41, T42)) → U22_ga(T41, T7, T42, fib61_in_ga(T41, T67))
U22_ga(T41, T7, T42, fib61_out_ga(T41, T67)) → U23_ga(T41, T7, add62_in_aaa(T42, T67, X82))
U23_ga(T41, T7, add62_out_aaa(T42, T67, X82)) → fib1_out_ga(s(s(s(T41))), T7)
U22_ga(T41, T7, T42, fib61_out_ga(T41, T67)) → U24_ga(T41, T7, add62_in_aaa(T42, T67, T68))
U24_ga(T41, T7, add62_out_aaa(T42, T67, T68)) → U25_ga(T41, T7, fib48_in_ga(T41, X10))
U25_ga(T41, T7, fib48_out_ga(T41, X10)) → fib1_out_ga(s(s(s(T41))), T7)
U24_ga(T41, T7, add62_out_aaa(T42, T67, T68)) → U26_ga(T41, T7, T68, fib48_in_ga(T41, T69))
U26_ga(T41, T7, T68, fib48_out_ga(T41, T69)) → U27_ga(T41, T7, add93_in_gaa(T68, T69, T7))
add93_in_gaa(0, 0, 0) → add93_out_gaa(0, 0, 0)
add93_in_gaa(s(T82), T83, s(T85)) → U14_gaa(T82, T83, T85, add93_in_gaa(T82, T83, T85))
add93_in_gaa(T92, s(T93), s(T95)) → U15_gaa(T92, T93, T95, add93_in_gaa(T92, T93, T95))
U15_gaa(T92, T93, T95, add93_out_gaa(T92, T93, T95)) → add93_out_gaa(T92, s(T93), s(T95))
U14_gaa(T82, T83, T85, add93_out_gaa(T82, T83, T85)) → add93_out_gaa(s(T82), T83, s(T85))
U27_ga(T41, T7, add93_out_gaa(T68, T69, T7)) → fib1_out_ga(s(s(s(T41))), T7)

(7) DependencyGraphProof (EQUIVALENT transformation)

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

(8) Complex Obligation (AND)

(9) Obligation:

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

ADD93_IN_GAA(T92, s(T93), s(T95)) → ADD93_IN_GAA(T92, T93, T95)
ADD93_IN_GAA(s(T82), T83, s(T85)) → ADD93_IN_GAA(T82, T83, T85)

The TRS R consists of the following rules:

fib1_in_ga(0, 0) → fib1_out_ga(0, 0)
fib1_in_ga(s(0), s(0)) → fib1_out_ga(s(0), s(0))
fib1_in_ga(s(s(0)), T7) → U16_ga(T7, fib20_in_a(X10))
fib20_in_a(0) → fib20_out_a(0)
U16_ga(T7, fib20_out_a(X10)) → fib1_out_ga(s(s(0)), T7)
fib1_in_ga(s(s(0)), T7) → U17_ga(T7, fib20_in_a(T9))
U17_ga(T7, fib20_out_a(T9)) → U18_ga(T7, add21_in_ga(T9, T7))
add21_in_ga(T20, s(T22)) → U2_ga(T20, T22, add33_in_ga(T20, T22))
add33_in_ga(0, 0) → add33_out_ga(0, 0)
add33_in_ga(s(T27), s(T29)) → U1_ga(T27, T29, add33_in_ga(T27, T29))
U1_ga(T27, T29, add33_out_ga(T27, T29)) → add33_out_ga(s(T27), s(T29))
U2_ga(T20, T22, add33_out_ga(T20, T22)) → add21_out_ga(T20, s(T22))
add21_in_ga(s(T34), s(T36)) → U3_ga(T34, T36, add21_in_ga(T34, T36))
U3_ga(T34, T36, add21_out_ga(T34, T36)) → add21_out_ga(s(T34), s(T36))
U18_ga(T7, add21_out_ga(T9, T7)) → fib1_out_ga(s(s(0)), T7)
fib1_in_ga(s(s(s(T41))), T7) → U19_ga(T41, T7, fib48_in_ga(T41, X80))
fib48_in_ga(0, s(0)) → fib48_out_ga(0, s(0))
fib48_in_ga(s(T45), X97) → U4_ga(T45, X97, p57_in_gaaa(T45, X95, X96, X97))
p57_in_gaaa(T45, X95, X96, X97) → U5_gaaa(T45, X95, X96, X97, fib48_in_ga(T45, X95))
U5_gaaa(T45, X95, X96, X97, fib48_out_ga(T45, X95)) → p57_out_gaaa(T45, X95, X96, X97)
p57_in_gaaa(T45, T46, X96, X97) → U6_gaaa(T45, T46, X96, X97, fib48_in_ga(T45, T46))
U6_gaaa(T45, T46, X96, X97, fib48_out_ga(T45, T46)) → U7_gaaa(T45, T46, X96, X97, fib61_in_ga(T45, X96))
fib61_in_ga(0, 0) → fib61_out_ga(0, 0)
fib61_in_ga(s(0), s(0)) → fib61_out_ga(s(0), s(0))
fib61_in_ga(s(s(T50)), X112) → U13_ga(T50, X112, p57_in_gaaa(T50, X110, X111, X112))
p57_in_gaaa(T45, T46, T47, X97) → U8_gaaa(T45, T46, T47, X97, fib48_in_ga(T45, T46))
U8_gaaa(T45, T46, T47, X97, fib48_out_ga(T45, T46)) → U9_gaaa(T45, T46, T47, X97, fib61_in_ga(T45, T47))
U9_gaaa(T45, T46, T47, X97, fib61_out_ga(T45, T47)) → U10_gaaa(T45, T46, T47, X97, add62_in_aaa(T46, T47, X97))
add62_in_aaa(0, 0, 0) → add62_out_aaa(0, 0, 0)
add62_in_aaa(s(T59), T60, s(X134)) → U11_aaa(T59, T60, X134, add62_in_aaa(T59, T60, X134))
add62_in_aaa(T65, s(T66), s(X149)) → U12_aaa(T65, T66, X149, add62_in_aaa(T65, T66, X149))
U12_aaa(T65, T66, X149, add62_out_aaa(T65, T66, X149)) → add62_out_aaa(T65, s(T66), s(X149))
U11_aaa(T59, T60, X134, add62_out_aaa(T59, T60, X134)) → add62_out_aaa(s(T59), T60, s(X134))
U10_gaaa(T45, T46, T47, X97, add62_out_aaa(T46, T47, X97)) → p57_out_gaaa(T45, T46, T47, X97)
U13_ga(T50, X112, p57_out_gaaa(T50, X110, X111, X112)) → fib61_out_ga(s(s(T50)), X112)
U7_gaaa(T45, T46, X96, X97, fib61_out_ga(T45, X96)) → p57_out_gaaa(T45, T46, X96, X97)
U4_ga(T45, X97, p57_out_gaaa(T45, X95, X96, X97)) → fib48_out_ga(s(T45), X97)
U19_ga(T41, T7, fib48_out_ga(T41, X80)) → fib1_out_ga(s(s(s(T41))), T7)
fib1_in_ga(s(s(s(T41))), T7) → U20_ga(T41, T7, fib48_in_ga(T41, T42))
U20_ga(T41, T7, fib48_out_ga(T41, T42)) → U21_ga(T41, T7, fib61_in_ga(T41, X81))
U21_ga(T41, T7, fib61_out_ga(T41, X81)) → fib1_out_ga(s(s(s(T41))), T7)
U20_ga(T41, T7, fib48_out_ga(T41, T42)) → U22_ga(T41, T7, T42, fib61_in_ga(T41, T67))
U22_ga(T41, T7, T42, fib61_out_ga(T41, T67)) → U23_ga(T41, T7, add62_in_aaa(T42, T67, X82))
U23_ga(T41, T7, add62_out_aaa(T42, T67, X82)) → fib1_out_ga(s(s(s(T41))), T7)
U22_ga(T41, T7, T42, fib61_out_ga(T41, T67)) → U24_ga(T41, T7, add62_in_aaa(T42, T67, T68))
U24_ga(T41, T7, add62_out_aaa(T42, T67, T68)) → U25_ga(T41, T7, fib48_in_ga(T41, X10))
U25_ga(T41, T7, fib48_out_ga(T41, X10)) → fib1_out_ga(s(s(s(T41))), T7)
U24_ga(T41, T7, add62_out_aaa(T42, T67, T68)) → U26_ga(T41, T7, T68, fib48_in_ga(T41, T69))
U26_ga(T41, T7, T68, fib48_out_ga(T41, T69)) → U27_ga(T41, T7, add93_in_gaa(T68, T69, T7))
add93_in_gaa(0, 0, 0) → add93_out_gaa(0, 0, 0)
add93_in_gaa(s(T82), T83, s(T85)) → U14_gaa(T82, T83, T85, add93_in_gaa(T82, T83, T85))
add93_in_gaa(T92, s(T93), s(T95)) → U15_gaa(T92, T93, T95, add93_in_gaa(T92, T93, T95))
U15_gaa(T92, T93, T95, add93_out_gaa(T92, T93, T95)) → add93_out_gaa(T92, s(T93), s(T95))
U14_gaa(T82, T83, T85, add93_out_gaa(T82, T83, T85)) → add93_out_gaa(s(T82), T83, s(T85))
U27_ga(T41, T7, add93_out_gaa(T68, T69, T7)) → fib1_out_ga(s(s(s(T41))), T7)

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

ADD93_IN_GAA(T92, s(T93), s(T95)) → ADD93_IN_GAA(T92, T93, T95)
ADD93_IN_GAA(s(T82), T83, s(T85)) → ADD93_IN_GAA(T82, T83, T85)

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

ADD93_IN_GAA(T92) → ADD93_IN_GAA(T92)
ADD93_IN_GAA(s(T82)) → ADD93_IN_GAA(T82)

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

(14) UsableRulesReductionPairsProof (EQUIVALENT transformation)

By using the usable rules with reduction pair processor [LPAR04] with a polynomial ordering [POLO], all dependency pairs and the corresponding usable rules [FROCOS05] can be oriented non-strictly. All non-usable rules are removed, and those dependency pairs and usable rules that have been oriented strictly or contain non-usable symbols in their left-hand side are removed as well.

The following dependency pairs can be deleted:

ADD93_IN_GAA(s(T82)) → ADD93_IN_GAA(T82)

No rules are removed from R.

Used ordering: POLO with Polynomial interpretation [POLO]:

POL(ADD93_IN_GAA(x₁)) = 2·x₁
POL(s(x₁)) = 2·x₁

(15) Obligation:

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

ADD93_IN_GAA(T92) → ADD93_IN_GAA(T92)

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

(16) NonTerminationProof (EQUIVALENT transformation)

We used the non-termination processor [FROCOS05] to show that the DP problem is infinite.
Found a loop by semiunifying a rule from P directly.

s = ADD93_IN_GAA(T92) evaluates to t =ADD93_IN_GAA(T92)

Thus s starts an infinite chain as s semiunifies with t with the following substitutions:

Semiunifier: [ ]
Matcher: [ ]

Rewriting sequence

The DP semiunifies directly so there is only one rewrite step from ADD93_IN_GAA(T92) to ADD93_IN_GAA(T92).

(17) NO

(18) Obligation:

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

ADD62_IN_AAA(T65, s(T66), s(X149)) → ADD62_IN_AAA(T65, T66, X149)
ADD62_IN_AAA(s(T59), T60, s(X134)) → ADD62_IN_AAA(T59, T60, X134)

The TRS R consists of the following rules:

fib1_in_ga(0, 0) → fib1_out_ga(0, 0)
fib1_in_ga(s(0), s(0)) → fib1_out_ga(s(0), s(0))
fib1_in_ga(s(s(0)), T7) → U16_ga(T7, fib20_in_a(X10))
fib20_in_a(0) → fib20_out_a(0)
U16_ga(T7, fib20_out_a(X10)) → fib1_out_ga(s(s(0)), T7)
fib1_in_ga(s(s(0)), T7) → U17_ga(T7, fib20_in_a(T9))
U17_ga(T7, fib20_out_a(T9)) → U18_ga(T7, add21_in_ga(T9, T7))
add21_in_ga(T20, s(T22)) → U2_ga(T20, T22, add33_in_ga(T20, T22))
add33_in_ga(0, 0) → add33_out_ga(0, 0)
add33_in_ga(s(T27), s(T29)) → U1_ga(T27, T29, add33_in_ga(T27, T29))
U1_ga(T27, T29, add33_out_ga(T27, T29)) → add33_out_ga(s(T27), s(T29))
U2_ga(T20, T22, add33_out_ga(T20, T22)) → add21_out_ga(T20, s(T22))
add21_in_ga(s(T34), s(T36)) → U3_ga(T34, T36, add21_in_ga(T34, T36))
U3_ga(T34, T36, add21_out_ga(T34, T36)) → add21_out_ga(s(T34), s(T36))
U18_ga(T7, add21_out_ga(T9, T7)) → fib1_out_ga(s(s(0)), T7)
fib1_in_ga(s(s(s(T41))), T7) → U19_ga(T41, T7, fib48_in_ga(T41, X80))
fib48_in_ga(0, s(0)) → fib48_out_ga(0, s(0))
fib48_in_ga(s(T45), X97) → U4_ga(T45, X97, p57_in_gaaa(T45, X95, X96, X97))
p57_in_gaaa(T45, X95, X96, X97) → U5_gaaa(T45, X95, X96, X97, fib48_in_ga(T45, X95))
U5_gaaa(T45, X95, X96, X97, fib48_out_ga(T45, X95)) → p57_out_gaaa(T45, X95, X96, X97)
p57_in_gaaa(T45, T46, X96, X97) → U6_gaaa(T45, T46, X96, X97, fib48_in_ga(T45, T46))
U6_gaaa(T45, T46, X96, X97, fib48_out_ga(T45, T46)) → U7_gaaa(T45, T46, X96, X97, fib61_in_ga(T45, X96))
fib61_in_ga(0, 0) → fib61_out_ga(0, 0)
fib61_in_ga(s(0), s(0)) → fib61_out_ga(s(0), s(0))
fib61_in_ga(s(s(T50)), X112) → U13_ga(T50, X112, p57_in_gaaa(T50, X110, X111, X112))
p57_in_gaaa(T45, T46, T47, X97) → U8_gaaa(T45, T46, T47, X97, fib48_in_ga(T45, T46))
U8_gaaa(T45, T46, T47, X97, fib48_out_ga(T45, T46)) → U9_gaaa(T45, T46, T47, X97, fib61_in_ga(T45, T47))
U9_gaaa(T45, T46, T47, X97, fib61_out_ga(T45, T47)) → U10_gaaa(T45, T46, T47, X97, add62_in_aaa(T46, T47, X97))
add62_in_aaa(0, 0, 0) → add62_out_aaa(0, 0, 0)
add62_in_aaa(s(T59), T60, s(X134)) → U11_aaa(T59, T60, X134, add62_in_aaa(T59, T60, X134))
add62_in_aaa(T65, s(T66), s(X149)) → U12_aaa(T65, T66, X149, add62_in_aaa(T65, T66, X149))
U12_aaa(T65, T66, X149, add62_out_aaa(T65, T66, X149)) → add62_out_aaa(T65, s(T66), s(X149))
U11_aaa(T59, T60, X134, add62_out_aaa(T59, T60, X134)) → add62_out_aaa(s(T59), T60, s(X134))
U10_gaaa(T45, T46, T47, X97, add62_out_aaa(T46, T47, X97)) → p57_out_gaaa(T45, T46, T47, X97)
U13_ga(T50, X112, p57_out_gaaa(T50, X110, X111, X112)) → fib61_out_ga(s(s(T50)), X112)
U7_gaaa(T45, T46, X96, X97, fib61_out_ga(T45, X96)) → p57_out_gaaa(T45, T46, X96, X97)
U4_ga(T45, X97, p57_out_gaaa(T45, X95, X96, X97)) → fib48_out_ga(s(T45), X97)
U19_ga(T41, T7, fib48_out_ga(T41, X80)) → fib1_out_ga(s(s(s(T41))), T7)
fib1_in_ga(s(s(s(T41))), T7) → U20_ga(T41, T7, fib48_in_ga(T41, T42))
U20_ga(T41, T7, fib48_out_ga(T41, T42)) → U21_ga(T41, T7, fib61_in_ga(T41, X81))
U21_ga(T41, T7, fib61_out_ga(T41, X81)) → fib1_out_ga(s(s(s(T41))), T7)
U20_ga(T41, T7, fib48_out_ga(T41, T42)) → U22_ga(T41, T7, T42, fib61_in_ga(T41, T67))
U22_ga(T41, T7, T42, fib61_out_ga(T41, T67)) → U23_ga(T41, T7, add62_in_aaa(T42, T67, X82))
U23_ga(T41, T7, add62_out_aaa(T42, T67, X82)) → fib1_out_ga(s(s(s(T41))), T7)
U22_ga(T41, T7, T42, fib61_out_ga(T41, T67)) → U24_ga(T41, T7, add62_in_aaa(T42, T67, T68))
U24_ga(T41, T7, add62_out_aaa(T42, T67, T68)) → U25_ga(T41, T7, fib48_in_ga(T41, X10))
U25_ga(T41, T7, fib48_out_ga(T41, X10)) → fib1_out_ga(s(s(s(T41))), T7)
U24_ga(T41, T7, add62_out_aaa(T42, T67, T68)) → U26_ga(T41, T7, T68, fib48_in_ga(T41, T69))
U26_ga(T41, T7, T68, fib48_out_ga(T41, T69)) → U27_ga(T41, T7, add93_in_gaa(T68, T69, T7))
add93_in_gaa(0, 0, 0) → add93_out_gaa(0, 0, 0)
add93_in_gaa(s(T82), T83, s(T85)) → U14_gaa(T82, T83, T85, add93_in_gaa(T82, T83, T85))
add93_in_gaa(T92, s(T93), s(T95)) → U15_gaa(T92, T93, T95, add93_in_gaa(T92, T93, T95))
U15_gaa(T92, T93, T95, add93_out_gaa(T92, T93, T95)) → add93_out_gaa(T92, s(T93), s(T95))
U14_gaa(T82, T83, T85, add93_out_gaa(T82, T83, T85)) → add93_out_gaa(s(T82), T83, s(T85))
U27_ga(T41, T7, add93_out_gaa(T68, T69, T7)) → fib1_out_ga(s(s(s(T41))), T7)

(19) UsableRulesProof (EQUIVALENT transformation)

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

(20) Obligation:

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

ADD62_IN_AAA(T65, s(T66), s(X149)) → ADD62_IN_AAA(T65, T66, X149)
ADD62_IN_AAA(s(T59), T60, s(X134)) → ADD62_IN_AAA(T59, T60, X134)

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

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

(21) PiDPToQDPProof (SOUND transformation)

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

(22) Obligation:

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

ADD62_IN_AAA → ADD62_IN_AAA

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

(23) NonTerminationProof (EQUIVALENT transformation)

We used the non-termination processor [FROCOS05] to show that the DP problem is infinite.
Found a loop by semiunifying a rule from P directly.

s = ADD62_IN_AAA evaluates to t =ADD62_IN_AAA

Thus s starts an infinite chain as s semiunifies with t with the following substitutions:

Matcher: [ ]
Semiunifier: [ ]

Rewriting sequence

The DP semiunifies directly so there is only one rewrite step from ADD62_IN_AAA to ADD62_IN_AAA.

(24) NO

(25) Obligation:

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

FIB48_IN_GA(s(T45), X97) → P57_IN_GAAA(T45, X95, X96, X97)
P57_IN_GAAA(T45, X95, X96, X97) → FIB48_IN_GA(T45, X95)
P57_IN_GAAA(T45, T46, X96, X97) → U6_GAAA(T45, T46, X96, X97, fib48_in_ga(T45, T46))
U6_GAAA(T45, T46, X96, X97, fib48_out_ga(T45, T46)) → FIB61_IN_GA(T45, X96)
FIB61_IN_GA(s(s(T50)), X112) → P57_IN_GAAA(T50, X110, X111, X112)
P57_IN_GAAA(T45, T46, T47, X97) → U8_GAAA(T45, T46, T47, X97, fib48_in_ga(T45, T46))
U8_GAAA(T45, T46, T47, X97, fib48_out_ga(T45, T46)) → FIB61_IN_GA(T45, T47)

The TRS R consists of the following rules:

fib1_in_ga(0, 0) → fib1_out_ga(0, 0)
fib1_in_ga(s(0), s(0)) → fib1_out_ga(s(0), s(0))
fib1_in_ga(s(s(0)), T7) → U16_ga(T7, fib20_in_a(X10))
fib20_in_a(0) → fib20_out_a(0)
U16_ga(T7, fib20_out_a(X10)) → fib1_out_ga(s(s(0)), T7)
fib1_in_ga(s(s(0)), T7) → U17_ga(T7, fib20_in_a(T9))
U17_ga(T7, fib20_out_a(T9)) → U18_ga(T7, add21_in_ga(T9, T7))
add21_in_ga(T20, s(T22)) → U2_ga(T20, T22, add33_in_ga(T20, T22))
add33_in_ga(0, 0) → add33_out_ga(0, 0)
add33_in_ga(s(T27), s(T29)) → U1_ga(T27, T29, add33_in_ga(T27, T29))
U1_ga(T27, T29, add33_out_ga(T27, T29)) → add33_out_ga(s(T27), s(T29))
U2_ga(T20, T22, add33_out_ga(T20, T22)) → add21_out_ga(T20, s(T22))
add21_in_ga(s(T34), s(T36)) → U3_ga(T34, T36, add21_in_ga(T34, T36))
U3_ga(T34, T36, add21_out_ga(T34, T36)) → add21_out_ga(s(T34), s(T36))
U18_ga(T7, add21_out_ga(T9, T7)) → fib1_out_ga(s(s(0)), T7)
fib1_in_ga(s(s(s(T41))), T7) → U19_ga(T41, T7, fib48_in_ga(T41, X80))
fib48_in_ga(0, s(0)) → fib48_out_ga(0, s(0))
fib48_in_ga(s(T45), X97) → U4_ga(T45, X97, p57_in_gaaa(T45, X95, X96, X97))
p57_in_gaaa(T45, X95, X96, X97) → U5_gaaa(T45, X95, X96, X97, fib48_in_ga(T45, X95))
U5_gaaa(T45, X95, X96, X97, fib48_out_ga(T45, X95)) → p57_out_gaaa(T45, X95, X96, X97)
p57_in_gaaa(T45, T46, X96, X97) → U6_gaaa(T45, T46, X96, X97, fib48_in_ga(T45, T46))
U6_gaaa(T45, T46, X96, X97, fib48_out_ga(T45, T46)) → U7_gaaa(T45, T46, X96, X97, fib61_in_ga(T45, X96))
fib61_in_ga(0, 0) → fib61_out_ga(0, 0)
fib61_in_ga(s(0), s(0)) → fib61_out_ga(s(0), s(0))
fib61_in_ga(s(s(T50)), X112) → U13_ga(T50, X112, p57_in_gaaa(T50, X110, X111, X112))
p57_in_gaaa(T45, T46, T47, X97) → U8_gaaa(T45, T46, T47, X97, fib48_in_ga(T45, T46))
U8_gaaa(T45, T46, T47, X97, fib48_out_ga(T45, T46)) → U9_gaaa(T45, T46, T47, X97, fib61_in_ga(T45, T47))
U9_gaaa(T45, T46, T47, X97, fib61_out_ga(T45, T47)) → U10_gaaa(T45, T46, T47, X97, add62_in_aaa(T46, T47, X97))
add62_in_aaa(0, 0, 0) → add62_out_aaa(0, 0, 0)
add62_in_aaa(s(T59), T60, s(X134)) → U11_aaa(T59, T60, X134, add62_in_aaa(T59, T60, X134))
add62_in_aaa(T65, s(T66), s(X149)) → U12_aaa(T65, T66, X149, add62_in_aaa(T65, T66, X149))
U12_aaa(T65, T66, X149, add62_out_aaa(T65, T66, X149)) → add62_out_aaa(T65, s(T66), s(X149))
U11_aaa(T59, T60, X134, add62_out_aaa(T59, T60, X134)) → add62_out_aaa(s(T59), T60, s(X134))
U10_gaaa(T45, T46, T47, X97, add62_out_aaa(T46, T47, X97)) → p57_out_gaaa(T45, T46, T47, X97)
U13_ga(T50, X112, p57_out_gaaa(T50, X110, X111, X112)) → fib61_out_ga(s(s(T50)), X112)
U7_gaaa(T45, T46, X96, X97, fib61_out_ga(T45, X96)) → p57_out_gaaa(T45, T46, X96, X97)
U4_ga(T45, X97, p57_out_gaaa(T45, X95, X96, X97)) → fib48_out_ga(s(T45), X97)
U19_ga(T41, T7, fib48_out_ga(T41, X80)) → fib1_out_ga(s(s(s(T41))), T7)
fib1_in_ga(s(s(s(T41))), T7) → U20_ga(T41, T7, fib48_in_ga(T41, T42))
U20_ga(T41, T7, fib48_out_ga(T41, T42)) → U21_ga(T41, T7, fib61_in_ga(T41, X81))
U21_ga(T41, T7, fib61_out_ga(T41, X81)) → fib1_out_ga(s(s(s(T41))), T7)
U20_ga(T41, T7, fib48_out_ga(T41, T42)) → U22_ga(T41, T7, T42, fib61_in_ga(T41, T67))
U22_ga(T41, T7, T42, fib61_out_ga(T41, T67)) → U23_ga(T41, T7, add62_in_aaa(T42, T67, X82))
U23_ga(T41, T7, add62_out_aaa(T42, T67, X82)) → fib1_out_ga(s(s(s(T41))), T7)
U22_ga(T41, T7, T42, fib61_out_ga(T41, T67)) → U24_ga(T41, T7, add62_in_aaa(T42, T67, T68))
U24_ga(T41, T7, add62_out_aaa(T42, T67, T68)) → U25_ga(T41, T7, fib48_in_ga(T41, X10))
U25_ga(T41, T7, fib48_out_ga(T41, X10)) → fib1_out_ga(s(s(s(T41))), T7)
U24_ga(T41, T7, add62_out_aaa(T42, T67, T68)) → U26_ga(T41, T7, T68, fib48_in_ga(T41, T69))
U26_ga(T41, T7, T68, fib48_out_ga(T41, T69)) → U27_ga(T41, T7, add93_in_gaa(T68, T69, T7))
add93_in_gaa(0, 0, 0) → add93_out_gaa(0, 0, 0)
add93_in_gaa(s(T82), T83, s(T85)) → U14_gaa(T82, T83, T85, add93_in_gaa(T82, T83, T85))
add93_in_gaa(T92, s(T93), s(T95)) → U15_gaa(T92, T93, T95, add93_in_gaa(T92, T93, T95))
U15_gaa(T92, T93, T95, add93_out_gaa(T92, T93, T95)) → add93_out_gaa(T92, s(T93), s(T95))
U14_gaa(T82, T83, T85, add93_out_gaa(T82, T83, T85)) → add93_out_gaa(s(T82), T83, s(T85))
U27_ga(T41, T7, add93_out_gaa(T68, T69, T7)) → fib1_out_ga(s(s(s(T41))), T7)

(26) UsableRulesProof (EQUIVALENT transformation)

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

(27) Obligation:

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

FIB48_IN_GA(s(T45), X97) → P57_IN_GAAA(T45, X95, X96, X97)
P57_IN_GAAA(T45, X95, X96, X97) → FIB48_IN_GA(T45, X95)
P57_IN_GAAA(T45, T46, X96, X97) → U6_GAAA(T45, T46, X96, X97, fib48_in_ga(T45, T46))
U6_GAAA(T45, T46, X96, X97, fib48_out_ga(T45, T46)) → FIB61_IN_GA(T45, X96)
FIB61_IN_GA(s(s(T50)), X112) → P57_IN_GAAA(T50, X110, X111, X112)
P57_IN_GAAA(T45, T46, T47, X97) → U8_GAAA(T45, T46, T47, X97, fib48_in_ga(T45, T46))
U8_GAAA(T45, T46, T47, X97, fib48_out_ga(T45, T46)) → FIB61_IN_GA(T45, T47)

The TRS R consists of the following rules:

fib48_in_ga(0, s(0)) → fib48_out_ga(0, s(0))
fib48_in_ga(s(T45), X97) → U4_ga(T45, X97, p57_in_gaaa(T45, X95, X96, X97))
U4_ga(T45, X97, p57_out_gaaa(T45, X95, X96, X97)) → fib48_out_ga(s(T45), X97)
p57_in_gaaa(T45, X95, X96, X97) → U5_gaaa(T45, X95, X96, X97, fib48_in_ga(T45, X95))
p57_in_gaaa(T45, T46, X96, X97) → U6_gaaa(T45, T46, X96, X97, fib48_in_ga(T45, T46))
p57_in_gaaa(T45, T46, T47, X97) → U8_gaaa(T45, T46, T47, X97, fib48_in_ga(T45, T46))
U5_gaaa(T45, X95, X96, X97, fib48_out_ga(T45, X95)) → p57_out_gaaa(T45, X95, X96, X97)
U6_gaaa(T45, T46, X96, X97, fib48_out_ga(T45, T46)) → U7_gaaa(T45, T46, X96, X97, fib61_in_ga(T45, X96))
U8_gaaa(T45, T46, T47, X97, fib48_out_ga(T45, T46)) → U9_gaaa(T45, T46, T47, X97, fib61_in_ga(T45, T47))
U7_gaaa(T45, T46, X96, X97, fib61_out_ga(T45, X96)) → p57_out_gaaa(T45, T46, X96, X97)
U9_gaaa(T45, T46, T47, X97, fib61_out_ga(T45, T47)) → U10_gaaa(T45, T46, T47, X97, add62_in_aaa(T46, T47, X97))
fib61_in_ga(0, 0) → fib61_out_ga(0, 0)
fib61_in_ga(s(0), s(0)) → fib61_out_ga(s(0), s(0))
fib61_in_ga(s(s(T50)), X112) → U13_ga(T50, X112, p57_in_gaaa(T50, X110, X111, X112))
U10_gaaa(T45, T46, T47, X97, add62_out_aaa(T46, T47, X97)) → p57_out_gaaa(T45, T46, T47, X97)
U13_ga(T50, X112, p57_out_gaaa(T50, X110, X111, X112)) → fib61_out_ga(s(s(T50)), X112)
add62_in_aaa(0, 0, 0) → add62_out_aaa(0, 0, 0)
add62_in_aaa(s(T59), T60, s(X134)) → U11_aaa(T59, T60, X134, add62_in_aaa(T59, T60, X134))
add62_in_aaa(T65, s(T66), s(X149)) → U12_aaa(T65, T66, X149, add62_in_aaa(T65, T66, X149))
U11_aaa(T59, T60, X134, add62_out_aaa(T59, T60, X134)) → add62_out_aaa(s(T59), T60, s(X134))
U12_aaa(T65, T66, X149, add62_out_aaa(T65, T66, X149)) → add62_out_aaa(T65, s(T66), s(X149))

The argument filtering Pi contains the following mapping:
0 = 0
s(x1) = s(x1)
fib48_in_ga(x1, x2) = fib48_in_ga(x1)
fib48_out_ga(x1, x2) = fib48_out_ga(x1)
U4_ga(x1, x2, x3) = U4_ga(x1, x3)
p57_in_gaaa(x1, x2, x3, x4) = p57_in_gaaa(x1)
U5_gaaa(x1, x2, x3, x4, x5) = U5_gaaa(x1, x5)
p57_out_gaaa(x1, x2, x3, x4) = p57_out_gaaa(x1)
U6_gaaa(x1, x2, x3, x4, x5) = U6_gaaa(x1, x5)
U7_gaaa(x1, x2, x3, x4, x5) = U7_gaaa(x1, x5)
fib61_in_ga(x1, x2) = fib61_in_ga(x1)
fib61_out_ga(x1, x2) = fib61_out_ga(x1)
U13_ga(x1, x2, x3) = U13_ga(x1, x3)
U8_gaaa(x1, x2, x3, x4, x5) = U8_gaaa(x1, x5)
U9_gaaa(x1, x2, x3, x4, x5) = U9_gaaa(x1, x5)
U10_gaaa(x1, x2, x3, x4, x5) = U10_gaaa(x1, x5)
add62_in_aaa(x1, x2, x3) = add62_in_aaa
add62_out_aaa(x1, x2, x3) = add62_out_aaa(x1, x2, x3)
U11_aaa(x1, x2, x3, x4) = U11_aaa(x4)
U12_aaa(x1, x2, x3, x4) = U12_aaa(x4)
FIB48_IN_GA(x1, x2) = FIB48_IN_GA(x1)
P57_IN_GAAA(x1, x2, x3, x4) = P57_IN_GAAA(x1)
U6_GAAA(x1, x2, x3, x4, x5) = U6_GAAA(x1, x5)
FIB61_IN_GA(x1, x2) = FIB61_IN_GA(x1)
U8_GAAA(x1, x2, x3, x4, x5) = U8_GAAA(x1, x5)

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

(28) PiDPToQDPProof (SOUND transformation)

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

(29) Obligation:

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

FIB48_IN_GA(s(T45)) → P57_IN_GAAA(T45)
P57_IN_GAAA(T45) → FIB48_IN_GA(T45)
P57_IN_GAAA(T45) → U6_GAAA(T45, fib48_in_ga(T45))
U6_GAAA(T45, fib48_out_ga(T45)) → FIB61_IN_GA(T45)
FIB61_IN_GA(s(s(T50))) → P57_IN_GAAA(T50)
P57_IN_GAAA(T45) → U8_GAAA(T45, fib48_in_ga(T45))
U8_GAAA(T45, fib48_out_ga(T45)) → FIB61_IN_GA(T45)

The TRS R consists of the following rules:

fib48_in_ga(0) → fib48_out_ga(0)
fib48_in_ga(s(T45)) → U4_ga(T45, p57_in_gaaa(T45))
U4_ga(T45, p57_out_gaaa(T45)) → fib48_out_ga(s(T45))
p57_in_gaaa(T45) → U5_gaaa(T45, fib48_in_ga(T45))
p57_in_gaaa(T45) → U6_gaaa(T45, fib48_in_ga(T45))
p57_in_gaaa(T45) → U8_gaaa(T45, fib48_in_ga(T45))
U5_gaaa(T45, fib48_out_ga(T45)) → p57_out_gaaa(T45)
U6_gaaa(T45, fib48_out_ga(T45)) → U7_gaaa(T45, fib61_in_ga(T45))
U8_gaaa(T45, fib48_out_ga(T45)) → U9_gaaa(T45, fib61_in_ga(T45))
U7_gaaa(T45, fib61_out_ga(T45)) → p57_out_gaaa(T45)
U9_gaaa(T45, fib61_out_ga(T45)) → U10_gaaa(T45, add62_in_aaa)
fib61_in_ga(0) → fib61_out_ga(0)
fib61_in_ga(s(0)) → fib61_out_ga(s(0))
fib61_in_ga(s(s(T50))) → U13_ga(T50, p57_in_gaaa(T50))
U10_gaaa(T45, add62_out_aaa(T46, T47, X97)) → p57_out_gaaa(T45)
U13_ga(T50, p57_out_gaaa(T50)) → fib61_out_ga(s(s(T50)))
add62_in_aaa → add62_out_aaa(0, 0, 0)
add62_in_aaa → U11_aaa(add62_in_aaa)
add62_in_aaa → U12_aaa(add62_in_aaa)
U11_aaa(add62_out_aaa(T59, T60, X134)) → add62_out_aaa(s(T59), T60, s(X134))
U12_aaa(add62_out_aaa(T65, T66, X149)) → add62_out_aaa(T65, s(T66), s(X149))

The set Q consists of the following terms:

fib48_in_ga(x0)
U4_ga(x0, x1)
p57_in_gaaa(x0)
U5_gaaa(x0, x1)
U6_gaaa(x0, x1)
U8_gaaa(x0, x1)
U7_gaaa(x0, x1)
U9_gaaa(x0, x1)
fib61_in_ga(x0)
U10_gaaa(x0, x1)
U13_ga(x0, x1)
add62_in_aaa
U11_aaa(x0)
U12_aaa(x0)

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

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

P57_IN_GAAA(T45) → FIB48_IN_GA(T45)
The graph contains the following edges 1 >= 1
FIB48_IN_GA(s(T45)) → P57_IN_GAAA(T45)
The graph contains the following edges 1 > 1
FIB61_IN_GA(s(s(T50))) → P57_IN_GAAA(T50)
The graph contains the following edges 1 > 1
U6_GAAA(T45, fib48_out_ga(T45)) → FIB61_IN_GA(T45)
The graph contains the following edges 1 >= 1, 2 > 1
U8_GAAA(T45, fib48_out_ga(T45)) → FIB61_IN_GA(T45)
The graph contains the following edges 1 >= 1, 2 > 1
P57_IN_GAAA(T45) → U6_GAAA(T45, fib48_in_ga(T45))
The graph contains the following edges 1 >= 1
P57_IN_GAAA(T45) → U8_GAAA(T45, fib48_in_ga(T45))
The graph contains the following edges 1 >= 1

(31) YES

(32) Obligation:

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

ADD33_IN_GA(s(T27), s(T29)) → ADD33_IN_GA(T27, T29)

The TRS R consists of the following rules:

fib1_in_ga(0, 0) → fib1_out_ga(0, 0)
fib1_in_ga(s(0), s(0)) → fib1_out_ga(s(0), s(0))
fib1_in_ga(s(s(0)), T7) → U16_ga(T7, fib20_in_a(X10))
fib20_in_a(0) → fib20_out_a(0)
U16_ga(T7, fib20_out_a(X10)) → fib1_out_ga(s(s(0)), T7)
fib1_in_ga(s(s(0)), T7) → U17_ga(T7, fib20_in_a(T9))
U17_ga(T7, fib20_out_a(T9)) → U18_ga(T7, add21_in_ga(T9, T7))
add21_in_ga(T20, s(T22)) → U2_ga(T20, T22, add33_in_ga(T20, T22))
add33_in_ga(0, 0) → add33_out_ga(0, 0)
add33_in_ga(s(T27), s(T29)) → U1_ga(T27, T29, add33_in_ga(T27, T29))
U1_ga(T27, T29, add33_out_ga(T27, T29)) → add33_out_ga(s(T27), s(T29))
U2_ga(T20, T22, add33_out_ga(T20, T22)) → add21_out_ga(T20, s(T22))
add21_in_ga(s(T34), s(T36)) → U3_ga(T34, T36, add21_in_ga(T34, T36))
U3_ga(T34, T36, add21_out_ga(T34, T36)) → add21_out_ga(s(T34), s(T36))
U18_ga(T7, add21_out_ga(T9, T7)) → fib1_out_ga(s(s(0)), T7)
fib1_in_ga(s(s(s(T41))), T7) → U19_ga(T41, T7, fib48_in_ga(T41, X80))
fib48_in_ga(0, s(0)) → fib48_out_ga(0, s(0))
fib48_in_ga(s(T45), X97) → U4_ga(T45, X97, p57_in_gaaa(T45, X95, X96, X97))
p57_in_gaaa(T45, X95, X96, X97) → U5_gaaa(T45, X95, X96, X97, fib48_in_ga(T45, X95))
U5_gaaa(T45, X95, X96, X97, fib48_out_ga(T45, X95)) → p57_out_gaaa(T45, X95, X96, X97)
p57_in_gaaa(T45, T46, X96, X97) → U6_gaaa(T45, T46, X96, X97, fib48_in_ga(T45, T46))
U6_gaaa(T45, T46, X96, X97, fib48_out_ga(T45, T46)) → U7_gaaa(T45, T46, X96, X97, fib61_in_ga(T45, X96))
fib61_in_ga(0, 0) → fib61_out_ga(0, 0)
fib61_in_ga(s(0), s(0)) → fib61_out_ga(s(0), s(0))
fib61_in_ga(s(s(T50)), X112) → U13_ga(T50, X112, p57_in_gaaa(T50, X110, X111, X112))
p57_in_gaaa(T45, T46, T47, X97) → U8_gaaa(T45, T46, T47, X97, fib48_in_ga(T45, T46))
U8_gaaa(T45, T46, T47, X97, fib48_out_ga(T45, T46)) → U9_gaaa(T45, T46, T47, X97, fib61_in_ga(T45, T47))
U9_gaaa(T45, T46, T47, X97, fib61_out_ga(T45, T47)) → U10_gaaa(T45, T46, T47, X97, add62_in_aaa(T46, T47, X97))
add62_in_aaa(0, 0, 0) → add62_out_aaa(0, 0, 0)
add62_in_aaa(s(T59), T60, s(X134)) → U11_aaa(T59, T60, X134, add62_in_aaa(T59, T60, X134))
add62_in_aaa(T65, s(T66), s(X149)) → U12_aaa(T65, T66, X149, add62_in_aaa(T65, T66, X149))
U12_aaa(T65, T66, X149, add62_out_aaa(T65, T66, X149)) → add62_out_aaa(T65, s(T66), s(X149))
U11_aaa(T59, T60, X134, add62_out_aaa(T59, T60, X134)) → add62_out_aaa(s(T59), T60, s(X134))
U10_gaaa(T45, T46, T47, X97, add62_out_aaa(T46, T47, X97)) → p57_out_gaaa(T45, T46, T47, X97)
U13_ga(T50, X112, p57_out_gaaa(T50, X110, X111, X112)) → fib61_out_ga(s(s(T50)), X112)
U7_gaaa(T45, T46, X96, X97, fib61_out_ga(T45, X96)) → p57_out_gaaa(T45, T46, X96, X97)
U4_ga(T45, X97, p57_out_gaaa(T45, X95, X96, X97)) → fib48_out_ga(s(T45), X97)
U19_ga(T41, T7, fib48_out_ga(T41, X80)) → fib1_out_ga(s(s(s(T41))), T7)
fib1_in_ga(s(s(s(T41))), T7) → U20_ga(T41, T7, fib48_in_ga(T41, T42))
U20_ga(T41, T7, fib48_out_ga(T41, T42)) → U21_ga(T41, T7, fib61_in_ga(T41, X81))
U21_ga(T41, T7, fib61_out_ga(T41, X81)) → fib1_out_ga(s(s(s(T41))), T7)
U20_ga(T41, T7, fib48_out_ga(T41, T42)) → U22_ga(T41, T7, T42, fib61_in_ga(T41, T67))
U22_ga(T41, T7, T42, fib61_out_ga(T41, T67)) → U23_ga(T41, T7, add62_in_aaa(T42, T67, X82))
U23_ga(T41, T7, add62_out_aaa(T42, T67, X82)) → fib1_out_ga(s(s(s(T41))), T7)
U22_ga(T41, T7, T42, fib61_out_ga(T41, T67)) → U24_ga(T41, T7, add62_in_aaa(T42, T67, T68))
U24_ga(T41, T7, add62_out_aaa(T42, T67, T68)) → U25_ga(T41, T7, fib48_in_ga(T41, X10))
U25_ga(T41, T7, fib48_out_ga(T41, X10)) → fib1_out_ga(s(s(s(T41))), T7)
U24_ga(T41, T7, add62_out_aaa(T42, T67, T68)) → U26_ga(T41, T7, T68, fib48_in_ga(T41, T69))
U26_ga(T41, T7, T68, fib48_out_ga(T41, T69)) → U27_ga(T41, T7, add93_in_gaa(T68, T69, T7))
add93_in_gaa(0, 0, 0) → add93_out_gaa(0, 0, 0)
add93_in_gaa(s(T82), T83, s(T85)) → U14_gaa(T82, T83, T85, add93_in_gaa(T82, T83, T85))
add93_in_gaa(T92, s(T93), s(T95)) → U15_gaa(T92, T93, T95, add93_in_gaa(T92, T93, T95))
U15_gaa(T92, T93, T95, add93_out_gaa(T92, T93, T95)) → add93_out_gaa(T92, s(T93), s(T95))
U14_gaa(T82, T83, T85, add93_out_gaa(T82, T83, T85)) → add93_out_gaa(s(T82), T83, s(T85))
U27_ga(T41, T7, add93_out_gaa(T68, T69, T7)) → fib1_out_ga(s(s(s(T41))), T7)

(33) UsableRulesProof (EQUIVALENT transformation)

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

(34) Obligation:

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

ADD33_IN_GA(s(T27), s(T29)) → ADD33_IN_GA(T27, T29)

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

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

(35) PiDPToQDPProof (SOUND transformation)

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

(36) Obligation:

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

ADD33_IN_GA(s(T27)) → ADD33_IN_GA(T27)

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

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

ADD33_IN_GA(s(T27)) → ADD33_IN_GA(T27)
The graph contains the following edges 1 > 1

(38) YES

(39) Obligation:

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

ADD21_IN_GA(s(T34), s(T36)) → ADD21_IN_GA(T34, T36)

The TRS R consists of the following rules:

fib1_in_ga(0, 0) → fib1_out_ga(0, 0)
fib1_in_ga(s(0), s(0)) → fib1_out_ga(s(0), s(0))
fib1_in_ga(s(s(0)), T7) → U16_ga(T7, fib20_in_a(X10))
fib20_in_a(0) → fib20_out_a(0)
U16_ga(T7, fib20_out_a(X10)) → fib1_out_ga(s(s(0)), T7)
fib1_in_ga(s(s(0)), T7) → U17_ga(T7, fib20_in_a(T9))
U17_ga(T7, fib20_out_a(T9)) → U18_ga(T7, add21_in_ga(T9, T7))
add21_in_ga(T20, s(T22)) → U2_ga(T20, T22, add33_in_ga(T20, T22))
add33_in_ga(0, 0) → add33_out_ga(0, 0)
add33_in_ga(s(T27), s(T29)) → U1_ga(T27, T29, add33_in_ga(T27, T29))
U1_ga(T27, T29, add33_out_ga(T27, T29)) → add33_out_ga(s(T27), s(T29))
U2_ga(T20, T22, add33_out_ga(T20, T22)) → add21_out_ga(T20, s(T22))
add21_in_ga(s(T34), s(T36)) → U3_ga(T34, T36, add21_in_ga(T34, T36))
U3_ga(T34, T36, add21_out_ga(T34, T36)) → add21_out_ga(s(T34), s(T36))
U18_ga(T7, add21_out_ga(T9, T7)) → fib1_out_ga(s(s(0)), T7)
fib1_in_ga(s(s(s(T41))), T7) → U19_ga(T41, T7, fib48_in_ga(T41, X80))
fib48_in_ga(0, s(0)) → fib48_out_ga(0, s(0))
fib48_in_ga(s(T45), X97) → U4_ga(T45, X97, p57_in_gaaa(T45, X95, X96, X97))
p57_in_gaaa(T45, X95, X96, X97) → U5_gaaa(T45, X95, X96, X97, fib48_in_ga(T45, X95))
U5_gaaa(T45, X95, X96, X97, fib48_out_ga(T45, X95)) → p57_out_gaaa(T45, X95, X96, X97)
p57_in_gaaa(T45, T46, X96, X97) → U6_gaaa(T45, T46, X96, X97, fib48_in_ga(T45, T46))
U6_gaaa(T45, T46, X96, X97, fib48_out_ga(T45, T46)) → U7_gaaa(T45, T46, X96, X97, fib61_in_ga(T45, X96))
fib61_in_ga(0, 0) → fib61_out_ga(0, 0)
fib61_in_ga(s(0), s(0)) → fib61_out_ga(s(0), s(0))
fib61_in_ga(s(s(T50)), X112) → U13_ga(T50, X112, p57_in_gaaa(T50, X110, X111, X112))
p57_in_gaaa(T45, T46, T47, X97) → U8_gaaa(T45, T46, T47, X97, fib48_in_ga(T45, T46))
U8_gaaa(T45, T46, T47, X97, fib48_out_ga(T45, T46)) → U9_gaaa(T45, T46, T47, X97, fib61_in_ga(T45, T47))
U9_gaaa(T45, T46, T47, X97, fib61_out_ga(T45, T47)) → U10_gaaa(T45, T46, T47, X97, add62_in_aaa(T46, T47, X97))
add62_in_aaa(0, 0, 0) → add62_out_aaa(0, 0, 0)
add62_in_aaa(s(T59), T60, s(X134)) → U11_aaa(T59, T60, X134, add62_in_aaa(T59, T60, X134))
add62_in_aaa(T65, s(T66), s(X149)) → U12_aaa(T65, T66, X149, add62_in_aaa(T65, T66, X149))
U12_aaa(T65, T66, X149, add62_out_aaa(T65, T66, X149)) → add62_out_aaa(T65, s(T66), s(X149))
U11_aaa(T59, T60, X134, add62_out_aaa(T59, T60, X134)) → add62_out_aaa(s(T59), T60, s(X134))
U10_gaaa(T45, T46, T47, X97, add62_out_aaa(T46, T47, X97)) → p57_out_gaaa(T45, T46, T47, X97)
U13_ga(T50, X112, p57_out_gaaa(T50, X110, X111, X112)) → fib61_out_ga(s(s(T50)), X112)
U7_gaaa(T45, T46, X96, X97, fib61_out_ga(T45, X96)) → p57_out_gaaa(T45, T46, X96, X97)
U4_ga(T45, X97, p57_out_gaaa(T45, X95, X96, X97)) → fib48_out_ga(s(T45), X97)
U19_ga(T41, T7, fib48_out_ga(T41, X80)) → fib1_out_ga(s(s(s(T41))), T7)
fib1_in_ga(s(s(s(T41))), T7) → U20_ga(T41, T7, fib48_in_ga(T41, T42))
U20_ga(T41, T7, fib48_out_ga(T41, T42)) → U21_ga(T41, T7, fib61_in_ga(T41, X81))
U21_ga(T41, T7, fib61_out_ga(T41, X81)) → fib1_out_ga(s(s(s(T41))), T7)
U20_ga(T41, T7, fib48_out_ga(T41, T42)) → U22_ga(T41, T7, T42, fib61_in_ga(T41, T67))
U22_ga(T41, T7, T42, fib61_out_ga(T41, T67)) → U23_ga(T41, T7, add62_in_aaa(T42, T67, X82))
U23_ga(T41, T7, add62_out_aaa(T42, T67, X82)) → fib1_out_ga(s(s(s(T41))), T7)
U22_ga(T41, T7, T42, fib61_out_ga(T41, T67)) → U24_ga(T41, T7, add62_in_aaa(T42, T67, T68))
U24_ga(T41, T7, add62_out_aaa(T42, T67, T68)) → U25_ga(T41, T7, fib48_in_ga(T41, X10))
U25_ga(T41, T7, fib48_out_ga(T41, X10)) → fib1_out_ga(s(s(s(T41))), T7)
U24_ga(T41, T7, add62_out_aaa(T42, T67, T68)) → U26_ga(T41, T7, T68, fib48_in_ga(T41, T69))
U26_ga(T41, T7, T68, fib48_out_ga(T41, T69)) → U27_ga(T41, T7, add93_in_gaa(T68, T69, T7))
add93_in_gaa(0, 0, 0) → add93_out_gaa(0, 0, 0)
add93_in_gaa(s(T82), T83, s(T85)) → U14_gaa(T82, T83, T85, add93_in_gaa(T82, T83, T85))
add93_in_gaa(T92, s(T93), s(T95)) → U15_gaa(T92, T93, T95, add93_in_gaa(T92, T93, T95))
U15_gaa(T92, T93, T95, add93_out_gaa(T92, T93, T95)) → add93_out_gaa(T92, s(T93), s(T95))
U14_gaa(T82, T83, T85, add93_out_gaa(T82, T83, T85)) → add93_out_gaa(s(T82), T83, s(T85))
U27_ga(T41, T7, add93_out_gaa(T68, T69, T7)) → fib1_out_ga(s(s(s(T41))), T7)

(40) UsableRulesProof (EQUIVALENT transformation)

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

(41) Obligation:

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

ADD21_IN_GA(s(T34), s(T36)) → ADD21_IN_GA(T34, T36)

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

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

(42) PiDPToQDPProof (SOUND transformation)

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

(43) Obligation:

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

ADD21_IN_GA(s(T34)) → ADD21_IN_GA(T34)

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

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

ADD21_IN_GA(s(T34)) → ADD21_IN_GA(T34)
The graph contains the following edges 1 > 1

(45) YES

(46) PrologToPiTRSProof (SOUND transformation)

fib1_in_ga(0, 0) → fib1_out_ga(0, 0)
fib1_in_ga(s(0), s(0)) → fib1_out_ga(s(0), s(0))
fib1_in_ga(s(s(0)), T7) → U16_ga(T7, fib20_in_a(X10))
fib20_in_a(0) → fib20_out_a(0)
U16_ga(T7, fib20_out_a(X10)) → fib1_out_ga(s(s(0)), T7)
fib1_in_ga(s(s(0)), T7) → U17_ga(T7, fib20_in_a(T9))
U17_ga(T7, fib20_out_a(T9)) → U18_ga(T7, add21_in_ga(T9, T7))
add21_in_ga(T20, s(T22)) → U2_ga(T20, T22, add33_in_ga(T20, T22))
add33_in_ga(0, 0) → add33_out_ga(0, 0)
add33_in_ga(s(T27), s(T29)) → U1_ga(T27, T29, add33_in_ga(T27, T29))
U1_ga(T27, T29, add33_out_ga(T27, T29)) → add33_out_ga(s(T27), s(T29))
U2_ga(T20, T22, add33_out_ga(T20, T22)) → add21_out_ga(T20, s(T22))
add21_in_ga(s(T34), s(T36)) → U3_ga(T34, T36, add21_in_ga(T34, T36))
U3_ga(T34, T36, add21_out_ga(T34, T36)) → add21_out_ga(s(T34), s(T36))
U18_ga(T7, add21_out_ga(T9, T7)) → fib1_out_ga(s(s(0)), T7)
fib1_in_ga(s(s(s(T41))), T7) → U19_ga(T41, T7, fib48_in_ga(T41, X80))
fib48_in_ga(0, s(0)) → fib48_out_ga(0, s(0))
fib48_in_ga(s(T45), X97) → U4_ga(T45, X97, p57_in_gaaa(T45, X95, X96, X97))
p57_in_gaaa(T45, X95, X96, X97) → U5_gaaa(T45, X95, X96, X97, fib48_in_ga(T45, X95))
U5_gaaa(T45, X95, X96, X97, fib48_out_ga(T45, X95)) → p57_out_gaaa(T45, X95, X96, X97)
p57_in_gaaa(T45, T46, X96, X97) → U6_gaaa(T45, T46, X96, X97, fib48_in_ga(T45, T46))
U6_gaaa(T45, T46, X96, X97, fib48_out_ga(T45, T46)) → U7_gaaa(T45, T46, X96, X97, fib61_in_ga(T45, X96))
fib61_in_ga(0, 0) → fib61_out_ga(0, 0)
fib61_in_ga(s(0), s(0)) → fib61_out_ga(s(0), s(0))
fib61_in_ga(s(s(T50)), X112) → U13_ga(T50, X112, p57_in_gaaa(T50, X110, X111, X112))
p57_in_gaaa(T45, T46, T47, X97) → U8_gaaa(T45, T46, T47, X97, fib48_in_ga(T45, T46))
U8_gaaa(T45, T46, T47, X97, fib48_out_ga(T45, T46)) → U9_gaaa(T45, T46, T47, X97, fib61_in_ga(T45, T47))
U9_gaaa(T45, T46, T47, X97, fib61_out_ga(T45, T47)) → U10_gaaa(T45, T46, T47, X97, add62_in_aaa(T46, T47, X97))
add62_in_aaa(0, 0, 0) → add62_out_aaa(0, 0, 0)
add62_in_aaa(s(T59), T60, s(X134)) → U11_aaa(T59, T60, X134, add62_in_aaa(T59, T60, X134))
add62_in_aaa(T65, s(T66), s(X149)) → U12_aaa(T65, T66, X149, add62_in_aaa(T65, T66, X149))
U12_aaa(T65, T66, X149, add62_out_aaa(T65, T66, X149)) → add62_out_aaa(T65, s(T66), s(X149))
U11_aaa(T59, T60, X134, add62_out_aaa(T59, T60, X134)) → add62_out_aaa(s(T59), T60, s(X134))
U10_gaaa(T45, T46, T47, X97, add62_out_aaa(T46, T47, X97)) → p57_out_gaaa(T45, T46, T47, X97)
U13_ga(T50, X112, p57_out_gaaa(T50, X110, X111, X112)) → fib61_out_ga(s(s(T50)), X112)
U7_gaaa(T45, T46, X96, X97, fib61_out_ga(T45, X96)) → p57_out_gaaa(T45, T46, X96, X97)
U4_ga(T45, X97, p57_out_gaaa(T45, X95, X96, X97)) → fib48_out_ga(s(T45), X97)
U19_ga(T41, T7, fib48_out_ga(T41, X80)) → fib1_out_ga(s(s(s(T41))), T7)
fib1_in_ga(s(s(s(T41))), T7) → U20_ga(T41, T7, fib48_in_ga(T41, T42))
U20_ga(T41, T7, fib48_out_ga(T41, T42)) → U21_ga(T41, T7, fib61_in_ga(T41, X81))
U21_ga(T41, T7, fib61_out_ga(T41, X81)) → fib1_out_ga(s(s(s(T41))), T7)
U20_ga(T41, T7, fib48_out_ga(T41, T42)) → U22_ga(T41, T7, T42, fib61_in_ga(T41, T67))
U22_ga(T41, T7, T42, fib61_out_ga(T41, T67)) → U23_ga(T41, T7, add62_in_aaa(T42, T67, X82))
U23_ga(T41, T7, add62_out_aaa(T42, T67, X82)) → fib1_out_ga(s(s(s(T41))), T7)
U22_ga(T41, T7, T42, fib61_out_ga(T41, T67)) → U24_ga(T41, T7, add62_in_aaa(T42, T67, T68))
U24_ga(T41, T7, add62_out_aaa(T42, T67, T68)) → U25_ga(T41, T7, fib48_in_ga(T41, X10))
U25_ga(T41, T7, fib48_out_ga(T41, X10)) → fib1_out_ga(s(s(s(T41))), T7)
U24_ga(T41, T7, add62_out_aaa(T42, T67, T68)) → U26_ga(T41, T7, T68, fib48_in_ga(T41, T69))
U26_ga(T41, T7, T68, fib48_out_ga(T41, T69)) → U27_ga(T41, T7, add93_in_gaa(T68, T69, T7))
add93_in_gaa(0, 0, 0) → add93_out_gaa(0, 0, 0)
add93_in_gaa(s(T82), T83, s(T85)) → U14_gaa(T82, T83, T85, add93_in_gaa(T82, T83, T85))
add93_in_gaa(T92, s(T93), s(T95)) → U15_gaa(T92, T93, T95, add93_in_gaa(T92, T93, T95))
U15_gaa(T92, T93, T95, add93_out_gaa(T92, T93, T95)) → add93_out_gaa(T92, s(T93), s(T95))
U14_gaa(T82, T83, T85, add93_out_gaa(T82, T83, T85)) → add93_out_gaa(s(T82), T83, s(T85))
U27_ga(T41, T7, add93_out_gaa(T68, T69, T7)) → fib1_out_ga(s(s(s(T41))), T7)

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog

(47) Obligation:

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

fib1_in_ga(0, 0) → fib1_out_ga(0, 0)
fib1_in_ga(s(0), s(0)) → fib1_out_ga(s(0), s(0))
fib1_in_ga(s(s(0)), T7) → U16_ga(T7, fib20_in_a(X10))
fib20_in_a(0) → fib20_out_a(0)
U16_ga(T7, fib20_out_a(X10)) → fib1_out_ga(s(s(0)), T7)
fib1_in_ga(s(s(0)), T7) → U17_ga(T7, fib20_in_a(T9))
U17_ga(T7, fib20_out_a(T9)) → U18_ga(T7, add21_in_ga(T9, T7))
add21_in_ga(T20, s(T22)) → U2_ga(T20, T22, add33_in_ga(T20, T22))
add33_in_ga(0, 0) → add33_out_ga(0, 0)
add33_in_ga(s(T27), s(T29)) → U1_ga(T27, T29, add33_in_ga(T27, T29))
U1_ga(T27, T29, add33_out_ga(T27, T29)) → add33_out_ga(s(T27), s(T29))
U2_ga(T20, T22, add33_out_ga(T20, T22)) → add21_out_ga(T20, s(T22))
add21_in_ga(s(T34), s(T36)) → U3_ga(T34, T36, add21_in_ga(T34, T36))
U3_ga(T34, T36, add21_out_ga(T34, T36)) → add21_out_ga(s(T34), s(T36))
U18_ga(T7, add21_out_ga(T9, T7)) → fib1_out_ga(s(s(0)), T7)
fib1_in_ga(s(s(s(T41))), T7) → U19_ga(T41, T7, fib48_in_ga(T41, X80))
fib48_in_ga(0, s(0)) → fib48_out_ga(0, s(0))
fib48_in_ga(s(T45), X97) → U4_ga(T45, X97, p57_in_gaaa(T45, X95, X96, X97))
p57_in_gaaa(T45, X95, X96, X97) → U5_gaaa(T45, X95, X96, X97, fib48_in_ga(T45, X95))
U5_gaaa(T45, X95, X96, X97, fib48_out_ga(T45, X95)) → p57_out_gaaa(T45, X95, X96, X97)
p57_in_gaaa(T45, T46, X96, X97) → U6_gaaa(T45, T46, X96, X97, fib48_in_ga(T45, T46))
U6_gaaa(T45, T46, X96, X97, fib48_out_ga(T45, T46)) → U7_gaaa(T45, T46, X96, X97, fib61_in_ga(T45, X96))
fib61_in_ga(0, 0) → fib61_out_ga(0, 0)
fib61_in_ga(s(0), s(0)) → fib61_out_ga(s(0), s(0))
fib61_in_ga(s(s(T50)), X112) → U13_ga(T50, X112, p57_in_gaaa(T50, X110, X111, X112))
p57_in_gaaa(T45, T46, T47, X97) → U8_gaaa(T45, T46, T47, X97, fib48_in_ga(T45, T46))
U8_gaaa(T45, T46, T47, X97, fib48_out_ga(T45, T46)) → U9_gaaa(T45, T46, T47, X97, fib61_in_ga(T45, T47))
U9_gaaa(T45, T46, T47, X97, fib61_out_ga(T45, T47)) → U10_gaaa(T45, T46, T47, X97, add62_in_aaa(T46, T47, X97))
add62_in_aaa(0, 0, 0) → add62_out_aaa(0, 0, 0)
add62_in_aaa(s(T59), T60, s(X134)) → U11_aaa(T59, T60, X134, add62_in_aaa(T59, T60, X134))
add62_in_aaa(T65, s(T66), s(X149)) → U12_aaa(T65, T66, X149, add62_in_aaa(T65, T66, X149))
U12_aaa(T65, T66, X149, add62_out_aaa(T65, T66, X149)) → add62_out_aaa(T65, s(T66), s(X149))
U11_aaa(T59, T60, X134, add62_out_aaa(T59, T60, X134)) → add62_out_aaa(s(T59), T60, s(X134))
U10_gaaa(T45, T46, T47, X97, add62_out_aaa(T46, T47, X97)) → p57_out_gaaa(T45, T46, T47, X97)
U13_ga(T50, X112, p57_out_gaaa(T50, X110, X111, X112)) → fib61_out_ga(s(s(T50)), X112)
U7_gaaa(T45, T46, X96, X97, fib61_out_ga(T45, X96)) → p57_out_gaaa(T45, T46, X96, X97)
U4_ga(T45, X97, p57_out_gaaa(T45, X95, X96, X97)) → fib48_out_ga(s(T45), X97)
U19_ga(T41, T7, fib48_out_ga(T41, X80)) → fib1_out_ga(s(s(s(T41))), T7)
fib1_in_ga(s(s(s(T41))), T7) → U20_ga(T41, T7, fib48_in_ga(T41, T42))
U20_ga(T41, T7, fib48_out_ga(T41, T42)) → U21_ga(T41, T7, fib61_in_ga(T41, X81))
U21_ga(T41, T7, fib61_out_ga(T41, X81)) → fib1_out_ga(s(s(s(T41))), T7)
U20_ga(T41, T7, fib48_out_ga(T41, T42)) → U22_ga(T41, T7, T42, fib61_in_ga(T41, T67))
U22_ga(T41, T7, T42, fib61_out_ga(T41, T67)) → U23_ga(T41, T7, add62_in_aaa(T42, T67, X82))
U23_ga(T41, T7, add62_out_aaa(T42, T67, X82)) → fib1_out_ga(s(s(s(T41))), T7)
U22_ga(T41, T7, T42, fib61_out_ga(T41, T67)) → U24_ga(T41, T7, add62_in_aaa(T42, T67, T68))
U24_ga(T41, T7, add62_out_aaa(T42, T67, T68)) → U25_ga(T41, T7, fib48_in_ga(T41, X10))
U25_ga(T41, T7, fib48_out_ga(T41, X10)) → fib1_out_ga(s(s(s(T41))), T7)
U24_ga(T41, T7, add62_out_aaa(T42, T67, T68)) → U26_ga(T41, T7, T68, fib48_in_ga(T41, T69))
U26_ga(T41, T7, T68, fib48_out_ga(T41, T69)) → U27_ga(T41, T7, add93_in_gaa(T68, T69, T7))
add93_in_gaa(0, 0, 0) → add93_out_gaa(0, 0, 0)
add93_in_gaa(s(T82), T83, s(T85)) → U14_gaa(T82, T83, T85, add93_in_gaa(T82, T83, T85))
add93_in_gaa(T92, s(T93), s(T95)) → U15_gaa(T92, T93, T95, add93_in_gaa(T92, T93, T95))
U15_gaa(T92, T93, T95, add93_out_gaa(T92, T93, T95)) → add93_out_gaa(T92, s(T93), s(T95))
U14_gaa(T82, T83, T85, add93_out_gaa(T82, T83, T85)) → add93_out_gaa(s(T82), T83, s(T85))
U27_ga(T41, T7, add93_out_gaa(T68, T69, T7)) → fib1_out_ga(s(s(s(T41))), T7)

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

FIB1_IN_GA(s(s(0)), T7) → U16_GA(T7, fib20_in_a(X10))
FIB1_IN_GA(s(s(0)), T7) → FIB20_IN_A(X10)
FIB1_IN_GA(s(s(0)), T7) → U17_GA(T7, fib20_in_a(T9))
U17_GA(T7, fib20_out_a(T9)) → U18_GA(T7, add21_in_ga(T9, T7))
U17_GA(T7, fib20_out_a(T9)) → ADD21_IN_GA(T9, T7)
ADD21_IN_GA(T20, s(T22)) → U2_GA(T20, T22, add33_in_ga(T20, T22))
ADD21_IN_GA(T20, s(T22)) → ADD33_IN_GA(T20, T22)
ADD33_IN_GA(s(T27), s(T29)) → U1_GA(T27, T29, add33_in_ga(T27, T29))
ADD33_IN_GA(s(T27), s(T29)) → ADD33_IN_GA(T27, T29)
ADD21_IN_GA(s(T34), s(T36)) → U3_GA(T34, T36, add21_in_ga(T34, T36))
ADD21_IN_GA(s(T34), s(T36)) → ADD21_IN_GA(T34, T36)
FIB1_IN_GA(s(s(s(T41))), T7) → U19_GA(T41, T7, fib48_in_ga(T41, X80))
FIB1_IN_GA(s(s(s(T41))), T7) → FIB48_IN_GA(T41, X80)
FIB48_IN_GA(s(T45), X97) → U4_GA(T45, X97, p57_in_gaaa(T45, X95, X96, X97))
FIB48_IN_GA(s(T45), X97) → P57_IN_GAAA(T45, X95, X96, X97)
P57_IN_GAAA(T45, X95, X96, X97) → U5_GAAA(T45, X95, X96, X97, fib48_in_ga(T45, X95))
P57_IN_GAAA(T45, X95, X96, X97) → FIB48_IN_GA(T45, X95)
P57_IN_GAAA(T45, T46, X96, X97) → U6_GAAA(T45, T46, X96, X97, fib48_in_ga(T45, T46))
U6_GAAA(T45, T46, X96, X97, fib48_out_ga(T45, T46)) → U7_GAAA(T45, T46, X96, X97, fib61_in_ga(T45, X96))
U6_GAAA(T45, T46, X96, X97, fib48_out_ga(T45, T46)) → FIB61_IN_GA(T45, X96)
FIB61_IN_GA(s(s(T50)), X112) → U13_GA(T50, X112, p57_in_gaaa(T50, X110, X111, X112))
FIB61_IN_GA(s(s(T50)), X112) → P57_IN_GAAA(T50, X110, X111, X112)
P57_IN_GAAA(T45, T46, T47, X97) → U8_GAAA(T45, T46, T47, X97, fib48_in_ga(T45, T46))
U8_GAAA(T45, T46, T47, X97, fib48_out_ga(T45, T46)) → U9_GAAA(T45, T46, T47, X97, fib61_in_ga(T45, T47))
U8_GAAA(T45, T46, T47, X97, fib48_out_ga(T45, T46)) → FIB61_IN_GA(T45, T47)
U9_GAAA(T45, T46, T47, X97, fib61_out_ga(T45, T47)) → U10_GAAA(T45, T46, T47, X97, add62_in_aaa(T46, T47, X97))
U9_GAAA(T45, T46, T47, X97, fib61_out_ga(T45, T47)) → ADD62_IN_AAA(T46, T47, X97)
ADD62_IN_AAA(s(T59), T60, s(X134)) → U11_AAA(T59, T60, X134, add62_in_aaa(T59, T60, X134))
ADD62_IN_AAA(s(T59), T60, s(X134)) → ADD62_IN_AAA(T59, T60, X134)
ADD62_IN_AAA(T65, s(T66), s(X149)) → U12_AAA(T65, T66, X149, add62_in_aaa(T65, T66, X149))
ADD62_IN_AAA(T65, s(T66), s(X149)) → ADD62_IN_AAA(T65, T66, X149)
FIB1_IN_GA(s(s(s(T41))), T7) → U20_GA(T41, T7, fib48_in_ga(T41, T42))
U20_GA(T41, T7, fib48_out_ga(T41, T42)) → U21_GA(T41, T7, fib61_in_ga(T41, X81))
U20_GA(T41, T7, fib48_out_ga(T41, T42)) → FIB61_IN_GA(T41, X81)
U20_GA(T41, T7, fib48_out_ga(T41, T42)) → U22_GA(T41, T7, T42, fib61_in_ga(T41, T67))
U22_GA(T41, T7, T42, fib61_out_ga(T41, T67)) → U23_GA(T41, T7, add62_in_aaa(T42, T67, X82))
U22_GA(T41, T7, T42, fib61_out_ga(T41, T67)) → ADD62_IN_AAA(T42, T67, X82)
U22_GA(T41, T7, T42, fib61_out_ga(T41, T67)) → U24_GA(T41, T7, add62_in_aaa(T42, T67, T68))
U24_GA(T41, T7, add62_out_aaa(T42, T67, T68)) → U25_GA(T41, T7, fib48_in_ga(T41, X10))
U24_GA(T41, T7, add62_out_aaa(T42, T67, T68)) → FIB48_IN_GA(T41, X10)
U24_GA(T41, T7, add62_out_aaa(T42, T67, T68)) → U26_GA(T41, T7, T68, fib48_in_ga(T41, T69))
U26_GA(T41, T7, T68, fib48_out_ga(T41, T69)) → U27_GA(T41, T7, add93_in_gaa(T68, T69, T7))
U26_GA(T41, T7, T68, fib48_out_ga(T41, T69)) → ADD93_IN_GAA(T68, T69, T7)
ADD93_IN_GAA(s(T82), T83, s(T85)) → U14_GAA(T82, T83, T85, add93_in_gaa(T82, T83, T85))
ADD93_IN_GAA(s(T82), T83, s(T85)) → ADD93_IN_GAA(T82, T83, T85)
ADD93_IN_GAA(T92, s(T93), s(T95)) → U15_GAA(T92, T93, T95, add93_in_gaa(T92, T93, T95))
ADD93_IN_GAA(T92, s(T93), s(T95)) → ADD93_IN_GAA(T92, T93, T95)

The TRS R consists of the following rules:

fib1_in_ga(0, 0) → fib1_out_ga(0, 0)
fib1_in_ga(s(0), s(0)) → fib1_out_ga(s(0), s(0))
fib1_in_ga(s(s(0)), T7) → U16_ga(T7, fib20_in_a(X10))
fib20_in_a(0) → fib20_out_a(0)
U16_ga(T7, fib20_out_a(X10)) → fib1_out_ga(s(s(0)), T7)
fib1_in_ga(s(s(0)), T7) → U17_ga(T7, fib20_in_a(T9))
U17_ga(T7, fib20_out_a(T9)) → U18_ga(T7, add21_in_ga(T9, T7))
add21_in_ga(T20, s(T22)) → U2_ga(T20, T22, add33_in_ga(T20, T22))
add33_in_ga(0, 0) → add33_out_ga(0, 0)
add33_in_ga(s(T27), s(T29)) → U1_ga(T27, T29, add33_in_ga(T27, T29))
U1_ga(T27, T29, add33_out_ga(T27, T29)) → add33_out_ga(s(T27), s(T29))
U2_ga(T20, T22, add33_out_ga(T20, T22)) → add21_out_ga(T20, s(T22))
add21_in_ga(s(T34), s(T36)) → U3_ga(T34, T36, add21_in_ga(T34, T36))
U3_ga(T34, T36, add21_out_ga(T34, T36)) → add21_out_ga(s(T34), s(T36))
U18_ga(T7, add21_out_ga(T9, T7)) → fib1_out_ga(s(s(0)), T7)
fib1_in_ga(s(s(s(T41))), T7) → U19_ga(T41, T7, fib48_in_ga(T41, X80))
fib48_in_ga(0, s(0)) → fib48_out_ga(0, s(0))
fib48_in_ga(s(T45), X97) → U4_ga(T45, X97, p57_in_gaaa(T45, X95, X96, X97))
p57_in_gaaa(T45, X95, X96, X97) → U5_gaaa(T45, X95, X96, X97, fib48_in_ga(T45, X95))
U5_gaaa(T45, X95, X96, X97, fib48_out_ga(T45, X95)) → p57_out_gaaa(T45, X95, X96, X97)
p57_in_gaaa(T45, T46, X96, X97) → U6_gaaa(T45, T46, X96, X97, fib48_in_ga(T45, T46))
U6_gaaa(T45, T46, X96, X97, fib48_out_ga(T45, T46)) → U7_gaaa(T45, T46, X96, X97, fib61_in_ga(T45, X96))
fib61_in_ga(0, 0) → fib61_out_ga(0, 0)
fib61_in_ga(s(0), s(0)) → fib61_out_ga(s(0), s(0))
fib61_in_ga(s(s(T50)), X112) → U13_ga(T50, X112, p57_in_gaaa(T50, X110, X111, X112))
p57_in_gaaa(T45, T46, T47, X97) → U8_gaaa(T45, T46, T47, X97, fib48_in_ga(T45, T46))
U8_gaaa(T45, T46, T47, X97, fib48_out_ga(T45, T46)) → U9_gaaa(T45, T46, T47, X97, fib61_in_ga(T45, T47))
U9_gaaa(T45, T46, T47, X97, fib61_out_ga(T45, T47)) → U10_gaaa(T45, T46, T47, X97, add62_in_aaa(T46, T47, X97))
add62_in_aaa(0, 0, 0) → add62_out_aaa(0, 0, 0)
add62_in_aaa(s(T59), T60, s(X134)) → U11_aaa(T59, T60, X134, add62_in_aaa(T59, T60, X134))
add62_in_aaa(T65, s(T66), s(X149)) → U12_aaa(T65, T66, X149, add62_in_aaa(T65, T66, X149))
U12_aaa(T65, T66, X149, add62_out_aaa(T65, T66, X149)) → add62_out_aaa(T65, s(T66), s(X149))
U11_aaa(T59, T60, X134, add62_out_aaa(T59, T60, X134)) → add62_out_aaa(s(T59), T60, s(X134))
U10_gaaa(T45, T46, T47, X97, add62_out_aaa(T46, T47, X97)) → p57_out_gaaa(T45, T46, T47, X97)
U13_ga(T50, X112, p57_out_gaaa(T50, X110, X111, X112)) → fib61_out_ga(s(s(T50)), X112)
U7_gaaa(T45, T46, X96, X97, fib61_out_ga(T45, X96)) → p57_out_gaaa(T45, T46, X96, X97)
U4_ga(T45, X97, p57_out_gaaa(T45, X95, X96, X97)) → fib48_out_ga(s(T45), X97)
U19_ga(T41, T7, fib48_out_ga(T41, X80)) → fib1_out_ga(s(s(s(T41))), T7)
fib1_in_ga(s(s(s(T41))), T7) → U20_ga(T41, T7, fib48_in_ga(T41, T42))
U20_ga(T41, T7, fib48_out_ga(T41, T42)) → U21_ga(T41, T7, fib61_in_ga(T41, X81))
U21_ga(T41, T7, fib61_out_ga(T41, X81)) → fib1_out_ga(s(s(s(T41))), T7)
U20_ga(T41, T7, fib48_out_ga(T41, T42)) → U22_ga(T41, T7, T42, fib61_in_ga(T41, T67))
U22_ga(T41, T7, T42, fib61_out_ga(T41, T67)) → U23_ga(T41, T7, add62_in_aaa(T42, T67, X82))
U23_ga(T41, T7, add62_out_aaa(T42, T67, X82)) → fib1_out_ga(s(s(s(T41))), T7)
U22_ga(T41, T7, T42, fib61_out_ga(T41, T67)) → U24_ga(T41, T7, add62_in_aaa(T42, T67, T68))
U24_ga(T41, T7, add62_out_aaa(T42, T67, T68)) → U25_ga(T41, T7, fib48_in_ga(T41, X10))
U25_ga(T41, T7, fib48_out_ga(T41, X10)) → fib1_out_ga(s(s(s(T41))), T7)
U24_ga(T41, T7, add62_out_aaa(T42, T67, T68)) → U26_ga(T41, T7, T68, fib48_in_ga(T41, T69))
U26_ga(T41, T7, T68, fib48_out_ga(T41, T69)) → U27_ga(T41, T7, add93_in_gaa(T68, T69, T7))
add93_in_gaa(0, 0, 0) → add93_out_gaa(0, 0, 0)
add93_in_gaa(s(T82), T83, s(T85)) → U14_gaa(T82, T83, T85, add93_in_gaa(T82, T83, T85))
add93_in_gaa(T92, s(T93), s(T95)) → U15_gaa(T92, T93, T95, add93_in_gaa(T92, T93, T95))
U15_gaa(T92, T93, T95, add93_out_gaa(T92, T93, T95)) → add93_out_gaa(T92, s(T93), s(T95))
U14_gaa(T82, T83, T85, add93_out_gaa(T82, T83, T85)) → add93_out_gaa(s(T82), T83, s(T85))
U27_ga(T41, T7, add93_out_gaa(T68, T69, T7)) → fib1_out_ga(s(s(s(T41))), T7)

The argument filtering Pi contains the following mapping:
fib1_in_ga(x1, x2) = fib1_in_ga(x1)
0 = 0
fib1_out_ga(x1, x2) = fib1_out_ga
s(x1) = s(x1)
U16_ga(x1, x2) = U16_ga(x2)
fib20_in_a(x1) = fib20_in_a
fib20_out_a(x1) = fib20_out_a(x1)
U17_ga(x1, x2) = U17_ga(x2)
U18_ga(x1, x2) = U18_ga(x2)
add21_in_ga(x1, x2) = add21_in_ga(x1)
U2_ga(x1, x2, x3) = U2_ga(x3)
add33_in_ga(x1, x2) = add33_in_ga(x1)
add33_out_ga(x1, x2) = add33_out_ga(x2)
U1_ga(x1, x2, x3) = U1_ga(x3)
add21_out_ga(x1, x2) = add21_out_ga(x2)
U3_ga(x1, x2, x3) = U3_ga(x3)
U19_ga(x1, x2, x3) = U19_ga(x3)
fib48_in_ga(x1, x2) = fib48_in_ga(x1)
fib48_out_ga(x1, x2) = fib48_out_ga
U4_ga(x1, x2, x3) = U4_ga(x3)
p57_in_gaaa(x1, x2, x3, x4) = p57_in_gaaa(x1)
U5_gaaa(x1, x2, x3, x4, x5) = U5_gaaa(x5)
p57_out_gaaa(x1, x2, x3, x4) = p57_out_gaaa
U6_gaaa(x1, x2, x3, x4, x5) = U6_gaaa(x1, x5)
U7_gaaa(x1, x2, x3, x4, x5) = U7_gaaa(x5)
fib61_in_ga(x1, x2) = fib61_in_ga(x1)
fib61_out_ga(x1, x2) = fib61_out_ga
U13_ga(x1, x2, x3) = U13_ga(x3)
U8_gaaa(x1, x2, x3, x4, x5) = U8_gaaa(x1, x5)
U9_gaaa(x1, x2, x3, x4, x5) = U9_gaaa(x5)
U10_gaaa(x1, x2, x3, x4, x5) = U10_gaaa(x5)
add62_in_aaa(x1, x2, x3) = add62_in_aaa
add62_out_aaa(x1, x2, x3) = add62_out_aaa(x1, x2, x3)
U11_aaa(x1, x2, x3, x4) = U11_aaa(x4)
U12_aaa(x1, x2, x3, x4) = U12_aaa(x4)
U20_ga(x1, x2, x3) = U20_ga(x1, x3)
U21_ga(x1, x2, x3) = U21_ga(x3)
U22_ga(x1, x2, x3, x4) = U22_ga(x1, x4)
U23_ga(x1, x2, x3) = U23_ga(x3)
U24_ga(x1, x2, x3) = U24_ga(x1, x3)
U25_ga(x1, x2, x3) = U25_ga(x3)
U26_ga(x1, x2, x3, x4) = U26_ga(x3, x4)
U27_ga(x1, x2, x3) = U27_ga(x3)
add93_in_gaa(x1, x2, x3) = add93_in_gaa(x1)
add93_out_gaa(x1, x2, x3) = add93_out_gaa(x2, x3)
U14_gaa(x1, x2, x3, x4) = U14_gaa(x4)
U15_gaa(x1, x2, x3, x4) = U15_gaa(x4)
FIB1_IN_GA(x1, x2) = FIB1_IN_GA(x1)
U16_GA(x1, x2) = U16_GA(x2)
FIB20_IN_A(x1) = FIB20_IN_A
U17_GA(x1, x2) = U17_GA(x2)
U18_GA(x1, x2) = U18_GA(x2)
ADD21_IN_GA(x1, x2) = ADD21_IN_GA(x1)
U2_GA(x1, x2, x3) = U2_GA(x3)
ADD33_IN_GA(x1, x2) = ADD33_IN_GA(x1)
U1_GA(x1, x2, x3) = U1_GA(x3)
U3_GA(x1, x2, x3) = U3_GA(x3)
U19_GA(x1, x2, x3) = U19_GA(x3)
FIB48_IN_GA(x1, x2) = FIB48_IN_GA(x1)
U4_GA(x1, x2, x3) = U4_GA(x3)
P57_IN_GAAA(x1, x2, x3, x4) = P57_IN_GAAA(x1)
U5_GAAA(x1, x2, x3, x4, x5) = U5_GAAA(x5)
U6_GAAA(x1, x2, x3, x4, x5) = U6_GAAA(x1, x5)
U7_GAAA(x1, x2, x3, x4, x5) = U7_GAAA(x5)
FIB61_IN_GA(x1, x2) = FIB61_IN_GA(x1)
U13_GA(x1, x2, x3) = U13_GA(x3)
U8_GAAA(x1, x2, x3, x4, x5) = U8_GAAA(x1, x5)
U9_GAAA(x1, x2, x3, x4, x5) = U9_GAAA(x5)
U10_GAAA(x1, x2, x3, x4, x5) = U10_GAAA(x5)
ADD62_IN_AAA(x1, x2, x3) = ADD62_IN_AAA
U11_AAA(x1, x2, x3, x4) = U11_AAA(x4)
U12_AAA(x1, x2, x3, x4) = U12_AAA(x4)
U20_GA(x1, x2, x3) = U20_GA(x1, x3)
U21_GA(x1, x2, x3) = U21_GA(x3)
U22_GA(x1, x2, x3, x4) = U22_GA(x1, x4)
U23_GA(x1, x2, x3) = U23_GA(x3)
U24_GA(x1, x2, x3) = U24_GA(x1, x3)
U25_GA(x1, x2, x3) = U25_GA(x3)
U26_GA(x1, x2, x3, x4) = U26_GA(x3, x4)
U27_GA(x1, x2, x3) = U27_GA(x3)
ADD93_IN_GAA(x1, x2, x3) = ADD93_IN_GAA(x1)
U14_GAA(x1, x2, x3, x4) = U14_GAA(x4)
U15_GAA(x1, x2, x3, x4) = U15_GAA(x4)

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

(49) Obligation:

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

FIB1_IN_GA(s(s(0)), T7) → U16_GA(T7, fib20_in_a(X10))
FIB1_IN_GA(s(s(0)), T7) → FIB20_IN_A(X10)
FIB1_IN_GA(s(s(0)), T7) → U17_GA(T7, fib20_in_a(T9))
U17_GA(T7, fib20_out_a(T9)) → U18_GA(T7, add21_in_ga(T9, T7))
U17_GA(T7, fib20_out_a(T9)) → ADD21_IN_GA(T9, T7)
ADD21_IN_GA(T20, s(T22)) → U2_GA(T20, T22, add33_in_ga(T20, T22))
ADD21_IN_GA(T20, s(T22)) → ADD33_IN_GA(T20, T22)
ADD33_IN_GA(s(T27), s(T29)) → U1_GA(T27, T29, add33_in_ga(T27, T29))
ADD33_IN_GA(s(T27), s(T29)) → ADD33_IN_GA(T27, T29)
ADD21_IN_GA(s(T34), s(T36)) → U3_GA(T34, T36, add21_in_ga(T34, T36))
ADD21_IN_GA(s(T34), s(T36)) → ADD21_IN_GA(T34, T36)
FIB1_IN_GA(s(s(s(T41))), T7) → U19_GA(T41, T7, fib48_in_ga(T41, X80))
FIB1_IN_GA(s(s(s(T41))), T7) → FIB48_IN_GA(T41, X80)
FIB48_IN_GA(s(T45), X97) → U4_GA(T45, X97, p57_in_gaaa(T45, X95, X96, X97))
FIB48_IN_GA(s(T45), X97) → P57_IN_GAAA(T45, X95, X96, X97)
P57_IN_GAAA(T45, X95, X96, X97) → U5_GAAA(T45, X95, X96, X97, fib48_in_ga(T45, X95))
P57_IN_GAAA(T45, X95, X96, X97) → FIB48_IN_GA(T45, X95)
P57_IN_GAAA(T45, T46, X96, X97) → U6_GAAA(T45, T46, X96, X97, fib48_in_ga(T45, T46))
U6_GAAA(T45, T46, X96, X97, fib48_out_ga(T45, T46)) → U7_GAAA(T45, T46, X96, X97, fib61_in_ga(T45, X96))
U6_GAAA(T45, T46, X96, X97, fib48_out_ga(T45, T46)) → FIB61_IN_GA(T45, X96)
FIB61_IN_GA(s(s(T50)), X112) → U13_GA(T50, X112, p57_in_gaaa(T50, X110, X111, X112))
FIB61_IN_GA(s(s(T50)), X112) → P57_IN_GAAA(T50, X110, X111, X112)
P57_IN_GAAA(T45, T46, T47, X97) → U8_GAAA(T45, T46, T47, X97, fib48_in_ga(T45, T46))
U8_GAAA(T45, T46, T47, X97, fib48_out_ga(T45, T46)) → U9_GAAA(T45, T46, T47, X97, fib61_in_ga(T45, T47))
U8_GAAA(T45, T46, T47, X97, fib48_out_ga(T45, T46)) → FIB61_IN_GA(T45, T47)
U9_GAAA(T45, T46, T47, X97, fib61_out_ga(T45, T47)) → U10_GAAA(T45, T46, T47, X97, add62_in_aaa(T46, T47, X97))
U9_GAAA(T45, T46, T47, X97, fib61_out_ga(T45, T47)) → ADD62_IN_AAA(T46, T47, X97)
ADD62_IN_AAA(s(T59), T60, s(X134)) → U11_AAA(T59, T60, X134, add62_in_aaa(T59, T60, X134))
ADD62_IN_AAA(s(T59), T60, s(X134)) → ADD62_IN_AAA(T59, T60, X134)
ADD62_IN_AAA(T65, s(T66), s(X149)) → U12_AAA(T65, T66, X149, add62_in_aaa(T65, T66, X149))
ADD62_IN_AAA(T65, s(T66), s(X149)) → ADD62_IN_AAA(T65, T66, X149)
FIB1_IN_GA(s(s(s(T41))), T7) → U20_GA(T41, T7, fib48_in_ga(T41, T42))
U20_GA(T41, T7, fib48_out_ga(T41, T42)) → U21_GA(T41, T7, fib61_in_ga(T41, X81))
U20_GA(T41, T7, fib48_out_ga(T41, T42)) → FIB61_IN_GA(T41, X81)
U20_GA(T41, T7, fib48_out_ga(T41, T42)) → U22_GA(T41, T7, T42, fib61_in_ga(T41, T67))
U22_GA(T41, T7, T42, fib61_out_ga(T41, T67)) → U23_GA(T41, T7, add62_in_aaa(T42, T67, X82))
U22_GA(T41, T7, T42, fib61_out_ga(T41, T67)) → ADD62_IN_AAA(T42, T67, X82)
U22_GA(T41, T7, T42, fib61_out_ga(T41, T67)) → U24_GA(T41, T7, add62_in_aaa(T42, T67, T68))
U24_GA(T41, T7, add62_out_aaa(T42, T67, T68)) → U25_GA(T41, T7, fib48_in_ga(T41, X10))
U24_GA(T41, T7, add62_out_aaa(T42, T67, T68)) → FIB48_IN_GA(T41, X10)
U24_GA(T41, T7, add62_out_aaa(T42, T67, T68)) → U26_GA(T41, T7, T68, fib48_in_ga(T41, T69))
U26_GA(T41, T7, T68, fib48_out_ga(T41, T69)) → U27_GA(T41, T7, add93_in_gaa(T68, T69, T7))
U26_GA(T41, T7, T68, fib48_out_ga(T41, T69)) → ADD93_IN_GAA(T68, T69, T7)
ADD93_IN_GAA(s(T82), T83, s(T85)) → U14_GAA(T82, T83, T85, add93_in_gaa(T82, T83, T85))
ADD93_IN_GAA(s(T82), T83, s(T85)) → ADD93_IN_GAA(T82, T83, T85)
ADD93_IN_GAA(T92, s(T93), s(T95)) → U15_GAA(T92, T93, T95, add93_in_gaa(T92, T93, T95))
ADD93_IN_GAA(T92, s(T93), s(T95)) → ADD93_IN_GAA(T92, T93, T95)

The TRS R consists of the following rules:

fib1_in_ga(0, 0) → fib1_out_ga(0, 0)
fib1_in_ga(s(0), s(0)) → fib1_out_ga(s(0), s(0))
fib1_in_ga(s(s(0)), T7) → U16_ga(T7, fib20_in_a(X10))
fib20_in_a(0) → fib20_out_a(0)
U16_ga(T7, fib20_out_a(X10)) → fib1_out_ga(s(s(0)), T7)
fib1_in_ga(s(s(0)), T7) → U17_ga(T7, fib20_in_a(T9))
U17_ga(T7, fib20_out_a(T9)) → U18_ga(T7, add21_in_ga(T9, T7))
add21_in_ga(T20, s(T22)) → U2_ga(T20, T22, add33_in_ga(T20, T22))
add33_in_ga(0, 0) → add33_out_ga(0, 0)
add33_in_ga(s(T27), s(T29)) → U1_ga(T27, T29, add33_in_ga(T27, T29))
U1_ga(T27, T29, add33_out_ga(T27, T29)) → add33_out_ga(s(T27), s(T29))
U2_ga(T20, T22, add33_out_ga(T20, T22)) → add21_out_ga(T20, s(T22))
add21_in_ga(s(T34), s(T36)) → U3_ga(T34, T36, add21_in_ga(T34, T36))
U3_ga(T34, T36, add21_out_ga(T34, T36)) → add21_out_ga(s(T34), s(T36))
U18_ga(T7, add21_out_ga(T9, T7)) → fib1_out_ga(s(s(0)), T7)
fib1_in_ga(s(s(s(T41))), T7) → U19_ga(T41, T7, fib48_in_ga(T41, X80))
fib48_in_ga(0, s(0)) → fib48_out_ga(0, s(0))
fib48_in_ga(s(T45), X97) → U4_ga(T45, X97, p57_in_gaaa(T45, X95, X96, X97))
p57_in_gaaa(T45, X95, X96, X97) → U5_gaaa(T45, X95, X96, X97, fib48_in_ga(T45, X95))
U5_gaaa(T45, X95, X96, X97, fib48_out_ga(T45, X95)) → p57_out_gaaa(T45, X95, X96, X97)
p57_in_gaaa(T45, T46, X96, X97) → U6_gaaa(T45, T46, X96, X97, fib48_in_ga(T45, T46))
U6_gaaa(T45, T46, X96, X97, fib48_out_ga(T45, T46)) → U7_gaaa(T45, T46, X96, X97, fib61_in_ga(T45, X96))
fib61_in_ga(0, 0) → fib61_out_ga(0, 0)
fib61_in_ga(s(0), s(0)) → fib61_out_ga(s(0), s(0))
fib61_in_ga(s(s(T50)), X112) → U13_ga(T50, X112, p57_in_gaaa(T50, X110, X111, X112))
p57_in_gaaa(T45, T46, T47, X97) → U8_gaaa(T45, T46, T47, X97, fib48_in_ga(T45, T46))
U8_gaaa(T45, T46, T47, X97, fib48_out_ga(T45, T46)) → U9_gaaa(T45, T46, T47, X97, fib61_in_ga(T45, T47))
U9_gaaa(T45, T46, T47, X97, fib61_out_ga(T45, T47)) → U10_gaaa(T45, T46, T47, X97, add62_in_aaa(T46, T47, X97))
add62_in_aaa(0, 0, 0) → add62_out_aaa(0, 0, 0)
add62_in_aaa(s(T59), T60, s(X134)) → U11_aaa(T59, T60, X134, add62_in_aaa(T59, T60, X134))
add62_in_aaa(T65, s(T66), s(X149)) → U12_aaa(T65, T66, X149, add62_in_aaa(T65, T66, X149))
U12_aaa(T65, T66, X149, add62_out_aaa(T65, T66, X149)) → add62_out_aaa(T65, s(T66), s(X149))
U11_aaa(T59, T60, X134, add62_out_aaa(T59, T60, X134)) → add62_out_aaa(s(T59), T60, s(X134))
U10_gaaa(T45, T46, T47, X97, add62_out_aaa(T46, T47, X97)) → p57_out_gaaa(T45, T46, T47, X97)
U13_ga(T50, X112, p57_out_gaaa(T50, X110, X111, X112)) → fib61_out_ga(s(s(T50)), X112)
U7_gaaa(T45, T46, X96, X97, fib61_out_ga(T45, X96)) → p57_out_gaaa(T45, T46, X96, X97)
U4_ga(T45, X97, p57_out_gaaa(T45, X95, X96, X97)) → fib48_out_ga(s(T45), X97)
U19_ga(T41, T7, fib48_out_ga(T41, X80)) → fib1_out_ga(s(s(s(T41))), T7)
fib1_in_ga(s(s(s(T41))), T7) → U20_ga(T41, T7, fib48_in_ga(T41, T42))
U20_ga(T41, T7, fib48_out_ga(T41, T42)) → U21_ga(T41, T7, fib61_in_ga(T41, X81))
U21_ga(T41, T7, fib61_out_ga(T41, X81)) → fib1_out_ga(s(s(s(T41))), T7)
U20_ga(T41, T7, fib48_out_ga(T41, T42)) → U22_ga(T41, T7, T42, fib61_in_ga(T41, T67))
U22_ga(T41, T7, T42, fib61_out_ga(T41, T67)) → U23_ga(T41, T7, add62_in_aaa(T42, T67, X82))
U23_ga(T41, T7, add62_out_aaa(T42, T67, X82)) → fib1_out_ga(s(s(s(T41))), T7)
U22_ga(T41, T7, T42, fib61_out_ga(T41, T67)) → U24_ga(T41, T7, add62_in_aaa(T42, T67, T68))
U24_ga(T41, T7, add62_out_aaa(T42, T67, T68)) → U25_ga(T41, T7, fib48_in_ga(T41, X10))
U25_ga(T41, T7, fib48_out_ga(T41, X10)) → fib1_out_ga(s(s(s(T41))), T7)
U24_ga(T41, T7, add62_out_aaa(T42, T67, T68)) → U26_ga(T41, T7, T68, fib48_in_ga(T41, T69))
U26_ga(T41, T7, T68, fib48_out_ga(T41, T69)) → U27_ga(T41, T7, add93_in_gaa(T68, T69, T7))
add93_in_gaa(0, 0, 0) → add93_out_gaa(0, 0, 0)
add93_in_gaa(s(T82), T83, s(T85)) → U14_gaa(T82, T83, T85, add93_in_gaa(T82, T83, T85))
add93_in_gaa(T92, s(T93), s(T95)) → U15_gaa(T92, T93, T95, add93_in_gaa(T92, T93, T95))
U15_gaa(T92, T93, T95, add93_out_gaa(T92, T93, T95)) → add93_out_gaa(T92, s(T93), s(T95))
U14_gaa(T82, T83, T85, add93_out_gaa(T82, T83, T85)) → add93_out_gaa(s(T82), T83, s(T85))
U27_ga(T41, T7, add93_out_gaa(T68, T69, T7)) → fib1_out_ga(s(s(s(T41))), T7)

(50) DependencyGraphProof (EQUIVALENT transformation)

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

(51) Complex Obligation (AND)

(52) Obligation:

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

ADD93_IN_GAA(T92, s(T93), s(T95)) → ADD93_IN_GAA(T92, T93, T95)
ADD93_IN_GAA(s(T82), T83, s(T85)) → ADD93_IN_GAA(T82, T83, T85)

The TRS R consists of the following rules:

fib1_in_ga(0, 0) → fib1_out_ga(0, 0)
fib1_in_ga(s(0), s(0)) → fib1_out_ga(s(0), s(0))
fib1_in_ga(s(s(0)), T7) → U16_ga(T7, fib20_in_a(X10))
fib20_in_a(0) → fib20_out_a(0)
U16_ga(T7, fib20_out_a(X10)) → fib1_out_ga(s(s(0)), T7)
fib1_in_ga(s(s(0)), T7) → U17_ga(T7, fib20_in_a(T9))
U17_ga(T7, fib20_out_a(T9)) → U18_ga(T7, add21_in_ga(T9, T7))
add21_in_ga(T20, s(T22)) → U2_ga(T20, T22, add33_in_ga(T20, T22))
add33_in_ga(0, 0) → add33_out_ga(0, 0)
add33_in_ga(s(T27), s(T29)) → U1_ga(T27, T29, add33_in_ga(T27, T29))
U1_ga(T27, T29, add33_out_ga(T27, T29)) → add33_out_ga(s(T27), s(T29))
U2_ga(T20, T22, add33_out_ga(T20, T22)) → add21_out_ga(T20, s(T22))
add21_in_ga(s(T34), s(T36)) → U3_ga(T34, T36, add21_in_ga(T34, T36))
U3_ga(T34, T36, add21_out_ga(T34, T36)) → add21_out_ga(s(T34), s(T36))
U18_ga(T7, add21_out_ga(T9, T7)) → fib1_out_ga(s(s(0)), T7)
fib1_in_ga(s(s(s(T41))), T7) → U19_ga(T41, T7, fib48_in_ga(T41, X80))
fib48_in_ga(0, s(0)) → fib48_out_ga(0, s(0))
fib48_in_ga(s(T45), X97) → U4_ga(T45, X97, p57_in_gaaa(T45, X95, X96, X97))
p57_in_gaaa(T45, X95, X96, X97) → U5_gaaa(T45, X95, X96, X97, fib48_in_ga(T45, X95))
U5_gaaa(T45, X95, X96, X97, fib48_out_ga(T45, X95)) → p57_out_gaaa(T45, X95, X96, X97)
p57_in_gaaa(T45, T46, X96, X97) → U6_gaaa(T45, T46, X96, X97, fib48_in_ga(T45, T46))
U6_gaaa(T45, T46, X96, X97, fib48_out_ga(T45, T46)) → U7_gaaa(T45, T46, X96, X97, fib61_in_ga(T45, X96))
fib61_in_ga(0, 0) → fib61_out_ga(0, 0)
fib61_in_ga(s(0), s(0)) → fib61_out_ga(s(0), s(0))
fib61_in_ga(s(s(T50)), X112) → U13_ga(T50, X112, p57_in_gaaa(T50, X110, X111, X112))
p57_in_gaaa(T45, T46, T47, X97) → U8_gaaa(T45, T46, T47, X97, fib48_in_ga(T45, T46))
U8_gaaa(T45, T46, T47, X97, fib48_out_ga(T45, T46)) → U9_gaaa(T45, T46, T47, X97, fib61_in_ga(T45, T47))
U9_gaaa(T45, T46, T47, X97, fib61_out_ga(T45, T47)) → U10_gaaa(T45, T46, T47, X97, add62_in_aaa(T46, T47, X97))
add62_in_aaa(0, 0, 0) → add62_out_aaa(0, 0, 0)
add62_in_aaa(s(T59), T60, s(X134)) → U11_aaa(T59, T60, X134, add62_in_aaa(T59, T60, X134))
add62_in_aaa(T65, s(T66), s(X149)) → U12_aaa(T65, T66, X149, add62_in_aaa(T65, T66, X149))
U12_aaa(T65, T66, X149, add62_out_aaa(T65, T66, X149)) → add62_out_aaa(T65, s(T66), s(X149))
U11_aaa(T59, T60, X134, add62_out_aaa(T59, T60, X134)) → add62_out_aaa(s(T59), T60, s(X134))
U10_gaaa(T45, T46, T47, X97, add62_out_aaa(T46, T47, X97)) → p57_out_gaaa(T45, T46, T47, X97)
U13_ga(T50, X112, p57_out_gaaa(T50, X110, X111, X112)) → fib61_out_ga(s(s(T50)), X112)
U7_gaaa(T45, T46, X96, X97, fib61_out_ga(T45, X96)) → p57_out_gaaa(T45, T46, X96, X97)
U4_ga(T45, X97, p57_out_gaaa(T45, X95, X96, X97)) → fib48_out_ga(s(T45), X97)
U19_ga(T41, T7, fib48_out_ga(T41, X80)) → fib1_out_ga(s(s(s(T41))), T7)
fib1_in_ga(s(s(s(T41))), T7) → U20_ga(T41, T7, fib48_in_ga(T41, T42))
U20_ga(T41, T7, fib48_out_ga(T41, T42)) → U21_ga(T41, T7, fib61_in_ga(T41, X81))
U21_ga(T41, T7, fib61_out_ga(T41, X81)) → fib1_out_ga(s(s(s(T41))), T7)
U20_ga(T41, T7, fib48_out_ga(T41, T42)) → U22_ga(T41, T7, T42, fib61_in_ga(T41, T67))
U22_ga(T41, T7, T42, fib61_out_ga(T41, T67)) → U23_ga(T41, T7, add62_in_aaa(T42, T67, X82))
U23_ga(T41, T7, add62_out_aaa(T42, T67, X82)) → fib1_out_ga(s(s(s(T41))), T7)
U22_ga(T41, T7, T42, fib61_out_ga(T41, T67)) → U24_ga(T41, T7, add62_in_aaa(T42, T67, T68))
U24_ga(T41, T7, add62_out_aaa(T42, T67, T68)) → U25_ga(T41, T7, fib48_in_ga(T41, X10))
U25_ga(T41, T7, fib48_out_ga(T41, X10)) → fib1_out_ga(s(s(s(T41))), T7)
U24_ga(T41, T7, add62_out_aaa(T42, T67, T68)) → U26_ga(T41, T7, T68, fib48_in_ga(T41, T69))
U26_ga(T41, T7, T68, fib48_out_ga(T41, T69)) → U27_ga(T41, T7, add93_in_gaa(T68, T69, T7))
add93_in_gaa(0, 0, 0) → add93_out_gaa(0, 0, 0)
add93_in_gaa(s(T82), T83, s(T85)) → U14_gaa(T82, T83, T85, add93_in_gaa(T82, T83, T85))
add93_in_gaa(T92, s(T93), s(T95)) → U15_gaa(T92, T93, T95, add93_in_gaa(T92, T93, T95))
U15_gaa(T92, T93, T95, add93_out_gaa(T92, T93, T95)) → add93_out_gaa(T92, s(T93), s(T95))
U14_gaa(T82, T83, T85, add93_out_gaa(T82, T83, T85)) → add93_out_gaa(s(T82), T83, s(T85))
U27_ga(T41, T7, add93_out_gaa(T68, T69, T7)) → fib1_out_ga(s(s(s(T41))), T7)

(53) UsableRulesProof (EQUIVALENT transformation)

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

(54) Obligation:

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

ADD93_IN_GAA(T92, s(T93), s(T95)) → ADD93_IN_GAA(T92, T93, T95)
ADD93_IN_GAA(s(T82), T83, s(T85)) → ADD93_IN_GAA(T82, T83, T85)

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

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

(55) PiDPToQDPProof (SOUND transformation)

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

(56) Obligation:

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

ADD93_IN_GAA(T92) → ADD93_IN_GAA(T92)
ADD93_IN_GAA(s(T82)) → ADD93_IN_GAA(T82)

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

(57) UsableRulesReductionPairsProof (EQUIVALENT transformation)

ADD93_IN_GAA(s(T82)) → ADD93_IN_GAA(T82)

No rules are removed from R.

Used ordering: POLO with Polynomial interpretation [POLO]:

POL(ADD93_IN_GAA(x₁)) = 2·x₁
POL(s(x₁)) = 2·x₁

(58) Obligation:

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

ADD93_IN_GAA(T92) → ADD93_IN_GAA(T92)

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

(59) NonTerminationProof (EQUIVALENT transformation)

Matcher: [ ]
Semiunifier: [ ]

Rewriting sequence

The DP semiunifies directly so there is only one rewrite step from ADD93_IN_GAA(T92) to ADD93_IN_GAA(T92).

(60) NO

(61) Obligation:

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

ADD62_IN_AAA(T65, s(T66), s(X149)) → ADD62_IN_AAA(T65, T66, X149)
ADD62_IN_AAA(s(T59), T60, s(X134)) → ADD62_IN_AAA(T59, T60, X134)

The TRS R consists of the following rules:

fib1_in_ga(0, 0) → fib1_out_ga(0, 0)
fib1_in_ga(s(0), s(0)) → fib1_out_ga(s(0), s(0))
fib1_in_ga(s(s(0)), T7) → U16_ga(T7, fib20_in_a(X10))
fib20_in_a(0) → fib20_out_a(0)
U16_ga(T7, fib20_out_a(X10)) → fib1_out_ga(s(s(0)), T7)
fib1_in_ga(s(s(0)), T7) → U17_ga(T7, fib20_in_a(T9))
U17_ga(T7, fib20_out_a(T9)) → U18_ga(T7, add21_in_ga(T9, T7))
add21_in_ga(T20, s(T22)) → U2_ga(T20, T22, add33_in_ga(T20, T22))
add33_in_ga(0, 0) → add33_out_ga(0, 0)
add33_in_ga(s(T27), s(T29)) → U1_ga(T27, T29, add33_in_ga(T27, T29))
U1_ga(T27, T29, add33_out_ga(T27, T29)) → add33_out_ga(s(T27), s(T29))
U2_ga(T20, T22, add33_out_ga(T20, T22)) → add21_out_ga(T20, s(T22))
add21_in_ga(s(T34), s(T36)) → U3_ga(T34, T36, add21_in_ga(T34, T36))
U3_ga(T34, T36, add21_out_ga(T34, T36)) → add21_out_ga(s(T34), s(T36))
U18_ga(T7, add21_out_ga(T9, T7)) → fib1_out_ga(s(s(0)), T7)
fib1_in_ga(s(s(s(T41))), T7) → U19_ga(T41, T7, fib48_in_ga(T41, X80))
fib48_in_ga(0, s(0)) → fib48_out_ga(0, s(0))
fib48_in_ga(s(T45), X97) → U4_ga(T45, X97, p57_in_gaaa(T45, X95, X96, X97))
p57_in_gaaa(T45, X95, X96, X97) → U5_gaaa(T45, X95, X96, X97, fib48_in_ga(T45, X95))
U5_gaaa(T45, X95, X96, X97, fib48_out_ga(T45, X95)) → p57_out_gaaa(T45, X95, X96, X97)
p57_in_gaaa(T45, T46, X96, X97) → U6_gaaa(T45, T46, X96, X97, fib48_in_ga(T45, T46))
U6_gaaa(T45, T46, X96, X97, fib48_out_ga(T45, T46)) → U7_gaaa(T45, T46, X96, X97, fib61_in_ga(T45, X96))
fib61_in_ga(0, 0) → fib61_out_ga(0, 0)
fib61_in_ga(s(0), s(0)) → fib61_out_ga(s(0), s(0))
fib61_in_ga(s(s(T50)), X112) → U13_ga(T50, X112, p57_in_gaaa(T50, X110, X111, X112))
p57_in_gaaa(T45, T46, T47, X97) → U8_gaaa(T45, T46, T47, X97, fib48_in_ga(T45, T46))
U8_gaaa(T45, T46, T47, X97, fib48_out_ga(T45, T46)) → U9_gaaa(T45, T46, T47, X97, fib61_in_ga(T45, T47))
U9_gaaa(T45, T46, T47, X97, fib61_out_ga(T45, T47)) → U10_gaaa(T45, T46, T47, X97, add62_in_aaa(T46, T47, X97))
add62_in_aaa(0, 0, 0) → add62_out_aaa(0, 0, 0)
add62_in_aaa(s(T59), T60, s(X134)) → U11_aaa(T59, T60, X134, add62_in_aaa(T59, T60, X134))
add62_in_aaa(T65, s(T66), s(X149)) → U12_aaa(T65, T66, X149, add62_in_aaa(T65, T66, X149))
U12_aaa(T65, T66, X149, add62_out_aaa(T65, T66, X149)) → add62_out_aaa(T65, s(T66), s(X149))
U11_aaa(T59, T60, X134, add62_out_aaa(T59, T60, X134)) → add62_out_aaa(s(T59), T60, s(X134))
U10_gaaa(T45, T46, T47, X97, add62_out_aaa(T46, T47, X97)) → p57_out_gaaa(T45, T46, T47, X97)
U13_ga(T50, X112, p57_out_gaaa(T50, X110, X111, X112)) → fib61_out_ga(s(s(T50)), X112)
U7_gaaa(T45, T46, X96, X97, fib61_out_ga(T45, X96)) → p57_out_gaaa(T45, T46, X96, X97)
U4_ga(T45, X97, p57_out_gaaa(T45, X95, X96, X97)) → fib48_out_ga(s(T45), X97)
U19_ga(T41, T7, fib48_out_ga(T41, X80)) → fib1_out_ga(s(s(s(T41))), T7)
fib1_in_ga(s(s(s(T41))), T7) → U20_ga(T41, T7, fib48_in_ga(T41, T42))
U20_ga(T41, T7, fib48_out_ga(T41, T42)) → U21_ga(T41, T7, fib61_in_ga(T41, X81))
U21_ga(T41, T7, fib61_out_ga(T41, X81)) → fib1_out_ga(s(s(s(T41))), T7)
U20_ga(T41, T7, fib48_out_ga(T41, T42)) → U22_ga(T41, T7, T42, fib61_in_ga(T41, T67))
U22_ga(T41, T7, T42, fib61_out_ga(T41, T67)) → U23_ga(T41, T7, add62_in_aaa(T42, T67, X82))
U23_ga(T41, T7, add62_out_aaa(T42, T67, X82)) → fib1_out_ga(s(s(s(T41))), T7)
U22_ga(T41, T7, T42, fib61_out_ga(T41, T67)) → U24_ga(T41, T7, add62_in_aaa(T42, T67, T68))
U24_ga(T41, T7, add62_out_aaa(T42, T67, T68)) → U25_ga(T41, T7, fib48_in_ga(T41, X10))
U25_ga(T41, T7, fib48_out_ga(T41, X10)) → fib1_out_ga(s(s(s(T41))), T7)
U24_ga(T41, T7, add62_out_aaa(T42, T67, T68)) → U26_ga(T41, T7, T68, fib48_in_ga(T41, T69))
U26_ga(T41, T7, T68, fib48_out_ga(T41, T69)) → U27_ga(T41, T7, add93_in_gaa(T68, T69, T7))
add93_in_gaa(0, 0, 0) → add93_out_gaa(0, 0, 0)
add93_in_gaa(s(T82), T83, s(T85)) → U14_gaa(T82, T83, T85, add93_in_gaa(T82, T83, T85))
add93_in_gaa(T92, s(T93), s(T95)) → U15_gaa(T92, T93, T95, add93_in_gaa(T92, T93, T95))
U15_gaa(T92, T93, T95, add93_out_gaa(T92, T93, T95)) → add93_out_gaa(T92, s(T93), s(T95))
U14_gaa(T82, T83, T85, add93_out_gaa(T82, T83, T85)) → add93_out_gaa(s(T82), T83, s(T85))
U27_ga(T41, T7, add93_out_gaa(T68, T69, T7)) → fib1_out_ga(s(s(s(T41))), T7)

(62) UsableRulesProof (EQUIVALENT transformation)

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

(63) Obligation:

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

ADD62_IN_AAA(T65, s(T66), s(X149)) → ADD62_IN_AAA(T65, T66, X149)
ADD62_IN_AAA(s(T59), T60, s(X134)) → ADD62_IN_AAA(T59, T60, X134)

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

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

(64) PiDPToQDPProof (SOUND transformation)

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

(65) Obligation:

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

ADD62_IN_AAA → ADD62_IN_AAA

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

(66) NonTerminationProof (EQUIVALENT transformation)

Semiunifier: [ ]
Matcher: [ ]

Rewriting sequence

The DP semiunifies directly so there is only one rewrite step from ADD62_IN_AAA to ADD62_IN_AAA.

(67) NO

(68) Obligation:

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

FIB48_IN_GA(s(T45), X97) → P57_IN_GAAA(T45, X95, X96, X97)
P57_IN_GAAA(T45, X95, X96, X97) → FIB48_IN_GA(T45, X95)
P57_IN_GAAA(T45, T46, X96, X97) → U6_GAAA(T45, T46, X96, X97, fib48_in_ga(T45, T46))
U6_GAAA(T45, T46, X96, X97, fib48_out_ga(T45, T46)) → FIB61_IN_GA(T45, X96)
FIB61_IN_GA(s(s(T50)), X112) → P57_IN_GAAA(T50, X110, X111, X112)
P57_IN_GAAA(T45, T46, T47, X97) → U8_GAAA(T45, T46, T47, X97, fib48_in_ga(T45, T46))
U8_GAAA(T45, T46, T47, X97, fib48_out_ga(T45, T46)) → FIB61_IN_GA(T45, T47)

The TRS R consists of the following rules:

fib1_in_ga(0, 0) → fib1_out_ga(0, 0)
fib1_in_ga(s(0), s(0)) → fib1_out_ga(s(0), s(0))
fib1_in_ga(s(s(0)), T7) → U16_ga(T7, fib20_in_a(X10))
fib20_in_a(0) → fib20_out_a(0)
U16_ga(T7, fib20_out_a(X10)) → fib1_out_ga(s(s(0)), T7)
fib1_in_ga(s(s(0)), T7) → U17_ga(T7, fib20_in_a(T9))
U17_ga(T7, fib20_out_a(T9)) → U18_ga(T7, add21_in_ga(T9, T7))
add21_in_ga(T20, s(T22)) → U2_ga(T20, T22, add33_in_ga(T20, T22))
add33_in_ga(0, 0) → add33_out_ga(0, 0)
add33_in_ga(s(T27), s(T29)) → U1_ga(T27, T29, add33_in_ga(T27, T29))
U1_ga(T27, T29, add33_out_ga(T27, T29)) → add33_out_ga(s(T27), s(T29))
U2_ga(T20, T22, add33_out_ga(T20, T22)) → add21_out_ga(T20, s(T22))
add21_in_ga(s(T34), s(T36)) → U3_ga(T34, T36, add21_in_ga(T34, T36))
U3_ga(T34, T36, add21_out_ga(T34, T36)) → add21_out_ga(s(T34), s(T36))
U18_ga(T7, add21_out_ga(T9, T7)) → fib1_out_ga(s(s(0)), T7)
fib1_in_ga(s(s(s(T41))), T7) → U19_ga(T41, T7, fib48_in_ga(T41, X80))
fib48_in_ga(0, s(0)) → fib48_out_ga(0, s(0))
fib48_in_ga(s(T45), X97) → U4_ga(T45, X97, p57_in_gaaa(T45, X95, X96, X97))
p57_in_gaaa(T45, X95, X96, X97) → U5_gaaa(T45, X95, X96, X97, fib48_in_ga(T45, X95))
U5_gaaa(T45, X95, X96, X97, fib48_out_ga(T45, X95)) → p57_out_gaaa(T45, X95, X96, X97)
p57_in_gaaa(T45, T46, X96, X97) → U6_gaaa(T45, T46, X96, X97, fib48_in_ga(T45, T46))
U6_gaaa(T45, T46, X96, X97, fib48_out_ga(T45, T46)) → U7_gaaa(T45, T46, X96, X97, fib61_in_ga(T45, X96))
fib61_in_ga(0, 0) → fib61_out_ga(0, 0)
fib61_in_ga(s(0), s(0)) → fib61_out_ga(s(0), s(0))
fib61_in_ga(s(s(T50)), X112) → U13_ga(T50, X112, p57_in_gaaa(T50, X110, X111, X112))
p57_in_gaaa(T45, T46, T47, X97) → U8_gaaa(T45, T46, T47, X97, fib48_in_ga(T45, T46))
U8_gaaa(T45, T46, T47, X97, fib48_out_ga(T45, T46)) → U9_gaaa(T45, T46, T47, X97, fib61_in_ga(T45, T47))
U9_gaaa(T45, T46, T47, X97, fib61_out_ga(T45, T47)) → U10_gaaa(T45, T46, T47, X97, add62_in_aaa(T46, T47, X97))
add62_in_aaa(0, 0, 0) → add62_out_aaa(0, 0, 0)
add62_in_aaa(s(T59), T60, s(X134)) → U11_aaa(T59, T60, X134, add62_in_aaa(T59, T60, X134))
add62_in_aaa(T65, s(T66), s(X149)) → U12_aaa(T65, T66, X149, add62_in_aaa(T65, T66, X149))
U12_aaa(T65, T66, X149, add62_out_aaa(T65, T66, X149)) → add62_out_aaa(T65, s(T66), s(X149))
U11_aaa(T59, T60, X134, add62_out_aaa(T59, T60, X134)) → add62_out_aaa(s(T59), T60, s(X134))
U10_gaaa(T45, T46, T47, X97, add62_out_aaa(T46, T47, X97)) → p57_out_gaaa(T45, T46, T47, X97)
U13_ga(T50, X112, p57_out_gaaa(T50, X110, X111, X112)) → fib61_out_ga(s(s(T50)), X112)
U7_gaaa(T45, T46, X96, X97, fib61_out_ga(T45, X96)) → p57_out_gaaa(T45, T46, X96, X97)
U4_ga(T45, X97, p57_out_gaaa(T45, X95, X96, X97)) → fib48_out_ga(s(T45), X97)
U19_ga(T41, T7, fib48_out_ga(T41, X80)) → fib1_out_ga(s(s(s(T41))), T7)
fib1_in_ga(s(s(s(T41))), T7) → U20_ga(T41, T7, fib48_in_ga(T41, T42))
U20_ga(T41, T7, fib48_out_ga(T41, T42)) → U21_ga(T41, T7, fib61_in_ga(T41, X81))
U21_ga(T41, T7, fib61_out_ga(T41, X81)) → fib1_out_ga(s(s(s(T41))), T7)
U20_ga(T41, T7, fib48_out_ga(T41, T42)) → U22_ga(T41, T7, T42, fib61_in_ga(T41, T67))
U22_ga(T41, T7, T42, fib61_out_ga(T41, T67)) → U23_ga(T41, T7, add62_in_aaa(T42, T67, X82))
U23_ga(T41, T7, add62_out_aaa(T42, T67, X82)) → fib1_out_ga(s(s(s(T41))), T7)
U22_ga(T41, T7, T42, fib61_out_ga(T41, T67)) → U24_ga(T41, T7, add62_in_aaa(T42, T67, T68))
U24_ga(T41, T7, add62_out_aaa(T42, T67, T68)) → U25_ga(T41, T7, fib48_in_ga(T41, X10))
U25_ga(T41, T7, fib48_out_ga(T41, X10)) → fib1_out_ga(s(s(s(T41))), T7)
U24_ga(T41, T7, add62_out_aaa(T42, T67, T68)) → U26_ga(T41, T7, T68, fib48_in_ga(T41, T69))
U26_ga(T41, T7, T68, fib48_out_ga(T41, T69)) → U27_ga(T41, T7, add93_in_gaa(T68, T69, T7))
add93_in_gaa(0, 0, 0) → add93_out_gaa(0, 0, 0)
add93_in_gaa(s(T82), T83, s(T85)) → U14_gaa(T82, T83, T85, add93_in_gaa(T82, T83, T85))
add93_in_gaa(T92, s(T93), s(T95)) → U15_gaa(T92, T93, T95, add93_in_gaa(T92, T93, T95))
U15_gaa(T92, T93, T95, add93_out_gaa(T92, T93, T95)) → add93_out_gaa(T92, s(T93), s(T95))
U14_gaa(T82, T83, T85, add93_out_gaa(T82, T83, T85)) → add93_out_gaa(s(T82), T83, s(T85))
U27_ga(T41, T7, add93_out_gaa(T68, T69, T7)) → fib1_out_ga(s(s(s(T41))), T7)

(69) UsableRulesProof (EQUIVALENT transformation)

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

(70) Obligation:

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

FIB48_IN_GA(s(T45), X97) → P57_IN_GAAA(T45, X95, X96, X97)
P57_IN_GAAA(T45, X95, X96, X97) → FIB48_IN_GA(T45, X95)
P57_IN_GAAA(T45, T46, X96, X97) → U6_GAAA(T45, T46, X96, X97, fib48_in_ga(T45, T46))
U6_GAAA(T45, T46, X96, X97, fib48_out_ga(T45, T46)) → FIB61_IN_GA(T45, X96)
FIB61_IN_GA(s(s(T50)), X112) → P57_IN_GAAA(T50, X110, X111, X112)
P57_IN_GAAA(T45, T46, T47, X97) → U8_GAAA(T45, T46, T47, X97, fib48_in_ga(T45, T46))
U8_GAAA(T45, T46, T47, X97, fib48_out_ga(T45, T46)) → FIB61_IN_GA(T45, T47)

The TRS R consists of the following rules:

fib48_in_ga(0, s(0)) → fib48_out_ga(0, s(0))
fib48_in_ga(s(T45), X97) → U4_ga(T45, X97, p57_in_gaaa(T45, X95, X96, X97))
U4_ga(T45, X97, p57_out_gaaa(T45, X95, X96, X97)) → fib48_out_ga(s(T45), X97)
p57_in_gaaa(T45, X95, X96, X97) → U5_gaaa(T45, X95, X96, X97, fib48_in_ga(T45, X95))
p57_in_gaaa(T45, T46, X96, X97) → U6_gaaa(T45, T46, X96, X97, fib48_in_ga(T45, T46))
p57_in_gaaa(T45, T46, T47, X97) → U8_gaaa(T45, T46, T47, X97, fib48_in_ga(T45, T46))
U5_gaaa(T45, X95, X96, X97, fib48_out_ga(T45, X95)) → p57_out_gaaa(T45, X95, X96, X97)
U6_gaaa(T45, T46, X96, X97, fib48_out_ga(T45, T46)) → U7_gaaa(T45, T46, X96, X97, fib61_in_ga(T45, X96))
U8_gaaa(T45, T46, T47, X97, fib48_out_ga(T45, T46)) → U9_gaaa(T45, T46, T47, X97, fib61_in_ga(T45, T47))
U7_gaaa(T45, T46, X96, X97, fib61_out_ga(T45, X96)) → p57_out_gaaa(T45, T46, X96, X97)
U9_gaaa(T45, T46, T47, X97, fib61_out_ga(T45, T47)) → U10_gaaa(T45, T46, T47, X97, add62_in_aaa(T46, T47, X97))
fib61_in_ga(0, 0) → fib61_out_ga(0, 0)
fib61_in_ga(s(0), s(0)) → fib61_out_ga(s(0), s(0))
fib61_in_ga(s(s(T50)), X112) → U13_ga(T50, X112, p57_in_gaaa(T50, X110, X111, X112))
U10_gaaa(T45, T46, T47, X97, add62_out_aaa(T46, T47, X97)) → p57_out_gaaa(T45, T46, T47, X97)
U13_ga(T50, X112, p57_out_gaaa(T50, X110, X111, X112)) → fib61_out_ga(s(s(T50)), X112)
add62_in_aaa(0, 0, 0) → add62_out_aaa(0, 0, 0)
add62_in_aaa(s(T59), T60, s(X134)) → U11_aaa(T59, T60, X134, add62_in_aaa(T59, T60, X134))
add62_in_aaa(T65, s(T66), s(X149)) → U12_aaa(T65, T66, X149, add62_in_aaa(T65, T66, X149))
U11_aaa(T59, T60, X134, add62_out_aaa(T59, T60, X134)) → add62_out_aaa(s(T59), T60, s(X134))
U12_aaa(T65, T66, X149, add62_out_aaa(T65, T66, X149)) → add62_out_aaa(T65, s(T66), s(X149))

The argument filtering Pi contains the following mapping:
0 = 0
s(x1) = s(x1)
fib48_in_ga(x1, x2) = fib48_in_ga(x1)
fib48_out_ga(x1, x2) = fib48_out_ga
U4_ga(x1, x2, x3) = U4_ga(x3)
p57_in_gaaa(x1, x2, x3, x4) = p57_in_gaaa(x1)
U5_gaaa(x1, x2, x3, x4, x5) = U5_gaaa(x5)
p57_out_gaaa(x1, x2, x3, x4) = p57_out_gaaa
U6_gaaa(x1, x2, x3, x4, x5) = U6_gaaa(x1, x5)
U7_gaaa(x1, x2, x3, x4, x5) = U7_gaaa(x5)
fib61_in_ga(x1, x2) = fib61_in_ga(x1)
fib61_out_ga(x1, x2) = fib61_out_ga
U13_ga(x1, x2, x3) = U13_ga(x3)
U8_gaaa(x1, x2, x3, x4, x5) = U8_gaaa(x1, x5)
U9_gaaa(x1, x2, x3, x4, x5) = U9_gaaa(x5)
U10_gaaa(x1, x2, x3, x4, x5) = U10_gaaa(x5)
add62_in_aaa(x1, x2, x3) = add62_in_aaa
add62_out_aaa(x1, x2, x3) = add62_out_aaa(x1, x2, x3)
U11_aaa(x1, x2, x3, x4) = U11_aaa(x4)
U12_aaa(x1, x2, x3, x4) = U12_aaa(x4)
FIB48_IN_GA(x1, x2) = FIB48_IN_GA(x1)
P57_IN_GAAA(x1, x2, x3, x4) = P57_IN_GAAA(x1)
U6_GAAA(x1, x2, x3, x4, x5) = U6_GAAA(x1, x5)
FIB61_IN_GA(x1, x2) = FIB61_IN_GA(x1)
U8_GAAA(x1, x2, x3, x4, x5) = U8_GAAA(x1, x5)

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

(71) PiDPToQDPProof (SOUND transformation)

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

(72) Obligation:

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

FIB48_IN_GA(s(T45)) → P57_IN_GAAA(T45)
P57_IN_GAAA(T45) → FIB48_IN_GA(T45)
P57_IN_GAAA(T45) → U6_GAAA(T45, fib48_in_ga(T45))
U6_GAAA(T45, fib48_out_ga) → FIB61_IN_GA(T45)
FIB61_IN_GA(s(s(T50))) → P57_IN_GAAA(T50)
P57_IN_GAAA(T45) → U8_GAAA(T45, fib48_in_ga(T45))
U8_GAAA(T45, fib48_out_ga) → FIB61_IN_GA(T45)

The TRS R consists of the following rules:

fib48_in_ga(0) → fib48_out_ga
fib48_in_ga(s(T45)) → U4_ga(p57_in_gaaa(T45))
U4_ga(p57_out_gaaa) → fib48_out_ga
p57_in_gaaa(T45) → U5_gaaa(fib48_in_ga(T45))
p57_in_gaaa(T45) → U6_gaaa(T45, fib48_in_ga(T45))
p57_in_gaaa(T45) → U8_gaaa(T45, fib48_in_ga(T45))
U5_gaaa(fib48_out_ga) → p57_out_gaaa
U6_gaaa(T45, fib48_out_ga) → U7_gaaa(fib61_in_ga(T45))
U8_gaaa(T45, fib48_out_ga) → U9_gaaa(fib61_in_ga(T45))
U7_gaaa(fib61_out_ga) → p57_out_gaaa
U9_gaaa(fib61_out_ga) → U10_gaaa(add62_in_aaa)
fib61_in_ga(0) → fib61_out_ga
fib61_in_ga(s(0)) → fib61_out_ga
fib61_in_ga(s(s(T50))) → U13_ga(p57_in_gaaa(T50))
U10_gaaa(add62_out_aaa(T46, T47, X97)) → p57_out_gaaa
U13_ga(p57_out_gaaa) → fib61_out_ga
add62_in_aaa → add62_out_aaa(0, 0, 0)
add62_in_aaa → U11_aaa(add62_in_aaa)
add62_in_aaa → U12_aaa(add62_in_aaa)
U11_aaa(add62_out_aaa(T59, T60, X134)) → add62_out_aaa(s(T59), T60, s(X134))
U12_aaa(add62_out_aaa(T65, T66, X149)) → add62_out_aaa(T65, s(T66), s(X149))

The set Q consists of the following terms:

fib48_in_ga(x0)
U4_ga(x0)
p57_in_gaaa(x0)
U5_gaaa(x0)
U6_gaaa(x0, x1)
U8_gaaa(x0, x1)
U7_gaaa(x0)
U9_gaaa(x0)
fib61_in_ga(x0)
U10_gaaa(x0)
U13_ga(x0)
add62_in_aaa
U11_aaa(x0)
U12_aaa(x0)

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

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

P57_IN_GAAA(T45) → FIB48_IN_GA(T45)
The graph contains the following edges 1 >= 1
FIB48_IN_GA(s(T45)) → P57_IN_GAAA(T45)
The graph contains the following edges 1 > 1
FIB61_IN_GA(s(s(T50))) → P57_IN_GAAA(T50)
The graph contains the following edges 1 > 1
U6_GAAA(T45, fib48_out_ga) → FIB61_IN_GA(T45)
The graph contains the following edges 1 >= 1
U8_GAAA(T45, fib48_out_ga) → FIB61_IN_GA(T45)
The graph contains the following edges 1 >= 1
P57_IN_GAAA(T45) → U6_GAAA(T45, fib48_in_ga(T45))
The graph contains the following edges 1 >= 1
P57_IN_GAAA(T45) → U8_GAAA(T45, fib48_in_ga(T45))
The graph contains the following edges 1 >= 1

(74) YES

(75) Obligation:

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

ADD33_IN_GA(s(T27), s(T29)) → ADD33_IN_GA(T27, T29)

The TRS R consists of the following rules:

fib1_in_ga(0, 0) → fib1_out_ga(0, 0)
fib1_in_ga(s(0), s(0)) → fib1_out_ga(s(0), s(0))
fib1_in_ga(s(s(0)), T7) → U16_ga(T7, fib20_in_a(X10))
fib20_in_a(0) → fib20_out_a(0)
U16_ga(T7, fib20_out_a(X10)) → fib1_out_ga(s(s(0)), T7)
fib1_in_ga(s(s(0)), T7) → U17_ga(T7, fib20_in_a(T9))
U17_ga(T7, fib20_out_a(T9)) → U18_ga(T7, add21_in_ga(T9, T7))
add21_in_ga(T20, s(T22)) → U2_ga(T20, T22, add33_in_ga(T20, T22))
add33_in_ga(0, 0) → add33_out_ga(0, 0)
add33_in_ga(s(T27), s(T29)) → U1_ga(T27, T29, add33_in_ga(T27, T29))
U1_ga(T27, T29, add33_out_ga(T27, T29)) → add33_out_ga(s(T27), s(T29))
U2_ga(T20, T22, add33_out_ga(T20, T22)) → add21_out_ga(T20, s(T22))
add21_in_ga(s(T34), s(T36)) → U3_ga(T34, T36, add21_in_ga(T34, T36))
U3_ga(T34, T36, add21_out_ga(T34, T36)) → add21_out_ga(s(T34), s(T36))
U18_ga(T7, add21_out_ga(T9, T7)) → fib1_out_ga(s(s(0)), T7)
fib1_in_ga(s(s(s(T41))), T7) → U19_ga(T41, T7, fib48_in_ga(T41, X80))
fib48_in_ga(0, s(0)) → fib48_out_ga(0, s(0))
fib48_in_ga(s(T45), X97) → U4_ga(T45, X97, p57_in_gaaa(T45, X95, X96, X97))
p57_in_gaaa(T45, X95, X96, X97) → U5_gaaa(T45, X95, X96, X97, fib48_in_ga(T45, X95))
U5_gaaa(T45, X95, X96, X97, fib48_out_ga(T45, X95)) → p57_out_gaaa(T45, X95, X96, X97)
p57_in_gaaa(T45, T46, X96, X97) → U6_gaaa(T45, T46, X96, X97, fib48_in_ga(T45, T46))
U6_gaaa(T45, T46, X96, X97, fib48_out_ga(T45, T46)) → U7_gaaa(T45, T46, X96, X97, fib61_in_ga(T45, X96))
fib61_in_ga(0, 0) → fib61_out_ga(0, 0)
fib61_in_ga(s(0), s(0)) → fib61_out_ga(s(0), s(0))
fib61_in_ga(s(s(T50)), X112) → U13_ga(T50, X112, p57_in_gaaa(T50, X110, X111, X112))
p57_in_gaaa(T45, T46, T47, X97) → U8_gaaa(T45, T46, T47, X97, fib48_in_ga(T45, T46))
U8_gaaa(T45, T46, T47, X97, fib48_out_ga(T45, T46)) → U9_gaaa(T45, T46, T47, X97, fib61_in_ga(T45, T47))
U9_gaaa(T45, T46, T47, X97, fib61_out_ga(T45, T47)) → U10_gaaa(T45, T46, T47, X97, add62_in_aaa(T46, T47, X97))
add62_in_aaa(0, 0, 0) → add62_out_aaa(0, 0, 0)
add62_in_aaa(s(T59), T60, s(X134)) → U11_aaa(T59, T60, X134, add62_in_aaa(T59, T60, X134))
add62_in_aaa(T65, s(T66), s(X149)) → U12_aaa(T65, T66, X149, add62_in_aaa(T65, T66, X149))
U12_aaa(T65, T66, X149, add62_out_aaa(T65, T66, X149)) → add62_out_aaa(T65, s(T66), s(X149))
U11_aaa(T59, T60, X134, add62_out_aaa(T59, T60, X134)) → add62_out_aaa(s(T59), T60, s(X134))
U10_gaaa(T45, T46, T47, X97, add62_out_aaa(T46, T47, X97)) → p57_out_gaaa(T45, T46, T47, X97)
U13_ga(T50, X112, p57_out_gaaa(T50, X110, X111, X112)) → fib61_out_ga(s(s(T50)), X112)
U7_gaaa(T45, T46, X96, X97, fib61_out_ga(T45, X96)) → p57_out_gaaa(T45, T46, X96, X97)
U4_ga(T45, X97, p57_out_gaaa(T45, X95, X96, X97)) → fib48_out_ga(s(T45), X97)
U19_ga(T41, T7, fib48_out_ga(T41, X80)) → fib1_out_ga(s(s(s(T41))), T7)
fib1_in_ga(s(s(s(T41))), T7) → U20_ga(T41, T7, fib48_in_ga(T41, T42))
U20_ga(T41, T7, fib48_out_ga(T41, T42)) → U21_ga(T41, T7, fib61_in_ga(T41, X81))
U21_ga(T41, T7, fib61_out_ga(T41, X81)) → fib1_out_ga(s(s(s(T41))), T7)
U20_ga(T41, T7, fib48_out_ga(T41, T42)) → U22_ga(T41, T7, T42, fib61_in_ga(T41, T67))
U22_ga(T41, T7, T42, fib61_out_ga(T41, T67)) → U23_ga(T41, T7, add62_in_aaa(T42, T67, X82))
U23_ga(T41, T7, add62_out_aaa(T42, T67, X82)) → fib1_out_ga(s(s(s(T41))), T7)
U22_ga(T41, T7, T42, fib61_out_ga(T41, T67)) → U24_ga(T41, T7, add62_in_aaa(T42, T67, T68))
U24_ga(T41, T7, add62_out_aaa(T42, T67, T68)) → U25_ga(T41, T7, fib48_in_ga(T41, X10))
U25_ga(T41, T7, fib48_out_ga(T41, X10)) → fib1_out_ga(s(s(s(T41))), T7)
U24_ga(T41, T7, add62_out_aaa(T42, T67, T68)) → U26_ga(T41, T7, T68, fib48_in_ga(T41, T69))
U26_ga(T41, T7, T68, fib48_out_ga(T41, T69)) → U27_ga(T41, T7, add93_in_gaa(T68, T69, T7))
add93_in_gaa(0, 0, 0) → add93_out_gaa(0, 0, 0)
add93_in_gaa(s(T82), T83, s(T85)) → U14_gaa(T82, T83, T85, add93_in_gaa(T82, T83, T85))
add93_in_gaa(T92, s(T93), s(T95)) → U15_gaa(T92, T93, T95, add93_in_gaa(T92, T93, T95))
U15_gaa(T92, T93, T95, add93_out_gaa(T92, T93, T95)) → add93_out_gaa(T92, s(T93), s(T95))
U14_gaa(T82, T83, T85, add93_out_gaa(T82, T83, T85)) → add93_out_gaa(s(T82), T83, s(T85))
U27_ga(T41, T7, add93_out_gaa(T68, T69, T7)) → fib1_out_ga(s(s(s(T41))), T7)

(76) UsableRulesProof (EQUIVALENT transformation)

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

(77) Obligation:

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

ADD33_IN_GA(s(T27), s(T29)) → ADD33_IN_GA(T27, T29)

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

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

(78) PiDPToQDPProof (SOUND transformation)

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

(79) Obligation:

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

ADD33_IN_GA(s(T27)) → ADD33_IN_GA(T27)

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

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

ADD33_IN_GA(s(T27)) → ADD33_IN_GA(T27)
The graph contains the following edges 1 > 1

(81) YES

(82) Obligation:

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

ADD21_IN_GA(s(T34), s(T36)) → ADD21_IN_GA(T34, T36)

The TRS R consists of the following rules:

fib1_in_ga(0, 0) → fib1_out_ga(0, 0)
fib1_in_ga(s(0), s(0)) → fib1_out_ga(s(0), s(0))
fib1_in_ga(s(s(0)), T7) → U16_ga(T7, fib20_in_a(X10))
fib20_in_a(0) → fib20_out_a(0)
U16_ga(T7, fib20_out_a(X10)) → fib1_out_ga(s(s(0)), T7)
fib1_in_ga(s(s(0)), T7) → U17_ga(T7, fib20_in_a(T9))
U17_ga(T7, fib20_out_a(T9)) → U18_ga(T7, add21_in_ga(T9, T7))
add21_in_ga(T20, s(T22)) → U2_ga(T20, T22, add33_in_ga(T20, T22))
add33_in_ga(0, 0) → add33_out_ga(0, 0)
add33_in_ga(s(T27), s(T29)) → U1_ga(T27, T29, add33_in_ga(T27, T29))
U1_ga(T27, T29, add33_out_ga(T27, T29)) → add33_out_ga(s(T27), s(T29))
U2_ga(T20, T22, add33_out_ga(T20, T22)) → add21_out_ga(T20, s(T22))
add21_in_ga(s(T34), s(T36)) → U3_ga(T34, T36, add21_in_ga(T34, T36))
U3_ga(T34, T36, add21_out_ga(T34, T36)) → add21_out_ga(s(T34), s(T36))
U18_ga(T7, add21_out_ga(T9, T7)) → fib1_out_ga(s(s(0)), T7)
fib1_in_ga(s(s(s(T41))), T7) → U19_ga(T41, T7, fib48_in_ga(T41, X80))
fib48_in_ga(0, s(0)) → fib48_out_ga(0, s(0))
fib48_in_ga(s(T45), X97) → U4_ga(T45, X97, p57_in_gaaa(T45, X95, X96, X97))
p57_in_gaaa(T45, X95, X96, X97) → U5_gaaa(T45, X95, X96, X97, fib48_in_ga(T45, X95))
U5_gaaa(T45, X95, X96, X97, fib48_out_ga(T45, X95)) → p57_out_gaaa(T45, X95, X96, X97)
p57_in_gaaa(T45, T46, X96, X97) → U6_gaaa(T45, T46, X96, X97, fib48_in_ga(T45, T46))
U6_gaaa(T45, T46, X96, X97, fib48_out_ga(T45, T46)) → U7_gaaa(T45, T46, X96, X97, fib61_in_ga(T45, X96))
fib61_in_ga(0, 0) → fib61_out_ga(0, 0)
fib61_in_ga(s(0), s(0)) → fib61_out_ga(s(0), s(0))
fib61_in_ga(s(s(T50)), X112) → U13_ga(T50, X112, p57_in_gaaa(T50, X110, X111, X112))
p57_in_gaaa(T45, T46, T47, X97) → U8_gaaa(T45, T46, T47, X97, fib48_in_ga(T45, T46))
U8_gaaa(T45, T46, T47, X97, fib48_out_ga(T45, T46)) → U9_gaaa(T45, T46, T47, X97, fib61_in_ga(T45, T47))
U9_gaaa(T45, T46, T47, X97, fib61_out_ga(T45, T47)) → U10_gaaa(T45, T46, T47, X97, add62_in_aaa(T46, T47, X97))
add62_in_aaa(0, 0, 0) → add62_out_aaa(0, 0, 0)
add62_in_aaa(s(T59), T60, s(X134)) → U11_aaa(T59, T60, X134, add62_in_aaa(T59, T60, X134))
add62_in_aaa(T65, s(T66), s(X149)) → U12_aaa(T65, T66, X149, add62_in_aaa(T65, T66, X149))
U12_aaa(T65, T66, X149, add62_out_aaa(T65, T66, X149)) → add62_out_aaa(T65, s(T66), s(X149))
U11_aaa(T59, T60, X134, add62_out_aaa(T59, T60, X134)) → add62_out_aaa(s(T59), T60, s(X134))
U10_gaaa(T45, T46, T47, X97, add62_out_aaa(T46, T47, X97)) → p57_out_gaaa(T45, T46, T47, X97)
U13_ga(T50, X112, p57_out_gaaa(T50, X110, X111, X112)) → fib61_out_ga(s(s(T50)), X112)
U7_gaaa(T45, T46, X96, X97, fib61_out_ga(T45, X96)) → p57_out_gaaa(T45, T46, X96, X97)
U4_ga(T45, X97, p57_out_gaaa(T45, X95, X96, X97)) → fib48_out_ga(s(T45), X97)
U19_ga(T41, T7, fib48_out_ga(T41, X80)) → fib1_out_ga(s(s(s(T41))), T7)
fib1_in_ga(s(s(s(T41))), T7) → U20_ga(T41, T7, fib48_in_ga(T41, T42))
U20_ga(T41, T7, fib48_out_ga(T41, T42)) → U21_ga(T41, T7, fib61_in_ga(T41, X81))
U21_ga(T41, T7, fib61_out_ga(T41, X81)) → fib1_out_ga(s(s(s(T41))), T7)
U20_ga(T41, T7, fib48_out_ga(T41, T42)) → U22_ga(T41, T7, T42, fib61_in_ga(T41, T67))
U22_ga(T41, T7, T42, fib61_out_ga(T41, T67)) → U23_ga(T41, T7, add62_in_aaa(T42, T67, X82))
U23_ga(T41, T7, add62_out_aaa(T42, T67, X82)) → fib1_out_ga(s(s(s(T41))), T7)
U22_ga(T41, T7, T42, fib61_out_ga(T41, T67)) → U24_ga(T41, T7, add62_in_aaa(T42, T67, T68))
U24_ga(T41, T7, add62_out_aaa(T42, T67, T68)) → U25_ga(T41, T7, fib48_in_ga(T41, X10))
U25_ga(T41, T7, fib48_out_ga(T41, X10)) → fib1_out_ga(s(s(s(T41))), T7)
U24_ga(T41, T7, add62_out_aaa(T42, T67, T68)) → U26_ga(T41, T7, T68, fib48_in_ga(T41, T69))
U26_ga(T41, T7, T68, fib48_out_ga(T41, T69)) → U27_ga(T41, T7, add93_in_gaa(T68, T69, T7))
add93_in_gaa(0, 0, 0) → add93_out_gaa(0, 0, 0)
add93_in_gaa(s(T82), T83, s(T85)) → U14_gaa(T82, T83, T85, add93_in_gaa(T82, T83, T85))
add93_in_gaa(T92, s(T93), s(T95)) → U15_gaa(T92, T93, T95, add93_in_gaa(T92, T93, T95))
U15_gaa(T92, T93, T95, add93_out_gaa(T92, T93, T95)) → add93_out_gaa(T92, s(T93), s(T95))
U14_gaa(T82, T83, T85, add93_out_gaa(T82, T83, T85)) → add93_out_gaa(s(T82), T83, s(T85))
U27_ga(T41, T7, add93_out_gaa(T68, T69, T7)) → fib1_out_ga(s(s(s(T41))), T7)

(83) UsableRulesProof (EQUIVALENT transformation)

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

(84) Obligation:

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

ADD21_IN_GA(s(T34), s(T36)) → ADD21_IN_GA(T34, T36)

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

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

(85) PiDPToQDPProof (SOUND transformation)

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

(86) Obligation:

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

ADD21_IN_GA(s(T34)) → ADD21_IN_GA(T34)

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

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

ADD21_IN_GA(s(T34)) → ADD21_IN_GA(T34)
The graph contains the following edges 1 > 1