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


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


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

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

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

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

goal (1 subgoal):
 1. prv (imp (lcnj \<phi>s) \<phi>)
[PROOF STEP]
by (induct \<phi>s arbitrary: \<phi>)
      (auto simp : prv_imp_cnjL prv_cnj_imp_monoR2 prv_imp_triv)
[PROOF STATE]
proof (state)
this:
prv (imp (lcnj \<phi>s) \<phi>)

goal:
No subgoals!
[PROOF STEP]
qed


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

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


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

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


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

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

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

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

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

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

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

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

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

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

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


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

goal (1 subgoal):
 1. prv (imp (lcnj (remdups \<phi>s)) (lcnj \<phi>s))
[PROOF STEP]
apply(induct \<phi>s)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. set [] \<subseteq> fmla \<Longrightarrow> prv (imp (lcnj (remdups [])) (lcnj []))
 2. \<And>a \<phi>s. \<lbrakk>set \<phi>s \<subseteq> fmla \<Longrightarrow> prv (imp (lcnj (remdups \<phi>s)) (lcnj \<phi>s)); set (a # \<phi>s) \<subseteq> fmla\<rbrakk> \<Longrightarrow> prv (imp (lcnj (remdups (a # \<phi>s))) (lcnj (a # \<phi>s)))
[PROOF STEP]
by (auto simp: prv_imp_cnj prv_lcnj_imp_in prv_cnj_mono prv_imp_refl)


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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

goal (1 subgoal):
 1. prv (imp (cnj \<phi>1 (lcnj (\<phi>2ss1 @ \<phi>2ss2))) (lcnj (\<phi>2ss1 @ \<phi>1 # \<phi>2ss2)))
[PROOF STEP]
by (intro prv_lcnj_imp_inner) auto
[PROOF STATE]
proof (state)
this:
prv (imp (cnj \<phi>1 (lcnj \<phi>2s)) (lcnj \<phi>2ss))

goal (2 subgoals):
 1. \<phi>1 \<in> set \<phi>2ss \<Longrightarrow> prv (imp (lcnj (\<phi>1 # \<phi>1s)) (lcnj \<phi>2ss))
 2. \<phi>1 \<notin> set \<phi>2ss \<Longrightarrow> prv (imp (lcnj (\<phi>1 # \<phi>1s)) (lcnj \<phi>2ss))
[PROOF STEP]
have 1: "prv (imp (lcnj \<phi>1s) (lcnj \<phi>2s))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (imp (lcnj \<phi>1s) (lcnj \<phi>2s))
[PROOF STEP]
using nin Cons.prems True \<phi>2s \<phi>2ss
[PROOF STATE]
proof (prove)
using this:
\<phi>1 \<notin> set \<phi>2s
set (\<phi>1 # \<phi>1s) \<subseteq> fmla
set \<phi>2ss \<subseteq> set (\<phi>1 # \<phi>1s)
distinct \<phi>2ss
\<phi>1 \<in> set \<phi>2ss
\<phi>2s \<equiv> \<phi>2ss1 @ \<phi>2ss2
\<phi>2ss = \<phi>2ss1 @ \<phi>1 # \<phi>2ss2

goal (1 subgoal):
 1. prv (imp (lcnj \<phi>1s) (lcnj \<phi>2s))
[PROOF STEP]
by (intro Cons.IH) auto
[PROOF STATE]
proof (state)
this:
prv (imp (lcnj \<phi>1s) (lcnj \<phi>2s))

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

goal (1 subgoal):
 1. prv (imp (cnj \<phi>1 (lcnj \<phi>1s)) (cnj \<phi>1 (lcnj \<phi>2s)))
[PROOF STEP]
by (intro prv_cnj_mono) (fastforce simp add: prv_imp_refl)+
[PROOF STATE]
proof (state)
this:
prv (imp (cnj \<phi>1 (lcnj \<phi>1s)) (cnj \<phi>1 (lcnj \<phi>2s)))

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

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

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

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

goal (1 subgoal):
 1. prv (imp (lcnj (\<phi>1 # \<phi>1s)) (lcnj \<phi>2ss))
[PROOF STEP]
by (meson Cons lcnj prv_imp_lcnj prv_lcnj_imp_in subset_iff)
[PROOF STATE]
proof (state)
this:
prv (imp (lcnj (\<phi>1 # \<phi>1s)) (lcnj \<phi>2ss))

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

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

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

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

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

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

goal:
No subgoals!
[PROOF STEP]
qed


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

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


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

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

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


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

goal (1 subgoal):
 1. prv (eqv (subst (scnj F) t x) (scnj ((\<lambda>\<phi>. subst \<phi> t x) ` F)))
[PROOF STEP]
unfolding scnj_def
[PROOF STATE]
proof (prove)
using this:
F \<subseteq> fmla
finite F
t \<in> trm
x \<in> var

goal (1 subgoal):
 1. prv (eqv (subst (lcnj (asList F)) t x) (lcnj (asList ((\<lambda>\<phi>. subst \<phi> t x) ` F))))
[PROOF STEP]
by (fastforce intro!: prv_lcnj_eqv)


[STATEMENT]
lemma prv_imp_subst_scnj:
  assumes "F \<subseteq> fmla" "finite F" "t \<in> trm" "x \<in> var"
  shows "prv (imp (subst (scnj F) t x) (scnj ((\<lambda>\<phi>. subst \<phi> t x) ` F)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (imp (subst (scnj F) t x) (scnj ((\<lambda>\<phi>. subst \<phi> t x) ` F)))
[PROOF STEP]
using prv_subst_scnj[OF assms] assms
[PROOF STATE]
proof (prove)
using this:
prv (eqv (subst (scnj F) t x) (scnj ((\<lambda>\<phi>. subst \<phi> t x) ` F)))
F \<subseteq> fmla
finite F
t \<in> trm
x \<in> var

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


[STATEMENT]
lemma prv_subst_scnj_imp:
  assumes "F \<subseteq> fmla" "finite F" "t \<in> trm" "x \<in> var"
  shows "prv (imp (scnj ((\<lambda>\<phi>. subst \<phi> t x) ` F)) (subst (scnj F) t x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (imp (scnj ((\<lambda>\<phi>. subst \<phi> t x) ` F)) (subst (scnj F) t x))
[PROOF STEP]
using prv_subst_scnj[OF assms] assms
[PROOF STATE]
proof (prove)
using this:
prv (eqv (subst (scnj F) t x) (scnj ((\<lambda>\<phi>. subst \<phi> t x) ` F)))
F \<subseteq> fmla
finite F
t \<in> trm
x \<in> var

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


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

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


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

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


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

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


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

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


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

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


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

goal (1 subgoal):
 1. prv (imp (scnj (insert \<phi> F)) (cnj \<phi> (scnj F)))
[PROOF STEP]
apply (intro prv_imp_cnj)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<lbrakk>F \<subseteq> fmla; finite F; \<phi> \<in> fmla\<rbrakk> \<Longrightarrow> scnj (insert \<phi> F) \<in> fmla
 2. \<lbrakk>F \<subseteq> fmla; finite F; \<phi> \<in> fmla\<rbrakk> \<Longrightarrow> scnj F \<in> fmla
 3. \<lbrakk>F \<subseteq> fmla; finite F; \<phi> \<in> fmla\<rbrakk> \<Longrightarrow> \<phi> \<in> fmla
 4. \<lbrakk>F \<subseteq> fmla; finite F; \<phi> \<in> fmla\<rbrakk> \<Longrightarrow> prv (imp (scnj (insert \<phi> F)) \<phi>)
 5. \<lbrakk>F \<subseteq> fmla; finite F; \<phi> \<in> fmla\<rbrakk> \<Longrightarrow> prv (imp (scnj (insert \<phi> F)) (scnj F))
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>F \<subseteq> fmla; finite F; \<phi> \<in> fmla\<rbrakk> \<Longrightarrow> scnj (insert \<phi> F) \<in> fmla
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>F \<subseteq> fmla; finite F; \<phi> \<in> fmla\<rbrakk> \<Longrightarrow> scnj F \<in> fmla
 2. \<lbrakk>F \<subseteq> fmla; finite F; \<phi> \<in> fmla\<rbrakk> \<Longrightarrow> \<phi> \<in> fmla
 3. \<lbrakk>F \<subseteq> fmla; finite F; \<phi> \<in> fmla\<rbrakk> \<Longrightarrow> prv (imp (scnj (insert \<phi> F)) \<phi>)
 4. \<lbrakk>F \<subseteq> fmla; finite F; \<phi> \<in> fmla\<rbrakk> \<Longrightarrow> prv (imp (scnj (insert \<phi> F)) (scnj F))
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>F \<subseteq> fmla; finite F; \<phi> \<in> fmla\<rbrakk> \<Longrightarrow> scnj F \<in> fmla
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>F \<subseteq> fmla; finite F; \<phi> \<in> fmla\<rbrakk> \<Longrightarrow> \<phi> \<in> fmla
 2. \<lbrakk>F \<subseteq> fmla; finite F; \<phi> \<in> fmla\<rbrakk> \<Longrightarrow> prv (imp (scnj (insert \<phi> F)) \<phi>)
 3. \<lbrakk>F \<subseteq> fmla; finite F; \<phi> \<in> fmla\<rbrakk> \<Longrightarrow> prv (imp (scnj (insert \<phi> F)) (scnj F))
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>F \<subseteq> fmla; finite F; \<phi> \<in> fmla\<rbrakk> \<Longrightarrow> \<phi> \<in> fmla
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>F \<subseteq> fmla; finite F; \<phi> \<in> fmla\<rbrakk> \<Longrightarrow> prv (imp (scnj (insert \<phi> F)) \<phi>)
 2. \<lbrakk>F \<subseteq> fmla; finite F; \<phi> \<in> fmla\<rbrakk> \<Longrightarrow> prv (imp (scnj (insert \<phi> F)) (scnj F))
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>F \<subseteq> fmla; finite F; \<phi> \<in> fmla\<rbrakk> \<Longrightarrow> prv (imp (scnj (insert \<phi> F)) \<phi>)
[PROOF STEP]
by (auto intro: prv_imp_refl prv_scnj_imp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>F \<subseteq> fmla; finite F; \<phi> \<in> fmla\<rbrakk> \<Longrightarrow> prv (imp (scnj (insert \<phi> F)) (scnj F))
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>F \<subseteq> fmla; finite F; \<phi> \<in> fmla\<rbrakk> \<Longrightarrow> prv (imp (scnj (insert \<phi> F)) (scnj F))
[PROOF STEP]
by (auto intro: prv_scnj_mono)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
.


[STATEMENT]
lemma prv_implies_scnj_insert:
  assumes "F \<subseteq> fmla" and "finite F" and "\<phi> \<in> fmla"
    and "prv (scnj (insert \<phi> F))"
  shows "prv (cnj \<phi> (scnj F))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (cnj \<phi> (scnj F))
[PROOF STEP]
by (meson assms  cnj finite.insertI insert_subset prv_imp_mp prv_imp_scnj_insert scnj)


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

goal (1 subgoal):
 1. prv (imp (cnj \<phi> (scnj F)) (scnj (insert \<phi> F)))
[PROOF STEP]
by (auto intro!: prv_imp_scnj prv_imp_cnjL
      simp: prv_cnj_imp_monoR2 prv_imp_triv prv_scnj_imp_in subset_iff)


[STATEMENT]
lemma prv_implies_cnj_scnj:
  assumes "F \<subseteq> fmla" and "finite F" and "\<phi> \<in> fmla"
    and "prv (cnj \<phi> (scnj F))"
  shows "prv (scnj (insert \<phi> F))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (scnj (insert \<phi> F))
[PROOF STEP]
by (meson assms  cnj finite.insertI insert_subset prv_imp_cnj_scnj prv_imp_mp scnj)


[STATEMENT]
lemma prv_eqv_scnj_insert:
  assumes "F \<subseteq> fmla" and "finite F" and "\<phi> \<in> fmla"
  shows "prv (eqv (scnj (insert \<phi> F)) (cnj \<phi> (scnj F)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (eqv (scnj (insert \<phi> F)) (cnj \<phi> (scnj F)))
[PROOF STEP]
by (simp add: assms prv_eqvI prv_imp_cnj_scnj prv_imp_scnj_insert)


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

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


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

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


[STATEMENT]
lemma prv_scnj2_imp_cnj:
  "\<phi> \<in> fmla \<Longrightarrow> \<psi> \<in> fmla \<Longrightarrow> prv (imp (scnj {\<phi>,\<psi>}) (cnj \<phi> \<psi>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<phi> \<in> fmla; \<psi> \<in> fmla\<rbrakk> \<Longrightarrow> prv (imp (scnj {\<phi>, \<psi>}) (cnj \<phi> \<psi>))
[PROOF STEP]
using prv_imp_cnj prv_scnj_imp_in
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?\<phi> \<in> fmla; ?\<chi> \<in> fmla; ?\<psi> \<in> fmla; prv (imp ?\<phi> ?\<psi>); prv (imp ?\<phi> ?\<chi>)\<rbrakk> \<Longrightarrow> prv (imp ?\<phi> (cnj ?\<psi> ?\<chi>))
\<lbrakk>?F \<subseteq> fmla; finite ?F; ?\<phi> \<in> ?F\<rbrakk> \<Longrightarrow> prv (imp (scnj ?F) ?\<phi>)

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


[STATEMENT]
lemma prv_cnj_imp_scnj2:
  "\<phi> \<in> fmla \<Longrightarrow> \<psi> \<in> fmla \<Longrightarrow> prv (imp (cnj \<phi> \<psi>) (scnj {\<phi>,\<psi>}))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<phi> \<in> fmla; \<psi> \<in> fmla\<rbrakk> \<Longrightarrow> prv (imp (cnj \<phi> \<psi>) (scnj {\<phi>, \<psi>}))
[PROOF STEP]
using prv_imp_cnjL prv_imp_cnjR prv_imp_scnj
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?\<phi> \<in> fmla; ?\<chi> \<in> fmla\<rbrakk> \<Longrightarrow> prv (imp (cnj ?\<phi> ?\<chi>) ?\<phi>)
\<lbrakk>?\<phi> \<in> fmla; ?\<chi> \<in> fmla\<rbrakk> \<Longrightarrow> prv (imp (cnj ?\<phi> ?\<chi>) ?\<chi>)
\<lbrakk>?\<chi> \<in> fmla; ?F \<subseteq> fmla; finite ?F; \<And>\<phi>. \<phi> \<in> ?F \<Longrightarrow> prv (imp ?\<chi> \<phi>)\<rbrakk> \<Longrightarrow> prv (imp ?\<chi> (scnj ?F))

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


[STATEMENT]
lemma prv_imp_imp_scnj2:
  "\<phi> \<in> fmla \<Longrightarrow> \<psi> \<in> fmla \<Longrightarrow> prv (imp \<phi> (imp \<psi> (scnj {\<phi>,\<psi>})))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<phi> \<in> fmla; \<psi> \<in> fmla\<rbrakk> \<Longrightarrow> prv (imp \<phi> (imp \<psi> (scnj {\<phi>, \<psi>})))
[PROOF STEP]
using prv_cnj_imp_scnj2 prv_cnj_imp
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?\<phi> \<in> fmla; ?\<psi> \<in> fmla\<rbrakk> \<Longrightarrow> prv (imp (cnj ?\<phi> ?\<psi>) (scnj {?\<phi>, ?\<psi>}))
\<lbrakk>?\<phi> \<in> fmla; ?\<chi> \<in> fmla; ?\<psi> \<in> fmla; prv (imp (cnj ?\<phi> ?\<chi>) ?\<psi>)\<rbrakk> \<Longrightarrow> prv (imp ?\<phi> (imp ?\<chi> ?\<psi>))

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


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

goal (1 subgoal):
 1. prv (eqv (rawpsubst (scnj F) txs) (scnj ((\<lambda>\<phi>. rawpsubst \<phi> txs) ` F)))
[PROOF STEP]
proof(induction txs arbitrary: F)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>F. \<lbrakk>F \<subseteq> fmla; finite F; snd ` set [] \<subseteq> var; fst ` set [] \<subseteq> trm\<rbrakk> \<Longrightarrow> prv (eqv (rawpsubst (scnj F) []) (scnj ((\<lambda>\<phi>. rawpsubst \<phi> []) ` F)))
 2. \<And>a txs F. \<lbrakk>\<And>F. \<lbrakk>F \<subseteq> fmla; finite F; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm\<rbrakk> \<Longrightarrow> prv (eqv (rawpsubst (scnj F) txs) (scnj ((\<lambda>\<phi>. rawpsubst \<phi> txs) ` F))); F \<subseteq> fmla; finite F; snd ` set (a # txs) \<subseteq> var; fst ` set (a # txs) \<subseteq> trm\<rbrakk> \<Longrightarrow> prv (eqv (rawpsubst (scnj F) (a # txs)) (scnj ((\<lambda>\<phi>. rawpsubst \<phi> (a # txs)) ` F)))
[PROOF STEP]
case (Cons tx txs)
[PROOF STATE]
proof (state)
this:
\<lbrakk>?F \<subseteq> fmla; finite ?F; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm\<rbrakk> \<Longrightarrow> prv (eqv (rawpsubst (scnj ?F) txs) (scnj ((\<lambda>\<phi>. rawpsubst \<phi> txs) ` ?F)))
F \<subseteq> fmla
finite F
snd ` set (tx # txs) \<subseteq> var
fst ` set (tx # txs) \<subseteq> trm

goal (2 subgoals):
 1. \<And>F. \<lbrakk>F \<subseteq> fmla; finite F; snd ` set [] \<subseteq> var; fst ` set [] \<subseteq> trm\<rbrakk> \<Longrightarrow> prv (eqv (rawpsubst (scnj F) []) (scnj ((\<lambda>\<phi>. rawpsubst \<phi> []) ` F)))
 2. \<And>a txs F. \<lbrakk>\<And>F. \<lbrakk>F \<subseteq> fmla; finite F; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm\<rbrakk> \<Longrightarrow> prv (eqv (rawpsubst (scnj F) txs) (scnj ((\<lambda>\<phi>. rawpsubst \<phi> txs) ` F))); F \<subseteq> fmla; finite F; snd ` set (a # txs) \<subseteq> var; fst ` set (a # txs) \<subseteq> trm\<rbrakk> \<Longrightarrow> prv (eqv (rawpsubst (scnj F) (a # txs)) (scnj ((\<lambda>\<phi>. rawpsubst \<phi> (a # txs)) ` F)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>?F \<subseteq> fmla; finite ?F; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm\<rbrakk> \<Longrightarrow> prv (eqv (rawpsubst (scnj ?F) txs) (scnj ((\<lambda>\<phi>. rawpsubst \<phi> txs) ` ?F)))
F \<subseteq> fmla
finite F
snd ` set (tx # txs) \<subseteq> var
fst ` set (tx # txs) \<subseteq> trm
[PROOF STEP]
obtain t x where tx[simp]: "tx = (t,x)"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?F \<subseteq> fmla; finite ?F; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm\<rbrakk> \<Longrightarrow> prv (eqv (rawpsubst (scnj ?F) txs) (scnj ((\<lambda>\<phi>. rawpsubst \<phi> txs) ` ?F)))
F \<subseteq> fmla
finite F
snd ` set (tx # txs) \<subseteq> var
fst ` set (tx # txs) \<subseteq> trm

goal (1 subgoal):
 1. (\<And>t x. tx = (t, x) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases tx) auto
[PROOF STATE]
proof (state)
this:
tx = (t, x)

goal (2 subgoals):
 1. \<And>F. \<lbrakk>F \<subseteq> fmla; finite F; snd ` set [] \<subseteq> var; fst ` set [] \<subseteq> trm\<rbrakk> \<Longrightarrow> prv (eqv (rawpsubst (scnj F) []) (scnj ((\<lambda>\<phi>. rawpsubst \<phi> []) ` F)))
 2. \<And>a txs F. \<lbrakk>\<And>F. \<lbrakk>F \<subseteq> fmla; finite F; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm\<rbrakk> \<Longrightarrow> prv (eqv (rawpsubst (scnj F) txs) (scnj ((\<lambda>\<phi>. rawpsubst \<phi> txs) ` F))); F \<subseteq> fmla; finite F; snd ` set (a # txs) \<subseteq> var; fst ` set (a # txs) \<subseteq> trm\<rbrakk> \<Longrightarrow> prv (eqv (rawpsubst (scnj F) (a # txs)) (scnj ((\<lambda>\<phi>. rawpsubst \<phi> (a # txs)) ` F)))
[PROOF STEP]
hence [simp]: "t \<in> trm" "x \<in> var"
[PROOF STATE]
proof (prove)
using this:
tx = (t, x)

goal (1 subgoal):
 1. t \<in> trm &&& x \<in> var
[PROOF STEP]
using Cons.prems
[PROOF STATE]
proof (prove)
using this:
tx = (t, x)
F \<subseteq> fmla
finite F
snd ` set (tx # txs) \<subseteq> var
fst ` set (tx # txs) \<subseteq> trm

goal (1 subgoal):
 1. t \<in> trm &&& x \<in> var
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
t \<in> trm
x \<in> var

goal (2 subgoals):
 1. \<And>F. \<lbrakk>F \<subseteq> fmla; finite F; snd ` set [] \<subseteq> var; fst ` set [] \<subseteq> trm\<rbrakk> \<Longrightarrow> prv (eqv (rawpsubst (scnj F) []) (scnj ((\<lambda>\<phi>. rawpsubst \<phi> []) ` F)))
 2. \<And>a txs F. \<lbrakk>\<And>F. \<lbrakk>F \<subseteq> fmla; finite F; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm\<rbrakk> \<Longrightarrow> prv (eqv (rawpsubst (scnj F) txs) (scnj ((\<lambda>\<phi>. rawpsubst \<phi> txs) ` F))); F \<subseteq> fmla; finite F; snd ` set (a # txs) \<subseteq> var; fst ` set (a # txs) \<subseteq> trm\<rbrakk> \<Longrightarrow> prv (eqv (rawpsubst (scnj F) (a # txs)) (scnj ((\<lambda>\<phi>. rawpsubst \<phi> (a # txs)) ` F)))
[PROOF STEP]
have 0: "(\<lambda>\<phi>. rawpsubst (subst \<phi> t x) txs) ` F =
           (\<lambda>\<phi>. rawpsubst \<phi> txs) ` ((\<lambda>\<phi>. subst \<phi> t x) ` F)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>\<phi>. rawpsubst (subst \<phi> t x) txs) ` F = (\<lambda>\<phi>. rawpsubst \<phi> txs) ` (\<lambda>\<phi>. subst \<phi> t x) ` F
[PROOF STEP]
using Cons.prems
[PROOF STATE]
proof (prove)
using this:
F \<subseteq> fmla
finite F
snd ` set (tx # txs) \<subseteq> var
fst ` set (tx # txs) \<subseteq> trm

goal (1 subgoal):
 1. (\<lambda>\<phi>. rawpsubst (subst \<phi> t x) txs) ` F = (\<lambda>\<phi>. rawpsubst \<phi> txs) ` (\<lambda>\<phi>. subst \<phi> t x) ` F
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<lambda>\<phi>. rawpsubst (subst \<phi> t x) txs) ` F = (\<lambda>\<phi>. rawpsubst \<phi> txs) ` (\<lambda>\<phi>. subst \<phi> t x) ` F

goal (2 subgoals):
 1. \<And>F. \<lbrakk>F \<subseteq> fmla; finite F; snd ` set [] \<subseteq> var; fst ` set [] \<subseteq> trm\<rbrakk> \<Longrightarrow> prv (eqv (rawpsubst (scnj F) []) (scnj ((\<lambda>\<phi>. rawpsubst \<phi> []) ` F)))
 2. \<And>a txs F. \<lbrakk>\<And>F. \<lbrakk>F \<subseteq> fmla; finite F; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm\<rbrakk> \<Longrightarrow> prv (eqv (rawpsubst (scnj F) txs) (scnj ((\<lambda>\<phi>. rawpsubst \<phi> txs) ` F))); F \<subseteq> fmla; finite F; snd ` set (a # txs) \<subseteq> var; fst ` set (a # txs) \<subseteq> trm\<rbrakk> \<Longrightarrow> prv (eqv (rawpsubst (scnj F) (a # txs)) (scnj ((\<lambda>\<phi>. rawpsubst \<phi> (a # txs)) ` F)))
[PROOF STEP]
have "prv (eqv (subst (scnj F) t x)
                 (scnj ((\<lambda>\<phi>. subst \<phi> t x) ` F)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (eqv (subst (scnj F) t x) (scnj ((\<lambda>\<phi>. subst \<phi> t x) ` F)))
[PROOF STEP]
using Cons.prems
[PROOF STATE]
proof (prove)
using this:
F \<subseteq> fmla
finite F
snd ` set (tx # txs) \<subseteq> var
fst ` set (tx # txs) \<subseteq> trm

goal (1 subgoal):
 1. prv (eqv (subst (scnj F) t x) (scnj ((\<lambda>\<phi>. subst \<phi> t x) ` F)))
[PROOF STEP]
by (intro prv_subst_scnj) auto
[PROOF STATE]
proof (state)
this:
prv (eqv (subst (scnj F) t x) (scnj ((\<lambda>\<phi>. subst \<phi> t x) ` F)))

goal (2 subgoals):
 1. \<And>F. \<lbrakk>F \<subseteq> fmla; finite F; snd ` set [] \<subseteq> var; fst ` set [] \<subseteq> trm\<rbrakk> \<Longrightarrow> prv (eqv (rawpsubst (scnj F) []) (scnj ((\<lambda>\<phi>. rawpsubst \<phi> []) ` F)))
 2. \<And>a txs F. \<lbrakk>\<And>F. \<lbrakk>F \<subseteq> fmla; finite F; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm\<rbrakk> \<Longrightarrow> prv (eqv (rawpsubst (scnj F) txs) (scnj ((\<lambda>\<phi>. rawpsubst \<phi> txs) ` F))); F \<subseteq> fmla; finite F; snd ` set (a # txs) \<subseteq> var; fst ` set (a # txs) \<subseteq> trm\<rbrakk> \<Longrightarrow> prv (eqv (rawpsubst (scnj F) (a # txs)) (scnj ((\<lambda>\<phi>. rawpsubst \<phi> (a # txs)) ` F)))
[PROOF STEP]
hence "prv (eqv (rawpsubst (subst (scnj F) t x) txs)
                  (rawpsubst (scnj ((\<lambda>\<phi>. subst \<phi> t x) ` F)) txs))"
[PROOF STATE]
proof (prove)
using this:
prv (eqv (subst (scnj F) t x) (scnj ((\<lambda>\<phi>. subst \<phi> t x) ` F)))

goal (1 subgoal):
 1. prv (eqv (rawpsubst (subst (scnj F) t x) txs) (rawpsubst (scnj ((\<lambda>\<phi>. subst \<phi> t x) ` F)) txs))
[PROOF STEP]
using Cons.prems
[PROOF STATE]
proof (prove)
using this:
prv (eqv (subst (scnj F) t x) (scnj ((\<lambda>\<phi>. subst \<phi> t x) ` F)))
F \<subseteq> fmla
finite F
snd ` set (tx # txs) \<subseteq> var
fst ` set (tx # txs) \<subseteq> trm

goal (1 subgoal):
 1. prv (eqv (rawpsubst (subst (scnj F) t x) txs) (rawpsubst (scnj ((\<lambda>\<phi>. subst \<phi> t x) ` F)) txs))
[PROOF STEP]
by (intro prv_eqv_rawpsubst) auto
[PROOF STATE]
proof (state)
this:
prv (eqv (rawpsubst (subst (scnj F) t x) txs) (rawpsubst (scnj ((\<lambda>\<phi>. subst \<phi> t x) ` F)) txs))

goal (2 subgoals):
 1. \<And>F. \<lbrakk>F \<subseteq> fmla; finite F; snd ` set [] \<subseteq> var; fst ` set [] \<subseteq> trm\<rbrakk> \<Longrightarrow> prv (eqv (rawpsubst (scnj F) []) (scnj ((\<lambda>\<phi>. rawpsubst \<phi> []) ` F)))
 2. \<And>a txs F. \<lbrakk>\<And>F. \<lbrakk>F \<subseteq> fmla; finite F; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm\<rbrakk> \<Longrightarrow> prv (eqv (rawpsubst (scnj F) txs) (scnj ((\<lambda>\<phi>. rawpsubst \<phi> txs) ` F))); F \<subseteq> fmla; finite F; snd ` set (a # txs) \<subseteq> var; fst ` set (a # txs) \<subseteq> trm\<rbrakk> \<Longrightarrow> prv (eqv (rawpsubst (scnj F) (a # txs)) (scnj ((\<lambda>\<phi>. rawpsubst \<phi> (a # txs)) ` F)))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
prv (eqv (rawpsubst (subst (scnj F) t x) txs) (rawpsubst (scnj ((\<lambda>\<phi>. subst \<phi> t x) ` F)) txs))

goal (2 subgoals):
 1. \<And>F. \<lbrakk>F \<subseteq> fmla; finite F; snd ` set [] \<subseteq> var; fst ` set [] \<subseteq> trm\<rbrakk> \<Longrightarrow> prv (eqv (rawpsubst (scnj F) []) (scnj ((\<lambda>\<phi>. rawpsubst \<phi> []) ` F)))
 2. \<And>a txs F. \<lbrakk>\<And>F. \<lbrakk>F \<subseteq> fmla; finite F; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm\<rbrakk> \<Longrightarrow> prv (eqv (rawpsubst (scnj F) txs) (scnj ((\<lambda>\<phi>. rawpsubst \<phi> txs) ` F))); F \<subseteq> fmla; finite F; snd ` set (a # txs) \<subseteq> var; fst ` set (a # txs) \<subseteq> trm\<rbrakk> \<Longrightarrow> prv (eqv (rawpsubst (scnj F) (a # txs)) (scnj ((\<lambda>\<phi>. rawpsubst \<phi> (a # txs)) ` F)))
[PROOF STEP]
have "prv (eqv (rawpsubst (scnj ((\<lambda>\<phi>. subst \<phi> t x) ` F)) txs)
                 (scnj ((\<lambda>\<phi>. rawpsubst (subst \<phi> t x) txs) ` F)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (eqv (rawpsubst (scnj ((\<lambda>\<phi>. subst \<phi> t x) ` F)) txs) (scnj ((\<lambda>\<phi>. rawpsubst (subst \<phi> t x) txs) ` F)))
[PROOF STEP]
unfolding 0
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (eqv (rawpsubst (scnj ((\<lambda>\<phi>. subst \<phi> t x) ` F)) txs) (scnj ((\<lambda>\<phi>. rawpsubst \<phi> txs) ` (\<lambda>\<phi>. subst \<phi> t x) ` F)))
[PROOF STEP]
using Cons.prems
[PROOF STATE]
proof (prove)
using this:
F \<subseteq> fmla
finite F
snd ` set (tx # txs) \<subseteq> var
fst ` set (tx # txs) \<subseteq> trm

goal (1 subgoal):
 1. prv (eqv (rawpsubst (scnj ((\<lambda>\<phi>. subst \<phi> t x) ` F)) txs) (scnj ((\<lambda>\<phi>. rawpsubst \<phi> txs) ` (\<lambda>\<phi>. subst \<phi> t x) ` F)))
[PROOF STEP]
by (intro Cons.IH) auto
[PROOF STATE]
proof (state)
this:
prv (eqv (rawpsubst (scnj ((\<lambda>\<phi>. subst \<phi> t x) ` F)) txs) (scnj ((\<lambda>\<phi>. rawpsubst (subst \<phi> t x) txs) ` F)))

goal (2 subgoals):
 1. \<And>F. \<lbrakk>F \<subseteq> fmla; finite F; snd ` set [] \<subseteq> var; fst ` set [] \<subseteq> trm\<rbrakk> \<Longrightarrow> prv (eqv (rawpsubst (scnj F) []) (scnj ((\<lambda>\<phi>. rawpsubst \<phi> []) ` F)))
 2. \<And>a txs F. \<lbrakk>\<And>F. \<lbrakk>F \<subseteq> fmla; finite F; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm\<rbrakk> \<Longrightarrow> prv (eqv (rawpsubst (scnj F) txs) (scnj ((\<lambda>\<phi>. rawpsubst \<phi> txs) ` F))); F \<subseteq> fmla; finite F; snd ` set (a # txs) \<subseteq> var; fst ` set (a # txs) \<subseteq> trm\<rbrakk> \<Longrightarrow> prv (eqv (rawpsubst (scnj F) (a # txs)) (scnj ((\<lambda>\<phi>. rawpsubst \<phi> (a # txs)) ` F)))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
prv (eqv (rawpsubst (subst (scnj F) t x) txs) (rawpsubst (scnj ((\<lambda>\<phi>. subst \<phi> t x) ` F)) txs))
prv (eqv (rawpsubst (scnj ((\<lambda>\<phi>. subst \<phi> t x) ` F)) txs) (scnj ((\<lambda>\<phi>. rawpsubst (subst \<phi> t x) txs) ` F)))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
prv (eqv (rawpsubst (subst (scnj F) t x) txs) (rawpsubst (scnj ((\<lambda>\<phi>. subst \<phi> t x) ` F)) txs))
prv (eqv (rawpsubst (scnj ((\<lambda>\<phi>. subst \<phi> t x) ` F)) txs) (scnj ((\<lambda>\<phi>. rawpsubst (subst \<phi> t x) txs) ` F)))

goal (1 subgoal):
 1. prv (eqv (rawpsubst (scnj F) (tx # txs)) (scnj ((\<lambda>\<phi>. rawpsubst \<phi> (tx # txs)) ` F)))
[PROOF STEP]
using Cons.prems
[PROOF STATE]
proof (prove)
using this:
prv (eqv (rawpsubst (subst (scnj F) t x) txs) (rawpsubst (scnj ((\<lambda>\<phi>. subst \<phi> t x) ` F)) txs))
prv (eqv (rawpsubst (scnj ((\<lambda>\<phi>. subst \<phi> t x) ` F)) txs) (scnj ((\<lambda>\<phi>. rawpsubst (subst \<phi> t x) txs) ` F)))
F \<subseteq> fmla
finite F
snd ` set (tx # txs) \<subseteq> var
fst ` set (tx # txs) \<subseteq> trm

goal (1 subgoal):
 1. prv (eqv (rawpsubst (scnj F) (tx # txs)) (scnj ((\<lambda>\<phi>. rawpsubst \<phi> (tx # txs)) ` F)))
[PROOF STEP]
apply -
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>prv (eqv (rawpsubst (subst (scnj F) t x) txs) (rawpsubst (scnj ((\<lambda>\<phi>. subst \<phi> t x) ` F)) txs)); prv (eqv (rawpsubst (scnj ((\<lambda>\<phi>. subst \<phi> t x) ` F)) txs) (scnj ((\<lambda>\<phi>. rawpsubst (subst \<phi> t x) txs) ` F))); F \<subseteq> fmla; finite F; snd ` set (tx # txs) \<subseteq> var; fst ` set (tx # txs) \<subseteq> trm\<rbrakk> \<Longrightarrow> prv (eqv (rawpsubst (scnj F) (tx # txs)) (scnj ((\<lambda>\<phi>. rawpsubst \<phi> (tx # txs)) ` F)))
[PROOF STEP]
by (rule prv_eqv_trans) (auto intro!: rawpsubst)
[PROOF STATE]
proof (state)
this:
prv (eqv (rawpsubst (scnj F) (tx # txs)) (scnj ((\<lambda>\<phi>. rawpsubst \<phi> (tx # txs)) ` F)))

goal (1 subgoal):
 1. \<And>F. \<lbrakk>F \<subseteq> fmla; finite F; snd ` set [] \<subseteq> var; fst ` set [] \<subseteq> trm\<rbrakk> \<Longrightarrow> prv (eqv (rawpsubst (scnj F) []) (scnj ((\<lambda>\<phi>. rawpsubst \<phi> []) ` F)))
[PROOF STEP]
qed(auto simp: image_def prv_eqv_refl)[]