[STATEMENT]
lemma heapmap_nres_rel_prodI:
      assumes "hmx \<le> \<Down>(UNIV \<times>\<^sub>r hmr_rel) h'x"
      assumes "h'x \<le> SPEC (\<lambda>(_,h'). h.heap_invar h')"
      assumes "hmx \<le>\<^sub>n SPEC (\<lambda>(r,hm'). RETURN (r,heapmap_\<alpha> hm') \<le> \<Down>(R\<times>\<^sub>rId) hx)"
      shows "hmx \<le> \<Down>(R\<times>\<^sub>rheapmap_rel) hx"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hmx \<le> \<Down> (R \<times>\<^sub>r heapmap_rel) hx
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
hmx \<le> \<Down> (UNIV \<times>\<^sub>r hmr_rel) h'x
h'x \<le> SPEC (\<lambda>(uu_, y). h.heap_invar y)
hmx \<le>\<^sub>n SPEC (\<lambda>(r, hm'). RETURN (r, heapmap_\<alpha> hm') \<le> \<Down> (R \<times>\<^sub>r Id) hx)

goal (1 subgoal):
 1. hmx \<le> \<Down> (R \<times>\<^sub>r heapmap_rel) hx
[PROOF STEP]
unfolding heapmap_rel_def hmr_rel_def br_def heapmap_invar_def
[PROOF STATE]
proof (prove)
using this:
hmx \<le> \<Down> (UNIV \<times>\<^sub>r {(c, a). a = hmr_\<alpha> c \<and> hmr_invar c}) h'x
h'x \<le> SPEC (\<lambda>(uu_, y). h.heap_invar y)
hmx \<le>\<^sub>n SPEC (\<lambda>(r, hm'). RETURN (r, heapmap_\<alpha> hm') \<le> \<Down> (R \<times>\<^sub>r Id) hx)

goal (1 subgoal):
 1. hmx \<le> \<Down> (R \<times>\<^sub>r {(c, a). a = heapmap_\<alpha> c \<and> hmr_invar c \<and> h.heap_invar (hmr_\<alpha> c)}) hx
[PROOF STEP]
apply (auto simp: pw_le_iff pw_leof_iff refine_pw_simps; blast)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done