--- a/Nominal/Abs.thy Thu Apr 01 08:06:01 2010 +0200
+++ b/Nominal/Abs.thy Thu Apr 01 08:48:33 2010 +0200
@@ -444,6 +444,12 @@
\<and> pi \<bullet> bsl = csl)"
by (simp_all add: alphas)
+lemma alphas3:
+ "(bsl, x1, x2, x3) \<approx>lst (\<lambda>(x1, y1, z1) (x2, y2, z2). R1 x1 x2 \<and> R2 y1 y2 \<and> R3 z1 z2) (\<lambda>(a, b, c). f1 a \<union> (f2 b \<union> f3 c)) pi (csl, y1, y2, y3) = (f1 x1 \<union> (f2 x2 \<union> f3 x3) - set bsl = f1 y1 \<union> (f2 y2 \<union> f3 y3) - set csl \<and>
+ (f1 x1 \<union> (f2 x2 \<union> f3 x3) - set bsl) \<sharp>* pi \<and>
+ R1 (pi \<bullet> x1) y1 \<and> R2 (pi \<bullet> x2) y2 \<and> R3 (pi \<bullet> x3) y3 \<and> pi \<bullet> bsl = csl)"
+by (simp add: alphas)
+
lemma alpha_gen_compose_sym:
fixes pi
assumes b: "(aa, t) \<approx>gen (\<lambda>x1 x2. R x1 x2 \<and> R x2 x1) f pi (ab, s)"