proposition: Theorem G2_1_equiv : Pr[G1] == Pr[G2_1].
proof: Proof. unfold G1, G2_1. comp_skip. eapply comp_spec_eq_impl_eq. comp_skip. eapply (@oc_comp_spec_eq _ _ _ _ _ _ _ _ _ _ _ _ _ _ (fun a b => forall x, arrayLookup _ a x = arrayLookup _ b x)); intuition. eapply comp_spec_symm. eapply comp_spec_consequence. eapply randomFunc_mem_spec; intuition. intuition. comp_simp. simpl in *. intuition. subst. eapply comp_spec_eq_refl. Qed.
imports: FCF PRF SplitVector cAU CompFold DetSem SemEquiv