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

goal (1 subgoal):
 1. psubst (cnj \<phi>1 \<phi>2) txs = cnj (psubst \<phi>1 txs) (psubst \<phi>2 txs)
[PROOF STEP]
have us_facts: "set us \<subseteq> var"
    "set us \<inter> Fvars \<phi>1 = {}"
    "set us \<inter> Fvars \<phi>2 = {}"
    "set us \<inter> \<Union> (FvarsT ` (fst ` (set txs))) = {}"
    "set us \<inter> snd ` (set txs) = {}"
    "length us = length txs"
    "distinct us"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (set us \<subseteq> var &&& set us \<inter> Fvars \<phi>1 = {} &&& set us \<inter> Fvars \<phi>2 = {}) &&& (set us \<inter> \<Union> (FvarsT ` fst ` set txs) = {} &&& set us \<inter> snd ` set txs = {}) &&& length us = length txs &&& distinct us
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<phi>1 \<in> fmla
\<phi>2 \<in> fmla
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> Fvars \<phi>1 = {} &&& set us \<inter> Fvars \<phi>2 = {}) &&& (set us \<inter> \<Union> (FvarsT ` fst ` set txs) = {} &&& set us \<inter> snd ` set txs = {}) &&& length us = length txs &&& distinct us
[PROOF STEP]
unfolding us
[PROOF STATE]
proof (prove)
using this:
\<phi>1 \<in> fmla
\<phi>2 \<in> fmla
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) [cnj \<phi>1 \<phi>2] (length txs)) \<subseteq> var &&& set (getFrN (map snd txs) (map fst txs) [cnj \<phi>1 \<phi>2] (length txs)) \<inter> Fvars \<phi>1 = {} &&& set (getFrN (map snd txs) (map fst txs) [cnj \<phi>1 \<phi>2] (length txs)) \<inter> Fvars \<phi>2 = {}) &&& (set (getFrN (map snd txs) (map fst txs) [cnj \<phi>1 \<phi>2] (length txs)) \<inter> \<Union> (FvarsT ` fst ` set txs) = {} &&& set (getFrN (map snd txs) (map fst txs) [cnj \<phi>1 \<phi>2] (length txs)) \<inter> snd ` set txs = {}) &&& length (getFrN (map snd txs) (map fst txs) [cnj \<phi>1 \<phi>2] (length txs)) = length txs &&& distinct (getFrN (map snd txs) (map fst txs) [cnj \<phi>1 \<phi>2] (length txs))
[PROOF STEP]
using getFrN_Fvars[of "map snd txs" "map fst txs" "[cnj \<phi>1 \<phi>2]" _ "length txs"]
      getFrN_FvarsT[of "map snd txs" "map fst txs" "[cnj \<phi>1 \<phi>2]" _ "length txs"]
      getFrN_var[of "map snd txs" "map fst txs" "[cnj \<phi>1 \<phi>2]" _ "length txs"]
      getFrN_length[of "map snd txs" "map fst txs" "[cnj \<phi>1 \<phi>2]" "length txs"]
[PROOF STATE]
proof (prove)
using this:
\<phi>1 \<in> fmla
\<phi>2 \<in> fmla
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 [cnj \<phi>1 \<phi>2] \<subseteq> fmla; ?\<phi> \<in> set [cnj \<phi>1 \<phi>2]\<rbrakk> \<Longrightarrow> set (getFrN (map snd txs) (map fst txs) [cnj \<phi>1 \<phi>2] (length txs)) \<inter> Fvars ?\<phi> = {}
\<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [cnj \<phi>1 \<phi>2] \<subseteq> fmla; ?t \<in> set (map fst txs)\<rbrakk> \<Longrightarrow> set (getFrN (map snd txs) (map fst txs) [cnj \<phi>1 \<phi>2] (length txs)) \<inter> FvarsT ?t = {}
\<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [cnj \<phi>1 \<phi>2] \<subseteq> fmla; ?t \<in> set (map fst txs)\<rbrakk> \<Longrightarrow> set (getFrN (map snd txs) (map fst txs) [cnj \<phi>1 \<phi>2] (length txs)) \<inter> set (map snd txs) = {}
\<lbrakk>set (map snd txs) \<subseteq> var; set (map fst txs) \<subseteq> trm; set [cnj \<phi>1 \<phi>2] \<subseteq> fmla\<rbrakk> \<Longrightarrow> length (getFrN (map snd txs) (map fst txs) [cnj \<phi>1 \<phi>2] (length txs)) = length txs

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

goal (1 subgoal):
 1. psubst (cnj \<phi>1 \<phi>2) txs = cnj (psubst \<phi>1 txs) (psubst \<phi>2 txs)
[PROOF STEP]
define vs1 where vs1: "vs1 = getFrN (map snd txs) (map fst txs) [\<phi>1] (length txs)"
[PROOF STATE]
proof (state)
this:
vs1 = getFrN (map snd txs) (map fst txs) [\<phi>1] (length txs)

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

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

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

goal (1 subgoal):
 1. psubst (cnj \<phi>1 \<phi>2) txs = cnj (psubst \<phi>1 txs) (psubst \<phi>2 txs)
[PROOF STEP]
define vs2 where vs2: "vs2 = getFrN (map snd txs) (map fst txs) [\<phi>2] (length txs)"
[PROOF STATE]
proof (state)
this:
vs2 = getFrN (map snd txs) (map fst txs) [\<phi>2] (length txs)

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

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

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

goal (1 subgoal):
 1. psubst (cnj \<phi>1 \<phi>2) txs = cnj (psubst \<phi>1 txs) (psubst \<phi>2 txs)
[PROOF STEP]
let ?tus = "zip (map fst txs) us"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. psubst (cnj \<phi>1 \<phi>2) txs = cnj (psubst \<phi>1 txs) (psubst \<phi>2 txs)
[PROOF STEP]
let ?uxs = "zip (map Var us) (map snd txs)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. psubst (cnj \<phi>1 \<phi>2) txs = cnj (psubst \<phi>1 txs) (psubst \<phi>2 txs)
[PROOF STEP]
let ?tvs1 = "zip (map fst txs) vs1"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. psubst (cnj \<phi>1 \<phi>2) txs = cnj (psubst \<phi>1 txs) (psubst \<phi>2 txs)
[PROOF STEP]
let ?vxs1 = "zip (map Var vs1) (map snd txs)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. psubst (cnj \<phi>1 \<phi>2) txs = cnj (psubst \<phi>1 txs) (psubst \<phi>2 txs)
[PROOF STEP]
let ?tvs2 = "zip (map fst txs) vs2"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. psubst (cnj \<phi>1 \<phi>2) txs = cnj (psubst \<phi>1 txs) (psubst \<phi>2 txs)
[PROOF STEP]
let ?vxs2 = "zip (map Var vs2) (map snd txs)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. psubst (cnj \<phi>1 \<phi>2) txs = cnj (psubst \<phi>1 txs) (psubst \<phi>2 txs)
[PROOF STEP]
let ?c = "rawpsubst (cnj \<phi>1 \<phi>2) ?uxs"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. psubst (cnj \<phi>1 \<phi>2) txs = cnj (psubst \<phi>1 txs) (psubst \<phi>2 txs)
[PROOF STEP]
have c: "?c = cnj (rawpsubst \<phi>1 ?uxs) (rawpsubst \<phi>2 ?uxs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rawpsubst (cnj \<phi>1 \<phi>2) (zip (map Var us) (map snd txs)) = cnj (rawpsubst \<phi>1 (zip (map Var us) (map snd txs))) (rawpsubst \<phi>2 (zip (map Var us) (map snd txs)))
[PROOF STEP]
using assms us_facts
[PROOF STATE]
proof (prove)
using this:
\<phi>1 \<in> fmla
\<phi>2 \<in> fmla
snd ` set txs \<subseteq> var
fst ` set txs \<subseteq> trm
distinct (map snd txs)
set us \<subseteq> var
set us \<inter> Fvars \<phi>1 = {}
set us \<inter> Fvars \<phi>2 = {}
set us \<inter> \<Union> (FvarsT ` fst ` set txs) = {}
set us \<inter> snd ` set txs = {}
length us = length txs
distinct us

goal (1 subgoal):
 1. rawpsubst (cnj \<phi>1 \<phi>2) (zip (map Var us) (map snd txs)) = cnj (rawpsubst \<phi>1 (zip (map Var us) (map snd txs))) (rawpsubst \<phi>2 (zip (map Var us) (map snd txs)))
[PROOF STEP]
by (intro rawpsubst_cnj) (auto intro!: rawpsubstT dest!: set_zip_D)
[PROOF STATE]
proof (state)
this:
rawpsubst (cnj \<phi>1 \<phi>2) (zip (map Var us) (map snd txs)) = cnj (rawpsubst \<phi>1 (zip (map Var us) (map snd txs))) (rawpsubst \<phi>2 (zip (map Var us) (map snd txs)))

goal (1 subgoal):
 1. psubst (cnj \<phi>1 \<phi>2) txs = cnj (psubst \<phi>1 txs) (psubst \<phi>2 txs)
[PROOF STEP]
have 0: "rawpsubst ?c ?tus =
    cnj (rawpsubst (rawpsubst \<phi>1 ?uxs) ?tus) (rawpsubst (rawpsubst \<phi>2 ?uxs) ?tus)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rawpsubst (rawpsubst (cnj \<phi>1 \<phi>2) (zip (map Var us) (map snd txs))) (zip (map fst txs) us) = cnj (rawpsubst (rawpsubst \<phi>1 (zip (map Var us) (map snd txs))) (zip (map fst txs) us)) (rawpsubst (rawpsubst \<phi>2 (zip (map Var us) (map snd txs))) (zip (map fst txs) us))
[PROOF STEP]
unfolding c
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rawpsubst (cnj (rawpsubst \<phi>1 (zip (map Var us) (map snd txs))) (rawpsubst \<phi>2 (zip (map Var us) (map snd txs)))) (zip (map fst txs) us) = cnj (rawpsubst (rawpsubst \<phi>1 (zip (map Var us) (map snd txs))) (zip (map fst txs) us)) (rawpsubst (rawpsubst \<phi>2 (zip (map Var us) (map snd txs))) (zip (map fst txs) us))
[PROOF STEP]
using assms us_facts
[PROOF STATE]
proof (prove)
using this:
\<phi>1 \<in> fmla
\<phi>2 \<in> fmla
snd ` set txs \<subseteq> var
fst ` set txs \<subseteq> trm
distinct (map snd txs)
set us \<subseteq> var
set us \<inter> Fvars \<phi>1 = {}
set us \<inter> Fvars \<phi>2 = {}
set us \<inter> \<Union> (FvarsT ` fst ` set txs) = {}
set us \<inter> snd ` set txs = {}
length us = length txs
distinct us

goal (1 subgoal):
 1. rawpsubst (cnj (rawpsubst \<phi>1 (zip (map Var us) (map snd txs))) (rawpsubst \<phi>2 (zip (map Var us) (map snd txs)))) (zip (map fst txs) us) = cnj (rawpsubst (rawpsubst \<phi>1 (zip (map Var us) (map snd txs))) (zip (map fst txs) us)) (rawpsubst (rawpsubst \<phi>2 (zip (map Var us) (map snd txs))) (zip (map fst txs) us))
[PROOF STEP]
by (intro rawpsubst_cnj) (auto dest!: set_zip_D intro!: rawpsubst)
[PROOF STATE]
proof (state)
this:
rawpsubst (rawpsubst (cnj \<phi>1 \<phi>2) (zip (map Var us) (map snd txs))) (zip (map fst txs) us) = cnj (rawpsubst (rawpsubst \<phi>1 (zip (map Var us) (map snd txs))) (zip (map fst txs) us)) (rawpsubst (rawpsubst \<phi>2 (zip (map Var us) (map snd txs))) (zip (map fst txs) us))

goal (1 subgoal):
 1. psubst (cnj \<phi>1 \<phi>2) txs = cnj (psubst \<phi>1 txs) (psubst \<phi>2 txs)
[PROOF STEP]
have 1: "rawpsubst (rawpsubst \<phi>1 ?uxs) ?tus = rawpsubst (rawpsubst \<phi>1 ?vxs1) ?tvs1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rawpsubst (rawpsubst \<phi>1 (zip (map Var us) (map snd txs))) (zip (map fst txs) us) = rawpsubst (rawpsubst \<phi>1 (zip (map Var vs1) (map snd txs))) (zip (map fst txs) vs1)
[PROOF STEP]
using assms vs1_facts us_facts
[PROOF STATE]
proof (prove)
using this:
\<phi>1 \<in> fmla
\<phi>2 \<in> fmla
snd ` set txs \<subseteq> var
fst ` set txs \<subseteq> trm
distinct (map snd txs)
set vs1 \<subseteq> var
set vs1 \<inter> Fvars \<phi>1 = {}
set vs1 \<inter> \<Union> (FvarsT ` fst ` set txs) = {}
set vs1 \<inter> snd ` set txs = {}
length vs1 = length txs
distinct vs1
set us \<subseteq> var
set us \<inter> Fvars \<phi>1 = {}
set us \<inter> Fvars \<phi>2 = {}
set us \<inter> \<Union> (FvarsT ` fst ` set txs) = {}
set us \<inter> snd ` set txs = {}
length us = length txs
distinct us

goal (1 subgoal):
 1. rawpsubst (rawpsubst \<phi>1 (zip (map Var us) (map snd txs))) (zip (map fst txs) us) = rawpsubst (rawpsubst \<phi>1 (zip (map Var vs1) (map snd txs))) (zip (map fst txs) vs1)
[PROOF STEP]
by (intro rawpsubst_compose_freshVar2) (auto intro!: rawpsubst)
[PROOF STATE]
proof (state)
this:
rawpsubst (rawpsubst \<phi>1 (zip (map Var us) (map snd txs))) (zip (map fst txs) us) = rawpsubst (rawpsubst \<phi>1 (zip (map Var vs1) (map snd txs))) (zip (map fst txs) vs1)

goal (1 subgoal):
 1. psubst (cnj \<phi>1 \<phi>2) txs = cnj (psubst \<phi>1 txs) (psubst \<phi>2 txs)
[PROOF STEP]
have 2: "rawpsubst (rawpsubst \<phi>2 ?uxs) ?tus = rawpsubst (rawpsubst \<phi>2 ?vxs2) ?tvs2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rawpsubst (rawpsubst \<phi>2 (zip (map Var us) (map snd txs))) (zip (map fst txs) us) = rawpsubst (rawpsubst \<phi>2 (zip (map Var vs2) (map snd txs))) (zip (map fst txs) vs2)
[PROOF STEP]
using assms vs2_facts us_facts
[PROOF STATE]
proof (prove)
using this:
\<phi>1 \<in> fmla
\<phi>2 \<in> fmla
snd ` set txs \<subseteq> var
fst ` set txs \<subseteq> trm
distinct (map snd txs)
set vs2 \<subseteq> var
set vs2 \<inter> Fvars \<phi>2 = {}
set vs2 \<inter> \<Union> (FvarsT ` fst ` set txs) = {}
set vs2 \<inter> snd ` set txs = {}
length vs2 = length txs
distinct vs2
set us \<subseteq> var
set us \<inter> Fvars \<phi>1 = {}
set us \<inter> Fvars \<phi>2 = {}
set us \<inter> \<Union> (FvarsT ` fst ` set txs) = {}
set us \<inter> snd ` set txs = {}
length us = length txs
distinct us

goal (1 subgoal):
 1. rawpsubst (rawpsubst \<phi>2 (zip (map Var us) (map snd txs))) (zip (map fst txs) us) = rawpsubst (rawpsubst \<phi>2 (zip (map Var vs2) (map snd txs))) (zip (map fst txs) vs2)
[PROOF STEP]
by (intro rawpsubst_compose_freshVar2)(auto intro!: rawpsubst)
[PROOF STATE]
proof (state)
this:
rawpsubst (rawpsubst \<phi>2 (zip (map Var us) (map snd txs))) (zip (map fst txs) us) = rawpsubst (rawpsubst \<phi>2 (zip (map Var vs2) (map snd txs))) (zip (map fst txs) vs2)

goal (1 subgoal):
 1. psubst (cnj \<phi>1 \<phi>2) txs = cnj (psubst \<phi>1 txs) (psubst \<phi>2 txs)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. psubst (cnj \<phi>1 \<phi>2) txs = cnj (psubst \<phi>1 txs) (psubst \<phi>2 txs)
[PROOF STEP]
unfolding psubst_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (let xs = map snd txs; ts = map fst txs; us = getFrN xs ts [cnj \<phi>1 \<phi>2] (length xs) in rawpsubst (rawpsubst (cnj \<phi>1 \<phi>2) (zip (map Var us) xs)) (zip ts us)) = cnj (let xs = map snd txs; ts = map fst txs; us = getFrN xs ts [\<phi>1] (length xs) in rawpsubst (rawpsubst \<phi>1 (zip (map Var us) xs)) (zip ts us)) (let xs = map snd txs; ts = map fst txs; us = getFrN xs ts [\<phi>2] (length xs) in rawpsubst (rawpsubst \<phi>2 (zip (map Var us) xs)) (zip ts us))
[PROOF STEP]
by (simp add: Let_def us[symmetric] vs1[symmetric] vs2[symmetric] 0 1 2)
[PROOF STATE]
proof (state)
this:
psubst (cnj \<phi>1 \<phi>2) txs = cnj (psubst \<phi>1 txs) (psubst \<phi>2 txs)

goal:
No subgoals!
[PROOF STEP]
qed