[STATEMENT]
lemma prv_imp_triv:
assumes phi: "\<phi> \<in> fmla" and psi: "\<psi> \<in> fmla"
shows "prv \<psi> \<Longrightarrow> prv (imp \<phi> \<psi>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv \<psi> \<Longrightarrow> prv (imp \<phi> \<psi>)
[PROOF STEP]
by (meson prv_imp_imp_triv prv_imp_mp imp phi psi)


[STATEMENT]
lemma prv_imp_refl:
assumes phi: "\<phi> \<in> fmla"
shows "prv (imp \<phi> \<phi>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (imp \<phi> \<phi>)
[PROOF STEP]
by (metis prv_imp_imp_triv prv_imp_mp prv_imp_trans imp phi)


[STATEMENT]
lemma prv_imp_refl2: "\<phi> \<in> fmla \<Longrightarrow> \<psi> \<in> fmla \<Longrightarrow> \<phi> = \<psi> \<Longrightarrow> prv (imp \<phi> \<psi>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<phi> \<in> fmla; \<psi> \<in> fmla; \<phi> = \<psi>\<rbrakk> \<Longrightarrow> prv (imp \<phi> \<psi>)
[PROOF STEP]
using prv_imp_refl
[PROOF STATE]
proof (prove)
using this:
?\<phi> \<in> fmla \<Longrightarrow> prv (imp ?\<phi> ?\<phi>)

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


[STATEMENT]
lemma prv_cnjI:
assumes phi: "\<phi> \<in> fmla" and chi: "\<chi> \<in> fmla"
shows "prv \<phi> \<Longrightarrow> prv \<chi> \<Longrightarrow> prv (cnj \<phi> \<chi>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>prv \<phi>; prv \<chi>\<rbrakk> \<Longrightarrow> prv (cnj \<phi> \<chi>)
[PROOF STEP]
by (meson cnj prv_imp_cnjI prv_imp_mp imp phi chi)


[STATEMENT]
lemma prv_cnjEL:
assumes phi: "\<phi> \<in> fmla" and chi: "\<chi> \<in> fmla"
shows "prv (cnj \<phi> \<chi>) \<Longrightarrow> prv \<phi>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (cnj \<phi> \<chi>) \<Longrightarrow> prv \<phi>
[PROOF STEP]
using chi phi prv_imp_cnjL prv_imp_mp
[PROOF STATE]
proof (prove)
using this:
\<chi> \<in> fmla
\<phi> \<in> fmla
\<lbrakk>?\<phi> \<in> fmla; ?\<chi> \<in> fmla\<rbrakk> \<Longrightarrow> prv (imp (cnj ?\<phi> ?\<chi>) ?\<phi>)
\<lbrakk>?\<phi> \<in> fmla; ?\<chi> \<in> fmla; prv (imp ?\<phi> ?\<chi>); prv ?\<phi>\<rbrakk> \<Longrightarrow> prv ?\<chi>

goal (1 subgoal):
 1. prv (cnj \<phi> \<chi>) \<Longrightarrow> prv \<phi>
[PROOF STEP]
by blast


[STATEMENT]
lemma prv_cnjER:
assumes phi: "\<phi> \<in> fmla" and chi: "\<chi> \<in> fmla"
shows "prv (cnj \<phi> \<chi>) \<Longrightarrow> prv \<chi>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (cnj \<phi> \<chi>) \<Longrightarrow> prv \<chi>
[PROOF STEP]
using chi phi prv_imp_cnjR prv_imp_mp
[PROOF STATE]
proof (prove)
using this:
\<chi> \<in> fmla
\<phi> \<in> fmla
\<lbrakk>?\<phi> \<in> fmla; ?\<chi> \<in> fmla\<rbrakk> \<Longrightarrow> prv (imp (cnj ?\<phi> ?\<chi>) ?\<chi>)
\<lbrakk>?\<phi> \<in> fmla; ?\<chi> \<in> fmla; prv (imp ?\<phi> ?\<chi>); prv ?\<phi>\<rbrakk> \<Longrightarrow> prv ?\<chi>

goal (1 subgoal):
 1. prv (cnj \<phi> \<chi>) \<Longrightarrow> prv \<chi>
[PROOF STEP]
by blast


[STATEMENT]
lemma prv_prv_imp_trans:
assumes phi: "\<phi> \<in> fmla" and chi: "\<chi> \<in> fmla" and psi: "\<psi> \<in> fmla"
assumes 1: "prv (imp \<phi> \<chi>)" and 2: "prv (imp \<chi> \<psi>)"
shows "prv (imp \<phi> \<psi>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (imp \<phi> \<psi>)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. prv (imp \<phi> \<psi>)
[PROOF STEP]
have "prv (imp \<phi> (imp \<chi> \<psi>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (imp \<phi> (imp \<chi> \<psi>))
[PROOF STEP]
by (simp add: 2 chi prv_imp_triv phi psi)
[PROOF STATE]
proof (state)
this:
prv (imp \<phi> (imp \<chi> \<psi>))

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

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma prv_imp_trans1:
assumes phi: "\<phi> \<in> fmla" and chi: "\<chi> \<in> fmla" and psi: "\<psi> \<in> fmla"
shows "prv (imp (imp \<chi> \<psi>) (imp (imp \<phi> \<chi>) (imp \<phi> \<psi>)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (imp (imp \<chi> \<psi>) (imp (imp \<phi> \<chi>) (imp \<phi> \<psi>)))
[PROOF STEP]
by (meson chi prv_prv_imp_trans prv_imp_imp_triv prv_imp_trans imp phi psi)


[STATEMENT]
lemma prv_imp_com:
assumes phi: "\<phi> \<in> fmla" and chi: "\<chi> \<in> fmla" and psi: "\<psi> \<in> fmla"
assumes "prv (imp \<phi> (imp \<chi> \<psi>))"
shows "prv (imp \<chi> (imp \<phi> \<psi>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (imp \<chi> (imp \<phi> \<psi>))
[PROOF STEP]
by (metis (no_types) assms prv_prv_imp_trans prv_imp_imp_triv prv_imp_mp prv_imp_trans imp)


[STATEMENT]
lemma prv_imp_trans2:
assumes phi: "\<phi> \<in> fmla" and chi: "\<chi> \<in> fmla" and psi: "\<psi> \<in> fmla"
shows "prv (imp (imp \<phi> \<chi>) (imp (imp \<chi> \<psi>) (imp \<phi> \<psi>)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (imp (imp \<phi> \<chi>) (imp (imp \<chi> \<psi>) (imp \<phi> \<psi>)))
[PROOF STEP]
using prv_imp_mp prv_imp_trans prv_imp_trans1 prv_imp_imp_triv
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?\<phi> \<in> fmla; ?\<chi> \<in> fmla; prv (imp ?\<phi> ?\<chi>); prv ?\<phi>\<rbrakk> \<Longrightarrow> prv ?\<chi>
\<lbrakk>?\<phi> \<in> fmla; ?\<chi> \<in> fmla; ?\<psi> \<in> fmla\<rbrakk> \<Longrightarrow> prv (imp (imp ?\<phi> (imp ?\<chi> ?\<psi>)) (imp (imp ?\<phi> ?\<chi>) (imp ?\<phi> ?\<psi>)))
\<lbrakk>?\<phi> \<in> fmla; ?\<chi> \<in> fmla; ?\<psi> \<in> fmla\<rbrakk> \<Longrightarrow> prv (imp (imp ?\<chi> ?\<psi>) (imp (imp ?\<phi> ?\<chi>) (imp ?\<phi> ?\<psi>)))
\<lbrakk>?\<phi> \<in> fmla; ?\<chi> \<in> fmla\<rbrakk> \<Longrightarrow> prv (imp ?\<phi> (imp ?\<chi> ?\<phi>))

goal (1 subgoal):
 1. prv (imp (imp \<phi> \<chi>) (imp (imp \<chi> \<psi>) (imp \<phi> \<psi>)))
[PROOF STEP]
by (meson chi prv_imp_com imp phi psi)


[STATEMENT]
lemma prv_imp_cnj:
assumes "\<phi> \<in> fmla" and "\<chi> \<in> fmla" and "\<psi> \<in> fmla"
shows "prv (imp \<phi> \<psi>) \<Longrightarrow> prv (imp \<phi> \<chi>) \<Longrightarrow> prv (imp \<phi> (cnj \<psi> \<chi>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>prv (imp \<phi> \<psi>); prv (imp \<phi> \<chi>)\<rbrakk> \<Longrightarrow> prv (imp \<phi> (cnj \<psi> \<chi>))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>prv (imp \<phi> \<psi>); prv (imp \<phi> \<chi>)\<rbrakk> \<Longrightarrow> prv (imp \<phi> (cnj \<psi> \<chi>))
[PROOF STEP]
assume "prv (imp \<phi> \<psi>)"
[PROOF STATE]
proof (state)
this:
prv (imp \<phi> \<psi>)

goal (1 subgoal):
 1. \<lbrakk>prv (imp \<phi> \<psi>); prv (imp \<phi> \<chi>)\<rbrakk> \<Longrightarrow> prv (imp \<phi> (cnj \<psi> \<chi>))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
prv (imp \<phi> \<psi>)

goal (1 subgoal):
 1. \<lbrakk>prv (imp \<phi> \<psi>); prv (imp \<phi> \<chi>)\<rbrakk> \<Longrightarrow> prv (imp \<phi> (cnj \<psi> \<chi>))
[PROOF STEP]
assume "prv (imp \<phi> \<chi>)"
[PROOF STATE]
proof (state)
this:
prv (imp \<phi> \<chi>)

goal (1 subgoal):
 1. \<lbrakk>prv (imp \<phi> \<psi>); prv (imp \<phi> \<chi>)\<rbrakk> \<Longrightarrow> prv (imp \<phi> (cnj \<psi> \<chi>))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
prv (imp \<phi> \<chi>)
[PROOF STEP]
have "prv (imp \<phi> (imp \<psi> f))" if "prv (imp \<chi> f)" "f \<in> fmla" for f
[PROOF STATE]
proof (prove)
using this:
prv (imp \<phi> \<chi>)

goal (1 subgoal):
 1. prv (imp \<phi> (imp \<psi> f))
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
prv (imp \<phi> \<chi>)
prv (imp \<chi> f)
f \<in> fmla

goal (1 subgoal):
 1. prv (imp \<phi> (imp \<psi> f))
[PROOF STEP]
by (metis (no_types) assms imp prv_imp_imp_triv prv_prv_imp_trans)
[PROOF STATE]
proof (state)
this:
\<lbrakk>prv (imp \<chi> ?f); ?f \<in> fmla\<rbrakk> \<Longrightarrow> prv (imp \<phi> (imp \<psi> ?f))

goal (1 subgoal):
 1. \<lbrakk>prv (imp \<phi> \<psi>); prv (imp \<phi> \<chi>)\<rbrakk> \<Longrightarrow> prv (imp \<phi> (cnj \<psi> \<chi>))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<lbrakk>prv (imp \<chi> ?f); ?f \<in> fmla\<rbrakk> \<Longrightarrow> prv (imp \<phi> (imp \<psi> ?f))

goal (1 subgoal):
 1. \<lbrakk>prv (imp \<phi> \<psi>); prv (imp \<phi> \<chi>)\<rbrakk> \<Longrightarrow> prv (imp \<phi> (cnj \<psi> \<chi>))
[PROOF STEP]
have "prv (imp \<phi> (imp \<psi> \<psi>)) \<Longrightarrow> prv (imp \<phi> (imp \<phi> \<psi>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (imp \<phi> (imp \<psi> \<psi>)) \<Longrightarrow> prv (imp \<phi> (imp \<phi> \<psi>))
[PROOF STEP]
using \<open>prv (imp \<phi> \<psi>)\<close>
[PROOF STATE]
proof (prove)
using this:
prv (imp \<phi> \<psi>)

goal (1 subgoal):
 1. prv (imp \<phi> (imp \<psi> \<psi>)) \<Longrightarrow> prv (imp \<phi> (imp \<phi> \<psi>))
[PROOF STEP]
by (metis (no_types) assms(1,3) imp prv_imp_com prv_prv_imp_trans)
[PROOF STATE]
proof (state)
this:
prv (imp \<phi> (imp \<psi> \<psi>)) \<Longrightarrow> prv (imp \<phi> (imp \<phi> \<psi>))

goal (1 subgoal):
 1. \<lbrakk>prv (imp \<phi> \<psi>); prv (imp \<phi> \<chi>)\<rbrakk> \<Longrightarrow> prv (imp \<phi> (cnj \<psi> \<chi>))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
prv (imp \<phi> \<psi>)
\<lbrakk>prv (imp \<chi> ?f); ?f \<in> fmla\<rbrakk> \<Longrightarrow> prv (imp \<phi> (imp \<psi> ?f))
prv (imp \<phi> (imp \<psi> \<psi>)) \<Longrightarrow> prv (imp \<phi> (imp \<phi> \<psi>))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
prv (imp \<phi> \<psi>)
\<lbrakk>prv (imp \<chi> ?f); ?f \<in> fmla\<rbrakk> \<Longrightarrow> prv (imp \<phi> (imp \<psi> ?f))
prv (imp \<phi> (imp \<psi> \<psi>)) \<Longrightarrow> prv (imp \<phi> (imp \<phi> \<psi>))

goal (1 subgoal):
 1. prv (imp \<phi> (cnj \<psi> \<chi>))
[PROOF STEP]
by (metis (no_types) assms cnj imp prv_imp_cnjI prv_imp_com prv_imp_mp prv_imp_trans)
[PROOF STATE]
proof (state)
this:
prv (imp \<phi> (cnj \<psi> \<chi>))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma prv_imp_imp_com:
assumes "\<phi> \<in> fmla" and "\<chi> \<in> fmla" and "\<psi> \<in> fmla"
shows
"prv (imp (imp \<phi> (imp \<chi> \<psi>))
          (imp \<chi> (imp \<phi> \<psi>)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (imp (imp \<phi> (imp \<chi> \<psi>)) (imp \<chi> (imp \<phi> \<psi>)))
[PROOF STEP]
by (metis (no_types) assms
   prv_prv_imp_trans prv_imp_com prv_imp_imp_triv prv_imp_trans imp)


[STATEMENT]
lemma prv_cnj_imp_monoR2:
assumes "\<phi> \<in> fmla" and "\<chi> \<in> fmla" and "\<psi> \<in> fmla"
assumes "prv (imp \<phi> (imp \<chi> \<psi>))"
shows "prv (imp (cnj \<phi> \<chi>) \<psi>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (imp (cnj \<phi> \<chi>) \<psi>)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. prv (imp (cnj \<phi> \<chi>) \<psi>)
[PROOF STEP]
have "prv (imp (cnj \<phi> \<chi>) (cnj \<phi> \<chi>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (imp (cnj \<phi> \<chi>) (cnj \<phi> \<chi>))
[PROOF STEP]
using prv_imp_refl
[PROOF STATE]
proof (prove)
using this:
?\<phi> \<in> fmla \<Longrightarrow> prv (imp ?\<phi> ?\<phi>)

goal (1 subgoal):
 1. prv (imp (cnj \<phi> \<chi>) (cnj \<phi> \<chi>))
[PROOF STEP]
by (blast intro: assms(1-3))
[PROOF STATE]
proof (state)
this:
prv (imp (cnj \<phi> \<chi>) (cnj \<phi> \<chi>))

goal (1 subgoal):
 1. prv (imp (cnj \<phi> \<chi>) \<psi>)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
prv (imp (cnj \<phi> \<chi>) (cnj \<phi> \<chi>))
[PROOF STEP]
have "prv (imp (imp (cnj \<phi> \<chi>) (imp (cnj \<phi> \<chi>) \<psi>)) (imp (cnj \<phi> \<chi>) \<psi>))"
[PROOF STATE]
proof (prove)
using this:
prv (imp (cnj \<phi> \<chi>) (cnj \<phi> \<chi>))

goal (1 subgoal):
 1. prv (imp (imp (cnj \<phi> \<chi>) (imp (cnj \<phi> \<chi>) \<psi>)) (imp (cnj \<phi> \<chi>) \<psi>))
[PROOF STEP]
by (metis (no_types) cnj imp assms(1-3) prv_imp_com prv_imp_mp prv_imp_trans)
[PROOF STATE]
proof (state)
this:
prv (imp (imp (cnj \<phi> \<chi>) (imp (cnj \<phi> \<chi>) \<psi>)) (imp (cnj \<phi> \<chi>) \<psi>))

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

goal (1 subgoal):
 1. prv (imp (cnj \<phi> \<chi>) \<psi>)
[PROOF STEP]
by (metis (no_types) imp cnj assms prv_imp_cnjL prv_imp_cnjR prv_imp_com prv_imp_mp prv_prv_imp_trans)
[PROOF STATE]
proof (state)
this:
prv (imp (cnj \<phi> \<chi>) \<psi>)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma prv_imp_imp_imp_cnj:
assumes "\<phi> \<in> fmla" and "\<chi> \<in> fmla" and "\<psi> \<in> fmla"
shows
"prv (imp (imp \<phi> (imp \<chi> \<psi>))
          (imp (cnj \<phi> \<chi>) \<psi>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (imp (imp \<phi> (imp \<chi> \<psi>)) (imp (cnj \<phi> \<chi>) \<psi>))
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. prv (imp (imp \<phi> (imp \<chi> \<psi>)) (imp (cnj \<phi> \<chi>) \<psi>))
[PROOF STEP]
have "prv (imp \<phi> (imp (imp \<phi> (imp \<chi> \<psi>)) (imp \<chi> \<psi>)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (imp \<phi> (imp (imp \<phi> (imp \<chi> \<psi>)) (imp \<chi> \<psi>)))
[PROOF STEP]
by (simp add: assms prv_imp_com prv_imp_refl)
[PROOF STATE]
proof (state)
this:
prv (imp \<phi> (imp (imp \<phi> (imp \<chi> \<psi>)) (imp \<chi> \<psi>)))

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

goal (1 subgoal):
 1. prv (imp \<phi> (imp \<chi> (imp (imp \<phi> (imp \<chi> \<psi>)) \<psi>)))
[PROOF STEP]
by (metis (no_types, lifting) assms prv_prv_imp_trans prv_imp_imp_com imp)
[PROOF STATE]
proof (state)
this:
prv (imp \<phi> (imp \<chi> (imp (imp \<phi> (imp \<chi> \<psi>)) \<psi>)))

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

goal (1 subgoal):
 1. prv (imp (cnj \<phi> \<chi>) (imp (imp \<phi> (imp \<chi> \<psi>)) \<psi>))
[PROOF STEP]
by (simp add: assms prv_cnj_imp_monoR2)
[PROOF STATE]
proof (state)
this:
prv (imp (cnj \<phi> \<chi>) (imp (imp \<phi> (imp \<chi> \<psi>)) \<psi>))

goal (1 subgoal):
 1. prv (imp (imp \<phi> (imp \<chi> \<psi>)) (imp (cnj \<phi> \<chi>) \<psi>))
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
prv (imp (cnj \<phi> \<chi>) (imp (imp \<phi> (imp \<chi> \<psi>)) \<psi>))

goal (1 subgoal):
 1. prv (imp (imp \<phi> (imp \<chi> \<psi>)) (imp (cnj \<phi> \<chi>) \<psi>))
[PROOF STEP]
using assms prv_imp_com prv_imp_mp
[PROOF STATE]
proof (prove)
using this:
prv (imp (cnj \<phi> \<chi>) (imp (imp \<phi> (imp \<chi> \<psi>)) \<psi>))
\<phi> \<in> fmla
\<chi> \<in> fmla
\<psi> \<in> fmla
\<lbrakk>?\<phi> \<in> fmla; ?\<chi> \<in> fmla; ?\<psi> \<in> fmla; prv (imp ?\<phi> (imp ?\<chi> ?\<psi>))\<rbrakk> \<Longrightarrow> prv (imp ?\<chi> (imp ?\<phi> ?\<psi>))
\<lbrakk>?\<phi> \<in> fmla; ?\<chi> \<in> fmla; prv (imp ?\<phi> ?\<chi>); prv ?\<phi>\<rbrakk> \<Longrightarrow> prv ?\<chi>

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma prv_imp_cnj_imp:
assumes "\<phi> \<in> fmla" and "\<chi> \<in> fmla" and "\<psi> \<in> fmla"
shows
"prv (imp (imp (cnj \<phi> \<chi>) \<psi>)
          (imp \<phi> (imp \<chi> \<psi>)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (imp (imp (cnj \<phi> \<chi>) \<psi>) (imp \<phi> (imp \<chi> \<psi>)))
[PROOF STEP]
by (metis (no_types) assms cnj prv_prv_imp_trans prv_imp_cnjI prv_imp_com prv_imp_trans2 imp)


[STATEMENT]
lemma prv_cnj_imp:
assumes "\<phi> \<in> fmla" and "\<chi> \<in> fmla" and "\<psi> \<in> fmla"
assumes "prv (imp (cnj \<phi> \<chi>) \<psi>)"
shows "prv (imp \<phi> (imp \<chi> \<psi>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (imp \<phi> (imp \<chi> \<psi>))
[PROOF STEP]
using assms prv_imp_cnj_imp prv_imp_mp
[PROOF STATE]
proof (prove)
using this:
\<phi> \<in> fmla
\<chi> \<in> fmla
\<psi> \<in> fmla
prv (imp (cnj \<phi> \<chi>) \<psi>)
\<lbrakk>?\<phi> \<in> fmla; ?\<chi> \<in> fmla; ?\<psi> \<in> fmla\<rbrakk> \<Longrightarrow> prv (imp (imp (cnj ?\<phi> ?\<chi>) ?\<psi>) (imp ?\<phi> (imp ?\<chi> ?\<psi>)))
\<lbrakk>?\<phi> \<in> fmla; ?\<chi> \<in> fmla; prv (imp ?\<phi> ?\<chi>); prv ?\<phi>\<rbrakk> \<Longrightarrow> prv ?\<chi>

goal (1 subgoal):
 1. prv (imp \<phi> (imp \<chi> \<psi>))
[PROOF STEP]
by (meson cnj imp)


[STATEMENT]
lemma prv_cnj_imp_monoR:
assumes "\<phi> \<in> fmla" and "\<chi> \<in> fmla" and "\<psi> \<in> fmla"
shows "prv (imp (imp \<phi> \<chi>) (imp (imp \<phi> \<psi>) (imp \<phi> (cnj \<chi> \<psi>))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (imp (imp \<phi> \<chi>) (imp (imp \<phi> \<psi>) (imp \<phi> (cnj \<chi> \<psi>))))
[PROOF STEP]
by (meson assms cnj imp prv_cnj_imp prv_cnj_imp_monoR2 prv_imp_cnj prv_imp_cnjL prv_imp_cnjR)


[STATEMENT]
lemma prv_imp_cnj3L:
assumes "\<phi>1 \<in> fmla" and "\<phi>2 \<in> fmla" and "\<chi> \<in> fmla"
shows "prv (imp (imp \<phi>1 \<chi>) (imp (cnj \<phi>1 \<phi>2) \<chi>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (imp (imp \<phi>1 \<chi>) (imp (cnj \<phi>1 \<phi>2) \<chi>))
[PROOF STEP]
using assms prv_imp_cnjL prv_imp_mp prv_imp_trans2
[PROOF STATE]
proof (prove)
using this:
\<phi>1 \<in> fmla
\<phi>2 \<in> fmla
\<chi> \<in> fmla
\<lbrakk>?\<phi> \<in> fmla; ?\<chi> \<in> fmla\<rbrakk> \<Longrightarrow> prv (imp (cnj ?\<phi> ?\<chi>) ?\<phi>)
\<lbrakk>?\<phi> \<in> fmla; ?\<chi> \<in> fmla; prv (imp ?\<phi> ?\<chi>); prv ?\<phi>\<rbrakk> \<Longrightarrow> prv ?\<chi>
\<lbrakk>?\<phi> \<in> fmla; ?\<chi> \<in> fmla; ?\<psi> \<in> fmla\<rbrakk> \<Longrightarrow> prv (imp (imp ?\<phi> ?\<chi>) (imp (imp ?\<chi> ?\<psi>) (imp ?\<phi> ?\<psi>)))

goal (1 subgoal):
 1. prv (imp (imp \<phi>1 \<chi>) (imp (cnj \<phi>1 \<phi>2) \<chi>))
[PROOF STEP]
by (metis cnj imp)


[STATEMENT]
lemma prv_imp_cnj3R:
assumes "\<phi>1 \<in> fmla" and "\<phi>2 \<in> fmla" and "\<chi> \<in> fmla"
shows "prv (imp (imp \<phi>2 \<chi>) (imp (cnj \<phi>1 \<phi>2) \<chi>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (imp (imp \<phi>2 \<chi>) (imp (cnj \<phi>1 \<phi>2) \<chi>))
[PROOF STEP]
using prv_imp_cnjR prv_imp_mp prv_imp_trans2
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?\<phi> \<in> fmla; ?\<chi> \<in> fmla\<rbrakk> \<Longrightarrow> prv (imp (cnj ?\<phi> ?\<chi>) ?\<chi>)
\<lbrakk>?\<phi> \<in> fmla; ?\<chi> \<in> fmla; prv (imp ?\<phi> ?\<chi>); prv ?\<phi>\<rbrakk> \<Longrightarrow> prv ?\<chi>
\<lbrakk>?\<phi> \<in> fmla; ?\<chi> \<in> fmla; ?\<psi> \<in> fmla\<rbrakk> \<Longrightarrow> prv (imp (imp ?\<phi> ?\<chi>) (imp (imp ?\<chi> ?\<psi>) (imp ?\<phi> ?\<psi>)))

goal (1 subgoal):
 1. prv (imp (imp \<phi>2 \<chi>) (imp (cnj \<phi>1 \<phi>2) \<chi>))
[PROOF STEP]
by (metis assms cnj imp)


[STATEMENT]
lemma prv_cnj_imp_mono:
assumes "\<phi>1 \<in> fmla" and "\<phi>2 \<in> fmla" and "\<chi>1 \<in> fmla" and "\<chi>2 \<in> fmla"
shows "prv (imp (imp \<phi>1 \<chi>1) (imp (imp \<phi>2 \<chi>2) (imp (cnj \<phi>1 \<phi>2) (cnj \<chi>1 \<chi>2))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (imp (imp \<phi>1 \<chi>1) (imp (imp \<phi>2 \<chi>2) (imp (cnj \<phi>1 \<phi>2) (cnj \<chi>1 \<chi>2))))
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. prv (imp (imp \<phi>1 \<chi>1) (imp (imp \<phi>2 \<chi>2) (imp (cnj \<phi>1 \<phi>2) (cnj \<chi>1 \<chi>2))))
[PROOF STEP]
have "prv (imp (imp (cnj \<phi>1 \<phi>2) \<chi>1) (imp (imp (cnj \<phi>1 \<phi>2) \<chi>2) (imp (cnj \<phi>1 \<phi>2) (cnj \<chi>1 \<chi>2))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (imp (imp (cnj \<phi>1 \<phi>2) \<chi>1) (imp (imp (cnj \<phi>1 \<phi>2) \<chi>2) (imp (cnj \<phi>1 \<phi>2) (cnj \<chi>1 \<chi>2))))
[PROOF STEP]
using prv_cnj_imp_monoR[of "cnj \<phi>1 \<phi>2" \<chi>1 \<chi>2] assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>cnj \<phi>1 \<phi>2 \<in> fmla; \<chi>1 \<in> fmla; \<chi>2 \<in> fmla\<rbrakk> \<Longrightarrow> prv (imp (imp (cnj \<phi>1 \<phi>2) \<chi>1) (imp (imp (cnj \<phi>1 \<phi>2) \<chi>2) (imp (cnj \<phi>1 \<phi>2) (cnj \<chi>1 \<chi>2))))
\<phi>1 \<in> fmla
\<phi>2 \<in> fmla
\<chi>1 \<in> fmla
\<chi>2 \<in> fmla

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

goal (1 subgoal):
 1. prv (imp (imp \<phi>1 \<chi>1) (imp (imp \<phi>2 \<chi>2) (imp (cnj \<phi>1 \<phi>2) (cnj \<chi>1 \<chi>2))))
[PROOF STEP]
hence "prv (imp (imp \<phi>1 \<chi>1) (imp (imp (cnj \<phi>1 \<phi>2) \<chi>2) (imp (cnj \<phi>1 \<phi>2) (cnj \<chi>1 \<chi>2))))"
[PROOF STATE]
proof (prove)
using this:
prv (imp (imp (cnj \<phi>1 \<phi>2) \<chi>1) (imp (imp (cnj \<phi>1 \<phi>2) \<chi>2) (imp (cnj \<phi>1 \<phi>2) (cnj \<chi>1 \<chi>2))))

goal (1 subgoal):
 1. prv (imp (imp \<phi>1 \<chi>1) (imp (imp (cnj \<phi>1 \<phi>2) \<chi>2) (imp (cnj \<phi>1 \<phi>2) (cnj \<chi>1 \<chi>2))))
[PROOF STEP]
by (metis (no_types) imp cnj assms prv_imp_cnj3L prv_prv_imp_trans)
[PROOF STATE]
proof (state)
this:
prv (imp (imp \<phi>1 \<chi>1) (imp (imp (cnj \<phi>1 \<phi>2) \<chi>2) (imp (cnj \<phi>1 \<phi>2) (cnj \<chi>1 \<chi>2))))

goal (1 subgoal):
 1. prv (imp (imp \<phi>1 \<chi>1) (imp (imp \<phi>2 \<chi>2) (imp (cnj \<phi>1 \<phi>2) (cnj \<chi>1 \<chi>2))))
[PROOF STEP]
hence "prv (imp (imp (cnj \<phi>1 \<phi>2) \<chi>2) (imp (imp \<phi>1 \<chi>1) (imp (cnj \<phi>1 \<phi>2) (cnj \<chi>1 \<chi>2))))"
[PROOF STATE]
proof (prove)
using this:
prv (imp (imp \<phi>1 \<chi>1) (imp (imp (cnj \<phi>1 \<phi>2) \<chi>2) (imp (cnj \<phi>1 \<phi>2) (cnj \<chi>1 \<chi>2))))

goal (1 subgoal):
 1. prv (imp (imp (cnj \<phi>1 \<phi>2) \<chi>2) (imp (imp \<phi>1 \<chi>1) (imp (cnj \<phi>1 \<phi>2) (cnj \<chi>1 \<chi>2))))
[PROOF STEP]
using prv_imp_com assms
[PROOF STATE]
proof (prove)
using this:
prv (imp (imp \<phi>1 \<chi>1) (imp (imp (cnj \<phi>1 \<phi>2) \<chi>2) (imp (cnj \<phi>1 \<phi>2) (cnj \<chi>1 \<chi>2))))
\<lbrakk>?\<phi> \<in> fmla; ?\<chi> \<in> fmla; ?\<psi> \<in> fmla; prv (imp ?\<phi> (imp ?\<chi> ?\<psi>))\<rbrakk> \<Longrightarrow> prv (imp ?\<chi> (imp ?\<phi> ?\<psi>))
\<phi>1 \<in> fmla
\<phi>2 \<in> fmla
\<chi>1 \<in> fmla
\<chi>2 \<in> fmla

goal (1 subgoal):
 1. prv (imp (imp (cnj \<phi>1 \<phi>2) \<chi>2) (imp (imp \<phi>1 \<chi>1) (imp (cnj \<phi>1 \<phi>2) (cnj \<chi>1 \<chi>2))))
[PROOF STEP]
by (meson cnj imp)
[PROOF STATE]
proof (state)
this:
prv (imp (imp (cnj \<phi>1 \<phi>2) \<chi>2) (imp (imp \<phi>1 \<chi>1) (imp (cnj \<phi>1 \<phi>2) (cnj \<chi>1 \<chi>2))))

goal (1 subgoal):
 1. prv (imp (imp \<phi>1 \<chi>1) (imp (imp \<phi>2 \<chi>2) (imp (cnj \<phi>1 \<phi>2) (cnj \<chi>1 \<chi>2))))
[PROOF STEP]
hence "prv (imp (imp \<phi>2 \<chi>2) (imp (imp \<phi>1 \<chi>1) (imp (cnj \<phi>1 \<phi>2) (cnj \<chi>1 \<chi>2))))"
[PROOF STATE]
proof (prove)
using this:
prv (imp (imp (cnj \<phi>1 \<phi>2) \<chi>2) (imp (imp \<phi>1 \<chi>1) (imp (cnj \<phi>1 \<phi>2) (cnj \<chi>1 \<chi>2))))

goal (1 subgoal):
 1. prv (imp (imp \<phi>2 \<chi>2) (imp (imp \<phi>1 \<chi>1) (imp (cnj \<phi>1 \<phi>2) (cnj \<chi>1 \<chi>2))))
[PROOF STEP]
using prv_imp_cnj3R prv_imp_mp prv_imp_trans1
[PROOF STATE]
proof (prove)
using this:
prv (imp (imp (cnj \<phi>1 \<phi>2) \<chi>2) (imp (imp \<phi>1 \<chi>1) (imp (cnj \<phi>1 \<phi>2) (cnj \<chi>1 \<chi>2))))
\<lbrakk>?\<phi>1.0 \<in> fmla; ?\<phi>2.0 \<in> fmla; ?\<chi> \<in> fmla\<rbrakk> \<Longrightarrow> prv (imp (imp ?\<phi>2.0 ?\<chi>) (imp (cnj ?\<phi>1.0 ?\<phi>2.0) ?\<chi>))
\<lbrakk>?\<phi> \<in> fmla; ?\<chi> \<in> fmla; prv (imp ?\<phi> ?\<chi>); prv ?\<phi>\<rbrakk> \<Longrightarrow> prv ?\<chi>
\<lbrakk>?\<phi> \<in> fmla; ?\<chi> \<in> fmla; ?\<psi> \<in> fmla\<rbrakk> \<Longrightarrow> prv (imp (imp ?\<chi> ?\<psi>) (imp (imp ?\<phi> ?\<chi>) (imp ?\<phi> ?\<psi>)))

goal (1 subgoal):
 1. prv (imp (imp \<phi>2 \<chi>2) (imp (imp \<phi>1 \<chi>1) (imp (cnj \<phi>1 \<phi>2) (cnj \<chi>1 \<chi>2))))
[PROOF STEP]
by (metis (no_types) assms cnj prv_prv_imp_trans imp)
[PROOF STATE]
proof (state)
this:
prv (imp (imp \<phi>2 \<chi>2) (imp (imp \<phi>1 \<chi>1) (imp (cnj \<phi>1 \<phi>2) (cnj \<chi>1 \<chi>2))))

goal (1 subgoal):
 1. prv (imp (imp \<phi>1 \<chi>1) (imp (imp \<phi>2 \<chi>2) (imp (cnj \<phi>1 \<phi>2) (cnj \<chi>1 \<chi>2))))
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
prv (imp (imp \<phi>2 \<chi>2) (imp (imp \<phi>1 \<chi>1) (imp (cnj \<phi>1 \<phi>2) (cnj \<chi>1 \<chi>2))))

goal (1 subgoal):
 1. prv (imp (imp \<phi>1 \<chi>1) (imp (imp \<phi>2 \<chi>2) (imp (cnj \<phi>1 \<phi>2) (cnj \<chi>1 \<chi>2))))
[PROOF STEP]
using prv_imp_com assms
[PROOF STATE]
proof (prove)
using this:
prv (imp (imp \<phi>2 \<chi>2) (imp (imp \<phi>1 \<chi>1) (imp (cnj \<phi>1 \<phi>2) (cnj \<chi>1 \<chi>2))))
\<lbrakk>?\<phi> \<in> fmla; ?\<chi> \<in> fmla; ?\<psi> \<in> fmla; prv (imp ?\<phi> (imp ?\<chi> ?\<psi>))\<rbrakk> \<Longrightarrow> prv (imp ?\<chi> (imp ?\<phi> ?\<psi>))
\<phi>1 \<in> fmla
\<phi>2 \<in> fmla
\<chi>1 \<in> fmla
\<chi>2 \<in> fmla

goal (1 subgoal):
 1. prv (imp (imp \<phi>1 \<chi>1) (imp (imp \<phi>2 \<chi>2) (imp (cnj \<phi>1 \<phi>2) (cnj \<chi>1 \<chi>2))))
[PROOF STEP]
by (meson cnj imp)
[PROOF STATE]
proof (state)
this:
prv (imp (imp \<phi>1 \<chi>1) (imp (imp \<phi>2 \<chi>2) (imp (cnj \<phi>1 \<phi>2) (cnj \<chi>1 \<chi>2))))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma prv_cnj_mono:
assumes "\<phi>1 \<in> fmla" and "\<phi>2 \<in> fmla" and "\<chi>1 \<in> fmla" and "\<chi>2 \<in> fmla"
assumes "prv (imp \<phi>1 \<chi>1)" and "prv (imp \<phi>2 \<chi>2)"
shows "prv (imp (cnj \<phi>1 \<phi>2) (cnj \<chi>1 \<chi>2))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (imp (cnj \<phi>1 \<phi>2) (cnj \<chi>1 \<chi>2))
[PROOF STEP]
using assms prv_cnj_imp_mono prv_imp_mp
[PROOF STATE]
proof (prove)
using this:
\<phi>1 \<in> fmla
\<phi>2 \<in> fmla
\<chi>1 \<in> fmla
\<chi>2 \<in> fmla
prv (imp \<phi>1 \<chi>1)
prv (imp \<phi>2 \<chi>2)
\<lbrakk>?\<phi>1.0 \<in> fmla; ?\<phi>2.0 \<in> fmla; ?\<chi>1.0 \<in> fmla; ?\<chi>2.0 \<in> fmla\<rbrakk> \<Longrightarrow> prv (imp (imp ?\<phi>1.0 ?\<chi>1.0) (imp (imp ?\<phi>2.0 ?\<chi>2.0) (imp (cnj ?\<phi>1.0 ?\<phi>2.0) (cnj ?\<chi>1.0 ?\<chi>2.0))))
\<lbrakk>?\<phi> \<in> fmla; ?\<chi> \<in> fmla; prv (imp ?\<phi> ?\<chi>); prv ?\<phi>\<rbrakk> \<Longrightarrow> prv ?\<chi>

goal (1 subgoal):
 1. prv (imp (cnj \<phi>1 \<phi>2) (cnj \<chi>1 \<chi>2))
[PROOF STEP]
by (metis (mono_tags) cnj prv_prv_imp_trans prv_imp_cnj prv_imp_cnjL prv_imp_cnjR)


[STATEMENT]
lemma prv_cnj_imp_monoR4:
assumes "\<phi> \<in> fmla" and "\<chi> \<in> fmla" and "\<psi>1 \<in> fmla" and "\<psi>2 \<in> fmla"
shows
"prv (imp (imp \<phi> (imp \<chi> \<psi>1))
          (imp (imp \<phi> (imp \<chi> \<psi>2)) (imp \<phi> (imp \<chi> (cnj \<psi>1 \<psi>2)))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (imp (imp \<phi> (imp \<chi> \<psi>1)) (imp (imp \<phi> (imp \<chi> \<psi>2)) (imp \<phi> (imp \<chi> (cnj \<psi>1 \<psi>2)))))
[PROOF STEP]
by (simp add: assms prv_cnj_imp prv_imp_cnj prv_imp_cnjL prv_imp_cnjR prv_cnj_imp_monoR2)


[STATEMENT]
lemma prv_imp_cnj4:
assumes "\<phi> \<in> fmla" and "\<chi> \<in> fmla" and "\<psi>1 \<in> fmla" and "\<psi>2 \<in> fmla"
shows "prv (imp \<phi> (imp \<chi> \<psi>1)) \<Longrightarrow> prv (imp \<phi> (imp \<chi> \<psi>2)) \<Longrightarrow> prv (imp \<phi> (imp \<chi> (cnj \<psi>1 \<psi>2)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>prv (imp \<phi> (imp \<chi> \<psi>1)); prv (imp \<phi> (imp \<chi> \<psi>2))\<rbrakk> \<Longrightarrow> prv (imp \<phi> (imp \<chi> (cnj \<psi>1 \<psi>2)))
[PROOF STEP]
by (simp add: assms prv_cnj_imp prv_imp_cnj prv_cnj_imp_monoR2)


[STATEMENT]
lemma prv_cnj_imp_monoR5:
assumes "\<phi>1 \<in> fmla" and "\<phi>2 \<in> fmla" and "\<chi>1 \<in> fmla" and "\<chi>2 \<in> fmla"
shows "prv (imp (imp \<phi>1 \<chi>1) (imp (imp \<phi>2 \<chi>2) (imp \<phi>1 (imp \<phi>2 (cnj \<chi>1 \<chi>2)))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (imp (imp \<phi>1 \<chi>1) (imp (imp \<phi>2 \<chi>2) (imp \<phi>1 (imp \<phi>2 (cnj \<chi>1 \<chi>2)))))
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. prv (imp (imp \<phi>1 \<chi>1) (imp (imp \<phi>2 \<chi>2) (imp \<phi>1 (imp \<phi>2 (cnj \<chi>1 \<chi>2)))))
[PROOF STEP]
have "prv (imp (imp \<phi>1 \<chi>1) (imp (imp \<phi>2 \<chi>2) (imp (cnj \<phi>1 \<phi>2) (cnj \<chi>1 \<chi>2))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (imp (imp \<phi>1 \<chi>1) (imp (imp \<phi>2 \<chi>2) (imp (cnj \<phi>1 \<phi>2) (cnj \<chi>1 \<chi>2))))
[PROOF STEP]
using prv_cnj_imp_mono[of \<phi>1 \<phi>2  \<chi>1 \<chi>2] assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<phi>1 \<in> fmla; \<phi>2 \<in> fmla; \<chi>1 \<in> fmla; \<chi>2 \<in> fmla\<rbrakk> \<Longrightarrow> prv (imp (imp \<phi>1 \<chi>1) (imp (imp \<phi>2 \<chi>2) (imp (cnj \<phi>1 \<phi>2) (cnj \<chi>1 \<chi>2))))
\<phi>1 \<in> fmla
\<phi>2 \<in> fmla
\<chi>1 \<in> fmla
\<chi>2 \<in> fmla

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

goal (1 subgoal):
 1. prv (imp (imp \<phi>1 \<chi>1) (imp (imp \<phi>2 \<chi>2) (imp \<phi>1 (imp \<phi>2 (cnj \<chi>1 \<chi>2)))))
[PROOF STEP]
hence "prv (imp (imp \<phi>1 \<chi>1) (imp (cnj \<phi>1 \<phi>2) (imp (imp \<phi>2 \<chi>2) (cnj \<chi>1 \<chi>2))))"
[PROOF STATE]
proof (prove)
using this:
prv (imp (imp \<phi>1 \<chi>1) (imp (imp \<phi>2 \<chi>2) (imp (cnj \<phi>1 \<phi>2) (cnj \<chi>1 \<chi>2))))

goal (1 subgoal):
 1. prv (imp (imp \<phi>1 \<chi>1) (imp (cnj \<phi>1 \<phi>2) (imp (imp \<phi>2 \<chi>2) (cnj \<chi>1 \<chi>2))))
[PROOF STEP]
by (metis (no_types, lifting) assms cnj imp prv_imp_imp_com prv_prv_imp_trans)
[PROOF STATE]
proof (state)
this:
prv (imp (imp \<phi>1 \<chi>1) (imp (cnj \<phi>1 \<phi>2) (imp (imp \<phi>2 \<chi>2) (cnj \<chi>1 \<chi>2))))

goal (1 subgoal):
 1. prv (imp (imp \<phi>1 \<chi>1) (imp (imp \<phi>2 \<chi>2) (imp \<phi>1 (imp \<phi>2 (cnj \<chi>1 \<chi>2)))))
[PROOF STEP]
hence "prv (imp (imp \<phi>1 \<chi>1) (imp \<phi>1 (imp \<phi>2 (imp (imp \<phi>2 \<chi>2) (cnj \<chi>1 \<chi>2)))))"
[PROOF STATE]
proof (prove)
using this:
prv (imp (imp \<phi>1 \<chi>1) (imp (cnj \<phi>1 \<phi>2) (imp (imp \<phi>2 \<chi>2) (cnj \<chi>1 \<chi>2))))

goal (1 subgoal):
 1. prv (imp (imp \<phi>1 \<chi>1) (imp \<phi>1 (imp \<phi>2 (imp (imp \<phi>2 \<chi>2) (cnj \<chi>1 \<chi>2)))))
[PROOF STEP]
using prv_imp_cnj_imp prv_imp_mp prv_imp_trans2
[PROOF STATE]
proof (prove)
using this:
prv (imp (imp \<phi>1 \<chi>1) (imp (cnj \<phi>1 \<phi>2) (imp (imp \<phi>2 \<chi>2) (cnj \<chi>1 \<chi>2))))
\<lbrakk>?\<phi> \<in> fmla; ?\<chi> \<in> fmla; ?\<psi> \<in> fmla\<rbrakk> \<Longrightarrow> prv (imp (imp (cnj ?\<phi> ?\<chi>) ?\<psi>) (imp ?\<phi> (imp ?\<chi> ?\<psi>)))
\<lbrakk>?\<phi> \<in> fmla; ?\<chi> \<in> fmla; prv (imp ?\<phi> ?\<chi>); prv ?\<phi>\<rbrakk> \<Longrightarrow> prv ?\<chi>
\<lbrakk>?\<phi> \<in> fmla; ?\<chi> \<in> fmla; ?\<psi> \<in> fmla\<rbrakk> \<Longrightarrow> prv (imp (imp ?\<phi> ?\<chi>) (imp (imp ?\<chi> ?\<psi>) (imp ?\<phi> ?\<psi>)))

goal (1 subgoal):
 1. prv (imp (imp \<phi>1 \<chi>1) (imp \<phi>1 (imp \<phi>2 (imp (imp \<phi>2 \<chi>2) (cnj \<chi>1 \<chi>2)))))
[PROOF STEP]
by (metis (mono_tags) assms cnj prv_prv_imp_trans imp)
[PROOF STATE]
proof (state)
this:
prv (imp (imp \<phi>1 \<chi>1) (imp \<phi>1 (imp \<phi>2 (imp (imp \<phi>2 \<chi>2) (cnj \<chi>1 \<chi>2)))))

goal (1 subgoal):
 1. prv (imp (imp \<phi>1 \<chi>1) (imp (imp \<phi>2 \<chi>2) (imp \<phi>1 (imp \<phi>2 (cnj \<chi>1 \<chi>2)))))
[PROOF STEP]
hence 1: "prv (imp (imp \<phi>1 \<chi>1) (imp \<phi>1 (imp (imp \<phi>2 \<chi>2) (imp \<phi>2  (cnj \<chi>1 \<chi>2)))))"
[PROOF STATE]
proof (prove)
using this:
prv (imp (imp \<phi>1 \<chi>1) (imp \<phi>1 (imp \<phi>2 (imp (imp \<phi>2 \<chi>2) (cnj \<chi>1 \<chi>2)))))

goal (1 subgoal):
 1. prv (imp (imp \<phi>1 \<chi>1) (imp \<phi>1 (imp (imp \<phi>2 \<chi>2) (imp \<phi>2 (cnj \<chi>1 \<chi>2)))))
[PROOF STEP]
using prv_cnj_imp prv_imp_cnjR prv_imp_mp prv_imp_trans1
[PROOF STATE]
proof (prove)
using this:
prv (imp (imp \<phi>1 \<chi>1) (imp \<phi>1 (imp \<phi>2 (imp (imp \<phi>2 \<chi>2) (cnj \<chi>1 \<chi>2)))))
\<lbrakk>?\<phi> \<in> fmla; ?\<chi> \<in> fmla; ?\<psi> \<in> fmla; prv (imp (cnj ?\<phi> ?\<chi>) ?\<psi>)\<rbrakk> \<Longrightarrow> prv (imp ?\<phi> (imp ?\<chi> ?\<psi>))
\<lbrakk>?\<phi> \<in> fmla; ?\<chi> \<in> fmla\<rbrakk> \<Longrightarrow> prv (imp (cnj ?\<phi> ?\<chi>) ?\<chi>)
\<lbrakk>?\<phi> \<in> fmla; ?\<chi> \<in> fmla; prv (imp ?\<phi> ?\<chi>); prv ?\<phi>\<rbrakk> \<Longrightarrow> prv ?\<chi>
\<lbrakk>?\<phi> \<in> fmla; ?\<chi> \<in> fmla; ?\<psi> \<in> fmla\<rbrakk> \<Longrightarrow> prv (imp (imp ?\<chi> ?\<psi>) (imp (imp ?\<phi> ?\<chi>) (imp ?\<phi> ?\<psi>)))

goal (1 subgoal):
 1. prv (imp (imp \<phi>1 \<chi>1) (imp \<phi>1 (imp (imp \<phi>2 \<chi>2) (imp \<phi>2 (cnj \<chi>1 \<chi>2)))))
[PROOF STEP]
by (metis (no_types) assms cnj prv_cnj_imp_monoR prv_prv_imp_trans prv_imp_imp_triv imp)
[PROOF STATE]
proof (state)
this:
prv (imp (imp \<phi>1 \<chi>1) (imp \<phi>1 (imp (imp \<phi>2 \<chi>2) (imp \<phi>2 (cnj \<chi>1 \<chi>2)))))

goal (1 subgoal):
 1. prv (imp (imp \<phi>1 \<chi>1) (imp (imp \<phi>2 \<chi>2) (imp \<phi>1 (imp \<phi>2 (cnj \<chi>1 \<chi>2)))))
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
prv (imp (imp \<phi>1 \<chi>1) (imp \<phi>1 (imp (imp \<phi>2 \<chi>2) (imp \<phi>2 (cnj \<chi>1 \<chi>2)))))

goal (1 subgoal):
 1. prv (imp (imp \<phi>1 \<chi>1) (imp (imp \<phi>2 \<chi>2) (imp \<phi>1 (imp \<phi>2 (cnj \<chi>1 \<chi>2)))))
[PROOF STEP]
by (metis (no_types, lifting) assms cnj imp prv_prv_imp_trans prv_imp_imp_com)
[PROOF STATE]
proof (state)
this:
prv (imp (imp \<phi>1 \<chi>1) (imp (imp \<phi>2 \<chi>2) (imp \<phi>1 (imp \<phi>2 (cnj \<chi>1 \<chi>2)))))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma prv_imp_cnj5:
assumes "\<phi>1 \<in> fmla" and "\<phi>2 \<in> fmla" and "\<chi>1 \<in> fmla" and "\<chi>2 \<in> fmla"
assumes "prv (imp \<phi>1 \<chi>1)" and "prv (imp \<phi>2 \<chi>2)"
shows "prv (imp \<phi>1 (imp \<phi>2 (cnj \<chi>1 \<chi>2)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (imp \<phi>1 (imp \<phi>2 (cnj \<chi>1 \<chi>2)))
[PROOF STEP]
by (simp add: assms prv_cnj_imp prv_cnj_mono)


[STATEMENT]
lemma prv_eqv_imp:
assumes "\<phi> \<in> fmla" and "\<chi> \<in> fmla"
shows "prv (imp (eqv \<phi> \<chi>) (eqv \<chi> \<phi>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (imp (eqv \<phi> \<chi>) (eqv \<chi> \<phi>))
[PROOF STEP]
by (simp add: assms prv_imp_cnj prv_imp_cnjL prv_imp_cnjR eqv_def)


[STATEMENT]
lemma prv_eqv_eqv:
assumes "\<phi> \<in> fmla" and "\<chi> \<in> fmla"
shows "prv (eqv (eqv \<phi> \<chi>) (eqv \<chi> \<phi>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (eqv (eqv \<phi> \<chi>) (eqv \<chi> \<phi>))
[PROOF STEP]
using assms prv_cnjI prv_eqv_imp eqv_def
[PROOF STATE]
proof (prove)
using this:
\<phi> \<in> fmla
\<chi> \<in> fmla
\<lbrakk>?\<phi> \<in> fmla; ?\<chi> \<in> fmla; prv ?\<phi>; prv ?\<chi>\<rbrakk> \<Longrightarrow> prv (cnj ?\<phi> ?\<chi>)
\<lbrakk>?\<phi> \<in> fmla; ?\<chi> \<in> fmla\<rbrakk> \<Longrightarrow> prv (imp (eqv ?\<phi> ?\<chi>) (eqv ?\<chi> ?\<phi>))
eqv ?\<phi> ?\<chi> = cnj (imp ?\<phi> ?\<chi>) (imp ?\<chi> ?\<phi>)

goal (1 subgoal):
 1. prv (eqv (eqv \<phi> \<chi>) (eqv \<chi> \<phi>))
[PROOF STEP]
by auto


[STATEMENT]
lemma prv_imp_eqvEL:
"\<phi>1 \<in> fmla \<Longrightarrow> \<phi>2 \<in> fmla \<Longrightarrow> prv (eqv \<phi>1 \<phi>2) \<Longrightarrow> prv (imp \<phi>1 \<phi>2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<phi>1 \<in> fmla; \<phi>2 \<in> fmla; prv (eqv \<phi>1 \<phi>2)\<rbrakk> \<Longrightarrow> prv (imp \<phi>1 \<phi>2)
[PROOF STEP]
unfolding eqv_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<phi>1 \<in> fmla; \<phi>2 \<in> fmla; prv (cnj (imp \<phi>1 \<phi>2) (imp \<phi>2 \<phi>1))\<rbrakk> \<Longrightarrow> prv (imp \<phi>1 \<phi>2)
[PROOF STEP]
by (meson cnj imp prv_imp_cnjL prv_imp_mp)


[STATEMENT]
lemma prv_imp_eqvER:
"\<phi>1 \<in> fmla \<Longrightarrow> \<phi>2 \<in> fmla \<Longrightarrow> prv (eqv \<phi>1 \<phi>2) \<Longrightarrow> prv (imp \<phi>2 \<phi>1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<phi>1 \<in> fmla; \<phi>2 \<in> fmla; prv (eqv \<phi>1 \<phi>2)\<rbrakk> \<Longrightarrow> prv (imp \<phi>2 \<phi>1)
[PROOF STEP]
unfolding eqv_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<phi>1 \<in> fmla; \<phi>2 \<in> fmla; prv (cnj (imp \<phi>1 \<phi>2) (imp \<phi>2 \<phi>1))\<rbrakk> \<Longrightarrow> prv (imp \<phi>2 \<phi>1)
[PROOF STEP]
by (meson cnj imp prv_imp_cnjR prv_imp_mp)


[STATEMENT]
lemma prv_eqv_imp_trans:
assumes "\<phi> \<in> fmla" and "\<chi> \<in> fmla" and "\<psi> \<in> fmla"
shows "prv (imp (eqv \<phi> \<chi>) (imp (eqv \<chi> \<psi>) (eqv \<phi> \<psi>)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (imp (eqv \<phi> \<chi>) (imp (eqv \<chi> \<psi>) (eqv \<phi> \<psi>)))
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. prv (imp (eqv \<phi> \<chi>) (imp (eqv \<chi> \<psi>) (eqv \<phi> \<psi>)))
[PROOF STEP]
have "prv (imp (eqv \<phi> \<chi>) (imp (imp \<chi> \<psi>) (imp \<phi> \<psi>)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (imp (eqv \<phi> \<chi>) (imp (imp \<chi> \<psi>) (imp \<phi> \<psi>)))
[PROOF STEP]
using assms prv_imp_cnjL prv_imp_mp prv_imp_trans2 eqv_def
[PROOF STATE]
proof (prove)
using this:
\<phi> \<in> fmla
\<chi> \<in> fmla
\<psi> \<in> fmla
\<lbrakk>?\<phi> \<in> fmla; ?\<chi> \<in> fmla\<rbrakk> \<Longrightarrow> prv (imp (cnj ?\<phi> ?\<chi>) ?\<phi>)
\<lbrakk>?\<phi> \<in> fmla; ?\<chi> \<in> fmla; prv (imp ?\<phi> ?\<chi>); prv ?\<phi>\<rbrakk> \<Longrightarrow> prv ?\<chi>
\<lbrakk>?\<phi> \<in> fmla; ?\<chi> \<in> fmla; ?\<psi> \<in> fmla\<rbrakk> \<Longrightarrow> prv (imp (imp ?\<phi> ?\<chi>) (imp (imp ?\<chi> ?\<psi>) (imp ?\<phi> ?\<psi>)))
eqv ?\<phi> ?\<chi> = cnj (imp ?\<phi> ?\<chi>) (imp ?\<chi> ?\<phi>)

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

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

goal (1 subgoal):
 1. prv (imp (eqv \<phi> \<chi>) (imp (eqv \<chi> \<psi>) (imp \<phi> \<psi>)))
[PROOF STEP]
using prv_imp_cnjL prv_imp_mp prv_imp_trans2 eqv_def
[PROOF STATE]
proof (prove)
using this:
prv (imp (eqv \<phi> \<chi>) (imp (imp \<chi> \<psi>) (imp \<phi> \<psi>)))
\<lbrakk>?\<phi> \<in> fmla; ?\<chi> \<in> fmla\<rbrakk> \<Longrightarrow> prv (imp (cnj ?\<phi> ?\<chi>) ?\<phi>)
\<lbrakk>?\<phi> \<in> fmla; ?\<chi> \<in> fmla; prv (imp ?\<phi> ?\<chi>); prv ?\<phi>\<rbrakk> \<Longrightarrow> prv ?\<chi>
\<lbrakk>?\<phi> \<in> fmla; ?\<chi> \<in> fmla; ?\<psi> \<in> fmla\<rbrakk> \<Longrightarrow> prv (imp (imp ?\<phi> ?\<chi>) (imp (imp ?\<chi> ?\<psi>) (imp ?\<phi> ?\<psi>)))
eqv ?\<phi> ?\<chi> = cnj (imp ?\<phi> ?\<chi>) (imp ?\<chi> ?\<phi>)

goal (1 subgoal):
 1. prv (imp (eqv \<phi> \<chi>) (imp (eqv \<chi> \<psi>) (imp \<phi> \<psi>)))
[PROOF STEP]
by (metis (no_types) assms prv_imp_cnj3L prv_imp_com eqv imp)
[PROOF STATE]
proof (state)
this:
prv (imp (eqv \<phi> \<chi>) (imp (eqv \<chi> \<psi>) (imp \<phi> \<psi>)))

goal (1 subgoal):
 1. prv (imp (eqv \<phi> \<chi>) (imp (eqv \<chi> \<psi>) (eqv \<phi> \<psi>)))
[PROOF STEP]
hence 1: "prv (imp (cnj (eqv \<phi> \<chi>) (eqv \<chi> \<psi>)) (imp \<phi> \<psi>))"
[PROOF STATE]
proof (prove)
using this:
prv (imp (eqv \<phi> \<chi>) (imp (eqv \<chi> \<psi>) (imp \<phi> \<psi>)))

goal (1 subgoal):
 1. prv (imp (cnj (eqv \<phi> \<chi>) (eqv \<chi> \<psi>)) (imp \<phi> \<psi>))
[PROOF STEP]
using prv_cnj_imp_monoR2
[PROOF STATE]
proof (prove)
using this:
prv (imp (eqv \<phi> \<chi>) (imp (eqv \<chi> \<psi>) (imp \<phi> \<psi>)))
\<lbrakk>?\<phi> \<in> fmla; ?\<chi> \<in> fmla; ?\<psi> \<in> fmla; prv (imp ?\<phi> (imp ?\<chi> ?\<psi>))\<rbrakk> \<Longrightarrow> prv (imp (cnj ?\<phi> ?\<chi>) ?\<psi>)

goal (1 subgoal):
 1. prv (imp (cnj (eqv \<phi> \<chi>) (eqv \<chi> \<psi>)) (imp \<phi> \<psi>))
[PROOF STEP]
by (simp add: assms(1) assms(2) assms(3))
[PROOF STATE]
proof (state)
this:
prv (imp (cnj (eqv \<phi> \<chi>) (eqv \<chi> \<psi>)) (imp \<phi> \<psi>))

goal (1 subgoal):
 1. prv (imp (eqv \<phi> \<chi>) (imp (eqv \<chi> \<psi>) (eqv \<phi> \<psi>)))
[PROOF STEP]
have "prv (imp (eqv \<phi> \<chi>) (imp (imp \<psi> \<chi>) (imp \<psi> \<phi>)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (imp (eqv \<phi> \<chi>) (imp (imp \<psi> \<chi>) (imp \<psi> \<phi>)))
[PROOF STEP]
using prv_imp_cnjR prv_imp_mp prv_imp_trans1 eqv_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?\<phi> \<in> fmla; ?\<chi> \<in> fmla\<rbrakk> \<Longrightarrow> prv (imp (cnj ?\<phi> ?\<chi>) ?\<chi>)
\<lbrakk>?\<phi> \<in> fmla; ?\<chi> \<in> fmla; prv (imp ?\<phi> ?\<chi>); prv ?\<phi>\<rbrakk> \<Longrightarrow> prv ?\<chi>
\<lbrakk>?\<phi> \<in> fmla; ?\<chi> \<in> fmla; ?\<psi> \<in> fmla\<rbrakk> \<Longrightarrow> prv (imp (imp ?\<chi> ?\<psi>) (imp (imp ?\<phi> ?\<chi>) (imp ?\<phi> ?\<psi>)))
eqv ?\<phi> ?\<chi> = cnj (imp ?\<phi> ?\<chi>) (imp ?\<chi> ?\<phi>)

goal (1 subgoal):
 1. prv (imp (eqv \<phi> \<chi>) (imp (imp \<psi> \<chi>) (imp \<psi> \<phi>)))
[PROOF STEP]
by (metis assms prv_cnj_imp_monoR2 prv_imp_triv imp)
[PROOF STATE]
proof (state)
this:
prv (imp (eqv \<phi> \<chi>) (imp (imp \<psi> \<chi>) (imp \<psi> \<phi>)))

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

goal (1 subgoal):
 1. prv (imp (eqv \<phi> \<chi>) (imp (eqv \<chi> \<psi>) (imp \<psi> \<phi>)))
[PROOF STEP]
by (metis assms cnj eqv_def imp prv_imp_cnj3R prv_prv_imp_trans)
[PROOF STATE]
proof (state)
this:
prv (imp (eqv \<phi> \<chi>) (imp (eqv \<chi> \<psi>) (imp \<psi> \<phi>)))

goal (1 subgoal):
 1. prv (imp (eqv \<phi> \<chi>) (imp (eqv \<chi> \<psi>) (eqv \<phi> \<psi>)))
[PROOF STEP]
hence 2: "prv (imp (cnj (eqv \<phi> \<chi>) (eqv \<chi> \<psi>)) (imp \<psi> \<phi>))"
[PROOF STATE]
proof (prove)
using this:
prv (imp (eqv \<phi> \<chi>) (imp (eqv \<chi> \<psi>) (imp \<psi> \<phi>)))

goal (1 subgoal):
 1. prv (imp (cnj (eqv \<phi> \<chi>) (eqv \<chi> \<psi>)) (imp \<psi> \<phi>))
[PROOF STEP]
using prv_cnj_imp_monoR2
[PROOF STATE]
proof (prove)
using this:
prv (imp (eqv \<phi> \<chi>) (imp (eqv \<chi> \<psi>) (imp \<psi> \<phi>)))
\<lbrakk>?\<phi> \<in> fmla; ?\<chi> \<in> fmla; ?\<psi> \<in> fmla; prv (imp ?\<phi> (imp ?\<chi> ?\<psi>))\<rbrakk> \<Longrightarrow> prv (imp (cnj ?\<phi> ?\<chi>) ?\<psi>)

goal (1 subgoal):
 1. prv (imp (cnj (eqv \<phi> \<chi>) (eqv \<chi> \<psi>)) (imp \<psi> \<phi>))
[PROOF STEP]
by (metis (no_types, lifting) assms eqv imp)
[PROOF STATE]
proof (state)
this:
prv (imp (cnj (eqv \<phi> \<chi>) (eqv \<chi> \<psi>)) (imp \<psi> \<phi>))

goal (1 subgoal):
 1. prv (imp (eqv \<phi> \<chi>) (imp (eqv \<chi> \<psi>) (eqv \<phi> \<psi>)))
[PROOF STEP]
have "prv (imp (cnj (eqv \<phi> \<chi>) (eqv \<chi> \<psi>)) (eqv \<phi> \<psi>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (imp (cnj (eqv \<phi> \<chi>) (eqv \<chi> \<psi>)) (eqv \<phi> \<psi>))
[PROOF STEP]
using 1 2
[PROOF STATE]
proof (prove)
using this:
prv (imp (cnj (eqv \<phi> \<chi>) (eqv \<chi> \<psi>)) (imp \<phi> \<psi>))
prv (imp (cnj (eqv \<phi> \<chi>) (eqv \<chi> \<psi>)) (imp \<psi> \<phi>))

goal (1 subgoal):
 1. prv (imp (cnj (eqv \<phi> \<chi>) (eqv \<chi> \<psi>)) (eqv \<phi> \<psi>))
[PROOF STEP]
using assms prv_imp_cnj
[PROOF STATE]
proof (prove)
using this:
prv (imp (cnj (eqv \<phi> \<chi>) (eqv \<chi> \<psi>)) (imp \<phi> \<psi>))
prv (imp (cnj (eqv \<phi> \<chi>) (eqv \<chi> \<psi>)) (imp \<psi> \<phi>))
\<phi> \<in> fmla
\<chi> \<in> fmla
\<psi> \<in> fmla
\<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>))

goal (1 subgoal):
 1. prv (imp (cnj (eqv \<phi> \<chi>) (eqv \<chi> \<psi>)) (eqv \<phi> \<psi>))
[PROOF STEP]
by (auto simp: eqv_def[of \<phi> \<psi>])
[PROOF STATE]
proof (state)
this:
prv (imp (cnj (eqv \<phi> \<chi>) (eqv \<chi> \<psi>)) (eqv \<phi> \<psi>))

goal (1 subgoal):
 1. prv (imp (eqv \<phi> \<chi>) (imp (eqv \<chi> \<psi>) (eqv \<phi> \<psi>)))
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
prv (imp (cnj (eqv \<phi> \<chi>) (eqv \<chi> \<psi>)) (eqv \<phi> \<psi>))

goal (1 subgoal):
 1. prv (imp (eqv \<phi> \<chi>) (imp (eqv \<chi> \<psi>) (eqv \<phi> \<psi>)))
[PROOF STEP]
by (simp add: assms prv_cnj_imp)
[PROOF STATE]
proof (state)
this:
prv (imp (eqv \<phi> \<chi>) (imp (eqv \<chi> \<psi>) (eqv \<phi> \<psi>)))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma prv_eqv_cnj_trans:
assumes "\<phi> \<in> fmla" and "\<chi> \<in> fmla" and "\<psi> \<in> fmla"
shows "prv (imp (cnj (eqv \<phi> \<chi>) (eqv \<chi> \<psi>)) (eqv \<phi> \<psi>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (imp (cnj (eqv \<phi> \<chi>) (eqv \<chi> \<psi>)) (eqv \<phi> \<psi>))
[PROOF STEP]
by (simp add: assms prv_eqv_imp_trans prv_cnj_imp_monoR2)


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


[STATEMENT]
lemma prv_eqv_refl: "\<phi> \<in> fmla \<Longrightarrow> prv (eqv \<phi> \<phi>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<phi> \<in> fmla \<Longrightarrow> prv (eqv \<phi> \<phi>)
[PROOF STEP]
by (simp add: prv_cnjI prv_imp_refl eqv_def)


[STATEMENT]
lemma prv_eqv_sym:
assumes "\<phi> \<in> fmla" and "\<chi> \<in> fmla"
shows "prv (eqv \<phi> \<chi>) \<Longrightarrow> prv (eqv \<chi> \<phi>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (eqv \<phi> \<chi>) \<Longrightarrow> prv (eqv \<chi> \<phi>)
[PROOF STEP]
using assms prv_cnjI prv_imp_cnjL prv_imp_cnjR prv_imp_mp eqv_def
[PROOF STATE]
proof (prove)
using this:
\<phi> \<in> fmla
\<chi> \<in> fmla
\<lbrakk>?\<phi> \<in> fmla; ?\<chi> \<in> fmla; prv ?\<phi>; prv ?\<chi>\<rbrakk> \<Longrightarrow> prv (cnj ?\<phi> ?\<chi>)
\<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>?\<phi> \<in> fmla; ?\<chi> \<in> fmla; prv (imp ?\<phi> ?\<chi>); prv ?\<phi>\<rbrakk> \<Longrightarrow> prv ?\<chi>
eqv ?\<phi> ?\<chi> = cnj (imp ?\<phi> ?\<chi>) (imp ?\<chi> ?\<phi>)

goal (1 subgoal):
 1. prv (eqv \<phi> \<chi>) \<Longrightarrow> prv (eqv \<chi> \<phi>)
[PROOF STEP]
by (meson prv_eqv_imp eqv)


[STATEMENT]
lemma prv_eqv_trans:
assumes "\<phi> \<in> fmla" and "\<chi> \<in> fmla" and "\<psi> \<in> fmla"
shows "prv (eqv \<phi> \<chi>) \<Longrightarrow> prv (eqv \<chi> \<psi>) \<Longrightarrow> prv (eqv \<phi> \<psi>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>prv (eqv \<phi> \<chi>); prv (eqv \<chi> \<psi>)\<rbrakk> \<Longrightarrow> prv (eqv \<phi> \<psi>)
[PROOF STEP]
using assms prv_cnjI prv_cnj_imp_monoR2 prv_imp_mp prv_imp_trans1 prv_imp_imp_triv eqv_def
[PROOF STATE]
proof (prove)
using this:
\<phi> \<in> fmla
\<chi> \<in> fmla
\<psi> \<in> fmla
\<lbrakk>?\<phi> \<in> fmla; ?\<chi> \<in> fmla; prv ?\<phi>; prv ?\<chi>\<rbrakk> \<Longrightarrow> prv (cnj ?\<phi> ?\<chi>)
\<lbrakk>?\<phi> \<in> fmla; ?\<chi> \<in> fmla; ?\<psi> \<in> fmla; prv (imp ?\<phi> (imp ?\<chi> ?\<psi>))\<rbrakk> \<Longrightarrow> prv (imp (cnj ?\<phi> ?\<chi>) ?\<psi>)
\<lbrakk>?\<phi> \<in> fmla; ?\<chi> \<in> fmla; prv (imp ?\<phi> ?\<chi>); prv ?\<phi>\<rbrakk> \<Longrightarrow> prv ?\<chi>
\<lbrakk>?\<phi> \<in> fmla; ?\<chi> \<in> fmla; ?\<psi> \<in> fmla\<rbrakk> \<Longrightarrow> prv (imp (imp ?\<chi> ?\<psi>) (imp (imp ?\<phi> ?\<chi>) (imp ?\<phi> ?\<psi>)))
\<lbrakk>?\<phi> \<in> fmla; ?\<chi> \<in> fmla\<rbrakk> \<Longrightarrow> prv (imp ?\<phi> (imp ?\<chi> ?\<phi>))
eqv ?\<phi> ?\<chi> = cnj (imp ?\<phi> ?\<chi>) (imp ?\<chi> ?\<phi>)

goal (1 subgoal):
 1. \<lbrakk>prv (eqv \<phi> \<chi>); prv (eqv \<chi> \<psi>)\<rbrakk> \<Longrightarrow> prv (eqv \<phi> \<psi>)
[PROOF STEP]
by (metis prv_prv_imp_trans prv_imp_cnjL prv_imp_cnjR eqv imp)


[STATEMENT]
lemma imp_imp_compat_eqvL:
assumes "\<phi>1 \<in> fmla" and "\<phi>2 \<in> fmla" and "\<chi> \<in> fmla"
shows "prv (imp (eqv \<phi>1 \<phi>2) (eqv (imp \<phi>1 \<chi>) (imp \<phi>2 \<chi>)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (imp (eqv \<phi>1 \<phi>2) (eqv (imp \<phi>1 \<chi>) (imp \<phi>2 \<chi>)))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. prv (imp (eqv \<phi>1 \<phi>2) (eqv (imp \<phi>1 \<chi>) (imp \<phi>2 \<chi>)))
[PROOF STEP]
have f: "prv (imp (eqv \<phi>1 \<phi>2) (eqv (imp \<phi>1 \<chi>) (imp \<phi>2 \<chi>)))"
    if "prv (imp (eqv \<phi>1 \<phi>2) (imp (imp \<phi>2 \<chi>) (imp \<phi>1 \<chi>)))" "prv (imp (eqv \<phi>1 \<phi>2) (imp (imp \<phi>1 \<chi>) (imp \<phi>2 \<chi>)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (imp (eqv \<phi>1 \<phi>2) (eqv (imp \<phi>1 \<chi>) (imp \<phi>2 \<chi>)))
[PROOF STEP]
using assms that prv_imp_cnj
[PROOF STATE]
proof (prove)
using this:
\<phi>1 \<in> fmla
\<phi>2 \<in> fmla
\<chi> \<in> fmla
prv (imp (eqv \<phi>1 \<phi>2) (imp (imp \<phi>2 \<chi>) (imp \<phi>1 \<chi>)))
prv (imp (eqv \<phi>1 \<phi>2) (imp (imp \<phi>1 \<chi>) (imp \<phi>2 \<chi>)))
\<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>))

goal (1 subgoal):
 1. prv (imp (eqv \<phi>1 \<phi>2) (eqv (imp \<phi>1 \<chi>) (imp \<phi>2 \<chi>)))
[PROOF STEP]
by (auto simp: eqv_def)
[PROOF STATE]
proof (state)
this:
\<lbrakk>prv (imp (eqv \<phi>1 \<phi>2) (imp (imp \<phi>2 \<chi>) (imp \<phi>1 \<chi>))); prv (imp (eqv \<phi>1 \<phi>2) (imp (imp \<phi>1 \<chi>) (imp \<phi>2 \<chi>)))\<rbrakk> \<Longrightarrow> prv (imp (eqv \<phi>1 \<phi>2) (eqv (imp \<phi>1 \<chi>) (imp \<phi>2 \<chi>)))

goal (1 subgoal):
 1. prv (imp (eqv \<phi>1 \<phi>2) (eqv (imp \<phi>1 \<chi>) (imp \<phi>2 \<chi>)))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<lbrakk>prv (imp (eqv \<phi>1 \<phi>2) (imp (imp \<phi>2 \<chi>) (imp \<phi>1 \<chi>))); prv (imp (eqv \<phi>1 \<phi>2) (imp (imp \<phi>1 \<chi>) (imp \<phi>2 \<chi>)))\<rbrakk> \<Longrightarrow> prv (imp (eqv \<phi>1 \<phi>2) (eqv (imp \<phi>1 \<chi>) (imp \<phi>2 \<chi>)))

goal (1 subgoal):
 1. prv (imp (eqv \<phi>1 \<phi>2) (eqv (imp \<phi>1 \<chi>) (imp \<phi>2 \<chi>)))
[PROOF STEP]
have "(prv (imp (eqv \<phi>1 \<phi>2) (imp \<phi>1 \<phi>2)) \<and> prv (imp (eqv \<phi>1 \<phi>2) (imp \<phi>2 \<phi>1)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (imp (eqv \<phi>1 \<phi>2) (imp \<phi>1 \<phi>2)) \<and> prv (imp (eqv \<phi>1 \<phi>2) (imp \<phi>2 \<phi>1))
[PROOF STEP]
by (simp add: assms eqv_def prv_imp_cnjL prv_imp_cnjR)
[PROOF STATE]
proof (state)
this:
prv (imp (eqv \<phi>1 \<phi>2) (imp \<phi>1 \<phi>2)) \<and> prv (imp (eqv \<phi>1 \<phi>2) (imp \<phi>2 \<phi>1))

goal (1 subgoal):
 1. prv (imp (eqv \<phi>1 \<phi>2) (eqv (imp \<phi>1 \<chi>) (imp \<phi>2 \<chi>)))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>prv (imp (eqv \<phi>1 \<phi>2) (imp (imp \<phi>2 \<chi>) (imp \<phi>1 \<chi>))); prv (imp (eqv \<phi>1 \<phi>2) (imp (imp \<phi>1 \<chi>) (imp \<phi>2 \<chi>)))\<rbrakk> \<Longrightarrow> prv (imp (eqv \<phi>1 \<phi>2) (eqv (imp \<phi>1 \<chi>) (imp \<phi>2 \<chi>)))
prv (imp (eqv \<phi>1 \<phi>2) (imp \<phi>1 \<phi>2)) \<and> prv (imp (eqv \<phi>1 \<phi>2) (imp \<phi>2 \<phi>1))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>prv (imp (eqv \<phi>1 \<phi>2) (imp (imp \<phi>2 \<chi>) (imp \<phi>1 \<chi>))); prv (imp (eqv \<phi>1 \<phi>2) (imp (imp \<phi>1 \<chi>) (imp \<phi>2 \<chi>)))\<rbrakk> \<Longrightarrow> prv (imp (eqv \<phi>1 \<phi>2) (eqv (imp \<phi>1 \<chi>) (imp \<phi>2 \<chi>)))
prv (imp (eqv \<phi>1 \<phi>2) (imp \<phi>1 \<phi>2)) \<and> prv (imp (eqv \<phi>1 \<phi>2) (imp \<phi>2 \<phi>1))

goal (1 subgoal):
 1. prv (imp (eqv \<phi>1 \<phi>2) (eqv (imp \<phi>1 \<chi>) (imp \<phi>2 \<chi>)))
[PROOF STEP]
by (metis (no_types) assms eqv imp prv_imp_trans2 prv_prv_imp_trans)
[PROOF STATE]
proof (state)
this:
prv (imp (eqv \<phi>1 \<phi>2) (eqv (imp \<phi>1 \<chi>) (imp \<phi>2 \<chi>)))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma imp_imp_compat_eqvR:
assumes "\<phi> \<in> fmla" and "\<chi>1 \<in> fmla" and "\<chi>2 \<in> fmla"
shows "prv (imp (eqv \<chi>1 \<chi>2) (eqv (imp \<phi> \<chi>1) (imp \<phi> \<chi>2)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (imp (eqv \<chi>1 \<chi>2) (eqv (imp \<phi> \<chi>1) (imp \<phi> \<chi>2)))
[PROOF STEP]
by (simp add: assms prv_cnj_mono prv_imp_trans1 eqv_def)


[STATEMENT]
lemma imp_imp_compat_eqv:
assumes "\<phi>1 \<in> fmla" and "\<phi>2 \<in> fmla" and "\<chi>1 \<in> fmla" and "\<chi>2 \<in> fmla"
shows "prv (imp (eqv \<phi>1 \<phi>2) (imp (eqv \<chi>1 \<chi>2) (eqv (imp \<phi>1 \<chi>1) (imp \<phi>2 \<chi>2))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (imp (eqv \<phi>1 \<phi>2) (imp (eqv \<chi>1 \<chi>2) (eqv (imp \<phi>1 \<chi>1) (imp \<phi>2 \<chi>2))))
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. prv (imp (eqv \<phi>1 \<phi>2) (imp (eqv \<chi>1 \<chi>2) (eqv (imp \<phi>1 \<chi>1) (imp \<phi>2 \<chi>2))))
[PROOF STEP]
have "prv (imp (eqv \<phi>1 \<phi>2) (imp (eqv \<chi>1 \<chi>2) (cnj (eqv (imp \<phi>1 \<chi>1) (imp \<phi>2 \<chi>1))
                                                    (eqv (imp \<phi>2 \<chi>1) (imp \<phi>2 \<chi>2)))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (imp (eqv \<phi>1 \<phi>2) (imp (eqv \<chi>1 \<chi>2) (cnj (eqv (imp \<phi>1 \<chi>1) (imp \<phi>2 \<chi>1)) (eqv (imp \<phi>2 \<chi>1) (imp \<phi>2 \<chi>2)))))
[PROOF STEP]
using prv_imp_cnj5
    [OF _ _ _ _ imp_imp_compat_eqvL[of \<phi>1 \<phi>2 \<chi>1] imp_imp_compat_eqvR[of \<phi>2 \<chi>1 \<chi>2]] assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>eqv \<phi>1 \<phi>2 \<in> fmla; eqv \<chi>1 \<chi>2 \<in> fmla; eqv (imp \<phi>1 \<chi>1) (imp \<phi>2 \<chi>1) \<in> fmla; eqv (imp \<phi>2 \<chi>1) (imp \<phi>2 \<chi>2) \<in> fmla; \<phi>1 \<in> fmla; \<phi>2 \<in> fmla; \<chi>1 \<in> fmla; \<phi>2 \<in> fmla; \<chi>1 \<in> fmla; \<chi>2 \<in> fmla\<rbrakk> \<Longrightarrow> prv (imp (eqv \<phi>1 \<phi>2) (imp (eqv \<chi>1 \<chi>2) (cnj (eqv (imp \<phi>1 \<chi>1) (imp \<phi>2 \<chi>1)) (eqv (imp \<phi>2 \<chi>1) (imp \<phi>2 \<chi>2)))))
\<phi>1 \<in> fmla
\<phi>2 \<in> fmla
\<chi>1 \<in> fmla
\<chi>2 \<in> fmla

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

goal (1 subgoal):
 1. prv (imp (eqv \<phi>1 \<phi>2) (imp (eqv \<chi>1 \<chi>2) (eqv (imp \<phi>1 \<chi>1) (imp \<phi>2 \<chi>2))))
[PROOF STEP]
hence "prv (imp (cnj (eqv \<phi>1 \<phi>2) (eqv \<chi>1 \<chi>2)) (cnj (eqv (imp \<phi>1 \<chi>1) (imp \<phi>2 \<chi>1))
                                                      (eqv (imp \<phi>2 \<chi>1) (imp \<phi>2 \<chi>2))))"
[PROOF STATE]
proof (prove)
using this:
prv (imp (eqv \<phi>1 \<phi>2) (imp (eqv \<chi>1 \<chi>2) (cnj (eqv (imp \<phi>1 \<chi>1) (imp \<phi>2 \<chi>1)) (eqv (imp \<phi>2 \<chi>1) (imp \<phi>2 \<chi>2)))))

goal (1 subgoal):
 1. prv (imp (cnj (eqv \<phi>1 \<phi>2) (eqv \<chi>1 \<chi>2)) (cnj (eqv (imp \<phi>1 \<chi>1) (imp \<phi>2 \<chi>1)) (eqv (imp \<phi>2 \<chi>1) (imp \<phi>2 \<chi>2))))
[PROOF STEP]
by(simp add: assms prv_cnj_imp_monoR2)
[PROOF STATE]
proof (state)
this:
prv (imp (cnj (eqv \<phi>1 \<phi>2) (eqv \<chi>1 \<chi>2)) (cnj (eqv (imp \<phi>1 \<chi>1) (imp \<phi>2 \<chi>1)) (eqv (imp \<phi>2 \<chi>1) (imp \<phi>2 \<chi>2))))

goal (1 subgoal):
 1. prv (imp (eqv \<phi>1 \<phi>2) (imp (eqv \<chi>1 \<chi>2) (eqv (imp \<phi>1 \<chi>1) (imp \<phi>2 \<chi>2))))
[PROOF STEP]
hence "prv (imp (cnj (eqv \<phi>1 \<phi>2) (eqv \<chi>1 \<chi>2)) (eqv (imp \<phi>1 \<chi>1) (imp \<phi>2 \<chi>2)))"
[PROOF STATE]
proof (prove)
using this:
prv (imp (cnj (eqv \<phi>1 \<phi>2) (eqv \<chi>1 \<chi>2)) (cnj (eqv (imp \<phi>1 \<chi>1) (imp \<phi>2 \<chi>1)) (eqv (imp \<phi>2 \<chi>1) (imp \<phi>2 \<chi>2))))

goal (1 subgoal):
 1. prv (imp (cnj (eqv \<phi>1 \<phi>2) (eqv \<chi>1 \<chi>2)) (eqv (imp \<phi>1 \<chi>1) (imp \<phi>2 \<chi>2)))
[PROOF STEP]
using assms prv_eqv_cnj_trans[of "imp \<phi>1 \<chi>1" "imp \<phi>2 \<chi>1" "imp \<phi>2 \<chi>2"]
[PROOF STATE]
proof (prove)
using this:
prv (imp (cnj (eqv \<phi>1 \<phi>2) (eqv \<chi>1 \<chi>2)) (cnj (eqv (imp \<phi>1 \<chi>1) (imp \<phi>2 \<chi>1)) (eqv (imp \<phi>2 \<chi>1) (imp \<phi>2 \<chi>2))))
\<phi>1 \<in> fmla
\<phi>2 \<in> fmla
\<chi>1 \<in> fmla
\<chi>2 \<in> fmla
\<lbrakk>imp \<phi>1 \<chi>1 \<in> fmla; imp \<phi>2 \<chi>1 \<in> fmla; imp \<phi>2 \<chi>2 \<in> fmla\<rbrakk> \<Longrightarrow> prv (imp (cnj (eqv (imp \<phi>1 \<chi>1) (imp \<phi>2 \<chi>1)) (eqv (imp \<phi>2 \<chi>1) (imp \<phi>2 \<chi>2))) (eqv (imp \<phi>1 \<chi>1) (imp \<phi>2 \<chi>2)))

goal (1 subgoal):
 1. prv (imp (cnj (eqv \<phi>1 \<phi>2) (eqv \<chi>1 \<chi>2)) (eqv (imp \<phi>1 \<chi>1) (imp \<phi>2 \<chi>2)))
[PROOF STEP]
using prv_imp_mp prv_imp_trans2
[PROOF STATE]
proof (prove)
using this:
prv (imp (cnj (eqv \<phi>1 \<phi>2) (eqv \<chi>1 \<chi>2)) (cnj (eqv (imp \<phi>1 \<chi>1) (imp \<phi>2 \<chi>1)) (eqv (imp \<phi>2 \<chi>1) (imp \<phi>2 \<chi>2))))
\<phi>1 \<in> fmla
\<phi>2 \<in> fmla
\<chi>1 \<in> fmla
\<chi>2 \<in> fmla
\<lbrakk>imp \<phi>1 \<chi>1 \<in> fmla; imp \<phi>2 \<chi>1 \<in> fmla; imp \<phi>2 \<chi>2 \<in> fmla\<rbrakk> \<Longrightarrow> prv (imp (cnj (eqv (imp \<phi>1 \<chi>1) (imp \<phi>2 \<chi>1)) (eqv (imp \<phi>2 \<chi>1) (imp \<phi>2 \<chi>2))) (eqv (imp \<phi>1 \<chi>1) (imp \<phi>2 \<chi>2)))
\<lbrakk>?\<phi> \<in> fmla; ?\<chi> \<in> fmla; prv (imp ?\<phi> ?\<chi>); prv ?\<phi>\<rbrakk> \<Longrightarrow> prv ?\<chi>
\<lbrakk>?\<phi> \<in> fmla; ?\<chi> \<in> fmla; ?\<psi> \<in> fmla\<rbrakk> \<Longrightarrow> prv (imp (imp ?\<phi> ?\<chi>) (imp (imp ?\<chi> ?\<psi>) (imp ?\<phi> ?\<psi>)))

goal (1 subgoal):
 1. prv (imp (cnj (eqv \<phi>1 \<phi>2) (eqv \<chi>1 \<chi>2)) (eqv (imp \<phi>1 \<chi>1) (imp \<phi>2 \<chi>2)))
[PROOF STEP]
by (metis (no_types) cnj prv_prv_imp_trans eqv imp)
[PROOF STATE]
proof (state)
this:
prv (imp (cnj (eqv \<phi>1 \<phi>2) (eqv \<chi>1 \<chi>2)) (eqv (imp \<phi>1 \<chi>1) (imp \<phi>2 \<chi>2)))

goal (1 subgoal):
 1. prv (imp (eqv \<phi>1 \<phi>2) (imp (eqv \<chi>1 \<chi>2) (eqv (imp \<phi>1 \<chi>1) (imp \<phi>2 \<chi>2))))
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
prv (imp (cnj (eqv \<phi>1 \<phi>2) (eqv \<chi>1 \<chi>2)) (eqv (imp \<phi>1 \<chi>1) (imp \<phi>2 \<chi>2)))

goal (1 subgoal):
 1. prv (imp (eqv \<phi>1 \<phi>2) (imp (eqv \<chi>1 \<chi>2) (eqv (imp \<phi>1 \<chi>1) (imp \<phi>2 \<chi>2))))
[PROOF STEP]
using assms prv_cnj_imp
[PROOF STATE]
proof (prove)
using this:
prv (imp (cnj (eqv \<phi>1 \<phi>2) (eqv \<chi>1 \<chi>2)) (eqv (imp \<phi>1 \<chi>1) (imp \<phi>2 \<chi>2)))
\<phi>1 \<in> fmla
\<phi>2 \<in> fmla
\<chi>1 \<in> fmla
\<chi>2 \<in> fmla
\<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. prv (imp (eqv \<phi>1 \<phi>2) (imp (eqv \<chi>1 \<chi>2) (eqv (imp \<phi>1 \<chi>1) (imp \<phi>2 \<chi>2))))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
prv (imp (eqv \<phi>1 \<phi>2) (imp (eqv \<chi>1 \<chi>2) (eqv (imp \<phi>1 \<chi>1) (imp \<phi>2 \<chi>2))))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma imp_compat_eqvL:
assumes "\<phi>1 \<in> fmla" and "\<phi>2 \<in> fmla" and "\<chi> \<in> fmla"
assumes "prv (eqv \<phi>1 \<phi>2)"
shows "prv (eqv (imp \<phi>1 \<chi>) (imp \<phi>2 \<chi>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (eqv (imp \<phi>1 \<chi>) (imp \<phi>2 \<chi>))
[PROOF STEP]
using assms prv_imp_mp imp_imp_compat_eqvL
[PROOF STATE]
proof (prove)
using this:
\<phi>1 \<in> fmla
\<phi>2 \<in> fmla
\<chi> \<in> fmla
prv (eqv \<phi>1 \<phi>2)
\<lbrakk>?\<phi> \<in> fmla; ?\<chi> \<in> fmla; prv (imp ?\<phi> ?\<chi>); prv ?\<phi>\<rbrakk> \<Longrightarrow> prv ?\<chi>
\<lbrakk>?\<phi>1.0 \<in> fmla; ?\<phi>2.0 \<in> fmla; ?\<chi> \<in> fmla\<rbrakk> \<Longrightarrow> prv (imp (eqv ?\<phi>1.0 ?\<phi>2.0) (eqv (imp ?\<phi>1.0 ?\<chi>) (imp ?\<phi>2.0 ?\<chi>)))

goal (1 subgoal):
 1. prv (eqv (imp \<phi>1 \<chi>) (imp \<phi>2 \<chi>))
[PROOF STEP]
by (meson eqv imp)


[STATEMENT]
lemma imp_compat_eqvR:
assumes "\<phi> \<in> fmla" and "\<chi>1 \<in> fmla" and "\<chi>2 \<in> fmla"
assumes "prv (eqv \<chi>1 \<chi>2)"
shows "prv (eqv (imp \<phi> \<chi>1) (imp \<phi> \<chi>2))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (eqv (imp \<phi> \<chi>1) (imp \<phi> \<chi>2))
[PROOF STEP]
using assms prv_imp_mp imp_imp_compat_eqvR
[PROOF STATE]
proof (prove)
using this:
\<phi> \<in> fmla
\<chi>1 \<in> fmla
\<chi>2 \<in> fmla
prv (eqv \<chi>1 \<chi>2)
\<lbrakk>?\<phi> \<in> fmla; ?\<chi> \<in> fmla; prv (imp ?\<phi> ?\<chi>); prv ?\<phi>\<rbrakk> \<Longrightarrow> prv ?\<chi>
\<lbrakk>?\<phi> \<in> fmla; ?\<chi>1.0 \<in> fmla; ?\<chi>2.0 \<in> fmla\<rbrakk> \<Longrightarrow> prv (imp (eqv ?\<chi>1.0 ?\<chi>2.0) (eqv (imp ?\<phi> ?\<chi>1.0) (imp ?\<phi> ?\<chi>2.0)))

goal (1 subgoal):
 1. prv (eqv (imp \<phi> \<chi>1) (imp \<phi> \<chi>2))
[PROOF STEP]
by (meson eqv imp)


[STATEMENT]
lemma imp_compat_eqv:
assumes "\<phi>1 \<in> fmla" and "\<phi>2 \<in> fmla" and "\<chi>1 \<in> fmla" and "\<chi>2 \<in> fmla"
assumes "prv (eqv \<phi>1 \<phi>2)" and "prv (eqv \<chi>1 \<chi>2)"
shows "prv (eqv (imp \<phi>1 \<chi>1) (imp \<phi>2 \<chi>2))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (eqv (imp \<phi>1 \<chi>1) (imp \<phi>2 \<chi>2))
[PROOF STEP]
using assms prv_imp_mp imp_imp_compat_eqv
[PROOF STATE]
proof (prove)
using this:
\<phi>1 \<in> fmla
\<phi>2 \<in> fmla
\<chi>1 \<in> fmla
\<chi>2 \<in> fmla
prv (eqv \<phi>1 \<phi>2)
prv (eqv \<chi>1 \<chi>2)
\<lbrakk>?\<phi> \<in> fmla; ?\<chi> \<in> fmla; prv (imp ?\<phi> ?\<chi>); prv ?\<phi>\<rbrakk> \<Longrightarrow> prv ?\<chi>
\<lbrakk>?\<phi>1.0 \<in> fmla; ?\<phi>2.0 \<in> fmla; ?\<chi>1.0 \<in> fmla; ?\<chi>2.0 \<in> fmla\<rbrakk> \<Longrightarrow> prv (imp (eqv ?\<phi>1.0 ?\<phi>2.0) (imp (eqv ?\<chi>1.0 ?\<chi>2.0) (eqv (imp ?\<phi>1.0 ?\<chi>1.0) (imp ?\<phi>2.0 ?\<chi>2.0))))

goal (1 subgoal):
 1. prv (eqv (imp \<phi>1 \<chi>1) (imp \<phi>2 \<chi>2))
[PROOF STEP]
by (metis eqv imp)


[STATEMENT]
lemma imp_cnj_compat_eqvL:
assumes "\<phi>1 \<in> fmla" and "\<phi>2 \<in> fmla" and "\<chi> \<in> fmla"
shows "prv (imp (eqv \<phi>1 \<phi>2) (eqv (cnj \<phi>1 \<chi>) (cnj \<phi>2 \<chi>)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (imp (eqv \<phi>1 \<phi>2) (eqv (cnj \<phi>1 \<chi>) (cnj \<phi>2 \<chi>)))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. prv (imp (eqv \<phi>1 \<phi>2) (eqv (cnj \<phi>1 \<chi>) (cnj \<phi>2 \<chi>)))
[PROOF STEP]
have "prv (imp (imp (imp \<phi>2 \<phi>1) (imp (cnj \<phi>2 \<chi>) (cnj \<phi>1 \<chi>)))
    (imp (cnj (imp \<phi>1 \<phi>2) (imp \<phi>2 \<phi>1)) (cnj (imp (cnj \<phi>1 \<chi>) (cnj \<phi>2 \<chi>))
    (imp (cnj \<phi>2 \<chi>) (cnj \<phi>1 \<chi>)))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (imp (imp (imp \<phi>2 \<phi>1) (imp (cnj \<phi>2 \<chi>) (cnj \<phi>1 \<chi>))) (imp (cnj (imp \<phi>1 \<phi>2) (imp \<phi>2 \<phi>1)) (cnj (imp (cnj \<phi>1 \<chi>) (cnj \<phi>2 \<chi>)) (imp (cnj \<phi>2 \<chi>) (cnj \<phi>1 \<chi>)))))
[PROOF STEP]
by (metis (no_types) imp cnj assms prv_imp_mp assms prv_cnj_imp_mono prv_imp_com prv_imp_refl)
[PROOF STATE]
proof (state)
this:
prv (imp (imp (imp \<phi>2 \<phi>1) (imp (cnj \<phi>2 \<chi>) (cnj \<phi>1 \<chi>))) (imp (cnj (imp \<phi>1 \<phi>2) (imp \<phi>2 \<phi>1)) (cnj (imp (cnj \<phi>1 \<chi>) (cnj \<phi>2 \<chi>)) (imp (cnj \<phi>2 \<chi>) (cnj \<phi>1 \<chi>)))))

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

goal (1 subgoal):
 1. prv (imp (eqv \<phi>1 \<phi>2) (eqv (cnj \<phi>1 \<chi>) (cnj \<phi>2 \<chi>)))
[PROOF STEP]
by (metis (no_types) imp cnj assms prv_imp_mp assms eqv_def prv_cnj_imp_mono prv_imp_com prv_imp_refl)
[PROOF STATE]
proof (state)
this:
prv (imp (eqv \<phi>1 \<phi>2) (eqv (cnj \<phi>1 \<chi>) (cnj \<phi>2 \<chi>)))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma imp_cnj_compat_eqvR:
assumes "\<phi> \<in> fmla" and "\<chi>1 \<in> fmla" and "\<chi>2 \<in> fmla"
shows "prv (imp (eqv \<chi>1 \<chi>2) (eqv (cnj \<phi> \<chi>1) (cnj \<phi> \<chi>2)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (imp (eqv \<chi>1 \<chi>2) (eqv (cnj \<phi> \<chi>1) (cnj \<phi> \<chi>2)))
[PROOF STEP]
by (simp add: assms prv_cnj_mono prv_imp_cnj3R prv_imp_cnj4 prv_imp_cnjL prv_imp_triv eqv_def)


[STATEMENT]
lemma imp_cnj_compat_eqv:
assumes "\<phi>1 \<in> fmla" and "\<phi>2 \<in> fmla" and "\<chi>1 \<in> fmla" and "\<chi>2 \<in> fmla"
shows "prv (imp (eqv \<phi>1 \<phi>2) (imp (eqv \<chi>1 \<chi>2) (eqv (cnj \<phi>1 \<chi>1) (cnj \<phi>2 \<chi>2))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (imp (eqv \<phi>1 \<phi>2) (imp (eqv \<chi>1 \<chi>2) (eqv (cnj \<phi>1 \<chi>1) (cnj \<phi>2 \<chi>2))))
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. prv (imp (eqv \<phi>1 \<phi>2) (imp (eqv \<chi>1 \<chi>2) (eqv (cnj \<phi>1 \<chi>1) (cnj \<phi>2 \<chi>2))))
[PROOF STEP]
have "prv (imp (eqv \<phi>1 \<phi>2) (imp (eqv \<chi>1 \<chi>2) (cnj (eqv (cnj \<phi>1 \<chi>1) (cnj \<phi>2 \<chi>1))
                                                    (eqv (cnj \<phi>2 \<chi>1) (cnj \<phi>2 \<chi>2)))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (imp (eqv \<phi>1 \<phi>2) (imp (eqv \<chi>1 \<chi>2) (cnj (eqv (cnj \<phi>1 \<chi>1) (cnj \<phi>2 \<chi>1)) (eqv (cnj \<phi>2 \<chi>1) (cnj \<phi>2 \<chi>2)))))
[PROOF STEP]
using prv_imp_cnj5
    [OF _ _ _ _ imp_cnj_compat_eqvL[of \<phi>1 \<phi>2 \<chi>1] imp_cnj_compat_eqvR[of \<phi>2 \<chi>1 \<chi>2]] assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>eqv \<phi>1 \<phi>2 \<in> fmla; eqv \<chi>1 \<chi>2 \<in> fmla; eqv (cnj \<phi>1 \<chi>1) (cnj \<phi>2 \<chi>1) \<in> fmla; eqv (cnj \<phi>2 \<chi>1) (cnj \<phi>2 \<chi>2) \<in> fmla; \<phi>1 \<in> fmla; \<phi>2 \<in> fmla; \<chi>1 \<in> fmla; \<phi>2 \<in> fmla; \<chi>1 \<in> fmla; \<chi>2 \<in> fmla\<rbrakk> \<Longrightarrow> prv (imp (eqv \<phi>1 \<phi>2) (imp (eqv \<chi>1 \<chi>2) (cnj (eqv (cnj \<phi>1 \<chi>1) (cnj \<phi>2 \<chi>1)) (eqv (cnj \<phi>2 \<chi>1) (cnj \<phi>2 \<chi>2)))))
\<phi>1 \<in> fmla
\<phi>2 \<in> fmla
\<chi>1 \<in> fmla
\<chi>2 \<in> fmla

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

goal (1 subgoal):
 1. prv (imp (eqv \<phi>1 \<phi>2) (imp (eqv \<chi>1 \<chi>2) (eqv (cnj \<phi>1 \<chi>1) (cnj \<phi>2 \<chi>2))))
[PROOF STEP]
hence "prv (imp (cnj (eqv \<phi>1 \<phi>2) (eqv \<chi>1 \<chi>2)) (cnj (eqv (cnj \<phi>1 \<chi>1) (cnj \<phi>2 \<chi>1))
                                                      (eqv (cnj \<phi>2 \<chi>1) (cnj \<phi>2 \<chi>2))))"
[PROOF STATE]
proof (prove)
using this:
prv (imp (eqv \<phi>1 \<phi>2) (imp (eqv \<chi>1 \<chi>2) (cnj (eqv (cnj \<phi>1 \<chi>1) (cnj \<phi>2 \<chi>1)) (eqv (cnj \<phi>2 \<chi>1) (cnj \<phi>2 \<chi>2)))))

goal (1 subgoal):
 1. prv (imp (cnj (eqv \<phi>1 \<phi>2) (eqv \<chi>1 \<chi>2)) (cnj (eqv (cnj \<phi>1 \<chi>1) (cnj \<phi>2 \<chi>1)) (eqv (cnj \<phi>2 \<chi>1) (cnj \<phi>2 \<chi>2))))
[PROOF STEP]
by(simp add: assms prv_cnj_imp_monoR2)
[PROOF STATE]
proof (state)
this:
prv (imp (cnj (eqv \<phi>1 \<phi>2) (eqv \<chi>1 \<chi>2)) (cnj (eqv (cnj \<phi>1 \<chi>1) (cnj \<phi>2 \<chi>1)) (eqv (cnj \<phi>2 \<chi>1) (cnj \<phi>2 \<chi>2))))

goal (1 subgoal):
 1. prv (imp (eqv \<phi>1 \<phi>2) (imp (eqv \<chi>1 \<chi>2) (eqv (cnj \<phi>1 \<chi>1) (cnj \<phi>2 \<chi>2))))
[PROOF STEP]
hence "prv (imp (cnj (eqv \<phi>1 \<phi>2) (eqv \<chi>1 \<chi>2)) (eqv (cnj \<phi>1 \<chi>1) (cnj \<phi>2 \<chi>2)))"
[PROOF STATE]
proof (prove)
using this:
prv (imp (cnj (eqv \<phi>1 \<phi>2) (eqv \<chi>1 \<chi>2)) (cnj (eqv (cnj \<phi>1 \<chi>1) (cnj \<phi>2 \<chi>1)) (eqv (cnj \<phi>2 \<chi>1) (cnj \<phi>2 \<chi>2))))

goal (1 subgoal):
 1. prv (imp (cnj (eqv \<phi>1 \<phi>2) (eqv \<chi>1 \<chi>2)) (eqv (cnj \<phi>1 \<chi>1) (cnj \<phi>2 \<chi>2)))
[PROOF STEP]
using assms prv_eqv_cnj_trans[of "cnj \<phi>1 \<chi>1" "cnj \<phi>2 \<chi>1" "cnj \<phi>2 \<chi>2"]
[PROOF STATE]
proof (prove)
using this:
prv (imp (cnj (eqv \<phi>1 \<phi>2) (eqv \<chi>1 \<chi>2)) (cnj (eqv (cnj \<phi>1 \<chi>1) (cnj \<phi>2 \<chi>1)) (eqv (cnj \<phi>2 \<chi>1) (cnj \<phi>2 \<chi>2))))
\<phi>1 \<in> fmla
\<phi>2 \<in> fmla
\<chi>1 \<in> fmla
\<chi>2 \<in> fmla
\<lbrakk>cnj \<phi>1 \<chi>1 \<in> fmla; cnj \<phi>2 \<chi>1 \<in> fmla; cnj \<phi>2 \<chi>2 \<in> fmla\<rbrakk> \<Longrightarrow> prv (imp (cnj (eqv (cnj \<phi>1 \<chi>1) (cnj \<phi>2 \<chi>1)) (eqv (cnj \<phi>2 \<chi>1) (cnj \<phi>2 \<chi>2))) (eqv (cnj \<phi>1 \<chi>1) (cnj \<phi>2 \<chi>2)))

goal (1 subgoal):
 1. prv (imp (cnj (eqv \<phi>1 \<phi>2) (eqv \<chi>1 \<chi>2)) (eqv (cnj \<phi>1 \<chi>1) (cnj \<phi>2 \<chi>2)))
[PROOF STEP]
using prv_imp_mp prv_imp_trans2
[PROOF STATE]
proof (prove)
using this:
prv (imp (cnj (eqv \<phi>1 \<phi>2) (eqv \<chi>1 \<chi>2)) (cnj (eqv (cnj \<phi>1 \<chi>1) (cnj \<phi>2 \<chi>1)) (eqv (cnj \<phi>2 \<chi>1) (cnj \<phi>2 \<chi>2))))
\<phi>1 \<in> fmla
\<phi>2 \<in> fmla
\<chi>1 \<in> fmla
\<chi>2 \<in> fmla
\<lbrakk>cnj \<phi>1 \<chi>1 \<in> fmla; cnj \<phi>2 \<chi>1 \<in> fmla; cnj \<phi>2 \<chi>2 \<in> fmla\<rbrakk> \<Longrightarrow> prv (imp (cnj (eqv (cnj \<phi>1 \<chi>1) (cnj \<phi>2 \<chi>1)) (eqv (cnj \<phi>2 \<chi>1) (cnj \<phi>2 \<chi>2))) (eqv (cnj \<phi>1 \<chi>1) (cnj \<phi>2 \<chi>2)))
\<lbrakk>?\<phi> \<in> fmla; ?\<chi> \<in> fmla; prv (imp ?\<phi> ?\<chi>); prv ?\<phi>\<rbrakk> \<Longrightarrow> prv ?\<chi>
\<lbrakk>?\<phi> \<in> fmla; ?\<chi> \<in> fmla; ?\<psi> \<in> fmla\<rbrakk> \<Longrightarrow> prv (imp (imp ?\<phi> ?\<chi>) (imp (imp ?\<chi> ?\<psi>) (imp ?\<phi> ?\<psi>)))

goal (1 subgoal):
 1. prv (imp (cnj (eqv \<phi>1 \<phi>2) (eqv \<chi>1 \<chi>2)) (eqv (cnj \<phi>1 \<chi>1) (cnj \<phi>2 \<chi>2)))
[PROOF STEP]
by (metis (no_types) cnj prv_prv_imp_trans eqv)
[PROOF STATE]
proof (state)
this:
prv (imp (cnj (eqv \<phi>1 \<phi>2) (eqv \<chi>1 \<chi>2)) (eqv (cnj \<phi>1 \<chi>1) (cnj \<phi>2 \<chi>2)))

goal (1 subgoal):
 1. prv (imp (eqv \<phi>1 \<phi>2) (imp (eqv \<chi>1 \<chi>2) (eqv (cnj \<phi>1 \<chi>1) (cnj \<phi>2 \<chi>2))))
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
prv (imp (cnj (eqv \<phi>1 \<phi>2) (eqv \<chi>1 \<chi>2)) (eqv (cnj \<phi>1 \<chi>1) (cnj \<phi>2 \<chi>2)))

goal (1 subgoal):
 1. prv (imp (eqv \<phi>1 \<phi>2) (imp (eqv \<chi>1 \<chi>2) (eqv (cnj \<phi>1 \<chi>1) (cnj \<phi>2 \<chi>2))))
[PROOF STEP]
using assms prv_cnj_imp
[PROOF STATE]
proof (prove)
using this:
prv (imp (cnj (eqv \<phi>1 \<phi>2) (eqv \<chi>1 \<chi>2)) (eqv (cnj \<phi>1 \<chi>1) (cnj \<phi>2 \<chi>2)))
\<phi>1 \<in> fmla
\<phi>2 \<in> fmla
\<chi>1 \<in> fmla
\<chi>2 \<in> fmla
\<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. prv (imp (eqv \<phi>1 \<phi>2) (imp (eqv \<chi>1 \<chi>2) (eqv (cnj \<phi>1 \<chi>1) (cnj \<phi>2 \<chi>2))))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
prv (imp (eqv \<phi>1 \<phi>2) (imp (eqv \<chi>1 \<chi>2) (eqv (cnj \<phi>1 \<chi>1) (cnj \<phi>2 \<chi>2))))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma cnj_compat_eqvL:
assumes "\<phi>1 \<in> fmla" and "\<phi>2 \<in> fmla" and "\<chi> \<in> fmla"
assumes "prv (eqv \<phi>1 \<phi>2)"
shows "prv (eqv (cnj \<phi>1 \<chi>) (cnj \<phi>2 \<chi>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (eqv (cnj \<phi>1 \<chi>) (cnj \<phi>2 \<chi>))
[PROOF STEP]
using assms prv_imp_mp imp_cnj_compat_eqvL
[PROOF STATE]
proof (prove)
using this:
\<phi>1 \<in> fmla
\<phi>2 \<in> fmla
\<chi> \<in> fmla
prv (eqv \<phi>1 \<phi>2)
\<lbrakk>?\<phi> \<in> fmla; ?\<chi> \<in> fmla; prv (imp ?\<phi> ?\<chi>); prv ?\<phi>\<rbrakk> \<Longrightarrow> prv ?\<chi>
\<lbrakk>?\<phi>1.0 \<in> fmla; ?\<phi>2.0 \<in> fmla; ?\<chi> \<in> fmla\<rbrakk> \<Longrightarrow> prv (imp (eqv ?\<phi>1.0 ?\<phi>2.0) (eqv (cnj ?\<phi>1.0 ?\<chi>) (cnj ?\<phi>2.0 ?\<chi>)))

goal (1 subgoal):
 1. prv (eqv (cnj \<phi>1 \<chi>) (cnj \<phi>2 \<chi>))
[PROOF STEP]
by (meson eqv cnj)


[STATEMENT]
lemma cnj_compat_eqvR:
assumes "\<phi> \<in> fmla" and "\<chi>1 \<in> fmla" and "\<chi>2 \<in> fmla"
assumes "prv (eqv \<chi>1 \<chi>2)"
shows "prv (eqv (cnj \<phi> \<chi>1) (cnj \<phi> \<chi>2))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (eqv (cnj \<phi> \<chi>1) (cnj \<phi> \<chi>2))
[PROOF STEP]
using assms prv_imp_mp imp_cnj_compat_eqvR
[PROOF STATE]
proof (prove)
using this:
\<phi> \<in> fmla
\<chi>1 \<in> fmla
\<chi>2 \<in> fmla
prv (eqv \<chi>1 \<chi>2)
\<lbrakk>?\<phi> \<in> fmla; ?\<chi> \<in> fmla; prv (imp ?\<phi> ?\<chi>); prv ?\<phi>\<rbrakk> \<Longrightarrow> prv ?\<chi>
\<lbrakk>?\<phi> \<in> fmla; ?\<chi>1.0 \<in> fmla; ?\<chi>2.0 \<in> fmla\<rbrakk> \<Longrightarrow> prv (imp (eqv ?\<chi>1.0 ?\<chi>2.0) (eqv (cnj ?\<phi> ?\<chi>1.0) (cnj ?\<phi> ?\<chi>2.0)))

goal (1 subgoal):
 1. prv (eqv (cnj \<phi> \<chi>1) (cnj \<phi> \<chi>2))
[PROOF STEP]
by (meson eqv cnj)


[STATEMENT]
lemma cnj_compat_eqv:
assumes "\<phi>1 \<in> fmla" and "\<phi>2 \<in> fmla" and "\<chi>1 \<in> fmla" and "\<chi>2 \<in> fmla"
assumes "prv (eqv \<phi>1 \<phi>2)" and "prv (eqv \<chi>1 \<chi>2)"
shows "prv (eqv (cnj \<phi>1 \<chi>1) (cnj \<phi>2 \<chi>2))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (eqv (cnj \<phi>1 \<chi>1) (cnj \<phi>2 \<chi>2))
[PROOF STEP]
using assms prv_imp_mp imp_cnj_compat_eqv
[PROOF STATE]
proof (prove)
using this:
\<phi>1 \<in> fmla
\<phi>2 \<in> fmla
\<chi>1 \<in> fmla
\<chi>2 \<in> fmla
prv (eqv \<phi>1 \<phi>2)
prv (eqv \<chi>1 \<chi>2)
\<lbrakk>?\<phi> \<in> fmla; ?\<chi> \<in> fmla; prv (imp ?\<phi> ?\<chi>); prv ?\<phi>\<rbrakk> \<Longrightarrow> prv ?\<chi>
\<lbrakk>?\<phi>1.0 \<in> fmla; ?\<phi>2.0 \<in> fmla; ?\<chi>1.0 \<in> fmla; ?\<chi>2.0 \<in> fmla\<rbrakk> \<Longrightarrow> prv (imp (eqv ?\<phi>1.0 ?\<phi>2.0) (imp (eqv ?\<chi>1.0 ?\<chi>2.0) (eqv (cnj ?\<phi>1.0 ?\<chi>1.0) (cnj ?\<phi>2.0 ?\<chi>2.0))))

goal (1 subgoal):
 1. prv (eqv (cnj \<phi>1 \<chi>1) (cnj \<phi>2 \<chi>2))
[PROOF STEP]
by (metis eqv imp cnj)


[STATEMENT]
lemma prv_eqv_prv:
  assumes "\<phi> \<in> fmla" and "\<chi> \<in> fmla"
  assumes "prv \<phi>" and "prv (eqv \<phi> \<chi>)"
  shows "prv \<chi>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv \<chi>
[PROOF STEP]
by (metis assms prv_imp_cnjL prv_imp_mp eqv eqv_def imp)


[STATEMENT]
lemma prv_eqv_prv_rev:
  assumes "\<phi> \<in> fmla" and "\<chi> \<in> fmla"
  assumes "prv \<phi>" and "prv (eqv \<chi> \<phi>)"
  shows "prv \<chi>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv \<chi>
[PROOF STEP]
using assms prv_eqv_prv prv_eqv_sym
[PROOF STATE]
proof (prove)
using this:
\<phi> \<in> fmla
\<chi> \<in> fmla
prv \<phi>
prv (eqv \<chi> \<phi>)
\<lbrakk>?\<phi> \<in> fmla; ?\<chi> \<in> fmla; prv ?\<phi>; prv (eqv ?\<phi> ?\<chi>)\<rbrakk> \<Longrightarrow> prv ?\<chi>
\<lbrakk>?\<phi> \<in> fmla; ?\<chi> \<in> fmla; prv (eqv ?\<phi> ?\<chi>)\<rbrakk> \<Longrightarrow> prv (eqv ?\<chi> ?\<phi>)

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


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


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


[STATEMENT]
lemma prv_eqv_imp_transi:
assumes "\<phi>1 \<in> fmla" and "\<phi>2 \<in> fmla" and "\<chi> \<in> fmla"
assumes "prv (eqv \<phi>1 \<phi>2)" and "prv (imp \<phi>2 \<chi>)"
shows "prv (imp \<phi>1 \<chi>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (imp \<phi>1 \<chi>)
[PROOF STEP]
by (meson assms prv_imp_eqv_transi prv_imp_refl prv_prv_imp_trans)


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


[STATEMENT]
lemma prv_imp_monoL: "\<phi> \<in> fmla \<Longrightarrow> \<chi> \<in> fmla \<Longrightarrow> \<psi> \<in> fmla \<Longrightarrow>
prv (imp \<chi> \<psi>) \<Longrightarrow> prv (imp (imp \<phi> \<chi>) (imp \<phi> \<psi>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<phi> \<in> fmla; \<chi> \<in> fmla; \<psi> \<in> fmla; prv (imp \<chi> \<psi>)\<rbrakk> \<Longrightarrow> prv (imp (imp \<phi> \<chi>) (imp \<phi> \<psi>))
[PROOF STEP]
by (meson imp prv_imp_mp prv_imp_trans1)


[STATEMENT]
lemma prv_imp_monoR: "\<phi> \<in> fmla \<Longrightarrow> \<chi> \<in> fmla \<Longrightarrow> \<psi> \<in> fmla \<Longrightarrow>
prv (imp \<psi> \<chi>) \<Longrightarrow> prv (imp (imp \<chi> \<phi>) (imp \<psi> \<phi>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<phi> \<in> fmla; \<chi> \<in> fmla; \<psi> \<in> fmla; prv (imp \<psi> \<chi>)\<rbrakk> \<Longrightarrow> prv (imp (imp \<chi> \<phi>) (imp \<psi> \<phi>))
[PROOF STEP]
by (meson imp prv_imp_mp prv_imp_trans2)


[STATEMENT]
lemma prv_cnj_com_imp:
 assumes \<phi>[simp]: "\<phi> \<in> fmla" and \<chi>[simp]: "\<chi> \<in> fmla"
 shows "prv (imp (cnj \<phi> \<chi>) (cnj \<chi> \<phi>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (imp (cnj \<phi> \<chi>) (cnj \<chi> \<phi>))
[PROOF STEP]
by (simp add: prv_imp_cnj prv_imp_cnjL prv_imp_cnjR)


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


[STATEMENT]
lemma prv_cnj_assoc_imp1:
 assumes \<phi>[simp]: "\<phi> \<in> fmla" and \<chi>[simp]: "\<chi> \<in> fmla" and \<psi>[simp]: "\<psi> \<in> fmla"
 shows "prv (imp (cnj \<phi> (cnj \<chi> \<psi>)) (cnj (cnj \<phi> \<chi>) \<psi>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (imp (cnj \<phi> (cnj \<chi> \<psi>)) (cnj (cnj \<phi> \<chi>) \<psi>))
[PROOF STEP]
by (simp add: prv_cnj_imp_monoR2 prv_imp_cnj prv_imp_cnjL prv_imp_cnjR prv_imp_triv)


[STATEMENT]
lemma prv_cnj_assoc_imp2:
 assumes \<phi>[simp]: "\<phi> \<in> fmla" and \<chi>[simp]: "\<chi> \<in> fmla" and \<psi>[simp]: "\<psi> \<in> fmla"
 shows "prv (imp (cnj (cnj \<phi> \<chi>) \<psi>) (cnj \<phi> (cnj \<chi> \<psi>)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (imp (cnj (cnj \<phi> \<chi>) \<psi>) (cnj \<phi> (cnj \<chi> \<psi>)))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. prv (imp (cnj (cnj \<phi> \<chi>) \<psi>) (cnj \<phi> (cnj \<chi> \<psi>)))
[PROOF STEP]
have "prv (imp (cnj \<phi> \<chi>) (imp \<psi> \<phi>)) \<and> cnj \<chi> \<psi> \<in> fmla \<and> cnj \<phi> \<chi> \<in> fmla"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (imp (cnj \<phi> \<chi>) (imp \<psi> \<phi>)) \<and> cnj \<chi> \<psi> \<in> fmla \<and> cnj \<phi> \<chi> \<in> fmla
[PROOF STEP]
by (meson \<chi> \<phi> \<psi> cnj imp prv_cnj_imp_monoR2 prv_imp_imp_triv prv_prv_imp_trans)
[PROOF STATE]
proof (state)
this:
prv (imp (cnj \<phi> \<chi>) (imp \<psi> \<phi>)) \<and> cnj \<chi> \<psi> \<in> fmla \<and> cnj \<phi> \<chi> \<in> fmla

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

goal (1 subgoal):
 1. prv (imp (cnj (cnj \<phi> \<chi>) \<psi>) (cnj \<phi> (cnj \<chi> \<psi>)))
[PROOF STEP]
using \<chi> \<phi> \<psi> cnj imp prv_cnj_imp_monoR2 prv_imp_cnj4 prv_imp_cnjI prv_imp_triv
[PROOF STATE]
proof (prove)
using this:
prv (imp (cnj \<phi> \<chi>) (imp \<psi> \<phi>)) \<and> cnj \<chi> \<psi> \<in> fmla \<and> cnj \<phi> \<chi> \<in> fmla
\<chi> \<in> fmla
\<phi> \<in> fmla
\<psi> \<in> fmla
\<lbrakk>?\<phi>1.0 \<in> fmla; ?\<phi>2.0 \<in> fmla\<rbrakk> \<Longrightarrow> cnj ?\<phi>1.0 ?\<phi>2.0 \<in> fmla
\<lbrakk>?\<phi>1.0 \<in> fmla; ?\<phi>2.0 \<in> fmla\<rbrakk> \<Longrightarrow> imp ?\<phi>1.0 ?\<phi>2.0 \<in> fmla
\<lbrakk>?\<phi> \<in> fmla; ?\<chi> \<in> fmla; ?\<psi> \<in> fmla; prv (imp ?\<phi> (imp ?\<chi> ?\<psi>))\<rbrakk> \<Longrightarrow> prv (imp (cnj ?\<phi> ?\<chi>) ?\<psi>)
\<lbrakk>?\<phi> \<in> fmla; ?\<chi> \<in> fmla; ?\<psi>1.0 \<in> fmla; ?\<psi>2.0 \<in> fmla; prv (imp ?\<phi> (imp ?\<chi> ?\<psi>1.0)); prv (imp ?\<phi> (imp ?\<chi> ?\<psi>2.0))\<rbrakk> \<Longrightarrow> prv (imp ?\<phi> (imp ?\<chi> (cnj ?\<psi>1.0 ?\<psi>2.0)))
\<lbrakk>?\<phi> \<in> fmla; ?\<chi> \<in> fmla\<rbrakk> \<Longrightarrow> prv (imp ?\<phi> (imp ?\<chi> (cnj ?\<phi> ?\<chi>)))
\<lbrakk>?\<phi> \<in> fmla; ?\<psi> \<in> fmla; prv ?\<psi>\<rbrakk> \<Longrightarrow> prv (imp ?\<phi> ?\<psi>)

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

goal:
No subgoals!
[PROOF STEP]
qed


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


[STATEMENT]
lemma prv_cnj_com_imp3:
  assumes "\<phi>1 \<in> fmla" "\<phi>2 \<in> fmla" "\<phi>3 \<in> fmla"
  shows "prv (imp (cnj \<phi>1 (cnj \<phi>2 \<phi>3))
                (cnj \<phi>2 (cnj \<phi>1 \<phi>3)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (imp (cnj \<phi>1 (cnj \<phi>2 \<phi>3)) (cnj \<phi>2 (cnj \<phi>1 \<phi>3)))
[PROOF STEP]
by (simp add: assms prv_cnj_imp_monoR2 prv_imp_cnj prv_imp_cnjL prv_imp_refl prv_imp_triv)


[STATEMENT]
lemma prv_allE:
  assumes "x \<in> var" and "\<phi> \<in> fmla" and "t \<in> trm"
  shows "prv (all x \<phi>) \<Longrightarrow> prv (subst \<phi> t x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (all x \<phi>) \<Longrightarrow> prv (subst \<phi> t x)
[PROOF STEP]
using assms prv_all_inst prv_imp_mp
[PROOF STATE]
proof (prove)
using this:
x \<in> var
\<phi> \<in> fmla
t \<in> trm
\<lbrakk>?x \<in> var; ?\<phi> \<in> fmla; ?t \<in> trm\<rbrakk> \<Longrightarrow> prv (imp (all ?x ?\<phi>) (subst ?\<phi> ?t ?x))
\<lbrakk>?\<phi> \<in> fmla; ?\<chi> \<in> fmla; prv (imp ?\<phi> ?\<chi>); prv ?\<phi>\<rbrakk> \<Longrightarrow> prv ?\<chi>

goal (1 subgoal):
 1. prv (all x \<phi>) \<Longrightarrow> prv (subst \<phi> t x)
[PROOF STEP]
by (meson subst all)


[STATEMENT]
lemma prv_exiI:
  assumes "x \<in> var" and "\<phi> \<in> fmla" and "t \<in> trm"
  shows "prv (subst \<phi> t x) \<Longrightarrow> prv (exi x \<phi>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (subst \<phi> t x) \<Longrightarrow> prv (exi x \<phi>)
[PROOF STEP]
using assms prv_exi_inst prv_imp_mp
[PROOF STATE]
proof (prove)
using this:
x \<in> var
\<phi> \<in> fmla
t \<in> trm
\<lbrakk>?x \<in> var; ?\<phi> \<in> fmla; ?t \<in> trm\<rbrakk> \<Longrightarrow> prv (imp (subst ?\<phi> ?t ?x) (exi ?x ?\<phi>))
\<lbrakk>?\<phi> \<in> fmla; ?\<chi> \<in> fmla; prv (imp ?\<phi> ?\<chi>); prv ?\<phi>\<rbrakk> \<Longrightarrow> prv ?\<chi>

goal (1 subgoal):
 1. prv (subst \<phi> t x) \<Longrightarrow> prv (exi x \<phi>)
[PROOF STEP]
by (meson subst exi)


[STATEMENT]
lemma prv_imp_imp_exi:
  assumes "x \<in> var" and "\<phi> \<in> fmla" and "\<chi> \<in> fmla"
  assumes "x \<notin> Fvars \<phi>"
  shows "prv (imp (exi x (imp \<phi> \<chi>)) (imp \<phi> (exi x \<chi>)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (imp (exi x (imp \<phi> \<chi>)) (imp \<phi> (exi x \<chi>)))
[PROOF STEP]
using assms imp exi Fvars_exi Fvars_imp Un_iff assms prv_exi_imp_gen prv_exi_inst prv_imp_mp
    prv_imp_trans1 member_remove remove_def subst_same_Var
[PROOF STATE]
proof (prove)
using this:
x \<in> var
\<phi> \<in> fmla
\<chi> \<in> fmla
x \<notin> Fvars \<phi>
\<lbrakk>?\<phi>1.0 \<in> fmla; ?\<phi>2.0 \<in> fmla\<rbrakk> \<Longrightarrow> imp ?\<phi>1.0 ?\<phi>2.0 \<in> fmla
\<lbrakk>?x \<in> var; ?\<phi> \<in> fmla\<rbrakk> \<Longrightarrow> exi ?x ?\<phi> \<in> fmla
\<lbrakk>?x \<in> var; ?\<phi> \<in> fmla\<rbrakk> \<Longrightarrow> Fvars (exi ?x ?\<phi>) = Fvars ?\<phi> - {?x}
\<lbrakk>?\<phi> \<in> fmla; ?\<chi> \<in> fmla\<rbrakk> \<Longrightarrow> Fvars (imp ?\<phi> ?\<chi>) = Fvars ?\<phi> \<union> Fvars ?\<chi>
(?c \<in> ?A \<union> ?B) = (?c \<in> ?A \<or> ?c \<in> ?B)
x \<in> var
\<phi> \<in> fmla
\<chi> \<in> fmla
x \<notin> Fvars \<phi>
\<lbrakk>?x \<in> var; ?\<phi> \<in> fmla; ?\<chi> \<in> fmla; ?x \<notin> Fvars ?\<chi>; prv (imp ?\<phi> ?\<chi>)\<rbrakk> \<Longrightarrow> prv (imp (exi ?x ?\<phi>) ?\<chi>)
\<lbrakk>?x \<in> var; ?\<phi> \<in> fmla; ?t \<in> trm\<rbrakk> \<Longrightarrow> prv (imp (subst ?\<phi> ?t ?x) (exi ?x ?\<phi>))
\<lbrakk>?\<phi> \<in> fmla; ?\<chi> \<in> fmla; prv (imp ?\<phi> ?\<chi>); prv ?\<phi>\<rbrakk> \<Longrightarrow> prv ?\<chi>
\<lbrakk>?\<phi> \<in> fmla; ?\<chi> \<in> fmla; ?\<psi> \<in> fmla\<rbrakk> \<Longrightarrow> prv (imp (imp ?\<chi> ?\<psi>) (imp (imp ?\<phi> ?\<chi>) (imp ?\<phi> ?\<psi>)))
(?x \<in> Set.remove ?y ?A) = (?x \<in> ?A \<and> ?x \<noteq> ?y)
Set.remove ?x ?A = ?A - {?x}
\<lbrakk>?\<phi> \<in> fmla; ?x \<in> var\<rbrakk> \<Longrightarrow> subst ?\<phi> (Var ?x) ?x = ?\<phi>

goal (1 subgoal):
 1. prv (imp (exi x (imp \<phi> \<chi>)) (imp \<phi> (exi x \<chi>)))
[PROOF STEP]
by (metis (full_types) Var)


[STATEMENT]
lemma prv_imp_exi:
  assumes "x \<in> var" and "\<phi> \<in> fmla" and "\<chi> \<in> fmla"
  shows "x \<notin> Fvars \<phi> \<Longrightarrow> prv (exi x (imp \<phi> \<chi>)) \<Longrightarrow> prv (imp \<phi> (exi x \<chi>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<notin> Fvars \<phi>; prv (exi x (imp \<phi> \<chi>))\<rbrakk> \<Longrightarrow> prv (imp \<phi> (exi x \<chi>))
[PROOF STEP]
using assms prv_imp_imp_exi prv_imp_mp
[PROOF STATE]
proof (prove)
using this:
x \<in> var
\<phi> \<in> fmla
\<chi> \<in> fmla
\<lbrakk>?x \<in> var; ?\<phi> \<in> fmla; ?\<chi> \<in> fmla; ?x \<notin> Fvars ?\<phi>\<rbrakk> \<Longrightarrow> prv (imp (exi ?x (imp ?\<phi> ?\<chi>)) (imp ?\<phi> (exi ?x ?\<chi>)))
\<lbrakk>?\<phi> \<in> fmla; ?\<chi> \<in> fmla; prv (imp ?\<phi> ?\<chi>); prv ?\<phi>\<rbrakk> \<Longrightarrow> prv ?\<chi>

goal (1 subgoal):
 1. \<lbrakk>x \<notin> Fvars \<phi>; prv (exi x (imp \<phi> \<chi>))\<rbrakk> \<Longrightarrow> prv (imp \<phi> (exi x \<chi>))
[PROOF STEP]
by (meson exi imp)


[STATEMENT]
lemma prv_exi_imp:
  assumes x: "x \<in> var" and "\<phi> \<in> fmla" and "\<chi> \<in> fmla"
  assumes "x \<notin> Fvars \<chi>" and d: "prv (all x (imp \<phi> \<chi>))"
  shows "prv (imp (exi x \<phi>) \<chi>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (imp (exi x \<phi>) \<chi>)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. prv (imp (exi x \<phi>) \<chi>)
[PROOF STEP]
have "prv (imp \<phi> \<chi>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (imp \<phi> \<chi>)
[PROOF STEP]
using prv_allE[of x _ "Var x", of "imp \<phi> \<chi>"] assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>x \<in> var; imp \<phi> \<chi> \<in> fmla; Var x \<in> trm; prv (all x (imp \<phi> \<chi>))\<rbrakk> \<Longrightarrow> prv (subst (imp \<phi> \<chi>) (Var x) x)
x \<in> var
\<phi> \<in> fmla
\<chi> \<in> fmla
x \<notin> Fvars \<chi>
prv (all x (imp \<phi> \<chi>))

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

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

goal (1 subgoal):
 1. prv (imp (exi x \<phi>) \<chi>)
[PROOF STEP]
using assms prv_exi_imp_gen
[PROOF STATE]
proof (prove)
using this:
prv (imp \<phi> \<chi>)
x \<in> var
\<phi> \<in> fmla
\<chi> \<in> fmla
x \<notin> Fvars \<chi>
prv (all x (imp \<phi> \<chi>))
\<lbrakk>?x \<in> var; ?\<phi> \<in> fmla; ?\<chi> \<in> fmla; ?x \<notin> Fvars ?\<chi>; prv (imp ?\<phi> ?\<chi>)\<rbrakk> \<Longrightarrow> prv (imp (exi ?x ?\<phi>) ?\<chi>)

goal (1 subgoal):
 1. prv (imp (exi x \<phi>) \<chi>)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
prv (imp (exi x \<phi>) \<chi>)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma prv_all_imp:
  assumes x: "x \<in> var" and "\<phi> \<in> fmla" and "\<chi> \<in> fmla"
  assumes "x \<notin> Fvars \<phi>" and "prv (all x (imp \<phi> \<chi>))"
  shows "prv (imp \<phi> (all x \<chi>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (imp \<phi> (all x \<chi>))
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. prv (imp \<phi> (all x \<chi>))
[PROOF STEP]
have "prv (imp \<phi> \<chi>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (imp \<phi> \<chi>)
[PROOF STEP]
using prv_allE[of x _ "Var x", of "imp \<phi> \<chi>"] assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>x \<in> var; imp \<phi> \<chi> \<in> fmla; Var x \<in> trm; prv (all x (imp \<phi> \<chi>))\<rbrakk> \<Longrightarrow> prv (subst (imp \<phi> \<chi>) (Var x) x)
x \<in> var
\<phi> \<in> fmla
\<chi> \<in> fmla
x \<notin> Fvars \<phi>
prv (all x (imp \<phi> \<chi>))

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

goal (1 subgoal):
 1. prv (imp \<phi> (all x \<chi>))
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
prv (imp \<phi> \<chi>)

goal (1 subgoal):
 1. prv (imp \<phi> (all x \<chi>))
[PROOF STEP]
using assms prv_all_imp_gen
[PROOF STATE]
proof (prove)
using this:
prv (imp \<phi> \<chi>)
x \<in> var
\<phi> \<in> fmla
\<chi> \<in> fmla
x \<notin> Fvars \<phi>
prv (all x (imp \<phi> \<chi>))
\<lbrakk>?x \<notin> Fvars ?\<phi>; prv (imp ?\<phi> ?\<chi>)\<rbrakk> \<Longrightarrow> prv (imp ?\<phi> (all ?x ?\<chi>))

goal (1 subgoal):
 1. prv (imp \<phi> (all x \<chi>))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
prv (imp \<phi> (all x \<chi>))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma prv_exi_inst_same:
  assumes "\<phi> \<in> fmla" "\<chi> \<in> fmla" "x \<in> var"
  shows "prv (imp \<phi> (exi x \<phi>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (imp \<phi> (exi x \<phi>))
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. prv (imp \<phi> (exi x \<phi>))
[PROOF STEP]
have 0: "\<phi> = subst \<phi> (Var x) x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<phi> = subst \<phi> (Var x) x
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<phi> \<in> fmla
\<chi> \<in> fmla
x \<in> var

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

goal (1 subgoal):
 1. prv (imp \<phi> (exi x \<phi>))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (imp \<phi> (exi x \<phi>))
[PROOF STEP]
apply(subst 0)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (imp (subst \<phi> (Var x) x) (exi x \<phi>))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<phi> \<in> fmla
\<chi> \<in> fmla
x \<in> var

goal (1 subgoal):
 1. prv (imp (subst \<phi> (Var x) x) (exi x \<phi>))
[PROOF STEP]
by (intro prv_exi_inst) auto
[PROOF STATE]
proof (state)
this:
prv (imp \<phi> (exi x \<phi>))

goal:
No subgoals!
[PROOF STEP]
qed