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

(0) Obligation:

Clauses:

search_tree(void).
search_tree(T) :- search_tree(T, X1, X2).
search_tree(tree(X, void, void), X, X).
search_tree(tree(X, void, Right), X, Max) :- ','(search_tree(Right, Min, Max), less(X, Min)).
search_tree(tree(X, Left, void), Min, X) :- ','(search_tree(Left, Min, Max), less(Max, X)).
search_tree(tree(X, Left, Right), Min1, Max2) :- ','(search_tree(Left, Min1, Max1), ','(less(Max1, X), ','(search_tree(Right, Min2, Max2), less(X, Min2)))).
less(0, s(X3)).
less(s(X), s(Y)) :- less(X, Y).

Query: search_tree(g)

(1) PrologToPiTRSViaGraphTransformerProof (SOUND transformation)

Transformed Prolog program to (Pi-)TRS.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
1 [label="A: search_tree(T1)\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
5 [label="5: search_tree(T1), SCOPE: 1, CLAUSE: 0 | search_tree(T1), SCOPE: 1, CLAUSE: 1\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
9 [label="9: true | search_tree(void), SCOPE: 1, CLAUSE: 1\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
11 [label="11: search_tree(T1), SCOPE: 1, CLAUSE: 1\n\nT1 is ground\nsearch_tree(T1) !=? search_tree(void)", fontsize=16, style=filled, fillcolor=lightyellow];
16 [label="16: search_tree(void), SCOPE: 1, CLAUSE: 1\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
18 [label="18: search_tree(void, X6, X7)\n\nX6 is free\nX7 is free", fontsize=16, style=filled, fillcolor=lightyellow];
20 [label="20: search_tree(void, X6, X7), SCOPE: 2, CLAUSE: 2 | search_tree(void, X6, X7), SCOPE: 2, CLAUSE: 3 | search_tree(void, X6, X7), SCOPE: 2, CLAUSE: 4 | search_tree(void, X6, X7), SCOPE: 2, CLAUSE: 5\n\nX6 is free\nX7 is free", fontsize=16, style=filled, fillcolor=lightyellow];
23 [label="23: search_tree(void, X6, X7), SCOPE: 2, CLAUSE: 3 | search_tree(void, X6, X7), SCOPE: 2, CLAUSE: 4 | search_tree(void, X6, X7), SCOPE: 2, CLAUSE: 5\n\nX6 is free\nX7 is free", fontsize=16, style=filled, fillcolor=lightyellow];
25 [label="25: search_tree(void, X6, X7), SCOPE: 2, CLAUSE: 4 | search_tree(void, X6, X7), SCOPE: 2, CLAUSE: 5\n\nX6 is free\nX7 is free", fontsize=16, style=filled, fillcolor=lightyellow];
27 [label="27: search_tree(void, X6, X7), SCOPE: 2, CLAUSE: 5\n\nX6 is free\nX7 is free", fontsize=16, style=filled, fillcolor=lightyellow];
29 [label="29: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
31 [label="31: search_tree(T3, X22, X23)\n\nT3 is ground\nX22 is free\nX23 is free\nsearch_tree(T3) !=? search_tree(void)", fontsize=16, style=filled, fillcolor=lightyellow];
33 [label="33: search_tree(T3, X22, X23), SCOPE: 3, CLAUSE: 2 | search_tree(T3, X22, X23), SCOPE: 3, CLAUSE: 3 | search_tree(T3, X22, X23), SCOPE: 3, CLAUSE: 4 | search_tree(T3, X22, X23), SCOPE: 3, CLAUSE: 5\n\nT3 is ground\nX22 is free\nX23 is free\nsearch_tree(T3) !=? search_tree(void)", fontsize=16, style=filled, fillcolor=lightyellow];
35 [label="35: search_tree(T3, X22, X23), SCOPE: 3, CLAUSE: 2\n\nT3 is ground\nX22 is free\nX23 is free\nsearch_tree(T3) !=? search_tree(void)", fontsize=16, style=filled, fillcolor=lightyellow];
37 [label="37: search_tree(T3, X22, X23), SCOPE: 3, CLAUSE: 3 | search_tree(T3, X22, X23), SCOPE: 3, CLAUSE: 4 | search_tree(T3, X22, X23), SCOPE: 3, CLAUSE: 5\n\nT3 is ground\nX22 is free\nX23 is free\nsearch_tree(T3) !=? search_tree(void)", fontsize=16, style=filled, fillcolor=lightyellow];
40 [label="40: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
43 [label="43: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
44 [label="44: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
50 [label="50: search_tree(T3, X22, X23), SCOPE: 3, CLAUSE: 3\n\nT3 is ground\nX22 is free\nX23 is free\nsearch_tree(T3) !=? search_tree(void)", fontsize=16, style=filled, fillcolor=lightyellow];
52 [label="52: search_tree(T3, X22, X23), SCOPE: 3, CLAUSE: 4 | search_tree(T3, X22, X23), SCOPE: 3, CLAUSE: 5\n\nT3 is ground\nX22 is free\nX23 is free\nsearch_tree(T3) !=? search_tree(void)", fontsize=16, style=filled, fillcolor=lightyellow];
55 [label="B: ','(search_tree(T18, X50, X51), less(T17, X50))\n\nT17 is ground\nT18 is ground\nX51 is free\nX50 is free", fontsize=16, style=filled, fillcolor=lightyellow];
58 [label="58: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
60 [label="E: search_tree(T18, X50, X51)\n\nT18 is ground\nX51 is free\nX50 is free", fontsize=16, style=filled, fillcolor=lightyellow];
61 [label="F: less(T17, T21)\n\nT17 is ground\nT21 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
65 [label="65: search_tree(T18, X50, X51), SCOPE: 4, CLAUSE: 2 | search_tree(T18, X50, X51), SCOPE: 4, CLAUSE: 3 | search_tree(T18, X50, X51), SCOPE: 4, CLAUSE: 4 | search_tree(T18, X50, X51), SCOPE: 4, CLAUSE: 5\n\nT18 is ground\nX51 is free\nX50 is free", fontsize=16, style=filled, fillcolor=lightyellow];
69 [label="69: search_tree(T18, X50, X51), SCOPE: 4, CLAUSE: 2\n\nT18 is ground\nX51 is free\nX50 is free", fontsize=16, style=filled, fillcolor=lightyellow];
70 [label="70: search_tree(T18, X50, X51), SCOPE: 4, CLAUSE: 3 | search_tree(T18, X50, X51), SCOPE: 4, CLAUSE: 4 | search_tree(T18, X50, X51), SCOPE: 4, CLAUSE: 5\n\nT18 is ground\nX51 is free\nX50 is free", fontsize=16, style=filled, fillcolor=lightyellow];
72 [label="72: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
73 [label="73: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
74 [label="74: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
78 [label="78: search_tree(T18, X50, X51), SCOPE: 4, CLAUSE: 3\n\nT18 is ground\nX51 is free\nX50 is free", fontsize=16, style=filled, fillcolor=lightyellow];
79 [label="79: search_tree(T18, X50, X51), SCOPE: 4, CLAUSE: 4 | search_tree(T18, X50, X51), SCOPE: 4, CLAUSE: 5\n\nT18 is ground\nX51 is free\nX50 is free", fontsize=16, style=filled, fillcolor=lightyellow];
89 [label="89: ','(search_tree(T39, X82, X83), less(T38, X82))\n\nT38 is ground\nT39 is ground\nX83 is free\nX82 is free", fontsize=16, style=filled, fillcolor=lightyellow];
91 [label="91: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
95 [label="95: search_tree(T18, X50, X51), SCOPE: 4, CLAUSE: 4\n\nT18 is ground\nX51 is free\nX50 is free", fontsize=16, style=filled, fillcolor=lightyellow];
96 [label="96: search_tree(T18, X50, X51), SCOPE: 4, CLAUSE: 5\n\nT18 is ground\nX51 is free\nX50 is free", fontsize=16, style=filled, fillcolor=lightyellow];
101 [label="C: ','(search_tree(T51, X108, X107), less(X107, T50))\n\nT50 is ground\nT51 is ground\nX108 is free\nX107 is free", fontsize=16, style=filled, fillcolor=lightyellow];
102 [label="102: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
105 [label="105: search_tree(T51, X108, X107)\n\nT51 is ground\nX108 is free\nX107 is free", fontsize=16, style=filled, fillcolor=lightyellow];
106 [label="106: less(T55, T50)\n\nT50 is ground\nT55 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
111 [label="D: ','(search_tree(T67, X138, X136), ','(less(X136, T66), ','(search_tree(T68, X137, X139), less(T66, X137))))\n\nT66 is ground\nT67 is ground\nT68 is ground\nX138 is free\nX139 is free\nX136 is free\nX137 is free", fontsize=16, style=filled, fillcolor=lightyellow];
112 [label="112: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
118 [label="118: search_tree(T67, X138, X136)\n\nT67 is ground\nX138 is free\nX136 is free", fontsize=16, style=filled, fillcolor=lightyellow];
119 [label="G: ','(less(T72, T66), ','(search_tree(T68, X137, X139), less(T66, X137)))\n\nT66 is ground\nT68 is ground\nT72 is ground\nX139 is free\nX137 is free", fontsize=16, style=filled, fillcolor=lightyellow];
125 [label="125: less(T72, T66)\n\nT66 is ground\nT72 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
126 [label="126: ','(search_tree(T68, X137, X139), less(T66, X137))\n\nT66 is ground\nT68 is ground\nX139 is free\nX137 is free", fontsize=16, style=filled, fillcolor=lightyellow];
127 [label="127: less(T17, T21), SCOPE: 5, CLAUSE: 6 | less(T17, T21), SCOPE: 5, CLAUSE: 7\n\nT17 is ground\nT21 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
128 [label="128: less(T17, T21), SCOPE: 5, CLAUSE: 6\n\nT17 is ground\nT21 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
129 [label="129: less(T17, T21), SCOPE: 5, CLAUSE: 7\n\nT17 is ground\nT21 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
131 [label="131: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
133 [label="133: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
134 [label="134: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
135 [label="135: less(T92, T93)\n\nT92 is ground\nT93 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
136 [label="136: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
139 [label="139: search_tree(T3, X22, X23), SCOPE: 3, CLAUSE: 4\n\nT3 is ground\nX22 is free\nX23 is free\nsearch_tree(T3) !=? search_tree(void)", fontsize=16, style=filled, fillcolor=lightyellow];
140 [label="140: search_tree(T3, X22, X23), SCOPE: 3, CLAUSE: 5\n\nT3 is ground\nX22 is free\nX23 is free\nsearch_tree(T3) !=? search_tree(void)", fontsize=16, style=filled, fillcolor=lightyellow];
143 [label="143: ','(search_tree(T105, X187, X186), less(X186, T104))\n\nT104 is ground\nT105 is ground\nX187 is free\nX186 is free", fontsize=16, style=filled, fillcolor=lightyellow];
144 [label="144: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
145 [label="145: ','(search_tree(T115, X213, X211), ','(less(X211, T114), ','(search_tree(T116, X212, X214), less(T114, X212))))\n\nT114 is ground\nT115 is ground\nT116 is ground\nX213 is free\nX214 is free\nX211 is free\nX212 is free", fontsize=16, style=filled, fillcolor=lightyellow];
146 [label="146: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
147 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
1 -> 147 [arrowhead = none ];
147 -> 5;

148 [label="EVAL with clause\nsearch_tree(void).\nand substitutionT1 -> void", fontsize=14, style = filled, fillcolor = lightblue];
5 -> 148 [arrowhead = none ];
148 -> 9;

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

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

151 [label="ONLY EVAL with clause\nsearch_tree(X21) :- search_tree(X21, X22, X23).\nand substitutionT1 -> T3,\nX21 -> T3", fontsize=14, style = filled, fillcolor = lightblue];
11 -> 151 [arrowhead = none ];
151 -> 31;

152 [label="ONLY EVAL with clause\nsearch_tree(X5) :- search_tree(X5, X6, X7).\nand substitutionX5 -> void", fontsize=14, style = filled, fillcolor = lightblue];
16 -> 152 [arrowhead = none ];
152 -> 18;

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

154 [label="BACKTRACK\nfor clause: search_tree(tree(X, void, void), X, X)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
20 -> 154 [arrowhead = none ];
154 -> 23;

155 [label="BACKTRACK\nfor clause: search_tree(tree(X, void, Right), X, Max) :- ','(search_tree(Right, Min, Max), less(X, Min))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
23 -> 155 [arrowhead = none ];
155 -> 25;

156 [label="BACKTRACK\nfor clause: search_tree(tree(X, Left, void), Min, X) :- ','(search_tree(Left, Min, Max), less(Max, X))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
25 -> 156 [arrowhead = none ];
156 -> 27;

157 [label="BACKTRACK\nfor clause: search_tree(tree(X, Left, Right), Min1, Max2) :- ','(search_tree(Left, Min1, Max1), ','(less(Max1, X), ','(search_tree(Right, Min2, Max2), less(X, Min2))))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
27 -> 157 [arrowhead = none ];
157 -> 29;

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

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

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

161 [label="EVAL with clause\nsearch_tree(tree(X28, void, void), X28, X28).\nand substitutionX28 -> T8,\nT3 -> tree(T8, void, void),\nX22 -> T8,\nX23 -> T8", fontsize=14, style = filled, fillcolor = lightblue];
35 -> 161 [arrowhead = none ];
161 -> 40;

162 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
35 -> 162 [arrowhead = none ];
162 -> 43;

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

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

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

166 [label="EVAL with clause\nsearch_tree(tree(X47, void, X48), X47, X49) :- ','(search_tree(X48, X50, X49), less(X47, X50)).\nand substitutionX47 -> T17,\nX48 -> T18,\nT3 -> tree(T17, void, T18),\nX22 -> T17,\nX23 -> X51,\nX49 -> X51", fontsize=14, style = filled, fillcolor = lightblue];
50 -> 166 [arrowhead = none ];
166 -> 55;

167 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
50 -> 167 [arrowhead = none ];
167 -> 58;

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

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

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

171 [label="SPLIT 2\nnew knowledge:\nT18 is ground\nT21 is ground\nT22 is ground\nreplacements:X50 -> T21,\nX51 -> T22", fontsize=14, style = filled, fillcolor = violet];
55 -> 171 [arrowhead = none ];
171 -> 61;

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

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

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

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

176 [label="EVAL with clause\nsearch_tree(tree(X60, void, void), X60, X60).\nand substitutionX60 -> T29,\nT18 -> tree(T29, void, void),\nX50 -> T29,\nX51 -> T29", fontsize=14, style = filled, fillcolor = lightblue];
69 -> 176 [arrowhead = none ];
176 -> 72;

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

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

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

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

181 [label="EVAL with clause\nsearch_tree(tree(X79, void, X80), X79, X81) :- ','(search_tree(X80, X82, X81), less(X79, X82)).\nand substitutionX79 -> T38,\nX80 -> T39,\nT18 -> tree(T38, void, T39),\nX50 -> T38,\nX51 -> X83,\nX81 -> X83", fontsize=14, style = filled, fillcolor = lightblue];
78 -> 181 [arrowhead = none ];
181 -> 89;

182 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
78 -> 182 [arrowhead = none ];
182 -> 91;

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

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

185 [label="INSTANCE with matching:\nT18 -> T39\nX50 -> X82\nX51 -> X83\nT17 -> T38", fontsize=14, style = filled, fillcolor = lightgrey];
89 -> 185 [arrowhead = none , style=dashed];
185 -> 55[style=dashed];

186 [label="EVAL with clause\nsearch_tree(tree(X104, X105, void), X106, X104) :- ','(search_tree(X105, X106, X107), less(X107, X104)).\nand substitutionX104 -> T50,\nX105 -> T51,\nT18 -> tree(T50, T51, void),\nX50 -> X108,\nX106 -> X108,\nX51 -> T50", fontsize=14, style = filled, fillcolor = lightblue];
95 -> 186 [arrowhead = none ];
186 -> 101;

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

188 [label="EVAL with clause\nsearch_tree(tree(X131, X132, X133), X134, X135) :- ','(search_tree(X132, X134, X136), ','(less(X136, X131), ','(search_tree(X133, X137, X135), less(X131, X137)))).\nand substitutionX131 -> T66,\nX132 -> T67,\nX133 -> T68,\nT18 -> tree(T66, T67, T68),\nX50 -> X138,\nX134 -> X138,\nX51 -> X139,\nX135 -> X139", fontsize=14, style = filled, fillcolor = lightblue];
96 -> 188 [arrowhead = none ];
188 -> 111;

189 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
96 -> 189 [arrowhead = none ];
189 -> 112;

190 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
101 -> 190 [arrowhead = none ];
190 -> 105;

191 [label="SPLIT 2\nnew knowledge:\nT51 is ground\nT54 is ground\nT55 is ground\nreplacements:X108 -> T54,\nX107 -> T55", fontsize=14, style = filled, fillcolor = violet];
101 -> 191 [arrowhead = none ];
191 -> 106;

192 [label="INSTANCE with matching:\nT18 -> T51\nX50 -> X108\nX51 -> X107", fontsize=14, style = filled, fillcolor = lightgrey];
105 -> 192 [arrowhead = none , style=dashed];
192 -> 60[style=dashed];

193 [label="INSTANCE with matching:\nT17 -> T55\nT21 -> T50", fontsize=14, style = filled, fillcolor = lightgrey];
106 -> 193 [arrowhead = none , style=dashed];
193 -> 61[style=dashed];

194 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
111 -> 194 [arrowhead = none ];
194 -> 118;

195 [label="SPLIT 2\nnew knowledge:\nT67 is ground\nT71 is ground\nT72 is ground\nreplacements:X138 -> T71,\nX136 -> T72", fontsize=14, style = filled, fillcolor = violet];
111 -> 195 [arrowhead = none ];
195 -> 119;

196 [label="INSTANCE with matching:\nT18 -> T67\nX50 -> X138\nX51 -> X136", fontsize=14, style = filled, fillcolor = lightgrey];
118 -> 196 [arrowhead = none , style=dashed];
196 -> 60[style=dashed];

197 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
119 -> 197 [arrowhead = none ];
197 -> 125;

198 [label="SPLIT 2\nnew knowledge:\nT72 is ground\nT66 is ground", fontsize=14, style = filled, fillcolor = violet];
119 -> 198 [arrowhead = none ];
198 -> 126;

199 [label="INSTANCE with matching:\nT17 -> T72\nT21 -> T66", fontsize=14, style = filled, fillcolor = lightgrey];
125 -> 199 [arrowhead = none , style=dashed];
199 -> 61[style=dashed];

200 [label="INSTANCE with matching:\nT18 -> T68\nX50 -> X137\nX51 -> X139\nT17 -> T66", fontsize=14, style = filled, fillcolor = lightgrey];
126 -> 200 [arrowhead = none , style=dashed];
200 -> 55[style=dashed];

201 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
127 -> 201 [arrowhead = none ];
201 -> 128;

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

203 [label="EVAL with clause\nless(0, s(X156)).\nand substitutionT17 -> 0,\nX156 -> T87,\nT21 -> s(T87)", fontsize=14, style = filled, fillcolor = lightblue];
128 -> 203 [arrowhead = none ];
203 -> 131;

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

205 [label="EVAL with clause\nless(s(X161), s(X162)) :- less(X161, X162).\nand substitutionX161 -> T92,\nT17 -> s(T92),\nX162 -> T93,\nT21 -> s(T93)", fontsize=14, style = filled, fillcolor = lightblue];
129 -> 205 [arrowhead = none ];
205 -> 135;

206 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
129 -> 206 [arrowhead = none ];
206 -> 136;

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

208 [label="INSTANCE with matching:\nT17 -> T92\nT21 -> T93", fontsize=14, style = filled, fillcolor = lightgrey];
135 -> 208 [arrowhead = none , style=dashed];
208 -> 61[style=dashed];

209 [label="EVAL with clause\nsearch_tree(tree(X183, X184, void), X185, X183) :- ','(search_tree(X184, X185, X186), less(X186, X183)).\nand substitutionX183 -> T104,\nX184 -> T105,\nT3 -> tree(T104, T105, void),\nX22 -> X187,\nX185 -> X187,\nX23 -> T104", fontsize=14, style = filled, fillcolor = lightblue];
139 -> 209 [arrowhead = none ];
209 -> 143;

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

211 [label="EVAL with clause\nsearch_tree(tree(X206, X207, X208), X209, X210) :- ','(search_tree(X207, X209, X211), ','(less(X211, X206), ','(search_tree(X208, X212, X210), less(X206, X212)))).\nand substitutionX206 -> T114,\nX207 -> T115,\nX208 -> T116,\nT3 -> tree(T114, T115, T116),\nX22 -> X213,\nX209 -> X213,\nX23 -> X214,\nX210 -> X214", fontsize=14, style = filled, fillcolor = lightblue];
140 -> 211 [arrowhead = none ];
211 -> 145;

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

213 [label="INSTANCE with matching:\nT51 -> T105\nX108 -> X187\nX107 -> X186\nT50 -> T104", fontsize=14, style = filled, fillcolor = lightgrey];
143 -> 213 [arrowhead = none , style=dashed];
213 -> 101[style=dashed];

214 [label="INSTANCE with matching:\nT67 -> T115\nX138 -> X213\nX136 -> X211\nT66 -> T114\nT68 -> T116\nX137 -> X212\nX139 -> X214", fontsize=14, style = filled, fillcolor = lightgrey];
145 -> 214 [arrowhead = none , style=dashed];
214 -> 111[style=dashed];

}

(2) Obligation:

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

search_treeA_in_g(void) → search_treeA_out_g(void)
search_treeA_in_g(tree(T8, void, void)) → search_treeA_out_g(tree(T8, void, void))
search_treeA_in_g(tree(T17, void, T18)) → U1_g(T17, T18, pB_in_gaag(T18, X50, X51, T17))
pB_in_gaag(T18, T21, T22, T17) → U8_gaag(T18, T21, T22, T17, search_treeE_in_gaa(T18, T21, T22))
search_treeE_in_gaa(tree(T29, void, void), T29, T29) → search_treeE_out_gaa(tree(T29, void, void), T29, T29)
search_treeE_in_gaa(tree(T38, void, T39), T38, X83) → U4_gaa(T38, T39, X83, pB_in_gaag(T39, X82, X83, T38))
U4_gaa(T38, T39, X83, pB_out_gaag(T39, X82, X83, T38)) → search_treeE_out_gaa(tree(T38, void, T39), T38, X83)
search_treeE_in_gaa(tree(T50, T51, void), X108, T50) → U5_gaa(T50, T51, X108, pC_in_gaag(T51, X108, X107, T50))
pC_in_gaag(T51, T54, T55, T50) → U10_gaag(T51, T54, T55, T50, search_treeE_in_gaa(T51, T54, T55))
search_treeE_in_gaa(tree(T66, T67, T68), X138, X139) → U6_gaa(T66, T67, T68, X138, X139, pD_in_gaaggaa(T67, X138, X136, T66, T68, X137, X139))
pD_in_gaaggaa(T67, T71, T72, T66, T68, X137, X139) → U12_gaaggaa(T67, T71, T72, T66, T68, X137, X139, search_treeE_in_gaa(T67, T71, T72))
U12_gaaggaa(T67, T71, T72, T66, T68, X137, X139, search_treeE_out_gaa(T67, T71, T72)) → U13_gaaggaa(T67, T71, T72, T66, T68, X137, X139, pG_in_gggaa(T72, T66, T68, X137, X139))
pG_in_gggaa(T72, T66, T68, X137, X139) → U14_gggaa(T72, T66, T68, X137, X139, lessF_in_gg(T72, T66))
lessF_in_gg(0, s(T87)) → lessF_out_gg(0, s(T87))
lessF_in_gg(s(T92), s(T93)) → U7_gg(T92, T93, lessF_in_gg(T92, T93))
U7_gg(T92, T93, lessF_out_gg(T92, T93)) → lessF_out_gg(s(T92), s(T93))
U14_gggaa(T72, T66, T68, X137, X139, lessF_out_gg(T72, T66)) → U15_gggaa(T72, T66, T68, X137, X139, pB_in_gaag(T68, X137, X139, T66))
U15_gggaa(T72, T66, T68, X137, X139, pB_out_gaag(T68, X137, X139, T66)) → pG_out_gggaa(T72, T66, T68, X137, X139)
U13_gaaggaa(T67, T71, T72, T66, T68, X137, X139, pG_out_gggaa(T72, T66, T68, X137, X139)) → pD_out_gaaggaa(T67, T71, T72, T66, T68, X137, X139)
U6_gaa(T66, T67, T68, X138, X139, pD_out_gaaggaa(T67, X138, X136, T66, T68, X137, X139)) → search_treeE_out_gaa(tree(T66, T67, T68), X138, X139)
U10_gaag(T51, T54, T55, T50, search_treeE_out_gaa(T51, T54, T55)) → U11_gaag(T51, T54, T55, T50, lessF_in_gg(T55, T50))
U11_gaag(T51, T54, T55, T50, lessF_out_gg(T55, T50)) → pC_out_gaag(T51, T54, T55, T50)
U5_gaa(T50, T51, X108, pC_out_gaag(T51, X108, X107, T50)) → search_treeE_out_gaa(tree(T50, T51, void), X108, T50)
U8_gaag(T18, T21, T22, T17, search_treeE_out_gaa(T18, T21, T22)) → U9_gaag(T18, T21, T22, T17, lessF_in_gg(T17, T21))
U9_gaag(T18, T21, T22, T17, lessF_out_gg(T17, T21)) → pB_out_gaag(T18, T21, T22, T17)
U1_g(T17, T18, pB_out_gaag(T18, X50, X51, T17)) → search_treeA_out_g(tree(T17, void, T18))
search_treeA_in_g(tree(T104, T105, void)) → U2_g(T104, T105, pC_in_gaag(T105, X187, X186, T104))
U2_g(T104, T105, pC_out_gaag(T105, X187, X186, T104)) → search_treeA_out_g(tree(T104, T105, void))
search_treeA_in_g(tree(T114, T115, T116)) → U3_g(T114, T115, T116, pD_in_gaaggaa(T115, X213, X211, T114, T116, X212, X214))
U3_g(T114, T115, T116, pD_out_gaaggaa(T115, X213, X211, T114, T116, X212, X214)) → search_treeA_out_g(tree(T114, T115, T116))

The argument filtering Pi contains the following mapping:
search_treeA_in_g(x1)  =  search_treeA_in_g(x1)
void  =  void
search_treeA_out_g(x1)  =  search_treeA_out_g(x1)
tree(x1, x2, x3)  =  tree(x1, x2, x3)
U1_g(x1, x2, x3)  =  U1_g(x1, x2, x3)
pB_in_gaag(x1, x2, x3, x4)  =  pB_in_gaag(x1, x4)
U8_gaag(x1, x2, x3, x4, x5)  =  U8_gaag(x1, x4, x5)
search_treeE_in_gaa(x1, x2, x3)  =  search_treeE_in_gaa(x1)
search_treeE_out_gaa(x1, x2, x3)  =  search_treeE_out_gaa(x1, x2, x3)
U4_gaa(x1, x2, x3, x4)  =  U4_gaa(x1, x2, x4)
pB_out_gaag(x1, x2, x3, x4)  =  pB_out_gaag(x1, x2, x3, x4)
U5_gaa(x1, x2, x3, x4)  =  U5_gaa(x1, x2, x4)
pC_in_gaag(x1, x2, x3, x4)  =  pC_in_gaag(x1, x4)
U10_gaag(x1, x2, x3, x4, x5)  =  U10_gaag(x1, x4, x5)
U6_gaa(x1, x2, x3, x4, x5, x6)  =  U6_gaa(x1, x2, x3, x6)
pD_in_gaaggaa(x1, x2, x3, x4, x5, x6, x7)  =  pD_in_gaaggaa(x1, x4, x5)
U12_gaaggaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  U12_gaaggaa(x1, x4, x5, x8)
U13_gaaggaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  U13_gaaggaa(x1, x2, x3, x4, x5, x8)
pG_in_gggaa(x1, x2, x3, x4, x5)  =  pG_in_gggaa(x1, x2, x3)
U14_gggaa(x1, x2, x3, x4, x5, x6)  =  U14_gggaa(x1, x2, x3, x6)
lessF_in_gg(x1, x2)  =  lessF_in_gg(x1, x2)
0  =  0
s(x1)  =  s(x1)
lessF_out_gg(x1, x2)  =  lessF_out_gg(x1, x2)
U7_gg(x1, x2, x3)  =  U7_gg(x1, x2, x3)
U15_gggaa(x1, x2, x3, x4, x5, x6)  =  U15_gggaa(x1, x2, x3, x6)
pG_out_gggaa(x1, x2, x3, x4, x5)  =  pG_out_gggaa(x1, x2, x3, x4, x5)
pD_out_gaaggaa(x1, x2, x3, x4, x5, x6, x7)  =  pD_out_gaaggaa(x1, x2, x3, x4, x5, x6, x7)
U11_gaag(x1, x2, x3, x4, x5)  =  U11_gaag(x1, x2, x3, x4, x5)
pC_out_gaag(x1, x2, x3, x4)  =  pC_out_gaag(x1, x2, x3, x4)
U9_gaag(x1, x2, x3, x4, x5)  =  U9_gaag(x1, x2, x3, x4, x5)
U2_g(x1, x2, x3)  =  U2_g(x1, x2, x3)
U3_g(x1, x2, x3, x4)  =  U3_g(x1, x2, x3, x4)

(3) DependencyPairsProof (EQUIVALENT transformation)

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

SEARCH_TREEA_IN_G(tree(T17, void, T18)) → U1_G(T17, T18, pB_in_gaag(T18, X50, X51, T17))
SEARCH_TREEA_IN_G(tree(T17, void, T18)) → PB_IN_GAAG(T18, X50, X51, T17)
PB_IN_GAAG(T18, T21, T22, T17) → U8_GAAG(T18, T21, T22, T17, search_treeE_in_gaa(T18, T21, T22))
PB_IN_GAAG(T18, T21, T22, T17) → SEARCH_TREEE_IN_GAA(T18, T21, T22)
SEARCH_TREEE_IN_GAA(tree(T38, void, T39), T38, X83) → U4_GAA(T38, T39, X83, pB_in_gaag(T39, X82, X83, T38))
SEARCH_TREEE_IN_GAA(tree(T38, void, T39), T38, X83) → PB_IN_GAAG(T39, X82, X83, T38)
SEARCH_TREEE_IN_GAA(tree(T50, T51, void), X108, T50) → U5_GAA(T50, T51, X108, pC_in_gaag(T51, X108, X107, T50))
SEARCH_TREEE_IN_GAA(tree(T50, T51, void), X108, T50) → PC_IN_GAAG(T51, X108, X107, T50)
PC_IN_GAAG(T51, T54, T55, T50) → U10_GAAG(T51, T54, T55, T50, search_treeE_in_gaa(T51, T54, T55))
PC_IN_GAAG(T51, T54, T55, T50) → SEARCH_TREEE_IN_GAA(T51, T54, T55)
SEARCH_TREEE_IN_GAA(tree(T66, T67, T68), X138, X139) → U6_GAA(T66, T67, T68, X138, X139, pD_in_gaaggaa(T67, X138, X136, T66, T68, X137, X139))
SEARCH_TREEE_IN_GAA(tree(T66, T67, T68), X138, X139) → PD_IN_GAAGGAA(T67, X138, X136, T66, T68, X137, X139)
PD_IN_GAAGGAA(T67, T71, T72, T66, T68, X137, X139) → U12_GAAGGAA(T67, T71, T72, T66, T68, X137, X139, search_treeE_in_gaa(T67, T71, T72))
PD_IN_GAAGGAA(T67, T71, T72, T66, T68, X137, X139) → SEARCH_TREEE_IN_GAA(T67, T71, T72)
U12_GAAGGAA(T67, T71, T72, T66, T68, X137, X139, search_treeE_out_gaa(T67, T71, T72)) → U13_GAAGGAA(T67, T71, T72, T66, T68, X137, X139, pG_in_gggaa(T72, T66, T68, X137, X139))
U12_GAAGGAA(T67, T71, T72, T66, T68, X137, X139, search_treeE_out_gaa(T67, T71, T72)) → PG_IN_GGGAA(T72, T66, T68, X137, X139)
PG_IN_GGGAA(T72, T66, T68, X137, X139) → U14_GGGAA(T72, T66, T68, X137, X139, lessF_in_gg(T72, T66))
PG_IN_GGGAA(T72, T66, T68, X137, X139) → LESSF_IN_GG(T72, T66)
LESSF_IN_GG(s(T92), s(T93)) → U7_GG(T92, T93, lessF_in_gg(T92, T93))
LESSF_IN_GG(s(T92), s(T93)) → LESSF_IN_GG(T92, T93)
U14_GGGAA(T72, T66, T68, X137, X139, lessF_out_gg(T72, T66)) → U15_GGGAA(T72, T66, T68, X137, X139, pB_in_gaag(T68, X137, X139, T66))
U14_GGGAA(T72, T66, T68, X137, X139, lessF_out_gg(T72, T66)) → PB_IN_GAAG(T68, X137, X139, T66)
U10_GAAG(T51, T54, T55, T50, search_treeE_out_gaa(T51, T54, T55)) → U11_GAAG(T51, T54, T55, T50, lessF_in_gg(T55, T50))
U10_GAAG(T51, T54, T55, T50, search_treeE_out_gaa(T51, T54, T55)) → LESSF_IN_GG(T55, T50)
U8_GAAG(T18, T21, T22, T17, search_treeE_out_gaa(T18, T21, T22)) → U9_GAAG(T18, T21, T22, T17, lessF_in_gg(T17, T21))
U8_GAAG(T18, T21, T22, T17, search_treeE_out_gaa(T18, T21, T22)) → LESSF_IN_GG(T17, T21)
SEARCH_TREEA_IN_G(tree(T104, T105, void)) → U2_G(T104, T105, pC_in_gaag(T105, X187, X186, T104))
SEARCH_TREEA_IN_G(tree(T104, T105, void)) → PC_IN_GAAG(T105, X187, X186, T104)
SEARCH_TREEA_IN_G(tree(T114, T115, T116)) → U3_G(T114, T115, T116, pD_in_gaaggaa(T115, X213, X211, T114, T116, X212, X214))
SEARCH_TREEA_IN_G(tree(T114, T115, T116)) → PD_IN_GAAGGAA(T115, X213, X211, T114, T116, X212, X214)

The TRS R consists of the following rules:

search_treeA_in_g(void) → search_treeA_out_g(void)
search_treeA_in_g(tree(T8, void, void)) → search_treeA_out_g(tree(T8, void, void))
search_treeA_in_g(tree(T17, void, T18)) → U1_g(T17, T18, pB_in_gaag(T18, X50, X51, T17))
pB_in_gaag(T18, T21, T22, T17) → U8_gaag(T18, T21, T22, T17, search_treeE_in_gaa(T18, T21, T22))
search_treeE_in_gaa(tree(T29, void, void), T29, T29) → search_treeE_out_gaa(tree(T29, void, void), T29, T29)
search_treeE_in_gaa(tree(T38, void, T39), T38, X83) → U4_gaa(T38, T39, X83, pB_in_gaag(T39, X82, X83, T38))
U4_gaa(T38, T39, X83, pB_out_gaag(T39, X82, X83, T38)) → search_treeE_out_gaa(tree(T38, void, T39), T38, X83)
search_treeE_in_gaa(tree(T50, T51, void), X108, T50) → U5_gaa(T50, T51, X108, pC_in_gaag(T51, X108, X107, T50))
pC_in_gaag(T51, T54, T55, T50) → U10_gaag(T51, T54, T55, T50, search_treeE_in_gaa(T51, T54, T55))
search_treeE_in_gaa(tree(T66, T67, T68), X138, X139) → U6_gaa(T66, T67, T68, X138, X139, pD_in_gaaggaa(T67, X138, X136, T66, T68, X137, X139))
pD_in_gaaggaa(T67, T71, T72, T66, T68, X137, X139) → U12_gaaggaa(T67, T71, T72, T66, T68, X137, X139, search_treeE_in_gaa(T67, T71, T72))
U12_gaaggaa(T67, T71, T72, T66, T68, X137, X139, search_treeE_out_gaa(T67, T71, T72)) → U13_gaaggaa(T67, T71, T72, T66, T68, X137, X139, pG_in_gggaa(T72, T66, T68, X137, X139))
pG_in_gggaa(T72, T66, T68, X137, X139) → U14_gggaa(T72, T66, T68, X137, X139, lessF_in_gg(T72, T66))
lessF_in_gg(0, s(T87)) → lessF_out_gg(0, s(T87))
lessF_in_gg(s(T92), s(T93)) → U7_gg(T92, T93, lessF_in_gg(T92, T93))
U7_gg(T92, T93, lessF_out_gg(T92, T93)) → lessF_out_gg(s(T92), s(T93))
U14_gggaa(T72, T66, T68, X137, X139, lessF_out_gg(T72, T66)) → U15_gggaa(T72, T66, T68, X137, X139, pB_in_gaag(T68, X137, X139, T66))
U15_gggaa(T72, T66, T68, X137, X139, pB_out_gaag(T68, X137, X139, T66)) → pG_out_gggaa(T72, T66, T68, X137, X139)
U13_gaaggaa(T67, T71, T72, T66, T68, X137, X139, pG_out_gggaa(T72, T66, T68, X137, X139)) → pD_out_gaaggaa(T67, T71, T72, T66, T68, X137, X139)
U6_gaa(T66, T67, T68, X138, X139, pD_out_gaaggaa(T67, X138, X136, T66, T68, X137, X139)) → search_treeE_out_gaa(tree(T66, T67, T68), X138, X139)
U10_gaag(T51, T54, T55, T50, search_treeE_out_gaa(T51, T54, T55)) → U11_gaag(T51, T54, T55, T50, lessF_in_gg(T55, T50))
U11_gaag(T51, T54, T55, T50, lessF_out_gg(T55, T50)) → pC_out_gaag(T51, T54, T55, T50)
U5_gaa(T50, T51, X108, pC_out_gaag(T51, X108, X107, T50)) → search_treeE_out_gaa(tree(T50, T51, void), X108, T50)
U8_gaag(T18, T21, T22, T17, search_treeE_out_gaa(T18, T21, T22)) → U9_gaag(T18, T21, T22, T17, lessF_in_gg(T17, T21))
U9_gaag(T18, T21, T22, T17, lessF_out_gg(T17, T21)) → pB_out_gaag(T18, T21, T22, T17)
U1_g(T17, T18, pB_out_gaag(T18, X50, X51, T17)) → search_treeA_out_g(tree(T17, void, T18))
search_treeA_in_g(tree(T104, T105, void)) → U2_g(T104, T105, pC_in_gaag(T105, X187, X186, T104))
U2_g(T104, T105, pC_out_gaag(T105, X187, X186, T104)) → search_treeA_out_g(tree(T104, T105, void))
search_treeA_in_g(tree(T114, T115, T116)) → U3_g(T114, T115, T116, pD_in_gaaggaa(T115, X213, X211, T114, T116, X212, X214))
U3_g(T114, T115, T116, pD_out_gaaggaa(T115, X213, X211, T114, T116, X212, X214)) → search_treeA_out_g(tree(T114, T115, T116))

The argument filtering Pi contains the following mapping:
search_treeA_in_g(x1)  =  search_treeA_in_g(x1)
void  =  void
search_treeA_out_g(x1)  =  search_treeA_out_g(x1)
tree(x1, x2, x3)  =  tree(x1, x2, x3)
U1_g(x1, x2, x3)  =  U1_g(x1, x2, x3)
pB_in_gaag(x1, x2, x3, x4)  =  pB_in_gaag(x1, x4)
U8_gaag(x1, x2, x3, x4, x5)  =  U8_gaag(x1, x4, x5)
search_treeE_in_gaa(x1, x2, x3)  =  search_treeE_in_gaa(x1)
search_treeE_out_gaa(x1, x2, x3)  =  search_treeE_out_gaa(x1, x2, x3)
U4_gaa(x1, x2, x3, x4)  =  U4_gaa(x1, x2, x4)
pB_out_gaag(x1, x2, x3, x4)  =  pB_out_gaag(x1, x2, x3, x4)
U5_gaa(x1, x2, x3, x4)  =  U5_gaa(x1, x2, x4)
pC_in_gaag(x1, x2, x3, x4)  =  pC_in_gaag(x1, x4)
U10_gaag(x1, x2, x3, x4, x5)  =  U10_gaag(x1, x4, x5)
U6_gaa(x1, x2, x3, x4, x5, x6)  =  U6_gaa(x1, x2, x3, x6)
pD_in_gaaggaa(x1, x2, x3, x4, x5, x6, x7)  =  pD_in_gaaggaa(x1, x4, x5)
U12_gaaggaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  U12_gaaggaa(x1, x4, x5, x8)
U13_gaaggaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  U13_gaaggaa(x1, x2, x3, x4, x5, x8)
pG_in_gggaa(x1, x2, x3, x4, x5)  =  pG_in_gggaa(x1, x2, x3)
U14_gggaa(x1, x2, x3, x4, x5, x6)  =  U14_gggaa(x1, x2, x3, x6)
lessF_in_gg(x1, x2)  =  lessF_in_gg(x1, x2)
0  =  0
s(x1)  =  s(x1)
lessF_out_gg(x1, x2)  =  lessF_out_gg(x1, x2)
U7_gg(x1, x2, x3)  =  U7_gg(x1, x2, x3)
U15_gggaa(x1, x2, x3, x4, x5, x6)  =  U15_gggaa(x1, x2, x3, x6)
pG_out_gggaa(x1, x2, x3, x4, x5)  =  pG_out_gggaa(x1, x2, x3, x4, x5)
pD_out_gaaggaa(x1, x2, x3, x4, x5, x6, x7)  =  pD_out_gaaggaa(x1, x2, x3, x4, x5, x6, x7)
U11_gaag(x1, x2, x3, x4, x5)  =  U11_gaag(x1, x2, x3, x4, x5)
pC_out_gaag(x1, x2, x3, x4)  =  pC_out_gaag(x1, x2, x3, x4)
U9_gaag(x1, x2, x3, x4, x5)  =  U9_gaag(x1, x2, x3, x4, x5)
U2_g(x1, x2, x3)  =  U2_g(x1, x2, x3)
U3_g(x1, x2, x3, x4)  =  U3_g(x1, x2, x3, x4)
SEARCH_TREEA_IN_G(x1)  =  SEARCH_TREEA_IN_G(x1)
U1_G(x1, x2, x3)  =  U1_G(x1, x2, x3)
PB_IN_GAAG(x1, x2, x3, x4)  =  PB_IN_GAAG(x1, x4)
U8_GAAG(x1, x2, x3, x4, x5)  =  U8_GAAG(x1, x4, x5)
SEARCH_TREEE_IN_GAA(x1, x2, x3)  =  SEARCH_TREEE_IN_GAA(x1)
U4_GAA(x1, x2, x3, x4)  =  U4_GAA(x1, x2, x4)
U5_GAA(x1, x2, x3, x4)  =  U5_GAA(x1, x2, x4)
PC_IN_GAAG(x1, x2, x3, x4)  =  PC_IN_GAAG(x1, x4)
U10_GAAG(x1, x2, x3, x4, x5)  =  U10_GAAG(x1, x4, x5)
U6_GAA(x1, x2, x3, x4, x5, x6)  =  U6_GAA(x1, x2, x3, x6)
PD_IN_GAAGGAA(x1, x2, x3, x4, x5, x6, x7)  =  PD_IN_GAAGGAA(x1, x4, x5)
U12_GAAGGAA(x1, x2, x3, x4, x5, x6, x7, x8)  =  U12_GAAGGAA(x1, x4, x5, x8)
U13_GAAGGAA(x1, x2, x3, x4, x5, x6, x7, x8)  =  U13_GAAGGAA(x1, x2, x3, x4, x5, x8)
PG_IN_GGGAA(x1, x2, x3, x4, x5)  =  PG_IN_GGGAA(x1, x2, x3)
U14_GGGAA(x1, x2, x3, x4, x5, x6)  =  U14_GGGAA(x1, x2, x3, x6)
LESSF_IN_GG(x1, x2)  =  LESSF_IN_GG(x1, x2)
U7_GG(x1, x2, x3)  =  U7_GG(x1, x2, x3)
U15_GGGAA(x1, x2, x3, x4, x5, x6)  =  U15_GGGAA(x1, x2, x3, x6)
U11_GAAG(x1, x2, x3, x4, x5)  =  U11_GAAG(x1, x2, x3, x4, x5)
U9_GAAG(x1, x2, x3, x4, x5)  =  U9_GAAG(x1, x2, x3, x4, x5)
U2_G(x1, x2, x3)  =  U2_G(x1, x2, x3)
U3_G(x1, x2, x3, x4)  =  U3_G(x1, x2, x3, x4)

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

(4) Obligation:

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

SEARCH_TREEA_IN_G(tree(T17, void, T18)) → U1_G(T17, T18, pB_in_gaag(T18, X50, X51, T17))
SEARCH_TREEA_IN_G(tree(T17, void, T18)) → PB_IN_GAAG(T18, X50, X51, T17)
PB_IN_GAAG(T18, T21, T22, T17) → U8_GAAG(T18, T21, T22, T17, search_treeE_in_gaa(T18, T21, T22))
PB_IN_GAAG(T18, T21, T22, T17) → SEARCH_TREEE_IN_GAA(T18, T21, T22)
SEARCH_TREEE_IN_GAA(tree(T38, void, T39), T38, X83) → U4_GAA(T38, T39, X83, pB_in_gaag(T39, X82, X83, T38))
SEARCH_TREEE_IN_GAA(tree(T38, void, T39), T38, X83) → PB_IN_GAAG(T39, X82, X83, T38)
SEARCH_TREEE_IN_GAA(tree(T50, T51, void), X108, T50) → U5_GAA(T50, T51, X108, pC_in_gaag(T51, X108, X107, T50))
SEARCH_TREEE_IN_GAA(tree(T50, T51, void), X108, T50) → PC_IN_GAAG(T51, X108, X107, T50)
PC_IN_GAAG(T51, T54, T55, T50) → U10_GAAG(T51, T54, T55, T50, search_treeE_in_gaa(T51, T54, T55))
PC_IN_GAAG(T51, T54, T55, T50) → SEARCH_TREEE_IN_GAA(T51, T54, T55)
SEARCH_TREEE_IN_GAA(tree(T66, T67, T68), X138, X139) → U6_GAA(T66, T67, T68, X138, X139, pD_in_gaaggaa(T67, X138, X136, T66, T68, X137, X139))
SEARCH_TREEE_IN_GAA(tree(T66, T67, T68), X138, X139) → PD_IN_GAAGGAA(T67, X138, X136, T66, T68, X137, X139)
PD_IN_GAAGGAA(T67, T71, T72, T66, T68, X137, X139) → U12_GAAGGAA(T67, T71, T72, T66, T68, X137, X139, search_treeE_in_gaa(T67, T71, T72))
PD_IN_GAAGGAA(T67, T71, T72, T66, T68, X137, X139) → SEARCH_TREEE_IN_GAA(T67, T71, T72)
U12_GAAGGAA(T67, T71, T72, T66, T68, X137, X139, search_treeE_out_gaa(T67, T71, T72)) → U13_GAAGGAA(T67, T71, T72, T66, T68, X137, X139, pG_in_gggaa(T72, T66, T68, X137, X139))
U12_GAAGGAA(T67, T71, T72, T66, T68, X137, X139, search_treeE_out_gaa(T67, T71, T72)) → PG_IN_GGGAA(T72, T66, T68, X137, X139)
PG_IN_GGGAA(T72, T66, T68, X137, X139) → U14_GGGAA(T72, T66, T68, X137, X139, lessF_in_gg(T72, T66))
PG_IN_GGGAA(T72, T66, T68, X137, X139) → LESSF_IN_GG(T72, T66)
LESSF_IN_GG(s(T92), s(T93)) → U7_GG(T92, T93, lessF_in_gg(T92, T93))
LESSF_IN_GG(s(T92), s(T93)) → LESSF_IN_GG(T92, T93)
U14_GGGAA(T72, T66, T68, X137, X139, lessF_out_gg(T72, T66)) → U15_GGGAA(T72, T66, T68, X137, X139, pB_in_gaag(T68, X137, X139, T66))
U14_GGGAA(T72, T66, T68, X137, X139, lessF_out_gg(T72, T66)) → PB_IN_GAAG(T68, X137, X139, T66)
U10_GAAG(T51, T54, T55, T50, search_treeE_out_gaa(T51, T54, T55)) → U11_GAAG(T51, T54, T55, T50, lessF_in_gg(T55, T50))
U10_GAAG(T51, T54, T55, T50, search_treeE_out_gaa(T51, T54, T55)) → LESSF_IN_GG(T55, T50)
U8_GAAG(T18, T21, T22, T17, search_treeE_out_gaa(T18, T21, T22)) → U9_GAAG(T18, T21, T22, T17, lessF_in_gg(T17, T21))
U8_GAAG(T18, T21, T22, T17, search_treeE_out_gaa(T18, T21, T22)) → LESSF_IN_GG(T17, T21)
SEARCH_TREEA_IN_G(tree(T104, T105, void)) → U2_G(T104, T105, pC_in_gaag(T105, X187, X186, T104))
SEARCH_TREEA_IN_G(tree(T104, T105, void)) → PC_IN_GAAG(T105, X187, X186, T104)
SEARCH_TREEA_IN_G(tree(T114, T115, T116)) → U3_G(T114, T115, T116, pD_in_gaaggaa(T115, X213, X211, T114, T116, X212, X214))
SEARCH_TREEA_IN_G(tree(T114, T115, T116)) → PD_IN_GAAGGAA(T115, X213, X211, T114, T116, X212, X214)

The TRS R consists of the following rules:

search_treeA_in_g(void) → search_treeA_out_g(void)
search_treeA_in_g(tree(T8, void, void)) → search_treeA_out_g(tree(T8, void, void))
search_treeA_in_g(tree(T17, void, T18)) → U1_g(T17, T18, pB_in_gaag(T18, X50, X51, T17))
pB_in_gaag(T18, T21, T22, T17) → U8_gaag(T18, T21, T22, T17, search_treeE_in_gaa(T18, T21, T22))
search_treeE_in_gaa(tree(T29, void, void), T29, T29) → search_treeE_out_gaa(tree(T29, void, void), T29, T29)
search_treeE_in_gaa(tree(T38, void, T39), T38, X83) → U4_gaa(T38, T39, X83, pB_in_gaag(T39, X82, X83, T38))
U4_gaa(T38, T39, X83, pB_out_gaag(T39, X82, X83, T38)) → search_treeE_out_gaa(tree(T38, void, T39), T38, X83)
search_treeE_in_gaa(tree(T50, T51, void), X108, T50) → U5_gaa(T50, T51, X108, pC_in_gaag(T51, X108, X107, T50))
pC_in_gaag(T51, T54, T55, T50) → U10_gaag(T51, T54, T55, T50, search_treeE_in_gaa(T51, T54, T55))
search_treeE_in_gaa(tree(T66, T67, T68), X138, X139) → U6_gaa(T66, T67, T68, X138, X139, pD_in_gaaggaa(T67, X138, X136, T66, T68, X137, X139))
pD_in_gaaggaa(T67, T71, T72, T66, T68, X137, X139) → U12_gaaggaa(T67, T71, T72, T66, T68, X137, X139, search_treeE_in_gaa(T67, T71, T72))
U12_gaaggaa(T67, T71, T72, T66, T68, X137, X139, search_treeE_out_gaa(T67, T71, T72)) → U13_gaaggaa(T67, T71, T72, T66, T68, X137, X139, pG_in_gggaa(T72, T66, T68, X137, X139))
pG_in_gggaa(T72, T66, T68, X137, X139) → U14_gggaa(T72, T66, T68, X137, X139, lessF_in_gg(T72, T66))
lessF_in_gg(0, s(T87)) → lessF_out_gg(0, s(T87))
lessF_in_gg(s(T92), s(T93)) → U7_gg(T92, T93, lessF_in_gg(T92, T93))
U7_gg(T92, T93, lessF_out_gg(T92, T93)) → lessF_out_gg(s(T92), s(T93))
U14_gggaa(T72, T66, T68, X137, X139, lessF_out_gg(T72, T66)) → U15_gggaa(T72, T66, T68, X137, X139, pB_in_gaag(T68, X137, X139, T66))
U15_gggaa(T72, T66, T68, X137, X139, pB_out_gaag(T68, X137, X139, T66)) → pG_out_gggaa(T72, T66, T68, X137, X139)
U13_gaaggaa(T67, T71, T72, T66, T68, X137, X139, pG_out_gggaa(T72, T66, T68, X137, X139)) → pD_out_gaaggaa(T67, T71, T72, T66, T68, X137, X139)
U6_gaa(T66, T67, T68, X138, X139, pD_out_gaaggaa(T67, X138, X136, T66, T68, X137, X139)) → search_treeE_out_gaa(tree(T66, T67, T68), X138, X139)
U10_gaag(T51, T54, T55, T50, search_treeE_out_gaa(T51, T54, T55)) → U11_gaag(T51, T54, T55, T50, lessF_in_gg(T55, T50))
U11_gaag(T51, T54, T55, T50, lessF_out_gg(T55, T50)) → pC_out_gaag(T51, T54, T55, T50)
U5_gaa(T50, T51, X108, pC_out_gaag(T51, X108, X107, T50)) → search_treeE_out_gaa(tree(T50, T51, void), X108, T50)
U8_gaag(T18, T21, T22, T17, search_treeE_out_gaa(T18, T21, T22)) → U9_gaag(T18, T21, T22, T17, lessF_in_gg(T17, T21))
U9_gaag(T18, T21, T22, T17, lessF_out_gg(T17, T21)) → pB_out_gaag(T18, T21, T22, T17)
U1_g(T17, T18, pB_out_gaag(T18, X50, X51, T17)) → search_treeA_out_g(tree(T17, void, T18))
search_treeA_in_g(tree(T104, T105, void)) → U2_g(T104, T105, pC_in_gaag(T105, X187, X186, T104))
U2_g(T104, T105, pC_out_gaag(T105, X187, X186, T104)) → search_treeA_out_g(tree(T104, T105, void))
search_treeA_in_g(tree(T114, T115, T116)) → U3_g(T114, T115, T116, pD_in_gaaggaa(T115, X213, X211, T114, T116, X212, X214))
U3_g(T114, T115, T116, pD_out_gaaggaa(T115, X213, X211, T114, T116, X212, X214)) → search_treeA_out_g(tree(T114, T115, T116))

The argument filtering Pi contains the following mapping:
search_treeA_in_g(x1)  =  search_treeA_in_g(x1)
void  =  void
search_treeA_out_g(x1)  =  search_treeA_out_g(x1)
tree(x1, x2, x3)  =  tree(x1, x2, x3)
U1_g(x1, x2, x3)  =  U1_g(x1, x2, x3)
pB_in_gaag(x1, x2, x3, x4)  =  pB_in_gaag(x1, x4)
U8_gaag(x1, x2, x3, x4, x5)  =  U8_gaag(x1, x4, x5)
search_treeE_in_gaa(x1, x2, x3)  =  search_treeE_in_gaa(x1)
search_treeE_out_gaa(x1, x2, x3)  =  search_treeE_out_gaa(x1, x2, x3)
U4_gaa(x1, x2, x3, x4)  =  U4_gaa(x1, x2, x4)
pB_out_gaag(x1, x2, x3, x4)  =  pB_out_gaag(x1, x2, x3, x4)
U5_gaa(x1, x2, x3, x4)  =  U5_gaa(x1, x2, x4)
pC_in_gaag(x1, x2, x3, x4)  =  pC_in_gaag(x1, x4)
U10_gaag(x1, x2, x3, x4, x5)  =  U10_gaag(x1, x4, x5)
U6_gaa(x1, x2, x3, x4, x5, x6)  =  U6_gaa(x1, x2, x3, x6)
pD_in_gaaggaa(x1, x2, x3, x4, x5, x6, x7)  =  pD_in_gaaggaa(x1, x4, x5)
U12_gaaggaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  U12_gaaggaa(x1, x4, x5, x8)
U13_gaaggaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  U13_gaaggaa(x1, x2, x3, x4, x5, x8)
pG_in_gggaa(x1, x2, x3, x4, x5)  =  pG_in_gggaa(x1, x2, x3)
U14_gggaa(x1, x2, x3, x4, x5, x6)  =  U14_gggaa(x1, x2, x3, x6)
lessF_in_gg(x1, x2)  =  lessF_in_gg(x1, x2)
0  =  0
s(x1)  =  s(x1)
lessF_out_gg(x1, x2)  =  lessF_out_gg(x1, x2)
U7_gg(x1, x2, x3)  =  U7_gg(x1, x2, x3)
U15_gggaa(x1, x2, x3, x4, x5, x6)  =  U15_gggaa(x1, x2, x3, x6)
pG_out_gggaa(x1, x2, x3, x4, x5)  =  pG_out_gggaa(x1, x2, x3, x4, x5)
pD_out_gaaggaa(x1, x2, x3, x4, x5, x6, x7)  =  pD_out_gaaggaa(x1, x2, x3, x4, x5, x6, x7)
U11_gaag(x1, x2, x3, x4, x5)  =  U11_gaag(x1, x2, x3, x4, x5)
pC_out_gaag(x1, x2, x3, x4)  =  pC_out_gaag(x1, x2, x3, x4)
U9_gaag(x1, x2, x3, x4, x5)  =  U9_gaag(x1, x2, x3, x4, x5)
U2_g(x1, x2, x3)  =  U2_g(x1, x2, x3)
U3_g(x1, x2, x3, x4)  =  U3_g(x1, x2, x3, x4)
SEARCH_TREEA_IN_G(x1)  =  SEARCH_TREEA_IN_G(x1)
U1_G(x1, x2, x3)  =  U1_G(x1, x2, x3)
PB_IN_GAAG(x1, x2, x3, x4)  =  PB_IN_GAAG(x1, x4)
U8_GAAG(x1, x2, x3, x4, x5)  =  U8_GAAG(x1, x4, x5)
SEARCH_TREEE_IN_GAA(x1, x2, x3)  =  SEARCH_TREEE_IN_GAA(x1)
U4_GAA(x1, x2, x3, x4)  =  U4_GAA(x1, x2, x4)
U5_GAA(x1, x2, x3, x4)  =  U5_GAA(x1, x2, x4)
PC_IN_GAAG(x1, x2, x3, x4)  =  PC_IN_GAAG(x1, x4)
U10_GAAG(x1, x2, x3, x4, x5)  =  U10_GAAG(x1, x4, x5)
U6_GAA(x1, x2, x3, x4, x5, x6)  =  U6_GAA(x1, x2, x3, x6)
PD_IN_GAAGGAA(x1, x2, x3, x4, x5, x6, x7)  =  PD_IN_GAAGGAA(x1, x4, x5)
U12_GAAGGAA(x1, x2, x3, x4, x5, x6, x7, x8)  =  U12_GAAGGAA(x1, x4, x5, x8)
U13_GAAGGAA(x1, x2, x3, x4, x5, x6, x7, x8)  =  U13_GAAGGAA(x1, x2, x3, x4, x5, x8)
PG_IN_GGGAA(x1, x2, x3, x4, x5)  =  PG_IN_GGGAA(x1, x2, x3)
U14_GGGAA(x1, x2, x3, x4, x5, x6)  =  U14_GGGAA(x1, x2, x3, x6)
LESSF_IN_GG(x1, x2)  =  LESSF_IN_GG(x1, x2)
U7_GG(x1, x2, x3)  =  U7_GG(x1, x2, x3)
U15_GGGAA(x1, x2, x3, x4, x5, x6)  =  U15_GGGAA(x1, x2, x3, x6)
U11_GAAG(x1, x2, x3, x4, x5)  =  U11_GAAG(x1, x2, x3, x4, x5)
U9_GAAG(x1, x2, x3, x4, x5)  =  U9_GAAG(x1, x2, x3, x4, x5)
U2_G(x1, x2, x3)  =  U2_G(x1, x2, x3)
U3_G(x1, x2, x3, x4)  =  U3_G(x1, x2, x3, x4)

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

(5) DependencyGraphProof (EQUIVALENT transformation)

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

(6) Complex Obligation (AND)

(7) Obligation:

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

LESSF_IN_GG(s(T92), s(T93)) → LESSF_IN_GG(T92, T93)

The TRS R consists of the following rules:

search_treeA_in_g(void) → search_treeA_out_g(void)
search_treeA_in_g(tree(T8, void, void)) → search_treeA_out_g(tree(T8, void, void))
search_treeA_in_g(tree(T17, void, T18)) → U1_g(T17, T18, pB_in_gaag(T18, X50, X51, T17))
pB_in_gaag(T18, T21, T22, T17) → U8_gaag(T18, T21, T22, T17, search_treeE_in_gaa(T18, T21, T22))
search_treeE_in_gaa(tree(T29, void, void), T29, T29) → search_treeE_out_gaa(tree(T29, void, void), T29, T29)
search_treeE_in_gaa(tree(T38, void, T39), T38, X83) → U4_gaa(T38, T39, X83, pB_in_gaag(T39, X82, X83, T38))
U4_gaa(T38, T39, X83, pB_out_gaag(T39, X82, X83, T38)) → search_treeE_out_gaa(tree(T38, void, T39), T38, X83)
search_treeE_in_gaa(tree(T50, T51, void), X108, T50) → U5_gaa(T50, T51, X108, pC_in_gaag(T51, X108, X107, T50))
pC_in_gaag(T51, T54, T55, T50) → U10_gaag(T51, T54, T55, T50, search_treeE_in_gaa(T51, T54, T55))
search_treeE_in_gaa(tree(T66, T67, T68), X138, X139) → U6_gaa(T66, T67, T68, X138, X139, pD_in_gaaggaa(T67, X138, X136, T66, T68, X137, X139))
pD_in_gaaggaa(T67, T71, T72, T66, T68, X137, X139) → U12_gaaggaa(T67, T71, T72, T66, T68, X137, X139, search_treeE_in_gaa(T67, T71, T72))
U12_gaaggaa(T67, T71, T72, T66, T68, X137, X139, search_treeE_out_gaa(T67, T71, T72)) → U13_gaaggaa(T67, T71, T72, T66, T68, X137, X139, pG_in_gggaa(T72, T66, T68, X137, X139))
pG_in_gggaa(T72, T66, T68, X137, X139) → U14_gggaa(T72, T66, T68, X137, X139, lessF_in_gg(T72, T66))
lessF_in_gg(0, s(T87)) → lessF_out_gg(0, s(T87))
lessF_in_gg(s(T92), s(T93)) → U7_gg(T92, T93, lessF_in_gg(T92, T93))
U7_gg(T92, T93, lessF_out_gg(T92, T93)) → lessF_out_gg(s(T92), s(T93))
U14_gggaa(T72, T66, T68, X137, X139, lessF_out_gg(T72, T66)) → U15_gggaa(T72, T66, T68, X137, X139, pB_in_gaag(T68, X137, X139, T66))
U15_gggaa(T72, T66, T68, X137, X139, pB_out_gaag(T68, X137, X139, T66)) → pG_out_gggaa(T72, T66, T68, X137, X139)
U13_gaaggaa(T67, T71, T72, T66, T68, X137, X139, pG_out_gggaa(T72, T66, T68, X137, X139)) → pD_out_gaaggaa(T67, T71, T72, T66, T68, X137, X139)
U6_gaa(T66, T67, T68, X138, X139, pD_out_gaaggaa(T67, X138, X136, T66, T68, X137, X139)) → search_treeE_out_gaa(tree(T66, T67, T68), X138, X139)
U10_gaag(T51, T54, T55, T50, search_treeE_out_gaa(T51, T54, T55)) → U11_gaag(T51, T54, T55, T50, lessF_in_gg(T55, T50))
U11_gaag(T51, T54, T55, T50, lessF_out_gg(T55, T50)) → pC_out_gaag(T51, T54, T55, T50)
U5_gaa(T50, T51, X108, pC_out_gaag(T51, X108, X107, T50)) → search_treeE_out_gaa(tree(T50, T51, void), X108, T50)
U8_gaag(T18, T21, T22, T17, search_treeE_out_gaa(T18, T21, T22)) → U9_gaag(T18, T21, T22, T17, lessF_in_gg(T17, T21))
U9_gaag(T18, T21, T22, T17, lessF_out_gg(T17, T21)) → pB_out_gaag(T18, T21, T22, T17)
U1_g(T17, T18, pB_out_gaag(T18, X50, X51, T17)) → search_treeA_out_g(tree(T17, void, T18))
search_treeA_in_g(tree(T104, T105, void)) → U2_g(T104, T105, pC_in_gaag(T105, X187, X186, T104))
U2_g(T104, T105, pC_out_gaag(T105, X187, X186, T104)) → search_treeA_out_g(tree(T104, T105, void))
search_treeA_in_g(tree(T114, T115, T116)) → U3_g(T114, T115, T116, pD_in_gaaggaa(T115, X213, X211, T114, T116, X212, X214))
U3_g(T114, T115, T116, pD_out_gaaggaa(T115, X213, X211, T114, T116, X212, X214)) → search_treeA_out_g(tree(T114, T115, T116))

The argument filtering Pi contains the following mapping:
search_treeA_in_g(x1)  =  search_treeA_in_g(x1)
void  =  void
search_treeA_out_g(x1)  =  search_treeA_out_g(x1)
tree(x1, x2, x3)  =  tree(x1, x2, x3)
U1_g(x1, x2, x3)  =  U1_g(x1, x2, x3)
pB_in_gaag(x1, x2, x3, x4)  =  pB_in_gaag(x1, x4)
U8_gaag(x1, x2, x3, x4, x5)  =  U8_gaag(x1, x4, x5)
search_treeE_in_gaa(x1, x2, x3)  =  search_treeE_in_gaa(x1)
search_treeE_out_gaa(x1, x2, x3)  =  search_treeE_out_gaa(x1, x2, x3)
U4_gaa(x1, x2, x3, x4)  =  U4_gaa(x1, x2, x4)
pB_out_gaag(x1, x2, x3, x4)  =  pB_out_gaag(x1, x2, x3, x4)
U5_gaa(x1, x2, x3, x4)  =  U5_gaa(x1, x2, x4)
pC_in_gaag(x1, x2, x3, x4)  =  pC_in_gaag(x1, x4)
U10_gaag(x1, x2, x3, x4, x5)  =  U10_gaag(x1, x4, x5)
U6_gaa(x1, x2, x3, x4, x5, x6)  =  U6_gaa(x1, x2, x3, x6)
pD_in_gaaggaa(x1, x2, x3, x4, x5, x6, x7)  =  pD_in_gaaggaa(x1, x4, x5)
U12_gaaggaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  U12_gaaggaa(x1, x4, x5, x8)
U13_gaaggaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  U13_gaaggaa(x1, x2, x3, x4, x5, x8)
pG_in_gggaa(x1, x2, x3, x4, x5)  =  pG_in_gggaa(x1, x2, x3)
U14_gggaa(x1, x2, x3, x4, x5, x6)  =  U14_gggaa(x1, x2, x3, x6)
lessF_in_gg(x1, x2)  =  lessF_in_gg(x1, x2)
0  =  0
s(x1)  =  s(x1)
lessF_out_gg(x1, x2)  =  lessF_out_gg(x1, x2)
U7_gg(x1, x2, x3)  =  U7_gg(x1, x2, x3)
U15_gggaa(x1, x2, x3, x4, x5, x6)  =  U15_gggaa(x1, x2, x3, x6)
pG_out_gggaa(x1, x2, x3, x4, x5)  =  pG_out_gggaa(x1, x2, x3, x4, x5)
pD_out_gaaggaa(x1, x2, x3, x4, x5, x6, x7)  =  pD_out_gaaggaa(x1, x2, x3, x4, x5, x6, x7)
U11_gaag(x1, x2, x3, x4, x5)  =  U11_gaag(x1, x2, x3, x4, x5)
pC_out_gaag(x1, x2, x3, x4)  =  pC_out_gaag(x1, x2, x3, x4)
U9_gaag(x1, x2, x3, x4, x5)  =  U9_gaag(x1, x2, x3, x4, x5)
U2_g(x1, x2, x3)  =  U2_g(x1, x2, x3)
U3_g(x1, x2, x3, x4)  =  U3_g(x1, x2, x3, x4)
LESSF_IN_GG(x1, x2)  =  LESSF_IN_GG(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:

LESSF_IN_GG(s(T92), s(T93)) → LESSF_IN_GG(T92, T93)

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

(10) PiDPToQDPProof (EQUIVALENT transformation)

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

(11) Obligation:

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

LESSF_IN_GG(s(T92), s(T93)) → LESSF_IN_GG(T92, T93)

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:

• LESSF_IN_GG(s(T92), s(T93)) → LESSF_IN_GG(T92, T93)
  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:

PB_IN_GAAG(T18, T21, T22, T17) → SEARCH_TREEE_IN_GAA(T18, T21, T22)
SEARCH_TREEE_IN_GAA(tree(T38, void, T39), T38, X83) → PB_IN_GAAG(T39, X82, X83, T38)
SEARCH_TREEE_IN_GAA(tree(T50, T51, void), X108, T50) → PC_IN_GAAG(T51, X108, X107, T50)
PC_IN_GAAG(T51, T54, T55, T50) → SEARCH_TREEE_IN_GAA(T51, T54, T55)
SEARCH_TREEE_IN_GAA(tree(T66, T67, T68), X138, X139) → PD_IN_GAAGGAA(T67, X138, X136, T66, T68, X137, X139)
PD_IN_GAAGGAA(T67, T71, T72, T66, T68, X137, X139) → U12_GAAGGAA(T67, T71, T72, T66, T68, X137, X139, search_treeE_in_gaa(T67, T71, T72))
U12_GAAGGAA(T67, T71, T72, T66, T68, X137, X139, search_treeE_out_gaa(T67, T71, T72)) → PG_IN_GGGAA(T72, T66, T68, X137, X139)
PG_IN_GGGAA(T72, T66, T68, X137, X139) → U14_GGGAA(T72, T66, T68, X137, X139, lessF_in_gg(T72, T66))
U14_GGGAA(T72, T66, T68, X137, X139, lessF_out_gg(T72, T66)) → PB_IN_GAAG(T68, X137, X139, T66)
PD_IN_GAAGGAA(T67, T71, T72, T66, T68, X137, X139) → SEARCH_TREEE_IN_GAA(T67, T71, T72)

The TRS R consists of the following rules:

search_treeA_in_g(void) → search_treeA_out_g(void)
search_treeA_in_g(tree(T8, void, void)) → search_treeA_out_g(tree(T8, void, void))
search_treeA_in_g(tree(T17, void, T18)) → U1_g(T17, T18, pB_in_gaag(T18, X50, X51, T17))
pB_in_gaag(T18, T21, T22, T17) → U8_gaag(T18, T21, T22, T17, search_treeE_in_gaa(T18, T21, T22))
search_treeE_in_gaa(tree(T29, void, void), T29, T29) → search_treeE_out_gaa(tree(T29, void, void), T29, T29)
search_treeE_in_gaa(tree(T38, void, T39), T38, X83) → U4_gaa(T38, T39, X83, pB_in_gaag(T39, X82, X83, T38))
U4_gaa(T38, T39, X83, pB_out_gaag(T39, X82, X83, T38)) → search_treeE_out_gaa(tree(T38, void, T39), T38, X83)
search_treeE_in_gaa(tree(T50, T51, void), X108, T50) → U5_gaa(T50, T51, X108, pC_in_gaag(T51, X108, X107, T50))
pC_in_gaag(T51, T54, T55, T50) → U10_gaag(T51, T54, T55, T50, search_treeE_in_gaa(T51, T54, T55))
search_treeE_in_gaa(tree(T66, T67, T68), X138, X139) → U6_gaa(T66, T67, T68, X138, X139, pD_in_gaaggaa(T67, X138, X136, T66, T68, X137, X139))
pD_in_gaaggaa(T67, T71, T72, T66, T68, X137, X139) → U12_gaaggaa(T67, T71, T72, T66, T68, X137, X139, search_treeE_in_gaa(T67, T71, T72))
U12_gaaggaa(T67, T71, T72, T66, T68, X137, X139, search_treeE_out_gaa(T67, T71, T72)) → U13_gaaggaa(T67, T71, T72, T66, T68, X137, X139, pG_in_gggaa(T72, T66, T68, X137, X139))
pG_in_gggaa(T72, T66, T68, X137, X139) → U14_gggaa(T72, T66, T68, X137, X139, lessF_in_gg(T72, T66))
lessF_in_gg(0, s(T87)) → lessF_out_gg(0, s(T87))
lessF_in_gg(s(T92), s(T93)) → U7_gg(T92, T93, lessF_in_gg(T92, T93))
U7_gg(T92, T93, lessF_out_gg(T92, T93)) → lessF_out_gg(s(T92), s(T93))
U14_gggaa(T72, T66, T68, X137, X139, lessF_out_gg(T72, T66)) → U15_gggaa(T72, T66, T68, X137, X139, pB_in_gaag(T68, X137, X139, T66))
U15_gggaa(T72, T66, T68, X137, X139, pB_out_gaag(T68, X137, X139, T66)) → pG_out_gggaa(T72, T66, T68, X137, X139)
U13_gaaggaa(T67, T71, T72, T66, T68, X137, X139, pG_out_gggaa(T72, T66, T68, X137, X139)) → pD_out_gaaggaa(T67, T71, T72, T66, T68, X137, X139)
U6_gaa(T66, T67, T68, X138, X139, pD_out_gaaggaa(T67, X138, X136, T66, T68, X137, X139)) → search_treeE_out_gaa(tree(T66, T67, T68), X138, X139)
U10_gaag(T51, T54, T55, T50, search_treeE_out_gaa(T51, T54, T55)) → U11_gaag(T51, T54, T55, T50, lessF_in_gg(T55, T50))
U11_gaag(T51, T54, T55, T50, lessF_out_gg(T55, T50)) → pC_out_gaag(T51, T54, T55, T50)
U5_gaa(T50, T51, X108, pC_out_gaag(T51, X108, X107, T50)) → search_treeE_out_gaa(tree(T50, T51, void), X108, T50)
U8_gaag(T18, T21, T22, T17, search_treeE_out_gaa(T18, T21, T22)) → U9_gaag(T18, T21, T22, T17, lessF_in_gg(T17, T21))
U9_gaag(T18, T21, T22, T17, lessF_out_gg(T17, T21)) → pB_out_gaag(T18, T21, T22, T17)
U1_g(T17, T18, pB_out_gaag(T18, X50, X51, T17)) → search_treeA_out_g(tree(T17, void, T18))
search_treeA_in_g(tree(T104, T105, void)) → U2_g(T104, T105, pC_in_gaag(T105, X187, X186, T104))
U2_g(T104, T105, pC_out_gaag(T105, X187, X186, T104)) → search_treeA_out_g(tree(T104, T105, void))
search_treeA_in_g(tree(T114, T115, T116)) → U3_g(T114, T115, T116, pD_in_gaaggaa(T115, X213, X211, T114, T116, X212, X214))
U3_g(T114, T115, T116, pD_out_gaaggaa(T115, X213, X211, T114, T116, X212, X214)) → search_treeA_out_g(tree(T114, T115, T116))

The argument filtering Pi contains the following mapping:
search_treeA_in_g(x1)  =  search_treeA_in_g(x1)
void  =  void
search_treeA_out_g(x1)  =  search_treeA_out_g(x1)
tree(x1, x2, x3)  =  tree(x1, x2, x3)
U1_g(x1, x2, x3)  =  U1_g(x1, x2, x3)
pB_in_gaag(x1, x2, x3, x4)  =  pB_in_gaag(x1, x4)
U8_gaag(x1, x2, x3, x4, x5)  =  U8_gaag(x1, x4, x5)
search_treeE_in_gaa(x1, x2, x3)  =  search_treeE_in_gaa(x1)
search_treeE_out_gaa(x1, x2, x3)  =  search_treeE_out_gaa(x1, x2, x3)
U4_gaa(x1, x2, x3, x4)  =  U4_gaa(x1, x2, x4)
pB_out_gaag(x1, x2, x3, x4)  =  pB_out_gaag(x1, x2, x3, x4)
U5_gaa(x1, x2, x3, x4)  =  U5_gaa(x1, x2, x4)
pC_in_gaag(x1, x2, x3, x4)  =  pC_in_gaag(x1, x4)
U10_gaag(x1, x2, x3, x4, x5)  =  U10_gaag(x1, x4, x5)
U6_gaa(x1, x2, x3, x4, x5, x6)  =  U6_gaa(x1, x2, x3, x6)
pD_in_gaaggaa(x1, x2, x3, x4, x5, x6, x7)  =  pD_in_gaaggaa(x1, x4, x5)
U12_gaaggaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  U12_gaaggaa(x1, x4, x5, x8)
U13_gaaggaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  U13_gaaggaa(x1, x2, x3, x4, x5, x8)
pG_in_gggaa(x1, x2, x3, x4, x5)  =  pG_in_gggaa(x1, x2, x3)
U14_gggaa(x1, x2, x3, x4, x5, x6)  =  U14_gggaa(x1, x2, x3, x6)
lessF_in_gg(x1, x2)  =  lessF_in_gg(x1, x2)
0  =  0
s(x1)  =  s(x1)
lessF_out_gg(x1, x2)  =  lessF_out_gg(x1, x2)
U7_gg(x1, x2, x3)  =  U7_gg(x1, x2, x3)
U15_gggaa(x1, x2, x3, x4, x5, x6)  =  U15_gggaa(x1, x2, x3, x6)
pG_out_gggaa(x1, x2, x3, x4, x5)  =  pG_out_gggaa(x1, x2, x3, x4, x5)
pD_out_gaaggaa(x1, x2, x3, x4, x5, x6, x7)  =  pD_out_gaaggaa(x1, x2, x3, x4, x5, x6, x7)
U11_gaag(x1, x2, x3, x4, x5)  =  U11_gaag(x1, x2, x3, x4, x5)
pC_out_gaag(x1, x2, x3, x4)  =  pC_out_gaag(x1, x2, x3, x4)
U9_gaag(x1, x2, x3, x4, x5)  =  U9_gaag(x1, x2, x3, x4, x5)
U2_g(x1, x2, x3)  =  U2_g(x1, x2, x3)
U3_g(x1, x2, x3, x4)  =  U3_g(x1, x2, x3, x4)
PB_IN_GAAG(x1, x2, x3, x4)  =  PB_IN_GAAG(x1, x4)
SEARCH_TREEE_IN_GAA(x1, x2, x3)  =  SEARCH_TREEE_IN_GAA(x1)
PC_IN_GAAG(x1, x2, x3, x4)  =  PC_IN_GAAG(x1, x4)
PD_IN_GAAGGAA(x1, x2, x3, x4, x5, x6, x7)  =  PD_IN_GAAGGAA(x1, x4, x5)
U12_GAAGGAA(x1, x2, x3, x4, x5, x6, x7, x8)  =  U12_GAAGGAA(x1, x4, x5, x8)
PG_IN_GGGAA(x1, x2, x3, x4, x5)  =  PG_IN_GGGAA(x1, x2, x3)
U14_GGGAA(x1, x2, x3, x4, x5, x6)  =  U14_GGGAA(x1, x2, x3, x6)

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:

PB_IN_GAAG(T18, T21, T22, T17) → SEARCH_TREEE_IN_GAA(T18, T21, T22)
SEARCH_TREEE_IN_GAA(tree(T38, void, T39), T38, X83) → PB_IN_GAAG(T39, X82, X83, T38)
SEARCH_TREEE_IN_GAA(tree(T50, T51, void), X108, T50) → PC_IN_GAAG(T51, X108, X107, T50)
PC_IN_GAAG(T51, T54, T55, T50) → SEARCH_TREEE_IN_GAA(T51, T54, T55)
SEARCH_TREEE_IN_GAA(tree(T66, T67, T68), X138, X139) → PD_IN_GAAGGAA(T67, X138, X136, T66, T68, X137, X139)
PD_IN_GAAGGAA(T67, T71, T72, T66, T68, X137, X139) → U12_GAAGGAA(T67, T71, T72, T66, T68, X137, X139, search_treeE_in_gaa(T67, T71, T72))
U12_GAAGGAA(T67, T71, T72, T66, T68, X137, X139, search_treeE_out_gaa(T67, T71, T72)) → PG_IN_GGGAA(T72, T66, T68, X137, X139)
PG_IN_GGGAA(T72, T66, T68, X137, X139) → U14_GGGAA(T72, T66, T68, X137, X139, lessF_in_gg(T72, T66))
U14_GGGAA(T72, T66, T68, X137, X139, lessF_out_gg(T72, T66)) → PB_IN_GAAG(T68, X137, X139, T66)
PD_IN_GAAGGAA(T67, T71, T72, T66, T68, X137, X139) → SEARCH_TREEE_IN_GAA(T67, T71, T72)

The TRS R consists of the following rules:

search_treeE_in_gaa(tree(T29, void, void), T29, T29) → search_treeE_out_gaa(tree(T29, void, void), T29, T29)
search_treeE_in_gaa(tree(T38, void, T39), T38, X83) → U4_gaa(T38, T39, X83, pB_in_gaag(T39, X82, X83, T38))
search_treeE_in_gaa(tree(T50, T51, void), X108, T50) → U5_gaa(T50, T51, X108, pC_in_gaag(T51, X108, X107, T50))
search_treeE_in_gaa(tree(T66, T67, T68), X138, X139) → U6_gaa(T66, T67, T68, X138, X139, pD_in_gaaggaa(T67, X138, X136, T66, T68, X137, X139))
lessF_in_gg(0, s(T87)) → lessF_out_gg(0, s(T87))
lessF_in_gg(s(T92), s(T93)) → U7_gg(T92, T93, lessF_in_gg(T92, T93))
U4_gaa(T38, T39, X83, pB_out_gaag(T39, X82, X83, T38)) → search_treeE_out_gaa(tree(T38, void, T39), T38, X83)
U5_gaa(T50, T51, X108, pC_out_gaag(T51, X108, X107, T50)) → search_treeE_out_gaa(tree(T50, T51, void), X108, T50)
U6_gaa(T66, T67, T68, X138, X139, pD_out_gaaggaa(T67, X138, X136, T66, T68, X137, X139)) → search_treeE_out_gaa(tree(T66, T67, T68), X138, X139)
U7_gg(T92, T93, lessF_out_gg(T92, T93)) → lessF_out_gg(s(T92), s(T93))
pB_in_gaag(T18, T21, T22, T17) → U8_gaag(T18, T21, T22, T17, search_treeE_in_gaa(T18, T21, T22))
pC_in_gaag(T51, T54, T55, T50) → U10_gaag(T51, T54, T55, T50, search_treeE_in_gaa(T51, T54, T55))
pD_in_gaaggaa(T67, T71, T72, T66, T68, X137, X139) → U12_gaaggaa(T67, T71, T72, T66, T68, X137, X139, search_treeE_in_gaa(T67, T71, T72))
U8_gaag(T18, T21, T22, T17, search_treeE_out_gaa(T18, T21, T22)) → U9_gaag(T18, T21, T22, T17, lessF_in_gg(T17, T21))
U10_gaag(T51, T54, T55, T50, search_treeE_out_gaa(T51, T54, T55)) → U11_gaag(T51, T54, T55, T50, lessF_in_gg(T55, T50))
U12_gaaggaa(T67, T71, T72, T66, T68, X137, X139, search_treeE_out_gaa(T67, T71, T72)) → U13_gaaggaa(T67, T71, T72, T66, T68, X137, X139, pG_in_gggaa(T72, T66, T68, X137, X139))
U9_gaag(T18, T21, T22, T17, lessF_out_gg(T17, T21)) → pB_out_gaag(T18, T21, T22, T17)
U11_gaag(T51, T54, T55, T50, lessF_out_gg(T55, T50)) → pC_out_gaag(T51, T54, T55, T50)
U13_gaaggaa(T67, T71, T72, T66, T68, X137, X139, pG_out_gggaa(T72, T66, T68, X137, X139)) → pD_out_gaaggaa(T67, T71, T72, T66, T68, X137, X139)
pG_in_gggaa(T72, T66, T68, X137, X139) → U14_gggaa(T72, T66, T68, X137, X139, lessF_in_gg(T72, T66))
U14_gggaa(T72, T66, T68, X137, X139, lessF_out_gg(T72, T66)) → U15_gggaa(T72, T66, T68, X137, X139, pB_in_gaag(T68, X137, X139, T66))
U15_gggaa(T72, T66, T68, X137, X139, pB_out_gaag(T68, X137, X139, T66)) → pG_out_gggaa(T72, T66, T68, X137, X139)

The argument filtering Pi contains the following mapping:
void  =  void
tree(x1, x2, x3)  =  tree(x1, x2, x3)
pB_in_gaag(x1, x2, x3, x4)  =  pB_in_gaag(x1, x4)
U8_gaag(x1, x2, x3, x4, x5)  =  U8_gaag(x1, x4, x5)
search_treeE_in_gaa(x1, x2, x3)  =  search_treeE_in_gaa(x1)
search_treeE_out_gaa(x1, x2, x3)  =  search_treeE_out_gaa(x1, x2, x3)
U4_gaa(x1, x2, x3, x4)  =  U4_gaa(x1, x2, x4)
pB_out_gaag(x1, x2, x3, x4)  =  pB_out_gaag(x1, x2, x3, x4)
U5_gaa(x1, x2, x3, x4)  =  U5_gaa(x1, x2, x4)
pC_in_gaag(x1, x2, x3, x4)  =  pC_in_gaag(x1, x4)
U10_gaag(x1, x2, x3, x4, x5)  =  U10_gaag(x1, x4, x5)
U6_gaa(x1, x2, x3, x4, x5, x6)  =  U6_gaa(x1, x2, x3, x6)
pD_in_gaaggaa(x1, x2, x3, x4, x5, x6, x7)  =  pD_in_gaaggaa(x1, x4, x5)
U12_gaaggaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  U12_gaaggaa(x1, x4, x5, x8)
U13_gaaggaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  U13_gaaggaa(x1, x2, x3, x4, x5, x8)
pG_in_gggaa(x1, x2, x3, x4, x5)  =  pG_in_gggaa(x1, x2, x3)
U14_gggaa(x1, x2, x3, x4, x5, x6)  =  U14_gggaa(x1, x2, x3, x6)
lessF_in_gg(x1, x2)  =  lessF_in_gg(x1, x2)
0  =  0
s(x1)  =  s(x1)
lessF_out_gg(x1, x2)  =  lessF_out_gg(x1, x2)
U7_gg(x1, x2, x3)  =  U7_gg(x1, x2, x3)
U15_gggaa(x1, x2, x3, x4, x5, x6)  =  U15_gggaa(x1, x2, x3, x6)
pG_out_gggaa(x1, x2, x3, x4, x5)  =  pG_out_gggaa(x1, x2, x3, x4, x5)
pD_out_gaaggaa(x1, x2, x3, x4, x5, x6, x7)  =  pD_out_gaaggaa(x1, x2, x3, x4, x5, x6, x7)
U11_gaag(x1, x2, x3, x4, x5)  =  U11_gaag(x1, x2, x3, x4, x5)
pC_out_gaag(x1, x2, x3, x4)  =  pC_out_gaag(x1, x2, x3, x4)
U9_gaag(x1, x2, x3, x4, x5)  =  U9_gaag(x1, x2, x3, x4, x5)
PB_IN_GAAG(x1, x2, x3, x4)  =  PB_IN_GAAG(x1, x4)
SEARCH_TREEE_IN_GAA(x1, x2, x3)  =  SEARCH_TREEE_IN_GAA(x1)
PC_IN_GAAG(x1, x2, x3, x4)  =  PC_IN_GAAG(x1, x4)
PD_IN_GAAGGAA(x1, x2, x3, x4, x5, x6, x7)  =  PD_IN_GAAGGAA(x1, x4, x5)
U12_GAAGGAA(x1, x2, x3, x4, x5, x6, x7, x8)  =  U12_GAAGGAA(x1, x4, x5, x8)
PG_IN_GGGAA(x1, x2, x3, x4, x5)  =  PG_IN_GGGAA(x1, x2, x3)
U14_GGGAA(x1, x2, x3, x4, x5, x6)  =  U14_GGGAA(x1, x2, x3, x6)

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:

PB_IN_GAAG(T18, T17) → SEARCH_TREEE_IN_GAA(T18)
SEARCH_TREEE_IN_GAA(tree(T38, void, T39)) → PB_IN_GAAG(T39, T38)
SEARCH_TREEE_IN_GAA(tree(T50, T51, void)) → PC_IN_GAAG(T51, T50)
PC_IN_GAAG(T51, T50) → SEARCH_TREEE_IN_GAA(T51)
SEARCH_TREEE_IN_GAA(tree(T66, T67, T68)) → PD_IN_GAAGGAA(T67, T66, T68)
PD_IN_GAAGGAA(T67, T66, T68) → U12_GAAGGAA(T67, T66, T68, search_treeE_in_gaa(T67))
U12_GAAGGAA(T67, T66, T68, search_treeE_out_gaa(T67, T71, T72)) → PG_IN_GGGAA(T72, T66, T68)
PG_IN_GGGAA(T72, T66, T68) → U14_GGGAA(T72, T66, T68, lessF_in_gg(T72, T66))
U14_GGGAA(T72, T66, T68, lessF_out_gg(T72, T66)) → PB_IN_GAAG(T68, T66)
PD_IN_GAAGGAA(T67, T66, T68) → SEARCH_TREEE_IN_GAA(T67)

The TRS R consists of the following rules:

search_treeE_in_gaa(tree(T29, void, void)) → search_treeE_out_gaa(tree(T29, void, void), T29, T29)
search_treeE_in_gaa(tree(T38, void, T39)) → U4_gaa(T38, T39, pB_in_gaag(T39, T38))
search_treeE_in_gaa(tree(T50, T51, void)) → U5_gaa(T50, T51, pC_in_gaag(T51, T50))
search_treeE_in_gaa(tree(T66, T67, T68)) → U6_gaa(T66, T67, T68, pD_in_gaaggaa(T67, T66, T68))
lessF_in_gg(0, s(T87)) → lessF_out_gg(0, s(T87))
lessF_in_gg(s(T92), s(T93)) → U7_gg(T92, T93, lessF_in_gg(T92, T93))
U4_gaa(T38, T39, pB_out_gaag(T39, X82, X83, T38)) → search_treeE_out_gaa(tree(T38, void, T39), T38, X83)
U5_gaa(T50, T51, pC_out_gaag(T51, X108, X107, T50)) → search_treeE_out_gaa(tree(T50, T51, void), X108, T50)
U6_gaa(T66, T67, T68, pD_out_gaaggaa(T67, X138, X136, T66, T68, X137, X139)) → search_treeE_out_gaa(tree(T66, T67, T68), X138, X139)
U7_gg(T92, T93, lessF_out_gg(T92, T93)) → lessF_out_gg(s(T92), s(T93))
pB_in_gaag(T18, T17) → U8_gaag(T18, T17, search_treeE_in_gaa(T18))
pC_in_gaag(T51, T50) → U10_gaag(T51, T50, search_treeE_in_gaa(T51))
pD_in_gaaggaa(T67, T66, T68) → U12_gaaggaa(T67, T66, T68, search_treeE_in_gaa(T67))
U8_gaag(T18, T17, search_treeE_out_gaa(T18, T21, T22)) → U9_gaag(T18, T21, T22, T17, lessF_in_gg(T17, T21))
U10_gaag(T51, T50, search_treeE_out_gaa(T51, T54, T55)) → U11_gaag(T51, T54, T55, T50, lessF_in_gg(T55, T50))
U12_gaaggaa(T67, T66, T68, search_treeE_out_gaa(T67, T71, T72)) → U13_gaaggaa(T67, T71, T72, T66, T68, pG_in_gggaa(T72, T66, T68))
U9_gaag(T18, T21, T22, T17, lessF_out_gg(T17, T21)) → pB_out_gaag(T18, T21, T22, T17)
U11_gaag(T51, T54, T55, T50, lessF_out_gg(T55, T50)) → pC_out_gaag(T51, T54, T55, T50)
U13_gaaggaa(T67, T71, T72, T66, T68, pG_out_gggaa(T72, T66, T68, X137, X139)) → pD_out_gaaggaa(T67, T71, T72, T66, T68, X137, X139)
pG_in_gggaa(T72, T66, T68) → U14_gggaa(T72, T66, T68, lessF_in_gg(T72, T66))
U14_gggaa(T72, T66, T68, lessF_out_gg(T72, T66)) → U15_gggaa(T72, T66, T68, pB_in_gaag(T68, T66))
U15_gggaa(T72, T66, T68, pB_out_gaag(T68, X137, X139, T66)) → pG_out_gggaa(T72, T66, T68, X137, X139)

The set Q consists of the following terms:

search_treeE_in_gaa(x0)
lessF_in_gg(x0, x1)
U4_gaa(x0, x1, x2)
U5_gaa(x0, x1, x2)
U6_gaa(x0, x1, x2, x3)
U7_gg(x0, x1, x2)
pB_in_gaag(x0, x1)
pC_in_gaag(x0, x1)
pD_in_gaaggaa(x0, x1, x2)
U8_gaag(x0, x1, x2)
U10_gaag(x0, x1, x2)
U12_gaaggaa(x0, x1, x2, x3)
U9_gaag(x0, x1, x2, x3, x4)
U11_gaag(x0, x1, x2, x3, x4)
U13_gaaggaa(x0, x1, x2, x3, x4, x5)
pG_in_gggaa(x0, x1, x2)
U14_gggaa(x0, x1, x2, x3)
U15_gggaa(x0, x1, x2, x3)

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:

• SEARCH_TREEE_IN_GAA(tree(T38, void, T39)) → PB_IN_GAAG(T39, T38)
  The graph contains the following edges 1 > 1, 1 > 2

• U14_GGGAA(T72, T66, T68, lessF_out_gg(T72, T66)) → PB_IN_GAAG(T68, T66)
  The graph contains the following edges 3 >= 1, 2 >= 2, 4 > 2

• PB_IN_GAAG(T18, T17) → SEARCH_TREEE_IN_GAA(T18)
  The graph contains the following edges 1 >= 1

• PC_IN_GAAG(T51, T50) → SEARCH_TREEE_IN_GAA(T51)
  The graph contains the following edges 1 >= 1

• PD_IN_GAAGGAA(T67, T66, T68) → SEARCH_TREEE_IN_GAA(T67)
  The graph contains the following edges 1 >= 1

• SEARCH_TREEE_IN_GAA(tree(T50, T51, void)) → PC_IN_GAAG(T51, T50)
  The graph contains the following edges 1 > 1, 1 > 2

• SEARCH_TREEE_IN_GAA(tree(T66, T67, T68)) → PD_IN_GAAGGAA(T67, T66, T68)
  The graph contains the following edges 1 > 1, 1 > 2, 1 > 3

• PD_IN_GAAGGAA(T67, T66, T68) → U12_GAAGGAA(T67, T66, T68, search_treeE_in_gaa(T67))
  The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 3

• U12_GAAGGAA(T67, T66, T68, search_treeE_out_gaa(T67, T71, T72)) → PG_IN_GGGAA(T72, T66, T68)
  The graph contains the following edges 4 > 1, 2 >= 2, 3 >= 3

• PG_IN_GGGAA(T72, T66, T68) → U14_GGGAA(T72, T66, T68, lessF_in_gg(T72, T66))
  The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 3

(20) YES