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