Left Termination proof of /tmp/tmppqlzJc/merge.pl

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

0 Prolog

↳1 PrologToPiTRSViaGraphTransformerProof (⇒, 168 ms)

↳2 PiTRS

↳3 DependencyPairsProof (⇔, 313 ms)

↳4 PiDP

↳5 DependencyGraphProof (⇔, 10 ms)

↳6 AND

    ↳7 PiDP

        ↳8 UsableRulesProof (⇔, 0 ms)

        ↳9 PiDP

        ↳10 PiDPToQDPProof (⇔, 10 ms)

        ↳11 QDP

        ↳12 QDPSizeChangeProof (⇔, 0 ms)

        ↳13 YES

    ↳14 PiDP

        ↳15 UsableRulesProof (⇔, 0 ms)

        ↳16 PiDP

        ↳17 PiDPToQDPProof (⇔, 0 ms)

        ↳18 QDP

        ↳19 QDPSizeChangeProof (⇔, 0 ms)

        ↳20 YES

    ↳21 PiDP

        ↳22 UsableRulesProof (⇔, 0 ms)

        ↳23 PiDP

        ↳24 PiDPToQDPProof (⇒, 28 ms)

        ↳25 QDP

        ↳26 QDPOrderProof (⇔, 227 ms)

        ↳27 QDP

        ↳28 DependencyGraphProof (⇔, 0 ms)

        ↳29 QDP

        ↳30 QDPOrderProof (⇔, 118 ms)

        ↳31 QDP

        ↳32 DependencyGraphProof (⇔, 0 ms)

        ↳33 QDP

        ↳34 UsableRulesProof (⇔, 0 ms)

        ↳35 QDP

        ↳36 QReductionProof (⇔, 0 ms)

        ↳37 QDP

        ↳38 QDPSizeChangeProof (⇔, 0 ms)

        ↳39 YES

(0) Obligation:

Clauses:

merge([], X, X).
merge(X, [], X).
merge(.(X, Xs), .(Y, Ys), .(X, Zs)) :- ','(leq(X, Y), merge(Xs, .(Y, Ys), Zs)).
merge(.(X, Xs), .(Y, Ys), .(Y, Zs)) :- ','(less(Y, X), merge(.(X, Xs), Ys, Zs)).
less(0, s(0)).
less(s(X), s(Y)) :- less(X, Y).
leq(0, 0).
leq(0, s(0)).
leq(s(X), s(Y)) :- leq(X, Y).

Query: merge(g,g,a)

(1) PrologToPiTRSViaGraphTransformerProof (SOUND transformation)

Transformed Prolog program to (Pi-)TRS.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
2 [label="A: merge(T1, T2, T3)\n\nT1 is ground\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
4 [label="4: merge(T1, T2, T3), SCOPE: 1, CLAUSE: 0 | merge(T1, T2, T3), SCOPE: 1, CLAUSE: 1 | merge(T1, T2, T3), SCOPE: 1, CLAUSE: 2 | merge(T1, T2, T3), SCOPE: 1, CLAUSE: 3\n\nT1 is ground\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
9 [label="9: true | merge([], T5, T3), SCOPE: 1, CLAUSE: 1 | merge([], T5, T3), SCOPE: 1, CLAUSE: 2 | merge([], T5, T3), SCOPE: 1, CLAUSE: 3\n\nT5 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
13 [label="13: merge(T1, T2, T3), SCOPE: 1, CLAUSE: 1 | merge(T1, T2, T3), SCOPE: 1, CLAUSE: 2 | merge(T1, T2, T3), SCOPE: 1, CLAUSE: 3\n\nT1 is ground\nT2 is ground\nX2 is free\nmerge(T1, T2, T3) !=? merge([], X2, X2)", fontsize=16, style=filled, fillcolor=lightyellow];
16 [label="16: merge([], T5, T3), SCOPE: 1, CLAUSE: 1 | merge([], T5, T3), SCOPE: 1, CLAUSE: 2 | merge([], T5, T3), SCOPE: 1, CLAUSE: 3\n\nT5 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
18 [label="18: true | merge([], [], T3), SCOPE: 1, CLAUSE: 2 | merge([], [], T3), SCOPE: 1, CLAUSE: 3\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
22 [label="22: merge([], T5, T3), SCOPE: 1, CLAUSE: 2 | merge([], T5, T3), SCOPE: 1, CLAUSE: 3\n\nT5 is ground\nX4 is free\nmerge([], T5, T3) !=? merge(X4, [], X4)", fontsize=16, style=filled, fillcolor=lightyellow];
24 [label="24: merge([], [], T3), SCOPE: 1, CLAUSE: 2 | merge([], [], T3), SCOPE: 1, CLAUSE: 3\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
26 [label="26: merge([], [], T3), SCOPE: 1, CLAUSE: 3\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
31 [label="31: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
33 [label="33: merge([], T5, T3), SCOPE: 1, CLAUSE: 3\n\nT5 is ground\nX4 is free\nmerge([], T5, T3) !=? merge(X4, [], X4)", fontsize=16, style=filled, fillcolor=lightyellow];
35 [label="35: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
39 [label="39: true | merge(T7, [], T3), SCOPE: 1, CLAUSE: 2 | merge(T7, [], T3), SCOPE: 1, CLAUSE: 3\n\nT7 is ground\nX2 is free\nmerge(T7, [], T3) !=? merge([], X2, X2)", fontsize=16, style=filled, fillcolor=lightyellow];
41 [label="41: merge(T1, T2, T3), SCOPE: 1, CLAUSE: 2 | merge(T1, T2, T3), SCOPE: 1, CLAUSE: 3\n\nT1 is ground\nT2 is ground\nX2 is free\nX26 is free\nmerge(T1, T2, T3) !=? merge([], X2, X2)\nmerge(T1, T2, T3) !=? merge(X26, [], X26)", fontsize=16, style=filled, fillcolor=lightyellow];
42 [label="42: merge(T7, [], T3), SCOPE: 1, CLAUSE: 2 | merge(T7, [], T3), SCOPE: 1, CLAUSE: 3\n\nT7 is ground\nX2 is free\nmerge(T7, [], T3) !=? merge([], X2, X2)", fontsize=16, style=filled, fillcolor=lightyellow];
45 [label="45: merge(T7, [], T3), SCOPE: 1, CLAUSE: 3\n\nT7 is ground\nX2 is free\nmerge(T7, [], T3) !=? merge([], X2, X2)", fontsize=16, style=filled, fillcolor=lightyellow];
46 [label="46: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
49 [label="49: ','(leq(T17, T19), merge(T18, .(T19, T20), T22)) | merge(.(T17, T18), .(T19, T20), T3), SCOPE: 1, CLAUSE: 3\n\nT17 is ground\nT18 is ground\nT19 is ground\nT20 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
51 [label="51: merge(T1, T2, T3), SCOPE: 1, CLAUSE: 3\n\nT1 is ground\nT2 is ground\nX2 is free\nX26 is free\nX42 is free\nX43 is free\nX44 is free\nX45 is free\nX46 is free\nmerge(T1, T2, T3) !=? merge([], X2, X2)\nmerge(T1, T2, T3) !=? merge(X26, [], X26)\nmerge(T1, T2, T3) !=? merge(.(X42, X43), .(X44, X45), .(X42, X46))", fontsize=16, style=filled, fillcolor=lightyellow];
53 [label="53: ','(leq(T17, T19), merge(T18, .(T19, T20), T22)), SCOPE: 2, CLAUSE: 6 | ','(leq(T17, T19), merge(T18, .(T19, T20), T22)), SCOPE: 2, CLAUSE: 7 | ','(leq(T17, T19), merge(T18, .(T19, T20), T22)), SCOPE: 2, CLAUSE: 8 | ?_2 | merge(.(T17, T18), .(T19, T20), T3), SCOPE: 1, CLAUSE: 3\n\nT17 is ground\nT18 is ground\nT19 is ground\nT20 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
54 [label="54: ','(leq(T17, T19), merge(T18, .(T19, T20), T22)), SCOPE: 2, CLAUSE: 6\n\nT17 is ground\nT18 is ground\nT19 is ground\nT20 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
55 [label="55: ','(leq(T17, T19), merge(T18, .(T19, T20), T22)), SCOPE: 2, CLAUSE: 7 | ','(leq(T17, T19), merge(T18, .(T19, T20), T22)), SCOPE: 2, CLAUSE: 8 | ?_2 | merge(.(T17, T18), .(T19, T20), T3), SCOPE: 1, CLAUSE: 3\n\nT17 is ground\nT18 is ground\nT19 is ground\nT20 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
57 [label="57: merge(T18, .(0, T20), T22)\n\nT18 is ground\nT20 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
59 [label="59: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
66 [label="66: ','(leq(T17, T19), merge(T18, .(T19, T20), T22)), SCOPE: 2, CLAUSE: 7\n\nT17 is ground\nT18 is ground\nT19 is ground\nT20 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
69 [label="69: ','(leq(T17, T19), merge(T18, .(T19, T20), T22)), SCOPE: 2, CLAUSE: 8 | ?_2 | merge(.(T17, T18), .(T19, T20), T3), SCOPE: 1, CLAUSE: 3\n\nT17 is ground\nT18 is ground\nT19 is ground\nT20 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
73 [label="73: merge(T18, .(s(0), T20), T22)\n\nT18 is ground\nT20 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
75 [label="75: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
79 [label="79: ','(leq(T17, T19), merge(T18, .(T19, T20), T22)), SCOPE: 2, CLAUSE: 8\n\nT17 is ground\nT18 is ground\nT19 is ground\nT20 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
80 [label="80: ?_2 | merge(.(T17, T18), .(T19, T20), T3), SCOPE: 1, CLAUSE: 3\n\nT17 is ground\nT18 is ground\nT19 is ground\nT20 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
86 [label="B: ','(leq(T35, T36), merge(T18, .(s(T36), T20), T22))\n\nT18 is ground\nT20 is ground\nT35 is ground\nT36 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
87 [label="87: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
90 [label="E: leq(T35, T36)\n\nT35 is ground\nT36 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
91 [label="91: merge(T18, .(s(T36), T20), T22)\n\nT18 is ground\nT20 is ground\nT36 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
94 [label="94: leq(T35, T36), SCOPE: 3, CLAUSE: 6 | leq(T35, T36), SCOPE: 3, CLAUSE: 7 | leq(T35, T36), SCOPE: 3, CLAUSE: 8\n\nT35 is ground\nT36 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
95 [label="95: leq(T35, T36), SCOPE: 3, CLAUSE: 6\n\nT35 is ground\nT36 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
96 [label="96: leq(T35, T36), SCOPE: 3, CLAUSE: 7 | leq(T35, T36), SCOPE: 3, CLAUSE: 8\n\nT35 is ground\nT36 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: leq(T35, T36), SCOPE: 3, CLAUSE: 7\n\nT35 is ground\nT36 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
101 [label="101: leq(T35, T36), SCOPE: 3, CLAUSE: 8\n\nT35 is ground\nT36 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
102 [label="102: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
103 [label="103: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
104 [label="104: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
109 [label="109: leq(T41, T42)\n\nT41 is ground\nT42 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
112 [label="112: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
123 [label="123: merge(.(T17, T18), .(T19, T20), T3), SCOPE: 1, CLAUSE: 3\n\nT17 is ground\nT18 is ground\nT19 is ground\nT20 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
139 [label="C: ','(less(T59, T57), merge(.(T57, T58), T60, T62))\n\nT57 is ground\nT58 is ground\nT59 is ground\nT60 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
140 [label="140: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
142 [label="F: less(T59, T57)\n\nT57 is ground\nT59 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
143 [label="143: merge(.(T57, T58), T60, T62)\n\nT57 is ground\nT58 is ground\nT60 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
144 [label="144: less(T59, T57), SCOPE: 4, CLAUSE: 4 | less(T59, T57), SCOPE: 4, CLAUSE: 5\n\nT57 is ground\nT59 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
145 [label="145: less(T59, T57), SCOPE: 4, CLAUSE: 4\n\nT57 is ground\nT59 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
146 [label="146: less(T59, T57), SCOPE: 4, CLAUSE: 5\n\nT57 is ground\nT59 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
147 [label="147: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
148 [label="148: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
149 [label="149: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
152 [label="152: less(T67, T68)\n\nT67 is ground\nT68 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
153 [label="153: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
162 [label="162: ','(less(T76, T74), merge(.(T74, T75), T77, T79))\n\nT74 is ground\nT75 is ground\nT76 is ground\nT77 is ground\nX42 is free\nX43 is free\nX44 is free\nX45 is free\nX46 is free\nmerge(.(T74, T75), .(T76, T77), T3) !=? merge(.(X42, X43), .(X44, X45), .(X42, X46))", fontsize=16, style=filled, fillcolor=lightyellow];
163 [label="163: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
164 [label="164: ','(less(T76, T74), merge(.(T74, T75), T77, T79)), SCOPE: 5, CLAUSE: 4 | ','(less(T76, T74), merge(.(T74, T75), T77, T79)), SCOPE: 5, CLAUSE: 5\n\nT74 is ground\nT75 is ground\nT76 is ground\nT77 is ground\nX42 is free\nX43 is free\nX44 is free\nX45 is free\nX46 is free\nmerge(.(T74, T75), .(T76, T77), T3) !=? merge(.(X42, X43), .(X44, X45), .(X42, X46))", fontsize=16, style=filled, fillcolor=lightyellow];
165 [label="165: ','(less(T76, T74), merge(.(T74, T75), T77, T79)), SCOPE: 5, CLAUSE: 4\n\nT74 is ground\nT75 is ground\nT76 is ground\nT77 is ground\nX42 is free\nX43 is free\nX44 is free\nX45 is free\nX46 is free\nmerge(.(T74, T75), .(T76, T77), T3) !=? merge(.(X42, X43), .(X44, X45), .(X42, X46))", fontsize=16, style=filled, fillcolor=lightyellow];
166 [label="166: ','(less(T76, T74), merge(.(T74, T75), T77, T79)), SCOPE: 5, CLAUSE: 5\n\nT74 is ground\nT75 is ground\nT76 is ground\nT77 is ground\nX42 is free\nX43 is free\nX44 is free\nX45 is free\nX46 is free\nmerge(.(T74, T75), .(T76, T77), T3) !=? merge(.(X42, X43), .(X44, X45), .(X42, X46))", fontsize=16, style=filled, fillcolor=lightyellow];
169 [label="169: merge(.(s(0), T75), T77, T79)\n\nT75 is ground\nT77 is ground\nX42 is free\nX43 is free\nX44 is free\nX45 is free\nX46 is free\nmerge(.(s(0), T75), .(0, T77), T3) !=? merge(.(X42, X43), .(X44, X45), .(X42, X46))", fontsize=16, style=filled, fillcolor=lightyellow];
170 [label="170: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
171 [label="D: ','(less(T84, T85), merge(.(s(T85), T75), T77, T79))\n\nT75 is ground\nT77 is ground\nT84 is ground\nT85 is ground\nX42 is free\nX43 is free\nX44 is free\nX45 is free\nX46 is free\nmerge(.(s(T85), T75), .(s(T84), T77), T3) !=? merge(.(X42, X43), .(X44, X45), .(X42, X46))", fontsize=16, style=filled, fillcolor=lightyellow];
172 [label="172: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
173 [label="173: less(T84, T85)\n\nT75 is ground\nT77 is ground\nT84 is ground\nT85 is ground\nX42 is free\nX43 is free\nX44 is free\nX45 is free\nX46 is free\nmerge(.(s(T85), T75), .(s(T84), T77), T3) !=? merge(.(X42, X43), .(X44, X45), .(X42, X46))", fontsize=16, style=filled, fillcolor=lightyellow];
174 [label="174: merge(.(s(T85), T75), T77, T79)\n\nT75 is ground\nT77 is ground\nT84 is ground\nT85 is ground\nX42 is free\nX43 is free\nX44 is free\nX45 is free\nX46 is free\nmerge(.(s(T85), T75), .(s(T84), T77), T3) !=? merge(.(X42, X43), .(X44, X45), .(X42, X46))", fontsize=16, style=filled, fillcolor=lightyellow];
175 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
2 -> 175 [arrowhead = none ];
175 -> 4;

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

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

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

179 [label="EVAL with clause\nmerge(X26, [], X26).\nand substitutionT1 -> T7,\nX26 -> T7,\nT2 -> [],\nT3 -> T7", fontsize=14, style = filled, fillcolor = lightblue];
13 -> 179 [arrowhead = none ];
179 -> 39;

180 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
13 -> 180 [arrowhead = none ];
180 -> 41;

181 [label="EVAL with clause\nmerge(X4, [], X4).\nand substitutionX4 -> [],\nT5 -> [],\nT3 -> []", fontsize=14, style = filled, fillcolor = lightblue];
16 -> 181 [arrowhead = none ];
181 -> 18;

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

183 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
18 -> 183 [arrowhead = none ];
183 -> 24;

184 [label="BACKTRACK\nfor clause: merge(.(X, Xs), .(Y, Ys), .(X, Zs)) :- ','(leq(X, Y), merge(Xs, .(Y, Ys), Zs))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
22 -> 184 [arrowhead = none ];
184 -> 33;

185 [label="BACKTRACK\nfor clause: merge(.(X, Xs), .(Y, Ys), .(X, Zs)) :- ','(leq(X, Y), merge(Xs, .(Y, Ys), Zs))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
24 -> 185 [arrowhead = none ];
185 -> 26;

186 [label="BACKTRACK\nfor clause: merge(.(X, Xs), .(Y, Ys), .(Y, Zs)) :- ','(less(Y, X), merge(.(X, Xs), Ys, Zs))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
26 -> 186 [arrowhead = none ];
186 -> 31;

187 [label="BACKTRACK\nfor clause: merge(.(X, Xs), .(Y, Ys), .(Y, Zs)) :- ','(less(Y, X), merge(.(X, Xs), Ys, Zs))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
33 -> 187 [arrowhead = none ];
187 -> 35;

188 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
39 -> 188 [arrowhead = none ];
188 -> 42;

189 [label="EVAL with clause\nmerge(.(X42, X43), .(X44, X45), .(X42, X46)) :- ','(leq(X42, X44), merge(X43, .(X44, X45), X46)).\nand substitutionX42 -> T17,\nX43 -> T18,\nT1 -> .(T17, T18),\nX44 -> T19,\nX45 -> T20,\nT2 -> .(T19, T20),\nX46 -> T22,\nT3 -> .(T17, T22),\nT21 -> T22", fontsize=14, style = filled, fillcolor = lightblue];
41 -> 189 [arrowhead = none ];
189 -> 49;

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

191 [label="BACKTRACK\nfor clause: merge(.(X, Xs), .(Y, Ys), .(X, Zs)) :- ','(leq(X, Y), merge(Xs, .(Y, Ys), Zs))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
42 -> 191 [arrowhead = none ];
191 -> 45;

192 [label="BACKTRACK\nfor clause: merge(.(X, Xs), .(Y, Ys), .(Y, Zs)) :- ','(less(Y, X), merge(.(X, Xs), Ys, Zs))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
45 -> 192 [arrowhead = none ];
192 -> 46;

193 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
49 -> 193 [arrowhead = none ];
193 -> 53;

194 [label="EVAL with clause\nmerge(.(X97, X98), .(X99, X100), .(X99, X101)) :- ','(less(X99, X97), merge(.(X97, X98), X100, X101)).\nand substitutionX97 -> T74,\nX98 -> T75,\nT1 -> .(T74, T75),\nX99 -> T76,\nX100 -> T77,\nT2 -> .(T76, T77),\nX101 -> T79,\nT3 -> .(T76, T79),\nT78 -> T79", fontsize=14, style = filled, fillcolor = lightblue];
51 -> 194 [arrowhead = none ];
194 -> 162;

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

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

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

198 [label="EVAL with clause\nleq(0, 0).\nand substitutionT17 -> 0,\nT19 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
54 -> 198 [arrowhead = none ];
198 -> 57;

199 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
54 -> 199 [arrowhead = none ];
199 -> 59;

200 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
55 -> 200 [arrowhead = none ];
200 -> 66;

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

202 [label="INSTANCE with matching:\nT1 -> T18\nT2 -> .(0, T20)\nT3 -> T22", fontsize=14, style = filled, fillcolor = lightgrey];
57 -> 202 [arrowhead = none , style=dashed];
202 -> 2[style=dashed];

203 [label="EVAL with clause\nleq(0, s(0)).\nand substitutionT17 -> 0,\nT19 -> s(0)", fontsize=14, style = filled, fillcolor = lightblue];
66 -> 203 [arrowhead = none ];
203 -> 73;

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

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

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

207 [label="INSTANCE with matching:\nT1 -> T18\nT2 -> .(s(0), T20)\nT3 -> T22", fontsize=14, style = filled, fillcolor = lightgrey];
73 -> 207 [arrowhead = none , style=dashed];
207 -> 2[style=dashed];

208 [label="EVAL with clause\nleq(s(X59), s(X60)) :- leq(X59, X60).\nand substitutionX59 -> T35,\nT17 -> s(T35),\nX60 -> T36,\nT19 -> s(T36)", fontsize=14, style = filled, fillcolor = lightblue];
79 -> 208 [arrowhead = none ];
208 -> 86;

209 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
79 -> 209 [arrowhead = none ];
209 -> 87;

210 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
80 -> 210 [arrowhead = none ];
210 -> 123;

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

212 [label="SPLIT 2\nnew knowledge:\nT35 is ground\nT36 is ground", fontsize=14, style = filled, fillcolor = violet];
86 -> 212 [arrowhead = none ];
212 -> 91;

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

214 [label="INSTANCE with matching:\nT1 -> T18\nT2 -> .(s(T36), T20)\nT3 -> T22", fontsize=14, style = filled, fillcolor = lightgrey];
91 -> 214 [arrowhead = none , style=dashed];
214 -> 2[style=dashed];

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

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

217 [label="EVAL with clause\nleq(0, 0).\nand substitutionT35 -> 0,\nT36 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
95 -> 217 [arrowhead = none ];
217 -> 97;

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

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

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

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

222 [label="EVAL with clause\nleq(0, s(0)).\nand substitutionT35 -> 0,\nT36 -> s(0)", fontsize=14, style = filled, fillcolor = lightblue];
100 -> 222 [arrowhead = none ];
222 -> 102;

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

224 [label="EVAL with clause\nleq(s(X65), s(X66)) :- leq(X65, X66).\nand substitutionX65 -> T41,\nT35 -> s(T41),\nX66 -> T42,\nT36 -> s(T42)", fontsize=14, style = filled, fillcolor = lightblue];
101 -> 224 [arrowhead = none ];
224 -> 109;

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

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

227 [label="INSTANCE with matching:\nT35 -> T41\nT36 -> T42", fontsize=14, style = filled, fillcolor = lightgrey];
109 -> 227 [arrowhead = none , style=dashed];
227 -> 90[style=dashed];

228 [label="EVAL with clause\nmerge(.(X79, X80), .(X81, X82), .(X81, X83)) :- ','(less(X81, X79), merge(.(X79, X80), X82, X83)).\nand substitutionT17 -> T57,\nX79 -> T57,\nT18 -> T58,\nX80 -> T58,\nT19 -> T59,\nX81 -> T59,\nT20 -> T60,\nX82 -> T60,\nX83 -> T62,\nT3 -> .(T59, T62),\nT61 -> T62", fontsize=14, style = filled, fillcolor = lightblue];
123 -> 228 [arrowhead = none ];
228 -> 139;

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

230 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
139 -> 230 [arrowhead = none ];
230 -> 142;

231 [label="SPLIT 2\nnew knowledge:\nT59 is ground\nT57 is ground", fontsize=14, style = filled, fillcolor = violet];
139 -> 231 [arrowhead = none ];
231 -> 143;

232 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
142 -> 232 [arrowhead = none ];
232 -> 144;

233 [label="INSTANCE with matching:\nT1 -> .(T57, T58)\nT2 -> T60\nT3 -> T62", fontsize=14, style = filled, fillcolor = lightgrey];
143 -> 233 [arrowhead = none , style=dashed];
233 -> 2[style=dashed];

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

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

236 [label="EVAL with clause\nless(0, s(0)).\nand substitutionT59 -> 0,\nT57 -> s(0)", fontsize=14, style = filled, fillcolor = lightblue];
145 -> 236 [arrowhead = none ];
236 -> 147;

237 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
145 -> 237 [arrowhead = none ];
237 -> 148;

238 [label="EVAL with clause\nless(s(X88), s(X89)) :- less(X88, X89).\nand substitutionX88 -> T67,\nT59 -> s(T67),\nX89 -> T68,\nT57 -> s(T68)", fontsize=14, style = filled, fillcolor = lightblue];
146 -> 238 [arrowhead = none ];
238 -> 152;

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

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

241 [label="INSTANCE with matching:\nT59 -> T67\nT57 -> T68", fontsize=14, style = filled, fillcolor = lightgrey];
152 -> 241 [arrowhead = none , style=dashed];
241 -> 142[style=dashed];

242 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
162 -> 242 [arrowhead = none ];
242 -> 164;

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

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

245 [label="EVAL with clause\nless(0, s(0)).\nand substitutionT76 -> 0,\nT74 -> s(0)", fontsize=14, style = filled, fillcolor = lightblue];
165 -> 245 [arrowhead = none ];
245 -> 169;

246 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
165 -> 246 [arrowhead = none ];
246 -> 170;

247 [label="EVAL with clause\nless(s(X108), s(X109)) :- less(X108, X109).\nand substitutionX108 -> T84,\nT76 -> s(T84),\nX109 -> T85,\nT74 -> s(T85)", fontsize=14, style = filled, fillcolor = lightblue];
166 -> 247 [arrowhead = none ];
247 -> 171;

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

249 [label="INSTANCE with matching:\nT1 -> .(s(0), T75)\nT2 -> T77\nT3 -> T79", fontsize=14, style = filled, fillcolor = lightgrey];
169 -> 249 [arrowhead = none , style=dashed];
249 -> 2[style=dashed];

250 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
171 -> 250 [arrowhead = none ];
250 -> 173;

251 [label="SPLIT 2\nnew knowledge:\nT84 is ground\nT85 is ground", fontsize=14, style = filled, fillcolor = violet];
171 -> 251 [arrowhead = none ];
251 -> 174;

252 [label="INSTANCE with matching:\nT59 -> T84\nT57 -> T85", fontsize=14, style = filled, fillcolor = lightgrey];
173 -> 252 [arrowhead = none , style=dashed];
252 -> 142[style=dashed];

253 [label="INSTANCE with matching:\nT1 -> .(s(T85), T75)\nT2 -> T77\nT3 -> T79", fontsize=14, style = filled, fillcolor = lightgrey];
174 -> 253 [arrowhead = none , style=dashed];
253 -> 2[style=dashed];

}

(2) Obligation:

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

mergeA_in_gga([], T5, T5) → mergeA_out_gga([], T5, T5)
mergeA_in_gga([], [], []) → mergeA_out_gga([], [], [])
mergeA_in_gga(T7, [], T7) → mergeA_out_gga(T7, [], T7)
mergeA_in_gga(.(0, T18), .(0, T20), .(0, T22)) → U1_gga(T18, T20, T22, mergeA_in_gga(T18, .(0, T20), T22))
mergeA_in_gga(.(0, T18), .(s(0), T20), .(0, T22)) → U2_gga(T18, T20, T22, mergeA_in_gga(T18, .(s(0), T20), T22))
mergeA_in_gga(.(s(T35), T18), .(s(T36), T20), .(s(T35), T22)) → U3_gga(T35, T18, T36, T20, T22, pB_in_gggga(T35, T36, T18, T20, T22))
pB_in_gggga(T35, T36, T18, T20, T22) → U9_gggga(T35, T36, T18, T20, T22, leqE_in_gg(T35, T36))
leqE_in_gg(0, 0) → leqE_out_gg(0, 0)
leqE_in_gg(0, s(0)) → leqE_out_gg(0, s(0))
leqE_in_gg(s(T41), s(T42)) → U7_gg(T41, T42, leqE_in_gg(T41, T42))
U7_gg(T41, T42, leqE_out_gg(T41, T42)) → leqE_out_gg(s(T41), s(T42))
U9_gggga(T35, T36, T18, T20, T22, leqE_out_gg(T35, T36)) → U10_gggga(T35, T36, T18, T20, T22, mergeA_in_gga(T18, .(s(T36), T20), T22))
mergeA_in_gga(.(T57, T58), .(T59, T60), .(T59, T62)) → U4_gga(T57, T58, T59, T60, T62, pC_in_gggga(T59, T57, T58, T60, T62))
pC_in_gggga(T59, T57, T58, T60, T62) → U11_gggga(T59, T57, T58, T60, T62, lessF_in_gg(T59, T57))
lessF_in_gg(0, s(0)) → lessF_out_gg(0, s(0))
lessF_in_gg(s(T67), s(T68)) → U8_gg(T67, T68, lessF_in_gg(T67, T68))
U8_gg(T67, T68, lessF_out_gg(T67, T68)) → lessF_out_gg(s(T67), s(T68))
U11_gggga(T59, T57, T58, T60, T62, lessF_out_gg(T59, T57)) → U12_gggga(T59, T57, T58, T60, T62, mergeA_in_gga(.(T57, T58), T60, T62))
mergeA_in_gga(.(s(0), T75), .(0, T77), .(0, T79)) → U5_gga(T75, T77, T79, mergeA_in_gga(.(s(0), T75), T77, T79))
mergeA_in_gga(.(s(T85), T75), .(s(T84), T77), .(s(T84), T79)) → U6_gga(T85, T75, T84, T77, T79, pD_in_gggga(T84, T85, T75, T77, T79))
pD_in_gggga(T84, T85, T75, T77, T79) → U13_gggga(T84, T85, T75, T77, T79, lessF_in_gg(T84, T85))
U13_gggga(T84, T85, T75, T77, T79, lessF_out_gg(T84, T85)) → U14_gggga(T84, T85, T75, T77, T79, mergeA_in_gga(.(s(T85), T75), T77, T79))
U14_gggga(T84, T85, T75, T77, T79, mergeA_out_gga(.(s(T85), T75), T77, T79)) → pD_out_gggga(T84, T85, T75, T77, T79)
U6_gga(T85, T75, T84, T77, T79, pD_out_gggga(T84, T85, T75, T77, T79)) → mergeA_out_gga(.(s(T85), T75), .(s(T84), T77), .(s(T84), T79))
U5_gga(T75, T77, T79, mergeA_out_gga(.(s(0), T75), T77, T79)) → mergeA_out_gga(.(s(0), T75), .(0, T77), .(0, T79))
U12_gggga(T59, T57, T58, T60, T62, mergeA_out_gga(.(T57, T58), T60, T62)) → pC_out_gggga(T59, T57, T58, T60, T62)
U4_gga(T57, T58, T59, T60, T62, pC_out_gggga(T59, T57, T58, T60, T62)) → mergeA_out_gga(.(T57, T58), .(T59, T60), .(T59, T62))
U10_gggga(T35, T36, T18, T20, T22, mergeA_out_gga(T18, .(s(T36), T20), T22)) → pB_out_gggga(T35, T36, T18, T20, T22)
U3_gga(T35, T18, T36, T20, T22, pB_out_gggga(T35, T36, T18, T20, T22)) → mergeA_out_gga(.(s(T35), T18), .(s(T36), T20), .(s(T35), T22))
U2_gga(T18, T20, T22, mergeA_out_gga(T18, .(s(0), T20), T22)) → mergeA_out_gga(.(0, T18), .(s(0), T20), .(0, T22))
U1_gga(T18, T20, T22, mergeA_out_gga(T18, .(0, T20), T22)) → mergeA_out_gga(.(0, T18), .(0, T20), .(0, T22))

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

MERGEA_IN_GGA(.(0, T18), .(0, T20), .(0, T22)) → U1_GGA(T18, T20, T22, mergeA_in_gga(T18, .(0, T20), T22))
MERGEA_IN_GGA(.(0, T18), .(0, T20), .(0, T22)) → MERGEA_IN_GGA(T18, .(0, T20), T22)
MERGEA_IN_GGA(.(0, T18), .(s(0), T20), .(0, T22)) → U2_GGA(T18, T20, T22, mergeA_in_gga(T18, .(s(0), T20), T22))
MERGEA_IN_GGA(.(0, T18), .(s(0), T20), .(0, T22)) → MERGEA_IN_GGA(T18, .(s(0), T20), T22)
MERGEA_IN_GGA(.(s(T35), T18), .(s(T36), T20), .(s(T35), T22)) → U3_GGA(T35, T18, T36, T20, T22, pB_in_gggga(T35, T36, T18, T20, T22))
MERGEA_IN_GGA(.(s(T35), T18), .(s(T36), T20), .(s(T35), T22)) → PB_IN_GGGGA(T35, T36, T18, T20, T22)
PB_IN_GGGGA(T35, T36, T18, T20, T22) → U9_GGGGA(T35, T36, T18, T20, T22, leqE_in_gg(T35, T36))
PB_IN_GGGGA(T35, T36, T18, T20, T22) → LEQE_IN_GG(T35, T36)
LEQE_IN_GG(s(T41), s(T42)) → U7_GG(T41, T42, leqE_in_gg(T41, T42))
LEQE_IN_GG(s(T41), s(T42)) → LEQE_IN_GG(T41, T42)
U9_GGGGA(T35, T36, T18, T20, T22, leqE_out_gg(T35, T36)) → U10_GGGGA(T35, T36, T18, T20, T22, mergeA_in_gga(T18, .(s(T36), T20), T22))
U9_GGGGA(T35, T36, T18, T20, T22, leqE_out_gg(T35, T36)) → MERGEA_IN_GGA(T18, .(s(T36), T20), T22)
MERGEA_IN_GGA(.(T57, T58), .(T59, T60), .(T59, T62)) → U4_GGA(T57, T58, T59, T60, T62, pC_in_gggga(T59, T57, T58, T60, T62))
MERGEA_IN_GGA(.(T57, T58), .(T59, T60), .(T59, T62)) → PC_IN_GGGGA(T59, T57, T58, T60, T62)
PC_IN_GGGGA(T59, T57, T58, T60, T62) → U11_GGGGA(T59, T57, T58, T60, T62, lessF_in_gg(T59, T57))
PC_IN_GGGGA(T59, T57, T58, T60, T62) → LESSF_IN_GG(T59, T57)
LESSF_IN_GG(s(T67), s(T68)) → U8_GG(T67, T68, lessF_in_gg(T67, T68))
LESSF_IN_GG(s(T67), s(T68)) → LESSF_IN_GG(T67, T68)
U11_GGGGA(T59, T57, T58, T60, T62, lessF_out_gg(T59, T57)) → U12_GGGGA(T59, T57, T58, T60, T62, mergeA_in_gga(.(T57, T58), T60, T62))
U11_GGGGA(T59, T57, T58, T60, T62, lessF_out_gg(T59, T57)) → MERGEA_IN_GGA(.(T57, T58), T60, T62)
MERGEA_IN_GGA(.(s(0), T75), .(0, T77), .(0, T79)) → U5_GGA(T75, T77, T79, mergeA_in_gga(.(s(0), T75), T77, T79))
MERGEA_IN_GGA(.(s(0), T75), .(0, T77), .(0, T79)) → MERGEA_IN_GGA(.(s(0), T75), T77, T79)
MERGEA_IN_GGA(.(s(T85), T75), .(s(T84), T77), .(s(T84), T79)) → U6_GGA(T85, T75, T84, T77, T79, pD_in_gggga(T84, T85, T75, T77, T79))
MERGEA_IN_GGA(.(s(T85), T75), .(s(T84), T77), .(s(T84), T79)) → PD_IN_GGGGA(T84, T85, T75, T77, T79)
PD_IN_GGGGA(T84, T85, T75, T77, T79) → U13_GGGGA(T84, T85, T75, T77, T79, lessF_in_gg(T84, T85))
PD_IN_GGGGA(T84, T85, T75, T77, T79) → LESSF_IN_GG(T84, T85)
U13_GGGGA(T84, T85, T75, T77, T79, lessF_out_gg(T84, T85)) → U14_GGGGA(T84, T85, T75, T77, T79, mergeA_in_gga(.(s(T85), T75), T77, T79))
U13_GGGGA(T84, T85, T75, T77, T79, lessF_out_gg(T84, T85)) → MERGEA_IN_GGA(.(s(T85), T75), T77, T79)

The TRS R consists of the following rules:

mergeA_in_gga([], T5, T5) → mergeA_out_gga([], T5, T5)
mergeA_in_gga([], [], []) → mergeA_out_gga([], [], [])
mergeA_in_gga(T7, [], T7) → mergeA_out_gga(T7, [], T7)
mergeA_in_gga(.(0, T18), .(0, T20), .(0, T22)) → U1_gga(T18, T20, T22, mergeA_in_gga(T18, .(0, T20), T22))
mergeA_in_gga(.(0, T18), .(s(0), T20), .(0, T22)) → U2_gga(T18, T20, T22, mergeA_in_gga(T18, .(s(0), T20), T22))
mergeA_in_gga(.(s(T35), T18), .(s(T36), T20), .(s(T35), T22)) → U3_gga(T35, T18, T36, T20, T22, pB_in_gggga(T35, T36, T18, T20, T22))
pB_in_gggga(T35, T36, T18, T20, T22) → U9_gggga(T35, T36, T18, T20, T22, leqE_in_gg(T35, T36))
leqE_in_gg(0, 0) → leqE_out_gg(0, 0)
leqE_in_gg(0, s(0)) → leqE_out_gg(0, s(0))
leqE_in_gg(s(T41), s(T42)) → U7_gg(T41, T42, leqE_in_gg(T41, T42))
U7_gg(T41, T42, leqE_out_gg(T41, T42)) → leqE_out_gg(s(T41), s(T42))
U9_gggga(T35, T36, T18, T20, T22, leqE_out_gg(T35, T36)) → U10_gggga(T35, T36, T18, T20, T22, mergeA_in_gga(T18, .(s(T36), T20), T22))
mergeA_in_gga(.(T57, T58), .(T59, T60), .(T59, T62)) → U4_gga(T57, T58, T59, T60, T62, pC_in_gggga(T59, T57, T58, T60, T62))
pC_in_gggga(T59, T57, T58, T60, T62) → U11_gggga(T59, T57, T58, T60, T62, lessF_in_gg(T59, T57))
lessF_in_gg(0, s(0)) → lessF_out_gg(0, s(0))
lessF_in_gg(s(T67), s(T68)) → U8_gg(T67, T68, lessF_in_gg(T67, T68))
U8_gg(T67, T68, lessF_out_gg(T67, T68)) → lessF_out_gg(s(T67), s(T68))
U11_gggga(T59, T57, T58, T60, T62, lessF_out_gg(T59, T57)) → U12_gggga(T59, T57, T58, T60, T62, mergeA_in_gga(.(T57, T58), T60, T62))
mergeA_in_gga(.(s(0), T75), .(0, T77), .(0, T79)) → U5_gga(T75, T77, T79, mergeA_in_gga(.(s(0), T75), T77, T79))
mergeA_in_gga(.(s(T85), T75), .(s(T84), T77), .(s(T84), T79)) → U6_gga(T85, T75, T84, T77, T79, pD_in_gggga(T84, T85, T75, T77, T79))
pD_in_gggga(T84, T85, T75, T77, T79) → U13_gggga(T84, T85, T75, T77, T79, lessF_in_gg(T84, T85))
U13_gggga(T84, T85, T75, T77, T79, lessF_out_gg(T84, T85)) → U14_gggga(T84, T85, T75, T77, T79, mergeA_in_gga(.(s(T85), T75), T77, T79))
U14_gggga(T84, T85, T75, T77, T79, mergeA_out_gga(.(s(T85), T75), T77, T79)) → pD_out_gggga(T84, T85, T75, T77, T79)
U6_gga(T85, T75, T84, T77, T79, pD_out_gggga(T84, T85, T75, T77, T79)) → mergeA_out_gga(.(s(T85), T75), .(s(T84), T77), .(s(T84), T79))
U5_gga(T75, T77, T79, mergeA_out_gga(.(s(0), T75), T77, T79)) → mergeA_out_gga(.(s(0), T75), .(0, T77), .(0, T79))
U12_gggga(T59, T57, T58, T60, T62, mergeA_out_gga(.(T57, T58), T60, T62)) → pC_out_gggga(T59, T57, T58, T60, T62)
U4_gga(T57, T58, T59, T60, T62, pC_out_gggga(T59, T57, T58, T60, T62)) → mergeA_out_gga(.(T57, T58), .(T59, T60), .(T59, T62))
U10_gggga(T35, T36, T18, T20, T22, mergeA_out_gga(T18, .(s(T36), T20), T22)) → pB_out_gggga(T35, T36, T18, T20, T22)
U3_gga(T35, T18, T36, T20, T22, pB_out_gggga(T35, T36, T18, T20, T22)) → mergeA_out_gga(.(s(T35), T18), .(s(T36), T20), .(s(T35), T22))
U2_gga(T18, T20, T22, mergeA_out_gga(T18, .(s(0), T20), T22)) → mergeA_out_gga(.(0, T18), .(s(0), T20), .(0, T22))
U1_gga(T18, T20, T22, mergeA_out_gga(T18, .(0, T20), T22)) → mergeA_out_gga(.(0, T18), .(0, T20), .(0, T22))

The argument filtering Pi contains the following mapping:
mergeA_in_gga(x1, x2, x3) = mergeA_in_gga(x1, x2)
[] = []
mergeA_out_gga(x1, x2, x3) = mergeA_out_gga(x1, x2, x3)
.(x1, x2) = .(x1, x2)
0 = 0
U1_gga(x1, x2, x3, x4) = U1_gga(x1, x2, x4)
s(x1) = s(x1)
U2_gga(x1, x2, x3, x4) = U2_gga(x1, x2, x4)
U3_gga(x1, x2, x3, x4, x5, x6) = U3_gga(x1, x2, x3, x4, x6)
pB_in_gggga(x1, x2, x3, x4, x5) = pB_in_gggga(x1, x2, x3, x4)
U9_gggga(x1, x2, x3, x4, x5, x6) = U9_gggga(x1, x2, x3, x4, x6)
leqE_in_gg(x1, x2) = leqE_in_gg(x1, x2)
leqE_out_gg(x1, x2) = leqE_out_gg(x1, x2)
U7_gg(x1, x2, x3) = U7_gg(x1, x2, x3)
U10_gggga(x1, x2, x3, x4, x5, x6) = U10_gggga(x1, x2, x3, x4, x6)
U4_gga(x1, x2, x3, x4, x5, x6) = U4_gga(x1, x2, x3, x4, x6)
pC_in_gggga(x1, x2, x3, x4, x5) = pC_in_gggga(x1, x2, x3, x4)
U11_gggga(x1, x2, x3, x4, x5, x6) = U11_gggga(x1, x2, x3, x4, x6)
lessF_in_gg(x1, x2) = lessF_in_gg(x1, x2)
lessF_out_gg(x1, x2) = lessF_out_gg(x1, x2)
U8_gg(x1, x2, x3) = U8_gg(x1, x2, x3)
U12_gggga(x1, x2, x3, x4, x5, x6) = U12_gggga(x1, x2, x3, x4, x6)
U5_gga(x1, x2, x3, x4) = U5_gga(x1, x2, x4)
U6_gga(x1, x2, x3, x4, x5, x6) = U6_gga(x1, x2, x3, x4, x6)
pD_in_gggga(x1, x2, x3, x4, x5) = pD_in_gggga(x1, x2, x3, x4)
U13_gggga(x1, x2, x3, x4, x5, x6) = U13_gggga(x1, x2, x3, x4, x6)
U14_gggga(x1, x2, x3, x4, x5, x6) = U14_gggga(x1, x2, x3, x4, x6)
pD_out_gggga(x1, x2, x3, x4, x5) = pD_out_gggga(x1, x2, x3, x4, x5)
pC_out_gggga(x1, x2, x3, x4, x5) = pC_out_gggga(x1, x2, x3, x4, x5)
pB_out_gggga(x1, x2, x3, x4, x5) = pB_out_gggga(x1, x2, x3, x4, x5)
MERGEA_IN_GGA(x1, x2, x3) = MERGEA_IN_GGA(x1, x2)
U1_GGA(x1, x2, x3, x4) = U1_GGA(x1, x2, x4)
U2_GGA(x1, x2, x3, x4) = U2_GGA(x1, x2, x4)
U3_GGA(x1, x2, x3, x4, x5, x6) = U3_GGA(x1, x2, x3, x4, x6)
PB_IN_GGGGA(x1, x2, x3, x4, x5) = PB_IN_GGGGA(x1, x2, x3, x4)
U9_GGGGA(x1, x2, x3, x4, x5, x6) = U9_GGGGA(x1, x2, x3, x4, x6)
LEQE_IN_GG(x1, x2) = LEQE_IN_GG(x1, x2)
U7_GG(x1, x2, x3) = U7_GG(x1, x2, x3)
U10_GGGGA(x1, x2, x3, x4, x5, x6) = U10_GGGGA(x1, x2, x3, x4, x6)
U4_GGA(x1, x2, x3, x4, x5, x6) = U4_GGA(x1, x2, x3, x4, x6)
PC_IN_GGGGA(x1, x2, x3, x4, x5) = PC_IN_GGGGA(x1, x2, x3, x4)
U11_GGGGA(x1, x2, x3, x4, x5, x6) = U11_GGGGA(x1, x2, x3, x4, x6)
LESSF_IN_GG(x1, x2) = LESSF_IN_GG(x1, x2)
U8_GG(x1, x2, x3) = U8_GG(x1, x2, x3)
U12_GGGGA(x1, x2, x3, x4, x5, x6) = U12_GGGGA(x1, x2, x3, x4, x6)
U5_GGA(x1, x2, x3, x4) = U5_GGA(x1, x2, x4)
U6_GGA(x1, x2, x3, x4, x5, x6) = U6_GGA(x1, x2, x3, x4, x6)
PD_IN_GGGGA(x1, x2, x3, x4, x5) = PD_IN_GGGGA(x1, x2, x3, x4)
U13_GGGGA(x1, x2, x3, x4, x5, x6) = U13_GGGGA(x1, x2, x3, x4, x6)
U14_GGGGA(x1, x2, x3, x4, x5, x6) = U14_GGGGA(x1, x2, x3, x4, x6)

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

(4) Obligation:

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

MERGEA_IN_GGA(.(0, T18), .(0, T20), .(0, T22)) → U1_GGA(T18, T20, T22, mergeA_in_gga(T18, .(0, T20), T22))
MERGEA_IN_GGA(.(0, T18), .(0, T20), .(0, T22)) → MERGEA_IN_GGA(T18, .(0, T20), T22)
MERGEA_IN_GGA(.(0, T18), .(s(0), T20), .(0, T22)) → U2_GGA(T18, T20, T22, mergeA_in_gga(T18, .(s(0), T20), T22))
MERGEA_IN_GGA(.(0, T18), .(s(0), T20), .(0, T22)) → MERGEA_IN_GGA(T18, .(s(0), T20), T22)
MERGEA_IN_GGA(.(s(T35), T18), .(s(T36), T20), .(s(T35), T22)) → U3_GGA(T35, T18, T36, T20, T22, pB_in_gggga(T35, T36, T18, T20, T22))
MERGEA_IN_GGA(.(s(T35), T18), .(s(T36), T20), .(s(T35), T22)) → PB_IN_GGGGA(T35, T36, T18, T20, T22)
PB_IN_GGGGA(T35, T36, T18, T20, T22) → U9_GGGGA(T35, T36, T18, T20, T22, leqE_in_gg(T35, T36))
PB_IN_GGGGA(T35, T36, T18, T20, T22) → LEQE_IN_GG(T35, T36)
LEQE_IN_GG(s(T41), s(T42)) → U7_GG(T41, T42, leqE_in_gg(T41, T42))
LEQE_IN_GG(s(T41), s(T42)) → LEQE_IN_GG(T41, T42)
U9_GGGGA(T35, T36, T18, T20, T22, leqE_out_gg(T35, T36)) → U10_GGGGA(T35, T36, T18, T20, T22, mergeA_in_gga(T18, .(s(T36), T20), T22))
U9_GGGGA(T35, T36, T18, T20, T22, leqE_out_gg(T35, T36)) → MERGEA_IN_GGA(T18, .(s(T36), T20), T22)
MERGEA_IN_GGA(.(T57, T58), .(T59, T60), .(T59, T62)) → U4_GGA(T57, T58, T59, T60, T62, pC_in_gggga(T59, T57, T58, T60, T62))
MERGEA_IN_GGA(.(T57, T58), .(T59, T60), .(T59, T62)) → PC_IN_GGGGA(T59, T57, T58, T60, T62)
PC_IN_GGGGA(T59, T57, T58, T60, T62) → U11_GGGGA(T59, T57, T58, T60, T62, lessF_in_gg(T59, T57))
PC_IN_GGGGA(T59, T57, T58, T60, T62) → LESSF_IN_GG(T59, T57)
LESSF_IN_GG(s(T67), s(T68)) → U8_GG(T67, T68, lessF_in_gg(T67, T68))
LESSF_IN_GG(s(T67), s(T68)) → LESSF_IN_GG(T67, T68)
U11_GGGGA(T59, T57, T58, T60, T62, lessF_out_gg(T59, T57)) → U12_GGGGA(T59, T57, T58, T60, T62, mergeA_in_gga(.(T57, T58), T60, T62))
U11_GGGGA(T59, T57, T58, T60, T62, lessF_out_gg(T59, T57)) → MERGEA_IN_GGA(.(T57, T58), T60, T62)
MERGEA_IN_GGA(.(s(0), T75), .(0, T77), .(0, T79)) → U5_GGA(T75, T77, T79, mergeA_in_gga(.(s(0), T75), T77, T79))
MERGEA_IN_GGA(.(s(0), T75), .(0, T77), .(0, T79)) → MERGEA_IN_GGA(.(s(0), T75), T77, T79)
MERGEA_IN_GGA(.(s(T85), T75), .(s(T84), T77), .(s(T84), T79)) → U6_GGA(T85, T75, T84, T77, T79, pD_in_gggga(T84, T85, T75, T77, T79))
MERGEA_IN_GGA(.(s(T85), T75), .(s(T84), T77), .(s(T84), T79)) → PD_IN_GGGGA(T84, T85, T75, T77, T79)
PD_IN_GGGGA(T84, T85, T75, T77, T79) → U13_GGGGA(T84, T85, T75, T77, T79, lessF_in_gg(T84, T85))
PD_IN_GGGGA(T84, T85, T75, T77, T79) → LESSF_IN_GG(T84, T85)
U13_GGGGA(T84, T85, T75, T77, T79, lessF_out_gg(T84, T85)) → U14_GGGGA(T84, T85, T75, T77, T79, mergeA_in_gga(.(s(T85), T75), T77, T79))
U13_GGGGA(T84, T85, T75, T77, T79, lessF_out_gg(T84, T85)) → MERGEA_IN_GGA(.(s(T85), T75), T77, T79)

The TRS R consists of the following rules:

mergeA_in_gga([], T5, T5) → mergeA_out_gga([], T5, T5)
mergeA_in_gga([], [], []) → mergeA_out_gga([], [], [])
mergeA_in_gga(T7, [], T7) → mergeA_out_gga(T7, [], T7)
mergeA_in_gga(.(0, T18), .(0, T20), .(0, T22)) → U1_gga(T18, T20, T22, mergeA_in_gga(T18, .(0, T20), T22))
mergeA_in_gga(.(0, T18), .(s(0), T20), .(0, T22)) → U2_gga(T18, T20, T22, mergeA_in_gga(T18, .(s(0), T20), T22))
mergeA_in_gga(.(s(T35), T18), .(s(T36), T20), .(s(T35), T22)) → U3_gga(T35, T18, T36, T20, T22, pB_in_gggga(T35, T36, T18, T20, T22))
pB_in_gggga(T35, T36, T18, T20, T22) → U9_gggga(T35, T36, T18, T20, T22, leqE_in_gg(T35, T36))
leqE_in_gg(0, 0) → leqE_out_gg(0, 0)
leqE_in_gg(0, s(0)) → leqE_out_gg(0, s(0))
leqE_in_gg(s(T41), s(T42)) → U7_gg(T41, T42, leqE_in_gg(T41, T42))
U7_gg(T41, T42, leqE_out_gg(T41, T42)) → leqE_out_gg(s(T41), s(T42))
U9_gggga(T35, T36, T18, T20, T22, leqE_out_gg(T35, T36)) → U10_gggga(T35, T36, T18, T20, T22, mergeA_in_gga(T18, .(s(T36), T20), T22))
mergeA_in_gga(.(T57, T58), .(T59, T60), .(T59, T62)) → U4_gga(T57, T58, T59, T60, T62, pC_in_gggga(T59, T57, T58, T60, T62))
pC_in_gggga(T59, T57, T58, T60, T62) → U11_gggga(T59, T57, T58, T60, T62, lessF_in_gg(T59, T57))
lessF_in_gg(0, s(0)) → lessF_out_gg(0, s(0))
lessF_in_gg(s(T67), s(T68)) → U8_gg(T67, T68, lessF_in_gg(T67, T68))
U8_gg(T67, T68, lessF_out_gg(T67, T68)) → lessF_out_gg(s(T67), s(T68))
U11_gggga(T59, T57, T58, T60, T62, lessF_out_gg(T59, T57)) → U12_gggga(T59, T57, T58, T60, T62, mergeA_in_gga(.(T57, T58), T60, T62))
mergeA_in_gga(.(s(0), T75), .(0, T77), .(0, T79)) → U5_gga(T75, T77, T79, mergeA_in_gga(.(s(0), T75), T77, T79))
mergeA_in_gga(.(s(T85), T75), .(s(T84), T77), .(s(T84), T79)) → U6_gga(T85, T75, T84, T77, T79, pD_in_gggga(T84, T85, T75, T77, T79))
pD_in_gggga(T84, T85, T75, T77, T79) → U13_gggga(T84, T85, T75, T77, T79, lessF_in_gg(T84, T85))
U13_gggga(T84, T85, T75, T77, T79, lessF_out_gg(T84, T85)) → U14_gggga(T84, T85, T75, T77, T79, mergeA_in_gga(.(s(T85), T75), T77, T79))
U14_gggga(T84, T85, T75, T77, T79, mergeA_out_gga(.(s(T85), T75), T77, T79)) → pD_out_gggga(T84, T85, T75, T77, T79)
U6_gga(T85, T75, T84, T77, T79, pD_out_gggga(T84, T85, T75, T77, T79)) → mergeA_out_gga(.(s(T85), T75), .(s(T84), T77), .(s(T84), T79))
U5_gga(T75, T77, T79, mergeA_out_gga(.(s(0), T75), T77, T79)) → mergeA_out_gga(.(s(0), T75), .(0, T77), .(0, T79))
U12_gggga(T59, T57, T58, T60, T62, mergeA_out_gga(.(T57, T58), T60, T62)) → pC_out_gggga(T59, T57, T58, T60, T62)
U4_gga(T57, T58, T59, T60, T62, pC_out_gggga(T59, T57, T58, T60, T62)) → mergeA_out_gga(.(T57, T58), .(T59, T60), .(T59, T62))
U10_gggga(T35, T36, T18, T20, T22, mergeA_out_gga(T18, .(s(T36), T20), T22)) → pB_out_gggga(T35, T36, T18, T20, T22)
U3_gga(T35, T18, T36, T20, T22, pB_out_gggga(T35, T36, T18, T20, T22)) → mergeA_out_gga(.(s(T35), T18), .(s(T36), T20), .(s(T35), T22))
U2_gga(T18, T20, T22, mergeA_out_gga(T18, .(s(0), T20), T22)) → mergeA_out_gga(.(0, T18), .(s(0), T20), .(0, T22))
U1_gga(T18, T20, T22, mergeA_out_gga(T18, .(0, T20), T22)) → mergeA_out_gga(.(0, T18), .(0, T20), .(0, T22))

(5) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 3 SCCs with 14 less nodes.

(6) Complex Obligation (AND)

(7) Obligation:

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

LESSF_IN_GG(s(T67), s(T68)) → LESSF_IN_GG(T67, T68)

The TRS R consists of the following rules:

mergeA_in_gga([], T5, T5) → mergeA_out_gga([], T5, T5)
mergeA_in_gga([], [], []) → mergeA_out_gga([], [], [])
mergeA_in_gga(T7, [], T7) → mergeA_out_gga(T7, [], T7)
mergeA_in_gga(.(0, T18), .(0, T20), .(0, T22)) → U1_gga(T18, T20, T22, mergeA_in_gga(T18, .(0, T20), T22))
mergeA_in_gga(.(0, T18), .(s(0), T20), .(0, T22)) → U2_gga(T18, T20, T22, mergeA_in_gga(T18, .(s(0), T20), T22))
mergeA_in_gga(.(s(T35), T18), .(s(T36), T20), .(s(T35), T22)) → U3_gga(T35, T18, T36, T20, T22, pB_in_gggga(T35, T36, T18, T20, T22))
pB_in_gggga(T35, T36, T18, T20, T22) → U9_gggga(T35, T36, T18, T20, T22, leqE_in_gg(T35, T36))
leqE_in_gg(0, 0) → leqE_out_gg(0, 0)
leqE_in_gg(0, s(0)) → leqE_out_gg(0, s(0))
leqE_in_gg(s(T41), s(T42)) → U7_gg(T41, T42, leqE_in_gg(T41, T42))
U7_gg(T41, T42, leqE_out_gg(T41, T42)) → leqE_out_gg(s(T41), s(T42))
U9_gggga(T35, T36, T18, T20, T22, leqE_out_gg(T35, T36)) → U10_gggga(T35, T36, T18, T20, T22, mergeA_in_gga(T18, .(s(T36), T20), T22))
mergeA_in_gga(.(T57, T58), .(T59, T60), .(T59, T62)) → U4_gga(T57, T58, T59, T60, T62, pC_in_gggga(T59, T57, T58, T60, T62))
pC_in_gggga(T59, T57, T58, T60, T62) → U11_gggga(T59, T57, T58, T60, T62, lessF_in_gg(T59, T57))
lessF_in_gg(0, s(0)) → lessF_out_gg(0, s(0))
lessF_in_gg(s(T67), s(T68)) → U8_gg(T67, T68, lessF_in_gg(T67, T68))
U8_gg(T67, T68, lessF_out_gg(T67, T68)) → lessF_out_gg(s(T67), s(T68))
U11_gggga(T59, T57, T58, T60, T62, lessF_out_gg(T59, T57)) → U12_gggga(T59, T57, T58, T60, T62, mergeA_in_gga(.(T57, T58), T60, T62))
mergeA_in_gga(.(s(0), T75), .(0, T77), .(0, T79)) → U5_gga(T75, T77, T79, mergeA_in_gga(.(s(0), T75), T77, T79))
mergeA_in_gga(.(s(T85), T75), .(s(T84), T77), .(s(T84), T79)) → U6_gga(T85, T75, T84, T77, T79, pD_in_gggga(T84, T85, T75, T77, T79))
pD_in_gggga(T84, T85, T75, T77, T79) → U13_gggga(T84, T85, T75, T77, T79, lessF_in_gg(T84, T85))
U13_gggga(T84, T85, T75, T77, T79, lessF_out_gg(T84, T85)) → U14_gggga(T84, T85, T75, T77, T79, mergeA_in_gga(.(s(T85), T75), T77, T79))
U14_gggga(T84, T85, T75, T77, T79, mergeA_out_gga(.(s(T85), T75), T77, T79)) → pD_out_gggga(T84, T85, T75, T77, T79)
U6_gga(T85, T75, T84, T77, T79, pD_out_gggga(T84, T85, T75, T77, T79)) → mergeA_out_gga(.(s(T85), T75), .(s(T84), T77), .(s(T84), T79))
U5_gga(T75, T77, T79, mergeA_out_gga(.(s(0), T75), T77, T79)) → mergeA_out_gga(.(s(0), T75), .(0, T77), .(0, T79))
U12_gggga(T59, T57, T58, T60, T62, mergeA_out_gga(.(T57, T58), T60, T62)) → pC_out_gggga(T59, T57, T58, T60, T62)
U4_gga(T57, T58, T59, T60, T62, pC_out_gggga(T59, T57, T58, T60, T62)) → mergeA_out_gga(.(T57, T58), .(T59, T60), .(T59, T62))
U10_gggga(T35, T36, T18, T20, T22, mergeA_out_gga(T18, .(s(T36), T20), T22)) → pB_out_gggga(T35, T36, T18, T20, T22)
U3_gga(T35, T18, T36, T20, T22, pB_out_gggga(T35, T36, T18, T20, T22)) → mergeA_out_gga(.(s(T35), T18), .(s(T36), T20), .(s(T35), T22))
U2_gga(T18, T20, T22, mergeA_out_gga(T18, .(s(0), T20), T22)) → mergeA_out_gga(.(0, T18), .(s(0), T20), .(0, T22))
U1_gga(T18, T20, T22, mergeA_out_gga(T18, .(0, T20), T22)) → mergeA_out_gga(.(0, T18), .(0, T20), .(0, T22))

(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(T67), s(T68)) → LESSF_IN_GG(T67, T68)

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(T67), s(T68)) → LESSF_IN_GG(T67, T68)

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(T67), s(T68)) → LESSF_IN_GG(T67, T68)
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:

LEQE_IN_GG(s(T41), s(T42)) → LEQE_IN_GG(T41, T42)

The TRS R consists of the following rules:

mergeA_in_gga([], T5, T5) → mergeA_out_gga([], T5, T5)
mergeA_in_gga([], [], []) → mergeA_out_gga([], [], [])
mergeA_in_gga(T7, [], T7) → mergeA_out_gga(T7, [], T7)
mergeA_in_gga(.(0, T18), .(0, T20), .(0, T22)) → U1_gga(T18, T20, T22, mergeA_in_gga(T18, .(0, T20), T22))
mergeA_in_gga(.(0, T18), .(s(0), T20), .(0, T22)) → U2_gga(T18, T20, T22, mergeA_in_gga(T18, .(s(0), T20), T22))
mergeA_in_gga(.(s(T35), T18), .(s(T36), T20), .(s(T35), T22)) → U3_gga(T35, T18, T36, T20, T22, pB_in_gggga(T35, T36, T18, T20, T22))
pB_in_gggga(T35, T36, T18, T20, T22) → U9_gggga(T35, T36, T18, T20, T22, leqE_in_gg(T35, T36))
leqE_in_gg(0, 0) → leqE_out_gg(0, 0)
leqE_in_gg(0, s(0)) → leqE_out_gg(0, s(0))
leqE_in_gg(s(T41), s(T42)) → U7_gg(T41, T42, leqE_in_gg(T41, T42))
U7_gg(T41, T42, leqE_out_gg(T41, T42)) → leqE_out_gg(s(T41), s(T42))
U9_gggga(T35, T36, T18, T20, T22, leqE_out_gg(T35, T36)) → U10_gggga(T35, T36, T18, T20, T22, mergeA_in_gga(T18, .(s(T36), T20), T22))
mergeA_in_gga(.(T57, T58), .(T59, T60), .(T59, T62)) → U4_gga(T57, T58, T59, T60, T62, pC_in_gggga(T59, T57, T58, T60, T62))
pC_in_gggga(T59, T57, T58, T60, T62) → U11_gggga(T59, T57, T58, T60, T62, lessF_in_gg(T59, T57))
lessF_in_gg(0, s(0)) → lessF_out_gg(0, s(0))
lessF_in_gg(s(T67), s(T68)) → U8_gg(T67, T68, lessF_in_gg(T67, T68))
U8_gg(T67, T68, lessF_out_gg(T67, T68)) → lessF_out_gg(s(T67), s(T68))
U11_gggga(T59, T57, T58, T60, T62, lessF_out_gg(T59, T57)) → U12_gggga(T59, T57, T58, T60, T62, mergeA_in_gga(.(T57, T58), T60, T62))
mergeA_in_gga(.(s(0), T75), .(0, T77), .(0, T79)) → U5_gga(T75, T77, T79, mergeA_in_gga(.(s(0), T75), T77, T79))
mergeA_in_gga(.(s(T85), T75), .(s(T84), T77), .(s(T84), T79)) → U6_gga(T85, T75, T84, T77, T79, pD_in_gggga(T84, T85, T75, T77, T79))
pD_in_gggga(T84, T85, T75, T77, T79) → U13_gggga(T84, T85, T75, T77, T79, lessF_in_gg(T84, T85))
U13_gggga(T84, T85, T75, T77, T79, lessF_out_gg(T84, T85)) → U14_gggga(T84, T85, T75, T77, T79, mergeA_in_gga(.(s(T85), T75), T77, T79))
U14_gggga(T84, T85, T75, T77, T79, mergeA_out_gga(.(s(T85), T75), T77, T79)) → pD_out_gggga(T84, T85, T75, T77, T79)
U6_gga(T85, T75, T84, T77, T79, pD_out_gggga(T84, T85, T75, T77, T79)) → mergeA_out_gga(.(s(T85), T75), .(s(T84), T77), .(s(T84), T79))
U5_gga(T75, T77, T79, mergeA_out_gga(.(s(0), T75), T77, T79)) → mergeA_out_gga(.(s(0), T75), .(0, T77), .(0, T79))
U12_gggga(T59, T57, T58, T60, T62, mergeA_out_gga(.(T57, T58), T60, T62)) → pC_out_gggga(T59, T57, T58, T60, T62)
U4_gga(T57, T58, T59, T60, T62, pC_out_gggga(T59, T57, T58, T60, T62)) → mergeA_out_gga(.(T57, T58), .(T59, T60), .(T59, T62))
U10_gggga(T35, T36, T18, T20, T22, mergeA_out_gga(T18, .(s(T36), T20), T22)) → pB_out_gggga(T35, T36, T18, T20, T22)
U3_gga(T35, T18, T36, T20, T22, pB_out_gggga(T35, T36, T18, T20, T22)) → mergeA_out_gga(.(s(T35), T18), .(s(T36), T20), .(s(T35), T22))
U2_gga(T18, T20, T22, mergeA_out_gga(T18, .(s(0), T20), T22)) → mergeA_out_gga(.(0, T18), .(s(0), T20), .(0, T22))
U1_gga(T18, T20, T22, mergeA_out_gga(T18, .(0, T20), T22)) → mergeA_out_gga(.(0, T18), .(0, T20), .(0, T22))

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

LEQE_IN_GG(s(T41), s(T42)) → LEQE_IN_GG(T41, T42)

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

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

LEQE_IN_GG(s(T41), s(T42)) → LEQE_IN_GG(T41, T42)

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:

LEQE_IN_GG(s(T41), s(T42)) → LEQE_IN_GG(T41, T42)
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:

MERGEA_IN_GGA(.(T57, T58), .(T59, T60), .(T59, T62)) → PC_IN_GGGGA(T59, T57, T58, T60, T62)
PC_IN_GGGGA(T59, T57, T58, T60, T62) → U11_GGGGA(T59, T57, T58, T60, T62, lessF_in_gg(T59, T57))
U11_GGGGA(T59, T57, T58, T60, T62, lessF_out_gg(T59, T57)) → MERGEA_IN_GGA(.(T57, T58), T60, T62)
MERGEA_IN_GGA(.(0, T18), .(0, T20), .(0, T22)) → MERGEA_IN_GGA(T18, .(0, T20), T22)
MERGEA_IN_GGA(.(s(0), T75), .(0, T77), .(0, T79)) → MERGEA_IN_GGA(.(s(0), T75), T77, T79)
MERGEA_IN_GGA(.(s(T35), T18), .(s(T36), T20), .(s(T35), T22)) → PB_IN_GGGGA(T35, T36, T18, T20, T22)
PB_IN_GGGGA(T35, T36, T18, T20, T22) → U9_GGGGA(T35, T36, T18, T20, T22, leqE_in_gg(T35, T36))
U9_GGGGA(T35, T36, T18, T20, T22, leqE_out_gg(T35, T36)) → MERGEA_IN_GGA(T18, .(s(T36), T20), T22)
MERGEA_IN_GGA(.(0, T18), .(s(0), T20), .(0, T22)) → MERGEA_IN_GGA(T18, .(s(0), T20), T22)
MERGEA_IN_GGA(.(s(T85), T75), .(s(T84), T77), .(s(T84), T79)) → PD_IN_GGGGA(T84, T85, T75, T77, T79)
PD_IN_GGGGA(T84, T85, T75, T77, T79) → U13_GGGGA(T84, T85, T75, T77, T79, lessF_in_gg(T84, T85))
U13_GGGGA(T84, T85, T75, T77, T79, lessF_out_gg(T84, T85)) → MERGEA_IN_GGA(.(s(T85), T75), T77, T79)

The TRS R consists of the following rules:

mergeA_in_gga([], T5, T5) → mergeA_out_gga([], T5, T5)
mergeA_in_gga([], [], []) → mergeA_out_gga([], [], [])
mergeA_in_gga(T7, [], T7) → mergeA_out_gga(T7, [], T7)
mergeA_in_gga(.(0, T18), .(0, T20), .(0, T22)) → U1_gga(T18, T20, T22, mergeA_in_gga(T18, .(0, T20), T22))
mergeA_in_gga(.(0, T18), .(s(0), T20), .(0, T22)) → U2_gga(T18, T20, T22, mergeA_in_gga(T18, .(s(0), T20), T22))
mergeA_in_gga(.(s(T35), T18), .(s(T36), T20), .(s(T35), T22)) → U3_gga(T35, T18, T36, T20, T22, pB_in_gggga(T35, T36, T18, T20, T22))
pB_in_gggga(T35, T36, T18, T20, T22) → U9_gggga(T35, T36, T18, T20, T22, leqE_in_gg(T35, T36))
leqE_in_gg(0, 0) → leqE_out_gg(0, 0)
leqE_in_gg(0, s(0)) → leqE_out_gg(0, s(0))
leqE_in_gg(s(T41), s(T42)) → U7_gg(T41, T42, leqE_in_gg(T41, T42))
U7_gg(T41, T42, leqE_out_gg(T41, T42)) → leqE_out_gg(s(T41), s(T42))
U9_gggga(T35, T36, T18, T20, T22, leqE_out_gg(T35, T36)) → U10_gggga(T35, T36, T18, T20, T22, mergeA_in_gga(T18, .(s(T36), T20), T22))
mergeA_in_gga(.(T57, T58), .(T59, T60), .(T59, T62)) → U4_gga(T57, T58, T59, T60, T62, pC_in_gggga(T59, T57, T58, T60, T62))
pC_in_gggga(T59, T57, T58, T60, T62) → U11_gggga(T59, T57, T58, T60, T62, lessF_in_gg(T59, T57))
lessF_in_gg(0, s(0)) → lessF_out_gg(0, s(0))
lessF_in_gg(s(T67), s(T68)) → U8_gg(T67, T68, lessF_in_gg(T67, T68))
U8_gg(T67, T68, lessF_out_gg(T67, T68)) → lessF_out_gg(s(T67), s(T68))
U11_gggga(T59, T57, T58, T60, T62, lessF_out_gg(T59, T57)) → U12_gggga(T59, T57, T58, T60, T62, mergeA_in_gga(.(T57, T58), T60, T62))
mergeA_in_gga(.(s(0), T75), .(0, T77), .(0, T79)) → U5_gga(T75, T77, T79, mergeA_in_gga(.(s(0), T75), T77, T79))
mergeA_in_gga(.(s(T85), T75), .(s(T84), T77), .(s(T84), T79)) → U6_gga(T85, T75, T84, T77, T79, pD_in_gggga(T84, T85, T75, T77, T79))
pD_in_gggga(T84, T85, T75, T77, T79) → U13_gggga(T84, T85, T75, T77, T79, lessF_in_gg(T84, T85))
U13_gggga(T84, T85, T75, T77, T79, lessF_out_gg(T84, T85)) → U14_gggga(T84, T85, T75, T77, T79, mergeA_in_gga(.(s(T85), T75), T77, T79))
U14_gggga(T84, T85, T75, T77, T79, mergeA_out_gga(.(s(T85), T75), T77, T79)) → pD_out_gggga(T84, T85, T75, T77, T79)
U6_gga(T85, T75, T84, T77, T79, pD_out_gggga(T84, T85, T75, T77, T79)) → mergeA_out_gga(.(s(T85), T75), .(s(T84), T77), .(s(T84), T79))
U5_gga(T75, T77, T79, mergeA_out_gga(.(s(0), T75), T77, T79)) → mergeA_out_gga(.(s(0), T75), .(0, T77), .(0, T79))
U12_gggga(T59, T57, T58, T60, T62, mergeA_out_gga(.(T57, T58), T60, T62)) → pC_out_gggga(T59, T57, T58, T60, T62)
U4_gga(T57, T58, T59, T60, T62, pC_out_gggga(T59, T57, T58, T60, T62)) → mergeA_out_gga(.(T57, T58), .(T59, T60), .(T59, T62))
U10_gggga(T35, T36, T18, T20, T22, mergeA_out_gga(T18, .(s(T36), T20), T22)) → pB_out_gggga(T35, T36, T18, T20, T22)
U3_gga(T35, T18, T36, T20, T22, pB_out_gggga(T35, T36, T18, T20, T22)) → mergeA_out_gga(.(s(T35), T18), .(s(T36), T20), .(s(T35), T22))
U2_gga(T18, T20, T22, mergeA_out_gga(T18, .(s(0), T20), T22)) → mergeA_out_gga(.(0, T18), .(s(0), T20), .(0, T22))
U1_gga(T18, T20, T22, mergeA_out_gga(T18, .(0, T20), T22)) → mergeA_out_gga(.(0, T18), .(0, T20), .(0, T22))

The argument filtering Pi contains the following mapping:
mergeA_in_gga(x1, x2, x3) = mergeA_in_gga(x1, x2)
[] = []
mergeA_out_gga(x1, x2, x3) = mergeA_out_gga(x1, x2, x3)
.(x1, x2) = .(x1, x2)
0 = 0
U1_gga(x1, x2, x3, x4) = U1_gga(x1, x2, x4)
s(x1) = s(x1)
U2_gga(x1, x2, x3, x4) = U2_gga(x1, x2, x4)
U3_gga(x1, x2, x3, x4, x5, x6) = U3_gga(x1, x2, x3, x4, x6)
pB_in_gggga(x1, x2, x3, x4, x5) = pB_in_gggga(x1, x2, x3, x4)
U9_gggga(x1, x2, x3, x4, x5, x6) = U9_gggga(x1, x2, x3, x4, x6)
leqE_in_gg(x1, x2) = leqE_in_gg(x1, x2)
leqE_out_gg(x1, x2) = leqE_out_gg(x1, x2)
U7_gg(x1, x2, x3) = U7_gg(x1, x2, x3)
U10_gggga(x1, x2, x3, x4, x5, x6) = U10_gggga(x1, x2, x3, x4, x6)
U4_gga(x1, x2, x3, x4, x5, x6) = U4_gga(x1, x2, x3, x4, x6)
pC_in_gggga(x1, x2, x3, x4, x5) = pC_in_gggga(x1, x2, x3, x4)
U11_gggga(x1, x2, x3, x4, x5, x6) = U11_gggga(x1, x2, x3, x4, x6)
lessF_in_gg(x1, x2) = lessF_in_gg(x1, x2)
lessF_out_gg(x1, x2) = lessF_out_gg(x1, x2)
U8_gg(x1, x2, x3) = U8_gg(x1, x2, x3)
U12_gggga(x1, x2, x3, x4, x5, x6) = U12_gggga(x1, x2, x3, x4, x6)
U5_gga(x1, x2, x3, x4) = U5_gga(x1, x2, x4)
U6_gga(x1, x2, x3, x4, x5, x6) = U6_gga(x1, x2, x3, x4, x6)
pD_in_gggga(x1, x2, x3, x4, x5) = pD_in_gggga(x1, x2, x3, x4)
U13_gggga(x1, x2, x3, x4, x5, x6) = U13_gggga(x1, x2, x3, x4, x6)
U14_gggga(x1, x2, x3, x4, x5, x6) = U14_gggga(x1, x2, x3, x4, x6)
pD_out_gggga(x1, x2, x3, x4, x5) = pD_out_gggga(x1, x2, x3, x4, x5)
pC_out_gggga(x1, x2, x3, x4, x5) = pC_out_gggga(x1, x2, x3, x4, x5)
pB_out_gggga(x1, x2, x3, x4, x5) = pB_out_gggga(x1, x2, x3, x4, x5)
MERGEA_IN_GGA(x1, x2, x3) = MERGEA_IN_GGA(x1, x2)
PB_IN_GGGGA(x1, x2, x3, x4, x5) = PB_IN_GGGGA(x1, x2, x3, x4)
U9_GGGGA(x1, x2, x3, x4, x5, x6) = U9_GGGGA(x1, x2, x3, x4, x6)
PC_IN_GGGGA(x1, x2, x3, x4, x5) = PC_IN_GGGGA(x1, x2, x3, x4)
U11_GGGGA(x1, x2, x3, x4, x5, x6) = U11_GGGGA(x1, x2, x3, x4, x6)
PD_IN_GGGGA(x1, x2, x3, x4, x5) = PD_IN_GGGGA(x1, x2, x3, x4)
U13_GGGGA(x1, x2, x3, x4, x5, x6) = U13_GGGGA(x1, x2, x3, x4, x6)

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:

MERGEA_IN_GGA(.(T57, T58), .(T59, T60), .(T59, T62)) → PC_IN_GGGGA(T59, T57, T58, T60, T62)
PC_IN_GGGGA(T59, T57, T58, T60, T62) → U11_GGGGA(T59, T57, T58, T60, T62, lessF_in_gg(T59, T57))
U11_GGGGA(T59, T57, T58, T60, T62, lessF_out_gg(T59, T57)) → MERGEA_IN_GGA(.(T57, T58), T60, T62)
MERGEA_IN_GGA(.(0, T18), .(0, T20), .(0, T22)) → MERGEA_IN_GGA(T18, .(0, T20), T22)
MERGEA_IN_GGA(.(s(0), T75), .(0, T77), .(0, T79)) → MERGEA_IN_GGA(.(s(0), T75), T77, T79)
MERGEA_IN_GGA(.(s(T35), T18), .(s(T36), T20), .(s(T35), T22)) → PB_IN_GGGGA(T35, T36, T18, T20, T22)
PB_IN_GGGGA(T35, T36, T18, T20, T22) → U9_GGGGA(T35, T36, T18, T20, T22, leqE_in_gg(T35, T36))
U9_GGGGA(T35, T36, T18, T20, T22, leqE_out_gg(T35, T36)) → MERGEA_IN_GGA(T18, .(s(T36), T20), T22)
MERGEA_IN_GGA(.(0, T18), .(s(0), T20), .(0, T22)) → MERGEA_IN_GGA(T18, .(s(0), T20), T22)
MERGEA_IN_GGA(.(s(T85), T75), .(s(T84), T77), .(s(T84), T79)) → PD_IN_GGGGA(T84, T85, T75, T77, T79)
PD_IN_GGGGA(T84, T85, T75, T77, T79) → U13_GGGGA(T84, T85, T75, T77, T79, lessF_in_gg(T84, T85))
U13_GGGGA(T84, T85, T75, T77, T79, lessF_out_gg(T84, T85)) → MERGEA_IN_GGA(.(s(T85), T75), T77, T79)

The TRS R consists of the following rules:

lessF_in_gg(0, s(0)) → lessF_out_gg(0, s(0))
lessF_in_gg(s(T67), s(T68)) → U8_gg(T67, T68, lessF_in_gg(T67, T68))
leqE_in_gg(0, 0) → leqE_out_gg(0, 0)
leqE_in_gg(0, s(0)) → leqE_out_gg(0, s(0))
leqE_in_gg(s(T41), s(T42)) → U7_gg(T41, T42, leqE_in_gg(T41, T42))
U8_gg(T67, T68, lessF_out_gg(T67, T68)) → lessF_out_gg(s(T67), s(T68))
U7_gg(T41, T42, leqE_out_gg(T41, T42)) → leqE_out_gg(s(T41), s(T42))

The argument filtering Pi contains the following mapping:
.(x1, x2) = .(x1, x2)
0 = 0
s(x1) = s(x1)
leqE_in_gg(x1, x2) = leqE_in_gg(x1, x2)
leqE_out_gg(x1, x2) = leqE_out_gg(x1, x2)
U7_gg(x1, x2, x3) = U7_gg(x1, x2, x3)
lessF_in_gg(x1, x2) = lessF_in_gg(x1, x2)
lessF_out_gg(x1, x2) = lessF_out_gg(x1, x2)
U8_gg(x1, x2, x3) = U8_gg(x1, x2, x3)
MERGEA_IN_GGA(x1, x2, x3) = MERGEA_IN_GGA(x1, x2)
PB_IN_GGGGA(x1, x2, x3, x4, x5) = PB_IN_GGGGA(x1, x2, x3, x4)
U9_GGGGA(x1, x2, x3, x4, x5, x6) = U9_GGGGA(x1, x2, x3, x4, x6)
PC_IN_GGGGA(x1, x2, x3, x4, x5) = PC_IN_GGGGA(x1, x2, x3, x4)
U11_GGGGA(x1, x2, x3, x4, x5, x6) = U11_GGGGA(x1, x2, x3, x4, x6)
PD_IN_GGGGA(x1, x2, x3, x4, x5) = PD_IN_GGGGA(x1, x2, x3, x4)
U13_GGGGA(x1, x2, x3, x4, x5, x6) = U13_GGGGA(x1, x2, x3, x4, x6)

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:

MERGEA_IN_GGA(.(T57, T58), .(T59, T60)) → PC_IN_GGGGA(T59, T57, T58, T60)
PC_IN_GGGGA(T59, T57, T58, T60) → U11_GGGGA(T59, T57, T58, T60, lessF_in_gg(T59, T57))
U11_GGGGA(T59, T57, T58, T60, lessF_out_gg(T59, T57)) → MERGEA_IN_GGA(.(T57, T58), T60)
MERGEA_IN_GGA(.(0, T18), .(0, T20)) → MERGEA_IN_GGA(T18, .(0, T20))
MERGEA_IN_GGA(.(s(0), T75), .(0, T77)) → MERGEA_IN_GGA(.(s(0), T75), T77)
MERGEA_IN_GGA(.(s(T35), T18), .(s(T36), T20)) → PB_IN_GGGGA(T35, T36, T18, T20)
PB_IN_GGGGA(T35, T36, T18, T20) → U9_GGGGA(T35, T36, T18, T20, leqE_in_gg(T35, T36))
U9_GGGGA(T35, T36, T18, T20, leqE_out_gg(T35, T36)) → MERGEA_IN_GGA(T18, .(s(T36), T20))
MERGEA_IN_GGA(.(0, T18), .(s(0), T20)) → MERGEA_IN_GGA(T18, .(s(0), T20))
MERGEA_IN_GGA(.(s(T85), T75), .(s(T84), T77)) → PD_IN_GGGGA(T84, T85, T75, T77)
PD_IN_GGGGA(T84, T85, T75, T77) → U13_GGGGA(T84, T85, T75, T77, lessF_in_gg(T84, T85))
U13_GGGGA(T84, T85, T75, T77, lessF_out_gg(T84, T85)) → MERGEA_IN_GGA(.(s(T85), T75), T77)

The TRS R consists of the following rules:

lessF_in_gg(0, s(0)) → lessF_out_gg(0, s(0))
lessF_in_gg(s(T67), s(T68)) → U8_gg(T67, T68, lessF_in_gg(T67, T68))
leqE_in_gg(0, 0) → leqE_out_gg(0, 0)
leqE_in_gg(0, s(0)) → leqE_out_gg(0, s(0))
leqE_in_gg(s(T41), s(T42)) → U7_gg(T41, T42, leqE_in_gg(T41, T42))
U8_gg(T67, T68, lessF_out_gg(T67, T68)) → lessF_out_gg(s(T67), s(T68))
U7_gg(T41, T42, leqE_out_gg(T41, T42)) → leqE_out_gg(s(T41), s(T42))

The set Q consists of the following terms:

lessF_in_gg(x0, x1)
leqE_in_gg(x0, x1)
U8_gg(x0, x1, x2)
U7_gg(x0, x1, x2)

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

(26) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04,JAR06].

The following pairs can be oriented strictly and are deleted.

PD_IN_GGGGA(T84, T85, T75, T77) → U13_GGGGA(T84, T85, T75, T77, lessF_in_gg(T84, T85))

The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial interpretation [POLO]:

POL(.(x₁, x₂)) = x₁ + x₂
POL(0) = 0
POL(MERGEA_IN_GGA(x₁, x₂)) = x₂
POL(PB_IN_GGGGA(x₁, x₂, x₃, x₄)) = 1 + x₄
POL(PC_IN_GGGGA(x₁, x₂, x₃, x₄)) = x₄
POL(PD_IN_GGGGA(x₁, x₂, x₃, x₄)) = 1 + x₄
POL(U11_GGGGA(x₁, x₂, x₃, x₄, x₅)) = x₄
POL(U13_GGGGA(x₁, x₂, x₃, x₄, x₅)) = x₄
POL(U7_gg(x₁, x₂, x₃)) = 0
POL(U8_gg(x₁, x₂, x₃)) = 0
POL(U9_GGGGA(x₁, x₂, x₃, x₄, x₅)) = 1 + x₄
POL(leqE_in_gg(x₁, x₂)) = 0
POL(leqE_out_gg(x₁, x₂)) = 0
POL(lessF_in_gg(x₁, x₂)) = 0
POL(lessF_out_gg(x₁, x₂)) = 0
POL(s(x₁)) = 1

The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:
none

(27) Obligation:

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

MERGEA_IN_GGA(.(T57, T58), .(T59, T60)) → PC_IN_GGGGA(T59, T57, T58, T60)
PC_IN_GGGGA(T59, T57, T58, T60) → U11_GGGGA(T59, T57, T58, T60, lessF_in_gg(T59, T57))
U11_GGGGA(T59, T57, T58, T60, lessF_out_gg(T59, T57)) → MERGEA_IN_GGA(.(T57, T58), T60)
MERGEA_IN_GGA(.(0, T18), .(0, T20)) → MERGEA_IN_GGA(T18, .(0, T20))
MERGEA_IN_GGA(.(s(0), T75), .(0, T77)) → MERGEA_IN_GGA(.(s(0), T75), T77)
MERGEA_IN_GGA(.(s(T35), T18), .(s(T36), T20)) → PB_IN_GGGGA(T35, T36, T18, T20)
PB_IN_GGGGA(T35, T36, T18, T20) → U9_GGGGA(T35, T36, T18, T20, leqE_in_gg(T35, T36))
U9_GGGGA(T35, T36, T18, T20, leqE_out_gg(T35, T36)) → MERGEA_IN_GGA(T18, .(s(T36), T20))
MERGEA_IN_GGA(.(0, T18), .(s(0), T20)) → MERGEA_IN_GGA(T18, .(s(0), T20))
MERGEA_IN_GGA(.(s(T85), T75), .(s(T84), T77)) → PD_IN_GGGGA(T84, T85, T75, T77)
U13_GGGGA(T84, T85, T75, T77, lessF_out_gg(T84, T85)) → MERGEA_IN_GGA(.(s(T85), T75), T77)

The TRS R consists of the following rules:

lessF_in_gg(0, s(0)) → lessF_out_gg(0, s(0))
lessF_in_gg(s(T67), s(T68)) → U8_gg(T67, T68, lessF_in_gg(T67, T68))
leqE_in_gg(0, 0) → leqE_out_gg(0, 0)
leqE_in_gg(0, s(0)) → leqE_out_gg(0, s(0))
leqE_in_gg(s(T41), s(T42)) → U7_gg(T41, T42, leqE_in_gg(T41, T42))
U8_gg(T67, T68, lessF_out_gg(T67, T68)) → lessF_out_gg(s(T67), s(T68))
U7_gg(T41, T42, leqE_out_gg(T41, T42)) → leqE_out_gg(s(T41), s(T42))

The set Q consists of the following terms:

lessF_in_gg(x0, x1)
leqE_in_gg(x0, x1)
U8_gg(x0, x1, x2)
U7_gg(x0, x1, x2)

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

(28) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 2 less nodes.

(29) Obligation:

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

PC_IN_GGGGA(T59, T57, T58, T60) → U11_GGGGA(T59, T57, T58, T60, lessF_in_gg(T59, T57))
U11_GGGGA(T59, T57, T58, T60, lessF_out_gg(T59, T57)) → MERGEA_IN_GGA(.(T57, T58), T60)
MERGEA_IN_GGA(.(T57, T58), .(T59, T60)) → PC_IN_GGGGA(T59, T57, T58, T60)
MERGEA_IN_GGA(.(0, T18), .(0, T20)) → MERGEA_IN_GGA(T18, .(0, T20))
MERGEA_IN_GGA(.(s(0), T75), .(0, T77)) → MERGEA_IN_GGA(.(s(0), T75), T77)
MERGEA_IN_GGA(.(s(T35), T18), .(s(T36), T20)) → PB_IN_GGGGA(T35, T36, T18, T20)
PB_IN_GGGGA(T35, T36, T18, T20) → U9_GGGGA(T35, T36, T18, T20, leqE_in_gg(T35, T36))
U9_GGGGA(T35, T36, T18, T20, leqE_out_gg(T35, T36)) → MERGEA_IN_GGA(T18, .(s(T36), T20))
MERGEA_IN_GGA(.(0, T18), .(s(0), T20)) → MERGEA_IN_GGA(T18, .(s(0), T20))

The TRS R consists of the following rules:

lessF_in_gg(0, s(0)) → lessF_out_gg(0, s(0))
lessF_in_gg(s(T67), s(T68)) → U8_gg(T67, T68, lessF_in_gg(T67, T68))
leqE_in_gg(0, 0) → leqE_out_gg(0, 0)
leqE_in_gg(0, s(0)) → leqE_out_gg(0, s(0))
leqE_in_gg(s(T41), s(T42)) → U7_gg(T41, T42, leqE_in_gg(T41, T42))
U8_gg(T67, T68, lessF_out_gg(T67, T68)) → lessF_out_gg(s(T67), s(T68))
U7_gg(T41, T42, leqE_out_gg(T41, T42)) → leqE_out_gg(s(T41), s(T42))

The set Q consists of the following terms:

lessF_in_gg(x0, x1)
leqE_in_gg(x0, x1)
U8_gg(x0, x1, x2)
U7_gg(x0, x1, x2)

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

(30) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04,JAR06].

The following pairs can be oriented strictly and are deleted.

MERGEA_IN_GGA(.(0, T18), .(0, T20)) → MERGEA_IN_GGA(T18, .(0, T20))
PB_IN_GGGGA(T35, T36, T18, T20) → U9_GGGGA(T35, T36, T18, T20, leqE_in_gg(T35, T36))
MERGEA_IN_GGA(.(0, T18), .(s(0), T20)) → MERGEA_IN_GGA(T18, .(s(0), T20))

The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial interpretation [POLO]:

POL(.(x₁, x₂)) = 1 + x₂
POL(0) = 0
POL(MERGEA_IN_GGA(x₁, x₂)) = x₁
POL(PB_IN_GGGGA(x₁, x₂, x₃, x₄)) = 1 + x₃
POL(PC_IN_GGGGA(x₁, x₂, x₃, x₄)) = 1 + x₃
POL(U11_GGGGA(x₁, x₂, x₃, x₄, x₅)) = 1 + x₃
POL(U7_gg(x₁, x₂, x₃)) = 0
POL(U8_gg(x₁, x₂, x₃)) = 0
POL(U9_GGGGA(x₁, x₂, x₃, x₄, x₅)) = x₃
POL(leqE_in_gg(x₁, x₂)) = 0
POL(leqE_out_gg(x₁, x₂)) = 0
POL(lessF_in_gg(x₁, x₂)) = 0
POL(lessF_out_gg(x₁, x₂)) = 0
POL(s(x₁)) = 0

The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:
none

(31) Obligation:

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

PC_IN_GGGGA(T59, T57, T58, T60) → U11_GGGGA(T59, T57, T58, T60, lessF_in_gg(T59, T57))
U11_GGGGA(T59, T57, T58, T60, lessF_out_gg(T59, T57)) → MERGEA_IN_GGA(.(T57, T58), T60)
MERGEA_IN_GGA(.(T57, T58), .(T59, T60)) → PC_IN_GGGGA(T59, T57, T58, T60)
MERGEA_IN_GGA(.(s(0), T75), .(0, T77)) → MERGEA_IN_GGA(.(s(0), T75), T77)
MERGEA_IN_GGA(.(s(T35), T18), .(s(T36), T20)) → PB_IN_GGGGA(T35, T36, T18, T20)
U9_GGGGA(T35, T36, T18, T20, leqE_out_gg(T35, T36)) → MERGEA_IN_GGA(T18, .(s(T36), T20))

The TRS R consists of the following rules:

lessF_in_gg(0, s(0)) → lessF_out_gg(0, s(0))
lessF_in_gg(s(T67), s(T68)) → U8_gg(T67, T68, lessF_in_gg(T67, T68))
leqE_in_gg(0, 0) → leqE_out_gg(0, 0)
leqE_in_gg(0, s(0)) → leqE_out_gg(0, s(0))
leqE_in_gg(s(T41), s(T42)) → U7_gg(T41, T42, leqE_in_gg(T41, T42))
U8_gg(T67, T68, lessF_out_gg(T67, T68)) → lessF_out_gg(s(T67), s(T68))
U7_gg(T41, T42, leqE_out_gg(T41, T42)) → leqE_out_gg(s(T41), s(T42))

The set Q consists of the following terms:

lessF_in_gg(x0, x1)
leqE_in_gg(x0, x1)
U8_gg(x0, x1, x2)
U7_gg(x0, x1, x2)

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

(32) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 2 less nodes.

(33) Obligation:

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

U11_GGGGA(T59, T57, T58, T60, lessF_out_gg(T59, T57)) → MERGEA_IN_GGA(.(T57, T58), T60)
MERGEA_IN_GGA(.(T57, T58), .(T59, T60)) → PC_IN_GGGGA(T59, T57, T58, T60)
PC_IN_GGGGA(T59, T57, T58, T60) → U11_GGGGA(T59, T57, T58, T60, lessF_in_gg(T59, T57))
MERGEA_IN_GGA(.(s(0), T75), .(0, T77)) → MERGEA_IN_GGA(.(s(0), T75), T77)

The TRS R consists of the following rules:

lessF_in_gg(0, s(0)) → lessF_out_gg(0, s(0))
lessF_in_gg(s(T67), s(T68)) → U8_gg(T67, T68, lessF_in_gg(T67, T68))
leqE_in_gg(0, 0) → leqE_out_gg(0, 0)
leqE_in_gg(0, s(0)) → leqE_out_gg(0, s(0))
leqE_in_gg(s(T41), s(T42)) → U7_gg(T41, T42, leqE_in_gg(T41, T42))
U8_gg(T67, T68, lessF_out_gg(T67, T68)) → lessF_out_gg(s(T67), s(T68))
U7_gg(T41, T42, leqE_out_gg(T41, T42)) → leqE_out_gg(s(T41), s(T42))

The set Q consists of the following terms:

lessF_in_gg(x0, x1)
leqE_in_gg(x0, x1)
U8_gg(x0, x1, x2)
U7_gg(x0, x1, x2)

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

(34) UsableRulesProof (EQUIVALENT transformation)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

(35) Obligation:

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

U11_GGGGA(T59, T57, T58, T60, lessF_out_gg(T59, T57)) → MERGEA_IN_GGA(.(T57, T58), T60)
MERGEA_IN_GGA(.(T57, T58), .(T59, T60)) → PC_IN_GGGGA(T59, T57, T58, T60)
PC_IN_GGGGA(T59, T57, T58, T60) → U11_GGGGA(T59, T57, T58, T60, lessF_in_gg(T59, T57))
MERGEA_IN_GGA(.(s(0), T75), .(0, T77)) → MERGEA_IN_GGA(.(s(0), T75), T77)

The TRS R consists of the following rules:

lessF_in_gg(0, s(0)) → lessF_out_gg(0, s(0))
lessF_in_gg(s(T67), s(T68)) → U8_gg(T67, T68, lessF_in_gg(T67, T68))
U8_gg(T67, T68, lessF_out_gg(T67, T68)) → lessF_out_gg(s(T67), s(T68))

The set Q consists of the following terms:

lessF_in_gg(x0, x1)
leqE_in_gg(x0, x1)
U8_gg(x0, x1, x2)
U7_gg(x0, x1, x2)

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

(36) QReductionProof (EQUIVALENT transformation)

We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

leqE_in_gg(x0, x1)
U7_gg(x0, x1, x2)

(37) Obligation:

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

U11_GGGGA(T59, T57, T58, T60, lessF_out_gg(T59, T57)) → MERGEA_IN_GGA(.(T57, T58), T60)
MERGEA_IN_GGA(.(T57, T58), .(T59, T60)) → PC_IN_GGGGA(T59, T57, T58, T60)
PC_IN_GGGGA(T59, T57, T58, T60) → U11_GGGGA(T59, T57, T58, T60, lessF_in_gg(T59, T57))
MERGEA_IN_GGA(.(s(0), T75), .(0, T77)) → MERGEA_IN_GGA(.(s(0), T75), T77)

The TRS R consists of the following rules:

lessF_in_gg(0, s(0)) → lessF_out_gg(0, s(0))
lessF_in_gg(s(T67), s(T68)) → U8_gg(T67, T68, lessF_in_gg(T67, T68))
U8_gg(T67, T68, lessF_out_gg(T67, T68)) → lessF_out_gg(s(T67), s(T68))

The set Q consists of the following terms:

lessF_in_gg(x0, x1)
U8_gg(x0, x1, x2)

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

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

PC_IN_GGGGA(T59, T57, T58, T60) → U11_GGGGA(T59, T57, T58, T60, lessF_in_gg(T59, T57))
The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 3, 4 >= 4
U11_GGGGA(T59, T57, T58, T60, lessF_out_gg(T59, T57)) → MERGEA_IN_GGA(.(T57, T58), T60)
The graph contains the following edges 4 >= 2
MERGEA_IN_GGA(.(s(0), T75), .(0, T77)) → MERGEA_IN_GGA(.(s(0), T75), T77)
The graph contains the following edges 1 >= 1, 2 > 2
MERGEA_IN_GGA(.(T57, T58), .(T59, T60)) → PC_IN_GGGGA(T59, T57, T58, T60)
The graph contains the following edges 2 > 1, 1 > 2, 1 > 3, 2 > 4

(0) Obligation:

(1) PrologToPiTRSViaGraphTransformerProof (SOUND transformation)

(2) Obligation:

(3) DependencyPairsProof (EQUIVALENT transformation)

(4) Obligation:

(5) DependencyGraphProof (EQUIVALENT transformation)

(6) Complex Obligation (AND)

(7) Obligation:

(8) UsableRulesProof (EQUIVALENT transformation)

(9) Obligation:

(10) PiDPToQDPProof (EQUIVALENT transformation)

(11) Obligation:

(12) QDPSizeChangeProof (EQUIVALENT transformation)

(13) YES

(14) Obligation:

(15) UsableRulesProof (EQUIVALENT transformation)

(16) Obligation:

(17) PiDPToQDPProof (EQUIVALENT transformation)

(18) Obligation:

(19) QDPSizeChangeProof (EQUIVALENT transformation)

(20) YES

(21) Obligation:

(22) UsableRulesProof (EQUIVALENT transformation)

(23) Obligation:

(24) PiDPToQDPProof (SOUND transformation)

(25) Obligation:

(26) QDPOrderProof (EQUIVALENT transformation)

(27) Obligation:

(28) DependencyGraphProof (EQUIVALENT transformation)

(29) Obligation:

(30) QDPOrderProof (EQUIVALENT transformation)

(31) Obligation:

(32) DependencyGraphProof (EQUIVALENT transformation)

(33) Obligation:

(34) UsableRulesProof (EQUIVALENT transformation)

(35) Obligation:

(36) QReductionProof (EQUIVALENT transformation)

(37) Obligation:

(38) QDPSizeChangeProof (EQUIVALENT transformation)

(39) YES