Understanding Lindell's proof of (semi-honest) oblivous transfer In Lindell's tutorial &quot;How to simulate it&quot; [2016/046], section 4.3, he gives a semi-honest protocol for oblivious transfer, based on enhanced trapdoor permutations and a corresponding hard-core predicate. I don't understand some details in the proof and hope somebody can explain it to me.
He gives the following definition: $B$ is a hard-core predicate of a trapdoor permutation $f_\alpha$ if:

for every non-uniform PPT adversary $A$ there exists a negligible function $\mu(n)$ such that for all $n$:
$$
\Pr[A(1^n, \alpha, r) = B(\alpha, f_\alpha^{-1}(S(\alpha; r)))] \leq \frac{1}{2} + \mu(n),
$$

where $\alpha$ is an index in the collection of functions $\{f_
\alpha\}$ and $S$ samples (almost uniformly) in the range/domain of $f_\alpha$.
Protocol 4.2 computes OT-functionality $((b_0,b_1), \sigma) \mapsto (\lambda, b_\sigma)$ as follows:

$P_1$ sends index $\alpha$ of a trapdoor function $f_\alpha$, where $P_1$ knows the trapdoor but $P_2$ does not.
$P_2$ samples random $x_\sigma$ and $y_{1-\sigma}$, computes $y_\sigma=f_\alpha(x_\sigma)$, and sends $(y_0, y_1)$.
$P_1$ uses the trapdoor to compute $x_0$ and $x_1$, then sends $B(\alpha, x_0) \oplus b_0$ and $B(\alpha, x_1) \oplus b_1$.
$P_2$ computes $B(\alpha, x_\sigma)$ and can therefore output $b_\sigma$.

Part of the proof of security (Theorem 4.3) constructs a simulator $S_2$ for corrupt party $P_2$ (the recipient), by showing that if you can distinguish the output of $S_2$ from that of $P_2$, you can use that to construct an algorithm $A$ that breaks the assumption that $B$ is a hard-core predicate, summarized as follows:

Algorithm $A$ [...] receives $(1^n, \alpha, r)$ for input. $A$'s aim is to guess $B(\alpha, S(\alpha; r))$.

However, there is no guessing because you can simply compute $B(\alpha, S(\alpha; r))$, right?
The final equation of the proof computes $\Pr[A(1^n, \alpha, r) = B(\alpha, x)]$, but it is unclear to me here what $x$ is in this expression (the preceding paragraph only mentions how to sample $x_\sigma$).
Given the definition of the hard-core predicate, I would have expected to see $f_\alpha^{-1}$ in this part of the proof.
The answer is that it's me and not you. There was a typo in the proof and indeed $x$ referred to here is $f^{-1}_\alpha(S(\alpha,r))$. I have made the change in the proof and updated the ePrint paper. Thank you for pointing out the typo.