equal
deleted
inserted
replaced
271 apply(drule_tac a="atom (xa)" in fresh_eqvt_at) |
271 apply(drule_tac a="atom (xa)" in fresh_eqvt_at) |
272 apply(simp_all add: finite_supp fresh_Pair) |
272 apply(simp_all add: finite_supp fresh_Pair) |
273 apply(subgoal_tac "(atom x \<rightleftharpoons> atom xa) \<bullet> sa = sa") |
273 apply(subgoal_tac "(atom x \<rightleftharpoons> atom xa) \<bullet> sa = sa") |
274 apply(subgoal_tac "(atom x \<rightleftharpoons> atom xa) \<bullet> ya = ya") |
274 apply(subgoal_tac "(atom x \<rightleftharpoons> atom xa) \<bullet> ya = ya") |
275 apply(simp add: eqvt_at_def) |
275 apply(simp add: eqvt_at_def) |
276 apply(rule perm_supp_eq,simp add: fresh_star_def fresh_Pair supp_swap)+ |
276 apply(simp_all add: swap_fresh_fresh) |
277 done |
277 done |
278 |
278 |
279 termination |
279 termination |
280 by (relation "measure (\<lambda>(t,_,_). size t)") (simp_all add: lam.size) |
280 by (relation "measure (\<lambda>(t,_,_). size t)") (simp_all add: lam.size) |
281 |
281 |