Proof on tree size using Isabelle
Your first goal is provable, but is somewhat non-trivial arithmetic. I believe that the issue is essentially Isabelle not knowing that 
$$S(x - 2) = x -1$$
is true for arbitrary $x$, and indeed, this property is false in general, if $x&lt;2$! This is because $x-2=0$ in Isabelle for $x=1$.

Here this doesn't occur, because $x=2\cdot 2^n$, so $x\geq 2$ for all $n\in\mathbb{N}$. But the simplifier doesn't know this. Adding a lemma along those lines, or making sure 2*nodes(explode n t) + 1 doesn't get simplified to S(2*nodes(explode n t)) should solve your issue.

Alternately, you could re-cast your whole proof in $\mathbb{Z}$, where subtraction behaves more sanely.