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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

goal (1 subgoal):
 1. lang n (rexp.Inter (rexp_of_alt n (FExists \<phi>)) (ENC n (FOV (FExists \<phi>)))) = lang n (rexp.Inter (rexp_of_alt' n (FExists \<phi>)) (ENC n (FOV (FExists \<phi>))))
[PROOF STEP]
using max_idx_vars[of "n + 1" \<phi>] wf_rexp_of_alt'[OF wf]
[PROOF STATE]
proof (prove)
using this:
wf_formula (n + 1) \<phi>
0 \<in> FOV \<phi>
pre_wf_formula (n + 1) \<phi> \<Longrightarrow> \<forall>p\<in>FOV \<phi> \<union> SOV \<phi>. p < n + 1
local.wf (n + 1) (rexp_of_alt' (n + 1) \<phi>)

goal (1 subgoal):
 1. lang n (rexp.Inter (rexp_of_alt n (FExists \<phi>)) (ENC n (FOV (FExists \<phi>)))) = lang n (rexp.Inter (rexp_of_alt' n (FExists \<phi>)) (ENC n (FOV (FExists \<phi>))))
[PROOF STEP]
unfolding rexp_of_alt.simps rexp_of_alt'.simps lang.simps Suc_eq_plus1
[PROOF STATE]
proof (prove)
using this:
wf_formula (n + 1) \<phi>
0 \<in> FOV \<phi>
pre_wf_formula (n + 1) \<phi> \<Longrightarrow> \<forall>p\<in>FOV \<phi> \<union> SOV \<phi>. p < n + 1
local.wf (n + 1) (rexp_of_alt' (n + 1) \<phi>)

goal (1 subgoal):
 1. lang n (samequot_exec (any, replicate n False) (Pr (rexp.Inter (rexp_of_alt (n + 1) \<phi>) (ENC (n + 1) (FOV \<phi>))))) \<inter> lang n (ENC n (FOV (FExists \<phi>))) = lang n (samequot_exec (any, replicate n False) (Pr (rexp.Inter (rexp_of_alt' (n + 1) \<phi>) (ENC (n + 1) {0})))) \<inter> lang n (ENC n (FOV (FExists \<phi>)))
[PROOF STEP]
proof (subst (1 2) lang_samequot_exec)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<lbrakk>wf_formula (n + 1) \<phi>; 0 \<in> FOV \<phi>; pre_wf_formula (n + 1) \<phi> \<Longrightarrow> \<forall>p\<in>FOV \<phi> \<union> SOV \<phi>. p < n + 1; local.wf (n + 1) (rexp_of_alt' (n + 1) \<phi>)\<rbrakk> \<Longrightarrow> local.wf n (Pr (rexp.Inter (rexp_of_alt' (n + 1) \<phi>) (ENC (n + 1) {0})))
 2. \<lbrakk>wf_formula (n + 1) \<phi>; 0 \<in> FOV \<phi>; pre_wf_formula (n + 1) \<phi> \<Longrightarrow> \<forall>p\<in>FOV \<phi> \<union> SOV \<phi>. p < n + 1; local.wf (n + 1) (rexp_of_alt' (n + 1) \<phi>)\<rbrakk> \<Longrightarrow> (any, replicate n False) \<in> (set \<circ> \<sigma> \<Sigma>) n
 3. \<lbrakk>wf_formula (n + 1) \<phi>; 0 \<in> FOV \<phi>; pre_wf_formula (n + 1) \<phi> \<Longrightarrow> \<forall>p\<in>FOV \<phi> \<union> SOV \<phi>. p < n + 1; local.wf (n + 1) (rexp_of_alt' (n + 1) \<phi>)\<rbrakk> \<Longrightarrow> local.wf n (Pr (rexp.Inter (rexp_of_alt (n + 1) \<phi>) (ENC (n + 1) (FOV \<phi>))))
 4. \<lbrakk>wf_formula (n + 1) \<phi>; 0 \<in> FOV \<phi>; pre_wf_formula (n + 1) \<phi> \<Longrightarrow> \<forall>p\<in>FOV \<phi> \<union> SOV \<phi>. p < n + 1; local.wf (n + 1) (rexp_of_alt' (n + 1) \<phi>)\<rbrakk> \<Longrightarrow> SAMEQUOT (any, replicate n False) (lang n (Pr (rexp.Inter (rexp_of_alt (n + 1) \<phi>) (ENC (n + 1) (FOV \<phi>))))) \<inter> lang n (ENC n (FOV (FExists \<phi>))) = SAMEQUOT (any, replicate n False) (lang n (Pr (rexp.Inter (rexp_of_alt' (n + 1) \<phi>) (ENC (n + 1) {0})))) \<inter> lang n (ENC n (FOV (FExists \<phi>)))
[PROOF STEP]
show "SAMEQUOT (any, replicate n False)
          (lang n (Pr (Inter (rexp_of_alt (n + 1) \<phi>) (ENC (n + 1) (FOV \<phi>))))) \<inter>
          lang n (ENC n (FOV (FExists \<phi>))) =
        SAMEQUOT (any, replicate n False)
          (lang n (Pr (Inter (rexp_of_alt' (n + 1) \<phi>) (ENC (n + 1) {0})))) \<inter>
          lang n (ENC n (FOV (FExists \<phi>)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. SAMEQUOT (any, replicate n False) (lang n (Pr (rexp.Inter (rexp_of_alt (n + 1) \<phi>) (ENC (n + 1) (FOV \<phi>))))) \<inter> lang n (ENC n (FOV (FExists \<phi>))) = SAMEQUOT (any, replicate n False) (lang n (Pr (rexp.Inter (rexp_of_alt' (n + 1) \<phi>) (ENC (n + 1) {0})))) \<inter> lang n (ENC n (FOV (FExists \<phi>)))
[PROOF STEP]
using wf 0 max_idx_vars[of "n + 1" \<phi>] wf_rexp_of_alt'[OF wf]
[PROOF STATE]
proof (prove)
using this:
wf_formula (n + 1) \<phi>
0 \<in> FOV \<phi>
pre_wf_formula (n + 1) \<phi> \<Longrightarrow> \<forall>p\<in>FOV \<phi> \<union> SOV \<phi>. p < n + 1
local.wf (n + 1) (rexp_of_alt' (n + 1) \<phi>)

goal (1 subgoal):
 1. SAMEQUOT (any, replicate n False) (lang n (Pr (rexp.Inter (rexp_of_alt (n + 1) \<phi>) (ENC (n + 1) (FOV \<phi>))))) \<inter> lang n (ENC n (FOV (FExists \<phi>))) = SAMEQUOT (any, replicate n False) (lang n (Pr (rexp.Inter (rexp_of_alt' (n + 1) \<phi>) (ENC (n + 1) {0})))) \<inter> lang n (ENC n (FOV (FExists \<phi>)))
[PROOF STEP]
unfolding lang.simps FExists.IH[OF wf, unfolded lang.simps]
[PROOF STATE]
proof (prove)
using this:
wf_formula (n + 1) \<phi>
0 \<in> FOV \<phi>
pre_wf_formula (n + 1) \<phi> \<Longrightarrow> \<forall>p\<in>FOV \<phi> \<union> SOV \<phi>. p < n + 1
local.wf (n + 1) (rexp_of_alt' (n + 1) \<phi>)

goal (1 subgoal):
 1. SAMEQUOT (any, replicate n False) (map \<pi> ` (lang (n + 1) (rexp_of_alt' (n + 1) \<phi>) \<inter> lang (n + 1) (ENC (n + 1) (FOV \<phi>)))) \<inter> lang n (ENC n (FOV (FExists \<phi>))) = SAMEQUOT (any, replicate n False) (map \<pi> ` (lang (n + 1) (rexp_of_alt' (n + 1) \<phi>) \<inter> lang (n + 1) (ENC (n + 1) {0}))) \<inter> lang n (ENC n (FOV (FExists \<phi>)))
[PROOF STEP]
by (subst (1) map_project_ENC) (auto dest: subsetD[OF lang_subset_lists])
[PROOF STATE]
proof (state)
this:
SAMEQUOT (any, replicate n False) (lang n (Pr (rexp.Inter (rexp_of_alt (n + 1) \<phi>) (ENC (n + 1) (FOV \<phi>))))) \<inter> lang n (ENC n (FOV (FExists \<phi>))) = SAMEQUOT (any, replicate n False) (lang n (Pr (rexp.Inter (rexp_of_alt' (n + 1) \<phi>) (ENC (n + 1) {0})))) \<inter> lang n (ENC n (FOV (FExists \<phi>)))

goal (3 subgoals):
 1. \<lbrakk>wf_formula (n + 1) \<phi>; 0 \<in> FOV \<phi>; pre_wf_formula (n + 1) \<phi> \<Longrightarrow> \<forall>p\<in>FOV \<phi> \<union> SOV \<phi>. p < n + 1; local.wf (n + 1) (rexp_of_alt' (n + 1) \<phi>)\<rbrakk> \<Longrightarrow> local.wf n (Pr (rexp.Inter (rexp_of_alt' (n + 1) \<phi>) (ENC (n + 1) {0})))
 2. \<lbrakk>wf_formula (n + 1) \<phi>; 0 \<in> FOV \<phi>; pre_wf_formula (n + 1) \<phi> \<Longrightarrow> \<forall>p\<in>FOV \<phi> \<union> SOV \<phi>. p < n + 1; local.wf (n + 1) (rexp_of_alt' (n + 1) \<phi>)\<rbrakk> \<Longrightarrow> (any, replicate n False) \<in> (set \<circ> \<sigma> \<Sigma>) n
 3. \<lbrakk>wf_formula (n + 1) \<phi>; 0 \<in> FOV \<phi>; pre_wf_formula (n + 1) \<phi> \<Longrightarrow> \<forall>p\<in>FOV \<phi> \<union> SOV \<phi>. p < n + 1; local.wf (n + 1) (rexp_of_alt' (n + 1) \<phi>)\<rbrakk> \<Longrightarrow> local.wf n (Pr (rexp.Inter (rexp_of_alt (n + 1) \<phi>) (ENC (n + 1) (FOV \<phi>))))
[PROOF STEP]
qed (auto simp add: wf_rexp_of_alt finite_FOV wf_rexp_ENC)
[PROOF STATE]
proof (state)
this:
lang n (rexp.Inter (rexp_of_alt n (FExists \<phi>)) (ENC n (FOV (FExists \<phi>)))) = lang n (rexp.Inter (rexp_of_alt' n (FExists \<phi>)) (ENC n (FOV (FExists \<phi>))))

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

goal (4 subgoals):
 1. \<And>x1 x2 n. wf_formula n (FQ x1 x2) \<Longrightarrow> lang n (rexp.Inter (rexp_of_alt n (FQ x1 x2)) (ENC n (FOV (FQ x1 x2)))) = lang n (rexp.Inter (rexp_of_alt' n (FQ x1 x2)) (ENC n (FOV (FQ x1 x2))))
 2. \<And>x1 x2 n. wf_formula n (FLess x1 x2) \<Longrightarrow> lang n (rexp.Inter (rexp_of_alt n (FLess x1 x2)) (ENC n (FOV (FLess x1 x2)))) = lang n (rexp.Inter (rexp_of_alt' n (FLess x1 x2)) (ENC n (FOV (FLess x1 x2))))
 3. \<And>x1 x2 n. wf_formula n (FIn x1 x2) \<Longrightarrow> lang n (rexp.Inter (rexp_of_alt n (FIn x1 x2)) (ENC n (FOV (FIn x1 x2)))) = lang n (rexp.Inter (rexp_of_alt' n (FIn x1 x2)) (ENC n (FOV (FIn x1 x2))))
 4. \<And>\<phi> n. \<lbrakk>\<And>n. wf_formula n \<phi> \<Longrightarrow> lang n (rexp.Inter (rexp_of_alt n \<phi>) (ENC n (FOV \<phi>))) = lang n (rexp.Inter (rexp_of_alt' n \<phi>) (ENC n (FOV \<phi>))); wf_formula n (FEXISTS \<phi>)\<rbrakk> \<Longrightarrow> lang n (rexp.Inter (rexp_of_alt n (FEXISTS \<phi>)) (ENC n (FOV (FEXISTS \<phi>)))) = lang n (rexp.Inter (rexp_of_alt' n (FEXISTS \<phi>)) (ENC n (FOV (FEXISTS \<phi>))))
[PROOF STEP]
hence wf: "wf_formula (n + 1) \<phi>" and 0: "0 \<notin> FOV \<phi>"
[PROOF STATE]
proof (prove)
using this:
wf_formula ?n2 \<phi> \<Longrightarrow> lang ?n2 (rexp.Inter (rexp_of_alt ?n2 \<phi>) (ENC ?n2 (FOV \<phi>))) = lang ?n2 (rexp.Inter (rexp_of_alt' ?n2 \<phi>) (ENC ?n2 (FOV \<phi>)))
wf_formula n (FEXISTS \<phi>)

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

goal (4 subgoals):
 1. \<And>x1 x2 n. wf_formula n (FQ x1 x2) \<Longrightarrow> lang n (rexp.Inter (rexp_of_alt n (FQ x1 x2)) (ENC n (FOV (FQ x1 x2)))) = lang n (rexp.Inter (rexp_of_alt' n (FQ x1 x2)) (ENC n (FOV (FQ x1 x2))))
 2. \<And>x1 x2 n. wf_formula n (FLess x1 x2) \<Longrightarrow> lang n (rexp.Inter (rexp_of_alt n (FLess x1 x2)) (ENC n (FOV (FLess x1 x2)))) = lang n (rexp.Inter (rexp_of_alt' n (FLess x1 x2)) (ENC n (FOV (FLess x1 x2))))
 3. \<And>x1 x2 n. wf_formula n (FIn x1 x2) \<Longrightarrow> lang n (rexp.Inter (rexp_of_alt n (FIn x1 x2)) (ENC n (FOV (FIn x1 x2)))) = lang n (rexp.Inter (rexp_of_alt' n (FIn x1 x2)) (ENC n (FOV (FIn x1 x2))))
 4. \<And>\<phi> n. \<lbrakk>\<And>n. wf_formula n \<phi> \<Longrightarrow> lang n (rexp.Inter (rexp_of_alt n \<phi>) (ENC n (FOV \<phi>))) = lang n (rexp.Inter (rexp_of_alt' n \<phi>) (ENC n (FOV \<phi>))); wf_formula n (FEXISTS \<phi>)\<rbrakk> \<Longrightarrow> lang n (rexp.Inter (rexp_of_alt n (FEXISTS \<phi>)) (ENC n (FOV (FEXISTS \<phi>)))) = lang n (rexp.Inter (rexp_of_alt' n (FEXISTS \<phi>)) (ENC n (FOV (FEXISTS \<phi>))))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
wf_formula (n + 1) \<phi>
0 \<notin> FOV \<phi>
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
wf_formula (n + 1) \<phi>
0 \<notin> FOV \<phi>

goal (1 subgoal):
 1. lang n (rexp.Inter (rexp_of_alt n (FEXISTS \<phi>)) (ENC n (FOV (FEXISTS \<phi>)))) = lang n (rexp.Inter (rexp_of_alt' n (FEXISTS \<phi>)) (ENC n (FOV (FEXISTS \<phi>))))
[PROOF STEP]
using max_idx_vars[of "n + 1" \<phi>] wf_rexp_of_alt'[OF wf]
[PROOF STATE]
proof (prove)
using this:
wf_formula (n + 1) \<phi>
0 \<notin> FOV \<phi>
pre_wf_formula (n + 1) \<phi> \<Longrightarrow> \<forall>p\<in>FOV \<phi> \<union> SOV \<phi>. p < n + 1
local.wf (n + 1) (rexp_of_alt' (n + 1) \<phi>)

goal (1 subgoal):
 1. lang n (rexp.Inter (rexp_of_alt n (FEXISTS \<phi>)) (ENC n (FOV (FEXISTS \<phi>)))) = lang n (rexp.Inter (rexp_of_alt' n (FEXISTS \<phi>)) (ENC n (FOV (FEXISTS \<phi>))))
[PROOF STEP]
unfolding rexp_of_alt.simps rexp_of_alt'.simps lang.simps Suc_eq_plus1
[PROOF STATE]
proof (prove)
using this:
wf_formula (n + 1) \<phi>
0 \<notin> FOV \<phi>
pre_wf_formula (n + 1) \<phi> \<Longrightarrow> \<forall>p\<in>FOV \<phi> \<union> SOV \<phi>. p < n + 1
local.wf (n + 1) (rexp_of_alt' (n + 1) \<phi>)

goal (1 subgoal):
 1. lang n (samequot_exec (any, replicate n False) (Pr (rexp.Inter (rexp_of_alt (n + 1) \<phi>) (ENC (n + 1) (FOV \<phi>))))) \<inter> lang n (ENC n (FOV (FEXISTS \<phi>))) = lang n (samequot_exec (any, replicate n False) (Pr (rexp_of_alt' (n + 1) \<phi>))) \<inter> lang n (ENC n (FOV (FEXISTS \<phi>)))
[PROOF STEP]
proof (subst (1 2) lang_samequot_exec)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<lbrakk>wf_formula (n + 1) \<phi>; 0 \<notin> FOV \<phi>; pre_wf_formula (n + 1) \<phi> \<Longrightarrow> \<forall>p\<in>FOV \<phi> \<union> SOV \<phi>. p < n + 1; local.wf (n + 1) (rexp_of_alt' (n + 1) \<phi>)\<rbrakk> \<Longrightarrow> local.wf n (Pr (rexp_of_alt' (n + 1) \<phi>))
 2. \<lbrakk>wf_formula (n + 1) \<phi>; 0 \<notin> FOV \<phi>; pre_wf_formula (n + 1) \<phi> \<Longrightarrow> \<forall>p\<in>FOV \<phi> \<union> SOV \<phi>. p < n + 1; local.wf (n + 1) (rexp_of_alt' (n + 1) \<phi>)\<rbrakk> \<Longrightarrow> (any, replicate n False) \<in> (set \<circ> \<sigma> \<Sigma>) n
 3. \<lbrakk>wf_formula (n + 1) \<phi>; 0 \<notin> FOV \<phi>; pre_wf_formula (n + 1) \<phi> \<Longrightarrow> \<forall>p\<in>FOV \<phi> \<union> SOV \<phi>. p < n + 1; local.wf (n + 1) (rexp_of_alt' (n + 1) \<phi>)\<rbrakk> \<Longrightarrow> local.wf n (Pr (rexp.Inter (rexp_of_alt (n + 1) \<phi>) (ENC (n + 1) (FOV \<phi>))))
 4. \<lbrakk>wf_formula (n + 1) \<phi>; 0 \<notin> FOV \<phi>; pre_wf_formula (n + 1) \<phi> \<Longrightarrow> \<forall>p\<in>FOV \<phi> \<union> SOV \<phi>. p < n + 1; local.wf (n + 1) (rexp_of_alt' (n + 1) \<phi>)\<rbrakk> \<Longrightarrow> SAMEQUOT (any, replicate n False) (lang n (Pr (rexp.Inter (rexp_of_alt (n + 1) \<phi>) (ENC (n + 1) (FOV \<phi>))))) \<inter> lang n (ENC n (FOV (FEXISTS \<phi>))) = SAMEQUOT (any, replicate n False) (lang n (Pr (rexp_of_alt' (n + 1) \<phi>))) \<inter> lang n (ENC n (FOV (FEXISTS \<phi>)))
[PROOF STEP]
show "SAMEQUOT (any, replicate n False)
          (lang n (Pr (Inter (rexp_of_alt (n + 1) \<phi>) (ENC (n + 1) (FOV \<phi>))))) \<inter>
          lang n (ENC n (FOV (FEXISTS \<phi>))) =
        SAMEQUOT (any, replicate n False)
          (lang n (Pr (rexp_of_alt' (n + 1) \<phi>))) \<inter>
          lang n (ENC n (FOV (FEXISTS \<phi>)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. SAMEQUOT (any, replicate n False) (lang n (Pr (rexp.Inter (rexp_of_alt (n + 1) \<phi>) (ENC (n + 1) (FOV \<phi>))))) \<inter> lang n (ENC n (FOV (FEXISTS \<phi>))) = SAMEQUOT (any, replicate n False) (lang n (Pr (rexp_of_alt' (n + 1) \<phi>))) \<inter> lang n (ENC n (FOV (FEXISTS \<phi>)))
[PROOF STEP]
using wf 0 max_idx_vars[of "n + 1" \<phi>] wf_rexp_of_alt'[OF wf]
[PROOF STATE]
proof (prove)
using this:
wf_formula (n + 1) \<phi>
0 \<notin> FOV \<phi>
pre_wf_formula (n + 1) \<phi> \<Longrightarrow> \<forall>p\<in>FOV \<phi> \<union> SOV \<phi>. p < n + 1
local.wf (n + 1) (rexp_of_alt' (n + 1) \<phi>)

goal (1 subgoal):
 1. SAMEQUOT (any, replicate n False) (lang n (Pr (rexp.Inter (rexp_of_alt (n + 1) \<phi>) (ENC (n + 1) (FOV \<phi>))))) \<inter> lang n (ENC n (FOV (FEXISTS \<phi>))) = SAMEQUOT (any, replicate n False) (lang n (Pr (rexp_of_alt' (n + 1) \<phi>))) \<inter> lang n (ENC n (FOV (FEXISTS \<phi>)))
[PROOF STEP]
unfolding lang.simps FEXISTS.IH[OF wf, unfolded lang.simps]
[PROOF STATE]
proof (prove)
using this:
wf_formula (n + 1) \<phi>
0 \<notin> FOV \<phi>
pre_wf_formula (n + 1) \<phi> \<Longrightarrow> \<forall>p\<in>FOV \<phi> \<union> SOV \<phi>. p < n + 1
local.wf (n + 1) (rexp_of_alt' (n + 1) \<phi>)

goal (1 subgoal):
 1. SAMEQUOT (any, replicate n False) (map \<pi> ` (lang (n + 1) (rexp_of_alt' (n + 1) \<phi>) \<inter> lang (n + 1) (ENC (n + 1) (FOV \<phi>)))) \<inter> lang n (ENC n (FOV (FEXISTS \<phi>))) = SAMEQUOT (any, replicate n False) (map \<pi> ` lang (n + 1) (rexp_of_alt' (n + 1) \<phi>)) \<inter> lang n (ENC n (FOV (FEXISTS \<phi>)))
[PROOF STEP]
by (subst (1) map_project_ENC) (auto dest: subsetD[OF lang_subset_lists])
[PROOF STATE]
proof (state)
this:
SAMEQUOT (any, replicate n False) (lang n (Pr (rexp.Inter (rexp_of_alt (n + 1) \<phi>) (ENC (n + 1) (FOV \<phi>))))) \<inter> lang n (ENC n (FOV (FEXISTS \<phi>))) = SAMEQUOT (any, replicate n False) (lang n (Pr (rexp_of_alt' (n + 1) \<phi>))) \<inter> lang n (ENC n (FOV (FEXISTS \<phi>)))

goal (3 subgoals):
 1. \<lbrakk>wf_formula (n + 1) \<phi>; 0 \<notin> FOV \<phi>; pre_wf_formula (n + 1) \<phi> \<Longrightarrow> \<forall>p\<in>FOV \<phi> \<union> SOV \<phi>. p < n + 1; local.wf (n + 1) (rexp_of_alt' (n + 1) \<phi>)\<rbrakk> \<Longrightarrow> local.wf n (Pr (rexp_of_alt' (n + 1) \<phi>))
 2. \<lbrakk>wf_formula (n + 1) \<phi>; 0 \<notin> FOV \<phi>; pre_wf_formula (n + 1) \<phi> \<Longrightarrow> \<forall>p\<in>FOV \<phi> \<union> SOV \<phi>. p < n + 1; local.wf (n + 1) (rexp_of_alt' (n + 1) \<phi>)\<rbrakk> \<Longrightarrow> (any, replicate n False) \<in> (set \<circ> \<sigma> \<Sigma>) n
 3. \<lbrakk>wf_formula (n + 1) \<phi>; 0 \<notin> FOV \<phi>; pre_wf_formula (n + 1) \<phi> \<Longrightarrow> \<forall>p\<in>FOV \<phi> \<union> SOV \<phi>. p < n + 1; local.wf (n + 1) (rexp_of_alt' (n + 1) \<phi>)\<rbrakk> \<Longrightarrow> local.wf n (Pr (rexp.Inter (rexp_of_alt (n + 1) \<phi>) (ENC (n + 1) (FOV \<phi>))))
[PROOF STEP]
qed (auto simp add: wf_rexp_of_alt finite_FOV wf_rexp_ENC)
[PROOF STATE]
proof (state)
this:
lang n (rexp.Inter (rexp_of_alt n (FEXISTS \<phi>)) (ENC n (FOV (FEXISTS \<phi>)))) = lang n (rexp.Inter (rexp_of_alt' n (FEXISTS \<phi>)) (ENC n (FOV (FEXISTS \<phi>))))

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


[STATEMENT]
theorem lang\<^sub>W\<^sub>S\<^sub>1\<^sub>S_rexp_of': "wf_formula n \<phi> \<Longrightarrow> lang\<^sub>W\<^sub>S\<^sub>1\<^sub>S n \<phi> = lang n (rexp_of' n \<phi>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf_formula n \<phi> \<Longrightarrow> lang\<^sub>W\<^sub>S\<^sub>1\<^sub>S n \<phi> = lang n (rexp_of' n \<phi>)
[PROOF STEP]
unfolding lang\<^sub>W\<^sub>S\<^sub>1\<^sub>S_rexp_of_rexp_of'[symmetric]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf_formula n \<phi> \<Longrightarrow> lang\<^sub>W\<^sub>S\<^sub>1\<^sub>S n \<phi> = lang n (rexp_of n \<phi>)
[PROOF STEP]
by (rule lang\<^sub>W\<^sub>S\<^sub>1\<^sub>S_rexp_of)


[STATEMENT]
theorem lang\<^sub>W\<^sub>S\<^sub>1\<^sub>S_rexp_of'': "wf_formula n \<phi> \<Longrightarrow> lang\<^sub>W\<^sub>S\<^sub>1\<^sub>S n \<phi> = lang n (rexp_of'' n \<phi>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf_formula n \<phi> \<Longrightarrow> lang\<^sub>W\<^sub>S\<^sub>1\<^sub>S n \<phi> = lang n (rexp_of'' n \<phi>)
[PROOF STEP]
unfolding lang\<^sub>M\<^sub>2\<^sub>L_rexp_of'_rexp_of''[symmetric]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf_formula n \<phi> \<Longrightarrow> lang\<^sub>W\<^sub>S\<^sub>1\<^sub>S n \<phi> = lang n (rexp_of' n \<phi>)
[PROOF STEP]
by (rule lang\<^sub>W\<^sub>S\<^sub>1\<^sub>S_rexp_of')


[STATEMENT]
lemma ssubsetI:
  assumes "\<And>\<pi> h. (\<pi>, h) \<in> A \<Longrightarrow> (\<pi>, h) \<in> B"
  shows "A \<subseteq> B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<subseteq> B
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
(?\<pi>, ?h) \<in> A \<Longrightarrow> (?\<pi>, ?h) \<in> B

goal (1 subgoal):
 1. A \<subseteq> B
[PROOF STEP]
by auto


[STATEMENT]
lemma double_inclusion:
  assumes "A \<subseteq> B"
      and "B \<subseteq> A"
    shows "A = B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A = B
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
A \<subseteq> B
B \<subseteq> A

goal (1 subgoal):
 1. A = B
[PROOF STEP]
by blast


[STATEMENT]
lemma add_masks_comm:
  "add_masks a b = add_masks b a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. add_masks a b = add_masks b a
[PROOF STEP]
proof (rule ext)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. add_masks a b x = add_masks b a x
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. add_masks a b x = add_masks b a x
[PROOF STEP]
show "add_masks a b x = add_masks b a x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. add_masks a b x = add_masks b a x
[PROOF STEP]
by (metis Rep_prat_inverse add.commute add_masks.simps padd.rep_eq)
[PROOF STATE]
proof (state)
this:
add_masks a b x = add_masks b a x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma add_masks_asso:
  "add_masks (add_masks a b) c = add_masks a (add_masks b c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. add_masks (add_masks a b) c = add_masks a (add_masks b c)
[PROOF STEP]
proof (rule ext)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. add_masks (add_masks a b) c x = add_masks a (add_masks b c) x
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. add_masks (add_masks a b) c x = add_masks a (add_masks b c) x
[PROOF STEP]
show "add_masks (add_masks a b) c x = add_masks a (add_masks b c) x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. add_masks (add_masks a b) c x = add_masks a (add_masks b c) x
[PROOF STEP]
by (metis Rep_prat_inverse add.assoc add_masks.simps padd.rep_eq)
[PROOF STATE]
proof (state)
this:
add_masks (add_masks a b) c x = add_masks a (add_masks b c) x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma minus_empty:
  "\<pi> = add_masks \<pi> empty_mask"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pi> = add_masks \<pi> empty_mask
[PROOF STEP]
proof (rule ext)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<pi> x = add_masks \<pi> empty_mask x
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<pi> x = add_masks \<pi> empty_mask x
[PROOF STEP]
show "\<pi> x = add_masks \<pi> empty_mask x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pi> x = add_masks \<pi> empty_mask x
[PROOF STEP]
by (metis Rep_prat_inverse add.right_neutral add_masks.simps empty_mask.simps padd.rep_eq pnone.rep_eq)
[PROOF STATE]
proof (state)
this:
\<pi> x = add_masks \<pi> empty_mask x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma add_acc_uni_mask:
  "add_acc \<pi> hl p = add_masks \<pi> (uni_mask hl p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. add_acc \<pi> hl p = add_masks \<pi> (uni_mask hl p)
[PROOF STEP]
proof (rule ext)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. add_acc \<pi> hl p x = add_masks \<pi> (uni_mask hl p) x
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. add_acc \<pi> hl p x = add_masks \<pi> (uni_mask hl p) x
[PROOF STEP]
show "add_acc \<pi> hl p x = add_masks \<pi> (uni_mask hl p) x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. add_acc \<pi> hl p x = add_masks \<pi> (uni_mask hl p) x
[PROOF STEP]
by (metis (no_types, opaque_lifting) add_acc.simps add_masks.simps fun_upd_apply minus_empty uni_mask.simps)
[PROOF STATE]
proof (state)
this:
add_acc \<pi> hl p x = add_masks \<pi> (uni_mask hl p) x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma add_masks_equiv_valid_null:
  "valid_null (add_masks a b) \<longleftrightarrow> valid_null a \<and> valid_null b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. valid_null (add_masks a b) = (valid_null a \<and> valid_null b)
[PROOF STEP]
by (metis (mono_tags, lifting) add_masks.simps padd_zero valid_null_def)


[STATEMENT]
lemma valid_maskI:
  assumes "\<And>hl. pgte pwrite (\<pi> hl)"
      and "\<And>f. \<pi> (null, f) = pnone"
    shows "valid_mask \<pi>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. valid_mask \<pi>
[PROOF STEP]
by (simp add: assms(1) assms(2))


[STATEMENT]
lemma greater_mask_equiv_def:
  "greater_mask \<pi>' \<pi> \<longleftrightarrow> (\<forall>hl. pgte (\<pi>' hl) (\<pi> hl))"
  (is "?A \<longleftrightarrow> ?B")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. greater_mask \<pi>' \<pi> = (\<forall>hl. pgte (\<pi>' hl) (\<pi> hl))
[PROOF STEP]
proof (rule iffI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. greater_mask \<pi>' \<pi> \<Longrightarrow> \<forall>hl. pgte (\<pi>' hl) (\<pi> hl)
 2. \<forall>hl. pgte (\<pi>' hl) (\<pi> hl) \<Longrightarrow> greater_mask \<pi>' \<pi>
[PROOF STEP]
show "?A \<Longrightarrow> ?B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. greater_mask \<pi>' \<pi> \<Longrightarrow> \<forall>hl. pgte (\<pi>' hl) (\<pi> hl)
[PROOF STEP]
proof (clarify)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>hl. greater_mask \<pi>' \<pi> \<Longrightarrow> pgte (\<pi>' hl) (\<pi> hl)
[PROOF STEP]
fix hl
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>hl. greater_mask \<pi>' \<pi> \<Longrightarrow> pgte (\<pi>' hl) (\<pi> hl)
[PROOF STEP]
assume "greater_mask \<pi>' \<pi>"
[PROOF STATE]
proof (state)
this:
greater_mask \<pi>' \<pi>

goal (1 subgoal):
 1. \<And>hl. greater_mask \<pi>' \<pi> \<Longrightarrow> pgte (\<pi>' hl) (\<pi> hl)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
greater_mask \<pi>' \<pi>
[PROOF STEP]
obtain r where "\<pi>' = add_masks \<pi> r"
[PROOF STATE]
proof (prove)
using this:
greater_mask \<pi>' \<pi>

goal (1 subgoal):
 1. (\<And>r. \<pi>' = add_masks \<pi> r \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using greater_mask_def
[PROOF STATE]
proof (prove)
using this:
greater_mask \<pi>' \<pi>
greater_mask ?\<pi>' ?\<pi> = (\<exists>r. ?\<pi>' = add_masks ?\<pi> r)

goal (1 subgoal):
 1. (\<And>r. \<pi>' = add_masks \<pi> r \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<pi>' = add_masks \<pi> r

goal (1 subgoal):
 1. \<And>hl. greater_mask \<pi>' \<pi> \<Longrightarrow> pgte (\<pi>' hl) (\<pi> hl)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<pi>' = add_masks \<pi> r
[PROOF STEP]
show "pgte (\<pi>' hl) (\<pi> hl)"
[PROOF STATE]
proof (prove)
using this:
\<pi>' = add_masks \<pi> r

goal (1 subgoal):
 1. pgte (\<pi>' hl) (\<pi> hl)
[PROOF STEP]
using Rep_prat padd.rep_eq pgte.rep_eq
[PROOF STATE]
proof (prove)
using this:
\<pi>' = add_masks \<pi> r
Rep_prat ?x \<in> {r |r. 0 \<le> r}
Rep_prat (padd ?x ?xa) = Rep_prat ?x + Rep_prat ?xa
pgte ?x ?xa = (Rep_prat ?xa \<le> Rep_prat ?x)

goal (1 subgoal):
 1. pgte (\<pi>' hl) (\<pi> hl)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
pgte (\<pi>' hl) (\<pi> hl)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
greater_mask \<pi>' \<pi> \<Longrightarrow> \<forall>hl. pgte (\<pi>' hl) (\<pi> hl)

goal (1 subgoal):
 1. \<forall>hl. pgte (\<pi>' hl) (\<pi> hl) \<Longrightarrow> greater_mask \<pi>' \<pi>
[PROOF STEP]
show "?B \<Longrightarrow> ?A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>hl. pgte (\<pi>' hl) (\<pi> hl) \<Longrightarrow> greater_mask \<pi>' \<pi>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>hl. pgte (\<pi>' hl) (\<pi> hl) \<Longrightarrow> greater_mask \<pi>' \<pi>
[PROOF STEP]
assume ?B
[PROOF STATE]
proof (state)
this:
\<forall>hl. pgte (\<pi>' hl) (\<pi> hl)

goal (1 subgoal):
 1. \<forall>hl. pgte (\<pi>' hl) (\<pi> hl) \<Longrightarrow> greater_mask \<pi>' \<pi>
[PROOF STEP]
let ?r = "\<lambda>hl. (SOME p. \<pi>' hl = padd (\<pi> hl) p)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>hl. pgte (\<pi>' hl) (\<pi> hl) \<Longrightarrow> greater_mask \<pi>' \<pi>
[PROOF STEP]
have "\<pi>' = add_masks \<pi> ?r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pi>' = add_masks \<pi> (\<lambda>hl. SOME p. \<pi>' hl = padd (\<pi> hl) p)
[PROOF STEP]
proof (rule ext)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<pi>' x = add_masks \<pi> (\<lambda>hl. SOME p. \<pi>' hl = padd (\<pi> hl) p) x
[PROOF STEP]
fix hl
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<pi>' x = add_masks \<pi> (\<lambda>hl. SOME p. \<pi>' hl = padd (\<pi> hl) p) x
[PROOF STEP]
have "\<pi>' hl = padd (\<pi> hl) (?r hl)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pi>' hl = padd (\<pi> hl) (SOME p. \<pi>' hl = padd (\<pi> hl) p)
[PROOF STEP]
by (meson \<open>\<forall>hl. pgte (\<pi>' hl) (\<pi> hl)\<close> p_greater_exists someI_ex)
[PROOF STATE]
proof (state)
this:
\<pi>' hl = padd (\<pi> hl) (SOME p. \<pi>' hl = padd (\<pi> hl) p)

goal (1 subgoal):
 1. \<And>x. \<pi>' x = add_masks \<pi> (\<lambda>hl. SOME p. \<pi>' hl = padd (\<pi> hl) p) x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<pi>' hl = padd (\<pi> hl) (SOME p. \<pi>' hl = padd (\<pi> hl) p)
[PROOF STEP]
show "\<pi>' hl = add_masks \<pi> ?r hl"
[PROOF STATE]
proof (prove)
using this:
\<pi>' hl = padd (\<pi> hl) (SOME p. \<pi>' hl = padd (\<pi> hl) p)

goal (1 subgoal):
 1. \<pi>' hl = add_masks \<pi> (\<lambda>hl. SOME p. \<pi>' hl = padd (\<pi> hl) p) hl
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<pi>' hl = add_masks \<pi> (\<lambda>hl. SOME p. \<pi>' hl = padd (\<pi> hl) p) hl

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<pi>' = add_masks \<pi> (\<lambda>hl. SOME p. \<pi>' hl = padd (\<pi> hl) p)

goal (1 subgoal):
 1. \<forall>hl. pgte (\<pi>' hl) (\<pi> hl) \<Longrightarrow> greater_mask \<pi>' \<pi>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<pi>' = add_masks \<pi> (\<lambda>hl. SOME p. \<pi>' hl = padd (\<pi> hl) p)
[PROOF STEP]
show ?A
[PROOF STATE]
proof (prove)
using this:
\<pi>' = add_masks \<pi> (\<lambda>hl. SOME p. \<pi>' hl = padd (\<pi> hl) p)

goal (1 subgoal):
 1. greater_mask \<pi>' \<pi>
[PROOF STEP]
using greater_mask_def
[PROOF STATE]
proof (prove)
using this:
\<pi>' = add_masks \<pi> (\<lambda>hl. SOME p. \<pi>' hl = padd (\<pi> hl) p)
greater_mask ?\<pi>' ?\<pi> = (\<exists>r. ?\<pi>' = add_masks ?\<pi> r)

goal (1 subgoal):
 1. greater_mask \<pi>' \<pi>
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
greater_mask \<pi>' \<pi>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>hl. pgte (\<pi>' hl) (\<pi> hl) \<Longrightarrow> greater_mask \<pi>' \<pi>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma greater_maskI:
  assumes "\<And>hl. pgte (\<pi>' hl) (\<pi> hl)"
  shows "greater_mask \<pi>' \<pi>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. greater_mask \<pi>' \<pi>
[PROOF STEP]
by (simp add: assms greater_mask_equiv_def)


[STATEMENT]
lemma greater_mask_properties:
  "greater_mask \<pi> \<pi>"
  "greater_mask a b \<and> greater_mask b c \<Longrightarrow> greater_mask a c"
  "greater_mask \<pi>' \<pi> \<and> greater_mask \<pi> \<pi>' \<Longrightarrow> \<pi> = \<pi>'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. greater_mask \<pi> \<pi> &&& (greater_mask a b \<and> greater_mask b c \<Longrightarrow> greater_mask a c) &&& (greater_mask \<pi>' \<pi> \<and> greater_mask \<pi> \<pi>' \<Longrightarrow> \<pi> = \<pi>')
[PROOF STEP]
apply (simp add: greater_maskI pgte.rep_eq)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. greater_mask a b \<and> greater_mask b c \<Longrightarrow> greater_mask a c
 2. greater_mask \<pi>' \<pi> \<and> greater_mask \<pi> \<pi>' \<Longrightarrow> \<pi> = \<pi>'
[PROOF STEP]
apply (metis add_masks_asso greater_mask_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. greater_mask \<pi>' \<pi> \<and> greater_mask \<pi> \<pi>' \<Longrightarrow> \<pi> = \<pi>'
[PROOF STEP]
proof (rule ext)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. greater_mask \<pi>' \<pi> \<and> greater_mask \<pi> \<pi>' \<Longrightarrow> \<pi> x = \<pi>' x
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. greater_mask \<pi>' \<pi> \<and> greater_mask \<pi> \<pi>' \<Longrightarrow> \<pi> x = \<pi>' x
[PROOF STEP]
assume "greater_mask \<pi>' \<pi> \<and> greater_mask \<pi> \<pi>'"
[PROOF STATE]
proof (state)
this:
greater_mask \<pi>' \<pi> \<and> greater_mask \<pi> \<pi>'

goal (1 subgoal):
 1. \<And>x. greater_mask \<pi>' \<pi> \<and> greater_mask \<pi> \<pi>' \<Longrightarrow> \<pi> x = \<pi>' x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
greater_mask \<pi>' \<pi> \<and> greater_mask \<pi> \<pi>'
[PROOF STEP]
show "\<pi> x = \<pi>' x"
[PROOF STATE]
proof (prove)
using this:
greater_mask \<pi>' \<pi> \<and> greater_mask \<pi> \<pi>'

goal (1 subgoal):
 1. \<pi> x = \<pi>' x
[PROOF STEP]
by (meson greater_mask_equiv_def pgte_antisym)
[PROOF STATE]
proof (state)
this:
\<pi> x = \<pi>' x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma greater_mask_decomp:
  assumes "greater_mask a (add_masks b c)"
  shows "\<exists>a1 a2. a = add_masks a1 a2 \<and> greater_mask a1 b \<and> greater_mask a2 c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>a1 a2. a = add_masks a1 a2 \<and> greater_mask a1 b \<and> greater_mask a2 c
[PROOF STEP]
by (metis add_masks_asso assms greater_mask_def greater_mask_properties(1))


[STATEMENT]
lemma upper_valid_aux:
  assumes "valid_mask a"
      and "a = add_masks b c"
    shows "valid_mask b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. valid_mask b
[PROOF STEP]
proof (rule valid_maskI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>hl. pgte pwrite (b hl)
 2. \<And>f. b (null, f) = pnone
[PROOF STEP]
show "\<And>hl. pgte pwrite (b hl)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>hl. pgte pwrite (b hl)
[PROOF STEP]
using assms(1) assms(2) p_greater_exists padd_asso
[PROOF STATE]
proof (prove)
using this:
valid_mask a
a = add_masks b c
pgte ?a ?b = (\<exists>r. ?a = padd ?b r)
padd (padd ?a ?b) ?c = padd ?a (padd ?b ?c)

goal (1 subgoal):
 1. \<And>hl. pgte pwrite (b hl)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
pgte pwrite (b ?hl)

goal (1 subgoal):
 1. \<And>f. b (null, f) = pnone
[PROOF STEP]
fix f
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>f. b (null, f) = pnone
[PROOF STEP]
show " b (null, f) = pnone"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. b (null, f) = pnone
[PROOF STEP]
by (metis add_masks_comm assms(1) assms(2) empty_mask.simps greater_mask_def greater_mask_equiv_def minus_empty pgte_antisym valid_mask.simps)
[PROOF STATE]
proof (state)
this:
b (null, f) = pnone

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma upper_valid:
  assumes "valid_mask a"
      and "a = add_masks b c"
    shows "valid_mask b \<and> valid_mask c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. valid_mask b \<and> valid_mask c
[PROOF STEP]
using add_masks_comm assms(1) assms(2) upper_valid_aux
[PROOF STATE]
proof (prove)
using this:
add_masks ?a ?b = add_masks ?b ?a
valid_mask a
a = add_masks b c
\<lbrakk>valid_mask ?a; ?a = add_masks ?b ?c\<rbrakk> \<Longrightarrow> valid_mask ?b

goal (1 subgoal):
 1. valid_mask b \<and> valid_mask c
[PROOF STEP]
by blast


[STATEMENT]
lemma equal_on_bmaskI:
  assumes "\<And>hl. \<pi> hl \<Longrightarrow> h hl = h' hl"
  shows "equal_on_bmask \<pi> h h'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. equal_on_bmask \<pi> h h'
[PROOF STEP]
using assms equal_on_bmask_def
[PROOF STATE]
proof (prove)
using this:
\<pi> ?hl \<Longrightarrow> h ?hl = h' ?hl
equal_on_bmask ?\<pi> ?h ?h' = (\<forall>hl. ?\<pi> hl \<longrightarrow> ?h hl = ?h' hl)

goal (1 subgoal):
 1. equal_on_bmask \<pi> h h'
[PROOF STEP]
by blast


[STATEMENT]
lemma big_add_greater:
  "big_greater_mask (big_add_masks A B) B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. big_greater_mask (big_add_masks A B) B
[PROOF STEP]
by (metis add_masks_comm big_add_masks_def big_greater_mask_def greater_mask_def)


[STATEMENT]
lemma big_greater_iff:
  "big_greater_mask A B \<Longrightarrow> (\<exists>C. A = big_add_masks B C)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. big_greater_mask A B \<Longrightarrow> \<exists>C. A = big_add_masks B C
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. big_greater_mask A B \<Longrightarrow> \<exists>C. A = big_add_masks B C
[PROOF STEP]
assume "big_greater_mask A B"
[PROOF STATE]
proof (state)
this:
big_greater_mask A B

goal (1 subgoal):
 1. big_greater_mask A B \<Longrightarrow> \<exists>C. A = big_add_masks B C
[PROOF STEP]
let ?C = "\<lambda>h. SOME r. A h = add_masks (B h) r"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. big_greater_mask A B \<Longrightarrow> \<exists>C. A = big_add_masks B C
[PROOF STEP]
have "A = big_add_masks B ?C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A = big_add_masks B (\<lambda>h. SOME r. A h = add_masks (B h) r)
[PROOF STEP]
proof (rule ext)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. A x = big_add_masks B (\<lambda>h. SOME r. A h = add_masks (B h) r) x
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. A x = big_add_masks B (\<lambda>h. SOME r. A h = add_masks (B h) r) x
[PROOF STEP]
have "A x = add_masks (B x) (?C x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A x = add_masks (B x) (SOME r. A x = add_masks (B x) r)
[PROOF STEP]
proof (rule ext)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xa. A x xa = add_masks (B x) (SOME r. A x = add_masks (B x) r) xa
[PROOF STEP]
fix xa
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xa. A x xa = add_masks (B x) (SOME r. A x = add_masks (B x) r) xa
[PROOF STEP]
have "A x = add_masks (B x) (SOME r. A x = add_masks (B x) r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A x = add_masks (B x) (SOME r. A x = add_masks (B x) r)
[PROOF STEP]
by (metis (mono_tags, lifting) \<open>big_greater_mask A B\<close> big_greater_mask_def greater_mask_def someI_ex)
[PROOF STATE]
proof (state)
this:
A x = add_masks (B x) (SOME r. A x = add_masks (B x) r)

goal (1 subgoal):
 1. \<And>xa. A x xa = add_masks (B x) (SOME r. A x = add_masks (B x) r) xa
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
A x = add_masks (B x) (SOME r. A x = add_masks (B x) r)
[PROOF STEP]
show "A x xa = add_masks (B x) (SOME r. A x = add_masks (B x) r) xa"
[PROOF STATE]
proof (prove)
using this:
A x = add_masks (B x) (SOME r. A x = add_masks (B x) r)

goal (1 subgoal):
 1. A x xa = add_masks (B x) (SOME r. A x = add_masks (B x) r) xa
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
A x xa = add_masks (B x) (SOME r. A x = add_masks (B x) r) xa

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
A x = add_masks (B x) (SOME r. A x = add_masks (B x) r)

goal (1 subgoal):
 1. \<And>x. A x = big_add_masks B (\<lambda>h. SOME r. A h = add_masks (B h) r) x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
A x = add_masks (B x) (SOME r. A x = add_masks (B x) r)
[PROOF STEP]
show "A x = big_add_masks B (\<lambda>h. SOME r. A h = add_masks (B h) r) x"
[PROOF STATE]
proof (prove)
using this:
A x = add_masks (B x) (SOME r. A x = add_masks (B x) r)

goal (1 subgoal):
 1. A x = big_add_masks B (\<lambda>h. SOME r. A h = add_masks (B h) r) x
[PROOF STEP]
by (metis (no_types, lifting) big_add_masks_def)
[PROOF STATE]
proof (state)
this:
A x = big_add_masks B (\<lambda>h. SOME r. A h = add_masks (B h) r) x

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
A = big_add_masks B (\<lambda>h. SOME r. A h = add_masks (B h) r)

goal (1 subgoal):
 1. big_greater_mask A B \<Longrightarrow> \<exists>C. A = big_add_masks B C
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
A = big_add_masks B (\<lambda>h. SOME r. A h = add_masks (B h) r)
[PROOF STEP]
show "\<exists>C. A = big_add_masks B C"
[PROOF STATE]
proof (prove)
using this:
A = big_add_masks B (\<lambda>h. SOME r. A h = add_masks (B h) r)

goal (1 subgoal):
 1. \<exists>C. A = big_add_masks B C
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
\<exists>C. A = big_add_masks B C

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma big_add_masks_asso:
  "big_add_masks A (big_add_masks B C) = big_add_masks (big_add_masks A B) C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. big_add_masks A (big_add_masks B C) = big_add_masks (big_add_masks A B) C
[PROOF STEP]
proof (rule ext)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. big_add_masks A (big_add_masks B C) x = big_add_masks (big_add_masks A B) C x
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. big_add_masks A (big_add_masks B C) x = big_add_masks (big_add_masks A B) C x
[PROOF STEP]
show "big_add_masks A (big_add_masks B C) x = big_add_masks (big_add_masks A B) C x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. big_add_masks A (big_add_masks B C) x = big_add_masks (big_add_masks A B) C x
[PROOF STEP]
by (simp add: add_masks_asso big_add_masks_def)
[PROOF STATE]
proof (state)
this:
big_add_masks A (big_add_masks B C) x = big_add_masks (big_add_masks A B) C x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma big_add_mask_neutral:
  "big_add_masks \<Pi> (\<lambda>_. empty_mask) = \<Pi>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. big_add_masks \<Pi> (\<lambda>_. empty_mask) = \<Pi>
[PROOF STEP]
proof (rule ext)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. big_add_masks \<Pi> (\<lambda>_. empty_mask) x = \<Pi> x
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. big_add_masks \<Pi> (\<lambda>_. empty_mask) x = \<Pi> x
[PROOF STEP]
show "big_add_masks \<Pi> (\<lambda>_. empty_mask) x = \<Pi> x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. big_add_masks \<Pi> (\<lambda>_. empty_mask) x = \<Pi> x
[PROOF STEP]
by (metis big_add_masks_def minus_empty)
[PROOF STATE]
proof (state)
this:
big_add_masks \<Pi> (\<lambda>_. empty_mask) x = \<Pi> x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma sym_equal_on_mask:
  "equal_on_mask \<pi> a b \<longleftrightarrow> equal_on_mask \<pi> b a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. equal_on_mask \<pi> a b = equal_on_mask \<pi> b a
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. equal_on_mask \<pi> a b = equal_on_mask \<pi> b a
[PROOF STEP]
have "\<And>a b. equal_on_mask \<pi> a b \<Longrightarrow> equal_on_mask \<pi> b a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b. equal_on_mask \<pi> a b \<Longrightarrow> equal_on_mask \<pi> b a
[PROOF STEP]
by (simp add: equal_on_mask_def)
[PROOF STATE]
proof (state)
this:
equal_on_mask \<pi> ?a ?b \<Longrightarrow> equal_on_mask \<pi> ?b ?a

goal (1 subgoal):
 1. equal_on_mask \<pi> a b = equal_on_mask \<pi> b a
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
equal_on_mask \<pi> ?a ?b \<Longrightarrow> equal_on_mask \<pi> ?b ?a
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
equal_on_mask \<pi> ?a ?b \<Longrightarrow> equal_on_mask \<pi> ?b ?a

goal (1 subgoal):
 1. equal_on_mask \<pi> a b = equal_on_mask \<pi> b a
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
equal_on_mask \<pi> a b = equal_on_mask \<pi> b a

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma greater_mask_uni_equiv:
  "greater_mask \<pi> (uni_mask hl r) \<longleftrightarrow> pgte (\<pi> hl) r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. greater_mask \<pi> (uni_mask hl r) = pgte (\<pi> hl) r
[PROOF STEP]
by (metis add_masks_comm fun_upd_apply greater_mask_def greater_mask_equiv_def minus_empty uni_mask.simps)


[STATEMENT]
lemma greater_mask_uniI:
  assumes "pgte (\<pi> hl) r"
  shows "greater_mask \<pi> (uni_mask hl r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. greater_mask \<pi> (uni_mask hl r)
[PROOF STEP]
using greater_mask_uni_equiv assms
[PROOF STATE]
proof (prove)
using this:
greater_mask ?\<pi> (uni_mask ?hl ?r) = pgte (?\<pi> ?hl) ?r
pgte (\<pi> hl) r

goal (1 subgoal):
 1. greater_mask \<pi> (uni_mask hl r)
[PROOF STEP]
by metis


[STATEMENT]
lemma greater_bmask_refl:
  "greater_bmask H H"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. greater_bmask H H
[PROOF STEP]
by (simp add: greater_bmask_def)


[STATEMENT]
lemma greater_bmask_trans:
  assumes "greater_bmask A B"
      and "greater_bmask B C"
    shows "greater_bmask A C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. greater_bmask A C
[PROOF STEP]
by (metis assms(1) assms(2) greater_bmask_def)


[STATEMENT]
lemma update_dm_same:
  "update_dm dm \<pi> \<pi> = dm"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. update_dm dm \<pi> \<pi> = dm
[PROOF STEP]
proof (rule ext)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. update_dm dm \<pi> \<pi> x = dm x
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. update_dm dm \<pi> \<pi> x = dm x
[PROOF STEP]
show "update_dm dm \<pi> \<pi> x = dm x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. update_dm dm \<pi> \<pi> x = dm x
[PROOF STEP]
by (simp add: pgt.rep_eq update_dm_def)
[PROOF STATE]
proof (state)
this:
update_dm dm \<pi> \<pi> x = dm x

goal:
No subgoals!
[PROOF STEP]
qed