proposition: Theorem FixedInRndList_prob : forall (ls : list A)(x : Bvector eta), (Pr[lsR <-$ compMap _ (fun _ => {0, 1}^eta) ls; ret (if (in_dec (EqDec_dec _) x lsR) then true else false) ] <= (length ls) / 2 ^ eta)%rat.
proof: Proof. induction ls; intuition. simpl. comp_simp. simpl. rewrite evalDist_ret_0. eapply rat0_le_all. intuition. simpl. inline_first. eapply leRat_trans. eapply (evalDist_bind_event_le _ _ (fun z => eqb x z)). eapply eqRat_impl_leRat. apply RndNat_eq_any. intuition. assert (Pr [lsR <-$ (lsb' <-$ compMap (Bvector_EqDec eta) (fun _ : A => { 0 , 1 }^eta) ls; ret (a0 :: lsb')%list); ret (if in_dec (EqDec_dec (Bvector_EqDec eta)) x lsR then true else false) ] == Pr [lsR <-$ compMap (Bvector_EqDec eta) (fun _ : A => { 0 , 1 }^eta) ls; ret (if in_dec (EqDec_dec (Bvector_EqDec eta)) x lsR then true else false) ]). inline_first. comp_skip. destruct (in_dec (EqDec_dec (Bvector_EqDec eta)) x (a0 :: x0)). simpl in i. intuition; subst. rewrite eqb_refl in *. discriminate. destruct (in_dec (EqDec_dec (Bvector_EqDec eta)) x x0); intuition. simpl in n; intuition. destruct (in_dec (EqDec_dec (Bvector_EqDec eta)) x x0); intuition. rewrite H1. rewrite IHls. reflexivity. eapply leRat_trans. 2:{ eapply eqRat_impl_leRat. symmetry. replace (S (length ls)) with (1 + (length ls))%nat. apply ratAdd_num. trivial. } reflexivity. Qed.
imports: FCF.FCF FCF.CompFold