[STATEMENT]
lemma optim_instrs_length:
  assumes "optim_instrs F ret pc \<Sigma>i xs = Some (\<Sigma>o, ys)"
  shows "length xs = length ys"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length xs = length ys
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
optim_instrs F ret pc \<Sigma>i xs = Some (\<Sigma>o, ys)

goal (1 subgoal):
 1. length xs = length ys
[PROOF STEP]
unfolding optim_instrs_def
[PROOF STATE]
proof (prove)
using this:
map_option (case_prod (\<lambda>(uu_, y). Pair y)) (monadic_fold_map (\<lambda>(pc, \<Sigma>) instr. map_option (\<lambda>(instr', \<Sigma>o). ((Suc pc, \<Sigma>o), instr')) (optim_instr F ret pc instr \<Sigma>)) (pc, \<Sigma>i) xs) = Some (\<Sigma>o, ys)

goal (1 subgoal):
 1. length xs = length ys
[PROOF STEP]
by (auto intro: monadic_fold_map_length)