[STATEMENT]
lemma lang\<^sub>W\<^sub>S\<^sub>1\<^sub>S_rexp_of_rexp_of':
  "wf_formula n \<phi> \<Longrightarrow> lang n (rexp_of n \<phi>) = lang n (rexp_of' n \<phi>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf_formula n \<phi> \<Longrightarrow> lang n (rexp_of n \<phi>) = lang n (rexp_of' n \<phi>)
[PROOF STEP]
unfolding rexp_of'_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf_formula n \<phi> \<Longrightarrow> lang n (rexp_of n \<phi>) = lang n (rexp.Inter (rexp_of_alt n \<phi>) (ENC n (FOV \<phi>)))
[PROOF STEP]
proof (induction \<phi> arbitrary: n)
[PROOF STATE]
proof (state)
goal (8 subgoals):
 1. \<And>x1 x2 n. wf_formula n (FQ x1 x2) \<Longrightarrow> lang n (rexp_of n (FQ x1 x2)) = lang n (rexp.Inter (rexp_of_alt n (FQ x1 x2)) (ENC n (FOV (FQ x1 x2))))
 2. \<And>x1 x2 n. wf_formula n (FLess x1 x2) \<Longrightarrow> lang n (rexp_of n (FLess x1 x2)) = lang n (rexp.Inter (rexp_of_alt n (FLess x1 x2)) (ENC n (FOV (FLess x1 x2))))
 3. \<And>x1 x2 n. wf_formula n (FIn x1 x2) \<Longrightarrow> lang n (rexp_of n (FIn x1 x2)) = lang n (rexp.Inter (rexp_of_alt n (FIn x1 x2)) (ENC n (FOV (FIn x1 x2))))
 4. \<And>\<phi> n. \<lbrakk>\<And>n. wf_formula n \<phi> \<Longrightarrow> lang n (rexp_of n \<phi>) = lang n (rexp.Inter (rexp_of_alt n \<phi>) (ENC n (FOV \<phi>))); wf_formula n (FNot \<phi>)\<rbrakk> \<Longrightarrow> lang n (rexp_of n (FNot \<phi>)) = lang n (rexp.Inter (rexp_of_alt n (FNot \<phi>)) (ENC n (FOV (FNot \<phi>))))
 5. \<And>\<phi>1 \<phi>2 n. \<lbrakk>\<And>n. wf_formula n \<phi>1 \<Longrightarrow> lang n (rexp_of n \<phi>1) = lang n (rexp.Inter (rexp_of_alt n \<phi>1) (ENC n (FOV \<phi>1))); \<And>n. wf_formula n \<phi>2 \<Longrightarrow> lang n (rexp_of n \<phi>2) = lang n (rexp.Inter (rexp_of_alt n \<phi>2) (ENC n (FOV \<phi>2))); wf_formula n (FOr \<phi>1 \<phi>2)\<rbrakk> \<Longrightarrow> lang n (rexp_of n (FOr \<phi>1 \<phi>2)) = lang n (rexp.Inter (rexp_of_alt n (FOr \<phi>1 \<phi>2)) (ENC n (FOV (FOr \<phi>1 \<phi>2))))
 6. \<And>\<phi>1 \<phi>2 n. \<lbrakk>\<And>n. wf_formula n \<phi>1 \<Longrightarrow> lang n (rexp_of n \<phi>1) = lang n (rexp.Inter (rexp_of_alt n \<phi>1) (ENC n (FOV \<phi>1))); \<And>n. wf_formula n \<phi>2 \<Longrightarrow> lang n (rexp_of n \<phi>2) = lang n (rexp.Inter (rexp_of_alt n \<phi>2) (ENC n (FOV \<phi>2))); wf_formula n (FAnd \<phi>1 \<phi>2)\<rbrakk> \<Longrightarrow> lang n (rexp_of n (FAnd \<phi>1 \<phi>2)) = lang n (rexp.Inter (rexp_of_alt n (FAnd \<phi>1 \<phi>2)) (ENC n (FOV (FAnd \<phi>1 \<phi>2))))
 7. \<And>\<phi> n. \<lbrakk>\<And>n. wf_formula n \<phi> \<Longrightarrow> lang n (rexp_of n \<phi>) = lang n (rexp.Inter (rexp_of_alt n \<phi>) (ENC n (FOV \<phi>))); wf_formula n (FExists \<phi>)\<rbrakk> \<Longrightarrow> lang n (rexp_of n (FExists \<phi>)) = lang n (rexp.Inter (rexp_of_alt n (FExists \<phi>)) (ENC n (FOV (FExists \<phi>))))
 8. \<And>\<phi> n. \<lbrakk>\<And>n. wf_formula n \<phi> \<Longrightarrow> lang n (rexp_of n \<phi>) = lang n (rexp.Inter (rexp_of_alt n \<phi>) (ENC n (FOV \<phi>))); wf_formula n (FEXISTS \<phi>)\<rbrakk> \<Longrightarrow> lang n (rexp_of n (FEXISTS \<phi>)) = lang n (rexp.Inter (rexp_of_alt n (FEXISTS \<phi>)) (ENC n (FOV (FEXISTS \<phi>))))
[PROOF STEP]
case (FNot \<phi>)
[PROOF STATE]
proof (state)
this:
wf_formula ?n2 \<phi> \<Longrightarrow> lang ?n2 (rexp_of ?n2 \<phi>) = lang ?n2 (rexp.Inter (rexp_of_alt ?n2 \<phi>) (ENC ?n2 (FOV \<phi>)))
wf_formula n (FNot \<phi>)

goal (8 subgoals):
 1. \<And>x1 x2 n. wf_formula n (FQ x1 x2) \<Longrightarrow> lang n (rexp_of n (FQ x1 x2)) = lang n (rexp.Inter (rexp_of_alt n (FQ x1 x2)) (ENC n (FOV (FQ x1 x2))))
 2. \<And>x1 x2 n. wf_formula n (FLess x1 x2) \<Longrightarrow> lang n (rexp_of n (FLess x1 x2)) = lang n (rexp.Inter (rexp_of_alt n (FLess x1 x2)) (ENC n (FOV (FLess x1 x2))))
 3. \<And>x1 x2 n. wf_formula n (FIn x1 x2) \<Longrightarrow> lang n (rexp_of n (FIn x1 x2)) = lang n (rexp.Inter (rexp_of_alt n (FIn x1 x2)) (ENC n (FOV (FIn x1 x2))))
 4. \<And>\<phi> n. \<lbrakk>\<And>n. wf_formula n \<phi> \<Longrightarrow> lang n (rexp_of n \<phi>) = lang n (rexp.Inter (rexp_of_alt n \<phi>) (ENC n (FOV \<phi>))); wf_formula n (FNot \<phi>)\<rbrakk> \<Longrightarrow> lang n (rexp_of n (FNot \<phi>)) = lang n (rexp.Inter (rexp_of_alt n (FNot \<phi>)) (ENC n (FOV (FNot \<phi>))))
 5. \<And>\<phi>1 \<phi>2 n. \<lbrakk>\<And>n. wf_formula n \<phi>1 \<Longrightarrow> lang n (rexp_of n \<phi>1) = lang n (rexp.Inter (rexp_of_alt n \<phi>1) (ENC n (FOV \<phi>1))); \<And>n. wf_formula n \<phi>2 \<Longrightarrow> lang n (rexp_of n \<phi>2) = lang n (rexp.Inter (rexp_of_alt n \<phi>2) (ENC n (FOV \<phi>2))); wf_formula n (FOr \<phi>1 \<phi>2)\<rbrakk> \<Longrightarrow> lang n (rexp_of n (FOr \<phi>1 \<phi>2)) = lang n (rexp.Inter (rexp_of_alt n (FOr \<phi>1 \<phi>2)) (ENC n (FOV (FOr \<phi>1 \<phi>2))))
 6. \<And>\<phi>1 \<phi>2 n. \<lbrakk>\<And>n. wf_formula n \<phi>1 \<Longrightarrow> lang n (rexp_of n \<phi>1) = lang n (rexp.Inter (rexp_of_alt n \<phi>1) (ENC n (FOV \<phi>1))); \<And>n. wf_formula n \<phi>2 \<Longrightarrow> lang n (rexp_of n \<phi>2) = lang n (rexp.Inter (rexp_of_alt n \<phi>2) (ENC n (FOV \<phi>2))); wf_formula n (FAnd \<phi>1 \<phi>2)\<rbrakk> \<Longrightarrow> lang n (rexp_of n (FAnd \<phi>1 \<phi>2)) = lang n (rexp.Inter (rexp_of_alt n (FAnd \<phi>1 \<phi>2)) (ENC n (FOV (FAnd \<phi>1 \<phi>2))))
 7. \<And>\<phi> n. \<lbrakk>\<And>n. wf_formula n \<phi> \<Longrightarrow> lang n (rexp_of n \<phi>) = lang n (rexp.Inter (rexp_of_alt n \<phi>) (ENC n (FOV \<phi>))); wf_formula n (FExists \<phi>)\<rbrakk> \<Longrightarrow> lang n (rexp_of n (FExists \<phi>)) = lang n (rexp.Inter (rexp_of_alt n (FExists \<phi>)) (ENC n (FOV (FExists \<phi>))))
 8. \<And>\<phi> n. \<lbrakk>\<And>n. wf_formula n \<phi> \<Longrightarrow> lang n (rexp_of n \<phi>) = lang n (rexp.Inter (rexp_of_alt n \<phi>) (ENC n (FOV \<phi>))); wf_formula n (FEXISTS \<phi>)\<rbrakk> \<Longrightarrow> lang n (rexp_of n (FEXISTS \<phi>)) = lang n (rexp.Inter (rexp_of_alt n (FEXISTS \<phi>)) (ENC n (FOV (FEXISTS \<phi>))))
[PROOF STEP]
hence "wf_formula n \<phi>"
[PROOF STATE]
proof (prove)
using this:
wf_formula ?n2 \<phi> \<Longrightarrow> lang ?n2 (rexp_of ?n2 \<phi>) = lang ?n2 (rexp.Inter (rexp_of_alt ?n2 \<phi>) (ENC ?n2 (FOV \<phi>)))
wf_formula n (FNot \<phi>)

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

goal (8 subgoals):
 1. \<And>x1 x2 n. wf_formula n (FQ x1 x2) \<Longrightarrow> lang n (rexp_of n (FQ x1 x2)) = lang n (rexp.Inter (rexp_of_alt n (FQ x1 x2)) (ENC n (FOV (FQ x1 x2))))
 2. \<And>x1 x2 n. wf_formula n (FLess x1 x2) \<Longrightarrow> lang n (rexp_of n (FLess x1 x2)) = lang n (rexp.Inter (rexp_of_alt n (FLess x1 x2)) (ENC n (FOV (FLess x1 x2))))
 3. \<And>x1 x2 n. wf_formula n (FIn x1 x2) \<Longrightarrow> lang n (rexp_of n (FIn x1 x2)) = lang n (rexp.Inter (rexp_of_alt n (FIn x1 x2)) (ENC n (FOV (FIn x1 x2))))
 4. \<And>\<phi> n. \<lbrakk>\<And>n. wf_formula n \<phi> \<Longrightarrow> lang n (rexp_of n \<phi>) = lang n (rexp.Inter (rexp_of_alt n \<phi>) (ENC n (FOV \<phi>))); wf_formula n (FNot \<phi>)\<rbrakk> \<Longrightarrow> lang n (rexp_of n (FNot \<phi>)) = lang n (rexp.Inter (rexp_of_alt n (FNot \<phi>)) (ENC n (FOV (FNot \<phi>))))
 5. \<And>\<phi>1 \<phi>2 n. \<lbrakk>\<And>n. wf_formula n \<phi>1 \<Longrightarrow> lang n (rexp_of n \<phi>1) = lang n (rexp.Inter (rexp_of_alt n \<phi>1) (ENC n (FOV \<phi>1))); \<And>n. wf_formula n \<phi>2 \<Longrightarrow> lang n (rexp_of n \<phi>2) = lang n (rexp.Inter (rexp_of_alt n \<phi>2) (ENC n (FOV \<phi>2))); wf_formula n (FOr \<phi>1 \<phi>2)\<rbrakk> \<Longrightarrow> lang n (rexp_of n (FOr \<phi>1 \<phi>2)) = lang n (rexp.Inter (rexp_of_alt n (FOr \<phi>1 \<phi>2)) (ENC n (FOV (FOr \<phi>1 \<phi>2))))
 6. \<And>\<phi>1 \<phi>2 n. \<lbrakk>\<And>n. wf_formula n \<phi>1 \<Longrightarrow> lang n (rexp_of n \<phi>1) = lang n (rexp.Inter (rexp_of_alt n \<phi>1) (ENC n (FOV \<phi>1))); \<And>n. wf_formula n \<phi>2 \<Longrightarrow> lang n (rexp_of n \<phi>2) = lang n (rexp.Inter (rexp_of_alt n \<phi>2) (ENC n (FOV \<phi>2))); wf_formula n (FAnd \<phi>1 \<phi>2)\<rbrakk> \<Longrightarrow> lang n (rexp_of n (FAnd \<phi>1 \<phi>2)) = lang n (rexp.Inter (rexp_of_alt n (FAnd \<phi>1 \<phi>2)) (ENC n (FOV (FAnd \<phi>1 \<phi>2))))
 7. \<And>\<phi> n. \<lbrakk>\<And>n. wf_formula n \<phi> \<Longrightarrow> lang n (rexp_of n \<phi>) = lang n (rexp.Inter (rexp_of_alt n \<phi>) (ENC n (FOV \<phi>))); wf_formula n (FExists \<phi>)\<rbrakk> \<Longrightarrow> lang n (rexp_of n (FExists \<phi>)) = lang n (rexp.Inter (rexp_of_alt n (FExists \<phi>)) (ENC n (FOV (FExists \<phi>))))
 8. \<And>\<phi> n. \<lbrakk>\<And>n. wf_formula n \<phi> \<Longrightarrow> lang n (rexp_of n \<phi>) = lang n (rexp.Inter (rexp_of_alt n \<phi>) (ENC n (FOV \<phi>))); wf_formula n (FEXISTS \<phi>)\<rbrakk> \<Longrightarrow> lang n (rexp_of n (FEXISTS \<phi>)) = lang n (rexp.Inter (rexp_of_alt n (FEXISTS \<phi>)) (ENC n (FOV (FEXISTS \<phi>))))
[PROOF STEP]
with FNot.IH
[PROOF STATE]
proof (chain)
picking this:
wf_formula ?n2 \<phi> \<Longrightarrow> lang ?n2 (rexp_of ?n2 \<phi>) = lang ?n2 (rexp.Inter (rexp_of_alt ?n2 \<phi>) (ENC ?n2 (FOV \<phi>)))
wf_formula n \<phi>
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
wf_formula ?n2 \<phi> \<Longrightarrow> lang ?n2 (rexp_of ?n2 \<phi>) = lang ?n2 (rexp.Inter (rexp_of_alt ?n2 \<phi>) (ENC ?n2 (FOV \<phi>)))
wf_formula n \<phi>

goal (1 subgoal):
 1. lang n (rexp_of n (FNot \<phi>)) = lang n (rexp.Inter (rexp_of_alt n (FNot \<phi>)) (ENC n (FOV (FNot \<phi>))))
[PROOF STEP]
unfolding rexp_of.simps rexp_of_alt.simps lang.simps ENC_FNot
[PROOF STATE]
proof (prove)
using this:
wf_formula ?n2 \<phi> \<Longrightarrow> lang ?n2 (rexp_of ?n2 \<phi>) = lang ?n2 (rexp_of_alt ?n2 \<phi>) \<inter> lang ?n2 (ENC ?n2 (FOV \<phi>))
wf_formula n \<phi>

goal (1 subgoal):
 1. (lists ((set \<circ> \<sigma> \<Sigma>) n) - lang n (rexp_of n \<phi>)) \<inter> lang n (ENC n (FOV \<phi>)) = (lists ((set \<circ> \<sigma> \<Sigma>) n) - lang n (rexp_of_alt n \<phi>)) \<inter> lang n (ENC n (FOV \<phi>))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
lang n (rexp_of n (FNot \<phi>)) = lang n (rexp.Inter (rexp_of_alt n (FNot \<phi>)) (ENC n (FOV (FNot \<phi>))))

goal (7 subgoals):
 1. \<And>x1 x2 n. wf_formula n (FQ x1 x2) \<Longrightarrow> lang n (rexp_of n (FQ x1 x2)) = lang n (rexp.Inter (rexp_of_alt n (FQ x1 x2)) (ENC n (FOV (FQ x1 x2))))
 2. \<And>x1 x2 n. wf_formula n (FLess x1 x2) \<Longrightarrow> lang n (rexp_of n (FLess x1 x2)) = lang n (rexp.Inter (rexp_of_alt n (FLess x1 x2)) (ENC n (FOV (FLess x1 x2))))
 3. \<And>x1 x2 n. wf_formula n (FIn x1 x2) \<Longrightarrow> lang n (rexp_of n (FIn x1 x2)) = lang n (rexp.Inter (rexp_of_alt n (FIn x1 x2)) (ENC n (FOV (FIn x1 x2))))
 4. \<And>\<phi>1 \<phi>2 n. \<lbrakk>\<And>n. wf_formula n \<phi>1 \<Longrightarrow> lang n (rexp_of n \<phi>1) = lang n (rexp.Inter (rexp_of_alt n \<phi>1) (ENC n (FOV \<phi>1))); \<And>n. wf_formula n \<phi>2 \<Longrightarrow> lang n (rexp_of n \<phi>2) = lang n (rexp.Inter (rexp_of_alt n \<phi>2) (ENC n (FOV \<phi>2))); wf_formula n (FOr \<phi>1 \<phi>2)\<rbrakk> \<Longrightarrow> lang n (rexp_of n (FOr \<phi>1 \<phi>2)) = lang n (rexp.Inter (rexp_of_alt n (FOr \<phi>1 \<phi>2)) (ENC n (FOV (FOr \<phi>1 \<phi>2))))
 5. \<And>\<phi>1 \<phi>2 n. \<lbrakk>\<And>n. wf_formula n \<phi>1 \<Longrightarrow> lang n (rexp_of n \<phi>1) = lang n (rexp.Inter (rexp_of_alt n \<phi>1) (ENC n (FOV \<phi>1))); \<And>n. wf_formula n \<phi>2 \<Longrightarrow> lang n (rexp_of n \<phi>2) = lang n (rexp.Inter (rexp_of_alt n \<phi>2) (ENC n (FOV \<phi>2))); wf_formula n (FAnd \<phi>1 \<phi>2)\<rbrakk> \<Longrightarrow> lang n (rexp_of n (FAnd \<phi>1 \<phi>2)) = lang n (rexp.Inter (rexp_of_alt n (FAnd \<phi>1 \<phi>2)) (ENC n (FOV (FAnd \<phi>1 \<phi>2))))
 6. \<And>\<phi> n. \<lbrakk>\<And>n. wf_formula n \<phi> \<Longrightarrow> lang n (rexp_of n \<phi>) = lang n (rexp.Inter (rexp_of_alt n \<phi>) (ENC n (FOV \<phi>))); wf_formula n (FExists \<phi>)\<rbrakk> \<Longrightarrow> lang n (rexp_of n (FExists \<phi>)) = lang n (rexp.Inter (rexp_of_alt n (FExists \<phi>)) (ENC n (FOV (FExists \<phi>))))
 7. \<And>\<phi> n. \<lbrakk>\<And>n. wf_formula n \<phi> \<Longrightarrow> lang n (rexp_of n \<phi>) = lang n (rexp.Inter (rexp_of_alt n \<phi>) (ENC n (FOV \<phi>))); wf_formula n (FEXISTS \<phi>)\<rbrakk> \<Longrightarrow> lang n (rexp_of n (FEXISTS \<phi>)) = lang n (rexp.Inter (rexp_of_alt n (FEXISTS \<phi>)) (ENC n (FOV (FEXISTS \<phi>))))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (7 subgoals):
 1. \<And>x1 x2 n. wf_formula n (FQ x1 x2) \<Longrightarrow> lang n (rexp_of n (FQ x1 x2)) = lang n (rexp.Inter (rexp_of_alt n (FQ x1 x2)) (ENC n (FOV (FQ x1 x2))))
 2. \<And>x1 x2 n. wf_formula n (FLess x1 x2) \<Longrightarrow> lang n (rexp_of n (FLess x1 x2)) = lang n (rexp.Inter (rexp_of_alt n (FLess x1 x2)) (ENC n (FOV (FLess x1 x2))))
 3. \<And>x1 x2 n. wf_formula n (FIn x1 x2) \<Longrightarrow> lang n (rexp_of n (FIn x1 x2)) = lang n (rexp.Inter (rexp_of_alt n (FIn x1 x2)) (ENC n (FOV (FIn x1 x2))))
 4. \<And>\<phi>1 \<phi>2 n. \<lbrakk>\<And>n. wf_formula n \<phi>1 \<Longrightarrow> lang n (rexp_of n \<phi>1) = lang n (rexp.Inter (rexp_of_alt n \<phi>1) (ENC n (FOV \<phi>1))); \<And>n. wf_formula n \<phi>2 \<Longrightarrow> lang n (rexp_of n \<phi>2) = lang n (rexp.Inter (rexp_of_alt n \<phi>2) (ENC n (FOV \<phi>2))); wf_formula n (FOr \<phi>1 \<phi>2)\<rbrakk> \<Longrightarrow> lang n (rexp_of n (FOr \<phi>1 \<phi>2)) = lang n (rexp.Inter (rexp_of_alt n (FOr \<phi>1 \<phi>2)) (ENC n (FOV (FOr \<phi>1 \<phi>2))))
 5. \<And>\<phi>1 \<phi>2 n. \<lbrakk>\<And>n. wf_formula n \<phi>1 \<Longrightarrow> lang n (rexp_of n \<phi>1) = lang n (rexp.Inter (rexp_of_alt n \<phi>1) (ENC n (FOV \<phi>1))); \<And>n. wf_formula n \<phi>2 \<Longrightarrow> lang n (rexp_of n \<phi>2) = lang n (rexp.Inter (rexp_of_alt n \<phi>2) (ENC n (FOV \<phi>2))); wf_formula n (FAnd \<phi>1 \<phi>2)\<rbrakk> \<Longrightarrow> lang n (rexp_of n (FAnd \<phi>1 \<phi>2)) = lang n (rexp.Inter (rexp_of_alt n (FAnd \<phi>1 \<phi>2)) (ENC n (FOV (FAnd \<phi>1 \<phi>2))))
 6. \<And>\<phi> n. \<lbrakk>\<And>n. wf_formula n \<phi> \<Longrightarrow> lang n (rexp_of n \<phi>) = lang n (rexp.Inter (rexp_of_alt n \<phi>) (ENC n (FOV \<phi>))); wf_formula n (FExists \<phi>)\<rbrakk> \<Longrightarrow> lang n (rexp_of n (FExists \<phi>)) = lang n (rexp.Inter (rexp_of_alt n (FExists \<phi>)) (ENC n (FOV (FExists \<phi>))))
 7. \<And>\<phi> n. \<lbrakk>\<And>n. wf_formula n \<phi> \<Longrightarrow> lang n (rexp_of n \<phi>) = lang n (rexp.Inter (rexp_of_alt n \<phi>) (ENC n (FOV \<phi>))); wf_formula n (FEXISTS \<phi>)\<rbrakk> \<Longrightarrow> lang n (rexp_of n (FEXISTS \<phi>)) = lang n (rexp.Inter (rexp_of_alt n (FEXISTS \<phi>)) (ENC n (FOV (FEXISTS \<phi>))))
[PROOF STEP]
case (FAnd \<phi>\<^sub>1 \<phi>\<^sub>2)
[PROOF STATE]
proof (state)
this:
wf_formula ?n2 \<phi>\<^sub>1 \<Longrightarrow> lang ?n2 (rexp_of ?n2 \<phi>\<^sub>1) = lang ?n2 (rexp.Inter (rexp_of_alt ?n2 \<phi>\<^sub>1) (ENC ?n2 (FOV \<phi>\<^sub>1)))
wf_formula ?n2 \<phi>\<^sub>2 \<Longrightarrow> lang ?n2 (rexp_of ?n2 \<phi>\<^sub>2) = lang ?n2 (rexp.Inter (rexp_of_alt ?n2 \<phi>\<^sub>2) (ENC ?n2 (FOV \<phi>\<^sub>2)))
wf_formula n (FAnd \<phi>\<^sub>1 \<phi>\<^sub>2)

goal (7 subgoals):
 1. \<And>x1 x2 n. wf_formula n (FQ x1 x2) \<Longrightarrow> lang n (rexp_of n (FQ x1 x2)) = lang n (rexp.Inter (rexp_of_alt n (FQ x1 x2)) (ENC n (FOV (FQ x1 x2))))
 2. \<And>x1 x2 n. wf_formula n (FLess x1 x2) \<Longrightarrow> lang n (rexp_of n (FLess x1 x2)) = lang n (rexp.Inter (rexp_of_alt n (FLess x1 x2)) (ENC n (FOV (FLess x1 x2))))
 3. \<And>x1 x2 n. wf_formula n (FIn x1 x2) \<Longrightarrow> lang n (rexp_of n (FIn x1 x2)) = lang n (rexp.Inter (rexp_of_alt n (FIn x1 x2)) (ENC n (FOV (FIn x1 x2))))
 4. \<And>\<phi>1 \<phi>2 n. \<lbrakk>\<And>n. wf_formula n \<phi>1 \<Longrightarrow> lang n (rexp_of n \<phi>1) = lang n (rexp.Inter (rexp_of_alt n \<phi>1) (ENC n (FOV \<phi>1))); \<And>n. wf_formula n \<phi>2 \<Longrightarrow> lang n (rexp_of n \<phi>2) = lang n (rexp.Inter (rexp_of_alt n \<phi>2) (ENC n (FOV \<phi>2))); wf_formula n (FOr \<phi>1 \<phi>2)\<rbrakk> \<Longrightarrow> lang n (rexp_of n (FOr \<phi>1 \<phi>2)) = lang n (rexp.Inter (rexp_of_alt n (FOr \<phi>1 \<phi>2)) (ENC n (FOV (FOr \<phi>1 \<phi>2))))
 5. \<And>\<phi>1 \<phi>2 n. \<lbrakk>\<And>n. wf_formula n \<phi>1 \<Longrightarrow> lang n (rexp_of n \<phi>1) = lang n (rexp.Inter (rexp_of_alt n \<phi>1) (ENC n (FOV \<phi>1))); \<And>n. wf_formula n \<phi>2 \<Longrightarrow> lang n (rexp_of n \<phi>2) = lang n (rexp.Inter (rexp_of_alt n \<phi>2) (ENC n (FOV \<phi>2))); wf_formula n (FAnd \<phi>1 \<phi>2)\<rbrakk> \<Longrightarrow> lang n (rexp_of n (FAnd \<phi>1 \<phi>2)) = lang n (rexp.Inter (rexp_of_alt n (FAnd \<phi>1 \<phi>2)) (ENC n (FOV (FAnd \<phi>1 \<phi>2))))
 6. \<And>\<phi> n. \<lbrakk>\<And>n. wf_formula n \<phi> \<Longrightarrow> lang n (rexp_of n \<phi>) = lang n (rexp.Inter (rexp_of_alt n \<phi>) (ENC n (FOV \<phi>))); wf_formula n (FExists \<phi>)\<rbrakk> \<Longrightarrow> lang n (rexp_of n (FExists \<phi>)) = lang n (rexp.Inter (rexp_of_alt n (FExists \<phi>)) (ENC n (FOV (FExists \<phi>))))
 7. \<And>\<phi> n. \<lbrakk>\<And>n. wf_formula n \<phi> \<Longrightarrow> lang n (rexp_of n \<phi>) = lang n (rexp.Inter (rexp_of_alt n \<phi>) (ENC n (FOV \<phi>))); wf_formula n (FEXISTS \<phi>)\<rbrakk> \<Longrightarrow> lang n (rexp_of n (FEXISTS \<phi>)) = lang n (rexp.Inter (rexp_of_alt n (FEXISTS \<phi>)) (ENC n (FOV (FEXISTS \<phi>))))
[PROOF STEP]
hence wf1: "wf_formula n \<phi>\<^sub>1" and wf2: "wf_formula n \<phi>\<^sub>2"
[PROOF STATE]
proof (prove)
using this:
wf_formula ?n2 \<phi>\<^sub>1 \<Longrightarrow> lang ?n2 (rexp_of ?n2 \<phi>\<^sub>1) = lang ?n2 (rexp.Inter (rexp_of_alt ?n2 \<phi>\<^sub>1) (ENC ?n2 (FOV \<phi>\<^sub>1)))
wf_formula ?n2 \<phi>\<^sub>2 \<Longrightarrow> lang ?n2 (rexp_of ?n2 \<phi>\<^sub>2) = lang ?n2 (rexp.Inter (rexp_of_alt ?n2 \<phi>\<^sub>2) (ENC ?n2 (FOV \<phi>\<^sub>2)))
wf_formula n (FAnd \<phi>\<^sub>1 \<phi>\<^sub>2)

goal (1 subgoal):
 1. wf_formula n \<phi>\<^sub>1 &&& wf_formula n \<phi>\<^sub>2
[PROOF STEP]
by force+
[PROOF STATE]
proof (state)
this:
wf_formula n \<phi>\<^sub>1
wf_formula n \<phi>\<^sub>2

goal (7 subgoals):
 1. \<And>x1 x2 n. wf_formula n (FQ x1 x2) \<Longrightarrow> lang n (rexp_of n (FQ x1 x2)) = lang n (rexp.Inter (rexp_of_alt n (FQ x1 x2)) (ENC n (FOV (FQ x1 x2))))
 2. \<And>x1 x2 n. wf_formula n (FLess x1 x2) \<Longrightarrow> lang n (rexp_of n (FLess x1 x2)) = lang n (rexp.Inter (rexp_of_alt n (FLess x1 x2)) (ENC n (FOV (FLess x1 x2))))
 3. \<And>x1 x2 n. wf_formula n (FIn x1 x2) \<Longrightarrow> lang n (rexp_of n (FIn x1 x2)) = lang n (rexp.Inter (rexp_of_alt n (FIn x1 x2)) (ENC n (FOV (FIn x1 x2))))
 4. \<And>\<phi>1 \<phi>2 n. \<lbrakk>\<And>n. wf_formula n \<phi>1 \<Longrightarrow> lang n (rexp_of n \<phi>1) = lang n (rexp.Inter (rexp_of_alt n \<phi>1) (ENC n (FOV \<phi>1))); \<And>n. wf_formula n \<phi>2 \<Longrightarrow> lang n (rexp_of n \<phi>2) = lang n (rexp.Inter (rexp_of_alt n \<phi>2) (ENC n (FOV \<phi>2))); wf_formula n (FOr \<phi>1 \<phi>2)\<rbrakk> \<Longrightarrow> lang n (rexp_of n (FOr \<phi>1 \<phi>2)) = lang n (rexp.Inter (rexp_of_alt n (FOr \<phi>1 \<phi>2)) (ENC n (FOV (FOr \<phi>1 \<phi>2))))
 5. \<And>\<phi>1 \<phi>2 n. \<lbrakk>\<And>n. wf_formula n \<phi>1 \<Longrightarrow> lang n (rexp_of n \<phi>1) = lang n (rexp.Inter (rexp_of_alt n \<phi>1) (ENC n (FOV \<phi>1))); \<And>n. wf_formula n \<phi>2 \<Longrightarrow> lang n (rexp_of n \<phi>2) = lang n (rexp.Inter (rexp_of_alt n \<phi>2) (ENC n (FOV \<phi>2))); wf_formula n (FAnd \<phi>1 \<phi>2)\<rbrakk> \<Longrightarrow> lang n (rexp_of n (FAnd \<phi>1 \<phi>2)) = lang n (rexp.Inter (rexp_of_alt n (FAnd \<phi>1 \<phi>2)) (ENC n (FOV (FAnd \<phi>1 \<phi>2))))
 6. \<And>\<phi> n. \<lbrakk>\<And>n. wf_formula n \<phi> \<Longrightarrow> lang n (rexp_of n \<phi>) = lang n (rexp.Inter (rexp_of_alt n \<phi>) (ENC n (FOV \<phi>))); wf_formula n (FExists \<phi>)\<rbrakk> \<Longrightarrow> lang n (rexp_of n (FExists \<phi>)) = lang n (rexp.Inter (rexp_of_alt n (FExists \<phi>)) (ENC n (FOV (FExists \<phi>))))
 7. \<And>\<phi> n. \<lbrakk>\<And>n. wf_formula n \<phi> \<Longrightarrow> lang n (rexp_of n \<phi>) = lang n (rexp.Inter (rexp_of_alt n \<phi>) (ENC n (FOV \<phi>))); wf_formula n (FEXISTS \<phi>)\<rbrakk> \<Longrightarrow> lang n (rexp_of n (FEXISTS \<phi>)) = lang n (rexp.Inter (rexp_of_alt n (FEXISTS \<phi>)) (ENC n (FOV (FEXISTS \<phi>))))
[PROOF STEP]
from FAnd.IH(1)[OF wf1] FAnd.IH(2)[OF wf2]
[PROOF STATE]
proof (chain)
picking this:
lang n (rexp_of n \<phi>\<^sub>1) = lang n (rexp.Inter (rexp_of_alt n \<phi>\<^sub>1) (ENC n (FOV \<phi>\<^sub>1)))
lang n (rexp_of n \<phi>\<^sub>2) = lang n (rexp.Inter (rexp_of_alt n \<phi>\<^sub>2) (ENC n (FOV \<phi>\<^sub>2)))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
lang n (rexp_of n \<phi>\<^sub>1) = lang n (rexp.Inter (rexp_of_alt n \<phi>\<^sub>1) (ENC n (FOV \<phi>\<^sub>1)))
lang n (rexp_of n \<phi>\<^sub>2) = lang n (rexp.Inter (rexp_of_alt n \<phi>\<^sub>2) (ENC n (FOV \<phi>\<^sub>2)))

goal (1 subgoal):
 1. lang n (rexp_of n (FAnd \<phi>\<^sub>1 \<phi>\<^sub>2)) = lang n (rexp.Inter (rexp_of_alt n (FAnd \<phi>\<^sub>1 \<phi>\<^sub>2)) (ENC n (FOV (FAnd \<phi>\<^sub>1 \<phi>\<^sub>2))))
[PROOF STEP]
using ENC_FAnd[OF FAnd.prems]
[PROOF STATE]
proof (prove)
using this:
lang n (rexp_of n \<phi>\<^sub>1) = lang n (rexp.Inter (rexp_of_alt n \<phi>\<^sub>1) (ENC n (FOV \<phi>\<^sub>1)))
lang n (rexp_of n \<phi>\<^sub>2) = lang n (rexp.Inter (rexp_of_alt n \<phi>\<^sub>2) (ENC n (FOV \<phi>\<^sub>2)))
lang n (ENC n (FOV (FAnd \<phi>\<^sub>1 \<phi>\<^sub>2))) \<subseteq> lang n (ENC n (FOV \<phi>\<^sub>1)) \<inter> lang n (ENC n (FOV \<phi>\<^sub>2))

goal (1 subgoal):
 1. lang n (rexp_of n (FAnd \<phi>\<^sub>1 \<phi>\<^sub>2)) = lang n (rexp.Inter (rexp_of_alt n (FAnd \<phi>\<^sub>1 \<phi>\<^sub>2)) (ENC n (FOV (FAnd \<phi>\<^sub>1 \<phi>\<^sub>2))))
[PROOF STEP]
unfolding rexp_of.simps rexp_of_alt.simps lang.simps rexp_of_list.simps
[PROOF STATE]
proof (prove)
using this:
lang n (rexp_of n \<phi>\<^sub>1) = lang n (rexp_of_alt n \<phi>\<^sub>1) \<inter> lang n (ENC n (FOV \<phi>\<^sub>1))
lang n (rexp_of n \<phi>\<^sub>2) = lang n (rexp_of_alt n \<phi>\<^sub>2) \<inter> lang n (ENC n (FOV \<phi>\<^sub>2))
lang n (ENC n (FOV (FAnd \<phi>\<^sub>1 \<phi>\<^sub>2))) \<subseteq> lang n (ENC n (FOV \<phi>\<^sub>1)) \<inter> lang n (ENC n (FOV \<phi>\<^sub>2))

goal (1 subgoal):
 1. lang n (rexp_of n \<phi>\<^sub>1) \<inter> (lang n (rexp_of n \<phi>\<^sub>2) \<inter> lang n (ENC n (FOV (FAnd \<phi>\<^sub>1 \<phi>\<^sub>2)))) = lang n (rexp_of_alt n \<phi>\<^sub>1) \<inter> lang n (rexp_of_alt n \<phi>\<^sub>2) \<inter> lang n (ENC n (FOV (FAnd \<phi>\<^sub>1 \<phi>\<^sub>2)))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
lang n (rexp_of n (FAnd \<phi>\<^sub>1 \<phi>\<^sub>2)) = lang n (rexp.Inter (rexp_of_alt n (FAnd \<phi>\<^sub>1 \<phi>\<^sub>2)) (ENC n (FOV (FAnd \<phi>\<^sub>1 \<phi>\<^sub>2))))

goal (6 subgoals):
 1. \<And>x1 x2 n. wf_formula n (FQ x1 x2) \<Longrightarrow> lang n (rexp_of n (FQ x1 x2)) = lang n (rexp.Inter (rexp_of_alt n (FQ x1 x2)) (ENC n (FOV (FQ x1 x2))))
 2. \<And>x1 x2 n. wf_formula n (FLess x1 x2) \<Longrightarrow> lang n (rexp_of n (FLess x1 x2)) = lang n (rexp.Inter (rexp_of_alt n (FLess x1 x2)) (ENC n (FOV (FLess x1 x2))))
 3. \<And>x1 x2 n. wf_formula n (FIn x1 x2) \<Longrightarrow> lang n (rexp_of n (FIn x1 x2)) = lang n (rexp.Inter (rexp_of_alt n (FIn x1 x2)) (ENC n (FOV (FIn x1 x2))))
 4. \<And>\<phi>1 \<phi>2 n. \<lbrakk>\<And>n. wf_formula n \<phi>1 \<Longrightarrow> lang n (rexp_of n \<phi>1) = lang n (rexp.Inter (rexp_of_alt n \<phi>1) (ENC n (FOV \<phi>1))); \<And>n. wf_formula n \<phi>2 \<Longrightarrow> lang n (rexp_of n \<phi>2) = lang n (rexp.Inter (rexp_of_alt n \<phi>2) (ENC n (FOV \<phi>2))); wf_formula n (FOr \<phi>1 \<phi>2)\<rbrakk> \<Longrightarrow> lang n (rexp_of n (FOr \<phi>1 \<phi>2)) = lang n (rexp.Inter (rexp_of_alt n (FOr \<phi>1 \<phi>2)) (ENC n (FOV (FOr \<phi>1 \<phi>2))))
 5. \<And>\<phi> n. \<lbrakk>\<And>n. wf_formula n \<phi> \<Longrightarrow> lang n (rexp_of n \<phi>) = lang n (rexp.Inter (rexp_of_alt n \<phi>) (ENC n (FOV \<phi>))); wf_formula n (FExists \<phi>)\<rbrakk> \<Longrightarrow> lang n (rexp_of n (FExists \<phi>)) = lang n (rexp.Inter (rexp_of_alt n (FExists \<phi>)) (ENC n (FOV (FExists \<phi>))))
 6. \<And>\<phi> n. \<lbrakk>\<And>n. wf_formula n \<phi> \<Longrightarrow> lang n (rexp_of n \<phi>) = lang n (rexp.Inter (rexp_of_alt n \<phi>) (ENC n (FOV \<phi>))); wf_formula n (FEXISTS \<phi>)\<rbrakk> \<Longrightarrow> lang n (rexp_of n (FEXISTS \<phi>)) = lang n (rexp.Inter (rexp_of_alt n (FEXISTS \<phi>)) (ENC n (FOV (FEXISTS \<phi>))))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. \<And>x1 x2 n. wf_formula n (FQ x1 x2) \<Longrightarrow> lang n (rexp_of n (FQ x1 x2)) = lang n (rexp.Inter (rexp_of_alt n (FQ x1 x2)) (ENC n (FOV (FQ x1 x2))))
 2. \<And>x1 x2 n. wf_formula n (FLess x1 x2) \<Longrightarrow> lang n (rexp_of n (FLess x1 x2)) = lang n (rexp.Inter (rexp_of_alt n (FLess x1 x2)) (ENC n (FOV (FLess x1 x2))))
 3. \<And>x1 x2 n. wf_formula n (FIn x1 x2) \<Longrightarrow> lang n (rexp_of n (FIn x1 x2)) = lang n (rexp.Inter (rexp_of_alt n (FIn x1 x2)) (ENC n (FOV (FIn x1 x2))))
 4. \<And>\<phi>1 \<phi>2 n. \<lbrakk>\<And>n. wf_formula n \<phi>1 \<Longrightarrow> lang n (rexp_of n \<phi>1) = lang n (rexp.Inter (rexp_of_alt n \<phi>1) (ENC n (FOV \<phi>1))); \<And>n. wf_formula n \<phi>2 \<Longrightarrow> lang n (rexp_of n \<phi>2) = lang n (rexp.Inter (rexp_of_alt n \<phi>2) (ENC n (FOV \<phi>2))); wf_formula n (FOr \<phi>1 \<phi>2)\<rbrakk> \<Longrightarrow> lang n (rexp_of n (FOr \<phi>1 \<phi>2)) = lang n (rexp.Inter (rexp_of_alt n (FOr \<phi>1 \<phi>2)) (ENC n (FOV (FOr \<phi>1 \<phi>2))))
 5. \<And>\<phi> n. \<lbrakk>\<And>n. wf_formula n \<phi> \<Longrightarrow> lang n (rexp_of n \<phi>) = lang n (rexp.Inter (rexp_of_alt n \<phi>) (ENC n (FOV \<phi>))); wf_formula n (FExists \<phi>)\<rbrakk> \<Longrightarrow> lang n (rexp_of n (FExists \<phi>)) = lang n (rexp.Inter (rexp_of_alt n (FExists \<phi>)) (ENC n (FOV (FExists \<phi>))))
 6. \<And>\<phi> n. \<lbrakk>\<And>n. wf_formula n \<phi> \<Longrightarrow> lang n (rexp_of n \<phi>) = lang n (rexp.Inter (rexp_of_alt n \<phi>) (ENC n (FOV \<phi>))); wf_formula n (FEXISTS \<phi>)\<rbrakk> \<Longrightarrow> lang n (rexp_of n (FEXISTS \<phi>)) = lang n (rexp.Inter (rexp_of_alt n (FEXISTS \<phi>)) (ENC n (FOV (FEXISTS \<phi>))))
[PROOF STEP]
case (FOr \<phi>\<^sub>1 \<phi>\<^sub>2)
[PROOF STATE]
proof (state)
this:
wf_formula ?n2 \<phi>\<^sub>1 \<Longrightarrow> lang ?n2 (rexp_of ?n2 \<phi>\<^sub>1) = lang ?n2 (rexp.Inter (rexp_of_alt ?n2 \<phi>\<^sub>1) (ENC ?n2 (FOV \<phi>\<^sub>1)))
wf_formula ?n2 \<phi>\<^sub>2 \<Longrightarrow> lang ?n2 (rexp_of ?n2 \<phi>\<^sub>2) = lang ?n2 (rexp.Inter (rexp_of_alt ?n2 \<phi>\<^sub>2) (ENC ?n2 (FOV \<phi>\<^sub>2)))
wf_formula n (FOr \<phi>\<^sub>1 \<phi>\<^sub>2)

goal (6 subgoals):
 1. \<And>x1 x2 n. wf_formula n (FQ x1 x2) \<Longrightarrow> lang n (rexp_of n (FQ x1 x2)) = lang n (rexp.Inter (rexp_of_alt n (FQ x1 x2)) (ENC n (FOV (FQ x1 x2))))
 2. \<And>x1 x2 n. wf_formula n (FLess x1 x2) \<Longrightarrow> lang n (rexp_of n (FLess x1 x2)) = lang n (rexp.Inter (rexp_of_alt n (FLess x1 x2)) (ENC n (FOV (FLess x1 x2))))
 3. \<And>x1 x2 n. wf_formula n (FIn x1 x2) \<Longrightarrow> lang n (rexp_of n (FIn x1 x2)) = lang n (rexp.Inter (rexp_of_alt n (FIn x1 x2)) (ENC n (FOV (FIn x1 x2))))
 4. \<And>\<phi>1 \<phi>2 n. \<lbrakk>\<And>n. wf_formula n \<phi>1 \<Longrightarrow> lang n (rexp_of n \<phi>1) = lang n (rexp.Inter (rexp_of_alt n \<phi>1) (ENC n (FOV \<phi>1))); \<And>n. wf_formula n \<phi>2 \<Longrightarrow> lang n (rexp_of n \<phi>2) = lang n (rexp.Inter (rexp_of_alt n \<phi>2) (ENC n (FOV \<phi>2))); wf_formula n (FOr \<phi>1 \<phi>2)\<rbrakk> \<Longrightarrow> lang n (rexp_of n (FOr \<phi>1 \<phi>2)) = lang n (rexp.Inter (rexp_of_alt n (FOr \<phi>1 \<phi>2)) (ENC n (FOV (FOr \<phi>1 \<phi>2))))
 5. \<And>\<phi> n. \<lbrakk>\<And>n. wf_formula n \<phi> \<Longrightarrow> lang n (rexp_of n \<phi>) = lang n (rexp.Inter (rexp_of_alt n \<phi>) (ENC n (FOV \<phi>))); wf_formula n (FExists \<phi>)\<rbrakk> \<Longrightarrow> lang n (rexp_of n (FExists \<phi>)) = lang n (rexp.Inter (rexp_of_alt n (FExists \<phi>)) (ENC n (FOV (FExists \<phi>))))
 6. \<And>\<phi> n. \<lbrakk>\<And>n. wf_formula n \<phi> \<Longrightarrow> lang n (rexp_of n \<phi>) = lang n (rexp.Inter (rexp_of_alt n \<phi>) (ENC n (FOV \<phi>))); wf_formula n (FEXISTS \<phi>)\<rbrakk> \<Longrightarrow> lang n (rexp_of n (FEXISTS \<phi>)) = lang n (rexp.Inter (rexp_of_alt n (FEXISTS \<phi>)) (ENC n (FOV (FEXISTS \<phi>))))
[PROOF STEP]
hence wf1: "wf_formula n \<phi>\<^sub>1" and wf2: "wf_formula n \<phi>\<^sub>2"
[PROOF STATE]
proof (prove)
using this:
wf_formula ?n2 \<phi>\<^sub>1 \<Longrightarrow> lang ?n2 (rexp_of ?n2 \<phi>\<^sub>1) = lang ?n2 (rexp.Inter (rexp_of_alt ?n2 \<phi>\<^sub>1) (ENC ?n2 (FOV \<phi>\<^sub>1)))
wf_formula ?n2 \<phi>\<^sub>2 \<Longrightarrow> lang ?n2 (rexp_of ?n2 \<phi>\<^sub>2) = lang ?n2 (rexp.Inter (rexp_of_alt ?n2 \<phi>\<^sub>2) (ENC ?n2 (FOV \<phi>\<^sub>2)))
wf_formula n (FOr \<phi>\<^sub>1 \<phi>\<^sub>2)

goal (1 subgoal):
 1. wf_formula n \<phi>\<^sub>1 &&& wf_formula n \<phi>\<^sub>2
[PROOF STEP]
by force+
[PROOF STATE]
proof (state)
this:
wf_formula n \<phi>\<^sub>1
wf_formula n \<phi>\<^sub>2

goal (6 subgoals):
 1. \<And>x1 x2 n. wf_formula n (FQ x1 x2) \<Longrightarrow> lang n (rexp_of n (FQ x1 x2)) = lang n (rexp.Inter (rexp_of_alt n (FQ x1 x2)) (ENC n (FOV (FQ x1 x2))))
 2. \<And>x1 x2 n. wf_formula n (FLess x1 x2) \<Longrightarrow> lang n (rexp_of n (FLess x1 x2)) = lang n (rexp.Inter (rexp_of_alt n (FLess x1 x2)) (ENC n (FOV (FLess x1 x2))))
 3. \<And>x1 x2 n. wf_formula n (FIn x1 x2) \<Longrightarrow> lang n (rexp_of n (FIn x1 x2)) = lang n (rexp.Inter (rexp_of_alt n (FIn x1 x2)) (ENC n (FOV (FIn x1 x2))))
 4. \<And>\<phi>1 \<phi>2 n. \<lbrakk>\<And>n. wf_formula n \<phi>1 \<Longrightarrow> lang n (rexp_of n \<phi>1) = lang n (rexp.Inter (rexp_of_alt n \<phi>1) (ENC n (FOV \<phi>1))); \<And>n. wf_formula n \<phi>2 \<Longrightarrow> lang n (rexp_of n \<phi>2) = lang n (rexp.Inter (rexp_of_alt n \<phi>2) (ENC n (FOV \<phi>2))); wf_formula n (FOr \<phi>1 \<phi>2)\<rbrakk> \<Longrightarrow> lang n (rexp_of n (FOr \<phi>1 \<phi>2)) = lang n (rexp.Inter (rexp_of_alt n (FOr \<phi>1 \<phi>2)) (ENC n (FOV (FOr \<phi>1 \<phi>2))))
 5. \<And>\<phi> n. \<lbrakk>\<And>n. wf_formula n \<phi> \<Longrightarrow> lang n (rexp_of n \<phi>) = lang n (rexp.Inter (rexp_of_alt n \<phi>) (ENC n (FOV \<phi>))); wf_formula n (FExists \<phi>)\<rbrakk> \<Longrightarrow> lang n (rexp_of n (FExists \<phi>)) = lang n (rexp.Inter (rexp_of_alt n (FExists \<phi>)) (ENC n (FOV (FExists \<phi>))))
 6. \<And>\<phi> n. \<lbrakk>\<And>n. wf_formula n \<phi> \<Longrightarrow> lang n (rexp_of n \<phi>) = lang n (rexp.Inter (rexp_of_alt n \<phi>) (ENC n (FOV \<phi>))); wf_formula n (FEXISTS \<phi>)\<rbrakk> \<Longrightarrow> lang n (rexp_of n (FEXISTS \<phi>)) = lang n (rexp.Inter (rexp_of_alt n (FEXISTS \<phi>)) (ENC n (FOV (FEXISTS \<phi>))))
[PROOF STEP]
from FOr.IH(1)[OF wf1] FOr.IH(2)[OF wf2]
[PROOF STATE]
proof (chain)
picking this:
lang n (rexp_of n \<phi>\<^sub>1) = lang n (rexp.Inter (rexp_of_alt n \<phi>\<^sub>1) (ENC n (FOV \<phi>\<^sub>1)))
lang n (rexp_of n \<phi>\<^sub>2) = lang n (rexp.Inter (rexp_of_alt n \<phi>\<^sub>2) (ENC n (FOV \<phi>\<^sub>2)))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
lang n (rexp_of n \<phi>\<^sub>1) = lang n (rexp.Inter (rexp_of_alt n \<phi>\<^sub>1) (ENC n (FOV \<phi>\<^sub>1)))
lang n (rexp_of n \<phi>\<^sub>2) = lang n (rexp.Inter (rexp_of_alt n \<phi>\<^sub>2) (ENC n (FOV \<phi>\<^sub>2)))

goal (1 subgoal):
 1. lang n (rexp_of n (FOr \<phi>\<^sub>1 \<phi>\<^sub>2)) = lang n (rexp.Inter (rexp_of_alt n (FOr \<phi>\<^sub>1 \<phi>\<^sub>2)) (ENC n (FOV (FOr \<phi>\<^sub>1 \<phi>\<^sub>2))))
[PROOF STEP]
using ENC_FOr[OF FOr.prems]
[PROOF STATE]
proof (prove)
using this:
lang n (rexp_of n \<phi>\<^sub>1) = lang n (rexp.Inter (rexp_of_alt n \<phi>\<^sub>1) (ENC n (FOV \<phi>\<^sub>1)))
lang n (rexp_of n \<phi>\<^sub>2) = lang n (rexp.Inter (rexp_of_alt n \<phi>\<^sub>2) (ENC n (FOV \<phi>\<^sub>2)))
lang n (ENC n (FOV (FOr \<phi>\<^sub>1 \<phi>\<^sub>2))) \<subseteq> lang n (ENC n (FOV \<phi>\<^sub>1)) \<inter> lang n (ENC n (FOV \<phi>\<^sub>2))

goal (1 subgoal):
 1. lang n (rexp_of n (FOr \<phi>\<^sub>1 \<phi>\<^sub>2)) = lang n (rexp.Inter (rexp_of_alt n (FOr \<phi>\<^sub>1 \<phi>\<^sub>2)) (ENC n (FOV (FOr \<phi>\<^sub>1 \<phi>\<^sub>2))))
[PROOF STEP]
unfolding rexp_of.simps rexp_of_alt.simps lang.simps
[PROOF STATE]
proof (prove)
using this:
lang n (rexp_of n \<phi>\<^sub>1) = lang n (rexp_of_alt n \<phi>\<^sub>1) \<inter> lang n (ENC n (FOV \<phi>\<^sub>1))
lang n (rexp_of n \<phi>\<^sub>2) = lang n (rexp_of_alt n \<phi>\<^sub>2) \<inter> lang n (ENC n (FOV \<phi>\<^sub>2))
lang n (ENC n (FOV (FOr \<phi>\<^sub>1 \<phi>\<^sub>2))) \<subseteq> lang n (ENC n (FOV \<phi>\<^sub>1)) \<inter> lang n (ENC n (FOV \<phi>\<^sub>2))

goal (1 subgoal):
 1. (lang n (rexp_of n \<phi>\<^sub>1) \<union> lang n (rexp_of n \<phi>\<^sub>2)) \<inter> lang n (ENC n (FOV (FOr \<phi>\<^sub>1 \<phi>\<^sub>2))) = (lang n (rexp_of_alt n \<phi>\<^sub>1) \<union> lang n (rexp_of_alt n \<phi>\<^sub>2)) \<inter> lang n (ENC n (FOV (FOr \<phi>\<^sub>1 \<phi>\<^sub>2)))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
lang n (rexp_of n (FOr \<phi>\<^sub>1 \<phi>\<^sub>2)) = lang n (rexp.Inter (rexp_of_alt n (FOr \<phi>\<^sub>1 \<phi>\<^sub>2)) (ENC n (FOV (FOr \<phi>\<^sub>1 \<phi>\<^sub>2))))

goal (5 subgoals):
 1. \<And>x1 x2 n. wf_formula n (FQ x1 x2) \<Longrightarrow> lang n (rexp_of n (FQ x1 x2)) = lang n (rexp.Inter (rexp_of_alt n (FQ x1 x2)) (ENC n (FOV (FQ x1 x2))))
 2. \<And>x1 x2 n. wf_formula n (FLess x1 x2) \<Longrightarrow> lang n (rexp_of n (FLess x1 x2)) = lang n (rexp.Inter (rexp_of_alt n (FLess x1 x2)) (ENC n (FOV (FLess x1 x2))))
 3. \<And>x1 x2 n. wf_formula n (FIn x1 x2) \<Longrightarrow> lang n (rexp_of n (FIn x1 x2)) = lang n (rexp.Inter (rexp_of_alt n (FIn x1 x2)) (ENC n (FOV (FIn x1 x2))))
 4. \<And>\<phi> n. \<lbrakk>\<And>n. wf_formula n \<phi> \<Longrightarrow> lang n (rexp_of n \<phi>) = lang n (rexp.Inter (rexp_of_alt n \<phi>) (ENC n (FOV \<phi>))); wf_formula n (FExists \<phi>)\<rbrakk> \<Longrightarrow> lang n (rexp_of n (FExists \<phi>)) = lang n (rexp.Inter (rexp_of_alt n (FExists \<phi>)) (ENC n (FOV (FExists \<phi>))))
 5. \<And>\<phi> n. \<lbrakk>\<And>n. wf_formula n \<phi> \<Longrightarrow> lang n (rexp_of n \<phi>) = lang n (rexp.Inter (rexp_of_alt n \<phi>) (ENC n (FOV \<phi>))); wf_formula n (FEXISTS \<phi>)\<rbrakk> \<Longrightarrow> lang n (rexp_of n (FEXISTS \<phi>)) = lang n (rexp.Inter (rexp_of_alt n (FEXISTS \<phi>)) (ENC n (FOV (FEXISTS \<phi>))))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>x1 x2 n. wf_formula n (FQ x1 x2) \<Longrightarrow> lang n (rexp_of n (FQ x1 x2)) = lang n (rexp.Inter (rexp_of_alt n (FQ x1 x2)) (ENC n (FOV (FQ x1 x2))))
 2. \<And>x1 x2 n. wf_formula n (FLess x1 x2) \<Longrightarrow> lang n (rexp_of n (FLess x1 x2)) = lang n (rexp.Inter (rexp_of_alt n (FLess x1 x2)) (ENC n (FOV (FLess x1 x2))))
 3. \<And>x1 x2 n. wf_formula n (FIn x1 x2) \<Longrightarrow> lang n (rexp_of n (FIn x1 x2)) = lang n (rexp.Inter (rexp_of_alt n (FIn x1 x2)) (ENC n (FOV (FIn x1 x2))))
 4. \<And>\<phi> n. \<lbrakk>\<And>n. wf_formula n \<phi> \<Longrightarrow> lang n (rexp_of n \<phi>) = lang n (rexp.Inter (rexp_of_alt n \<phi>) (ENC n (FOV \<phi>))); wf_formula n (FExists \<phi>)\<rbrakk> \<Longrightarrow> lang n (rexp_of n (FExists \<phi>)) = lang n (rexp.Inter (rexp_of_alt n (FExists \<phi>)) (ENC n (FOV (FExists \<phi>))))
 5. \<And>\<phi> n. \<lbrakk>\<And>n. wf_formula n \<phi> \<Longrightarrow> lang n (rexp_of n \<phi>) = lang n (rexp.Inter (rexp_of_alt n \<phi>) (ENC n (FOV \<phi>))); wf_formula n (FEXISTS \<phi>)\<rbrakk> \<Longrightarrow> lang n (rexp_of n (FEXISTS \<phi>)) = lang n (rexp.Inter (rexp_of_alt n (FEXISTS \<phi>)) (ENC n (FOV (FEXISTS \<phi>))))
[PROOF STEP]
case (FExists \<phi>)
[PROOF STATE]
proof (state)
this:
wf_formula ?n2 \<phi> \<Longrightarrow> lang ?n2 (rexp_of ?n2 \<phi>) = lang ?n2 (rexp.Inter (rexp_of_alt ?n2 \<phi>) (ENC ?n2 (FOV \<phi>)))
wf_formula n (FExists \<phi>)

goal (5 subgoals):
 1. \<And>x1 x2 n. wf_formula n (FQ x1 x2) \<Longrightarrow> lang n (rexp_of n (FQ x1 x2)) = lang n (rexp.Inter (rexp_of_alt n (FQ x1 x2)) (ENC n (FOV (FQ x1 x2))))
 2. \<And>x1 x2 n. wf_formula n (FLess x1 x2) \<Longrightarrow> lang n (rexp_of n (FLess x1 x2)) = lang n (rexp.Inter (rexp_of_alt n (FLess x1 x2)) (ENC n (FOV (FLess x1 x2))))
 3. \<And>x1 x2 n. wf_formula n (FIn x1 x2) \<Longrightarrow> lang n (rexp_of n (FIn x1 x2)) = lang n (rexp.Inter (rexp_of_alt n (FIn x1 x2)) (ENC n (FOV (FIn x1 x2))))
 4. \<And>\<phi> n. \<lbrakk>\<And>n. wf_formula n \<phi> \<Longrightarrow> lang n (rexp_of n \<phi>) = lang n (rexp.Inter (rexp_of_alt n \<phi>) (ENC n (FOV \<phi>))); wf_formula n (FExists \<phi>)\<rbrakk> \<Longrightarrow> lang n (rexp_of n (FExists \<phi>)) = lang n (rexp.Inter (rexp_of_alt n (FExists \<phi>)) (ENC n (FOV (FExists \<phi>))))
 5. \<And>\<phi> n. \<lbrakk>\<And>n. wf_formula n \<phi> \<Longrightarrow> lang n (rexp_of n \<phi>) = lang n (rexp.Inter (rexp_of_alt n \<phi>) (ENC n (FOV \<phi>))); wf_formula n (FEXISTS \<phi>)\<rbrakk> \<Longrightarrow> lang n (rexp_of n (FEXISTS \<phi>)) = lang n (rexp.Inter (rexp_of_alt n (FEXISTS \<phi>)) (ENC n (FOV (FEXISTS \<phi>))))
[PROOF STEP]
from FExists(2)
[PROOF STATE]
proof (chain)
picking this:
wf_formula n (FExists \<phi>)
[PROOF STEP]
have IH: "lang (n + 1) (rexp_of (n + 1) \<phi>) =
    lang (n + 1) (Inter (rexp_of_alt (n + 1) \<phi>) (ENC (n + 1) (FOV \<phi>)))"
[PROOF STATE]
proof (prove)
using this:
wf_formula n (FExists \<phi>)

goal (1 subgoal):
 1. lang (n + 1) (rexp_of (n + 1) \<phi>) = lang (n + 1) (rexp.Inter (rexp_of_alt (n + 1) \<phi>) (ENC (n + 1) (FOV \<phi>)))
[PROOF STEP]
by (intro FExists.IH) auto
[PROOF STATE]
proof (state)
this:
lang (n + 1) (rexp_of (n + 1) \<phi>) = lang (n + 1) (rexp.Inter (rexp_of_alt (n + 1) \<phi>) (ENC (n + 1) (FOV \<phi>)))

goal (5 subgoals):
 1. \<And>x1 x2 n. wf_formula n (FQ x1 x2) \<Longrightarrow> lang n (rexp_of n (FQ x1 x2)) = lang n (rexp.Inter (rexp_of_alt n (FQ x1 x2)) (ENC n (FOV (FQ x1 x2))))
 2. \<And>x1 x2 n. wf_formula n (FLess x1 x2) \<Longrightarrow> lang n (rexp_of n (FLess x1 x2)) = lang n (rexp.Inter (rexp_of_alt n (FLess x1 x2)) (ENC n (FOV (FLess x1 x2))))
 3. \<And>x1 x2 n. wf_formula n (FIn x1 x2) \<Longrightarrow> lang n (rexp_of n (FIn x1 x2)) = lang n (rexp.Inter (rexp_of_alt n (FIn x1 x2)) (ENC n (FOV (FIn x1 x2))))
 4. \<And>\<phi> n. \<lbrakk>\<And>n. wf_formula n \<phi> \<Longrightarrow> lang n (rexp_of n \<phi>) = lang n (rexp.Inter (rexp_of_alt n \<phi>) (ENC n (FOV \<phi>))); wf_formula n (FExists \<phi>)\<rbrakk> \<Longrightarrow> lang n (rexp_of n (FExists \<phi>)) = lang n (rexp.Inter (rexp_of_alt n (FExists \<phi>)) (ENC n (FOV (FExists \<phi>))))
 5. \<And>\<phi> n. \<lbrakk>\<And>n. wf_formula n \<phi> \<Longrightarrow> lang n (rexp_of n \<phi>) = lang n (rexp.Inter (rexp_of_alt n \<phi>) (ENC n (FOV \<phi>))); wf_formula n (FEXISTS \<phi>)\<rbrakk> \<Longrightarrow> lang n (rexp_of n (FEXISTS \<phi>)) = lang n (rexp.Inter (rexp_of_alt n (FEXISTS \<phi>)) (ENC n (FOV (FEXISTS \<phi>))))
[PROOF STEP]
have \<sigma>: "(any, replicate n False) \<in> (set o \<sigma> \<Sigma>) n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (any, replicate n False) \<in> (set \<circ> \<sigma> \<Sigma>) n
[PROOF STEP]
by (auto simp: \<sigma>_def set_n_lists image_iff)
[PROOF STATE]
proof (state)
this:
(any, replicate n False) \<in> (set \<circ> \<sigma> \<Sigma>) n

goal (5 subgoals):
 1. \<And>x1 x2 n. wf_formula n (FQ x1 x2) \<Longrightarrow> lang n (rexp_of n (FQ x1 x2)) = lang n (rexp.Inter (rexp_of_alt n (FQ x1 x2)) (ENC n (FOV (FQ x1 x2))))
 2. \<And>x1 x2 n. wf_formula n (FLess x1 x2) \<Longrightarrow> lang n (rexp_of n (FLess x1 x2)) = lang n (rexp.Inter (rexp_of_alt n (FLess x1 x2)) (ENC n (FOV (FLess x1 x2))))
 3. \<And>x1 x2 n. wf_formula n (FIn x1 x2) \<Longrightarrow> lang n (rexp_of n (FIn x1 x2)) = lang n (rexp.Inter (rexp_of_alt n (FIn x1 x2)) (ENC n (FOV (FIn x1 x2))))
 4. \<And>\<phi> n. \<lbrakk>\<And>n. wf_formula n \<phi> \<Longrightarrow> lang n (rexp_of n \<phi>) = lang n (rexp.Inter (rexp_of_alt n \<phi>) (ENC n (FOV \<phi>))); wf_formula n (FExists \<phi>)\<rbrakk> \<Longrightarrow> lang n (rexp_of n (FExists \<phi>)) = lang n (rexp.Inter (rexp_of_alt n (FExists \<phi>)) (ENC n (FOV (FExists \<phi>))))
 5. \<And>\<phi> n. \<lbrakk>\<And>n. wf_formula n \<phi> \<Longrightarrow> lang n (rexp_of n \<phi>) = lang n (rexp.Inter (rexp_of_alt n \<phi>) (ENC n (FOV \<phi>))); wf_formula n (FEXISTS \<phi>)\<rbrakk> \<Longrightarrow> lang n (rexp_of n (FEXISTS \<phi>)) = lang n (rexp.Inter (rexp_of_alt n (FEXISTS \<phi>)) (ENC n (FOV (FEXISTS \<phi>))))
[PROOF STEP]
from FExists(2)
[PROOF STATE]
proof (chain)
picking this:
wf_formula n (FExists \<phi>)
[PROOF STEP]
have wf: "wf n (Pr (rexp.Inter (rexp_of_alt (n + 1) \<phi>) (ENC (n + 1) (FOV \<phi>))))"
    "wf n (Pr (rexp_of (n + 1) \<phi>))"
[PROOF STATE]
proof (prove)
using this:
wf_formula n (FExists \<phi>)

goal (1 subgoal):
 1. local.wf n (Pr (rexp.Inter (rexp_of_alt (n + 1) \<phi>) (ENC (n + 1) (FOV \<phi>)))) &&& local.wf n (Pr (rexp_of (n + 1) \<phi>))
[PROOF STEP]
by (fastforce simp: max_idx_vars intro!: wf_rexp_of wf_rexp_of_alt wf_rexp_ENC[OF finite_FOV])+
[PROOF STATE]
proof (state)
this:
local.wf n (Pr (rexp.Inter (rexp_of_alt (n + 1) \<phi>) (ENC (n + 1) (FOV \<phi>))))
local.wf n (Pr (rexp_of (n + 1) \<phi>))

goal (5 subgoals):
 1. \<And>x1 x2 n. wf_formula n (FQ x1 x2) \<Longrightarrow> lang n (rexp_of n (FQ x1 x2)) = lang n (rexp.Inter (rexp_of_alt n (FQ x1 x2)) (ENC n (FOV (FQ x1 x2))))
 2. \<And>x1 x2 n. wf_formula n (FLess x1 x2) \<Longrightarrow> lang n (rexp_of n (FLess x1 x2)) = lang n (rexp.Inter (rexp_of_alt n (FLess x1 x2)) (ENC n (FOV (FLess x1 x2))))
 3. \<And>x1 x2 n. wf_formula n (FIn x1 x2) \<Longrightarrow> lang n (rexp_of n (FIn x1 x2)) = lang n (rexp.Inter (rexp_of_alt n (FIn x1 x2)) (ENC n (FOV (FIn x1 x2))))
 4. \<And>\<phi> n. \<lbrakk>\<And>n. wf_formula n \<phi> \<Longrightarrow> lang n (rexp_of n \<phi>) = lang n (rexp.Inter (rexp_of_alt n \<phi>) (ENC n (FOV \<phi>))); wf_formula n (FExists \<phi>)\<rbrakk> \<Longrightarrow> lang n (rexp_of n (FExists \<phi>)) = lang n (rexp.Inter (rexp_of_alt n (FExists \<phi>)) (ENC n (FOV (FExists \<phi>))))
 5. \<And>\<phi> n. \<lbrakk>\<And>n. wf_formula n \<phi> \<Longrightarrow> lang n (rexp_of n \<phi>) = lang n (rexp.Inter (rexp_of_alt n \<phi>) (ENC n (FOV \<phi>))); wf_formula n (FEXISTS \<phi>)\<rbrakk> \<Longrightarrow> lang n (rexp_of n (FEXISTS \<phi>)) = lang n (rexp.Inter (rexp_of_alt n (FEXISTS \<phi>)) (ENC n (FOV (FEXISTS \<phi>))))
[PROOF STEP]
note lang_quot = lang_samequot_exec[OF wf(1) \<sigma>] lang_samequot_exec[OF wf(2) \<sigma>]
[PROOF STATE]
proof (state)
this:
lang n (samequot_exec (any, replicate n False) (Pr (rexp.Inter (rexp_of_alt (n + 1) \<phi>) (ENC (n + 1) (FOV \<phi>))))) = SAMEQUOT (any, replicate n False) (lang n (Pr (rexp.Inter (rexp_of_alt (n + 1) \<phi>) (ENC (n + 1) (FOV \<phi>)))))
lang n (samequot_exec (any, replicate n False) (Pr (rexp_of (n + 1) \<phi>))) = SAMEQUOT (any, replicate n False) (lang n (Pr (rexp_of (n + 1) \<phi>)))

goal (5 subgoals):
 1. \<And>x1 x2 n. wf_formula n (FQ x1 x2) \<Longrightarrow> lang n (rexp_of n (FQ x1 x2)) = lang n (rexp.Inter (rexp_of_alt n (FQ x1 x2)) (ENC n (FOV (FQ x1 x2))))
 2. \<And>x1 x2 n. wf_formula n (FLess x1 x2) \<Longrightarrow> lang n (rexp_of n (FLess x1 x2)) = lang n (rexp.Inter (rexp_of_alt n (FLess x1 x2)) (ENC n (FOV (FLess x1 x2))))
 3. \<And>x1 x2 n. wf_formula n (FIn x1 x2) \<Longrightarrow> lang n (rexp_of n (FIn x1 x2)) = lang n (rexp.Inter (rexp_of_alt n (FIn x1 x2)) (ENC n (FOV (FIn x1 x2))))
 4. \<And>\<phi> n. \<lbrakk>\<And>n. wf_formula n \<phi> \<Longrightarrow> lang n (rexp_of n \<phi>) = lang n (rexp.Inter (rexp_of_alt n \<phi>) (ENC n (FOV \<phi>))); wf_formula n (FExists \<phi>)\<rbrakk> \<Longrightarrow> lang n (rexp_of n (FExists \<phi>)) = lang n (rexp.Inter (rexp_of_alt n (FExists \<phi>)) (ENC n (FOV (FExists \<phi>))))
 5. \<And>\<phi> n. \<lbrakk>\<And>n. wf_formula n \<phi> \<Longrightarrow> lang n (rexp_of n \<phi>) = lang n (rexp.Inter (rexp_of_alt n \<phi>) (ENC n (FOV \<phi>))); wf_formula n (FEXISTS \<phi>)\<rbrakk> \<Longrightarrow> lang n (rexp_of n (FEXISTS \<phi>)) = lang n (rexp.Inter (rexp_of_alt n (FEXISTS \<phi>)) (ENC n (FOV (FEXISTS \<phi>))))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lang n (rexp_of n (FExists \<phi>)) = lang n (rexp.Inter (rexp_of_alt n (FExists \<phi>)) (ENC n (FOV (FExists \<phi>))))
[PROOF STEP]
unfolding rexp_of.simps rexp_of_alt.simps lang.simps IH lang_quot Suc_eq_plus1
    ENC_FExists[OF FExists.prems, unfolded Suc_eq_plus1]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. SAMEQUOT (any, replicate n False) (map \<pi> ` (lang (n + 1) (rexp_of_alt (n + 1) \<phi>) \<inter> lang (n + 1) (ENC (n + 1) (FOV \<phi>)))) = SAMEQUOT (any, replicate n False) (map \<pi> ` (lang (n + 1) (rexp_of_alt (n + 1) \<phi>) \<inter> lang (n + 1) (ENC (n + 1) (FOV \<phi>)))) \<inter> SAMEQUOT (any, replicate n False) (map \<pi> ` lang (n + 1) (ENC (n + 1) (FOV \<phi>)))
[PROOF STEP]
by (auto simp add: SAMEQUOT_def)
[PROOF STATE]
proof (state)
this:
lang n (rexp_of n (FExists \<phi>)) = lang n (rexp.Inter (rexp_of_alt n (FExists \<phi>)) (ENC n (FOV (FExists \<phi>))))

goal (4 subgoals):
 1. \<And>x1 x2 n. wf_formula n (FQ x1 x2) \<Longrightarrow> lang n (rexp_of n (FQ x1 x2)) = lang n (rexp.Inter (rexp_of_alt n (FQ x1 x2)) (ENC n (FOV (FQ x1 x2))))
 2. \<And>x1 x2 n. wf_formula n (FLess x1 x2) \<Longrightarrow> lang n (rexp_of n (FLess x1 x2)) = lang n (rexp.Inter (rexp_of_alt n (FLess x1 x2)) (ENC n (FOV (FLess x1 x2))))
 3. \<And>x1 x2 n. wf_formula n (FIn x1 x2) \<Longrightarrow> lang n (rexp_of n (FIn x1 x2)) = lang n (rexp.Inter (rexp_of_alt n (FIn x1 x2)) (ENC n (FOV (FIn x1 x2))))
 4. \<And>\<phi> n. \<lbrakk>\<And>n. wf_formula n \<phi> \<Longrightarrow> lang n (rexp_of n \<phi>) = lang n (rexp.Inter (rexp_of_alt n \<phi>) (ENC n (FOV \<phi>))); wf_formula n (FEXISTS \<phi>)\<rbrakk> \<Longrightarrow> lang n (rexp_of n (FEXISTS \<phi>)) = lang n (rexp.Inter (rexp_of_alt n (FEXISTS \<phi>)) (ENC n (FOV (FEXISTS \<phi>))))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>x1 x2 n. wf_formula n (FQ x1 x2) \<Longrightarrow> lang n (rexp_of n (FQ x1 x2)) = lang n (rexp.Inter (rexp_of_alt n (FQ x1 x2)) (ENC n (FOV (FQ x1 x2))))
 2. \<And>x1 x2 n. wf_formula n (FLess x1 x2) \<Longrightarrow> lang n (rexp_of n (FLess x1 x2)) = lang n (rexp.Inter (rexp_of_alt n (FLess x1 x2)) (ENC n (FOV (FLess x1 x2))))
 3. \<And>x1 x2 n. wf_formula n (FIn x1 x2) \<Longrightarrow> lang n (rexp_of n (FIn x1 x2)) = lang n (rexp.Inter (rexp_of_alt n (FIn x1 x2)) (ENC n (FOV (FIn x1 x2))))
 4. \<And>\<phi> n. \<lbrakk>\<And>n. wf_formula n \<phi> \<Longrightarrow> lang n (rexp_of n \<phi>) = lang n (rexp.Inter (rexp_of_alt n \<phi>) (ENC n (FOV \<phi>))); wf_formula n (FEXISTS \<phi>)\<rbrakk> \<Longrightarrow> lang n (rexp_of n (FEXISTS \<phi>)) = lang n (rexp.Inter (rexp_of_alt n (FEXISTS \<phi>)) (ENC n (FOV (FEXISTS \<phi>))))
[PROOF STEP]
case (FEXISTS \<phi>)
[PROOF STATE]
proof (state)
this:
wf_formula ?n2 \<phi> \<Longrightarrow> lang ?n2 (rexp_of ?n2 \<phi>) = lang ?n2 (rexp.Inter (rexp_of_alt ?n2 \<phi>) (ENC ?n2 (FOV \<phi>)))
wf_formula n (FEXISTS \<phi>)

goal (4 subgoals):
 1. \<And>x1 x2 n. wf_formula n (FQ x1 x2) \<Longrightarrow> lang n (rexp_of n (FQ x1 x2)) = lang n (rexp.Inter (rexp_of_alt n (FQ x1 x2)) (ENC n (FOV (FQ x1 x2))))
 2. \<And>x1 x2 n. wf_formula n (FLess x1 x2) \<Longrightarrow> lang n (rexp_of n (FLess x1 x2)) = lang n (rexp.Inter (rexp_of_alt n (FLess x1 x2)) (ENC n (FOV (FLess x1 x2))))
 3. \<And>x1 x2 n. wf_formula n (FIn x1 x2) \<Longrightarrow> lang n (rexp_of n (FIn x1 x2)) = lang n (rexp.Inter (rexp_of_alt n (FIn x1 x2)) (ENC n (FOV (FIn x1 x2))))
 4. \<And>\<phi> n. \<lbrakk>\<And>n. wf_formula n \<phi> \<Longrightarrow> lang n (rexp_of n \<phi>) = lang n (rexp.Inter (rexp_of_alt n \<phi>) (ENC n (FOV \<phi>))); wf_formula n (FEXISTS \<phi>)\<rbrakk> \<Longrightarrow> lang n (rexp_of n (FEXISTS \<phi>)) = lang n (rexp.Inter (rexp_of_alt n (FEXISTS \<phi>)) (ENC n (FOV (FEXISTS \<phi>))))
[PROOF STEP]
from FEXISTS(2)
[PROOF STATE]
proof (chain)
picking this:
wf_formula n (FEXISTS \<phi>)
[PROOF STEP]
have IH: "lang (n + 1) (rexp_of (n + 1) \<phi>) =
    lang (n + 1) (Inter (rexp_of_alt (n + 1) \<phi>) (ENC (n + 1) (FOV \<phi>)))"
[PROOF STATE]
proof (prove)
using this:
wf_formula n (FEXISTS \<phi>)

goal (1 subgoal):
 1. lang (n + 1) (rexp_of (n + 1) \<phi>) = lang (n + 1) (rexp.Inter (rexp_of_alt (n + 1) \<phi>) (ENC (n + 1) (FOV \<phi>)))
[PROOF STEP]
by (intro FEXISTS.IH) auto
[PROOF STATE]
proof (state)
this:
lang (n + 1) (rexp_of (n + 1) \<phi>) = lang (n + 1) (rexp.Inter (rexp_of_alt (n + 1) \<phi>) (ENC (n + 1) (FOV \<phi>)))

goal (4 subgoals):
 1. \<And>x1 x2 n. wf_formula n (FQ x1 x2) \<Longrightarrow> lang n (rexp_of n (FQ x1 x2)) = lang n (rexp.Inter (rexp_of_alt n (FQ x1 x2)) (ENC n (FOV (FQ x1 x2))))
 2. \<And>x1 x2 n. wf_formula n (FLess x1 x2) \<Longrightarrow> lang n (rexp_of n (FLess x1 x2)) = lang n (rexp.Inter (rexp_of_alt n (FLess x1 x2)) (ENC n (FOV (FLess x1 x2))))
 3. \<And>x1 x2 n. wf_formula n (FIn x1 x2) \<Longrightarrow> lang n (rexp_of n (FIn x1 x2)) = lang n (rexp.Inter (rexp_of_alt n (FIn x1 x2)) (ENC n (FOV (FIn x1 x2))))
 4. \<And>\<phi> n. \<lbrakk>\<And>n. wf_formula n \<phi> \<Longrightarrow> lang n (rexp_of n \<phi>) = lang n (rexp.Inter (rexp_of_alt n \<phi>) (ENC n (FOV \<phi>))); wf_formula n (FEXISTS \<phi>)\<rbrakk> \<Longrightarrow> lang n (rexp_of n (FEXISTS \<phi>)) = lang n (rexp.Inter (rexp_of_alt n (FEXISTS \<phi>)) (ENC n (FOV (FEXISTS \<phi>))))
[PROOF STEP]
have \<sigma>: "(any, replicate n False) \<in> (set o \<sigma> \<Sigma>) n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (any, replicate n False) \<in> (set \<circ> \<sigma> \<Sigma>) n
[PROOF STEP]
by (auto simp: \<sigma>_def set_n_lists image_iff)
[PROOF STATE]
proof (state)
this:
(any, replicate n False) \<in> (set \<circ> \<sigma> \<Sigma>) n

goal (4 subgoals):
 1. \<And>x1 x2 n. wf_formula n (FQ x1 x2) \<Longrightarrow> lang n (rexp_of n (FQ x1 x2)) = lang n (rexp.Inter (rexp_of_alt n (FQ x1 x2)) (ENC n (FOV (FQ x1 x2))))
 2. \<And>x1 x2 n. wf_formula n (FLess x1 x2) \<Longrightarrow> lang n (rexp_of n (FLess x1 x2)) = lang n (rexp.Inter (rexp_of_alt n (FLess x1 x2)) (ENC n (FOV (FLess x1 x2))))
 3. \<And>x1 x2 n. wf_formula n (FIn x1 x2) \<Longrightarrow> lang n (rexp_of n (FIn x1 x2)) = lang n (rexp.Inter (rexp_of_alt n (FIn x1 x2)) (ENC n (FOV (FIn x1 x2))))
 4. \<And>\<phi> n. \<lbrakk>\<And>n. wf_formula n \<phi> \<Longrightarrow> lang n (rexp_of n \<phi>) = lang n (rexp.Inter (rexp_of_alt n \<phi>) (ENC n (FOV \<phi>))); wf_formula n (FEXISTS \<phi>)\<rbrakk> \<Longrightarrow> lang n (rexp_of n (FEXISTS \<phi>)) = lang n (rexp.Inter (rexp_of_alt n (FEXISTS \<phi>)) (ENC n (FOV (FEXISTS \<phi>))))
[PROOF STEP]
from FEXISTS(2)
[PROOF STATE]
proof (chain)
picking this:
wf_formula n (FEXISTS \<phi>)
[PROOF STEP]
have wf: "wf n (Pr (rexp.Inter (rexp_of_alt (n + 1) \<phi>) (ENC (n + 1) (FOV \<phi>))))"
    "wf n (Pr (rexp_of (n + 1) \<phi>))"
[PROOF STATE]
proof (prove)
using this:
wf_formula n (FEXISTS \<phi>)

goal (1 subgoal):
 1. local.wf n (Pr (rexp.Inter (rexp_of_alt (n + 1) \<phi>) (ENC (n + 1) (FOV \<phi>)))) &&& local.wf n (Pr (rexp_of (n + 1) \<phi>))
[PROOF STEP]
by (fastforce simp: max_idx_vars intro: wf_rexp_of wf_rexp_of_alt wf_rexp_ENC[OF finite_FOV])+
[PROOF STATE]
proof (state)
this:
local.wf n (Pr (rexp.Inter (rexp_of_alt (n + 1) \<phi>) (ENC (n + 1) (FOV \<phi>))))
local.wf n (Pr (rexp_of (n + 1) \<phi>))

goal (4 subgoals):
 1. \<And>x1 x2 n. wf_formula n (FQ x1 x2) \<Longrightarrow> lang n (rexp_of n (FQ x1 x2)) = lang n (rexp.Inter (rexp_of_alt n (FQ x1 x2)) (ENC n (FOV (FQ x1 x2))))
 2. \<And>x1 x2 n. wf_formula n (FLess x1 x2) \<Longrightarrow> lang n (rexp_of n (FLess x1 x2)) = lang n (rexp.Inter (rexp_of_alt n (FLess x1 x2)) (ENC n (FOV (FLess x1 x2))))
 3. \<And>x1 x2 n. wf_formula n (FIn x1 x2) \<Longrightarrow> lang n (rexp_of n (FIn x1 x2)) = lang n (rexp.Inter (rexp_of_alt n (FIn x1 x2)) (ENC n (FOV (FIn x1 x2))))
 4. \<And>\<phi> n. \<lbrakk>\<And>n. wf_formula n \<phi> \<Longrightarrow> lang n (rexp_of n \<phi>) = lang n (rexp.Inter (rexp_of_alt n \<phi>) (ENC n (FOV \<phi>))); wf_formula n (FEXISTS \<phi>)\<rbrakk> \<Longrightarrow> lang n (rexp_of n (FEXISTS \<phi>)) = lang n (rexp.Inter (rexp_of_alt n (FEXISTS \<phi>)) (ENC n (FOV (FEXISTS \<phi>))))
[PROOF STEP]
note lang_quot = lang_samequot_exec[OF wf(1) \<sigma>] lang_samequot_exec[OF wf(2) \<sigma>]
[PROOF STATE]
proof (state)
this:
lang n (samequot_exec (any, replicate n False) (Pr (rexp.Inter (rexp_of_alt (n + 1) \<phi>) (ENC (n + 1) (FOV \<phi>))))) = SAMEQUOT (any, replicate n False) (lang n (Pr (rexp.Inter (rexp_of_alt (n + 1) \<phi>) (ENC (n + 1) (FOV \<phi>)))))
lang n (samequot_exec (any, replicate n False) (Pr (rexp_of (n + 1) \<phi>))) = SAMEQUOT (any, replicate n False) (lang n (Pr (rexp_of (n + 1) \<phi>)))

goal (4 subgoals):
 1. \<And>x1 x2 n. wf_formula n (FQ x1 x2) \<Longrightarrow> lang n (rexp_of n (FQ x1 x2)) = lang n (rexp.Inter (rexp_of_alt n (FQ x1 x2)) (ENC n (FOV (FQ x1 x2))))
 2. \<And>x1 x2 n. wf_formula n (FLess x1 x2) \<Longrightarrow> lang n (rexp_of n (FLess x1 x2)) = lang n (rexp.Inter (rexp_of_alt n (FLess x1 x2)) (ENC n (FOV (FLess x1 x2))))
 3. \<And>x1 x2 n. wf_formula n (FIn x1 x2) \<Longrightarrow> lang n (rexp_of n (FIn x1 x2)) = lang n (rexp.Inter (rexp_of_alt n (FIn x1 x2)) (ENC n (FOV (FIn x1 x2))))
 4. \<And>\<phi> n. \<lbrakk>\<And>n. wf_formula n \<phi> \<Longrightarrow> lang n (rexp_of n \<phi>) = lang n (rexp.Inter (rexp_of_alt n \<phi>) (ENC n (FOV \<phi>))); wf_formula n (FEXISTS \<phi>)\<rbrakk> \<Longrightarrow> lang n (rexp_of n (FEXISTS \<phi>)) = lang n (rexp.Inter (rexp_of_alt n (FEXISTS \<phi>)) (ENC n (FOV (FEXISTS \<phi>))))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lang n (rexp_of n (FEXISTS \<phi>)) = lang n (rexp.Inter (rexp_of_alt n (FEXISTS \<phi>)) (ENC n (FOV (FEXISTS \<phi>))))
[PROOF STEP]
unfolding rexp_of.simps rexp_of_alt.simps lang.simps IH lang_quot Suc_eq_plus1
    ENC_FEXISTS[OF FEXISTS.prems, unfolded Suc_eq_plus1]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. SAMEQUOT (any, replicate n False) (map \<pi> ` (lang (n + 1) (rexp_of_alt (n + 1) \<phi>) \<inter> lang (n + 1) (ENC (n + 1) (FOV \<phi>)))) = SAMEQUOT (any, replicate n False) (map \<pi> ` (lang (n + 1) (rexp_of_alt (n + 1) \<phi>) \<inter> lang (n + 1) (ENC (n + 1) (FOV \<phi>)))) \<inter> SAMEQUOT (any, replicate n False) (map \<pi> ` lang (n + 1) (ENC (n + 1) (FOV \<phi>)))
[PROOF STEP]
by (auto simp add: SAMEQUOT_def)
[PROOF STATE]
proof (state)
this:
lang n (rexp_of n (FEXISTS \<phi>)) = lang n (rexp.Inter (rexp_of_alt n (FEXISTS \<phi>)) (ENC n (FOV (FEXISTS \<phi>))))

goal (3 subgoals):
 1. \<And>x1 x2 n. wf_formula n (FQ x1 x2) \<Longrightarrow> lang n (rexp_of n (FQ x1 x2)) = lang n (rexp.Inter (rexp_of_alt n (FQ x1 x2)) (ENC n (FOV (FQ x1 x2))))
 2. \<And>x1 x2 n. wf_formula n (FLess x1 x2) \<Longrightarrow> lang n (rexp_of n (FLess x1 x2)) = lang n (rexp.Inter (rexp_of_alt n (FLess x1 x2)) (ENC n (FOV (FLess x1 x2))))
 3. \<And>x1 x2 n. wf_formula n (FIn x1 x2) \<Longrightarrow> lang n (rexp_of n (FIn x1 x2)) = lang n (rexp.Inter (rexp_of_alt n (FIn x1 x2)) (ENC n (FOV (FIn x1 x2))))
[PROOF STEP]
qed auto


[STATEMENT]
lemma SAMEQUTO_UN[simp]: "SAMEQUOT x (\<Union>y \<in> A. B y) = (\<Union>y \<in> A. SAMEQUOT x (B y))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. SAMEQUOT x (\<Union> (B ` A)) = (\<Union>y\<in>A. SAMEQUOT x (B y))
[PROOF STEP]
unfolding SAMEQUOT_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {fin_cut_same x xa @ replicate m x |xa m. xa \<in> \<Union> (B ` A)} = (\<Union>y\<in>A. {fin_cut_same x xa @ replicate m x |xa m. xa \<in> B y})
[PROOF STEP]
by auto


[STATEMENT]
lemma finite_positions_in_row[simp]:
  "n > 0 \<Longrightarrow> finite (positions_in_row (x @- sconst (any, replicate n False)) 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < n \<Longrightarrow> finite (positions_in_row (x @- sconst (any, replicate n False)) 0)
[PROOF STEP]
unfolding positions_in_row shift_snth
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < n \<Longrightarrow> finite {p. snd (if p < length x then x ! p else sconst (any, replicate n False) !! (p - length x)) ! 0}
[PROOF STEP]
by auto


[STATEMENT]
lemma fin_cut_same_snoc: "fin_cut_same x (xs @ [y]) = (if x = y then fin_cut_same x xs else xs @ [y])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fin_cut_same x (xs @ [y]) = (if x = y then fin_cut_same x xs else xs @ [y])
[PROOF STEP]
by (induct xs) auto


[STATEMENT]
lemma fin_cut_same_idem: "fin_cut_same x (fin_cut_same x xs) = fin_cut_same x xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fin_cut_same x (fin_cut_same x xs) = fin_cut_same x xs
[PROOF STEP]
by (induct xs) auto


[STATEMENT]
lemma cut_same_sconst: "cut_same x (xs @- sconst x) = fin_cut_same x xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cut_same x (xs @- sconst x) = fin_cut_same x xs
[PROOF STEP]
proof (induct xs rule: rev_induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. cut_same x ([] @- sconst x) = fin_cut_same x []
 2. \<And>xa xs. cut_same x (xs @- sconst x) = fin_cut_same x xs \<Longrightarrow> cut_same x ((xs @ [xa]) @- sconst x) = fin_cut_same x (xs @ [xa])
[PROOF STEP]
case (snoc y ys)
[PROOF STATE]
proof (state)
this:
cut_same x (ys @- sconst x) = fin_cut_same x ys

goal (2 subgoals):
 1. cut_same x ([] @- sconst x) = fin_cut_same x []
 2. \<And>xa xs. cut_same x (xs @- sconst x) = fin_cut_same x xs \<Longrightarrow> cut_same x ((xs @ [xa]) @- sconst x) = fin_cut_same x (xs @ [xa])
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
cut_same x (ys @- sconst x) = fin_cut_same x ys
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
cut_same x (ys @- sconst x) = fin_cut_same x ys

goal (1 subgoal):
 1. cut_same x ((ys @ [y]) @- sconst x) = fin_cut_same x (ys @ [y])
[PROOF STEP]
by (auto simp del: id_apply simp add: fin_cut_same_snoc sconst_collapse)
[PROOF STATE]
proof (state)
this:
cut_same x ((ys @ [y]) @- sconst x) = fin_cut_same x (ys @ [y])

goal (1 subgoal):
 1. cut_same x ([] @- sconst x) = fin_cut_same x []
[PROOF STEP]
qed (simp del: id_apply)


[STATEMENT]
lemma length_cut_same: "length (cut_same x s) = (LEAST n. sdrop n s = sconst x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (cut_same x s) = (LEAST n. sdrop n s = sconst x)
[PROOF STEP]
unfolding cut_same_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (stake (LEAST n. sdrop n s = sconst x) s) = (LEAST n. sdrop n s = sconst x)
[PROOF STEP]
by simp


[STATEMENT]
lemma enc_alt: "wf_interp w I \<Longrightarrow>
  x \<in> enc (w, I) \<longleftrightarrow> x @- sconst ((any, replicate (length I) False)) = stream_enc (w, I)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf_interp w I \<Longrightarrow> (x \<in> enc (w, I)) = (x @- sconst (any, replicate (length I) False) = stream_enc (w, I))
[PROOF STEP]
unfolding enc.simps
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf_interp w I \<Longrightarrow> (x \<in> {x. \<exists>n. x = cut_same (any, replicate (length I) False) (stream_enc (w, I)) @ replicate n (any, replicate (length I) False)}) = (x @- sconst (any, replicate (length I) False) = stream_enc (w, I))
[PROOF STEP]
by (force simp only: shift_append shift_replicate_sconst stream_enc_cut_same[symmetric]
    length_append length_replicate length_cut_same sdrop_shift drop_all diff_self_eq_0
    shift.simps sdrop.simps
    dest: sym[of _ "stream_enc (w, I)"]
    intro: shift_sconst_inj[rotated, of _ "(any, replicate (length I) False)"] Least_le
      exI[of _ "length x - length (cut_same (any, replicate (length I) False) (stream_enc (w, I)))"]
      le_add_diff_inverse[symmetric] )


[STATEMENT]
lemma stream_stream_eqI: "\<lbrakk>\<forall>(_, x) \<in> sset xs. x \<noteq> []; \<forall>(_, x) \<in> sset ys. x \<noteq> [];
  smap (\<lambda>(_, x). hd x) xs = smap (\<lambda>(_, x). hd x) ys; smap \<pi> xs = smap \<pi> ys\<rbrakk> \<Longrightarrow> xs = ys"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>(uu_, x)\<in>sset xs. x \<noteq> []; \<forall>(uu_, x)\<in>sset ys. x \<noteq> []; smap (\<lambda>(uu_, x). hd x) xs = smap (\<lambda>(uu_, x). hd x) ys; smap \<pi> xs = smap \<pi> ys\<rbrakk> \<Longrightarrow> xs = ys
[PROOF STEP]
proof (coinduction arbitrary: xs ys)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xs ys. \<lbrakk>\<forall>x. x \<in> sset xs \<longrightarrow> (case x of (uu_, x) \<Rightarrow> x \<noteq> []); \<forall>x. x \<in> sset ys \<longrightarrow> (case x of (uu_, x) \<Rightarrow> x \<noteq> []); smap (\<lambda>(uu_, y). hd y) xs = smap (\<lambda>(uu_, y). hd y) ys; smap \<pi> xs = smap \<pi> ys\<rbrakk> \<Longrightarrow> shd xs = shd ys \<and> (\<exists>xsa ysa. stl xs = xsa \<and> stl ys = ysa \<and> (\<forall>x. x \<in> sset xsa \<longrightarrow> (case x of (uu_, x) \<Rightarrow> x \<noteq> [])) \<and> (\<forall>x. x \<in> sset ysa \<longrightarrow> (case x of (uu_, x) \<Rightarrow> x \<noteq> [])) \<and> smap (\<lambda>(uu_, y). hd y) xsa = smap (\<lambda>(uu_, y). hd y) ysa \<and> smap \<pi> xsa = smap \<pi> ysa)
[PROOF STEP]
case Eq_stream
[PROOF STATE]
proof (state)
this:
\<forall>x. x \<in> sset xs \<longrightarrow> (case x of (uu_, x) \<Rightarrow> x \<noteq> [])
\<forall>x. x \<in> sset ys \<longrightarrow> (case x of (uu_, x) \<Rightarrow> x \<noteq> [])
smap (\<lambda>(uu_, y). hd y) xs = smap (\<lambda>(uu_, y). hd y) ys
smap \<pi> xs = smap \<pi> ys

goal (1 subgoal):
 1. \<And>xs ys. \<lbrakk>\<forall>x. x \<in> sset xs \<longrightarrow> (case x of (uu_, x) \<Rightarrow> x \<noteq> []); \<forall>x. x \<in> sset ys \<longrightarrow> (case x of (uu_, x) \<Rightarrow> x \<noteq> []); smap (\<lambda>(uu_, y). hd y) xs = smap (\<lambda>(uu_, y). hd y) ys; smap \<pi> xs = smap \<pi> ys\<rbrakk> \<Longrightarrow> shd xs = shd ys \<and> (\<exists>xsa ysa. stl xs = xsa \<and> stl ys = ysa \<and> (\<forall>x. x \<in> sset xsa \<longrightarrow> (case x of (uu_, x) \<Rightarrow> x \<noteq> [])) \<and> (\<forall>x. x \<in> sset ysa \<longrightarrow> (case x of (uu_, x) \<Rightarrow> x \<noteq> [])) \<and> smap (\<lambda>(uu_, y). hd y) xsa = smap (\<lambda>(uu_, y). hd y) ysa \<and> smap \<pi> xsa = smap \<pi> ysa)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>x. x \<in> sset xs \<longrightarrow> (case x of (uu_, x) \<Rightarrow> x \<noteq> [])
\<forall>x. x \<in> sset ys \<longrightarrow> (case x of (uu_, x) \<Rightarrow> x \<noteq> [])
smap (\<lambda>(uu_, y). hd y) xs = smap (\<lambda>(uu_, y). hd y) ys
smap \<pi> xs = smap \<pi> ys
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<forall>x. x \<in> sset xs \<longrightarrow> (case x of (uu_, x) \<Rightarrow> x \<noteq> [])
\<forall>x. x \<in> sset ys \<longrightarrow> (case x of (uu_, x) \<Rightarrow> x \<noteq> [])
smap (\<lambda>(uu_, y). hd y) xs = smap (\<lambda>(uu_, y). hd y) ys
smap \<pi> xs = smap \<pi> ys

goal (1 subgoal):
 1. shd xs = shd ys \<and> (\<exists>xs ys. stl xs = xs \<and> stl ys = ys \<and> (\<forall>x. x \<in> sset xs \<longrightarrow> (case x of (uu_, x) \<Rightarrow> x \<noteq> [])) \<and> (\<forall>x. x \<in> sset ys \<longrightarrow> (case x of (uu_, x) \<Rightarrow> x \<noteq> [])) \<and> smap (\<lambda>(uu_, y). hd y) xs = smap (\<lambda>(uu_, y). hd y) ys \<and> smap \<pi> xs = smap \<pi> ys)
[PROOF STEP]
proof (cases xs ys rule: stream.exhaust[case_product stream.exhaust])
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x1__ x2__ x1a__ x2a__. \<lbrakk>\<forall>x. x \<in> sset xs \<longrightarrow> (case x of (uu_, x) \<Rightarrow> x \<noteq> []); \<forall>x. x \<in> sset ys \<longrightarrow> (case x of (uu_, x) \<Rightarrow> x \<noteq> []); smap (\<lambda>(uu_, y). hd y) xs = smap (\<lambda>(uu_, y). hd y) ys; smap \<pi> xs = smap \<pi> ys; xs = x1__ ## x2__; ys = x1a__ ## x2a__\<rbrakk> \<Longrightarrow> shd xs = shd ys \<and> (\<exists>xs ys. stl xs = xs \<and> stl ys = ys \<and> (\<forall>x. x \<in> sset xs \<longrightarrow> (case x of (uu_, x) \<Rightarrow> x \<noteq> [])) \<and> (\<forall>x. x \<in> sset ys \<longrightarrow> (case x of (uu_, x) \<Rightarrow> x \<noteq> [])) \<and> smap (\<lambda>(uu_, y). hd y) xs = smap (\<lambda>(uu_, y). hd y) ys \<and> smap \<pi> xs = smap \<pi> ys)
[PROOF STEP]
case (SCons_SCons h1 t1 h2 t2)
[PROOF STATE]
proof (state)
this:
xs = h1 ## t1
ys = h2 ## t2

goal (1 subgoal):
 1. \<And>x1__ x2__ x1a__ x2a__. \<lbrakk>\<forall>x. x \<in> sset xs \<longrightarrow> (case x of (uu_, x) \<Rightarrow> x \<noteq> []); \<forall>x. x \<in> sset ys \<longrightarrow> (case x of (uu_, x) \<Rightarrow> x \<noteq> []); smap (\<lambda>(uu_, y). hd y) xs = smap (\<lambda>(uu_, y). hd y) ys; smap \<pi> xs = smap \<pi> ys; xs = x1__ ## x2__; ys = x1a__ ## x2a__\<rbrakk> \<Longrightarrow> shd xs = shd ys \<and> (\<exists>xs ys. stl xs = xs \<and> stl ys = ys \<and> (\<forall>x. x \<in> sset xs \<longrightarrow> (case x of (uu_, x) \<Rightarrow> x \<noteq> [])) \<and> (\<forall>x. x \<in> sset ys \<longrightarrow> (case x of (uu_, x) \<Rightarrow> x \<noteq> [])) \<and> smap (\<lambda>(uu_, y). hd y) xs = smap (\<lambda>(uu_, y). hd y) ys \<and> smap \<pi> xs = smap \<pi> ys)
[PROOF STEP]
with Eq_stream
[PROOF STATE]
proof (chain)
picking this:
\<forall>x. x \<in> sset xs \<longrightarrow> (case x of (uu_, x) \<Rightarrow> x \<noteq> [])
\<forall>x. x \<in> sset ys \<longrightarrow> (case x of (uu_, x) \<Rightarrow> x \<noteq> [])
smap (\<lambda>(uu_, y). hd y) xs = smap (\<lambda>(uu_, y). hd y) ys
smap \<pi> xs = smap \<pi> ys
xs = h1 ## t1
ys = h2 ## t2
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>x. x \<in> sset xs \<longrightarrow> (case x of (uu_, x) \<Rightarrow> x \<noteq> [])
\<forall>x. x \<in> sset ys \<longrightarrow> (case x of (uu_, x) \<Rightarrow> x \<noteq> [])
smap (\<lambda>(uu_, y). hd y) xs = smap (\<lambda>(uu_, y). hd y) ys
smap \<pi> xs = smap \<pi> ys
xs = h1 ## t1
ys = h2 ## t2

goal (1 subgoal):
 1. shd xs = shd ys \<and> (\<exists>xs ys. stl xs = xs \<and> stl ys = ys \<and> (\<forall>x. x \<in> sset xs \<longrightarrow> (case x of (uu_, x) \<Rightarrow> x \<noteq> [])) \<and> (\<forall>x. x \<in> sset ys \<longrightarrow> (case x of (uu_, x) \<Rightarrow> x \<noteq> [])) \<and> smap (\<lambda>(uu_, y). hd y) xs = smap (\<lambda>(uu_, y). hd y) ys \<and> smap \<pi> xs = smap \<pi> ys)
[PROOF STEP]
by (cases "snd h1" "snd h2" rule: list.exhaust[case_product list.exhaust])
        (auto simp: \<pi>_def split: prod.splits)
[PROOF STATE]
proof (state)
this:
shd xs = shd ys \<and> (\<exists>xs ys. stl xs = xs \<and> stl ys = ys \<and> (\<forall>x. x \<in> sset xs \<longrightarrow> (case x of (uu_, x) \<Rightarrow> x \<noteq> [])) \<and> (\<forall>x. x \<in> sset ys \<longrightarrow> (case x of (uu_, x) \<Rightarrow> x \<noteq> [])) \<and> smap (\<lambda>(uu_, y). hd y) xs = smap (\<lambda>(uu_, y). hd y) ys \<and> smap \<pi> xs = smap \<pi> ys)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
shd xs = shd ys \<and> (\<exists>xs ys. stl xs = xs \<and> stl ys = ys \<and> (\<forall>x. x \<in> sset xs \<longrightarrow> (case x of (uu_, x) \<Rightarrow> x \<noteq> [])) \<and> (\<forall>x. x \<in> sset ys \<longrightarrow> (case x of (uu_, x) \<Rightarrow> x \<noteq> [])) \<and> smap (\<lambda>(uu_, y). hd y) xs = smap (\<lambda>(uu_, y). hd y) ys \<and> smap \<pi> xs = smap \<pi> ys)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma project_enc_extend:
  fixes x I
  defines "n \<equiv> length I"
  defines "z \<equiv> \<lambda>n. (any, replicate n False)"
  defines "I' \<equiv> Inr (positions_in_row (x @- sconst (z (Suc n))) 0) # I"
  assumes wf: "wf_interp w I"
  assumes enc: "fin_cut_same (z n) (map \<pi> x) @ replicate m (z n) \<in> enc (w, I)"
  assumes nonempty: "\<forall>(_, x) \<in> set x. x \<noteq> []"
  shows "x \<in> enc (w, I')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> enc (w, I')
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x \<in> enc (w, I')
[PROOF STEP]
have [simp]: "\<pi> (z (Suc n)) = z n"
    and z_def: "\<And>n. z n = (any, replicate n False)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pi> (z (Suc n)) = z n &&& (\<And>n. z n = (any, replicate n False))
[PROOF STEP]
unfolding \<pi>_def z_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (case (any, replicate (Suc n) False) of (a, bs) \<Rightarrow> (a, tl bs)) = (any, replicate n False) &&& (\<And>n. (any, replicate n False) = (any, replicate n False))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<pi> (z (Suc n)) = z n
z ?n2 = (any, replicate ?n2 False)

goal (1 subgoal):
 1. x \<in> enc (w, I')
[PROOF STEP]
have wf': "wf_interp w I'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf_interp w I'
[PROOF STEP]
by (simp add: wf I'_def z_def del: replicate_Suc)
[PROOF STATE]
proof (state)
this:
wf_interp w I'

goal (1 subgoal):
 1. x \<in> enc (w, I')
[PROOF STEP]
note simps[simp del] = stream_enc.simps
[PROOF STATE]
proof (state)
this:
stream_enc (?w, ?I) = smap2 (enc_atom ?I) nats (?w @- sconst any)

goal (1 subgoal):
 1. x \<in> enc (w, I')
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> enc (w, I')
[PROOF STEP]
unfolding enc_alt[OF wf']
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x @- sconst (any, replicate (length I') False) = stream_enc (w, I')
[PROOF STEP]
proof (rule stream_stream_eqI)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<forall>(uu_, x)\<in>sset (x @- sconst (any, replicate (length I') False)). x \<noteq> []
 2. \<forall>(uu_, x)\<in>sset (stream_enc (w, I')). x \<noteq> []
 3. smap (\<lambda>(uu_, x). hd x) (x @- sconst (any, replicate (length I') False)) = smap (\<lambda>(uu_, x). hd x) (stream_enc (w, I'))
 4. smap \<pi> (x @- sconst (any, replicate (length I') False)) = smap \<pi> (stream_enc (w, I'))
[PROOF STEP]
from nonempty stream_smap_nats[of "map (\<lambda>(_, y). hd y) x @- sconst False"]
      smap_szip_fst
[PROOF STATE]
proof (chain)
picking this:
\<forall>(uu_, x)\<in>set x. x \<noteq> []
map (\<lambda>(uu_, y). hd y) x @- sconst False = smap ((!!) (map (\<lambda>(uu_, y). hd y) x @- sconst False)) nats
smap (\<lambda>x. ?f (fst x)) (szip ?s1.0 ?s2.0) = smap ?f ?s1.0
[PROOF STEP]
show "smap (\<lambda>(_, x). hd x) (x @- sconst (any, replicate (length I') False)) =
      smap (\<lambda>(_, x). hd x) (stream_enc (w, I'))"
[PROOF STATE]
proof (prove)
using this:
\<forall>(uu_, x)\<in>set x. x \<noteq> []
map (\<lambda>(uu_, y). hd y) x @- sconst False = smap ((!!) (map (\<lambda>(uu_, y). hd y) x @- sconst False)) nats
smap (\<lambda>x. ?f (fst x)) (szip ?s1.0 ?s2.0) = smap ?f ?s1.0

goal (1 subgoal):
 1. smap (\<lambda>(uu_, x). hd x) (x @- sconst (any, replicate (length I') False)) = smap (\<lambda>(uu_, x). hd x) (stream_enc (w, I'))
[PROOF STEP]
by (auto simp add: stream_enc.simps I'_def z_def smap2_szip stream.map_comp o_def split_def
        positions_in_row shift_snth hd_conv_nth intro: smap_szip_fst[symmetric]
        cong: stream.map_cong)
[PROOF STATE]
proof (state)
this:
smap (\<lambda>(uu_, x). hd x) (x @- sconst (any, replicate (length I') False)) = smap (\<lambda>(uu_, x). hd x) (stream_enc (w, I'))

goal (3 subgoals):
 1. \<forall>(uu_, x)\<in>sset (x @- sconst (any, replicate (length I') False)). x \<noteq> []
 2. \<forall>(uu_, x)\<in>sset (stream_enc (w, I')). x \<noteq> []
 3. smap \<pi> (x @- sconst (any, replicate (length I') False)) = smap \<pi> (stream_enc (w, I'))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<forall>(uu_, x)\<in>sset (x @- sconst (any, replicate (length I') False)). x \<noteq> []
 2. \<forall>(uu_, x)\<in>sset (stream_enc (w, I')). x \<noteq> []
 3. smap \<pi> (x @- sconst (any, replicate (length I') False)) = smap \<pi> (stream_enc (w, I'))
[PROOF STEP]
from wf
[PROOF STATE]
proof (chain)
picking this:
wf_interp w I
[PROOF STEP]
have "fin_cut_same (z n) (map \<pi> x) = cut_same (z n) (stream_enc (w, I))"
[PROOF STATE]
proof (prove)
using this:
wf_interp w I

goal (1 subgoal):
 1. fin_cut_same (z n) (map \<pi> x) = cut_same (z n) (stream_enc (w, I))
[PROOF STEP]
using stream_enc_enc[OF _ enc]
[PROOF STATE]
proof (prove)
using this:
wf_interp w I
\<forall>x\<in>set I. case x of Inl a \<Rightarrow> True | Inr P \<Rightarrow> finite P \<Longrightarrow> stream_enc (w, I) = (fin_cut_same (z n) (map \<pi> x) @ replicate m (z n)) @- sconst (any, replicate (length I) False)

goal (1 subgoal):
 1. fin_cut_same (z n) (map \<pi> x) = cut_same (z n) (stream_enc (w, I))
[PROOF STEP]
by (auto simp add: cut_same_sconst z_def n_def fin_cut_same_idem)
[PROOF STATE]
proof (state)
this:
fin_cut_same (z n) (map \<pi> x) = cut_same (z n) (stream_enc (w, I))

goal (3 subgoals):
 1. \<forall>(uu_, x)\<in>sset (x @- sconst (any, replicate (length I') False)). x \<noteq> []
 2. \<forall>(uu_, x)\<in>sset (stream_enc (w, I')). x \<noteq> []
 3. smap \<pi> (x @- sconst (any, replicate (length I') False)) = smap \<pi> (stream_enc (w, I'))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
fin_cut_same (z n) (map \<pi> x) = cut_same (z n) (stream_enc (w, I))
[PROOF STEP]
obtain m' where \<pi>x: "map \<pi> x = cut_same (z n) (stream_enc (w, I)) @ replicate m' (z n)"
[PROOF STATE]
proof (prove)
using this:
fin_cut_same (z n) (map \<pi> x) = cut_same (z n) (stream_enc (w, I))

goal (1 subgoal):
 1. (\<And>m'. map \<pi> x = cut_same (z n) (stream_enc (w, I)) @ replicate m' (z n) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto dest!: fin_cut_sameE)
[PROOF STATE]
proof (state)
this:
map \<pi> x = cut_same (z n) (stream_enc (w, I)) @ replicate m' (z n)

goal (3 subgoals):
 1. \<forall>(uu_, x)\<in>sset (x @- sconst (any, replicate (length I') False)). x \<noteq> []
 2. \<forall>(uu_, x)\<in>sset (stream_enc (w, I')). x \<noteq> []
 3. smap \<pi> (x @- sconst (any, replicate (length I') False)) = smap \<pi> (stream_enc (w, I'))
[PROOF STEP]
with wf
[PROOF STATE]
proof (chain)
picking this:
wf_interp w I
map \<pi> x = cut_same (z n) (stream_enc (w, I)) @ replicate m' (z n)
[PROOF STEP]
show "smap \<pi> (x @- sconst (any, replicate (length I') False)) =
      smap \<pi> (stream_enc (w, I'))"
[PROOF STATE]
proof (prove)
using this:
wf_interp w I
map \<pi> x = cut_same (z n) (stream_enc (w, I)) @ replicate m' (z n)

goal (1 subgoal):
 1. smap \<pi> (x @- sconst (any, replicate (length I') False)) = smap \<pi> (stream_enc (w, I'))
[PROOF STEP]
by (simp del: replicate_Suc add: n_def[symmetric] z_def[symmetric] I'_def
        stream_enc_cut_same[of I, symmetric, folded n_def z_def])
[PROOF STATE]
proof (state)
this:
smap \<pi> (x @- sconst (any, replicate (length I') False)) = smap \<pi> (stream_enc (w, I'))

goal (2 subgoals):
 1. \<forall>(uu_, x)\<in>sset (x @- sconst (any, replicate (length I') False)). x \<noteq> []
 2. \<forall>(uu_, x)\<in>sset (stream_enc (w, I')). x \<noteq> []
[PROOF STEP]
qed (insert nonempty, simp_all add: stream_enc.simps I'_def split_beta smap2_szip stream.set_map)
[PROOF STATE]
proof (state)
this:
x \<in> enc (w, I')

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma pred_case_conv: "x - Suc 0 = (case x of 0 \<Rightarrow> 0 | Suc m \<Rightarrow> m)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x - Suc 0 = (case x of 0 \<Rightarrow> 0 | Suc m \<Rightarrow> m)
[PROOF STEP]
by (cases x) auto


[STATEMENT]
lemma in_pred_image_iff: "0 \<notin> X \<Longrightarrow> (x \<in> (\<lambda>x. x - Suc 0) ` X) = (Suc x \<in> X)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<notin> X \<Longrightarrow> (x \<in> (\<lambda>x. x - Suc 0) ` X) = (Suc x \<in> X)
[PROOF STEP]
by (auto simp: pred_case_conv split: nat.splits)