proposition: Theorem qam_count_gen' : 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)(n : nat), (forall a b x y, In (a, b) (getSupport (o x y)) -> count b <= n + (count x)) -> forall a b, In (a, b) (getSupport (c _ _ o s)) -> count b <= q * n + (count s).
proof: Proof. Opaque getSupport. induction 1; intuition; simpl in *. repeat simp_in_support. destruct x. rewrite mult_plus_distr_r. pose proof H4. eapply (IHqueries_at_most' _ count) in H4. eapply (H1 _ _ _ count) in H5. rewrite H5. rewrite plus_comm. rewrite <- (plus_assoc). rewrite (plus_comm (q2 * n)). rewrite plus_assoc. eapply plus_le_compat. eauto. eapply le_refl. intuition. intuition. rewrite plus_0_r. eapply H; eauto. Transparent getSupport. repeat simp_in_support. intuition. repeat simp_in_support. destruct x. simpl in *. specialize (IHqueries_at_most' (S * S0)%type (fun p => count (snd p)) _ (fun (x : S * S0) (y : A) => p <-$ (oc (fst x) y) S0 eqds0 o (snd x); ret (fst (fst p), (snd (fst p), snd p))) (s, s0) (q2 * n) ). eapply le_trans. eapply IHqueries_at_most'. intuition. simpl. repeat simp_in_support. destruct x. simpl in *. eapply H1. eauto. eauto. eauto. simpl. rewrite mult_assoc. intuition. eapply le_trans. eapply IHqueries_at_most'. eauto. eauto. eapply plus_le_compat; intuition. eapply mult_le_compat; intuition. Grab Existential Variables. eapply in_oc_supp_complete; eauto. Qed.
imports: FCF PRF RndInList