fact: Definition fp (l:ab_env)(b:bexpr)(i:instr) (f:ab_env->a_instr*option ab_env):= match fp2 l l b i f with found i' l' => (i', l') | cont l' => match fp2 l l' b i f with found i'' l'' => (i'', l'') | cont l'' => let l := widen2 l in match fp1 l l b i f with (i, Some _) => (i, Some l) | (i, None) => (i, None) end end end.
imports: syntax little denot Bool List String ZArith axiom