[STATEMENT]
theorem algo_impl_correct': "
  <array_assn int_assn xs xsi> 
    all_left_impl xsi 
  <\<lambda>lfi. \<exists>\<^sub>Alf. array_assn int_assn xs xsi 
        * array_assn (option_assn id_assn) lf lfi 
        * \<up>(all_left_spec xs lf)>\<^sub>t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. <array_assn int_assn xs xsi> all_left_impl xsi <\<lambda>r. \<exists>\<^sub>Alf. array_assn int_assn xs xsi * array_assn (option_assn nat_assn) lf r * \<up> (all_left_spec xs lf)>\<^sub>t
[PROOF STEP]
apply (rule cons_rule[OF _ _ algo_impl_correct[to_hnr, THEN hn_refineD, unfolded autoref_tag_defs]])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. array_assn int_assn xs xsi \<Longrightarrow>\<^sub>A hn_ctxt (fst (array_assn int_assn, array_assn int_assn)) ?x2 xsi
 2. \<And>x. hn_ctxt (snd (array_assn int_assn, array_assn int_assn)) ?x2 xsi * (\<exists>\<^sub>Axa. array_assn (option_assn nat_assn) xa x * \<up> (RETURN xa \<le> (SPEC \<circ> all_left_spec) ?x2)) * true \<Longrightarrow>\<^sub>A (\<exists>\<^sub>Alf. array_assn int_assn xs xsi * array_assn (option_assn nat_assn) lf x * \<up> (all_left_spec xs lf)) * true
 3. nofail ((SPEC \<circ> all_left_spec) ?x2)
[PROOF STEP]
apply (simp add: hn_ctxt_def, rule ent_refl)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. hn_ctxt (snd (array_assn int_assn, array_assn int_assn)) xs xsi * (\<exists>\<^sub>Axa. array_assn (option_assn nat_assn) xa x * \<up> (RETURN xa \<le> (SPEC \<circ> all_left_spec) xs)) * true \<Longrightarrow>\<^sub>A (\<exists>\<^sub>Alf. array_assn int_assn xs xsi * array_assn (option_assn nat_assn) lf x * \<up> (all_left_spec xs lf)) * true
 2. nofail ((SPEC \<circ> all_left_spec) xs)
[PROOF STEP]
by (auto simp: hn_ctxt_def)