mod SEQUENT-RULES-PROP-LOG is
  protecting PROP-LOG .
  sort Configuration .
  subsort Sequent < Configuration .
  op empty : -> Configuration .
  op __ : Configuration Configuration -> Configuration
                                         [assoc comm id: empty] .
  vars R S : PropSet .
  vars P Q : Prop .

  rl [Identity] :        empty
                    => -----------
                       |- (P, ~ P) .

  rl [Cut] :           |- (R, P) |- (S, ~ P)
                    => ---------------------
                            |- (R, S) .

  rl [Weakening] :       |- R
                    => ---------
                       |- (R, P) .

  rl [Disjunction] :     |- (R, P, Q)
                    => ----------------
                       |- (R, (P \/ Q)) .

  rl [Conjunction] :   |- (R, P) |- (S, Q)
                    => -------------------
                       |- (R, S, (P /\ Q)) .

  rl [Truth] :          empty
                    => -------
                        |- tt .
endm