[STATEMENT]
lemma ignore_Inl_Inter:
  "\<lbrakk> S \<noteq> {}; \<Inter>S \<noteq> {} \<rbrakk> \<Longrightarrow> (\<Inter>A\<in>S. {(x, y). ignore_Inl x y} `` {x. Basic_BNFs.setl x \<union> Basic_BNFs.setr x \<subseteq> A}) \<subseteq> {(x, y). ignore_Inl x y} `` (\<Inter>A\<in>S. {x. Basic_BNFs.setl x \<union> Basic_BNFs.setr x \<subseteq> A})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>S \<noteq> {}; \<Inter> S \<noteq> {}\<rbrakk> \<Longrightarrow> (\<Inter>A\<in>S. {(x, y). ignore_Inl x y} `` {x. Basic_BNFs.setl x \<union> Basic_BNFs.setr x \<subseteq> A}) \<subseteq> {(x, y). ignore_Inl x y} `` (\<Inter>A\<in>S. {x. Basic_BNFs.setl x \<union> Basic_BNFs.setr x \<subseteq> A})
[PROOF STEP]
apply(clarsimp; safe; clarsimp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xa xb. \<lbrakk>\<forall>xa\<in>S. \<exists>xb. Basic_BNFs.setl xb \<subseteq> xa \<and> Basic_BNFs.setr xb \<subseteq> xa \<and> ignore_Inl xb x; \<forall>xa\<in>\<Inter>x\<in>S. {xa. Basic_BNFs.setl xa \<subseteq> x \<and> Basic_BNFs.setr xa \<subseteq> x}. \<not> ignore_Inl xa x; xa \<in> S; \<forall>x\<in>S. xb \<in> x\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
subgoal for x A x'
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>xa\<in>S. \<exists>xb. Basic_BNFs.setl xb \<subseteq> xa \<and> Basic_BNFs.setr xb \<subseteq> xa \<and> ignore_Inl xb x; \<forall>xa\<in>\<Inter>x\<in>S. {xa. Basic_BNFs.setl xa \<subseteq> x \<and> Basic_BNFs.setr xa \<subseteq> x}. \<not> ignore_Inl xa x; A \<in> S; \<forall>x\<in>S. x' \<in> x\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply(cases x)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a. \<lbrakk>\<forall>xa\<in>S. \<exists>xb. Basic_BNFs.setl xb \<subseteq> xa \<and> Basic_BNFs.setr xb \<subseteq> xa \<and> ignore_Inl xb x; \<forall>xa\<in>\<Inter>x\<in>S. {xa. Basic_BNFs.setl xa \<subseteq> x \<and> Basic_BNFs.setr xa \<subseteq> x}. \<not> ignore_Inl xa x; A \<in> S; \<forall>x\<in>S. x' \<in> x; x = Inl a\<rbrakk> \<Longrightarrow> False
 2. \<And>b. \<lbrakk>\<forall>xa\<in>S. \<exists>xb. Basic_BNFs.setl xb \<subseteq> xa \<and> Basic_BNFs.setr xb \<subseteq> xa \<and> ignore_Inl xb x; \<forall>xa\<in>\<Inter>x\<in>S. {xa. Basic_BNFs.setl xa \<subseteq> x \<and> Basic_BNFs.setr xa \<subseteq> x}. \<not> ignore_Inl xa x; A \<in> S; \<forall>x\<in>S. x' \<in> x; x = Inr b\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply(drule bspec[where x="Inl x'"])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>a. \<lbrakk>\<forall>xa\<in>S. \<exists>xb. Basic_BNFs.setl xb \<subseteq> xa \<and> Basic_BNFs.setr xb \<subseteq> xa \<and> ignore_Inl xb x; A \<in> S; \<forall>x\<in>S. x' \<in> x; x = Inl a\<rbrakk> \<Longrightarrow> Inl x' \<in> (\<Inter>x\<in>S. {xa. Basic_BNFs.setl xa \<subseteq> x \<and> Basic_BNFs.setr xa \<subseteq> x})
 2. \<And>a. \<lbrakk>\<forall>xa\<in>S. \<exists>xb. Basic_BNFs.setl xb \<subseteq> xa \<and> Basic_BNFs.setr xb \<subseteq> xa \<and> ignore_Inl xb x; A \<in> S; \<forall>x\<in>S. x' \<in> x; x = Inl a; \<not> ignore_Inl (Inl x') x\<rbrakk> \<Longrightarrow> False
 3. \<And>b. \<lbrakk>\<forall>xa\<in>S. \<exists>xb. Basic_BNFs.setl xb \<subseteq> xa \<and> Basic_BNFs.setr xb \<subseteq> xa \<and> ignore_Inl xb x; \<forall>xa\<in>\<Inter>x\<in>S. {xa. Basic_BNFs.setl xa \<subseteq> x \<and> Basic_BNFs.setr xa \<subseteq> x}. \<not> ignore_Inl xa x; A \<in> S; \<forall>x\<in>S. x' \<in> x; x = Inr b\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a. \<lbrakk>\<forall>xa\<in>S. \<exists>xb. Basic_BNFs.setl xb \<subseteq> xa \<and> Basic_BNFs.setr xb \<subseteq> xa \<and> ignore_Inl xb x; A \<in> S; \<forall>x\<in>S. x' \<in> x; x = Inl a; \<not> ignore_Inl (Inl x') x\<rbrakk> \<Longrightarrow> False
 2. \<And>b. \<lbrakk>\<forall>xa\<in>S. \<exists>xb. Basic_BNFs.setl xb \<subseteq> xa \<and> Basic_BNFs.setr xb \<subseteq> xa \<and> ignore_Inl xb x; \<forall>xa\<in>\<Inter>x\<in>S. {xa. Basic_BNFs.setl xa \<subseteq> x \<and> Basic_BNFs.setr xa \<subseteq> x}. \<not> ignore_Inl xa x; A \<in> S; \<forall>x\<in>S. x' \<in> x; x = Inr b\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>b. \<lbrakk>\<forall>xa\<in>S. \<exists>xb. Basic_BNFs.setl xb \<subseteq> xa \<and> Basic_BNFs.setr xb \<subseteq> xa \<and> ignore_Inl xb x; \<forall>xa\<in>\<Inter>x\<in>S. {xa. Basic_BNFs.setl xa \<subseteq> x \<and> Basic_BNFs.setr xa \<subseteq> x}. \<not> ignore_Inl xa x; A \<in> S; \<forall>x\<in>S. x' \<in> x; x = Inr b\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>b. \<lbrakk>\<forall>x\<in>S. b \<in> x; \<forall>x\<in>\<Inter>x\<in>S. {xa. Basic_BNFs.setl xa \<subseteq> x \<and> Basic_BNFs.setr xa \<subseteq> x}. x \<noteq> Inr b; A \<in> S; \<forall>x\<in>S. x' \<in> x; x = Inr b\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply(drule bspec[where x="Inr _"])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>b. \<lbrakk>\<forall>x\<in>S. b \<in> x; A \<in> S; \<forall>x\<in>S. x' \<in> x; x = Inr b\<rbrakk> \<Longrightarrow> Inr (?uu12 b) \<in> (\<Inter>x\<in>S. {xa. Basic_BNFs.setl xa \<subseteq> x \<and> Basic_BNFs.setr xa \<subseteq> x})
 2. \<And>b. \<lbrakk>\<forall>x\<in>S. b \<in> x; A \<in> S; \<forall>x\<in>S. x' \<in> x; x = Inr b; Inr (?uu12 b) \<noteq> Inr b\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>b. \<lbrakk>\<forall>x\<in>S. b \<in> x; A \<in> S; \<forall>x\<in>S. x' \<in> x; x = Inr b; Inr b \<noteq> Inr b\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done