proposition: Lemma phi_terminates_n : forall (A:Type) (t:A->option bool) f r r', phi t f r = Some r' -> exists n, iter _ (F_phi A t f) n (fun g => None) r = Some r'.
proof: Proof. intros A t f r r' Heq. assert (Hlub : lub (f_order' A) (phi t f) (fun n => iter _ (F_phi A t f) n (fun x : A => None))). apply least_fixpoint_lub_iterates; auto. intros g x; apply option_cpo_none_bot. unfold f_order'; apply F_phi_continuous. unfold phi, F_phi, f_order'; apply Tarski_fix_prop. exact (F_phi_continuous A t f). apply (lub_some_witness _ _ _ r r' (phi t f) Heq Hlub). Qed.
imports: Relations ClassicalEpsilon function_cpo constructs syntax little