[STATEMENT]
lemma "create_name_igba \<phi> \<le> SPEC (\<lambda>G. igba G \<and> (\<forall>\<xi>. igba.accept G \<xi> \<longleftrightarrow> \<xi> \<Turnstile>\<^sub>r \<phi>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. create_name_igba \<phi> \<le> SPEC (\<lambda>G. igba G \<and> (\<forall>\<xi>. igba.accept G \<xi> = \<xi> \<Turnstile>\<^sub>r \<phi>))
[PROOF STEP]
unfolding create_name_igba_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. create_name_gba \<phi> \<bind> (\<lambda>A. gba_to_idx A \<bind> (\<lambda>A'. stat_set_data_nres (card (g_V A)) (card (g_V0 A')) (igbg_num_acc A') \<bind> (\<lambda>_. RETURN A'))) \<le> SPEC (\<lambda>G. igba G \<and> (\<forall>\<xi>. igba.accept G \<xi> = \<xi> \<Turnstile>\<^sub>r \<phi>))
[PROOF STEP]
proof (refine_rcg refine_vcg, clarsimp_all)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>gba x; finite (g_V x); \<forall>\<xi>. gba.accept x \<xi> = \<xi> \<Turnstile>\<^sub>r \<phi>\<rbrakk> \<Longrightarrow> gba_to_idx x \<le> SPEC (\<lambda>A'. igba A' \<and> (\<forall>\<xi>. igba.accept A' \<xi> = \<xi> \<Turnstile>\<^sub>r \<phi>))
[PROOF STEP]
fix G :: "(nat, 'a set) gba_rec"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>gba x; finite (g_V x); \<forall>\<xi>. gba.accept x \<xi> = \<xi> \<Turnstile>\<^sub>r \<phi>\<rbrakk> \<Longrightarrow> gba_to_idx x \<le> SPEC (\<lambda>A'. igba A' \<and> (\<forall>\<xi>. igba.accept A' \<xi> = \<xi> \<Turnstile>\<^sub>r \<phi>))
[PROOF STEP]
assume "gba G"
[PROOF STATE]
proof (state)
this:
gba G

goal (1 subgoal):
 1. \<And>x. \<lbrakk>gba x; finite (g_V x); \<forall>\<xi>. gba.accept x \<xi> = \<xi> \<Turnstile>\<^sub>r \<phi>\<rbrakk> \<Longrightarrow> gba_to_idx x \<le> SPEC (\<lambda>A'. igba A' \<and> (\<forall>\<xi>. igba.accept A' \<xi> = \<xi> \<Turnstile>\<^sub>r \<phi>))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
gba G
[PROOF STEP]
interpret gba G
[PROOF STATE]
proof (prove)
using this:
gba G

goal (1 subgoal):
 1. gba G
[PROOF STEP]
.
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>gba x; finite (g_V x); \<forall>\<xi>. gba.accept x \<xi> = \<xi> \<Turnstile>\<^sub>r \<phi>\<rbrakk> \<Longrightarrow> gba_to_idx x \<le> SPEC (\<lambda>A'. igba A' \<and> (\<forall>\<xi>. igba.accept A' \<xi> = \<xi> \<Turnstile>\<^sub>r \<phi>))
[PROOF STEP]
note [refine_vcg] = order_trans[OF gba_to_idx_ext_correct]
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<And>A. A \<in> F \<Longrightarrow> finite A; SPEC (\<lambda>G'. igba.accept G' = accept \<and> g_V G' = V \<and> g_E G' = E \<and> g_V0 G' = V0 \<and> igba_rec.more G' = ?ecnv1 G \<and> igba G') \<le> ?z\<rbrakk> \<Longrightarrow> gba_to_idx_ext ?ecnv1 G \<le> ?z

goal (1 subgoal):
 1. \<And>x. \<lbrakk>gba x; finite (g_V x); \<forall>\<xi>. gba.accept x \<xi> = \<xi> \<Turnstile>\<^sub>r \<phi>\<rbrakk> \<Longrightarrow> gba_to_idx x \<le> SPEC (\<lambda>A'. igba A' \<and> (\<forall>\<xi>. igba.accept A' \<xi> = \<xi> \<Turnstile>\<^sub>r \<phi>))
[PROOF STEP]
assume "\<forall>\<xi>. gba.accept G \<xi> = \<xi> \<Turnstile>\<^sub>r \<phi>" "finite (g_V G)"
[PROOF STATE]
proof (state)
this:
\<forall>\<xi>. accept \<xi> = \<xi> \<Turnstile>\<^sub>r \<phi>
finite V

goal (1 subgoal):
 1. \<And>x. \<lbrakk>gba x; finite (g_V x); \<forall>\<xi>. gba.accept x \<xi> = \<xi> \<Turnstile>\<^sub>r \<phi>\<rbrakk> \<Longrightarrow> gba_to_idx x \<le> SPEC (\<lambda>A'. igba A' \<and> (\<forall>\<xi>. igba.accept A' \<xi> = \<xi> \<Turnstile>\<^sub>r \<phi>))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>\<xi>. accept \<xi> = \<xi> \<Turnstile>\<^sub>r \<phi>
finite V
[PROOF STEP]
show "gba_to_idx G \<le> SPEC (\<lambda>G'. igba G' \<and> (\<forall>\<xi>. igba.accept G' \<xi> = \<xi> \<Turnstile>\<^sub>r \<phi>))"
[PROOF STATE]
proof (prove)
using this:
\<forall>\<xi>. accept \<xi> = \<xi> \<Turnstile>\<^sub>r \<phi>
finite V

goal (1 subgoal):
 1. gba_to_idx G \<le> SPEC (\<lambda>G'. igba G' \<and> (\<forall>\<xi>. igba.accept G' \<xi> = \<xi> \<Turnstile>\<^sub>r \<phi>))
[PROOF STEP]
by (refine_rcg refine_vcg) (auto intro: finite_V_Fe)
[PROOF STATE]
proof (state)
this:
gba_to_idx G \<le> SPEC (\<lambda>G'. igba G' \<and> (\<forall>\<xi>. igba.accept G' \<xi> = \<xi> \<Turnstile>\<^sub>r \<phi>))

goal:
No subgoals!
[PROOF STEP]
qed