Can you expand the same formula in different branches in the method of analytic tableaux?

Question

I need to prove $\vdash_{TA} (p \land q) \lor (p \land r) \rightarrow p \land (q \lor r)$

For that, I did such:

But I've expanded $Fp \land (q \lor r)$ twice in different branches though, is this allowed?

Answer 1

Not only is that allowed, but it is in fact mandated! As long as we still have one or more open branches, we need to explore the possible ways in which the statements that occur in that branch can have the truth-value as assigned, i.e. we need to keep applying decomposition rules until either we get all closed branches, or until there is nothing left to decompose.

In your case, once you have reached the $Tr$ in the right branch, that branch is still open, but the $FP\land (Q \lor R)$ has not yet been decomposed in that branch. And since there is nothing else to do, you have to decompose it at that point.