. Lemma-65, For any , and for any {{ 1 , ? , } , there exists an equivalent command derived from smaller commands of type 1 , ? , by application of a rule in Fig

. Proof, The result follows from Lemma 42 and Lemma 64 by mapping each inversion as follows

. Proof, Up to equivalence, one can assume R -normal: indeed, the normal form exists by Theorem 55, its derivation is equivalent by Lemma 42, and it has the same size by definition. Then one has either = () or = () as observed in Proposition 32, with and R -normal. We sort them into one of three cases: either +, or ! + , derived as in the above statement

N. Alechina, M. Mendler, E. Valeria-de-paiva, and . Ritter, Categorical and Kripke Semantics for Constructive S4 Modal Logic, Proc. CSL, pp.292-307, 2001.
DOI : 10.1007/3-540-44802-0_21
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.13.6306

J. Andreoli, Logic Programming with Focusing Proofs in Linear Logic, Journal of Logic and Computation, vol.2, issue.3, pp.297-347, 1992.
DOI : 10.1093/logcom/2.3.297

[. Baelde, A. Doumane, and A. Saurin, Infinitary proof theory: the multiplicative additive case, Proc. CSL, p.48, 2016.
URL : https://hal.archives-ouvertes.fr/hal-01339037

G. Bierman, 10 [BNG15] Taus Brock-Nannestad and Nicolas Guenot, Focused linear logic and the -calculus, Proc. TLCA, pp.78-93, 1995.

T. Brock-nannestad, N. Guenot, and D. Gustafsson, Computation in focused intuitionistic logic, Proceedings of the 17th International Symposium on Principles and Practice of Declarative Programming, PPDP '15, pp.43-54, 2015.
DOI : 10.1007/10721975_10
URL : https://hal.archives-ouvertes.fr/hal-01249216

P. Curien, M. Fiore, and G. Munch-maccagnoni, A Theory of Effects and Resources: Adjunction Models and Polarised Calculi, Proc. POPL, p.47, 2006.
URL : https://hal.archives-ouvertes.fr/hal-01256092

P. Curien and H. Herbelin, The duality of computation, ACM SIGPLAN Notices, vol.35, issue.9, pp.233-243, 2000.
DOI : 10.1145/357766.351262
URL : https://hal.archives-ouvertes.fr/inria-00156377

[. Chaudhuri, S. Hetzl, and D. Miller, A multi-focused proof system isomorphic to expansion proofs 47 [CMS08] Kaustuv Chaudhuri, Dale Miller, and Alexis Saurin, Canonical sequent proofs via multifocusing On closed categories of functors, Fifth Ifip International Conference On Theoretical Computer Science?Tcs, pp.383-396, 1970.

J. Vincent-danos, H. Joinet, and . Schellinx, A New Deconstructive Logic: Linear Logic, Limits of small functors, pp.755-807, 1997.

J. Egger, R. Møgelberg, and A. Simpson, The enriched effect calculus: syntax and semantics, Journal of Logic and Computation, vol.24, issue.3, pp.615-654, 2012.
DOI : 10.1093/logcom/exs025
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.221.997

M. Felleisen, On the expressive power of programming languages, Science of Computer Programming, vol.17, issue.1-3, pp.35-75, 1991.
DOI : 10.1016/0167-6423(91)90036-W

[. and L. Logic, Interprétation fonctionnelle et élimination des coupures dans l'arithmétique d'ordre supérieur, Gir91] _ , A new constructive logic: Classical logic II: Vers l'imperfection, Visions des Sciences, pp.37-38, 1972.

]. _. Gir11 and T. B. Spot, Lectures on Logic 10 [Kri93] Jean-Louis Krivine, Lambda-calculus, types and models, Has16] Masahito Hasegawa, Linear exponential comonads without symmetry, Fourth International Workshop on Linearity Classical Logic, Panoramas et Synthèses, pp.50-87, 1701.

[. Laurent, A proof of the focalization property of linear logic, lecture notes, p.46, 2004.

L. Paul-blain, Adjunction models for call-by-push-value with stacks, Theory and Application of Categories, pp.75-110, 2005.

C. Liang and D. Miller, Focusing and Polarization in Intuitionistic Logic, CSL Focusing and polarization in linear, intuitionistic, and classical logics, Theor. Comput. Sci, vol.410, issue.42, pp.451-465, 2007.
DOI : 10.1016/j.tcs.2009.07.041
URL : http://doi.org/10.1016/j.tcs.2009.07.041

P. Maneggia, Models of linear polymorphism 10 [Mel09] Paul-André Melliès, Categorical semantics of linear logic, Panoramas et Synthèses, Maccagnoni, Focalisation and Classical Realisability Proc. CSL, LNCS, pp.15-215, 2004.

[. and G. Scherer, Polarised Intermediate Representation of Lambda Calculus with Sums, Proc. LICS 2015, p.47, 2003.
URL : https://hal.archives-ouvertes.fr/hal-01160579

A. Schalk, Whats is a categorical model of linear logic, p.10, 2004.

G. Scherer, Multi-focusing on extensional rewriting with sums, 13th International Conference on Typed Lambda Calculi and Applications, TLCA 2015 LIPIcs Schloss Dagstuhl -Leibniz- Zentrum fuer Informatik, pp.317-331, 2015.
URL : https://hal.archives-ouvertes.fr/hal-01235372

R. J. Simmons, Structural Focalization, ACM Transactions on Computational Logic, vol.15, issue.3, pp.1-21, 2014.
DOI : 10.1007/s10990-011-9071-2
URL : http://arxiv.org/abs/1109.6273

V. Van, O. , and F. Van-raamsdonk, Weak Orthogonality Implies Confluence: The Higher Order Case, Proc. LFCS Femke van Raamsdonk, Higher-order Rewriting, Proc. Rewrit. Tech. App, pp.379-392, 1994.

[. Wadler, Call-by-value is dual to call-by-name, SIGPLAN Not, pp.189-201, 2003.
DOI : 10.1145/944705.944723