In Sara Negri & Jan von Plato, Structural Proof Theory (2001), page 51, various properties of the system G3cp of classical propositional logic are showed.
Theorem 3.1.1 [page 49] proves that all rules of G3cp are invertible.
The following topic is about root-first proof search and decomposition of a sequent $\Gamma \Rightarrow \Delta$, and state the following :
Lemma 3.1.2: The decomposition of a sequent $\Gamma \Rightarrow \Delta$ into topsequents in G3cp is unique.
The proof is a one-line proof :
"By noting that successive application of any two logical rules in G3cp commutes."
It is not clear to me what "commute" means in this context: I must consider first a rule $R_1$ followed by $R_2$ going from top to bottom and then reversing the order : $R_2$ followed by $R_1$ but in the reverse direction ?
I've difficulties in figuring how to "reverse the order" of, for example, $L_{\lor}$ followed by $L_{\supset}$ ...
Thanks
After a night's sleep, I think that the answer is easier than I've expected.
In the classical sequent calculus G3cp we allow multisuccedent sequents $\Gamma \Rightarrow \Delta$.
In the root-first proof search, we decompose the formulas "bottom-up", using the invertibility property of the rules.
When we decompose a specific formula $\varphi$ in e.g. $\Delta$, if we consider the formation tree for $\varphi$, when we "open it" (i.e. if we consider it as $(\lnot \alpha)$ or $(\alpha_1 \lor \alpha_2)$ or $(\alpha_1 \land \alpha_2)$ and we cancel the outermost parentheses) a single connective will "surfaces"; so there is no ambiguities about the rule to be applied.
The presence of multisuccedents means that $\Gamma \Rightarrow \Delta$ can be, for example :
When we say that "successive application of any two logical rules in G3cp commutes" we means simply that starting the decomposition process from $\alpha_1 \lor \alpha_2$ produces the same end result that starting from $\beta_1 \land \beta_2$.