* Honda et al. (1998) Kohei Honda, Vasco T. Vasconcelos, and Makoto Kubo. 1998\.  Language primitives and type discipline for structured communication-based programming. In _Programming Languages and Systems_ , Chris Hankin (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg, 122–138.  https://doi.org/10.1007/BFb0053567
  * Honda et al. (2008) Kohei Honda, Nobuko Yoshida, and Marco Carbone. 2008\.  Multiparty Asynchronous Session Types. In _Proc. of 35th Symp. on Princ. of Prog. Lang._ (San Francisco, California, USA) _(POPL ’08)_. ACM, New York, NY, USA, 273–284.  https://doi.org/10.1145/1328897.1328472
  * Honda et al. (2016) Kohei Honda, Nobuko Yoshida, and Marco Carbone. 2016\.  Multiparty Asynchronous Session Types.  _J. ACM_ 63, 1 (2016), 9:1–9:67.  https://doi.org/10.1145/2827695
  * Horne (2020) Ross Horne. 2020\.  Session Subtyping and Multiparty Compatibility Using Circular Sequents. In _31st International Conference on Concurrency Theory (CONCUR 2020)_ _(Leibniz International Proceedings in Informatics (LIPIcs), Vol. 171)_ , Igor Konnov and Laura Kovács (Eds.). Schloss Dagstuhl–Leibniz-Zentrum für Informatik, Dagstuhl, Germany, 12:1–12:22.  https://doi.org/10.4230/LIPIcs.CONCUR.2020.12
  * Hu and Yoshida (2016) Raymond Hu and Nobuko Yoshida. 2016.  Hybrid Session Verification Through Endpoint API Generation. In _Fundamental Approaches to Software Engineering - 19th International Conference, FASE 2016,Eindhoven, The Netherlands_ _(Lecture Notes in Computer Science, Vol. 9633)_ , Perdita Stevens and Andrzej Wasowski (Eds.). Springer, 401–418.  https://doi.org/10.1007/978-3-662-49665-7_24
  * Hu and Yoshida (2017) Raymond Hu and Nobuko Yoshida. 2017.  Explicit Connection Actions in Multiparty Session Types. In _FASE_ _(LNCS, Vol. 10202)_. 116–133.  https://doi.org/10.1007/978-3-662-54494-5_7
  * Hu et al. (2008) Raymond Hu, Nobuko Yoshida, and Kohei Honda. 2008\.  Session-Based Distributed Programming in Java. In _ECOOP 2008 – Object-Oriented Programming_ , Jan Vitek (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg, 516–541.  https://doi.org/10.1007/978-3-540-70592-5_22
  * Imai et al. (2020) Keigo Imai, Rumyana Neykova, Nobuko Yoshida, and Shoji Yuen. 2020.  Multiparty Session Programming With Global Protocol Combinators. In _34th European Conference on Object-Oriented Programming (ECOOP 2020)_ _(Leibniz International Proceedings in Informatics (LIPIcs), Vol. 166)_ , Robert Hirschfeld and Tobias Pape (Eds.). Schloss Dagstuhl–Leibniz-Zentrum für Informatik, Dagstuhl, Germany, 9:1–9:30.  https://doi.org/10.4230/LIPIcs.ECOOP.2020.9
  * Jacobs et al. (2022) Jules Jacobs, Stephanie Balzer, and Robbert Krebbers. 2022\.  Multiparty GV: Functional Multiparty Session Types with Certified Deadlock Freedom.  _Proc. ACM Program. Lang._ 6, ICFP, Article 107 (aug 2022), 30 pages.  https://doi.org/10.1145/3547638
  * Kiczales et al. (1997) Gregor Kiczales, John Lamping, Anurag Mendhekar, Chris Maeda, Cristina Lopes, Jean-Marc Loingtier, and John Irwin. 1997.  Aspect-oriented programming. In _ECOOP’97 — Object-Oriented Programming_ , Mehmet Akşit and Satoshi Matsuoka (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 220–242.  https://doi.org/10.1007/BFb0053381
  * Lagaillardie et al. (2022) Nicolas Lagaillardie, Rumyana Neykova, and Nobuko Yoshida. 2022\.  Stay Safe Under Panic: Affine Rust Programming with Multiparty Session Types. In _36th European Conference on Object-Oriented Programming (ECOOP 2022)_ _(Leibniz International Proceedings in Informatics (LIPIcs), Vol. 222)_ , Karim Ali and Jan Vitek (Eds.). Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl, Germany, 4:1–4:29.  https://doi.org/10.4230/LIPIcs.ECOOP.2022.4
  * Lange and Tuosto (2012) Julien Lange and Emilio Tuosto. 2012.  Synthesising Choreographies from Local Session Types. In _CONCUR 2012 – Concurrency Theory_ , Maciej Koutny and Irek Ulidowski (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 225–239.  https://doi.org/10.1007/978-3-642-32940-1_17
  * Lange et al. (2015) Julien Lange, Emilio Tuosto, and Nobuko Yoshida. 2015\.  From communicating machines to graphical choreographies. In _42nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages_. ACM, 221–232.  https://doi.org/10.1145/2676726.2676964
  * Lange and Yoshida (2019) Julien Lange and Nobuko Yoshida. 2019.  Verifying Asynchronous Interactions via Communicating Session Automata. In _Computer Aided Verification_ , Isil Dillig and Serdar Tasiran (Eds.). Springer International Publishing, Cham, 97–117.  https://doi.org/10.1007/978-3-030-25540-4_6
  * MIT (2022) MIT. 2022.  Kerberos: The Network Authentication Protocol.  https://web.mit.edu/kerberos/.  Accessed: 20/10/2022.
  * Miu et al. (2021) Anson Miu, Francisco Ferreira, Nobuko Yoshida, and Fangyi Zhou. 2021.  Communication-Safe Web Programming in TypeScript with Routed Multiparty Session Types. In _Proceedings of the 30th ACM SIGPLAN International Conference on Compiler Construction_ (Virtual, Republic of Korea) _(CC 2021)_. Association for Computing Machinery, New York, NY, USA, 94–106.  https://doi.org/10.1145/3446804.3446854
  * Montesi (2013) Fabrizio Montesi. 2013\.  _Choreographic Programming_.  Ph. D. Dissertation.  https://www.fabriziomontesi.com/files/choreographic_programming.pdf
  * Montesi and Yoshida (2013) Fabrizio Montesi and Nobuko Yoshida. 2013.  Compositional Choreographies. In _CONCUR 2013 – Concurrency Theory_ , Pedro R. D’Argenio and Hernán Melgratti (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 425–439.  https://doi.org/10.1007/978-3-642-40184-8_30
  * Neykova et al. (2018) Rumyana Neykova, Raymond Hu, Nobuko Yoshida, and Fahd Abdeljallal. 2018.  A Session Type Provider: Compile-time API Generation for Distributed Protocols with Interaction Refinements in F#. In _27th International Conference on Compiler Construction_. ACM, 128–138.  https://doi.org/10.1145/3178372.3179495
  * Neykova and Yoshida (2019) Rumyana Neykova and Nobuko Yoshida. 2019.  _Featherweight Scribble_. LNCS, Vol. 11665.  Springer, Cham, 236–259.  https://doi.org/10.1007/978-3-030-21485-2_14
  * OMG (2022) OMG. 2022.  Business Process Model and Notation.  https://www.bpmn.org/.  Accessed: 20/10/2022.
  * Padovani et al. (2014) Luca Padovani, Vasco Thudichum Vasconcelos, and Hugo Torres Vieira. 2014.  Typing Liveness in Multiparty Communicating Systems. In _Coordination Models and Languages_ , Eva Kühn and Rosario Pugliese (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 147–162.  https://doi.org/10.1007/978-3-662-43376-8_10
  * Savanovic et al. (2020) Zorica Savanovic, Letterio Galletta, and Hugo Torres Vieira. 2020\.  A type language for message passing component-based systems. In _Proceedings 13th Interaction and Concurrency Experience, ICE 2020, Online, 19 June 2020_ _(EPTCS, Vol. 324)_ , Julien Lange, Anastasia Mavridou, Larisa Safina, and Alceste Scalas (Eds.). 3–24.  https://doi.org/10.4204/EPTCS.324.3
  * Scalas et al. (2017) Alceste Scalas, Ornela Dardha, Raymond Hu, and Nobuko Yoshida. 2017.  A Linear Decomposition of Multiparty Sessions for Safe Distributed Programming. In _ECOOP_.  https://doi.org/10.4230/LIPIcs.ECOOP.2017.24
  * Scalas and Yoshida (2016) Alceste Scalas and Nobuko Yoshida. 2016.  Lightweight Session Programming in Scala. In _30th European Conference on Object-Oriented Programming (ECOOP 2016)_ _(Leibniz International Proceedings in Informatics (LIPIcs), Vol. 56)_ , Shriram Krishnamurthi and Benjamin S. Lerner (Eds.). Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany, 21:1–21:28.  https://doi.org/10.4230/LIPIcs.ECOOP.2016.21
  * Scalas and Yoshida (2019) Alceste Scalas and Nobuko Yoshida. 2019.  Less Is More: Multiparty Session Types Revisited. In _46th ACM SIGPLAN Symposium on Principles of Programming Languages_ , Vol. 3. ACM, 30:1–30:29.  https://doi.org/10.1145/3290343
  * Scalas et al. (2019) Alceste Scalas, Nobuko Yoshida, and Elias Benussi. 2019\.  Verifying Message-passing Programs with Dependent Behavioural Types. In _Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation_ (Phoenix, AZ, USA) _(PLDI 2019)_. ACM, New York, NY, USA, 502–516.  https://doi.org/10.1145/3314221.3322484
  * Stolze et al. (2021) Claude Stolze, Marino Miculan, and Pietro Di Gianantonio. 2021\.  Composable Partial Multiparty Session Types. In _FACS 2021 Conference Proceedings_ , Vol. 13077. Springer.  https://doi.org/10.1007/978-3-030-90636-8_3
  * Tabareau et al. (2014) Nicolas Tabareau, Mario Südholt, and Éric Tanter. 2014\.  Aspectual Session Types. In _Proceedings of the 13th International Conference on Modularity_ (Lugano, Switzerland) _(MODULARITY ’14)_. Association for Computing Machinery, New York, NY, USA, 193–204.  https://doi.org/10.1145/2577080.2577085
  * Ungar and Smith (1987) David Ungar and Randall B. Smith. 1987.  Self: The Power of Simplicity _(OOPSLA ’87)_. Association for Computing Machinery, New York, NY, USA, 227–242.  https://doi.org/10.1145/38765.38828
  * Viering et al. (2021) Malte Viering, Raymond Hu, Patrick Eugster, and Lukasz Ziarek. 2021.  A Multiparty Session Typing Discipline for Fault-Tolerant Event-Driven Distributed Programming.  _Proc. ACM Program. Lang._ 5, OOPSLA, Article 124 (oct 2021), 30 pages.  https://doi.org/10.1145/3485501
  * Yonezawa and Tokoro (1986) A Yonezawa and M Tokoro. 1986.  _Object-oriented concurrent programming_.  The MIT Press.
  * Yoshida and Gheri (2020) Nobuko Yoshida and Lorenzo Gheri. 2020.  A Very Gentle Introduction to Multiparty Session Types. In _Distributed Computing and Internet Technology_ , Dang Van Hung and Meenakshi D´Souza (Eds.). Springer International Publishing, Cham, 73–93.  https://doi.org/10.1007/978-3-030-36987-3_5
  * Yoshida et al. (2013) Nobuko Yoshida, Raymond Hu, Rumyana Neykova, and Nicholas Ng. 2013\.  The Scribble Protocol Language. In _Trustworthy Global Computing - 8th International Symposium, TGC 2013, Buenos Aires, Argentina_ _(Lecture Notes in Computer Science, Vol. 8358)_ , Martín Abadi and Alberto Lluch-Lafuente (Eds.). Springer, 22–41.  https://doi.org/10.1007/978-3-319-05119-2_3
  * Yoshida et al. (2021) Nobuko Yoshida, Fangyi Zhou, and Francisco Ferreira. 2021\.  Communicating Finite State Machines and an Extensible Toolchain for Multiparty Session Types. In _Fundamentals of Computation Theory_ , Evripidis Bampis and Aris Pagourtzis (Eds.). Springer International Publishing, Cham, 18–35.  https://doi.org/10.1007/978-3-030-86593-1_2
  * Zhou et al. (2020) Fangyi Zhou, Francisco Ferreira, Raymond Hu, Rumyana Neykova, and Nobuko Yoshida. 2020.  Statically Verified Refinements for Multiparty Protocols.  _Proc. ACM Program. Lang._ 4, OOPSLA, Article 148 (nov 2020), 30 pages.  https://doi.org/10.1145/3428216

##  Appendix A Communication Protocol for the Company, from Overview

In Figure 9 the communication protocol for the whole company from §2.

dadsw${\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\textbf{{f}}}_{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}1}}$${\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\textbf{{f}}}_{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}2}}$prodprodprodprodpriceokgopricepublishwaitwaitwaitwaitwait
Figure 9. Whole Communication in the Company

##  Appendix B Definitions and Proofs

###  B.1. Compositionality: Building Back a Subprotocol into a Global One

###### Definition B.1 (Guardedness for Hybrid Types).

We define _guardedness_ as a predicate on hybrid types, with the following
inductive rules:

$\begin{array}[]{c}\dfrac{}{\texttt{\small guarded}\
\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{\mathtt{end}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}}\quad\dfrac{}{\texttt{\small
guarded}\
\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{X}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}}\quad\dfrac{\texttt{\small
not\\_pure\\_rec}\;\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{X}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\;\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\quad\texttt{\small
guarded}\
\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}}{\texttt{\small
guarded}\
(\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{\mu\definecolor{currbkp}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{X}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}.\definecolor{currbkp}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0})}\quad\dfrac{\texttt{\small
guarded}\;\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H_{1}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\quad\texttt{\small
guarded}\;\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H_{2}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}}{\texttt{\small
guarded}\
(\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{\definecolor{currbkp}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H_{1}}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}|\definecolor{currbkp}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H_{2}}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0})}\\\\[8.53581pt]
\dfrac{\forall i\in I.\texttt{\small guarded}\
{\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{\definecolor{currbkp}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H}\color[rgb]{0.1,0.4,0.1}{}_{i}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}}}{\texttt{\small
guarded}\
(\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{{{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\textbf{{p}}}}}!{{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\textbf{{q}}}}};\\{{{\color[rgb]{0.28125,0.23828125,0.55078125}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.55078125}{\ell_{i}}}}({\color[rgb]{0.28125,0.23828125,0.546875}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.546875}{{\color[rgb]{0.28125,0.23828125,0.546875}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.546875}{\texttt{\small
S}}}_{i}}}).\definecolor{currbkp}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H}\color[rgb]{0.1,0.4,0.1}{}_{i}\\}_{i\in
I}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0})}\quad\dfrac{\forall
i\in I.\texttt{\small guarded}\
{\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{\definecolor{currbkp}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H}\color[rgb]{0.1,0.4,0.1}{}_{i}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}}}{\texttt{\small
guarded}\
(\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{{{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\textbf{{p}}}}}?{{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\textbf{{q}}}}};\\{{{\color[rgb]{0.28125,0.23828125,0.55078125}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.55078125}{\ell_{i}}}}({\color[rgb]{0.28125,0.23828125,0.546875}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.546875}{{\color[rgb]{0.28125,0.23828125,0.546875}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.546875}{\texttt{\small
S}}}_{i}}}).\definecolor{currbkp}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H}\color[rgb]{0.1,0.4,0.1}{}_{i}\\}_{i\in
I}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0})}\quad\dfrac{\forall
i\in I.\texttt{\small guarded}\
{\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{\definecolor{currbkp}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H}\color[rgb]{0.1,0.4,0.1}{}_{i}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}}}{\texttt{\small
guarded}\
(\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\textbf{{p}}}}\to{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\textbf{{q}}}}:\\{{{\color[rgb]{0.28125,0.23828125,0.55078125}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.55078125}{\ell_{i}}}}({\color[rgb]{0.28125,0.23828125,0.546875}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.546875}{{\color[rgb]{0.28125,0.23828125,0.546875}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.546875}{\texttt{\small
S}}}_{i}}}).\definecolor{currbkp}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H}\color[rgb]{0.1,0.4,0.1}{}_{i}\\}_{i\in
I}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0})}\end{array}\vspace*{3mm}$

where $\texttt{\small
not\\_pure\\_rec}\;\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{X}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\;\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}$
means that
$\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}$
is different from
$\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{\mu\definecolor{currbkp}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{Y_{1}}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}.\dots\definecolor{currbkp}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{\mu\definecolor{currbkp}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{Y_{n}}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}.\definecolor{currbkp}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{X}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}$
and also
$\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\neq\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{X}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}$.

The above definition is adapted from the Coq-mechanised MPST metatheory in
(Castro-Perez et al., 2021) (Definitions A.2 and A.10 in the appendix of the
extended version of the paper (Castro-Perez et al., 2021)).

The next six lemmas are preliminary results, adapted from classic multiparty
session type theories. They are needed for the base cases of induction in the
build-back theorem (Theorem B.17). For all the lemmas below, the proofs go by
structural induction.

###### Lemma B.2 (Projection and Closed Types).

$\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{\upharpoonright}}_{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{E}}$
is closed iff
$\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}$
is closed.

###### Lemma B.3 (Localiser and Closed Types).

${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{{\sf{loc}}\;}}\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}$
is closed iff
$\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}$
is closed.

###### Lemma B.4 (Projection onto Internal Participants).

If
${\textsf{ipart}}({\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}})\subseteq
E$ then
$\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{\upharpoonright}}_{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{E}}=\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}$.

###### Lemma B.5 (Projection onto Disjoint Participants $(1)$).

If
${\textsf{ipart}}({\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}})\cap
E^{\prime}=\emptyset$ and
$\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}$
is closed, then
$\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{\upharpoonright}}_{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{E^{\prime}}}=\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{\mathtt{end}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}$.

###### Lemma B.6 (Projection onto Disjoint Participants $(2)$).

If
${\textsf{ipart}}({\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}})\cap
E^{\prime}=\emptyset$ and
$\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}$
is _not_ closed, then
$\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{\upharpoonright}}_{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{E^{\prime}}}=\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{\mu
Y_{1}.\dots.\mu
Y_{n}.}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{X}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}$
(if such projection exists).

###### Lemma B.7 (Projection is Guarded).

If
$\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{\upharpoonright}}_{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{E}}$
is guarded (if it is defined and
$\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}$
is guarded).

The following definitions and lemmas introduce objects and results needed for
the main algorithm and ultimately for proving Theorem B.17. They guarantee the
good behaviour of our compositionality algorithm, with respect to full merge
((Deniélou and Yoshida, 2013) and Definition 3.6 in this paper) for projection
and its “dual” for the localiser (Definition 3.8 in this paper).

The _binary unmerge for localiser_
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{\sf
unmL^{bin}}}$ takes a type
$\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H^{\dagger}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}$
(first argument) and “unmerges” it, according to the structure of two other
types
$\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H^{L}_{1}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}$
and
$\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H^{L}_{2}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}$
(second and third arguments); thus
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{\sf
unmL^{bin}}}$ returns a pair of types, the unmerged components of
$\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H^{\dagger}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}$.
The non-binary version of the _unmerge for localiser_
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{\sf
unmL}}$ is defined by iterating the binary one, thus allowing for unmerging
into $n$ types. The role of this function is clarified by Lemma B.11.

To correctly define such function we need an auxiliary function that handles
the case in which a projection merge is equal to a localiser one:
$\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{\bigsqcup}_{i\in
I}\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H^{\dagger}_{i}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}=\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{\bigsqcup^{L}}_{j\in
J}\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{\definecolor{currbkp}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H^{L}}\color[rgb]{0.1,0.4,0.1}{}_{j}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}$.
In this case we want to obtain, for all $i\in I,j\in J$,
$\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{\definecolor{currbkp}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H^{L}}\color[rgb]{0.1,0.4,0.1}{}^{i}_{j}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}$
such that
$\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{\bigsqcup}_{i}\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{\definecolor{currbkp}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H^{L}}\color[rgb]{0.1,0.4,0.1}{}^{i}_{j}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}=\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{\definecolor{currbkp}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H^{L}}\color[rgb]{0.1,0.4,0.1}{}_{j}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}$
and
$\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{\bigsqcup^{L}}_{j}\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{\definecolor{currbkp}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H^{L}}\color[rgb]{0.1,0.4,0.1}{}^{i}_{j}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}=\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H^{\dagger}_{i}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}$.

###### Definition B.8 (Localiser Unmerge for Projection Merge).

The partial function _binary localiser-unmerge for projection merge_
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{{\sf
unmLP^{bin}}\;\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H^{\dagger}_{1}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\;\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H^{\dagger}_{2}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\;\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H^{L}_{1}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\;\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H^{L}_{2}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}}}$
is recursively defined by the following equations, whenever the recursive call
is defined (we use $\pi_{1}$ and $\pi_{2}$ to indicate standard pair
projections):

$\begin{array}[]{l}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{{\sf
unmLP^{bin}}\;\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{\mathtt{end}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\;\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{\mathtt{end}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\;\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{\mathtt{end}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\;\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{\mathtt{end}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}}}=((\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{\mathtt{end}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0},\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{\mathtt{end}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}),(\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{\mathtt{end}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0},\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{\mathtt{end}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}))\\\
{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{{\sf
unmLP^{bin}}\;\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{X}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\;\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{X}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\;\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{X}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\;\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{X}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}}}=((\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{X}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0},\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{X}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}),(\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{X}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0},\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{X}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}))\\\
{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{{\sf
unmLP^{bin}}\;\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{\mu\definecolor{currbkp}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{X}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}.\definecolor{currbkp}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H^{\dagger}_{1}}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\;\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{\mu\definecolor{currbkp}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{X}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}.\definecolor{currbkp}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H^{\dagger}_{2}}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\;\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{\mu\definecolor{currbkp}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{X}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}.\definecolor{currbkp}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H^{L}_{1}}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\;\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{\mu\definecolor{currbkp}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{X}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}.\definecolor{currbkp}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H^{L}_{2}}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}}}=((\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{\mu\definecolor{currbkp}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{X}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}.\definecolor{currbkp}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H^{1}_{1}}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0},\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{\mu\definecolor{currbkp}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{X}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}.\definecolor{currbkp}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H^{1}_{2}}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}),(\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{\mu\definecolor{currbkp}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{X}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}.\definecolor{currbkp}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H^{2}_{2}}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0},\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{\mu\definecolor{currbkp}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{X}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}.\definecolor{currbkp}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H^{2}_{2}}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}))\\\
\qquad\text{where}\
\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{\definecolor{currbkp}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H}\color[rgb]{0.1,0.4,0.1}{}^{n}_{m}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}=\pi_{n}(\pi_{m}({\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{{\sf
unmLP^{bin}}\;\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H^{\dagger}_{1}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\;\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H^{\dagger}_{2}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\;\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H^{L}_{1}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\;\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H^{L}_{2}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}}})))\
\text{for $n,m=1,2$}\\\
{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{{\sf
unmLP^{bin}}\;(\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{{{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\textbf{{p}}}}}!{{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\textbf{{q}}}}};\\{{{\color[rgb]{0.28125,0.23828125,0.55078125}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.55078125}{\ell_{i}}}}({\color[rgb]{0.28125,0.23828125,0.546875}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.546875}{{\color[rgb]{0.28125,0.23828125,0.546875}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.546875}{\texttt{\small
S}}}_{i}}}).\definecolor{currbkp}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H^{\dagger}_{1}}\color[rgb]{0.1,0.4,0.1}{}_{i}\\}_{i\in
I}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0})\;(\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{{{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\textbf{{p}}}}}!{{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\textbf{{q}}}}};\\{{{\color[rgb]{0.28125,0.23828125,0.55078125}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.55078125}{\ell_{i}}}}({\color[rgb]{0.28125,0.23828125,0.546875}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.546875}{{\color[rgb]{0.28125,0.23828125,0.546875}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.546875}{\texttt{\small
S}}}_{i}}}).\definecolor{currbkp}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H^{\dagger}_{2}}\color[rgb]{0.1,0.4,0.1}{}_{i}\\}_{i\in
I}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0})\;(\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{{{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\textbf{{p}}}}}!{{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\textbf{{q}}}}};\\{{{\color[rgb]{0.28125,0.23828125,0.55078125}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.55078125}{\ell_{j}}}}({\color[rgb]{0.28125,0.23828125,0.546875}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.546875}{{\color[rgb]{0.28125,0.23828125,0.546875}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.546875}{\texttt{\small
S}}}_{j}}}).\definecolor{currbkp}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H^{L}_{1}}\color[rgb]{0.1,0.4,0.1}{}_{j}\\}_{j\in
J}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0})\;(\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{{{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\textbf{{p}}}}}!{{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\textbf{{q}}}}};\\{{{\color[rgb]{0.28125,0.23828125,0.55078125}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.55078125}{\ell_{k}}}}({\color[rgb]{0.28125,0.23828125,0.546875}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.546875}{{\color[rgb]{0.28125,0.23828125,0.546875}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.546875}{\texttt{\small
S}}}_{k}}}).\definecolor{currbkp}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H^{L}_{2}}\color[rgb]{0.1,0.4,0.1}{}_{k}\\}_{k\in
K}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0})}}=\\\
\qquad((\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{{{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\textbf{{p}}}}}!{{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\textbf{{q}}}}};\\{{{\color[rgb]{0.28125,0.23828125,0.55078125}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.55078125}{\ell_{j}}}}({\color[rgb]{0.28125,0.23828125,0.546875}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.546875}{{\color[rgb]{0.28125,0.23828125,0.546875}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.546875}{\texttt{\small
S}}}_{j}}}).\definecolor{currbkp}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H^{1}_{1}}\color[rgb]{0.1,0.4,0.1}{}_{j}\\}_{j\in
J}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0},\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{{{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\textbf{{p}}}}}!{{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\textbf{{q}}}}};\\{{{\color[rgb]{0.28125,0.23828125,0.55078125}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.55078125}{\ell_{k}}}}({\color[rgb]{0.28125,0.23828125,0.546875}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.546875}{{\color[rgb]{0.28125,0.23828125,0.546875}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.546875}{\texttt{\small
S}}}_{k}}}).\definecolor{currbkp}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H^{1}_{2}}\color[rgb]{0.1,0.4,0.1}{}_{k}\\}_{k\in
K}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}),(\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{{{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\textbf{{p}}}}}!{{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\textbf{{q}}}}};\\{{{\color[rgb]{0.28125,0.23828125,0.55078125}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.55078125}{\ell_{j}}}}({\color[rgb]{0.28125,0.23828125,0.546875}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.546875}{{\color[rgb]{0.28125,0.23828125,0.546875}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.546875}{\texttt{\small
S}}}_{j}}}).\definecolor{currbkp}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H^{2}_{1}}\color[rgb]{0.1,0.4,0.1}{}_{j}\\}_{j\in
J}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0},\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{{{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\textbf{{p}}}}}!{{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\textbf{{q}}}}};\\{{{\color[rgb]{0.28125,0.23828125,0.55078125}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.55078125}{\ell_{k}}}}({\color[rgb]{0.28125,0.23828125,0.546875}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.546875}{{\color[rgb]{0.28125,0.23828125,0.546875}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.546875}{\texttt{\small
S}}}_{k}}}).\definecolor{currbkp}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H^{2}_{2}}\color[rgb]{0.1,0.4,0.1}{}_{k}\\}_{k\in
K}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}))\\\
\qquad\text{where $J\cup K=I$ and, for $n,m=1,2$,}\
\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{{\definecolor{currbkp}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H}\color[rgb]{0.1,0.4,0.1}{}^{n}_{m}}_{i}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}=\begin{cases}\pi_{n}(\pi_{m}({\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{{\sf
unmLP^{bin}}\;\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{{\definecolor{currbkp}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H^{\dagger}_{1}}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}}_{i}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\;\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{{\definecolor{currbkp}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H^{\dagger}_{2}}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}}_{i}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\;\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{{\definecolor{currbkp}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H^{L}_{1}}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}}_{i}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\;\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{{\definecolor{currbkp}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H^{L}_{2}}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}}_{i}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}}}))\
\text{if $i\in J\cup K$}\\\
\pi_{n}(\pi_{m}({\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{{\sf
unmLP^{bin}}\;\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{{\definecolor{currbkp}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H^{\dagger}_{1}}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}}_{i}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\;\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{{\definecolor{currbkp}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H^{\dagger}_{2}}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}}_{i}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\;\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{{\definecolor{currbkp}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H^{L}_{1}}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}}_{i}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\;\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{{\definecolor{currbkp}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H^{L}_{1}}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}}_{i}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}}}))\
\text{if $i\in J\backslash K$}\\\
\pi_{n}(\pi_{m}({\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{{\sf
unmLP^{bin}}\;\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{{\definecolor{currbkp}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H^{\dagger}_{1}}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}}_{i}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\;\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{{\definecolor{currbkp}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H^{\dagger}_{2}}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}}_{i}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\;\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{{\definecolor{currbkp}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H^{L}_{2}}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}}_{i}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\;\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{{\definecolor{currbkp}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H^{L}_{2}}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}}_{i}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}}}))\
\text{if $i\in K\backslash J$}\end{cases}\\\
{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{{\sf
unmLP^{bin}}\;(\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{{{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\textbf{{p}}}}}?{{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\textbf{{q}}}}};\\{{{\color[rgb]{0.28125,0.23828125,0.55078125}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.55078125}{\ell_{j}}}}({\color[rgb]{0.28125,0.23828125,0.546875}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.546875}{{\color[rgb]{0.28125,0.23828125,0.546875}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.546875}{\texttt{\small
S}}}_{j}}}).\definecolor{currbkp}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H^{\dagger}_{1}}\color[rgb]{0.1,0.4,0.1}{}_{j}\\}_{j\in
J}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0})\;(\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{{{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\textbf{{p}}}}}?{{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\textbf{{q}}}}};\\{{{\color[rgb]{0.28125,0.23828125,0.55078125}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.55078125}{\ell_{k}}}}({\color[rgb]{0.28125,0.23828125,0.546875}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.546875}{{\color[rgb]{0.28125,0.23828125,0.546875}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.546875}{\texttt{\small
S}}}_{k}}}).\definecolor{currbkp}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H^{\dagger}_{2}}\color[rgb]{0.1,0.4,0.1}{}_{k}\\}_{k\in
K}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0})\;(\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{{{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\textbf{{p}}}}}?{{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\textbf{{q}}}}};\\{{{\color[rgb]{0.28125,0.23828125,0.55078125}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.55078125}{\ell_{i}}}}({\color[rgb]{0.28125,0.23828125,0.546875}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.546875}{{\color[rgb]{0.28125,0.23828125,0.546875}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.546875}{\texttt{\small
S}}}_{i}}}).\definecolor{currbkp}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H^{L}_{1}}\color[rgb]{0.1,0.4,0.1}{}_{i}\\}_{i\in
I}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0})\;(\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{{{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\textbf{{p}}}}}?{{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\textbf{{q}}}}};\\{{{\color[rgb]{0.28125,0.23828125,0.55078125}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.55078125}{\ell_{i}}}}({\color[rgb]{0.28125,0.23828125,0.546875}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.546875}{{\color[rgb]{0.28125,0.23828125,0.546875}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.546875}{\texttt{\small
S}}}_{i}}}).\definecolor{currbkp}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H^{L}_{2}}\color[rgb]{0.1,0.4,0.1}{}_{i}\\}_{i\in
I}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0})}}=\\\
\qquad((\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{{{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\textbf{{p}}}}}?{{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\textbf{{q}}}}};\\{{{\color[rgb]{0.28125,0.23828125,0.55078125}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.55078125}{\ell_{j}}}}({\color[rgb]{0.28125,0.23828125,0.546875}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.546875}{{\color[rgb]{0.28125,0.23828125,0.546875}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.546875}{\texttt{\small
S}}}_{j}}}).\definecolor{currbkp}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H^{1}_{1}}\color[rgb]{0.1,0.4,0.1}{}_{j}\\}_{j\in
J}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0},\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{{{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\textbf{{p}}}}}?{{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\textbf{{q}}}}};\\{{{\color[rgb]{0.28125,0.23828125,0.55078125}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.55078125}{\ell_{j}}}}({\color[rgb]{0.28125,0.23828125,0.546875}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.546875}{{\color[rgb]{0.28125,0.23828125,0.546875}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.546875}{\texttt{\small
S}}}_{j}}}).\definecolor{currbkp}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H^{1}_{2}}\color[rgb]{0.1,0.4,0.1}{}_{j}\\}_{j\in
J}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}),(\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{{{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\textbf{{p}}}}}?{{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\textbf{{q}}}}};\\{{{\color[rgb]{0.28125,0.23828125,0.55078125}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.55078125}{\ell_{k}}}}({\color[rgb]{0.28125,0.23828125,0.546875}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.546875}{{\color[rgb]{0.28125,0.23828125,0.546875}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.546875}{\texttt{\small
S}}}_{k}}}).\definecolor{currbkp}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H^{2}_{1}}\color[rgb]{0.1,0.4,0.1}{}_{k}\\}_{k\in
K}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0},\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{{{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\textbf{{p}}}}}?{{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\textbf{{q}}}}};\\{{{\color[rgb]{0.28125,0.23828125,0.55078125}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.55078125}{\ell_{k}}}}({\color[rgb]{0.28125,0.23828125,0.546875}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.546875}{{\color[rgb]{0.28125,0.23828125,0.546875}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.546875}{\texttt{\small
S}}}_{k}}}).\definecolor{currbkp}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H^{2}_{2}}\color[rgb]{0.1,0.4,0.1}{}_{k}\\}_{k\in
K}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}))\\\
\qquad\text{where $J\cup K=I$ and, for $n,m=1,2$,}\
\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{{\definecolor{currbkp}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H}\color[rgb]{0.1,0.4,0.1}{}^{n}_{m}}_{i}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}=\begin{cases}\pi_{n}(\pi_{m}({\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{{\sf
unmLP^{bin}}\;\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{{\definecolor{currbkp}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H^{\dagger}_{1}}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}}_{i}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\;\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{{\definecolor{currbkp}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H^{\dagger}_{2}}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}}_{i}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\;\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{{\definecolor{currbkp}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H^{L}_{1}}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}}_{i}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\;\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{{\definecolor{currbkp}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H^{L}_{2}}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}}_{i}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}}}))\
\text{if $i\in J\cup K$}\\\
\pi_{n}(\pi_{m}({\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{{\sf
unmLP^{bin}}\;\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{{\definecolor{currbkp}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H^{\dagger}_{1}}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}}_{i}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\;\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{{\definecolor{currbkp}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H^{\dagger}_{1}}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}}_{i}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\;\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{{\definecolor{currbkp}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H^{L}_{1}}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}}_{i}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\;\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{{\definecolor{currbkp}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H^{L}_{2}}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}}_{i}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}}}))\
\text{if $i\in J\backslash K$}\\\
\pi_{n}(\pi_{m}({\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{{\sf
unmLP^{bin}}\;\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{{\definecolor{currbkp}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H^{\dagger}_{2}}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}}_{i}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\;\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{{\definecolor{currbkp}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H^{\dagger}_{2}}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}}_{i}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\;\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{{\definecolor{currbkp}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H^{L}_{1}}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}}_{i}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\;\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{{\definecolor{currbkp}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H^{L}_{2}}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}}_{i}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}}}))\
\text{if $i\in K\backslash J$}\end{cases}\\\
{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{{\sf
unmLP^{bin}}\;(\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\textbf{{p}}}}\to{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\textbf{{q}}}}:\\{{{\color[rgb]{0.28125,0.23828125,0.55078125}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.55078125}{\ell_{i}}}}({\color[rgb]{0.28125,0.23828125,0.546875}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.546875}{{\color[rgb]{0.28125,0.23828125,0.546875}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.546875}{\texttt{\small
S}}}_{i}}}).\definecolor{currbkp}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H^{\dagger}_{1}}\color[rgb]{0.1,0.4,0.1}{}_{i}\\}_{i\in
I}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0})\;(\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\textbf{{p}}}}\to{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\textbf{{q}}}}:\\{{{\color[rgb]{0.28125,0.23828125,0.55078125}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.55078125}{\ell_{i}}}}({\color[rgb]{0.28125,0.23828125,0.546875}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.546875}{{\color[rgb]{0.28125,0.23828125,0.546875}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.546875}{\texttt{\small
S}}}_{i}}}).\definecolor{currbkp}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H^{\dagger}_{2}}\color[rgb]{0.1,0.4,0.1}{}_{i}\\}_{i\in
I}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0})\;(\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\textbf{{p}}}}\to{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\textbf{{q}}}}:\\{{{\color[rgb]{0.28125,0.23828125,0.55078125}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.55078125}{\ell_{i}}}}({\color[rgb]{0.28125,0.23828125,0.546875}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.546875}{{\color[rgb]{0.28125,0.23828125,0.546875}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.546875}{\texttt{\small
S}}}_{i}}}).\definecolor{currbkp}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H^{L}_{1}}\color[rgb]{0.1,0.4,0.1}{}_{i}\\}_{i\in
I}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0})\;(\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\textbf{{p}}}}\to{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\textbf{{q}}}}:\\{{{\color[rgb]{0.28125,0.23828125,0.55078125}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.55078125}{\ell_{i}}}}({\color[rgb]{0.28125,0.23828125,0.546875}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.546875}{{\color[rgb]{0.28125,0.23828125,0.546875}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.546875}{\texttt{\small
S}}}_{i}}}).\definecolor{currbkp}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H^{L}_{2}}\color[rgb]{0.1,0.4,0.1}{}_{i}\\}_{i\in
I}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0})}}\\\
=((\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\textbf{{p}}}}\to{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\textbf{{q}}}}:\\{{{\color[rgb]{0.28125,0.23828125,0.55078125}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.55078125}{\ell_{i}}}}({\color[rgb]{0.28125,0.23828125,0.546875}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.546875}{{\color[rgb]{0.28125,0.23828125,0.546875}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.546875}{\texttt{\small
S}}}_{i}}}).\definecolor{currbkp}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H^{1}_{1}}\color[rgb]{0.1,0.4,0.1}{}_{i}\\}_{i\in
I}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0},\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\textbf{{p}}}}\to{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\textbf{{q}}}}:\\{{{\color[rgb]{0.28125,0.23828125,0.55078125}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.55078125}{\ell_{i}}}}({\color[rgb]{0.28125,0.23828125,0.546875}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.546875}{{\color[rgb]{0.28125,0.23828125,0.546875}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.546875}{\texttt{\small
S}}}_{i}}}).\definecolor{currbkp}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H^{1}_{2}}\color[rgb]{0.1,0.4,0.1}{}_{i}\\}_{i\in
I}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}),(\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\textbf{{p}}}}\to{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\textbf{{q}}}}:\\{{{\color[rgb]{0.28125,0.23828125,0.55078125}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.55078125}{\ell_{i}}}}({\color[rgb]{0.28125,0.23828125,0.546875}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.546875}{{\color[rgb]{0.28125,0.23828125,0.546875}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.546875}{\texttt{\small
S}}}_{i}}}).\definecolor{currbkp}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H^{2}_{1}}\color[rgb]{0.1,0.4,0.1}{}_{i}\\}_{i\in
I}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0},\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\textbf{{p}}}}\to{{\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\textbf{{q}}}}:\\{{{\color[rgb]{0.28125,0.23828125,0.55078125}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.55078125}{\ell_{i}}}}({\color[rgb]{0.28125,0.23828125,0.546875}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.546875}{{\color[rgb]{0.28125,0.23828125,0.546875}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.546875}{\texttt{\small
S}}}_{i}}}).\definecolor{currbkp}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H^{2}_{2}}\color[rgb]{0.1,0.4,0.1}{}_{i}\\}_{i\in
I}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}))\\\
\qquad\text{where, for $n,m=1,2$,}\
\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{{\definecolor{currbkp}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H}\color[rgb]{0.1,0.4,0.1}{}^{n}_{m}}_{i}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}=\pi_{n}(\pi_{m}({\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{{\sf
unmLP^{bin}}\;\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{{\definecolor{currbkp}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H^{\dagger}_{1}}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}}_{i}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\;\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{{\definecolor{currbkp}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H^{\dagger}_{2}}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}}_{i}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\;\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{{\definecolor{currbkp}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H^{L}_{1}}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}}_{i}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\;\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{{\definecolor{currbkp}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H^{L}_{2}}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}}_{i}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}}}))\\\\[5.69054pt]
\text{undefined otherwise}\end{array}$

The partial function _localiser-unmerge for projection merge_
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{{\sf
unmLP}\;L_{P}\;L_{L}}}$ takes as input two lists of types instead of two
pairs. It returns a tuple of lists: if
$L_{P}=[\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H^{\dagger}_{1}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0},\dots,\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{\definecolor{currbkp}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H^{\dagger}}\color[rgb]{0.1,0.4,0.1}{}_{n}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}]$
and
$L_{L}=[\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H^{L}_{1}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0},\dots,\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{\definecolor{currbkp}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H^{L}}\color[rgb]{0.1,0.4,0.1}{}_{m}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}]$
the result list is of the kind
$([\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{\definecolor{currbkp}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H}\color[rgb]{0.1,0.4,0.1}{}^{1}_{1}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0},\dots,\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{\definecolor{currbkp}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H}\color[rgb]{0.1,0.4,0.1}{}^{1}_{m}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}],\dots,[\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{\definecolor{currbkp}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H}\color[rgb]{0.1,0.4,0.1}{}^{n}_{1}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0},\dots,\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{\definecolor{currbkp}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H}\color[rgb]{0.1,0.4,0.1}{}^{n}_{m}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}])$
($\pi_{i}$ indicate the standard projection of the $i$-th component of the
tuple).
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{\sf
unmLP}}$ is defined by recursion (on the sum of the lengths of $L_{P}$ and
$L_{L}$) by the following equations.

$\begin{array}[]{l}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{{\sf
unmLP}\;[]\;L_{L}}}=([])\\\
{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{{\sf
unmLP}\;[\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H^{\dagger}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}]\;L_{L}}}=([L_{L}])\\\
{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{{\sf
unmLP}\;[\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H^{\dagger}_{1}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0},\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H^{\dagger}_{2}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}]\;L_{L}}}=\begin{cases}([],[])\
\text{if $L_{L}=[]$}\\\
([\pi_{1}(\pi_{1}({\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{{\sf
unmLP^{bin}}\;\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H^{\dagger}_{1}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\;\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H^{\dagger}_{2}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\;\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H^{L}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\;\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H^{L}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}}})),\pi_{1}(\pi_{2}({\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{{\sf
unmLP^{bin}}\;\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H^{\dagger}_{1}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\;\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H^{\dagger}_{2}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\;\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H^{L}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\;\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H^{L}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}}}))])\
\text{if
$L_{L}=[\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H^{L}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}]$}\\\
([\pi_{1}(\pi_{1}({\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{{\sf
unmLP^{bin}}\;\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H^{\dagger}_{1}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\;\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H^{\dagger}_{2}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\;\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H^{L}_{1}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\;\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H^{L}_{2}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}}})),\pi_{2}(\pi_{1}({\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{{\sf
unmLP^{bin}}\;\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H^{\dagger}_{1}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\;\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H^{\dagger}_{2}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\;\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H^{L}_{1}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\;\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H^{L}_{2}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}}}))],\\\
\ \
[\pi_{1}(\pi_{2}({\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{{\sf
unmLP^{bin}}\;\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H^{\dagger}_{1}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\;\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H^{\dagger}_{2}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\;\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H^{L}_{1}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\;\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H^{L}_{2}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}}})),\pi_{2}(\pi_{2}({\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{{\sf
unmLP^{bin}}\;\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H^{\dagger}_{1}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\;\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H^{\dagger}_{2}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\;\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H^{L}_{1}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\;\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H^{L}_{2}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}}}))])\
\text{if
$L_{L}=[\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H^{L}_{1}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0},\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H^{L}_{2}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}]$}\\\
(\pi_{1}(\pi_{1}(U))\\#L^{1},\pi_{1}(\pi_{2}(U))\\#L^{2})\\\ \qquad\text{if
$L_{L}=[\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H^{L}_{1}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0},\dots,\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{\definecolor{currbkp}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H^{L}}\color[rgb]{0.1,0.4,0.1}{}_{m}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}]$,
where, for $i=1,2$}\\\ \qquad
L^{i}=\pi_{i}({\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{{\sf
unmLP}\;[(\pi_{2}(\pi_{1}(U))),(\pi_{2}(\pi_{2}(U)))]\;[\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H^{L}_{2}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0},\dots,\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{\definecolor{currbkp}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H^{L}}\color[rgb]{0.1,0.4,0.1}{}_{m}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}]}})\
\text{and}\\\ \qquad
U={\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{{\sf
unmLP^{bin}}\;\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H^{\dagger}_{1}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\;\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H^{\dagger}_{2}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\;\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H^{L}_{1}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\;(\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{\bigsqcup^{L}}_{k=2\dots
m}\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{\definecolor{currbkp}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H^{L}}\color[rgb]{0.1,0.4,0.1}{}_{k}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0})}}\end{cases}\\\
{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{{\sf
unmLP}\;[\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H^{\dagger}_{1}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0},\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H^{\dagger}_{2}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0},\dots,\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{\definecolor{currbkp}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H^{\dagger}}\color[rgb]{0.1,0.4,0.1}{}_{n}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}]\;L_{L}}}=(L^{1},\pi_{1}({\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{{\sf
unmLP}\;[\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H^{\dagger}_{2}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0},\dots,\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{\definecolor{currbkp}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H^{\dagger}}\color[rgb]{0.1,0.4,0.1}{}_{n}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}]\;L^{2}}}),\dots,\pi_{n-1}({\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{{\sf
unmLP}\;[\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H^{\dagger}_{2}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0},\dots,\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{\definecolor{currbkp}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H^{\dagger}}\color[rgb]{0.1,0.4,0.1}{}_{n}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}]\;L^{2}}}))\\\
\qquad\text{where, for $i=1,2$,}\
L^{i}={\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{{\sf
unmLP}\;[\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H^{\dagger}_{1}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0},(\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{\bigsqcup}_{k=2,\dots,n}\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{\definecolor{currbkp}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H^{\dagger}}\color[rgb]{0.1,0.4,0.1}{}_{k}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0})]\;L_{L}}}\end{array}$

###### Lemma B.9.

We are given hybrid types
$\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H^{\dagger}_{1}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0},\dots,\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{\definecolor{currbkp}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H^{\dagger}}\color[rgb]{0.1,0.4,0.1}{}_{n}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}$
and
$\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H^{L}_{1}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0},\dots,\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{\definecolor{currbkp}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H^{L}}\color[rgb]{0.1,0.4,0.1}{}_{m}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}$,
such that
$\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{\bigsqcup}_{i=1,\dots,n}\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H^{\dagger}_{i}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}=\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{\bigsqcup^{L}}_{j=1,\dots,m}\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{\definecolor{currbkp}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H^{L}}\color[rgb]{0.1,0.4,0.1}{}_{j}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}$.
Then $\
{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{{\sf
unmLP}\;[\;\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H^{\dagger}_{1}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}}},\dots,\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{\definecolor{currbkp}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H^{\dagger}}\color[rgb]{0.1,0.4,0.1}{}_{n}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}][\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H^{L}_{1}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0},\dots,\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{\definecolor{currbkp}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H^{L}}\color[rgb]{0.1,0.4,0.1}{}_{m}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}]\
$ is defined and, if we set

${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{{\sf
unmLP}\;[\;\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H^{\dagger}_{1}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}}},\dots,\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{\definecolor{currbkp}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H^{\dagger}}\color[rgb]{0.1,0.4,0.1}{}_{n}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}][\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H^{L}_{1}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0},\dots,\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{\definecolor{currbkp}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H^{L}}\color[rgb]{0.1,0.4,0.1}{}_{m}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}]=([\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{\definecolor{currbkp}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H^{L}}\color[rgb]{0.1,0.4,0.1}{}^{1}_{1}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0},\dots,\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{\definecolor{currbkp}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H^{L}}\color[rgb]{0.1,0.4,0.1}{}^{1}_{m}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}],\dots,[\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{\definecolor{currbkp}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H^{L}}\color[rgb]{0.1,0.4,0.1}{}^{n}_{1}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0},\dots,\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{\definecolor{currbkp}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H^{L}}\color[rgb]{0.1,0.4,0.1}{}^{n}_{m}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}])\text{,}$

we have that:

  * •

$\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{\bigsqcup^{L}}_{j=1,\dots,m},\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{\definecolor{currbkp}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H^{L}}\color[rgb]{0.1,0.4,0.1}{}^{i}_{j}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}=\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H^{\dagger}_{i}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}$,
for all $i=1,\dots,n$, and

  * •

$\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{\bigsqcup}_{i=1,\dots,n},\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{\definecolor{currbkp}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H^{L}}\color[rgb]{0.1,0.4,0.1}{}^{i}_{j}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}=\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{\definecolor{currbkp}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H^{L}}\color[rgb]{0.1,0.4,0.1}{}_{j}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}$,
for all $j=1,\dots,n$.

###### Proof.

  * •

We first prove the base cases, in particular the case in which $n=2$ and $m=2$
(formally we first prove the result for
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{\sf
unmLP^{bin}}}$). This is done by structural induction on
$\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H^{\dagger}_{1}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}$,
exploiting the hypothesis and the inductive nature both of
$\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{\sqcup}$
and
$\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{\sqcup^{L}}$.

  * •

We conclude by induction on $n+m$, by following the definition of
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{\sf
unmLP}}$.

∎

We now define the unmerge for the localiser (Definition B.10) and ensure that
it has the desired behaviour (Lemma B.11).

###### Definition B.10 (Localiser Unmerge).

The partial function _binary unmerge for localiser_
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{{\sf
unmL^{bin}_{E}}\;\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H^{\dagger}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\;\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H^{L}_{1}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\;\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H^{L}_{2}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}}}$
is defined if
${\textsf{ipart}}({\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H^{L}_{1}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}})\cup{\textsf{ipart}}({\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H^{L}_{2}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}})\subseteq
E$ by the following equations, by recursion on
$\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{\sf{depth}}(\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H^{\dagger}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0})$,
whenever the recursive call is defined (we use $\pi_{1}$ and $\pi_{2}$ to
indicate standard pair projections; we also make implicit the dependency on
$E$ using the notation
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{\sf
unmL^{bin}}}$ instead of $ulbE$):

$\begin{array}[]{l}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{{\sf
unmL^{bin}}\;\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{\mathtt{end}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\;\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H^{L}_{1}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\;\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H^{L}_{2}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}}}=(\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{\mathtt{end}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0},\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{\mathtt{end}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0})\\\
{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{{\sf
unmL^{bin}}\;\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{X}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\;\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H^{L}_{1}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\;\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H^{L}_{2}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}}}=(\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{X}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0},\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{X}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0})\\\
{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{{\sf
unmL^{bin}}\;(\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{\mu\definecolor{currbkp}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{X}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}.\definecolor{currbkp}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H^{\dagger}}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0})\;\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H^{L}_{1}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\;\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H^{L}_{2}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}}}=\begin{cases}(\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{\mu\definecolor{currbkp}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{X}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}.\pi_{1}({\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{{\sf
unmL^{bin}}\;\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H^{\dagger}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\;\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{{H^{L}_{1}}^{\prime}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\;\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{{H^{L}_{2}}^{\prime}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}}})}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0},\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{\mu\definecolor{currbkp}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{X}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}.\pi_{2}({\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{{\sf
unmL^{bin}}\;\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H^{\dagger}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\;\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{{H^{L}_{1}}^{\prime}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\;\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{{H^{L}_{2}}^{\prime}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}}})}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0})\\\
\qquad\text{if
$\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H^{L}_{1}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}=\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{\mu\definecolor{currbkp}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{X}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}.\definecolor{currbkp}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{{H^{L}_{1}}^{\prime}}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}$
and
$\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H^{L}_{2}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}=\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{\mu\definecolor{currbkp}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{X}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}.\definecolor{currbkp}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{{H^{L}_{2}}^{\prime}}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}$}\\\
(\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{\mu\definecolor{currbkp}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{X}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}.\definecolor{currbkp}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H^{\dagger}}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0},\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{\mu\definecolor{currbkp}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{X}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}.\definecolor{currbkp}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H^{\dagger}}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0})\
\text{if
$\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H^{L}_{1}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}=\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H^{L}_{2}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}=\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{\mathtt{end}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}$}\end{cases}\\\
{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{{\sf
unmL^{bin}}\;(\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{\definecolor{currbkp}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H^{\dagger}_{1}}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}|\definecolor{currbkp}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H^{\dagger}_{2}}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0})\;\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H^{L}_{1}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\;\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H^{L}_{2}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}}}=\begin{cases}(\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{(\pi_{1}({\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{{\sf
unmL^{bin}}\;\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H^{\dagger}_{1}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\;\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H^{L}_{1}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\;\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H^{L}_{2}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}}}))|\definecolor{currbkp}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H^{\dagger}_{2}}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0},\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{(\pi_{2}({\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{{\sf
unmL^{bin}}\;\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H^{\dagger}_{1}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\;\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H^{L}_{1}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\;\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H^{L}_{2}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}}}))|\definecolor{currbkp}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H^{\dagger}_{2}}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0})\
\\\ \qquad\text{if
$E\cap{\textsf{ipart}}({\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H^{\dagger}_{2}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}})=\emptyset$}\\\
(\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{\definecolor{currbkp}{rgb}{0.1,0.4,0.1}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}{H^{\dagger}_{1}}\color[rgb]{0.1,0.4,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.4,0.1}|(\pi_{1}({\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{{\sf