Left Termination proof of /tmp/tmp0PX5JL/t.pl

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

0 Prolog

↳1 PrologToPiTRSViaGraphTransformerProof (⇒, 158 ms)

↳2 PiTRS

↳3 DependencyPairsProof (⇔, 86 ms)

↳4 PiDP

↳5 DependencyGraphProof (⇔, 0 ms)

↳6 AND

    ↳7 PiDP

        ↳8 UsableRulesProof (⇔, 0 ms)

        ↳9 PiDP

        ↳10 PiDPToQDPProof (⇒, 0 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 (⇒, 0 ms)

        ↳25 QDP

        ↳26 QDPSizeChangeProof (⇔, 0 ms)

        ↳27 YES

    ↳28 PiDP

        ↳29 UsableRulesProof (⇔, 0 ms)

        ↳30 PiDP

        ↳31 PiDPToQDPProof (⇒, 0 ms)

        ↳32 QDP

        ↳33 QDPOrderProof (⇔, 110 ms)

        ↳34 QDP

        ↳35 DependencyGraphProof (⇔, 0 ms)

        ↳36 TRUE

(0) Obligation:

Clauses:

t(N) :- ','(ll(N, Xs), ','(select(X1, Xs, Xs1), ','(ll(M, Xs1), t(M)))).
t(0).
ll(s(N), .(X, Xs)) :- ll(N, Xs).
ll(0, []).
select(X, .(Y, Xs), .(Y, Ys)) :- select(X, Xs, Ys).
select(X, .(X, Xs), Xs).

Query: t(g)

(1) PrologToPiTRSViaGraphTransformerProof (SOUND transformation)

Transformed Prolog program to (Pi-)TRS.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
3 [label="A: t(T1)\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
4 [label="4: t(T1), SCOPE: 1, CLAUSE: 0 | t(T1), SCOPE: 1, CLAUSE: 1\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
7 [label="7: ','(ll(T3, X4), ','(select(X5, X4, X6), ','(ll(X7, X6), t(X7)))) | t(T3), SCOPE: 1, CLAUSE: 1\n\nT3 is ground\nX4 is free\nX5 is free\nX6 is free\nX7 is free", fontsize=16, style=filled, fillcolor=lightyellow];
10 [label="10: ','(ll(T3, X4), ','(select(X5, X4, X6), ','(ll(X7, X6), t(X7)))), SCOPE: 2, CLAUSE: 2 | ','(ll(T3, X4), ','(select(X5, X4, X6), ','(ll(X7, X6), t(X7)))), SCOPE: 2, CLAUSE: 3 | ?_2 | t(T3), SCOPE: 1, CLAUSE: 1\n\nT3 is ground\nX4 is free\nX5 is free\nX6 is free\nX7 is free", fontsize=16, style=filled, fillcolor=lightyellow];
11 [label="11: ','(ll(T3, X4), ','(select(X5, X4, X6), ','(ll(X7, X6), t(X7)))), SCOPE: 2, CLAUSE: 2\n\nT3 is ground\nX4 is free\nX5 is free\nX6 is free\nX7 is free", fontsize=16, style=filled, fillcolor=lightyellow];
12 [label="12: ','(ll(T3, X4), ','(select(X5, X4, X6), ','(ll(X7, X6), t(X7)))), SCOPE: 2, CLAUSE: 3 | ?_2 | t(T3), SCOPE: 1, CLAUSE: 1\n\nT3 is ground\nX4 is free\nX5 is free\nX6 is free\nX7 is free", fontsize=16, style=filled, fillcolor=lightyellow];
14 [label="B: ','(ll(T8, X32), ','(select(X5, .(X31, X32), X6), ','(ll(X7, X6), t(X7))))\n\nT8 is ground\nX5 is free\nX6 is free\nX7 is free\nX31 is free\nX32 is free", fontsize=16, style=filled, fillcolor=lightyellow];
19 [label="19: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
24 [label="D: ll(T8, X32)\n\nT8 is ground\nX32 is free", fontsize=16, style=filled, fillcolor=lightyellow];
25 [label="I: ','(select(X5, .(X31, T10), X6), ','(ll(X7, X6), t(X7)))\n\nX5 is free\nX6 is free\nX7 is free\nX31 is free", fontsize=16, style=filled, fillcolor=lightyellow];
30 [label="30: ll(T8, X32), SCOPE: 3, CLAUSE: 2 | ll(T8, X32), SCOPE: 3, CLAUSE: 3\n\nT8 is ground\nX32 is free", fontsize=16, style=filled, fillcolor=lightyellow];
33 [label="33: ll(T8, X32), SCOPE: 3, CLAUSE: 2\n\nT8 is ground\nX32 is free", fontsize=16, style=filled, fillcolor=lightyellow];
34 [label="34: ll(T8, X32), SCOPE: 3, CLAUSE: 3\n\nT8 is ground\nX32 is free", fontsize=16, style=filled, fillcolor=lightyellow];
39 [label="39: ll(T16, X67)\n\nT16 is ground\nX67 is free", fontsize=16, style=filled, fillcolor=lightyellow];
40 [label="40: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
46 [label="46: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
47 [label="47: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
48 [label="48: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
54 [label="H: select(X5, .(X31, T10), X6)\n\nX5 is free\nX6 is free\nX31 is free", fontsize=16, style=filled, fillcolor=lightyellow];
55 [label="J: ','(ll(X7, T21), t(X7))\n\nX7 is free", fontsize=16, style=filled, fillcolor=lightyellow];
57 [label="57: select(X5, .(X31, T10), X6), SCOPE: 4, CLAUSE: 4 | select(X5, .(X31, T10), X6), SCOPE: 4, CLAUSE: 5\n\nX5 is free\nX6 is free\nX31 is free", fontsize=16, style=filled, fillcolor=lightyellow];
63 [label="63: select(X5, .(X31, T10), X6), SCOPE: 4, CLAUSE: 4\n\nX5 is free\nX6 is free\nX31 is free", fontsize=16, style=filled, fillcolor=lightyellow];
64 [label="64: select(X5, .(X31, T10), X6), SCOPE: 4, CLAUSE: 5\n\nX5 is free\nX6 is free\nX31 is free", fontsize=16, style=filled, fillcolor=lightyellow];
70 [label="E: select(X131, T34, X133)\n\nX131 is free\nX133 is free", fontsize=16, style=filled, fillcolor=lightyellow];
73 [label="73: select(X131, T34, X133), SCOPE: 5, CLAUSE: 4 | select(X131, T34, X133), SCOPE: 5, CLAUSE: 5\n\nX131 is free\nX133 is free", fontsize=16, style=filled, fillcolor=lightyellow];
75 [label="75: select(X131, T34, X133), SCOPE: 5, CLAUSE: 4\n\nX131 is free\nX133 is free", fontsize=16, style=filled, fillcolor=lightyellow];
76 [label="76: select(X131, T34, X133), SCOPE: 5, CLAUSE: 5\n\nX131 is free\nX133 is free", fontsize=16, style=filled, fillcolor=lightyellow];
83 [label="83: select(X168, T47, X169)\n\nX168 is free\nX169 is free", fontsize=16, style=filled, fillcolor=lightyellow];
84 [label="84: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
92 [label="92: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
93 [label="93: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
94 [label="94: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
95 [label="95: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
96 [label="96: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
98 [label="F: ll(X7, T21)\n\nX7 is free", fontsize=16, style=filled, fillcolor=lightyellow];
99 [label="99: t(T61)\n\nT61 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
102 [label="102: ll(X7, T21), SCOPE: 6, CLAUSE: 2 | ll(X7, T21), SCOPE: 6, CLAUSE: 3\n\nX7 is free", fontsize=16, style=filled, fillcolor=lightyellow];
103 [label="103: ll(X7, T21), SCOPE: 6, CLAUSE: 2\n\nX7 is free", fontsize=16, style=filled, fillcolor=lightyellow];
104 [label="104: ll(X7, T21), SCOPE: 6, CLAUSE: 3\n\nX7 is free", fontsize=16, style=filled, fillcolor=lightyellow];
105 [label="105: ll(X221, T74)\n\nX221 is free", fontsize=16, style=filled, fillcolor=lightyellow];
106 [label="106: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
107 [label="107: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
108 [label="108: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
109 [label="109: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
110 [label="110: ','(ll(T3, X4), ','(select(X5, X4, X6), ','(ll(X7, X6), t(X7)))), SCOPE: 2, CLAUSE: 3\n\nT3 is ground\nX4 is free\nX5 is free\nX6 is free\nX7 is free", fontsize=16, style=filled, fillcolor=lightyellow];
111 [label="111: ?_2 | t(T3), SCOPE: 1, CLAUSE: 1\n\nT3 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
112 [label="C: ','(select(X5, [], X6), ','(ll(X7, X6), t(X7)))\n\nX5 is free\nX6 is free\nX7 is free", fontsize=16, style=filled, fillcolor=lightyellow];
113 [label="113: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
114 [label="K: select(X5, [], X6)\n\nX5 is free\nX6 is free", fontsize=16, style=filled, fillcolor=lightyellow];
115 [label="L: ','(ll(X7, T79), t(X7))\n\nT79 is ground\nX7 is free", fontsize=16, style=filled, fillcolor=lightyellow];
116 [label="116: select(X5, [], X6), SCOPE: 7, CLAUSE: 4 | select(X5, [], X6), SCOPE: 7, CLAUSE: 5\n\nX5 is free\nX6 is free", fontsize=16, style=filled, fillcolor=lightyellow];
119 [label="119: select(X5, [], X6), SCOPE: 7, CLAUSE: 5\n\nX5 is free\nX6 is free", fontsize=16, style=filled, fillcolor=lightyellow];
120 [label="120: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
124 [label="G: ll(X7, T79)\n\nT79 is ground\nX7 is free", fontsize=16, style=filled, fillcolor=lightyellow];
125 [label="125: t(T82)\n\nT82 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
126 [label="126: ll(X7, T79), SCOPE: 8, CLAUSE: 2 | ll(X7, T79), SCOPE: 8, CLAUSE: 3\n\nT79 is ground\nX7 is free", fontsize=16, style=filled, fillcolor=lightyellow];
127 [label="127: ll(X7, T79), SCOPE: 8, CLAUSE: 2\n\nT79 is ground\nX7 is free", fontsize=16, style=filled, fillcolor=lightyellow];
128 [label="128: ll(X7, T79), SCOPE: 8, CLAUSE: 3\n\nT79 is ground\nX7 is free", fontsize=16, style=filled, fillcolor=lightyellow];
129 [label="129: ll(X276, T94)\n\nT94 is ground\nX276 is free", fontsize=16, style=filled, fillcolor=lightyellow];
130 [label="130: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
133 [label="133: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
134 [label="134: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
135 [label="135: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
138 [label="138: t(T3), SCOPE: 1, CLAUSE: 1\n\nT3 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
140 [label="140: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
141 [label="141: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
142 [label="142: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
143 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
3 -> 143 [arrowhead = none ];
143 -> 4;

144 [label="ONLY EVAL with clause\nt(X3) :- ','(ll(X3, X4), ','(select(X5, X4, X6), ','(ll(X7, X6), t(X7)))).\nand substitutionT1 -> T3,\nX3 -> T3", fontsize=14, style = filled, fillcolor = lightblue];
4 -> 144 [arrowhead = none ];
144 -> 7;

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

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

147 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
10 -> 147 [arrowhead = none ];
147 -> 12;

148 [label="EVAL with clause\nll(s(X28), .(X29, X30)) :- ll(X28, X30).\nand substitutionX28 -> T8,\nT3 -> s(T8),\nX29 -> X31,\nX30 -> X32,\nX4 -> .(X31, X32)", fontsize=14, style = filled, fillcolor = lightblue];
11 -> 148 [arrowhead = none ];
148 -> 14;

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

150 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
12 -> 150 [arrowhead = none ];
150 -> 110;

151 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
12 -> 151 [arrowhead = none ];
151 -> 111;

152 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
14 -> 152 [arrowhead = none ];
152 -> 24;

153 [label="SPLIT 2\nnew knowledge:\nT8 is ground\nreplacements:X32 -> T10", fontsize=14, style = filled, fillcolor = violet];
14 -> 153 [arrowhead = none ];
153 -> 25;

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

155 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
25 -> 155 [arrowhead = none ];
155 -> 54;

156 [label="SPLIT 2\nreplacements:X5 -> T19,\nX31 -> T20,\nX6 -> T21", fontsize=14, style = filled, fillcolor = violet];
25 -> 156 [arrowhead = none ];
156 -> 55;

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

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

159 [label="EVAL with clause\nll(s(X63), .(X64, X65)) :- ll(X63, X65).\nand substitutionX63 -> T16,\nT8 -> s(T16),\nX64 -> X66,\nX65 -> X67,\nX32 -> .(X66, X67)", fontsize=14, style = filled, fillcolor = lightblue];
33 -> 159 [arrowhead = none ];
159 -> 39;

160 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
33 -> 160 [arrowhead = none ];
160 -> 40;

161 [label="EVAL with clause\nll(0, []).\nand substitutionT8 -> 0,\nX32 -> []", fontsize=14, style = filled, fillcolor = lightblue];
34 -> 161 [arrowhead = none ];
161 -> 46;

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

163 [label="INSTANCE with matching:\nT8 -> T16\nX32 -> X67", fontsize=14, style = filled, fillcolor = lightgrey];
39 -> 163 [arrowhead = none , style=dashed];
163 -> 24[style=dashed];

164 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
46 -> 164 [arrowhead = none ];
164 -> 48;

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

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

167 [label="SPLIT 2\nnew knowledge:\nT61 is ground\nreplacements:X7 -> T61", fontsize=14, style = filled, fillcolor = violet];
55 -> 167 [arrowhead = none ];
167 -> 99;

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

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

170 [label="ONLY EVAL with clause\nselect(X127, .(X128, X129), .(X128, X130)) :- select(X127, X129, X130).\nand substitutionX5 -> X131,\nX127 -> X131,\nX31 -> X132,\nX128 -> X132,\nT10 -> T34,\nX129 -> T34,\nX130 -> X133,\nX6 -> .(X132, X133),\nT33 -> T34", fontsize=14, style = filled, fillcolor = lightblue];
63 -> 170 [arrowhead = none ];
170 -> 70;

171 [label="ONLY EVAL with clause\nselect(X191, .(X191, X192), X192).\nand substitutionX5 -> X193,\nX191 -> X193,\nX31 -> X193,\nT10 -> T58,\nX192 -> T58,\nX6 -> T58", fontsize=14, style = filled, fillcolor = lightblue];
64 -> 171 [arrowhead = none ];
171 -> 95;

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

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

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

175 [label="EVAL with clause\nselect(X164, .(X165, X166), .(X165, X167)) :- select(X164, X166, X167).\nand substitutionX131 -> X168,\nX164 -> X168,\nX165 -> T45,\nX166 -> T47,\nT34 -> .(T45, T47),\nX167 -> X169,\nX133 -> .(T45, X169),\nT46 -> T47", fontsize=14, style = filled, fillcolor = lightblue];
75 -> 175 [arrowhead = none ];
175 -> 83;

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

177 [label="EVAL with clause\nselect(X182, .(X182, X183), X183).\nand substitutionX131 -> T54,\nX182 -> T54,\nX184 -> T54,\nX183 -> T55,\nT34 -> .(T54, T55),\nX133 -> T55", fontsize=14, style = filled, fillcolor = lightblue];
76 -> 177 [arrowhead = none ];
177 -> 92;

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

179 [label="INSTANCE with matching:\nX131 -> X168\nT34 -> T47\nX133 -> X169", fontsize=14, style = filled, fillcolor = lightgrey];
83 -> 179 [arrowhead = none , style=dashed];
179 -> 70[style=dashed];

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

181 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
95 -> 181 [arrowhead = none ];
181 -> 96;

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

183 [label="INSTANCE with matching:\nT1 -> T61", fontsize=14, style = filled, fillcolor = lightgrey];
99 -> 183 [arrowhead = none , style=dashed];
183 -> 3[style=dashed];

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

185 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
102 -> 185 [arrowhead = none ];
185 -> 104;

186 [label="EVAL with clause\nll(s(X218), .(X219, X220)) :- ll(X218, X220).\nand substitutionX218 -> X221,\nX7 -> s(X221),\nX219 -> T72,\nX220 -> T74,\nT21 -> .(T72, T74),\nT73 -> T74", fontsize=14, style = filled, fillcolor = lightblue];
103 -> 186 [arrowhead = none ];
186 -> 105;

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

188 [label="EVAL with clause\nll(0, []).\nand substitutionX7 -> 0,\nT21 -> []", fontsize=14, style = filled, fillcolor = lightblue];
104 -> 188 [arrowhead = none ];
188 -> 107;

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

190 [label="INSTANCE with matching:\nX7 -> X221\nT21 -> T74", fontsize=14, style = filled, fillcolor = lightgrey];
105 -> 190 [arrowhead = none , style=dashed];
190 -> 98[style=dashed];

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

192 [label="EVAL with clause\nll(0, []).\nand substitutionT3 -> 0,\nX4 -> []", fontsize=14, style = filled, fillcolor = lightblue];
110 -> 192 [arrowhead = none ];
192 -> 112;

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

194 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
111 -> 194 [arrowhead = none ];
194 -> 138;

195 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
112 -> 195 [arrowhead = none ];
195 -> 114;

196 [label="SPLIT 2\nnew knowledge:\nT78 is ground\nT79 is ground\nreplacements:X5 -> T78,\nX6 -> T79", fontsize=14, style = filled, fillcolor = violet];
112 -> 196 [arrowhead = none ];
196 -> 115;

197 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
114 -> 197 [arrowhead = none ];
197 -> 116;

198 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
115 -> 198 [arrowhead = none ];
198 -> 124;

199 [label="SPLIT 2\nnew knowledge:\nT82 is ground\nT79 is ground\nreplacements:X7 -> T82", fontsize=14, style = filled, fillcolor = violet];
115 -> 199 [arrowhead = none ];
199 -> 125;

200 [label="BACKTRACK\nfor clause: select(X, .(Y, Xs), .(Y, Ys)) :- select(X, Xs, Ys)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
116 -> 200 [arrowhead = none ];
200 -> 119;

201 [label="BACKTRACK\nfor clause: select(X, .(X, Xs), Xs)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
119 -> 201 [arrowhead = none ];
201 -> 120;

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

203 [label="INSTANCE with matching:\nT1 -> T82", fontsize=14, style = filled, fillcolor = lightgrey];
125 -> 203 [arrowhead = none , style=dashed];
203 -> 3[style=dashed];

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

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

206 [label="EVAL with clause\nll(s(X273), .(X274, X275)) :- ll(X273, X275).\nand substitutionX273 -> X276,\nX7 -> s(X276),\nX274 -> T93,\nX275 -> T94,\nT79 -> .(T93, T94)", fontsize=14, style = filled, fillcolor = lightblue];
127 -> 206 [arrowhead = none ];
206 -> 129;

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

208 [label="EVAL with clause\nll(0, []).\nand substitutionX7 -> 0,\nT79 -> []", fontsize=14, style = filled, fillcolor = lightblue];
128 -> 208 [arrowhead = none ];
208 -> 133;

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

210 [label="INSTANCE with matching:\nX7 -> X276\nT79 -> T94", fontsize=14, style = filled, fillcolor = lightgrey];
129 -> 210 [arrowhead = none , style=dashed];
210 -> 124[style=dashed];

211 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
133 -> 211 [arrowhead = none ];
211 -> 135;

212 [label="EVAL with clause\nt(0).\nand substitutionT3 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
138 -> 212 [arrowhead = none ];
212 -> 140;

213 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
138 -> 213 [arrowhead = none ];
213 -> 141;

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

}

(2) Obligation:

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

tA_in_g(s(T8)) → U1_g(T8, pB_in_gaaaaa(T8, X32, X5, X31, X6, X7))
pB_in_gaaaaa(T8, T10, X5, X31, X6, X7) → U7_gaaaaa(T8, T10, X5, X31, X6, X7, llD_in_ga(T8, T10))
llD_in_ga(s(T16), .(X66, X67)) → U2_ga(T16, X66, X67, llD_in_ga(T16, X67))
llD_in_ga(0, []) → llD_out_ga(0, [])
U2_ga(T16, X66, X67, llD_out_ga(T16, X67)) → llD_out_ga(s(T16), .(X66, X67))
U7_gaaaaa(T8, T10, X5, X31, X6, X7, llD_out_ga(T8, T10)) → U8_gaaaaa(T8, T10, X5, X31, X6, X7, pI_in_aagaa(X5, X31, T10, X6, X7))
pI_in_aagaa(T19, T20, T10, T21, X7) → U9_aagaa(T19, T20, T10, T21, X7, selectH_in_aaga(T19, T20, T10, T21))
selectH_in_aaga(X131, X132, T34, .(X132, X133)) → U6_aaga(X131, X132, T34, X133, selectE_in_aga(X131, T34, X133))
selectE_in_aga(X168, .(T45, T47), .(T45, X169)) → U3_aga(X168, T45, T47, X169, selectE_in_aga(X168, T47, X169))
selectE_in_aga(T54, .(T54, T55), T55) → selectE_out_aga(T54, .(T54, T55), T55)
U3_aga(X168, T45, T47, X169, selectE_out_aga(X168, T47, X169)) → selectE_out_aga(X168, .(T45, T47), .(T45, X169))
U6_aaga(X131, X132, T34, X133, selectE_out_aga(X131, T34, X133)) → selectH_out_aaga(X131, X132, T34, .(X132, X133))
selectH_in_aaga(X193, X193, T58, T58) → selectH_out_aaga(X193, X193, T58, T58)
U9_aagaa(T19, T20, T10, T21, X7, selectH_out_aaga(T19, T20, T10, T21)) → U10_aagaa(T19, T20, T10, T21, X7, pJ_in_ag(X7, T21))
pJ_in_ag(T61, T21) → U11_ag(T61, T21, llF_in_ag(T61, T21))
llF_in_ag(s(X221), .(T72, T74)) → U4_ag(X221, T72, T74, llF_in_ag(X221, T74))
llF_in_ag(0, []) → llF_out_ag(0, [])
U4_ag(X221, T72, T74, llF_out_ag(X221, T74)) → llF_out_ag(s(X221), .(T72, T74))
U11_ag(T61, T21, llF_out_ag(T61, T21)) → U12_ag(T61, T21, tA_in_g(T61))
tA_in_g(0) → tA_out_g(0)
U12_ag(T61, T21, tA_out_g(T61)) → pJ_out_ag(T61, T21)
U10_aagaa(T19, T20, T10, T21, X7, pJ_out_ag(X7, T21)) → pI_out_aagaa(T19, T20, T10, T21, X7)
U8_gaaaaa(T8, T10, X5, X31, X6, X7, pI_out_aagaa(X5, X31, T10, X6, X7)) → pB_out_gaaaaa(T8, T10, X5, X31, X6, X7)
U1_g(T8, pB_out_gaaaaa(T8, X32, X5, X31, X6, X7)) → tA_out_g(s(T8))

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

TA_IN_G(s(T8)) → U1_G(T8, pB_in_gaaaaa(T8, X32, X5, X31, X6, X7))
TA_IN_G(s(T8)) → PB_IN_GAAAAA(T8, X32, X5, X31, X6, X7)
PB_IN_GAAAAA(T8, T10, X5, X31, X6, X7) → U7_GAAAAA(T8, T10, X5, X31, X6, X7, llD_in_ga(T8, T10))
PB_IN_GAAAAA(T8, T10, X5, X31, X6, X7) → LLD_IN_GA(T8, T10)
LLD_IN_GA(s(T16), .(X66, X67)) → U2_GA(T16, X66, X67, llD_in_ga(T16, X67))
LLD_IN_GA(s(T16), .(X66, X67)) → LLD_IN_GA(T16, X67)
U7_GAAAAA(T8, T10, X5, X31, X6, X7, llD_out_ga(T8, T10)) → U8_GAAAAA(T8, T10, X5, X31, X6, X7, pI_in_aagaa(X5, X31, T10, X6, X7))
U7_GAAAAA(T8, T10, X5, X31, X6, X7, llD_out_ga(T8, T10)) → PI_IN_AAGAA(X5, X31, T10, X6, X7)
PI_IN_AAGAA(T19, T20, T10, T21, X7) → U9_AAGAA(T19, T20, T10, T21, X7, selectH_in_aaga(T19, T20, T10, T21))
PI_IN_AAGAA(T19, T20, T10, T21, X7) → SELECTH_IN_AAGA(T19, T20, T10, T21)
SELECTH_IN_AAGA(X131, X132, T34, .(X132, X133)) → U6_AAGA(X131, X132, T34, X133, selectE_in_aga(X131, T34, X133))
SELECTH_IN_AAGA(X131, X132, T34, .(X132, X133)) → SELECTE_IN_AGA(X131, T34, X133)
SELECTE_IN_AGA(X168, .(T45, T47), .(T45, X169)) → U3_AGA(X168, T45, T47, X169, selectE_in_aga(X168, T47, X169))
SELECTE_IN_AGA(X168, .(T45, T47), .(T45, X169)) → SELECTE_IN_AGA(X168, T47, X169)
U9_AAGAA(T19, T20, T10, T21, X7, selectH_out_aaga(T19, T20, T10, T21)) → U10_AAGAA(T19, T20, T10, T21, X7, pJ_in_ag(X7, T21))
U9_AAGAA(T19, T20, T10, T21, X7, selectH_out_aaga(T19, T20, T10, T21)) → PJ_IN_AG(X7, T21)
PJ_IN_AG(T61, T21) → U11_AG(T61, T21, llF_in_ag(T61, T21))
PJ_IN_AG(T61, T21) → LLF_IN_AG(T61, T21)
LLF_IN_AG(s(X221), .(T72, T74)) → U4_AG(X221, T72, T74, llF_in_ag(X221, T74))
LLF_IN_AG(s(X221), .(T72, T74)) → LLF_IN_AG(X221, T74)
U11_AG(T61, T21, llF_out_ag(T61, T21)) → U12_AG(T61, T21, tA_in_g(T61))
U11_AG(T61, T21, llF_out_ag(T61, T21)) → TA_IN_G(T61)

The TRS R consists of the following rules:

tA_in_g(s(T8)) → U1_g(T8, pB_in_gaaaaa(T8, X32, X5, X31, X6, X7))
pB_in_gaaaaa(T8, T10, X5, X31, X6, X7) → U7_gaaaaa(T8, T10, X5, X31, X6, X7, llD_in_ga(T8, T10))
llD_in_ga(s(T16), .(X66, X67)) → U2_ga(T16, X66, X67, llD_in_ga(T16, X67))
llD_in_ga(0, []) → llD_out_ga(0, [])
U2_ga(T16, X66, X67, llD_out_ga(T16, X67)) → llD_out_ga(s(T16), .(X66, X67))
U7_gaaaaa(T8, T10, X5, X31, X6, X7, llD_out_ga(T8, T10)) → U8_gaaaaa(T8, T10, X5, X31, X6, X7, pI_in_aagaa(X5, X31, T10, X6, X7))
pI_in_aagaa(T19, T20, T10, T21, X7) → U9_aagaa(T19, T20, T10, T21, X7, selectH_in_aaga(T19, T20, T10, T21))
selectH_in_aaga(X131, X132, T34, .(X132, X133)) → U6_aaga(X131, X132, T34, X133, selectE_in_aga(X131, T34, X133))
selectE_in_aga(X168, .(T45, T47), .(T45, X169)) → U3_aga(X168, T45, T47, X169, selectE_in_aga(X168, T47, X169))
selectE_in_aga(T54, .(T54, T55), T55) → selectE_out_aga(T54, .(T54, T55), T55)
U3_aga(X168, T45, T47, X169, selectE_out_aga(X168, T47, X169)) → selectE_out_aga(X168, .(T45, T47), .(T45, X169))
U6_aaga(X131, X132, T34, X133, selectE_out_aga(X131, T34, X133)) → selectH_out_aaga(X131, X132, T34, .(X132, X133))
selectH_in_aaga(X193, X193, T58, T58) → selectH_out_aaga(X193, X193, T58, T58)
U9_aagaa(T19, T20, T10, T21, X7, selectH_out_aaga(T19, T20, T10, T21)) → U10_aagaa(T19, T20, T10, T21, X7, pJ_in_ag(X7, T21))
pJ_in_ag(T61, T21) → U11_ag(T61, T21, llF_in_ag(T61, T21))
llF_in_ag(s(X221), .(T72, T74)) → U4_ag(X221, T72, T74, llF_in_ag(X221, T74))
llF_in_ag(0, []) → llF_out_ag(0, [])
U4_ag(X221, T72, T74, llF_out_ag(X221, T74)) → llF_out_ag(s(X221), .(T72, T74))
U11_ag(T61, T21, llF_out_ag(T61, T21)) → U12_ag(T61, T21, tA_in_g(T61))
tA_in_g(0) → tA_out_g(0)
U12_ag(T61, T21, tA_out_g(T61)) → pJ_out_ag(T61, T21)
U10_aagaa(T19, T20, T10, T21, X7, pJ_out_ag(X7, T21)) → pI_out_aagaa(T19, T20, T10, T21, X7)
U8_gaaaaa(T8, T10, X5, X31, X6, X7, pI_out_aagaa(X5, X31, T10, X6, X7)) → pB_out_gaaaaa(T8, T10, X5, X31, X6, X7)
U1_g(T8, pB_out_gaaaaa(T8, X32, X5, X31, X6, X7)) → tA_out_g(s(T8))

The argument filtering Pi contains the following mapping:
tA_in_g(x1) = tA_in_g(x1)
s(x1) = s(x1)
U1_g(x1, x2) = U1_g(x1, x2)
pB_in_gaaaaa(x1, x2, x3, x4, x5, x6) = pB_in_gaaaaa(x1)
U7_gaaaaa(x1, x2, x3, x4, x5, x6, x7) = U7_gaaaaa(x1, x7)
llD_in_ga(x1, x2) = llD_in_ga(x1)
U2_ga(x1, x2, x3, x4) = U2_ga(x1, x4)
0 = 0
llD_out_ga(x1, x2) = llD_out_ga(x1, x2)
.(x1, x2) = .(x2)
U8_gaaaaa(x1, x2, x3, x4, x5, x6, x7) = U8_gaaaaa(x1, x2, x7)
pI_in_aagaa(x1, x2, x3, x4, x5) = pI_in_aagaa(x3)
U9_aagaa(x1, x2, x3, x4, x5, x6) = U9_aagaa(x3, x6)
selectH_in_aaga(x1, x2, x3, x4) = selectH_in_aaga(x3)
U6_aaga(x1, x2, x3, x4, x5) = U6_aaga(x3, x5)
selectE_in_aga(x1, x2, x3) = selectE_in_aga(x2)
U3_aga(x1, x2, x3, x4, x5) = U3_aga(x3, x5)
selectE_out_aga(x1, x2, x3) = selectE_out_aga(x2, x3)
selectH_out_aaga(x1, x2, x3, x4) = selectH_out_aaga(x3, x4)
U10_aagaa(x1, x2, x3, x4, x5, x6) = U10_aagaa(x3, x4, x6)
pJ_in_ag(x1, x2) = pJ_in_ag(x2)
U11_ag(x1, x2, x3) = U11_ag(x2, x3)
llF_in_ag(x1, x2) = llF_in_ag(x2)
U4_ag(x1, x2, x3, x4) = U4_ag(x3, x4)
[] = []
llF_out_ag(x1, x2) = llF_out_ag(x1, x2)
U12_ag(x1, x2, x3) = U12_ag(x1, x2, x3)
tA_out_g(x1) = tA_out_g(x1)
pJ_out_ag(x1, x2) = pJ_out_ag(x1, x2)
pI_out_aagaa(x1, x2, x3, x4, x5) = pI_out_aagaa(x3, x4, x5)
pB_out_gaaaaa(x1, x2, x3, x4, x5, x6) = pB_out_gaaaaa(x1, x2, x5, x6)
TA_IN_G(x1) = TA_IN_G(x1)
U1_G(x1, x2) = U1_G(x1, x2)
PB_IN_GAAAAA(x1, x2, x3, x4, x5, x6) = PB_IN_GAAAAA(x1)
U7_GAAAAA(x1, x2, x3, x4, x5, x6, x7) = U7_GAAAAA(x1, x7)
LLD_IN_GA(x1, x2) = LLD_IN_GA(x1)
U2_GA(x1, x2, x3, x4) = U2_GA(x1, x4)
U8_GAAAAA(x1, x2, x3, x4, x5, x6, x7) = U8_GAAAAA(x1, x2, x7)
PI_IN_AAGAA(x1, x2, x3, x4, x5) = PI_IN_AAGAA(x3)
U9_AAGAA(x1, x2, x3, x4, x5, x6) = U9_AAGAA(x3, x6)
SELECTH_IN_AAGA(x1, x2, x3, x4) = SELECTH_IN_AAGA(x3)
U6_AAGA(x1, x2, x3, x4, x5) = U6_AAGA(x3, x5)
SELECTE_IN_AGA(x1, x2, x3) = SELECTE_IN_AGA(x2)
U3_AGA(x1, x2, x3, x4, x5) = U3_AGA(x3, x5)
U10_AAGAA(x1, x2, x3, x4, x5, x6) = U10_AAGAA(x3, x4, x6)
PJ_IN_AG(x1, x2) = PJ_IN_AG(x2)
U11_AG(x1, x2, x3) = U11_AG(x2, x3)
LLF_IN_AG(x1, x2) = LLF_IN_AG(x2)
U4_AG(x1, x2, x3, x4) = U4_AG(x3, x4)
U12_AG(x1, x2, x3) = U12_AG(x1, x2, x3)

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

(4) Obligation:

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

TA_IN_G(s(T8)) → U1_G(T8, pB_in_gaaaaa(T8, X32, X5, X31, X6, X7))
TA_IN_G(s(T8)) → PB_IN_GAAAAA(T8, X32, X5, X31, X6, X7)
PB_IN_GAAAAA(T8, T10, X5, X31, X6, X7) → U7_GAAAAA(T8, T10, X5, X31, X6, X7, llD_in_ga(T8, T10))
PB_IN_GAAAAA(T8, T10, X5, X31, X6, X7) → LLD_IN_GA(T8, T10)
LLD_IN_GA(s(T16), .(X66, X67)) → U2_GA(T16, X66, X67, llD_in_ga(T16, X67))
LLD_IN_GA(s(T16), .(X66, X67)) → LLD_IN_GA(T16, X67)
U7_GAAAAA(T8, T10, X5, X31, X6, X7, llD_out_ga(T8, T10)) → U8_GAAAAA(T8, T10, X5, X31, X6, X7, pI_in_aagaa(X5, X31, T10, X6, X7))
U7_GAAAAA(T8, T10, X5, X31, X6, X7, llD_out_ga(T8, T10)) → PI_IN_AAGAA(X5, X31, T10, X6, X7)
PI_IN_AAGAA(T19, T20, T10, T21, X7) → U9_AAGAA(T19, T20, T10, T21, X7, selectH_in_aaga(T19, T20, T10, T21))
PI_IN_AAGAA(T19, T20, T10, T21, X7) → SELECTH_IN_AAGA(T19, T20, T10, T21)
SELECTH_IN_AAGA(X131, X132, T34, .(X132, X133)) → U6_AAGA(X131, X132, T34, X133, selectE_in_aga(X131, T34, X133))
SELECTH_IN_AAGA(X131, X132, T34, .(X132, X133)) → SELECTE_IN_AGA(X131, T34, X133)
SELECTE_IN_AGA(X168, .(T45, T47), .(T45, X169)) → U3_AGA(X168, T45, T47, X169, selectE_in_aga(X168, T47, X169))
SELECTE_IN_AGA(X168, .(T45, T47), .(T45, X169)) → SELECTE_IN_AGA(X168, T47, X169)
U9_AAGAA(T19, T20, T10, T21, X7, selectH_out_aaga(T19, T20, T10, T21)) → U10_AAGAA(T19, T20, T10, T21, X7, pJ_in_ag(X7, T21))
U9_AAGAA(T19, T20, T10, T21, X7, selectH_out_aaga(T19, T20, T10, T21)) → PJ_IN_AG(X7, T21)
PJ_IN_AG(T61, T21) → U11_AG(T61, T21, llF_in_ag(T61, T21))
PJ_IN_AG(T61, T21) → LLF_IN_AG(T61, T21)
LLF_IN_AG(s(X221), .(T72, T74)) → U4_AG(X221, T72, T74, llF_in_ag(X221, T74))
LLF_IN_AG(s(X221), .(T72, T74)) → LLF_IN_AG(X221, T74)
U11_AG(T61, T21, llF_out_ag(T61, T21)) → U12_AG(T61, T21, tA_in_g(T61))
U11_AG(T61, T21, llF_out_ag(T61, T21)) → TA_IN_G(T61)

The TRS R consists of the following rules:

tA_in_g(s(T8)) → U1_g(T8, pB_in_gaaaaa(T8, X32, X5, X31, X6, X7))
pB_in_gaaaaa(T8, T10, X5, X31, X6, X7) → U7_gaaaaa(T8, T10, X5, X31, X6, X7, llD_in_ga(T8, T10))
llD_in_ga(s(T16), .(X66, X67)) → U2_ga(T16, X66, X67, llD_in_ga(T16, X67))
llD_in_ga(0, []) → llD_out_ga(0, [])
U2_ga(T16, X66, X67, llD_out_ga(T16, X67)) → llD_out_ga(s(T16), .(X66, X67))
U7_gaaaaa(T8, T10, X5, X31, X6, X7, llD_out_ga(T8, T10)) → U8_gaaaaa(T8, T10, X5, X31, X6, X7, pI_in_aagaa(X5, X31, T10, X6, X7))
pI_in_aagaa(T19, T20, T10, T21, X7) → U9_aagaa(T19, T20, T10, T21, X7, selectH_in_aaga(T19, T20, T10, T21))
selectH_in_aaga(X131, X132, T34, .(X132, X133)) → U6_aaga(X131, X132, T34, X133, selectE_in_aga(X131, T34, X133))
selectE_in_aga(X168, .(T45, T47), .(T45, X169)) → U3_aga(X168, T45, T47, X169, selectE_in_aga(X168, T47, X169))
selectE_in_aga(T54, .(T54, T55), T55) → selectE_out_aga(T54, .(T54, T55), T55)
U3_aga(X168, T45, T47, X169, selectE_out_aga(X168, T47, X169)) → selectE_out_aga(X168, .(T45, T47), .(T45, X169))
U6_aaga(X131, X132, T34, X133, selectE_out_aga(X131, T34, X133)) → selectH_out_aaga(X131, X132, T34, .(X132, X133))
selectH_in_aaga(X193, X193, T58, T58) → selectH_out_aaga(X193, X193, T58, T58)
U9_aagaa(T19, T20, T10, T21, X7, selectH_out_aaga(T19, T20, T10, T21)) → U10_aagaa(T19, T20, T10, T21, X7, pJ_in_ag(X7, T21))
pJ_in_ag(T61, T21) → U11_ag(T61, T21, llF_in_ag(T61, T21))
llF_in_ag(s(X221), .(T72, T74)) → U4_ag(X221, T72, T74, llF_in_ag(X221, T74))
llF_in_ag(0, []) → llF_out_ag(0, [])
U4_ag(X221, T72, T74, llF_out_ag(X221, T74)) → llF_out_ag(s(X221), .(T72, T74))
U11_ag(T61, T21, llF_out_ag(T61, T21)) → U12_ag(T61, T21, tA_in_g(T61))
tA_in_g(0) → tA_out_g(0)
U12_ag(T61, T21, tA_out_g(T61)) → pJ_out_ag(T61, T21)
U10_aagaa(T19, T20, T10, T21, X7, pJ_out_ag(X7, T21)) → pI_out_aagaa(T19, T20, T10, T21, X7)
U8_gaaaaa(T8, T10, X5, X31, X6, X7, pI_out_aagaa(X5, X31, T10, X6, X7)) → pB_out_gaaaaa(T8, T10, X5, X31, X6, X7)
U1_g(T8, pB_out_gaaaaa(T8, X32, X5, X31, X6, X7)) → tA_out_g(s(T8))

(5) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 4 SCCs with 12 less nodes.

(6) Complex Obligation (AND)

(7) Obligation:

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

LLF_IN_AG(s(X221), .(T72, T74)) → LLF_IN_AG(X221, T74)

The TRS R consists of the following rules:

tA_in_g(s(T8)) → U1_g(T8, pB_in_gaaaaa(T8, X32, X5, X31, X6, X7))
pB_in_gaaaaa(T8, T10, X5, X31, X6, X7) → U7_gaaaaa(T8, T10, X5, X31, X6, X7, llD_in_ga(T8, T10))
llD_in_ga(s(T16), .(X66, X67)) → U2_ga(T16, X66, X67, llD_in_ga(T16, X67))
llD_in_ga(0, []) → llD_out_ga(0, [])
U2_ga(T16, X66, X67, llD_out_ga(T16, X67)) → llD_out_ga(s(T16), .(X66, X67))
U7_gaaaaa(T8, T10, X5, X31, X6, X7, llD_out_ga(T8, T10)) → U8_gaaaaa(T8, T10, X5, X31, X6, X7, pI_in_aagaa(X5, X31, T10, X6, X7))
pI_in_aagaa(T19, T20, T10, T21, X7) → U9_aagaa(T19, T20, T10, T21, X7, selectH_in_aaga(T19, T20, T10, T21))
selectH_in_aaga(X131, X132, T34, .(X132, X133)) → U6_aaga(X131, X132, T34, X133, selectE_in_aga(X131, T34, X133))
selectE_in_aga(X168, .(T45, T47), .(T45, X169)) → U3_aga(X168, T45, T47, X169, selectE_in_aga(X168, T47, X169))
selectE_in_aga(T54, .(T54, T55), T55) → selectE_out_aga(T54, .(T54, T55), T55)
U3_aga(X168, T45, T47, X169, selectE_out_aga(X168, T47, X169)) → selectE_out_aga(X168, .(T45, T47), .(T45, X169))
U6_aaga(X131, X132, T34, X133, selectE_out_aga(X131, T34, X133)) → selectH_out_aaga(X131, X132, T34, .(X132, X133))
selectH_in_aaga(X193, X193, T58, T58) → selectH_out_aaga(X193, X193, T58, T58)
U9_aagaa(T19, T20, T10, T21, X7, selectH_out_aaga(T19, T20, T10, T21)) → U10_aagaa(T19, T20, T10, T21, X7, pJ_in_ag(X7, T21))
pJ_in_ag(T61, T21) → U11_ag(T61, T21, llF_in_ag(T61, T21))
llF_in_ag(s(X221), .(T72, T74)) → U4_ag(X221, T72, T74, llF_in_ag(X221, T74))
llF_in_ag(0, []) → llF_out_ag(0, [])
U4_ag(X221, T72, T74, llF_out_ag(X221, T74)) → llF_out_ag(s(X221), .(T72, T74))
U11_ag(T61, T21, llF_out_ag(T61, T21)) → U12_ag(T61, T21, tA_in_g(T61))
tA_in_g(0) → tA_out_g(0)
U12_ag(T61, T21, tA_out_g(T61)) → pJ_out_ag(T61, T21)
U10_aagaa(T19, T20, T10, T21, X7, pJ_out_ag(X7, T21)) → pI_out_aagaa(T19, T20, T10, T21, X7)
U8_gaaaaa(T8, T10, X5, X31, X6, X7, pI_out_aagaa(X5, X31, T10, X6, X7)) → pB_out_gaaaaa(T8, T10, X5, X31, X6, X7)
U1_g(T8, pB_out_gaaaaa(T8, X32, X5, X31, X6, X7)) → tA_out_g(s(T8))

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

LLF_IN_AG(s(X221), .(T72, T74)) → LLF_IN_AG(X221, T74)

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

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

(10) PiDPToQDPProof (SOUND transformation)

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

(11) Obligation:

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

LLF_IN_AG(.(T74)) → LLF_IN_AG(T74)

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:

LLF_IN_AG(.(T74)) → LLF_IN_AG(T74)
The graph contains the following edges 1 > 1

(13) YES

(14) Obligation:

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

SELECTE_IN_AGA(X168, .(T45, T47), .(T45, X169)) → SELECTE_IN_AGA(X168, T47, X169)

The TRS R consists of the following rules:

tA_in_g(s(T8)) → U1_g(T8, pB_in_gaaaaa(T8, X32, X5, X31, X6, X7))
pB_in_gaaaaa(T8, T10, X5, X31, X6, X7) → U7_gaaaaa(T8, T10, X5, X31, X6, X7, llD_in_ga(T8, T10))
llD_in_ga(s(T16), .(X66, X67)) → U2_ga(T16, X66, X67, llD_in_ga(T16, X67))
llD_in_ga(0, []) → llD_out_ga(0, [])
U2_ga(T16, X66, X67, llD_out_ga(T16, X67)) → llD_out_ga(s(T16), .(X66, X67))
U7_gaaaaa(T8, T10, X5, X31, X6, X7, llD_out_ga(T8, T10)) → U8_gaaaaa(T8, T10, X5, X31, X6, X7, pI_in_aagaa(X5, X31, T10, X6, X7))
pI_in_aagaa(T19, T20, T10, T21, X7) → U9_aagaa(T19, T20, T10, T21, X7, selectH_in_aaga(T19, T20, T10, T21))
selectH_in_aaga(X131, X132, T34, .(X132, X133)) → U6_aaga(X131, X132, T34, X133, selectE_in_aga(X131, T34, X133))
selectE_in_aga(X168, .(T45, T47), .(T45, X169)) → U3_aga(X168, T45, T47, X169, selectE_in_aga(X168, T47, X169))
selectE_in_aga(T54, .(T54, T55), T55) → selectE_out_aga(T54, .(T54, T55), T55)
U3_aga(X168, T45, T47, X169, selectE_out_aga(X168, T47, X169)) → selectE_out_aga(X168, .(T45, T47), .(T45, X169))
U6_aaga(X131, X132, T34, X133, selectE_out_aga(X131, T34, X133)) → selectH_out_aaga(X131, X132, T34, .(X132, X133))
selectH_in_aaga(X193, X193, T58, T58) → selectH_out_aaga(X193, X193, T58, T58)
U9_aagaa(T19, T20, T10, T21, X7, selectH_out_aaga(T19, T20, T10, T21)) → U10_aagaa(T19, T20, T10, T21, X7, pJ_in_ag(X7, T21))
pJ_in_ag(T61, T21) → U11_ag(T61, T21, llF_in_ag(T61, T21))
llF_in_ag(s(X221), .(T72, T74)) → U4_ag(X221, T72, T74, llF_in_ag(X221, T74))
llF_in_ag(0, []) → llF_out_ag(0, [])
U4_ag(X221, T72, T74, llF_out_ag(X221, T74)) → llF_out_ag(s(X221), .(T72, T74))
U11_ag(T61, T21, llF_out_ag(T61, T21)) → U12_ag(T61, T21, tA_in_g(T61))
tA_in_g(0) → tA_out_g(0)
U12_ag(T61, T21, tA_out_g(T61)) → pJ_out_ag(T61, T21)
U10_aagaa(T19, T20, T10, T21, X7, pJ_out_ag(X7, T21)) → pI_out_aagaa(T19, T20, T10, T21, X7)
U8_gaaaaa(T8, T10, X5, X31, X6, X7, pI_out_aagaa(X5, X31, T10, X6, X7)) → pB_out_gaaaaa(T8, T10, X5, X31, X6, X7)
U1_g(T8, pB_out_gaaaaa(T8, X32, X5, X31, X6, X7)) → tA_out_g(s(T8))

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

SELECTE_IN_AGA(X168, .(T45, T47), .(T45, X169)) → SELECTE_IN_AGA(X168, T47, X169)

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

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

(17) PiDPToQDPProof (SOUND transformation)

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

(18) Obligation:

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

SELECTE_IN_AGA(.(T47)) → SELECTE_IN_AGA(T47)

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:

SELECTE_IN_AGA(.(T47)) → SELECTE_IN_AGA(T47)
The graph contains the following edges 1 > 1

(20) YES

(21) Obligation:

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

LLD_IN_GA(s(T16), .(X66, X67)) → LLD_IN_GA(T16, X67)

The TRS R consists of the following rules:

tA_in_g(s(T8)) → U1_g(T8, pB_in_gaaaaa(T8, X32, X5, X31, X6, X7))
pB_in_gaaaaa(T8, T10, X5, X31, X6, X7) → U7_gaaaaa(T8, T10, X5, X31, X6, X7, llD_in_ga(T8, T10))
llD_in_ga(s(T16), .(X66, X67)) → U2_ga(T16, X66, X67, llD_in_ga(T16, X67))
llD_in_ga(0, []) → llD_out_ga(0, [])
U2_ga(T16, X66, X67, llD_out_ga(T16, X67)) → llD_out_ga(s(T16), .(X66, X67))
U7_gaaaaa(T8, T10, X5, X31, X6, X7, llD_out_ga(T8, T10)) → U8_gaaaaa(T8, T10, X5, X31, X6, X7, pI_in_aagaa(X5, X31, T10, X6, X7))
pI_in_aagaa(T19, T20, T10, T21, X7) → U9_aagaa(T19, T20, T10, T21, X7, selectH_in_aaga(T19, T20, T10, T21))
selectH_in_aaga(X131, X132, T34, .(X132, X133)) → U6_aaga(X131, X132, T34, X133, selectE_in_aga(X131, T34, X133))
selectE_in_aga(X168, .(T45, T47), .(T45, X169)) → U3_aga(X168, T45, T47, X169, selectE_in_aga(X168, T47, X169))
selectE_in_aga(T54, .(T54, T55), T55) → selectE_out_aga(T54, .(T54, T55), T55)
U3_aga(X168, T45, T47, X169, selectE_out_aga(X168, T47, X169)) → selectE_out_aga(X168, .(T45, T47), .(T45, X169))
U6_aaga(X131, X132, T34, X133, selectE_out_aga(X131, T34, X133)) → selectH_out_aaga(X131, X132, T34, .(X132, X133))
selectH_in_aaga(X193, X193, T58, T58) → selectH_out_aaga(X193, X193, T58, T58)
U9_aagaa(T19, T20, T10, T21, X7, selectH_out_aaga(T19, T20, T10, T21)) → U10_aagaa(T19, T20, T10, T21, X7, pJ_in_ag(X7, T21))
pJ_in_ag(T61, T21) → U11_ag(T61, T21, llF_in_ag(T61, T21))
llF_in_ag(s(X221), .(T72, T74)) → U4_ag(X221, T72, T74, llF_in_ag(X221, T74))
llF_in_ag(0, []) → llF_out_ag(0, [])
U4_ag(X221, T72, T74, llF_out_ag(X221, T74)) → llF_out_ag(s(X221), .(T72, T74))
U11_ag(T61, T21, llF_out_ag(T61, T21)) → U12_ag(T61, T21, tA_in_g(T61))
tA_in_g(0) → tA_out_g(0)
U12_ag(T61, T21, tA_out_g(T61)) → pJ_out_ag(T61, T21)
U10_aagaa(T19, T20, T10, T21, X7, pJ_out_ag(X7, T21)) → pI_out_aagaa(T19, T20, T10, T21, X7)
U8_gaaaaa(T8, T10, X5, X31, X6, X7, pI_out_aagaa(X5, X31, T10, X6, X7)) → pB_out_gaaaaa(T8, T10, X5, X31, X6, X7)
U1_g(T8, pB_out_gaaaaa(T8, X32, X5, X31, X6, X7)) → tA_out_g(s(T8))

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

LLD_IN_GA(s(T16), .(X66, X67)) → LLD_IN_GA(T16, X67)

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

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

(24) PiDPToQDPProof (SOUND transformation)

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

(25) Obligation:

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

LLD_IN_GA(s(T16)) → LLD_IN_GA(T16)

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

(26) QDPSizeChangeProof (EQUIVALENT transformation)

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

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

LLD_IN_GA(s(T16)) → LLD_IN_GA(T16)
The graph contains the following edges 1 > 1

(27) YES

(28) Obligation:

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

TA_IN_G(s(T8)) → PB_IN_GAAAAA(T8, X32, X5, X31, X6, X7)
PB_IN_GAAAAA(T8, T10, X5, X31, X6, X7) → U7_GAAAAA(T8, T10, X5, X31, X6, X7, llD_in_ga(T8, T10))
U7_GAAAAA(T8, T10, X5, X31, X6, X7, llD_out_ga(T8, T10)) → PI_IN_AAGAA(X5, X31, T10, X6, X7)
PI_IN_AAGAA(T19, T20, T10, T21, X7) → U9_AAGAA(T19, T20, T10, T21, X7, selectH_in_aaga(T19, T20, T10, T21))
U9_AAGAA(T19, T20, T10, T21, X7, selectH_out_aaga(T19, T20, T10, T21)) → PJ_IN_AG(X7, T21)
PJ_IN_AG(T61, T21) → U11_AG(T61, T21, llF_in_ag(T61, T21))
U11_AG(T61, T21, llF_out_ag(T61, T21)) → TA_IN_G(T61)

The TRS R consists of the following rules:

tA_in_g(s(T8)) → U1_g(T8, pB_in_gaaaaa(T8, X32, X5, X31, X6, X7))
pB_in_gaaaaa(T8, T10, X5, X31, X6, X7) → U7_gaaaaa(T8, T10, X5, X31, X6, X7, llD_in_ga(T8, T10))
llD_in_ga(s(T16), .(X66, X67)) → U2_ga(T16, X66, X67, llD_in_ga(T16, X67))
llD_in_ga(0, []) → llD_out_ga(0, [])
U2_ga(T16, X66, X67, llD_out_ga(T16, X67)) → llD_out_ga(s(T16), .(X66, X67))
U7_gaaaaa(T8, T10, X5, X31, X6, X7, llD_out_ga(T8, T10)) → U8_gaaaaa(T8, T10, X5, X31, X6, X7, pI_in_aagaa(X5, X31, T10, X6, X7))
pI_in_aagaa(T19, T20, T10, T21, X7) → U9_aagaa(T19, T20, T10, T21, X7, selectH_in_aaga(T19, T20, T10, T21))
selectH_in_aaga(X131, X132, T34, .(X132, X133)) → U6_aaga(X131, X132, T34, X133, selectE_in_aga(X131, T34, X133))
selectE_in_aga(X168, .(T45, T47), .(T45, X169)) → U3_aga(X168, T45, T47, X169, selectE_in_aga(X168, T47, X169))
selectE_in_aga(T54, .(T54, T55), T55) → selectE_out_aga(T54, .(T54, T55), T55)
U3_aga(X168, T45, T47, X169, selectE_out_aga(X168, T47, X169)) → selectE_out_aga(X168, .(T45, T47), .(T45, X169))
U6_aaga(X131, X132, T34, X133, selectE_out_aga(X131, T34, X133)) → selectH_out_aaga(X131, X132, T34, .(X132, X133))
selectH_in_aaga(X193, X193, T58, T58) → selectH_out_aaga(X193, X193, T58, T58)
U9_aagaa(T19, T20, T10, T21, X7, selectH_out_aaga(T19, T20, T10, T21)) → U10_aagaa(T19, T20, T10, T21, X7, pJ_in_ag(X7, T21))
pJ_in_ag(T61, T21) → U11_ag(T61, T21, llF_in_ag(T61, T21))
llF_in_ag(s(X221), .(T72, T74)) → U4_ag(X221, T72, T74, llF_in_ag(X221, T74))
llF_in_ag(0, []) → llF_out_ag(0, [])
U4_ag(X221, T72, T74, llF_out_ag(X221, T74)) → llF_out_ag(s(X221), .(T72, T74))
U11_ag(T61, T21, llF_out_ag(T61, T21)) → U12_ag(T61, T21, tA_in_g(T61))
tA_in_g(0) → tA_out_g(0)
U12_ag(T61, T21, tA_out_g(T61)) → pJ_out_ag(T61, T21)
U10_aagaa(T19, T20, T10, T21, X7, pJ_out_ag(X7, T21)) → pI_out_aagaa(T19, T20, T10, T21, X7)
U8_gaaaaa(T8, T10, X5, X31, X6, X7, pI_out_aagaa(X5, X31, T10, X6, X7)) → pB_out_gaaaaa(T8, T10, X5, X31, X6, X7)
U1_g(T8, pB_out_gaaaaa(T8, X32, X5, X31, X6, X7)) → tA_out_g(s(T8))

The argument filtering Pi contains the following mapping:
tA_in_g(x1) = tA_in_g(x1)
s(x1) = s(x1)
U1_g(x1, x2) = U1_g(x1, x2)
pB_in_gaaaaa(x1, x2, x3, x4, x5, x6) = pB_in_gaaaaa(x1)
U7_gaaaaa(x1, x2, x3, x4, x5, x6, x7) = U7_gaaaaa(x1, x7)
llD_in_ga(x1, x2) = llD_in_ga(x1)
U2_ga(x1, x2, x3, x4) = U2_ga(x1, x4)
0 = 0
llD_out_ga(x1, x2) = llD_out_ga(x1, x2)
.(x1, x2) = .(x2)
U8_gaaaaa(x1, x2, x3, x4, x5, x6, x7) = U8_gaaaaa(x1, x2, x7)
pI_in_aagaa(x1, x2, x3, x4, x5) = pI_in_aagaa(x3)
U9_aagaa(x1, x2, x3, x4, x5, x6) = U9_aagaa(x3, x6)
selectH_in_aaga(x1, x2, x3, x4) = selectH_in_aaga(x3)
U6_aaga(x1, x2, x3, x4, x5) = U6_aaga(x3, x5)
selectE_in_aga(x1, x2, x3) = selectE_in_aga(x2)
U3_aga(x1, x2, x3, x4, x5) = U3_aga(x3, x5)
selectE_out_aga(x1, x2, x3) = selectE_out_aga(x2, x3)
selectH_out_aaga(x1, x2, x3, x4) = selectH_out_aaga(x3, x4)
U10_aagaa(x1, x2, x3, x4, x5, x6) = U10_aagaa(x3, x4, x6)
pJ_in_ag(x1, x2) = pJ_in_ag(x2)
U11_ag(x1, x2, x3) = U11_ag(x2, x3)
llF_in_ag(x1, x2) = llF_in_ag(x2)
U4_ag(x1, x2, x3, x4) = U4_ag(x3, x4)
[] = []
llF_out_ag(x1, x2) = llF_out_ag(x1, x2)
U12_ag(x1, x2, x3) = U12_ag(x1, x2, x3)
tA_out_g(x1) = tA_out_g(x1)
pJ_out_ag(x1, x2) = pJ_out_ag(x1, x2)
pI_out_aagaa(x1, x2, x3, x4, x5) = pI_out_aagaa(x3, x4, x5)
pB_out_gaaaaa(x1, x2, x3, x4, x5, x6) = pB_out_gaaaaa(x1, x2, x5, x6)
TA_IN_G(x1) = TA_IN_G(x1)
PB_IN_GAAAAA(x1, x2, x3, x4, x5, x6) = PB_IN_GAAAAA(x1)
U7_GAAAAA(x1, x2, x3, x4, x5, x6, x7) = U7_GAAAAA(x1, x7)
PI_IN_AAGAA(x1, x2, x3, x4, x5) = PI_IN_AAGAA(x3)
U9_AAGAA(x1, x2, x3, x4, x5, x6) = U9_AAGAA(x3, x6)
PJ_IN_AG(x1, x2) = PJ_IN_AG(x2)
U11_AG(x1, x2, x3) = U11_AG(x2, x3)

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

(29) UsableRulesProof (EQUIVALENT transformation)

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

(30) Obligation:

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

TA_IN_G(s(T8)) → PB_IN_GAAAAA(T8, X32, X5, X31, X6, X7)
PB_IN_GAAAAA(T8, T10, X5, X31, X6, X7) → U7_GAAAAA(T8, T10, X5, X31, X6, X7, llD_in_ga(T8, T10))
U7_GAAAAA(T8, T10, X5, X31, X6, X7, llD_out_ga(T8, T10)) → PI_IN_AAGAA(X5, X31, T10, X6, X7)
PI_IN_AAGAA(T19, T20, T10, T21, X7) → U9_AAGAA(T19, T20, T10, T21, X7, selectH_in_aaga(T19, T20, T10, T21))
U9_AAGAA(T19, T20, T10, T21, X7, selectH_out_aaga(T19, T20, T10, T21)) → PJ_IN_AG(X7, T21)
PJ_IN_AG(T61, T21) → U11_AG(T61, T21, llF_in_ag(T61, T21))
U11_AG(T61, T21, llF_out_ag(T61, T21)) → TA_IN_G(T61)

The TRS R consists of the following rules:

llD_in_ga(s(T16), .(X66, X67)) → U2_ga(T16, X66, X67, llD_in_ga(T16, X67))
llD_in_ga(0, []) → llD_out_ga(0, [])
selectH_in_aaga(X131, X132, T34, .(X132, X133)) → U6_aaga(X131, X132, T34, X133, selectE_in_aga(X131, T34, X133))
selectH_in_aaga(X193, X193, T58, T58) → selectH_out_aaga(X193, X193, T58, T58)
llF_in_ag(s(X221), .(T72, T74)) → U4_ag(X221, T72, T74, llF_in_ag(X221, T74))
llF_in_ag(0, []) → llF_out_ag(0, [])
U2_ga(T16, X66, X67, llD_out_ga(T16, X67)) → llD_out_ga(s(T16), .(X66, X67))
U6_aaga(X131, X132, T34, X133, selectE_out_aga(X131, T34, X133)) → selectH_out_aaga(X131, X132, T34, .(X132, X133))
U4_ag(X221, T72, T74, llF_out_ag(X221, T74)) → llF_out_ag(s(X221), .(T72, T74))
selectE_in_aga(X168, .(T45, T47), .(T45, X169)) → U3_aga(X168, T45, T47, X169, selectE_in_aga(X168, T47, X169))
selectE_in_aga(T54, .(T54, T55), T55) → selectE_out_aga(T54, .(T54, T55), T55)
U3_aga(X168, T45, T47, X169, selectE_out_aga(X168, T47, X169)) → selectE_out_aga(X168, .(T45, T47), .(T45, X169))

The argument filtering Pi contains the following mapping:
s(x1) = s(x1)
llD_in_ga(x1, x2) = llD_in_ga(x1)
U2_ga(x1, x2, x3, x4) = U2_ga(x1, x4)
0 = 0
llD_out_ga(x1, x2) = llD_out_ga(x1, x2)
.(x1, x2) = .(x2)
selectH_in_aaga(x1, x2, x3, x4) = selectH_in_aaga(x3)
U6_aaga(x1, x2, x3, x4, x5) = U6_aaga(x3, x5)
selectE_in_aga(x1, x2, x3) = selectE_in_aga(x2)
U3_aga(x1, x2, x3, x4, x5) = U3_aga(x3, x5)
selectE_out_aga(x1, x2, x3) = selectE_out_aga(x2, x3)
selectH_out_aaga(x1, x2, x3, x4) = selectH_out_aaga(x3, x4)
llF_in_ag(x1, x2) = llF_in_ag(x2)
U4_ag(x1, x2, x3, x4) = U4_ag(x3, x4)
[] = []
llF_out_ag(x1, x2) = llF_out_ag(x1, x2)
TA_IN_G(x1) = TA_IN_G(x1)
PB_IN_GAAAAA(x1, x2, x3, x4, x5, x6) = PB_IN_GAAAAA(x1)
U7_GAAAAA(x1, x2, x3, x4, x5, x6, x7) = U7_GAAAAA(x1, x7)
PI_IN_AAGAA(x1, x2, x3, x4, x5) = PI_IN_AAGAA(x3)
U9_AAGAA(x1, x2, x3, x4, x5, x6) = U9_AAGAA(x3, x6)
PJ_IN_AG(x1, x2) = PJ_IN_AG(x2)
U11_AG(x1, x2, x3) = U11_AG(x2, x3)

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

(31) PiDPToQDPProof (SOUND transformation)

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

(32) Obligation:

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

TA_IN_G(s(T8)) → PB_IN_GAAAAA(T8)
PB_IN_GAAAAA(T8) → U7_GAAAAA(T8, llD_in_ga(T8))
U7_GAAAAA(T8, llD_out_ga(T8, T10)) → PI_IN_AAGAA(T10)
PI_IN_AAGAA(T10) → U9_AAGAA(T10, selectH_in_aaga(T10))
U9_AAGAA(T10, selectH_out_aaga(T10, T21)) → PJ_IN_AG(T21)
PJ_IN_AG(T21) → U11_AG(T21, llF_in_ag(T21))
U11_AG(T21, llF_out_ag(T61, T21)) → TA_IN_G(T61)

The TRS R consists of the following rules:

llD_in_ga(s(T16)) → U2_ga(T16, llD_in_ga(T16))
llD_in_ga(0) → llD_out_ga(0, [])
selectH_in_aaga(T34) → U6_aaga(T34, selectE_in_aga(T34))
selectH_in_aaga(T58) → selectH_out_aaga(T58, T58)
llF_in_ag(.(T74)) → U4_ag(T74, llF_in_ag(T74))
llF_in_ag([]) → llF_out_ag(0, [])
U2_ga(T16, llD_out_ga(T16, X67)) → llD_out_ga(s(T16), .(X67))
U6_aaga(T34, selectE_out_aga(T34, X133)) → selectH_out_aaga(T34, .(X133))
U4_ag(T74, llF_out_ag(X221, T74)) → llF_out_ag(s(X221), .(T74))
selectE_in_aga(.(T47)) → U3_aga(T47, selectE_in_aga(T47))
selectE_in_aga(.(T55)) → selectE_out_aga(.(T55), T55)
U3_aga(T47, selectE_out_aga(T47, X169)) → selectE_out_aga(.(T47), .(X169))

The set Q consists of the following terms:

llD_in_ga(x0)
selectH_in_aaga(x0)
llF_in_ag(x0)
U2_ga(x0, x1)
U6_aaga(x0, x1)
U4_ag(x0, x1)
selectE_in_aga(x0)
U3_aga(x0, x1)

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

(33) QDPOrderProof (EQUIVALENT transformation)

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

The following pairs can be oriented strictly and are deleted.

U9_AAGAA(T10, selectH_out_aaga(T10, T21)) → PJ_IN_AG(T21)

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

POL(.(x₁)) = 1 + x₁
POL(0) = 0
POL(PB_IN_GAAAAA(x₁)) = 1 + x₁
POL(PI_IN_AAGAA(x₁)) = 1 + x₁
POL(PJ_IN_AG(x₁)) = x₁
POL(TA_IN_G(x₁)) = x₁
POL(U11_AG(x₁, x₂)) = x₂
POL(U2_ga(x₁, x₂)) = 1 + x₂
POL(U3_aga(x₁, x₂)) = 1 + x₂
POL(U4_ag(x₁, x₂)) = 1 + x₂
POL(U6_aaga(x₁, x₂)) = x₂
POL(U7_GAAAAA(x₁, x₂)) = 1 + x₂
POL(U9_AAGAA(x₁, x₂)) = 1 + x₂
POL([]) = 0
POL(llD_in_ga(x₁)) = x₁
POL(llD_out_ga(x₁, x₂)) = x₂
POL(llF_in_ag(x₁)) = x₁
POL(llF_out_ag(x₁, x₂)) = x₁
POL(s(x₁)) = 1 + x₁
POL(selectE_in_aga(x₁)) = x₁
POL(selectE_out_aga(x₁, x₂)) = 1 + x₂
POL(selectH_in_aaga(x₁)) = x₁
POL(selectH_out_aaga(x₁, x₂)) = x₂

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

llD_in_ga(s(T16)) → U2_ga(T16, llD_in_ga(T16))
llD_in_ga(0) → llD_out_ga(0, [])
selectH_in_aaga(T34) → U6_aaga(T34, selectE_in_aga(T34))
selectH_in_aaga(T58) → selectH_out_aaga(T58, T58)
llF_in_ag(.(T74)) → U4_ag(T74, llF_in_ag(T74))
llF_in_ag([]) → llF_out_ag(0, [])
U2_ga(T16, llD_out_ga(T16, X67)) → llD_out_ga(s(T16), .(X67))
selectE_in_aga(.(T47)) → U3_aga(T47, selectE_in_aga(T47))
selectE_in_aga(.(T55)) → selectE_out_aga(.(T55), T55)
U6_aaga(T34, selectE_out_aga(T34, X133)) → selectH_out_aaga(T34, .(X133))
U4_ag(T74, llF_out_ag(X221, T74)) → llF_out_ag(s(X221), .(T74))
U3_aga(T47, selectE_out_aga(T47, X169)) → selectE_out_aga(.(T47), .(X169))

(34) Obligation:

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

TA_IN_G(s(T8)) → PB_IN_GAAAAA(T8)
PB_IN_GAAAAA(T8) → U7_GAAAAA(T8, llD_in_ga(T8))
U7_GAAAAA(T8, llD_out_ga(T8, T10)) → PI_IN_AAGAA(T10)
PI_IN_AAGAA(T10) → U9_AAGAA(T10, selectH_in_aaga(T10))
PJ_IN_AG(T21) → U11_AG(T21, llF_in_ag(T21))
U11_AG(T21, llF_out_ag(T61, T21)) → TA_IN_G(T61)

The TRS R consists of the following rules:

llD_in_ga(s(T16)) → U2_ga(T16, llD_in_ga(T16))
llD_in_ga(0) → llD_out_ga(0, [])
selectH_in_aaga(T34) → U6_aaga(T34, selectE_in_aga(T34))
selectH_in_aaga(T58) → selectH_out_aaga(T58, T58)
llF_in_ag(.(T74)) → U4_ag(T74, llF_in_ag(T74))
llF_in_ag([]) → llF_out_ag(0, [])
U2_ga(T16, llD_out_ga(T16, X67)) → llD_out_ga(s(T16), .(X67))
U6_aaga(T34, selectE_out_aga(T34, X133)) → selectH_out_aaga(T34, .(X133))
U4_ag(T74, llF_out_ag(X221, T74)) → llF_out_ag(s(X221), .(T74))
selectE_in_aga(.(T47)) → U3_aga(T47, selectE_in_aga(T47))
selectE_in_aga(.(T55)) → selectE_out_aga(.(T55), T55)
U3_aga(T47, selectE_out_aga(T47, X169)) → selectE_out_aga(.(T47), .(X169))

The set Q consists of the following terms:

llD_in_ga(x0)
selectH_in_aaga(x0)
llF_in_ag(x0)
U2_ga(x0, x1)
U6_aaga(x0, x1)
U4_ag(x0, x1)
selectE_in_aga(x0)
U3_aga(x0, x1)

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

(35) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 6 less nodes.

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

(21) Obligation:

(22) UsableRulesProof (EQUIVALENT transformation)

(23) Obligation:

(24) PiDPToQDPProof (SOUND transformation)

(25) Obligation:

(26) QDPSizeChangeProof (EQUIVALENT transformation)

(27) YES

(28) Obligation:

(29) UsableRulesProof (EQUIVALENT transformation)

(30) Obligation:

(31) PiDPToQDPProof (SOUND transformation)

(32) Obligation:

(33) QDPOrderProof (EQUIVALENT transformation)

(34) Obligation:

(35) DependencyGraphProof (EQUIVALENT transformation)

(36) TRUE