[STATEMENT]
lemma prv_imp_psubst_scnj:
  assumes "F \<subseteq> fmla" "finite F" "snd ` set txs \<subseteq> var" "fst ` set txs \<subseteq> trm"
    and "distinct (map snd txs)"
  shows "prv (imp (psubst (scnj F) txs) (scnj ((\<lambda>\<phi>. psubst \<phi> txs) ` F)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (imp (psubst (scnj F) txs) (scnj ((\<lambda>\<phi>. psubst \<phi> txs) ` F)))
[PROOF STEP]
using prv_psubst_scnj[OF assms] assms
[PROOF STATE]
proof (prove)
using this:
prv (eqv (psubst (scnj F) txs) (scnj ((\<lambda>\<phi>. psubst \<phi> txs) ` F)))
F \<subseteq> fmla
finite F
snd ` set txs \<subseteq> var
fst ` set txs \<subseteq> trm
distinct (map snd txs)

goal (1 subgoal):
 1. prv (imp (psubst (scnj F) txs) (scnj ((\<lambda>\<phi>. psubst \<phi> txs) ` F)))
[PROOF STEP]
apply(intro prv_imp_eqvEL)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>prv (eqv (psubst (scnj F) txs) (scnj ((\<lambda>\<phi>. psubst \<phi> txs) ` F))); F \<subseteq> fmla; finite F; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; distinct (map snd txs)\<rbrakk> \<Longrightarrow> psubst (scnj F) txs \<in> fmla
 2. \<lbrakk>prv (eqv (psubst (scnj F) txs) (scnj ((\<lambda>\<phi>. psubst \<phi> txs) ` F))); F \<subseteq> fmla; finite F; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; distinct (map snd txs)\<rbrakk> \<Longrightarrow> scnj ((\<lambda>\<phi>. psubst \<phi> txs) ` F) \<in> fmla
 3. \<lbrakk>prv (eqv (psubst (scnj F) txs) (scnj ((\<lambda>\<phi>. psubst \<phi> txs) ` F))); F \<subseteq> fmla; finite F; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; distinct (map snd txs)\<rbrakk> \<Longrightarrow> prv (eqv (psubst (scnj F) txs) (scnj ((\<lambda>\<phi>. psubst \<phi> txs) ` F)))
[PROOF STEP]
by auto


[STATEMENT]
lemma prv_psubst_scnj_imp:
  assumes "F \<subseteq> fmla" "finite F" "snd ` set txs \<subseteq> var" "fst ` set txs \<subseteq> trm"
    and "distinct (map snd txs)"
  shows "prv (imp (scnj ((\<lambda>\<phi>. psubst \<phi> txs) ` F)) (psubst (scnj F) txs))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (imp (scnj ((\<lambda>\<phi>. psubst \<phi> txs) ` F)) (psubst (scnj F) txs))
[PROOF STEP]
using prv_psubst_scnj[OF assms] assms
[PROOF STATE]
proof (prove)
using this:
prv (eqv (psubst (scnj F) txs) (scnj ((\<lambda>\<phi>. psubst \<phi> txs) ` F)))
F \<subseteq> fmla
finite F
snd ` set txs \<subseteq> var
fst ` set txs \<subseteq> trm
distinct (map snd txs)

goal (1 subgoal):
 1. prv (imp (scnj ((\<lambda>\<phi>. psubst \<phi> txs) ` F)) (psubst (scnj F) txs))
[PROOF STEP]
apply(intro prv_imp_eqvER)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>prv (eqv (psubst (scnj F) txs) (scnj ((\<lambda>\<phi>. psubst \<phi> txs) ` F))); F \<subseteq> fmla; finite F; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; distinct (map snd txs)\<rbrakk> \<Longrightarrow> psubst (scnj F) txs \<in> fmla
 2. \<lbrakk>prv (eqv (psubst (scnj F) txs) (scnj ((\<lambda>\<phi>. psubst \<phi> txs) ` F))); F \<subseteq> fmla; finite F; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; distinct (map snd txs)\<rbrakk> \<Longrightarrow> scnj ((\<lambda>\<phi>. psubst \<phi> txs) ` F) \<in> fmla
 3. \<lbrakk>prv (eqv (psubst (scnj F) txs) (scnj ((\<lambda>\<phi>. psubst \<phi> txs) ` F))); F \<subseteq> fmla; finite F; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; distinct (map snd txs)\<rbrakk> \<Longrightarrow> prv (eqv (psubst (scnj F) txs) (scnj ((\<lambda>\<phi>. psubst \<phi> txs) ` F)))
[PROOF STEP]
by auto


[STATEMENT]
lemma consistent_def2: "consistent \<longleftrightarrow> (\<exists>\<phi> \<in> fmla. \<not> prv \<phi>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. consistent = (\<exists>\<phi>\<in>fmla. \<not> prv \<phi>)
[PROOF STEP]
unfolding consistent_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<not> prv fls) = (\<exists>\<phi>\<in>fmla. \<not> prv \<phi>)
[PROOF STEP]
using prv_expl
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?\<phi> \<in> fmla; prv fls\<rbrakk> \<Longrightarrow> prv ?\<phi>

goal (1 subgoal):
 1. (\<not> prv fls) = (\<exists>\<phi>\<in>fmla. \<not> prv \<phi>)
[PROOF STEP]
by blast


[STATEMENT]
lemma consistent_def3: "consistent \<longleftrightarrow> (\<forall>\<phi> \<in> fmla. \<not> (prv \<phi> \<and> prv (neg \<phi>)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. consistent = (\<forall>\<phi>\<in>fmla. \<not> (prv \<phi> \<and> prv (neg \<phi>)))
[PROOF STEP]
unfolding consistent_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<not> prv fls) = (\<forall>\<phi>\<in>fmla. \<not> (prv \<phi> \<and> prv (neg \<phi>)))
[PROOF STEP]
using prv_neg_fls neg_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?\<phi> \<in> fmla; prv ?\<phi>; prv (neg ?\<phi>)\<rbrakk> \<Longrightarrow> prv fls
neg ?\<phi> = imp ?\<phi> fls

goal (1 subgoal):
 1. (\<not> prv fls) = (\<forall>\<phi>\<in>fmla. \<not> (prv \<phi> \<and> prv (neg \<phi>)))
[PROOF STEP]
by auto


[STATEMENT]
lemma \<omega>consistent_impliesStd1:
  "\<omega>consistent \<Longrightarrow>
 \<omega>consistentStd1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<omega>consistent \<Longrightarrow> \<omega>consistentStd1
[PROOF STEP]
unfolding \<omega>consistent_def \<omega>consistentStd1_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>\<phi>\<in>fmla. \<forall>x\<in>var. Fvars \<phi> = {x} \<longrightarrow> (\<forall>n\<in>num. prv (neg (subst \<phi> n x))) \<longrightarrow> \<not> prv (neg (neg (exi x \<phi>))) \<Longrightarrow> \<forall>\<phi>\<in>fmla. \<forall>x\<in>var. Fvars \<phi> = {x} \<longrightarrow> (\<forall>n\<in>num. prv (neg (subst \<phi> n x))) \<longrightarrow> \<not> prv (exi x \<phi>)
[PROOF STEP]
using prv_neg_neg
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?\<phi> \<in> fmla; prv ?\<phi>\<rbrakk> \<Longrightarrow> prv (neg (neg ?\<phi>))

goal (1 subgoal):
 1. \<forall>\<phi>\<in>fmla. \<forall>x\<in>var. Fvars \<phi> = {x} \<longrightarrow> (\<forall>n\<in>num. prv (neg (subst \<phi> n x))) \<longrightarrow> \<not> prv (neg (neg (exi x \<phi>))) \<Longrightarrow> \<forall>\<phi>\<in>fmla. \<forall>x\<in>var. Fvars \<phi> = {x} \<longrightarrow> (\<forall>n\<in>num. prv (neg (subst \<phi> n x))) \<longrightarrow> \<not> prv (exi x \<phi>)
[PROOF STEP]
by blast


[STATEMENT]
lemma \<omega>consistent_impliesStd2:
  "\<omega>consistent \<Longrightarrow>
 \<omega>consistentStd2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<omega>consistent \<Longrightarrow> \<omega>consistentStd2
[PROOF STEP]
by (auto dest!: \<omega>consistent_impliesStd1 bspec[of _ _ "neg _"]
      simp: \<omega>consistentStd1_def \<omega>consistentStd2_def prv_neg_neg)


[STATEMENT]
lemma \<omega>consistent_iffStd1:
  assumes "\<And> \<phi>. \<phi> \<in> fmla \<Longrightarrow> prv (imp (neg (neg \<phi>)) \<phi>)"
  shows "\<omega>consistent \<longleftrightarrow> \<omega>consistentStd1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<omega>consistent = \<omega>consistentStd1
[PROOF STEP]
apply standard
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<omega>consistent \<Longrightarrow> \<omega>consistentStd1
 2. \<omega>consistentStd1 \<Longrightarrow> \<omega>consistent
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<omega>consistent \<Longrightarrow> \<omega>consistentStd1
[PROOF STEP]
using \<omega>consistent_impliesStd1
[PROOF STATE]
proof (prove)
using this:
\<omega>consistent \<Longrightarrow> \<omega>consistentStd1

goal (1 subgoal):
 1. \<omega>consistent \<Longrightarrow> \<omega>consistentStd1
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<omega>consistentStd1 \<Longrightarrow> \<omega>consistent
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<omega>consistentStd1 \<Longrightarrow> \<omega>consistent
[PROOF STEP]
unfolding \<omega>consistentStd1_def \<omega>consistent_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>\<phi>\<in>fmla. \<forall>x\<in>var. Fvars \<phi> = {x} \<longrightarrow> (\<forall>n\<in>num. prv (neg (subst \<phi> n x))) \<longrightarrow> \<not> prv (exi x \<phi>) \<Longrightarrow> \<forall>\<phi>\<in>fmla. \<forall>x\<in>var. Fvars \<phi> = {x} \<longrightarrow> (\<forall>n\<in>num. prv (neg (subst \<phi> n x))) \<longrightarrow> \<not> prv (neg (neg (exi x \<phi>)))
[PROOF STEP]
by (meson assms exi neg prv_imp_mp)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
.


[STATEMENT]
lemma \<omega>consistent_iffStd2:
  assumes "\<And> \<phi>. \<phi> \<in> fmla \<Longrightarrow> prv (imp (neg (neg \<phi>)) \<phi>)"
  shows "\<omega>consistent \<longleftrightarrow> \<omega>consistentStd2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<omega>consistent = \<omega>consistentStd2
[PROOF STEP]
unfolding \<omega>consistent_iffStd1[OF assms, simplified]
    \<omega>consistentStd1_def \<omega>consistentStd2_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>\<phi>\<in>fmla. \<forall>x\<in>var. Fvars \<phi> = {x} \<longrightarrow> (\<forall>n\<in>num. prv (neg (subst \<phi> n x))) \<longrightarrow> \<not> prv (exi x \<phi>)) = (\<forall>\<phi>\<in>fmla. \<forall>x\<in>var. Fvars \<phi> = {x} \<longrightarrow> (\<forall>n\<in>num. prv (subst \<phi> n x)) \<longrightarrow> \<not> prv (exi x (neg \<phi>)))
[PROOF STEP]
apply safe
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>\<phi> x. \<lbrakk>\<forall>\<phi>\<in>fmla. \<forall>x\<in>var. Fvars \<phi> = {x} \<longrightarrow> (\<forall>n\<in>num. prv (neg (subst \<phi> n x))) \<longrightarrow> \<not> prv (exi x \<phi>); \<phi> \<in> fmla; x \<in> var; Fvars \<phi> = {x}; \<forall>n\<in>num. prv (subst \<phi> n x); prv (exi x (neg \<phi>))\<rbrakk> \<Longrightarrow> False
 2. \<And>\<phi> x. \<lbrakk>\<forall>\<phi>\<in>fmla. \<forall>x\<in>var. Fvars \<phi> = {x} \<longrightarrow> (\<forall>n\<in>num. prv (subst \<phi> n x)) \<longrightarrow> \<not> prv (exi x (neg \<phi>)); \<phi> \<in> fmla; x \<in> var; Fvars \<phi> = {x}; \<forall>n\<in>num. prv (neg (subst \<phi> n x)); prv (exi x \<phi>)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
subgoal for \<phi> x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>\<phi>\<in>fmla. \<forall>x\<in>var. Fvars \<phi> = {x} \<longrightarrow> (\<forall>n\<in>num. prv (neg (subst \<phi> n x))) \<longrightarrow> \<not> prv (exi x \<phi>); \<phi> \<in> fmla; x \<in> var; Fvars \<phi> = {x}; \<forall>n\<in>num. prv (subst \<phi> n x); prv (exi x (neg \<phi>))\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
by (auto simp: prv_neg_neg dest: bspec[of _ _ "neg _"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>\<phi> x. \<lbrakk>\<forall>\<phi>\<in>fmla. \<forall>x\<in>var. Fvars \<phi> = {x} \<longrightarrow> (\<forall>n\<in>num. prv (subst \<phi> n x)) \<longrightarrow> \<not> prv (exi x (neg \<phi>)); \<phi> \<in> fmla; x \<in> var; Fvars \<phi> = {x}; \<forall>n\<in>num. prv (neg (subst \<phi> n x)); prv (exi x \<phi>)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
subgoal for \<phi> x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>\<phi>\<in>fmla. \<forall>x\<in>var. Fvars \<phi> = {x} \<longrightarrow> (\<forall>n\<in>num. prv (subst \<phi> n x)) \<longrightarrow> \<not> prv (exi x (neg \<phi>)); \<phi> \<in> fmla; x \<in> var; Fvars \<phi> = {x}; \<forall>n\<in>num. prv (neg (subst \<phi> n x)); prv (exi x \<phi>)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
using  prv_exi_congW prv_imp_neg_fls
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?\<phi> \<in> fmla; ?\<chi> \<in> fmla; ?x \<in> var; prv (imp ?\<phi> ?\<chi>); prv (exi ?x ?\<phi>)\<rbrakk> \<Longrightarrow> prv (exi ?x ?\<chi>)
?\<phi> \<in> fmla \<Longrightarrow> prv (imp ?\<phi> (imp (neg ?\<phi>) fls))

goal (1 subgoal):
 1. \<lbrakk>\<forall>\<phi>\<in>fmla. \<forall>x\<in>var. Fvars \<phi> = {x} \<longrightarrow> (\<forall>n\<in>num. prv (subst \<phi> n x)) \<longrightarrow> \<not> prv (exi x (neg \<phi>)); \<phi> \<in> fmla; x \<in> var; Fvars \<phi> = {x}; \<forall>n\<in>num. prv (neg (subst \<phi> n x)); prv (exi x \<phi>)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
by (auto simp: neg_def prv_neg_neg dest!: bspec[of _ _ "neg _"])
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
.


[STATEMENT]
lemma \<omega>consistentStd1_implies_consistent:
  assumes "\<omega>consistentStd1"
  shows "consistent"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. consistent
[PROOF STEP]
unfolding consistent_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> prv fls
[PROOF STEP]
proof safe
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. prv fls \<Longrightarrow> False
[PROOF STEP]
assume pf: "prv fls"
[PROOF STATE]
proof (state)
this:
prv fls

goal (1 subgoal):
 1. prv fls \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
prv fls
[PROOF STEP]
obtain x where x: "x \<in> var" "x \<notin> Fvars fls"
[PROOF STATE]
proof (prove)
using this:
prv fls

goal (1 subgoal):
 1. (\<And>x. \<lbrakk>x \<in> var; x \<notin> Fvars fls\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using finite_Fvars getFresh
[PROOF STATE]
proof (prove)
using this:
prv fls
?\<phi> \<in> fmla \<Longrightarrow> finite (Fvars ?\<phi>)
finite ?V \<Longrightarrow> getFresh ?V \<in> var \<and> getFresh ?V \<notin> ?V

goal (1 subgoal):
 1. (\<And>x. \<lbrakk>x \<in> var; x \<notin> Fvars fls\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<in> var
x \<notin> Fvars fls

goal (1 subgoal):
 1. prv fls \<Longrightarrow> False
[PROOF STEP]
let ?fls = "cnj (fls) (eql (Var x) (Var x))"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. prv fls \<Longrightarrow> False
[PROOF STEP]
have 0: "\<forall> n \<in> num. prv (neg (subst ?fls n x))" and 1: "prv (exi x fls)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>n\<in>num. prv (neg (subst (cnj fls (eql (Var x) (Var x))) n x)) &&& prv (exi x fls)
[PROOF STEP]
using x fls
[PROOF STATE]
proof (prove)
using this:
x \<in> var
x \<notin> Fvars fls
fls \<in> fmla

goal (1 subgoal):
 1. \<forall>n\<in>num. prv (neg (subst (cnj fls (eql (Var x) (Var x))) n x)) &&& prv (exi x fls)
[PROOF STEP]
by (auto simp: pf prv_expl)
[PROOF STATE]
proof (state)
this:
\<forall>n\<in>num. prv (neg (subst (cnj fls (eql (Var x) (Var x))) n x))
prv (exi x fls)

goal (1 subgoal):
 1. prv fls \<Longrightarrow> False
[PROOF STEP]
have 2: "\<not> prv (exi x ?fls)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> prv (exi x (cnj fls (eql (Var x) (Var x))))
[PROOF STEP]
using 0 fls x assms
[PROOF STATE]
proof (prove)
using this:
\<forall>n\<in>num. prv (neg (subst (cnj fls (eql (Var x) (Var x))) n x))
fls \<in> fmla
x \<in> var
x \<notin> Fvars fls
\<omega>consistentStd1

goal (1 subgoal):
 1. \<not> prv (exi x (cnj fls (eql (Var x) (Var x))))
[PROOF STEP]
unfolding \<omega>consistentStd1_def
[PROOF STATE]
proof (prove)
using this:
\<forall>n\<in>num. prv (neg (subst (cnj fls (eql (Var x) (Var x))) n x))
fls \<in> fmla
x \<in> var
x \<notin> Fvars fls
\<forall>\<phi>\<in>fmla. \<forall>x\<in>var. Fvars \<phi> = {x} \<longrightarrow> (\<forall>n\<in>num. prv (neg (subst \<phi> n x))) \<longrightarrow> \<not> prv (exi x \<phi>)

goal (1 subgoal):
 1. \<not> prv (exi x (cnj fls (eql (Var x) (Var x))))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<not> prv (exi x (cnj fls (eql (Var x) (Var x))))

goal (1 subgoal):
 1. prv fls \<Longrightarrow> False
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. False
[PROOF STEP]
using 1 2 consistent_def consistent_def2 pf x(1)
[PROOF STATE]
proof (prove)
using this:
prv (exi x fls)
\<not> prv (exi x (cnj fls (eql (Var x) (Var x))))
consistent \<equiv> \<not> prv fls
consistent = (\<exists>\<phi>\<in>fmla. \<not> prv \<phi>)
prv fls
x \<in> var

goal (1 subgoal):
 1. False
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma \<omega>consistentStd2_implies_consistent:
  assumes "\<omega>consistentStd2"
  shows "consistent"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. consistent
[PROOF STEP]
unfolding consistent_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> prv fls
[PROOF STEP]
proof safe
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. prv fls \<Longrightarrow> False
[PROOF STEP]
assume pf: "prv fls"
[PROOF STATE]
proof (state)
this:
prv fls

goal (1 subgoal):
 1. prv fls \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
prv fls
[PROOF STEP]
obtain x where x: "x \<in> var" "x \<notin> Fvars fls"
[PROOF STATE]
proof (prove)
using this:
prv fls

goal (1 subgoal):
 1. (\<And>x. \<lbrakk>x \<in> var; x \<notin> Fvars fls\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using finite_Fvars getFresh
[PROOF STATE]
proof (prove)
using this:
prv fls
?\<phi> \<in> fmla \<Longrightarrow> finite (Fvars ?\<phi>)
finite ?V \<Longrightarrow> getFresh ?V \<in> var \<and> getFresh ?V \<notin> ?V

goal (1 subgoal):
 1. (\<And>x. \<lbrakk>x \<in> var; x \<notin> Fvars fls\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<in> var
x \<notin> Fvars fls

goal (1 subgoal):
 1. prv fls \<Longrightarrow> False
[PROOF STEP]
let ?fls = "cnj (fls) (eql (Var x) (Var x))"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. prv fls \<Longrightarrow> False
[PROOF STEP]
have 0: "\<forall> n \<in> num. prv (subst ?fls n x)" and 1: "prv (exi x (neg ?fls))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>n\<in>num. prv (subst (cnj fls (eql (Var x) (Var x))) n x) &&& prv (exi x (neg (cnj fls (eql (Var x) (Var x)))))
[PROOF STEP]
using x fls
[PROOF STATE]
proof (prove)
using this:
x \<in> var
x \<notin> Fvars fls
fls \<in> fmla

goal (1 subgoal):
 1. \<forall>n\<in>num. prv (subst (cnj fls (eql (Var x) (Var x))) n x) &&& prv (exi x (neg (cnj fls (eql (Var x) (Var x)))))
[PROOF STEP]
by (auto simp: pf prv_expl)
[PROOF STATE]
proof (state)
this:
\<forall>n\<in>num. prv (subst (cnj fls (eql (Var x) (Var x))) n x)
prv (exi x (neg (cnj fls (eql (Var x) (Var x)))))

goal (1 subgoal):
 1. prv fls \<Longrightarrow> False
[PROOF STEP]
have 2: "\<not> prv (exi x (neg ?fls))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> prv (exi x (neg (cnj fls (eql (Var x) (Var x)))))
[PROOF STEP]
using 0 fls x assms
[PROOF STATE]
proof (prove)
using this:
\<forall>n\<in>num. prv (subst (cnj fls (eql (Var x) (Var x))) n x)
fls \<in> fmla
x \<in> var
x \<notin> Fvars fls
\<omega>consistentStd2

goal (1 subgoal):
 1. \<not> prv (exi x (neg (cnj fls (eql (Var x) (Var x)))))
[PROOF STEP]
unfolding \<omega>consistentStd2_def
[PROOF STATE]
proof (prove)
using this:
\<forall>n\<in>num. prv (subst (cnj fls (eql (Var x) (Var x))) n x)
fls \<in> fmla
x \<in> var
x \<notin> Fvars fls
\<forall>\<phi>\<in>fmla. \<forall>x\<in>var. Fvars \<phi> = {x} \<longrightarrow> (\<forall>n\<in>num. prv (subst \<phi> n x)) \<longrightarrow> \<not> prv (exi x (neg \<phi>))

goal (1 subgoal):
 1. \<not> prv (exi x (neg (cnj fls (eql (Var x) (Var x)))))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<not> prv (exi x (neg (cnj fls (eql (Var x) (Var x)))))

goal (1 subgoal):
 1. prv fls \<Longrightarrow> False
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. False
[PROOF STEP]
using 1 2
[PROOF STATE]
proof (prove)
using this:
prv (exi x (neg (cnj fls (eql (Var x) (Var x)))))
\<not> prv (exi x (neg (cnj fls (eql (Var x) (Var x)))))

goal (1 subgoal):
 1. False
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma prv_imp_dsjEE:
  assumes \<phi>[simp]: "\<phi> \<in> fmla" and \<chi>[simp]: "\<chi> \<in> fmla" and \<psi>[simp]: "\<psi> \<in> fmla"
  assumes " prv (imp \<phi> \<psi>)" and "prv (imp \<chi> \<psi>)"
  shows "prv (imp (dsj \<phi> \<chi>) \<psi>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (imp (dsj \<phi> \<chi>) \<psi>)
[PROOF STEP]
by (metis assms dsj imp prv_imp_dsjE prv_imp_mp)


[STATEMENT]
lemma prv_dsj_cases:
  assumes "\<phi>1 \<in> fmla" "\<phi>2 \<in> fmla" "\<chi> \<in> fmla"
    and "prv (dsj \<phi>1 \<phi>2)" and "prv (imp \<phi>1 \<chi>)" and "prv (imp \<phi>2 \<chi>)"
  shows "prv \<chi>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv \<chi>
[PROOF STEP]
by (meson assms  dsj prv_imp_dsjEE prv_imp_mp)


[STATEMENT]
lemma prv_dsj_com_imp:
  assumes \<phi>[simp]: "\<phi> \<in> fmla" and \<chi>[simp]: "\<chi> \<in> fmla"
  shows "prv (imp (dsj \<phi> \<chi>) (dsj \<chi> \<phi>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (imp (dsj \<phi> \<chi>) (dsj \<chi> \<phi>))
[PROOF STEP]
by (metis \<chi> \<phi> dsj imp prv_dsj_impL prv_dsj_impR prv_imp_dsjE prv_imp_mp)


[STATEMENT]
lemma prv_dsj_com:
  assumes \<phi>[simp]: "\<phi> \<in> fmla" and \<chi>[simp]: "\<chi> \<in> fmla"
  shows "prv (eqv (dsj \<phi> \<chi>) (dsj \<chi> \<phi>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (eqv (dsj \<phi> \<chi>) (dsj \<chi> \<phi>))
[PROOF STEP]
by (simp add: prv_dsj_com_imp prv_eqvI)


[STATEMENT]
lemma prv_dsj_assoc_imp1:
  assumes \<phi>[simp]: "\<phi> \<in> fmla" and \<chi>[simp]: "\<chi> \<in> fmla" and \<psi>[simp]: "\<psi> \<in> fmla"
  shows "prv (imp (dsj \<phi> (dsj \<chi> \<psi>)) (dsj (dsj \<phi> \<chi>) \<psi>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (imp (dsj \<phi> (dsj \<chi> \<psi>)) (dsj (dsj \<phi> \<chi>) \<psi>))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. prv (imp (dsj \<phi> (dsj \<chi> \<psi>)) (dsj (dsj \<phi> \<chi>) \<psi>))
[PROOF STEP]
have f1: "\<And>f fa fb. f \<notin> fmla \<or> \<not> prv (imp fa fb) \<or> fb \<notin> fmla \<or> fa \<notin> fmla \<or> prv (imp fa (dsj fb f))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>f fa fb. f \<notin> fmla \<or> \<not> prv (imp fa fb) \<or> fb \<notin> fmla \<or> fa \<notin> fmla \<or> prv (imp fa (dsj fb f))
[PROOF STEP]
by (meson dsj prv_dsj_impL prv_prv_imp_trans)
[PROOF STATE]
proof (state)
this:
?f \<notin> fmla \<or> \<not> prv (imp ?fa ?fb) \<or> ?fb \<notin> fmla \<or> ?fa \<notin> fmla \<or> prv (imp ?fa (dsj ?fb ?f))

goal (1 subgoal):
 1. prv (imp (dsj \<phi> (dsj \<chi> \<psi>)) (dsj (dsj \<phi> \<chi>) \<psi>))
[PROOF STEP]
have "prv (imp \<phi> (dsj \<phi> \<chi>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (imp \<phi> (dsj \<phi> \<chi>))
[PROOF STEP]
by (simp add: prv_dsj_impL)
[PROOF STATE]
proof (state)
this:
prv (imp \<phi> (dsj \<phi> \<chi>))

goal (1 subgoal):
 1. prv (imp (dsj \<phi> (dsj \<chi> \<psi>)) (dsj (dsj \<phi> \<chi>) \<psi>))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
prv (imp \<phi> (dsj \<phi> \<chi>))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
prv (imp \<phi> (dsj \<phi> \<chi>))

goal (1 subgoal):
 1. prv (imp (dsj \<phi> (dsj \<chi> \<psi>)) (dsj (dsj \<phi> \<chi>) \<psi>))
[PROOF STEP]
using f1 \<chi> \<phi> \<psi> dsj prv_dsj_impR prv_imp_dsjEE
[PROOF STATE]
proof (prove)
using this:
prv (imp \<phi> (dsj \<phi> \<chi>))
?f \<notin> fmla \<or> \<not> prv (imp ?fa ?fb) \<or> ?fb \<notin> fmla \<or> ?fa \<notin> fmla \<or> prv (imp ?fa (dsj ?fb ?f))
\<chi> \<in> fmla
\<phi> \<in> fmla
\<psi> \<in> fmla
\<lbrakk>?\<phi> \<in> fmla; ?\<chi> \<in> fmla\<rbrakk> \<Longrightarrow> dsj ?\<phi> ?\<chi> \<in> fmla
\<lbrakk>?\<phi> \<in> fmla; ?\<chi> \<in> fmla\<rbrakk> \<Longrightarrow> prv (imp ?\<chi> (dsj ?\<phi> ?\<chi>))
\<lbrakk>?\<phi> \<in> fmla; ?\<chi> \<in> fmla; ?\<psi> \<in> fmla; prv (imp ?\<phi> ?\<psi>); prv (imp ?\<chi> ?\<psi>)\<rbrakk> \<Longrightarrow> prv (imp (dsj ?\<phi> ?\<chi>) ?\<psi>)

goal (1 subgoal):
 1. prv (imp (dsj \<phi> (dsj \<chi> \<psi>)) (dsj (dsj \<phi> \<chi>) \<psi>))
[PROOF STEP]
by presburger
[PROOF STATE]
proof (state)
this:
prv (imp (dsj \<phi> (dsj \<chi> \<psi>)) (dsj (dsj \<phi> \<chi>) \<psi>))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma prv_dsj_assoc_imp2:
 assumes \<phi>[simp]: "\<phi> \<in> fmla" and \<chi>[simp]: "\<chi> \<in> fmla" and \<psi>[simp]: "\<psi> \<in> fmla"
 shows "prv (imp (dsj (dsj \<phi> \<chi>) \<psi>) (dsj \<phi> (dsj \<chi> \<psi>)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (imp (dsj (dsj \<phi> \<chi>) \<psi>) (dsj \<phi> (dsj \<chi> \<psi>)))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. prv (imp (dsj (dsj \<phi> \<chi>) \<psi>) (dsj \<phi> (dsj \<chi> \<psi>)))
[PROOF STEP]
have f1: "\<forall>f fa fb. (((prv (imp f (dsj fa fb)) \<or> \<not> prv (imp f (dsj fb fa))) \<or> f \<notin> fmla) \<or> fa \<notin> fmla) \<or> fb \<notin> fmla"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>f fa fb. (((prv (imp f (dsj fa fb)) \<or> \<not> prv (imp f (dsj fb fa))) \<or> f \<notin> fmla) \<or> fa \<notin> fmla) \<or> fb \<notin> fmla
[PROOF STEP]
by (meson dsj prv_dsj_com_imp prv_prv_imp_trans)
[PROOF STATE]
proof (state)
this:
\<forall>f fa fb. (((prv (imp f (dsj fa fb)) \<or> \<not> prv (imp f (dsj fb fa))) \<or> f \<notin> fmla) \<or> fa \<notin> fmla) \<or> fb \<notin> fmla

goal (1 subgoal):
 1. prv (imp (dsj (dsj \<phi> \<chi>) \<psi>) (dsj \<phi> (dsj \<chi> \<psi>)))
[PROOF STEP]
have "\<forall>f fa fb. (((prv (imp f (dsj fa fb)) \<or> \<not> prv (imp f fa)) \<or> fa \<notin> fmla) \<or> f \<notin> fmla) \<or> fb \<notin> fmla"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>f fa fb. (((prv (imp f (dsj fa fb)) \<or> \<not> prv (imp f fa)) \<or> fa \<notin> fmla) \<or> f \<notin> fmla) \<or> fb \<notin> fmla
[PROOF STEP]
by (meson dsj prv_dsj_impL prv_prv_imp_trans)
[PROOF STATE]
proof (state)
this:
\<forall>f fa fb. (((prv (imp f (dsj fa fb)) \<or> \<not> prv (imp f fa)) \<or> fa \<notin> fmla) \<or> f \<notin> fmla) \<or> fb \<notin> fmla

goal (1 subgoal):
 1. prv (imp (dsj (dsj \<phi> \<chi>) \<psi>) (dsj \<phi> (dsj \<chi> \<psi>)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>f fa fb. (((prv (imp f (dsj fa fb)) \<or> \<not> prv (imp f fa)) \<or> fa \<notin> fmla) \<or> f \<notin> fmla) \<or> fb \<notin> fmla
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>f fa fb. (((prv (imp f (dsj fa fb)) \<or> \<not> prv (imp f fa)) \<or> fa \<notin> fmla) \<or> f \<notin> fmla) \<or> fb \<notin> fmla

goal (1 subgoal):
 1. prv (imp (dsj (dsj \<phi> \<chi>) \<psi>) (dsj \<phi> (dsj \<chi> \<psi>)))
[PROOF STEP]
using f1
[PROOF STATE]
proof (prove)
using this:
\<forall>f fa fb. (((prv (imp f (dsj fa fb)) \<or> \<not> prv (imp f fa)) \<or> fa \<notin> fmla) \<or> f \<notin> fmla) \<or> fb \<notin> fmla
\<forall>f fa fb. (((prv (imp f (dsj fa fb)) \<or> \<not> prv (imp f (dsj fb fa))) \<or> f \<notin> fmla) \<or> fa \<notin> fmla) \<or> fb \<notin> fmla

goal (1 subgoal):
 1. prv (imp (dsj (dsj \<phi> \<chi>) \<psi>) (dsj \<phi> (dsj \<chi> \<psi>)))
[PROOF STEP]
by (metis \<chi> \<phi> \<psi> dsj prv_dsj_impR prv_imp_dsjEE)
[PROOF STATE]
proof (state)
this:
prv (imp (dsj (dsj \<phi> \<chi>) \<psi>) (dsj \<phi> (dsj \<chi> \<psi>)))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma prv_dsj_assoc:
 assumes \<phi>[simp]: "\<phi> \<in> fmla" and \<chi>[simp]: "\<chi> \<in> fmla" and \<psi>[simp]: "\<psi> \<in> fmla"
 shows "prv (eqv (dsj \<phi> (dsj \<chi> \<psi>)) (dsj (dsj \<phi> \<chi>) \<psi>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (eqv (dsj \<phi> (dsj \<chi> \<psi>)) (dsj (dsj \<phi> \<chi>) \<psi>))
[PROOF STEP]
by (simp add: prv_dsj_assoc_imp1 prv_dsj_assoc_imp2 prv_eqvI)


[STATEMENT]
lemma prv_dsj_com_imp3:
assumes "\<phi>1 \<in> fmla" "\<phi>2 \<in> fmla" "\<phi>3 \<in> fmla"
shows "prv (imp (dsj \<phi>1 (dsj \<phi>2 \<phi>3))
                (dsj \<phi>2 (dsj \<phi>1 \<phi>3)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (imp (dsj \<phi>1 (dsj \<phi>2 \<phi>3)) (dsj \<phi>2 (dsj \<phi>1 \<phi>3)))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. prv (imp (dsj \<phi>1 (dsj \<phi>2 \<phi>3)) (dsj \<phi>2 (dsj \<phi>1 \<phi>3)))
[PROOF STEP]
have "\<forall>f fa fb. (((prv (imp f (dsj fb fa)) \<or> \<not> prv (imp f fa)) \<or> fa \<notin> fmla) \<or> f \<notin> fmla) \<or> fb \<notin> fmla"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>f fa fb. (((prv (imp f (dsj fb fa)) \<or> \<not> prv (imp f fa)) \<or> fa \<notin> fmla) \<or> f \<notin> fmla) \<or> fb \<notin> fmla
[PROOF STEP]
by (meson dsj prv_dsj_impR prv_prv_imp_trans)
[PROOF STATE]
proof (state)
this:
\<forall>f fa fb. (((prv (imp f (dsj fb fa)) \<or> \<not> prv (imp f fa)) \<or> fa \<notin> fmla) \<or> f \<notin> fmla) \<or> fb \<notin> fmla

goal (1 subgoal):
 1. prv (imp (dsj \<phi>1 (dsj \<phi>2 \<phi>3)) (dsj \<phi>2 (dsj \<phi>1 \<phi>3)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>f fa fb. (((prv (imp f (dsj fb fa)) \<or> \<not> prv (imp f fa)) \<or> fa \<notin> fmla) \<or> f \<notin> fmla) \<or> fb \<notin> fmla
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>f fa fb. (((prv (imp f (dsj fb fa)) \<or> \<not> prv (imp f fa)) \<or> fa \<notin> fmla) \<or> f \<notin> fmla) \<or> fb \<notin> fmla

goal (1 subgoal):
 1. prv (imp (dsj \<phi>1 (dsj \<phi>2 \<phi>3)) (dsj \<phi>2 (dsj \<phi>1 \<phi>3)))
[PROOF STEP]
by (meson assms(1) assms(2) assms(3) dsj prv_dsj_impL prv_dsj_impR prv_imp_dsjEE)
[PROOF STATE]
proof (state)
this:
prv (imp (dsj \<phi>1 (dsj \<phi>2 \<phi>3)) (dsj \<phi>2 (dsj \<phi>1 \<phi>3)))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma prv_dsj_mono:
"\<phi>1 \<in> fmla \<Longrightarrow> \<phi>2 \<in> fmla \<Longrightarrow> \<chi>1 \<in> fmla \<Longrightarrow> \<chi>2 \<in> fmla \<Longrightarrow>
prv (imp \<phi>1 \<chi>1) \<Longrightarrow> prv (imp \<phi>2 \<chi>2) \<Longrightarrow> prv (imp (dsj \<phi>1 \<phi>2) (dsj \<chi>1 \<chi>2))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<phi>1 \<in> fmla; \<phi>2 \<in> fmla; \<chi>1 \<in> fmla; \<chi>2 \<in> fmla; prv (imp \<phi>1 \<chi>1); prv (imp \<phi>2 \<chi>2)\<rbrakk> \<Longrightarrow> prv (imp (dsj \<phi>1 \<phi>2) (dsj \<chi>1 \<chi>2))
[PROOF STEP]
by (meson dsj prv_dsj_impL prv_dsj_impR prv_imp_dsjEE prv_prv_imp_trans)


[STATEMENT]
lemma prv_cnj_dsj_distrib1:
 assumes \<phi>[simp]: "\<phi> \<in> fmla" and \<chi>1[simp]: "\<chi>1 \<in> fmla" and \<chi>2[simp]: "\<chi>2 \<in> fmla"
 shows "prv (imp (cnj \<phi> (dsj \<chi>1 \<chi>2)) (dsj (cnj \<phi> \<chi>1) (cnj \<phi> \<chi>2)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (imp (cnj \<phi> (dsj \<chi>1 \<chi>2)) (dsj (cnj \<phi> \<chi>1) (cnj \<phi> \<chi>2)))
[PROOF STEP]
by (simp add: prv_cnj_imp prv_cnj_imp_monoR2 prv_dsj_impL prv_dsj_impR prv_imp_com prv_imp_dsjEE)


[STATEMENT]
lemma prv_cnj_dsj_distrib2:
 assumes \<phi>[simp]: "\<phi> \<in> fmla" and \<chi>1[simp]: "\<chi>1 \<in> fmla" and \<chi>2[simp]: "\<chi>2 \<in> fmla"
 shows "prv (imp (dsj (cnj \<phi> \<chi>1) (cnj \<phi> \<chi>2)) (cnj \<phi> (dsj \<chi>1 \<chi>2)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (imp (dsj (cnj \<phi> \<chi>1) (cnj \<phi> \<chi>2)) (cnj \<phi> (dsj \<chi>1 \<chi>2)))
[PROOF STEP]
by (simp add: prv_cnj_mono prv_dsj_impL prv_dsj_impR prv_imp_dsjEE prv_imp_refl)


[STATEMENT]
lemma prv_dsj_cnj_distrib1:
 assumes \<phi>[simp]: "\<phi> \<in> fmla" and \<chi>1[simp]: "\<chi>1 \<in> fmla" and \<chi>2[simp]: "\<chi>2 \<in> fmla"
 shows "prv (imp (dsj \<phi> (cnj \<chi>1 \<chi>2)) (cnj (dsj \<phi> \<chi>1) (dsj \<phi> \<chi>2)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (imp (dsj \<phi> (cnj \<chi>1 \<chi>2)) (cnj (dsj \<phi> \<chi>1) (dsj \<phi> \<chi>2)))
[PROOF STEP]
by (simp add: prv_cnj_mono prv_dsj_impL prv_dsj_impR prv_imp_cnj prv_imp_dsjEE)


[STATEMENT]
lemma prv_dsj_cnj_distrib2:
 assumes \<phi>[simp]: "\<phi> \<in> fmla" and \<chi>1[simp]: "\<chi>1 \<in> fmla" and \<chi>2[simp]: "\<chi>2 \<in> fmla"
 shows "prv (imp (cnj (dsj \<phi> \<chi>1) (dsj \<phi> \<chi>2)) (dsj \<phi> (cnj \<chi>1 \<chi>2)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (imp (cnj (dsj \<phi> \<chi>1) (dsj \<phi> \<chi>2)) (dsj \<phi> (cnj \<chi>1 \<chi>2)))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. prv (imp (cnj (dsj \<phi> \<chi>1) (dsj \<phi> \<chi>2)) (dsj \<phi> (cnj \<chi>1 \<chi>2)))
[PROOF STEP]
have "\<forall>f fa fb. (((prv (imp f (imp fb fa)) \<or> \<not> prv (imp f fa)) \<or> fa \<notin> fmla) \<or> f \<notin> fmla) \<or> fb \<notin> fmla"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>f fa fb. (((prv (imp f (imp fb fa)) \<or> \<not> prv (imp f fa)) \<or> fa \<notin> fmla) \<or> f \<notin> fmla) \<or> fb \<notin> fmla
[PROOF STEP]
by (meson imp prv_imp_imp_triv prv_prv_imp_trans)
[PROOF STATE]
proof (state)
this:
\<forall>f fa fb. (((prv (imp f (imp fb fa)) \<or> \<not> prv (imp f fa)) \<or> fa \<notin> fmla) \<or> f \<notin> fmla) \<or> fb \<notin> fmla

goal (1 subgoal):
 1. prv (imp (cnj (dsj \<phi> \<chi>1) (dsj \<phi> \<chi>2)) (dsj \<phi> (cnj \<chi>1 \<chi>2)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>f fa fb. (((prv (imp f (imp fb fa)) \<or> \<not> prv (imp f fa)) \<or> fa \<notin> fmla) \<or> f \<notin> fmla) \<or> fb \<notin> fmla
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>f fa fb. (((prv (imp f (imp fb fa)) \<or> \<not> prv (imp f fa)) \<or> fa \<notin> fmla) \<or> f \<notin> fmla) \<or> fb \<notin> fmla

goal (1 subgoal):
 1. prv (imp (cnj (dsj \<phi> \<chi>1) (dsj \<phi> \<chi>2)) (dsj \<phi> (cnj \<chi>1 \<chi>2)))
[PROOF STEP]
by (metis \<chi>1 \<chi>2 \<phi> cnj dsj imp prv_cnj_imp prv_cnj_imp_monoR2 prv_dsj_impL prv_dsj_impR
        prv_imp_com prv_imp_dsjEE)
[PROOF STATE]
proof (state)
this:
prv (imp (cnj (dsj \<phi> \<chi>1) (dsj \<phi> \<chi>2)) (dsj \<phi> (cnj \<chi>1 \<chi>2)))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma prv_dsj_cnj_distrib:
 assumes \<phi>[simp]: "\<phi> \<in> fmla" and \<chi>1[simp]: "\<chi>1 \<in> fmla" and \<chi>2[simp]: "\<chi>2 \<in> fmla"
 shows "prv (eqv (dsj \<phi> (cnj \<chi>1 \<chi>2)) (cnj (dsj \<phi> \<chi>1) (dsj \<phi> \<chi>2)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (eqv (dsj \<phi> (cnj \<chi>1 \<chi>2)) (cnj (dsj \<phi> \<chi>1) (dsj \<phi> \<chi>2)))
[PROOF STEP]
by (simp add: prv_dsj_cnj_distrib1 prv_dsj_cnj_distrib2 prv_eqvI)


[STATEMENT]
lemma prv_dsjR_fls: "\<phi> \<in> fmla \<Longrightarrow> prv (eqv (dsj fls \<phi>) \<phi>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<phi> \<in> fmla \<Longrightarrow> prv (eqv (dsj fls \<phi>) \<phi>)
[PROOF STEP]
by (simp add: prv_dsj_impR prv_eqvI prv_imp_dsjEE prv_imp_refl)


[STATEMENT]
lemma prv_dsjL_fls: "\<phi> \<in> fmla \<Longrightarrow> prv (eqv (dsj \<phi> fls) \<phi>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<phi> \<in> fmla \<Longrightarrow> prv (eqv (dsj \<phi> fls) \<phi>)
[PROOF STEP]
by (simp add: prv_dsj_impL prv_eqvI prv_imp_dsjEE prv_imp_refl)


[STATEMENT]
lemma prv_dsjR_tru: "\<phi> \<in> fmla \<Longrightarrow> prv (eqv (dsj tru \<phi>) tru)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<phi> \<in> fmla \<Longrightarrow> prv (eqv (dsj tru \<phi>) tru)
[PROOF STEP]
by (simp add: prv_dsj_impL prv_eqvI prv_imp_tru)


[STATEMENT]
lemma prv_dsjL_tru: "\<phi> \<in> fmla \<Longrightarrow> prv (eqv (dsj \<phi> tru) tru)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<phi> \<in> fmla \<Longrightarrow> prv (eqv (dsj \<phi> tru) tru)
[PROOF STEP]
by (simp add: prv_dsj_impR prv_eqvI prv_imp_tru)


[STATEMENT]
lemma prv_imp_ldsj_in:
  assumes "set \<phi>s \<subseteq> fmla"
  and "\<phi> \<in> set \<phi>s"
  shows "prv (imp \<phi> (ldsj \<phi>s))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (imp \<phi> (ldsj \<phi>s))
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. prv (imp \<phi> (ldsj \<phi>s))
[PROOF STEP]
have "\<phi> \<in> fmla"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<phi> \<in> fmla
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
set \<phi>s \<subseteq> fmla
\<phi> \<in> set \<phi>s

goal (1 subgoal):
 1. \<phi> \<in> fmla
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<phi> \<in> fmla

goal (1 subgoal):
 1. prv (imp \<phi> (ldsj \<phi>s))
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<phi> \<in> fmla

goal (1 subgoal):
 1. prv (imp \<phi> (ldsj \<phi>s))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<phi> \<in> fmla
set \<phi>s \<subseteq> fmla
\<phi> \<in> set \<phi>s

goal (1 subgoal):
 1. prv (imp \<phi> (ldsj \<phi>s))
[PROOF STEP]
apply(induct \<phi>s arbitrary: \<phi>)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>\<phi>. \<lbrakk>\<phi> \<in> fmla; set [] \<subseteq> fmla; \<phi> \<in> set []\<rbrakk> \<Longrightarrow> prv (imp \<phi> (ldsj []))
 2. \<And>a \<phi>s \<phi>. \<lbrakk>\<And>\<phi>. \<lbrakk>\<phi> \<in> fmla; set \<phi>s \<subseteq> fmla; \<phi> \<in> set \<phi>s\<rbrakk> \<Longrightarrow> prv (imp \<phi> (ldsj \<phi>s)); \<phi> \<in> fmla; set (a # \<phi>s) \<subseteq> fmla; \<phi> \<in> set (a # \<phi>s)\<rbrakk> \<Longrightarrow> prv (imp \<phi> (ldsj (a # \<phi>s)))
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<phi>_ \<in> fmla; set [] \<subseteq> fmla; \<phi>_ \<in> set []\<rbrakk> \<Longrightarrow> prv (imp \<phi>_ (ldsj []))
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a \<phi>s \<phi>. \<lbrakk>\<And>\<phi>. \<lbrakk>\<phi> \<in> fmla; set \<phi>s \<subseteq> fmla; \<phi> \<in> set \<phi>s\<rbrakk> \<Longrightarrow> prv (imp \<phi> (ldsj \<phi>s)); \<phi> \<in> fmla; set (a # \<phi>s) \<subseteq> fmla; \<phi> \<in> set (a # \<phi>s)\<rbrakk> \<Longrightarrow> prv (imp \<phi> (ldsj (a # \<phi>s)))
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>\<phi>. \<lbrakk>\<phi> \<in> fmla; set \<phi>s_ \<subseteq> fmla; \<phi> \<in> set \<phi>s_\<rbrakk> \<Longrightarrow> prv (imp \<phi> (ldsj \<phi>s_)); \<phi>_ \<in> fmla; set (a_ # \<phi>s_) \<subseteq> fmla; \<phi>_ \<in> set (a_ # \<phi>s_)\<rbrakk> \<Longrightarrow> prv (imp \<phi>_ (ldsj (a_ # \<phi>s_)))
[PROOF STEP]
by (simp add: prv_dsj_impL)
    (meson dsj ldsj prv_dsj_impL prv_dsj_impR prv_prv_imp_trans)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
prv (imp \<phi> (ldsj \<phi>s))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma prv_imp_ldsj:
assumes "\<chi> \<in> fmla" and "set \<phi>s \<subseteq> fmla"
and "\<phi> \<in> set \<phi>s" and "prv (imp \<chi> \<phi>)"
shows "prv (imp \<chi> (ldsj \<phi>s))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (imp \<chi> (ldsj \<phi>s))
[PROOF STEP]
using assms ldsj prv_imp_ldsj_in prv_prv_imp_trans
[PROOF STATE]
proof (prove)
using this:
\<chi> \<in> fmla
set \<phi>s \<subseteq> fmla
\<phi> \<in> set \<phi>s
prv (imp \<chi> \<phi>)
set ?\<phi>s \<subseteq> fmla \<Longrightarrow> ldsj ?\<phi>s \<in> fmla
\<lbrakk>set ?\<phi>s \<subseteq> fmla; ?\<phi> \<in> set ?\<phi>s\<rbrakk> \<Longrightarrow> prv (imp ?\<phi> (ldsj ?\<phi>s))
\<lbrakk>?\<phi> \<in> fmla; ?\<chi> \<in> fmla; ?\<psi> \<in> fmla; prv (imp ?\<phi> ?\<chi>); prv (imp ?\<chi> ?\<psi>)\<rbrakk> \<Longrightarrow> prv (imp ?\<phi> ?\<psi>)

goal (1 subgoal):
 1. prv (imp \<chi> (ldsj \<phi>s))
[PROOF STEP]
by blast


[STATEMENT]
lemma prv_ldsj_imp:
  assumes "\<chi> \<in> fmla" and "set \<phi>s \<subseteq> fmla"
  and "\<And>\<phi>. \<phi> \<in> set \<phi>s \<Longrightarrow> prv (imp \<phi> \<chi>)"
  shows "prv (imp (ldsj \<phi>s) \<chi>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (imp (ldsj \<phi>s) \<chi>)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<chi> \<in> fmla
set \<phi>s \<subseteq> fmla
?\<phi> \<in> set \<phi>s \<Longrightarrow> prv (imp ?\<phi> \<chi>)

goal (1 subgoal):
 1. prv (imp (ldsj \<phi>s) \<chi>)
[PROOF STEP]
by (induct \<phi>s arbitrary: \<chi>)
     (auto simp add: prv_imp_tru prv_imp_com prv_imp_dsjEE)


[STATEMENT]
lemma prv_ldsj_imp_inner:
assumes "\<phi> \<in> fmla" "set \<phi>1s \<subseteq> fmla" "set \<phi>2s \<subseteq> fmla"
shows "prv (imp (ldsj (\<phi>1s @ \<phi> # \<phi>2s)) (dsj \<phi> (ldsj (\<phi>1s @ \<phi>2s))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (imp (ldsj (\<phi>1s @ \<phi> # \<phi>2s)) (dsj \<phi> (ldsj (\<phi>1s @ \<phi>2s))))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<phi> \<in> fmla
set \<phi>1s \<subseteq> fmla
set \<phi>2s \<subseteq> fmla

goal (1 subgoal):
 1. prv (imp (ldsj (\<phi>1s @ \<phi> # \<phi>2s)) (dsj \<phi> (ldsj (\<phi>1s @ \<phi>2s))))
[PROOF STEP]
proof(induction \<phi>1s)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>\<phi> \<in> fmla; set [] \<subseteq> fmla; set \<phi>2s \<subseteq> fmla\<rbrakk> \<Longrightarrow> prv (imp (ldsj ([] @ \<phi> # \<phi>2s)) (dsj \<phi> (ldsj ([] @ \<phi>2s))))
 2. \<And>a \<phi>1s. \<lbrakk>\<lbrakk>\<phi> \<in> fmla; set \<phi>1s \<subseteq> fmla; set \<phi>2s \<subseteq> fmla\<rbrakk> \<Longrightarrow> prv (imp (ldsj (\<phi>1s @ \<phi> # \<phi>2s)) (dsj \<phi> (ldsj (\<phi>1s @ \<phi>2s)))); \<phi> \<in> fmla; set (a # \<phi>1s) \<subseteq> fmla; set \<phi>2s \<subseteq> fmla\<rbrakk> \<Longrightarrow> prv (imp (ldsj ((a # \<phi>1s) @ \<phi> # \<phi>2s)) (dsj \<phi> (ldsj ((a # \<phi>1s) @ \<phi>2s))))
[PROOF STEP]
case (Cons \<phi>1 \<phi>1s)
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<phi> \<in> fmla; set \<phi>1s \<subseteq> fmla; set \<phi>2s \<subseteq> fmla\<rbrakk> \<Longrightarrow> prv (imp (ldsj (\<phi>1s @ \<phi> # \<phi>2s)) (dsj \<phi> (ldsj (\<phi>1s @ \<phi>2s))))
\<phi> \<in> fmla
set (\<phi>1 # \<phi>1s) \<subseteq> fmla
set \<phi>2s \<subseteq> fmla

goal (2 subgoals):
 1. \<lbrakk>\<phi> \<in> fmla; set [] \<subseteq> fmla; set \<phi>2s \<subseteq> fmla\<rbrakk> \<Longrightarrow> prv (imp (ldsj ([] @ \<phi> # \<phi>2s)) (dsj \<phi> (ldsj ([] @ \<phi>2s))))
 2. \<And>a \<phi>1s. \<lbrakk>\<lbrakk>\<phi> \<in> fmla; set \<phi>1s \<subseteq> fmla; set \<phi>2s \<subseteq> fmla\<rbrakk> \<Longrightarrow> prv (imp (ldsj (\<phi>1s @ \<phi> # \<phi>2s)) (dsj \<phi> (ldsj (\<phi>1s @ \<phi>2s)))); \<phi> \<in> fmla; set (a # \<phi>1s) \<subseteq> fmla; set \<phi>2s \<subseteq> fmla\<rbrakk> \<Longrightarrow> prv (imp (ldsj ((a # \<phi>1s) @ \<phi> # \<phi>2s)) (dsj \<phi> (ldsj ((a # \<phi>1s) @ \<phi>2s))))
[PROOF STEP]
have [intro!]: "set (\<phi>1s @ \<phi>2s) \<subseteq> fmla" "set (\<phi>1s @ \<phi> # \<phi>2s) \<subseteq> fmla"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (\<phi>1s @ \<phi>2s) \<subseteq> fmla &&& set (\<phi>1s @ \<phi> # \<phi>2s) \<subseteq> fmla
[PROOF STEP]
using Cons
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<phi> \<in> fmla; set \<phi>1s \<subseteq> fmla; set \<phi>2s \<subseteq> fmla\<rbrakk> \<Longrightarrow> prv (imp (ldsj (\<phi>1s @ \<phi> # \<phi>2s)) (dsj \<phi> (ldsj (\<phi>1s @ \<phi>2s))))
\<phi> \<in> fmla
set (\<phi>1 # \<phi>1s) \<subseteq> fmla
set \<phi>2s \<subseteq> fmla

goal (1 subgoal):
 1. set (\<phi>1s @ \<phi>2s) \<subseteq> fmla &&& set (\<phi>1s @ \<phi> # \<phi>2s) \<subseteq> fmla
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
set (\<phi>1s @ \<phi>2s) \<subseteq> fmla
set (\<phi>1s @ \<phi> # \<phi>2s) \<subseteq> fmla

goal (2 subgoals):
 1. \<lbrakk>\<phi> \<in> fmla; set [] \<subseteq> fmla; set \<phi>2s \<subseteq> fmla\<rbrakk> \<Longrightarrow> prv (imp (ldsj ([] @ \<phi> # \<phi>2s)) (dsj \<phi> (ldsj ([] @ \<phi>2s))))
 2. \<And>a \<phi>1s. \<lbrakk>\<lbrakk>\<phi> \<in> fmla; set \<phi>1s \<subseteq> fmla; set \<phi>2s \<subseteq> fmla\<rbrakk> \<Longrightarrow> prv (imp (ldsj (\<phi>1s @ \<phi> # \<phi>2s)) (dsj \<phi> (ldsj (\<phi>1s @ \<phi>2s)))); \<phi> \<in> fmla; set (a # \<phi>1s) \<subseteq> fmla; set \<phi>2s \<subseteq> fmla\<rbrakk> \<Longrightarrow> prv (imp (ldsj ((a # \<phi>1s) @ \<phi> # \<phi>2s)) (dsj \<phi> (ldsj ((a # \<phi>1s) @ \<phi>2s))))
[PROOF STEP]
have 0: "prv (imp (dsj \<phi>1 (dsj \<phi> (ldsj (\<phi>1s @ \<phi>2s))))
                 (dsj \<phi> (dsj \<phi>1 (ldsj (\<phi>1s @ \<phi>2s)))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (imp (dsj \<phi>1 (dsj \<phi> (ldsj (\<phi>1s @ \<phi>2s)))) (dsj \<phi> (dsj \<phi>1 (ldsj (\<phi>1s @ \<phi>2s)))))
[PROOF STEP]
using Cons
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<phi> \<in> fmla; set \<phi>1s \<subseteq> fmla; set \<phi>2s \<subseteq> fmla\<rbrakk> \<Longrightarrow> prv (imp (ldsj (\<phi>1s @ \<phi> # \<phi>2s)) (dsj \<phi> (ldsj (\<phi>1s @ \<phi>2s))))
\<phi> \<in> fmla
set (\<phi>1 # \<phi>1s) \<subseteq> fmla
set \<phi>2s \<subseteq> fmla

goal (1 subgoal):
 1. prv (imp (dsj \<phi>1 (dsj \<phi> (ldsj (\<phi>1s @ \<phi>2s)))) (dsj \<phi> (dsj \<phi>1 (ldsj (\<phi>1s @ \<phi>2s)))))
[PROOF STEP]
by (intro prv_dsj_com_imp3) fastforce+
[PROOF STATE]
proof (state)
this:
prv (imp (dsj \<phi>1 (dsj \<phi> (ldsj (\<phi>1s @ \<phi>2s)))) (dsj \<phi> (dsj \<phi>1 (ldsj (\<phi>1s @ \<phi>2s)))))

goal (2 subgoals):
 1. \<lbrakk>\<phi> \<in> fmla; set [] \<subseteq> fmla; set \<phi>2s \<subseteq> fmla\<rbrakk> \<Longrightarrow> prv (imp (ldsj ([] @ \<phi> # \<phi>2s)) (dsj \<phi> (ldsj ([] @ \<phi>2s))))
 2. \<And>a \<phi>1s. \<lbrakk>\<lbrakk>\<phi> \<in> fmla; set \<phi>1s \<subseteq> fmla; set \<phi>2s \<subseteq> fmla\<rbrakk> \<Longrightarrow> prv (imp (ldsj (\<phi>1s @ \<phi> # \<phi>2s)) (dsj \<phi> (ldsj (\<phi>1s @ \<phi>2s)))); \<phi> \<in> fmla; set (a # \<phi>1s) \<subseteq> fmla; set \<phi>2s \<subseteq> fmla\<rbrakk> \<Longrightarrow> prv (imp (ldsj ((a # \<phi>1s) @ \<phi> # \<phi>2s)) (dsj \<phi> (ldsj ((a # \<phi>1s) @ \<phi>2s))))
[PROOF STEP]
have 1: "prv (imp (dsj \<phi>1 (ldsj (\<phi>1s @ \<phi> # \<phi>2s)))
                (dsj \<phi>1 (dsj \<phi> (ldsj (\<phi>1s @ \<phi>2s)))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (imp (dsj \<phi>1 (ldsj (\<phi>1s @ \<phi> # \<phi>2s))) (dsj \<phi>1 (dsj \<phi> (ldsj (\<phi>1s @ \<phi>2s)))))
[PROOF STEP]
using Cons
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<phi> \<in> fmla; set \<phi>1s \<subseteq> fmla; set \<phi>2s \<subseteq> fmla\<rbrakk> \<Longrightarrow> prv (imp (ldsj (\<phi>1s @ \<phi> # \<phi>2s)) (dsj \<phi> (ldsj (\<phi>1s @ \<phi>2s))))
\<phi> \<in> fmla
set (\<phi>1 # \<phi>1s) \<subseteq> fmla
set \<phi>2s \<subseteq> fmla

goal (1 subgoal):
 1. prv (imp (dsj \<phi>1 (ldsj (\<phi>1s @ \<phi> # \<phi>2s))) (dsj \<phi>1 (dsj \<phi> (ldsj (\<phi>1s @ \<phi>2s)))))
[PROOF STEP]
by (intro prv_dsj_mono) (auto simp add: prv_imp_refl)
[PROOF STATE]
proof (state)
this:
prv (imp (dsj \<phi>1 (ldsj (\<phi>1s @ \<phi> # \<phi>2s))) (dsj \<phi>1 (dsj \<phi> (ldsj (\<phi>1s @ \<phi>2s)))))

goal (2 subgoals):
 1. \<lbrakk>\<phi> \<in> fmla; set [] \<subseteq> fmla; set \<phi>2s \<subseteq> fmla\<rbrakk> \<Longrightarrow> prv (imp (ldsj ([] @ \<phi> # \<phi>2s)) (dsj \<phi> (ldsj ([] @ \<phi>2s))))
 2. \<And>a \<phi>1s. \<lbrakk>\<lbrakk>\<phi> \<in> fmla; set \<phi>1s \<subseteq> fmla; set \<phi>2s \<subseteq> fmla\<rbrakk> \<Longrightarrow> prv (imp (ldsj (\<phi>1s @ \<phi> # \<phi>2s)) (dsj \<phi> (ldsj (\<phi>1s @ \<phi>2s)))); \<phi> \<in> fmla; set (a # \<phi>1s) \<subseteq> fmla; set \<phi>2s \<subseteq> fmla\<rbrakk> \<Longrightarrow> prv (imp (ldsj ((a # \<phi>1s) @ \<phi> # \<phi>2s)) (dsj \<phi> (ldsj ((a # \<phi>1s) @ \<phi>2s))))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (imp (ldsj ((\<phi>1 # \<phi>1s) @ \<phi> # \<phi>2s)) (dsj \<phi> (ldsj ((\<phi>1 # \<phi>1s) @ \<phi>2s))))
[PROOF STEP]
using prv_prv_imp_trans[OF _ _ _ 1 0] Cons
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>dsj \<phi>1 (ldsj (\<phi>1s @ \<phi> # \<phi>2s)) \<in> fmla; dsj \<phi>1 (dsj \<phi> (ldsj (\<phi>1s @ \<phi>2s))) \<in> fmla; dsj \<phi> (dsj \<phi>1 (ldsj (\<phi>1s @ \<phi>2s))) \<in> fmla\<rbrakk> \<Longrightarrow> prv (imp (dsj \<phi>1 (ldsj (\<phi>1s @ \<phi> # \<phi>2s))) (dsj \<phi> (dsj \<phi>1 (ldsj (\<phi>1s @ \<phi>2s)))))
\<lbrakk>\<phi> \<in> fmla; set \<phi>1s \<subseteq> fmla; set \<phi>2s \<subseteq> fmla\<rbrakk> \<Longrightarrow> prv (imp (ldsj (\<phi>1s @ \<phi> # \<phi>2s)) (dsj \<phi> (ldsj (\<phi>1s @ \<phi>2s))))
\<phi> \<in> fmla
set (\<phi>1 # \<phi>1s) \<subseteq> fmla
set \<phi>2s \<subseteq> fmla

goal (1 subgoal):
 1. prv (imp (ldsj ((\<phi>1 # \<phi>1s) @ \<phi> # \<phi>2s)) (dsj \<phi> (ldsj ((\<phi>1 # \<phi>1s) @ \<phi>2s))))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
prv (imp (ldsj ((\<phi>1 # \<phi>1s) @ \<phi> # \<phi>2s)) (dsj \<phi> (ldsj ((\<phi>1 # \<phi>1s) @ \<phi>2s))))

goal (1 subgoal):
 1. \<lbrakk>\<phi> \<in> fmla; set [] \<subseteq> fmla; set \<phi>2s \<subseteq> fmla\<rbrakk> \<Longrightarrow> prv (imp (ldsj ([] @ \<phi> # \<phi>2s)) (dsj \<phi> (ldsj ([] @ \<phi>2s))))
[PROOF STEP]
qed(simp add: prv_imp_refl)


[STATEMENT]
lemma prv_ldsj_imp_remdups:
assumes "set \<phi>s \<subseteq> fmla"
shows "prv (imp  (ldsj \<phi>s) (ldsj (remdups \<phi>s)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (imp (ldsj \<phi>s) (ldsj (remdups \<phi>s)))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
set \<phi>s \<subseteq> fmla

goal (1 subgoal):
 1. prv (imp (ldsj \<phi>s) (ldsj (remdups \<phi>s)))
[PROOF STEP]
apply(induct \<phi>s)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. set [] \<subseteq> fmla \<Longrightarrow> prv (imp (ldsj []) (ldsj (remdups [])))
 2. \<And>a \<phi>s. \<lbrakk>set \<phi>s \<subseteq> fmla \<Longrightarrow> prv (imp (ldsj \<phi>s) (ldsj (remdups \<phi>s))); set (a # \<phi>s) \<subseteq> fmla\<rbrakk> \<Longrightarrow> prv (imp (ldsj (a # \<phi>s)) (ldsj (remdups (a # \<phi>s))))
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set [] \<subseteq> fmla \<Longrightarrow> prv (imp (ldsj []) (ldsj (remdups [])))
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a \<phi>s. \<lbrakk>set \<phi>s \<subseteq> fmla \<Longrightarrow> prv (imp (ldsj \<phi>s) (ldsj (remdups \<phi>s))); set (a # \<phi>s) \<subseteq> fmla\<rbrakk> \<Longrightarrow> prv (imp (ldsj (a # \<phi>s)) (ldsj (remdups (a # \<phi>s))))
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>set \<phi>s_ \<subseteq> fmla \<Longrightarrow> prv (imp (ldsj \<phi>s_) (ldsj (remdups \<phi>s_))); set (a_ # \<phi>s_) \<subseteq> fmla\<rbrakk> \<Longrightarrow> prv (imp (ldsj (a_ # \<phi>s_)) (ldsj (remdups (a_ # \<phi>s_))))
[PROOF STEP]
by (metis ldsj prv_imp_ldsj_in prv_ldsj_imp set_remdups)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
.


[STATEMENT]
lemma prv_ldsj_mono:
assumes \<phi>2s: "set \<phi>2s \<subseteq> fmla" and "set \<phi>1s \<subseteq> set \<phi>2s"
shows "prv (imp (ldsj \<phi>1s) (ldsj \<phi>2s))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (imp (ldsj \<phi>1s) (ldsj \<phi>2s))
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. prv (imp (ldsj \<phi>1s) (ldsj \<phi>2s))
[PROOF STEP]
define \<phi>1s' where \<phi>1s': "\<phi>1s' = remdups \<phi>1s"
[PROOF STATE]
proof (state)
this:
\<phi>1s' = remdups \<phi>1s

goal (1 subgoal):
 1. prv (imp (ldsj \<phi>1s) (ldsj \<phi>2s))
[PROOF STEP]
have A: "set \<phi>1s' \<subseteq> set \<phi>2s" "distinct \<phi>1s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set \<phi>1s' \<subseteq> set \<phi>2s &&& distinct \<phi>1s'
[PROOF STEP]
unfolding \<phi>1s'
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (remdups \<phi>1s) \<subseteq> set \<phi>2s &&& distinct (remdups \<phi>1s)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
set \<phi>2s \<subseteq> fmla
set \<phi>1s \<subseteq> set \<phi>2s

goal (1 subgoal):
 1. set (remdups \<phi>1s) \<subseteq> set \<phi>2s &&& distinct (remdups \<phi>1s)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
set \<phi>1s' \<subseteq> set \<phi>2s
distinct \<phi>1s'

goal (1 subgoal):
 1. prv (imp (ldsj \<phi>1s) (ldsj \<phi>2s))
[PROOF STEP]
have B: "prv (imp (ldsj \<phi>1s') (ldsj \<phi>2s))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (imp (ldsj \<phi>1s') (ldsj \<phi>2s))
[PROOF STEP]
using \<phi>2s A
[PROOF STATE]
proof (prove)
using this:
set \<phi>2s \<subseteq> fmla
set \<phi>1s' \<subseteq> set \<phi>2s
distinct \<phi>1s'

goal (1 subgoal):
 1. prv (imp (ldsj \<phi>1s') (ldsj \<phi>2s))
[PROOF STEP]
proof(induction \<phi>2s arbitrary: \<phi>1s')
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>\<phi>1s'. \<lbrakk>set [] \<subseteq> fmla; set \<phi>1s' \<subseteq> set []; distinct \<phi>1s'\<rbrakk> \<Longrightarrow> prv (imp (ldsj \<phi>1s') (ldsj []))
 2. \<And>a \<phi>2s \<phi>1s'. \<lbrakk>\<And>\<phi>1s'. \<lbrakk>set \<phi>2s \<subseteq> fmla; set \<phi>1s' \<subseteq> set \<phi>2s; distinct \<phi>1s'\<rbrakk> \<Longrightarrow> prv (imp (ldsj \<phi>1s') (ldsj \<phi>2s)); set (a # \<phi>2s) \<subseteq> fmla; set \<phi>1s' \<subseteq> set (a # \<phi>2s); distinct \<phi>1s'\<rbrakk> \<Longrightarrow> prv (imp (ldsj \<phi>1s') (ldsj (a # \<phi>2s)))
[PROOF STEP]
case (Cons \<phi>2 \<phi>2s \<phi>1ss)
[PROOF STATE]
proof (state)
this:
\<lbrakk>set \<phi>2s \<subseteq> fmla; set ?\<phi>1s' \<subseteq> set \<phi>2s; distinct ?\<phi>1s'\<rbrakk> \<Longrightarrow> prv (imp (ldsj ?\<phi>1s') (ldsj \<phi>2s))
set (\<phi>2 # \<phi>2s) \<subseteq> fmla
set \<phi>1ss \<subseteq> set (\<phi>2 # \<phi>2s)
distinct \<phi>1ss

goal (2 subgoals):
 1. \<And>\<phi>1s'. \<lbrakk>set [] \<subseteq> fmla; set \<phi>1s' \<subseteq> set []; distinct \<phi>1s'\<rbrakk> \<Longrightarrow> prv (imp (ldsj \<phi>1s') (ldsj []))
 2. \<And>a \<phi>2s \<phi>1s'. \<lbrakk>\<And>\<phi>1s'. \<lbrakk>set \<phi>2s \<subseteq> fmla; set \<phi>1s' \<subseteq> set \<phi>2s; distinct \<phi>1s'\<rbrakk> \<Longrightarrow> prv (imp (ldsj \<phi>1s') (ldsj \<phi>2s)); set (a # \<phi>2s) \<subseteq> fmla; set \<phi>1s' \<subseteq> set (a # \<phi>2s); distinct \<phi>1s'\<rbrakk> \<Longrightarrow> prv (imp (ldsj \<phi>1s') (ldsj (a # \<phi>2s)))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (imp (ldsj \<phi>1ss) (ldsj (\<phi>2 # \<phi>2s)))
[PROOF STEP]
proof(cases "\<phi>2 \<in> set \<phi>1ss")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<phi>2 \<in> set \<phi>1ss \<Longrightarrow> prv (imp (ldsj \<phi>1ss) (ldsj (\<phi>2 # \<phi>2s)))
 2. \<phi>2 \<notin> set \<phi>1ss \<Longrightarrow> prv (imp (ldsj \<phi>1ss) (ldsj (\<phi>2 # \<phi>2s)))
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
\<phi>2 \<in> set \<phi>1ss

goal (2 subgoals):
 1. \<phi>2 \<in> set \<phi>1ss \<Longrightarrow> prv (imp (ldsj \<phi>1ss) (ldsj (\<phi>2 # \<phi>2s)))
 2. \<phi>2 \<notin> set \<phi>1ss \<Longrightarrow> prv (imp (ldsj \<phi>1ss) (ldsj (\<phi>2 # \<phi>2s)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<phi>2 \<in> set \<phi>1ss
[PROOF STEP]
obtain \<phi>1ss1 \<phi>1ss2 where \<phi>1ss: "\<phi>1ss = \<phi>1ss1 @ \<phi>2 # \<phi>1ss2"
[PROOF STATE]
proof (prove)
using this:
\<phi>2 \<in> set \<phi>1ss

goal (1 subgoal):
 1. (\<And>\<phi>1ss1 \<phi>1ss2. \<phi>1ss = \<phi>1ss1 @ \<phi>2 # \<phi>1ss2 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (meson split_list)
[PROOF STATE]
proof (state)
this:
\<phi>1ss = \<phi>1ss1 @ \<phi>2 # \<phi>1ss2

goal (2 subgoals):
 1. \<phi>2 \<in> set \<phi>1ss \<Longrightarrow> prv (imp (ldsj \<phi>1ss) (ldsj (\<phi>2 # \<phi>2s)))
 2. \<phi>2 \<notin> set \<phi>1ss \<Longrightarrow> prv (imp (ldsj \<phi>1ss) (ldsj (\<phi>2 # \<phi>2s)))
[PROOF STEP]
define \<phi>1s where \<phi>1s: "\<phi>1s \<equiv> \<phi>1ss1 @ \<phi>1ss2"
[PROOF STATE]
proof (state)
this:
\<phi>1s \<equiv> \<phi>1ss1 @ \<phi>1ss2

goal (2 subgoals):
 1. \<phi>2 \<in> set \<phi>1ss \<Longrightarrow> prv (imp (ldsj \<phi>1ss) (ldsj (\<phi>2 # \<phi>2s)))
 2. \<phi>2 \<notin> set \<phi>1ss \<Longrightarrow> prv (imp (ldsj \<phi>1ss) (ldsj (\<phi>2 # \<phi>2s)))
[PROOF STEP]
have nin: "\<phi>2 \<notin> set \<phi>1s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<phi>2 \<notin> set \<phi>1s
[PROOF STEP]
using \<phi>1ss \<open>distinct \<phi>1ss\<close>
[PROOF STATE]
proof (prove)
using this:
\<phi>1ss = \<phi>1ss1 @ \<phi>2 # \<phi>1ss2
distinct \<phi>1ss

goal (1 subgoal):
 1. \<phi>2 \<notin> set \<phi>1s
[PROOF STEP]
unfolding \<phi>1s
[PROOF STATE]
proof (prove)
using this:
\<phi>1ss = \<phi>1ss1 @ \<phi>2 # \<phi>1ss2
distinct \<phi>1ss

goal (1 subgoal):
 1. \<phi>2 \<notin> set (\<phi>1ss1 @ \<phi>1ss2)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<phi>2 \<notin> set \<phi>1s

goal (2 subgoals):
 1. \<phi>2 \<in> set \<phi>1ss \<Longrightarrow> prv (imp (ldsj \<phi>1ss) (ldsj (\<phi>2 # \<phi>2s)))
 2. \<phi>2 \<notin> set \<phi>1ss \<Longrightarrow> prv (imp (ldsj \<phi>1ss) (ldsj (\<phi>2 # \<phi>2s)))
[PROOF STEP]
have [intro!,simp]: "set \<phi>1s \<subseteq> fmla"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set \<phi>1s \<subseteq> fmla
[PROOF STEP]
unfolding \<phi>1s
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (\<phi>1ss1 @ \<phi>1ss2) \<subseteq> fmla
[PROOF STEP]
using \<phi>1ss Cons
[PROOF STATE]
proof (prove)
using this:
\<phi>1ss = \<phi>1ss1 @ \<phi>2 # \<phi>1ss2
\<lbrakk>set \<phi>2s \<subseteq> fmla; set ?\<phi>1s' \<subseteq> set \<phi>2s; distinct ?\<phi>1s'\<rbrakk> \<Longrightarrow> prv (imp (ldsj ?\<phi>1s') (ldsj \<phi>2s))
set (\<phi>2 # \<phi>2s) \<subseteq> fmla
set \<phi>1ss \<subseteq> set (\<phi>2 # \<phi>2s)
distinct \<phi>1ss

goal (1 subgoal):
 1. set (\<phi>1ss1 @ \<phi>1ss2) \<subseteq> fmla
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
set \<phi>1s \<subseteq> fmla

goal (2 subgoals):
 1. \<phi>2 \<in> set \<phi>1ss \<Longrightarrow> prv (imp (ldsj \<phi>1ss) (ldsj (\<phi>2 # \<phi>2s)))
 2. \<phi>2 \<notin> set \<phi>1ss \<Longrightarrow> prv (imp (ldsj \<phi>1ss) (ldsj (\<phi>2 # \<phi>2s)))
[PROOF STEP]
have 0: "prv (imp (ldsj \<phi>1ss) (dsj \<phi>2 (ldsj \<phi>1s)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (imp (ldsj \<phi>1ss) (dsj \<phi>2 (ldsj \<phi>1s)))
[PROOF STEP]
unfolding \<phi>1s \<phi>1ss
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (imp (ldsj (\<phi>1ss1 @ \<phi>2 # \<phi>1ss2)) (dsj \<phi>2 (ldsj (\<phi>1ss1 @ \<phi>1ss2))))
[PROOF STEP]
apply(rule prv_ldsj_imp_inner)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<phi>2 \<in> fmla
 2. set \<phi>1ss1 \<subseteq> fmla
 3. set \<phi>1ss2 \<subseteq> fmla
[PROOF STEP]
using Cons \<phi>1ss
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>set \<phi>2s \<subseteq> fmla; set ?\<phi>1s' \<subseteq> set \<phi>2s; distinct ?\<phi>1s'\<rbrakk> \<Longrightarrow> prv (imp (ldsj ?\<phi>1s') (ldsj \<phi>2s))
set (\<phi>2 # \<phi>2s) \<subseteq> fmla
set \<phi>1ss \<subseteq> set (\<phi>2 # \<phi>2s)
distinct \<phi>1ss
\<phi>1ss = \<phi>1ss1 @ \<phi>2 # \<phi>1ss2

goal (3 subgoals):
 1. \<phi>2 \<in> fmla
 2. set \<phi>1ss1 \<subseteq> fmla
 3. set \<phi>1ss2 \<subseteq> fmla
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
prv (imp (ldsj \<phi>1ss) (dsj \<phi>2 (ldsj \<phi>1s)))

goal (2 subgoals):
 1. \<phi>2 \<in> set \<phi>1ss \<Longrightarrow> prv (imp (ldsj \<phi>1ss) (ldsj (\<phi>2 # \<phi>2s)))
 2. \<phi>2 \<notin> set \<phi>1ss \<Longrightarrow> prv (imp (ldsj \<phi>1ss) (ldsj (\<phi>2 # \<phi>2s)))
[PROOF STEP]
have 1: "prv (imp (ldsj \<phi>1s) (ldsj \<phi>2s))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (imp (ldsj \<phi>1s) (ldsj \<phi>2s))
[PROOF STEP]
apply(rule Cons.IH)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. set \<phi>2s \<subseteq> fmla
 2. set \<phi>1s \<subseteq> set \<phi>2s
 3. distinct \<phi>1s
[PROOF STEP]
using nin Cons.prems True
[PROOF STATE]
proof (prove)
using this:
\<phi>2 \<notin> set \<phi>1s
set (\<phi>2 # \<phi>2s) \<subseteq> fmla
set \<phi>1ss \<subseteq> set (\<phi>2 # \<phi>2s)
distinct \<phi>1ss
\<phi>2 \<in> set \<phi>1ss

goal (3 subgoals):
 1. set \<phi>2s \<subseteq> fmla
 2. set \<phi>1s \<subseteq> set \<phi>2s
 3. distinct \<phi>1s
[PROOF STEP]
using \<phi>1s \<phi>1ss
[PROOF STATE]
proof (prove)
using this:
\<phi>2 \<notin> set \<phi>1s
set (\<phi>2 # \<phi>2s) \<subseteq> fmla
set \<phi>1ss \<subseteq> set (\<phi>2 # \<phi>2s)
distinct \<phi>1ss
\<phi>2 \<in> set \<phi>1ss
\<phi>1s \<equiv> \<phi>1ss1 @ \<phi>1ss2
\<phi>1ss = \<phi>1ss1 @ \<phi>2 # \<phi>1ss2

goal (3 subgoals):
 1. set \<phi>2s \<subseteq> fmla
 2. set \<phi>1s \<subseteq> set \<phi>2s
 3. distinct \<phi>1s
[PROOF STEP]
by  auto
[PROOF STATE]
proof (state)
this:
prv (imp (ldsj \<phi>1s) (ldsj \<phi>2s))

goal (2 subgoals):
 1. \<phi>2 \<in> set \<phi>1ss \<Longrightarrow> prv (imp (ldsj \<phi>1ss) (ldsj (\<phi>2 # \<phi>2s)))
 2. \<phi>2 \<notin> set \<phi>1ss \<Longrightarrow> prv (imp (ldsj \<phi>1ss) (ldsj (\<phi>2 # \<phi>2s)))
[PROOF STEP]
have 2: "prv (imp (dsj \<phi>2 (ldsj \<phi>1s)) (dsj \<phi>2 (ldsj \<phi>2s)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (imp (dsj \<phi>2 (ldsj \<phi>1s)) (dsj \<phi>2 (ldsj \<phi>2s)))
[PROOF STEP]
using Cons \<phi>1ss \<phi>1s 1
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>set \<phi>2s \<subseteq> fmla; set ?\<phi>1s' \<subseteq> set \<phi>2s; distinct ?\<phi>1s'\<rbrakk> \<Longrightarrow> prv (imp (ldsj ?\<phi>1s') (ldsj \<phi>2s))
set (\<phi>2 # \<phi>2s) \<subseteq> fmla
set \<phi>1ss \<subseteq> set (\<phi>2 # \<phi>2s)
distinct \<phi>1ss
\<phi>1ss = \<phi>1ss1 @ \<phi>2 # \<phi>1ss2
\<phi>1s \<equiv> \<phi>1ss1 @ \<phi>1ss2
prv (imp (ldsj \<phi>1s) (ldsj \<phi>2s))

goal (1 subgoal):
 1. prv (imp (dsj \<phi>2 (ldsj \<phi>1s)) (dsj \<phi>2 (ldsj \<phi>2s)))
[PROOF STEP]
apply(intro prv_dsj_mono)
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<lbrakk>\<And>\<phi>1s'. \<lbrakk>set \<phi>2s \<subseteq> fmla; set \<phi>1s' \<subseteq> set \<phi>2s; distinct \<phi>1s'\<rbrakk> \<Longrightarrow> prv (imp (ldsj \<phi>1s') (ldsj \<phi>2s)); set (\<phi>2 # \<phi>2s) \<subseteq> fmla; set \<phi>1ss \<subseteq> set (\<phi>2 # \<phi>2s); distinct \<phi>1ss; \<phi>1ss = \<phi>1ss1 @ \<phi>2 # \<phi>1ss2; \<phi>1s \<equiv> \<phi>1ss1 @ \<phi>1ss2; prv (imp (ldsj \<phi>1s) (ldsj \<phi>2s))\<rbrakk> \<Longrightarrow> \<phi>2 \<in> fmla
 2. \<lbrakk>\<And>\<phi>1s'. \<lbrakk>set \<phi>2s \<subseteq> fmla; set \<phi>1s' \<subseteq> set \<phi>2s; distinct \<phi>1s'\<rbrakk> \<Longrightarrow> prv (imp (ldsj \<phi>1s') (ldsj \<phi>2s)); set (\<phi>2 # \<phi>2s) \<subseteq> fmla; set \<phi>1ss \<subseteq> set (\<phi>2 # \<phi>2s); distinct \<phi>1ss; \<phi>1ss = \<phi>1ss1 @ \<phi>2 # \<phi>1ss2; \<phi>1s \<equiv> \<phi>1ss1 @ \<phi>1ss2; prv (imp (ldsj \<phi>1s) (ldsj \<phi>2s))\<rbrakk> \<Longrightarrow> ldsj \<phi>1s \<in> fmla
 3. \<lbrakk>\<And>\<phi>1s'. \<lbrakk>set \<phi>2s \<subseteq> fmla; set \<phi>1s' \<subseteq> set \<phi>2s; distinct \<phi>1s'\<rbrakk> \<Longrightarrow> prv (imp (ldsj \<phi>1s') (ldsj \<phi>2s)); set (\<phi>2 # \<phi>2s) \<subseteq> fmla; set \<phi>1ss \<subseteq> set (\<phi>2 # \<phi>2s); distinct \<phi>1ss; \<phi>1ss = \<phi>1ss1 @ \<phi>2 # \<phi>1ss2; \<phi>1s \<equiv> \<phi>1ss1 @ \<phi>1ss2; prv (imp (ldsj \<phi>1s) (ldsj \<phi>2s))\<rbrakk> \<Longrightarrow> \<phi>2 \<in> fmla
 4. \<lbrakk>\<And>\<phi>1s'. \<lbrakk>set \<phi>2s \<subseteq> fmla; set \<phi>1s' \<subseteq> set \<phi>2s; distinct \<phi>1s'\<rbrakk> \<Longrightarrow> prv (imp (ldsj \<phi>1s') (ldsj \<phi>2s)); set (\<phi>2 # \<phi>2s) \<subseteq> fmla; set \<phi>1ss \<subseteq> set (\<phi>2 # \<phi>2s); distinct \<phi>1ss; \<phi>1ss = \<phi>1ss1 @ \<phi>2 # \<phi>1ss2; \<phi>1s \<equiv> \<phi>1ss1 @ \<phi>1ss2; prv (imp (ldsj \<phi>1s) (ldsj \<phi>2s))\<rbrakk> \<Longrightarrow> ldsj \<phi>2s \<in> fmla
 5. \<lbrakk>\<And>\<phi>1s'. \<lbrakk>set \<phi>2s \<subseteq> fmla; set \<phi>1s' \<subseteq> set \<phi>2s; distinct \<phi>1s'\<rbrakk> \<Longrightarrow> prv (imp (ldsj \<phi>1s') (ldsj \<phi>2s)); set (\<phi>2 # \<phi>2s) \<subseteq> fmla; set \<phi>1ss \<subseteq> set (\<phi>2 # \<phi>2s); distinct \<phi>1ss; \<phi>1ss = \<phi>1ss1 @ \<phi>2 # \<phi>1ss2; \<phi>1s \<equiv> \<phi>1ss1 @ \<phi>1ss2; prv (imp (ldsj \<phi>1s) (ldsj \<phi>2s))\<rbrakk> \<Longrightarrow> prv (imp \<phi>2 \<phi>2)
 6. \<lbrakk>\<And>\<phi>1s'. \<lbrakk>set \<phi>2s \<subseteq> fmla; set \<phi>1s' \<subseteq> set \<phi>2s; distinct \<phi>1s'\<rbrakk> \<Longrightarrow> prv (imp (ldsj \<phi>1s') (ldsj \<phi>2s)); set (\<phi>2 # \<phi>2s) \<subseteq> fmla; set \<phi>1ss \<subseteq> set (\<phi>2 # \<phi>2s); distinct \<phi>1ss; \<phi>1ss = \<phi>1ss1 @ \<phi>2 # \<phi>1ss2; \<phi>1s \<equiv> \<phi>1ss1 @ \<phi>1ss2; prv (imp (ldsj \<phi>1s) (ldsj \<phi>2s))\<rbrakk> \<Longrightarrow> prv (imp (ldsj \<phi>1s) (ldsj \<phi>2s))
[PROOF STEP]
using prv_imp_refl
[PROOF STATE]
proof (prove)
using this:
?\<phi> \<in> fmla \<Longrightarrow> prv (imp ?\<phi> ?\<phi>)

goal (6 subgoals):
 1. \<lbrakk>\<And>\<phi>1s'. \<lbrakk>set \<phi>2s \<subseteq> fmla; set \<phi>1s' \<subseteq> set \<phi>2s; distinct \<phi>1s'\<rbrakk> \<Longrightarrow> prv (imp (ldsj \<phi>1s') (ldsj \<phi>2s)); set (\<phi>2 # \<phi>2s) \<subseteq> fmla; set \<phi>1ss \<subseteq> set (\<phi>2 # \<phi>2s); distinct \<phi>1ss; \<phi>1ss = \<phi>1ss1 @ \<phi>2 # \<phi>1ss2; \<phi>1s \<equiv> \<phi>1ss1 @ \<phi>1ss2; prv (imp (ldsj \<phi>1s) (ldsj \<phi>2s))\<rbrakk> \<Longrightarrow> \<phi>2 \<in> fmla
 2. \<lbrakk>\<And>\<phi>1s'. \<lbrakk>set \<phi>2s \<subseteq> fmla; set \<phi>1s' \<subseteq> set \<phi>2s; distinct \<phi>1s'\<rbrakk> \<Longrightarrow> prv (imp (ldsj \<phi>1s') (ldsj \<phi>2s)); set (\<phi>2 # \<phi>2s) \<subseteq> fmla; set \<phi>1ss \<subseteq> set (\<phi>2 # \<phi>2s); distinct \<phi>1ss; \<phi>1ss = \<phi>1ss1 @ \<phi>2 # \<phi>1ss2; \<phi>1s \<equiv> \<phi>1ss1 @ \<phi>1ss2; prv (imp (ldsj \<phi>1s) (ldsj \<phi>2s))\<rbrakk> \<Longrightarrow> ldsj \<phi>1s \<in> fmla
 3. \<lbrakk>\<And>\<phi>1s'. \<lbrakk>set \<phi>2s \<subseteq> fmla; set \<phi>1s' \<subseteq> set \<phi>2s; distinct \<phi>1s'\<rbrakk> \<Longrightarrow> prv (imp (ldsj \<phi>1s') (ldsj \<phi>2s)); set (\<phi>2 # \<phi>2s) \<subseteq> fmla; set \<phi>1ss \<subseteq> set (\<phi>2 # \<phi>2s); distinct \<phi>1ss; \<phi>1ss = \<phi>1ss1 @ \<phi>2 # \<phi>1ss2; \<phi>1s \<equiv> \<phi>1ss1 @ \<phi>1ss2; prv (imp (ldsj \<phi>1s) (ldsj \<phi>2s))\<rbrakk> \<Longrightarrow> \<phi>2 \<in> fmla
 4. \<lbrakk>\<And>\<phi>1s'. \<lbrakk>set \<phi>2s \<subseteq> fmla; set \<phi>1s' \<subseteq> set \<phi>2s; distinct \<phi>1s'\<rbrakk> \<Longrightarrow> prv (imp (ldsj \<phi>1s') (ldsj \<phi>2s)); set (\<phi>2 # \<phi>2s) \<subseteq> fmla; set \<phi>1ss \<subseteq> set (\<phi>2 # \<phi>2s); distinct \<phi>1ss; \<phi>1ss = \<phi>1ss1 @ \<phi>2 # \<phi>1ss2; \<phi>1s \<equiv> \<phi>1ss1 @ \<phi>1ss2; prv (imp (ldsj \<phi>1s) (ldsj \<phi>2s))\<rbrakk> \<Longrightarrow> ldsj \<phi>2s \<in> fmla
 5. \<lbrakk>\<And>\<phi>1s'. \<lbrakk>set \<phi>2s \<subseteq> fmla; set \<phi>1s' \<subseteq> set \<phi>2s; distinct \<phi>1s'\<rbrakk> \<Longrightarrow> prv (imp (ldsj \<phi>1s') (ldsj \<phi>2s)); set (\<phi>2 # \<phi>2s) \<subseteq> fmla; set \<phi>1ss \<subseteq> set (\<phi>2 # \<phi>2s); distinct \<phi>1ss; \<phi>1ss = \<phi>1ss1 @ \<phi>2 # \<phi>1ss2; \<phi>1s \<equiv> \<phi>1ss1 @ \<phi>1ss2; prv (imp (ldsj \<phi>1s) (ldsj \<phi>2s))\<rbrakk> \<Longrightarrow> prv (imp \<phi>2 \<phi>2)
 6. \<lbrakk>\<And>\<phi>1s'. \<lbrakk>set \<phi>2s \<subseteq> fmla; set \<phi>1s' \<subseteq> set \<phi>2s; distinct \<phi>1s'\<rbrakk> \<Longrightarrow> prv (imp (ldsj \<phi>1s') (ldsj \<phi>2s)); set (\<phi>2 # \<phi>2s) \<subseteq> fmla; set \<phi>1ss \<subseteq> set (\<phi>2 # \<phi>2s); distinct \<phi>1ss; \<phi>1ss = \<phi>1ss1 @ \<phi>2 # \<phi>1ss2; \<phi>1s \<equiv> \<phi>1ss1 @ \<phi>1ss2; prv (imp (ldsj \<phi>1s) (ldsj \<phi>2s))\<rbrakk> \<Longrightarrow> prv (imp (ldsj \<phi>1s) (ldsj \<phi>2s))
[PROOF STEP]
by auto blast+
[PROOF STATE]
proof (state)
this:
prv (imp (dsj \<phi>2 (ldsj \<phi>1s)) (dsj \<phi>2 (ldsj \<phi>2s)))

goal (2 subgoals):
 1. \<phi>2 \<in> set \<phi>1ss \<Longrightarrow> prv (imp (ldsj \<phi>1ss) (ldsj (\<phi>2 # \<phi>2s)))
 2. \<phi>2 \<notin> set \<phi>1ss \<Longrightarrow> prv (imp (ldsj \<phi>1ss) (ldsj (\<phi>2 # \<phi>2s)))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (imp (ldsj \<phi>1ss) (ldsj (\<phi>2 # \<phi>2s)))
[PROOF STEP]
using Cons
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>set \<phi>2s \<subseteq> fmla; set ?\<phi>1s' \<subseteq> set \<phi>2s; distinct ?\<phi>1s'\<rbrakk> \<Longrightarrow> prv (imp (ldsj ?\<phi>1s') (ldsj \<phi>2s))
set (\<phi>2 # \<phi>2s) \<subseteq> fmla
set \<phi>1ss \<subseteq> set (\<phi>2 # \<phi>2s)
distinct \<phi>1ss

goal (1 subgoal):
 1. prv (imp (ldsj \<phi>1ss) (ldsj (\<phi>2 # \<phi>2s)))
[PROOF STEP]
by (auto intro!: prv_prv_imp_trans[OF _ _ _ 0 2])
[PROOF STATE]
proof (state)
this:
prv (imp (ldsj \<phi>1ss) (ldsj (\<phi>2 # \<phi>2s)))

goal (1 subgoal):
 1. \<phi>2 \<notin> set \<phi>1ss \<Longrightarrow> prv (imp (ldsj \<phi>1ss) (ldsj (\<phi>2 # \<phi>2s)))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<phi>2 \<notin> set \<phi>1ss \<Longrightarrow> prv (imp (ldsj \<phi>1ss) (ldsj (\<phi>2 # \<phi>2s)))
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<phi>2 \<notin> set \<phi>1ss

goal (1 subgoal):
 1. \<phi>2 \<notin> set \<phi>1ss \<Longrightarrow> prv (imp (ldsj \<phi>1ss) (ldsj (\<phi>2 # \<phi>2s)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<phi>2 \<notin> set \<phi>1ss
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<phi>2 \<notin> set \<phi>1ss

goal (1 subgoal):
 1. prv (imp (ldsj \<phi>1ss) (ldsj (\<phi>2 # \<phi>2s)))
[PROOF STEP]
using Cons
[PROOF STATE]
proof (prove)
using this:
\<phi>2 \<notin> set \<phi>1ss
\<lbrakk>set \<phi>2s \<subseteq> fmla; set ?\<phi>1s' \<subseteq> set \<phi>2s; distinct ?\<phi>1s'\<rbrakk> \<Longrightarrow> prv (imp (ldsj ?\<phi>1s') (ldsj \<phi>2s))
set (\<phi>2 # \<phi>2s) \<subseteq> fmla
set \<phi>1ss \<subseteq> set (\<phi>2 # \<phi>2s)
distinct \<phi>1ss

goal (1 subgoal):
 1. prv (imp (ldsj \<phi>1ss) (ldsj (\<phi>2 # \<phi>2s)))
[PROOF STEP]
by (meson ldsj order.trans prv_imp_ldsj_in prv_ldsj_imp subset_code(1))
[PROOF STATE]
proof (state)
this:
prv (imp (ldsj \<phi>1ss) (ldsj (\<phi>2 # \<phi>2s)))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
prv (imp (ldsj \<phi>1ss) (ldsj (\<phi>2 # \<phi>2s)))

goal (1 subgoal):
 1. \<And>\<phi>1s'. \<lbrakk>set [] \<subseteq> fmla; set \<phi>1s' \<subseteq> set []; distinct \<phi>1s'\<rbrakk> \<Longrightarrow> prv (imp (ldsj \<phi>1s') (ldsj []))
[PROOF STEP]
qed(simp add: prv_imp_refl)
[PROOF STATE]
proof (state)
this:
prv (imp (ldsj \<phi>1s') (ldsj \<phi>2s))

goal (1 subgoal):
 1. prv (imp (ldsj \<phi>1s) (ldsj \<phi>2s))
[PROOF STEP]
have C: "prv (imp (ldsj \<phi>1s) (ldsj \<phi>1s'))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (imp (ldsj \<phi>1s) (ldsj \<phi>1s'))
[PROOF STEP]
unfolding \<phi>1s'
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (imp (ldsj \<phi>1s) (ldsj (remdups \<phi>1s)))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
set \<phi>2s \<subseteq> fmla
set \<phi>1s \<subseteq> set \<phi>2s

goal (1 subgoal):
 1. prv (imp (ldsj \<phi>1s) (ldsj (remdups \<phi>1s)))
[PROOF STEP]
by (intro prv_ldsj_imp_remdups) auto
[PROOF STATE]
proof (state)
this:
prv (imp (ldsj \<phi>1s) (ldsj \<phi>1s'))

goal (1 subgoal):
 1. prv (imp (ldsj \<phi>1s) (ldsj \<phi>2s))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (imp (ldsj \<phi>1s) (ldsj \<phi>2s))
[PROOF STEP]
using A assms
[PROOF STATE]
proof (prove)
using this:
set \<phi>1s' \<subseteq> set \<phi>2s
distinct \<phi>1s'
set \<phi>2s \<subseteq> fmla
set \<phi>1s \<subseteq> set \<phi>2s

goal (1 subgoal):
 1. prv (imp (ldsj \<phi>1s) (ldsj \<phi>2s))
[PROOF STEP]
by (intro prv_prv_imp_trans[OF _ _ _ C B]) auto
[PROOF STATE]
proof (state)
this:
prv (imp (ldsj \<phi>1s) (ldsj \<phi>2s))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma prv_ldsj_eqv:
assumes "set \<phi>1s \<subseteq> fmla" and "set \<phi>2s = set \<phi>1s"
shows "prv (eqv (ldsj \<phi>1s) (ldsj \<phi>2s))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (eqv (ldsj \<phi>1s) (ldsj \<phi>2s))
[PROOF STEP]
using assms prv_ldsj_mono
[PROOF STATE]
proof (prove)
using this:
set \<phi>1s \<subseteq> fmla
set \<phi>2s = set \<phi>1s
\<lbrakk>set ?\<phi>2s \<subseteq> fmla; set ?\<phi>1s \<subseteq> set ?\<phi>2s\<rbrakk> \<Longrightarrow> prv (imp (ldsj ?\<phi>1s) (ldsj ?\<phi>2s))

goal (1 subgoal):
 1. prv (eqv (ldsj \<phi>1s) (ldsj \<phi>2s))
[PROOF STEP]
by (intro prv_eqvI) auto


[STATEMENT]
lemma prv_ldsj_mono_imp:
  assumes "set \<phi>1s \<subseteq> fmla" "set \<phi>2s \<subseteq> fmla" and "\<forall> \<phi>1 \<in> set \<phi>1s. \<exists> \<phi>2 \<in> set \<phi>2s. prv (imp \<phi>1 \<phi>2)"
  shows "prv (imp (ldsj \<phi>1s) (ldsj \<phi>2s))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (imp (ldsj \<phi>1s) (ldsj \<phi>2s))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
set \<phi>1s \<subseteq> fmla
set \<phi>2s \<subseteq> fmla
\<forall>\<phi>1\<in>set \<phi>1s. \<exists>\<phi>2\<in>set \<phi>2s. prv (imp \<phi>1 \<phi>2)

goal (1 subgoal):
 1. prv (imp (ldsj \<phi>1s) (ldsj \<phi>2s))
[PROOF STEP]
apply(intro prv_ldsj_imp)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>set \<phi>1s \<subseteq> fmla; set \<phi>2s \<subseteq> fmla; \<forall>\<phi>1\<in>set \<phi>1s. \<exists>\<phi>2\<in>set \<phi>2s. prv (imp \<phi>1 \<phi>2)\<rbrakk> \<Longrightarrow> ldsj \<phi>2s \<in> fmla
 2. \<lbrakk>set \<phi>1s \<subseteq> fmla; set \<phi>2s \<subseteq> fmla; \<forall>\<phi>1\<in>set \<phi>1s. \<exists>\<phi>2\<in>set \<phi>2s. prv (imp \<phi>1 \<phi>2)\<rbrakk> \<Longrightarrow> set \<phi>1s \<subseteq> fmla
 3. \<And>\<phi>. \<lbrakk>set \<phi>1s \<subseteq> fmla; set \<phi>2s \<subseteq> fmla; \<forall>\<phi>1\<in>set \<phi>1s. \<exists>\<phi>2\<in>set \<phi>2s. prv (imp \<phi>1 \<phi>2); \<phi> \<in> set \<phi>1s\<rbrakk> \<Longrightarrow> prv (imp \<phi> (ldsj \<phi>2s))
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>set \<phi>1s \<subseteq> fmla; set \<phi>2s \<subseteq> fmla; \<forall>\<phi>1\<in>set \<phi>1s. \<exists>\<phi>2\<in>set \<phi>2s. prv (imp \<phi>1 \<phi>2)\<rbrakk> \<Longrightarrow> ldsj \<phi>2s \<in> fmla
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>set \<phi>1s \<subseteq> fmla; set \<phi>2s \<subseteq> fmla; \<forall>\<phi>1\<in>set \<phi>1s. \<exists>\<phi>2\<in>set \<phi>2s. prv (imp \<phi>1 \<phi>2)\<rbrakk> \<Longrightarrow> set \<phi>1s \<subseteq> fmla
 2. \<And>\<phi>. \<lbrakk>set \<phi>1s \<subseteq> fmla; set \<phi>2s \<subseteq> fmla; \<forall>\<phi>1\<in>set \<phi>1s. \<exists>\<phi>2\<in>set \<phi>2s. prv (imp \<phi>1 \<phi>2); \<phi> \<in> set \<phi>1s\<rbrakk> \<Longrightarrow> prv (imp \<phi> (ldsj \<phi>2s))
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>set \<phi>1s \<subseteq> fmla; set \<phi>2s \<subseteq> fmla; \<forall>\<phi>1\<in>set \<phi>1s. \<exists>\<phi>2\<in>set \<phi>2s. prv (imp \<phi>1 \<phi>2)\<rbrakk> \<Longrightarrow> set \<phi>1s \<subseteq> fmla
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>\<phi>. \<lbrakk>set \<phi>1s \<subseteq> fmla; set \<phi>2s \<subseteq> fmla; \<forall>\<phi>1\<in>set \<phi>1s. \<exists>\<phi>2\<in>set \<phi>2s. prv (imp \<phi>1 \<phi>2); \<phi> \<in> set \<phi>1s\<rbrakk> \<Longrightarrow> prv (imp \<phi> (ldsj \<phi>2s))
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>set \<phi>1s \<subseteq> fmla; set \<phi>2s \<subseteq> fmla; \<forall>\<phi>1\<in>set \<phi>1s. \<exists>\<phi>2\<in>set \<phi>2s. prv (imp \<phi>1 \<phi>2); \<phi>_ \<in> set \<phi>1s\<rbrakk> \<Longrightarrow> prv (imp \<phi>_ (ldsj \<phi>2s))
[PROOF STEP]
using prv_imp_ldsj
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?\<chi> \<in> fmla; set ?\<phi>s \<subseteq> fmla; ?\<phi> \<in> set ?\<phi>s; prv (imp ?\<chi> ?\<phi>)\<rbrakk> \<Longrightarrow> prv (imp ?\<chi> (ldsj ?\<phi>s))

goal (1 subgoal):
 1. \<lbrakk>set \<phi>1s \<subseteq> fmla; set \<phi>2s \<subseteq> fmla; \<forall>\<phi>1\<in>set \<phi>1s. \<exists>\<phi>2\<in>set \<phi>2s. prv (imp \<phi>1 \<phi>2); \<phi>_ \<in> set \<phi>1s\<rbrakk> \<Longrightarrow> prv (imp \<phi>_ (ldsj \<phi>2s))
[PROOF STEP]
by blast
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
.


[STATEMENT]
lemma prv_subst_sdsj:
"F \<subseteq> fmla \<Longrightarrow> finite F \<Longrightarrow> t \<in> trm \<Longrightarrow> x \<in> var \<Longrightarrow>
 prv (eqv (subst (sdsj F) t x) (sdsj ((\<lambda>\<phi>. subst \<phi> t x) ` F)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>F \<subseteq> fmla; finite F; t \<in> trm; x \<in> var\<rbrakk> \<Longrightarrow> prv (eqv (subst (sdsj F) t x) (sdsj ((\<lambda>\<phi>. subst \<phi> t x) ` F)))
[PROOF STEP]
unfolding sdsj_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>F \<subseteq> fmla; finite F; t \<in> trm; x \<in> var\<rbrakk> \<Longrightarrow> prv (eqv (subst (ldsj (asList F)) t x) (ldsj (asList ((\<lambda>\<phi>. subst \<phi> t x) ` F))))
[PROOF STEP]
by (fastforce intro!: prv_ldsj_eqv)


[STATEMENT]
lemma prv_imp_sdsj_in:
  assumes "\<phi> \<in> fmla" and "F \<subseteq> fmla" "finite F"
  and "\<phi> \<in> F"
  shows "prv (imp \<phi> (sdsj F))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (imp \<phi> (sdsj F))
[PROOF STEP]
unfolding sdsj_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (imp \<phi> (ldsj (asList F)))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<phi> \<in> fmla
F \<subseteq> fmla
finite F
\<phi> \<in> F

goal (1 subgoal):
 1. prv (imp \<phi> (ldsj (asList F)))
[PROOF STEP]
by (intro prv_imp_ldsj_in) auto


[STATEMENT]
lemma prv_imp_sdsj:
assumes "\<chi> \<in> fmla" and "F \<subseteq> fmla" "finite F"
and "\<phi> \<in> F" and "prv (imp \<chi> \<phi>)"
shows "prv (imp \<chi> (sdsj F))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (imp \<chi> (sdsj F))
[PROOF STEP]
unfolding sdsj_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (imp \<chi> (ldsj (asList F)))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<chi> \<in> fmla
F \<subseteq> fmla
finite F
\<phi> \<in> F
prv (imp \<chi> \<phi>)

goal (1 subgoal):
 1. prv (imp \<chi> (ldsj (asList F)))
[PROOF STEP]
by (intro prv_imp_ldsj) auto


[STATEMENT]
lemma prv_sdsj_imp:
  assumes "\<chi> \<in> fmla" and "F \<subseteq> fmla" "finite F"
  and "\<And>\<phi>. \<phi> \<in> F \<Longrightarrow> prv (imp \<phi> \<chi>)"
  shows "prv (imp (sdsj F) \<chi>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (imp (sdsj F) \<chi>)
[PROOF STEP]
unfolding sdsj_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (imp (ldsj (asList F)) \<chi>)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<chi> \<in> fmla
F \<subseteq> fmla
finite F
?\<phi> \<in> F \<Longrightarrow> prv (imp ?\<phi> \<chi>)

goal (1 subgoal):
 1. prv (imp (ldsj (asList F)) \<chi>)
[PROOF STEP]
by (intro prv_ldsj_imp) auto


[STATEMENT]
lemma prv_sdsj_mono:
assumes "F2 \<subseteq> fmla" and "F1 \<subseteq> F2" and "finite F2"
shows "prv (imp (sdsj F1) (sdsj F2))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (imp (sdsj F1) (sdsj F2))
[PROOF STEP]
unfolding sdsj_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (imp (ldsj (asList F1)) (ldsj (asList F2)))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
F2 \<subseteq> fmla
F1 \<subseteq> F2
finite F2

goal (1 subgoal):
 1. prv (imp (ldsj (asList F1)) (ldsj (asList F2)))
[PROOF STEP]
apply(intro prv_ldsj_mono)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>F2 \<subseteq> fmla; F1 \<subseteq> F2; finite F2\<rbrakk> \<Longrightarrow> set (asList F2) \<subseteq> fmla
 2. \<lbrakk>F2 \<subseteq> fmla; F1 \<subseteq> F2; finite F2\<rbrakk> \<Longrightarrow> set (asList F1) \<subseteq> set (asList F2)
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>F2 \<subseteq> fmla; F1 \<subseteq> F2; finite F2\<rbrakk> \<Longrightarrow> set (asList F2) \<subseteq> fmla
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>F2 \<subseteq> fmla; F1 \<subseteq> F2; finite F2\<rbrakk> \<Longrightarrow> set (asList F1) \<subseteq> set (asList F2)
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>F2 \<subseteq> fmla; F1 \<subseteq> F2; finite F2\<rbrakk> \<Longrightarrow> set (asList F1) \<subseteq> set (asList F2)
[PROOF STEP]
by (metis asList infinite_super)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
.


[STATEMENT]
lemma prv_sdsj_mono_imp:
  assumes "F1 \<subseteq> fmla" "F2 \<subseteq> fmla" "finite F1" "finite F2"
  and "\<forall> \<phi>1 \<in> F1. \<exists> \<phi>2 \<in> F2. prv (imp \<phi>1 \<phi>2)"
  shows "prv (imp (sdsj F1) (sdsj F2))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (imp (sdsj F1) (sdsj F2))
[PROOF STEP]
unfolding sdsj_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (imp (ldsj (asList F1)) (ldsj (asList F2)))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
F1 \<subseteq> fmla
F2 \<subseteq> fmla
finite F1
finite F2
\<forall>\<phi>1\<in>F1. \<exists>\<phi>2\<in>F2. prv (imp \<phi>1 \<phi>2)

goal (1 subgoal):
 1. prv (imp (ldsj (asList F1)) (ldsj (asList F2)))
[PROOF STEP]
by (intro prv_ldsj_mono_imp) auto


[STATEMENT]
lemma prv_sdsj_cases:
assumes "F \<subseteq> fmla" "finite F" "\<psi> \<in> fmla"
and "prv (sdsj F)" and "\<And> \<phi>. \<phi> \<in> F \<Longrightarrow> prv (imp \<phi> \<psi>)"
shows "prv \<psi>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv \<psi>
[PROOF STEP]
by (meson assms prv_imp_mp prv_sdsj_imp sdsj)


[STATEMENT]
lemma prv_sdsj1_imp:
"\<phi> \<in> fmla \<Longrightarrow> prv (imp (sdsj {\<phi>}) \<phi>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<phi> \<in> fmla \<Longrightarrow> prv (imp (sdsj {\<phi>}) \<phi>)
[PROOF STEP]
using prv_imp_refl prv_sdsj_imp
[PROOF STATE]
proof (prove)
using this:
?\<phi> \<in> fmla \<Longrightarrow> prv (imp ?\<phi> ?\<phi>)
\<lbrakk>?\<chi> \<in> fmla; ?F \<subseteq> fmla; finite ?F; \<And>\<phi>. \<phi> \<in> ?F \<Longrightarrow> prv (imp \<phi> ?\<chi>)\<rbrakk> \<Longrightarrow> prv (imp (sdsj ?F) ?\<chi>)

goal (1 subgoal):
 1. \<phi> \<in> fmla \<Longrightarrow> prv (imp (sdsj {\<phi>}) \<phi>)
[PROOF STEP]
by fastforce


[STATEMENT]
lemma prv_imp_sdsj1:
"\<phi> \<in> fmla \<Longrightarrow> prv (imp \<phi> (sdsj {\<phi>}))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<phi> \<in> fmla \<Longrightarrow> prv (imp \<phi> (sdsj {\<phi>}))
[PROOF STEP]
using prv_imp_refl prv_imp_sdsj
[PROOF STATE]
proof (prove)
using this:
?\<phi> \<in> fmla \<Longrightarrow> prv (imp ?\<phi> ?\<phi>)
\<lbrakk>?\<chi> \<in> fmla; ?F \<subseteq> fmla; finite ?F; ?\<phi> \<in> ?F; prv (imp ?\<chi> ?\<phi>)\<rbrakk> \<Longrightarrow> prv (imp ?\<chi> (sdsj ?F))

goal (1 subgoal):
 1. \<phi> \<in> fmla \<Longrightarrow> prv (imp \<phi> (sdsj {\<phi>}))
[PROOF STEP]
by fastforce


[STATEMENT]
lemma prv_sdsj2_imp_dsj:
"\<phi> \<in> fmla \<Longrightarrow> \<psi> \<in> fmla \<Longrightarrow> prv (imp (sdsj {\<phi>,\<psi>}) (dsj \<phi> \<psi>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<phi> \<in> fmla; \<psi> \<in> fmla\<rbrakk> \<Longrightarrow> prv (imp (sdsj {\<phi>, \<psi>}) (dsj \<phi> \<psi>))
[PROOF STEP]
using prv_dsj_impL prv_dsj_impR prv_sdsj_imp
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?\<phi> \<in> fmla; ?\<chi> \<in> fmla\<rbrakk> \<Longrightarrow> prv (imp ?\<phi> (dsj ?\<phi> ?\<chi>))
\<lbrakk>?\<phi> \<in> fmla; ?\<chi> \<in> fmla\<rbrakk> \<Longrightarrow> prv (imp ?\<chi> (dsj ?\<phi> ?\<chi>))
\<lbrakk>?\<chi> \<in> fmla; ?F \<subseteq> fmla; finite ?F; \<And>\<phi>. \<phi> \<in> ?F \<Longrightarrow> prv (imp \<phi> ?\<chi>)\<rbrakk> \<Longrightarrow> prv (imp (sdsj ?F) ?\<chi>)

goal (1 subgoal):
 1. \<lbrakk>\<phi> \<in> fmla; \<psi> \<in> fmla\<rbrakk> \<Longrightarrow> prv (imp (sdsj {\<phi>, \<psi>}) (dsj \<phi> \<psi>))
[PROOF STEP]
by fastforce


[STATEMENT]
lemma prv_dsj_imp_sdsj2:
"\<phi> \<in> fmla \<Longrightarrow> \<psi> \<in> fmla \<Longrightarrow> prv (imp (dsj \<phi> \<psi>) (sdsj {\<phi>,\<psi>}))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<phi> \<in> fmla; \<psi> \<in> fmla\<rbrakk> \<Longrightarrow> prv (imp (dsj \<phi> \<psi>) (sdsj {\<phi>, \<psi>}))
[PROOF STEP]
by (simp add: prv_imp_dsjEE prv_imp_sdsj_in)