[STATEMENT]
lemma hm_valid_refine: "(hm_valid,h.valid)\<in>hmr_rel \<rightarrow> nat_rel \<rightarrow> bool_rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (hm_valid, h.valid) \<in> hmr_rel \<rightarrow> nat_rel \<rightarrow> bool_rel
[PROOF STEP]
apply (intro fun_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_valid a aa, h.valid a' a'a) \<in> bool_rel
[PROOF STEP]
unfolding hm_valid_def h.valid_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> (0 < aa \<and> aa \<le> hm_length a, 0 < a'a \<and> a'a \<le> length a') \<in> bool_rel
[PROOF STEP]
by (parametricity add: hm_length_refine)