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

(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) PrologToDTProblemTransformerProof (SOUND transformation)

Built DT 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:

Triples:

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

Clauses:

addc33(0, 0).
addc33(s(T27), s(T29)) :- addc33(T27, T29).
addc21(T20, s(T22)) :- addc33(T20, T22).
addc21(s(T34), s(T36)) :- addc21(T34, T36).
fibc48(0, s(0)).
fibc48(s(T45), X97) :- qc57(T45, X95, X96, X97).
qc57(T45, T46, T47, X97) :- ','(fibc48(T45, T46), ','(fibc61(T45, T47), addc62(T46, T47, X97))).
addc62(0, 0, 0).
addc62(s(T59), T60, s(X134)) :- addc62(T59, T60, X134).
addc62(T65, s(T66), s(X149)) :- addc62(T65, T66, X149).
fibc61(0, 0).
fibc61(s(0), s(0)).
fibc61(s(s(T50)), X112) :- qc57(T50, X110, X111, X112).
addc93(0, 0, 0).
addc93(s(T82), T83, s(T85)) :- addc93(T82, T83, T85).
addc93(T92, s(T93), s(T95)) :- addc93(T92, T93, T95).
fibc20(0).

Afs:

fib1(x1, x2)  =  fib1(x1)

(3) TriplesToPiDPProof (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)
fibc48_in: (b,f)
qc57_in: (b,f,f,f)
fibc61_in: (b,f)
addc62_in: (b,b,f)
fib61_in: (b,f)
add62_in: (b,b,f)
add93_in: (b,b,f)
Transforming TRIPLES into the following Term Rewriting System:
Pi DP problem:
The TRS P consists of the following rules:

FIB1_IN_GA(s(s(0)), T7) → U16_GA(T7, fibc20_in_a(T9))
U16_GA(T7, fibc20_out_a(T9)) → U17_GA(T7, add21_in_ga(T9, T7))
U16_GA(T7, fibc20_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) → U18_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, fibc48_in_ga(T45, T46))
U6_GAAA(T45, T46, X96, X97, fibc48_out_ga(T45, T46)) → U7_GAAA(T45, T46, X96, X97, fib61_in_ga(T45, X96))
U6_GAAA(T45, T46, X96, X97, fibc48_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, fibc48_in_ga(T45, T46))
U8_GAAA(T45, T46, T47, X97, fibc48_out_ga(T45, T46)) → U9_GAAA(T45, T46, T47, X97, fibc61_in_ga(T45, T47))
U9_GAAA(T45, T46, T47, X97, fibc61_out_ga(T45, T47)) → U10_GAAA(T45, T46, T47, X97, add62_in_gga(T46, T47, X97))
U9_GAAA(T45, T46, T47, X97, fibc61_out_ga(T45, T47)) → ADD62_IN_GGA(T46, T47, X97)
ADD62_IN_GGA(s(T59), T60, s(X134)) → U11_GGA(T59, T60, X134, add62_in_gga(T59, T60, X134))
ADD62_IN_GGA(s(T59), T60, s(X134)) → ADD62_IN_GGA(T59, T60, X134)
ADD62_IN_GGA(T65, s(T66), s(X149)) → U12_GGA(T65, T66, X149, add62_in_gga(T65, T66, X149))
ADD62_IN_GGA(T65, s(T66), s(X149)) → ADD62_IN_GGA(T65, T66, X149)
FIB1_IN_GA(s(s(s(T41))), T7) → U19_GA(T41, T7, fibc48_in_ga(T41, T42))
U19_GA(T41, T7, fibc48_out_ga(T41, T42)) → U20_GA(T41, T7, fib61_in_ga(T41, X81))
U19_GA(T41, T7, fibc48_out_ga(T41, T42)) → FIB61_IN_GA(T41, X81)
U19_GA(T41, T7, fibc48_out_ga(T41, T42)) → U21_GA(T41, T7, T42, fibc61_in_ga(T41, T67))
U21_GA(T41, T7, T42, fibc61_out_ga(T41, T67)) → U22_GA(T41, T7, add62_in_gga(T42, T67, X82))
U21_GA(T41, T7, T42, fibc61_out_ga(T41, T67)) → ADD62_IN_GGA(T42, T67, X82)
U21_GA(T41, T7, T42, fibc61_out_ga(T41, T67)) → U23_GA(T41, T7, addc62_in_gga(T42, T67, T68))
U23_GA(T41, T7, addc62_out_gga(T42, T67, T68)) → U24_GA(T41, T7, fib48_in_ga(T41, X10))
U23_GA(T41, T7, addc62_out_gga(T42, T67, T68)) → FIB48_IN_GA(T41, X10)
U23_GA(T41, T7, addc62_out_gga(T42, T67, T68)) → U25_GA(T41, T7, T68, fibc48_in_ga(T41, T69))
U25_GA(T41, T7, T68, fibc48_out_ga(T41, T69)) → U26_GA(T41, T7, add93_in_gga(T68, T69, T7))
U25_GA(T41, T7, T68, fibc48_out_ga(T41, T69)) → ADD93_IN_GGA(T68, T69, T7)
ADD93_IN_GGA(s(T82), T83, s(T85)) → U14_GGA(T82, T83, T85, add93_in_gga(T82, T83, T85))
ADD93_IN_GGA(s(T82), T83, s(T85)) → ADD93_IN_GGA(T82, T83, T85)
ADD93_IN_GGA(T92, s(T93), s(T95)) → U15_GGA(T92, T93, T95, add93_in_gga(T92, T93, T95))
ADD93_IN_GGA(T92, s(T93), s(T95)) → ADD93_IN_GGA(T92, T93, T95)

The TRS R consists of the following rules:

fibc20_in_a(0) → fibc20_out_a(0)
fibc48_in_ga(0, s(0)) → fibc48_out_ga(0, s(0))
fibc48_in_ga(s(T45), X97) → U31_ga(T45, X97, qc57_in_gaaa(T45, X95, X96, X97))
qc57_in_gaaa(T45, T46, T47, X97) → U32_gaaa(T45, T46, T47, X97, fibc48_in_ga(T45, T46))
U32_gaaa(T45, T46, T47, X97, fibc48_out_ga(T45, T46)) → U33_gaaa(T45, T46, T47, X97, fibc61_in_ga(T45, T47))
fibc61_in_ga(0, 0) → fibc61_out_ga(0, 0)
fibc61_in_ga(s(0), s(0)) → fibc61_out_ga(s(0), s(0))
fibc61_in_ga(s(s(T50)), X112) → U37_ga(T50, X112, qc57_in_gaaa(T50, X110, X111, X112))
U37_ga(T50, X112, qc57_out_gaaa(T50, X110, X111, X112)) → fibc61_out_ga(s(s(T50)), X112)
U33_gaaa(T45, T46, T47, X97, fibc61_out_ga(T45, T47)) → U34_gaaa(T45, T46, T47, X97, addc62_in_gga(T46, T47, X97))
addc62_in_gga(0, 0, 0) → addc62_out_gga(0, 0, 0)
addc62_in_gga(s(T59), T60, s(X134)) → U35_gga(T59, T60, X134, addc62_in_gga(T59, T60, X134))
addc62_in_gga(T65, s(T66), s(X149)) → U36_gga(T65, T66, X149, addc62_in_gga(T65, T66, X149))
U36_gga(T65, T66, X149, addc62_out_gga(T65, T66, X149)) → addc62_out_gga(T65, s(T66), s(X149))
U35_gga(T59, T60, X134, addc62_out_gga(T59, T60, X134)) → addc62_out_gga(s(T59), T60, s(X134))
U34_gaaa(T45, T46, T47, X97, addc62_out_gga(T46, T47, X97)) → qc57_out_gaaa(T45, T46, T47, X97)
U31_ga(T45, X97, qc57_out_gaaa(T45, X95, X96, X97)) → fibc48_out_ga(s(T45), X97)

The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
0  =  0
fibc20_in_a(x1)  =  fibc20_in_a
fibc20_out_a(x1)  =  fibc20_out_a(x1)
add21_in_ga(x1, x2)  =  add21_in_ga(x1)
add33_in_ga(x1, x2)  =  add33_in_ga(x1)
fib48_in_ga(x1, x2)  =  fib48_in_ga(x1)
p57_in_gaaa(x1, x2, x3, x4)  =  p57_in_gaaa(x1)
fibc48_in_ga(x1, x2)  =  fibc48_in_ga(x1)
fibc48_out_ga(x1, x2)  =  fibc48_out_ga(x1, x2)
U31_ga(x1, x2, x3)  =  U31_ga(x1, x3)
qc57_in_gaaa(x1, x2, x3, x4)  =  qc57_in_gaaa(x1)
U32_gaaa(x1, x2, x3, x4, x5)  =  U32_gaaa(x1, x5)
U33_gaaa(x1, x2, x3, x4, x5)  =  U33_gaaa(x1, x2, x5)
fibc61_in_ga(x1, x2)  =  fibc61_in_ga(x1)
fibc61_out_ga(x1, x2)  =  fibc61_out_ga(x1, x2)
U37_ga(x1, x2, x3)  =  U37_ga(x1, x3)
qc57_out_gaaa(x1, x2, x3, x4)  =  qc57_out_gaaa(x1, x2, x3, x4)
U34_gaaa(x1, x2, x3, x4, x5)  =  U34_gaaa(x1, x2, x3, x5)
addc62_in_gga(x1, x2, x3)  =  addc62_in_gga(x1, x2)
addc62_out_gga(x1, x2, x3)  =  addc62_out_gga(x1, x2, x3)
U35_gga(x1, x2, x3, x4)  =  U35_gga(x1, x2, x4)
U36_gga(x1, x2, x3, x4)  =  U36_gga(x1, x2, x4)
fib61_in_ga(x1, x2)  =  fib61_in_ga(x1)
add62_in_gga(x1, x2, x3)  =  add62_in_gga(x1, x2)
add93_in_gga(x1, x2, x3)  =  add93_in_gga(x1, x2)
FIB1_IN_GA(x1, x2)  =  FIB1_IN_GA(x1)
U16_GA(x1, x2)  =  U16_GA(x2)
U17_GA(x1, x2)  =  U17_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)
U18_GA(x1, x2, x3)  =  U18_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, x2, x5)
U10_GAAA(x1, x2, x3, x4, x5)  =  U10_GAAA(x1, x5)
ADD62_IN_GGA(x1, x2, x3)  =  ADD62_IN_GGA(x1, x2)
U11_GGA(x1, x2, x3, x4)  =  U11_GGA(x1, x2, x4)
U12_GGA(x1, x2, x3, x4)  =  U12_GGA(x1, x2, x4)
U19_GA(x1, x2, x3)  =  U19_GA(x1, x3)
U20_GA(x1, x2, x3)  =  U20_GA(x1, x3)
U21_GA(x1, x2, x3, x4)  =  U21_GA(x1, x3, x4)
U22_GA(x1, x2, x3)  =  U22_GA(x1, x3)
U23_GA(x1, x2, x3)  =  U23_GA(x1, x3)
U24_GA(x1, x2, x3)  =  U24_GA(x1, x3)
U25_GA(x1, x2, x3, x4)  =  U25_GA(x1, x3, x4)
U26_GA(x1, x2, x3)  =  U26_GA(x1, x3)
ADD93_IN_GGA(x1, x2, x3)  =  ADD93_IN_GGA(x1, x2)
U14_GGA(x1, x2, x3, x4)  =  U14_GGA(x1, x2, x4)
U15_GGA(x1, x2, x3, x4)  =  U15_GGA(x1, x2, x4)

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

Infinitary Constructor Rewriting Termination of PiDP implies Termination of TRIPLES

(4) Obligation:

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

FIB1_IN_GA(s(s(0)), T7) → U16_GA(T7, fibc20_in_a(T9))
U16_GA(T7, fibc20_out_a(T9)) → U17_GA(T7, add21_in_ga(T9, T7))
U16_GA(T7, fibc20_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) → U18_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, fibc48_in_ga(T45, T46))
U6_GAAA(T45, T46, X96, X97, fibc48_out_ga(T45, T46)) → U7_GAAA(T45, T46, X96, X97, fib61_in_ga(T45, X96))
U6_GAAA(T45, T46, X96, X97, fibc48_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, fibc48_in_ga(T45, T46))
U8_GAAA(T45, T46, T47, X97, fibc48_out_ga(T45, T46)) → U9_GAAA(T45, T46, T47, X97, fibc61_in_ga(T45, T47))
U9_GAAA(T45, T46, T47, X97, fibc61_out_ga(T45, T47)) → U10_GAAA(T45, T46, T47, X97, add62_in_gga(T46, T47, X97))
U9_GAAA(T45, T46, T47, X97, fibc61_out_ga(T45, T47)) → ADD62_IN_GGA(T46, T47, X97)
ADD62_IN_GGA(s(T59), T60, s(X134)) → U11_GGA(T59, T60, X134, add62_in_gga(T59, T60, X134))
ADD62_IN_GGA(s(T59), T60, s(X134)) → ADD62_IN_GGA(T59, T60, X134)
ADD62_IN_GGA(T65, s(T66), s(X149)) → U12_GGA(T65, T66, X149, add62_in_gga(T65, T66, X149))
ADD62_IN_GGA(T65, s(T66), s(X149)) → ADD62_IN_GGA(T65, T66, X149)
FIB1_IN_GA(s(s(s(T41))), T7) → U19_GA(T41, T7, fibc48_in_ga(T41, T42))
U19_GA(T41, T7, fibc48_out_ga(T41, T42)) → U20_GA(T41, T7, fib61_in_ga(T41, X81))
U19_GA(T41, T7, fibc48_out_ga(T41, T42)) → FIB61_IN_GA(T41, X81)
U19_GA(T41, T7, fibc48_out_ga(T41, T42)) → U21_GA(T41, T7, T42, fibc61_in_ga(T41, T67))
U21_GA(T41, T7, T42, fibc61_out_ga(T41, T67)) → U22_GA(T41, T7, add62_in_gga(T42, T67, X82))
U21_GA(T41, T7, T42, fibc61_out_ga(T41, T67)) → ADD62_IN_GGA(T42, T67, X82)
U21_GA(T41, T7, T42, fibc61_out_ga(T41, T67)) → U23_GA(T41, T7, addc62_in_gga(T42, T67, T68))
U23_GA(T41, T7, addc62_out_gga(T42, T67, T68)) → U24_GA(T41, T7, fib48_in_ga(T41, X10))
U23_GA(T41, T7, addc62_out_gga(T42, T67, T68)) → FIB48_IN_GA(T41, X10)
U23_GA(T41, T7, addc62_out_gga(T42, T67, T68)) → U25_GA(T41, T7, T68, fibc48_in_ga(T41, T69))
U25_GA(T41, T7, T68, fibc48_out_ga(T41, T69)) → U26_GA(T41, T7, add93_in_gga(T68, T69, T7))
U25_GA(T41, T7, T68, fibc48_out_ga(T41, T69)) → ADD93_IN_GGA(T68, T69, T7)
ADD93_IN_GGA(s(T82), T83, s(T85)) → U14_GGA(T82, T83, T85, add93_in_gga(T82, T83, T85))
ADD93_IN_GGA(s(T82), T83, s(T85)) → ADD93_IN_GGA(T82, T83, T85)
ADD93_IN_GGA(T92, s(T93), s(T95)) → U15_GGA(T92, T93, T95, add93_in_gga(T92, T93, T95))
ADD93_IN_GGA(T92, s(T93), s(T95)) → ADD93_IN_GGA(T92, T93, T95)

The TRS R consists of the following rules:

fibc20_in_a(0) → fibc20_out_a(0)
fibc48_in_ga(0, s(0)) → fibc48_out_ga(0, s(0))
fibc48_in_ga(s(T45), X97) → U31_ga(T45, X97, qc57_in_gaaa(T45, X95, X96, X97))
qc57_in_gaaa(T45, T46, T47, X97) → U32_gaaa(T45, T46, T47, X97, fibc48_in_ga(T45, T46))
U32_gaaa(T45, T46, T47, X97, fibc48_out_ga(T45, T46)) → U33_gaaa(T45, T46, T47, X97, fibc61_in_ga(T45, T47))
fibc61_in_ga(0, 0) → fibc61_out_ga(0, 0)
fibc61_in_ga(s(0), s(0)) → fibc61_out_ga(s(0), s(0))
fibc61_in_ga(s(s(T50)), X112) → U37_ga(T50, X112, qc57_in_gaaa(T50, X110, X111, X112))
U37_ga(T50, X112, qc57_out_gaaa(T50, X110, X111, X112)) → fibc61_out_ga(s(s(T50)), X112)
U33_gaaa(T45, T46, T47, X97, fibc61_out_ga(T45, T47)) → U34_gaaa(T45, T46, T47, X97, addc62_in_gga(T46, T47, X97))
addc62_in_gga(0, 0, 0) → addc62_out_gga(0, 0, 0)
addc62_in_gga(s(T59), T60, s(X134)) → U35_gga(T59, T60, X134, addc62_in_gga(T59, T60, X134))
addc62_in_gga(T65, s(T66), s(X149)) → U36_gga(T65, T66, X149, addc62_in_gga(T65, T66, X149))
U36_gga(T65, T66, X149, addc62_out_gga(T65, T66, X149)) → addc62_out_gga(T65, s(T66), s(X149))
U35_gga(T59, T60, X134, addc62_out_gga(T59, T60, X134)) → addc62_out_gga(s(T59), T60, s(X134))
U34_gaaa(T45, T46, T47, X97, addc62_out_gga(T46, T47, X97)) → qc57_out_gaaa(T45, T46, T47, X97)
U31_ga(T45, X97, qc57_out_gaaa(T45, X95, X96, X97)) → fibc48_out_ga(s(T45), X97)

The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
0  =  0
fibc20_in_a(x1)  =  fibc20_in_a
fibc20_out_a(x1)  =  fibc20_out_a(x1)
add21_in_ga(x1, x2)  =  add21_in_ga(x1)
add33_in_ga(x1, x2)  =  add33_in_ga(x1)
fib48_in_ga(x1, x2)  =  fib48_in_ga(x1)
p57_in_gaaa(x1, x2, x3, x4)  =  p57_in_gaaa(x1)
fibc48_in_ga(x1, x2)  =  fibc48_in_ga(x1)
fibc48_out_ga(x1, x2)  =  fibc48_out_ga(x1, x2)
U31_ga(x1, x2, x3)  =  U31_ga(x1, x3)
qc57_in_gaaa(x1, x2, x3, x4)  =  qc57_in_gaaa(x1)
U32_gaaa(x1, x2, x3, x4, x5)  =  U32_gaaa(x1, x5)
U33_gaaa(x1, x2, x3, x4, x5)  =  U33_gaaa(x1, x2, x5)
fibc61_in_ga(x1, x2)  =  fibc61_in_ga(x1)
fibc61_out_ga(x1, x2)  =  fibc61_out_ga(x1, x2)
U37_ga(x1, x2, x3)  =  U37_ga(x1, x3)
qc57_out_gaaa(x1, x2, x3, x4)  =  qc57_out_gaaa(x1, x2, x3, x4)
U34_gaaa(x1, x2, x3, x4, x5)  =  U34_gaaa(x1, x2, x3, x5)
addc62_in_gga(x1, x2, x3)  =  addc62_in_gga(x1, x2)
addc62_out_gga(x1, x2, x3)  =  addc62_out_gga(x1, x2, x3)
U35_gga(x1, x2, x3, x4)  =  U35_gga(x1, x2, x4)
U36_gga(x1, x2, x3, x4)  =  U36_gga(x1, x2, x4)
fib61_in_ga(x1, x2)  =  fib61_in_ga(x1)
add62_in_gga(x1, x2, x3)  =  add62_in_gga(x1, x2)
add93_in_gga(x1, x2, x3)  =  add93_in_gga(x1, x2)
FIB1_IN_GA(x1, x2)  =  FIB1_IN_GA(x1)
U16_GA(x1, x2)  =  U16_GA(x2)
U17_GA(x1, x2)  =  U17_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)
U18_GA(x1, x2, x3)  =  U18_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, x2, x5)
U10_GAAA(x1, x2, x3, x4, x5)  =  U10_GAAA(x1, x5)
ADD62_IN_GGA(x1, x2, x3)  =  ADD62_IN_GGA(x1, x2)
U11_GGA(x1, x2, x3, x4)  =  U11_GGA(x1, x2, x4)
U12_GGA(x1, x2, x3, x4)  =  U12_GGA(x1, x2, x4)
U19_GA(x1, x2, x3)  =  U19_GA(x1, x3)
U20_GA(x1, x2, x3)  =  U20_GA(x1, x3)
U21_GA(x1, x2, x3, x4)  =  U21_GA(x1, x3, x4)
U22_GA(x1, x2, x3)  =  U22_GA(x1, x3)
U23_GA(x1, x2, x3)  =  U23_GA(x1, x3)
U24_GA(x1, x2, x3)  =  U24_GA(x1, x3)
U25_GA(x1, x2, x3, x4)  =  U25_GA(x1, x3, x4)
U26_GA(x1, x2, x3)  =  U26_GA(x1, x3)
ADD93_IN_GGA(x1, x2, x3)  =  ADD93_IN_GGA(x1, x2)
U14_GGA(x1, x2, x3, x4)  =  U14_GGA(x1, x2, x4)
U15_GGA(x1, x2, x3, x4)  =  U15_GGA(x1, x2, x4)

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

(5) DependencyGraphProof (EQUIVALENT transformation)

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

(6) Complex Obligation (AND)

(7) Obligation:

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

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

The TRS R consists of the following rules:

fibc20_in_a(0) → fibc20_out_a(0)
fibc48_in_ga(0, s(0)) → fibc48_out_ga(0, s(0))
fibc48_in_ga(s(T45), X97) → U31_ga(T45, X97, qc57_in_gaaa(T45, X95, X96, X97))
qc57_in_gaaa(T45, T46, T47, X97) → U32_gaaa(T45, T46, T47, X97, fibc48_in_ga(T45, T46))
U32_gaaa(T45, T46, T47, X97, fibc48_out_ga(T45, T46)) → U33_gaaa(T45, T46, T47, X97, fibc61_in_ga(T45, T47))
fibc61_in_ga(0, 0) → fibc61_out_ga(0, 0)
fibc61_in_ga(s(0), s(0)) → fibc61_out_ga(s(0), s(0))
fibc61_in_ga(s(s(T50)), X112) → U37_ga(T50, X112, qc57_in_gaaa(T50, X110, X111, X112))
U37_ga(T50, X112, qc57_out_gaaa(T50, X110, X111, X112)) → fibc61_out_ga(s(s(T50)), X112)
U33_gaaa(T45, T46, T47, X97, fibc61_out_ga(T45, T47)) → U34_gaaa(T45, T46, T47, X97, addc62_in_gga(T46, T47, X97))
addc62_in_gga(0, 0, 0) → addc62_out_gga(0, 0, 0)
addc62_in_gga(s(T59), T60, s(X134)) → U35_gga(T59, T60, X134, addc62_in_gga(T59, T60, X134))
addc62_in_gga(T65, s(T66), s(X149)) → U36_gga(T65, T66, X149, addc62_in_gga(T65, T66, X149))
U36_gga(T65, T66, X149, addc62_out_gga(T65, T66, X149)) → addc62_out_gga(T65, s(T66), s(X149))
U35_gga(T59, T60, X134, addc62_out_gga(T59, T60, X134)) → addc62_out_gga(s(T59), T60, s(X134))
U34_gaaa(T45, T46, T47, X97, addc62_out_gga(T46, T47, X97)) → qc57_out_gaaa(T45, T46, T47, X97)
U31_ga(T45, X97, qc57_out_gaaa(T45, X95, X96, X97)) → fibc48_out_ga(s(T45), X97)

The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
0  =  0
fibc20_in_a(x1)  =  fibc20_in_a
fibc20_out_a(x1)  =  fibc20_out_a(x1)
fibc48_in_ga(x1, x2)  =  fibc48_in_ga(x1)
fibc48_out_ga(x1, x2)  =  fibc48_out_ga(x1, x2)
U31_ga(x1, x2, x3)  =  U31_ga(x1, x3)
qc57_in_gaaa(x1, x2, x3, x4)  =  qc57_in_gaaa(x1)
U32_gaaa(x1, x2, x3, x4, x5)  =  U32_gaaa(x1, x5)
U33_gaaa(x1, x2, x3, x4, x5)  =  U33_gaaa(x1, x2, x5)
fibc61_in_ga(x1, x2)  =  fibc61_in_ga(x1)
fibc61_out_ga(x1, x2)  =  fibc61_out_ga(x1, x2)
U37_ga(x1, x2, x3)  =  U37_ga(x1, x3)
qc57_out_gaaa(x1, x2, x3, x4)  =  qc57_out_gaaa(x1, x2, x3, x4)
U34_gaaa(x1, x2, x3, x4, x5)  =  U34_gaaa(x1, x2, x3, x5)
addc62_in_gga(x1, x2, x3)  =  addc62_in_gga(x1, x2)
addc62_out_gga(x1, x2, x3)  =  addc62_out_gga(x1, x2, x3)
U35_gga(x1, x2, x3, x4)  =  U35_gga(x1, x2, x4)
U36_gga(x1, x2, x3, x4)  =  U36_gga(x1, x2, x4)
ADD93_IN_GGA(x1, x2, x3)  =  ADD93_IN_GGA(x1, x2)

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

(8) UsableRulesProof (EQUIVALENT transformation)

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

(9) Obligation:

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

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

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

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

(10) PiDPToQDPProof (SOUND transformation)

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

(11) Obligation:

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

ADD93_IN_GGA(T92, s(T93)) → ADD93_IN_GGA(T92, T93)
ADD93_IN_GGA(s(T82), T83) → ADD93_IN_GGA(T82, T83)

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

(12) QDPSizeChangeProof (EQUIVALENT transformation)

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

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

• ADD93_IN_GGA(T92, s(T93)) → ADD93_IN_GGA(T92, T93)
  The graph contains the following edges 1 >= 1, 2 > 2

• ADD93_IN_GGA(s(T82), T83) → ADD93_IN_GGA(T82, T83)
  The graph contains the following edges 1 > 1, 2 >= 2

(13) YES

(14) Obligation:

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

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

The TRS R consists of the following rules:

fibc20_in_a(0) → fibc20_out_a(0)
fibc48_in_ga(0, s(0)) → fibc48_out_ga(0, s(0))
fibc48_in_ga(s(T45), X97) → U31_ga(T45, X97, qc57_in_gaaa(T45, X95, X96, X97))
qc57_in_gaaa(T45, T46, T47, X97) → U32_gaaa(T45, T46, T47, X97, fibc48_in_ga(T45, T46))
U32_gaaa(T45, T46, T47, X97, fibc48_out_ga(T45, T46)) → U33_gaaa(T45, T46, T47, X97, fibc61_in_ga(T45, T47))
fibc61_in_ga(0, 0) → fibc61_out_ga(0, 0)
fibc61_in_ga(s(0), s(0)) → fibc61_out_ga(s(0), s(0))
fibc61_in_ga(s(s(T50)), X112) → U37_ga(T50, X112, qc57_in_gaaa(T50, X110, X111, X112))
U37_ga(T50, X112, qc57_out_gaaa(T50, X110, X111, X112)) → fibc61_out_ga(s(s(T50)), X112)
U33_gaaa(T45, T46, T47, X97, fibc61_out_ga(T45, T47)) → U34_gaaa(T45, T46, T47, X97, addc62_in_gga(T46, T47, X97))
addc62_in_gga(0, 0, 0) → addc62_out_gga(0, 0, 0)
addc62_in_gga(s(T59), T60, s(X134)) → U35_gga(T59, T60, X134, addc62_in_gga(T59, T60, X134))
addc62_in_gga(T65, s(T66), s(X149)) → U36_gga(T65, T66, X149, addc62_in_gga(T65, T66, X149))
U36_gga(T65, T66, X149, addc62_out_gga(T65, T66, X149)) → addc62_out_gga(T65, s(T66), s(X149))
U35_gga(T59, T60, X134, addc62_out_gga(T59, T60, X134)) → addc62_out_gga(s(T59), T60, s(X134))
U34_gaaa(T45, T46, T47, X97, addc62_out_gga(T46, T47, X97)) → qc57_out_gaaa(T45, T46, T47, X97)
U31_ga(T45, X97, qc57_out_gaaa(T45, X95, X96, X97)) → fibc48_out_ga(s(T45), X97)

The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
0  =  0
fibc20_in_a(x1)  =  fibc20_in_a
fibc20_out_a(x1)  =  fibc20_out_a(x1)
fibc48_in_ga(x1, x2)  =  fibc48_in_ga(x1)
fibc48_out_ga(x1, x2)  =  fibc48_out_ga(x1, x2)
U31_ga(x1, x2, x3)  =  U31_ga(x1, x3)
qc57_in_gaaa(x1, x2, x3, x4)  =  qc57_in_gaaa(x1)
U32_gaaa(x1, x2, x3, x4, x5)  =  U32_gaaa(x1, x5)
U33_gaaa(x1, x2, x3, x4, x5)  =  U33_gaaa(x1, x2, x5)
fibc61_in_ga(x1, x2)  =  fibc61_in_ga(x1)
fibc61_out_ga(x1, x2)  =  fibc61_out_ga(x1, x2)
U37_ga(x1, x2, x3)  =  U37_ga(x1, x3)
qc57_out_gaaa(x1, x2, x3, x4)  =  qc57_out_gaaa(x1, x2, x3, x4)
U34_gaaa(x1, x2, x3, x4, x5)  =  U34_gaaa(x1, x2, x3, x5)
addc62_in_gga(x1, x2, x3)  =  addc62_in_gga(x1, x2)
addc62_out_gga(x1, x2, x3)  =  addc62_out_gga(x1, x2, x3)
U35_gga(x1, x2, x3, x4)  =  U35_gga(x1, x2, x4)
U36_gga(x1, x2, x3, x4)  =  U36_gga(x1, x2, x4)
ADD62_IN_GGA(x1, x2, x3)  =  ADD62_IN_GGA(x1, x2)

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

(15) UsableRulesProof (EQUIVALENT transformation)

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

(16) Obligation:

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

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

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

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

(17) PiDPToQDPProof (SOUND transformation)

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

(18) Obligation:

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

ADD62_IN_GGA(T65, s(T66)) → ADD62_IN_GGA(T65, T66)
ADD62_IN_GGA(s(T59), T60) → ADD62_IN_GGA(T59, T60)

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

(19) QDPSizeChangeProof (EQUIVALENT transformation)

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

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

• ADD62_IN_GGA(T65, s(T66)) → ADD62_IN_GGA(T65, T66)
  The graph contains the following edges 1 >= 1, 2 > 2

• ADD62_IN_GGA(s(T59), T60) → ADD62_IN_GGA(T59, T60)
  The graph contains the following edges 1 > 1, 2 >= 2

(20) YES

(21) 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, fibc48_in_ga(T45, T46))
U6_GAAA(T45, T46, X96, X97, fibc48_out_ga(T45, T46)) → FIB61_IN_GA(T45, X96)
FIB61_IN_GA(s(s(T50)), X112) → P57_IN_GAAA(T50, X110, X111, X112)

The TRS R consists of the following rules:

fibc20_in_a(0) → fibc20_out_a(0)
fibc48_in_ga(0, s(0)) → fibc48_out_ga(0, s(0))
fibc48_in_ga(s(T45), X97) → U31_ga(T45, X97, qc57_in_gaaa(T45, X95, X96, X97))
qc57_in_gaaa(T45, T46, T47, X97) → U32_gaaa(T45, T46, T47, X97, fibc48_in_ga(T45, T46))
U32_gaaa(T45, T46, T47, X97, fibc48_out_ga(T45, T46)) → U33_gaaa(T45, T46, T47, X97, fibc61_in_ga(T45, T47))
fibc61_in_ga(0, 0) → fibc61_out_ga(0, 0)
fibc61_in_ga(s(0), s(0)) → fibc61_out_ga(s(0), s(0))
fibc61_in_ga(s(s(T50)), X112) → U37_ga(T50, X112, qc57_in_gaaa(T50, X110, X111, X112))
U37_ga(T50, X112, qc57_out_gaaa(T50, X110, X111, X112)) → fibc61_out_ga(s(s(T50)), X112)
U33_gaaa(T45, T46, T47, X97, fibc61_out_ga(T45, T47)) → U34_gaaa(T45, T46, T47, X97, addc62_in_gga(T46, T47, X97))
addc62_in_gga(0, 0, 0) → addc62_out_gga(0, 0, 0)
addc62_in_gga(s(T59), T60, s(X134)) → U35_gga(T59, T60, X134, addc62_in_gga(T59, T60, X134))
addc62_in_gga(T65, s(T66), s(X149)) → U36_gga(T65, T66, X149, addc62_in_gga(T65, T66, X149))
U36_gga(T65, T66, X149, addc62_out_gga(T65, T66, X149)) → addc62_out_gga(T65, s(T66), s(X149))
U35_gga(T59, T60, X134, addc62_out_gga(T59, T60, X134)) → addc62_out_gga(s(T59), T60, s(X134))
U34_gaaa(T45, T46, T47, X97, addc62_out_gga(T46, T47, X97)) → qc57_out_gaaa(T45, T46, T47, X97)
U31_ga(T45, X97, qc57_out_gaaa(T45, X95, X96, X97)) → fibc48_out_ga(s(T45), X97)

The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
0  =  0
fibc20_in_a(x1)  =  fibc20_in_a
fibc20_out_a(x1)  =  fibc20_out_a(x1)
fibc48_in_ga(x1, x2)  =  fibc48_in_ga(x1)
fibc48_out_ga(x1, x2)  =  fibc48_out_ga(x1, x2)
U31_ga(x1, x2, x3)  =  U31_ga(x1, x3)
qc57_in_gaaa(x1, x2, x3, x4)  =  qc57_in_gaaa(x1)
U32_gaaa(x1, x2, x3, x4, x5)  =  U32_gaaa(x1, x5)
U33_gaaa(x1, x2, x3, x4, x5)  =  U33_gaaa(x1, x2, x5)
fibc61_in_ga(x1, x2)  =  fibc61_in_ga(x1)
fibc61_out_ga(x1, x2)  =  fibc61_out_ga(x1, x2)
U37_ga(x1, x2, x3)  =  U37_ga(x1, x3)
qc57_out_gaaa(x1, x2, x3, x4)  =  qc57_out_gaaa(x1, x2, x3, x4)
U34_gaaa(x1, x2, x3, x4, x5)  =  U34_gaaa(x1, x2, x3, x5)
addc62_in_gga(x1, x2, x3)  =  addc62_in_gga(x1, x2)
addc62_out_gga(x1, x2, x3)  =  addc62_out_gga(x1, x2, x3)
U35_gga(x1, x2, x3, x4)  =  U35_gga(x1, x2, x4)
U36_gga(x1, x2, x3, x4)  =  U36_gga(x1, x2, 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)

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

(22) UsableRulesProof (EQUIVALENT transformation)

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

(23) Obligation:

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

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, fibc48_in_ga(T45, T46))
U6_GAAA(T45, T46, X96, X97, fibc48_out_ga(T45, T46)) → FIB61_IN_GA(T45, X96)
FIB61_IN_GA(s(s(T50)), X112) → P57_IN_GAAA(T50, X110, X111, X112)

The TRS R consists of the following rules:

fibc48_in_ga(0, s(0)) → fibc48_out_ga(0, s(0))
fibc48_in_ga(s(T45), X97) → U31_ga(T45, X97, qc57_in_gaaa(T45, X95, X96, X97))
U31_ga(T45, X97, qc57_out_gaaa(T45, X95, X96, X97)) → fibc48_out_ga(s(T45), X97)
qc57_in_gaaa(T45, T46, T47, X97) → U32_gaaa(T45, T46, T47, X97, fibc48_in_ga(T45, T46))
U32_gaaa(T45, T46, T47, X97, fibc48_out_ga(T45, T46)) → U33_gaaa(T45, T46, T47, X97, fibc61_in_ga(T45, T47))
U33_gaaa(T45, T46, T47, X97, fibc61_out_ga(T45, T47)) → U34_gaaa(T45, T46, T47, X97, addc62_in_gga(T46, T47, X97))
fibc61_in_ga(0, 0) → fibc61_out_ga(0, 0)
fibc61_in_ga(s(0), s(0)) → fibc61_out_ga(s(0), s(0))
fibc61_in_ga(s(s(T50)), X112) → U37_ga(T50, X112, qc57_in_gaaa(T50, X110, X111, X112))
U34_gaaa(T45, T46, T47, X97, addc62_out_gga(T46, T47, X97)) → qc57_out_gaaa(T45, T46, T47, X97)
U37_ga(T50, X112, qc57_out_gaaa(T50, X110, X111, X112)) → fibc61_out_ga(s(s(T50)), X112)
addc62_in_gga(0, 0, 0) → addc62_out_gga(0, 0, 0)
addc62_in_gga(s(T59), T60, s(X134)) → U35_gga(T59, T60, X134, addc62_in_gga(T59, T60, X134))
addc62_in_gga(T65, s(T66), s(X149)) → U36_gga(T65, T66, X149, addc62_in_gga(T65, T66, X149))
U35_gga(T59, T60, X134, addc62_out_gga(T59, T60, X134)) → addc62_out_gga(s(T59), T60, s(X134))
U36_gga(T65, T66, X149, addc62_out_gga(T65, T66, X149)) → addc62_out_gga(T65, s(T66), s(X149))

The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
0  =  0
fibc48_in_ga(x1, x2)  =  fibc48_in_ga(x1)
fibc48_out_ga(x1, x2)  =  fibc48_out_ga(x1, x2)
U31_ga(x1, x2, x3)  =  U31_ga(x1, x3)
qc57_in_gaaa(x1, x2, x3, x4)  =  qc57_in_gaaa(x1)
U32_gaaa(x1, x2, x3, x4, x5)  =  U32_gaaa(x1, x5)
U33_gaaa(x1, x2, x3, x4, x5)  =  U33_gaaa(x1, x2, x5)
fibc61_in_ga(x1, x2)  =  fibc61_in_ga(x1)
fibc61_out_ga(x1, x2)  =  fibc61_out_ga(x1, x2)
U37_ga(x1, x2, x3)  =  U37_ga(x1, x3)
qc57_out_gaaa(x1, x2, x3, x4)  =  qc57_out_gaaa(x1, x2, x3, x4)
U34_gaaa(x1, x2, x3, x4, x5)  =  U34_gaaa(x1, x2, x3, x5)
addc62_in_gga(x1, x2, x3)  =  addc62_in_gga(x1, x2)
addc62_out_gga(x1, x2, x3)  =  addc62_out_gga(x1, x2, x3)
U35_gga(x1, x2, x3, x4)  =  U35_gga(x1, x2, x4)
U36_gga(x1, x2, x3, x4)  =  U36_gga(x1, x2, 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)

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

(24) PiDPToQDPProof (SOUND transformation)

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

(25) Obligation:

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

FIB48_IN_GA(s(T45)) → P57_IN_GAAA(T45)
P57_IN_GAAA(T45) → FIB48_IN_GA(T45)
P57_IN_GAAA(T45) → U6_GAAA(T45, fibc48_in_ga(T45))
U6_GAAA(T45, fibc48_out_ga(T45, T46)) → FIB61_IN_GA(T45)
FIB61_IN_GA(s(s(T50))) → P57_IN_GAAA(T50)

The TRS R consists of the following rules:

fibc48_in_ga(0) → fibc48_out_ga(0, s(0))
fibc48_in_ga(s(T45)) → U31_ga(T45, qc57_in_gaaa(T45))
U31_ga(T45, qc57_out_gaaa(T45, X95, X96, X97)) → fibc48_out_ga(s(T45), X97)
qc57_in_gaaa(T45) → U32_gaaa(T45, fibc48_in_ga(T45))
U32_gaaa(T45, fibc48_out_ga(T45, T46)) → U33_gaaa(T45, T46, fibc61_in_ga(T45))
U33_gaaa(T45, T46, fibc61_out_ga(T45, T47)) → U34_gaaa(T45, T46, T47, addc62_in_gga(T46, T47))
fibc61_in_ga(0) → fibc61_out_ga(0, 0)
fibc61_in_ga(s(0)) → fibc61_out_ga(s(0), s(0))
fibc61_in_ga(s(s(T50))) → U37_ga(T50, qc57_in_gaaa(T50))
U34_gaaa(T45, T46, T47, addc62_out_gga(T46, T47, X97)) → qc57_out_gaaa(T45, T46, T47, X97)
U37_ga(T50, qc57_out_gaaa(T50, X110, X111, X112)) → fibc61_out_ga(s(s(T50)), X112)
addc62_in_gga(0, 0) → addc62_out_gga(0, 0, 0)
addc62_in_gga(s(T59), T60) → U35_gga(T59, T60, addc62_in_gga(T59, T60))
addc62_in_gga(T65, s(T66)) → U36_gga(T65, T66, addc62_in_gga(T65, T66))
U35_gga(T59, T60, addc62_out_gga(T59, T60, X134)) → addc62_out_gga(s(T59), T60, s(X134))
U36_gga(T65, T66, addc62_out_gga(T65, T66, X149)) → addc62_out_gga(T65, s(T66), s(X149))

The set Q consists of the following terms:

fibc48_in_ga(x0)
U31_ga(x0, x1)
qc57_in_gaaa(x0)
U32_gaaa(x0, x1)
U33_gaaa(x0, x1, x2)
fibc61_in_ga(x0)
U34_gaaa(x0, x1, x2, x3)
U37_ga(x0, x1)
addc62_in_gga(x0, x1)
U35_gga(x0, x1, x2)
U36_gga(x0, x1, x2)

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

(26) QDPSizeChangeProof (EQUIVALENT transformation)

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

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

• P57_IN_GAAA(T45) → FIB48_IN_GA(T45)
  The graph contains the following edges 1 >= 1

• P57_IN_GAAA(T45) → U6_GAAA(T45, fibc48_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, fibc48_out_ga(T45, T46)) → FIB61_IN_GA(T45)
  The graph contains the following edges 1 >= 1, 2 > 1

(27) YES

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

fibc20_in_a(0) → fibc20_out_a(0)
fibc48_in_ga(0, s(0)) → fibc48_out_ga(0, s(0))
fibc48_in_ga(s(T45), X97) → U31_ga(T45, X97, qc57_in_gaaa(T45, X95, X96, X97))
qc57_in_gaaa(T45, T46, T47, X97) → U32_gaaa(T45, T46, T47, X97, fibc48_in_ga(T45, T46))
U32_gaaa(T45, T46, T47, X97, fibc48_out_ga(T45, T46)) → U33_gaaa(T45, T46, T47, X97, fibc61_in_ga(T45, T47))
fibc61_in_ga(0, 0) → fibc61_out_ga(0, 0)
fibc61_in_ga(s(0), s(0)) → fibc61_out_ga(s(0), s(0))
fibc61_in_ga(s(s(T50)), X112) → U37_ga(T50, X112, qc57_in_gaaa(T50, X110, X111, X112))
U37_ga(T50, X112, qc57_out_gaaa(T50, X110, X111, X112)) → fibc61_out_ga(s(s(T50)), X112)
U33_gaaa(T45, T46, T47, X97, fibc61_out_ga(T45, T47)) → U34_gaaa(T45, T46, T47, X97, addc62_in_gga(T46, T47, X97))
addc62_in_gga(0, 0, 0) → addc62_out_gga(0, 0, 0)
addc62_in_gga(s(T59), T60, s(X134)) → U35_gga(T59, T60, X134, addc62_in_gga(T59, T60, X134))
addc62_in_gga(T65, s(T66), s(X149)) → U36_gga(T65, T66, X149, addc62_in_gga(T65, T66, X149))
U36_gga(T65, T66, X149, addc62_out_gga(T65, T66, X149)) → addc62_out_gga(T65, s(T66), s(X149))
U35_gga(T59, T60, X134, addc62_out_gga(T59, T60, X134)) → addc62_out_gga(s(T59), T60, s(X134))
U34_gaaa(T45, T46, T47, X97, addc62_out_gga(T46, T47, X97)) → qc57_out_gaaa(T45, T46, T47, X97)
U31_ga(T45, X97, qc57_out_gaaa(T45, X95, X96, X97)) → fibc48_out_ga(s(T45), X97)

The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
0  =  0
fibc20_in_a(x1)  =  fibc20_in_a
fibc20_out_a(x1)  =  fibc20_out_a(x1)
fibc48_in_ga(x1, x2)  =  fibc48_in_ga(x1)
fibc48_out_ga(x1, x2)  =  fibc48_out_ga(x1, x2)
U31_ga(x1, x2, x3)  =  U31_ga(x1, x3)
qc57_in_gaaa(x1, x2, x3, x4)  =  qc57_in_gaaa(x1)
U32_gaaa(x1, x2, x3, x4, x5)  =  U32_gaaa(x1, x5)
U33_gaaa(x1, x2, x3, x4, x5)  =  U33_gaaa(x1, x2, x5)
fibc61_in_ga(x1, x2)  =  fibc61_in_ga(x1)
fibc61_out_ga(x1, x2)  =  fibc61_out_ga(x1, x2)
U37_ga(x1, x2, x3)  =  U37_ga(x1, x3)
qc57_out_gaaa(x1, x2, x3, x4)  =  qc57_out_gaaa(x1, x2, x3, x4)
U34_gaaa(x1, x2, x3, x4, x5)  =  U34_gaaa(x1, x2, x3, x5)
addc62_in_gga(x1, x2, x3)  =  addc62_in_gga(x1, x2)
addc62_out_gga(x1, x2, x3)  =  addc62_out_gga(x1, x2, x3)
U35_gga(x1, x2, x3, x4)  =  U35_gga(x1, x2, x4)
U36_gga(x1, x2, x3, x4)  =  U36_gga(x1, x2, x4)
ADD33_IN_GA(x1, x2)  =  ADD33_IN_GA(x1)

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

(29) UsableRulesProof (EQUIVALENT transformation)

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

(30) Obligation:

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

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

(31) PiDPToQDPProof (SOUND transformation)

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

(32) Obligation:

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

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

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

(33) QDPSizeChangeProof (EQUIVALENT transformation)

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

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

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

(34) YES

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

fibc20_in_a(0) → fibc20_out_a(0)
fibc48_in_ga(0, s(0)) → fibc48_out_ga(0, s(0))
fibc48_in_ga(s(T45), X97) → U31_ga(T45, X97, qc57_in_gaaa(T45, X95, X96, X97))
qc57_in_gaaa(T45, T46, T47, X97) → U32_gaaa(T45, T46, T47, X97, fibc48_in_ga(T45, T46))
U32_gaaa(T45, T46, T47, X97, fibc48_out_ga(T45, T46)) → U33_gaaa(T45, T46, T47, X97, fibc61_in_ga(T45, T47))
fibc61_in_ga(0, 0) → fibc61_out_ga(0, 0)
fibc61_in_ga(s(0), s(0)) → fibc61_out_ga(s(0), s(0))
fibc61_in_ga(s(s(T50)), X112) → U37_ga(T50, X112, qc57_in_gaaa(T50, X110, X111, X112))
U37_ga(T50, X112, qc57_out_gaaa(T50, X110, X111, X112)) → fibc61_out_ga(s(s(T50)), X112)
U33_gaaa(T45, T46, T47, X97, fibc61_out_ga(T45, T47)) → U34_gaaa(T45, T46, T47, X97, addc62_in_gga(T46, T47, X97))
addc62_in_gga(0, 0, 0) → addc62_out_gga(0, 0, 0)
addc62_in_gga(s(T59), T60, s(X134)) → U35_gga(T59, T60, X134, addc62_in_gga(T59, T60, X134))
addc62_in_gga(T65, s(T66), s(X149)) → U36_gga(T65, T66, X149, addc62_in_gga(T65, T66, X149))
U36_gga(T65, T66, X149, addc62_out_gga(T65, T66, X149)) → addc62_out_gga(T65, s(T66), s(X149))
U35_gga(T59, T60, X134, addc62_out_gga(T59, T60, X134)) → addc62_out_gga(s(T59), T60, s(X134))
U34_gaaa(T45, T46, T47, X97, addc62_out_gga(T46, T47, X97)) → qc57_out_gaaa(T45, T46, T47, X97)
U31_ga(T45, X97, qc57_out_gaaa(T45, X95, X96, X97)) → fibc48_out_ga(s(T45), X97)

The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
0  =  0
fibc20_in_a(x1)  =  fibc20_in_a
fibc20_out_a(x1)  =  fibc20_out_a(x1)
fibc48_in_ga(x1, x2)  =  fibc48_in_ga(x1)
fibc48_out_ga(x1, x2)  =  fibc48_out_ga(x1, x2)
U31_ga(x1, x2, x3)  =  U31_ga(x1, x3)
qc57_in_gaaa(x1, x2, x3, x4)  =  qc57_in_gaaa(x1)
U32_gaaa(x1, x2, x3, x4, x5)  =  U32_gaaa(x1, x5)
U33_gaaa(x1, x2, x3, x4, x5)  =  U33_gaaa(x1, x2, x5)
fibc61_in_ga(x1, x2)  =  fibc61_in_ga(x1)
fibc61_out_ga(x1, x2)  =  fibc61_out_ga(x1, x2)
U37_ga(x1, x2, x3)  =  U37_ga(x1, x3)
qc57_out_gaaa(x1, x2, x3, x4)  =  qc57_out_gaaa(x1, x2, x3, x4)
U34_gaaa(x1, x2, x3, x4, x5)  =  U34_gaaa(x1, x2, x3, x5)
addc62_in_gga(x1, x2, x3)  =  addc62_in_gga(x1, x2)
addc62_out_gga(x1, x2, x3)  =  addc62_out_gga(x1, x2, x3)
U35_gga(x1, x2, x3, x4)  =  U35_gga(x1, x2, x4)
U36_gga(x1, x2, x3, x4)  =  U36_gga(x1, x2, x4)
ADD21_IN_GA(x1, x2)  =  ADD21_IN_GA(x1)

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

(36) UsableRulesProof (EQUIVALENT transformation)

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

(37) Obligation:

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

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

(38) PiDPToQDPProof (SOUND transformation)

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

(39) Obligation:

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

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

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

(40) QDPSizeChangeProof (EQUIVALENT transformation)

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

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

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

(41) YES