[STATEMENT]
lemma map_project_Int_ENC:
  fixes X Z n
  defines "z \<equiv> (any, replicate n False)"
  assumes "0 \<notin> X" "X \<subseteq> {0 ..< n + 1}" "Z \<subseteq> lists ((set o \<sigma> \<Sigma>) (n + 1))"
  shows "SAMEQUOT z (map \<pi> ` (Z \<inter> lang (n + 1) (ENC (n + 1) X))) =
    SAMEQUOT z (map \<pi> ` Z) \<inter> lang n (ENC n ((\<lambda>x. x - 1) ` X))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. SAMEQUOT z (map \<pi> ` (Z \<inter> lang (n + 1) (ENC (n + 1) X))) = SAMEQUOT z (map \<pi> ` Z) \<inter> lang n (ENC n ((\<lambda>x. x - 1) ` X))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. SAMEQUOT z (map \<pi> ` (Z \<inter> lang (n + 1) (ENC (n + 1) X))) = SAMEQUOT z (map \<pi> ` Z) \<inter> lang n (ENC n ((\<lambda>x. x - 1) ` X))
[PROOF STEP]
let ?Y = "{0 ..< n + 1} - X"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. SAMEQUOT z (map \<pi> ` (Z \<inter> lang (n + 1) (ENC (n + 1) X))) = SAMEQUOT z (map \<pi> ` Z) \<inter> lang n (ENC n ((\<lambda>x. x - 1) ` X))
[PROOF STEP]
let ?fX = "(\<lambda>x. x - 1) ` X"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. SAMEQUOT z (map \<pi> ` (Z \<inter> lang (n + 1) (ENC (n + 1) X))) = SAMEQUOT z (map \<pi> ` Z) \<inter> lang n (ENC n ((\<lambda>x. x - 1) ` X))
[PROOF STEP]
let ?fY = "{0 ..< n} - (\<lambda>x. x - 1) ` X"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. SAMEQUOT z (map \<pi> ` (Z \<inter> lang (n + 1) (ENC (n + 1) X))) = SAMEQUOT z (map \<pi> ` Z) \<inter> lang n (ENC n ((\<lambda>x. x - 1) ` X))
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
z \<equiv> (any, replicate n False)
0 \<notin> X
X \<subseteq> {0..<n + 1}
Z \<subseteq> lists ((set \<circ> \<sigma> \<Sigma>) (n + 1))
[PROOF STEP]
have *: "(\<lambda>x. x - 1) ` X \<subseteq> {0 ..< n}"
[PROOF STATE]
proof (prove)
using this:
z \<equiv> (any, replicate n False)
0 \<notin> X
X \<subseteq> {0..<n + 1}
Z \<subseteq> lists ((set \<circ> \<sigma> \<Sigma>) (n + 1))

goal (1 subgoal):
 1. (\<lambda>x. x - 1) ` X \<subseteq> {0..<n}
[PROOF STEP]
by (cases n) auto
[PROOF STATE]
proof (state)
this:
(\<lambda>x. x - 1) ` X \<subseteq> {0..<n}

goal (1 subgoal):
 1. SAMEQUOT z (map \<pi> ` (Z \<inter> lang (n + 1) (ENC (n + 1) X))) = SAMEQUOT z (map \<pi> ` Z) \<inter> lang n (ENC n ((\<lambda>x. x - 1) ` X))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. SAMEQUOT z (map \<pi> ` (Z \<inter> lang (n + 1) (ENC (n + 1) X))) = SAMEQUOT z (map \<pi> ` Z) \<inter> lang n (ENC n ((\<lambda>x. x - 1) ` X))
[PROOF STEP]
proof (safe elim!: subsetD[OF SAMEQUOT_mono[OF subset_trans[OF image_Int_subset Int_lower1]]])
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. x \<in> SAMEQUOT z (map \<pi> ` (Z \<inter> lang (n + 1) (ENC (n + 1) X))) \<Longrightarrow> x \<in> lang n (ENC n ((\<lambda>x. x - 1) ` X))
 2. \<And>x. \<lbrakk>x \<in> SAMEQUOT z (map \<pi> ` Z); x \<in> lang n (ENC n ((\<lambda>x. x - 1) ` X))\<rbrakk> \<Longrightarrow> x \<in> SAMEQUOT z (map \<pi> ` (Z \<inter> lang (n + 1) (ENC (n + 1) X)))
[PROOF STEP]
fix w
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. x \<in> SAMEQUOT z (map \<pi> ` (Z \<inter> lang (n + 1) (ENC (n + 1) X))) \<Longrightarrow> x \<in> lang n (ENC n ((\<lambda>x. x - 1) ` X))
 2. \<And>x. \<lbrakk>x \<in> SAMEQUOT z (map \<pi> ` Z); x \<in> lang n (ENC n ((\<lambda>x. x - 1) ` X))\<rbrakk> \<Longrightarrow> x \<in> SAMEQUOT z (map \<pi> ` (Z \<inter> lang (n + 1) (ENC (n + 1) X)))
[PROOF STEP]
assume "w \<in> SAMEQUOT z (map \<pi> ` (Z \<inter> lang (n + 1) (ENC (n + 1) X)))"
[PROOF STATE]
proof (state)
this:
w \<in> SAMEQUOT z (map \<pi> ` (Z \<inter> lang (n + 1) (ENC (n + 1) X)))

goal (2 subgoals):
 1. \<And>x. x \<in> SAMEQUOT z (map \<pi> ` (Z \<inter> lang (n + 1) (ENC (n + 1) X))) \<Longrightarrow> x \<in> lang n (ENC n ((\<lambda>x. x - 1) ` X))
 2. \<And>x. \<lbrakk>x \<in> SAMEQUOT z (map \<pi> ` Z); x \<in> lang n (ENC n ((\<lambda>x. x - 1) ` X))\<rbrakk> \<Longrightarrow> x \<in> SAMEQUOT z (map \<pi> ` (Z \<inter> lang (n + 1) (ENC (n + 1) X)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
w \<in> SAMEQUOT z (map \<pi> ` (Z \<inter> lang (n + 1) (ENC (n + 1) X)))
[PROOF STEP]
have "w \<in> SAMEQUOT z (map \<pi> ` lang (n + 1) (ENC (n + 1) X))"
[PROOF STATE]
proof (prove)
using this:
w \<in> SAMEQUOT z (map \<pi> ` (Z \<inter> lang (n + 1) (ENC (n + 1) X)))

goal (1 subgoal):
 1. w \<in> SAMEQUOT z (map \<pi> ` lang (n + 1) (ENC (n + 1) X))
[PROOF STEP]
by (rule rev_subsetD[OF _ SAMEQUOT_mono]) auto
[PROOF STATE]
proof (state)
this:
w \<in> SAMEQUOT z (map \<pi> ` lang (n + 1) (ENC (n + 1) X))

goal (2 subgoals):
 1. \<And>x. x \<in> SAMEQUOT z (map \<pi> ` (Z \<inter> lang (n + 1) (ENC (n + 1) X))) \<Longrightarrow> x \<in> lang n (ENC n ((\<lambda>x. x - 1) ` X))
 2. \<And>x. \<lbrakk>x \<in> SAMEQUOT z (map \<pi> ` Z); x \<in> lang n (ENC n ((\<lambda>x. x - 1) ` X))\<rbrakk> \<Longrightarrow> x \<in> SAMEQUOT z (map \<pi> ` (Z \<inter> lang (n + 1) (ENC (n + 1) X)))
[PROOF STEP]
with assms(2)
[PROOF STATE]
proof (chain)
picking this:
0 \<notin> X
w \<in> SAMEQUOT z (map \<pi> ` lang (n + 1) (ENC (n + 1) X))
[PROOF STEP]
show "w \<in> lang n (ENC n ((\<lambda>x. x - 1) ` X))"
[PROOF STATE]
proof (prove)
using this:
0 \<notin> X
w \<in> SAMEQUOT z (map \<pi> ` lang (n + 1) (ENC (n + 1) X))

goal (1 subgoal):
 1. w \<in> lang n (ENC n ((\<lambda>x. x - 1) ` X))
[PROOF STEP]
unfolding lang_ENC[OF assms(3) subset_refl] lang_ENC[OF * subset_refl]
[PROOF STATE]
proof (prove)
using this:
0 \<notin> X
w \<in> SAMEQUOT z (map \<pi> ` \<Union> {enc (w, I) |w I. length I = n + 1 \<and> wf_interp w I \<and> (\<forall>i\<in>X. case I ! i of Inl x \<Rightarrow> True | Inr x \<Rightarrow> False) \<and> (\<forall>i\<in>{0..<n + 1} - X. case I ! i of Inl x \<Rightarrow> False | Inr x \<Rightarrow> True)})

goal (1 subgoal):
 1. w \<in> \<Union> {enc (w, I) |w I. length I = n \<and> wf_interp w I \<and> (\<forall>i\<in>(\<lambda>x. x - 1) ` X. case I ! i of Inl x \<Rightarrow> True | Inr x \<Rightarrow> False) \<and> (\<forall>i\<in>{0..<n} - (\<lambda>x. x - 1) ` X. case I ! i of Inl x \<Rightarrow> False | Inr x \<Rightarrow> True)}
[PROOF STEP]
by (auto simp: image_Union z_def length_Suc_conv simp del: enc.simps
        intro!: exI[of _ "enc (w, I)" for w I, OF conjI[of _ "x \<in> A" for x A]])
        (fastforce simp: nth_Cons image_iff split: nat.splits sum.splits)
[PROOF STATE]
proof (state)
this:
w \<in> lang n (ENC n ((\<lambda>x. x - 1) ` X))

goal (1 subgoal):
 1. \<And>x. \<lbrakk>x \<in> SAMEQUOT z (map \<pi> ` Z); x \<in> lang n (ENC n ((\<lambda>x. x - 1) ` X))\<rbrakk> \<Longrightarrow> x \<in> SAMEQUOT z (map \<pi> ` (Z \<inter> lang (n + 1) (ENC (n + 1) X)))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>x \<in> SAMEQUOT z (map \<pi> ` Z); x \<in> lang n (ENC n ((\<lambda>x. x - 1) ` X))\<rbrakk> \<Longrightarrow> x \<in> SAMEQUOT z (map \<pi> ` (Z \<inter> lang (n + 1) (ENC (n + 1) X)))
[PROOF STEP]
fix w
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>x \<in> SAMEQUOT z (map \<pi> ` Z); x \<in> lang n (ENC n ((\<lambda>x. x - 1) ` X))\<rbrakk> \<Longrightarrow> x \<in> SAMEQUOT z (map \<pi> ` (Z \<inter> lang (n + 1) (ENC (n + 1) X)))
[PROOF STEP]
assume "w \<in> SAMEQUOT z (map \<pi> ` Z)" "w \<in> lang n (ENC n ((\<lambda>x. x - 1) ` X))"
[PROOF STATE]
proof (state)
this:
w \<in> SAMEQUOT z (map \<pi> ` Z)
w \<in> lang n (ENC n ((\<lambda>x. x - 1) ` X))

goal (1 subgoal):
 1. \<And>x. \<lbrakk>x \<in> SAMEQUOT z (map \<pi> ` Z); x \<in> lang n (ENC n ((\<lambda>x. x - 1) ` X))\<rbrakk> \<Longrightarrow> x \<in> SAMEQUOT z (map \<pi> ` (Z \<inter> lang (n + 1) (ENC (n + 1) X)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
w \<in> SAMEQUOT z (map \<pi> ` Z)
w \<in> lang n (ENC n ((\<lambda>x. x - 1) ` X))
[PROOF STEP]
show "w \<in> SAMEQUOT z (map \<pi> ` (Z \<inter> lang (n + 1) (ENC (n + 1) X)))"
[PROOF STATE]
proof (prove)
using this:
w \<in> SAMEQUOT z (map \<pi> ` Z)
w \<in> lang n (ENC n ((\<lambda>x. x - 1) ` X))

goal (1 subgoal):
 1. w \<in> SAMEQUOT z (map \<pi> ` (Z \<inter> lang (n + 1) (ENC (n + 1) X)))
[PROOF STEP]
unfolding  z_def SAMEQUOT_def
[PROOF STATE]
proof (prove)
using this:
w \<in> {fin_cut_same (any, replicate n False) x @ replicate m (any, replicate n False) |x m. x \<in> map \<pi> ` Z}
w \<in> lang n (ENC n ((\<lambda>x. x - 1) ` X))

goal (1 subgoal):
 1. w \<in> {fin_cut_same (any, replicate n False) x @ replicate m (any, replicate n False) |x m. x \<in> map \<pi> ` (Z \<inter> lang (n + 1) (ENC (n + 1) X))}
[PROOF STEP]
proof (safe, intro exI conjI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x m xa. \<lbrakk>fin_cut_same (any, replicate n False) (map \<pi> xa) @ replicate m (any, replicate n False) \<in> lang n (ENC n ((\<lambda>x. x - 1) ` X)); w = fin_cut_same (any, replicate n False) (map \<pi> xa) @ replicate m (any, replicate n False); xa \<in> Z; w \<in> {fin_cut_same (any, replicate n False) x @ replicate m (any, replicate n False) |x m. x \<in> map \<pi> ` Z}; w \<in> lang n (ENC n ((\<lambda>x. x - 1) ` X))\<rbrakk> \<Longrightarrow> fin_cut_same (any, replicate n False) (map \<pi> xa) @ replicate m (any, replicate n False) = fin_cut_same (any, replicate n False) (?x13 x m xa) @ replicate (?m14 x m xa) (any, replicate n False)
 2. \<And>x m xa. \<lbrakk>fin_cut_same (any, replicate n False) (map \<pi> xa) @ replicate m (any, replicate n False) \<in> lang n (ENC n ((\<lambda>x. x - 1) ` X)); w = fin_cut_same (any, replicate n False) (map \<pi> xa) @ replicate m (any, replicate n False); xa \<in> Z; w \<in> {fin_cut_same (any, replicate n False) x @ replicate m (any, replicate n False) |x m. x \<in> map \<pi> ` Z}; w \<in> lang n (ENC n ((\<lambda>x. x - 1) ` X))\<rbrakk> \<Longrightarrow> ?x13 x m xa \<in> map \<pi> ` (Z \<inter> lang (n + 1) (ENC (n + 1) X))
[PROOF STEP]
fix m x
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x m xa. \<lbrakk>fin_cut_same (any, replicate n False) (map \<pi> xa) @ replicate m (any, replicate n False) \<in> lang n (ENC n ((\<lambda>x. x - 1) ` X)); w = fin_cut_same (any, replicate n False) (map \<pi> xa) @ replicate m (any, replicate n False); xa \<in> Z; w \<in> {fin_cut_same (any, replicate n False) x @ replicate m (any, replicate n False) |x m. x \<in> map \<pi> ` Z}; w \<in> lang n (ENC n ((\<lambda>x. x - 1) ` X))\<rbrakk> \<Longrightarrow> fin_cut_same (any, replicate n False) (map \<pi> xa) @ replicate m (any, replicate n False) = fin_cut_same (any, replicate n False) (?x13 x m xa) @ replicate (?m14 x m xa) (any, replicate n False)
 2. \<And>x m xa. \<lbrakk>fin_cut_same (any, replicate n False) (map \<pi> xa) @ replicate m (any, replicate n False) \<in> lang n (ENC n ((\<lambda>x. x - 1) ` X)); w = fin_cut_same (any, replicate n False) (map \<pi> xa) @ replicate m (any, replicate n False); xa \<in> Z; w \<in> {fin_cut_same (any, replicate n False) x @ replicate m (any, replicate n False) |x m. x \<in> map \<pi> ` Z}; w \<in> lang n (ENC n ((\<lambda>x. x - 1) ` X))\<rbrakk> \<Longrightarrow> ?x13 x m xa \<in> map \<pi> ` (Z \<inter> lang (n + 1) (ENC (n + 1) X))
[PROOF STEP]
assume \<pi>x: "fin_cut_same (any, replicate n False) (map \<pi> x) @
       replicate m (any, replicate n False) \<in> lang n (ENC n ((\<lambda>x. x - 1) ` X))" and "x \<in> Z"
[PROOF STATE]
proof (state)
this:
fin_cut_same (any, replicate n False) (map \<pi> x) @ replicate m (any, replicate n False) \<in> lang n (ENC n ((\<lambda>x. x - 1) ` X))
x \<in> Z

goal (2 subgoals):
 1. \<And>x m xa. \<lbrakk>fin_cut_same (any, replicate n False) (map \<pi> xa) @ replicate m (any, replicate n False) \<in> lang n (ENC n ((\<lambda>x. x - 1) ` X)); w = fin_cut_same (any, replicate n False) (map \<pi> xa) @ replicate m (any, replicate n False); xa \<in> Z; w \<in> {fin_cut_same (any, replicate n False) x @ replicate m (any, replicate n False) |x m. x \<in> map \<pi> ` Z}; w \<in> lang n (ENC n ((\<lambda>x. x - 1) ` X))\<rbrakk> \<Longrightarrow> fin_cut_same (any, replicate n False) (map \<pi> xa) @ replicate m (any, replicate n False) = fin_cut_same (any, replicate n False) (?x13 x m xa) @ replicate (?m14 x m xa) (any, replicate n False)
 2. \<And>x m xa. \<lbrakk>fin_cut_same (any, replicate n False) (map \<pi> xa) @ replicate m (any, replicate n False) \<in> lang n (ENC n ((\<lambda>x. x - 1) ` X)); w = fin_cut_same (any, replicate n False) (map \<pi> xa) @ replicate m (any, replicate n False); xa \<in> Z; w \<in> {fin_cut_same (any, replicate n False) x @ replicate m (any, replicate n False) |x m. x \<in> map \<pi> ` Z}; w \<in> lang n (ENC n ((\<lambda>x. x - 1) ` X))\<rbrakk> \<Longrightarrow> ?x13 x m xa \<in> map \<pi> ` (Z \<inter> lang (n + 1) (ENC (n + 1) X))
[PROOF STEP]
show "map \<pi> x \<in> map \<pi> ` (Z \<inter> lang (n + 1) (ENC (n + 1) X))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map \<pi> x \<in> map \<pi> ` (Z \<inter> lang (n + 1) (ENC (n + 1) X))
[PROOF STEP]
proof (intro imageI IntI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. x \<in> Z
 2. x \<in> lang (n + 1) (ENC (n + 1) X)
[PROOF STEP]
from \<open>x \<in> Z\<close> assms(4)
[PROOF STATE]
proof (chain)
picking this:
x \<in> Z
Z \<subseteq> lists ((set \<circ> \<sigma> \<Sigma>) (n + 1))
[PROOF STEP]
have "\<forall>(_, x)\<in>set x. x \<noteq> []"
[PROOF STATE]
proof (prove)
using this:
x \<in> Z
Z \<subseteq> lists ((set \<circ> \<sigma> \<Sigma>) (n + 1))

goal (1 subgoal):
 1. \<forall>(uu_, x)\<in>set x. x \<noteq> []
[PROOF STEP]
by (auto simp: \<sigma>_def)
[PROOF STATE]
proof (state)
this:
\<forall>(uu_, x)\<in>set x. x \<noteq> []

goal (2 subgoals):
 1. x \<in> Z
 2. x \<in> lang (n + 1) (ENC (n + 1) X)
[PROOF STEP]
with \<pi>x assms(2)
[PROOF STATE]
proof (chain)
picking this:
fin_cut_same (any, replicate n False) (map \<pi> x) @ replicate m (any, replicate n False) \<in> lang n (ENC n ((\<lambda>x. x - 1) ` X))
0 \<notin> X
\<forall>(uu_, x)\<in>set x. x \<noteq> []
[PROOF STEP]
show "x \<in> lang (n + 1) (ENC (n + 1) X)"
[PROOF STATE]
proof (prove)
using this:
fin_cut_same (any, replicate n False) (map \<pi> x) @ replicate m (any, replicate n False) \<in> lang n (ENC n ((\<lambda>x. x - 1) ` X))
0 \<notin> X
\<forall>(uu_, x)\<in>set x. x \<noteq> []

goal (1 subgoal):
 1. x \<in> lang (n + 1) (ENC (n + 1) X)
[PROOF STEP]
unfolding lang_ENC[OF assms(3) subset_refl] lang_ENC[OF * subset_refl]
[PROOF STATE]
proof (prove)
using this:
fin_cut_same (any, replicate n False) (map \<pi> x) @ replicate m (any, replicate n False) \<in> \<Union> {enc (w, I) |w I. length I = n \<and> wf_interp w I \<and> (\<forall>i\<in>(\<lambda>x. x - 1) ` X. case I ! i of Inl x \<Rightarrow> True | Inr x \<Rightarrow> False) \<and> (\<forall>i\<in>{0..<n} - (\<lambda>x. x - 1) ` X. case I ! i of Inl x \<Rightarrow> False | Inr x \<Rightarrow> True)}
0 \<notin> X
\<forall>(uu_, x)\<in>set x. x \<noteq> []

goal (1 subgoal):
 1. x \<in> \<Union> {enc (w, I) |w I. length I = n + 1 \<and> wf_interp w I \<and> (\<forall>i\<in>X. case I ! i of Inl x \<Rightarrow> True | Inr x \<Rightarrow> False) \<and> (\<forall>i\<in>{0..<n + 1} - X. case I ! i of Inl x \<Rightarrow> False | Inr x \<Rightarrow> True)}
[PROOF STEP]
proof (safe, intro UnionI[OF _ project_enc_extend[rotated]] CollectI exI conjI)
[PROOF STATE]
proof (state)
goal (10 subgoals):
 1. \<And>Xa w I. \<lbrakk>0 \<notin> X; \<forall>(uu_, x)\<in>set x. x \<noteq> []; fin_cut_same (any, replicate (length I) False) (map \<pi> x) @ replicate m (any, replicate (length I) False) \<in> enc (w, I); n = length I; \<forall>a\<in>set w. a \<in> set \<Sigma>; Ball (set I) (case_sum (\<lambda>a. True) finite); \<forall>i\<in>(\<lambda>x. x - 1) ` X. case I ! i of Inl x \<Rightarrow> True | Inr x \<Rightarrow> False; \<forall>i\<in>{0..<length I} - (\<lambda>x. x - 1) ` X. case I ! i of Inl x \<Rightarrow> False | Inr x \<Rightarrow> True; fin_cut_same (any, replicate n False) (map \<pi> x) @ replicate m (any, replicate n False) \<in> \<Union> {enc (w, I) |w I. length I = n \<and> wf_interp w I \<and> (\<forall>i\<in>(\<lambda>x. x - 1) ` X. case I ! i of Inl x \<Rightarrow> True | Inr x \<Rightarrow> False) \<and> (\<forall>i\<in>{0..<n} - (\<lambda>x. x - 1) ` X. case I ! i of Inl x \<Rightarrow> False | Inr x \<Rightarrow> True)}; 0 \<notin> X; \<forall>(uu_, x)\<in>set x. x \<noteq> []\<rbrakk> \<Longrightarrow> enc (?w26 Xa w I, Inr (positions_in_row (x @- sconst (any, replicate (Suc (length (?I26 Xa w I))) False)) 0) # ?I26 Xa w I) = enc (?w30 Xa w I, ?I31 Xa w I)
 2. \<And>Xa w I. \<lbrakk>0 \<notin> X; \<forall>(uu_, x)\<in>set x. x \<noteq> []; fin_cut_same (any, replicate (length I) False) (map \<pi> x) @ replicate m (any, replicate (length I) False) \<in> enc (w, I); n = length I; \<forall>a\<in>set w. a \<in> set \<Sigma>; Ball (set I) (case_sum (\<lambda>a. True) finite); \<forall>i\<in>(\<lambda>x. x - 1) ` X. case I ! i of Inl x \<Rightarrow> True | Inr x \<Rightarrow> False; \<forall>i\<in>{0..<length I} - (\<lambda>x. x - 1) ` X. case I ! i of Inl x \<Rightarrow> False | Inr x \<Rightarrow> True; fin_cut_same (any, replicate n False) (map \<pi> x) @ replicate m (any, replicate n False) \<in> \<Union> {enc (w, I) |w I. length I = n \<and> wf_interp w I \<and> (\<forall>i\<in>(\<lambda>x. x - 1) ` X. case I ! i of Inl x \<Rightarrow> True | Inr x \<Rightarrow> False) \<and> (\<forall>i\<in>{0..<n} - (\<lambda>x. x - 1) ` X. case I ! i of Inl x \<Rightarrow> False | Inr x \<Rightarrow> True)}; 0 \<notin> X; \<forall>(uu_, x)\<in>set x. x \<noteq> []\<rbrakk> \<Longrightarrow> length (?I31 Xa w I) = length I + 1
 3. \<And>Xa w I. \<lbrakk>0 \<notin> X; \<forall>(uu_, x)\<in>set x. x \<noteq> []; fin_cut_same (any, replicate (length I) False) (map \<pi> x) @ replicate m (any, replicate (length I) False) \<in> enc (w, I); n = length I; \<forall>a\<in>set w. a \<in> set \<Sigma>; Ball (set I) (case_sum (\<lambda>a. True) finite); \<forall>i\<in>(\<lambda>x. x - 1) ` X. case I ! i of Inl x \<Rightarrow> True | Inr x \<Rightarrow> False; \<forall>i\<in>{0..<length I} - (\<lambda>x. x - 1) ` X. case I ! i of Inl x \<Rightarrow> False | Inr x \<Rightarrow> True; fin_cut_same (any, replicate n False) (map \<pi> x) @ replicate m (any, replicate n False) \<in> \<Union> {enc (w, I) |w I. length I = n \<and> wf_interp w I \<and> (\<forall>i\<in>(\<lambda>x. x - 1) ` X. case I ! i of Inl x \<Rightarrow> True | Inr x \<Rightarrow> False) \<and> (\<forall>i\<in>{0..<n} - (\<lambda>x. x - 1) ` X. case I ! i of Inl x \<Rightarrow> False | Inr x \<Rightarrow> True)}; 0 \<notin> X; \<forall>(uu_, x)\<in>set x. x \<noteq> []\<rbrakk> \<Longrightarrow> \<forall>a\<in>set (?w30 Xa w I). a \<in> set \<Sigma>
 4. \<And>Xa w I. \<lbrakk>0 \<notin> X; \<forall>(uu_, x)\<in>set x. x \<noteq> []; fin_cut_same (any, replicate (length I) False) (map \<pi> x) @ replicate m (any, replicate (length I) False) \<in> enc (w, I); n = length I; \<forall>a\<in>set w. a \<in> set \<Sigma>; Ball (set I) (case_sum (\<lambda>a. True) finite); \<forall>i\<in>(\<lambda>x. x - 1) ` X. case I ! i of Inl x \<Rightarrow> True | Inr x \<Rightarrow> False; \<forall>i\<in>{0..<length I} - (\<lambda>x. x - 1) ` X. case I ! i of Inl x \<Rightarrow> False | Inr x \<Rightarrow> True; fin_cut_same (any, replicate n False) (map \<pi> x) @ replicate m (any, replicate n False) \<in> \<Union> {enc (w, I) |w I. length I = n \<and> wf_interp w I \<and> (\<forall>i\<in>(\<lambda>x. x - 1) ` X. case I ! i of Inl x \<Rightarrow> True | Inr x \<Rightarrow> False) \<and> (\<forall>i\<in>{0..<n} - (\<lambda>x. x - 1) ` X. case I ! i of Inl x \<Rightarrow> False | Inr x \<Rightarrow> True)}; 0 \<notin> X; \<forall>(uu_, x)\<in>set x. x \<noteq> []\<rbrakk> \<Longrightarrow> Ball (set (?I31 Xa w I)) (case_sum (\<lambda>a. True) finite)
 5. \<And>Xa w I. \<lbrakk>0 \<notin> X; \<forall>(uu_, x)\<in>set x. x \<noteq> []; fin_cut_same (any, replicate (length I) False) (map \<pi> x) @ replicate m (any, replicate (length I) False) \<in> enc (w, I); n = length I; \<forall>a\<in>set w. a \<in> set \<Sigma>; Ball (set I) (case_sum (\<lambda>a. True) finite); \<forall>i\<in>(\<lambda>x. x - 1) ` X. case I ! i of Inl x \<Rightarrow> True | Inr x \<Rightarrow> False; \<forall>i\<in>{0..<length I} - (\<lambda>x. x - 1) ` X. case I ! i of Inl x \<Rightarrow> False | Inr x \<Rightarrow> True; fin_cut_same (any, replicate n False) (map \<pi> x) @ replicate m (any, replicate n False) \<in> \<Union> {enc (w, I) |w I. length I = n \<and> wf_interp w I \<and> (\<forall>i\<in>(\<lambda>x. x - 1) ` X. case I ! i of Inl x \<Rightarrow> True | Inr x \<Rightarrow> False) \<and> (\<forall>i\<in>{0..<n} - (\<lambda>x. x - 1) ` X. case I ! i of Inl x \<Rightarrow> False | Inr x \<Rightarrow> True)}; 0 \<notin> X; \<forall>(uu_, x)\<in>set x. x \<noteq> []\<rbrakk> \<Longrightarrow> \<forall>i\<in>X. case ?I31 Xa w I ! i of Inl x \<Rightarrow> True | Inr x \<Rightarrow> False
 6. \<And>Xa w I. \<lbrakk>0 \<notin> X; \<forall>(uu_, x)\<in>set x. x \<noteq> []; fin_cut_same (any, replicate (length I) False) (map \<pi> x) @ replicate m (any, replicate (length I) False) \<in> enc (w, I); n = length I; \<forall>a\<in>set w. a \<in> set \<Sigma>; Ball (set I) (case_sum (\<lambda>a. True) finite); \<forall>i\<in>(\<lambda>x. x - 1) ` X. case I ! i of Inl x \<Rightarrow> True | Inr x \<Rightarrow> False; \<forall>i\<in>{0..<length I} - (\<lambda>x. x - 1) ` X. case I ! i of Inl x \<Rightarrow> False | Inr x \<Rightarrow> True; fin_cut_same (any, replicate n False) (map \<pi> x) @ replicate m (any, replicate n False) \<in> \<Union> {enc (w, I) |w I. length I = n \<and> wf_interp w I \<and> (\<forall>i\<in>(\<lambda>x. x - 1) ` X. case I ! i of Inl x \<Rightarrow> True | Inr x \<Rightarrow> False) \<and> (\<forall>i\<in>{0..<n} - (\<lambda>x. x - 1) ` X. case I ! i of Inl x \<Rightarrow> False | Inr x \<Rightarrow> True)}; 0 \<notin> X; \<forall>(uu_, x)\<in>set x. x \<noteq> []\<rbrakk> \<Longrightarrow> \<forall>i\<in>{0..<length I + 1} - X. case ?I31 Xa w I ! i of Inl x \<Rightarrow> False | Inr x \<Rightarrow> True
 7. \<And>Xa w I. \<lbrakk>0 \<notin> X; \<forall>(uu_, x)\<in>set x. x \<noteq> []; fin_cut_same (any, replicate (length I) False) (map \<pi> x) @ replicate m (any, replicate (length I) False) \<in> enc (w, I); n = length I; \<forall>a\<in>set w. a \<in> set \<Sigma>; Ball (set I) (case_sum (\<lambda>a. True) finite); \<forall>i\<in>(\<lambda>x. x - 1) ` X. case I ! i of Inl x \<Rightarrow> True | Inr x \<Rightarrow> False; \<forall>i\<in>{0..<length I} - (\<lambda>x. x - 1) ` X. case I ! i of Inl x \<Rightarrow> False | Inr x \<Rightarrow> True; fin_cut_same (any, replicate n False) (map \<pi> x) @ replicate m (any, replicate n False) \<in> \<Union> {enc (w, I) |w I. length I = n \<and> wf_interp w I \<and> (\<forall>i\<in>(\<lambda>x. x - 1) ` X. case I ! i of Inl x \<Rightarrow> True | Inr x \<Rightarrow> False) \<and> (\<forall>i\<in>{0..<n} - (\<lambda>x. x - 1) ` X. case I ! i of Inl x \<Rightarrow> False | Inr x \<Rightarrow> True)}; 0 \<notin> X; \<forall>(uu_, x)\<in>set x. x \<noteq> []\<rbrakk> \<Longrightarrow> fin_cut_same (any, replicate (length (?I26 Xa w I)) False) (map \<pi> x) @ replicate (?m26 Xa w I) (any, replicate (length (?I26 Xa w I)) False) \<in> enc (?w26 Xa w I, ?I26 Xa w I)
 8. \<And>Xa w I. \<lbrakk>0 \<notin> X; \<forall>(uu_, x)\<in>set x. x \<noteq> []; fin_cut_same (any, replicate (length I) False) (map \<pi> x) @ replicate m (any, replicate (length I) False) \<in> enc (w, I); n = length I; \<forall>a\<in>set w. a \<in> set \<Sigma>; Ball (set I) (case_sum (\<lambda>a. True) finite); \<forall>i\<in>(\<lambda>x. x - 1) ` X. case I ! i of Inl x \<Rightarrow> True | Inr x \<Rightarrow> False; \<forall>i\<in>{0..<length I} - (\<lambda>x. x - 1) ` X. case I ! i of Inl x \<Rightarrow> False | Inr x \<Rightarrow> True; fin_cut_same (any, replicate n False) (map \<pi> x) @ replicate m (any, replicate n False) \<in> \<Union> {enc (w, I) |w I. length I = n \<and> wf_interp w I \<and> (\<forall>i\<in>(\<lambda>x. x - 1) ` X. case I ! i of Inl x \<Rightarrow> True | Inr x \<Rightarrow> False) \<and> (\<forall>i\<in>{0..<n} - (\<lambda>x. x - 1) ` X. case I ! i of Inl x \<Rightarrow> False | Inr x \<Rightarrow> True)}; 0 \<notin> X; \<forall>(uu_, x)\<in>set x. x \<noteq> []\<rbrakk> \<Longrightarrow> \<forall>(uu_, x)\<in>set x. x \<noteq> []
 9. \<And>Xa w I. \<lbrakk>0 \<notin> X; \<forall>(uu_, x)\<in>set x. x \<noteq> []; fin_cut_same (any, replicate (length I) False) (map \<pi> x) @ replicate m (any, replicate (length I) False) \<in> enc (w, I); n = length I; \<forall>a\<in>set w. a \<in> set \<Sigma>; Ball (set I) (case_sum (\<lambda>a. True) finite); \<forall>i\<in>(\<lambda>x. x - 1) ` X. case I ! i of Inl x \<Rightarrow> True | Inr x \<Rightarrow> False; \<forall>i\<in>{0..<length I} - (\<lambda>x. x - 1) ` X. case I ! i of Inl x \<Rightarrow> False | Inr x \<Rightarrow> True; fin_cut_same (any, replicate n False) (map \<pi> x) @ replicate m (any, replicate n False) \<in> \<Union> {enc (w, I) |w I. length I = n \<and> wf_interp w I \<and> (\<forall>i\<in>(\<lambda>x. x - 1) ` X. case I ! i of Inl x \<Rightarrow> True | Inr x \<Rightarrow> False) \<and> (\<forall>i\<in>{0..<n} - (\<lambda>x. x - 1) ` X. case I ! i of Inl x \<Rightarrow> False | Inr x \<Rightarrow> True)}; 0 \<notin> X; \<forall>(uu_, x)\<in>set x. x \<noteq> []\<rbrakk> \<Longrightarrow> \<forall>a\<in>set (?w26 Xa w I). a \<in> set \<Sigma>
 10. \<And>Xa w I. \<lbrakk>0 \<notin> X; \<forall>(uu_, x)\<in>set x. x \<noteq> []; fin_cut_same (any, replicate (length I) False) (map \<pi> x) @ replicate m (any, replicate (length I) False) \<in> enc (w, I); n = length I; \<forall>a\<in>set w. a \<in> set \<Sigma>; Ball (set I) (case_sum (\<lambda>a. True) finite); \<forall>i\<in>(\<lambda>x. x - 1) ` X. case I ! i of Inl x \<Rightarrow> True | Inr x \<Rightarrow> False; \<forall>i\<in>{0..<length I} - (\<lambda>x. x - 1) ` X. case I ! i of Inl x \<Rightarrow> False | Inr x \<Rightarrow> True; fin_cut_same (any, replicate n False) (map \<pi> x) @ replicate m (any, replicate n False) \<in> \<Union> {enc (w, I) |w I. length I = n \<and> wf_interp w I \<and> (\<forall>i\<in>(\<lambda>x. x - 1) ` X. case I ! i of Inl x \<Rightarrow> True | Inr x \<Rightarrow> False) \<and> (\<forall>i\<in>{0..<n} - (\<lambda>x. x - 1) ` X. case I ! i of Inl x \<Rightarrow> False | Inr x \<Rightarrow> True)}; 0 \<notin> X; \<forall>(uu_, x)\<in>set x. x \<noteq> []\<rbrakk> \<Longrightarrow> \<forall>x\<in>set (?I26 Xa w I). case x of Inl a \<Rightarrow> True | Inr P \<Rightarrow> finite P
[PROOF STEP]
fix w and I :: "(nat + nat set) list"
[PROOF STATE]
proof (state)
goal (10 subgoals):
 1. \<And>Xa w I. \<lbrakk>0 \<notin> X; \<forall>(uu_, x)\<in>set x. x \<noteq> []; fin_cut_same (any, replicate (length I) False) (map \<pi> x) @ replicate m (any, replicate (length I) False) \<in> enc (w, I); n = length I; \<forall>a\<in>set w. a \<in> set \<Sigma>; Ball (set I) (case_sum (\<lambda>a. True) finite); \<forall>i\<in>(\<lambda>x. x - 1) ` X. case I ! i of Inl x \<Rightarrow> True | Inr x \<Rightarrow> False; \<forall>i\<in>{0..<length I} - (\<lambda>x. x - 1) ` X. case I ! i of Inl x \<Rightarrow> False | Inr x \<Rightarrow> True; fin_cut_same (any, replicate n False) (map \<pi> x) @ replicate m (any, replicate n False) \<in> \<Union> {enc (w, I) |w I. length I = n \<and> wf_interp w I \<and> (\<forall>i\<in>(\<lambda>x. x - 1) ` X. case I ! i of Inl x \<Rightarrow> True | Inr x \<Rightarrow> False) \<and> (\<forall>i\<in>{0..<n} - (\<lambda>x. x - 1) ` X. case I ! i of Inl x \<Rightarrow> False | Inr x \<Rightarrow> True)}; 0 \<notin> X; \<forall>(uu_, x)\<in>set x. x \<noteq> []\<rbrakk> \<Longrightarrow> enc (?w26 Xa w I, Inr (positions_in_row (x @- sconst (any, replicate (Suc (length (?I26 Xa w I))) False)) 0) # ?I26 Xa w I) = enc (?w30 Xa w I, ?I31 Xa w I)
 2. \<And>Xa w I. \<lbrakk>0 \<notin> X; \<forall>(uu_, x)\<in>set x. x \<noteq> []; fin_cut_same (any, replicate (length I) False) (map \<pi> x) @ replicate m (any, replicate (length I) False) \<in> enc (w, I); n = length I; \<forall>a\<in>set w. a \<in> set \<Sigma>; Ball (set I) (case_sum (\<lambda>a. True) finite); \<forall>i\<in>(\<lambda>x. x - 1) ` X. case I ! i of Inl x \<Rightarrow> True | Inr x \<Rightarrow> False; \<forall>i\<in>{0..<length I} - (\<lambda>x. x - 1) ` X. case I ! i of Inl x \<Rightarrow> False | Inr x \<Rightarrow> True; fin_cut_same (any, replicate n False) (map \<pi> x) @ replicate m (any, replicate n False) \<in> \<Union> {enc (w, I) |w I. length I = n \<and> wf_interp w I \<and> (\<forall>i\<in>(\<lambda>x. x - 1) ` X. case I ! i of Inl x \<Rightarrow> True | Inr x \<Rightarrow> False) \<and> (\<forall>i\<in>{0..<n} - (\<lambda>x. x - 1) ` X. case I ! i of Inl x \<Rightarrow> False | Inr x \<Rightarrow> True)}; 0 \<notin> X; \<forall>(uu_, x)\<in>set x. x \<noteq> []\<rbrakk> \<Longrightarrow> length (?I31 Xa w I) = length I + 1
 3. \<And>Xa w I. \<lbrakk>0 \<notin> X; \<forall>(uu_, x)\<in>set x. x \<noteq> []; fin_cut_same (any, replicate (length I) False) (map \<pi> x) @ replicate m (any, replicate (length I) False) \<in> enc (w, I); n = length I; \<forall>a\<in>set w. a \<in> set \<Sigma>; Ball (set I) (case_sum (\<lambda>a. True) finite); \<forall>i\<in>(\<lambda>x. x - 1) ` X. case I ! i of Inl x \<Rightarrow> True | Inr x \<Rightarrow> False; \<forall>i\<in>{0..<length I} - (\<lambda>x. x - 1) ` X. case I ! i of Inl x \<Rightarrow> False | Inr x \<Rightarrow> True; fin_cut_same (any, replicate n False) (map \<pi> x) @ replicate m (any, replicate n False) \<in> \<Union> {enc (w, I) |w I. length I = n \<and> wf_interp w I \<and> (\<forall>i\<in>(\<lambda>x. x - 1) ` X. case I ! i of Inl x \<Rightarrow> True | Inr x \<Rightarrow> False) \<and> (\<forall>i\<in>{0..<n} - (\<lambda>x. x - 1) ` X. case I ! i of Inl x \<Rightarrow> False | Inr x \<Rightarrow> True)}; 0 \<notin> X; \<forall>(uu_, x)\<in>set x. x \<noteq> []\<rbrakk> \<Longrightarrow> \<forall>a\<in>set (?w30 Xa w I). a \<in> set \<Sigma>
 4. \<And>Xa w I. \<lbrakk>0 \<notin> X; \<forall>(uu_, x)\<in>set x. x \<noteq> []; fin_cut_same (any, replicate (length I) False) (map \<pi> x) @ replicate m (any, replicate (length I) False) \<in> enc (w, I); n = length I; \<forall>a\<in>set w. a \<in> set \<Sigma>; Ball (set I) (case_sum (\<lambda>a. True) finite); \<forall>i\<in>(\<lambda>x. x - 1) ` X. case I ! i of Inl x \<Rightarrow> True | Inr x \<Rightarrow> False; \<forall>i\<in>{0..<length I} - (\<lambda>x. x - 1) ` X. case I ! i of Inl x \<Rightarrow> False | Inr x \<Rightarrow> True; fin_cut_same (any, replicate n False) (map \<pi> x) @ replicate m (any, replicate n False) \<in> \<Union> {enc (w, I) |w I. length I = n \<and> wf_interp w I \<and> (\<forall>i\<in>(\<lambda>x. x - 1) ` X. case I ! i of Inl x \<Rightarrow> True | Inr x \<Rightarrow> False) \<and> (\<forall>i\<in>{0..<n} - (\<lambda>x. x - 1) ` X. case I ! i of Inl x \<Rightarrow> False | Inr x \<Rightarrow> True)}; 0 \<notin> X; \<forall>(uu_, x)\<in>set x. x \<noteq> []\<rbrakk> \<Longrightarrow> Ball (set (?I31 Xa w I)) (case_sum (\<lambda>a. True) finite)
 5. \<And>Xa w I. \<lbrakk>0 \<notin> X; \<forall>(uu_, x)\<in>set x. x \<noteq> []; fin_cut_same (any, replicate (length I) False) (map \<pi> x) @ replicate m (any, replicate (length I) False) \<in> enc (w, I); n = length I; \<forall>a\<in>set w. a \<in> set \<Sigma>; Ball (set I) (case_sum (\<lambda>a. True) finite); \<forall>i\<in>(\<lambda>x. x - 1) ` X. case I ! i of Inl x \<Rightarrow> True | Inr x \<Rightarrow> False; \<forall>i\<in>{0..<length I} - (\<lambda>x. x - 1) ` X. case I ! i of Inl x \<Rightarrow> False | Inr x \<Rightarrow> True; fin_cut_same (any, replicate n False) (map \<pi> x) @ replicate m (any, replicate n False) \<in> \<Union> {enc (w, I) |w I. length I = n \<and> wf_interp w I \<and> (\<forall>i\<in>(\<lambda>x. x - 1) ` X. case I ! i of Inl x \<Rightarrow> True | Inr x \<Rightarrow> False) \<and> (\<forall>i\<in>{0..<n} - (\<lambda>x. x - 1) ` X. case I ! i of Inl x \<Rightarrow> False | Inr x \<Rightarrow> True)}; 0 \<notin> X; \<forall>(uu_, x)\<in>set x. x \<noteq> []\<rbrakk> \<Longrightarrow> \<forall>i\<in>X. case ?I31 Xa w I ! i of Inl x \<Rightarrow> True | Inr x \<Rightarrow> False
 6. \<And>Xa w I. \<lbrakk>0 \<notin> X; \<forall>(uu_, x)\<in>set x. x \<noteq> []; fin_cut_same (any, replicate (length I) False) (map \<pi> x) @ replicate m (any, replicate (length I) False) \<in> enc (w, I); n = length I; \<forall>a\<in>set w. a \<in> set \<Sigma>; Ball (set I) (case_sum (\<lambda>a. True) finite); \<forall>i\<in>(\<lambda>x. x - 1) ` X. case I ! i of Inl x \<Rightarrow> True | Inr x \<Rightarrow> False; \<forall>i\<in>{0..<length I} - (\<lambda>x. x - 1) ` X. case I ! i of Inl x \<Rightarrow> False | Inr x \<Rightarrow> True; fin_cut_same (any, replicate n False) (map \<pi> x) @ replicate m (any, replicate n False) \<in> \<Union> {enc (w, I) |w I. length I = n \<and> wf_interp w I \<and> (\<forall>i\<in>(\<lambda>x. x - 1) ` X. case I ! i of Inl x \<Rightarrow> True | Inr x \<Rightarrow> False) \<and> (\<forall>i\<in>{0..<n} - (\<lambda>x. x - 1) ` X. case I ! i of Inl x \<Rightarrow> False | Inr x \<Rightarrow> True)}; 0 \<notin> X; \<forall>(uu_, x)\<in>set x. x \<noteq> []\<rbrakk> \<Longrightarrow> \<forall>i\<in>{0..<length I + 1} - X. case ?I31 Xa w I ! i of Inl x \<Rightarrow> False | Inr x \<Rightarrow> True
 7. \<And>Xa w I. \<lbrakk>0 \<notin> X; \<forall>(uu_, x)\<in>set x. x \<noteq> []; fin_cut_same (any, replicate (length I) False) (map \<pi> x) @ replicate m (any, replicate (length I) False) \<in> enc (w, I); n = length I; \<forall>a\<in>set w. a \<in> set \<Sigma>; Ball (set I) (case_sum (\<lambda>a. True) finite); \<forall>i\<in>(\<lambda>x. x - 1) ` X. case I ! i of Inl x \<Rightarrow> True | Inr x \<Rightarrow> False; \<forall>i\<in>{0..<length I} - (\<lambda>x. x - 1) ` X. case I ! i of Inl x \<Rightarrow> False | Inr x \<Rightarrow> True; fin_cut_same (any, replicate n False) (map \<pi> x) @ replicate m (any, replicate n False) \<in> \<Union> {enc (w, I) |w I. length I = n \<and> wf_interp w I \<and> (\<forall>i\<in>(\<lambda>x. x - 1) ` X. case I ! i of Inl x \<Rightarrow> True | Inr x \<Rightarrow> False) \<and> (\<forall>i\<in>{0..<n} - (\<lambda>x. x - 1) ` X. case I ! i of Inl x \<Rightarrow> False | Inr x \<Rightarrow> True)}; 0 \<notin> X; \<forall>(uu_, x)\<in>set x. x \<noteq> []\<rbrakk> \<Longrightarrow> fin_cut_same (any, replicate (length (?I26 Xa w I)) False) (map \<pi> x) @ replicate (?m26 Xa w I) (any, replicate (length (?I26 Xa w I)) False) \<in> enc (?w26 Xa w I, ?I26 Xa w I)
 8. \<And>Xa w I. \<lbrakk>0 \<notin> X; \<forall>(uu_, x)\<in>set x. x \<noteq> []; fin_cut_same (any, replicate (length I) False) (map \<pi> x) @ replicate m (any, replicate (length I) False) \<in> enc (w, I); n = length I; \<forall>a\<in>set w. a \<in> set \<Sigma>; Ball (set I) (case_sum (\<lambda>a. True) finite); \<forall>i\<in>(\<lambda>x. x - 1) ` X. case I ! i of Inl x \<Rightarrow> True | Inr x \<Rightarrow> False; \<forall>i\<in>{0..<length I} - (\<lambda>x. x - 1) ` X. case I ! i of Inl x \<Rightarrow> False | Inr x \<Rightarrow> True; fin_cut_same (any, replicate n False) (map \<pi> x) @ replicate m (any, replicate n False) \<in> \<Union> {enc (w, I) |w I. length I = n \<and> wf_interp w I \<and> (\<forall>i\<in>(\<lambda>x. x - 1) ` X. case I ! i of Inl x \<Rightarrow> True | Inr x \<Rightarrow> False) \<and> (\<forall>i\<in>{0..<n} - (\<lambda>x. x - 1) ` X. case I ! i of Inl x \<Rightarrow> False | Inr x \<Rightarrow> True)}; 0 \<notin> X; \<forall>(uu_, x)\<in>set x. x \<noteq> []\<rbrakk> \<Longrightarrow> \<forall>(uu_, x)\<in>set x. x \<noteq> []
 9. \<And>Xa w I. \<lbrakk>0 \<notin> X; \<forall>(uu_, x)\<in>set x. x \<noteq> []; fin_cut_same (any, replicate (length I) False) (map \<pi> x) @ replicate m (any, replicate (length I) False) \<in> enc (w, I); n = length I; \<forall>a\<in>set w. a \<in> set \<Sigma>; Ball (set I) (case_sum (\<lambda>a. True) finite); \<forall>i\<in>(\<lambda>x. x - 1) ` X. case I ! i of Inl x \<Rightarrow> True | Inr x \<Rightarrow> False; \<forall>i\<in>{0..<length I} - (\<lambda>x. x - 1) ` X. case I ! i of Inl x \<Rightarrow> False | Inr x \<Rightarrow> True; fin_cut_same (any, replicate n False) (map \<pi> x) @ replicate m (any, replicate n False) \<in> \<Union> {enc (w, I) |w I. length I = n \<and> wf_interp w I \<and> (\<forall>i\<in>(\<lambda>x. x - 1) ` X. case I ! i of Inl x \<Rightarrow> True | Inr x \<Rightarrow> False) \<and> (\<forall>i\<in>{0..<n} - (\<lambda>x. x - 1) ` X. case I ! i of Inl x \<Rightarrow> False | Inr x \<Rightarrow> True)}; 0 \<notin> X; \<forall>(uu_, x)\<in>set x. x \<noteq> []\<rbrakk> \<Longrightarrow> \<forall>a\<in>set (?w26 Xa w I). a \<in> set \<Sigma>
 10. \<And>Xa w I. \<lbrakk>0 \<notin> X; \<forall>(uu_, x)\<in>set x. x \<noteq> []; fin_cut_same (any, replicate (length I) False) (map \<pi> x) @ replicate m (any, replicate (length I) False) \<in> enc (w, I); n = length I; \<forall>a\<in>set w. a \<in> set \<Sigma>; Ball (set I) (case_sum (\<lambda>a. True) finite); \<forall>i\<in>(\<lambda>x. x - 1) ` X. case I ! i of Inl x \<Rightarrow> True | Inr x \<Rightarrow> False; \<forall>i\<in>{0..<length I} - (\<lambda>x. x - 1) ` X. case I ! i of Inl x \<Rightarrow> False | Inr x \<Rightarrow> True; fin_cut_same (any, replicate n False) (map \<pi> x) @ replicate m (any, replicate n False) \<in> \<Union> {enc (w, I) |w I. length I = n \<and> wf_interp w I \<and> (\<forall>i\<in>(\<lambda>x. x - 1) ` X. case I ! i of Inl x \<Rightarrow> True | Inr x \<Rightarrow> False) \<and> (\<forall>i\<in>{0..<n} - (\<lambda>x. x - 1) ` X. case I ! i of Inl x \<Rightarrow> False | Inr x \<Rightarrow> True)}; 0 \<notin> X; \<forall>(uu_, x)\<in>set x. x \<noteq> []\<rbrakk> \<Longrightarrow> \<forall>x\<in>set (?I26 Xa w I). case x of Inl a \<Rightarrow> True | Inr P \<Rightarrow> finite P
[PROOF STEP]
assume "Ball (set I) (case_sum (\<lambda>a. True) finite)"
[PROOF STATE]
proof (state)
this:
Ball (set I) (case_sum (\<lambda>a. True) finite)

goal (10 subgoals):
 1. \<And>Xa w I. \<lbrakk>0 \<notin> X; \<forall>(uu_, x)\<in>set x. x \<noteq> []; fin_cut_same (any, replicate (length I) False) (map \<pi> x) @ replicate m (any, replicate (length I) False) \<in> enc (w, I); n = length I; \<forall>a\<in>set w. a \<in> set \<Sigma>; Ball (set I) (case_sum (\<lambda>a. True) finite); \<forall>i\<in>(\<lambda>x. x - 1) ` X. case I ! i of Inl x \<Rightarrow> True | Inr x \<Rightarrow> False; \<forall>i\<in>{0..<length I} - (\<lambda>x. x - 1) ` X. case I ! i of Inl x \<Rightarrow> False | Inr x \<Rightarrow> True; fin_cut_same (any, replicate n False) (map \<pi> x) @ replicate m (any, replicate n False) \<in> \<Union> {enc (w, I) |w I. length I = n \<and> wf_interp w I \<and> (\<forall>i\<in>(\<lambda>x. x - 1) ` X. case I ! i of Inl x \<Rightarrow> True | Inr x \<Rightarrow> False) \<and> (\<forall>i\<in>{0..<n} - (\<lambda>x. x - 1) ` X. case I ! i of Inl x \<Rightarrow> False | Inr x \<Rightarrow> True)}; 0 \<notin> X; \<forall>(uu_, x)\<in>set x. x \<noteq> []\<rbrakk> \<Longrightarrow> enc (?w26 Xa w I, Inr (positions_in_row (x @- sconst (any, replicate (Suc (length (?I26 Xa w I))) False)) 0) # ?I26 Xa w I) = enc (?w30 Xa w I, ?I31 Xa w I)
 2. \<And>Xa w I. \<lbrakk>0 \<notin> X; \<forall>(uu_, x)\<in>set x. x \<noteq> []; fin_cut_same (any, replicate (length I) False) (map \<pi> x) @ replicate m (any, replicate (length I) False) \<in> enc (w, I); n = length I; \<forall>a\<in>set w. a \<in> set \<Sigma>; Ball (set I) (case_sum (\<lambda>a. True) finite); \<forall>i\<in>(\<lambda>x. x - 1) ` X. case I ! i of Inl x \<Rightarrow> True | Inr x \<Rightarrow> False; \<forall>i\<in>{0..<length I} - (\<lambda>x. x - 1) ` X. case I ! i of Inl x \<Rightarrow> False | Inr x \<Rightarrow> True; fin_cut_same (any, replicate n False) (map \<pi> x) @ replicate m (any, replicate n False) \<in> \<Union> {enc (w, I) |w I. length I = n \<and> wf_interp w I \<and> (\<forall>i\<in>(\<lambda>x. x - 1) ` X. case I ! i of Inl x \<Rightarrow> True | Inr x \<Rightarrow> False) \<and> (\<forall>i\<in>{0..<n} - (\<lambda>x. x - 1) ` X. case I ! i of Inl x \<Rightarrow> False | Inr x \<Rightarrow> True)}; 0 \<notin> X; \<forall>(uu_, x)\<in>set x. x \<noteq> []\<rbrakk> \<Longrightarrow> length (?I31 Xa w I) = length I + 1
 3. \<And>Xa w I. \<lbrakk>0 \<notin> X; \<forall>(uu_, x)\<in>set x. x \<noteq> []; fin_cut_same (any, replicate (length I) False) (map \<pi> x) @ replicate m (any, replicate (length I) False) \<in> enc (w, I); n = length I; \<forall>a\<in>set w. a \<in> set \<Sigma>; Ball (set I) (case_sum (\<lambda>a. True) finite); \<forall>i\<in>(\<lambda>x. x - 1) ` X. case I ! i of Inl x \<Rightarrow> True | Inr x \<Rightarrow> False; \<forall>i\<in>{0..<length I} - (\<lambda>x. x - 1) ` X. case I ! i of Inl x \<Rightarrow> False | Inr x \<Rightarrow> True; fin_cut_same (any, replicate n False) (map \<pi> x) @ replicate m (any, replicate n False) \<in> \<Union> {enc (w, I) |w I. length I = n \<and> wf_interp w I \<and> (\<forall>i\<in>(\<lambda>x. x - 1) ` X. case I ! i of Inl x \<Rightarrow> True | Inr x \<Rightarrow> False) \<and> (\<forall>i\<in>{0..<n} - (\<lambda>x. x - 1) ` X. case I ! i of Inl x \<Rightarrow> False | Inr x \<Rightarrow> True)}; 0 \<notin> X; \<forall>(uu_, x)\<in>set x. x \<noteq> []\<rbrakk> \<Longrightarrow> \<forall>a\<in>set (?w30 Xa w I). a \<in> set \<Sigma>
 4. \<And>Xa w I. \<lbrakk>0 \<notin> X; \<forall>(uu_, x)\<in>set x. x \<noteq> []; fin_cut_same (any, replicate (length I) False) (map \<pi> x) @ replicate m (any, replicate (length I) False) \<in> enc (w, I); n = length I; \<forall>a\<in>set w. a \<in> set \<Sigma>; Ball (set I) (case_sum (\<lambda>a. True) finite); \<forall>i\<in>(\<lambda>x. x - 1) ` X. case I ! i of Inl x \<Rightarrow> True | Inr x \<Rightarrow> False; \<forall>i\<in>{0..<length I} - (\<lambda>x. x - 1) ` X. case I ! i of Inl x \<Rightarrow> False | Inr x \<Rightarrow> True; fin_cut_same (any, replicate n False) (map \<pi> x) @ replicate m (any, replicate n False) \<in> \<Union> {enc (w, I) |w I. length I = n \<and> wf_interp w I \<and> (\<forall>i\<in>(\<lambda>x. x - 1) ` X. case I ! i of Inl x \<Rightarrow> True | Inr x \<Rightarrow> False) \<and> (\<forall>i\<in>{0..<n} - (\<lambda>x. x - 1) ` X. case I ! i of Inl x \<Rightarrow> False | Inr x \<Rightarrow> True)}; 0 \<notin> X; \<forall>(uu_, x)\<in>set x. x \<noteq> []\<rbrakk> \<Longrightarrow> Ball (set (?I31 Xa w I)) (case_sum (\<lambda>a. True) finite)
 5. \<And>Xa w I. \<lbrakk>0 \<notin> X; \<forall>(uu_, x)\<in>set x. x \<noteq> []; fin_cut_same (any, replicate (length I) False) (map \<pi> x) @ replicate m (any, replicate (length I) False) \<in> enc (w, I); n = length I; \<forall>a\<in>set w. a \<in> set \<Sigma>; Ball (set I) (case_sum (\<lambda>a. True) finite); \<forall>i\<in>(\<lambda>x. x - 1) ` X. case I ! i of Inl x \<Rightarrow> True | Inr x \<Rightarrow> False; \<forall>i\<in>{0..<length I} - (\<lambda>x. x - 1) ` X. case I ! i of Inl x \<Rightarrow> False | Inr x \<Rightarrow> True; fin_cut_same (any, replicate n False) (map \<pi> x) @ replicate m (any, replicate n False) \<in> \<Union> {enc (w, I) |w I. length I = n \<and> wf_interp w I \<and> (\<forall>i\<in>(\<lambda>x. x - 1) ` X. case I ! i of Inl x \<Rightarrow> True | Inr x \<Rightarrow> False) \<and> (\<forall>i\<in>{0..<n} - (\<lambda>x. x - 1) ` X. case I ! i of Inl x \<Rightarrow> False | Inr x \<Rightarrow> True)}; 0 \<notin> X; \<forall>(uu_, x)\<in>set x. x \<noteq> []\<rbrakk> \<Longrightarrow> \<forall>i\<in>X. case ?I31 Xa w I ! i of Inl x \<Rightarrow> True | Inr x \<Rightarrow> False
 6. \<And>Xa w I. \<lbrakk>0 \<notin> X; \<forall>(uu_, x)\<in>set x. x \<noteq> []; fin_cut_same (any, replicate (length I) False) (map \<pi> x) @ replicate m (any, replicate (length I) False) \<in> enc (w, I); n = length I; \<forall>a\<in>set w. a \<in> set \<Sigma>; Ball (set I) (case_sum (\<lambda>a. True) finite); \<forall>i\<in>(\<lambda>x. x - 1) ` X. case I ! i of Inl x \<Rightarrow> True | Inr x \<Rightarrow> False; \<forall>i\<in>{0..<length I} - (\<lambda>x. x - 1) ` X. case I ! i of Inl x \<Rightarrow> False | Inr x \<Rightarrow> True; fin_cut_same (any, replicate n False) (map \<pi> x) @ replicate m (any, replicate n False) \<in> \<Union> {enc (w, I) |w I. length I = n \<and> wf_interp w I \<and> (\<forall>i\<in>(\<lambda>x. x - 1) ` X. case I ! i of Inl x \<Rightarrow> True | Inr x \<Rightarrow> False) \<and> (\<forall>i\<in>{0..<n} - (\<lambda>x. x - 1) ` X. case I ! i of Inl x \<Rightarrow> False | Inr x \<Rightarrow> True)}; 0 \<notin> X; \<forall>(uu_, x)\<in>set x. x \<noteq> []\<rbrakk> \<Longrightarrow> \<forall>i\<in>{0..<length I + 1} - X. case ?I31 Xa w I ! i of Inl x \<Rightarrow> False | Inr x \<Rightarrow> True
 7. \<And>Xa w I. \<lbrakk>0 \<notin> X; \<forall>(uu_, x)\<in>set x. x \<noteq> []; fin_cut_same (any, replicate (length I) False) (map \<pi> x) @ replicate m (any, replicate (length I) False) \<in> enc (w, I); n = length I; \<forall>a\<in>set w. a \<in> set \<Sigma>; Ball (set I) (case_sum (\<lambda>a. True) finite); \<forall>i\<in>(\<lambda>x. x - 1) ` X. case I ! i of Inl x \<Rightarrow> True | Inr x \<Rightarrow> False; \<forall>i\<in>{0..<length I} - (\<lambda>x. x - 1) ` X. case I ! i of Inl x \<Rightarrow> False | Inr x \<Rightarrow> True; fin_cut_same (any, replicate n False) (map \<pi> x) @ replicate m (any, replicate n False) \<in> \<Union> {enc (w, I) |w I. length I = n \<and> wf_interp w I \<and> (\<forall>i\<in>(\<lambda>x. x - 1) ` X. case I ! i of Inl x \<Rightarrow> True | Inr x \<Rightarrow> False) \<and> (\<forall>i\<in>{0..<n} - (\<lambda>x. x - 1) ` X. case I ! i of Inl x \<Rightarrow> False | Inr x \<Rightarrow> True)}; 0 \<notin> X; \<forall>(uu_, x)\<in>set x. x \<noteq> []\<rbrakk> \<Longrightarrow> fin_cut_same (any, replicate (length (?I26 Xa w I)) False) (map \<pi> x) @ replicate (?m26 Xa w I) (any, replicate (length (?I26 Xa w I)) False) \<in> enc (?w26 Xa w I, ?I26 Xa w I)
 8. \<And>Xa w I. \<lbrakk>0 \<notin> X; \<forall>(uu_, x)\<in>set x. x \<noteq> []; fin_cut_same (any, replicate (length I) False) (map \<pi> x) @ replicate m (any, replicate (length I) False) \<in> enc (w, I); n = length I; \<forall>a\<in>set w. a \<in> set \<Sigma>; Ball (set I) (case_sum (\<lambda>a. True) finite); \<forall>i\<in>(\<lambda>x. x - 1) ` X. case I ! i of Inl x \<Rightarrow> True | Inr x \<Rightarrow> False; \<forall>i\<in>{0..<length I} - (\<lambda>x. x - 1) ` X. case I ! i of Inl x \<Rightarrow> False | Inr x \<Rightarrow> True; fin_cut_same (any, replicate n False) (map \<pi> x) @ replicate m (any, replicate n False) \<in> \<Union> {enc (w, I) |w I. length I = n \<and> wf_interp w I \<and> (\<forall>i\<in>(\<lambda>x. x - 1) ` X. case I ! i of Inl x \<Rightarrow> True | Inr x \<Rightarrow> False) \<and> (\<forall>i\<in>{0..<n} - (\<lambda>x. x - 1) ` X. case I ! i of Inl x \<Rightarrow> False | Inr x \<Rightarrow> True)}; 0 \<notin> X; \<forall>(uu_, x)\<in>set x. x \<noteq> []\<rbrakk> \<Longrightarrow> \<forall>(uu_, x)\<in>set x. x \<noteq> []
 9. \<And>Xa w I. \<lbrakk>0 \<notin> X; \<forall>(uu_, x)\<in>set x. x \<noteq> []; fin_cut_same (any, replicate (length I) False) (map \<pi> x) @ replicate m (any, replicate (length I) False) \<in> enc (w, I); n = length I; \<forall>a\<in>set w. a \<in> set \<Sigma>; Ball (set I) (case_sum (\<lambda>a. True) finite); \<forall>i\<in>(\<lambda>x. x - 1) ` X. case I ! i of Inl x \<Rightarrow> True | Inr x \<Rightarrow> False; \<forall>i\<in>{0..<length I} - (\<lambda>x. x - 1) ` X. case I ! i of Inl x \<Rightarrow> False | Inr x \<Rightarrow> True; fin_cut_same (any, replicate n False) (map \<pi> x) @ replicate m (any, replicate n False) \<in> \<Union> {enc (w, I) |w I. length I = n \<and> wf_interp w I \<and> (\<forall>i\<in>(\<lambda>x. x - 1) ` X. case I ! i of Inl x \<Rightarrow> True | Inr x \<Rightarrow> False) \<and> (\<forall>i\<in>{0..<n} - (\<lambda>x. x - 1) ` X. case I ! i of Inl x \<Rightarrow> False | Inr x \<Rightarrow> True)}; 0 \<notin> X; \<forall>(uu_, x)\<in>set x. x \<noteq> []\<rbrakk> \<Longrightarrow> \<forall>a\<in>set (?w26 Xa w I). a \<in> set \<Sigma>
 10. \<And>Xa w I. \<lbrakk>0 \<notin> X; \<forall>(uu_, x)\<in>set x. x \<noteq> []; fin_cut_same (any, replicate (length I) False) (map \<pi> x) @ replicate m (any, replicate (length I) False) \<in> enc (w, I); n = length I; \<forall>a\<in>set w. a \<in> set \<Sigma>; Ball (set I) (case_sum (\<lambda>a. True) finite); \<forall>i\<in>(\<lambda>x. x - 1) ` X. case I ! i of Inl x \<Rightarrow> True | Inr x \<Rightarrow> False; \<forall>i\<in>{0..<length I} - (\<lambda>x. x - 1) ` X. case I ! i of Inl x \<Rightarrow> False | Inr x \<Rightarrow> True; fin_cut_same (any, replicate n False) (map \<pi> x) @ replicate m (any, replicate n False) \<in> \<Union> {enc (w, I) |w I. length I = n \<and> wf_interp w I \<and> (\<forall>i\<in>(\<lambda>x. x - 1) ` X. case I ! i of Inl x \<Rightarrow> True | Inr x \<Rightarrow> False) \<and> (\<forall>i\<in>{0..<n} - (\<lambda>x. x - 1) ` X. case I ! i of Inl x \<Rightarrow> False | Inr x \<Rightarrow> True)}; 0 \<notin> X; \<forall>(uu_, x)\<in>set x. x \<noteq> []\<rbrakk> \<Longrightarrow> \<forall>x\<in>set (?I26 Xa w I). case x of Inl a \<Rightarrow> True | Inr P \<Rightarrow> finite P
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Ball (set I) (case_sum (\<lambda>a. True) finite)
[PROOF STEP]
show "Ball (set
             (Inr (positions_in_row (x @- sconst (any, replicate (Suc (length I)) False)) 0) #I))
           (case_sum (\<lambda>a. True) finite)"
[PROOF STATE]
proof (prove)
using this:
Ball (set I) (case_sum (\<lambda>a. True) finite)

goal (1 subgoal):
 1. Ball (set (Inr (positions_in_row (x @- sconst (any, replicate (Suc (length I)) False)) 0) # I)) (case_sum (\<lambda>a. True) finite)
[PROOF STEP]
by (auto simp del: replicate_Suc)
[PROOF STATE]
proof (state)
this:
Ball (set (Inr (positions_in_row (x @- sconst (any, replicate (Suc (length I)) False)) 0) # I)) (case_sum (\<lambda>a. True) finite)

goal (9 subgoals):
 1. \<And>Xa w I. \<lbrakk>0 \<notin> X; \<forall>(uu_, x)\<in>set x. x \<noteq> []; fin_cut_same (any, replicate (length I) False) (map \<pi> x) @ replicate m (any, replicate (length I) False) \<in> enc (w, I); n = length I; \<forall>a\<in>set w. a \<in> set \<Sigma>; Ball (set I) (case_sum (\<lambda>a. True) finite); \<forall>i\<in>(\<lambda>x. x - 1) ` X. case I ! i of Inl x \<Rightarrow> True | Inr x \<Rightarrow> False; \<forall>i\<in>{0..<length I} - (\<lambda>x. x - 1) ` X. case I ! i of Inl x \<Rightarrow> False | Inr x \<Rightarrow> True; fin_cut_same (any, replicate n False) (map \<pi> x) @ replicate m (any, replicate n False) \<in> \<Union> {enc (w, I) |w I. length I = n \<and> wf_interp w I \<and> (\<forall>i\<in>(\<lambda>x. x - 1) ` X. case I ! i of Inl x \<Rightarrow> True | Inr x \<Rightarrow> False) \<and> (\<forall>i\<in>{0..<n} - (\<lambda>x. x - 1) ` X. case I ! i of Inl x \<Rightarrow> False | Inr x \<Rightarrow> True)}; 0 \<notin> X; \<forall>(uu_, x)\<in>set x. x \<noteq> []\<rbrakk> \<Longrightarrow> enc (?w26 Xa w I, Inr (positions_in_row (x @- sconst (any, replicate (Suc (length (?I26 Xa w I))) False)) 0) # ?I26 Xa w I) = enc (?w30 Xa w I, Inr (positions_in_row (x @- sconst (any, replicate (Suc (length I)) False)) 0) # I)
 2. \<And>Xa w I. \<lbrakk>0 \<notin> X; \<forall>(uu_, x)\<in>set x. x \<noteq> []; fin_cut_same (any, replicate (length I) False) (map \<pi> x) @ replicate m (any, replicate (length I) False) \<in> enc (w, I); n = length I; \<forall>a\<in>set w. a \<in> set \<Sigma>; Ball (set I) (case_sum (\<lambda>a. True) finite); \<forall>i\<in>(\<lambda>x. x - 1) ` X. case I ! i of Inl x \<Rightarrow> True | Inr x \<Rightarrow> False; \<forall>i\<in>{0..<length I} - (\<lambda>x. x - 1) ` X. case I ! i of Inl x \<Rightarrow> False | Inr x \<Rightarrow> True; fin_cut_same (any, replicate n False) (map \<pi> x) @ replicate m (any, replicate n False) \<in> \<Union> {enc (w, I) |w I. length I = n \<and> wf_interp w I \<and> (\<forall>i\<in>(\<lambda>x. x - 1) ` X. case I ! i of Inl x \<Rightarrow> True | Inr x \<Rightarrow> False) \<and> (\<forall>i\<in>{0..<n} - (\<lambda>x. x - 1) ` X. case I ! i of Inl x \<Rightarrow> False | Inr x \<Rightarrow> True)}; 0 \<notin> X; \<forall>(uu_, x)\<in>set x. x \<noteq> []\<rbrakk> \<Longrightarrow> length (Inr (positions_in_row (x @- sconst (any, replicate (Suc (length I)) False)) 0) # I) = length I + 1
 3. \<And>Xa w I. \<lbrakk>0 \<notin> X; \<forall>(uu_, x)\<in>set x. x \<noteq> []; fin_cut_same (any, replicate (length I) False) (map \<pi> x) @ replicate m (any, replicate (length I) False) \<in> enc (w, I); n = length I; \<forall>a\<in>set w. a \<in> set \<Sigma>; Ball (set I) (case_sum (\<lambda>a. True) finite); \<forall>i\<in>(\<lambda>x. x - 1) ` X. case I ! i of Inl x \<Rightarrow> True | Inr x \<Rightarrow> False; \<forall>i\<in>{0..<length I} - (\<lambda>x. x - 1) ` X. case I ! i of Inl x \<Rightarrow> False | Inr x \<Rightarrow> True; fin_cut_same (any, replicate n False) (map \<pi> x) @ replicate m (any, replicate n False) \<in> \<Union> {enc (w, I) |w I. length I = n \<and> wf_interp w I \<and> (\<forall>i\<in>(\<lambda>x. x - 1) ` X. case I ! i of Inl x \<Rightarrow> True | Inr x \<Rightarrow> False) \<and> (\<forall>i\<in>{0..<n} - (\<lambda>x. x - 1) ` X. case I ! i of Inl x \<Rightarrow> False | Inr x \<Rightarrow> True)}; 0 \<notin> X; \<forall>(uu_, x)\<in>set x. x \<noteq> []\<rbrakk> \<Longrightarrow> \<forall>a\<in>set (?w30 Xa w I). a \<in> set \<Sigma>
 4. \<And>Xa w I. \<lbrakk>0 \<notin> X; \<forall>(uu_, x)\<in>set x. x \<noteq> []; fin_cut_same (any, replicate (length I) False) (map \<pi> x) @ replicate m (any, replicate (length I) False) \<in> enc (w, I); n = length I; \<forall>a\<in>set w. a \<in> set \<Sigma>; Ball (set I) (case_sum (\<lambda>a. True) finite); \<forall>i\<in>(\<lambda>x. x - 1) ` X. case I ! i of Inl x \<Rightarrow> True | Inr x \<Rightarrow> False; \<forall>i\<in>{0..<length I} - (\<lambda>x. x - 1) ` X. case I ! i of Inl x \<Rightarrow> False | Inr x \<Rightarrow> True; fin_cut_same (any, replicate n False) (map \<pi> x) @ replicate m (any, replicate n False) \<in> \<Union> {enc (w, I) |w I. length I = n \<and> wf_interp w I \<and> (\<forall>i\<in>(\<lambda>x. x - 1) ` X. case I ! i of Inl x \<Rightarrow> True | Inr x \<Rightarrow> False) \<and> (\<forall>i\<in>{0..<n} - (\<lambda>x. x - 1) ` X. case I ! i of Inl x \<Rightarrow> False | Inr x \<Rightarrow> True)}; 0 \<notin> X; \<forall>(uu_, x)\<in>set x. x \<noteq> []\<rbrakk> \<Longrightarrow> \<forall>i\<in>X. case (Inr (positions_in_row (x @- sconst (any, replicate (Suc (length I)) False)) 0) # I) ! i of Inl x \<Rightarrow> True | Inr x \<Rightarrow> False
 5. \<And>Xa w I. \<lbrakk>0 \<notin> X; \<forall>(uu_, x)\<in>set x. x \<noteq> []; fin_cut_same (any, replicate (length I) False) (map \<pi> x) @ replicate m (any, replicate (length I) False) \<in> enc (w, I); n = length I; \<forall>a\<in>set w. a \<in> set \<Sigma>; Ball (set I) (case_sum (\<lambda>a. True) finite); \<forall>i\<in>(\<lambda>x. x - 1) ` X. case I ! i of Inl x \<Rightarrow> True | Inr x \<Rightarrow> False; \<forall>i\<in>{0..<length I} - (\<lambda>x. x - 1) ` X. case I ! i of Inl x \<Rightarrow> False | Inr x \<Rightarrow> True; fin_cut_same (any, replicate n False) (map \<pi> x) @ replicate m (any, replicate n False) \<in> \<Union> {enc (w, I) |w I. length I = n \<and> wf_interp w I \<and> (\<forall>i\<in>(\<lambda>x. x - 1) ` X. case I ! i of Inl x \<Rightarrow> True | Inr x \<Rightarrow> False) \<and> (\<forall>i\<in>{0..<n} - (\<lambda>x. x - 1) ` X. case I ! i of Inl x \<Rightarrow> False | Inr x \<Rightarrow> True)}; 0 \<notin> X; \<forall>(uu_, x)\<in>set x. x \<noteq> []\<rbrakk> \<Longrightarrow> \<forall>i\<in>{0..<length I + 1} - X. case (Inr (positions_in_row (x @- sconst (any, replicate (Suc (length I)) False)) 0) # I) ! i of Inl x \<Rightarrow> False | Inr x \<Rightarrow> True
 6. \<And>Xa w I. \<lbrakk>0 \<notin> X; \<forall>(uu_, x)\<in>set x. x \<noteq> []; fin_cut_same (any, replicate (length I) False) (map \<pi> x) @ replicate m (any, replicate (length I) False) \<in> enc (w, I); n = length I; \<forall>a\<in>set w. a \<in> set \<Sigma>; Ball (set I) (case_sum (\<lambda>a. True) finite); \<forall>i\<in>(\<lambda>x. x - 1) ` X. case I ! i of Inl x \<Rightarrow> True | Inr x \<Rightarrow> False; \<forall>i\<in>{0..<length I} - (\<lambda>x. x - 1) ` X. case I ! i of Inl x \<Rightarrow> False | Inr x \<Rightarrow> True; fin_cut_same (any, replicate n False) (map \<pi> x) @ replicate m (any, replicate n False) \<in> \<Union> {enc (w, I) |w I. length I = n \<and> wf_interp w I \<and> (\<forall>i\<in>(\<lambda>x. x - 1) ` X. case I ! i of Inl x \<Rightarrow> True | Inr x \<Rightarrow> False) \<and> (\<forall>i\<in>{0..<n} - (\<lambda>x. x - 1) ` X. case I ! i of Inl x \<Rightarrow> False | Inr x \<Rightarrow> True)}; 0 \<notin> X; \<forall>(uu_, x)\<in>set x. x \<noteq> []\<rbrakk> \<Longrightarrow> fin_cut_same (any, replicate (length (?I26 Xa w I)) False) (map \<pi> x) @ replicate (?m26 Xa w I) (any, replicate (length (?I26 Xa w I)) False) \<in> enc (?w26 Xa w I, ?I26 Xa w I)
 7. \<And>Xa w I. \<lbrakk>0 \<notin> X; \<forall>(uu_, x)\<in>set x. x \<noteq> []; fin_cut_same (any, replicate (length I) False) (map \<pi> x) @ replicate m (any, replicate (length I) False) \<in> enc (w, I); n = length I; \<forall>a\<in>set w. a \<in> set \<Sigma>; Ball (set I) (case_sum (\<lambda>a. True) finite); \<forall>i\<in>(\<lambda>x. x - 1) ` X. case I ! i of Inl x \<Rightarrow> True | Inr x \<Rightarrow> False; \<forall>i\<in>{0..<length I} - (\<lambda>x. x - 1) ` X. case I ! i of Inl x \<Rightarrow> False | Inr x \<Rightarrow> True; fin_cut_same (any, replicate n False) (map \<pi> x) @ replicate m (any, replicate n False) \<in> \<Union> {enc (w, I) |w I. length I = n \<and> wf_interp w I \<and> (\<forall>i\<in>(\<lambda>x. x - 1) ` X. case I ! i of Inl x \<Rightarrow> True | Inr x \<Rightarrow> False) \<and> (\<forall>i\<in>{0..<n} - (\<lambda>x. x - 1) ` X. case I ! i of Inl x \<Rightarrow> False | Inr x \<Rightarrow> True)}; 0 \<notin> X; \<forall>(uu_, x)\<in>set x. x \<noteq> []\<rbrakk> \<Longrightarrow> \<forall>(uu_, x)\<in>set x. x \<noteq> []
 8. \<And>Xa w I. \<lbrakk>0 \<notin> X; \<forall>(uu_, x)\<in>set x. x \<noteq> []; fin_cut_same (any, replicate (length I) False) (map \<pi> x) @ replicate m (any, replicate (length I) False) \<in> enc (w, I); n = length I; \<forall>a\<in>set w. a \<in> set \<Sigma>; Ball (set I) (case_sum (\<lambda>a. True) finite); \<forall>i\<in>(\<lambda>x. x - 1) ` X. case I ! i of Inl x \<Rightarrow> True | Inr x \<Rightarrow> False; \<forall>i\<in>{0..<length I} - (\<lambda>x. x - 1) ` X. case I ! i of Inl x \<Rightarrow> False | Inr x \<Rightarrow> True; fin_cut_same (any, replicate n False) (map \<pi> x) @ replicate m (any, replicate n False) \<in> \<Union> {enc (w, I) |w I. length I = n \<and> wf_interp w I \<and> (\<forall>i\<in>(\<lambda>x. x - 1) ` X. case I ! i of Inl x \<Rightarrow> True | Inr x \<Rightarrow> False) \<and> (\<forall>i\<in>{0..<n} - (\<lambda>x. x - 1) ` X. case I ! i of Inl x \<Rightarrow> False | Inr x \<Rightarrow> True)}; 0 \<notin> X; \<forall>(uu_, x)\<in>set x. x \<noteq> []\<rbrakk> \<Longrightarrow> \<forall>a\<in>set (?w26 Xa w I). a \<in> set \<Sigma>
 9. \<And>Xa w I. \<lbrakk>0 \<notin> X; \<forall>(uu_, x)\<in>set x. x \<noteq> []; fin_cut_same (any, replicate (length I) False) (map \<pi> x) @ replicate m (any, replicate (length I) False) \<in> enc (w, I); n = length I; \<forall>a\<in>set w. a \<in> set \<Sigma>; Ball (set I) (case_sum (\<lambda>a. True) finite); \<forall>i\<in>(\<lambda>x. x - 1) ` X. case I ! i of Inl x \<Rightarrow> True | Inr x \<Rightarrow> False; \<forall>i\<in>{0..<length I} - (\<lambda>x. x - 1) ` X. case I ! i of Inl x \<Rightarrow> False | Inr x \<Rightarrow> True; fin_cut_same (any, replicate n False) (map \<pi> x) @ replicate m (any, replicate n False) \<in> \<Union> {enc (w, I) |w I. length I = n \<and> wf_interp w I \<and> (\<forall>i\<in>(\<lambda>x. x - 1) ` X. case I ! i of Inl x \<Rightarrow> True | Inr x \<Rightarrow> False) \<and> (\<forall>i\<in>{0..<n} - (\<lambda>x. x - 1) ` X. case I ! i of Inl x \<Rightarrow> False | Inr x \<Rightarrow> True)}; 0 \<notin> X; \<forall>(uu_, x)\<in>set x. x \<noteq> []\<rbrakk> \<Longrightarrow> \<forall>x\<in>set (?I26 Xa w I). case x of Inl a \<Rightarrow> True | Inr P \<Rightarrow> finite P
[PROOF STEP]
qed (auto simp add: nth_Cons' Ball_def in_pred_image_iff)
[PROOF STATE]
proof (state)
this:
x \<in> lang (n + 1) (ENC (n + 1) X)

goal (1 subgoal):
 1. x \<in> Z
[PROOF STEP]
qed (rule \<open>x \<in> Z\<close>)
[PROOF STATE]
proof (state)
this:
map \<pi> x \<in> map \<pi> ` (Z \<inter> lang (n + 1) (ENC (n + 1) X))

goal (1 subgoal):
 1. \<And>x m xa. \<lbrakk>fin_cut_same (any, replicate n False) (map \<pi> xa) @ replicate m (any, replicate n False) \<in> lang n (ENC n ((\<lambda>x. x - 1) ` X)); w = fin_cut_same (any, replicate n False) (map \<pi> xa) @ replicate m (any, replicate n False); xa \<in> Z; w \<in> {fin_cut_same (any, replicate n False) x @ replicate m (any, replicate n False) |x m. x \<in> map \<pi> ` Z}; w \<in> lang n (ENC n ((\<lambda>x. x - 1) ` X))\<rbrakk> \<Longrightarrow> fin_cut_same (any, replicate n False) (map \<pi> xa) @ replicate m (any, replicate n False) = fin_cut_same (any, replicate n False) (map \<pi> xa) @ replicate (?m14 x m xa) (any, replicate n False)
[PROOF STEP]
qed (rule refl)
[PROOF STATE]
proof (state)
this:
w \<in> SAMEQUOT z (map \<pi> ` (Z \<inter> lang (n + 1) (ENC (n + 1) X)))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
SAMEQUOT z (map \<pi> ` (Z \<inter> lang (n + 1) (ENC (n + 1) X))) = SAMEQUOT z (map \<pi> ` Z) \<inter> lang n (ENC n ((\<lambda>x. x - 1) ` X))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma lang_ENC_split:
  assumes "finite X" "X = Y1 \<union> Y2" "n = 0 \<or> (\<forall>p \<in> X. p < n)"
  shows "lang n (ENC n X) = lang n (ENC n Y1) \<inter> lang n (ENC n Y2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lang n (ENC n X) = lang n (ENC n Y1) \<inter> lang n (ENC n Y2)
[PROOF STEP]
unfolding ENC_def lang_INTERSECT
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if sorted_list_of_set (valid_ENC n ` X) = [] then lists ((set \<circ> \<sigma> \<Sigma>) n) else \<Inter> (lang n ` set (sorted_list_of_set (valid_ENC n ` X)))) = (if sorted_list_of_set (valid_ENC n ` Y1) = [] then lists ((set \<circ> \<sigma> \<Sigma>) n) else \<Inter> (lang n ` set (sorted_list_of_set (valid_ENC n ` Y1)))) \<inter> (if sorted_list_of_set (valid_ENC n ` Y2) = [] then lists ((set \<circ> \<sigma> \<Sigma>) n) else \<Inter> (lang n ` set (sorted_list_of_set (valid_ENC n ` Y2))))
[PROOF STEP]
using assms lang_subset_lists[OF wf_rexp_valid_ENC, of n]
[PROOF STATE]
proof (prove)
using this:
finite X
X = Y1 \<union> Y2
n = 0 \<or> (\<forall>p\<in>X. p < n)
n = 0 \<or> ?p1 < n \<Longrightarrow> lang n (valid_ENC n ?p1) \<subseteq> lists ((set \<circ> \<sigma> \<Sigma>) n)

goal (1 subgoal):
 1. (if sorted_list_of_set (valid_ENC n ` X) = [] then lists ((set \<circ> \<sigma> \<Sigma>) n) else \<Inter> (lang n ` set (sorted_list_of_set (valid_ENC n ` X)))) = (if sorted_list_of_set (valid_ENC n ` Y1) = [] then lists ((set \<circ> \<sigma> \<Sigma>) n) else \<Inter> (lang n ` set (sorted_list_of_set (valid_ENC n ` Y1)))) \<inter> (if sorted_list_of_set (valid_ENC n ` Y2) = [] then lists ((set \<circ> \<sigma> \<Sigma>) n) else \<Inter> (lang n ` set (sorted_list_of_set (valid_ENC n ` Y2))))
[PROOF STEP]
by auto


[STATEMENT]
lemma map_project_ENC:
  fixes n
  assumes "X \<subseteq> {0 ..< n + 1}" "Z \<subseteq> lists ((set o \<sigma> \<Sigma>) (n + 1))"
  defines "z \<equiv> (any, replicate n False)"
  shows "SAMEQUOT z (map \<pi> ` (Z \<inter> lang (n + 1) (ENC (n + 1) X))) =
    (if 0 \<in> X
    then SAMEQUOT z (map \<pi> ` (Z \<inter> lang (n + 1) (ENC (n + 1) {0}))) \<inter> lang n (ENC n ((\<lambda>x. x - 1) ` (X - {0})))
    else SAMEQUOT z (map \<pi> ` Z) \<inter> lang n (ENC n ((\<lambda>x. x - 1) ` (X - {0}))))"
    (is "?L = (if _ then ?R1 else ?R2)")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. SAMEQUOT z (map \<pi> ` (Z \<inter> lang (n + 1) (ENC (n + 1) X))) = (if 0 \<in> X then SAMEQUOT z (map \<pi> ` (Z \<inter> lang (n + 1) (ENC (n + 1) {0}))) \<inter> lang n (ENC n ((\<lambda>x. x - 1) ` (X - {0}))) else SAMEQUOT z (map \<pi> ` Z) \<inter> lang n (ENC n ((\<lambda>x. x - 1) ` (X - {0}))))
[PROOF STEP]
proof (split if_splits, intro conjI impI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. 0 \<in> X \<Longrightarrow> SAMEQUOT z (map \<pi> ` (Z \<inter> lang (n + 1) (ENC (n + 1) X))) = SAMEQUOT z (map \<pi> ` (Z \<inter> lang (n + 1) (ENC (n + 1) {0}))) \<inter> lang n (ENC n ((\<lambda>x. x - 1) ` (X - {0})))
 2. 0 \<notin> X \<Longrightarrow> SAMEQUOT z (map \<pi> ` (Z \<inter> lang (n + 1) (ENC (n + 1) X))) = SAMEQUOT z (map \<pi> ` Z) \<inter> lang n (ENC n ((\<lambda>x. x - 1) ` (X - {0})))
[PROOF STEP]
assume 0: "0 \<notin> X"
[PROOF STATE]
proof (state)
this:
0 \<notin> X

goal (2 subgoals):
 1. 0 \<in> X \<Longrightarrow> SAMEQUOT z (map \<pi> ` (Z \<inter> lang (n + 1) (ENC (n + 1) X))) = SAMEQUOT z (map \<pi> ` (Z \<inter> lang (n + 1) (ENC (n + 1) {0}))) \<inter> lang n (ENC n ((\<lambda>x. x - 1) ` (X - {0})))
 2. 0 \<notin> X \<Longrightarrow> SAMEQUOT z (map \<pi> ` (Z \<inter> lang (n + 1) (ENC (n + 1) X))) = SAMEQUOT z (map \<pi> ` Z) \<inter> lang n (ENC n ((\<lambda>x. x - 1) ` (X - {0})))
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
X \<subseteq> {0..<n + 1}
Z \<subseteq> lists ((set \<circ> \<sigma> \<Sigma>) (n + 1))
z \<equiv> (any, replicate n False)
[PROOF STEP]
have fin: "finite X" "finite ((\<lambda>x. x - 1) ` X)"
[PROOF STATE]
proof (prove)
using this:
X \<subseteq> {0..<n + 1}
Z \<subseteq> lists ((set \<circ> \<sigma> \<Sigma>) (n + 1))
z \<equiv> (any, replicate n False)

goal (1 subgoal):
 1. finite X &&& finite ((\<lambda>x. x - 1) ` X)
[PROOF STEP]
by (auto elim: finite_subset intro!: finite_imageI[of "X"])
[PROOF STATE]
proof (state)
this:
finite X
finite ((\<lambda>x. x - 1) ` X)

goal (2 subgoals):
 1. 0 \<in> X \<Longrightarrow> SAMEQUOT z (map \<pi> ` (Z \<inter> lang (n + 1) (ENC (n + 1) X))) = SAMEQUOT z (map \<pi> ` (Z \<inter> lang (n + 1) (ENC (n + 1) {0}))) \<inter> lang n (ENC n ((\<lambda>x. x - 1) ` (X - {0})))
 2. 0 \<notin> X \<Longrightarrow> SAMEQUOT z (map \<pi> ` (Z \<inter> lang (n + 1) (ENC (n + 1) X))) = SAMEQUOT z (map \<pi> ` Z) \<inter> lang n (ENC n ((\<lambda>x. x - 1) ` (X - {0})))
[PROOF STEP]
from 0
[PROOF STATE]
proof (chain)
picking this:
0 \<notin> X
[PROOF STEP]
show "?L = ?R2"
[PROOF STATE]
proof (prove)
using this:
0 \<notin> X

goal (1 subgoal):
 1. SAMEQUOT z (map \<pi> ` (Z \<inter> lang (n + 1) (ENC (n + 1) X))) = SAMEQUOT z (map \<pi> ` Z) \<inter> lang n (ENC n ((\<lambda>x. x - 1) ` (X - {0})))
[PROOF STEP]
using map_project_Int_ENC[OF 0 assms(1,2)]
[PROOF STATE]
proof (prove)
using this:
0 \<notin> X
SAMEQUOT (any, replicate n False) (map \<pi> ` (Z \<inter> lang (n + 1) (ENC (n + 1) X))) = SAMEQUOT (any, replicate n False) (map \<pi> ` Z) \<inter> lang n (ENC n ((\<lambda>x. x - 1) ` X))

goal (1 subgoal):
 1. SAMEQUOT z (map \<pi> ` (Z \<inter> lang (n + 1) (ENC (n + 1) X))) = SAMEQUOT z (map \<pi> ` Z) \<inter> lang n (ENC n ((\<lambda>x. x - 1) ` (X - {0})))
[PROOF STEP]
unfolding lists_image[symmetric] \<pi>_\<sigma>
      Int_absorb1[OF lang_subset_lists[OF wf_rexp_ENC[OF fin(1)]], of "n + 1"]
      Int_absorb1[OF lang_subset_lists[OF wf_rexp_ENC[OF fin(2)]], of n]
[PROOF STATE]
proof (prove)
using this:
0 \<notin> X
SAMEQUOT (any, replicate n False) (map \<pi> ` (Z \<inter> lang (n + 1) (ENC (n + 1) X))) = SAMEQUOT (any, replicate n False) (map \<pi> ` Z) \<inter> lang n (ENC n ((\<lambda>x. x - 1) ` X))

goal (1 subgoal):
 1. SAMEQUOT z (map \<pi> ` (Z \<inter> lang (n + 1) (ENC (n + 1) X))) = SAMEQUOT z (map \<pi> ` Z) \<inter> lang n (ENC n ((\<lambda>x. x - 1) ` (X - {0})))
[PROOF STEP]
unfolding z_def
[PROOF STATE]
proof (prove)
using this:
0 \<notin> X
SAMEQUOT (any, replicate n False) (map \<pi> ` (Z \<inter> lang (n + 1) (ENC (n + 1) X))) = SAMEQUOT (any, replicate n False) (map \<pi> ` Z) \<inter> lang n (ENC n ((\<lambda>x. x - 1) ` X))

goal (1 subgoal):
 1. SAMEQUOT (any, replicate n False) (map \<pi> ` (Z \<inter> lang (n + 1) (ENC (n + 1) X))) = SAMEQUOT (any, replicate n False) (map \<pi> ` Z) \<inter> lang n (ENC n ((\<lambda>x. x - 1) ` (X - {0})))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
SAMEQUOT z (map \<pi> ` (Z \<inter> lang (n + 1) (ENC (n + 1) X))) = SAMEQUOT z (map \<pi> ` Z) \<inter> lang n (ENC n ((\<lambda>x. x - 1) ` (X - {0})))

goal (1 subgoal):
 1. 0 \<in> X \<Longrightarrow> SAMEQUOT z (map \<pi> ` (Z \<inter> lang (n + 1) (ENC (n + 1) X))) = SAMEQUOT z (map \<pi> ` (Z \<inter> lang (n + 1) (ENC (n + 1) {0}))) \<inter> lang n (ENC n ((\<lambda>x. x - 1) ` (X - {0})))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. 0 \<in> X \<Longrightarrow> SAMEQUOT z (map \<pi> ` (Z \<inter> lang (n + 1) (ENC (n + 1) X))) = SAMEQUOT z (map \<pi> ` (Z \<inter> lang (n + 1) (ENC (n + 1) {0}))) \<inter> lang n (ENC n ((\<lambda>x. x - 1) ` (X - {0})))
[PROOF STEP]
assume "0 \<in> X"
[PROOF STATE]
proof (state)
this:
0 \<in> X

goal (1 subgoal):
 1. 0 \<in> X \<Longrightarrow> SAMEQUOT z (map \<pi> ` (Z \<inter> lang (n + 1) (ENC (n + 1) X))) = SAMEQUOT z (map \<pi> ` (Z \<inter> lang (n + 1) (ENC (n + 1) {0}))) \<inter> lang n (ENC n ((\<lambda>x. x - 1) ` (X - {0})))
[PROOF STEP]
hence 0: "0 \<notin> X - {0}" and X: "X = {0} \<union> (X - {0})"
[PROOF STATE]
proof (prove)
using this:
0 \<in> X

goal (1 subgoal):
 1. 0 \<notin> X - {0} &&& X = {0} \<union> (X - {0})
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
0 \<notin> X - {0}
X = {0} \<union> (X - {0})

goal (1 subgoal):
 1. 0 \<in> X \<Longrightarrow> SAMEQUOT z (map \<pi> ` (Z \<inter> lang (n + 1) (ENC (n + 1) X))) = SAMEQUOT z (map \<pi> ` (Z \<inter> lang (n + 1) (ENC (n + 1) {0}))) \<inter> lang n (ENC n ((\<lambda>x. x - 1) ` (X - {0})))
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
X \<subseteq> {0..<n + 1}
Z \<subseteq> lists ((set \<circ> \<sigma> \<Sigma>) (n + 1))
z \<equiv> (any, replicate n False)
[PROOF STEP]
have fin: "finite X"
[PROOF STATE]
proof (prove)
using this:
X \<subseteq> {0..<n + 1}
Z \<subseteq> lists ((set \<circ> \<sigma> \<Sigma>) (n + 1))
z \<equiv> (any, replicate n False)

goal (1 subgoal):
 1. finite X
[PROOF STEP]
by (auto elim: finite_subset intro!: finite_imageI[of "X"])
[PROOF STATE]
proof (state)
this:
finite X

goal (1 subgoal):
 1. 0 \<in> X \<Longrightarrow> SAMEQUOT z (map \<pi> ` (Z \<inter> lang (n + 1) (ENC (n + 1) X))) = SAMEQUOT z (map \<pi> ` (Z \<inter> lang (n + 1) (ENC (n + 1) {0}))) \<inter> lang n (ENC n ((\<lambda>x. x - 1) ` (X - {0})))
[PROOF STEP]
have "?L = SAMEQUOT z (map \<pi> ` ((Z \<inter> lang (n + 1) (ENC (n + 1) {0})) \<inter> lang (n + 1) (ENC (n + 1) (X - {0}))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. SAMEQUOT z (map \<pi> ` (Z \<inter> lang (n + 1) (ENC (n + 1) X))) = SAMEQUOT z (map \<pi> ` (Z \<inter> lang (n + 1) (ENC (n + 1) {0}) \<inter> lang (n + 1) (ENC (n + 1) (X - {0}))))
[PROOF STEP]
unfolding Int_assoc z_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. SAMEQUOT (any, replicate n False) (map \<pi> ` (Z \<inter> lang (n + 1) (ENC (n + 1) X))) = SAMEQUOT (any, replicate n False) (map \<pi> ` (Z \<inter> (lang (n + 1) (ENC (n + 1) {0}) \<inter> lang (n + 1) (ENC (n + 1) (X - {0})))))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
X \<subseteq> {0..<n + 1}
Z \<subseteq> lists ((set \<circ> \<sigma> \<Sigma>) (n + 1))
z \<equiv> (any, replicate n False)

goal (1 subgoal):
 1. SAMEQUOT (any, replicate n False) (map \<pi> ` (Z \<inter> lang (n + 1) (ENC (n + 1) X))) = SAMEQUOT (any, replicate n False) (map \<pi> ` (Z \<inter> (lang (n + 1) (ENC (n + 1) {0}) \<inter> lang (n + 1) (ENC (n + 1) (X - {0})))))
[PROOF STEP]
by (subst lang_ENC_split[OF fin X, of "n + 1"]) auto
[PROOF STATE]
proof (state)
this:
SAMEQUOT z (map \<pi> ` (Z \<inter> lang (n + 1) (ENC (n + 1) X))) = SAMEQUOT z (map \<pi> ` (Z \<inter> lang (n + 1) (ENC (n + 1) {0}) \<inter> lang (n + 1) (ENC (n + 1) (X - {0}))))

goal (1 subgoal):
 1. 0 \<in> X \<Longrightarrow> SAMEQUOT z (map \<pi> ` (Z \<inter> lang (n + 1) (ENC (n + 1) X))) = SAMEQUOT z (map \<pi> ` (Z \<inter> lang (n + 1) (ENC (n + 1) {0}))) \<inter> lang n (ENC n ((\<lambda>x. x - 1) ` (X - {0})))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
SAMEQUOT z (map \<pi> ` (Z \<inter> lang (n + 1) (ENC (n + 1) X))) = SAMEQUOT z (map \<pi> ` (Z \<inter> lang (n + 1) (ENC (n + 1) {0}) \<inter> lang (n + 1) (ENC (n + 1) (X - {0}))))

goal (1 subgoal):
 1. 0 \<in> X \<Longrightarrow> SAMEQUOT z (map \<pi> ` (Z \<inter> lang (n + 1) (ENC (n + 1) X))) = SAMEQUOT z (map \<pi> ` (Z \<inter> lang (n + 1) (ENC (n + 1) {0}))) \<inter> lang n (ENC n ((\<lambda>x. x - 1) ` (X - {0})))
[PROOF STEP]
have "\<dots> = ?R1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. SAMEQUOT z (map \<pi> ` (Z \<inter> lang (n + 1) (ENC (n + 1) {0}) \<inter> lang (n + 1) (ENC (n + 1) (X - {0})))) = SAMEQUOT z (map \<pi> ` (Z \<inter> lang (n + 1) (ENC (n + 1) {0}))) \<inter> lang n (ENC n ((\<lambda>x. x - 1) ` (X - {0})))
[PROOF STEP]
unfolding z_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. SAMEQUOT (any, replicate n False) (map \<pi> ` (Z \<inter> lang (n + 1) (ENC (n + 1) {0}) \<inter> lang (n + 1) (ENC (n + 1) (X - {0})))) = SAMEQUOT (any, replicate n False) (map \<pi> ` (Z \<inter> lang (n + 1) (ENC (n + 1) {0}))) \<inter> lang n (ENC n ((\<lambda>x. x - 1) ` (X - {0})))
[PROOF STEP]
using assms(1,2)
[PROOF STATE]
proof (prove)
using this:
X \<subseteq> {0..<n + 1}
Z \<subseteq> lists ((set \<circ> \<sigma> \<Sigma>) (n + 1))

goal (1 subgoal):
 1. SAMEQUOT (any, replicate n False) (map \<pi> ` (Z \<inter> lang (n + 1) (ENC (n + 1) {0}) \<inter> lang (n + 1) (ENC (n + 1) (X - {0})))) = SAMEQUOT (any, replicate n False) (map \<pi> ` (Z \<inter> lang (n + 1) (ENC (n + 1) {0}))) \<inter> lang n (ENC n ((\<lambda>x. x - 1) ` (X - {0})))
[PROOF STEP]
by (intro map_project_Int_ENC) auto
[PROOF STATE]
proof (state)
this:
SAMEQUOT z (map \<pi> ` (Z \<inter> lang (n + 1) (ENC (n + 1) {0}) \<inter> lang (n + 1) (ENC (n + 1) (X - {0})))) = SAMEQUOT z (map \<pi> ` (Z \<inter> lang (n + 1) (ENC (n + 1) {0}))) \<inter> lang n (ENC n ((\<lambda>x. x - 1) ` (X - {0})))

goal (1 subgoal):
 1. 0 \<in> X \<Longrightarrow> SAMEQUOT z (map \<pi> ` (Z \<inter> lang (n + 1) (ENC (n + 1) X))) = SAMEQUOT z (map \<pi> ` (Z \<inter> lang (n + 1) (ENC (n + 1) {0}))) \<inter> lang n (ENC n ((\<lambda>x. x - 1) ` (X - {0})))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
SAMEQUOT z (map \<pi> ` (Z \<inter> lang (n + 1) (ENC (n + 1) X))) = SAMEQUOT z (map \<pi> ` (Z \<inter> lang (n + 1) (ENC (n + 1) {0}))) \<inter> lang n (ENC n ((\<lambda>x. x - 1) ` (X - {0})))
[PROOF STEP]
show "?L = ?R1"
[PROOF STATE]
proof (prove)
using this:
SAMEQUOT z (map \<pi> ` (Z \<inter> lang (n + 1) (ENC (n + 1) X))) = SAMEQUOT z (map \<pi> ` (Z \<inter> lang (n + 1) (ENC (n + 1) {0}))) \<inter> lang n (ENC n ((\<lambda>x. x - 1) ` (X - {0})))

goal (1 subgoal):
 1. SAMEQUOT z (map \<pi> ` (Z \<inter> lang (n + 1) (ENC (n + 1) X))) = SAMEQUOT z (map \<pi> ` (Z \<inter> lang (n + 1) (ENC (n + 1) {0}))) \<inter> lang n (ENC n ((\<lambda>x. x - 1) ` (X - {0})))
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
SAMEQUOT z (map \<pi> ` (Z \<inter> lang (n + 1) (ENC (n + 1) X))) = SAMEQUOT z (map \<pi> ` (Z \<inter> lang (n + 1) (ENC (n + 1) {0}))) \<inter> lang n (ENC n ((\<lambda>x. x - 1) ` (X - {0})))

goal:
No subgoals!
[PROOF STEP]
qed