[STATEMENT]
lemma load_size:
  "(load m n off l = None) = (mem_size m < (off + n + l))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (load m n off l = None) = (mem_size m < off + n + l)
[PROOF STEP]
unfolding load_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((if n + off + l \<le> mem_size m then Some (read_bytes m (n + off) l) else None) = None) = (mem_size m < off + n + l)
[PROOF STEP]
by (cases "n + off + l \<le> mem_size m") auto