363     using set_renaming_perm2 by blast

   363     using set_renaming_perm2 by blast

   364   from * have "\<forall>b \<in> supp x. p \<bullet> b = p' \<bullet> b" by blast

   364   from * have "\<forall>b \<in> supp x. p \<bullet> b = p' \<bullet> b" by blast

   365   then have a: "p \<bullet> x = p' \<bullet> x" using supp_perm_perm_eq by auto

   365   then have a: "p \<bullet> x = p' \<bullet> x" using supp_perm_perm_eq by auto

   366   from * have "\<forall>b \<in> as. p \<bullet> b = p' \<bullet> b" by blast

   366   from * have "\<forall>b \<in> as. p \<bullet> b = p' \<bullet> b" by blast

   367   then have zb: "p \<bullet> as = p' \<bullet> as" 

   367   then have zb: "p \<bullet> as = p' \<bullet> as" 

   369     apply(rule_tac x="xa" in exI)

   369     apply(rule_tac x="xa" in exI)

   370     apply(simp)

   370     apply(simp)

   371     done

   371     done

   372   have zc: "p' \<bullet> as = as'" using asm by (simp add: alphas)

   372   have zc: "p' \<bullet> as = as'" using asm by (simp add: alphas)

   373   from 0 have 1: "(supp x - as) \<sharp>* p" using *

   373   from 0 have 1: "(supp x - as) \<sharp>* p" using *

   798     then have "Abs_set {a} x = Abs_set {b} y \<longleftrightarrow> (a = b \<and> x = y)" by (simp add: Abs1_eq)

   798     then have "Abs_set {a} x = Abs_set {b} y \<longleftrightarrow> (a = b \<and> x = y)" by (simp add: Abs1_eq)

   799   }

   799   }

   800   moreover

   800   moreover

   801   { assume *: "a \<noteq> b" and **: "Abs_set {a} x = Abs_set {b} y"

   801   { assume *: "a \<noteq> b" and **: "Abs_set {a} x = Abs_set {b} y"

   802     have #: "a \<sharp> Abs_set {b} y" by (simp add: **[symmetric] Abs_fresh_iff)

   802     have #: "a \<sharp> Abs_set {b} y" by (simp add: **[symmetric] Abs_fresh_iff)

   804     also have "\<dots> = Abs_set {b} y"

   804     also have "\<dots> = Abs_set {b} y"

   805       by (rule swap_fresh_fresh) (simp add: #, simp add: Abs_fresh_iff)

   805       by (rule swap_fresh_fresh) (simp add: #, simp add: Abs_fresh_iff)

   806     also have "\<dots> = Abs_set {a} x" using ** by simp

   806     also have "\<dots> = Abs_set {a} x" using ** by simp

   807     finally have "a \<noteq> b \<and> x = (a \<rightleftharpoons> b) \<bullet> y \<and> a \<sharp> y" using # * by (simp add: Abs1_eq Abs_fresh_iff)

   807     finally have "a \<noteq> b \<and> x = (a \<rightleftharpoons> b) \<bullet> y \<and> a \<sharp> y" using # * by (simp add: Abs1_eq Abs_fresh_iff)

   808   }

   808   }

   809   moreover 

   809   moreover 

   810   { assume *: "a \<noteq> b" and **: "x = (a \<rightleftharpoons> b) \<bullet> y \<and> a \<sharp> y"

   810   { assume *: "a \<noteq> b" and **: "x = (a \<rightleftharpoons> b) \<bullet> y \<and> a \<sharp> y"

   811     have "Abs_set {a} x = Abs_set {a} ((a \<rightleftharpoons> b) \<bullet> y)" using ** by simp

   811     have "Abs_set {a} x = Abs_set {a} ((a \<rightleftharpoons> b) \<bullet> y)" using ** by simp

   813     also have "\<dots> = Abs_set {b} y"

   813     also have "\<dots> = Abs_set {b} y"

   814       by (rule swap_fresh_fresh) (simp add: Abs_fresh_iff **, simp add: Abs_fresh_iff)

   814       by (rule swap_fresh_fresh) (simp add: Abs_fresh_iff **, simp add: Abs_fresh_iff)

   815     finally have "Abs_set {a} x = Abs_set {b} y" .

   815     finally have "Abs_set {a} x = Abs_set {b} y" .

   816   }

   816   }

   817   ultimately 

   817   ultimately 

   822     then have "Abs_res {a} x = Abs_res {b} y \<longleftrightarrow> (a = b \<and> x = y)" by (simp add: Abs1_eq)

   822     then have "Abs_res {a} x = Abs_res {b} y \<longleftrightarrow> (a = b \<and> x = y)" by (simp add: Abs1_eq)

   823   }

   823   }

   824   moreover

   824   moreover

   825   { assume *: "a \<noteq> b" and **: "Abs_res {a} x = Abs_res {b} y"

   825   { assume *: "a \<noteq> b" and **: "Abs_res {a} x = Abs_res {b} y"

   826     have #: "a \<sharp> Abs_res {b} y" by (simp add: **[symmetric] Abs_fresh_iff)

   826     have #: "a \<sharp> Abs_res {b} y" by (simp add: **[symmetric] Abs_fresh_iff)

   828     also have "\<dots> = Abs_res {b} y"

   828     also have "\<dots> = Abs_res {b} y"

   829       by (rule swap_fresh_fresh) (simp add: #, simp add: Abs_fresh_iff)

   829       by (rule swap_fresh_fresh) (simp add: #, simp add: Abs_fresh_iff)

   830     also have "\<dots> = Abs_res {a} x" using ** by simp

   830     also have "\<dots> = Abs_res {a} x" using ** by simp

   831     finally have "a \<noteq> b \<and> x = (a \<rightleftharpoons> b) \<bullet> y \<and> a \<sharp> y" using # * by (simp add: Abs1_eq Abs_fresh_iff)

   831     finally have "a \<noteq> b \<and> x = (a \<rightleftharpoons> b) \<bullet> y \<and> a \<sharp> y" using # * by (simp add: Abs1_eq Abs_fresh_iff)

   832   }

   832   }

   833   moreover 

   833   moreover 

   834   { assume *: "a \<noteq> b" and **: "x = (a \<rightleftharpoons> b) \<bullet> y \<and> a \<sharp> y"

   834   { assume *: "a \<noteq> b" and **: "x = (a \<rightleftharpoons> b) \<bullet> y \<and> a \<sharp> y"

   835     have "Abs_res {a} x = Abs_res {a} ((a \<rightleftharpoons> b) \<bullet> y)" using ** by simp

   835     have "Abs_res {a} x = Abs_res {a} ((a \<rightleftharpoons> b) \<bullet> y)" using ** by simp

   837     also have "\<dots> = Abs_res {b} y"

   837     also have "\<dots> = Abs_res {b} y"

   838       by (rule swap_fresh_fresh) (simp add: Abs_fresh_iff **, simp add: Abs_fresh_iff)

   838       by (rule swap_fresh_fresh) (simp add: Abs_fresh_iff **, simp add: Abs_fresh_iff)

   839     finally have "Abs_res {a} x = Abs_res {b} y" .

   839     finally have "Abs_res {a} x = Abs_res {b} y" .

   840   }

   840   }

   841   ultimately 

   841   ultimately