[STATEMENT]
lemma wf_rexp_of_alt: "wf_formula n \<phi> \<Longrightarrow> wf n (rexp_of_alt n \<phi>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf_formula n \<phi> \<Longrightarrow> local.wf n (rexp_of_alt n \<phi>)
[PROOF STEP]
by (induct \<phi> arbitrary: n)
    (auto intro!: wf_samequot_exec wf_rexp_ENC,
     auto simp: max_idx_vars finite_FOV)


[STATEMENT]
lemma wf_rexp_of': "wf_formula n \<phi> \<Longrightarrow> wf n (rexp_of' n \<phi>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf_formula n \<phi> \<Longrightarrow> local.wf n (rexp_of' n \<phi>)
[PROOF STEP]
unfolding rexp_of'_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf_formula n \<phi> \<Longrightarrow> local.wf n (rexp.Inter (rexp_of_alt n \<phi>) (ENC n (FOV \<phi>)))
[PROOF STEP]
by (auto simp: max_idx_vars intro: wf_rexp_of_alt wf_rexp_ENC[OF finite_FOV])


[STATEMENT]
lemma wf_rexp_of_alt': "wf_formula n \<phi> \<Longrightarrow> wf n (rexp_of_alt' n \<phi>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf_formula n \<phi> \<Longrightarrow> local.wf n (rexp_of_alt' n \<phi>)
[PROOF STEP]
by (induct \<phi> arbitrary: n)
    (auto intro!: wf_samequot_exec wf_rexp_ENC,
     auto simp: max_idx_vars finite_FOV)


[STATEMENT]
lemma wf_rexp_of'': "wf_formula n \<phi> \<Longrightarrow> wf n (rexp_of'' n \<phi>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf_formula n \<phi> \<Longrightarrow> local.wf n (rexp_of'' n \<phi>)
[PROOF STEP]
unfolding rexp_of''_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf_formula n \<phi> \<Longrightarrow> local.wf n (rexp.Inter (rexp_of_alt' n \<phi>) (ENC n (FOV \<phi>)))
[PROOF STEP]
by (auto simp: wf_rexp_ENC wf_rexp_of_alt' finite_FOV max_idx_vars)


[STATEMENT]
lemma ENC_FNot: "ENC n (FOV (FNot \<phi>)) = ENC n (FOV \<phi>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ENC n (FOV (FNot \<phi>)) = ENC n (FOV \<phi>)
[PROOF STEP]
unfolding ENC_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. INTERSECT (sorted_list_of_set (valid_ENC n ` FOV (FNot \<phi>))) = INTERSECT (sorted_list_of_set (valid_ENC n ` FOV \<phi>))
[PROOF STEP]
by auto


[STATEMENT]
lemma ENC_FAnd:
  "wf_formula n (FAnd \<phi> \<psi>) \<Longrightarrow> lang n (ENC n (FOV (FAnd \<phi> \<psi>))) \<subseteq> lang n (ENC n (FOV \<phi>)) \<inter> lang n (ENC n (FOV \<psi>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf_formula n (FAnd \<phi> \<psi>) \<Longrightarrow> lang n (ENC n (FOV (FAnd \<phi> \<psi>))) \<subseteq> lang n (ENC n (FOV \<phi>)) \<inter> lang n (ENC n (FOV \<psi>))
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>wf_formula n (FAnd \<phi> \<psi>); x \<in> lang n (ENC n (FOV (FAnd \<phi> \<psi>)))\<rbrakk> \<Longrightarrow> x \<in> lang n (ENC n (FOV \<phi>)) \<inter> lang n (ENC n (FOV \<psi>))
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>wf_formula n (FAnd \<phi> \<psi>); x \<in> lang n (ENC n (FOV (FAnd \<phi> \<psi>)))\<rbrakk> \<Longrightarrow> x \<in> lang n (ENC n (FOV \<phi>)) \<inter> lang n (ENC n (FOV \<psi>))
[PROOF STEP]
assume wf: "wf_formula n (FAnd \<phi> \<psi>)" and x: "x \<in> lang n (ENC n (FOV (FAnd \<phi> \<psi>)))"
[PROOF STATE]
proof (state)
this:
wf_formula n (FAnd \<phi> \<psi>)
x \<in> lang n (ENC n (FOV (FAnd \<phi> \<psi>)))

goal (1 subgoal):
 1. \<And>x. \<lbrakk>wf_formula n (FAnd \<phi> \<psi>); x \<in> lang n (ENC n (FOV (FAnd \<phi> \<psi>)))\<rbrakk> \<Longrightarrow> x \<in> lang n (ENC n (FOV \<phi>)) \<inter> lang n (ENC n (FOV \<psi>))
[PROOF STEP]
hence wf1: "wf_formula n \<phi>" and wf2: "wf_formula n \<psi>"
[PROOF STATE]
proof (prove)
using this:
wf_formula n (FAnd \<phi> \<psi>)
x \<in> lang n (ENC n (FOV (FAnd \<phi> \<psi>)))

goal (1 subgoal):
 1. wf_formula n \<phi> &&& wf_formula n \<psi>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
wf_formula n \<phi>
wf_formula n \<psi>

goal (1 subgoal):
 1. \<And>x. \<lbrakk>wf_formula n (FAnd \<phi> \<psi>); x \<in> lang n (ENC n (FOV (FAnd \<phi> \<psi>)))\<rbrakk> \<Longrightarrow> x \<in> lang n (ENC n (FOV \<phi>)) \<inter> lang n (ENC n (FOV \<psi>))
[PROOF STEP]
from x
[PROOF STATE]
proof (chain)
picking this:
x \<in> lang n (ENC n (FOV (FAnd \<phi> \<psi>)))
[PROOF STEP]
obtain w I where I: "x \<in> enc (w, I)" "wf_interp_for_formula (w, I) (FAnd \<phi> \<psi>)" "length I = n"
[PROOF STATE]
proof (prove)
using this:
x \<in> lang n (ENC n (FOV (FAnd \<phi> \<psi>)))

goal (1 subgoal):
 1. (\<And>w I. \<lbrakk>x \<in> enc (w, I); wf_interp_for_formula (w, I) (FAnd \<phi> \<psi>); length I = n\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using lang_ENC_formula[OF wf]
[PROOF STATE]
proof (prove)
using this:
x \<in> lang n (ENC n (FOV (FAnd \<phi> \<psi>)))
lang n (ENC n (FOV (FAnd \<phi> \<psi>))) = \<Union> {enc (w, I) |w I. length I = n \<and> wf_interp_for_formula (w, I) (FAnd \<phi> \<psi>)}

goal (1 subgoal):
 1. (\<And>w I. \<lbrakk>x \<in> enc (w, I); wf_interp_for_formula (w, I) (FAnd \<phi> \<psi>); length I = n\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<in> enc (w, I)
wf_interp_for_formula (w, I) (FAnd \<phi> \<psi>)
length I = n

goal (1 subgoal):
 1. \<And>x. \<lbrakk>wf_formula n (FAnd \<phi> \<psi>); x \<in> lang n (ENC n (FOV (FAnd \<phi> \<psi>)))\<rbrakk> \<Longrightarrow> x \<in> lang n (ENC n (FOV \<phi>)) \<inter> lang n (ENC n (FOV \<psi>))
[PROOF STEP]
hence "wf_interp_for_formula (w, I) \<phi>" "wf_interp_for_formula (w, I) \<psi>"
[PROOF STATE]
proof (prove)
using this:
x \<in> enc (w, I)
wf_interp_for_formula (w, I) (FAnd \<phi> \<psi>)
length I = n

goal (1 subgoal):
 1. wf_interp_for_formula (w, I) \<phi> &&& wf_interp_for_formula (w, I) \<psi>
[PROOF STEP]
using wf_interp_for_formula_FAnd
[PROOF STATE]
proof (prove)
using this:
x \<in> enc (w, I)
wf_interp_for_formula (w, I) (FAnd \<phi> \<psi>)
length I = n
wf_interp_for_formula (?w, ?I) (FAnd ?\<phi>1.0 ?\<phi>2.0) = (wf_interp_for_formula (?w, ?I) ?\<phi>1.0 \<and> wf_interp_for_formula (?w, ?I) ?\<phi>2.0)

goal (1 subgoal):
 1. wf_interp_for_formula (w, I) \<phi> &&& wf_interp_for_formula (w, I) \<psi>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
wf_interp_for_formula (w, I) \<phi>
wf_interp_for_formula (w, I) \<psi>

goal (1 subgoal):
 1. \<And>x. \<lbrakk>wf_formula n (FAnd \<phi> \<psi>); x \<in> lang n (ENC n (FOV (FAnd \<phi> \<psi>)))\<rbrakk> \<Longrightarrow> x \<in> lang n (ENC n (FOV \<phi>)) \<inter> lang n (ENC n (FOV \<psi>))
[PROOF STEP]
thus "x \<in> lang n (ENC n (FOV \<phi>)) \<inter> lang n (ENC n (FOV \<psi>))"
[PROOF STATE]
proof (prove)
using this:
wf_interp_for_formula (w, I) \<phi>
wf_interp_for_formula (w, I) \<psi>

goal (1 subgoal):
 1. x \<in> lang n (ENC n (FOV \<phi>)) \<inter> lang n (ENC n (FOV \<psi>))
[PROOF STEP]
unfolding lang_ENC_formula[OF wf1] lang_ENC_formula[OF wf2]
[PROOF STATE]
proof (prove)
using this:
wf_interp_for_formula (w, I) \<phi>
wf_interp_for_formula (w, I) \<psi>

goal (1 subgoal):
 1. x \<in> \<Union> {enc (w, I) |w I. length I = n \<and> wf_interp_for_formula (w, I) \<phi>} \<inter> \<Union> {enc (w, I) |w I. length I = n \<and> wf_interp_for_formula (w, I) \<psi>}
[PROOF STEP]
using I
[PROOF STATE]
proof (prove)
using this:
wf_interp_for_formula (w, I) \<phi>
wf_interp_for_formula (w, I) \<psi>
x \<in> enc (w, I)
wf_interp_for_formula (w, I) (FAnd \<phi> \<psi>)
length I = n

goal (1 subgoal):
 1. x \<in> \<Union> {enc (w, I) |w I. length I = n \<and> wf_interp_for_formula (w, I) \<phi>} \<inter> \<Union> {enc (w, I) |w I. length I = n \<and> wf_interp_for_formula (w, I) \<psi>}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
x \<in> lang n (ENC n (FOV \<phi>)) \<inter> lang n (ENC n (FOV \<psi>))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ENC_FOr:
  "wf_formula n (FOr \<phi> \<psi>) \<Longrightarrow> lang n (ENC n (FOV (FOr \<phi> \<psi>))) \<subseteq> lang n (ENC n (FOV \<phi>)) \<inter> lang n (ENC n (FOV \<psi>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf_formula n (FOr \<phi> \<psi>) \<Longrightarrow> lang n (ENC n (FOV (FOr \<phi> \<psi>))) \<subseteq> lang n (ENC n (FOV \<phi>)) \<inter> lang n (ENC n (FOV \<psi>))
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>wf_formula n (FOr \<phi> \<psi>); x \<in> lang n (ENC n (FOV (FOr \<phi> \<psi>)))\<rbrakk> \<Longrightarrow> x \<in> lang n (ENC n (FOV \<phi>)) \<inter> lang n (ENC n (FOV \<psi>))
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>wf_formula n (FOr \<phi> \<psi>); x \<in> lang n (ENC n (FOV (FOr \<phi> \<psi>)))\<rbrakk> \<Longrightarrow> x \<in> lang n (ENC n (FOV \<phi>)) \<inter> lang n (ENC n (FOV \<psi>))
[PROOF STEP]
assume wf: "wf_formula n (FOr \<phi> \<psi>)" and x: "x \<in> lang n (ENC n (FOV (FOr \<phi> \<psi>)))"
[PROOF STATE]
proof (state)
this:
wf_formula n (FOr \<phi> \<psi>)
x \<in> lang n (ENC n (FOV (FOr \<phi> \<psi>)))

goal (1 subgoal):
 1. \<And>x. \<lbrakk>wf_formula n (FOr \<phi> \<psi>); x \<in> lang n (ENC n (FOV (FOr \<phi> \<psi>)))\<rbrakk> \<Longrightarrow> x \<in> lang n (ENC n (FOV \<phi>)) \<inter> lang n (ENC n (FOV \<psi>))
[PROOF STEP]
hence wf1: "wf_formula n \<phi>" and wf2: "wf_formula n \<psi>"
[PROOF STATE]
proof (prove)
using this:
wf_formula n (FOr \<phi> \<psi>)
x \<in> lang n (ENC n (FOV (FOr \<phi> \<psi>)))

goal (1 subgoal):
 1. wf_formula n \<phi> &&& wf_formula n \<psi>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
wf_formula n \<phi>
wf_formula n \<psi>

goal (1 subgoal):
 1. \<And>x. \<lbrakk>wf_formula n (FOr \<phi> \<psi>); x \<in> lang n (ENC n (FOV (FOr \<phi> \<psi>)))\<rbrakk> \<Longrightarrow> x \<in> lang n (ENC n (FOV \<phi>)) \<inter> lang n (ENC n (FOV \<psi>))
[PROOF STEP]
from x
[PROOF STATE]
proof (chain)
picking this:
x \<in> lang n (ENC n (FOV (FOr \<phi> \<psi>)))
[PROOF STEP]
obtain w I where I: "x \<in> enc (w, I)" "wf_interp_for_formula (w, I) (FOr \<phi> \<psi>)" "length I = n"
[PROOF STATE]
proof (prove)
using this:
x \<in> lang n (ENC n (FOV (FOr \<phi> \<psi>)))

goal (1 subgoal):
 1. (\<And>w I. \<lbrakk>x \<in> enc (w, I); wf_interp_for_formula (w, I) (FOr \<phi> \<psi>); length I = n\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using lang_ENC_formula[OF wf]
[PROOF STATE]
proof (prove)
using this:
x \<in> lang n (ENC n (FOV (FOr \<phi> \<psi>)))
lang n (ENC n (FOV (FOr \<phi> \<psi>))) = \<Union> {enc (w, I) |w I. length I = n \<and> wf_interp_for_formula (w, I) (FOr \<phi> \<psi>)}

goal (1 subgoal):
 1. (\<And>w I. \<lbrakk>x \<in> enc (w, I); wf_interp_for_formula (w, I) (FOr \<phi> \<psi>); length I = n\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<in> enc (w, I)
wf_interp_for_formula (w, I) (FOr \<phi> \<psi>)
length I = n

goal (1 subgoal):
 1. \<And>x. \<lbrakk>wf_formula n (FOr \<phi> \<psi>); x \<in> lang n (ENC n (FOV (FOr \<phi> \<psi>)))\<rbrakk> \<Longrightarrow> x \<in> lang n (ENC n (FOV \<phi>)) \<inter> lang n (ENC n (FOV \<psi>))
[PROOF STEP]
hence "wf_interp_for_formula (w, I) \<phi>" "wf_interp_for_formula (w, I) \<psi>"
[PROOF STATE]
proof (prove)
using this:
x \<in> enc (w, I)
wf_interp_for_formula (w, I) (FOr \<phi> \<psi>)
length I = n

goal (1 subgoal):
 1. wf_interp_for_formula (w, I) \<phi> &&& wf_interp_for_formula (w, I) \<psi>
[PROOF STEP]
using wf_interp_for_formula_FOr
[PROOF STATE]
proof (prove)
using this:
x \<in> enc (w, I)
wf_interp_for_formula (w, I) (FOr \<phi> \<psi>)
length I = n
wf_interp_for_formula (?w, ?I) (FOr ?\<phi>1.0 ?\<phi>2.0) = (wf_interp_for_formula (?w, ?I) ?\<phi>1.0 \<and> wf_interp_for_formula (?w, ?I) ?\<phi>2.0)

goal (1 subgoal):
 1. wf_interp_for_formula (w, I) \<phi> &&& wf_interp_for_formula (w, I) \<psi>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
wf_interp_for_formula (w, I) \<phi>
wf_interp_for_formula (w, I) \<psi>

goal (1 subgoal):
 1. \<And>x. \<lbrakk>wf_formula n (FOr \<phi> \<psi>); x \<in> lang n (ENC n (FOV (FOr \<phi> \<psi>)))\<rbrakk> \<Longrightarrow> x \<in> lang n (ENC n (FOV \<phi>)) \<inter> lang n (ENC n (FOV \<psi>))
[PROOF STEP]
thus "x \<in> lang n (ENC n (FOV \<phi>)) \<inter> lang n (ENC n (FOV \<psi>))"
[PROOF STATE]
proof (prove)
using this:
wf_interp_for_formula (w, I) \<phi>
wf_interp_for_formula (w, I) \<psi>

goal (1 subgoal):
 1. x \<in> lang n (ENC n (FOV \<phi>)) \<inter> lang n (ENC n (FOV \<psi>))
[PROOF STEP]
unfolding lang_ENC_formula[OF wf1] lang_ENC_formula[OF wf2]
[PROOF STATE]
proof (prove)
using this:
wf_interp_for_formula (w, I) \<phi>
wf_interp_for_formula (w, I) \<psi>

goal (1 subgoal):
 1. x \<in> \<Union> {enc (w, I) |w I. length I = n \<and> wf_interp_for_formula (w, I) \<phi>} \<inter> \<Union> {enc (w, I) |w I. length I = n \<and> wf_interp_for_formula (w, I) \<psi>}
[PROOF STEP]
using I
[PROOF STATE]
proof (prove)
using this:
wf_interp_for_formula (w, I) \<phi>
wf_interp_for_formula (w, I) \<psi>
x \<in> enc (w, I)
wf_interp_for_formula (w, I) (FOr \<phi> \<psi>)
length I = n

goal (1 subgoal):
 1. x \<in> \<Union> {enc (w, I) |w I. length I = n \<and> wf_interp_for_formula (w, I) \<phi>} \<inter> \<Union> {enc (w, I) |w I. length I = n \<and> wf_interp_for_formula (w, I) \<psi>}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
x \<in> lang n (ENC n (FOV \<phi>)) \<inter> lang n (ENC n (FOV \<psi>))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ENC_FExists:
  "wf_formula n (FExists \<phi>) \<Longrightarrow> lang n (ENC n (FOV (FExists \<phi>))) =
  SAMEQUOT (any, replicate n False) (map \<pi> ` lang (Suc n) (ENC (Suc n) (FOV \<phi>)))" (is "_ \<Longrightarrow> ?L = ?R")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf_formula n (FExists \<phi>) \<Longrightarrow> lang n (ENC n (FOV (FExists \<phi>))) = SAMEQUOT (any, replicate n False) (map \<pi> ` lang (Suc n) (ENC (Suc n) (FOV \<phi>)))
[PROOF STEP]
proof (intro equalityI subsetI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>wf_formula n (FExists \<phi>); x \<in> lang n (ENC n (FOV (FExists \<phi>)))\<rbrakk> \<Longrightarrow> x \<in> SAMEQUOT (any, replicate n False) (map \<pi> ` lang (Suc n) (ENC (Suc n) (FOV \<phi>)))
 2. \<And>x. \<lbrakk>wf_formula n (FExists \<phi>); x \<in> SAMEQUOT (any, replicate n False) (map \<pi> ` lang (Suc n) (ENC (Suc n) (FOV \<phi>)))\<rbrakk> \<Longrightarrow> x \<in> lang n (ENC n (FOV (FExists \<phi>)))
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>wf_formula n (FExists \<phi>); x \<in> lang n (ENC n (FOV (FExists \<phi>)))\<rbrakk> \<Longrightarrow> x \<in> SAMEQUOT (any, replicate n False) (map \<pi> ` lang (Suc n) (ENC (Suc n) (FOV \<phi>)))
 2. \<And>x. \<lbrakk>wf_formula n (FExists \<phi>); x \<in> SAMEQUOT (any, replicate n False) (map \<pi> ` lang (Suc n) (ENC (Suc n) (FOV \<phi>)))\<rbrakk> \<Longrightarrow> x \<in> lang n (ENC n (FOV (FExists \<phi>)))
[PROOF STEP]
assume wf: "wf_formula n (FExists \<phi>)" and x: "x \<in> ?L"
[PROOF STATE]
proof (state)
this:
wf_formula n (FExists \<phi>)
x \<in> lang n (ENC n (FOV (FExists \<phi>)))

goal (2 subgoals):
 1. \<And>x. \<lbrakk>wf_formula n (FExists \<phi>); x \<in> lang n (ENC n (FOV (FExists \<phi>)))\<rbrakk> \<Longrightarrow> x \<in> SAMEQUOT (any, replicate n False) (map \<pi> ` lang (Suc n) (ENC (Suc n) (FOV \<phi>)))
 2. \<And>x. \<lbrakk>wf_formula n (FExists \<phi>); x \<in> SAMEQUOT (any, replicate n False) (map \<pi> ` lang (Suc n) (ENC (Suc n) (FOV \<phi>)))\<rbrakk> \<Longrightarrow> x \<in> lang n (ENC n (FOV (FExists \<phi>)))
[PROOF STEP]
hence wf1: "wf_formula (Suc n) \<phi>"
[PROOF STATE]
proof (prove)
using this:
wf_formula n (FExists \<phi>)
x \<in> lang n (ENC n (FOV (FExists \<phi>)))

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

goal (2 subgoals):
 1. \<And>x. \<lbrakk>wf_formula n (FExists \<phi>); x \<in> lang n (ENC n (FOV (FExists \<phi>)))\<rbrakk> \<Longrightarrow> x \<in> SAMEQUOT (any, replicate n False) (map \<pi> ` lang (Suc n) (ENC (Suc n) (FOV \<phi>)))
 2. \<And>x. \<lbrakk>wf_formula n (FExists \<phi>); x \<in> SAMEQUOT (any, replicate n False) (map \<pi> ` lang (Suc n) (ENC (Suc n) (FOV \<phi>)))\<rbrakk> \<Longrightarrow> x \<in> lang n (ENC n (FOV (FExists \<phi>)))
[PROOF STEP]
from x
[PROOF STATE]
proof (chain)
picking this:
x \<in> lang n (ENC n (FOV (FExists \<phi>)))
[PROOF STEP]
obtain w I where I: "x \<in> enc (w, I)" "wf_interp_for_formula (w, I) (FExists \<phi>)" "length I = n"
[PROOF STATE]
proof (prove)
using this:
x \<in> lang n (ENC n (FOV (FExists \<phi>)))

goal (1 subgoal):
 1. (\<And>w I. \<lbrakk>x \<in> enc (w, I); wf_interp_for_formula (w, I) (FExists \<phi>); length I = n\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using lang_ENC_formula[OF wf]
[PROOF STATE]
proof (prove)
using this:
x \<in> lang n (ENC n (FOV (FExists \<phi>)))
lang n (ENC n (FOV (FExists \<phi>))) = \<Union> {enc (w, I) |w I. length I = n \<and> wf_interp_for_formula (w, I) (FExists \<phi>)}

goal (1 subgoal):
 1. (\<And>w I. \<lbrakk>x \<in> enc (w, I); wf_interp_for_formula (w, I) (FExists \<phi>); length I = n\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<in> enc (w, I)
wf_interp_for_formula (w, I) (FExists \<phi>)
length I = n

goal (2 subgoals):
 1. \<And>x. \<lbrakk>wf_formula n (FExists \<phi>); x \<in> lang n (ENC n (FOV (FExists \<phi>)))\<rbrakk> \<Longrightarrow> x \<in> SAMEQUOT (any, replicate n False) (map \<pi> ` lang (Suc n) (ENC (Suc n) (FOV \<phi>)))
 2. \<And>x. \<lbrakk>wf_formula n (FExists \<phi>); x \<in> SAMEQUOT (any, replicate n False) (map \<pi> ` lang (Suc n) (ENC (Suc n) (FOV \<phi>)))\<rbrakk> \<Longrightarrow> x \<in> lang n (ENC n (FOV (FExists \<phi>)))
[PROOF STEP]
from I(2)
[PROOF STATE]
proof (chain)
picking this:
wf_interp_for_formula (w, I) (FExists \<phi>)
[PROOF STEP]
obtain p where "wf_interp_for_formula (w, Inl p # I) \<phi>"
[PROOF STATE]
proof (prove)
using this:
wf_interp_for_formula (w, I) (FExists \<phi>)

goal (1 subgoal):
 1. (\<And>p. wf_interp_for_formula (w, Inl p # I) \<phi> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using wf_interp_for_formula_FExists[OF wf[folded I(3)]]
[PROOF STATE]
proof (prove)
using this:
wf_interp_for_formula (w, I) (FExists \<phi>)
wf_interp_for_formula (?w, I) (FExists \<phi>) = (\<forall>p. wf_interp_for_formula (?w, Inl p # I) \<phi>)

goal (1 subgoal):
 1. (\<And>p. wf_interp_for_formula (w, Inl p # I) \<phi> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
wf_interp_for_formula (w, Inl p # I) \<phi>

goal (2 subgoals):
 1. \<And>x. \<lbrakk>wf_formula n (FExists \<phi>); x \<in> lang n (ENC n (FOV (FExists \<phi>)))\<rbrakk> \<Longrightarrow> x \<in> SAMEQUOT (any, replicate n False) (map \<pi> ` lang (Suc n) (ENC (Suc n) (FOV \<phi>)))
 2. \<And>x. \<lbrakk>wf_formula n (FExists \<phi>); x \<in> SAMEQUOT (any, replicate n False) (map \<pi> ` lang (Suc n) (ENC (Suc n) (FOV \<phi>)))\<rbrakk> \<Longrightarrow> x \<in> lang n (ENC n (FOV (FExists \<phi>)))
[PROOF STEP]
with I(3)
[PROOF STATE]
proof (chain)
picking this:
length I = n
wf_interp_for_formula (w, Inl p # I) \<phi>
[PROOF STEP]
show "x \<in> ?R"
[PROOF STATE]
proof (prove)
using this:
length I = n
wf_interp_for_formula (w, Inl p # I) \<phi>

goal (1 subgoal):
 1. x \<in> SAMEQUOT (any, replicate n False) (map \<pi> ` lang (Suc n) (ENC (Suc n) (FOV \<phi>)))
[PROOF STEP]
unfolding lang_ENC_formula[OF wf1]
[PROOF STATE]
proof (prove)
using this:
length I = n
wf_interp_for_formula (w, Inl p # I) \<phi>

goal (1 subgoal):
 1. x \<in> SAMEQUOT (any, replicate n False) (map \<pi> ` \<Union> {enc (w, I) |w I. length I = Suc n \<and> wf_interp_for_formula (w, I) \<phi>})
[PROOF STEP]
using I(1) tl_enc[of "Inl p" I, symmetric]
[PROOF STATE]
proof (prove)
using this:
length I = n
wf_interp_for_formula (w, Inl p # I) \<phi>
x \<in> enc (w, I)
\<forall>x\<in>set (Inl p # I). case x of Inl a \<Rightarrow> True | Inr P \<Rightarrow> finite P \<Longrightarrow> enc (?w, I) = SAMEQUOT (any, replicate (length I) False) (map \<pi> ` enc (?w, Inl p # I))

goal (1 subgoal):
 1. x \<in> SAMEQUOT (any, replicate n False) (map \<pi> ` \<Union> {enc (w, I) |w I. length I = Suc n \<and> wf_interp_for_formula (w, I) \<phi>})
[PROOF STEP]
by (simp del: enc.simps)
      (fastforce simp del: enc.simps elim!: rev_subsetD[OF _ SAMEQUOT_mono[OF image_mono]]
        intro: exI[of _ "enc (w, Inl p # I)"])
[PROOF STATE]
proof (state)
this:
x \<in> SAMEQUOT (any, replicate n False) (map \<pi> ` lang (Suc n) (ENC (Suc n) (FOV \<phi>)))

goal (1 subgoal):
 1. \<And>x. \<lbrakk>wf_formula n (FExists \<phi>); x \<in> SAMEQUOT (any, replicate n False) (map \<pi> ` lang (Suc n) (ENC (Suc n) (FOV \<phi>)))\<rbrakk> \<Longrightarrow> x \<in> lang n (ENC n (FOV (FExists \<phi>)))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>wf_formula n (FExists \<phi>); x \<in> SAMEQUOT (any, replicate n False) (map \<pi> ` lang (Suc n) (ENC (Suc n) (FOV \<phi>)))\<rbrakk> \<Longrightarrow> x \<in> lang n (ENC n (FOV (FExists \<phi>)))
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>wf_formula n (FExists \<phi>); x \<in> SAMEQUOT (any, replicate n False) (map \<pi> ` lang (Suc n) (ENC (Suc n) (FOV \<phi>)))\<rbrakk> \<Longrightarrow> x \<in> lang n (ENC n (FOV (FExists \<phi>)))
[PROOF STEP]
assume wf: "wf_formula n (FExists \<phi>)" and x: "x \<in> ?R"
[PROOF STATE]
proof (state)
this:
wf_formula n (FExists \<phi>)
x \<in> SAMEQUOT (any, replicate n False) (map \<pi> ` lang (Suc n) (ENC (Suc n) (FOV \<phi>)))

goal (1 subgoal):
 1. \<And>x. \<lbrakk>wf_formula n (FExists \<phi>); x \<in> SAMEQUOT (any, replicate n False) (map \<pi> ` lang (Suc n) (ENC (Suc n) (FOV \<phi>)))\<rbrakk> \<Longrightarrow> x \<in> lang n (ENC n (FOV (FExists \<phi>)))
[PROOF STEP]
hence wf1: "wf_formula (Suc n) \<phi>" and "0 \<in> FOV \<phi>"
[PROOF STATE]
proof (prove)
using this:
wf_formula n (FExists \<phi>)
x \<in> SAMEQUOT (any, replicate n False) (map \<pi> ` lang (Suc n) (ENC (Suc n) (FOV \<phi>)))

goal (1 subgoal):
 1. wf_formula (Suc n) \<phi> &&& 0 \<in> FOV \<phi>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
wf_formula (Suc n) \<phi>
0 \<in> FOV \<phi>

goal (1 subgoal):
 1. \<And>x. \<lbrakk>wf_formula n (FExists \<phi>); x \<in> SAMEQUOT (any, replicate n False) (map \<pi> ` lang (Suc n) (ENC (Suc n) (FOV \<phi>)))\<rbrakk> \<Longrightarrow> x \<in> lang n (ENC n (FOV (FExists \<phi>)))
[PROOF STEP]
from x
[PROOF STATE]
proof (chain)
picking this:
x \<in> SAMEQUOT (any, replicate n False) (map \<pi> ` lang (Suc n) (ENC (Suc n) (FOV \<phi>)))
[PROOF STEP]
obtain w I where I: "x \<in> SAMEQUOT (any, replicate n False) (map \<pi> ` enc (w, I))"
    "wf_interp_for_formula (w, I) \<phi>" "length I = Suc n"
[PROOF STATE]
proof (prove)
using this:
x \<in> SAMEQUOT (any, replicate n False) (map \<pi> ` lang (Suc n) (ENC (Suc n) (FOV \<phi>)))

goal (1 subgoal):
 1. (\<And>w I. \<lbrakk>x \<in> SAMEQUOT (any, replicate n False) (map \<pi> ` enc (w, I)); wf_interp_for_formula (w, I) \<phi>; length I = Suc n\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using lang_ENC_formula[OF wf1]
[PROOF STATE]
proof (prove)
using this:
x \<in> SAMEQUOT (any, replicate n False) (map \<pi> ` lang (Suc n) (ENC (Suc n) (FOV \<phi>)))
lang (Suc n) (ENC (Suc n) (FOV \<phi>)) = \<Union> {enc (w, I) |w I. length I = Suc n \<and> wf_interp_for_formula (w, I) \<phi>}

goal (1 subgoal):
 1. (\<And>w I. \<lbrakk>x \<in> SAMEQUOT (any, replicate n False) (map \<pi> ` enc (w, I)); wf_interp_for_formula (w, I) \<phi>; length I = Suc n\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding SAMEQUOT_def
[PROOF STATE]
proof (prove)
using this:
x \<in> {fin_cut_same (any, replicate n False) x @ replicate m (any, replicate n False) |x m. x \<in> map \<pi> ` lang (Suc n) (ENC (Suc n) (FOV \<phi>))}
lang (Suc n) (ENC (Suc n) (FOV \<phi>)) = \<Union> {enc (w, I) |w I. length I = Suc n \<and> wf_interp_for_formula (w, I) \<phi>}

goal (1 subgoal):
 1. (\<And>w I. \<lbrakk>x \<in> {fin_cut_same (any, replicate n False) x @ replicate m (any, replicate n False) |x m. x \<in> map \<pi> ` enc (w, I)}; wf_interp_for_formula (w, I) \<phi>; length I = Suc n\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
x \<in> SAMEQUOT (any, replicate n False) (map \<pi> ` enc (w, I))
wf_interp_for_formula (w, I) \<phi>
length I = Suc n

goal (1 subgoal):
 1. \<And>x. \<lbrakk>wf_formula n (FExists \<phi>); x \<in> SAMEQUOT (any, replicate n False) (map \<pi> ` lang (Suc n) (ENC (Suc n) (FOV \<phi>)))\<rbrakk> \<Longrightarrow> x \<in> lang n (ENC n (FOV (FExists \<phi>)))
[PROOF STEP]
with \<open>0 \<in> FOV \<phi>\<close>
[PROOF STATE]
proof (chain)
picking this:
0 \<in> FOV \<phi>
x \<in> SAMEQUOT (any, replicate n False) (map \<pi> ` enc (w, I))
wf_interp_for_formula (w, I) \<phi>
length I = Suc n
[PROOF STEP]
obtain p I' where I': "I = Inl p # I'"
[PROOF STATE]
proof (prove)
using this:
0 \<in> FOV \<phi>
x \<in> SAMEQUOT (any, replicate n False) (map \<pi> ` enc (w, I))
wf_interp_for_formula (w, I) \<phi>
length I = Suc n

goal (1 subgoal):
 1. (\<And>p I'. I = Inl p # I' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases I) (fastforce split: sum.splits)+
[PROOF STATE]
proof (state)
this:
I = Inl p # I'

goal (1 subgoal):
 1. \<And>x. \<lbrakk>wf_formula n (FExists \<phi>); x \<in> SAMEQUOT (any, replicate n False) (map \<pi> ` lang (Suc n) (ENC (Suc n) (FOV \<phi>)))\<rbrakk> \<Longrightarrow> x \<in> lang n (ENC n (FOV (FExists \<phi>)))
[PROOF STEP]
with I
[PROOF STATE]
proof (chain)
picking this:
x \<in> SAMEQUOT (any, replicate n False) (map \<pi> ` enc (w, I))
wf_interp_for_formula (w, I) \<phi>
length I = Suc n
I = Inl p # I'
[PROOF STEP]
have wtlI: "x \<in> enc (w, I')" "length I' = n"
[PROOF STATE]
proof (prove)
using this:
x \<in> SAMEQUOT (any, replicate n False) (map \<pi> ` enc (w, I))
wf_interp_for_formula (w, I) \<phi>
length I = Suc n
I = Inl p # I'

goal (1 subgoal):
 1. x \<in> enc (w, I') &&& length I' = n
[PROOF STEP]
using tl_enc[of "Inl p" I' w]
[PROOF STATE]
proof (prove)
using this:
x \<in> SAMEQUOT (any, replicate n False) (map \<pi> ` enc (w, I))
wf_interp_for_formula (w, I) \<phi>
length I = Suc n
I = Inl p # I'
\<forall>x\<in>set (Inl p # I'). case x of Inl a \<Rightarrow> True | Inr P \<Rightarrow> finite P \<Longrightarrow> SAMEQUOT (any, replicate (length I') False) (map \<pi> ` enc (w, Inl p # I')) = enc (w, I')

goal (1 subgoal):
 1. x \<in> enc (w, I') &&& length I' = n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<in> enc (w, I')
length I' = n

goal (1 subgoal):
 1. \<And>x. \<lbrakk>wf_formula n (FExists \<phi>); x \<in> SAMEQUOT (any, replicate n False) (map \<pi> ` lang (Suc n) (ENC (Suc n) (FOV \<phi>)))\<rbrakk> \<Longrightarrow> x \<in> lang n (ENC n (FOV (FExists \<phi>)))
[PROOF STEP]
have "wf_interp_for_formula (w, I') (FExists \<phi>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf_interp_for_formula (w, I') (FExists \<phi>)
[PROOF STEP]
using wf_interp_for_formula_FExists[OF wf[folded wtlI(2)]]
          wf_interp_for_formula_any_Inl[OF I(2)[unfolded I']]
[PROOF STATE]
proof (prove)
using this:
wf_interp_for_formula (?w, I') (FExists \<phi>) = (\<forall>p. wf_interp_for_formula (?w, Inl p # I') \<phi>)
\<forall>p. wf_interp_for_formula (w, Inl p # I') \<phi>

goal (1 subgoal):
 1. wf_interp_for_formula (w, I') (FExists \<phi>)
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
wf_interp_for_formula (w, I') (FExists \<phi>)

goal (1 subgoal):
 1. \<And>x. \<lbrakk>wf_formula n (FExists \<phi>); x \<in> SAMEQUOT (any, replicate n False) (map \<pi> ` lang (Suc n) (ENC (Suc n) (FOV \<phi>)))\<rbrakk> \<Longrightarrow> x \<in> lang n (ENC n (FOV (FExists \<phi>)))
[PROOF STEP]
with wtlI
[PROOF STATE]
proof (chain)
picking this:
x \<in> enc (w, I')
length I' = n
wf_interp_for_formula (w, I') (FExists \<phi>)
[PROOF STEP]
show "x \<in> ?L"
[PROOF STATE]
proof (prove)
using this:
x \<in> enc (w, I')
length I' = n
wf_interp_for_formula (w, I') (FExists \<phi>)

goal (1 subgoal):
 1. x \<in> lang n (ENC n (FOV (FExists \<phi>)))
[PROOF STEP]
unfolding lang_ENC_formula[OF wf]
[PROOF STATE]
proof (prove)
using this:
x \<in> enc (w, I')
length I' = n
wf_interp_for_formula (w, I') (FExists \<phi>)

goal (1 subgoal):
 1. x \<in> \<Union> {enc (w, I) |w I. length I = n \<and> wf_interp_for_formula (w, I) (FExists \<phi>)}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
x \<in> lang n (ENC n (FOV (FExists \<phi>)))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ENC_FEXISTS:
  "wf_formula n (FEXISTS \<phi>) \<Longrightarrow> lang n (ENC n (FOV (FEXISTS \<phi>))) =
  SAMEQUOT (any, replicate n False) (map \<pi> ` lang (Suc n) (ENC (Suc n) (FOV \<phi>)))" (is "_ \<Longrightarrow> ?L = ?R")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf_formula n (FEXISTS \<phi>) \<Longrightarrow> lang n (ENC n (FOV (FEXISTS \<phi>))) = SAMEQUOT (any, replicate n False) (map \<pi> ` lang (Suc n) (ENC (Suc n) (FOV \<phi>)))
[PROOF STEP]
proof (intro equalityI subsetI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>wf_formula n (FEXISTS \<phi>); x \<in> lang n (ENC n (FOV (FEXISTS \<phi>)))\<rbrakk> \<Longrightarrow> x \<in> SAMEQUOT (any, replicate n False) (map \<pi> ` lang (Suc n) (ENC (Suc n) (FOV \<phi>)))
 2. \<And>x. \<lbrakk>wf_formula n (FEXISTS \<phi>); x \<in> SAMEQUOT (any, replicate n False) (map \<pi> ` lang (Suc n) (ENC (Suc n) (FOV \<phi>)))\<rbrakk> \<Longrightarrow> x \<in> lang n (ENC n (FOV (FEXISTS \<phi>)))
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>wf_formula n (FEXISTS \<phi>); x \<in> lang n (ENC n (FOV (FEXISTS \<phi>)))\<rbrakk> \<Longrightarrow> x \<in> SAMEQUOT (any, replicate n False) (map \<pi> ` lang (Suc n) (ENC (Suc n) (FOV \<phi>)))
 2. \<And>x. \<lbrakk>wf_formula n (FEXISTS \<phi>); x \<in> SAMEQUOT (any, replicate n False) (map \<pi> ` lang (Suc n) (ENC (Suc n) (FOV \<phi>)))\<rbrakk> \<Longrightarrow> x \<in> lang n (ENC n (FOV (FEXISTS \<phi>)))
[PROOF STEP]
assume wf: "wf_formula n (FEXISTS \<phi>)" and x: "x \<in> ?L"
[PROOF STATE]
proof (state)
this:
wf_formula n (FEXISTS \<phi>)
x \<in> lang n (ENC n (FOV (FEXISTS \<phi>)))

goal (2 subgoals):
 1. \<And>x. \<lbrakk>wf_formula n (FEXISTS \<phi>); x \<in> lang n (ENC n (FOV (FEXISTS \<phi>)))\<rbrakk> \<Longrightarrow> x \<in> SAMEQUOT (any, replicate n False) (map \<pi> ` lang (Suc n) (ENC (Suc n) (FOV \<phi>)))
 2. \<And>x. \<lbrakk>wf_formula n (FEXISTS \<phi>); x \<in> SAMEQUOT (any, replicate n False) (map \<pi> ` lang (Suc n) (ENC (Suc n) (FOV \<phi>)))\<rbrakk> \<Longrightarrow> x \<in> lang n (ENC n (FOV (FEXISTS \<phi>)))
[PROOF STEP]
hence wf1: "wf_formula (Suc n) \<phi>"
[PROOF STATE]
proof (prove)
using this:
wf_formula n (FEXISTS \<phi>)
x \<in> lang n (ENC n (FOV (FEXISTS \<phi>)))

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

goal (2 subgoals):
 1. \<And>x. \<lbrakk>wf_formula n (FEXISTS \<phi>); x \<in> lang n (ENC n (FOV (FEXISTS \<phi>)))\<rbrakk> \<Longrightarrow> x \<in> SAMEQUOT (any, replicate n False) (map \<pi> ` lang (Suc n) (ENC (Suc n) (FOV \<phi>)))
 2. \<And>x. \<lbrakk>wf_formula n (FEXISTS \<phi>); x \<in> SAMEQUOT (any, replicate n False) (map \<pi> ` lang (Suc n) (ENC (Suc n) (FOV \<phi>)))\<rbrakk> \<Longrightarrow> x \<in> lang n (ENC n (FOV (FEXISTS \<phi>)))
[PROOF STEP]
from x
[PROOF STATE]
proof (chain)
picking this:
x \<in> lang n (ENC n (FOV (FEXISTS \<phi>)))
[PROOF STEP]
obtain w I where I: "x \<in> enc (w, I)" "wf_interp_for_formula (w, I) (FEXISTS \<phi>)" "length I = n"
[PROOF STATE]
proof (prove)
using this:
x \<in> lang n (ENC n (FOV (FEXISTS \<phi>)))

goal (1 subgoal):
 1. (\<And>w I. \<lbrakk>x \<in> enc (w, I); wf_interp_for_formula (w, I) (FEXISTS \<phi>); length I = n\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using lang_ENC_formula[OF wf]
[PROOF STATE]
proof (prove)
using this:
x \<in> lang n (ENC n (FOV (FEXISTS \<phi>)))
lang n (ENC n (FOV (FEXISTS \<phi>))) = \<Union> {enc (w, I) |w I. length I = n \<and> wf_interp_for_formula (w, I) (FEXISTS \<phi>)}

goal (1 subgoal):
 1. (\<And>w I. \<lbrakk>x \<in> enc (w, I); wf_interp_for_formula (w, I) (FEXISTS \<phi>); length I = n\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<in> enc (w, I)
wf_interp_for_formula (w, I) (FEXISTS \<phi>)
length I = n

goal (2 subgoals):
 1. \<And>x. \<lbrakk>wf_formula n (FEXISTS \<phi>); x \<in> lang n (ENC n (FOV (FEXISTS \<phi>)))\<rbrakk> \<Longrightarrow> x \<in> SAMEQUOT (any, replicate n False) (map \<pi> ` lang (Suc n) (ENC (Suc n) (FOV \<phi>)))
 2. \<And>x. \<lbrakk>wf_formula n (FEXISTS \<phi>); x \<in> SAMEQUOT (any, replicate n False) (map \<pi> ` lang (Suc n) (ENC (Suc n) (FOV \<phi>)))\<rbrakk> \<Longrightarrow> x \<in> lang n (ENC n (FOV (FEXISTS \<phi>)))
[PROOF STEP]
from I(2)
[PROOF STATE]
proof (chain)
picking this:
wf_interp_for_formula (w, I) (FEXISTS \<phi>)
[PROOF STEP]
obtain P where "wf_interp_for_formula (w, Inr P # I) \<phi>"
[PROOF STATE]
proof (prove)
using this:
wf_interp_for_formula (w, I) (FEXISTS \<phi>)

goal (1 subgoal):
 1. (\<And>P. wf_interp_for_formula (w, Inr P # I) \<phi> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using wf_interp_for_formula_FEXISTS[OF wf[folded I(3)]]
[PROOF STATE]
proof (prove)
using this:
wf_interp_for_formula (w, I) (FEXISTS \<phi>)
wf_interp_for_formula (?w, I) (FEXISTS \<phi>) = (\<forall>P. finite P \<longrightarrow> wf_interp_for_formula (?w, Inr P # I) \<phi>)

goal (1 subgoal):
 1. (\<And>P. wf_interp_for_formula (w, Inr P # I) \<phi> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
wf_interp_for_formula (w, Inr P # I) \<phi>

goal (2 subgoals):
 1. \<And>x. \<lbrakk>wf_formula n (FEXISTS \<phi>); x \<in> lang n (ENC n (FOV (FEXISTS \<phi>)))\<rbrakk> \<Longrightarrow> x \<in> SAMEQUOT (any, replicate n False) (map \<pi> ` lang (Suc n) (ENC (Suc n) (FOV \<phi>)))
 2. \<And>x. \<lbrakk>wf_formula n (FEXISTS \<phi>); x \<in> SAMEQUOT (any, replicate n False) (map \<pi> ` lang (Suc n) (ENC (Suc n) (FOV \<phi>)))\<rbrakk> \<Longrightarrow> x \<in> lang n (ENC n (FOV (FEXISTS \<phi>)))
[PROOF STEP]
with I(3)
[PROOF STATE]
proof (chain)
picking this:
length I = n
wf_interp_for_formula (w, Inr P # I) \<phi>
[PROOF STEP]
show "x \<in> ?R"
[PROOF STATE]
proof (prove)
using this:
length I = n
wf_interp_for_formula (w, Inr P # I) \<phi>

goal (1 subgoal):
 1. x \<in> SAMEQUOT (any, replicate n False) (map \<pi> ` lang (Suc n) (ENC (Suc n) (FOV \<phi>)))
[PROOF STEP]
unfolding lang_ENC_formula[OF wf1]
[PROOF STATE]
proof (prove)
using this:
length I = n
wf_interp_for_formula (w, Inr P # I) \<phi>

goal (1 subgoal):
 1. x \<in> SAMEQUOT (any, replicate n False) (map \<pi> ` \<Union> {enc (w, I) |w I. length I = Suc n \<and> wf_interp_for_formula (w, I) \<phi>})
[PROOF STEP]
using I(1) tl_enc[of "Inr P" I, symmetric]
[PROOF STATE]
proof (prove)
using this:
length I = n
wf_interp_for_formula (w, Inr P # I) \<phi>
x \<in> enc (w, I)
\<forall>x\<in>set (Inr P # I). case x of Inl a \<Rightarrow> True | Inr P \<Rightarrow> finite P \<Longrightarrow> enc (?w, I) = SAMEQUOT (any, replicate (length I) False) (map \<pi> ` enc (?w, Inr P # I))

goal (1 subgoal):
 1. x \<in> SAMEQUOT (any, replicate n False) (map \<pi> ` \<Union> {enc (w, I) |w I. length I = Suc n \<and> wf_interp_for_formula (w, I) \<phi>})
[PROOF STEP]
by (simp del: enc.simps)
      (fastforce simp del: enc.simps elim!: rev_subsetD[OF _ SAMEQUOT_mono[OF image_mono]]
        intro: exI[of _ "enc (w, Inr P # I)"])
[PROOF STATE]
proof (state)
this:
x \<in> SAMEQUOT (any, replicate n False) (map \<pi> ` lang (Suc n) (ENC (Suc n) (FOV \<phi>)))

goal (1 subgoal):
 1. \<And>x. \<lbrakk>wf_formula n (FEXISTS \<phi>); x \<in> SAMEQUOT (any, replicate n False) (map \<pi> ` lang (Suc n) (ENC (Suc n) (FOV \<phi>)))\<rbrakk> \<Longrightarrow> x \<in> lang n (ENC n (FOV (FEXISTS \<phi>)))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>wf_formula n (FEXISTS \<phi>); x \<in> SAMEQUOT (any, replicate n False) (map \<pi> ` lang (Suc n) (ENC (Suc n) (FOV \<phi>)))\<rbrakk> \<Longrightarrow> x \<in> lang n (ENC n (FOV (FEXISTS \<phi>)))
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>wf_formula n (FEXISTS \<phi>); x \<in> SAMEQUOT (any, replicate n False) (map \<pi> ` lang (Suc n) (ENC (Suc n) (FOV \<phi>)))\<rbrakk> \<Longrightarrow> x \<in> lang n (ENC n (FOV (FEXISTS \<phi>)))
[PROOF STEP]
assume wf: "wf_formula n (FEXISTS \<phi>)" and x: "x \<in> ?R"
[PROOF STATE]
proof (state)
this:
wf_formula n (FEXISTS \<phi>)
x \<in> SAMEQUOT (any, replicate n False) (map \<pi> ` lang (Suc n) (ENC (Suc n) (FOV \<phi>)))

goal (1 subgoal):
 1. \<And>x. \<lbrakk>wf_formula n (FEXISTS \<phi>); x \<in> SAMEQUOT (any, replicate n False) (map \<pi> ` lang (Suc n) (ENC (Suc n) (FOV \<phi>)))\<rbrakk> \<Longrightarrow> x \<in> lang n (ENC n (FOV (FEXISTS \<phi>)))
[PROOF STEP]
hence wf1: "wf_formula (Suc n) \<phi>" and "0 \<in> SOV \<phi>"
[PROOF STATE]
proof (prove)
using this:
wf_formula n (FEXISTS \<phi>)
x \<in> SAMEQUOT (any, replicate n False) (map \<pi> ` lang (Suc n) (ENC (Suc n) (FOV \<phi>)))

goal (1 subgoal):
 1. wf_formula (Suc n) \<phi> &&& 0 \<in> SOV \<phi>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
wf_formula (Suc n) \<phi>
0 \<in> SOV \<phi>

goal (1 subgoal):
 1. \<And>x. \<lbrakk>wf_formula n (FEXISTS \<phi>); x \<in> SAMEQUOT (any, replicate n False) (map \<pi> ` lang (Suc n) (ENC (Suc n) (FOV \<phi>)))\<rbrakk> \<Longrightarrow> x \<in> lang n (ENC n (FOV (FEXISTS \<phi>)))
[PROOF STEP]
from x
[PROOF STATE]
proof (chain)
picking this:
x \<in> SAMEQUOT (any, replicate n False) (map \<pi> ` lang (Suc n) (ENC (Suc n) (FOV \<phi>)))
[PROOF STEP]
obtain w I where I: "x \<in> SAMEQUOT (any, replicate n False) (map \<pi> ` enc (w, I))"
    "wf_interp_for_formula (w, I) \<phi>" "length I = Suc n"
[PROOF STATE]
proof (prove)
using this:
x \<in> SAMEQUOT (any, replicate n False) (map \<pi> ` lang (Suc n) (ENC (Suc n) (FOV \<phi>)))

goal (1 subgoal):
 1. (\<And>w I. \<lbrakk>x \<in> SAMEQUOT (any, replicate n False) (map \<pi> ` enc (w, I)); wf_interp_for_formula (w, I) \<phi>; length I = Suc n\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using lang_ENC_formula[OF wf1]
[PROOF STATE]
proof (prove)
using this:
x \<in> SAMEQUOT (any, replicate n False) (map \<pi> ` lang (Suc n) (ENC (Suc n) (FOV \<phi>)))
lang (Suc n) (ENC (Suc n) (FOV \<phi>)) = \<Union> {enc (w, I) |w I. length I = Suc n \<and> wf_interp_for_formula (w, I) \<phi>}

goal (1 subgoal):
 1. (\<And>w I. \<lbrakk>x \<in> SAMEQUOT (any, replicate n False) (map \<pi> ` enc (w, I)); wf_interp_for_formula (w, I) \<phi>; length I = Suc n\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding SAMEQUOT_def
[PROOF STATE]
proof (prove)
using this:
x \<in> {fin_cut_same (any, replicate n False) x @ replicate m (any, replicate n False) |x m. x \<in> map \<pi> ` lang (Suc n) (ENC (Suc n) (FOV \<phi>))}
lang (Suc n) (ENC (Suc n) (FOV \<phi>)) = \<Union> {enc (w, I) |w I. length I = Suc n \<and> wf_interp_for_formula (w, I) \<phi>}

goal (1 subgoal):
 1. (\<And>w I. \<lbrakk>x \<in> {fin_cut_same (any, replicate n False) x @ replicate m (any, replicate n False) |x m. x \<in> map \<pi> ` enc (w, I)}; wf_interp_for_formula (w, I) \<phi>; length I = Suc n\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
x \<in> SAMEQUOT (any, replicate n False) (map \<pi> ` enc (w, I))
wf_interp_for_formula (w, I) \<phi>
length I = Suc n

goal (1 subgoal):
 1. \<And>x. \<lbrakk>wf_formula n (FEXISTS \<phi>); x \<in> SAMEQUOT (any, replicate n False) (map \<pi> ` lang (Suc n) (ENC (Suc n) (FOV \<phi>)))\<rbrakk> \<Longrightarrow> x \<in> lang n (ENC n (FOV (FEXISTS \<phi>)))
[PROOF STEP]
with \<open>0 \<in> SOV \<phi>\<close>
[PROOF STATE]
proof (chain)
picking this:
0 \<in> SOV \<phi>
x \<in> SAMEQUOT (any, replicate n False) (map \<pi> ` enc (w, I))
wf_interp_for_formula (w, I) \<phi>
length I = Suc n
[PROOF STEP]
obtain P I' where I': "I = Inr P # I'"
[PROOF STATE]
proof (prove)
using this:
0 \<in> SOV \<phi>
x \<in> SAMEQUOT (any, replicate n False) (map \<pi> ` enc (w, I))
wf_interp_for_formula (w, I) \<phi>
length I = Suc n

goal (1 subgoal):
 1. (\<And>P I'. I = Inr P # I' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases I) (fastforce split: sum.splits)+
[PROOF STATE]
proof (state)
this:
I = Inr P # I'

goal (1 subgoal):
 1. \<And>x. \<lbrakk>wf_formula n (FEXISTS \<phi>); x \<in> SAMEQUOT (any, replicate n False) (map \<pi> ` lang (Suc n) (ENC (Suc n) (FOV \<phi>)))\<rbrakk> \<Longrightarrow> x \<in> lang n (ENC n (FOV (FEXISTS \<phi>)))
[PROOF STEP]
with I
[PROOF STATE]
proof (chain)
picking this:
x \<in> SAMEQUOT (any, replicate n False) (map \<pi> ` enc (w, I))
wf_interp_for_formula (w, I) \<phi>
length I = Suc n
I = Inr P # I'
[PROOF STEP]
have wtlI: "x \<in> enc (w, I')" "length I' = n"
[PROOF STATE]
proof (prove)
using this:
x \<in> SAMEQUOT (any, replicate n False) (map \<pi> ` enc (w, I))
wf_interp_for_formula (w, I) \<phi>
length I = Suc n
I = Inr P # I'

goal (1 subgoal):
 1. x \<in> enc (w, I') &&& length I' = n
[PROOF STEP]
using tl_enc[of "Inr P" I' w]
[PROOF STATE]
proof (prove)
using this:
x \<in> SAMEQUOT (any, replicate n False) (map \<pi> ` enc (w, I))
wf_interp_for_formula (w, I) \<phi>
length I = Suc n
I = Inr P # I'
\<forall>x\<in>set (Inr P # I'). case x of Inl a \<Rightarrow> True | Inr P \<Rightarrow> finite P \<Longrightarrow> SAMEQUOT (any, replicate (length I') False) (map \<pi> ` enc (w, Inr P # I')) = enc (w, I')

goal (1 subgoal):
 1. x \<in> enc (w, I') &&& length I' = n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<in> enc (w, I')
length I' = n

goal (1 subgoal):
 1. \<And>x. \<lbrakk>wf_formula n (FEXISTS \<phi>); x \<in> SAMEQUOT (any, replicate n False) (map \<pi> ` lang (Suc n) (ENC (Suc n) (FOV \<phi>)))\<rbrakk> \<Longrightarrow> x \<in> lang n (ENC n (FOV (FEXISTS \<phi>)))
[PROOF STEP]
have "wf_interp_for_formula (w, I') (FEXISTS \<phi>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf_interp_for_formula (w, I') (FEXISTS \<phi>)
[PROOF STEP]
using wf_interp_for_formula_FEXISTS[OF wf[folded wtlI(2)]]
          wf_interp_for_formula_any_Inr[OF I(2)[unfolded I']]
[PROOF STATE]
proof (prove)
using this:
wf_interp_for_formula (?w, I') (FEXISTS \<phi>) = (\<forall>P. finite P \<longrightarrow> wf_interp_for_formula (?w, Inr P # I') \<phi>)
\<forall>P. finite P \<longrightarrow> wf_interp_for_formula (w, Inr P # I') \<phi>

goal (1 subgoal):
 1. wf_interp_for_formula (w, I') (FEXISTS \<phi>)
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
wf_interp_for_formula (w, I') (FEXISTS \<phi>)

goal (1 subgoal):
 1. \<And>x. \<lbrakk>wf_formula n (FEXISTS \<phi>); x \<in> SAMEQUOT (any, replicate n False) (map \<pi> ` lang (Suc n) (ENC (Suc n) (FOV \<phi>)))\<rbrakk> \<Longrightarrow> x \<in> lang n (ENC n (FOV (FEXISTS \<phi>)))
[PROOF STEP]
with wtlI
[PROOF STATE]
proof (chain)
picking this:
x \<in> enc (w, I')
length I' = n
wf_interp_for_formula (w, I') (FEXISTS \<phi>)
[PROOF STEP]
show "x \<in> ?L"
[PROOF STATE]
proof (prove)
using this:
x \<in> enc (w, I')
length I' = n
wf_interp_for_formula (w, I') (FEXISTS \<phi>)

goal (1 subgoal):
 1. x \<in> lang n (ENC n (FOV (FEXISTS \<phi>)))
[PROOF STEP]
unfolding lang_ENC_formula[OF wf]
[PROOF STATE]
proof (prove)
using this:
x \<in> enc (w, I')
length I' = n
wf_interp_for_formula (w, I') (FEXISTS \<phi>)

goal (1 subgoal):
 1. x \<in> \<Union> {enc (w, I) |w I. length I = n \<and> wf_interp_for_formula (w, I) (FEXISTS \<phi>)}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
x \<in> lang n (ENC n (FOV (FEXISTS \<phi>)))

goal:
No subgoals!
[PROOF STEP]
qed