[STATEMENT]
lemma coalesce_eq_Err_D [rule_format]:
  "\<lbrakk> semilat(err A, Err.le r, lift2 f) \<rbrakk>
  \<Longrightarrow> \<forall>xs. xs \<in> list n A \<longrightarrow> (\<forall>ys. ys \<in> list n A \<longrightarrow>
      coalesce (xs [\<squnion>\<^bsub>f\<^esub>] ys) = Err \<longrightarrow>
      \<not>(\<exists>zs \<in> list n A. xs [\<sqsubseteq>\<^bsub>r\<^esub>] zs \<and> ys [\<sqsubseteq>\<^bsub>r\<^esub>] zs))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. semilat (err A, Err.le r, lift2 f) \<Longrightarrow> \<forall>xs. xs \<in> list n A \<longrightarrow> (\<forall>ys. ys \<in> list n A \<longrightarrow> coalesce (xs [+f] ys) = Err \<longrightarrow> \<not> (\<exists>zs\<in>list n A. xs [\<sqsubseteq>\<^bsub>r\<^esub>] zs \<and> ys [\<sqsubseteq>\<^bsub>r\<^esub>] zs))
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. semilat (err A, Err.le r, lift2 f) \<Longrightarrow> \<forall>xs. xs \<in> list n A \<longrightarrow> (\<forall>ys. ys \<in> list n A \<longrightarrow> coalesce (xs [+f] ys) = Err \<longrightarrow> \<not> (\<exists>zs\<in>list n A. xs [\<sqsubseteq>\<^bsub>r\<^esub>] zs \<and> ys [\<sqsubseteq>\<^bsub>r\<^esub>] zs))
[PROOF STEP]
apply (induct n)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. semilat (err A, Err.le r, lift2 f) \<Longrightarrow> \<forall>xs. xs \<in> list 0 A \<longrightarrow> (\<forall>ys. ys \<in> list 0 A \<longrightarrow> coalesce (xs [+f] ys) = Err \<longrightarrow> \<not> (\<exists>zs\<in>list 0 A. xs [\<sqsubseteq>\<^bsub>r\<^esub>] zs \<and> ys [\<sqsubseteq>\<^bsub>r\<^esub>] zs))
 2. \<And>n. \<lbrakk>semilat (err A, Err.le r, lift2 f) \<Longrightarrow> \<forall>xs. xs \<in> list n A \<longrightarrow> (\<forall>ys. ys \<in> list n A \<longrightarrow> coalesce (xs [+f] ys) = Err \<longrightarrow> \<not> (\<exists>zs\<in>list n A. xs [\<sqsubseteq>\<^bsub>r\<^esub>] zs \<and> ys [\<sqsubseteq>\<^bsub>r\<^esub>] zs)); semilat (err A, Err.le r, lift2 f)\<rbrakk> \<Longrightarrow> \<forall>xs. xs \<in> list (Suc n) A \<longrightarrow> (\<forall>ys. ys \<in> list (Suc n) A \<longrightarrow> coalesce (xs [+f] ys) = Err \<longrightarrow> \<not> (\<exists>zs\<in>list (Suc n) A. xs [\<sqsubseteq>\<^bsub>r\<^esub>] zs \<and> ys [\<sqsubseteq>\<^bsub>r\<^esub>] zs))
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>semilat (err A, Err.le r, lift2 f) \<Longrightarrow> \<forall>xs. xs \<in> list n A \<longrightarrow> (\<forall>ys. ys \<in> list n A \<longrightarrow> coalesce (xs [+f] ys) = Err \<longrightarrow> \<not> (\<exists>zs\<in>list n A. xs [\<sqsubseteq>\<^bsub>r\<^esub>] zs \<and> ys [\<sqsubseteq>\<^bsub>r\<^esub>] zs)); semilat (err A, Err.le r, lift2 f)\<rbrakk> \<Longrightarrow> \<forall>xs. xs \<in> list (Suc n) A \<longrightarrow> (\<forall>ys. ys \<in> list (Suc n) A \<longrightarrow> coalesce (xs [+f] ys) = Err \<longrightarrow> \<not> (\<exists>zs\<in>list (Suc n) A. xs [\<sqsubseteq>\<^bsub>r\<^esub>] zs \<and> ys [\<sqsubseteq>\<^bsub>r\<^esub>] zs))
[PROOF STEP]
apply clarify
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n xs ys zs. \<lbrakk>semilat (err A, Err.le r, lift2 f) \<Longrightarrow> \<forall>xs. xs \<in> list n A \<longrightarrow> (\<forall>ys. ys \<in> list n A \<longrightarrow> coalesce (xs [+f] ys) = Err \<longrightarrow> \<not> (\<exists>zs\<in>list n A. xs [\<sqsubseteq>\<^bsub>r\<^esub>] zs \<and> ys [\<sqsubseteq>\<^bsub>r\<^esub>] zs)); semilat (err A, Err.le r, lift2 f); xs \<in> list (Suc n) A; ys \<in> list (Suc n) A; coalesce (xs [+f] ys) = Err; zs \<in> list (Suc n) A; xs [\<sqsubseteq>\<^bsub>r\<^esub>] zs; ys [\<sqsubseteq>\<^bsub>r\<^esub>] zs\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (simp add: in_list_Suc_iff)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n xs ys zs. \<lbrakk>\<forall>xs. xs \<in> list n A \<longrightarrow> (\<forall>ys. ys \<in> list n A \<longrightarrow> coalesce (xs [+f] ys) = Err \<longrightarrow> (\<forall>zs\<in>list n A. xs [\<sqsubseteq>\<^bsub>r\<^esub>] zs \<longrightarrow> \<not> ys [\<sqsubseteq>\<^bsub>r\<^esub>] zs)); semilat (err A, Err.le r, lift2 f); \<exists>y\<in>A. \<exists>ys\<in>list n A. xs = y # ys; \<exists>y\<in>A. \<exists>ysa\<in>list n A. ys = y # ysa; coalesce (xs [+f] ys) = Err; \<exists>y\<in>A. \<exists>ys\<in>list n A. zs = y # ys; xs [\<sqsubseteq>\<^bsub>r\<^esub>] zs; ys [\<sqsubseteq>\<^bsub>r\<^esub>] zs\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply clarify
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n xs ys zs y ya yb ysa ysb ysc. \<lbrakk>\<forall>xs. xs \<in> list n A \<longrightarrow> (\<forall>ys. ys \<in> list n A \<longrightarrow> coalesce (xs [+f] ys) = Err \<longrightarrow> (\<forall>zs\<in>list n A. xs [\<sqsubseteq>\<^bsub>r\<^esub>] zs \<longrightarrow> \<not> ys [\<sqsubseteq>\<^bsub>r\<^esub>] zs)); semilat (err A, Err.le r, lift2 f); coalesce (y # ysa [+f] (ya # ysb)) = Err; y \<in> A; ya \<in> A; yb \<in> A; ysa \<in> list n A; ysb \<in> list n A; ysc \<in> list n A; y \<sqsubseteq>\<^bsub>r\<^esub> yb; ysa [\<sqsubseteq>\<^bsub>r\<^esub>] ysc; ya \<sqsubseteq>\<^bsub>r\<^esub> yb; ysb [\<sqsubseteq>\<^bsub>r\<^esub>] ysc\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (simp split: err.split_asm add: lem Err.sup_def lift2_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n y ya yb ysa ysb ysc. \<lbrakk>y \<in> A; ya \<in> A; yb \<in> A; ysa \<in> list n A; ysb \<in> list n A; ysc \<in> list n A; y \<sqsubseteq>\<^bsub>r\<^esub> yb; ysa [\<sqsubseteq>\<^bsub>r\<^esub>] ysc; ya \<sqsubseteq>\<^bsub>r\<^esub> yb; ysb [\<sqsubseteq>\<^bsub>r\<^esub>] ysc; \<forall>xs. xs \<in> list n A \<longrightarrow> (\<forall>ys. ys \<in> list n A \<longrightarrow> coalesce (xs [+f] ys) = Err \<longrightarrow> (\<forall>zs\<in>list n A. xs [\<sqsubseteq>\<^bsub>r\<^esub>] zs \<longrightarrow> \<not> ys [\<sqsubseteq>\<^bsub>r\<^esub>] zs)); semilat (err A, Err.le r, lift2 f); y \<squnion>\<^bsub>f\<^esub> ya = Err\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (blast dest: lift2_eq_ErrD)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma closed_err_lift2_conv:
  "closed (err A) (lift2 f) = (\<forall>x\<in>A. \<forall>y\<in>A. x \<squnion>\<^sub>f y \<in> err A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. closed (err A) (lift2 f) = (\<forall>x\<in>A. \<forall>y\<in>A. x \<squnion>\<^bsub>f\<^esub> y \<in> err A)
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. closed (err A) (lift2 f) = (\<forall>x\<in>A. \<forall>y\<in>A. x \<squnion>\<^bsub>f\<^esub> y \<in> err A)
[PROOF STEP]
apply (unfold closed_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>x\<in>err A. \<forall>y\<in>err A. x \<squnion>\<^bsub>lift2 f\<^esub> y \<in> err A) = (\<forall>x\<in>A. \<forall>y\<in>A. x \<squnion>\<^bsub>f\<^esub> y \<in> err A)
[PROOF STEP]
apply (simp add: err_def')
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma closed_map2_list [rule_format]:
  "closed (err A) (lift2 f) \<Longrightarrow>
  \<forall>xs. xs \<in> list n A \<longrightarrow> (\<forall>ys. ys \<in> list n A \<longrightarrow>
  map2 f xs ys \<in> list n (err A))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. closed (err A) (lift2 f) \<Longrightarrow> \<forall>xs. xs \<in> list n A \<longrightarrow> (\<forall>ys. ys \<in> list n A \<longrightarrow> map2 f xs ys \<in> list n (err A))
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. closed (err A) (lift2 f) \<Longrightarrow> \<forall>xs. xs \<in> list n A \<longrightarrow> (\<forall>ys. ys \<in> list n A \<longrightarrow> map2 f xs ys \<in> list n (err A))
[PROOF STEP]
apply (induct n)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. closed (err A) (lift2 f) \<Longrightarrow> \<forall>xs. xs \<in> list 0 A \<longrightarrow> (\<forall>ys. ys \<in> list 0 A \<longrightarrow> map2 f xs ys \<in> list 0 (err A))
 2. \<And>n. \<lbrakk>closed (err A) (lift2 f) \<Longrightarrow> \<forall>xs. xs \<in> list n A \<longrightarrow> (\<forall>ys. ys \<in> list n A \<longrightarrow> map2 f xs ys \<in> list n (err A)); closed (err A) (lift2 f)\<rbrakk> \<Longrightarrow> \<forall>xs. xs \<in> list (Suc n) A \<longrightarrow> (\<forall>ys. ys \<in> list (Suc n) A \<longrightarrow> map2 f xs ys \<in> list (Suc n) (err A))
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>closed (err A) (lift2 f) \<Longrightarrow> \<forall>xs. xs \<in> list n A \<longrightarrow> (\<forall>ys. ys \<in> list n A \<longrightarrow> map2 f xs ys \<in> list n (err A)); closed (err A) (lift2 f)\<rbrakk> \<Longrightarrow> \<forall>xs. xs \<in> list (Suc n) A \<longrightarrow> (\<forall>ys. ys \<in> list (Suc n) A \<longrightarrow> map2 f xs ys \<in> list (Suc n) (err A))
[PROOF STEP]
apply clarify
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n xs ys. \<lbrakk>closed (err A) (lift2 f) \<Longrightarrow> \<forall>xs. xs \<in> list n A \<longrightarrow> (\<forall>ys. ys \<in> list n A \<longrightarrow> map2 f xs ys \<in> list n (err A)); closed (err A) (lift2 f); xs \<in> list (Suc n) A; ys \<in> list (Suc n) A\<rbrakk> \<Longrightarrow> map2 f xs ys \<in> list (Suc n) (err A)
[PROOF STEP]
apply (simp add: in_list_Suc_iff)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n xs ys. \<lbrakk>\<forall>xs. xs \<in> list n A \<longrightarrow> (\<forall>ys. ys \<in> list n A \<longrightarrow> map2 f xs ys \<in> list n (err A)); closed (err A) (lift2 f); \<exists>y\<in>A. \<exists>ys\<in>list n A. xs = y # ys; \<exists>y\<in>A. \<exists>ysa\<in>list n A. ys = y # ysa\<rbrakk> \<Longrightarrow> \<exists>y\<in>err A. \<exists>ysa\<in>list n (err A). map2 f xs ys = y # ysa
[PROOF STEP]
apply clarify
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n xs ys y ya ysa ysb. \<lbrakk>\<forall>xs. xs \<in> list n A \<longrightarrow> (\<forall>ys. ys \<in> list n A \<longrightarrow> map2 f xs ys \<in> list n (err A)); closed (err A) (lift2 f); y \<in> A; ya \<in> A; ysa \<in> list n A; ysb \<in> list n A\<rbrakk> \<Longrightarrow> \<exists>yb\<in>err A. \<exists>ys\<in>list n (err A). map2 f (y # ysa) (ya # ysb) = yb # ys
[PROOF STEP]
apply (simp add: plussub_def closed_err_lift2_conv)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma closed_lift2_sup:
  "closed (err A) (lift2 f) \<Longrightarrow>
  closed (err (list n A)) (lift2 (sup f))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. closed (err A) (lift2 f) \<Longrightarrow> closed (err (list n A)) (lift2 (Listn.sup f))
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. closed (err A) (lift2 f) \<Longrightarrow> closed (err (list n A)) (lift2 (Listn.sup f))
[PROOF STEP]
by (fastforce  simp add: closed_def plussub_def sup_def lift2_def
                          coalesce_in_err_list closed_map2_list
                split: err.split)


[STATEMENT]
lemma err_semilat_sup:
  "err_semilat (A,r,f) \<Longrightarrow>
  err_semilat (list n A, Listn.le r, sup f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. err_semilat (A, r, f) \<Longrightarrow> err_semilat (list n A, Listn.le r, Listn.sup f)
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. err_semilat (A, r, f) \<Longrightarrow> err_semilat (list n A, Listn.le r, Listn.sup f)
[PROOF STEP]
apply (unfold Err.sl_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. semilat (case (A, r, f) of (A, r, f) \<Rightarrow> (err A, Err.le r, lift2 f)) \<Longrightarrow> semilat (case (list n A, Listn.le r, Listn.sup f) of (A, r, f) \<Rightarrow> (err A, Err.le r, lift2 f))
[PROOF STEP]
apply (simp only: split_conv)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. semilat (err A, Err.le r, lift2 f) \<Longrightarrow> semilat (err (list n A), Err.le (Listn.le r), lift2 (Listn.sup f))
[PROOF STEP]
apply (simp (no_asm) only: semilat_Def plussub_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. semilat (err A, Err.le r, lift2 f) \<Longrightarrow> order (Err.le (Listn.le r)) \<and> closed (err (list n A)) (lift2 (Listn.sup f)) \<and> (\<forall>x\<in>err (list n A). \<forall>y\<in>err (list n A). x \<sqsubseteq>\<^bsub>Err.le (Listn.le r)\<^esub> lift2 (Listn.sup f) x y) \<and> (\<forall>x\<in>err (list n A). \<forall>y\<in>err (list n A). y \<sqsubseteq>\<^bsub>Err.le (Listn.le r)\<^esub> lift2 (Listn.sup f) x y) \<and> (\<forall>x\<in>err (list n A). \<forall>y\<in>err (list n A). \<forall>z\<in>err (list n A). x \<sqsubseteq>\<^bsub>Err.le (Listn.le r)\<^esub> z \<and> y \<sqsubseteq>\<^bsub>Err.le (Listn.le r)\<^esub> z \<longrightarrow> lift2 (Listn.sup f) x y \<sqsubseteq>\<^bsub>Err.le (Listn.le r)\<^esub> z)
[PROOF STEP]
apply (simp (no_asm_simp) only: Semilat.closedI [OF Semilat.intro] closed_lift2_sup)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. semilat (err A, Err.le r, lift2 f) \<Longrightarrow> order (Err.le (Listn.le r)) \<and> True \<and> (\<forall>x\<in>err (list n A). \<forall>y\<in>err (list n A). x \<sqsubseteq>\<^bsub>Err.le (Listn.le r)\<^esub> lift2 (Listn.sup f) x y) \<and> (\<forall>x\<in>err (list n A). \<forall>y\<in>err (list n A). y \<sqsubseteq>\<^bsub>Err.le (Listn.le r)\<^esub> lift2 (Listn.sup f) x y) \<and> (\<forall>x\<in>err (list n A). \<forall>y\<in>err (list n A). \<forall>z\<in>err (list n A). x \<sqsubseteq>\<^bsub>Err.le (Listn.le r)\<^esub> z \<and> y \<sqsubseteq>\<^bsub>Err.le (Listn.le r)\<^esub> z \<longrightarrow> lift2 (Listn.sup f) x y \<sqsubseteq>\<^bsub>Err.le (Listn.le r)\<^esub> z)
[PROOF STEP]
apply (rule conjI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. semilat (err A, Err.le r, lift2 f) \<Longrightarrow> order (Err.le (Listn.le r))
 2. semilat (err A, Err.le r, lift2 f) \<Longrightarrow> True \<and> (\<forall>x\<in>err (list n A). \<forall>y\<in>err (list n A). x \<sqsubseteq>\<^bsub>Err.le (Listn.le r)\<^esub> lift2 (Listn.sup f) x y) \<and> (\<forall>x\<in>err (list n A). \<forall>y\<in>err (list n A). y \<sqsubseteq>\<^bsub>Err.le (Listn.le r)\<^esub> lift2 (Listn.sup f) x y) \<and> (\<forall>x\<in>err (list n A). \<forall>y\<in>err (list n A). \<forall>z\<in>err (list n A). x \<sqsubseteq>\<^bsub>Err.le (Listn.le r)\<^esub> z \<and> y \<sqsubseteq>\<^bsub>Err.le (Listn.le r)\<^esub> z \<longrightarrow> lift2 (Listn.sup f) x y \<sqsubseteq>\<^bsub>Err.le (Listn.le r)\<^esub> z)
[PROOF STEP]
apply (drule Semilat.orderI [OF Semilat.intro])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. order (Err.le r) \<Longrightarrow> order (Err.le (Listn.le r))
 2. semilat (err A, Err.le r, lift2 f) \<Longrightarrow> True \<and> (\<forall>x\<in>err (list n A). \<forall>y\<in>err (list n A). x \<sqsubseteq>\<^bsub>Err.le (Listn.le r)\<^esub> lift2 (Listn.sup f) x y) \<and> (\<forall>x\<in>err (list n A). \<forall>y\<in>err (list n A). y \<sqsubseteq>\<^bsub>Err.le (Listn.le r)\<^esub> lift2 (Listn.sup f) x y) \<and> (\<forall>x\<in>err (list n A). \<forall>y\<in>err (list n A). \<forall>z\<in>err (list n A). x \<sqsubseteq>\<^bsub>Err.le (Listn.le r)\<^esub> z \<and> y \<sqsubseteq>\<^bsub>Err.le (Listn.le r)\<^esub> z \<longrightarrow> lift2 (Listn.sup f) x y \<sqsubseteq>\<^bsub>Err.le (Listn.le r)\<^esub> z)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. semilat (err A, Err.le r, lift2 f) \<Longrightarrow> True \<and> (\<forall>x\<in>err (list n A). \<forall>y\<in>err (list n A). x \<sqsubseteq>\<^bsub>Err.le (Listn.le r)\<^esub> lift2 (Listn.sup f) x y) \<and> (\<forall>x\<in>err (list n A). \<forall>y\<in>err (list n A). y \<sqsubseteq>\<^bsub>Err.le (Listn.le r)\<^esub> lift2 (Listn.sup f) x y) \<and> (\<forall>x\<in>err (list n A). \<forall>y\<in>err (list n A). \<forall>z\<in>err (list n A). x \<sqsubseteq>\<^bsub>Err.le (Listn.le r)\<^esub> z \<and> y \<sqsubseteq>\<^bsub>Err.le (Listn.le r)\<^esub> z \<longrightarrow> lift2 (Listn.sup f) x y \<sqsubseteq>\<^bsub>Err.le (Listn.le r)\<^esub> z)
[PROOF STEP]
apply (simp (no_asm) only: unfold_lesub_err Err.le_def err_def' sup_def lift2_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. semilat (err A, Err.le r, lift2 f) \<Longrightarrow> True \<and> (\<forall>x\<in>insert Err {x. \<exists>y\<in>list n A. x = OK y}. \<forall>y\<in>insert Err {x. \<exists>y\<in>list n A. x = OK y}. case case x of Err \<Rightarrow> Err | OK x \<Rightarrow> case y of Err \<Rightarrow> Err | OK y \<Rightarrow> if length x = length y then coalesce (x [+f] y) else Err of Err \<Rightarrow> True | OK y \<Rightarrow> case x of Err \<Rightarrow> False | OK x \<Rightarrow> x [\<sqsubseteq>\<^bsub>r\<^esub>] y) \<and> (\<forall>x\<in>insert Err {x. \<exists>y\<in>list n A. x = OK y}. \<forall>y\<in>insert Err {x. \<exists>y\<in>list n A. x = OK y}. case case x of Err \<Rightarrow> Err | OK x \<Rightarrow> case y of Err \<Rightarrow> Err | OK y \<Rightarrow> if length x = length y then coalesce (x [+f] y) else Err of Err \<Rightarrow> True | OK ya \<Rightarrow> case y of Err \<Rightarrow> False | OK x \<Rightarrow> x [\<sqsubseteq>\<^bsub>r\<^esub>] ya) \<and> (\<forall>x\<in>insert Err {x. \<exists>y\<in>list n A. x = OK y}. \<forall>y\<in>insert Err {x. \<exists>y\<in>list n A. x = OK y}. \<forall>z\<in>insert Err {x. \<exists>y\<in>list n A. x = OK y}. (case z of Err \<Rightarrow> True | OK y \<Rightarrow> case x of Err \<Rightarrow> False | OK x \<Rightarrow> x [\<sqsubseteq>\<^bsub>r\<^esub>] y) \<and> (case z of Err \<Rightarrow> True | OK ya \<Rightarrow> case y of Err \<Rightarrow> False | OK x \<Rightarrow> x [\<sqsubseteq>\<^bsub>r\<^esub>] ya) \<longrightarrow> (case z of Err \<Rightarrow> True | OK ya \<Rightarrow> case case x of Err \<Rightarrow> Err | OK x \<Rightarrow> case y of Err \<Rightarrow> Err | OK y \<Rightarrow> if length x = length y then coalesce (x [+f] y) else Err of Err \<Rightarrow> False | OK x \<Rightarrow> x [\<sqsubseteq>\<^bsub>r\<^esub>] ya))
[PROOF STEP]
apply (simp (no_asm_simp) add: coalesce_eq_OK1_D coalesce_eq_OK2_D split: err.split)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. semilat (err A, Err.le r, lift2 f) \<Longrightarrow> \<forall>y\<in>list n A. \<forall>ya\<in>list n A. \<forall>yb\<in>list n A. (coalesce (y [+f] ya) = Err \<longrightarrow> y [\<sqsubseteq>\<^bsub>r\<^esub>] yb \<longrightarrow> \<not> ya [\<sqsubseteq>\<^bsub>r\<^esub>] yb) \<and> (\<forall>x2. coalesce (y [+f] ya) = OK x2 \<longrightarrow> y [\<sqsubseteq>\<^bsub>r\<^esub>] yb \<and> ya [\<sqsubseteq>\<^bsub>r\<^esub>] yb \<longrightarrow> x2 [\<sqsubseteq>\<^bsub>r\<^esub>] yb)
[PROOF STEP]
apply (blast intro: coalesce_eq_OK_ub_D dest: coalesce_eq_Err_D)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma err_semilat_upto_esl:
  "\<And>L. err_semilat L \<Longrightarrow> err_semilat(upto_esl m L)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>L. err_semilat L \<Longrightarrow> err_semilat (upto_esl m L)
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>L. err_semilat L \<Longrightarrow> err_semilat (upto_esl m L)
[PROOF STEP]
apply (unfold Listn.upto_esl_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>L. err_semilat L \<Longrightarrow> err_semilat (case L of (A, r, f) \<Rightarrow> (\<Union> {list n A |n. n \<le> m}, Listn.le r, Listn.sup f))
[PROOF STEP]
apply (simp (no_asm_simp) only: split_tupled_all)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a aa b. err_semilat (a, aa, b) \<Longrightarrow> err_semilat (case (a, aa, b) of (A, r, f) \<Rightarrow> (\<Union> {list n A |n. n \<le> m}, Listn.le r, Listn.sup f))
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a aa b. err_semilat (a, aa, b) \<Longrightarrow> err_semilat (\<Union> {list n a |n. n \<le> m}, Listn.le aa, Listn.sup b)
[PROOF STEP]
apply (fastforce intro!: err_semilat_UnionI err_semilat_sup
                dest: lesub_list_impl_same_size
                simp add: plussub_def Listn.sup_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma cnf_of_encode_interfering_operator_pair_exclusion_is_i[simp]:
  "cnf (encode_interfering_operator_pair_exclusion \<Pi> k op\<^sub>1 op\<^sub>2) = {{
    (Operator k (index (strips_problem.operators_of \<Pi>) op\<^sub>1))\<inverse>
      , (Operator k (index (strips_problem.operators_of \<Pi>) op\<^sub>2))\<inverse> }}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cnf (encode_interfering_operator_pair_exclusion \<Pi> k op\<^sub>1 op\<^sub>2) = {{(Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>1))\<inverse>, (Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>2))\<inverse>}}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. cnf (encode_interfering_operator_pair_exclusion \<Pi> k op\<^sub>1 op\<^sub>2) = {{(Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>1))\<inverse>, (Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>2))\<inverse>}}
[PROOF STEP]
let ?ops = "strips_problem.operators_of \<Pi>"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. cnf (encode_interfering_operator_pair_exclusion \<Pi> k op\<^sub>1 op\<^sub>2) = {{(Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>1))\<inverse>, (Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>2))\<inverse>}}
[PROOF STEP]
have "cnf (encode_interfering_operator_pair_exclusion \<Pi> k op\<^sub>1 op\<^sub>2)
    = cnf (\<^bold>\<not>(Atom (Operator k (index ?ops op\<^sub>1))) \<^bold>\<or> \<^bold>\<not>(Atom (Operator k (index ?ops op\<^sub>2))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cnf (encode_interfering_operator_pair_exclusion \<Pi> k op\<^sub>1 op\<^sub>2) = cnf (\<^bold>\<not> (Atom (Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>1))) \<^bold>\<or> \<^bold>\<not> (Atom (Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>2))))
[PROOF STEP]
unfolding encode_interfering_operator_pair_exclusion_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cnf (let ops = \<Pi>\<^sub>\<O> in \<^bold>\<not> (Atom (Operator k (index ops op\<^sub>1))) \<^bold>\<or> \<^bold>\<not> (Atom (Operator k (index ops op\<^sub>2)))) = cnf (\<^bold>\<not> (Atom (Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>1))) \<^bold>\<or> \<^bold>\<not> (Atom (Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>2))))
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
cnf (encode_interfering_operator_pair_exclusion \<Pi> k op\<^sub>1 op\<^sub>2) = cnf (\<^bold>\<not> (Atom (Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>1))) \<^bold>\<or> \<^bold>\<not> (Atom (Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>2))))

goal (1 subgoal):
 1. cnf (encode_interfering_operator_pair_exclusion \<Pi> k op\<^sub>1 op\<^sub>2) = {{(Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>1))\<inverse>, (Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>2))\<inverse>}}
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
cnf (encode_interfering_operator_pair_exclusion \<Pi> k op\<^sub>1 op\<^sub>2) = cnf (\<^bold>\<not> (Atom (Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>1))) \<^bold>\<or> \<^bold>\<not> (Atom (Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>2))))

goal (1 subgoal):
 1. cnf (encode_interfering_operator_pair_exclusion \<Pi> k op\<^sub>1 op\<^sub>2) = {{(Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>1))\<inverse>, (Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>2))\<inverse>}}
[PROOF STEP]
have "\<dots> = { C \<union> D | C D.
    C \<in> cnf (\<^bold>\<not>(Atom (Operator k (index ?ops op\<^sub>1))))
    \<and> D \<in> cnf (\<^bold>\<not>(Atom (Operator k (index ?ops op\<^sub>2)))) }"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cnf (\<^bold>\<not> (Atom (Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>1))) \<^bold>\<or> \<^bold>\<not> (Atom (Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>2)))) = {C \<union> D |C D. C \<in> cnf (\<^bold>\<not> (Atom (Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>1)))) \<and> D \<in> cnf (\<^bold>\<not> (Atom (Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>2))))}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
cnf (\<^bold>\<not> (Atom (Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>1))) \<^bold>\<or> \<^bold>\<not> (Atom (Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>2)))) = {C \<union> D |C D. C \<in> cnf (\<^bold>\<not> (Atom (Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>1)))) \<and> D \<in> cnf (\<^bold>\<not> (Atom (Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>2))))}

goal (1 subgoal):
 1. cnf (encode_interfering_operator_pair_exclusion \<Pi> k op\<^sub>1 op\<^sub>2) = {{(Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>1))\<inverse>, (Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>2))\<inverse>}}
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
cnf (encode_interfering_operator_pair_exclusion \<Pi> k op\<^sub>1 op\<^sub>2) = {C \<union> D |C D. C \<in> cnf (\<^bold>\<not> (Atom (Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>1)))) \<and> D \<in> cnf (\<^bold>\<not> (Atom (Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>2))))}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
cnf (encode_interfering_operator_pair_exclusion \<Pi> k op\<^sub>1 op\<^sub>2) = {C \<union> D |C D. C \<in> cnf (\<^bold>\<not> (Atom (Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>1)))) \<and> D \<in> cnf (\<^bold>\<not> (Atom (Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>2))))}

goal (1 subgoal):
 1. cnf (encode_interfering_operator_pair_exclusion \<Pi> k op\<^sub>1 op\<^sub>2) = {{(Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>1))\<inverse>, (Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>2))\<inverse>}}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
cnf (encode_interfering_operator_pair_exclusion \<Pi> k op\<^sub>1 op\<^sub>2) = {{(Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>1))\<inverse>, (Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>2))\<inverse>}}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma cnf_of_encode_interfering_operator_exclusion_is_ii[simp]:
  "set [encode_interfering_operator_pair_exclusion \<Pi> k op\<^sub>1 op\<^sub>2.
      (op\<^sub>1, op\<^sub>2) \<leftarrow> filter (\<lambda>(op\<^sub>1, op\<^sub>2).
          index (strips_problem.operators_of \<Pi>) op\<^sub>1 \<noteq> index (strips_problem.operators_of \<Pi>) op\<^sub>2
          \<and> are_operators_interfering op\<^sub>1 op\<^sub>2)
        (List.product (strips_problem.operators_of \<Pi>) (strips_problem.operators_of \<Pi>))
        , k \<leftarrow> [0..<t]]
    = (\<Union>(op\<^sub>1, op\<^sub>2)
        \<in> { (op\<^sub>1, op\<^sub>2) \<in> set (operators_of \<Pi>) \<times> set (operators_of \<Pi>).
          index (strips_problem.operators_of \<Pi>) op\<^sub>1 \<noteq> index (strips_problem.operators_of \<Pi>) op\<^sub>2
          \<and> are_operators_interfering op\<^sub>1 op\<^sub>2 }.
      (\<lambda>k. encode_interfering_operator_pair_exclusion \<Pi> k op\<^sub>1 op\<^sub>2) ` {0..<t})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (concat (map (\<lambda>(op\<^sub>1, op\<^sub>2). map (\<lambda>k. encode_interfering_operator_pair_exclusion \<Pi> k op\<^sub>1 op\<^sub>2) [0..<t]) (filter (\<lambda>(op\<^sub>1, op\<^sub>2). index (\<Pi>\<^sub>\<O>) op\<^sub>1 \<noteq> index (\<Pi>\<^sub>\<O>) op\<^sub>2 \<and> are_operators_interfering op\<^sub>1 op\<^sub>2) (List.product (\<Pi>\<^sub>\<O>) (\<Pi>\<^sub>\<O>))))) = (\<Union>(op\<^sub>1, op\<^sub>2)\<in>{(op\<^sub>1, op\<^sub>2). (op\<^sub>1, op\<^sub>2) \<in> set (\<Pi>\<^sub>\<O>) \<times> set (\<Pi>\<^sub>\<O>) \<and> index (\<Pi>\<^sub>\<O>) op\<^sub>1 \<noteq> index (\<Pi>\<^sub>\<O>) op\<^sub>2 \<and> are_operators_interfering op\<^sub>1 op\<^sub>2}. (\<lambda>k. encode_interfering_operator_pair_exclusion \<Pi> k op\<^sub>1 op\<^sub>2) ` {0..<t})
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. set (concat (map (\<lambda>(op\<^sub>1, op\<^sub>2). map (\<lambda>k. encode_interfering_operator_pair_exclusion \<Pi> k op\<^sub>1 op\<^sub>2) [0..<t]) (filter (\<lambda>(op\<^sub>1, op\<^sub>2). index (\<Pi>\<^sub>\<O>) op\<^sub>1 \<noteq> index (\<Pi>\<^sub>\<O>) op\<^sub>2 \<and> are_operators_interfering op\<^sub>1 op\<^sub>2) (List.product (\<Pi>\<^sub>\<O>) (\<Pi>\<^sub>\<O>))))) = (\<Union>(op\<^sub>1, op\<^sub>2)\<in>{(op\<^sub>1, op\<^sub>2). (op\<^sub>1, op\<^sub>2) \<in> set (\<Pi>\<^sub>\<O>) \<times> set (\<Pi>\<^sub>\<O>) \<and> index (\<Pi>\<^sub>\<O>) op\<^sub>1 \<noteq> index (\<Pi>\<^sub>\<O>) op\<^sub>2 \<and> are_operators_interfering op\<^sub>1 op\<^sub>2}. (\<lambda>k. encode_interfering_operator_pair_exclusion \<Pi> k op\<^sub>1 op\<^sub>2) ` {0..<t})
[PROOF STEP]
let ?ops = "strips_problem.operators_of \<Pi>"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. set (concat (map (\<lambda>(op\<^sub>1, op\<^sub>2). map (\<lambda>k. encode_interfering_operator_pair_exclusion \<Pi> k op\<^sub>1 op\<^sub>2) [0..<t]) (filter (\<lambda>(op\<^sub>1, op\<^sub>2). index (\<Pi>\<^sub>\<O>) op\<^sub>1 \<noteq> index (\<Pi>\<^sub>\<O>) op\<^sub>2 \<and> are_operators_interfering op\<^sub>1 op\<^sub>2) (List.product (\<Pi>\<^sub>\<O>) (\<Pi>\<^sub>\<O>))))) = (\<Union>(op\<^sub>1, op\<^sub>2)\<in>{(op\<^sub>1, op\<^sub>2). (op\<^sub>1, op\<^sub>2) \<in> set (\<Pi>\<^sub>\<O>) \<times> set (\<Pi>\<^sub>\<O>) \<and> index (\<Pi>\<^sub>\<O>) op\<^sub>1 \<noteq> index (\<Pi>\<^sub>\<O>) op\<^sub>2 \<and> are_operators_interfering op\<^sub>1 op\<^sub>2}. (\<lambda>k. encode_interfering_operator_pair_exclusion \<Pi> k op\<^sub>1 op\<^sub>2) ` {0..<t})
[PROOF STEP]
let ?interfering = "filter (\<lambda>(op\<^sub>1, op\<^sub>2). index ?ops op\<^sub>1 \<noteq> index ?ops op\<^sub>2
    \<and> are_operators_interfering op\<^sub>1 op\<^sub>2) (List.product ?ops ?ops)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. set (concat (map (\<lambda>(op\<^sub>1, op\<^sub>2). map (\<lambda>k. encode_interfering_operator_pair_exclusion \<Pi> k op\<^sub>1 op\<^sub>2) [0..<t]) (filter (\<lambda>(op\<^sub>1, op\<^sub>2). index (\<Pi>\<^sub>\<O>) op\<^sub>1 \<noteq> index (\<Pi>\<^sub>\<O>) op\<^sub>2 \<and> are_operators_interfering op\<^sub>1 op\<^sub>2) (List.product (\<Pi>\<^sub>\<O>) (\<Pi>\<^sub>\<O>))))) = (\<Union>(op\<^sub>1, op\<^sub>2)\<in>{(op\<^sub>1, op\<^sub>2). (op\<^sub>1, op\<^sub>2) \<in> set (\<Pi>\<^sub>\<O>) \<times> set (\<Pi>\<^sub>\<O>) \<and> index (\<Pi>\<^sub>\<O>) op\<^sub>1 \<noteq> index (\<Pi>\<^sub>\<O>) op\<^sub>2 \<and> are_operators_interfering op\<^sub>1 op\<^sub>2}. (\<lambda>k. encode_interfering_operator_pair_exclusion \<Pi> k op\<^sub>1 op\<^sub>2) ` {0..<t})
[PROOF STEP]
let ?fs = "[encode_interfering_operator_pair_exclusion \<Pi> k op\<^sub>1 op\<^sub>2.
    (op\<^sub>1, op\<^sub>2) \<leftarrow> ?interfering, k \<leftarrow> [0..<t]]"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. set (concat (map (\<lambda>(op\<^sub>1, op\<^sub>2). map (\<lambda>k. encode_interfering_operator_pair_exclusion \<Pi> k op\<^sub>1 op\<^sub>2) [0..<t]) (filter (\<lambda>(op\<^sub>1, op\<^sub>2). index (\<Pi>\<^sub>\<O>) op\<^sub>1 \<noteq> index (\<Pi>\<^sub>\<O>) op\<^sub>2 \<and> are_operators_interfering op\<^sub>1 op\<^sub>2) (List.product (\<Pi>\<^sub>\<O>) (\<Pi>\<^sub>\<O>))))) = (\<Union>(op\<^sub>1, op\<^sub>2)\<in>{(op\<^sub>1, op\<^sub>2). (op\<^sub>1, op\<^sub>2) \<in> set (\<Pi>\<^sub>\<O>) \<times> set (\<Pi>\<^sub>\<O>) \<and> index (\<Pi>\<^sub>\<O>) op\<^sub>1 \<noteq> index (\<Pi>\<^sub>\<O>) op\<^sub>2 \<and> are_operators_interfering op\<^sub>1 op\<^sub>2}. (\<lambda>k. encode_interfering_operator_pair_exclusion \<Pi> k op\<^sub>1 op\<^sub>2) ` {0..<t})
[PROOF STEP]
have "set ?fs = \<Union>(set
    ` (\<lambda>(op\<^sub>1, op\<^sub>2). map (\<lambda>k. encode_interfering_operator_pair_exclusion \<Pi> k op\<^sub>1 op\<^sub>2) [0..<t])
    ` (set (filter (\<lambda>(op\<^sub>1, op\<^sub>2). index ?ops op\<^sub>1 \<noteq> index ?ops op\<^sub>2 \<and> are_operators_interfering op\<^sub>1 op\<^sub>2)
      (List.product ?ops ?ops))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (concat (map (\<lambda>(op\<^sub>1, op\<^sub>2). map (\<lambda>k. encode_interfering_operator_pair_exclusion \<Pi> k op\<^sub>1 op\<^sub>2) [0..<t]) (filter (\<lambda>(op\<^sub>1, op\<^sub>2). index (\<Pi>\<^sub>\<O>) op\<^sub>1 \<noteq> index (\<Pi>\<^sub>\<O>) op\<^sub>2 \<and> are_operators_interfering op\<^sub>1 op\<^sub>2) (List.product (\<Pi>\<^sub>\<O>) (\<Pi>\<^sub>\<O>))))) = \<Union> (set ` (\<lambda>(op\<^sub>1, op\<^sub>2). map (\<lambda>k. encode_interfering_operator_pair_exclusion \<Pi> k op\<^sub>1 op\<^sub>2) [0..<t]) ` set (filter (\<lambda>(op\<^sub>1, op\<^sub>2). index (\<Pi>\<^sub>\<O>) op\<^sub>1 \<noteq> index (\<Pi>\<^sub>\<O>) op\<^sub>2 \<and> are_operators_interfering op\<^sub>1 op\<^sub>2) (List.product (\<Pi>\<^sub>\<O>) (\<Pi>\<^sub>\<O>))))
[PROOF STEP]
unfolding set_concat set_map
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Union> (set ` (\<lambda>(op\<^sub>1, op\<^sub>2). map (\<lambda>k. encode_interfering_operator_pair_exclusion \<Pi> k op\<^sub>1 op\<^sub>2) [0..<t]) ` set (filter (\<lambda>(op\<^sub>1, op\<^sub>2). index (\<Pi>\<^sub>\<O>) op\<^sub>1 \<noteq> index (\<Pi>\<^sub>\<O>) op\<^sub>2 \<and> are_operators_interfering op\<^sub>1 op\<^sub>2) (List.product (\<Pi>\<^sub>\<O>) (\<Pi>\<^sub>\<O>)))) = \<Union> (set ` (\<lambda>(op\<^sub>1, op\<^sub>2). map (\<lambda>k. encode_interfering_operator_pair_exclusion \<Pi> k op\<^sub>1 op\<^sub>2) [0..<t]) ` set (filter (\<lambda>(op\<^sub>1, op\<^sub>2). index (\<Pi>\<^sub>\<O>) op\<^sub>1 \<noteq> index (\<Pi>\<^sub>\<O>) op\<^sub>2 \<and> are_operators_interfering op\<^sub>1 op\<^sub>2) (List.product (\<Pi>\<^sub>\<O>) (\<Pi>\<^sub>\<O>))))
[PROOF STEP]
by blast
  \<comment> \<open> TODO slow. \<close>
[PROOF STATE]
proof (state)
this:
set (concat (map (\<lambda>(op\<^sub>1, op\<^sub>2). map (\<lambda>k. encode_interfering_operator_pair_exclusion \<Pi> k op\<^sub>1 op\<^sub>2) [0..<t]) (filter (\<lambda>(op\<^sub>1, op\<^sub>2). index (\<Pi>\<^sub>\<O>) op\<^sub>1 \<noteq> index (\<Pi>\<^sub>\<O>) op\<^sub>2 \<and> are_operators_interfering op\<^sub>1 op\<^sub>2) (List.product (\<Pi>\<^sub>\<O>) (\<Pi>\<^sub>\<O>))))) = \<Union> (set ` (\<lambda>(op\<^sub>1, op\<^sub>2). map (\<lambda>k. encode_interfering_operator_pair_exclusion \<Pi> k op\<^sub>1 op\<^sub>2) [0..<t]) ` set (filter (\<lambda>(op\<^sub>1, op\<^sub>2). index (\<Pi>\<^sub>\<O>) op\<^sub>1 \<noteq> index (\<Pi>\<^sub>\<O>) op\<^sub>2 \<and> are_operators_interfering op\<^sub>1 op\<^sub>2) (List.product (\<Pi>\<^sub>\<O>) (\<Pi>\<^sub>\<O>))))

goal (1 subgoal):
 1. set (concat (map (\<lambda>(op\<^sub>1, op\<^sub>2). map (\<lambda>k. encode_interfering_operator_pair_exclusion \<Pi> k op\<^sub>1 op\<^sub>2) [0..<t]) (filter (\<lambda>(op\<^sub>1, op\<^sub>2). index (\<Pi>\<^sub>\<O>) op\<^sub>1 \<noteq> index (\<Pi>\<^sub>\<O>) op\<^sub>2 \<and> are_operators_interfering op\<^sub>1 op\<^sub>2) (List.product (\<Pi>\<^sub>\<O>) (\<Pi>\<^sub>\<O>))))) = (\<Union>(op\<^sub>1, op\<^sub>2)\<in>{(op\<^sub>1, op\<^sub>2). (op\<^sub>1, op\<^sub>2) \<in> set (\<Pi>\<^sub>\<O>) \<times> set (\<Pi>\<^sub>\<O>) \<and> index (\<Pi>\<^sub>\<O>) op\<^sub>1 \<noteq> index (\<Pi>\<^sub>\<O>) op\<^sub>2 \<and> are_operators_interfering op\<^sub>1 op\<^sub>2}. (\<lambda>k. encode_interfering_operator_pair_exclusion \<Pi> k op\<^sub>1 op\<^sub>2) ` {0..<t})
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
set (concat (map (\<lambda>(op\<^sub>1, op\<^sub>2). map (\<lambda>k. encode_interfering_operator_pair_exclusion \<Pi> k op\<^sub>1 op\<^sub>2) [0..<t]) (filter (\<lambda>(op\<^sub>1, op\<^sub>2). index (\<Pi>\<^sub>\<O>) op\<^sub>1 \<noteq> index (\<Pi>\<^sub>\<O>) op\<^sub>2 \<and> are_operators_interfering op\<^sub>1 op\<^sub>2) (List.product (\<Pi>\<^sub>\<O>) (\<Pi>\<^sub>\<O>))))) = \<Union> (set ` (\<lambda>(op\<^sub>1, op\<^sub>2). map (\<lambda>k. encode_interfering_operator_pair_exclusion \<Pi> k op\<^sub>1 op\<^sub>2) [0..<t]) ` set (filter (\<lambda>(op\<^sub>1, op\<^sub>2). index (\<Pi>\<^sub>\<O>) op\<^sub>1 \<noteq> index (\<Pi>\<^sub>\<O>) op\<^sub>2 \<and> are_operators_interfering op\<^sub>1 op\<^sub>2) (List.product (\<Pi>\<^sub>\<O>) (\<Pi>\<^sub>\<O>))))

goal (1 subgoal):
 1. set (concat (map (\<lambda>(op\<^sub>1, op\<^sub>2). map (\<lambda>k. encode_interfering_operator_pair_exclusion \<Pi> k op\<^sub>1 op\<^sub>2) [0..<t]) (filter (\<lambda>(op\<^sub>1, op\<^sub>2). index (\<Pi>\<^sub>\<O>) op\<^sub>1 \<noteq> index (\<Pi>\<^sub>\<O>) op\<^sub>2 \<and> are_operators_interfering op\<^sub>1 op\<^sub>2) (List.product (\<Pi>\<^sub>\<O>) (\<Pi>\<^sub>\<O>))))) = (\<Union>(op\<^sub>1, op\<^sub>2)\<in>{(op\<^sub>1, op\<^sub>2). (op\<^sub>1, op\<^sub>2) \<in> set (\<Pi>\<^sub>\<O>) \<times> set (\<Pi>\<^sub>\<O>) \<and> index (\<Pi>\<^sub>\<O>) op\<^sub>1 \<noteq> index (\<Pi>\<^sub>\<O>) op\<^sub>2 \<and> are_operators_interfering op\<^sub>1 op\<^sub>2}. (\<lambda>k. encode_interfering_operator_pair_exclusion \<Pi> k op\<^sub>1 op\<^sub>2) ` {0..<t})
[PROOF STEP]
have "\<dots> = \<Union>((\<lambda>(op\<^sub>1, op\<^sub>2).
      set (map (\<lambda>k. encode_interfering_operator_pair_exclusion \<Pi> k op\<^sub>1 op\<^sub>2) [0..<t]))
    ` (set (filter (\<lambda>(op\<^sub>1, op\<^sub>2). index ?ops op\<^sub>1 \<noteq> index ?ops op\<^sub>2 \<and> are_operators_interfering op\<^sub>1 op\<^sub>2)
      (List.product ?ops ?ops))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Union> (set ` (\<lambda>(op\<^sub>1, op\<^sub>2). map (\<lambda>k. encode_interfering_operator_pair_exclusion \<Pi> k op\<^sub>1 op\<^sub>2) [0..<t]) ` set (filter (\<lambda>(op\<^sub>1, op\<^sub>2). index (\<Pi>\<^sub>\<O>) op\<^sub>1 \<noteq> index (\<Pi>\<^sub>\<O>) op\<^sub>2 \<and> are_operators_interfering op\<^sub>1 op\<^sub>2) (List.product (\<Pi>\<^sub>\<O>) (\<Pi>\<^sub>\<O>)))) = (\<Union>(op\<^sub>1, op\<^sub>2)\<in>set (filter (\<lambda>(op\<^sub>1, op\<^sub>2). index (\<Pi>\<^sub>\<O>) op\<^sub>1 \<noteq> index (\<Pi>\<^sub>\<O>) op\<^sub>2 \<and> are_operators_interfering op\<^sub>1 op\<^sub>2) (List.product (\<Pi>\<^sub>\<O>) (\<Pi>\<^sub>\<O>))). set (map (\<lambda>k. encode_interfering_operator_pair_exclusion \<Pi> k op\<^sub>1 op\<^sub>2) [0..<t]))
[PROOF STEP]
unfolding image_comp[of
        set "\<lambda>(op\<^sub>1, op\<^sub>2). map (\<lambda>k. encode_interfering_operator_pair_exclusion \<Pi> k op\<^sub>1 op\<^sub>2) [0..<t]"]
      comp_apply
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Union>x\<in>set (filter (\<lambda>(op\<^sub>1, op\<^sub>2). index (\<Pi>\<^sub>\<O>) op\<^sub>1 \<noteq> index (\<Pi>\<^sub>\<O>) op\<^sub>2 \<and> are_operators_interfering op\<^sub>1 op\<^sub>2) (List.product (\<Pi>\<^sub>\<O>) (\<Pi>\<^sub>\<O>))). set (case x of (op\<^sub>1, op\<^sub>2) \<Rightarrow> map (\<lambda>k. encode_interfering_operator_pair_exclusion \<Pi> k op\<^sub>1 op\<^sub>2) [0..<t])) = (\<Union>(op\<^sub>1, op\<^sub>2)\<in>set (filter (\<lambda>(op\<^sub>1, op\<^sub>2). index (\<Pi>\<^sub>\<O>) op\<^sub>1 \<noteq> index (\<Pi>\<^sub>\<O>) op\<^sub>2 \<and> are_operators_interfering op\<^sub>1 op\<^sub>2) (List.product (\<Pi>\<^sub>\<O>) (\<Pi>\<^sub>\<O>))). set (map (\<lambda>k. encode_interfering_operator_pair_exclusion \<Pi> k op\<^sub>1 op\<^sub>2) [0..<t]))
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
\<Union> (set ` (\<lambda>(op\<^sub>1, op\<^sub>2). map (\<lambda>k. encode_interfering_operator_pair_exclusion \<Pi> k op\<^sub>1 op\<^sub>2) [0..<t]) ` set (filter (\<lambda>(op\<^sub>1, op\<^sub>2). index (\<Pi>\<^sub>\<O>) op\<^sub>1 \<noteq> index (\<Pi>\<^sub>\<O>) op\<^sub>2 \<and> are_operators_interfering op\<^sub>1 op\<^sub>2) (List.product (\<Pi>\<^sub>\<O>) (\<Pi>\<^sub>\<O>)))) = (\<Union>(op\<^sub>1, op\<^sub>2)\<in>set (filter (\<lambda>(op\<^sub>1, op\<^sub>2). index (\<Pi>\<^sub>\<O>) op\<^sub>1 \<noteq> index (\<Pi>\<^sub>\<O>) op\<^sub>2 \<and> are_operators_interfering op\<^sub>1 op\<^sub>2) (List.product (\<Pi>\<^sub>\<O>) (\<Pi>\<^sub>\<O>))). set (map (\<lambda>k. encode_interfering_operator_pair_exclusion \<Pi> k op\<^sub>1 op\<^sub>2) [0..<t]))

goal (1 subgoal):
 1. set (concat (map (\<lambda>(op\<^sub>1, op\<^sub>2). map (\<lambda>k. encode_interfering_operator_pair_exclusion \<Pi> k op\<^sub>1 op\<^sub>2) [0..<t]) (filter (\<lambda>(op\<^sub>1, op\<^sub>2). index (\<Pi>\<^sub>\<O>) op\<^sub>1 \<noteq> index (\<Pi>\<^sub>\<O>) op\<^sub>2 \<and> are_operators_interfering op\<^sub>1 op\<^sub>2) (List.product (\<Pi>\<^sub>\<O>) (\<Pi>\<^sub>\<O>))))) = (\<Union>(op\<^sub>1, op\<^sub>2)\<in>{(op\<^sub>1, op\<^sub>2). (op\<^sub>1, op\<^sub>2) \<in> set (\<Pi>\<^sub>\<O>) \<times> set (\<Pi>\<^sub>\<O>) \<and> index (\<Pi>\<^sub>\<O>) op\<^sub>1 \<noteq> index (\<Pi>\<^sub>\<O>) op\<^sub>2 \<and> are_operators_interfering op\<^sub>1 op\<^sub>2}. (\<lambda>k. encode_interfering_operator_pair_exclusion \<Pi> k op\<^sub>1 op\<^sub>2) ` {0..<t})
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<Union> (set ` (\<lambda>(op\<^sub>1, op\<^sub>2). map (\<lambda>k. encode_interfering_operator_pair_exclusion \<Pi> k op\<^sub>1 op\<^sub>2) [0..<t]) ` set (filter (\<lambda>(op\<^sub>1, op\<^sub>2). index (\<Pi>\<^sub>\<O>) op\<^sub>1 \<noteq> index (\<Pi>\<^sub>\<O>) op\<^sub>2 \<and> are_operators_interfering op\<^sub>1 op\<^sub>2) (List.product (\<Pi>\<^sub>\<O>) (\<Pi>\<^sub>\<O>)))) = (\<Union>(op\<^sub>1, op\<^sub>2)\<in>set (filter (\<lambda>(op\<^sub>1, op\<^sub>2). index (\<Pi>\<^sub>\<O>) op\<^sub>1 \<noteq> index (\<Pi>\<^sub>\<O>) op\<^sub>2 \<and> are_operators_interfering op\<^sub>1 op\<^sub>2) (List.product (\<Pi>\<^sub>\<O>) (\<Pi>\<^sub>\<O>))). set (map (\<lambda>k. encode_interfering_operator_pair_exclusion \<Pi> k op\<^sub>1 op\<^sub>2) [0..<t]))

goal (1 subgoal):
 1. set (concat (map (\<lambda>(op\<^sub>1, op\<^sub>2). map (\<lambda>k. encode_interfering_operator_pair_exclusion \<Pi> k op\<^sub>1 op\<^sub>2) [0..<t]) (filter (\<lambda>(op\<^sub>1, op\<^sub>2). index (\<Pi>\<^sub>\<O>) op\<^sub>1 \<noteq> index (\<Pi>\<^sub>\<O>) op\<^sub>2 \<and> are_operators_interfering op\<^sub>1 op\<^sub>2) (List.product (\<Pi>\<^sub>\<O>) (\<Pi>\<^sub>\<O>))))) = (\<Union>(op\<^sub>1, op\<^sub>2)\<in>{(op\<^sub>1, op\<^sub>2). (op\<^sub>1, op\<^sub>2) \<in> set (\<Pi>\<^sub>\<O>) \<times> set (\<Pi>\<^sub>\<O>) \<and> index (\<Pi>\<^sub>\<O>) op\<^sub>1 \<noteq> index (\<Pi>\<^sub>\<O>) op\<^sub>2 \<and> are_operators_interfering op\<^sub>1 op\<^sub>2}. (\<lambda>k. encode_interfering_operator_pair_exclusion \<Pi> k op\<^sub>1 op\<^sub>2) ` {0..<t})
[PROOF STEP]
have "\<dots> = \<Union>((\<lambda>(op\<^sub>1, op\<^sub>2).
      (\<lambda>k. encode_interfering_operator_pair_exclusion \<Pi> k op\<^sub>1 op\<^sub>2) ` {0..<t})
    ` (set (filter (\<lambda>(op\<^sub>1, op\<^sub>2). index ?ops op\<^sub>1 \<noteq> index ?ops op\<^sub>2 \<and> are_operators_interfering op\<^sub>1 op\<^sub>2)
      (List.product ?ops ?ops))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Union>(op\<^sub>1, op\<^sub>2)\<in>set (filter (\<lambda>(op\<^sub>1, op\<^sub>2). index (\<Pi>\<^sub>\<O>) op\<^sub>1 \<noteq> index (\<Pi>\<^sub>\<O>) op\<^sub>2 \<and> are_operators_interfering op\<^sub>1 op\<^sub>2) (List.product (\<Pi>\<^sub>\<O>) (\<Pi>\<^sub>\<O>))). set (map (\<lambda>k. encode_interfering_operator_pair_exclusion \<Pi> k op\<^sub>1 op\<^sub>2) [0..<t])) = (\<Union>(op\<^sub>1, op\<^sub>2)\<in>set (filter (\<lambda>(op\<^sub>1, op\<^sub>2). index (\<Pi>\<^sub>\<O>) op\<^sub>1 \<noteq> index (\<Pi>\<^sub>\<O>) op\<^sub>2 \<and> are_operators_interfering op\<^sub>1 op\<^sub>2) (List.product (\<Pi>\<^sub>\<O>) (\<Pi>\<^sub>\<O>))). (\<lambda>k. encode_interfering_operator_pair_exclusion \<Pi> k op\<^sub>1 op\<^sub>2) ` {0..<t})
[PROOF STEP]
unfolding set_map[of _ "[0..<t]"] atLeastLessThan_upt[of 0 t]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Union>(op\<^sub>1, op\<^sub>2)\<in>set (filter (\<lambda>(op\<^sub>1, op\<^sub>2). index (\<Pi>\<^sub>\<O>) op\<^sub>1 \<noteq> index (\<Pi>\<^sub>\<O>) op\<^sub>2 \<and> are_operators_interfering op\<^sub>1 op\<^sub>2) (List.product (\<Pi>\<^sub>\<O>) (\<Pi>\<^sub>\<O>))). (\<lambda>k. encode_interfering_operator_pair_exclusion \<Pi> k op\<^sub>1 op\<^sub>2) ` set [0..<t]) = (\<Union>(op\<^sub>1, op\<^sub>2)\<in>set (filter (\<lambda>(op\<^sub>1, op\<^sub>2). index (\<Pi>\<^sub>\<O>) op\<^sub>1 \<noteq> index (\<Pi>\<^sub>\<O>) op\<^sub>2 \<and> are_operators_interfering op\<^sub>1 op\<^sub>2) (List.product (\<Pi>\<^sub>\<O>) (\<Pi>\<^sub>\<O>))). (\<lambda>k. encode_interfering_operator_pair_exclusion \<Pi> k op\<^sub>1 op\<^sub>2) ` set [0..<t])
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(\<Union>(op\<^sub>1, op\<^sub>2)\<in>set (filter (\<lambda>(op\<^sub>1, op\<^sub>2). index (\<Pi>\<^sub>\<O>) op\<^sub>1 \<noteq> index (\<Pi>\<^sub>\<O>) op\<^sub>2 \<and> are_operators_interfering op\<^sub>1 op\<^sub>2) (List.product (\<Pi>\<^sub>\<O>) (\<Pi>\<^sub>\<O>))). set (map (\<lambda>k. encode_interfering_operator_pair_exclusion \<Pi> k op\<^sub>1 op\<^sub>2) [0..<t])) = (\<Union>(op\<^sub>1, op\<^sub>2)\<in>set (filter (\<lambda>(op\<^sub>1, op\<^sub>2). index (\<Pi>\<^sub>\<O>) op\<^sub>1 \<noteq> index (\<Pi>\<^sub>\<O>) op\<^sub>2 \<and> are_operators_interfering op\<^sub>1 op\<^sub>2) (List.product (\<Pi>\<^sub>\<O>) (\<Pi>\<^sub>\<O>))). (\<lambda>k. encode_interfering_operator_pair_exclusion \<Pi> k op\<^sub>1 op\<^sub>2) ` {0..<t})

goal (1 subgoal):
 1. set (concat (map (\<lambda>(op\<^sub>1, op\<^sub>2). map (\<lambda>k. encode_interfering_operator_pair_exclusion \<Pi> k op\<^sub>1 op\<^sub>2) [0..<t]) (filter (\<lambda>(op\<^sub>1, op\<^sub>2). index (\<Pi>\<^sub>\<O>) op\<^sub>1 \<noteq> index (\<Pi>\<^sub>\<O>) op\<^sub>2 \<and> are_operators_interfering op\<^sub>1 op\<^sub>2) (List.product (\<Pi>\<^sub>\<O>) (\<Pi>\<^sub>\<O>))))) = (\<Union>(op\<^sub>1, op\<^sub>2)\<in>{(op\<^sub>1, op\<^sub>2). (op\<^sub>1, op\<^sub>2) \<in> set (\<Pi>\<^sub>\<O>) \<times> set (\<Pi>\<^sub>\<O>) \<and> index (\<Pi>\<^sub>\<O>) op\<^sub>1 \<noteq> index (\<Pi>\<^sub>\<O>) op\<^sub>2 \<and> are_operators_interfering op\<^sub>1 op\<^sub>2}. (\<lambda>k. encode_interfering_operator_pair_exclusion \<Pi> k op\<^sub>1 op\<^sub>2) ` {0..<t})
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Union>(op\<^sub>1, op\<^sub>2)\<in>set (filter (\<lambda>(op\<^sub>1, op\<^sub>2). index (\<Pi>\<^sub>\<O>) op\<^sub>1 \<noteq> index (\<Pi>\<^sub>\<O>) op\<^sub>2 \<and> are_operators_interfering op\<^sub>1 op\<^sub>2) (List.product (\<Pi>\<^sub>\<O>) (\<Pi>\<^sub>\<O>))). set (map (\<lambda>k. encode_interfering_operator_pair_exclusion \<Pi> k op\<^sub>1 op\<^sub>2) [0..<t])) = (\<Union>(op\<^sub>1, op\<^sub>2)\<in>set (filter (\<lambda>(op\<^sub>1, op\<^sub>2). index (\<Pi>\<^sub>\<O>) op\<^sub>1 \<noteq> index (\<Pi>\<^sub>\<O>) op\<^sub>2 \<and> are_operators_interfering op\<^sub>1 op\<^sub>2) (List.product (\<Pi>\<^sub>\<O>) (\<Pi>\<^sub>\<O>))). (\<lambda>k. encode_interfering_operator_pair_exclusion \<Pi> k op\<^sub>1 op\<^sub>2) ` {0..<t})

goal (1 subgoal):
 1. set (concat (map (\<lambda>(op\<^sub>1, op\<^sub>2). map (\<lambda>k. encode_interfering_operator_pair_exclusion \<Pi> k op\<^sub>1 op\<^sub>2) [0..<t]) (filter (\<lambda>(op\<^sub>1, op\<^sub>2). index (\<Pi>\<^sub>\<O>) op\<^sub>1 \<noteq> index (\<Pi>\<^sub>\<O>) op\<^sub>2 \<and> are_operators_interfering op\<^sub>1 op\<^sub>2) (List.product (\<Pi>\<^sub>\<O>) (\<Pi>\<^sub>\<O>))))) = (\<Union>(op\<^sub>1, op\<^sub>2)\<in>{(op\<^sub>1, op\<^sub>2). (op\<^sub>1, op\<^sub>2) \<in> set (\<Pi>\<^sub>\<O>) \<times> set (\<Pi>\<^sub>\<O>) \<and> index (\<Pi>\<^sub>\<O>) op\<^sub>1 \<noteq> index (\<Pi>\<^sub>\<O>) op\<^sub>2 \<and> are_operators_interfering op\<^sub>1 op\<^sub>2}. (\<lambda>k. encode_interfering_operator_pair_exclusion \<Pi> k op\<^sub>1 op\<^sub>2) ` {0..<t})
[PROOF STEP]
have "\<dots> = \<Union>((\<lambda>(op\<^sub>1, op\<^sub>2).
      (\<lambda>k. encode_interfering_operator_pair_exclusion \<Pi> k op\<^sub>1 op\<^sub>2) ` {0..<t})
    ` (Set.filter (\<lambda>(op\<^sub>1, op\<^sub>2). index ?ops op\<^sub>1 \<noteq> index ?ops op\<^sub>2 \<and> are_operators_interfering op\<^sub>1 op\<^sub>2)
      (set (List.product ?ops ?ops))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Union>(op\<^sub>1, op\<^sub>2)\<in>set (filter (\<lambda>(op\<^sub>1, op\<^sub>2). index (\<Pi>\<^sub>\<O>) op\<^sub>1 \<noteq> index (\<Pi>\<^sub>\<O>) op\<^sub>2 \<and> are_operators_interfering op\<^sub>1 op\<^sub>2) (List.product (\<Pi>\<^sub>\<O>) (\<Pi>\<^sub>\<O>))). (\<lambda>k. encode_interfering_operator_pair_exclusion \<Pi> k op\<^sub>1 op\<^sub>2) ` {0..<t}) = (\<Union>(op\<^sub>1, op\<^sub>2)\<in>Set.filter (\<lambda>(op\<^sub>1, op\<^sub>2). index (\<Pi>\<^sub>\<O>) op\<^sub>1 \<noteq> index (\<Pi>\<^sub>\<O>) op\<^sub>2 \<and> are_operators_interfering op\<^sub>1 op\<^sub>2) (set (List.product (\<Pi>\<^sub>\<O>) (\<Pi>\<^sub>\<O>))). (\<lambda>k. encode_interfering_operator_pair_exclusion \<Pi> k op\<^sub>1 op\<^sub>2) ` {0..<t})
[PROOF STEP]
unfolding set_filter[of "\<lambda>(op\<^sub>1, op\<^sub>2). are_operators_interfering op\<^sub>1 op\<^sub>2" "List.product ?ops ?ops"]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Union>(op\<^sub>1, op\<^sub>2)\<in>set (filter (\<lambda>(op\<^sub>1, op\<^sub>2). index (\<Pi>\<^sub>\<O>) op\<^sub>1 \<noteq> index (\<Pi>\<^sub>\<O>) op\<^sub>2 \<and> are_operators_interfering op\<^sub>1 op\<^sub>2) (List.product (\<Pi>\<^sub>\<O>) (\<Pi>\<^sub>\<O>))). (\<lambda>k. encode_interfering_operator_pair_exclusion \<Pi> k op\<^sub>1 op\<^sub>2) ` {0..<t}) = (\<Union>(op\<^sub>1, op\<^sub>2)\<in>Set.filter (\<lambda>(op\<^sub>1, op\<^sub>2). index (\<Pi>\<^sub>\<O>) op\<^sub>1 \<noteq> index (\<Pi>\<^sub>\<O>) op\<^sub>2 \<and> are_operators_interfering op\<^sub>1 op\<^sub>2) (set (List.product (\<Pi>\<^sub>\<O>) (\<Pi>\<^sub>\<O>))). (\<lambda>k. encode_interfering_operator_pair_exclusion \<Pi> k op\<^sub>1 op\<^sub>2) ` {0..<t})
[PROOF STEP]
by force
  \<comment> \<open> TODO slow.\<close>
[PROOF STATE]
proof (state)
this:
(\<Union>(op\<^sub>1, op\<^sub>2)\<in>set (filter (\<lambda>(op\<^sub>1, op\<^sub>2). index (\<Pi>\<^sub>\<O>) op\<^sub>1 \<noteq> index (\<Pi>\<^sub>\<O>) op\<^sub>2 \<and> are_operators_interfering op\<^sub>1 op\<^sub>2) (List.product (\<Pi>\<^sub>\<O>) (\<Pi>\<^sub>\<O>))). (\<lambda>k. encode_interfering_operator_pair_exclusion \<Pi> k op\<^sub>1 op\<^sub>2) ` {0..<t}) = (\<Union>(op\<^sub>1, op\<^sub>2)\<in>Set.filter (\<lambda>(op\<^sub>1, op\<^sub>2). index (\<Pi>\<^sub>\<O>) op\<^sub>1 \<noteq> index (\<Pi>\<^sub>\<O>) op\<^sub>2 \<and> are_operators_interfering op\<^sub>1 op\<^sub>2) (set (List.product (\<Pi>\<^sub>\<O>) (\<Pi>\<^sub>\<O>))). (\<lambda>k. encode_interfering_operator_pair_exclusion \<Pi> k op\<^sub>1 op\<^sub>2) ` {0..<t})

goal (1 subgoal):
 1. set (concat (map (\<lambda>(op\<^sub>1, op\<^sub>2). map (\<lambda>k. encode_interfering_operator_pair_exclusion \<Pi> k op\<^sub>1 op\<^sub>2) [0..<t]) (filter (\<lambda>(op\<^sub>1, op\<^sub>2). index (\<Pi>\<^sub>\<O>) op\<^sub>1 \<noteq> index (\<Pi>\<^sub>\<O>) op\<^sub>2 \<and> are_operators_interfering op\<^sub>1 op\<^sub>2) (List.product (\<Pi>\<^sub>\<O>) (\<Pi>\<^sub>\<O>))))) = (\<Union>(op\<^sub>1, op\<^sub>2)\<in>{(op\<^sub>1, op\<^sub>2). (op\<^sub>1, op\<^sub>2) \<in> set (\<Pi>\<^sub>\<O>) \<times> set (\<Pi>\<^sub>\<O>) \<and> index (\<Pi>\<^sub>\<O>) op\<^sub>1 \<noteq> index (\<Pi>\<^sub>\<O>) op\<^sub>2 \<and> are_operators_interfering op\<^sub>1 op\<^sub>2}. (\<lambda>k. encode_interfering_operator_pair_exclusion \<Pi> k op\<^sub>1 op\<^sub>2) ` {0..<t})
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
set (concat (map (\<lambda>(op\<^sub>1, op\<^sub>2). map (\<lambda>k. encode_interfering_operator_pair_exclusion \<Pi> k op\<^sub>1 op\<^sub>2) [0..<t]) (filter (\<lambda>(op\<^sub>1, op\<^sub>2). index (\<Pi>\<^sub>\<O>) op\<^sub>1 \<noteq> index (\<Pi>\<^sub>\<O>) op\<^sub>2 \<and> are_operators_interfering op\<^sub>1 op\<^sub>2) (List.product (\<Pi>\<^sub>\<O>) (\<Pi>\<^sub>\<O>))))) = (\<Union>(op\<^sub>1, op\<^sub>2)\<in>Set.filter (\<lambda>(op\<^sub>1, op\<^sub>2). index (\<Pi>\<^sub>\<O>) op\<^sub>1 \<noteq> index (\<Pi>\<^sub>\<O>) op\<^sub>2 \<and> are_operators_interfering op\<^sub>1 op\<^sub>2) (set (List.product (\<Pi>\<^sub>\<O>) (\<Pi>\<^sub>\<O>))). (\<lambda>k. encode_interfering_operator_pair_exclusion \<Pi> k op\<^sub>1 op\<^sub>2) ` {0..<t})
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
set (concat (map (\<lambda>(op\<^sub>1, op\<^sub>2). map (\<lambda>k. encode_interfering_operator_pair_exclusion \<Pi> k op\<^sub>1 op\<^sub>2) [0..<t]) (filter (\<lambda>(op\<^sub>1, op\<^sub>2). index (\<Pi>\<^sub>\<O>) op\<^sub>1 \<noteq> index (\<Pi>\<^sub>\<O>) op\<^sub>2 \<and> are_operators_interfering op\<^sub>1 op\<^sub>2) (List.product (\<Pi>\<^sub>\<O>) (\<Pi>\<^sub>\<O>))))) = (\<Union>(op\<^sub>1, op\<^sub>2)\<in>Set.filter (\<lambda>(op\<^sub>1, op\<^sub>2). index (\<Pi>\<^sub>\<O>) op\<^sub>1 \<noteq> index (\<Pi>\<^sub>\<O>) op\<^sub>2 \<and> are_operators_interfering op\<^sub>1 op\<^sub>2) (set (List.product (\<Pi>\<^sub>\<O>) (\<Pi>\<^sub>\<O>))). (\<lambda>k. encode_interfering_operator_pair_exclusion \<Pi> k op\<^sub>1 op\<^sub>2) ` {0..<t})

goal (1 subgoal):
 1. set (concat (map (\<lambda>(op\<^sub>1, op\<^sub>2). map (\<lambda>k. encode_interfering_operator_pair_exclusion \<Pi> k op\<^sub>1 op\<^sub>2) [0..<t]) (filter (\<lambda>(op\<^sub>1, op\<^sub>2). index (\<Pi>\<^sub>\<O>) op\<^sub>1 \<noteq> index (\<Pi>\<^sub>\<O>) op\<^sub>2 \<and> are_operators_interfering op\<^sub>1 op\<^sub>2) (List.product (\<Pi>\<^sub>\<O>) (\<Pi>\<^sub>\<O>))))) = (\<Union>(op\<^sub>1, op\<^sub>2)\<in>{(op\<^sub>1, op\<^sub>2). (op\<^sub>1, op\<^sub>2) \<in> set (\<Pi>\<^sub>\<O>) \<times> set (\<Pi>\<^sub>\<O>) \<and> index (\<Pi>\<^sub>\<O>) op\<^sub>1 \<noteq> index (\<Pi>\<^sub>\<O>) op\<^sub>2 \<and> are_operators_interfering op\<^sub>1 op\<^sub>2}. (\<lambda>k. encode_interfering_operator_pair_exclusion \<Pi> k op\<^sub>1 op\<^sub>2) ` {0..<t})
[PROOF STEP]
unfolding operators_of_def set_product[of ?ops ?ops]
[PROOF STATE]
proof (prove)
using this:
set (concat (map (\<lambda>(op\<^sub>1, op\<^sub>2). map (\<lambda>k. encode_interfering_operator_pair_exclusion \<Pi> k op\<^sub>1 op\<^sub>2) [0..<t]) (filter (\<lambda>(op\<^sub>1, op\<^sub>2). index ((id \<circ> Record.iso_tuple_snd Record.tuple_iso_tuple \<circ> Record.iso_tuple_fst Record.tuple_iso_tuple \<circ> Record.iso_tuple_fst strips_problem_ext_Tuple_Iso) \<Pi>) op\<^sub>1 \<noteq> index ((id \<circ> Record.iso_tuple_snd Record.tuple_iso_tuple \<circ> Record.iso_tuple_fst Record.tuple_iso_tuple \<circ> Record.iso_tuple_fst strips_problem_ext_Tuple_Iso) \<Pi>) op\<^sub>2 \<and> are_operators_interfering op\<^sub>1 op\<^sub>2) (List.product ((id \<circ> Record.iso_tuple_snd Record.tuple_iso_tuple \<circ> Record.iso_tuple_fst Record.tuple_iso_tuple \<circ> Record.iso_tuple_fst strips_problem_ext_Tuple_Iso) \<Pi>) ((id \<circ> Record.iso_tuple_snd Record.tuple_iso_tuple \<circ> Record.iso_tuple_fst Record.tuple_iso_tuple \<circ> Record.iso_tuple_fst strips_problem_ext_Tuple_Iso) \<Pi>))))) = (\<Union>(op\<^sub>1, op\<^sub>2)\<in>Set.filter (\<lambda>(op\<^sub>1, op\<^sub>2). index ((id \<circ> Record.iso_tuple_snd Record.tuple_iso_tuple \<circ> Record.iso_tuple_fst Record.tuple_iso_tuple \<circ> Record.iso_tuple_fst strips_problem_ext_Tuple_Iso) \<Pi>) op\<^sub>1 \<noteq> index ((id \<circ> Record.iso_tuple_snd Record.tuple_iso_tuple \<circ> Record.iso_tuple_fst Record.tuple_iso_tuple \<circ> Record.iso_tuple_fst strips_problem_ext_Tuple_Iso) \<Pi>) op\<^sub>2 \<and> are_operators_interfering op\<^sub>1 op\<^sub>2) (set (List.product ((id \<circ> Record.iso_tuple_snd Record.tuple_iso_tuple \<circ> Record.iso_tuple_fst Record.tuple_iso_tuple \<circ> Record.iso_tuple_fst strips_problem_ext_Tuple_Iso) \<Pi>) ((id \<circ> Record.iso_tuple_snd Record.tuple_iso_tuple \<circ> Record.iso_tuple_fst Record.tuple_iso_tuple \<circ> Record.iso_tuple_fst strips_problem_ext_Tuple_Iso) \<Pi>))). (\<lambda>k. encode_interfering_operator_pair_exclusion \<Pi> k op\<^sub>1 op\<^sub>2) ` {0..<t})

goal (1 subgoal):
 1. set (concat (map (\<lambda>(op\<^sub>1, op\<^sub>2). map (\<lambda>k. encode_interfering_operator_pair_exclusion \<Pi> k op\<^sub>1 op\<^sub>2) [0..<t]) (filter (\<lambda>(op\<^sub>1, op\<^sub>2). index ((id \<circ> Record.iso_tuple_snd Record.tuple_iso_tuple \<circ> Record.iso_tuple_fst Record.tuple_iso_tuple \<circ> Record.iso_tuple_fst strips_problem_ext_Tuple_Iso) \<Pi>) op\<^sub>1 \<noteq> index ((id \<circ> Record.iso_tuple_snd Record.tuple_iso_tuple \<circ> Record.iso_tuple_fst Record.tuple_iso_tuple \<circ> Record.iso_tuple_fst strips_problem_ext_Tuple_Iso) \<Pi>) op\<^sub>2 \<and> are_operators_interfering op\<^sub>1 op\<^sub>2) (List.product ((id \<circ> Record.iso_tuple_snd Record.tuple_iso_tuple \<circ> Record.iso_tuple_fst Record.tuple_iso_tuple \<circ> Record.iso_tuple_fst strips_problem_ext_Tuple_Iso) \<Pi>) ((id \<circ> Record.iso_tuple_snd Record.tuple_iso_tuple \<circ> Record.iso_tuple_fst Record.tuple_iso_tuple \<circ> Record.iso_tuple_fst strips_problem_ext_Tuple_Iso) \<Pi>))))) = (\<Union>(op\<^sub>1, op\<^sub>2)\<in>{(op\<^sub>1, op\<^sub>2). (op\<^sub>1, op\<^sub>2) \<in> set ((id \<circ> Record.iso_tuple_snd Record.tuple_iso_tuple \<circ> Record.iso_tuple_fst Record.tuple_iso_tuple \<circ> Record.iso_tuple_fst strips_problem_ext_Tuple_Iso) \<Pi>) \<times> set ((id \<circ> Record.iso_tuple_snd Record.tuple_iso_tuple \<circ> Record.iso_tuple_fst Record.tuple_iso_tuple \<circ> Record.iso_tuple_fst strips_problem_ext_Tuple_Iso) \<Pi>) \<and> index ((id \<circ> Record.iso_tuple_snd Record.tuple_iso_tuple \<circ> Record.iso_tuple_fst Record.tuple_iso_tuple \<circ> Record.iso_tuple_fst strips_problem_ext_Tuple_Iso) \<Pi>) op\<^sub>1 \<noteq> index ((id \<circ> Record.iso_tuple_snd Record.tuple_iso_tuple \<circ> Record.iso_tuple_fst Record.tuple_iso_tuple \<circ> Record.iso_tuple_fst strips_problem_ext_Tuple_Iso) \<Pi>) op\<^sub>2 \<and> are_operators_interfering op\<^sub>1 op\<^sub>2}. (\<lambda>k. encode_interfering_operator_pair_exclusion \<Pi> k op\<^sub>1 op\<^sub>2) ` {0..<t})
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
set (concat (map (\<lambda>(op\<^sub>1, op\<^sub>2). map (\<lambda>k. encode_interfering_operator_pair_exclusion \<Pi> k op\<^sub>1 op\<^sub>2) [0..<t]) (filter (\<lambda>(op\<^sub>1, op\<^sub>2). index (\<Pi>\<^sub>\<O>) op\<^sub>1 \<noteq> index (\<Pi>\<^sub>\<O>) op\<^sub>2 \<and> are_operators_interfering op\<^sub>1 op\<^sub>2) (List.product (\<Pi>\<^sub>\<O>) (\<Pi>\<^sub>\<O>))))) = (\<Union>(op\<^sub>1, op\<^sub>2)\<in>{(op\<^sub>1, op\<^sub>2). (op\<^sub>1, op\<^sub>2) \<in> set (\<Pi>\<^sub>\<O>) \<times> set (\<Pi>\<^sub>\<O>) \<and> index (\<Pi>\<^sub>\<O>) op\<^sub>1 \<noteq> index (\<Pi>\<^sub>\<O>) op\<^sub>2 \<and> are_operators_interfering op\<^sub>1 op\<^sub>2}. (\<lambda>k. encode_interfering_operator_pair_exclusion \<Pi> k op\<^sub>1 op\<^sub>2) ` {0..<t})

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma cnf_of_encode_interfering_operator_exclusion_is_iii[simp]:
  (* TODO why is this necessary? *)
  fixes \<Pi> :: "'variable strips_problem"
  shows "cnf ` set [encode_interfering_operator_pair_exclusion \<Pi> k op\<^sub>1 op\<^sub>2.
      (op\<^sub>1, op\<^sub>2) \<leftarrow> filter (\<lambda>(op\<^sub>1, op\<^sub>2).
          index (strips_problem.operators_of \<Pi>) op\<^sub>1 \<noteq> index (strips_problem.operators_of \<Pi>) op\<^sub>2
          \<and> are_operators_interfering op\<^sub>1 op\<^sub>2)
        (List.product (strips_problem.operators_of \<Pi>) (strips_problem.operators_of \<Pi>))
      , k \<leftarrow> [0..<t]]
    = (\<Union>(op\<^sub>1, op\<^sub>2)
        \<in> { (op\<^sub>1, op\<^sub>2) \<in> set (strips_problem.operators_of \<Pi>) \<times> set (strips_problem.operators_of \<Pi>).
          index (strips_problem.operators_of \<Pi>) op\<^sub>1 \<noteq> index (strips_problem.operators_of \<Pi>) op\<^sub>2
          \<and> are_operators_interfering op\<^sub>1 op\<^sub>2 }.
      {{{ (Operator k (index (strips_problem.operators_of \<Pi>) op\<^sub>1))\<inverse>
        , (Operator k (index (strips_problem.operators_of \<Pi>) op\<^sub>2))\<inverse> }} | k. k \<in> {0..<t}})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cnf ` set (concat (map (\<lambda>(op\<^sub>1, op\<^sub>2). map (\<lambda>k. encode_interfering_operator_pair_exclusion \<Pi> k op\<^sub>1 op\<^sub>2) [0..<t]) (filter (\<lambda>(op\<^sub>1, op\<^sub>2). index (\<Pi>\<^sub>\<O>) op\<^sub>1 \<noteq> index (\<Pi>\<^sub>\<O>) op\<^sub>2 \<and> are_operators_interfering op\<^sub>1 op\<^sub>2) (List.product (\<Pi>\<^sub>\<O>) (\<Pi>\<^sub>\<O>))))) = (\<Union>(op\<^sub>1, op\<^sub>2)\<in>{(op\<^sub>1, op\<^sub>2). (op\<^sub>1, op\<^sub>2) \<in> set (\<Pi>\<^sub>\<O>) \<times> set (\<Pi>\<^sub>\<O>) \<and> index (\<Pi>\<^sub>\<O>) op\<^sub>1 \<noteq> index (\<Pi>\<^sub>\<O>) op\<^sub>2 \<and> are_operators_interfering op\<^sub>1 op\<^sub>2}. {{{(Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>1))\<inverse>, (Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>2))\<inverse>}} |k. k \<in> {0..<t}})
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. cnf ` set (concat (map (\<lambda>(op\<^sub>1, op\<^sub>2). map (\<lambda>k. encode_interfering_operator_pair_exclusion \<Pi> k op\<^sub>1 op\<^sub>2) [0..<t]) (filter (\<lambda>(op\<^sub>1, op\<^sub>2). index (\<Pi>\<^sub>\<O>) op\<^sub>1 \<noteq> index (\<Pi>\<^sub>\<O>) op\<^sub>2 \<and> are_operators_interfering op\<^sub>1 op\<^sub>2) (List.product (\<Pi>\<^sub>\<O>) (\<Pi>\<^sub>\<O>))))) = (\<Union>(op\<^sub>1, op\<^sub>2)\<in>{(op\<^sub>1, op\<^sub>2). (op\<^sub>1, op\<^sub>2) \<in> set (\<Pi>\<^sub>\<O>) \<times> set (\<Pi>\<^sub>\<O>) \<and> index (\<Pi>\<^sub>\<O>) op\<^sub>1 \<noteq> index (\<Pi>\<^sub>\<O>) op\<^sub>2 \<and> are_operators_interfering op\<^sub>1 op\<^sub>2}. {{{(Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>1))\<inverse>, (Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>2))\<inverse>}} |k. k \<in> {0..<t}})
[PROOF STEP]
let ?ops = "strips_problem.operators_of \<Pi>"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. cnf ` set (concat (map (\<lambda>(op\<^sub>1, op\<^sub>2). map (\<lambda>k. encode_interfering_operator_pair_exclusion \<Pi> k op\<^sub>1 op\<^sub>2) [0..<t]) (filter (\<lambda>(op\<^sub>1, op\<^sub>2). index (\<Pi>\<^sub>\<O>) op\<^sub>1 \<noteq> index (\<Pi>\<^sub>\<O>) op\<^sub>2 \<and> are_operators_interfering op\<^sub>1 op\<^sub>2) (List.product (\<Pi>\<^sub>\<O>) (\<Pi>\<^sub>\<O>))))) = (\<Union>(op\<^sub>1, op\<^sub>2)\<in>{(op\<^sub>1, op\<^sub>2). (op\<^sub>1, op\<^sub>2) \<in> set (\<Pi>\<^sub>\<O>) \<times> set (\<Pi>\<^sub>\<O>) \<and> index (\<Pi>\<^sub>\<O>) op\<^sub>1 \<noteq> index (\<Pi>\<^sub>\<O>) op\<^sub>2 \<and> are_operators_interfering op\<^sub>1 op\<^sub>2}. {{{(Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>1))\<inverse>, (Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>2))\<inverse>}} |k. k \<in> {0..<t}})
[PROOF STEP]
let ?interfering = "filter (\<lambda>(op\<^sub>1, op\<^sub>2). index ?ops op\<^sub>1 \<noteq> index ?ops op\<^sub>2
    \<and> are_operators_interfering op\<^sub>1 op\<^sub>2) (List.product ?ops ?ops)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. cnf ` set (concat (map (\<lambda>(op\<^sub>1, op\<^sub>2). map (\<lambda>k. encode_interfering_operator_pair_exclusion \<Pi> k op\<^sub>1 op\<^sub>2) [0..<t]) (filter (\<lambda>(op\<^sub>1, op\<^sub>2). index (\<Pi>\<^sub>\<O>) op\<^sub>1 \<noteq> index (\<Pi>\<^sub>\<O>) op\<^sub>2 \<and> are_operators_interfering op\<^sub>1 op\<^sub>2) (List.product (\<Pi>\<^sub>\<O>) (\<Pi>\<^sub>\<O>))))) = (\<Union>(op\<^sub>1, op\<^sub>2)\<in>{(op\<^sub>1, op\<^sub>2). (op\<^sub>1, op\<^sub>2) \<in> set (\<Pi>\<^sub>\<O>) \<times> set (\<Pi>\<^sub>\<O>) \<and> index (\<Pi>\<^sub>\<O>) op\<^sub>1 \<noteq> index (\<Pi>\<^sub>\<O>) op\<^sub>2 \<and> are_operators_interfering op\<^sub>1 op\<^sub>2}. {{{(Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>1))\<inverse>, (Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>2))\<inverse>}} |k. k \<in> {0..<t}})
[PROOF STEP]
let ?fs = "[encode_interfering_operator_pair_exclusion \<Pi> k op\<^sub>1 op\<^sub>2.
    (op\<^sub>1, op\<^sub>2) \<leftarrow> ?interfering, k \<leftarrow> [0..<t]]"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. cnf ` set (concat (map (\<lambda>(op\<^sub>1, op\<^sub>2). map (\<lambda>k. encode_interfering_operator_pair_exclusion \<Pi> k op\<^sub>1 op\<^sub>2) [0..<t]) (filter (\<lambda>(op\<^sub>1, op\<^sub>2). index (\<Pi>\<^sub>\<O>) op\<^sub>1 \<noteq> index (\<Pi>\<^sub>\<O>) op\<^sub>2 \<and> are_operators_interfering op\<^sub>1 op\<^sub>2) (List.product (\<Pi>\<^sub>\<O>) (\<Pi>\<^sub>\<O>))))) = (\<Union>(op\<^sub>1, op\<^sub>2)\<in>{(op\<^sub>1, op\<^sub>2). (op\<^sub>1, op\<^sub>2) \<in> set (\<Pi>\<^sub>\<O>) \<times> set (\<Pi>\<^sub>\<O>) \<and> index (\<Pi>\<^sub>\<O>) op\<^sub>1 \<noteq> index (\<Pi>\<^sub>\<O>) op\<^sub>2 \<and> are_operators_interfering op\<^sub>1 op\<^sub>2}. {{{(Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>1))\<inverse>, (Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>2))\<inverse>}} |k. k \<in> {0..<t}})
[PROOF STEP]
have "cnf ` set ?fs = cnf ` (\<Union>(op\<^sub>1, op\<^sub>2) \<in> { (op\<^sub>1, op\<^sub>2).
    (op\<^sub>1, op\<^sub>2) \<in> set (operators_of \<Pi>) \<times> set (operators_of \<Pi>) \<and> index ?ops op\<^sub>1 \<noteq> index ?ops op\<^sub>2
      \<and> are_operators_interfering op\<^sub>1 op\<^sub>2 }.
    (\<lambda>k. encode_interfering_operator_pair_exclusion \<Pi> k op\<^sub>1 op\<^sub>2) ` {0..<t})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cnf ` set (concat (map (\<lambda>(op\<^sub>1, op\<^sub>2). map (\<lambda>k. encode_interfering_operator_pair_exclusion \<Pi> k op\<^sub>1 op\<^sub>2) [0..<t]) (filter (\<lambda>(op\<^sub>1, op\<^sub>2). index (\<Pi>\<^sub>\<O>) op\<^sub>1 \<noteq> index (\<Pi>\<^sub>\<O>) op\<^sub>2 \<and> are_operators_interfering op\<^sub>1 op\<^sub>2) (List.product (\<Pi>\<^sub>\<O>) (\<Pi>\<^sub>\<O>))))) = cnf ` (\<Union>(op\<^sub>1, op\<^sub>2)\<in>{(op\<^sub>1, op\<^sub>2). (op\<^sub>1, op\<^sub>2) \<in> set (\<Pi>\<^sub>\<O>) \<times> set (\<Pi>\<^sub>\<O>) \<and> index (\<Pi>\<^sub>\<O>) op\<^sub>1 \<noteq> index (\<Pi>\<^sub>\<O>) op\<^sub>2 \<and> are_operators_interfering op\<^sub>1 op\<^sub>2}. (\<lambda>k. encode_interfering_operator_pair_exclusion \<Pi> k op\<^sub>1 op\<^sub>2) ` {0..<t})
[PROOF STEP]
unfolding cnf_of_encode_interfering_operator_exclusion_is_ii
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cnf ` (\<Union>(op\<^sub>1, op\<^sub>2)\<in>{(op\<^sub>1, op\<^sub>2). (op\<^sub>1, op\<^sub>2) \<in> set (\<Pi>\<^sub>\<O>) \<times> set (\<Pi>\<^sub>\<O>) \<and> index (\<Pi>\<^sub>\<O>) op\<^sub>1 \<noteq> index (\<Pi>\<^sub>\<O>) op\<^sub>2 \<and> are_operators_interfering op\<^sub>1 op\<^sub>2}. (\<lambda>k. encode_interfering_operator_pair_exclusion \<Pi> k op\<^sub>1 op\<^sub>2) ` {0..<t}) = cnf ` (\<Union>(op\<^sub>1, op\<^sub>2)\<in>{(op\<^sub>1, op\<^sub>2). (op\<^sub>1, op\<^sub>2) \<in> set (\<Pi>\<^sub>\<O>) \<times> set (\<Pi>\<^sub>\<O>) \<and> index (\<Pi>\<^sub>\<O>) op\<^sub>1 \<noteq> index (\<Pi>\<^sub>\<O>) op\<^sub>2 \<and> are_operators_interfering op\<^sub>1 op\<^sub>2}. (\<lambda>k. encode_interfering_operator_pair_exclusion \<Pi> k op\<^sub>1 op\<^sub>2) ` {0..<t})
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
cnf ` set (concat (map (\<lambda>(op\<^sub>1, op\<^sub>2). map (\<lambda>k. encode_interfering_operator_pair_exclusion \<Pi> k op\<^sub>1 op\<^sub>2) [0..<t]) (filter (\<lambda>(op\<^sub>1, op\<^sub>2). index (\<Pi>\<^sub>\<O>) op\<^sub>1 \<noteq> index (\<Pi>\<^sub>\<O>) op\<^sub>2 \<and> are_operators_interfering op\<^sub>1 op\<^sub>2) (List.product (\<Pi>\<^sub>\<O>) (\<Pi>\<^sub>\<O>))))) = cnf ` (\<Union>(op\<^sub>1, op\<^sub>2)\<in>{(op\<^sub>1, op\<^sub>2). (op\<^sub>1, op\<^sub>2) \<in> set (\<Pi>\<^sub>\<O>) \<times> set (\<Pi>\<^sub>\<O>) \<and> index (\<Pi>\<^sub>\<O>) op\<^sub>1 \<noteq> index (\<Pi>\<^sub>\<O>) op\<^sub>2 \<and> are_operators_interfering op\<^sub>1 op\<^sub>2}. (\<lambda>k. encode_interfering_operator_pair_exclusion \<Pi> k op\<^sub>1 op\<^sub>2) ` {0..<t})

goal (1 subgoal):
 1. cnf ` set (concat (map (\<lambda>(op\<^sub>1, op\<^sub>2). map (\<lambda>k. encode_interfering_operator_pair_exclusion \<Pi> k op\<^sub>1 op\<^sub>2) [0..<t]) (filter (\<lambda>(op\<^sub>1, op\<^sub>2). index (\<Pi>\<^sub>\<O>) op\<^sub>1 \<noteq> index (\<Pi>\<^sub>\<O>) op\<^sub>2 \<and> are_operators_interfering op\<^sub>1 op\<^sub>2) (List.product (\<Pi>\<^sub>\<O>) (\<Pi>\<^sub>\<O>))))) = (\<Union>(op\<^sub>1, op\<^sub>2)\<in>{(op\<^sub>1, op\<^sub>2). (op\<^sub>1, op\<^sub>2) \<in> set (\<Pi>\<^sub>\<O>) \<times> set (\<Pi>\<^sub>\<O>) \<and> index (\<Pi>\<^sub>\<O>) op\<^sub>1 \<noteq> index (\<Pi>\<^sub>\<O>) op\<^sub>2 \<and> are_operators_interfering op\<^sub>1 op\<^sub>2}. {{{(Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>1))\<inverse>, (Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>2))\<inverse>}} |k. k \<in> {0..<t}})
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
cnf ` set (concat (map (\<lambda>(op\<^sub>1, op\<^sub>2). map (\<lambda>k. encode_interfering_operator_pair_exclusion \<Pi> k op\<^sub>1 op\<^sub>2) [0..<t]) (filter (\<lambda>(op\<^sub>1, op\<^sub>2). index (\<Pi>\<^sub>\<O>) op\<^sub>1 \<noteq> index (\<Pi>\<^sub>\<O>) op\<^sub>2 \<and> are_operators_interfering op\<^sub>1 op\<^sub>2) (List.product (\<Pi>\<^sub>\<O>) (\<Pi>\<^sub>\<O>))))) = cnf ` (\<Union>(op\<^sub>1, op\<^sub>2)\<in>{(op\<^sub>1, op\<^sub>2). (op\<^sub>1, op\<^sub>2) \<in> set (\<Pi>\<^sub>\<O>) \<times> set (\<Pi>\<^sub>\<O>) \<and> index (\<Pi>\<^sub>\<O>) op\<^sub>1 \<noteq> index (\<Pi>\<^sub>\<O>) op\<^sub>2 \<and> are_operators_interfering op\<^sub>1 op\<^sub>2}. (\<lambda>k. encode_interfering_operator_pair_exclusion \<Pi> k op\<^sub>1 op\<^sub>2) ` {0..<t})

goal (1 subgoal):
 1. cnf ` set (concat (map (\<lambda>(op\<^sub>1, op\<^sub>2). map (\<lambda>k. encode_interfering_operator_pair_exclusion \<Pi> k op\<^sub>1 op\<^sub>2) [0..<t]) (filter (\<lambda>(op\<^sub>1, op\<^sub>2). index (\<Pi>\<^sub>\<O>) op\<^sub>1 \<noteq> index (\<Pi>\<^sub>\<O>) op\<^sub>2 \<and> are_operators_interfering op\<^sub>1 op\<^sub>2) (List.product (\<Pi>\<^sub>\<O>) (\<Pi>\<^sub>\<O>))))) = (\<Union>(op\<^sub>1, op\<^sub>2)\<in>{(op\<^sub>1, op\<^sub>2). (op\<^sub>1, op\<^sub>2) \<in> set (\<Pi>\<^sub>\<O>) \<times> set (\<Pi>\<^sub>\<O>) \<and> index (\<Pi>\<^sub>\<O>) op\<^sub>1 \<noteq> index (\<Pi>\<^sub>\<O>) op\<^sub>2 \<and> are_operators_interfering op\<^sub>1 op\<^sub>2}. {{{(Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>1))\<inverse>, (Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>2))\<inverse>}} |k. k \<in> {0..<t}})
[PROOF STEP]
have "\<dots> = (\<Union>(op\<^sub>1, op\<^sub>2) \<in> { (op\<^sub>1, op\<^sub>2).
    (op\<^sub>1, op\<^sub>2) \<in> set (operators_of \<Pi>) \<times> set (operators_of \<Pi>) \<and> index ?ops op\<^sub>1 \<noteq> index ?ops op\<^sub>2
      \<and> are_operators_interfering op\<^sub>1 op\<^sub>2 }.
    (\<lambda>k. cnf (encode_interfering_operator_pair_exclusion \<Pi> k op\<^sub>1 op\<^sub>2)) ` {0..<t})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cnf ` (\<Union>(op\<^sub>1, op\<^sub>2)\<in>{(op\<^sub>1, op\<^sub>2). (op\<^sub>1, op\<^sub>2) \<in> set (\<Pi>\<^sub>\<O>) \<times> set (\<Pi>\<^sub>\<O>) \<and> index (\<Pi>\<^sub>\<O>) op\<^sub>1 \<noteq> index (\<Pi>\<^sub>\<O>) op\<^sub>2 \<and> are_operators_interfering op\<^sub>1 op\<^sub>2}. (\<lambda>k. encode_interfering_operator_pair_exclusion \<Pi> k op\<^sub>1 op\<^sub>2) ` {0..<t}) = (\<Union>(op\<^sub>1, op\<^sub>2)\<in>{(op\<^sub>1, op\<^sub>2). (op\<^sub>1, op\<^sub>2) \<in> set (\<Pi>\<^sub>\<O>) \<times> set (\<Pi>\<^sub>\<O>) \<and> index (\<Pi>\<^sub>\<O>) op\<^sub>1 \<noteq> index (\<Pi>\<^sub>\<O>) op\<^sub>2 \<and> are_operators_interfering op\<^sub>1 op\<^sub>2}. (\<lambda>k. cnf (encode_interfering_operator_pair_exclusion \<Pi> k op\<^sub>1 op\<^sub>2)) ` {0..<t})
[PROOF STEP]
unfolding image_Un image_comp comp_apply
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cnf ` (\<Union>(op\<^sub>1, op\<^sub>2)\<in>{(op\<^sub>1, op\<^sub>2). (op\<^sub>1, op\<^sub>2) \<in> set (\<Pi>\<^sub>\<O>) \<times> set (\<Pi>\<^sub>\<O>) \<and> index (\<Pi>\<^sub>\<O>) op\<^sub>1 \<noteq> index (\<Pi>\<^sub>\<O>) op\<^sub>2 \<and> are_operators_interfering op\<^sub>1 op\<^sub>2}. (\<lambda>k. encode_interfering_operator_pair_exclusion \<Pi> k op\<^sub>1 op\<^sub>2) ` {0..<t}) = (\<Union>(op\<^sub>1, op\<^sub>2)\<in>{(op\<^sub>1, op\<^sub>2). (op\<^sub>1, op\<^sub>2) \<in> set (\<Pi>\<^sub>\<O>) \<times> set (\<Pi>\<^sub>\<O>) \<and> index (\<Pi>\<^sub>\<O>) op\<^sub>1 \<noteq> index (\<Pi>\<^sub>\<O>) op\<^sub>2 \<and> are_operators_interfering op\<^sub>1 op\<^sub>2}. (\<lambda>k. cnf (encode_interfering_operator_pair_exclusion \<Pi> k op\<^sub>1 op\<^sub>2)) ` {0..<t})
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
cnf ` (\<Union>(op\<^sub>1, op\<^sub>2)\<in>{(op\<^sub>1, op\<^sub>2). (op\<^sub>1, op\<^sub>2) \<in> set (\<Pi>\<^sub>\<O>) \<times> set (\<Pi>\<^sub>\<O>) \<and> index (\<Pi>\<^sub>\<O>) op\<^sub>1 \<noteq> index (\<Pi>\<^sub>\<O>) op\<^sub>2 \<and> are_operators_interfering op\<^sub>1 op\<^sub>2}. (\<lambda>k. encode_interfering_operator_pair_exclusion \<Pi> k op\<^sub>1 op\<^sub>2) ` {0..<t}) = (\<Union>(op\<^sub>1, op\<^sub>2)\<in>{(op\<^sub>1, op\<^sub>2). (op\<^sub>1, op\<^sub>2) \<in> set (\<Pi>\<^sub>\<O>) \<times> set (\<Pi>\<^sub>\<O>) \<and> index (\<Pi>\<^sub>\<O>) op\<^sub>1 \<noteq> index (\<Pi>\<^sub>\<O>) op\<^sub>2 \<and> are_operators_interfering op\<^sub>1 op\<^sub>2}. (\<lambda>k. cnf (encode_interfering_operator_pair_exclusion \<Pi> k op\<^sub>1 op\<^sub>2)) ` {0..<t})

goal (1 subgoal):
 1. cnf ` set (concat (map (\<lambda>(op\<^sub>1, op\<^sub>2). map (\<lambda>k. encode_interfering_operator_pair_exclusion \<Pi> k op\<^sub>1 op\<^sub>2) [0..<t]) (filter (\<lambda>(op\<^sub>1, op\<^sub>2). index (\<Pi>\<^sub>\<O>) op\<^sub>1 \<noteq> index (\<Pi>\<^sub>\<O>) op\<^sub>2 \<and> are_operators_interfering op\<^sub>1 op\<^sub>2) (List.product (\<Pi>\<^sub>\<O>) (\<Pi>\<^sub>\<O>))))) = (\<Union>(op\<^sub>1, op\<^sub>2)\<in>{(op\<^sub>1, op\<^sub>2). (op\<^sub>1, op\<^sub>2) \<in> set (\<Pi>\<^sub>\<O>) \<times> set (\<Pi>\<^sub>\<O>) \<and> index (\<Pi>\<^sub>\<O>) op\<^sub>1 \<noteq> index (\<Pi>\<^sub>\<O>) op\<^sub>2 \<and> are_operators_interfering op\<^sub>1 op\<^sub>2}. {{{(Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>1))\<inverse>, (Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>2))\<inverse>}} |k. k \<in> {0..<t}})
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
cnf ` (\<Union>(op\<^sub>1, op\<^sub>2)\<in>{(op\<^sub>1, op\<^sub>2). (op\<^sub>1, op\<^sub>2) \<in> set (\<Pi>\<^sub>\<O>) \<times> set (\<Pi>\<^sub>\<O>) \<and> index (\<Pi>\<^sub>\<O>) op\<^sub>1 \<noteq> index (\<Pi>\<^sub>\<O>) op\<^sub>2 \<and> are_operators_interfering op\<^sub>1 op\<^sub>2}. (\<lambda>k. encode_interfering_operator_pair_exclusion \<Pi> k op\<^sub>1 op\<^sub>2) ` {0..<t}) = (\<Union>(op\<^sub>1, op\<^sub>2)\<in>{(op\<^sub>1, op\<^sub>2). (op\<^sub>1, op\<^sub>2) \<in> set (\<Pi>\<^sub>\<O>) \<times> set (\<Pi>\<^sub>\<O>) \<and> index (\<Pi>\<^sub>\<O>) op\<^sub>1 \<noteq> index (\<Pi>\<^sub>\<O>) op\<^sub>2 \<and> are_operators_interfering op\<^sub>1 op\<^sub>2}. (\<lambda>k. cnf (encode_interfering_operator_pair_exclusion \<Pi> k op\<^sub>1 op\<^sub>2)) ` {0..<t})

goal (1 subgoal):
 1. cnf ` set (concat (map (\<lambda>(op\<^sub>1, op\<^sub>2). map (\<lambda>k. encode_interfering_operator_pair_exclusion \<Pi> k op\<^sub>1 op\<^sub>2) [0..<t]) (filter (\<lambda>(op\<^sub>1, op\<^sub>2). index (\<Pi>\<^sub>\<O>) op\<^sub>1 \<noteq> index (\<Pi>\<^sub>\<O>) op\<^sub>2 \<and> are_operators_interfering op\<^sub>1 op\<^sub>2) (List.product (\<Pi>\<^sub>\<O>) (\<Pi>\<^sub>\<O>))))) = (\<Union>(op\<^sub>1, op\<^sub>2)\<in>{(op\<^sub>1, op\<^sub>2). (op\<^sub>1, op\<^sub>2) \<in> set (\<Pi>\<^sub>\<O>) \<times> set (\<Pi>\<^sub>\<O>) \<and> index (\<Pi>\<^sub>\<O>) op\<^sub>1 \<noteq> index (\<Pi>\<^sub>\<O>) op\<^sub>2 \<and> are_operators_interfering op\<^sub>1 op\<^sub>2}. {{{(Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>1))\<inverse>, (Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>2))\<inverse>}} |k. k \<in> {0..<t}})
[PROOF STEP]
have "\<dots> = (\<Union>(op\<^sub>1, op\<^sub>2) \<in> { (op\<^sub>1, op\<^sub>2).
    (op\<^sub>1, op\<^sub>2) \<in> set (operators_of \<Pi>) \<times> set (operators_of \<Pi>) \<and> index ?ops op\<^sub>1 \<noteq> index ?ops op\<^sub>2
      \<and> are_operators_interfering op\<^sub>1 op\<^sub>2 }.
    (\<lambda>k. {{ (Operator k (index ?ops op\<^sub>1))\<inverse>, (Operator k (index ?ops op\<^sub>2))\<inverse> }}) ` {0..<t})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Union>(op\<^sub>1, op\<^sub>2)\<in>{(op\<^sub>1, op\<^sub>2). (op\<^sub>1, op\<^sub>2) \<in> set (\<Pi>\<^sub>\<O>) \<times> set (\<Pi>\<^sub>\<O>) \<and> index (\<Pi>\<^sub>\<O>) op\<^sub>1 \<noteq> index (\<Pi>\<^sub>\<O>) op\<^sub>2 \<and> are_operators_interfering op\<^sub>1 op\<^sub>2}. (\<lambda>k. cnf (encode_interfering_operator_pair_exclusion \<Pi> k op\<^sub>1 op\<^sub>2)) ` {0..<t}) = (\<Union>(op\<^sub>1, op\<^sub>2)\<in>{(op\<^sub>1, op\<^sub>2). (op\<^sub>1, op\<^sub>2) \<in> set (\<Pi>\<^sub>\<O>) \<times> set (\<Pi>\<^sub>\<O>) \<and> index (\<Pi>\<^sub>\<O>) op\<^sub>1 \<noteq> index (\<Pi>\<^sub>\<O>) op\<^sub>2 \<and> are_operators_interfering op\<^sub>1 op\<^sub>2}. (\<lambda>k. {{(Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>1))\<inverse>, (Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>2))\<inverse>}}) ` {0..<t})
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<Union>(op\<^sub>1, op\<^sub>2)\<in>{(op\<^sub>1, op\<^sub>2). (op\<^sub>1, op\<^sub>2) \<in> set (\<Pi>\<^sub>\<O>) \<times> set (\<Pi>\<^sub>\<O>) \<and> index (\<Pi>\<^sub>\<O>) op\<^sub>1 \<noteq> index (\<Pi>\<^sub>\<O>) op\<^sub>2 \<and> are_operators_interfering op\<^sub>1 op\<^sub>2}. (\<lambda>k. cnf (encode_interfering_operator_pair_exclusion \<Pi> k op\<^sub>1 op\<^sub>2)) ` {0..<t}) = (\<Union>(op\<^sub>1, op\<^sub>2)\<in>{(op\<^sub>1, op\<^sub>2). (op\<^sub>1, op\<^sub>2) \<in> set (\<Pi>\<^sub>\<O>) \<times> set (\<Pi>\<^sub>\<O>) \<and> index (\<Pi>\<^sub>\<O>) op\<^sub>1 \<noteq> index (\<Pi>\<^sub>\<O>) op\<^sub>2 \<and> are_operators_interfering op\<^sub>1 op\<^sub>2}. (\<lambda>k. {{(Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>1))\<inverse>, (Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>2))\<inverse>}}) ` {0..<t})

goal (1 subgoal):
 1. cnf ` set (concat (map (\<lambda>(op\<^sub>1, op\<^sub>2). map (\<lambda>k. encode_interfering_operator_pair_exclusion \<Pi> k op\<^sub>1 op\<^sub>2) [0..<t]) (filter (\<lambda>(op\<^sub>1, op\<^sub>2). index (\<Pi>\<^sub>\<O>) op\<^sub>1 \<noteq> index (\<Pi>\<^sub>\<O>) op\<^sub>2 \<and> are_operators_interfering op\<^sub>1 op\<^sub>2) (List.product (\<Pi>\<^sub>\<O>) (\<Pi>\<^sub>\<O>))))) = (\<Union>(op\<^sub>1, op\<^sub>2)\<in>{(op\<^sub>1, op\<^sub>2). (op\<^sub>1, op\<^sub>2) \<in> set (\<Pi>\<^sub>\<O>) \<times> set (\<Pi>\<^sub>\<O>) \<and> index (\<Pi>\<^sub>\<O>) op\<^sub>1 \<noteq> index (\<Pi>\<^sub>\<O>) op\<^sub>2 \<and> are_operators_interfering op\<^sub>1 op\<^sub>2}. {{{(Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>1))\<inverse>, (Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>2))\<inverse>}} |k. k \<in> {0..<t}})
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Union>(op\<^sub>1, op\<^sub>2)\<in>{(op\<^sub>1, op\<^sub>2). (op\<^sub>1, op\<^sub>2) \<in> set (\<Pi>\<^sub>\<O>) \<times> set (\<Pi>\<^sub>\<O>) \<and> index (\<Pi>\<^sub>\<O>) op\<^sub>1 \<noteq> index (\<Pi>\<^sub>\<O>) op\<^sub>2 \<and> are_operators_interfering op\<^sub>1 op\<^sub>2}. (\<lambda>k. cnf (encode_interfering_operator_pair_exclusion \<Pi> k op\<^sub>1 op\<^sub>2)) ` {0..<t}) = (\<Union>(op\<^sub>1, op\<^sub>2)\<in>{(op\<^sub>1, op\<^sub>2). (op\<^sub>1, op\<^sub>2) \<in> set (\<Pi>\<^sub>\<O>) \<times> set (\<Pi>\<^sub>\<O>) \<and> index (\<Pi>\<^sub>\<O>) op\<^sub>1 \<noteq> index (\<Pi>\<^sub>\<O>) op\<^sub>2 \<and> are_operators_interfering op\<^sub>1 op\<^sub>2}. (\<lambda>k. {{(Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>1))\<inverse>, (Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>2))\<inverse>}}) ` {0..<t})

goal (1 subgoal):
 1. cnf ` set (concat (map (\<lambda>(op\<^sub>1, op\<^sub>2). map (\<lambda>k. encode_interfering_operator_pair_exclusion \<Pi> k op\<^sub>1 op\<^sub>2) [0..<t]) (filter (\<lambda>(op\<^sub>1, op\<^sub>2). index (\<Pi>\<^sub>\<O>) op\<^sub>1 \<noteq> index (\<Pi>\<^sub>\<O>) op\<^sub>2 \<and> are_operators_interfering op\<^sub>1 op\<^sub>2) (List.product (\<Pi>\<^sub>\<O>) (\<Pi>\<^sub>\<O>))))) = (\<Union>(op\<^sub>1, op\<^sub>2)\<in>{(op\<^sub>1, op\<^sub>2). (op\<^sub>1, op\<^sub>2) \<in> set (\<Pi>\<^sub>\<O>) \<times> set (\<Pi>\<^sub>\<O>) \<and> index (\<Pi>\<^sub>\<O>) op\<^sub>1 \<noteq> index (\<Pi>\<^sub>\<O>) op\<^sub>2 \<and> are_operators_interfering op\<^sub>1 op\<^sub>2}. {{{(Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>1))\<inverse>, (Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>2))\<inverse>}} |k. k \<in> {0..<t}})
[PROOF STEP]
have "\<dots> = (\<Union>(op\<^sub>1, op\<^sub>2) \<in> { (op\<^sub>1, op\<^sub>2).
    (op\<^sub>1, op\<^sub>2) \<in> set (operators_of \<Pi>) \<times> set (operators_of \<Pi>) \<and> index ?ops op\<^sub>1 \<noteq> index ?ops op\<^sub>2
        \<and> are_operators_interfering op\<^sub>1 op\<^sub>2 }.
      (\<lambda>k. {{ (Operator k (index ?ops op\<^sub>1))\<inverse>, (Operator k (index ?ops op\<^sub>2))\<inverse> }})
        ` { k | k. k \<in> {0..<t}})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Union>(op\<^sub>1, op\<^sub>2)\<in>{(op\<^sub>1, op\<^sub>2). (op\<^sub>1, op\<^sub>2) \<in> set (\<Pi>\<^sub>\<O>) \<times> set (\<Pi>\<^sub>\<O>) \<and> index (\<Pi>\<^sub>\<O>) op\<^sub>1 \<noteq> index (\<Pi>\<^sub>\<O>) op\<^sub>2 \<and> are_operators_interfering op\<^sub>1 op\<^sub>2}. (\<lambda>k. {{(Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>1))\<inverse>, (Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>2))\<inverse>}}) ` {0..<t}) = (\<Union>(op\<^sub>1, op\<^sub>2)\<in>{(op\<^sub>1, op\<^sub>2). (op\<^sub>1, op\<^sub>2) \<in> set (\<Pi>\<^sub>\<O>) \<times> set (\<Pi>\<^sub>\<O>) \<and> index (\<Pi>\<^sub>\<O>) op\<^sub>1 \<noteq> index (\<Pi>\<^sub>\<O>) op\<^sub>2 \<and> are_operators_interfering op\<^sub>1 op\<^sub>2}. (\<lambda>k. {{(Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>1))\<inverse>, (Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>2))\<inverse>}}) ` {k |k. k \<in> {0..<t}})
[PROOF STEP]
by blast
  \<comment> \<open> TODO slow.\<close>
[PROOF STATE]
proof (state)
this:
(\<Union>(op\<^sub>1, op\<^sub>2)\<in>{(op\<^sub>1, op\<^sub>2). (op\<^sub>1, op\<^sub>2) \<in> set (\<Pi>\<^sub>\<O>) \<times> set (\<Pi>\<^sub>\<O>) \<and> index (\<Pi>\<^sub>\<O>) op\<^sub>1 \<noteq> index (\<Pi>\<^sub>\<O>) op\<^sub>2 \<and> are_operators_interfering op\<^sub>1 op\<^sub>2}. (\<lambda>k. {{(Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>1))\<inverse>, (Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>2))\<inverse>}}) ` {0..<t}) = (\<Union>(op\<^sub>1, op\<^sub>2)\<in>{(op\<^sub>1, op\<^sub>2). (op\<^sub>1, op\<^sub>2) \<in> set (\<Pi>\<^sub>\<O>) \<times> set (\<Pi>\<^sub>\<O>) \<and> index (\<Pi>\<^sub>\<O>) op\<^sub>1 \<noteq> index (\<Pi>\<^sub>\<O>) op\<^sub>2 \<and> are_operators_interfering op\<^sub>1 op\<^sub>2}. (\<lambda>k. {{(Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>1))\<inverse>, (Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>2))\<inverse>}}) ` {k |k. k \<in> {0..<t}})

goal (1 subgoal):
 1. cnf ` set (concat (map (\<lambda>(op\<^sub>1, op\<^sub>2). map (\<lambda>k. encode_interfering_operator_pair_exclusion \<Pi> k op\<^sub>1 op\<^sub>2) [0..<t]) (filter (\<lambda>(op\<^sub>1, op\<^sub>2). index (\<Pi>\<^sub>\<O>) op\<^sub>1 \<noteq> index (\<Pi>\<^sub>\<O>) op\<^sub>2 \<and> are_operators_interfering op\<^sub>1 op\<^sub>2) (List.product (\<Pi>\<^sub>\<O>) (\<Pi>\<^sub>\<O>))))) = (\<Union>(op\<^sub>1, op\<^sub>2)\<in>{(op\<^sub>1, op\<^sub>2). (op\<^sub>1, op\<^sub>2) \<in> set (\<Pi>\<^sub>\<O>) \<times> set (\<Pi>\<^sub>\<O>) \<and> index (\<Pi>\<^sub>\<O>) op\<^sub>1 \<noteq> index (\<Pi>\<^sub>\<O>) op\<^sub>2 \<and> are_operators_interfering op\<^sub>1 op\<^sub>2}. {{{(Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>1))\<inverse>, (Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>2))\<inverse>}} |k. k \<in> {0..<t}})
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
cnf ` set (concat (map (\<lambda>(op\<^sub>1, op\<^sub>2). map (\<lambda>k. encode_interfering_operator_pair_exclusion \<Pi> k op\<^sub>1 op\<^sub>2) [0..<t]) (filter (\<lambda>(op\<^sub>1, op\<^sub>2). index (\<Pi>\<^sub>\<O>) op\<^sub>1 \<noteq> index (\<Pi>\<^sub>\<O>) op\<^sub>2 \<and> are_operators_interfering op\<^sub>1 op\<^sub>2) (List.product (\<Pi>\<^sub>\<O>) (\<Pi>\<^sub>\<O>))))) = (\<Union>(op\<^sub>1, op\<^sub>2)\<in>{(op\<^sub>1, op\<^sub>2). (op\<^sub>1, op\<^sub>2) \<in> set (\<Pi>\<^sub>\<O>) \<times> set (\<Pi>\<^sub>\<O>) \<and> index (\<Pi>\<^sub>\<O>) op\<^sub>1 \<noteq> index (\<Pi>\<^sub>\<O>) op\<^sub>2 \<and> are_operators_interfering op\<^sub>1 op\<^sub>2}. (\<lambda>k. {{(Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>1))\<inverse>, (Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>2))\<inverse>}}) ` {k |k. k \<in> {0..<t}})
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
cnf ` set (concat (map (\<lambda>(op\<^sub>1, op\<^sub>2). map (\<lambda>k. encode_interfering_operator_pair_exclusion \<Pi> k op\<^sub>1 op\<^sub>2) [0..<t]) (filter (\<lambda>(op\<^sub>1, op\<^sub>2). index (\<Pi>\<^sub>\<O>) op\<^sub>1 \<noteq> index (\<Pi>\<^sub>\<O>) op\<^sub>2 \<and> are_operators_interfering op\<^sub>1 op\<^sub>2) (List.product (\<Pi>\<^sub>\<O>) (\<Pi>\<^sub>\<O>))))) = (\<Union>(op\<^sub>1, op\<^sub>2)\<in>{(op\<^sub>1, op\<^sub>2). (op\<^sub>1, op\<^sub>2) \<in> set (\<Pi>\<^sub>\<O>) \<times> set (\<Pi>\<^sub>\<O>) \<and> index (\<Pi>\<^sub>\<O>) op\<^sub>1 \<noteq> index (\<Pi>\<^sub>\<O>) op\<^sub>2 \<and> are_operators_interfering op\<^sub>1 op\<^sub>2}. (\<lambda>k. {{(Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>1))\<inverse>, (Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>2))\<inverse>}}) ` {k |k. k \<in> {0..<t}})

goal (1 subgoal):
 1. cnf ` set (concat (map (\<lambda>(op\<^sub>1, op\<^sub>2). map (\<lambda>k. encode_interfering_operator_pair_exclusion \<Pi> k op\<^sub>1 op\<^sub>2) [0..<t]) (filter (\<lambda>(op\<^sub>1, op\<^sub>2). index (\<Pi>\<^sub>\<O>) op\<^sub>1 \<noteq> index (\<Pi>\<^sub>\<O>) op\<^sub>2 \<and> are_operators_interfering op\<^sub>1 op\<^sub>2) (List.product (\<Pi>\<^sub>\<O>) (\<Pi>\<^sub>\<O>))))) = (\<Union>(op\<^sub>1, op\<^sub>2)\<in>{(op\<^sub>1, op\<^sub>2). (op\<^sub>1, op\<^sub>2) \<in> set (\<Pi>\<^sub>\<O>) \<times> set (\<Pi>\<^sub>\<O>) \<and> index (\<Pi>\<^sub>\<O>) op\<^sub>1 \<noteq> index (\<Pi>\<^sub>\<O>) op\<^sub>2 \<and> are_operators_interfering op\<^sub>1 op\<^sub>2}. {{{(Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>1))\<inverse>, (Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>2))\<inverse>}} |k. k \<in> {0..<t}})
[PROOF STEP]
unfolding operators_of_def setcompr_eq_image[of _ "\<lambda>k. k \<in> {0..<t}"]
[PROOF STATE]
proof (prove)
using this:
cnf ` set (concat (map (\<lambda>(op\<^sub>1, op\<^sub>2). map (\<lambda>k. encode_interfering_operator_pair_exclusion \<Pi> k op\<^sub>1 op\<^sub>2) [0..<t]) (filter (\<lambda>(op\<^sub>1, op\<^sub>2). index ((id \<circ> Record.iso_tuple_snd Record.tuple_iso_tuple \<circ> Record.iso_tuple_fst Record.tuple_iso_tuple \<circ> Record.iso_tuple_fst strips_problem_ext_Tuple_Iso) \<Pi>) op\<^sub>1 \<noteq> index ((id \<circ> Record.iso_tuple_snd Record.tuple_iso_tuple \<circ> Record.iso_tuple_fst Record.tuple_iso_tuple \<circ> Record.iso_tuple_fst strips_problem_ext_Tuple_Iso) \<Pi>) op\<^sub>2 \<and> are_operators_interfering op\<^sub>1 op\<^sub>2) (List.product ((id \<circ> Record.iso_tuple_snd Record.tuple_iso_tuple \<circ> Record.iso_tuple_fst Record.tuple_iso_tuple \<circ> Record.iso_tuple_fst strips_problem_ext_Tuple_Iso) \<Pi>) ((id \<circ> Record.iso_tuple_snd Record.tuple_iso_tuple \<circ> Record.iso_tuple_fst Record.tuple_iso_tuple \<circ> Record.iso_tuple_fst strips_problem_ext_Tuple_Iso) \<Pi>))))) = (\<Union>(op\<^sub>1, op\<^sub>2)\<in>{(op\<^sub>1, op\<^sub>2). (op\<^sub>1, op\<^sub>2) \<in> set ((id \<circ> Record.iso_tuple_snd Record.tuple_iso_tuple \<circ> Record.iso_tuple_fst Record.tuple_iso_tuple \<circ> Record.iso_tuple_fst strips_problem_ext_Tuple_Iso) \<Pi>) \<times> set ((id \<circ> Record.iso_tuple_snd Record.tuple_iso_tuple \<circ> Record.iso_tuple_fst Record.tuple_iso_tuple \<circ> Record.iso_tuple_fst strips_problem_ext_Tuple_Iso) \<Pi>) \<and> index ((id \<circ> Record.iso_tuple_snd Record.tuple_iso_tuple \<circ> Record.iso_tuple_fst Record.tuple_iso_tuple \<circ> Record.iso_tuple_fst strips_problem_ext_Tuple_Iso) \<Pi>) op\<^sub>1 \<noteq> index ((id \<circ> Record.iso_tuple_snd Record.tuple_iso_tuple \<circ> Record.iso_tuple_fst Record.tuple_iso_tuple \<circ> Record.iso_tuple_fst strips_problem_ext_Tuple_Iso) \<Pi>) op\<^sub>2 \<and> are_operators_interfering op\<^sub>1 op\<^sub>2}. (\<lambda>k. {{(Operator k (index ((id \<circ> Record.iso_tuple_snd Record.tuple_iso_tuple \<circ> Record.iso_tuple_fst Record.tuple_iso_tuple \<circ> Record.iso_tuple_fst strips_problem_ext_Tuple_Iso) \<Pi>) op\<^sub>1))\<inverse>, (Operator k (index ((id \<circ> Record.iso_tuple_snd Record.tuple_iso_tuple \<circ> Record.iso_tuple_fst Record.tuple_iso_tuple \<circ> Record.iso_tuple_fst strips_problem_ext_Tuple_Iso) \<Pi>) op\<^sub>2))\<inverse>}}) ` (\<lambda>k. k) ` {k. k \<in> {0..<t}})

goal (1 subgoal):
 1. cnf ` set (concat (map (\<lambda>(op\<^sub>1, op\<^sub>2). map (\<lambda>k. encode_interfering_operator_pair_exclusion \<Pi> k op\<^sub>1 op\<^sub>2) [0..<t]) (filter (\<lambda>(op\<^sub>1, op\<^sub>2). index ((id \<circ> Record.iso_tuple_snd Record.tuple_iso_tuple \<circ> Record.iso_tuple_fst Record.tuple_iso_tuple \<circ> Record.iso_tuple_fst strips_problem_ext_Tuple_Iso) \<Pi>) op\<^sub>1 \<noteq> index ((id \<circ> Record.iso_tuple_snd Record.tuple_iso_tuple \<circ> Record.iso_tuple_fst Record.tuple_iso_tuple \<circ> Record.iso_tuple_fst strips_problem_ext_Tuple_Iso) \<Pi>) op\<^sub>2 \<and> are_operators_interfering op\<^sub>1 op\<^sub>2) (List.product ((id \<circ> Record.iso_tuple_snd Record.tuple_iso_tuple \<circ> Record.iso_tuple_fst Record.tuple_iso_tuple \<circ> Record.iso_tuple_fst strips_problem_ext_Tuple_Iso) \<Pi>) ((id \<circ> Record.iso_tuple_snd Record.tuple_iso_tuple \<circ> Record.iso_tuple_fst Record.tuple_iso_tuple \<circ> Record.iso_tuple_fst strips_problem_ext_Tuple_Iso) \<Pi>))))) = (\<Union>(op\<^sub>1, op\<^sub>2)\<in>{(op\<^sub>1, op\<^sub>2). (op\<^sub>1, op\<^sub>2) \<in> set ((id \<circ> Record.iso_tuple_snd Record.tuple_iso_tuple \<circ> Record.iso_tuple_fst Record.tuple_iso_tuple \<circ> Record.iso_tuple_fst strips_problem_ext_Tuple_Iso) \<Pi>) \<times> set ((id \<circ> Record.iso_tuple_snd Record.tuple_iso_tuple \<circ> Record.iso_tuple_fst Record.tuple_iso_tuple \<circ> Record.iso_tuple_fst strips_problem_ext_Tuple_Iso) \<Pi>) \<and> index ((id \<circ> Record.iso_tuple_snd Record.tuple_iso_tuple \<circ> Record.iso_tuple_fst Record.tuple_iso_tuple \<circ> Record.iso_tuple_fst strips_problem_ext_Tuple_Iso) \<Pi>) op\<^sub>1 \<noteq> index ((id \<circ> Record.iso_tuple_snd Record.tuple_iso_tuple \<circ> Record.iso_tuple_fst Record.tuple_iso_tuple \<circ> Record.iso_tuple_fst strips_problem_ext_Tuple_Iso) \<Pi>) op\<^sub>2 \<and> are_operators_interfering op\<^sub>1 op\<^sub>2}. (\<lambda>k. {{(Operator k (index ((id \<circ> Record.iso_tuple_snd Record.tuple_iso_tuple \<circ> Record.iso_tuple_fst Record.tuple_iso_tuple \<circ> Record.iso_tuple_fst strips_problem_ext_Tuple_Iso) \<Pi>) op\<^sub>1))\<inverse>, (Operator k (index ((id \<circ> Record.iso_tuple_snd Record.tuple_iso_tuple \<circ> Record.iso_tuple_fst Record.tuple_iso_tuple \<circ> Record.iso_tuple_fst strips_problem_ext_Tuple_Iso) \<Pi>) op\<^sub>2))\<inverse>}}) ` {k. k \<in> {0..<t}})
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
cnf ` set (concat (map (\<lambda>(op\<^sub>1, op\<^sub>2). map (\<lambda>k. encode_interfering_operator_pair_exclusion \<Pi> k op\<^sub>1 op\<^sub>2) [0..<t]) (filter (\<lambda>(op\<^sub>1, op\<^sub>2). index (\<Pi>\<^sub>\<O>) op\<^sub>1 \<noteq> index (\<Pi>\<^sub>\<O>) op\<^sub>2 \<and> are_operators_interfering op\<^sub>1 op\<^sub>2) (List.product (\<Pi>\<^sub>\<O>) (\<Pi>\<^sub>\<O>))))) = (\<Union>(op\<^sub>1, op\<^sub>2)\<in>{(op\<^sub>1, op\<^sub>2). (op\<^sub>1, op\<^sub>2) \<in> set (\<Pi>\<^sub>\<O>) \<times> set (\<Pi>\<^sub>\<O>) \<and> index (\<Pi>\<^sub>\<O>) op\<^sub>1 \<noteq> index (\<Pi>\<^sub>\<O>) op\<^sub>2 \<and> are_operators_interfering op\<^sub>1 op\<^sub>2}. {{{(Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>1))\<inverse>, (Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>2))\<inverse>}} |k. k \<in> {0..<t}})

goal:
No subgoals!
[PROOF STEP]
qed