[STATEMENT]
lemma monadic_nfoldli_refine_aux':
  assumes SS: "set l' \<subseteq> S"
  assumes c_ref: "\<And>s s'. hn_refine
    (\<Gamma> * hn_ctxt Rs s' s)
    (c s)
    (\<Gamma> * hn_ctxt Rs s' s)
    bool_assn
    (c' s')"
  assumes f_ref: "\<And>x x' s s'. \<lbrakk>x' \<in> S\<rbrakk> \<Longrightarrow> hn_refine
    (\<Gamma> * hn_ctxt Rl x' x * hn_ctxt Rs s' s)
    (f x s)
    (\<Gamma> * hn_ctxt Rl' x' x * hn_invalid Rs s' s) Rs
    (f' x' s')"

  assumes merge[sepref_frame_merge_rules]: "\<And>x x'. hn_ctxt Rl' x' x \<or>\<^sub>A hn_ctxt Rl x' x \<Longrightarrow>\<^sub>t hn_ctxt Rl'' x' x"
  notes [sepref_frame_merge_rules] = merge_sat2[OF merge]

  shows "hn_refine
    (\<Gamma> * hn_ctxt (list_assn Rl) l' l * hn_ctxt Rs s' s)
    (imp_nfoldli l c f s)
    (\<Gamma> * hn_ctxt (list_assn Rl'') l' l * hn_invalid Rs s' s) Rs
    (monadic_nfoldli l' c' f' s')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) l' l * hn_ctxt Rs s' s) (imp_nfoldli l c f s) (\<Gamma> * hn_ctxt (list_assn Rl'') l' l * hn_invalid Rs s' s) Rs (monadic_nfoldli l' c' f' s')
[PROOF STEP]
apply1 (subst monadic_nfoldli_assert_aux[OF SS,symmetric])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) l' l * hn_ctxt Rs s' s) (imp_nfoldli l c f s) (\<Gamma> * hn_ctxt (list_assn Rl'') l' l * hn_invalid Rs s' s) Rs (monadic_nfoldli l' c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) s')
[PROOF STEP]
applyF (induct p\<equiv>Rl l' l
    arbitrary: s s'
    rule: list_assn.induct)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) [] [] * hn_ctxt Rs s' s) (imp_nfoldli [] c f s) (\<Gamma> * hn_ctxt (list_assn Rl'') [] [] * hn_invalid Rs s' s) Rs (monadic_nfoldli [] c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) s')
 2. \<And>a as ca cs s s'. (\<And>s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) as cs * hn_ctxt Rs s' s) (imp_nfoldli cs c f s) (\<Gamma> * hn_ctxt (list_assn Rl'') as cs * hn_invalid Rs s' s) Rs (monadic_nfoldli as c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) s')) \<Longrightarrow> hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) (a # as) (ca # cs) * hn_ctxt Rs s' s) (imp_nfoldli (ca # cs) c f s) (\<Gamma> * hn_ctxt (list_assn Rl'') (a # as) (ca # cs) * hn_invalid Rs s' s) Rs (monadic_nfoldli (a # as) c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) s')
 3. \<And>v va s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) (v # va) [] * hn_ctxt Rs s' s) (imp_nfoldli [] c f s) (\<Gamma> * hn_ctxt (list_assn Rl'') (v # va) [] * hn_invalid Rs s' s) Rs (monadic_nfoldli (v # va) c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) s')
 4. \<And>v va s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) [] (v # va) * hn_ctxt Rs s' s) (imp_nfoldli (v # va) c f s) (\<Gamma> * hn_ctxt (list_assn Rl'') [] (v # va) * hn_invalid Rs s' s) Rs (monadic_nfoldli [] c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) s')
[PROOF STEP]
applyF simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s s'. hn_refine (\<Gamma> * hn_ctxt Rs s' s) (return s) (\<Gamma> * hn_invalid Rs s' s) Rs (RETURN s')
[PROOF STEP]
apply (rule hn_refine_cons_post)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>s s'. hn_refine (\<Gamma> * hn_ctxt Rs s' s) (return s) (?Q5 s s') Rs (RETURN s')
 2. \<And>s s'. ?Q5 s s' \<Longrightarrow>\<^sub>t \<Gamma> * hn_invalid Rs s' s
[PROOF STEP]
apply (rule hn_refine_frame[OF hnr_RETURN_pass])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>s s'. \<Gamma> * hn_ctxt Rs s' s \<Longrightarrow>\<^sub>t ?F8 s s' * hn_ctxt Rs s' s
 2. \<And>s s'. ?F8 s s' * hn_invalid Rs s' s \<Longrightarrow>\<^sub>t \<Gamma> * hn_invalid Rs s' s
[PROOF STEP]
apply (tactic \<open>Sepref_Frame.frame_tac (K (K no_tac)) @{context} 1\<close>)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<Gamma> * hn_invalid Rs s' s \<Longrightarrow>\<^sub>t \<Gamma> * hn_invalid Rs s' s
[PROOF STEP]
apply (simp add: hn_ctxt_def ent_true_drop)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
solved
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>a as ca cs s s'. (\<And>s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) as cs * hn_ctxt Rs s' s) (imp_nfoldli cs c f s) (\<Gamma> * hn_ctxt (list_assn Rl'') as cs * hn_invalid Rs s' s) Rs (monadic_nfoldli as c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) s')) \<Longrightarrow> hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) (a # as) (ca # cs) * hn_ctxt Rs s' s) (imp_nfoldli (ca # cs) c f s) (\<Gamma> * hn_ctxt (list_assn Rl'') (a # as) (ca # cs) * hn_invalid Rs s' s) Rs (monadic_nfoldli (a # as) c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) s')
 2. \<And>v va s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) (v # va) [] * hn_ctxt Rs s' s) (imp_nfoldli [] c f s) (\<Gamma> * hn_ctxt (list_assn Rl'') (v # va) [] * hn_invalid Rs s' s) Rs (monadic_nfoldli (v # va) c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) s')
 3. \<And>v va s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) [] (v # va) * hn_ctxt Rs s' s) (imp_nfoldli (v # va) c f s) (\<Gamma> * hn_ctxt (list_assn Rl'') [] (v # va) * hn_invalid Rs s' s) Rs (monadic_nfoldli [] c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) s')
[PROOF STEP]
apply (simp only: imp_nfoldli_simps monadic_nfoldli_simp)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>a as ca cs s s'. (\<And>s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) as cs * hn_ctxt Rs s' s) (imp_nfoldli cs c f s) (\<Gamma> * hn_ctxt (list_assn Rl'') as cs * hn_invalid Rs s' s) Rs (monadic_nfoldli as c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) s')) \<Longrightarrow> hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) (a # as) (ca # cs) * hn_ctxt Rs s' s) (c s \<bind> (\<lambda>b. if b then f ca s \<bind> imp_nfoldli cs c f else return s)) (\<Gamma> * hn_ctxt (list_assn Rl'') (a # as) (ca # cs) * hn_invalid Rs s' s) Rs (c' s' \<bind> (\<lambda>b. if b then ASSERT (a \<in> S) \<bind> (\<lambda>_. f' a s') \<bind> monadic_nfoldli as c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) else RETURN s'))
 2. \<And>v va s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) (v # va) [] * hn_ctxt Rs s' s) (imp_nfoldli [] c f s) (\<Gamma> * hn_ctxt (list_assn Rl'') (v # va) [] * hn_invalid Rs s' s) Rs (monadic_nfoldli (v # va) c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) s')
 3. \<And>v va s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) [] (v # va) * hn_ctxt Rs s' s) (imp_nfoldli (v # va) c f s) (\<Gamma> * hn_ctxt (list_assn Rl'') [] (v # va) * hn_invalid Rs s' s) Rs (monadic_nfoldli [] c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) s')
[PROOF STEP]
apply (rule hnr_bind)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>a as ca cs s s'. (\<And>s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) as cs * hn_ctxt Rs s' s) (imp_nfoldli cs c f s) (\<Gamma> * hn_ctxt (list_assn Rl'') as cs * hn_invalid Rs s' s) Rs (monadic_nfoldli as c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) s')) \<Longrightarrow> hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) (a # as) (ca # cs) * hn_ctxt Rs s' s) (c s) (?\<Gamma>1.17 a as ca cs s s') (?Rh17 a as ca cs s s') (c' s')
 2. \<And>a as ca cs s s' x x'. \<lbrakk>\<And>s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) as cs * hn_ctxt Rs s' s) (imp_nfoldli cs c f s) (\<Gamma> * hn_ctxt (list_assn Rl'') as cs * hn_invalid Rs s' s) Rs (monadic_nfoldli as c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) s'); RETURN x \<le> c' s'\<rbrakk> \<Longrightarrow> hn_refine (?\<Gamma>1.17 a as ca cs s s' * hn_ctxt (?Rh17 a as ca cs s s') x x') (if x' then f ca s \<bind> imp_nfoldli cs c f else return s) (?\<Gamma>2.17 a as ca cs s s' x x') Rs (if x then ASSERT (a \<in> S) \<bind> (\<lambda>_. f' a s') \<bind> monadic_nfoldli as c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) else RETURN s')
 3. \<And>a as ca cs s s' x x'. (\<And>s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) as cs * hn_ctxt Rs s' s) (imp_nfoldli cs c f s) (\<Gamma> * hn_ctxt (list_assn Rl'') as cs * hn_invalid Rs s' s) Rs (monadic_nfoldli as c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) s')) \<Longrightarrow> ?\<Gamma>2.17 a as ca cs s s' x x' \<Longrightarrow>\<^sub>t \<Gamma> * hn_ctxt (list_assn Rl'') (a # as) (ca # cs) * hn_invalid Rs s' s * hn_ctxt (?Rx17 a as ca cs s s') x x'
 4. \<And>v va s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) (v # va) [] * hn_ctxt Rs s' s) (imp_nfoldli [] c f s) (\<Gamma> * hn_ctxt (list_assn Rl'') (v # va) [] * hn_invalid Rs s' s) Rs (monadic_nfoldli (v # va) c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) s')
 5. \<And>v va s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) [] (v # va) * hn_ctxt Rs s' s) (imp_nfoldli (v # va) c f s) (\<Gamma> * hn_ctxt (list_assn Rl'') [] (v # va) * hn_invalid Rs s' s) Rs (monadic_nfoldli [] c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) s')
[PROOF STEP]
apply (rule hn_refine_frame[OF c_ref])
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>a as ca cs s s'. (\<And>s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) as cs * hn_ctxt Rs s' s) (imp_nfoldli cs c f s) (\<Gamma> * hn_ctxt (list_assn Rl'') as cs * hn_invalid Rs s' s) Rs (monadic_nfoldli as c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) s')) \<Longrightarrow> \<Gamma> * hn_ctxt (list_assn Rl) (a # as) (ca # cs) * hn_ctxt Rs s' s \<Longrightarrow>\<^sub>t ?F21 a as ca cs s s' * (\<Gamma> * hn_ctxt Rs s' s)
 2. \<And>a as ca cs s s' x x'. \<lbrakk>\<And>s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) as cs * hn_ctxt Rs s' s) (imp_nfoldli cs c f s) (\<Gamma> * hn_ctxt (list_assn Rl'') as cs * hn_invalid Rs s' s) Rs (monadic_nfoldli as c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) s'); RETURN x \<le> c' s'\<rbrakk> \<Longrightarrow> hn_refine (?F21 a as ca cs s s' * (\<Gamma> * hn_ctxt Rs s' s) * hn_val bool_rel x x') (if x' then f ca s \<bind> imp_nfoldli cs c f else return s) (?\<Gamma>2.17 a as ca cs s s' x x') Rs (if x then ASSERT (a \<in> S) \<bind> (\<lambda>_. f' a s') \<bind> monadic_nfoldli as c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) else RETURN s')
 3. \<And>a as ca cs s s' x x'. (\<And>s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) as cs * hn_ctxt Rs s' s) (imp_nfoldli cs c f s) (\<Gamma> * hn_ctxt (list_assn Rl'') as cs * hn_invalid Rs s' s) Rs (monadic_nfoldli as c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) s')) \<Longrightarrow> ?\<Gamma>2.17 a as ca cs s s' x x' \<Longrightarrow>\<^sub>t \<Gamma> * hn_ctxt (list_assn Rl'') (a # as) (ca # cs) * hn_invalid Rs s' s * hn_ctxt (?Rx17 a as ca cs s s') x x'
 4. \<And>v va s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) (v # va) [] * hn_ctxt Rs s' s) (imp_nfoldli [] c f s) (\<Gamma> * hn_ctxt (list_assn Rl'') (v # va) [] * hn_invalid Rs s' s) Rs (monadic_nfoldli (v # va) c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) s')
 5. \<And>v va s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) [] (v # va) * hn_ctxt Rs s' s) (imp_nfoldli (v # va) c f s) (\<Gamma> * hn_ctxt (list_assn Rl'') [] (v # va) * hn_invalid Rs s' s) Rs (monadic_nfoldli [] c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) s')
[PROOF STEP]
apply (tactic \<open>Sepref_Frame.frame_tac (K (K no_tac)) @{context} 1\<close>)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>a as ca cs s s' x x'. \<lbrakk>\<And>s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) as cs * hn_ctxt Rs s' s) (imp_nfoldli cs c f s) (\<Gamma> * hn_ctxt (list_assn Rl'') as cs * hn_invalid Rs s' s) Rs (monadic_nfoldli as c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) s'); RETURN x \<le> c' s'\<rbrakk> \<Longrightarrow> hn_refine (hn_ctxt (list_assn Rl) (a # as) (ca # cs) * (\<Gamma> * hn_ctxt Rs s' s) * hn_val bool_rel x x') (if x' then f ca s \<bind> imp_nfoldli cs c f else return s) (?\<Gamma>2.17 a as ca cs s s' x x') Rs (if x then ASSERT (a \<in> S) \<bind> (\<lambda>_. f' a s') \<bind> monadic_nfoldli as c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) else RETURN s')
 2. \<And>a as ca cs s s' x x'. (\<And>s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) as cs * hn_ctxt Rs s' s) (imp_nfoldli cs c f s) (\<Gamma> * hn_ctxt (list_assn Rl'') as cs * hn_invalid Rs s' s) Rs (monadic_nfoldli as c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) s')) \<Longrightarrow> ?\<Gamma>2.17 a as ca cs s s' x x' \<Longrightarrow>\<^sub>t \<Gamma> * hn_ctxt (list_assn Rl'') (a # as) (ca # cs) * hn_invalid Rs s' s * hn_ctxt (?Rx17 a as ca cs s s') x x'
 3. \<And>v va s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) (v # va) [] * hn_ctxt Rs s' s) (imp_nfoldli [] c f s) (\<Gamma> * hn_ctxt (list_assn Rl'') (v # va) [] * hn_invalid Rs s' s) Rs (monadic_nfoldli (v # va) c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) s')
 4. \<And>v va s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) [] (v # va) * hn_ctxt Rs s' s) (imp_nfoldli (v # va) c f s) (\<Gamma> * hn_ctxt (list_assn Rl'') [] (v # va) * hn_invalid Rs s' s) Rs (monadic_nfoldli [] c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) s')
[PROOF STEP]
apply (rule hnr_If)
[PROOF STATE]
proof (prove)
goal (7 subgoals):
 1. \<And>a as ca cs s s' x x'. \<lbrakk>\<And>s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) as cs * hn_ctxt Rs s' s) (imp_nfoldli cs c f s) (\<Gamma> * hn_ctxt (list_assn Rl'') as cs * hn_invalid Rs s' s) Rs (monadic_nfoldli as c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) s'); RETURN x \<le> c' s'\<rbrakk> \<Longrightarrow> hn_ctxt (list_assn Rl) (a # as) (ca # cs) * (\<Gamma> * hn_ctxt Rs s' s) * hn_val bool_rel x x' \<Longrightarrow>\<^sub>t ?\<Gamma>1.29 a as ca cs s s' x x' * hn_val bool_rel x x'
 2. \<And>a as ca cs s s' x x'. \<lbrakk>\<And>s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) as cs * hn_ctxt Rs s' s) (imp_nfoldli cs c f s) (\<Gamma> * hn_ctxt (list_assn Rl'') as cs * hn_invalid Rs s' s) Rs (monadic_nfoldli as c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) s'); RETURN x \<le> c' s'; x\<rbrakk> \<Longrightarrow> hn_refine (?\<Gamma>1.29 a as ca cs s s' x x' * hn_val bool_rel x x') (f ca s \<bind> imp_nfoldli cs c f) (?\<Gamma>2b29 a as ca cs s s' x x') Rs (ASSERT (a \<in> S) \<bind> (\<lambda>_. f' a s') \<bind> monadic_nfoldli as c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)))
 3. \<And>a as ca cs s s' x x'. \<lbrakk>\<And>s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) as cs * hn_ctxt Rs s' s) (imp_nfoldli cs c f s) (\<Gamma> * hn_ctxt (list_assn Rl'') as cs * hn_invalid Rs s' s) Rs (monadic_nfoldli as c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) s'); RETURN x \<le> c' s'; \<not> x\<rbrakk> \<Longrightarrow> hn_refine (?\<Gamma>1.29 a as ca cs s s' x x' * hn_val bool_rel x x') (return s) (?\<Gamma>2c29 a as ca cs s s' x x') Rs (RETURN s')
 4. \<And>a as ca cs s s' x x'. \<lbrakk>\<And>s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) as cs * hn_ctxt Rs s' s) (imp_nfoldli cs c f s) (\<Gamma> * hn_ctxt (list_assn Rl'') as cs * hn_invalid Rs s' s) Rs (monadic_nfoldli as c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) s'); RETURN x \<le> c' s'\<rbrakk> \<Longrightarrow> ?\<Gamma>2b29 a as ca cs s s' x x' \<or>\<^sub>A ?\<Gamma>2c29 a as ca cs s s' x x' \<Longrightarrow>\<^sub>t ?\<Gamma>2.17 a as ca cs s s' x x'
 5. \<And>a as ca cs s s' x x'. (\<And>s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) as cs * hn_ctxt Rs s' s) (imp_nfoldli cs c f s) (\<Gamma> * hn_ctxt (list_assn Rl'') as cs * hn_invalid Rs s' s) Rs (monadic_nfoldli as c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) s')) \<Longrightarrow> ?\<Gamma>2.17 a as ca cs s s' x x' \<Longrightarrow>\<^sub>t \<Gamma> * hn_ctxt (list_assn Rl'') (a # as) (ca # cs) * hn_invalid Rs s' s * hn_ctxt (?Rx17 a as ca cs s s') x x'
 6. \<And>v va s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) (v # va) [] * hn_ctxt Rs s' s) (imp_nfoldli [] c f s) (\<Gamma> * hn_ctxt (list_assn Rl'') (v # va) [] * hn_invalid Rs s' s) Rs (monadic_nfoldli (v # va) c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) s')
 7. \<And>v va s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) [] (v # va) * hn_ctxt Rs s' s) (imp_nfoldli (v # va) c f s) (\<Gamma> * hn_ctxt (list_assn Rl'') [] (v # va) * hn_invalid Rs s' s) Rs (monadic_nfoldli [] c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) s')
[PROOF STEP]
apply (tactic \<open>Sepref_Frame.frame_tac (K (K no_tac)) @{context} 1\<close>)
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<And>a as ca cs s s' x x'. \<lbrakk>\<And>s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) as cs * hn_ctxt Rs s' s) (imp_nfoldli cs c f s) (\<Gamma> * hn_ctxt (list_assn Rl'') as cs * hn_invalid Rs s' s) Rs (monadic_nfoldli as c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) s'); RETURN x \<le> c' s'; x\<rbrakk> \<Longrightarrow> hn_refine (hn_ctxt (list_assn Rl) (a # as) (ca # cs) * \<Gamma> * hn_ctxt Rs s' s * hn_val bool_rel x x') (f ca s \<bind> imp_nfoldli cs c f) (?\<Gamma>2b29 a as ca cs s s' x x') Rs (ASSERT (a \<in> S) \<bind> (\<lambda>_. f' a s') \<bind> monadic_nfoldli as c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)))
 2. \<And>a as ca cs s s' x x'. \<lbrakk>\<And>s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) as cs * hn_ctxt Rs s' s) (imp_nfoldli cs c f s) (\<Gamma> * hn_ctxt (list_assn Rl'') as cs * hn_invalid Rs s' s) Rs (monadic_nfoldli as c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) s'); RETURN x \<le> c' s'; \<not> x\<rbrakk> \<Longrightarrow> hn_refine (hn_ctxt (list_assn Rl) (a # as) (ca # cs) * \<Gamma> * hn_ctxt Rs s' s * hn_val bool_rel x x') (return s) (?\<Gamma>2c29 a as ca cs s s' x x') Rs (RETURN s')
 3. \<And>a as ca cs s s' x x'. \<lbrakk>\<And>s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) as cs * hn_ctxt Rs s' s) (imp_nfoldli cs c f s) (\<Gamma> * hn_ctxt (list_assn Rl'') as cs * hn_invalid Rs s' s) Rs (monadic_nfoldli as c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) s'); RETURN x \<le> c' s'\<rbrakk> \<Longrightarrow> ?\<Gamma>2b29 a as ca cs s s' x x' \<or>\<^sub>A ?\<Gamma>2c29 a as ca cs s s' x x' \<Longrightarrow>\<^sub>t ?\<Gamma>2.17 a as ca cs s s' x x'
 4. \<And>a as ca cs s s' x x'. (\<And>s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) as cs * hn_ctxt Rs s' s) (imp_nfoldli cs c f s) (\<Gamma> * hn_ctxt (list_assn Rl'') as cs * hn_invalid Rs s' s) Rs (monadic_nfoldli as c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) s')) \<Longrightarrow> ?\<Gamma>2.17 a as ca cs s s' x x' \<Longrightarrow>\<^sub>t \<Gamma> * hn_ctxt (list_assn Rl'') (a # as) (ca # cs) * hn_invalid Rs s' s * hn_ctxt (?Rx17 a as ca cs s s') x x'
 5. \<And>v va s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) (v # va) [] * hn_ctxt Rs s' s) (imp_nfoldli [] c f s) (\<Gamma> * hn_ctxt (list_assn Rl'') (v # va) [] * hn_invalid Rs s' s) Rs (monadic_nfoldli (v # va) c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) s')
 6. \<And>v va s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) [] (v # va) * hn_ctxt Rs s' s) (imp_nfoldli (v # va) c f s) (\<Gamma> * hn_ctxt (list_assn Rl'') [] (v # va) * hn_invalid Rs s' s) Rs (monadic_nfoldli [] c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) s')
[PROOF STEP]
apply (simp only: nres_monad_laws)
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<And>a as ca cs s s' x x'. \<lbrakk>\<And>s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) as cs * hn_ctxt Rs s' s) (imp_nfoldli cs c f s) (\<Gamma> * hn_ctxt (list_assn Rl'') as cs * hn_invalid Rs s' s) Rs (monadic_nfoldli as c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) s'); RETURN True \<le> c' s'; x\<rbrakk> \<Longrightarrow> hn_refine (hn_ctxt (list_assn Rl) (a # as) (ca # cs) * \<Gamma> * hn_ctxt Rs s' s * hn_val bool_rel True x') (f ca s \<bind> imp_nfoldli cs c f) (?\<Gamma>2b29 a as ca cs s s' True x') Rs (ASSERT (a \<in> S) \<bind> (\<lambda>x. f' a s' \<bind> monadic_nfoldli as c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s))))
 2. \<And>a as ca cs s s' x x'. \<lbrakk>\<And>s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) as cs * hn_ctxt Rs s' s) (imp_nfoldli cs c f s) (\<Gamma> * hn_ctxt (list_assn Rl'') as cs * hn_invalid Rs s' s) Rs (monadic_nfoldli as c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) s'); RETURN x \<le> c' s'; \<not> x\<rbrakk> \<Longrightarrow> hn_refine (hn_ctxt (list_assn Rl) (a # as) (ca # cs) * \<Gamma> * hn_ctxt Rs s' s * hn_val bool_rel x x') (return s) (?\<Gamma>2c29 a as ca cs s s' x x') Rs (RETURN s')
 3. \<And>a as ca cs s s' x x'. \<lbrakk>\<And>s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) as cs * hn_ctxt Rs s' s) (imp_nfoldli cs c f s) (\<Gamma> * hn_ctxt (list_assn Rl'') as cs * hn_invalid Rs s' s) Rs (monadic_nfoldli as c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) s'); RETURN x \<le> c' s'\<rbrakk> \<Longrightarrow> ?\<Gamma>2b29 a as ca cs s s' x x' \<or>\<^sub>A ?\<Gamma>2c29 a as ca cs s s' x x' \<Longrightarrow>\<^sub>t ?\<Gamma>2.17 a as ca cs s s' x x'
 4. \<And>a as ca cs s s' x x'. (\<And>s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) as cs * hn_ctxt Rs s' s) (imp_nfoldli cs c f s) (\<Gamma> * hn_ctxt (list_assn Rl'') as cs * hn_invalid Rs s' s) Rs (monadic_nfoldli as c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) s')) \<Longrightarrow> ?\<Gamma>2.17 a as ca cs s s' x x' \<Longrightarrow>\<^sub>t \<Gamma> * hn_ctxt (list_assn Rl'') (a # as) (ca # cs) * hn_invalid Rs s' s * hn_ctxt (?Rx17 a as ca cs s s') x x'
 5. \<And>v va s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) (v # va) [] * hn_ctxt Rs s' s) (imp_nfoldli [] c f s) (\<Gamma> * hn_ctxt (list_assn Rl'') (v # va) [] * hn_invalid Rs s' s) Rs (monadic_nfoldli (v # va) c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) s')
 6. \<And>v va s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) [] (v # va) * hn_ctxt Rs s' s) (imp_nfoldli (v # va) c f s) (\<Gamma> * hn_ctxt (list_assn Rl'') [] (v # va) * hn_invalid Rs s' s) Rs (monadic_nfoldli [] c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) s')
[PROOF STEP]
apply (rule hnr_ASSERT)
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<And>a as ca cs s s' x x'. \<lbrakk>\<And>s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) as cs * hn_ctxt Rs s' s) (imp_nfoldli cs c f s) (\<Gamma> * hn_ctxt (list_assn Rl'') as cs * hn_invalid Rs s' s) Rs (monadic_nfoldli as c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) s'); RETURN True \<le> c' s'; x; a \<in> S\<rbrakk> \<Longrightarrow> hn_refine (hn_ctxt (list_assn Rl) (a # as) (ca # cs) * \<Gamma> * hn_ctxt Rs s' s * hn_val bool_rel True x') (f ca s \<bind> imp_nfoldli cs c f) (?\<Gamma>2b29 a as ca cs s s' True x') Rs (f' a s' \<bind> monadic_nfoldli as c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)))
 2. \<And>a as ca cs s s' x x'. \<lbrakk>\<And>s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) as cs * hn_ctxt Rs s' s) (imp_nfoldli cs c f s) (\<Gamma> * hn_ctxt (list_assn Rl'') as cs * hn_invalid Rs s' s) Rs (monadic_nfoldli as c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) s'); RETURN x \<le> c' s'; \<not> x\<rbrakk> \<Longrightarrow> hn_refine (hn_ctxt (list_assn Rl) (a # as) (ca # cs) * \<Gamma> * hn_ctxt Rs s' s * hn_val bool_rel x x') (return s) (?\<Gamma>2c29 a as ca cs s s' x x') Rs (RETURN s')
 3. \<And>a as ca cs s s' x x'. \<lbrakk>\<And>s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) as cs * hn_ctxt Rs s' s) (imp_nfoldli cs c f s) (\<Gamma> * hn_ctxt (list_assn Rl'') as cs * hn_invalid Rs s' s) Rs (monadic_nfoldli as c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) s'); RETURN x \<le> c' s'\<rbrakk> \<Longrightarrow> ?\<Gamma>2b29 a as ca cs s s' x x' \<or>\<^sub>A ?\<Gamma>2c29 a as ca cs s s' x x' \<Longrightarrow>\<^sub>t ?\<Gamma>2.17 a as ca cs s s' x x'
 4. \<And>a as ca cs s s' x x'. (\<And>s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) as cs * hn_ctxt Rs s' s) (imp_nfoldli cs c f s) (\<Gamma> * hn_ctxt (list_assn Rl'') as cs * hn_invalid Rs s' s) Rs (monadic_nfoldli as c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) s')) \<Longrightarrow> ?\<Gamma>2.17 a as ca cs s s' x x' \<Longrightarrow>\<^sub>t \<Gamma> * hn_ctxt (list_assn Rl'') (a # as) (ca # cs) * hn_invalid Rs s' s * hn_ctxt (?Rx17 a as ca cs s s') x x'
 5. \<And>v va s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) (v # va) [] * hn_ctxt Rs s' s) (imp_nfoldli [] c f s) (\<Gamma> * hn_ctxt (list_assn Rl'') (v # va) [] * hn_invalid Rs s' s) Rs (monadic_nfoldli (v # va) c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) s')
 6. \<And>v va s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) [] (v # va) * hn_ctxt Rs s' s) (imp_nfoldli (v # va) c f s) (\<Gamma> * hn_ctxt (list_assn Rl'') [] (v # va) * hn_invalid Rs s' s) Rs (monadic_nfoldli [] c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) s')
[PROOF STEP]
apply (rule hnr_bind)
[PROOF STATE]
proof (prove)
goal (8 subgoals):
 1. \<And>a as ca cs s s' x x'. \<lbrakk>\<And>s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) as cs * hn_ctxt Rs s' s) (imp_nfoldli cs c f s) (\<Gamma> * hn_ctxt (list_assn Rl'') as cs * hn_invalid Rs s' s) Rs (monadic_nfoldli as c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) s'); RETURN True \<le> c' s'; x; a \<in> S\<rbrakk> \<Longrightarrow> hn_refine (hn_ctxt (list_assn Rl) (a # as) (ca # cs) * \<Gamma> * hn_ctxt Rs s' s * hn_val bool_rel True x') (f ca s) (?\<Gamma>1.40 a as ca cs s s' x x') (?Rh40 a as ca cs s s' x x') (f' a s')
 2. \<And>a as ca cs s s' x x' xa x'a. \<lbrakk>\<And>s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) as cs * hn_ctxt Rs s' s) (imp_nfoldli cs c f s) (\<Gamma> * hn_ctxt (list_assn Rl'') as cs * hn_invalid Rs s' s) Rs (monadic_nfoldli as c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) s'); RETURN True \<le> c' s'; x; a \<in> S; RETURN xa \<le> f' a s'\<rbrakk> \<Longrightarrow> hn_refine (?\<Gamma>1.40 a as ca cs s s' x x' * hn_ctxt (?Rh40 a as ca cs s s' x x') xa x'a) (imp_nfoldli cs c f x'a) (?\<Gamma>2.40 a as ca cs s s' x x' xa x'a) Rs (monadic_nfoldli as c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) xa)
 3. \<And>a as ca cs s s' x x' xa x'a. \<lbrakk>\<And>s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) as cs * hn_ctxt Rs s' s) (imp_nfoldli cs c f s) (\<Gamma> * hn_ctxt (list_assn Rl'') as cs * hn_invalid Rs s' s) Rs (monadic_nfoldli as c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) s'); RETURN True \<le> c' s'; x; a \<in> S\<rbrakk> \<Longrightarrow> ?\<Gamma>2.40 a as ca cs s s' x x' xa x'a \<Longrightarrow>\<^sub>t ?\<Gamma>2b29 a as ca cs s s' True x' * hn_ctxt (?Rx40 a as ca cs s s' x x') xa x'a
 4. \<And>a as ca cs s s' x x'. \<lbrakk>\<And>s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) as cs * hn_ctxt Rs s' s) (imp_nfoldli cs c f s) (\<Gamma> * hn_ctxt (list_assn Rl'') as cs * hn_invalid Rs s' s) Rs (monadic_nfoldli as c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) s'); RETURN x \<le> c' s'; \<not> x\<rbrakk> \<Longrightarrow> hn_refine (hn_ctxt (list_assn Rl) (a # as) (ca # cs) * \<Gamma> * hn_ctxt Rs s' s * hn_val bool_rel x x') (return s) (?\<Gamma>2c29 a as ca cs s s' x x') Rs (RETURN s')
 5. \<And>a as ca cs s s' x x'. \<lbrakk>\<And>s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) as cs * hn_ctxt Rs s' s) (imp_nfoldli cs c f s) (\<Gamma> * hn_ctxt (list_assn Rl'') as cs * hn_invalid Rs s' s) Rs (monadic_nfoldli as c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) s'); RETURN x \<le> c' s'\<rbrakk> \<Longrightarrow> ?\<Gamma>2b29 a as ca cs s s' x x' \<or>\<^sub>A ?\<Gamma>2c29 a as ca cs s s' x x' \<Longrightarrow>\<^sub>t ?\<Gamma>2.17 a as ca cs s s' x x'
 6. \<And>a as ca cs s s' x x'. (\<And>s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) as cs * hn_ctxt Rs s' s) (imp_nfoldli cs c f s) (\<Gamma> * hn_ctxt (list_assn Rl'') as cs * hn_invalid Rs s' s) Rs (monadic_nfoldli as c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) s')) \<Longrightarrow> ?\<Gamma>2.17 a as ca cs s s' x x' \<Longrightarrow>\<^sub>t \<Gamma> * hn_ctxt (list_assn Rl'') (a # as) (ca # cs) * hn_invalid Rs s' s * hn_ctxt (?Rx17 a as ca cs s s') x x'
 7. \<And>v va s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) (v # va) [] * hn_ctxt Rs s' s) (imp_nfoldli [] c f s) (\<Gamma> * hn_ctxt (list_assn Rl'') (v # va) [] * hn_invalid Rs s' s) Rs (monadic_nfoldli (v # va) c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) s')
 8. \<And>v va s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) [] (v # va) * hn_ctxt Rs s' s) (imp_nfoldli (v # va) c f s) (\<Gamma> * hn_ctxt (list_assn Rl'') [] (v # va) * hn_invalid Rs s' s) Rs (monadic_nfoldli [] c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) s')
[PROOF STEP]
apply (rule hn_refine_frame[OF f_ref])
[PROOF STATE]
proof (prove)
goal (9 subgoals):
 1. \<And>a as ca cs s s' x x'. \<lbrakk>\<And>s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) as cs * hn_ctxt Rs s' s) (imp_nfoldli cs c f s) (\<Gamma> * hn_ctxt (list_assn Rl'') as cs * hn_invalid Rs s' s) Rs (monadic_nfoldli as c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) s'); RETURN True \<le> c' s'; x; a \<in> S\<rbrakk> \<Longrightarrow> a \<in> S
 2. \<And>a as ca cs s s' x x'. \<lbrakk>\<And>s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) as cs * hn_ctxt Rs s' s) (imp_nfoldli cs c f s) (\<Gamma> * hn_ctxt (list_assn Rl'') as cs * hn_invalid Rs s' s) Rs (monadic_nfoldli as c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) s'); RETURN True \<le> c' s'; x; a \<in> S\<rbrakk> \<Longrightarrow> hn_ctxt (list_assn Rl) (a # as) (ca # cs) * \<Gamma> * hn_ctxt Rs s' s * hn_val bool_rel True x' \<Longrightarrow>\<^sub>t ?F45 a as ca cs s s' x x' * (\<Gamma> * hn_ctxt Rl a ca * hn_ctxt Rs s' s)
 3. \<And>a as ca cs s s' x x' xa x'a. \<lbrakk>\<And>s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) as cs * hn_ctxt Rs s' s) (imp_nfoldli cs c f s) (\<Gamma> * hn_ctxt (list_assn Rl'') as cs * hn_invalid Rs s' s) Rs (monadic_nfoldli as c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) s'); RETURN True \<le> c' s'; x; a \<in> S; RETURN xa \<le> f' a s'\<rbrakk> \<Longrightarrow> hn_refine (?F45 a as ca cs s s' x x' * (\<Gamma> * hn_ctxt Rl' a ca * hn_invalid Rs s' s) * hn_ctxt Rs xa x'a) (imp_nfoldli cs c f x'a) (?\<Gamma>2.40 a as ca cs s s' x x' xa x'a) Rs (monadic_nfoldli as c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) xa)
 4. \<And>a as ca cs s s' x x' xa x'a. \<lbrakk>\<And>s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) as cs * hn_ctxt Rs s' s) (imp_nfoldli cs c f s) (\<Gamma> * hn_ctxt (list_assn Rl'') as cs * hn_invalid Rs s' s) Rs (monadic_nfoldli as c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) s'); RETURN True \<le> c' s'; x; a \<in> S\<rbrakk> \<Longrightarrow> ?\<Gamma>2.40 a as ca cs s s' x x' xa x'a \<Longrightarrow>\<^sub>t ?\<Gamma>2b29 a as ca cs s s' True x' * hn_ctxt (?Rx40 a as ca cs s s' x x') xa x'a
 5. \<And>a as ca cs s s' x x'. \<lbrakk>\<And>s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) as cs * hn_ctxt Rs s' s) (imp_nfoldli cs c f s) (\<Gamma> * hn_ctxt (list_assn Rl'') as cs * hn_invalid Rs s' s) Rs (monadic_nfoldli as c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) s'); RETURN x \<le> c' s'; \<not> x\<rbrakk> \<Longrightarrow> hn_refine (hn_ctxt (list_assn Rl) (a # as) (ca # cs) * \<Gamma> * hn_ctxt Rs s' s * hn_val bool_rel x x') (return s) (?\<Gamma>2c29 a as ca cs s s' x x') Rs (RETURN s')
 6. \<And>a as ca cs s s' x x'. \<lbrakk>\<And>s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) as cs * hn_ctxt Rs s' s) (imp_nfoldli cs c f s) (\<Gamma> * hn_ctxt (list_assn Rl'') as cs * hn_invalid Rs s' s) Rs (monadic_nfoldli as c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) s'); RETURN x \<le> c' s'\<rbrakk> \<Longrightarrow> ?\<Gamma>2b29 a as ca cs s s' x x' \<or>\<^sub>A ?\<Gamma>2c29 a as ca cs s s' x x' \<Longrightarrow>\<^sub>t ?\<Gamma>2.17 a as ca cs s s' x x'
 7. \<And>a as ca cs s s' x x'. (\<And>s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) as cs * hn_ctxt Rs s' s) (imp_nfoldli cs c f s) (\<Gamma> * hn_ctxt (list_assn Rl'') as cs * hn_invalid Rs s' s) Rs (monadic_nfoldli as c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) s')) \<Longrightarrow> ?\<Gamma>2.17 a as ca cs s s' x x' \<Longrightarrow>\<^sub>t \<Gamma> * hn_ctxt (list_assn Rl'') (a # as) (ca # cs) * hn_invalid Rs s' s * hn_ctxt (?Rx17 a as ca cs s s') x x'
 8. \<And>v va s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) (v # va) [] * hn_ctxt Rs s' s) (imp_nfoldli [] c f s) (\<Gamma> * hn_ctxt (list_assn Rl'') (v # va) [] * hn_invalid Rs s' s) Rs (monadic_nfoldli (v # va) c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) s')
 9. \<And>v va s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) [] (v # va) * hn_ctxt Rs s' s) (imp_nfoldli (v # va) c f s) (\<Gamma> * hn_ctxt (list_assn Rl'') [] (v # va) * hn_invalid Rs s' s) Rs (monadic_nfoldli [] c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) s')
[PROOF STEP]
apply assumption
[PROOF STATE]
proof (prove)
goal (8 subgoals):
 1. \<And>a as ca cs s s' x x'. \<lbrakk>\<And>s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) as cs * hn_ctxt Rs s' s) (imp_nfoldli cs c f s) (\<Gamma> * hn_ctxt (list_assn Rl'') as cs * hn_invalid Rs s' s) Rs (monadic_nfoldli as c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) s'); RETURN True \<le> c' s'; x; a \<in> S\<rbrakk> \<Longrightarrow> hn_ctxt (list_assn Rl) (a # as) (ca # cs) * \<Gamma> * hn_ctxt Rs s' s * hn_val bool_rel True x' \<Longrightarrow>\<^sub>t ?F45 a as ca cs s s' x x' * (\<Gamma> * hn_ctxt Rl a ca * hn_ctxt Rs s' s)
 2. \<And>a as ca cs s s' x x' xa x'a. \<lbrakk>\<And>s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) as cs * hn_ctxt Rs s' s) (imp_nfoldli cs c f s) (\<Gamma> * hn_ctxt (list_assn Rl'') as cs * hn_invalid Rs s' s) Rs (monadic_nfoldli as c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) s'); RETURN True \<le> c' s'; x; a \<in> S; RETURN xa \<le> f' a s'\<rbrakk> \<Longrightarrow> hn_refine (?F45 a as ca cs s s' x x' * (\<Gamma> * hn_ctxt Rl' a ca * hn_invalid Rs s' s) * hn_ctxt Rs xa x'a) (imp_nfoldli cs c f x'a) (?\<Gamma>2.40 a as ca cs s s' x x' xa x'a) Rs (monadic_nfoldli as c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) xa)
 3. \<And>a as ca cs s s' x x' xa x'a. \<lbrakk>\<And>s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) as cs * hn_ctxt Rs s' s) (imp_nfoldli cs c f s) (\<Gamma> * hn_ctxt (list_assn Rl'') as cs * hn_invalid Rs s' s) Rs (monadic_nfoldli as c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) s'); RETURN True \<le> c' s'; x; a \<in> S\<rbrakk> \<Longrightarrow> ?\<Gamma>2.40 a as ca cs s s' x x' xa x'a \<Longrightarrow>\<^sub>t ?\<Gamma>2b29 a as ca cs s s' True x' * hn_ctxt (?Rx40 a as ca cs s s' x x') xa x'a
 4. \<And>a as ca cs s s' x x'. \<lbrakk>\<And>s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) as cs * hn_ctxt Rs s' s) (imp_nfoldli cs c f s) (\<Gamma> * hn_ctxt (list_assn Rl'') as cs * hn_invalid Rs s' s) Rs (monadic_nfoldli as c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) s'); RETURN x \<le> c' s'; \<not> x\<rbrakk> \<Longrightarrow> hn_refine (hn_ctxt (list_assn Rl) (a # as) (ca # cs) * \<Gamma> * hn_ctxt Rs s' s * hn_val bool_rel x x') (return s) (?\<Gamma>2c29 a as ca cs s s' x x') Rs (RETURN s')
 5. \<And>a as ca cs s s' x x'. \<lbrakk>\<And>s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) as cs * hn_ctxt Rs s' s) (imp_nfoldli cs c f s) (\<Gamma> * hn_ctxt (list_assn Rl'') as cs * hn_invalid Rs s' s) Rs (monadic_nfoldli as c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) s'); RETURN x \<le> c' s'\<rbrakk> \<Longrightarrow> ?\<Gamma>2b29 a as ca cs s s' x x' \<or>\<^sub>A ?\<Gamma>2c29 a as ca cs s s' x x' \<Longrightarrow>\<^sub>t ?\<Gamma>2.17 a as ca cs s s' x x'
 6. \<And>a as ca cs s s' x x'. (\<And>s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) as cs * hn_ctxt Rs s' s) (imp_nfoldli cs c f s) (\<Gamma> * hn_ctxt (list_assn Rl'') as cs * hn_invalid Rs s' s) Rs (monadic_nfoldli as c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) s')) \<Longrightarrow> ?\<Gamma>2.17 a as ca cs s s' x x' \<Longrightarrow>\<^sub>t \<Gamma> * hn_ctxt (list_assn Rl'') (a # as) (ca # cs) * hn_invalid Rs s' s * hn_ctxt (?Rx17 a as ca cs s s') x x'
 7. \<And>v va s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) (v # va) [] * hn_ctxt Rs s' s) (imp_nfoldli [] c f s) (\<Gamma> * hn_ctxt (list_assn Rl'') (v # va) [] * hn_invalid Rs s' s) Rs (monadic_nfoldli (v # va) c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) s')
 8. \<And>v va s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) [] (v # va) * hn_ctxt Rs s' s) (imp_nfoldli (v # va) c f s) (\<Gamma> * hn_ctxt (list_assn Rl'') [] (v # va) * hn_invalid Rs s' s) Rs (monadic_nfoldli [] c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) s')
[PROOF STEP]
apply (simp add: assn_aci)
[PROOF STATE]
proof (prove)
goal (8 subgoals):
 1. \<And>a as ca cs s s' x x'. \<lbrakk>\<And>s s'. hn_refine (\<Gamma> * hn_ctxt Rs s' s * hn_ctxt (list_assn Rl) as cs) (imp_nfoldli cs c f s) (\<Gamma> * hn_invalid Rs s' s * hn_ctxt (list_assn Rl'') as cs) Rs (monadic_nfoldli as c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) s'); RETURN True \<le> c' s'; x; a \<in> S\<rbrakk> \<Longrightarrow> \<Gamma> * hn_ctxt Rl a ca * hn_ctxt Rs s' s * hn_val bool_rel True x' * hn_ctxt (list_assn Rl) as cs \<Longrightarrow>\<^sub>t \<Gamma> * hn_ctxt Rl a ca * hn_ctxt Rs s' s * ?F45 a as ca cs s s' True x'
 2. \<And>a as ca cs s s' x x' xa x'a. \<lbrakk>\<And>s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) as cs * hn_ctxt Rs s' s) (imp_nfoldli cs c f s) (\<Gamma> * hn_ctxt (list_assn Rl'') as cs * hn_invalid Rs s' s) Rs (monadic_nfoldli as c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) s'); RETURN True \<le> c' s'; x; a \<in> S; RETURN xa \<le> f' a s'\<rbrakk> \<Longrightarrow> hn_refine (?F45 a as ca cs s s' x x' * (\<Gamma> * hn_ctxt Rl' a ca * hn_invalid Rs s' s) * hn_ctxt Rs xa x'a) (imp_nfoldli cs c f x'a) (?\<Gamma>2.40 a as ca cs s s' x x' xa x'a) Rs (monadic_nfoldli as c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) xa)
 3. \<And>a as ca cs s s' x x' xa x'a. \<lbrakk>\<And>s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) as cs * hn_ctxt Rs s' s) (imp_nfoldli cs c f s) (\<Gamma> * hn_ctxt (list_assn Rl'') as cs * hn_invalid Rs s' s) Rs (monadic_nfoldli as c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) s'); RETURN True \<le> c' s'; x; a \<in> S\<rbrakk> \<Longrightarrow> ?\<Gamma>2.40 a as ca cs s s' x x' xa x'a \<Longrightarrow>\<^sub>t ?\<Gamma>2b29 a as ca cs s s' True x' * hn_ctxt (?Rx40 a as ca cs s s' x x') xa x'a
 4. \<And>a as ca cs s s' x x'. \<lbrakk>\<And>s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) as cs * hn_ctxt Rs s' s) (imp_nfoldli cs c f s) (\<Gamma> * hn_ctxt (list_assn Rl'') as cs * hn_invalid Rs s' s) Rs (monadic_nfoldli as c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) s'); RETURN x \<le> c' s'; \<not> x\<rbrakk> \<Longrightarrow> hn_refine (hn_ctxt (list_assn Rl) (a # as) (ca # cs) * \<Gamma> * hn_ctxt Rs s' s * hn_val bool_rel x x') (return s) (?\<Gamma>2c29 a as ca cs s s' x x') Rs (RETURN s')
 5. \<And>a as ca cs s s' x x'. \<lbrakk>\<And>s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) as cs * hn_ctxt Rs s' s) (imp_nfoldli cs c f s) (\<Gamma> * hn_ctxt (list_assn Rl'') as cs * hn_invalid Rs s' s) Rs (monadic_nfoldli as c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) s'); RETURN x \<le> c' s'\<rbrakk> \<Longrightarrow> ?\<Gamma>2b29 a as ca cs s s' x x' \<or>\<^sub>A ?\<Gamma>2c29 a as ca cs s s' x x' \<Longrightarrow>\<^sub>t ?\<Gamma>2.17 a as ca cs s s' x x'
 6. \<And>a as ca cs s s' x x'. (\<And>s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) as cs * hn_ctxt Rs s' s) (imp_nfoldli cs c f s) (\<Gamma> * hn_ctxt (list_assn Rl'') as cs * hn_invalid Rs s' s) Rs (monadic_nfoldli as c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) s')) \<Longrightarrow> ?\<Gamma>2.17 a as ca cs s s' x x' \<Longrightarrow>\<^sub>t \<Gamma> * hn_ctxt (list_assn Rl'') (a # as) (ca # cs) * hn_invalid Rs s' s * hn_ctxt (?Rx17 a as ca cs s s') x x'
 7. \<And>v va s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) (v # va) [] * hn_ctxt Rs s' s) (imp_nfoldli [] c f s) (\<Gamma> * hn_ctxt (list_assn Rl'') (v # va) [] * hn_invalid Rs s' s) Rs (monadic_nfoldli (v # va) c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) s')
 8. \<And>v va s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) [] (v # va) * hn_ctxt Rs s' s) (imp_nfoldli (v # va) c f s) (\<Gamma> * hn_ctxt (list_assn Rl'') [] (v # va) * hn_invalid Rs s' s) Rs (monadic_nfoldli [] c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) s')
[PROOF STEP]
apply (rule ent_imp_entt)
[PROOF STATE]
proof (prove)
goal (8 subgoals):
 1. \<And>a as ca cs s s' x x'. \<lbrakk>\<And>s s'. hn_refine (\<Gamma> * hn_ctxt Rs s' s * hn_ctxt (list_assn Rl) as cs) (imp_nfoldli cs c f s) (\<Gamma> * hn_invalid Rs s' s * hn_ctxt (list_assn Rl'') as cs) Rs (monadic_nfoldli as c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) s'); RETURN True \<le> c' s'; x; a \<in> S\<rbrakk> \<Longrightarrow> \<Gamma> * hn_ctxt Rl a ca * hn_ctxt Rs s' s * hn_val bool_rel True x' * hn_ctxt (list_assn Rl) as cs \<Longrightarrow>\<^sub>A \<Gamma> * hn_ctxt Rl a ca * hn_ctxt Rs s' s * ?F45 a as ca cs s s' True x'
 2. \<And>a as ca cs s s' x x' xa x'a. \<lbrakk>\<And>s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) as cs * hn_ctxt Rs s' s) (imp_nfoldli cs c f s) (\<Gamma> * hn_ctxt (list_assn Rl'') as cs * hn_invalid Rs s' s) Rs (monadic_nfoldli as c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) s'); RETURN True \<le> c' s'; x; a \<in> S; RETURN xa \<le> f' a s'\<rbrakk> \<Longrightarrow> hn_refine (?F45 a as ca cs s s' x x' * (\<Gamma> * hn_ctxt Rl' a ca * hn_invalid Rs s' s) * hn_ctxt Rs xa x'a) (imp_nfoldli cs c f x'a) (?\<Gamma>2.40 a as ca cs s s' x x' xa x'a) Rs (monadic_nfoldli as c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) xa)
 3. \<And>a as ca cs s s' x x' xa x'a. \<lbrakk>\<And>s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) as cs * hn_ctxt Rs s' s) (imp_nfoldli cs c f s) (\<Gamma> * hn_ctxt (list_assn Rl'') as cs * hn_invalid Rs s' s) Rs (monadic_nfoldli as c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) s'); RETURN True \<le> c' s'; x; a \<in> S\<rbrakk> \<Longrightarrow> ?\<Gamma>2.40 a as ca cs s s' x x' xa x'a \<Longrightarrow>\<^sub>t ?\<Gamma>2b29 a as ca cs s s' True x' * hn_ctxt (?Rx40 a as ca cs s s' x x') xa x'a
 4. \<And>a as ca cs s s' x x'. \<lbrakk>\<And>s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) as cs * hn_ctxt Rs s' s) (imp_nfoldli cs c f s) (\<Gamma> * hn_ctxt (list_assn Rl'') as cs * hn_invalid Rs s' s) Rs (monadic_nfoldli as c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) s'); RETURN x \<le> c' s'; \<not> x\<rbrakk> \<Longrightarrow> hn_refine (hn_ctxt (list_assn Rl) (a # as) (ca # cs) * \<Gamma> * hn_ctxt Rs s' s * hn_val bool_rel x x') (return s) (?\<Gamma>2c29 a as ca cs s s' x x') Rs (RETURN s')
 5. \<And>a as ca cs s s' x x'. \<lbrakk>\<And>s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) as cs * hn_ctxt Rs s' s) (imp_nfoldli cs c f s) (\<Gamma> * hn_ctxt (list_assn Rl'') as cs * hn_invalid Rs s' s) Rs (monadic_nfoldli as c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) s'); RETURN x \<le> c' s'\<rbrakk> \<Longrightarrow> ?\<Gamma>2b29 a as ca cs s s' x x' \<or>\<^sub>A ?\<Gamma>2c29 a as ca cs s s' x x' \<Longrightarrow>\<^sub>t ?\<Gamma>2.17 a as ca cs s s' x x'
 6. \<And>a as ca cs s s' x x'. (\<And>s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) as cs * hn_ctxt Rs s' s) (imp_nfoldli cs c f s) (\<Gamma> * hn_ctxt (list_assn Rl'') as cs * hn_invalid Rs s' s) Rs (monadic_nfoldli as c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) s')) \<Longrightarrow> ?\<Gamma>2.17 a as ca cs s s' x x' \<Longrightarrow>\<^sub>t \<Gamma> * hn_ctxt (list_assn Rl'') (a # as) (ca # cs) * hn_invalid Rs s' s * hn_ctxt (?Rx17 a as ca cs s s') x x'
 7. \<And>v va s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) (v # va) [] * hn_ctxt Rs s' s) (imp_nfoldli [] c f s) (\<Gamma> * hn_ctxt (list_assn Rl'') (v # va) [] * hn_invalid Rs s' s) Rs (monadic_nfoldli (v # va) c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) s')
 8. \<And>v va s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) [] (v # va) * hn_ctxt Rs s' s) (imp_nfoldli (v # va) c f s) (\<Gamma> * hn_ctxt (list_assn Rl'') [] (v # va) * hn_invalid Rs s' s) Rs (monadic_nfoldli [] c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) s')
[PROOF STEP]
apply (fr_rot_rhs 1)
[PROOF STATE]
proof (prove)
goal (8 subgoals):
 1. \<And>a as ca cs s s' x x'. \<lbrakk>\<And>s s'. hn_refine (\<Gamma> * hn_ctxt Rs s' s * hn_ctxt (list_assn Rl) as cs) (imp_nfoldli cs c f s) (\<Gamma> * hn_invalid Rs s' s * hn_ctxt (list_assn Rl'') as cs) Rs (monadic_nfoldli as c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) s'); RETURN True \<le> c' s'; x; a \<in> S\<rbrakk> \<Longrightarrow> \<Gamma> * hn_ctxt Rl a ca * hn_ctxt Rs s' s * hn_val bool_rel True x' * hn_ctxt (list_assn Rl) as cs \<Longrightarrow>\<^sub>A ?F45 a as ca cs s s' True x' * \<Gamma> * hn_ctxt Rl a ca * hn_ctxt Rs s' s
 2. \<And>a as ca cs s s' x x' xa x'a. \<lbrakk>\<And>s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) as cs * hn_ctxt Rs s' s) (imp_nfoldli cs c f s) (\<Gamma> * hn_ctxt (list_assn Rl'') as cs * hn_invalid Rs s' s) Rs (monadic_nfoldli as c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) s'); RETURN True \<le> c' s'; x; a \<in> S; RETURN xa \<le> f' a s'\<rbrakk> \<Longrightarrow> hn_refine (?F45 a as ca cs s s' x x' * (\<Gamma> * hn_ctxt Rl' a ca * hn_invalid Rs s' s) * hn_ctxt Rs xa x'a) (imp_nfoldli cs c f x'a) (?\<Gamma>2.40 a as ca cs s s' x x' xa x'a) Rs (monadic_nfoldli as c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) xa)
 3. \<And>a as ca cs s s' x x' xa x'a. \<lbrakk>\<And>s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) as cs * hn_ctxt Rs s' s) (imp_nfoldli cs c f s) (\<Gamma> * hn_ctxt (list_assn Rl'') as cs * hn_invalid Rs s' s) Rs (monadic_nfoldli as c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) s'); RETURN True \<le> c' s'; x; a \<in> S\<rbrakk> \<Longrightarrow> ?\<Gamma>2.40 a as ca cs s s' x x' xa x'a \<Longrightarrow>\<^sub>t ?\<Gamma>2b29 a as ca cs s s' True x' * hn_ctxt (?Rx40 a as ca cs s s' x x') xa x'a
 4. \<And>a as ca cs s s' x x'. \<lbrakk>\<And>s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) as cs * hn_ctxt Rs s' s) (imp_nfoldli cs c f s) (\<Gamma> * hn_ctxt (list_assn Rl'') as cs * hn_invalid Rs s' s) Rs (monadic_nfoldli as c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) s'); RETURN x \<le> c' s'; \<not> x\<rbrakk> \<Longrightarrow> hn_refine (hn_ctxt (list_assn Rl) (a # as) (ca # cs) * \<Gamma> * hn_ctxt Rs s' s * hn_val bool_rel x x') (return s) (?\<Gamma>2c29 a as ca cs s s' x x') Rs (RETURN s')
 5. \<And>a as ca cs s s' x x'. \<lbrakk>\<And>s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) as cs * hn_ctxt Rs s' s) (imp_nfoldli cs c f s) (\<Gamma> * hn_ctxt (list_assn Rl'') as cs * hn_invalid Rs s' s) Rs (monadic_nfoldli as c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) s'); RETURN x \<le> c' s'\<rbrakk> \<Longrightarrow> ?\<Gamma>2b29 a as ca cs s s' x x' \<or>\<^sub>A ?\<Gamma>2c29 a as ca cs s s' x x' \<Longrightarrow>\<^sub>t ?\<Gamma>2.17 a as ca cs s s' x x'
 6. \<And>a as ca cs s s' x x'. (\<And>s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) as cs * hn_ctxt Rs s' s) (imp_nfoldli cs c f s) (\<Gamma> * hn_ctxt (list_assn Rl'') as cs * hn_invalid Rs s' s) Rs (monadic_nfoldli as c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) s')) \<Longrightarrow> ?\<Gamma>2.17 a as ca cs s s' x x' \<Longrightarrow>\<^sub>t \<Gamma> * hn_ctxt (list_assn Rl'') (a # as) (ca # cs) * hn_invalid Rs s' s * hn_ctxt (?Rx17 a as ca cs s s') x x'
 7. \<And>v va s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) (v # va) [] * hn_ctxt Rs s' s) (imp_nfoldli [] c f s) (\<Gamma> * hn_ctxt (list_assn Rl'') (v # va) [] * hn_invalid Rs s' s) Rs (monadic_nfoldli (v # va) c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) s')
 8. \<And>v va s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) [] (v # va) * hn_ctxt Rs s' s) (imp_nfoldli (v # va) c f s) (\<Gamma> * hn_ctxt (list_assn Rl'') [] (v # va) * hn_invalid Rs s' s) Rs (monadic_nfoldli [] c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) s')
[PROOF STEP]
apply (fr_rot 2)
[PROOF STATE]
proof (prove)
goal (8 subgoals):
 1. \<And>a as ca cs s s' x x'. \<lbrakk>\<And>s s'. hn_refine (\<Gamma> * hn_ctxt Rs s' s * hn_ctxt (list_assn Rl) as cs) (imp_nfoldli cs c f s) (\<Gamma> * hn_invalid Rs s' s * hn_ctxt (list_assn Rl'') as cs) Rs (monadic_nfoldli as c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) s'); RETURN True \<le> c' s'; x; a \<in> S\<rbrakk> \<Longrightarrow> hn_val bool_rel True x' * hn_ctxt (list_assn Rl) as cs * \<Gamma> * hn_ctxt Rl a ca * hn_ctxt Rs s' s \<Longrightarrow>\<^sub>A ?F45 a as ca cs s s' True x' * \<Gamma> * hn_ctxt Rl a ca * hn_ctxt Rs s' s
 2. \<And>a as ca cs s s' x x' xa x'a. \<lbrakk>\<And>s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) as cs * hn_ctxt Rs s' s) (imp_nfoldli cs c f s) (\<Gamma> * hn_ctxt (list_assn Rl'') as cs * hn_invalid Rs s' s) Rs (monadic_nfoldli as c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) s'); RETURN True \<le> c' s'; x; a \<in> S; RETURN xa \<le> f' a s'\<rbrakk> \<Longrightarrow> hn_refine (?F45 a as ca cs s s' x x' * (\<Gamma> * hn_ctxt Rl' a ca * hn_invalid Rs s' s) * hn_ctxt Rs xa x'a) (imp_nfoldli cs c f x'a) (?\<Gamma>2.40 a as ca cs s s' x x' xa x'a) Rs (monadic_nfoldli as c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) xa)
 3. \<And>a as ca cs s s' x x' xa x'a. \<lbrakk>\<And>s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) as cs * hn_ctxt Rs s' s) (imp_nfoldli cs c f s) (\<Gamma> * hn_ctxt (list_assn Rl'') as cs * hn_invalid Rs s' s) Rs (monadic_nfoldli as c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) s'); RETURN True \<le> c' s'; x; a \<in> S\<rbrakk> \<Longrightarrow> ?\<Gamma>2.40 a as ca cs s s' x x' xa x'a \<Longrightarrow>\<^sub>t ?\<Gamma>2b29 a as ca cs s s' True x' * hn_ctxt (?Rx40 a as ca cs s s' x x') xa x'a
 4. \<And>a as ca cs s s' x x'. \<lbrakk>\<And>s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) as cs * hn_ctxt Rs s' s) (imp_nfoldli cs c f s) (\<Gamma> * hn_ctxt (list_assn Rl'') as cs * hn_invalid Rs s' s) Rs (monadic_nfoldli as c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) s'); RETURN x \<le> c' s'; \<not> x\<rbrakk> \<Longrightarrow> hn_refine (hn_ctxt (list_assn Rl) (a # as) (ca # cs) * \<Gamma> * hn_ctxt Rs s' s * hn_val bool_rel x x') (return s) (?\<Gamma>2c29 a as ca cs s s' x x') Rs (RETURN s')
 5. \<And>a as ca cs s s' x x'. \<lbrakk>\<And>s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) as cs * hn_ctxt Rs s' s) (imp_nfoldli cs c f s) (\<Gamma> * hn_ctxt (list_assn Rl'') as cs * hn_invalid Rs s' s) Rs (monadic_nfoldli as c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) s'); RETURN x \<le> c' s'\<rbrakk> \<Longrightarrow> ?\<Gamma>2b29 a as ca cs s s' x x' \<or>\<^sub>A ?\<Gamma>2c29 a as ca cs s s' x x' \<Longrightarrow>\<^sub>t ?\<Gamma>2.17 a as ca cs s s' x x'
 6. \<And>a as ca cs s s' x x'. (\<And>s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) as cs * hn_ctxt Rs s' s) (imp_nfoldli cs c f s) (\<Gamma> * hn_ctxt (list_assn Rl'') as cs * hn_invalid Rs s' s) Rs (monadic_nfoldli as c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) s')) \<Longrightarrow> ?\<Gamma>2.17 a as ca cs s s' x x' \<Longrightarrow>\<^sub>t \<Gamma> * hn_ctxt (list_assn Rl'') (a # as) (ca # cs) * hn_invalid Rs s' s * hn_ctxt (?Rx17 a as ca cs s s') x x'
 7. \<And>v va s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) (v # va) [] * hn_ctxt Rs s' s) (imp_nfoldli [] c f s) (\<Gamma> * hn_ctxt (list_assn Rl'') (v # va) [] * hn_invalid Rs s' s) Rs (monadic_nfoldli (v # va) c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) s')
 8. \<And>v va s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) [] (v # va) * hn_ctxt Rs s' s) (imp_nfoldli (v # va) c f s) (\<Gamma> * hn_ctxt (list_assn Rl'') [] (v # va) * hn_invalid Rs s' s) Rs (monadic_nfoldli [] c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) s')
[PROOF STEP]
apply (rule fr_refl)
[PROOF STATE]
proof (prove)
goal (8 subgoals):
 1. \<And>a as ca cs s s' x x'. \<lbrakk>\<And>s s'. hn_refine (\<Gamma> * hn_ctxt Rs s' s * hn_ctxt (list_assn Rl) as cs) (imp_nfoldli cs c f s) (\<Gamma> * hn_invalid Rs s' s * hn_ctxt (list_assn Rl'') as cs) Rs (monadic_nfoldli as c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) s'); RETURN True \<le> c' s'; x; a \<in> S\<rbrakk> \<Longrightarrow> hn_val bool_rel True x' * hn_ctxt (list_assn Rl) as cs * \<Gamma> * hn_ctxt Rl a ca \<Longrightarrow>\<^sub>A ?F45 a as ca cs s s' True x' * \<Gamma> * hn_ctxt Rl a ca
 2. \<And>a as ca cs s s' x x' xa x'a. \<lbrakk>\<And>s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) as cs * hn_ctxt Rs s' s) (imp_nfoldli cs c f s) (\<Gamma> * hn_ctxt (list_assn Rl'') as cs * hn_invalid Rs s' s) Rs (monadic_nfoldli as c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) s'); RETURN True \<le> c' s'; x; a \<in> S; RETURN xa \<le> f' a s'\<rbrakk> \<Longrightarrow> hn_refine (?F45 a as ca cs s s' x x' * (\<Gamma> * hn_ctxt Rl' a ca * hn_invalid Rs s' s) * hn_ctxt Rs xa x'a) (imp_nfoldli cs c f x'a) (?\<Gamma>2.40 a as ca cs s s' x x' xa x'a) Rs (monadic_nfoldli as c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) xa)
 3. \<And>a as ca cs s s' x x' xa x'a. \<lbrakk>\<And>s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) as cs * hn_ctxt Rs s' s) (imp_nfoldli cs c f s) (\<Gamma> * hn_ctxt (list_assn Rl'') as cs * hn_invalid Rs s' s) Rs (monadic_nfoldli as c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) s'); RETURN True \<le> c' s'; x; a \<in> S\<rbrakk> \<Longrightarrow> ?\<Gamma>2.40 a as ca cs s s' x x' xa x'a \<Longrightarrow>\<^sub>t ?\<Gamma>2b29 a as ca cs s s' True x' * hn_ctxt (?Rx40 a as ca cs s s' x x') xa x'a
 4. \<And>a as ca cs s s' x x'. \<lbrakk>\<And>s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) as cs * hn_ctxt Rs s' s) (imp_nfoldli cs c f s) (\<Gamma> * hn_ctxt (list_assn Rl'') as cs * hn_invalid Rs s' s) Rs (monadic_nfoldli as c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) s'); RETURN x \<le> c' s'; \<not> x\<rbrakk> \<Longrightarrow> hn_refine (hn_ctxt (list_assn Rl) (a # as) (ca # cs) * \<Gamma> * hn_ctxt Rs s' s * hn_val bool_rel x x') (return s) (?\<Gamma>2c29 a as ca cs s s' x x') Rs (RETURN s')
 5. \<And>a as ca cs s s' x x'. \<lbrakk>\<And>s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) as cs * hn_ctxt Rs s' s) (imp_nfoldli cs c f s) (\<Gamma> * hn_ctxt (list_assn Rl'') as cs * hn_invalid Rs s' s) Rs (monadic_nfoldli as c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) s'); RETURN x \<le> c' s'\<rbrakk> \<Longrightarrow> ?\<Gamma>2b29 a as ca cs s s' x x' \<or>\<^sub>A ?\<Gamma>2c29 a as ca cs s s' x x' \<Longrightarrow>\<^sub>t ?\<Gamma>2.17 a as ca cs s s' x x'
 6. \<And>a as ca cs s s' x x'. (\<And>s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) as cs * hn_ctxt Rs s' s) (imp_nfoldli cs c f s) (\<Gamma> * hn_ctxt (list_assn Rl'') as cs * hn_invalid Rs s' s) Rs (monadic_nfoldli as c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) s')) \<Longrightarrow> ?\<Gamma>2.17 a as ca cs s s' x x' \<Longrightarrow>\<^sub>t \<Gamma> * hn_ctxt (list_assn Rl'') (a # as) (ca # cs) * hn_invalid Rs s' s * hn_ctxt (?Rx17 a as ca cs s s') x x'
 7. \<And>v va s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) (v # va) [] * hn_ctxt Rs s' s) (imp_nfoldli [] c f s) (\<Gamma> * hn_ctxt (list_assn Rl'') (v # va) [] * hn_invalid Rs s' s) Rs (monadic_nfoldli (v # va) c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) s')
 8. \<And>v va s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) [] (v # va) * hn_ctxt Rs s' s) (imp_nfoldli (v # va) c f s) (\<Gamma> * hn_ctxt (list_assn Rl'') [] (v # va) * hn_invalid Rs s' s) Rs (monadic_nfoldli [] c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) s')
[PROOF STEP]
apply (rule fr_refl)
[PROOF STATE]
proof (prove)
goal (8 subgoals):
 1. \<And>a as ca cs s s' x x'. \<lbrakk>\<And>s s'. hn_refine (\<Gamma> * hn_ctxt Rs s' s * hn_ctxt (list_assn Rl) as cs) (imp_nfoldli cs c f s) (\<Gamma> * hn_invalid Rs s' s * hn_ctxt (list_assn Rl'') as cs) Rs (monadic_nfoldli as c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) s'); RETURN True \<le> c' s'; x; a \<in> S\<rbrakk> \<Longrightarrow> hn_val bool_rel True x' * hn_ctxt (list_assn Rl) as cs * \<Gamma> \<Longrightarrow>\<^sub>A ?F45 a as ca cs s s' True x' * \<Gamma>
 2. \<And>a as ca cs s s' x x' xa x'a. \<lbrakk>\<And>s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) as cs * hn_ctxt Rs s' s) (imp_nfoldli cs c f s) (\<Gamma> * hn_ctxt (list_assn Rl'') as cs * hn_invalid Rs s' s) Rs (monadic_nfoldli as c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) s'); RETURN True \<le> c' s'; x; a \<in> S; RETURN xa \<le> f' a s'\<rbrakk> \<Longrightarrow> hn_refine (?F45 a as ca cs s s' x x' * (\<Gamma> * hn_ctxt Rl' a ca * hn_invalid Rs s' s) * hn_ctxt Rs xa x'a) (imp_nfoldli cs c f x'a) (?\<Gamma>2.40 a as ca cs s s' x x' xa x'a) Rs (monadic_nfoldli as c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) xa)
 3. \<And>a as ca cs s s' x x' xa x'a. \<lbrakk>\<And>s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) as cs * hn_ctxt Rs s' s) (imp_nfoldli cs c f s) (\<Gamma> * hn_ctxt (list_assn Rl'') as cs * hn_invalid Rs s' s) Rs (monadic_nfoldli as c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) s'); RETURN True \<le> c' s'; x; a \<in> S\<rbrakk> \<Longrightarrow> ?\<Gamma>2.40 a as ca cs s s' x x' xa x'a \<Longrightarrow>\<^sub>t ?\<Gamma>2b29 a as ca cs s s' True x' * hn_ctxt (?Rx40 a as ca cs s s' x x') xa x'a
 4. \<And>a as ca cs s s' x x'. \<lbrakk>\<And>s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) as cs * hn_ctxt Rs s' s) (imp_nfoldli cs c f s) (\<Gamma> * hn_ctxt (list_assn Rl'') as cs * hn_invalid Rs s' s) Rs (monadic_nfoldli as c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) s'); RETURN x \<le> c' s'; \<not> x\<rbrakk> \<Longrightarrow> hn_refine (hn_ctxt (list_assn Rl) (a # as) (ca # cs) * \<Gamma> * hn_ctxt Rs s' s * hn_val bool_rel x x') (return s) (?\<Gamma>2c29 a as ca cs s s' x x') Rs (RETURN s')
 5. \<And>a as ca cs s s' x x'. \<lbrakk>\<And>s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) as cs * hn_ctxt Rs s' s) (imp_nfoldli cs c f s) (\<Gamma> * hn_ctxt (list_assn Rl'') as cs * hn_invalid Rs s' s) Rs (monadic_nfoldli as c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) s'); RETURN x \<le> c' s'\<rbrakk> \<Longrightarrow> ?\<Gamma>2b29 a as ca cs s s' x x' \<or>\<^sub>A ?\<Gamma>2c29 a as ca cs s s' x x' \<Longrightarrow>\<^sub>t ?\<Gamma>2.17 a as ca cs s s' x x'
 6. \<And>a as ca cs s s' x x'. (\<And>s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) as cs * hn_ctxt Rs s' s) (imp_nfoldli cs c f s) (\<Gamma> * hn_ctxt (list_assn Rl'') as cs * hn_invalid Rs s' s) Rs (monadic_nfoldli as c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) s')) \<Longrightarrow> ?\<Gamma>2.17 a as ca cs s s' x x' \<Longrightarrow>\<^sub>t \<Gamma> * hn_ctxt (list_assn Rl'') (a # as) (ca # cs) * hn_invalid Rs s' s * hn_ctxt (?Rx17 a as ca cs s s') x x'
 7. \<And>v va s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) (v # va) [] * hn_ctxt Rs s' s) (imp_nfoldli [] c f s) (\<Gamma> * hn_ctxt (list_assn Rl'') (v # va) [] * hn_invalid Rs s' s) Rs (monadic_nfoldli (v # va) c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) s')
 8. \<And>v va s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) [] (v # va) * hn_ctxt Rs s' s) (imp_nfoldli (v # va) c f s) (\<Gamma> * hn_ctxt (list_assn Rl'') [] (v # va) * hn_invalid Rs s' s) Rs (monadic_nfoldli [] c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) s')
[PROOF STEP]
apply (rule fr_refl)
[PROOF STATE]
proof (prove)
goal (8 subgoals):
 1. \<And>a as ca cs s s' x x'. \<lbrakk>\<And>s s'. hn_refine (\<Gamma> * hn_ctxt Rs s' s * hn_ctxt (list_assn Rl) as cs) (imp_nfoldli cs c f s) (\<Gamma> * hn_invalid Rs s' s * hn_ctxt (list_assn Rl'') as cs) Rs (monadic_nfoldli as c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) s'); RETURN True \<le> c' s'; x; a \<in> S\<rbrakk> \<Longrightarrow> hn_val bool_rel True x' * hn_ctxt (list_assn Rl) as cs \<Longrightarrow>\<^sub>A ?F45 a as ca cs s s' True x'
 2. \<And>a as ca cs s s' x x' xa x'a. \<lbrakk>\<And>s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) as cs * hn_ctxt Rs s' s) (imp_nfoldli cs c f s) (\<Gamma> * hn_ctxt (list_assn Rl'') as cs * hn_invalid Rs s' s) Rs (monadic_nfoldli as c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) s'); RETURN True \<le> c' s'; x; a \<in> S; RETURN xa \<le> f' a s'\<rbrakk> \<Longrightarrow> hn_refine (?F45 a as ca cs s s' x x' * (\<Gamma> * hn_ctxt Rl' a ca * hn_invalid Rs s' s) * hn_ctxt Rs xa x'a) (imp_nfoldli cs c f x'a) (?\<Gamma>2.40 a as ca cs s s' x x' xa x'a) Rs (monadic_nfoldli as c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) xa)
 3. \<And>a as ca cs s s' x x' xa x'a. \<lbrakk>\<And>s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) as cs * hn_ctxt Rs s' s) (imp_nfoldli cs c f s) (\<Gamma> * hn_ctxt (list_assn Rl'') as cs * hn_invalid Rs s' s) Rs (monadic_nfoldli as c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) s'); RETURN True \<le> c' s'; x; a \<in> S\<rbrakk> \<Longrightarrow> ?\<Gamma>2.40 a as ca cs s s' x x' xa x'a \<Longrightarrow>\<^sub>t ?\<Gamma>2b29 a as ca cs s s' True x' * hn_ctxt (?Rx40 a as ca cs s s' x x') xa x'a
 4. \<And>a as ca cs s s' x x'. \<lbrakk>\<And>s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) as cs * hn_ctxt Rs s' s) (imp_nfoldli cs c f s) (\<Gamma> * hn_ctxt (list_assn Rl'') as cs * hn_invalid Rs s' s) Rs (monadic_nfoldli as c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) s'); RETURN x \<le> c' s'; \<not> x\<rbrakk> \<Longrightarrow> hn_refine (hn_ctxt (list_assn Rl) (a # as) (ca # cs) * \<Gamma> * hn_ctxt Rs s' s * hn_val bool_rel x x') (return s) (?\<Gamma>2c29 a as ca cs s s' x x') Rs (RETURN s')
 5. \<And>a as ca cs s s' x x'. \<lbrakk>\<And>s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) as cs * hn_ctxt Rs s' s) (imp_nfoldli cs c f s) (\<Gamma> * hn_ctxt (list_assn Rl'') as cs * hn_invalid Rs s' s) Rs (monadic_nfoldli as c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) s'); RETURN x \<le> c' s'\<rbrakk> \<Longrightarrow> ?\<Gamma>2b29 a as ca cs s s' x x' \<or>\<^sub>A ?\<Gamma>2c29 a as ca cs s s' x x' \<Longrightarrow>\<^sub>t ?\<Gamma>2.17 a as ca cs s s' x x'
 6. \<And>a as ca cs s s' x x'. (\<And>s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) as cs * hn_ctxt Rs s' s) (imp_nfoldli cs c f s) (\<Gamma> * hn_ctxt (list_assn Rl'') as cs * hn_invalid Rs s' s) Rs (monadic_nfoldli as c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) s')) \<Longrightarrow> ?\<Gamma>2.17 a as ca cs s s' x x' \<Longrightarrow>\<^sub>t \<Gamma> * hn_ctxt (list_assn Rl'') (a # as) (ca # cs) * hn_invalid Rs s' s * hn_ctxt (?Rx17 a as ca cs s s') x x'
 7. \<And>v va s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) (v # va) [] * hn_ctxt Rs s' s) (imp_nfoldli [] c f s) (\<Gamma> * hn_ctxt (list_assn Rl'') (v # va) [] * hn_invalid Rs s' s) Rs (monadic_nfoldli (v # va) c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) s')
 8. \<And>v va s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) [] (v # va) * hn_ctxt Rs s' s) (imp_nfoldli (v # va) c f s) (\<Gamma> * hn_ctxt (list_assn Rl'') [] (v # va) * hn_invalid Rs s' s) Rs (monadic_nfoldli [] c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) s')
[PROOF STEP]
apply (rule ent_refl)
[PROOF STATE]
proof (prove)
goal (7 subgoals):
 1. \<And>a as ca cs s s' x x' xa x'a. \<lbrakk>\<And>s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) as cs * hn_ctxt Rs s' s) (imp_nfoldli cs c f s) (\<Gamma> * hn_ctxt (list_assn Rl'') as cs * hn_invalid Rs s' s) Rs (monadic_nfoldli as c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) s'); RETURN True \<le> c' s'; x; a \<in> S; RETURN xa \<le> f' a s'\<rbrakk> \<Longrightarrow> hn_refine (hn_val bool_rel x x' * hn_ctxt (list_assn Rl) as cs * (\<Gamma> * hn_ctxt Rl' a ca * hn_invalid Rs s' s) * hn_ctxt Rs xa x'a) (imp_nfoldli cs c f x'a) (?\<Gamma>2.40 a as ca cs s s' x x' xa x'a) Rs (monadic_nfoldli as c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) xa)
 2. \<And>a as ca cs s s' x x' xa x'a. \<lbrakk>\<And>s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) as cs * hn_ctxt Rs s' s) (imp_nfoldli cs c f s) (\<Gamma> * hn_ctxt (list_assn Rl'') as cs * hn_invalid Rs s' s) Rs (monadic_nfoldli as c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) s'); RETURN True \<le> c' s'; x; a \<in> S\<rbrakk> \<Longrightarrow> ?\<Gamma>2.40 a as ca cs s s' x x' xa x'a \<Longrightarrow>\<^sub>t ?\<Gamma>2b29 a as ca cs s s' True x' * hn_ctxt (?Rx40 a as ca cs s s' x x') xa x'a
 3. \<And>a as ca cs s s' x x'. \<lbrakk>\<And>s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) as cs * hn_ctxt Rs s' s) (imp_nfoldli cs c f s) (\<Gamma> * hn_ctxt (list_assn Rl'') as cs * hn_invalid Rs s' s) Rs (monadic_nfoldli as c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) s'); RETURN x \<le> c' s'; \<not> x\<rbrakk> \<Longrightarrow> hn_refine (hn_ctxt (list_assn Rl) (a # as) (ca # cs) * \<Gamma> * hn_ctxt Rs s' s * hn_val bool_rel x x') (return s) (?\<Gamma>2c29 a as ca cs s s' x x') Rs (RETURN s')
 4. \<And>a as ca cs s s' x x'. \<lbrakk>\<And>s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) as cs * hn_ctxt Rs s' s) (imp_nfoldli cs c f s) (\<Gamma> * hn_ctxt (list_assn Rl'') as cs * hn_invalid Rs s' s) Rs (monadic_nfoldli as c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) s'); RETURN x \<le> c' s'\<rbrakk> \<Longrightarrow> ?\<Gamma>2b29 a as ca cs s s' x x' \<or>\<^sub>A ?\<Gamma>2c29 a as ca cs s s' x x' \<Longrightarrow>\<^sub>t ?\<Gamma>2.17 a as ca cs s s' x x'
 5. \<And>a as ca cs s s' x x'. (\<And>s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) as cs * hn_ctxt Rs s' s) (imp_nfoldli cs c f s) (\<Gamma> * hn_ctxt (list_assn Rl'') as cs * hn_invalid Rs s' s) Rs (monadic_nfoldli as c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) s')) \<Longrightarrow> ?\<Gamma>2.17 a as ca cs s s' x x' \<Longrightarrow>\<^sub>t \<Gamma> * hn_ctxt (list_assn Rl'') (a # as) (ca # cs) * hn_invalid Rs s' s * hn_ctxt (?Rx17 a as ca cs s s') x x'
 6. \<And>v va s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) (v # va) [] * hn_ctxt Rs s' s) (imp_nfoldli [] c f s) (\<Gamma> * hn_ctxt (list_assn Rl'') (v # va) [] * hn_invalid Rs s' s) Rs (monadic_nfoldli (v # va) c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) s')
 7. \<And>v va s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) [] (v # va) * hn_ctxt Rs s' s) (imp_nfoldli (v # va) c f s) (\<Gamma> * hn_ctxt (list_assn Rl'') [] (v # va) * hn_invalid Rs s' s) Rs (monadic_nfoldli [] c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) s')
[PROOF STEP]
applyF (rule hn_refine_frame)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a as ca cs s s' x x' xa x'a. \<lbrakk>\<And>s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) as cs * hn_ctxt Rs s' s) (imp_nfoldli cs c f s) (\<Gamma> * hn_ctxt (list_assn Rl'') as cs * hn_invalid Rs s' s) Rs (monadic_nfoldli as c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) s'); RETURN True \<le> c' s'; x; a \<in> S; RETURN xa \<le> f' a s'\<rbrakk> \<Longrightarrow> hn_refine (?P'64 a as ca cs s s' x x' xa x'a) (imp_nfoldli cs c f x'a) (?Q'64 a as ca cs s s' x x' xa x'a) Rs (monadic_nfoldli as c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) xa)
 2. \<And>a as ca cs s s' x x' xa x'a. \<lbrakk>\<And>s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) as cs * hn_ctxt Rs s' s) (imp_nfoldli cs c f s) (\<Gamma> * hn_ctxt (list_assn Rl'') as cs * hn_invalid Rs s' s) Rs (monadic_nfoldli as c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) s'); RETURN True \<le> c' s'; x; a \<in> S; RETURN xa \<le> f' a s'\<rbrakk> \<Longrightarrow> hn_val bool_rel x x' * hn_ctxt (list_assn Rl) as cs * (\<Gamma> * hn_ctxt Rl' a ca * hn_invalid Rs s' s) * hn_ctxt Rs xa x'a \<Longrightarrow>\<^sub>t ?F64 a as ca cs s s' x x' xa x'a * ?P'64 a as ca cs s s' x x' xa x'a
[PROOF STEP]
applyS rprems
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a as ca cs s s' x x' xa x'a. \<lbrakk>\<And>s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) as cs * hn_ctxt Rs s' s) (imp_nfoldli cs c f s) (\<Gamma> * hn_ctxt (list_assn Rl'') as cs * hn_invalid Rs s' s) Rs (monadic_nfoldli as c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) s'); RETURN True \<le> c' s'; x; a \<in> S; RETURN xa \<le> f' a s'\<rbrakk> \<Longrightarrow> hn_val bool_rel x x' * hn_ctxt (list_assn Rl) as cs * (\<Gamma> * hn_ctxt Rl' a ca * hn_invalid Rs s' s) * hn_ctxt Rs xa x'a \<Longrightarrow>\<^sub>t ?F64 a as ca cs s s' x x' xa x'a * (\<Gamma> * hn_ctxt (list_assn Rl) as cs * hn_ctxt Rs xa x'a)
[PROOF STEP]
focus
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a as ca cs s s' x x' xa x'a. \<lbrakk>\<And>s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) as cs * hn_ctxt Rs s' s) (imp_nfoldli cs c f s) (\<Gamma> * hn_ctxt (list_assn Rl'') as cs * hn_invalid Rs s' s) Rs (monadic_nfoldli as c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) s'); RETURN True \<le> c' s'; x; a \<in> S; RETURN xa \<le> f' a s'\<rbrakk> \<Longrightarrow> hn_val bool_rel x x' * hn_ctxt (list_assn Rl) as cs * (\<Gamma> * hn_ctxt Rl' a ca * hn_invalid Rs s' s) * hn_ctxt Rs xa x'a \<Longrightarrow>\<^sub>t ?F64 a as ca cs s s' x x' xa x'a * (\<Gamma> * hn_ctxt (list_assn Rl) as cs * hn_ctxt Rs xa x'a)
[PROOF STEP]
apply (simp add: assn_aci)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a as ca cs s s' x x' xa x'a. \<lbrakk>\<And>s s'. hn_refine (\<Gamma> * hn_ctxt Rs s' s * hn_ctxt (list_assn Rl) as cs) (imp_nfoldli cs c f s) (\<Gamma> * hn_invalid Rs s' s * hn_ctxt (list_assn Rl'') as cs) Rs (monadic_nfoldli as c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) s'); RETURN True \<le> c' s'; x; a \<in> S; RETURN xa \<le> f' a s'\<rbrakk> \<Longrightarrow> \<Gamma> * hn_ctxt Rl' a ca * hn_ctxt Rs xa x'a * hn_invalid Rs s' s * hn_val bool_rel True x' * hn_ctxt (list_assn Rl) as cs \<Longrightarrow>\<^sub>t \<Gamma> * hn_ctxt Rs xa x'a * hn_ctxt (list_assn Rl) as cs * ?F64 a as ca cs s s' True x' xa x'a
[PROOF STEP]
apply (rule ent_imp_entt)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a as ca cs s s' x x' xa x'a. \<lbrakk>\<And>s s'. hn_refine (\<Gamma> * hn_ctxt Rs s' s * hn_ctxt (list_assn Rl) as cs) (imp_nfoldli cs c f s) (\<Gamma> * hn_invalid Rs s' s * hn_ctxt (list_assn Rl'') as cs) Rs (monadic_nfoldli as c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) s'); RETURN True \<le> c' s'; x; a \<in> S; RETURN xa \<le> f' a s'\<rbrakk> \<Longrightarrow> \<Gamma> * hn_ctxt Rl' a ca * hn_ctxt Rs xa x'a * hn_invalid Rs s' s * hn_val bool_rel True x' * hn_ctxt (list_assn Rl) as cs \<Longrightarrow>\<^sub>A \<Gamma> * hn_ctxt Rs xa x'a * hn_ctxt (list_assn Rl) as cs * ?F64 a as ca cs s s' True x' xa x'a
[PROOF STEP]
apply (fr_rot_rhs 1, rule fr_refl)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a as ca cs s s' x x' xa x'a. \<lbrakk>\<And>s s'. hn_refine (\<Gamma> * hn_ctxt Rs s' s * hn_ctxt (list_assn Rl) as cs) (imp_nfoldli cs c f s) (\<Gamma> * hn_invalid Rs s' s * hn_ctxt (list_assn Rl'') as cs) Rs (monadic_nfoldli as c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) s'); RETURN True \<le> c' s'; x; a \<in> S; RETURN xa \<le> f' a s'\<rbrakk> \<Longrightarrow> \<Gamma> * hn_ctxt Rl' a ca * hn_ctxt Rs xa x'a * hn_invalid Rs s' s * hn_val bool_rel True x' \<Longrightarrow>\<^sub>A ?F64 a as ca cs s s' True x' xa x'a * \<Gamma> * hn_ctxt Rs xa x'a
[PROOF STEP]
apply (fr_rot 2, rule fr_refl)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a as ca cs s s' x x' xa x'a. \<lbrakk>\<And>s s'. hn_refine (\<Gamma> * hn_ctxt Rs s' s * hn_ctxt (list_assn Rl) as cs) (imp_nfoldli cs c f s) (\<Gamma> * hn_invalid Rs s' s * hn_ctxt (list_assn Rl'') as cs) Rs (monadic_nfoldli as c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) s'); RETURN True \<le> c' s'; x; a \<in> S; RETURN xa \<le> f' a s'\<rbrakk> \<Longrightarrow> hn_invalid Rs s' s * hn_val bool_rel True x' * \<Gamma> * hn_ctxt Rl' a ca \<Longrightarrow>\<^sub>A ?F64 a as ca cs s s' True x' xa x'a * \<Gamma>
[PROOF STEP]
apply (fr_rot 1, rule fr_refl)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a as ca cs s s' x x' xa x'a. \<lbrakk>\<And>s s'. hn_refine (\<Gamma> * hn_ctxt Rs s' s * hn_ctxt (list_assn Rl) as cs) (imp_nfoldli cs c f s) (\<Gamma> * hn_invalid Rs s' s * hn_ctxt (list_assn Rl'') as cs) Rs (monadic_nfoldli as c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) s'); RETURN True \<le> c' s'; x; a \<in> S; RETURN xa \<le> f' a s'\<rbrakk> \<Longrightarrow> hn_ctxt Rl' a ca * hn_invalid Rs s' s * hn_val bool_rel True x' \<Longrightarrow>\<^sub>A ?F64 a as ca cs s s' True x' xa x'a
[PROOF STEP]
apply (rule ent_refl)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
solved
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
solved
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<And>a as ca cs s s' x x' xa x'a. \<lbrakk>\<And>s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) as cs * hn_ctxt Rs s' s) (imp_nfoldli cs c f s) (\<Gamma> * hn_ctxt (list_assn Rl'') as cs * hn_invalid Rs s' s) Rs (monadic_nfoldli as c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) s'); RETURN True \<le> c' s'; x; a \<in> S\<rbrakk> \<Longrightarrow> hn_ctxt Rl' a ca * hn_invalid Rs s' s * hn_val bool_rel x x' * (\<Gamma> * hn_ctxt (list_assn Rl'') as cs * hn_invalid Rs xa x'a) \<Longrightarrow>\<^sub>t ?\<Gamma>2b29 a as ca cs s s' True x' * hn_ctxt (?Rx40 a as ca cs s s' x x') xa x'a
 2. \<And>a as ca cs s s' x x'. \<lbrakk>\<And>s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) as cs * hn_ctxt Rs s' s) (imp_nfoldli cs c f s) (\<Gamma> * hn_ctxt (list_assn Rl'') as cs * hn_invalid Rs s' s) Rs (monadic_nfoldli as c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) s'); RETURN x \<le> c' s'; \<not> x\<rbrakk> \<Longrightarrow> hn_refine (hn_ctxt (list_assn Rl) (a # as) (ca # cs) * \<Gamma> * hn_ctxt Rs s' s * hn_val bool_rel x x') (return s) (?\<Gamma>2c29 a as ca cs s s' x x') Rs (RETURN s')
 3. \<And>a as ca cs s s' x x'. \<lbrakk>\<And>s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) as cs * hn_ctxt Rs s' s) (imp_nfoldli cs c f s) (\<Gamma> * hn_ctxt (list_assn Rl'') as cs * hn_invalid Rs s' s) Rs (monadic_nfoldli as c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) s'); RETURN x \<le> c' s'\<rbrakk> \<Longrightarrow> ?\<Gamma>2b29 a as ca cs s s' x x' \<or>\<^sub>A ?\<Gamma>2c29 a as ca cs s s' x x' \<Longrightarrow>\<^sub>t ?\<Gamma>2.17 a as ca cs s s' x x'
 4. \<And>a as ca cs s s' x x'. (\<And>s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) as cs * hn_ctxt Rs s' s) (imp_nfoldli cs c f s) (\<Gamma> * hn_ctxt (list_assn Rl'') as cs * hn_invalid Rs s' s) Rs (monadic_nfoldli as c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) s')) \<Longrightarrow> ?\<Gamma>2.17 a as ca cs s s' x x' \<Longrightarrow>\<^sub>t \<Gamma> * hn_ctxt (list_assn Rl'') (a # as) (ca # cs) * hn_invalid Rs s' s * hn_ctxt (?Rx17 a as ca cs s s') x x'
 5. \<And>v va s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) (v # va) [] * hn_ctxt Rs s' s) (imp_nfoldli [] c f s) (\<Gamma> * hn_ctxt (list_assn Rl'') (v # va) [] * hn_invalid Rs s' s) Rs (monadic_nfoldli (v # va) c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) s')
 6. \<And>v va s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) [] (v # va) * hn_ctxt Rs s' s) (imp_nfoldli (v # va) c f s) (\<Gamma> * hn_ctxt (list_assn Rl'') [] (v # va) * hn_invalid Rs s' s) Rs (monadic_nfoldli [] c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) s')
[PROOF STEP]
focus (simp add: assn_assoc)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a as ca cs s s' x x' xa x'a. \<lbrakk>\<And>s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) as cs * hn_ctxt Rs s' s) (imp_nfoldli cs c f s) (\<Gamma> * hn_ctxt (list_assn Rl'') as cs * hn_invalid Rs s' s) Rs (monadic_nfoldli as c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) s'); RETURN True \<le> c' s'; x; a \<in> S\<rbrakk> \<Longrightarrow> hn_ctxt Rl' a ca * hn_invalid Rs s' s * hn_val bool_rel True x' * \<Gamma> * hn_ctxt (list_assn Rl'') as cs * hn_invalid Rs xa x'a \<Longrightarrow>\<^sub>t ?\<Gamma>2b29 a as ca cs s s' True x' * hn_ctxt (?Rx40 a as ca cs s s' True x') xa x'a
[PROOF STEP]
apply (rule ent_imp_entt)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a as ca cs s s' x x' xa x'a. \<lbrakk>\<And>s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) as cs * hn_ctxt Rs s' s) (imp_nfoldli cs c f s) (\<Gamma> * hn_ctxt (list_assn Rl'') as cs * hn_invalid Rs s' s) Rs (monadic_nfoldli as c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) s'); RETURN True \<le> c' s'; x; a \<in> S\<rbrakk> \<Longrightarrow> hn_ctxt Rl' a ca * hn_invalid Rs s' s * hn_val bool_rel True x' * \<Gamma> * hn_ctxt (list_assn Rl'') as cs * hn_invalid Rs xa x'a \<Longrightarrow>\<^sub>A ?\<Gamma>2b29 a as ca cs s s' True x' * hn_ctxt (?Rx40 a as ca cs s s' True x') xa x'a
[PROOF STEP]
apply (rule fr_refl)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a as ca cs s s' x x' xa x'a. \<lbrakk>\<And>s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) as cs * hn_ctxt Rs s' s) (imp_nfoldli cs c f s) (\<Gamma> * hn_ctxt (list_assn Rl'') as cs * hn_invalid Rs s' s) Rs (monadic_nfoldli as c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) s'); RETURN True \<le> c' s'; x; a \<in> S\<rbrakk> \<Longrightarrow> hn_ctxt Rl' a ca * hn_invalid Rs s' s * hn_val bool_rel True x' * \<Gamma> * hn_ctxt (list_assn Rl'') as cs \<Longrightarrow>\<^sub>A ?\<Gamma>2b29 a as ca cs s s' True x'
[PROOF STEP]
apply (rule ent_refl)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
solved
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>a as ca cs s s' x x'. \<lbrakk>\<And>s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) as cs * hn_ctxt Rs s' s) (imp_nfoldli cs c f s) (\<Gamma> * hn_ctxt (list_assn Rl'') as cs * hn_invalid Rs s' s) Rs (monadic_nfoldli as c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) s'); RETURN x \<le> c' s'; \<not> x\<rbrakk> \<Longrightarrow> hn_refine (hn_ctxt (list_assn Rl) (a # as) (ca # cs) * \<Gamma> * hn_ctxt Rs s' s * hn_val bool_rel x x') (return s) (?\<Gamma>2c29 a as ca cs s s' x x') Rs (RETURN s')
 2. \<And>a as ca cs s s' x x'. \<lbrakk>\<And>s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) as cs * hn_ctxt Rs s' s) (imp_nfoldli cs c f s) (\<Gamma> * hn_ctxt (list_assn Rl'') as cs * hn_invalid Rs s' s) Rs (monadic_nfoldli as c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) s'); RETURN x \<le> c' s'\<rbrakk> \<Longrightarrow> hn_ctxt Rl' a ca * hn_invalid Rs s' s * hn_val bool_rel x x' * \<Gamma> * hn_ctxt (list_assn Rl'') as cs \<or>\<^sub>A ?\<Gamma>2c29 a as ca cs s s' x x' \<Longrightarrow>\<^sub>t ?\<Gamma>2.17 a as ca cs s s' x x'
 3. \<And>a as ca cs s s' x x'. (\<And>s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) as cs * hn_ctxt Rs s' s) (imp_nfoldli cs c f s) (\<Gamma> * hn_ctxt (list_assn Rl'') as cs * hn_invalid Rs s' s) Rs (monadic_nfoldli as c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) s')) \<Longrightarrow> ?\<Gamma>2.17 a as ca cs s s' x x' \<Longrightarrow>\<^sub>t \<Gamma> * hn_ctxt (list_assn Rl'') (a # as) (ca # cs) * hn_invalid Rs s' s * hn_ctxt (?Rx17 a as ca cs s s') x x'
 4. \<And>v va s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) (v # va) [] * hn_ctxt Rs s' s) (imp_nfoldli [] c f s) (\<Gamma> * hn_ctxt (list_assn Rl'') (v # va) [] * hn_invalid Rs s' s) Rs (monadic_nfoldli (v # va) c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) s')
 5. \<And>v va s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) [] (v # va) * hn_ctxt Rs s' s) (imp_nfoldli (v # va) c f s) (\<Gamma> * hn_ctxt (list_assn Rl'') [] (v # va) * hn_invalid Rs s' s) Rs (monadic_nfoldli [] c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) s')
[PROOF STEP]
apply1 (rule hn_refine_frame[OF hnr_RETURN_pass])
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>a as ca cs s s' x x'. \<lbrakk>\<And>s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) as cs * hn_ctxt Rs s' s) (imp_nfoldli cs c f s) (\<Gamma> * hn_ctxt (list_assn Rl'') as cs * hn_invalid Rs s' s) Rs (monadic_nfoldli as c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) s'); RETURN x \<le> c' s'; \<not> x\<rbrakk> \<Longrightarrow> hn_ctxt (list_assn Rl) (a # as) (ca # cs) * \<Gamma> * hn_ctxt Rs s' s * hn_val bool_rel x x' \<Longrightarrow>\<^sub>t ?F170 a as ca cs s s' x x' * hn_ctxt Rs s' s
 2. \<And>a as ca cs s s' x x'. \<lbrakk>\<And>s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) as cs * hn_ctxt Rs s' s) (imp_nfoldli cs c f s) (\<Gamma> * hn_ctxt (list_assn Rl'') as cs * hn_invalid Rs s' s) Rs (monadic_nfoldli as c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) s'); RETURN x \<le> c' s'\<rbrakk> \<Longrightarrow> hn_ctxt Rl' a ca * hn_invalid Rs s' s * hn_val bool_rel x x' * \<Gamma> * hn_ctxt (list_assn Rl'') as cs \<or>\<^sub>A ?F170 a as ca cs s s' x x' * hn_invalid Rs s' s \<Longrightarrow>\<^sub>t ?\<Gamma>2.17 a as ca cs s s' x x'
 3. \<And>a as ca cs s s' x x'. (\<And>s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) as cs * hn_ctxt Rs s' s) (imp_nfoldli cs c f s) (\<Gamma> * hn_ctxt (list_assn Rl'') as cs * hn_invalid Rs s' s) Rs (monadic_nfoldli as c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) s')) \<Longrightarrow> ?\<Gamma>2.17 a as ca cs s s' x x' \<Longrightarrow>\<^sub>t \<Gamma> * hn_ctxt (list_assn Rl'') (a # as) (ca # cs) * hn_invalid Rs s' s * hn_ctxt (?Rx17 a as ca cs s s') x x'
 4. \<And>v va s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) (v # va) [] * hn_ctxt Rs s' s) (imp_nfoldli [] c f s) (\<Gamma> * hn_ctxt (list_assn Rl'') (v # va) [] * hn_invalid Rs s' s) Rs (monadic_nfoldli (v # va) c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) s')
 5. \<And>v va s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) [] (v # va) * hn_ctxt Rs s' s) (imp_nfoldli (v # va) c f s) (\<Gamma> * hn_ctxt (list_assn Rl'') [] (v # va) * hn_invalid Rs s' s) Rs (monadic_nfoldli [] c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) s')
[PROOF STEP]
applyS (tactic \<open>Sepref_Frame.frame_tac (K (K no_tac)) @{context} 1\<close>)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>a as ca cs s s' x x'. \<lbrakk>\<And>s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) as cs * hn_ctxt Rs s' s) (imp_nfoldli cs c f s) (\<Gamma> * hn_ctxt (list_assn Rl'') as cs * hn_invalid Rs s' s) Rs (monadic_nfoldli as c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) s'); RETURN x \<le> c' s'\<rbrakk> \<Longrightarrow> hn_ctxt Rl' a ca * hn_invalid Rs s' s * hn_val bool_rel x x' * \<Gamma> * hn_ctxt (list_assn Rl'') as cs \<or>\<^sub>A hn_ctxt (list_assn Rl) (a # as) (ca # cs) * \<Gamma> * hn_val bool_rel x x' * hn_invalid Rs s' s \<Longrightarrow>\<^sub>t ?\<Gamma>2.17 a as ca cs s s' x x'
 2. \<And>a as ca cs s s' x x'. (\<And>s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) as cs * hn_ctxt Rs s' s) (imp_nfoldli cs c f s) (\<Gamma> * hn_ctxt (list_assn Rl'') as cs * hn_invalid Rs s' s) Rs (monadic_nfoldli as c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) s')) \<Longrightarrow> ?\<Gamma>2.17 a as ca cs s s' x x' \<Longrightarrow>\<^sub>t \<Gamma> * hn_ctxt (list_assn Rl'') (a # as) (ca # cs) * hn_invalid Rs s' s * hn_ctxt (?Rx17 a as ca cs s s') x x'
 3. \<And>v va s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) (v # va) [] * hn_ctxt Rs s' s) (imp_nfoldli [] c f s) (\<Gamma> * hn_ctxt (list_assn Rl'') (v # va) [] * hn_invalid Rs s' s) Rs (monadic_nfoldli (v # va) c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) s')
 4. \<And>v va s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) [] (v # va) * hn_ctxt Rs s' s) (imp_nfoldli (v # va) c f s) (\<Gamma> * hn_ctxt (list_assn Rl'') [] (v # va) * hn_invalid Rs s' s) Rs (monadic_nfoldli [] c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) s')
[PROOF STEP]
apply1 (simp add: assn_assoc)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>a as ca cs s s' x x'. \<lbrakk>\<And>s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) as cs * hn_ctxt Rs s' s) (imp_nfoldli cs c f s) (\<Gamma> * hn_ctxt (list_assn Rl'') as cs * hn_invalid Rs s' s) Rs (monadic_nfoldli as c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) s'); RETURN x \<le> c' s'\<rbrakk> \<Longrightarrow> hn_ctxt Rl' a ca * hn_invalid Rs s' s * hn_val bool_rel x x' * \<Gamma> * hn_ctxt (list_assn Rl'') as cs \<or>\<^sub>A hn_ctxt Rl a ca * hn_ctxt (list_assn Rl) as cs * \<Gamma> * hn_val bool_rel x x' * hn_invalid Rs s' s \<Longrightarrow>\<^sub>t ?\<Gamma>2.17 a as ca cs s s' x x'
 2. \<And>a as ca cs s s' x x'. (\<And>s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) as cs * hn_ctxt Rs s' s) (imp_nfoldli cs c f s) (\<Gamma> * hn_ctxt (list_assn Rl'') as cs * hn_invalid Rs s' s) Rs (monadic_nfoldli as c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) s')) \<Longrightarrow> ?\<Gamma>2.17 a as ca cs s s' x x' \<Longrightarrow>\<^sub>t \<Gamma> * hn_ctxt (list_assn Rl'') (a # as) (ca # cs) * hn_invalid Rs s' s * hn_ctxt (?Rx17 a as ca cs s s') x x'
 3. \<And>v va s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) (v # va) [] * hn_ctxt Rs s' s) (imp_nfoldli [] c f s) (\<Gamma> * hn_ctxt (list_assn Rl'') (v # va) [] * hn_invalid Rs s' s) Rs (monadic_nfoldli (v # va) c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) s')
 4. \<And>v va s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) [] (v # va) * hn_ctxt Rs s' s) (imp_nfoldli (v # va) c f s) (\<Gamma> * hn_ctxt (list_assn Rl'') [] (v # va) * hn_invalid Rs s' s) Rs (monadic_nfoldli [] c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) s')
[PROOF STEP]
applyS (tactic \<open>Sepref_Frame.merge_tac (K (K no_tac)) @{context} 1\<close>)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>a as ca cs s s' x x'. (\<And>s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) as cs * hn_ctxt Rs s' s) (imp_nfoldli cs c f s) (\<Gamma> * hn_ctxt (list_assn Rl'') as cs * hn_invalid Rs s' s) Rs (monadic_nfoldli as c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) s')) \<Longrightarrow> \<Gamma> * hn_val bool_rel x x' * hn_invalid Rs s' s * hn_ctxt (list_assn Rl'') as cs * hn_ctxt Rl'' a ca \<Longrightarrow>\<^sub>t \<Gamma> * hn_ctxt (list_assn Rl'') (a # as) (ca # cs) * hn_invalid Rs s' s * hn_ctxt (?Rx17 a as ca cs s s') x x'
 2. \<And>v va s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) (v # va) [] * hn_ctxt Rs s' s) (imp_nfoldli [] c f s) (\<Gamma> * hn_ctxt (list_assn Rl'') (v # va) [] * hn_invalid Rs s' s) Rs (monadic_nfoldli (v # va) c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) s')
 3. \<And>v va s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) [] (v # va) * hn_ctxt Rs s' s) (imp_nfoldli (v # va) c f s) (\<Gamma> * hn_ctxt (list_assn Rl'') [] (v # va) * hn_invalid Rs s' s) Rs (monadic_nfoldli [] c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) s')
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>a as ca cs s s' x x'. (\<And>s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) as cs * hn_ctxt Rs s' s) (imp_nfoldli cs c f s) (\<Gamma> * hn_ctxt (list_assn Rl'') as cs * hn_invalid Rs s' s) Rs (monadic_nfoldli as c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) s')) \<Longrightarrow> \<Gamma> * hn_val bool_rel x x' * hn_invalid Rs s' s * hn_ctxt (list_assn Rl'') as cs * hn_ctxt Rl'' a ca \<Longrightarrow>\<^sub>t \<Gamma> * (hn_ctxt Rl'' a ca * hn_ctxt (list_assn Rl'') as cs) * hn_invalid Rs s' s * hn_ctxt (?Rx17 a as ca cs s s') x x'
 2. \<And>v va s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) (v # va) [] * hn_ctxt Rs s' s) (imp_nfoldli [] c f s) (\<Gamma> * hn_ctxt (list_assn Rl'') (v # va) [] * hn_invalid Rs s' s) Rs (monadic_nfoldli (v # va) c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) s')
 3. \<And>v va s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) [] (v # va) * hn_ctxt Rs s' s) (imp_nfoldli (v # va) c f s) (\<Gamma> * hn_ctxt (list_assn Rl'') [] (v # va) * hn_invalid Rs s' s) Rs (monadic_nfoldli [] c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) s')
[PROOF STEP]
apply (rule ent_imp_entt)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>a as ca cs s s' x x'. (\<And>s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) as cs * hn_ctxt Rs s' s) (imp_nfoldli cs c f s) (\<Gamma> * hn_ctxt (list_assn Rl'') as cs * hn_invalid Rs s' s) Rs (monadic_nfoldli as c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) s')) \<Longrightarrow> \<Gamma> * hn_val bool_rel x x' * hn_invalid Rs s' s * hn_ctxt (list_assn Rl'') as cs * hn_ctxt Rl'' a ca \<Longrightarrow>\<^sub>A \<Gamma> * (hn_ctxt Rl'' a ca * hn_ctxt (list_assn Rl'') as cs) * hn_invalid Rs s' s * hn_ctxt (?Rx17 a as ca cs s s') x x'
 2. \<And>v va s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) (v # va) [] * hn_ctxt Rs s' s) (imp_nfoldli [] c f s) (\<Gamma> * hn_ctxt (list_assn Rl'') (v # va) [] * hn_invalid Rs s' s) Rs (monadic_nfoldli (v # va) c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) s')
 3. \<And>v va s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) [] (v # va) * hn_ctxt Rs s' s) (imp_nfoldli (v # va) c f s) (\<Gamma> * hn_ctxt (list_assn Rl'') [] (v # va) * hn_invalid Rs s' s) Rs (monadic_nfoldli [] c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) s')
[PROOF STEP]
apply solve_entails
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>v va s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) (v # va) [] * hn_ctxt Rs s' s) (imp_nfoldli [] c f s) (\<Gamma> * hn_ctxt (list_assn Rl'') (v # va) [] * hn_invalid Rs s' s) Rs (monadic_nfoldli (v # va) c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) s')
 2. \<And>v va s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) [] (v # va) * hn_ctxt Rs s' s) (imp_nfoldli (v # va) c f s) (\<Gamma> * hn_ctxt (list_assn Rl'') [] (v # va) * hn_invalid Rs s' s) Rs (monadic_nfoldli [] c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) s')
[PROOF STEP]
apply (rule, sep_auto)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>v va s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) [] (v # va) * hn_ctxt Rs s' s) (imp_nfoldli (v # va) c f s) (\<Gamma> * hn_ctxt (list_assn Rl'') [] (v # va) * hn_invalid Rs s' s) Rs (monadic_nfoldli [] c' (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f' x s)) s')
[PROOF STEP]
apply (rule, sep_auto)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
solved
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done