  The following figure illustrates the focusing proof system linear logic. Notice that the two phases are represented by different arrows: the up-arrow denotes the asynchronous phase and the down-arrow denotes the synchronous phase. Also, sequents are divided into three zones (where the zones are separated by either a semicolon or an up or down-arrow). In particular, to the left of the up-arrow and down-arrow are the two zones. The zone written as \(\Psi\) denotes a set of formulas that can be used any number of times in the proof of that sequent. The zone written as \(\Delta\) denotes a multiset of formulas that are restricted as in MALL. The zone to the right of an up-arrow is also a multiset of formulas while the zone to the right of a down-arrow is a single formula. It is possible to impose an arbitrary order on the formulas to the right of the up-arrow since the introduction of asynchronous formulas can be done in any order.  Atoms are given polarity and in the figure below, \(A\) stands for positive atoms and the negation of \(A\) stands  for negative atoms. Proofs built by these inference rules are called focused proofs. The result in  Andreoli 1992  is that focused proofs are complete for linear logic.