proposition: Theorem qam_count : forall (A B C : Set)(c : OracleComp A B C)(q : nat), queries_at_most c q -> forall (S : Set)(count : S -> nat)(eqds : EqDec S)(o : S -> A -> Comp (B * S))(s : S), (forall a b x y, In (a, b) (getSupport (o x y)) -> count b <= 1 + (count x)) -> count s = 0 -> forall a b, In (a, b) (getSupport (c _ _ o s)) -> count b <= q.
proof: Proof. intuition. eapply Nat.le_trans. eapply qam_count_gen; eauto. lia. Qed.
imports: FCF.FCF