The Kleene * axioms and rules are from the article
P. Jipsen, From semirings to residuated Kleene lattices, Studia Logica 76(2) (2004), 291-303.
Note: Wojciech Buszkowski, On Action Logic, Journal of Logic and Computation, (2006) shows that the system implemented here is not complete without the cut rule.
The (in)equations are in the language of residuated Kleene lattices. Specifically, the language used here has
Standard equational results about residuated Kleene lattices
To display the proofs in a linear fashion, rather than the more usual Gentzen style, the proof trees are displayed from the root downwards, with the depth of nodes indicated by the indentation level. (Only the branching rules increase the indentation depth.) Each sequent is labeled by the name of the rule that produced it. When a terminal node is reached, the indentation level decreases again.