[STATEMENT]
lemma lang\<^sub>W\<^sub>S\<^sub>1\<^sub>S_FOr:
  assumes "wf_formula n (FOr \<phi>\<^sub>1 \<phi>\<^sub>2)"
  shows "lang\<^sub>W\<^sub>S\<^sub>1\<^sub>S n (FOr \<phi>\<^sub>1 \<phi>\<^sub>2) \<subseteq>
    (lang\<^sub>W\<^sub>S\<^sub>1\<^sub>S n \<phi>\<^sub>1 \<union> lang\<^sub>W\<^sub>S\<^sub>1\<^sub>S n \<phi>\<^sub>2) \<inter> \<Union>{enc (w, I) | w I. length I = n \<and> wf_interp_for_formula (w, I) (FOr \<phi>\<^sub>1 \<phi>\<^sub>2)}"
    (is "_ \<subseteq> (?L1 \<union> ?L2) \<inter> ?ENC")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lang\<^sub>W\<^sub>S\<^sub>1\<^sub>S n (FOr \<phi>\<^sub>1 \<phi>\<^sub>2) \<subseteq> (lang\<^sub>W\<^sub>S\<^sub>1\<^sub>S n \<phi>\<^sub>1 \<union> lang\<^sub>W\<^sub>S\<^sub>1\<^sub>S n \<phi>\<^sub>2) \<inter> \<Union> {enc (w, I) |w I. length I = n \<and> wf_interp_for_formula (w, I) (FOr \<phi>\<^sub>1 \<phi>\<^sub>2)}
[PROOF STEP]
proof (intro equalityI subsetI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> lang\<^sub>W\<^sub>S\<^sub>1\<^sub>S n (FOr \<phi>\<^sub>1 \<phi>\<^sub>2) \<Longrightarrow> x \<in> (lang\<^sub>W\<^sub>S\<^sub>1\<^sub>S n \<phi>\<^sub>1 \<union> lang\<^sub>W\<^sub>S\<^sub>1\<^sub>S n \<phi>\<^sub>2) \<inter> \<Union> {enc (w, I) |w I. length I = n \<and> wf_interp_for_formula (w, I) (FOr \<phi>\<^sub>1 \<phi>\<^sub>2)}
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> lang\<^sub>W\<^sub>S\<^sub>1\<^sub>S n (FOr \<phi>\<^sub>1 \<phi>\<^sub>2) \<Longrightarrow> x \<in> (lang\<^sub>W\<^sub>S\<^sub>1\<^sub>S n \<phi>\<^sub>1 \<union> lang\<^sub>W\<^sub>S\<^sub>1\<^sub>S n \<phi>\<^sub>2) \<inter> \<Union> {enc (w, I) |w I. length I = n \<and> wf_interp_for_formula (w, I) (FOr \<phi>\<^sub>1 \<phi>\<^sub>2)}
[PROOF STEP]
assume "x \<in> lang\<^sub>W\<^sub>S\<^sub>1\<^sub>S n (FOr \<phi>\<^sub>1 \<phi>\<^sub>2)"
[PROOF STATE]
proof (state)
this:
x \<in> lang\<^sub>W\<^sub>S\<^sub>1\<^sub>S n (FOr \<phi>\<^sub>1 \<phi>\<^sub>2)

goal (1 subgoal):
 1. \<And>x. x \<in> lang\<^sub>W\<^sub>S\<^sub>1\<^sub>S n (FOr \<phi>\<^sub>1 \<phi>\<^sub>2) \<Longrightarrow> x \<in> (lang\<^sub>W\<^sub>S\<^sub>1\<^sub>S n \<phi>\<^sub>1 \<union> lang\<^sub>W\<^sub>S\<^sub>1\<^sub>S n \<phi>\<^sub>2) \<inter> \<Union> {enc (w, I) |w I. length I = n \<and> wf_interp_for_formula (w, I) (FOr \<phi>\<^sub>1 \<phi>\<^sub>2)}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> lang\<^sub>W\<^sub>S\<^sub>1\<^sub>S n (FOr \<phi>\<^sub>1 \<phi>\<^sub>2)
[PROOF STEP]
obtain w I where
    *: "x \<in> enc (w, I)" "wf_interp_for_formula (w, I) (FOr \<phi>\<^sub>1 \<phi>\<^sub>2)" "length I = n" and
     "satisfies (w, I) \<phi>\<^sub>1 \<or> satisfies (w, I) \<phi>\<^sub>2"
[PROOF STATE]
proof (prove)
using this:
x \<in> lang\<^sub>W\<^sub>S\<^sub>1\<^sub>S n (FOr \<phi>\<^sub>1 \<phi>\<^sub>2)

goal (1 subgoal):
 1. (\<And>w I. \<lbrakk>x \<in> enc (w, I); wf_interp_for_formula (w, I) (FOr \<phi>\<^sub>1 \<phi>\<^sub>2); length I = n; (w, I) \<Turnstile> \<phi>\<^sub>1 \<or> (w, I) \<Turnstile> \<phi>\<^sub>2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding lang\<^sub>W\<^sub>S\<^sub>1\<^sub>S_def
[PROOF STATE]
proof (prove)
using this:
x \<in> \<Union> {enc (w, I) |w I. length I = n \<and> wf_interp_for_formula (w, I) (FOr \<phi>\<^sub>1 \<phi>\<^sub>2) \<and> (w, I) \<Turnstile> FOr \<phi>\<^sub>1 \<phi>\<^sub>2}

goal (1 subgoal):
 1. (\<And>w I. \<lbrakk>x \<in> enc (w, I); wf_interp_for_formula (w, I) (FOr \<phi>\<^sub>1 \<phi>\<^sub>2); length I = n; (w, I) \<Turnstile> \<phi>\<^sub>1 \<or> (w, I) \<Turnstile> \<phi>\<^sub>2\<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>\<^sub>1 \<phi>\<^sub>2)
length I = n
(w, I) \<Turnstile> \<phi>\<^sub>1 \<or> (w, I) \<Turnstile> \<phi>\<^sub>2

goal (1 subgoal):
 1. \<And>x. x \<in> lang\<^sub>W\<^sub>S\<^sub>1\<^sub>S n (FOr \<phi>\<^sub>1 \<phi>\<^sub>2) \<Longrightarrow> x \<in> (lang\<^sub>W\<^sub>S\<^sub>1\<^sub>S n \<phi>\<^sub>1 \<union> lang\<^sub>W\<^sub>S\<^sub>1\<^sub>S n \<phi>\<^sub>2) \<inter> \<Union> {enc (w, I) |w I. length I = n \<and> wf_interp_for_formula (w, I) (FOr \<phi>\<^sub>1 \<phi>\<^sub>2)}
[PROOF STEP]
thus "x \<in> (?L1 \<union> ?L2) \<inter> ?ENC"
[PROOF STATE]
proof (prove)
using this:
x \<in> enc (w, I)
wf_interp_for_formula (w, I) (FOr \<phi>\<^sub>1 \<phi>\<^sub>2)
length I = n
(w, I) \<Turnstile> \<phi>\<^sub>1 \<or> (w, I) \<Turnstile> \<phi>\<^sub>2

goal (1 subgoal):
 1. x \<in> (lang\<^sub>W\<^sub>S\<^sub>1\<^sub>S n \<phi>\<^sub>1 \<union> lang\<^sub>W\<^sub>S\<^sub>1\<^sub>S n \<phi>\<^sub>2) \<inter> \<Union> {enc (w, I) |w I. length I = n \<and> wf_interp_for_formula (w, I) (FOr \<phi>\<^sub>1 \<phi>\<^sub>2)}
[PROOF STEP]
proof (elim disjE)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>x \<in> enc (w, I); wf_interp_for_formula (w, I) (FOr \<phi>\<^sub>1 \<phi>\<^sub>2); length I = n; (w, I) \<Turnstile> \<phi>\<^sub>1\<rbrakk> \<Longrightarrow> x \<in> (lang\<^sub>W\<^sub>S\<^sub>1\<^sub>S n \<phi>\<^sub>1 \<union> lang\<^sub>W\<^sub>S\<^sub>1\<^sub>S n \<phi>\<^sub>2) \<inter> \<Union> {enc (w, I) |w I. length I = n \<and> wf_interp_for_formula (w, I) (FOr \<phi>\<^sub>1 \<phi>\<^sub>2)}
 2. \<lbrakk>x \<in> enc (w, I); wf_interp_for_formula (w, I) (FOr \<phi>\<^sub>1 \<phi>\<^sub>2); length I = n; (w, I) \<Turnstile> \<phi>\<^sub>2\<rbrakk> \<Longrightarrow> x \<in> (lang\<^sub>W\<^sub>S\<^sub>1\<^sub>S n \<phi>\<^sub>1 \<union> lang\<^sub>W\<^sub>S\<^sub>1\<^sub>S n \<phi>\<^sub>2) \<inter> \<Union> {enc (w, I) |w I. length I = n \<and> wf_interp_for_formula (w, I) (FOr \<phi>\<^sub>1 \<phi>\<^sub>2)}
[PROOF STEP]
assume "satisfies (w, I) \<phi>\<^sub>1"
[PROOF STATE]
proof (state)
this:
(w, I) \<Turnstile> \<phi>\<^sub>1

goal (2 subgoals):
 1. \<lbrakk>x \<in> enc (w, I); wf_interp_for_formula (w, I) (FOr \<phi>\<^sub>1 \<phi>\<^sub>2); length I = n; (w, I) \<Turnstile> \<phi>\<^sub>1\<rbrakk> \<Longrightarrow> x \<in> (lang\<^sub>W\<^sub>S\<^sub>1\<^sub>S n \<phi>\<^sub>1 \<union> lang\<^sub>W\<^sub>S\<^sub>1\<^sub>S n \<phi>\<^sub>2) \<inter> \<Union> {enc (w, I) |w I. length I = n \<and> wf_interp_for_formula (w, I) (FOr \<phi>\<^sub>1 \<phi>\<^sub>2)}
 2. \<lbrakk>x \<in> enc (w, I); wf_interp_for_formula (w, I) (FOr \<phi>\<^sub>1 \<phi>\<^sub>2); length I = n; (w, I) \<Turnstile> \<phi>\<^sub>2\<rbrakk> \<Longrightarrow> x \<in> (lang\<^sub>W\<^sub>S\<^sub>1\<^sub>S n \<phi>\<^sub>1 \<union> lang\<^sub>W\<^sub>S\<^sub>1\<^sub>S n \<phi>\<^sub>2) \<inter> \<Union> {enc (w, I) |w I. length I = n \<and> wf_interp_for_formula (w, I) (FOr \<phi>\<^sub>1 \<phi>\<^sub>2)}
[PROOF STEP]
with *
[PROOF STATE]
proof (chain)
picking this:
x \<in> enc (w, I)
wf_interp_for_formula (w, I) (FOr \<phi>\<^sub>1 \<phi>\<^sub>2)
length I = n
(w, I) \<Turnstile> \<phi>\<^sub>1
[PROOF STEP]
have "x \<in> ?L1"
[PROOF STATE]
proof (prove)
using this:
x \<in> enc (w, I)
wf_interp_for_formula (w, I) (FOr \<phi>\<^sub>1 \<phi>\<^sub>2)
length I = n
(w, I) \<Turnstile> \<phi>\<^sub>1

goal (1 subgoal):
 1. x \<in> lang\<^sub>W\<^sub>S\<^sub>1\<^sub>S n \<phi>\<^sub>1
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
x \<in> enc (w, I)
wf_interp_for_formula (w, I) (FOr \<phi>\<^sub>1 \<phi>\<^sub>2)
length I = n
(w, I) \<Turnstile> \<phi>\<^sub>1
wf_formula n (FOr \<phi>\<^sub>1 \<phi>\<^sub>2)

goal (1 subgoal):
 1. x \<in> lang\<^sub>W\<^sub>S\<^sub>1\<^sub>S n \<phi>\<^sub>1
[PROOF STEP]
unfolding lang\<^sub>W\<^sub>S\<^sub>1\<^sub>S_def
[PROOF STATE]
proof (prove)
using this:
x \<in> enc (w, I)
wf_interp_for_formula (w, I) (FOr \<phi>\<^sub>1 \<phi>\<^sub>2)
length I = n
(w, I) \<Turnstile> \<phi>\<^sub>1
wf_formula n (FOr \<phi>\<^sub>1 \<phi>\<^sub>2)

goal (1 subgoal):
 1. x \<in> \<Union> {enc (w, I) |w I. length I = n \<and> wf_interp_for_formula (w, I) \<phi>\<^sub>1 \<and> (w, I) \<Turnstile> \<phi>\<^sub>1}
[PROOF STEP]
by (fastforce simp del: enc.simps)
[PROOF STATE]
proof (state)
this:
x \<in> lang\<^sub>W\<^sub>S\<^sub>1\<^sub>S n \<phi>\<^sub>1

goal (2 subgoals):
 1. \<lbrakk>x \<in> enc (w, I); wf_interp_for_formula (w, I) (FOr \<phi>\<^sub>1 \<phi>\<^sub>2); length I = n; (w, I) \<Turnstile> \<phi>\<^sub>1\<rbrakk> \<Longrightarrow> x \<in> (lang\<^sub>W\<^sub>S\<^sub>1\<^sub>S n \<phi>\<^sub>1 \<union> lang\<^sub>W\<^sub>S\<^sub>1\<^sub>S n \<phi>\<^sub>2) \<inter> \<Union> {enc (w, I) |w I. length I = n \<and> wf_interp_for_formula (w, I) (FOr \<phi>\<^sub>1 \<phi>\<^sub>2)}
 2. \<lbrakk>x \<in> enc (w, I); wf_interp_for_formula (w, I) (FOr \<phi>\<^sub>1 \<phi>\<^sub>2); length I = n; (w, I) \<Turnstile> \<phi>\<^sub>2\<rbrakk> \<Longrightarrow> x \<in> (lang\<^sub>W\<^sub>S\<^sub>1\<^sub>S n \<phi>\<^sub>1 \<union> lang\<^sub>W\<^sub>S\<^sub>1\<^sub>S n \<phi>\<^sub>2) \<inter> \<Union> {enc (w, I) |w I. length I = n \<and> wf_interp_for_formula (w, I) (FOr \<phi>\<^sub>1 \<phi>\<^sub>2)}
[PROOF STEP]
with *
[PROOF STATE]
proof (chain)
picking this:
x \<in> enc (w, I)
wf_interp_for_formula (w, I) (FOr \<phi>\<^sub>1 \<phi>\<^sub>2)
length I = n
x \<in> lang\<^sub>W\<^sub>S\<^sub>1\<^sub>S n \<phi>\<^sub>1
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
x \<in> enc (w, I)
wf_interp_for_formula (w, I) (FOr \<phi>\<^sub>1 \<phi>\<^sub>2)
length I = n
x \<in> lang\<^sub>W\<^sub>S\<^sub>1\<^sub>S n \<phi>\<^sub>1

goal (1 subgoal):
 1. x \<in> (lang\<^sub>W\<^sub>S\<^sub>1\<^sub>S n \<phi>\<^sub>1 \<union> lang\<^sub>W\<^sub>S\<^sub>1\<^sub>S n \<phi>\<^sub>2) \<inter> \<Union> {enc (w, I) |w I. length I = n \<and> wf_interp_for_formula (w, I) (FOr \<phi>\<^sub>1 \<phi>\<^sub>2)}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<in> (lang\<^sub>W\<^sub>S\<^sub>1\<^sub>S n \<phi>\<^sub>1 \<union> lang\<^sub>W\<^sub>S\<^sub>1\<^sub>S n \<phi>\<^sub>2) \<inter> \<Union> {enc (w, I) |w I. length I = n \<and> wf_interp_for_formula (w, I) (FOr \<phi>\<^sub>1 \<phi>\<^sub>2)}

goal (1 subgoal):
 1. \<lbrakk>x \<in> enc (w, I); wf_interp_for_formula (w, I) (FOr \<phi>\<^sub>1 \<phi>\<^sub>2); length I = n; (w, I) \<Turnstile> \<phi>\<^sub>2\<rbrakk> \<Longrightarrow> x \<in> (lang\<^sub>W\<^sub>S\<^sub>1\<^sub>S n \<phi>\<^sub>1 \<union> lang\<^sub>W\<^sub>S\<^sub>1\<^sub>S n \<phi>\<^sub>2) \<inter> \<Union> {enc (w, I) |w I. length I = n \<and> wf_interp_for_formula (w, I) (FOr \<phi>\<^sub>1 \<phi>\<^sub>2)}
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>x \<in> enc (w, I); wf_interp_for_formula (w, I) (FOr \<phi>\<^sub>1 \<phi>\<^sub>2); length I = n; (w, I) \<Turnstile> \<phi>\<^sub>2\<rbrakk> \<Longrightarrow> x \<in> (lang\<^sub>W\<^sub>S\<^sub>1\<^sub>S n \<phi>\<^sub>1 \<union> lang\<^sub>W\<^sub>S\<^sub>1\<^sub>S n \<phi>\<^sub>2) \<inter> \<Union> {enc (w, I) |w I. length I = n \<and> wf_interp_for_formula (w, I) (FOr \<phi>\<^sub>1 \<phi>\<^sub>2)}
[PROOF STEP]
assume "satisfies (w, I) \<phi>\<^sub>2"
[PROOF STATE]
proof (state)
this:
(w, I) \<Turnstile> \<phi>\<^sub>2

goal (1 subgoal):
 1. \<lbrakk>x \<in> enc (w, I); wf_interp_for_formula (w, I) (FOr \<phi>\<^sub>1 \<phi>\<^sub>2); length I = n; (w, I) \<Turnstile> \<phi>\<^sub>2\<rbrakk> \<Longrightarrow> x \<in> (lang\<^sub>W\<^sub>S\<^sub>1\<^sub>S n \<phi>\<^sub>1 \<union> lang\<^sub>W\<^sub>S\<^sub>1\<^sub>S n \<phi>\<^sub>2) \<inter> \<Union> {enc (w, I) |w I. length I = n \<and> wf_interp_for_formula (w, I) (FOr \<phi>\<^sub>1 \<phi>\<^sub>2)}
[PROOF STEP]
with *
[PROOF STATE]
proof (chain)
picking this:
x \<in> enc (w, I)
wf_interp_for_formula (w, I) (FOr \<phi>\<^sub>1 \<phi>\<^sub>2)
length I = n
(w, I) \<Turnstile> \<phi>\<^sub>2
[PROOF STEP]
have "x \<in>?L2"
[PROOF STATE]
proof (prove)
using this:
x \<in> enc (w, I)
wf_interp_for_formula (w, I) (FOr \<phi>\<^sub>1 \<phi>\<^sub>2)
length I = n
(w, I) \<Turnstile> \<phi>\<^sub>2

goal (1 subgoal):
 1. x \<in> lang\<^sub>W\<^sub>S\<^sub>1\<^sub>S n \<phi>\<^sub>2
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
x \<in> enc (w, I)
wf_interp_for_formula (w, I) (FOr \<phi>\<^sub>1 \<phi>\<^sub>2)
length I = n
(w, I) \<Turnstile> \<phi>\<^sub>2
wf_formula n (FOr \<phi>\<^sub>1 \<phi>\<^sub>2)

goal (1 subgoal):
 1. x \<in> lang\<^sub>W\<^sub>S\<^sub>1\<^sub>S n \<phi>\<^sub>2
[PROOF STEP]
unfolding lang\<^sub>W\<^sub>S\<^sub>1\<^sub>S_def
[PROOF STATE]
proof (prove)
using this:
x \<in> enc (w, I)
wf_interp_for_formula (w, I) (FOr \<phi>\<^sub>1 \<phi>\<^sub>2)
length I = n
(w, I) \<Turnstile> \<phi>\<^sub>2
wf_formula n (FOr \<phi>\<^sub>1 \<phi>\<^sub>2)

goal (1 subgoal):
 1. x \<in> \<Union> {enc (w, I) |w I. length I = n \<and> wf_interp_for_formula (w, I) \<phi>\<^sub>2 \<and> (w, I) \<Turnstile> \<phi>\<^sub>2}
[PROOF STEP]
by (fastforce simp del: enc.simps)
[PROOF STATE]
proof (state)
this:
x \<in> lang\<^sub>W\<^sub>S\<^sub>1\<^sub>S n \<phi>\<^sub>2

goal (1 subgoal):
 1. \<lbrakk>x \<in> enc (w, I); wf_interp_for_formula (w, I) (FOr \<phi>\<^sub>1 \<phi>\<^sub>2); length I = n; (w, I) \<Turnstile> \<phi>\<^sub>2\<rbrakk> \<Longrightarrow> x \<in> (lang\<^sub>W\<^sub>S\<^sub>1\<^sub>S n \<phi>\<^sub>1 \<union> lang\<^sub>W\<^sub>S\<^sub>1\<^sub>S n \<phi>\<^sub>2) \<inter> \<Union> {enc (w, I) |w I. length I = n \<and> wf_interp_for_formula (w, I) (FOr \<phi>\<^sub>1 \<phi>\<^sub>2)}
[PROOF STEP]
with *
[PROOF STATE]
proof (chain)
picking this:
x \<in> enc (w, I)
wf_interp_for_formula (w, I) (FOr \<phi>\<^sub>1 \<phi>\<^sub>2)
length I = n
x \<in> lang\<^sub>W\<^sub>S\<^sub>1\<^sub>S n \<phi>\<^sub>2
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
x \<in> enc (w, I)
wf_interp_for_formula (w, I) (FOr \<phi>\<^sub>1 \<phi>\<^sub>2)
length I = n
x \<in> lang\<^sub>W\<^sub>S\<^sub>1\<^sub>S n \<phi>\<^sub>2

goal (1 subgoal):
 1. x \<in> (lang\<^sub>W\<^sub>S\<^sub>1\<^sub>S n \<phi>\<^sub>1 \<union> lang\<^sub>W\<^sub>S\<^sub>1\<^sub>S n \<phi>\<^sub>2) \<inter> \<Union> {enc (w, I) |w I. length I = n \<and> wf_interp_for_formula (w, I) (FOr \<phi>\<^sub>1 \<phi>\<^sub>2)}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<in> (lang\<^sub>W\<^sub>S\<^sub>1\<^sub>S n \<phi>\<^sub>1 \<union> lang\<^sub>W\<^sub>S\<^sub>1\<^sub>S n \<phi>\<^sub>2) \<inter> \<Union> {enc (w, I) |w I. length I = n \<and> wf_interp_for_formula (w, I) (FOr \<phi>\<^sub>1 \<phi>\<^sub>2)}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
x \<in> (lang\<^sub>W\<^sub>S\<^sub>1\<^sub>S n \<phi>\<^sub>1 \<union> lang\<^sub>W\<^sub>S\<^sub>1\<^sub>S n \<phi>\<^sub>2) \<inter> \<Union> {enc (w, I) |w I. length I = n \<and> wf_interp_for_formula (w, I) (FOr \<phi>\<^sub>1 \<phi>\<^sub>2)}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma lang\<^sub>W\<^sub>S\<^sub>1\<^sub>S_FAnd:
  assumes "wf_formula n (FAnd \<phi>\<^sub>1 \<phi>\<^sub>2)"
  shows "lang\<^sub>W\<^sub>S\<^sub>1\<^sub>S n (FAnd \<phi>\<^sub>1 \<phi>\<^sub>2) \<subseteq>
    lang\<^sub>W\<^sub>S\<^sub>1\<^sub>S n \<phi>\<^sub>1 \<inter> lang\<^sub>W\<^sub>S\<^sub>1\<^sub>S n \<phi>\<^sub>2 \<inter> \<Union>{enc (w, I) | w I. length I = n \<and> wf_interp_for_formula (w, I) (FAnd \<phi>\<^sub>1 \<phi>\<^sub>2)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lang\<^sub>W\<^sub>S\<^sub>1\<^sub>S n (FAnd \<phi>\<^sub>1 \<phi>\<^sub>2) \<subseteq> lang\<^sub>W\<^sub>S\<^sub>1\<^sub>S n \<phi>\<^sub>1 \<inter> lang\<^sub>W\<^sub>S\<^sub>1\<^sub>S n \<phi>\<^sub>2 \<inter> \<Union> {enc (w, I) |w I. length I = n \<and> wf_interp_for_formula (w, I) (FAnd \<phi>\<^sub>1 \<phi>\<^sub>2)}
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
wf_formula n (FAnd \<phi>\<^sub>1 \<phi>\<^sub>2)

goal (1 subgoal):
 1. lang\<^sub>W\<^sub>S\<^sub>1\<^sub>S n (FAnd \<phi>\<^sub>1 \<phi>\<^sub>2) \<subseteq> lang\<^sub>W\<^sub>S\<^sub>1\<^sub>S n \<phi>\<^sub>1 \<inter> lang\<^sub>W\<^sub>S\<^sub>1\<^sub>S n \<phi>\<^sub>2 \<inter> \<Union> {enc (w, I) |w I. length I = n \<and> wf_interp_for_formula (w, I) (FAnd \<phi>\<^sub>1 \<phi>\<^sub>2)}
[PROOF STEP]
unfolding lang\<^sub>W\<^sub>S\<^sub>1\<^sub>S_def
[PROOF STATE]
proof (prove)
using this:
wf_formula n (FAnd \<phi>\<^sub>1 \<phi>\<^sub>2)

goal (1 subgoal):
 1. \<Union> {enc (w, I) |w I. length I = n \<and> wf_interp_for_formula (w, I) (FAnd \<phi>\<^sub>1 \<phi>\<^sub>2) \<and> (w, I) \<Turnstile> FAnd \<phi>\<^sub>1 \<phi>\<^sub>2} \<subseteq> \<Union> {enc (w, I) |w I. length I = n \<and> wf_interp_for_formula (w, I) \<phi>\<^sub>1 \<and> (w, I) \<Turnstile> \<phi>\<^sub>1} \<inter> \<Union> {enc (w, I) |w I. length I = n \<and> wf_interp_for_formula (w, I) \<phi>\<^sub>2 \<and> (w, I) \<Turnstile> \<phi>\<^sub>2} \<inter> \<Union> {enc (w, I) |w I. length I = n \<and> wf_interp_for_formula (w, I) (FAnd \<phi>\<^sub>1 \<phi>\<^sub>2)}
[PROOF STEP]
by (fastforce simp del: enc.simps)


[STATEMENT]
lemma enc_eqI:
  assumes "x \<in> enc (w, I)" "x \<in> enc (w', I')" "wf_interp_for_formula (w, I) \<phi>" "wf_interp_for_formula (w', I') \<phi>"
    "length I = length I'"
  shows "enc (w, I) = enc (w', I')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. enc (w, I) = enc (w', I')
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. enc (w, I) = enc (w', I')
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
x \<in> enc (w, I)
x \<in> enc (w', I')
wf_interp_for_formula (w, I) \<phi>
wf_interp_for_formula (w', I') \<phi>
length I = length I'
[PROOF STEP]
have "stream_enc (w, I) = stream_enc (w', I')"
[PROOF STATE]
proof (prove)
using this:
x \<in> enc (w, I)
x \<in> enc (w', I')
wf_interp_for_formula (w, I) \<phi>
wf_interp_for_formula (w', I') \<phi>
length I = length I'

goal (1 subgoal):
 1. stream_enc (w, I) = stream_enc (w', I')
[PROOF STEP]
by (intro box_equals[OF _ stream_enc_enc[symmetric] stream_enc_enc[symmetric]]) auto
[PROOF STATE]
proof (state)
this:
stream_enc (w, I) = stream_enc (w', I')

goal (1 subgoal):
 1. enc (w, I) = enc (w', I')
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
stream_enc (w, I) = stream_enc (w', I')

goal (1 subgoal):
 1. enc (w, I) = enc (w', I')
[PROOF STEP]
using assms(5)
[PROOF STATE]
proof (prove)
using this:
stream_enc (w, I) = stream_enc (w', I')
length I = length I'

goal (1 subgoal):
 1. enc (w, I) = enc (w', I')
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
enc (w, I) = enc (w', I')

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma enc_eq_welldef:
  "\<lbrakk>enc (w, I) = enc (w', I'); wf_formula (length I) \<phi>; wf_interp_for_formula (w, I) \<phi> ;wf_interp_for_formula (w', I') \<phi>\<rbrakk> \<Longrightarrow>
  (w, I) \<Turnstile> \<phi> \<longleftrightarrow> (w', I') \<Turnstile> \<phi>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>enc (w, I) = enc (w', I'); wf_formula (length I) \<phi>; wf_interp_for_formula (w, I) \<phi>; wf_interp_for_formula (w', I') \<phi>\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> \<phi>) = ((w', I') \<Turnstile> \<phi>)
[PROOF STEP]
by (intro stream_enc_welldef) (auto simp del: stream_enc.simps intro!: enc_stream_enc)


[STATEMENT]
lemma enc_welldef:
  "\<lbrakk>x \<in> enc (w, I); x \<in> enc (w', I'); length I = length I'; wf_formula (length I) \<phi>;
  wf_interp_for_formula (w, I) \<phi> ;wf_interp_for_formula (w', I') \<phi>\<rbrakk> \<Longrightarrow>
  (w, I) \<Turnstile> \<phi> \<longleftrightarrow> (w', I') \<Turnstile> \<phi>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> enc (w, I); x \<in> enc (w', I'); length I = length I'; wf_formula (length I) \<phi>; wf_interp_for_formula (w, I) \<phi>; wf_interp_for_formula (w', I') \<phi>\<rbrakk> \<Longrightarrow> ((w, I) \<Turnstile> \<phi>) = ((w', I') \<Turnstile> \<phi>)
[PROOF STEP]
by (intro enc_eq_welldef[OF enc_eqI])


[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]
by (induct \<phi> arbitrary: n)
    (auto intro!: wf_samequot_exec wf_rexp_ENC,
    auto simp: max_idx_vars finite_FOV)