I am working through the proof of a theorem about a derivation system. The theorem requires an induction derivation trees that end with a rule $R$ which has two premises $P_1$ and $P_2$. The proof proceeds by induction on the sum of the nodes of the premises: $nodes(P_1)+nodes(P_2)$.
The author skips over details of the proof and I am trying to fill them in for myself. I'm having trouble understanding the induction principle being used and the structure of the induction proof.
My understanding as to the structure of the proof is as follows: let $m=nodes(P_1)$ and $n=nodes(P_2)$.
- Base: Show the property holds for all possible derivation trees where the sum $m+n$ equals 0.
- Induction Hypothesis: Suppose the property holds for all derivation trees where $m+n=k$.
- Inductive Step: Show the property holds for all derivation trees where the sum of the nodes $m+n$ equals $K+1$. This amounts to doing a case analysis on both $P_1$ and $P_2$ where one considers all possible final rules to derive $P_1$ and $P_2$ (this is all the ways to have $m+n=K+1$), and showing that in each case the property holds assuming it holds for derivations with $m+n=K$.
Is this the correct understanding of the structure of the induction proof and the induction principle? Is there an equivalent way to induction principle that can be used here?