Is this theory of recursive counting equi-interpretable with PA? To the theory presented in this link, add a two place function symbol $\#$ denoting a counting function on numbers in sets, to the list of primitives of that language, and add the axiom:
$\#^K (x) = n \leftrightarrow [x=min(K) \land n=1] \lor [x \in K \land min(K) < x \land n= S[\#^K(P^K(x))]$
Define $P^K(x) = y \iff  x \in K \land y \in K \land  y < x \land \not \exists z \in K (y < z < x)] $ 
Define Successor as:
$x=S(y) \iff y < x \land \not \exists z (y < z < x)$
Define: $ x = min(K) \iff x \in K \land \forall y \in K (x \leq y)$

Would the resulting theory be equi-interpretable with Peano arithemtic "PA"? And thus conservatively extends PA.

 A: At a glance, the answer is yes. 
As an upper bound on strength, the argument you give in your previous question works once we include $\#$.
The lower bound is then provided as follows: if $M$ is a model of PA, then $M$ equipped with its internally-finite sets "is" a model of your theory (we have to massage the language a bit of course). Here an internally-finite set is a set of the form $\{x: n>x\wedge M\models\varphi(x)\}$ for some formula with parameters $\varphi$ and some $n\in M$.
There is a subtlety with this lower bound: to prove comprehension, we need to show that something definable by quantifying over internally-finite sets is definable in the original sense. This follows from the following: for each formula $\varphi(x; y_1,...,y_k)$, PA proves the following:

For all $a_1,...,a_k, n$, there is a $c$ such that for all $i$ we have $$p_i\vert c\iff i<n\wedge \varphi(i; a_1,...,a_k).$$

That is, in any model of PA, all the internally-finite sets are in fact quantifier-freely definable, and we can quantify over formulas of bounded quantifier complexity.
