lib \lib{prg-real}^H
    proc \prgsamp_H()
        \seed \gets \bits^\secpar
        // $H(\seed)$:
        A \| B := G(\seed)
        C \| D := G(B)
        return $A \| C \| D$
end

caption The starting point is $\lib{prg-real}^H$.

\equiv

lib 
    proc \prgsamp_H()
        A \| B := \prgsamp_G()
        C \| D := G(B)
        return $A \| C \| D$
end
lib \lib{prg-real}^G
    proc \prgsamp_G()
        \seed \gets \bits^\secpar
        return $G(\seed)$
end

caption Factor out everything to do with $\seed$ into a new scope. This makes an instance of $\lib{prg-real}^G$ appear and has no effect on the adversary (calling program).

\indist

lib 
    proc \prgsamp_H()
        A \| B := \prgsamp_G()
        C \| D := G(B)
        return $A \| C \| D$
end
lib \lib{prg-rand}^G
    proc \prgsamp_G()
        Y \gets \bits^{2\secpar}
        return $Y$
end

caption Since $G$ is a secure PRG, replacing $\lib{prg-real}^G$ with $\lib{prg-rand}^G$ has only negligible effect on the adversary (calling program).

\equiv

lib 
    proc \prgsamp_H()
        A \| B \gets \bits^{2\secpar}
        C \| D := G(B)
        return $A \| C \| D$
end

caption The call to $\prgsamp_G$ can be inlined, causing no effect on the adversary (calling program).

\equiv

lib 
    proc \prgsamp_H()
        A \gets \bits^\secpar
        B \gets \bits^\secpar
        C \| D := G(B)
        return $A \| C \| D$
end

caption Uniformly sampling $2\secpar$ bits is the same as uniformly (and independently) sampling its two halves.


\equiv


lib 
    proc \prgsamp_H()
        A \gets \bits^\secpar
        C \| D := \prgsamp_G()
        return $A \| C \| D$
end
lib \lib{prg-real}^G
    proc \prgsamp_G()
        \seed \gets \bits^\secpar
        return $G(\seed)$
end

caption We can repeat a similar sequence of steps, now focusing on the call to $G(B)$.

\indist


lib 
    proc \prgsamp_H()
        A \gets \bits^\secpar
        C \| D := \prgsamp_G()
        return $A \| C \| D$
end
lib \lib{prg-rand}^G
    proc \prgsamp_G()
        Y \gets \bits^{2\secpar}
        return $Y$
end

\equiv

lib 
    proc \prgsamp_H()
        A \gets \bits^\secpar
        C \| D \gets \bits^{2\secpar}
        return $A \| C \| D$
end

\equiv

lib \lib{prg-rand}^H
    proc \prgsamp_H()
        Y \gets \bits^{3\secpar}
        return $Y$
end

caption Concatenating $\secpar$ uniformly sampled bits with $2\secpar$ <i>independent,</i> 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.