proposition: Theorem G2_4_5_equiv : Pr[x <-$ G2_4; ret fst x] == Pr[G2_5].
proof: Proof. unfold G2_4, G2_5. inline_first. comp_irr_l. wftac. inline_first. eapply comp_spec_eq_impl_eq. comp_skip. eapply (@oc_comp_spec_eq _ _ _ _ _ _ _ _ _ _ _ _ _ _ (fun a b => forall z, arrayLookup _ a (z, (F x z)) = arrayLookup _ b z)). intuition. intuition. unfold randomFunc_mem. rewrite H0. case_eq ( arrayLookup (list_EqDec (Bvector_EqDec b)) x2 a); intuition. eapply comp_spec_ret; intuition. simpl in *. unfold eqbPair. simpl. case_eq (eqb z a); intuition. simpl. rewrite eqb_leibniz in H3. subst. rewrite eqbBvector_complete. trivial. simpl. eauto. comp_skip. apply (oneVector c). apply (oneVector c). eapply comp_spec_ret; intuition. simpl. unfold eqbPair. simpl. case_eq (eqb z a); intuition. simpl. rewrite eqb_leibniz in H5. subst. rewrite eqbBvector_complete. trivial. simpl. trivial. comp_simp. simpl in *. intuition; subst. eapply comp_spec_eq_refl. Qed.
imports: FCF PRF SplitVector cAU CompFold DetSem SemEquiv