[STATEMENT]
lemma hm_sink_op_\<alpha>_correct: "hm_sink_op hm i \<le>\<^sub>n SPEC (\<lambda>hm'. heapmap_\<alpha> hm' = heapmap_\<alpha> hm)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hm_sink_op hm i \<le>\<^sub>n SPEC (\<lambda>hm'. heapmap_\<alpha> hm' = heapmap_\<alpha> hm)
[PROOF STEP]
apply (rule leof_add_nofailI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nofail (hm_sink_op hm i) \<Longrightarrow> hm_sink_op hm i \<le>\<^sub>n SPEC (\<lambda>hm'. heapmap_\<alpha> hm' = heapmap_\<alpha> hm)
[PROOF STEP]
apply (drule hm_sink_op_nofail_imp_valid)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hm_valid hm i \<Longrightarrow> hm_sink_op hm i \<le>\<^sub>n SPEC (\<lambda>hm'. heapmap_\<alpha> hm' = heapmap_\<alpha> hm)
[PROOF STEP]
unfolding hm_sink_op_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hm_valid hm i \<Longrightarrow> REC\<^sub>T (\<lambda>D (h, k). ASSERT (0 < k \<and> k \<le> hm_length h) \<bind> (\<lambda>_. let len = hm_length h in if 2 * k \<le> len then let j = 2 * k in hm_prio_of_op h j \<bind> (\<lambda>pj. (if j < len then hm_prio_of_op h (Suc j) \<bind> (\<lambda>psj. if psj < pj then RETURN (j + 1) else RETURN j) else RETURN j) \<bind> (\<lambda>j. hm_prio_of_op h j \<bind> (\<lambda>pj. hm_prio_of_op h k \<bind> (\<lambda>pk. if pj < pk then hm_exch_op h k j \<bind> (\<lambda>h. D (h, j)) else RETURN h)))) else RETURN h)) (hm, i) \<le>\<^sub>n SPEC (\<lambda>hm'. heapmap_\<alpha> hm' = heapmap_\<alpha> hm)
[PROOF STEP]
apply (rule RECT_rule_leof[where
            pre="\<lambda>(hm',i). hm_valid hm' i \<and> heapmap_\<alpha> hm' = heapmap_\<alpha> hm \<and> hm_length hm' = hm_length hm"
            and V = "measure (\<lambda>(hm',i). hm_length hm' - i)"
            ])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. hm_valid hm i \<Longrightarrow> wf (measure (\<lambda>(hm', i). hm_length hm' - i))
 2. hm_valid hm i \<Longrightarrow> case (hm, i) of (hm', i) \<Rightarrow> hm_valid hm' i \<and> heapmap_\<alpha> hm' = heapmap_\<alpha> hm \<and> hm_length hm' = hm_length hm
 3. \<And>f x. \<lbrakk>hm_valid hm i; \<And>x'. \<lbrakk>case x' of (hm', i) \<Rightarrow> hm_valid hm' i \<and> heapmap_\<alpha> hm' = heapmap_\<alpha> hm \<and> hm_length hm' = hm_length hm; (x', x) \<in> measure (\<lambda>(hm', i). hm_length hm' - i)\<rbrakk> \<Longrightarrow> f x' \<le>\<^sub>n SPEC (\<lambda>hm'. heapmap_\<alpha> hm' = heapmap_\<alpha> hm); case x of (hm', i) \<Rightarrow> hm_valid hm' i \<and> heapmap_\<alpha> hm' = heapmap_\<alpha> hm \<and> hm_length hm' = hm_length hm; REC\<^sub>T (\<lambda>D a. case a of (h, k) \<Rightarrow> ASSERT (0 < k \<and> k \<le> hm_length h) \<bind> (\<lambda>_. let len = hm_length h in if 2 * k \<le> len then let j = 2 * k in hm_prio_of_op h j \<bind> (\<lambda>pj. (if j < len then hm_prio_of_op h (Suc j) \<bind> (\<lambda>psj. if psj < pj then RETURN (j + 1) else RETURN j) else RETURN j) \<bind> (\<lambda>j. hm_prio_of_op h j \<bind> (\<lambda>pj. hm_prio_of_op h k \<bind> (\<lambda>pk. if pj < pk then hm_exch_op h k j \<bind> (\<lambda>h. D (h, j)) else RETURN h)))) else RETURN h)) = f\<rbrakk> \<Longrightarrow> (case x of (h, k) \<Rightarrow> ASSERT (0 < k \<and> k \<le> hm_length h) \<bind> (\<lambda>_. let len = hm_length h in if 2 * k \<le> len then let j = 2 * k in hm_prio_of_op h j \<bind> (\<lambda>pj. (if j < len then hm_prio_of_op h (Suc j) \<bind> (\<lambda>psj. if psj < pj then RETURN (j + 1) else RETURN j) else RETURN j) \<bind> (\<lambda>j. hm_prio_of_op h j \<bind> (\<lambda>pj. hm_prio_of_op h k \<bind> (\<lambda>pk. if pj < pk then hm_exch_op h k j \<bind> (\<lambda>h. f (h, j)) else RETURN h)))) else RETURN h)) \<le>\<^sub>n SPEC (\<lambda>hm'. heapmap_\<alpha> hm' = heapmap_\<alpha> hm)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. hm_valid hm i \<Longrightarrow> case (hm, i) of (hm', i) \<Rightarrow> hm_valid hm' i \<and> heapmap_\<alpha> hm' = heapmap_\<alpha> hm \<and> hm_length hm' = hm_length hm
 2. \<And>f x. \<lbrakk>hm_valid hm i; \<And>x'. \<lbrakk>case x' of (hm', i) \<Rightarrow> hm_valid hm' i \<and> heapmap_\<alpha> hm' = heapmap_\<alpha> hm \<and> hm_length hm' = hm_length hm; (x', x) \<in> measure (\<lambda>(hm', i). hm_length hm' - i)\<rbrakk> \<Longrightarrow> f x' \<le>\<^sub>n SPEC (\<lambda>hm'. heapmap_\<alpha> hm' = heapmap_\<alpha> hm); case x of (hm', i) \<Rightarrow> hm_valid hm' i \<and> heapmap_\<alpha> hm' = heapmap_\<alpha> hm \<and> hm_length hm' = hm_length hm; REC\<^sub>T (\<lambda>D a. case a of (h, k) \<Rightarrow> ASSERT (0 < k \<and> k \<le> hm_length h) \<bind> (\<lambda>_. let len = hm_length h in if 2 * k \<le> len then let j = 2 * k in hm_prio_of_op h j \<bind> (\<lambda>pj. (if j < len then hm_prio_of_op h (Suc j) \<bind> (\<lambda>psj. if psj < pj then RETURN (j + 1) else RETURN j) else RETURN j) \<bind> (\<lambda>j. hm_prio_of_op h j \<bind> (\<lambda>pj. hm_prio_of_op h k \<bind> (\<lambda>pk. if pj < pk then hm_exch_op h k j \<bind> (\<lambda>h. D (h, j)) else RETURN h)))) else RETURN h)) = f\<rbrakk> \<Longrightarrow> (case x of (h, k) \<Rightarrow> ASSERT (0 < k \<and> k \<le> hm_length h) \<bind> (\<lambda>_. let len = hm_length h in if 2 * k \<le> len then let j = 2 * k in hm_prio_of_op h j \<bind> (\<lambda>pj. (if j < len then hm_prio_of_op h (Suc j) \<bind> (\<lambda>psj. if psj < pj then RETURN (j + 1) else RETURN j) else RETURN j) \<bind> (\<lambda>j. hm_prio_of_op h j \<bind> (\<lambda>pj. hm_prio_of_op h k \<bind> (\<lambda>pk. if pj < pk then hm_exch_op h k j \<bind> (\<lambda>h. f (h, j)) else RETURN h)))) else RETURN h)) \<le>\<^sub>n SPEC (\<lambda>hm'. heapmap_\<alpha> hm' = heapmap_\<alpha> hm)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>f x. \<lbrakk>hm_valid hm i; \<And>x'. \<lbrakk>case x' of (hm', i) \<Rightarrow> hm_valid hm' i \<and> heapmap_\<alpha> hm' = heapmap_\<alpha> hm \<and> hm_length hm' = hm_length hm; (x', x) \<in> measure (\<lambda>(hm', i). hm_length hm' - i)\<rbrakk> \<Longrightarrow> f x' \<le>\<^sub>n SPEC (\<lambda>hm'. heapmap_\<alpha> hm' = heapmap_\<alpha> hm); case x of (hm', i) \<Rightarrow> hm_valid hm' i \<and> heapmap_\<alpha> hm' = heapmap_\<alpha> hm \<and> hm_length hm' = hm_length hm; REC\<^sub>T (\<lambda>D a. case a of (h, k) \<Rightarrow> ASSERT (0 < k \<and> k \<le> hm_length h) \<bind> (\<lambda>_. let len = hm_length h in if 2 * k \<le> len then let j = 2 * k in hm_prio_of_op h j \<bind> (\<lambda>pj. (if j < len then hm_prio_of_op h (Suc j) \<bind> (\<lambda>psj. if psj < pj then RETURN (j + 1) else RETURN j) else RETURN j) \<bind> (\<lambda>j. hm_prio_of_op h j \<bind> (\<lambda>pj. hm_prio_of_op h k \<bind> (\<lambda>pk. if pj < pk then hm_exch_op h k j \<bind> (\<lambda>h. D (h, j)) else RETURN h)))) else RETURN h)) = f\<rbrakk> \<Longrightarrow> (case x of (h, k) \<Rightarrow> ASSERT (0 < k \<and> k \<le> hm_length h) \<bind> (\<lambda>_. let len = hm_length h in if 2 * k \<le> len then let j = 2 * k in hm_prio_of_op h j \<bind> (\<lambda>pj. (if j < len then hm_prio_of_op h (Suc j) \<bind> (\<lambda>psj. if psj < pj then RETURN (j + 1) else RETURN j) else RETURN j) \<bind> (\<lambda>j. hm_prio_of_op h j \<bind> (\<lambda>pj. hm_prio_of_op h k \<bind> (\<lambda>pk. if pj < pk then hm_exch_op h k j \<bind> (\<lambda>h. f (h, j)) else RETURN h)))) else RETURN h)) \<le>\<^sub>n SPEC (\<lambda>hm'. heapmap_\<alpha> hm' = heapmap_\<alpha> hm)
[PROOF STEP]
unfolding hm_prio_of_op_def hm_val_of_op_def hm_exch_op_def
        hm_key_of_op_def hm_the_lookup_op_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>f x. \<lbrakk>hm_valid hm i; \<And>x'. \<lbrakk>case x' of (hm', i) \<Rightarrow> hm_valid hm' i \<and> heapmap_\<alpha> hm' = heapmap_\<alpha> hm \<and> hm_length hm' = hm_length hm; (x', x) \<in> measure (\<lambda>(hm', i). hm_length hm' - i)\<rbrakk> \<Longrightarrow> f x' \<le>\<^sub>n SPEC (\<lambda>hm'. heapmap_\<alpha> hm' = heapmap_\<alpha> hm); case x of (hm', i) \<Rightarrow> hm_valid hm' i \<and> heapmap_\<alpha> hm' = heapmap_\<alpha> hm \<and> hm_length hm' = hm_length hm; REC\<^sub>T (\<lambda>D a. case a of (h, k) \<Rightarrow> ASSERT (0 < k \<and> k \<le> hm_length h) \<bind> (\<lambda>_. let len = hm_length h in if 2 * k \<le> len then let j = 2 * k in (case h of (pq, m) \<Rightarrow> \<lambda>i. ASSERT (0 < i) \<bind> (\<lambda>_. mop_list_get pq (i - 1))) j \<bind> (\<lambda>k. ASSERT (heapmap_\<alpha> h k \<noteq> None \<and> hmr_invar h) \<bind> (\<lambda>_. RETURN (the (heapmap_\<alpha> h k))) \<bind> RETURN) \<bind> (\<lambda>v. RETURN (prio v)) \<bind> (\<lambda>pj. (if j < len then (case h of (pq, m) \<Rightarrow> \<lambda>i. ASSERT (0 < i) \<bind> (\<lambda>_. mop_list_get pq (i - 1))) (Suc j) \<bind> (\<lambda>k. ASSERT (heapmap_\<alpha> h k \<noteq> None \<and> hmr_invar h) \<bind> (\<lambda>_. RETURN (the (heapmap_\<alpha> h k))) \<bind> RETURN) \<bind> (\<lambda>v. RETURN (prio v)) \<bind> (\<lambda>psj. if psj < pj then RETURN (j + 1) else RETURN j) else RETURN j) \<bind> (\<lambda>j. (case h of (pq, m) \<Rightarrow> \<lambda>i. ASSERT (0 < i) \<bind> (\<lambda>_. mop_list_get pq (i - 1))) j \<bind> (\<lambda>k. ASSERT (heapmap_\<alpha> h k \<noteq> None \<and> hmr_invar h) \<bind> (\<lambda>_. RETURN (the (heapmap_\<alpha> h k))) \<bind> RETURN) \<bind> (\<lambda>v. RETURN (prio v)) \<bind> (\<lambda>pj. (case h of (pq, m) \<Rightarrow> \<lambda>i. ASSERT (0 < i) \<bind> (\<lambda>_. mop_list_get pq (i - 1))) k \<bind> (\<lambda>k. ASSERT (heapmap_\<alpha> h k \<noteq> None \<and> hmr_invar h) \<bind> (\<lambda>_. RETURN (the (heapmap_\<alpha> h k))) \<bind> RETURN) \<bind> (\<lambda>v. RETURN (prio v)) \<bind> (\<lambda>pk. if pj < pk then (case h of (pq, m) \<Rightarrow> \<lambda>i j. ASSERT (hm_valid (pq, m) i) \<bind> (\<lambda>_. ASSERT (hm_valid (pq, m) j) \<bind> (\<lambda>_. ASSERT (hmr_invar (pq, m)) \<bind> (\<lambda>_. mop_list_swap pq (i - 1) (j - 1) \<bind> (\<lambda>pq. RETURN (pq, m)))))) k j \<bind> (\<lambda>h. D (h, j)) else RETURN h)))) else RETURN h)) = f\<rbrakk> \<Longrightarrow> (case x of (h, k) \<Rightarrow> ASSERT (0 < k \<and> k \<le> hm_length h) \<bind> (\<lambda>_. let len = hm_length h in if 2 * k \<le> len then let j = 2 * k in (case h of (pq, m) \<Rightarrow> \<lambda>i. ASSERT (0 < i) \<bind> (\<lambda>_. mop_list_get pq (i - 1))) j \<bind> (\<lambda>k. ASSERT (heapmap_\<alpha> h k \<noteq> None \<and> hmr_invar h) \<bind> (\<lambda>_. RETURN (the (heapmap_\<alpha> h k))) \<bind> RETURN) \<bind> (\<lambda>v. RETURN (prio v)) \<bind> (\<lambda>pj. (if j < len then (case h of (pq, m) \<Rightarrow> \<lambda>i. ASSERT (0 < i) \<bind> (\<lambda>_. mop_list_get pq (i - 1))) (Suc j) \<bind> (\<lambda>k. ASSERT (heapmap_\<alpha> h k \<noteq> None \<and> hmr_invar h) \<bind> (\<lambda>_. RETURN (the (heapmap_\<alpha> h k))) \<bind> RETURN) \<bind> (\<lambda>v. RETURN (prio v)) \<bind> (\<lambda>psj. if psj < pj then RETURN (j + 1) else RETURN j) else RETURN j) \<bind> (\<lambda>j. (case h of (pq, m) \<Rightarrow> \<lambda>i. ASSERT (0 < i) \<bind> (\<lambda>_. mop_list_get pq (i - 1))) j \<bind> (\<lambda>k. ASSERT (heapmap_\<alpha> h k \<noteq> None \<and> hmr_invar h) \<bind> (\<lambda>_. RETURN (the (heapmap_\<alpha> h k))) \<bind> RETURN) \<bind> (\<lambda>v. RETURN (prio v)) \<bind> (\<lambda>pj. (case h of (pq, m) \<Rightarrow> \<lambda>i. ASSERT (0 < i) \<bind> (\<lambda>_. mop_list_get pq (i - 1))) k \<bind> (\<lambda>k. ASSERT (heapmap_\<alpha> h k \<noteq> None \<and> hmr_invar h) \<bind> (\<lambda>_. RETURN (the (heapmap_\<alpha> h k))) \<bind> RETURN) \<bind> (\<lambda>v. RETURN (prio v)) \<bind> (\<lambda>pk. if pj < pk then (case h of (pq, m) \<Rightarrow> \<lambda>i j. ASSERT (hm_valid (pq, m) i) \<bind> (\<lambda>_. ASSERT (hm_valid (pq, m) j) \<bind> (\<lambda>_. ASSERT (hmr_invar (pq, m)) \<bind> (\<lambda>_. mop_list_swap pq (i - 1) (j - 1) \<bind> (\<lambda>pq. RETURN (pq, m)))))) k j \<bind> (\<lambda>h. f (h, j)) else RETURN h)))) else RETURN h)) \<le>\<^sub>n SPEC (\<lambda>hm'. heapmap_\<alpha> hm' = heapmap_\<alpha> hm)
[PROOF STEP]
apply (refine_vcg)
[PROOF STATE]
proof (prove)
goal (7 subgoals):
 1. \<And>f x x1 x1a x2 x1b x2a x2b. \<lbrakk>hm_valid hm i; \<And>x'. \<lbrakk>case x' of (hm', i) \<Rightarrow> hm_valid hm' i \<and> heapmap_\<alpha> hm' = heapmap_\<alpha> hm \<and> hm_length hm' = hm_length hm; (x', x) \<in> measure (\<lambda>(hm', i). hm_length hm' - i)\<rbrakk> \<Longrightarrow> f x' \<le>\<^sub>n SPEC (\<lambda>hm'. heapmap_\<alpha> hm' = heapmap_\<alpha> hm); case x of (hm', i) \<Rightarrow> hm_valid hm' i \<and> heapmap_\<alpha> hm' = heapmap_\<alpha> hm \<and> hm_length hm' = hm_length hm; REC\<^sub>T (\<lambda>D a. case a of (h, k) \<Rightarrow> ASSERT (0 < k \<and> k \<le> hm_length h) \<bind> (\<lambda>_. let len = hm_length h in if 2 * k \<le> len then let j = 2 * k in (case h of (pq, m) \<Rightarrow> \<lambda>i. ASSERT (0 < i) \<bind> (\<lambda>_. mop_list_get pq (i - 1))) j \<bind> (\<lambda>k. ASSERT (heapmap_\<alpha> h k \<noteq> None \<and> hmr_invar h) \<bind> (\<lambda>_. RETURN (the (heapmap_\<alpha> h k))) \<bind> RETURN) \<bind> (\<lambda>v. RETURN (prio v)) \<bind> (\<lambda>pj. (if j < len then (case h of (pq, m) \<Rightarrow> \<lambda>i. ASSERT (0 < i) \<bind> (\<lambda>_. mop_list_get pq (i - 1))) (Suc j) \<bind> (\<lambda>k. ASSERT (heapmap_\<alpha> h k \<noteq> None \<and> hmr_invar h) \<bind> (\<lambda>_. RETURN (the (heapmap_\<alpha> h k))) \<bind> RETURN) \<bind> (\<lambda>v. RETURN (prio v)) \<bind> (\<lambda>psj. if psj < pj then RETURN (j + 1) else RETURN j) else RETURN j) \<bind> (\<lambda>j. (case h of (pq, m) \<Rightarrow> \<lambda>i. ASSERT (0 < i) \<bind> (\<lambda>_. mop_list_get pq (i - 1))) j \<bind> (\<lambda>k. ASSERT (heapmap_\<alpha> h k \<noteq> None \<and> hmr_invar h) \<bind> (\<lambda>_. RETURN (the (heapmap_\<alpha> h k))) \<bind> RETURN) \<bind> (\<lambda>v. RETURN (prio v)) \<bind> (\<lambda>pj. (case h of (pq, m) \<Rightarrow> \<lambda>i. ASSERT (0 < i) \<bind> (\<lambda>_. mop_list_get pq (i - 1))) k \<bind> (\<lambda>k. ASSERT (heapmap_\<alpha> h k \<noteq> None \<and> hmr_invar h) \<bind> (\<lambda>_. RETURN (the (heapmap_\<alpha> h k))) \<bind> RETURN) \<bind> (\<lambda>v. RETURN (prio v)) \<bind> (\<lambda>pk. if pj < pk then (case h of (pq, m) \<Rightarrow> \<lambda>i j. ASSERT (hm_valid (pq, m) i) \<bind> (\<lambda>_. ASSERT (hm_valid (pq, m) j) \<bind> (\<lambda>_. ASSERT (hmr_invar (pq, m)) \<bind> (\<lambda>_. mop_list_swap pq (i - 1) (j - 1) \<bind> (\<lambda>pq. RETURN (pq, m)))))) k j \<bind> (\<lambda>h. D (h, j)) else RETURN h)))) else RETURN h)) = f; x1 = (x1a, x2); x1 = (x1b, x2a); x = (x1, x2b); 0 < x2b \<and> x2b \<le> hm_length x1; 2 * x2b \<le> hm_length x1; 0 < 2 * x2b; 2 * x2b - 1 < length x1b; heapmap_\<alpha> x1 (x1b ! (2 * x2b - 1)) \<noteq> None \<and> hmr_invar x1; 2 * x2b < hm_length x1; 0 < Suc (2 * x2b); Suc (2 * x2b) - 1 < length x1b; heapmap_\<alpha> x1 (x1b ! (Suc (2 * x2b) - 1)) \<noteq> None \<and> hmr_invar x1; prio (the (heapmap_\<alpha> x1 (x1b ! (Suc (2 * x2b) - 1)))) < prio (the (heapmap_\<alpha> x1 (x1b ! (2 * x2b - 1)))); 0 < 2 * x2b + 1; 2 * x2b + 1 - 1 < length x1b; heapmap_\<alpha> x1 (x1b ! (2 * x2b + 1 - 1)) \<noteq> None \<and> hmr_invar x1; 0 < x2b; x2b - 1 < length x1b; heapmap_\<alpha> x1 (x1b ! (x2b - 1)) \<noteq> None \<and> hmr_invar x1; prio (the (heapmap_\<alpha> x1 (x1b ! (2 * x2b + 1 - 1)))) < prio (the (heapmap_\<alpha> x1 (x1b ! (x2b - 1)))); hm_valid (x1a, x2) x2b; hm_valid (x1a, x2) (2 * x2b + 1); hmr_invar (x1a, x2); x2b - 1 < length x1a \<and> 2 * x2b + 1 - 1 < length x1a\<rbrakk> \<Longrightarrow> f ((swap x1a (x2b - 1) (2 * x2b + 1 - 1), x2), 2 * x2b + 1) \<le>\<^sub>n SPEC (\<lambda>hm'. heapmap_\<alpha> hm' = heapmap_\<alpha> hm)
 2. \<And>f x x1 x1a x2 x1b x2a x2b. \<lbrakk>hm_valid hm i; \<And>x'. \<lbrakk>case x' of (hm', i) \<Rightarrow> hm_valid hm' i \<and> heapmap_\<alpha> hm' = heapmap_\<alpha> hm \<and> hm_length hm' = hm_length hm; (x', x) \<in> measure (\<lambda>(hm', i). hm_length hm' - i)\<rbrakk> \<Longrightarrow> f x' \<le>\<^sub>n SPEC (\<lambda>hm'. heapmap_\<alpha> hm' = heapmap_\<alpha> hm); case x of (hm', i) \<Rightarrow> hm_valid hm' i \<and> heapmap_\<alpha> hm' = heapmap_\<alpha> hm \<and> hm_length hm' = hm_length hm; REC\<^sub>T (\<lambda>D a. case a of (h, k) \<Rightarrow> ASSERT (0 < k \<and> k \<le> hm_length h) \<bind> (\<lambda>_. let len = hm_length h in if 2 * k \<le> len then let j = 2 * k in (case h of (pq, m) \<Rightarrow> \<lambda>i. ASSERT (0 < i) \<bind> (\<lambda>_. mop_list_get pq (i - 1))) j \<bind> (\<lambda>k. ASSERT (heapmap_\<alpha> h k \<noteq> None \<and> hmr_invar h) \<bind> (\<lambda>_. RETURN (the (heapmap_\<alpha> h k))) \<bind> RETURN) \<bind> (\<lambda>v. RETURN (prio v)) \<bind> (\<lambda>pj. (if j < len then (case h of (pq, m) \<Rightarrow> \<lambda>i. ASSERT (0 < i) \<bind> (\<lambda>_. mop_list_get pq (i - 1))) (Suc j) \<bind> (\<lambda>k. ASSERT (heapmap_\<alpha> h k \<noteq> None \<and> hmr_invar h) \<bind> (\<lambda>_. RETURN (the (heapmap_\<alpha> h k))) \<bind> RETURN) \<bind> (\<lambda>v. RETURN (prio v)) \<bind> (\<lambda>psj. if psj < pj then RETURN (j + 1) else RETURN j) else RETURN j) \<bind> (\<lambda>j. (case h of (pq, m) \<Rightarrow> \<lambda>i. ASSERT (0 < i) \<bind> (\<lambda>_. mop_list_get pq (i - 1))) j \<bind> (\<lambda>k. ASSERT (heapmap_\<alpha> h k \<noteq> None \<and> hmr_invar h) \<bind> (\<lambda>_. RETURN (the (heapmap_\<alpha> h k))) \<bind> RETURN) \<bind> (\<lambda>v. RETURN (prio v)) \<bind> (\<lambda>pj. (case h of (pq, m) \<Rightarrow> \<lambda>i. ASSERT (0 < i) \<bind> (\<lambda>_. mop_list_get pq (i - 1))) k \<bind> (\<lambda>k. ASSERT (heapmap_\<alpha> h k \<noteq> None \<and> hmr_invar h) \<bind> (\<lambda>_. RETURN (the (heapmap_\<alpha> h k))) \<bind> RETURN) \<bind> (\<lambda>v. RETURN (prio v)) \<bind> (\<lambda>pk. if pj < pk then (case h of (pq, m) \<Rightarrow> \<lambda>i j. ASSERT (hm_valid (pq, m) i) \<bind> (\<lambda>_. ASSERT (hm_valid (pq, m) j) \<bind> (\<lambda>_. ASSERT (hmr_invar (pq, m)) \<bind> (\<lambda>_. mop_list_swap pq (i - 1) (j - 1) \<bind> (\<lambda>pq. RETURN (pq, m)))))) k j \<bind> (\<lambda>h. D (h, j)) else RETURN h)))) else RETURN h)) = f; x1 = (x1a, x2); x1 = (x1b, x2a); x = (x1, x2b); 0 < x2b \<and> x2b \<le> hm_length x1; 2 * x2b \<le> hm_length x1; 0 < 2 * x2b; 2 * x2b - 1 < length x1b; heapmap_\<alpha> x1 (x1b ! (2 * x2b - 1)) \<noteq> None \<and> hmr_invar x1; 2 * x2b < hm_length x1; 0 < Suc (2 * x2b); Suc (2 * x2b) - 1 < length x1b; heapmap_\<alpha> x1 (x1b ! (Suc (2 * x2b) - 1)) \<noteq> None \<and> hmr_invar x1; prio (the (heapmap_\<alpha> x1 (x1b ! (Suc (2 * x2b) - 1)))) < prio (the (heapmap_\<alpha> x1 (x1b ! (2 * x2b - 1)))); 0 < 2 * x2b + 1; 2 * x2b + 1 - 1 < length x1b; heapmap_\<alpha> x1 (x1b ! (2 * x2b + 1 - 1)) \<noteq> None \<and> hmr_invar x1; 0 < x2b; x2b - 1 < length x1b; heapmap_\<alpha> x1 (x1b ! (x2b - 1)) \<noteq> None \<and> hmr_invar x1; \<not> prio (the (heapmap_\<alpha> x1 (x1b ! (2 * x2b + 1 - 1)))) < prio (the (heapmap_\<alpha> x1 (x1b ! (x2b - 1))))\<rbrakk> \<Longrightarrow> heapmap_\<alpha> x1 = heapmap_\<alpha> hm
 3. \<And>f x x1 x1a x2 x1b x2a x2b. \<lbrakk>hm_valid hm i; \<And>x'. \<lbrakk>case x' of (hm', i) \<Rightarrow> hm_valid hm' i \<and> heapmap_\<alpha> hm' = heapmap_\<alpha> hm \<and> hm_length hm' = hm_length hm; (x', x) \<in> measure (\<lambda>(hm', i). hm_length hm' - i)\<rbrakk> \<Longrightarrow> f x' \<le>\<^sub>n SPEC (\<lambda>hm'. heapmap_\<alpha> hm' = heapmap_\<alpha> hm); case x of (hm', i) \<Rightarrow> hm_valid hm' i \<and> heapmap_\<alpha> hm' = heapmap_\<alpha> hm \<and> hm_length hm' = hm_length hm; REC\<^sub>T (\<lambda>D a. case a of (h, k) \<Rightarrow> ASSERT (0 < k \<and> k \<le> hm_length h) \<bind> (\<lambda>_. let len = hm_length h in if 2 * k \<le> len then let j = 2 * k in (case h of (pq, m) \<Rightarrow> \<lambda>i. ASSERT (0 < i) \<bind> (\<lambda>_. mop_list_get pq (i - 1))) j \<bind> (\<lambda>k. ASSERT (heapmap_\<alpha> h k \<noteq> None \<and> hmr_invar h) \<bind> (\<lambda>_. RETURN (the (heapmap_\<alpha> h k))) \<bind> RETURN) \<bind> (\<lambda>v. RETURN (prio v)) \<bind> (\<lambda>pj. (if j < len then (case h of (pq, m) \<Rightarrow> \<lambda>i. ASSERT (0 < i) \<bind> (\<lambda>_. mop_list_get pq (i - 1))) (Suc j) \<bind> (\<lambda>k. ASSERT (heapmap_\<alpha> h k \<noteq> None \<and> hmr_invar h) \<bind> (\<lambda>_. RETURN (the (heapmap_\<alpha> h k))) \<bind> RETURN) \<bind> (\<lambda>v. RETURN (prio v)) \<bind> (\<lambda>psj. if psj < pj then RETURN (j + 1) else RETURN j) else RETURN j) \<bind> (\<lambda>j. (case h of (pq, m) \<Rightarrow> \<lambda>i. ASSERT (0 < i) \<bind> (\<lambda>_. mop_list_get pq (i - 1))) j \<bind> (\<lambda>k. ASSERT (heapmap_\<alpha> h k \<noteq> None \<and> hmr_invar h) \<bind> (\<lambda>_. RETURN (the (heapmap_\<alpha> h k))) \<bind> RETURN) \<bind> (\<lambda>v. RETURN (prio v)) \<bind> (\<lambda>pj. (case h of (pq, m) \<Rightarrow> \<lambda>i. ASSERT (0 < i) \<bind> (\<lambda>_. mop_list_get pq (i - 1))) k \<bind> (\<lambda>k. ASSERT (heapmap_\<alpha> h k \<noteq> None \<and> hmr_invar h) \<bind> (\<lambda>_. RETURN (the (heapmap_\<alpha> h k))) \<bind> RETURN) \<bind> (\<lambda>v. RETURN (prio v)) \<bind> (\<lambda>pk. if pj < pk then (case h of (pq, m) \<Rightarrow> \<lambda>i j. ASSERT (hm_valid (pq, m) i) \<bind> (\<lambda>_. ASSERT (hm_valid (pq, m) j) \<bind> (\<lambda>_. ASSERT (hmr_invar (pq, m)) \<bind> (\<lambda>_. mop_list_swap pq (i - 1) (j - 1) \<bind> (\<lambda>pq. RETURN (pq, m)))))) k j \<bind> (\<lambda>h. D (h, j)) else RETURN h)))) else RETURN h)) = f; x1 = (x1a, x2); x1 = (x1b, x2a); x = (x1, x2b); 0 < x2b \<and> x2b \<le> hm_length x1; 2 * x2b \<le> hm_length x1; 0 < 2 * x2b; 2 * x2b - 1 < length x1b; heapmap_\<alpha> x1 (x1b ! (2 * x2b - 1)) \<noteq> None \<and> hmr_invar x1; 2 * x2b < hm_length x1; 0 < Suc (2 * x2b); Suc (2 * x2b) - 1 < length x1b; heapmap_\<alpha> x1 (x1b ! (Suc (2 * x2b) - 1)) \<noteq> None \<and> hmr_invar x1; \<not> prio (the (heapmap_\<alpha> x1 (x1b ! (Suc (2 * x2b) - 1)))) < prio (the (heapmap_\<alpha> x1 (x1b ! (2 * x2b - 1)))); 0 < 2 * x2b; 2 * x2b - 1 < length x1b; heapmap_\<alpha> x1 (x1b ! (2 * x2b - 1)) \<noteq> None \<and> hmr_invar x1; 0 < x2b; x2b - 1 < length x1b; heapmap_\<alpha> x1 (x1b ! (x2b - 1)) \<noteq> None \<and> hmr_invar x1; prio (the (heapmap_\<alpha> x1 (x1b ! (2 * x2b - 1)))) < prio (the (heapmap_\<alpha> x1 (x1b ! (x2b - 1)))); hm_valid (x1a, x2) x2b; hm_valid (x1a, x2) (2 * x2b); hmr_invar (x1a, x2); x2b - 1 < length x1a \<and> 2 * x2b - 1 < length x1a\<rbrakk> \<Longrightarrow> f ((swap x1a (x2b - 1) (2 * x2b - 1), x2), 2 * x2b) \<le>\<^sub>n SPEC (\<lambda>hm'. heapmap_\<alpha> hm' = heapmap_\<alpha> hm)
 4. \<And>f x x1 x1a x2 x1b x2a x2b. \<lbrakk>hm_valid hm i; \<And>x'. \<lbrakk>case x' of (hm', i) \<Rightarrow> hm_valid hm' i \<and> heapmap_\<alpha> hm' = heapmap_\<alpha> hm \<and> hm_length hm' = hm_length hm; (x', x) \<in> measure (\<lambda>(hm', i). hm_length hm' - i)\<rbrakk> \<Longrightarrow> f x' \<le>\<^sub>n SPEC (\<lambda>hm'. heapmap_\<alpha> hm' = heapmap_\<alpha> hm); case x of (hm', i) \<Rightarrow> hm_valid hm' i \<and> heapmap_\<alpha> hm' = heapmap_\<alpha> hm \<and> hm_length hm' = hm_length hm; REC\<^sub>T (\<lambda>D a. case a of (h, k) \<Rightarrow> ASSERT (0 < k \<and> k \<le> hm_length h) \<bind> (\<lambda>_. let len = hm_length h in if 2 * k \<le> len then let j = 2 * k in (case h of (pq, m) \<Rightarrow> \<lambda>i. ASSERT (0 < i) \<bind> (\<lambda>_. mop_list_get pq (i - 1))) j \<bind> (\<lambda>k. ASSERT (heapmap_\<alpha> h k \<noteq> None \<and> hmr_invar h) \<bind> (\<lambda>_. RETURN (the (heapmap_\<alpha> h k))) \<bind> RETURN) \<bind> (\<lambda>v. RETURN (prio v)) \<bind> (\<lambda>pj. (if j < len then (case h of (pq, m) \<Rightarrow> \<lambda>i. ASSERT (0 < i) \<bind> (\<lambda>_. mop_list_get pq (i - 1))) (Suc j) \<bind> (\<lambda>k. ASSERT (heapmap_\<alpha> h k \<noteq> None \<and> hmr_invar h) \<bind> (\<lambda>_. RETURN (the (heapmap_\<alpha> h k))) \<bind> RETURN) \<bind> (\<lambda>v. RETURN (prio v)) \<bind> (\<lambda>psj. if psj < pj then RETURN (j + 1) else RETURN j) else RETURN j) \<bind> (\<lambda>j. (case h of (pq, m) \<Rightarrow> \<lambda>i. ASSERT (0 < i) \<bind> (\<lambda>_. mop_list_get pq (i - 1))) j \<bind> (\<lambda>k. ASSERT (heapmap_\<alpha> h k \<noteq> None \<and> hmr_invar h) \<bind> (\<lambda>_. RETURN (the (heapmap_\<alpha> h k))) \<bind> RETURN) \<bind> (\<lambda>v. RETURN (prio v)) \<bind> (\<lambda>pj. (case h of (pq, m) \<Rightarrow> \<lambda>i. ASSERT (0 < i) \<bind> (\<lambda>_. mop_list_get pq (i - 1))) k \<bind> (\<lambda>k. ASSERT (heapmap_\<alpha> h k \<noteq> None \<and> hmr_invar h) \<bind> (\<lambda>_. RETURN (the (heapmap_\<alpha> h k))) \<bind> RETURN) \<bind> (\<lambda>v. RETURN (prio v)) \<bind> (\<lambda>pk. if pj < pk then (case h of (pq, m) \<Rightarrow> \<lambda>i j. ASSERT (hm_valid (pq, m) i) \<bind> (\<lambda>_. ASSERT (hm_valid (pq, m) j) \<bind> (\<lambda>_. ASSERT (hmr_invar (pq, m)) \<bind> (\<lambda>_. mop_list_swap pq (i - 1) (j - 1) \<bind> (\<lambda>pq. RETURN (pq, m)))))) k j \<bind> (\<lambda>h. D (h, j)) else RETURN h)))) else RETURN h)) = f; x1 = (x1a, x2); x1 = (x1b, x2a); x = (x1, x2b); 0 < x2b \<and> x2b \<le> hm_length x1; 2 * x2b \<le> hm_length x1; 0 < 2 * x2b; 2 * x2b - 1 < length x1b; heapmap_\<alpha> x1 (x1b ! (2 * x2b - 1)) \<noteq> None \<and> hmr_invar x1; 2 * x2b < hm_length x1; 0 < Suc (2 * x2b); Suc (2 * x2b) - 1 < length x1b; heapmap_\<alpha> x1 (x1b ! (Suc (2 * x2b) - 1)) \<noteq> None \<and> hmr_invar x1; \<not> prio (the (heapmap_\<alpha> x1 (x1b ! (Suc (2 * x2b) - 1)))) < prio (the (heapmap_\<alpha> x1 (x1b ! (2 * x2b - 1)))); 0 < 2 * x2b; 2 * x2b - 1 < length x1b; heapmap_\<alpha> x1 (x1b ! (2 * x2b - 1)) \<noteq> None \<and> hmr_invar x1; 0 < x2b; x2b - 1 < length x1b; heapmap_\<alpha> x1 (x1b ! (x2b - 1)) \<noteq> None \<and> hmr_invar x1; \<not> prio (the (heapmap_\<alpha> x1 (x1b ! (2 * x2b - 1)))) < prio (the (heapmap_\<alpha> x1 (x1b ! (x2b - 1))))\<rbrakk> \<Longrightarrow> heapmap_\<alpha> x1 = heapmap_\<alpha> hm
 5. \<And>f x x1 x1a x2 x1b x2a x2b. \<lbrakk>hm_valid hm i; \<And>x'. \<lbrakk>case x' of (hm', i) \<Rightarrow> hm_valid hm' i \<and> heapmap_\<alpha> hm' = heapmap_\<alpha> hm \<and> hm_length hm' = hm_length hm; (x', x) \<in> measure (\<lambda>(hm', i). hm_length hm' - i)\<rbrakk> \<Longrightarrow> f x' \<le>\<^sub>n SPEC (\<lambda>hm'. heapmap_\<alpha> hm' = heapmap_\<alpha> hm); case x of (hm', i) \<Rightarrow> hm_valid hm' i \<and> heapmap_\<alpha> hm' = heapmap_\<alpha> hm \<and> hm_length hm' = hm_length hm; REC\<^sub>T (\<lambda>D a. case a of (h, k) \<Rightarrow> ASSERT (0 < k \<and> k \<le> hm_length h) \<bind> (\<lambda>_. let len = hm_length h in if 2 * k \<le> len then let j = 2 * k in (case h of (pq, m) \<Rightarrow> \<lambda>i. ASSERT (0 < i) \<bind> (\<lambda>_. mop_list_get pq (i - 1))) j \<bind> (\<lambda>k. ASSERT (heapmap_\<alpha> h k \<noteq> None \<and> hmr_invar h) \<bind> (\<lambda>_. RETURN (the (heapmap_\<alpha> h k))) \<bind> RETURN) \<bind> (\<lambda>v. RETURN (prio v)) \<bind> (\<lambda>pj. (if j < len then (case h of (pq, m) \<Rightarrow> \<lambda>i. ASSERT (0 < i) \<bind> (\<lambda>_. mop_list_get pq (i - 1))) (Suc j) \<bind> (\<lambda>k. ASSERT (heapmap_\<alpha> h k \<noteq> None \<and> hmr_invar h) \<bind> (\<lambda>_. RETURN (the (heapmap_\<alpha> h k))) \<bind> RETURN) \<bind> (\<lambda>v. RETURN (prio v)) \<bind> (\<lambda>psj. if psj < pj then RETURN (j + 1) else RETURN j) else RETURN j) \<bind> (\<lambda>j. (case h of (pq, m) \<Rightarrow> \<lambda>i. ASSERT (0 < i) \<bind> (\<lambda>_. mop_list_get pq (i - 1))) j \<bind> (\<lambda>k. ASSERT (heapmap_\<alpha> h k \<noteq> None \<and> hmr_invar h) \<bind> (\<lambda>_. RETURN (the (heapmap_\<alpha> h k))) \<bind> RETURN) \<bind> (\<lambda>v. RETURN (prio v)) \<bind> (\<lambda>pj. (case h of (pq, m) \<Rightarrow> \<lambda>i. ASSERT (0 < i) \<bind> (\<lambda>_. mop_list_get pq (i - 1))) k \<bind> (\<lambda>k. ASSERT (heapmap_\<alpha> h k \<noteq> None \<and> hmr_invar h) \<bind> (\<lambda>_. RETURN (the (heapmap_\<alpha> h k))) \<bind> RETURN) \<bind> (\<lambda>v. RETURN (prio v)) \<bind> (\<lambda>pk. if pj < pk then (case h of (pq, m) \<Rightarrow> \<lambda>i j. ASSERT (hm_valid (pq, m) i) \<bind> (\<lambda>_. ASSERT (hm_valid (pq, m) j) \<bind> (\<lambda>_. ASSERT (hmr_invar (pq, m)) \<bind> (\<lambda>_. mop_list_swap pq (i - 1) (j - 1) \<bind> (\<lambda>pq. RETURN (pq, m)))))) k j \<bind> (\<lambda>h. D (h, j)) else RETURN h)))) else RETURN h)) = f; x1 = (x1a, x2); x1 = (x1b, x2a); x = (x1, x2b); 0 < x2b \<and> x2b \<le> hm_length x1; 2 * x2b \<le> hm_length x1; 0 < 2 * x2b; 2 * x2b - 1 < length x1b; heapmap_\<alpha> x1 (x1b ! (2 * x2b - 1)) \<noteq> None \<and> hmr_invar x1; \<not> 2 * x2b < hm_length x1; 0 < 2 * x2b; 2 * x2b - 1 < length x1b; heapmap_\<alpha> x1 (x1b ! (2 * x2b - 1)) \<noteq> None \<and> hmr_invar x1; 0 < x2b; x2b - 1 < length x1b; heapmap_\<alpha> x1 (x1b ! (x2b - 1)) \<noteq> None \<and> hmr_invar x1; prio (the (heapmap_\<alpha> x1 (x1b ! (2 * x2b - 1)))) < prio (the (heapmap_\<alpha> x1 (x1b ! (x2b - 1)))); hm_valid (x1a, x2) x2b; hm_valid (x1a, x2) (2 * x2b); hmr_invar (x1a, x2); x2b - 1 < length x1a \<and> 2 * x2b - 1 < length x1a\<rbrakk> \<Longrightarrow> f ((swap x1a (x2b - 1) (2 * x2b - 1), x2), 2 * x2b) \<le>\<^sub>n SPEC (\<lambda>hm'. heapmap_\<alpha> hm' = heapmap_\<alpha> hm)
 6. \<And>f x x1 x1a x2 x1b x2a x2b. \<lbrakk>hm_valid hm i; \<And>x'. \<lbrakk>case x' of (hm', i) \<Rightarrow> hm_valid hm' i \<and> heapmap_\<alpha> hm' = heapmap_\<alpha> hm \<and> hm_length hm' = hm_length hm; (x', x) \<in> measure (\<lambda>(hm', i). hm_length hm' - i)\<rbrakk> \<Longrightarrow> f x' \<le>\<^sub>n SPEC (\<lambda>hm'. heapmap_\<alpha> hm' = heapmap_\<alpha> hm); case x of (hm', i) \<Rightarrow> hm_valid hm' i \<and> heapmap_\<alpha> hm' = heapmap_\<alpha> hm \<and> hm_length hm' = hm_length hm; REC\<^sub>T (\<lambda>D a. case a of (h, k) \<Rightarrow> ASSERT (0 < k \<and> k \<le> hm_length h) \<bind> (\<lambda>_. let len = hm_length h in if 2 * k \<le> len then let j = 2 * k in (case h of (pq, m) \<Rightarrow> \<lambda>i. ASSERT (0 < i) \<bind> (\<lambda>_. mop_list_get pq (i - 1))) j \<bind> (\<lambda>k. ASSERT (heapmap_\<alpha> h k \<noteq> None \<and> hmr_invar h) \<bind> (\<lambda>_. RETURN (the (heapmap_\<alpha> h k))) \<bind> RETURN) \<bind> (\<lambda>v. RETURN (prio v)) \<bind> (\<lambda>pj. (if j < len then (case h of (pq, m) \<Rightarrow> \<lambda>i. ASSERT (0 < i) \<bind> (\<lambda>_. mop_list_get pq (i - 1))) (Suc j) \<bind> (\<lambda>k. ASSERT (heapmap_\<alpha> h k \<noteq> None \<and> hmr_invar h) \<bind> (\<lambda>_. RETURN (the (heapmap_\<alpha> h k))) \<bind> RETURN) \<bind> (\<lambda>v. RETURN (prio v)) \<bind> (\<lambda>psj. if psj < pj then RETURN (j + 1) else RETURN j) else RETURN j) \<bind> (\<lambda>j. (case h of (pq, m) \<Rightarrow> \<lambda>i. ASSERT (0 < i) \<bind> (\<lambda>_. mop_list_get pq (i - 1))) j \<bind> (\<lambda>k. ASSERT (heapmap_\<alpha> h k \<noteq> None \<and> hmr_invar h) \<bind> (\<lambda>_. RETURN (the (heapmap_\<alpha> h k))) \<bind> RETURN) \<bind> (\<lambda>v. RETURN (prio v)) \<bind> (\<lambda>pj. (case h of (pq, m) \<Rightarrow> \<lambda>i. ASSERT (0 < i) \<bind> (\<lambda>_. mop_list_get pq (i - 1))) k \<bind> (\<lambda>k. ASSERT (heapmap_\<alpha> h k \<noteq> None \<and> hmr_invar h) \<bind> (\<lambda>_. RETURN (the (heapmap_\<alpha> h k))) \<bind> RETURN) \<bind> (\<lambda>v. RETURN (prio v)) \<bind> (\<lambda>pk. if pj < pk then (case h of (pq, m) \<Rightarrow> \<lambda>i j. ASSERT (hm_valid (pq, m) i) \<bind> (\<lambda>_. ASSERT (hm_valid (pq, m) j) \<bind> (\<lambda>_. ASSERT (hmr_invar (pq, m)) \<bind> (\<lambda>_. mop_list_swap pq (i - 1) (j - 1) \<bind> (\<lambda>pq. RETURN (pq, m)))))) k j \<bind> (\<lambda>h. D (h, j)) else RETURN h)))) else RETURN h)) = f; x1 = (x1a, x2); x1 = (x1b, x2a); x = (x1, x2b); 0 < x2b \<and> x2b \<le> hm_length x1; 2 * x2b \<le> hm_length x1; 0 < 2 * x2b; 2 * x2b - 1 < length x1b; heapmap_\<alpha> x1 (x1b ! (2 * x2b - 1)) \<noteq> None \<and> hmr_invar x1; \<not> 2 * x2b < hm_length x1; 0 < 2 * x2b; 2 * x2b - 1 < length x1b; heapmap_\<alpha> x1 (x1b ! (2 * x2b - 1)) \<noteq> None \<and> hmr_invar x1; 0 < x2b; x2b - 1 < length x1b; heapmap_\<alpha> x1 (x1b ! (x2b - 1)) \<noteq> None \<and> hmr_invar x1; \<not> prio (the (heapmap_\<alpha> x1 (x1b ! (2 * x2b - 1)))) < prio (the (heapmap_\<alpha> x1 (x1b ! (x2b - 1))))\<rbrakk> \<Longrightarrow> heapmap_\<alpha> x1 = heapmap_\<alpha> hm
 7. \<And>f x x1 x1a x2 x1b x2a x2b. \<lbrakk>hm_valid hm i; \<And>x'. \<lbrakk>case x' of (hm', i) \<Rightarrow> hm_valid hm' i \<and> heapmap_\<alpha> hm' = heapmap_\<alpha> hm \<and> hm_length hm' = hm_length hm; (x', x) \<in> measure (\<lambda>(hm', i). hm_length hm' - i)\<rbrakk> \<Longrightarrow> f x' \<le>\<^sub>n SPEC (\<lambda>hm'. heapmap_\<alpha> hm' = heapmap_\<alpha> hm); case x of (hm', i) \<Rightarrow> hm_valid hm' i \<and> heapmap_\<alpha> hm' = heapmap_\<alpha> hm \<and> hm_length hm' = hm_length hm; REC\<^sub>T (\<lambda>D a. case a of (h, k) \<Rightarrow> ASSERT (0 < k \<and> k \<le> hm_length h) \<bind> (\<lambda>_. let len = hm_length h in if 2 * k \<le> len then let j = 2 * k in (case h of (pq, m) \<Rightarrow> \<lambda>i. ASSERT (0 < i) \<bind> (\<lambda>_. mop_list_get pq (i - 1))) j \<bind> (\<lambda>k. ASSERT (heapmap_\<alpha> h k \<noteq> None \<and> hmr_invar h) \<bind> (\<lambda>_. RETURN (the (heapmap_\<alpha> h k))) \<bind> RETURN) \<bind> (\<lambda>v. RETURN (prio v)) \<bind> (\<lambda>pj. (if j < len then (case h of (pq, m) \<Rightarrow> \<lambda>i. ASSERT (0 < i) \<bind> (\<lambda>_. mop_list_get pq (i - 1))) (Suc j) \<bind> (\<lambda>k. ASSERT (heapmap_\<alpha> h k \<noteq> None \<and> hmr_invar h) \<bind> (\<lambda>_. RETURN (the (heapmap_\<alpha> h k))) \<bind> RETURN) \<bind> (\<lambda>v. RETURN (prio v)) \<bind> (\<lambda>psj. if psj < pj then RETURN (j + 1) else RETURN j) else RETURN j) \<bind> (\<lambda>j. (case h of (pq, m) \<Rightarrow> \<lambda>i. ASSERT (0 < i) \<bind> (\<lambda>_. mop_list_get pq (i - 1))) j \<bind> (\<lambda>k. ASSERT (heapmap_\<alpha> h k \<noteq> None \<and> hmr_invar h) \<bind> (\<lambda>_. RETURN (the (heapmap_\<alpha> h k))) \<bind> RETURN) \<bind> (\<lambda>v. RETURN (prio v)) \<bind> (\<lambda>pj. (case h of (pq, m) \<Rightarrow> \<lambda>i. ASSERT (0 < i) \<bind> (\<lambda>_. mop_list_get pq (i - 1))) k \<bind> (\<lambda>k. ASSERT (heapmap_\<alpha> h k \<noteq> None \<and> hmr_invar h) \<bind> (\<lambda>_. RETURN (the (heapmap_\<alpha> h k))) \<bind> RETURN) \<bind> (\<lambda>v. RETURN (prio v)) \<bind> (\<lambda>pk. if pj < pk then (case h of (pq, m) \<Rightarrow> \<lambda>i j. ASSERT (hm_valid (pq, m) i) \<bind> (\<lambda>_. ASSERT (hm_valid (pq, m) j) \<bind> (\<lambda>_. ASSERT (hmr_invar (pq, m)) \<bind> (\<lambda>_. mop_list_swap pq (i - 1) (j - 1) \<bind> (\<lambda>pq. RETURN (pq, m)))))) k j \<bind> (\<lambda>h. D (h, j)) else RETURN h)))) else RETURN h)) = f; x1 = (x1a, x2); x1 = (x1b, x2a); x = (x1, x2b); 0 < x2b \<and> x2b \<le> hm_length x1; \<not> 2 * x2b \<le> hm_length x1\<rbrakk> \<Longrightarrow> heapmap_\<alpha> x1 = heapmap_\<alpha> hm
[PROOF STEP]
apply (vc_solve simp add: hm_valid_def hm_length_def)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x1a x2 x2b y ya yb. \<lbrakk>\<And>a b ba. \<lbrakk>0 < ba \<and> ba \<le> length a \<and> heapmap_\<alpha> (a, b) = heapmap_\<alpha> hm \<and> length a = (case hm of (pq, uu_) \<Rightarrow> length pq); (case hm of (pq, uu_) \<Rightarrow> length pq) - ba < (case hm of (pq, uu_) \<Rightarrow> length pq) - x2b\<rbrakk> \<Longrightarrow> REC\<^sub>T (\<lambda>D (h, k). ASSERT (0 < k \<and> k \<le> (case h of (pq, uu_) \<Rightarrow> length pq)) \<bind> (\<lambda>_. let len = case h of (pq, uu_) \<Rightarrow> length pq in if 2 * k \<le> len then let j = 2 * k in (case h of (pq, m) \<Rightarrow> \<lambda>i. ASSERT (0 < i) \<bind> (\<lambda>_. mop_list_get pq (i - 1))) j \<bind> (\<lambda>k. ASSERT (heapmap_\<alpha> h k \<noteq> None \<and> hmr_invar h) \<bind> (\<lambda>_. RETURN (the (heapmap_\<alpha> h k))) \<bind> RETURN) \<bind> (\<lambda>v. RETURN (prio v)) \<bind> (\<lambda>pj. (if j < len then (case h of (pq, m) \<Rightarrow> \<lambda>i. ASSERT (0 < i) \<bind> (\<lambda>_. mop_list_get pq (i - 1))) (Suc j) \<bind> (\<lambda>k. ASSERT (heapmap_\<alpha> h k \<noteq> None \<and> hmr_invar h) \<bind> (\<lambda>_. RETURN (the (heapmap_\<alpha> h k))) \<bind> RETURN) \<bind> (\<lambda>v. RETURN (prio v)) \<bind> (\<lambda>psj. if psj < pj then RETURN (j + 1) else RETURN j) else RETURN j) \<bind> (\<lambda>j. (case h of (pq, m) \<Rightarrow> \<lambda>i. ASSERT (0 < i) \<bind> (\<lambda>_. mop_list_get pq (i - 1))) j \<bind> (\<lambda>k. ASSERT (heapmap_\<alpha> h k \<noteq> None \<and> hmr_invar h) \<bind> (\<lambda>_. RETURN (the (heapmap_\<alpha> h k))) \<bind> RETURN) \<bind> (\<lambda>v. RETURN (prio v)) \<bind> (\<lambda>pj. (case h of (pq, m) \<Rightarrow> \<lambda>i. ASSERT (0 < i) \<bind> (\<lambda>_. mop_list_get pq (i - 1))) k \<bind> (\<lambda>k. ASSERT (heapmap_\<alpha> h k \<noteq> None \<and> hmr_invar h) \<bind> (\<lambda>_. RETURN (the (heapmap_\<alpha> h k))) \<bind> RETURN) \<bind> (\<lambda>v. RETURN (prio v)) \<bind> (\<lambda>pk. if pj < pk then (case h of (pq, m) \<Rightarrow> \<lambda>i j. ASSERT (hm_valid (pq, m) i) \<bind> (\<lambda>_. ASSERT (hm_valid (pq, m) j) \<bind> (\<lambda>_. ASSERT (hmr_invar (pq, m)) \<bind> (\<lambda>_. mop_list_swap pq (i - 1) (j - 1) \<bind> (\<lambda>pq. RETURN (pq, m)))))) k j \<bind> (\<lambda>h. D (h, j)) else RETURN h)))) else RETURN h)) ((a, b), ba) \<le>\<^sub>n SPEC (\<lambda>hm'. heapmap_\<alpha> hm' = heapmap_\<alpha> hm); 2 * x2b - Suc 0 < (case hm of (pq, uu_) \<Rightarrow> length pq); 2 * x2b < (case hm of (pq, uu_) \<Rightarrow> length pq); prio ya < prio y; 0 < x2b; x2b - Suc 0 < (case hm of (pq, uu_) \<Rightarrow> length pq); prio ya < prio yb; hmr_invar (x1a, x2); heapmap_\<alpha> hm (x1a ! (2 * x2b - Suc 0)) = Some y; heapmap_\<alpha> hm (x1a ! (2 * x2b)) = Some ya; heapmap_\<alpha> hm (x1a ! (x2b - Suc 0)) = Some yb; 0 < i; i \<le> (case hm of (pq, uu_) \<Rightarrow> length pq); heapmap_\<alpha> (x1a, x2) = heapmap_\<alpha> hm; length x1a = (case hm of (pq, uu_) \<Rightarrow> length pq)\<rbrakk> \<Longrightarrow> REC\<^sub>T (\<lambda>D (h, k). ASSERT (0 < k \<and> k \<le> (case h of (pq, uu_) \<Rightarrow> length pq)) \<bind> (\<lambda>_. let len = case h of (pq, uu_) \<Rightarrow> length pq in if 2 * k \<le> len then let j = 2 * k in (case h of (pq, m) \<Rightarrow> \<lambda>i. ASSERT (0 < i) \<bind> (\<lambda>_. mop_list_get pq (i - 1))) j \<bind> (\<lambda>k. ASSERT (heapmap_\<alpha> h k \<noteq> None \<and> hmr_invar h) \<bind> (\<lambda>_. RETURN (the (heapmap_\<alpha> h k))) \<bind> RETURN) \<bind> (\<lambda>v. RETURN (prio v)) \<bind> (\<lambda>pj. (if j < len then (case h of (pq, m) \<Rightarrow> \<lambda>i. ASSERT (0 < i) \<bind> (\<lambda>_. mop_list_get pq (i - 1))) (Suc j) \<bind> (\<lambda>k. ASSERT (heapmap_\<alpha> h k \<noteq> None \<and> hmr_invar h) \<bind> (\<lambda>_. RETURN (the (heapmap_\<alpha> h k))) \<bind> RETURN) \<bind> (\<lambda>v. RETURN (prio v)) \<bind> (\<lambda>psj. if psj < pj then RETURN (j + 1) else RETURN j) else RETURN j) \<bind> (\<lambda>j. (case h of (pq, m) \<Rightarrow> \<lambda>i. ASSERT (0 < i) \<bind> (\<lambda>_. mop_list_get pq (i - 1))) j \<bind> (\<lambda>k. ASSERT (heapmap_\<alpha> h k \<noteq> None \<and> hmr_invar h) \<bind> (\<lambda>_. RETURN (the (heapmap_\<alpha> h k))) \<bind> RETURN) \<bind> (\<lambda>v. RETURN (prio v)) \<bind> (\<lambda>pj. (case h of (pq, m) \<Rightarrow> \<lambda>i. ASSERT (0 < i) \<bind> (\<lambda>_. mop_list_get pq (i - 1))) k \<bind> (\<lambda>k. ASSERT (heapmap_\<alpha> h k \<noteq> None \<and> hmr_invar h) \<bind> (\<lambda>_. RETURN (the (heapmap_\<alpha> h k))) \<bind> RETURN) \<bind> (\<lambda>v. RETURN (prio v)) \<bind> (\<lambda>pk. if pj < pk then (case h of (pq, m) \<Rightarrow> \<lambda>i j. ASSERT (hm_valid (pq, m) i) \<bind> (\<lambda>_. ASSERT (hm_valid (pq, m) j) \<bind> (\<lambda>_. ASSERT (hmr_invar (pq, m)) \<bind> (\<lambda>_. mop_list_swap pq (i - 1) (j - 1) \<bind> (\<lambda>pq. RETURN (pq, m)))))) k j \<bind> (\<lambda>h. D (h, j)) else RETURN h)))) else RETURN h)) ((swap x1a (x2b - Suc 0) (2 * x2b), x2), Suc (2 * x2b)) \<le>\<^sub>n SPEC (\<lambda>hm'. heapmap_\<alpha> hm' = heapmap_\<alpha> hm)
 2. \<And>x1a x2 x2b y ya yb. \<lbrakk>\<And>a b ba. \<lbrakk>0 < ba \<and> ba \<le> length a \<and> heapmap_\<alpha> (a, b) = heapmap_\<alpha> hm \<and> length a = (case hm of (pq, uu_) \<Rightarrow> length pq); (case hm of (pq, uu_) \<Rightarrow> length pq) - ba < (case hm of (pq, uu_) \<Rightarrow> length pq) - x2b\<rbrakk> \<Longrightarrow> REC\<^sub>T (\<lambda>D (h, k). ASSERT (0 < k \<and> k \<le> (case h of (pq, uu_) \<Rightarrow> length pq)) \<bind> (\<lambda>_. let len = case h of (pq, uu_) \<Rightarrow> length pq in if 2 * k \<le> len then let j = 2 * k in (case h of (pq, m) \<Rightarrow> \<lambda>i. ASSERT (0 < i) \<bind> (\<lambda>_. mop_list_get pq (i - 1))) j \<bind> (\<lambda>k. ASSERT (heapmap_\<alpha> h k \<noteq> None \<and> hmr_invar h) \<bind> (\<lambda>_. RETURN (the (heapmap_\<alpha> h k))) \<bind> RETURN) \<bind> (\<lambda>v. RETURN (prio v)) \<bind> (\<lambda>pj. (if j < len then (case h of (pq, m) \<Rightarrow> \<lambda>i. ASSERT (0 < i) \<bind> (\<lambda>_. mop_list_get pq (i - 1))) (Suc j) \<bind> (\<lambda>k. ASSERT (heapmap_\<alpha> h k \<noteq> None \<and> hmr_invar h) \<bind> (\<lambda>_. RETURN (the (heapmap_\<alpha> h k))) \<bind> RETURN) \<bind> (\<lambda>v. RETURN (prio v)) \<bind> (\<lambda>psj. if psj < pj then RETURN (j + 1) else RETURN j) else RETURN j) \<bind> (\<lambda>j. (case h of (pq, m) \<Rightarrow> \<lambda>i. ASSERT (0 < i) \<bind> (\<lambda>_. mop_list_get pq (i - 1))) j \<bind> (\<lambda>k. ASSERT (heapmap_\<alpha> h k \<noteq> None \<and> hmr_invar h) \<bind> (\<lambda>_. RETURN (the (heapmap_\<alpha> h k))) \<bind> RETURN) \<bind> (\<lambda>v. RETURN (prio v)) \<bind> (\<lambda>pj. (case h of (pq, m) \<Rightarrow> \<lambda>i. ASSERT (0 < i) \<bind> (\<lambda>_. mop_list_get pq (i - 1))) k \<bind> (\<lambda>k. ASSERT (heapmap_\<alpha> h k \<noteq> None \<and> hmr_invar h) \<bind> (\<lambda>_. RETURN (the (heapmap_\<alpha> h k))) \<bind> RETURN) \<bind> (\<lambda>v. RETURN (prio v)) \<bind> (\<lambda>pk. if pj < pk then (case h of (pq, m) \<Rightarrow> \<lambda>i j. ASSERT (hm_valid (pq, m) i) \<bind> (\<lambda>_. ASSERT (hm_valid (pq, m) j) \<bind> (\<lambda>_. ASSERT (hmr_invar (pq, m)) \<bind> (\<lambda>_. mop_list_swap pq (i - 1) (j - 1) \<bind> (\<lambda>pq. RETURN (pq, m)))))) k j \<bind> (\<lambda>h. D (h, j)) else RETURN h)))) else RETURN h)) ((a, b), ba) \<le>\<^sub>n SPEC (\<lambda>hm'. heapmap_\<alpha> hm' = heapmap_\<alpha> hm); 2 * x2b - Suc 0 < (case hm of (pq, uu_) \<Rightarrow> length pq); 2 * x2b < (case hm of (pq, uu_) \<Rightarrow> length pq); \<not> prio ya < prio y; 0 < x2b; x2b - Suc 0 < (case hm of (pq, uu_) \<Rightarrow> length pq); prio y < prio yb; hmr_invar (x1a, x2); heapmap_\<alpha> hm (x1a ! (2 * x2b - Suc 0)) = Some y; heapmap_\<alpha> hm (x1a ! (2 * x2b)) = Some ya; heapmap_\<alpha> hm (x1a ! (x2b - Suc 0)) = Some yb; 0 < i; i \<le> (case hm of (pq, uu_) \<Rightarrow> length pq); heapmap_\<alpha> (x1a, x2) = heapmap_\<alpha> hm; length x1a = (case hm of (pq, uu_) \<Rightarrow> length pq)\<rbrakk> \<Longrightarrow> REC\<^sub>T (\<lambda>D (h, k). ASSERT (0 < k \<and> k \<le> (case h of (pq, uu_) \<Rightarrow> length pq)) \<bind> (\<lambda>_. let len = case h of (pq, uu_) \<Rightarrow> length pq in if 2 * k \<le> len then let j = 2 * k in (case h of (pq, m) \<Rightarrow> \<lambda>i. ASSERT (0 < i) \<bind> (\<lambda>_. mop_list_get pq (i - 1))) j \<bind> (\<lambda>k. ASSERT (heapmap_\<alpha> h k \<noteq> None \<and> hmr_invar h) \<bind> (\<lambda>_. RETURN (the (heapmap_\<alpha> h k))) \<bind> RETURN) \<bind> (\<lambda>v. RETURN (prio v)) \<bind> (\<lambda>pj. (if j < len then (case h of (pq, m) \<Rightarrow> \<lambda>i. ASSERT (0 < i) \<bind> (\<lambda>_. mop_list_get pq (i - 1))) (Suc j) \<bind> (\<lambda>k. ASSERT (heapmap_\<alpha> h k \<noteq> None \<and> hmr_invar h) \<bind> (\<lambda>_. RETURN (the (heapmap_\<alpha> h k))) \<bind> RETURN) \<bind> (\<lambda>v. RETURN (prio v)) \<bind> (\<lambda>psj. if psj < pj then RETURN (j + 1) else RETURN j) else RETURN j) \<bind> (\<lambda>j. (case h of (pq, m) \<Rightarrow> \<lambda>i. ASSERT (0 < i) \<bind> (\<lambda>_. mop_list_get pq (i - 1))) j \<bind> (\<lambda>k. ASSERT (heapmap_\<alpha> h k \<noteq> None \<and> hmr_invar h) \<bind> (\<lambda>_. RETURN (the (heapmap_\<alpha> h k))) \<bind> RETURN) \<bind> (\<lambda>v. RETURN (prio v)) \<bind> (\<lambda>pj. (case h of (pq, m) \<Rightarrow> \<lambda>i. ASSERT (0 < i) \<bind> (\<lambda>_. mop_list_get pq (i - 1))) k \<bind> (\<lambda>k. ASSERT (heapmap_\<alpha> h k \<noteq> None \<and> hmr_invar h) \<bind> (\<lambda>_. RETURN (the (heapmap_\<alpha> h k))) \<bind> RETURN) \<bind> (\<lambda>v. RETURN (prio v)) \<bind> (\<lambda>pk. if pj < pk then (case h of (pq, m) \<Rightarrow> \<lambda>i j. ASSERT (hm_valid (pq, m) i) \<bind> (\<lambda>_. ASSERT (hm_valid (pq, m) j) \<bind> (\<lambda>_. ASSERT (hmr_invar (pq, m)) \<bind> (\<lambda>_. mop_list_swap pq (i - 1) (j - 1) \<bind> (\<lambda>pq. RETURN (pq, m)))))) k j \<bind> (\<lambda>h. D (h, j)) else RETURN h)))) else RETURN h)) ((swap x1a (x2b - Suc 0) (2 * x2b - Suc 0), x2), 2 * x2b) \<le>\<^sub>n SPEC (\<lambda>hm'. heapmap_\<alpha> hm' = heapmap_\<alpha> hm)
 3. \<And>x1a x2 x2b y ya. \<lbrakk>\<And>a b ba. \<lbrakk>0 < ba \<and> ba \<le> length a \<and> heapmap_\<alpha> (a, b) = heapmap_\<alpha> hm \<and> length a = (case hm of (pq, uu_) \<Rightarrow> length pq); (case hm of (pq, uu_) \<Rightarrow> length pq) - ba < (case hm of (pq, uu_) \<Rightarrow> length pq) - x2b\<rbrakk> \<Longrightarrow> REC\<^sub>T (\<lambda>D (h, k). ASSERT (0 < k \<and> k \<le> (case h of (pq, uu_) \<Rightarrow> length pq)) \<bind> (\<lambda>_. let len = case h of (pq, uu_) \<Rightarrow> length pq in if 2 * k \<le> len then let j = 2 * k in (case h of (pq, m) \<Rightarrow> \<lambda>i. ASSERT (0 < i) \<bind> (\<lambda>_. mop_list_get pq (i - 1))) j \<bind> (\<lambda>k. ASSERT (heapmap_\<alpha> h k \<noteq> None \<and> hmr_invar h) \<bind> (\<lambda>_. RETURN (the (heapmap_\<alpha> h k))) \<bind> RETURN) \<bind> (\<lambda>v. RETURN (prio v)) \<bind> (\<lambda>pj. (if j < len then (case h of (pq, m) \<Rightarrow> \<lambda>i. ASSERT (0 < i) \<bind> (\<lambda>_. mop_list_get pq (i - 1))) (Suc j) \<bind> (\<lambda>k. ASSERT (heapmap_\<alpha> h k \<noteq> None \<and> hmr_invar h) \<bind> (\<lambda>_. RETURN (the (heapmap_\<alpha> h k))) \<bind> RETURN) \<bind> (\<lambda>v. RETURN (prio v)) \<bind> (\<lambda>psj. if psj < pj then RETURN (j + 1) else RETURN j) else RETURN j) \<bind> (\<lambda>j. (case h of (pq, m) \<Rightarrow> \<lambda>i. ASSERT (0 < i) \<bind> (\<lambda>_. mop_list_get pq (i - 1))) j \<bind> (\<lambda>k. ASSERT (heapmap_\<alpha> h k \<noteq> None \<and> hmr_invar h) \<bind> (\<lambda>_. RETURN (the (heapmap_\<alpha> h k))) \<bind> RETURN) \<bind> (\<lambda>v. RETURN (prio v)) \<bind> (\<lambda>pj. (case h of (pq, m) \<Rightarrow> \<lambda>i. ASSERT (0 < i) \<bind> (\<lambda>_. mop_list_get pq (i - 1))) k \<bind> (\<lambda>k. ASSERT (heapmap_\<alpha> h k \<noteq> None \<and> hmr_invar h) \<bind> (\<lambda>_. RETURN (the (heapmap_\<alpha> h k))) \<bind> RETURN) \<bind> (\<lambda>v. RETURN (prio v)) \<bind> (\<lambda>pk. if pj < pk then (case h of (pq, m) \<Rightarrow> \<lambda>i j. ASSERT (hm_valid (pq, m) i) \<bind> (\<lambda>_. ASSERT (hm_valid (pq, m) j) \<bind> (\<lambda>_. ASSERT (hmr_invar (pq, m)) \<bind> (\<lambda>_. mop_list_swap pq (i - 1) (j - 1) \<bind> (\<lambda>pq. RETURN (pq, m)))))) k j \<bind> (\<lambda>h. D (h, j)) else RETURN h)))) else RETURN h)) ((a, b), ba) \<le>\<^sub>n SPEC (\<lambda>hm'. heapmap_\<alpha> hm' = heapmap_\<alpha> hm); 2 * x2b = (case hm of (pq, uu_) \<Rightarrow> length pq); x2b - Suc 0 < (case hm of (pq, uu_) \<Rightarrow> length pq); prio y < prio ya; hmr_invar (x1a, x2); heapmap_\<alpha> hm (x1a ! ((case hm of (pq, uu_) \<Rightarrow> length pq) - Suc 0)) = Some y; heapmap_\<alpha> hm (x1a ! (x2b - Suc 0)) = Some ya; 0 < i; i \<le> (case hm of (pq, uu_) \<Rightarrow> length pq); heapmap_\<alpha> (x1a, x2) = heapmap_\<alpha> hm; length x1a = (case hm of (pq, uu_) \<Rightarrow> length pq)\<rbrakk> \<Longrightarrow> REC\<^sub>T (\<lambda>D (h, k). ASSERT (0 < k \<and> k \<le> (case h of (pq, uu_) \<Rightarrow> length pq)) \<bind> (\<lambda>_. let len = case h of (pq, uu_) \<Rightarrow> length pq in if 2 * k \<le> len then let j = 2 * k in (case h of (pq, m) \<Rightarrow> \<lambda>i. ASSERT (0 < i) \<bind> (\<lambda>_. mop_list_get pq (i - 1))) j \<bind> (\<lambda>k. ASSERT (heapmap_\<alpha> h k \<noteq> None \<and> hmr_invar h) \<bind> (\<lambda>_. RETURN (the (heapmap_\<alpha> h k))) \<bind> RETURN) \<bind> (\<lambda>v. RETURN (prio v)) \<bind> (\<lambda>pj. (if j < len then (case h of (pq, m) \<Rightarrow> \<lambda>i. ASSERT (0 < i) \<bind> (\<lambda>_. mop_list_get pq (i - 1))) (Suc j) \<bind> (\<lambda>k. ASSERT (heapmap_\<alpha> h k \<noteq> None \<and> hmr_invar h) \<bind> (\<lambda>_. RETURN (the (heapmap_\<alpha> h k))) \<bind> RETURN) \<bind> (\<lambda>v. RETURN (prio v)) \<bind> (\<lambda>psj. if psj < pj then RETURN (j + 1) else RETURN j) else RETURN j) \<bind> (\<lambda>j. (case h of (pq, m) \<Rightarrow> \<lambda>i. ASSERT (0 < i) \<bind> (\<lambda>_. mop_list_get pq (i - 1))) j \<bind> (\<lambda>k. ASSERT (heapmap_\<alpha> h k \<noteq> None \<and> hmr_invar h) \<bind> (\<lambda>_. RETURN (the (heapmap_\<alpha> h k))) \<bind> RETURN) \<bind> (\<lambda>v. RETURN (prio v)) \<bind> (\<lambda>pj. (case h of (pq, m) \<Rightarrow> \<lambda>i. ASSERT (0 < i) \<bind> (\<lambda>_. mop_list_get pq (i - 1))) k \<bind> (\<lambda>k. ASSERT (heapmap_\<alpha> h k \<noteq> None \<and> hmr_invar h) \<bind> (\<lambda>_. RETURN (the (heapmap_\<alpha> h k))) \<bind> RETURN) \<bind> (\<lambda>v. RETURN (prio v)) \<bind> (\<lambda>pk. if pj < pk then (case h of (pq, m) \<Rightarrow> \<lambda>i j. ASSERT (hm_valid (pq, m) i) \<bind> (\<lambda>_. ASSERT (hm_valid (pq, m) j) \<bind> (\<lambda>_. ASSERT (hmr_invar (pq, m)) \<bind> (\<lambda>_. mop_list_swap pq (i - 1) (j - 1) \<bind> (\<lambda>pq. RETURN (pq, m)))))) k j \<bind> (\<lambda>h. D (h, j)) else RETURN h)))) else RETURN h)) ((swap x1a (x2b - Suc 0) ((case hm of (pq, uu_) \<Rightarrow> length pq) - Suc 0), x2), case hm of (pq, uu_) \<Rightarrow> length pq) \<le>\<^sub>n SPEC (\<lambda>hm'. heapmap_\<alpha> hm' = heapmap_\<alpha> hm)
[PROOF STEP]
(* Takes long *)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x1a x2 x2b y ya yb. \<lbrakk>\<And>a b ba. \<lbrakk>0 < ba \<and> ba \<le> length a \<and> heapmap_\<alpha> (a, b) = heapmap_\<alpha> hm \<and> length a = (case hm of (pq, uu_) \<Rightarrow> length pq); (case hm of (pq, uu_) \<Rightarrow> length pq) - ba < (case hm of (pq, uu_) \<Rightarrow> length pq) - x2b\<rbrakk> \<Longrightarrow> REC\<^sub>T (\<lambda>D (h, k). ASSERT (0 < k \<and> k \<le> (case h of (pq, uu_) \<Rightarrow> length pq)) \<bind> (\<lambda>_. let len = case h of (pq, uu_) \<Rightarrow> length pq in if 2 * k \<le> len then let j = 2 * k in (case h of (pq, m) \<Rightarrow> \<lambda>i. ASSERT (0 < i) \<bind> (\<lambda>_. mop_list_get pq (i - 1))) j \<bind> (\<lambda>k. ASSERT (heapmap_\<alpha> h k \<noteq> None \<and> hmr_invar h) \<bind> (\<lambda>_. RETURN (the (heapmap_\<alpha> h k))) \<bind> RETURN) \<bind> (\<lambda>v. RETURN (prio v)) \<bind> (\<lambda>pj. (if j < len then (case h of (pq, m) \<Rightarrow> \<lambda>i. ASSERT (0 < i) \<bind> (\<lambda>_. mop_list_get pq (i - 1))) (Suc j) \<bind> (\<lambda>k. ASSERT (heapmap_\<alpha> h k \<noteq> None \<and> hmr_invar h) \<bind> (\<lambda>_. RETURN (the (heapmap_\<alpha> h k))) \<bind> RETURN) \<bind> (\<lambda>v. RETURN (prio v)) \<bind> (\<lambda>psj. if psj < pj then RETURN (j + 1) else RETURN j) else RETURN j) \<bind> (\<lambda>j. (case h of (pq, m) \<Rightarrow> \<lambda>i. ASSERT (0 < i) \<bind> (\<lambda>_. mop_list_get pq (i - 1))) j \<bind> (\<lambda>k. ASSERT (heapmap_\<alpha> h k \<noteq> None \<and> hmr_invar h) \<bind> (\<lambda>_. RETURN (the (heapmap_\<alpha> h k))) \<bind> RETURN) \<bind> (\<lambda>v. RETURN (prio v)) \<bind> (\<lambda>pj. (case h of (pq, m) \<Rightarrow> \<lambda>i. ASSERT (0 < i) \<bind> (\<lambda>_. mop_list_get pq (i - 1))) k \<bind> (\<lambda>k. ASSERT (heapmap_\<alpha> h k \<noteq> None \<and> hmr_invar h) \<bind> (\<lambda>_. RETURN (the (heapmap_\<alpha> h k))) \<bind> RETURN) \<bind> (\<lambda>v. RETURN (prio v)) \<bind> (\<lambda>pk. if pj < pk then (case h of (pq, m) \<Rightarrow> \<lambda>i j. ASSERT (hm_valid (pq, m) i) \<bind> (\<lambda>_. ASSERT (hm_valid (pq, m) j) \<bind> (\<lambda>_. ASSERT (hmr_invar (pq, m)) \<bind> (\<lambda>_. mop_list_swap pq (i - 1) (j - 1) \<bind> (\<lambda>pq. RETURN (pq, m)))))) k j \<bind> (\<lambda>h. D (h, j)) else RETURN h)))) else RETURN h)) ((a, b), ba) \<le>\<^sub>n SPEC (\<lambda>hm'. heapmap_\<alpha> hm' = heapmap_\<alpha> hm); 2 * x2b - Suc 0 < (case hm of (pq, uu_) \<Rightarrow> length pq); 2 * x2b < (case hm of (pq, uu_) \<Rightarrow> length pq); prio ya < prio y; 0 < x2b; x2b - Suc 0 < (case hm of (pq, uu_) \<Rightarrow> length pq); prio ya < prio yb; hmr_invar (x1a, x2); heapmap_\<alpha> hm (x1a ! (2 * x2b - Suc 0)) = Some y; heapmap_\<alpha> hm (x1a ! (2 * x2b)) = Some ya; heapmap_\<alpha> hm (x1a ! (x2b - Suc 0)) = Some yb; 0 < i; i \<le> (case hm of (pq, uu_) \<Rightarrow> length pq); heapmap_\<alpha> (x1a, x2) = heapmap_\<alpha> hm; length x1a = (case hm of (pq, uu_) \<Rightarrow> length pq)\<rbrakk> \<Longrightarrow> REC\<^sub>T (\<lambda>D (h, k). ASSERT (0 < k \<and> k \<le> (case h of (pq, uu_) \<Rightarrow> length pq)) \<bind> (\<lambda>_. let len = case h of (pq, uu_) \<Rightarrow> length pq in if 2 * k \<le> len then let j = 2 * k in (case h of (pq, m) \<Rightarrow> \<lambda>i. ASSERT (0 < i) \<bind> (\<lambda>_. mop_list_get pq (i - 1))) j \<bind> (\<lambda>k. ASSERT (heapmap_\<alpha> h k \<noteq> None \<and> hmr_invar h) \<bind> (\<lambda>_. RETURN (the (heapmap_\<alpha> h k))) \<bind> RETURN) \<bind> (\<lambda>v. RETURN (prio v)) \<bind> (\<lambda>pj. (if j < len then (case h of (pq, m) \<Rightarrow> \<lambda>i. ASSERT (0 < i) \<bind> (\<lambda>_. mop_list_get pq (i - 1))) (Suc j) \<bind> (\<lambda>k. ASSERT (heapmap_\<alpha> h k \<noteq> None \<and> hmr_invar h) \<bind> (\<lambda>_. RETURN (the (heapmap_\<alpha> h k))) \<bind> RETURN) \<bind> (\<lambda>v. RETURN (prio v)) \<bind> (\<lambda>psj. if psj < pj then RETURN (j + 1) else RETURN j) else RETURN j) \<bind> (\<lambda>j. (case h of (pq, m) \<Rightarrow> \<lambda>i. ASSERT (0 < i) \<bind> (\<lambda>_. mop_list_get pq (i - 1))) j \<bind> (\<lambda>k. ASSERT (heapmap_\<alpha> h k \<noteq> None \<and> hmr_invar h) \<bind> (\<lambda>_. RETURN (the (heapmap_\<alpha> h k))) \<bind> RETURN) \<bind> (\<lambda>v. RETURN (prio v)) \<bind> (\<lambda>pj. (case h of (pq, m) \<Rightarrow> \<lambda>i. ASSERT (0 < i) \<bind> (\<lambda>_. mop_list_get pq (i - 1))) k \<bind> (\<lambda>k. ASSERT (heapmap_\<alpha> h k \<noteq> None \<and> hmr_invar h) \<bind> (\<lambda>_. RETURN (the (heapmap_\<alpha> h k))) \<bind> RETURN) \<bind> (\<lambda>v. RETURN (prio v)) \<bind> (\<lambda>pk. if pj < pk then (case h of (pq, m) \<Rightarrow> \<lambda>i j. ASSERT (hm_valid (pq, m) i) \<bind> (\<lambda>_. ASSERT (hm_valid (pq, m) j) \<bind> (\<lambda>_. ASSERT (hmr_invar (pq, m)) \<bind> (\<lambda>_. mop_list_swap pq (i - 1) (j - 1) \<bind> (\<lambda>pq. RETURN (pq, m)))))) k j \<bind> (\<lambda>h. D (h, j)) else RETURN h)))) else RETURN h)) ((swap x1a (x2b - Suc 0) (2 * x2b), x2), Suc (2 * x2b)) \<le>\<^sub>n SPEC (\<lambda>hm'. heapmap_\<alpha> hm' = heapmap_\<alpha> hm)
 2. \<And>x1a x2 x2b y ya yb. \<lbrakk>\<And>a b ba. \<lbrakk>0 < ba \<and> ba \<le> length a \<and> heapmap_\<alpha> (a, b) = heapmap_\<alpha> hm \<and> length a = (case hm of (pq, uu_) \<Rightarrow> length pq); (case hm of (pq, uu_) \<Rightarrow> length pq) - ba < (case hm of (pq, uu_) \<Rightarrow> length pq) - x2b\<rbrakk> \<Longrightarrow> REC\<^sub>T (\<lambda>D (h, k). ASSERT (0 < k \<and> k \<le> (case h of (pq, uu_) \<Rightarrow> length pq)) \<bind> (\<lambda>_. let len = case h of (pq, uu_) \<Rightarrow> length pq in if 2 * k \<le> len then let j = 2 * k in (case h of (pq, m) \<Rightarrow> \<lambda>i. ASSERT (0 < i) \<bind> (\<lambda>_. mop_list_get pq (i - 1))) j \<bind> (\<lambda>k. ASSERT (heapmap_\<alpha> h k \<noteq> None \<and> hmr_invar h) \<bind> (\<lambda>_. RETURN (the (heapmap_\<alpha> h k))) \<bind> RETURN) \<bind> (\<lambda>v. RETURN (prio v)) \<bind> (\<lambda>pj. (if j < len then (case h of (pq, m) \<Rightarrow> \<lambda>i. ASSERT (0 < i) \<bind> (\<lambda>_. mop_list_get pq (i - 1))) (Suc j) \<bind> (\<lambda>k. ASSERT (heapmap_\<alpha> h k \<noteq> None \<and> hmr_invar h) \<bind> (\<lambda>_. RETURN (the (heapmap_\<alpha> h k))) \<bind> RETURN) \<bind> (\<lambda>v. RETURN (prio v)) \<bind> (\<lambda>psj. if psj < pj then RETURN (j + 1) else RETURN j) else RETURN j) \<bind> (\<lambda>j. (case h of (pq, m) \<Rightarrow> \<lambda>i. ASSERT (0 < i) \<bind> (\<lambda>_. mop_list_get pq (i - 1))) j \<bind> (\<lambda>k. ASSERT (heapmap_\<alpha> h k \<noteq> None \<and> hmr_invar h) \<bind> (\<lambda>_. RETURN (the (heapmap_\<alpha> h k))) \<bind> RETURN) \<bind> (\<lambda>v. RETURN (prio v)) \<bind> (\<lambda>pj. (case h of (pq, m) \<Rightarrow> \<lambda>i. ASSERT (0 < i) \<bind> (\<lambda>_. mop_list_get pq (i - 1))) k \<bind> (\<lambda>k. ASSERT (heapmap_\<alpha> h k \<noteq> None \<and> hmr_invar h) \<bind> (\<lambda>_. RETURN (the (heapmap_\<alpha> h k))) \<bind> RETURN) \<bind> (\<lambda>v. RETURN (prio v)) \<bind> (\<lambda>pk. if pj < pk then (case h of (pq, m) \<Rightarrow> \<lambda>i j. ASSERT (hm_valid (pq, m) i) \<bind> (\<lambda>_. ASSERT (hm_valid (pq, m) j) \<bind> (\<lambda>_. ASSERT (hmr_invar (pq, m)) \<bind> (\<lambda>_. mop_list_swap pq (i - 1) (j - 1) \<bind> (\<lambda>pq. RETURN (pq, m)))))) k j \<bind> (\<lambda>h. D (h, j)) else RETURN h)))) else RETURN h)) ((a, b), ba) \<le>\<^sub>n SPEC (\<lambda>hm'. heapmap_\<alpha> hm' = heapmap_\<alpha> hm); 2 * x2b - Suc 0 < (case hm of (pq, uu_) \<Rightarrow> length pq); 2 * x2b < (case hm of (pq, uu_) \<Rightarrow> length pq); \<not> prio ya < prio y; 0 < x2b; x2b - Suc 0 < (case hm of (pq, uu_) \<Rightarrow> length pq); prio y < prio yb; hmr_invar (x1a, x2); heapmap_\<alpha> hm (x1a ! (2 * x2b - Suc 0)) = Some y; heapmap_\<alpha> hm (x1a ! (2 * x2b)) = Some ya; heapmap_\<alpha> hm (x1a ! (x2b - Suc 0)) = Some yb; 0 < i; i \<le> (case hm of (pq, uu_) \<Rightarrow> length pq); heapmap_\<alpha> (x1a, x2) = heapmap_\<alpha> hm; length x1a = (case hm of (pq, uu_) \<Rightarrow> length pq)\<rbrakk> \<Longrightarrow> REC\<^sub>T (\<lambda>D (h, k). ASSERT (0 < k \<and> k \<le> (case h of (pq, uu_) \<Rightarrow> length pq)) \<bind> (\<lambda>_. let len = case h of (pq, uu_) \<Rightarrow> length pq in if 2 * k \<le> len then let j = 2 * k in (case h of (pq, m) \<Rightarrow> \<lambda>i. ASSERT (0 < i) \<bind> (\<lambda>_. mop_list_get pq (i - 1))) j \<bind> (\<lambda>k. ASSERT (heapmap_\<alpha> h k \<noteq> None \<and> hmr_invar h) \<bind> (\<lambda>_. RETURN (the (heapmap_\<alpha> h k))) \<bind> RETURN) \<bind> (\<lambda>v. RETURN (prio v)) \<bind> (\<lambda>pj. (if j < len then (case h of (pq, m) \<Rightarrow> \<lambda>i. ASSERT (0 < i) \<bind> (\<lambda>_. mop_list_get pq (i - 1))) (Suc j) \<bind> (\<lambda>k. ASSERT (heapmap_\<alpha> h k \<noteq> None \<and> hmr_invar h) \<bind> (\<lambda>_. RETURN (the (heapmap_\<alpha> h k))) \<bind> RETURN) \<bind> (\<lambda>v. RETURN (prio v)) \<bind> (\<lambda>psj. if psj < pj then RETURN (j + 1) else RETURN j) else RETURN j) \<bind> (\<lambda>j. (case h of (pq, m) \<Rightarrow> \<lambda>i. ASSERT (0 < i) \<bind> (\<lambda>_. mop_list_get pq (i - 1))) j \<bind> (\<lambda>k. ASSERT (heapmap_\<alpha> h k \<noteq> None \<and> hmr_invar h) \<bind> (\<lambda>_. RETURN (the (heapmap_\<alpha> h k))) \<bind> RETURN) \<bind> (\<lambda>v. RETURN (prio v)) \<bind> (\<lambda>pj. (case h of (pq, m) \<Rightarrow> \<lambda>i. ASSERT (0 < i) \<bind> (\<lambda>_. mop_list_get pq (i - 1))) k \<bind> (\<lambda>k. ASSERT (heapmap_\<alpha> h k \<noteq> None \<and> hmr_invar h) \<bind> (\<lambda>_. RETURN (the (heapmap_\<alpha> h k))) \<bind> RETURN) \<bind> (\<lambda>v. RETURN (prio v)) \<bind> (\<lambda>pk. if pj < pk then (case h of (pq, m) \<Rightarrow> \<lambda>i j. ASSERT (hm_valid (pq, m) i) \<bind> (\<lambda>_. ASSERT (hm_valid (pq, m) j) \<bind> (\<lambda>_. ASSERT (hmr_invar (pq, m)) \<bind> (\<lambda>_. mop_list_swap pq (i - 1) (j - 1) \<bind> (\<lambda>pq. RETURN (pq, m)))))) k j \<bind> (\<lambda>h. D (h, j)) else RETURN h)))) else RETURN h)) ((swap x1a (x2b - Suc 0) (2 * x2b - Suc 0), x2), 2 * x2b) \<le>\<^sub>n SPEC (\<lambda>hm'. heapmap_\<alpha> hm' = heapmap_\<alpha> hm)
 3. \<And>x1a x2 x2b y ya. \<lbrakk>\<And>a b ba. \<lbrakk>0 < ba \<and> ba \<le> length a \<and> heapmap_\<alpha> (a, b) = heapmap_\<alpha> hm \<and> length a = (case hm of (pq, uu_) \<Rightarrow> length pq); (case hm of (pq, uu_) \<Rightarrow> length pq) - ba < (case hm of (pq, uu_) \<Rightarrow> length pq) - x2b\<rbrakk> \<Longrightarrow> REC\<^sub>T (\<lambda>D (h, k). ASSERT (0 < k \<and> k \<le> (case h of (pq, uu_) \<Rightarrow> length pq)) \<bind> (\<lambda>_. let len = case h of (pq, uu_) \<Rightarrow> length pq in if 2 * k \<le> len then let j = 2 * k in (case h of (pq, m) \<Rightarrow> \<lambda>i. ASSERT (0 < i) \<bind> (\<lambda>_. mop_list_get pq (i - 1))) j \<bind> (\<lambda>k. ASSERT (heapmap_\<alpha> h k \<noteq> None \<and> hmr_invar h) \<bind> (\<lambda>_. RETURN (the (heapmap_\<alpha> h k))) \<bind> RETURN) \<bind> (\<lambda>v. RETURN (prio v)) \<bind> (\<lambda>pj. (if j < len then (case h of (pq, m) \<Rightarrow> \<lambda>i. ASSERT (0 < i) \<bind> (\<lambda>_. mop_list_get pq (i - 1))) (Suc j) \<bind> (\<lambda>k. ASSERT (heapmap_\<alpha> h k \<noteq> None \<and> hmr_invar h) \<bind> (\<lambda>_. RETURN (the (heapmap_\<alpha> h k))) \<bind> RETURN) \<bind> (\<lambda>v. RETURN (prio v)) \<bind> (\<lambda>psj. if psj < pj then RETURN (j + 1) else RETURN j) else RETURN j) \<bind> (\<lambda>j. (case h of (pq, m) \<Rightarrow> \<lambda>i. ASSERT (0 < i) \<bind> (\<lambda>_. mop_list_get pq (i - 1))) j \<bind> (\<lambda>k. ASSERT (heapmap_\<alpha> h k \<noteq> None \<and> hmr_invar h) \<bind> (\<lambda>_. RETURN (the (heapmap_\<alpha> h k))) \<bind> RETURN) \<bind> (\<lambda>v. RETURN (prio v)) \<bind> (\<lambda>pj. (case h of (pq, m) \<Rightarrow> \<lambda>i. ASSERT (0 < i) \<bind> (\<lambda>_. mop_list_get pq (i - 1))) k \<bind> (\<lambda>k. ASSERT (heapmap_\<alpha> h k \<noteq> None \<and> hmr_invar h) \<bind> (\<lambda>_. RETURN (the (heapmap_\<alpha> h k))) \<bind> RETURN) \<bind> (\<lambda>v. RETURN (prio v)) \<bind> (\<lambda>pk. if pj < pk then (case h of (pq, m) \<Rightarrow> \<lambda>i j. ASSERT (hm_valid (pq, m) i) \<bind> (\<lambda>_. ASSERT (hm_valid (pq, m) j) \<bind> (\<lambda>_. ASSERT (hmr_invar (pq, m)) \<bind> (\<lambda>_. mop_list_swap pq (i - 1) (j - 1) \<bind> (\<lambda>pq. RETURN (pq, m)))))) k j \<bind> (\<lambda>h. D (h, j)) else RETURN h)))) else RETURN h)) ((a, b), ba) \<le>\<^sub>n SPEC (\<lambda>hm'. heapmap_\<alpha> hm' = heapmap_\<alpha> hm); 2 * x2b = (case hm of (pq, uu_) \<Rightarrow> length pq); x2b - Suc 0 < (case hm of (pq, uu_) \<Rightarrow> length pq); prio y < prio ya; hmr_invar (x1a, x2); heapmap_\<alpha> hm (x1a ! ((case hm of (pq, uu_) \<Rightarrow> length pq) - Suc 0)) = Some y; heapmap_\<alpha> hm (x1a ! (x2b - Suc 0)) = Some ya; 0 < i; i \<le> (case hm of (pq, uu_) \<Rightarrow> length pq); heapmap_\<alpha> (x1a, x2) = heapmap_\<alpha> hm; length x1a = (case hm of (pq, uu_) \<Rightarrow> length pq)\<rbrakk> \<Longrightarrow> REC\<^sub>T (\<lambda>D (h, k). ASSERT (0 < k \<and> k \<le> (case h of (pq, uu_) \<Rightarrow> length pq)) \<bind> (\<lambda>_. let len = case h of (pq, uu_) \<Rightarrow> length pq in if 2 * k \<le> len then let j = 2 * k in (case h of (pq, m) \<Rightarrow> \<lambda>i. ASSERT (0 < i) \<bind> (\<lambda>_. mop_list_get pq (i - 1))) j \<bind> (\<lambda>k. ASSERT (heapmap_\<alpha> h k \<noteq> None \<and> hmr_invar h) \<bind> (\<lambda>_. RETURN (the (heapmap_\<alpha> h k))) \<bind> RETURN) \<bind> (\<lambda>v. RETURN (prio v)) \<bind> (\<lambda>pj. (if j < len then (case h of (pq, m) \<Rightarrow> \<lambda>i. ASSERT (0 < i) \<bind> (\<lambda>_. mop_list_get pq (i - 1))) (Suc j) \<bind> (\<lambda>k. ASSERT (heapmap_\<alpha> h k \<noteq> None \<and> hmr_invar h) \<bind> (\<lambda>_. RETURN (the (heapmap_\<alpha> h k))) \<bind> RETURN) \<bind> (\<lambda>v. RETURN (prio v)) \<bind> (\<lambda>psj. if psj < pj then RETURN (j + 1) else RETURN j) else RETURN j) \<bind> (\<lambda>j. (case h of (pq, m) \<Rightarrow> \<lambda>i. ASSERT (0 < i) \<bind> (\<lambda>_. mop_list_get pq (i - 1))) j \<bind> (\<lambda>k. ASSERT (heapmap_\<alpha> h k \<noteq> None \<and> hmr_invar h) \<bind> (\<lambda>_. RETURN (the (heapmap_\<alpha> h k))) \<bind> RETURN) \<bind> (\<lambda>v. RETURN (prio v)) \<bind> (\<lambda>pj. (case h of (pq, m) \<Rightarrow> \<lambda>i. ASSERT (0 < i) \<bind> (\<lambda>_. mop_list_get pq (i - 1))) k \<bind> (\<lambda>k. ASSERT (heapmap_\<alpha> h k \<noteq> None \<and> hmr_invar h) \<bind> (\<lambda>_. RETURN (the (heapmap_\<alpha> h k))) \<bind> RETURN) \<bind> (\<lambda>v. RETURN (prio v)) \<bind> (\<lambda>pk. if pj < pk then (case h of (pq, m) \<Rightarrow> \<lambda>i j. ASSERT (hm_valid (pq, m) i) \<bind> (\<lambda>_. ASSERT (hm_valid (pq, m) j) \<bind> (\<lambda>_. ASSERT (hmr_invar (pq, m)) \<bind> (\<lambda>_. mop_list_swap pq (i - 1) (j - 1) \<bind> (\<lambda>pq. RETURN (pq, m)))))) k j \<bind> (\<lambda>h. D (h, j)) else RETURN h)))) else RETURN h)) ((swap x1a (x2b - Suc 0) ((case hm of (pq, uu_) \<Rightarrow> length pq) - Suc 0), x2), case hm of (pq, uu_) \<Rightarrow> length pq) \<le>\<^sub>n SPEC (\<lambda>hm'. heapmap_\<alpha> hm' = heapmap_\<alpha> hm)
[PROOF STEP]
apply rprems
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>x1a x2 x2b y ya yb. \<lbrakk>2 * x2b - Suc 0 < (case hm of (pq, uu_) \<Rightarrow> length pq); 2 * x2b < (case hm of (pq, uu_) \<Rightarrow> length pq); prio ya < prio y; 0 < x2b; x2b - Suc 0 < (case hm of (pq, uu_) \<Rightarrow> length pq); prio ya < prio yb; hmr_invar (x1a, x2); heapmap_\<alpha> hm (x1a ! (2 * x2b - Suc 0)) = Some y; heapmap_\<alpha> hm (x1a ! (2 * x2b)) = Some ya; heapmap_\<alpha> hm (x1a ! (x2b - Suc 0)) = Some yb; 0 < i; i \<le> (case hm of (pq, uu_) \<Rightarrow> length pq); heapmap_\<alpha> (x1a, x2) = heapmap_\<alpha> hm; length x1a = (case hm of (pq, uu_) \<Rightarrow> length pq)\<rbrakk> \<Longrightarrow> 0 < Suc (2 * x2b) \<and> Suc (2 * x2b) \<le> length (swap x1a (x2b - Suc 0) (2 * x2b)) \<and> heapmap_\<alpha> (swap x1a (x2b - Suc 0) (2 * x2b), x2) = heapmap_\<alpha> hm \<and> length (swap x1a (x2b - Suc 0) (2 * x2b)) = (case hm of (pq, uu_) \<Rightarrow> length pq)
 2. \<And>x1a x2 x2b y ya yb. \<lbrakk>2 * x2b - Suc 0 < (case hm of (pq, uu_) \<Rightarrow> length pq); 2 * x2b < (case hm of (pq, uu_) \<Rightarrow> length pq); prio ya < prio y; 0 < x2b; x2b - Suc 0 < (case hm of (pq, uu_) \<Rightarrow> length pq); prio ya < prio yb; hmr_invar (x1a, x2); heapmap_\<alpha> hm (x1a ! (2 * x2b - Suc 0)) = Some y; heapmap_\<alpha> hm (x1a ! (2 * x2b)) = Some ya; heapmap_\<alpha> hm (x1a ! (x2b - Suc 0)) = Some yb; 0 < i; i \<le> (case hm of (pq, uu_) \<Rightarrow> length pq); heapmap_\<alpha> (x1a, x2) = heapmap_\<alpha> hm; length x1a = (case hm of (pq, uu_) \<Rightarrow> length pq)\<rbrakk> \<Longrightarrow> (case hm of (pq, uu_) \<Rightarrow> length pq) - Suc (2 * x2b) < (case hm of (pq, uu_) \<Rightarrow> length pq) - x2b
 3. \<And>x1a x2 x2b y ya yb. \<lbrakk>\<And>a b ba. \<lbrakk>0 < ba \<and> ba \<le> length a \<and> heapmap_\<alpha> (a, b) = heapmap_\<alpha> hm \<and> length a = (case hm of (pq, uu_) \<Rightarrow> length pq); (case hm of (pq, uu_) \<Rightarrow> length pq) - ba < (case hm of (pq, uu_) \<Rightarrow> length pq) - x2b\<rbrakk> \<Longrightarrow> REC\<^sub>T (\<lambda>D (h, k). ASSERT (0 < k \<and> k \<le> (case h of (pq, uu_) \<Rightarrow> length pq)) \<bind> (\<lambda>_. let len = case h of (pq, uu_) \<Rightarrow> length pq in if 2 * k \<le> len then let j = 2 * k in (case h of (pq, m) \<Rightarrow> \<lambda>i. ASSERT (0 < i) \<bind> (\<lambda>_. mop_list_get pq (i - 1))) j \<bind> (\<lambda>k. ASSERT (heapmap_\<alpha> h k \<noteq> None \<and> hmr_invar h) \<bind> (\<lambda>_. RETURN (the (heapmap_\<alpha> h k))) \<bind> RETURN) \<bind> (\<lambda>v. RETURN (prio v)) \<bind> (\<lambda>pj. (if j < len then (case h of (pq, m) \<Rightarrow> \<lambda>i. ASSERT (0 < i) \<bind> (\<lambda>_. mop_list_get pq (i - 1))) (Suc j) \<bind> (\<lambda>k. ASSERT (heapmap_\<alpha> h k \<noteq> None \<and> hmr_invar h) \<bind> (\<lambda>_. RETURN (the (heapmap_\<alpha> h k))) \<bind> RETURN) \<bind> (\<lambda>v. RETURN (prio v)) \<bind> (\<lambda>psj. if psj < pj then RETURN (j + 1) else RETURN j) else RETURN j) \<bind> (\<lambda>j. (case h of (pq, m) \<Rightarrow> \<lambda>i. ASSERT (0 < i) \<bind> (\<lambda>_. mop_list_get pq (i - 1))) j \<bind> (\<lambda>k. ASSERT (heapmap_\<alpha> h k \<noteq> None \<and> hmr_invar h) \<bind> (\<lambda>_. RETURN (the (heapmap_\<alpha> h k))) \<bind> RETURN) \<bind> (\<lambda>v. RETURN (prio v)) \<bind> (\<lambda>pj. (case h of (pq, m) \<Rightarrow> \<lambda>i. ASSERT (0 < i) \<bind> (\<lambda>_. mop_list_get pq (i - 1))) k \<bind> (\<lambda>k. ASSERT (heapmap_\<alpha> h k \<noteq> None \<and> hmr_invar h) \<bind> (\<lambda>_. RETURN (the (heapmap_\<alpha> h k))) \<bind> RETURN) \<bind> (\<lambda>v. RETURN (prio v)) \<bind> (\<lambda>pk. if pj < pk then (case h of (pq, m) \<Rightarrow> \<lambda>i j. ASSERT (hm_valid (pq, m) i) \<bind> (\<lambda>_. ASSERT (hm_valid (pq, m) j) \<bind> (\<lambda>_. ASSERT (hmr_invar (pq, m)) \<bind> (\<lambda>_. mop_list_swap pq (i - 1) (j - 1) \<bind> (\<lambda>pq. RETURN (pq, m)))))) k j \<bind> (\<lambda>h. D (h, j)) else RETURN h)))) else RETURN h)) ((a, b), ba) \<le>\<^sub>n SPEC (\<lambda>hm'. heapmap_\<alpha> hm' = heapmap_\<alpha> hm); 2 * x2b - Suc 0 < (case hm of (pq, uu_) \<Rightarrow> length pq); 2 * x2b < (case hm of (pq, uu_) \<Rightarrow> length pq); \<not> prio ya < prio y; 0 < x2b; x2b - Suc 0 < (case hm of (pq, uu_) \<Rightarrow> length pq); prio y < prio yb; hmr_invar (x1a, x2); heapmap_\<alpha> hm (x1a ! (2 * x2b - Suc 0)) = Some y; heapmap_\<alpha> hm (x1a ! (2 * x2b)) = Some ya; heapmap_\<alpha> hm (x1a ! (x2b - Suc 0)) = Some yb; 0 < i; i \<le> (case hm of (pq, uu_) \<Rightarrow> length pq); heapmap_\<alpha> (x1a, x2) = heapmap_\<alpha> hm; length x1a = (case hm of (pq, uu_) \<Rightarrow> length pq)\<rbrakk> \<Longrightarrow> REC\<^sub>T (\<lambda>D (h, k). ASSERT (0 < k \<and> k \<le> (case h of (pq, uu_) \<Rightarrow> length pq)) \<bind> (\<lambda>_. let len = case h of (pq, uu_) \<Rightarrow> length pq in if 2 * k \<le> len then let j = 2 * k in (case h of (pq, m) \<Rightarrow> \<lambda>i. ASSERT (0 < i) \<bind> (\<lambda>_. mop_list_get pq (i - 1))) j \<bind> (\<lambda>k. ASSERT (heapmap_\<alpha> h k \<noteq> None \<and> hmr_invar h) \<bind> (\<lambda>_. RETURN (the (heapmap_\<alpha> h k))) \<bind> RETURN) \<bind> (\<lambda>v. RETURN (prio v)) \<bind> (\<lambda>pj. (if j < len then (case h of (pq, m) \<Rightarrow> \<lambda>i. ASSERT (0 < i) \<bind> (\<lambda>_. mop_list_get pq (i - 1))) (Suc j) \<bind> (\<lambda>k. ASSERT (heapmap_\<alpha> h k \<noteq> None \<and> hmr_invar h) \<bind> (\<lambda>_. RETURN (the (heapmap_\<alpha> h k))) \<bind> RETURN) \<bind> (\<lambda>v. RETURN (prio v)) \<bind> (\<lambda>psj. if psj < pj then RETURN (j + 1) else RETURN j) else RETURN j) \<bind> (\<lambda>j. (case h of (pq, m) \<Rightarrow> \<lambda>i. ASSERT (0 < i) \<bind> (\<lambda>_. mop_list_get pq (i - 1))) j \<bind> (\<lambda>k. ASSERT (heapmap_\<alpha> h k \<noteq> None \<and> hmr_invar h) \<bind> (\<lambda>_. RETURN (the (heapmap_\<alpha> h k))) \<bind> RETURN) \<bind> (\<lambda>v. RETURN (prio v)) \<bind> (\<lambda>pj. (case h of (pq, m) \<Rightarrow> \<lambda>i. ASSERT (0 < i) \<bind> (\<lambda>_. mop_list_get pq (i - 1))) k \<bind> (\<lambda>k. ASSERT (heapmap_\<alpha> h k \<noteq> None \<and> hmr_invar h) \<bind> (\<lambda>_. RETURN (the (heapmap_\<alpha> h k))) \<bind> RETURN) \<bind> (\<lambda>v. RETURN (prio v)) \<bind> (\<lambda>pk. if pj < pk then (case h of (pq, m) \<Rightarrow> \<lambda>i j. ASSERT (hm_valid (pq, m) i) \<bind> (\<lambda>_. ASSERT (hm_valid (pq, m) j) \<bind> (\<lambda>_. ASSERT (hmr_invar (pq, m)) \<bind> (\<lambda>_. mop_list_swap pq (i - 1) (j - 1) \<bind> (\<lambda>pq. RETURN (pq, m)))))) k j \<bind> (\<lambda>h. D (h, j)) else RETURN h)))) else RETURN h)) ((swap x1a (x2b - Suc 0) (2 * x2b - Suc 0), x2), 2 * x2b) \<le>\<^sub>n SPEC (\<lambda>hm'. heapmap_\<alpha> hm' = heapmap_\<alpha> hm)
 4. \<And>x1a x2 x2b y ya. \<lbrakk>\<And>a b ba. \<lbrakk>0 < ba \<and> ba \<le> length a \<and> heapmap_\<alpha> (a, b) = heapmap_\<alpha> hm \<and> length a = (case hm of (pq, uu_) \<Rightarrow> length pq); (case hm of (pq, uu_) \<Rightarrow> length pq) - ba < (case hm of (pq, uu_) \<Rightarrow> length pq) - x2b\<rbrakk> \<Longrightarrow> REC\<^sub>T (\<lambda>D (h, k). ASSERT (0 < k \<and> k \<le> (case h of (pq, uu_) \<Rightarrow> length pq)) \<bind> (\<lambda>_. let len = case h of (pq, uu_) \<Rightarrow> length pq in if 2 * k \<le> len then let j = 2 * k in (case h of (pq, m) \<Rightarrow> \<lambda>i. ASSERT (0 < i) \<bind> (\<lambda>_. mop_list_get pq (i - 1))) j \<bind> (\<lambda>k. ASSERT (heapmap_\<alpha> h k \<noteq> None \<and> hmr_invar h) \<bind> (\<lambda>_. RETURN (the (heapmap_\<alpha> h k))) \<bind> RETURN) \<bind> (\<lambda>v. RETURN (prio v)) \<bind> (\<lambda>pj. (if j < len then (case h of (pq, m) \<Rightarrow> \<lambda>i. ASSERT (0 < i) \<bind> (\<lambda>_. mop_list_get pq (i - 1))) (Suc j) \<bind> (\<lambda>k. ASSERT (heapmap_\<alpha> h k \<noteq> None \<and> hmr_invar h) \<bind> (\<lambda>_. RETURN (the (heapmap_\<alpha> h k))) \<bind> RETURN) \<bind> (\<lambda>v. RETURN (prio v)) \<bind> (\<lambda>psj. if psj < pj then RETURN (j + 1) else RETURN j) else RETURN j) \<bind> (\<lambda>j. (case h of (pq, m) \<Rightarrow> \<lambda>i. ASSERT (0 < i) \<bind> (\<lambda>_. mop_list_get pq (i - 1))) j \<bind> (\<lambda>k. ASSERT (heapmap_\<alpha> h k \<noteq> None \<and> hmr_invar h) \<bind> (\<lambda>_. RETURN (the (heapmap_\<alpha> h k))) \<bind> RETURN) \<bind> (\<lambda>v. RETURN (prio v)) \<bind> (\<lambda>pj. (case h of (pq, m) \<Rightarrow> \<lambda>i. ASSERT (0 < i) \<bind> (\<lambda>_. mop_list_get pq (i - 1))) k \<bind> (\<lambda>k. ASSERT (heapmap_\<alpha> h k \<noteq> None \<and> hmr_invar h) \<bind> (\<lambda>_. RETURN (the (heapmap_\<alpha> h k))) \<bind> RETURN) \<bind> (\<lambda>v. RETURN (prio v)) \<bind> (\<lambda>pk. if pj < pk then (case h of (pq, m) \<Rightarrow> \<lambda>i j. ASSERT (hm_valid (pq, m) i) \<bind> (\<lambda>_. ASSERT (hm_valid (pq, m) j) \<bind> (\<lambda>_. ASSERT (hmr_invar (pq, m)) \<bind> (\<lambda>_. mop_list_swap pq (i - 1) (j - 1) \<bind> (\<lambda>pq. RETURN (pq, m)))))) k j \<bind> (\<lambda>h. D (h, j)) else RETURN h)))) else RETURN h)) ((a, b), ba) \<le>\<^sub>n SPEC (\<lambda>hm'. heapmap_\<alpha> hm' = heapmap_\<alpha> hm); 2 * x2b = (case hm of (pq, uu_) \<Rightarrow> length pq); x2b - Suc 0 < (case hm of (pq, uu_) \<Rightarrow> length pq); prio y < prio ya; hmr_invar (x1a, x2); heapmap_\<alpha> hm (x1a ! ((case hm of (pq, uu_) \<Rightarrow> length pq) - Suc 0)) = Some y; heapmap_\<alpha> hm (x1a ! (x2b - Suc 0)) = Some ya; 0 < i; i \<le> (case hm of (pq, uu_) \<Rightarrow> length pq); heapmap_\<alpha> (x1a, x2) = heapmap_\<alpha> hm; length x1a = (case hm of (pq, uu_) \<Rightarrow> length pq)\<rbrakk> \<Longrightarrow> REC\<^sub>T (\<lambda>D (h, k). ASSERT (0 < k \<and> k \<le> (case h of (pq, uu_) \<Rightarrow> length pq)) \<bind> (\<lambda>_. let len = case h of (pq, uu_) \<Rightarrow> length pq in if 2 * k \<le> len then let j = 2 * k in (case h of (pq, m) \<Rightarrow> \<lambda>i. ASSERT (0 < i) \<bind> (\<lambda>_. mop_list_get pq (i - 1))) j \<bind> (\<lambda>k. ASSERT (heapmap_\<alpha> h k \<noteq> None \<and> hmr_invar h) \<bind> (\<lambda>_. RETURN (the (heapmap_\<alpha> h k))) \<bind> RETURN) \<bind> (\<lambda>v. RETURN (prio v)) \<bind> (\<lambda>pj. (if j < len then (case h of (pq, m) \<Rightarrow> \<lambda>i. ASSERT (0 < i) \<bind> (\<lambda>_. mop_list_get pq (i - 1))) (Suc j) \<bind> (\<lambda>k. ASSERT (heapmap_\<alpha> h k \<noteq> None \<and> hmr_invar h) \<bind> (\<lambda>_. RETURN (the (heapmap_\<alpha> h k))) \<bind> RETURN) \<bind> (\<lambda>v. RETURN (prio v)) \<bind> (\<lambda>psj. if psj < pj then RETURN (j + 1) else RETURN j) else RETURN j) \<bind> (\<lambda>j. (case h of (pq, m) \<Rightarrow> \<lambda>i. ASSERT (0 < i) \<bind> (\<lambda>_. mop_list_get pq (i - 1))) j \<bind> (\<lambda>k. ASSERT (heapmap_\<alpha> h k \<noteq> None \<and> hmr_invar h) \<bind> (\<lambda>_. RETURN (the (heapmap_\<alpha> h k))) \<bind> RETURN) \<bind> (\<lambda>v. RETURN (prio v)) \<bind> (\<lambda>pj. (case h of (pq, m) \<Rightarrow> \<lambda>i. ASSERT (0 < i) \<bind> (\<lambda>_. mop_list_get pq (i - 1))) k \<bind> (\<lambda>k. ASSERT (heapmap_\<alpha> h k \<noteq> None \<and> hmr_invar h) \<bind> (\<lambda>_. RETURN (the (heapmap_\<alpha> h k))) \<bind> RETURN) \<bind> (\<lambda>v. RETURN (prio v)) \<bind> (\<lambda>pk. if pj < pk then (case h of (pq, m) \<Rightarrow> \<lambda>i j. ASSERT (hm_valid (pq, m) i) \<bind> (\<lambda>_. ASSERT (hm_valid (pq, m) j) \<bind> (\<lambda>_. ASSERT (hmr_invar (pq, m)) \<bind> (\<lambda>_. mop_list_swap pq (i - 1) (j - 1) \<bind> (\<lambda>pq. RETURN (pq, m)))))) k j \<bind> (\<lambda>h. D (h, j)) else RETURN h)))) else RETURN h)) ((swap x1a (x2b - Suc 0) ((case hm of (pq, uu_) \<Rightarrow> length pq) - Suc 0), x2), case hm of (pq, uu_) \<Rightarrow> length pq) \<le>\<^sub>n SPEC (\<lambda>hm'. heapmap_\<alpha> hm' = heapmap_\<alpha> hm)
[PROOF STEP]
apply (vc_solve simp: heapmap_\<alpha>_def h.parent_def split: prod.splits)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x1a x2b y ya yb x1 x2a. \<lbrakk>2 * x2b < length x1; prio ya < prio y; 0 < x2b; x2b - Suc 0 < length x1; prio ya < prio yb; hmr_invar (x1a, x2a); x2a (x1a ! (2 * x2b - Suc 0)) = Some y; x2a (x1a ! (2 * x2b)) = Some ya; x2a (x1a ! (x2b - Suc 0)) = Some yb; 0 < i; i \<le> length x1; length x1a = length x1; hm = (x1, x2a); 2 * x2b - Suc 0 < length x1\<rbrakk> \<Longrightarrow> length x1 - Suc (2 * x2b) < length x1 - x2b
[PROOF STEP]
apply (auto)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma hm_repair_op_refine: "(hm_repair_op, h.repair_op) \<in> hmr_rel \<rightarrow> nat_rel \<rightarrow> \<langle>hmr_rel\<rangle>nres_rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (hm_repair_op, h.repair_op) \<in> hmr_rel \<rightarrow> nat_rel \<rightarrow> \<langle>hmr_rel\<rangle>nres_rel
[PROOF STEP]
apply (intro fun_relI nres_relI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a a' aa a'a. \<lbrakk>(a, a') \<in> hmr_rel; (aa, a'a) \<in> nat_rel\<rbrakk> \<Longrightarrow> hm_repair_op a aa \<le> \<Down> hmr_rel (h.repair_op a' a'a)
[PROOF STEP]
unfolding hm_repair_op_def h.repair_op_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a a' aa a'a. \<lbrakk>(a, a') \<in> hmr_rel; (aa, a'a) \<in> nat_rel\<rbrakk> \<Longrightarrow> hm_sink_op a aa \<bind> (\<lambda>hm. hm_swim_op hm aa \<bind> RETURN) \<le> \<Down> hmr_rel (h.sink_op a' a'a \<bind> (\<lambda>h. h.swim_op h a'a \<bind> RETURN))
[PROOF STEP]
by refine_rcg


[STATEMENT]
lemma hm_repair_op_\<alpha>_correct: "hm_repair_op hm i \<le>\<^sub>n SPEC (\<lambda>hm'. heapmap_\<alpha> hm' = heapmap_\<alpha> hm)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hm_repair_op hm i \<le>\<^sub>n SPEC (\<lambda>hm'. heapmap_\<alpha> hm' = heapmap_\<alpha> hm)
[PROOF STEP]
unfolding hm_repair_op_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hm_sink_op hm i \<bind> (\<lambda>hm. hm_swim_op hm i \<bind> RETURN) \<le>\<^sub>n SPEC (\<lambda>hm'. heapmap_\<alpha> hm' = heapmap_\<alpha> hm)
[PROOF STEP]
apply (refine_vcg
        hm_swim_op_\<alpha>_correct[THEN leof_trans]
        hm_sink_op_\<alpha>_correct[THEN leof_trans])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>x \<in> {hm'. heapmap_\<alpha> hm' = heapmap_\<alpha> hm}; xa \<in> {hm'. heapmap_\<alpha> hm' = heapmap_\<alpha> x}\<rbrakk> \<Longrightarrow> heapmap_\<alpha> xa = heapmap_\<alpha> hm
[PROOF STEP]
by auto


[STATEMENT]
lemma hm_empty_aref: "(hm_empty_op,RETURN op_map_empty) \<in> \<langle>heapmap_rel\<rangle>nres_rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (hm_empty_op, RETURN op_map_empty) \<in> \<langle>heapmap_rel\<rangle>nres_rel
[PROOF STEP]
unfolding hm_empty_op_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (RETURN ([], Map.empty), RETURN op_map_empty) \<in> \<langle>heapmap_rel\<rangle>nres_rel
[PROOF STEP]
by (auto simp: heapmap_rel_defs hmr_rel_defs intro: nres_relI)


[STATEMENT]
lemma hm_insert_op_refine[refine]: "\<lbrakk> heapmap_\<alpha> hm k = None; (hm,h)\<in>hmr_rel \<rbrakk> \<Longrightarrow>
      hm_insert_op k v hm \<le> \<Down>hmr_rel (h.insert_op v h)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>heapmap_\<alpha> hm k = None; (hm, h) \<in> hmr_rel\<rbrakk> \<Longrightarrow> hm_insert_op k v hm \<le> \<Down> hmr_rel (h.insert_op v h)
[PROOF STEP]
unfolding hm_insert_op_def h.insert_op_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>heapmap_\<alpha> hm k = None; (hm, h) \<in> hmr_rel\<rbrakk> \<Longrightarrow> ASSERT (h.heap_invar (hmr_\<alpha> hm)) \<bind> (\<lambda>_. hm_append_op hm k v \<bind> (\<lambda>h. let l = hm_length h in hm_swim_op h l \<bind> RETURN)) \<le> \<Down> hmr_rel (ASSERT (h.heap_invar h) \<bind> (\<lambda>_. h.append_op h v \<bind> (\<lambda>h. let l = length h in h.swim_op h l \<bind> RETURN)))
[PROOF STEP]
apply refine_rcg
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>heapmap_\<alpha> hm k = None; (hm, h) \<in> hmr_rel; h.heap_invar h\<rbrakk> \<Longrightarrow> h.heap_invar (hmr_\<alpha> hm)
[PROOF STEP]
by (auto simp: hmr_rel_def br_def)


[STATEMENT]
lemma hm_insert_op_aref:
      "(hm_insert_op,mop_map_update_new) \<in> Id \<rightarrow> Id \<rightarrow> heapmap_rel \<rightarrow> \<langle>heapmap_rel\<rangle>nres_rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (hm_insert_op, mop_map_update_new) \<in> Id \<rightarrow> Id \<rightarrow> heapmap_rel \<rightarrow> \<langle>heapmap_rel\<rangle>nres_rel
[PROOF STEP]
apply (intro fun_relI nres_relI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a a' aa a'a ab a'b. \<lbrakk>(a, a') \<in> Id; (aa, a'a) \<in> Id; (ab, a'b) \<in> heapmap_rel\<rbrakk> \<Longrightarrow> hm_insert_op a aa ab \<le> \<Down> heapmap_rel (mop_map_update_new a' a'a a'b)
[PROOF STEP]
unfolding mop_map_update_new_alt
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a a' aa a'a ab a'b. \<lbrakk>(a, a') \<in> Id; (aa, a'a) \<in> Id; (ab, a'b) \<in> heapmap_rel\<rbrakk> \<Longrightarrow> hm_insert_op a aa ab \<le> \<Down> heapmap_rel (ASSERT (pre_map_update_new ((a', a'a), a'b)) \<bind> (\<lambda>_. RETURN (op_map_update_new a' a'a a'b)))
[PROOF STEP]
apply (rule ASSERT_refine_right)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a a' aa a'a ab a'b. \<lbrakk>(a, a') \<in> Id; (aa, a'a) \<in> Id; (ab, a'b) \<in> heapmap_rel; pre_map_update_new ((a', a'a), a'b)\<rbrakk> \<Longrightarrow> hm_insert_op a aa ab \<le> \<Down> heapmap_rel (RETURN (op_map_update_new a' a'a a'b))
[PROOF STEP]
apply (rule heapmap_nres_relI''[OF hm_insert_op_refine h.insert_op_correct])
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>a a' aa a'a ab a'b. \<lbrakk>(a, a') \<in> Id; (aa, a'a) \<in> Id; (ab, a'b) \<in> heapmap_rel; pre_map_update_new ((a', a'a), a'b)\<rbrakk> \<Longrightarrow> heapmap_\<alpha> ab a = None
 2. \<And>a a' aa a'a ab a'b. \<lbrakk>(a, a') \<in> Id; (aa, a'a) \<in> Id; (ab, a'b) \<in> heapmap_rel; pre_map_update_new ((a', a'a), a'b)\<rbrakk> \<Longrightarrow> (ab, ?h7 a a' aa a'a ab a'b) \<in> hmr_rel
 3. \<And>a a' aa a'a ab a'b. \<lbrakk>(a, a') \<in> Id; (aa, a'a) \<in> Id; (ab, a'b) \<in> heapmap_rel; pre_map_update_new ((a', a'a), a'b)\<rbrakk> \<Longrightarrow> h.heap_invar (?h7 a a' aa a'a ab a'b)
 4. \<And>a a' aa a'a ab a'b h'. \<lbrakk>(a, a') \<in> Id; (aa, a'a) \<in> Id; (ab, a'b) \<in> heapmap_rel; pre_map_update_new ((a', a'a), a'b); h.heap_invar h' \<and> h.\<alpha> h' = h.\<alpha> (?h7 a a' aa a'a ab a'b) + {#aa#}\<rbrakk> \<Longrightarrow> h.heap_invar h'
 5. \<And>a a' aa a'a ab a'b. \<lbrakk>(a, a') \<in> Id; (aa, a'a) \<in> Id; (ab, a'b) \<in> heapmap_rel; pre_map_update_new ((a', a'a), a'b)\<rbrakk> \<Longrightarrow> hm_insert_op a aa ab \<le>\<^sub>n SPEC (\<lambda>hm'. RETURN (heapmap_\<alpha> hm') \<le> RETURN (op_map_update_new a' a'a a'b))
[PROOF STEP]
apply (unfold heapmap_rel_def in_br_conv; clarsimp)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>a a' aa a'a ab a'b. \<lbrakk>(a, a') \<in> Id; (aa, a'a) \<in> Id; (ab, a'b) \<in> heapmap_rel; pre_map_update_new ((a', a'a), a'b)\<rbrakk> \<Longrightarrow> (ab, ?h7 a a' aa a'a ab a'b) \<in> hmr_rel
 2. \<And>a a' aa a'a ab a'b. \<lbrakk>(a, a') \<in> Id; (aa, a'a) \<in> Id; (ab, a'b) \<in> heapmap_rel; pre_map_update_new ((a', a'a), a'b)\<rbrakk> \<Longrightarrow> h.heap_invar (?h7 a a' aa a'a ab a'b)
 3. \<And>a a' aa a'a ab a'b h'. \<lbrakk>(a, a') \<in> Id; (aa, a'a) \<in> Id; (ab, a'b) \<in> heapmap_rel; pre_map_update_new ((a', a'a), a'b); h.heap_invar h' \<and> h.\<alpha> h' = h.\<alpha> (?h7 a a' aa a'a ab a'b) + {#aa#}\<rbrakk> \<Longrightarrow> h.heap_invar h'
 4. \<And>a a' aa a'a ab a'b. \<lbrakk>(a, a') \<in> Id; (aa, a'a) \<in> Id; (ab, a'b) \<in> heapmap_rel; pre_map_update_new ((a', a'a), a'b)\<rbrakk> \<Longrightarrow> hm_insert_op a aa ab \<le>\<^sub>n SPEC (\<lambda>hm'. RETURN (heapmap_\<alpha> hm') \<le> RETURN (op_map_update_new a' a'a a'b))
[PROOF STEP]
apply (erule heapmap_hmr_relI)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>a a' aa a'a ab a'b. \<lbrakk>(a, a') \<in> Id; (aa, a'a) \<in> Id; (ab, a'b) \<in> heapmap_rel; pre_map_update_new ((a', a'a), a'b)\<rbrakk> \<Longrightarrow> h.heap_invar (hmr_\<alpha> ab)
 2. \<And>a a' aa a'a ab a'b h'. \<lbrakk>(a, a') \<in> Id; (aa, a'a) \<in> Id; (ab, a'b) \<in> heapmap_rel; pre_map_update_new ((a', a'a), a'b); h.heap_invar h' \<and> h.\<alpha> h' = h.\<alpha> (hmr_\<alpha> ab) + {#aa#}\<rbrakk> \<Longrightarrow> h.heap_invar h'
 3. \<And>a a' aa a'a ab a'b. \<lbrakk>(a, a') \<in> Id; (aa, a'a) \<in> Id; (ab, a'b) \<in> heapmap_rel; pre_map_update_new ((a', a'a), a'b)\<rbrakk> \<Longrightarrow> hm_insert_op a aa ab \<le>\<^sub>n SPEC (\<lambda>hm'. RETURN (heapmap_\<alpha> hm') \<le> RETURN (op_map_update_new a' a'a a'b))
[PROOF STEP]
apply (unfold heapmap_rel_def in_br_conv; clarsimp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a a' aa a'a ab a'b h'. \<lbrakk>(a, a') \<in> Id; (aa, a'a) \<in> Id; (ab, a'b) \<in> heapmap_rel; pre_map_update_new ((a', a'a), a'b); h.heap_invar h' \<and> h.\<alpha> h' = h.\<alpha> (hmr_\<alpha> ab) + {#aa#}\<rbrakk> \<Longrightarrow> h.heap_invar h'
 2. \<And>a a' aa a'a ab a'b. \<lbrakk>(a, a') \<in> Id; (aa, a'a) \<in> Id; (ab, a'b) \<in> heapmap_rel; pre_map_update_new ((a', a'a), a'b)\<rbrakk> \<Longrightarrow> hm_insert_op a aa ab \<le>\<^sub>n SPEC (\<lambda>hm'. RETURN (heapmap_\<alpha> hm') \<le> RETURN (op_map_update_new a' a'a a'b))
[PROOF STEP]
apply (unfold heapmap_rel_def in_br_conv; clarsimp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a a' aa a'a ab a'b. \<lbrakk>(a, a') \<in> Id; (aa, a'a) \<in> Id; (ab, a'b) \<in> heapmap_rel; pre_map_update_new ((a', a'a), a'b)\<rbrakk> \<Longrightarrow> hm_insert_op a aa ab \<le>\<^sub>n SPEC (\<lambda>hm'. RETURN (heapmap_\<alpha> hm') \<le> RETURN (op_map_update_new a' a'a a'b))
[PROOF STEP]
unfolding hm_insert_op_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a a' aa a'a ab a'b. \<lbrakk>(a, a') \<in> Id; (aa, a'a) \<in> Id; (ab, a'b) \<in> heapmap_rel; pre_map_update_new ((a', a'a), a'b)\<rbrakk> \<Longrightarrow> ASSERT (h.heap_invar (hmr_\<alpha> ab)) \<bind> (\<lambda>_. hm_append_op ab a aa \<bind> (\<lambda>h. let l = hm_length h in hm_swim_op h l \<bind> RETURN)) \<le>\<^sub>n SPEC (\<lambda>hm'. RETURN (heapmap_\<alpha> hm') \<le> RETURN (op_map_update_new a' a'a a'b))
[PROOF STEP]
apply (refine_vcg
        hm_append_op_\<alpha>_correct[THEN leof_trans]
        hm_swim_op_\<alpha>_correct[THEN leof_trans])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a a' aa a'a ab a'b x xa. \<lbrakk>(a, a') \<in> Id; (aa, a'a) \<in> Id; (ab, a'b) \<in> heapmap_rel; pre_map_update_new ((a', a'a), a'b); h.heap_invar (hmr_\<alpha> ab); x \<in> {hm'. heapmap_\<alpha> hm' = heapmap_\<alpha> ab(a \<mapsto> aa)}; xa \<in> {hm'. heapmap_\<alpha> hm' = heapmap_\<alpha> x}\<rbrakk> \<Longrightarrow> op_map_update_new a' a'a a'b = heapmap_\<alpha> xa
[PROOF STEP]
apply (unfold heapmap_rel_def in_br_conv; clarsimp)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma hmr_\<alpha>_empty_iff[simp]:
      "hmr_invar hm \<Longrightarrow> hmr_\<alpha> hm = [] \<longleftrightarrow> heapmap_\<alpha> hm = Map.empty"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hmr_invar hm \<Longrightarrow> (hmr_\<alpha> hm = []) = (heapmap_\<alpha> hm = Map.empty)
[PROOF STEP]
by (auto
        simp: hmr_\<alpha>_def heapmap_invar_def heapmap_\<alpha>_def hmr_invar_def
        split: prod.split)


[STATEMENT]
lemma hm_is_empty_op_refine: "(hm_is_empty_op, h.is_empty_op) \<in> hmr_rel \<rightarrow> \<langle>bool_rel\<rangle>nres_rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (hm_is_empty_op, h.is_empty_op) \<in> hmr_rel \<rightarrow> \<langle>bool_rel\<rangle>nres_rel
[PROOF STEP]
apply (intro fun_relI nres_relI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a a'. (a, a') \<in> hmr_rel \<Longrightarrow> hm_is_empty_op a \<le> \<Down> bool_rel (h.is_empty_op a')
[PROOF STEP]
unfolding hm_is_empty_op_def h.is_empty_op_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a a'. (a, a') \<in> hmr_rel \<Longrightarrow> ASSERT (hmr_invar a) \<bind> (\<lambda>_. let l = hm_length a in RETURN (l = 0)) \<le> \<Down> bool_rel (ASSERT (h.heap_invar a') \<bind> (\<lambda>_. let l = length a' in RETURN (l = 0)))
[PROOF STEP]
apply refine_rcg
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a a'. \<lbrakk>(a, a') \<in> hmr_rel; h.heap_invar a'\<rbrakk> \<Longrightarrow> hmr_invar a
 2. \<And>a a'. \<lbrakk>(a, a') \<in> hmr_rel; h.heap_invar a'; hmr_invar a\<rbrakk> \<Longrightarrow> (hm_length a = 0, length a' = 0) \<in> bool_rel
[PROOF STEP]
apply (auto simp: hmr_rel_defs) []
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a a'. \<lbrakk>(a, a') \<in> hmr_rel; h.heap_invar a'; hmr_invar a\<rbrakk> \<Longrightarrow> (hm_length a = 0, length a' = 0) \<in> bool_rel
[PROOF STEP]
apply (parametricity add: hm_length_refine)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma hm_is_empty_op_aref: "(hm_is_empty_op, RETURN o op_map_is_empty) \<in> heapmap_rel \<rightarrow> \<langle>bool_rel\<rangle>nres_rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (hm_is_empty_op, RETURN \<circ> op_map_is_empty) \<in> heapmap_rel \<rightarrow> \<langle>bool_rel\<rangle>nres_rel
[PROOF STEP]
apply (intro fun_relI nres_relI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a a'. (a, a') \<in> heapmap_rel \<Longrightarrow> hm_is_empty_op a \<le> \<Down> bool_rel ((RETURN \<circ> op_map_is_empty) a')
[PROOF STEP]
unfolding hm_is_empty_op_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a a'. (a, a') \<in> heapmap_rel \<Longrightarrow> ASSERT (hmr_invar a) \<bind> (\<lambda>_. let l = hm_length a in RETURN (l = 0)) \<le> \<Down> bool_rel ((RETURN \<circ> op_map_is_empty) a')
[PROOF STEP]
apply refine_vcg
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a a'. (a, a') \<in> heapmap_rel \<Longrightarrow> hmr_invar a
 2. \<And>a a'. \<lbrakk>(a, a') \<in> heapmap_rel; hmr_invar a\<rbrakk> \<Longrightarrow> RETURN (hm_length a = 0) \<le> \<Down> bool_rel ((RETURN \<circ> op_map_is_empty) a')
[PROOF STEP]
apply (auto simp: hmr_rel_defs heapmap_rel_defs hm_length_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma hm_lookup_op_aref: "(hm_lookup_op,RETURN oo op_map_lookup) \<in> Id \<rightarrow> heapmap_rel \<rightarrow> \<langle>\<langle>Id\<rangle>option_rel\<rangle>nres_rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (hm_lookup_op, RETURN \<circ>\<circ> op_map_lookup) \<in> Id \<rightarrow> heapmap_rel \<rightarrow> \<langle>\<langle>Id\<rangle>option_rel\<rangle>nres_rel
[PROOF STEP]
apply (intro fun_relI nres_relI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a a' aa a'a. \<lbrakk>(a, a') \<in> Id; (aa, a'a) \<in> heapmap_rel\<rbrakk> \<Longrightarrow> hm_lookup_op a aa \<le> \<Down> (\<langle>Id\<rangle>option_rel) ((RETURN \<circ>\<circ> op_map_lookup) a' a'a)
[PROOF STEP]
unfolding hm_lookup_op_def heapmap_rel_def in_br_conv
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a a' aa a'a. \<lbrakk>(a, a') \<in> Id; a'a = heapmap_\<alpha> aa \<and> heapmap_invar aa\<rbrakk> \<Longrightarrow> ASSERT (heapmap_invar aa) \<bind> (\<lambda>_. RETURN (heapmap_\<alpha> aa a)) \<le> \<Down> (\<langle>Id\<rangle>option_rel) ((RETURN \<circ>\<circ> op_map_lookup) a' a'a)
[PROOF STEP]
apply refine_vcg
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a a' aa a'a. \<lbrakk>(a, a') \<in> Id; a'a = heapmap_\<alpha> aa \<and> heapmap_invar aa\<rbrakk> \<Longrightarrow> heapmap_invar aa
 2. \<And>a a' aa a'a. \<lbrakk>(a, a') \<in> Id; a'a = heapmap_\<alpha> aa \<and> heapmap_invar aa; heapmap_invar aa\<rbrakk> \<Longrightarrow> RETURN (heapmap_\<alpha> aa a) \<le> \<Down> (\<langle>Id\<rangle>option_rel) ((RETURN \<circ>\<circ> op_map_lookup) a' a'a)
[PROOF STEP]
apply simp_all
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma hm_contains_key_op_aref: "(hm_contains_key_op,RETURN oo op_map_contains_key) \<in> Id \<rightarrow> heapmap_rel \<rightarrow> \<langle>bool_rel\<rangle>nres_rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (hm_contains_key_op, RETURN \<circ>\<circ> op_map_contains_key) \<in> Id \<rightarrow> heapmap_rel \<rightarrow> \<langle>bool_rel\<rangle>nres_rel
[PROOF STEP]
apply (intro fun_relI nres_relI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a a' aa a'a. \<lbrakk>(a, a') \<in> Id; (aa, a'a) \<in> heapmap_rel\<rbrakk> \<Longrightarrow> hm_contains_key_op a aa \<le> \<Down> bool_rel ((RETURN \<circ>\<circ> op_map_contains_key) a' a'a)
[PROOF STEP]
unfolding hm_contains_key_op_def heapmap_rel_defs
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a a' aa a'a. \<lbrakk>(a, a') \<in> Id; (aa, a'a) \<in> {(c, a). a = (case c of (pq, m) \<Rightarrow> m) \<and> hmr_invar c \<and> h.heap_invar (hmr_\<alpha> c)}\<rbrakk> \<Longrightarrow> (case aa of (pq, m) \<Rightarrow> ASSERT (hmr_invar (pq, m) \<and> h.heap_invar (hmr_\<alpha> (pq, m))) \<bind> (\<lambda>_. RETURN (a \<in> dom m))) \<le> \<Down> bool_rel ((RETURN \<circ>\<circ> op_map_contains_key) a' a'a)
[PROOF STEP]
apply refine_vcg
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>a a' aa a'a x1 x2. \<lbrakk>(a, a') \<in> Id; (aa, a'a) \<in> {(c, a). a = (case c of (pq, m) \<Rightarrow> m) \<and> hmr_invar c \<and> h.heap_invar (hmr_\<alpha> c)}; aa = (x1, x2)\<rbrakk> \<Longrightarrow> hmr_invar (x1, x2)
 2. \<And>a a' aa a'a x1 x2. \<lbrakk>(a, a') \<in> Id; (aa, a'a) \<in> {(c, a). a = (case c of (pq, m) \<Rightarrow> m) \<and> hmr_invar c \<and> h.heap_invar (hmr_\<alpha> c)}; aa = (x1, x2)\<rbrakk> \<Longrightarrow> h.heap_invar (hmr_\<alpha> (x1, x2))
 3. \<And>a a' aa a'a x1 x2. \<lbrakk>(a, a') \<in> Id; (aa, a'a) \<in> {(c, a). a = (case c of (pq, m) \<Rightarrow> m) \<and> hmr_invar c \<and> h.heap_invar (hmr_\<alpha> c)}; aa = (x1, x2); hmr_invar (x1, x2) \<and> h.heap_invar (hmr_\<alpha> (x1, x2))\<rbrakk> \<Longrightarrow> RETURN (a \<in> dom x2) \<le> \<Down> bool_rel ((RETURN \<circ>\<circ> op_map_contains_key) a' a'a)
[PROOF STEP]
by (auto)


[STATEMENT]
lemma (in heapstruct) decrease_key_op_invar:
      "\<lbrakk>heap_invar h; valid h i; prio v \<le> prio_of h i\<rbrakk> \<Longrightarrow> decrease_key_op i v h \<le> SPEC heap_invar"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>heap_invar h; valid h i; prio v \<le> prio_of h i\<rbrakk> \<Longrightarrow> decrease_key_op i v h \<le> SPEC heap_invar
[PROOF STEP]
unfolding decrease_key_op_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>heap_invar h; valid h i; prio v \<le> prio_of h i\<rbrakk> \<Longrightarrow> ASSERT (valid h i \<and> prio v \<le> prio_of h i) \<bind> (\<lambda>_. update_op h i v \<bind> (\<lambda>h. swim_op h i)) \<le> SPEC heap_invar
[PROOF STEP]
apply refine_vcg
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>heap_invar h; valid h i; prio v \<le> prio_of h i; valid h i \<and> prio v \<le> prio_of h i; x = update h i v\<rbrakk> \<Longrightarrow> swim_invar x i
 2. \<And>x xa. \<lbrakk>heap_invar h; valid h i; prio v \<le> prio_of h i; valid h i \<and> prio v \<le> prio_of h i; x = update h i v; \<alpha> xa = \<alpha> x \<and> heap_invar xa \<and> length xa = length x\<rbrakk> \<Longrightarrow> heap_invar xa
[PROOF STEP]
by (auto simp: swim_invar_decr)


[STATEMENT]
lemma index_op_inline_refine:
      assumes "heapmap_invar hm"
      assumes "heapmap_\<alpha> hm k \<noteq> None"
      assumes "f (hm_index hm k) \<le> m"
      shows "do {i \<leftarrow> hm_index_op hm k; f i} \<le> m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hm_index_op hm k \<bind> f \<le> m
[PROOF STEP]
using hm_index_op_correct[of hm k] assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>hmr_invar hm; heapmap_\<alpha> hm k \<noteq> None\<rbrakk> \<Longrightarrow> hm_index_op hm k \<le> SPEC (\<lambda>r. r = hm_index hm k)
heapmap_invar hm
heapmap_\<alpha> hm k \<noteq> None
f (hm_index hm k) \<le> m

goal (1 subgoal):
 1. hm_index_op hm k \<bind> f \<le> m
[PROOF STEP]
by (auto simp: pw_le_iff refine_pw_simps)