like very much this site.
Let's consider the following rules of a deduction system (due to Sch\"{u}tte). I'll write them all, but some of them may not be useful.
WEAK RULES
Rule 1: \begin{equation} \frac{C \vee A \vee B \vee D}{C \vee B \vee A \vee D} \end{equation}
Rule 2: \begin{equation} \frac{A \vee A \vee D}{A \vee D} \end{equation}
STRONG RULES
rule A: \begin{equation} \frac{D}{A \vee D}\quad\text{(where $A$ is a closed wff)} \end{equation}
De Morgan rule: \begin{equation} \frac{\neg A \vee D \quad \neg B\vee D}{\neg(A \vee B)\vee D} \end{equation}
Negation: \begin{equation} \frac{A \vee D }{\neg\neg A \vee D} \end{equation}
Quantification: \begin{equation} \frac{\neg A(t)\vee D}{(\neg(x)A(x))\vee D} \end{equation}
Infinite Induction: \begin{equation} \frac{A(\bar{n}) \vee D\quad \text{for all natural numbers n}}{((x)A(x))\vee D} \quad \text{($\bar{n}$ is a numeral)} \end{equation}
CUT RULE
\begin{equation} \frac{C \vee A \quad \neg A\vee D}{C \vee D} \end{equation}
Formulas C and D are called auxiliary formulas. We can remove them (except in rule A) obtaining other instances of the rules.
I need to prove that from a proof of a formula that is a consequence of some premises using one of those rules (for example De Morgan rule), it is possible to obtain a proof of the premises. The proof in question is obtained by working on the original one. There is a description of how it is done, but I don't understand it. I'll try to explain.
Suppose that a formula $A$ is obtained by DeMorgan rule and then it is of the form $\neg(B \vee E) \vee D$. Taking a proof of $A$, we can consider all the subformulas $\neg(B \vee E)$ of the proof tree obtained starting with $\neg(B \vee E)$ in $A$ and climbing back along the proof tree. (Here it is not clear to me what is the real meaning.) This process (what process?) continues through the weak rules used and through the strong rules used in which $\neg(B \vee E)$ is a subformula of an auxiliary wff. This process can end only with a rule A or with a De Morgan rule. The set of all occurrencies of $\neg(B \vee E)$ is called \emph{history} of $\neg(B \vee E)$. Now replace all the occurrencies of $\neg(B \vee E)$ in its history with $\neg B$. Then we obtain another proof tree (after removing all those formulas that are not necessary) whose terminal formula is just $\neg B \vee D$ (that is, one of the premises in De Morgan rule). Substitution with $\neg E$ yields a proof of $\neg E \vee D$ (the other premise).
What method we precisely use to build that new proof tree? Can you show me an example of how to prove premises for De Morgan rule using the method described above?
Thank you very much.