appendix sectionnotation

Proof nets and switchings

symbol	meaning	first
symbol	meaning	first
${MLL}^{-}$	classical one-sided unit-free multiplicative linear logic	chapter 40
$⊢ Γ$	one-sided sequent with formula multiset $Γ$	chapter 40
$A^{⟂}$	involutive linear negation	chapter 40
$A \otimes B$	multiplicative tensor	chapter 40
$A ℘ B$	multiplicative par	chapter 40
$N (Π)$	proof structure translated from derivation $Π$	chapter 40
$G_{σ} (N)$	correction graph of net candidate $N$ under switching $σ$	chapter 40
$k (A), e (A)$	kingdom and empire of formula occurrence $A$	chapter 40
$A ≼ B$	kingdom order, meaning $A \in k (B)$	chapter 40
$\sum_{c} \| A_{c} \|$ , $# atomic$	coordinates of the lexicographic cut-reduction measure	chapter 40
cut vertex	degree-two vertex joining dual conclusion occurrences by two cut edges	chapter 40