fact: Fixpoint evalDist_OC(A B C: Set)(c : OracleComp A B C): forall(S : Set), EqDec S -> (S -> A -> Comp (B * S)) -> S -> Comp (C * S) := match c in (OracleComp A B C) return (forall(S : Set), EqDec S -> (S -> A -> Comp (B * S)) -> S -> Comp (C * S)) with | @OC_Query A' B' a => fun (S : Set)(eqds : EqDec S)(o : S -> A' -> Comp (B' * S))(s : S) => o s a | @OC_Run A'' B'' C' A' B' S' eqds' eqda'' eqdb'' c' o' s' => fun (S : Set)(eqds : EqDec S)(o : S -> A' -> Comp (B' * S))(s : S) => p <-$ evalDist_OC c' (pair_EqDec eqds' eqds) (fun x y => p <-$ evalDist_OC (o' (fst x) y) _ o (snd x); ret (fst (fst p), (snd (fst p), snd p))) (s', s); Ret (EqDec_dec (pair_EqDec (pair_EqDec (oc_EqDec c' (fun x => fst (oc_base_exists (o' s' x) (fun y => fst (comp_base_exists (o s y))))) (fun x => EqDec_pair_l (oc_EqDec (o' s' x) (fun y => fst (comp_base_exists (o s y))) (fun y => EqDec_pair_l (comp_EqDec (o s y)) s)) s' )) _) _ )) (fst p, fst (snd p), snd (snd p)) | @OC_Ret A' B' C' c => fun (S : Set)(eqds : EqDec S)(o : S -> A' -> Comp (B' * S))(s : S) => x <-$ c; Ret (EqDec_dec (pair_EqDec (comp_EqDec c) _ )) (x, s) | @OC_Bind A' B' C' C'' c' f' => fun (S : Set)(eqds : EqDec S)(o : S -> A' -> Comp (B' * S))(s : S) => [z, s'] <-$2 evalDist_OC c' _ o s; evalDist_OC (f' z) _ o s' end.
imports: FCF.Comp FCF.Rat FCF.Fold List FCF.Blist micromega.Lia FCF.StdNat FCF.NotationV1 FCF.EqDec