In proof transformation mode, the labels of actions for cut elimination are not very helpful: there are just three arrows, with titles "Eliminate cut key-case" and "Eliminate cut or commute it on {left,right} hand-side". For a beginner, this is not very helpful (especially the ambiguity on left/right arrows).
for the topmost cut, both arrows say "Eliminate cut or commute it on {left,right} hand-side" but do not perform the same action. I would prefer the left one to display "Eliminate left ax-cut" and the right one "Commute with ⊗ rule on the right".
Of course, once the tree, the cut and the cut formula is known, this information can be derived by the user, but for a beginner I believe it would be helpful to explain precisely what will happen if she clicks one of the arrows.
If this is too much of a hassle, or as a temporary fix, maybe it would be sufficient to have a visual distinction (maybe different colors) for key cases vs commutations.
In proof transformation mode, the labels of actions for cut elimination are not very helpful: there are just three arrows, with titles "Eliminate cut key-case" and "Eliminate cut or commute it on {left,right} hand-side". For a beginner, this is not very helpful (especially the ambiguity on left/right arrows).
Here are some examples:
https://ccll.linear-logic.org/?s=a%5E%7Cb%5E%7Cc%5E%2Ca*b*c&proof_transformation=1&p=XQAAgAD%2F%2F%2F%2F%2F%2F%2F%2F%2F%2FwA9iIoHZADSvL4AO2WnajJ4cSZ3uOM1Jm1oajsTKyplYJSCC8%2FPl15o2cdBQSb4YZcxhmXAc51ccjjCsG2aTjsvseHnnoUnYJFaubpBdlUHkNFdnM58AqCZ%2B7oWPR5Df%2BZ7jfEKeGFfJ0AWNDOaBOWalkNtNgp7u3m0TM%2BqTgaiOPN3oCQiJe2rfGZLr7MM7Cb5PAtL8D8vLHf7iDEZnnuDc%2B7w5j55G1R8zigZ4pK2Ur83ybnU5shKwkZj5Zu3l3jmXhnSeRN%2FRCk9WWkaRMm3EGbL%2F4sdX9xYHh4ql%2FDumYFBOmZ0BWzs06%2BoIneY6BjJznmixwmCaM5B29WlSwvdbf6o5ch3yX4B3jshyoD%2BoW7lekjwtOu5tfiCACRfrlJSaqg3LdbE4NsCC6Qotvinqqi%2BqHGVMJJJuaKSkZ0D0a23jysxC08Y%2FP7MWIOpKhGkZm7GtdYbdHbow3DtL2q0OJ34UVBP%2F%2F%2FGpcIu
the left arrow says "Eliminate cut or commute it on left hand-side" but I would prefer something like "Commute with ⅋ rule on the left".
https://ccll.linear-logic.org/?s=a%5E%7Cb%5E%7Cc%5E%2Ca*b*c&proof_transformation=1&p=XQAAgAD%2F%2F%2F%2F%2F%2F%2F%2F%2F%2FwA9iIoHZADSvL4AO2WnajJ4cSZ3uOM1Jm1oajsTKyplYJSCC8%2FPl15o2cdBQSb4YZcxhmXAc51ccjjCsG2aTjsvseHnnoUnYJFaubpBdlUHkNFdnM58AqCZ%2B7oWPR5Df%2BZ7jfEKeGFfJ0AWNDOaBOWalkNtNgp7u3m0TM%2BqTgY724rEAvLB4uVbqMydWAvSgQyTXa%2BTroHDohE1RMqC2Z1OyrrgX%2BAA2VEjCex%2FpxXaygOX4lstcA8WHTMteLQ214pkc1JbjJCJuNbG%2F5bfGgdg0ikAsSBWNQ30FaTGZCKl4pegcAplfvwgYx9De14QeyiUB7ucRj2fmE%2BaedIBYEMPj9qKRlMc7q7IG%2Fn2yR9xMFwaAAEUuTVs%2BeqG4gpvBRQtNQzEId2KQZ1hFBPlN8%2BIIAoAkHwazbGW2AURr7vOlFikKvEKdlSXhF5hnXdGn4YAa%2BdbXPStHNvn1LSjo47fpNRKfX%2F%2F7ESrDw%3D%3D
the left arrow says "Eliminate cut key-case" but I would prefer something like "Eliminate ⊗/⅋ key-case".
https://ccll.linear-logic.org/?s=a%5E%7Cb%5E%7Cc%5E%2Ca*b*c&proof_transformation=1&p=XQAAgAD%2F%2F%2F%2F%2F%2F%2F%2F%2F%2FwA9iIoHZADSvL4AO2WnajJ4cSZ3uOM1Jm1oajsTKyplYJSCC8%2FPl15o2cdBQSb4YZcxhmXAc51ccjjCsG2aTjsvseHnnoUnYJFaubpBdlUHkNFdnM58AqCZ%2B7oWPR5Df%2BZ7jfEKeGFfJ0AWNDOaBOWalkNtNgp7u3m0TM%2BqTgY724rEAvLB4uVbqMydWAvSgQyTXa%2BTroHDohE1RMqC2Z1OyrrgX%2BAA2VEjCex%2FpxXaygOl3DkvxU%2FU5if1KteAWxHI25U4c8towGkhC4bclwhf4aQO%2FJAkg6foYLfhSI%2FhlVjVdEfvqC9Pgkb0dE17RNfEh2zdDANw4wQF5pIzbco18EPumnVZmRHj9O8yYlPOEPk3g2HVlDu3MxpZy5X1Jj7C%2BuNCHmnQ7F6GOgC6B%2Fs1veYAG8ATL9ooAbkspD10wWgea3mnoK3PHJr1616mTXhycwICeermCE1ljP%2B9ECmdn8ZlH6tbGBoAdEriG%2FTARsgze09cKnxDqX%2F%2BLkBY
for the topmost cut, both arrows say "Eliminate cut or commute it on {left,right} hand-side" but do not perform the same action. I would prefer the left one to display "Eliminate left ax-cut" and the right one "Commute with ⊗ rule on the right".
Of course, once the tree, the cut and the cut formula is known, this information can be derived by the user, but for a beginner I believe it would be helpful to explain precisely what will happen if she clicks one of the arrows.
If this is too much of a hassle, or as a temporary fix, maybe it would be sufficient to have a visual distinction (maybe different colors) for key cases vs commutations.