proposition: Theorem DM_RC_G2_G3_close : forall (c : A -> Comp B) k x, (forall a s_A, In (a, s_A) (getSupport A1) -> well_formed_comp (c a)) -> (forall a s_A, In (a, s_A) (getSupport A1) -> exists b, In b (filter P (getSupport (c a)))) -> (forall a s_A, In (a, s_A) (getSupport A1) -> Pr[b <-$ c a; ret (negb (P b))] <= k) -> | evalDist (DM_RC_G2 c) x - evalDist (DM_RC_G3 c) x | <= expRat k n.
proof: Proof. intuition. unfold DM_RC_G2, DM_RC_G3. eapply evalDist_bind_distance; intuition. rewrite ratDistance_comm. eapply leRat_trans. eapply compMap_Repeat_close. wftac. edestruct H0. eauto. apply filter_In in H3. intuition. specialize (A2_wf b0 x0). apply well_formed_val_exists in A2_wf. destruct A2_wf. econstructor. eapply filter_In. intuition. eapply getSupport_In_Seq. eauto. eapply getSupport_In_Seq. eauto. simpl. intuition. simpl. trivial. eapply expRat_leRat_compat. eapply leRat_trans. 2:{ eapply H1. eauto. } comp_inline_l. comp_skip. inline_first. comp_irr_l. simpl. intuition. Qed.
imports: FCF.FCF FCF.CompFold FCF.RndNat FCF.Hybrid