[
[
['5','add','hl'],
['6','add','hl'],
['94','add','hl'],
['23','remove','slide-up'],
['10','add','slide-down']
],
[
['95','add','hl'],
['95','remove','slide-left'],
['96-slide','remove','slide-left'],
['3','add','hidden'],
['5','remove','hl'],
['5','add','hidden'],
['6','remove','hl'],
['6','add','hidden'],
['94','remove','hl'],
['94','add','slide-right']
],
[
['95','remove','hl']
],
[
['96-flip','add','flipped'],
['23','add','slide-down']
],
[
['97','add','hl']
],
[
['98','add','hl'],
['98','remove','slide-right'],
['97','remove','hl'],
['97','add','slide-left'],
['96-slide','add','slide-left']
],
[
['98','remove','hl'],
['99','add','hl'],
['51','remove','slide-up']
],
[
['100','add','hl'],
['100','remove','slide-left'],
['48','add','hl'],
['48','remove','hidden'],
['99','remove','hl'],
['99','add','slide-right']
],
[
['100','remove','hl'],
['48','remove','hl'],
['48','add','hl'],
['102','add','hl'],
['64','remove','slide-up'],
['51','add','slide-down']
],
[
['103','add','hl'],
['103','remove','slide-left'],
['96-slide','remove','slide-left'],
['96-flip','remove','flipped'],
['48','remove','hl'],
['48','add','hidden'],
['102','remove','hl'],
['102','add','slide-right']
],
[
['103','remove','hl']
],
[
['96-flip','add','flipped'],
['64','add','slide-down']
],
[
['104','add','hl']
],
[
['105','add','hl'],
['105','remove','slide-right'],
['104','remove','hl'],
['104','add','slide-left'],
['96-slide','add','slide-left']
],
[
['105','remove','hl'],
['7','add','hl'],
['8','add','hl'],
['107','add','hl'],
['91','remove','slide-up']
],
[
['87','remove','hidden'],
['99','add','hl'],
['99','remove','slide-right'],
['97','add','hl'],
['97','remove','slide-left'],
['94','add','hl'],
['94','remove','slide-right'],
['104','add','hl'],
['104','remove','slide-left'],
['102','add','hl'],
['102','remove','slide-right'],
['89','add','hl'],
['89','remove','hidden'],
['108','add','hl'],
['108','remove','slide-left'],
['7','remove','hl'],
['7','add','hidden'],
['8','remove','hl'],
['8','add','hidden'],
['107','remove','hl'],
['107','add','slide-right']
],
[
['99','remove','hl'],
['97','remove','hl'],
['94','remove','hl'],
['104','remove','hl'],
['102','remove','hl'],
['89','remove','hl'],
['108','remove','hl']
]
]
The starting point is $\lib{prg-real}^H$.
We can apply a three-hop maneuver to the first call to $G$, replacing ``$A\|B := G(\seed)$'' with ``$A\|B \gets \bits^{2\secpar}$.''
Uniformly sampling $2\secpar$ bits is the same as uniformly (and independently) sampling its two halves.
Now we can apply a three-hop maneuver to the remaining call to $G$.
Concatenating $\secpar$ uniformly sampled bits with $2\secpar$ \emph{independent,} uniformly sampled bits is the same as sampling $3\secpar$ uniform bits. The result of this change is the $\lib{prg-rand}^H$ library, which completes the proof.
$\lib{prg-real}^H$
$\lib{prg-rand}^H$
$\seed \gets \bits^\secpar$
$A $
$\| B $
${}:= {}$
$G(\seed)$
$\prgsamp_G()$
${}\gets \bits^{2\secpar}$
${}\gets \bits^\secpar$
$B \gets \bits^\secpar$
$C \| D $
${}\gets \bits^{2\secpar}$
$Y \gets \bits^{3\secpar}$
$\link$
$\lib{prg-real}^G$
$\seed \gets \bits^\secpar$
return $G(\seed)$
$\lib{prg-rand}^G$
$Y \gets \bits^{2\secpar}$
return $Y$