# Theory Renaming

```section‹Renaming of variables in internalized formulas›

theory Renaming
imports
"ZF-Constructible.Formula"
ZF_Miscellanea
begin

subsection‹Renaming of free variables›

definition
union_fun :: "[i,i,i,i] ⇒ i" where
"union_fun(f,g,m,p) ≡ λj ∈ m ∪ p  . if j∈m then f`j else g`j"

lemma union_fun_type:
assumes "f ∈ m → n"
"g ∈ p → q"
shows "union_fun(f,g,m,p) ∈ m ∪ p → n ∪ q"
proof -
let ?h="union_fun(f,g,m,p)"
have
D: "?h`x ∈ n ∪ q" if "x ∈ m ∪ p" for x
proof (cases "x ∈ m")
case True
then have
"x ∈ m ∪ p" by simp
with ‹x∈m›
have "?h`x = f`x"
unfolding union_fun_def  beta by simp
with ‹f ∈ m → n› ‹x∈m›
have "?h`x ∈ n" by simp
then show ?thesis ..
next
case False
with ‹x ∈ m ∪ p›
have "x ∈ p"
by auto
with ‹x∉m›
have "?h`x = g`x"
unfolding union_fun_def using beta by simp
with ‹g ∈ p → q› ‹x∈p›
have "?h`x ∈ q" by simp
then show ?thesis ..
qed
have A:"function(?h)" unfolding union_fun_def using function_lam by simp
have " x∈ (m ∪ p) × (n ∪ q)" if "x∈ ?h" for x
using that lamE[of x "m ∪ p" _ "x ∈ (m ∪ p) × (n ∪ q)"] D unfolding union_fun_def
by auto
then have B:"?h ⊆ (m ∪ p) × (n ∪ q)" ..
have "m ∪ p ⊆ domain(?h)"
unfolding union_fun_def using domain_lam by simp
with A B
show ?thesis using  Pi_iff [THEN iffD2] by simp
qed

lemma union_fun_action :
assumes
"env ∈ list(M)"
"env' ∈ list(M)"
"length(env) = m ∪ p"
"∀ i . i ∈ m ⟶  nth(f`i,env') = nth(i,env)"
"∀ j . j ∈ p ⟶ nth(g`j,env') = nth(j,env)"
shows "∀ i . i ∈ m ∪ p ⟶
nth(i,env) = nth(union_fun(f,g,m,p)`i,env')"
proof -
let ?h = "union_fun(f,g,m,p)"
have "nth(x, env) = nth(?h`x,env')" if "x ∈ m ∪ p" for x
using that
proof (cases "x∈m")
case True
with ‹x∈m›
have "?h`x = f`x"
unfolding union_fun_def  beta by simp
with assms ‹x∈m›
have "nth(x,env) = nth(?h`x,env')" by simp
then show ?thesis .
next
case False
with ‹x ∈ m ∪ p›
have
"x ∈ p" "x∉m"  by auto
then
have "?h`x = g`x"
unfolding union_fun_def beta by simp
with assms ‹x∈p›
have "nth(x,env) = nth(?h`x,env')" by simp
then show ?thesis .
qed
then show ?thesis by simp
qed

lemma id_fn_type :
assumes "n ∈ nat"
shows "id(n) ∈ n → n"
unfolding id_def using ‹n∈nat› by simp

lemma id_fn_action:
assumes "n ∈ nat" "env∈list(M)"
shows "⋀ j . j < n ⟹ nth(j,env) = nth(id(n)`j,env)"
proof -
show "nth(j,env) = nth(id(n)`j,env)" if "j < n" for j using that ‹n∈nat› ltD by simp
qed

definition
rsum :: "[i,i,i,i,i] ⇒ i" where
"rsum(f,g,m,n,p) ≡ λj ∈ m+⇩ωp  . if j<m then f`j else (g`(j#-m))+⇩ωn"

lemma sum_inl:
assumes "m ∈ nat" "n∈nat"
"f ∈ m→n" "x ∈ m"
shows "rsum(f,g,m,n,p)`x = f`x"
proof -
from ‹m∈nat›
have "m≤m+⇩ωp"
with assms
have "x∈m+⇩ωp"
using ltI[of x m] lt_trans2[of x m "m+⇩ωp"] ltD by simp
from assms
have "x<m"
using ltI by simp
with ‹x∈m+⇩ωp›
show ?thesis unfolding rsum_def by simp
qed

lemma sum_inr:
assumes "m ∈ nat" "n∈nat" "p∈nat"
"g∈p→q" "m ≤ x" "x < m+⇩ωp"
shows "rsum(f,g,m,n,p)`x = g`(x#-m)+⇩ωn"
proof -
from assms
have "x∈nat"
using in_n_in_nat[of "m+⇩ωp"] ltD
by simp
with assms
have "¬ x<m"
using not_lt_iff_le[THEN iffD2] by simp
from assms
have "x∈m+⇩ωp"
using ltD by simp
with ‹¬ x<m›
show ?thesis unfolding rsum_def by simp
qed

lemma sum_action :
assumes "m ∈ nat" "n∈nat" "p∈nat" "q∈nat"
"f ∈ m→n" "g∈p→q"
"env ∈ list(M)"
"env' ∈ list(M)"
"env1 ∈ list(M)"
"env2 ∈ list(M)"
"length(env) = m"
"length(env1) = p"
"length(env') = n"
"⋀ i . i < m ⟹ nth(i,env) = nth(f`i,env')"
"⋀ j. j < p ⟹ nth(j,env1) = nth(g`j,env2)"
shows "∀ i . i < m+⇩ωp ⟶
nth(i,env@env1) = nth(rsum(f,g,m,n,p)`i,env'@env2)"
proof -
let ?h = "rsum(f,g,m,n,p)"
from ‹m∈nat› ‹n∈nat› ‹q∈nat›
have "m≤m+⇩ωp" "n≤n+⇩ωq" "q≤n+⇩ωq"
from ‹p∈nat›
have "p = (m+⇩ωp)#-m" using diff_add_inverse2 by simp
have "nth(x, env @ env1) = nth(?h`x,env'@env2)" if "x<m+⇩ωp" for x
proof (cases "x<m")
case True
then
have 2: "?h`x= f`x" "x∈m" "f`x ∈ n" "x∈nat"
using assms sum_inl ltD apply_type[of f m _ x] in_n_in_nat by simp_all
with ‹x<m› assms
have "f`x < n" "f`x<length(env')"  "f`x∈nat"
using ltI in_n_in_nat by simp_all
with 2 ‹x<m› assms
have "nth(x,env@env1) = nth(x,env)"
using nth_append[OF ‹env∈list(M)›] ‹x∈nat› by simp
also
have
"... = nth(f`x,env')"
using 2 ‹x<m› assms by simp
also
have "... = nth(f`x,env'@env2)"
using nth_append[OF ‹env'∈list(M)›] ‹f`x<length(env')› ‹f`x ∈nat› by simp
also
have "... = nth(?h`x,env'@env2)"
using 2 by simp
finally
have "nth(x, env @ env1) = nth(?h`x,env'@env2)" .
then show ?thesis .
next
case False
have "x∈nat"
using that in_n_in_nat[of "m+⇩ωp" x] ltD ‹p∈nat› ‹m∈nat› by simp
with ‹length(env) = m›
have "m≤x" "length(env) ≤ x"
using not_lt_iff_le ‹m∈nat› ‹¬x<m› by simp_all
with ‹¬x<m› ‹length(env) = m›
have 2 : "?h`x= g`(x#-m)+⇩ωn"  "¬ x <length(env)"
unfolding rsum_def
using  sum_inr that beta ltD by simp_all
from assms ‹x∈nat› ‹p=m+⇩ωp#-m›
have "x#-m < p"
using diff_mono[OF _ _ _ ‹x<m+⇩ωp› ‹m≤x›] by simp
then have "x#-m∈p" using ltD by simp
with ‹g∈p→q›
have "g`(x#-m) ∈ q"  by simp
with ‹q∈nat› ‹length(env') = n›
have "g`(x#-m) < q" "g`(x#-m)∈nat" using ltI in_n_in_nat by simp_all
with ‹q∈nat› ‹n∈nat›
have "(g`(x#-m))+⇩ωn <n+⇩ωq" "n ≤ g`(x#-m)+⇩ωn" "¬ g`(x#-m)+⇩ωn < length(env')"
using add_lt_mono1[of "g`(x#-m)" _ n,OF _ ‹q∈nat›]
by simp_all
from assms ‹¬ x < length(env)› ‹length(env) = m›
have "nth(x,env @ env1) = nth(x#-m,env1)"
using nth_append[OF ‹env∈list(M)› ‹x∈nat›] by simp
also
have "... = nth(g`(x#-m),env2)"
using assms ‹x#-m < p› by simp
also
have "... = nth((g`(x#-m)+⇩ωn)#-length(env'),env2)"
using  ‹length(env') = n›
by simp
also
have "... = nth((g`(x#-m)+⇩ωn),env'@env2)"
using  nth_append[OF ‹env'∈list(M)›] ‹n∈nat› ‹¬ g`(x#-m)+⇩ωn < length(env')›
by simp
also
have "... = nth(?h`x,env'@env2)"
using 2 by simp
finally
have "nth(x, env @ env1) = nth(?h`x,env'@env2)" .
then show ?thesis .
qed
then show ?thesis by simp
qed

lemma sum_type  :
assumes "m ∈ nat" "n∈nat" "p∈nat" "q∈nat"
"f ∈ m→n" "g∈p→q"
shows "rsum(f,g,m,n,p) ∈ (m+⇩ωp) → (n+⇩ωq)"
proof -
let ?h = "rsum(f,g,m,n,p)"
from ‹m∈nat› ‹n∈nat› ‹q∈nat›
have "m≤m+⇩ωp" "n≤n+⇩ωq" "q≤n+⇩ωq"
from ‹p∈nat›
have "p = (m+⇩ωp)#-m" using diff_add_inverse2 by simp
{fix x
assume 1: "x∈m+⇩ωp" "x<m"
with 1 have "?h`x= f`x" "x∈m"
using assms sum_inl ltD by simp_all
with ‹f∈m→n›
have "?h`x ∈ n" by simp
with ‹n∈nat› have "?h`x < n" using ltI by simp
with ‹n≤n+⇩ωq›
have "?h`x < n+⇩ωq" using lt_trans2 by simp
then
have "?h`x ∈ n+⇩ωq"  using ltD by simp
}
then have 1:"?h`x ∈ n+⇩ωq" if "x∈m+⇩ωp" "x<m" for x using that .
{fix x
assume 1: "x∈m+⇩ωp" "m≤x"
then have "x<m+⇩ωp" "x∈nat" using ltI in_n_in_nat[of "m+⇩ωp"] ltD by simp_all
with 1
have 2 : "?h`x= g`(x#-m)+⇩ωn"
using assms sum_inr ltD by simp_all
from assms ‹x∈nat› ‹p=m+⇩ωp#-m›
have "x#-m < p" using diff_mono[OF _ _ _ ‹x<m+⇩ωp› ‹m≤x›] by simp
then have "x#-m∈p" using ltD by simp
with ‹g∈p→q›
have "g`(x#-m) ∈ q"  by simp
with ‹q∈nat› have "g`(x#-m) < q" using ltI by simp
with ‹q∈nat›
have "(g`(x#-m))+⇩ωn <n+⇩ωq" using add_lt_mono1[of "g`(x#-m)" _ n,OF _ ‹q∈nat›] by simp
with 2
have "?h`x ∈ n+⇩ωq"  using ltD by simp
}
then have 2:"?h`x ∈ n+⇩ωq" if "x∈m+⇩ωp" "m≤x" for x using that .
have
D: "?h`x ∈ n+⇩ωq" if "x∈m+⇩ωp" for x
using that
proof (cases "x<m")
case True
then show ?thesis using 1 that by simp
next
case False
with ‹m∈nat› have "m≤x" using not_lt_iff_le that in_n_in_nat[of "m+⇩ωp"] by simp
then show ?thesis using 2 that by simp
qed
have A:"function(?h)" unfolding rsum_def using function_lam by simp
have " x∈ (m +⇩ω p) × (n +⇩ω q)" if "x∈ ?h" for x
using that lamE[of x "m+⇩ωp" _ "x ∈ (m +⇩ω p) × (n +⇩ω q)"] D unfolding rsum_def
by auto
then have B:"?h ⊆ (m +⇩ω p) × (n +⇩ω q)" ..
have "m +⇩ω p ⊆ domain(?h)"
unfolding rsum_def using domain_lam by simp
with A B
show ?thesis using  Pi_iff [THEN iffD2] by simp
qed

lemma sum_type_id :
assumes
"f ∈ length(env)→length(env')"
"env ∈ list(M)"
"env' ∈ list(M)"
"env1 ∈ list(M)"
shows
"rsum(f,id(length(env1)),length(env),length(env'),length(env1)) ∈
(length(env)+⇩ωlength(env1)) → (length(env')+⇩ωlength(env1))"
using assms length_type id_fn_type sum_type
by simp

lemma sum_type_id_aux2 :
assumes
"f ∈ m→n"
"m ∈ nat" "n ∈ nat"
"env1 ∈ list(M)"
shows
"rsum(f,id(length(env1)),m,n,length(env1)) ∈
(m+⇩ωlength(env1)) → (n+⇩ωlength(env1))"
using assms id_fn_type sum_type
by auto

lemma sum_action_id :
assumes
"env ∈ list(M)"
"env' ∈ list(M)"
"f ∈ length(env)→length(env')"
"env1 ∈ list(M)"
"⋀ i . i < length(env) ⟹ nth(i,env) = nth(f`i,env')"
shows "⋀ i . i < length(env)+⇩ωlength(env1) ⟹
nth(i,env@env1) = nth(rsum(f,id(length(env1)),length(env),length(env'),length(env1))`i,env'@env1)"
proof -
from assms
have "length(env)∈nat" (is "?m ∈ _") by simp
from assms have "length(env')∈nat" (is "?n ∈ _") by simp
from assms have "length(env1)∈nat" (is "?p ∈ _") by simp
note lenv = id_fn_action[OF ‹?p∈nat› ‹env1∈list(M)›]
note lenv_ty = id_fn_type[OF ‹?p∈nat›]
{
fix i
assume "i < length(env)+⇩ωlength(env1)"
have "nth(i,env@env1) = nth(rsum(f,id(length(env1)),?m,?n,?p)`i,env'@env1)"
using sum_action[OF ‹?m∈nat› ‹?n∈nat› ‹?p∈nat› ‹?p∈nat› ‹f∈?m→?n›
lenv_ty ‹env∈list(M)› ‹env'∈list(M)›
‹env1∈list(M)› ‹env1∈list(M)› _
_ _  assms(5) lenv
] ‹i<?m+⇩ωlength(env1)› by simp
}
then show "⋀ i . i < ?m+⇩ωlength(env1) ⟹
nth(i,env@env1) = nth(rsum(f,id(?p),?m,?n,?p)`i,env'@env1)" by simp
qed

lemma sum_action_id_aux :
assumes
"f ∈ m→n"
"env ∈ list(M)"
"env' ∈ list(M)"
"env1 ∈ list(M)"
"length(env) = m"
"length(env') = n"
"length(env1) = p"
"⋀ i . i < m ⟹ nth(i,env) = nth(f`i,env')"
shows "⋀ i . i < m+⇩ωlength(env1) ⟹
nth(i,env@env1) = nth(rsum(f,id(length(env1)),m,n,length(env1))`i,env'@env1)"
using assms length_type id_fn_type sum_action_id
by auto

definition
sum_id :: "[i,i] ⇒ i" where
"sum_id(m,f) ≡ rsum(λx∈1.x,f,1,1,m)"

lemma sum_id0 : "m∈nat⟹sum_id(m,f)`0 = 0"
by(unfold sum_id_def,subst sum_inl,auto)

lemma sum_idS : "p∈nat ⟹ q∈nat ⟹ f∈p→q ⟹ x ∈ p ⟹ sum_id(p,f)`(succ(x)) = succ(f`x)"
by(subgoal_tac "x∈nat",unfold sum_id_def,subst sum_inr,

lemma sum_id_tc_aux :
"p ∈ nat ⟹  q ∈ nat ⟹ f ∈ p → q ⟹ sum_id(p,f) ∈ 1+⇩ωp → 1+⇩ωq"
by (unfold sum_id_def,rule sum_type,simp_all)

lemma sum_id_tc :
"n ∈ nat ⟹ m ∈ nat ⟹ f ∈ n → m ⟹ sum_id(n,f) ∈ succ(n) → succ(m)"
by(rule ssubst[of  "succ(n) → succ(m)" "1+⇩ωn → 1+⇩ωm"],
simp,rule sum_id_tc_aux,simp_all)

subsection‹Renaming of formulas›

consts   ren :: "i⇒i"
primrec
"ren(Member(x,y)) =
(λ n ∈ nat . λ m ∈ nat. λf ∈ n → m. Member (f`x, f`y))"

"ren(Equal(x,y)) =
(λ n ∈ nat . λ m ∈ nat. λf ∈ n → m. Equal (f`x, f`y))"

"ren(Nand(p,q)) =
(λ n ∈ nat . λ m ∈ nat. λf ∈ n → m. Nand (ren(p)`n`m`f, ren(q)`n`m`f))"

"ren(Forall(p)) =
(λ n ∈ nat . λ m ∈ nat. λf ∈ n → m. Forall (ren(p)`succ(n)`succ(m)`sum_id(n,f)))"

lemma arity_meml : "l ∈ nat ⟹ Member(x,y) ∈ formula ⟹ arity(Member(x,y)) ≤ l ⟹ x ∈ l"
by(simp,rule subsetD,rule le_imp_subset,assumption,simp)
lemma arity_memr : "l ∈ nat ⟹ Member(x,y) ∈ formula ⟹ arity(Member(x,y)) ≤ l ⟹ y ∈ l"
by(simp,rule subsetD,rule le_imp_subset,assumption,simp)
lemma arity_eql : "l ∈ nat ⟹ Equal(x,y) ∈ formula ⟹ arity(Equal(x,y)) ≤ l ⟹ x ∈ l"
by(simp,rule subsetD,rule le_imp_subset,assumption,simp)
lemma arity_eqr : "l ∈ nat ⟹ Equal(x,y) ∈ formula ⟹ arity(Equal(x,y)) ≤ l ⟹ y ∈ l"
by(simp,rule subsetD,rule le_imp_subset,assumption,simp)
lemma  nand_ar1 : "p ∈ formula ⟹ q∈formula ⟹arity(p) ≤ arity(Nand(p,q))"
by (simp,rule Un_upper1_le,simp+)
lemma nand_ar2 : "p ∈ formula ⟹ q∈formula ⟹arity(q) ≤ arity(Nand(p,q))"
by (simp,rule Un_upper2_le,simp+)

lemma nand_ar1D : "p ∈ formula ⟹ q∈formula ⟹ arity(Nand(p,q)) ≤ n ⟹ arity(p) ≤ n"
by(auto simp add:  le_trans[OF Un_upper1_le[of "arity(p)" "arity(q)"]])
lemma nand_ar2D : "p ∈ formula ⟹ q∈formula ⟹ arity(Nand(p,q)) ≤ n ⟹ arity(q) ≤ n"
by(auto simp add:  le_trans[OF Un_upper2_le[of "arity(p)" "arity(q)"]])

lemma ren_tc : "p ∈ formula ⟹
(⋀ n m f . n ∈ nat ⟹ m ∈ nat ⟹ f ∈ n→m ⟹  ren(p)`n`m`f ∈ formula)"
by (induct set:formula,auto simp add: app_nm sum_id_tc)

lemma arity_ren :
fixes "p"
assumes "p ∈ formula"
shows "⋀ n m f . n ∈ nat ⟹ m ∈ nat ⟹ f ∈ n→m ⟹ arity(p) ≤ n ⟹ arity(ren(p)`n`m`f)≤m"
using assms
proof (induct set:formula)
case (Member x y)
then have "f`x ∈ m" "f`y ∈ m"
then show ?case using Member by (simp add: Un_least_lt ltI)
next
case (Equal x y)
then have "f`x ∈ m" "f`y ∈ m"
then show ?case using Equal by (simp add: Un_least_lt ltI)
next
case (Nand p q)
then have "arity(p)≤arity(Nand(p,q))"
"arity(q)≤arity(Nand(p,q))"
by (subst  nand_ar1,simp,simp,simp,subst nand_ar2,simp+)
then have "arity(p)≤n"
and "arity(q)≤n" using Nand
by (rule_tac j="arity(Nand(p,q))" in le_trans,simp,simp)+
then have "arity(ren(p)`n`m`f) ≤ m" and  "arity(ren(q)`n`m`f) ≤ m"
using Nand by auto
then show ?case using Nand by (simp add:Un_least_lt)
next
case (Forall p)
from Forall have "succ(n)∈nat"  "succ(m)∈nat" by auto
from Forall have 2: "sum_id(n,f) ∈ succ(n)→succ(m)" by (simp add:sum_id_tc)
from Forall have 3:"arity(p) ≤ succ(n)" by (rule_tac n="arity(p)" in natE,simp+)
then have "arity(ren(p)`succ(n)`succ(m)`sum_id(n,f))≤succ(m)" using
Forall ‹succ(n)∈nat› ‹succ(m)∈nat› 2 by force
then show ?case using Forall 2 3 ren_tc arity_type pred_le by auto
qed

lemma arity_forallE : "p ∈ formula ⟹ m ∈ nat ⟹ arity(Forall(p)) ≤ m ⟹ arity(p) ≤ succ(m)"
by(rule_tac n="arity(p)" in natE,erule arity_type,simp+)

lemma env_coincidence_sum_id :
assumes "m ∈ nat" "n ∈ nat"
"ρ ∈ list(A)" "ρ' ∈ list(A)"
"f ∈ n → m"
"⋀ i . i < n ⟹ nth(i,ρ) = nth(f`i,ρ')"
"a ∈ A" "j ∈ succ(n)"
shows "nth(j,Cons(a,ρ)) = nth(sum_id(n,f)`j,Cons(a,ρ'))"
proof -
let ?g="sum_id(n,f)"
have "succ(n) ∈ nat" using ‹n∈nat› by simp
then have "j ∈ nat" using ‹j∈succ(n)› in_n_in_nat by blast
then have "nth(j,Cons(a,ρ)) = nth(?g`j,Cons(a,ρ'))"
proof (cases rule:natE[OF ‹j∈nat›])
case 1
then show ?thesis using assms sum_id0 by simp
next
case (2 i)
with ‹j∈succ(n)› have "succ(i)∈succ(n)" by simp
with ‹n∈nat› have "i ∈ n" using nat_succD assms by simp
have "f`i∈m" using ‹f∈n→m› apply_type ‹i∈n› by simp
then have "f`i ∈ nat" using in_n_in_nat ‹m∈nat› by simp
have "nth(succ(i),Cons(a,ρ)) = nth(i,ρ)" using ‹i∈nat› by simp
also have "... = nth(f`i,ρ')" using assms ‹i∈n› ltI by simp
also have "... = nth(succ(f`i),Cons(a,ρ'))" using ‹f`i∈nat› by simp
also have "... = nth(?g`succ(i),Cons(a,ρ'))"
using assms sum_idS[OF ‹n∈nat› ‹m∈nat›  ‹f∈n→m› ‹i ∈ n›] cases by simp
finally have "nth(succ(i),Cons(a,ρ)) = nth(?g`succ(i),Cons(a,ρ'))" .
then show ?thesis using ‹j=succ(i)› by simp
qed
then show ?thesis .
qed

lemma sats_iff_sats_ren :
assumes "φ ∈ formula"
shows  "⟦  n ∈ nat ; m ∈ nat ; ρ ∈ list(M) ; ρ' ∈ list(M) ; f ∈ n → m ;
arity(φ) ≤ n ;
⋀ i . i < n ⟹ nth(i,ρ) = nth(f`i,ρ') ⟧ ⟹
sats(M,φ,ρ) ⟷ sats(M,ren(φ)`n`m`f,ρ')"
using ‹φ ∈ formula›
proof(induct φ arbitrary:n m ρ ρ' f)
case (Member x y)
have "ren(Member(x,y))`n`m`f = Member(f`x,f`y)" using Member assms arity_type by force
moreover
have "x ∈ n" using Member arity_meml by simp
moreover
have "y ∈ n" using Member arity_memr by simp
ultimately
show ?case using Member ltI by simp
next
case (Equal x y)
have "ren(Equal(x,y))`n`m`f = Equal(f`x,f`y)" using Equal assms arity_type by force
moreover
have "x ∈ n" using Equal arity_eql by simp
moreover
have "y ∈ n" using Equal arity_eqr by simp
ultimately show ?case using Equal ltI by simp
next
case (Nand p q)
have "ren(Nand(p,q))`n`m`f = Nand(ren(p)`n`m`f,ren(q)`n`m`f)" using Nand by simp
moreover
have "arity(p) ≤ n" using Nand nand_ar1D by simp
moreover from this
have "i ∈ arity(p) ⟹ i ∈ n" for i using subsetD[OF le_imp_subset[OF ‹arity(p) ≤ n›]] by simp
moreover from this
have "i ∈ arity(p) ⟹ nth(i,ρ) = nth(f`i,ρ')" for i using Nand ltI by simp
moreover from this
have "sats(M,p,ρ) ⟷ sats(M,ren(p)`n`m`f,ρ')" using ‹arity(p)≤n› Nand by simp
have "arity(q) ≤ n" using Nand nand_ar2D by simp
moreover from this
have "i ∈ arity(q) ⟹ i ∈ n" for i using subsetD[OF le_imp_subset[OF ‹arity(q) ≤ n›]] by simp
moreover from this
have "i ∈ arity(q) ⟹ nth(i,ρ) = nth(f`i,ρ')" for i using Nand ltI by simp
moreover from this
have "sats(M,q,ρ) ⟷ sats(M,ren(q)`n`m`f,ρ')" using assms ‹arity(q)≤n› Nand by simp
ultimately
show ?case using Nand by simp
next
case (Forall p)
have 0:"ren(Forall(p))`n`m`f = Forall(ren(p)`succ(n)`succ(m)`sum_id(n,f))"
using Forall by simp
have 1:"sum_id(n,f) ∈ succ(n) → succ(m)" (is "?g ∈ _") using sum_id_tc Forall by simp
then have 2: "arity(p) ≤ succ(n)"
using Forall le_trans[of _ "succ(pred(arity(p)))"] succpred_leI by simp
have "succ(n)∈nat" "succ(m)∈nat" using Forall by auto
then have A:"⋀ j .j < succ(n) ⟹ nth(j, Cons(a, ρ)) = nth(?g`j, Cons(a, ρ'))" if "a∈M" for a
using that env_coincidence_sum_id Forall ltD by force
have
"sats(M,p,Cons(a,ρ)) ⟷ sats(M,ren(p)`succ(n)`succ(m)`?g,Cons(a,ρ'))" if "a∈M" for a
proof -
have C:"Cons(a,ρ) ∈ list(M)" "Cons(a,ρ')∈list(M)" using Forall that by auto
have "sats(M,p,Cons(a,ρ)) ⟷ sats(M,ren(p)`succ(n)`succ(m)`?g,Cons(a,ρ'))"
using Forall(2)[OF ‹succ(n)∈nat› ‹succ(m)∈nat› C(1) C(2) 1 2 A[OF ‹a∈M›]] by simp
then show ?thesis .
qed
then show ?case using Forall 0 1 2 by simp
qed

end```