[STATEMENT]
lemma veval'_correct':
  assumes "\<Gamma>\<^sub>2 \<turnstile>\<^sub>v t \<down> v\<^sub>2" "wellformed t" "wellformed_venv \<Gamma>\<^sub>2"
  assumes "\<not> shadows_consts t" "not_shadows_vconsts_env \<Gamma>\<^sub>2"
  assumes "welldefined t"
  assumes "closed t"
  assumes "fmrel_on_fset (consts t) vrelated (fmap_of_list rs) \<Gamma>\<^sub>2"
  obtains v\<^sub>1 where "rs, fmempty \<turnstile>\<^sub>v t \<down> v\<^sub>1" "\<turnstile>\<^sub>v v\<^sub>1 \<approx> v\<^sub>2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>v\<^sub>1. \<lbrakk>rs, fmempty \<turnstile>\<^sub>v t \<down> v\<^sub>1; \<turnstile>\<^sub>v v\<^sub>1 \<approx> v\<^sub>2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof (rule veval'_correct[where \<Gamma>\<^sub>1 = fmempty])
[PROOF STATE]
proof (state)
goal (10 subgoals):
 1. (\<And>v\<^sub>1. \<lbrakk>rs, fmempty \<turnstile>\<^sub>v t \<down> v\<^sub>1; \<turnstile>\<^sub>v v\<^sub>1 \<approx> v\<^sub>2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> ?\<Gamma>\<^sub>26 \<turnstile>\<^sub>v ?t6 \<down> ?v\<^sub>26
 2. (\<And>v\<^sub>1. \<lbrakk>rs, fmempty \<turnstile>\<^sub>v t \<down> v\<^sub>1; \<turnstile>\<^sub>v v\<^sub>1 \<approx> v\<^sub>2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> pre_strong_term_class.wellformed ?t6
 3. (\<And>v\<^sub>1. \<lbrakk>rs, fmempty \<turnstile>\<^sub>v t \<down> v\<^sub>1; \<turnstile>\<^sub>v v\<^sub>1 \<approx> v\<^sub>2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> wellformed_venv ?\<Gamma>\<^sub>26
 4. (\<And>v\<^sub>1. \<lbrakk>rs, fmempty \<turnstile>\<^sub>v t \<down> v\<^sub>1; \<turnstile>\<^sub>v v\<^sub>1 \<approx> v\<^sub>2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> \<not> shadows_consts ?t6
 5. (\<And>v\<^sub>1. \<lbrakk>rs, fmempty \<turnstile>\<^sub>v t \<down> v\<^sub>1; \<turnstile>\<^sub>v v\<^sub>1 \<approx> v\<^sub>2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> not_shadows_vconsts_env ?\<Gamma>\<^sub>26
 6. (\<And>v\<^sub>1. \<lbrakk>rs, fmempty \<turnstile>\<^sub>v t \<down> v\<^sub>1; \<turnstile>\<^sub>v v\<^sub>1 \<approx> v\<^sub>2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> consts ?t6 |\<subseteq>| all_consts
 7. (\<And>v\<^sub>1. \<lbrakk>rs, fmempty \<turnstile>\<^sub>v t \<down> v\<^sub>1; \<turnstile>\<^sub>v v\<^sub>1 \<approx> v\<^sub>2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> fmpred (\<lambda>_. vwelldefined) fmempty
 8. (\<And>v\<^sub>1. \<lbrakk>rs, fmempty \<turnstile>\<^sub>v t \<down> v\<^sub>1; \<turnstile>\<^sub>v v\<^sub>1 \<approx> v\<^sub>2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> fmrel_on_fset (frees ?t6) vrelated fmempty ?\<Gamma>\<^sub>26
 9. (\<And>v\<^sub>1. \<lbrakk>rs, fmempty \<turnstile>\<^sub>v t \<down> v\<^sub>1; \<turnstile>\<^sub>v v\<^sub>1 \<approx> v\<^sub>2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> fmrel_on_fset (consts ?t6) vrelated (fmap_of_list rs) ?\<Gamma>\<^sub>26
 10. \<And>v\<^sub>1. \<lbrakk>\<And>v\<^sub>1. \<lbrakk>rs, fmempty \<turnstile>\<^sub>v t \<down> v\<^sub>1; \<turnstile>\<^sub>v v\<^sub>1 \<approx> v\<^sub>2\<rbrakk> \<Longrightarrow> thesis; rs, fmempty \<turnstile>\<^sub>v ?t6 \<down> v\<^sub>1; \<turnstile>\<^sub>v v\<^sub>1 \<approx> ?v\<^sub>26\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
show "fmpred (\<lambda>_. vwelldefined) fmempty"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fmpred (\<lambda>_. vwelldefined) fmempty
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
fmpred (\<lambda>_. vwelldefined) fmempty

goal (9 subgoals):
 1. (\<And>v\<^sub>1. \<lbrakk>rs, fmempty \<turnstile>\<^sub>v t \<down> v\<^sub>1; \<turnstile>\<^sub>v v\<^sub>1 \<approx> v\<^sub>2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> ?\<Gamma>\<^sub>26 \<turnstile>\<^sub>v ?t6 \<down> ?v\<^sub>26
 2. (\<And>v\<^sub>1. \<lbrakk>rs, fmempty \<turnstile>\<^sub>v t \<down> v\<^sub>1; \<turnstile>\<^sub>v v\<^sub>1 \<approx> v\<^sub>2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> pre_strong_term_class.wellformed ?t6
 3. (\<And>v\<^sub>1. \<lbrakk>rs, fmempty \<turnstile>\<^sub>v t \<down> v\<^sub>1; \<turnstile>\<^sub>v v\<^sub>1 \<approx> v\<^sub>2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> wellformed_venv ?\<Gamma>\<^sub>26
 4. (\<And>v\<^sub>1. \<lbrakk>rs, fmempty \<turnstile>\<^sub>v t \<down> v\<^sub>1; \<turnstile>\<^sub>v v\<^sub>1 \<approx> v\<^sub>2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> \<not> shadows_consts ?t6
 5. (\<And>v\<^sub>1. \<lbrakk>rs, fmempty \<turnstile>\<^sub>v t \<down> v\<^sub>1; \<turnstile>\<^sub>v v\<^sub>1 \<approx> v\<^sub>2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> not_shadows_vconsts_env ?\<Gamma>\<^sub>26
 6. (\<And>v\<^sub>1. \<lbrakk>rs, fmempty \<turnstile>\<^sub>v t \<down> v\<^sub>1; \<turnstile>\<^sub>v v\<^sub>1 \<approx> v\<^sub>2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> consts ?t6 |\<subseteq>| all_consts
 7. (\<And>v\<^sub>1. \<lbrakk>rs, fmempty \<turnstile>\<^sub>v t \<down> v\<^sub>1; \<turnstile>\<^sub>v v\<^sub>1 \<approx> v\<^sub>2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> fmrel_on_fset (frees ?t6) vrelated fmempty ?\<Gamma>\<^sub>26
 8. (\<And>v\<^sub>1. \<lbrakk>rs, fmempty \<turnstile>\<^sub>v t \<down> v\<^sub>1; \<turnstile>\<^sub>v v\<^sub>1 \<approx> v\<^sub>2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> fmrel_on_fset (consts ?t6) vrelated (fmap_of_list rs) ?\<Gamma>\<^sub>26
 9. \<And>v\<^sub>1. \<lbrakk>\<And>v\<^sub>1. \<lbrakk>rs, fmempty \<turnstile>\<^sub>v t \<down> v\<^sub>1; \<turnstile>\<^sub>v v\<^sub>1 \<approx> v\<^sub>2\<rbrakk> \<Longrightarrow> thesis; rs, fmempty \<turnstile>\<^sub>v ?t6 \<down> v\<^sub>1; \<turnstile>\<^sub>v v\<^sub>1 \<approx> ?v\<^sub>26\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (9 subgoals):
 1. (\<And>v\<^sub>1. \<lbrakk>rs, fmempty \<turnstile>\<^sub>v t \<down> v\<^sub>1; \<turnstile>\<^sub>v v\<^sub>1 \<approx> v\<^sub>2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> ?\<Gamma>\<^sub>26 \<turnstile>\<^sub>v ?t6 \<down> ?v\<^sub>26
 2. (\<And>v\<^sub>1. \<lbrakk>rs, fmempty \<turnstile>\<^sub>v t \<down> v\<^sub>1; \<turnstile>\<^sub>v v\<^sub>1 \<approx> v\<^sub>2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> pre_strong_term_class.wellformed ?t6
 3. (\<And>v\<^sub>1. \<lbrakk>rs, fmempty \<turnstile>\<^sub>v t \<down> v\<^sub>1; \<turnstile>\<^sub>v v\<^sub>1 \<approx> v\<^sub>2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> wellformed_venv ?\<Gamma>\<^sub>26
 4. (\<And>v\<^sub>1. \<lbrakk>rs, fmempty \<turnstile>\<^sub>v t \<down> v\<^sub>1; \<turnstile>\<^sub>v v\<^sub>1 \<approx> v\<^sub>2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> \<not> shadows_consts ?t6
 5. (\<And>v\<^sub>1. \<lbrakk>rs, fmempty \<turnstile>\<^sub>v t \<down> v\<^sub>1; \<turnstile>\<^sub>v v\<^sub>1 \<approx> v\<^sub>2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> not_shadows_vconsts_env ?\<Gamma>\<^sub>26
 6. (\<And>v\<^sub>1. \<lbrakk>rs, fmempty \<turnstile>\<^sub>v t \<down> v\<^sub>1; \<turnstile>\<^sub>v v\<^sub>1 \<approx> v\<^sub>2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> consts ?t6 |\<subseteq>| all_consts
 7. (\<And>v\<^sub>1. \<lbrakk>rs, fmempty \<turnstile>\<^sub>v t \<down> v\<^sub>1; \<turnstile>\<^sub>v v\<^sub>1 \<approx> v\<^sub>2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> fmrel_on_fset (frees ?t6) vrelated fmempty ?\<Gamma>\<^sub>26
 8. (\<And>v\<^sub>1. \<lbrakk>rs, fmempty \<turnstile>\<^sub>v t \<down> v\<^sub>1; \<turnstile>\<^sub>v v\<^sub>1 \<approx> v\<^sub>2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> fmrel_on_fset (consts ?t6) vrelated (fmap_of_list rs) ?\<Gamma>\<^sub>26
 9. \<And>v\<^sub>1. \<lbrakk>\<And>v\<^sub>1. \<lbrakk>rs, fmempty \<turnstile>\<^sub>v t \<down> v\<^sub>1; \<turnstile>\<^sub>v v\<^sub>1 \<approx> v\<^sub>2\<rbrakk> \<Longrightarrow> thesis; rs, fmempty \<turnstile>\<^sub>v ?t6 \<down> v\<^sub>1; \<turnstile>\<^sub>v v\<^sub>1 \<approx> ?v\<^sub>26\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
show "fmrel_on_fset (frees t) vrelated fmempty \<Gamma>\<^sub>2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fmrel_on_fset (frees t) vrelated fmempty \<Gamma>\<^sub>2
[PROOF STEP]
using \<open>closed t\<close>
[PROOF STATE]
proof (prove)
using this:
closed t

goal (1 subgoal):
 1. fmrel_on_fset (frees t) vrelated fmempty \<Gamma>\<^sub>2
[PROOF STEP]
unfolding closed_except_def
[PROOF STATE]
proof (prove)
using this:
frees t |\<subseteq>| {||}

goal (1 subgoal):
 1. fmrel_on_fset (frees t) vrelated fmempty \<Gamma>\<^sub>2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
fmrel_on_fset (frees t) vrelated fmempty \<Gamma>\<^sub>2

goal (8 subgoals):
 1. (\<And>v\<^sub>1. \<lbrakk>rs, fmempty \<turnstile>\<^sub>v t \<down> v\<^sub>1; \<turnstile>\<^sub>v v\<^sub>1 \<approx> v\<^sub>2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> \<Gamma>\<^sub>2 \<turnstile>\<^sub>v t \<down> ?v\<^sub>26
 2. (\<And>v\<^sub>1. \<lbrakk>rs, fmempty \<turnstile>\<^sub>v t \<down> v\<^sub>1; \<turnstile>\<^sub>v v\<^sub>1 \<approx> v\<^sub>2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> pre_strong_term_class.wellformed t
 3. (\<And>v\<^sub>1. \<lbrakk>rs, fmempty \<turnstile>\<^sub>v t \<down> v\<^sub>1; \<turnstile>\<^sub>v v\<^sub>1 \<approx> v\<^sub>2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> wellformed_venv \<Gamma>\<^sub>2
 4. (\<And>v\<^sub>1. \<lbrakk>rs, fmempty \<turnstile>\<^sub>v t \<down> v\<^sub>1; \<turnstile>\<^sub>v v\<^sub>1 \<approx> v\<^sub>2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> \<not> shadows_consts t
 5. (\<And>v\<^sub>1. \<lbrakk>rs, fmempty \<turnstile>\<^sub>v t \<down> v\<^sub>1; \<turnstile>\<^sub>v v\<^sub>1 \<approx> v\<^sub>2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> not_shadows_vconsts_env \<Gamma>\<^sub>2
 6. (\<And>v\<^sub>1. \<lbrakk>rs, fmempty \<turnstile>\<^sub>v t \<down> v\<^sub>1; \<turnstile>\<^sub>v v\<^sub>1 \<approx> v\<^sub>2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> consts t |\<subseteq>| all_consts
 7. (\<And>v\<^sub>1. \<lbrakk>rs, fmempty \<turnstile>\<^sub>v t \<down> v\<^sub>1; \<turnstile>\<^sub>v v\<^sub>1 \<approx> v\<^sub>2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> fmrel_on_fset (consts t) vrelated (fmap_of_list rs) \<Gamma>\<^sub>2
 8. \<And>v\<^sub>1. \<lbrakk>\<And>v\<^sub>1. \<lbrakk>rs, fmempty \<turnstile>\<^sub>v t \<down> v\<^sub>1; \<turnstile>\<^sub>v v\<^sub>1 \<approx> v\<^sub>2\<rbrakk> \<Longrightarrow> thesis; rs, fmempty \<turnstile>\<^sub>v t \<down> v\<^sub>1; \<turnstile>\<^sub>v v\<^sub>1 \<approx> ?v\<^sub>26\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
qed (rule assms)+