[STATEMENT]
lemma veval'_closed:
  assumes "\<Gamma> \<turnstile>\<^sub>v t \<down> v" "closed_except t (fmdom \<Gamma>)" "closed_venv \<Gamma>"
  assumes "wellformed t" "wellformed_venv \<Gamma>"
  shows "vclosed v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vclosed v
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<Gamma> \<turnstile>\<^sub>v t \<down> v
closed_except t (fmdom \<Gamma>)
closed_venv \<Gamma>
pre_strong_term_class.wellformed t
wellformed_venv \<Gamma>

goal (1 subgoal):
 1. vclosed v
[PROOF STEP]
proof induction
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. \<And>name \<Gamma> val. \<lbrakk>name |\<notin>| C; fmlookup \<Gamma> name = Some val; closed_except (Sconst name) (fmdom \<Gamma>); closed_venv \<Gamma>; pre_strong_term_class.wellformed (Sconst name); wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vclosed val
 2. \<And>\<Gamma> name val. \<lbrakk>fmlookup \<Gamma> name = Some val; closed_except (Svar name) (fmdom \<Gamma>); closed_venv \<Gamma>; pre_strong_term_class.wellformed (Svar name); wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vclosed val
 3. \<And>\<Gamma> cs. \<lbrakk>closed_except (Sabs cs) (fmdom \<Gamma>); closed_venv \<Gamma>; pre_strong_term_class.wellformed (Sabs cs); wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vclosed (Vabs cs \<Gamma>)
 4. \<And>\<Gamma> t cs \<Gamma>' u u' env uu_ rhs val. \<lbrakk>\<Gamma> \<turnstile>\<^sub>v t \<down> Vabs cs \<Gamma>'; \<lbrakk>closed_except t (fmdom \<Gamma>); closed_venv \<Gamma>; pre_strong_term_class.wellformed t; wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vclosed (Vabs cs \<Gamma>'); \<Gamma> \<turnstile>\<^sub>v u \<down> u'; \<lbrakk>closed_except u (fmdom \<Gamma>); closed_venv \<Gamma>; pre_strong_term_class.wellformed u; wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vclosed u'; vfind_match cs u' = Some (env, uu_, rhs); \<Gamma>' ++\<^sub>f env \<turnstile>\<^sub>v rhs \<down> val; \<lbrakk>closed_except rhs (fmdom (\<Gamma>' ++\<^sub>f env)); closed_venv (\<Gamma>' ++\<^sub>f env); pre_strong_term_class.wellformed rhs; wellformed_venv (\<Gamma>' ++\<^sub>f env)\<rbrakk> \<Longrightarrow> vclosed val; closed_except (t $\<^sub>s u) (fmdom \<Gamma>); closed_venv \<Gamma>; pre_strong_term_class.wellformed (t $\<^sub>s u); wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vclosed val
 5. \<And>\<Gamma> t css name \<Gamma>' cs u u' env uv_ rhs val. \<lbrakk>\<Gamma> \<turnstile>\<^sub>v t \<down> Vrecabs css name \<Gamma>'; \<lbrakk>closed_except t (fmdom \<Gamma>); closed_venv \<Gamma>; pre_strong_term_class.wellformed t; wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vclosed (Vrecabs css name \<Gamma>'); fmlookup css name = Some cs; \<Gamma> \<turnstile>\<^sub>v u \<down> u'; \<lbrakk>closed_except u (fmdom \<Gamma>); closed_venv \<Gamma>; pre_strong_term_class.wellformed u; wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vclosed u'; vfind_match cs u' = Some (env, uv_, rhs); \<Gamma>' ++\<^sub>f mk_rec_env css \<Gamma>' ++\<^sub>f env \<turnstile>\<^sub>v rhs \<down> val; \<lbrakk>closed_except rhs (fmdom (\<Gamma>' ++\<^sub>f mk_rec_env css \<Gamma>' ++\<^sub>f env)); closed_venv (\<Gamma>' ++\<^sub>f mk_rec_env css \<Gamma>' ++\<^sub>f env); pre_strong_term_class.wellformed rhs; wellformed_venv (\<Gamma>' ++\<^sub>f mk_rec_env css \<Gamma>' ++\<^sub>f env)\<rbrakk> \<Longrightarrow> vclosed val; closed_except (t $\<^sub>s u) (fmdom \<Gamma>); closed_venv \<Gamma>; pre_strong_term_class.wellformed (t $\<^sub>s u); wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vclosed val
 6. \<And>name \<Gamma> ts us. \<lbrakk>name |\<in>| C; list_all2 (\<lambda>x1 x2. \<Gamma> \<turnstile>\<^sub>v x1 \<down> x2 \<and> (closed_except x1 (fmdom \<Gamma>) \<longrightarrow> closed_venv \<Gamma> \<longrightarrow> pre_strong_term_class.wellformed x1 \<longrightarrow> wellformed_venv \<Gamma> \<longrightarrow> vclosed x2)) ts us; closed_except (name $$ ts) (fmdom \<Gamma>); closed_venv \<Gamma>; pre_strong_term_class.wellformed (name $$ ts); wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vclosed (Vconstr name us)
[PROOF STEP]
case (comb \<Gamma> t cs \<Gamma>' u u' env pat rhs val)
[PROOF STATE]
proof (state)
this:
\<Gamma> \<turnstile>\<^sub>v t \<down> Vabs cs \<Gamma>'
\<Gamma> \<turnstile>\<^sub>v u \<down> u'
vfind_match cs u' = Some (env, pat, rhs)
\<Gamma>' ++\<^sub>f env \<turnstile>\<^sub>v rhs \<down> val
\<lbrakk>closed_except t (fmdom \<Gamma>); closed_venv \<Gamma>; pre_strong_term_class.wellformed t; wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vclosed (Vabs cs \<Gamma>')
\<lbrakk>closed_except u (fmdom \<Gamma>); closed_venv \<Gamma>; pre_strong_term_class.wellformed u; wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vclosed u'
\<lbrakk>closed_except rhs (fmdom (\<Gamma>' ++\<^sub>f env)); closed_venv (\<Gamma>' ++\<^sub>f env); pre_strong_term_class.wellformed rhs; wellformed_venv (\<Gamma>' ++\<^sub>f env)\<rbrakk> \<Longrightarrow> vclosed val
closed_except (t $\<^sub>s u) (fmdom \<Gamma>)
closed_venv \<Gamma>
pre_strong_term_class.wellformed (t $\<^sub>s u)
wellformed_venv \<Gamma>

goal (6 subgoals):
 1. \<And>name \<Gamma> val. \<lbrakk>name |\<notin>| C; fmlookup \<Gamma> name = Some val; closed_except (Sconst name) (fmdom \<Gamma>); closed_venv \<Gamma>; pre_strong_term_class.wellformed (Sconst name); wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vclosed val
 2. \<And>\<Gamma> name val. \<lbrakk>fmlookup \<Gamma> name = Some val; closed_except (Svar name) (fmdom \<Gamma>); closed_venv \<Gamma>; pre_strong_term_class.wellformed (Svar name); wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vclosed val
 3. \<And>\<Gamma> cs. \<lbrakk>closed_except (Sabs cs) (fmdom \<Gamma>); closed_venv \<Gamma>; pre_strong_term_class.wellformed (Sabs cs); wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vclosed (Vabs cs \<Gamma>)
 4. \<And>\<Gamma> t cs \<Gamma>' u u' env uu_ rhs val. \<lbrakk>\<Gamma> \<turnstile>\<^sub>v t \<down> Vabs cs \<Gamma>'; \<lbrakk>closed_except t (fmdom \<Gamma>); closed_venv \<Gamma>; pre_strong_term_class.wellformed t; wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vclosed (Vabs cs \<Gamma>'); \<Gamma> \<turnstile>\<^sub>v u \<down> u'; \<lbrakk>closed_except u (fmdom \<Gamma>); closed_venv \<Gamma>; pre_strong_term_class.wellformed u; wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vclosed u'; vfind_match cs u' = Some (env, uu_, rhs); \<Gamma>' ++\<^sub>f env \<turnstile>\<^sub>v rhs \<down> val; \<lbrakk>closed_except rhs (fmdom (\<Gamma>' ++\<^sub>f env)); closed_venv (\<Gamma>' ++\<^sub>f env); pre_strong_term_class.wellformed rhs; wellformed_venv (\<Gamma>' ++\<^sub>f env)\<rbrakk> \<Longrightarrow> vclosed val; closed_except (t $\<^sub>s u) (fmdom \<Gamma>); closed_venv \<Gamma>; pre_strong_term_class.wellformed (t $\<^sub>s u); wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vclosed val
 5. \<And>\<Gamma> t css name \<Gamma>' cs u u' env uv_ rhs val. \<lbrakk>\<Gamma> \<turnstile>\<^sub>v t \<down> Vrecabs css name \<Gamma>'; \<lbrakk>closed_except t (fmdom \<Gamma>); closed_venv \<Gamma>; pre_strong_term_class.wellformed t; wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vclosed (Vrecabs css name \<Gamma>'); fmlookup css name = Some cs; \<Gamma> \<turnstile>\<^sub>v u \<down> u'; \<lbrakk>closed_except u (fmdom \<Gamma>); closed_venv \<Gamma>; pre_strong_term_class.wellformed u; wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vclosed u'; vfind_match cs u' = Some (env, uv_, rhs); \<Gamma>' ++\<^sub>f mk_rec_env css \<Gamma>' ++\<^sub>f env \<turnstile>\<^sub>v rhs \<down> val; \<lbrakk>closed_except rhs (fmdom (\<Gamma>' ++\<^sub>f mk_rec_env css \<Gamma>' ++\<^sub>f env)); closed_venv (\<Gamma>' ++\<^sub>f mk_rec_env css \<Gamma>' ++\<^sub>f env); pre_strong_term_class.wellformed rhs; wellformed_venv (\<Gamma>' ++\<^sub>f mk_rec_env css \<Gamma>' ++\<^sub>f env)\<rbrakk> \<Longrightarrow> vclosed val; closed_except (t $\<^sub>s u) (fmdom \<Gamma>); closed_venv \<Gamma>; pre_strong_term_class.wellformed (t $\<^sub>s u); wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vclosed val
 6. \<And>name \<Gamma> ts us. \<lbrakk>name |\<in>| C; list_all2 (\<lambda>x1 x2. \<Gamma> \<turnstile>\<^sub>v x1 \<down> x2 \<and> (closed_except x1 (fmdom \<Gamma>) \<longrightarrow> closed_venv \<Gamma> \<longrightarrow> pre_strong_term_class.wellformed x1 \<longrightarrow> wellformed_venv \<Gamma> \<longrightarrow> vclosed x2)) ts us; closed_except (name $$ ts) (fmdom \<Gamma>); closed_venv \<Gamma>; pre_strong_term_class.wellformed (name $$ ts); wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vclosed (Vconstr name us)
[PROOF STEP]
hence "vclosed (Vabs cs \<Gamma>')"
[PROOF STATE]
proof (prove)
using this:
\<Gamma> \<turnstile>\<^sub>v t \<down> Vabs cs \<Gamma>'
\<Gamma> \<turnstile>\<^sub>v u \<down> u'
vfind_match cs u' = Some (env, pat, rhs)
\<Gamma>' ++\<^sub>f env \<turnstile>\<^sub>v rhs \<down> val
\<lbrakk>closed_except t (fmdom \<Gamma>); closed_venv \<Gamma>; pre_strong_term_class.wellformed t; wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vclosed (Vabs cs \<Gamma>')
\<lbrakk>closed_except u (fmdom \<Gamma>); closed_venv \<Gamma>; pre_strong_term_class.wellformed u; wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vclosed u'
\<lbrakk>closed_except rhs (fmdom (\<Gamma>' ++\<^sub>f env)); closed_venv (\<Gamma>' ++\<^sub>f env); pre_strong_term_class.wellformed rhs; wellformed_venv (\<Gamma>' ++\<^sub>f env)\<rbrakk> \<Longrightarrow> vclosed val
closed_except (t $\<^sub>s u) (fmdom \<Gamma>)
closed_venv \<Gamma>
pre_strong_term_class.wellformed (t $\<^sub>s u)
wellformed_venv \<Gamma>

goal (1 subgoal):
 1. vclosed (Vabs cs \<Gamma>')
[PROOF STEP]
by (auto simp: closed_except_def)
[PROOF STATE]
proof (state)
this:
vclosed (Vabs cs \<Gamma>')

goal (6 subgoals):
 1. \<And>name \<Gamma> val. \<lbrakk>name |\<notin>| C; fmlookup \<Gamma> name = Some val; closed_except (Sconst name) (fmdom \<Gamma>); closed_venv \<Gamma>; pre_strong_term_class.wellformed (Sconst name); wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vclosed val
 2. \<And>\<Gamma> name val. \<lbrakk>fmlookup \<Gamma> name = Some val; closed_except (Svar name) (fmdom \<Gamma>); closed_venv \<Gamma>; pre_strong_term_class.wellformed (Svar name); wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vclosed val
 3. \<And>\<Gamma> cs. \<lbrakk>closed_except (Sabs cs) (fmdom \<Gamma>); closed_venv \<Gamma>; pre_strong_term_class.wellformed (Sabs cs); wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vclosed (Vabs cs \<Gamma>)
 4. \<And>\<Gamma> t cs \<Gamma>' u u' env uu_ rhs val. \<lbrakk>\<Gamma> \<turnstile>\<^sub>v t \<down> Vabs cs \<Gamma>'; \<lbrakk>closed_except t (fmdom \<Gamma>); closed_venv \<Gamma>; pre_strong_term_class.wellformed t; wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vclosed (Vabs cs \<Gamma>'); \<Gamma> \<turnstile>\<^sub>v u \<down> u'; \<lbrakk>closed_except u (fmdom \<Gamma>); closed_venv \<Gamma>; pre_strong_term_class.wellformed u; wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vclosed u'; vfind_match cs u' = Some (env, uu_, rhs); \<Gamma>' ++\<^sub>f env \<turnstile>\<^sub>v rhs \<down> val; \<lbrakk>closed_except rhs (fmdom (\<Gamma>' ++\<^sub>f env)); closed_venv (\<Gamma>' ++\<^sub>f env); pre_strong_term_class.wellformed rhs; wellformed_venv (\<Gamma>' ++\<^sub>f env)\<rbrakk> \<Longrightarrow> vclosed val; closed_except (t $\<^sub>s u) (fmdom \<Gamma>); closed_venv \<Gamma>; pre_strong_term_class.wellformed (t $\<^sub>s u); wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vclosed val
 5. \<And>\<Gamma> t css name \<Gamma>' cs u u' env uv_ rhs val. \<lbrakk>\<Gamma> \<turnstile>\<^sub>v t \<down> Vrecabs css name \<Gamma>'; \<lbrakk>closed_except t (fmdom \<Gamma>); closed_venv \<Gamma>; pre_strong_term_class.wellformed t; wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vclosed (Vrecabs css name \<Gamma>'); fmlookup css name = Some cs; \<Gamma> \<turnstile>\<^sub>v u \<down> u'; \<lbrakk>closed_except u (fmdom \<Gamma>); closed_venv \<Gamma>; pre_strong_term_class.wellformed u; wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vclosed u'; vfind_match cs u' = Some (env, uv_, rhs); \<Gamma>' ++\<^sub>f mk_rec_env css \<Gamma>' ++\<^sub>f env \<turnstile>\<^sub>v rhs \<down> val; \<lbrakk>closed_except rhs (fmdom (\<Gamma>' ++\<^sub>f mk_rec_env css \<Gamma>' ++\<^sub>f env)); closed_venv (\<Gamma>' ++\<^sub>f mk_rec_env css \<Gamma>' ++\<^sub>f env); pre_strong_term_class.wellformed rhs; wellformed_venv (\<Gamma>' ++\<^sub>f mk_rec_env css \<Gamma>' ++\<^sub>f env)\<rbrakk> \<Longrightarrow> vclosed val; closed_except (t $\<^sub>s u) (fmdom \<Gamma>); closed_venv \<Gamma>; pre_strong_term_class.wellformed (t $\<^sub>s u); wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vclosed val
 6. \<And>name \<Gamma> ts us. \<lbrakk>name |\<in>| C; list_all2 (\<lambda>x1 x2. \<Gamma> \<turnstile>\<^sub>v x1 \<down> x2 \<and> (closed_except x1 (fmdom \<Gamma>) \<longrightarrow> closed_venv \<Gamma> \<longrightarrow> pre_strong_term_class.wellformed x1 \<longrightarrow> wellformed_venv \<Gamma> \<longrightarrow> vclosed x2)) ts us; closed_except (name $$ ts) (fmdom \<Gamma>); closed_venv \<Gamma>; pre_strong_term_class.wellformed (name $$ ts); wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vclosed (Vconstr name us)
[PROOF STEP]
have "(pat, rhs) \<in> set cs" "vmatch (mk_pat pat) u' = Some env"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (pat, rhs) \<in> set cs &&& vmatch (mk_pat pat) u' = Some env
[PROOF STEP]
by (rule vfind_match_elem; fact)+
[PROOF STATE]
proof (state)
this:
(pat, rhs) \<in> set cs
vmatch (mk_pat pat) u' = Some env

goal (6 subgoals):
 1. \<And>name \<Gamma> val. \<lbrakk>name |\<notin>| C; fmlookup \<Gamma> name = Some val; closed_except (Sconst name) (fmdom \<Gamma>); closed_venv \<Gamma>; pre_strong_term_class.wellformed (Sconst name); wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vclosed val
 2. \<And>\<Gamma> name val. \<lbrakk>fmlookup \<Gamma> name = Some val; closed_except (Svar name) (fmdom \<Gamma>); closed_venv \<Gamma>; pre_strong_term_class.wellformed (Svar name); wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vclosed val
 3. \<And>\<Gamma> cs. \<lbrakk>closed_except (Sabs cs) (fmdom \<Gamma>); closed_venv \<Gamma>; pre_strong_term_class.wellformed (Sabs cs); wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vclosed (Vabs cs \<Gamma>)
 4. \<And>\<Gamma> t cs \<Gamma>' u u' env uu_ rhs val. \<lbrakk>\<Gamma> \<turnstile>\<^sub>v t \<down> Vabs cs \<Gamma>'; \<lbrakk>closed_except t (fmdom \<Gamma>); closed_venv \<Gamma>; pre_strong_term_class.wellformed t; wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vclosed (Vabs cs \<Gamma>'); \<Gamma> \<turnstile>\<^sub>v u \<down> u'; \<lbrakk>closed_except u (fmdom \<Gamma>); closed_venv \<Gamma>; pre_strong_term_class.wellformed u; wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vclosed u'; vfind_match cs u' = Some (env, uu_, rhs); \<Gamma>' ++\<^sub>f env \<turnstile>\<^sub>v rhs \<down> val; \<lbrakk>closed_except rhs (fmdom (\<Gamma>' ++\<^sub>f env)); closed_venv (\<Gamma>' ++\<^sub>f env); pre_strong_term_class.wellformed rhs; wellformed_venv (\<Gamma>' ++\<^sub>f env)\<rbrakk> \<Longrightarrow> vclosed val; closed_except (t $\<^sub>s u) (fmdom \<Gamma>); closed_venv \<Gamma>; pre_strong_term_class.wellformed (t $\<^sub>s u); wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vclosed val
 5. \<And>\<Gamma> t css name \<Gamma>' cs u u' env uv_ rhs val. \<lbrakk>\<Gamma> \<turnstile>\<^sub>v t \<down> Vrecabs css name \<Gamma>'; \<lbrakk>closed_except t (fmdom \<Gamma>); closed_venv \<Gamma>; pre_strong_term_class.wellformed t; wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vclosed (Vrecabs css name \<Gamma>'); fmlookup css name = Some cs; \<Gamma> \<turnstile>\<^sub>v u \<down> u'; \<lbrakk>closed_except u (fmdom \<Gamma>); closed_venv \<Gamma>; pre_strong_term_class.wellformed u; wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vclosed u'; vfind_match cs u' = Some (env, uv_, rhs); \<Gamma>' ++\<^sub>f mk_rec_env css \<Gamma>' ++\<^sub>f env \<turnstile>\<^sub>v rhs \<down> val; \<lbrakk>closed_except rhs (fmdom (\<Gamma>' ++\<^sub>f mk_rec_env css \<Gamma>' ++\<^sub>f env)); closed_venv (\<Gamma>' ++\<^sub>f mk_rec_env css \<Gamma>' ++\<^sub>f env); pre_strong_term_class.wellformed rhs; wellformed_venv (\<Gamma>' ++\<^sub>f mk_rec_env css \<Gamma>' ++\<^sub>f env)\<rbrakk> \<Longrightarrow> vclosed val; closed_except (t $\<^sub>s u) (fmdom \<Gamma>); closed_venv \<Gamma>; pre_strong_term_class.wellformed (t $\<^sub>s u); wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vclosed val
 6. \<And>name \<Gamma> ts us. \<lbrakk>name |\<in>| C; list_all2 (\<lambda>x1 x2. \<Gamma> \<turnstile>\<^sub>v x1 \<down> x2 \<and> (closed_except x1 (fmdom \<Gamma>) \<longrightarrow> closed_venv \<Gamma> \<longrightarrow> pre_strong_term_class.wellformed x1 \<longrightarrow> wellformed_venv \<Gamma> \<longrightarrow> vclosed x2)) ts us; closed_except (name $$ ts) (fmdom \<Gamma>); closed_venv \<Gamma>; pre_strong_term_class.wellformed (name $$ ts); wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vclosed (Vconstr name us)
[PROOF STEP]
hence "fmdom env = patvars (mk_pat pat)"
[PROOF STATE]
proof (prove)
using this:
(pat, rhs) \<in> set cs
vmatch (mk_pat pat) u' = Some env

goal (1 subgoal):
 1. fmdom env = patvars (mk_pat pat)
[PROOF STEP]
by (simp add: vmatch_dom)
[PROOF STATE]
proof (state)
this:
fmdom env = patvars (mk_pat pat)

goal (6 subgoals):
 1. \<And>name \<Gamma> val. \<lbrakk>name |\<notin>| C; fmlookup \<Gamma> name = Some val; closed_except (Sconst name) (fmdom \<Gamma>); closed_venv \<Gamma>; pre_strong_term_class.wellformed (Sconst name); wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vclosed val
 2. \<And>\<Gamma> name val. \<lbrakk>fmlookup \<Gamma> name = Some val; closed_except (Svar name) (fmdom \<Gamma>); closed_venv \<Gamma>; pre_strong_term_class.wellformed (Svar name); wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vclosed val
 3. \<And>\<Gamma> cs. \<lbrakk>closed_except (Sabs cs) (fmdom \<Gamma>); closed_venv \<Gamma>; pre_strong_term_class.wellformed (Sabs cs); wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vclosed (Vabs cs \<Gamma>)
 4. \<And>\<Gamma> t cs \<Gamma>' u u' env uu_ rhs val. \<lbrakk>\<Gamma> \<turnstile>\<^sub>v t \<down> Vabs cs \<Gamma>'; \<lbrakk>closed_except t (fmdom \<Gamma>); closed_venv \<Gamma>; pre_strong_term_class.wellformed t; wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vclosed (Vabs cs \<Gamma>'); \<Gamma> \<turnstile>\<^sub>v u \<down> u'; \<lbrakk>closed_except u (fmdom \<Gamma>); closed_venv \<Gamma>; pre_strong_term_class.wellformed u; wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vclosed u'; vfind_match cs u' = Some (env, uu_, rhs); \<Gamma>' ++\<^sub>f env \<turnstile>\<^sub>v rhs \<down> val; \<lbrakk>closed_except rhs (fmdom (\<Gamma>' ++\<^sub>f env)); closed_venv (\<Gamma>' ++\<^sub>f env); pre_strong_term_class.wellformed rhs; wellformed_venv (\<Gamma>' ++\<^sub>f env)\<rbrakk> \<Longrightarrow> vclosed val; closed_except (t $\<^sub>s u) (fmdom \<Gamma>); closed_venv \<Gamma>; pre_strong_term_class.wellformed (t $\<^sub>s u); wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vclosed val
 5. \<And>\<Gamma> t css name \<Gamma>' cs u u' env uv_ rhs val. \<lbrakk>\<Gamma> \<turnstile>\<^sub>v t \<down> Vrecabs css name \<Gamma>'; \<lbrakk>closed_except t (fmdom \<Gamma>); closed_venv \<Gamma>; pre_strong_term_class.wellformed t; wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vclosed (Vrecabs css name \<Gamma>'); fmlookup css name = Some cs; \<Gamma> \<turnstile>\<^sub>v u \<down> u'; \<lbrakk>closed_except u (fmdom \<Gamma>); closed_venv \<Gamma>; pre_strong_term_class.wellformed u; wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vclosed u'; vfind_match cs u' = Some (env, uv_, rhs); \<Gamma>' ++\<^sub>f mk_rec_env css \<Gamma>' ++\<^sub>f env \<turnstile>\<^sub>v rhs \<down> val; \<lbrakk>closed_except rhs (fmdom (\<Gamma>' ++\<^sub>f mk_rec_env css \<Gamma>' ++\<^sub>f env)); closed_venv (\<Gamma>' ++\<^sub>f mk_rec_env css \<Gamma>' ++\<^sub>f env); pre_strong_term_class.wellformed rhs; wellformed_venv (\<Gamma>' ++\<^sub>f mk_rec_env css \<Gamma>' ++\<^sub>f env)\<rbrakk> \<Longrightarrow> vclosed val; closed_except (t $\<^sub>s u) (fmdom \<Gamma>); closed_venv \<Gamma>; pre_strong_term_class.wellformed (t $\<^sub>s u); wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vclosed val
 6. \<And>name \<Gamma> ts us. \<lbrakk>name |\<in>| C; list_all2 (\<lambda>x1 x2. \<Gamma> \<turnstile>\<^sub>v x1 \<down> x2 \<and> (closed_except x1 (fmdom \<Gamma>) \<longrightarrow> closed_venv \<Gamma> \<longrightarrow> pre_strong_term_class.wellformed x1 \<longrightarrow> wellformed_venv \<Gamma> \<longrightarrow> vclosed x2)) ts us; closed_except (name $$ ts) (fmdom \<Gamma>); closed_venv \<Gamma>; pre_strong_term_class.wellformed (name $$ ts); wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vclosed (Vconstr name us)
[PROOF STEP]
have "vwellformed (Vabs cs \<Gamma>')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vwellformed (Vabs cs \<Gamma>')
[PROOF STEP]
apply (rule veval'_wellformed)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. ?\<Gamma> \<turnstile>\<^sub>v ?t \<down> Vabs cs \<Gamma>'
 2. pre_strong_term_class.wellformed ?t
 3. wellformed_venv ?\<Gamma>
[PROOF STEP]
using comb
[PROOF STATE]
proof (prove)
using this:
\<Gamma> \<turnstile>\<^sub>v t \<down> Vabs cs \<Gamma>'
\<Gamma> \<turnstile>\<^sub>v u \<down> u'
vfind_match cs u' = Some (env, pat, rhs)
\<Gamma>' ++\<^sub>f env \<turnstile>\<^sub>v rhs \<down> val
\<lbrakk>closed_except t (fmdom \<Gamma>); closed_venv \<Gamma>; pre_strong_term_class.wellformed t; wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vclosed (Vabs cs \<Gamma>')
\<lbrakk>closed_except u (fmdom \<Gamma>); closed_venv \<Gamma>; pre_strong_term_class.wellformed u; wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vclosed u'
\<lbrakk>closed_except rhs (fmdom (\<Gamma>' ++\<^sub>f env)); closed_venv (\<Gamma>' ++\<^sub>f env); pre_strong_term_class.wellformed rhs; wellformed_venv (\<Gamma>' ++\<^sub>f env)\<rbrakk> \<Longrightarrow> vclosed val
closed_except (t $\<^sub>s u) (fmdom \<Gamma>)
closed_venv \<Gamma>
pre_strong_term_class.wellformed (t $\<^sub>s u)
wellformed_venv \<Gamma>

goal (3 subgoals):
 1. ?\<Gamma> \<turnstile>\<^sub>v ?t \<down> Vabs cs \<Gamma>'
 2. pre_strong_term_class.wellformed ?t
 3. wellformed_venv ?\<Gamma>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
vwellformed (Vabs cs \<Gamma>')

goal (6 subgoals):
 1. \<And>name \<Gamma> val. \<lbrakk>name |\<notin>| C; fmlookup \<Gamma> name = Some val; closed_except (Sconst name) (fmdom \<Gamma>); closed_venv \<Gamma>; pre_strong_term_class.wellformed (Sconst name); wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vclosed val
 2. \<And>\<Gamma> name val. \<lbrakk>fmlookup \<Gamma> name = Some val; closed_except (Svar name) (fmdom \<Gamma>); closed_venv \<Gamma>; pre_strong_term_class.wellformed (Svar name); wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vclosed val
 3. \<And>\<Gamma> cs. \<lbrakk>closed_except (Sabs cs) (fmdom \<Gamma>); closed_venv \<Gamma>; pre_strong_term_class.wellformed (Sabs cs); wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vclosed (Vabs cs \<Gamma>)
 4. \<And>\<Gamma> t cs \<Gamma>' u u' env uu_ rhs val. \<lbrakk>\<Gamma> \<turnstile>\<^sub>v t \<down> Vabs cs \<Gamma>'; \<lbrakk>closed_except t (fmdom \<Gamma>); closed_venv \<Gamma>; pre_strong_term_class.wellformed t; wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vclosed (Vabs cs \<Gamma>'); \<Gamma> \<turnstile>\<^sub>v u \<down> u'; \<lbrakk>closed_except u (fmdom \<Gamma>); closed_venv \<Gamma>; pre_strong_term_class.wellformed u; wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vclosed u'; vfind_match cs u' = Some (env, uu_, rhs); \<Gamma>' ++\<^sub>f env \<turnstile>\<^sub>v rhs \<down> val; \<lbrakk>closed_except rhs (fmdom (\<Gamma>' ++\<^sub>f env)); closed_venv (\<Gamma>' ++\<^sub>f env); pre_strong_term_class.wellformed rhs; wellformed_venv (\<Gamma>' ++\<^sub>f env)\<rbrakk> \<Longrightarrow> vclosed val; closed_except (t $\<^sub>s u) (fmdom \<Gamma>); closed_venv \<Gamma>; pre_strong_term_class.wellformed (t $\<^sub>s u); wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vclosed val
 5. \<And>\<Gamma> t css name \<Gamma>' cs u u' env uv_ rhs val. \<lbrakk>\<Gamma> \<turnstile>\<^sub>v t \<down> Vrecabs css name \<Gamma>'; \<lbrakk>closed_except t (fmdom \<Gamma>); closed_venv \<Gamma>; pre_strong_term_class.wellformed t; wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vclosed (Vrecabs css name \<Gamma>'); fmlookup css name = Some cs; \<Gamma> \<turnstile>\<^sub>v u \<down> u'; \<lbrakk>closed_except u (fmdom \<Gamma>); closed_venv \<Gamma>; pre_strong_term_class.wellformed u; wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vclosed u'; vfind_match cs u' = Some (env, uv_, rhs); \<Gamma>' ++\<^sub>f mk_rec_env css \<Gamma>' ++\<^sub>f env \<turnstile>\<^sub>v rhs \<down> val; \<lbrakk>closed_except rhs (fmdom (\<Gamma>' ++\<^sub>f mk_rec_env css \<Gamma>' ++\<^sub>f env)); closed_venv (\<Gamma>' ++\<^sub>f mk_rec_env css \<Gamma>' ++\<^sub>f env); pre_strong_term_class.wellformed rhs; wellformed_venv (\<Gamma>' ++\<^sub>f mk_rec_env css \<Gamma>' ++\<^sub>f env)\<rbrakk> \<Longrightarrow> vclosed val; closed_except (t $\<^sub>s u) (fmdom \<Gamma>); closed_venv \<Gamma>; pre_strong_term_class.wellformed (t $\<^sub>s u); wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vclosed val
 6. \<And>name \<Gamma> ts us. \<lbrakk>name |\<in>| C; list_all2 (\<lambda>x1 x2. \<Gamma> \<turnstile>\<^sub>v x1 \<down> x2 \<and> (closed_except x1 (fmdom \<Gamma>) \<longrightarrow> closed_venv \<Gamma> \<longrightarrow> pre_strong_term_class.wellformed x1 \<longrightarrow> wellformed_venv \<Gamma> \<longrightarrow> vclosed x2)) ts us; closed_except (name $$ ts) (fmdom \<Gamma>); closed_venv \<Gamma>; pre_strong_term_class.wellformed (name $$ ts); wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vclosed (Vconstr name us)
[PROOF STEP]
hence "linear pat"
[PROOF STATE]
proof (prove)
using this:
vwellformed (Vabs cs \<Gamma>')

goal (1 subgoal):
 1. linear pat
[PROOF STEP]
using \<open>(pat, rhs) \<in> set cs\<close>
[PROOF STATE]
proof (prove)
using this:
vwellformed (Vabs cs \<Gamma>')
(pat, rhs) \<in> set cs

goal (1 subgoal):
 1. linear pat
[PROOF STEP]
by (auto simp: list_all_iff)
[PROOF STATE]
proof (state)
this:
linear pat

goal (6 subgoals):
 1. \<And>name \<Gamma> val. \<lbrakk>name |\<notin>| C; fmlookup \<Gamma> name = Some val; closed_except (Sconst name) (fmdom \<Gamma>); closed_venv \<Gamma>; pre_strong_term_class.wellformed (Sconst name); wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vclosed val
 2. \<And>\<Gamma> name val. \<lbrakk>fmlookup \<Gamma> name = Some val; closed_except (Svar name) (fmdom \<Gamma>); closed_venv \<Gamma>; pre_strong_term_class.wellformed (Svar name); wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vclosed val
 3. \<And>\<Gamma> cs. \<lbrakk>closed_except (Sabs cs) (fmdom \<Gamma>); closed_venv \<Gamma>; pre_strong_term_class.wellformed (Sabs cs); wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vclosed (Vabs cs \<Gamma>)
 4. \<And>\<Gamma> t cs \<Gamma>' u u' env uu_ rhs val. \<lbrakk>\<Gamma> \<turnstile>\<^sub>v t \<down> Vabs cs \<Gamma>'; \<lbrakk>closed_except t (fmdom \<Gamma>); closed_venv \<Gamma>; pre_strong_term_class.wellformed t; wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vclosed (Vabs cs \<Gamma>'); \<Gamma> \<turnstile>\<^sub>v u \<down> u'; \<lbrakk>closed_except u (fmdom \<Gamma>); closed_venv \<Gamma>; pre_strong_term_class.wellformed u; wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vclosed u'; vfind_match cs u' = Some (env, uu_, rhs); \<Gamma>' ++\<^sub>f env \<turnstile>\<^sub>v rhs \<down> val; \<lbrakk>closed_except rhs (fmdom (\<Gamma>' ++\<^sub>f env)); closed_venv (\<Gamma>' ++\<^sub>f env); pre_strong_term_class.wellformed rhs; wellformed_venv (\<Gamma>' ++\<^sub>f env)\<rbrakk> \<Longrightarrow> vclosed val; closed_except (t $\<^sub>s u) (fmdom \<Gamma>); closed_venv \<Gamma>; pre_strong_term_class.wellformed (t $\<^sub>s u); wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vclosed val
 5. \<And>\<Gamma> t css name \<Gamma>' cs u u' env uv_ rhs val. \<lbrakk>\<Gamma> \<turnstile>\<^sub>v t \<down> Vrecabs css name \<Gamma>'; \<lbrakk>closed_except t (fmdom \<Gamma>); closed_venv \<Gamma>; pre_strong_term_class.wellformed t; wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vclosed (Vrecabs css name \<Gamma>'); fmlookup css name = Some cs; \<Gamma> \<turnstile>\<^sub>v u \<down> u'; \<lbrakk>closed_except u (fmdom \<Gamma>); closed_venv \<Gamma>; pre_strong_term_class.wellformed u; wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vclosed u'; vfind_match cs u' = Some (env, uv_, rhs); \<Gamma>' ++\<^sub>f mk_rec_env css \<Gamma>' ++\<^sub>f env \<turnstile>\<^sub>v rhs \<down> val; \<lbrakk>closed_except rhs (fmdom (\<Gamma>' ++\<^sub>f mk_rec_env css \<Gamma>' ++\<^sub>f env)); closed_venv (\<Gamma>' ++\<^sub>f mk_rec_env css \<Gamma>' ++\<^sub>f env); pre_strong_term_class.wellformed rhs; wellformed_venv (\<Gamma>' ++\<^sub>f mk_rec_env css \<Gamma>' ++\<^sub>f env)\<rbrakk> \<Longrightarrow> vclosed val; closed_except (t $\<^sub>s u) (fmdom \<Gamma>); closed_venv \<Gamma>; pre_strong_term_class.wellformed (t $\<^sub>s u); wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vclosed val
 6. \<And>name \<Gamma> ts us. \<lbrakk>name |\<in>| C; list_all2 (\<lambda>x1 x2. \<Gamma> \<turnstile>\<^sub>v x1 \<down> x2 \<and> (closed_except x1 (fmdom \<Gamma>) \<longrightarrow> closed_venv \<Gamma> \<longrightarrow> pre_strong_term_class.wellformed x1 \<longrightarrow> wellformed_venv \<Gamma> \<longrightarrow> vclosed x2)) ts us; closed_except (name $$ ts) (fmdom \<Gamma>); closed_venv \<Gamma>; pre_strong_term_class.wellformed (name $$ ts); wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vclosed (Vconstr name us)
[PROOF STEP]
hence "fmdom env = frees pat"
[PROOF STATE]
proof (prove)
using this:
linear pat

goal (1 subgoal):
 1. fmdom env = frees pat
[PROOF STEP]
unfolding \<open>fmdom env = _\<close>
[PROOF STATE]
proof (prove)
using this:
linear pat

goal (1 subgoal):
 1. patvars (mk_pat pat) = frees pat
[PROOF STEP]
by (simp add: mk_pat_frees)
[PROOF STATE]
proof (state)
this:
fmdom env = frees pat

goal (6 subgoals):
 1. \<And>name \<Gamma> val. \<lbrakk>name |\<notin>| C; fmlookup \<Gamma> name = Some val; closed_except (Sconst name) (fmdom \<Gamma>); closed_venv \<Gamma>; pre_strong_term_class.wellformed (Sconst name); wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vclosed val
 2. \<And>\<Gamma> name val. \<lbrakk>fmlookup \<Gamma> name = Some val; closed_except (Svar name) (fmdom \<Gamma>); closed_venv \<Gamma>; pre_strong_term_class.wellformed (Svar name); wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vclosed val
 3. \<And>\<Gamma> cs. \<lbrakk>closed_except (Sabs cs) (fmdom \<Gamma>); closed_venv \<Gamma>; pre_strong_term_class.wellformed (Sabs cs); wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vclosed (Vabs cs \<Gamma>)
 4. \<And>\<Gamma> t cs \<Gamma>' u u' env uu_ rhs val. \<lbrakk>\<Gamma> \<turnstile>\<^sub>v t \<down> Vabs cs \<Gamma>'; \<lbrakk>closed_except t (fmdom \<Gamma>); closed_venv \<Gamma>; pre_strong_term_class.wellformed t; wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vclosed (Vabs cs \<Gamma>'); \<Gamma> \<turnstile>\<^sub>v u \<down> u'; \<lbrakk>closed_except u (fmdom \<Gamma>); closed_venv \<Gamma>; pre_strong_term_class.wellformed u; wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vclosed u'; vfind_match cs u' = Some (env, uu_, rhs); \<Gamma>' ++\<^sub>f env \<turnstile>\<^sub>v rhs \<down> val; \<lbrakk>closed_except rhs (fmdom (\<Gamma>' ++\<^sub>f env)); closed_venv (\<Gamma>' ++\<^sub>f env); pre_strong_term_class.wellformed rhs; wellformed_venv (\<Gamma>' ++\<^sub>f env)\<rbrakk> \<Longrightarrow> vclosed val; closed_except (t $\<^sub>s u) (fmdom \<Gamma>); closed_venv \<Gamma>; pre_strong_term_class.wellformed (t $\<^sub>s u); wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vclosed val
 5. \<And>\<Gamma> t css name \<Gamma>' cs u u' env uv_ rhs val. \<lbrakk>\<Gamma> \<turnstile>\<^sub>v t \<down> Vrecabs css name \<Gamma>'; \<lbrakk>closed_except t (fmdom \<Gamma>); closed_venv \<Gamma>; pre_strong_term_class.wellformed t; wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vclosed (Vrecabs css name \<Gamma>'); fmlookup css name = Some cs; \<Gamma> \<turnstile>\<^sub>v u \<down> u'; \<lbrakk>closed_except u (fmdom \<Gamma>); closed_venv \<Gamma>; pre_strong_term_class.wellformed u; wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vclosed u'; vfind_match cs u' = Some (env, uv_, rhs); \<Gamma>' ++\<^sub>f mk_rec_env css \<Gamma>' ++\<^sub>f env \<turnstile>\<^sub>v rhs \<down> val; \<lbrakk>closed_except rhs (fmdom (\<Gamma>' ++\<^sub>f mk_rec_env css \<Gamma>' ++\<^sub>f env)); closed_venv (\<Gamma>' ++\<^sub>f mk_rec_env css \<Gamma>' ++\<^sub>f env); pre_strong_term_class.wellformed rhs; wellformed_venv (\<Gamma>' ++\<^sub>f mk_rec_env css \<Gamma>' ++\<^sub>f env)\<rbrakk> \<Longrightarrow> vclosed val; closed_except (t $\<^sub>s u) (fmdom \<Gamma>); closed_venv \<Gamma>; pre_strong_term_class.wellformed (t $\<^sub>s u); wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vclosed val
 6. \<And>name \<Gamma> ts us. \<lbrakk>name |\<in>| C; list_all2 (\<lambda>x1 x2. \<Gamma> \<turnstile>\<^sub>v x1 \<down> x2 \<and> (closed_except x1 (fmdom \<Gamma>) \<longrightarrow> closed_venv \<Gamma> \<longrightarrow> pre_strong_term_class.wellformed x1 \<longrightarrow> wellformed_venv \<Gamma> \<longrightarrow> vclosed x2)) ts us; closed_except (name $$ ts) (fmdom \<Gamma>); closed_venv \<Gamma>; pre_strong_term_class.wellformed (name $$ ts); wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vclosed (Vconstr name us)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vclosed val
[PROOF STEP]
proof (rule comb)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. closed_except rhs (fmdom (\<Gamma>' ++\<^sub>f env))
 2. closed_venv (\<Gamma>' ++\<^sub>f env)
 3. pre_strong_term_class.wellformed rhs
 4. wellformed_venv (\<Gamma>' ++\<^sub>f env)
[PROOF STEP]
show "wellformed rhs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pre_strong_term_class.wellformed rhs
[PROOF STEP]
using \<open>(pat, rhs) \<in> set cs\<close> \<open>vwellformed (Vabs cs \<Gamma>')\<close>
[PROOF STATE]
proof (prove)
using this:
(pat, rhs) \<in> set cs
vwellformed (Vabs cs \<Gamma>')

goal (1 subgoal):
 1. pre_strong_term_class.wellformed rhs
[PROOF STEP]
by (auto simp: list_all_iff)
[PROOF STATE]
proof (state)
this:
pre_strong_term_class.wellformed rhs

goal (3 subgoals):
 1. closed_except rhs (fmdom (\<Gamma>' ++\<^sub>f env))
 2. closed_venv (\<Gamma>' ++\<^sub>f env)
 3. wellformed_venv (\<Gamma>' ++\<^sub>f env)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. closed_except rhs (fmdom (\<Gamma>' ++\<^sub>f env))
 2. closed_venv (\<Gamma>' ++\<^sub>f env)
 3. wellformed_venv (\<Gamma>' ++\<^sub>f env)
[PROOF STEP]
show "closed_venv (\<Gamma>' ++\<^sub>f env)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. closed_venv (\<Gamma>' ++\<^sub>f env)
[PROOF STEP]
apply rule
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. closed_venv \<Gamma>'
 2. closed_venv env
[PROOF STEP]
using \<open>vclosed (Vabs cs \<Gamma>')\<close>
[PROOF STATE]
proof (prove)
using this:
vclosed (Vabs cs \<Gamma>')

goal (2 subgoals):
 1. closed_venv \<Gamma>'
 2. closed_venv env
[PROOF STEP]
apply auto[]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. closed_venv env
[PROOF STEP]
apply (rule vclosed.vmatch_env)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. vmatch ?pat6 ?v6 = Some env
 2. vclosed ?v6
[PROOF STEP]
apply (rule vfind_match_elem)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. vfind_match ?cs9 ?v6 = Some (env, ?pat9, ?rhs9)
 2. vclosed ?v6
[PROOF STEP]
using comb
[PROOF STATE]
proof (prove)
using this:
\<Gamma> \<turnstile>\<^sub>v t \<down> Vabs cs \<Gamma>'
\<Gamma> \<turnstile>\<^sub>v u \<down> u'
vfind_match cs u' = Some (env, pat, rhs)
\<Gamma>' ++\<^sub>f env \<turnstile>\<^sub>v rhs \<down> val
\<lbrakk>closed_except t (fmdom \<Gamma>); closed_venv \<Gamma>; pre_strong_term_class.wellformed t; wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vclosed (Vabs cs \<Gamma>')
\<lbrakk>closed_except u (fmdom \<Gamma>); closed_venv \<Gamma>; pre_strong_term_class.wellformed u; wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vclosed u'
\<lbrakk>closed_except rhs (fmdom (\<Gamma>' ++\<^sub>f env)); closed_venv (\<Gamma>' ++\<^sub>f env); pre_strong_term_class.wellformed rhs; wellformed_venv (\<Gamma>' ++\<^sub>f env)\<rbrakk> \<Longrightarrow> vclosed val
closed_except (t $\<^sub>s u) (fmdom \<Gamma>)
closed_venv \<Gamma>
pre_strong_term_class.wellformed (t $\<^sub>s u)
wellformed_venv \<Gamma>

goal (2 subgoals):
 1. vfind_match ?cs9 ?v6 = Some (env, ?pat9, ?rhs9)
 2. vclosed ?v6
[PROOF STEP]
by (auto simp: closed_except_def)
[PROOF STATE]
proof (state)
this:
closed_venv (\<Gamma>' ++\<^sub>f env)

goal (2 subgoals):
 1. closed_except rhs (fmdom (\<Gamma>' ++\<^sub>f env))
 2. wellformed_venv (\<Gamma>' ++\<^sub>f env)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. closed_except rhs (fmdom (\<Gamma>' ++\<^sub>f env))
 2. wellformed_venv (\<Gamma>' ++\<^sub>f env)
[PROOF STEP]
show "closed_except rhs (fmdom (\<Gamma>' ++\<^sub>f env))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. closed_except rhs (fmdom (\<Gamma>' ++\<^sub>f env))
[PROOF STEP]
using \<open>vclosed (Vabs cs \<Gamma>')\<close> \<open>fmdom env = frees pat\<close> \<open>(pat, rhs) \<in> set cs\<close>
[PROOF STATE]
proof (prove)
using this:
vclosed (Vabs cs \<Gamma>')
fmdom env = frees pat
(pat, rhs) \<in> set cs

goal (1 subgoal):
 1. closed_except rhs (fmdom (\<Gamma>' ++\<^sub>f env))
[PROOF STEP]
by (auto simp: list_all_iff)
[PROOF STATE]
proof (state)
this:
closed_except rhs (fmdom (\<Gamma>' ++\<^sub>f env))

goal (1 subgoal):
 1. wellformed_venv (\<Gamma>' ++\<^sub>f env)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. wellformed_venv (\<Gamma>' ++\<^sub>f env)
[PROOF STEP]
show "wellformed_venv (\<Gamma>' ++\<^sub>f env)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wellformed_venv (\<Gamma>' ++\<^sub>f env)
[PROOF STEP]
apply rule
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. wellformed_venv \<Gamma>'
 2. wellformed_venv env
[PROOF STEP]
using \<open>vwellformed (Vabs cs \<Gamma>')\<close>
[PROOF STATE]
proof (prove)
using this:
vwellformed (Vabs cs \<Gamma>')

goal (2 subgoals):
 1. wellformed_venv \<Gamma>'
 2. wellformed_venv env
[PROOF STEP]
apply auto[]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wellformed_venv env
[PROOF STEP]
apply (rule vwellformed.vmatch_env)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. vmatch ?pat6 ?v6 = Some env
 2. vwellformed ?v6
[PROOF STEP]
apply (rule vfind_match_elem)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. vfind_match ?cs9 ?v6 = Some (env, ?pat9, ?rhs9)
 2. vwellformed ?v6
[PROOF STEP]
apply fact
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vwellformed u'
[PROOF STEP]
apply (rule veval'_wellformed)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. ?\<Gamma>12 \<turnstile>\<^sub>v ?t12 \<down> u'
 2. pre_strong_term_class.wellformed ?t12
 3. wellformed_venv ?\<Gamma>12
[PROOF STEP]
using comb
[PROOF STATE]
proof (prove)
using this:
\<Gamma> \<turnstile>\<^sub>v t \<down> Vabs cs \<Gamma>'
\<Gamma> \<turnstile>\<^sub>v u \<down> u'
vfind_match cs u' = Some (env, pat, rhs)
\<Gamma>' ++\<^sub>f env \<turnstile>\<^sub>v rhs \<down> val
\<lbrakk>closed_except t (fmdom \<Gamma>); closed_venv \<Gamma>; pre_strong_term_class.wellformed t; wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vclosed (Vabs cs \<Gamma>')
\<lbrakk>closed_except u (fmdom \<Gamma>); closed_venv \<Gamma>; pre_strong_term_class.wellformed u; wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vclosed u'
\<lbrakk>closed_except rhs (fmdom (\<Gamma>' ++\<^sub>f env)); closed_venv (\<Gamma>' ++\<^sub>f env); pre_strong_term_class.wellformed rhs; wellformed_venv (\<Gamma>' ++\<^sub>f env)\<rbrakk> \<Longrightarrow> vclosed val
closed_except (t $\<^sub>s u) (fmdom \<Gamma>)
closed_venv \<Gamma>
pre_strong_term_class.wellformed (t $\<^sub>s u)
wellformed_venv \<Gamma>

goal (3 subgoals):
 1. ?\<Gamma>12 \<turnstile>\<^sub>v ?t12 \<down> u'
 2. pre_strong_term_class.wellformed ?t12
 3. wellformed_venv ?\<Gamma>12
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
wellformed_venv (\<Gamma>' ++\<^sub>f env)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
vclosed val

goal (5 subgoals):
 1. \<And>name \<Gamma> val. \<lbrakk>name |\<notin>| C; fmlookup \<Gamma> name = Some val; closed_except (Sconst name) (fmdom \<Gamma>); closed_venv \<Gamma>; pre_strong_term_class.wellformed (Sconst name); wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vclosed val
 2. \<And>\<Gamma> name val. \<lbrakk>fmlookup \<Gamma> name = Some val; closed_except (Svar name) (fmdom \<Gamma>); closed_venv \<Gamma>; pre_strong_term_class.wellformed (Svar name); wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vclosed val
 3. \<And>\<Gamma> cs. \<lbrakk>closed_except (Sabs cs) (fmdom \<Gamma>); closed_venv \<Gamma>; pre_strong_term_class.wellformed (Sabs cs); wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vclosed (Vabs cs \<Gamma>)
 4. \<And>\<Gamma> t css name \<Gamma>' cs u u' env uv_ rhs val. \<lbrakk>\<Gamma> \<turnstile>\<^sub>v t \<down> Vrecabs css name \<Gamma>'; \<lbrakk>closed_except t (fmdom \<Gamma>); closed_venv \<Gamma>; pre_strong_term_class.wellformed t; wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vclosed (Vrecabs css name \<Gamma>'); fmlookup css name = Some cs; \<Gamma> \<turnstile>\<^sub>v u \<down> u'; \<lbrakk>closed_except u (fmdom \<Gamma>); closed_venv \<Gamma>; pre_strong_term_class.wellformed u; wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vclosed u'; vfind_match cs u' = Some (env, uv_, rhs); \<Gamma>' ++\<^sub>f mk_rec_env css \<Gamma>' ++\<^sub>f env \<turnstile>\<^sub>v rhs \<down> val; \<lbrakk>closed_except rhs (fmdom (\<Gamma>' ++\<^sub>f mk_rec_env css \<Gamma>' ++\<^sub>f env)); closed_venv (\<Gamma>' ++\<^sub>f mk_rec_env css \<Gamma>' ++\<^sub>f env); pre_strong_term_class.wellformed rhs; wellformed_venv (\<Gamma>' ++\<^sub>f mk_rec_env css \<Gamma>' ++\<^sub>f env)\<rbrakk> \<Longrightarrow> vclosed val; closed_except (t $\<^sub>s u) (fmdom \<Gamma>); closed_venv \<Gamma>; pre_strong_term_class.wellformed (t $\<^sub>s u); wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vclosed val
 5. \<And>name \<Gamma> ts us. \<lbrakk>name |\<in>| C; list_all2 (\<lambda>x1 x2. \<Gamma> \<turnstile>\<^sub>v x1 \<down> x2 \<and> (closed_except x1 (fmdom \<Gamma>) \<longrightarrow> closed_venv \<Gamma> \<longrightarrow> pre_strong_term_class.wellformed x1 \<longrightarrow> wellformed_venv \<Gamma> \<longrightarrow> vclosed x2)) ts us; closed_except (name $$ ts) (fmdom \<Gamma>); closed_venv \<Gamma>; pre_strong_term_class.wellformed (name $$ ts); wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vclosed (Vconstr name us)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>name \<Gamma> val. \<lbrakk>name |\<notin>| C; fmlookup \<Gamma> name = Some val; closed_except (Sconst name) (fmdom \<Gamma>); closed_venv \<Gamma>; pre_strong_term_class.wellformed (Sconst name); wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vclosed val
 2. \<And>\<Gamma> name val. \<lbrakk>fmlookup \<Gamma> name = Some val; closed_except (Svar name) (fmdom \<Gamma>); closed_venv \<Gamma>; pre_strong_term_class.wellformed (Svar name); wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vclosed val
 3. \<And>\<Gamma> cs. \<lbrakk>closed_except (Sabs cs) (fmdom \<Gamma>); closed_venv \<Gamma>; pre_strong_term_class.wellformed (Sabs cs); wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vclosed (Vabs cs \<Gamma>)
 4. \<And>\<Gamma> t css name \<Gamma>' cs u u' env uv_ rhs val. \<lbrakk>\<Gamma> \<turnstile>\<^sub>v t \<down> Vrecabs css name \<Gamma>'; \<lbrakk>closed_except t (fmdom \<Gamma>); closed_venv \<Gamma>; pre_strong_term_class.wellformed t; wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vclosed (Vrecabs css name \<Gamma>'); fmlookup css name = Some cs; \<Gamma> \<turnstile>\<^sub>v u \<down> u'; \<lbrakk>closed_except u (fmdom \<Gamma>); closed_venv \<Gamma>; pre_strong_term_class.wellformed u; wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vclosed u'; vfind_match cs u' = Some (env, uv_, rhs); \<Gamma>' ++\<^sub>f mk_rec_env css \<Gamma>' ++\<^sub>f env \<turnstile>\<^sub>v rhs \<down> val; \<lbrakk>closed_except rhs (fmdom (\<Gamma>' ++\<^sub>f mk_rec_env css \<Gamma>' ++\<^sub>f env)); closed_venv (\<Gamma>' ++\<^sub>f mk_rec_env css \<Gamma>' ++\<^sub>f env); pre_strong_term_class.wellformed rhs; wellformed_venv (\<Gamma>' ++\<^sub>f mk_rec_env css \<Gamma>' ++\<^sub>f env)\<rbrakk> \<Longrightarrow> vclosed val; closed_except (t $\<^sub>s u) (fmdom \<Gamma>); closed_venv \<Gamma>; pre_strong_term_class.wellformed (t $\<^sub>s u); wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vclosed val
 5. \<And>name \<Gamma> ts us. \<lbrakk>name |\<in>| C; list_all2 (\<lambda>x1 x2. \<Gamma> \<turnstile>\<^sub>v x1 \<down> x2 \<and> (closed_except x1 (fmdom \<Gamma>) \<longrightarrow> closed_venv \<Gamma> \<longrightarrow> pre_strong_term_class.wellformed x1 \<longrightarrow> wellformed_venv \<Gamma> \<longrightarrow> vclosed x2)) ts us; closed_except (name $$ ts) (fmdom \<Gamma>); closed_venv \<Gamma>; pre_strong_term_class.wellformed (name $$ ts); wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vclosed (Vconstr name us)
[PROOF STEP]
case (rec_comb \<Gamma> t css name \<Gamma>' cs u u' env pat rhs val)
[PROOF STATE]
proof (state)
this:
\<Gamma> \<turnstile>\<^sub>v t \<down> Vrecabs css name \<Gamma>'
fmlookup css name = Some cs
\<Gamma> \<turnstile>\<^sub>v u \<down> u'
vfind_match cs u' = Some (env, pat, rhs)
\<Gamma>' ++\<^sub>f mk_rec_env css \<Gamma>' ++\<^sub>f env \<turnstile>\<^sub>v rhs \<down> val
\<lbrakk>closed_except t (fmdom \<Gamma>); closed_venv \<Gamma>; pre_strong_term_class.wellformed t; wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vclosed (Vrecabs css name \<Gamma>')
\<lbrakk>closed_except u (fmdom \<Gamma>); closed_venv \<Gamma>; pre_strong_term_class.wellformed u; wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vclosed u'
\<lbrakk>closed_except rhs (fmdom (\<Gamma>' ++\<^sub>f mk_rec_env css \<Gamma>' ++\<^sub>f env)); closed_venv (\<Gamma>' ++\<^sub>f mk_rec_env css \<Gamma>' ++\<^sub>f env); pre_strong_term_class.wellformed rhs; wellformed_venv (\<Gamma>' ++\<^sub>f mk_rec_env css \<Gamma>' ++\<^sub>f env)\<rbrakk> \<Longrightarrow> vclosed val
closed_except (t $\<^sub>s u) (fmdom \<Gamma>)
closed_venv \<Gamma>
pre_strong_term_class.wellformed (t $\<^sub>s u)
wellformed_venv \<Gamma>

goal (5 subgoals):
 1. \<And>name \<Gamma> val. \<lbrakk>name |\<notin>| C; fmlookup \<Gamma> name = Some val; closed_except (Sconst name) (fmdom \<Gamma>); closed_venv \<Gamma>; pre_strong_term_class.wellformed (Sconst name); wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vclosed val
 2. \<And>\<Gamma> name val. \<lbrakk>fmlookup \<Gamma> name = Some val; closed_except (Svar name) (fmdom \<Gamma>); closed_venv \<Gamma>; pre_strong_term_class.wellformed (Svar name); wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vclosed val
 3. \<And>\<Gamma> cs. \<lbrakk>closed_except (Sabs cs) (fmdom \<Gamma>); closed_venv \<Gamma>; pre_strong_term_class.wellformed (Sabs cs); wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vclosed (Vabs cs \<Gamma>)
 4. \<And>\<Gamma> t css name \<Gamma>' cs u u' env uv_ rhs val. \<lbrakk>\<Gamma> \<turnstile>\<^sub>v t \<down> Vrecabs css name \<Gamma>'; \<lbrakk>closed_except t (fmdom \<Gamma>); closed_venv \<Gamma>; pre_strong_term_class.wellformed t; wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vclosed (Vrecabs css name \<Gamma>'); fmlookup css name = Some cs; \<Gamma> \<turnstile>\<^sub>v u \<down> u'; \<lbrakk>closed_except u (fmdom \<Gamma>); closed_venv \<Gamma>; pre_strong_term_class.wellformed u; wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vclosed u'; vfind_match cs u' = Some (env, uv_, rhs); \<Gamma>' ++\<^sub>f mk_rec_env css \<Gamma>' ++\<^sub>f env \<turnstile>\<^sub>v rhs \<down> val; \<lbrakk>closed_except rhs (fmdom (\<Gamma>' ++\<^sub>f mk_rec_env css \<Gamma>' ++\<^sub>f env)); closed_venv (\<Gamma>' ++\<^sub>f mk_rec_env css \<Gamma>' ++\<^sub>f env); pre_strong_term_class.wellformed rhs; wellformed_venv (\<Gamma>' ++\<^sub>f mk_rec_env css \<Gamma>' ++\<^sub>f env)\<rbrakk> \<Longrightarrow> vclosed val; closed_except (t $\<^sub>s u) (fmdom \<Gamma>); closed_venv \<Gamma>; pre_strong_term_class.wellformed (t $\<^sub>s u); wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vclosed val
 5. \<And>name \<Gamma> ts us. \<lbrakk>name |\<in>| C; list_all2 (\<lambda>x1 x2. \<Gamma> \<turnstile>\<^sub>v x1 \<down> x2 \<and> (closed_except x1 (fmdom \<Gamma>) \<longrightarrow> closed_venv \<Gamma> \<longrightarrow> pre_strong_term_class.wellformed x1 \<longrightarrow> wellformed_venv \<Gamma> \<longrightarrow> vclosed x2)) ts us; closed_except (name $$ ts) (fmdom \<Gamma>); closed_venv \<Gamma>; pre_strong_term_class.wellformed (name $$ ts); wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vclosed (Vconstr name us)
[PROOF STEP]
have "(pat, rhs) \<in> set cs" "vmatch (mk_pat pat) u' = Some env"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (pat, rhs) \<in> set cs &&& vmatch (mk_pat pat) u' = Some env
[PROOF STEP]
by (rule vfind_match_elem; fact)+
[PROOF STATE]
proof (state)
this:
(pat, rhs) \<in> set cs
vmatch (mk_pat pat) u' = Some env

goal (5 subgoals):
 1. \<And>name \<Gamma> val. \<lbrakk>name |\<notin>| C; fmlookup \<Gamma> name = Some val; closed_except (Sconst name) (fmdom \<Gamma>); closed_venv \<Gamma>; pre_strong_term_class.wellformed (Sconst name); wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vclosed val
 2. \<And>\<Gamma> name val. \<lbrakk>fmlookup \<Gamma> name = Some val; closed_except (Svar name) (fmdom \<Gamma>); closed_venv \<Gamma>; pre_strong_term_class.wellformed (Svar name); wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vclosed val
 3. \<And>\<Gamma> cs. \<lbrakk>closed_except (Sabs cs) (fmdom \<Gamma>); closed_venv \<Gamma>; pre_strong_term_class.wellformed (Sabs cs); wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vclosed (Vabs cs \<Gamma>)
 4. \<And>\<Gamma> t css name \<Gamma>' cs u u' env uv_ rhs val. \<lbrakk>\<Gamma> \<turnstile>\<^sub>v t \<down> Vrecabs css name \<Gamma>'; \<lbrakk>closed_except t (fmdom \<Gamma>); closed_venv \<Gamma>; pre_strong_term_class.wellformed t; wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vclosed (Vrecabs css name \<Gamma>'); fmlookup css name = Some cs; \<Gamma> \<turnstile>\<^sub>v u \<down> u'; \<lbrakk>closed_except u (fmdom \<Gamma>); closed_venv \<Gamma>; pre_strong_term_class.wellformed u; wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vclosed u'; vfind_match cs u' = Some (env, uv_, rhs); \<Gamma>' ++\<^sub>f mk_rec_env css \<Gamma>' ++\<^sub>f env \<turnstile>\<^sub>v rhs \<down> val; \<lbrakk>closed_except rhs (fmdom (\<Gamma>' ++\<^sub>f mk_rec_env css \<Gamma>' ++\<^sub>f env)); closed_venv (\<Gamma>' ++\<^sub>f mk_rec_env css \<Gamma>' ++\<^sub>f env); pre_strong_term_class.wellformed rhs; wellformed_venv (\<Gamma>' ++\<^sub>f mk_rec_env css \<Gamma>' ++\<^sub>f env)\<rbrakk> \<Longrightarrow> vclosed val; closed_except (t $\<^sub>s u) (fmdom \<Gamma>); closed_venv \<Gamma>; pre_strong_term_class.wellformed (t $\<^sub>s u); wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vclosed val
 5. \<And>name \<Gamma> ts us. \<lbrakk>name |\<in>| C; list_all2 (\<lambda>x1 x2. \<Gamma> \<turnstile>\<^sub>v x1 \<down> x2 \<and> (closed_except x1 (fmdom \<Gamma>) \<longrightarrow> closed_venv \<Gamma> \<longrightarrow> pre_strong_term_class.wellformed x1 \<longrightarrow> wellformed_venv \<Gamma> \<longrightarrow> vclosed x2)) ts us; closed_except (name $$ ts) (fmdom \<Gamma>); closed_venv \<Gamma>; pre_strong_term_class.wellformed (name $$ ts); wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vclosed (Vconstr name us)
[PROOF STEP]
hence "fmdom env = patvars (mk_pat pat)"
[PROOF STATE]
proof (prove)
using this:
(pat, rhs) \<in> set cs
vmatch (mk_pat pat) u' = Some env

goal (1 subgoal):
 1. fmdom env = patvars (mk_pat pat)
[PROOF STEP]
by (simp add: vmatch_dom)
[PROOF STATE]
proof (state)
this:
fmdom env = patvars (mk_pat pat)

goal (5 subgoals):
 1. \<And>name \<Gamma> val. \<lbrakk>name |\<notin>| C; fmlookup \<Gamma> name = Some val; closed_except (Sconst name) (fmdom \<Gamma>); closed_venv \<Gamma>; pre_strong_term_class.wellformed (Sconst name); wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vclosed val
 2. \<And>\<Gamma> name val. \<lbrakk>fmlookup \<Gamma> name = Some val; closed_except (Svar name) (fmdom \<Gamma>); closed_venv \<Gamma>; pre_strong_term_class.wellformed (Svar name); wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vclosed val
 3. \<And>\<Gamma> cs. \<lbrakk>closed_except (Sabs cs) (fmdom \<Gamma>); closed_venv \<Gamma>; pre_strong_term_class.wellformed (Sabs cs); wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vclosed (Vabs cs \<Gamma>)
 4. \<And>\<Gamma> t css name \<Gamma>' cs u u' env uv_ rhs val. \<lbrakk>\<Gamma> \<turnstile>\<^sub>v t \<down> Vrecabs css name \<Gamma>'; \<lbrakk>closed_except t (fmdom \<Gamma>); closed_venv \<Gamma>; pre_strong_term_class.wellformed t; wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vclosed (Vrecabs css name \<Gamma>'); fmlookup css name = Some cs; \<Gamma> \<turnstile>\<^sub>v u \<down> u'; \<lbrakk>closed_except u (fmdom \<Gamma>); closed_venv \<Gamma>; pre_strong_term_class.wellformed u; wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vclosed u'; vfind_match cs u' = Some (env, uv_, rhs); \<Gamma>' ++\<^sub>f mk_rec_env css \<Gamma>' ++\<^sub>f env \<turnstile>\<^sub>v rhs \<down> val; \<lbrakk>closed_except rhs (fmdom (\<Gamma>' ++\<^sub>f mk_rec_env css \<Gamma>' ++\<^sub>f env)); closed_venv (\<Gamma>' ++\<^sub>f mk_rec_env css \<Gamma>' ++\<^sub>f env); pre_strong_term_class.wellformed rhs; wellformed_venv (\<Gamma>' ++\<^sub>f mk_rec_env css \<Gamma>' ++\<^sub>f env)\<rbrakk> \<Longrightarrow> vclosed val; closed_except (t $\<^sub>s u) (fmdom \<Gamma>); closed_venv \<Gamma>; pre_strong_term_class.wellformed (t $\<^sub>s u); wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vclosed val
 5. \<And>name \<Gamma> ts us. \<lbrakk>name |\<in>| C; list_all2 (\<lambda>x1 x2. \<Gamma> \<turnstile>\<^sub>v x1 \<down> x2 \<and> (closed_except x1 (fmdom \<Gamma>) \<longrightarrow> closed_venv \<Gamma> \<longrightarrow> pre_strong_term_class.wellformed x1 \<longrightarrow> wellformed_venv \<Gamma> \<longrightarrow> vclosed x2)) ts us; closed_except (name $$ ts) (fmdom \<Gamma>); closed_venv \<Gamma>; pre_strong_term_class.wellformed (name $$ ts); wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vclosed (Vconstr name us)
[PROOF STEP]
have "vwellformed (Vrecabs css name \<Gamma>')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vwellformed (Vrecabs css name \<Gamma>')
[PROOF STEP]
apply (rule veval'_wellformed)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. ?\<Gamma> \<turnstile>\<^sub>v ?t \<down> Vrecabs css name \<Gamma>'
 2. pre_strong_term_class.wellformed ?t
 3. wellformed_venv ?\<Gamma>
[PROOF STEP]
using rec_comb
[PROOF STATE]
proof (prove)
using this:
\<Gamma> \<turnstile>\<^sub>v t \<down> Vrecabs css name \<Gamma>'
fmlookup css name = Some cs
\<Gamma> \<turnstile>\<^sub>v u \<down> u'
vfind_match cs u' = Some (env, pat, rhs)
\<Gamma>' ++\<^sub>f mk_rec_env css \<Gamma>' ++\<^sub>f env \<turnstile>\<^sub>v rhs \<down> val
\<lbrakk>closed_except t (fmdom \<Gamma>); closed_venv \<Gamma>; pre_strong_term_class.wellformed t; wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vclosed (Vrecabs css name \<Gamma>')
\<lbrakk>closed_except u (fmdom \<Gamma>); closed_venv \<Gamma>; pre_strong_term_class.wellformed u; wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vclosed u'
\<lbrakk>closed_except rhs (fmdom (\<Gamma>' ++\<^sub>f mk_rec_env css \<Gamma>' ++\<^sub>f env)); closed_venv (\<Gamma>' ++\<^sub>f mk_rec_env css \<Gamma>' ++\<^sub>f env); pre_strong_term_class.wellformed rhs; wellformed_venv (\<Gamma>' ++\<^sub>f mk_rec_env css \<Gamma>' ++\<^sub>f env)\<rbrakk> \<Longrightarrow> vclosed val
closed_except (t $\<^sub>s u) (fmdom \<Gamma>)
closed_venv \<Gamma>
pre_strong_term_class.wellformed (t $\<^sub>s u)
wellformed_venv \<Gamma>

goal (3 subgoals):
 1. ?\<Gamma> \<turnstile>\<^sub>v ?t \<down> Vrecabs css name \<Gamma>'
 2. pre_strong_term_class.wellformed ?t
 3. wellformed_venv ?\<Gamma>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
vwellformed (Vrecabs css name \<Gamma>')

goal (5 subgoals):
 1. \<And>name \<Gamma> val. \<lbrakk>name |\<notin>| C; fmlookup \<Gamma> name = Some val; closed_except (Sconst name) (fmdom \<Gamma>); closed_venv \<Gamma>; pre_strong_term_class.wellformed (Sconst name); wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vclosed val
 2. \<And>\<Gamma> name val. \<lbrakk>fmlookup \<Gamma> name = Some val; closed_except (Svar name) (fmdom \<Gamma>); closed_venv \<Gamma>; pre_strong_term_class.wellformed (Svar name); wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vclosed val
 3. \<And>\<Gamma> cs. \<lbrakk>closed_except (Sabs cs) (fmdom \<Gamma>); closed_venv \<Gamma>; pre_strong_term_class.wellformed (Sabs cs); wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vclosed (Vabs cs \<Gamma>)
 4. \<And>\<Gamma> t css name \<Gamma>' cs u u' env uv_ rhs val. \<lbrakk>\<Gamma> \<turnstile>\<^sub>v t \<down> Vrecabs css name \<Gamma>'; \<lbrakk>closed_except t (fmdom \<Gamma>); closed_venv \<Gamma>; pre_strong_term_class.wellformed t; wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vclosed (Vrecabs css name \<Gamma>'); fmlookup css name = Some cs; \<Gamma> \<turnstile>\<^sub>v u \<down> u'; \<lbrakk>closed_except u (fmdom \<Gamma>); closed_venv \<Gamma>; pre_strong_term_class.wellformed u; wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vclosed u'; vfind_match cs u' = Some (env, uv_, rhs); \<Gamma>' ++\<^sub>f mk_rec_env css \<Gamma>' ++\<^sub>f env \<turnstile>\<^sub>v rhs \<down> val; \<lbrakk>closed_except rhs (fmdom (\<Gamma>' ++\<^sub>f mk_rec_env css \<Gamma>' ++\<^sub>f env)); closed_venv (\<Gamma>' ++\<^sub>f mk_rec_env css \<Gamma>' ++\<^sub>f env); pre_strong_term_class.wellformed rhs; wellformed_venv (\<Gamma>' ++\<^sub>f mk_rec_env css \<Gamma>' ++\<^sub>f env)\<rbrakk> \<Longrightarrow> vclosed val; closed_except (t $\<^sub>s u) (fmdom \<Gamma>); closed_venv \<Gamma>; pre_strong_term_class.wellformed (t $\<^sub>s u); wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vclosed val
 5. \<And>name \<Gamma> ts us. \<lbrakk>name |\<in>| C; list_all2 (\<lambda>x1 x2. \<Gamma> \<turnstile>\<^sub>v x1 \<down> x2 \<and> (closed_except x1 (fmdom \<Gamma>) \<longrightarrow> closed_venv \<Gamma> \<longrightarrow> pre_strong_term_class.wellformed x1 \<longrightarrow> wellformed_venv \<Gamma> \<longrightarrow> vclosed x2)) ts us; closed_except (name $$ ts) (fmdom \<Gamma>); closed_venv \<Gamma>; pre_strong_term_class.wellformed (name $$ ts); wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vclosed (Vconstr name us)
[PROOF STEP]
hence "wellformed_clauses cs"
[PROOF STATE]
proof (prove)
using this:
vwellformed (Vrecabs css name \<Gamma>')

goal (1 subgoal):
 1. wellformed_clauses cs
[PROOF STEP]
using rec_comb
[PROOF STATE]
proof (prove)
using this:
vwellformed (Vrecabs css name \<Gamma>')
\<Gamma> \<turnstile>\<^sub>v t \<down> Vrecabs css name \<Gamma>'
fmlookup css name = Some cs
\<Gamma> \<turnstile>\<^sub>v u \<down> u'
vfind_match cs u' = Some (env, pat, rhs)
\<Gamma>' ++\<^sub>f mk_rec_env css \<Gamma>' ++\<^sub>f env \<turnstile>\<^sub>v rhs \<down> val
\<lbrakk>closed_except t (fmdom \<Gamma>); closed_venv \<Gamma>; pre_strong_term_class.wellformed t; wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vclosed (Vrecabs css name \<Gamma>')
\<lbrakk>closed_except u (fmdom \<Gamma>); closed_venv \<Gamma>; pre_strong_term_class.wellformed u; wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vclosed u'
\<lbrakk>closed_except rhs (fmdom (\<Gamma>' ++\<^sub>f mk_rec_env css \<Gamma>' ++\<^sub>f env)); closed_venv (\<Gamma>' ++\<^sub>f mk_rec_env css \<Gamma>' ++\<^sub>f env); pre_strong_term_class.wellformed rhs; wellformed_venv (\<Gamma>' ++\<^sub>f mk_rec_env css \<Gamma>' ++\<^sub>f env)\<rbrakk> \<Longrightarrow> vclosed val
closed_except (t $\<^sub>s u) (fmdom \<Gamma>)
closed_venv \<Gamma>
pre_strong_term_class.wellformed (t $\<^sub>s u)
wellformed_venv \<Gamma>

goal (1 subgoal):
 1. wellformed_clauses cs
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
wellformed_clauses cs

goal (5 subgoals):
 1. \<And>name \<Gamma> val. \<lbrakk>name |\<notin>| C; fmlookup \<Gamma> name = Some val; closed_except (Sconst name) (fmdom \<Gamma>); closed_venv \<Gamma>; pre_strong_term_class.wellformed (Sconst name); wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vclosed val
 2. \<And>\<Gamma> name val. \<lbrakk>fmlookup \<Gamma> name = Some val; closed_except (Svar name) (fmdom \<Gamma>); closed_venv \<Gamma>; pre_strong_term_class.wellformed (Svar name); wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vclosed val
 3. \<And>\<Gamma> cs. \<lbrakk>closed_except (Sabs cs) (fmdom \<Gamma>); closed_venv \<Gamma>; pre_strong_term_class.wellformed (Sabs cs); wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vclosed (Vabs cs \<Gamma>)
 4. \<And>\<Gamma> t css name \<Gamma>' cs u u' env uv_ rhs val. \<lbrakk>\<Gamma> \<turnstile>\<^sub>v t \<down> Vrecabs css name \<Gamma>'; \<lbrakk>closed_except t (fmdom \<Gamma>); closed_venv \<Gamma>; pre_strong_term_class.wellformed t; wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vclosed (Vrecabs css name \<Gamma>'); fmlookup css name = Some cs; \<Gamma> \<turnstile>\<^sub>v u \<down> u'; \<lbrakk>closed_except u (fmdom \<Gamma>); closed_venv \<Gamma>; pre_strong_term_class.wellformed u; wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vclosed u'; vfind_match cs u' = Some (env, uv_, rhs); \<Gamma>' ++\<^sub>f mk_rec_env css \<Gamma>' ++\<^sub>f env \<turnstile>\<^sub>v rhs \<down> val; \<lbrakk>closed_except rhs (fmdom (\<Gamma>' ++\<^sub>f mk_rec_env css \<Gamma>' ++\<^sub>f env)); closed_venv (\<Gamma>' ++\<^sub>f mk_rec_env css \<Gamma>' ++\<^sub>f env); pre_strong_term_class.wellformed rhs; wellformed_venv (\<Gamma>' ++\<^sub>f mk_rec_env css \<Gamma>' ++\<^sub>f env)\<rbrakk> \<Longrightarrow> vclosed val; closed_except (t $\<^sub>s u) (fmdom \<Gamma>); closed_venv \<Gamma>; pre_strong_term_class.wellformed (t $\<^sub>s u); wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vclosed val
 5. \<And>name \<Gamma> ts us. \<lbrakk>name |\<in>| C; list_all2 (\<lambda>x1 x2. \<Gamma> \<turnstile>\<^sub>v x1 \<down> x2 \<and> (closed_except x1 (fmdom \<Gamma>) \<longrightarrow> closed_venv \<Gamma> \<longrightarrow> pre_strong_term_class.wellformed x1 \<longrightarrow> wellformed_venv \<Gamma> \<longrightarrow> vclosed x2)) ts us; closed_except (name $$ ts) (fmdom \<Gamma>); closed_venv \<Gamma>; pre_strong_term_class.wellformed (name $$ ts); wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vclosed (Vconstr name us)
[PROOF STEP]
hence "linear pat"
[PROOF STATE]
proof (prove)
using this:
wellformed_clauses cs

goal (1 subgoal):
 1. linear pat
[PROOF STEP]
using \<open>(pat, rhs) \<in> set cs\<close>
[PROOF STATE]
proof (prove)
using this:
wellformed_clauses cs
(pat, rhs) \<in> set cs

goal (1 subgoal):
 1. linear pat
[PROOF STEP]
by (auto simp: list_all_iff)
[PROOF STATE]
proof (state)
this:
linear pat

goal (5 subgoals):
 1. \<And>name \<Gamma> val. \<lbrakk>name |\<notin>| C; fmlookup \<Gamma> name = Some val; closed_except (Sconst name) (fmdom \<Gamma>); closed_venv \<Gamma>; pre_strong_term_class.wellformed (Sconst name); wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vclosed val
 2. \<And>\<Gamma> name val. \<lbrakk>fmlookup \<Gamma> name = Some val; closed_except (Svar name) (fmdom \<Gamma>); closed_venv \<Gamma>; pre_strong_term_class.wellformed (Svar name); wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vclosed val
 3. \<And>\<Gamma> cs. \<lbrakk>closed_except (Sabs cs) (fmdom \<Gamma>); closed_venv \<Gamma>; pre_strong_term_class.wellformed (Sabs cs); wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vclosed (Vabs cs \<Gamma>)
 4. \<And>\<Gamma> t css name \<Gamma>' cs u u' env uv_ rhs val. \<lbrakk>\<Gamma> \<turnstile>\<^sub>v t \<down> Vrecabs css name \<Gamma>'; \<lbrakk>closed_except t (fmdom \<Gamma>); closed_venv \<Gamma>; pre_strong_term_class.wellformed t; wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vclosed (Vrecabs css name \<Gamma>'); fmlookup css name = Some cs; \<Gamma> \<turnstile>\<^sub>v u \<down> u'; \<lbrakk>closed_except u (fmdom \<Gamma>); closed_venv \<Gamma>; pre_strong_term_class.wellformed u; wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vclosed u'; vfind_match cs u' = Some (env, uv_, rhs); \<Gamma>' ++\<^sub>f mk_rec_env css \<Gamma>' ++\<^sub>f env \<turnstile>\<^sub>v rhs \<down> val; \<lbrakk>closed_except rhs (fmdom (\<Gamma>' ++\<^sub>f mk_rec_env css \<Gamma>' ++\<^sub>f env)); closed_venv (\<Gamma>' ++\<^sub>f mk_rec_env css \<Gamma>' ++\<^sub>f env); pre_strong_term_class.wellformed rhs; wellformed_venv (\<Gamma>' ++\<^sub>f mk_rec_env css \<Gamma>' ++\<^sub>f env)\<rbrakk> \<Longrightarrow> vclosed val; closed_except (t $\<^sub>s u) (fmdom \<Gamma>); closed_venv \<Gamma>; pre_strong_term_class.wellformed (t $\<^sub>s u); wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vclosed val
 5. \<And>name \<Gamma> ts us. \<lbrakk>name |\<in>| C; list_all2 (\<lambda>x1 x2. \<Gamma> \<turnstile>\<^sub>v x1 \<down> x2 \<and> (closed_except x1 (fmdom \<Gamma>) \<longrightarrow> closed_venv \<Gamma> \<longrightarrow> pre_strong_term_class.wellformed x1 \<longrightarrow> wellformed_venv \<Gamma> \<longrightarrow> vclosed x2)) ts us; closed_except (name $$ ts) (fmdom \<Gamma>); closed_venv \<Gamma>; pre_strong_term_class.wellformed (name $$ ts); wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vclosed (Vconstr name us)
[PROOF STEP]
hence "fmdom env = frees pat"
[PROOF STATE]
proof (prove)
using this:
linear pat

goal (1 subgoal):
 1. fmdom env = frees pat
[PROOF STEP]
unfolding \<open>fmdom env = _\<close>
[PROOF STATE]
proof (prove)
using this:
linear pat

goal (1 subgoal):
 1. patvars (mk_pat pat) = frees pat
[PROOF STEP]
by (simp add: mk_pat_frees)
[PROOF STATE]
proof (state)
this:
fmdom env = frees pat

goal (5 subgoals):
 1. \<And>name \<Gamma> val. \<lbrakk>name |\<notin>| C; fmlookup \<Gamma> name = Some val; closed_except (Sconst name) (fmdom \<Gamma>); closed_venv \<Gamma>; pre_strong_term_class.wellformed (Sconst name); wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vclosed val
 2. \<And>\<Gamma> name val. \<lbrakk>fmlookup \<Gamma> name = Some val; closed_except (Svar name) (fmdom \<Gamma>); closed_venv \<Gamma>; pre_strong_term_class.wellformed (Svar name); wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vclosed val
 3. \<And>\<Gamma> cs. \<lbrakk>closed_except (Sabs cs) (fmdom \<Gamma>); closed_venv \<Gamma>; pre_strong_term_class.wellformed (Sabs cs); wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vclosed (Vabs cs \<Gamma>)
 4. \<And>\<Gamma> t css name \<Gamma>' cs u u' env uv_ rhs val. \<lbrakk>\<Gamma> \<turnstile>\<^sub>v t \<down> Vrecabs css name \<Gamma>'; \<lbrakk>closed_except t (fmdom \<Gamma>); closed_venv \<Gamma>; pre_strong_term_class.wellformed t; wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vclosed (Vrecabs css name \<Gamma>'); fmlookup css name = Some cs; \<Gamma> \<turnstile>\<^sub>v u \<down> u'; \<lbrakk>closed_except u (fmdom \<Gamma>); closed_venv \<Gamma>; pre_strong_term_class.wellformed u; wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vclosed u'; vfind_match cs u' = Some (env, uv_, rhs); \<Gamma>' ++\<^sub>f mk_rec_env css \<Gamma>' ++\<^sub>f env \<turnstile>\<^sub>v rhs \<down> val; \<lbrakk>closed_except rhs (fmdom (\<Gamma>' ++\<^sub>f mk_rec_env css \<Gamma>' ++\<^sub>f env)); closed_venv (\<Gamma>' ++\<^sub>f mk_rec_env css \<Gamma>' ++\<^sub>f env); pre_strong_term_class.wellformed rhs; wellformed_venv (\<Gamma>' ++\<^sub>f mk_rec_env css \<Gamma>' ++\<^sub>f env)\<rbrakk> \<Longrightarrow> vclosed val; closed_except (t $\<^sub>s u) (fmdom \<Gamma>); closed_venv \<Gamma>; pre_strong_term_class.wellformed (t $\<^sub>s u); wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vclosed val
 5. \<And>name \<Gamma> ts us. \<lbrakk>name |\<in>| C; list_all2 (\<lambda>x1 x2. \<Gamma> \<turnstile>\<^sub>v x1 \<down> x2 \<and> (closed_except x1 (fmdom \<Gamma>) \<longrightarrow> closed_venv \<Gamma> \<longrightarrow> pre_strong_term_class.wellformed x1 \<longrightarrow> wellformed_venv \<Gamma> \<longrightarrow> vclosed x2)) ts us; closed_except (name $$ ts) (fmdom \<Gamma>); closed_venv \<Gamma>; pre_strong_term_class.wellformed (name $$ ts); wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vclosed (Vconstr name us)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vclosed val
[PROOF STEP]
proof (rule rec_comb)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. closed_except rhs (fmdom (\<Gamma>' ++\<^sub>f mk_rec_env css \<Gamma>' ++\<^sub>f env))
 2. closed_venv (\<Gamma>' ++\<^sub>f mk_rec_env css \<Gamma>' ++\<^sub>f env)
 3. pre_strong_term_class.wellformed rhs
 4. wellformed_venv (\<Gamma>' ++\<^sub>f mk_rec_env css \<Gamma>' ++\<^sub>f env)
[PROOF STEP]
show "closed_venv (\<Gamma>' ++\<^sub>f mk_rec_env css \<Gamma>' ++\<^sub>f env)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. closed_venv (\<Gamma>' ++\<^sub>f mk_rec_env css \<Gamma>' ++\<^sub>f env)
[PROOF STEP]
proof (intro fmpred_add)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. closed_venv \<Gamma>'
 2. closed_venv (mk_rec_env css \<Gamma>')
 3. closed_venv env
[PROOF STEP]
show "closed_venv \<Gamma>'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. closed_venv \<Gamma>'
[PROOF STEP]
using rec_comb
[PROOF STATE]
proof (prove)
using this:
\<Gamma> \<turnstile>\<^sub>v t \<down> Vrecabs css name \<Gamma>'
fmlookup css name = Some cs
\<Gamma> \<turnstile>\<^sub>v u \<down> u'
vfind_match cs u' = Some (env, pat, rhs)
\<Gamma>' ++\<^sub>f mk_rec_env css \<Gamma>' ++\<^sub>f env \<turnstile>\<^sub>v rhs \<down> val
\<lbrakk>closed_except t (fmdom \<Gamma>); closed_venv \<Gamma>; pre_strong_term_class.wellformed t; wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vclosed (Vrecabs css name \<Gamma>')
\<lbrakk>closed_except u (fmdom \<Gamma>); closed_venv \<Gamma>; pre_strong_term_class.wellformed u; wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vclosed u'
\<lbrakk>closed_except rhs (fmdom (\<Gamma>' ++\<^sub>f mk_rec_env css \<Gamma>' ++\<^sub>f env)); closed_venv (\<Gamma>' ++\<^sub>f mk_rec_env css \<Gamma>' ++\<^sub>f env); pre_strong_term_class.wellformed rhs; wellformed_venv (\<Gamma>' ++\<^sub>f mk_rec_env css \<Gamma>' ++\<^sub>f env)\<rbrakk> \<Longrightarrow> vclosed val
closed_except (t $\<^sub>s u) (fmdom \<Gamma>)
closed_venv \<Gamma>
pre_strong_term_class.wellformed (t $\<^sub>s u)
wellformed_venv \<Gamma>

goal (1 subgoal):
 1. closed_venv \<Gamma>'
[PROOF STEP]
by (auto simp: closed_except_def)
[PROOF STATE]
proof (state)
this:
closed_venv \<Gamma>'

goal (2 subgoals):
 1. closed_venv (mk_rec_env css \<Gamma>')
 2. closed_venv env
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. closed_venv (mk_rec_env css \<Gamma>')
 2. closed_venv env
[PROOF STEP]
show "closed_venv env"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. closed_venv env
[PROOF STEP]
using rec_comb
[PROOF STATE]
proof (prove)
using this:
\<Gamma> \<turnstile>\<^sub>v t \<down> Vrecabs css name \<Gamma>'
fmlookup css name = Some cs
\<Gamma> \<turnstile>\<^sub>v u \<down> u'
vfind_match cs u' = Some (env, pat, rhs)
\<Gamma>' ++\<^sub>f mk_rec_env css \<Gamma>' ++\<^sub>f env \<turnstile>\<^sub>v rhs \<down> val
\<lbrakk>closed_except t (fmdom \<Gamma>); closed_venv \<Gamma>; pre_strong_term_class.wellformed t; wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vclosed (Vrecabs css name \<Gamma>')
\<lbrakk>closed_except u (fmdom \<Gamma>); closed_venv \<Gamma>; pre_strong_term_class.wellformed u; wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vclosed u'
\<lbrakk>closed_except rhs (fmdom (\<Gamma>' ++\<^sub>f mk_rec_env css \<Gamma>' ++\<^sub>f env)); closed_venv (\<Gamma>' ++\<^sub>f mk_rec_env css \<Gamma>' ++\<^sub>f env); pre_strong_term_class.wellformed rhs; wellformed_venv (\<Gamma>' ++\<^sub>f mk_rec_env css \<Gamma>' ++\<^sub>f env)\<rbrakk> \<Longrightarrow> vclosed val
closed_except (t $\<^sub>s u) (fmdom \<Gamma>)
closed_venv \<Gamma>
pre_strong_term_class.wellformed (t $\<^sub>s u)
wellformed_venv \<Gamma>

goal (1 subgoal):
 1. closed_venv env
[PROOF STEP]
by (auto simp: closed_except_def dest: vfind_match_elem intro: vclosed.vmatch_env)
[PROOF STATE]
proof (state)
this:
closed_venv env

goal (1 subgoal):
 1. closed_venv (mk_rec_env css \<Gamma>')
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. closed_venv (mk_rec_env css \<Gamma>')
[PROOF STEP]
show "closed_venv (mk_rec_env css \<Gamma>')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. closed_venv (mk_rec_env css \<Gamma>')
[PROOF STEP]
unfolding mk_rec_env_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. closed_venv (fmmap_keys (\<lambda>name cs. Vrecabs css name \<Gamma>') css)
[PROOF STEP]
using rec_comb
[PROOF STATE]
proof (prove)
using this:
\<Gamma> \<turnstile>\<^sub>v t \<down> Vrecabs css name \<Gamma>'
fmlookup css name = Some cs
\<Gamma> \<turnstile>\<^sub>v u \<down> u'
vfind_match cs u' = Some (env, pat, rhs)
\<Gamma>' ++\<^sub>f mk_rec_env css \<Gamma>' ++\<^sub>f env \<turnstile>\<^sub>v rhs \<down> val
\<lbrakk>closed_except t (fmdom \<Gamma>); closed_venv \<Gamma>; pre_strong_term_class.wellformed t; wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vclosed (Vrecabs css name \<Gamma>')
\<lbrakk>closed_except u (fmdom \<Gamma>); closed_venv \<Gamma>; pre_strong_term_class.wellformed u; wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vclosed u'
\<lbrakk>closed_except rhs (fmdom (\<Gamma>' ++\<^sub>f mk_rec_env css \<Gamma>' ++\<^sub>f env)); closed_venv (\<Gamma>' ++\<^sub>f mk_rec_env css \<Gamma>' ++\<^sub>f env); pre_strong_term_class.wellformed rhs; wellformed_venv (\<Gamma>' ++\<^sub>f mk_rec_env css \<Gamma>' ++\<^sub>f env)\<rbrakk> \<Longrightarrow> vclosed val
closed_except (t $\<^sub>s u) (fmdom \<Gamma>)
closed_venv \<Gamma>
pre_strong_term_class.wellformed (t $\<^sub>s u)
wellformed_venv \<Gamma>

goal (1 subgoal):
 1. closed_venv (fmmap_keys (\<lambda>name cs. Vrecabs css name \<Gamma>') css)
[PROOF STEP]
by (auto simp: closed_except_def intro: fmdomI)
[PROOF STATE]
proof (state)
this:
closed_venv (mk_rec_env css \<Gamma>')

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
closed_venv (\<Gamma>' ++\<^sub>f mk_rec_env css \<Gamma>' ++\<^sub>f env)

goal (3 subgoals):
 1. closed_except rhs (fmdom (\<Gamma>' ++\<^sub>f mk_rec_env css \<Gamma>' ++\<^sub>f env))
 2. pre_strong_term_class.wellformed rhs
 3. wellformed_venv (\<Gamma>' ++\<^sub>f mk_rec_env css \<Gamma>' ++\<^sub>f env)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. closed_except rhs (fmdom (\<Gamma>' ++\<^sub>f mk_rec_env css \<Gamma>' ++\<^sub>f env))
 2. pre_strong_term_class.wellformed rhs
 3. wellformed_venv (\<Gamma>' ++\<^sub>f mk_rec_env css \<Gamma>' ++\<^sub>f env)
[PROOF STEP]
have "vclosed (Vrecabs css name \<Gamma>')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vclosed (Vrecabs css name \<Gamma>')
[PROOF STEP]
using mk_rec_env_def
[PROOF STATE]
proof (prove)
using this:
mk_rec_env ?css ?\<Gamma>' = fmmap_keys (\<lambda>name cs. Vrecabs ?css name ?\<Gamma>') ?css

goal (1 subgoal):
 1. vclosed (Vrecabs css name \<Gamma>')
[PROOF STEP]
using rec_comb
[PROOF STATE]
proof (prove)
using this:
mk_rec_env ?css ?\<Gamma>' = fmmap_keys (\<lambda>name cs. Vrecabs ?css name ?\<Gamma>') ?css
\<Gamma> \<turnstile>\<^sub>v t \<down> Vrecabs css name \<Gamma>'
fmlookup css name = Some cs
\<Gamma> \<turnstile>\<^sub>v u \<down> u'
vfind_match cs u' = Some (env, pat, rhs)
\<Gamma>' ++\<^sub>f mk_rec_env css \<Gamma>' ++\<^sub>f env \<turnstile>\<^sub>v rhs \<down> val
\<lbrakk>closed_except t (fmdom \<Gamma>); closed_venv \<Gamma>; pre_strong_term_class.wellformed t; wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vclosed (Vrecabs css name \<Gamma>')
\<lbrakk>closed_except u (fmdom \<Gamma>); closed_venv \<Gamma>; pre_strong_term_class.wellformed u; wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vclosed u'
\<lbrakk>closed_except rhs (fmdom (\<Gamma>' ++\<^sub>f mk_rec_env css \<Gamma>' ++\<^sub>f env)); closed_venv (\<Gamma>' ++\<^sub>f mk_rec_env css \<Gamma>' ++\<^sub>f env); pre_strong_term_class.wellformed rhs; wellformed_venv (\<Gamma>' ++\<^sub>f mk_rec_env css \<Gamma>' ++\<^sub>f env)\<rbrakk> \<Longrightarrow> vclosed val
closed_except (t $\<^sub>s u) (fmdom \<Gamma>)
closed_venv \<Gamma>
pre_strong_term_class.wellformed (t $\<^sub>s u)
wellformed_venv \<Gamma>

goal (1 subgoal):
 1. vclosed (Vrecabs css name \<Gamma>')
[PROOF STEP]
by (auto simp: closed_except_def intro: fmdom'I)
[PROOF STATE]
proof (state)
this:
vclosed (Vrecabs css name \<Gamma>')

goal (3 subgoals):
 1. closed_except rhs (fmdom (\<Gamma>' ++\<^sub>f mk_rec_env css \<Gamma>' ++\<^sub>f env))
 2. pre_strong_term_class.wellformed rhs
 3. wellformed_venv (\<Gamma>' ++\<^sub>f mk_rec_env css \<Gamma>' ++\<^sub>f env)
[PROOF STEP]
hence "closed_except rhs (fmdom \<Gamma>' |\<union>| frees pat)"
[PROOF STATE]
proof (prove)
using this:
vclosed (Vrecabs css name \<Gamma>')

goal (1 subgoal):
 1. closed_except rhs (fmdom \<Gamma>' |\<union>| frees pat)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. closed_venv \<Gamma>' \<and> fmpred (\<lambda>_. list_all (\<lambda>(pat, t). closed_except t (fmdom \<Gamma>' |\<union>| frees pat))) css \<and> name |\<in>| fmdom css \<Longrightarrow> closed_except rhs (fmdom \<Gamma>' |\<union>| frees pat)
[PROOF STEP]
apply (elim conjE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>closed_venv \<Gamma>'; fmpred (\<lambda>_. list_all (\<lambda>(pat, t). closed_except t (fmdom \<Gamma>' |\<union>| frees pat))) css; name |\<in>| fmdom css\<rbrakk> \<Longrightarrow> closed_except rhs (fmdom \<Gamma>' |\<union>| frees pat)
[PROOF STEP]
apply (drule fmpredD[where m = css])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>closed_venv \<Gamma>'; name |\<in>| fmdom css\<rbrakk> \<Longrightarrow> fmlookup css ?x3 = Some ?y3
 2. \<lbrakk>closed_venv \<Gamma>'; name |\<in>| fmdom css; list_all (\<lambda>(pat, t). closed_except t (fmdom \<Gamma>' |\<union>| frees pat)) ?y3\<rbrakk> \<Longrightarrow> closed_except rhs (fmdom \<Gamma>' |\<union>| frees pat)
[PROOF STEP]
apply (rule rec_comb)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>closed_venv \<Gamma>'; name |\<in>| fmdom css; list_all (\<lambda>(pat, t). closed_except t (fmdom \<Gamma>' |\<union>| frees pat)) cs\<rbrakk> \<Longrightarrow> closed_except rhs (fmdom \<Gamma>' |\<union>| frees pat)
[PROOF STEP]
using \<open>(pat, rhs) \<in> set cs\<close>
[PROOF STATE]
proof (prove)
using this:
(pat, rhs) \<in> set cs

goal (1 subgoal):
 1. \<lbrakk>closed_venv \<Gamma>'; name |\<in>| fmdom css; list_all (\<lambda>(pat, t). closed_except t (fmdom \<Gamma>' |\<union>| frees pat)) cs\<rbrakk> \<Longrightarrow> closed_except rhs (fmdom \<Gamma>' |\<union>| frees pat)
[PROOF STEP]
unfolding list_all_iff
[PROOF STATE]
proof (prove)
using this:
(pat, rhs) \<in> set cs

goal (1 subgoal):
 1. \<lbrakk>closed_venv \<Gamma>'; name |\<in>| fmdom css; \<forall>(pat, t)\<in>set cs. closed_except t (fmdom \<Gamma>' |\<union>| frees pat)\<rbrakk> \<Longrightarrow> closed_except rhs (fmdom \<Gamma>' |\<union>| frees pat)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
closed_except rhs (fmdom \<Gamma>' |\<union>| frees pat)

goal (3 subgoals):
 1. closed_except rhs (fmdom (\<Gamma>' ++\<^sub>f mk_rec_env css \<Gamma>' ++\<^sub>f env))
 2. pre_strong_term_class.wellformed rhs
 3. wellformed_venv (\<Gamma>' ++\<^sub>f mk_rec_env css \<Gamma>' ++\<^sub>f env)
[PROOF STEP]
thus "closed_except rhs (fmdom (\<Gamma>' ++\<^sub>f mk_rec_env css \<Gamma>' ++\<^sub>f env))"
[PROOF STATE]
proof (prove)
using this:
closed_except rhs (fmdom \<Gamma>' |\<union>| frees pat)

goal (1 subgoal):
 1. closed_except rhs (fmdom (\<Gamma>' ++\<^sub>f mk_rec_env css \<Gamma>' ++\<^sub>f env))
[PROOF STEP]
unfolding closed_except_def
[PROOF STATE]
proof (prove)
using this:
frees rhs |\<subseteq>| fmdom \<Gamma>' |\<union>| frees pat

goal (1 subgoal):
 1. frees rhs |\<subseteq>| fmdom (\<Gamma>' ++\<^sub>f mk_rec_env css \<Gamma>' ++\<^sub>f env)
[PROOF STEP]
using \<open>fmdom env = frees pat\<close>
[PROOF STATE]
proof (prove)
using this:
frees rhs |\<subseteq>| fmdom \<Gamma>' |\<union>| frees pat
fmdom env = frees pat

goal (1 subgoal):
 1. frees rhs |\<subseteq>| fmdom (\<Gamma>' ++\<^sub>f mk_rec_env css \<Gamma>' ++\<^sub>f env)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
closed_except rhs (fmdom (\<Gamma>' ++\<^sub>f mk_rec_env css \<Gamma>' ++\<^sub>f env))

goal (2 subgoals):
 1. pre_strong_term_class.wellformed rhs
 2. wellformed_venv (\<Gamma>' ++\<^sub>f mk_rec_env css \<Gamma>' ++\<^sub>f env)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. pre_strong_term_class.wellformed rhs
 2. wellformed_venv (\<Gamma>' ++\<^sub>f mk_rec_env css \<Gamma>' ++\<^sub>f env)
[PROOF STEP]
show "wellformed rhs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pre_strong_term_class.wellformed rhs
[PROOF STEP]
using \<open>wellformed_clauses cs\<close> \<open>(pat, rhs) \<in> set cs\<close>
[PROOF STATE]
proof (prove)
using this:
wellformed_clauses cs
(pat, rhs) \<in> set cs

goal (1 subgoal):
 1. pre_strong_term_class.wellformed rhs
[PROOF STEP]
by (auto simp: list_all_iff)
[PROOF STATE]
proof (state)
this:
pre_strong_term_class.wellformed rhs

goal (1 subgoal):
 1. wellformed_venv (\<Gamma>' ++\<^sub>f mk_rec_env css \<Gamma>' ++\<^sub>f env)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. wellformed_venv (\<Gamma>' ++\<^sub>f mk_rec_env css \<Gamma>' ++\<^sub>f env)
[PROOF STEP]
show "wellformed_venv (\<Gamma>' ++\<^sub>f mk_rec_env css \<Gamma>' ++\<^sub>f env)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wellformed_venv (\<Gamma>' ++\<^sub>f mk_rec_env css \<Gamma>' ++\<^sub>f env)
[PROOF STEP]
proof (intro fmpred_add)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. wellformed_venv \<Gamma>'
 2. wellformed_venv (mk_rec_env css \<Gamma>')
 3. wellformed_venv env
[PROOF STEP]
show "wellformed_venv \<Gamma>'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wellformed_venv \<Gamma>'
[PROOF STEP]
using \<open>vwellformed (Vrecabs css name \<Gamma>')\<close>
[PROOF STATE]
proof (prove)
using this:
vwellformed (Vrecabs css name \<Gamma>')

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

goal (2 subgoals):
 1. wellformed_venv (mk_rec_env css \<Gamma>')
 2. wellformed_venv env
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. wellformed_venv (mk_rec_env css \<Gamma>')
 2. wellformed_venv env
[PROOF STEP]
show "wellformed_venv env"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wellformed_venv env
[PROOF STEP]
using rec_comb
[PROOF STATE]
proof (prove)
using this:
\<Gamma> \<turnstile>\<^sub>v t \<down> Vrecabs css name \<Gamma>'
fmlookup css name = Some cs
\<Gamma> \<turnstile>\<^sub>v u \<down> u'
vfind_match cs u' = Some (env, pat, rhs)
\<Gamma>' ++\<^sub>f mk_rec_env css \<Gamma>' ++\<^sub>f env \<turnstile>\<^sub>v rhs \<down> val
\<lbrakk>closed_except t (fmdom \<Gamma>); closed_venv \<Gamma>; pre_strong_term_class.wellformed t; wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vclosed (Vrecabs css name \<Gamma>')
\<lbrakk>closed_except u (fmdom \<Gamma>); closed_venv \<Gamma>; pre_strong_term_class.wellformed u; wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vclosed u'
\<lbrakk>closed_except rhs (fmdom (\<Gamma>' ++\<^sub>f mk_rec_env css \<Gamma>' ++\<^sub>f env)); closed_venv (\<Gamma>' ++\<^sub>f mk_rec_env css \<Gamma>' ++\<^sub>f env); pre_strong_term_class.wellformed rhs; wellformed_venv (\<Gamma>' ++\<^sub>f mk_rec_env css \<Gamma>' ++\<^sub>f env)\<rbrakk> \<Longrightarrow> vclosed val
closed_except (t $\<^sub>s u) (fmdom \<Gamma>)
closed_venv \<Gamma>
pre_strong_term_class.wellformed (t $\<^sub>s u)
wellformed_venv \<Gamma>

goal (1 subgoal):
 1. wellformed_venv env
[PROOF STEP]
by (auto dest: vfind_match_elem intro: veval'_wellformed vwellformed.vmatch_env)
[PROOF STATE]
proof (state)
this:
wellformed_venv env

goal (1 subgoal):
 1. wellformed_venv (mk_rec_env css \<Gamma>')
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. wellformed_venv (mk_rec_env css \<Gamma>')
[PROOF STEP]
show "wellformed_venv (mk_rec_env css \<Gamma>')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wellformed_venv (mk_rec_env css \<Gamma>')
[PROOF STEP]
unfolding mk_rec_env_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wellformed_venv (fmmap_keys (\<lambda>name cs. Vrecabs css name \<Gamma>') css)
[PROOF STEP]
using \<open>vwellformed (Vrecabs css name \<Gamma>')\<close>
[PROOF STATE]
proof (prove)
using this:
vwellformed (Vrecabs css name \<Gamma>')

goal (1 subgoal):
 1. wellformed_venv (fmmap_keys (\<lambda>name cs. Vrecabs css name \<Gamma>') css)
[PROOF STEP]
by (auto intro: fmdomI)
[PROOF STATE]
proof (state)
this:
wellformed_venv (mk_rec_env css \<Gamma>')

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
wellformed_venv (\<Gamma>' ++\<^sub>f mk_rec_env css \<Gamma>' ++\<^sub>f env)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
vclosed val

goal (4 subgoals):
 1. \<And>name \<Gamma> val. \<lbrakk>name |\<notin>| C; fmlookup \<Gamma> name = Some val; closed_except (Sconst name) (fmdom \<Gamma>); closed_venv \<Gamma>; pre_strong_term_class.wellformed (Sconst name); wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vclosed val
 2. \<And>\<Gamma> name val. \<lbrakk>fmlookup \<Gamma> name = Some val; closed_except (Svar name) (fmdom \<Gamma>); closed_venv \<Gamma>; pre_strong_term_class.wellformed (Svar name); wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vclosed val
 3. \<And>\<Gamma> cs. \<lbrakk>closed_except (Sabs cs) (fmdom \<Gamma>); closed_venv \<Gamma>; pre_strong_term_class.wellformed (Sabs cs); wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vclosed (Vabs cs \<Gamma>)
 4. \<And>name \<Gamma> ts us. \<lbrakk>name |\<in>| C; list_all2 (\<lambda>x1 x2. \<Gamma> \<turnstile>\<^sub>v x1 \<down> x2 \<and> (closed_except x1 (fmdom \<Gamma>) \<longrightarrow> closed_venv \<Gamma> \<longrightarrow> pre_strong_term_class.wellformed x1 \<longrightarrow> wellformed_venv \<Gamma> \<longrightarrow> vclosed x2)) ts us; closed_except (name $$ ts) (fmdom \<Gamma>); closed_venv \<Gamma>; pre_strong_term_class.wellformed (name $$ ts); wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vclosed (Vconstr name us)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>name \<Gamma> val. \<lbrakk>name |\<notin>| C; fmlookup \<Gamma> name = Some val; closed_except (Sconst name) (fmdom \<Gamma>); closed_venv \<Gamma>; pre_strong_term_class.wellformed (Sconst name); wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vclosed val
 2. \<And>\<Gamma> name val. \<lbrakk>fmlookup \<Gamma> name = Some val; closed_except (Svar name) (fmdom \<Gamma>); closed_venv \<Gamma>; pre_strong_term_class.wellformed (Svar name); wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vclosed val
 3. \<And>\<Gamma> cs. \<lbrakk>closed_except (Sabs cs) (fmdom \<Gamma>); closed_venv \<Gamma>; pre_strong_term_class.wellformed (Sabs cs); wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vclosed (Vabs cs \<Gamma>)
 4. \<And>name \<Gamma> ts us. \<lbrakk>name |\<in>| C; list_all2 (\<lambda>x1 x2. \<Gamma> \<turnstile>\<^sub>v x1 \<down> x2 \<and> (closed_except x1 (fmdom \<Gamma>) \<longrightarrow> closed_venv \<Gamma> \<longrightarrow> pre_strong_term_class.wellformed x1 \<longrightarrow> wellformed_venv \<Gamma> \<longrightarrow> vclosed x2)) ts us; closed_except (name $$ ts) (fmdom \<Gamma>); closed_venv \<Gamma>; pre_strong_term_class.wellformed (name $$ ts); wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vclosed (Vconstr name us)
[PROOF STEP]
case (constr name \<Gamma> ts us)
[PROOF STATE]
proof (state)
this:
name |\<in>| C
list_all2 (\<lambda>x1 x2. \<Gamma> \<turnstile>\<^sub>v x1 \<down> x2 \<and> (closed_except x1 (fmdom \<Gamma>) \<longrightarrow> closed_venv \<Gamma> \<longrightarrow> pre_strong_term_class.wellformed x1 \<longrightarrow> wellformed_venv \<Gamma> \<longrightarrow> vclosed x2)) ts us
closed_except (name $$ ts) (fmdom \<Gamma>)
closed_venv \<Gamma>
pre_strong_term_class.wellformed (name $$ ts)
wellformed_venv \<Gamma>

goal (4 subgoals):
 1. \<And>name \<Gamma> val. \<lbrakk>name |\<notin>| C; fmlookup \<Gamma> name = Some val; closed_except (Sconst name) (fmdom \<Gamma>); closed_venv \<Gamma>; pre_strong_term_class.wellformed (Sconst name); wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vclosed val
 2. \<And>\<Gamma> name val. \<lbrakk>fmlookup \<Gamma> name = Some val; closed_except (Svar name) (fmdom \<Gamma>); closed_venv \<Gamma>; pre_strong_term_class.wellformed (Svar name); wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vclosed val
 3. \<And>\<Gamma> cs. \<lbrakk>closed_except (Sabs cs) (fmdom \<Gamma>); closed_venv \<Gamma>; pre_strong_term_class.wellformed (Sabs cs); wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vclosed (Vabs cs \<Gamma>)
 4. \<And>name \<Gamma> ts us. \<lbrakk>name |\<in>| C; list_all2 (\<lambda>x1 x2. \<Gamma> \<turnstile>\<^sub>v x1 \<down> x2 \<and> (closed_except x1 (fmdom \<Gamma>) \<longrightarrow> closed_venv \<Gamma> \<longrightarrow> pre_strong_term_class.wellformed x1 \<longrightarrow> wellformed_venv \<Gamma> \<longrightarrow> vclosed x2)) ts us; closed_except (name $$ ts) (fmdom \<Gamma>); closed_venv \<Gamma>; pre_strong_term_class.wellformed (name $$ ts); wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vclosed (Vconstr name us)
[PROOF STEP]
have "list_all vclosed us"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. list_all vclosed us
[PROOF STEP]
using \<open>list_all2 _ _ _\<close> \<open>closed_except (_ $$ _) _\<close> \<open>wellformed (_ $$ _)\<close>
[PROOF STATE]
proof (prove)
using this:
list_all2 (\<lambda>x1 x2. \<Gamma> \<turnstile>\<^sub>v x1 \<down> x2 \<and> (closed_except x1 (fmdom \<Gamma>) \<longrightarrow> closed_venv \<Gamma> \<longrightarrow> pre_strong_term_class.wellformed x1 \<longrightarrow> wellformed_venv \<Gamma> \<longrightarrow> vclosed x2)) ts us
closed_except (name $$ ts) (fmdom \<Gamma>)
pre_strong_term_class.wellformed (name $$ ts)

goal (1 subgoal):
 1. list_all vclosed us
[PROOF STEP]
proof (induction ts us rule: list.rel_induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>closed_except (name $$ []) (fmdom \<Gamma>); pre_strong_term_class.wellformed (name $$ [])\<rbrakk> \<Longrightarrow> list_all vclosed []
 2. \<And>a21 a22 b21 b22. \<lbrakk>\<Gamma> \<turnstile>\<^sub>v a21 \<down> b21 \<and> (closed_except a21 (fmdom \<Gamma>) \<longrightarrow> closed_venv \<Gamma> \<longrightarrow> pre_strong_term_class.wellformed a21 \<longrightarrow> wellformed_venv \<Gamma> \<longrightarrow> vclosed b21); \<lbrakk>closed_except (name $$ a22) (fmdom \<Gamma>); pre_strong_term_class.wellformed (name $$ a22)\<rbrakk> \<Longrightarrow> list_all vclosed b22; closed_except (name $$ (a21 # a22)) (fmdom \<Gamma>); pre_strong_term_class.wellformed (name $$ (a21 # a22))\<rbrakk> \<Longrightarrow> list_all vclosed (b21 # b22)
[PROOF STEP]
case (Cons v vs u us)
[PROOF STATE]
proof (state)
this:
\<Gamma> \<turnstile>\<^sub>v v \<down> u \<and> (closed_except v (fmdom \<Gamma>) \<longrightarrow> closed_venv \<Gamma> \<longrightarrow> pre_strong_term_class.wellformed v \<longrightarrow> wellformed_venv \<Gamma> \<longrightarrow> vclosed u)
\<lbrakk>closed_except (name $$ vs) (fmdom \<Gamma>); pre_strong_term_class.wellformed (name $$ vs)\<rbrakk> \<Longrightarrow> list_all vclosed us
closed_except (name $$ (v # vs)) (fmdom \<Gamma>)
pre_strong_term_class.wellformed (name $$ (v # vs))

goal (2 subgoals):
 1. \<lbrakk>closed_except (name $$ []) (fmdom \<Gamma>); pre_strong_term_class.wellformed (name $$ [])\<rbrakk> \<Longrightarrow> list_all vclosed []
 2. \<And>a21 a22 b21 b22. \<lbrakk>\<Gamma> \<turnstile>\<^sub>v a21 \<down> b21 \<and> (closed_except a21 (fmdom \<Gamma>) \<longrightarrow> closed_venv \<Gamma> \<longrightarrow> pre_strong_term_class.wellformed a21 \<longrightarrow> wellformed_venv \<Gamma> \<longrightarrow> vclosed b21); \<lbrakk>closed_except (name $$ a22) (fmdom \<Gamma>); pre_strong_term_class.wellformed (name $$ a22)\<rbrakk> \<Longrightarrow> list_all vclosed b22; closed_except (name $$ (a21 # a22)) (fmdom \<Gamma>); pre_strong_term_class.wellformed (name $$ (a21 # a22))\<rbrakk> \<Longrightarrow> list_all vclosed (b21 # b22)
[PROOF STEP]
with constr
[PROOF STATE]
proof (chain)
picking this:
name |\<in>| C
list_all2 (\<lambda>x1 x2. \<Gamma> \<turnstile>\<^sub>v x1 \<down> x2 \<and> (closed_except x1 (fmdom \<Gamma>) \<longrightarrow> closed_venv \<Gamma> \<longrightarrow> pre_strong_term_class.wellformed x1 \<longrightarrow> wellformed_venv \<Gamma> \<longrightarrow> vclosed x2)) ts us__
closed_except (name $$ ts) (fmdom \<Gamma>)
closed_venv \<Gamma>
pre_strong_term_class.wellformed (name $$ ts)
wellformed_venv \<Gamma>
\<Gamma> \<turnstile>\<^sub>v v \<down> u \<and> (closed_except v (fmdom \<Gamma>) \<longrightarrow> closed_venv \<Gamma> \<longrightarrow> pre_strong_term_class.wellformed v \<longrightarrow> wellformed_venv \<Gamma> \<longrightarrow> vclosed u)
\<lbrakk>closed_except (name $$ vs) (fmdom \<Gamma>); pre_strong_term_class.wellformed (name $$ vs)\<rbrakk> \<Longrightarrow> list_all vclosed us
closed_except (name $$ (v # vs)) (fmdom \<Gamma>)
pre_strong_term_class.wellformed (name $$ (v # vs))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
name |\<in>| C
list_all2 (\<lambda>x1 x2. \<Gamma> \<turnstile>\<^sub>v x1 \<down> x2 \<and> (closed_except x1 (fmdom \<Gamma>) \<longrightarrow> closed_venv \<Gamma> \<longrightarrow> pre_strong_term_class.wellformed x1 \<longrightarrow> wellformed_venv \<Gamma> \<longrightarrow> vclosed x2)) ts us__
closed_except (name $$ ts) (fmdom \<Gamma>)
closed_venv \<Gamma>
pre_strong_term_class.wellformed (name $$ ts)
wellformed_venv \<Gamma>
\<Gamma> \<turnstile>\<^sub>v v \<down> u \<and> (closed_except v (fmdom \<Gamma>) \<longrightarrow> closed_venv \<Gamma> \<longrightarrow> pre_strong_term_class.wellformed v \<longrightarrow> wellformed_venv \<Gamma> \<longrightarrow> vclosed u)
\<lbrakk>closed_except (name $$ vs) (fmdom \<Gamma>); pre_strong_term_class.wellformed (name $$ vs)\<rbrakk> \<Longrightarrow> list_all vclosed us
closed_except (name $$ (v # vs)) (fmdom \<Gamma>)
pre_strong_term_class.wellformed (name $$ (v # vs))

goal (1 subgoal):
 1. list_all vclosed (u # us)
[PROOF STEP]
unfolding closed.list_comb wellformed.list_comb
[PROOF STATE]
proof (prove)
using this:
name |\<in>| C
list_all2 (\<lambda>x1 x2. \<Gamma> \<turnstile>\<^sub>v x1 \<down> x2 \<and> (closed_except x1 (fmdom \<Gamma>) \<longrightarrow> closed_venv \<Gamma> \<longrightarrow> pre_strong_term_class.wellformed x1 \<longrightarrow> wellformed_venv \<Gamma> \<longrightarrow> vclosed x2)) ts us__
closed_except (const name) (fmdom \<Gamma>) \<and> list_all (\<lambda>t. closed_except t (fmdom \<Gamma>)) ts
closed_venv \<Gamma>
pre_strong_term_class.wellformed (const name) \<and> list_all pre_strong_term_class.wellformed ts
wellformed_venv \<Gamma>
\<Gamma> \<turnstile>\<^sub>v v \<down> u \<and> (closed_except v (fmdom \<Gamma>) \<longrightarrow> closed_venv \<Gamma> \<longrightarrow> pre_strong_term_class.wellformed v \<longrightarrow> wellformed_venv \<Gamma> \<longrightarrow> vclosed u)
\<lbrakk>closed_except (const name) (fmdom \<Gamma>) \<and> list_all (\<lambda>t. closed_except t (fmdom \<Gamma>)) vs; pre_strong_term_class.wellformed (const name) \<and> list_all pre_strong_term_class.wellformed vs\<rbrakk> \<Longrightarrow> list_all vclosed us
closed_except (const name) (fmdom \<Gamma>) \<and> list_all (\<lambda>t. closed_except t (fmdom \<Gamma>)) (v # vs)
pre_strong_term_class.wellformed (const name) \<and> list_all pre_strong_term_class.wellformed (v # vs)

goal (1 subgoal):
 1. list_all vclosed (u # us)
[PROOF STEP]
by (auto simp: Sterm.closed_except_simps)
[PROOF STATE]
proof (state)
this:
list_all vclosed (u # us)

goal (1 subgoal):
 1. \<lbrakk>closed_except (name $$ []) (fmdom \<Gamma>); pre_strong_term_class.wellformed (name $$ [])\<rbrakk> \<Longrightarrow> list_all vclosed []
[PROOF STEP]
qed simp
[PROOF STATE]
proof (state)
this:
list_all vclosed us

goal (4 subgoals):
 1. \<And>name \<Gamma> val. \<lbrakk>name |\<notin>| C; fmlookup \<Gamma> name = Some val; closed_except (Sconst name) (fmdom \<Gamma>); closed_venv \<Gamma>; pre_strong_term_class.wellformed (Sconst name); wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vclosed val
 2. \<And>\<Gamma> name val. \<lbrakk>fmlookup \<Gamma> name = Some val; closed_except (Svar name) (fmdom \<Gamma>); closed_venv \<Gamma>; pre_strong_term_class.wellformed (Svar name); wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vclosed val
 3. \<And>\<Gamma> cs. \<lbrakk>closed_except (Sabs cs) (fmdom \<Gamma>); closed_venv \<Gamma>; pre_strong_term_class.wellformed (Sabs cs); wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vclosed (Vabs cs \<Gamma>)
 4. \<And>name \<Gamma> ts us. \<lbrakk>name |\<in>| C; list_all2 (\<lambda>x1 x2. \<Gamma> \<turnstile>\<^sub>v x1 \<down> x2 \<and> (closed_except x1 (fmdom \<Gamma>) \<longrightarrow> closed_venv \<Gamma> \<longrightarrow> pre_strong_term_class.wellformed x1 \<longrightarrow> wellformed_venv \<Gamma> \<longrightarrow> vclosed x2)) ts us; closed_except (name $$ ts) (fmdom \<Gamma>); closed_venv \<Gamma>; pre_strong_term_class.wellformed (name $$ ts); wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vclosed (Vconstr name us)
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
list_all vclosed us

goal (1 subgoal):
 1. vclosed (Vconstr name us)
[PROOF STEP]
by (simp add: list_all_iff)
[PROOF STATE]
proof (state)
this:
vclosed (Vconstr name us)

goal (3 subgoals):
 1. \<And>name \<Gamma> val. \<lbrakk>name |\<notin>| C; fmlookup \<Gamma> name = Some val; closed_except (Sconst name) (fmdom \<Gamma>); closed_venv \<Gamma>; pre_strong_term_class.wellformed (Sconst name); wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vclosed val
 2. \<And>\<Gamma> name val. \<lbrakk>fmlookup \<Gamma> name = Some val; closed_except (Svar name) (fmdom \<Gamma>); closed_venv \<Gamma>; pre_strong_term_class.wellformed (Svar name); wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vclosed val
 3. \<And>\<Gamma> cs. \<lbrakk>closed_except (Sabs cs) (fmdom \<Gamma>); closed_venv \<Gamma>; pre_strong_term_class.wellformed (Sabs cs); wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vclosed (Vabs cs \<Gamma>)
[PROOF STEP]
qed (auto simp: Sterm.closed_except_simps)