proposition: Theorem randomFunc_mem_spec : forall (D R : Set)(eqdd : EqDec D)(eqdr : EqDec R)(RndR : Comp R) (x1 x2 : list (D * R)) a, (forall z, arrayLookup _ x1 z = arrayLookup _ x2 z) -> comp_spec (fun y1 y2 => fst y1 = fst y2 /\ (forall x, arrayLookup _ (snd y1) x = arrayLookup _ (snd y2) x)) (randomFunc_mem _ _ RndR x1 a) (randomFunc RndR _ x2 a).
proof: Proof. intuition. unfold randomFunc, randomFunc_mem. rewrite H. case_eq (arrayLookup eqdd x2 a ); intuition. eapply comp_spec_ret; intuition. simpl. case_eq (eqb x a); intuition. rewrite eqb_leibniz in H1. subst. intuition. comp_skip. eapply comp_base_exists; intuition. eapply comp_base_exists; intuition. eapply comp_spec_ret; intuition. simpl. rewrite H. trivial. Qed.
imports: FCF PRF SplitVector cAU CompFold DetSem SemEquiv