**Q:** What exactly is a power admissible model?

**Background:** Admissible models, introduced by Jon Barwise, form the building blocks of inner model theory. They are transitive models $\mathcal M = (M; \in)$ satisfying a suitable fragment of set theory, namely **K**ripke-**P**latek set theory. Sifting through a couple of papers by John Steel, the term *power admissible model* sprung up a few times and since no definition or reference was given, I more or less assumed that they were just admissible models with enough closure properties such that the given argument would work.

Today I decided to take a closer look at them and after some online research I found a definition of power admissible sets in Cook, Rathjen. Classifying the Provably Total set Functions of $\operatorname{KP}$ and $\operatorname{KP}(\mathcal{P})$, namely Definition 8.2. According to them, a transitive model $\mathcal{M} = (M; \in)$ is *power admissible* iff it satisfies $\operatorname{KP}^{\mathcal{P}}$, the extension of $\operatorname{KP}$ to formulae in $\mathcal L = \{ \in, \mathcal{P}\}$, interpreting, for any $x, y \in \mathcal{M}$,
$$
\mathcal{P}^{\mathcal{M}}(x,y) \iff y \subseteq x.
$$
It seems very likely to me that this is in fact the kind of structure Steel has in mind. However, since I am interested in some technical details of his constructions that rely on the precise properties of $\mathcal{M}$, I'd like to verify this educated guess.