[STATEMENT]
lemma nprv_clear5_3:
"nprv {\<phi>1,\<phi>2,\<phi>4,\<phi>5} \<psi> \<Longrightarrow> \<phi>1 \<in> fmla \<Longrightarrow> \<phi>2 \<in> fmla \<Longrightarrow> \<phi>3 \<in> fmla \<Longrightarrow> \<phi>4 \<in> fmla \<Longrightarrow> \<phi>5 \<in> fmla \<Longrightarrow> \<psi> \<in> fmla \<Longrightarrow>
 nprv {\<phi>1,\<phi>2,\<phi>3,\<phi>4,\<phi>5} \<psi>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>nprv {\<phi>1, \<phi>2, \<phi>4, \<phi>5} \<psi>; \<phi>1 \<in> fmla; \<phi>2 \<in> fmla; \<phi>3 \<in> fmla; \<phi>4 \<in> fmla; \<phi>5 \<in> fmla; \<psi> \<in> fmla\<rbrakk> \<Longrightarrow> nprv {\<phi>1, \<phi>2, \<phi>3, \<phi>4, \<phi>5} \<psi>
[PROOF STEP]
by (rule nprv_mono) auto


[STATEMENT]
lemma nprv_clear5_4:
"nprv {\<phi>1,\<phi>2,\<phi>3,\<phi>5} \<psi> \<Longrightarrow> \<phi>1 \<in> fmla \<Longrightarrow> \<phi>2 \<in> fmla \<Longrightarrow> \<phi>3 \<in> fmla \<Longrightarrow> \<phi>4 \<in> fmla \<Longrightarrow> \<phi>5 \<in> fmla \<Longrightarrow> \<psi> \<in> fmla \<Longrightarrow>
 nprv {\<phi>1,\<phi>2,\<phi>3,\<phi>4,\<phi>5} \<psi>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>nprv {\<phi>1, \<phi>2, \<phi>3, \<phi>5} \<psi>; \<phi>1 \<in> fmla; \<phi>2 \<in> fmla; \<phi>3 \<in> fmla; \<phi>4 \<in> fmla; \<phi>5 \<in> fmla; \<psi> \<in> fmla\<rbrakk> \<Longrightarrow> nprv {\<phi>1, \<phi>2, \<phi>3, \<phi>4, \<phi>5} \<psi>
[PROOF STEP]
by (rule nprv_mono) auto


[STATEMENT]
lemma nprv_clear5_5:
"nprv {\<phi>1,\<phi>2,\<phi>3,\<phi>4} \<psi> \<Longrightarrow> \<phi>1 \<in> fmla \<Longrightarrow> \<phi>2 \<in> fmla \<Longrightarrow> \<phi>3 \<in> fmla \<Longrightarrow> \<phi>4 \<in> fmla \<Longrightarrow> \<phi>5 \<in> fmla \<Longrightarrow> \<psi> \<in> fmla \<Longrightarrow>
 nprv {\<phi>1,\<phi>2,\<phi>3,\<phi>4,\<phi>5} \<psi>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>nprv {\<phi>1, \<phi>2, \<phi>3, \<phi>4} \<psi>; \<phi>1 \<in> fmla; \<phi>2 \<in> fmla; \<phi>3 \<in> fmla; \<phi>4 \<in> fmla; \<phi>5 \<in> fmla; \<psi> \<in> fmla\<rbrakk> \<Longrightarrow> nprv {\<phi>1, \<phi>2, \<phi>3, \<phi>4, \<phi>5} \<psi>
[PROOF STEP]
by (rule nprv_mono) auto


[STATEMENT]
lemma nprv_subst:
assumes "x \<in> var" "t \<in> trm" "\<psi> \<in> fmla" "finite F" "F \<subseteq> fmla"
and 1: "nprv F \<psi>"
shows "nprv ((\<lambda>\<phi>. subst \<phi> t x) ` F) (subst \<psi> t x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nprv ((\<lambda>\<phi>. subst \<phi> t x) ` F) (subst \<psi> t x)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
x \<in> var
t \<in> trm
\<psi> \<in> fmla
finite F
F \<subseteq> fmla
nprv F \<psi>

goal (1 subgoal):
 1. nprv ((\<lambda>\<phi>. subst \<phi> t x) ` F) (subst \<psi> t x)
[PROOF STEP]
using prv_subst[OF _ _ _ 1[unfolded nprv_def]]
[PROOF STATE]
proof (prove)
using this:
x \<in> var
t \<in> trm
\<psi> \<in> fmla
finite F
F \<subseteq> fmla
nprv F \<psi>
\<lbrakk>?x \<in> var; imp (scnj F) \<psi> \<in> fmla; ?t \<in> trm\<rbrakk> \<Longrightarrow> prv (subst (imp (scnj F) \<psi>) ?t ?x)

goal (1 subgoal):
 1. nprv ((\<lambda>\<phi>. subst \<phi> t x) ` F) (subst \<psi> t x)
[PROOF STEP]
unfolding nprv_def
[PROOF STATE]
proof (prove)
using this:
x \<in> var
t \<in> trm
\<psi> \<in> fmla
finite F
F \<subseteq> fmla
prv (imp (scnj F) \<psi>)
\<lbrakk>?x \<in> var; imp (scnj F) \<psi> \<in> fmla; ?t \<in> trm\<rbrakk> \<Longrightarrow> prv (subst (imp (scnj F) \<psi>) ?t ?x)

goal (1 subgoal):
 1. prv (imp (scnj ((\<lambda>\<phi>. subst \<phi> t x) ` F)) (subst \<psi> t x))
[PROOF STEP]
by (intro prv_prv_imp_trans[OF _ _ _ prv_subst_scnj_imp]) auto


[STATEMENT]
lemma nprv_subst_fresh:
assumes 0: "x \<in> var" "t \<in> trm" "\<psi> \<in> fmla" "finite F" "F \<subseteq> fmla"
"nprv F \<psi>" and 1: "x \<notin> \<Union> (Fvars ` F)"
shows "nprv F (subst \<psi> t x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nprv F (subst \<psi> t x)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. nprv F (subst \<psi> t x)
[PROOF STEP]
have 2: "(\<lambda>\<phi>. subst \<phi> t x) ` F = F"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>\<phi>. subst \<phi> t x) ` F = F
[PROOF STEP]
unfolding image_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {y. \<exists>xa\<in>F. y = subst xa t x} = F
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
x \<in> var
t \<in> trm
\<psi> \<in> fmla
finite F
F \<subseteq> fmla
nprv F \<psi>
x \<notin> \<Union> (Fvars ` F)

goal (1 subgoal):
 1. {y. \<exists>xa\<in>F. y = subst xa t x} = F
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
(\<lambda>\<phi>. subst \<phi> t x) ` F = F

goal (1 subgoal):
 1. nprv F (subst \<psi> t x)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nprv F (subst \<psi> t x)
[PROOF STEP]
using nprv_subst[OF 0]
[PROOF STATE]
proof (prove)
using this:
nprv ((\<lambda>\<phi>. subst \<phi> t x) ` F) (subst \<psi> t x)

goal (1 subgoal):
 1. nprv F (subst \<psi> t x)
[PROOF STEP]
unfolding 2
[PROOF STATE]
proof (prove)
using this:
nprv F (subst \<psi> t x)

goal (1 subgoal):
 1. nprv F (subst \<psi> t x)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
nprv F (subst \<psi> t x)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma nprv_subst_rev:
assumes 0: "x \<in> var" "y \<in> var" "\<psi> \<in> fmla" "finite F" "F \<subseteq> fmla"
and f: "y = x \<or> (y \<notin> Fvars \<psi> \<and> y \<notin> \<Union> (Fvars ` F))"
and 1: "nprv ((\<lambda>\<phi>. subst \<phi> (Var y) x) ` F) (subst \<psi> (Var y) x)"
shows "nprv F \<psi>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nprv F \<psi>
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. nprv F \<psi>
[PROOF STEP]
have 0: "subst (subst \<psi> (Var y) x) (Var x) y = \<psi>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. subst (subst \<psi> (Var y) x) (Var x) y = \<psi>
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
x \<in> var
y \<in> var
\<psi> \<in> fmla
finite F
F \<subseteq> fmla
y = x \<or> y \<notin> Fvars \<psi> \<and> y \<notin> \<Union> (Fvars ` F)
nprv ((\<lambda>\<phi>. subst \<phi> (Var y) x) ` F) (subst \<psi> (Var y) x)

goal (1 subgoal):
 1. subst (subst \<psi> (Var y) x) (Var x) y = \<psi>
[PROOF STEP]
by (auto simp: subst_compose_eq_or)
[PROOF STATE]
proof (state)
this:
subst (subst \<psi> (Var y) x) (Var x) y = \<psi>

goal (1 subgoal):
 1. nprv F \<psi>
[PROOF STEP]
have "nprv ((\<lambda>\<phi>. subst \<phi> (Var x) y) ` (\<lambda>\<phi>. subst \<phi> (Var y) x) ` F) \<psi>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nprv ((\<lambda>\<phi>. subst \<phi> (Var x) y) ` (\<lambda>\<phi>. subst \<phi> (Var y) x) ` F) \<psi>
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
x \<in> var
y \<in> var
\<psi> \<in> fmla
finite F
F \<subseteq> fmla
y = x \<or> y \<notin> Fvars \<psi> \<and> y \<notin> \<Union> (Fvars ` F)
nprv ((\<lambda>\<phi>. subst \<phi> (Var y) x) ` F) (subst \<psi> (Var y) x)

goal (1 subgoal):
 1. nprv ((\<lambda>\<phi>. subst \<phi> (Var x) y) ` (\<lambda>\<phi>. subst \<phi> (Var y) x) ` F) \<psi>
[PROOF STEP]
apply(subst 0[symmetric])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> var; y \<in> var; \<psi> \<in> fmla; finite F; F \<subseteq> fmla; y = x \<or> y \<notin> Fvars \<psi> \<and> y \<notin> \<Union> (Fvars ` F); nprv ((\<lambda>\<phi>. subst \<phi> (Var y) x) ` F) (subst \<psi> (Var y) x)\<rbrakk> \<Longrightarrow> nprv ((\<lambda>\<phi>. subst \<phi> (Var x) y) ` (\<lambda>\<phi>. subst \<phi> (Var y) x) ` F) (subst (subst \<psi> (Var y) x) (Var x) y)
[PROOF STEP]
by (rule nprv_subst) auto
[PROOF STATE]
proof (state)
this:
nprv ((\<lambda>\<phi>. subst \<phi> (Var x) y) ` (\<lambda>\<phi>. subst \<phi> (Var y) x) ` F) \<psi>

goal (1 subgoal):
 1. nprv F \<psi>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
nprv ((\<lambda>\<phi>. subst \<phi> (Var x) y) ` (\<lambda>\<phi>. subst \<phi> (Var y) x) ` F) \<psi>

goal (1 subgoal):
 1. nprv F \<psi>
[PROOF STEP]
have "prv (imp (scnj F)
                 (scnj ((\<lambda>\<phi>. subst \<phi> (Var x) y) ` (\<lambda>\<phi>. subst \<phi> (Var y) x) ` F)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (imp (scnj F) (scnj ((\<lambda>\<phi>. subst \<phi> (Var x) y) ` (\<lambda>\<phi>. subst \<phi> (Var y) x) ` F)))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
x \<in> var
y \<in> var
\<psi> \<in> fmla
finite F
F \<subseteq> fmla
y = x \<or> y \<notin> Fvars \<psi> \<and> y \<notin> \<Union> (Fvars ` F)
nprv ((\<lambda>\<phi>. subst \<phi> (Var y) x) ` F) (subst \<psi> (Var y) x)

goal (1 subgoal):
 1. prv (imp (scnj F) (scnj ((\<lambda>\<phi>. subst \<phi> (Var x) y) ` (\<lambda>\<phi>. subst \<phi> (Var y) x) ` F)))
[PROOF STEP]
apply(intro prv_scnj_mono_imp)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<lbrakk>x \<in> var; y \<in> var; \<psi> \<in> fmla; finite F; F \<subseteq> fmla; y = x \<or> y \<notin> Fvars \<psi> \<and> y \<notin> \<Union> (Fvars ` F); nprv ((\<lambda>\<phi>. subst \<phi> (Var y) x) ` F) (subst \<psi> (Var y) x)\<rbrakk> \<Longrightarrow> F \<subseteq> fmla
 2. \<lbrakk>x \<in> var; y \<in> var; \<psi> \<in> fmla; finite F; F \<subseteq> fmla; y = x \<or> y \<notin> Fvars \<psi> \<and> y \<notin> \<Union> (Fvars ` F); nprv ((\<lambda>\<phi>. subst \<phi> (Var y) x) ` F) (subst \<psi> (Var y) x)\<rbrakk> \<Longrightarrow> (\<lambda>\<phi>. subst \<phi> (Var x) y) ` (\<lambda>\<phi>. subst \<phi> (Var y) x) ` F \<subseteq> fmla
 3. \<lbrakk>x \<in> var; y \<in> var; \<psi> \<in> fmla; finite F; F \<subseteq> fmla; y = x \<or> y \<notin> Fvars \<psi> \<and> y \<notin> \<Union> (Fvars ` F); nprv ((\<lambda>\<phi>. subst \<phi> (Var y) x) ` F) (subst \<psi> (Var y) x)\<rbrakk> \<Longrightarrow> finite F
 4. \<lbrakk>x \<in> var; y \<in> var; \<psi> \<in> fmla; finite F; F \<subseteq> fmla; y = x \<or> y \<notin> Fvars \<psi> \<and> y \<notin> \<Union> (Fvars ` F); nprv ((\<lambda>\<phi>. subst \<phi> (Var y) x) ` F) (subst \<psi> (Var y) x)\<rbrakk> \<Longrightarrow> finite ((\<lambda>\<phi>. subst \<phi> (Var x) y) ` (\<lambda>\<phi>. subst \<phi> (Var y) x) ` F)
 5. \<lbrakk>x \<in> var; y \<in> var; \<psi> \<in> fmla; finite F; F \<subseteq> fmla; y = x \<or> y \<notin> Fvars \<psi> \<and> y \<notin> \<Union> (Fvars ` F); nprv ((\<lambda>\<phi>. subst \<phi> (Var y) x) ` F) (subst \<psi> (Var y) x)\<rbrakk> \<Longrightarrow> \<forall>\<phi>2\<in>(\<lambda>\<phi>. subst \<phi> (Var x) y) ` (\<lambda>\<phi>. subst \<phi> (Var y) x) ` F. \<exists>\<phi>1\<in>F. prv (imp \<phi>1 \<phi>2)
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> var; y \<in> var; \<psi> \<in> fmla; finite F; F \<subseteq> fmla; y = x \<or> y \<notin> Fvars \<psi> \<and> y \<notin> \<Union> (Fvars ` F); nprv ((\<lambda>\<phi>. subst \<phi> (Var y) x) ` F) (subst \<psi> (Var y) x)\<rbrakk> \<Longrightarrow> F \<subseteq> fmla
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>x \<in> var; y \<in> var; \<psi> \<in> fmla; finite F; F \<subseteq> fmla; y = x \<or> y \<notin> Fvars \<psi> \<and> y \<notin> \<Union> (Fvars ` F); nprv ((\<lambda>\<phi>. subst \<phi> (Var y) x) ` F) (subst \<psi> (Var y) x)\<rbrakk> \<Longrightarrow> (\<lambda>\<phi>. subst \<phi> (Var x) y) ` (\<lambda>\<phi>. subst \<phi> (Var y) x) ` F \<subseteq> fmla
 2. \<lbrakk>x \<in> var; y \<in> var; \<psi> \<in> fmla; finite F; F \<subseteq> fmla; y = x \<or> y \<notin> Fvars \<psi> \<and> y \<notin> \<Union> (Fvars ` F); nprv ((\<lambda>\<phi>. subst \<phi> (Var y) x) ` F) (subst \<psi> (Var y) x)\<rbrakk> \<Longrightarrow> finite F
 3. \<lbrakk>x \<in> var; y \<in> var; \<psi> \<in> fmla; finite F; F \<subseteq> fmla; y = x \<or> y \<notin> Fvars \<psi> \<and> y \<notin> \<Union> (Fvars ` F); nprv ((\<lambda>\<phi>. subst \<phi> (Var y) x) ` F) (subst \<psi> (Var y) x)\<rbrakk> \<Longrightarrow> finite ((\<lambda>\<phi>. subst \<phi> (Var x) y) ` (\<lambda>\<phi>. subst \<phi> (Var y) x) ` F)
 4. \<lbrakk>x \<in> var; y \<in> var; \<psi> \<in> fmla; finite F; F \<subseteq> fmla; y = x \<or> y \<notin> Fvars \<psi> \<and> y \<notin> \<Union> (Fvars ` F); nprv ((\<lambda>\<phi>. subst \<phi> (Var y) x) ` F) (subst \<psi> (Var y) x)\<rbrakk> \<Longrightarrow> \<forall>\<phi>2\<in>(\<lambda>\<phi>. subst \<phi> (Var x) y) ` (\<lambda>\<phi>. subst \<phi> (Var y) x) ` F. \<exists>\<phi>1\<in>F. prv (imp \<phi>1 \<phi>2)
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> var; y \<in> var; \<psi> \<in> fmla; finite F; F \<subseteq> fmla; y = x \<or> y \<notin> Fvars \<psi> \<and> y \<notin> \<Union> (Fvars ` F); nprv ((\<lambda>\<phi>. subst \<phi> (Var y) x) ` F) (subst \<psi> (Var y) x)\<rbrakk> \<Longrightarrow> (\<lambda>\<phi>. subst \<phi> (Var x) y) ` (\<lambda>\<phi>. subst \<phi> (Var y) x) ` F \<subseteq> fmla
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>x \<in> var; y \<in> var; \<psi> \<in> fmla; finite F; F \<subseteq> fmla; y = x \<or> y \<notin> Fvars \<psi> \<and> y \<notin> \<Union> (Fvars ` F); nprv ((\<lambda>\<phi>. subst \<phi> (Var y) x) ` F) (subst \<psi> (Var y) x)\<rbrakk> \<Longrightarrow> finite F
 2. \<lbrakk>x \<in> var; y \<in> var; \<psi> \<in> fmla; finite F; F \<subseteq> fmla; y = x \<or> y \<notin> Fvars \<psi> \<and> y \<notin> \<Union> (Fvars ` F); nprv ((\<lambda>\<phi>. subst \<phi> (Var y) x) ` F) (subst \<psi> (Var y) x)\<rbrakk> \<Longrightarrow> finite ((\<lambda>\<phi>. subst \<phi> (Var x) y) ` (\<lambda>\<phi>. subst \<phi> (Var y) x) ` F)
 3. \<lbrakk>x \<in> var; y \<in> var; \<psi> \<in> fmla; finite F; F \<subseteq> fmla; y = x \<or> y \<notin> Fvars \<psi> \<and> y \<notin> \<Union> (Fvars ` F); nprv ((\<lambda>\<phi>. subst \<phi> (Var y) x) ` F) (subst \<psi> (Var y) x)\<rbrakk> \<Longrightarrow> \<forall>\<phi>2\<in>(\<lambda>\<phi>. subst \<phi> (Var x) y) ` (\<lambda>\<phi>. subst \<phi> (Var y) x) ` F. \<exists>\<phi>1\<in>F. prv (imp \<phi>1 \<phi>2)
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> var; y \<in> var; \<psi> \<in> fmla; finite F; F \<subseteq> fmla; y = x \<or> y \<notin> Fvars \<psi> \<and> y \<notin> \<Union> (Fvars ` F); nprv ((\<lambda>\<phi>. subst \<phi> (Var y) x) ` F) (subst \<psi> (Var y) x)\<rbrakk> \<Longrightarrow> finite F
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>x \<in> var; y \<in> var; \<psi> \<in> fmla; finite F; F \<subseteq> fmla; y = x \<or> y \<notin> Fvars \<psi> \<and> y \<notin> \<Union> (Fvars ` F); nprv ((\<lambda>\<phi>. subst \<phi> (Var y) x) ` F) (subst \<psi> (Var y) x)\<rbrakk> \<Longrightarrow> finite ((\<lambda>\<phi>. subst \<phi> (Var x) y) ` (\<lambda>\<phi>. subst \<phi> (Var y) x) ` F)
 2. \<lbrakk>x \<in> var; y \<in> var; \<psi> \<in> fmla; finite F; F \<subseteq> fmla; y = x \<or> y \<notin> Fvars \<psi> \<and> y \<notin> \<Union> (Fvars ` F); nprv ((\<lambda>\<phi>. subst \<phi> (Var y) x) ` F) (subst \<psi> (Var y) x)\<rbrakk> \<Longrightarrow> \<forall>\<phi>2\<in>(\<lambda>\<phi>. subst \<phi> (Var x) y) ` (\<lambda>\<phi>. subst \<phi> (Var y) x) ` F. \<exists>\<phi>1\<in>F. prv (imp \<phi>1 \<phi>2)
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> var; y \<in> var; \<psi> \<in> fmla; finite F; F \<subseteq> fmla; y = x \<or> y \<notin> Fvars \<psi> \<and> y \<notin> \<Union> (Fvars ` F); nprv ((\<lambda>\<phi>. subst \<phi> (Var y) x) ` F) (subst \<psi> (Var y) x)\<rbrakk> \<Longrightarrow> finite ((\<lambda>\<phi>. subst \<phi> (Var x) y) ` (\<lambda>\<phi>. subst \<phi> (Var y) x) ` F)
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> var; y \<in> var; \<psi> \<in> fmla; finite F; F \<subseteq> fmla; y = x \<or> y \<notin> Fvars \<psi> \<and> y \<notin> \<Union> (Fvars ` F); nprv ((\<lambda>\<phi>. subst \<phi> (Var y) x) ` F) (subst \<psi> (Var y) x)\<rbrakk> \<Longrightarrow> \<forall>\<phi>2\<in>(\<lambda>\<phi>. subst \<phi> (Var x) y) ` (\<lambda>\<phi>. subst \<phi> (Var y) x) ` F. \<exists>\<phi>1\<in>F. prv (imp \<phi>1 \<phi>2)
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> var; y \<in> var; \<psi> \<in> fmla; finite F; F \<subseteq> fmla; y = x \<or> y \<notin> Fvars \<psi> \<and> y \<notin> \<Union> (Fvars ` F); nprv ((\<lambda>\<phi>. subst \<phi> (Var y) x) ` F) (subst \<psi> (Var y) x)\<rbrakk> \<Longrightarrow> \<forall>\<phi>2\<in>(\<lambda>\<phi>. subst \<phi> (Var x) y) ` (\<lambda>\<phi>. subst \<phi> (Var y) x) ` F. \<exists>\<phi>1\<in>F. prv (imp \<phi>1 \<phi>2)
[PROOF STEP]
apply clarify
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>\<phi>2 \<phi> \<phi>'. \<lbrakk>x \<in> var; y \<in> var; \<psi> \<in> fmla; finite F; F \<subseteq> fmla; y = x \<or> y \<notin> Fvars \<psi> \<and> y \<notin> \<Union> (Fvars ` F); nprv ((\<lambda>\<phi>. subst \<phi> (Var y) x) ` F) (subst \<psi> (Var y) x); \<phi>' \<in> F\<rbrakk> \<Longrightarrow> \<exists>\<phi>1\<in>F. prv (imp \<phi>1 (subst (subst \<phi>' (Var y) x) (Var x) y))
[PROOF STEP]
subgoal for _ _ \<phi>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> var; y \<in> var; \<psi> \<in> fmla; finite F; F \<subseteq> fmla; y = x \<or> y \<notin> Fvars \<psi> \<and> y \<notin> \<Union> (Fvars ` F); nprv ((\<lambda>\<phi>. subst \<phi> (Var y) x) ` F) (subst \<psi> (Var y) x); \<phi> \<in> F\<rbrakk> \<Longrightarrow> \<exists>\<phi>1\<in>F. prv (imp \<phi>1 (subst (subst \<phi> (Var y) x) (Var x) y))
[PROOF STEP]
by (auto simp: subst_compose_eq_or intro!: bexI[of _ \<phi>] prv_imp_refl2)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
.
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
prv (imp (scnj F) (scnj ((\<lambda>\<phi>. subst \<phi> (Var x) y) ` (\<lambda>\<phi>. subst \<phi> (Var y) x) ` F)))

goal (1 subgoal):
 1. nprv F \<psi>
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
nprv ((\<lambda>\<phi>. subst \<phi> (Var x) y) ` (\<lambda>\<phi>. subst \<phi> (Var y) x) ` F) \<psi>
prv (imp (scnj F) (scnj ((\<lambda>\<phi>. subst \<phi> (Var x) y) ` (\<lambda>\<phi>. subst \<phi> (Var y) x) ` F)))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
nprv ((\<lambda>\<phi>. subst \<phi> (Var x) y) ` (\<lambda>\<phi>. subst \<phi> (Var y) x) ` F) \<psi>
prv (imp (scnj F) (scnj ((\<lambda>\<phi>. subst \<phi> (Var x) y) ` (\<lambda>\<phi>. subst \<phi> (Var y) x) ` F)))

goal (1 subgoal):
 1. nprv F \<psi>
[PROOF STEP]
unfolding nprv_def
[PROOF STATE]
proof (prove)
using this:
prv (imp (scnj ((\<lambda>\<phi>. subst \<phi> (Var x) y) ` (\<lambda>\<phi>. subst \<phi> (Var y) x) ` F)) \<psi>)
prv (imp (scnj F) (scnj ((\<lambda>\<phi>. subst \<phi> (Var x) y) ` (\<lambda>\<phi>. subst \<phi> (Var y) x) ` F)))

goal (1 subgoal):
 1. prv (imp (scnj F) \<psi>)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
prv (imp (scnj ((\<lambda>\<phi>. subst \<phi> (Var x) y) ` (\<lambda>\<phi>. subst \<phi> (Var y) x) ` F)) \<psi>)
prv (imp (scnj F) (scnj ((\<lambda>\<phi>. subst \<phi> (Var x) y) ` (\<lambda>\<phi>. subst \<phi> (Var y) x) ` F)))
x \<in> var
y \<in> var
\<psi> \<in> fmla
finite F
F \<subseteq> fmla
y = x \<or> y \<notin> Fvars \<psi> \<and> y \<notin> \<Union> (Fvars ` F)
nprv ((\<lambda>\<phi>. subst \<phi> (Var y) x) ` F) (subst \<psi> (Var y) x)

goal (1 subgoal):
 1. prv (imp (scnj F) \<psi>)
[PROOF STEP]
apply-
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>prv (imp (scnj ((\<lambda>\<phi>. subst \<phi> (Var x) y) ` (\<lambda>\<phi>. subst \<phi> (Var y) x) ` F)) \<psi>); prv (imp (scnj F) (scnj ((\<lambda>\<phi>. subst \<phi> (Var x) y) ` (\<lambda>\<phi>. subst \<phi> (Var y) x) ` F))); x \<in> var; y \<in> var; \<psi> \<in> fmla; finite F; F \<subseteq> fmla; y = x \<or> y \<notin> Fvars \<psi> \<and> y \<notin> \<Union> (Fvars ` F); nprv ((\<lambda>\<phi>. subst \<phi> (Var y) x) ` F) (subst \<psi> (Var y) x)\<rbrakk> \<Longrightarrow> prv (imp (scnj F) \<psi>)
[PROOF STEP]
by(rule prv_prv_imp_trans) auto
[PROOF STATE]
proof (state)
this:
nprv F \<psi>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma nprv_psubst:
assumes 0: "snd ` set txs \<subseteq> var" "fst ` set txs \<subseteq> trm" "\<psi> \<in> fmla" "finite F" "F \<subseteq> fmla"
"distinct (map snd txs)"
and 1: "nprv F \<psi>"
shows "nprv ((\<lambda>\<phi>. psubst \<phi> txs) ` F) (psubst \<psi> txs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nprv ((\<lambda>\<phi>. psubst \<phi> txs) ` F) (psubst \<psi> txs)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
snd ` set txs \<subseteq> var
fst ` set txs \<subseteq> trm
\<psi> \<in> fmla
finite F
F \<subseteq> fmla
distinct (map snd txs)
nprv F \<psi>

goal (1 subgoal):
 1. nprv ((\<lambda>\<phi>. psubst \<phi> txs) ` F) (psubst \<psi> txs)
[PROOF STEP]
unfolding nprv_def
[PROOF STATE]
proof (prove)
using this:
snd ` set txs \<subseteq> var
fst ` set txs \<subseteq> trm
\<psi> \<in> fmla
finite F
F \<subseteq> fmla
distinct (map snd txs)
prv (imp (scnj F) \<psi>)

goal (1 subgoal):
 1. prv (imp (scnj ((\<lambda>\<phi>. psubst \<phi> txs) ` F)) (psubst \<psi> txs))
[PROOF STEP]
apply(intro prv_prv_imp_trans[OF _ _ _ prv_psubst_scnj_imp])
[PROOF STATE]
proof (prove)
goal (9 subgoals):
 1. \<lbrakk>snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; \<psi> \<in> fmla; finite F; F \<subseteq> fmla; distinct (map snd txs); prv (imp (scnj F) \<psi>)\<rbrakk> \<Longrightarrow> scnj ((\<lambda>\<phi>. psubst \<phi> txs) ` F) \<in> fmla
 2. \<lbrakk>snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; \<psi> \<in> fmla; finite F; F \<subseteq> fmla; distinct (map snd txs); prv (imp (scnj F) \<psi>)\<rbrakk> \<Longrightarrow> psubst (scnj F) txs \<in> fmla
 3. \<lbrakk>snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; \<psi> \<in> fmla; finite F; F \<subseteq> fmla; distinct (map snd txs); prv (imp (scnj F) \<psi>)\<rbrakk> \<Longrightarrow> psubst \<psi> txs \<in> fmla
 4. \<lbrakk>snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; \<psi> \<in> fmla; finite F; F \<subseteq> fmla; distinct (map snd txs); prv (imp (scnj F) \<psi>)\<rbrakk> \<Longrightarrow> F \<subseteq> fmla
 5. \<lbrakk>snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; \<psi> \<in> fmla; finite F; F \<subseteq> fmla; distinct (map snd txs); prv (imp (scnj F) \<psi>)\<rbrakk> \<Longrightarrow> finite F
 6. \<lbrakk>snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; \<psi> \<in> fmla; finite F; F \<subseteq> fmla; distinct (map snd txs); prv (imp (scnj F) \<psi>)\<rbrakk> \<Longrightarrow> snd ` set txs \<subseteq> var
 7. \<lbrakk>snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; \<psi> \<in> fmla; finite F; F \<subseteq> fmla; distinct (map snd txs); prv (imp (scnj F) \<psi>)\<rbrakk> \<Longrightarrow> fst ` set txs \<subseteq> trm
 8. \<lbrakk>snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; \<psi> \<in> fmla; finite F; F \<subseteq> fmla; distinct (map snd txs); prv (imp (scnj F) \<psi>)\<rbrakk> \<Longrightarrow> distinct (map snd txs)
 9. \<lbrakk>snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; \<psi> \<in> fmla; finite F; F \<subseteq> fmla; distinct (map snd txs); prv (imp (scnj F) \<psi>)\<rbrakk> \<Longrightarrow> prv (imp (psubst (scnj F) txs) (psubst \<psi> txs))
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; \<psi> \<in> fmla; finite F; F \<subseteq> fmla; distinct (map snd txs); prv (imp (scnj F) \<psi>)\<rbrakk> \<Longrightarrow> scnj ((\<lambda>\<phi>. psubst \<phi> txs) ` F) \<in> fmla
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal (8 subgoals):
 1. \<lbrakk>snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; \<psi> \<in> fmla; finite F; F \<subseteq> fmla; distinct (map snd txs); prv (imp (scnj F) \<psi>)\<rbrakk> \<Longrightarrow> psubst (scnj F) txs \<in> fmla
 2. \<lbrakk>snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; \<psi> \<in> fmla; finite F; F \<subseteq> fmla; distinct (map snd txs); prv (imp (scnj F) \<psi>)\<rbrakk> \<Longrightarrow> psubst \<psi> txs \<in> fmla
 3. \<lbrakk>snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; \<psi> \<in> fmla; finite F; F \<subseteq> fmla; distinct (map snd txs); prv (imp (scnj F) \<psi>)\<rbrakk> \<Longrightarrow> F \<subseteq> fmla
 4. \<lbrakk>snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; \<psi> \<in> fmla; finite F; F \<subseteq> fmla; distinct (map snd txs); prv (imp (scnj F) \<psi>)\<rbrakk> \<Longrightarrow> finite F
 5. \<lbrakk>snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; \<psi> \<in> fmla; finite F; F \<subseteq> fmla; distinct (map snd txs); prv (imp (scnj F) \<psi>)\<rbrakk> \<Longrightarrow> snd ` set txs \<subseteq> var
 6. \<lbrakk>snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; \<psi> \<in> fmla; finite F; F \<subseteq> fmla; distinct (map snd txs); prv (imp (scnj F) \<psi>)\<rbrakk> \<Longrightarrow> fst ` set txs \<subseteq> trm
 7. \<lbrakk>snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; \<psi> \<in> fmla; finite F; F \<subseteq> fmla; distinct (map snd txs); prv (imp (scnj F) \<psi>)\<rbrakk> \<Longrightarrow> distinct (map snd txs)
 8. \<lbrakk>snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; \<psi> \<in> fmla; finite F; F \<subseteq> fmla; distinct (map snd txs); prv (imp (scnj F) \<psi>)\<rbrakk> \<Longrightarrow> prv (imp (psubst (scnj F) txs) (psubst \<psi> txs))
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; \<psi> \<in> fmla; finite F; F \<subseteq> fmla; distinct (map snd txs); prv (imp (scnj F) \<psi>)\<rbrakk> \<Longrightarrow> psubst (scnj F) txs \<in> fmla
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal (7 subgoals):
 1. \<lbrakk>snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; \<psi> \<in> fmla; finite F; F \<subseteq> fmla; distinct (map snd txs); prv (imp (scnj F) \<psi>)\<rbrakk> \<Longrightarrow> psubst \<psi> txs \<in> fmla
 2. \<lbrakk>snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; \<psi> \<in> fmla; finite F; F \<subseteq> fmla; distinct (map snd txs); prv (imp (scnj F) \<psi>)\<rbrakk> \<Longrightarrow> F \<subseteq> fmla
 3. \<lbrakk>snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; \<psi> \<in> fmla; finite F; F \<subseteq> fmla; distinct (map snd txs); prv (imp (scnj F) \<psi>)\<rbrakk> \<Longrightarrow> finite F
 4. \<lbrakk>snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; \<psi> \<in> fmla; finite F; F \<subseteq> fmla; distinct (map snd txs); prv (imp (scnj F) \<psi>)\<rbrakk> \<Longrightarrow> snd ` set txs \<subseteq> var
 5. \<lbrakk>snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; \<psi> \<in> fmla; finite F; F \<subseteq> fmla; distinct (map snd txs); prv (imp (scnj F) \<psi>)\<rbrakk> \<Longrightarrow> fst ` set txs \<subseteq> trm
 6. \<lbrakk>snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; \<psi> \<in> fmla; finite F; F \<subseteq> fmla; distinct (map snd txs); prv (imp (scnj F) \<psi>)\<rbrakk> \<Longrightarrow> distinct (map snd txs)
 7. \<lbrakk>snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; \<psi> \<in> fmla; finite F; F \<subseteq> fmla; distinct (map snd txs); prv (imp (scnj F) \<psi>)\<rbrakk> \<Longrightarrow> prv (imp (psubst (scnj F) txs) (psubst \<psi> txs))
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; \<psi> \<in> fmla; finite F; F \<subseteq> fmla; distinct (map snd txs); prv (imp (scnj F) \<psi>)\<rbrakk> \<Longrightarrow> psubst \<psi> txs \<in> fmla
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<lbrakk>snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; \<psi> \<in> fmla; finite F; F \<subseteq> fmla; distinct (map snd txs); prv (imp (scnj F) \<psi>)\<rbrakk> \<Longrightarrow> F \<subseteq> fmla
 2. \<lbrakk>snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; \<psi> \<in> fmla; finite F; F \<subseteq> fmla; distinct (map snd txs); prv (imp (scnj F) \<psi>)\<rbrakk> \<Longrightarrow> finite F
 3. \<lbrakk>snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; \<psi> \<in> fmla; finite F; F \<subseteq> fmla; distinct (map snd txs); prv (imp (scnj F) \<psi>)\<rbrakk> \<Longrightarrow> snd ` set txs \<subseteq> var
 4. \<lbrakk>snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; \<psi> \<in> fmla; finite F; F \<subseteq> fmla; distinct (map snd txs); prv (imp (scnj F) \<psi>)\<rbrakk> \<Longrightarrow> fst ` set txs \<subseteq> trm
 5. \<lbrakk>snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; \<psi> \<in> fmla; finite F; F \<subseteq> fmla; distinct (map snd txs); prv (imp (scnj F) \<psi>)\<rbrakk> \<Longrightarrow> distinct (map snd txs)
 6. \<lbrakk>snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; \<psi> \<in> fmla; finite F; F \<subseteq> fmla; distinct (map snd txs); prv (imp (scnj F) \<psi>)\<rbrakk> \<Longrightarrow> prv (imp (psubst (scnj F) txs) (psubst \<psi> txs))
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; \<psi> \<in> fmla; finite F; F \<subseteq> fmla; distinct (map snd txs); prv (imp (scnj F) \<psi>)\<rbrakk> \<Longrightarrow> F \<subseteq> fmla
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<lbrakk>snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; \<psi> \<in> fmla; finite F; F \<subseteq> fmla; distinct (map snd txs); prv (imp (scnj F) \<psi>)\<rbrakk> \<Longrightarrow> finite F
 2. \<lbrakk>snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; \<psi> \<in> fmla; finite F; F \<subseteq> fmla; distinct (map snd txs); prv (imp (scnj F) \<psi>)\<rbrakk> \<Longrightarrow> snd ` set txs \<subseteq> var
 3. \<lbrakk>snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; \<psi> \<in> fmla; finite F; F \<subseteq> fmla; distinct (map snd txs); prv (imp (scnj F) \<psi>)\<rbrakk> \<Longrightarrow> fst ` set txs \<subseteq> trm
 4. \<lbrakk>snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; \<psi> \<in> fmla; finite F; F \<subseteq> fmla; distinct (map snd txs); prv (imp (scnj F) \<psi>)\<rbrakk> \<Longrightarrow> distinct (map snd txs)
 5. \<lbrakk>snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; \<psi> \<in> fmla; finite F; F \<subseteq> fmla; distinct (map snd txs); prv (imp (scnj F) \<psi>)\<rbrakk> \<Longrightarrow> prv (imp (psubst (scnj F) txs) (psubst \<psi> txs))
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; \<psi> \<in> fmla; finite F; F \<subseteq> fmla; distinct (map snd txs); prv (imp (scnj F) \<psi>)\<rbrakk> \<Longrightarrow> finite F
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; \<psi> \<in> fmla; finite F; F \<subseteq> fmla; distinct (map snd txs); prv (imp (scnj F) \<psi>)\<rbrakk> \<Longrightarrow> snd ` set txs \<subseteq> var
 2. \<lbrakk>snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; \<psi> \<in> fmla; finite F; F \<subseteq> fmla; distinct (map snd txs); prv (imp (scnj F) \<psi>)\<rbrakk> \<Longrightarrow> fst ` set txs \<subseteq> trm
 3. \<lbrakk>snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; \<psi> \<in> fmla; finite F; F \<subseteq> fmla; distinct (map snd txs); prv (imp (scnj F) \<psi>)\<rbrakk> \<Longrightarrow> distinct (map snd txs)
 4. \<lbrakk>snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; \<psi> \<in> fmla; finite F; F \<subseteq> fmla; distinct (map snd txs); prv (imp (scnj F) \<psi>)\<rbrakk> \<Longrightarrow> prv (imp (psubst (scnj F) txs) (psubst \<psi> txs))
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; \<psi> \<in> fmla; finite F; F \<subseteq> fmla; distinct (map snd txs); prv (imp (scnj F) \<psi>)\<rbrakk> \<Longrightarrow> snd ` set txs \<subseteq> var
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; \<psi> \<in> fmla; finite F; F \<subseteq> fmla; distinct (map snd txs); prv (imp (scnj F) \<psi>)\<rbrakk> \<Longrightarrow> fst ` set txs \<subseteq> trm
 2. \<lbrakk>snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; \<psi> \<in> fmla; finite F; F \<subseteq> fmla; distinct (map snd txs); prv (imp (scnj F) \<psi>)\<rbrakk> \<Longrightarrow> distinct (map snd txs)
 3. \<lbrakk>snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; \<psi> \<in> fmla; finite F; F \<subseteq> fmla; distinct (map snd txs); prv (imp (scnj F) \<psi>)\<rbrakk> \<Longrightarrow> prv (imp (psubst (scnj F) txs) (psubst \<psi> txs))
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; \<psi> \<in> fmla; finite F; F \<subseteq> fmla; distinct (map snd txs); prv (imp (scnj F) \<psi>)\<rbrakk> \<Longrightarrow> fst ` set txs \<subseteq> trm
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; \<psi> \<in> fmla; finite F; F \<subseteq> fmla; distinct (map snd txs); prv (imp (scnj F) \<psi>)\<rbrakk> \<Longrightarrow> distinct (map snd txs)
 2. \<lbrakk>snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; \<psi> \<in> fmla; finite F; F \<subseteq> fmla; distinct (map snd txs); prv (imp (scnj F) \<psi>)\<rbrakk> \<Longrightarrow> prv (imp (psubst (scnj F) txs) (psubst \<psi> txs))
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; \<psi> \<in> fmla; finite F; F \<subseteq> fmla; distinct (map snd txs); prv (imp (scnj F) \<psi>)\<rbrakk> \<Longrightarrow> distinct (map snd txs)
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; \<psi> \<in> fmla; finite F; F \<subseteq> fmla; distinct (map snd txs); prv (imp (scnj F) \<psi>)\<rbrakk> \<Longrightarrow> prv (imp (psubst (scnj F) txs) (psubst \<psi> txs))
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; \<psi> \<in> fmla; finite F; F \<subseteq> fmla; distinct (map snd txs); prv (imp (scnj F) \<psi>)\<rbrakk> \<Longrightarrow> prv (imp (psubst (scnj F) txs) (psubst \<psi> txs))
[PROOF STEP]
using prv_psubst[OF _ _ _ 1[unfolded nprv_def]]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>imp (scnj F) \<psi> \<in> fmla; snd ` set ?txs \<subseteq> var; fst ` set ?txs \<subseteq> trm\<rbrakk> \<Longrightarrow> prv (psubst (imp (scnj F) \<psi>) ?txs)

goal (1 subgoal):
 1. \<lbrakk>snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; \<psi> \<in> fmla; finite F; F \<subseteq> fmla; distinct (map snd txs); prv (imp (scnj F) \<psi>)\<rbrakk> \<Longrightarrow> prv (imp (psubst (scnj F) txs) (psubst \<psi> txs))
[PROOF STEP]
by (metis imp psubst_imp scnj)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
.


[STATEMENT]
lemma nprv_impI:
"nprv (insert \<phi> F) \<psi> \<Longrightarrow>
 F \<subseteq> fmla \<Longrightarrow> finite F \<Longrightarrow> \<phi> \<in> fmla \<Longrightarrow> \<psi> \<in> fmla \<Longrightarrow>
 nprv F (imp \<phi> \<psi>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>nprv (insert \<phi> F) \<psi>; F \<subseteq> fmla; finite F; \<phi> \<in> fmla; \<psi> \<in> fmla\<rbrakk> \<Longrightarrow> nprv F (imp \<phi> \<psi>)
[PROOF STEP]
unfolding nprv_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>prv (imp (scnj (insert \<phi> F)) \<psi>); F \<subseteq> fmla; finite F; \<phi> \<in> fmla; \<psi> \<in> fmla\<rbrakk> \<Longrightarrow> prv (imp (scnj F) (imp \<phi> \<psi>))
[PROOF STEP]
by (metis cnj finite.insertI insert_subset prv_cnj_imp prv_imp_cnj_scnj prv_imp_com prv_prv_imp_trans scnj)


[STATEMENT]
lemma nprv_impI_rev:
assumes "nprv F (imp \<phi> \<psi>)"
and "F \<subseteq> fmla" and "finite F" and "\<phi> \<in> fmla" and "\<psi> \<in> fmla"
shows "nprv (insert \<phi> F) \<psi>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nprv (insert \<phi> F) \<psi>
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
nprv F (imp \<phi> \<psi>)
F \<subseteq> fmla
finite F
\<phi> \<in> fmla
\<psi> \<in> fmla

goal (1 subgoal):
 1. nprv (insert \<phi> F) \<psi>
[PROOF STEP]
unfolding nprv_def
[PROOF STATE]
proof (prove)
using this:
prv (imp (scnj F) (imp \<phi> \<psi>))
F \<subseteq> fmla
finite F
\<phi> \<in> fmla
\<psi> \<in> fmla

goal (1 subgoal):
 1. prv (imp (scnj (insert \<phi> F)) \<psi>)
[PROOF STEP]
by (metis cnj finite.insertI insert_subset prv_cnj_imp_monoR2 prv_eqv_imp_transi
    prv_eqv_scnj_insert prv_imp_com scnj)


[STATEMENT]
lemma nprv_impI_rev2:
assumes "nprv F (imp \<phi> \<psi>)" and G: "insert \<phi> F \<subseteq> G"
and "G \<subseteq> fmla" and "finite G" and "\<phi> \<in> fmla" and "\<psi> \<in> fmla"
shows "nprv G \<psi>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nprv G \<psi>
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
nprv F (imp \<phi> \<psi>)
insert \<phi> F \<subseteq> G
G \<subseteq> fmla
finite G
\<phi> \<in> fmla
\<psi> \<in> fmla

goal (1 subgoal):
 1. nprv G \<psi>
[PROOF STEP]
apply-
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>nprv F (imp \<phi> \<psi>); insert \<phi> F \<subseteq> G; G \<subseteq> fmla; finite G; \<phi> \<in> fmla; \<psi> \<in> fmla\<rbrakk> \<Longrightarrow> nprv G \<psi>
[PROOF STEP]
apply(rule nprv_mono[of "insert \<phi> F"])
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<lbrakk>nprv F (imp \<phi> \<psi>); insert \<phi> F \<subseteq> G; G \<subseteq> fmla; finite G; \<phi> \<in> fmla; \<psi> \<in> fmla\<rbrakk> \<Longrightarrow> nprv (insert \<phi> F) \<psi>
 2. \<lbrakk>nprv F (imp \<phi> \<psi>); insert \<phi> F \<subseteq> G; G \<subseteq> fmla; finite G; \<phi> \<in> fmla; \<psi> \<in> fmla\<rbrakk> \<Longrightarrow> G \<subseteq> fmla
 3. \<lbrakk>nprv F (imp \<phi> \<psi>); insert \<phi> F \<subseteq> G; G \<subseteq> fmla; finite G; \<phi> \<in> fmla; \<psi> \<in> fmla\<rbrakk> \<Longrightarrow> finite G
 4. \<lbrakk>nprv F (imp \<phi> \<psi>); insert \<phi> F \<subseteq> G; G \<subseteq> fmla; finite G; \<phi> \<in> fmla; \<psi> \<in> fmla\<rbrakk> \<Longrightarrow> insert \<phi> F \<subseteq> G
 5. \<lbrakk>nprv F (imp \<phi> \<psi>); insert \<phi> F \<subseteq> G; G \<subseteq> fmla; finite G; \<phi> \<in> fmla; \<psi> \<in> fmla\<rbrakk> \<Longrightarrow> \<psi> \<in> fmla
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>nprv F (imp \<phi> \<psi>); insert \<phi> F \<subseteq> G; G \<subseteq> fmla; finite G; \<phi> \<in> fmla; \<psi> \<in> fmla\<rbrakk> \<Longrightarrow> nprv (insert \<phi> F) \<psi>
[PROOF STEP]
by (meson nprv_impI_rev order_trans rev_finite_subset subset_insertI)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>nprv F (imp \<phi> \<psi>); insert \<phi> F \<subseteq> G; G \<subseteq> fmla; finite G; \<phi> \<in> fmla; \<psi> \<in> fmla\<rbrakk> \<Longrightarrow> G \<subseteq> fmla
 2. \<lbrakk>nprv F (imp \<phi> \<psi>); insert \<phi> F \<subseteq> G; G \<subseteq> fmla; finite G; \<phi> \<in> fmla; \<psi> \<in> fmla\<rbrakk> \<Longrightarrow> finite G
 3. \<lbrakk>nprv F (imp \<phi> \<psi>); insert \<phi> F \<subseteq> G; G \<subseteq> fmla; finite G; \<phi> \<in> fmla; \<psi> \<in> fmla\<rbrakk> \<Longrightarrow> insert \<phi> F \<subseteq> G
 4. \<lbrakk>nprv F (imp \<phi> \<psi>); insert \<phi> F \<subseteq> G; G \<subseteq> fmla; finite G; \<phi> \<in> fmla; \<psi> \<in> fmla\<rbrakk> \<Longrightarrow> \<psi> \<in> fmla
[PROOF STEP]
by auto


[STATEMENT]
lemma nprv_mp:
"nprv F (imp \<phi> \<psi>) \<Longrightarrow> nprv F \<phi> \<Longrightarrow>
 F \<subseteq> fmla \<Longrightarrow> finite F \<Longrightarrow> \<phi> \<in> fmla \<Longrightarrow> \<psi> \<in> fmla \<Longrightarrow>
 nprv F \<psi>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>nprv F (imp \<phi> \<psi>); nprv F \<phi>; F \<subseteq> fmla; finite F; \<phi> \<in> fmla; \<psi> \<in> fmla\<rbrakk> \<Longrightarrow> nprv F \<psi>
[PROOF STEP]
unfolding nprv_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>prv (imp (scnj F) (imp \<phi> \<psi>)); prv (imp (scnj F) \<phi>); F \<subseteq> fmla; finite F; \<phi> \<in> fmla; \<psi> \<in> fmla\<rbrakk> \<Longrightarrow> prv (imp (scnj F) \<psi>)
[PROOF STEP]
by (metis (full_types) cnj prv_cnj_imp_monoR2 prv_imp_cnj prv_imp_refl prv_prv_imp_trans scnj)


[STATEMENT]
lemma nprv_impE:
"nprv F (imp \<phi> \<psi>) \<Longrightarrow> nprv F \<phi> \<Longrightarrow>  nprv (insert \<psi> F) \<chi> \<Longrightarrow>
 F \<subseteq> fmla \<Longrightarrow> finite F \<Longrightarrow> \<phi> \<in> fmla \<Longrightarrow> \<psi> \<in> fmla \<Longrightarrow> \<chi> \<in> fmla \<Longrightarrow>
 nprv F \<chi>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>nprv F (imp \<phi> \<psi>); nprv F \<phi>; nprv (insert \<psi> F) \<chi>; F \<subseteq> fmla; finite F; \<phi> \<in> fmla; \<psi> \<in> fmla; \<chi> \<in> fmla\<rbrakk> \<Longrightarrow> nprv F \<chi>
[PROOF STEP]
using nprv_cut nprv_mp
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>nprv ?F ?\<phi>; nprv (insert ?\<phi> ?F) ?\<psi>; ?F \<subseteq> fmla; finite ?F; ?\<phi> \<in> fmla; ?\<psi> \<in> fmla\<rbrakk> \<Longrightarrow> nprv ?F ?\<psi>
\<lbrakk>nprv ?F (imp ?\<phi> ?\<psi>); nprv ?F ?\<phi>; ?F \<subseteq> fmla; finite ?F; ?\<phi> \<in> fmla; ?\<psi> \<in> fmla\<rbrakk> \<Longrightarrow> nprv ?F ?\<psi>

goal (1 subgoal):
 1. \<lbrakk>nprv F (imp \<phi> \<psi>); nprv F \<phi>; nprv (insert \<psi> F) \<chi>; F \<subseteq> fmla; finite F; \<phi> \<in> fmla; \<psi> \<in> fmla; \<chi> \<in> fmla\<rbrakk> \<Longrightarrow> nprv F \<chi>
[PROOF STEP]
by blast


[STATEMENT]
lemma nprv_cnjI:
"nprv F \<phi> \<Longrightarrow> nprv F \<psi> \<Longrightarrow>
 F \<subseteq> fmla \<Longrightarrow> finite F \<Longrightarrow> \<phi> \<in> fmla \<Longrightarrow> \<psi> \<in> fmla \<Longrightarrow>
 nprv F (cnj \<phi> \<psi>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>nprv F \<phi>; nprv F \<psi>; F \<subseteq> fmla; finite F; \<phi> \<in> fmla; \<psi> \<in> fmla\<rbrakk> \<Longrightarrow> nprv F (cnj \<phi> \<psi>)
[PROOF STEP]
unfolding nprv_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>prv (imp (scnj F) \<phi>); prv (imp (scnj F) \<psi>); F \<subseteq> fmla; finite F; \<phi> \<in> fmla; \<psi> \<in> fmla\<rbrakk> \<Longrightarrow> prv (imp (scnj F) (cnj \<phi> \<psi>))
[PROOF STEP]
by (simp add: prv_imp_cnj)


[STATEMENT]
lemma nprv_cnjE:
"nprv F (cnj \<phi>1 \<phi>2) \<Longrightarrow> nprv (insert \<phi>1 (insert \<phi>2 F)) \<psi> \<Longrightarrow>
 F \<subseteq> fmla \<Longrightarrow> finite F \<Longrightarrow> \<phi>1 \<in> fmla \<Longrightarrow> \<phi>2 \<in> fmla \<Longrightarrow> \<psi> \<in> fmla \<Longrightarrow>
 nprv F \<psi>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>nprv F (cnj \<phi>1 \<phi>2); nprv (insert \<phi>1 (insert \<phi>2 F)) \<psi>; F \<subseteq> fmla; finite F; \<phi>1 \<in> fmla; \<phi>2 \<in> fmla; \<psi> \<in> fmla\<rbrakk> \<Longrightarrow> nprv F \<psi>
[PROOF STEP]
unfolding nprv_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>prv (imp (scnj F) (cnj \<phi>1 \<phi>2)); prv (imp (scnj (insert \<phi>1 (insert \<phi>2 F))) \<psi>); F \<subseteq> fmla; finite F; \<phi>1 \<in> fmla; \<phi>2 \<in> fmla; \<psi> \<in> fmla\<rbrakk> \<Longrightarrow> prv (imp (scnj F) \<psi>)
[PROOF STEP]
by (metis cnj nprv_cut2 nprv_def prv_imp_cnjL prv_imp_cnjR prv_prv_imp_trans scnj)


[STATEMENT]
lemma nprv_dsjIL:
"nprv F \<phi> \<Longrightarrow>
 F \<subseteq> fmla \<Longrightarrow> finite F \<Longrightarrow> \<phi> \<in> fmla \<Longrightarrow> \<psi> \<in> fmla \<Longrightarrow>
 nprv F (dsj \<phi> \<psi>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>nprv F \<phi>; F \<subseteq> fmla; finite F; \<phi> \<in> fmla; \<psi> \<in> fmla\<rbrakk> \<Longrightarrow> nprv F (dsj \<phi> \<psi>)
[PROOF STEP]
unfolding nprv_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>prv (imp (scnj F) \<phi>); F \<subseteq> fmla; finite F; \<phi> \<in> fmla; \<psi> \<in> fmla\<rbrakk> \<Longrightarrow> prv (imp (scnj F) (dsj \<phi> \<psi>))
[PROOF STEP]
by (meson dsj prv_dsj_impL prv_prv_imp_trans scnj)


[STATEMENT]
lemma nprv_dsjIR:
"nprv F \<psi> \<Longrightarrow>
 F \<subseteq> fmla \<Longrightarrow> finite F \<Longrightarrow> \<phi> \<in> fmla \<Longrightarrow> \<psi> \<in> fmla \<Longrightarrow>
 nprv F (dsj \<phi> \<psi>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>nprv F \<psi>; F \<subseteq> fmla; finite F; \<phi> \<in> fmla; \<psi> \<in> fmla\<rbrakk> \<Longrightarrow> nprv F (dsj \<phi> \<psi>)
[PROOF STEP]
unfolding nprv_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>prv (imp (scnj F) \<psi>); F \<subseteq> fmla; finite F; \<phi> \<in> fmla; \<psi> \<in> fmla\<rbrakk> \<Longrightarrow> prv (imp (scnj F) (dsj \<phi> \<psi>))
[PROOF STEP]
by (meson dsj prv_dsj_impR prv_prv_imp_trans scnj)


[STATEMENT]
lemma nprv_dsjE:
assumes "nprv F (dsj \<phi> \<psi>)"
and "nprv (insert \<phi> F) \<chi>" "nprv (insert \<psi> F) \<chi>"
and "F \<subseteq> fmla" "finite F" "\<phi> \<in> fmla" "\<psi> \<in> fmla" "\<chi> \<in> fmla"
shows "nprv F \<chi>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nprv F \<chi>
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. nprv F \<chi>
[PROOF STEP]
have "nprv F (imp (dsj \<phi> \<psi>) \<chi>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nprv F (imp (dsj \<phi> \<psi>) \<chi>)
[PROOF STEP]
by (meson assms dsj imp nprv_def nprv_impI prv_imp_com prv_imp_dsjEE scnj)
[PROOF STATE]
proof (state)
this:
nprv F (imp (dsj \<phi> \<psi>) \<chi>)

goal (1 subgoal):
 1. nprv F \<chi>
[PROOF STEP]
hence "nprv (insert (dsj \<phi> \<psi>) F) \<chi>"
[PROOF STATE]
proof (prove)
using this:
nprv F (imp (dsj \<phi> \<psi>) \<chi>)

goal (1 subgoal):
 1. nprv (insert (dsj \<phi> \<psi>) F) \<chi>
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
nprv F (imp (dsj \<phi> \<psi>) \<chi>)
nprv F (dsj \<phi> \<psi>)
nprv (insert \<phi> F) \<chi>
nprv (insert \<psi> F) \<chi>
F \<subseteq> fmla
finite F
\<phi> \<in> fmla
\<psi> \<in> fmla
\<chi> \<in> fmla

goal (1 subgoal):
 1. nprv (insert (dsj \<phi> \<psi>) F) \<chi>
[PROOF STEP]
by (simp add: nprv_impI_rev)
[PROOF STATE]
proof (state)
this:
nprv (insert (dsj \<phi> \<psi>) F) \<chi>

goal (1 subgoal):
 1. nprv F \<chi>
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
nprv (insert (dsj \<phi> \<psi>) F) \<chi>

goal (1 subgoal):
 1. nprv F \<chi>
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
nprv (insert (dsj \<phi> \<psi>) F) \<chi>
nprv F (dsj \<phi> \<psi>)
nprv (insert \<phi> F) \<chi>
nprv (insert \<psi> F) \<chi>
F \<subseteq> fmla
finite F
\<phi> \<in> fmla
\<psi> \<in> fmla
\<chi> \<in> fmla

goal (1 subgoal):
 1. nprv F \<chi>
[PROOF STEP]
by (meson dsj nprv_cut)
[PROOF STATE]
proof (state)
this:
nprv F \<chi>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma nprv_flsE: "nprv F fls \<Longrightarrow> F \<subseteq> fmla \<Longrightarrow> finite F \<Longrightarrow> \<phi> \<in> fmla \<Longrightarrow>  nprv F \<phi>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>nprv F fls; F \<subseteq> fmla; finite F; \<phi> \<in> fmla\<rbrakk> \<Longrightarrow> nprv F \<phi>
[PROOF STEP]
unfolding nprv_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>prv (imp (scnj F) fls); F \<subseteq> fmla; finite F; \<phi> \<in> fmla\<rbrakk> \<Longrightarrow> prv (imp (scnj F) \<phi>)
[PROOF STEP]
using prv_prv_imp_trans scnj
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?\<phi> \<in> fmla; ?\<chi> \<in> fmla; ?\<psi> \<in> fmla; prv (imp ?\<phi> ?\<chi>); prv (imp ?\<chi> ?\<psi>)\<rbrakk> \<Longrightarrow> prv (imp ?\<phi> ?\<psi>)
\<lbrakk>?F \<subseteq> fmla; finite ?F\<rbrakk> \<Longrightarrow> scnj ?F \<in> fmla

goal (1 subgoal):
 1. \<lbrakk>prv (imp (scnj F) fls); F \<subseteq> fmla; finite F; \<phi> \<in> fmla\<rbrakk> \<Longrightarrow> prv (imp (scnj F) \<phi>)
[PROOF STEP]
by blast


[STATEMENT]
lemma nprv_truI: "F \<subseteq> fmla \<Longrightarrow> finite F \<Longrightarrow> nprv F tru"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>F \<subseteq> fmla; finite F\<rbrakk> \<Longrightarrow> nprv F tru
[PROOF STEP]
unfolding nprv_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>F \<subseteq> fmla; finite F\<rbrakk> \<Longrightarrow> prv (imp (scnj F) tru)
[PROOF STEP]
by (simp add: prv_imp_tru)


[STATEMENT]
lemma nprv_negI:
"nprv (insert \<phi> F) fls \<Longrightarrow>
 F \<subseteq> fmla \<Longrightarrow> finite F \<Longrightarrow> \<phi> \<in> fmla \<Longrightarrow>
 nprv F (neg \<phi>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>nprv (insert \<phi> F) fls; F \<subseteq> fmla; finite F; \<phi> \<in> fmla\<rbrakk> \<Longrightarrow> nprv F (neg \<phi>)
[PROOF STEP]
unfolding neg_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>nprv (insert \<phi> F) fls; F \<subseteq> fmla; finite F; \<phi> \<in> fmla\<rbrakk> \<Longrightarrow> nprv F (imp \<phi> fls)
[PROOF STEP]
by (auto intro: nprv_impI)


[STATEMENT]
lemma nprv_neg_fls:
"nprv F (neg \<phi>) \<Longrightarrow> nprv F \<phi> \<Longrightarrow>
 F \<subseteq> fmla \<Longrightarrow> finite F \<Longrightarrow> \<phi> \<in> fmla \<Longrightarrow> \<psi> \<in> fmla \<Longrightarrow>
 nprv F fls"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>nprv F (neg \<phi>); nprv F \<phi>; F \<subseteq> fmla; finite F; \<phi> \<in> fmla; \<psi> \<in> fmla\<rbrakk> \<Longrightarrow> nprv F fls
[PROOF STEP]
unfolding neg_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>nprv F (imp \<phi> fls); nprv F \<phi>; F \<subseteq> fmla; finite F; \<phi> \<in> fmla; \<psi> \<in> fmla\<rbrakk> \<Longrightarrow> nprv F fls
[PROOF STEP]
using nprv_mp
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>nprv ?F (imp ?\<phi> ?\<psi>); nprv ?F ?\<phi>; ?F \<subseteq> fmla; finite ?F; ?\<phi> \<in> fmla; ?\<psi> \<in> fmla\<rbrakk> \<Longrightarrow> nprv ?F ?\<psi>

goal (1 subgoal):
 1. \<lbrakk>nprv F (imp \<phi> fls); nprv F \<phi>; F \<subseteq> fmla; finite F; \<phi> \<in> fmla; \<psi> \<in> fmla\<rbrakk> \<Longrightarrow> nprv F fls
[PROOF STEP]
by blast


[STATEMENT]
lemma nprv_negE:
"nprv F (neg \<phi>) \<Longrightarrow> nprv F \<phi> \<Longrightarrow>
 F \<subseteq> fmla \<Longrightarrow> finite F \<Longrightarrow> \<phi> \<in> fmla \<Longrightarrow> \<psi> \<in> fmla \<Longrightarrow>
 nprv F \<psi>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>nprv F (neg \<phi>); nprv F \<phi>; F \<subseteq> fmla; finite F; \<phi> \<in> fmla; \<psi> \<in> fmla\<rbrakk> \<Longrightarrow> nprv F \<psi>
[PROOF STEP]
using nprv_flsE nprv_neg_fls
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>nprv ?F fls; ?F \<subseteq> fmla; finite ?F; ?\<phi> \<in> fmla\<rbrakk> \<Longrightarrow> nprv ?F ?\<phi>
\<lbrakk>nprv ?F (neg ?\<phi>); nprv ?F ?\<phi>; ?F \<subseteq> fmla; finite ?F; ?\<phi> \<in> fmla; ?\<psi> \<in> fmla\<rbrakk> \<Longrightarrow> nprv ?F fls

goal (1 subgoal):
 1. \<lbrakk>nprv F (neg \<phi>); nprv F \<phi>; F \<subseteq> fmla; finite F; \<phi> \<in> fmla; \<psi> \<in> fmla\<rbrakk> \<Longrightarrow> nprv F \<psi>
[PROOF STEP]
by blast


[STATEMENT]
lemma nprv_scnjI:
"(\<And> \<psi>. \<psi> \<in> G \<Longrightarrow> nprv F \<psi>) \<Longrightarrow>
 F \<subseteq> fmla \<Longrightarrow> finite F \<Longrightarrow> G \<subseteq> fmla \<Longrightarrow> finite G \<Longrightarrow>
 nprv F (scnj G)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>\<psi>. \<psi> \<in> G \<Longrightarrow> nprv F \<psi>; F \<subseteq> fmla; finite F; G \<subseteq> fmla; finite G\<rbrakk> \<Longrightarrow> nprv F (scnj G)
[PROOF STEP]
unfolding nprv_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>\<psi>. \<psi> \<in> G \<Longrightarrow> prv (imp (scnj F) \<psi>); F \<subseteq> fmla; finite F; G \<subseteq> fmla; finite G\<rbrakk> \<Longrightarrow> prv (imp (scnj F) (scnj G))
[PROOF STEP]
by (simp add: prv_imp_scnj)


[STATEMENT]
lemma nprv_scnjE:
"nprv F (scnj G) \<Longrightarrow> nprv (G \<union> F) \<psi> \<Longrightarrow>
 F \<subseteq> fmla \<Longrightarrow> finite F \<Longrightarrow> G \<subseteq> fmla \<Longrightarrow> finite G \<Longrightarrow> \<psi> \<in> fmla \<Longrightarrow>
 nprv F \<psi>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>nprv F (scnj G); nprv (G \<union> F) \<psi>; F \<subseteq> fmla; finite F; G \<subseteq> fmla; finite G; \<psi> \<in> fmla\<rbrakk> \<Longrightarrow> nprv F \<psi>
[PROOF STEP]
apply(rule nprv_cut_set[of _ G])
[PROOF STATE]
proof (prove)
goal (7 subgoals):
 1. \<lbrakk>nprv F (scnj G); nprv (G \<union> F) \<psi>; F \<subseteq> fmla; finite F; G \<subseteq> fmla; finite G; \<psi> \<in> fmla\<rbrakk> \<Longrightarrow> finite F
 2. \<lbrakk>nprv F (scnj G); nprv (G \<union> F) \<psi>; F \<subseteq> fmla; finite F; G \<subseteq> fmla; finite G; \<psi> \<in> fmla\<rbrakk> \<Longrightarrow> F \<subseteq> fmla
 3. \<lbrakk>nprv F (scnj G); nprv (G \<union> F) \<psi>; F \<subseteq> fmla; finite F; G \<subseteq> fmla; finite G; \<psi> \<in> fmla\<rbrakk> \<Longrightarrow> finite G
 4. \<lbrakk>nprv F (scnj G); nprv (G \<union> F) \<psi>; F \<subseteq> fmla; finite F; G \<subseteq> fmla; finite G; \<psi> \<in> fmla\<rbrakk> \<Longrightarrow> G \<subseteq> fmla
 5. \<lbrakk>nprv F (scnj G); nprv (G \<union> F) \<psi>; F \<subseteq> fmla; finite F; G \<subseteq> fmla; finite G; \<psi> \<in> fmla\<rbrakk> \<Longrightarrow> \<psi> \<in> fmla
 6. \<And>\<psi>'. \<lbrakk>nprv F (scnj G); nprv (G \<union> F) \<psi>; F \<subseteq> fmla; finite F; G \<subseteq> fmla; finite G; \<psi> \<in> fmla; \<psi>' \<in> G\<rbrakk> \<Longrightarrow> nprv F \<psi>'
 7. \<lbrakk>nprv F (scnj G); nprv (G \<union> F) \<psi>; F \<subseteq> fmla; finite F; G \<subseteq> fmla; finite G; \<psi> \<in> fmla\<rbrakk> \<Longrightarrow> nprv (G \<union> F) \<psi>
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>nprv F (scnj G); nprv (G \<union> F) \<psi>; F \<subseteq> fmla; finite F; G \<subseteq> fmla; finite G; \<psi> \<in> fmla\<rbrakk> \<Longrightarrow> finite F
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<lbrakk>nprv F (scnj G); nprv (G \<union> F) \<psi>; F \<subseteq> fmla; finite F; G \<subseteq> fmla; finite G; \<psi> \<in> fmla\<rbrakk> \<Longrightarrow> F \<subseteq> fmla
 2. \<lbrakk>nprv F (scnj G); nprv (G \<union> F) \<psi>; F \<subseteq> fmla; finite F; G \<subseteq> fmla; finite G; \<psi> \<in> fmla\<rbrakk> \<Longrightarrow> finite G
 3. \<lbrakk>nprv F (scnj G); nprv (G \<union> F) \<psi>; F \<subseteq> fmla; finite F; G \<subseteq> fmla; finite G; \<psi> \<in> fmla\<rbrakk> \<Longrightarrow> G \<subseteq> fmla
 4. \<lbrakk>nprv F (scnj G); nprv (G \<union> F) \<psi>; F \<subseteq> fmla; finite F; G \<subseteq> fmla; finite G; \<psi> \<in> fmla\<rbrakk> \<Longrightarrow> \<psi> \<in> fmla
 5. \<And>\<psi>'. \<lbrakk>nprv F (scnj G); nprv (G \<union> F) \<psi>; F \<subseteq> fmla; finite F; G \<subseteq> fmla; finite G; \<psi> \<in> fmla; \<psi>' \<in> G\<rbrakk> \<Longrightarrow> nprv F \<psi>'
 6. \<lbrakk>nprv F (scnj G); nprv (G \<union> F) \<psi>; F \<subseteq> fmla; finite F; G \<subseteq> fmla; finite G; \<psi> \<in> fmla\<rbrakk> \<Longrightarrow> nprv (G \<union> F) \<psi>
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>nprv F (scnj G); nprv (G \<union> F) \<psi>; F \<subseteq> fmla; finite F; G \<subseteq> fmla; finite G; \<psi> \<in> fmla\<rbrakk> \<Longrightarrow> F \<subseteq> fmla
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<lbrakk>nprv F (scnj G); nprv (G \<union> F) \<psi>; F \<subseteq> fmla; finite F; G \<subseteq> fmla; finite G; \<psi> \<in> fmla\<rbrakk> \<Longrightarrow> finite G
 2. \<lbrakk>nprv F (scnj G); nprv (G \<union> F) \<psi>; F \<subseteq> fmla; finite F; G \<subseteq> fmla; finite G; \<psi> \<in> fmla\<rbrakk> \<Longrightarrow> G \<subseteq> fmla
 3. \<lbrakk>nprv F (scnj G); nprv (G \<union> F) \<psi>; F \<subseteq> fmla; finite F; G \<subseteq> fmla; finite G; \<psi> \<in> fmla\<rbrakk> \<Longrightarrow> \<psi> \<in> fmla
 4. \<And>\<psi>'. \<lbrakk>nprv F (scnj G); nprv (G \<union> F) \<psi>; F \<subseteq> fmla; finite F; G \<subseteq> fmla; finite G; \<psi> \<in> fmla; \<psi>' \<in> G\<rbrakk> \<Longrightarrow> nprv F \<psi>'
 5. \<lbrakk>nprv F (scnj G); nprv (G \<union> F) \<psi>; F \<subseteq> fmla; finite F; G \<subseteq> fmla; finite G; \<psi> \<in> fmla\<rbrakk> \<Longrightarrow> nprv (G \<union> F) \<psi>
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>nprv F (scnj G); nprv (G \<union> F) \<psi>; F \<subseteq> fmla; finite F; G \<subseteq> fmla; finite G; \<psi> \<in> fmla\<rbrakk> \<Longrightarrow> finite G
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>nprv F (scnj G); nprv (G \<union> F) \<psi>; F \<subseteq> fmla; finite F; G \<subseteq> fmla; finite G; \<psi> \<in> fmla\<rbrakk> \<Longrightarrow> G \<subseteq> fmla
 2. \<lbrakk>nprv F (scnj G); nprv (G \<union> F) \<psi>; F \<subseteq> fmla; finite F; G \<subseteq> fmla; finite G; \<psi> \<in> fmla\<rbrakk> \<Longrightarrow> \<psi> \<in> fmla
 3. \<And>\<psi>'. \<lbrakk>nprv F (scnj G); nprv (G \<union> F) \<psi>; F \<subseteq> fmla; finite F; G \<subseteq> fmla; finite G; \<psi> \<in> fmla; \<psi>' \<in> G\<rbrakk> \<Longrightarrow> nprv F \<psi>'
 4. \<lbrakk>nprv F (scnj G); nprv (G \<union> F) \<psi>; F \<subseteq> fmla; finite F; G \<subseteq> fmla; finite G; \<psi> \<in> fmla\<rbrakk> \<Longrightarrow> nprv (G \<union> F) \<psi>
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>nprv F (scnj G); nprv (G \<union> F) \<psi>; F \<subseteq> fmla; finite F; G \<subseteq> fmla; finite G; \<psi> \<in> fmla\<rbrakk> \<Longrightarrow> G \<subseteq> fmla
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>nprv F (scnj G); nprv (G \<union> F) \<psi>; F \<subseteq> fmla; finite F; G \<subseteq> fmla; finite G; \<psi> \<in> fmla\<rbrakk> \<Longrightarrow> \<psi> \<in> fmla
 2. \<And>\<psi>'. \<lbrakk>nprv F (scnj G); nprv (G \<union> F) \<psi>; F \<subseteq> fmla; finite F; G \<subseteq> fmla; finite G; \<psi> \<in> fmla; \<psi>' \<in> G\<rbrakk> \<Longrightarrow> nprv F \<psi>'
 3. \<lbrakk>nprv F (scnj G); nprv (G \<union> F) \<psi>; F \<subseteq> fmla; finite F; G \<subseteq> fmla; finite G; \<psi> \<in> fmla\<rbrakk> \<Longrightarrow> nprv (G \<union> F) \<psi>
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>nprv F (scnj G); nprv (G \<union> F) \<psi>; F \<subseteq> fmla; finite F; G \<subseteq> fmla; finite G; \<psi> \<in> fmla\<rbrakk> \<Longrightarrow> \<psi> \<in> fmla
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>\<psi>'. \<lbrakk>nprv F (scnj G); nprv (G \<union> F) \<psi>; F \<subseteq> fmla; finite F; G \<subseteq> fmla; finite G; \<psi> \<in> fmla; \<psi>' \<in> G\<rbrakk> \<Longrightarrow> nprv F \<psi>'
 2. \<lbrakk>nprv F (scnj G); nprv (G \<union> F) \<psi>; F \<subseteq> fmla; finite F; G \<subseteq> fmla; finite G; \<psi> \<in> fmla\<rbrakk> \<Longrightarrow> nprv (G \<union> F) \<psi>
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>nprv F (scnj G); nprv (G \<union> F) \<psi>; F \<subseteq> fmla; finite F; G \<subseteq> fmla; finite G; \<psi> \<in> fmla; \<psi>'_ \<in> G\<rbrakk> \<Longrightarrow> nprv F \<psi>'_
[PROOF STEP]
by (meson in_mono nprv_def prv_prv_imp_trans prv_scnj_imp_in scnj)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>nprv F (scnj G); nprv (G \<union> F) \<psi>; F \<subseteq> fmla; finite F; G \<subseteq> fmla; finite G; \<psi> \<in> fmla\<rbrakk> \<Longrightarrow> nprv (G \<union> F) \<psi>
[PROOF STEP]
.


[STATEMENT]
lemma nprv_lcnjI:
"(\<And> \<psi>. \<psi> \<in> set \<psi>s \<Longrightarrow> nprv F \<psi>) \<Longrightarrow>
 F \<subseteq> fmla \<Longrightarrow> finite F \<Longrightarrow> set \<psi>s \<subseteq> fmla \<Longrightarrow>
 nprv F (lcnj \<psi>s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>\<psi>. \<psi> \<in> set \<psi>s \<Longrightarrow> nprv F \<psi>; F \<subseteq> fmla; finite F; set \<psi>s \<subseteq> fmla\<rbrakk> \<Longrightarrow> nprv F (lcnj \<psi>s)
[PROOF STEP]
unfolding nprv_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>\<psi>. \<psi> \<in> set \<psi>s \<Longrightarrow> prv (imp (scnj F) \<psi>); F \<subseteq> fmla; finite F; set \<psi>s \<subseteq> fmla\<rbrakk> \<Longrightarrow> prv (imp (scnj F) (lcnj \<psi>s))
[PROOF STEP]
by (simp add: prv_imp_lcnj)


[STATEMENT]
lemma nprv_lcnjE:
"nprv F (lcnj \<phi>s) \<Longrightarrow> nprv (set \<phi>s \<union> F) \<psi> \<Longrightarrow>
 F \<subseteq> fmla \<Longrightarrow> finite F \<Longrightarrow> set \<phi>s \<subseteq> fmla \<Longrightarrow> \<psi> \<in> fmla \<Longrightarrow>
 nprv F \<psi>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>nprv F (lcnj \<phi>s); nprv (set \<phi>s \<union> F) \<psi>; F \<subseteq> fmla; finite F; set \<phi>s \<subseteq> fmla; \<psi> \<in> fmla\<rbrakk> \<Longrightarrow> nprv F \<psi>
[PROOF STEP]
apply(rule nprv_cut_set[of _ "set \<phi>s \<union> F"])
[PROOF STATE]
proof (prove)
goal (7 subgoals):
 1. \<lbrakk>nprv F (lcnj \<phi>s); nprv (set \<phi>s \<union> F) \<psi>; F \<subseteq> fmla; finite F; set \<phi>s \<subseteq> fmla; \<psi> \<in> fmla\<rbrakk> \<Longrightarrow> finite F
 2. \<lbrakk>nprv F (lcnj \<phi>s); nprv (set \<phi>s \<union> F) \<psi>; F \<subseteq> fmla; finite F; set \<phi>s \<subseteq> fmla; \<psi> \<in> fmla\<rbrakk> \<Longrightarrow> F \<subseteq> fmla
 3. \<lbrakk>nprv F (lcnj \<phi>s); nprv (set \<phi>s \<union> F) \<psi>; F \<subseteq> fmla; finite F; set \<phi>s \<subseteq> fmla; \<psi> \<in> fmla\<rbrakk> \<Longrightarrow> finite (set \<phi>s \<union> F)
 4. \<lbrakk>nprv F (lcnj \<phi>s); nprv (set \<phi>s \<union> F) \<psi>; F \<subseteq> fmla; finite F; set \<phi>s \<subseteq> fmla; \<psi> \<in> fmla\<rbrakk> \<Longrightarrow> set \<phi>s \<union> F \<subseteq> fmla
 5. \<lbrakk>nprv F (lcnj \<phi>s); nprv (set \<phi>s \<union> F) \<psi>; F \<subseteq> fmla; finite F; set \<phi>s \<subseteq> fmla; \<psi> \<in> fmla\<rbrakk> \<Longrightarrow> \<psi> \<in> fmla
 6. \<And>\<psi>'. \<lbrakk>nprv F (lcnj \<phi>s); nprv (set \<phi>s \<union> F) \<psi>; F \<subseteq> fmla; finite F; set \<phi>s \<subseteq> fmla; \<psi> \<in> fmla; \<psi>' \<in> set \<phi>s \<union> F\<rbrakk> \<Longrightarrow> nprv F \<psi>'
 7. \<lbrakk>nprv F (lcnj \<phi>s); nprv (set \<phi>s \<union> F) \<psi>; F \<subseteq> fmla; finite F; set \<phi>s \<subseteq> fmla; \<psi> \<in> fmla\<rbrakk> \<Longrightarrow> nprv (set \<phi>s \<union> F \<union> F) \<psi>
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>nprv F (lcnj \<phi>s); nprv (set \<phi>s \<union> F) \<psi>; F \<subseteq> fmla; finite F; set \<phi>s \<subseteq> fmla; \<psi> \<in> fmla\<rbrakk> \<Longrightarrow> finite F
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<lbrakk>nprv F (lcnj \<phi>s); nprv (set \<phi>s \<union> F) \<psi>; F \<subseteq> fmla; finite F; set \<phi>s \<subseteq> fmla; \<psi> \<in> fmla\<rbrakk> \<Longrightarrow> F \<subseteq> fmla
 2. \<lbrakk>nprv F (lcnj \<phi>s); nprv (set \<phi>s \<union> F) \<psi>; F \<subseteq> fmla; finite F; set \<phi>s \<subseteq> fmla; \<psi> \<in> fmla\<rbrakk> \<Longrightarrow> finite (set \<phi>s \<union> F)
 3. \<lbrakk>nprv F (lcnj \<phi>s); nprv (set \<phi>s \<union> F) \<psi>; F \<subseteq> fmla; finite F; set \<phi>s \<subseteq> fmla; \<psi> \<in> fmla\<rbrakk> \<Longrightarrow> set \<phi>s \<union> F \<subseteq> fmla
 4. \<lbrakk>nprv F (lcnj \<phi>s); nprv (set \<phi>s \<union> F) \<psi>; F \<subseteq> fmla; finite F; set \<phi>s \<subseteq> fmla; \<psi> \<in> fmla\<rbrakk> \<Longrightarrow> \<psi> \<in> fmla
 5. \<And>\<psi>'. \<lbrakk>nprv F (lcnj \<phi>s); nprv (set \<phi>s \<union> F) \<psi>; F \<subseteq> fmla; finite F; set \<phi>s \<subseteq> fmla; \<psi> \<in> fmla; \<psi>' \<in> set \<phi>s \<union> F\<rbrakk> \<Longrightarrow> nprv F \<psi>'
 6. \<lbrakk>nprv F (lcnj \<phi>s); nprv (set \<phi>s \<union> F) \<psi>; F \<subseteq> fmla; finite F; set \<phi>s \<subseteq> fmla; \<psi> \<in> fmla\<rbrakk> \<Longrightarrow> nprv (set \<phi>s \<union> F \<union> F) \<psi>
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>nprv F (lcnj \<phi>s); nprv (set \<phi>s \<union> F) \<psi>; F \<subseteq> fmla; finite F; set \<phi>s \<subseteq> fmla; \<psi> \<in> fmla\<rbrakk> \<Longrightarrow> F \<subseteq> fmla
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<lbrakk>nprv F (lcnj \<phi>s); nprv (set \<phi>s \<union> F) \<psi>; F \<subseteq> fmla; finite F; set \<phi>s \<subseteq> fmla; \<psi> \<in> fmla\<rbrakk> \<Longrightarrow> finite (set \<phi>s \<union> F)
 2. \<lbrakk>nprv F (lcnj \<phi>s); nprv (set \<phi>s \<union> F) \<psi>; F \<subseteq> fmla; finite F; set \<phi>s \<subseteq> fmla; \<psi> \<in> fmla\<rbrakk> \<Longrightarrow> set \<phi>s \<union> F \<subseteq> fmla
 3. \<lbrakk>nprv F (lcnj \<phi>s); nprv (set \<phi>s \<union> F) \<psi>; F \<subseteq> fmla; finite F; set \<phi>s \<subseteq> fmla; \<psi> \<in> fmla\<rbrakk> \<Longrightarrow> \<psi> \<in> fmla
 4. \<And>\<psi>'. \<lbrakk>nprv F (lcnj \<phi>s); nprv (set \<phi>s \<union> F) \<psi>; F \<subseteq> fmla; finite F; set \<phi>s \<subseteq> fmla; \<psi> \<in> fmla; \<psi>' \<in> set \<phi>s \<union> F\<rbrakk> \<Longrightarrow> nprv F \<psi>'
 5. \<lbrakk>nprv F (lcnj \<phi>s); nprv (set \<phi>s \<union> F) \<psi>; F \<subseteq> fmla; finite F; set \<phi>s \<subseteq> fmla; \<psi> \<in> fmla\<rbrakk> \<Longrightarrow> nprv (set \<phi>s \<union> F \<union> F) \<psi>
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>nprv F (lcnj \<phi>s); nprv (set \<phi>s \<union> F) \<psi>; F \<subseteq> fmla; finite F; set \<phi>s \<subseteq> fmla; \<psi> \<in> fmla\<rbrakk> \<Longrightarrow> finite (set \<phi>s \<union> F)
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>nprv F (lcnj \<phi>s); nprv (set \<phi>s \<union> F) \<psi>; F \<subseteq> fmla; finite F; set \<phi>s \<subseteq> fmla; \<psi> \<in> fmla\<rbrakk> \<Longrightarrow> set \<phi>s \<union> F \<subseteq> fmla
 2. \<lbrakk>nprv F (lcnj \<phi>s); nprv (set \<phi>s \<union> F) \<psi>; F \<subseteq> fmla; finite F; set \<phi>s \<subseteq> fmla; \<psi> \<in> fmla\<rbrakk> \<Longrightarrow> \<psi> \<in> fmla
 3. \<And>\<psi>'. \<lbrakk>nprv F (lcnj \<phi>s); nprv (set \<phi>s \<union> F) \<psi>; F \<subseteq> fmla; finite F; set \<phi>s \<subseteq> fmla; \<psi> \<in> fmla; \<psi>' \<in> set \<phi>s \<union> F\<rbrakk> \<Longrightarrow> nprv F \<psi>'
 4. \<lbrakk>nprv F (lcnj \<phi>s); nprv (set \<phi>s \<union> F) \<psi>; F \<subseteq> fmla; finite F; set \<phi>s \<subseteq> fmla; \<psi> \<in> fmla\<rbrakk> \<Longrightarrow> nprv (set \<phi>s \<union> F \<union> F) \<psi>
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>nprv F (lcnj \<phi>s); nprv (set \<phi>s \<union> F) \<psi>; F \<subseteq> fmla; finite F; set \<phi>s \<subseteq> fmla; \<psi> \<in> fmla\<rbrakk> \<Longrightarrow> set \<phi>s \<union> F \<subseteq> fmla
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>nprv F (lcnj \<phi>s); nprv (set \<phi>s \<union> F) \<psi>; F \<subseteq> fmla; finite F; set \<phi>s \<subseteq> fmla; \<psi> \<in> fmla\<rbrakk> \<Longrightarrow> \<psi> \<in> fmla
 2. \<And>\<psi>'. \<lbrakk>nprv F (lcnj \<phi>s); nprv (set \<phi>s \<union> F) \<psi>; F \<subseteq> fmla; finite F; set \<phi>s \<subseteq> fmla; \<psi> \<in> fmla; \<psi>' \<in> set \<phi>s \<union> F\<rbrakk> \<Longrightarrow> nprv F \<psi>'
 3. \<lbrakk>nprv F (lcnj \<phi>s); nprv (set \<phi>s \<union> F) \<psi>; F \<subseteq> fmla; finite F; set \<phi>s \<subseteq> fmla; \<psi> \<in> fmla\<rbrakk> \<Longrightarrow> nprv (set \<phi>s \<union> F \<union> F) \<psi>
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>nprv F (lcnj \<phi>s); nprv (set \<phi>s \<union> F) \<psi>; F \<subseteq> fmla; finite F; set \<phi>s \<subseteq> fmla; \<psi> \<in> fmla\<rbrakk> \<Longrightarrow> \<psi> \<in> fmla
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>\<psi>'. \<lbrakk>nprv F (lcnj \<phi>s); nprv (set \<phi>s \<union> F) \<psi>; F \<subseteq> fmla; finite F; set \<phi>s \<subseteq> fmla; \<psi> \<in> fmla; \<psi>' \<in> set \<phi>s \<union> F\<rbrakk> \<Longrightarrow> nprv F \<psi>'
 2. \<lbrakk>nprv F (lcnj \<phi>s); nprv (set \<phi>s \<union> F) \<psi>; F \<subseteq> fmla; finite F; set \<phi>s \<subseteq> fmla; \<psi> \<in> fmla\<rbrakk> \<Longrightarrow> nprv (set \<phi>s \<union> F \<union> F) \<psi>
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>nprv F (lcnj \<phi>s); nprv (set \<phi>s \<union> F) \<psi>; F \<subseteq> fmla; finite F; set \<phi>s \<subseteq> fmla; \<psi> \<in> fmla; \<psi>'_ \<in> set \<phi>s \<union> F\<rbrakk> \<Longrightarrow> nprv F \<psi>'_
[PROOF STEP]
apply (elim UnE)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>nprv F (lcnj \<phi>s); nprv (set \<phi>s \<union> F) \<psi>; F \<subseteq> fmla; finite F; set \<phi>s \<subseteq> fmla; \<psi> \<in> fmla; \<psi>'_ \<in> set \<phi>s\<rbrakk> \<Longrightarrow> nprv F \<psi>'_
 2. \<lbrakk>nprv F (lcnj \<phi>s); nprv (set \<phi>s \<union> F) \<psi>; F \<subseteq> fmla; finite F; set \<phi>s \<subseteq> fmla; \<psi> \<in> fmla; \<psi>'_ \<in> F\<rbrakk> \<Longrightarrow> nprv F \<psi>'_
[PROOF STEP]
apply (meson lcnj nprv_def prv_lcnj_imp_in prv_prv_imp_trans scnj subset_code(1))
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>nprv F (lcnj \<phi>s); nprv (set \<phi>s \<union> F) \<psi>; F \<subseteq> fmla; finite F; set \<phi>s \<subseteq> fmla; \<psi> \<in> fmla; \<psi>'_ \<in> F\<rbrakk> \<Longrightarrow> nprv F \<psi>'_
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>nprv F (lcnj \<phi>s); nprv (set \<phi>s \<union> F) \<psi>; F \<subseteq> fmla; finite F; set \<phi>s \<subseteq> fmla; \<psi> \<in> fmla\<rbrakk> \<Longrightarrow> nprv (set \<phi>s \<union> F \<union> F) \<psi>
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>nprv F (lcnj \<phi>s); nprv (set \<phi>s \<union> F) \<psi>; F \<subseteq> fmla; finite F; set \<phi>s \<subseteq> fmla; \<psi> \<in> fmla\<rbrakk> \<Longrightarrow> nprv (set \<phi>s \<union> F \<union> F) \<psi>
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
.


[STATEMENT]
lemma nprv_sdsjI:
"nprv F \<phi> \<Longrightarrow>
 F \<subseteq> fmla \<Longrightarrow> finite F \<Longrightarrow> G \<subseteq> fmla \<Longrightarrow> finite G \<Longrightarrow> \<phi> \<in> G \<Longrightarrow>
 nprv F (sdsj G)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>nprv F \<phi>; F \<subseteq> fmla; finite F; G \<subseteq> fmla; finite G; \<phi> \<in> G\<rbrakk> \<Longrightarrow> nprv F (sdsj G)
[PROOF STEP]
unfolding nprv_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>prv (imp (scnj F) \<phi>); F \<subseteq> fmla; finite F; G \<subseteq> fmla; finite G; \<phi> \<in> G\<rbrakk> \<Longrightarrow> prv (imp (scnj F) (sdsj G))
[PROOF STEP]
by (simp add: prv_imp_sdsj)


[STATEMENT]
lemma nprv_sdsjE:
assumes "nprv F (sdsj G)"
and "\<And> \<psi>. \<psi> \<in> G \<Longrightarrow> nprv (insert \<psi> F) \<chi>"
and "F \<subseteq> fmla" "finite F" "G \<subseteq> fmla" "finite G" "\<chi> \<in> fmla"
shows "nprv F \<chi>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nprv F \<chi>
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. nprv F \<chi>
[PROOF STEP]
have 0: "prv (imp (sdsj G) (imp (scnj F) \<chi>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (imp (sdsj G) (imp (scnj F) \<chi>))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
nprv F (sdsj G)
?\<psi> \<in> G \<Longrightarrow> nprv (insert ?\<psi> F) \<chi>
F \<subseteq> fmla
finite F
G \<subseteq> fmla
finite G
\<chi> \<in> fmla

goal (1 subgoal):
 1. prv (imp (sdsj G) (imp (scnj F) \<chi>))
[PROOF STEP]
apply(intro prv_sdsj_imp)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>nprv F (sdsj G); \<And>\<psi>. \<psi> \<in> G \<Longrightarrow> nprv (insert \<psi> F) \<chi>; F \<subseteq> fmla; finite F; G \<subseteq> fmla; finite G; \<chi> \<in> fmla\<rbrakk> \<Longrightarrow> imp (scnj F) \<chi> \<in> fmla
 2. \<lbrakk>nprv F (sdsj G); \<And>\<psi>. \<psi> \<in> G \<Longrightarrow> nprv (insert \<psi> F) \<chi>; F \<subseteq> fmla; finite F; G \<subseteq> fmla; finite G; \<chi> \<in> fmla\<rbrakk> \<Longrightarrow> G \<subseteq> fmla
 3. \<lbrakk>nprv F (sdsj G); \<And>\<psi>. \<psi> \<in> G \<Longrightarrow> nprv (insert \<psi> F) \<chi>; F \<subseteq> fmla; finite F; G \<subseteq> fmla; finite G; \<chi> \<in> fmla\<rbrakk> \<Longrightarrow> finite G
 4. \<And>\<phi>. \<lbrakk>nprv F (sdsj G); \<And>\<psi>. \<psi> \<in> G \<Longrightarrow> nprv (insert \<psi> F) \<chi>; F \<subseteq> fmla; finite F; G \<subseteq> fmla; finite G; \<chi> \<in> fmla; \<phi> \<in> G\<rbrakk> \<Longrightarrow> prv (imp \<phi> (imp (scnj F) \<chi>))
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>nprv F (sdsj G); \<And>\<psi>. \<psi> \<in> G \<Longrightarrow> nprv (insert \<psi> F) \<chi>; F \<subseteq> fmla; finite F; G \<subseteq> fmla; finite G; \<chi> \<in> fmla\<rbrakk> \<Longrightarrow> imp (scnj F) \<chi> \<in> fmla
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>nprv F (sdsj G); \<And>\<psi>. \<psi> \<in> G \<Longrightarrow> nprv (insert \<psi> F) \<chi>; F \<subseteq> fmla; finite F; G \<subseteq> fmla; finite G; \<chi> \<in> fmla\<rbrakk> \<Longrightarrow> G \<subseteq> fmla
 2. \<lbrakk>nprv F (sdsj G); \<And>\<psi>. \<psi> \<in> G \<Longrightarrow> nprv (insert \<psi> F) \<chi>; F \<subseteq> fmla; finite F; G \<subseteq> fmla; finite G; \<chi> \<in> fmla\<rbrakk> \<Longrightarrow> finite G
 3. \<And>\<phi>. \<lbrakk>nprv F (sdsj G); \<And>\<psi>. \<psi> \<in> G \<Longrightarrow> nprv (insert \<psi> F) \<chi>; F \<subseteq> fmla; finite F; G \<subseteq> fmla; finite G; \<chi> \<in> fmla; \<phi> \<in> G\<rbrakk> \<Longrightarrow> prv (imp \<phi> (imp (scnj F) \<chi>))
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>nprv F (sdsj G); \<And>\<psi>. \<psi> \<in> G \<Longrightarrow> nprv (insert \<psi> F) \<chi>; F \<subseteq> fmla; finite F; G \<subseteq> fmla; finite G; \<chi> \<in> fmla\<rbrakk> \<Longrightarrow> G \<subseteq> fmla
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>nprv F (sdsj G); \<And>\<psi>. \<psi> \<in> G \<Longrightarrow> nprv (insert \<psi> F) \<chi>; F \<subseteq> fmla; finite F; G \<subseteq> fmla; finite G; \<chi> \<in> fmla\<rbrakk> \<Longrightarrow> finite G
 2. \<And>\<phi>. \<lbrakk>nprv F (sdsj G); \<And>\<psi>. \<psi> \<in> G \<Longrightarrow> nprv (insert \<psi> F) \<chi>; F \<subseteq> fmla; finite F; G \<subseteq> fmla; finite G; \<chi> \<in> fmla; \<phi> \<in> G\<rbrakk> \<Longrightarrow> prv (imp \<phi> (imp (scnj F) \<chi>))
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>nprv F (sdsj G); \<And>\<psi>. \<psi> \<in> G \<Longrightarrow> nprv (insert \<psi> F) \<chi>; F \<subseteq> fmla; finite F; G \<subseteq> fmla; finite G; \<chi> \<in> fmla\<rbrakk> \<Longrightarrow> finite G
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>\<phi>. \<lbrakk>nprv F (sdsj G); \<And>\<psi>. \<psi> \<in> G \<Longrightarrow> nprv (insert \<psi> F) \<chi>; F \<subseteq> fmla; finite F; G \<subseteq> fmla; finite G; \<chi> \<in> fmla; \<phi> \<in> G\<rbrakk> \<Longrightarrow> prv (imp \<phi> (imp (scnj F) \<chi>))
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>nprv F (sdsj G); \<And>\<psi>. \<psi> \<in> G \<Longrightarrow> nprv (insert \<psi> F) \<chi>; F \<subseteq> fmla; finite F; G \<subseteq> fmla; finite G; \<chi> \<in> fmla; \<phi>_ \<in> G\<rbrakk> \<Longrightarrow> prv (imp \<phi>_ (imp (scnj F) \<chi>))
[PROOF STEP]
by (meson nprv_def nprv_impI prv_imp_com scnj set_rev_mp)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
prv (imp (sdsj G) (imp (scnj F) \<chi>))

goal (1 subgoal):
 1. nprv F \<chi>
[PROOF STEP]
hence "nprv F (imp (sdsj G) \<chi>)"
[PROOF STATE]
proof (prove)
using this:
prv (imp (sdsj G) (imp (scnj F) \<chi>))

goal (1 subgoal):
 1. nprv F (imp (sdsj G) \<chi>)
[PROOF STEP]
by (simp add: 0 assms nprv_def prv_imp_com)
[PROOF STATE]
proof (state)
this:
nprv F (imp (sdsj G) \<chi>)

goal (1 subgoal):
 1. nprv F \<chi>
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
nprv F (imp (sdsj G) \<chi>)

goal (1 subgoal):
 1. nprv F \<chi>
[PROOF STEP]
using assms nprv_mp
[PROOF STATE]
proof (prove)
using this:
nprv F (imp (sdsj G) \<chi>)
nprv F (sdsj G)
?\<psi> \<in> G \<Longrightarrow> nprv (insert ?\<psi> F) \<chi>
F \<subseteq> fmla
finite F
G \<subseteq> fmla
finite G
\<chi> \<in> fmla
\<lbrakk>nprv ?F (imp ?\<phi> ?\<psi>); nprv ?F ?\<phi>; ?F \<subseteq> fmla; finite ?F; ?\<phi> \<in> fmla; ?\<psi> \<in> fmla\<rbrakk> \<Longrightarrow> nprv ?F ?\<psi>

goal (1 subgoal):
 1. nprv F \<chi>
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
nprv F \<chi>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma nprv_ldsjI:
"nprv F \<phi> \<Longrightarrow>
 F \<subseteq> fmla \<Longrightarrow> finite F \<Longrightarrow> set \<phi>s \<subseteq> fmla \<Longrightarrow>  \<phi> \<in> set \<phi>s \<Longrightarrow>
 nprv F (ldsj \<phi>s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>nprv F \<phi>; F \<subseteq> fmla; finite F; set \<phi>s \<subseteq> fmla; \<phi> \<in> set \<phi>s\<rbrakk> \<Longrightarrow> nprv F (ldsj \<phi>s)
[PROOF STEP]
unfolding nprv_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>prv (imp (scnj F) \<phi>); F \<subseteq> fmla; finite F; set \<phi>s \<subseteq> fmla; \<phi> \<in> set \<phi>s\<rbrakk> \<Longrightarrow> prv (imp (scnj F) (ldsj \<phi>s))
[PROOF STEP]
by(simp add: prv_imp_ldsj)


[STATEMENT]
lemma nprv_ldsjE:
assumes "nprv F (ldsj \<psi>s)"
and "\<And> \<psi>. \<psi> \<in> set \<psi>s \<Longrightarrow> nprv (insert \<psi> F) \<chi>"
and "F \<subseteq> fmla" "finite F" "set \<psi>s \<subseteq> fmla"  "\<chi> \<in> fmla"
shows "nprv F \<chi>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nprv F \<chi>
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. nprv F \<chi>
[PROOF STEP]
have 0: "prv (imp (ldsj \<psi>s) (imp (scnj F) \<chi>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (imp (ldsj \<psi>s) (imp (scnj F) \<chi>))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
nprv F (ldsj \<psi>s)
?\<psi> \<in> set \<psi>s \<Longrightarrow> nprv (insert ?\<psi> F) \<chi>
F \<subseteq> fmla
finite F
set \<psi>s \<subseteq> fmla
\<chi> \<in> fmla

goal (1 subgoal):
 1. prv (imp (ldsj \<psi>s) (imp (scnj F) \<chi>))
[PROOF STEP]
apply(intro prv_ldsj_imp)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>nprv F (ldsj \<psi>s); \<And>\<psi>. \<psi> \<in> set \<psi>s \<Longrightarrow> nprv (insert \<psi> F) \<chi>; F \<subseteq> fmla; finite F; set \<psi>s \<subseteq> fmla; \<chi> \<in> fmla\<rbrakk> \<Longrightarrow> imp (scnj F) \<chi> \<in> fmla
 2. \<lbrakk>nprv F (ldsj \<psi>s); \<And>\<psi>. \<psi> \<in> set \<psi>s \<Longrightarrow> nprv (insert \<psi> F) \<chi>; F \<subseteq> fmla; finite F; set \<psi>s \<subseteq> fmla; \<chi> \<in> fmla\<rbrakk> \<Longrightarrow> set \<psi>s \<subseteq> fmla
 3. \<And>\<phi>. \<lbrakk>nprv F (ldsj \<psi>s); \<And>\<psi>. \<psi> \<in> set \<psi>s \<Longrightarrow> nprv (insert \<psi> F) \<chi>; F \<subseteq> fmla; finite F; set \<psi>s \<subseteq> fmla; \<chi> \<in> fmla; \<phi> \<in> set \<psi>s\<rbrakk> \<Longrightarrow> prv (imp \<phi> (imp (scnj F) \<chi>))
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>nprv F (ldsj \<psi>s); \<And>\<psi>. \<psi> \<in> set \<psi>s \<Longrightarrow> nprv (insert \<psi> F) \<chi>; F \<subseteq> fmla; finite F; set \<psi>s \<subseteq> fmla; \<chi> \<in> fmla\<rbrakk> \<Longrightarrow> imp (scnj F) \<chi> \<in> fmla
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>nprv F (ldsj \<psi>s); \<And>\<psi>. \<psi> \<in> set \<psi>s \<Longrightarrow> nprv (insert \<psi> F) \<chi>; F \<subseteq> fmla; finite F; set \<psi>s \<subseteq> fmla; \<chi> \<in> fmla\<rbrakk> \<Longrightarrow> set \<psi>s \<subseteq> fmla
 2. \<And>\<phi>. \<lbrakk>nprv F (ldsj \<psi>s); \<And>\<psi>. \<psi> \<in> set \<psi>s \<Longrightarrow> nprv (insert \<psi> F) \<chi>; F \<subseteq> fmla; finite F; set \<psi>s \<subseteq> fmla; \<chi> \<in> fmla; \<phi> \<in> set \<psi>s\<rbrakk> \<Longrightarrow> prv (imp \<phi> (imp (scnj F) \<chi>))
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>nprv F (ldsj \<psi>s); \<And>\<psi>. \<psi> \<in> set \<psi>s \<Longrightarrow> nprv (insert \<psi> F) \<chi>; F \<subseteq> fmla; finite F; set \<psi>s \<subseteq> fmla; \<chi> \<in> fmla\<rbrakk> \<Longrightarrow> set \<psi>s \<subseteq> fmla
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>\<phi>. \<lbrakk>nprv F (ldsj \<psi>s); \<And>\<psi>. \<psi> \<in> set \<psi>s \<Longrightarrow> nprv (insert \<psi> F) \<chi>; F \<subseteq> fmla; finite F; set \<psi>s \<subseteq> fmla; \<chi> \<in> fmla; \<phi> \<in> set \<psi>s\<rbrakk> \<Longrightarrow> prv (imp \<phi> (imp (scnj F) \<chi>))
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>nprv F (ldsj \<psi>s); \<And>\<psi>. \<psi> \<in> set \<psi>s \<Longrightarrow> nprv (insert \<psi> F) \<chi>; F \<subseteq> fmla; finite F; set \<psi>s \<subseteq> fmla; \<chi> \<in> fmla; \<phi>_ \<in> set \<psi>s\<rbrakk> \<Longrightarrow> prv (imp \<phi>_ (imp (scnj F) \<chi>))
[PROOF STEP]
by (meson nprv_def nprv_impI prv_imp_com scnj set_rev_mp)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
prv (imp (ldsj \<psi>s) (imp (scnj F) \<chi>))

goal (1 subgoal):
 1. nprv F \<chi>
[PROOF STEP]
hence "nprv F (imp (ldsj \<psi>s) \<chi>)"
[PROOF STATE]
proof (prove)
using this:
prv (imp (ldsj \<psi>s) (imp (scnj F) \<chi>))

goal (1 subgoal):
 1. nprv F (imp (ldsj \<psi>s) \<chi>)
[PROOF STEP]
by (simp add: 0 assms nprv_def prv_imp_com)
[PROOF STATE]
proof (state)
this:
nprv F (imp (ldsj \<psi>s) \<chi>)

goal (1 subgoal):
 1. nprv F \<chi>
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
nprv F (imp (ldsj \<psi>s) \<chi>)

goal (1 subgoal):
 1. nprv F \<chi>
[PROOF STEP]
using assms nprv_mp
[PROOF STATE]
proof (prove)
using this:
nprv F (imp (ldsj \<psi>s) \<chi>)
nprv F (ldsj \<psi>s)
?\<psi> \<in> set \<psi>s \<Longrightarrow> nprv (insert ?\<psi> F) \<chi>
F \<subseteq> fmla
finite F
set \<psi>s \<subseteq> fmla
\<chi> \<in> fmla
\<lbrakk>nprv ?F (imp ?\<phi> ?\<psi>); nprv ?F ?\<phi>; ?F \<subseteq> fmla; finite ?F; ?\<phi> \<in> fmla; ?\<psi> \<in> fmla\<rbrakk> \<Longrightarrow> nprv ?F ?\<psi>

goal (1 subgoal):
 1. nprv F \<chi>
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
nprv F \<chi>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma nprv_allI:
"nprv F \<phi> \<Longrightarrow>
 F \<subseteq> fmla \<Longrightarrow> finite F \<Longrightarrow> \<phi> \<in> fmla \<Longrightarrow> x \<in> var \<Longrightarrow> x \<notin> \<Union> (Fvars ` F) \<Longrightarrow>
 nprv F (all x \<phi>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>nprv F \<phi>; F \<subseteq> fmla; finite F; \<phi> \<in> fmla; x \<in> var; x \<notin> \<Union> (Fvars ` F)\<rbrakk> \<Longrightarrow> nprv F (all x \<phi>)
[PROOF STEP]
unfolding nprv_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>prv (imp (scnj F) \<phi>); F \<subseteq> fmla; finite F; \<phi> \<in> fmla; x \<in> var; x \<notin> \<Union> (Fvars ` F)\<rbrakk> \<Longrightarrow> prv (imp (scnj F) (all x \<phi>))
[PROOF STEP]
by (rule prv_all_imp_gen) auto


[STATEMENT]
lemma nprv_allE:
assumes "nprv F (all x \<phi>)" "nprv (insert (subst \<phi> t x) F) \<psi>"
"F \<subseteq> fmla" "finite F" "\<phi> \<in> fmla" "t \<in> trm" "x \<in> var" "\<psi> \<in> fmla"
shows "nprv F \<psi>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nprv F \<psi>
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. nprv F \<psi>
[PROOF STEP]
have "nprv F (subst \<phi> t x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nprv F (subst \<phi> t x)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
nprv F (all x \<phi>)
nprv (insert (subst \<phi> t x) F) \<psi>
F \<subseteq> fmla
finite F
\<phi> \<in> fmla
t \<in> trm
x \<in> var
\<psi> \<in> fmla

goal (1 subgoal):
 1. nprv F (subst \<phi> t x)
[PROOF STEP]
unfolding nprv_def
[PROOF STATE]
proof (prove)
using this:
prv (imp (scnj F) (all x \<phi>))
prv (imp (scnj (insert (subst \<phi> t x) F)) \<psi>)
F \<subseteq> fmla
finite F
\<phi> \<in> fmla
t \<in> trm
x \<in> var
\<psi> \<in> fmla

goal (1 subgoal):
 1. prv (imp (scnj F) (subst \<phi> t x))
[PROOF STEP]
by (meson all subst prv_all_inst prv_prv_imp_trans scnj)
[PROOF STATE]
proof (state)
this:
nprv F (subst \<phi> t x)

goal (1 subgoal):
 1. nprv F \<psi>
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
nprv F (subst \<phi> t x)

goal (1 subgoal):
 1. nprv F \<psi>
[PROOF STEP]
by (meson assms local.subst nprv_cut)
[PROOF STATE]
proof (state)
this:
nprv F \<psi>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma nprv_exiI:
"nprv F (subst \<phi> t x) \<Longrightarrow>
 F \<subseteq> fmla \<Longrightarrow> finite F \<Longrightarrow> \<phi> \<in> fmla \<Longrightarrow> t \<in> trm \<Longrightarrow> x \<in> var \<Longrightarrow>
 nprv F (exi x \<phi>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>nprv F (subst \<phi> t x); F \<subseteq> fmla; finite F; \<phi> \<in> fmla; t \<in> trm; x \<in> var\<rbrakk> \<Longrightarrow> nprv F (exi x \<phi>)
[PROOF STEP]
unfolding nprv_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>prv (imp (scnj F) (subst \<phi> t x)); F \<subseteq> fmla; finite F; \<phi> \<in> fmla; t \<in> trm; x \<in> var\<rbrakk> \<Longrightarrow> prv (imp (scnj F) (exi x \<phi>))
[PROOF STEP]
by (meson exi local.subst prv_exi_inst prv_prv_imp_trans scnj)


[STATEMENT]
lemma nprv_exiE:
assumes n: "nprv F (exi x \<phi>)"
and nn: "nprv (insert \<phi> F) \<psi>"
and 0[simp]: "F \<subseteq> fmla" "finite F" "\<phi> \<in> fmla" "x \<in> var" "\<psi> \<in> fmla"
and x: "x \<notin> \<Union> (Fvars ` F)" "x \<notin> Fvars \<psi>"
shows "nprv F \<psi>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nprv F \<psi>
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. nprv F \<psi>
[PROOF STEP]
have "nprv F (imp (exi x \<phi>) \<psi>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nprv F (imp (exi x \<phi>) \<psi>)
[PROOF STEP]
unfolding nprv_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (imp (scnj F) (imp (exi x \<phi>) \<psi>))
[PROOF STEP]
apply(rule prv_imp_com)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. exi x \<phi> \<in> fmla
 2. scnj F \<in> fmla
 3. \<psi> \<in> fmla
 4. prv (imp (exi x \<phi>) (imp (scnj F) \<psi>))
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. exi x \<phi> \<in> fmla
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. scnj F \<in> fmla
 2. \<psi> \<in> fmla
 3. prv (imp (exi x \<phi>) (imp (scnj F) \<psi>))
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. scnj F \<in> fmla
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<psi> \<in> fmla
 2. prv (imp (exi x \<phi>) (imp (scnj F) \<psi>))
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<psi> \<in> fmla
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (imp (exi x \<phi>) (imp (scnj F) \<psi>))
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (imp (exi x \<phi>) (imp (scnj F) \<psi>))
[PROOF STEP]
apply(rule prv_exi_imp_gen)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. x \<in> var
 2. \<phi> \<in> fmla
 3. imp (scnj F) \<psi> \<in> fmla
 4. x \<notin> Fvars (imp (scnj F) \<psi>)
 5. prv (imp \<phi> (imp (scnj F) \<psi>))
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> var
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<phi> \<in> fmla
 2. imp (scnj F) \<psi> \<in> fmla
 3. x \<notin> Fvars (imp (scnj F) \<psi>)
 4. prv (imp \<phi> (imp (scnj F) \<psi>))
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<phi> \<in> fmla
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. imp (scnj F) \<psi> \<in> fmla
 2. x \<notin> Fvars (imp (scnj F) \<psi>)
 3. prv (imp \<phi> (imp (scnj F) \<psi>))
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. imp (scnj F) \<psi> \<in> fmla
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. x \<notin> Fvars (imp (scnj F) \<psi>)
 2. prv (imp \<phi> (imp (scnj F) \<psi>))
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<notin> Fvars (imp (scnj F) \<psi>)
[PROOF STEP]
using x
[PROOF STATE]
proof (prove)
using this:
x \<notin> \<Union> (Fvars ` F)
x \<notin> Fvars \<psi>

goal (1 subgoal):
 1. x \<notin> Fvars (imp (scnj F) \<psi>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (imp \<phi> (imp (scnj F) \<psi>))
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (imp \<phi> (imp (scnj F) \<psi>))
[PROOF STEP]
apply(rule prv_imp_com)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. scnj F \<in> fmla
 2. \<phi> \<in> fmla
 3. \<psi> \<in> fmla
 4. prv (imp (scnj F) (imp \<phi> \<psi>))
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. scnj F \<in> fmla
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<phi> \<in> fmla
 2. \<psi> \<in> fmla
 3. prv (imp (scnj F) (imp \<phi> \<psi>))
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<phi> \<in> fmla
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<psi> \<in> fmla
 2. prv (imp (scnj F) (imp \<phi> \<psi>))
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<psi> \<in> fmla
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (imp (scnj F) (imp \<phi> \<psi>))
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (imp (scnj F) (imp \<phi> \<psi>))
[PROOF STEP]
using assms(3-5) assms(7) nn nprv_def nprv_impI
[PROOF STATE]
proof (prove)
using this:
F \<subseteq> fmla
finite F
\<phi> \<in> fmla
\<psi> \<in> fmla
nprv (insert \<phi> F) \<psi>
nprv ?F ?\<phi> \<equiv> prv (imp (scnj ?F) ?\<phi>)
\<lbrakk>nprv (insert ?\<phi> ?F) ?\<psi>; ?F \<subseteq> fmla; finite ?F; ?\<phi> \<in> fmla; ?\<psi> \<in> fmla\<rbrakk> \<Longrightarrow> nprv ?F (imp ?\<phi> ?\<psi>)

goal (1 subgoal):
 1. prv (imp (scnj F) (imp \<phi> \<psi>))
[PROOF STEP]
by blast
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
.
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
.
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
nprv F (imp (exi x \<phi>) \<psi>)

goal (1 subgoal):
 1. nprv F \<psi>
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
nprv F (imp (exi x \<phi>) \<psi>)

goal (1 subgoal):
 1. nprv F \<psi>
[PROOF STEP]
using n assms nprv_mp
[PROOF STATE]
proof (prove)
using this:
nprv F (imp (exi x \<phi>) \<psi>)
nprv F (exi x \<phi>)
nprv F (exi x \<phi>)
nprv (insert \<phi> F) \<psi>
F \<subseteq> fmla
finite F
\<phi> \<in> fmla
x \<in> var
\<psi> \<in> fmla
x \<notin> \<Union> (Fvars ` F)
x \<notin> Fvars \<psi>
\<lbrakk>nprv ?F (imp ?\<phi> ?\<psi>); nprv ?F ?\<phi>; ?F \<subseteq> fmla; finite ?F; ?\<phi> \<in> fmla; ?\<psi> \<in> fmla\<rbrakk> \<Longrightarrow> nprv ?F ?\<psi>

goal (1 subgoal):
 1. nprv F \<psi>
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
nprv F \<psi>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma nprv_addLemmaE:
assumes "prv \<phi>" "nprv (insert \<phi> F) \<psi>"
and "\<phi> \<in> fmla" "\<psi> \<in> fmla" and "F \<subseteq> fmla" and "finite F"
shows "nprv F \<psi>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nprv F \<psi>
[PROOF STEP]
using assms nprv_cut prv_nprvI
[PROOF STATE]
proof (prove)
using this:
prv \<phi>
nprv (insert \<phi> F) \<psi>
\<phi> \<in> fmla
\<psi> \<in> fmla
F \<subseteq> fmla
finite F
\<lbrakk>nprv ?F ?\<phi>; nprv (insert ?\<phi> ?F) ?\<psi>; ?F \<subseteq> fmla; finite ?F; ?\<phi> \<in> fmla; ?\<psi> \<in> fmla\<rbrakk> \<Longrightarrow> nprv ?F ?\<psi>
\<lbrakk>prv ?\<phi>; ?\<phi> \<in> fmla; ?F \<subseteq> fmla; finite ?F\<rbrakk> \<Longrightarrow> nprv ?F ?\<phi>

goal (1 subgoal):
 1. nprv F \<psi>
[PROOF STEP]
by blast


[STATEMENT]
lemma nprv_addImpLemmaI:
assumes "prv (imp \<phi>1 \<phi>2)"
and "F \<subseteq> fmla" "finite F" "\<phi>1 \<in> fmla" "\<phi>2 \<in> fmla"
and "nprv F \<phi>1"
shows "nprv F \<phi>2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nprv F \<phi>2
[PROOF STEP]
by (meson assms nprv_def prv_prv_imp_trans scnj)


[STATEMENT]
lemma nprv_addImpLemmaE:
assumes "prv (imp \<phi>1 \<phi>2)" and "nprv F \<phi>1" and "nprv ((insert \<phi>2) F) \<psi>"
and "F \<subseteq> fmla" "finite F" "\<phi>1 \<in> fmla" "\<phi>2 \<in> fmla" "\<psi> \<in> fmla"
shows "nprv F \<psi>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nprv F \<psi>
[PROOF STEP]
using assms nprv_addImpLemmaI nprv_cut
[PROOF STATE]
proof (prove)
using this:
prv (imp \<phi>1 \<phi>2)
nprv F \<phi>1
nprv (insert \<phi>2 F) \<psi>
F \<subseteq> fmla
finite F
\<phi>1 \<in> fmla
\<phi>2 \<in> fmla
\<psi> \<in> fmla
\<lbrakk>prv (imp ?\<phi>1.0 ?\<phi>2.0); ?F \<subseteq> fmla; finite ?F; ?\<phi>1.0 \<in> fmla; ?\<phi>2.0 \<in> fmla; nprv ?F ?\<phi>1.0\<rbrakk> \<Longrightarrow> nprv ?F ?\<phi>2.0
\<lbrakk>nprv ?F ?\<phi>; nprv (insert ?\<phi> ?F) ?\<psi>; ?F \<subseteq> fmla; finite ?F; ?\<phi> \<in> fmla; ?\<psi> \<in> fmla\<rbrakk> \<Longrightarrow> nprv ?F ?\<psi>

goal (1 subgoal):
 1. nprv F \<psi>
[PROOF STEP]
by blast


[STATEMENT]
lemma nprv_addImp2LemmaI:
assumes "prv (imp \<phi>1 (imp \<phi>2 \<phi>3))"
and "F \<subseteq> fmla" "finite F" "\<phi>1 \<in> fmla" "\<phi>2 \<in> fmla" "\<phi>3 \<in> fmla"
and "nprv F \<phi>1" "nprv F \<phi>2"
shows "nprv F \<phi>3"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nprv F \<phi>3
[PROOF STEP]
by (meson assms imp nprv_addImpLemmaI nprv_mp)


[STATEMENT]
lemma nprv_addImp2LemmaE:
assumes "prv (imp \<phi>1 (imp \<phi>2 \<phi>3))" and "nprv F \<phi>1" and "nprv F \<phi>2" and "nprv ((insert \<phi>3) F) \<psi>"
and "F \<subseteq> fmla" "finite F" "\<phi>1 \<in> fmla" "\<phi>2 \<in> fmla"  "\<phi>3 \<in> fmla" "\<psi> \<in> fmla"
shows "nprv F \<psi>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nprv F \<psi>
[PROOF STEP]
by (meson assms nprv_addImp2LemmaI nprv_cut)


[STATEMENT]
lemma nprv_addImp3LemmaI:
assumes "prv (imp \<phi>1 (imp \<phi>2 (imp \<phi>3 \<phi>4)))"
and "F \<subseteq> fmla" "finite F" "\<phi>1 \<in> fmla" "\<phi>2 \<in> fmla" "\<phi>3 \<in> fmla" "\<phi>4 \<in> fmla"
and "nprv F \<phi>1" "nprv F \<phi>2" "nprv F \<phi>3"
shows "nprv F \<phi>4"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nprv F \<phi>4
[PROOF STEP]
by (meson assms imp nprv_addImpLemmaI nprv_mp)


[STATEMENT]
lemma nprv_addImp3LemmaE:
assumes "prv (imp \<phi>1 (imp \<phi>2 (imp \<phi>3 \<phi>4)))"  and "nprv F \<phi>1" and "nprv F \<phi>2" and "nprv F \<phi>3"
and "nprv ((insert \<phi>4) F) \<psi>"
and "F \<subseteq> fmla" "finite F" "\<phi>1 \<in> fmla" "\<phi>2 \<in> fmla" "\<phi>3 \<in> fmla" "\<phi>4 \<in> fmla" "\<psi> \<in> fmla"
shows "nprv F \<psi>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nprv F \<psi>
[PROOF STEP]
by (meson assms nprv_addImp3LemmaI nprv_cut)


[STATEMENT]
lemma nprv_addDsjLemmaE:
assumes "prv (dsj \<phi>1 \<phi>2)" and "nprv (insert \<phi>1 F) \<psi>" and "nprv ((insert \<phi>2) F) \<psi>"
and "F \<subseteq> fmla" "finite F" "\<phi>1 \<in> fmla" "\<phi>2 \<in> fmla" "\<psi> \<in> fmla"
shows "nprv F \<psi>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nprv F \<psi>
[PROOF STEP]
by (meson assms dsj nprv_clear nprv_dsjE prv_nprv0I)


[STATEMENT]
lemma nprv_eql_reflI: "F \<subseteq> fmla \<Longrightarrow> finite F \<Longrightarrow> t \<in> trm \<Longrightarrow> nprv F (eql t t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>F \<subseteq> fmla; finite F; t \<in> trm\<rbrakk> \<Longrightarrow> nprv F (eql t t)
[PROOF STEP]
by (simp add: prv_eql_reflT prv_nprvI)


[STATEMENT]
lemma nprv_eq_eqlI: "t1 = t2 \<Longrightarrow> F \<subseteq> fmla \<Longrightarrow> finite F \<Longrightarrow> t1 \<in> trm \<Longrightarrow> nprv F (eql t1 t2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>t1 = t2; F \<subseteq> fmla; finite F; t1 \<in> trm\<rbrakk> \<Longrightarrow> nprv F (eql t1 t2)
[PROOF STEP]
by (simp add: prv_eql_reflT prv_nprvI)