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

(0) Obligation:

Clauses:

perm1(L, M) :- ','(eq_len1(L, M), same_sets(L, M)).
eq_len1([], []).
eq_len1(.(X1, Xs), .(X2, Ys)) :- eq_len1(Xs, Ys).
member(X, .(X, X3)).
member(X, .(X4, T)) :- member(X, T).
same_sets([], X5).
same_sets(.(X, Xs), L) :- ','(member(X, L), same_sets(Xs, L)).

Query: perm1(g,g)

(1) PrologToPiTRSViaGraphTransformerProof (SOUND transformation)

Transformed Prolog program to (Pi-)TRS.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
2 [label="A: perm1(T1, T2)\n\nT1 is ground\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
6 [label="6: perm1(T1, T2), SCOPE: 1, CLAUSE: 0\n\nT1 is ground\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
8 [label="8: ','(eq_len1(T5, T6), same_sets(T5, T6))\n\nT5 is ground\nT6 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
11 [label="11: ','(eq_len1(T5, T6), same_sets(T5, T6)), SCOPE: 2, CLAUSE: 1 | ','(eq_len1(T5, T6), same_sets(T5, T6)), SCOPE: 2, CLAUSE: 2\n\nT5 is ground\nT6 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
13 [label="13: ','(eq_len1(T5, T6), same_sets(T5, T6)), SCOPE: 2, CLAUSE: 1\n\nT5 is ground\nT6 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
15 [label="15: ','(eq_len1(T5, T6), same_sets(T5, T6)), SCOPE: 2, CLAUSE: 2\n\nT5 is ground\nT6 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
16 [label="16: same_sets([], [])\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
19 [label="19: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
21 [label="21: same_sets([], []), SCOPE: 3, CLAUSE: 5 | same_sets([], []), SCOPE: 3, CLAUSE: 6\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
24 [label="24: same_sets([], []), SCOPE: 3, CLAUSE: 5\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
27 [label="27: same_sets([], []), SCOPE: 3, CLAUSE: 6\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
30 [label="30: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
31 [label="31: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
34 [label="34: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
41 [label="B: ','(eq_len1(T16, T18), same_sets(.(T15, T16), .(T17, T18)))\n\nT15 is ground\nT16 is ground\nT17 is ground\nT18 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
43 [label="43: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
48 [label="C: eq_len1(T16, T18)\n\nT16 is ground\nT18 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
49 [label="E: same_sets(.(T15, T16), .(T17, T18))\n\nT15 is ground\nT16 is ground\nT17 is ground\nT18 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
51 [label="51: eq_len1(T16, T18), SCOPE: 4, CLAUSE: 1 | eq_len1(T16, T18), SCOPE: 4, CLAUSE: 2\n\nT16 is ground\nT18 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
54 [label="54: eq_len1(T16, T18), SCOPE: 4, CLAUSE: 1\n\nT16 is ground\nT18 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
55 [label="55: eq_len1(T16, T18), SCOPE: 4, CLAUSE: 2\n\nT16 is ground\nT18 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
60 [label="60: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
61 [label="61: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
62 [label="62: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
65 [label="65: eq_len1(T28, T30)\n\nT28 is ground\nT30 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
66 [label="66: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
74 [label="74: same_sets(.(T15, T16), .(T17, T18)), SCOPE: 5, CLAUSE: 5 | same_sets(.(T15, T16), .(T17, T18)), SCOPE: 5, CLAUSE: 6\n\nT15 is ground\nT16 is ground\nT17 is ground\nT18 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
75 [label="75: same_sets(.(T15, T16), .(T17, T18)), SCOPE: 5, CLAUSE: 6\n\nT15 is ground\nT16 is ground\nT17 is ground\nT18 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
79 [label="F: ','(member(T43, .(T45, T46)), same_sets(T44, .(T45, T46)))\n\nT43 is ground\nT44 is ground\nT45 is ground\nT46 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
84 [label="G: member(T43, .(T45, T46))\n\nT43 is ground\nT45 is ground\nT46 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
85 [label="H: same_sets(T44, .(T45, T46))\n\nT44 is ground\nT45 is ground\nT46 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
87 [label="87: member(T43, .(T45, T46)), SCOPE: 6, CLAUSE: 3 | member(T43, .(T45, T46)), SCOPE: 6, CLAUSE: 4\n\nT43 is ground\nT45 is ground\nT46 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
90 [label="90: member(T43, .(T45, T46)), SCOPE: 6, CLAUSE: 3\n\nT43 is ground\nT45 is ground\nT46 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
91 [label="91: member(T43, .(T45, T46)), SCOPE: 6, CLAUSE: 4\n\nT43 is ground\nT45 is ground\nT46 is ground", 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];
97 [label="97: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
105 [label="D: member(T75, T77)\n\nT75 is ground\nT77 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
107 [label="107: member(T75, T77), SCOPE: 7, CLAUSE: 3 | member(T75, T77), SCOPE: 7, CLAUSE: 4\n\nT75 is ground\nT77 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
112 [label="112: member(T75, T77), SCOPE: 7, CLAUSE: 3\n\nT75 is ground\nT77 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
113 [label="113: member(T75, T77), SCOPE: 7, CLAUSE: 4\n\nT75 is ground\nT77 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
117 [label="117: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
118 [label="118: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
119 [label="119: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
122 [label="122: member(T98, T100)\n\nT98 is ground\nT100 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
123 [label="123: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
125 [label="125: same_sets(T44, .(T45, T46)), SCOPE: 8, CLAUSE: 5 | same_sets(T44, .(T45, T46)), SCOPE: 8, CLAUSE: 6\n\nT44 is ground\nT45 is ground\nT46 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
128 [label="128: same_sets(T44, .(T45, T46)), SCOPE: 8, CLAUSE: 5\n\nT44 is ground\nT45 is ground\nT46 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
129 [label="129: same_sets(T44, .(T45, T46)), SCOPE: 8, CLAUSE: 6\n\nT44 is ground\nT45 is ground\nT46 is ground", 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: ','(member(T127, .(T129, T130)), same_sets(T128, .(T129, T130)))\n\nT127 is ground\nT128 is ground\nT129 is ground\nT130 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
139 [label="139: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
140 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
2 -> 140 [arrowhead = none ];
140 -> 6;

141 [label="ONLY EVAL with clause\nperm1(X8, X9) :- ','(eq_len1(X8, X9), same_sets(X8, X9)).\nand substitutionT1 -> T5,\nX8 -> T5,\nT2 -> T6,\nX9 -> T6", fontsize=14, style = filled, fillcolor = lightblue];
6 -> 141 [arrowhead = none ];
141 -> 8;

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

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

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

145 [label="EVAL with clause\neq_len1([], []).\nand substitutionT5 -> [],\nT6 -> []", fontsize=14, style = filled, fillcolor = lightblue];
13 -> 145 [arrowhead = none ];
145 -> 16;

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

147 [label="EVAL with clause\neq_len1(.(X27, X28), .(X29, X30)) :- eq_len1(X28, X30).\nand substitutionX27 -> T15,\nX28 -> T16,\nT5 -> .(T15, T16),\nX29 -> T17,\nX30 -> T18,\nT6 -> .(T17, T18)", fontsize=14, style = filled, fillcolor = lightblue];
15 -> 147 [arrowhead = none ];
147 -> 41;

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

149 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
16 -> 149 [arrowhead = none ];
149 -> 21;

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

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

152 [label="ONLY EVAL with clause\nsame_sets([], X15).\nand substitutionX15 -> []", fontsize=14, style = filled, fillcolor = lightblue];
24 -> 152 [arrowhead = none ];
152 -> 30;

153 [label="BACKTRACK\nfor clause: same_sets(.(X, Xs), L) :- ','(member(X, L), same_sets(Xs, L))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
27 -> 153 [arrowhead = none ];
153 -> 34;

154 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
30 -> 154 [arrowhead = none ];
154 -> 31;

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

156 [label="SPLIT 2\nnew knowledge:\nT16 is ground\nT18 is ground", fontsize=14, style = filled, fillcolor = violet];
41 -> 156 [arrowhead = none ];
156 -> 49;

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

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

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

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

161 [label="EVAL with clause\neq_len1([], []).\nand substitutionT16 -> [],\nT18 -> []", fontsize=14, style = filled, fillcolor = lightblue];
54 -> 161 [arrowhead = none ];
161 -> 60;

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

163 [label="EVAL with clause\neq_len1(.(X39, X40), .(X41, X42)) :- eq_len1(X40, X42).\nand substitutionX39 -> T27,\nX40 -> T28,\nT16 -> .(T27, T28),\nX41 -> T29,\nX42 -> T30,\nT18 -> .(T29, T30)", fontsize=14, style = filled, fillcolor = lightblue];
55 -> 163 [arrowhead = none ];
163 -> 65;

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

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

166 [label="INSTANCE with matching:\nT16 -> T28\nT18 -> T30", fontsize=14, style = filled, fillcolor = lightgrey];
65 -> 166 [arrowhead = none , style=dashed];
166 -> 48[style=dashed];

167 [label="BACKTRACK\nfor clause: same_sets([], X5)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
74 -> 167 [arrowhead = none ];
167 -> 75;

168 [label="ONLY EVAL with clause\nsame_sets(.(X56, X57), X58) :- ','(member(X56, X58), same_sets(X57, X58)).\nand substitutionT15 -> T43,\nX56 -> T43,\nT16 -> T44,\nX57 -> T44,\nT17 -> T45,\nT18 -> T46,\nX58 -> .(T45, T46)", fontsize=14, style = filled, fillcolor = lightblue];
75 -> 168 [arrowhead = none ];
168 -> 79;

169 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
79 -> 169 [arrowhead = none ];
169 -> 84;

170 [label="SPLIT 2\nnew knowledge:\nT43 is ground\nT45 is ground\nT46 is ground", fontsize=14, style = filled, fillcolor = violet];
79 -> 170 [arrowhead = none ];
170 -> 85;

171 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
84 -> 171 [arrowhead = none ];
171 -> 87;

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

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

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

175 [label="EVAL with clause\nmember(X75, .(X75, X76)).\nand substitutionT43 -> T63,\nX75 -> T63,\nT45 -> T63,\nT46 -> T64,\nX76 -> T64", fontsize=14, style = filled, fillcolor = lightblue];
90 -> 175 [arrowhead = none ];
175 -> 95;

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

177 [label="ONLY EVAL with clause\nmember(X87, .(X88, X89)) :- member(X87, X89).\nand substitutionT43 -> T75,\nX87 -> T75,\nT45 -> T76,\nX88 -> T76,\nT46 -> T77,\nX89 -> T77", fontsize=14, style = filled, fillcolor = lightblue];
91 -> 177 [arrowhead = none ];
177 -> 105;

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

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

180 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
107 -> 180 [arrowhead = none ];
180 -> 112;

181 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
107 -> 181 [arrowhead = none ];
181 -> 113;

182 [label="EVAL with clause\nmember(X102, .(X102, X103)).\nand substitutionT75 -> T90,\nX102 -> T90,\nX103 -> T91,\nT77 -> .(T90, T91)", fontsize=14, style = filled, fillcolor = lightblue];
112 -> 182 [arrowhead = none ];
182 -> 117;

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

184 [label="EVAL with clause\nmember(X110, .(X111, X112)) :- member(X110, X112).\nand substitutionT75 -> T98,\nX110 -> T98,\nX111 -> T99,\nX112 -> T100,\nT77 -> .(T99, T100)", fontsize=14, style = filled, fillcolor = lightblue];
113 -> 184 [arrowhead = none ];
184 -> 122;

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

186 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
117 -> 186 [arrowhead = none ];
186 -> 119;

187 [label="INSTANCE with matching:\nT75 -> T98\nT77 -> T100", fontsize=14, style = filled, fillcolor = lightgrey];
122 -> 187 [arrowhead = none , style=dashed];
187 -> 105[style=dashed];

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

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

190 [label="EVAL with clause\nsame_sets([], X123).\nand substitutionT44 -> [],\nT45 -> T117,\nT46 -> T118,\nX123 -> .(T117, T118)", fontsize=14, style = filled, fillcolor = lightblue];
128 -> 190 [arrowhead = none ];
190 -> 133;

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

192 [label="EVAL with clause\nsame_sets(.(X130, X131), X132) :- ','(member(X130, X132), same_sets(X131, X132)).\nand substitutionX130 -> T127,\nX131 -> T128,\nT44 -> .(T127, T128),\nT45 -> T129,\nT46 -> T130,\nX132 -> .(T129, T130)", fontsize=14, style = filled, fillcolor = lightblue];
129 -> 192 [arrowhead = none ];
192 -> 138;

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

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

195 [label="INSTANCE with matching:\nT43 -> T127\nT45 -> T129\nT46 -> T130\nT44 -> T128", fontsize=14, style = filled, fillcolor = lightgrey];
138 -> 195 [arrowhead = none , style=dashed];
195 -> 79[style=dashed];

}

(2) Obligation:

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

perm1A_in_gg([], []) → perm1A_out_gg([], [])
perm1A_in_gg(.(T15, T16), .(T17, T18)) → U1_gg(T15, T16, T17, T18, pB_in_gggg(T16, T18, T15, T17))
pB_in_gggg(T16, T18, T15, T17) → U7_gggg(T16, T18, T15, T17, eq_len1C_in_gg(T16, T18))
eq_len1C_in_gg([], []) → eq_len1C_out_gg([], [])
eq_len1C_in_gg(.(T27, T28), .(T29, T30)) → U2_gg(T27, T28, T29, T30, eq_len1C_in_gg(T28, T30))
U2_gg(T27, T28, T29, T30, eq_len1C_out_gg(T28, T30)) → eq_len1C_out_gg(.(T27, T28), .(T29, T30))
U7_gggg(T16, T18, T15, T17, eq_len1C_out_gg(T16, T18)) → U8_gggg(T16, T18, T15, T17, same_setsE_in_gggg(T15, T16, T17, T18))
same_setsE_in_gggg(T43, T44, T45, T46) → U4_gggg(T43, T44, T45, T46, pF_in_gggg(T43, T45, T46, T44))
pF_in_gggg(T43, T45, T46, T44) → U9_gggg(T43, T45, T46, T44, memberG_in_ggg(T43, T45, T46))
memberG_in_ggg(T63, T63, T64) → memberG_out_ggg(T63, T63, T64)
memberG_in_ggg(T75, T76, T77) → U5_ggg(T75, T76, T77, memberD_in_gg(T75, T77))
memberD_in_gg(T90, .(T90, T91)) → memberD_out_gg(T90, .(T90, T91))
memberD_in_gg(T98, .(T99, T100)) → U3_gg(T98, T99, T100, memberD_in_gg(T98, T100))
U3_gg(T98, T99, T100, memberD_out_gg(T98, T100)) → memberD_out_gg(T98, .(T99, T100))
U5_ggg(T75, T76, T77, memberD_out_gg(T75, T77)) → memberG_out_ggg(T75, T76, T77)
U9_gggg(T43, T45, T46, T44, memberG_out_ggg(T43, T45, T46)) → U10_gggg(T43, T45, T46, T44, same_setsH_in_ggg(T44, T45, T46))
same_setsH_in_ggg([], T117, T118) → same_setsH_out_ggg([], T117, T118)
same_setsH_in_ggg(.(T127, T128), T129, T130) → U6_ggg(T127, T128, T129, T130, pF_in_gggg(T127, T129, T130, T128))
U6_ggg(T127, T128, T129, T130, pF_out_gggg(T127, T129, T130, T128)) → same_setsH_out_ggg(.(T127, T128), T129, T130)
U10_gggg(T43, T45, T46, T44, same_setsH_out_ggg(T44, T45, T46)) → pF_out_gggg(T43, T45, T46, T44)
U4_gggg(T43, T44, T45, T46, pF_out_gggg(T43, T45, T46, T44)) → same_setsE_out_gggg(T43, T44, T45, T46)
U8_gggg(T16, T18, T15, T17, same_setsE_out_gggg(T15, T16, T17, T18)) → pB_out_gggg(T16, T18, T15, T17)
U1_gg(T15, T16, T17, T18, pB_out_gggg(T16, T18, T15, T17)) → perm1A_out_gg(.(T15, T16), .(T17, T18))

Pi is empty.

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

PERM1A_IN_GG(.(T15, T16), .(T17, T18)) → U1_GG(T15, T16, T17, T18, pB_in_gggg(T16, T18, T15, T17))
PERM1A_IN_GG(.(T15, T16), .(T17, T18)) → PB_IN_GGGG(T16, T18, T15, T17)
PB_IN_GGGG(T16, T18, T15, T17) → U7_GGGG(T16, T18, T15, T17, eq_len1C_in_gg(T16, T18))
PB_IN_GGGG(T16, T18, T15, T17) → EQ_LEN1C_IN_GG(T16, T18)
EQ_LEN1C_IN_GG(.(T27, T28), .(T29, T30)) → U2_GG(T27, T28, T29, T30, eq_len1C_in_gg(T28, T30))
EQ_LEN1C_IN_GG(.(T27, T28), .(T29, T30)) → EQ_LEN1C_IN_GG(T28, T30)
U7_GGGG(T16, T18, T15, T17, eq_len1C_out_gg(T16, T18)) → U8_GGGG(T16, T18, T15, T17, same_setsE_in_gggg(T15, T16, T17, T18))
U7_GGGG(T16, T18, T15, T17, eq_len1C_out_gg(T16, T18)) → SAME_SETSE_IN_GGGG(T15, T16, T17, T18)
SAME_SETSE_IN_GGGG(T43, T44, T45, T46) → U4_GGGG(T43, T44, T45, T46, pF_in_gggg(T43, T45, T46, T44))
SAME_SETSE_IN_GGGG(T43, T44, T45, T46) → PF_IN_GGGG(T43, T45, T46, T44)
PF_IN_GGGG(T43, T45, T46, T44) → U9_GGGG(T43, T45, T46, T44, memberG_in_ggg(T43, T45, T46))
PF_IN_GGGG(T43, T45, T46, T44) → MEMBERG_IN_GGG(T43, T45, T46)
MEMBERG_IN_GGG(T75, T76, T77) → U5_GGG(T75, T76, T77, memberD_in_gg(T75, T77))
MEMBERG_IN_GGG(T75, T76, T77) → MEMBERD_IN_GG(T75, T77)
MEMBERD_IN_GG(T98, .(T99, T100)) → U3_GG(T98, T99, T100, memberD_in_gg(T98, T100))
MEMBERD_IN_GG(T98, .(T99, T100)) → MEMBERD_IN_GG(T98, T100)
U9_GGGG(T43, T45, T46, T44, memberG_out_ggg(T43, T45, T46)) → U10_GGGG(T43, T45, T46, T44, same_setsH_in_ggg(T44, T45, T46))
U9_GGGG(T43, T45, T46, T44, memberG_out_ggg(T43, T45, T46)) → SAME_SETSH_IN_GGG(T44, T45, T46)
SAME_SETSH_IN_GGG(.(T127, T128), T129, T130) → U6_GGG(T127, T128, T129, T130, pF_in_gggg(T127, T129, T130, T128))
SAME_SETSH_IN_GGG(.(T127, T128), T129, T130) → PF_IN_GGGG(T127, T129, T130, T128)

The TRS R consists of the following rules:

perm1A_in_gg([], []) → perm1A_out_gg([], [])
perm1A_in_gg(.(T15, T16), .(T17, T18)) → U1_gg(T15, T16, T17, T18, pB_in_gggg(T16, T18, T15, T17))
pB_in_gggg(T16, T18, T15, T17) → U7_gggg(T16, T18, T15, T17, eq_len1C_in_gg(T16, T18))
eq_len1C_in_gg([], []) → eq_len1C_out_gg([], [])
eq_len1C_in_gg(.(T27, T28), .(T29, T30)) → U2_gg(T27, T28, T29, T30, eq_len1C_in_gg(T28, T30))
U2_gg(T27, T28, T29, T30, eq_len1C_out_gg(T28, T30)) → eq_len1C_out_gg(.(T27, T28), .(T29, T30))
U7_gggg(T16, T18, T15, T17, eq_len1C_out_gg(T16, T18)) → U8_gggg(T16, T18, T15, T17, same_setsE_in_gggg(T15, T16, T17, T18))
same_setsE_in_gggg(T43, T44, T45, T46) → U4_gggg(T43, T44, T45, T46, pF_in_gggg(T43, T45, T46, T44))
pF_in_gggg(T43, T45, T46, T44) → U9_gggg(T43, T45, T46, T44, memberG_in_ggg(T43, T45, T46))
memberG_in_ggg(T63, T63, T64) → memberG_out_ggg(T63, T63, T64)
memberG_in_ggg(T75, T76, T77) → U5_ggg(T75, T76, T77, memberD_in_gg(T75, T77))
memberD_in_gg(T90, .(T90, T91)) → memberD_out_gg(T90, .(T90, T91))
memberD_in_gg(T98, .(T99, T100)) → U3_gg(T98, T99, T100, memberD_in_gg(T98, T100))
U3_gg(T98, T99, T100, memberD_out_gg(T98, T100)) → memberD_out_gg(T98, .(T99, T100))
U5_ggg(T75, T76, T77, memberD_out_gg(T75, T77)) → memberG_out_ggg(T75, T76, T77)
U9_gggg(T43, T45, T46, T44, memberG_out_ggg(T43, T45, T46)) → U10_gggg(T43, T45, T46, T44, same_setsH_in_ggg(T44, T45, T46))
same_setsH_in_ggg([], T117, T118) → same_setsH_out_ggg([], T117, T118)
same_setsH_in_ggg(.(T127, T128), T129, T130) → U6_ggg(T127, T128, T129, T130, pF_in_gggg(T127, T129, T130, T128))
U6_ggg(T127, T128, T129, T130, pF_out_gggg(T127, T129, T130, T128)) → same_setsH_out_ggg(.(T127, T128), T129, T130)
U10_gggg(T43, T45, T46, T44, same_setsH_out_ggg(T44, T45, T46)) → pF_out_gggg(T43, T45, T46, T44)
U4_gggg(T43, T44, T45, T46, pF_out_gggg(T43, T45, T46, T44)) → same_setsE_out_gggg(T43, T44, T45, T46)
U8_gggg(T16, T18, T15, T17, same_setsE_out_gggg(T15, T16, T17, T18)) → pB_out_gggg(T16, T18, T15, T17)
U1_gg(T15, T16, T17, T18, pB_out_gggg(T16, T18, T15, T17)) → perm1A_out_gg(.(T15, T16), .(T17, T18))

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

(4) Obligation:

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

PERM1A_IN_GG(.(T15, T16), .(T17, T18)) → U1_GG(T15, T16, T17, T18, pB_in_gggg(T16, T18, T15, T17))
PERM1A_IN_GG(.(T15, T16), .(T17, T18)) → PB_IN_GGGG(T16, T18, T15, T17)
PB_IN_GGGG(T16, T18, T15, T17) → U7_GGGG(T16, T18, T15, T17, eq_len1C_in_gg(T16, T18))
PB_IN_GGGG(T16, T18, T15, T17) → EQ_LEN1C_IN_GG(T16, T18)
EQ_LEN1C_IN_GG(.(T27, T28), .(T29, T30)) → U2_GG(T27, T28, T29, T30, eq_len1C_in_gg(T28, T30))
EQ_LEN1C_IN_GG(.(T27, T28), .(T29, T30)) → EQ_LEN1C_IN_GG(T28, T30)
U7_GGGG(T16, T18, T15, T17, eq_len1C_out_gg(T16, T18)) → U8_GGGG(T16, T18, T15, T17, same_setsE_in_gggg(T15, T16, T17, T18))
U7_GGGG(T16, T18, T15, T17, eq_len1C_out_gg(T16, T18)) → SAME_SETSE_IN_GGGG(T15, T16, T17, T18)
SAME_SETSE_IN_GGGG(T43, T44, T45, T46) → U4_GGGG(T43, T44, T45, T46, pF_in_gggg(T43, T45, T46, T44))
SAME_SETSE_IN_GGGG(T43, T44, T45, T46) → PF_IN_GGGG(T43, T45, T46, T44)
PF_IN_GGGG(T43, T45, T46, T44) → U9_GGGG(T43, T45, T46, T44, memberG_in_ggg(T43, T45, T46))
PF_IN_GGGG(T43, T45, T46, T44) → MEMBERG_IN_GGG(T43, T45, T46)
MEMBERG_IN_GGG(T75, T76, T77) → U5_GGG(T75, T76, T77, memberD_in_gg(T75, T77))
MEMBERG_IN_GGG(T75, T76, T77) → MEMBERD_IN_GG(T75, T77)
MEMBERD_IN_GG(T98, .(T99, T100)) → U3_GG(T98, T99, T100, memberD_in_gg(T98, T100))
MEMBERD_IN_GG(T98, .(T99, T100)) → MEMBERD_IN_GG(T98, T100)
U9_GGGG(T43, T45, T46, T44, memberG_out_ggg(T43, T45, T46)) → U10_GGGG(T43, T45, T46, T44, same_setsH_in_ggg(T44, T45, T46))
U9_GGGG(T43, T45, T46, T44, memberG_out_ggg(T43, T45, T46)) → SAME_SETSH_IN_GGG(T44, T45, T46)
SAME_SETSH_IN_GGG(.(T127, T128), T129, T130) → U6_GGG(T127, T128, T129, T130, pF_in_gggg(T127, T129, T130, T128))
SAME_SETSH_IN_GGG(.(T127, T128), T129, T130) → PF_IN_GGGG(T127, T129, T130, T128)

The TRS R consists of the following rules:

perm1A_in_gg([], []) → perm1A_out_gg([], [])
perm1A_in_gg(.(T15, T16), .(T17, T18)) → U1_gg(T15, T16, T17, T18, pB_in_gggg(T16, T18, T15, T17))
pB_in_gggg(T16, T18, T15, T17) → U7_gggg(T16, T18, T15, T17, eq_len1C_in_gg(T16, T18))
eq_len1C_in_gg([], []) → eq_len1C_out_gg([], [])
eq_len1C_in_gg(.(T27, T28), .(T29, T30)) → U2_gg(T27, T28, T29, T30, eq_len1C_in_gg(T28, T30))
U2_gg(T27, T28, T29, T30, eq_len1C_out_gg(T28, T30)) → eq_len1C_out_gg(.(T27, T28), .(T29, T30))
U7_gggg(T16, T18, T15, T17, eq_len1C_out_gg(T16, T18)) → U8_gggg(T16, T18, T15, T17, same_setsE_in_gggg(T15, T16, T17, T18))
same_setsE_in_gggg(T43, T44, T45, T46) → U4_gggg(T43, T44, T45, T46, pF_in_gggg(T43, T45, T46, T44))
pF_in_gggg(T43, T45, T46, T44) → U9_gggg(T43, T45, T46, T44, memberG_in_ggg(T43, T45, T46))
memberG_in_ggg(T63, T63, T64) → memberG_out_ggg(T63, T63, T64)
memberG_in_ggg(T75, T76, T77) → U5_ggg(T75, T76, T77, memberD_in_gg(T75, T77))
memberD_in_gg(T90, .(T90, T91)) → memberD_out_gg(T90, .(T90, T91))
memberD_in_gg(T98, .(T99, T100)) → U3_gg(T98, T99, T100, memberD_in_gg(T98, T100))
U3_gg(T98, T99, T100, memberD_out_gg(T98, T100)) → memberD_out_gg(T98, .(T99, T100))
U5_ggg(T75, T76, T77, memberD_out_gg(T75, T77)) → memberG_out_ggg(T75, T76, T77)
U9_gggg(T43, T45, T46, T44, memberG_out_ggg(T43, T45, T46)) → U10_gggg(T43, T45, T46, T44, same_setsH_in_ggg(T44, T45, T46))
same_setsH_in_ggg([], T117, T118) → same_setsH_out_ggg([], T117, T118)
same_setsH_in_ggg(.(T127, T128), T129, T130) → U6_ggg(T127, T128, T129, T130, pF_in_gggg(T127, T129, T130, T128))
U6_ggg(T127, T128, T129, T130, pF_out_gggg(T127, T129, T130, T128)) → same_setsH_out_ggg(.(T127, T128), T129, T130)
U10_gggg(T43, T45, T46, T44, same_setsH_out_ggg(T44, T45, T46)) → pF_out_gggg(T43, T45, T46, T44)
U4_gggg(T43, T44, T45, T46, pF_out_gggg(T43, T45, T46, T44)) → same_setsE_out_gggg(T43, T44, T45, T46)
U8_gggg(T16, T18, T15, T17, same_setsE_out_gggg(T15, T16, T17, T18)) → pB_out_gggg(T16, T18, T15, T17)
U1_gg(T15, T16, T17, T18, pB_out_gggg(T16, T18, T15, T17)) → perm1A_out_gg(.(T15, T16), .(T17, T18))

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

(5) DependencyGraphProof (EQUIVALENT transformation)

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

(6) Complex Obligation (AND)

(7) Obligation:

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

MEMBERD_IN_GG(T98, .(T99, T100)) → MEMBERD_IN_GG(T98, T100)

The TRS R consists of the following rules:

perm1A_in_gg([], []) → perm1A_out_gg([], [])
perm1A_in_gg(.(T15, T16), .(T17, T18)) → U1_gg(T15, T16, T17, T18, pB_in_gggg(T16, T18, T15, T17))
pB_in_gggg(T16, T18, T15, T17) → U7_gggg(T16, T18, T15, T17, eq_len1C_in_gg(T16, T18))
eq_len1C_in_gg([], []) → eq_len1C_out_gg([], [])
eq_len1C_in_gg(.(T27, T28), .(T29, T30)) → U2_gg(T27, T28, T29, T30, eq_len1C_in_gg(T28, T30))
U2_gg(T27, T28, T29, T30, eq_len1C_out_gg(T28, T30)) → eq_len1C_out_gg(.(T27, T28), .(T29, T30))
U7_gggg(T16, T18, T15, T17, eq_len1C_out_gg(T16, T18)) → U8_gggg(T16, T18, T15, T17, same_setsE_in_gggg(T15, T16, T17, T18))
same_setsE_in_gggg(T43, T44, T45, T46) → U4_gggg(T43, T44, T45, T46, pF_in_gggg(T43, T45, T46, T44))
pF_in_gggg(T43, T45, T46, T44) → U9_gggg(T43, T45, T46, T44, memberG_in_ggg(T43, T45, T46))
memberG_in_ggg(T63, T63, T64) → memberG_out_ggg(T63, T63, T64)
memberG_in_ggg(T75, T76, T77) → U5_ggg(T75, T76, T77, memberD_in_gg(T75, T77))
memberD_in_gg(T90, .(T90, T91)) → memberD_out_gg(T90, .(T90, T91))
memberD_in_gg(T98, .(T99, T100)) → U3_gg(T98, T99, T100, memberD_in_gg(T98, T100))
U3_gg(T98, T99, T100, memberD_out_gg(T98, T100)) → memberD_out_gg(T98, .(T99, T100))
U5_ggg(T75, T76, T77, memberD_out_gg(T75, T77)) → memberG_out_ggg(T75, T76, T77)
U9_gggg(T43, T45, T46, T44, memberG_out_ggg(T43, T45, T46)) → U10_gggg(T43, T45, T46, T44, same_setsH_in_ggg(T44, T45, T46))
same_setsH_in_ggg([], T117, T118) → same_setsH_out_ggg([], T117, T118)
same_setsH_in_ggg(.(T127, T128), T129, T130) → U6_ggg(T127, T128, T129, T130, pF_in_gggg(T127, T129, T130, T128))
U6_ggg(T127, T128, T129, T130, pF_out_gggg(T127, T129, T130, T128)) → same_setsH_out_ggg(.(T127, T128), T129, T130)
U10_gggg(T43, T45, T46, T44, same_setsH_out_ggg(T44, T45, T46)) → pF_out_gggg(T43, T45, T46, T44)
U4_gggg(T43, T44, T45, T46, pF_out_gggg(T43, T45, T46, T44)) → same_setsE_out_gggg(T43, T44, T45, T46)
U8_gggg(T16, T18, T15, T17, same_setsE_out_gggg(T15, T16, T17, T18)) → pB_out_gggg(T16, T18, T15, T17)
U1_gg(T15, T16, T17, T18, pB_out_gggg(T16, T18, T15, T17)) → perm1A_out_gg(.(T15, T16), .(T17, T18))

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

(8) UsableRulesProof (EQUIVALENT transformation)

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

(9) Obligation:

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

MEMBERD_IN_GG(T98, .(T99, T100)) → MEMBERD_IN_GG(T98, T100)

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:

MEMBERD_IN_GG(T98, .(T99, T100)) → MEMBERD_IN_GG(T98, T100)

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:

• MEMBERD_IN_GG(T98, .(T99, T100)) → MEMBERD_IN_GG(T98, T100)
  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:

U9_GGGG(T43, T45, T46, T44, memberG_out_ggg(T43, T45, T46)) → SAME_SETSH_IN_GGG(T44, T45, T46)
SAME_SETSH_IN_GGG(.(T127, T128), T129, T130) → PF_IN_GGGG(T127, T129, T130, T128)
PF_IN_GGGG(T43, T45, T46, T44) → U9_GGGG(T43, T45, T46, T44, memberG_in_ggg(T43, T45, T46))

The TRS R consists of the following rules:

perm1A_in_gg([], []) → perm1A_out_gg([], [])
perm1A_in_gg(.(T15, T16), .(T17, T18)) → U1_gg(T15, T16, T17, T18, pB_in_gggg(T16, T18, T15, T17))
pB_in_gggg(T16, T18, T15, T17) → U7_gggg(T16, T18, T15, T17, eq_len1C_in_gg(T16, T18))
eq_len1C_in_gg([], []) → eq_len1C_out_gg([], [])
eq_len1C_in_gg(.(T27, T28), .(T29, T30)) → U2_gg(T27, T28, T29, T30, eq_len1C_in_gg(T28, T30))
U2_gg(T27, T28, T29, T30, eq_len1C_out_gg(T28, T30)) → eq_len1C_out_gg(.(T27, T28), .(T29, T30))
U7_gggg(T16, T18, T15, T17, eq_len1C_out_gg(T16, T18)) → U8_gggg(T16, T18, T15, T17, same_setsE_in_gggg(T15, T16, T17, T18))
same_setsE_in_gggg(T43, T44, T45, T46) → U4_gggg(T43, T44, T45, T46, pF_in_gggg(T43, T45, T46, T44))
pF_in_gggg(T43, T45, T46, T44) → U9_gggg(T43, T45, T46, T44, memberG_in_ggg(T43, T45, T46))
memberG_in_ggg(T63, T63, T64) → memberG_out_ggg(T63, T63, T64)
memberG_in_ggg(T75, T76, T77) → U5_ggg(T75, T76, T77, memberD_in_gg(T75, T77))
memberD_in_gg(T90, .(T90, T91)) → memberD_out_gg(T90, .(T90, T91))
memberD_in_gg(T98, .(T99, T100)) → U3_gg(T98, T99, T100, memberD_in_gg(T98, T100))
U3_gg(T98, T99, T100, memberD_out_gg(T98, T100)) → memberD_out_gg(T98, .(T99, T100))
U5_ggg(T75, T76, T77, memberD_out_gg(T75, T77)) → memberG_out_ggg(T75, T76, T77)
U9_gggg(T43, T45, T46, T44, memberG_out_ggg(T43, T45, T46)) → U10_gggg(T43, T45, T46, T44, same_setsH_in_ggg(T44, T45, T46))
same_setsH_in_ggg([], T117, T118) → same_setsH_out_ggg([], T117, T118)
same_setsH_in_ggg(.(T127, T128), T129, T130) → U6_ggg(T127, T128, T129, T130, pF_in_gggg(T127, T129, T130, T128))
U6_ggg(T127, T128, T129, T130, pF_out_gggg(T127, T129, T130, T128)) → same_setsH_out_ggg(.(T127, T128), T129, T130)
U10_gggg(T43, T45, T46, T44, same_setsH_out_ggg(T44, T45, T46)) → pF_out_gggg(T43, T45, T46, T44)
U4_gggg(T43, T44, T45, T46, pF_out_gggg(T43, T45, T46, T44)) → same_setsE_out_gggg(T43, T44, T45, T46)
U8_gggg(T16, T18, T15, T17, same_setsE_out_gggg(T15, T16, T17, T18)) → pB_out_gggg(T16, T18, T15, T17)
U1_gg(T15, T16, T17, T18, pB_out_gggg(T16, T18, T15, T17)) → perm1A_out_gg(.(T15, T16), .(T17, T18))

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

(15) UsableRulesProof (EQUIVALENT transformation)

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

(16) Obligation:

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

U9_GGGG(T43, T45, T46, T44, memberG_out_ggg(T43, T45, T46)) → SAME_SETSH_IN_GGG(T44, T45, T46)
SAME_SETSH_IN_GGG(.(T127, T128), T129, T130) → PF_IN_GGGG(T127, T129, T130, T128)
PF_IN_GGGG(T43, T45, T46, T44) → U9_GGGG(T43, T45, T46, T44, memberG_in_ggg(T43, T45, T46))

The TRS R consists of the following rules:

memberG_in_ggg(T63, T63, T64) → memberG_out_ggg(T63, T63, T64)
memberG_in_ggg(T75, T76, T77) → U5_ggg(T75, T76, T77, memberD_in_gg(T75, T77))
U5_ggg(T75, T76, T77, memberD_out_gg(T75, T77)) → memberG_out_ggg(T75, T76, T77)
memberD_in_gg(T90, .(T90, T91)) → memberD_out_gg(T90, .(T90, T91))
memberD_in_gg(T98, .(T99, T100)) → U3_gg(T98, T99, T100, memberD_in_gg(T98, T100))
U3_gg(T98, T99, T100, memberD_out_gg(T98, T100)) → memberD_out_gg(T98, .(T99, T100))

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

(17) PiDPToQDPProof (EQUIVALENT transformation)

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

(18) Obligation:

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

U9_GGGG(T43, T45, T46, T44, memberG_out_ggg(T43, T45, T46)) → SAME_SETSH_IN_GGG(T44, T45, T46)
SAME_SETSH_IN_GGG(.(T127, T128), T129, T130) → PF_IN_GGGG(T127, T129, T130, T128)
PF_IN_GGGG(T43, T45, T46, T44) → U9_GGGG(T43, T45, T46, T44, memberG_in_ggg(T43, T45, T46))

The TRS R consists of the following rules:

memberG_in_ggg(T63, T63, T64) → memberG_out_ggg(T63, T63, T64)
memberG_in_ggg(T75, T76, T77) → U5_ggg(T75, T76, T77, memberD_in_gg(T75, T77))
U5_ggg(T75, T76, T77, memberD_out_gg(T75, T77)) → memberG_out_ggg(T75, T76, T77)
memberD_in_gg(T90, .(T90, T91)) → memberD_out_gg(T90, .(T90, T91))
memberD_in_gg(T98, .(T99, T100)) → U3_gg(T98, T99, T100, memberD_in_gg(T98, T100))
U3_gg(T98, T99, T100, memberD_out_gg(T98, T100)) → memberD_out_gg(T98, .(T99, T100))

The set Q consists of the following terms:

memberG_in_ggg(x0, x1, x2)
U5_ggg(x0, x1, x2, x3)
memberD_in_gg(x0, x1)
U3_gg(x0, x1, x2, x3)

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

(19) QDPSizeChangeProof (EQUIVALENT transformation)

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

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

• SAME_SETSH_IN_GGG(.(T127, T128), T129, T130) → PF_IN_GGGG(T127, T129, T130, T128)
  The graph contains the following edges 1 > 1, 2 >= 2, 3 >= 3, 1 > 4

• PF_IN_GGGG(T43, T45, T46, T44) → U9_GGGG(T43, T45, T46, T44, memberG_in_ggg(T43, T45, T46))
  The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 3, 4 >= 4

• U9_GGGG(T43, T45, T46, T44, memberG_out_ggg(T43, T45, T46)) → SAME_SETSH_IN_GGG(T44, T45, T46)
  The graph contains the following edges 4 >= 1, 2 >= 2, 5 > 2, 3 >= 3, 5 > 3

(20) YES

(21) Obligation:

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

EQ_LEN1C_IN_GG(.(T27, T28), .(T29, T30)) → EQ_LEN1C_IN_GG(T28, T30)

The TRS R consists of the following rules:

perm1A_in_gg([], []) → perm1A_out_gg([], [])
perm1A_in_gg(.(T15, T16), .(T17, T18)) → U1_gg(T15, T16, T17, T18, pB_in_gggg(T16, T18, T15, T17))
pB_in_gggg(T16, T18, T15, T17) → U7_gggg(T16, T18, T15, T17, eq_len1C_in_gg(T16, T18))
eq_len1C_in_gg([], []) → eq_len1C_out_gg([], [])
eq_len1C_in_gg(.(T27, T28), .(T29, T30)) → U2_gg(T27, T28, T29, T30, eq_len1C_in_gg(T28, T30))
U2_gg(T27, T28, T29, T30, eq_len1C_out_gg(T28, T30)) → eq_len1C_out_gg(.(T27, T28), .(T29, T30))
U7_gggg(T16, T18, T15, T17, eq_len1C_out_gg(T16, T18)) → U8_gggg(T16, T18, T15, T17, same_setsE_in_gggg(T15, T16, T17, T18))
same_setsE_in_gggg(T43, T44, T45, T46) → U4_gggg(T43, T44, T45, T46, pF_in_gggg(T43, T45, T46, T44))
pF_in_gggg(T43, T45, T46, T44) → U9_gggg(T43, T45, T46, T44, memberG_in_ggg(T43, T45, T46))
memberG_in_ggg(T63, T63, T64) → memberG_out_ggg(T63, T63, T64)
memberG_in_ggg(T75, T76, T77) → U5_ggg(T75, T76, T77, memberD_in_gg(T75, T77))
memberD_in_gg(T90, .(T90, T91)) → memberD_out_gg(T90, .(T90, T91))
memberD_in_gg(T98, .(T99, T100)) → U3_gg(T98, T99, T100, memberD_in_gg(T98, T100))
U3_gg(T98, T99, T100, memberD_out_gg(T98, T100)) → memberD_out_gg(T98, .(T99, T100))
U5_ggg(T75, T76, T77, memberD_out_gg(T75, T77)) → memberG_out_ggg(T75, T76, T77)
U9_gggg(T43, T45, T46, T44, memberG_out_ggg(T43, T45, T46)) → U10_gggg(T43, T45, T46, T44, same_setsH_in_ggg(T44, T45, T46))
same_setsH_in_ggg([], T117, T118) → same_setsH_out_ggg([], T117, T118)
same_setsH_in_ggg(.(T127, T128), T129, T130) → U6_ggg(T127, T128, T129, T130, pF_in_gggg(T127, T129, T130, T128))
U6_ggg(T127, T128, T129, T130, pF_out_gggg(T127, T129, T130, T128)) → same_setsH_out_ggg(.(T127, T128), T129, T130)
U10_gggg(T43, T45, T46, T44, same_setsH_out_ggg(T44, T45, T46)) → pF_out_gggg(T43, T45, T46, T44)
U4_gggg(T43, T44, T45, T46, pF_out_gggg(T43, T45, T46, T44)) → same_setsE_out_gggg(T43, T44, T45, T46)
U8_gggg(T16, T18, T15, T17, same_setsE_out_gggg(T15, T16, T17, T18)) → pB_out_gggg(T16, T18, T15, T17)
U1_gg(T15, T16, T17, T18, pB_out_gggg(T16, T18, T15, T17)) → perm1A_out_gg(.(T15, T16), .(T17, T18))

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

(22) UsableRulesProof (EQUIVALENT transformation)

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

(23) Obligation:

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

EQ_LEN1C_IN_GG(.(T27, T28), .(T29, T30)) → EQ_LEN1C_IN_GG(T28, T30)

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

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

EQ_LEN1C_IN_GG(.(T27, T28), .(T29, T30)) → EQ_LEN1C_IN_GG(T28, T30)

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:

• EQ_LEN1C_IN_GG(.(T27, T28), .(T29, T30)) → EQ_LEN1C_IN_GG(T28, T30)
  The graph contains the following edges 1 > 1, 2 > 2

(27) YES