[STATEMENT]
lemma encD:
  "\<lbrakk>v \<in> enc (w, I); (\<forall>x \<in> set I. case x of Inr P \<Rightarrow> finite P | _ \<Rightarrow> True)\<rbrakk> \<Longrightarrow>
  v = map (case_prod (enc_atom I)) (zip [0 ..< length v] (stake (length v) (w @- sconst any)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>v \<in> enc (w, I); \<forall>x\<in>set I. case x of Inl a \<Rightarrow> True | Inr P \<Rightarrow> finite P\<rbrakk> \<Longrightarrow> v = map2 (enc_atom I) [0..<length v] (stake (length v) (w @- sconst any))
[PROOF STEP]
by (erule box_equals[OF sym[OF arg_cong[of _ _ "stake (length v)" ,OF stream_enc_enc]]])
   (auto simp: stake_shift sdrop_shift stake_add[symmetric] map_replicate_const)


[STATEMENT]
lemma enc_Inl: "\<lbrakk>x \<in> enc (w, I); (\<forall>x \<in> set I. case x of Inr P \<Rightarrow> finite P | _ \<Rightarrow> True);
  m < length I; I ! m = Inl p\<rbrakk> \<Longrightarrow> p < length x \<and> snd (x ! p) ! m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> enc (w, I); \<forall>x\<in>set I. case x of Inl a \<Rightarrow> True | Inr P \<Rightarrow> finite P; m < length I; I ! m = Inl p\<rbrakk> \<Longrightarrow> p < length x \<and> snd (x ! p) ! m
[PROOF STEP]
by (auto dest!: less_length_cut_same_Inl[of _ _ _ w] simp: nth_append cut_same_def)


[STATEMENT]
lemma enc_Inr: assumes "x \<in> enc (w, I)" "\<forall>x \<in> set I. case x of Inr P \<Rightarrow> finite P | _ \<Rightarrow> True"
  "M < length I" "I ! M = Inr P"
  shows "p \<in> P \<longleftrightarrow> p < length x \<and> snd (x ! p) ! M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (p \<in> P) = (p < length x \<and> snd (x ! p) ! M)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. p \<in> P \<Longrightarrow> p < length x \<and> snd (x ! p) ! M
 2. p < length x \<and> snd (x ! p) ! M \<Longrightarrow> p \<in> P
[PROOF STEP]
assume "p \<in> P"
[PROOF STATE]
proof (state)
this:
p \<in> P

goal (2 subgoals):
 1. p \<in> P \<Longrightarrow> p < length x \<and> snd (x ! p) ! M
 2. p < length x \<and> snd (x ! p) ! M \<Longrightarrow> p \<in> P
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
x \<in> enc (w, I)
\<forall>x\<in>set I. case x of Inl a \<Rightarrow> True | Inr P \<Rightarrow> finite P
M < length I
I ! M = Inr P
p \<in> P
[PROOF STEP]
show "p < length x \<and> snd (x ! p) ! M"
[PROOF STATE]
proof (prove)
using this:
x \<in> enc (w, I)
\<forall>x\<in>set I. case x of Inl a \<Rightarrow> True | Inr P \<Rightarrow> finite P
M < length I
I ! M = Inr P
p \<in> P

goal (1 subgoal):
 1. p < length x \<and> snd (x ! p) ! M
[PROOF STEP]
by (auto dest!: less_length_cut_same_Inr[of _ _ _ w] simp: nth_append cut_same_def)
[PROOF STATE]
proof (state)
this:
p < length x \<and> snd (x ! p) ! M

goal (1 subgoal):
 1. p < length x \<and> snd (x ! p) ! M \<Longrightarrow> p \<in> P
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. p < length x \<and> snd (x ! p) ! M \<Longrightarrow> p \<in> P
[PROOF STEP]
assume "p < length x \<and> snd (x ! p) ! M"
[PROOF STATE]
proof (state)
this:
p < length x \<and> snd (x ! p) ! M

goal (1 subgoal):
 1. p < length x \<and> snd (x ! p) ! M \<Longrightarrow> p \<in> P
[PROOF STEP]
thus "p \<in> P"
[PROOF STATE]
proof (prove)
using this:
p < length x \<and> snd (x ! p) ! M

goal (1 subgoal):
 1. p \<in> P
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
p < length x \<and> snd (x ! p) ! M
x \<in> enc (w, I)
\<forall>x\<in>set I. case x of Inl a \<Rightarrow> True | Inr P \<Rightarrow> finite P
M < length I
I ! M = Inr P

goal (1 subgoal):
 1. p \<in> P
[PROOF STEP]
by (subst (asm) (2) encD[OF assms(1,2)]) auto
[PROOF STATE]
proof (state)
this:
p \<in> P

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma enc_length:
  assumes "enc (w, I) = enc (w', I')"
  shows "length I = length I'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length I = length I'
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. length I = length I'
[PROOF STEP]
let ?cL = "\<lambda>w I. cut_same (any, replicate (length I) False) (stream_enc (w, I))"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. length I = length I'
[PROOF STEP]
let ?w = "\<lambda>w I m. ?cL w I @ replicate (m - length (?cL w I)) (any, replicate (length I) False)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. length I = length I'
[PROOF STEP]
let ?max = "max (length (?cL w I)) (length (?cL w' I')) + 1"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. length I = length I'
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
enc (w, I) = enc (w', I')
[PROOF STEP]
have "?w w I ?max \<in> enc (w, I)" "?w w' I' ?max \<in> enc (w', I')"
[PROOF STATE]
proof (prove)
using this:
enc (w, I) = enc (w', I')

goal (1 subgoal):
 1. cut_same (any, replicate (length I) False) (stream_enc (w, I)) @ replicate (max (length (cut_same (any, replicate (length I) False) (stream_enc (w, I)))) (length (cut_same (any, replicate (length I') False) (stream_enc (w', I')))) + 1 - length (cut_same (any, replicate (length I) False) (stream_enc (w, I)))) (any, replicate (length I) False) \<in> enc (w, I) &&& cut_same (any, replicate (length I') False) (stream_enc (w', I')) @ replicate (max (length (cut_same (any, replicate (length I) False) (stream_enc (w, I)))) (length (cut_same (any, replicate (length I') False) (stream_enc (w', I')))) + 1 - length (cut_same (any, replicate (length I') False) (stream_enc (w', I')))) (any, replicate (length I') False) \<in> enc (w', I')
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
cut_same (any, replicate (length I) False) (stream_enc (w, I)) @ replicate (max (length (cut_same (any, replicate (length I) False) (stream_enc (w, I)))) (length (cut_same (any, replicate (length I') False) (stream_enc (w', I')))) + 1 - length (cut_same (any, replicate (length I) False) (stream_enc (w, I)))) (any, replicate (length I) False) \<in> enc (w, I)
cut_same (any, replicate (length I') False) (stream_enc (w', I')) @ replicate (max (length (cut_same (any, replicate (length I) False) (stream_enc (w, I)))) (length (cut_same (any, replicate (length I') False) (stream_enc (w', I')))) + 1 - length (cut_same (any, replicate (length I') False) (stream_enc (w', I')))) (any, replicate (length I') False) \<in> enc (w', I')

goal (1 subgoal):
 1. length I = length I'
[PROOF STEP]
hence "?w w I ?max = ?w w' I' ?max"
[PROOF STATE]
proof (prove)
using this:
cut_same (any, replicate (length I) False) (stream_enc (w, I)) @ replicate (max (length (cut_same (any, replicate (length I) False) (stream_enc (w, I)))) (length (cut_same (any, replicate (length I') False) (stream_enc (w', I')))) + 1 - length (cut_same (any, replicate (length I) False) (stream_enc (w, I)))) (any, replicate (length I) False) \<in> enc (w, I)
cut_same (any, replicate (length I') False) (stream_enc (w', I')) @ replicate (max (length (cut_same (any, replicate (length I) False) (stream_enc (w, I)))) (length (cut_same (any, replicate (length I') False) (stream_enc (w', I')))) + 1 - length (cut_same (any, replicate (length I') False) (stream_enc (w', I')))) (any, replicate (length I') False) \<in> enc (w', I')

goal (1 subgoal):
 1. cut_same (any, replicate (length I) False) (stream_enc (w, I)) @ replicate (max (length (cut_same (any, replicate (length I) False) (stream_enc (w, I)))) (length (cut_same (any, replicate (length I') False) (stream_enc (w', I')))) + 1 - length (cut_same (any, replicate (length I) False) (stream_enc (w, I)))) (any, replicate (length I) False) = cut_same (any, replicate (length I') False) (stream_enc (w', I')) @ replicate (max (length (cut_same (any, replicate (length I) False) (stream_enc (w, I)))) (length (cut_same (any, replicate (length I') False) (stream_enc (w', I')))) + 1 - length (cut_same (any, replicate (length I') False) (stream_enc (w', I')))) (any, replicate (length I') False)
[PROOF STEP]
using enc_unique_length assms
[PROOF STATE]
proof (prove)
using this:
cut_same (any, replicate (length I) False) (stream_enc (w, I)) @ replicate (max (length (cut_same (any, replicate (length I) False) (stream_enc (w, I)))) (length (cut_same (any, replicate (length I') False) (stream_enc (w', I')))) + 1 - length (cut_same (any, replicate (length I) False) (stream_enc (w, I)))) (any, replicate (length I) False) \<in> enc (w, I)
cut_same (any, replicate (length I') False) (stream_enc (w', I')) @ replicate (max (length (cut_same (any, replicate (length I) False) (stream_enc (w, I)))) (length (cut_same (any, replicate (length I') False) (stream_enc (w', I')))) + 1 - length (cut_same (any, replicate (length I') False) (stream_enc (w', I')))) (any, replicate (length I') False) \<in> enc (w', I')
?v \<in> enc (?w, ?I) \<Longrightarrow> \<forall>v'. length v' = length ?v \<and> v' \<in> enc (?w, ?I) \<longrightarrow> ?v = v'
enc (w, I) = enc (w', I')

goal (1 subgoal):
 1. cut_same (any, replicate (length I) False) (stream_enc (w, I)) @ replicate (max (length (cut_same (any, replicate (length I) False) (stream_enc (w, I)))) (length (cut_same (any, replicate (length I') False) (stream_enc (w', I')))) + 1 - length (cut_same (any, replicate (length I) False) (stream_enc (w, I)))) (any, replicate (length I) False) = cut_same (any, replicate (length I') False) (stream_enc (w', I')) @ replicate (max (length (cut_same (any, replicate (length I) False) (stream_enc (w, I)))) (length (cut_same (any, replicate (length I') False) (stream_enc (w', I')))) + 1 - length (cut_same (any, replicate (length I') False) (stream_enc (w', I')))) (any, replicate (length I') False)
[PROOF STEP]
by (simp del: enc.simps)
[PROOF STATE]
proof (state)
this:
cut_same (any, replicate (length I) False) (stream_enc (w, I)) @ replicate (max (length (cut_same (any, replicate (length I) False) (stream_enc (w, I)))) (length (cut_same (any, replicate (length I') False) (stream_enc (w', I')))) + 1 - length (cut_same (any, replicate (length I) False) (stream_enc (w, I)))) (any, replicate (length I) False) = cut_same (any, replicate (length I') False) (stream_enc (w', I')) @ replicate (max (length (cut_same (any, replicate (length I) False) (stream_enc (w, I)))) (length (cut_same (any, replicate (length I') False) (stream_enc (w', I')))) + 1 - length (cut_same (any, replicate (length I') False) (stream_enc (w', I')))) (any, replicate (length I') False)

goal (1 subgoal):
 1. length I = length I'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
cut_same (any, replicate (length I) False) (stream_enc (w, I)) @ replicate (max (length (cut_same (any, replicate (length I) False) (stream_enc (w, I)))) (length (cut_same (any, replicate (length I') False) (stream_enc (w', I')))) + 1 - length (cut_same (any, replicate (length I) False) (stream_enc (w, I)))) (any, replicate (length I) False) = cut_same (any, replicate (length I') False) (stream_enc (w', I')) @ replicate (max (length (cut_same (any, replicate (length I) False) (stream_enc (w, I)))) (length (cut_same (any, replicate (length I') False) (stream_enc (w', I')))) + 1 - length (cut_same (any, replicate (length I') False) (stream_enc (w', I')))) (any, replicate (length I') False)

goal (1 subgoal):
 1. length I = length I'
[PROOF STEP]
have "last (?w w I ?max) = (any, replicate (length I) False)"
                "last (?w w' I' ?max) = (any, replicate (length I') False)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. last (cut_same (any, replicate (length I) False) (stream_enc (w, I)) @ replicate (max (length (cut_same (any, replicate (length I) False) (stream_enc (w, I)))) (length (cut_same (any, replicate (length I') False) (stream_enc (w', I')))) + 1 - length (cut_same (any, replicate (length I) False) (stream_enc (w, I)))) (any, replicate (length I) False)) = (any, replicate (length I) False) &&& last (cut_same (any, replicate (length I') False) (stream_enc (w', I')) @ replicate (max (length (cut_same (any, replicate (length I) False) (stream_enc (w, I)))) (length (cut_same (any, replicate (length I') False) (stream_enc (w', I')))) + 1 - length (cut_same (any, replicate (length I') False) (stream_enc (w', I')))) (any, replicate (length I') False)) = (any, replicate (length I') False)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
last (cut_same (any, replicate (length I) False) (stream_enc (w, I)) @ replicate (max (length (cut_same (any, replicate (length I) False) (stream_enc (w, I)))) (length (cut_same (any, replicate (length I') False) (stream_enc (w', I')))) + 1 - length (cut_same (any, replicate (length I) False) (stream_enc (w, I)))) (any, replicate (length I) False)) = (any, replicate (length I) False)
last (cut_same (any, replicate (length I') False) (stream_enc (w', I')) @ replicate (max (length (cut_same (any, replicate (length I) False) (stream_enc (w, I)))) (length (cut_same (any, replicate (length I') False) (stream_enc (w', I')))) + 1 - length (cut_same (any, replicate (length I') False) (stream_enc (w', I')))) (any, replicate (length I') False)) = (any, replicate (length I') False)

goal (1 subgoal):
 1. length I = length I'
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
cut_same (any, replicate (length I) False) (stream_enc (w, I)) @ replicate (max (length (cut_same (any, replicate (length I) False) (stream_enc (w, I)))) (length (cut_same (any, replicate (length I') False) (stream_enc (w', I')))) + 1 - length (cut_same (any, replicate (length I) False) (stream_enc (w, I)))) (any, replicate (length I) False) = cut_same (any, replicate (length I') False) (stream_enc (w', I')) @ replicate (max (length (cut_same (any, replicate (length I) False) (stream_enc (w, I)))) (length (cut_same (any, replicate (length I') False) (stream_enc (w', I')))) + 1 - length (cut_same (any, replicate (length I') False) (stream_enc (w', I')))) (any, replicate (length I') False)
last (cut_same (any, replicate (length I) False) (stream_enc (w, I)) @ replicate (max (length (cut_same (any, replicate (length I) False) (stream_enc (w, I)))) (length (cut_same (any, replicate (length I') False) (stream_enc (w', I')))) + 1 - length (cut_same (any, replicate (length I) False) (stream_enc (w, I)))) (any, replicate (length I) False)) = (any, replicate (length I) False)
last (cut_same (any, replicate (length I') False) (stream_enc (w', I')) @ replicate (max (length (cut_same (any, replicate (length I) False) (stream_enc (w, I)))) (length (cut_same (any, replicate (length I') False) (stream_enc (w', I')))) + 1 - length (cut_same (any, replicate (length I') False) (stream_enc (w', I')))) (any, replicate (length I') False)) = (any, replicate (length I') False)
[PROOF STEP]
show "length I = length I'"
[PROOF STATE]
proof (prove)
using this:
cut_same (any, replicate (length I) False) (stream_enc (w, I)) @ replicate (max (length (cut_same (any, replicate (length I) False) (stream_enc (w, I)))) (length (cut_same (any, replicate (length I') False) (stream_enc (w', I')))) + 1 - length (cut_same (any, replicate (length I) False) (stream_enc (w, I)))) (any, replicate (length I) False) = cut_same (any, replicate (length I') False) (stream_enc (w', I')) @ replicate (max (length (cut_same (any, replicate (length I) False) (stream_enc (w, I)))) (length (cut_same (any, replicate (length I') False) (stream_enc (w', I')))) + 1 - length (cut_same (any, replicate (length I') False) (stream_enc (w', I')))) (any, replicate (length I') False)
last (cut_same (any, replicate (length I) False) (stream_enc (w, I)) @ replicate (max (length (cut_same (any, replicate (length I) False) (stream_enc (w, I)))) (length (cut_same (any, replicate (length I') False) (stream_enc (w', I')))) + 1 - length (cut_same (any, replicate (length I) False) (stream_enc (w, I)))) (any, replicate (length I) False)) = (any, replicate (length I) False)
last (cut_same (any, replicate (length I') False) (stream_enc (w', I')) @ replicate (max (length (cut_same (any, replicate (length I) False) (stream_enc (w, I)))) (length (cut_same (any, replicate (length I') False) (stream_enc (w', I')))) + 1 - length (cut_same (any, replicate (length I') False) (stream_enc (w', I')))) (any, replicate (length I') False)) = (any, replicate (length I') False)

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma enc_stream_enc:
  "\<lbrakk>(\<forall>x \<in> set I. case x of Inr P \<Rightarrow> finite P | _ \<Rightarrow> True);
    (\<forall>x \<in> set I'. case x of Inr P \<Rightarrow> finite P | _ \<Rightarrow> True);
    enc (w, I) = enc (w', I')\<rbrakk> \<Longrightarrow> stream_enc (w, I) = stream_enc (w', I')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>x\<in>set I. case x of Inl a \<Rightarrow> True | Inr P \<Rightarrow> finite P; \<forall>x\<in>set I'. case x of Inl a \<Rightarrow> True | Inr P \<Rightarrow> finite P; enc (w, I) = enc (w', I')\<rbrakk> \<Longrightarrow> stream_enc (w, I) = stream_enc (w', I')
[PROOF STEP]
by (rule box_equals[OF _ sym[OF stream_enc_enc_some] sym[OF stream_enc_enc_some]])
    (auto dest: enc_length simp del: enc.simps)


[STATEMENT]
lemma encD_ex: "\<lbrakk>x \<in> enc (w, I); (\<forall>x \<in> set I. case x of Inr P \<Rightarrow> finite P | _ \<Rightarrow> True)\<rbrakk> \<Longrightarrow>
  \<exists>n. x = map (case_prod (enc_atom I)) (zip [0 ..< n] (stake n (w @- sconst any)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> enc (w, I); \<forall>x\<in>set I. case x of Inl a \<Rightarrow> True | Inr P \<Rightarrow> finite P\<rbrakk> \<Longrightarrow> \<exists>n. x = map2 (enc_atom I) [0..<n] (stake n (w @- sconst any))
[PROOF STEP]
by (auto dest!: encD simp del: enc.simps)


[STATEMENT]
lemma enc_set_\<sigma>: "\<lbrakk>x \<in> enc (w, I); (\<forall>x \<in> set I. case x of Inr P \<Rightarrow> finite P | _ \<Rightarrow> True);
  length I = n; a \<in> set x; set w \<subseteq> set \<Sigma>\<rbrakk> \<Longrightarrow> a \<in> set (\<sigma> \<Sigma> n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> enc (w, I); \<forall>x\<in>set I. case x of Inl a \<Rightarrow> True | Inr P \<Rightarrow> finite P; length I = n; a \<in> set x; set w \<subseteq> set \<Sigma>\<rbrakk> \<Longrightarrow> a \<in> set (\<sigma> \<Sigma> n)
[PROOF STEP]
by (force dest: encD_ex intro: enc_atom_\<sigma> simp: in_set_zip shift_snth simp del: enc.simps)


[STATEMENT]
lemma positions_in_row: "positions_in_row s i = {p. snd (s !! p) ! i}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. positions_in_row s i = {p. snd (s !! p) ! i}
[PROOF STEP]
unfolding positions_in_row_def Option.these_def smap2_szip stream.set_map sset_range
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. the ` {x \<in> range ((!!) (smap (\<lambda>(p, uu_, bs). if bs ! i then Some p else None) (szip nats s))). x \<noteq> None} = {p. snd (s !! p) ! i}
[PROOF STEP]
by (auto split: if_split_asm intro!: image_eqI[of _ the] split: prod.splits)


[STATEMENT]
lemma positions_in_row_unique: "\<exists>!p. snd (s !! p) ! i \<Longrightarrow>
  the_elem (positions_in_row s i) = (THE p. snd (s !! p) ! i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>!p. snd (s !! p) ! i \<Longrightarrow> the_elem (positions_in_row s i) = (THE p. snd (s !! p) ! i)
[PROOF STEP]
by (rule the1I2) (auto simp: the_elem_def positions_in_row)


[STATEMENT]
lemma positions_in_row_nth: "\<exists>!p. snd (s !! p) ! i \<Longrightarrow>
  snd (s !! the_elem (positions_in_row s i)) ! i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>!p. snd (s !! p) ! i \<Longrightarrow> snd (s !! the_elem (positions_in_row s i)) ! i
[PROOF STEP]
unfolding positions_in_row_unique
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>!p. snd (s !! p) ! i \<Longrightarrow> snd (s !! (THE p. snd (s !! p) ! i)) ! i
[PROOF STEP]
by (rule the1I2) auto


[STATEMENT]
lemma dec_word_stream_enc: "dec_word (stream_enc (w, I)) = cut_same any (w @- sconst any)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dec_word (stream_enc (w, I)) = cut_same any (w @- sconst any)
[PROOF STEP]
unfolding dec_word_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cut_same any (smap fst (stream_enc (w, I))) = cut_same any (w @- sconst any)
[PROOF STEP]
by (auto intro!: arg_cong[of _ _ "cut_same any"] simp: smap2_alt)


[STATEMENT]
lemma stream_dec_Inl: "\<lbrakk>i \<in> FO; i < n\<rbrakk> \<Longrightarrow> \<exists>p. stream_dec n FO s ! i = Inl p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>i \<in> FO; i < n\<rbrakk> \<Longrightarrow> \<exists>p. stream_dec n FO s ! i = Inl p
[PROOF STEP]
unfolding stream_dec_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>i \<in> FO; i < n\<rbrakk> \<Longrightarrow> \<exists>p. map (\<lambda>i. if i \<in> FO then Inl (the_elem (positions_in_row s i)) else Inr (positions_in_row s i)) [0..<n] ! i = Inl p
[PROOF STEP]
using nth_map[of n "[0..<n]"]
[PROOF STATE]
proof (prove)
using this:
n < length [0..<n] \<Longrightarrow> map ?f [0..<n] ! n = ?f ([0..<n] ! n)

goal (1 subgoal):
 1. \<lbrakk>i \<in> FO; i < n\<rbrakk> \<Longrightarrow> \<exists>p. map (\<lambda>i. if i \<in> FO then Inl (the_elem (positions_in_row s i)) else Inr (positions_in_row s i)) [0..<n] ! i = Inl p
[PROOF STEP]
by auto


[STATEMENT]
lemma stream_dec_not_Inr: "\<lbrakk>stream_dec n FO s ! i = Inr P; i \<in> FO; i < n\<rbrakk> \<Longrightarrow> False"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>stream_dec n FO s ! i = Inr P; i \<in> FO; i < n\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
unfolding stream_dec_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>map (\<lambda>i. if i \<in> FO then Inl (the_elem (positions_in_row s i)) else Inr (positions_in_row s i)) [0..<n] ! i = Inr P; i \<in> FO; i < n\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
using nth_map[of n "[0..<n]"]
[PROOF STATE]
proof (prove)
using this:
n < length [0..<n] \<Longrightarrow> map ?f [0..<n] ! n = ?f ([0..<n] ! n)

goal (1 subgoal):
 1. \<lbrakk>map (\<lambda>i. if i \<in> FO then Inl (the_elem (positions_in_row s i)) else Inr (positions_in_row s i)) [0..<n] ! i = Inr P; i \<in> FO; i < n\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
by auto


[STATEMENT]
lemma stream_dec_Inr: "\<lbrakk>i \<notin> FO; i < n\<rbrakk> \<Longrightarrow> \<exists>P. stream_dec n FO s ! i = Inr P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>i \<notin> FO; i < n\<rbrakk> \<Longrightarrow> \<exists>P. stream_dec n FO s ! i = Inr P
[PROOF STEP]
unfolding stream_dec_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>i \<notin> FO; i < n\<rbrakk> \<Longrightarrow> \<exists>P. map (\<lambda>i. if i \<in> FO then Inl (the_elem (positions_in_row s i)) else Inr (positions_in_row s i)) [0..<n] ! i = Inr P
[PROOF STEP]
using nth_map[of n "[0..<n]"]
[PROOF STATE]
proof (prove)
using this:
n < length [0..<n] \<Longrightarrow> map ?f [0..<n] ! n = ?f ([0..<n] ! n)

goal (1 subgoal):
 1. \<lbrakk>i \<notin> FO; i < n\<rbrakk> \<Longrightarrow> \<exists>P. map (\<lambda>i. if i \<in> FO then Inl (the_elem (positions_in_row s i)) else Inr (positions_in_row s i)) [0..<n] ! i = Inr P
[PROOF STEP]
by auto


[STATEMENT]
lemma stream_dec_not_Inl: "\<lbrakk>stream_dec n FO s ! i = Inl p; i \<notin> FO; i < n\<rbrakk> \<Longrightarrow> False"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>stream_dec n FO s ! i = Inl p; i \<notin> FO; i < n\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
unfolding stream_dec_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>map (\<lambda>i. if i \<in> FO then Inl (the_elem (positions_in_row s i)) else Inr (positions_in_row s i)) [0..<n] ! i = Inl p; i \<notin> FO; i < n\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
using nth_map[of n "[0..<n]"]
[PROOF STATE]
proof (prove)
using this:
n < length [0..<n] \<Longrightarrow> map ?f [0..<n] ! n = ?f ([0..<n] ! n)

goal (1 subgoal):
 1. \<lbrakk>map (\<lambda>i. if i \<in> FO then Inl (the_elem (positions_in_row s i)) else Inr (positions_in_row s i)) [0..<n] ! i = Inl p; i \<notin> FO; i < n\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
by auto


[STATEMENT]
lemma Inr_dec_finite: "\<lbrakk>\<forall>i<n. finite {p. snd (s !! p) ! i}; Inr P \<in> set (stream_dec n FO s)\<rbrakk> \<Longrightarrow>
  finite P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>i<n. finite {p. snd (s !! p) ! i}; Inr P \<in> set (stream_dec n FO s)\<rbrakk> \<Longrightarrow> finite P
[PROOF STEP]
unfolding stream_dec_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>i<n. finite {p. snd (s !! p) ! i}; Inr P \<in> set (map (\<lambda>i. if i \<in> FO then Inl (the_elem (positions_in_row s i)) else Inr (positions_in_row s i)) [0..<n])\<rbrakk> \<Longrightarrow> finite P
[PROOF STEP]
by (auto simp: positions_in_row)


[STATEMENT]
lemma enc_atom_dec:
  "\<lbrakk>\<forall>p. length (snd (s !! p)) = n; \<forall>i \<in> FO. i < n \<longrightarrow> (\<exists>!p. snd (s !! p) ! i); a = fst (s !! p)\<rbrakk> \<Longrightarrow>
   enc_atom (stream_dec n FO s) p a = s !! p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>p. length (snd (s !! p)) = n; \<forall>i\<in>FO. i < n \<longrightarrow> (\<exists>!p. snd (s !! p) ! i); a = fst (s !! p)\<rbrakk> \<Longrightarrow> enc_atom (stream_dec n FO s) p a = s !! p
[PROOF STEP]
unfolding stream_dec_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>p. length (snd (s !! p)) = n; \<forall>i\<in>FO. i < n \<longrightarrow> (\<exists>!p. snd (s !! p) ! i); a = fst (s !! p)\<rbrakk> \<Longrightarrow> enc_atom (map (\<lambda>i. if i \<in> FO then Inl (the_elem (positions_in_row s i)) else Inr (positions_in_row s i)) [0..<n]) p a = s !! p
[PROOF STEP]
by (rule sym, subst surjective_pairing[of "s !! p"])
    (auto intro!: nth_equalityI simp: positions_in_row simp del: prod.collapse split: if_split_asm,
    (metis positions_in_row positions_in_row_nth)+)


[STATEMENT]
lemma length_stream_dec[simp]: "length (stream_dec n FO x) = n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (stream_dec n FO x) = n
[PROOF STEP]
unfolding stream_dec_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (map (\<lambda>i. if i \<in> FO then Inl (the_elem (positions_in_row x i)) else Inr (positions_in_row x i)) [0..<n]) = n
[PROOF STEP]
by auto


[STATEMENT]
lemma stream_enc_dec:
  "\<lbrakk>\<exists>n. sdrop n (smap fst s) = sconst any;
   stream_all (\<lambda>x. length (snd x) = n) s; \<forall>i \<in> FO. (\<exists>!p. snd (s !! p) ! i)\<rbrakk> \<Longrightarrow>
   stream_enc (dec_word s, stream_dec n FO s) = s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<exists>n. sdrop n (smap fst s) = sconst any; stream_all (\<lambda>x. length (snd x) = n) s; \<forall>i\<in>FO. \<exists>!p. snd (s !! p) ! i\<rbrakk> \<Longrightarrow> stream_enc (dec_word s, stream_dec n FO s) = s
[PROOF STEP]
unfolding dec_word_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<exists>n. sdrop n (smap fst s) = sconst any; stream_all (\<lambda>x. length (snd x) = n) s; \<forall>i\<in>FO. \<exists>!p. snd (s !! p) ! i\<rbrakk> \<Longrightarrow> stream_enc (cut_same any (smap fst s), stream_dec n FO s) = s
[PROOF STEP]
by (drule LeastI_ex)
    (auto intro!: enc_atom_dec simp: smap2_alt cut_same_def
    simp del: stake_smap sdrop_smap
    intro!: trans[OF arg_cong2[of _ _ _ _ "(!!)"] snth_smap]
            trans[OF arg_cong2[of _ _ _ _ "(@-)"] stake_sdrop])


[STATEMENT]
lemma stream_enc_unique:
  "i < length I \<Longrightarrow> \<exists>p. I ! i = Inl p \<Longrightarrow> \<exists>!p. snd (stream_enc (w, I) !! p) ! i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>i < length I; \<exists>p. I ! i = Inl p\<rbrakk> \<Longrightarrow> \<exists>!p. snd (stream_enc (w, I) !! p) ! i
[PROOF STEP]
by auto


[STATEMENT]
lemma stream_dec_enc_Inl:
  "\<lbrakk>stream_dec n FO (stream_enc (w, I)) ! i = Inl p'; I ! i = Inl p; i \<in> FO; i < n; length I = n\<rbrakk> \<Longrightarrow>
  p = p'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>stream_dec n FO (stream_enc (w, I)) ! i = Inl p'; I ! i = Inl p; i \<in> FO; i < n; length I = n\<rbrakk> \<Longrightarrow> p = p'
[PROOF STEP]
unfolding stream_dec_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>map (\<lambda>i. if i \<in> FO then Inl (the_elem (positions_in_row (stream_enc (w, I)) i)) else Inr (positions_in_row (stream_enc (w, I)) i)) [0..<n] ! i = Inl p'; I ! i = Inl p; i \<in> FO; i < n; length I = n\<rbrakk> \<Longrightarrow> p = p'
[PROOF STEP]
by (auto intro!: trans[OF _ sym[OF  positions_in_row_unique[OF stream_enc_unique]]]
    simp del: stream_enc.simps) simp


[STATEMENT]
lemma stream_dec_enc_Inr:
  "\<lbrakk>stream_dec n FO (stream_enc (w, I)) ! i = Inr P'; I ! i = Inr P; i \<notin> FO; i < n; length I = n\<rbrakk> \<Longrightarrow>
  P = P'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>stream_dec n FO (stream_enc (w, I)) ! i = Inr P'; I ! i = Inr P; i \<notin> FO; i < n; length I = n\<rbrakk> \<Longrightarrow> P = P'
[PROOF STEP]
unfolding stream_dec_def positions_in_row
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>map (\<lambda>i. if i \<in> FO then Inl (the_elem {p. snd (stream_enc (w, I) !! p) ! i}) else Inr {p. snd (stream_enc (w, I) !! p) ! i}) [0..<n] ! i = Inr P'; I ! i = Inr P; i \<notin> FO; i < n; length I = n\<rbrakk> \<Longrightarrow> P = P'
[PROOF STEP]
by auto


[STATEMENT]
lemma Collect_snth: "{p. P ((x ## s) !! p)} \<subseteq> {0} \<union> Suc ` {p. P (s !! p)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {p. P ((x ## s) !! p)} \<subseteq> {0} \<union> Suc ` {p. P (s !! p)}
[PROOF STEP]
unfolding image_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {p. P ((x ## s) !! p)} \<subseteq> {0} \<union> {y. \<exists>x\<in>{p. P (s !! p)}. y = Suc x}
[PROOF STEP]
by (auto simp: gr0_conv_Suc)


[STATEMENT]
lemma finite_True_in_row: "\<forall>i < n. finite {p. snd ((w @- sconst (any, replicate n False)) !! p) ! i}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i<n. finite {p. snd ((w @- sconst (any, replicate n False)) !! p) ! i}
[PROOF STEP]
by (induct w) (auto simp: id_def[symmetric] intro: finite_subset[OF Collect_snth])


[STATEMENT]
lemma lang_ENC:
 assumes "FO \<subseteq> {0 ..< n}" "SO \<subseteq> {0 ..< n} - FO"
 shows "lang n (ENC n FO) = \<Union>{enc (w, I) | w I . length I = n \<and> wf_interp w I \<and>
   (\<forall>i \<in> FO. case I ! i of Inl _ \<Rightarrow> True | Inr _ \<Rightarrow> False) \<and>
   (\<forall>i \<in> SO. case I ! i of Inl _ \<Rightarrow> False | Inr _ \<Rightarrow> True)}"
   (is "?L = ?R")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lang n (ENC n FO) = \<Union> {enc (w, I) |w I. length I = n \<and> wf_interp w I \<and> (\<forall>i\<in>FO. case I ! i of Inl x \<Rightarrow> True | Inr x \<Rightarrow> False) \<and> (\<forall>i\<in>SO. case I ! i of Inl x \<Rightarrow> False | Inr x \<Rightarrow> True)}
[PROOF STEP]
proof (intro equalityI subsetI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. x \<in> lang n (ENC n FO) \<Longrightarrow> x \<in> \<Union> {enc (w, I) |w I. length I = n \<and> wf_interp w I \<and> (\<forall>i\<in>FO. case I ! i of Inl x \<Rightarrow> True | Inr x \<Rightarrow> False) \<and> (\<forall>i\<in>SO. case I ! i of Inl x \<Rightarrow> False | Inr x \<Rightarrow> True)}
 2. \<And>x. x \<in> \<Union> {enc (w, I) |w I. length I = n \<and> wf_interp w I \<and> (\<forall>i\<in>FO. case I ! i of Inl x \<Rightarrow> True | Inr x \<Rightarrow> False) \<and> (\<forall>i\<in>SO. case I ! i of Inl x \<Rightarrow> False | Inr x \<Rightarrow> True)} \<Longrightarrow> x \<in> lang n (ENC n FO)
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. x \<in> lang n (ENC n FO) \<Longrightarrow> x \<in> \<Union> {enc (w, I) |w I. length I = n \<and> wf_interp w I \<and> (\<forall>i\<in>FO. case I ! i of Inl x \<Rightarrow> True | Inr x \<Rightarrow> False) \<and> (\<forall>i\<in>SO. case I ! i of Inl x \<Rightarrow> False | Inr x \<Rightarrow> True)}
 2. \<And>x. x \<in> \<Union> {enc (w, I) |w I. length I = n \<and> wf_interp w I \<and> (\<forall>i\<in>FO. case I ! i of Inl x \<Rightarrow> True | Inr x \<Rightarrow> False) \<and> (\<forall>i\<in>SO. case I ! i of Inl x \<Rightarrow> False | Inr x \<Rightarrow> True)} \<Longrightarrow> x \<in> lang n (ENC n FO)
[PROOF STEP]
assume L: "x \<in> ?L"
[PROOF STATE]
proof (state)
this:
x \<in> lang n (ENC n FO)

goal (2 subgoals):
 1. \<And>x. x \<in> lang n (ENC n FO) \<Longrightarrow> x \<in> \<Union> {enc (w, I) |w I. length I = n \<and> wf_interp w I \<and> (\<forall>i\<in>FO. case I ! i of Inl x \<Rightarrow> True | Inr x \<Rightarrow> False) \<and> (\<forall>i\<in>SO. case I ! i of Inl x \<Rightarrow> False | Inr x \<Rightarrow> True)}
 2. \<And>x. x \<in> \<Union> {enc (w, I) |w I. length I = n \<and> wf_interp w I \<and> (\<forall>i\<in>FO. case I ! i of Inl x \<Rightarrow> True | Inr x \<Rightarrow> False) \<and> (\<forall>i\<in>SO. case I ! i of Inl x \<Rightarrow> False | Inr x \<Rightarrow> True)} \<Longrightarrow> x \<in> lang n (ENC n FO)
[PROOF STEP]
from assms(1)
[PROOF STATE]
proof (chain)
picking this:
FO \<subseteq> {0..<n}
[PROOF STEP]
have fin: "finite FO"
[PROOF STATE]
proof (prove)
using this:
FO \<subseteq> {0..<n}

goal (1 subgoal):
 1. finite FO
[PROOF STEP]
by (auto simp: finite_subset)
[PROOF STATE]
proof (state)
this:
finite FO

goal (2 subgoals):
 1. \<And>x. x \<in> lang n (ENC n FO) \<Longrightarrow> x \<in> \<Union> {enc (w, I) |w I. length I = n \<and> wf_interp w I \<and> (\<forall>i\<in>FO. case I ! i of Inl x \<Rightarrow> True | Inr x \<Rightarrow> False) \<and> (\<forall>i\<in>SO. case I ! i of Inl x \<Rightarrow> False | Inr x \<Rightarrow> True)}
 2. \<And>x. x \<in> \<Union> {enc (w, I) |w I. length I = n \<and> wf_interp w I \<and> (\<forall>i\<in>FO. case I ! i of Inl x \<Rightarrow> True | Inr x \<Rightarrow> False) \<and> (\<forall>i\<in>SO. case I ! i of Inl x \<Rightarrow> False | Inr x \<Rightarrow> True)} \<Longrightarrow> x \<in> lang n (ENC n FO)
[PROOF STEP]
have *: "set x \<subseteq> set (\<sigma> \<Sigma> n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set x \<subseteq> set (\<sigma> \<Sigma> n)
[PROOF STEP]
using subsetD[OF assms(1)]
    bspec[OF wf_lang_wf_word[OF wf_rexp_ENC[OF fin]] L]
[PROOF STATE]
proof (prove)
using this:
?c \<in> FO \<Longrightarrow> ?c \<in> {0..<n}
n = 0 \<or> (\<forall>v\<in>FO. v < n) \<Longrightarrow> wf_word n x

goal (1 subgoal):
 1. set x \<subseteq> set (\<sigma> \<Sigma> n)
[PROOF STEP]
by (cases n) (auto simp: wf_word)
[PROOF STATE]
proof (state)
this:
set x \<subseteq> set (\<sigma> \<Sigma> n)

goal (2 subgoals):
 1. \<And>x. x \<in> lang n (ENC n FO) \<Longrightarrow> x \<in> \<Union> {enc (w, I) |w I. length I = n \<and> wf_interp w I \<and> (\<forall>i\<in>FO. case I ! i of Inl x \<Rightarrow> True | Inr x \<Rightarrow> False) \<and> (\<forall>i\<in>SO. case I ! i of Inl x \<Rightarrow> False | Inr x \<Rightarrow> True)}
 2. \<And>x. x \<in> \<Union> {enc (w, I) |w I. length I = n \<and> wf_interp w I \<and> (\<forall>i\<in>FO. case I ! i of Inl x \<Rightarrow> True | Inr x \<Rightarrow> False) \<and> (\<forall>i\<in>SO. case I ! i of Inl x \<Rightarrow> False | Inr x \<Rightarrow> True)} \<Longrightarrow> x \<in> lang n (ENC n FO)
[PROOF STEP]
let ?s = "x @- sconst (any, replicate n False)"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. x \<in> lang n (ENC n FO) \<Longrightarrow> x \<in> \<Union> {enc (w, I) |w I. length I = n \<and> wf_interp w I \<and> (\<forall>i\<in>FO. case I ! i of Inl x \<Rightarrow> True | Inr x \<Rightarrow> False) \<and> (\<forall>i\<in>SO. case I ! i of Inl x \<Rightarrow> False | Inr x \<Rightarrow> True)}
 2. \<And>x. x \<in> \<Union> {enc (w, I) |w I. length I = n \<and> wf_interp w I \<and> (\<forall>i\<in>FO. case I ! i of Inl x \<Rightarrow> True | Inr x \<Rightarrow> False) \<and> (\<forall>i\<in>SO. case I ! i of Inl x \<Rightarrow> False | Inr x \<Rightarrow> True)} \<Longrightarrow> x \<in> lang n (ENC n FO)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
FO \<subseteq> {0..<n}
SO \<subseteq> {0..<n} - FO
[PROOF STEP]
have "list_all (\<lambda>bs. length (snd bs) = n) x"
[PROOF STATE]
proof (prove)
using this:
FO \<subseteq> {0..<n}
SO \<subseteq> {0..<n} - FO

goal (1 subgoal):
 1. list_all (\<lambda>bs. length (snd bs) = n) x
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
FO \<subseteq> {0..<n}
SO \<subseteq> {0..<n} - FO
set x \<subseteq> set (\<sigma> \<Sigma> n)

goal (1 subgoal):
 1. list_all (\<lambda>bs. length (snd bs) = n) x
[PROOF STEP]
by (auto simp: list_all_iff \<sigma>_def set_n_lists)
[PROOF STATE]
proof (state)
this:
list_all (\<lambda>bs. length (snd bs) = n) x

goal (2 subgoals):
 1. \<And>x. x \<in> lang n (ENC n FO) \<Longrightarrow> x \<in> \<Union> {enc (w, I) |w I. length I = n \<and> wf_interp w I \<and> (\<forall>i\<in>FO. case I ! i of Inl x \<Rightarrow> True | Inr x \<Rightarrow> False) \<and> (\<forall>i\<in>SO. case I ! i of Inl x \<Rightarrow> False | Inr x \<Rightarrow> True)}
 2. \<And>x. x \<in> \<Union> {enc (w, I) |w I. length I = n \<and> wf_interp w I \<and> (\<forall>i\<in>FO. case I ! i of Inl x \<Rightarrow> True | Inr x \<Rightarrow> False) \<and> (\<forall>i\<in>SO. case I ! i of Inl x \<Rightarrow> False | Inr x \<Rightarrow> True)} \<Longrightarrow> x \<in> lang n (ENC n FO)
[PROOF STEP]
hence "stream_all (\<lambda>x. length (snd x) = n) (x @- sconst (any, replicate n False))"
[PROOF STATE]
proof (prove)
using this:
list_all (\<lambda>bs. length (snd bs) = n) x

goal (1 subgoal):
 1. stream_all (\<lambda>x. length (snd x) = n) (x @- sconst (any, replicate n False))
[PROOF STEP]
by (auto simp only: stream_all_shift sset_sconst length_replicate snd_conv)
[PROOF STATE]
proof (state)
this:
stream_all (\<lambda>x. length (snd x) = n) (x @- sconst (any, replicate n False))

goal (2 subgoals):
 1. \<And>x. x \<in> lang n (ENC n FO) \<Longrightarrow> x \<in> \<Union> {enc (w, I) |w I. length I = n \<and> wf_interp w I \<and> (\<forall>i\<in>FO. case I ! i of Inl x \<Rightarrow> True | Inr x \<Rightarrow> False) \<and> (\<forall>i\<in>SO. case I ! i of Inl x \<Rightarrow> False | Inr x \<Rightarrow> True)}
 2. \<And>x. x \<in> \<Union> {enc (w, I) |w I. length I = n \<and> wf_interp w I \<and> (\<forall>i\<in>FO. case I ! i of Inl x \<Rightarrow> True | Inr x \<Rightarrow> False) \<and> (\<forall>i\<in>SO. case I ! i of Inl x \<Rightarrow> False | Inr x \<Rightarrow> True)} \<Longrightarrow> x \<in> lang n (ENC n FO)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
stream_all (\<lambda>x. length (snd x) = n) (x @- sconst (any, replicate n False))

goal (2 subgoals):
 1. \<And>x. x \<in> lang n (ENC n FO) \<Longrightarrow> x \<in> \<Union> {enc (w, I) |w I. length I = n \<and> wf_interp w I \<and> (\<forall>i\<in>FO. case I ! i of Inl x \<Rightarrow> True | Inr x \<Rightarrow> False) \<and> (\<forall>i\<in>SO. case I ! i of Inl x \<Rightarrow> False | Inr x \<Rightarrow> True)}
 2. \<And>x. x \<in> \<Union> {enc (w, I) |w I. length I = n \<and> wf_interp w I \<and> (\<forall>i\<in>FO. case I ! i of Inl x \<Rightarrow> True | Inr x \<Rightarrow> False) \<and> (\<forall>i\<in>SO. case I ! i of Inl x \<Rightarrow> False | Inr x \<Rightarrow> True)} \<Longrightarrow> x \<in> lang n (ENC n FO)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
stream_all (\<lambda>x. length (snd x) = n) (x @- sconst (any, replicate n False))

goal (2 subgoals):
 1. \<And>x. x \<in> lang n (ENC n FO) \<Longrightarrow> x \<in> \<Union> {enc (w, I) |w I. length I = n \<and> wf_interp w I \<and> (\<forall>i\<in>FO. case I ! i of Inl x \<Rightarrow> True | Inr x \<Rightarrow> False) \<and> (\<forall>i\<in>SO. case I ! i of Inl x \<Rightarrow> False | Inr x \<Rightarrow> True)}
 2. \<And>x. x \<in> \<Union> {enc (w, I) |w I. length I = n \<and> wf_interp w I \<and> (\<forall>i\<in>FO. case I ! i of Inl x \<Rightarrow> True | Inr x \<Rightarrow> False) \<and> (\<forall>i\<in>SO. case I ! i of Inl x \<Rightarrow> False | Inr x \<Rightarrow> True)} \<Longrightarrow> x \<in> lang n (ENC n FO)
[PROOF STEP]
fix m
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. x \<in> lang n (ENC n FO) \<Longrightarrow> x \<in> \<Union> {enc (w, I) |w I. length I = n \<and> wf_interp w I \<and> (\<forall>i\<in>FO. case I ! i of Inl x \<Rightarrow> True | Inr x \<Rightarrow> False) \<and> (\<forall>i\<in>SO. case I ! i of Inl x \<Rightarrow> False | Inr x \<Rightarrow> True)}
 2. \<And>x. x \<in> \<Union> {enc (w, I) |w I. length I = n \<and> wf_interp w I \<and> (\<forall>i\<in>FO. case I ! i of Inl x \<Rightarrow> True | Inr x \<Rightarrow> False) \<and> (\<forall>i\<in>SO. case I ! i of Inl x \<Rightarrow> False | Inr x \<Rightarrow> True)} \<Longrightarrow> x \<in> lang n (ENC n FO)
[PROOF STEP]
assume "m \<in> FO"
[PROOF STATE]
proof (state)
this:
m \<in> FO

goal (2 subgoals):
 1. \<And>x. x \<in> lang n (ENC n FO) \<Longrightarrow> x \<in> \<Union> {enc (w, I) |w I. length I = n \<and> wf_interp w I \<and> (\<forall>i\<in>FO. case I ! i of Inl x \<Rightarrow> True | Inr x \<Rightarrow> False) \<and> (\<forall>i\<in>SO. case I ! i of Inl x \<Rightarrow> False | Inr x \<Rightarrow> True)}
 2. \<And>x. x \<in> \<Union> {enc (w, I) |w I. length I = n \<and> wf_interp w I \<and> (\<forall>i\<in>FO. case I ! i of Inl x \<Rightarrow> True | Inr x \<Rightarrow> False) \<and> (\<forall>i\<in>SO. case I ! i of Inl x \<Rightarrow> False | Inr x \<Rightarrow> True)} \<Longrightarrow> x \<in> lang n (ENC n FO)
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
FO \<subseteq> {0..<n}
SO \<subseteq> {0..<n} - FO
m \<in> FO
[PROOF STEP]
have "m < n"
[PROOF STATE]
proof (prove)
using this:
FO \<subseteq> {0..<n}
SO \<subseteq> {0..<n} - FO
m \<in> FO

goal (1 subgoal):
 1. m < n
[PROOF STEP]
by (auto simp: max_idx_vars)
[PROOF STATE]
proof (state)
this:
m < n

goal (2 subgoals):
 1. \<And>x. x \<in> lang n (ENC n FO) \<Longrightarrow> x \<in> \<Union> {enc (w, I) |w I. length I = n \<and> wf_interp w I \<and> (\<forall>i\<in>FO. case I ! i of Inl x \<Rightarrow> True | Inr x \<Rightarrow> False) \<and> (\<forall>i\<in>SO. case I ! i of Inl x \<Rightarrow> False | Inr x \<Rightarrow> True)}
 2. \<And>x. x \<in> \<Union> {enc (w, I) |w I. length I = n \<and> wf_interp w I \<and> (\<forall>i\<in>FO. case I ! i of Inl x \<Rightarrow> True | Inr x \<Rightarrow> False) \<and> (\<forall>i\<in>SO. case I ! i of Inl x \<Rightarrow> False | Inr x \<Rightarrow> True)} \<Longrightarrow> x \<in> lang n (ENC n FO)
[PROOF STEP]
with L \<open>m \<in> FO\<close> assms
[PROOF STATE]
proof (chain)
picking this:
x \<in> lang n (ENC n FO)
m \<in> FO
FO \<subseteq> {0..<n}
SO \<subseteq> {0..<n} - FO
m < n
[PROOF STEP]
obtain u z v where uzv: "x = u @ z @ v"
      "u \<in> star (lang n (Atom (Arbitrary_Except m False)))"
      "z \<in> lang n (Atom (Arbitrary_Except m True))"
      "v \<in> star (lang n (Atom (Arbitrary_Except m False)))"
[PROOF STATE]
proof (prove)
using this:
x \<in> lang n (ENC n FO)
m \<in> FO
FO \<subseteq> {0..<n}
SO \<subseteq> {0..<n} - FO
m < n

goal (1 subgoal):
 1. (\<And>u z v. \<lbrakk>x = u @ z @ v; u \<in> star (lang n (Atom (Arbitrary_Except m False))); z \<in> lang n (Atom (Arbitrary_Except m True)); v \<in> star (lang n (Atom (Arbitrary_Except m False)))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding ENC_def
[PROOF STATE]
proof (prove)
using this:
x \<in> lang n (INTERSECT (sorted_list_of_set (valid_ENC n ` FO)))
m \<in> FO
FO \<subseteq> {0..<n}
SO \<subseteq> {0..<n} - FO
m < n

goal (1 subgoal):
 1. (\<And>u z v. \<lbrakk>x = u @ z @ v; u \<in> star (lang n (Atom (Arbitrary_Except m False))); z \<in> lang n (Atom (Arbitrary_Except m True)); v \<in> star (lang n (Atom (Arbitrary_Except m False)))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases n)
       (auto simp: not_less max_idx_vars valid_ENC_def fin intro!: wf_rexp_valid_ENC finite_FOV
        dest!: iffD1[OF lang_flatten_INTERSECT, rotated -1], fast)
[PROOF STATE]
proof (state)
this:
x = u @ z @ v
u \<in> star (lang n (Atom (Arbitrary_Except m False)))
z \<in> lang n (Atom (Arbitrary_Except m True))
v \<in> star (lang n (Atom (Arbitrary_Except m False)))

goal (2 subgoals):
 1. \<And>x. x \<in> lang n (ENC n FO) \<Longrightarrow> x \<in> \<Union> {enc (w, I) |w I. length I = n \<and> wf_interp w I \<and> (\<forall>i\<in>FO. case I ! i of Inl x \<Rightarrow> True | Inr x \<Rightarrow> False) \<and> (\<forall>i\<in>SO. case I ! i of Inl x \<Rightarrow> False | Inr x \<Rightarrow> True)}
 2. \<And>x. x \<in> \<Union> {enc (w, I) |w I. length I = n \<and> wf_interp w I \<and> (\<forall>i\<in>FO. case I ! i of Inl x \<Rightarrow> True | Inr x \<Rightarrow> False) \<and> (\<forall>i\<in>SO. case I ! i of Inl x \<Rightarrow> False | Inr x \<Rightarrow> True)} \<Longrightarrow> x \<in> lang n (ENC n FO)
[PROOF STEP]
with \<open>m < n\<close>
[PROOF STATE]
proof (chain)
picking this:
m < n
x = u @ z @ v
u \<in> star (lang n (Atom (Arbitrary_Except m False)))
z \<in> lang n (Atom (Arbitrary_Except m True))
v \<in> star (lang n (Atom (Arbitrary_Except m False)))
[PROOF STEP]
have "\<exists>!p.  snd (x ! p) ! m \<and> p < length x"
[PROOF STATE]
proof (prove)
using this:
m < n
x = u @ z @ v
u \<in> star (lang n (Atom (Arbitrary_Except m False)))
z \<in> lang n (Atom (Arbitrary_Except m True))
v \<in> star (lang n (Atom (Arbitrary_Except m False)))

goal (1 subgoal):
 1. \<exists>!p. snd (x ! p) ! m \<and> p < length x
[PROOF STEP]
proof (intro ex1I[of _ "length u"])
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>m < n; x = u @ z @ v; u \<in> star (lang n (Atom (Arbitrary_Except m False))); z \<in> lang n (Atom (Arbitrary_Except m True)); v \<in> star (lang n (Atom (Arbitrary_Except m False)))\<rbrakk> \<Longrightarrow> snd (x ! length u) ! m \<and> length u < length x
 2. \<And>p. \<lbrakk>m < n; x = u @ z @ v; u \<in> star (lang n (Atom (Arbitrary_Except m False))); z \<in> lang n (Atom (Arbitrary_Except m True)); v \<in> star (lang n (Atom (Arbitrary_Except m False))); snd (x ! p) ! m \<and> p < length x\<rbrakk> \<Longrightarrow> p = length u
[PROOF STEP]
fix p
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>m < n; x = u @ z @ v; u \<in> star (lang n (Atom (Arbitrary_Except m False))); z \<in> lang n (Atom (Arbitrary_Except m True)); v \<in> star (lang n (Atom (Arbitrary_Except m False)))\<rbrakk> \<Longrightarrow> snd (x ! length u) ! m \<and> length u < length x
 2. \<And>p. \<lbrakk>m < n; x = u @ z @ v; u \<in> star (lang n (Atom (Arbitrary_Except m False))); z \<in> lang n (Atom (Arbitrary_Except m True)); v \<in> star (lang n (Atom (Arbitrary_Except m False))); snd (x ! p) ! m \<and> p < length x\<rbrakk> \<Longrightarrow> p = length u
[PROOF STEP]
assume "m < n" "snd (x ! p) ! m \<and> p < length x"
[PROOF STATE]
proof (state)
this:
m < n
snd (x ! p) ! m \<and> p < length x

goal (2 subgoals):
 1. \<lbrakk>m < n; x = u @ z @ v; u \<in> star (lang n (Atom (Arbitrary_Except m False))); z \<in> lang n (Atom (Arbitrary_Except m True)); v \<in> star (lang n (Atom (Arbitrary_Except m False)))\<rbrakk> \<Longrightarrow> snd (x ! length u) ! m \<and> length u < length x
 2. \<And>p. \<lbrakk>m < n; x = u @ z @ v; u \<in> star (lang n (Atom (Arbitrary_Except m False))); z \<in> lang n (Atom (Arbitrary_Except m True)); v \<in> star (lang n (Atom (Arbitrary_Except m False))); snd (x ! p) ! m \<and> p < length x\<rbrakk> \<Longrightarrow> p = length u
[PROOF STEP]
with star_Arbitrary_ExceptD[OF uzv(2)] Arbitrary_ExceptD[OF uzv(3)] star_Arbitrary_ExceptD[OF uzv(4)]
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>m < n; ?i < length u\<rbrakk> \<Longrightarrow> snd (u ! ?i) ! m = False
m < n \<Longrightarrow> \<exists>x. z = [x] \<and> snd x ! m = True
\<lbrakk>m < n; ?i < length v\<rbrakk> \<Longrightarrow> snd (v ! ?i) ! m = False
m < n
snd (x ! p) ! m \<and> p < length x
[PROOF STEP]
show "p = length u"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>m < n; ?i < length u\<rbrakk> \<Longrightarrow> snd (u ! ?i) ! m = False
m < n \<Longrightarrow> \<exists>x. z = [x] \<and> snd x ! m = True
\<lbrakk>m < n; ?i < length v\<rbrakk> \<Longrightarrow> snd (v ! ?i) ! m = False
m < n
snd (x ! p) ! m \<and> p < length x

goal (1 subgoal):
 1. p = length u
[PROOF STEP]
by (cases rule: linorder_cases) (auto simp: nth_append uzv(1))
[PROOF STATE]
proof (state)
this:
p = length u

goal (1 subgoal):
 1. \<lbrakk>m < n; x = u @ z @ v; u \<in> star (lang n (Atom (Arbitrary_Except m False))); z \<in> lang n (Atom (Arbitrary_Except m True)); v \<in> star (lang n (Atom (Arbitrary_Except m False)))\<rbrakk> \<Longrightarrow> snd (x ! length u) ! m \<and> length u < length x
[PROOF STEP]
qed (auto dest!: Arbitrary_ExceptD)
[PROOF STATE]
proof (state)
this:
\<exists>!p. snd (x ! p) ! m \<and> p < length x

goal (2 subgoals):
 1. \<And>x. x \<in> lang n (ENC n FO) \<Longrightarrow> x \<in> \<Union> {enc (w, I) |w I. length I = n \<and> wf_interp w I \<and> (\<forall>i\<in>FO. case I ! i of Inl x \<Rightarrow> True | Inr x \<Rightarrow> False) \<and> (\<forall>i\<in>SO. case I ! i of Inl x \<Rightarrow> False | Inr x \<Rightarrow> True)}
 2. \<And>x. x \<in> \<Union> {enc (w, I) |w I. length I = n \<and> wf_interp w I \<and> (\<forall>i\<in>FO. case I ! i of Inl x \<Rightarrow> True | Inr x \<Rightarrow> False) \<and> (\<forall>i\<in>SO. case I ! i of Inl x \<Rightarrow> False | Inr x \<Rightarrow> True)} \<Longrightarrow> x \<in> lang n (ENC n FO)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>!p. snd (x ! p) ! m \<and> p < length x
[PROOF STEP]
obtain p where p: "p < length x" "snd (x ! p) ! m"
      "\<And>q. snd (x ! q) ! m \<and> q < length x \<longrightarrow> q = p"
[PROOF STATE]
proof (prove)
using this:
\<exists>!p. snd (x ! p) ! m \<and> p < length x

goal (1 subgoal):
 1. (\<And>p. \<lbrakk>p < length x; snd (x ! p) ! m; \<And>q. snd (x ! q) ! m \<and> q < length x \<longrightarrow> q = p\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
p < length x
snd (x ! p) ! m
snd (x ! ?q2) ! m \<and> ?q2 < length x \<longrightarrow> ?q2 = p

goal (2 subgoals):
 1. \<And>x. x \<in> lang n (ENC n FO) \<Longrightarrow> x \<in> \<Union> {enc (w, I) |w I. length I = n \<and> wf_interp w I \<and> (\<forall>i\<in>FO. case I ! i of Inl x \<Rightarrow> True | Inr x \<Rightarrow> False) \<and> (\<forall>i\<in>SO. case I ! i of Inl x \<Rightarrow> False | Inr x \<Rightarrow> True)}
 2. \<And>x. x \<in> \<Union> {enc (w, I) |w I. length I = n \<and> wf_interp w I \<and> (\<forall>i\<in>FO. case I ! i of Inl x \<Rightarrow> True | Inr x \<Rightarrow> False) \<and> (\<forall>i\<in>SO. case I ! i of Inl x \<Rightarrow> False | Inr x \<Rightarrow> True)} \<Longrightarrow> x \<in> lang n (ENC n FO)
[PROOF STEP]
from this(1,2)
[PROOF STATE]
proof (chain)
picking this:
p < length x
snd (x ! p) ! m
[PROOF STEP]
have "\<exists>!p. snd (?s !! p) ! m"
[PROOF STATE]
proof (prove)
using this:
p < length x
snd (x ! p) ! m

goal (1 subgoal):
 1. \<exists>!p. snd ((x @- sconst (any, replicate n False)) !! p) ! m
[PROOF STEP]
proof (intro ex1I[of _ p])
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>p < length x; snd (x ! p) ! m\<rbrakk> \<Longrightarrow> snd ((x @- sconst (any, replicate n False)) !! p) ! m
 2. \<And>pa. \<lbrakk>p < length x; snd (x ! p) ! m; snd ((x @- sconst (any, replicate n False)) !! pa) ! m\<rbrakk> \<Longrightarrow> pa = p
[PROOF STEP]
fix q
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>p < length x; snd (x ! p) ! m\<rbrakk> \<Longrightarrow> snd ((x @- sconst (any, replicate n False)) !! p) ! m
 2. \<And>pa. \<lbrakk>p < length x; snd (x ! p) ! m; snd ((x @- sconst (any, replicate n False)) !! pa) ! m\<rbrakk> \<Longrightarrow> pa = p
[PROOF STEP]
from p(1,2) p(3)[of q] \<open>m < n\<close>
[PROOF STATE]
proof (chain)
picking this:
p < length x
snd (x ! p) ! m
snd (x ! q) ! m \<and> q < length x \<longrightarrow> q = p
m < n
[PROOF STEP]
show "snd (?s !! q) ! m \<Longrightarrow> q = p"
[PROOF STATE]
proof (prove)
using this:
p < length x
snd (x ! p) ! m
snd (x ! q) ! m \<and> q < length x \<longrightarrow> q = p
m < n

goal (1 subgoal):
 1. snd ((x @- sconst (any, replicate n False)) !! q) ! m \<Longrightarrow> q = p
[PROOF STEP]
by (cases "q < length x")  auto
[PROOF STATE]
proof (state)
this:
snd ((x @- sconst (any, replicate n False)) !! q) ! m \<Longrightarrow> q = p

goal (1 subgoal):
 1. \<lbrakk>p < length x; snd (x ! p) ! m\<rbrakk> \<Longrightarrow> snd ((x @- sconst (any, replicate n False)) !! p) ! m
[PROOF STEP]
qed auto
[PROOF STATE]
proof (state)
this:
\<exists>!p. snd ((x @- sconst (any, replicate n False)) !! p) ! m

goal (2 subgoals):
 1. \<And>x. x \<in> lang n (ENC n FO) \<Longrightarrow> x \<in> \<Union> {enc (w, I) |w I. length I = n \<and> wf_interp w I \<and> (\<forall>i\<in>FO. case I ! i of Inl x \<Rightarrow> True | Inr x \<Rightarrow> False) \<and> (\<forall>i\<in>SO. case I ! i of Inl x \<Rightarrow> False | Inr x \<Rightarrow> True)}
 2. \<And>x. x \<in> \<Union> {enc (w, I) |w I. length I = n \<and> wf_interp w I \<and> (\<forall>i\<in>FO. case I ! i of Inl x \<Rightarrow> True | Inr x \<Rightarrow> False) \<and> (\<forall>i\<in>SO. case I ! i of Inl x \<Rightarrow> False | Inr x \<Rightarrow> True)} \<Longrightarrow> x \<in> lang n (ENC n FO)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?m4 \<in> FO \<Longrightarrow> \<exists>!p. snd ((x @- sconst (any, replicate n False)) !! p) ! ?m4

goal (2 subgoals):
 1. \<And>x. x \<in> lang n (ENC n FO) \<Longrightarrow> x \<in> \<Union> {enc (w, I) |w I. length I = n \<and> wf_interp w I \<and> (\<forall>i\<in>FO. case I ! i of Inl x \<Rightarrow> True | Inr x \<Rightarrow> False) \<and> (\<forall>i\<in>SO. case I ! i of Inl x \<Rightarrow> False | Inr x \<Rightarrow> True)}
 2. \<And>x. x \<in> \<Union> {enc (w, I) |w I. length I = n \<and> wf_interp w I \<and> (\<forall>i\<in>FO. case I ! i of Inl x \<Rightarrow> True | Inr x \<Rightarrow> False) \<and> (\<forall>i\<in>SO. case I ! i of Inl x \<Rightarrow> False | Inr x \<Rightarrow> True)} \<Longrightarrow> x \<in> lang n (ENC n FO)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
?m4 \<in> FO \<Longrightarrow> \<exists>!p. snd ((x @- sconst (any, replicate n False)) !! p) ! ?m4

goal (2 subgoals):
 1. \<And>x. x \<in> lang n (ENC n FO) \<Longrightarrow> x \<in> \<Union> {enc (w, I) |w I. length I = n \<and> wf_interp w I \<and> (\<forall>i\<in>FO. case I ! i of Inl x \<Rightarrow> True | Inr x \<Rightarrow> False) \<and> (\<forall>i\<in>SO. case I ! i of Inl x \<Rightarrow> False | Inr x \<Rightarrow> True)}
 2. \<And>x. x \<in> \<Union> {enc (w, I) |w I. length I = n \<and> wf_interp w I \<and> (\<forall>i\<in>FO. case I ! i of Inl x \<Rightarrow> True | Inr x \<Rightarrow> False) \<and> (\<forall>i\<in>SO. case I ! i of Inl x \<Rightarrow> False | Inr x \<Rightarrow> True)} \<Longrightarrow> x \<in> lang n (ENC n FO)
[PROOF STEP]
have "sdrop (length x) (smap fst (x @- sconst (any, replicate n False))) = sconst any"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sdrop (length x) (smap fst (x @- sconst (any, replicate n False))) = sconst any
[PROOF STEP]
unfolding sdrop_smap
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. smap fst (sdrop (length x) (x @- sconst (any, replicate n False))) = sconst any
[PROOF STEP]
by (simp add: sdrop_shift)
[PROOF STATE]
proof (state)
this:
sdrop (length x) (smap fst (x @- sconst (any, replicate n False))) = sconst any

goal (2 subgoals):
 1. \<And>x. x \<in> lang n (ENC n FO) \<Longrightarrow> x \<in> \<Union> {enc (w, I) |w I. length I = n \<and> wf_interp w I \<and> (\<forall>i\<in>FO. case I ! i of Inl x \<Rightarrow> True | Inr x \<Rightarrow> False) \<and> (\<forall>i\<in>SO. case I ! i of Inl x \<Rightarrow> False | Inr x \<Rightarrow> True)}
 2. \<And>x. x \<in> \<Union> {enc (w, I) |w I. length I = n \<and> wf_interp w I \<and> (\<forall>i\<in>FO. case I ! i of Inl x \<Rightarrow> True | Inr x \<Rightarrow> False) \<and> (\<forall>i\<in>SO. case I ! i of Inl x \<Rightarrow> False | Inr x \<Rightarrow> True)} \<Longrightarrow> x \<in> lang n (ENC n FO)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
stream_all (\<lambda>x. length (snd x) = n) (x @- sconst (any, replicate n False))
?m4 \<in> FO \<Longrightarrow> \<exists>!p. snd ((x @- sconst (any, replicate n False)) !! p) ! ?m4
sdrop (length x) (smap fst (x @- sconst (any, replicate n False))) = sconst any
[PROOF STEP]
have enc_dec: "stream_enc (dec_word ?s, stream_dec n FO ?s) =
    x @- sconst (any, replicate n False)"
[PROOF STATE]
proof (prove)
using this:
stream_all (\<lambda>x. length (snd x) = n) (x @- sconst (any, replicate n False))
?m4 \<in> FO \<Longrightarrow> \<exists>!p. snd ((x @- sconst (any, replicate n False)) !! p) ! ?m4
sdrop (length x) (smap fst (x @- sconst (any, replicate n False))) = sconst any

goal (1 subgoal):
 1. stream_enc (dec_word (x @- sconst (any, replicate n False)), stream_dec n FO (x @- sconst (any, replicate n False))) = x @- sconst (any, replicate n False)
[PROOF STEP]
by (intro stream_enc_dec) auto
[PROOF STATE]
proof (state)
this:
stream_enc (dec_word (x @- sconst (any, replicate n False)), stream_dec n FO (x @- sconst (any, replicate n False))) = x @- sconst (any, replicate n False)

goal (2 subgoals):
 1. \<And>x. x \<in> lang n (ENC n FO) \<Longrightarrow> x \<in> \<Union> {enc (w, I) |w I. length I = n \<and> wf_interp w I \<and> (\<forall>i\<in>FO. case I ! i of Inl x \<Rightarrow> True | Inr x \<Rightarrow> False) \<and> (\<forall>i\<in>SO. case I ! i of Inl x \<Rightarrow> False | Inr x \<Rightarrow> True)}
 2. \<And>x. x \<in> \<Union> {enc (w, I) |w I. length I = n \<and> wf_interp w I \<and> (\<forall>i\<in>FO. case I ! i of Inl x \<Rightarrow> True | Inr x \<Rightarrow> False) \<and> (\<forall>i\<in>SO. case I ! i of Inl x \<Rightarrow> False | Inr x \<Rightarrow> True)} \<Longrightarrow> x \<in> lang n (ENC n FO)
[PROOF STEP]
define I where "I = stream_dec n FO ?s"
[PROOF STATE]
proof (state)
this:
I = stream_dec n FO (x @- sconst (any, replicate n False))

goal (2 subgoals):
 1. \<And>x. x \<in> lang n (ENC n FO) \<Longrightarrow> x \<in> \<Union> {enc (w, I) |w I. length I = n \<and> wf_interp w I \<and> (\<forall>i\<in>FO. case I ! i of Inl x \<Rightarrow> True | Inr x \<Rightarrow> False) \<and> (\<forall>i\<in>SO. case I ! i of Inl x \<Rightarrow> False | Inr x \<Rightarrow> True)}
 2. \<And>x. x \<in> \<Union> {enc (w, I) |w I. length I = n \<and> wf_interp w I \<and> (\<forall>i\<in>FO. case I ! i of Inl x \<Rightarrow> True | Inr x \<Rightarrow> False) \<and> (\<forall>i\<in>SO. case I ! i of Inl x \<Rightarrow> False | Inr x \<Rightarrow> True)} \<Longrightarrow> x \<in> lang n (ENC n FO)
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
FO \<subseteq> {0..<n}
SO \<subseteq> {0..<n} - FO
I = stream_dec n FO (x @- sconst (any, replicate n False))
[PROOF STEP]
have "wf_interp (dec_word ?s) I \<and>
   (\<forall>i \<in> FO. case I ! i of Inl _ \<Rightarrow> True | Inr _ \<Rightarrow> False) \<and>
   (\<forall>i \<in> SO. case I ! i of Inl _ \<Rightarrow> False | Inr _ \<Rightarrow> True)"
[PROOF STATE]
proof (prove)
using this:
FO \<subseteq> {0..<n}
SO \<subseteq> {0..<n} - FO
I = stream_dec n FO (x @- sconst (any, replicate n False))

goal (1 subgoal):
 1. wf_interp (dec_word (x @- sconst (any, replicate n False))) I \<and> (\<forall>i\<in>FO. case I ! i of Inl x \<Rightarrow> True | Inr x \<Rightarrow> False) \<and> (\<forall>i\<in>SO. case I ! i of Inl x \<Rightarrow> False | Inr x \<Rightarrow> True)
[PROOF STEP]
unfolding I_def dec_word_def
[PROOF STATE]
proof (prove)
using this:
FO \<subseteq> {0..<n}
SO \<subseteq> {0..<n} - FO
stream_dec n FO (x @- sconst (any, replicate n False)) = stream_dec n FO (x @- sconst (any, replicate n False))

goal (1 subgoal):
 1. wf_interp (cut_same any (smap fst (x @- sconst (any, replicate n False)))) (stream_dec n FO (x @- sconst (any, replicate n False))) \<and> (\<forall>i\<in>FO. case stream_dec n FO (x @- sconst (any, replicate n False)) ! i of Inl x \<Rightarrow> True | Inr x \<Rightarrow> False) \<and> (\<forall>i\<in>SO. case stream_dec n FO (x @- sconst (any, replicate n False)) ! i of Inl x \<Rightarrow> False | Inr x \<Rightarrow> True)
[PROOF STEP]
by (auto dest: stream_dec_not_Inr stream_dec_not_Inl simp: \<sigma>_def  max_idx_vars
      dest!: subsetD[OF set_cut_same[of any "map fst x"]] subsetD[OF *]  split: sum.splits)
      (auto simp: stream_dec_def positions_in_row finite_True_in_row)
[PROOF STATE]
proof (state)
this:
wf_interp (dec_word (x @- sconst (any, replicate n False))) I \<and> (\<forall>i\<in>FO. case I ! i of Inl x \<Rightarrow> True | Inr x \<Rightarrow> False) \<and> (\<forall>i\<in>SO. case I ! i of Inl x \<Rightarrow> False | Inr x \<Rightarrow> True)

goal (2 subgoals):
 1. \<And>x. x \<in> lang n (ENC n FO) \<Longrightarrow> x \<in> \<Union> {enc (w, I) |w I. length I = n \<and> wf_interp w I \<and> (\<forall>i\<in>FO. case I ! i of Inl x \<Rightarrow> True | Inr x \<Rightarrow> False) \<and> (\<forall>i\<in>SO. case I ! i of Inl x \<Rightarrow> False | Inr x \<Rightarrow> True)}
 2. \<And>x. x \<in> \<Union> {enc (w, I) |w I. length I = n \<and> wf_interp w I \<and> (\<forall>i\<in>FO. case I ! i of Inl x \<Rightarrow> True | Inr x \<Rightarrow> False) \<and> (\<forall>i\<in>SO. case I ! i of Inl x \<Rightarrow> False | Inr x \<Rightarrow> True)} \<Longrightarrow> x \<in> lang n (ENC n FO)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
wf_interp (dec_word (x @- sconst (any, replicate n False))) I \<and> (\<forall>i\<in>FO. case I ! i of Inl x \<Rightarrow> True | Inr x \<Rightarrow> False) \<and> (\<forall>i\<in>SO. case I ! i of Inl x \<Rightarrow> False | Inr x \<Rightarrow> True)

goal (2 subgoals):
 1. \<And>x. x \<in> lang n (ENC n FO) \<Longrightarrow> x \<in> \<Union> {enc (w, I) |w I. length I = n \<and> wf_interp w I \<and> (\<forall>i\<in>FO. case I ! i of Inl x \<Rightarrow> True | Inr x \<Rightarrow> False) \<and> (\<forall>i\<in>SO. case I ! i of Inl x \<Rightarrow> False | Inr x \<Rightarrow> True)}
 2. \<And>x. x \<in> \<Union> {enc (w, I) |w I. length I = n \<and> wf_interp w I \<and> (\<forall>i\<in>FO. case I ! i of Inl x \<Rightarrow> True | Inr x \<Rightarrow> False) \<and> (\<forall>i\<in>SO. case I ! i of Inl x \<Rightarrow> False | Inr x \<Rightarrow> True)} \<Longrightarrow> x \<in> lang n (ENC n FO)
[PROOF STEP]
have "length I = n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length I = n
[PROOF STEP]
unfolding I_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (stream_dec n FO (x @- sconst (any, replicate n False))) = n
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
length I = n

goal (2 subgoals):
 1. \<And>x. x \<in> lang n (ENC n FO) \<Longrightarrow> x \<in> \<Union> {enc (w, I) |w I. length I = n \<and> wf_interp w I \<and> (\<forall>i\<in>FO. case I ! i of Inl x \<Rightarrow> True | Inr x \<Rightarrow> False) \<and> (\<forall>i\<in>SO. case I ! i of Inl x \<Rightarrow> False | Inr x \<Rightarrow> True)}
 2. \<And>x. x \<in> \<Union> {enc (w, I) |w I. length I = n \<and> wf_interp w I \<and> (\<forall>i\<in>FO. case I ! i of Inl x \<Rightarrow> True | Inr x \<Rightarrow> False) \<and> (\<forall>i\<in>SO. case I ! i of Inl x \<Rightarrow> False | Inr x \<Rightarrow> True)} \<Longrightarrow> x \<in> lang n (ENC n FO)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
length I = n

goal (2 subgoals):
 1. \<And>x. x \<in> lang n (ENC n FO) \<Longrightarrow> x \<in> \<Union> {enc (w, I) |w I. length I = n \<and> wf_interp w I \<and> (\<forall>i\<in>FO. case I ! i of Inl x \<Rightarrow> True | Inr x \<Rightarrow> False) \<and> (\<forall>i\<in>SO. case I ! i of Inl x \<Rightarrow> False | Inr x \<Rightarrow> True)}
 2. \<And>x. x \<in> \<Union> {enc (w, I) |w I. length I = n \<and> wf_interp w I \<and> (\<forall>i\<in>FO. case I ! i of Inl x \<Rightarrow> True | Inr x \<Rightarrow> False) \<and> (\<forall>i\<in>SO. case I ! i of Inl x \<Rightarrow> False | Inr x \<Rightarrow> True)} \<Longrightarrow> x \<in> lang n (ENC n FO)
[PROOF STEP]
have "x \<in> enc (dec_word ?s, I)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> enc (dec_word (x @- sconst (any, replicate n False)), I)
[PROOF STEP]
unfolding I_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> enc (dec_word (x @- sconst (any, replicate n False)), stream_dec n FO (x @- sconst (any, replicate n False)))
[PROOF STEP]
by (simp add: enc_dec cut_same_shift_sconst del: stream_enc.simps)
[PROOF STATE]
proof (state)
this:
x \<in> enc (dec_word (x @- sconst (any, replicate n False)), I)

goal (2 subgoals):
 1. \<And>x. x \<in> lang n (ENC n FO) \<Longrightarrow> x \<in> \<Union> {enc (w, I) |w I. length I = n \<and> wf_interp w I \<and> (\<forall>i\<in>FO. case I ! i of Inl x \<Rightarrow> True | Inr x \<Rightarrow> False) \<and> (\<forall>i\<in>SO. case I ! i of Inl x \<Rightarrow> False | Inr x \<Rightarrow> True)}
 2. \<And>x. x \<in> \<Union> {enc (w, I) |w I. length I = n \<and> wf_interp w I \<and> (\<forall>i\<in>FO. case I ! i of Inl x \<Rightarrow> True | Inr x \<Rightarrow> False) \<and> (\<forall>i\<in>SO. case I ! i of Inl x \<Rightarrow> False | Inr x \<Rightarrow> True)} \<Longrightarrow> x \<in> lang n (ENC n FO)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
wf_interp (dec_word (x @- sconst (any, replicate n False))) I \<and> (\<forall>i\<in>FO. case I ! i of Inl x \<Rightarrow> True | Inr x \<Rightarrow> False) \<and> (\<forall>i\<in>SO. case I ! i of Inl x \<Rightarrow> False | Inr x \<Rightarrow> True)
length I = n
x \<in> enc (dec_word (x @- sconst (any, replicate n False)), I)
[PROOF STEP]
show "x \<in> ?R"
[PROOF STATE]
proof (prove)
using this:
wf_interp (dec_word (x @- sconst (any, replicate n False))) I \<and> (\<forall>i\<in>FO. case I ! i of Inl x \<Rightarrow> True | Inr x \<Rightarrow> False) \<and> (\<forall>i\<in>SO. case I ! i of Inl x \<Rightarrow> False | Inr x \<Rightarrow> True)
length I = n
x \<in> enc (dec_word (x @- sconst (any, replicate n False)), I)

goal (1 subgoal):
 1. x \<in> \<Union> {enc (w, I) |w I. length I = n \<and> wf_interp w I \<and> (\<forall>i\<in>FO. case I ! i of Inl x \<Rightarrow> True | Inr x \<Rightarrow> False) \<and> (\<forall>i\<in>SO. case I ! i of Inl x \<Rightarrow> False | Inr x \<Rightarrow> True)}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
x \<in> \<Union> {enc (w, I) |w I. length I = n \<and> wf_interp w I \<and> (\<forall>i\<in>FO. case I ! i of Inl x \<Rightarrow> True | Inr x \<Rightarrow> False) \<and> (\<forall>i\<in>SO. case I ! i of Inl x \<Rightarrow> False | Inr x \<Rightarrow> True)}

goal (1 subgoal):
 1. \<And>x. x \<in> \<Union> {enc (w, I) |w I. length I = n \<and> wf_interp w I \<and> (\<forall>i\<in>FO. case I ! i of Inl x \<Rightarrow> True | Inr x \<Rightarrow> False) \<and> (\<forall>i\<in>SO. case I ! i of Inl x \<Rightarrow> False | Inr x \<Rightarrow> True)} \<Longrightarrow> x \<in> lang n (ENC n FO)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> \<Union> {enc (w, I) |w I. length I = n \<and> wf_interp w I \<and> (\<forall>i\<in>FO. case I ! i of Inl x \<Rightarrow> True | Inr x \<Rightarrow> False) \<and> (\<forall>i\<in>SO. case I ! i of Inl x \<Rightarrow> False | Inr x \<Rightarrow> True)} \<Longrightarrow> x \<in> lang n (ENC n FO)
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> \<Union> {enc (w, I) |w I. length I = n \<and> wf_interp w I \<and> (\<forall>i\<in>FO. case I ! i of Inl x \<Rightarrow> True | Inr x \<Rightarrow> False) \<and> (\<forall>i\<in>SO. case I ! i of Inl x \<Rightarrow> False | Inr x \<Rightarrow> True)} \<Longrightarrow> x \<in> lang n (ENC n FO)
[PROOF STEP]
assume "x \<in> ?R"
[PROOF STATE]
proof (state)
this:
x \<in> \<Union> {enc (w, I) |w I. length I = n \<and> wf_interp w I \<and> (\<forall>i\<in>FO. case I ! i of Inl x \<Rightarrow> True | Inr x \<Rightarrow> False) \<and> (\<forall>i\<in>SO. case I ! i of Inl x \<Rightarrow> False | Inr x \<Rightarrow> True)}

goal (1 subgoal):
 1. \<And>x. x \<in> \<Union> {enc (w, I) |w I. length I = n \<and> wf_interp w I \<and> (\<forall>i\<in>FO. case I ! i of Inl x \<Rightarrow> True | Inr x \<Rightarrow> False) \<and> (\<forall>i\<in>SO. case I ! i of Inl x \<Rightarrow> False | Inr x \<Rightarrow> True)} \<Longrightarrow> x \<in> lang n (ENC n FO)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> \<Union> {enc (w, I) |w I. length I = n \<and> wf_interp w I \<and> (\<forall>i\<in>FO. case I ! i of Inl x \<Rightarrow> True | Inr x \<Rightarrow> False) \<and> (\<forall>i\<in>SO. case I ! i of Inl x \<Rightarrow> False | Inr x \<Rightarrow> True)}
[PROOF STEP]
obtain w I where I: "x \<in> enc (w, I)" "wf_interp w I \<and>
   (\<forall>i \<in> FO. case I ! i of Inl _ \<Rightarrow> True | Inr _ \<Rightarrow> False) \<and>
   (\<forall>i \<in> SO. case I ! i of Inl _ \<Rightarrow> False | Inr _ \<Rightarrow> True)" "length I = n"
[PROOF STATE]
proof (prove)
using this:
x \<in> \<Union> {enc (w, I) |w I. length I = n \<and> wf_interp w I \<and> (\<forall>i\<in>FO. case I ! i of Inl x \<Rightarrow> True | Inr x \<Rightarrow> False) \<and> (\<forall>i\<in>SO. case I ! i of Inl x \<Rightarrow> False | Inr x \<Rightarrow> True)}

goal (1 subgoal):
 1. (\<And>w I. \<lbrakk>x \<in> enc (w, I); wf_interp w I \<and> (\<forall>i\<in>FO. case I ! i of Inl x \<Rightarrow> True | Inr x \<Rightarrow> False) \<and> (\<forall>i\<in>SO. case I ! i of Inl x \<Rightarrow> False | Inr x \<Rightarrow> True); length I = n\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
x \<in> enc (w, I)
wf_interp w I \<and> (\<forall>i\<in>FO. case I ! i of Inl x \<Rightarrow> True | Inr x \<Rightarrow> False) \<and> (\<forall>i\<in>SO. case I ! i of Inl x \<Rightarrow> False | Inr x \<Rightarrow> True)
length I = n

goal (1 subgoal):
 1. \<And>x. x \<in> \<Union> {enc (w, I) |w I. length I = n \<and> wf_interp w I \<and> (\<forall>i\<in>FO. case I ! i of Inl x \<Rightarrow> True | Inr x \<Rightarrow> False) \<and> (\<forall>i\<in>SO. case I ! i of Inl x \<Rightarrow> False | Inr x \<Rightarrow> True)} \<Longrightarrow> x \<in> lang n (ENC n FO)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
x \<in> enc (w, I)
wf_interp w I \<and> (\<forall>i\<in>FO. case I ! i of Inl x \<Rightarrow> True | Inr x \<Rightarrow> False) \<and> (\<forall>i\<in>SO. case I ! i of Inl x \<Rightarrow> False | Inr x \<Rightarrow> True)
length I = n

goal (1 subgoal):
 1. \<And>x. x \<in> \<Union> {enc (w, I) |w I. length I = n \<and> wf_interp w I \<and> (\<forall>i\<in>FO. case I ! i of Inl x \<Rightarrow> True | Inr x \<Rightarrow> False) \<and> (\<forall>i\<in>SO. case I ! i of Inl x \<Rightarrow> False | Inr x \<Rightarrow> True)} \<Longrightarrow> x \<in> lang n (ENC n FO)
[PROOF STEP]
fix i
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> \<Union> {enc (w, I) |w I. length I = n \<and> wf_interp w I \<and> (\<forall>i\<in>FO. case I ! i of Inl x \<Rightarrow> True | Inr x \<Rightarrow> False) \<and> (\<forall>i\<in>SO. case I ! i of Inl x \<Rightarrow> False | Inr x \<Rightarrow> True)} \<Longrightarrow> x \<in> lang n (ENC n FO)
[PROOF STEP]
from I(2)
[PROOF STATE]
proof (chain)
picking this:
wf_interp w I \<and> (\<forall>i\<in>FO. case I ! i of Inl x \<Rightarrow> True | Inr x \<Rightarrow> False) \<and> (\<forall>i\<in>SO. case I ! i of Inl x \<Rightarrow> False | Inr x \<Rightarrow> True)
[PROOF STEP]
have "(w @- sconst any) !! i \<in> set \<Sigma>"
[PROOF STATE]
proof (prove)
using this:
wf_interp w I \<and> (\<forall>i\<in>FO. case I ! i of Inl x \<Rightarrow> True | Inr x \<Rightarrow> False) \<and> (\<forall>i\<in>SO. case I ! i of Inl x \<Rightarrow> False | Inr x \<Rightarrow> True)

goal (1 subgoal):
 1. (w @- sconst any) !! i \<in> set \<Sigma>
[PROOF STEP]
by (cases "i < length w") auto
[PROOF STATE]
proof (state)
this:
(w @- sconst any) !! i \<in> set \<Sigma>

goal (1 subgoal):
 1. \<And>x. x \<in> \<Union> {enc (w, I) |w I. length I = n \<and> wf_interp w I \<and> (\<forall>i\<in>FO. case I ! i of Inl x \<Rightarrow> True | Inr x \<Rightarrow> False) \<and> (\<forall>i\<in>SO. case I ! i of Inl x \<Rightarrow> False | Inr x \<Rightarrow> True)} \<Longrightarrow> x \<in> lang n (ENC n FO)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
(w @- sconst any) !! ?i4 \<in> set \<Sigma>

goal (1 subgoal):
 1. \<And>x. x \<in> \<Union> {enc (w, I) |w I. length I = n \<and> wf_interp w I \<and> (\<forall>i\<in>FO. case I ! i of Inl x \<Rightarrow> True | Inr x \<Rightarrow> False) \<and> (\<forall>i\<in>SO. case I ! i of Inl x \<Rightarrow> False | Inr x \<Rightarrow> True)} \<Longrightarrow> x \<in> lang n (ENC n FO)
[PROOF STEP]
note * = this
[PROOF STATE]
proof (state)
this:
(w @- sconst any) !! ?i4 \<in> set \<Sigma>

goal (1 subgoal):
 1. \<And>x. x \<in> \<Union> {enc (w, I) |w I. length I = n \<and> wf_interp w I \<and> (\<forall>i\<in>FO. case I ! i of Inl x \<Rightarrow> True | Inr x \<Rightarrow> False) \<and> (\<forall>i\<in>SO. case I ! i of Inl x \<Rightarrow> False | Inr x \<Rightarrow> True)} \<Longrightarrow> x \<in> lang n (ENC n FO)
[PROOF STEP]
from I
[PROOF STATE]
proof (chain)
picking this:
x \<in> enc (w, I)
wf_interp w I \<and> (\<forall>i\<in>FO. case I ! i of Inl x \<Rightarrow> True | Inr x \<Rightarrow> False) \<and> (\<forall>i\<in>SO. case I ! i of Inl x \<Rightarrow> False | Inr x \<Rightarrow> True)
length I = n
[PROOF STEP]
have "x @- sconst (any, replicate (length I) False) = stream_enc (w, I)" (is "x @- ?F = ?s")
[PROOF STATE]
proof (prove)
using this:
x \<in> enc (w, I)
wf_interp w I \<and> (\<forall>i\<in>FO. case I ! i of Inl x \<Rightarrow> True | Inr x \<Rightarrow> False) \<and> (\<forall>i\<in>SO. case I ! i of Inl x \<Rightarrow> False | Inr x \<Rightarrow> True)
length I = n

goal (1 subgoal):
 1. x @- sconst (any, replicate (length I) False) = stream_enc (w, I)
[PROOF STEP]
by (intro stream_enc_enc[symmetric]) auto
[PROOF STATE]
proof (state)
this:
x @- sconst (any, replicate (length I) False) = stream_enc (w, I)

goal (1 subgoal):
 1. \<And>x. x \<in> \<Union> {enc (w, I) |w I. length I = n \<and> wf_interp w I \<and> (\<forall>i\<in>FO. case I ! i of Inl x \<Rightarrow> True | Inr x \<Rightarrow> False) \<and> (\<forall>i\<in>SO. case I ! i of Inl x \<Rightarrow> False | Inr x \<Rightarrow> True)} \<Longrightarrow> x \<in> lang n (ENC n FO)
[PROOF STEP]
with * \<open>length I = n\<close>
[PROOF STATE]
proof (chain)
picking this:
(w @- sconst any) !! ?i4 \<in> set \<Sigma>
length I = n
x @- sconst (any, replicate (length I) False) = stream_enc (w, I)
[PROOF STEP]
have "\<forall>x \<in> set x. length (snd x) = n \<and> fst x \<in> set \<Sigma>"
[PROOF STATE]
proof (prove)
using this:
(w @- sconst any) !! ?i4 \<in> set \<Sigma>
length I = n
x @- sconst (any, replicate (length I) False) = stream_enc (w, I)

goal (1 subgoal):
 1. \<forall>x\<in>set x. length (snd x) = n \<and> fst x \<in> set \<Sigma>
[PROOF STEP]
by (auto dest!: shift_snth_less[of _ _ ?F, symmetric] simp: in_set_conv_nth)
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>set x. length (snd x) = n \<and> fst x \<in> set \<Sigma>

goal (1 subgoal):
 1. \<And>x. x \<in> \<Union> {enc (w, I) |w I. length I = n \<and> wf_interp w I \<and> (\<forall>i\<in>FO. case I ! i of Inl x \<Rightarrow> True | Inr x \<Rightarrow> False) \<and> (\<forall>i\<in>SO. case I ! i of Inl x \<Rightarrow> False | Inr x \<Rightarrow> True)} \<Longrightarrow> x \<in> lang n (ENC n FO)
[PROOF STEP]
thus "x \<in> ?L"
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>set x. length (snd x) = n \<and> fst x \<in> set \<Sigma>

goal (1 subgoal):
 1. x \<in> lang n (ENC n FO)
[PROOF STEP]
proof (cases "FO = {}")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>\<forall>x\<in>set x. length (snd x) = n \<and> fst x \<in> set \<Sigma>; FO = {}\<rbrakk> \<Longrightarrow> x \<in> lang n (ENC n FO)
 2. \<lbrakk>\<forall>x\<in>set x. length (snd x) = n \<and> fst x \<in> set \<Sigma>; FO \<noteq> {}\<rbrakk> \<Longrightarrow> x \<in> lang n (ENC n FO)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
FO \<noteq> {}

goal (2 subgoals):
 1. \<lbrakk>\<forall>x\<in>set x. length (snd x) = n \<and> fst x \<in> set \<Sigma>; FO = {}\<rbrakk> \<Longrightarrow> x \<in> lang n (ENC n FO)
 2. \<lbrakk>\<forall>x\<in>set x. length (snd x) = n \<and> fst x \<in> set \<Sigma>; FO \<noteq> {}\<rbrakk> \<Longrightarrow> x \<in> lang n (ENC n FO)
[PROOF STEP]
hence nonempty: "valid_ENC n ` FO \<noteq> {}"
[PROOF STATE]
proof (prove)
using this:
FO \<noteq> {}

goal (1 subgoal):
 1. valid_ENC n ` FO \<noteq> {}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
valid_ENC n ` FO \<noteq> {}

goal (2 subgoals):
 1. \<lbrakk>\<forall>x\<in>set x. length (snd x) = n \<and> fst x \<in> set \<Sigma>; FO = {}\<rbrakk> \<Longrightarrow> x \<in> lang n (ENC n FO)
 2. \<lbrakk>\<forall>x\<in>set x. length (snd x) = n \<and> fst x \<in> set \<Sigma>; FO \<noteq> {}\<rbrakk> \<Longrightarrow> x \<in> lang n (ENC n FO)
[PROOF STEP]
have finite: "finite (valid_ENC n ` FO)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (valid_ENC n ` FO)
[PROOF STEP]
by (rule finite_imageI[OF finite_subset[OF assms(1)]]) simp
[PROOF STATE]
proof (state)
this:
finite (valid_ENC n ` FO)

goal (2 subgoals):
 1. \<lbrakk>\<forall>x\<in>set x. length (snd x) = n \<and> fst x \<in> set \<Sigma>; FO = {}\<rbrakk> \<Longrightarrow> x \<in> lang n (ENC n FO)
 2. \<lbrakk>\<forall>x\<in>set x. length (snd x) = n \<and> fst x \<in> set \<Sigma>; FO \<noteq> {}\<rbrakk> \<Longrightarrow> x \<in> lang n (ENC n FO)
[PROOF STEP]
from False assms(1)
[PROOF STATE]
proof (chain)
picking this:
FO \<noteq> {}
FO \<subseteq> {0..<n}
[PROOF STEP]
have "0 < n"
[PROOF STATE]
proof (prove)
using this:
FO \<noteq> {}
FO \<subseteq> {0..<n}

goal (1 subgoal):
 1. 0 < n
[PROOF STEP]
by (cases n) (auto split: dest!: max_idx_vars)
[PROOF STATE]
proof (state)
this:
0 < n

goal (2 subgoals):
 1. \<lbrakk>\<forall>x\<in>set x. length (snd x) = n \<and> fst x \<in> set \<Sigma>; FO = {}\<rbrakk> \<Longrightarrow> x \<in> lang n (ENC n FO)
 2. \<lbrakk>\<forall>x\<in>set x. length (snd x) = n \<and> fst x \<in> set \<Sigma>; FO \<noteq> {}\<rbrakk> \<Longrightarrow> x \<in> lang n (ENC n FO)
[PROOF STEP]
with wf_rexp_valid_ENC assms
[PROOF STATE]
proof (chain)
picking this:
?n = 0 \<or> ?p < ?n \<Longrightarrow> local.wf ?n (valid_ENC ?n ?p)
FO \<subseteq> {0..<n}
SO \<subseteq> {0..<n} - FO
0 < n
[PROOF STEP]
have wf_rexp: "\<forall>x \<in> valid_ENC n ` FO. wf n x"
[PROOF STATE]
proof (prove)
using this:
?n = 0 \<or> ?p < ?n \<Longrightarrow> local.wf ?n (valid_ENC ?n ?p)
FO \<subseteq> {0..<n}
SO \<subseteq> {0..<n} - FO
0 < n

goal (1 subgoal):
 1. \<forall>x\<in>valid_ENC n ` FO. local.wf n x
[PROOF STEP]
by (auto simp: max_idx_vars)
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>valid_ENC n ` FO. local.wf n x

goal (2 subgoals):
 1. \<lbrakk>\<forall>x\<in>set x. length (snd x) = n \<and> fst x \<in> set \<Sigma>; FO = {}\<rbrakk> \<Longrightarrow> x \<in> lang n (ENC n FO)
 2. \<lbrakk>\<forall>x\<in>set x. length (snd x) = n \<and> fst x \<in> set \<Sigma>; FO \<noteq> {}\<rbrakk> \<Longrightarrow> x \<in> lang n (ENC n FO)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>valid_ENC n ` FO. local.wf n x

goal (2 subgoals):
 1. \<lbrakk>\<forall>x\<in>set x. length (snd x) = n \<and> fst x \<in> set \<Sigma>; FO = {}\<rbrakk> \<Longrightarrow> x \<in> lang n (ENC n FO)
 2. \<lbrakk>\<forall>x\<in>set x. length (snd x) = n \<and> fst x \<in> set \<Sigma>; FO \<noteq> {}\<rbrakk> \<Longrightarrow> x \<in> lang n (ENC n FO)
[PROOF STEP]
fix r
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>\<forall>x\<in>set x. length (snd x) = n \<and> fst x \<in> set \<Sigma>; FO = {}\<rbrakk> \<Longrightarrow> x \<in> lang n (ENC n FO)
 2. \<lbrakk>\<forall>x\<in>set x. length (snd x) = n \<and> fst x \<in> set \<Sigma>; FO \<noteq> {}\<rbrakk> \<Longrightarrow> x \<in> lang n (ENC n FO)
[PROOF STEP]
assume "r \<in> FO"
[PROOF STATE]
proof (state)
this:
r \<in> FO

goal (2 subgoals):
 1. \<lbrakk>\<forall>x\<in>set x. length (snd x) = n \<and> fst x \<in> set \<Sigma>; FO = {}\<rbrakk> \<Longrightarrow> x \<in> lang n (ENC n FO)
 2. \<lbrakk>\<forall>x\<in>set x. length (snd x) = n \<and> fst x \<in> set \<Sigma>; FO \<noteq> {}\<rbrakk> \<Longrightarrow> x \<in> lang n (ENC n FO)
[PROOF STEP]
with I(2)
[PROOF STATE]
proof (chain)
picking this:
wf_interp w I \<and> (\<forall>i\<in>FO. case I ! i of Inl x \<Rightarrow> True | Inr x \<Rightarrow> False) \<and> (\<forall>i\<in>SO. case I ! i of Inl x \<Rightarrow> False | Inr x \<Rightarrow> True)
r \<in> FO
[PROOF STEP]
obtain p where p: "I ! r = Inl p"
[PROOF STATE]
proof (prove)
using this:
wf_interp w I \<and> (\<forall>i\<in>FO. case I ! i of Inl x \<Rightarrow> True | Inr x \<Rightarrow> False) \<and> (\<forall>i\<in>SO. case I ! i of Inl x \<Rightarrow> False | Inr x \<Rightarrow> True)
r \<in> FO

goal (1 subgoal):
 1. (\<And>p. I ! r = Inl p \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases "I ! r") auto
[PROOF STATE]
proof (state)
this:
I ! r = Inl p

goal (2 subgoals):
 1. \<lbrakk>\<forall>x\<in>set x. length (snd x) = n \<and> fst x \<in> set \<Sigma>; FO = {}\<rbrakk> \<Longrightarrow> x \<in> lang n (ENC n FO)
 2. \<lbrakk>\<forall>x\<in>set x. length (snd x) = n \<and> fst x \<in> set \<Sigma>; FO \<noteq> {}\<rbrakk> \<Longrightarrow> x \<in> lang n (ENC n FO)
[PROOF STEP]
from \<open>r \<in> FO\<close> assms I(2,3)
[PROOF STATE]
proof (chain)
picking this:
r \<in> FO
FO \<subseteq> {0..<n}
SO \<subseteq> {0..<n} - FO
wf_interp w I \<and> (\<forall>i\<in>FO. case I ! i of Inl x \<Rightarrow> True | Inr x \<Rightarrow> False) \<and> (\<forall>i\<in>SO. case I ! i of Inl x \<Rightarrow> False | Inr x \<Rightarrow> True)
length I = n
[PROOF STEP]
have r: "r < length I"
[PROOF STATE]
proof (prove)
using this:
r \<in> FO
FO \<subseteq> {0..<n}
SO \<subseteq> {0..<n} - FO
wf_interp w I \<and> (\<forall>i\<in>FO. case I ! i of Inl x \<Rightarrow> True | Inr x \<Rightarrow> False) \<and> (\<forall>i\<in>SO. case I ! i of Inl x \<Rightarrow> False | Inr x \<Rightarrow> True)
length I = n

goal (1 subgoal):
 1. r < length I
[PROOF STEP]
by (auto dest!: max_idx_vars)
[PROOF STATE]
proof (state)
this:
r < length I

goal (2 subgoals):
 1. \<lbrakk>\<forall>x\<in>set x. length (snd x) = n \<and> fst x \<in> set \<Sigma>; FO = {}\<rbrakk> \<Longrightarrow> x \<in> lang n (ENC n FO)
 2. \<lbrakk>\<forall>x\<in>set x. length (snd x) = n \<and> fst x \<in> set \<Sigma>; FO \<noteq> {}\<rbrakk> \<Longrightarrow> x \<in> lang n (ENC n FO)
[PROOF STEP]
from p I(1,2) r
[PROOF STATE]
proof (chain)
picking this:
I ! r = Inl p
x \<in> enc (w, I)
wf_interp w I \<and> (\<forall>i\<in>FO. case I ! i of Inl x \<Rightarrow> True | Inr x \<Rightarrow> False) \<and> (\<forall>i\<in>SO. case I ! i of Inl x \<Rightarrow> False | Inr x \<Rightarrow> True)
r < length I
[PROOF STEP]
have "p < length x"
[PROOF STATE]
proof (prove)
using this:
I ! r = Inl p
x \<in> enc (w, I)
wf_interp w I \<and> (\<forall>i\<in>FO. case I ! i of Inl x \<Rightarrow> True | Inr x \<Rightarrow> False) \<and> (\<forall>i\<in>SO. case I ! i of Inl x \<Rightarrow> False | Inr x \<Rightarrow> True)
r < length I

goal (1 subgoal):
 1. p < length x
[PROOF STEP]
using less_length_cut_same_Inl[of I r p w]
[PROOF STATE]
proof (prove)
using this:
I ! r = Inl p
x \<in> enc (w, I)
wf_interp w I \<and> (\<forall>i\<in>FO. case I ! i of Inl x \<Rightarrow> True | Inr x \<Rightarrow> False) \<and> (\<forall>i\<in>SO. case I ! i of Inl x \<Rightarrow> False | Inr x \<Rightarrow> True)
r < length I
\<lbrakk>\<forall>x\<in>set I. case x of Inl a \<Rightarrow> True | Inr P \<Rightarrow> finite P; r < length I; I ! r = Inl p\<rbrakk> \<Longrightarrow> p < length (cut_same (any, replicate (length I) False) (stream_enc (w, I)))

goal (1 subgoal):
 1. p < length x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
p < length x

goal (2 subgoals):
 1. \<lbrakk>\<forall>x\<in>set x. length (snd x) = n \<and> fst x \<in> set \<Sigma>; FO = {}\<rbrakk> \<Longrightarrow> x \<in> lang n (ENC n FO)
 2. \<lbrakk>\<forall>x\<in>set x. length (snd x) = n \<and> fst x \<in> set \<Sigma>; FO \<noteq> {}\<rbrakk> \<Longrightarrow> x \<in> lang n (ENC n FO)
[PROOF STEP]
with p I r *
[PROOF STATE]
proof (chain)
picking this:
I ! r = Inl p
x \<in> enc (w, I)
wf_interp w I \<and> (\<forall>i\<in>FO. case I ! i of Inl x \<Rightarrow> True | Inr x \<Rightarrow> False) \<and> (\<forall>i\<in>SO. case I ! i of Inl x \<Rightarrow> False | Inr x \<Rightarrow> True)
length I = n
r < length I
(w @- sconst any) !! ?i4 \<in> set \<Sigma>
p < length x
[PROOF STEP]
have "[x ! p] \<in> lang n (Atom (Arbitrary_Except r True))"
[PROOF STATE]
proof (prove)
using this:
I ! r = Inl p
x \<in> enc (w, I)
wf_interp w I \<and> (\<forall>i\<in>FO. case I ! i of Inl x \<Rightarrow> True | Inr x \<Rightarrow> False) \<and> (\<forall>i\<in>SO. case I ! i of Inl x \<Rightarrow> False | Inr x \<Rightarrow> True)
length I = n
r < length I
(w @- sconst any) !! ?i4 \<in> set \<Sigma>
p < length x

goal (1 subgoal):
 1. [x ! p] \<in> lang n (Atom (Arbitrary_Except r True))
[PROOF STEP]
by (subst encD[of x w I]) (auto simp del: lang.simps intro!: enc_atom_lang_Arbitrary_Except_True)
[PROOF STATE]
proof (state)
this:
[x ! p] \<in> lang n (Atom (Arbitrary_Except r True))

goal (2 subgoals):
 1. \<lbrakk>\<forall>x\<in>set x. length (snd x) = n \<and> fst x \<in> set \<Sigma>; FO = {}\<rbrakk> \<Longrightarrow> x \<in> lang n (ENC n FO)
 2. \<lbrakk>\<forall>x\<in>set x. length (snd x) = n \<and> fst x \<in> set \<Sigma>; FO \<noteq> {}\<rbrakk> \<Longrightarrow> x \<in> lang n (ENC n FO)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
[x ! p] \<in> lang n (Atom (Arbitrary_Except r True))

goal (2 subgoals):
 1. \<lbrakk>\<forall>x\<in>set x. length (snd x) = n \<and> fst x \<in> set \<Sigma>; FO = {}\<rbrakk> \<Longrightarrow> x \<in> lang n (ENC n FO)
 2. \<lbrakk>\<forall>x\<in>set x. length (snd x) = n \<and> fst x \<in> set \<Sigma>; FO \<noteq> {}\<rbrakk> \<Longrightarrow> x \<in> lang n (ENC n FO)
[PROOF STEP]
from p I r *
[PROOF STATE]
proof (chain)
picking this:
I ! r = Inl p
x \<in> enc (w, I)
wf_interp w I \<and> (\<forall>i\<in>FO. case I ! i of Inl x \<Rightarrow> True | Inr x \<Rightarrow> False) \<and> (\<forall>i\<in>SO. case I ! i of Inl x \<Rightarrow> False | Inr x \<Rightarrow> True)
length I = n
r < length I
(w @- sconst any) !! ?i4 \<in> set \<Sigma>
[PROOF STEP]
have "take p x \<in> star (lang n (Atom (Arbitrary_Except r False)))"
[PROOF STATE]
proof (prove)
using this:
I ! r = Inl p
x \<in> enc (w, I)
wf_interp w I \<and> (\<forall>i\<in>FO. case I ! i of Inl x \<Rightarrow> True | Inr x \<Rightarrow> False) \<and> (\<forall>i\<in>SO. case I ! i of Inl x \<Rightarrow> False | Inr x \<Rightarrow> True)
length I = n
r < length I
(w @- sconst any) !! ?i4 \<in> set \<Sigma>

goal (1 subgoal):
 1. take p x \<in> star (lang n (Atom (Arbitrary_Except r False)))
[PROOF STEP]
by (subst encD[of x]) (auto  simp del: lang.simps simp: in_set_conv_nth intro!: Ball_starI enc_atom_lang_Arbitrary_Except_False)
[PROOF STATE]
proof (state)
this:
take p x \<in> star (lang n (Atom (Arbitrary_Except r False)))

goal (2 subgoals):
 1. \<lbrakk>\<forall>x\<in>set x. length (snd x) = n \<and> fst x \<in> set \<Sigma>; FO = {}\<rbrakk> \<Longrightarrow> x \<in> lang n (ENC n FO)
 2. \<lbrakk>\<forall>x\<in>set x. length (snd x) = n \<and> fst x \<in> set \<Sigma>; FO \<noteq> {}\<rbrakk> \<Longrightarrow> x \<in> lang n (ENC n FO)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
take p x \<in> star (lang n (Atom (Arbitrary_Except r False)))

goal (2 subgoals):
 1. \<lbrakk>\<forall>x\<in>set x. length (snd x) = n \<and> fst x \<in> set \<Sigma>; FO = {}\<rbrakk> \<Longrightarrow> x \<in> lang n (ENC n FO)
 2. \<lbrakk>\<forall>x\<in>set x. length (snd x) = n \<and> fst x \<in> set \<Sigma>; FO \<noteq> {}\<rbrakk> \<Longrightarrow> x \<in> lang n (ENC n FO)
[PROOF STEP]
from p I r *
[PROOF STATE]
proof (chain)
picking this:
I ! r = Inl p
x \<in> enc (w, I)
wf_interp w I \<and> (\<forall>i\<in>FO. case I ! i of Inl x \<Rightarrow> True | Inr x \<Rightarrow> False) \<and> (\<forall>i\<in>SO. case I ! i of Inl x \<Rightarrow> False | Inr x \<Rightarrow> True)
length I = n
r < length I
(w @- sconst any) !! ?i4 \<in> set \<Sigma>
[PROOF STEP]
have "drop (Suc p) x \<in> star (lang n (Atom (Arbitrary_Except r False)))"
[PROOF STATE]
proof (prove)
using this:
I ! r = Inl p
x \<in> enc (w, I)
wf_interp w I \<and> (\<forall>i\<in>FO. case I ! i of Inl x \<Rightarrow> True | Inr x \<Rightarrow> False) \<and> (\<forall>i\<in>SO. case I ! i of Inl x \<Rightarrow> False | Inr x \<Rightarrow> True)
length I = n
r < length I
(w @- sconst any) !! ?i4 \<in> set \<Sigma>

goal (1 subgoal):
 1. drop (Suc p) x \<in> star (lang n (Atom (Arbitrary_Except r False)))
[PROOF STEP]
by (subst encD[of x]) (auto simp: in_set_conv_nth simp del: lang.simps snth.simps intro!: Ball_starI enc_atom_lang_Arbitrary_Except_False)
[PROOF STATE]
proof (state)
this:
drop (Suc p) x \<in> star (lang n (Atom (Arbitrary_Except r False)))

goal (2 subgoals):
 1. \<lbrakk>\<forall>x\<in>set x. length (snd x) = n \<and> fst x \<in> set \<Sigma>; FO = {}\<rbrakk> \<Longrightarrow> x \<in> lang n (ENC n FO)
 2. \<lbrakk>\<forall>x\<in>set x. length (snd x) = n \<and> fst x \<in> set \<Sigma>; FO \<noteq> {}\<rbrakk> \<Longrightarrow> x \<in> lang n (ENC n FO)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
[x ! p] \<in> lang n (Atom (Arbitrary_Except r True))
take p x \<in> star (lang n (Atom (Arbitrary_Except r False)))
drop (Suc p) x \<in> star (lang n (Atom (Arbitrary_Except r False)))
[PROOF STEP]
have "take p x @ [x ! p] @ drop (p + 1) x \<in> lang n (valid_ENC n r)"
[PROOF STATE]
proof (prove)
using this:
[x ! p] \<in> lang n (Atom (Arbitrary_Except r True))
take p x \<in> star (lang n (Atom (Arbitrary_Except r False)))
drop (Suc p) x \<in> star (lang n (Atom (Arbitrary_Except r False)))

goal (1 subgoal):
 1. take p x @ [x ! p] @ drop (p + 1) x \<in> lang n (valid_ENC n r)
[PROOF STEP]
using \<open>0 < n\<close>
[PROOF STATE]
proof (prove)
using this:
[x ! p] \<in> lang n (Atom (Arbitrary_Except r True))
take p x \<in> star (lang n (Atom (Arbitrary_Except r False)))
drop (Suc p) x \<in> star (lang n (Atom (Arbitrary_Except r False)))
0 < n

goal (1 subgoal):
 1. take p x @ [x ! p] @ drop (p + 1) x \<in> lang n (valid_ENC n r)
[PROOF STEP]
unfolding valid_ENC_def
[PROOF STATE]
proof (prove)
using this:
[x ! p] \<in> lang n (Atom (Arbitrary_Except r True))
take p x \<in> star (lang n (Atom (Arbitrary_Except r False)))
drop (Suc p) x \<in> star (lang n (Atom (Arbitrary_Except r False)))
0 < n

goal (1 subgoal):
 1. take p x @ [x ! p] @ drop (p + 1) x \<in> lang n (if n = 0 then Full else TIMES [Star (Atom (Arbitrary_Except r False)), Atom (Arbitrary_Except r True), Star (Atom (Arbitrary_Except r False))])
[PROOF STEP]
by (auto simp del: append.simps)
[PROOF STATE]
proof (state)
this:
take p x @ [x ! p] @ drop (p + 1) x \<in> lang n (valid_ENC n r)

goal (2 subgoals):
 1. \<lbrakk>\<forall>x\<in>set x. length (snd x) = n \<and> fst x \<in> set \<Sigma>; FO = {}\<rbrakk> \<Longrightarrow> x \<in> lang n (ENC n FO)
 2. \<lbrakk>\<forall>x\<in>set x. length (snd x) = n \<and> fst x \<in> set \<Sigma>; FO \<noteq> {}\<rbrakk> \<Longrightarrow> x \<in> lang n (ENC n FO)
[PROOF STEP]
hence "x \<in> lang n (valid_ENC n r)"
[PROOF STATE]
proof (prove)
using this:
take p x @ [x ! p] @ drop (p + 1) x \<in> lang n (valid_ENC n r)

goal (1 subgoal):
 1. x \<in> lang n (valid_ENC n r)
[PROOF STEP]
using id_take_nth_drop[OF \<open>p < length x\<close>]
[PROOF STATE]
proof (prove)
using this:
take p x @ [x ! p] @ drop (p + 1) x \<in> lang n (valid_ENC n r)
x = take p x @ x ! p # drop (Suc p) x

goal (1 subgoal):
 1. x \<in> lang n (valid_ENC n r)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<in> lang n (valid_ENC n r)

goal (2 subgoals):
 1. \<lbrakk>\<forall>x\<in>set x. length (snd x) = n \<and> fst x \<in> set \<Sigma>; FO = {}\<rbrakk> \<Longrightarrow> x \<in> lang n (ENC n FO)
 2. \<lbrakk>\<forall>x\<in>set x. length (snd x) = n \<and> fst x \<in> set \<Sigma>; FO \<noteq> {}\<rbrakk> \<Longrightarrow> x \<in> lang n (ENC n FO)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?r4 \<in> FO \<Longrightarrow> x \<in> lang n (valid_ENC n ?r4)

goal (2 subgoals):
 1. \<lbrakk>\<forall>x\<in>set x. length (snd x) = n \<and> fst x \<in> set \<Sigma>; FO = {}\<rbrakk> \<Longrightarrow> x \<in> lang n (ENC n FO)
 2. \<lbrakk>\<forall>x\<in>set x. length (snd x) = n \<and> fst x \<in> set \<Sigma>; FO \<noteq> {}\<rbrakk> \<Longrightarrow> x \<in> lang n (ENC n FO)
[PROOF STEP]
with False lang_flatten_INTERSECT[OF finite nonempty wf_rexp]
[PROOF STATE]
proof (chain)
picking this:
FO \<noteq> {}
(?w \<in> lang n (INTERSECT (sorted_list_of_set (valid_ENC n ` FO)))) = (\<forall>r\<in>valid_ENC n ` FO. ?w \<in> lang n r)
?r4 \<in> FO \<Longrightarrow> x \<in> lang n (valid_ENC n ?r4)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
FO \<noteq> {}
(?w \<in> lang n (INTERSECT (sorted_list_of_set (valid_ENC n ` FO)))) = (\<forall>r\<in>valid_ENC n ` FO. ?w \<in> lang n r)
?r4 \<in> FO \<Longrightarrow> x \<in> lang n (valid_ENC n ?r4)

goal (1 subgoal):
 1. x \<in> lang n (ENC n FO)
[PROOF STEP]
by (auto simp: ENC_def)
[PROOF STATE]
proof (state)
this:
x \<in> lang n (ENC n FO)

goal (1 subgoal):
 1. \<lbrakk>\<forall>x\<in>set x. length (snd x) = n \<and> fst x \<in> set \<Sigma>; FO = {}\<rbrakk> \<Longrightarrow> x \<in> lang n (ENC n FO)
[PROOF STEP]
qed (simp add: ENC_def, auto simp: \<sigma>_def set_n_lists image_iff)
[PROOF STATE]
proof (state)
this:
x \<in> lang n (ENC n FO)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma lang_ENC_formula:
  assumes "wf_formula n \<phi>"
  shows "lang n (ENC n (FOV \<phi>)) = \<Union>{enc (w, I) | w I . length I = n \<and> wf_interp_for_formula (w, I) \<phi>}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lang n (ENC n (FOV \<phi>)) = \<Union> {enc (w, I) |w I. length I = n \<and> wf_interp_for_formula (w, I) \<phi>}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. lang n (ENC n (FOV \<phi>)) = \<Union> {enc (w, I) |w I. length I = n \<and> wf_interp_for_formula (w, I) \<phi>}
[PROOF STEP]
from assms max_idx_vars
[PROOF STATE]
proof (chain)
picking this:
wf_formula n \<phi>
pre_wf_formula ?n ?\<phi> \<Longrightarrow> \<forall>p\<in>FOV ?\<phi> \<union> SOV ?\<phi>. p < ?n
[PROOF STEP]
have *: "FOV \<phi> \<subseteq> {0 ..< n}" "SOV \<phi> \<subseteq> {0 ..< n} - FOV \<phi>"
[PROOF STATE]
proof (prove)
using this:
wf_formula n \<phi>
pre_wf_formula ?n ?\<phi> \<Longrightarrow> \<forall>p\<in>FOV ?\<phi> \<union> SOV ?\<phi>. p < ?n

goal (1 subgoal):
 1. FOV \<phi> \<subseteq> {0..<n} &&& SOV \<phi> \<subseteq> {0..<n} - FOV \<phi>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
FOV \<phi> \<subseteq> {0..<n}
SOV \<phi> \<subseteq> {0..<n} - FOV \<phi>

goal (1 subgoal):
 1. lang n (ENC n (FOV \<phi>)) = \<Union> {enc (w, I) |w I. length I = n \<and> wf_interp_for_formula (w, I) \<phi>}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lang n (ENC n (FOV \<phi>)) = \<Union> {enc (w, I) |w I. length I = n \<and> wf_interp_for_formula (w, I) \<phi>}
[PROOF STEP]
unfolding lang_ENC[OF *]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Union> {enc (w, I) |w I. length I = n \<and> wf_interp w I \<and> (\<forall>i\<in>FOV \<phi>. case I ! i of Inl x \<Rightarrow> True | Inr x \<Rightarrow> False) \<and> (\<forall>i\<in>SOV \<phi>. case I ! i of Inl x \<Rightarrow> False | Inr x \<Rightarrow> True)} = \<Union> {enc (w, I) |w I. length I = n \<and> wf_interp_for_formula (w, I) \<phi>}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
lang n (ENC n (FOV \<phi>)) = \<Union> {enc (w, I) |w I. length I = n \<and> wf_interp_for_formula (w, I) \<phi>}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma wf_interp_for_formula_FExists:
 "\<lbrakk>wf_formula (length I) (FExists \<phi>)\<rbrakk>\<Longrightarrow>
  wf_interp_for_formula (w, I) (FExists \<phi>) \<longleftrightarrow> (\<forall>p. wf_interp_for_formula (w, Inl p # I) \<phi>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf_formula (length I) (FExists \<phi>) \<Longrightarrow> wf_interp_for_formula (w, I) (FExists \<phi>) = (\<forall>p. wf_interp_for_formula (w, Inl p # I) \<phi>)
[PROOF STEP]
by (auto simp: nth_Cons' split: if_split_asm)


[STATEMENT]
lemma wf_interp_for_formula_any_Inl: "wf_interp_for_formula (w, Inl p # I) \<phi> \<Longrightarrow>
  \<forall>p. wf_interp_for_formula (w, Inl p # I) \<phi>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf_interp_for_formula (w, Inl p # I) \<phi> \<Longrightarrow> \<forall>p. wf_interp_for_formula (w, Inl p # I) \<phi>
[PROOF STEP]
by (auto simp: nth_Cons' split: if_split_asm)


[STATEMENT]
lemma wf_interp_for_formula_FEXISTS:
 "\<lbrakk>wf_formula (length I) (FEXISTS \<phi>)\<rbrakk>\<Longrightarrow>
  wf_interp_for_formula (w, I) (FEXISTS \<phi>) \<longleftrightarrow> (\<forall>P. finite P \<longrightarrow> wf_interp_for_formula (w, Inr P # I) \<phi>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf_formula (length I) (FEXISTS \<phi>) \<Longrightarrow> wf_interp_for_formula (w, I) (FEXISTS \<phi>) = (\<forall>P. finite P \<longrightarrow> wf_interp_for_formula (w, Inr P # I) \<phi>)
[PROOF STEP]
by (auto simp: nth_Cons' split: if_split_asm)


[STATEMENT]
lemma wf_interp_for_formula_any_Inr: "wf_interp_for_formula (w, Inr P # I) \<phi> \<Longrightarrow>
  \<forall>P. finite P \<longrightarrow> wf_interp_for_formula (w, Inr P # I) \<phi>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf_interp_for_formula (w, Inr P # I) \<phi> \<Longrightarrow> \<forall>P. finite P \<longrightarrow> wf_interp_for_formula (w, Inr P # I) \<phi>
[PROOF STEP]
by (auto simp: nth_Cons' split: if_split_asm)


[STATEMENT]
lemma wf_interp_for_formula_FOr:
  "wf_interp_for_formula (w, I) (FOr \<phi>1 \<phi>2) =
     (wf_interp_for_formula (w, I) \<phi>1 \<and> wf_interp_for_formula (w, I) \<phi>2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf_interp_for_formula (w, I) (FOr \<phi>1 \<phi>2) = (wf_interp_for_formula (w, I) \<phi>1 \<and> wf_interp_for_formula (w, I) \<phi>2)
[PROOF STEP]
by auto


[STATEMENT]
lemma wf_interp_for_formula_FAnd:
  "wf_interp_for_formula (w, I) (FAnd \<phi>1 \<phi>2) =
     (wf_interp_for_formula (w, I) \<phi>1 \<and> wf_interp_for_formula (w, I) \<phi>2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf_interp_for_formula (w, I) (FAnd \<phi>1 \<phi>2) = (wf_interp_for_formula (w, I) \<phi>1 \<and> wf_interp_for_formula (w, I) \<phi>2)
[PROOF STEP]
by auto