349   "alpha1 (a, x) (b, y) \<longleftrightarrow> (a = b \<and> x = y) \<or> (a \<noteq> b \<and> x = (a \<rightleftharpoons> b) \<bullet> y \<and> a \<sharp> y)"

   349   "alpha1 (a, x) (b, y) \<longleftrightarrow> (a = b \<and> x = y) \<or> (a \<noteq> b \<and> x = (a \<rightleftharpoons> b) \<bullet> y \<and> a \<sharp> y)"

   350 

   350 

   351 notation 

   351 notation 

   352   alpha1 ("_ \<approx>abs1 _")

   352   alpha1 ("_ \<approx>abs1 _")

   353 

   353 

   356 lemma qq:

   354 lemma qq:

   357   fixes S::"atom set"

   355   fixes S::"atom set"

   358   assumes a: "supp p \<inter> S = {}"

   356   assumes a: "supp p \<inter> S = {}"

   359   shows "p \<bullet> S = S"

   357   shows "p \<bullet> S = S"

   360 using a

   358 using a

   500 using a

   498 using a

   501 apply(case_tac "a = b")

   499 apply(case_tac "a = b")

   502 apply(simp)

   500 apply(simp)

   503 oops

   501 oops

   504 

   502 

   505 

   512 

   506 end

   513 end

   507 

   514