proposition: Theorem G2_1_2_equiv : Pr[G2_1] == Pr[G2_2].
proof: Proof. unfold G2_1, G2_2. comp_skip. eapply comp_spec_eq_impl_eq. comp_skip. eapply (@oc_comp_spec_eq _ _ _ _ _ _ _ _ _ _ _ _ _ _ (fun a b => list_pred (fun c d => fst c = (snd (fst d)) /\ snd c = snd d) a b)). econstructor. intuition. unfold randomFunc_mem, F_randomFunc. erewrite arrayLookup_f_equiv ; eauto. destruct (arrayLookup_f (Bvector_EqDec b) x2 (F x a) ); intuition. eapply comp_spec_ret; intuition. simpl. econstructor. simpl. intuition. trivial. comp_skip. apply (oneVector c). apply (oneVector c). eapply comp_spec_ret; intuition. simpl. econstructor. intuition. eauto. comp_simp. simpl in *; intuition. subst. eapply comp_spec_eq_refl. Qed.
imports: FCF PRF SplitVector cAU CompFold DetSem SemEquiv