proposition: Theorem oc_eventProb_0_1 : forall (S : Set)(count : S -> nat)(evt : S -> bool)(k : nat -> Rat) (A B C : Set)(c : OracleComp A B C) n, queries_at_most c n -> forall (eqds : EqDec S)(o : S -> A -> Comp (B * S)) (s : S), (forall (n1 n2 : nat), (n1 <= n2)%nat -> (k n1 <= k n2)) -> evt s = false -> (forall s a, evt s = false -> Pr[p <-$ o s a; ret (evt (snd p))] <= (k (1 + (count s))%nat)) -> (forall s s' a b, In (b, s') (getSupport (o s a)) -> count s' <= 1 + (count s))%nat -> count s = 0%nat -> Pr[p <-$ c _ _ o s; ret (evt (snd p))] <= (n / 1) * (k n).
proof: Proof. intuition. eapply leRat_trans. eapply oc_eventProb; intuition. eauto. rewrite H4. rewrite Nat.mul_1_l. rewrite Nat.add_0_r. intuition. Qed.
imports: FCF.FCF