equal
deleted
inserted
replaced
1581 |
1581 |
1582 lemma at_set_avoiding3: |
1582 lemma at_set_avoiding3: |
1583 assumes "finite xs" |
1583 assumes "finite xs" |
1584 and "finite (supp c)" "finite (supp x)" |
1584 and "finite (supp c)" "finite (supp x)" |
1585 and "xs \<sharp>* x" |
1585 and "xs \<sharp>* x" |
1586 shows "\<exists>p. (p \<bullet> xs) \<sharp>* c \<and> x = p \<bullet> x" |
1586 shows "\<exists>p. (p \<bullet> xs) \<sharp>* c \<and> supp x \<sharp>* p \<and> supp p \<subseteq> xs \<union> (p \<bullet> xs)" |
1587 using at_set_avoiding2[OF assms] |
1587 using assms |
1588 by (auto simp add: supp_perm_eq) |
1588 apply(erule_tac c="(c, x)" in at_set_avoiding) |
|
1589 apply(simp add: supp_Pair) |
|
1590 apply(rule_tac x="p" in exI) |
|
1591 apply(simp add: fresh_star_prod) |
|
1592 apply(rule fresh_star_supp_conv) |
|
1593 apply(auto simp add: fresh_star_def) |
|
1594 done |
1589 |
1595 |
1590 |
1596 |
1591 lemma at_set_avoiding2_atom: |
1597 lemma at_set_avoiding2_atom: |
1592 assumes "finite (supp c)" "finite (supp x)" |
1598 assumes "finite (supp c)" "finite (supp x)" |
1593 and b: "a \<sharp> x" |
1599 and b: "a \<sharp> x" |