proposition: Theorem PRF_DRBG_f_bad_spec : forall n v ls, comp_spec (fun x1 x2 => Permutation (fst (split (snd x1))) ((fst (split ls)) ++ x2)) ((PRF_DRBG_f_G2 v n) _ _ (fun (ls : list (D * Bvector eta)) (a : D) => x <-$ { 0 , 1 }^eta; ret (x, (a, x) :: ls)) ls) (PRF_DRBG_f_bad v n).
proof: Proof. induction n; intuition; simpl in *. fcf_simp. fcf_spec_ret. simpl. rewrite app_nil_r. apply Permutation_refl. fcf_inline_first. fcf_skip. fcf_skip. fcf_spec_ret. simpl in H3. simpl. destruct (split ls). simpl in H3. simpl. eapply Permutation_trans. apply H3. apply Permutation_cons_app. apply Permutation_refl. Qed.
imports: FCF HasDups RndInList CompFold Permutation PRF