[STATEMENT]
lemma prv_exi_cong:
  assumes "\<phi> \<in> fmla" "\<chi> \<in> fmla" "x \<in> var"
    and "prv (imp \<phi> \<chi>)"
  shows "prv (imp (exi x \<phi>) (exi x \<chi>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (imp (exi x \<phi>) (exi x \<chi>))
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. prv (imp (exi x \<phi>) (exi x \<chi>))
[PROOF STEP]
have 0: "prv (imp \<chi> (exi x \<chi>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (imp \<chi> (exi x \<chi>))
[PROOF STEP]
using assms prv_exi_inst_same
[PROOF STATE]
proof (prove)
using this:
\<phi> \<in> fmla
\<chi> \<in> fmla
x \<in> var
prv (imp \<phi> \<chi>)
\<lbrakk>?\<phi> \<in> fmla; ?\<chi> \<in> fmla; ?x \<in> var\<rbrakk> \<Longrightarrow> prv (imp ?\<phi> (exi ?x ?\<phi>))

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

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

goal (1 subgoal):
 1. prv (imp (exi x \<phi>) (exi x \<chi>))
[PROOF STEP]
apply(intro prv_exi_imp_gen)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<lbrakk>\<phi> \<in> fmla; \<chi> \<in> fmla; x \<in> var; prv (imp \<phi> \<chi>)\<rbrakk> \<Longrightarrow> x \<in> var
 2. \<lbrakk>\<phi> \<in> fmla; \<chi> \<in> fmla; x \<in> var; prv (imp \<phi> \<chi>)\<rbrakk> \<Longrightarrow> \<phi> \<in> fmla
 3. \<lbrakk>\<phi> \<in> fmla; \<chi> \<in> fmla; x \<in> var; prv (imp \<phi> \<chi>)\<rbrakk> \<Longrightarrow> exi x \<chi> \<in> fmla
 4. \<lbrakk>\<phi> \<in> fmla; \<chi> \<in> fmla; x \<in> var; prv (imp \<phi> \<chi>)\<rbrakk> \<Longrightarrow> x \<notin> Fvars (exi x \<chi>)
 5. \<lbrakk>\<phi> \<in> fmla; \<chi> \<in> fmla; x \<in> var; prv (imp \<phi> \<chi>)\<rbrakk> \<Longrightarrow> prv (imp \<phi> (exi x \<chi>))
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<phi> \<in> fmla; \<chi> \<in> fmla; x \<in> var; prv (imp \<phi> \<chi>)\<rbrakk> \<Longrightarrow> x \<in> var
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>\<phi> \<in> fmla; \<chi> \<in> fmla; x \<in> var; prv (imp \<phi> \<chi>)\<rbrakk> \<Longrightarrow> \<phi> \<in> fmla
 2. \<lbrakk>\<phi> \<in> fmla; \<chi> \<in> fmla; x \<in> var; prv (imp \<phi> \<chi>)\<rbrakk> \<Longrightarrow> exi x \<chi> \<in> fmla
 3. \<lbrakk>\<phi> \<in> fmla; \<chi> \<in> fmla; x \<in> var; prv (imp \<phi> \<chi>)\<rbrakk> \<Longrightarrow> x \<notin> Fvars (exi x \<chi>)
 4. \<lbrakk>\<phi> \<in> fmla; \<chi> \<in> fmla; x \<in> var; prv (imp \<phi> \<chi>)\<rbrakk> \<Longrightarrow> prv (imp \<phi> (exi x \<chi>))
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<phi> \<in> fmla; \<chi> \<in> fmla; x \<in> var; prv (imp \<phi> \<chi>)\<rbrakk> \<Longrightarrow> \<phi> \<in> fmla
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>\<phi> \<in> fmla; \<chi> \<in> fmla; x \<in> var; prv (imp \<phi> \<chi>)\<rbrakk> \<Longrightarrow> exi x \<chi> \<in> fmla
 2. \<lbrakk>\<phi> \<in> fmla; \<chi> \<in> fmla; x \<in> var; prv (imp \<phi> \<chi>)\<rbrakk> \<Longrightarrow> x \<notin> Fvars (exi x \<chi>)
 3. \<lbrakk>\<phi> \<in> fmla; \<chi> \<in> fmla; x \<in> var; prv (imp \<phi> \<chi>)\<rbrakk> \<Longrightarrow> prv (imp \<phi> (exi x \<chi>))
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<phi> \<in> fmla; \<chi> \<in> fmla; x \<in> var; prv (imp \<phi> \<chi>)\<rbrakk> \<Longrightarrow> exi x \<chi> \<in> fmla
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<phi> \<in> fmla; \<chi> \<in> fmla; x \<in> var; prv (imp \<phi> \<chi>)\<rbrakk> \<Longrightarrow> x \<notin> Fvars (exi x \<chi>)
 2. \<lbrakk>\<phi> \<in> fmla; \<chi> \<in> fmla; x \<in> var; prv (imp \<phi> \<chi>)\<rbrakk> \<Longrightarrow> prv (imp \<phi> (exi x \<chi>))
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<phi> \<in> fmla; \<chi> \<in> fmla; x \<in> var; prv (imp \<phi> \<chi>)\<rbrakk> \<Longrightarrow> x \<notin> Fvars (exi x \<chi>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<phi> \<in> fmla; \<chi> \<in> fmla; x \<in> var; prv (imp \<phi> \<chi>)\<rbrakk> \<Longrightarrow> prv (imp \<phi> (exi x \<chi>))
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<phi> \<in> fmla; \<chi> \<in> fmla; x \<in> var; prv (imp \<phi> \<chi>)\<rbrakk> \<Longrightarrow> prv (imp \<phi> (exi x \<chi>))
[PROOF STEP]
using "0" exi prv_prv_imp_trans
[PROOF STATE]
proof (prove)
using this:
prv (imp \<chi> (exi x \<chi>))
\<lbrakk>?x \<in> var; ?\<phi> \<in> fmla\<rbrakk> \<Longrightarrow> exi ?x ?\<phi> \<in> fmla
\<lbrakk>?\<phi> \<in> fmla; ?\<chi> \<in> fmla; ?\<psi> \<in> fmla; prv (imp ?\<phi> ?\<chi>); prv (imp ?\<chi> ?\<psi>)\<rbrakk> \<Longrightarrow> prv (imp ?\<phi> ?\<psi>)

goal (1 subgoal):
 1. \<lbrakk>\<phi> \<in> fmla; \<chi> \<in> fmla; x \<in> var; prv (imp \<phi> \<chi>)\<rbrakk> \<Longrightarrow> prv (imp \<phi> (exi x \<chi>))
[PROOF STEP]
by blast
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
prv (imp (exi x \<phi>) (exi x \<chi>))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma prv_exi_congW:
  assumes "\<phi> \<in> fmla" "\<chi> \<in> fmla" "x \<in> var"
    and "prv (imp \<phi> \<chi>)" "prv (exi x \<phi>)"
  shows "prv (exi x \<chi>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (exi x \<chi>)
[PROOF STEP]
by (meson exi assms prv_exi_cong prv_imp_mp)


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

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

goal (1 subgoal):
 1. prv (imp (all x \<phi>) (all x \<chi>))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (imp (all x \<phi>) (all x \<chi>))
[PROOF STEP]
by (simp add: "0" assms prv_all_imp_gen)
[PROOF STATE]
proof (state)
this:
prv (imp (all x \<phi>) (all x \<chi>))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma prv_all_congW:
  assumes "\<phi> \<in> fmla" "\<chi> \<in> fmla" "x \<in> var"
    and "prv (imp \<phi> \<chi>)" "prv (all x \<phi>)"
  shows "prv (all x \<chi>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (all x \<chi>)
[PROOF STEP]
by (meson all assms prv_all_cong prv_imp_mp)


[STATEMENT]
lemma exists_no_Fvars: "\<exists> \<phi>. \<phi> \<in> fmla \<and> prv \<phi> \<and> Fvars \<phi> = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>\<phi>. \<phi> \<in> fmla \<and> prv \<phi> \<and> Fvars \<phi> = {}
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>\<phi>. \<phi> \<in> fmla \<and> prv \<phi> \<and> Fvars \<phi> = {}
[PROOF STEP]
obtain n where [simp]: "n \<in> num"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>n. n \<in> num \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using numNE
[PROOF STATE]
proof (prove)
using this:
num \<noteq> {}

goal (1 subgoal):
 1. (\<And>n. n \<in> num \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
n \<in> num

goal (1 subgoal):
 1. \<exists>\<phi>. \<phi> \<in> fmla \<and> prv \<phi> \<and> Fvars \<phi> = {}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>\<phi>. \<phi> \<in> fmla \<and> prv \<phi> \<and> Fvars \<phi> = {}
[PROOF STEP]
by (intro exI[of _ "imp (eql n n) (eql n n)"]) (simp add: prv_imp_refl)
[PROOF STATE]
proof (state)
this:
\<exists>\<phi>. \<phi> \<in> fmla \<and> prv \<phi> \<and> Fvars \<phi> = {}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma prv_all_gen:
  assumes "x \<in> var" and "\<phi> \<in> fmla"
  assumes "prv \<phi>" shows "prv (all x \<phi>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (all x \<phi>)
[PROOF STEP]
using assms prv_all_imp_gen prv_imp_mp prv_imp_triv exists_no_Fvars
[PROOF STATE]
proof (prove)
using this:
x \<in> var
\<phi> \<in> fmla
prv \<phi>
\<lbrakk>?x \<notin> Fvars ?\<phi>; prv (imp ?\<phi> ?\<chi>)\<rbrakk> \<Longrightarrow> prv (imp ?\<phi> (all ?x ?\<chi>))
\<lbrakk>?\<phi> \<in> fmla; ?\<chi> \<in> fmla; prv (imp ?\<phi> ?\<chi>); prv ?\<phi>\<rbrakk> \<Longrightarrow> prv ?\<chi>
\<lbrakk>?\<phi> \<in> fmla; ?\<psi> \<in> fmla; prv ?\<psi>\<rbrakk> \<Longrightarrow> prv (imp ?\<phi> ?\<psi>)
\<exists>\<phi>. \<phi> \<in> fmla \<and> prv \<phi> \<and> Fvars \<phi> = {}

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


[STATEMENT]
lemma all_subst_rename_prv:
  "\<phi> \<in> fmla \<Longrightarrow> x \<in> var \<Longrightarrow> y \<in> var \<Longrightarrow>
   y \<notin> Fvars \<phi> \<Longrightarrow> prv (all x \<phi>) \<Longrightarrow> prv (all y (subst \<phi> (Var y) x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<phi> \<in> fmla; x \<in> var; y \<in> var; y \<notin> Fvars \<phi>; prv (all x \<phi>)\<rbrakk> \<Longrightarrow> prv (all y (subst \<phi> (Var y) x))
[PROOF STEP]
by (simp add: prv_allE prv_all_gen)


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

goal (1 subgoal):
 1. prv \<phi>
[PROOF STEP]
by (metis Var subst_same_Var)


[STATEMENT]
lemma prv_subst:
  assumes "x \<in> var" and "\<phi> \<in> fmla" and "t \<in> trm"
  shows "prv \<phi> \<Longrightarrow> prv (subst \<phi> t x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv \<phi> \<Longrightarrow> prv (subst \<phi> t x)
[PROOF STEP]
by (simp add: assms prv_allE prv_all_gen)


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

goal (1 subgoal):
 1. prv (rawpsubst \<phi> txs)
[PROOF STEP]
apply (induct txs arbitrary: \<phi>)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>\<phi>. \<lbrakk>\<phi> \<in> fmla; snd ` set [] \<subseteq> var; fst ` set [] \<subseteq> trm; prv \<phi>\<rbrakk> \<Longrightarrow> prv (rawpsubst \<phi> [])
 2. \<And>a txs \<phi>. \<lbrakk>\<And>\<phi>. \<lbrakk>\<phi> \<in> fmla; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; prv \<phi>\<rbrakk> \<Longrightarrow> prv (rawpsubst \<phi> txs); \<phi> \<in> fmla; snd ` set (a # txs) \<subseteq> var; fst ` set (a # txs) \<subseteq> trm; prv \<phi>\<rbrakk> \<Longrightarrow> prv (rawpsubst \<phi> (a # txs))
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<phi>_ \<in> fmla; snd ` set [] \<subseteq> var; fst ` set [] \<subseteq> trm; prv \<phi>_\<rbrakk> \<Longrightarrow> prv (rawpsubst \<phi>_ [])
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a txs \<phi>. \<lbrakk>\<And>\<phi>. \<lbrakk>\<phi> \<in> fmla; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; prv \<phi>\<rbrakk> \<Longrightarrow> prv (rawpsubst \<phi> txs); \<phi> \<in> fmla; snd ` set (a # txs) \<subseteq> var; fst ` set (a # txs) \<subseteq> trm; prv \<phi>\<rbrakk> \<Longrightarrow> prv (rawpsubst \<phi> (a # txs))
[PROOF STEP]
subgoal for tx txs \<phi>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>\<phi>. \<lbrakk>\<phi> \<in> fmla; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; prv \<phi>\<rbrakk> \<Longrightarrow> prv (rawpsubst \<phi> txs); \<phi> \<in> fmla; snd ` set (tx # txs) \<subseteq> var; fst ` set (tx # txs) \<subseteq> trm; prv \<phi>\<rbrakk> \<Longrightarrow> prv (rawpsubst \<phi> (tx # txs))
[PROOF STEP]
by (cases tx) (auto intro: prv_subst)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
.


[STATEMENT]
lemma prv_psubst:
  assumes "\<phi> \<in> fmla" and "snd ` (set txs) \<subseteq> var" and "fst ` (set txs) \<subseteq> trm"
    and "prv \<phi>"
  shows "prv (psubst \<phi> txs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (psubst \<phi> txs)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. prv (psubst \<phi> txs)
[PROOF STEP]
define us where us: "us \<equiv> getFrN (map snd txs) (map fst txs) [\<phi>] (length txs)"
[PROOF STATE]
proof (state)
this:
us \<equiv> getFrN (map snd txs) (map fst txs) [\<phi>] (length txs)

goal (1 subgoal):
 1. prv (psubst \<phi> txs)
[PROOF STEP]
have us_facts: "set us \<subseteq> var"
    "set us \<inter> Fvars \<phi> = {}"
    "set us \<inter> \<Union> (FvarsT ` (fst ` (set txs))) = {}"
    "set us \<inter> snd ` (set txs) = {}"
    "length us = length txs"
    "distinct us"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (set us \<subseteq> var &&& set us \<inter> Fvars \<phi> = {} &&& set us \<inter> \<Union> (FvarsT ` fst ` set txs) = {}) &&& set us \<inter> snd ` set txs = {} &&& length us = length txs &&& distinct us
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<phi> \<in> fmla
snd ` set txs \<subseteq> var
fst ` set txs \<subseteq> trm
prv \<phi>

goal (1 subgoal):
 1. (set us \<subseteq> var &&& set us \<inter> Fvars \<phi> = {} &&& set us \<inter> \<Union> (FvarsT ` fst ` set txs) = {}) &&& set us \<inter> snd ` set txs = {} &&& length us = length txs &&& distinct us
[PROOF STEP]
unfolding us
[PROOF STATE]
proof (prove)
using this:
\<phi> \<in> fmla
snd ` set txs \<subseteq> var
fst ` set txs \<subseteq> trm
prv \<phi>

goal (1 subgoal):
 1. (set (getFrN (map snd txs) (map fst txs) [\<phi>] (length txs)) \<subseteq> var &&& set (getFrN (map snd txs) (map fst txs) [\<phi>] (length txs)) \<inter> Fvars \<phi> = {} &&& set (getFrN (map snd txs) (map fst txs) [\<phi>] (length txs)) \<inter> \<Union> (FvarsT ` fst ` set txs) = {}) &&& set (getFrN (map snd txs) (map fst txs) [\<phi>] (length txs)) \<inter> snd ` set txs = {} &&& length (getFrN (map snd txs) (map fst txs) [\<phi>] (length txs)) = length txs &&& distinct (getFrN (map snd txs) (map fst txs) [\<phi>] (length txs))
[PROOF STEP]
using getFrN_FvarsT[of "map snd txs" "map fst txs" "[\<phi>]" _ "length txs"]
      getFrN_Fvars[of "map snd txs" "map fst txs" "[\<phi>]" _ "length txs"]
      getFrN_var[of "map snd txs" "map fst txs" "[\<phi>]" _ "length txs"]
      getFrN_length[of "map snd txs" "map fst txs" "[\<phi>]" "length txs"]
      getFrN_length[of "map snd txs" "map fst txs" "[\<phi>]" "length txs"]
[PROOF STATE]
proof (prove)
using this:
\<phi> \<in> fmla
snd ` set txs \<subseteq> var
fst ` set txs \<subseteq> trm
prv \<phi>
\<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [\<phi>] \<subseteq> fmla; ?t \<in> set (map fst txs)\<rbrakk> \<Longrightarrow> set (getFrN (map snd txs) (map fst txs) [\<phi>] (length txs)) \<inter> FvarsT ?t = {}
\<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [\<phi>] \<subseteq> fmla; ?\<phi> \<in> set [\<phi>]\<rbrakk> \<Longrightarrow> set (getFrN (map snd txs) (map fst txs) [\<phi>] (length txs)) \<inter> Fvars ?\<phi> = {}
\<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [\<phi>] \<subseteq> fmla; ?t \<in> set (map fst txs)\<rbrakk> \<Longrightarrow> set (getFrN (map snd txs) (map fst txs) [\<phi>] (length txs)) \<inter> set (map snd txs) = {}
\<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [\<phi>] \<subseteq> fmla\<rbrakk> \<Longrightarrow> length (getFrN (map snd txs) (map fst txs) [\<phi>] (length txs)) = length txs
\<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [\<phi>] \<subseteq> fmla\<rbrakk> \<Longrightarrow> length (getFrN (map snd txs) (map fst txs) [\<phi>] (length txs)) = length txs

goal (1 subgoal):
 1. (set (getFrN (map snd txs) (map fst txs) [\<phi>] (length txs)) \<subseteq> var &&& set (getFrN (map snd txs) (map fst txs) [\<phi>] (length txs)) \<inter> Fvars \<phi> = {} &&& set (getFrN (map snd txs) (map fst txs) [\<phi>] (length txs)) \<inter> \<Union> (FvarsT ` fst ` set txs) = {}) &&& set (getFrN (map snd txs) (map fst txs) [\<phi>] (length txs)) \<inter> snd ` set txs = {} &&& length (getFrN (map snd txs) (map fst txs) [\<phi>] (length txs)) = length txs &&& distinct (getFrN (map snd txs) (map fst txs) [\<phi>] (length txs))
[PROOF STEP]
apply -
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<lbrakk>\<phi> \<in> fmla; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; prv \<phi>; \<And>t. \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [\<phi>] \<subseteq> fmla; t \<in> set (map fst txs)\<rbrakk> \<Longrightarrow> set (getFrN (map snd txs) (map fst txs) [\<phi>] (length txs)) \<inter> FvarsT t = {}; \<And>\<phi>'. \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [\<phi>] \<subseteq> fmla; \<phi>' \<in> set [\<phi>]\<rbrakk> \<Longrightarrow> set (getFrN (map snd txs) (map fst txs) [\<phi>] (length txs)) \<inter> Fvars \<phi>' = {}; \<And>t. \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [\<phi>] \<subseteq> fmla; t \<in> set (map fst txs)\<rbrakk> \<Longrightarrow> set (getFrN (map snd txs) (map fst txs) [\<phi>] (length txs)) \<inter> set (map snd txs) = {}; \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [\<phi>] \<subseteq> fmla\<rbrakk> \<Longrightarrow> length (getFrN (map snd txs) (map fst txs) [\<phi>] (length txs)) = length txs; \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [\<phi>] \<subseteq> fmla\<rbrakk> \<Longrightarrow> length (getFrN (map snd txs) (map fst txs) [\<phi>] (length txs)) = length txs\<rbrakk> \<Longrightarrow> set (getFrN (map snd txs) (map fst txs) [\<phi>] (length txs)) \<subseteq> var
 2. \<lbrakk>\<phi> \<in> fmla; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; prv \<phi>; \<And>t. \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [\<phi>] \<subseteq> fmla; t \<in> set (map fst txs)\<rbrakk> \<Longrightarrow> set (getFrN (map snd txs) (map fst txs) [\<phi>] (length txs)) \<inter> FvarsT t = {}; \<And>\<phi>'. \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [\<phi>] \<subseteq> fmla; \<phi>' \<in> set [\<phi>]\<rbrakk> \<Longrightarrow> set (getFrN (map snd txs) (map fst txs) [\<phi>] (length txs)) \<inter> Fvars \<phi>' = {}; \<And>t. \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [\<phi>] \<subseteq> fmla; t \<in> set (map fst txs)\<rbrakk> \<Longrightarrow> set (getFrN (map snd txs) (map fst txs) [\<phi>] (length txs)) \<inter> set (map snd txs) = {}; \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [\<phi>] \<subseteq> fmla\<rbrakk> \<Longrightarrow> length (getFrN (map snd txs) (map fst txs) [\<phi>] (length txs)) = length txs; \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [\<phi>] \<subseteq> fmla\<rbrakk> \<Longrightarrow> length (getFrN (map snd txs) (map fst txs) [\<phi>] (length txs)) = length txs\<rbrakk> \<Longrightarrow> set (getFrN (map snd txs) (map fst txs) [\<phi>] (length txs)) \<inter> Fvars \<phi> = {}
 3. \<lbrakk>\<phi> \<in> fmla; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; prv \<phi>; \<And>t. \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [\<phi>] \<subseteq> fmla; t \<in> set (map fst txs)\<rbrakk> \<Longrightarrow> set (getFrN (map snd txs) (map fst txs) [\<phi>] (length txs)) \<inter> FvarsT t = {}; \<And>\<phi>'. \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [\<phi>] \<subseteq> fmla; \<phi>' \<in> set [\<phi>]\<rbrakk> \<Longrightarrow> set (getFrN (map snd txs) (map fst txs) [\<phi>] (length txs)) \<inter> Fvars \<phi>' = {}; \<And>t. \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [\<phi>] \<subseteq> fmla; t \<in> set (map fst txs)\<rbrakk> \<Longrightarrow> set (getFrN (map snd txs) (map fst txs) [\<phi>] (length txs)) \<inter> set (map snd txs) = {}; \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [\<phi>] \<subseteq> fmla\<rbrakk> \<Longrightarrow> length (getFrN (map snd txs) (map fst txs) [\<phi>] (length txs)) = length txs; \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [\<phi>] \<subseteq> fmla\<rbrakk> \<Longrightarrow> length (getFrN (map snd txs) (map fst txs) [\<phi>] (length txs)) = length txs\<rbrakk> \<Longrightarrow> set (getFrN (map snd txs) (map fst txs) [\<phi>] (length txs)) \<inter> \<Union> (FvarsT ` fst ` set txs) = {}
 4. \<lbrakk>\<phi> \<in> fmla; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; prv \<phi>; \<And>t. \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [\<phi>] \<subseteq> fmla; t \<in> set (map fst txs)\<rbrakk> \<Longrightarrow> set (getFrN (map snd txs) (map fst txs) [\<phi>] (length txs)) \<inter> FvarsT t = {}; \<And>\<phi>'. \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [\<phi>] \<subseteq> fmla; \<phi>' \<in> set [\<phi>]\<rbrakk> \<Longrightarrow> set (getFrN (map snd txs) (map fst txs) [\<phi>] (length txs)) \<inter> Fvars \<phi>' = {}; \<And>t. \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [\<phi>] \<subseteq> fmla; t \<in> set (map fst txs)\<rbrakk> \<Longrightarrow> set (getFrN (map snd txs) (map fst txs) [\<phi>] (length txs)) \<inter> set (map snd txs) = {}; \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [\<phi>] \<subseteq> fmla\<rbrakk> \<Longrightarrow> length (getFrN (map snd txs) (map fst txs) [\<phi>] (length txs)) = length txs; \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [\<phi>] \<subseteq> fmla\<rbrakk> \<Longrightarrow> length (getFrN (map snd txs) (map fst txs) [\<phi>] (length txs)) = length txs\<rbrakk> \<Longrightarrow> set (getFrN (map snd txs) (map fst txs) [\<phi>] (length txs)) \<inter> snd ` set txs = {}
 5. \<lbrakk>\<phi> \<in> fmla; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; prv \<phi>; \<And>t. \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [\<phi>] \<subseteq> fmla; t \<in> set (map fst txs)\<rbrakk> \<Longrightarrow> set (getFrN (map snd txs) (map fst txs) [\<phi>] (length txs)) \<inter> FvarsT t = {}; \<And>\<phi>'. \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [\<phi>] \<subseteq> fmla; \<phi>' \<in> set [\<phi>]\<rbrakk> \<Longrightarrow> set (getFrN (map snd txs) (map fst txs) [\<phi>] (length txs)) \<inter> Fvars \<phi>' = {}; \<And>t. \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [\<phi>] \<subseteq> fmla; t \<in> set (map fst txs)\<rbrakk> \<Longrightarrow> set (getFrN (map snd txs) (map fst txs) [\<phi>] (length txs)) \<inter> set (map snd txs) = {}; \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [\<phi>] \<subseteq> fmla\<rbrakk> \<Longrightarrow> length (getFrN (map snd txs) (map fst txs) [\<phi>] (length txs)) = length txs; \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [\<phi>] \<subseteq> fmla\<rbrakk> \<Longrightarrow> length (getFrN (map snd txs) (map fst txs) [\<phi>] (length txs)) = length txs\<rbrakk> \<Longrightarrow> length (getFrN (map snd txs) (map fst txs) [\<phi>] (length txs)) = length txs
 6. \<lbrakk>\<phi> \<in> fmla; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; prv \<phi>; \<And>t. \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [\<phi>] \<subseteq> fmla; t \<in> set (map fst txs)\<rbrakk> \<Longrightarrow> set (getFrN (map snd txs) (map fst txs) [\<phi>] (length txs)) \<inter> FvarsT t = {}; \<And>\<phi>'. \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [\<phi>] \<subseteq> fmla; \<phi>' \<in> set [\<phi>]\<rbrakk> \<Longrightarrow> set (getFrN (map snd txs) (map fst txs) [\<phi>] (length txs)) \<inter> Fvars \<phi>' = {}; \<And>t. \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [\<phi>] \<subseteq> fmla; t \<in> set (map fst txs)\<rbrakk> \<Longrightarrow> set (getFrN (map snd txs) (map fst txs) [\<phi>] (length txs)) \<inter> set (map snd txs) = {}; \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [\<phi>] \<subseteq> fmla\<rbrakk> \<Longrightarrow> length (getFrN (map snd txs) (map fst txs) [\<phi>] (length txs)) = length txs; \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [\<phi>] \<subseteq> fmla\<rbrakk> \<Longrightarrow> length (getFrN (map snd txs) (map fst txs) [\<phi>] (length txs)) = length txs\<rbrakk> \<Longrightarrow> distinct (getFrN (map snd txs) (map fst txs) [\<phi>] (length txs))
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<phi> \<in> fmla; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; prv \<phi>; \<And>t. \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [\<phi>] \<subseteq> fmla; t \<in> set (map fst txs)\<rbrakk> \<Longrightarrow> set (getFrN (map snd txs) (map fst txs) [\<phi>] (length txs)) \<inter> FvarsT t = {}; \<And>\<phi>'. \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [\<phi>] \<subseteq> fmla; \<phi>' \<in> set [\<phi>]\<rbrakk> \<Longrightarrow> set (getFrN (map snd txs) (map fst txs) [\<phi>] (length txs)) \<inter> Fvars \<phi>' = {}; \<And>t. \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [\<phi>] \<subseteq> fmla; t \<in> set (map fst txs)\<rbrakk> \<Longrightarrow> set (getFrN (map snd txs) (map fst txs) [\<phi>] (length txs)) \<inter> set (map snd txs) = {}; \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [\<phi>] \<subseteq> fmla\<rbrakk> \<Longrightarrow> length (getFrN (map snd txs) (map fst txs) [\<phi>] (length txs)) = length txs; \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [\<phi>] \<subseteq> fmla\<rbrakk> \<Longrightarrow> length (getFrN (map snd txs) (map fst txs) [\<phi>] (length txs)) = length txs\<rbrakk> \<Longrightarrow> set (getFrN (map snd txs) (map fst txs) [\<phi>] (length txs)) \<subseteq> var
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<lbrakk>\<phi> \<in> fmla; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; prv \<phi>; \<And>t. \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [\<phi>] \<subseteq> fmla; t \<in> set (map fst txs)\<rbrakk> \<Longrightarrow> set (getFrN (map snd txs) (map fst txs) [\<phi>] (length txs)) \<inter> FvarsT t = {}; \<And>\<phi>'. \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [\<phi>] \<subseteq> fmla; \<phi>' \<in> set [\<phi>]\<rbrakk> \<Longrightarrow> set (getFrN (map snd txs) (map fst txs) [\<phi>] (length txs)) \<inter> Fvars \<phi>' = {}; \<And>t. \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [\<phi>] \<subseteq> fmla; t \<in> set (map fst txs)\<rbrakk> \<Longrightarrow> set (getFrN (map snd txs) (map fst txs) [\<phi>] (length txs)) \<inter> set (map snd txs) = {}; \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [\<phi>] \<subseteq> fmla\<rbrakk> \<Longrightarrow> length (getFrN (map snd txs) (map fst txs) [\<phi>] (length txs)) = length txs; \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [\<phi>] \<subseteq> fmla\<rbrakk> \<Longrightarrow> length (getFrN (map snd txs) (map fst txs) [\<phi>] (length txs)) = length txs\<rbrakk> \<Longrightarrow> set (getFrN (map snd txs) (map fst txs) [\<phi>] (length txs)) \<inter> Fvars \<phi> = {}
 2. \<lbrakk>\<phi> \<in> fmla; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; prv \<phi>; \<And>t. \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [\<phi>] \<subseteq> fmla; t \<in> set (map fst txs)\<rbrakk> \<Longrightarrow> set (getFrN (map snd txs) (map fst txs) [\<phi>] (length txs)) \<inter> FvarsT t = {}; \<And>\<phi>'. \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [\<phi>] \<subseteq> fmla; \<phi>' \<in> set [\<phi>]\<rbrakk> \<Longrightarrow> set (getFrN (map snd txs) (map fst txs) [\<phi>] (length txs)) \<inter> Fvars \<phi>' = {}; \<And>t. \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [\<phi>] \<subseteq> fmla; t \<in> set (map fst txs)\<rbrakk> \<Longrightarrow> set (getFrN (map snd txs) (map fst txs) [\<phi>] (length txs)) \<inter> set (map snd txs) = {}; \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [\<phi>] \<subseteq> fmla\<rbrakk> \<Longrightarrow> length (getFrN (map snd txs) (map fst txs) [\<phi>] (length txs)) = length txs; \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [\<phi>] \<subseteq> fmla\<rbrakk> \<Longrightarrow> length (getFrN (map snd txs) (map fst txs) [\<phi>] (length txs)) = length txs\<rbrakk> \<Longrightarrow> set (getFrN (map snd txs) (map fst txs) [\<phi>] (length txs)) \<inter> \<Union> (FvarsT ` fst ` set txs) = {}
 3. \<lbrakk>\<phi> \<in> fmla; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; prv \<phi>; \<And>t. \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [\<phi>] \<subseteq> fmla; t \<in> set (map fst txs)\<rbrakk> \<Longrightarrow> set (getFrN (map snd txs) (map fst txs) [\<phi>] (length txs)) \<inter> FvarsT t = {}; \<And>\<phi>'. \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [\<phi>] \<subseteq> fmla; \<phi>' \<in> set [\<phi>]\<rbrakk> \<Longrightarrow> set (getFrN (map snd txs) (map fst txs) [\<phi>] (length txs)) \<inter> Fvars \<phi>' = {}; \<And>t. \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [\<phi>] \<subseteq> fmla; t \<in> set (map fst txs)\<rbrakk> \<Longrightarrow> set (getFrN (map snd txs) (map fst txs) [\<phi>] (length txs)) \<inter> set (map snd txs) = {}; \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [\<phi>] \<subseteq> fmla\<rbrakk> \<Longrightarrow> length (getFrN (map snd txs) (map fst txs) [\<phi>] (length txs)) = length txs; \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [\<phi>] \<subseteq> fmla\<rbrakk> \<Longrightarrow> length (getFrN (map snd txs) (map fst txs) [\<phi>] (length txs)) = length txs\<rbrakk> \<Longrightarrow> set (getFrN (map snd txs) (map fst txs) [\<phi>] (length txs)) \<inter> snd ` set txs = {}
 4. \<lbrakk>\<phi> \<in> fmla; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; prv \<phi>; \<And>t. \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [\<phi>] \<subseteq> fmla; t \<in> set (map fst txs)\<rbrakk> \<Longrightarrow> set (getFrN (map snd txs) (map fst txs) [\<phi>] (length txs)) \<inter> FvarsT t = {}; \<And>\<phi>'. \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [\<phi>] \<subseteq> fmla; \<phi>' \<in> set [\<phi>]\<rbrakk> \<Longrightarrow> set (getFrN (map snd txs) (map fst txs) [\<phi>] (length txs)) \<inter> Fvars \<phi>' = {}; \<And>t. \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [\<phi>] \<subseteq> fmla; t \<in> set (map fst txs)\<rbrakk> \<Longrightarrow> set (getFrN (map snd txs) (map fst txs) [\<phi>] (length txs)) \<inter> set (map snd txs) = {}; \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [\<phi>] \<subseteq> fmla\<rbrakk> \<Longrightarrow> length (getFrN (map snd txs) (map fst txs) [\<phi>] (length txs)) = length txs; \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [\<phi>] \<subseteq> fmla\<rbrakk> \<Longrightarrow> length (getFrN (map snd txs) (map fst txs) [\<phi>] (length txs)) = length txs\<rbrakk> \<Longrightarrow> length (getFrN (map snd txs) (map fst txs) [\<phi>] (length txs)) = length txs
 5. \<lbrakk>\<phi> \<in> fmla; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; prv \<phi>; \<And>t. \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [\<phi>] \<subseteq> fmla; t \<in> set (map fst txs)\<rbrakk> \<Longrightarrow> set (getFrN (map snd txs) (map fst txs) [\<phi>] (length txs)) \<inter> FvarsT t = {}; \<And>\<phi>'. \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [\<phi>] \<subseteq> fmla; \<phi>' \<in> set [\<phi>]\<rbrakk> \<Longrightarrow> set (getFrN (map snd txs) (map fst txs) [\<phi>] (length txs)) \<inter> Fvars \<phi>' = {}; \<And>t. \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [\<phi>] \<subseteq> fmla; t \<in> set (map fst txs)\<rbrakk> \<Longrightarrow> set (getFrN (map snd txs) (map fst txs) [\<phi>] (length txs)) \<inter> set (map snd txs) = {}; \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [\<phi>] \<subseteq> fmla\<rbrakk> \<Longrightarrow> length (getFrN (map snd txs) (map fst txs) [\<phi>] (length txs)) = length txs; \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [\<phi>] \<subseteq> fmla\<rbrakk> \<Longrightarrow> length (getFrN (map snd txs) (map fst txs) [\<phi>] (length txs)) = length txs\<rbrakk> \<Longrightarrow> distinct (getFrN (map snd txs) (map fst txs) [\<phi>] (length txs))
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<phi> \<in> fmla; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; prv \<phi>; \<And>t. \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [\<phi>] \<subseteq> fmla; t \<in> set (map fst txs)\<rbrakk> \<Longrightarrow> set (getFrN (map snd txs) (map fst txs) [\<phi>] (length txs)) \<inter> FvarsT t = {}; \<And>\<phi>'. \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [\<phi>] \<subseteq> fmla; \<phi>' \<in> set [\<phi>]\<rbrakk> \<Longrightarrow> set (getFrN (map snd txs) (map fst txs) [\<phi>] (length txs)) \<inter> Fvars \<phi>' = {}; \<And>t. \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [\<phi>] \<subseteq> fmla; t \<in> set (map fst txs)\<rbrakk> \<Longrightarrow> set (getFrN (map snd txs) (map fst txs) [\<phi>] (length txs)) \<inter> set (map snd txs) = {}; \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [\<phi>] \<subseteq> fmla\<rbrakk> \<Longrightarrow> length (getFrN (map snd txs) (map fst txs) [\<phi>] (length txs)) = length txs; \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [\<phi>] \<subseteq> fmla\<rbrakk> \<Longrightarrow> length (getFrN (map snd txs) (map fst txs) [\<phi>] (length txs)) = length txs\<rbrakk> \<Longrightarrow> set (getFrN (map snd txs) (map fst txs) [\<phi>] (length txs)) \<inter> Fvars \<phi> = {}
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>\<phi> \<in> fmla; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; prv \<phi>; \<And>t. \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [\<phi>] \<subseteq> fmla; t \<in> set (map fst txs)\<rbrakk> \<Longrightarrow> set (getFrN (map snd txs) (map fst txs) [\<phi>] (length txs)) \<inter> FvarsT t = {}; \<And>\<phi>'. \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [\<phi>] \<subseteq> fmla; \<phi>' \<in> set [\<phi>]\<rbrakk> \<Longrightarrow> set (getFrN (map snd txs) (map fst txs) [\<phi>] (length txs)) \<inter> Fvars \<phi>' = {}; \<And>t. \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [\<phi>] \<subseteq> fmla; t \<in> set (map fst txs)\<rbrakk> \<Longrightarrow> set (getFrN (map snd txs) (map fst txs) [\<phi>] (length txs)) \<inter> set (map snd txs) = {}; \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [\<phi>] \<subseteq> fmla\<rbrakk> \<Longrightarrow> length (getFrN (map snd txs) (map fst txs) [\<phi>] (length txs)) = length txs; \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [\<phi>] \<subseteq> fmla\<rbrakk> \<Longrightarrow> length (getFrN (map snd txs) (map fst txs) [\<phi>] (length txs)) = length txs\<rbrakk> \<Longrightarrow> set (getFrN (map snd txs) (map fst txs) [\<phi>] (length txs)) \<inter> \<Union> (FvarsT ` fst ` set txs) = {}
 2. \<lbrakk>\<phi> \<in> fmla; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; prv \<phi>; \<And>t. \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [\<phi>] \<subseteq> fmla; t \<in> set (map fst txs)\<rbrakk> \<Longrightarrow> set (getFrN (map snd txs) (map fst txs) [\<phi>] (length txs)) \<inter> FvarsT t = {}; \<And>\<phi>'. \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [\<phi>] \<subseteq> fmla; \<phi>' \<in> set [\<phi>]\<rbrakk> \<Longrightarrow> set (getFrN (map snd txs) (map fst txs) [\<phi>] (length txs)) \<inter> Fvars \<phi>' = {}; \<And>t. \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [\<phi>] \<subseteq> fmla; t \<in> set (map fst txs)\<rbrakk> \<Longrightarrow> set (getFrN (map snd txs) (map fst txs) [\<phi>] (length txs)) \<inter> set (map snd txs) = {}; \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [\<phi>] \<subseteq> fmla\<rbrakk> \<Longrightarrow> length (getFrN (map snd txs) (map fst txs) [\<phi>] (length txs)) = length txs; \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [\<phi>] \<subseteq> fmla\<rbrakk> \<Longrightarrow> length (getFrN (map snd txs) (map fst txs) [\<phi>] (length txs)) = length txs\<rbrakk> \<Longrightarrow> set (getFrN (map snd txs) (map fst txs) [\<phi>] (length txs)) \<inter> snd ` set txs = {}
 3. \<lbrakk>\<phi> \<in> fmla; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; prv \<phi>; \<And>t. \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [\<phi>] \<subseteq> fmla; t \<in> set (map fst txs)\<rbrakk> \<Longrightarrow> set (getFrN (map snd txs) (map fst txs) [\<phi>] (length txs)) \<inter> FvarsT t = {}; \<And>\<phi>'. \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [\<phi>] \<subseteq> fmla; \<phi>' \<in> set [\<phi>]\<rbrakk> \<Longrightarrow> set (getFrN (map snd txs) (map fst txs) [\<phi>] (length txs)) \<inter> Fvars \<phi>' = {}; \<And>t. \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [\<phi>] \<subseteq> fmla; t \<in> set (map fst txs)\<rbrakk> \<Longrightarrow> set (getFrN (map snd txs) (map fst txs) [\<phi>] (length txs)) \<inter> set (map snd txs) = {}; \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [\<phi>] \<subseteq> fmla\<rbrakk> \<Longrightarrow> length (getFrN (map snd txs) (map fst txs) [\<phi>] (length txs)) = length txs; \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [\<phi>] \<subseteq> fmla\<rbrakk> \<Longrightarrow> length (getFrN (map snd txs) (map fst txs) [\<phi>] (length txs)) = length txs\<rbrakk> \<Longrightarrow> length (getFrN (map snd txs) (map fst txs) [\<phi>] (length txs)) = length txs
 4. \<lbrakk>\<phi> \<in> fmla; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; prv \<phi>; \<And>t. \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [\<phi>] \<subseteq> fmla; t \<in> set (map fst txs)\<rbrakk> \<Longrightarrow> set (getFrN (map snd txs) (map fst txs) [\<phi>] (length txs)) \<inter> FvarsT t = {}; \<And>\<phi>'. \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [\<phi>] \<subseteq> fmla; \<phi>' \<in> set [\<phi>]\<rbrakk> \<Longrightarrow> set (getFrN (map snd txs) (map fst txs) [\<phi>] (length txs)) \<inter> Fvars \<phi>' = {}; \<And>t. \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [\<phi>] \<subseteq> fmla; t \<in> set (map fst txs)\<rbrakk> \<Longrightarrow> set (getFrN (map snd txs) (map fst txs) [\<phi>] (length txs)) \<inter> set (map snd txs) = {}; \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [\<phi>] \<subseteq> fmla\<rbrakk> \<Longrightarrow> length (getFrN (map snd txs) (map fst txs) [\<phi>] (length txs)) = length txs; \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [\<phi>] \<subseteq> fmla\<rbrakk> \<Longrightarrow> length (getFrN (map snd txs) (map fst txs) [\<phi>] (length txs)) = length txs\<rbrakk> \<Longrightarrow> distinct (getFrN (map snd txs) (map fst txs) [\<phi>] (length txs))
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<phi> \<in> fmla; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; prv \<phi>; \<And>t. \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [\<phi>] \<subseteq> fmla; t \<in> set (map fst txs)\<rbrakk> \<Longrightarrow> set (getFrN (map snd txs) (map fst txs) [\<phi>] (length txs)) \<inter> FvarsT t = {}; \<And>\<phi>'. \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [\<phi>] \<subseteq> fmla; \<phi>' \<in> set [\<phi>]\<rbrakk> \<Longrightarrow> set (getFrN (map snd txs) (map fst txs) [\<phi>] (length txs)) \<inter> Fvars \<phi>' = {}; \<And>t. \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [\<phi>] \<subseteq> fmla; t \<in> set (map fst txs)\<rbrakk> \<Longrightarrow> set (getFrN (map snd txs) (map fst txs) [\<phi>] (length txs)) \<inter> set (map snd txs) = {}; \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [\<phi>] \<subseteq> fmla\<rbrakk> \<Longrightarrow> length (getFrN (map snd txs) (map fst txs) [\<phi>] (length txs)) = length txs; \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [\<phi>] \<subseteq> fmla\<rbrakk> \<Longrightarrow> length (getFrN (map snd txs) (map fst txs) [\<phi>] (length txs)) = length txs\<rbrakk> \<Longrightarrow> set (getFrN (map snd txs) (map fst txs) [\<phi>] (length txs)) \<inter> \<Union> (FvarsT ` fst ` set txs) = {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>\<phi> \<in> fmla; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; prv \<phi>; \<And>t. \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [\<phi>] \<subseteq> fmla; t \<in> set (map fst txs)\<rbrakk> \<Longrightarrow> set (getFrN (map snd txs) (map fst txs) [\<phi>] (length txs)) \<inter> FvarsT t = {}; \<And>\<phi>'. \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [\<phi>] \<subseteq> fmla; \<phi>' \<in> set [\<phi>]\<rbrakk> \<Longrightarrow> set (getFrN (map snd txs) (map fst txs) [\<phi>] (length txs)) \<inter> Fvars \<phi>' = {}; \<And>t. \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [\<phi>] \<subseteq> fmla; t \<in> set (map fst txs)\<rbrakk> \<Longrightarrow> set (getFrN (map snd txs) (map fst txs) [\<phi>] (length txs)) \<inter> set (map snd txs) = {}; \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [\<phi>] \<subseteq> fmla\<rbrakk> \<Longrightarrow> length (getFrN (map snd txs) (map fst txs) [\<phi>] (length txs)) = length txs; \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [\<phi>] \<subseteq> fmla\<rbrakk> \<Longrightarrow> length (getFrN (map snd txs) (map fst txs) [\<phi>] (length txs)) = length txs\<rbrakk> \<Longrightarrow> set (getFrN (map snd txs) (map fst txs) [\<phi>] (length txs)) \<inter> snd ` set txs = {}
 2. \<lbrakk>\<phi> \<in> fmla; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; prv \<phi>; \<And>t. \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [\<phi>] \<subseteq> fmla; t \<in> set (map fst txs)\<rbrakk> \<Longrightarrow> set (getFrN (map snd txs) (map fst txs) [\<phi>] (length txs)) \<inter> FvarsT t = {}; \<And>\<phi>'. \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [\<phi>] \<subseteq> fmla; \<phi>' \<in> set [\<phi>]\<rbrakk> \<Longrightarrow> set (getFrN (map snd txs) (map fst txs) [\<phi>] (length txs)) \<inter> Fvars \<phi>' = {}; \<And>t. \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [\<phi>] \<subseteq> fmla; t \<in> set (map fst txs)\<rbrakk> \<Longrightarrow> set (getFrN (map snd txs) (map fst txs) [\<phi>] (length txs)) \<inter> set (map snd txs) = {}; \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [\<phi>] \<subseteq> fmla\<rbrakk> \<Longrightarrow> length (getFrN (map snd txs) (map fst txs) [\<phi>] (length txs)) = length txs; \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [\<phi>] \<subseteq> fmla\<rbrakk> \<Longrightarrow> length (getFrN (map snd txs) (map fst txs) [\<phi>] (length txs)) = length txs\<rbrakk> \<Longrightarrow> length (getFrN (map snd txs) (map fst txs) [\<phi>] (length txs)) = length txs
 3. \<lbrakk>\<phi> \<in> fmla; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; prv \<phi>; \<And>t. \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [\<phi>] \<subseteq> fmla; t \<in> set (map fst txs)\<rbrakk> \<Longrightarrow> set (getFrN (map snd txs) (map fst txs) [\<phi>] (length txs)) \<inter> FvarsT t = {}; \<And>\<phi>'. \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [\<phi>] \<subseteq> fmla; \<phi>' \<in> set [\<phi>]\<rbrakk> \<Longrightarrow> set (getFrN (map snd txs) (map fst txs) [\<phi>] (length txs)) \<inter> Fvars \<phi>' = {}; \<And>t. \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [\<phi>] \<subseteq> fmla; t \<in> set (map fst txs)\<rbrakk> \<Longrightarrow> set (getFrN (map snd txs) (map fst txs) [\<phi>] (length txs)) \<inter> set (map snd txs) = {}; \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [\<phi>] \<subseteq> fmla\<rbrakk> \<Longrightarrow> length (getFrN (map snd txs) (map fst txs) [\<phi>] (length txs)) = length txs; \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [\<phi>] \<subseteq> fmla\<rbrakk> \<Longrightarrow> length (getFrN (map snd txs) (map fst txs) [\<phi>] (length txs)) = length txs\<rbrakk> \<Longrightarrow> distinct (getFrN (map snd txs) (map fst txs) [\<phi>] (length txs))
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<phi> \<in> fmla; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; prv \<phi>; \<And>t. \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [\<phi>] \<subseteq> fmla; t \<in> set (map fst txs)\<rbrakk> \<Longrightarrow> set (getFrN (map snd txs) (map fst txs) [\<phi>] (length txs)) \<inter> FvarsT t = {}; \<And>\<phi>'. \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [\<phi>] \<subseteq> fmla; \<phi>' \<in> set [\<phi>]\<rbrakk> \<Longrightarrow> set (getFrN (map snd txs) (map fst txs) [\<phi>] (length txs)) \<inter> Fvars \<phi>' = {}; \<And>t. \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [\<phi>] \<subseteq> fmla; t \<in> set (map fst txs)\<rbrakk> \<Longrightarrow> set (getFrN (map snd txs) (map fst txs) [\<phi>] (length txs)) \<inter> set (map snd txs) = {}; \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [\<phi>] \<subseteq> fmla\<rbrakk> \<Longrightarrow> length (getFrN (map snd txs) (map fst txs) [\<phi>] (length txs)) = length txs; \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [\<phi>] \<subseteq> fmla\<rbrakk> \<Longrightarrow> length (getFrN (map snd txs) (map fst txs) [\<phi>] (length txs)) = length txs\<rbrakk> \<Longrightarrow> set (getFrN (map snd txs) (map fst txs) [\<phi>] (length txs)) \<inter> snd ` set txs = {}
[PROOF STEP]
by (fastforce simp: image_iff)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<phi> \<in> fmla; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; prv \<phi>; \<And>t. \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [\<phi>] \<subseteq> fmla; t \<in> set (map fst txs)\<rbrakk> \<Longrightarrow> set (getFrN (map snd txs) (map fst txs) [\<phi>] (length txs)) \<inter> FvarsT t = {}; \<And>\<phi>'. \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [\<phi>] \<subseteq> fmla; \<phi>' \<in> set [\<phi>]\<rbrakk> \<Longrightarrow> set (getFrN (map snd txs) (map fst txs) [\<phi>] (length txs)) \<inter> Fvars \<phi>' = {}; \<And>t. \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [\<phi>] \<subseteq> fmla; t \<in> set (map fst txs)\<rbrakk> \<Longrightarrow> set (getFrN (map snd txs) (map fst txs) [\<phi>] (length txs)) \<inter> set (map snd txs) = {}; \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [\<phi>] \<subseteq> fmla\<rbrakk> \<Longrightarrow> length (getFrN (map snd txs) (map fst txs) [\<phi>] (length txs)) = length txs; \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [\<phi>] \<subseteq> fmla\<rbrakk> \<Longrightarrow> length (getFrN (map snd txs) (map fst txs) [\<phi>] (length txs)) = length txs\<rbrakk> \<Longrightarrow> length (getFrN (map snd txs) (map fst txs) [\<phi>] (length txs)) = length txs
 2. \<lbrakk>\<phi> \<in> fmla; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; prv \<phi>; \<And>t. \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [\<phi>] \<subseteq> fmla; t \<in> set (map fst txs)\<rbrakk> \<Longrightarrow> set (getFrN (map snd txs) (map fst txs) [\<phi>] (length txs)) \<inter> FvarsT t = {}; \<And>\<phi>'. \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [\<phi>] \<subseteq> fmla; \<phi>' \<in> set [\<phi>]\<rbrakk> \<Longrightarrow> set (getFrN (map snd txs) (map fst txs) [\<phi>] (length txs)) \<inter> Fvars \<phi>' = {}; \<And>t. \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [\<phi>] \<subseteq> fmla; t \<in> set (map fst txs)\<rbrakk> \<Longrightarrow> set (getFrN (map snd txs) (map fst txs) [\<phi>] (length txs)) \<inter> set (map snd txs) = {}; \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [\<phi>] \<subseteq> fmla\<rbrakk> \<Longrightarrow> length (getFrN (map snd txs) (map fst txs) [\<phi>] (length txs)) = length txs; \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [\<phi>] \<subseteq> fmla\<rbrakk> \<Longrightarrow> length (getFrN (map snd txs) (map fst txs) [\<phi>] (length txs)) = length txs\<rbrakk> \<Longrightarrow> distinct (getFrN (map snd txs) (map fst txs) [\<phi>] (length txs))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
set us \<subseteq> var
set us \<inter> Fvars \<phi> = {}
set us \<inter> \<Union> (FvarsT ` fst ` set txs) = {}
set us \<inter> snd ` set txs = {}
length us = length txs
distinct us

goal (1 subgoal):
 1. prv (psubst \<phi> txs)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (psubst \<phi> txs)
[PROOF STEP]
using assms us_facts
[PROOF STATE]
proof (prove)
using this:
\<phi> \<in> fmla
snd ` set txs \<subseteq> var
fst ` set txs \<subseteq> trm
prv \<phi>
set us \<subseteq> var
set us \<inter> Fvars \<phi> = {}
set us \<inter> \<Union> (FvarsT ` fst ` set txs) = {}
set us \<inter> snd ` set txs = {}
length us = length txs
distinct us

goal (1 subgoal):
 1. prv (psubst \<phi> txs)
[PROOF STEP]
unfolding psubst_def
[PROOF STATE]
proof (prove)
using this:
\<phi> \<in> fmla
snd ` set txs \<subseteq> var
fst ` set txs \<subseteq> trm
prv \<phi>
set us \<subseteq> var
set us \<inter> Fvars \<phi> = {}
set us \<inter> \<Union> (FvarsT ` fst ` set txs) = {}
set us \<inter> snd ` set txs = {}
length us = length txs
distinct us

goal (1 subgoal):
 1. prv (let xs = map snd txs; ts = map fst txs; us = getFrN xs ts [\<phi>] (length xs) in rawpsubst (rawpsubst \<phi> (zip (map Var us) xs)) (zip ts us))
[PROOF STEP]
by (auto simp: Let_def us[symmetric] intro!: prv_rawpsubst rawpsubst dest!: set_zip_D)
[PROOF STATE]
proof (state)
this:
prv (psubst \<phi> txs)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma prv_eqv_rawpsubst:
  "\<phi> \<in> fmla \<Longrightarrow> \<psi> \<in> fmla \<Longrightarrow> snd ` set txs \<subseteq> var \<Longrightarrow> fst ` set txs \<subseteq> trm \<Longrightarrow> prv (eqv \<phi> \<psi>) \<Longrightarrow>
 prv (eqv (rawpsubst \<phi> txs) (rawpsubst \<psi> txs))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<phi> \<in> fmla; \<psi> \<in> fmla; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; prv (eqv \<phi> \<psi>)\<rbrakk> \<Longrightarrow> prv (eqv (rawpsubst \<phi> txs) (rawpsubst \<psi> txs))
[PROOF STEP]
by (metis eqv prv_rawpsubst rawpsubst_eqv)


[STATEMENT]
lemma prv_eqv_psubst:
  "\<phi> \<in> fmla \<Longrightarrow> \<psi> \<in> fmla \<Longrightarrow> snd ` set txs \<subseteq> var \<Longrightarrow> fst ` set txs \<subseteq> trm \<Longrightarrow> prv (eqv \<phi> \<psi>) \<Longrightarrow>
 distinct (map snd txs) \<Longrightarrow>
 prv (eqv (psubst \<phi> txs) (psubst \<psi> txs))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<phi> \<in> fmla; \<psi> \<in> fmla; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; prv (eqv \<phi> \<psi>); distinct (map snd txs)\<rbrakk> \<Longrightarrow> prv (eqv (psubst \<phi> txs) (psubst \<psi> txs))
[PROOF STEP]
by (metis eqv prv_psubst psubst_eqv)


[STATEMENT]
lemma prv_all_imp_trans:
  assumes "x \<in> var" and "\<phi> \<in> fmla" and "\<chi> \<in> fmla" and "\<psi> \<in> fmla"
  shows "prv (all x (imp \<phi> \<chi>)) \<Longrightarrow> prv (all x (imp \<chi> \<psi>)) \<Longrightarrow> prv (all x (imp \<phi> \<psi>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>prv (all x (imp \<phi> \<chi>)); prv (all x (imp \<chi> \<psi>))\<rbrakk> \<Longrightarrow> prv (all x (imp \<phi> \<psi>))
[PROOF STEP]
by (metis Var assms prv_allE prv_all_gen prv_prv_imp_trans imp subst_same_Var)


[STATEMENT]
lemma prv_all_imp_cnj:
  assumes "x \<in> var" and "\<phi> \<in> fmla" and "\<chi> \<in> fmla" and "\<psi> \<in> fmla"
  shows "prv (all x (imp \<phi> (imp \<psi> \<chi>))) \<Longrightarrow> prv (all x (imp (cnj \<psi> \<phi>) \<chi>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (all x (imp \<phi> (imp \<psi> \<chi>))) \<Longrightarrow> prv (all x (imp (cnj \<psi> \<phi>) \<chi>))
[PROOF STEP]
by (metis Var assms cnj prv_allE prv_all_gen prv_imp_com prv_cnj_imp_monoR2 imp subst_same_Var)


[STATEMENT]
lemma prv_all_imp_cnj_rev:
  assumes "x \<in> var" and "\<phi> \<in> fmla" and "\<chi> \<in> fmla" and "\<psi> \<in> fmla"
  shows "prv (all x (imp (cnj \<phi> \<psi>) \<chi>)) \<Longrightarrow> prv (all x (imp \<phi> (imp \<psi> \<chi>)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (all x (imp (cnj \<phi> \<psi>) \<chi>)) \<Longrightarrow> prv (all x (imp \<phi> (imp \<psi> \<chi>)))
[PROOF STEP]
by (metis (full_types) Var assms cnj prv_allE prv_all_gen prv_cnj_imp imp subst_same_Var)


[STATEMENT]
lemma prv_eql_reflT:
  assumes t: "t \<in> trm"
  shows "prv (eql t t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (eql t t)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. prv (eql t t)
[PROOF STEP]
obtain x where x: "x \<in> var"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>x. x \<in> var \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using var_NE
[PROOF STATE]
proof (prove)
using this:
var \<noteq> {}

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

goal (1 subgoal):
 1. prv (eql t t)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (eql t t)
[PROOF STEP]
using prv_subst[OF x _ t prv_eql_refl[OF x]] x t
[PROOF STATE]
proof (prove)
using this:
eql (Var x) (Var x) \<in> fmla \<Longrightarrow> prv (subst (eql (Var x) (Var x)) t x)
x \<in> var
t \<in> trm

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma prv_eql_subst_trm:
  assumes xx: "x \<in> var" and \<phi>: "\<phi> \<in> fmla" and "t1 \<in> trm" and "t2 \<in> trm"
  shows "prv ((imp (eql t1 t2)
                 (imp (subst \<phi> t1 x) (subst \<phi> t2 x))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (imp (eql t1 t2) (imp (subst \<phi> t1 x) (subst \<phi> t2 x)))
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. prv (imp (eql t1 t2) (imp (subst \<phi> t1 x) (subst \<phi> t2 x)))
[PROOF STEP]
have "finite ({x} \<union> FvarsT t1 \<union> FvarsT t2 \<union> Fvars \<phi>)" (is "finite ?A")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite ({x} \<union> FvarsT t1 \<union> FvarsT t2 \<union> Fvars \<phi>)
[PROOF STEP]
by (simp add: assms finite_FvarsT finite_Fvars)
[PROOF STATE]
proof (state)
this:
finite ({x} \<union> FvarsT t1 \<union> FvarsT t2 \<union> Fvars \<phi>)

goal (1 subgoal):
 1. prv (imp (eql t1 t2) (imp (subst \<phi> t1 x) (subst \<phi> t2 x)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
finite ({x} \<union> FvarsT t1 \<union> FvarsT t2 \<union> Fvars \<phi>)
[PROOF STEP]
obtain y where y: "y \<in> var" and "y \<notin> ?A"
[PROOF STATE]
proof (prove)
using this:
finite ({x} \<union> FvarsT t1 \<union> FvarsT t2 \<union> Fvars \<phi>)

goal (1 subgoal):
 1. (\<And>y. \<lbrakk>y \<in> var; y \<notin> {x} \<union> FvarsT t1 \<union> FvarsT t2 \<union> Fvars \<phi>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (meson finite_subset infinite_var subset_iff)
[PROOF STATE]
proof (state)
this:
y \<in> var
y \<notin> {x} \<union> FvarsT t1 \<union> FvarsT t2 \<union> Fvars \<phi>

goal (1 subgoal):
 1. prv (imp (eql t1 t2) (imp (subst \<phi> t1 x) (subst \<phi> t2 x)))
[PROOF STEP]
hence xy: "x \<noteq> y" and yt1: "y \<notin> FvarsT t1" and yt2: "y \<notin> FvarsT t2" and y\<phi>: "y \<notin> Fvars \<phi>"
[PROOF STATE]
proof (prove)
using this:
y \<in> var
y \<notin> {x} \<union> FvarsT t1 \<union> FvarsT t2 \<union> Fvars \<phi>

goal (1 subgoal):
 1. (x \<noteq> y &&& y \<notin> FvarsT t1) &&& y \<notin> FvarsT t2 &&& y \<notin> Fvars \<phi>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<noteq> y
y \<notin> FvarsT t1
y \<notin> FvarsT t2
y \<notin> Fvars \<phi>

goal (1 subgoal):
 1. prv (imp (eql t1 t2) (imp (subst \<phi> t1 x) (subst \<phi> t2 x)))
[PROOF STEP]
have x: "x \<notin> Fvars (subst \<phi> (Var y) x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<notin> Fvars (subst \<phi> (Var y) x)
[PROOF STEP]
using xy y assms
[PROOF STATE]
proof (prove)
using this:
x \<noteq> y
y \<in> var
x \<in> var
\<phi> \<in> fmla
t1 \<in> trm
t2 \<in> trm

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

goal (1 subgoal):
 1. prv (imp (eql t1 t2) (imp (subst \<phi> t1 x) (subst \<phi> t2 x)))
[PROOF STEP]
hence 1: "prv (imp (eql t1 (Var y)) (imp (subst \<phi> t1 x) (subst \<phi> (Var y) x)))"
[PROOF STATE]
proof (prove)
using this:
x \<notin> Fvars (subst \<phi> (Var y) x)

goal (1 subgoal):
 1. prv (imp (eql t1 (Var y)) (imp (subst \<phi> t1 x) (subst \<phi> (Var y) x)))
[PROOF STEP]
using xy y assms prv_subst[OF xx _ _ prv_eql_subst[OF xx y \<phi>]]
[PROOF STATE]
proof (prove)
using this:
x \<notin> Fvars (subst \<phi> (Var y) x)
x \<noteq> y
y \<in> var
x \<in> var
\<phi> \<in> fmla
t1 \<in> trm
t2 \<in> trm
\<lbrakk>imp (eql (Var x) (Var y)) (imp \<phi> (subst \<phi> (Var y) x)) \<in> fmla; ?t \<in> trm\<rbrakk> \<Longrightarrow> prv (subst (imp (eql (Var x) (Var y)) (imp \<phi> (subst \<phi> (Var y) x))) ?t x)

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

goal (1 subgoal):
 1. prv (imp (eql t1 t2) (imp (subst \<phi> t1 x) (subst \<phi> t2 x)))
[PROOF STEP]
have yy: "y \<notin> Fvars (subst \<phi> t1 x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y \<notin> Fvars (subst \<phi> t1 x)
[PROOF STEP]
using yt1 y\<phi> assms
[PROOF STATE]
proof (prove)
using this:
y \<notin> FvarsT t1
y \<notin> Fvars \<phi>
x \<in> var
\<phi> \<in> fmla
t1 \<in> trm
t2 \<in> trm

goal (1 subgoal):
 1. y \<notin> Fvars (subst \<phi> t1 x)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
y \<notin> Fvars (subst \<phi> t1 x)

goal (1 subgoal):
 1. prv (imp (eql t1 t2) (imp (subst \<phi> t1 x) (subst \<phi> t2 x)))
[PROOF STEP]
from prv_subst[OF y _ _ 1, of t2]
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>imp (eql t1 (Var y)) (imp (subst \<phi> t1 x) (subst \<phi> (Var y) x)) \<in> fmla; t2 \<in> trm\<rbrakk> \<Longrightarrow> prv (subst (imp (eql t1 (Var y)) (imp (subst \<phi> t1 x) (subst \<phi> (Var y) x))) t2 y)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>imp (eql t1 (Var y)) (imp (subst \<phi> t1 x) (subst \<phi> (Var y) x)) \<in> fmla; t2 \<in> trm\<rbrakk> \<Longrightarrow> prv (subst (imp (eql t1 (Var y)) (imp (subst \<phi> t1 x) (subst \<phi> (Var y) x))) t2 y)

goal (1 subgoal):
 1. prv (imp (eql t1 t2) (imp (subst \<phi> t1 x) (subst \<phi> t2 x)))
[PROOF STEP]
using xy yt1 yt2 y\<phi> x xx y yy assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>imp (eql t1 (Var y)) (imp (subst \<phi> t1 x) (subst \<phi> (Var y) x)) \<in> fmla; t2 \<in> trm\<rbrakk> \<Longrightarrow> prv (subst (imp (eql t1 (Var y)) (imp (subst \<phi> t1 x) (subst \<phi> (Var y) x))) t2 y)
x \<noteq> y
y \<notin> FvarsT t1
y \<notin> FvarsT t2
y \<notin> Fvars \<phi>
x \<notin> Fvars (subst \<phi> (Var y) x)
x \<in> var
y \<in> var
y \<notin> Fvars (subst \<phi> t1 x)
x \<in> var
\<phi> \<in> fmla
t1 \<in> trm
t2 \<in> trm

goal (1 subgoal):
 1. prv (imp (eql t1 t2) (imp (subst \<phi> t1 x) (subst \<phi> t2 x)))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
prv (imp (eql t1 t2) (imp (subst \<phi> t1 x) (subst \<phi> t2 x)))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma prv_eql_subst_trm2:
  assumes "x \<in> var" and "\<phi> \<in> fmla" and "t1 \<in> trm" and "t2 \<in> trm"
  assumes "prv (eql t1 t2)"
  shows "prv (imp (subst \<phi> t1 x) (subst \<phi> t2 x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (imp (subst \<phi> t1 x) (subst \<phi> t2 x))
[PROOF STEP]
by (meson assms eql imp local.subst prv_eql_subst_trm prv_imp_mp)


[STATEMENT]
lemma prv_eql_sym:
  assumes [simp]: "t1 \<in> trm" "t2 \<in> trm"
  shows "prv (imp (eql t1 t2) (eql t2 t1))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (imp (eql t1 t2) (eql t2 t1))
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. prv (imp (eql t1 t2) (eql t2 t1))
[PROOF STEP]
obtain x where x[simp]: "x \<in> var" "x \<notin> FvarsT t1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>x. \<lbrakk>x \<in> var; x \<notin> FvarsT t1\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (meson assms finite_FvarsT finite_subset infinite_var subsetI)
[PROOF STATE]
proof (state)
this:
x \<in> var
x \<notin> FvarsT t1

goal (1 subgoal):
 1. prv (imp (eql t1 t2) (eql t2 t1))
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
x \<in> var
x \<notin> FvarsT t1

goal (1 subgoal):
 1. prv (imp (eql t1 t2) (eql t2 t1))
[PROOF STEP]
using prv_eql_subst_trm[of x "eql (Var x) t1" t1 t2, simplified]
[PROOF STATE]
proof (prove)
using this:
x \<in> var
x \<notin> FvarsT t1
prv (imp (eql t1 t2) (imp (eql t1 t1) (eql t2 t1)))

goal (1 subgoal):
 1. prv (imp (eql t1 t2) (eql t2 t1))
[PROOF STEP]
by (meson assms eql imp prv_eql_reflT prv_imp_com prv_imp_mp)
[PROOF STATE]
proof (state)
this:
prv (imp (eql t1 t2) (eql t2 t1))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma prv_prv_eql_sym: "t1 \<in> trm \<Longrightarrow> t2 \<in> trm \<Longrightarrow> prv (eql t1 t2) \<Longrightarrow> prv (eql t2 t1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>t1 \<in> trm; t2 \<in> trm; prv (eql t1 t2)\<rbrakk> \<Longrightarrow> prv (eql t2 t1)
[PROOF STEP]
by (meson eql prv_eql_sym prv_imp_mp)


[STATEMENT]
lemma prv_all_eql:
  assumes "x \<in> var" and "y \<in> var" and "\<phi> \<in> fmla" and "t1 \<in> trm" and "t2 \<in> trm"
  shows "prv (all x ((imp (eql t1 t2)
                   (imp (subst \<phi> t2 y) (subst \<phi> t1 y)))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (all x (imp (eql t1 t2) (imp (subst \<phi> t2 y) (subst \<phi> t1 y))))
[PROOF STEP]
by (meson subst assms prv_all_gen prv_prv_imp_trans prv_eql_subst_trm prv_eql_sym eql imp)


[STATEMENT]
lemma prv_eql_subst_trm_rev:
  assumes "t1 \<in> trm" and "t2 \<in> trm" and "\<phi> \<in> fmla" and "y \<in> var"
  shows
    "prv ((imp (eql t1 t2)
           (imp (subst \<phi> t2 y) (subst \<phi> t1 y))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (imp (eql t1 t2) (imp (subst \<phi> t2 y) (subst \<phi> t1 y)))
[PROOF STEP]
using assms prv_all_eql prv_all_inst prv_imp_mp subst_same_Var
[PROOF STATE]
proof (prove)
using this:
t1 \<in> trm
t2 \<in> trm
\<phi> \<in> fmla
y \<in> var
\<lbrakk>?x \<in> var; ?y \<in> var; ?\<phi> \<in> fmla; ?t1.0 \<in> trm; ?t2.0 \<in> trm\<rbrakk> \<Longrightarrow> prv (all ?x (imp (eql ?t1.0 ?t2.0) (imp (subst ?\<phi> ?t2.0 ?y) (subst ?\<phi> ?t1.0 ?y))))
\<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>
\<lbrakk>?\<phi> \<in> fmla; ?x \<in> var\<rbrakk> \<Longrightarrow> subst ?\<phi> (Var ?x) ?x = ?\<phi>

goal (1 subgoal):
 1. prv (imp (eql t1 t2) (imp (subst \<phi> t2 y) (subst \<phi> t1 y)))
[PROOF STEP]
by (meson subst prv_prv_imp_trans prv_eql_subst_trm prv_eql_sym eql imp)


[STATEMENT]
lemma prv_eql_subst_trm_rev2:
  assumes "x \<in> var" and "\<phi> \<in> fmla" and "t1 \<in> trm" and "t2 \<in> trm"
  assumes "prv (eql t1 t2)"
  shows "prv (imp (subst \<phi> t2 x) (subst \<phi> t1 x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (imp (subst \<phi> t2 x) (subst \<phi> t1 x))
[PROOF STEP]
by (meson assms eql imp local.subst prv_eql_subst_trm_rev prv_imp_mp)


[STATEMENT]
lemma prv_eql_subst_trm_eqv:
  assumes "x \<in> var" and "\<phi> \<in> fmla" and "t1 \<in> trm" and "t2 \<in> trm"
  assumes "prv (eql t1 t2)"
  shows "prv (eqv (subst \<phi> t1 x) (subst \<phi> t2 x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (eqv (subst \<phi> t1 x) (subst \<phi> t2 x))
[PROOF STEP]
using assms prv_eql_subst_trm2[OF assms] prv_eql_subst_trm_rev2[OF assms]
    prv_eqvI
[PROOF STATE]
proof (prove)
using this:
x \<in> var
\<phi> \<in> fmla
t1 \<in> trm
t2 \<in> trm
prv (eql t1 t2)
prv (imp (subst \<phi> t1 x) (subst \<phi> t2 x))
prv (imp (subst \<phi> t2 x) (subst \<phi> t1 x))
\<lbrakk>?\<phi> \<in> fmla; ?\<chi> \<in> fmla; prv (imp ?\<phi> ?\<chi>); prv (imp ?\<chi> ?\<phi>)\<rbrakk> \<Longrightarrow> prv (eqv ?\<phi> ?\<chi>)

goal (1 subgoal):
 1. prv (eqv (subst \<phi> t1 x) (subst \<phi> t2 x))
[PROOF STEP]
by auto


[STATEMENT]
lemma prv_eql_subst_trm_id:
  assumes "y \<in> var" "\<phi> \<in> fmla" and "n \<in> num"
  shows "prv (imp (eql (Var y) n) (imp \<phi> (subst \<phi> n y)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (imp (eql (Var y) n) (imp \<phi> (subst \<phi> n y)))
[PROOF STEP]
using assms prv_eql_subst_trm
[PROOF STATE]
proof (prove)
using this:
y \<in> var
\<phi> \<in> fmla
n \<in> num
\<lbrakk>?x \<in> var; ?\<phi> \<in> fmla; ?t1.0 \<in> trm; ?t2.0 \<in> trm\<rbrakk> \<Longrightarrow> prv (imp (eql ?t1.0 ?t2.0) (imp (subst ?\<phi> ?t1.0 ?x) (subst ?\<phi> ?t2.0 ?x)))

goal (1 subgoal):
 1. prv (imp (eql (Var y) n) (imp \<phi> (subst \<phi> n y)))
[PROOF STEP]
by (metis Var in_num subst_same_Var)


[STATEMENT]
lemma prv_eql_subst_trm_id_back:
  assumes "y \<in> var" "\<phi> \<in> fmla" and "n \<in> num"
  shows "prv (imp (eql (Var y) n) (imp (subst \<phi> n y) \<phi>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (imp (eql (Var y) n) (imp (subst \<phi> n y) \<phi>))
[PROOF STEP]
by (metis Var assms in_num prv_eql_subst_trm_rev subst_same_Var)


[STATEMENT]
lemma prv_eql_subst_trm_id_rev:
  assumes "y \<in> var" "\<phi> \<in> fmla" and "n \<in> num"
  shows "prv (imp (eql n (Var y)) (imp \<phi> (subst \<phi> n y)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (imp (eql n (Var y)) (imp \<phi> (subst \<phi> n y)))
[PROOF STEP]
using assms prv_eql_subst_trm_rev
[PROOF STATE]
proof (prove)
using this:
y \<in> var
\<phi> \<in> fmla
n \<in> num
\<lbrakk>?t1.0 \<in> trm; ?t2.0 \<in> trm; ?\<phi> \<in> fmla; ?y \<in> var\<rbrakk> \<Longrightarrow> prv (imp (eql ?t1.0 ?t2.0) (imp (subst ?\<phi> ?t2.0 ?y) (subst ?\<phi> ?t1.0 ?y)))

goal (1 subgoal):
 1. prv (imp (eql n (Var y)) (imp \<phi> (subst \<phi> n y)))
[PROOF STEP]
by (metis Var in_num subst_same_Var)


[STATEMENT]
lemma prv_eql_subst_trm_id_back_rev:
  assumes "y \<in> var" "\<phi> \<in> fmla" and "n \<in> num"
  shows "prv (imp (eql n (Var y)) (imp (subst \<phi> n y) \<phi>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (imp (eql n (Var y)) (imp (subst \<phi> n y) \<phi>))
[PROOF STEP]
by (metis (full_types) Var assms in_num prv_eql_subst_trm subst_same_Var)


[STATEMENT]
lemma prv_eql_imp_trans_rev:
  assumes t1[simp]: "t1 \<in> trm" and t2[simp]: "t2 \<in> trm" and t3[simp]: "t3 \<in> trm"
  shows "prv (imp (eql t1 t2) (imp (eql t1 t3) (eql t2 t3)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (imp (eql t1 t2) (imp (eql t1 t3) (eql t2 t3)))
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. prv (imp (eql t1 t2) (imp (eql t1 t3) (eql t2 t3)))
[PROOF STEP]
obtain y1 where y1[simp]: "y1 \<in> var" and "y1 \<notin> FvarsT t1 \<union> FvarsT t2 \<union> FvarsT t3"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>y1. \<lbrakk>y1 \<in> var; y1 \<notin> FvarsT t1 \<union> FvarsT t2 \<union> FvarsT t3\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using finite_FvarsT finite_subset infinite_var subsetI t1 t2 t3
[PROOF STATE]
proof (prove)
using this:
?t \<in> trm \<Longrightarrow> finite (FvarsT ?t)
\<lbrakk>?A \<subseteq> ?B; finite ?B\<rbrakk> \<Longrightarrow> finite ?A
infinite var
(\<And>x. x \<in> ?A \<Longrightarrow> x \<in> ?B) \<Longrightarrow> ?A \<subseteq> ?B
t1 \<in> trm
t2 \<in> trm
t3 \<in> trm

goal (1 subgoal):
 1. (\<And>y1. \<lbrakk>y1 \<in> var; y1 \<notin> FvarsT t1 \<union> FvarsT t2 \<union> FvarsT t3\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis (full_types) infinite_Un)
[PROOF STATE]
proof (state)
this:
y1 \<in> var
y1 \<notin> FvarsT t1 \<union> FvarsT t2 \<union> FvarsT t3

goal (1 subgoal):
 1. prv (imp (eql t1 t2) (imp (eql t1 t3) (eql t2 t3)))
[PROOF STEP]
hence [simp]: "y1 \<notin> FvarsT t1" "y1 \<notin> FvarsT t2" "y1 \<notin>  FvarsT t3"
[PROOF STATE]
proof (prove)
using this:
y1 \<in> var
y1 \<notin> FvarsT t1 \<union> FvarsT t2 \<union> FvarsT t3

goal (1 subgoal):
 1. y1 \<notin> FvarsT t1 &&& y1 \<notin> FvarsT t2 &&& y1 \<notin> FvarsT t3
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
y1 \<notin> FvarsT t1
y1 \<notin> FvarsT t2
y1 \<notin> FvarsT t3

goal (1 subgoal):
 1. prv (imp (eql t1 t2) (imp (eql t1 t3) (eql t2 t3)))
[PROOF STEP]
obtain y2 where y2[simp]: "y2 \<in> var" and "y2 \<notin> FvarsT t1 \<union> FvarsT t2 \<union> FvarsT t3 \<union> {y1}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>y2. \<lbrakk>y2 \<in> var; y2 \<notin> FvarsT t1 \<union> FvarsT t2 \<union> FvarsT t3 \<union> {y1}\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using finite_FvarsT finite_subset infinite_var subsetI t1 t2 t3
[PROOF STATE]
proof (prove)
using this:
?t \<in> trm \<Longrightarrow> finite (FvarsT ?t)
\<lbrakk>?A \<subseteq> ?B; finite ?B\<rbrakk> \<Longrightarrow> finite ?A
infinite var
(\<And>x. x \<in> ?A \<Longrightarrow> x \<in> ?B) \<Longrightarrow> ?A \<subseteq> ?B
t1 \<in> trm
t2 \<in> trm
t3 \<in> trm

goal (1 subgoal):
 1. (\<And>y2. \<lbrakk>y2 \<in> var; y2 \<notin> FvarsT t1 \<union> FvarsT t2 \<union> FvarsT t3 \<union> {y1}\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis (full_types) finite_insert infinite_Un insert_is_Un)
[PROOF STATE]
proof (state)
this:
y2 \<in> var
y2 \<notin> FvarsT t1 \<union> FvarsT t2 \<union> FvarsT t3 \<union> {y1}

goal (1 subgoal):
 1. prv (imp (eql t1 t2) (imp (eql t1 t3) (eql t2 t3)))
[PROOF STEP]
hence [simp]: "y2 \<notin> FvarsT t1" "y2 \<notin> FvarsT t2" "y2 \<notin>  FvarsT t3" "y1 \<noteq> y2"
[PROOF STATE]
proof (prove)
using this:
y2 \<in> var
y2 \<notin> FvarsT t1 \<union> FvarsT t2 \<union> FvarsT t3 \<union> {y1}

goal (1 subgoal):
 1. (y2 \<notin> FvarsT t1 &&& y2 \<notin> FvarsT t2) &&& y2 \<notin> FvarsT t3 &&& y1 \<noteq> y2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
y2 \<notin> FvarsT t1
y2 \<notin> FvarsT t2
y2 \<notin> FvarsT t3
y1 \<noteq> y2

goal (1 subgoal):
 1. prv (imp (eql t1 t2) (imp (eql t1 t3) (eql t2 t3)))
[PROOF STEP]
have 0: "prv (imp (eql (Var y1) (Var y2))
                    (imp (eql (Var y1) t3) (eql (Var y2) t3)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (imp (eql (Var y1) (Var y2)) (imp (eql (Var y1) t3) (eql (Var y2) t3)))
[PROOF STEP]
using prv_eql_subst[OF y1 y2, of "eql (Var y1) t3"]
[PROOF STATE]
proof (prove)
using this:
eql (Var y1) t3 \<in> fmla \<Longrightarrow> prv (imp (eql (Var y1) (Var y2)) (imp (eql (Var y1) t3) (subst (eql (Var y1) t3) (Var y2) y1)))

goal (1 subgoal):
 1. prv (imp (eql (Var y1) (Var y2)) (imp (eql (Var y1) t3) (eql (Var y2) t3)))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
prv (imp (eql (Var y1) (Var y2)) (imp (eql (Var y1) t3) (eql (Var y2) t3)))

goal (1 subgoal):
 1. prv (imp (eql t1 t2) (imp (eql t1 t3) (eql t2 t3)))
[PROOF STEP]
note 1 = prv_subst[OF y1 _ t1 0, simplified]
[PROOF STATE]
proof (state)
this:
prv (imp (eql t1 (Var y2)) (imp (eql t1 t3) (eql (Var y2) t3)))

goal (1 subgoal):
 1. prv (imp (eql t1 t2) (imp (eql t1 t3) (eql t2 t3)))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (imp (eql t1 t2) (imp (eql t1 t3) (eql t2 t3)))
[PROOF STEP]
using prv_subst[OF y2 _ t2 1, simplified]
[PROOF STATE]
proof (prove)
using this:
prv (imp (eql t1 t2) (imp (eql t1 t3) (eql t2 t3)))

goal (1 subgoal):
 1. prv (imp (eql t1 t2) (imp (eql t1 t3) (eql t2 t3)))
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
prv (imp (eql t1 t2) (imp (eql t1 t3) (eql t2 t3)))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma prv_eql_imp_trans:
  assumes t1[simp]: "t1 \<in> trm" and t2[simp]: "t2 \<in> trm" and t3[simp]: "t3 \<in> trm"
  shows "prv (imp (eql t1 t2) (imp (eql t2 t3) (eql t1 t3)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (imp (eql t1 t2) (imp (eql t2 t3) (eql t1 t3)))
[PROOF STEP]
by (meson eql imp prv_eql_sym prv_eql_imp_trans_rev prv_prv_imp_trans t1 t2 t3)


[STATEMENT]
lemma prv_eql_trans:
  assumes t1[simp]: "t1 \<in> trm" and t2[simp]: "t2 \<in> trm" and t3[simp]: "t3 \<in> trm"
    and "prv (eql t1 t2)" and "prv (eql t2 t3)"
  shows "prv (eql t1 t3)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (eql t1 t3)
[PROOF STEP]
by (meson assms cnj eql prv_cnjI prv_cnj_imp_monoR2 prv_eql_imp_trans prv_imp_mp)


[STATEMENT]
lemma prv_subst_imp_softSubst:
  assumes [simp,intro!]: "x \<in> var" "t \<in> trm" "\<phi> \<in> fmla" "x \<notin> FvarsT t"
  shows "prv (imp (subst \<phi> t x) (softSubst \<phi> t x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (imp (subst \<phi> t x) (softSubst \<phi> t x))
[PROOF STEP]
unfolding softSubst_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (imp (subst \<phi> t x) (exi x (cnj (eql (Var x) t) \<phi>)))
[PROOF STEP]
by (rule prv_imp_exi)
    (auto simp: prv_eql_reflT prv_imp_cnj prv_imp_refl prv_imp_triv subst_compose_same
      intro: prv_exiI[of _ _ t])


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

goal (1 subgoal):
 1. prv (softSubst \<phi> t x)
[PROOF STEP]
by (metis Var cnj eql exi subst prv_imp_mp softSubst_def)


[STATEMENT]
lemma prv_softSubst_imp_subst:
  assumes [simp,intro!]: "x \<in> var" "t \<in> trm" "\<phi> \<in> fmla" "x \<notin> FvarsT t"
  shows "prv (imp (softSubst \<phi> t x) (subst \<phi> t x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (imp (softSubst \<phi> t x) (subst \<phi> t x))
[PROOF STEP]
unfolding softSubst_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (imp (exi x (cnj (eql (Var x) t) \<phi>)) (subst \<phi> t x))
[PROOF STEP]
apply(rule prv_exi_imp_gen)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. x \<in> var
 2. cnj (eql (Var x) t) \<phi> \<in> fmla
 3. subst \<phi> t x \<in> fmla
 4. x \<notin> Fvars (subst \<phi> t x)
 5. prv (imp (cnj (eql (Var x) t) \<phi>) (subst \<phi> t x))
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> var
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. cnj (eql (Var x) t) \<phi> \<in> fmla
 2. subst \<phi> t x \<in> fmla
 3. x \<notin> Fvars (subst \<phi> t x)
 4. prv (imp (cnj (eql (Var x) t) \<phi>) (subst \<phi> t x))
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cnj (eql (Var x) t) \<phi> \<in> fmla
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. subst \<phi> t x \<in> fmla
 2. x \<notin> Fvars (subst \<phi> t x)
 3. prv (imp (cnj (eql (Var x) t) \<phi>) (subst \<phi> t x))
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. subst \<phi> t x \<in> fmla
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. x \<notin> Fvars (subst \<phi> t x)
 2. prv (imp (cnj (eql (Var x) t) \<phi>) (subst \<phi> t x))
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<notin> Fvars (subst \<phi> t x)
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (imp (cnj (eql (Var x) t) \<phi>) (subst \<phi> t x))
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (imp (cnj (eql (Var x) t) \<phi>) (subst \<phi> t x))
[PROOF STEP]
by (metis Var assms(1-3) eql subst prv_cnj_imp_monoR2 prv_eql_subst_trm subst_same_Var)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
.


[STATEMENT]
lemma prv_softSubst_implies_subst:
  assumes "x \<in> var" "t \<in> trm" "\<phi> \<in> fmla"
    and "x \<notin> FvarsT t"
    and "prv (softSubst \<phi> t x)"
  shows "prv (subst \<phi> t x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (subst \<phi> t x)
[PROOF STEP]
by (metis Var assms cnj eql exi local.subst prv_imp_mp prv_softSubst_imp_subst softSubst_def)


[STATEMENT]
lemma prv_softSubst_eqv_subst:
  assumes [simp,intro!]: "x \<in> var" "t \<in> trm" "\<phi> \<in> fmla" "x \<notin> FvarsT t"
  shows "prv (eqv (softSubst \<phi> t x) (subst \<phi> t x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (eqv (softSubst \<phi> t x) (subst \<phi> t x))
[PROOF STEP]
by (metis Var assms cnj eql exi local.subst prv_eqvI prv_softSubst_imp_subst prv_subst_imp_softSubst softSubst_def)


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

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


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


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


[STATEMENT]
lemma prv_imp_neg_fls:
  assumes "\<phi> \<in> fmla"
  shows "prv (imp \<phi> (imp (neg \<phi>) fls))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (imp \<phi> (imp (neg \<phi>) fls))
[PROOF STEP]
using assms prv_imp_com prv_imp_refl neg_def
[PROOF STATE]
proof (prove)
using this:
\<phi> \<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>))
?\<phi> \<in> fmla \<Longrightarrow> prv (imp ?\<phi> ?\<phi>)
neg ?\<phi> = imp ?\<phi> fls

goal (1 subgoal):
 1. prv (imp \<phi> (imp (neg \<phi>) fls))
[PROOF STEP]
by auto


[STATEMENT]
lemma prv_neg_fls:
  assumes "\<phi> \<in> fmla"
  assumes "prv \<phi>" and "prv (neg \<phi>)"
  shows "prv fls"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv fls
[PROOF STEP]
by (metis assms prv_imp_mp fls neg_def)


[STATEMENT]
lemma prv_imp_neg_neg:
  assumes "\<phi> \<in> fmla"
  shows "prv (imp \<phi> (neg (neg \<phi>)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (imp \<phi> (neg (neg \<phi>)))
[PROOF STEP]
using assms prv_imp_neg_fls neg_def
[PROOF STATE]
proof (prove)
using this:
\<phi> \<in> fmla
?\<phi> \<in> fmla \<Longrightarrow> prv (imp ?\<phi> (imp (neg ?\<phi>) fls))
neg ?\<phi> = imp ?\<phi> fls

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


[STATEMENT]
lemma prv_neg_neg:
  assumes "\<phi> \<in> fmla"
  assumes "prv \<phi>"
  shows "prv (neg (neg \<phi>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (neg (neg \<phi>))
[PROOF STEP]
by (metis assms prv_imp_mp prv_imp_neg_fls neg neg_def)


[STATEMENT]
lemma prv_imp_imp_neg_rev:
  assumes "\<phi> \<in> fmla" and "\<chi> \<in> fmla"
  shows "prv (imp (imp \<phi> \<chi>)
                (imp (neg \<chi>) (neg \<phi>)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (imp (imp \<phi> \<chi>) (imp (neg \<chi>) (neg \<phi>)))
[PROOF STEP]
unfolding neg_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (imp (imp \<phi> \<chi>) (imp (imp \<chi> fls) (imp \<phi> fls)))
[PROOF STEP]
using prv_imp_trans2[OF assms fls]
[PROOF STATE]
proof (prove)
using this:
prv (imp (imp \<phi> \<chi>) (imp (imp \<chi> fls) (imp \<phi> fls)))

goal (1 subgoal):
 1. prv (imp (imp \<phi> \<chi>) (imp (imp \<chi> fls) (imp \<phi> fls)))
[PROOF STEP]
.


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


[STATEMENT]
lemma prv_eqv_neg_prv_fls:
  "\<phi> \<in> fmla \<Longrightarrow>
prv (eqv \<phi> (neg \<phi>)) \<Longrightarrow> prv fls"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<phi> \<in> fmla; prv (eqv \<phi> (neg \<phi>))\<rbrakk> \<Longrightarrow> prv fls
[PROOF STEP]
by (metis cnj fls neg neg_def prv_cnj_imp_monoR2 prv_eqv_imp_transi prv_imp_cnj prv_imp_eqvER prv_imp_mp prv_imp_neg_rev)


[STATEMENT]
lemma prv_eqv_eqv_neg_prv_fls:
  "\<phi> \<in> fmla \<Longrightarrow> \<chi> \<in> fmla \<Longrightarrow>
prv (eqv \<phi> \<chi>) \<Longrightarrow> prv (eqv \<phi> (neg \<chi>))\<Longrightarrow> prv fls"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<phi> \<in> fmla; \<chi> \<in> fmla; prv (eqv \<phi> \<chi>); prv (eqv \<phi> (neg \<chi>))\<rbrakk> \<Longrightarrow> prv fls
[PROOF STEP]
by (meson neg prv_eqv_neg_prv_fls prv_eqv_sym prv_eqv_trans)


[STATEMENT]
lemma prv_eqv_eqv_neg_prv_fls2:
  "\<phi> \<in> fmla \<Longrightarrow> \<chi> \<in> fmla \<Longrightarrow>
prv (eqv \<phi> \<chi>) \<Longrightarrow> prv (eqv \<chi> (neg \<phi>))\<Longrightarrow> prv fls"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<phi> \<in> fmla; \<chi> \<in> fmla; prv (eqv \<phi> \<chi>); prv (eqv \<chi> (neg \<phi>))\<rbrakk> \<Longrightarrow> prv fls
[PROOF STEP]
by (simp add: prv_eqv_eqv_neg_prv_fls prv_eqv_sym)


[STATEMENT]
lemma prv_neg_imp_imp_trans:
  assumes "\<phi> \<in> fmla" "\<chi> \<in> fmla"  "\<psi> \<in> fmla"
    and "prv (neg \<phi>)"
    and "prv (imp \<chi> (imp \<psi> \<phi>))"
  shows "prv (imp \<chi> (neg \<psi>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (imp \<chi> (neg \<psi>))
[PROOF STEP]
unfolding neg_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (imp \<chi> (imp \<psi> fls))
[PROOF STEP]
by (metis assms cnj fls neg_def prv_cnj_imp prv_cnj_imp_monoR2 prv_prv_imp_trans)


[STATEMENT]
lemma prv_imp_neg_imp_neg_imp:
  assumes "\<phi> \<in> fmla" "\<chi> \<in> fmla"
    and "prv (neg \<phi>)"
  shows "prv ((imp \<chi> (neg (imp \<chi> \<phi>))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (imp \<chi> (neg (imp \<chi> \<phi>)))
[PROOF STEP]
by (metis assms fls imp neg_def prv_imp_com prv_imp_monoL)


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


[STATEMENT]
lemma prv_imp_neg_imp_cnjL:
  assumes "\<phi> \<in> fmla" "\<phi>1 \<in> fmla" "\<phi>2 \<in> fmla"
    and "prv (imp \<phi> (neg \<phi>1))"
  shows "prv (imp \<phi> (neg (cnj \<phi>1 \<phi>2)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (imp \<phi> (neg (cnj \<phi>1 \<phi>2)))
[PROOF STEP]
unfolding neg_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (imp \<phi> (imp (cnj \<phi>1 \<phi>2) fls))
[PROOF STEP]
by (metis assms cnj fls neg neg_def prv_imp_cnj3L prv_prv_imp_trans)


[STATEMENT]
lemma prv_imp_neg_imp_cnjR:
  assumes "\<phi> \<in> fmla" "\<phi>1 \<in> fmla" "\<phi>2 \<in> fmla"
    and "prv (imp \<phi> (neg \<phi>2))"
  shows "prv (imp \<phi> (neg (cnj \<phi>1 \<phi>2)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (imp \<phi> (neg (cnj \<phi>1 \<phi>2)))
[PROOF STEP]
unfolding neg_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (imp \<phi> (imp (cnj \<phi>1 \<phi>2) fls))
[PROOF STEP]
by (metis assms cnj fls neg neg_def prv_imp_cnj3R prv_prv_imp_trans)


[STATEMENT]
lemma prv_all_neg_imp_neg_exi:
  assumes x: "x \<in> var" and \<phi>: "\<phi> \<in> fmla"
  shows "prv (imp (all x (neg \<phi>)) (neg (exi x \<phi>)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (imp (all x (neg \<phi>)) (neg (exi x \<phi>)))
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. prv (imp (all x (neg \<phi>)) (neg (exi x \<phi>)))
[PROOF STEP]
have 0: "prv (imp (all x (neg \<phi>)) (imp \<phi> fls))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (imp (all x (neg \<phi>)) (imp \<phi> fls))
[PROOF STEP]
using prv_all_inst[OF x, of "neg \<phi>" "Var x",simplified] assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>neg \<phi> \<in> fmla; Var x \<in> trm\<rbrakk> \<Longrightarrow> prv (imp (all x (neg \<phi>)) (subst (neg \<phi>) (Var x) x))
x \<in> var
\<phi> \<in> fmla

goal (1 subgoal):
 1. prv (imp (all x (neg \<phi>)) (imp \<phi> fls))
[PROOF STEP]
by (auto simp: neg_def)
[PROOF STATE]
proof (state)
this:
prv (imp (all x (neg \<phi>)) (imp \<phi> fls))

goal (1 subgoal):
 1. prv (imp (all x (neg \<phi>)) (neg (exi x \<phi>)))
[PROOF STEP]
have 1: "prv (imp \<phi> (imp (all x (neg \<phi>)) fls))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (imp \<phi> (imp (all x (neg \<phi>)) fls))
[PROOF STEP]
using 0
[PROOF STATE]
proof (prove)
using this:
prv (imp (all x (neg \<phi>)) (imp \<phi> fls))

goal (1 subgoal):
 1. prv (imp \<phi> (imp (all x (neg \<phi>)) fls))
[PROOF STEP]
by (simp add: assms  prv_imp_com)
[PROOF STATE]
proof (state)
this:
prv (imp \<phi> (imp (all x (neg \<phi>)) fls))

goal (1 subgoal):
 1. prv (imp (all x (neg \<phi>)) (neg (exi x \<phi>)))
[PROOF STEP]
have 2: "prv (imp (exi x \<phi>) (imp (all x (neg \<phi>)) fls))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (imp (exi x \<phi>) (imp (all x (neg \<phi>)) fls))
[PROOF STEP]
using 1 assms
[PROOF STATE]
proof (prove)
using this:
prv (imp \<phi> (imp (all x (neg \<phi>)) fls))
x \<in> var
\<phi> \<in> fmla

goal (1 subgoal):
 1. prv (imp (exi x \<phi>) (imp (all x (neg \<phi>)) fls))
[PROOF STEP]
by (intro prv_exi_imp_gen) auto
[PROOF STATE]
proof (state)
this:
prv (imp (exi x \<phi>) (imp (all x (neg \<phi>)) fls))

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

goal (1 subgoal):
 1. prv (imp (all x (neg \<phi>)) (neg (exi x \<phi>)))
[PROOF STEP]
by (simp add: assms  neg_def prv_imp_com)
[PROOF STATE]
proof (state)
this:
prv (imp (all x (neg \<phi>)) (neg (exi x \<phi>)))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma prv_neg_exi_imp_all_neg:
  assumes x: "x \<in> var" and \<phi>: "\<phi> \<in> fmla"
  shows "prv (imp (neg (exi x \<phi>)) (all x (neg \<phi>)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (imp (neg (exi x \<phi>)) (all x (neg \<phi>)))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
x \<in> var
\<phi> \<in> fmla

goal (1 subgoal):
 1. prv (imp (neg (exi x \<phi>)) (all x (neg \<phi>)))
[PROOF STEP]
by (intro prv_all_imp_gen[of x "neg (exi x \<phi>)"])
    (auto simp: prv_exi_inst_same prv_imp_neg_rev)


[STATEMENT]
lemma prv_neg_exi_eqv_all_neg:
  assumes x: "x \<in> var" and \<phi>: "\<phi> \<in> fmla"
  shows "prv (eqv (neg (exi x \<phi>)) (all x (neg \<phi>)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (eqv (neg (exi x \<phi>)) (all x (neg \<phi>)))
[PROOF STEP]
by (simp add: \<phi> prv_all_neg_imp_neg_exi prv_eqvI prv_neg_exi_imp_all_neg x)


[STATEMENT]
lemma prv_neg_exi_implies_all_neg:
  assumes x: "x \<in> var" and \<phi>: "\<phi> \<in> fmla" and "prv (neg (exi x \<phi>))"
  shows "prv (all x (neg \<phi>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (all x (neg \<phi>))
[PROOF STEP]
by (meson \<phi> all assms(3) exi neg prv_imp_mp prv_neg_exi_imp_all_neg x)


[STATEMENT]
lemma prv_neg_neg_exi:
  assumes "x \<in> var" "\<phi> \<in> fmla"
    and "prv (neg \<phi>)"
  shows "prv (neg (exi x \<phi>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (neg (exi x \<phi>))
[PROOF STEP]
using assms neg_def prv_exi_imp_gen
[PROOF STATE]
proof (prove)
using this:
x \<in> var
\<phi> \<in> fmla
prv (neg \<phi>)
neg ?\<phi> = imp ?\<phi> fls
\<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 (neg (exi x \<phi>))
[PROOF STEP]
by auto


[STATEMENT]
lemma prv_exi_imp_exiI:
  assumes [simp]: "x \<in> var" "y \<in> var" "\<phi> \<in> fmla" and yx: "y = x \<or> y \<notin> Fvars \<phi>"
  shows "prv (imp (exi x \<phi>) (exi y (subst \<phi> (Var y) x)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (imp (exi x \<phi>) (exi y (subst \<phi> (Var y) x)))
[PROOF STEP]
proof(cases "y = x")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. y = x \<Longrightarrow> prv (imp (exi x \<phi>) (exi y (subst \<phi> (Var y) x)))
 2. y \<noteq> x \<Longrightarrow> prv (imp (exi x \<phi>) (exi y (subst \<phi> (Var y) x)))
[PROOF STEP]
case [simp]: False
[PROOF STATE]
proof (state)
this:
y \<noteq> x

goal (2 subgoals):
 1. y = x \<Longrightarrow> prv (imp (exi x \<phi>) (exi y (subst \<phi> (Var y) x)))
 2. y \<noteq> x \<Longrightarrow> prv (imp (exi x \<phi>) (exi y (subst \<phi> (Var y) x)))
[PROOF STEP]
hence [simp]: "x \<noteq> y"
[PROOF STATE]
proof (prove)
using this:
y \<noteq> x

goal (1 subgoal):
 1. x \<noteq> y
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
x \<noteq> y

goal (2 subgoals):
 1. y = x \<Longrightarrow> prv (imp (exi x \<phi>) (exi y (subst \<phi> (Var y) x)))
 2. y \<noteq> x \<Longrightarrow> prv (imp (exi x \<phi>) (exi y (subst \<phi> (Var y) x)))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (imp (exi x \<phi>) (exi y (subst \<phi> (Var y) x)))
[PROOF STEP]
apply(rule prv_exi_imp_gen)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. x \<in> var
 2. \<phi> \<in> fmla
 3. exi y (subst \<phi> (Var y) x) \<in> fmla
 4. x \<notin> Fvars (exi y (subst \<phi> (Var y) x))
 5. prv (imp \<phi> (exi y (subst \<phi> (Var y) x)))
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> var
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<phi> \<in> fmla
 2. exi y (subst \<phi> (Var y) x) \<in> fmla
 3. x \<notin> Fvars (exi y (subst \<phi> (Var y) x))
 4. prv (imp \<phi> (exi y (subst \<phi> (Var y) x)))
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<phi> \<in> fmla
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. exi y (subst \<phi> (Var y) x) \<in> fmla
 2. x \<notin> Fvars (exi y (subst \<phi> (Var y) x))
 3. prv (imp \<phi> (exi y (subst \<phi> (Var y) x)))
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. exi y (subst \<phi> (Var y) x) \<in> fmla
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. x \<notin> Fvars (exi y (subst \<phi> (Var y) x))
 2. prv (imp \<phi> (exi y (subst \<phi> (Var y) x)))
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<notin> Fvars (exi y (subst \<phi> (Var y) x))
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (imp \<phi> (exi y (subst \<phi> (Var y) x)))
[PROOF STEP]
using yx
[PROOF STATE]
proof (prove)
using this:
y = x \<or> y \<notin> Fvars \<phi>

goal (1 subgoal):
 1. prv (imp \<phi> (exi y (subst \<phi> (Var y) x)))
[PROOF STEP]
by (auto intro!: prv_imp_exi prv_exiI[of _ _ "Var x"]
        simp: prv_imp_refl2)
[PROOF STATE]
proof (state)
this:
prv (imp (exi x \<phi>) (exi y (subst \<phi> (Var y) x)))

goal (1 subgoal):
 1. y = x \<Longrightarrow> prv (imp (exi x \<phi>) (exi y (subst \<phi> (Var y) x)))
[PROOF STEP]
qed(simp add: yx prv_imp_refl)


[STATEMENT]
lemma prv_imp_neg_allI:
  assumes "\<phi> \<in> fmla" "\<chi> \<in> fmla" "t \<in> trm" "x \<in> var"
    and "prv (imp \<phi> (neg (subst \<chi> t x)))"
  shows "prv (imp \<phi> (neg (all x \<chi>)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (imp \<phi> (neg (all x \<chi>)))
[PROOF STEP]
by (meson all assms subst neg prv_all_inst prv_imp_neg_rev prv_prv_imp_trans)


[STATEMENT]
lemma prv_imp_neg_allWI:
  assumes "\<chi> \<in> fmla" "t \<in> trm" "x \<in> var"
    and "prv (neg (subst \<chi> t x))"
  shows "prv (neg (all x \<chi>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (neg (all x \<chi>))
[PROOF STEP]
by (metis all assms fls subst neg_def prv_all_inst prv_prv_imp_trans)


[STATEMENT]
lemma prv_imp_tru: "\<phi> \<in> fmla \<Longrightarrow> prv (imp \<phi> tru)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<phi> \<in> fmla \<Longrightarrow> prv (imp \<phi> tru)
[PROOF STEP]
by (simp add: neg_def prv_imp_triv tru_def)


[STATEMENT]
lemma prv_tru_imp: "\<phi> \<in> fmla \<Longrightarrow> prv (eqv (imp tru \<phi>) \<phi>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<phi> \<in> fmla \<Longrightarrow> prv (eqv (imp tru \<phi>) \<phi>)
[PROOF STEP]
by (metis imp neg_def prv_eqvI prv_fls prv_imp_com prv_imp_imp_triv prv_imp_mp prv_imp_refl tru tru_def)


[STATEMENT]
lemma prv_fls_neg_tru: "\<phi> \<in> fmla \<Longrightarrow> prv (eqv fls (neg tru))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<phi> \<in> fmla \<Longrightarrow> prv (eqv fls (neg tru))
[PROOF STEP]
using neg_def prv_eqvI prv_neg_neg tru_def
[PROOF STATE]
proof (prove)
using this:
neg ?\<phi> = imp ?\<phi> fls
\<lbrakk>?\<phi> \<in> fmla; ?\<chi> \<in> fmla; prv (imp ?\<phi> ?\<chi>); prv (imp ?\<chi> ?\<phi>)\<rbrakk> \<Longrightarrow> prv (eqv ?\<phi> ?\<chi>)
\<lbrakk>?\<phi> \<in> fmla; prv ?\<phi>\<rbrakk> \<Longrightarrow> prv (neg (neg ?\<phi>))
tru = neg fls

goal (1 subgoal):
 1. \<phi> \<in> fmla \<Longrightarrow> prv (eqv fls (neg tru))
[PROOF STEP]
by auto


[STATEMENT]
lemma prv_tru_neg_fls: "\<phi> \<in> fmla \<Longrightarrow> prv (eqv tru (neg fls))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<phi> \<in> fmla \<Longrightarrow> prv (eqv tru (neg fls))
[PROOF STEP]
by (simp add: prv_eqv_refl tru_def)