equal
deleted
inserted
replaced
1577 apply(simp add: fresh_star_prod) |
1577 apply(simp add: fresh_star_prod) |
1578 apply(rule fresh_star_supp_conv) |
1578 apply(rule fresh_star_supp_conv) |
1579 apply(auto simp add: fresh_star_def) |
1579 apply(auto simp add: fresh_star_def) |
1580 done |
1580 done |
1581 |
1581 |
|
1582 lemma at_set_avoiding3: |
|
1583 assumes "finite xs" |
|
1584 and "finite (supp c)" "finite (supp x)" |
|
1585 and "xs \<sharp>* x" |
|
1586 shows "\<exists>p. (p \<bullet> xs) \<sharp>* c \<and> x = p \<bullet> x" |
|
1587 using at_set_avoiding2[OF assms] |
|
1588 by (auto simp add: supp_perm_eq) |
|
1589 |
|
1590 |
1582 lemma at_set_avoiding2_atom: |
1591 lemma at_set_avoiding2_atom: |
1583 assumes "finite (supp c)" "finite (supp x)" |
1592 assumes "finite (supp c)" "finite (supp x)" |
1584 and b: "a \<sharp> x" |
1593 and b: "a \<sharp> x" |
1585 shows "\<exists>p. (p \<bullet> a) \<sharp> c \<and> supp x \<sharp>* p" |
1594 shows "\<exists>p. (p \<bullet> a) \<sharp> c \<and> supp x \<sharp>* p" |
1586 proof - |
1595 proof - |