Prove that $ \text{len}(q^*) \le 3\text{len}(q) -2 $ Prove by induction where q is a formula in proposition logic:
$$ \text{len}(q^*) \le 3\text{len}(q) -2 $$ 
Where the star property (*) is defined as follows:
$$ \text{atom}^* = \text{atom} $$
 $$ (\neg(q))^*=  \neg(q^*) $$
 $$ (w \land x)^* = \neg (\neg w^* \lor \neg x^*) $$
The function Len gives the total number of connectives + the number of proposition letters in a formula.
My proof up till now, here for atoms:
$$ \text{len}(q^*) \le 3\text{len}(q) - 2 $$
$$ \text{len}(q)  \le 3\text{len}(q) - 2$$
$$ 1 \le 1 $$
And here for conjunction:
$$ \text{len}((q \land w)^*) \le 3\text{len}(q \land w) - 2 $$
$$ \text{len}( \neg(\neg w^* \lor \neg x^*)) \le 3(\text{len}(q) + \text{len}(w) + 1) -2 $$
$$ \text{len}(w^*) + len (q^*) + 4 \le 3(\text{len}(q) + \text{len}(w) + 1) -2 $$
Is this correct or sufficient? Any recommendations? I have no idea how to solve the last inequality.
 A: Edit: As pointed out in the comments, a self contained proof would have been better than just finishing what Ferengi Godfried started and pointing out that the last part can be done in the same way. So here is a full, self-contained proof.
Answer: We have to prove by induction that for a formula $q$ in propositional logic which consists only of atoms, negation and conjunction (since the $^*$-operator is only defined for atoms, $\wedge$ and $\neg$), the following inequality holds: 
\begin{equation}
\text{len}(q^*) \leq 3\text{len}(q) - 2\qquad (1)
\end{equation}
The induction is on $\text{len}$ of the formula $q$ (i.e. on the number of connectives $\wedge$ and $\neg$ plus the number of atoms in $q$) and has three steps, the base case (where $q$ is an atom) and then two induction steps for negation and conjunction.
Atoms: According to the definition of the $^*$-operator, we have $q^* = q$ for every atom $q$. Using $\text{len}(q) = 1$ for atoms, the inequality follows straightforward:
\begin{equation}
\text{len}(q^*) = \text{len}(q) = 1 \leq 1 = 3\text{len}(q) - 2
\end{equation}
Negation: For negation, we have $(\neg q)^* = \neg(q^*)$ for a formula $q$. Noting that
\begin{equation}
3\text{len}(\neg q) - 2 = 3(\text{len}(q) + 1) - 2 = 3\text{len}(q) + 1 \qquad (2)
\end{equation}
we have
\begin{equation}
\text{len}((\neg q)^*) = \text{len}(\neg(q^*)) = \text{len}(q^*) + 1 \leq 3\text{len}(q) - 2 + 1 \leq 3\text{len}(\neg q) - 2 
\end{equation}
The induction hypothesis $(1)$ was used at the first inequality and $(2)$ at the second. 
Conjunction: Again by definition, we have $(w \wedge x)^* = \neg(\neg w^* \vee \neg x^*)$ for formulas $w$ and $x$. Since
\begin{equation}
3\text{len}(w \wedge x) - 2 = 3(\text{len}(w) + \text{len}(x) + 1) - 2 = 3\text{len}(w) + 3\text{len}(x) + 1 \qquad (3)
\end{equation}
and
\begin{equation}
\text{len}((w \wedge x)^*) = \text{len}(\neg(\neg w^* \vee \neg x^*)) = \text{len}(w^*) + \text{len}(x^*) + 4 \qquad (4)
\end{equation}
we have
\begin{equation}
\text{len}((w \wedge x)^*) = \text{len}(w^*) + \text{len}(x^*) + 4 \leq 3\text{len}(w) - 2 + 3\text{len}(x) - 2 + 4 \leq 3\text{len}(w \wedge x) - 2
\end{equation}
Again, $(4)$ was used at the first equality, the induction hypothesis $(1)$ at the first inequality, and $(3)$ at the second equality. 
We have proven that the inequality holds for atoms, negation and conjunction, what means that we are finished.
