81 apply(rule conjI) |
81 apply(rule conjI) |
82 apply(elim conjE) |
82 apply(elim conjE) |
83 apply(erule_tac c="(da,ea)" in Abs_lst1_fcb2) |
83 apply(erule_tac c="(da,ea)" in Abs_lst1_fcb2) |
84 apply(simp add: Abs_fresh_iff) |
84 apply(simp add: Abs_fresh_iff) |
85 apply(simp add: fresh_at_base fresh_star_def fresh_Pair) |
85 apply(simp add: fresh_at_base fresh_star_def fresh_Pair) |
86 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
86 apply(simp add: eqvt_at_def) |
87 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
87 apply(simp add: atom_eqvt fresh_star_Pair perm_supp_eq) |
|
88 apply(clarify) |
|
89 apply(simp add: eqvt_at_def) |
|
90 apply(simp add: atom_eqvt fresh_star_Pair perm_supp_eq) |
88 apply(elim conjE) |
91 apply(elim conjE) |
89 apply(erule_tac c="(da,ea)" in Abs_lst1_fcb2) |
92 apply(erule_tac c="(da,ea)" in Abs_lst1_fcb2) |
90 apply(simp add: Abs_fresh_iff) |
93 apply(simp add: Abs_fresh_iff) |
91 apply(simp add: fresh_at_base fresh_star_def fresh_Pair) |
94 apply(simp add: fresh_at_base fresh_star_def fresh_Pair) |
92 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
95 apply(simp add: eqvt_at_def) |
93 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
96 apply(simp add: atom_eqvt fresh_star_Pair perm_supp_eq) |
94 apply(elim conjE) |
97 apply(simp add: eqvt_at_def) |
95 apply(subgoal_tac "eqvt_at crename_sumC (M, da, ea)") |
98 apply(simp add: atom_eqvt fresh_star_Pair perm_supp_eq) |
96 apply(subgoal_tac "eqvt_at crename_sumC (Ma, da, ea)") |
99 apply(elim conjE) |
97 apply(erule Abs_lst1_fcb2) |
100 apply(subgoal_tac "eqvt_at crename_sumC (M, da, ea)") |
98 apply(simp add: Abs_fresh_iff) |
101 apply(subgoal_tac "eqvt_at crename_sumC (Ma, da, ea)") |
99 apply(simp add: fresh_at_base fresh_star_def fresh_Pair) |
102 apply(erule Abs_lst1_fcb2) |
100 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
103 apply(simp add: Abs_fresh_iff) |
|
104 apply(simp add: fresh_at_base fresh_star_def fresh_Pair) |
|
105 apply(simp add: eqvt_at_def) |
|
106 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
|
107 apply(simp add: eqvt_at_def) |
101 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
108 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
102 apply(blast) |
109 apply(blast) |
103 apply(blast) |
110 apply(blast) |
104 apply(elim conjE) |
111 apply(elim conjE) |
105 apply(erule_tac c="(da,ea)" in Abs_lst1_fcb2) |
112 apply(erule_tac c="(da,ea)" in Abs_lst1_fcb2) |
106 apply(simp add: Abs_fresh_iff) |
113 apply(simp add: Abs_fresh_iff) |
107 apply(simp add: fresh_at_base fresh_star_def fresh_Pair) |
114 apply(simp add: fresh_at_base fresh_star_def fresh_Pair) |
108 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
115 apply(simp add: eqvt_at_def) |
109 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
116 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
110 apply(rule conjI) |
117 apply(simp add: eqvt_at_def) |
111 apply(elim conjE) |
118 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
112 apply(subgoal_tac "eqvt_at crename_sumC (M, da, ea)") |
119 apply(rule conjI) |
113 apply(subgoal_tac "eqvt_at crename_sumC (Ma, da, ea)") |
120 apply(elim conjE) |
114 apply(erule Abs_lst1_fcb2) |
121 apply(subgoal_tac "eqvt_at crename_sumC (M, da, ea)") |
115 apply(simp add: Abs_fresh_iff) |
122 apply(subgoal_tac "eqvt_at crename_sumC (Ma, da, ea)") |
116 apply(simp add: fresh_at_base fresh_star_def fresh_Pair) |
123 apply(erule Abs_lst1_fcb2) |
117 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
124 apply(simp add: Abs_fresh_iff) |
|
125 apply(simp add: fresh_at_base fresh_star_def fresh_Pair) |
|
126 apply(simp add: eqvt_at_def) |
|
127 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
|
128 apply(simp add: eqvt_at_def) |
118 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
129 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
119 apply(blast) |
130 apply(blast) |
120 apply(blast) |
131 apply(blast) |
121 apply(erule conjE)+ |
132 apply(erule conjE)+ |
122 apply(subgoal_tac "eqvt_at crename_sumC (N, da, ea)") |
133 apply(subgoal_tac "eqvt_at crename_sumC (N, da, ea)") |
123 apply(subgoal_tac "eqvt_at crename_sumC (Na, da, ea)") |
134 apply(subgoal_tac "eqvt_at crename_sumC (Na, da, ea)") |
124 apply(erule Abs_lst1_fcb2) |
135 apply(erule Abs_lst1_fcb2) |
125 apply(simp add: Abs_fresh_iff) |
136 apply(simp add: Abs_fresh_iff) |
126 apply(simp add: fresh_at_base fresh_star_def fresh_Pair) |
137 apply(simp add: fresh_at_base fresh_star_def fresh_Pair) |
127 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
138 apply(simp add: eqvt_at_def) |
|
139 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
|
140 apply(simp add: eqvt_at_def) |
128 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
141 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
129 apply(blast) |
142 apply(blast) |
130 apply(blast) |
143 apply(blast) |
131 apply(elim conjE) |
144 apply(elim conjE) |
132 apply(erule_tac c="(da,ea)" in Abs_lst1_fcb2) |
145 apply(erule_tac c="(da,ea)" in Abs_lst1_fcb2) |
133 apply(simp add: Abs_fresh_iff) |
146 apply(simp add: Abs_fresh_iff) |
134 apply(simp add: fresh_at_base fresh_star_def fresh_Pair) |
147 apply(simp add: fresh_at_base fresh_star_def fresh_Pair) |
135 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
148 apply(simp add: eqvt_at_def) |
|
149 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
|
150 apply(simp add: eqvt_at_def) |
136 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
151 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
137 apply(elim conjE) |
152 apply(elim conjE) |
138 apply(erule_tac c="(da,ea)" in Abs_lst1_fcb2) |
153 apply(erule_tac c="(da,ea)" in Abs_lst1_fcb2) |
139 apply(simp add: Abs_fresh_iff) |
154 apply(simp add: Abs_fresh_iff) |
140 apply(simp add: fresh_at_base fresh_star_def fresh_Pair) |
155 apply(simp add: fresh_at_base fresh_star_def fresh_Pair) |
141 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
156 apply(simp add: eqvt_at_def) |
142 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
157 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
143 apply(elim conjE) |
158 apply(simp add: eqvt_at_def) |
144 apply(subgoal_tac "eqvt_at crename_sumC (M, da, ea)") |
159 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
145 apply(subgoal_tac "eqvt_at crename_sumC (Ma, da, ea)") |
160 apply(elim conjE) |
146 apply(erule Abs_lst1_fcb2) |
161 apply(subgoal_tac "eqvt_at crename_sumC (M, da, ea)") |
147 apply(simp add: Abs_fresh_iff) |
162 apply(subgoal_tac "eqvt_at crename_sumC (Ma, da, ea)") |
148 apply(simp add: fresh_at_base fresh_star_def fresh_Pair) |
163 apply(erule Abs_lst1_fcb2) |
149 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
164 apply(simp add: Abs_fresh_iff) |
150 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
165 apply(simp add: fresh_at_base fresh_star_def fresh_Pair) |
151 apply(blast) |
166 apply(simp add: eqvt_at_def) |
152 apply(blast) |
167 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
153 apply(erule conjE)+ |
168 apply(simp add: eqvt_at_def) |
154 apply(subgoal_tac "eqvt_at crename_sumC (M, da, ea)") |
169 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
155 apply(subgoal_tac "eqvt_at crename_sumC (Ma, da, ea)") |
170 apply(blast) |
156 apply(erule Abs_lst1_fcb2) |
171 apply(blast) |
157 apply(simp add: Abs_fresh_iff) |
172 apply(erule conjE)+ |
158 apply(simp add: fresh_at_base fresh_star_def fresh_Pair) |
173 apply(subgoal_tac "eqvt_at crename_sumC (M, da, ea)") |
159 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
174 apply(subgoal_tac "eqvt_at crename_sumC (Ma, da, ea)") |
160 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
175 apply(erule Abs_lst1_fcb2) |
161 apply(blast) |
176 apply(simp add: Abs_fresh_iff) |
162 apply(blast) |
177 apply(simp add: fresh_at_base fresh_star_def fresh_Pair) |
163 apply(rule conjI) |
178 apply(simp add: eqvt_at_def) |
164 apply(erule conjE)+ |
179 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
165 apply(subgoal_tac "eqvt_at crename_sumC (M, da, ea)") |
180 apply(simp add: eqvt_at_def) |
166 apply(subgoal_tac "eqvt_at crename_sumC (Ma, da, ea)") |
181 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
167 apply(erule Abs_lst1_fcb2) |
182 apply(blast) |
168 apply(simp add: Abs_fresh_iff) |
183 apply(blast) |
169 apply(simp add: fresh_at_base fresh_star_def fresh_Pair) |
184 apply(rule conjI) |
170 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
185 apply(erule conjE)+ |
|
186 apply(subgoal_tac "eqvt_at crename_sumC (M, da, ea)") |
|
187 apply(subgoal_tac "eqvt_at crename_sumC (Ma, da, ea)") |
|
188 apply(erule Abs_lst1_fcb2) |
|
189 apply(simp add: Abs_fresh_iff) |
|
190 apply(simp add: fresh_at_base fresh_star_def fresh_Pair) |
|
191 apply(simp add: eqvt_at_def) |
|
192 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
|
193 apply(simp add: eqvt_at_def) |
171 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
194 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
172 apply(blast) |
195 apply(blast) |
173 apply(blast) |
196 apply(blast) |
174 apply(erule conjE)+ |
197 apply(erule conjE)+ |
175 apply(subgoal_tac "eqvt_at crename_sumC (N, da, ea)") |
198 apply(subgoal_tac "eqvt_at crename_sumC (N, da, ea)") |
176 apply(subgoal_tac "eqvt_at crename_sumC (Na, da, ea)") |
199 apply(subgoal_tac "eqvt_at crename_sumC (Na, da, ea)") |
177 apply(erule Abs_lst1_fcb2) |
200 apply(erule Abs_lst1_fcb2) |
178 apply(simp add: Abs_fresh_iff) |
201 apply(simp add: Abs_fresh_iff) |
179 apply(simp add: fresh_at_base fresh_star_def fresh_Pair) |
202 apply(simp add: fresh_at_base fresh_star_def fresh_Pair) |
180 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
203 apply(simp add: eqvt_at_def) |
|
204 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
|
205 apply(simp add: eqvt_at_def) |
181 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
206 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
182 apply(blast) |
207 apply(blast) |
183 apply(blast) |
208 apply(blast) |
184 defer |
209 defer |
185 apply(erule conjE)+ |
210 apply(erule conjE)+ |
252 apply(rule conjI) |
284 apply(rule conjI) |
253 apply(elim conjE) |
285 apply(elim conjE) |
254 apply(erule_tac c="(ua,va)" in Abs_lst1_fcb2) |
286 apply(erule_tac c="(ua,va)" in Abs_lst1_fcb2) |
255 apply(simp add: Abs_fresh_iff) |
287 apply(simp add: Abs_fresh_iff) |
256 apply(simp add: fresh_at_base fresh_star_def fresh_Pair) |
288 apply(simp add: fresh_at_base fresh_star_def fresh_Pair) |
257 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
289 apply(simp add: eqvt_at_def) |
|
290 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
|
291 apply(simp add: eqvt_at_def) |
258 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
292 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
259 apply(elim conjE) |
293 apply(elim conjE) |
260 apply(erule_tac c="(ua,va)" in Abs_lst1_fcb2) |
294 apply(erule_tac c="(ua,va)" in Abs_lst1_fcb2) |
261 apply(simp add: Abs_fresh_iff) |
295 apply(simp add: Abs_fresh_iff) |
262 apply(simp add: fresh_at_base fresh_star_def fresh_Pair) |
296 apply(simp add: fresh_at_base fresh_star_def fresh_Pair) |
263 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
297 apply(simp add: eqvt_at_def) |
|
298 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
|
299 apply(simp add: eqvt_at_def) |
264 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
300 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
265 apply(elim conjE) |
301 apply(elim conjE) |
266 apply(erule_tac c="(ua,va)" in Abs_lst1_fcb2) |
302 apply(erule_tac c="(ua,va)" in Abs_lst1_fcb2) |
267 apply(simp add: Abs_fresh_iff) |
303 apply(simp add: Abs_fresh_iff) |
268 apply(simp add: fresh_at_base fresh_star_def fresh_Pair) |
304 apply(simp add: fresh_at_base fresh_star_def fresh_Pair) |
269 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
305 apply(simp add: eqvt_at_def) |
270 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
306 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
271 apply(elim conjE) |
307 apply(simp add: eqvt_at_def) |
272 apply(subgoal_tac "eqvt_at nrename_sumC (M, ua, va)") |
308 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
273 apply(subgoal_tac "eqvt_at nrename_sumC (Ma, ua, va)") |
309 apply(elim conjE) |
274 apply(erule Abs_lst1_fcb2) |
310 apply(subgoal_tac "eqvt_at nrename_sumC (M, ua, va)") |
275 apply(simp add: Abs_fresh_iff) |
311 apply(subgoal_tac "eqvt_at nrename_sumC (Ma, ua, va)") |
276 apply(simp add: fresh_at_base fresh_star_def fresh_Pair) |
312 apply(erule Abs_lst1_fcb2) |
277 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
313 apply(simp add: Abs_fresh_iff) |
278 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
314 apply(simp add: fresh_at_base fresh_star_def fresh_Pair) |
279 apply(blast) |
315 apply(simp add: eqvt_at_def) |
280 apply(blast) |
316 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
281 apply(elim conjE) |
317 apply(simp add: eqvt_at_def) |
282 apply(rule conjI) |
318 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
283 apply(subgoal_tac "eqvt_at nrename_sumC (M, ua, va)") |
319 apply(blast) |
284 apply(subgoal_tac "eqvt_at nrename_sumC (Ma, ua, va)") |
320 apply(blast) |
285 apply(erule Abs_lst1_fcb2) |
321 apply(elim conjE) |
286 apply(simp add: Abs_fresh_iff) |
322 apply(rule conjI) |
287 apply(simp add: fresh_at_base fresh_star_def fresh_Pair) |
323 apply(subgoal_tac "eqvt_at nrename_sumC (M, ua, va)") |
288 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
324 apply(subgoal_tac "eqvt_at nrename_sumC (Ma, ua, va)") |
|
325 apply(erule Abs_lst1_fcb2) |
|
326 apply(simp add: Abs_fresh_iff) |
|
327 apply(simp add: fresh_at_base fresh_star_def fresh_Pair) |
|
328 apply(simp add: eqvt_at_def) |
|
329 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
|
330 apply(simp add: eqvt_at_def) |
289 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
331 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
290 apply(blast) |
332 apply(blast) |
291 apply(blast) |
333 apply(blast) |
292 apply(subgoal_tac "eqvt_at nrename_sumC (N, ua, va)") |
334 apply(subgoal_tac "eqvt_at nrename_sumC (N, ua, va)") |
293 apply(subgoal_tac "eqvt_at nrename_sumC (Na, ua, va)") |
335 apply(subgoal_tac "eqvt_at nrename_sumC (Na, ua, va)") |
294 apply(erule Abs_lst1_fcb2) |
336 apply(erule Abs_lst1_fcb2) |
295 apply(simp add: Abs_fresh_iff) |
337 apply(simp add: Abs_fresh_iff) |
296 apply(simp add: fresh_at_base fresh_star_def fresh_Pair) |
338 apply(simp add: fresh_at_base fresh_star_def fresh_Pair) |
297 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
339 apply(simp add: eqvt_at_def) |
298 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
340 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
299 apply(blast) |
341 apply(simp add: eqvt_at_def) |
300 apply(blast) |
342 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
301 apply(elim conjE) |
343 apply(blast) |
302 apply(subgoal_tac "eqvt_at nrename_sumC (M, ua, va)") |
344 apply(blast) |
303 apply(subgoal_tac "eqvt_at nrename_sumC (Ma, ua, va)") |
345 apply(elim conjE) |
304 apply(erule Abs_lst1_fcb2) |
346 apply(subgoal_tac "eqvt_at nrename_sumC (M, ua, va)") |
305 apply(simp add: Abs_fresh_iff) |
347 apply(subgoal_tac "eqvt_at nrename_sumC (Ma, ua, va)") |
306 apply(simp add: fresh_at_base fresh_star_def fresh_Pair) |
348 apply(erule Abs_lst1_fcb2) |
307 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
349 apply(simp add: Abs_fresh_iff) |
|
350 apply(simp add: fresh_at_base fresh_star_def fresh_Pair) |
|
351 apply(simp add: eqvt_at_def) |
|
352 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
|
353 apply(simp add: eqvt_at_def) |
308 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
354 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
309 apply(blast) |
355 apply(blast) |
310 apply(blast) |
356 apply(blast) |
311 apply(elim conjE)+ |
357 apply(elim conjE)+ |
312 apply(subgoal_tac "eqvt_at nrename_sumC (M, ua, va)") |
358 apply(subgoal_tac "eqvt_at nrename_sumC (M, ua, va)") |
313 apply(subgoal_tac "eqvt_at nrename_sumC (Ma, ua, va)") |
359 apply(subgoal_tac "eqvt_at nrename_sumC (Ma, ua, va)") |
314 apply(erule Abs_lst1_fcb2) |
360 apply(erule Abs_lst1_fcb2) |
315 apply(simp add: Abs_fresh_iff) |
361 apply(simp add: Abs_fresh_iff) |
316 apply(simp add: fresh_at_base fresh_star_def fresh_Pair) |
362 apply(simp add: fresh_at_base fresh_star_def fresh_Pair) |
317 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
363 apply(simp add: eqvt_at_def) |
|
364 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
|
365 apply(simp add: eqvt_at_def) |
318 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
366 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
319 apply(blast) |
367 apply(blast) |
320 apply(blast) |
368 apply(blast) |
321 apply(elim conjE)+ |
369 apply(elim conjE)+ |
322 apply(erule_tac c="(ua,va)" in Abs_lst1_fcb2) |
370 apply(erule_tac c="(ua,va)" in Abs_lst1_fcb2) |
323 apply(simp add: Abs_fresh_iff) |
371 apply(simp add: Abs_fresh_iff) |
324 apply(simp add: fresh_at_base fresh_star_def fresh_Pair) |
372 apply(simp add: fresh_at_base fresh_star_def fresh_Pair) |
325 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
373 apply(simp add: eqvt_at_def) |
|
374 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
|
375 apply(simp add: eqvt_at_def) |
326 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
376 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
327 apply(elim conjE) |
377 apply(elim conjE) |
328 apply(erule_tac c="(ua,va)" in Abs_lst1_fcb2) |
378 apply(erule_tac c="(ua,va)" in Abs_lst1_fcb2) |
329 apply(simp add: Abs_fresh_iff) |
379 apply(simp add: Abs_fresh_iff) |
330 apply(simp add: fresh_at_base fresh_star_def fresh_Pair) |
380 apply(simp add: fresh_at_base fresh_star_def fresh_Pair) |
331 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
381 apply(simp add: eqvt_at_def) |
332 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
382 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
333 apply(elim conjE) |
383 apply(simp add: eqvt_at_def) |
334 apply(rule conjI) |
384 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
335 apply(subgoal_tac "eqvt_at nrename_sumC (M, ua, va)") |
385 apply(elim conjE) |
336 apply(subgoal_tac "eqvt_at nrename_sumC (Ma, ua, va)") |
386 apply(rule conjI) |
337 apply(erule Abs_lst1_fcb2) |
387 apply(subgoal_tac "eqvt_at nrename_sumC (M, ua, va)") |
338 apply(simp add: Abs_fresh_iff) |
388 apply(subgoal_tac "eqvt_at nrename_sumC (Ma, ua, va)") |
339 apply(simp add: fresh_at_base fresh_star_def fresh_Pair) |
389 apply(erule Abs_lst1_fcb2) |
340 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
390 apply(simp add: Abs_fresh_iff) |
|
391 apply(simp add: fresh_at_base fresh_star_def fresh_Pair) |
|
392 apply(simp add: eqvt_at_def) |
|
393 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
|
394 apply(simp add: eqvt_at_def) |
341 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
395 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
342 apply(blast) |
396 apply(blast) |
343 apply(blast) |
397 apply(blast) |
344 apply(subgoal_tac "eqvt_at nrename_sumC (N, ua, va)") |
398 apply(subgoal_tac "eqvt_at nrename_sumC (N, ua, va)") |
345 apply(subgoal_tac "eqvt_at nrename_sumC (Na, ua, va)") |
399 apply(subgoal_tac "eqvt_at nrename_sumC (Na, ua, va)") |
346 apply(erule Abs_lst1_fcb2) |
400 apply(erule Abs_lst1_fcb2) |
347 apply(simp add: Abs_fresh_iff) |
401 apply(simp add: Abs_fresh_iff) |
348 apply(simp add: fresh_at_base fresh_star_def fresh_Pair) |
402 apply(simp add: fresh_at_base fresh_star_def fresh_Pair) |
349 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
403 apply(simp add: eqvt_at_def) |
|
404 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
|
405 apply(simp add: eqvt_at_def) |
350 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
406 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
351 apply(blast) |
407 apply(blast) |
352 apply(blast) |
408 apply(blast) |
353 apply(erule conjE)+ |
409 apply(erule conjE)+ |
354 apply(erule Abs_lst_fcb2) |
410 apply(erule Abs_lst_fcb2) |
355 apply(simp add: Abs_fresh_star) |
411 apply(simp add: Abs_fresh_star) |
356 apply(simp add: fresh_at_base fresh_star_def fresh_Pair) |
412 apply(simp add: fresh_at_base fresh_star_def fresh_Pair) |
357 apply(simp add: fresh_at_base fresh_star_def fresh_Pair) |
413 apply(simp add: fresh_at_base fresh_star_def fresh_Pair) |
358 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
414 apply(simp add: eqvt_at_def) |
359 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
415 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
360 apply(erule conjE)+ |
416 apply(simp add: eqvt_at_def) |
361 apply(rule conjI) |
417 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
362 apply(subgoal_tac "eqvt_at nrename_sumC (M, ua, va)") |
418 apply(erule conjE)+ |
363 apply(subgoal_tac "eqvt_at nrename_sumC (Ma, ua, va)") |
419 apply(rule conjI) |
364 apply(erule Abs_lst1_fcb2) |
420 apply(subgoal_tac "eqvt_at nrename_sumC (M, ua, va)") |
365 apply(simp add: Abs_fresh_iff) |
421 apply(subgoal_tac "eqvt_at nrename_sumC (Ma, ua, va)") |
366 apply(simp add: fresh_at_base fresh_star_def fresh_Pair) |
422 apply(erule Abs_lst1_fcb2) |
367 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
423 apply(simp add: Abs_fresh_iff) |
|
424 apply(simp add: fresh_at_base fresh_star_def fresh_Pair) |
|
425 apply(simp add: eqvt_at_def) |
|
426 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
|
427 apply(simp add: eqvt_at_def) |
368 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
428 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
369 apply(blast) |
429 apply(blast) |
370 apply(blast) |
430 apply(blast) |
371 apply(subgoal_tac "eqvt_at nrename_sumC (N, ua, va)") |
431 apply(subgoal_tac "eqvt_at nrename_sumC (N, ua, va)") |
372 apply(subgoal_tac "eqvt_at nrename_sumC (Na, ua, va)") |
432 apply(subgoal_tac "eqvt_at nrename_sumC (Na, ua, va)") |
373 apply(erule Abs_lst1_fcb2) |
433 apply(erule Abs_lst1_fcb2) |
374 apply(simp add: Abs_fresh_iff) |
434 apply(simp add: Abs_fresh_iff) |
375 apply(simp add: fresh_at_base fresh_star_def fresh_Pair) |
435 apply(simp add: fresh_at_base fresh_star_def fresh_Pair) |
376 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
436 apply(simp add: eqvt_at_def) |
|
437 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
|
438 apply(simp add: eqvt_at_def) |
377 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
439 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
378 apply(blast) |
440 apply(blast) |
379 apply(blast) |
441 apply(blast) |
380 done |
442 done |
381 |
443 |