Left Termination proof of /tmp/tmp5kwiMJ/overlap2.pl

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

0 Prolog

↳1 PrologToPiTRSViaGraphTransformerProof (⇒, 160 ms)

↳2 PiTRS

↳3 DependencyPairsProof (⇔, 19 ms)

↳4 PiDP

↳5 DependencyGraphProof (⇔, 0 ms)

↳6 AND

    ↳7 PiDP

        ↳8 UsableRulesProof (⇔, 0 ms)

        ↳9 PiDP

        ↳10 PiDPToQDPProof (⇔, 16 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

(0) Obligation:

Clauses:

overlap(Xs, Ys) :- ','(member(X, Xs), member(X, Ys)).
member(X, Y) :- ','(no(empty(Y)), head(Y, X)).
member(X, Y) :- ','(no(empty(Y)), ','(tail(Y, T), member(X, T))).
head([], X1).
head(.(H, X2), H).
tail([], []).
tail(.(X3, T), T).
empty([]).
no(X) :- ','(X, ','(!, failure(a))).
no(X4).
failure(b).

Query: overlap(g,g)

(1) PrologToPiTRSViaGraphTransformerProof (SOUND transformation)

Transformed Prolog program to (Pi-)TRS.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
1 [label="A: overlap(T1, T2)\n\nT1 is ground\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
4 [label="4: overlap(T1, T2), SCOPE: 1, CLAUSE: 0\n\nT1 is ground\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
7 [label="B: ','(member(X9, T5), member(X9, T6))\n\nT5 is ground\nT6 is ground\nX9 is free", fontsize=16, style=filled, fillcolor=lightyellow];
11 [label="11: ','(member(X9, T5), member(X9, T6)), SCOPE: 2, CLAUSE: 1 | ','(member(X9, T5), member(X9, T6)), SCOPE: 2, CLAUSE: 2\n\nT5 is ground\nT6 is ground\nX9 is free", fontsize=16, style=filled, fillcolor=lightyellow];
13 [label="13: ','(member(X9, T5), member(X9, T6)), SCOPE: 2, CLAUSE: 1\n\nT5 is ground\nT6 is ground\nX9 is free", fontsize=16, style=filled, fillcolor=lightyellow];
15 [label="15: ','(member(X9, T5), member(X9, T6)), SCOPE: 2, CLAUSE: 2\n\nT5 is ground\nT6 is ground\nX9 is free", fontsize=16, style=filled, fillcolor=lightyellow];
17 [label="17: ','(','(no(empty(T13)), head(T13, X30)), member(X30, T6))\n\nT6 is ground\nT13 is ground\nX30 is free", fontsize=16, style=filled, fillcolor=lightyellow];
20 [label="20: ','(','(no(empty(T13)), head(T13, X30)), member(X30, T6)), SCOPE: 3, CLAUSE: 8 | ','(','(no(empty(T13)), head(T13, X30)), member(X30, T6)), SCOPE: 3, CLAUSE: 9\n\nT6 is ground\nT13 is ground\nX30 is free", fontsize=16, style=filled, fillcolor=lightyellow];
24 [label="24: ','(','(call(empty(T17)), ','(!_3, failure(a))), ','(head(T17, X30), member(X30, T6))) | ','(','(no(empty(T17)), head(T17, X30)), member(X30, T6)), SCOPE: 3, CLAUSE: 9\n\nT6 is ground\nT17 is ground\nX30 is free", fontsize=16, style=filled, fillcolor=lightyellow];
26 [label="26: ','(empty(T17), ','(','(!_3, failure(a)), ','(head(T17, X30), member(X30, T6)))) | ?_4 | ','(','(no(empty(T17)), head(T17, X30)), member(X30, T6)), SCOPE: 3, CLAUSE: 9\n\nT6 is ground\nT17 is ground\nX30 is free", fontsize=16, style=filled, fillcolor=lightyellow];
30 [label="30: ','(empty(T17), ','(','(!_3, failure(a)), ','(head(T17, X30), member(X30, T6)))), SCOPE: 5, CLAUSE: 7 | ?_5 | ?_4 | ','(','(no(empty(T17)), head(T17, X30)), member(X30, T6)), SCOPE: 3, CLAUSE: 9\n\nT6 is ground\nT17 is ground\nX30 is free", fontsize=16, style=filled, fillcolor=lightyellow];
34 [label="34: ','(','(!_3, failure(a)), ','(head([], X30), member(X30, T6))) | ?_5 | ?_4 | ','(','(no(empty([])), head([], X30)), member(X30, T6)), SCOPE: 3, CLAUSE: 9\n\nT6 is ground\nX30 is free", fontsize=16, style=filled, fillcolor=lightyellow];
36 [label="36: ?_5 | ?_4 | ','(','(no(empty(T17)), head(T17, X30)), member(X30, T6)), SCOPE: 3, CLAUSE: 9\n\nT6 is ground\nT17 is ground\nX30 is free\nempty(T17) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
38 [label="38: ','(failure(a), ','(head([], X30), member(X30, T6)))\n\nT6 is ground\nX30 is free", fontsize=16, style=filled, fillcolor=lightyellow];
45 [label="45: ','(failure(a), ','(head([], X30), member(X30, T6))), SCOPE: 6, CLAUSE: 10\n\nT6 is ground\nX30 is free", fontsize=16, style=filled, fillcolor=lightyellow];
46 [label="46: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
47 [label="47: ?_4 | ','(','(no(empty(T17)), head(T17, X30)), member(X30, T6)), SCOPE: 3, CLAUSE: 9\n\nT6 is ground\nT17 is ground\nX30 is free\nempty(T17) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
49 [label="49: ','(','(no(empty(T17)), head(T17, X30)), member(X30, T6)), SCOPE: 3, CLAUSE: 9\n\nT6 is ground\nT17 is ground\nX30 is free\nempty(T17) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
57 [label="57: ','(head(T22, X30), member(X30, T6))\n\nT6 is ground\nT22 is ground\nX30 is free\nempty(T22) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
61 [label="61: ','(head(T22, X30), member(X30, T6)), SCOPE: 7, CLAUSE: 3 | ','(head(T22, X30), member(X30, T6)), SCOPE: 7, CLAUSE: 4\n\nT6 is ground\nT22 is ground\nX30 is free\nempty(T22) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
64 [label="64: ','(head(T22, X30), member(X30, T6)), SCOPE: 7, CLAUSE: 4\n\nT6 is ground\nT22 is ground\nX30 is free\nempty(T22) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
66 [label="C: member(T28, T6)\n\nT6 is ground\nT28 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
67 [label="67: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
70 [label="70: member(T28, T6), SCOPE: 8, CLAUSE: 1 | member(T28, T6), SCOPE: 8, CLAUSE: 2\n\nT6 is ground\nT28 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
72 [label="72: member(T28, T6), SCOPE: 8, CLAUSE: 1\n\nT6 is ground\nT28 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
73 [label="73: member(T28, T6), SCOPE: 8, CLAUSE: 2\n\nT6 is ground\nT28 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
79 [label="79: ','(no(empty(T41)), head(T41, T40))\n\nT40 is ground\nT41 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
81 [label="81: ','(no(empty(T41)), head(T41, T40)), SCOPE: 9, CLAUSE: 8 | ','(no(empty(T41)), head(T41, T40)), SCOPE: 9, CLAUSE: 9\n\nT40 is ground\nT41 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
84 [label="84: ','(','(call(empty(T44)), ','(!_9, failure(a))), head(T44, T40)) | ','(no(empty(T44)), head(T44, T40)), SCOPE: 9, CLAUSE: 9\n\nT40 is ground\nT44 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
86 [label="86: ','(empty(T44), ','(','(!_9, failure(a)), head(T44, T40))) | ?_10 | ','(no(empty(T44)), head(T44, T40)), SCOPE: 9, CLAUSE: 9\n\nT40 is ground\nT44 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
88 [label="88: ','(empty(T44), ','(','(!_9, failure(a)), head(T44, T40))), SCOPE: 11, CLAUSE: 7 | ?_11 | ?_10 | ','(no(empty(T44)), head(T44, T40)), SCOPE: 9, CLAUSE: 9\n\nT40 is ground\nT44 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
90 [label="90: ','(','(!_9, failure(a)), head([], T40)) | ?_11 | ?_10 | ','(no(empty([])), head([], T40)), SCOPE: 9, CLAUSE: 9\n\nT40 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
93 [label="93: ?_11 | ?_10 | ','(no(empty(T44)), head(T44, T40)), SCOPE: 9, CLAUSE: 9\n\nT40 is ground\nT44 is ground\nempty(T44) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
95 [label="95: ','(failure(a), head([], T40))\n\nT40 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
98 [label="98: ','(failure(a), head([], T40)), SCOPE: 12, CLAUSE: 10\n\nT40 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
99 [label="99: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
101 [label="101: ?_10 | ','(no(empty(T44)), head(T44, T40)), SCOPE: 9, CLAUSE: 9\n\nT40 is ground\nT44 is ground\nempty(T44) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
102 [label="102: ','(no(empty(T44)), head(T44, T40)), SCOPE: 9, CLAUSE: 9\n\nT40 is ground\nT44 is ground\nempty(T44) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
105 [label="105: head(T47, T40)\n\nT40 is ground\nT47 is ground\nempty(T47) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
107 [label="107: head(T47, T40), SCOPE: 13, CLAUSE: 3 | head(T47, T40), SCOPE: 13, CLAUSE: 4\n\nT40 is ground\nT47 is ground\nempty(T47) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
108 [label="108: head(T47, T40), SCOPE: 13, CLAUSE: 4\n\nT40 is ground\nT47 is ground\nempty(T47) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
111 [label="111: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
113 [label="113: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
114 [label="114: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
119 [label="119: ','(no(empty(T61)), ','(tail(T61, X92), member(T60, X92)))\n\nT60 is ground\nT61 is ground\nX92 is free", fontsize=16, style=filled, fillcolor=lightyellow];
143 [label="143: ','(no(empty(T61)), ','(tail(T61, X92), member(T60, X92))), SCOPE: 14, CLAUSE: 8 | ','(no(empty(T61)), ','(tail(T61, X92), member(T60, X92))), SCOPE: 14, CLAUSE: 9\n\nT60 is ground\nT61 is ground\nX92 is free", fontsize=16, style=filled, fillcolor=lightyellow];
148 [label="148: ','(','(call(empty(T65)), ','(!_14, failure(a))), ','(tail(T65, X92), member(T60, X92))) | ','(no(empty(T65)), ','(tail(T65, X92), member(T60, X92))), SCOPE: 14, CLAUSE: 9\n\nT60 is ground\nT65 is ground\nX92 is free", fontsize=16, style=filled, fillcolor=lightyellow];
150 [label="150: ','(empty(T65), ','(','(!_14, failure(a)), ','(tail(T65, X92), member(T60, X92)))) | ?_15 | ','(no(empty(T65)), ','(tail(T65, X92), member(T60, X92))), SCOPE: 14, CLAUSE: 9\n\nT60 is ground\nT65 is ground\nX92 is free", fontsize=16, style=filled, fillcolor=lightyellow];
151 [label="151: ','(empty(T65), ','(','(!_14, failure(a)), ','(tail(T65, X92), member(T60, X92)))), SCOPE: 16, CLAUSE: 7 | ?_16 | ?_15 | ','(no(empty(T65)), ','(tail(T65, X92), member(T60, X92))), SCOPE: 14, CLAUSE: 9\n\nT60 is ground\nT65 is ground\nX92 is free", fontsize=16, style=filled, fillcolor=lightyellow];
152 [label="152: ','(','(!_14, failure(a)), ','(tail([], X92), member(T60, X92))) | ?_16 | ?_15 | ','(no(empty([])), ','(tail([], X92), member(T60, X92))), SCOPE: 14, CLAUSE: 9\n\nT60 is ground\nX92 is free", fontsize=16, style=filled, fillcolor=lightyellow];
154 [label="154: ?_16 | ?_15 | ','(no(empty(T65)), ','(tail(T65, X92), member(T60, X92))), SCOPE: 14, CLAUSE: 9\n\nT60 is ground\nT65 is ground\nX92 is free\nempty(T65) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
155 [label="155: ','(failure(a), ','(tail([], X92), member(T60, X92)))\n\nT60 is ground\nX92 is free", fontsize=16, style=filled, fillcolor=lightyellow];
157 [label="157: ','(failure(a), ','(tail([], X92), member(T60, X92))), SCOPE: 17, CLAUSE: 10\n\nT60 is ground\nX92 is free", fontsize=16, style=filled, fillcolor=lightyellow];
159 [label="159: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
160 [label="160: ?_15 | ','(no(empty(T65)), ','(tail(T65, X92), member(T60, X92))), SCOPE: 14, CLAUSE: 9\n\nT60 is ground\nT65 is ground\nX92 is free\nempty(T65) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
161 [label="161: ','(no(empty(T65)), ','(tail(T65, X92), member(T60, X92))), SCOPE: 14, CLAUSE: 9\n\nT60 is ground\nT65 is ground\nX92 is free\nempty(T65) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
164 [label="164: ','(tail(T70, X92), member(T60, X92))\n\nT60 is ground\nT70 is ground\nX92 is free\nempty(T70) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
165 [label="165: ','(tail(T70, X92), member(T60, X92)), SCOPE: 18, CLAUSE: 5 | ','(tail(T70, X92), member(T60, X92)), SCOPE: 18, CLAUSE: 6\n\nT60 is ground\nT70 is ground\nX92 is free\nempty(T70) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
166 [label="166: ','(tail(T70, X92), member(T60, X92)), SCOPE: 18, CLAUSE: 6\n\nT60 is ground\nT70 is ground\nX92 is free\nempty(T70) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
171 [label="171: member(T60, T77)\n\nT60 is ground\nT77 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
172 [label="172: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
189 [label="189: ','(','(no(empty(T82)), ','(tail(T82, X132), member(X133, X132))), member(X133, T6))\n\nT6 is ground\nT82 is ground\nX133 is free\nX132 is free", fontsize=16, style=filled, fillcolor=lightyellow];
196 [label="196: ','(','(no(empty(T82)), ','(tail(T82, X132), member(X133, X132))), member(X133, T6)), SCOPE: 19, CLAUSE: 8 | ','(','(no(empty(T82)), ','(tail(T82, X132), member(X133, X132))), member(X133, T6)), SCOPE: 19, CLAUSE: 9\n\nT6 is ground\nT82 is ground\nX133 is free\nX132 is free", fontsize=16, style=filled, fillcolor=lightyellow];
199 [label="199: ','(','(call(empty(T85)), ','(!_19, failure(a))), ','(','(tail(T85, X132), member(X133, X132)), member(X133, T6))) | ','(','(no(empty(T85)), ','(tail(T85, X132), member(X133, X132))), member(X133, T6)), SCOPE: 19, CLAUSE: 9\n\nT6 is ground\nT85 is ground\nX133 is free\nX132 is free", fontsize=16, style=filled, fillcolor=lightyellow];
202 [label="202: ','(empty(T85), ','(','(!_19, failure(a)), ','(','(tail(T85, X132), member(X133, X132)), member(X133, T6)))) | ?_20 | ','(','(no(empty(T85)), ','(tail(T85, X132), member(X133, X132))), member(X133, T6)), SCOPE: 19, CLAUSE: 9\n\nT6 is ground\nT85 is ground\nX133 is free\nX132 is free", fontsize=16, style=filled, fillcolor=lightyellow];
203 [label="203: ','(empty(T85), ','(','(!_19, failure(a)), ','(','(tail(T85, X132), member(X133, X132)), member(X133, T6)))), SCOPE: 21, CLAUSE: 7 | ?_21 | ?_20 | ','(','(no(empty(T85)), ','(tail(T85, X132), member(X133, X132))), member(X133, T6)), SCOPE: 19, CLAUSE: 9\n\nT6 is ground\nT85 is ground\nX133 is free\nX132 is free", fontsize=16, style=filled, fillcolor=lightyellow];
205 [label="205: ','(','(!_19, failure(a)), ','(','(tail([], X132), member(X133, X132)), member(X133, T6))) | ?_21 | ?_20 | ','(','(no(empty([])), ','(tail([], X132), member(X133, X132))), member(X133, T6)), SCOPE: 19, CLAUSE: 9\n\nT6 is ground\nX133 is free\nX132 is free", fontsize=16, style=filled, fillcolor=lightyellow];
207 [label="207: ?_21 | ?_20 | ','(','(no(empty(T85)), ','(tail(T85, X132), member(X133, X132))), member(X133, T6)), SCOPE: 19, CLAUSE: 9\n\nT6 is ground\nT85 is ground\nX133 is free\nX132 is free\nempty(T85) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
208 [label="208: ','(failure(a), ','(','(tail([], X132), member(X133, X132)), member(X133, T6)))\n\nT6 is ground\nX133 is free\nX132 is free", fontsize=16, style=filled, fillcolor=lightyellow];
209 [label="209: ','(failure(a), ','(','(tail([], X132), member(X133, X132)), member(X133, T6))), SCOPE: 22, CLAUSE: 10\n\nT6 is ground\nX133 is free\nX132 is free", fontsize=16, style=filled, fillcolor=lightyellow];
210 [label="210: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
211 [label="211: ?_20 | ','(','(no(empty(T85)), ','(tail(T85, X132), member(X133, X132))), member(X133, T6)), SCOPE: 19, CLAUSE: 9\n\nT6 is ground\nT85 is ground\nX133 is free\nX132 is free\nempty(T85) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
213 [label="213: ','(','(no(empty(T85)), ','(tail(T85, X132), member(X133, X132))), member(X133, T6)), SCOPE: 19, CLAUSE: 9\n\nT6 is ground\nT85 is ground\nX133 is free\nX132 is free\nempty(T85) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
215 [label="215: ','(','(tail(T88, X132), member(X133, X132)), member(X133, T6))\n\nT6 is ground\nT88 is ground\nX133 is free\nX132 is free\nempty(T88) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
216 [label="216: ','(','(tail(T88, X132), member(X133, X132)), member(X133, T6)), SCOPE: 23, CLAUSE: 5 | ','(','(tail(T88, X132), member(X133, X132)), member(X133, T6)), SCOPE: 23, CLAUSE: 6\n\nT6 is ground\nT88 is ground\nX133 is free\nX132 is free\nempty(T88) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
217 [label="217: ','(','(tail(T88, X132), member(X133, X132)), member(X133, T6)), SCOPE: 23, CLAUSE: 6\n\nT6 is ground\nT88 is ground\nX133 is free\nX132 is free\nempty(T88) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
219 [label="219: ','(member(X133, T94), member(X133, T6))\n\nT6 is ground\nT94 is ground\nX133 is free", fontsize=16, style=filled, fillcolor=lightyellow];
220 [label="220: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
221 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
1 -> 221 [arrowhead = none ];
221 -> 4;

222 [label="ONLY EVAL with clause\noverlap(X7, X8) :- ','(member(X9, X7), member(X9, X8)).\nand substitutionT1 -> T5,\nX7 -> T5,\nT2 -> T6,\nX8 -> T6", fontsize=14, style = filled, fillcolor = lightblue];
4 -> 222 [arrowhead = none ];
222 -> 7;

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

224 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
11 -> 224 [arrowhead = none ];
224 -> 13;

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

226 [label="ONLY EVAL with clause\nmember(X28, X29) :- ','(no(empty(X29)), head(X29, X28)).\nand substitutionX9 -> X30,\nX28 -> X30,\nT5 -> T13,\nX29 -> T13", fontsize=14, style = filled, fillcolor = lightblue];
13 -> 226 [arrowhead = none ];
226 -> 17;

227 [label="ONLY EVAL with clause\nmember(X130, X131) :- ','(no(empty(X131)), ','(tail(X131, X132), member(X130, X132))).\nand substitutionX9 -> X133,\nX130 -> X133,\nT5 -> T82,\nX131 -> T82", fontsize=14, style = filled, fillcolor = lightblue];
15 -> 227 [arrowhead = none ];
227 -> 189;

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

229 [label="ONLY EVAL with clause\nno(X36) :- ','(call(X36), ','(!_3, failure(a))).\nand substitutionT13 -> T17,\nX36 -> empty(T17)", fontsize=14, style = filled, fillcolor = lightblue];
20 -> 229 [arrowhead = none ];
229 -> 24;

230 [label="CALL", fontsize=14, style = filled, fillcolor = lightcyan];
24 -> 230 [arrowhead = none ];
230 -> 26;

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

232 [label="EVAL with clause\nempty([]).\nand substitutionT17 -> []", fontsize=14, style = filled, fillcolor = lightblue];
30 -> 232 [arrowhead = none ];
232 -> 34;

233 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
30 -> 233 [arrowhead = none ];
233 -> 36;

234 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
34 -> 234 [arrowhead = none ];
234 -> 38;

235 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
36 -> 235 [arrowhead = none ];
235 -> 47;

236 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
38 -> 236 [arrowhead = none ];
236 -> 45;

237 [label="BACKTRACK\nfor clause: failure(b)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
45 -> 237 [arrowhead = none ];
237 -> 46;

238 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
47 -> 238 [arrowhead = none ];
238 -> 49;

239 [label="ONLY EVAL with clause\nno(X45).\nand substitutionT17 -> T22,\nX45 -> empty(T22)", fontsize=14, style = filled, fillcolor = lightblue];
49 -> 239 [arrowhead = none ];
239 -> 57;

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

241 [label="BACKTRACK\nfor clause: head([], X1)\nwith clash: (empty(T22), empty([]))", fontsize=14, style = filled, fillcolor = lightgreen];
61 -> 241 [arrowhead = none ];
241 -> 64;

242 [label="EVAL with clause\nhead(.(X55, X56), X55).\nand substitutionX55 -> T28,\nX56 -> T29,\nT22 -> .(T28, T29),\nX30 -> T28", fontsize=14, style = filled, fillcolor = lightblue];
64 -> 242 [arrowhead = none ];
242 -> 66;

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

244 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
66 -> 244 [arrowhead = none ];
244 -> 70;

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

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

247 [label="ONLY EVAL with clause\nmember(X67, X68) :- ','(no(empty(X68)), head(X68, X67)).\nand substitutionT28 -> T40,\nX67 -> T40,\nT6 -> T41,\nX68 -> T41", fontsize=14, style = filled, fillcolor = lightblue];
72 -> 247 [arrowhead = none ];
247 -> 79;

248 [label="ONLY EVAL with clause\nmember(X90, X91) :- ','(no(empty(X91)), ','(tail(X91, X92), member(X90, X92))).\nand substitutionT28 -> T60,\nX90 -> T60,\nT6 -> T61,\nX91 -> T61", fontsize=14, style = filled, fillcolor = lightblue];
73 -> 248 [arrowhead = none ];
248 -> 119;

249 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
79 -> 249 [arrowhead = none ];
249 -> 81;

250 [label="ONLY EVAL with clause\nno(X71) :- ','(call(X71), ','(!_9, failure(a))).\nand substitutionT41 -> T44,\nX71 -> empty(T44)", fontsize=14, style = filled, fillcolor = lightblue];
81 -> 250 [arrowhead = none ];
250 -> 84;

251 [label="CALL", fontsize=14, style = filled, fillcolor = lightcyan];
84 -> 251 [arrowhead = none ];
251 -> 86;

252 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
86 -> 252 [arrowhead = none ];
252 -> 88;

253 [label="EVAL with clause\nempty([]).\nand substitutionT44 -> []", fontsize=14, style = filled, fillcolor = lightblue];
88 -> 253 [arrowhead = none ];
253 -> 90;

254 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
88 -> 254 [arrowhead = none ];
254 -> 93;

255 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
90 -> 255 [arrowhead = none ];
255 -> 95;

256 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
93 -> 256 [arrowhead = none ];
256 -> 101;

257 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
95 -> 257 [arrowhead = none ];
257 -> 98;

258 [label="BACKTRACK\nfor clause: failure(b)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
98 -> 258 [arrowhead = none ];
258 -> 99;

259 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
101 -> 259 [arrowhead = none ];
259 -> 102;

260 [label="ONLY EVAL with clause\nno(X74).\nand substitutionT44 -> T47,\nX74 -> empty(T47)", fontsize=14, style = filled, fillcolor = lightblue];
102 -> 260 [arrowhead = none ];
260 -> 105;

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

262 [label="BACKTRACK\nfor clause: head([], X1)\nwith clash: (empty(T47), empty([]))", fontsize=14, style = filled, fillcolor = lightgreen];
107 -> 262 [arrowhead = none ];
262 -> 108;

263 [label="EVAL with clause\nhead(.(X80, X81), X80).\nand substitutionX80 -> T53,\nX81 -> T54,\nT47 -> .(T53, T54),\nT40 -> T53", fontsize=14, style = filled, fillcolor = lightblue];
108 -> 263 [arrowhead = none ];
263 -> 111;

264 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
108 -> 264 [arrowhead = none ];
264 -> 113;

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

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

267 [label="ONLY EVAL with clause\nno(X98) :- ','(call(X98), ','(!_14, failure(a))).\nand substitutionT61 -> T65,\nX98 -> empty(T65)", fontsize=14, style = filled, fillcolor = lightblue];
143 -> 267 [arrowhead = none ];
267 -> 148;

268 [label="CALL", fontsize=14, style = filled, fillcolor = lightcyan];
148 -> 268 [arrowhead = none ];
268 -> 150;

269 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
150 -> 269 [arrowhead = none ];
269 -> 151;

270 [label="EVAL with clause\nempty([]).\nand substitutionT65 -> []", fontsize=14, style = filled, fillcolor = lightblue];
151 -> 270 [arrowhead = none ];
270 -> 152;

271 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
151 -> 271 [arrowhead = none ];
271 -> 154;

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

273 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
154 -> 273 [arrowhead = none ];
273 -> 160;

274 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
155 -> 274 [arrowhead = none ];
274 -> 157;

275 [label="BACKTRACK\nfor clause: failure(b)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
157 -> 275 [arrowhead = none ];
275 -> 159;

276 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
160 -> 276 [arrowhead = none ];
276 -> 161;

277 [label="ONLY EVAL with clause\nno(X107).\nand substitutionT65 -> T70,\nX107 -> empty(T70)", fontsize=14, style = filled, fillcolor = lightblue];
161 -> 277 [arrowhead = none ];
277 -> 164;

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

279 [label="BACKTRACK\nfor clause: tail([], [])\nwith clash: (empty(T70), empty([]))", fontsize=14, style = filled, fillcolor = lightgreen];
165 -> 279 [arrowhead = none ];
279 -> 166;

280 [label="EVAL with clause\ntail(.(X115, X116), X116).\nand substitutionX115 -> T76,\nX116 -> T77,\nT70 -> .(T76, T77),\nX92 -> T77", fontsize=14, style = filled, fillcolor = lightblue];
166 -> 280 [arrowhead = none ];
280 -> 171;

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

282 [label="INSTANCE with matching:\nT28 -> T60\nT6 -> T77", fontsize=14, style = filled, fillcolor = lightgrey];
171 -> 282 [arrowhead = none , style=dashed];
282 -> 66[style=dashed];

283 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
189 -> 283 [arrowhead = none ];
283 -> 196;

284 [label="ONLY EVAL with clause\nno(X140) :- ','(call(X140), ','(!_19, failure(a))).\nand substitutionT82 -> T85,\nX140 -> empty(T85)", fontsize=14, style = filled, fillcolor = lightblue];
196 -> 284 [arrowhead = none ];
284 -> 199;

285 [label="CALL", fontsize=14, style = filled, fillcolor = lightcyan];
199 -> 285 [arrowhead = none ];
285 -> 202;

286 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
202 -> 286 [arrowhead = none ];
286 -> 203;

287 [label="EVAL with clause\nempty([]).\nand substitutionT85 -> []", fontsize=14, style = filled, fillcolor = lightblue];
203 -> 287 [arrowhead = none ];
287 -> 205;

288 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
203 -> 288 [arrowhead = none ];
288 -> 207;

289 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
205 -> 289 [arrowhead = none ];
289 -> 208;

290 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
207 -> 290 [arrowhead = none ];
290 -> 211;

291 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
208 -> 291 [arrowhead = none ];
291 -> 209;

292 [label="BACKTRACK\nfor clause: failure(b)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
209 -> 292 [arrowhead = none ];
292 -> 210;

293 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
211 -> 293 [arrowhead = none ];
293 -> 213;

294 [label="ONLY EVAL with clause\nno(X151).\nand substitutionT85 -> T88,\nX151 -> empty(T88)", fontsize=14, style = filled, fillcolor = lightblue];
213 -> 294 [arrowhead = none ];
294 -> 215;

295 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
215 -> 295 [arrowhead = none ];
295 -> 216;

296 [label="BACKTRACK\nfor clause: tail([], [])\nwith clash: (empty(T88), empty([]))", fontsize=14, style = filled, fillcolor = lightgreen];
216 -> 296 [arrowhead = none ];
296 -> 217;

297 [label="EVAL with clause\ntail(.(X160, X161), X161).\nand substitutionX160 -> T93,\nX161 -> T94,\nT88 -> .(T93, T94),\nX132 -> T94", fontsize=14, style = filled, fillcolor = lightblue];
217 -> 297 [arrowhead = none ];
297 -> 219;

298 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
217 -> 298 [arrowhead = none ];
298 -> 220;

299 [label="INSTANCE with matching:\nX9 -> X133\nT5 -> T94", fontsize=14, style = filled, fillcolor = lightgrey];
219 -> 299 [arrowhead = none , style=dashed];
299 -> 7[style=dashed];

}

(2) Obligation:

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

overlapA_in_gg(T5, T6) → U1_gg(T5, T6, pB_in_agg(X9, T5, T6))
pB_in_agg(T28, .(T28, T29), T6) → U3_agg(T28, T29, T6, memberC_in_gg(T28, T6))
memberC_in_gg(T53, .(T53, T54)) → memberC_out_gg(T53, .(T53, T54))
memberC_in_gg(T60, .(T76, T77)) → U2_gg(T60, T76, T77, memberC_in_gg(T60, T77))
U2_gg(T60, T76, T77, memberC_out_gg(T60, T77)) → memberC_out_gg(T60, .(T76, T77))
U3_agg(T28, T29, T6, memberC_out_gg(T28, T6)) → pB_out_agg(T28, .(T28, T29), T6)
pB_in_agg(X133, .(T93, T94), T6) → U4_agg(X133, T93, T94, T6, pB_in_agg(X133, T94, T6))
U4_agg(X133, T93, T94, T6, pB_out_agg(X133, T94, T6)) → pB_out_agg(X133, .(T93, T94), T6)
U1_gg(T5, T6, pB_out_agg(X9, T5, T6)) → overlapA_out_gg(T5, T6)

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

OVERLAPA_IN_GG(T5, T6) → U1_GG(T5, T6, pB_in_agg(X9, T5, T6))
OVERLAPA_IN_GG(T5, T6) → PB_IN_AGG(X9, T5, T6)
PB_IN_AGG(T28, .(T28, T29), T6) → U3_AGG(T28, T29, T6, memberC_in_gg(T28, T6))
PB_IN_AGG(T28, .(T28, T29), T6) → MEMBERC_IN_GG(T28, T6)
MEMBERC_IN_GG(T60, .(T76, T77)) → U2_GG(T60, T76, T77, memberC_in_gg(T60, T77))
MEMBERC_IN_GG(T60, .(T76, T77)) → MEMBERC_IN_GG(T60, T77)
PB_IN_AGG(X133, .(T93, T94), T6) → U4_AGG(X133, T93, T94, T6, pB_in_agg(X133, T94, T6))
PB_IN_AGG(X133, .(T93, T94), T6) → PB_IN_AGG(X133, T94, T6)

The TRS R consists of the following rules:

overlapA_in_gg(T5, T6) → U1_gg(T5, T6, pB_in_agg(X9, T5, T6))
pB_in_agg(T28, .(T28, T29), T6) → U3_agg(T28, T29, T6, memberC_in_gg(T28, T6))
memberC_in_gg(T53, .(T53, T54)) → memberC_out_gg(T53, .(T53, T54))
memberC_in_gg(T60, .(T76, T77)) → U2_gg(T60, T76, T77, memberC_in_gg(T60, T77))
U2_gg(T60, T76, T77, memberC_out_gg(T60, T77)) → memberC_out_gg(T60, .(T76, T77))
U3_agg(T28, T29, T6, memberC_out_gg(T28, T6)) → pB_out_agg(T28, .(T28, T29), T6)
pB_in_agg(X133, .(T93, T94), T6) → U4_agg(X133, T93, T94, T6, pB_in_agg(X133, T94, T6))
U4_agg(X133, T93, T94, T6, pB_out_agg(X133, T94, T6)) → pB_out_agg(X133, .(T93, T94), T6)
U1_gg(T5, T6, pB_out_agg(X9, T5, T6)) → overlapA_out_gg(T5, T6)

The argument filtering Pi contains the following mapping:
overlapA_in_gg(x1, x2) = overlapA_in_gg(x1, x2)
U1_gg(x1, x2, x3) = U1_gg(x1, x2, x3)
pB_in_agg(x1, x2, x3) = pB_in_agg(x2, x3)
.(x1, x2) = .(x1, x2)
U3_agg(x1, x2, x3, x4) = U3_agg(x1, x2, x3, x4)
memberC_in_gg(x1, x2) = memberC_in_gg(x1, x2)
memberC_out_gg(x1, x2) = memberC_out_gg(x1, x2)
U2_gg(x1, x2, x3, x4) = U2_gg(x1, x2, x3, x4)
pB_out_agg(x1, x2, x3) = pB_out_agg(x1, x2, x3)
U4_agg(x1, x2, x3, x4, x5) = U4_agg(x2, x3, x4, x5)
overlapA_out_gg(x1, x2) = overlapA_out_gg(x1, x2)
OVERLAPA_IN_GG(x1, x2) = OVERLAPA_IN_GG(x1, x2)
U1_GG(x1, x2, x3) = U1_GG(x1, x2, x3)
PB_IN_AGG(x1, x2, x3) = PB_IN_AGG(x2, x3)
U3_AGG(x1, x2, x3, x4) = U3_AGG(x1, x2, x3, x4)
MEMBERC_IN_GG(x1, x2) = MEMBERC_IN_GG(x1, x2)
U2_GG(x1, x2, x3, x4) = U2_GG(x1, x2, x3, x4)
U4_AGG(x1, x2, x3, x4, x5) = U4_AGG(x2, x3, x4, x5)

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

(4) Obligation:

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

OVERLAPA_IN_GG(T5, T6) → U1_GG(T5, T6, pB_in_agg(X9, T5, T6))
OVERLAPA_IN_GG(T5, T6) → PB_IN_AGG(X9, T5, T6)
PB_IN_AGG(T28, .(T28, T29), T6) → U3_AGG(T28, T29, T6, memberC_in_gg(T28, T6))
PB_IN_AGG(T28, .(T28, T29), T6) → MEMBERC_IN_GG(T28, T6)
MEMBERC_IN_GG(T60, .(T76, T77)) → U2_GG(T60, T76, T77, memberC_in_gg(T60, T77))
MEMBERC_IN_GG(T60, .(T76, T77)) → MEMBERC_IN_GG(T60, T77)
PB_IN_AGG(X133, .(T93, T94), T6) → U4_AGG(X133, T93, T94, T6, pB_in_agg(X133, T94, T6))
PB_IN_AGG(X133, .(T93, T94), T6) → PB_IN_AGG(X133, T94, T6)

The TRS R consists of the following rules:

overlapA_in_gg(T5, T6) → U1_gg(T5, T6, pB_in_agg(X9, T5, T6))
pB_in_agg(T28, .(T28, T29), T6) → U3_agg(T28, T29, T6, memberC_in_gg(T28, T6))
memberC_in_gg(T53, .(T53, T54)) → memberC_out_gg(T53, .(T53, T54))
memberC_in_gg(T60, .(T76, T77)) → U2_gg(T60, T76, T77, memberC_in_gg(T60, T77))
U2_gg(T60, T76, T77, memberC_out_gg(T60, T77)) → memberC_out_gg(T60, .(T76, T77))
U3_agg(T28, T29, T6, memberC_out_gg(T28, T6)) → pB_out_agg(T28, .(T28, T29), T6)
pB_in_agg(X133, .(T93, T94), T6) → U4_agg(X133, T93, T94, T6, pB_in_agg(X133, T94, T6))
U4_agg(X133, T93, T94, T6, pB_out_agg(X133, T94, T6)) → pB_out_agg(X133, .(T93, T94), T6)
U1_gg(T5, T6, pB_out_agg(X9, T5, T6)) → overlapA_out_gg(T5, T6)

(5) DependencyGraphProof (EQUIVALENT transformation)

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

(6) Complex Obligation (AND)

(7) Obligation:

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

MEMBERC_IN_GG(T60, .(T76, T77)) → MEMBERC_IN_GG(T60, T77)

The TRS R consists of the following rules:

overlapA_in_gg(T5, T6) → U1_gg(T5, T6, pB_in_agg(X9, T5, T6))
pB_in_agg(T28, .(T28, T29), T6) → U3_agg(T28, T29, T6, memberC_in_gg(T28, T6))
memberC_in_gg(T53, .(T53, T54)) → memberC_out_gg(T53, .(T53, T54))
memberC_in_gg(T60, .(T76, T77)) → U2_gg(T60, T76, T77, memberC_in_gg(T60, T77))
U2_gg(T60, T76, T77, memberC_out_gg(T60, T77)) → memberC_out_gg(T60, .(T76, T77))
U3_agg(T28, T29, T6, memberC_out_gg(T28, T6)) → pB_out_agg(T28, .(T28, T29), T6)
pB_in_agg(X133, .(T93, T94), T6) → U4_agg(X133, T93, T94, T6, pB_in_agg(X133, T94, T6))
U4_agg(X133, T93, T94, T6, pB_out_agg(X133, T94, T6)) → pB_out_agg(X133, .(T93, T94), T6)
U1_gg(T5, T6, pB_out_agg(X9, T5, T6)) → overlapA_out_gg(T5, T6)

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

MEMBERC_IN_GG(T60, .(T76, T77)) → MEMBERC_IN_GG(T60, T77)

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:

MEMBERC_IN_GG(T60, .(T76, T77)) → MEMBERC_IN_GG(T60, T77)

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:

MEMBERC_IN_GG(T60, .(T76, T77)) → MEMBERC_IN_GG(T60, T77)
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_AGG(X133, .(T93, T94), T6) → PB_IN_AGG(X133, T94, T6)

The TRS R consists of the following rules:

overlapA_in_gg(T5, T6) → U1_gg(T5, T6, pB_in_agg(X9, T5, T6))
pB_in_agg(T28, .(T28, T29), T6) → U3_agg(T28, T29, T6, memberC_in_gg(T28, T6))
memberC_in_gg(T53, .(T53, T54)) → memberC_out_gg(T53, .(T53, T54))
memberC_in_gg(T60, .(T76, T77)) → U2_gg(T60, T76, T77, memberC_in_gg(T60, T77))
U2_gg(T60, T76, T77, memberC_out_gg(T60, T77)) → memberC_out_gg(T60, .(T76, T77))
U3_agg(T28, T29, T6, memberC_out_gg(T28, T6)) → pB_out_agg(T28, .(T28, T29), T6)
pB_in_agg(X133, .(T93, T94), T6) → U4_agg(X133, T93, T94, T6, pB_in_agg(X133, T94, T6))
U4_agg(X133, T93, T94, T6, pB_out_agg(X133, T94, T6)) → pB_out_agg(X133, .(T93, T94), T6)
U1_gg(T5, T6, pB_out_agg(X9, T5, T6)) → overlapA_out_gg(T5, T6)

(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_AGG(X133, .(T93, T94), T6) → PB_IN_AGG(X133, T94, T6)

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

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_AGG(.(T93, T94), T6) → PB_IN_AGG(T94, T6)

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:

PB_IN_AGG(.(T93, T94), T6) → PB_IN_AGG(T94, T6)
The graph contains the following edges 1 > 1, 2 >= 2

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

(18) Obligation:

(19) QDPSizeChangeProof (EQUIVALENT transformation)

(20) YES