proposition: Theorem TrueRepeat_G1_bad_equiv : Pr [x <-$ TrueRepeat_G3; ret snd x ] == Pr[TrueRepeat_G3_bad].
proof: Proof. unfold TrueRepeat_G3, TrueRepeat_G3_bad. inline_first. comp_skip. assert( Pr [x0 <-$ (bs <-$ compMap eqdb (fun _ : nat => c x) (forNats n); _ <-$ Repeat (c x) P; ret (fold_left (fun (b : bool) (x0 : B) => b || f x0) bs false, if hd_error (filter P bs) then false else true)); ret snd x0 ] == Pr [x0 <-$ (_ <-$ Repeat (c x) P; bs <-$ compMap eqdb (fun _ : nat => c x) (forNats n); ret (fold_left (fun (b : bool) (x0 : B) => b || f x0) bs false, if hd_error (filter P bs) then false else true)); ret snd x0 ] ). comp_skip. comp_swap_r. comp_skip. rewrite H0. clear H0. inline_first. comp_irr_l. edestruct Repeat_c_terminating. eauto. eapply well_formed_Repeat. unfold eq_dec; intuition. eapply (EqDec_dec _). eauto. eauto. assert ( Pr [x1 <-$ (bs <-$ compMap eqdb (fun _ : nat => c x) (forNats n); ret (fold_left (fun (b : bool) (x1 : B) => b || f x1) bs false, if hd_error (filter P bs) then false else true)); ret snd x1 ] == Pr [bs <-$ compMap eqdb (fun _ : nat => c x) (forNats n); ret (fold_left (fun b z => b && negb (P z)) bs true)] ). inline_first. comp_skip. eapply comp_spec_eq_impl_eq. simpl. eapply comp_spec_ret. eapply hd_filter_false_eq_and_false. rewrite H1. clear H1. symmetry. eapply comp_spec_eq_impl_eq. eapply comp_spec_eq_trans. eapply fold_map_fission_spec_eq. intros. eapply comp_spec_eq_refl. comp_skip. eapply compFold_ret_eq. Qed.
imports: FCF.FCF FCF.CompFold FCF.RndNat FCF.Hybrid