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

goal (1 subgoal):
 1. prv (eqv (psubst (scnj F) txs) (scnj ((\<lambda>\<phi>. psubst \<phi> txs) ` F)))
[PROOF STEP]
have us_facts: "set us \<subseteq> var"
    "set us \<inter> \<Union> (Fvars ` F) = {}"
    "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> \<Union> (Fvars ` F) = {} &&& 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:
F \<subseteq> fmla
finite F
snd ` set txs \<subseteq> var
fst ` set txs \<subseteq> trm
distinct (map snd txs)

goal (1 subgoal):
 1. (set us \<subseteq> var &&& set us \<inter> \<Union> (Fvars ` F) = {} &&& 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:
F \<subseteq> fmla
finite F
snd ` set txs \<subseteq> var
fst ` set txs \<subseteq> trm
distinct (map snd txs)

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

goal (1 subgoal):
 1. (set (getFrN (map snd txs) (map fst txs) [scnj F] (length txs)) \<subseteq> var &&& set (getFrN (map snd txs) (map fst txs) [scnj F] (length txs)) \<inter> \<Union> (Fvars ` F) = {} &&& set (getFrN (map snd txs) (map fst txs) [scnj F] (length txs)) \<inter> \<Union> (FvarsT ` fst ` set txs) = {}) &&& set (getFrN (map snd txs) (map fst txs) [scnj F] (length txs)) \<inter> snd ` set txs = {} &&& length (getFrN (map snd txs) (map fst txs) [scnj F] (length txs)) = length txs &&& distinct (getFrN (map snd txs) (map fst txs) [scnj F] (length txs))
[PROOF STEP]
apply -
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<lbrakk>F \<subseteq> fmla; finite F; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; distinct (map snd txs); \<And>\<phi>. \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [scnj F] \<subseteq> fmla; \<phi> \<in> set [scnj F]\<rbrakk> \<Longrightarrow> set (getFrN (map snd txs) (map fst txs) [scnj F] (length txs)) \<inter> Fvars \<phi> = {}; \<And>t. \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [scnj F] \<subseteq> fmla; t \<in> set (map fst txs)\<rbrakk> \<Longrightarrow> set (getFrN (map snd txs) (map fst txs) [scnj F] (length txs)) \<inter> FvarsT t = {}; \<And>t. \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [scnj F] \<subseteq> fmla; t \<in> set (map fst txs)\<rbrakk> \<Longrightarrow> set (getFrN (map snd txs) (map fst txs) [scnj F] (length txs)) \<inter> set (map snd txs) = {}; \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [scnj F] \<subseteq> fmla\<rbrakk> \<Longrightarrow> length (getFrN (map snd txs) (map fst txs) [scnj F] (length txs)) = length txs\<rbrakk> \<Longrightarrow> set (getFrN (map snd txs) (map fst txs) [scnj F] (length txs)) \<subseteq> var
 2. \<lbrakk>F \<subseteq> fmla; finite F; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; distinct (map snd txs); \<And>\<phi>. \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [scnj F] \<subseteq> fmla; \<phi> \<in> set [scnj F]\<rbrakk> \<Longrightarrow> set (getFrN (map snd txs) (map fst txs) [scnj F] (length txs)) \<inter> Fvars \<phi> = {}; \<And>t. \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [scnj F] \<subseteq> fmla; t \<in> set (map fst txs)\<rbrakk> \<Longrightarrow> set (getFrN (map snd txs) (map fst txs) [scnj F] (length txs)) \<inter> FvarsT t = {}; \<And>t. \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [scnj F] \<subseteq> fmla; t \<in> set (map fst txs)\<rbrakk> \<Longrightarrow> set (getFrN (map snd txs) (map fst txs) [scnj F] (length txs)) \<inter> set (map snd txs) = {}; \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [scnj F] \<subseteq> fmla\<rbrakk> \<Longrightarrow> length (getFrN (map snd txs) (map fst txs) [scnj F] (length txs)) = length txs\<rbrakk> \<Longrightarrow> set (getFrN (map snd txs) (map fst txs) [scnj F] (length txs)) \<inter> \<Union> (Fvars ` F) = {}
 3. \<lbrakk>F \<subseteq> fmla; finite F; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; distinct (map snd txs); \<And>\<phi>. \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [scnj F] \<subseteq> fmla; \<phi> \<in> set [scnj F]\<rbrakk> \<Longrightarrow> set (getFrN (map snd txs) (map fst txs) [scnj F] (length txs)) \<inter> Fvars \<phi> = {}; \<And>t. \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [scnj F] \<subseteq> fmla; t \<in> set (map fst txs)\<rbrakk> \<Longrightarrow> set (getFrN (map snd txs) (map fst txs) [scnj F] (length txs)) \<inter> FvarsT t = {}; \<And>t. \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [scnj F] \<subseteq> fmla; t \<in> set (map fst txs)\<rbrakk> \<Longrightarrow> set (getFrN (map snd txs) (map fst txs) [scnj F] (length txs)) \<inter> set (map snd txs) = {}; \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [scnj F] \<subseteq> fmla\<rbrakk> \<Longrightarrow> length (getFrN (map snd txs) (map fst txs) [scnj F] (length txs)) = length txs\<rbrakk> \<Longrightarrow> set (getFrN (map snd txs) (map fst txs) [scnj F] (length txs)) \<inter> \<Union> (FvarsT ` fst ` set txs) = {}
 4. \<lbrakk>F \<subseteq> fmla; finite F; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; distinct (map snd txs); \<And>\<phi>. \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [scnj F] \<subseteq> fmla; \<phi> \<in> set [scnj F]\<rbrakk> \<Longrightarrow> set (getFrN (map snd txs) (map fst txs) [scnj F] (length txs)) \<inter> Fvars \<phi> = {}; \<And>t. \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [scnj F] \<subseteq> fmla; t \<in> set (map fst txs)\<rbrakk> \<Longrightarrow> set (getFrN (map snd txs) (map fst txs) [scnj F] (length txs)) \<inter> FvarsT t = {}; \<And>t. \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [scnj F] \<subseteq> fmla; t \<in> set (map fst txs)\<rbrakk> \<Longrightarrow> set (getFrN (map snd txs) (map fst txs) [scnj F] (length txs)) \<inter> set (map snd txs) = {}; \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [scnj F] \<subseteq> fmla\<rbrakk> \<Longrightarrow> length (getFrN (map snd txs) (map fst txs) [scnj F] (length txs)) = length txs\<rbrakk> \<Longrightarrow> set (getFrN (map snd txs) (map fst txs) [scnj F] (length txs)) \<inter> snd ` set txs = {}
 5. \<lbrakk>F \<subseteq> fmla; finite F; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; distinct (map snd txs); \<And>\<phi>. \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [scnj F] \<subseteq> fmla; \<phi> \<in> set [scnj F]\<rbrakk> \<Longrightarrow> set (getFrN (map snd txs) (map fst txs) [scnj F] (length txs)) \<inter> Fvars \<phi> = {}; \<And>t. \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [scnj F] \<subseteq> fmla; t \<in> set (map fst txs)\<rbrakk> \<Longrightarrow> set (getFrN (map snd txs) (map fst txs) [scnj F] (length txs)) \<inter> FvarsT t = {}; \<And>t. \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [scnj F] \<subseteq> fmla; t \<in> set (map fst txs)\<rbrakk> \<Longrightarrow> set (getFrN (map snd txs) (map fst txs) [scnj F] (length txs)) \<inter> set (map snd txs) = {}; \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [scnj F] \<subseteq> fmla\<rbrakk> \<Longrightarrow> length (getFrN (map snd txs) (map fst txs) [scnj F] (length txs)) = length txs\<rbrakk> \<Longrightarrow> length (getFrN (map snd txs) (map fst txs) [scnj F] (length txs)) = length txs
 6. \<lbrakk>F \<subseteq> fmla; finite F; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; distinct (map snd txs); \<And>\<phi>. \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [scnj F] \<subseteq> fmla; \<phi> \<in> set [scnj F]\<rbrakk> \<Longrightarrow> set (getFrN (map snd txs) (map fst txs) [scnj F] (length txs)) \<inter> Fvars \<phi> = {}; \<And>t. \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [scnj F] \<subseteq> fmla; t \<in> set (map fst txs)\<rbrakk> \<Longrightarrow> set (getFrN (map snd txs) (map fst txs) [scnj F] (length txs)) \<inter> FvarsT t = {}; \<And>t. \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [scnj F] \<subseteq> fmla; t \<in> set (map fst txs)\<rbrakk> \<Longrightarrow> set (getFrN (map snd txs) (map fst txs) [scnj F] (length txs)) \<inter> set (map snd txs) = {}; \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [scnj F] \<subseteq> fmla\<rbrakk> \<Longrightarrow> length (getFrN (map snd txs) (map fst txs) [scnj F] (length txs)) = length txs\<rbrakk> \<Longrightarrow> distinct (getFrN (map snd txs) (map fst txs) [scnj F] (length txs))
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>F \<subseteq> fmla; finite F; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; distinct (map snd txs); \<And>\<phi>. \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [scnj F] \<subseteq> fmla; \<phi> \<in> set [scnj F]\<rbrakk> \<Longrightarrow> set (getFrN (map snd txs) (map fst txs) [scnj F] (length txs)) \<inter> Fvars \<phi> = {}; \<And>t. \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [scnj F] \<subseteq> fmla; t \<in> set (map fst txs)\<rbrakk> \<Longrightarrow> set (getFrN (map snd txs) (map fst txs) [scnj F] (length txs)) \<inter> FvarsT t = {}; \<And>t. \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [scnj F] \<subseteq> fmla; t \<in> set (map fst txs)\<rbrakk> \<Longrightarrow> set (getFrN (map snd txs) (map fst txs) [scnj F] (length txs)) \<inter> set (map snd txs) = {}; \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [scnj F] \<subseteq> fmla\<rbrakk> \<Longrightarrow> length (getFrN (map snd txs) (map fst txs) [scnj F] (length txs)) = length txs\<rbrakk> \<Longrightarrow> set (getFrN (map snd txs) (map fst txs) [scnj F] (length txs)) \<subseteq> var
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<lbrakk>F \<subseteq> fmla; finite F; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; distinct (map snd txs); \<And>\<phi>. \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [scnj F] \<subseteq> fmla; \<phi> \<in> set [scnj F]\<rbrakk> \<Longrightarrow> set (getFrN (map snd txs) (map fst txs) [scnj F] (length txs)) \<inter> Fvars \<phi> = {}; \<And>t. \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [scnj F] \<subseteq> fmla; t \<in> set (map fst txs)\<rbrakk> \<Longrightarrow> set (getFrN (map snd txs) (map fst txs) [scnj F] (length txs)) \<inter> FvarsT t = {}; \<And>t. \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [scnj F] \<subseteq> fmla; t \<in> set (map fst txs)\<rbrakk> \<Longrightarrow> set (getFrN (map snd txs) (map fst txs) [scnj F] (length txs)) \<inter> set (map snd txs) = {}; \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [scnj F] \<subseteq> fmla\<rbrakk> \<Longrightarrow> length (getFrN (map snd txs) (map fst txs) [scnj F] (length txs)) = length txs\<rbrakk> \<Longrightarrow> set (getFrN (map snd txs) (map fst txs) [scnj F] (length txs)) \<inter> \<Union> (Fvars ` F) = {}
 2. \<lbrakk>F \<subseteq> fmla; finite F; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; distinct (map snd txs); \<And>\<phi>. \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [scnj F] \<subseteq> fmla; \<phi> \<in> set [scnj F]\<rbrakk> \<Longrightarrow> set (getFrN (map snd txs) (map fst txs) [scnj F] (length txs)) \<inter> Fvars \<phi> = {}; \<And>t. \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [scnj F] \<subseteq> fmla; t \<in> set (map fst txs)\<rbrakk> \<Longrightarrow> set (getFrN (map snd txs) (map fst txs) [scnj F] (length txs)) \<inter> FvarsT t = {}; \<And>t. \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [scnj F] \<subseteq> fmla; t \<in> set (map fst txs)\<rbrakk> \<Longrightarrow> set (getFrN (map snd txs) (map fst txs) [scnj F] (length txs)) \<inter> set (map snd txs) = {}; \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [scnj F] \<subseteq> fmla\<rbrakk> \<Longrightarrow> length (getFrN (map snd txs) (map fst txs) [scnj F] (length txs)) = length txs\<rbrakk> \<Longrightarrow> set (getFrN (map snd txs) (map fst txs) [scnj F] (length txs)) \<inter> \<Union> (FvarsT ` fst ` set txs) = {}
 3. \<lbrakk>F \<subseteq> fmla; finite F; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; distinct (map snd txs); \<And>\<phi>. \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [scnj F] \<subseteq> fmla; \<phi> \<in> set [scnj F]\<rbrakk> \<Longrightarrow> set (getFrN (map snd txs) (map fst txs) [scnj F] (length txs)) \<inter> Fvars \<phi> = {}; \<And>t. \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [scnj F] \<subseteq> fmla; t \<in> set (map fst txs)\<rbrakk> \<Longrightarrow> set (getFrN (map snd txs) (map fst txs) [scnj F] (length txs)) \<inter> FvarsT t = {}; \<And>t. \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [scnj F] \<subseteq> fmla; t \<in> set (map fst txs)\<rbrakk> \<Longrightarrow> set (getFrN (map snd txs) (map fst txs) [scnj F] (length txs)) \<inter> set (map snd txs) = {}; \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [scnj F] \<subseteq> fmla\<rbrakk> \<Longrightarrow> length (getFrN (map snd txs) (map fst txs) [scnj F] (length txs)) = length txs\<rbrakk> \<Longrightarrow> set (getFrN (map snd txs) (map fst txs) [scnj F] (length txs)) \<inter> snd ` set txs = {}
 4. \<lbrakk>F \<subseteq> fmla; finite F; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; distinct (map snd txs); \<And>\<phi>. \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [scnj F] \<subseteq> fmla; \<phi> \<in> set [scnj F]\<rbrakk> \<Longrightarrow> set (getFrN (map snd txs) (map fst txs) [scnj F] (length txs)) \<inter> Fvars \<phi> = {}; \<And>t. \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [scnj F] \<subseteq> fmla; t \<in> set (map fst txs)\<rbrakk> \<Longrightarrow> set (getFrN (map snd txs) (map fst txs) [scnj F] (length txs)) \<inter> FvarsT t = {}; \<And>t. \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [scnj F] \<subseteq> fmla; t \<in> set (map fst txs)\<rbrakk> \<Longrightarrow> set (getFrN (map snd txs) (map fst txs) [scnj F] (length txs)) \<inter> set (map snd txs) = {}; \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [scnj F] \<subseteq> fmla\<rbrakk> \<Longrightarrow> length (getFrN (map snd txs) (map fst txs) [scnj F] (length txs)) = length txs\<rbrakk> \<Longrightarrow> length (getFrN (map snd txs) (map fst txs) [scnj F] (length txs)) = length txs
 5. \<lbrakk>F \<subseteq> fmla; finite F; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; distinct (map snd txs); \<And>\<phi>. \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [scnj F] \<subseteq> fmla; \<phi> \<in> set [scnj F]\<rbrakk> \<Longrightarrow> set (getFrN (map snd txs) (map fst txs) [scnj F] (length txs)) \<inter> Fvars \<phi> = {}; \<And>t. \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [scnj F] \<subseteq> fmla; t \<in> set (map fst txs)\<rbrakk> \<Longrightarrow> set (getFrN (map snd txs) (map fst txs) [scnj F] (length txs)) \<inter> FvarsT t = {}; \<And>t. \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [scnj F] \<subseteq> fmla; t \<in> set (map fst txs)\<rbrakk> \<Longrightarrow> set (getFrN (map snd txs) (map fst txs) [scnj F] (length txs)) \<inter> set (map snd txs) = {}; \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [scnj F] \<subseteq> fmla\<rbrakk> \<Longrightarrow> length (getFrN (map snd txs) (map fst txs) [scnj F] (length txs)) = length txs\<rbrakk> \<Longrightarrow> distinct (getFrN (map snd txs) (map fst txs) [scnj F] (length txs))
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>F \<subseteq> fmla; finite F; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; distinct (map snd txs); \<And>\<phi>. \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [scnj F] \<subseteq> fmla; \<phi> \<in> set [scnj F]\<rbrakk> \<Longrightarrow> set (getFrN (map snd txs) (map fst txs) [scnj F] (length txs)) \<inter> Fvars \<phi> = {}; \<And>t. \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [scnj F] \<subseteq> fmla; t \<in> set (map fst txs)\<rbrakk> \<Longrightarrow> set (getFrN (map snd txs) (map fst txs) [scnj F] (length txs)) \<inter> FvarsT t = {}; \<And>t. \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [scnj F] \<subseteq> fmla; t \<in> set (map fst txs)\<rbrakk> \<Longrightarrow> set (getFrN (map snd txs) (map fst txs) [scnj F] (length txs)) \<inter> set (map snd txs) = {}; \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [scnj F] \<subseteq> fmla\<rbrakk> \<Longrightarrow> length (getFrN (map snd txs) (map fst txs) [scnj F] (length txs)) = length txs\<rbrakk> \<Longrightarrow> set (getFrN (map snd txs) (map fst txs) [scnj F] (length txs)) \<inter> \<Union> (Fvars ` F) = {}
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>F \<subseteq> fmla; finite F; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; distinct (map snd txs); \<And>\<phi>. \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [scnj F] \<subseteq> fmla; \<phi> \<in> set [scnj F]\<rbrakk> \<Longrightarrow> set (getFrN (map snd txs) (map fst txs) [scnj F] (length txs)) \<inter> Fvars \<phi> = {}; \<And>t. \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [scnj F] \<subseteq> fmla; t \<in> set (map fst txs)\<rbrakk> \<Longrightarrow> set (getFrN (map snd txs) (map fst txs) [scnj F] (length txs)) \<inter> FvarsT t = {}; \<And>t. \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [scnj F] \<subseteq> fmla; t \<in> set (map fst txs)\<rbrakk> \<Longrightarrow> set (getFrN (map snd txs) (map fst txs) [scnj F] (length txs)) \<inter> set (map snd txs) = {}; \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [scnj F] \<subseteq> fmla\<rbrakk> \<Longrightarrow> length (getFrN (map snd txs) (map fst txs) [scnj F] (length txs)) = length txs\<rbrakk> \<Longrightarrow> set (getFrN (map snd txs) (map fst txs) [scnj F] (length txs)) \<inter> \<Union> (FvarsT ` fst ` set txs) = {}
 2. \<lbrakk>F \<subseteq> fmla; finite F; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; distinct (map snd txs); \<And>\<phi>. \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [scnj F] \<subseteq> fmla; \<phi> \<in> set [scnj F]\<rbrakk> \<Longrightarrow> set (getFrN (map snd txs) (map fst txs) [scnj F] (length txs)) \<inter> Fvars \<phi> = {}; \<And>t. \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [scnj F] \<subseteq> fmla; t \<in> set (map fst txs)\<rbrakk> \<Longrightarrow> set (getFrN (map snd txs) (map fst txs) [scnj F] (length txs)) \<inter> FvarsT t = {}; \<And>t. \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [scnj F] \<subseteq> fmla; t \<in> set (map fst txs)\<rbrakk> \<Longrightarrow> set (getFrN (map snd txs) (map fst txs) [scnj F] (length txs)) \<inter> set (map snd txs) = {}; \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [scnj F] \<subseteq> fmla\<rbrakk> \<Longrightarrow> length (getFrN (map snd txs) (map fst txs) [scnj F] (length txs)) = length txs\<rbrakk> \<Longrightarrow> set (getFrN (map snd txs) (map fst txs) [scnj F] (length txs)) \<inter> snd ` set txs = {}
 3. \<lbrakk>F \<subseteq> fmla; finite F; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; distinct (map snd txs); \<And>\<phi>. \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [scnj F] \<subseteq> fmla; \<phi> \<in> set [scnj F]\<rbrakk> \<Longrightarrow> set (getFrN (map snd txs) (map fst txs) [scnj F] (length txs)) \<inter> Fvars \<phi> = {}; \<And>t. \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [scnj F] \<subseteq> fmla; t \<in> set (map fst txs)\<rbrakk> \<Longrightarrow> set (getFrN (map snd txs) (map fst txs) [scnj F] (length txs)) \<inter> FvarsT t = {}; \<And>t. \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [scnj F] \<subseteq> fmla; t \<in> set (map fst txs)\<rbrakk> \<Longrightarrow> set (getFrN (map snd txs) (map fst txs) [scnj F] (length txs)) \<inter> set (map snd txs) = {}; \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [scnj F] \<subseteq> fmla\<rbrakk> \<Longrightarrow> length (getFrN (map snd txs) (map fst txs) [scnj F] (length txs)) = length txs\<rbrakk> \<Longrightarrow> length (getFrN (map snd txs) (map fst txs) [scnj F] (length txs)) = length txs
 4. \<lbrakk>F \<subseteq> fmla; finite F; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; distinct (map snd txs); \<And>\<phi>. \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [scnj F] \<subseteq> fmla; \<phi> \<in> set [scnj F]\<rbrakk> \<Longrightarrow> set (getFrN (map snd txs) (map fst txs) [scnj F] (length txs)) \<inter> Fvars \<phi> = {}; \<And>t. \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [scnj F] \<subseteq> fmla; t \<in> set (map fst txs)\<rbrakk> \<Longrightarrow> set (getFrN (map snd txs) (map fst txs) [scnj F] (length txs)) \<inter> FvarsT t = {}; \<And>t. \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [scnj F] \<subseteq> fmla; t \<in> set (map fst txs)\<rbrakk> \<Longrightarrow> set (getFrN (map snd txs) (map fst txs) [scnj F] (length txs)) \<inter> set (map snd txs) = {}; \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [scnj F] \<subseteq> fmla\<rbrakk> \<Longrightarrow> length (getFrN (map snd txs) (map fst txs) [scnj F] (length txs)) = length txs\<rbrakk> \<Longrightarrow> distinct (getFrN (map snd txs) (map fst txs) [scnj F] (length txs))
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>F \<subseteq> fmla; finite F; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; distinct (map snd txs); \<And>\<phi>. \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [scnj F] \<subseteq> fmla; \<phi> \<in> set [scnj F]\<rbrakk> \<Longrightarrow> set (getFrN (map snd txs) (map fst txs) [scnj F] (length txs)) \<inter> Fvars \<phi> = {}; \<And>t. \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [scnj F] \<subseteq> fmla; t \<in> set (map fst txs)\<rbrakk> \<Longrightarrow> set (getFrN (map snd txs) (map fst txs) [scnj F] (length txs)) \<inter> FvarsT t = {}; \<And>t. \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [scnj F] \<subseteq> fmla; t \<in> set (map fst txs)\<rbrakk> \<Longrightarrow> set (getFrN (map snd txs) (map fst txs) [scnj F] (length txs)) \<inter> set (map snd txs) = {}; \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [scnj F] \<subseteq> fmla\<rbrakk> \<Longrightarrow> length (getFrN (map snd txs) (map fst txs) [scnj F] (length txs)) = length txs\<rbrakk> \<Longrightarrow> set (getFrN (map snd txs) (map fst txs) [scnj F] (length txs)) \<inter> \<Union> (FvarsT ` fst ` set txs) = {}
[PROOF STEP]
by (fastforce simp: image_iff)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>F \<subseteq> fmla; finite F; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; distinct (map snd txs); \<And>\<phi>. \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [scnj F] \<subseteq> fmla; \<phi> \<in> set [scnj F]\<rbrakk> \<Longrightarrow> set (getFrN (map snd txs) (map fst txs) [scnj F] (length txs)) \<inter> Fvars \<phi> = {}; \<And>t. \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [scnj F] \<subseteq> fmla; t \<in> set (map fst txs)\<rbrakk> \<Longrightarrow> set (getFrN (map snd txs) (map fst txs) [scnj F] (length txs)) \<inter> FvarsT t = {}; \<And>t. \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [scnj F] \<subseteq> fmla; t \<in> set (map fst txs)\<rbrakk> \<Longrightarrow> set (getFrN (map snd txs) (map fst txs) [scnj F] (length txs)) \<inter> set (map snd txs) = {}; \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [scnj F] \<subseteq> fmla\<rbrakk> \<Longrightarrow> length (getFrN (map snd txs) (map fst txs) [scnj F] (length txs)) = length txs\<rbrakk> \<Longrightarrow> set (getFrN (map snd txs) (map fst txs) [scnj F] (length txs)) \<inter> snd ` set txs = {}
 2. \<lbrakk>F \<subseteq> fmla; finite F; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; distinct (map snd txs); \<And>\<phi>. \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [scnj F] \<subseteq> fmla; \<phi> \<in> set [scnj F]\<rbrakk> \<Longrightarrow> set (getFrN (map snd txs) (map fst txs) [scnj F] (length txs)) \<inter> Fvars \<phi> = {}; \<And>t. \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [scnj F] \<subseteq> fmla; t \<in> set (map fst txs)\<rbrakk> \<Longrightarrow> set (getFrN (map snd txs) (map fst txs) [scnj F] (length txs)) \<inter> FvarsT t = {}; \<And>t. \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [scnj F] \<subseteq> fmla; t \<in> set (map fst txs)\<rbrakk> \<Longrightarrow> set (getFrN (map snd txs) (map fst txs) [scnj F] (length txs)) \<inter> set (map snd txs) = {}; \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [scnj F] \<subseteq> fmla\<rbrakk> \<Longrightarrow> length (getFrN (map snd txs) (map fst txs) [scnj F] (length txs)) = length txs\<rbrakk> \<Longrightarrow> length (getFrN (map snd txs) (map fst txs) [scnj F] (length txs)) = length txs
 3. \<lbrakk>F \<subseteq> fmla; finite F; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; distinct (map snd txs); \<And>\<phi>. \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [scnj F] \<subseteq> fmla; \<phi> \<in> set [scnj F]\<rbrakk> \<Longrightarrow> set (getFrN (map snd txs) (map fst txs) [scnj F] (length txs)) \<inter> Fvars \<phi> = {}; \<And>t. \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [scnj F] \<subseteq> fmla; t \<in> set (map fst txs)\<rbrakk> \<Longrightarrow> set (getFrN (map snd txs) (map fst txs) [scnj F] (length txs)) \<inter> FvarsT t = {}; \<And>t. \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [scnj F] \<subseteq> fmla; t \<in> set (map fst txs)\<rbrakk> \<Longrightarrow> set (getFrN (map snd txs) (map fst txs) [scnj F] (length txs)) \<inter> set (map snd txs) = {}; \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [scnj F] \<subseteq> fmla\<rbrakk> \<Longrightarrow> length (getFrN (map snd txs) (map fst txs) [scnj F] (length txs)) = length txs\<rbrakk> \<Longrightarrow> distinct (getFrN (map snd txs) (map fst txs) [scnj F] (length txs))
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>F \<subseteq> fmla; finite F; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; distinct (map snd txs); \<And>\<phi>. \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [scnj F] \<subseteq> fmla; \<phi> \<in> set [scnj F]\<rbrakk> \<Longrightarrow> set (getFrN (map snd txs) (map fst txs) [scnj F] (length txs)) \<inter> Fvars \<phi> = {}; \<And>t. \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [scnj F] \<subseteq> fmla; t \<in> set (map fst txs)\<rbrakk> \<Longrightarrow> set (getFrN (map snd txs) (map fst txs) [scnj F] (length txs)) \<inter> FvarsT t = {}; \<And>t. \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [scnj F] \<subseteq> fmla; t \<in> set (map fst txs)\<rbrakk> \<Longrightarrow> set (getFrN (map snd txs) (map fst txs) [scnj F] (length txs)) \<inter> set (map snd txs) = {}; \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [scnj F] \<subseteq> fmla\<rbrakk> \<Longrightarrow> length (getFrN (map snd txs) (map fst txs) [scnj F] (length txs)) = length txs\<rbrakk> \<Longrightarrow> set (getFrN (map snd txs) (map fst txs) [scnj F] (length txs)) \<inter> snd ` set txs = {}
[PROOF STEP]
by (fastforce simp: image_iff)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>F \<subseteq> fmla; finite F; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; distinct (map snd txs); \<And>\<phi>. \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [scnj F] \<subseteq> fmla; \<phi> \<in> set [scnj F]\<rbrakk> \<Longrightarrow> set (getFrN (map snd txs) (map fst txs) [scnj F] (length txs)) \<inter> Fvars \<phi> = {}; \<And>t. \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [scnj F] \<subseteq> fmla; t \<in> set (map fst txs)\<rbrakk> \<Longrightarrow> set (getFrN (map snd txs) (map fst txs) [scnj F] (length txs)) \<inter> FvarsT t = {}; \<And>t. \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [scnj F] \<subseteq> fmla; t \<in> set (map fst txs)\<rbrakk> \<Longrightarrow> set (getFrN (map snd txs) (map fst txs) [scnj F] (length txs)) \<inter> set (map snd txs) = {}; \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [scnj F] \<subseteq> fmla\<rbrakk> \<Longrightarrow> length (getFrN (map snd txs) (map fst txs) [scnj F] (length txs)) = length txs\<rbrakk> \<Longrightarrow> length (getFrN (map snd txs) (map fst txs) [scnj F] (length txs)) = length txs
 2. \<lbrakk>F \<subseteq> fmla; finite F; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; distinct (map snd txs); \<And>\<phi>. \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [scnj F] \<subseteq> fmla; \<phi> \<in> set [scnj F]\<rbrakk> \<Longrightarrow> set (getFrN (map snd txs) (map fst txs) [scnj F] (length txs)) \<inter> Fvars \<phi> = {}; \<And>t. \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [scnj F] \<subseteq> fmla; t \<in> set (map fst txs)\<rbrakk> \<Longrightarrow> set (getFrN (map snd txs) (map fst txs) [scnj F] (length txs)) \<inter> FvarsT t = {}; \<And>t. \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [scnj F] \<subseteq> fmla; t \<in> set (map fst txs)\<rbrakk> \<Longrightarrow> set (getFrN (map snd txs) (map fst txs) [scnj F] (length txs)) \<inter> set (map snd txs) = {}; \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [scnj F] \<subseteq> fmla\<rbrakk> \<Longrightarrow> length (getFrN (map snd txs) (map fst txs) [scnj F] (length txs)) = length txs\<rbrakk> \<Longrightarrow> distinct (getFrN (map snd txs) (map fst txs) [scnj F] (length txs))
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>F \<subseteq> fmla; finite F; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; distinct (map snd txs); \<And>\<phi>. \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [scnj F] \<subseteq> fmla; \<phi> \<in> set [scnj F]\<rbrakk> \<Longrightarrow> set (getFrN (map snd txs) (map fst txs) [scnj F] (length txs)) \<inter> Fvars \<phi> = {}; \<And>t. \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [scnj F] \<subseteq> fmla; t \<in> set (map fst txs)\<rbrakk> \<Longrightarrow> set (getFrN (map snd txs) (map fst txs) [scnj F] (length txs)) \<inter> FvarsT t = {}; \<And>t. \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [scnj F] \<subseteq> fmla; t \<in> set (map fst txs)\<rbrakk> \<Longrightarrow> set (getFrN (map snd txs) (map fst txs) [scnj F] (length txs)) \<inter> set (map snd txs) = {}; \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [scnj F] \<subseteq> fmla\<rbrakk> \<Longrightarrow> length (getFrN (map snd txs) (map fst txs) [scnj F] (length txs)) = length txs\<rbrakk> \<Longrightarrow> length (getFrN (map snd txs) (map fst txs) [scnj F] (length txs)) = length txs
[PROOF STEP]
by (fastforce simp: image_iff)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>F \<subseteq> fmla; finite F; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; distinct (map snd txs); \<And>\<phi>. \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [scnj F] \<subseteq> fmla; \<phi> \<in> set [scnj F]\<rbrakk> \<Longrightarrow> set (getFrN (map snd txs) (map fst txs) [scnj F] (length txs)) \<inter> Fvars \<phi> = {}; \<And>t. \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [scnj F] \<subseteq> fmla; t \<in> set (map fst txs)\<rbrakk> \<Longrightarrow> set (getFrN (map snd txs) (map fst txs) [scnj F] (length txs)) \<inter> FvarsT t = {}; \<And>t. \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [scnj F] \<subseteq> fmla; t \<in> set (map fst txs)\<rbrakk> \<Longrightarrow> set (getFrN (map snd txs) (map fst txs) [scnj F] (length txs)) \<inter> set (map snd txs) = {}; \<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [scnj F] \<subseteq> fmla\<rbrakk> \<Longrightarrow> length (getFrN (map snd txs) (map fst txs) [scnj F] (length txs)) = length txs\<rbrakk> \<Longrightarrow> distinct (getFrN (map snd txs) (map fst txs) [scnj F] (length txs))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
set us \<subseteq> var
set us \<inter> \<Union> (Fvars ` F) = {}
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 (eqv (psubst (scnj F) txs) (scnj ((\<lambda>\<phi>. psubst \<phi> txs) ` F)))
[PROOF STEP]
define vs where vs: "vs \<equiv> \<lambda> \<phi>. getFrN (map snd txs) (map fst txs) [\<phi>] (length txs)"
[PROOF STATE]
proof (state)
this:
vs \<equiv> \<lambda>\<phi>. getFrN (map snd txs) (map fst txs) [\<phi>] (length txs)

goal (1 subgoal):
 1. prv (eqv (psubst (scnj F) txs) (scnj ((\<lambda>\<phi>. psubst \<phi> txs) ` F)))
[PROOF STEP]
hence vss: "\<And>\<phi>. vs \<phi> = getFrN (map snd txs) (map fst txs) [\<phi>] (length txs)"
[PROOF STATE]
proof (prove)
using this:
vs \<equiv> \<lambda>\<phi>. getFrN (map snd txs) (map fst txs) [\<phi>] (length txs)

goal (1 subgoal):
 1. \<And>\<phi>. vs \<phi> = getFrN (map snd txs) (map fst txs) [\<phi>] (length txs)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
vs ?\<phi> = getFrN (map snd txs) (map fst txs) [?\<phi>] (length txs)

goal (1 subgoal):
 1. prv (eqv (psubst (scnj F) txs) (scnj ((\<lambda>\<phi>. psubst \<phi> txs) ` F)))
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
vs ?\<phi> = getFrN (map snd txs) (map fst txs) [?\<phi>] (length txs)

goal (1 subgoal):
 1. prv (eqv (psubst (scnj F) txs) (scnj ((\<lambda>\<phi>. psubst \<phi> txs) ` F)))
[PROOF STEP]
fix \<phi>
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. prv (eqv (psubst (scnj F) txs) (scnj ((\<lambda>\<phi>. psubst \<phi> txs) ` F)))
[PROOF STEP]
assume "\<phi> \<in> F"
[PROOF STATE]
proof (state)
this:
\<phi> \<in> F

goal (1 subgoal):
 1. prv (eqv (psubst (scnj F) txs) (scnj ((\<lambda>\<phi>. psubst \<phi> txs) ` F)))
[PROOF STEP]
hence "\<phi> \<in> fmla"
[PROOF STATE]
proof (prove)
using this:
\<phi> \<in> F

goal (1 subgoal):
 1. \<phi> \<in> fmla
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<phi> \<in> F
F \<subseteq> fmla
finite F
snd ` set txs \<subseteq> var
fst ` set txs \<subseteq> trm
distinct (map snd txs)

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

goal (1 subgoal):
 1. prv (eqv (psubst (scnj F) txs) (scnj ((\<lambda>\<phi>. psubst \<phi> txs) ` F)))
[PROOF STEP]
hence "set (vs \<phi>)  \<subseteq> var \<and>
    set (vs \<phi>) \<inter> Fvars \<phi> = {} \<and>
    set (vs \<phi>) \<inter> \<Union> (FvarsT ` (fst ` (set txs))) = {} \<and>
    set (vs \<phi>) \<inter> snd ` (set txs) = {} \<and>
    length (vs \<phi>) = length txs \<and>
    distinct (vs \<phi>)"
[PROOF STATE]
proof (prove)
using this:
\<phi> \<in> fmla

goal (1 subgoal):
 1. set (vs \<phi>) \<subseteq> var \<and> set (vs \<phi>) \<inter> Fvars \<phi> = {} \<and> set (vs \<phi>) \<inter> \<Union> (FvarsT ` fst ` set txs) = {} \<and> set (vs \<phi>) \<inter> snd ` set txs = {} \<and> length (vs \<phi>) = length txs \<and> distinct (vs \<phi>)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<phi> \<in> fmla
F \<subseteq> fmla
finite F
snd ` set txs \<subseteq> var
fst ` set txs \<subseteq> trm
distinct (map snd txs)

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

goal (1 subgoal):
 1. set (getFrN (map snd txs) (map fst txs) [\<phi>] (length txs)) \<subseteq> var \<and> set (getFrN (map snd txs) (map fst txs) [\<phi>] (length txs)) \<inter> Fvars \<phi> = {} \<and> set (getFrN (map snd txs) (map fst txs) [\<phi>] (length txs)) \<inter> \<Union> (FvarsT ` fst ` set txs) = {} \<and> set (getFrN (map snd txs) (map fst txs) [\<phi>] (length txs)) \<inter> snd ` set txs = {} \<and> length (getFrN (map snd txs) (map fst txs) [\<phi>] (length txs)) = length txs \<and> distinct (getFrN (map snd txs) (map fst txs) [\<phi>] (length txs))
[PROOF STEP]
using getFrN_Fvars[of "map snd txs" "map fst txs" "[\<phi>]" _ "length txs"]
        getFrN_FvarsT[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"]
[PROOF STATE]
proof (prove)
using this:
\<phi> \<in> fmla
F \<subseteq> fmla
finite F
snd ` set txs \<subseteq> var
fst ` set txs \<subseteq> trm
distinct (map snd txs)
\<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> FvarsT ?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

goal (1 subgoal):
 1. set (getFrN (map snd txs) (map fst txs) [\<phi>] (length txs)) \<subseteq> var \<and> set (getFrN (map snd txs) (map fst txs) [\<phi>] (length txs)) \<inter> Fvars \<phi> = {} \<and> set (getFrN (map snd txs) (map fst txs) [\<phi>] (length txs)) \<inter> \<Union> (FvarsT ` fst ` set txs) = {} \<and> set (getFrN (map snd txs) (map fst txs) [\<phi>] (length txs)) \<inter> snd ` set txs = {} \<and> length (getFrN (map snd txs) (map fst txs) [\<phi>] (length txs)) = length txs \<and> distinct (getFrN (map snd txs) (map fst txs) [\<phi>] (length txs))
[PROOF STEP]
apply (intro conjI)
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<lbrakk>\<phi> \<in> fmla; F \<subseteq> fmla; finite F; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; distinct (map snd txs); \<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> FvarsT t = {}; \<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\<rbrakk> \<Longrightarrow> set (getFrN (map snd txs) (map fst txs) [\<phi>] (length txs)) \<subseteq> var
 2. \<lbrakk>\<phi> \<in> fmla; F \<subseteq> fmla; finite F; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; distinct (map snd txs); \<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> FvarsT t = {}; \<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\<rbrakk> \<Longrightarrow> set (getFrN (map snd txs) (map fst txs) [\<phi>] (length txs)) \<inter> Fvars \<phi> = {}
 3. \<lbrakk>\<phi> \<in> fmla; F \<subseteq> fmla; finite F; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; distinct (map snd txs); \<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> FvarsT t = {}; \<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\<rbrakk> \<Longrightarrow> set (getFrN (map snd txs) (map fst txs) [\<phi>] (length txs)) \<inter> \<Union> (FvarsT ` fst ` set txs) = {}
 4. \<lbrakk>\<phi> \<in> fmla; F \<subseteq> fmla; finite F; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; distinct (map snd txs); \<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> FvarsT t = {}; \<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\<rbrakk> \<Longrightarrow> set (getFrN (map snd txs) (map fst txs) [\<phi>] (length txs)) \<inter> snd ` set txs = {}
 5. \<lbrakk>\<phi> \<in> fmla; F \<subseteq> fmla; finite F; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; distinct (map snd txs); \<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> FvarsT t = {}; \<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\<rbrakk> \<Longrightarrow> length (getFrN (map snd txs) (map fst txs) [\<phi>] (length txs)) = length txs
 6. \<lbrakk>\<phi> \<in> fmla; F \<subseteq> fmla; finite F; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; distinct (map snd txs); \<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> FvarsT t = {}; \<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\<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; F \<subseteq> fmla; finite F; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; distinct (map snd txs); \<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> FvarsT t = {}; \<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\<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; F \<subseteq> fmla; finite F; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; distinct (map snd txs); \<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> FvarsT t = {}; \<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\<rbrakk> \<Longrightarrow> set (getFrN (map snd txs) (map fst txs) [\<phi>] (length txs)) \<inter> Fvars \<phi> = {}
 2. \<lbrakk>\<phi> \<in> fmla; F \<subseteq> fmla; finite F; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; distinct (map snd txs); \<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> FvarsT t = {}; \<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\<rbrakk> \<Longrightarrow> set (getFrN (map snd txs) (map fst txs) [\<phi>] (length txs)) \<inter> \<Union> (FvarsT ` fst ` set txs) = {}
 3. \<lbrakk>\<phi> \<in> fmla; F \<subseteq> fmla; finite F; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; distinct (map snd txs); \<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> FvarsT t = {}; \<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\<rbrakk> \<Longrightarrow> set (getFrN (map snd txs) (map fst txs) [\<phi>] (length txs)) \<inter> snd ` set txs = {}
 4. \<lbrakk>\<phi> \<in> fmla; F \<subseteq> fmla; finite F; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; distinct (map snd txs); \<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> FvarsT t = {}; \<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\<rbrakk> \<Longrightarrow> length (getFrN (map snd txs) (map fst txs) [\<phi>] (length txs)) = length txs
 5. \<lbrakk>\<phi> \<in> fmla; F \<subseteq> fmla; finite F; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; distinct (map snd txs); \<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> FvarsT t = {}; \<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\<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; F \<subseteq> fmla; finite F; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; distinct (map snd txs); \<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> FvarsT t = {}; \<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\<rbrakk> \<Longrightarrow> set (getFrN (map snd txs) (map fst txs) [\<phi>] (length txs)) \<inter> Fvars \<phi> = {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>\<phi> \<in> fmla; F \<subseteq> fmla; finite F; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; distinct (map snd txs); \<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> FvarsT t = {}; \<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\<rbrakk> \<Longrightarrow> set (getFrN (map snd txs) (map fst txs) [\<phi>] (length txs)) \<inter> \<Union> (FvarsT ` fst ` set txs) = {}
 2. \<lbrakk>\<phi> \<in> fmla; F \<subseteq> fmla; finite F; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; distinct (map snd txs); \<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> FvarsT t = {}; \<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\<rbrakk> \<Longrightarrow> set (getFrN (map snd txs) (map fst txs) [\<phi>] (length txs)) \<inter> snd ` set txs = {}
 3. \<lbrakk>\<phi> \<in> fmla; F \<subseteq> fmla; finite F; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; distinct (map snd txs); \<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> FvarsT t = {}; \<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\<rbrakk> \<Longrightarrow> length (getFrN (map snd txs) (map fst txs) [\<phi>] (length txs)) = length txs
 4. \<lbrakk>\<phi> \<in> fmla; F \<subseteq> fmla; finite F; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; distinct (map snd txs); \<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> FvarsT t = {}; \<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\<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; F \<subseteq> fmla; finite F; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; distinct (map snd txs); \<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> FvarsT t = {}; \<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\<rbrakk> \<Longrightarrow> set (getFrN (map snd txs) (map fst txs) [\<phi>] (length txs)) \<inter> \<Union> (FvarsT ` fst ` set txs) = {}
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>\<phi> \<in> fmla; F \<subseteq> fmla; finite F; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; distinct (map snd txs); \<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> FvarsT t = {}; \<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\<rbrakk> \<Longrightarrow> set (getFrN (map snd txs) (map fst txs) [\<phi>] (length txs)) \<inter> snd ` set txs = {}
 2. \<lbrakk>\<phi> \<in> fmla; F \<subseteq> fmla; finite F; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; distinct (map snd txs); \<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> FvarsT t = {}; \<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\<rbrakk> \<Longrightarrow> length (getFrN (map snd txs) (map fst txs) [\<phi>] (length txs)) = length txs
 3. \<lbrakk>\<phi> \<in> fmla; F \<subseteq> fmla; finite F; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; distinct (map snd txs); \<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> FvarsT t = {}; \<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\<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; F \<subseteq> fmla; finite F; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; distinct (map snd txs); \<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> FvarsT t = {}; \<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\<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; F \<subseteq> fmla; finite F; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; distinct (map snd txs); \<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> FvarsT t = {}; \<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\<rbrakk> \<Longrightarrow> length (getFrN (map snd txs) (map fst txs) [\<phi>] (length txs)) = length txs
 2. \<lbrakk>\<phi> \<in> fmla; F \<subseteq> fmla; finite F; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; distinct (map snd txs); \<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> FvarsT t = {}; \<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\<rbrakk> \<Longrightarrow> distinct (getFrN (map snd txs) (map fst txs) [\<phi>] (length txs))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
set (vs \<phi>) \<subseteq> var \<and> set (vs \<phi>) \<inter> Fvars \<phi> = {} \<and> set (vs \<phi>) \<inter> \<Union> (FvarsT ` fst ` set txs) = {} \<and> set (vs \<phi>) \<inter> snd ` set txs = {} \<and> length (vs \<phi>) = length txs \<and> distinct (vs \<phi>)

goal (1 subgoal):
 1. prv (eqv (psubst (scnj F) txs) (scnj ((\<lambda>\<phi>. psubst \<phi> txs) ` F)))
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?\<phi>2 \<in> F \<Longrightarrow> set (vs ?\<phi>2) \<subseteq> var \<and> set (vs ?\<phi>2) \<inter> Fvars ?\<phi>2 = {} \<and> set (vs ?\<phi>2) \<inter> \<Union> (FvarsT ` fst ` set txs) = {} \<and> set (vs ?\<phi>2) \<inter> snd ` set txs = {} \<and> length (vs ?\<phi>2) = length txs \<and> distinct (vs ?\<phi>2)

goal (1 subgoal):
 1. prv (eqv (psubst (scnj F) txs) (scnj ((\<lambda>\<phi>. psubst \<phi> txs) ` F)))
[PROOF STEP]
note vs_facts = this
[PROOF STATE]
proof (state)
this:
?\<phi>2 \<in> F \<Longrightarrow> set (vs ?\<phi>2) \<subseteq> var \<and> set (vs ?\<phi>2) \<inter> Fvars ?\<phi>2 = {} \<and> set (vs ?\<phi>2) \<inter> \<Union> (FvarsT ` fst ` set txs) = {} \<and> set (vs ?\<phi>2) \<inter> snd ` set txs = {} \<and> length (vs ?\<phi>2) = length txs \<and> distinct (vs ?\<phi>2)

goal (1 subgoal):
 1. prv (eqv (psubst (scnj F) txs) (scnj ((\<lambda>\<phi>. psubst \<phi> txs) ` F)))
[PROOF STEP]
have [simp]: "\<And> x f. f \<in> F \<Longrightarrow> x \<in> set (vs f) \<Longrightarrow> x \<in> var"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x f. \<lbrakk>f \<in> F; x \<in> set (vs f)\<rbrakk> \<Longrightarrow> x \<in> var
[PROOF STEP]
using vs_facts
[PROOF STATE]
proof (prove)
using this:
?\<phi>2 \<in> F \<Longrightarrow> set (vs ?\<phi>2) \<subseteq> var \<and> set (vs ?\<phi>2) \<inter> Fvars ?\<phi>2 = {} \<and> set (vs ?\<phi>2) \<inter> \<Union> (FvarsT ` fst ` set txs) = {} \<and> set (vs ?\<phi>2) \<inter> snd ` set txs = {} \<and> length (vs ?\<phi>2) = length txs \<and> distinct (vs ?\<phi>2)

goal (1 subgoal):
 1. \<And>x f. \<lbrakk>f \<in> F; x \<in> set (vs f)\<rbrakk> \<Longrightarrow> x \<in> var
[PROOF STEP]
by (meson subsetD)
[PROOF STATE]
proof (state)
this:
\<lbrakk>?f \<in> F; ?x \<in> set (vs ?f)\<rbrakk> \<Longrightarrow> ?x \<in> var

goal (1 subgoal):
 1. prv (eqv (psubst (scnj F) txs) (scnj ((\<lambda>\<phi>. psubst \<phi> txs) ` F)))
[PROOF STEP]
let ?tus = "zip (map fst txs) us"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. prv (eqv (psubst (scnj F) txs) (scnj ((\<lambda>\<phi>. psubst \<phi> txs) ` F)))
[PROOF STEP]
let ?uxs = "zip (map Var us) (map snd txs)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. prv (eqv (psubst (scnj F) txs) (scnj ((\<lambda>\<phi>. psubst \<phi> txs) ` F)))
[PROOF STEP]
let ?tvs = "\<lambda> \<phi>. zip (map fst txs) (vs \<phi>)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. prv (eqv (psubst (scnj F) txs) (scnj ((\<lambda>\<phi>. psubst \<phi> txs) ` F)))
[PROOF STEP]
let ?vxs = "\<lambda> \<phi>. zip (map Var (vs \<phi>)) (map snd txs)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. prv (eqv (psubst (scnj F) txs) (scnj ((\<lambda>\<phi>. psubst \<phi> txs) ` F)))
[PROOF STEP]
let ?c = "rawpsubst (scnj F) ?uxs"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. prv (eqv (psubst (scnj F) txs) (scnj ((\<lambda>\<phi>. psubst \<phi> txs) ` F)))
[PROOF STEP]
have c: "prv (eqv ?c
                   (scnj ((\<lambda>\<phi>. rawpsubst \<phi> ?uxs) ` F)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (eqv (rawpsubst (scnj F) (zip (map Var us) (map snd txs))) (scnj ((\<lambda>\<phi>. rawpsubst \<phi> (zip (map Var us) (map snd txs))) ` F)))
[PROOF STEP]
using assms us_facts
[PROOF STATE]
proof (prove)
using this:
F \<subseteq> fmla
finite F
snd ` set txs \<subseteq> var
fst ` set txs \<subseteq> trm
distinct (map snd txs)
set us \<subseteq> var
set us \<inter> \<Union> (Fvars ` F) = {}
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 (eqv (rawpsubst (scnj F) (zip (map Var us) (map snd txs))) (scnj ((\<lambda>\<phi>. rawpsubst \<phi> (zip (map Var us) (map snd txs))) ` F)))
[PROOF STEP]
by (intro prv_rawpsubst_scnj) (auto intro!: rawpsubstT dest!: set_zip_D)
[PROOF STATE]
proof (state)
this:
prv (eqv (rawpsubst (scnj F) (zip (map Var us) (map snd txs))) (scnj ((\<lambda>\<phi>. rawpsubst \<phi> (zip (map Var us) (map snd txs))) ` F)))

goal (1 subgoal):
 1. prv (eqv (psubst (scnj F) txs) (scnj ((\<lambda>\<phi>. psubst \<phi> txs) ` F)))
[PROOF STEP]
hence "prv (eqv (rawpsubst ?c ?tus)
                  (rawpsubst (scnj ((\<lambda>\<phi>. rawpsubst \<phi> ?uxs) ` F)) ?tus))"
[PROOF STATE]
proof (prove)
using this:
prv (eqv (rawpsubst (scnj F) (zip (map Var us) (map snd txs))) (scnj ((\<lambda>\<phi>. rawpsubst \<phi> (zip (map Var us) (map snd txs))) ` F)))

goal (1 subgoal):
 1. prv (eqv (rawpsubst (rawpsubst (scnj F) (zip (map Var us) (map snd txs))) (zip (map fst txs) us)) (rawpsubst (scnj ((\<lambda>\<phi>. rawpsubst \<phi> (zip (map Var us) (map snd txs))) ` F)) (zip (map fst txs) us)))
[PROOF STEP]
using assms us_facts
[PROOF STATE]
proof (prove)
using this:
prv (eqv (rawpsubst (scnj F) (zip (map Var us) (map snd txs))) (scnj ((\<lambda>\<phi>. rawpsubst \<phi> (zip (map Var us) (map snd txs))) ` F)))
F \<subseteq> fmla
finite F
snd ` set txs \<subseteq> var
fst ` set txs \<subseteq> trm
distinct (map snd txs)
set us \<subseteq> var
set us \<inter> \<Union> (Fvars ` F) = {}
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 (eqv (rawpsubst (rawpsubst (scnj F) (zip (map Var us) (map snd txs))) (zip (map fst txs) us)) (rawpsubst (scnj ((\<lambda>\<phi>. rawpsubst \<phi> (zip (map Var us) (map snd txs))) ` F)) (zip (map fst txs) us)))
[PROOF STEP]
by (intro prv_eqv_rawpsubst) (auto intro!: rawpsubst dest!: set_zip_D)
[PROOF STATE]
proof (state)
this:
prv (eqv (rawpsubst (rawpsubst (scnj F) (zip (map Var us) (map snd txs))) (zip (map fst txs) us)) (rawpsubst (scnj ((\<lambda>\<phi>. rawpsubst \<phi> (zip (map Var us) (map snd txs))) ` F)) (zip (map fst txs) us)))

goal (1 subgoal):
 1. prv (eqv (psubst (scnj F) txs) (scnj ((\<lambda>\<phi>. psubst \<phi> txs) ` F)))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
prv (eqv (rawpsubst (rawpsubst (scnj F) (zip (map Var us) (map snd txs))) (zip (map fst txs) us)) (rawpsubst (scnj ((\<lambda>\<phi>. rawpsubst \<phi> (zip (map Var us) (map snd txs))) ` F)) (zip (map fst txs) us)))

goal (1 subgoal):
 1. prv (eqv (psubst (scnj F) txs) (scnj ((\<lambda>\<phi>. psubst \<phi> txs) ` F)))
[PROOF STEP]
have "prv (eqv (rawpsubst (scnj ((\<lambda>\<phi>. rawpsubst \<phi> ?uxs) ` F)) ?tus)
                 (scnj ((\<lambda>\<phi>. rawpsubst \<phi> ?tus) ` ((\<lambda>\<phi>. rawpsubst \<phi> ?uxs) ` F))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (eqv (rawpsubst (scnj ((\<lambda>\<phi>. rawpsubst \<phi> (zip (map Var us) (map snd txs))) ` F)) (zip (map fst txs) us)) (scnj ((\<lambda>\<phi>. rawpsubst \<phi> (zip (map fst txs) us)) ` (\<lambda>\<phi>. rawpsubst \<phi> (zip (map Var us) (map snd txs))) ` F)))
[PROOF STEP]
using assms us_facts
[PROOF STATE]
proof (prove)
using this:
F \<subseteq> fmla
finite F
snd ` set txs \<subseteq> var
fst ` set txs \<subseteq> trm
distinct (map snd txs)
set us \<subseteq> var
set us \<inter> \<Union> (Fvars ` F) = {}
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 (eqv (rawpsubst (scnj ((\<lambda>\<phi>. rawpsubst \<phi> (zip (map Var us) (map snd txs))) ` F)) (zip (map fst txs) us)) (scnj ((\<lambda>\<phi>. rawpsubst \<phi> (zip (map fst txs) us)) ` (\<lambda>\<phi>. rawpsubst \<phi> (zip (map Var us) (map snd txs))) ` F)))
[PROOF STEP]
by (intro prv_rawpsubst_scnj) (auto intro!: rawpsubst dest!: set_zip_D)
[PROOF STATE]
proof (state)
this:
prv (eqv (rawpsubst (scnj ((\<lambda>\<phi>. rawpsubst \<phi> (zip (map Var us) (map snd txs))) ` F)) (zip (map fst txs) us)) (scnj ((\<lambda>\<phi>. rawpsubst \<phi> (zip (map fst txs) us)) ` (\<lambda>\<phi>. rawpsubst \<phi> (zip (map Var us) (map snd txs))) ` F)))

goal (1 subgoal):
 1. prv (eqv (psubst (scnj F) txs) (scnj ((\<lambda>\<phi>. psubst \<phi> txs) ` F)))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
prv (eqv (rawpsubst (rawpsubst (scnj F) (zip (map Var us) (map snd txs))) (zip (map fst txs) us)) (rawpsubst (scnj ((\<lambda>\<phi>. rawpsubst \<phi> (zip (map Var us) (map snd txs))) ` F)) (zip (map fst txs) us)))
prv (eqv (rawpsubst (scnj ((\<lambda>\<phi>. rawpsubst \<phi> (zip (map Var us) (map snd txs))) ` F)) (zip (map fst txs) us)) (scnj ((\<lambda>\<phi>. rawpsubst \<phi> (zip (map fst txs) us)) ` (\<lambda>\<phi>. rawpsubst \<phi> (zip (map Var us) (map snd txs))) ` F)))
[PROOF STEP]
have 0: "prv (eqv (rawpsubst ?c ?tus)
                    (scnj ((\<lambda>\<phi>. rawpsubst \<phi> ?tus) ` ((\<lambda>\<phi>. rawpsubst \<phi> ?uxs) ` F))))"
[PROOF STATE]
proof (prove)
using this:
prv (eqv (rawpsubst (rawpsubst (scnj F) (zip (map Var us) (map snd txs))) (zip (map fst txs) us)) (rawpsubst (scnj ((\<lambda>\<phi>. rawpsubst \<phi> (zip (map Var us) (map snd txs))) ` F)) (zip (map fst txs) us)))
prv (eqv (rawpsubst (scnj ((\<lambda>\<phi>. rawpsubst \<phi> (zip (map Var us) (map snd txs))) ` F)) (zip (map fst txs) us)) (scnj ((\<lambda>\<phi>. rawpsubst \<phi> (zip (map fst txs) us)) ` (\<lambda>\<phi>. rawpsubst \<phi> (zip (map Var us) (map snd txs))) ` F)))

goal (1 subgoal):
 1. prv (eqv (rawpsubst (rawpsubst (scnj F) (zip (map Var us) (map snd txs))) (zip (map fst txs) us)) (scnj ((\<lambda>\<phi>. rawpsubst \<phi> (zip (map fst txs) us)) ` (\<lambda>\<phi>. rawpsubst \<phi> (zip (map Var us) (map snd txs))) ` F)))
[PROOF STEP]
using assms us_facts
[PROOF STATE]
proof (prove)
using this:
prv (eqv (rawpsubst (rawpsubst (scnj F) (zip (map Var us) (map snd txs))) (zip (map fst txs) us)) (rawpsubst (scnj ((\<lambda>\<phi>. rawpsubst \<phi> (zip (map Var us) (map snd txs))) ` F)) (zip (map fst txs) us)))
prv (eqv (rawpsubst (scnj ((\<lambda>\<phi>. rawpsubst \<phi> (zip (map Var us) (map snd txs))) ` F)) (zip (map fst txs) us)) (scnj ((\<lambda>\<phi>. rawpsubst \<phi> (zip (map fst txs) us)) ` (\<lambda>\<phi>. rawpsubst \<phi> (zip (map Var us) (map snd txs))) ` F)))
F \<subseteq> fmla
finite F
snd ` set txs \<subseteq> var
fst ` set txs \<subseteq> trm
distinct (map snd txs)
set us \<subseteq> var
set us \<inter> \<Union> (Fvars ` F) = {}
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 (eqv (rawpsubst (rawpsubst (scnj F) (zip (map Var us) (map snd txs))) (zip (map fst txs) us)) (scnj ((\<lambda>\<phi>. rawpsubst \<phi> (zip (map fst txs) us)) ` (\<lambda>\<phi>. rawpsubst \<phi> (zip (map Var us) (map snd txs))) ` F)))
[PROOF STEP]
apply -
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>prv (eqv (rawpsubst (rawpsubst (scnj F) (zip (map Var us) (map snd txs))) (zip (map fst txs) us)) (rawpsubst (scnj ((\<lambda>\<phi>. rawpsubst \<phi> (zip (map Var us) (map snd txs))) ` F)) (zip (map fst txs) us))); prv (eqv (rawpsubst (scnj ((\<lambda>\<phi>. rawpsubst \<phi> (zip (map Var us) (map snd txs))) ` F)) (zip (map fst txs) us)) (scnj ((\<lambda>\<phi>. rawpsubst \<phi> (zip (map fst txs) us)) ` (\<lambda>\<phi>. rawpsubst \<phi> (zip (map Var us) (map snd txs))) ` F))); F \<subseteq> fmla; finite F; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; distinct (map snd txs); set us \<subseteq> var; set us \<inter> \<Union> (Fvars ` F) = {}; set us \<inter> \<Union> (FvarsT ` fst ` set txs) = {}; set us \<inter> snd ` set txs = {}; length us = length txs; distinct us\<rbrakk> \<Longrightarrow> prv (eqv (rawpsubst (rawpsubst (scnj F) (zip (map Var us) (map snd txs))) (zip (map fst txs) us)) (scnj ((\<lambda>\<phi>. rawpsubst \<phi> (zip (map fst txs) us)) ` (\<lambda>\<phi>. rawpsubst \<phi> (zip (map Var us) (map snd txs))) ` F)))
[PROOF STEP]
by (rule prv_eqv_trans) (auto intro!: rawpsubst dest!: set_zip_D)
[PROOF STATE]
proof (state)
this:
prv (eqv (rawpsubst (rawpsubst (scnj F) (zip (map Var us) (map snd txs))) (zip (map fst txs) us)) (scnj ((\<lambda>\<phi>. rawpsubst \<phi> (zip (map fst txs) us)) ` (\<lambda>\<phi>. rawpsubst \<phi> (zip (map Var us) (map snd txs))) ` F)))

goal (1 subgoal):
 1. prv (eqv (psubst (scnj F) txs) (scnj ((\<lambda>\<phi>. psubst \<phi> txs) ` F)))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
prv (eqv (rawpsubst (rawpsubst (scnj F) (zip (map Var us) (map snd txs))) (zip (map fst txs) us)) (scnj ((\<lambda>\<phi>. rawpsubst \<phi> (zip (map fst txs) us)) ` (\<lambda>\<phi>. rawpsubst \<phi> (zip (map Var us) (map snd txs))) ` F)))

goal (1 subgoal):
 1. prv (eqv (psubst (scnj F) txs) (scnj ((\<lambda>\<phi>. psubst \<phi> txs) ` F)))
[PROOF STEP]
have "prv (eqv (scnj ((\<lambda>\<phi>. rawpsubst \<phi> ?tus) ` ((\<lambda>\<phi>. rawpsubst \<phi> ?uxs) ` F)))
                 (scnj ((\<lambda>\<phi>. rawpsubst (rawpsubst \<phi> (?vxs \<phi>)) (?tvs \<phi>)) ` F)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (eqv (scnj ((\<lambda>\<phi>. rawpsubst \<phi> (zip (map fst txs) us)) ` (\<lambda>\<phi>. rawpsubst \<phi> (zip (map Var us) (map snd txs))) ` F)) (scnj ((\<lambda>\<phi>. rawpsubst (rawpsubst \<phi> (zip (map Var (vs \<phi>)) (map snd txs))) (zip (map fst txs) (vs \<phi>))) ` F)))
[PROOF STEP]
using assms us_facts vs_facts
[PROOF STATE]
proof (prove)
using this:
F \<subseteq> fmla
finite F
snd ` set txs \<subseteq> var
fst ` set txs \<subseteq> trm
distinct (map snd txs)
set us \<subseteq> var
set us \<inter> \<Union> (Fvars ` F) = {}
set us \<inter> \<Union> (FvarsT ` fst ` set txs) = {}
set us \<inter> snd ` set txs = {}
length us = length txs
distinct us
?\<phi>2 \<in> F \<Longrightarrow> set (vs ?\<phi>2) \<subseteq> var \<and> set (vs ?\<phi>2) \<inter> Fvars ?\<phi>2 = {} \<and> set (vs ?\<phi>2) \<inter> \<Union> (FvarsT ` fst ` set txs) = {} \<and> set (vs ?\<phi>2) \<inter> snd ` set txs = {} \<and> length (vs ?\<phi>2) = length txs \<and> distinct (vs ?\<phi>2)

goal (1 subgoal):
 1. prv (eqv (scnj ((\<lambda>\<phi>. rawpsubst \<phi> (zip (map fst txs) us)) ` (\<lambda>\<phi>. rawpsubst \<phi> (zip (map Var us) (map snd txs))) ` F)) (scnj ((\<lambda>\<phi>. rawpsubst (rawpsubst \<phi> (zip (map Var (vs \<phi>)) (map snd txs))) (zip (map fst txs) (vs \<phi>))) ` F)))
[PROOF STEP]
apply(intro prv_eqvI)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>F \<subseteq> fmla; finite F; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; distinct (map snd txs); set us \<subseteq> var; set us \<inter> \<Union> (Fvars ` F) = {}; set us \<inter> \<Union> (FvarsT ` fst ` set txs) = {}; set us \<inter> snd ` set txs = {}; length us = length txs; distinct us; \<And>\<phi>. \<phi> \<in> F \<Longrightarrow> set (vs \<phi>) \<subseteq> var \<and> set (vs \<phi>) \<inter> Fvars \<phi> = {} \<and> set (vs \<phi>) \<inter> \<Union> (FvarsT ` fst ` set txs) = {} \<and> set (vs \<phi>) \<inter> snd ` set txs = {} \<and> length (vs \<phi>) = length txs \<and> distinct (vs \<phi>)\<rbrakk> \<Longrightarrow> scnj ((\<lambda>\<phi>. rawpsubst \<phi> (zip (map fst txs) us)) ` (\<lambda>\<phi>. rawpsubst \<phi> (zip (map Var us) (map snd txs))) ` F) \<in> fmla
 2. \<lbrakk>F \<subseteq> fmla; finite F; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; distinct (map snd txs); set us \<subseteq> var; set us \<inter> \<Union> (Fvars ` F) = {}; set us \<inter> \<Union> (FvarsT ` fst ` set txs) = {}; set us \<inter> snd ` set txs = {}; length us = length txs; distinct us; \<And>\<phi>. \<phi> \<in> F \<Longrightarrow> set (vs \<phi>) \<subseteq> var \<and> set (vs \<phi>) \<inter> Fvars \<phi> = {} \<and> set (vs \<phi>) \<inter> \<Union> (FvarsT ` fst ` set txs) = {} \<and> set (vs \<phi>) \<inter> snd ` set txs = {} \<and> length (vs \<phi>) = length txs \<and> distinct (vs \<phi>)\<rbrakk> \<Longrightarrow> scnj ((\<lambda>\<phi>. rawpsubst (rawpsubst \<phi> (zip (map Var (vs \<phi>)) (map snd txs))) (zip (map fst txs) (vs \<phi>))) ` F) \<in> fmla
 3. \<lbrakk>F \<subseteq> fmla; finite F; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; distinct (map snd txs); set us \<subseteq> var; set us \<inter> \<Union> (Fvars ` F) = {}; set us \<inter> \<Union> (FvarsT ` fst ` set txs) = {}; set us \<inter> snd ` set txs = {}; length us = length txs; distinct us; \<And>\<phi>. \<phi> \<in> F \<Longrightarrow> set (vs \<phi>) \<subseteq> var \<and> set (vs \<phi>) \<inter> Fvars \<phi> = {} \<and> set (vs \<phi>) \<inter> \<Union> (FvarsT ` fst ` set txs) = {} \<and> set (vs \<phi>) \<inter> snd ` set txs = {} \<and> length (vs \<phi>) = length txs \<and> distinct (vs \<phi>)\<rbrakk> \<Longrightarrow> prv (imp (scnj ((\<lambda>\<phi>. rawpsubst \<phi> (zip (map fst txs) us)) ` (\<lambda>\<phi>. rawpsubst \<phi> (zip (map Var us) (map snd txs))) ` F)) (scnj ((\<lambda>\<phi>. rawpsubst (rawpsubst \<phi> (zip (map Var (vs \<phi>)) (map snd txs))) (zip (map fst txs) (vs \<phi>))) ` F)))
 4. \<lbrakk>F \<subseteq> fmla; finite F; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; distinct (map snd txs); set us \<subseteq> var; set us \<inter> \<Union> (Fvars ` F) = {}; set us \<inter> \<Union> (FvarsT ` fst ` set txs) = {}; set us \<inter> snd ` set txs = {}; length us = length txs; distinct us; \<And>\<phi>. \<phi> \<in> F \<Longrightarrow> set (vs \<phi>) \<subseteq> var \<and> set (vs \<phi>) \<inter> Fvars \<phi> = {} \<and> set (vs \<phi>) \<inter> \<Union> (FvarsT ` fst ` set txs) = {} \<and> set (vs \<phi>) \<inter> snd ` set txs = {} \<and> length (vs \<phi>) = length txs \<and> distinct (vs \<phi>)\<rbrakk> \<Longrightarrow> prv (imp (scnj ((\<lambda>\<phi>. rawpsubst (rawpsubst \<phi> (zip (map Var (vs \<phi>)) (map snd txs))) (zip (map fst txs) (vs \<phi>))) ` F)) (scnj ((\<lambda>\<phi>. rawpsubst \<phi> (zip (map fst txs) us)) ` (\<lambda>\<phi>. rawpsubst \<phi> (zip (map Var us) (map snd txs))) ` F)))
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>F \<subseteq> fmla; finite F; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; distinct (map snd txs); set us \<subseteq> var; set us \<inter> \<Union> (Fvars ` F) = {}; set us \<inter> \<Union> (FvarsT ` fst ` set txs) = {}; set us \<inter> snd ` set txs = {}; length us = length txs; distinct us; \<And>\<phi>. \<phi> \<in> F \<Longrightarrow> set (vs \<phi>) \<subseteq> var \<and> set (vs \<phi>) \<inter> Fvars \<phi> = {} \<and> set (vs \<phi>) \<inter> \<Union> (FvarsT ` fst ` set txs) = {} \<and> set (vs \<phi>) \<inter> snd ` set txs = {} \<and> length (vs \<phi>) = length txs \<and> distinct (vs \<phi>)\<rbrakk> \<Longrightarrow> scnj ((\<lambda>\<phi>. rawpsubst \<phi> (zip (map fst txs) us)) ` (\<lambda>\<phi>. rawpsubst \<phi> (zip (map Var us) (map snd txs))) ` F) \<in> fmla
[PROOF STEP]
by (auto intro!: rawpsubst dest!: set_zip_D)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>F \<subseteq> fmla; finite F; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; distinct (map snd txs); set us \<subseteq> var; set us \<inter> \<Union> (Fvars ` F) = {}; set us \<inter> \<Union> (FvarsT ` fst ` set txs) = {}; set us \<inter> snd ` set txs = {}; length us = length txs; distinct us; \<And>\<phi>. \<phi> \<in> F \<Longrightarrow> set (vs \<phi>) \<subseteq> var \<and> set (vs \<phi>) \<inter> Fvars \<phi> = {} \<and> set (vs \<phi>) \<inter> \<Union> (FvarsT ` fst ` set txs) = {} \<and> set (vs \<phi>) \<inter> snd ` set txs = {} \<and> length (vs \<phi>) = length txs \<and> distinct (vs \<phi>)\<rbrakk> \<Longrightarrow> scnj ((\<lambda>\<phi>. rawpsubst (rawpsubst \<phi> (zip (map Var (vs \<phi>)) (map snd txs))) (zip (map fst txs) (vs \<phi>))) ` F) \<in> fmla
 2. \<lbrakk>F \<subseteq> fmla; finite F; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; distinct (map snd txs); set us \<subseteq> var; set us \<inter> \<Union> (Fvars ` F) = {}; set us \<inter> \<Union> (FvarsT ` fst ` set txs) = {}; set us \<inter> snd ` set txs = {}; length us = length txs; distinct us; \<And>\<phi>. \<phi> \<in> F \<Longrightarrow> set (vs \<phi>) \<subseteq> var \<and> set (vs \<phi>) \<inter> Fvars \<phi> = {} \<and> set (vs \<phi>) \<inter> \<Union> (FvarsT ` fst ` set txs) = {} \<and> set (vs \<phi>) \<inter> snd ` set txs = {} \<and> length (vs \<phi>) = length txs \<and> distinct (vs \<phi>)\<rbrakk> \<Longrightarrow> prv (imp (scnj ((\<lambda>\<phi>. rawpsubst \<phi> (zip (map fst txs) us)) ` (\<lambda>\<phi>. rawpsubst \<phi> (zip (map Var us) (map snd txs))) ` F)) (scnj ((\<lambda>\<phi>. rawpsubst (rawpsubst \<phi> (zip (map Var (vs \<phi>)) (map snd txs))) (zip (map fst txs) (vs \<phi>))) ` F)))
 3. \<lbrakk>F \<subseteq> fmla; finite F; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; distinct (map snd txs); set us \<subseteq> var; set us \<inter> \<Union> (Fvars ` F) = {}; set us \<inter> \<Union> (FvarsT ` fst ` set txs) = {}; set us \<inter> snd ` set txs = {}; length us = length txs; distinct us; \<And>\<phi>. \<phi> \<in> F \<Longrightarrow> set (vs \<phi>) \<subseteq> var \<and> set (vs \<phi>) \<inter> Fvars \<phi> = {} \<and> set (vs \<phi>) \<inter> \<Union> (FvarsT ` fst ` set txs) = {} \<and> set (vs \<phi>) \<inter> snd ` set txs = {} \<and> length (vs \<phi>) = length txs \<and> distinct (vs \<phi>)\<rbrakk> \<Longrightarrow> prv (imp (scnj ((\<lambda>\<phi>. rawpsubst (rawpsubst \<phi> (zip (map Var (vs \<phi>)) (map snd txs))) (zip (map fst txs) (vs \<phi>))) ` F)) (scnj ((\<lambda>\<phi>. rawpsubst \<phi> (zip (map fst txs) us)) ` (\<lambda>\<phi>. rawpsubst \<phi> (zip (map Var us) (map snd txs))) ` F)))
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>F \<subseteq> fmla; finite F; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; distinct (map snd txs); set us \<subseteq> var; set us \<inter> \<Union> (Fvars ` F) = {}; set us \<inter> \<Union> (FvarsT ` fst ` set txs) = {}; set us \<inter> snd ` set txs = {}; length us = length txs; distinct us; \<And>\<phi>. \<phi> \<in> F \<Longrightarrow> set (vs \<phi>) \<subseteq> var \<and> set (vs \<phi>) \<inter> Fvars \<phi> = {} \<and> set (vs \<phi>) \<inter> \<Union> (FvarsT ` fst ` set txs) = {} \<and> set (vs \<phi>) \<inter> snd ` set txs = {} \<and> length (vs \<phi>) = length txs \<and> distinct (vs \<phi>)\<rbrakk> \<Longrightarrow> scnj ((\<lambda>\<phi>. rawpsubst (rawpsubst \<phi> (zip (map Var (vs \<phi>)) (map snd txs))) (zip (map fst txs) (vs \<phi>))) ` F) \<in> fmla
[PROOF STEP]
by (auto intro!: rawpsubst dest!: set_zip_D)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>F \<subseteq> fmla; finite F; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; distinct (map snd txs); set us \<subseteq> var; set us \<inter> \<Union> (Fvars ` F) = {}; set us \<inter> \<Union> (FvarsT ` fst ` set txs) = {}; set us \<inter> snd ` set txs = {}; length us = length txs; distinct us; \<And>\<phi>. \<phi> \<in> F \<Longrightarrow> set (vs \<phi>) \<subseteq> var \<and> set (vs \<phi>) \<inter> Fvars \<phi> = {} \<and> set (vs \<phi>) \<inter> \<Union> (FvarsT ` fst ` set txs) = {} \<and> set (vs \<phi>) \<inter> snd ` set txs = {} \<and> length (vs \<phi>) = length txs \<and> distinct (vs \<phi>)\<rbrakk> \<Longrightarrow> prv (imp (scnj ((\<lambda>\<phi>. rawpsubst \<phi> (zip (map fst txs) us)) ` (\<lambda>\<phi>. rawpsubst \<phi> (zip (map Var us) (map snd txs))) ` F)) (scnj ((\<lambda>\<phi>. rawpsubst (rawpsubst \<phi> (zip (map Var (vs \<phi>)) (map snd txs))) (zip (map fst txs) (vs \<phi>))) ` F)))
 2. \<lbrakk>F \<subseteq> fmla; finite F; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; distinct (map snd txs); set us \<subseteq> var; set us \<inter> \<Union> (Fvars ` F) = {}; set us \<inter> \<Union> (FvarsT ` fst ` set txs) = {}; set us \<inter> snd ` set txs = {}; length us = length txs; distinct us; \<And>\<phi>. \<phi> \<in> F \<Longrightarrow> set (vs \<phi>) \<subseteq> var \<and> set (vs \<phi>) \<inter> Fvars \<phi> = {} \<and> set (vs \<phi>) \<inter> \<Union> (FvarsT ` fst ` set txs) = {} \<and> set (vs \<phi>) \<inter> snd ` set txs = {} \<and> length (vs \<phi>) = length txs \<and> distinct (vs \<phi>)\<rbrakk> \<Longrightarrow> prv (imp (scnj ((\<lambda>\<phi>. rawpsubst (rawpsubst \<phi> (zip (map Var (vs \<phi>)) (map snd txs))) (zip (map fst txs) (vs \<phi>))) ` F)) (scnj ((\<lambda>\<phi>. rawpsubst \<phi> (zip (map fst txs) us)) ` (\<lambda>\<phi>. rawpsubst \<phi> (zip (map Var us) (map snd txs))) ` F)))
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>F \<subseteq> fmla; finite F; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; distinct (map snd txs); set us \<subseteq> var; set us \<inter> \<Union> (Fvars ` F) = {}; set us \<inter> \<Union> (FvarsT ` fst ` set txs) = {}; set us \<inter> snd ` set txs = {}; length us = length txs; distinct us; \<And>\<phi>. \<phi> \<in> F \<Longrightarrow> set (vs \<phi>) \<subseteq> var \<and> set (vs \<phi>) \<inter> Fvars \<phi> = {} \<and> set (vs \<phi>) \<inter> \<Union> (FvarsT ` fst ` set txs) = {} \<and> set (vs \<phi>) \<inter> snd ` set txs = {} \<and> length (vs \<phi>) = length txs \<and> distinct (vs \<phi>)\<rbrakk> \<Longrightarrow> prv (imp (scnj ((\<lambda>\<phi>. rawpsubst \<phi> (zip (map fst txs) us)) ` (\<lambda>\<phi>. rawpsubst \<phi> (zip (map Var us) (map snd txs))) ` F)) (scnj ((\<lambda>\<phi>. rawpsubst (rawpsubst \<phi> (zip (map Var (vs \<phi>)) (map snd txs))) (zip (map fst txs) (vs \<phi>))) ` F)))
[PROOF STEP]
apply(rule prv_scnj_mono_imp)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<lbrakk>F \<subseteq> fmla; finite F; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; distinct (map snd txs); set us \<subseteq> var; set us \<inter> \<Union> (Fvars ` F) = {}; set us \<inter> \<Union> (FvarsT ` fst ` set txs) = {}; set us \<inter> snd ` set txs = {}; length us = length txs; distinct us; \<And>\<phi>. \<phi> \<in> F \<Longrightarrow> set (vs \<phi>) \<subseteq> var \<and> set (vs \<phi>) \<inter> Fvars \<phi> = {} \<and> set (vs \<phi>) \<inter> \<Union> (FvarsT ` fst ` set txs) = {} \<and> set (vs \<phi>) \<inter> snd ` set txs = {} \<and> length (vs \<phi>) = length txs \<and> distinct (vs \<phi>)\<rbrakk> \<Longrightarrow> (\<lambda>\<phi>. rawpsubst \<phi> (zip (map fst txs) us)) ` (\<lambda>\<phi>. rawpsubst \<phi> (zip (map Var us) (map snd txs))) ` F \<subseteq> fmla
 2. \<lbrakk>F \<subseteq> fmla; finite F; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; distinct (map snd txs); set us \<subseteq> var; set us \<inter> \<Union> (Fvars ` F) = {}; set us \<inter> \<Union> (FvarsT ` fst ` set txs) = {}; set us \<inter> snd ` set txs = {}; length us = length txs; distinct us; \<And>\<phi>. \<phi> \<in> F \<Longrightarrow> set (vs \<phi>) \<subseteq> var \<and> set (vs \<phi>) \<inter> Fvars \<phi> = {} \<and> set (vs \<phi>) \<inter> \<Union> (FvarsT ` fst ` set txs) = {} \<and> set (vs \<phi>) \<inter> snd ` set txs = {} \<and> length (vs \<phi>) = length txs \<and> distinct (vs \<phi>)\<rbrakk> \<Longrightarrow> (\<lambda>\<phi>. rawpsubst (rawpsubst \<phi> (zip (map Var (vs \<phi>)) (map snd txs))) (zip (map fst txs) (vs \<phi>))) ` F \<subseteq> fmla
 3. \<lbrakk>F \<subseteq> fmla; finite F; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; distinct (map snd txs); set us \<subseteq> var; set us \<inter> \<Union> (Fvars ` F) = {}; set us \<inter> \<Union> (FvarsT ` fst ` set txs) = {}; set us \<inter> snd ` set txs = {}; length us = length txs; distinct us; \<And>\<phi>. \<phi> \<in> F \<Longrightarrow> set (vs \<phi>) \<subseteq> var \<and> set (vs \<phi>) \<inter> Fvars \<phi> = {} \<and> set (vs \<phi>) \<inter> \<Union> (FvarsT ` fst ` set txs) = {} \<and> set (vs \<phi>) \<inter> snd ` set txs = {} \<and> length (vs \<phi>) = length txs \<and> distinct (vs \<phi>)\<rbrakk> \<Longrightarrow> finite ((\<lambda>\<phi>. rawpsubst \<phi> (zip (map fst txs) us)) ` (\<lambda>\<phi>. rawpsubst \<phi> (zip (map Var us) (map snd txs))) ` F)
 4. \<lbrakk>F \<subseteq> fmla; finite F; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; distinct (map snd txs); set us \<subseteq> var; set us \<inter> \<Union> (Fvars ` F) = {}; set us \<inter> \<Union> (FvarsT ` fst ` set txs) = {}; set us \<inter> snd ` set txs = {}; length us = length txs; distinct us; \<And>\<phi>. \<phi> \<in> F \<Longrightarrow> set (vs \<phi>) \<subseteq> var \<and> set (vs \<phi>) \<inter> Fvars \<phi> = {} \<and> set (vs \<phi>) \<inter> \<Union> (FvarsT ` fst ` set txs) = {} \<and> set (vs \<phi>) \<inter> snd ` set txs = {} \<and> length (vs \<phi>) = length txs \<and> distinct (vs \<phi>)\<rbrakk> \<Longrightarrow> finite ((\<lambda>\<phi>. rawpsubst (rawpsubst \<phi> (zip (map Var (vs \<phi>)) (map snd txs))) (zip (map fst txs) (vs \<phi>))) ` F)
 5. \<lbrakk>F \<subseteq> fmla; finite F; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; distinct (map snd txs); set us \<subseteq> var; set us \<inter> \<Union> (Fvars ` F) = {}; set us \<inter> \<Union> (FvarsT ` fst ` set txs) = {}; set us \<inter> snd ` set txs = {}; length us = length txs; distinct us; \<And>\<phi>. \<phi> \<in> F \<Longrightarrow> set (vs \<phi>) \<subseteq> var \<and> set (vs \<phi>) \<inter> Fvars \<phi> = {} \<and> set (vs \<phi>) \<inter> \<Union> (FvarsT ` fst ` set txs) = {} \<and> set (vs \<phi>) \<inter> snd ` set txs = {} \<and> length (vs \<phi>) = length txs \<and> distinct (vs \<phi>)\<rbrakk> \<Longrightarrow> \<forall>\<phi>2\<in>(\<lambda>\<phi>. rawpsubst (rawpsubst \<phi> (zip (map Var (vs \<phi>)) (map snd txs))) (zip (map fst txs) (vs \<phi>))) ` F. \<exists>\<phi>1\<in>(\<lambda>\<phi>. rawpsubst \<phi> (zip (map fst txs) us)) ` (\<lambda>\<phi>. rawpsubst \<phi> (zip (map Var us) (map snd txs))) ` F. prv (imp \<phi>1 \<phi>2)
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>F \<subseteq> fmla; finite F; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; distinct (map snd txs); set us \<subseteq> var; set us \<inter> \<Union> (Fvars ` F) = {}; set us \<inter> \<Union> (FvarsT ` fst ` set txs) = {}; set us \<inter> snd ` set txs = {}; length us = length txs; distinct us; \<And>\<phi>. \<phi> \<in> F \<Longrightarrow> set (vs \<phi>) \<subseteq> var \<and> set (vs \<phi>) \<inter> Fvars \<phi> = {} \<and> set (vs \<phi>) \<inter> \<Union> (FvarsT ` fst ` set txs) = {} \<and> set (vs \<phi>) \<inter> snd ` set txs = {} \<and> length (vs \<phi>) = length txs \<and> distinct (vs \<phi>)\<rbrakk> \<Longrightarrow> (\<lambda>\<phi>. rawpsubst \<phi> (zip (map fst txs) us)) ` (\<lambda>\<phi>. rawpsubst \<phi> (zip (map Var us) (map snd txs))) ` F \<subseteq> fmla
[PROOF STEP]
by (auto intro!: rawpsubst dest!: set_zip_D)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>F \<subseteq> fmla; finite F; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; distinct (map snd txs); set us \<subseteq> var; set us \<inter> \<Union> (Fvars ` F) = {}; set us \<inter> \<Union> (FvarsT ` fst ` set txs) = {}; set us \<inter> snd ` set txs = {}; length us = length txs; distinct us; \<And>\<phi>. \<phi> \<in> F \<Longrightarrow> set (vs \<phi>) \<subseteq> var \<and> set (vs \<phi>) \<inter> Fvars \<phi> = {} \<and> set (vs \<phi>) \<inter> \<Union> (FvarsT ` fst ` set txs) = {} \<and> set (vs \<phi>) \<inter> snd ` set txs = {} \<and> length (vs \<phi>) = length txs \<and> distinct (vs \<phi>)\<rbrakk> \<Longrightarrow> (\<lambda>\<phi>. rawpsubst (rawpsubst \<phi> (zip (map Var (vs \<phi>)) (map snd txs))) (zip (map fst txs) (vs \<phi>))) ` F \<subseteq> fmla
 2. \<lbrakk>F \<subseteq> fmla; finite F; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; distinct (map snd txs); set us \<subseteq> var; set us \<inter> \<Union> (Fvars ` F) = {}; set us \<inter> \<Union> (FvarsT ` fst ` set txs) = {}; set us \<inter> snd ` set txs = {}; length us = length txs; distinct us; \<And>\<phi>. \<phi> \<in> F \<Longrightarrow> set (vs \<phi>) \<subseteq> var \<and> set (vs \<phi>) \<inter> Fvars \<phi> = {} \<and> set (vs \<phi>) \<inter> \<Union> (FvarsT ` fst ` set txs) = {} \<and> set (vs \<phi>) \<inter> snd ` set txs = {} \<and> length (vs \<phi>) = length txs \<and> distinct (vs \<phi>)\<rbrakk> \<Longrightarrow> finite ((\<lambda>\<phi>. rawpsubst \<phi> (zip (map fst txs) us)) ` (\<lambda>\<phi>. rawpsubst \<phi> (zip (map Var us) (map snd txs))) ` F)
 3. \<lbrakk>F \<subseteq> fmla; finite F; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; distinct (map snd txs); set us \<subseteq> var; set us \<inter> \<Union> (Fvars ` F) = {}; set us \<inter> \<Union> (FvarsT ` fst ` set txs) = {}; set us \<inter> snd ` set txs = {}; length us = length txs; distinct us; \<And>\<phi>. \<phi> \<in> F \<Longrightarrow> set (vs \<phi>) \<subseteq> var \<and> set (vs \<phi>) \<inter> Fvars \<phi> = {} \<and> set (vs \<phi>) \<inter> \<Union> (FvarsT ` fst ` set txs) = {} \<and> set (vs \<phi>) \<inter> snd ` set txs = {} \<and> length (vs \<phi>) = length txs \<and> distinct (vs \<phi>)\<rbrakk> \<Longrightarrow> finite ((\<lambda>\<phi>. rawpsubst (rawpsubst \<phi> (zip (map Var (vs \<phi>)) (map snd txs))) (zip (map fst txs) (vs \<phi>))) ` F)
 4. \<lbrakk>F \<subseteq> fmla; finite F; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; distinct (map snd txs); set us \<subseteq> var; set us \<inter> \<Union> (Fvars ` F) = {}; set us \<inter> \<Union> (FvarsT ` fst ` set txs) = {}; set us \<inter> snd ` set txs = {}; length us = length txs; distinct us; \<And>\<phi>. \<phi> \<in> F \<Longrightarrow> set (vs \<phi>) \<subseteq> var \<and> set (vs \<phi>) \<inter> Fvars \<phi> = {} \<and> set (vs \<phi>) \<inter> \<Union> (FvarsT ` fst ` set txs) = {} \<and> set (vs \<phi>) \<inter> snd ` set txs = {} \<and> length (vs \<phi>) = length txs \<and> distinct (vs \<phi>)\<rbrakk> \<Longrightarrow> \<forall>\<phi>2\<in>(\<lambda>\<phi>. rawpsubst (rawpsubst \<phi> (zip (map Var (vs \<phi>)) (map snd txs))) (zip (map fst txs) (vs \<phi>))) ` F. \<exists>\<phi>1\<in>(\<lambda>\<phi>. rawpsubst \<phi> (zip (map fst txs) us)) ` (\<lambda>\<phi>. rawpsubst \<phi> (zip (map Var us) (map snd txs))) ` F. prv (imp \<phi>1 \<phi>2)
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>F \<subseteq> fmla; finite F; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; distinct (map snd txs); set us \<subseteq> var; set us \<inter> \<Union> (Fvars ` F) = {}; set us \<inter> \<Union> (FvarsT ` fst ` set txs) = {}; set us \<inter> snd ` set txs = {}; length us = length txs; distinct us; \<And>\<phi>. \<phi> \<in> F \<Longrightarrow> set (vs \<phi>) \<subseteq> var \<and> set (vs \<phi>) \<inter> Fvars \<phi> = {} \<and> set (vs \<phi>) \<inter> \<Union> (FvarsT ` fst ` set txs) = {} \<and> set (vs \<phi>) \<inter> snd ` set txs = {} \<and> length (vs \<phi>) = length txs \<and> distinct (vs \<phi>)\<rbrakk> \<Longrightarrow> (\<lambda>\<phi>. rawpsubst (rawpsubst \<phi> (zip (map Var (vs \<phi>)) (map snd txs))) (zip (map fst txs) (vs \<phi>))) ` F \<subseteq> fmla
[PROOF STEP]
by (auto intro!: rawpsubst dest!: set_zip_D)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>F \<subseteq> fmla; finite F; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; distinct (map snd txs); set us \<subseteq> var; set us \<inter> \<Union> (Fvars ` F) = {}; set us \<inter> \<Union> (FvarsT ` fst ` set txs) = {}; set us \<inter> snd ` set txs = {}; length us = length txs; distinct us; \<And>\<phi>. \<phi> \<in> F \<Longrightarrow> set (vs \<phi>) \<subseteq> var \<and> set (vs \<phi>) \<inter> Fvars \<phi> = {} \<and> set (vs \<phi>) \<inter> \<Union> (FvarsT ` fst ` set txs) = {} \<and> set (vs \<phi>) \<inter> snd ` set txs = {} \<and> length (vs \<phi>) = length txs \<and> distinct (vs \<phi>)\<rbrakk> \<Longrightarrow> finite ((\<lambda>\<phi>. rawpsubst \<phi> (zip (map fst txs) us)) ` (\<lambda>\<phi>. rawpsubst \<phi> (zip (map Var us) (map snd txs))) ` F)
 2. \<lbrakk>F \<subseteq> fmla; finite F; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; distinct (map snd txs); set us \<subseteq> var; set us \<inter> \<Union> (Fvars ` F) = {}; set us \<inter> \<Union> (FvarsT ` fst ` set txs) = {}; set us \<inter> snd ` set txs = {}; length us = length txs; distinct us; \<And>\<phi>. \<phi> \<in> F \<Longrightarrow> set (vs \<phi>) \<subseteq> var \<and> set (vs \<phi>) \<inter> Fvars \<phi> = {} \<and> set (vs \<phi>) \<inter> \<Union> (FvarsT ` fst ` set txs) = {} \<and> set (vs \<phi>) \<inter> snd ` set txs = {} \<and> length (vs \<phi>) = length txs \<and> distinct (vs \<phi>)\<rbrakk> \<Longrightarrow> finite ((\<lambda>\<phi>. rawpsubst (rawpsubst \<phi> (zip (map Var (vs \<phi>)) (map snd txs))) (zip (map fst txs) (vs \<phi>))) ` F)
 3. \<lbrakk>F \<subseteq> fmla; finite F; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; distinct (map snd txs); set us \<subseteq> var; set us \<inter> \<Union> (Fvars ` F) = {}; set us \<inter> \<Union> (FvarsT ` fst ` set txs) = {}; set us \<inter> snd ` set txs = {}; length us = length txs; distinct us; \<And>\<phi>. \<phi> \<in> F \<Longrightarrow> set (vs \<phi>) \<subseteq> var \<and> set (vs \<phi>) \<inter> Fvars \<phi> = {} \<and> set (vs \<phi>) \<inter> \<Union> (FvarsT ` fst ` set txs) = {} \<and> set (vs \<phi>) \<inter> snd ` set txs = {} \<and> length (vs \<phi>) = length txs \<and> distinct (vs \<phi>)\<rbrakk> \<Longrightarrow> \<forall>\<phi>2\<in>(\<lambda>\<phi>. rawpsubst (rawpsubst \<phi> (zip (map Var (vs \<phi>)) (map snd txs))) (zip (map fst txs) (vs \<phi>))) ` F. \<exists>\<phi>1\<in>(\<lambda>\<phi>. rawpsubst \<phi> (zip (map fst txs) us)) ` (\<lambda>\<phi>. rawpsubst \<phi> (zip (map Var us) (map snd txs))) ` F. prv (imp \<phi>1 \<phi>2)
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>F \<subseteq> fmla; finite F; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; distinct (map snd txs); set us \<subseteq> var; set us \<inter> \<Union> (Fvars ` F) = {}; set us \<inter> \<Union> (FvarsT ` fst ` set txs) = {}; set us \<inter> snd ` set txs = {}; length us = length txs; distinct us; \<And>\<phi>. \<phi> \<in> F \<Longrightarrow> set (vs \<phi>) \<subseteq> var \<and> set (vs \<phi>) \<inter> Fvars \<phi> = {} \<and> set (vs \<phi>) \<inter> \<Union> (FvarsT ` fst ` set txs) = {} \<and> set (vs \<phi>) \<inter> snd ` set txs = {} \<and> length (vs \<phi>) = length txs \<and> distinct (vs \<phi>)\<rbrakk> \<Longrightarrow> finite ((\<lambda>\<phi>. rawpsubst \<phi> (zip (map fst txs) us)) ` (\<lambda>\<phi>. rawpsubst \<phi> (zip (map Var us) (map snd txs))) ` F)
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>F \<subseteq> fmla; finite F; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; distinct (map snd txs); set us \<subseteq> var; set us \<inter> \<Union> (Fvars ` F) = {}; set us \<inter> \<Union> (FvarsT ` fst ` set txs) = {}; set us \<inter> snd ` set txs = {}; length us = length txs; distinct us; \<And>\<phi>. \<phi> \<in> F \<Longrightarrow> set (vs \<phi>) \<subseteq> var \<and> set (vs \<phi>) \<inter> Fvars \<phi> = {} \<and> set (vs \<phi>) \<inter> \<Union> (FvarsT ` fst ` set txs) = {} \<and> set (vs \<phi>) \<inter> snd ` set txs = {} \<and> length (vs \<phi>) = length txs \<and> distinct (vs \<phi>)\<rbrakk> \<Longrightarrow> finite ((\<lambda>\<phi>. rawpsubst (rawpsubst \<phi> (zip (map Var (vs \<phi>)) (map snd txs))) (zip (map fst txs) (vs \<phi>))) ` F)
 2. \<lbrakk>F \<subseteq> fmla; finite F; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; distinct (map snd txs); set us \<subseteq> var; set us \<inter> \<Union> (Fvars ` F) = {}; set us \<inter> \<Union> (FvarsT ` fst ` set txs) = {}; set us \<inter> snd ` set txs = {}; length us = length txs; distinct us; \<And>\<phi>. \<phi> \<in> F \<Longrightarrow> set (vs \<phi>) \<subseteq> var \<and> set (vs \<phi>) \<inter> Fvars \<phi> = {} \<and> set (vs \<phi>) \<inter> \<Union> (FvarsT ` fst ` set txs) = {} \<and> set (vs \<phi>) \<inter> snd ` set txs = {} \<and> length (vs \<phi>) = length txs \<and> distinct (vs \<phi>)\<rbrakk> \<Longrightarrow> \<forall>\<phi>2\<in>(\<lambda>\<phi>. rawpsubst (rawpsubst \<phi> (zip (map Var (vs \<phi>)) (map snd txs))) (zip (map fst txs) (vs \<phi>))) ` F. \<exists>\<phi>1\<in>(\<lambda>\<phi>. rawpsubst \<phi> (zip (map fst txs) us)) ` (\<lambda>\<phi>. rawpsubst \<phi> (zip (map Var us) (map snd txs))) ` F. prv (imp \<phi>1 \<phi>2)
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>F \<subseteq> fmla; finite F; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; distinct (map snd txs); set us \<subseteq> var; set us \<inter> \<Union> (Fvars ` F) = {}; set us \<inter> \<Union> (FvarsT ` fst ` set txs) = {}; set us \<inter> snd ` set txs = {}; length us = length txs; distinct us; \<And>\<phi>. \<phi> \<in> F \<Longrightarrow> set (vs \<phi>) \<subseteq> var \<and> set (vs \<phi>) \<inter> Fvars \<phi> = {} \<and> set (vs \<phi>) \<inter> \<Union> (FvarsT ` fst ` set txs) = {} \<and> set (vs \<phi>) \<inter> snd ` set txs = {} \<and> length (vs \<phi>) = length txs \<and> distinct (vs \<phi>)\<rbrakk> \<Longrightarrow> finite ((\<lambda>\<phi>. rawpsubst (rawpsubst \<phi> (zip (map Var (vs \<phi>)) (map snd txs))) (zip (map fst txs) (vs \<phi>))) ` F)
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>F \<subseteq> fmla; finite F; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; distinct (map snd txs); set us \<subseteq> var; set us \<inter> \<Union> (Fvars ` F) = {}; set us \<inter> \<Union> (FvarsT ` fst ` set txs) = {}; set us \<inter> snd ` set txs = {}; length us = length txs; distinct us; \<And>\<phi>. \<phi> \<in> F \<Longrightarrow> set (vs \<phi>) \<subseteq> var \<and> set (vs \<phi>) \<inter> Fvars \<phi> = {} \<and> set (vs \<phi>) \<inter> \<Union> (FvarsT ` fst ` set txs) = {} \<and> set (vs \<phi>) \<inter> snd ` set txs = {} \<and> length (vs \<phi>) = length txs \<and> distinct (vs \<phi>)\<rbrakk> \<Longrightarrow> \<forall>\<phi>2\<in>(\<lambda>\<phi>. rawpsubst (rawpsubst \<phi> (zip (map Var (vs \<phi>)) (map snd txs))) (zip (map fst txs) (vs \<phi>))) ` F. \<exists>\<phi>1\<in>(\<lambda>\<phi>. rawpsubst \<phi> (zip (map fst txs) us)) ` (\<lambda>\<phi>. rawpsubst \<phi> (zip (map Var us) (map snd txs))) ` F. prv (imp \<phi>1 \<phi>2)
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>F \<subseteq> fmla; finite F; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; distinct (map snd txs); set us \<subseteq> var; set us \<inter> \<Union> (Fvars ` F) = {}; set us \<inter> \<Union> (FvarsT ` fst ` set txs) = {}; set us \<inter> snd ` set txs = {}; length us = length txs; distinct us; \<And>\<phi>. \<phi> \<in> F \<Longrightarrow> set (vs \<phi>) \<subseteq> var \<and> set (vs \<phi>) \<inter> Fvars \<phi> = {} \<and> set (vs \<phi>) \<inter> \<Union> (FvarsT ` fst ` set txs) = {} \<and> set (vs \<phi>) \<inter> snd ` set txs = {} \<and> length (vs \<phi>) = length txs \<and> distinct (vs \<phi>)\<rbrakk> \<Longrightarrow> \<forall>\<phi>2\<in>(\<lambda>\<phi>. rawpsubst (rawpsubst \<phi> (zip (map Var (vs \<phi>)) (map snd txs))) (zip (map fst txs) (vs \<phi>))) ` F. \<exists>\<phi>1\<in>(\<lambda>\<phi>. rawpsubst \<phi> (zip (map fst txs) us)) ` (\<lambda>\<phi>. rawpsubst \<phi> (zip (map Var us) (map snd txs))) ` F. prv (imp \<phi>1 \<phi>2)
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>\<phi>2. \<lbrakk>F \<subseteq> fmla; finite F; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; distinct (map snd txs); set us \<subseteq> var; set us \<inter> \<Union> (Fvars ` F) = {}; set us \<inter> (\<Union>a\<in>set txs. FvarsT (fst a)) = {}; set us \<inter> snd ` set txs = {}; length us = length txs; distinct us; \<And>\<phi>. \<phi> \<in> F \<Longrightarrow> set (vs \<phi>) \<subseteq> var \<and> set (vs \<phi>) \<inter> Fvars \<phi> = {} \<and> set (vs \<phi>) \<inter> (\<Union>a\<in>set txs. FvarsT (fst a)) = {} \<and> set (vs \<phi>) \<inter> snd ` set txs = {} \<and> length (vs \<phi>) = length txs \<and> distinct (vs \<phi>); \<phi>2 \<in> F\<rbrakk> \<Longrightarrow> \<exists>\<phi>1\<in>F. prv (imp (rawpsubst (rawpsubst \<phi>1 (zip (map Var us) (map snd txs))) (zip (map fst txs) us)) (rawpsubst (rawpsubst \<phi>2 (zip (map Var (vs \<phi>2)) (map snd txs))) (zip (map fst txs) (vs \<phi>2))))
[PROOF STEP]
subgoal for \<phi>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>F \<subseteq> fmla; finite F; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; distinct (map snd txs); set us \<subseteq> var; set us \<inter> \<Union> (Fvars ` F) = {}; set us \<inter> (\<Union>a\<in>set txs. FvarsT (fst a)) = {}; set us \<inter> snd ` set txs = {}; length us = length txs; distinct us; \<And>\<phi>. \<phi> \<in> F \<Longrightarrow> set (vs \<phi>) \<subseteq> var \<and> set (vs \<phi>) \<inter> Fvars \<phi> = {} \<and> set (vs \<phi>) \<inter> (\<Union>a\<in>set txs. FvarsT (fst a)) = {} \<and> set (vs \<phi>) \<inter> snd ` set txs = {} \<and> length (vs \<phi>) = length txs \<and> distinct (vs \<phi>); \<phi> \<in> F\<rbrakk> \<Longrightarrow> \<exists>\<phi>1\<in>F. prv (imp (rawpsubst (rawpsubst \<phi>1 (zip (map Var us) (map snd txs))) (zip (map fst txs) us)) (rawpsubst (rawpsubst \<phi> (zip (map Var (vs \<phi>)) (map snd txs))) (zip (map fst txs) (vs \<phi>))))
[PROOF STEP]
apply(rule bexI[of _ \<phi>])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>F \<subseteq> fmla; finite F; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; distinct (map snd txs); set us \<subseteq> var; set us \<inter> \<Union> (Fvars ` F) = {}; set us \<inter> (\<Union>a\<in>set txs. FvarsT (fst a)) = {}; set us \<inter> snd ` set txs = {}; length us = length txs; distinct us; \<And>\<phi>. \<phi> \<in> F \<Longrightarrow> set (vs \<phi>) \<subseteq> var \<and> set (vs \<phi>) \<inter> Fvars \<phi> = {} \<and> set (vs \<phi>) \<inter> (\<Union>a\<in>set txs. FvarsT (fst a)) = {} \<and> set (vs \<phi>) \<inter> snd ` set txs = {} \<and> length (vs \<phi>) = length txs \<and> distinct (vs \<phi>); \<phi> \<in> F\<rbrakk> \<Longrightarrow> prv (imp (rawpsubst (rawpsubst \<phi> (zip (map Var us) (map snd txs))) (zip (map fst txs) us)) (rawpsubst (rawpsubst \<phi> (zip (map Var (vs \<phi>)) (map snd txs))) (zip (map fst txs) (vs \<phi>))))
 2. \<lbrakk>F \<subseteq> fmla; finite F; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; distinct (map snd txs); set us \<subseteq> var; set us \<inter> \<Union> (Fvars ` F) = {}; set us \<inter> (\<Union>a\<in>set txs. FvarsT (fst a)) = {}; set us \<inter> snd ` set txs = {}; length us = length txs; distinct us; \<And>\<phi>. \<phi> \<in> F \<Longrightarrow> set (vs \<phi>) \<subseteq> var \<and> set (vs \<phi>) \<inter> Fvars \<phi> = {} \<and> set (vs \<phi>) \<inter> (\<Union>a\<in>set txs. FvarsT (fst a)) = {} \<and> set (vs \<phi>) \<inter> snd ` set txs = {} \<and> length (vs \<phi>) = length txs \<and> distinct (vs \<phi>); \<phi> \<in> F\<rbrakk> \<Longrightarrow> \<phi> \<in> F
[PROOF STEP]
apply(rule prv_imp_refl2)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>F \<subseteq> fmla; finite F; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; distinct (map snd txs); set us \<subseteq> var; set us \<inter> \<Union> (Fvars ` F) = {}; set us \<inter> (\<Union>a\<in>set txs. FvarsT (fst a)) = {}; set us \<inter> snd ` set txs = {}; length us = length txs; distinct us; \<And>\<phi>. \<phi> \<in> F \<Longrightarrow> set (vs \<phi>) \<subseteq> var \<and> set (vs \<phi>) \<inter> Fvars \<phi> = {} \<and> set (vs \<phi>) \<inter> (\<Union>a\<in>set txs. FvarsT (fst a)) = {} \<and> set (vs \<phi>) \<inter> snd ` set txs = {} \<and> length (vs \<phi>) = length txs \<and> distinct (vs \<phi>); \<phi> \<in> F\<rbrakk> \<Longrightarrow> rawpsubst (rawpsubst \<phi> (zip (map Var us) (map snd txs))) (zip (map fst txs) us) \<in> fmla
 2. \<lbrakk>F \<subseteq> fmla; finite F; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; distinct (map snd txs); set us \<subseteq> var; set us \<inter> \<Union> (Fvars ` F) = {}; set us \<inter> (\<Union>a\<in>set txs. FvarsT (fst a)) = {}; set us \<inter> snd ` set txs = {}; length us = length txs; distinct us; \<And>\<phi>. \<phi> \<in> F \<Longrightarrow> set (vs \<phi>) \<subseteq> var \<and> set (vs \<phi>) \<inter> Fvars \<phi> = {} \<and> set (vs \<phi>) \<inter> (\<Union>a\<in>set txs. FvarsT (fst a)) = {} \<and> set (vs \<phi>) \<inter> snd ` set txs = {} \<and> length (vs \<phi>) = length txs \<and> distinct (vs \<phi>); \<phi> \<in> F\<rbrakk> \<Longrightarrow> rawpsubst (rawpsubst \<phi> (zip (map Var (vs \<phi>)) (map snd txs))) (zip (map fst txs) (vs \<phi>)) \<in> fmla
 3. \<lbrakk>F \<subseteq> fmla; finite F; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; distinct (map snd txs); set us \<subseteq> var; set us \<inter> \<Union> (Fvars ` F) = {}; set us \<inter> (\<Union>a\<in>set txs. FvarsT (fst a)) = {}; set us \<inter> snd ` set txs = {}; length us = length txs; distinct us; \<And>\<phi>. \<phi> \<in> F \<Longrightarrow> set (vs \<phi>) \<subseteq> var \<and> set (vs \<phi>) \<inter> Fvars \<phi> = {} \<and> set (vs \<phi>) \<inter> (\<Union>a\<in>set txs. FvarsT (fst a)) = {} \<and> set (vs \<phi>) \<inter> snd ` set txs = {} \<and> length (vs \<phi>) = length txs \<and> distinct (vs \<phi>); \<phi> \<in> F\<rbrakk> \<Longrightarrow> rawpsubst (rawpsubst \<phi> (zip (map Var us) (map snd txs))) (zip (map fst txs) us) = rawpsubst (rawpsubst \<phi> (zip (map Var (vs \<phi>)) (map snd txs))) (zip (map fst txs) (vs \<phi>))
 4. \<lbrakk>F \<subseteq> fmla; finite F; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; distinct (map snd txs); set us \<subseteq> var; set us \<inter> \<Union> (Fvars ` F) = {}; set us \<inter> (\<Union>a\<in>set txs. FvarsT (fst a)) = {}; set us \<inter> snd ` set txs = {}; length us = length txs; distinct us; \<And>\<phi>. \<phi> \<in> F \<Longrightarrow> set (vs \<phi>) \<subseteq> var \<and> set (vs \<phi>) \<inter> Fvars \<phi> = {} \<and> set (vs \<phi>) \<inter> (\<Union>a\<in>set txs. FvarsT (fst a)) = {} \<and> set (vs \<phi>) \<inter> snd ` set txs = {} \<and> length (vs \<phi>) = length txs \<and> distinct (vs \<phi>); \<phi> \<in> F\<rbrakk> \<Longrightarrow> \<phi> \<in> F
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>F \<subseteq> fmla; finite F; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; distinct (map snd txs); set us \<subseteq> var; set us \<inter> \<Union> (Fvars ` F) = {}; set us \<inter> (\<Union>a\<in>set txs. FvarsT (fst a)) = {}; set us \<inter> snd ` set txs = {}; length us = length txs; distinct us; \<And>\<phi>. \<phi> \<in> F \<Longrightarrow> set (vs \<phi>) \<subseteq> var \<and> set (vs \<phi>) \<inter> Fvars \<phi> = {} \<and> set (vs \<phi>) \<inter> (\<Union>a\<in>set txs. FvarsT (fst a)) = {} \<and> set (vs \<phi>) \<inter> snd ` set txs = {} \<and> length (vs \<phi>) = length txs \<and> distinct (vs \<phi>); \<phi> \<in> F\<rbrakk> \<Longrightarrow> rawpsubst (rawpsubst \<phi> (zip (map Var us) (map snd txs))) (zip (map fst txs) us) \<in> fmla
[PROOF STEP]
by (auto intro!: rawpsubst dest!: set_zip_D)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>F \<subseteq> fmla; finite F; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; distinct (map snd txs); set us \<subseteq> var; set us \<inter> \<Union> (Fvars ` F) = {}; set us \<inter> (\<Union>a\<in>set txs. FvarsT (fst a)) = {}; set us \<inter> snd ` set txs = {}; length us = length txs; distinct us; \<And>\<phi>. \<phi> \<in> F \<Longrightarrow> set (vs \<phi>) \<subseteq> var \<and> set (vs \<phi>) \<inter> Fvars \<phi> = {} \<and> set (vs \<phi>) \<inter> (\<Union>a\<in>set txs. FvarsT (fst a)) = {} \<and> set (vs \<phi>) \<inter> snd ` set txs = {} \<and> length (vs \<phi>) = length txs \<and> distinct (vs \<phi>); \<phi> \<in> F\<rbrakk> \<Longrightarrow> rawpsubst (rawpsubst \<phi> (zip (map Var (vs \<phi>)) (map snd txs))) (zip (map fst txs) (vs \<phi>)) \<in> fmla
 2. \<lbrakk>F \<subseteq> fmla; finite F; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; distinct (map snd txs); set us \<subseteq> var; set us \<inter> \<Union> (Fvars ` F) = {}; set us \<inter> (\<Union>a\<in>set txs. FvarsT (fst a)) = {}; set us \<inter> snd ` set txs = {}; length us = length txs; distinct us; \<And>\<phi>. \<phi> \<in> F \<Longrightarrow> set (vs \<phi>) \<subseteq> var \<and> set (vs \<phi>) \<inter> Fvars \<phi> = {} \<and> set (vs \<phi>) \<inter> (\<Union>a\<in>set txs. FvarsT (fst a)) = {} \<and> set (vs \<phi>) \<inter> snd ` set txs = {} \<and> length (vs \<phi>) = length txs \<and> distinct (vs \<phi>); \<phi> \<in> F\<rbrakk> \<Longrightarrow> rawpsubst (rawpsubst \<phi> (zip (map Var us) (map snd txs))) (zip (map fst txs) us) = rawpsubst (rawpsubst \<phi> (zip (map Var (vs \<phi>)) (map snd txs))) (zip (map fst txs) (vs \<phi>))
 3. \<lbrakk>F \<subseteq> fmla; finite F; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; distinct (map snd txs); set us \<subseteq> var; set us \<inter> \<Union> (Fvars ` F) = {}; set us \<inter> (\<Union>a\<in>set txs. FvarsT (fst a)) = {}; set us \<inter> snd ` set txs = {}; length us = length txs; distinct us; \<And>\<phi>. \<phi> \<in> F \<Longrightarrow> set (vs \<phi>) \<subseteq> var \<and> set (vs \<phi>) \<inter> Fvars \<phi> = {} \<and> set (vs \<phi>) \<inter> (\<Union>a\<in>set txs. FvarsT (fst a)) = {} \<and> set (vs \<phi>) \<inter> snd ` set txs = {} \<and> length (vs \<phi>) = length txs \<and> distinct (vs \<phi>); \<phi> \<in> F\<rbrakk> \<Longrightarrow> \<phi> \<in> F
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>F \<subseteq> fmla; finite F; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; distinct (map snd txs); set us \<subseteq> var; set us \<inter> \<Union> (Fvars ` F) = {}; set us \<inter> (\<Union>a\<in>set txs. FvarsT (fst a)) = {}; set us \<inter> snd ` set txs = {}; length us = length txs; distinct us; \<And>\<phi>. \<phi> \<in> F \<Longrightarrow> set (vs \<phi>) \<subseteq> var \<and> set (vs \<phi>) \<inter> Fvars \<phi> = {} \<and> set (vs \<phi>) \<inter> (\<Union>a\<in>set txs. FvarsT (fst a)) = {} \<and> set (vs \<phi>) \<inter> snd ` set txs = {} \<and> length (vs \<phi>) = length txs \<and> distinct (vs \<phi>); \<phi> \<in> F\<rbrakk> \<Longrightarrow> rawpsubst (rawpsubst \<phi> (zip (map Var (vs \<phi>)) (map snd txs))) (zip (map fst txs) (vs \<phi>)) \<in> fmla
[PROOF STEP]
by (auto intro!: rawpsubst dest!: set_zip_D)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>F \<subseteq> fmla; finite F; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; distinct (map snd txs); set us \<subseteq> var; set us \<inter> \<Union> (Fvars ` F) = {}; set us \<inter> (\<Union>a\<in>set txs. FvarsT (fst a)) = {}; set us \<inter> snd ` set txs = {}; length us = length txs; distinct us; \<And>\<phi>. \<phi> \<in> F \<Longrightarrow> set (vs \<phi>) \<subseteq> var \<and> set (vs \<phi>) \<inter> Fvars \<phi> = {} \<and> set (vs \<phi>) \<inter> (\<Union>a\<in>set txs. FvarsT (fst a)) = {} \<and> set (vs \<phi>) \<inter> snd ` set txs = {} \<and> length (vs \<phi>) = length txs \<and> distinct (vs \<phi>); \<phi> \<in> F\<rbrakk> \<Longrightarrow> rawpsubst (rawpsubst \<phi> (zip (map Var us) (map snd txs))) (zip (map fst txs) us) = rawpsubst (rawpsubst \<phi> (zip (map Var (vs \<phi>)) (map snd txs))) (zip (map fst txs) (vs \<phi>))
 2. \<lbrakk>F \<subseteq> fmla; finite F; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; distinct (map snd txs); set us \<subseteq> var; set us \<inter> \<Union> (Fvars ` F) = {}; set us \<inter> (\<Union>a\<in>set txs. FvarsT (fst a)) = {}; set us \<inter> snd ` set txs = {}; length us = length txs; distinct us; \<And>\<phi>. \<phi> \<in> F \<Longrightarrow> set (vs \<phi>) \<subseteq> var \<and> set (vs \<phi>) \<inter> Fvars \<phi> = {} \<and> set (vs \<phi>) \<inter> (\<Union>a\<in>set txs. FvarsT (fst a)) = {} \<and> set (vs \<phi>) \<inter> snd ` set txs = {} \<and> length (vs \<phi>) = length txs \<and> distinct (vs \<phi>); \<phi> \<in> F\<rbrakk> \<Longrightarrow> \<phi> \<in> F
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>F \<subseteq> fmla; finite F; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; distinct (map snd txs); set us \<subseteq> var; set us \<inter> \<Union> (Fvars ` F) = {}; set us \<inter> (\<Union>a\<in>set txs. FvarsT (fst a)) = {}; set us \<inter> snd ` set txs = {}; length us = length txs; distinct us; \<And>\<phi>. \<phi> \<in> F \<Longrightarrow> set (vs \<phi>) \<subseteq> var \<and> set (vs \<phi>) \<inter> Fvars \<phi> = {} \<and> set (vs \<phi>) \<inter> (\<Union>a\<in>set txs. FvarsT (fst a)) = {} \<and> set (vs \<phi>) \<inter> snd ` set txs = {} \<and> length (vs \<phi>) = length txs \<and> distinct (vs \<phi>); \<phi> \<in> F\<rbrakk> \<Longrightarrow> rawpsubst (rawpsubst \<phi> (zip (map Var us) (map snd txs))) (zip (map fst txs) us) = rawpsubst (rawpsubst \<phi> (zip (map Var (vs \<phi>)) (map snd txs))) (zip (map fst txs) (vs \<phi>))
[PROOF STEP]
by (rule rawpsubst_compose_freshVar2)
              (auto intro!: rawpsubst dest!: set_zip_D)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>F \<subseteq> fmla; finite F; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; distinct (map snd txs); set us \<subseteq> var; set us \<inter> \<Union> (Fvars ` F) = {}; set us \<inter> (\<Union>a\<in>set txs. FvarsT (fst a)) = {}; set us \<inter> snd ` set txs = {}; length us = length txs; distinct us; \<And>\<phi>. \<phi> \<in> F \<Longrightarrow> set (vs \<phi>) \<subseteq> var \<and> set (vs \<phi>) \<inter> Fvars \<phi> = {} \<and> set (vs \<phi>) \<inter> (\<Union>a\<in>set txs. FvarsT (fst a)) = {} \<and> set (vs \<phi>) \<inter> snd ` set txs = {} \<and> length (vs \<phi>) = length txs \<and> distinct (vs \<phi>); \<phi> \<in> F\<rbrakk> \<Longrightarrow> \<phi> \<in> F
[PROOF STEP]
.
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
.
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
.
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>F \<subseteq> fmla; finite F; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; distinct (map snd txs); set us \<subseteq> var; set us \<inter> \<Union> (Fvars ` F) = {}; set us \<inter> \<Union> (FvarsT ` fst ` set txs) = {}; set us \<inter> snd ` set txs = {}; length us = length txs; distinct us; \<And>\<phi>. \<phi> \<in> F \<Longrightarrow> set (vs \<phi>) \<subseteq> var \<and> set (vs \<phi>) \<inter> Fvars \<phi> = {} \<and> set (vs \<phi>) \<inter> \<Union> (FvarsT ` fst ` set txs) = {} \<and> set (vs \<phi>) \<inter> snd ` set txs = {} \<and> length (vs \<phi>) = length txs \<and> distinct (vs \<phi>)\<rbrakk> \<Longrightarrow> prv (imp (scnj ((\<lambda>\<phi>. rawpsubst (rawpsubst \<phi> (zip (map Var (vs \<phi>)) (map snd txs))) (zip (map fst txs) (vs \<phi>))) ` F)) (scnj ((\<lambda>\<phi>. rawpsubst \<phi> (zip (map fst txs) us)) ` (\<lambda>\<phi>. rawpsubst \<phi> (zip (map Var us) (map snd txs))) ` F)))
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>F \<subseteq> fmla; finite F; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; distinct (map snd txs); set us \<subseteq> var; set us \<inter> \<Union> (Fvars ` F) = {}; set us \<inter> \<Union> (FvarsT ` fst ` set txs) = {}; set us \<inter> snd ` set txs = {}; length us = length txs; distinct us; \<And>\<phi>. \<phi> \<in> F \<Longrightarrow> set (vs \<phi>) \<subseteq> var \<and> set (vs \<phi>) \<inter> Fvars \<phi> = {} \<and> set (vs \<phi>) \<inter> \<Union> (FvarsT ` fst ` set txs) = {} \<and> set (vs \<phi>) \<inter> snd ` set txs = {} \<and> length (vs \<phi>) = length txs \<and> distinct (vs \<phi>)\<rbrakk> \<Longrightarrow> prv (imp (scnj ((\<lambda>\<phi>. rawpsubst (rawpsubst \<phi> (zip (map Var (vs \<phi>)) (map snd txs))) (zip (map fst txs) (vs \<phi>))) ` F)) (scnj ((\<lambda>\<phi>. rawpsubst \<phi> (zip (map fst txs) us)) ` (\<lambda>\<phi>. rawpsubst \<phi> (zip (map Var us) (map snd txs))) ` F)))
[PROOF STEP]
apply(rule prv_scnj_mono_imp)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<lbrakk>F \<subseteq> fmla; finite F; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; distinct (map snd txs); set us \<subseteq> var; set us \<inter> \<Union> (Fvars ` F) = {}; set us \<inter> \<Union> (FvarsT ` fst ` set txs) = {}; set us \<inter> snd ` set txs = {}; length us = length txs; distinct us; \<And>\<phi>. \<phi> \<in> F \<Longrightarrow> set (vs \<phi>) \<subseteq> var \<and> set (vs \<phi>) \<inter> Fvars \<phi> = {} \<and> set (vs \<phi>) \<inter> \<Union> (FvarsT ` fst ` set txs) = {} \<and> set (vs \<phi>) \<inter> snd ` set txs = {} \<and> length (vs \<phi>) = length txs \<and> distinct (vs \<phi>)\<rbrakk> \<Longrightarrow> (\<lambda>\<phi>. rawpsubst (rawpsubst \<phi> (zip (map Var (vs \<phi>)) (map snd txs))) (zip (map fst txs) (vs \<phi>))) ` F \<subseteq> fmla
 2. \<lbrakk>F \<subseteq> fmla; finite F; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; distinct (map snd txs); set us \<subseteq> var; set us \<inter> \<Union> (Fvars ` F) = {}; set us \<inter> \<Union> (FvarsT ` fst ` set txs) = {}; set us \<inter> snd ` set txs = {}; length us = length txs; distinct us; \<And>\<phi>. \<phi> \<in> F \<Longrightarrow> set (vs \<phi>) \<subseteq> var \<and> set (vs \<phi>) \<inter> Fvars \<phi> = {} \<and> set (vs \<phi>) \<inter> \<Union> (FvarsT ` fst ` set txs) = {} \<and> set (vs \<phi>) \<inter> snd ` set txs = {} \<and> length (vs \<phi>) = length txs \<and> distinct (vs \<phi>)\<rbrakk> \<Longrightarrow> (\<lambda>\<phi>. rawpsubst \<phi> (zip (map fst txs) us)) ` (\<lambda>\<phi>. rawpsubst \<phi> (zip (map Var us) (map snd txs))) ` F \<subseteq> fmla
 3. \<lbrakk>F \<subseteq> fmla; finite F; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; distinct (map snd txs); set us \<subseteq> var; set us \<inter> \<Union> (Fvars ` F) = {}; set us \<inter> \<Union> (FvarsT ` fst ` set txs) = {}; set us \<inter> snd ` set txs = {}; length us = length txs; distinct us; \<And>\<phi>. \<phi> \<in> F \<Longrightarrow> set (vs \<phi>) \<subseteq> var \<and> set (vs \<phi>) \<inter> Fvars \<phi> = {} \<and> set (vs \<phi>) \<inter> \<Union> (FvarsT ` fst ` set txs) = {} \<and> set (vs \<phi>) \<inter> snd ` set txs = {} \<and> length (vs \<phi>) = length txs \<and> distinct (vs \<phi>)\<rbrakk> \<Longrightarrow> finite ((\<lambda>\<phi>. rawpsubst (rawpsubst \<phi> (zip (map Var (vs \<phi>)) (map snd txs))) (zip (map fst txs) (vs \<phi>))) ` F)
 4. \<lbrakk>F \<subseteq> fmla; finite F; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; distinct (map snd txs); set us \<subseteq> var; set us \<inter> \<Union> (Fvars ` F) = {}; set us \<inter> \<Union> (FvarsT ` fst ` set txs) = {}; set us \<inter> snd ` set txs = {}; length us = length txs; distinct us; \<And>\<phi>. \<phi> \<in> F \<Longrightarrow> set (vs \<phi>) \<subseteq> var \<and> set (vs \<phi>) \<inter> Fvars \<phi> = {} \<and> set (vs \<phi>) \<inter> \<Union> (FvarsT ` fst ` set txs) = {} \<and> set (vs \<phi>) \<inter> snd ` set txs = {} \<and> length (vs \<phi>) = length txs \<and> distinct (vs \<phi>)\<rbrakk> \<Longrightarrow> finite ((\<lambda>\<phi>. rawpsubst \<phi> (zip (map fst txs) us)) ` (\<lambda>\<phi>. rawpsubst \<phi> (zip (map Var us) (map snd txs))) ` F)
 5. \<lbrakk>F \<subseteq> fmla; finite F; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; distinct (map snd txs); set us \<subseteq> var; set us \<inter> \<Union> (Fvars ` F) = {}; set us \<inter> \<Union> (FvarsT ` fst ` set txs) = {}; set us \<inter> snd ` set txs = {}; length us = length txs; distinct us; \<And>\<phi>. \<phi> \<in> F \<Longrightarrow> set (vs \<phi>) \<subseteq> var \<and> set (vs \<phi>) \<inter> Fvars \<phi> = {} \<and> set (vs \<phi>) \<inter> \<Union> (FvarsT ` fst ` set txs) = {} \<and> set (vs \<phi>) \<inter> snd ` set txs = {} \<and> length (vs \<phi>) = length txs \<and> distinct (vs \<phi>)\<rbrakk> \<Longrightarrow> \<forall>\<phi>2\<in>(\<lambda>\<phi>. rawpsubst \<phi> (zip (map fst txs) us)) ` (\<lambda>\<phi>. rawpsubst \<phi> (zip (map Var us) (map snd txs))) ` F. \<exists>\<phi>1\<in>(\<lambda>\<phi>. rawpsubst (rawpsubst \<phi> (zip (map Var (vs \<phi>)) (map snd txs))) (zip (map fst txs) (vs \<phi>))) ` F. prv (imp \<phi>1 \<phi>2)
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>F \<subseteq> fmla; finite F; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; distinct (map snd txs); set us \<subseteq> var; set us \<inter> \<Union> (Fvars ` F) = {}; set us \<inter> \<Union> (FvarsT ` fst ` set txs) = {}; set us \<inter> snd ` set txs = {}; length us = length txs; distinct us; \<And>\<phi>. \<phi> \<in> F \<Longrightarrow> set (vs \<phi>) \<subseteq> var \<and> set (vs \<phi>) \<inter> Fvars \<phi> = {} \<and> set (vs \<phi>) \<inter> \<Union> (FvarsT ` fst ` set txs) = {} \<and> set (vs \<phi>) \<inter> snd ` set txs = {} \<and> length (vs \<phi>) = length txs \<and> distinct (vs \<phi>)\<rbrakk> \<Longrightarrow> (\<lambda>\<phi>. rawpsubst (rawpsubst \<phi> (zip (map Var (vs \<phi>)) (map snd txs))) (zip (map fst txs) (vs \<phi>))) ` F \<subseteq> fmla
[PROOF STEP]
by (auto intro!: rawpsubst dest!: set_zip_D)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>F \<subseteq> fmla; finite F; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; distinct (map snd txs); set us \<subseteq> var; set us \<inter> \<Union> (Fvars ` F) = {}; set us \<inter> \<Union> (FvarsT ` fst ` set txs) = {}; set us \<inter> snd ` set txs = {}; length us = length txs; distinct us; \<And>\<phi>. \<phi> \<in> F \<Longrightarrow> set (vs \<phi>) \<subseteq> var \<and> set (vs \<phi>) \<inter> Fvars \<phi> = {} \<and> set (vs \<phi>) \<inter> \<Union> (FvarsT ` fst ` set txs) = {} \<and> set (vs \<phi>) \<inter> snd ` set txs = {} \<and> length (vs \<phi>) = length txs \<and> distinct (vs \<phi>)\<rbrakk> \<Longrightarrow> (\<lambda>\<phi>. rawpsubst \<phi> (zip (map fst txs) us)) ` (\<lambda>\<phi>. rawpsubst \<phi> (zip (map Var us) (map snd txs))) ` F \<subseteq> fmla
 2. \<lbrakk>F \<subseteq> fmla; finite F; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; distinct (map snd txs); set us \<subseteq> var; set us \<inter> \<Union> (Fvars ` F) = {}; set us \<inter> \<Union> (FvarsT ` fst ` set txs) = {}; set us \<inter> snd ` set txs = {}; length us = length txs; distinct us; \<And>\<phi>. \<phi> \<in> F \<Longrightarrow> set (vs \<phi>) \<subseteq> var \<and> set (vs \<phi>) \<inter> Fvars \<phi> = {} \<and> set (vs \<phi>) \<inter> \<Union> (FvarsT ` fst ` set txs) = {} \<and> set (vs \<phi>) \<inter> snd ` set txs = {} \<and> length (vs \<phi>) = length txs \<and> distinct (vs \<phi>)\<rbrakk> \<Longrightarrow> finite ((\<lambda>\<phi>. rawpsubst (rawpsubst \<phi> (zip (map Var (vs \<phi>)) (map snd txs))) (zip (map fst txs) (vs \<phi>))) ` F)
 3. \<lbrakk>F \<subseteq> fmla; finite F; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; distinct (map snd txs); set us \<subseteq> var; set us \<inter> \<Union> (Fvars ` F) = {}; set us \<inter> \<Union> (FvarsT ` fst ` set txs) = {}; set us \<inter> snd ` set txs = {}; length us = length txs; distinct us; \<And>\<phi>. \<phi> \<in> F \<Longrightarrow> set (vs \<phi>) \<subseteq> var \<and> set (vs \<phi>) \<inter> Fvars \<phi> = {} \<and> set (vs \<phi>) \<inter> \<Union> (FvarsT ` fst ` set txs) = {} \<and> set (vs \<phi>) \<inter> snd ` set txs = {} \<and> length (vs \<phi>) = length txs \<and> distinct (vs \<phi>)\<rbrakk> \<Longrightarrow> finite ((\<lambda>\<phi>. rawpsubst \<phi> (zip (map fst txs) us)) ` (\<lambda>\<phi>. rawpsubst \<phi> (zip (map Var us) (map snd txs))) ` F)
 4. \<lbrakk>F \<subseteq> fmla; finite F; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; distinct (map snd txs); set us \<subseteq> var; set us \<inter> \<Union> (Fvars ` F) = {}; set us \<inter> \<Union> (FvarsT ` fst ` set txs) = {}; set us \<inter> snd ` set txs = {}; length us = length txs; distinct us; \<And>\<phi>. \<phi> \<in> F \<Longrightarrow> set (vs \<phi>) \<subseteq> var \<and> set (vs \<phi>) \<inter> Fvars \<phi> = {} \<and> set (vs \<phi>) \<inter> \<Union> (FvarsT ` fst ` set txs) = {} \<and> set (vs \<phi>) \<inter> snd ` set txs = {} \<and> length (vs \<phi>) = length txs \<and> distinct (vs \<phi>)\<rbrakk> \<Longrightarrow> \<forall>\<phi>2\<in>(\<lambda>\<phi>. rawpsubst \<phi> (zip (map fst txs) us)) ` (\<lambda>\<phi>. rawpsubst \<phi> (zip (map Var us) (map snd txs))) ` F. \<exists>\<phi>1\<in>(\<lambda>\<phi>. rawpsubst (rawpsubst \<phi> (zip (map Var (vs \<phi>)) (map snd txs))) (zip (map fst txs) (vs \<phi>))) ` F. prv (imp \<phi>1 \<phi>2)
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>F \<subseteq> fmla; finite F; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; distinct (map snd txs); set us \<subseteq> var; set us \<inter> \<Union> (Fvars ` F) = {}; set us \<inter> \<Union> (FvarsT ` fst ` set txs) = {}; set us \<inter> snd ` set txs = {}; length us = length txs; distinct us; \<And>\<phi>. \<phi> \<in> F \<Longrightarrow> set (vs \<phi>) \<subseteq> var \<and> set (vs \<phi>) \<inter> Fvars \<phi> = {} \<and> set (vs \<phi>) \<inter> \<Union> (FvarsT ` fst ` set txs) = {} \<and> set (vs \<phi>) \<inter> snd ` set txs = {} \<and> length (vs \<phi>) = length txs \<and> distinct (vs \<phi>)\<rbrakk> \<Longrightarrow> (\<lambda>\<phi>. rawpsubst \<phi> (zip (map fst txs) us)) ` (\<lambda>\<phi>. rawpsubst \<phi> (zip (map Var us) (map snd txs))) ` F \<subseteq> fmla
[PROOF STEP]
by (auto intro!: rawpsubst dest!: set_zip_D)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>F \<subseteq> fmla; finite F; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; distinct (map snd txs); set us \<subseteq> var; set us \<inter> \<Union> (Fvars ` F) = {}; set us \<inter> \<Union> (FvarsT ` fst ` set txs) = {}; set us \<inter> snd ` set txs = {}; length us = length txs; distinct us; \<And>\<phi>. \<phi> \<in> F \<Longrightarrow> set (vs \<phi>) \<subseteq> var \<and> set (vs \<phi>) \<inter> Fvars \<phi> = {} \<and> set (vs \<phi>) \<inter> \<Union> (FvarsT ` fst ` set txs) = {} \<and> set (vs \<phi>) \<inter> snd ` set txs = {} \<and> length (vs \<phi>) = length txs \<and> distinct (vs \<phi>)\<rbrakk> \<Longrightarrow> finite ((\<lambda>\<phi>. rawpsubst (rawpsubst \<phi> (zip (map Var (vs \<phi>)) (map snd txs))) (zip (map fst txs) (vs \<phi>))) ` F)
 2. \<lbrakk>F \<subseteq> fmla; finite F; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; distinct (map snd txs); set us \<subseteq> var; set us \<inter> \<Union> (Fvars ` F) = {}; set us \<inter> \<Union> (FvarsT ` fst ` set txs) = {}; set us \<inter> snd ` set txs = {}; length us = length txs; distinct us; \<And>\<phi>. \<phi> \<in> F \<Longrightarrow> set (vs \<phi>) \<subseteq> var \<and> set (vs \<phi>) \<inter> Fvars \<phi> = {} \<and> set (vs \<phi>) \<inter> \<Union> (FvarsT ` fst ` set txs) = {} \<and> set (vs \<phi>) \<inter> snd ` set txs = {} \<and> length (vs \<phi>) = length txs \<and> distinct (vs \<phi>)\<rbrakk> \<Longrightarrow> finite ((\<lambda>\<phi>. rawpsubst \<phi> (zip (map fst txs) us)) ` (\<lambda>\<phi>. rawpsubst \<phi> (zip (map Var us) (map snd txs))) ` F)
 3. \<lbrakk>F \<subseteq> fmla; finite F; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; distinct (map snd txs); set us \<subseteq> var; set us \<inter> \<Union> (Fvars ` F) = {}; set us \<inter> \<Union> (FvarsT ` fst ` set txs) = {}; set us \<inter> snd ` set txs = {}; length us = length txs; distinct us; \<And>\<phi>. \<phi> \<in> F \<Longrightarrow> set (vs \<phi>) \<subseteq> var \<and> set (vs \<phi>) \<inter> Fvars \<phi> = {} \<and> set (vs \<phi>) \<inter> \<Union> (FvarsT ` fst ` set txs) = {} \<and> set (vs \<phi>) \<inter> snd ` set txs = {} \<and> length (vs \<phi>) = length txs \<and> distinct (vs \<phi>)\<rbrakk> \<Longrightarrow> \<forall>\<phi>2\<in>(\<lambda>\<phi>. rawpsubst \<phi> (zip (map fst txs) us)) ` (\<lambda>\<phi>. rawpsubst \<phi> (zip (map Var us) (map snd txs))) ` F. \<exists>\<phi>1\<in>(\<lambda>\<phi>. rawpsubst (rawpsubst \<phi> (zip (map Var (vs \<phi>)) (map snd txs))) (zip (map fst txs) (vs \<phi>))) ` F. prv (imp \<phi>1 \<phi>2)
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>F \<subseteq> fmla; finite F; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; distinct (map snd txs); set us \<subseteq> var; set us \<inter> \<Union> (Fvars ` F) = {}; set us \<inter> \<Union> (FvarsT ` fst ` set txs) = {}; set us \<inter> snd ` set txs = {}; length us = length txs; distinct us; \<And>\<phi>. \<phi> \<in> F \<Longrightarrow> set (vs \<phi>) \<subseteq> var \<and> set (vs \<phi>) \<inter> Fvars \<phi> = {} \<and> set (vs \<phi>) \<inter> \<Union> (FvarsT ` fst ` set txs) = {} \<and> set (vs \<phi>) \<inter> snd ` set txs = {} \<and> length (vs \<phi>) = length txs \<and> distinct (vs \<phi>)\<rbrakk> \<Longrightarrow> finite ((\<lambda>\<phi>. rawpsubst (rawpsubst \<phi> (zip (map Var (vs \<phi>)) (map snd txs))) (zip (map fst txs) (vs \<phi>))) ` F)
[PROOF STEP]
by (auto intro!: rawpsubst dest!: set_zip_D)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>F \<subseteq> fmla; finite F; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; distinct (map snd txs); set us \<subseteq> var; set us \<inter> \<Union> (Fvars ` F) = {}; set us \<inter> \<Union> (FvarsT ` fst ` set txs) = {}; set us \<inter> snd ` set txs = {}; length us = length txs; distinct us; \<And>\<phi>. \<phi> \<in> F \<Longrightarrow> set (vs \<phi>) \<subseteq> var \<and> set (vs \<phi>) \<inter> Fvars \<phi> = {} \<and> set (vs \<phi>) \<inter> \<Union> (FvarsT ` fst ` set txs) = {} \<and> set (vs \<phi>) \<inter> snd ` set txs = {} \<and> length (vs \<phi>) = length txs \<and> distinct (vs \<phi>)\<rbrakk> \<Longrightarrow> finite ((\<lambda>\<phi>. rawpsubst \<phi> (zip (map fst txs) us)) ` (\<lambda>\<phi>. rawpsubst \<phi> (zip (map Var us) (map snd txs))) ` F)
 2. \<lbrakk>F \<subseteq> fmla; finite F; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; distinct (map snd txs); set us \<subseteq> var; set us \<inter> \<Union> (Fvars ` F) = {}; set us \<inter> \<Union> (FvarsT ` fst ` set txs) = {}; set us \<inter> snd ` set txs = {}; length us = length txs; distinct us; \<And>\<phi>. \<phi> \<in> F \<Longrightarrow> set (vs \<phi>) \<subseteq> var \<and> set (vs \<phi>) \<inter> Fvars \<phi> = {} \<and> set (vs \<phi>) \<inter> \<Union> (FvarsT ` fst ` set txs) = {} \<and> set (vs \<phi>) \<inter> snd ` set txs = {} \<and> length (vs \<phi>) = length txs \<and> distinct (vs \<phi>)\<rbrakk> \<Longrightarrow> \<forall>\<phi>2\<in>(\<lambda>\<phi>. rawpsubst \<phi> (zip (map fst txs) us)) ` (\<lambda>\<phi>. rawpsubst \<phi> (zip (map Var us) (map snd txs))) ` F. \<exists>\<phi>1\<in>(\<lambda>\<phi>. rawpsubst (rawpsubst \<phi> (zip (map Var (vs \<phi>)) (map snd txs))) (zip (map fst txs) (vs \<phi>))) ` F. prv (imp \<phi>1 \<phi>2)
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>F \<subseteq> fmla; finite F; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; distinct (map snd txs); set us \<subseteq> var; set us \<inter> \<Union> (Fvars ` F) = {}; set us \<inter> \<Union> (FvarsT ` fst ` set txs) = {}; set us \<inter> snd ` set txs = {}; length us = length txs; distinct us; \<And>\<phi>. \<phi> \<in> F \<Longrightarrow> set (vs \<phi>) \<subseteq> var \<and> set (vs \<phi>) \<inter> Fvars \<phi> = {} \<and> set (vs \<phi>) \<inter> \<Union> (FvarsT ` fst ` set txs) = {} \<and> set (vs \<phi>) \<inter> snd ` set txs = {} \<and> length (vs \<phi>) = length txs \<and> distinct (vs \<phi>)\<rbrakk> \<Longrightarrow> finite ((\<lambda>\<phi>. rawpsubst \<phi> (zip (map fst txs) us)) ` (\<lambda>\<phi>. rawpsubst \<phi> (zip (map Var us) (map snd txs))) ` F)
[PROOF STEP]
by (auto intro!: rawpsubst dest!: set_zip_D)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>F \<subseteq> fmla; finite F; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; distinct (map snd txs); set us \<subseteq> var; set us \<inter> \<Union> (Fvars ` F) = {}; set us \<inter> \<Union> (FvarsT ` fst ` set txs) = {}; set us \<inter> snd ` set txs = {}; length us = length txs; distinct us; \<And>\<phi>. \<phi> \<in> F \<Longrightarrow> set (vs \<phi>) \<subseteq> var \<and> set (vs \<phi>) \<inter> Fvars \<phi> = {} \<and> set (vs \<phi>) \<inter> \<Union> (FvarsT ` fst ` set txs) = {} \<and> set (vs \<phi>) \<inter> snd ` set txs = {} \<and> length (vs \<phi>) = length txs \<and> distinct (vs \<phi>)\<rbrakk> \<Longrightarrow> \<forall>\<phi>2\<in>(\<lambda>\<phi>. rawpsubst \<phi> (zip (map fst txs) us)) ` (\<lambda>\<phi>. rawpsubst \<phi> (zip (map Var us) (map snd txs))) ` F. \<exists>\<phi>1\<in>(\<lambda>\<phi>. rawpsubst (rawpsubst \<phi> (zip (map Var (vs \<phi>)) (map snd txs))) (zip (map fst txs) (vs \<phi>))) ` F. prv (imp \<phi>1 \<phi>2)
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>F \<subseteq> fmla; finite F; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; distinct (map snd txs); set us \<subseteq> var; set us \<inter> \<Union> (Fvars ` F) = {}; set us \<inter> \<Union> (FvarsT ` fst ` set txs) = {}; set us \<inter> snd ` set txs = {}; length us = length txs; distinct us; \<And>\<phi>. \<phi> \<in> F \<Longrightarrow> set (vs \<phi>) \<subseteq> var \<and> set (vs \<phi>) \<inter> Fvars \<phi> = {} \<and> set (vs \<phi>) \<inter> \<Union> (FvarsT ` fst ` set txs) = {} \<and> set (vs \<phi>) \<inter> snd ` set txs = {} \<and> length (vs \<phi>) = length txs \<and> distinct (vs \<phi>)\<rbrakk> \<Longrightarrow> \<forall>\<phi>2\<in>(\<lambda>\<phi>. rawpsubst \<phi> (zip (map fst txs) us)) ` (\<lambda>\<phi>. rawpsubst \<phi> (zip (map Var us) (map snd txs))) ` F. \<exists>\<phi>1\<in>(\<lambda>\<phi>. rawpsubst (rawpsubst \<phi> (zip (map Var (vs \<phi>)) (map snd txs))) (zip (map fst txs) (vs \<phi>))) ` F. prv (imp \<phi>1 \<phi>2)
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>\<phi>2. \<lbrakk>F \<subseteq> fmla; finite F; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; distinct (map snd txs); set us \<subseteq> var; set us \<inter> \<Union> (Fvars ` F) = {}; set us \<inter> (\<Union>a\<in>set txs. FvarsT (fst a)) = {}; set us \<inter> snd ` set txs = {}; length us = length txs; distinct us; \<And>\<phi>. \<phi> \<in> F \<Longrightarrow> set (vs \<phi>) \<subseteq> var \<and> set (vs \<phi>) \<inter> Fvars \<phi> = {} \<and> set (vs \<phi>) \<inter> (\<Union>a\<in>set txs. FvarsT (fst a)) = {} \<and> set (vs \<phi>) \<inter> snd ` set txs = {} \<and> length (vs \<phi>) = length txs \<and> distinct (vs \<phi>); \<phi>2 \<in> F\<rbrakk> \<Longrightarrow> \<exists>\<phi>1\<in>F. prv (imp (rawpsubst (rawpsubst \<phi>1 (zip (map Var (vs \<phi>1)) (map snd txs))) (zip (map fst txs) (vs \<phi>1))) (rawpsubst (rawpsubst \<phi>2 (zip (map Var us) (map snd txs))) (zip (map fst txs) us)))
[PROOF STEP]
subgoal for \<phi>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>F \<subseteq> fmla; finite F; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; distinct (map snd txs); set us \<subseteq> var; set us \<inter> \<Union> (Fvars ` F) = {}; set us \<inter> (\<Union>a\<in>set txs. FvarsT (fst a)) = {}; set us \<inter> snd ` set txs = {}; length us = length txs; distinct us; \<And>\<phi>. \<phi> \<in> F \<Longrightarrow> set (vs \<phi>) \<subseteq> var \<and> set (vs \<phi>) \<inter> Fvars \<phi> = {} \<and> set (vs \<phi>) \<inter> (\<Union>a\<in>set txs. FvarsT (fst a)) = {} \<and> set (vs \<phi>) \<inter> snd ` set txs = {} \<and> length (vs \<phi>) = length txs \<and> distinct (vs \<phi>); \<phi> \<in> F\<rbrakk> \<Longrightarrow> \<exists>\<phi>1\<in>F. prv (imp (rawpsubst (rawpsubst \<phi>1 (zip (map Var (vs \<phi>1)) (map snd txs))) (zip (map fst txs) (vs \<phi>1))) (rawpsubst (rawpsubst \<phi> (zip (map Var us) (map snd txs))) (zip (map fst txs) us)))
[PROOF STEP]
apply(rule bexI[of _ \<phi>])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>F \<subseteq> fmla; finite F; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; distinct (map snd txs); set us \<subseteq> var; set us \<inter> \<Union> (Fvars ` F) = {}; set us \<inter> (\<Union>a\<in>set txs. FvarsT (fst a)) = {}; set us \<inter> snd ` set txs = {}; length us = length txs; distinct us; \<And>\<phi>. \<phi> \<in> F \<Longrightarrow> set (vs \<phi>) \<subseteq> var \<and> set (vs \<phi>) \<inter> Fvars \<phi> = {} \<and> set (vs \<phi>) \<inter> (\<Union>a\<in>set txs. FvarsT (fst a)) = {} \<and> set (vs \<phi>) \<inter> snd ` set txs = {} \<and> length (vs \<phi>) = length txs \<and> distinct (vs \<phi>); \<phi> \<in> F\<rbrakk> \<Longrightarrow> prv (imp (rawpsubst (rawpsubst \<phi> (zip (map Var (vs \<phi>)) (map snd txs))) (zip (map fst txs) (vs \<phi>))) (rawpsubst (rawpsubst \<phi> (zip (map Var us) (map snd txs))) (zip (map fst txs) us)))
 2. \<lbrakk>F \<subseteq> fmla; finite F; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; distinct (map snd txs); set us \<subseteq> var; set us \<inter> \<Union> (Fvars ` F) = {}; set us \<inter> (\<Union>a\<in>set txs. FvarsT (fst a)) = {}; set us \<inter> snd ` set txs = {}; length us = length txs; distinct us; \<And>\<phi>. \<phi> \<in> F \<Longrightarrow> set (vs \<phi>) \<subseteq> var \<and> set (vs \<phi>) \<inter> Fvars \<phi> = {} \<and> set (vs \<phi>) \<inter> (\<Union>a\<in>set txs. FvarsT (fst a)) = {} \<and> set (vs \<phi>) \<inter> snd ` set txs = {} \<and> length (vs \<phi>) = length txs \<and> distinct (vs \<phi>); \<phi> \<in> F\<rbrakk> \<Longrightarrow> \<phi> \<in> F
[PROOF STEP]
apply(rule prv_imp_refl2)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>F \<subseteq> fmla; finite F; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; distinct (map snd txs); set us \<subseteq> var; set us \<inter> \<Union> (Fvars ` F) = {}; set us \<inter> (\<Union>a\<in>set txs. FvarsT (fst a)) = {}; set us \<inter> snd ` set txs = {}; length us = length txs; distinct us; \<And>\<phi>. \<phi> \<in> F \<Longrightarrow> set (vs \<phi>) \<subseteq> var \<and> set (vs \<phi>) \<inter> Fvars \<phi> = {} \<and> set (vs \<phi>) \<inter> (\<Union>a\<in>set txs. FvarsT (fst a)) = {} \<and> set (vs \<phi>) \<inter> snd ` set txs = {} \<and> length (vs \<phi>) = length txs \<and> distinct (vs \<phi>); \<phi> \<in> F\<rbrakk> \<Longrightarrow> rawpsubst (rawpsubst \<phi> (zip (map Var (vs \<phi>)) (map snd txs))) (zip (map fst txs) (vs \<phi>)) \<in> fmla
 2. \<lbrakk>F \<subseteq> fmla; finite F; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; distinct (map snd txs); set us \<subseteq> var; set us \<inter> \<Union> (Fvars ` F) = {}; set us \<inter> (\<Union>a\<in>set txs. FvarsT (fst a)) = {}; set us \<inter> snd ` set txs = {}; length us = length txs; distinct us; \<And>\<phi>. \<phi> \<in> F \<Longrightarrow> set (vs \<phi>) \<subseteq> var \<and> set (vs \<phi>) \<inter> Fvars \<phi> = {} \<and> set (vs \<phi>) \<inter> (\<Union>a\<in>set txs. FvarsT (fst a)) = {} \<and> set (vs \<phi>) \<inter> snd ` set txs = {} \<and> length (vs \<phi>) = length txs \<and> distinct (vs \<phi>); \<phi> \<in> F\<rbrakk> \<Longrightarrow> rawpsubst (rawpsubst \<phi> (zip (map Var us) (map snd txs))) (zip (map fst txs) us) \<in> fmla
 3. \<lbrakk>F \<subseteq> fmla; finite F; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; distinct (map snd txs); set us \<subseteq> var; set us \<inter> \<Union> (Fvars ` F) = {}; set us \<inter> (\<Union>a\<in>set txs. FvarsT (fst a)) = {}; set us \<inter> snd ` set txs = {}; length us = length txs; distinct us; \<And>\<phi>. \<phi> \<in> F \<Longrightarrow> set (vs \<phi>) \<subseteq> var \<and> set (vs \<phi>) \<inter> Fvars \<phi> = {} \<and> set (vs \<phi>) \<inter> (\<Union>a\<in>set txs. FvarsT (fst a)) = {} \<and> set (vs \<phi>) \<inter> snd ` set txs = {} \<and> length (vs \<phi>) = length txs \<and> distinct (vs \<phi>); \<phi> \<in> F\<rbrakk> \<Longrightarrow> rawpsubst (rawpsubst \<phi> (zip (map Var (vs \<phi>)) (map snd txs))) (zip (map fst txs) (vs \<phi>)) = rawpsubst (rawpsubst \<phi> (zip (map Var us) (map snd txs))) (zip (map fst txs) us)
 4. \<lbrakk>F \<subseteq> fmla; finite F; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; distinct (map snd txs); set us \<subseteq> var; set us \<inter> \<Union> (Fvars ` F) = {}; set us \<inter> (\<Union>a\<in>set txs. FvarsT (fst a)) = {}; set us \<inter> snd ` set txs = {}; length us = length txs; distinct us; \<And>\<phi>. \<phi> \<in> F \<Longrightarrow> set (vs \<phi>) \<subseteq> var \<and> set (vs \<phi>) \<inter> Fvars \<phi> = {} \<and> set (vs \<phi>) \<inter> (\<Union>a\<in>set txs. FvarsT (fst a)) = {} \<and> set (vs \<phi>) \<inter> snd ` set txs = {} \<and> length (vs \<phi>) = length txs \<and> distinct (vs \<phi>); \<phi> \<in> F\<rbrakk> \<Longrightarrow> \<phi> \<in> F
[PROOF STEP]
apply (auto intro!: rawpsubst dest!: set_zip_D)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>F \<subseteq> fmla; finite F; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; distinct (map snd txs); set us \<subseteq> var; set us \<inter> \<Union> (Fvars ` F) = {}; set us \<inter> (\<Union>a\<in>set txs. FvarsT (fst a)) = {}; set us \<inter> snd ` set txs = {}; length us = length txs; distinct us; \<And>\<phi>. \<phi> \<in> F \<Longrightarrow> set (vs \<phi>) \<subseteq> var \<and> set (vs \<phi>) \<inter> Fvars \<phi> = {} \<and> set (vs \<phi>) \<inter> (\<Union>a\<in>set txs. FvarsT (fst a)) = {} \<and> set (vs \<phi>) \<inter> snd ` set txs = {} \<and> length (vs \<phi>) = length txs \<and> distinct (vs \<phi>); \<phi> \<in> F\<rbrakk> \<Longrightarrow> rawpsubst (rawpsubst \<phi> (zip (map Var (vs \<phi>)) (map snd txs))) (zip (map fst txs) (vs \<phi>)) = rawpsubst (rawpsubst \<phi> (zip (map Var us) (map snd txs))) (zip (map fst txs) us)
[PROOF STEP]
apply(rule rawpsubst_compose_freshVar2)
[PROOF STATE]
proof (prove)
goal (17 subgoals):
 1. \<lbrakk>F \<subseteq> fmla; finite F; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; distinct (map snd txs); set us \<subseteq> var; set us \<inter> \<Union> (Fvars ` F) = {}; set us \<inter> (\<Union>a\<in>set txs. FvarsT (fst a)) = {}; set us \<inter> snd ` set txs = {}; length us = length txs; distinct us; \<And>\<phi>. \<phi> \<in> F \<Longrightarrow> set (vs \<phi>) \<subseteq> var \<and> set (vs \<phi>) \<inter> Fvars \<phi> = {} \<and> set (vs \<phi>) \<inter> (\<Union>a\<in>set txs. FvarsT (fst a)) = {} \<and> set (vs \<phi>) \<inter> snd ` set txs = {} \<and> length (vs \<phi>) = length txs \<and> distinct (vs \<phi>); \<phi> \<in> F\<rbrakk> \<Longrightarrow> \<phi> \<in> fmla
 2. \<lbrakk>F \<subseteq> fmla; finite F; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; distinct (map snd txs); set us \<subseteq> var; set us \<inter> \<Union> (Fvars ` F) = {}; set us \<inter> (\<Union>a\<in>set txs. FvarsT (fst a)) = {}; set us \<inter> snd ` set txs = {}; length us = length txs; distinct us; \<And>\<phi>. \<phi> \<in> F \<Longrightarrow> set (vs \<phi>) \<subseteq> var \<and> set (vs \<phi>) \<inter> Fvars \<phi> = {} \<and> set (vs \<phi>) \<inter> (\<Union>a\<in>set txs. FvarsT (fst a)) = {} \<and> set (vs \<phi>) \<inter> snd ` set txs = {} \<and> length (vs \<phi>) = length txs \<and> distinct (vs \<phi>); \<phi> \<in> F\<rbrakk> \<Longrightarrow> set (map fst txs) \<subseteq> trm
 3. \<lbrakk>F \<subseteq> fmla; finite F; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; distinct (map snd txs); set us \<subseteq> var; set us \<inter> \<Union> (Fvars ` F) = {}; set us \<inter> (\<Union>a\<in>set txs. FvarsT (fst a)) = {}; set us \<inter> snd ` set txs = {}; length us = length txs; distinct us; \<And>\<phi>. \<phi> \<in> F \<Longrightarrow> set (vs \<phi>) \<subseteq> var \<and> set (vs \<phi>) \<inter> Fvars \<phi> = {} \<and> set (vs \<phi>) \<inter> (\<Union>a\<in>set txs. FvarsT (fst a)) = {} \<and> set (vs \<phi>) \<inter> snd ` set txs = {} \<and> length (vs \<phi>) = length txs \<and> distinct (vs \<phi>); \<phi> \<in> F\<rbrakk> \<Longrightarrow> set (map snd txs) \<subseteq> var
 4. \<lbrakk>F \<subseteq> fmla; finite F; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; distinct (map snd txs); set us \<subseteq> var; set us \<inter> \<Union> (Fvars ` F) = {}; set us \<inter> (\<Union>a\<in>set txs. FvarsT (fst a)) = {}; set us \<inter> snd ` set txs = {}; length us = length txs; distinct us; \<And>\<phi>. \<phi> \<in> F \<Longrightarrow> set (vs \<phi>) \<subseteq> var \<and> set (vs \<phi>) \<inter> Fvars \<phi> = {} \<and> set (vs \<phi>) \<inter> (\<Union>a\<in>set txs. FvarsT (fst a)) = {} \<and> set (vs \<phi>) \<inter> snd ` set txs = {} \<and> length (vs \<phi>) = length txs \<and> distinct (vs \<phi>); \<phi> \<in> F\<rbrakk> \<Longrightarrow> distinct (map snd txs)
 5. \<lbrakk>F \<subseteq> fmla; finite F; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; distinct (map snd txs); set us \<subseteq> var; set us \<inter> \<Union> (Fvars ` F) = {}; set us \<inter> (\<Union>a\<in>set txs. FvarsT (fst a)) = {}; set us \<inter> snd ` set txs = {}; length us = length txs; distinct us; \<And>\<phi>. \<phi> \<in> F \<Longrightarrow> set (vs \<phi>) \<subseteq> var \<and> set (vs \<phi>) \<inter> Fvars \<phi> = {} \<and> set (vs \<phi>) \<inter> (\<Union>a\<in>set txs. FvarsT (fst a)) = {} \<and> set (vs \<phi>) \<inter> snd ` set txs = {} \<and> length (vs \<phi>) = length txs \<and> distinct (vs \<phi>); \<phi> \<in> F\<rbrakk> \<Longrightarrow> set (vs \<phi>) \<subseteq> var
 6. \<lbrakk>F \<subseteq> fmla; finite F; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; distinct (map snd txs); set us \<subseteq> var; set us \<inter> \<Union> (Fvars ` F) = {}; set us \<inter> (\<Union>a\<in>set txs. FvarsT (fst a)) = {}; set us \<inter> snd ` set txs = {}; length us = length txs; distinct us; \<And>\<phi>. \<phi> \<in> F \<Longrightarrow> set (vs \<phi>) \<subseteq> var \<and> set (vs \<phi>) \<inter> Fvars \<phi> = {} \<and> set (vs \<phi>) \<inter> (\<Union>a\<in>set txs. FvarsT (fst a)) = {} \<and> set (vs \<phi>) \<inter> snd ` set txs = {} \<and> length (vs \<phi>) = length txs \<and> distinct (vs \<phi>); \<phi> \<in> F\<rbrakk> \<Longrightarrow> distinct (vs \<phi>)
 7. \<lbrakk>F \<subseteq> fmla; finite F; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; distinct (map snd txs); set us \<subseteq> var; set us \<inter> \<Union> (Fvars ` F) = {}; set us \<inter> (\<Union>a\<in>set txs. FvarsT (fst a)) = {}; set us \<inter> snd ` set txs = {}; length us = length txs; distinct us; \<And>\<phi>. \<phi> \<in> F \<Longrightarrow> set (vs \<phi>) \<subseteq> var \<and> set (vs \<phi>) \<inter> Fvars \<phi> = {} \<and> set (vs \<phi>) \<inter> (\<Union>a\<in>set txs. FvarsT (fst a)) = {} \<and> set (vs \<phi>) \<inter> snd ` set txs = {} \<and> length (vs \<phi>) = length txs \<and> distinct (vs \<phi>); \<phi> \<in> F\<rbrakk> \<Longrightarrow> set (vs \<phi>) \<inter> Fvars \<phi> = {}
 8. \<lbrakk>F \<subseteq> fmla; finite F; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; distinct (map snd txs); set us \<subseteq> var; set us \<inter> \<Union> (Fvars ` F) = {}; set us \<inter> (\<Union>a\<in>set txs. FvarsT (fst a)) = {}; set us \<inter> snd ` set txs = {}; length us = length txs; distinct us; \<And>\<phi>. \<phi> \<in> F \<Longrightarrow> set (vs \<phi>) \<subseteq> var \<and> set (vs \<phi>) \<inter> Fvars \<phi> = {} \<and> set (vs \<phi>) \<inter> (\<Union>a\<in>set txs. FvarsT (fst a)) = {} \<and> set (vs \<phi>) \<inter> snd ` set txs = {} \<and> length (vs \<phi>) = length txs \<and> distinct (vs \<phi>); \<phi> \<in> F\<rbrakk> \<Longrightarrow> set (vs \<phi>) \<inter> \<Union> (FvarsT ` set (map fst txs)) = {}
 9. \<lbrakk>F \<subseteq> fmla; finite F; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; distinct (map snd txs); set us \<subseteq> var; set us \<inter> \<Union> (Fvars ` F) = {}; set us \<inter> (\<Union>a\<in>set txs. FvarsT (fst a)) = {}; set us \<inter> snd ` set txs = {}; length us = length txs; distinct us; \<And>\<phi>. \<phi> \<in> F \<Longrightarrow> set (vs \<phi>) \<subseteq> var \<and> set (vs \<phi>) \<inter> Fvars \<phi> = {} \<and> set (vs \<phi>) \<inter> (\<Union>a\<in>set txs. FvarsT (fst a)) = {} \<and> set (vs \<phi>) \<inter> snd ` set txs = {} \<and> length (vs \<phi>) = length txs \<and> distinct (vs \<phi>); \<phi> \<in> F\<rbrakk> \<Longrightarrow> set (vs \<phi>) \<inter> set (map snd txs) = {}
 10. \<lbrakk>F \<subseteq> fmla; finite F; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; distinct (map snd txs); set us \<subseteq> var; set us \<inter> \<Union> (Fvars ` F) = {}; set us \<inter> (\<Union>a\<in>set txs. FvarsT (fst a)) = {}; set us \<inter> snd ` set txs = {}; length us = length txs; distinct us; \<And>\<phi>. \<phi> \<in> F \<Longrightarrow> set (vs \<phi>) \<subseteq> var \<and> set (vs \<phi>) \<inter> Fvars \<phi> = {} \<and> set (vs \<phi>) \<inter> (\<Union>a\<in>set txs. FvarsT (fst a)) = {} \<and> set (vs \<phi>) \<inter> snd ` set txs = {} \<and> length (vs \<phi>) = length txs \<and> distinct (vs \<phi>); \<phi> \<in> F\<rbrakk> \<Longrightarrow> set us \<subseteq> var
A total of 17 subgoals...
[PROOF STEP]
apply (auto intro!: rawpsubst dest!: set_zip_D)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
.
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
.
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
.
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
prv (eqv (scnj ((\<lambda>\<phi>. rawpsubst \<phi> (zip (map fst txs) us)) ` (\<lambda>\<phi>. rawpsubst \<phi> (zip (map Var us) (map snd txs))) ` F)) (scnj ((\<lambda>\<phi>. rawpsubst (rawpsubst \<phi> (zip (map Var (vs \<phi>)) (map snd txs))) (zip (map fst txs) (vs \<phi>))) ` F)))

goal (1 subgoal):
 1. prv (eqv (psubst (scnj F) txs) (scnj ((\<lambda>\<phi>. psubst \<phi> txs) ` F)))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
prv (eqv (rawpsubst (rawpsubst (scnj F) (zip (map Var us) (map snd txs))) (zip (map fst txs) us)) (scnj ((\<lambda>\<phi>. rawpsubst \<phi> (zip (map fst txs) us)) ` (\<lambda>\<phi>. rawpsubst \<phi> (zip (map Var us) (map snd txs))) ` F)))
prv (eqv (scnj ((\<lambda>\<phi>. rawpsubst \<phi> (zip (map fst txs) us)) ` (\<lambda>\<phi>. rawpsubst \<phi> (zip (map Var us) (map snd txs))) ` F)) (scnj ((\<lambda>\<phi>. rawpsubst (rawpsubst \<phi> (zip (map Var (vs \<phi>)) (map snd txs))) (zip (map fst txs) (vs \<phi>))) ` F)))
[PROOF STEP]
have "prv (eqv (rawpsubst (rawpsubst (scnj F) ?uxs) ?tus)
           (scnj ((\<lambda>\<phi>. rawpsubst (rawpsubst \<phi> (?vxs \<phi>)) (?tvs \<phi>)) ` F)))"
[PROOF STATE]
proof (prove)
using this:
prv (eqv (rawpsubst (rawpsubst (scnj F) (zip (map Var us) (map snd txs))) (zip (map fst txs) us)) (scnj ((\<lambda>\<phi>. rawpsubst \<phi> (zip (map fst txs) us)) ` (\<lambda>\<phi>. rawpsubst \<phi> (zip (map Var us) (map snd txs))) ` F)))
prv (eqv (scnj ((\<lambda>\<phi>. rawpsubst \<phi> (zip (map fst txs) us)) ` (\<lambda>\<phi>. rawpsubst \<phi> (zip (map Var us) (map snd txs))) ` F)) (scnj ((\<lambda>\<phi>. rawpsubst (rawpsubst \<phi> (zip (map Var (vs \<phi>)) (map snd txs))) (zip (map fst txs) (vs \<phi>))) ` F)))

goal (1 subgoal):
 1. prv (eqv (rawpsubst (rawpsubst (scnj F) (zip (map Var us) (map snd txs))) (zip (map fst txs) us)) (scnj ((\<lambda>\<phi>. rawpsubst (rawpsubst \<phi> (zip (map Var (vs \<phi>)) (map snd txs))) (zip (map fst txs) (vs \<phi>))) ` F)))
[PROOF STEP]
using assms us_facts
[PROOF STATE]
proof (prove)
using this:
prv (eqv (rawpsubst (rawpsubst (scnj F) (zip (map Var us) (map snd txs))) (zip (map fst txs) us)) (scnj ((\<lambda>\<phi>. rawpsubst \<phi> (zip (map fst txs) us)) ` (\<lambda>\<phi>. rawpsubst \<phi> (zip (map Var us) (map snd txs))) ` F)))
prv (eqv (scnj ((\<lambda>\<phi>. rawpsubst \<phi> (zip (map fst txs) us)) ` (\<lambda>\<phi>. rawpsubst \<phi> (zip (map Var us) (map snd txs))) ` F)) (scnj ((\<lambda>\<phi>. rawpsubst (rawpsubst \<phi> (zip (map Var (vs \<phi>)) (map snd txs))) (zip (map fst txs) (vs \<phi>))) ` F)))
F \<subseteq> fmla
finite F
snd ` set txs \<subseteq> var
fst ` set txs \<subseteq> trm
distinct (map snd txs)
set us \<subseteq> var
set us \<inter> \<Union> (Fvars ` F) = {}
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 (eqv (rawpsubst (rawpsubst (scnj F) (zip (map Var us) (map snd txs))) (zip (map fst txs) us)) (scnj ((\<lambda>\<phi>. rawpsubst (rawpsubst \<phi> (zip (map Var (vs \<phi>)) (map snd txs))) (zip (map fst txs) (vs \<phi>))) ` F)))
[PROOF STEP]
apply -
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>prv (eqv (rawpsubst (rawpsubst (scnj F) (zip (map Var us) (map snd txs))) (zip (map fst txs) us)) (scnj ((\<lambda>\<phi>. rawpsubst \<phi> (zip (map fst txs) us)) ` (\<lambda>\<phi>. rawpsubst \<phi> (zip (map Var us) (map snd txs))) ` F))); prv (eqv (scnj ((\<lambda>\<phi>. rawpsubst \<phi> (zip (map fst txs) us)) ` (\<lambda>\<phi>. rawpsubst \<phi> (zip (map Var us) (map snd txs))) ` F)) (scnj ((\<lambda>\<phi>. rawpsubst (rawpsubst \<phi> (zip (map Var (vs \<phi>)) (map snd txs))) (zip (map fst txs) (vs \<phi>))) ` F))); F \<subseteq> fmla; finite F; snd ` set txs \<subseteq> var; fst ` set txs \<subseteq> trm; distinct (map snd txs); set us \<subseteq> var; set us \<inter> \<Union> (Fvars ` F) = {}; set us \<inter> \<Union> (FvarsT ` fst ` set txs) = {}; set us \<inter> snd ` set txs = {}; length us = length txs; distinct us\<rbrakk> \<Longrightarrow> prv (eqv (rawpsubst (rawpsubst (scnj F) (zip (map Var us) (map snd txs))) (zip (map fst txs) us)) (scnj ((\<lambda>\<phi>. rawpsubst (rawpsubst \<phi> (zip (map Var (vs \<phi>)) (map snd txs))) (zip (map fst txs) (vs \<phi>))) ` F)))
[PROOF STEP]
by (rule prv_eqv_trans) (auto intro!: rawpsubst dest!: set_zip_D)
[PROOF STATE]
proof (state)
this:
prv (eqv (rawpsubst (rawpsubst (scnj F) (zip (map Var us) (map snd txs))) (zip (map fst txs) us)) (scnj ((\<lambda>\<phi>. rawpsubst (rawpsubst \<phi> (zip (map Var (vs \<phi>)) (map snd txs))) (zip (map fst txs) (vs \<phi>))) ` F)))

goal (1 subgoal):
 1. prv (eqv (psubst (scnj F) txs) (scnj ((\<lambda>\<phi>. psubst \<phi> txs) ` F)))
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
prv (eqv (rawpsubst (rawpsubst (scnj F) (zip (map Var us) (map snd txs))) (zip (map fst txs) us)) (scnj ((\<lambda>\<phi>. rawpsubst (rawpsubst \<phi> (zip (map Var (vs \<phi>)) (map snd txs))) (zip (map fst txs) (vs \<phi>))) ` F)))

goal (1 subgoal):
 1. prv (eqv (psubst (scnj F) txs) (scnj ((\<lambda>\<phi>. psubst \<phi> txs) ` F)))
[PROOF STEP]
unfolding psubst_def
[PROOF STATE]
proof (prove)
using this:
prv (eqv (rawpsubst (rawpsubst (scnj F) (zip (map Var us) (map snd txs))) (zip (map fst txs) us)) (scnj ((\<lambda>\<phi>. rawpsubst (rawpsubst \<phi> (zip (map Var (vs \<phi>)) (map snd txs))) (zip (map fst txs) (vs \<phi>))) ` F)))

goal (1 subgoal):
 1. prv (eqv (let xs = map snd txs; ts = map fst txs; us = getFrN xs ts [scnj F] (length xs) in rawpsubst (rawpsubst (scnj F) (zip (map Var us) xs)) (zip ts us)) (scnj ((\<lambda>\<phi>. 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)) ` F)))
[PROOF STEP]
by (simp add: Let_def us[symmetric] vss)
[PROOF STATE]
proof (state)
this:
prv (eqv (psubst (scnj F) txs) (scnj ((\<lambda>\<phi>. psubst \<phi> txs) ` F)))

goal:
No subgoals!
[PROOF STEP]
qed