I am going through normal deduction and I am pretty confused right now. I have read the definition:
Definition: A derivation (in propositional logic) is normal if no main premise in an elimination rule is the conclusion in any other rule but $\land E$ or $\to E$.
Then I looked at an example where they showed a derivation which isn't normal. $$\dfrac{\dfrac{\to E\dfrac{\neg\neg(\phi\to\psi)\quad\quad[\neg(\phi\to\psi)]^1}\bot}{ϕ\to ψ}RAA \quad\quad ϕ}{\psi}\to E.$$
Let's look at the last two lines. If i have understood it right, It shouldn't matter what kind of introduction rule you use where they used the RAA (They say here though that it's where they use RAA which is the problem). It could for example be $\lor I$ there? But if this is the case do you interpret RAA as an introduction rule? Also if I've understood it right, if it were in normal form then I could be sure there wouldn't be an or elimination rule in the place of RAA if there would be an elimination rule there, it should be either $\land$ or $\to$? Sorry, it's pretty hard to state my questions since it's hard for me to understand what the definition says. Hope someone can answer. If you want me to try to state my questions better, just tell me. Thanks :)
The derivation is not normal (according to the definition) because $ϕ → ψ$, which is the main premise of the last $\to E$, is the conclusion of RAA, which is not $\land E$ nor $\to E$.