Hybrid Sequence:
The starting point is $\lib{prf-real+ro}$.
We can introduce a cache in $\prfquery$ to avoid recomputing the same thing twice. We can also change $\Pi^\pm$ to sample their outputs with replacement; the change has negligible effect. Because of this change, the sets $\mathcal{A}$ and $\mathcal{B}$ are no longer used anywhere, but we retain them for a later hybrid.\FORMATTINGHACK{\pagebreak}
We can change $\prfquery$ to sample $V$ uniformly instead of calling $\Pi^+(U)$. This changes the library's behavior \emph{only if} at the end of the execution $U \in \mathcal{A}$, meaning that $U$ was the input to some direct call to $\Pi^+$ or output of some direct call to $\Pi^-$. We trigger a bad event in this case, and will later show that its probability is negligible.\FORMATTINGHACK{\pagebreak}
$\prftable[X]$ now plays the role of a OTP ciphertext, interpreting $V$ as the uniformly sampled key. Thus, it is distributed uniformly.
We can change $\Pi^+$ and $\Pi^-$ back to their original implementation, sampling their outputs without replacement.
Every $U$ value has the form $U = X \oplus \key$. So instead of keeping track of $U$-values, we can keep track of just $X$-values and recompute the $U$-values later when determining the bad event. That way, $\key$ is not needed until the end of time. The result is $\lib{prf-rand+ro}$, with extra bad-event logic at the end of time.\FORMATTINGHACK{\pagebreak}
$\lib{prf-real+ro}$
$\key \gets \bits^\secpar$
$\prfquery$($X$):
// return $F(\key,A)$
$U := \key \oplus X$
$V $
${}:= \Pi^+(U)$
${}\gets \bits^\secpar$
return
$V \oplus \key$
$\prftable[X]$
$\Pi^+$($A$):
if $\iptable^+[A]$ undefined:
$B \gets \bits^\secpar$
${} \setminus \mathcal{B}$
$$
${} \setminus \mathcal{B}$
$\iptable^+[A] := B; \mathcal{A} := \mathcal{A} \cup \{ A \}$
$\iptable^-[B] := A; \mathcal{B} := \mathcal{B} \cup \{ B \}$
return $\iptable^+[A]$
$\Pi^-$($Y$):
if $\iptable^-[B]$ undefined:
$A \gets \bits^\secpar$
${} \setminus \mathcal{A}$
$$
${} \setminus \mathcal{A}$
$\iptable^+[A] := B; \mathcal{A} := \mathcal{A} \cup \{ A \}$
$\iptable^-[B] := A; \mathcal{B} := \mathcal{B} \cup \{ B \}$
return $\iptable^-[B]$