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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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