[STATEMENT]
lemma cat_SemiCAT_is_iso_arrI:
  assumes "\<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>.\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<alpha>\<^esub> \<BB>"
  shows "\<FF> : \<AA> \<mapsto>\<^sub>i\<^sub>s\<^sub>o\<^bsub>cat_SemiCAT \<alpha>\<^esub> \<BB>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF> : \<AA> \<mapsto>\<^sub>i\<^sub>s\<^sub>o\<^bsub>cat_SemiCAT \<alpha>\<^esub> \<BB>
[PROOF STEP]
proof(intro is_iso_arrI is_inverseI)
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<FF> : \<AA> \<mapsto>\<^bsub>cat_SemiCAT \<alpha>\<^esub> \<BB>
 2. ?g : ?b1 \<mapsto>\<^bsub>cat_SemiCAT \<alpha>\<^esub> ?a1
 3. \<FF> : ?a1 \<mapsto>\<^bsub>cat_SemiCAT \<alpha>\<^esub> ?b1
 4. ?g \<circ>\<^sub>A\<^bsub>cat_SemiCAT \<alpha>\<^esub> \<FF> = cat_SemiCAT \<alpha>\<lparr>CId\<rparr>\<lparr>?a1\<rparr>
 5. \<FF> \<circ>\<^sub>A\<^bsub>cat_SemiCAT \<alpha>\<^esub> ?g = cat_SemiCAT \<alpha>\<lparr>CId\<rparr>\<lparr>?b1\<rparr>
[PROOF STEP]
interpret is_iso_semifunctor \<alpha> \<AA> \<BB> \<FF>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>.\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<alpha>\<^esub> \<BB>
[PROOF STEP]
by (rule assms)
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<FF> : \<AA> \<mapsto>\<^bsub>cat_SemiCAT \<alpha>\<^esub> \<BB>
 2. ?g : ?b1 \<mapsto>\<^bsub>cat_SemiCAT \<alpha>\<^esub> ?a1
 3. \<FF> : ?a1 \<mapsto>\<^bsub>cat_SemiCAT \<alpha>\<^esub> ?b1
 4. ?g \<circ>\<^sub>A\<^bsub>cat_SemiCAT \<alpha>\<^esub> \<FF> = cat_SemiCAT \<alpha>\<lparr>CId\<rparr>\<lparr>?a1\<rparr>
 5. \<FF> \<circ>\<^sub>A\<^bsub>cat_SemiCAT \<alpha>\<^esub> ?g = cat_SemiCAT \<alpha>\<lparr>CId\<rparr>\<lparr>?b1\<rparr>
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
\<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>.\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<alpha>\<^esub> \<BB>
[PROOF STEP]
show \<FF>: "\<FF> : \<AA> \<mapsto>\<^bsub>cat_SemiCAT \<alpha>\<^esub> \<BB>"
[PROOF STATE]
proof (prove)
using this:
\<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>.\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<alpha>\<^esub> \<BB>

goal (1 subgoal):
 1. \<FF> : \<AA> \<mapsto>\<^bsub>cat_SemiCAT \<alpha>\<^esub> \<BB>
[PROOF STEP]
unfolding cat_SemiCAT_is_arr_iff
[PROOF STATE]
proof (prove)
using this:
\<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>.\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<alpha>\<^esub> \<BB>

goal (1 subgoal):
 1. \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<FF> : \<AA> \<mapsto>\<^bsub>cat_SemiCAT \<alpha>\<^esub> \<BB>

goal (4 subgoals):
 1. ?g : ?b1 \<mapsto>\<^bsub>cat_SemiCAT \<alpha>\<^esub> ?a1
 2. \<FF> : ?a1 \<mapsto>\<^bsub>cat_SemiCAT \<alpha>\<^esub> ?b1
 3. ?g \<circ>\<^sub>A\<^bsub>cat_SemiCAT \<alpha>\<^esub> \<FF> = cat_SemiCAT \<alpha>\<lparr>CId\<rparr>\<lparr>?a1\<rparr>
 4. \<FF> \<circ>\<^sub>A\<^bsub>cat_SemiCAT \<alpha>\<^esub> ?g = cat_SemiCAT \<alpha>\<lparr>CId\<rparr>\<lparr>?b1\<rparr>
[PROOF STEP]
note iso_thms = is_iso_semifunctor_is_iso_arr[OF assms]
[PROOF STATE]
proof (state)
this:
inv_dghm \<FF> : \<BB> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>.\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<alpha>\<^esub> \<AA>
inv_dghm \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> = dghm_id \<AA>
\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M inv_dghm \<FF> = dghm_id \<BB>

goal (4 subgoals):
 1. ?g : ?b1 \<mapsto>\<^bsub>cat_SemiCAT \<alpha>\<^esub> ?a1
 2. \<FF> : ?a1 \<mapsto>\<^bsub>cat_SemiCAT \<alpha>\<^esub> ?b1
 3. ?g \<circ>\<^sub>A\<^bsub>cat_SemiCAT \<alpha>\<^esub> \<FF> = cat_SemiCAT \<alpha>\<lparr>CId\<rparr>\<lparr>?a1\<rparr>
 4. \<FF> \<circ>\<^sub>A\<^bsub>cat_SemiCAT \<alpha>\<^esub> ?g = cat_SemiCAT \<alpha>\<lparr>CId\<rparr>\<lparr>?b1\<rparr>
[PROOF STEP]
from iso_thms(1)
[PROOF STATE]
proof (chain)
picking this:
inv_dghm \<FF> : \<BB> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>.\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<alpha>\<^esub> \<AA>
[PROOF STEP]
show inv_\<FF>: "inv_smcf \<FF> : \<BB> \<mapsto>\<^bsub>cat_SemiCAT \<alpha>\<^esub> \<AA>"
[PROOF STATE]
proof (prove)
using this:
inv_dghm \<FF> : \<BB> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>.\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<alpha>\<^esub> \<AA>

goal (1 subgoal):
 1. inv_dghm \<FF> : \<BB> \<mapsto>\<^bsub>cat_SemiCAT \<alpha>\<^esub> \<AA>
[PROOF STEP]
unfolding cat_SemiCAT_is_arr_iff
[PROOF STATE]
proof (prove)
using this:
inv_dghm \<FF> : \<BB> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>.\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<alpha>\<^esub> \<AA>

goal (1 subgoal):
 1. inv_dghm \<FF> : \<BB> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
inv_dghm \<FF> : \<BB> \<mapsto>\<^bsub>cat_SemiCAT \<alpha>\<^esub> \<AA>

goal (3 subgoals):
 1. \<FF> : \<AA> \<mapsto>\<^bsub>cat_SemiCAT \<alpha>\<^esub> \<BB>
 2. inv_dghm \<FF> \<circ>\<^sub>A\<^bsub>cat_SemiCAT \<alpha>\<^esub> \<FF> = cat_SemiCAT \<alpha>\<lparr>CId\<rparr>\<lparr>\<AA>\<rparr>
 3. \<FF> \<circ>\<^sub>A\<^bsub>cat_SemiCAT \<alpha>\<^esub> inv_dghm \<FF> = cat_SemiCAT \<alpha>\<lparr>CId\<rparr>\<lparr>\<BB>\<rparr>
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
\<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>.\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<alpha>\<^esub> \<BB>
[PROOF STEP]
show "\<FF> : \<AA> \<mapsto>\<^bsub>cat_SemiCAT \<alpha>\<^esub> \<BB>"
[PROOF STATE]
proof (prove)
using this:
\<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>.\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<alpha>\<^esub> \<BB>

goal (1 subgoal):
 1. \<FF> : \<AA> \<mapsto>\<^bsub>cat_SemiCAT \<alpha>\<^esub> \<BB>
[PROOF STEP]
unfolding cat_SemiCAT_is_arr_iff
[PROOF STATE]
proof (prove)
using this:
\<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>.\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<alpha>\<^esub> \<BB>

goal (1 subgoal):
 1. \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<FF> : \<AA> \<mapsto>\<^bsub>cat_SemiCAT \<alpha>\<^esub> \<BB>

goal (2 subgoals):
 1. inv_dghm \<FF> \<circ>\<^sub>A\<^bsub>cat_SemiCAT \<alpha>\<^esub> \<FF> = cat_SemiCAT \<alpha>\<lparr>CId\<rparr>\<lparr>\<AA>\<rparr>
 2. \<FF> \<circ>\<^sub>A\<^bsub>cat_SemiCAT \<alpha>\<^esub> inv_dghm \<FF> = cat_SemiCAT \<alpha>\<lparr>CId\<rparr>\<lparr>\<BB>\<rparr>
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
\<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>.\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<alpha>\<^esub> \<BB>
[PROOF STEP]
have \<AA>: "semicategory \<alpha> \<AA>" and \<BB>: "semicategory \<alpha> \<BB>"
[PROOF STATE]
proof (prove)
using this:
\<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>.\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<alpha>\<^esub> \<BB>

goal (1 subgoal):
 1. semicategory \<alpha> \<AA> &&& semicategory \<alpha> \<BB>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
semicategory \<alpha> \<AA>
semicategory \<alpha> \<BB>

goal (2 subgoals):
 1. inv_dghm \<FF> \<circ>\<^sub>A\<^bsub>cat_SemiCAT \<alpha>\<^esub> \<FF> = cat_SemiCAT \<alpha>\<lparr>CId\<rparr>\<lparr>\<AA>\<rparr>
 2. \<FF> \<circ>\<^sub>A\<^bsub>cat_SemiCAT \<alpha>\<^esub> inv_dghm \<FF> = cat_SemiCAT \<alpha>\<lparr>CId\<rparr>\<lparr>\<BB>\<rparr>
[PROOF STEP]
show "inv_smcf \<FF> \<circ>\<^sub>A\<^bsub>cat_SemiCAT \<alpha>\<^esub> \<FF> = cat_SemiCAT \<alpha>\<lparr>CId\<rparr>\<lparr>\<AA>\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inv_dghm \<FF> \<circ>\<^sub>A\<^bsub>cat_SemiCAT \<alpha>\<^esub> \<FF> = cat_SemiCAT \<alpha>\<lparr>CId\<rparr>\<lparr>\<AA>\<rparr>
[PROOF STEP]
unfolding cat_SemiCAT_CId_app[OF \<AA>] cat_SemiCAT_Comp_app[OF inv_\<FF> \<FF>]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inv_dghm \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> = dghm_id \<AA>
[PROOF STEP]
by (rule iso_thms(2))
[PROOF STATE]
proof (state)
this:
inv_dghm \<FF> \<circ>\<^sub>A\<^bsub>cat_SemiCAT \<alpha>\<^esub> \<FF> = cat_SemiCAT \<alpha>\<lparr>CId\<rparr>\<lparr>\<AA>\<rparr>

goal (1 subgoal):
 1. \<FF> \<circ>\<^sub>A\<^bsub>cat_SemiCAT \<alpha>\<^esub> inv_dghm \<FF> = cat_SemiCAT \<alpha>\<lparr>CId\<rparr>\<lparr>\<BB>\<rparr>
[PROOF STEP]
show "\<FF> \<circ>\<^sub>A\<^bsub>cat_SemiCAT \<alpha>\<^esub> inv_smcf \<FF> = cat_SemiCAT \<alpha>\<lparr>CId\<rparr>\<lparr>\<BB>\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF> \<circ>\<^sub>A\<^bsub>cat_SemiCAT \<alpha>\<^esub> inv_dghm \<FF> = cat_SemiCAT \<alpha>\<lparr>CId\<rparr>\<lparr>\<BB>\<rparr>
[PROOF STEP]
unfolding cat_SemiCAT_CId_app[OF \<BB>] cat_SemiCAT_Comp_app[OF \<FF> inv_\<FF>]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M inv_dghm \<FF> = dghm_id \<BB>
[PROOF STEP]
by (rule iso_thms(3))
[PROOF STATE]
proof (state)
this:
\<FF> \<circ>\<^sub>A\<^bsub>cat_SemiCAT \<alpha>\<^esub> inv_dghm \<FF> = cat_SemiCAT \<alpha>\<lparr>CId\<rparr>\<lparr>\<BB>\<rparr>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma tendsto_unique_eventually:
  fixes x x' :: "'a :: t2_space"
  shows "F \<noteq> bot \<Longrightarrow> eventually (\<lambda>x. f x = g x) F \<Longrightarrow> (f \<longlongrightarrow> x) F \<Longrightarrow> (g \<longlongrightarrow> x') F \<Longrightarrow> x = x'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>F \<noteq> \<bottom>; \<forall>\<^sub>F x in F. f x = g x; (f \<longlongrightarrow> x) F; (g \<longlongrightarrow> x') F\<rbrakk> \<Longrightarrow> x = x'
[PROOF STEP]
by (metis tendsto_unique filterlim_cong)


[STATEMENT]
lemma [intro]:
  "composable_tm (tm_copy_begin_orig, 0)"
  "composable_tm (tm_copy_loop_orig, 0)"
  "composable_tm (tm_copy_end_new, 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. composable_tm0 tm_copy_begin_orig &&& composable_tm0 tm_copy_loop_orig &&& composable_tm0 tm_copy_end_new
[PROOF STEP]
by (auto simp: composable_tm.simps tm_copy_end_new_def tm_copy_loop_orig_def tm_copy_begin_orig_def)


[STATEMENT]
lemma fst_annotate_rlen_le: "(k, a) \<in> set (annotate_rlen l) \<Longrightarrow> k < length l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (k, a) \<in> set (annotate_rlen l) \<Longrightarrow> k < length l
[PROOF STEP]
by(induction l arbitrary: k; simp; force)


[STATEMENT]
lemma universal_arrow_of_if_cat_representation:
  \<comment>\<open>See Proposition 2 in Chapter III-2 in \cite{mac_lane_categories_2010}.\<close>
  assumes "\<KK> : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> cat_Set \<alpha>"
    and "cat_representation \<alpha> \<KK> r \<psi>"
    and "\<aa> \<in>\<^sub>\<circ> cat_Set \<alpha>\<lparr>Obj\<rparr>"
  shows "universal_arrow_of
    \<KK> (set {\<aa>}) r (ntcf_paa \<aa> (\<KK>\<lparr>ObjMap\<rparr>\<lparr>r\<rparr>) (\<psi>\<lparr>NTMap\<rparr>\<lparr>r\<rparr>\<lparr>ArrVal\<rparr>\<lparr>\<CC>\<lparr>CId\<rparr>\<lparr>r\<rparr>\<rparr>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. universal_arrow_of \<KK> (ZFC_in_HOL.set {\<aa>}) r (ntcf_paa \<aa> (\<KK>\<lparr>ObjMap\<rparr>\<lparr>r\<rparr>) (\<psi>\<lparr>NTMap\<rparr>\<lparr>r\<rparr>\<lparr>ArrVal\<rparr>\<lparr>\<CC>\<lparr>CId\<rparr>\<lparr>r\<rparr>\<rparr>))
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. universal_arrow_of \<KK> (ZFC_in_HOL.set {\<aa>}) r (ntcf_paa \<aa> (\<KK>\<lparr>ObjMap\<rparr>\<lparr>r\<rparr>) (\<psi>\<lparr>NTMap\<rparr>\<lparr>r\<rparr>\<lparr>ArrVal\<rparr>\<lparr>\<CC>\<lparr>CId\<rparr>\<lparr>r\<rparr>\<rparr>))
[PROOF STEP]
note r\<psi> = cat_representationD[OF assms(2,1)]
[PROOF STATE]
proof (state)
this:
r \<in>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr>
\<psi> : Hom\<^sub>O\<^sub>.\<^sub>C\<^bsub>\<alpha>\<^esub>\<CC>(r,-) \<mapsto>\<^sub>C\<^sub>F\<^sub>.\<^sub>i\<^sub>s\<^sub>o \<KK> : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> cat_Set \<alpha>

goal (1 subgoal):
 1. universal_arrow_of \<KK> (ZFC_in_HOL.set {\<aa>}) r (ntcf_paa \<aa> (\<KK>\<lparr>ObjMap\<rparr>\<lparr>r\<rparr>) (\<psi>\<lparr>NTMap\<rparr>\<lparr>r\<rparr>\<lparr>ArrVal\<rparr>\<lparr>\<CC>\<lparr>CId\<rparr>\<lparr>r\<rparr>\<rparr>))
[PROOF STEP]
interpret \<KK>: is_functor \<alpha> \<CC> \<open>cat_Set \<alpha>\<close> \<KK>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<KK> : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> cat_Set \<alpha>
[PROOF STEP]
by (rule assms(1))
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. universal_arrow_of \<KK> (ZFC_in_HOL.set {\<aa>}) r (ntcf_paa \<aa> (\<KK>\<lparr>ObjMap\<rparr>\<lparr>r\<rparr>) (\<psi>\<lparr>NTMap\<rparr>\<lparr>r\<rparr>\<lparr>ArrVal\<rparr>\<lparr>\<CC>\<lparr>CId\<rparr>\<lparr>r\<rparr>\<rparr>))
[PROOF STEP]
interpret \<psi>: is_iso_ntcf \<alpha> \<CC> \<open>cat_Set \<alpha>\<close> \<open>Hom\<^sub>O\<^sub>.\<^sub>C\<^bsub>\<alpha>\<^esub>\<CC>(r,-)\<close> \<KK> \<psi>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<psi> : Hom\<^sub>O\<^sub>.\<^sub>C\<^bsub>\<alpha>\<^esub>\<CC>(r,-) \<mapsto>\<^sub>C\<^sub>F\<^sub>.\<^sub>i\<^sub>s\<^sub>o \<KK> : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> cat_Set \<alpha>
[PROOF STEP]
by (rule r\<psi>(2))
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. universal_arrow_of \<KK> (ZFC_in_HOL.set {\<aa>}) r (ntcf_paa \<aa> (\<KK>\<lparr>ObjMap\<rparr>\<lparr>r\<rparr>) (\<psi>\<lparr>NTMap\<rparr>\<lparr>r\<rparr>\<lparr>ArrVal\<rparr>\<lparr>\<CC>\<lparr>CId\<rparr>\<lparr>r\<rparr>\<rparr>))
[PROOF STEP]
from assms(3)
[PROOF STATE]
proof (chain)
picking this:
\<aa> \<in>\<^sub>\<circ> cat_Set \<alpha>\<lparr>Obj\<rparr>
[PROOF STEP]
have set_\<aa>: "set {\<aa>} \<in>\<^sub>\<circ> cat_Set \<alpha>\<lparr>Obj\<rparr>"
[PROOF STATE]
proof (prove)
using this:
\<aa> \<in>\<^sub>\<circ> cat_Set \<alpha>\<lparr>Obj\<rparr>

goal (1 subgoal):
 1. ZFC_in_HOL.set {\<aa>} \<in>\<^sub>\<circ> cat_Set \<alpha>\<lparr>Obj\<rparr>
[PROOF STEP]
by (simp add: Limit_vsingleton_in_VsetI cat_Set_components(1))
[PROOF STATE]
proof (state)
this:
ZFC_in_HOL.set {\<aa>} \<in>\<^sub>\<circ> cat_Set \<alpha>\<lparr>Obj\<rparr>

goal (1 subgoal):
 1. universal_arrow_of \<KK> (ZFC_in_HOL.set {\<aa>}) r (ntcf_paa \<aa> (\<KK>\<lparr>ObjMap\<rparr>\<lparr>r\<rparr>) (\<psi>\<lparr>NTMap\<rparr>\<lparr>r\<rparr>\<lparr>ArrVal\<rparr>\<lparr>\<CC>\<lparr>CId\<rparr>\<lparr>r\<rparr>\<rparr>))
[PROOF STEP]
from
    ntcf_cf_comp_is_iso_ntcf[
      OF \<KK>.ntcf_pointed_inv_is_iso_ntcf[OF assms(3)] assms(1)
      ]
[PROOF STATE]
proof (chain)
picking this:
ntcf_pointed_inv \<alpha> \<aa> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK> : dghm_id (cat_Set \<alpha>) \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK> \<mapsto>\<^sub>C\<^sub>F\<^sub>.\<^sub>i\<^sub>s\<^sub>o Hom\<^sub>O\<^sub>.\<^sub>C\<^bsub>\<alpha>\<^esub>cat_Set \<alpha>(ZFC_in_HOL.set {\<aa>},-) \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK> : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> cat_Set \<alpha>
[PROOF STEP]
have \<aa>\<KK>: "ntcf_pointed_inv \<alpha> \<aa> \<circ>\<^sub>N\<^sub>T\<^sub>C\<^sub>F\<^sub>-\<^sub>C\<^sub>F \<KK> :
    \<KK> \<mapsto>\<^sub>C\<^sub>F\<^sub>.\<^sub>i\<^sub>s\<^sub>o Hom\<^sub>O\<^sub>.\<^sub>C\<^bsub>\<alpha>\<^esub>cat_Set \<alpha> (set {\<aa>},-) \<circ>\<^sub>C\<^sub>F \<KK> : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> cat_Set \<alpha>"
[PROOF STATE]
proof (prove)
using this:
ntcf_pointed_inv \<alpha> \<aa> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK> : dghm_id (cat_Set \<alpha>) \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK> \<mapsto>\<^sub>C\<^sub>F\<^sub>.\<^sub>i\<^sub>s\<^sub>o Hom\<^sub>O\<^sub>.\<^sub>C\<^bsub>\<alpha>\<^esub>cat_Set \<alpha>(ZFC_in_HOL.set {\<aa>},-) \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK> : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> cat_Set \<alpha>

goal (1 subgoal):
 1. ntcf_pointed_inv \<alpha> \<aa> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK> : \<KK> \<mapsto>\<^sub>C\<^sub>F\<^sub>.\<^sub>i\<^sub>s\<^sub>o Hom\<^sub>O\<^sub>.\<^sub>C\<^bsub>\<alpha>\<^esub>cat_Set \<alpha>(ZFC_in_HOL.set {\<aa>},-) \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK> : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> cat_Set \<alpha>
[PROOF STEP]
by (cs_prems cs_simp: cat_cs_simps)
[PROOF STATE]
proof (state)
this:
ntcf_pointed_inv \<alpha> \<aa> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK> : \<KK> \<mapsto>\<^sub>C\<^sub>F\<^sub>.\<^sub>i\<^sub>s\<^sub>o Hom\<^sub>O\<^sub>.\<^sub>C\<^bsub>\<alpha>\<^esub>cat_Set \<alpha>(ZFC_in_HOL.set {\<aa>},-) \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK> : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> cat_Set \<alpha>

goal (1 subgoal):
 1. universal_arrow_of \<KK> (ZFC_in_HOL.set {\<aa>}) r (ntcf_paa \<aa> (\<KK>\<lparr>ObjMap\<rparr>\<lparr>r\<rparr>) (\<psi>\<lparr>NTMap\<rparr>\<lparr>r\<rparr>\<lparr>ArrVal\<rparr>\<lparr>\<CC>\<lparr>CId\<rparr>\<lparr>r\<rparr>\<rparr>))
[PROOF STEP]
from iso_ntcf_is_iso_arr(1)[OF \<aa>\<KK>] r\<psi> assms(3)
[PROOF STATE]
proof (chain)
picking this:
inv_ntcf (ntcf_pointed_inv \<alpha> \<aa> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK>) : Hom\<^sub>O\<^sub>.\<^sub>C\<^bsub>\<alpha>\<^esub>cat_Set \<alpha>(ZFC_in_HOL.set {\<aa>},-) \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK> \<mapsto>\<^sub>C\<^sub>F\<^sub>.\<^sub>i\<^sub>s\<^sub>o \<KK> : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> cat_Set \<alpha>
r \<in>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr>
\<psi> : Hom\<^sub>O\<^sub>.\<^sub>C\<^bsub>\<alpha>\<^esub>\<CC>(r,-) \<mapsto>\<^sub>C\<^sub>F\<^sub>.\<^sub>i\<^sub>s\<^sub>o \<KK> : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> cat_Set \<alpha>
\<aa> \<in>\<^sub>\<circ> cat_Set \<alpha>\<lparr>Obj\<rparr>
[PROOF STEP]
have [cat_cs_simps]:
    "((ntcf_pointed_inv \<alpha> \<aa> \<circ>\<^sub>N\<^sub>T\<^sub>C\<^sub>F\<^sub>-\<^sub>C\<^sub>F \<KK> \<bullet>\<^sub>N\<^sub>T\<^sub>C\<^sub>F \<psi>)\<lparr>NTMap\<rparr>\<lparr>r\<rparr>\<lparr>ArrVal\<rparr>\<lparr>\<CC>\<lparr>CId\<rparr>\<lparr>r\<rparr>\<rparr>) =
      ntcf_paa \<aa> (\<KK>\<lparr>ObjMap\<rparr>\<lparr>r\<rparr>) (\<psi>\<lparr>NTMap\<rparr>\<lparr>r\<rparr>\<lparr>ArrVal\<rparr>\<lparr>\<CC>\<lparr>CId\<rparr>\<lparr>r\<rparr>\<rparr>)"
[PROOF STATE]
proof (prove)
using this:
inv_ntcf (ntcf_pointed_inv \<alpha> \<aa> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK>) : Hom\<^sub>O\<^sub>.\<^sub>C\<^bsub>\<alpha>\<^esub>cat_Set \<alpha>(ZFC_in_HOL.set {\<aa>},-) \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK> \<mapsto>\<^sub>C\<^sub>F\<^sub>.\<^sub>i\<^sub>s\<^sub>o \<KK> : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> cat_Set \<alpha>
r \<in>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr>
\<psi> : Hom\<^sub>O\<^sub>.\<^sub>C\<^bsub>\<alpha>\<^esub>\<CC>(r,-) \<mapsto>\<^sub>C\<^sub>F\<^sub>.\<^sub>i\<^sub>s\<^sub>o \<KK> : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> cat_Set \<alpha>
\<aa> \<in>\<^sub>\<circ> cat_Set \<alpha>\<lparr>Obj\<rparr>

goal (1 subgoal):
 1. (ntcf_pointed_inv \<alpha> \<aa> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<psi>)\<lparr>NTMap\<rparr>\<lparr>r\<rparr>\<lparr>ArrVal\<rparr>\<lparr>\<CC>\<lparr>CId\<rparr>\<lparr>r\<rparr>\<rparr> = ntcf_paa \<aa> (\<KK>\<lparr>ObjMap\<rparr>\<lparr>r\<rparr>) (\<psi>\<lparr>NTMap\<rparr>\<lparr>r\<rparr>\<lparr>ArrVal\<rparr>\<lparr>\<CC>\<lparr>CId\<rparr>\<lparr>r\<rparr>\<rparr>)
[PROOF STEP]
by
      (
        cs_concl
          cs_simp: cat_cs_simps
          cs_intro: cat_Set_cs_intros cat_cs_intros cat_op_intros
      )
[PROOF STATE]
proof (state)
this:
(ntcf_pointed_inv \<alpha> \<aa> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<psi>)\<lparr>NTMap\<rparr>\<lparr>r\<rparr>\<lparr>ArrVal\<rparr>\<lparr>\<CC>\<lparr>CId\<rparr>\<lparr>r\<rparr>\<rparr> = ntcf_paa \<aa> (\<KK>\<lparr>ObjMap\<rparr>\<lparr>r\<rparr>) (\<psi>\<lparr>NTMap\<rparr>\<lparr>r\<rparr>\<lparr>ArrVal\<rparr>\<lparr>\<CC>\<lparr>CId\<rparr>\<lparr>r\<rparr>\<rparr>)

goal (1 subgoal):
 1. universal_arrow_of \<KK> (ZFC_in_HOL.set {\<aa>}) r (ntcf_paa \<aa> (\<KK>\<lparr>ObjMap\<rparr>\<lparr>r\<rparr>) (\<psi>\<lparr>NTMap\<rparr>\<lparr>r\<rparr>\<lparr>ArrVal\<rparr>\<lparr>\<CC>\<lparr>CId\<rparr>\<lparr>r\<rparr>\<rparr>))
[PROOF STEP]
show "universal_arrow_of
    \<KK> (set {\<aa>}) r (ntcf_paa \<aa> (\<KK>\<lparr>ObjMap\<rparr>\<lparr>r\<rparr>) (\<psi>\<lparr>NTMap\<rparr>\<lparr>r\<rparr>\<lparr>ArrVal\<rparr>\<lparr>\<CC>\<lparr>CId\<rparr>\<lparr>r\<rparr>\<rparr>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. universal_arrow_of \<KK> (ZFC_in_HOL.set {\<aa>}) r (ntcf_paa \<aa> (\<KK>\<lparr>ObjMap\<rparr>\<lparr>r\<rparr>) (\<psi>\<lparr>NTMap\<rparr>\<lparr>r\<rparr>\<lparr>ArrVal\<rparr>\<lparr>\<CC>\<lparr>CId\<rparr>\<lparr>r\<rparr>\<rparr>))
[PROOF STEP]
by
      (
        rule \<KK>.cf_universal_arrow_of_if_is_iso_ntcf
          [
            OF r\<psi>(1) set_\<aa> ntcf_vcomp_is_iso_ntcf[OF \<aa>\<KK> r\<psi>(2)],
            unfolded cat_cs_simps
          ]
      )
[PROOF STATE]
proof (state)
this:
universal_arrow_of \<KK> (ZFC_in_HOL.set {\<aa>}) r (ntcf_paa \<aa> (\<KK>\<lparr>ObjMap\<rparr>\<lparr>r\<rparr>) (\<psi>\<lparr>NTMap\<rparr>\<lparr>r\<rparr>\<lparr>ArrVal\<rparr>\<lparr>\<CC>\<lparr>CId\<rparr>\<lparr>r\<rparr>\<rparr>))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma b_e_type_get_local:
  assumes "\<C> \<turnstile> [e] : (ts _> ts')"
          "e = Get_local i"
  shows "\<exists>t. ts' = ts@[t] \<and> (local \<C>)!i = t" "i < length(local \<C>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>t. ts' = ts @ [t] \<and> local \<C> ! i = t &&& i < length (local \<C>)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<C> \<turnstile> [e] : ts _> ts'
e = Get_local i

goal (1 subgoal):
 1. \<exists>t. ts' = ts @ [t] \<and> local \<C> ! i = t &&& i < length (local \<C>)
[PROOF STEP]
by (induction "[e]" "(ts _> ts')" arbitrary: ts ts' rule: b_e_typing.induct, auto)


[STATEMENT]
lemma toEnum_of_nat[simp]: "n < 2 ^ LENGTH('a) \<Longrightarrow> (toEnum n :: 'a :: len word) = of_nat n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n < 2 ^ LENGTH('a) \<Longrightarrow> toEnum n = word_of_nat n
[PROOF STEP]
by (simp add: toEnum_def length_word_enum enum_word_def)


[STATEMENT]
lemma ID_inf: "Der_inf \<phi> \<Longrightarrow> Int_inf(\<I>\<^sub>D \<phi>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Der_inf \<phi> \<Longrightarrow> Int_inf (\<I>\<^sub>D \<phi>)
[PROOF STEP]
by (simp add: CD_inf dual_der2 iADDI_MULT_dual1)


[STATEMENT]
lemma dtail_root_in_set:
  assumes "e \<in> darcs t" and "t = Node r xs" and "dtail t dt e = r"
  shows "e \<in> snd ` fset xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. e \<in> snd ` fset xs
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. e \<notin> snd ` fset xs \<Longrightarrow> False
[PROOF STEP]
assume "e \<notin> snd ` fset xs"
[PROOF STATE]
proof (state)
this:
e \<notin> snd ` fset xs

goal (1 subgoal):
 1. e \<notin> snd ` fset xs \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
e \<notin> snd ` fset xs
[PROOF STEP]
obtain x e1 where x_def: "(x,e1) \<in> fset xs \<and> e \<in> darcs x"
[PROOF STATE]
proof (prove)
using this:
e \<notin> snd ` fset xs

goal (1 subgoal):
 1. (\<And>x e1. (x, e1) \<in> fset xs \<and> e \<in> darcs x \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms(1,2)
[PROOF STATE]
proof (prove)
using this:
e \<notin> snd ` fset xs
e \<in> darcs t
t = Node r xs

goal (1 subgoal):
 1. (\<And>x e1. (x, e1) \<in> fset xs \<and> e \<in> darcs x \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
(x, e1) \<in> fset xs \<and> e \<in> darcs x

goal (1 subgoal):
 1. e \<notin> snd ` fset xs \<Longrightarrow> False
[PROOF STEP]
interpret X: wf_dtree x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf_dtree x
[PROOF STEP]
using assms(2) x_def wf_dtree_rec
[PROOF STATE]
proof (prove)
using this:
t = Node r xs
(x, e1) \<in> fset xs \<and> e \<in> darcs x
\<lbrakk>Node ?r ?xs = t; (?x, ?e) \<in> fset ?xs\<rbrakk> \<Longrightarrow> wf_dtree ?x

goal (1 subgoal):
 1. wf_dtree x
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. e \<notin> snd ` fset xs \<Longrightarrow> False
[PROOF STEP]
have "dtail t dt e = dtail x dt e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dtail t dt e = dtail x dt e
[PROOF STEP]
using dtail_in_child_eq_child[of x] wf_arcs assms(2) x_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>(x, ?e1.0) \<in> fset ?xs; ?e \<in> darcs x; wf_darcs (Node ?r ?xs)\<rbrakk> \<Longrightarrow> dtail (Node ?r ?xs) ?def ?e = dtail x ?def ?e
wf_darcs t
t = Node r xs
(x, e1) \<in> fset xs \<and> e \<in> darcs x

goal (1 subgoal):
 1. dtail t dt e = dtail x dt e
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
dtail t dt e = dtail x dt e

goal (1 subgoal):
 1. e \<notin> snd ` fset xs \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
dtail t dt e = dtail x dt e
[PROOF STEP]
have "dtail t dt e \<in> dverts x"
[PROOF STATE]
proof (prove)
using this:
dtail t dt e = dtail x dt e

goal (1 subgoal):
 1. dtail t dt e \<in> dverts x
[PROOF STEP]
using X.dtail_in_dverts x_def
[PROOF STATE]
proof (prove)
using this:
dtail t dt e = dtail x dt e
?e \<in> darcs x \<Longrightarrow> dtail x ?def ?e \<in> dverts x
(x, e1) \<in> fset xs \<and> e \<in> darcs x

goal (1 subgoal):
 1. dtail t dt e \<in> dverts x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
dtail t dt e \<in> dverts x

goal (1 subgoal):
 1. e \<notin> snd ` fset xs \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
dtail t dt e \<in> dverts x
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
dtail t dt e \<in> dverts x

goal (1 subgoal):
 1. False
[PROOF STEP]
using assms(2,3) wf_verts x_def
[PROOF STATE]
proof (prove)
using this:
dtail t dt e \<in> dverts x
t = Node r xs
dtail t dt e = r
wf_dverts t
(x, e1) \<in> fset xs \<and> e \<in> darcs x

goal (1 subgoal):
 1. False
[PROOF STEP]
unfolding wf_dverts_iff_dverts'
[PROOF STATE]
proof (prove)
using this:
dtail t dt e \<in> dverts x
t = Node r xs
dtail t dt e = r
wf_dverts' t
(x, e1) \<in> fset xs \<and> e \<in> darcs x

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma arev_in_arcs[simp]: "a \<in> arcs G \<Longrightarrow> arev a \<in> arcs G"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<in> arcs G \<Longrightarrow> arev a \<in> arcs G
[PROOF STEP]
by (metis arev_arev arev_dom)


[STATEMENT]
lemma nxt_Power_dfa [simp]: "dfa.nxt Power_dfa = (\<lambda>Q x. HF(\<Union>q \<in> epsclo (hfset Q). epsclo (nxt M q x)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dfa.nxt Power_dfa = (\<lambda>Q x. HF (\<Union>q\<in>epsclo (hfset Q). epsclo (nfa.nxt M q x)))
[PROOF STEP]
by (simp add: Power_dfa_def)


[STATEMENT]
lemma mult_ge1_powers [mono_intros]:
  assumes "a \<ge> (1::'a::linordered_idom)"
  shows "1 \<le> a * a" "1 \<le> a * a * a" "1 \<le> a * a * a * a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (1::'a) \<le> a * a &&& (1::'a) \<le> a * a * a &&& (1::'a) \<le> a * a * a * a
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
(1::'a) \<le> a

goal (1 subgoal):
 1. (1::'a) \<le> a * a &&& (1::'a) \<le> a * a * a &&& (1::'a) \<le> a * a * a * a
[PROOF STEP]
by (meson assms dual_order.trans mult_ge1_mono(1) zero_le_one)+


[STATEMENT]
lemma ample_subset:
      assumes "ample_set q A"
      shows "A \<subseteq> {a. en a q}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<subseteq> {a. en a q}
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
ample_set q A

goal (1 subgoal):
 1. A \<subseteq> {a. en a q}
[PROOF STEP]
unfolding ample_set_def
[PROOF STATE]
proof (prove)
using this:
A \<subseteq> {a. en a q} \<and> (A \<subset> {a. en a q} \<longrightarrow> A \<noteq> {}) \<and> (\<forall>a. A \<subset> {a. en a q} \<longrightarrow> a \<in> A \<longrightarrow> src (ex a q) q) \<and> (A \<subset> {a. en a q} \<longrightarrow> A \<subseteq> invisible) \<and> (\<forall>w. A \<subset> {a. en a q} \<longrightarrow> path w q \<longrightarrow> A \<inter> set w = {} \<longrightarrow> Ind A (set w))

goal (1 subgoal):
 1. A \<subseteq> {a. en a q}
[PROOF STEP]
by auto


[STATEMENT]
lemma is_symbol_distinct: "is_symbol x \<Longrightarrow> is_terminal x \<noteq> is_nonterminal x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_symbol x \<Longrightarrow> is_terminal x \<noteq> is_nonterminal x
[PROOF STEP]
apply (insert disjunct_symbols)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_symbol x; \<NN> \<inter> \<TT> = {}\<rbrakk> \<Longrightarrow> is_terminal x \<noteq> is_nonterminal x
[PROOF STEP]
apply (auto simp add: is_symbol_def is_terminal_def is_nonterminal_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma ahm_invar_auxE:
  assumes "ahm_invar_aux bhc n a"
  obtains "\<forall>h. h < array_length a \<longrightarrow>
      bucket_ok bhc (array_length a) h (array_get a h) \<and>
      list_map_invar (array_get a h)" and
  "n = array_foldl (\<lambda>_ n kvs. n + length kvs) 0 a" and
  "array_length a > 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lbrakk>\<forall>h<array_length a. bucket_ok bhc (array_length a) h (array_get a h) \<and> list_map_invar (array_get a h); n = array_foldl (\<lambda>_ n kvs. n + length kvs) 0 a; 1 < array_length a\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
ahm_invar_aux bhc n a

goal (1 subgoal):
 1. (\<lbrakk>\<forall>h<array_length a. bucket_ok bhc (array_length a) h (array_get a h) \<and> list_map_invar (array_get a h); n = array_foldl (\<lambda>_ n kvs. n + length kvs) 0 a; 1 < array_length a\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding ahm_invar_aux_def
[PROOF STATE]
proof (prove)
using this:
(\<forall>h<array_length a. bucket_ok bhc (array_length a) h (array_get a h) \<and> list_map_invar (array_get a h)) \<and> array_foldl (\<lambda>_ n kvs. n + length kvs) 0 a = n \<and> 1 < array_length a

goal (1 subgoal):
 1. (\<lbrakk>\<forall>h<array_length a. bucket_ok bhc (array_length a) h (array_get a h) \<and> list_map_invar (array_get a h); n = array_foldl (\<lambda>_ n kvs. n + length kvs) 0 a; 1 < array_length a\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast


[STATEMENT]
lemma cwf_cNode_seqOf:
  "cwf (cNode (s, r) cts) \<Longrightarrow> eff r s (fimage seqOf cts)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cwf (cNode (s, r) cts) \<Longrightarrow> eff r s (seqOf |`| cts)
[PROOF STEP]
by (auto elim: cwf.cases)


[STATEMENT]
lemma analz_Un_EncSet2:
assumes "Enc_keys_clean H" and "K \<subseteq> range LtK" and "K \<inter> synth (analz H) = {}"
shows "analz (EncSet G K \<union> H) \<subseteq> EncSet G K \<union> analz H"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. analz (EncSet G K \<union> H) \<subseteq> EncSet G K \<union> analz H
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> analz (EncSet G K \<union> H) \<Longrightarrow> x \<in> EncSet G K \<union> analz H
[PROOF STEP]
fix X
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> analz (EncSet G K \<union> H) \<Longrightarrow> x \<in> EncSet G K \<union> analz H
[PROOF STEP]
assume "X \<in> analz (EncSet G K \<union> H)"
[PROOF STATE]
proof (state)
this:
X \<in> analz (EncSet G K \<union> H)

goal (1 subgoal):
 1. \<And>x. x \<in> analz (EncSet G K \<union> H) \<Longrightarrow> x \<in> EncSet G K \<union> analz H
[PROOF STEP]
thus "X \<in> EncSet G K \<union> analz H"
[PROOF STATE]
proof (prove)
using this:
X \<in> analz (EncSet G K \<union> H)

goal (1 subgoal):
 1. X \<in> EncSet G K \<union> analz H
[PROOF STEP]
proof (induction X rule: analz.induct)
[PROOF STATE]
proof (state)
goal (7 subgoals):
 1. \<And>X. X \<in> EncSet G K \<union> H \<Longrightarrow> X \<in> EncSet G K \<union> analz H
 2. \<And>X Y. \<lbrakk>\<langle>X, Y\<rangle> \<in> analz (EncSet G K \<union> H); \<langle>X, Y\<rangle> \<in> EncSet G K \<union> analz H\<rbrakk> \<Longrightarrow> X \<in> EncSet G K \<union> analz H
 3. \<And>X Y. \<lbrakk>\<langle>X, Y\<rangle> \<in> analz (EncSet G K \<union> H); \<langle>X, Y\<rangle> \<in> EncSet G K \<union> analz H\<rbrakk> \<Longrightarrow> Y \<in> EncSet G K \<union> analz H
 4. \<And>X Y. \<lbrakk>Enc X Y \<in> analz (EncSet G K \<union> H); Enc X Y \<in> EncSet G K \<union> analz H; Y \<in> synth (analz (EncSet G K \<union> H) \<inter> {a. a \<in> EncSet G K \<union> analz H})\<rbrakk> \<Longrightarrow> X \<in> EncSet G K \<union> analz H
 5. \<And>X Y. \<lbrakk>Aenc X (pubK Y) \<in> analz (EncSet G K \<union> H); Aenc X (pubK Y) \<in> EncSet G K \<union> analz H; priK Y \<in> analz (EncSet G K \<union> H); priK Y \<in> EncSet G K \<union> analz H\<rbrakk> \<Longrightarrow> X \<in> EncSet G K \<union> analz H
 6. \<And>X Y. \<lbrakk>Aenc X (epubK Y) \<in> analz (EncSet G K \<union> H); Aenc X (epubK Y) \<in> EncSet G K \<union> analz H; epriK Y \<in> synth (analz (EncSet G K \<union> H) \<inter> {a. a \<in> EncSet G K \<union> analz H})\<rbrakk> \<Longrightarrow> X \<in> EncSet G K \<union> analz H
 7. \<And>X Y. \<lbrakk>Sign X (priK Y) \<in> analz (EncSet G K \<union> H); Sign X (priK Y) \<in> EncSet G K \<union> analz H; pubK Y \<in> analz (EncSet G K \<union> H); pubK Y \<in> EncSet G K \<union> analz H\<rbrakk> \<Longrightarrow> X \<in> EncSet G K \<union> analz H
[PROOF STEP]
case (Dec Y K')
[PROOF STATE]
proof (state)
this:
Enc Y K' \<in> analz (EncSet G K \<union> H)
Enc Y K' \<in> EncSet G K \<union> analz H
K' \<in> synth (analz (EncSet G K \<union> H) \<inter> {a. a \<in> EncSet G K \<union> analz H})

goal (7 subgoals):
 1. \<And>X. X \<in> EncSet G K \<union> H \<Longrightarrow> X \<in> EncSet G K \<union> analz H
 2. \<And>X Y. \<lbrakk>\<langle>X, Y\<rangle> \<in> analz (EncSet G K \<union> H); \<langle>X, Y\<rangle> \<in> EncSet G K \<union> analz H\<rbrakk> \<Longrightarrow> X \<in> EncSet G K \<union> analz H
 3. \<And>X Y. \<lbrakk>\<langle>X, Y\<rangle> \<in> analz (EncSet G K \<union> H); \<langle>X, Y\<rangle> \<in> EncSet G K \<union> analz H\<rbrakk> \<Longrightarrow> Y \<in> EncSet G K \<union> analz H
 4. \<And>X Y. \<lbrakk>Enc X Y \<in> analz (EncSet G K \<union> H); Enc X Y \<in> EncSet G K \<union> analz H; Y \<in> synth (analz (EncSet G K \<union> H) \<inter> {a. a \<in> EncSet G K \<union> analz H})\<rbrakk> \<Longrightarrow> X \<in> EncSet G K \<union> analz H
 5. \<And>X Y. \<lbrakk>Aenc X (pubK Y) \<in> analz (EncSet G K \<union> H); Aenc X (pubK Y) \<in> EncSet G K \<union> analz H; priK Y \<in> analz (EncSet G K \<union> H); priK Y \<in> EncSet G K \<union> analz H\<rbrakk> \<Longrightarrow> X \<in> EncSet G K \<union> analz H
 6. \<And>X Y. \<lbrakk>Aenc X (epubK Y) \<in> analz (EncSet G K \<union> H); Aenc X (epubK Y) \<in> EncSet G K \<union> analz H; epriK Y \<in> synth (analz (EncSet G K \<union> H) \<inter> {a. a \<in> EncSet G K \<union> analz H})\<rbrakk> \<Longrightarrow> X \<in> EncSet G K \<union> analz H
 7. \<And>X Y. \<lbrakk>Sign X (priK Y) \<in> analz (EncSet G K \<union> H); Sign X (priK Y) \<in> EncSet G K \<union> analz H; pubK Y \<in> analz (EncSet G K \<union> H); pubK Y \<in> EncSet G K \<union> analz H\<rbrakk> \<Longrightarrow> X \<in> EncSet G K \<union> analz H
[PROOF STEP]
from Dec.IH(1)
[PROOF STATE]
proof (chain)
picking this:
Enc Y K' \<in> EncSet G K \<union> analz H
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
Enc Y K' \<in> EncSet G K \<union> analz H

goal (1 subgoal):
 1. Y \<in> EncSet G K \<union> analz H
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. Enc Y K' \<in> EncSet G K \<Longrightarrow> Y \<in> EncSet G K \<union> analz H
 2. Enc Y K' \<in> analz H \<Longrightarrow> Y \<in> EncSet G K \<union> analz H
[PROOF STEP]
assume "Enc Y K' \<in> analz H"
[PROOF STATE]
proof (state)
this:
Enc Y K' \<in> analz H

goal (2 subgoals):
 1. Enc Y K' \<in> EncSet G K \<Longrightarrow> Y \<in> EncSet G K \<union> analz H
 2. Enc Y K' \<in> analz H \<Longrightarrow> Y \<in> EncSet G K \<union> analz H
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
Enc Y K' \<in> analz H

goal (2 subgoals):
 1. Enc Y K' \<in> EncSet G K \<Longrightarrow> Y \<in> EncSet G K \<union> analz H
 2. Enc Y K' \<in> analz H \<Longrightarrow> Y \<in> EncSet G K \<union> analz H
[PROOF STEP]
have "K' \<in> synth (analz H)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. K' \<in> synth (analz H)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. K' \<in> synth (analz H)
[PROOF STEP]
have "K' \<in> range LtK \<union> payload"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. K' \<in> range LtK \<union> payload
[PROOF STEP]
using \<open>Enc Y K' \<in> analz H\<close> assms(1)
[PROOF STATE]
proof (prove)
using this:
Enc Y K' \<in> analz H
Enc_keys_clean H

goal (1 subgoal):
 1. K' \<in> range LtK \<union> payload
[PROOF STEP]
by (auto dest: Enc_keys_clean_analz)
[PROOF STATE]
proof (state)
this:
K' \<in> range LtK \<union> payload

goal (1 subgoal):
 1. K' \<in> synth (analz H)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
K' \<in> range LtK \<union> payload

goal (1 subgoal):
 1. K' \<in> synth (analz H)
[PROOF STEP]
from Dec.IH(2)
[PROOF STATE]
proof (chain)
picking this:
K' \<in> synth (analz (EncSet G K \<union> H) \<inter> {a. a \<in> EncSet G K \<union> analz H})
[PROOF STEP]
have H: "K' \<in> synth (EncSet G K \<union> analz H)"
[PROOF STATE]
proof (prove)
using this:
K' \<in> synth (analz (EncSet G K \<union> H) \<inter> {a. a \<in> EncSet G K \<union> analz H})

goal (1 subgoal):
 1. K' \<in> synth (EncSet G K \<union> analz H)
[PROOF STEP]
by (auto simp add: Collect_disj_eq dest: synth_Int2)
[PROOF STATE]
proof (state)
this:
K' \<in> synth (EncSet G K \<union> analz H)

goal (1 subgoal):
 1. K' \<in> synth (analz H)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
K' \<in> synth (EncSet G K \<union> analz H)

goal (1 subgoal):
 1. K' \<in> synth (analz H)
[PROOF STEP]
hence "K' \<in> synth (analz H) \<union> -payload"
[PROOF STATE]
proof (prove)
using this:
K' \<in> synth (EncSet G K \<union> analz H)

goal (1 subgoal):
 1. K' \<in> synth (analz H) \<union> - payload
[PROOF STEP]
proof (rule synth_payload2 [THEN [2] rev_subsetD], auto elim!: payload_Enc)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>X Y. \<lbrakk>K' \<in> synth (EncSet G K \<union> analz H); X \<in> payload; Y \<in> payload; X \<in> G; Y \<in> K\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
fix X Y
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>X Y. \<lbrakk>K' \<in> synth (EncSet G K \<union> analz H); X \<in> payload; Y \<in> payload; X \<in> G; Y \<in> K\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
assume "Y \<in> K" "Y \<in> payload"
[PROOF STATE]
proof (state)
this:
Y \<in> K
Y \<in> payload

goal (1 subgoal):
 1. \<And>X Y. \<lbrakk>K' \<in> synth (EncSet G K \<union> analz H); X \<in> payload; Y \<in> payload; X \<in> G; Y \<in> K\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
with \<open>K \<subseteq> range LtK\<close>
[PROOF STATE]
proof (chain)
picking this:
K \<subseteq> range LtK
Y \<in> K
Y \<in> payload
[PROOF STEP]
obtain KK where "Y = LtK KK"
[PROOF STATE]
proof (prove)
using this:
K \<subseteq> range LtK
Y \<in> K
Y \<in> payload

goal (1 subgoal):
 1. (\<And>KK. Y = LtK KK \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Y = LtK KK

goal (1 subgoal):
 1. \<And>X Y. \<lbrakk>K' \<in> synth (EncSet G K \<union> analz H); X \<in> payload; Y \<in> payload; X \<in> G; Y \<in> K\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
with \<open>Y \<in> payload\<close>
[PROOF STATE]
proof (chain)
picking this:
Y \<in> payload
Y = LtK KK
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
Y \<in> payload
Y = LtK KK

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
K' \<in> synth (analz H) \<union> - payload

goal (1 subgoal):
 1. K' \<in> synth (analz H)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
K' \<in> range LtK \<union> payload
K' \<in> synth (EncSet G K \<union> analz H)
K' \<in> synth (analz H) \<union> - payload
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
K' \<in> range LtK \<union> payload
K' \<in> synth (EncSet G K \<union> analz H)
K' \<in> synth (analz H) \<union> - payload

goal (1 subgoal):
 1. K' \<in> synth (analz H)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
K' \<in> synth (analz H)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
K' \<in> synth (analz H)

goal (2 subgoals):
 1. Enc Y K' \<in> EncSet G K \<Longrightarrow> Y \<in> EncSet G K \<union> analz H
 2. Enc Y K' \<in> analz H \<Longrightarrow> Y \<in> EncSet G K \<union> analz H
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
Enc Y K' \<in> analz H
K' \<in> synth (analz H)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
Enc Y K' \<in> analz H
K' \<in> synth (analz H)

goal (1 subgoal):
 1. Y \<in> EncSet G K \<union> analz H
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Y \<in> EncSet G K \<union> analz H

goal (1 subgoal):
 1. Enc Y K' \<in> EncSet G K \<Longrightarrow> Y \<in> EncSet G K \<union> analz H
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Enc Y K' \<in> EncSet G K \<Longrightarrow> Y \<in> EncSet G K \<union> analz H
[PROOF STEP]
assume "Enc Y K' \<in> EncSet G K"
[PROOF STATE]
proof (state)
this:
Enc Y K' \<in> EncSet G K

goal (1 subgoal):
 1. Enc Y K' \<in> EncSet G K \<Longrightarrow> Y \<in> EncSet G K \<union> analz H
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
Enc Y K' \<in> EncSet G K

goal (1 subgoal):
 1. Enc Y K' \<in> EncSet G K \<Longrightarrow> Y \<in> EncSet G K \<union> analz H
[PROOF STEP]
hence "K' \<in> K"
[PROOF STATE]
proof (prove)
using this:
Enc Y K' \<in> EncSet G K

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

goal (1 subgoal):
 1. Enc Y K' \<in> EncSet G K \<Longrightarrow> Y \<in> EncSet G K \<union> analz H
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
K' \<in> K

goal (1 subgoal):
 1. Enc Y K' \<in> EncSet G K \<Longrightarrow> Y \<in> EncSet G K \<union> analz H
[PROOF STEP]
with \<open>K \<subseteq> range LtK\<close>
[PROOF STATE]
proof (chain)
picking this:
K \<subseteq> range LtK
K' \<in> K
[PROOF STEP]
obtain KK where "K' = LtK KK"
[PROOF STATE]
proof (prove)
using this:
K \<subseteq> range LtK
K' \<in> K

goal (1 subgoal):
 1. (\<And>KK. K' = LtK KK \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
K' = LtK KK

goal (1 subgoal):
 1. Enc Y K' \<in> EncSet G K \<Longrightarrow> Y \<in> EncSet G K \<union> analz H
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
K' = LtK KK

goal (1 subgoal):
 1. Enc Y K' \<in> EncSet G K \<Longrightarrow> Y \<in> EncSet G K \<union> analz H
[PROOF STEP]
with Dec.IH(2)
[PROOF STATE]
proof (chain)
picking this:
K' \<in> synth (analz (EncSet G K \<union> H) \<inter> {a. a \<in> EncSet G K \<union> analz H})
K' = LtK KK
[PROOF STEP]
have "K' \<in> analz H"
[PROOF STATE]
proof (prove)
using this:
K' \<in> synth (analz (EncSet G K \<union> H) \<inter> {a. a \<in> EncSet G K \<union> analz H})
K' = LtK KK

goal (1 subgoal):
 1. K' \<in> analz H
[PROOF STEP]
by (auto simp add: Collect_disj_eq dest: synth_Int2)
[PROOF STATE]
proof (state)
this:
K' \<in> analz H

goal (1 subgoal):
 1. Enc Y K' \<in> EncSet G K \<Longrightarrow> Y \<in> EncSet G K \<union> analz H
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
Enc Y K' \<in> EncSet G K
K' \<in> K
K' = LtK KK
K' \<in> analz H
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
Enc Y K' \<in> EncSet G K
K' \<in> K
K' = LtK KK
K' \<in> analz H

goal (1 subgoal):
 1. Y \<in> EncSet G K \<union> analz H
[PROOF STEP]
using \<open>K \<inter> synth (analz H) = {}\<close>
[PROOF STATE]
proof (prove)
using this:
Enc Y K' \<in> EncSet G K
K' \<in> K
K' = LtK KK
K' \<in> analz H
K \<inter> synth (analz H) = {}

goal (1 subgoal):
 1. Y \<in> EncSet G K \<union> analz H
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Y \<in> EncSet G K \<union> analz H

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
Y \<in> EncSet G K \<union> analz H

goal (6 subgoals):
 1. \<And>X. X \<in> EncSet G K \<union> H \<Longrightarrow> X \<in> EncSet G K \<union> analz H
 2. \<And>X Y. \<lbrakk>\<langle>X, Y\<rangle> \<in> analz (EncSet G K \<union> H); \<langle>X, Y\<rangle> \<in> EncSet G K \<union> analz H\<rbrakk> \<Longrightarrow> X \<in> EncSet G K \<union> analz H
 3. \<And>X Y. \<lbrakk>\<langle>X, Y\<rangle> \<in> analz (EncSet G K \<union> H); \<langle>X, Y\<rangle> \<in> EncSet G K \<union> analz H\<rbrakk> \<Longrightarrow> Y \<in> EncSet G K \<union> analz H
 4. \<And>X Y. \<lbrakk>Aenc X (pubK Y) \<in> analz (EncSet G K \<union> H); Aenc X (pubK Y) \<in> EncSet G K \<union> analz H; priK Y \<in> analz (EncSet G K \<union> H); priK Y \<in> EncSet G K \<union> analz H\<rbrakk> \<Longrightarrow> X \<in> EncSet G K \<union> analz H
 5. \<And>X Y. \<lbrakk>Aenc X (epubK Y) \<in> analz (EncSet G K \<union> H); Aenc X (epubK Y) \<in> EncSet G K \<union> analz H; epriK Y \<in> synth (analz (EncSet G K \<union> H) \<inter> {a. a \<in> EncSet G K \<union> analz H})\<rbrakk> \<Longrightarrow> X \<in> EncSet G K \<union> analz H
 6. \<And>X Y. \<lbrakk>Sign X (priK Y) \<in> analz (EncSet G K \<union> H); Sign X (priK Y) \<in> EncSet G K \<union> analz H; pubK Y \<in> analz (EncSet G K \<union> H); pubK Y \<in> EncSet G K \<union> analz H\<rbrakk> \<Longrightarrow> X \<in> EncSet G K \<union> analz H
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. \<And>X. X \<in> EncSet G K \<union> H \<Longrightarrow> X \<in> EncSet G K \<union> analz H
 2. \<And>X Y. \<lbrakk>\<langle>X, Y\<rangle> \<in> analz (EncSet G K \<union> H); \<langle>X, Y\<rangle> \<in> EncSet G K \<union> analz H\<rbrakk> \<Longrightarrow> X \<in> EncSet G K \<union> analz H
 3. \<And>X Y. \<lbrakk>\<langle>X, Y\<rangle> \<in> analz (EncSet G K \<union> H); \<langle>X, Y\<rangle> \<in> EncSet G K \<union> analz H\<rbrakk> \<Longrightarrow> Y \<in> EncSet G K \<union> analz H
 4. \<And>X Y. \<lbrakk>Aenc X (pubK Y) \<in> analz (EncSet G K \<union> H); Aenc X (pubK Y) \<in> EncSet G K \<union> analz H; priK Y \<in> analz (EncSet G K \<union> H); priK Y \<in> EncSet G K \<union> analz H\<rbrakk> \<Longrightarrow> X \<in> EncSet G K \<union> analz H
 5. \<And>X Y. \<lbrakk>Aenc X (epubK Y) \<in> analz (EncSet G K \<union> H); Aenc X (epubK Y) \<in> EncSet G K \<union> analz H; epriK Y \<in> synth (analz (EncSet G K \<union> H) \<inter> {a. a \<in> EncSet G K \<union> analz H})\<rbrakk> \<Longrightarrow> X \<in> EncSet G K \<union> analz H
 6. \<And>X Y. \<lbrakk>Sign X (priK Y) \<in> analz (EncSet G K \<union> H); Sign X (priK Y) \<in> EncSet G K \<union> analz H; pubK Y \<in> analz (EncSet G K \<union> H); pubK Y \<in> EncSet G K \<union> analz H\<rbrakk> \<Longrightarrow> X \<in> EncSet G K \<union> analz H
[PROOF STEP]
case (Adec_eph Y K')
[PROOF STATE]
proof (state)
this:
Aenc Y (epubK K') \<in> analz (EncSet G K \<union> H)
Aenc Y (epubK K') \<in> EncSet G K \<union> analz H
epriK K' \<in> synth (analz (EncSet G K \<union> H) \<inter> {a. a \<in> EncSet G K \<union> analz H})

goal (6 subgoals):
 1. \<And>X. X \<in> EncSet G K \<union> H \<Longrightarrow> X \<in> EncSet G K \<union> analz H
 2. \<And>X Y. \<lbrakk>\<langle>X, Y\<rangle> \<in> analz (EncSet G K \<union> H); \<langle>X, Y\<rangle> \<in> EncSet G K \<union> analz H\<rbrakk> \<Longrightarrow> X \<in> EncSet G K \<union> analz H
 3. \<And>X Y. \<lbrakk>\<langle>X, Y\<rangle> \<in> analz (EncSet G K \<union> H); \<langle>X, Y\<rangle> \<in> EncSet G K \<union> analz H\<rbrakk> \<Longrightarrow> Y \<in> EncSet G K \<union> analz H
 4. \<And>X Y. \<lbrakk>Aenc X (pubK Y) \<in> analz (EncSet G K \<union> H); Aenc X (pubK Y) \<in> EncSet G K \<union> analz H; priK Y \<in> analz (EncSet G K \<union> H); priK Y \<in> EncSet G K \<union> analz H\<rbrakk> \<Longrightarrow> X \<in> EncSet G K \<union> analz H
 5. \<And>X Y. \<lbrakk>Aenc X (epubK Y) \<in> analz (EncSet G K \<union> H); Aenc X (epubK Y) \<in> EncSet G K \<union> analz H; epriK Y \<in> synth (analz (EncSet G K \<union> H) \<inter> {a. a \<in> EncSet G K \<union> analz H})\<rbrakk> \<Longrightarrow> X \<in> EncSet G K \<union> analz H
 6. \<And>X Y. \<lbrakk>Sign X (priK Y) \<in> analz (EncSet G K \<union> H); Sign X (priK Y) \<in> EncSet G K \<union> analz H; pubK Y \<in> analz (EncSet G K \<union> H); pubK Y \<in> EncSet G K \<union> analz H\<rbrakk> \<Longrightarrow> X \<in> EncSet G K \<union> analz H
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
Aenc Y (epubK K') \<in> analz (EncSet G K \<union> H)
Aenc Y (epubK K') \<in> EncSet G K \<union> analz H
epriK K' \<in> synth (analz (EncSet G K \<union> H) \<inter> {a. a \<in> EncSet G K \<union> analz H})

goal (1 subgoal):
 1. Y \<in> EncSet G K \<union> analz H
[PROOF STEP]
by (auto dest!: EpriK_synth)
[PROOF STATE]
proof (state)
this:
Y \<in> EncSet G K \<union> analz H

goal (5 subgoals):
 1. \<And>X. X \<in> EncSet G K \<union> H \<Longrightarrow> X \<in> EncSet G K \<union> analz H
 2. \<And>X Y. \<lbrakk>\<langle>X, Y\<rangle> \<in> analz (EncSet G K \<union> H); \<langle>X, Y\<rangle> \<in> EncSet G K \<union> analz H\<rbrakk> \<Longrightarrow> X \<in> EncSet G K \<union> analz H
 3. \<And>X Y. \<lbrakk>\<langle>X, Y\<rangle> \<in> analz (EncSet G K \<union> H); \<langle>X, Y\<rangle> \<in> EncSet G K \<union> analz H\<rbrakk> \<Longrightarrow> Y \<in> EncSet G K \<union> analz H
 4. \<And>X Y. \<lbrakk>Aenc X (pubK Y) \<in> analz (EncSet G K \<union> H); Aenc X (pubK Y) \<in> EncSet G K \<union> analz H; priK Y \<in> analz (EncSet G K \<union> H); priK Y \<in> EncSet G K \<union> analz H\<rbrakk> \<Longrightarrow> X \<in> EncSet G K \<union> analz H
 5. \<And>X Y. \<lbrakk>Sign X (priK Y) \<in> analz (EncSet G K \<union> H); Sign X (priK Y) \<in> EncSet G K \<union> analz H; pubK Y \<in> analz (EncSet G K \<union> H); pubK Y \<in> EncSet G K \<union> analz H\<rbrakk> \<Longrightarrow> X \<in> EncSet G K \<union> analz H
[PROOF STEP]
qed (insert assms(2), auto)
[PROOF STATE]
proof (state)
this:
X \<in> EncSet G K \<union> analz H

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma index_less_size_conv:
  "(index xs x < size xs) = (x \<in> set xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (index xs x < length xs) = (x \<in> set xs)
[PROOF STEP]
by(auto simp: index_def find_index_less_size_conv)


[STATEMENT]
lemma bind_is_OK_E3 [elim]:
  assumes "h \<turnstile> ok (f \<bind> g)" and "pure f h"
  obtains x where "h \<turnstile> f \<rightarrow>\<^sub>r x"  and "h \<turnstile> ok (g x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>x. \<lbrakk>h \<turnstile> f \<rightarrow>\<^sub>r x; h \<turnstile> ok g x\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
h \<turnstile> ok Heap_Error_Monad.bind f g
pure f h

goal (1 subgoal):
 1. (\<And>x. \<lbrakk>h \<turnstile> f \<rightarrow>\<^sub>r x; h \<turnstile> ok g x\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(auto simp add: bind_def returns_result_def returns_heap_def is_OK_def execute_def pure_def
               split: sum.splits)


[STATEMENT]
lemma adopt_node_types_preserved:
  assumes "w \<in> adopt_node_locs parent owner_document document_ptr"
  assumes "h \<turnstile> w \<rightarrow>\<^sub>h h'"
  shows "type_wf h = type_wf h'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. type_wf h = type_wf h'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
w \<in> adopt_node_locs parent owner_document document_ptr
h \<turnstile> w \<rightarrow>\<^sub>h h'

goal (1 subgoal):
 1. type_wf h = type_wf h'
[PROOF STEP]
using remove_child_types_preserved
[PROOF STATE]
proof (prove)
using this:
w \<in> adopt_node_locs parent owner_document document_ptr
h \<turnstile> w \<rightarrow>\<^sub>h h'
\<lbrakk>?w \<in> remove_child_locs ?ptr ?owner_document; ?h \<turnstile> ?w \<rightarrow>\<^sub>h ?h'\<rbrakk> \<Longrightarrow> type_wf ?h = type_wf ?h'

goal (1 subgoal):
 1. type_wf h = type_wf h'
[PROOF STEP]
using set_disconnected_nodes_types_preserved
[PROOF STATE]
proof (prove)
using this:
w \<in> adopt_node_locs parent owner_document document_ptr
h \<turnstile> w \<rightarrow>\<^sub>h h'
\<lbrakk>?w \<in> remove_child_locs ?ptr ?owner_document; ?h \<turnstile> ?w \<rightarrow>\<^sub>h ?h'\<rbrakk> \<Longrightarrow> type_wf ?h = type_wf ?h'
\<lbrakk>?w \<in> set_disconnected_nodes_locs ?document_ptr; ?h \<turnstile> ?w \<rightarrow>\<^sub>h ?h'\<rbrakk> \<Longrightarrow> type_wf ?h = type_wf ?h'

goal (1 subgoal):
 1. type_wf h = type_wf h'
[PROOF STEP]
unfolding adopt_node_locs_def
[PROOF STATE]
proof (prove)
using this:
w \<in> (if parent = None then {} else remove_child_locs (the parent) owner_document) \<union> set_disconnected_nodes_locs document_ptr \<union> set_disconnected_nodes_locs owner_document
h \<turnstile> w \<rightarrow>\<^sub>h h'
\<lbrakk>?w \<in> remove_child_locs ?ptr ?owner_document; ?h \<turnstile> ?w \<rightarrow>\<^sub>h ?h'\<rbrakk> \<Longrightarrow> type_wf ?h = type_wf ?h'
\<lbrakk>?w \<in> set_disconnected_nodes_locs ?document_ptr; ?h \<turnstile> ?w \<rightarrow>\<^sub>h ?h'\<rbrakk> \<Longrightarrow> type_wf ?h = type_wf ?h'

goal (1 subgoal):
 1. type_wf h = type_wf h'
[PROOF STEP]
by (auto split: if_splits)


[STATEMENT]
lemma refine_basic:
  "\<lbrakk> init Tc \<subseteq> R``(init Ta); {R} (trans Ta), (trans Tc) {> R} \<rbrakk>
  \<Longrightarrow> PO_refines R Ta Tc"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>init Tc \<subseteq> R `` init Ta; {R} TS.trans Ta, TS.trans Tc {> R}\<rbrakk> \<Longrightarrow> PO_refines R Ta Tc
[PROOF STEP]
by (simp add: PO_refines_def)


[STATEMENT]
lemma ZFfunApp:
  assumes "x |\<in>| A"
  shows   "(ZFfun A B f) |@| x = f x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ZFfun A B f |@| x = f x
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ZFfun A B f |@| x = f x
[PROOF STEP]
have "(ZFfun A B f) |@| x = app (Lambda A f) x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ZFfun A B f |@| x = Lambda A f \<acute> x
[PROOF STEP]
by (simp add: ZFfun_def ZFfunApp_def Snd)
[PROOF STATE]
proof (state)
this:
ZFfun A B f |@| x = Lambda A f \<acute> x

goal (1 subgoal):
 1. ZFfun A B f |@| x = f x
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
ZFfun A B f |@| x = Lambda A f \<acute> x

goal (1 subgoal):
 1. ZFfun A B f |@| x = f x
[PROOF STEP]
have "... = f x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Lambda A f \<acute> x = f x
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
x |\<in>| A

goal (1 subgoal):
 1. Lambda A f \<acute> x = f x
[PROOF STEP]
by (simp add: Lambda_app)
[PROOF STATE]
proof (state)
this:
Lambda A f \<acute> x = f x

goal (1 subgoal):
 1. ZFfun A B f |@| x = f x
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
ZFfun A B f |@| x = f x
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
ZFfun A B f |@| x = f x

goal (1 subgoal):
 1. ZFfun A B f |@| x = f x
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
ZFfun A B f |@| x = f x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma add_conj_le:
  shows "z + cnj z \<le> 2 * cmod z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. z + cnj z \<le> complex_of_real (2 * cmod z)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. z + cnj z \<le> complex_of_real (2 * cmod z)
[PROOF STEP]
have z: "z + cnj z = 2 * Re z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. z + cnj z = complex_of_real (2 * Re z)
[PROOF STEP]
by (simp add: complex_add_cnj)
[PROOF STATE]
proof (state)
this:
z + cnj z = complex_of_real (2 * Re z)

goal (1 subgoal):
 1. z + cnj z \<le> complex_of_real (2 * cmod z)
[PROOF STEP]
have "Re z \<le> cmod z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Re z \<le> cmod z
[PROOF STEP]
by (simp add: complex_Re_le_cmod)
[PROOF STATE]
proof (state)
this:
Re z \<le> cmod z

goal (1 subgoal):
 1. z + cnj z \<le> complex_of_real (2 * cmod z)
[PROOF STEP]
hence "2 *complex_of_real (Re z) \<le> 2 * complex_of_real (cmod z)"
[PROOF STATE]
proof (prove)
using this:
Re z \<le> cmod z

goal (1 subgoal):
 1. 2 * complex_of_real (Re z) \<le> 2 * complex_of_real (cmod z)
[PROOF STEP]
using less_eq_complex_def
[PROOF STATE]
proof (prove)
using this:
Re z \<le> cmod z
(?x \<le> ?y) = (Re ?x \<le> Re ?y \<and> Im ?x = Im ?y)

goal (1 subgoal):
 1. 2 * complex_of_real (Re z) \<le> 2 * complex_of_real (cmod z)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
2 * complex_of_real (Re z) \<le> 2 * complex_of_real (cmod z)

goal (1 subgoal):
 1. z + cnj z \<le> complex_of_real (2 * cmod z)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
2 * complex_of_real (Re z) \<le> 2 * complex_of_real (cmod z)

goal (1 subgoal):
 1. z + cnj z \<le> complex_of_real (2 * cmod z)
[PROOF STEP]
using z
[PROOF STATE]
proof (prove)
using this:
2 * complex_of_real (Re z) \<le> 2 * complex_of_real (cmod z)
z + cnj z = complex_of_real (2 * Re z)

goal (1 subgoal):
 1. z + cnj z \<le> complex_of_real (2 * cmod z)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
z + cnj z \<le> complex_of_real (2 * cmod z)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem eta_expansion_safe':
  assumes "n \<le> arg_prefix S"
  shows "(\<Gamma>, eta_expand n e, S) \<Rightarrow>\<^sup>* (\<Gamma>, e, S)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Gamma>, eta_expand n e, S) \<Rightarrow>\<^sup>* (\<Gamma>, e, S)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<Gamma>, eta_expand n e, S) \<Rightarrow>\<^sup>* (\<Gamma>, e, S)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
n \<le> arg_prefix S
[PROOF STEP]
have "set (take n S) \<subseteq> range Arg" and "length (take n S) = n"
[PROOF STATE]
proof (prove)
using this:
n \<le> arg_prefix S

goal (1 subgoal):
 1. set (take n S) \<subseteq> range Arg &&& length (take n S) = n
[PROOF STEP]
apply (induction S arbitrary: n rule: arg_prefix.induct)
[PROOF STATE]
proof (prove)
goal (10 subgoals):
 1. \<And>n. n \<le> arg_prefix [] \<Longrightarrow> set (take n []) \<subseteq> range Arg
 2. \<And>n. n \<le> arg_prefix [] \<Longrightarrow> length (take n []) = n
 3. \<And>x S n. \<lbrakk>\<And>n. n \<le> arg_prefix S \<Longrightarrow> set (take n S) \<subseteq> range Arg; \<And>n. n \<le> arg_prefix S \<Longrightarrow> length (take n S) = n; n \<le> arg_prefix (Arg x # S)\<rbrakk> \<Longrightarrow> set (take n (Arg x # S)) \<subseteq> range Arg
 4. \<And>x S n. \<lbrakk>\<And>n. n \<le> arg_prefix S \<Longrightarrow> set (take n S) \<subseteq> range Arg; \<And>n. n \<le> arg_prefix S \<Longrightarrow> length (take n S) = n; n \<le> arg_prefix (Arg x # S)\<rbrakk> \<Longrightarrow> length (take n (Arg x # S)) = n
 5. \<And>e1 e2 S n. n \<le> arg_prefix (Alts e1 e2 # S) \<Longrightarrow> set (take n (Alts e1 e2 # S)) \<subseteq> range Arg
 6. \<And>e1 e2 S n. n \<le> arg_prefix (Alts e1 e2 # S) \<Longrightarrow> length (take n (Alts e1 e2 # S)) = n
 7. \<And>x S n. n \<le> arg_prefix (Upd x # S) \<Longrightarrow> set (take n (Upd x # S)) \<subseteq> range Arg
 8. \<And>x S n. n \<le> arg_prefix (Upd x # S) \<Longrightarrow> length (take n (Upd x # S)) = n
 9. \<And>x S n. n \<le> arg_prefix (Dummy x # S) \<Longrightarrow> set (take n (Dummy x # S)) \<subseteq> range Arg
 10. \<And>x S n. n \<le> arg_prefix (Dummy x # S) \<Longrightarrow> length (take n (Dummy x # S)) = n
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x S n xa. \<lbrakk>\<And>n. n \<le> arg_prefix S \<Longrightarrow> set (take n S) \<subseteq> range Arg; \<And>n. n \<le> arg_prefix S \<Longrightarrow> min (length S) n = n; n \<le> Suc (arg_prefix S); xa \<in> set (take n (Arg x # S))\<rbrakk> \<Longrightarrow> xa \<in> range Arg
 2. \<And>S n. \<lbrakk>\<And>n. n \<le> arg_prefix S \<Longrightarrow> set (take n S) \<subseteq> range Arg; \<And>n. n \<le> arg_prefix S \<Longrightarrow> min (length S) n = n; n \<le> Suc (arg_prefix S)\<rbrakk> \<Longrightarrow> min (Suc (length S)) n = n
[PROOF STEP]
apply (case_tac n, auto)+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
set (take n S) \<subseteq> range Arg
length (take n S) = n

goal (1 subgoal):
 1. (\<Gamma>, eta_expand n e, S) \<Rightarrow>\<^sup>* (\<Gamma>, e, S)
[PROOF STEP]
hence "S = take n S @ drop n S"
[PROOF STATE]
proof (prove)
using this:
set (take n S) \<subseteq> range Arg
length (take n S) = n

goal (1 subgoal):
 1. S = take n S @ drop n S
[PROOF STEP]
by (metis append_take_drop_id)
[PROOF STATE]
proof (state)
this:
S = take n S @ drop n S

goal (1 subgoal):
 1. (\<Gamma>, eta_expand n e, S) \<Rightarrow>\<^sup>* (\<Gamma>, e, S)
[PROOF STEP]
with eta_expansion_safe[OF \<open>_ \<subseteq> _\<close>] \<open>length _ = _\<close>
[PROOF STATE]
proof (chain)
picking this:
(?\<Gamma>, eta_expand (length (take n S)) ?e, take n S @ ?S) \<Rightarrow>\<^sup>* (?\<Gamma>, ?e, take n S @ ?S)
length (take n S) = n
S = take n S @ drop n S
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(?\<Gamma>, eta_expand (length (take n S)) ?e, take n S @ ?S) \<Rightarrow>\<^sup>* (?\<Gamma>, ?e, take n S @ ?S)
length (take n S) = n
S = take n S @ drop n S

goal (1 subgoal):
 1. (\<Gamma>, eta_expand n e, S) \<Rightarrow>\<^sup>* (\<Gamma>, e, S)
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
(\<Gamma>, eta_expand n e, S) \<Rightarrow>\<^sup>* (\<Gamma>, e, S)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma map_step:
  assumes "inj g" "vs = vs' \<circ> g" "((s, vs), (t, ws)) \<in> step M"
  shows "((f s, vs'), (f t, \<lambda>x. if x \<in> range g then ws (inv g x) else vs' x)) \<in> step (map_minsky f g M)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((f s, vs'), f t, \<lambda>x. if x \<in> range g then ws (inv g x) else vs' x) \<in> step (map_minsky f g M)
[PROOF STEP]
using assms(3)
[PROOF STATE]
proof (prove)
using this:
((s, vs), t, ws) \<in> step M

goal (1 subgoal):
 1. ((f s, vs'), f t, \<lambda>x. if x \<in> range g then ws (inv g x) else vs' x) \<in> step (map_minsky f g M)
[PROOF STEP]
proof (cases rule: step.cases)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>v. \<lbrakk>ws = (\<lambda>x. if x = v then Suc (vs v) else vs x); (s, Inc v t) \<in> M\<rbrakk> \<Longrightarrow> ((f s, vs'), f t, \<lambda>x. if x \<in> range g then ws (inv g x) else vs' x) \<in> step (map_minsky f g M)
 2. \<And>v sz n. \<lbrakk>ws = (\<lambda>x. if x = v then n else vs x); (s, Dec v t sz) \<in> M; vs v = Suc n\<rbrakk> \<Longrightarrow> ((f s, vs'), f t, \<lambda>x. if x \<in> range g then ws (inv g x) else vs' x) \<in> step (map_minsky f g M)
 3. \<And>v sn. \<lbrakk>ws = vs; (s, Dec v sn t) \<in> M; vs v = 0\<rbrakk> \<Longrightarrow> ((f s, vs'), f t, \<lambda>x. if x \<in> range g then ws (inv g x) else vs' x) \<in> step (map_minsky f g M)
[PROOF STEP]
case (inc v)
[PROOF STATE]
proof (state)
this:
ws = (\<lambda>x. if x = v then Suc (vs v) else vs x)
(s, Inc v t) \<in> M

goal (3 subgoals):
 1. \<And>v. \<lbrakk>ws = (\<lambda>x. if x = v then Suc (vs v) else vs x); (s, Inc v t) \<in> M\<rbrakk> \<Longrightarrow> ((f s, vs'), f t, \<lambda>x. if x \<in> range g then ws (inv g x) else vs' x) \<in> step (map_minsky f g M)
 2. \<And>v sz n. \<lbrakk>ws = (\<lambda>x. if x = v then n else vs x); (s, Dec v t sz) \<in> M; vs v = Suc n\<rbrakk> \<Longrightarrow> ((f s, vs'), f t, \<lambda>x. if x \<in> range g then ws (inv g x) else vs' x) \<in> step (map_minsky f g M)
 3. \<And>v sn. \<lbrakk>ws = vs; (s, Dec v sn t) \<in> M; vs v = 0\<rbrakk> \<Longrightarrow> ((f s, vs'), f t, \<lambda>x. if x \<in> range g then ws (inv g x) else vs' x) \<in> step (map_minsky f g M)
[PROOF STEP]
note [simp] = inc(1)
[PROOF STATE]
proof (state)
this:
ws = (\<lambda>x. if x = v then Suc (vs v) else vs x)

goal (3 subgoals):
 1. \<And>v. \<lbrakk>ws = (\<lambda>x. if x = v then Suc (vs v) else vs x); (s, Inc v t) \<in> M\<rbrakk> \<Longrightarrow> ((f s, vs'), f t, \<lambda>x. if x \<in> range g then ws (inv g x) else vs' x) \<in> step (map_minsky f g M)
 2. \<And>v sz n. \<lbrakk>ws = (\<lambda>x. if x = v then n else vs x); (s, Dec v t sz) \<in> M; vs v = Suc n\<rbrakk> \<Longrightarrow> ((f s, vs'), f t, \<lambda>x. if x \<in> range g then ws (inv g x) else vs' x) \<in> step (map_minsky f g M)
 3. \<And>v sn. \<lbrakk>ws = vs; (s, Dec v sn t) \<in> M; vs v = 0\<rbrakk> \<Longrightarrow> ((f s, vs'), f t, \<lambda>x. if x \<in> range g then ws (inv g x) else vs' x) \<in> step (map_minsky f g M)
[PROOF STEP]
let ?ws' = "\<lambda>w. if w = g v then Suc (vs' (g v)) else vs' w"
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>v. \<lbrakk>ws = (\<lambda>x. if x = v then Suc (vs v) else vs x); (s, Inc v t) \<in> M\<rbrakk> \<Longrightarrow> ((f s, vs'), f t, \<lambda>x. if x \<in> range g then ws (inv g x) else vs' x) \<in> step (map_minsky f g M)
 2. \<And>v sz n. \<lbrakk>ws = (\<lambda>x. if x = v then n else vs x); (s, Dec v t sz) \<in> M; vs v = Suc n\<rbrakk> \<Longrightarrow> ((f s, vs'), f t, \<lambda>x. if x \<in> range g then ws (inv g x) else vs' x) \<in> step (map_minsky f g M)
 3. \<And>v sn. \<lbrakk>ws = vs; (s, Dec v sn t) \<in> M; vs v = 0\<rbrakk> \<Longrightarrow> ((f s, vs'), f t, \<lambda>x. if x \<in> range g then ws (inv g x) else vs' x) \<in> step (map_minsky f g M)
[PROOF STEP]
have "((f s, vs'), (f t, ?ws')) \<in> step (map_minsky f g M)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((f s, vs'), f t, \<lambda>w. if w = g v then Suc (vs' (g v)) else vs' w) \<in> step (map_minsky f g M)
[PROOF STEP]
using inc(2) step.inc[of "f s" "g v" "f t" "map_minsky f g M" vs']
[PROOF STATE]
proof (prove)
using this:
(s, Inc v t) \<in> M
(f s, Inc (g v) (f t)) \<in> map_minsky f g M \<Longrightarrow> ((f s, vs'), f t, \<lambda>x. if x = g v then Suc (vs' (g v)) else vs' x) \<in> step (map_minsky f g M)

goal (1 subgoal):
 1. ((f s, vs'), f t, \<lambda>w. if w = g v then Suc (vs' (g v)) else vs' w) \<in> step (map_minsky f g M)
[PROOF STEP]
by (force simp: map_minsky_def)
[PROOF STATE]
proof (state)
this:
((f s, vs'), f t, \<lambda>w. if w = g v then Suc (vs' (g v)) else vs' w) \<in> step (map_minsky f g M)

goal (3 subgoals):
 1. \<And>v. \<lbrakk>ws = (\<lambda>x. if x = v then Suc (vs v) else vs x); (s, Inc v t) \<in> M\<rbrakk> \<Longrightarrow> ((f s, vs'), f t, \<lambda>x. if x \<in> range g then ws (inv g x) else vs' x) \<in> step (map_minsky f g M)
 2. \<And>v sz n. \<lbrakk>ws = (\<lambda>x. if x = v then n else vs x); (s, Dec v t sz) \<in> M; vs v = Suc n\<rbrakk> \<Longrightarrow> ((f s, vs'), f t, \<lambda>x. if x \<in> range g then ws (inv g x) else vs' x) \<in> step (map_minsky f g M)
 3. \<And>v sn. \<lbrakk>ws = vs; (s, Dec v sn t) \<in> M; vs v = 0\<rbrakk> \<Longrightarrow> ((f s, vs'), f t, \<lambda>x. if x \<in> range g then ws (inv g x) else vs' x) \<in> step (map_minsky f g M)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
((f s, vs'), f t, \<lambda>w. if w = g v then Suc (vs' (g v)) else vs' w) \<in> step (map_minsky f g M)

goal (3 subgoals):
 1. \<And>v. \<lbrakk>ws = (\<lambda>x. if x = v then Suc (vs v) else vs x); (s, Inc v t) \<in> M\<rbrakk> \<Longrightarrow> ((f s, vs'), f t, \<lambda>x. if x \<in> range g then ws (inv g x) else vs' x) \<in> step (map_minsky f g M)
 2. \<And>v sz n. \<lbrakk>ws = (\<lambda>x. if x = v then n else vs x); (s, Dec v t sz) \<in> M; vs v = Suc n\<rbrakk> \<Longrightarrow> ((f s, vs'), f t, \<lambda>x. if x \<in> range g then ws (inv g x) else vs' x) \<in> step (map_minsky f g M)
 3. \<And>v sn. \<lbrakk>ws = vs; (s, Dec v sn t) \<in> M; vs v = 0\<rbrakk> \<Longrightarrow> ((f s, vs'), f t, \<lambda>x. if x \<in> range g then ws (inv g x) else vs' x) \<in> step (map_minsky f g M)
[PROOF STEP]
have "(\<lambda>x. if x \<in> range g then ws (inv g x) else vs' x) = ?ws'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. if x \<in> range g then ws (inv g x) else vs' x) = (\<lambda>w. if w = g v then Suc (vs' (g v)) else vs' w)
[PROOF STEP]
using assms(1,2)
[PROOF STATE]
proof (prove)
using this:
inj g
vs = vs' \<circ> g

goal (1 subgoal):
 1. (\<lambda>x. if x \<in> range g then ws (inv g x) else vs' x) = (\<lambda>w. if w = g v then Suc (vs' (g v)) else vs' w)
[PROOF STEP]
by (auto intro!: ext simp: injD image_def)
[PROOF STATE]
proof (state)
this:
(\<lambda>x. if x \<in> range g then ws (inv g x) else vs' x) = (\<lambda>w. if w = g v then Suc (vs' (g v)) else vs' w)

goal (3 subgoals):
 1. \<And>v. \<lbrakk>ws = (\<lambda>x. if x = v then Suc (vs v) else vs x); (s, Inc v t) \<in> M\<rbrakk> \<Longrightarrow> ((f s, vs'), f t, \<lambda>x. if x \<in> range g then ws (inv g x) else vs' x) \<in> step (map_minsky f g M)
 2. \<And>v sz n. \<lbrakk>ws = (\<lambda>x. if x = v then n else vs x); (s, Dec v t sz) \<in> M; vs v = Suc n\<rbrakk> \<Longrightarrow> ((f s, vs'), f t, \<lambda>x. if x \<in> range g then ws (inv g x) else vs' x) \<in> step (map_minsky f g M)
 3. \<And>v sn. \<lbrakk>ws = vs; (s, Dec v sn t) \<in> M; vs v = 0\<rbrakk> \<Longrightarrow> ((f s, vs'), f t, \<lambda>x. if x \<in> range g then ws (inv g x) else vs' x) \<in> step (map_minsky f g M)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
((f s, vs'), f t, \<lambda>w. if w = g v then Suc (vs' (g v)) else vs' w) \<in> step (map_minsky f g M)
(\<lambda>x. if x \<in> range g then ws (inv g x) else vs' x) = (\<lambda>w. if w = g v then Suc (vs' (g v)) else vs' w)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
((f s, vs'), f t, \<lambda>w. if w = g v then Suc (vs' (g v)) else vs' w) \<in> step (map_minsky f g M)
(\<lambda>x. if x \<in> range g then ws (inv g x) else vs' x) = (\<lambda>w. if w = g v then Suc (vs' (g v)) else vs' w)

goal (1 subgoal):
 1. ((f s, vs'), f t, \<lambda>x. if x \<in> range g then ws (inv g x) else vs' x) \<in> step (map_minsky f g M)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
((f s, vs'), f t, \<lambda>x. if x \<in> range g then ws (inv g x) else vs' x) \<in> step (map_minsky f g M)

goal (2 subgoals):
 1. \<And>v sz n. \<lbrakk>ws = (\<lambda>x. if x = v then n else vs x); (s, Dec v t sz) \<in> M; vs v = Suc n\<rbrakk> \<Longrightarrow> ((f s, vs'), f t, \<lambda>x. if x \<in> range g then ws (inv g x) else vs' x) \<in> step (map_minsky f g M)
 2. \<And>v sn. \<lbrakk>ws = vs; (s, Dec v sn t) \<in> M; vs v = 0\<rbrakk> \<Longrightarrow> ((f s, vs'), f t, \<lambda>x. if x \<in> range g then ws (inv g x) else vs' x) \<in> step (map_minsky f g M)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>v sz n. \<lbrakk>ws = (\<lambda>x. if x = v then n else vs x); (s, Dec v t sz) \<in> M; vs v = Suc n\<rbrakk> \<Longrightarrow> ((f s, vs'), f t, \<lambda>x. if x \<in> range g then ws (inv g x) else vs' x) \<in> step (map_minsky f g M)
 2. \<And>v sn. \<lbrakk>ws = vs; (s, Dec v sn t) \<in> M; vs v = 0\<rbrakk> \<Longrightarrow> ((f s, vs'), f t, \<lambda>x. if x \<in> range g then ws (inv g x) else vs' x) \<in> step (map_minsky f g M)
[PROOF STEP]
case (decn v sz n)
[PROOF STATE]
proof (state)
this:
ws = (\<lambda>x. if x = v then n else vs x)
(s, Dec v t sz) \<in> M
vs v = Suc n

goal (2 subgoals):
 1. \<And>v sz n. \<lbrakk>ws = (\<lambda>x. if x = v then n else vs x); (s, Dec v t sz) \<in> M; vs v = Suc n\<rbrakk> \<Longrightarrow> ((f s, vs'), f t, \<lambda>x. if x \<in> range g then ws (inv g x) else vs' x) \<in> step (map_minsky f g M)
 2. \<And>v sn. \<lbrakk>ws = vs; (s, Dec v sn t) \<in> M; vs v = 0\<rbrakk> \<Longrightarrow> ((f s, vs'), f t, \<lambda>x. if x \<in> range g then ws (inv g x) else vs' x) \<in> step (map_minsky f g M)
[PROOF STEP]
note [simp] = decn(1)
[PROOF STATE]
proof (state)
this:
ws = (\<lambda>x. if x = v then n else vs x)

goal (2 subgoals):
 1. \<And>v sz n. \<lbrakk>ws = (\<lambda>x. if x = v then n else vs x); (s, Dec v t sz) \<in> M; vs v = Suc n\<rbrakk> \<Longrightarrow> ((f s, vs'), f t, \<lambda>x. if x \<in> range g then ws (inv g x) else vs' x) \<in> step (map_minsky f g M)
 2. \<And>v sn. \<lbrakk>ws = vs; (s, Dec v sn t) \<in> M; vs v = 0\<rbrakk> \<Longrightarrow> ((f s, vs'), f t, \<lambda>x. if x \<in> range g then ws (inv g x) else vs' x) \<in> step (map_minsky f g M)
[PROOF STEP]
let ?ws' = "\<lambda>x. if x = g v then n else vs' x"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>v sz n. \<lbrakk>ws = (\<lambda>x. if x = v then n else vs x); (s, Dec v t sz) \<in> M; vs v = Suc n\<rbrakk> \<Longrightarrow> ((f s, vs'), f t, \<lambda>x. if x \<in> range g then ws (inv g x) else vs' x) \<in> step (map_minsky f g M)
 2. \<And>v sn. \<lbrakk>ws = vs; (s, Dec v sn t) \<in> M; vs v = 0\<rbrakk> \<Longrightarrow> ((f s, vs'), f t, \<lambda>x. if x \<in> range g then ws (inv g x) else vs' x) \<in> step (map_minsky f g M)
[PROOF STEP]
have "((f s, vs'), (f t, ?ws')) \<in> step (map_minsky f g M)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((f s, vs'), f t, \<lambda>x. if x = g v then n else vs' x) \<in> step (map_minsky f g M)
[PROOF STEP]
using assms(2) decn(2-) step.decn[of "f s" "g v" "f t" "f sz" "map_minsky f g M" vs' n]
[PROOF STATE]
proof (prove)
using this:
vs = vs' \<circ> g
(s, Dec v t sz) \<in> M
vs v = Suc n
\<lbrakk>(f s, Dec (g v) (f t) (f sz)) \<in> map_minsky f g M; vs' (g v) = Suc n\<rbrakk> \<Longrightarrow> ((f s, vs'), f t, \<lambda>x. if x = g v then n else vs' x) \<in> step (map_minsky f g M)

goal (1 subgoal):
 1. ((f s, vs'), f t, \<lambda>x. if x = g v then n else vs' x) \<in> step (map_minsky f g M)
[PROOF STEP]
by (force simp: map_minsky_def)
[PROOF STATE]
proof (state)
this:
((f s, vs'), f t, \<lambda>x. if x = g v then n else vs' x) \<in> step (map_minsky f g M)

goal (2 subgoals):
 1. \<And>v sz n. \<lbrakk>ws = (\<lambda>x. if x = v then n else vs x); (s, Dec v t sz) \<in> M; vs v = Suc n\<rbrakk> \<Longrightarrow> ((f s, vs'), f t, \<lambda>x. if x \<in> range g then ws (inv g x) else vs' x) \<in> step (map_minsky f g M)
 2. \<And>v sn. \<lbrakk>ws = vs; (s, Dec v sn t) \<in> M; vs v = 0\<rbrakk> \<Longrightarrow> ((f s, vs'), f t, \<lambda>x. if x \<in> range g then ws (inv g x) else vs' x) \<in> step (map_minsky f g M)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
((f s, vs'), f t, \<lambda>x. if x = g v then n else vs' x) \<in> step (map_minsky f g M)

goal (2 subgoals):
 1. \<And>v sz n. \<lbrakk>ws = (\<lambda>x. if x = v then n else vs x); (s, Dec v t sz) \<in> M; vs v = Suc n\<rbrakk> \<Longrightarrow> ((f s, vs'), f t, \<lambda>x. if x \<in> range g then ws (inv g x) else vs' x) \<in> step (map_minsky f g M)
 2. \<And>v sn. \<lbrakk>ws = vs; (s, Dec v sn t) \<in> M; vs v = 0\<rbrakk> \<Longrightarrow> ((f s, vs'), f t, \<lambda>x. if x \<in> range g then ws (inv g x) else vs' x) \<in> step (map_minsky f g M)
[PROOF STEP]
have "(\<lambda>x. if x \<in> range g then ws (inv g x) else vs' x) = ?ws'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. if x \<in> range g then ws (inv g x) else vs' x) = (\<lambda>x. if x = g v then n else vs' x)
[PROOF STEP]
using assms(1,2)
[PROOF STATE]
proof (prove)
using this:
inj g
vs = vs' \<circ> g

goal (1 subgoal):
 1. (\<lambda>x. if x \<in> range g then ws (inv g x) else vs' x) = (\<lambda>x. if x = g v then n else vs' x)
[PROOF STEP]
by (auto intro!: ext simp: injD image_def)
[PROOF STATE]
proof (state)
this:
(\<lambda>x. if x \<in> range g then ws (inv g x) else vs' x) = (\<lambda>x. if x = g v then n else vs' x)

goal (2 subgoals):
 1. \<And>v sz n. \<lbrakk>ws = (\<lambda>x. if x = v then n else vs x); (s, Dec v t sz) \<in> M; vs v = Suc n\<rbrakk> \<Longrightarrow> ((f s, vs'), f t, \<lambda>x. if x \<in> range g then ws (inv g x) else vs' x) \<in> step (map_minsky f g M)
 2. \<And>v sn. \<lbrakk>ws = vs; (s, Dec v sn t) \<in> M; vs v = 0\<rbrakk> \<Longrightarrow> ((f s, vs'), f t, \<lambda>x. if x \<in> range g then ws (inv g x) else vs' x) \<in> step (map_minsky f g M)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
((f s, vs'), f t, \<lambda>x. if x = g v then n else vs' x) \<in> step (map_minsky f g M)
(\<lambda>x. if x \<in> range g then ws (inv g x) else vs' x) = (\<lambda>x. if x = g v then n else vs' x)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
((f s, vs'), f t, \<lambda>x. if x = g v then n else vs' x) \<in> step (map_minsky f g M)
(\<lambda>x. if x \<in> range g then ws (inv g x) else vs' x) = (\<lambda>x. if x = g v then n else vs' x)

goal (1 subgoal):
 1. ((f s, vs'), f t, \<lambda>x. if x \<in> range g then ws (inv g x) else vs' x) \<in> step (map_minsky f g M)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
((f s, vs'), f t, \<lambda>x. if x \<in> range g then ws (inv g x) else vs' x) \<in> step (map_minsky f g M)

goal (1 subgoal):
 1. \<And>v sn. \<lbrakk>ws = vs; (s, Dec v sn t) \<in> M; vs v = 0\<rbrakk> \<Longrightarrow> ((f s, vs'), f t, \<lambda>x. if x \<in> range g then ws (inv g x) else vs' x) \<in> step (map_minsky f g M)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>v sn. \<lbrakk>ws = vs; (s, Dec v sn t) \<in> M; vs v = 0\<rbrakk> \<Longrightarrow> ((f s, vs'), f t, \<lambda>x. if x \<in> range g then ws (inv g x) else vs' x) \<in> step (map_minsky f g M)
[PROOF STEP]
case (decz v sn)
[PROOF STATE]
proof (state)
this:
ws = vs
(s, Dec v sn t) \<in> M
vs v = 0

goal (1 subgoal):
 1. \<And>v sn. \<lbrakk>ws = vs; (s, Dec v sn t) \<in> M; vs v = 0\<rbrakk> \<Longrightarrow> ((f s, vs'), f t, \<lambda>x. if x \<in> range g then ws (inv g x) else vs' x) \<in> step (map_minsky f g M)
[PROOF STEP]
note [simp] = decz(1)
[PROOF STATE]
proof (state)
this:
ws = vs

goal (1 subgoal):
 1. \<And>v sn. \<lbrakk>ws = vs; (s, Dec v sn t) \<in> M; vs v = 0\<rbrakk> \<Longrightarrow> ((f s, vs'), f t, \<lambda>x. if x \<in> range g then ws (inv g x) else vs' x) \<in> step (map_minsky f g M)
[PROOF STEP]
have "((f s, vs'), (f t, vs')) \<in> step (map_minsky f g M)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((f s, vs'), f t, vs') \<in> step (map_minsky f g M)
[PROOF STEP]
using assms(2) decz(2-) step.decz[of "f s" "g v" "f sn" "f t" "map_minsky f g M" vs']
[PROOF STATE]
proof (prove)
using this:
vs = vs' \<circ> g
(s, Dec v sn t) \<in> M
vs v = 0
\<lbrakk>(f s, Dec (g v) (f sn) (f t)) \<in> map_minsky f g M; vs' (g v) = 0\<rbrakk> \<Longrightarrow> ((f s, vs'), f t, vs') \<in> step (map_minsky f g M)

goal (1 subgoal):
 1. ((f s, vs'), f t, vs') \<in> step (map_minsky f g M)
[PROOF STEP]
by (force simp: map_minsky_def)
[PROOF STATE]
proof (state)
this:
((f s, vs'), f t, vs') \<in> step (map_minsky f g M)

goal (1 subgoal):
 1. \<And>v sn. \<lbrakk>ws = vs; (s, Dec v sn t) \<in> M; vs v = 0\<rbrakk> \<Longrightarrow> ((f s, vs'), f t, \<lambda>x. if x \<in> range g then ws (inv g x) else vs' x) \<in> step (map_minsky f g M)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
((f s, vs'), f t, vs') \<in> step (map_minsky f g M)

goal (1 subgoal):
 1. \<And>v sn. \<lbrakk>ws = vs; (s, Dec v sn t) \<in> M; vs v = 0\<rbrakk> \<Longrightarrow> ((f s, vs'), f t, \<lambda>x. if x \<in> range g then ws (inv g x) else vs' x) \<in> step (map_minsky f g M)
[PROOF STEP]
have "(\<lambda>x. if x \<in> range g then ws (inv g x) else vs' x) = vs'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. if x \<in> range g then ws (inv g x) else vs' x) = vs'
[PROOF STEP]
using assms(1,2)
[PROOF STATE]
proof (prove)
using this:
inj g
vs = vs' \<circ> g

goal (1 subgoal):
 1. (\<lambda>x. if x \<in> range g then ws (inv g x) else vs' x) = vs'
[PROOF STEP]
by (auto intro!: ext simp: injD image_def)
[PROOF STATE]
proof (state)
this:
(\<lambda>x. if x \<in> range g then ws (inv g x) else vs' x) = vs'

goal (1 subgoal):
 1. \<And>v sn. \<lbrakk>ws = vs; (s, Dec v sn t) \<in> M; vs v = 0\<rbrakk> \<Longrightarrow> ((f s, vs'), f t, \<lambda>x. if x \<in> range g then ws (inv g x) else vs' x) \<in> step (map_minsky f g M)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
((f s, vs'), f t, vs') \<in> step (map_minsky f g M)
(\<lambda>x. if x \<in> range g then ws (inv g x) else vs' x) = vs'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
((f s, vs'), f t, vs') \<in> step (map_minsky f g M)
(\<lambda>x. if x \<in> range g then ws (inv g x) else vs' x) = vs'

goal (1 subgoal):
 1. ((f s, vs'), f t, \<lambda>x. if x \<in> range g then ws (inv g x) else vs' x) \<in> step (map_minsky f g M)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
((f s, vs'), f t, \<lambda>x. if x \<in> range g then ws (inv g x) else vs' x) \<in> step (map_minsky f g M)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma mk_minsky_copy2:
  assumes "u \<noteq> v" "u \<noteq> w" "v \<noteq> w"
  shows "mk_minsky (\<lambda>vs vs'. vs' =
    (\<lambda>x. if x = u then 0 else if x = v then vs u else if x = w then vs u else vs x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mk_minsky (\<lambda>vs vs'. vs' = (\<lambda>x. if x = u then 0 else if x = v then vs u else if x = w then vs u else vs x))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
u \<noteq> v
u \<noteq> w
v \<noteq> w

goal (1 subgoal):
 1. mk_minsky (\<lambda>vs vs'. vs' = (\<lambda>x. if x = u then 0 else if x = v then vs u else if x = w then vs u else vs x))
[PROOF STEP]
by (intro mk_minsky_seq[OF mk_minsky_seq', OF
    mk_minsky_zero[of v]            \<comment> \<open> v[v] := 0                                           \<close>
    mk_minsky_zero[of w]            \<comment> \<open> v[w] := 0                                           \<close>
    mk_minsky_add2[of u v w]]) auto \<comment> \<open> v[v] := v[v] + v[u], v[w] := v[w] + v[u], v[u] := 0 \<close>