[MatteoFrigo]

You got it. There are a few nuisances, e.g. the "theorem statement" must be hashed as well so that proving that name=Mickey has a different oracle than proving that name=Goofy, but your basic understanding is correct.