I have to proof the following theorem:
Proof that $\eta_1 \vee \eta_2 \equiv DISTR(\eta_1, \eta_2)$.
The algorithm DISTR($\eta_1, \eta_2$) is the following:
Now I want to use induction to prove this, but I don't know how to start with the 2 different propositional formulas $\eta_1$ and $\eta_2$. Do I have to use some sort of multidimensional induction (http://www.mathblog.dk/proof-method-multidimensional-induction/) or can I just use induction on the length of $\eta_ \vee \eta_2$?
EDIT: I've tried to proof the theorem by using the tips from the comments and so far I found this:
We deliver a proof by induction on $rank(\eta_1) + rank(\eta_2)$.
Induction basis: Suppose $rank(\eta_1) + rank(\eta_2) = 0$. This implies that both $\eta_1$ and $\eta_2$ are atoms. Thus we find ourselves to be in the default case of the algorithm and it returns $\eta_1 \vee \eta_2$.
Induction step: Suppose that $rank(\eta_1) + rank(\eta_2) > 0$. We now have to distinguish different cases:
First case: Suppose $\eta_1 \equiv \eta_a \wedge \eta_b$. We know that $rank(\eta_a) < rank(\eta_1) + rank(\eta_2)$ and $rank(\eta_b) < rank(\eta_1) + rank(\eta_2)$ and $rank(\eta_2) < rank(\eta_1) + rank(\eta_2)$. So by induction, we find that $DISTR(\eta_1, \eta_2) \equiv DISTR(\eta_a, \eta_2) \wedge DISTR(\eta_b, \eta_2)$ and thus $DISTR(\eta_1, \eta_2) \equiv (\eta_a \vee \eta_2) \wedge (\eta_b \vee \eta_2)$.
Now I'm not sure on how to continue... Do I use the distribution-rule on $(\eta_a \vee \eta_2) \wedge (\eta_b \vee \eta_2)$ ? Or did I made a mistake more at the beginning of the proof?
Picking up at the induction step:
Case 1: $\eta_1 = \eta_a\land\eta_b$.
We have $rank(\eta_a), rank(\eta_b) < 1 + \max(rank(\eta_a), rank(\eta_b)) = rank(\eta_1)$, so $$rank(\eta_a) + rank(\eta_2), rank(\eta_b) + rank(\eta_2) < rank(\eta_1) + rank(\eta_2).$$ Therefore the induction hypothesis applies to the recursive calls, and we have: $DISTR(\eta_a, \eta_2)\equiv \eta_a \lor \eta_2$ and $DISTR(\eta_b, \eta_2)\equiv \eta_b \lor \eta_2$. Thus: $$\begin{align} DISTR(\eta_1, \eta_2) &= DISTR(\eta_a, \eta_2) \land DISTR(\eta_a, \eta_2) \\ &\equiv (\eta_a \lor \eta_2)\land(\eta_b \lor \eta_2) \tag{by IH} \\ &\equiv (\eta_a \land\eta_b) \lor \eta_2 \tag{$\lor$ distributes over $\land$} \\ &= \eta_1 \lor \eta_2. \end{align}$$
Case 2: $\eta_2 = \eta_c\land\eta_d$. Just like Case 1.
Case 3: Neither $\eta_1$ nor $\eta_2$ is a conjunction.
Then $DISTR(\eta_1, \eta_2) = \eta_1\lor\eta_2$, so obviously they're equivalent.