Hybrid Sequence:
\FORMATTINGHACK{\pagebreak}The starting point of the hybrid proof is $\lib{crhf-real+ic}$.
Instead of sampling outputs of $\ic^\pm$ without replacement, we can sample them with replacement. The change is indistinguishable, using the now-standard birthday reasoning. As a result of the change, the sets $\mathcal{A}[\key]$ and $\mathcal{B}[\key]$ are no longer needed and can be removed.
Whenever $\ic^\pm$ is called, we can compute the associated $H$-output and store it. Then $\crhfcmp$ can refer directly to these stored values.
Instead of sampling ideal cipher output and then computing $H[\key\|A]$, we can sample $H[\key\|A]$ first and solve for the ideal cipher output. Care is needed in $\ic^-$ because we need to sample $H[\key\|A]$ before knowing what $A$ is.\FORMATTINGHACK{\pagebreak}
Now all values assigned to $H[\cdot]$ are sampled uniformly. We can instead sample them without replacement, with negligible effect on the calling program.
Now all values assigned to $H[\cdot]$ are \emph{distinct,} and therefore $H[X\|Y] == H[X'\|Y']$ if and only if $X\|Y = X'\|Y'$.
$\lib{crhf-real+ic}$
$\crhfcmp$($X\|Y, X'\|Y'$):
$Z := \ic^+(X,Y) \oplus Y$
$Z' := \ic^+(X',Y') \oplus Y'$
return
$Z == Z'$
$H[X\|Y] == H[X'\|Y']$
$X\|Y == X'\|Y'$
$\ic^+$($\key,A$):
if $\prftable^+[\key,A]$ undefined:
$B $
${}\gets \bits^\secpar$
${} \setminus \mathcal{B}[\key]$
$$
${}:= A \oplus H[\key\|A]$
$\prftable^+[\key,A] := B$
$; \mathcal{A}[\key] := \mathcal{A}[\key] \cup \{ A \}$
$$
$\prftable^-[\key,B] := A$
$; \mathcal{B}[\key] := \mathcal{B}[\key] \cup \{ B \}$
$$
return $\prftable^+[\key,A]$
$\ic^-$($\key,B$):
if $\prftable^-[\key,B]$ undefined:
$A $
${}\gets \bits^\secpar$
${} \setminus \mathcal{A}[\key]$
$$
${}:= B \oplus H$
$\prftable^+[\key,A] := B$
$; \mathcal{A}[\key] := \mathcal{A}[\key] \cup \{ A \}$
$$
$\prftable^-[\key,B] := A$
$; \mathcal{B}[\key] := \mathcal{B}[\key] \cup \{ B \}$
$$
return $\prftable^-[\key,B]$