proposition: Theorem mixed_fixed_point : forall I A B {IB:Inhab B} (M:family I B) (E:binary B) (P:A->Prop) (F:(A->B)->(A->B)) (R:binary A) (S:I->A->B->Prop), COFE M -> wf R -> E = similar M -> mixed_continuous M S -> mixed_contractive M P F R S -> exists (f:A->B), partial_fixed_point E F (Build_partial f P) /\ (forall i x, P x -> S i x (f x)).
proof: Proof. Proof using. introv IB Cofe WfR SimE Conti Contr. forwards (f&Fixf&Qf): (@cofe_fixed_point (I*A) (A->B) _ (corec_rec_family M P R) F (fun p f => let (i,x) := p in P x -> S i x (f x))). apply~ corec_rec_cofe. introv Limu Qiui. unfolds in Limu. simpls. intros [i x] Kix Px. applys Conti. apply~ (Qiui (i,x)). intros j Rji. apply~ (>> Limu Kix j x). apply~ mixed_contractive_as_contractive. exists (Build_partial f P). destruct Fixf as [Fixf _]. split. unfold partial_fixed_point. simpl. rewrite corec_rec_similar in Fixf. rewrite SimE. apply Fixf. intros. apply~ (Qf (i,x)). Qed.
imports: TLC(LibTactics LibLogic LibReflect LibEpsilon LibInt LibProd LibSum LibOperation LibRelation LibWf LibOrder LibMin)