780   "(bs, x1, x2) \<approx>gen (\<lambda>(x1, y1) (x2, y2). R1 x1 x2 \<and> R2 y1 y2) (\<lambda>(a, b). f1 a \<union> f2 b) pi (cs, y1, y2) =

   780   "(bs, x1, x2) \<approx>gen (\<lambda>(x1, y1) (x2, y2). R1 x1 x2 \<and> R2 y1 y2) (\<lambda>(a, b). f1 a \<union> f2 b) pi (cs, y1, y2) =

   781   (f1 x1 \<union> f2 x2 - bs = f1 y1 \<union> f2 y2 - cs \<and> (f1 x1 \<union> f2 x2 - bs) \<sharp>* pi \<and> R1 (pi \<bullet> x1) y1 \<and> R2 (pi \<bullet> x2) y2

   781   (f1 x1 \<union> f2 x2 - bs = f1 y1 \<union> f2 y2 - cs \<and> (f1 x1 \<union> f2 x2 - bs) \<sharp>* pi \<and> R1 (pi \<bullet> x1) y1 \<and> R2 (pi \<bullet> x2) y2

   782   \<and> pi \<bullet> bs = cs)"

   782   \<and> pi \<bullet> bs = cs)"

   783 by (simp add: alpha_gen)

   783 by (simp add: alpha_gen)

   784 

   784 

   785 end

   790 end

   786 

   791