[STATEMENT]
lemma dr_Seq:
  assumes drAB: "drefines \<phi> P A B"
      and drBC: "drefines \<phi> Q C D"
      and wpB:  "\<guillemotleft>P\<guillemotright> \<tturnstile> wp B \<guillemotleft>Q\<guillemotright>"
      and wB:   "well_def B"
      and wC:   "well_def C"
      and wD:   "well_def D"
  shows "drefines \<phi> P (A;;C) (B;;D)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. drefines \<phi> P (A ;; C) (B ;; D)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>Pa Q. \<lbrakk>unitary Pa; unitary Q; Pa \<tturnstile> wp (A ;; C) Q\<rbrakk> \<Longrightarrow> \<guillemotleft> P \<guillemotright> && (Pa \<circ> \<phi>) \<tturnstile> wp (B ;; D) (Q \<circ> \<phi>)
[PROOF STEP]
fix R and S
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>Pa Q. \<lbrakk>unitary Pa; unitary Q; Pa \<tturnstile> wp (A ;; C) Q\<rbrakk> \<Longrightarrow> \<guillemotleft> P \<guillemotright> && (Pa \<circ> \<phi>) \<tturnstile> wp (B ;; D) (Q \<circ> \<phi>)
[PROOF STEP]
assume uR: "unitary R" and uS: "unitary S"
     and wpAC: "R \<tturnstile> wp (A;;C) S"
[PROOF STATE]
proof (state)
this:
unitary R
unitary S
R \<tturnstile> wp (A ;; C) S

goal (1 subgoal):
 1. \<And>Pa Q. \<lbrakk>unitary Pa; unitary Q; Pa \<tturnstile> wp (A ;; C) Q\<rbrakk> \<Longrightarrow> \<guillemotleft> P \<guillemotright> && (Pa \<circ> \<phi>) \<tturnstile> wp (B ;; D) (Q \<circ> \<phi>)
[PROOF STEP]
from uR
[PROOF STATE]
proof (chain)
picking this:
unitary R
[PROOF STEP]
have "\<guillemotleft>P\<guillemotright> && (R o \<phi>) = \<guillemotleft>P\<guillemotright> && (\<guillemotleft>P\<guillemotright> && (R o \<phi>))"
[PROOF STATE]
proof (prove)
using this:
unitary R

goal (1 subgoal):
 1. \<guillemotleft> P \<guillemotright> && (R \<circ> \<phi>) = \<guillemotleft> P \<guillemotright> && (\<guillemotleft> P \<guillemotright> && (R \<circ> \<phi>))
[PROOF STEP]
by(simp add:exp_conj_assoc)
[PROOF STATE]
proof (state)
this:
\<guillemotleft> P \<guillemotright> && (R \<circ> \<phi>) = \<guillemotleft> P \<guillemotright> && (\<guillemotleft> P \<guillemotright> && (R \<circ> \<phi>))

goal (1 subgoal):
 1. \<And>Pa Q. \<lbrakk>unitary Pa; unitary Q; Pa \<tturnstile> wp (A ;; C) Q\<rbrakk> \<Longrightarrow> \<guillemotleft> P \<guillemotright> && (Pa \<circ> \<phi>) \<tturnstile> wp (B ;; D) (Q \<circ> \<phi>)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<guillemotleft> P \<guillemotright> && (R \<circ> \<phi>) = \<guillemotleft> P \<guillemotright> && (\<guillemotleft> P \<guillemotright> && (R \<circ> \<phi>))

goal (1 subgoal):
 1. \<And>Pa Q. \<lbrakk>unitary Pa; unitary Q; Pa \<tturnstile> wp (A ;; C) Q\<rbrakk> \<Longrightarrow> \<guillemotleft> P \<guillemotright> && (Pa \<circ> \<phi>) \<tturnstile> wp (B ;; D) (Q \<circ> \<phi>)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
\<guillemotleft> P \<guillemotright> && (R \<circ> \<phi>) = \<guillemotleft> P \<guillemotright> && (\<guillemotleft> P \<guillemotright> && (R \<circ> \<phi>))

goal (1 subgoal):
 1. \<And>Pa Q. \<lbrakk>unitary Pa; unitary Q; Pa \<tturnstile> wp (A ;; C) Q\<rbrakk> \<Longrightarrow> \<guillemotleft> P \<guillemotright> && (Pa \<circ> \<phi>) \<tturnstile> wp (B ;; D) (Q \<circ> \<phi>)
[PROOF STEP]
from well_def_wp_healthy[OF wC] uR uS
     and wpAC[unfolded eval_wp_Seq o_def]
[PROOF STATE]
proof (chain)
picking this:
healthy (wp C)
unitary R
unitary S
R \<tturnstile> wp A (wp C S)
[PROOF STEP]
have "\<guillemotleft>P\<guillemotright> && (R o \<phi>) \<tturnstile> wp B (wp C S o \<phi>)"
[PROOF STATE]
proof (prove)
using this:
healthy (wp C)
unitary R
unitary S
R \<tturnstile> wp A (wp C S)

goal (1 subgoal):
 1. \<guillemotleft> P \<guillemotright> && (R \<circ> \<phi>) \<tturnstile> wp B (wp C S \<circ> \<phi>)
[PROOF STEP]
by(auto intro:drefinesD[OF drAB])
[PROOF STATE]
proof (state)
this:
\<guillemotleft> P \<guillemotright> && (R \<circ> \<phi>) \<tturnstile> wp B (wp C S \<circ> \<phi>)

goal (1 subgoal):
 1. \<And>Pa Q. \<lbrakk>unitary Pa; unitary Q; Pa \<tturnstile> wp (A ;; C) Q\<rbrakk> \<Longrightarrow> \<guillemotleft> P \<guillemotright> && (Pa \<circ> \<phi>) \<tturnstile> wp (B ;; D) (Q \<circ> \<phi>)
[PROOF STEP]
with wpB well_def_wp_healthy[OF wC] uS
         sublinear_sub_conj[OF well_def_wp_sublinear, OF wB]
[PROOF STATE]
proof (chain)
picking this:
\<guillemotleft> P \<guillemotright> \<tturnstile> wp B \<guillemotleft> Q \<guillemotright>
healthy (wp C)
unitary S
sub_conj (wp B)
\<guillemotleft> P \<guillemotright> && (R \<circ> \<phi>) \<tturnstile> wp B (wp C S \<circ> \<phi>)
[PROOF STEP]
have "\<guillemotleft>P\<guillemotright> && (\<guillemotleft>P\<guillemotright> && (R o \<phi>)) \<tturnstile> wp B (\<guillemotleft>Q\<guillemotright> && (wp C S o \<phi>))"
[PROOF STATE]
proof (prove)
using this:
\<guillemotleft> P \<guillemotright> \<tturnstile> wp B \<guillemotleft> Q \<guillemotright>
healthy (wp C)
unitary S
sub_conj (wp B)
\<guillemotleft> P \<guillemotright> && (R \<circ> \<phi>) \<tturnstile> wp B (wp C S \<circ> \<phi>)

goal (1 subgoal):
 1. \<guillemotleft> P \<guillemotright> && (\<guillemotleft> P \<guillemotright> && (R \<circ> \<phi>)) \<tturnstile> wp B (\<guillemotleft> Q \<guillemotright> && (wp C S \<circ> \<phi>))
[PROOF STEP]
by(auto intro!:entails_combine dest!:unitary_sound)
[PROOF STATE]
proof (state)
this:
\<guillemotleft> P \<guillemotright> && (\<guillemotleft> P \<guillemotright> && (R \<circ> \<phi>)) \<tturnstile> wp B (\<guillemotleft> Q \<guillemotright> && (wp C S \<circ> \<phi>))

goal (1 subgoal):
 1. \<And>Pa Q. \<lbrakk>unitary Pa; unitary Q; Pa \<tturnstile> wp (A ;; C) Q\<rbrakk> \<Longrightarrow> \<guillemotleft> P \<guillemotright> && (Pa \<circ> \<phi>) \<tturnstile> wp (B ;; D) (Q \<circ> \<phi>)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<guillemotleft> P \<guillemotright> && (\<guillemotleft> P \<guillemotright> && (R \<circ> \<phi>)) \<tturnstile> wp B (\<guillemotleft> Q \<guillemotright> && (wp C S \<circ> \<phi>))

goal (1 subgoal):
 1. \<And>Pa Q. \<lbrakk>unitary Pa; unitary Q; Pa \<tturnstile> wp (A ;; C) Q\<rbrakk> \<Longrightarrow> \<guillemotleft> P \<guillemotright> && (Pa \<circ> \<phi>) \<tturnstile> wp (B ;; D) (Q \<circ> \<phi>)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<guillemotleft> P \<guillemotright> && (\<guillemotleft> P \<guillemotright> && (R \<circ> \<phi>)) \<tturnstile> wp B (\<guillemotleft> Q \<guillemotright> && (wp C S \<circ> \<phi>))

goal (1 subgoal):
 1. \<And>Pa Q. \<lbrakk>unitary Pa; unitary Q; Pa \<tturnstile> wp (A ;; C) Q\<rbrakk> \<Longrightarrow> \<guillemotleft> P \<guillemotright> && (Pa \<circ> \<phi>) \<tturnstile> wp (B ;; D) (Q \<circ> \<phi>)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
\<guillemotleft> P \<guillemotright> && (\<guillemotleft> P \<guillemotright> && (R \<circ> \<phi>)) \<tturnstile> wp B (\<guillemotleft> Q \<guillemotright> && (wp C S \<circ> \<phi>))

goal (1 subgoal):
 1. \<And>Pa Q. \<lbrakk>unitary Pa; unitary Q; Pa \<tturnstile> wp (A ;; C) Q\<rbrakk> \<Longrightarrow> \<guillemotleft> P \<guillemotright> && (Pa \<circ> \<phi>) \<tturnstile> wp (B ;; D) (Q \<circ> \<phi>)
[PROOF STEP]
from uS well_def_wp_healthy[OF wC]
[PROOF STATE]
proof (chain)
picking this:
unitary S
healthy (wp C)
[PROOF STEP]
have "\<guillemotleft>Q\<guillemotright> && (wp C S o \<phi>) \<tturnstile> wp D (S o \<phi>)"
[PROOF STATE]
proof (prove)
using this:
unitary S
healthy (wp C)

goal (1 subgoal):
 1. \<guillemotleft> Q \<guillemotright> && (wp C S \<circ> \<phi>) \<tturnstile> wp D (S \<circ> \<phi>)
[PROOF STEP]
by(auto intro!:drefinesD[OF drBC])
[PROOF STATE]
proof (state)
this:
\<guillemotleft> Q \<guillemotright> && (wp C S \<circ> \<phi>) \<tturnstile> wp D (S \<circ> \<phi>)

goal (1 subgoal):
 1. \<And>Pa Q. \<lbrakk>unitary Pa; unitary Q; Pa \<tturnstile> wp (A ;; C) Q\<rbrakk> \<Longrightarrow> \<guillemotleft> P \<guillemotright> && (Pa \<circ> \<phi>) \<tturnstile> wp (B ;; D) (Q \<circ> \<phi>)
[PROOF STEP]
with well_def_wp_healthy[OF wB] well_def_wp_healthy[OF wC]
         well_def_wp_healthy[OF wD] and unitary_sound[OF uS]
[PROOF STATE]
proof (chain)
picking this:
healthy (wp B)
healthy (wp C)
healthy (wp D)
sound S
\<guillemotleft> Q \<guillemotright> && (wp C S \<circ> \<phi>) \<tturnstile> wp D (S \<circ> \<phi>)
[PROOF STEP]
have "wp B (\<guillemotleft>Q\<guillemotright> && (wp C S o \<phi>)) \<tturnstile> wp B (wp D (S o \<phi>))"
[PROOF STATE]
proof (prove)
using this:
healthy (wp B)
healthy (wp C)
healthy (wp D)
sound S
\<guillemotleft> Q \<guillemotright> && (wp C S \<circ> \<phi>) \<tturnstile> wp D (S \<circ> \<phi>)

goal (1 subgoal):
 1. wp B (\<guillemotleft> Q \<guillemotright> && (wp C S \<circ> \<phi>)) \<tturnstile> wp B (wp D (S \<circ> \<phi>))
[PROOF STEP]
by(blast intro!:mono_transD)
[PROOF STATE]
proof (state)
this:
wp B (\<guillemotleft> Q \<guillemotright> && (wp C S \<circ> \<phi>)) \<tturnstile> wp B (wp D (S \<circ> \<phi>))

goal (1 subgoal):
 1. \<And>Pa Q. \<lbrakk>unitary Pa; unitary Q; Pa \<tturnstile> wp (A ;; C) Q\<rbrakk> \<Longrightarrow> \<guillemotleft> P \<guillemotright> && (Pa \<circ> \<phi>) \<tturnstile> wp (B ;; D) (Q \<circ> \<phi>)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
wp B (\<guillemotleft> Q \<guillemotright> && (wp C S \<circ> \<phi>)) \<tturnstile> wp B (wp D (S \<circ> \<phi>))

goal (1 subgoal):
 1. \<And>Pa Q. \<lbrakk>unitary Pa; unitary Q; Pa \<tturnstile> wp (A ;; C) Q\<rbrakk> \<Longrightarrow> \<guillemotleft> P \<guillemotright> && (Pa \<circ> \<phi>) \<tturnstile> wp (B ;; D) (Q \<circ> \<phi>)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
\<guillemotleft> P \<guillemotright> && (R \<circ> \<phi>) \<tturnstile> wp B (wp D (S \<circ> \<phi>))
[PROOF STEP]
show "\<guillemotleft>P\<guillemotright> && (R o \<phi>) \<tturnstile> wp (B;;D) (S o \<phi>)"
[PROOF STATE]
proof (prove)
using this:
\<guillemotleft> P \<guillemotright> && (R \<circ> \<phi>) \<tturnstile> wp B (wp D (S \<circ> \<phi>))

goal (1 subgoal):
 1. \<guillemotleft> P \<guillemotright> && (R \<circ> \<phi>) \<tturnstile> wp (B ;; D) (S \<circ> \<phi>)
[PROOF STEP]
unfolding wp_eval o_def
[PROOF STATE]
proof (prove)
using this:
\<guillemotleft> P \<guillemotright> && (\<lambda>x. R (\<phi> x)) \<tturnstile> wp B (wp D (\<lambda>x. S (\<phi> x)))

goal (1 subgoal):
 1. \<guillemotleft> P \<guillemotright> && (\<lambda>x. R (\<phi> x)) \<tturnstile> wp B (wp D (\<lambda>x. S (\<phi> x)))
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
\<guillemotleft> P \<guillemotright> && (R \<circ> \<phi>) \<tturnstile> wp (B ;; D) (S \<circ> \<phi>)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma dr_repeat:
  fixes \<phi> :: "'a \<Rightarrow> 'b"
  assumes dr_ab: "drefines \<phi> G a b"
      and Gpr:  "\<guillemotleft>G\<guillemotright> \<tturnstile> wp b \<guillemotleft>G\<guillemotright>"
      and wa:    "well_def a"
      and wb:    "well_def b"
  shows "drefines \<phi> G (repeat n a) (repeat n b)" (is "?X n")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. drefines \<phi> G (repeat n a) (repeat n b)
[PROOF STEP]
proof(induct n)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. drefines \<phi> G (repeat 0 a) (repeat 0 b)
 2. \<And>n. drefines \<phi> G (repeat n a) (repeat n b) \<Longrightarrow> drefines \<phi> G (repeat (Suc n) a) (repeat (Suc n) b)
[PROOF STEP]
show "?X 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. drefines \<phi> G (repeat 0 a) (repeat 0 b)
[PROOF STEP]
by(simp add:dr_Skip)
[PROOF STATE]
proof (state)
this:
drefines \<phi> G (repeat 0 a) (repeat 0 b)

goal (1 subgoal):
 1. \<And>n. drefines \<phi> G (repeat n a) (repeat n b) \<Longrightarrow> drefines \<phi> G (repeat (Suc n) a) (repeat (Suc n) b)
[PROOF STEP]
fix n
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n. drefines \<phi> G (repeat n a) (repeat n b) \<Longrightarrow> drefines \<phi> G (repeat (Suc n) a) (repeat (Suc n) b)
[PROOF STEP]
assume IH: "?X n"
[PROOF STATE]
proof (state)
this:
drefines \<phi> G (repeat n a) (repeat n b)

goal (1 subgoal):
 1. \<And>n. drefines \<phi> G (repeat n a) (repeat n b) \<Longrightarrow> drefines \<phi> G (repeat (Suc n) a) (repeat (Suc n) b)
[PROOF STEP]
thus "?X (Suc n)"
[PROOF STATE]
proof (prove)
using this:
drefines \<phi> G (repeat n a) (repeat n b)

goal (1 subgoal):
 1. drefines \<phi> G (repeat (Suc n) a) (repeat (Suc n) b)
[PROOF STEP]
by(auto intro!:dr_Seq Gpr assms wd_intros)
[PROOF STATE]
proof (state)
this:
drefines \<phi> G (repeat (Suc n) a) (repeat (Suc n) b)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma "Fr_1 \<F>' \<and> Fr_2 \<F>' \<and> Fr_4 \<F>'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Fr_1 \<F>' \<and> Fr_2 \<F>' \<and> Fr_4 \<F>'
[PROOF STEP]
by (simp add: Fr_1_def Fr_2_def Fr_4_def conn)


[STATEMENT]
lemma "Cl_1 \<C>' \<and> Cl_2 \<C>' \<and> Cl_4 \<C>'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Cl_1 \<C>' \<and> Cl_2 \<C>' \<and> Br_6 \<C>'
[PROOF STEP]
using ADDI_def CF2 IDEMb_def Cl_fr_def PC4
[PROOF STATE]
proof (prove)
using this:
Cl_1 ?\<phi> \<equiv> \<forall>A B w. ?\<phi> (A \<^bold>\<or> B) w = (?\<phi> A \<^bold>\<or> ?\<phi> B) w
Cl_2 (\<C>\<^sub>F ?\<phi>)
Cl_4' ?\<phi> \<equiv> \<forall>A. contains (?\<phi> A) (?\<phi> (?\<phi> A))
\<C>\<^sub>F ?\<F> \<equiv> \<lambda>A. A \<^bold>\<or> ?\<F> A
Cl_2 ?\<phi> \<Longrightarrow> Br_6 ?\<phi> = Cl_4' ?\<phi>

goal (1 subgoal):
 1. Cl_1 \<C>' \<and> Cl_2 \<C>' \<and> Br_6 \<C>'
[PROOF STEP]
unfolding conn
[PROOF STATE]
proof (prove)
using this:
Cl_1 ?\<phi> \<equiv> \<forall>A B w. ?\<phi> (\<lambda>w. A w \<or> B w) w = (?\<phi> A w \<or> ?\<phi> B w)
Cl_2 (\<C>\<^sub>F ?\<phi>)
Cl_4' ?\<phi> \<equiv> \<forall>A. contains (?\<phi> A) (?\<phi> (?\<phi> A))
\<C>\<^sub>F ?\<F> \<equiv> \<lambda>A w. A w \<or> ?\<F> A w
Cl_2 ?\<phi> \<Longrightarrow> Br_6 ?\<phi> = Cl_4' ?\<phi>

goal (1 subgoal):
 1. Cl_1 \<C>' \<and> Cl_2 \<C>' \<and> Br_6 \<C>'
[PROOF STEP]
by auto


[STATEMENT]
lemma "Fr_3 \<F>'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Fr_3 \<F>'
[PROOF STEP]
nitpick
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Fr_3 \<F>'
[PROOF STEP]
oops


[STATEMENT]
lemma "Cl_3 \<C>'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Fr_3 \<C>'
[PROOF STEP]
nitpick
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Fr_3 \<C>'
[PROOF STEP]
oops


[STATEMENT]
lemma "Fr_3 \<F>' \<Longrightarrow> \<forall>A. \<F>'(A) \<^bold>\<approx> \<^bold>\<bottom>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Fr_3 \<F>' \<Longrightarrow> \<forall>A w. Q w = \<^bold>\<bottom> w
[PROOF STEP]
by (simp add: NOR_def)


[STATEMENT]
lemma Q_def1: "\<forall>A. Q \<^bold>\<approx> \<^bold>\<not>A \<^bold>\<and> \<^bold>\<not>(\<^bold>\<not>A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>A w. Q w = (\<^bold>\<not> A \<^bold>\<and> \<C>' (\<I> (\<C>'\<^sup>c (\<I> (\<^bold>\<midarrow>A))))) w
[PROOF STEP]
using Cl_fr_def IF2 dEXP_def conn
[PROOF STATE]
proof (prove)
using this:
\<C>\<^sub>F ?\<F> \<equiv> \<lambda>A. A \<^bold>\<or> ?\<F> A
Int_2 (\<I>\<^sub>F ?\<phi>)
Int_2 ?\<phi> \<equiv> \<forall>A. contains A (?\<phi> A)
?A \<^bold>\<and> ?B \<equiv> \<lambda>w. ?A w \<and> ?B w
?A \<^bold>\<or> ?B \<equiv> \<lambda>w. ?A w \<or> ?B w
\<^bold>\<top> \<equiv> \<lambda>w. True
\<^bold>\<bottom> \<equiv> \<lambda>w. False
?A \<^bold>\<rightarrow> ?B \<equiv> \<lambda>w. ?B w \<longleftarrow> ?A w
?A \<^bold>\<leftrightarrow> ?B \<equiv> \<lambda>w. ?A w = ?B w
?A \<^bold>\<leftharpoonup> ?B \<equiv> \<lambda>w. ?A w \<and> \<sim>?B w
\<^bold>\<midarrow>?A \<equiv> \<lambda>w. \<sim>?A w
\<^bold>\<not>\<^sup>I ?A \<equiv> \<I> (\<^bold>\<midarrow>?A)
\<^bold>\<not>\<^sup>C ?A \<equiv> \<C> (\<^bold>\<midarrow>?A)
?\<beta> \<^bold>\<Leftarrow> ?\<alpha> \<equiv> \<I> (?\<alpha> \<^bold>\<rightarrow> ?\<beta>)

goal (1 subgoal):
 1. \<forall>A w. Q w = (\<^bold>\<not> A \<^bold>\<and> \<C>' (\<I> (\<C>'\<^sup>c (\<I> (\<^bold>\<midarrow>A))))) w
[PROOF STEP]
by auto


[STATEMENT]
lemma Q_def2: "Fr_1b \<F> \<Longrightarrow> \<forall>A. Q \<^bold>\<approx> \<^bold>\<not>(A \<^bold>\<or> \<^bold>\<not>A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Fr_1b \<F> \<Longrightarrow> \<forall>A w. Q w = \<C>' (\<I> ((\<^bold>\<or>) A\<^sup>c (\<^bold>\<not> A))) w
[PROOF STEP]
by (smt Cl_fr_def IF2 dEXP_def MONO_def monI conn)


[STATEMENT]
lemma neg_Idef: "\<forall>A. \<^bold>\<not>A \<^bold>\<approx> \<I>(\<^bold>\<midarrow>A) \<^bold>\<or> Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>A w. \<^bold>\<not> A w = (\<I> (\<^bold>\<midarrow>A) \<^bold>\<or> Q) w
[PROOF STEP]
by (simp add: Cl_fr_def)


[STATEMENT]
lemma neg_Cdef: "Fr_2 \<F> \<Longrightarrow> \<forall>A. \<^bold>\<not>A \<^bold>\<approx> \<C>(A) \<^bold>\<rightarrow> Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Fr_2 \<F> \<Longrightarrow> \<forall>A w. \<^bold>\<not> A w = (\<C> A \<^bold>\<rightarrow> Q) w
[PROOF STEP]
using Cl_fr_def Fr_2_def Int_fr_def conn
[PROOF STATE]
proof (prove)
using this:
\<C>\<^sub>F ?\<F> \<equiv> \<lambda>A. A \<^bold>\<or> ?\<F> A
Fr_2 ?\<phi> \<equiv> \<forall>A w. ?\<phi> A w = ?\<phi> (\<^bold>\<midarrow>A) w
\<I>\<^sub>F ?\<F> \<equiv> \<lambda>A. A \<^bold>\<leftharpoonup> ?\<F> A
?A \<^bold>\<and> ?B \<equiv> \<lambda>w. ?A w \<and> ?B w
?A \<^bold>\<or> ?B \<equiv> \<lambda>w. ?A w \<or> ?B w
\<^bold>\<top> \<equiv> \<lambda>w. True
\<^bold>\<bottom> \<equiv> \<lambda>w. False
?A \<^bold>\<rightarrow> ?B \<equiv> \<lambda>w. ?B w \<longleftarrow> ?A w
?A \<^bold>\<leftrightarrow> ?B \<equiv> \<lambda>w. ?A w = ?B w
?A \<^bold>\<leftharpoonup> ?B \<equiv> \<lambda>w. ?A w \<and> \<sim>?B w
\<^bold>\<midarrow>?A \<equiv> \<lambda>w. \<sim>?A w
\<^bold>\<not>\<^sup>I ?A \<equiv> \<I> (\<^bold>\<midarrow>?A)
\<^bold>\<not>\<^sup>C ?A \<equiv> \<C> (\<^bold>\<midarrow>?A)
?\<beta> \<^bold>\<Leftarrow> ?\<alpha> \<equiv> \<I> (?\<alpha> \<^bold>\<rightarrow> ?\<beta>)

goal (1 subgoal):
 1. Fr_2 \<F> \<Longrightarrow> \<forall>A w. \<^bold>\<not> A w = (\<C> A \<^bold>\<rightarrow> Q) w
[PROOF STEP]
by auto


[STATEMENT]
lemma "\<FF> \<F> \<Longrightarrow> TND \<^bold>\<not>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF> \<F> \<Longrightarrow> TND \<^bold>\<not>
[PROOF STEP]
nitpick
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF> \<F> \<Longrightarrow> TND \<^bold>\<not>
[PROOF STEP]
oops


[STATEMENT]
lemma "\<FF> \<F> \<Longrightarrow> TNDw \<^bold>\<not>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF> \<F> \<Longrightarrow> TNDw \<^bold>\<not>
[PROOF STEP]
nitpick
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF> \<F> \<Longrightarrow> TNDw \<^bold>\<not>
[PROOF STEP]
oops


[STATEMENT]
lemma "\<FF> \<F> \<Longrightarrow> TNDm \<^bold>\<not>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF> \<F> \<Longrightarrow> TNDm \<^bold>\<not>
[PROOF STEP]
nitpick
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF> \<F> \<Longrightarrow> TNDm \<^bold>\<not>
[PROOF STEP]
oops


[STATEMENT]
lemma ECQw: "ECQw \<^bold>\<not>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ECQw \<^bold>\<not>
[PROOF STEP]
using Cl_fr_def Disj_I ECQw_def
[PROOF STATE]
proof (prove)
using this:
\<C>\<^sub>F ?\<F> \<equiv> \<lambda>A. A \<^bold>\<or> ?\<F> A
\<forall>A w. (\<I> \<^bold>\<sqinter> compl) A w = \<^bold>\<bottom> w
ECQw ?\<eta> \<equiv> \<forall>a b. contains (?\<eta> b) (a \<^bold>\<and> ?\<eta> a)

goal (1 subgoal):
 1. ECQw \<^bold>\<not>
[PROOF STEP]
unfolding conn
[PROOF STATE]
proof (prove)
using this:
\<C>\<^sub>F ?\<F> \<equiv> \<lambda>A w. A w \<or> ?\<F> A w
\<forall>A w. (\<I> A w \<and> \<sim>A w) = False
ECQw ?\<eta> \<equiv> \<forall>a b. contains (?\<eta> b) (\<lambda>w. a w \<and> ?\<eta> a w)

goal (1 subgoal):
 1. ECQw (\<lambda>A. \<C>' (\<I> (\<lambda>w. \<sim>A w)))
[PROOF STEP]
by auto


[STATEMENT]
lemma ECQm: "ECQm \<^bold>\<not>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ECQm \<^bold>\<not>
[PROOF STEP]
using Cl_fr_def Disj_I ECQm_def
[PROOF STATE]
proof (prove)
using this:
\<C>\<^sub>F ?\<F> \<equiv> \<lambda>A. A \<^bold>\<or> ?\<F> A
\<forall>A w. (\<I> \<^bold>\<sqinter> compl) A w = \<^bold>\<bottom> w
ECQm ?\<eta> \<equiv> \<forall>a. contains (?\<eta> \<^bold>\<top>) (a \<^bold>\<and> ?\<eta> a)

goal (1 subgoal):
 1. ECQm \<^bold>\<not>
[PROOF STEP]
unfolding conn
[PROOF STATE]
proof (prove)
using this:
\<C>\<^sub>F ?\<F> \<equiv> \<lambda>A w. A w \<or> ?\<F> A w
\<forall>A w. (\<I> A w \<and> \<sim>A w) = False
ECQm ?\<eta> \<equiv> \<forall>a. contains (?\<eta> (\<lambda>w. True)) (\<lambda>w. a w \<and> ?\<eta> a w)

goal (1 subgoal):
 1. ECQm (\<lambda>A. \<C>' (\<I> (\<lambda>w. \<sim>A w)))
[PROOF STEP]
by auto


[STATEMENT]
lemma "\<FF> \<F> \<Longrightarrow> LNC \<^bold>\<not>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF> \<F> \<Longrightarrow> LNC \<^bold>\<not>
[PROOF STEP]
nitpick
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF> \<F> \<Longrightarrow> LNC \<^bold>\<not>
[PROOF STEP]
oops


[STATEMENT]
lemma "\<FF> \<F> \<Longrightarrow> DNI \<^bold>\<not>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF> \<F> \<Longrightarrow> DNI \<^bold>\<not>
[PROOF STEP]
nitpick
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF> \<F> \<Longrightarrow> DNI \<^bold>\<not>
[PROOF STEP]
oops


[STATEMENT]
lemma "\<FF> \<F> \<Longrightarrow> DNE \<^bold>\<not>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF> \<F> \<Longrightarrow> DNE \<^bold>\<not>
[PROOF STEP]
nitpick
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF> \<F> \<Longrightarrow> DNE \<^bold>\<not>
[PROOF STEP]
oops


[STATEMENT]
lemma CoPw: "Fr_1b \<F> \<Longrightarrow> CoPw \<^bold>\<not>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Fr_1b \<F> \<Longrightarrow> CoPw \<^bold>\<not>
[PROOF STEP]
using Cl_fr_def MONO_def monI
[PROOF STATE]
proof (prove)
using this:
\<C>\<^sub>F ?\<F> \<equiv> \<lambda>A. A \<^bold>\<or> ?\<F> A
MONO ?\<phi> \<equiv> \<forall>A. contains (\<lambda>B. contains (?\<phi> B) (?\<phi> A)) (\<lambda>B. contains B A)
Fr_1b \<F> \<Longrightarrow> MONO \<I>

goal (1 subgoal):
 1. Fr_1b \<F> \<Longrightarrow> CoPw \<^bold>\<not>
[PROOF STEP]
unfolding Defs conn
[PROOF STATE]
proof (prove)
using this:
\<C>\<^sub>F ?\<F> \<equiv> \<lambda>A w. A w \<or> ?\<F> A w
MONO ?\<phi> \<equiv> \<forall>A. contains (\<lambda>B. contains (?\<phi> B) (?\<phi> A)) (\<lambda>B. contains B A)
Fr_1b \<F> \<Longrightarrow> MONO \<I>

goal (1 subgoal):
 1. Fr_1b \<F> \<Longrightarrow> \<forall>a. contains (\<lambda>b. contains (\<C>' (\<I> (\<lambda>w. \<sim>a w))) (\<C>' (\<I> (\<lambda>w. \<sim>b w)))) (\<lambda>b. contains b a)
[PROOF STEP]
by smt


[STATEMENT]
lemma "\<FF> \<F> \<Longrightarrow> CoP1 \<^bold>\<not>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF> \<F> \<Longrightarrow> CoP1 \<^bold>\<not>
[PROOF STEP]
nitpick
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF> \<F> \<Longrightarrow> CoP1 \<^bold>\<not>
[PROOF STEP]
oops


[STATEMENT]
lemma "\<FF> \<F> \<Longrightarrow> CoP2 \<^bold>\<not>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF> \<F> \<Longrightarrow> CoP2 \<^bold>\<not>
[PROOF STEP]
nitpick
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF> \<F> \<Longrightarrow> CoP2 \<^bold>\<not>
[PROOF STEP]
oops


[STATEMENT]
lemma "\<FF> \<F> \<Longrightarrow> CoP3 \<^bold>\<not>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF> \<F> \<Longrightarrow> CoP3 \<^bold>\<not>
[PROOF STEP]
nitpick
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF> \<F> \<Longrightarrow> CoP3 \<^bold>\<not>
[PROOF STEP]
oops


[STATEMENT]
lemma "\<FF> \<F> \<Longrightarrow> XCoP \<^bold>\<not>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF> \<F> \<Longrightarrow> XCoP \<^bold>\<not>
[PROOF STEP]
nitpick
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF> \<F> \<Longrightarrow> XCoP \<^bold>\<not>
[PROOF STEP]
oops


[STATEMENT]
lemma "\<FF> \<F> \<Longrightarrow> DM3 \<^bold>\<not>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF> \<F> \<Longrightarrow> DM3 \<^bold>\<not>
[PROOF STEP]
nitpick
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF> \<F> \<Longrightarrow> DM3 \<^bold>\<not>
[PROOF STEP]
oops


[STATEMENT]
lemma Nor: "Fr_2 \<F> \<Longrightarrow> Fr_3 \<F> \<Longrightarrow> nNor \<^bold>\<not>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Fr_2 \<F>; Fr_3 \<F>\<rbrakk> \<Longrightarrow> nNor \<^bold>\<not>
[PROOF STEP]
using Cl_fr_def nNor_I nNor_def
[PROOF STATE]
proof (prove)
using this:
\<C>\<^sub>F ?\<F> \<equiv> \<lambda>A. A \<^bold>\<or> ?\<F> A
\<lbrakk>Fr_2 \<F>; Fr_3 \<F>\<rbrakk> \<Longrightarrow> nNor \<^bold>\<not>\<^sup>I
nNor ?\<eta> \<equiv> \<forall>w. ?\<eta> \<^bold>\<bottom> w = \<^bold>\<top> w

goal (1 subgoal):
 1. \<lbrakk>Fr_2 \<F>; Fr_3 \<F>\<rbrakk> \<Longrightarrow> nNor \<^bold>\<not>
[PROOF STEP]
unfolding conn
[PROOF STATE]
proof (prove)
using this:
\<C>\<^sub>F ?\<F> \<equiv> \<lambda>A w. A w \<or> ?\<F> A w
\<lbrakk>Fr_2 \<F>; Fr_3 \<F>\<rbrakk> \<Longrightarrow> nNor (\<lambda>A. \<I> (\<lambda>w. \<sim>A w))
nNor ?\<eta> \<equiv> \<forall>w. ?\<eta> (\<lambda>w. False) w = True

goal (1 subgoal):
 1. \<lbrakk>Fr_2 \<F>; Fr_3 \<F>\<rbrakk> \<Longrightarrow> nNor (\<lambda>A. \<C>' (\<I> (\<lambda>w. \<sim>A w)))
[PROOF STEP]
by auto


[STATEMENT]
lemma "\<FF> \<F> \<Longrightarrow> nDNor \<^bold>\<not>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF> \<F> \<Longrightarrow> nDNor \<^bold>\<not>
[PROOF STEP]
nitpick
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF> \<F> \<Longrightarrow> nDNor \<^bold>\<not>
[PROOF STEP]
oops


[STATEMENT]
lemma "\<FF> \<F> \<Longrightarrow> lCoPw(\<^bold>\<rightarrow>) \<^bold>\<not>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF> \<F> \<Longrightarrow> lCoPw (\<^bold>\<rightarrow>) \<^bold>\<not>
[PROOF STEP]
nitpick
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF> \<F> \<Longrightarrow> lCoPw (\<^bold>\<rightarrow>) \<^bold>\<not>
[PROOF STEP]
oops


[STATEMENT]
lemma "\<FF> \<F> \<Longrightarrow> lCoP1(\<^bold>\<rightarrow>) \<^bold>\<not>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF> \<F> \<Longrightarrow> lCoP1 (\<^bold>\<rightarrow>) \<^bold>\<not>
[PROOF STEP]
nitpick
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF> \<F> \<Longrightarrow> lCoP1 (\<^bold>\<rightarrow>) \<^bold>\<not>
[PROOF STEP]
oops


[STATEMENT]
lemma "\<FF> \<F> \<Longrightarrow> lCoP2(\<^bold>\<rightarrow>) \<^bold>\<not>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF> \<F> \<Longrightarrow> lCoP2 (\<^bold>\<rightarrow>) \<^bold>\<not>
[PROOF STEP]
nitpick
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF> \<F> \<Longrightarrow> lCoP2 (\<^bold>\<rightarrow>) \<^bold>\<not>
[PROOF STEP]
oops


[STATEMENT]
lemma "\<FF> \<F> \<Longrightarrow> lCoP3(\<^bold>\<rightarrow>) \<^bold>\<not>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF> \<F> \<Longrightarrow> lCoP3 (\<^bold>\<rightarrow>) \<^bold>\<not>
[PROOF STEP]
nitpick
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF> \<F> \<Longrightarrow> lCoP3 (\<^bold>\<rightarrow>) \<^bold>\<not>
[PROOF STEP]
oops


[STATEMENT]
lemma "\<FF> \<F> \<Longrightarrow> DS1(\<^bold>\<rightarrow>) \<^bold>\<not>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF> \<F> \<Longrightarrow> DS1 (\<^bold>\<rightarrow>) \<^bold>\<not>
[PROOF STEP]
nitpick
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF> \<F> \<Longrightarrow> DS1 (\<^bold>\<rightarrow>) \<^bold>\<not>
[PROOF STEP]
oops


[STATEMENT]
lemma "\<FF> \<F> \<Longrightarrow> DS2(\<^bold>\<rightarrow>) \<^bold>\<not>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF> \<F> \<Longrightarrow> DS2 (\<^bold>\<rightarrow>) \<^bold>\<not>
[PROOF STEP]
nitpick
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF> \<F> \<Longrightarrow> DS2 (\<^bold>\<rightarrow>) \<^bold>\<not>
[PROOF STEP]
oops


[STATEMENT]
lemma "DNI \<^bold>\<not> \<and> DNE \<^bold>\<not> \<longrightarrow> ECQ \<^bold>\<not>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ECQ \<^bold>\<not> \<longleftarrow> DNI \<^bold>\<not> \<and> DNE \<^bold>\<not>
[PROOF STEP]
using DNE_def ECQ_def Int_fr_def neg_Idef
[PROOF STATE]
proof (prove)
using this:
DNE ?\<eta> \<equiv> \<forall>a. contains a (?\<eta> (?\<eta> a))
ECQ ?\<eta> \<equiv> \<forall>a w. (a \<^bold>\<and> ?\<eta> a) w = \<^bold>\<bottom> w
\<I>\<^sub>F ?\<F> \<equiv> \<lambda>A. A \<^bold>\<leftharpoonup> ?\<F> A
\<forall>A w. \<^bold>\<not> A w = (\<I> (\<^bold>\<midarrow>A) \<^bold>\<or> Q) w

goal (1 subgoal):
 1. ECQ \<^bold>\<not> \<longleftarrow> DNI \<^bold>\<not> \<and> DNE \<^bold>\<not>
[PROOF STEP]
unfolding conn
[PROOF STATE]
proof (prove)
using this:
DNE ?\<eta> \<equiv> \<forall>a. contains a (?\<eta> (?\<eta> a))
ECQ ?\<eta> \<equiv> \<forall>a w. (a w \<and> ?\<eta> a w) = False
\<I>\<^sub>F ?\<F> \<equiv> \<lambda>A w. A w \<and> \<sim>?\<F> A w
\<forall>A w. \<C>' (\<I> (\<lambda>w. \<sim>A w)) w = (\<I> (\<lambda>w. \<sim>A w) w \<or> Q w)

goal (1 subgoal):
 1. ECQ (\<lambda>A. \<C>' (\<I> (\<lambda>w. \<sim>A w))) \<longleftarrow> DNI (\<lambda>A. \<C>' (\<I> (\<lambda>w. \<sim>A w))) \<and> DNE (\<lambda>A. \<C>' (\<I> (\<lambda>w. \<sim>A w)))
[PROOF STEP]
by (metis (no_types, lifting))


[STATEMENT]
lemma "\<sim>ECQ \<^bold>\<not> \<and> DM1 \<^bold>\<not> \<and> DM2 \<^bold>\<not> \<and> DM3 \<^bold>\<not> \<and> DM4 \<^bold>\<not> \<and> \<FF> \<F>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<sim>ECQ \<^bold>\<not> \<and> DM1 \<^bold>\<not> \<and> DM2 \<^bold>\<not> \<and> DM3 \<^bold>\<not> \<and> DM4 \<^bold>\<not> \<and> \<FF> \<F>
[PROOF STEP]
nitpick[satisfy,card w=3]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<sim>ECQ \<^bold>\<not> \<and> DM1 \<^bold>\<not> \<and> DM2 \<^bold>\<not> \<and> DM3 \<^bold>\<not> \<and> DM4 \<^bold>\<not> \<and> \<FF> \<F>
[PROOF STEP]
oops


[STATEMENT]
lemma "\<FF> \<F> \<Longrightarrow> \<forall>a b. (\<^bold>\<not>a \<^bold>\<Rightarrow> (a \<^bold>\<Rightarrow> b)) \<^bold>\<approx> \<^bold>\<top>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF> \<F> \<Longrightarrow> \<forall>a b w. ((b \<^bold>\<Leftarrow> a) \<^bold>\<Leftarrow> \<^bold>\<not> a) w = \<^bold>\<top> w
[PROOF STEP]
nitpick
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF> \<F> \<Longrightarrow> \<forall>a b w. ((b \<^bold>\<Leftarrow> a) \<^bold>\<Leftarrow> \<^bold>\<not> a) w = \<^bold>\<top> w
[PROOF STEP]
oops


[STATEMENT]
lemma "\<FF> \<F> \<Longrightarrow> \<forall>a b. (\<^bold>\<not>a \<^bold>\<rightarrow> (a \<^bold>\<rightarrow> b)) \<^bold>\<approx> \<^bold>\<top>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF> \<F> \<Longrightarrow> \<forall>a b w. (\<^bold>\<not> a \<^bold>\<rightarrow> a \<^bold>\<rightarrow> b) w = \<^bold>\<top> w
[PROOF STEP]
nitpick
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF> \<F> \<Longrightarrow> \<forall>a b w. (\<^bold>\<not> a \<^bold>\<rightarrow> a \<^bold>\<rightarrow> b) w = \<^bold>\<top> w
[PROOF STEP]
oops


[STATEMENT]
lemma "\<FF> \<F> \<Longrightarrow> \<forall>a b. (a \<^bold>\<and> \<^bold>\<not>a \<^bold>\<Rightarrow> b) \<^bold>\<approx> \<^bold>\<top>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF> \<F> \<Longrightarrow> \<forall>a b w. (b \<^bold>\<Leftarrow> a \<^bold>\<and> \<^bold>\<not> a) w = \<^bold>\<top> w
[PROOF STEP]
nitpick
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF> \<F> \<Longrightarrow> \<forall>a b w. (b \<^bold>\<Leftarrow> a \<^bold>\<and> \<^bold>\<not> a) w = \<^bold>\<top> w
[PROOF STEP]
oops


[STATEMENT]
lemma "\<FF> \<F> \<Longrightarrow> \<forall>a b. (a \<^bold>\<and> \<^bold>\<not>a \<^bold>\<rightarrow> b) \<^bold>\<approx> \<^bold>\<top>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF> \<F> \<Longrightarrow> \<forall>a b w. (a \<^bold>\<and> \<^bold>\<not> a \<^bold>\<rightarrow> b) w = \<^bold>\<top> w
[PROOF STEP]
nitpick
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF> \<F> \<Longrightarrow> \<forall>a b w. (a \<^bold>\<and> \<^bold>\<not> a \<^bold>\<rightarrow> b) w = \<^bold>\<top> w
[PROOF STEP]
oops


[STATEMENT]
lemma "\<FF> \<F> \<Longrightarrow> \<forall>a b. (a \<^bold>\<Rightarrow> (b \<^bold>\<or> \<^bold>\<not>b)) \<^bold>\<approx> \<^bold>\<top>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF> \<F> \<Longrightarrow> \<forall>a b w. (b \<^bold>\<or> \<^bold>\<not> b \<^bold>\<Leftarrow> a) w = \<^bold>\<top> w
[PROOF STEP]
nitpick
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF> \<F> \<Longrightarrow> \<forall>a b w. (b \<^bold>\<or> \<^bold>\<not> b \<^bold>\<Leftarrow> a) w = \<^bold>\<top> w
[PROOF STEP]
oops


[STATEMENT]
lemma "\<FF> \<F> \<Longrightarrow> \<forall>a b. (a \<^bold>\<rightarrow> (b \<^bold>\<or> \<^bold>\<not>b)) \<^bold>\<approx> \<^bold>\<top>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF> \<F> \<Longrightarrow> \<forall>a b w. (a \<^bold>\<rightarrow> b \<^bold>\<or> \<^bold>\<not> b) w = \<^bold>\<top> w
[PROOF STEP]
nitpick
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF> \<F> \<Longrightarrow> \<forall>a b w. (a \<^bold>\<rightarrow> b \<^bold>\<or> \<^bold>\<not> b) w = \<^bold>\<top> w
[PROOF STEP]
oops


[STATEMENT]
lemma "\<FF> \<F> \<Longrightarrow> \<forall>a. (a \<^bold>\<rightarrow> \<^bold>\<not>a) \<^bold>\<rightarrow> \<^bold>\<not>a \<^bold>\<approx> \<^bold>\<top>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF> \<F> \<Longrightarrow> \<forall>a w. ((a \<^bold>\<rightarrow> \<^bold>\<not> a) \<^bold>\<rightarrow> \<^bold>\<not> a) w = \<^bold>\<top> w
[PROOF STEP]
nitpick
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF> \<F> \<Longrightarrow> \<forall>a w. ((a \<^bold>\<rightarrow> \<^bold>\<not> a) \<^bold>\<rightarrow> \<^bold>\<not> a) w = \<^bold>\<top> w
[PROOF STEP]
oops


[STATEMENT]
lemma "\<FF> \<F> \<Longrightarrow> \<forall>a b. (a \<^bold>\<and> \<^bold>\<not>a) \<^bold>\<Rightarrow> b \<^bold>\<approx> \<^bold>\<top>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF> \<F> \<Longrightarrow> \<forall>a b w. (b \<^bold>\<Leftarrow> a \<^bold>\<and> \<^bold>\<not> a) w = \<^bold>\<top> w
[PROOF STEP]
nitpick
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF> \<F> \<Longrightarrow> \<forall>a b w. (b \<^bold>\<Leftarrow> a \<^bold>\<and> \<^bold>\<not> a) w = \<^bold>\<top> w
[PROOF STEP]
oops


[STATEMENT]
lemma "\<FF> \<F> \<Longrightarrow> \<forall>a b. (a \<^bold>\<and> \<^bold>\<not>a) \<^bold>\<rightarrow> b \<^bold>\<approx> \<^bold>\<top>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF> \<F> \<Longrightarrow> \<forall>a b w. (a \<^bold>\<and> \<^bold>\<not> a \<^bold>\<rightarrow> b) w = \<^bold>\<top> w
[PROOF STEP]
nitpick
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF> \<F> \<Longrightarrow> \<forall>a b w. (a \<^bold>\<and> \<^bold>\<not> a \<^bold>\<rightarrow> b) w = \<^bold>\<top> w
[PROOF STEP]
oops


[STATEMENT]
lemma "\<FF> \<F> \<Longrightarrow> \<forall>a b. a \<^bold>\<Rightarrow> (b \<^bold>\<or> \<^bold>\<not>b) \<^bold>\<approx> \<^bold>\<top>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF> \<F> \<Longrightarrow> \<forall>a b w. (b \<^bold>\<or> \<^bold>\<not> b \<^bold>\<Leftarrow> a) w = \<^bold>\<top> w
[PROOF STEP]
nitpick
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF> \<F> \<Longrightarrow> \<forall>a b w. (b \<^bold>\<or> \<^bold>\<not> b \<^bold>\<Leftarrow> a) w = \<^bold>\<top> w
[PROOF STEP]
oops


[STATEMENT]
lemma "\<FF> \<F> \<Longrightarrow> \<forall>a b. a \<^bold>\<rightarrow> (b \<^bold>\<or> \<^bold>\<not>b) \<^bold>\<approx> \<^bold>\<top>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF> \<F> \<Longrightarrow> \<forall>a b w. (a \<^bold>\<rightarrow> b \<^bold>\<or> \<^bold>\<not> b) w = \<^bold>\<top> w
[PROOF STEP]
nitpick
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF> \<F> \<Longrightarrow> \<forall>a b w. (a \<^bold>\<rightarrow> b \<^bold>\<or> \<^bold>\<not> b) w = \<^bold>\<top> w
[PROOF STEP]
oops


[STATEMENT]
lemma "\<FF> \<F> \<Longrightarrow> \<forall>a b. (a \<^bold>\<leftrightarrow> b) \<^bold>\<Rightarrow> (\<^bold>\<not>a \<^bold>\<leftrightarrow> \<^bold>\<not>b) \<^bold>\<approx> \<^bold>\<top>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF> \<F> \<Longrightarrow> \<forall>a b w. ((\<^bold>\<not> a \<^bold>\<leftrightarrow> \<^bold>\<not> b) \<^bold>\<Leftarrow> (a \<^bold>\<leftrightarrow> b)) w = \<^bold>\<top> w
[PROOF STEP]
nitpick
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF> \<F> \<Longrightarrow> \<forall>a b w. ((\<^bold>\<not> a \<^bold>\<leftrightarrow> \<^bold>\<not> b) \<^bold>\<Leftarrow> (a \<^bold>\<leftrightarrow> b)) w = \<^bold>\<top> w
[PROOF STEP]
oops


[STATEMENT]
lemma "\<FF> \<F> \<Longrightarrow> \<forall>a b. (a \<^bold>\<leftrightarrow> b) \<^bold>\<rightarrow> (\<^bold>\<not>a \<^bold>\<leftrightarrow> \<^bold>\<not>b) \<^bold>\<approx> \<^bold>\<top>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF> \<F> \<Longrightarrow> \<forall>a b w. ((a \<^bold>\<leftrightarrow> b) \<^bold>\<rightarrow> \<^bold>\<not> a \<^bold>\<leftrightarrow> \<^bold>\<not> b) w = \<^bold>\<top> w
[PROOF STEP]
nitpick
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF> \<F> \<Longrightarrow> \<forall>a b w. ((a \<^bold>\<leftrightarrow> b) \<^bold>\<rightarrow> \<^bold>\<not> a \<^bold>\<leftrightarrow> \<^bold>\<not> b) w = \<^bold>\<top> w
[PROOF STEP]
oops


[STATEMENT]
lemma "\<FF> \<F> \<Longrightarrow> \<forall>a b. (a \<^bold>\<Rightarrow> b) \<^bold>\<and> (a \<^bold>\<Rightarrow> \<^bold>\<not>b) \<^bold>\<Rightarrow> \<^bold>\<not>a \<^bold>\<approx> \<^bold>\<top>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF> \<F> \<Longrightarrow> \<forall>a b w. (\<^bold>\<not> a \<^bold>\<Leftarrow> ((\<^bold>\<Leftarrow>) b \<^bold>\<sqinter> (\<^bold>\<Leftarrow>) (\<^bold>\<not> b)) a) w = \<^bold>\<top> w
[PROOF STEP]
nitpick
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF> \<F> \<Longrightarrow> \<forall>a b w. (\<^bold>\<not> a \<^bold>\<Leftarrow> ((\<^bold>\<Leftarrow>) b \<^bold>\<sqinter> (\<^bold>\<Leftarrow>) (\<^bold>\<not> b)) a) w = \<^bold>\<top> w
[PROOF STEP]
oops


[STATEMENT]
lemma "\<FF> \<F> \<Longrightarrow> \<forall>a b. (a \<^bold>\<rightarrow> b) \<^bold>\<and> (a \<^bold>\<rightarrow> \<^bold>\<not>b) \<^bold>\<Rightarrow> \<^bold>\<not>a \<^bold>\<approx> \<^bold>\<top>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF> \<F> \<Longrightarrow> \<forall>a b w. (\<^bold>\<not> a \<^bold>\<Leftarrow> (a \<^bold>\<rightarrow> b) \<^bold>\<and> (a \<^bold>\<rightarrow> \<^bold>\<not> b)) w = \<^bold>\<top> w
[PROOF STEP]
nitpick
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF> \<F> \<Longrightarrow> \<forall>a b w. (\<^bold>\<not> a \<^bold>\<Leftarrow> (a \<^bold>\<rightarrow> b) \<^bold>\<and> (a \<^bold>\<rightarrow> \<^bold>\<not> b)) w = \<^bold>\<top> w
[PROOF STEP]
oops


[STATEMENT]
lemma "\<FF> \<F> \<Longrightarrow> \<forall>a. (\<^bold>\<not>a  \<^bold>\<Rightarrow>  \<^bold>\<bottom>) \<^bold>\<approx> \<^bold>\<top>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF> \<F> \<Longrightarrow> \<forall>a w. (\<^bold>\<bottom> \<^bold>\<Leftarrow> \<^bold>\<not> a) w = \<^bold>\<top> w
[PROOF STEP]
nitpick
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF> \<F> \<Longrightarrow> \<forall>a w. (\<^bold>\<bottom> \<^bold>\<Leftarrow> \<^bold>\<not> a) w = \<^bold>\<top> w
[PROOF STEP]
oops


[STATEMENT]
lemma "\<FF> \<F> \<Longrightarrow> \<forall>a. (\<^bold>\<not>a  \<^bold>\<rightarrow>  \<^bold>\<bottom>) \<^bold>\<approx> \<^bold>\<top>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF> \<F> \<Longrightarrow> \<forall>a w. (\<^bold>\<not> a \<^bold>\<rightarrow> \<^bold>\<bottom>) w = \<^bold>\<top> w
[PROOF STEP]
nitpick
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF> \<F> \<Longrightarrow> \<forall>a w. (\<^bold>\<not> a \<^bold>\<rightarrow> \<^bold>\<bottom>) w = \<^bold>\<top> w
[PROOF STEP]
oops


[STATEMENT]
lemma "\<FF> \<F> \<Longrightarrow> \<forall>a. (\<^bold>\<not>a \<^bold>\<Rightarrow> \<^bold>\<not>(\<^bold>\<not>\<^bold>\<top>)) \<^bold>\<approx> \<^bold>\<top>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF> \<F> \<Longrightarrow> \<forall>a w. (\<C>' (\<I> (\<C>'\<^sup>c (\<I> (\<^bold>\<midarrow>\<^bold>\<top>)))) \<^bold>\<Leftarrow> \<^bold>\<not> a) w = \<^bold>\<top> w
[PROOF STEP]
nitpick
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF> \<F> \<Longrightarrow> \<forall>a w. (\<C>' (\<I> (\<C>'\<^sup>c (\<I> (\<^bold>\<midarrow>\<^bold>\<top>)))) \<^bold>\<Leftarrow> \<^bold>\<not> a) w = \<^bold>\<top> w
[PROOF STEP]
oops


[STATEMENT]
lemma "\<FF> \<F> \<Longrightarrow> \<forall>a. (\<^bold>\<not>a \<^bold>\<rightarrow> \<^bold>\<not>(\<^bold>\<not>\<^bold>\<top>)) \<^bold>\<approx> \<^bold>\<top>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF> \<F> \<Longrightarrow> \<forall>a w. (\<^bold>\<not> a \<^bold>\<rightarrow> \<C>' (\<I> (\<C>'\<^sup>c (\<I> (\<^bold>\<midarrow>\<^bold>\<top>))))) w = \<^bold>\<top> w
[PROOF STEP]
nitpick
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF> \<F> \<Longrightarrow> \<forall>a w. (\<^bold>\<not> a \<^bold>\<rightarrow> \<C>' (\<I> (\<C>'\<^sup>c (\<I> (\<^bold>\<midarrow>\<^bold>\<top>))))) w = \<^bold>\<top> w
[PROOF STEP]
oops


[STATEMENT]
lemma "\<FF> \<F> \<Longrightarrow> \<forall>a. \<^bold>\<not>(\<^bold>\<not>(\<^bold>\<not>a)) \<^bold>\<Rightarrow> \<^bold>\<not>a \<^bold>\<approx> \<^bold>\<top>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF> \<F> \<Longrightarrow> \<forall>a w. (\<^bold>\<not> a \<^bold>\<Leftarrow> \<C>' (\<I> (\<C>'\<^sup>c (\<I> (\<C>'\<^sup>c (\<I> (\<^bold>\<midarrow>a))))))) w = \<^bold>\<top> w
[PROOF STEP]
nitpick
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF> \<F> \<Longrightarrow> \<forall>a w. (\<^bold>\<not> a \<^bold>\<Leftarrow> \<C>' (\<I> (\<C>'\<^sup>c (\<I> (\<C>'\<^sup>c (\<I> (\<^bold>\<midarrow>a))))))) w = \<^bold>\<top> w
[PROOF STEP]
oops


[STATEMENT]
lemma "\<FF> \<F> \<Longrightarrow> \<forall>a. \<^bold>\<not>(\<^bold>\<not>(\<^bold>\<not>a)) \<^bold>\<rightarrow> \<^bold>\<not>a \<^bold>\<approx> \<^bold>\<top>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF> \<F> \<Longrightarrow> \<forall>a w. (\<C>' (\<I> (\<C>'\<^sup>c (\<I> (\<C>'\<^sup>c (\<I> (\<^bold>\<midarrow>a)))))) \<^bold>\<rightarrow> \<^bold>\<not> a) w = \<^bold>\<top> w
[PROOF STEP]
nitpick
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF> \<F> \<Longrightarrow> \<forall>a w. (\<C>' (\<I> (\<C>'\<^sup>c (\<I> (\<C>'\<^sup>c (\<I> (\<^bold>\<midarrow>a)))))) \<^bold>\<rightarrow> \<^bold>\<not> a) w = \<^bold>\<top> w
[PROOF STEP]
oops


[STATEMENT]
lemma lCoPw: "Fr_1 \<F> \<Longrightarrow> Fr_2 \<F> \<Longrightarrow> Fr_3 \<F> \<Longrightarrow> Fr_4 \<F> \<Longrightarrow> lCoPw(\<^bold>\<Rightarrow>) \<^bold>\<not>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Fr_1 \<F>; Fr_2 \<F>; Fr_3 \<F>; Fr_4 \<F>\<rbrakk> \<Longrightarrow> lCoPw (\<^bold>\<Rightarrow>) \<^bold>\<not>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>Fr_1 \<F>; Fr_2 \<F>; Fr_3 \<F>; Fr_4 \<F>\<rbrakk> \<Longrightarrow> lCoPw (\<^bold>\<Rightarrow>) \<^bold>\<not>
[PROOF STEP]
assume fr1: "Fr_1 \<F>" and fr2: "Fr_2 \<F>" and fr3: "Fr_3 \<F>" and fr4: "Fr_4 \<F>"
[PROOF STATE]
proof (state)
this:
Fr_1 \<F>
Fr_2 \<F>
Fr_3 \<F>
Fr_4 \<F>

goal (1 subgoal):
 1. \<lbrakk>Fr_1 \<F>; Fr_2 \<F>; Fr_3 \<F>; Fr_4 \<F>\<rbrakk> \<Longrightarrow> lCoPw (\<^bold>\<Rightarrow>) \<^bold>\<not>
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
Fr_1 \<F>
Fr_2 \<F>
Fr_3 \<F>
Fr_4 \<F>

goal (1 subgoal):
 1. \<lbrakk>Fr_1 \<F>; Fr_2 \<F>; Fr_3 \<F>; Fr_4 \<F>\<rbrakk> \<Longrightarrow> lCoPw (\<^bold>\<Rightarrow>) \<^bold>\<not>
[PROOF STEP]
fix a b
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>Fr_1 \<F>; Fr_2 \<F>; Fr_3 \<F>; Fr_4 \<F>\<rbrakk> \<Longrightarrow> lCoPw (\<^bold>\<Rightarrow>) \<^bold>\<not>
[PROOF STEP]
from fr2
[PROOF STATE]
proof (chain)
picking this:
Fr_2 \<F>
[PROOF STEP]
have "\<^bold>\<not>b \<^bold>\<rightarrow> \<^bold>\<not>a \<^bold>\<approx> (\<C> a \<^bold>\<rightarrow> \<C> b) \<^bold>\<or> Q"
[PROOF STATE]
proof (prove)
using this:
Fr_2 \<F>

goal (1 subgoal):
 1. \<forall>w. (\<^bold>\<not> b \<^bold>\<rightarrow> \<^bold>\<not> a) w = ((\<C> a \<^bold>\<rightarrow> \<C> b) \<^bold>\<or> Q) w
[PROOF STEP]
using Cl_fr_def Fr_2_def Int_fr_def conn
[PROOF STATE]
proof (prove)
using this:
Fr_2 \<F>
\<C>\<^sub>F ?\<F> \<equiv> \<lambda>A. A \<^bold>\<or> ?\<F> A
Fr_2 ?\<phi> \<equiv> \<forall>A w. ?\<phi> A w = ?\<phi> (\<^bold>\<midarrow>A) w
\<I>\<^sub>F ?\<F> \<equiv> \<lambda>A. A \<^bold>\<leftharpoonup> ?\<F> A
?A \<^bold>\<and> ?B \<equiv> \<lambda>w. ?A w \<and> ?B w
?A \<^bold>\<or> ?B \<equiv> \<lambda>w. ?A w \<or> ?B w
\<^bold>\<top> \<equiv> \<lambda>w. True
\<^bold>\<bottom> \<equiv> \<lambda>w. False
?A \<^bold>\<rightarrow> ?B \<equiv> \<lambda>w. ?B w \<longleftarrow> ?A w
?A \<^bold>\<leftrightarrow> ?B \<equiv> \<lambda>w. ?A w = ?B w
?A \<^bold>\<leftharpoonup> ?B \<equiv> \<lambda>w. ?A w \<and> \<sim>?B w
\<^bold>\<midarrow>?A \<equiv> \<lambda>w. \<sim>?A w
\<^bold>\<not>\<^sup>I ?A \<equiv> \<I> (\<^bold>\<midarrow>?A)
\<^bold>\<not>\<^sup>C ?A \<equiv> \<C> (\<^bold>\<midarrow>?A)
?\<beta> \<^bold>\<Leftarrow> ?\<alpha> \<equiv> \<I> (?\<alpha> \<^bold>\<rightarrow> ?\<beta>)

goal (1 subgoal):
 1. \<forall>w. (\<^bold>\<not> b \<^bold>\<rightarrow> \<^bold>\<not> a) w = ((\<C> a \<^bold>\<rightarrow> \<C> b) \<^bold>\<or> Q) w
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>w. (\<^bold>\<not> b \<^bold>\<rightarrow> \<^bold>\<not> a) w = ((\<C> a \<^bold>\<rightarrow> \<C> b) \<^bold>\<or> Q) w

goal (1 subgoal):
 1. \<lbrakk>Fr_1 \<F>; Fr_2 \<F>; Fr_3 \<F>; Fr_4 \<F>\<rbrakk> \<Longrightarrow> lCoPw (\<^bold>\<Rightarrow>) \<^bold>\<not>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>w. (\<^bold>\<not> b \<^bold>\<rightarrow> \<^bold>\<not> a) w = ((\<C> a \<^bold>\<rightarrow> \<C> b) \<^bold>\<or> Q) w

goal (1 subgoal):
 1. \<lbrakk>Fr_1 \<F>; Fr_2 \<F>; Fr_3 \<F>; Fr_4 \<F>\<rbrakk> \<Longrightarrow> lCoPw (\<^bold>\<Rightarrow>) \<^bold>\<not>
[PROOF STEP]
from fr1 fr2 fr3
[PROOF STATE]
proof (chain)
picking this:
Fr_1 \<F>
Fr_2 \<F>
Fr_3 \<F>
[PROOF STEP]
have "\<I>(a \<^bold>\<rightarrow> b) \<^bold>\<preceq> \<C> a \<^bold>\<rightarrow> \<C> b"
[PROOF STATE]
proof (prove)
using this:
Fr_1 \<F>
Fr_2 \<F>
Fr_3 \<F>

goal (1 subgoal):
 1. contains (\<C> a \<^bold>\<rightarrow> \<C> b) (\<I> (a \<^bold>\<rightarrow> b))
[PROOF STEP]
using IC_imp
[PROOF STATE]
proof (prove)
using this:
Fr_1 \<F>
Fr_2 \<F>
Fr_3 \<F>
\<lbrakk>Fr_1 \<F>; Fr_2 \<F>; Fr_3 \<F>\<rbrakk> \<Longrightarrow> \<forall>A B. contains (\<C> A \<^bold>\<rightarrow> \<C> B) (\<I> (A \<^bold>\<rightarrow> B))

goal (1 subgoal):
 1. contains (\<C> a \<^bold>\<rightarrow> \<C> b) (\<I> (a \<^bold>\<rightarrow> b))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
contains (\<C> a \<^bold>\<rightarrow> \<C> b) (\<I> (a \<^bold>\<rightarrow> b))

goal (1 subgoal):
 1. \<lbrakk>Fr_1 \<F>; Fr_2 \<F>; Fr_3 \<F>; Fr_4 \<F>\<rbrakk> \<Longrightarrow> lCoPw (\<^bold>\<Rightarrow>) \<^bold>\<not>
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<forall>w. (\<^bold>\<not> b \<^bold>\<rightarrow> \<^bold>\<not> a) w = ((\<C> a \<^bold>\<rightarrow> \<C> b) \<^bold>\<or> Q) w
contains (\<C> a \<^bold>\<rightarrow> \<C> b) (\<I> (a \<^bold>\<rightarrow> b))
[PROOF STEP]
have "\<I>(a \<^bold>\<rightarrow> b) \<^bold>\<preceq> \<^bold>\<not>b \<^bold>\<rightarrow> \<^bold>\<not>a"
[PROOF STATE]
proof (prove)
using this:
\<forall>w. (\<^bold>\<not> b \<^bold>\<rightarrow> \<^bold>\<not> a) w = ((\<C> a \<^bold>\<rightarrow> \<C> b) \<^bold>\<or> Q) w
contains (\<C> a \<^bold>\<rightarrow> \<C> b) (\<I> (a \<^bold>\<rightarrow> b))

goal (1 subgoal):
 1. contains (\<^bold>\<not> b \<^bold>\<rightarrow> \<^bold>\<not> a) (\<I> (a \<^bold>\<rightarrow> b))
[PROOF STEP]
unfolding conn
[PROOF STATE]
proof (prove)
using this:
\<forall>w. (\<C>' (\<I> (\<lambda>w. \<sim>a w)) w \<longleftarrow> \<C>' (\<I> (\<lambda>w. \<sim>b w)) w) = ((\<C> b w \<longleftarrow> \<C> a w) \<or> Q w)
contains (\<lambda>w. \<C> b w \<longleftarrow> \<C> a w) (\<I> (\<lambda>w. b w \<longleftarrow> a w))

goal (1 subgoal):
 1. contains (\<lambda>w. \<C>' (\<I> (\<lambda>w. \<sim>a w)) w \<longleftarrow> \<C>' (\<I> (\<lambda>w. \<sim>b w)) w) (\<I> (\<lambda>w. b w \<longleftarrow> a w))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
contains (\<^bold>\<not> b \<^bold>\<rightarrow> \<^bold>\<not> a) (\<I> (a \<^bold>\<rightarrow> b))

goal (1 subgoal):
 1. \<lbrakk>Fr_1 \<F>; Fr_2 \<F>; Fr_3 \<F>; Fr_4 \<F>\<rbrakk> \<Longrightarrow> lCoPw (\<^bold>\<Rightarrow>) \<^bold>\<not>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
contains (\<^bold>\<not> b \<^bold>\<rightarrow> \<^bold>\<not> a) (\<I> (a \<^bold>\<rightarrow> b))

goal (1 subgoal):
 1. \<lbrakk>Fr_1 \<F>; Fr_2 \<F>; Fr_3 \<F>; Fr_4 \<F>\<rbrakk> \<Longrightarrow> lCoPw (\<^bold>\<Rightarrow>) \<^bold>\<not>
[PROOF STEP]
from fr1 fr2 fr4
[PROOF STATE]
proof (chain)
picking this:
Fr_1 \<F>
Fr_2 \<F>
Fr_4 \<F>
[PROOF STEP]
have "let A=(a \<^bold>\<rightarrow> b); B=(\<^bold>\<not>b \<^bold>\<rightarrow> \<^bold>\<not>a) in \<I> A \<^bold>\<preceq> B \<longrightarrow> \<I> A \<^bold>\<preceq> \<I> B"
[PROOF STATE]
proof (prove)
using this:
Fr_1 \<F>
Fr_2 \<F>
Fr_4 \<F>

goal (1 subgoal):
 1. let A = a \<^bold>\<rightarrow> b; B = \<^bold>\<not> b \<^bold>\<rightarrow> \<^bold>\<not> a in contains (\<I> B) (\<I> A) \<longleftarrow> contains B (\<I> A)
[PROOF STEP]
using PF1 MONO_MULTa IF1a IF4 PI9 Int_9_def
[PROOF STATE]
proof (prove)
using this:
Fr_1 \<F>
Fr_2 \<F>
Fr_4 \<F>
Fr_1 ?\<phi> = (Fr_1a ?\<phi> \<and> Fr_1b ?\<phi>)
MONO ?\<phi> = Int_1a ?\<phi>
Fr_1b ?\<phi> \<Longrightarrow> Int_1a (\<I>\<^sub>F ?\<phi>)
\<lbrakk>Fr_1a ?\<phi>; Fr_2 ?\<phi>; Fr_4 ?\<phi>\<rbrakk> \<Longrightarrow> Br_6 (\<I>\<^sub>F ?\<phi>)
\<lbrakk>Int_1a ?\<phi>; Br_6 ?\<phi>\<rbrakk> \<Longrightarrow> Int_9 ?\<phi>
Int_9 ?\<phi> \<equiv> \<forall>A. contains (\<lambda>B. contains (?\<phi> B) (?\<phi> A)) (\<lambda>B. contains B (?\<phi> A))

goal (1 subgoal):
 1. let A = a \<^bold>\<rightarrow> b; B = \<^bold>\<not> b \<^bold>\<rightarrow> \<^bold>\<not> a in contains (\<I> B) (\<I> A) \<longleftarrow> contains B (\<I> A)
[PROOF STEP]
by smt
[PROOF STATE]
proof (state)
this:
let A = a \<^bold>\<rightarrow> b; B = \<^bold>\<not> b \<^bold>\<rightarrow> \<^bold>\<not> a in contains (\<I> B) (\<I> A) \<longleftarrow> contains B (\<I> A)

goal (1 subgoal):
 1. \<lbrakk>Fr_1 \<F>; Fr_2 \<F>; Fr_3 \<F>; Fr_4 \<F>\<rbrakk> \<Longrightarrow> lCoPw (\<^bold>\<Rightarrow>) \<^bold>\<not>
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
contains (\<^bold>\<not> b \<^bold>\<rightarrow> \<^bold>\<not> a) (\<I> (a \<^bold>\<rightarrow> b))
let A = a \<^bold>\<rightarrow> b; B = \<^bold>\<not> b \<^bold>\<rightarrow> \<^bold>\<not> a in contains (\<I> B) (\<I> A) \<longleftarrow> contains B (\<I> A)
[PROOF STEP]
have "\<I>(a \<^bold>\<rightarrow> b) \<^bold>\<preceq> \<I>(\<^bold>\<not>b \<^bold>\<rightarrow> \<^bold>\<not>a)"
[PROOF STATE]
proof (prove)
using this:
contains (\<^bold>\<not> b \<^bold>\<rightarrow> \<^bold>\<not> a) (\<I> (a \<^bold>\<rightarrow> b))
let A = a \<^bold>\<rightarrow> b; B = \<^bold>\<not> b \<^bold>\<rightarrow> \<^bold>\<not> a in contains (\<I> B) (\<I> A) \<longleftarrow> contains B (\<I> A)

goal (1 subgoal):
 1. contains (\<I> (\<^bold>\<not> b \<^bold>\<rightarrow> \<^bold>\<not> a)) (\<I> (a \<^bold>\<rightarrow> b))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
contains (\<I> (\<^bold>\<not> b \<^bold>\<rightarrow> \<^bold>\<not> a)) (\<I> (a \<^bold>\<rightarrow> b))

goal (1 subgoal):
 1. \<lbrakk>Fr_1 \<F>; Fr_2 \<F>; Fr_3 \<F>; Fr_4 \<F>\<rbrakk> \<Longrightarrow> lCoPw (\<^bold>\<Rightarrow>) \<^bold>\<not>
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
contains (\<I> (\<^bold>\<not> ?b2 \<^bold>\<rightarrow> \<^bold>\<not> ?a2)) (\<I> (?a2 \<^bold>\<rightarrow> ?b2))

goal (1 subgoal):
 1. \<lbrakk>Fr_1 \<F>; Fr_2 \<F>; Fr_3 \<F>; Fr_4 \<F>\<rbrakk> \<Longrightarrow> lCoPw (\<^bold>\<Rightarrow>) \<^bold>\<not>
[PROOF STEP]
hence "lCoPw(\<^bold>\<Rightarrow>) \<^bold>\<not>"
[PROOF STATE]
proof (prove)
using this:
contains (\<I> (\<^bold>\<not> ?b2 \<^bold>\<rightarrow> \<^bold>\<not> ?a2)) (\<I> (?a2 \<^bold>\<rightarrow> ?b2))

goal (1 subgoal):
 1. lCoPw (\<^bold>\<Rightarrow>) \<^bold>\<not>
[PROOF STEP]
unfolding Defs conn
[PROOF STATE]
proof (prove)
using this:
contains (\<I> (\<lambda>w. \<C>' (\<I> (\<lambda>w. \<sim>?a2 w)) w \<longleftarrow> \<C>' (\<I> (\<lambda>w. \<sim>?b2 w)) w)) (\<I> (\<lambda>w. ?b2 w \<longleftarrow> ?a2 w))

goal (1 subgoal):
 1. \<forall>a b. contains (\<I> (\<lambda>w. \<C>' (\<I> (\<lambda>w. \<sim>a w)) w \<longleftarrow> \<C>' (\<I> (\<lambda>w. \<sim>b w)) w)) (\<I> (\<lambda>w. b w \<longleftarrow> a w))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
lCoPw (\<^bold>\<Rightarrow>) \<^bold>\<not>

goal (1 subgoal):
 1. \<lbrakk>Fr_1 \<F>; Fr_2 \<F>; Fr_3 \<F>; Fr_4 \<F>\<rbrakk> \<Longrightarrow> lCoPw (\<^bold>\<Rightarrow>) \<^bold>\<not>
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
lCoPw (\<^bold>\<Rightarrow>) \<^bold>\<not>

goal (1 subgoal):
 1. lCoPw (\<^bold>\<Rightarrow>) \<^bold>\<not>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
lCoPw (\<^bold>\<Rightarrow>) \<^bold>\<not>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma lCoPw_strict: "\<FF> \<F> \<Longrightarrow> \<forall>a b. (a \<^bold>\<Rightarrow> b) \<^bold>\<Rightarrow> (\<^bold>\<not>b \<^bold>\<Rightarrow> \<^bold>\<not>a) \<^bold>\<approx> \<^bold>\<top>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF> \<F> \<Longrightarrow> \<forall>a b w. ((\<^bold>\<not> a \<^bold>\<Leftarrow> \<^bold>\<not> b) \<^bold>\<Leftarrow> (b \<^bold>\<Leftarrow> a)) w = \<^bold>\<top> w
[PROOF STEP]
by (metis (no_types, lifting) DTw2 lCoPw lCoPw_def)


[STATEMENT]
lemma "\<FF> \<F> \<Longrightarrow> lCoP1(\<^bold>\<Rightarrow>) \<^bold>\<not>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF> \<F> \<Longrightarrow> lCoP1 (\<^bold>\<Rightarrow>) \<^bold>\<not>
[PROOF STEP]
nitpick
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF> \<F> \<Longrightarrow> lCoP1 (\<^bold>\<Rightarrow>) \<^bold>\<not>
[PROOF STEP]
oops


[STATEMENT]
lemma "\<FF> \<F> \<Longrightarrow> lCoP2(\<^bold>\<Rightarrow>) \<^bold>\<not>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF> \<F> \<Longrightarrow> lCoP2 (\<^bold>\<Rightarrow>) \<^bold>\<not>
[PROOF STEP]
nitpick
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF> \<F> \<Longrightarrow> lCoP2 (\<^bold>\<Rightarrow>) \<^bold>\<not>
[PROOF STEP]
oops


[STATEMENT]
lemma "\<FF> \<F> \<Longrightarrow> lCoP3(\<^bold>\<Rightarrow>) \<^bold>\<not>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF> \<F> \<Longrightarrow> lCoP3 (\<^bold>\<Rightarrow>) \<^bold>\<not>
[PROOF STEP]
nitpick
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF> \<F> \<Longrightarrow> lCoP3 (\<^bold>\<Rightarrow>) \<^bold>\<not>
[PROOF STEP]
oops


[STATEMENT]
lemma "\<FF> \<F> \<Longrightarrow> DS1(\<^bold>\<Rightarrow>) \<^bold>\<not>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF> \<F> \<Longrightarrow> DS1 (\<^bold>\<Rightarrow>) \<^bold>\<not>
[PROOF STEP]
nitpick
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF> \<F> \<Longrightarrow> DS1 (\<^bold>\<Rightarrow>) \<^bold>\<not>
[PROOF STEP]
oops


[STATEMENT]
lemma "\<FF> \<F> \<Longrightarrow> DS2(\<^bold>\<Rightarrow>) \<^bold>\<not>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF> \<F> \<Longrightarrow> DS2 (\<^bold>\<Rightarrow>) \<^bold>\<not>
[PROOF STEP]
nitpick
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF> \<F> \<Longrightarrow> DS2 (\<^bold>\<Rightarrow>) \<^bold>\<not>
[PROOF STEP]
oops


[STATEMENT]
lemma "\<FF> \<F> \<Longrightarrow> DS4(\<^bold>\<Rightarrow>) \<^bold>\<not>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF> \<F> \<Longrightarrow> DS4 (\<^bold>\<Rightarrow>) \<^bold>\<not>
[PROOF STEP]
nitpick
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF> \<F> \<Longrightarrow> DS4 (\<^bold>\<Rightarrow>) \<^bold>\<not>
[PROOF STEP]
oops


[STATEMENT]
lemma DNI_lCoP1: "Fr_1 \<F> \<Longrightarrow> Fr_2 \<F> \<Longrightarrow> Fr_3 \<F> \<Longrightarrow> Fr_4 \<F> \<Longrightarrow> DNI \<^bold>\<not> \<longrightarrow> lCoP1(\<^bold>\<Rightarrow>) \<^bold>\<not>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Fr_1 \<F>; Fr_2 \<F>; Fr_3 \<F>; Fr_4 \<F>\<rbrakk> \<Longrightarrow> lCoP1 (\<^bold>\<Rightarrow>) \<^bold>\<not> \<longleftarrow> DNI \<^bold>\<not>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>Fr_1 \<F>; Fr_2 \<F>; Fr_3 \<F>; Fr_4 \<F>\<rbrakk> \<Longrightarrow> lCoP1 (\<^bold>\<Rightarrow>) \<^bold>\<not> \<longleftarrow> DNI \<^bold>\<not>
[PROOF STEP]
assume fr1: "Fr_1 \<F>" and fr2: "Fr_2 \<F>" and fr3: "Fr_3 \<F>" and fr4: "Fr_4 \<F>"
[PROOF STATE]
proof (state)
this:
Fr_1 \<F>
Fr_2 \<F>
Fr_3 \<F>
Fr_4 \<F>

goal (1 subgoal):
 1. \<lbrakk>Fr_1 \<F>; Fr_2 \<F>; Fr_3 \<F>; Fr_4 \<F>\<rbrakk> \<Longrightarrow> lCoP1 (\<^bold>\<Rightarrow>) \<^bold>\<not> \<longleftarrow> DNI \<^bold>\<not>
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
Fr_1 \<F>
Fr_2 \<F>
Fr_3 \<F>
Fr_4 \<F>

goal (1 subgoal):
 1. \<lbrakk>Fr_1 \<F>; Fr_2 \<F>; Fr_3 \<F>; Fr_4 \<F>\<rbrakk> \<Longrightarrow> lCoP1 (\<^bold>\<Rightarrow>) \<^bold>\<not> \<longleftarrow> DNI \<^bold>\<not>
[PROOF STEP]
assume dni: "DNI \<^bold>\<not>"
[PROOF STATE]
proof (state)
this:
DNI \<^bold>\<not>

goal (1 subgoal):
 1. \<lbrakk>Fr_1 \<F>; Fr_2 \<F>; Fr_3 \<F>; Fr_4 \<F>\<rbrakk> \<Longrightarrow> lCoP1 (\<^bold>\<Rightarrow>) \<^bold>\<not> \<longleftarrow> DNI \<^bold>\<not>
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
DNI \<^bold>\<not>

goal (1 subgoal):
 1. \<lbrakk>Fr_1 \<F>; Fr_2 \<F>; Fr_3 \<F>; Fr_4 \<F>\<rbrakk> \<Longrightarrow> lCoP1 (\<^bold>\<Rightarrow>) \<^bold>\<not> \<longleftarrow> DNI \<^bold>\<not>
[PROOF STEP]
fix a b
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>Fr_1 \<F>; Fr_2 \<F>; Fr_3 \<F>; Fr_4 \<F>\<rbrakk> \<Longrightarrow> lCoP1 (\<^bold>\<Rightarrow>) \<^bold>\<not> \<longleftarrow> DNI \<^bold>\<not>
[PROOF STEP]
from fr1 fr2 fr3 fr4
[PROOF STATE]
proof (chain)
picking this:
Fr_1 \<F>
Fr_2 \<F>
Fr_3 \<F>
Fr_4 \<F>
[PROOF STEP]
have "lCoPw(\<^bold>\<Rightarrow>) \<^bold>\<not>"
[PROOF STATE]
proof (prove)
using this:
Fr_1 \<F>
Fr_2 \<F>
Fr_3 \<F>
Fr_4 \<F>

goal (1 subgoal):
 1. lCoPw (\<^bold>\<Rightarrow>) \<^bold>\<not>
[PROOF STEP]
using lCoPw
[PROOF STATE]
proof (prove)
using this:
Fr_1 \<F>
Fr_2 \<F>
Fr_3 \<F>
Fr_4 \<F>
\<lbrakk>Fr_1 \<F>; Fr_2 \<F>; Fr_3 \<F>; Fr_4 \<F>\<rbrakk> \<Longrightarrow> lCoPw (\<^bold>\<Rightarrow>) \<^bold>\<not>

goal (1 subgoal):
 1. lCoPw (\<^bold>\<Rightarrow>) \<^bold>\<not>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
lCoPw (\<^bold>\<Rightarrow>) \<^bold>\<not>

goal (1 subgoal):
 1. \<lbrakk>Fr_1 \<F>; Fr_2 \<F>; Fr_3 \<F>; Fr_4 \<F>\<rbrakk> \<Longrightarrow> lCoP1 (\<^bold>\<Rightarrow>) \<^bold>\<not> \<longleftarrow> DNI \<^bold>\<not>
[PROOF STEP]
hence 1: "a \<^bold>\<Rightarrow> \<^bold>\<not>b \<^bold>\<preceq> \<^bold>\<not>(\<^bold>\<not>b) \<^bold>\<Rightarrow> \<^bold>\<not>a"
[PROOF STATE]
proof (prove)
using this:
lCoPw (\<^bold>\<Rightarrow>) \<^bold>\<not>

goal (1 subgoal):
 1. contains (\<^bold>\<not> a \<^bold>\<Leftarrow> \<C>' (\<I> (\<C>'\<^sup>c (\<I> (\<^bold>\<midarrow>b))))) (\<^bold>\<not> b \<^bold>\<Leftarrow> a)
[PROOF STEP]
unfolding lCoPw_def
[PROOF STATE]
proof (prove)
using this:
\<forall>a b. contains (\<^bold>\<not> a \<^bold>\<Leftarrow> \<^bold>\<not> b) (b \<^bold>\<Leftarrow> a)

goal (1 subgoal):
 1. contains (\<^bold>\<not> a \<^bold>\<Leftarrow> \<C>' (\<I> (\<C>'\<^sup>c (\<I> (\<^bold>\<midarrow>b))))) (\<^bold>\<not> b \<^bold>\<Leftarrow> a)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
contains (\<^bold>\<not> a \<^bold>\<Leftarrow> \<C>' (\<I> (\<C>'\<^sup>c (\<I> (\<^bold>\<midarrow>b))))) (\<^bold>\<not> b \<^bold>\<Leftarrow> a)

goal (1 subgoal):
 1. \<lbrakk>Fr_1 \<F>; Fr_2 \<F>; Fr_3 \<F>; Fr_4 \<F>\<rbrakk> \<Longrightarrow> lCoP1 (\<^bold>\<Rightarrow>) \<^bold>\<not> \<longleftarrow> DNI \<^bold>\<not>
[PROOF STEP]
from fr1
[PROOF STATE]
proof (chain)
picking this:
Fr_1 \<F>
[PROOF STEP]
have 2: "let A=b; B=\<^bold>\<not>(\<^bold>\<not>b); C=\<^bold>\<not>a in A \<^bold>\<preceq> B \<longrightarrow>  \<I>(B \<^bold>\<rightarrow> C) \<^bold>\<preceq> \<I>(A \<^bold>\<rightarrow> C)"
[PROOF STATE]
proof (prove)
using this:
Fr_1 \<F>

goal (1 subgoal):
 1. let A = b; B = \<C>' (\<I> (\<C>'\<^sup>c (\<I> (\<^bold>\<midarrow>b)))); C = \<^bold>\<not> a in contains (\<I> (A \<^bold>\<rightarrow> C)) (\<I> (B \<^bold>\<rightarrow> C)) \<longleftarrow> contains B A
[PROOF STEP]
by (simp add: MONO_ant PF1 monI)
[PROOF STATE]
proof (state)
this:
let A = b; B = \<C>' (\<I> (\<C>'\<^sup>c (\<I> (\<^bold>\<midarrow>b)))); C = \<^bold>\<not> a in contains (\<I> (A \<^bold>\<rightarrow> C)) (\<I> (B \<^bold>\<rightarrow> C)) \<longleftarrow> contains B A

goal (1 subgoal):
 1. \<lbrakk>Fr_1 \<F>; Fr_2 \<F>; Fr_3 \<F>; Fr_4 \<F>\<rbrakk> \<Longrightarrow> lCoP1 (\<^bold>\<Rightarrow>) \<^bold>\<not> \<longleftarrow> DNI \<^bold>\<not>
[PROOF STEP]
from dni
[PROOF STATE]
proof (chain)
picking this:
DNI \<^bold>\<not>
[PROOF STEP]
have dnib: "b \<^bold>\<preceq> \<^bold>\<not>(\<^bold>\<not>b)"
[PROOF STATE]
proof (prove)
using this:
DNI \<^bold>\<not>

goal (1 subgoal):
 1. contains (\<C>' (\<I> (\<C>'\<^sup>c (\<I> (\<^bold>\<midarrow>b))))) b
[PROOF STEP]
unfolding DNI_def
[PROOF STATE]
proof (prove)
using this:
\<forall>a. contains (\<C>' (\<I> (\<C>'\<^sup>c (\<I> (\<^bold>\<midarrow>a))))) a

goal (1 subgoal):
 1. contains (\<C>' (\<I> (\<C>'\<^sup>c (\<I> (\<^bold>\<midarrow>b))))) b
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
contains (\<C>' (\<I> (\<C>'\<^sup>c (\<I> (\<^bold>\<midarrow>b))))) b

goal (1 subgoal):
 1. \<lbrakk>Fr_1 \<F>; Fr_2 \<F>; Fr_3 \<F>; Fr_4 \<F>\<rbrakk> \<Longrightarrow> lCoP1 (\<^bold>\<Rightarrow>) \<^bold>\<not> \<longleftarrow> DNI \<^bold>\<not>
[PROOF STEP]
from 1 2 dnib
[PROOF STATE]
proof (chain)
picking this:
contains (\<^bold>\<not> a \<^bold>\<Leftarrow> \<C>' (\<I> (\<C>'\<^sup>c (\<I> (\<^bold>\<midarrow>b))))) (\<^bold>\<not> b \<^bold>\<Leftarrow> a)
let A = b; B = \<C>' (\<I> (\<C>'\<^sup>c (\<I> (\<^bold>\<midarrow>b)))); C = \<^bold>\<not> a in contains (\<I> (A \<^bold>\<rightarrow> C)) (\<I> (B \<^bold>\<rightarrow> C)) \<longleftarrow> contains B A
contains (\<C>' (\<I> (\<C>'\<^sup>c (\<I> (\<^bold>\<midarrow>b))))) b
[PROOF STEP]
have "a \<^bold>\<Rightarrow> \<^bold>\<not>b \<^bold>\<preceq> b \<^bold>\<Rightarrow> \<^bold>\<not>a"
[PROOF STATE]
proof (prove)
using this:
contains (\<^bold>\<not> a \<^bold>\<Leftarrow> \<C>' (\<I> (\<C>'\<^sup>c (\<I> (\<^bold>\<midarrow>b))))) (\<^bold>\<not> b \<^bold>\<Leftarrow> a)
let A = b; B = \<C>' (\<I> (\<C>'\<^sup>c (\<I> (\<^bold>\<midarrow>b)))); C = \<^bold>\<not> a in contains (\<I> (A \<^bold>\<rightarrow> C)) (\<I> (B \<^bold>\<rightarrow> C)) \<longleftarrow> contains B A
contains (\<C>' (\<I> (\<C>'\<^sup>c (\<I> (\<^bold>\<midarrow>b))))) b

goal (1 subgoal):
 1. contains (\<^bold>\<not> a \<^bold>\<Leftarrow> b) (\<^bold>\<not> b \<^bold>\<Leftarrow> a)
[PROOF STEP]
unfolding conn
[PROOF STATE]
proof (prove)
using this:
contains (\<I> (\<lambda>w. \<C>' (\<I> (\<lambda>w. \<sim>a w)) w \<longleftarrow> \<C>' (\<I> (\<lambda>w. \<sim>\<C>' (\<I> (\<lambda>w. \<sim>b w)) w)) w)) (\<I> (\<lambda>w. \<C>' (\<I> (\<lambda>w. \<sim>b w)) w \<longleftarrow> a w))
let A = b; B = \<C>' (\<I> (\<lambda>w. \<sim>\<C>' (\<I> (\<lambda>w. \<sim>b w)) w)); C = \<C>' (\<I> (\<lambda>w. \<sim>a w)) in contains (\<I> (\<lambda>w. C w \<longleftarrow> A w)) (\<I> (\<lambda>w. C w \<longleftarrow> B w)) \<longleftarrow> contains B A
contains (\<C>' (\<I> (\<lambda>w. \<sim>\<C>' (\<I> (\<lambda>w. \<sim>b w)) w))) b

goal (1 subgoal):
 1. contains (\<I> (\<lambda>w. \<C>' (\<I> (\<lambda>w. \<sim>a w)) w \<longleftarrow> b w)) (\<I> (\<lambda>w. \<C>' (\<I> (\<lambda>w. \<sim>b w)) w \<longleftarrow> a w))
[PROOF STEP]
by meson
[PROOF STATE]
proof (state)
this:
contains (\<^bold>\<not> a \<^bold>\<Leftarrow> b) (\<^bold>\<not> b \<^bold>\<Leftarrow> a)

goal (1 subgoal):
 1. \<lbrakk>Fr_1 \<F>; Fr_2 \<F>; Fr_3 \<F>; Fr_4 \<F>\<rbrakk> \<Longrightarrow> lCoP1 (\<^bold>\<Rightarrow>) \<^bold>\<not> \<longleftarrow> DNI \<^bold>\<not>
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
contains (\<^bold>\<not> ?a2 \<^bold>\<Leftarrow> ?b2) (\<^bold>\<not> ?b2 \<^bold>\<Leftarrow> ?a2)

goal (1 subgoal):
 1. \<lbrakk>Fr_1 \<F>; Fr_2 \<F>; Fr_3 \<F>; Fr_4 \<F>\<rbrakk> \<Longrightarrow> lCoP1 (\<^bold>\<Rightarrow>) \<^bold>\<not> \<longleftarrow> DNI \<^bold>\<not>
[PROOF STEP]
hence "lCoP1(\<^bold>\<Rightarrow>) \<^bold>\<not>"
[PROOF STATE]
proof (prove)
using this:
contains (\<^bold>\<not> ?a2 \<^bold>\<Leftarrow> ?b2) (\<^bold>\<not> ?b2 \<^bold>\<Leftarrow> ?a2)

goal (1 subgoal):
 1. lCoP1 (\<^bold>\<Rightarrow>) \<^bold>\<not>
[PROOF STEP]
unfolding Defs
[PROOF STATE]
proof (prove)
using this:
contains (\<^bold>\<not> ?a2 \<^bold>\<Leftarrow> ?b2) (\<^bold>\<not> ?b2 \<^bold>\<Leftarrow> ?a2)

goal (1 subgoal):
 1. \<forall>a b. contains (\<^bold>\<not> a \<^bold>\<Leftarrow> b) (\<^bold>\<not> b \<^bold>\<Leftarrow> a)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
lCoP1 (\<^bold>\<Rightarrow>) \<^bold>\<not>

goal (1 subgoal):
 1. \<lbrakk>Fr_1 \<F>; Fr_2 \<F>; Fr_3 \<F>; Fr_4 \<F>\<rbrakk> \<Longrightarrow> lCoP1 (\<^bold>\<Rightarrow>) \<^bold>\<not> \<longleftarrow> DNI \<^bold>\<not>
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
DNI \<^bold>\<not> \<Longrightarrow> lCoP1 (\<^bold>\<Rightarrow>) \<^bold>\<not>

goal (1 subgoal):
 1. \<lbrakk>Fr_1 \<F>; Fr_2 \<F>; Fr_3 \<F>; Fr_4 \<F>\<rbrakk> \<Longrightarrow> lCoP1 (\<^bold>\<Rightarrow>) \<^bold>\<not> \<longleftarrow> DNI \<^bold>\<not>
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
DNI \<^bold>\<not> \<Longrightarrow> lCoP1 (\<^bold>\<Rightarrow>) \<^bold>\<not>

goal (1 subgoal):
 1. lCoP1 (\<^bold>\<Rightarrow>) \<^bold>\<not> \<longleftarrow> DNI \<^bold>\<not>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
lCoP1 (\<^bold>\<Rightarrow>) \<^bold>\<not> \<longleftarrow> DNI \<^bold>\<not>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma CoP1_LNC: "CoP1 \<^bold>\<not> \<Longrightarrow> LNC \<^bold>\<not>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. CoP1 \<^bold>\<not> \<Longrightarrow> LNC \<^bold>\<not>
[PROOF STEP]
using CoP1_def ECQm_def LNC_def  Cl_fr_def Disj_I ECQm_def
[PROOF STATE]
proof (prove)
using this:
CoP1 ?\<eta> \<equiv> \<forall>a. contains (contains (?\<eta> a)) (\<lambda>b. contains (?\<eta> b) a)
ECQm ?\<eta> \<equiv> \<forall>a. contains (?\<eta> \<^bold>\<top>) (a \<^bold>\<and> ?\<eta> a)
LNC ?\<eta> \<equiv> \<forall>a w. ?\<eta> (a \<^bold>\<and> ?\<eta> a) w = \<^bold>\<top> w
\<C>\<^sub>F ?\<F> \<equiv> \<lambda>A. A \<^bold>\<or> ?\<F> A
\<forall>A w. (\<I> \<^bold>\<sqinter> compl) A w = \<^bold>\<bottom> w
ECQm ?\<eta> \<equiv> \<forall>a. contains (?\<eta> \<^bold>\<top>) (a \<^bold>\<and> ?\<eta> a)

goal (1 subgoal):
 1. CoP1 \<^bold>\<not> \<Longrightarrow> LNC \<^bold>\<not>
[PROOF STEP]
unfolding conn
[PROOF STATE]
proof (prove)
using this:
CoP1 ?\<eta> \<equiv> \<forall>a. contains (contains (?\<eta> a)) (\<lambda>b. contains (?\<eta> b) a)
ECQm ?\<eta> \<equiv> \<forall>a. contains (?\<eta> (\<lambda>w. True)) (\<lambda>w. a w \<and> ?\<eta> a w)
LNC ?\<eta> \<equiv> \<forall>a w. ?\<eta> (\<lambda>w. a w \<and> ?\<eta> a w) w = True
\<C>\<^sub>F ?\<F> \<equiv> \<lambda>A w. A w \<or> ?\<F> A w
\<forall>A w. (\<I> A w \<and> \<sim>A w) = False
ECQm ?\<eta> \<equiv> \<forall>a. contains (?\<eta> (\<lambda>w. True)) (\<lambda>w. a w \<and> ?\<eta> a w)

goal (1 subgoal):
 1. CoP1 (\<lambda>A. \<C>' (\<I> (\<lambda>w. \<sim>A w))) \<Longrightarrow> LNC (\<lambda>A. \<C>' (\<I> (\<lambda>w. \<sim>A w)))
[PROOF STEP]
by smt


[STATEMENT]
lemma DNI_LNC: "Fr_1b \<F> \<Longrightarrow> DNI \<^bold>\<not> \<Longrightarrow> LNC \<^bold>\<not>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Fr_1b \<F>; DNI \<^bold>\<not>\<rbrakk> \<Longrightarrow> LNC \<^bold>\<not>
[PROOF STEP]
by (simp add: CoP1_LNC DNI_CoP1)


[STATEMENT]
lemma MT: "Fr_1 \<F> \<Longrightarrow> Fr_2 \<F> \<Longrightarrow> Fr_3 \<F> \<Longrightarrow> \<forall>a b. (a \<^bold>\<Rightarrow> b) \<^bold>\<and> \<^bold>\<not>b \<^bold>\<preceq> \<^bold>\<not>a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Fr_1 \<F>; Fr_2 \<F>; Fr_3 \<F>\<rbrakk> \<Longrightarrow> \<forall>a b. contains (\<^bold>\<not> a) ((b \<^bold>\<Leftarrow> a) \<^bold>\<and> \<^bold>\<not> b)
[PROOF STEP]
using Cl_fr_def Fr_2_def IC_imp Int_fr_def
[PROOF STATE]
proof (prove)
using this:
\<C>\<^sub>F ?\<F> \<equiv> \<lambda>A. A \<^bold>\<or> ?\<F> A
Fr_2 ?\<phi> \<equiv> \<forall>A w. ?\<phi> A w = ?\<phi> (\<^bold>\<midarrow>A) w
\<lbrakk>Fr_1 \<F>; Fr_2 \<F>; Fr_3 \<F>\<rbrakk> \<Longrightarrow> \<forall>A B. contains (\<C> A \<^bold>\<rightarrow> \<C> B) (\<I> (A \<^bold>\<rightarrow> B))
\<I>\<^sub>F ?\<F> \<equiv> \<lambda>A. A \<^bold>\<leftharpoonup> ?\<F> A

goal (1 subgoal):
 1. \<lbrakk>Fr_1 \<F>; Fr_2 \<F>; Fr_3 \<F>\<rbrakk> \<Longrightarrow> \<forall>a b. contains (\<^bold>\<not> a) ((b \<^bold>\<Leftarrow> a) \<^bold>\<and> \<^bold>\<not> b)
[PROOF STEP]
unfolding conn
[PROOF STATE]
proof (prove)
using this:
\<C>\<^sub>F ?\<F> \<equiv> \<lambda>A w. A w \<or> ?\<F> A w
Fr_2 ?\<phi> \<equiv> \<forall>A w. ?\<phi> A w = ?\<phi> (\<lambda>w. \<sim>A w) w
\<lbrakk>Fr_1 \<F>; Fr_2 \<F>; Fr_3 \<F>\<rbrakk> \<Longrightarrow> \<forall>A B. contains (\<lambda>w. \<C> B w \<longleftarrow> \<C> A w) (\<I> (\<lambda>w. B w \<longleftarrow> A w))
\<I>\<^sub>F ?\<F> \<equiv> \<lambda>A w. A w \<and> \<sim>?\<F> A w

goal (1 subgoal):
 1. \<lbrakk>Fr_1 \<F>; Fr_2 \<F>; Fr_3 \<F>\<rbrakk> \<Longrightarrow> \<forall>a b. contains (\<C>' (\<I> (\<lambda>w. \<sim>a w))) (\<lambda>w. \<I> (\<lambda>w. b w \<longleftarrow> a w) w \<and> \<C>' (\<I> (\<lambda>w. \<sim>b w)) w)
[PROOF STEP]
by metis


[STATEMENT]
lemma MT': "Fr_1 \<F> \<Longrightarrow> Fr_2 \<F> \<Longrightarrow> Fr_3 \<F> \<Longrightarrow> \<forall>a b. ((a \<^bold>\<Rightarrow> b) \<^bold>\<and> \<^bold>\<not>b) \<^bold>\<Rightarrow> \<^bold>\<not>a \<^bold>\<approx> \<^bold>\<top>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Fr_1 \<F>; Fr_2 \<F>; Fr_3 \<F>\<rbrakk> \<Longrightarrow> \<forall>a b w. (\<^bold>\<not> a \<^bold>\<Leftarrow> (b \<^bold>\<Leftarrow> a) \<^bold>\<and> \<^bold>\<not> b) w = \<^bold>\<top> w
[PROOF STEP]
by (simp add: DTw2 MT)


[STATEMENT]
lemma "JML \<Longrightarrow> TND \<^bold>\<not>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (SML3 \<and> Fr_2 \<F> \<and> Fr_3 \<F> \<and> Fr_4 \<F>) \<and> DNI \<^bold>\<not> \<Longrightarrow> TND \<^bold>\<not>
[PROOF STEP]
nitpick
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (SML3 \<and> Fr_2 \<F> \<and> Fr_3 \<F> \<and> Fr_4 \<F>) \<and> DNI \<^bold>\<not> \<Longrightarrow> TND \<^bold>\<not>
[PROOF STEP]
oops


[STATEMENT]
lemma "JML \<Longrightarrow> TNDw \<^bold>\<not>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (SML3 \<and> Fr_2 \<F> \<and> Fr_3 \<F> \<and> Fr_4 \<F>) \<and> DNI \<^bold>\<not> \<Longrightarrow> TNDw \<^bold>\<not>
[PROOF STEP]
nitpick
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (SML3 \<and> Fr_2 \<F> \<and> Fr_3 \<F> \<and> Fr_4 \<F>) \<and> DNI \<^bold>\<not> \<Longrightarrow> TNDw \<^bold>\<not>
[PROOF STEP]
oops


[STATEMENT]
lemma "JML \<Longrightarrow> TNDm \<^bold>\<not>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (SML3 \<and> Fr_2 \<F> \<and> Fr_3 \<F> \<and> Fr_4 \<F>) \<and> DNI \<^bold>\<not> \<Longrightarrow> TNDm \<^bold>\<not>
[PROOF STEP]
nitpick
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (SML3 \<and> Fr_2 \<F> \<and> Fr_3 \<F> \<and> Fr_4 \<F>) \<and> DNI \<^bold>\<not> \<Longrightarrow> TNDm \<^bold>\<not>
[PROOF STEP]
oops


[STATEMENT]
lemma "JML \<Longrightarrow> ECQ \<^bold>\<not>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (SML3 \<and> Fr_2 \<F> \<and> Fr_3 \<F> \<and> Fr_4 \<F>) \<and> DNI \<^bold>\<not> \<Longrightarrow> ECQ \<^bold>\<not>
[PROOF STEP]
nitpick
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (SML3 \<and> Fr_2 \<F> \<and> Fr_3 \<F> \<and> Fr_4 \<F>) \<and> DNI \<^bold>\<not> \<Longrightarrow> ECQ \<^bold>\<not>
[PROOF STEP]
oops


[STATEMENT]
lemma "ECQw \<^bold>\<not>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ECQw \<^bold>\<not>
[PROOF STEP]
using Cl_fr_def Disj_I ECQw_def
[PROOF STATE]
proof (prove)
using this:
\<C>\<^sub>F ?\<F> \<equiv> \<lambda>A. A \<^bold>\<or> ?\<F> A
\<forall>A w. (\<I> \<^bold>\<sqinter> compl) A w = \<^bold>\<bottom> w
ECQw ?\<eta> \<equiv> \<forall>a b. contains (?\<eta> b) (a \<^bold>\<and> ?\<eta> a)

goal (1 subgoal):
 1. ECQw \<^bold>\<not>
[PROOF STEP]
unfolding conn
[PROOF STATE]
proof (prove)
using this:
\<C>\<^sub>F ?\<F> \<equiv> \<lambda>A w. A w \<or> ?\<F> A w
\<forall>A w. (\<I> A w \<and> \<sim>A w) = False
ECQw ?\<eta> \<equiv> \<forall>a b. contains (?\<eta> b) (\<lambda>w. a w \<and> ?\<eta> a w)

goal (1 subgoal):
 1. ECQw (\<lambda>A. \<C>' (\<I> (\<lambda>w. \<sim>A w)))
[PROOF STEP]
by auto


[STATEMENT]
lemma "ECQm \<^bold>\<not>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ECQm \<^bold>\<not>
[PROOF STEP]
using Cl_fr_def Disj_I ECQm_def
[PROOF STATE]
proof (prove)
using this:
\<C>\<^sub>F ?\<F> \<equiv> \<lambda>A. A \<^bold>\<or> ?\<F> A
\<forall>A w. (\<I> \<^bold>\<sqinter> compl) A w = \<^bold>\<bottom> w
ECQm ?\<eta> \<equiv> \<forall>a. contains (?\<eta> \<^bold>\<top>) (a \<^bold>\<and> ?\<eta> a)

goal (1 subgoal):
 1. ECQm \<^bold>\<not>
[PROOF STEP]
unfolding conn
[PROOF STATE]
proof (prove)
using this:
\<C>\<^sub>F ?\<F> \<equiv> \<lambda>A w. A w \<or> ?\<F> A w
\<forall>A w. (\<I> A w \<and> \<sim>A w) = False
ECQm ?\<eta> \<equiv> \<forall>a. contains (?\<eta> (\<lambda>w. True)) (\<lambda>w. a w \<and> ?\<eta> a w)

goal (1 subgoal):
 1. ECQm (\<lambda>A. \<C>' (\<I> (\<lambda>w. \<sim>A w)))
[PROOF STEP]
by auto


[STATEMENT]
lemma "JML \<Longrightarrow> LNC \<^bold>\<not>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (SML3 \<and> Fr_2 \<F> \<and> Fr_3 \<F> \<and> Fr_4 \<F>) \<and> DNI \<^bold>\<not> \<Longrightarrow> LNC \<^bold>\<not>
[PROOF STEP]
using DNI_LNC PF1
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>SML4; DNI \<^bold>\<not>\<rbrakk> \<Longrightarrow> LNC \<^bold>\<not>
Fr_1 ?\<phi> = (Fr_1a ?\<phi> \<and> Fr_1b ?\<phi>)

goal (1 subgoal):
 1. (SML3 \<and> Fr_2 \<F> \<and> Fr_3 \<F> \<and> Fr_4 \<F>) \<and> DNI \<^bold>\<not> \<Longrightarrow> LNC \<^bold>\<not>
[PROOF STEP]
by blast


[STATEMENT]
lemma "SML1 \<Longrightarrow> LNC \<^bold>\<not>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. SML3 \<and> Fr_2 \<F> \<and> Fr_3 \<F> \<and> Fr_4 \<F> \<Longrightarrow> LNC \<^bold>\<not>
[PROOF STEP]
nitpick
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. SML3 \<and> Fr_2 \<F> \<and> Fr_3 \<F> \<and> Fr_4 \<F> \<Longrightarrow> LNC \<^bold>\<not>
[PROOF STEP]
oops


[STATEMENT]
lemma "JML \<Longrightarrow> DNI \<^bold>\<not>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (SML3 \<and> Fr_2 \<F> \<and> Fr_3 \<F> \<and> Fr_4 \<F>) \<and> DNI \<^bold>\<not> \<Longrightarrow> DNI \<^bold>\<not>
[PROOF STEP]
using CoP1_def2
[PROOF STATE]
proof (prove)
using this:
CoP1 ?\<eta> = (CoPw ?\<eta> \<and> DNI ?\<eta>)

goal (1 subgoal):
 1. (SML3 \<and> Fr_2 \<F> \<and> Fr_3 \<F> \<and> Fr_4 \<F>) \<and> DNI \<^bold>\<not> \<Longrightarrow> DNI \<^bold>\<not>
[PROOF STEP]
by blast


[STATEMENT]
lemma "SML1 \<Longrightarrow> rDNI \<^bold>\<not>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. SML3 \<and> Fr_2 \<F> \<and> Fr_3 \<F> \<and> Fr_4 \<F> \<Longrightarrow> rDNI \<^bold>\<not>
[PROOF STEP]
nitpick
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. SML3 \<and> Fr_2 \<F> \<and> Fr_3 \<F> \<and> Fr_4 \<F> \<Longrightarrow> rDNI \<^bold>\<not>
[PROOF STEP]
oops


[STATEMENT]
lemma "JML \<Longrightarrow> rDNE \<^bold>\<not>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (SML3 \<and> Fr_2 \<F> \<and> Fr_3 \<F> \<and> Fr_4 \<F>) \<and> DNI \<^bold>\<not> \<Longrightarrow> rDNE \<^bold>\<not>
[PROOF STEP]
nitpick
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (SML3 \<and> Fr_2 \<F> \<and> Fr_3 \<F> \<and> Fr_4 \<F>) \<and> DNI \<^bold>\<not> \<Longrightarrow> rDNE \<^bold>\<not>
[PROOF STEP]
oops


[STATEMENT]
lemma "SML4 \<Longrightarrow> CoPw \<^bold>\<not>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. SML4 \<Longrightarrow> CoPw \<^bold>\<not>
[PROOF STEP]
unfolding Defs
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. SML4 \<Longrightarrow> \<forall>a. contains (\<lambda>b. contains (\<^bold>\<not> a) (\<^bold>\<not> b)) (\<lambda>b. contains b a)
[PROOF STEP]
by (smt Cl_fr_def MONO_def monI conn)


[STATEMENT]
lemma "JML \<Longrightarrow> CoP1 \<^bold>\<not>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (SML3 \<and> Fr_2 \<F> \<and> Fr_3 \<F> \<and> Fr_4 \<F>) \<and> DNI \<^bold>\<not> \<Longrightarrow> CoP1 \<^bold>\<not>
[PROOF STEP]
using DNI_CoP1 PF1
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>SML4; DNI \<^bold>\<not>\<rbrakk> \<Longrightarrow> CoP1 \<^bold>\<not>
Fr_1 ?\<phi> = (Fr_1a ?\<phi> \<and> Fr_1b ?\<phi>)

goal (1 subgoal):
 1. (SML3 \<and> Fr_2 \<F> \<and> Fr_3 \<F> \<and> Fr_4 \<F>) \<and> DNI \<^bold>\<not> \<Longrightarrow> CoP1 \<^bold>\<not>
[PROOF STEP]
by blast


[STATEMENT]
lemma "SML1 \<Longrightarrow> MT1 \<^bold>\<not>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. SML3 \<and> Fr_2 \<F> \<and> Fr_3 \<F> \<and> Fr_4 \<F> \<Longrightarrow> MT1 \<^bold>\<not>
[PROOF STEP]
nitpick
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. SML3 \<and> Fr_2 \<F> \<and> Fr_3 \<F> \<and> Fr_4 \<F> \<Longrightarrow> MT1 \<^bold>\<not>
[PROOF STEP]
oops


[STATEMENT]
lemma "JML \<Longrightarrow> MT2 \<^bold>\<not>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (SML3 \<and> Fr_2 \<F> \<and> Fr_3 \<F> \<and> Fr_4 \<F>) \<and> DNI \<^bold>\<not> \<Longrightarrow> MT2 \<^bold>\<not>
[PROOF STEP]
nitpick
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (SML3 \<and> Fr_2 \<F> \<and> Fr_3 \<F> \<and> Fr_4 \<F>) \<and> DNI \<^bold>\<not> \<Longrightarrow> MT2 \<^bold>\<not>
[PROOF STEP]
oops


[STATEMENT]
lemma "JML \<Longrightarrow> MT3 \<^bold>\<not>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (SML3 \<and> Fr_2 \<F> \<and> Fr_3 \<F> \<and> Fr_4 \<F>) \<and> DNI \<^bold>\<not> \<Longrightarrow> MT3 \<^bold>\<not>
[PROOF STEP]
nitpick
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (SML3 \<and> Fr_2 \<F> \<and> Fr_3 \<F> \<and> Fr_4 \<F>) \<and> DNI \<^bold>\<not> \<Longrightarrow> MT3 \<^bold>\<not>
[PROOF STEP]
oops


[STATEMENT]
lemma "JML \<Longrightarrow> XCoP \<^bold>\<not>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (SML3 \<and> Fr_2 \<F> \<and> Fr_3 \<F> \<and> Fr_4 \<F>) \<and> DNI \<^bold>\<not> \<Longrightarrow> XCoP \<^bold>\<not>
[PROOF STEP]
nitpick
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (SML3 \<and> Fr_2 \<F> \<and> Fr_3 \<F> \<and> Fr_4 \<F>) \<and> DNI \<^bold>\<not> \<Longrightarrow> XCoP \<^bold>\<not>
[PROOF STEP]
oops


[STATEMENT]
lemma "JML \<Longrightarrow> DM3 \<^bold>\<not>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (SML3 \<and> Fr_2 \<F> \<and> Fr_3 \<F> \<and> Fr_4 \<F>) \<and> DNI \<^bold>\<not> \<Longrightarrow> DM3 \<^bold>\<not>
[PROOF STEP]
nitpick
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (SML3 \<and> Fr_2 \<F> \<and> Fr_3 \<F> \<and> Fr_4 \<F>) \<and> DNI \<^bold>\<not> \<Longrightarrow> DM3 \<^bold>\<not>
[PROOF STEP]
oops


[STATEMENT]
lemma "SML3 \<Longrightarrow> DM4 \<^bold>\<not>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. SML3 \<Longrightarrow> DM4 \<^bold>\<not>
[PROOF STEP]
by (simp add: DM4 PF1)


[STATEMENT]
lemma "SML4 \<Longrightarrow> DM4 \<^bold>\<not>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. SML4 \<Longrightarrow> DM4 \<^bold>\<not>
[PROOF STEP]
nitpick
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. SML4 \<Longrightarrow> DM4 \<^bold>\<not>
[PROOF STEP]
oops


[STATEMENT]
lemma "SML2 \<Longrightarrow> nNor \<^bold>\<not>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. SML3 \<and> Fr_2 \<F> \<and> Fr_3 \<F> \<Longrightarrow> nNor \<^bold>\<not>
[PROOF STEP]
using Cl_fr_def nNor_I nNor_def
[PROOF STATE]
proof (prove)
using this:
\<C>\<^sub>F ?\<F> \<equiv> \<lambda>A. A \<^bold>\<or> ?\<F> A
\<lbrakk>Fr_2 \<F>; Fr_3 \<F>\<rbrakk> \<Longrightarrow> nNor \<^bold>\<not>\<^sup>I
nNor ?\<eta> \<equiv> \<forall>w. ?\<eta> \<^bold>\<bottom> w = \<^bold>\<top> w

goal (1 subgoal):
 1. SML3 \<and> Fr_2 \<F> \<and> Fr_3 \<F> \<Longrightarrow> nNor \<^bold>\<not>
[PROOF STEP]
unfolding conn
[PROOF STATE]
proof (prove)
using this:
\<C>\<^sub>F ?\<F> \<equiv> \<lambda>A w. A w \<or> ?\<F> A w
\<lbrakk>Fr_2 \<F>; Fr_3 \<F>\<rbrakk> \<Longrightarrow> nNor (\<lambda>A. \<I> (\<lambda>w. \<sim>A w))
nNor ?\<eta> \<equiv> \<forall>w. ?\<eta> (\<lambda>w. False) w = True

goal (1 subgoal):
 1. SML3 \<and> Fr_2 \<F> \<and> Fr_3 \<F> \<Longrightarrow> nNor (\<lambda>A. \<C>' (\<I> (\<lambda>w. \<sim>A w)))
[PROOF STEP]
by auto


[STATEMENT]
lemma "SML3 \<Longrightarrow> nNor \<^bold>\<not>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. SML3 \<Longrightarrow> nNor \<^bold>\<not>
[PROOF STEP]
nitpick
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. SML3 \<Longrightarrow> nNor \<^bold>\<not>
[PROOF STEP]
oops


[STATEMENT]
lemma "JML \<Longrightarrow> nDNor \<^bold>\<not>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (SML3 \<and> Fr_2 \<F> \<and> Fr_3 \<F> \<and> Fr_4 \<F>) \<and> DNI \<^bold>\<not> \<Longrightarrow> nDNor \<^bold>\<not>
[PROOF STEP]
nitpick
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (SML3 \<and> Fr_2 \<F> \<and> Fr_3 \<F> \<and> Fr_4 \<F>) \<and> DNI \<^bold>\<not> \<Longrightarrow> nDNor \<^bold>\<not>
[PROOF STEP]
oops


[STATEMENT]
lemma "JML \<Longrightarrow> lCoPw(\<^bold>\<rightarrow>) \<^bold>\<not>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (SML3 \<and> Fr_2 \<F> \<and> Fr_3 \<F> \<and> Fr_4 \<F>) \<and> DNI \<^bold>\<not> \<Longrightarrow> lCoPw (\<^bold>\<rightarrow>) \<^bold>\<not>
[PROOF STEP]
nitpick
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (SML3 \<and> Fr_2 \<F> \<and> Fr_3 \<F> \<and> Fr_4 \<F>) \<and> DNI \<^bold>\<not> \<Longrightarrow> lCoPw (\<^bold>\<rightarrow>) \<^bold>\<not>
[PROOF STEP]
oops


[STATEMENT]
lemma "JML \<Longrightarrow> lCoP1(\<^bold>\<rightarrow>) \<^bold>\<not>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (SML3 \<and> Fr_2 \<F> \<and> Fr_3 \<F> \<and> Fr_4 \<F>) \<and> DNI \<^bold>\<not> \<Longrightarrow> lCoP1 (\<^bold>\<rightarrow>) \<^bold>\<not>
[PROOF STEP]
nitpick
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (SML3 \<and> Fr_2 \<F> \<and> Fr_3 \<F> \<and> Fr_4 \<F>) \<and> DNI \<^bold>\<not> \<Longrightarrow> lCoP1 (\<^bold>\<rightarrow>) \<^bold>\<not>
[PROOF STEP]
oops


[STATEMENT]
lemma "JML \<Longrightarrow> lCoP2(\<^bold>\<rightarrow>) \<^bold>\<not>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (SML3 \<and> Fr_2 \<F> \<and> Fr_3 \<F> \<and> Fr_4 \<F>) \<and> DNI \<^bold>\<not> \<Longrightarrow> lCoP2 (\<^bold>\<rightarrow>) \<^bold>\<not>
[PROOF STEP]
nitpick
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (SML3 \<and> Fr_2 \<F> \<and> Fr_3 \<F> \<and> Fr_4 \<F>) \<and> DNI \<^bold>\<not> \<Longrightarrow> lCoP2 (\<^bold>\<rightarrow>) \<^bold>\<not>
[PROOF STEP]
oops


[STATEMENT]
lemma "JML \<Longrightarrow> lCoP3(\<^bold>\<rightarrow>) \<^bold>\<not>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (SML3 \<and> Fr_2 \<F> \<and> Fr_3 \<F> \<and> Fr_4 \<F>) \<and> DNI \<^bold>\<not> \<Longrightarrow> lCoP3 (\<^bold>\<rightarrow>) \<^bold>\<not>
[PROOF STEP]
nitpick
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (SML3 \<and> Fr_2 \<F> \<and> Fr_3 \<F> \<and> Fr_4 \<F>) \<and> DNI \<^bold>\<not> \<Longrightarrow> lCoP3 (\<^bold>\<rightarrow>) \<^bold>\<not>
[PROOF STEP]
oops


[STATEMENT]
lemma "JML \<Longrightarrow> DS1(\<^bold>\<rightarrow>) \<^bold>\<not>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (SML3 \<and> Fr_2 \<F> \<and> Fr_3 \<F> \<and> Fr_4 \<F>) \<and> DNI \<^bold>\<not> \<Longrightarrow> DS1 (\<^bold>\<rightarrow>) \<^bold>\<not>
[PROOF STEP]
nitpick
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (SML3 \<and> Fr_2 \<F> \<and> Fr_3 \<F> \<and> Fr_4 \<F>) \<and> DNI \<^bold>\<not> \<Longrightarrow> DS1 (\<^bold>\<rightarrow>) \<^bold>\<not>
[PROOF STEP]
oops


[STATEMENT]
lemma "JML \<Longrightarrow> DS2(\<^bold>\<rightarrow>) \<^bold>\<not>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (SML3 \<and> Fr_2 \<F> \<and> Fr_3 \<F> \<and> Fr_4 \<F>) \<and> DNI \<^bold>\<not> \<Longrightarrow> DS2 (\<^bold>\<rightarrow>) \<^bold>\<not>
[PROOF STEP]
nitpick
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (SML3 \<and> Fr_2 \<F> \<and> Fr_3 \<F> \<and> Fr_4 \<F>) \<and> DNI \<^bold>\<not> \<Longrightarrow> DS2 (\<^bold>\<rightarrow>) \<^bold>\<not>
[PROOF STEP]
oops


[STATEMENT]
lemma "SML1 \<Longrightarrow> lCoPw(\<^bold>\<Rightarrow>) \<^bold>\<not>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. SML3 \<and> Fr_2 \<F> \<and> Fr_3 \<F> \<and> Fr_4 \<F> \<Longrightarrow> lCoPw (\<^bold>\<Rightarrow>) \<^bold>\<not>
[PROOF STEP]
using lCoPw
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>SML3; Fr_2 \<F>; Fr_3 \<F>; Fr_4 \<F>\<rbrakk> \<Longrightarrow> lCoPw (\<^bold>\<Rightarrow>) \<^bold>\<not>

goal (1 subgoal):
 1. SML3 \<and> Fr_2 \<F> \<and> Fr_3 \<F> \<and> Fr_4 \<F> \<Longrightarrow> lCoPw (\<^bold>\<Rightarrow>) \<^bold>\<not>
[PROOF STEP]
by blast


[STATEMENT]
lemma "SML2 \<Longrightarrow> lCoPw(\<^bold>\<Rightarrow>) \<^bold>\<not>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. SML3 \<and> Fr_2 \<F> \<and> Fr_3 \<F> \<Longrightarrow> lCoPw (\<^bold>\<Rightarrow>) \<^bold>\<not>
[PROOF STEP]
nitpick
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. SML3 \<and> Fr_2 \<F> \<and> Fr_3 \<F> \<Longrightarrow> lCoPw (\<^bold>\<Rightarrow>) \<^bold>\<not>
[PROOF STEP]
oops


[STATEMENT]
lemma "JML \<Longrightarrow> lCoP1(\<^bold>\<Rightarrow>) \<^bold>\<not>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (SML3 \<and> Fr_2 \<F> \<and> Fr_3 \<F> \<and> Fr_4 \<F>) \<and> DNI \<^bold>\<not> \<Longrightarrow> lCoP1 (\<^bold>\<Rightarrow>) \<^bold>\<not>
[PROOF STEP]
using CoP1_def2 DNI_lCoP1
[PROOF STATE]
proof (prove)
using this:
CoP1 ?\<eta> = (CoPw ?\<eta> \<and> DNI ?\<eta>)
\<lbrakk>SML3; Fr_2 \<F>; Fr_3 \<F>; Fr_4 \<F>\<rbrakk> \<Longrightarrow> lCoP1 (\<^bold>\<Rightarrow>) \<^bold>\<not> \<longleftarrow> DNI \<^bold>\<not>

goal (1 subgoal):
 1. (SML3 \<and> Fr_2 \<F> \<and> Fr_3 \<F> \<and> Fr_4 \<F>) \<and> DNI \<^bold>\<not> \<Longrightarrow> lCoP1 (\<^bold>\<Rightarrow>) \<^bold>\<not>
[PROOF STEP]
by blast


[STATEMENT]
lemma "SML1 \<Longrightarrow> lCoP1(\<^bold>\<Rightarrow>) \<^bold>\<not>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. SML3 \<and> Fr_2 \<F> \<and> Fr_3 \<F> \<and> Fr_4 \<F> \<Longrightarrow> lCoP1 (\<^bold>\<Rightarrow>) \<^bold>\<not>
[PROOF STEP]
nitpick
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. SML3 \<and> Fr_2 \<F> \<and> Fr_3 \<F> \<and> Fr_4 \<F> \<Longrightarrow> lCoP1 (\<^bold>\<Rightarrow>) \<^bold>\<not>
[PROOF STEP]
oops


[STATEMENT]
lemma "JML \<Longrightarrow> lCoP2(\<^bold>\<Rightarrow>) \<^bold>\<not>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (SML3 \<and> Fr_2 \<F> \<and> Fr_3 \<F> \<and> Fr_4 \<F>) \<and> DNI \<^bold>\<not> \<Longrightarrow> lCoP2 (\<^bold>\<Rightarrow>) \<^bold>\<not>
[PROOF STEP]
nitpick
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (SML3 \<and> Fr_2 \<F> \<and> Fr_3 \<F> \<and> Fr_4 \<F>) \<and> DNI \<^bold>\<not> \<Longrightarrow> lCoP2 (\<^bold>\<Rightarrow>) \<^bold>\<not>
[PROOF STEP]
oops


[STATEMENT]
lemma "JML \<Longrightarrow> lCoP3(\<^bold>\<Rightarrow>) \<^bold>\<not>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (SML3 \<and> Fr_2 \<F> \<and> Fr_3 \<F> \<and> Fr_4 \<F>) \<and> DNI \<^bold>\<not> \<Longrightarrow> lCoP3 (\<^bold>\<Rightarrow>) \<^bold>\<not>
[PROOF STEP]
nitpick
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (SML3 \<and> Fr_2 \<F> \<and> Fr_3 \<F> \<and> Fr_4 \<F>) \<and> DNI \<^bold>\<not> \<Longrightarrow> lCoP3 (\<^bold>\<Rightarrow>) \<^bold>\<not>
[PROOF STEP]
oops


[STATEMENT]
lemma "SML2 \<Longrightarrow> lMT0(\<^bold>\<Rightarrow>) \<^bold>\<not>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. SML3 \<and> Fr_2 \<F> \<and> Fr_3 \<F> \<Longrightarrow> lMT0 (\<^bold>\<Rightarrow>) \<^bold>\<not>
[PROOF STEP]
unfolding Defs
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. SML3 \<and> Fr_2 \<F> \<and> Fr_3 \<F> \<Longrightarrow> \<forall>a b. contains (\<^bold>\<not> a) ((b \<^bold>\<Leftarrow> a) \<^bold>\<and> \<^bold>\<not> b)
[PROOF STEP]
using MT
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>SML3; Fr_2 \<F>; Fr_3 \<F>\<rbrakk> \<Longrightarrow> \<forall>a b. contains (\<^bold>\<not> a) ((b \<^bold>\<Leftarrow> a) \<^bold>\<and> \<^bold>\<not> b)

goal (1 subgoal):
 1. SML3 \<and> Fr_2 \<F> \<and> Fr_3 \<F> \<Longrightarrow> \<forall>a b. contains (\<^bold>\<not> a) ((b \<^bold>\<Leftarrow> a) \<^bold>\<and> \<^bold>\<not> b)
[PROOF STEP]
by auto


[STATEMENT]
lemma "SML3 \<Longrightarrow> lMT0(\<^bold>\<Rightarrow>) \<^bold>\<not>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. SML3 \<Longrightarrow> lMT0 (\<^bold>\<Rightarrow>) \<^bold>\<not>
[PROOF STEP]
(*nitpick*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. SML3 \<Longrightarrow> lMT0 (\<^bold>\<Rightarrow>) \<^bold>\<not>
[PROOF STEP]
oops


[STATEMENT]
lemma "SML4 \<Longrightarrow> lMT0(\<^bold>\<Rightarrow>) \<^bold>\<not>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. SML4 \<Longrightarrow> lMT0 (\<^bold>\<Rightarrow>) \<^bold>\<not>
[PROOF STEP]
nitpick
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. SML4 \<Longrightarrow> lMT0 (\<^bold>\<Rightarrow>) \<^bold>\<not>
[PROOF STEP]
oops


[STATEMENT]
lemma "JML \<Longrightarrow> lMT1(\<^bold>\<Rightarrow>) \<^bold>\<not>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (SML3 \<and> Fr_2 \<F> \<and> Fr_3 \<F> \<and> Fr_4 \<F>) \<and> DNI \<^bold>\<not> \<Longrightarrow> lMT1 (\<^bold>\<Rightarrow>) \<^bold>\<not>
[PROOF STEP]
by (smt DNI_lCoP1 DT1 lCoP1_def lMT1_def)


[STATEMENT]
lemma "SML1 \<Longrightarrow> lMT1(\<^bold>\<Rightarrow>) \<^bold>\<not>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. SML3 \<and> Fr_2 \<F> \<and> Fr_3 \<F> \<and> Fr_4 \<F> \<Longrightarrow> lMT1 (\<^bold>\<Rightarrow>) \<^bold>\<not>
[PROOF STEP]
nitpick
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. SML3 \<and> Fr_2 \<F> \<and> Fr_3 \<F> \<and> Fr_4 \<F> \<Longrightarrow> lMT1 (\<^bold>\<Rightarrow>) \<^bold>\<not>
[PROOF STEP]
oops


[STATEMENT]
lemma "JML \<Longrightarrow> lMT2(\<^bold>\<Rightarrow>) \<^bold>\<not>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (SML3 \<and> Fr_2 \<F> \<and> Fr_3 \<F> \<and> Fr_4 \<F>) \<and> DNI \<^bold>\<not> \<Longrightarrow> lMT2 (\<^bold>\<Rightarrow>) \<^bold>\<not>
[PROOF STEP]
nitpick
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (SML3 \<and> Fr_2 \<F> \<and> Fr_3 \<F> \<and> Fr_4 \<F>) \<and> DNI \<^bold>\<not> \<Longrightarrow> lMT2 (\<^bold>\<Rightarrow>) \<^bold>\<not>
[PROOF STEP]
oops


[STATEMENT]
lemma "JML \<Longrightarrow> lMT3(\<^bold>\<Rightarrow>) \<^bold>\<not>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (SML3 \<and> Fr_2 \<F> \<and> Fr_3 \<F> \<and> Fr_4 \<F>) \<and> DNI \<^bold>\<not> \<Longrightarrow> lMT3 (\<^bold>\<Rightarrow>) \<^bold>\<not>
[PROOF STEP]
nitpick
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (SML3 \<and> Fr_2 \<F> \<and> Fr_3 \<F> \<and> Fr_4 \<F>) \<and> DNI \<^bold>\<not> \<Longrightarrow> lMT3 (\<^bold>\<Rightarrow>) \<^bold>\<not>
[PROOF STEP]
oops


[STATEMENT]
lemma "JML \<Longrightarrow> DS1(\<^bold>\<Rightarrow>) \<^bold>\<not>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (SML3 \<and> Fr_2 \<F> \<and> Fr_3 \<F> \<and> Fr_4 \<F>) \<and> DNI \<^bold>\<not> \<Longrightarrow> DS1 (\<^bold>\<Rightarrow>) \<^bold>\<not>
[PROOF STEP]
nitpick
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (SML3 \<and> Fr_2 \<F> \<and> Fr_3 \<F> \<and> Fr_4 \<F>) \<and> DNI \<^bold>\<not> \<Longrightarrow> DS1 (\<^bold>\<Rightarrow>) \<^bold>\<not>
[PROOF STEP]
oops


[STATEMENT]
lemma "JML \<Longrightarrow> DS2(\<^bold>\<Rightarrow>) \<^bold>\<not>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (SML3 \<and> Fr_2 \<F> \<and> Fr_3 \<F> \<and> Fr_4 \<F>) \<and> DNI \<^bold>\<not> \<Longrightarrow> DS2 (\<^bold>\<Rightarrow>) \<^bold>\<not>
[PROOF STEP]
nitpick
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (SML3 \<and> Fr_2 \<F> \<and> Fr_3 \<F> \<and> Fr_4 \<F>) \<and> DNI \<^bold>\<not> \<Longrightarrow> DS2 (\<^bold>\<Rightarrow>) \<^bold>\<not>
[PROOF STEP]
oops


[STATEMENT]
lemma "JML \<Longrightarrow> DS3(\<^bold>\<Rightarrow>) \<^bold>\<not>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (SML3 \<and> Fr_2 \<F> \<and> Fr_3 \<F> \<and> Fr_4 \<F>) \<and> DNI \<^bold>\<not> \<Longrightarrow> DS3 (\<^bold>\<Rightarrow>) \<^bold>\<not>
[PROOF STEP]
nitpick
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (SML3 \<and> Fr_2 \<F> \<and> Fr_3 \<F> \<and> Fr_4 \<F>) \<and> DNI \<^bold>\<not> \<Longrightarrow> DS3 (\<^bold>\<Rightarrow>) \<^bold>\<not>
[PROOF STEP]
oops


[STATEMENT]
lemma "JML \<Longrightarrow> DS4(\<^bold>\<Rightarrow>) \<^bold>\<not>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (SML3 \<and> Fr_2 \<F> \<and> Fr_3 \<F> \<and> Fr_4 \<F>) \<and> DNI \<^bold>\<not> \<Longrightarrow> DS4 (\<^bold>\<Rightarrow>) \<^bold>\<not>
[PROOF STEP]
nitpick
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (SML3 \<and> Fr_2 \<F> \<and> Fr_3 \<F> \<and> Fr_4 \<F>) \<and> DNI \<^bold>\<not> \<Longrightarrow> DS4 (\<^bold>\<Rightarrow>) \<^bold>\<not>
[PROOF STEP]
oops


[STATEMENT]
lemma cat_0_components:
  shows "cat_0\<lparr>Obj\<rparr> = 0"
    and "cat_0\<lparr>Arr\<rparr> = 0"
    and "cat_0\<lparr>Dom\<rparr> = 0"
    and "cat_0\<lparr>Cod\<rparr> = 0"
    and "cat_0\<lparr>Comp\<rparr> = 0"
    and "cat_0\<lparr>CId\<rparr> = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (cat_0\<lparr>Obj\<rparr> = []\<^sub>\<circ> &&& cat_0\<lparr>Arr\<rparr> = []\<^sub>\<circ> &&& cat_0\<lparr>Dom\<rparr> = []\<^sub>\<circ>) &&& cat_0\<lparr>Cod\<rparr> = []\<^sub>\<circ> &&& cat_0\<lparr>Comp\<rparr> = []\<^sub>\<circ> &&& cat_0\<lparr>CId\<rparr> = []\<^sub>\<circ>
[PROOF STEP]
unfolding cat_0_def dg_field_simps
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ([[]\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>]\<^sub>\<circ>\<lparr>[]\<^sub>\<circ>\<rparr> = []\<^sub>\<circ> &&& [[]\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>]\<^sub>\<circ>\<lparr>1\<^sub>\<nat>\<rparr> = []\<^sub>\<circ> &&& [[]\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>]\<^sub>\<circ>\<lparr>2\<^sub>\<nat>\<rparr> = []\<^sub>\<circ>) &&& [[]\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>]\<^sub>\<circ>\<lparr>3\<^sub>\<nat>\<rparr> = []\<^sub>\<circ> &&& [[]\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>]\<^sub>\<circ>\<lparr>4\<^sub>\<nat>\<rparr> = []\<^sub>\<circ> &&& [[]\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>]\<^sub>\<circ>\<lparr>5\<^sub>\<nat>\<rparr> = []\<^sub>\<circ>
[PROOF STEP]
by (simp_all add: nat_omega_simps)


[STATEMENT]
lemma cat_smc_cat_0: "cat_smc cat_0 = smc_0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cat_smc cat_0 = smc_0
[PROOF STEP]
unfolding cat_smc_def cat_0_def smc_0_def dg_field_simps
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [[[]\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>]\<^sub>\<circ>\<lparr>[]\<^sub>\<circ>\<rparr>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>]\<^sub>\<circ>\<lparr>1\<^sub>\<nat>\<rparr>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>]\<^sub>\<circ>\<lparr>2\<^sub>\<nat>\<rparr>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>]\<^sub>\<circ>\<lparr>3\<^sub>\<nat>\<rparr>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>]\<^sub>\<circ>\<lparr>4\<^sub>\<nat>\<rparr>]\<^sub>\<circ> = [[]\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>]\<^sub>\<circ>
[PROOF STEP]
by (simp add: nat_omega_simps)


[STATEMENT]
lemma (in \<Z>) category_cat_0[cat_cs_intros]: "category \<alpha> cat_0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. category \<alpha> cat_0
[PROOF STEP]
proof(intro categoryI)
[PROOF STATE]
proof (state)
goal (9 subgoals):
 1. \<Z> \<alpha>
 2. vfsequence cat_0
 3. vsv (cat_0\<lparr>CId\<rparr>)
 4. vcard cat_0 = 6\<^sub>\<nat>
 5. semicategory \<alpha> (cat_smc cat_0)
 6. \<D>\<^sub>\<circ> (cat_0\<lparr>CId\<rparr>) = cat_0\<lparr>Obj\<rparr>
 7. \<And>a. a \<in>\<^sub>\<circ> cat_0\<lparr>Obj\<rparr> \<Longrightarrow> cat_0\<lparr>CId\<rparr>\<lparr>a\<rparr> : a \<mapsto>\<^bsub>cat_0\<^esub> a
 8. \<And>a b f. f : a \<mapsto>\<^bsub>cat_0\<^esub> b \<Longrightarrow> cat_0\<lparr>CId\<rparr>\<lparr>b\<rparr> \<circ>\<^sub>A\<^bsub>cat_0\<^esub> f = f
 9. \<And>b c f. f : b \<mapsto>\<^bsub>cat_0\<^esub> c \<Longrightarrow> f \<circ>\<^sub>A\<^bsub>cat_0\<^esub> cat_0\<lparr>CId\<rparr>\<lparr>b\<rparr> = f
[PROOF STEP]
show "vfsequence cat_0" "vcard cat_0 = 6\<^sub>\<nat>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vfsequence cat_0 &&& vcard cat_0 = 6\<^sub>\<nat>
[PROOF STEP]
by (simp_all add: cat_0_def nat_omega_simps)
[PROOF STATE]
proof (state)
this:
vfsequence cat_0
vcard cat_0 = 6\<^sub>\<nat>

goal (7 subgoals):
 1. \<Z> \<alpha>
 2. vsv (cat_0\<lparr>CId\<rparr>)
 3. semicategory \<alpha> (cat_smc cat_0)
 4. \<D>\<^sub>\<circ> (cat_0\<lparr>CId\<rparr>) = cat_0\<lparr>Obj\<rparr>
 5. \<And>a. a \<in>\<^sub>\<circ> cat_0\<lparr>Obj\<rparr> \<Longrightarrow> cat_0\<lparr>CId\<rparr>\<lparr>a\<rparr> : a \<mapsto>\<^bsub>cat_0\<^esub> a
 6. \<And>a b f. f : a \<mapsto>\<^bsub>cat_0\<^esub> b \<Longrightarrow> cat_0\<lparr>CId\<rparr>\<lparr>b\<rparr> \<circ>\<^sub>A\<^bsub>cat_0\<^esub> f = f
 7. \<And>b c f. f : b \<mapsto>\<^bsub>cat_0\<^esub> c \<Longrightarrow> f \<circ>\<^sub>A\<^bsub>cat_0\<^esub> cat_0\<lparr>CId\<rparr>\<lparr>b\<rparr> = f
[PROOF STEP]
qed
  (
    auto simp:
      \<Z>_axioms
      cat_0_components
      cat_0_is_arr_iff
      cat_smc_cat_0
      \<Z>.semicategory_smc_0
  )