The definition of $M\_n^\sharp$ in [OIMT10] is the unique sound, $(\omega,\omega\_1,\omega\_1+1)$-iterable mouse which is not $n$-small, but all of whose proper initial segments are $n$-small.


What is the general definition of $M\_n^\sharp(X)$ for an arbitrary set $X$? For reals $x$ it seems to be identical to the definition above, but where the underlying universe of our mouse is of the form $J\_\alpha^{\vec E}[x]$ instead of $J\_\alpha^{\vec E}$. This so-called "$x$-mouse" is only defined for reals $x$ though (at least in [Schin14]). In [CMI14, p.9] it seems as though they require that $X\in M\_n^\sharp(X)$, so this doesn't seem to generalise. Are we working with $J\_\alpha^{\vec E}(X)$'s instead, so that $M\_n^\sharp(X)$ ceases to be countable?


* *[OIMT10] Steel: "Outline of Inner Model Theory", 2010*
* *[Schin14] Schindler: "Set Theory - Exploring Independence and Truth", 2014*
* *[CMI14] Schindler, Steel: "The Core Model Induction", 2014*



Definition of $M_n^\sharp(X)$ for arbitrary set $X$
See following article by Foreman-Magidor-Schindler:



> 
> [The consistency strength of successive cardinals with the tree property](https://www.cambridge.org/core/journals/journal-of-symbolic-logic/article/div-classtitlethe-consistency-strength-of-successive-cardinals-with-the-tree-propertydiv/C7A69BE2768837CC7C8B35ACC3F02D12).
> 
> 
> 


On page 1841 of the paper, they define the general notion you are looking for.


