proposition: Theorem G2_4_5_eq_until_bad : forall z, evalDist G2_4 (z, false) == evalDist G2_5 (z, false).
proof: Proof. pose proof @RF_Encrypt_bad_preserved as RF_Encrypt_bad_preserved. pose proof @RF_Encrypt_bad_wf as RF_Encrypt_bad_wf. intuition. unfold G2_4, G2_5. do 4 (comp_skip; comp_simp). eapply comp_spec_impl_eq. eapply comp_spec_seq; eauto with inhabited. eapply (@oc_comp_spec_eq_until_bad _ _ _ _ _ _ _ _ _ _ _ _ _ (fun a => snd a) (fun a => snd a) (fun a b => forall z, z <> x -> arrayLookup _ (fst a) z = arrayLookup _ (fst b) z)). intuition. solve [intros; apply RF_Encrypt_bad_wf]. intuition. intuition. simpl in H5; subst. unfold RF_Encrypt_bad, PRFE_RandomFunc, randomFunc. comp_skip. case_eq (eqb x b); intuition. prog_irr_l. destruct (arrayLookup (Bvector_EqDec eta) a b); wftac. prog_irr_r. destruct (arrayLookup (Bvector_EqDec eta) a0 b); wftac. prog_simp. eapply comp_spec_ret; simpl in *; intuition. rewrite orb_true_r in H10. discriminate. rewrite orb_true_r in H10. discriminate. case_eq (arrayLookup (Bvector_EqDec eta) a b); intuition. rewrite <- H4. simpl. rewrite H8. prog_simp. eapply comp_spec_ret; simpl in *; intuition. intuition; subst. rewrite eqb_refl in H7. discriminate. rewrite <- H4. simpl. rewrite H8. prog_inline_l. prog_inline_r. comp_skip. prog_simp. eapply comp_spec_ret; simpl in *; intuition. case_eq (eqbBvector z0 b); intuition. intuition. subst. rewrite eqb_refl in H7. discriminate. intuition. eapply RF_Encrypt_bad_preserved. eapply H5. trivial. intuition. eapply RF_Encrypt_bad_preserved. eapply H5. trivial. intuition. simpl. case_eq (eqbBvector z0 x); intuition. apply eqbBvector_sound in H5; intuition. trivial. intuition. prog_simp. eapply comp_spec_ret; simpl in *; intros. destruct p1; simpl in *; subst. intuition. inversion H6; clear H6; subst. intuition. subst. trivial. inversion H6; clear H6; subst. intuition. subst. trivial. Unshelve. eauto. Qed.
imports: FCF PRF Encryption RndInList OTP WC_PolyTime