Let $f$ be a propositional formula in negative normal form. It holds:
Applying the rules $$A\lor(B\land C)\to(A\lor V)\land(A\lor C)$$ and $$(B\land C)\lor A\to(B\lor A)\land(C\lor A)$$ as many as possible leads to a CNF formula of $f$.
How can one prove the statement above?
My approach: Induction over the structure of formula $f$. The cases with $f=x_i$, $f = \neg x_i$ and $f = f_1 \land f_2$ are easy.
But I have trouble with the last case $f = f_1 \lor f_2$. With the induction hypothesis one can say that applying the rules of $f_1$ and $f_2$ leads to formulas in CNF for both subformulas. But where to go from here?