only non-algorithmic detail of the presentation was constructing $\mathcal{U}$
in F:Rec; in the implementation, we add $t\rightarrow\mathsf{Ty}$ to the
context instead of $\nu t.\mathcal{U}\rightarrow\mathsf{Ty}$. This means the
context contains non-well-formed VS types, which makes the theory more
unwieldy but yields a convenient implementation. When processing a type
declaration, GML generates the associated VS type, and also generates a
constructor and deconstructor function for each constructor. Constructor
applications are desugared to ordinary applications of the constructor
function and the deconstructor function is used during pattern matching.
Another major challenge is implementing unification on vertex structures. At
the moment, our implementation uses a set of heuristics that are not
guaranteed to be complete (i.e., unification may fail for VSs that could be
unified, resulting in a spurious type error) but work well in practice on the
large examples tested.

In addition to extending the subset of OCaml supported by GML, we have also
substantially re-architected the code. In GMLμ, the graph type checker is
completely separate from the type checker. This simplifies the implementation
and has a number of other benefits. First, all futures in a program are known
by the time graph checking begins. This allows the implementation to infer
graph types in several instances where type annotations would previously have
been required (one such instance is noted in prior work (Muller, 2022) as a
limitation of GML, which is not a limitation of GMLμ). Additionally, this
architecture would simplify the process of integrating graph checking as an
extension of the OCaml compiler, as an additional pass on type-checked ASTs.

###  6.1. Examples

To show the utility of GMLμ, we discuss several example programs for which it
can infer and visualize graph types.

#### Produce-consume

The producer-consumer example of Blelloch and Reid-Miller (1997), shown in
Figure 28, is similar to the  function of Figure 5, but allows the pipelined
list to be finite (ending with ). As in the pipeline example, the  constructor
allows the tail of the  to continue being computed in a future. We compose ,
which (for the sake of a simple example) outputs a list of the numbers 1–n,
with the  function which calculates the sum of the list. In the graph of the
composed functions (right side of the figure), the touches of  happen in
parallel with the production of the list.

⬇

Figure 28. Blelloch-Reid-Miller produce-consume example

#### Tree Sum

In Figure 29, we present operations on a pipelined tree data structure
(Blelloch and Reid-Miller, 1997). As with , the two subtrees of an  are
futures, so they may be computed asynchronously while the value at the node is
used. The function  generates a tree of numbers 0 to 10, then  calculates the
sum of elements in the generated tree. While the particular application of
summing a binary tree is fairly simple, one can imagine using the same
structure for more complicated use-cases. Because of the design of the data
structure,  immediately returns a future and then  can perform its calculation
as later recursive steps of  are still executing.

⬇

Figure 29. Sum over elements in a pipelined tree.

#### Tree Reverse

The function in Figure 30 reverses a pipelined tree of the type defined in
Figure 29. Here, the interesting feature of the output was not the
visualization of the function’s graph type, which shows a similar structure to
and , but the function type, which is

$\mathsf{reverse}:\Pi[u_{f}\\!:\\!\mathsf{vtree};u_{t}\\!:\\!\mathsf{vtree}].\mathsf{ftree}~{}u_{t}\xrightarrow{G}\mathsf{ftree}~{}u_{f}$

where $\mathsf{vtree}=\nu t.t\times\blacklozenge\times t\times\blacklozenge$.
We omit the graph type $G$ for clarity. The function takes two VS parameters
and a tree indexed by $u_{t}$ and returns a tree indexed by $u_{f}$.

⬇

Figure 30. Reverse a pipelined tree.

At first glance, this may seem imprecise because one might expect the VSs
parameterizing the input and output tree to be related (after all, the output
tree is the reverse of the input). However, this is not correct:  touches (in
a pipelined way) all of the futures of the input tree and constructs a new
tree with the reversed values but new futures from the VS $u_{f}$. Here, not
just the graph type but the return type parameterized by its VS can correct a
misunderstanding about the parallel behavior of a program.

###  6.2. Limitations

Though our inference algorithm checks most useful programs, there are some
limitations. First, polymorphic types cannot be instantiated with types that
include futures. For example, a list of futures would have to be explicitly
defined as a new type  rather than by instantiating built-in lists to form the
type . This represents a design trade-off; graph types are not currently
expressive enough to represent, say, a  function on lists of futures. If the
standard list type could be instantiated with a future, the polymorphic
function would need to be assigned a general enough type to cover all
instantiations of , which wouldn’t be possible. A limitation we inherit from
GML is that functional arguments of higher order functions cannot spawn
futures. This is possible in $\lambda^{G\mu}$, but cannot be inferred without
annotations.

##  7\. Related Work

#### Graph Types and Related Analyses.

The use of graphs to represent the parallel programs dates back to at least
the late 1960s (Karp and Miller, 1966; Rodriguez Bezos, 1969). Our notation is
most directly inspired by the work of Blelloch and Greiner (1995, 1996) and
Spoonhower (2009), who extended these graphs with notations for futures. In
this work, graphs were produced dynamically from programs using a cost
semantics, which abstractly evaluates the program to form the graph (or a
family of graphs if execution is nondeterministically). The first work we are
aware of on statically approximating such graphs for fine-grained parallel
programs was the prior work of one of us (Muller, 2022), which developed a
calculus $\lambda^{G}$ and corresponding graph type system for inferring graph
types of parallel programs with futures. Our work builds on $\lambda^{G}$,
including the use of an affine type system to ensure that vertex names are
unique and therefore do not appear twice in a graph, which would result in an
invalid graph. However, the main thrust of this paper is overcoming the
significant limitation in $\lambda^{G}$ that affine treatment of vertex names
prevents building collections of futures.

Dependency graphs are frequently used to represent control dependencies in
coarse-grained parallel programs and these have been the target of several
static analyses (e.g., (Chen et al., 2002; Cheng, 1993; Kasahara et al.,
1995)) but such tools do not contend with the substantial dynamicity inherent
in fine-grained parallel programs, especially those with futures. Dependency
graphs are also used to represent other dependencies in a program, including
data dependencies; analyzing the structure of such dependencies is a form of
program slicing (e.g., (Weiser, 1984; Korel, 1987)).

As observed in prior work (Muller, 2022), graph type systems draw on ideas
from region type systems (Tofte and Talpin, 1997), where assigning a vertex to
a future corresponds to allocating an object within a region of memory, in
order to aid in memory management and/or ensure safety (e.g. (Fluet et al.,
2006)), including in the presence of concurrency and complex, dynamic data
structures (Milano et al., 2022). It is not possible to list all of the
related work on regions and related systems, so we refer the interested reader
to the chapter by Henglein et al. (2005). Two major differences with region
systems are that vertex assignments must be unique (whereas typically many
objects are allocated within a single region) and that, to generate useful
graphs, we wish for vertex assignments to be visible at a global scope (see
the example from the Introduction of why locally allocated vertices are not
suitable for graph types of data structures).

#### Heterogeneous and Indexed Data Structures.

Indexed types (Zenger, 1997; Xi and Pfenning, 1999), a limited form of
dependent types in which a type is indexed by a value from a specified domain,
have long been used to add expressiveness to types—a classic example is a type
of vectors indexed with a natural number giving the vector’s length. We index
recursive data types with a vertex structure to assign unique vertices to
futures in recursive data structures. Vertex structures have a non-trivial
semantics of their own but are not first-class objects at the expression
level, so computation on VSs may be seen as an instance of type-level
computation. A similar indexing idea and type-level computation have been
previously combined to achieve heterogeneity in HList (Kiselyov et al., 2004),
a Haskell library that expresses heterogeneous lists by indexing the list type
constructor with a type-level list. Their work does not appear to generalize
beyond lists or to infinite indices.

Richer forms of type-level computation have been explored, and could be used
to further generalize the theory of vertex structures. Yorgey et al. (2012)
extend Haskell’s kind system with features for expressing a variety of type-
level data structures. As another example, we have considered extending vertex
structures with sums (so a vertex structure could, e.g., represent a finite
list) and using type-level matching (Blanvillain et al., 2022) to constrain
the lengths of lists by the length of the vertex structure parameter. While
this would expand the expressiveness of vertex structures, extending VSs
beyond tree-like corecursive structures causes a problem for inference and so
it seems likely that such an extension would require programmer annotations in
some cases.

We note that this paper enters a rich design space of combining data and
codata (e.g. (Thibodeau et al., 2016)). We have shown in Section 5 that any
data type can be “overapproximated by” a codata type in the sense that there
is a straightforward, local mapping from nodes in the data type’s AST to those
of the codata type (the vertex structure in our case). Whether this has a
deeper meaning in the theory of data and codata is left to future work.

#### Affine Type Systems.

We use an affine type system to handle vertex structures and ensure that
vertex names in output graphs are unique. Affine type systems have been used
in a number of languages to ensure safe usage of resources (broadly
construed), notably including Cyclone (Jim et al., 2002) and Rust (Rus,
[n.d.]). Our notation for splitting and availability is inspired by Cogent
(O’Connor et al., 2021), which uses these ideas for an affine treatment of
record types.

#### Encoding in Rust.

As a memory safety focused language, Rust’s type system would likely benefit
from the features GML. Though Rust is able to encode other type systems such
as session types (Jespersen et al., 2015; Lagaillardie et al., 2020), we do
not believe GML could be usefully or at least conveniently encoded in Rust as
is. The main limiting factor we forsee is that we believe each vertex name
would need its own lifetime. This is a problem because Rust requires all
lifetimes to be declared statically, and each piece of code can only refer to
finitely many lifetimes. However, in GML, vertex names are generated
dynamically, therefore a function might manipulate infinitely many vertices.

##  8\. Conclusion

We have presented a type system for annotating parallel programs with futures
with graph types, which compactly represent the parallel structure of the
program. Unlike prior work, we support complex data structures containing
futures. As evidenced by our prototype implementation, it is possible to infer
these graph types automatically for examples that use this feature for
efficient pipelined algorithms. Our implementation is also able to generate
visualizations of the resulting graph types, which can aid in understanding
the structure of parallel code and finding bugs.

In the future, we hope to expand on the types of program analysis and bug-
finding that can be done with these graph types. For example, we could build
on the prototype analyses of Muller (2022) to study deadlock and asymptotic
complexity in the complex, pipelined graphs that arise from programs with data
structures of futures. We also plan to scale the implementation up to support
a larger subset of OCaml, with the goal of integrating the analysis into the
OCaml compiler. Finally, because the graph type system itself does not depend
on a particular source language, we plan to explore implementing the graph
type system in front-ends for a variety of languages, so that more programmers
can benefit from graph types as an analysis tool and reasoning aid.

## References

  * (1)
  * Rus ([n.d.]) [n.d.].  The Rust language.  https://www.rust-lang.org.  Accessed: 2023-07-07.
  * Babaoğlu et al. (1993) Özalp Babaoğlu, Keith Marzullo, and Fred B. Schneider. 1993\.  A Formalization of Priority Inversion.  _Real-Time Systems_ 5, 4 (1993), 285–303.  https://doi.org/10.1007/BF01088832
  * Banerjee et al. (2006) Utpal Banerjee, Brian Bliss, Zhiqiang Ma, and Paul Petersen. 2006.  A Theory of Data Race Detection. In _Proceedings of the 2006 Workshop on Parallel and Distributed Systems: Testing and Debugging_ (Portland, Maine, USA) _(PADTAD ’06)_. Association for Computing Machinery, New York, NY, USA, 69–78.  https://doi.org/10.1145/1147403.1147416
  * Blanvillain et al. (2022) Olivier Blanvillain, Jonathan Immanuel Brachthäuser, Maxime Kjaer, and Martin Odersky. 2022\.  Type-level programming with match types.  _Proceedings of the ACM on Programming Languages_ 6 (1 2022).  Issue POPL. https://doi.org/10.1145/3498698 We could use something like this to give stronger guarantees with VSs, e.g., have some finite VSs.
  * Blelloch and Greiner (1995) Guy Blelloch and John Greiner. 1995.  Parallelism in Sequential Functional Languages. In _Proceedings of the Seventh International Conference on Functional Programming Languages and Computer Architecture_ (La Jolla, California, USA) _(FPCA ’95)_. Association for Computing Machinery, New York, NY, USA, 226–237.  https://doi.org/10.1145/224164.224210
  * Blelloch and Greiner (1996) Guy E. Blelloch and John Greiner. 1996.  A Provable Time and Space Efficient Implementation of NESL. In _Proceedings of the First ACM SIGPLAN International Conference on Functional Programming_ (Philadelphia, Pennsylvania, USA) _(ICFP ’96)_. Association for Computing Machinery, New York, NY, USA, 213–225.  https://doi.org/10.1145/232627.232650
  * Blelloch and Reid-Miller (1997) Guy E. Blelloch and Margaret Reid-Miller. 1997.  Pipelining with Futures. In _Proceedings of the Ninth Annual ACM Symposium on Parallel Algorithms and Architectures_ (Newport, Rhode Island, USA) _(SPAA ’97)_. Association for Computing Machinery, New York, NY, USA, 249–259.  https://doi.org/10.1145/258492.258517
  * Chen et al. (2002) Zhenqiang Chen, Baowen Xu, Jianjun Zhao, and Hongji Yang. 2002\.  Static Dependency Analysis for Concurrent Ada 95 Programs. In _Reliable Software Technologies — Ada-Europe 2002_ , Johann Blieberger and Alfred Strohmeier (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 219–230.  https://doi.org/10.1007/3-540-48046-3_17
  * Cheng (1993) Jingde Cheng. 1993\.  Process dependence net of distributed programs and its applications in development of distributed systems. In _Proceedings of 1993 IEEE 17th International Computer Software and Applications Conference COMPSAC ’93_. 231–240.  https://doi.org/10.1109/CMPSAC.1993.404187
  * Cogumbreiro et al. (2018) Tiago Cogumbreiro, Raymond Hu, Francisco Martins, and Nobuko Yoshida. 2018.  Dynamic Deadlock Verification for General Barrier Synchronisation.  _ACM Trans. Program. Lang. Syst._ 41, 1, Article 1 (Dec. 2018), 38 pages.  https://doi.org/10.1145/3229060
  * Fluet et al. (2006) Matthew Fluet, Greg Morrisett, and Amal Ahmed. 2006\.  Linear Regions Are All You Need. In _Proceedings of the 15th European Conference on Programming Languages and Systems_ (Vienna, Austria) _(ESOP’06)_. Springer-Verlag, Berlin, Heidelberg, 7–21.  https://doi.org/10.1007/11693024_2
  * Gansner and North (2000) Emden R. Gansner and Stephen C. North. 2000.  An Open Graph Visualization System and Its Applications to Software Engineering.  _Softw. Pract. Exper._ 30, 11 (Sept. 2000), 1203–1233.  https://doi.org/10.1002/1097-024X(200009)30:11<1203::AID-SPE338>3.0.CO;2-N
  * Henglein et al. (2005) Fritz Henglein, Henning Makholm, and Henning Niss. 2005\.  Effect Types and Region-Based Memory Management.  In _Advanced Topics in Types and Programming Languages_ , Benjamin C. Pierce (Ed.). MIT Press, Cambridge, Massachusetts, Chapter 3, 87–135.
  * Jespersen et al. (2015) Thomas Bracht Laumann Jespersen, Philip Munksgaard, and Ken Friis Larsen. 2015.  Session Types for Rust. In _Proceedings of the 11th ACM SIGPLAN Workshop on Generic Programming_ (Vancouver, BC, Canada) _(WGP 2015)_. Association for Computing Machinery, New York, NY, USA, 13–22.  https://doi.org/10.1145/2808098.2808100
  * Jim et al. (2002) Trevor Jim, J. Greg Morrisett, Dan Grossman, Michael W. Hicks, James Cheney, and Yanling Wang. 2002.  Cyclone: A Safe Dialect of C. In _Proceedings of the General Track of the Annual Conference on USENIX Annual Technical Conference_ _(ATEC ’02)_. USENIX Association, USA, 275–288.
  * Karp and Miller (1966) Richard M. Karp and Rayamond E. Miller. 1966.  Properties of a Model for Parallel Computations: Determinacy, Termination, Queueing.  _SIAM J. Appl. Math._ 14, 6 (1966), 1390–1411.  https://doi.org/10.1137/0114108
  * Kasahara et al. (1995) Y. Kasahara, Y. Nomura, M. Kamachi, J. Cheng, and K. Ushijima. 1995.  An integrated support environment for distributed software development based on unified program representations. In _Proceedings 1995 Asia Pacific Software Engineering Conference_. 254–263.  https://doi.org/10.1109/APSEC.1995.496974
  * Kiselyov et al. (2004) Oleg Kiselyov, Ralf Lämmel, and Keean Schupke. 2004\.  Strongly typed heterogeneous collections.  _Proceedings of the ACM SIGPLAN 2004 Haskell Workshop, Haskell’04_ (2004), 96–107.  https://doi.org/10.1145/1017472.1017488
  * Korel (1987) Bogdan Korel. 1987\.  The program dependence graph in static program testing.  _Inform. Process. Lett._ 24, 2 (1987), 103–108.  https://doi.org/10.1016/0020-0190(87)90102-5
  * Lagaillardie et al. (2020) Nicolas Lagaillardie, Rumyana Neykova, and Nobuko Yoshida. 2020\.  Implementing Multiparty Session Types in Rust. In _Coordination Models and Languages: 22nd IFIP WG 6.1 International Conference, COORDINATION 2020, Held as Part of the 15th International Federated Conference on Distributed Computing Techniques, DisCoTec 2020, Valletta, Malta, June 15–19, 2020, Proceedings_ (Valletta, Malta). Springer-Verlag, Berlin, Heidelberg, 127–136.  https://doi.org/10.1007/978-3-030-50029-0_8
  * Milano et al. (2022) Mae Milano, Joshua Turcotti, and Andrew C. Myers. 2022\.  A Flexible Type System for Fearless Concurrency. In _Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation_ (San Diego, CA, USA) _(PLDI 2022)_. Association for Computing Machinery, New York, NY, USA, 458–473.  https://doi.org/10.1145/3519939.3523443
  * Muller (2022) Stefan K. Muller. 2022\.  Static Prediction of Parallel Computation Graphs.  _Proc. ACM Program. Lang._ 6, POPL, Article 46 (jan 2022), 31 pages.  https://doi.org/10.1145/3498708
  * O’Connor et al. (2021) Liam O’Connor, Zilin Chen, Christine Rizkallah, Vincent Jackson, Sidney Amani, Gerwin Klein, Toby Murray, Thomas Sewell, and Gabriele Keller. 2021.  Cogent: uniqueness types and certifying compilation.  _J. Funct. Program._ 31 (2021), e25.  https://doi.org/10.1017/S095679682100023X
  * Rodriguez Bezos (1969) Jorge E Rodriguez Bezos. 1969\.  _A Graph Model for Parallel Computations_.  Ph.D. Dissertation. Massachusetts Institute of Technology, Cambridge, Massachusetts.
  * Sivaramakrishnan et al. (2020) K. C. Sivaramakrishnan, Stephen Dolan, Leo White, Sadiq Jaffer, Tom Kelly, Anmol Sahoo, Sudha Parimala, Atul Dhiman, and Anil Madhavapeddy. 2020\.  Retrofitting parallelism onto OCaml.  _Proc. ACM Program. Lang._ 4, ICFP (2020), 113:1–113:30.  https://doi.org/10.1145/3408995
  * Spoonhower (2009) Daniel Spoonhower. 2009\.  _Scheduling Deterministic Parallel Programs_.  Ph.D. Dissertation. Carnegie Mellon University, Pittsburgh, PA, USA.
  * Thibodeau et al. (2016) David Thibodeau, Andrew Cave, and Brigitte Pientka. 2016\.  Indexed Codata Types. In _Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming_ (Nara, Japan) _(ICFP 2016)_. Association for Computing Machinery, New York, NY, USA, 351–363.  https://doi.org/10.1145/2951913.2951929
  * Tofte and Talpin (1997) Mads Tofte and Jean-Pierre Talpin. 1997.  Region-Based Memory Management.  _Information and Computation_ 132, 2 (1997), 109–176.  https://doi.org/10.1006/inco.1996.2613
  * Weiser (1984) Mark Weiser. 1984\.  Program Slicing.  _IEEE Transactions on Software Engineering_ SE-10, 4 (1984), 352–357.  https://doi.org/10.1109/TSE.1984.5010248
  * Xi and Pfenning (1999) Hongwei Xi and Frank Pfenning. 1999.  Dependent Types in Practical Programming. In _Proceedings of the 26th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages_ (San Antonio, Texas, USA) _(POPL ’99)_. Association for Computing Machinery, New York, NY, USA, 214–227.  https://doi.org/10.1145/292540.292560
  * Yorgey et al. (2012) Brent A. Yorgey, Stephanie Weirich, Julien Cretin, Simon Peyton Jones, Dimitrios Vytiniotis, and José Pedro Magalhães. 2012\.  Giving Haskell a Promotion. In _Proceedings of the 8th ACM SIGPLAN Workshop on Types in Language Design and Implementation_ (Philadelphia, Pennsylvania, USA) _(TLDI ’12)_. Association for Computing Machinery, New York, NY, USA, 53–66.  https://doi.org/10.1145/2103786.2103795
  * Zenger (1997) Christoph Zenger. 1997\.  Indexed types.  _Theoretical Computer Science_ 187, 1 (1997), 147–165.  https://doi.org/10.1016/S0304-3975(97)00062-5

##  Appendix A From Section 3

(U:OmegaGen) $\displaystyle\displaystyle{\hbox{\hskip 0.0pt\vbox{\hbox{\hskip
0.0pt\hbox{\hskip 0.0pt\hbox{}}}\vbox{\hbox{\hskip
0.0pt\hbox{}}\vbox{}}}}\over\hbox{\hskip
45.14929pt\vbox{\vbox{}\hbox{\hskip-45.14929pt\hbox{\hbox{$\displaystyle\displaystyle\Omega,\vec{u}:\mathcal{U};\Psi\vdash\mathsf{gen}(\vec{u}):\mathcal{U}$}}}}}}$
(U:PsiGen) $\displaystyle\displaystyle{\hbox{\hskip 0.0pt\vbox{\hbox{\hskip
0.0pt\hbox{\hskip 0.0pt\hbox{}}}\vbox{\hbox{\hskip
0.0pt\hbox{}}\vbox{}}}}\over\hbox{\hskip
43.48267pt\vbox{\vbox{}\hbox{\hskip-43.48265pt\hbox{\hbox{$\displaystyle\displaystyle\Omega;\Psi,\vec{u}:\mathcal{U}\vdash\mathsf{gen}(\vec{u}):\mathcal{U}$}}}}}}$
(OM:Gen) $\displaystyle\displaystyle{\hbox{\hskip
26.41106pt\vbox{\hbox{\hskip-26.41104pt\hbox{\hbox{$\displaystyle\displaystyle\Omega\rightsquigarrow\Omega_{1}\boxplus\Omega_{2}$}}}\vbox{}}}\over\hbox{\hskip
44.61598pt\vbox{\vbox{}\hbox{\hskip-44.61597pt\hbox{\hbox{$\displaystyle\displaystyle\Omega,\vec{u}:\mathcal{U}\rightsquigarrow\Omega_{1},\vec{u}:\mathcal{U}\boxplus\Omega_{2}$}}}}}}$
(OM:GenTypeSplit) $\displaystyle\displaystyle{\hbox{\hskip
59.35pt\vbox{\hbox{\hskip-59.34999pt\hbox{\hbox{$\displaystyle\displaystyle\Omega\rightsquigarrow\Omega_{1}\boxplus\Omega_{2}$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle\mathcal{U}\rightsquigarrow\mathcal{U}_{1}\boxplus\mathcal{U}_{2}$}}}}\vbox{}}}\over\hbox{\hskip
57.21288pt\vbox{\vbox{}\hbox{\hskip-57.21286pt\hbox{\hbox{$\displaystyle\displaystyle\Omega,\vec{u}:\mathcal{U}\rightsquigarrow\Omega_{1},\vec{u}:\mathcal{U}_{1}\boxplus\Omega_{2},\vec{u}:\mathcal{U}_{2}$}}}}}}$
Figure 31. Extended rules for VS typing and $\Omega$ context splitting with
generators.

Figure 31 gives the typing rules for generators and the $\Omega$ context
splitting rules for contexts containing generators, which are symmetric to
their VS variable counterparts in Figures 7 and 10 respectively. Generators
behave identically to VS variables throughout this section of the appendix,
with the exception that generators cannot be substituted for using the
substitution lemma given in this section.

We will now describe some technical properties of VS type splitting and
$\Omega$ context splitting. Lemma 1 gives the canonical forms of VS types and
$\Omega$-contexts that are involved in splitting judgements. Lemma 2 states if
$\mathcal{U}$ splits into $\mathcal{U}_{1}$ and $\mathcal{U}_{2}$, then all
subtypes of $\mathcal{U}$ also split into $\mathcal{U}_{1}$ and
$\mathcal{U}_{2}$ (i.e. $\mathcal{U}$ can be ”strengthened” in the splitting
judgement). Lemma 3 states that VS type splitting and $\Omega$ splitting are
associative. For example, if $\mathcal{U}$ splits into three disjoint types,
this is manifested by having $\mathcal{U}$ split into one of the three types
and an intermediate $\mathcal{U}^{\prime}$ that splits into the other two
types. The associative nature of splitting allows any one of the three types
to be split directly from $\mathcal{U}$ whie guaranteeing the existance of an
intermediate $\mathcal{U}^{\prime}$ that splits into the other two types.
Loosely speaking, the order in which disjoint VS types and $\Omega$s are split
from a single source is inconsequential.

###### Lemma 0.

  1. (1)

If $\mathcal{U}\rightsquigarrow\mathcal{U}_{1}\boxplus\mathcal{U}_{2}$ then
one of the following is true:

    1. (a)

$\mathcal{U}=\mathcal{U}_{3}^{\blacksquare}\times\mathcal{U}_{4}^{\blacksquare}$.

    2. (b)

$\mathcal{U}=\mathcal{U}_{3}^{\blacksquare}\times\mathcal{U}_{4}^{\square}$.

    3. (c)

$\mathcal{U}=\mathcal{U}_{3}^{\square}\times\mathcal{U}_{4}^{\blacksquare}$.

    4. (d)

$\mathcal{U}=\nu t.\mathcal{U}_{3}$.

  2. (2)

If
$\mathcal{U}_{1}^{\blacksquare}\times\mathcal{U}_{2}^{\square}\rightsquigarrow\mathcal{U}_{3}\boxplus\mathcal{U}_{4}$
then there exists a $\mathcal{U}_{1}^{\prime}$ and
$\mathcal{U}_{1}^{\prime\prime}$ such that
$\mathcal{U}_{1}\rightsquigarrow\mathcal{U}_{1}^{\prime}\boxplus\mathcal{U}_{1}^{\prime\prime}$
and
$\mathcal{U}_{1}^{\prime\blacksquare}\times\mathcal{U}_{2}^{\square}\sqsubseteq\mathcal{U}_{3}$
and
$\mathcal{U}_{1}^{\prime\prime\blacksquare}\times\mathcal{U}_{2}^{\square}\sqsubseteq\mathcal{U}_{4}$.

  3. (3)

If
$\mathcal{U}_{1}^{\square}\times\mathcal{U}_{2}^{\blacksquare}\rightsquigarrow\mathcal{U}_{3}\boxplus\mathcal{U}_{4}$
then there exists a $\mathcal{U}_{2}^{\prime}$ and
$\mathcal{U}_{2}^{\prime\prime}$ such that
$\mathcal{U}_{2}\rightsquigarrow\mathcal{U}_{2}^{\prime}\boxplus\mathcal{U}_{2}^{\prime\prime}$
and
$\mathcal{U}_{1}^{\square}\times\mathcal{U}_{2}^{\prime\blacksquare}\sqsubseteq\mathcal{U}_{3}$
and
$\mathcal{U}_{1}^{\square}\times\mathcal{U}_{2}^{\prime\prime\blacksquare}\sqsubseteq\mathcal{U}_{4}$.

  4. (4)

If
$\mathcal{U}_{1}^{\blacksquare}\times\mathcal{U}_{2}^{\blacksquare}\rightsquigarrow\mathcal{U}_{3}\boxplus\mathcal{U}_{4}$
then at least one of the following is true:

    1. (a)

$\mathcal{U}_{1}^{\blacksquare}\times\mathcal{U}_{2}^{\square}\sqsubseteq\mathcal{U}_{3}$
and
$\mathcal{U}_{1}^{\square}\times\mathcal{U}_{2}^{\blacksquare}\sqsubseteq\mathcal{U}_{4}$.

    2. (b)

$\mathcal{U}_{1}^{\square}\times\mathcal{U}_{2}^{\blacksquare}\sqsubseteq\mathcal{U}_{3}$
and
$\mathcal{U}_{1}^{\blacksquare}\times\mathcal{U}_{2}^{\square}\sqsubseteq\mathcal{U}_{4}$.

    3. (c)

There exists a $\mathcal{U}_{1}^{\prime}$ and $\mathcal{U}_{1}^{\prime\prime}$
such that
$\mathcal{U}_{1}\rightsquigarrow\mathcal{U}_{1}^{\prime}\boxplus\mathcal{U}_{1}^{\prime\prime}$
and
$\mathcal{U}_{1}^{\prime\blacksquare}\times\mathcal{U}_{2}^{\blacksquare}\sqsubseteq\mathcal{U}_{3}$
and
$\mathcal{U}_{1}^{\prime\prime\blacksquare}\times\mathcal{U}_{2}^{\square}\sqsubseteq\mathcal{U}_{4}$.

    4. (d)

There exists a $\mathcal{U}_{1}^{\prime}$ and $\mathcal{U}_{1}^{\prime\prime}$
such that
$\mathcal{U}_{1}\rightsquigarrow\mathcal{U}_{1}^{\prime}\boxplus\mathcal{U}_{1}^{\prime\prime}$
and
$\mathcal{U}_{1}^{\prime\blacksquare}\times\mathcal{U}_{2}^{\square}\sqsubseteq\mathcal{U}_{3}$
and
$\mathcal{U}_{1}^{\prime\prime\blacksquare}\times\mathcal{U}_{2}^{\blacksquare}\sqsubseteq\mathcal{U}_{4}$.

    5. (e)

There exists a $\mathcal{U}_{2}^{\prime}$ and $\mathcal{U}_{2}^{\prime\prime}$
such that
$\mathcal{U}_{2}\rightsquigarrow\mathcal{U}_{2}^{\prime}\boxplus\mathcal{U}_{2}^{\prime\prime}$
and
$\mathcal{U}_{1}^{\blacksquare}\times\mathcal{U}_{2}^{\prime\blacksquare}\sqsubseteq\mathcal{U}_{3}$
and
$\mathcal{U}_{1}^{\square}\times\mathcal{U}_{2}^{\prime\prime\blacksquare}\sqsubseteq\mathcal{U}_{4}$.

    6. (f)

There exists a $\mathcal{U}_{2}^{\prime}$ and $\mathcal{U}_{2}^{\prime\prime}$
such that
$\mathcal{U}_{2}\rightsquigarrow\mathcal{U}_{2}^{\prime}\boxplus\mathcal{U}_{2}^{\prime\prime}$
and
$\mathcal{U}_{1}^{\square}\times\mathcal{U}_{2}^{\prime\blacksquare}\sqsubseteq\mathcal{U}_{3}$
and
$\mathcal{U}_{1}^{\blacksquare}\times\mathcal{U}_{2}^{\prime\prime\blacksquare}\sqsubseteq\mathcal{U}_{4}$.

    7. (g)

There exists a $\mathcal{U}_{1}^{\prime}$ and $\mathcal{U}_{1}^{\prime\prime}$
and $\mathcal{U}_{2}^{\prime}$ and $\mathcal{U}_{2}^{\prime\prime}$ such that
$\mathcal{U}_{1}\rightsquigarrow\mathcal{U}_{1}^{\prime}\boxplus\mathcal{U}_{1}^{\prime\prime}$
and
$\mathcal{U}_{2}\rightsquigarrow\mathcal{U}_{2}^{\prime}\boxplus\mathcal{U}_{2}^{\prime\prime}$
and
$\mathcal{U}_{1}^{\prime\blacksquare}\times\mathcal{U}_{2}^{\prime\blacksquare}\sqsubseteq\mathcal{U}_{3}$
and
$\mathcal{U}_{1}^{\prime\prime\blacksquare}\times\mathcal{U}_{2}^{\prime\prime\blacksquare}\sqsubseteq\mathcal{U}_{4}$.

  5. (5)

If $\Omega,u:\mathcal{U}\rightsquigarrow\Omega_{1}\boxplus\Omega_{2}$, then
one of the following is true:

    1. (a)

$\Omega_{1}=\Omega_{1}^{\prime},u:\mathcal{U}$ and
$\Omega\rightsquigarrow\Omega_{1}^{\prime}\boxplus\Omega_{2}$ and
$u\notin\Omega_{2}$.

    2. (b)

$\Omega_{2}=\Omega_{2}^{\prime},u:\mathcal{U}$ and
$\Omega\rightsquigarrow\Omega_{1}\boxplus\Omega_{2}^{\prime}$ and
$u\notin\Omega_{1}$.

    3. (c)

$\mathcal{U}\rightsquigarrow\mathcal{U}_{1}\boxplus\mathcal{U}_{2}$ and
$\Omega_{1}=\Omega_{1}^{\prime},u:\mathcal{U}_{1}$ and
$\Omega_{2}=\Omega_{2}^{\prime},u:\mathcal{U}_{2}$ and
$\Omega\rightsquigarrow\Omega_{1}^{\prime}\boxplus\Omega_{2}^{\prime}$.

    4. (d)

$\mathcal{U}\rightsquigarrow\mathcal{U}_{1}\boxplus\mathcal{U}_{2}$ and
$\Omega_{1}=\Omega_{1}^{\prime},u:\mathcal{U}_{2}$ and
$\Omega_{2}=\Omega_{2}^{\prime},u:\mathcal{U}_{1}$ and
$\Omega\rightsquigarrow\Omega_{1}^{\prime}\boxplus\Omega_{2}^{\prime}$.

  6. (6)

If $\Omega,\vec{u}:\mathcal{U}\rightsquigarrow\Omega_{1}\boxplus\Omega_{2}$,
then one of the following is true:

    1. (a)

$\Omega_{1}=\Omega_{1}^{\prime},\vec{u}:\mathcal{U}$ and
$\Omega\rightsquigarrow\Omega_{1}^{\prime}\boxplus\Omega_{2}$ and
$\vec{u}\notin\Omega_{2}$.

    2. (b)

$\Omega_{2}=\Omega_{2}^{\prime},\vec{u}:\mathcal{U}$ and
$\Omega\rightsquigarrow\Omega_{1}\boxplus\Omega_{2}^{\prime}$ and
$\vec{u}\notin\Omega_{1}$.

    3. (c)

$\mathcal{U}\rightsquigarrow\mathcal{U}_{1}\boxplus\mathcal{U}_{2}$ and
$\Omega_{1}=\Omega_{1}^{\prime},\vec{u}:\mathcal{U}_{1}$ and
$\Omega_{2}=\Omega_{2}^{\prime},\vec{u}:\mathcal{U}_{2}$ and
$\Omega\rightsquigarrow\Omega_{1}^{\prime}\boxplus\Omega_{2}^{\prime}$.

    4. (d)

$\mathcal{U}\rightsquigarrow\mathcal{U}_{1}\boxplus\mathcal{U}_{2}$ and
$\Omega_{1}=\Omega_{1}^{\prime},\vec{u}:\mathcal{U}_{2}$ and
$\Omega_{2}=\Omega_{2}^{\prime},\vec{u}:\mathcal{U}_{1}$ and
$\Omega\rightsquigarrow\Omega_{1}^{\prime}\boxplus\Omega_{2}^{\prime}$.

###### Proof.

  1. (1)

By induction on the derivation of
$\mathcal{U}\rightsquigarrow\mathcal{U}_{3}\boxplus\mathcal{U}_{4}$.

     * •

US:Prod. By inversion on the rule.

     * •

US:SplitBoth. By inversion on the rule.

     * •

US:SplitLeft. By inversion on the rule.

     * •

US:SplitRight. By inversion on the rule.

     * •

US:Corecursive. By inversion on the rule.

     * •

US:Subtype By induction.

     * •

US:Commutative. By induction.

  2. (2)

By induction on the derivation of
$\mathcal{U}_{1}^{\blacksquare}\times\mathcal{U}_{2}^{\square}\rightsquigarrow\mathcal{U}_{3}\boxplus\mathcal{U}_{4}$.

     * •

US:SplitLeft. By inversion on the rule.

     * •

US:Subtype. Then
$\mathcal{U}_{1}^{\blacksquare}\times\mathcal{U}_{2}^{\square}\rightsquigarrow\mathcal{U}_{3}^{\prime}\boxplus\mathcal{U}_{4}$
and $\mathcal{U}_{3}^{\prime}\sqsubseteq\mathcal{U}_{3}$. By induction, there
exists $\mathcal{U}_{1}^{\prime}$ and $\mathcal{U}_{1}^{\prime\prime}$ such
that
$\mathcal{U}_{1}\rightsquigarrow\mathcal{U}_{1}^{\prime}\boxplus\mathcal{U}_{1}^{\prime\prime}$
and
$\mathcal{U}_{1}^{\prime\blacksquare}\times\mathcal{U}_{2}^{\square}\sqsubseteq\mathcal{U}_{3}^{\prime}$
and
$\mathcal{U}_{1}^{\prime\prime\blacksquare}\times\mathcal{U}_{2}^{\square}\sqsubseteq\mathcal{U}_{4}$.
Apply UT:Transitive.

     * •

US:Commutative. Then
$\mathcal{U}_{1}^{\blacksquare}\times\mathcal{U}_{2}^{\square}\rightsquigarrow\mathcal{U}_{4}\boxplus\mathcal{U}_{3}$.
By induction, there exists $\mathcal{U}_{1}^{\prime\prime}$ and
$\mathcal{U}_{1}^{\prime}$ such that
$\mathcal{U}_{1}\rightsquigarrow\mathcal{U}_{1}^{\prime\prime}\boxplus\mathcal{U}_{1}^{\prime}$
and
$\mathcal{U}_{1}^{\prime\prime\blacksquare}\times\mathcal{U}_{2}^{\square}\sqsubseteq\mathcal{U}_{4}$
and
$\mathcal{U}_{1}^{\prime\blacksquare}\times\mathcal{U}_{2}^{\square}\sqsubseteq\mathcal{U}_{3}$.
Apply US:Commutative.

  3. (3)

By symmetry with part 2.

  4. (4)

By induction on the derivation of
$\mathcal{U}_{1}^{\blacksquare}\times\mathcal{U}_{2}^{\blacksquare}\rightsquigarrow\mathcal{U}_{3}\boxplus\mathcal{U}_{4}$

     * •

US:Prod. By inversion on the rule.

     * •

US:SplitBoth. By inversion on the rule.

     * •

US:SplitLeft. By inversion on the rule.

     * •

US:SplitRight. By inversion on the rule.

     * •

US:Subtype. Then
$\mathcal{U}_{1}^{\blacksquare}\times\mathcal{U}_{2}^{\blacksquare}\rightsquigarrow\mathcal{U}_{3}^{\prime}\boxplus\mathcal{U}_{4}$
and $\mathcal{U}_{3}^{\prime}\sqsubseteq\mathcal{U}_{3}$. By induction and an
application of UT:Transitive.

     * •

US:Commutative. Then
$\mathcal{U}_{1}^{\blacksquare}\times\mathcal{U}_{2}^{\square}\rightsquigarrow\mathcal{U}_{4}\boxplus\mathcal{U}_{3}$.
By induction, there are seven cases:

       1. (a)

$\mathcal{U}_{1}^{\blacksquare}\times\mathcal{U}_{2}^{\square}\sqsubseteq\mathcal{U}_{4}$
and
$\mathcal{U}_{1}^{\square}\times\mathcal{U}_{2}^{\blacksquare}\sqsubseteq\mathcal{U}_{3}$.

       2. (b)

$\mathcal{U}_{1}^{\square}\times\mathcal{U}_{2}^{\blacksquare}\sqsubseteq\mathcal{U}_{4}$
and
$\mathcal{U}_{1}^{\blacksquare}\times\mathcal{U}_{2}^{\square}\sqsubseteq\mathcal{U}_{3}$.

       3. (c)

There exists $\mathcal{U}_{1}^{\prime\prime}$ and $\mathcal{U}_{1}^{\prime}$
such that
$\mathcal{U}_{1}\rightsquigarrow\mathcal{U}_{1}^{\prime\prime}\boxplus\mathcal{U}_{1}^{\prime}$
and
$\mathcal{U}_{1}^{\prime\prime\blacksquare}\times\mathcal{U}_{2}^{\blacksquare}\sqsubseteq\mathcal{U}_{4}$
and
$\mathcal{U}_{1}^{\prime\blacksquare}\times\mathcal{U}_{2}^{\square}\sqsubseteq\mathcal{U}_{3}$.
Apply US:Commutative.

       4. (d)

There exists $\mathcal{U}_{1}^{\prime\prime}$ and $\mathcal{U}_{1}^{\prime}$
such that
$\mathcal{U}_{1}\rightsquigarrow\mathcal{U}_{1}^{\prime\prime}\boxplus\mathcal{U}_{1}^{\prime}$
and
$\mathcal{U}_{1}^{\prime\prime\blacksquare}\times\mathcal{U}_{2}^{\square}\sqsubseteq\mathcal{U}_{4}$
and
$\mathcal{U}_{1}^{\prime\blacksquare}\times\mathcal{U}_{2}^{\blacksquare}\sqsubseteq\mathcal{U}_{3}$.
Apply US:Commutative.

       5. (e)

There exists $\mathcal{U}_{2}^{\prime\prime}$ and $\mathcal{U}_{2}^{\prime}$
such that
$\mathcal{U}_{2}\rightsquigarrow\mathcal{U}_{2}^{\prime\prime}\boxplus\mathcal{U}_{2}^{\prime}$
and
$\mathcal{U}_{1}^{\blacksquare}\times\mathcal{U}_{2}^{\prime\prime\blacksquare}\sqsubseteq\mathcal{U}_{4}$
and
$\mathcal{U}_{1}^{\square}\times\mathcal{U}_{2}^{\prime\blacksquare}\sqsubseteq\mathcal{U}_{3}$.
Apply US:Commutative.

       6. (f)

There exists $\mathcal{U}_{2}^{\prime\prime}$ and $\mathcal{U}_{2}^{\prime}$
such that
$\mathcal{U}_{2}\rightsquigarrow\mathcal{U}_{2}^{\prime\prime}\boxplus\mathcal{U}_{2}^{\prime}$
and
$\mathcal{U}_{1}^{\square}\times\mathcal{U}_{2}^{\prime\prime\blacksquare}\sqsubseteq\mathcal{U}_{4}$
and
$\mathcal{U}_{1}^{\blacksquare}\times\mathcal{U}_{2}^{\prime\blacksquare}\sqsubseteq\mathcal{U}_{3}$.
Apply US:Commutative.

       7. (g)

There exists $\mathcal{U}_{1}^{\prime\prime}$ and $\mathcal{U}_{1}^{\prime}$
and $\mathcal{U}_{2}^{\prime\prime}$ and $\mathcal{U}_{2}^{\prime}$ such that
$\mathcal{U}_{1}\rightsquigarrow\mathcal{U}_{1}^{\prime\prime}\boxplus\mathcal{U}_{1}^{\prime}$
and
$\mathcal{U}_{2}\rightsquigarrow\mathcal{U}_{2}^{\prime\prime}\boxplus\mathcal{U}_{2}^{\prime}$
and
$\mathcal{U}_{1}^{\prime\prime\blacksquare}\times\mathcal{U}_{2}^{\prime\prime\blacksquare}\sqsubseteq\mathcal{U}_{4}$
and
$\mathcal{U}_{1}^{\prime\blacksquare}\times\mathcal{U}_{2}^{\prime\blacksquare}\sqsubseteq\mathcal{U}_{3}$.
Apply US:Commutative twice.

  5. (5)

By induction on the derivation of
$\Omega,u:\mathcal{U}\rightsquigarrow\Omega_{1}\boxplus\Omega_{2}$.

     * •

OM:Var. By inversion on the rule. Since $\Omega,u:\mathcal{U}$ can contain
only a single binding for $u$, $u\notin\Omega$, so $u\notin\Omega_{2}$.

     * •

OM:VarTypeSplit. By inversion on the rule.

     * •

OM:Commutative. By induction, there are four cases:

       1. (a)

$\Omega_{2}=\Omega_{2}^{\prime},u:\mathcal{U}$ and
$\Omega\rightsquigarrow\Omega_{2}^{\prime}\boxplus\Omega_{1}$ and
$u\notin\Omega_{1}$. Apply OM:Commutative.

       2. (b)

$\Omega_{1}=\Omega_{1}^{\prime},u:\mathcal{U}$ and
$\Omega\rightsquigarrow\Omega_{2}\boxplus\Omega_{1}^{\prime}$ and
$u\notin\Omega_{2}$. Apply OM:Commutative.

       3. (c)

$\mathcal{U}\rightsquigarrow\mathcal{U}_{1}\boxplus\mathcal{U}_{2}$ and
$\Omega_{2}=\Omega_{2}^{\prime},u:\mathcal{U}_{1}$ and
$\Omega_{1}=\Omega_{1}^{\prime},u:\mathcal{U}_{2}$ and
$\Omega\rightsquigarrow\Omega_{2}^{\prime}\boxplus\Omega_{1}^{\prime}$. Apply
OM:Commutative and US:Commutative.

       4. (d)

$\mathcal{U}\rightsquigarrow\mathcal{U}_{1}\boxplus\mathcal{U}_{2}$ and
$\Omega_{2}=\Omega_{2}^{\prime},u:\mathcal{U}_{2}$ and
$\Omega_{1}=\Omega_{1}^{\prime},u:\mathcal{U}_{1}$ and
$\Omega\rightsquigarrow\Omega_{2}^{\prime}\boxplus\Omega_{1}^{\prime}$. Apply
OM:Commutative.

  6. (6)

By symmetry with part 5.

∎

###### Lemma 0.

  1. (1)

If $\nu t.\mathcal{U}\rightsquigarrow\mathcal{U}_{1}\boxplus\mathcal{U}_{2}$
then $\mathcal{U}[\nu
t.\mathcal{U}/t]\rightsquigarrow\mathcal{U}_{1}^{\prime}\boxplus\mathcal{U}_{2}^{\prime}$.

  2. (2)

If $\mathcal{U}\sqsubseteq\mathcal{U}^{\prime}$ and
$\mathcal{U}^{\prime}\rightsquigarrow\mathcal{U}_{1}\boxplus\mathcal{U}_{2}$
then $\mathcal{U}\rightsquigarrow\mathcal{U}_{1}\boxplus\mathcal{U}_{2}$.

###### Proof.

  1. (1)

By induction on the derivation of $\nu
t.\mathcal{U}\rightsquigarrow\mathcal{U}_{1}\boxplus\mathcal{U}_{2}$.

     * •

US:Corecursive. By inversion on the rule.

     * •

US:Subtype. Then $\nu
t.\mathcal{U}\rightsquigarrow\mathcal{U}_{1}^{\prime}\boxplus\mathcal{U}_{2}$
and $\mathcal{U}_{1}^{\prime}\sqsubseteq\mathcal{U}_{1}$. By induction,
$\mathcal{U}[\nu
t.\mathcal{U}/t]\rightsquigarrow\mathcal{U}_{1}^{\prime}\boxplus\mathcal{U}_{2}$.
Apply US:Subtype.

     * •

US:Commutative. Then $\nu
t.\mathcal{U}\rightsquigarrow\mathcal{U}_{2}\boxplus\mathcal{U}_{1}$. By
induction, $\mathcal{U}[\nu
t.\mathcal{U}/t]\rightsquigarrow\mathcal{U}_{2}\boxplus\mathcal{U}_{1}$. Apply
US:Commutative.

  2. (2)

By induction on the derivation of
$\mathcal{U}\sqsubseteq\mathcal{U}^{\prime}$.

     * •

UT:ProdLeft. Then
$\mathcal{U}=\mathcal{U}_{3}^{a_{1}}\times\mathcal{U}_{4}^{a_{2}}$ and
$\mathcal{U}^{\prime}=\mathcal{U}_{5}^{\square}\times\mathcal{U}_{4}^{a_{2}}$.
By Lemma 1, $a_{2}=\blacksquare$. By Lemma 1, there exists
$\mathcal{U}_{4}^{\prime}$ and $\mathcal{U}_{4}^{\prime\prime}$ such that
$\mathcal{U}_{4}\rightsquigarrow\mathcal{U}_{4}^{\prime}\boxplus\mathcal{U}_{4}^{\prime\prime}$
and
$\mathcal{U}_{5}^{\square}\times\mathcal{U}_{4}^{\prime\blacksquare}\sqsubseteq\mathcal{U}_{1}$
and
$\mathcal{U}_{5}^{\square}\times\mathcal{U}_{4}^{\prime\prime\blacksquare}\sqsubseteq\mathcal{U}_{2}$.
By US:SplitRight,
$\mathcal{U}\rightsquigarrow\mathcal{U}_{3}^{a_{1}}\times\mathcal{U}_{4}^{\prime\blacksquare}\boxplus\mathcal{U}_{3}^{\square}\times\mathcal{U}_{4}^{\prime\prime\blacksquare}$.
By UT:PairLeft,
$\mathcal{U}_{3}^{a_{1}}\times\mathcal{U}_{4}^{\prime\blacksquare}\sqsubseteq\mathcal{U}_{5}^{\square}\times\mathcal{U}_{4}^{\prime\blacksquare}$.
By UT:PairLeft,
$\mathcal{U}_{3}^{\square}\times\mathcal{U}_{4}^{\prime\prime\blacksquare}\sqsubseteq\mathcal{U}_{5}^{\square}\times\mathcal{U}_{4}^{\prime\prime\blacksquare}$.
Apply US:Subtype four times.

     * •

UT:ProdLeft. By symmetry with the previous case.

     * •

UT:Prod. Then
$\mathcal{U}=\mathcal{U}_{3}^{a_{1}}\times\mathcal{U}_{4}^{a_{2}}$ and
$\mathcal{U}^{\prime}=\mathcal{U}_{3}^{\prime
a_{1}}\times\mathcal{U}_{4}^{\prime a_{2}}$ and
$\mathcal{U}_{3}\sqsubseteq\mathcal{U}_{3}^{\prime}$ and
$\mathcal{U}_{4}\sqsubseteq\mathcal{U}_{4}^{\prime}$. By Lemma 1, there are
three cases:

       1. (a)

$a_{1}=\blacksquare$ and $a_{2}=\square$. By Lemma 1, there exists
$\mathcal{U}_{3}^{\prime\prime}$ and $\mathcal{U}_{3}^{\prime\prime\prime}$
such that
$\mathcal{U}_{3}^{\prime}\rightsquigarrow\mathcal{U}_{3}^{\prime\prime}\boxplus\mathcal{U}_{3}^{\prime\prime\prime}$
and
$\mathcal{U}_{3}^{\prime\prime\blacksquare}\times\mathcal{U}_{4}^{\prime\square}\sqsubseteq\mathcal{U}_{1}$
and
$\mathcal{U}_{3}^{\prime\prime\prime\blacksquare}\times\mathcal{U}_{4}^{\prime\square}\sqsubseteq\mathcal{U}_{2}$.
By induction,
$\mathcal{U}_{3}\rightsquigarrow\mathcal{U}_{3}^{\prime\prime}\boxplus\mathcal{U}_{3}^{\prime\prime\prime}$.
By US:SplitLeft,
$\mathcal{U}\rightsquigarrow\mathcal{U}_{3}^{\prime\prime\blacksquare}\times\mathcal{U}_{4}^{\square}\boxplus\mathcal{U}_{3}^{\prime\prime\prime\blacksquare}\times\mathcal{U}_{4}^{\square}$.
By UT:Pair,
$\mathcal{U}_{3}^{\prime\prime\blacksquare}\times\mathcal{U}_{4}^{\square}\sqsubseteq\mathcal{U}_{3}^{\prime\prime\blacksquare}\times\mathcal{U}_{4}^{\prime\square}$.
By UT:Pair,
$\mathcal{U}_{3}^{\prime\prime\prime\blacksquare}\times\mathcal{U}_{4}^{\square}\sqsubseteq\mathcal{U}_{3}^{\prime\prime\prime\blacksquare}\times\mathcal{U}_{4}^{\prime\square}$.
Apply US:Subtype four times.

       2. (b)

$a_{1}=\square$ and $a_{2}=\blacksquare$. By symmetry with the previous case.

       3. (c)

$a_{1}=a_{2}=\blacksquare$. By Lemma 1, there are seven cases:

         1. (i)

$\mathcal{U}_{3}^{\prime\blacksquare}\times\mathcal{U}_{4}^{\prime\square}\sqsubseteq\mathcal{U}_{1}$
and
$\mathcal{U}_{3}^{\prime\square}\times\mathcal{U}_{4}^{\prime\blacksquare}\sqsubseteq\mathcal{U}_{2}$.
By US:Prod,
$\mathcal{U}\rightsquigarrow\mathcal{U}_{3}^{\blacksquare}\times\mathcal{U}_{4}^{\square}\boxplus\mathcal{U}_{3}^{\square}\times\mathcal{U}_{4}^{\blacksquare}$.
By UT:Prod,
$\mathcal{U}_{3}^{\blacksquare}\times\mathcal{U}_{4}^{\square}\sqsubseteq\mathcal{U}_{3}^{\prime\blacksquare}\times\mathcal{U}_{4}^{\prime\square}$.
By UT:Prod,
$\mathcal{U}_{3}^{\square}\times\mathcal{U}_{4}^{\blacksquare}\sqsubseteq\mathcal{U}_{3}^{\prime\square}\times\mathcal{U}_{4}^{\prime\blacksquare}$.
Apply US:Subtype twice.

         2. (ii)

$\mathcal{U}_{3}^{\prime\square}\times\mathcal{U}_{4}^{\prime\blacksquare}\sqsubseteq\mathcal{U}_{1}$
and
$\mathcal{U}_{3}^{\prime\blacksquare}\times\mathcal{U}_{4}^{\prime\square}\sqsubseteq\mathcal{U}_{2}$.
By symmetry with the previous case.

         3. (iii)

There exists $\mathcal{U}_{3}^{\prime\prime}$ and
$\mathcal{U}_{3}^{\prime\prime\prime}$ such that
$\mathcal{U}_{3}^{\prime}\rightsquigarrow\mathcal{U}_{3}^{\prime\prime}\boxplus\mathcal{U}_{3}^{\prime\prime\prime}$
and
$\mathcal{U}_{3}^{\prime\prime\blacksquare}\times\mathcal{U}_{4}^{\prime\blacksquare}\sqsubseteq\mathcal{U}_{1}$
and
$\mathcal{U}_{3}^{\prime\prime\prime\blacksquare}\times\mathcal{U}_{4}^{\prime\square}\sqsubseteq\mathcal{U}_{2}$.
By induction,
$\mathcal{U}_{3}\rightsquigarrow\mathcal{U}_{3}^{\prime\prime}\boxplus\mathcal{U}_{3}^{\prime\prime\prime}$.
By US:SplitLeft,
$\mathcal{U}\rightsquigarrow\mathcal{U}_{3}^{\prime\prime\blacksquare}\times\mathcal{U}_{4}^{\blacksquare}\boxplus\mathcal{U}_{3}^{\prime\prime\prime\blacksquare}\times\mathcal{U}_{4}^{\square}$.
By UT:Pair,
$\mathcal{U}_{3}^{\prime\prime\blacksquare}\times\mathcal{U}_{4}^{\blacksquare}\sqsubseteq\mathcal{U}_{3}^{\prime\prime\blacksquare}\times\mathcal{U}_{4}^{\prime\blacksquare}$.
By UT:Pair,
$\mathcal{U}_{3}^{\prime\prime\prime\blacksquare}\times\mathcal{U}_{4}^{\square}\sqsubseteq\mathcal{U}_{3}^{\prime\prime\prime\blacksquare}\times\mathcal{U}_{4}^{\prime\square}$.
Apply US:Subtype four times.

         4. (iv)

There exists $\mathcal{U}_{3}^{\prime\prime}$ and
$\mathcal{U}_{3}^{\prime\prime\prime}$ such that
$\mathcal{U}_{3}^{\prime}\rightsquigarrow\mathcal{U}_{3}^{\prime\prime}\boxplus\mathcal{U}_{3}^{\prime\prime\prime}$
and
$\mathcal{U}_{3}^{\prime\prime\blacksquare}\times\mathcal{U}_{4}^{\prime\square}\sqsubseteq\mathcal{U}_{1}$
and
$\mathcal{U}_{3}^{\prime\prime\prime\blacksquare}\times\mathcal{U}_{4}^{\prime\blacksquare}\sqsubseteq\mathcal{U}_{2}$.
By symmetry with the previous case.

         5. (v)

There exists $\mathcal{U}_{4}^{\prime\prime}$ and
$\mathcal{U}_{4}^{\prime\prime\prime}$ such that
$\mathcal{U}_{4}^{\prime}\rightsquigarrow\mathcal{U}_{4}^{\prime\prime}\boxplus\mathcal{U}_{4}^{\prime\prime\prime}$
and
$\mathcal{U}_{3}^{\prime\blacksquare}\times\mathcal{U}_{4}^{\prime\prime\blacksquare}\sqsubseteq\mathcal{U}_{1}$
and
$\mathcal{U}_{3}^{\prime\square}\times\mathcal{U}_{4}^{\prime\prime\prime\blacksquare}\sqsubseteq\mathcal{U}_{2}$.
By symmetry with the previous case.

         6. (vi)

There exists $\mathcal{U}_{4}^{\prime\prime}$ and
$\mathcal{U}_{4}^{\prime\prime\prime}$ such that
$\mathcal{U}_{4}^{\prime}\rightsquigarrow\mathcal{U}_{4}^{\prime\prime}\boxplus\mathcal{U}_{4}^{\prime\prime\prime}$
and
$\mathcal{U}_{3}^{\prime\square}\times\mathcal{U}_{4}^{\prime\prime\blacksquare}\sqsubseteq\mathcal{U}_{1}$
and
$\mathcal{U}_{3}^{\prime\blacksquare}\times\mathcal{U}_{4}^{\prime\prime\prime\blacksquare}\sqsubseteq\mathcal{U}_{2}$.
By symmetry with the previous case.

         7. (vii)

There exists $\mathcal{U}_{3}^{\prime\prime}$ and
$\mathcal{U}_{3}^{\prime\prime\prime}$ and $\mathcal{U}_{4}^{\prime\prime}$
and $\mathcal{U}_{4}^{\prime\prime\prime}$ such that
$\mathcal{U}_{3}^{\prime}\rightsquigarrow\mathcal{U}_{3}^{\prime\prime}\boxplus\mathcal{U}_{3}^{\prime\prime\prime}$
and
$\mathcal{U}_{4}^{\prime}\rightsquigarrow\mathcal{U}_{4}^{\prime\prime}\boxplus\mathcal{U}_{4}^{\prime\prime\prime}$
and
$\mathcal{U}_{3}^{\prime\prime\blacksquare}\times\mathcal{U}_{4}^{\prime\prime\blacksquare}\sqsubseteq\mathcal{U}_{1}$
and
$\mathcal{U}_{3}^{\prime\prime\prime\blacksquare}\times\mathcal{U}_{4}^{\prime\prime\prime\blacksquare}\sqsubseteq\mathcal{U}_{2}$.
By induction,
$\mathcal{U}_{3}\rightsquigarrow\mathcal{U}_{3}^{\prime\prime}\boxplus\mathcal{U}_{3}^{\prime\prime\prime}$
and
$\mathcal{U}_{4}\rightsquigarrow\mathcal{U}_{4}^{\prime\prime}\boxplus\mathcal{U}_{4}^{\prime\prime\prime}$.
By US:SplitBoth,
$\mathcal{U}\rightsquigarrow\mathcal{U}_{3}^{\prime\prime\blacksquare}\times\mathcal{U}_{4}^{\prime\prime\blacksquare}\boxplus\mathcal{U}_{3}^{\prime\prime\prime\blacksquare}\times\mathcal{U}_{4}^{\prime\prime\prime\blacksquare}$.
Apply US:Subtype twice.

     * •

UT:Corec1. Then $\mathcal{U}=\nu t.\mathcal{U}^{\prime\prime}$ and
$\mathcal{U}^{\prime}=\mathcal{U}^{\prime\prime}[\nu
t.\mathcal{U}^{\prime\prime}/t]$. Apply US:Recursive.

     * •

UT:Corec2. Then $\mathcal{U}=\mathcal{U}^{\prime\prime}[\nu
t.\mathcal{U}^{\prime\prime}/t]$ and $\mathcal{U}^{\prime}=\nu
t.\mathcal{U}^{\prime\prime}$. By part 1.

     * •

UT:Transitive. Then $\mathcal{U}\sqsubseteq\mathcal{U}^{\prime\prime}$ and
$\mathcal{U}^{\prime\prime}\sqsubseteq\mathcal{U}^{\prime}$. By induction,
$\mathcal{U}^{\prime\prime}\rightsquigarrow\mathcal{U}_{1}\boxplus\mathcal{U}_{2}$.
By induction.

∎

###### Lemma 0.

  1. (1)

If $\mathcal{U}\rightsquigarrow\mathcal{U}_{1}\boxplus\mathcal{U}_{2}$ then:

    1. (a)

If
$\mathcal{U}_{1}\rightsquigarrow\mathcal{U}_{1}^{\prime}\boxplus\mathcal{U}_{1}^{\prime\prime}$
then there exists a $\mathcal{U}^{\prime}$ such that
$\mathcal{U}\rightsquigarrow\mathcal{U}^{\prime}\boxplus\mathcal{U}_{1}^{\prime\prime}$
and
$\mathcal{U}^{\prime}\rightsquigarrow\mathcal{U}_{1}^{\prime}\boxplus\mathcal{U}_{2}$.

    2. (b)

If
$\mathcal{U}_{2}\rightsquigarrow\mathcal{U}_{2}^{\prime}\boxplus\mathcal{U}_{2}^{\prime\prime}$
then there exists a $\mathcal{U}^{\prime}$ such that
$\mathcal{U}\rightsquigarrow\mathcal{U}^{\prime}\boxplus\mathcal{U}_{2}^{\prime\prime}$
and
$\mathcal{U}^{\prime}\rightsquigarrow\mathcal{U}_{2}^{\prime}\boxplus\mathcal{U}_{1}$.

  2. (2)

If $\Omega\rightsquigarrow\Omega_{1}\boxplus\Omega_{2}$ then:

    1. (a)

If
$\Omega_{1}\rightsquigarrow\Omega_{1}^{\prime}\boxplus\Omega_{1}^{\prime\prime}$
then there exists an $\Omega^{\prime}$ such that
$\Omega\rightsquigarrow\Omega^{\prime}\boxplus\Omega_{1}^{\prime\prime}$ and
$\Omega^{\prime}\rightsquigarrow\Omega_{1}^{\prime}\boxplus\Omega_{2}$.

    2. (b)

If
$\Omega_{2}\rightsquigarrow\Omega_{2}^{\prime}\boxplus\Omega_{2}^{\prime\prime}$
then there exists an $\Omega^{\prime}$ such that
$\Omega\rightsquigarrow\Omega^{\prime}\boxplus\Omega_{2}^{\prime\prime}$ and
$\Omega^{\prime}\rightsquigarrow\Omega_{2}^{\prime}\boxplus\Omega_{1}$.

  3. (3)

If $\Omega\rightsquigarrow\Omega_{1}\boxplus\Omega_{2}$ and
$\Omega_{1}\rightsquigarrow\Omega_{1}^{\prime}\boxplus\Omega_{1}^{\prime\prime}$
and
$\Omega_{2}\rightsquigarrow\Omega_{2}^{\prime}\boxplus\Omega_{2}^{\prime\prime}$
then there exists an $\Omega^{\prime}$ and $\Omega^{\prime\prime}$ such that
$\Omega\rightsquigarrow\Omega^{\prime}\boxplus\Omega^{\prime\prime}$ and
$\Omega^{\prime}\rightsquigarrow\Omega_{1}^{\prime}\boxplus\Omega_{2}^{\prime}$
and
$\Omega^{\prime\prime}\rightsquigarrow\Omega_{1}^{\prime\prime}\boxplus\Omega_{2}^{\prime\prime}$.

###### Proof.

  1. (1)

By induction on the derivation of
$\mathcal{U}\rightsquigarrow\mathcal{U}_{1}\boxplus\mathcal{U}_{2}$.

     * •

US:Prod. Then
$\mathcal{U}=\mathcal{U}_{3}^{\blacksquare}\times\mathcal{U}_{4}^{\blacksquare}$
and
$\mathcal{U}_{1}=\mathcal{U}_{3}^{\blacksquare}\times\mathcal{U}_{4}^{\square}$
and
$\mathcal{U}_{2}=\mathcal{U}_{3}^{\square}\times\mathcal{U}_{4}^{\blacksquare}$.

       1. (a)

If
$\mathcal{U}_{1}\rightsquigarrow\mathcal{U}_{1}^{\prime}\boxplus\mathcal{U}_{1}^{\prime\prime}$,
by Lemma 1, there exists $\mathcal{U}_{3}^{\prime}$ and
$\mathcal{U}_{3}^{\prime\prime}$ such that
$\mathcal{U}_{3}\rightsquigarrow\mathcal{U}_{3}^{\prime}\boxplus\mathcal{U}_{3}^{\prime\prime}$
and
$\mathcal{U}_{3}^{\prime\blacksquare}\times\mathcal{U}_{4}^{\square}\sqsubseteq\mathcal{U}_{1}^{\prime}$
and
$\mathcal{U}_{3}^{\prime\prime\blacksquare}\times\mathcal{U}_{4}^{\square}\sqsubseteq\mathcal{U}_{1}^{\prime\prime}$.
By US:SplitLeft,
$\mathcal{U}\rightsquigarrow\mathcal{U}_{3}^{\prime\blacksquare}\times\mathcal{U}_{4}^{\blacksquare}\boxplus\mathcal{U}_{3}^{\prime\prime\blacksquare}\times\mathcal{U}_{4}^{\square}$.
By US:Subtype,
$\mathcal{U}\rightsquigarrow\mathcal{U}_{3}^{\prime\blacksquare}\times\mathcal{U}_{4}^{\blacksquare}\boxplus\mathcal{U}_{1}^{\prime\prime}$.
By US:Prod,
$\mathcal{U}_{3}^{\prime\blacksquare}\times\mathcal{U}_{4}^{\blacksquare}\rightsquigarrow\mathcal{U}_{3}^{\prime\blacksquare}\times\mathcal{U}_{4}^{\square}\boxplus\mathcal{U}_{3}^{\prime\square}\times\mathcal{U}_{4}^{\blacksquare}$.
By UT:ProdLeft,
$\mathcal{U}_{3}^{\prime\square}\times\mathcal{U}_{4}^{\blacksquare}\sqsubseteq\mathcal{U}_{3}^{\square}\times\mathcal{U}_{4}^{\blacksquare}$.
Apply US:Subtype twice.

       2. (b)

If
$\mathcal{U}_{2}\rightsquigarrow\mathcal{U}_{2}^{\prime}\boxplus\mathcal{U}_{2}^{\prime\prime}$,
by symmetry with the previous case.

     * •

US:SplitLeft. Then
$\mathcal{U}=\mathcal{U}_{3}^{\blacksquare}\times\mathcal{U}_{4}^{a}$ and
$\mathcal{U}_{3}\rightsquigarrow\mathcal{U}_{3}^{\prime}\boxplus\mathcal{U}_{3}^{\prime\prime}$
and
$\mathcal{U}_{1}=\mathcal{U}_{3}^{\prime\blacksquare}\times\mathcal{U}_{4}^{a}$
and
$\mathcal{U}_{2}=\mathcal{U}_{3}^{\prime\prime\blacksquare}\times\mathcal{U}_{4}^{\square}$.

       1. (a)

If
$\mathcal{U}_{1}\rightsquigarrow\mathcal{U}_{1}^{\prime}\boxplus\mathcal{U}_{1}^{\prime\prime}$,
there are two cases:

         1. (i)

$a=\square$. By Lemma 1, there exists $\mathcal{U}_{3}^{\prime\prime\prime}$
and $\mathcal{U}_{3}^{\prime\prime\prime\prime}$ such that
$\mathcal{U}_{3}^{\prime}\rightsquigarrow\mathcal{U}_{3}^{\prime\prime\prime}\boxplus\mathcal{U}_{3}^{\prime\prime\prime\prime}$
and
$\mathcal{U}_{3}^{\prime\prime\prime\blacksquare}\times\mathcal{U}_{4}^{\square}\sqsubseteq\mathcal{U}_{1}^{\prime}$
and
$\mathcal{U}_{3}^{\prime\prime\prime\prime\blacksquare}\times\mathcal{U}_{4}^{\square}\sqsubseteq\mathcal{U}_{1}^{\prime\prime}$.
By induction, there exists $\mathcal{U}^{\prime\prime}$ such that
$\mathcal{U}_{3}\rightsquigarrow\mathcal{U}^{\prime\prime}\boxplus\mathcal{U}_{3}^{\prime\prime\prime\prime}$
and
$\mathcal{U}^{\prime\prime}\rightsquigarrow\mathcal{U}_{3}^{\prime\prime\prime}\boxplus\mathcal{U}_{3}^{\prime\prime}$.
By US:SplitLeft,
$\mathcal{U}\rightsquigarrow\mathcal{U}^{\prime\prime\blacksquare}\times\mathcal{U}_{4}^{\square}\boxplus\mathcal{U}_{3}^{\prime\prime\prime\prime\blacksquare}\times\mathcal{U}_{4}^{\square}$.
By US:Subtype,
$\mathcal{U}\rightsquigarrow\mathcal{U}^{\prime\prime\blacksquare}\times\mathcal{U}_{4}^{\square}\boxplus\mathcal{U}_{1}^{\prime\prime}$.
By US:SplitLeft,
$\mathcal{U}^{\prime\prime\blacksquare}\times\mathcal{U}_{4}^{\square}\rightsquigarrow\mathcal{U}_{3}^{\prime\prime\prime\blacksquare}\times\mathcal{U}_{4}^{\square}\boxplus\mathcal{U}_{2}$.
Apply US:Subtype.

         2. (ii)

$a=\blacksquare$. By Lemma 1, there are seven cases:

           1. (A)

$\mathcal{U}_{3}^{\prime\blacksquare}\times\mathcal{U}_{4}^{\square}\sqsubseteq\mathcal{U}_{1}^{\prime}$
and
$\mathcal{U}_{3}^{\prime\square}\times\mathcal{U}_{4}^{\blacksquare}\sqsubseteq\mathcal{U}_{1}^{\prime\prime}$.
By US:Prod,
$\mathcal{U}\rightsquigarrow\mathcal{U}_{3}^{\blacksquare}\times\mathcal{U}_{4}^{\square}\boxplus\mathcal{U}_{3}^{\square}\times\mathcal{U}_{4}^{\blacksquare}$.
By UT:ProdLeft,
$\mathcal{U}_{3}^{\square}\times\mathcal{U}_{4}^{\blacksquare}\sqsubseteq\mathcal{U}_{3}^{\prime\square}\times\mathcal{U}_{4}^{\blacksquare}$.
By two applications of US:Subtype,
$\mathcal{U}\rightsquigarrow\mathcal{U}_{3}^{\blacksquare}\times\mathcal{U}_{4}^{\square}\boxplus\mathcal{U}_{1}^{\prime\prime}$.
By US:SplitLeft,
$\mathcal{U}_{3}^{\blacksquare}\times\mathcal{U}_{4}^{\square}\rightsquigarrow\mathcal{U}_{3}^{\prime\blacksquare}\times\mathcal{U}_{4}^{\square}\boxplus\mathcal{U}_{2}$.
Apply US:Subtype.

           2. (B)

$\mathcal{U}_{3}^{\prime\square}\times\mathcal{U}_{4}^{\blacksquare}\sqsubseteq\mathcal{U}_{1}^{\prime}$
and
$\mathcal{U}_{3}^{\prime\blacksquare}\times\mathcal{U}_{4}^{\square}\sqsubseteq\mathcal{U}_{1}^{\prime\prime}$.
By symmetry with the previous case.

           3. (C)

There exists $\mathcal{U}_{3}^{\prime\prime\prime}$ and
$\mathcal{U}_{3}^{\prime\prime\prime\prime}$ such that
$\mathcal{U}_{3}^{\prime}\rightsquigarrow\mathcal{U}_{3}^{\prime\prime\prime}\boxplus\mathcal{U}_{3}^{\prime\prime\prime\prime}$
and
$\mathcal{U}_{3}^{\prime\prime\prime\blacksquare}\times\mathcal{U}_{4}^{\blacksquare}\sqsubseteq\mathcal{U}_{1}^{\prime}$
and
$\mathcal{U}_{3}^{\prime\prime\prime\prime\blacksquare}\times\mathcal{U}_{4}^{\square}\sqsubseteq\mathcal{U}_{1}^{\prime\prime}$.
By induction, there exists $\mathcal{U}^{\prime\prime}$ such that
$\mathcal{U}_{3}\rightsquigarrow\mathcal{U}^{\prime\prime}\boxplus\mathcal{U}_{3}^{\prime\prime\prime\prime}$
and
$\mathcal{U}^{\prime\prime}\rightsquigarrow\mathcal{U}_{3}^{\prime\prime\prime}\boxplus\mathcal{U}_{3}^{\prime\prime}$.
By US:SplitLeft,
$\mathcal{U}\rightsquigarrow\mathcal{U}^{\prime\prime\blacksquare}\times\mathcal{U}_{4}^{\blacksquare}\boxplus\mathcal{U}_{3}^{\prime\prime\prime\prime\blacksquare}\times\mathcal{U}_{4}^{\square}$.
By US:Subtype,
$\mathcal{U}\rightsquigarrow\mathcal{U}^{\prime\prime\blacksquare}\times\mathcal{U}_{4}^{\blacksquare}\boxplus\mathcal{U}_{1}^{\prime\prime}$.
By US:SplitLeft,
$\mathcal{U}^{\prime\prime\blacksquare}\times\mathcal{U}_{4}^{\blacksquare}\rightsquigarrow\mathcal{U}_{3}^{\prime\prime\prime\blacksquare}\times\mathcal{U}_{4}^{\blacksquare}\boxplus\mathcal{U}_{2}$.
Apply US:Subtype.

           4. (D)

There exists $\mathcal{U}_{3}^{\prime\prime\prime}$ and
$\mathcal{U}_{3}^{\prime\prime\prime\prime}$ such that
$\mathcal{U}_{3}^{\prime}\rightsquigarrow\mathcal{U}_{3}^{\prime\prime\prime}\boxplus\mathcal{U}_{3}^{\prime\prime\prime\prime}$
and
$\mathcal{U}_{3}^{\prime\prime\prime\blacksquare}\times\mathcal{U}_{4}^{\square}\sqsubseteq\mathcal{U}_{1}^{\prime}$
and
$\mathcal{U}_{3}^{\prime\prime\prime\prime\blacksquare}\times\mathcal{U}_{4}^{\blacksquare}\sqsubseteq\mathcal{U}_{1}^{\prime\prime}$.
By symmetry with the previous case.

           5. (E)

There exists $\mathcal{U}_{4}^{\prime}$ and $\mathcal{U}_{4}^{\prime\prime}$
such that
$\mathcal{U}_{4}\rightsquigarrow\mathcal{U}_{4}^{\prime}\boxplus\mathcal{U}_{4}^{\prime\prime}$
and
$\mathcal{U}_{3}^{\prime\blacksquare}\times\mathcal{U}_{4}^{\prime\blacksquare}\sqsubseteq\mathcal{U}_{1}^{\prime}$
and
$\mathcal{U}_{3}^{\prime\square}\times\mathcal{U}_{4}^{\prime\prime\blacksquare}\sqsubseteq\mathcal{U}_{1}^{\prime\prime}$.
By US:SplitRight,
$\mathcal{U}\rightsquigarrow\mathcal{U}_{3}^{\blacksquare}\times\mathcal{U}_{4}^{\prime\blacksquare}\boxplus\mathcal{U}_{3}^{\square}\times\mathcal{U}_{4}^{\prime\prime\blacksquare}$.
By UT:ProdLeft,
$\mathcal{U}_{3}^{\square}\times\mathcal{U}_{4}^{\prime\prime\blacksquare}\sqsubseteq\mathcal{U}_{3}^{\prime\square}\times\mathcal{U}_{4}^{\prime\prime\blacksquare}$.
By two applications of US:Subtype,
$\mathcal{U}\rightsquigarrow\mathcal{U}_{3}^{\blacksquare}\times\mathcal{U}_{4}^{\prime\blacksquare}\boxplus\mathcal{U}_{1}^{\prime\prime}$.
By US:SplitLeft,
$\mathcal{U}_{3}^{\blacksquare}\times\mathcal{U}_{4}^{\prime\blacksquare}\rightsquigarrow\mathcal{U}_{3}^{\prime\blacksquare}\times\mathcal{U}_{4}^{\prime\blacksquare}\boxplus\mathcal{U}_{2}$.
Apply US:Subtype.

           6. (F)

There exists $\mathcal{U}_{4}^{\prime}$ and $\mathcal{U}_{4}^{\prime\prime}$
such that
$\mathcal{U}_{4}\rightsquigarrow\mathcal{U}_{4}^{\prime}\boxplus\mathcal{U}_{4}^{\prime\prime}$
and
$\mathcal{U}_{3}^{\prime\square}\times\mathcal{U}_{4}^{\prime\blacksquare}\sqsubseteq\mathcal{U}_{1}^{\prime}$
and
$\mathcal{U}_{3}^{\prime\blacksquare}\times\mathcal{U}_{4}^{\prime\prime\blacksquare}\sqsubseteq\mathcal{U}_{1}^{\prime\prime}$.
By symmetry with the previous case.

           7. (G)

There exists $\mathcal{U}_{3}^{\prime\prime\prime}$ and
$\mathcal{U}_{3}^{\prime\prime\prime\prime}$ and $\mathcal{U}_{4}^{\prime}$
and $\mathcal{U}_{4}^{\prime\prime}$ such that
$\mathcal{U}_{3}^{\prime}\rightsquigarrow\mathcal{U}_{3}^{\prime\prime\prime}\boxplus\mathcal{U}_{3}^{\prime\prime\prime\prime}$
and
$\mathcal{U}_{4}\rightsquigarrow\mathcal{U}_{4}^{\prime}\boxplus\mathcal{U}_{4}^{\prime\prime}$
and
$\mathcal{U}_{3}^{\prime\prime\prime\blacksquare}\times\mathcal{U}_{4}^{\prime\blacksquare}\sqsubseteq\mathcal{U}_{1}^{\prime}$
and
$\mathcal{U}_{3}^{\prime\prime\prime\prime\blacksquare}\times\mathcal{U}_{4}^{\prime\prime\blacksquare}\sqsubseteq\mathcal{U}_{1}^{\prime\prime}$.
By induction, there exists $\mathcal{U}^{\prime\prime}$ such that
$\mathcal{U}_{3}\rightsquigarrow\mathcal{U}^{\prime\prime}\boxplus\mathcal{U}_{3}^{\prime\prime\prime\prime}$
and
$\mathcal{U}^{\prime\prime}\rightsquigarrow\mathcal{U}_{3}^{\prime\prime\prime}\boxplus\mathcal{U}_{3}^{\prime\prime}$.
By US:SplitBoth,
$\mathcal{U}\rightsquigarrow\mathcal{U}^{\prime\prime\blacksquare}\times\mathcal{U}_{4}^{\prime\blacksquare}\boxplus\mathcal{U}_{3}^{\prime\prime\prime\prime\blacksquare}\times\mathcal{U}_{4}^{\prime\prime\blacksquare}$.
By US:Subtype,
$\mathcal{U}\rightsquigarrow\mathcal{U}^{\prime\prime\blacksquare}\times\mathcal{U}_{4}^{\prime\blacksquare}\boxplus\mathcal{U}_{1}^{\prime\prime}$.
By US:SplitLeft,
$\mathcal{U}^{\prime\prime\blacksquare}\times\mathcal{U}_{4}^{\prime\blacksquare}\rightsquigarrow\mathcal{U}_{3}^{\prime\prime\prime\blacksquare}\times\mathcal{U}_{4}^{\prime\blacksquare}\boxplus\mathcal{U}_{3}^{\prime\prime\blacksquare}\times\mathcal{U}_{4}^{\prime\square}$.
By UT:ProdRight,
$\mathcal{U}_{3}^{\prime\prime\blacksquare}\times\mathcal{U}_{4}^{\prime\square}\sqsubseteq\mathcal{U}_{2}$.
Apply US:Subtype twice.

       2. (b)

If
$\mathcal{U}_{2}\rightsquigarrow\mathcal{U}_{2}^{\prime}\boxplus\mathcal{U}_{2}^{\prime\prime}$,
by symmetry with the previous case when $a=\square$.

     * •

US:SplitRight. By symmetry with the previous case.

     * •

US:SplitBoth. Then
$\mathcal{U}=\mathcal{U}_{3}^{\blacksquare}\times\mathcal{U}_{4}^{\blacksquare}$
and
$\mathcal{U}_{3}\rightsquigarrow\mathcal{U}_{3}^{\prime}\boxplus\mathcal{U}_{3}^{\prime\prime}$
and
$\mathcal{U}_{4}\rightsquigarrow\mathcal{U}_{4}^{\prime}\boxplus\mathcal{U}_{4}^{\prime\prime}$
and
$\mathcal{U}_{1}=\mathcal{U}_{3}^{\prime\blacksquare}\times\mathcal{U}_{4}^{\prime\blacksquare}$
and
$\mathcal{U}_{2}=\mathcal{U}_{3}^{\prime\prime\blacksquare}\times\mathcal{U}_{4}^{\prime\prime\blacksquare}$.

       1. (a)

If
$\mathcal{U}_{1}\rightsquigarrow\mathcal{U}_{1}^{\prime}\boxplus\mathcal{U}_{1}^{\prime\prime}$,
by Lemma 1, there are seven cases:

         1. (i)

$\mathcal{U}_{3}^{\prime\blacksquare}\times\mathcal{U}_{4}^{\prime\square}\sqsubseteq\mathcal{U}_{1}^{\prime}$
and
$\mathcal{U}_{3}^{\prime\square}\times\mathcal{U}_{4}^{\prime\blacksquare}\sqsubseteq\mathcal{U}_{1}^{\prime\prime}$.
By US:Commutative,
$\mathcal{U}_{4}\rightsquigarrow\mathcal{U}_{4}^{\prime\prime}\boxplus\mathcal{U}_{4}^{\prime}$.
By US:SplitRight,
$\mathcal{U}\rightsquigarrow\mathcal{U}_{3}^{\blacksquare}\times\mathcal{U}_{4}^{\prime\prime\blacksquare}\boxplus\mathcal{U}_{3}^{\square}\times\mathcal{U}_{4}^{\prime\blacksquare}$.
By UT:ProdLeft,
$\mathcal{U}_{3}^{\square}\times\mathcal{U}_{4}^{\prime\blacksquare}\sqsubseteq\mathcal{U}_{3}^{\prime\square}\times\mathcal{U}_{4}^{\prime\blacksquare}$.
By two applications of US:Subtype,
$\mathcal{U}\rightsquigarrow\mathcal{U}_{3}^{\blacksquare}\times\mathcal{U}_{4}^{\prime\prime\blacksquare}\boxplus\mathcal{U}_{1}^{\prime\prime}$.
By US:Commutative,
$\mathcal{U}_{3}\rightsquigarrow\mathcal{U}_{3}^{\prime\prime}\boxplus\mathcal{U}_{3}^{\prime}$.
By US:SplitLeft,
$\mathcal{U}_{3}^{\blacksquare}\times\mathcal{U}_{4}^{\prime\prime\blacksquare}\rightsquigarrow\mathcal{U}_{2}\boxplus\mathcal{U}_{3}^{\prime\blacksquare}\times\mathcal{U}_{4}^{\prime\prime\square}$.
By US:Commutative,
$\mathcal{U}_{3}^{\blacksquare}\times\mathcal{U}_{4}^{\prime\prime\blacksquare}\rightsquigarrow\mathcal{U}_{3}^{\prime\blacksquare}\times\mathcal{U}_{4}^{\prime\prime\square}\boxplus\mathcal{U}_{2}$.
By UT:ProdRight,
$\mathcal{U}_{3}^{\prime\blacksquare}\times\mathcal{U}_{4}^{\prime\prime\square}\sqsubseteq\mathcal{U}_{3}^{\prime\blacksquare}\times\mathcal{U}_{4}^{\prime\square}$.
Apply US:Subtype.

         2. (ii)

$\mathcal{U}_{3}^{\prime\square}\times\mathcal{U}_{4}^{\prime\blacksquare}\sqsubseteq\mathcal{U}_{1}^{\prime}$
and
$\mathcal{U}_{3}^{\prime\blacksquare}\times\mathcal{U}_{4}^{\prime\square}\sqsubseteq\mathcal{U}_{1}^{\prime\prime}$.
By symmetry with the previous case.

         3. (iii)

There exists $\mathcal{U}_{3}^{\prime\prime\prime}$ and
$\mathcal{U}_{3}^{\prime\prime\prime\prime}$ such that
$\mathcal{U}_{3}^{\prime}\rightsquigarrow\mathcal{U}_{3}^{\prime\prime\prime}\boxplus\mathcal{U}_{3}^{\prime\prime\prime\prime}$
and
$\mathcal{U}_{3}^{\prime\prime\prime\blacksquare}\times\mathcal{U}_{4}^{\prime\blacksquare}\sqsubseteq\mathcal{U}_{1}^{\prime}$
and
$\mathcal{U}_{3}^{\prime\prime\prime\prime\blacksquare}\times\mathcal{U}_{4}^{\prime\square}\sqsubseteq\mathcal{U}_{1}^{\prime\prime}$.
By induction, there exists $\mathcal{U}^{\prime\prime}$ such that
$\mathcal{U}_{3}\rightsquigarrow\mathcal{U}^{\prime\prime}\boxplus\mathcal{U}_{3}^{\prime\prime\prime\prime}$
and
$\mathcal{U}^{\prime\prime}\rightsquigarrow\mathcal{U}_{3}^{\prime\prime\prime}\boxplus\mathcal{U}_{3}^{\prime\prime}$.
By US:SplitLeft,
$\mathcal{U}\rightsquigarrow\mathcal{U}^{\prime\prime\blacksquare}\times\mathcal{U}_{4}^{\blacksquare}\boxplus\mathcal{U}_{3}^{\prime\prime\prime\prime\blacksquare}\times\mathcal{U}_{4}^{\square}$.
By UT:ProdRight,
$\mathcal{U}_{3}^{\prime\prime\prime\prime\blacksquare}\times\mathcal{U}_{4}^{\square}\sqsubseteq\mathcal{U}_{3}^{\prime\prime\prime\prime\blacksquare}\times\mathcal{U}_{4}^{\prime\square}$.
By two applications of US:Subtype,
$\mathcal{U}\rightsquigarrow\mathcal{U}^{\prime\prime\blacksquare}\times\mathcal{U}_{4}^{\blacksquare}\boxplus\mathcal{U}_{1}^{\prime\prime}$.
By US:SplitBoth,
$\mathcal{U}^{\prime\prime\blacksquare}\times\mathcal{U}_{4}^{\blacksquare}\rightsquigarrow\mathcal{U}_{3}^{\prime\prime\prime\blacksquare}\times\mathcal{U}_{4}^{\prime\blacksquare}\boxplus\mathcal{U}_{2}$.
Apply US:Subtype.

         4. (iv)

There exists $\mathcal{U}_{3}^{\prime\prime\prime}$ and
$\mathcal{U}_{3}^{\prime\prime\prime\prime}$ such that
$\mathcal{U}_{3}^{\prime}\rightsquigarrow\mathcal{U}_{3}^{\prime\prime\prime}\boxplus\mathcal{U}_{3}^{\prime\prime\prime\prime}$
and
$\mathcal{U}_{3}^{\prime\prime\prime\blacksquare}\times\mathcal{U}_{4}^{\prime\square}\sqsubseteq\mathcal{U}_{1}^{\prime}$
and
$\mathcal{U}_{3}^{\prime\prime\prime\prime\blacksquare}\times\mathcal{U}_{4}^{\prime\blacksquare}\sqsubseteq\mathcal{U}_{1}^{\prime\prime}$.
By symmetry with the previous case.

         5. (v)

There exists $\mathcal{U}_{4}^{\prime\prime\prime}$ and
$\mathcal{U}_{4}^{\prime\prime\prime\prime}$ such that
$\mathcal{U}_{4}^{\prime}\rightsquigarrow\mathcal{U}_{4}^{\prime\prime\prime}\boxplus\mathcal{U}_{4}^{\prime\prime\prime\prime}$
and
$\mathcal{U}_{3}^{\prime\blacksquare}\times\mathcal{U}_{4}^{\prime\prime\prime\blacksquare}\sqsubseteq\mathcal{U}_{1}^{\prime}$
and
$\mathcal{U}_{3}^{\prime\square}\times\mathcal{U}_{4}^{\prime\prime\prime\prime\blacksquare}\sqsubseteq\mathcal{U}_{1}^{\prime\prime}$.
By symmetry with the previous case.

         6. (vi)

There exists $\mathcal{U}_{4}^{\prime\prime\prime}$ and
$\mathcal{U}_{4}^{\prime\prime\prime\prime}$ such that
$\mathcal{U}_{4}^{\prime}\rightsquigarrow\mathcal{U}_{4}^{\prime\prime\prime}\boxplus\mathcal{U}_{4}^{\prime\prime\prime\prime}$
and
$\mathcal{U}_{3}^{\prime\square}\times\mathcal{U}_{4}^{\prime\prime\prime\blacksquare}\sqsubseteq\mathcal{U}_{1}^{\prime}$
and
$\mathcal{U}_{3}^{\prime\blacksquare}\times\mathcal{U}_{4}^{\prime\prime\prime\prime\blacksquare}\sqsubseteq\mathcal{U}_{1}^{\prime\prime}$.
By symmetry with the previous case.

         7. (vii)

There exists $\mathcal{U}_{3}^{\prime\prime\prime}$ and
$\mathcal{U}_{3}^{\prime\prime\prime\prime}$ and
$\mathcal{U}_{4}^{\prime\prime\prime}$ and
$\mathcal{U}_{4}^{\prime\prime\prime\prime}$ such that
$\mathcal{U}_{3}^{\prime}\rightsquigarrow\mathcal{U}_{3}^{\prime\prime\prime}\boxplus\mathcal{U}_{3}^{\prime\prime\prime\prime}$
and
$\mathcal{U}_{4}^{\prime}\rightsquigarrow\mathcal{U}_{4}^{\prime\prime\prime}\boxplus\mathcal{U}_{4}^{\prime\prime\prime\prime}$
and
$\mathcal{U}_{3}^{\prime\prime\prime\blacksquare}\times\mathcal{U}_{4}^{\prime\prime\prime\blacksquare}\sqsubseteq\mathcal{U}_{1}^{\prime}$
and
$\mathcal{U}_{3}^{\prime\prime\prime\prime\blacksquare}\times\mathcal{U}_{4}^{\prime\prime\prime\prime\blacksquare}\sqsubseteq\mathcal{U}_{1}^{\prime\prime}$.
By induction, there exists $\mathcal{U}^{\prime\prime}$ such that
$\mathcal{U}_{3}\rightsquigarrow\mathcal{U}^{\prime\prime}\boxplus\mathcal{U}_{3}^{\prime\prime\prime\prime}$
and
$\mathcal{U}^{\prime\prime}\rightsquigarrow\mathcal{U}_{3}^{\prime\prime\prime}\boxplus\mathcal{U}_{3}^{\prime\prime}$
and there exists $\mathcal{U}^{\prime\prime\prime}$ such that
$\mathcal{U}_{4}\rightsquigarrow\mathcal{U}^{\prime\prime\prime}\boxplus\mathcal{U}_{4}^{\prime\prime\prime\prime}$
and
$\mathcal{U}^{\prime\prime\prime}\rightsquigarrow\mathcal{U}_{4}^{\prime\prime\prime}\boxplus\mathcal{U}_{4}^{\prime\prime}$.
By US:SplitBoth,
$\mathcal{U}\rightsquigarrow\mathcal{U}^{\prime\prime\blacksquare}\times\mathcal{U}^{\prime\prime\prime\blacksquare}\boxplus\mathcal{U}_{3}^{\prime\prime\prime\prime\blacksquare}\times\mathcal{U}_{4}^{\prime\prime\prime\prime\blacksquare}$.
By US:Subtype,
$\mathcal{U}\rightsquigarrow\mathcal{U}^{\prime\prime\blacksquare}\times\mathcal{U}^{\prime\prime\prime\blacksquare}\boxplus\mathcal{U}_{1}^{\prime\prime}$.
By US:SplitBoth,
$\mathcal{U}^{\prime\prime\blacksquare}\times\mathcal{U}^{\prime\prime\prime\blacksquare}\rightsquigarrow\mathcal{U}_{3}^{\prime\prime\prime\blacksquare}\times\mathcal{U}_{4}^{\prime\prime\prime\blacksquare}\boxplus\mathcal{U}_{2}$.
Apply US:Subtype.

       2. (b)

If
$\mathcal{U}_{2}\rightsquigarrow\mathcal{U}_{2}^{\prime}\boxplus\mathcal{U}_{2}^{\prime\prime}$,
by symmetry with the previous case.

     * •

US:Recursive. Then $\mathcal{U}=\mu t.\mathcal{U}^{\prime\prime}$ and
$\mathcal{U}^{\prime\prime}[\mu
t.\mathcal{U}^{\prime\prime}/t]\rightsquigarrow\mathcal{U}_{1}\boxplus\mathcal{U}_{2}$.

       1. (a)

If
$\mathcal{U}_{1}\rightsquigarrow\mathcal{U}_{1}^{\prime}\boxplus\mathcal{U}_{1}^{\prime\prime}$,
by induction, there exists $\mathcal{U}^{\prime}$ such that
$\mathcal{U}^{\prime\prime}[\mu
t.\mathcal{U}^{\prime\prime}/t]\rightsquigarrow\mathcal{U}^{\prime}\boxplus\mathcal{U}_{1}^{\prime\prime}$
and
$\mathcal{U}^{\prime}\rightsquigarrow\mathcal{U}_{1}^{\prime}\boxplus\mathcal{U}_{2}$.
Apply US:Recursive.

       2. (b)

If
$\mathcal{U}_{2}\rightsquigarrow\mathcal{U}_{2}^{\prime}\boxplus\mathcal{U}_{2}^{\prime\prime}$,
by symmetry with the previous case.

     * •

US:Corecursive. By symmetry with the previous case.

     * •

US:Subtype. Then
$\mathcal{U}\rightsquigarrow\mathcal{U}_{1}^{\prime\prime\prime}\boxplus\mathcal{U}_{2}$
and $\mathcal{U}_{1}^{\prime\prime\prime}\sqsubseteq\mathcal{U}_{1}$.

       1. (a)

If
$\mathcal{U}_{1}\rightsquigarrow\mathcal{U}_{1}^{\prime}\boxplus\mathcal{U}_{1}^{\prime\prime}$,
by Lemma 2,
$\mathcal{U}_{1}^{\prime\prime\prime}\rightsquigarrow\mathcal{U}_{1}^{\prime}\boxplus\mathcal{U}_{1}^{\prime\prime}$.
By induction.

       2. (b)

If
$\mathcal{U}_{2}\rightsquigarrow\mathcal{U}_{2}^{\prime}\boxplus\mathcal{U}_{2}^{\prime\prime}$,
by induction, there exists $\mathcal{U}^{\prime}$ such that
$\mathcal{U}\rightsquigarrow\mathcal{U}^{\prime}\boxplus\mathcal{U}_{2}^{\prime\prime}$
and
$\mathcal{U}^{\prime}\rightsquigarrow\mathcal{U}_{2}^{\prime}\boxplus\mathcal{U}_{1}^{\prime\prime\prime}$.
By US:Commutative and US:Subtype,
$\mathcal{U}^{\prime}\rightsquigarrow\mathcal{U}_{1}\boxplus\mathcal{U}_{2}^{\prime}$.
Apply US:Commutative.

     * •

US:Commutative. By induction.

  2. (2)

By induction on the derivation of
$\Omega\rightsquigarrow\Omega_{1}\boxplus\Omega_{2}$.

     * •

OM:Empty. Then $\Omega=\Omega_{1}=\Omega_{2}=\cdot$.

       1. (a)

If
$\Omega_{1}\rightsquigarrow\Omega_{1}^{\prime}\boxplus\Omega_{1}^{\prime\prime}$,
by inversion on OM:Empty,
$\Omega_{1}^{\prime}=\Omega_{1}^{\prime\prime}=\cdot$. Let $\Omega_{3}=\cdot$.
Apply OM:Empty twice.

       2. (b)

If
$\Omega_{2}\rightsquigarrow\Omega_{2}^{\prime}\boxplus\Omega_{2}^{\prime\prime}$,
by symmetry with the previous case.

     * •

OM:Commutative. By induction.

     * •

OM:Var. Then $\Omega=\Omega^{\prime\prime},u:\mathcal{U}$ and
$\Omega_{1}=\Omega_{3},u:\mathcal{U}$ and
$\Omega^{\prime\prime}\rightsquigarrow\Omega_{3}\boxplus\Omega_{2}$.

       1. (a)

If
$\Omega_{1}\rightsquigarrow\Omega_{1}^{\prime}\boxplus\Omega_{1}^{\prime\prime}$,
by Lemma 1, there are four cases:

         1. (i)

$\Omega_{1}^{\prime}=\Omega_{1}^{\prime\prime\prime},u:\mathcal{U}$ and
$\Omega_{3}\rightsquigarrow\Omega_{1}^{\prime\prime\prime}\boxplus\Omega_{1}^{\prime\prime}$.
By induction, there exists $\Omega^{\prime\prime\prime}$ such that
$\Omega^{\prime\prime}\rightsquigarrow\Omega^{\prime\prime\prime}\boxplus\Omega_{1}^{\prime\prime}$
and
$\Omega^{\prime\prime\prime}\rightsquigarrow\Omega_{1}^{\prime\prime\prime}\boxplus\Omega_{2}$.
By OM:Var,
$\Omega\rightsquigarrow\Omega^{\prime\prime\prime},u:\mathcal{U}\boxplus\Omega_{1}^{\prime\prime}$.
By OM:Var,
$\Omega^{\prime\prime\prime},u:\mathcal{U}\rightsquigarrow\Omega_{1}^{\prime}\boxplus\Omega_{2}$.

         2. (ii)

$\Omega_{1}^{\prime\prime}=\Omega_{1}^{\prime\prime\prime\prime},u:\mathcal{U}$
and
$\Omega_{3}\rightsquigarrow\Omega_{1}^{\prime}\boxplus\Omega_{1}^{\prime\prime\prime\prime}$.
By symmetry with the previous case.

         3. (iii)

$\mathcal{U}\rightsquigarrow\mathcal{U}_{1}\boxplus\mathcal{U}_{2}$ and
$\Omega_{1}^{\prime}=\Omega_{1}^{\prime\prime\prime},u:\mathcal{U}_{1}$ and
$\Omega_{1}^{\prime\prime}=\Omega_{1}^{\prime\prime\prime\prime},u:\mathcal{U}_{2}$
and
$\Omega_{3}\rightsquigarrow\Omega_{1}^{\prime\prime\prime}\boxplus\Omega_{1}^{\prime\prime\prime\prime}$.
By induction, there exists $\Omega^{\prime\prime\prime}$ such that
$\Omega^{\prime\prime}\rightsquigarrow\Omega^{\prime\prime\prime}\boxplus\Omega_{1}^{\prime\prime\prime\prime}$
and
$\Omega^{\prime\prime\prime}\rightsquigarrow\Omega_{1}^{\prime\prime\prime}\boxplus\Omega_{2}$.
By OM:VarTypeSplit,
$\Omega\rightsquigarrow\Omega^{\prime\prime\prime},u:\mathcal{U}_{1}\boxplus\Omega_{1}^{\prime\prime}$.
By OM:Var,
$\Omega^{\prime\prime\prime},u:\mathcal{U}\rightsquigarrow\Omega_{1}^{\prime}\boxplus\Omega_{2}$.

         4. (iv)

$\mathcal{U}\rightsquigarrow\mathcal{U}_{1}\boxplus\mathcal{U}_{2}$ and
$\Omega_{1}^{\prime}=\Omega_{1}^{\prime\prime\prime},u:\mathcal{U}_{2}$ and
$\Omega_{1}^{\prime\prime}=\Omega_{1}^{\prime\prime\prime\prime},u:\mathcal{U}_{1}$
and
$\Omega_{3}\rightsquigarrow\Omega_{1}^{\prime\prime\prime}\boxplus\Omega_{1}^{\prime\prime\prime\prime}$.
By symmetry with the previous case.

       2. (b)

If
$\Omega_{2}\rightsquigarrow\Omega_{2}^{\prime}\boxplus\Omega_{2}^{\prime\prime}$,
by induction, there exists $\Omega^{\prime\prime\prime}$ such that
$\Omega^{\prime\prime}\rightsquigarrow\Omega^{\prime\prime\prime}\boxplus\Omega_{2}^{\prime\prime}$
and
$\Omega^{\prime\prime\prime}\rightsquigarrow\Omega_{2}^{\prime}\boxplus\Omega_{3}$.
By OM:Var,
$\Omega\rightsquigarrow\Omega^{\prime\prime\prime},u:\mathcal{U}\boxplus\Omega_{2}^{\prime\prime}$.
By OM:Commutative and OM:Var,
$\Omega^{\prime\prime\prime},u:\mathcal{U}\rightsquigarrow\Omega_{1}\boxplus\Omega_{2}^{\prime}$.
Apply OM:Commutative.

     * •

OM:Gen. By symmetry with the previous case.

     * •

OM:VarTypeSplit. Then $\Omega=\Omega^{\prime\prime},u:\mathcal{U}$ and
$\mathcal{U}\rightsquigarrow\mathcal{U}_{1}\boxplus\mathcal{U}_{2}$ and
$\Omega_{1}=\Omega_{3},u:\mathcal{U}_{1}$ and
$\Omega_{2}=\Omega_{4},u:\mathcal{U}_{2}$ and
$\Omega^{\prime\prime}\rightsquigarrow\Omega_{3}\boxplus\Omega_{4}$.

       1. (a)

If
$\Omega_{1}\rightsquigarrow\Omega_{1}^{\prime}\boxplus\Omega_{1}^{\prime\prime}$,
by Lemma 1, there are four cases:

         1. (i)

$\Omega_{1}^{\prime}=\Omega_{1}^{\prime\prime\prime},u:\mathcal{U}_{1}$ and
$\Omega_{3}\rightsquigarrow\Omega_{1}^{\prime\prime\prime}\boxplus\Omega_{1}^{\prime\prime}$.
By induction, there exists $\Omega^{\prime\prime\prime}$ such that
$\Omega^{\prime\prime}\rightsquigarrow\Omega^{\prime\prime\prime}\boxplus\Omega_{1}^{\prime\prime}$
and
$\Omega^{\prime\prime\prime}\rightsquigarrow\Omega_{1}^{\prime\prime\prime}\boxplus\Omega_{4}$.
By OM:Var,
$\Omega\rightsquigarrow\Omega^{\prime\prime\prime},u:\mathcal{U}\boxplus\Omega_{1}^{\prime\prime}$.
By OM:VarTypeSplit,
$\Omega^{\prime\prime\prime},u:\mathcal{U}\rightsquigarrow\Omega_{1}^{\prime}\boxplus\Omega_{2}$.

         2. (ii)

$\Omega_{1}^{\prime\prime}=\Omega_{1}^{\prime\prime\prime\prime},u:\mathcal{U}$
and
$\Omega_{3}\rightsquigarrow\Omega_{1}^{\prime}\boxplus\Omega_{1}^{\prime\prime\prime\prime}$.
By symmetry with the previous case.

         3. (iii)

$\mathcal{U}_{1}\rightsquigarrow\mathcal{U}_{1}^{\prime}\boxplus\mathcal{U}_{1}^{\prime\prime}$
and
$\Omega_{1}^{\prime}=\Omega_{1}^{\prime\prime\prime},u:\mathcal{U}_{1}^{\prime}$
and
$\Omega_{1}^{\prime\prime}=\Omega_{1}^{\prime\prime\prime\prime},u:\mathcal{U}_{1}^{\prime\prime}$
and
$\Omega_{3}\rightsquigarrow\Omega_{1}^{\prime\prime\prime}\boxplus\Omega_{1}^{\prime\prime\prime\prime}$.
By part 1, there exists $\mathcal{U}^{\prime}$ such that
$\mathcal{U}\rightsquigarrow\mathcal{U}^{\prime}\boxplus\mathcal{U}_{1}^{\prime\prime}$
and
$\mathcal{U}^{\prime}\rightsquigarrow\mathcal{U}_{1}^{\prime}\boxplus\mathcal{U}_{2}$.
By induction, there exists $\Omega^{\prime\prime\prime}$ such that
$\Omega^{\prime\prime}\rightsquigarrow\Omega^{\prime\prime\prime}\boxplus\Omega_{1}^{\prime\prime\prime\prime}$
and
$\Omega^{\prime\prime\prime}\rightsquigarrow\Omega_{1}^{\prime\prime\prime}\boxplus\Omega_{4}$.
By OM:VarTypeSplit,
$\Omega\rightsquigarrow\Omega^{\prime\prime\prime},u:\mathcal{U}^{\prime}\boxplus\Omega_{1}^{\prime\prime}$.
By OM:VarTypeSplit,
$\Omega^{\prime\prime\prime},u:\mathcal{U}^{\prime}\rightsquigarrow\Omega_{1}^{\prime}\boxplus\Omega_{2}$.

         4. (iv)

$\mathcal{U}_{1}\rightsquigarrow\mathcal{U}_{1}^{\prime}\boxplus\mathcal{U}_{1}^{\prime\prime}$
and
$\Omega_{1}^{\prime}=\Omega_{1}^{\prime\prime\prime},u:\mathcal{U}_{1}^{\prime\prime}$
and
$\Omega_{1}^{\prime\prime}=\Omega_{1}^{\prime\prime\prime\prime},u:\mathcal{U}_{1}^{\prime}$
and
$\Omega_{3}\rightsquigarrow\Omega_{1}^{\prime\prime\prime}\boxplus\Omega_{1}^{\prime\prime\prime\prime}$.
By symmetry with the previous case.

       2. (b)

If
$\Omega_{2}\rightsquigarrow\Omega_{2}^{\prime}\boxplus\Omega_{2}^{\prime\prime}$,
by symmetry with the previous case.

     * •

OM:GenTypeSplit. By symmetry with the previous case.

  3. (3)

By part 2, there exists $\Omega^{\prime\prime\prime}$ such that
$\Omega\rightsquigarrow\Omega^{\prime\prime\prime}\boxplus\Omega_{1}^{\prime\prime}$
and
$\Omega^{\prime\prime\prime}\rightsquigarrow\Omega_{1}^{\prime}\boxplus\Omega_{2}$.
By part 2, there exists $\Omega^{\prime}$ such that
$\Omega^{\prime\prime\prime}\rightsquigarrow\Omega^{\prime}\boxplus\Omega_{2}^{\prime\prime}$
and
$\Omega^{\prime}\rightsquigarrow\Omega_{2}^{\prime}\boxplus\Omega_{1}^{\prime}$.
By OM:Commutative,
$\Omega^{\prime}\rightsquigarrow\Omega_{1}^{\prime}\boxplus\Omega_{2}^{\prime}$.
By OM:Commutative,
$\Omega^{\prime\prime\prime}\rightsquigarrow\Omega_{2}^{\prime\prime}\boxplus\Omega^{\prime}$.
By part 2, there exists $\Omega^{\prime\prime}$ such that
$\Omega\rightsquigarrow\Omega^{\prime\prime}\boxplus\Omega^{\prime}$ and
$\Omega^{\prime\prime}\rightsquigarrow\Omega_{2}^{\prime\prime}\boxplus\Omega_{1}^{\prime\prime}$.
By OM:Commutative,
$\Omega\rightsquigarrow\Omega^{\prime}\boxplus\Omega^{\prime\prime}$. By
OM:Commutative,
$\Omega^{\prime\prime}\rightsquigarrow\Omega_{1}^{\prime\prime}\boxplus\Omega_{2}^{\prime\prime}$.

∎

With the help of Lemmas 4 and 5, Lemma 6 proves that $\Omega$ context
splitting maintains weakening in VS typing: if $\Omega$ splits into
$\Omega^{\prime}$ and $U$ is well-typed under $\Omega^{\prime}$, then $U$ is
also well-typed under $\Omega$. The notable complication is a result of rule
OM:VarTypeSplit: a variable $u$ may be mapped to $\mathcal{U}$ in $\Omega$
while being mapped to $\mathcal{U}^{\prime}$ in $\Omega^{\prime}$ if
$\mathcal{U}$ splits into $\mathcal{U}^{\prime}$. In order for
$\Omega^{\prime}$ to be weakened to $\Omega$, it must be valid for $u$ to have
type $\mathcal{U}$ when it was expected to have type $\mathcal{U}^{\prime}$;
in other words, $\mathcal{U}$ must be a subtype of $\mathcal{U}^{\prime}$.
This is accomplished by Lemma 4, which shows that VS types always split into
supertypes. Lemma 5 acts as intermidiate between 4 and 6, stating that if
$\Omega$ splits into $\Omega^{\prime}$ and a variable $u$ is mapped to
$\mathcal{U}$ in $\Omega^{\prime}$, then $u$ is mapped to a subtype of
$\mathcal{U}$ in $\Omega$. An additional consequence of Lemma 5 is that
$\Omega$ context splitting cannot introduce new domain elements: if $\Omega$
splits into $\Omega^{\prime}$, then only variables and generators within
$\Omega$ may appear within $\Omega^{\prime}$.

###### Lemma 0.

If $\mathcal{U}\rightsquigarrow\mathcal{U}_{1}\boxplus\mathcal{U}_{2}$ then
$\mathcal{U}\sqsubseteq\mathcal{U}_{1}$ and
$\mathcal{U}\sqsubseteq\mathcal{U}_{2}$.

###### Proof.

By induction on the derivation of
$\mathcal{U}\rightsquigarrow\mathcal{U}_{1}\boxplus\mathcal{U}_{2}$.

  * •

US:Prod. Then
$\mathcal{U}=\mathcal{U}_{1}^{\prime\blacksquare}\times\mathcal{U}_{2}^{\prime\blacksquare}$
and
$\mathcal{U}_{1}=\mathcal{U}_{1}^{\prime\blacksquare}\times\mathcal{U}_{2}^{\prime\square}$
and
$\mathcal{U}_{2}=\mathcal{U}_{1}^{\prime\square}\times\mathcal{U}_{2}^{\prime\blacksquare}$.
Apply UT:ProdLeft and UT:ProdRight.

  * •

US:SplitBoth. Then
$\mathcal{U}=\mathcal{U}_{1}^{\prime\blacksquare}\times\mathcal{U}_{2}^{\prime\blacksquare}$
and
$\mathcal{U}_{1}=\mathcal{U}_{1}^{\prime\prime\blacksquare}\times\mathcal{U}_{2}^{\prime\prime\blacksquare}$
and
$\mathcal{U}_{2}=\mathcal{U}_{1}^{\prime\prime\prime\blacksquare}\times\mathcal{U}_{2}^{\prime\prime\prime\blacksquare}$
and
$\mathcal{U}_{1}^{\prime}\rightsquigarrow\mathcal{U}_{1}^{\prime\prime}\boxplus\mathcal{U}_{1}^{\prime\prime\prime}$
and
$\mathcal{U}_{2}^{\prime}\rightsquigarrow\mathcal{U}_{2}^{\prime\prime}\boxplus\mathcal{U}_{2}^{\prime\prime\prime}$.
By induction,
$\mathcal{U}_{1}^{\prime}\sqsubseteq\mathcal{U}_{1}^{\prime\prime}$ and
$\mathcal{U}_{1}^{\prime}\sqsubseteq\mathcal{U}_{1}^{\prime\prime\prime}$ and
$\mathcal{U}_{2}^{\prime}\sqsubseteq\mathcal{U}_{2}^{\prime\prime}$ and
$\mathcal{U}_{2}^{\prime}\sqsubseteq\mathcal{U}_{2}^{\prime\prime\prime}$.
Apply UT:Prod twice.

  * •

US:SplitLeft. Then
$\mathcal{U}=\mathcal{U}_{1}^{\prime\blacksquare}\times\mathcal{U}_{2}^{\prime
a}$ and
$\mathcal{U}_{1}=\mathcal{U}_{1}^{\prime\prime\blacksquare}\times\mathcal{U}_{2}^{\prime
a}$ and
$\mathcal{U}_{2}=\mathcal{U}_{1}^{\prime\prime\prime\blacksquare}\times\mathcal{U}_{2}^{\prime\square}$
and
$\mathcal{U}_{1}^{\prime}\rightsquigarrow\mathcal{U}_{1}^{\prime\prime}\boxplus\mathcal{U}_{1}^{\prime\prime\prime}$.
By induction,
$\mathcal{U}_{1}^{\prime}\sqsubseteq\mathcal{U}_{1}^{\prime\prime}$ and
$\mathcal{U}_{1}^{\prime}\sqsubseteq\mathcal{U}_{1}^{\prime\prime\prime}$. By
UT:Prod, $\mathcal{U}\sqsubseteq\mathcal{U}_{1}$ and
$\mathcal{U}\sqsubseteq\mathcal{U}_{1}^{\prime\prime\prime\blacksquare}\times\mathcal{U}_{2}^{\prime
a}$. By UT:ProdRight,
$\mathcal{U}_{1}^{\prime\prime\prime\blacksquare}\times\mathcal{U}_{2}^{\prime
a}\sqsubseteq\mathcal{U}_{2}$. Apply UT:Transitive.

  * •

US:SplitRight. By symmetry with the previous case.

  * •

US:Corecursive. Then $\mathcal{U}=\nu t.\mathcal{U}^{\prime}$ and
$\mathcal{U}^{\prime}[\nu
t.\mathcal{U}^{\prime}/t]\rightsquigarrow\mathcal{U}_{1}\boxplus\mathcal{U}_{2}$.
By induction,
$\mathcal{U}^{\prime}[\nu t.\mathcal{U}^{\prime}/t]\sqsubseteq\mathcal{U}_{1}$
and $\mathcal{U}^{\prime}[\nu
t.\mathcal{U}^{\prime}/t]\sqsubseteq\mathcal{U}_{2}$. By UT:Rec1,
$\mathcal{U}\sqsubseteq\mathcal{U}^{\prime}[\nu t.\mathcal{U}^{\prime}/t]$.
Apply UT:Transitive twice.

  * •

US:Subtype. Then $\mathcal{U}_{1}^{\prime}\sqsubseteq\mathcal{U}_{1}$. and
$\mathcal{U}\rightsquigarrow\mathcal{U}_{1}^{\prime}\boxplus\mathcal{U}_{2}$.
By induction, $\mathcal{U}\sqsubseteq\mathcal{U}_{1}^{\prime}$ and
$\mathcal{U}\sqsubseteq\mathcal{U}_{2}$. Apply UT:Transitive.

  * •

US:Commutative. By induction.

∎

###### Lemma 0.

If $\Omega\rightsquigarrow\Omega_{1}\boxplus\Omega_{2}$ then:

  1. (1)

If $u:\mathcal{U}\in\Omega_{1}$ then $u:\mathcal{U}^{\prime}\in\Omega$ and
$\mathcal{U}^{\prime}\sqsubseteq\mathcal{U}$.

  2. (2)

If $u:\mathcal{U}\in\Omega_{2}$ then $u:\mathcal{U}^{\prime}\in\Omega$ and
$\mathcal{U}^{\prime}\sqsubseteq\mathcal{U}$.

  3. (3)

If $\vec{u}:\mathcal{U}\in\Omega_{1}$ then
$\vec{u}:\mathcal{U}^{\prime}\in\Omega$ and
$\mathcal{U}^{\prime}\sqsubseteq\mathcal{U}$.

  4. (4)

If $\vec{u}:\mathcal{U}\in\Omega_{2}$ then
$\vec{u}:\mathcal{U}^{\prime}\in\Omega$ and
$\mathcal{U}^{\prime}\sqsubseteq\mathcal{U}$.

###### Proof.

By induction on the derivation of
$\Omega\rightsquigarrow\Omega_{1}\boxplus\Omega_{2}$.

  * •

OM:Commutative. By induction.

  * •

OM:Var. Then $\Omega=\Omega^{\prime},u^{\prime}:\mathcal{U}^{\prime\prime}$
and $\Omega_{1}=\Omega_{1}^{\prime},u^{\prime}:\mathcal{U}^{\prime\prime}$ and
$\Omega^{\prime}\rightsquigarrow\Omega_{1}^{\prime}\boxplus\Omega_{2}$.

    1. (1)

$u:\mathcal{U}\in\Omega_{1}$. There are two cases:

      1. (a)

$u=u^{\prime}$. Then $\mathcal{U}=\mathcal{U}^{\prime\prime}$ and
$u:\mathcal{U}\in\Omega$.

      2. (b)

$u\neq u^{\prime}$. Then $u:\mathcal{U}\in\Omega_{1}^{\prime}$. By induction,
$u:\mathcal{U}^{\prime}\in\Omega^{\prime}$ and
$\mathcal{U}^{\prime}\sqsubseteq\mathcal{U}$. Therefore,
$u:\mathcal{U}^{\prime}\in\Omega$.

    2. (2)

$u:\mathcal{U}\in\Omega_{2}$. By induction,
$u:\mathcal{U}^{\prime}\in\Omega^{\prime}$ and
$\mathcal{U}^{\prime}\sqsubseteq\mathcal{U}$. Therefore,
$u:\mathcal{U}^{\prime}\in\Omega$.

    3. (3)

$\vec{u}:\mathcal{U}\in\Omega_{1}$. Then
$\vec{u}:\mathcal{U}\in\Omega_{1}^{\prime}$. By induction,
$\vec{u}:\mathcal{U}^{\prime}\in\Omega^{\prime}$ and
$\mathcal{U}^{\prime}\sqsubseteq\mathcal{U}$. Therefore,
$\vec{u}:\mathcal{U}^{\prime}\in\Omega$.

    4. (4)

$\vec{u}:\mathcal{U}\in\Omega_{2}$. By induction,
$\vec{u}:\mathcal{U}^{\prime}\in\Omega^{\prime}$ and
$\mathcal{U}^{\prime}\sqsubseteq\mathcal{U}$. Therefore,
$\vec{u}:\mathcal{U}^{\prime}\in\Omega$.

  * •

OM:Gen. By symmetry with the previous case.

  * •

OM:VarTypeSplit. Then
$\Omega=\Omega^{\prime},u^{\prime}:\mathcal{U}^{\prime\prime}$ and
$\mathcal{U}^{\prime\prime}\rightsquigarrow\mathcal{U}_{1}\boxplus\mathcal{U}_{2}$.
and $\Omega_{1}=\Omega_{1}^{\prime},u^{\prime}:\mathcal{U}_{1}$. and
$\Omega_{2}=\Omega_{2}^{\prime},u^{\prime}:\mathcal{U}_{2}$.

    1. (1)

$u:\mathcal{U}\in\Omega_{1}$. There are two cases:

      1. (a)

$u=u^{\prime}$. Then $\mathcal{U}=\mathcal{U}_{1}$ and
$u:\mathcal{U}^{\prime\prime}\in\Omega$. By Lemma 4,
$\mathcal{U}^{\prime\prime}\sqsubseteq\mathcal{U}$.

      2. (b)

$u\neq u^{\prime}$. Then $u:\mathcal{U}\in\Omega_{1}^{\prime}$. By induction,
$u:\mathcal{U}^{\prime}\in\Omega^{\prime}$ and
$\mathcal{U}^{\prime}\sqsubseteq\mathcal{U}$. Therefore,
$u:\mathcal{U}^{\prime}\in\Omega$.

    2. (2)

$u:\mathcal{U}\in\Omega_{2}$. By symmetry with the previous case.

    3. (3)

$\vec{u}:\mathcal{U}\in\Omega_{1}$. Then
$\vec{u}:\mathcal{U}\in\Omega_{1}^{\prime}$. By induction,
$\vec{u}:\mathcal{U}^{\prime}\in\Omega^{\prime}$ and
$\mathcal{U}^{\prime}\sqsubseteq\mathcal{U}$. Therefore,
$\vec{u}:\mathcal{U}^{\prime}\in\Omega$.

    4. (4)

$\vec{u}:\mathcal{U}\in\Omega_{2}$. By symmetry with the previous case.

  * •

OM:GenTypeSplit. By symmetry with the previous case.

∎

###### Lemma 0.

If $\Omega\rightsquigarrow\Omega_{1}\boxplus\Omega_{0}$ and
$\Omega_{1};\Psi\vdash U:\mathcal{U}$ then $\Omega;\Psi\vdash U:\mathcal{U}$.

###### Proof.

By induction on the derivation of $\Omega_{1};\Psi\vdash U:\mathcal{U}$.

  * •

U:OmegaVar. Then $U=u$ and $\Omega_{1}=\Omega_{1}^{\prime},u:\mathcal{U}$. By
Lemma 5, $u:\mathcal{U}^{\prime}\in\Omega$ and
$\mathcal{U}^{\prime}\sqsubseteq\mathcal{U}$. By U:OmegaVar,
$\Omega;\Psi\vdash U:\mathcal{U}^{\prime}$. Apply U:Subtype.

  * •

U:OmegaSeed. By symmetry with the previous case.

  * •

U:PsiVar. Apply U:PsiVar.

  * •

U:PsiSeed. By symmetry with the previous case.

  * •

U:Pair. Then $U=(U_{1},U_{2})$ and
$\mathcal{U}=\mathcal{U}_{1}^{\blacksquare}\times\mathcal{U}_{2}^{\blacksquare}$
and
$\Omega_{1}\rightsquigarrow\Omega_{1}^{\prime}\boxplus\Omega_{1}^{\prime\prime}$
and $\Omega_{1}^{\prime};\Psi\vdash U_{1}:\mathcal{U}_{1}$ and
$\Omega_{1}^{\prime\prime};\Psi\vdash U_{2}:\mathcal{U}_{2}$. By Lemma 3,
there exists $\Omega^{\prime}$ such that
$\Omega\rightsquigarrow\Omega^{\prime}\boxplus\Omega_{1}^{\prime\prime}$ and
$\Omega^{\prime}\rightsquigarrow\Omega_{1}^{\prime}\boxplus\Omega_{0}$. By
induction, $\Omega^{\prime};\Psi\vdash U_{1}:\mathcal{U}_{1}$. Apply U:Pair.

  * •

All other cases are by induction and self-application.

∎

(DW:Empty) $\displaystyle\displaystyle{\hbox{\hskip 0.0pt\vbox{\hbox{\hskip
0.0pt\hbox{\hskip 0.0pt\hbox{}}}\vbox{\hbox{\hskip
0.0pt\hbox{}}\vbox{}}}}\over\hbox{\hskip
24.25005pt\vbox{\vbox{}\hbox{\hskip-24.25003pt\hbox{\hbox{$\displaystyle\displaystyle\Delta;\Omega;\Psi\vdash\bullet:*$}}}}}}$
(DW:Var) $\displaystyle\displaystyle{\hbox{\hskip 0.0pt\vbox{\hbox{\hskip
0.0pt\hbox{\hskip 0.0pt\hbox{}}}\vbox{\hbox{\hskip
0.0pt\hbox{}}\vbox{}}}}\over\hbox{\hskip
43.05772pt\vbox{\vbox{}\hbox{\hskip-43.05771pt\hbox{\hbox{$\displaystyle\displaystyle\Delta,\gamma:\kappa_{G};\Omega;\Psi\vdash\gamma:\kappa_{G}$}}}}}}$
(DW:Seq) $\displaystyle\displaystyle{\hbox{\hskip
99.13638pt\vbox{\hbox{\hskip-99.13637pt\hbox{\hbox{$\displaystyle\displaystyle\Omega\rightsquigarrow\Omega_{1}\boxplus\Omega_{2}$}\hskip
18.00003pt\hbox{\hbox{$\displaystyle\displaystyle\Delta;\Omega_{1};\Psi\vdash
G_{1}:*$}\hskip
18.00003pt\hbox{\hbox{$\displaystyle\displaystyle\Delta;\Omega_{2};\Psi\vdash
G_{2}:*$}}}}}\vbox{}}}\over\hbox{\hskip
36.34628pt\vbox{\vbox{}\hbox{\hskip-36.34627pt\hbox{\hbox{$\displaystyle\displaystyle\Delta;\Omega;\Psi\vdash
G_{1}\mathbin{\oplus}G_{2}:*$}}}}}}$ (DW:Or)
$\displaystyle\displaystyle{\hbox{\hskip
65.09631pt\vbox{\hbox{\hskip-65.09631pt\hbox{\hbox{$\displaystyle\displaystyle\Delta;\Omega;\Psi\vdash
G_{1}:*$}\hskip
18.00003pt\hbox{\hbox{$\displaystyle\displaystyle\Delta;\Omega;\Psi\vdash
G_{2}:*$}}}}\vbox{}}}\over\hbox{\hskip
36.84628pt\vbox{\vbox{}\hbox{\hskip-36.84627pt\hbox{\hbox{$\displaystyle\displaystyle\Delta;\Omega;\Psi\vdash
G_{1}\lor G_{2}:*$}}}}}}$ (DW:Spawn) $\displaystyle\displaystyle{\hbox{\hskip
91.14136pt\vbox{\hbox{\hskip-91.14134pt\hbox{\hbox{$\displaystyle\displaystyle\Omega\rightsquigarrow\Omega_{1}\boxplus\Omega_{2}$}\hskip
18.00003pt\hbox{\hbox{$\displaystyle\displaystyle\Delta;\Omega_{1};\Psi\vdash
G:*$}\hskip
18.00003pt\hbox{\hbox{$\displaystyle\displaystyle\Omega_{2};\cdot\vdash
U:\blacklozenge$}}}}}\vbox{}}}\over\hbox{\hskip
46.85854pt\vbox{\vbox{}\hbox{\hskip-46.85854pt\hbox{\hbox{$\displaystyle\displaystyle\Delta;\Omega;\Psi\vdash
G\\!\sswarrow_{U}:*$}}}}}}$ (DW:Touch)
$\displaystyle\displaystyle{\hbox{\hskip
23.31313pt\vbox{\hbox{\hskip-23.31313pt\hbox{\hbox{$\displaystyle\displaystyle\cdot;\Psi\vdash
U:\blacklozenge$}}}\vbox{}}}\over\hbox{\hskip
42.19542pt\vbox{\vbox{}\hbox{\hskip-42.1954pt\hbox{\hbox{$\displaystyle\displaystyle\Delta;\Omega;\Psi\vdash\mathop{{}^{U}\\!\ssearrow}:*$}}}}}}$
(DW:New) $\displaystyle\displaystyle{\hbox{\hskip
46.69028pt\vbox{\hbox{\hskip-46.69028pt\hbox{\hbox{$\displaystyle\displaystyle\Delta;\Omega,u:\mathcal{U};\Psi,u:\mathcal{U}\vdash
G:*$}}}\vbox{}}}\over\hbox{\hskip
46.2377pt\vbox{\vbox{}\hbox{\hskip-46.23769pt\hbox{\hbox{$\displaystyle\displaystyle\Delta;\Omega;\Psi\vdash\mathsf{new}~{}u\\!:\\!\mathcal{U}.G:*$}}}}}}$
(DW:Pi) $\displaystyle\displaystyle{\hbox{\hskip
61.98137pt\vbox{\hbox{\hskip-61.98137pt\hbox{\hbox{$\displaystyle\displaystyle\Delta;\Omega,u_{f}:\mathcal{U}_{f};\Psi,u_{f}:\mathcal{U}_{f},u_{t}:\mathcal{U}_{t}\vdash
G:*$}}}\vbox{}}}\over\hbox{\hskip
90.75246pt\vbox{\vbox{}\hbox{\hskip-90.75246pt\hbox{\hbox{$\displaystyle\displaystyle\Delta;\Omega;\Psi\vdash\Pi[u_{f}\\!:\\!\mathcal{U}_{f};u_{t}\\!:\\!\mathcal{U}_{t}].G:\Pi[u_{f}\\!:\\!\mathcal{U}_{f};u_{t}\\!:\\!\mathcal{U}_{t}].*$}}}}}}$
(DW:RecPi) $\displaystyle\displaystyle{\hbox{\hskip
96.66832pt\vbox{\hbox{\hskip-96.6683pt\hbox{\hbox{$\displaystyle\displaystyle\Delta,\gamma:\Pi[u_{f}\\!:\\!\mathcal{U}_{f};u_{t}\\!:\\!\mathcal{U}_{t}].*;u_{f}:\mathcal{U}_{f};\Psi,u_{f}:\mathcal{U}_{f},u_{t}:\mathcal{U}_{t}\vdash
G:*$}}}\vbox{}}}\over\hbox{\hskip
97.79372pt\vbox{\vbox{}\hbox{\hskip-97.79372pt\hbox{\hbox{$\displaystyle\displaystyle\Delta;\Omega;\Psi\vdash\mu\gamma.\Pi[u_{f}\\!:\\!\mathcal{U}_{f};u_{t}\\!:\\!\mathcal{U}_{t}].G:\Pi[u_{f}\\!:\\!\mathcal{U}_{f};u_{t}\\!:\\!\mathcal{U}_{t}].*$}}}}}}$
(DW:App) $\displaystyle\displaystyle{\hbox{\hskip
190.08981pt\vbox{\hbox{\hskip-190.08981pt\hbox{\hbox{$\displaystyle\displaystyle\Omega\rightsquigarrow\Omega_{1}\boxplus\Omega_{2}$}\hskip
18.00003pt\hbox{\hbox{$\displaystyle\displaystyle\Delta;\Omega_{1};\Psi\vdash
G:\Pi[u_{f}\\!:\\!\mathcal{U}_{f};u_{t}\\!:\\!\mathcal{U}_{t}].*$}\hskip
18.00003pt\hbox{\hbox{$\displaystyle\displaystyle\Omega_{2};\cdot\vdash
U_{f}:\mathcal{U}_{f}$}\hskip
18.00003pt\hbox{\hbox{$\displaystyle\displaystyle\cdot;\Psi\vdash
U_{f}:\mathcal{U}_{f}$}\hskip
18.00003pt\hbox{\hbox{$\displaystyle\displaystyle\cdot;\Psi\vdash
U_{t}:\mathcal{U}_{t}$}}}}}}}\vbox{}}}\over\hbox{\hskip
40.82938pt\vbox{\vbox{}\hbox{\hskip-40.82938pt\hbox{\hbox{$\displaystyle\displaystyle\Delta;\Omega;\Psi\vdash
G[U_{f};U_{t}]:*$}}}}}}$ Figure 32. Rules for graph type formation.
(UE:Reflexive) $\displaystyle\displaystyle{\hbox{\hskip
22.43813pt\vbox{\hbox{\hskip-22.43813pt\hbox{\hbox{$\displaystyle\displaystyle\cdot;\Psi\vdash
U:\mathcal{U}$}}}\vbox{}}}\over\hbox{\hskip
27.75125pt\vbox{\vbox{}\hbox{\hskip-27.75124pt\hbox{\hbox{$\displaystyle\displaystyle\Psi\vdash
U\equiv U:\mathcal{U}$}}}}}}$ (UE:Commutative)
$\displaystyle\displaystyle{\hbox{\hskip
27.19424pt\vbox{\hbox{\hskip-27.19423pt\hbox{\hbox{$\displaystyle\displaystyle\Psi\vdash
U^{\prime}\equiv U:\mathcal{U}$}}}\vbox{}}}\over\hbox{\hskip
27.19424pt\vbox{\vbox{}\hbox{\hskip-27.19423pt\hbox{\hbox{$\displaystyle\displaystyle\Psi\vdash
U\equiv U^{\prime}:\mathcal{U}$}}}}}}$ (UE:Transitive)
$\displaystyle\displaystyle{\hbox{\hskip
64.21747pt\vbox{\hbox{\hskip-64.21747pt\hbox{\hbox{$\displaystyle\displaystyle\Psi\vdash
U\equiv U^{\prime\prime}:\mathcal{U}$}\hskip
18.00003pt\hbox{\hbox{$\displaystyle\displaystyle\Psi\vdash
U^{\prime\prime}\equiv U^{\prime}:\mathcal{U}$}}}}\vbox{}}}\over\hbox{\hskip
27.19424pt\vbox{\vbox{}\hbox{\hskip-27.19423pt\hbox{\hbox{$\displaystyle\displaystyle\Psi\vdash
U\equiv U^{\prime}:\mathcal{U}$}}}}}}$ (UE:OnlyLeftPair)
$\displaystyle\displaystyle{\hbox{\hskip
66.50551pt\vbox{\hbox{\hskip-66.50551pt\hbox{\hbox{$\displaystyle\displaystyle\Psi\vdash
U_{1}\equiv U_{1}^{\prime}:\mathcal{U}_{1}$}\hskip
18.00003pt\hbox{\hbox{$\displaystyle\displaystyle\Psi^{\prime}\vdash
U_{2}\equiv U_{2}^{\prime}:\mathcal{U}_{2}$}}}}\vbox{}}}\over\hbox{\hskip
60.3125pt\vbox{\vbox{}\hbox{\hskip-60.31248pt\hbox{\hbox{$\displaystyle\displaystyle\Psi\vdash(U_{1},U_{2})\equiv(U_{1}^{\prime},U_{2}^{\prime}):\mathcal{U}_{1}^{\blacksquare}\times\mathcal{U}_{2}^{\square}$}}}}}}$
(UE:OnlyRightPair) $\displaystyle\displaystyle{\hbox{\hskip
65.25551pt\vbox{\hbox{\hskip-65.25551pt\hbox{\hbox{$\displaystyle\displaystyle\Psi^{\prime}\vdash
U_{1}\equiv U_{1}^{\prime}:\mathcal{U}_{1}$}\hskip
18.00003pt\hbox{\hbox{$\displaystyle\displaystyle\Psi\vdash U_{2}\equiv
U_{2}^{\prime}:\mathcal{U}_{2}$}}}}\vbox{}}}\over\hbox{\hskip
60.3125pt\vbox{\vbox{}\hbox{\hskip-60.31248pt\hbox{\hbox{$\displaystyle\displaystyle\Psi\vdash(U_{1},U_{2})\equiv(U_{1},U_{2}^{\prime}):\mathcal{U}_{1}^{\square}\times\mathcal{U}_{2}^{\blacksquare}$}}}}}}$
(UE:Pair) $\displaystyle\displaystyle{\hbox{\hskip
67.06252pt\vbox{\hbox{\hskip-67.06252pt\hbox{\hbox{$\displaystyle\displaystyle\Psi\vdash
U_{1}\equiv U_{1}^{\prime}:\mathcal{U}_{1}$}\hskip
18.00003pt\hbox{\hbox{$\displaystyle\displaystyle\Psi\vdash U_{2}\equiv
U_{2}^{\prime}:\mathcal{U}_{2}$}}}}\vbox{}}}\over\hbox{\hskip
60.3125pt\vbox{\vbox{}\hbox{\hskip-60.31248pt\hbox{\hbox{$\displaystyle\displaystyle\Psi\vdash(U_{1},U_{2})\equiv(U_{1}^{\prime},U_{2}^{\prime}):\mathcal{U}_{1}^{\blacksquare}\times\mathcal{U}_{2}^{\blacksquare}$}}}}}}$
(UE:Fst) $\displaystyle\displaystyle{\hbox{\hskip
36.58926pt\vbox{\hbox{\hskip-36.58925pt\hbox{\hbox{$\displaystyle\displaystyle\Psi\vdash
U\equiv
U^{\prime}:\mathcal{U}_{1}^{\blacksquare}\times\mathcal{U}_{2}^{a}$}}}\vbox{}}}\over\hbox{\hskip
38.75119pt\vbox{\vbox{}\hbox{\hskip-38.75119pt\hbox{\hbox{$\displaystyle\displaystyle\Psi\vdash\mathsf{fst}~{}U\equiv\mathsf{fst}~{}U^{\prime}:\mathcal{U}_{1}$}}}}}}$
(UE:Snd) $\displaystyle\displaystyle{\hbox{\hskip
36.58926pt\vbox{\hbox{\hskip-36.58925pt\hbox{\hbox{$\displaystyle\displaystyle\Psi\vdash
U\equiv
U^{\prime}:\mathcal{U}_{1}^{a}\times\mathcal{U}_{2}^{\blacksquare}$}}}\vbox{}}}\over\hbox{\hskip
42.5012pt\vbox{\vbox{}\hbox{\hskip-42.5012pt\hbox{\hbox{$\displaystyle\displaystyle\Psi\vdash\mathsf{snd}~{}U\equiv\mathsf{snd}~{}U^{\prime}:\mathcal{U}_{2}$}}}}}}$
(UE:FstPair) $\displaystyle\displaystyle{\hbox{\hskip
48.72939pt\vbox{\hbox{\hskip-48.72937pt\hbox{\hbox{$\displaystyle\displaystyle\Psi\vdash
U\equiv(U_{1},U_{2}):\mathcal{U}_{1}^{\blacksquare}\times\mathcal{U}_{2}^{a}$}}}\vbox{}}}\over\hbox{\hskip
34.16972pt\vbox{\vbox{}\hbox{\hskip-34.16972pt\hbox{\hbox{$\displaystyle\displaystyle\Psi\vdash\mathsf{fst}~{}U\equiv
U_{1}:\mathcal{U}_{1}$}}}}}}$ (UE:SndPair)
$\displaystyle\displaystyle{\hbox{\hskip
48.72939pt\vbox{\hbox{\hskip-48.72937pt\hbox{\hbox{$\displaystyle\displaystyle\Psi\vdash
U\equiv(U_{1},U_{2}):\mathcal{U}_{1}^{a}\times\mathcal{U}_{2}^{\blacksquare}$}}}\vbox{}}}\over\hbox{\hskip
36.04474pt\vbox{\vbox{}\hbox{\hskip-36.04472pt\hbox{\hbox{$\displaystyle\displaystyle\Psi\vdash\mathsf{snd}~{}U\equiv
U_{2}:\mathcal{U}_{2}$}}}}}}$ (UE:Subtype)
$\displaystyle\displaystyle{\hbox{\hskip
47.83026pt\vbox{\hbox{\hskip-47.83026pt\hbox{\hbox{$\displaystyle\displaystyle\Psi\vdash
U\equiv U^{\prime}:\mathcal{U}^{\prime}$}\hskip
18.00003pt\hbox{\hbox{$\displaystyle\displaystyle\mathcal{U}^{\prime}\sqsubseteq\mathcal{U}$}}}}\vbox{}}}\over\hbox{\hskip
27.19424pt\vbox{\vbox{}\hbox{\hskip-27.19423pt\hbox{\hbox{$\displaystyle\displaystyle\Psi\vdash
U\equiv U^{\prime}:\mathcal{U}$}}}}}}$ Figure 33. Vertex structure
equivalence. (CE:Reflexive) $\displaystyle\displaystyle{\hbox{\hskip
29.54015pt\vbox{\hbox{\hskip-29.54013pt\hbox{\hbox{$\displaystyle\displaystyle\Delta;\Psi;\Upsilon\vdash
c::\kappa$}}}\vbox{}}}\over\hbox{\hskip
37.48755pt\vbox{\vbox{}\hbox{\hskip-37.48755pt\hbox{\hbox{$\displaystyle\displaystyle\Delta;\Psi;\Upsilon\vdash
c\equiv c::\kappa$}}}}}}$ (CE:Commutative)
$\displaystyle\displaystyle{\hbox{\hskip
36.93054pt\vbox{\hbox{\hskip-36.93054pt\hbox{\hbox{$\displaystyle\displaystyle\Delta;\Psi;\Upsilon\vdash
c^{\prime}\equiv c::\kappa$}}}\vbox{}}}\over\hbox{\hskip
36.93054pt\vbox{\vbox{}\hbox{\hskip-36.93054pt\hbox{\hbox{$\displaystyle\displaystyle\Delta;\Psi;\Upsilon\vdash
c\equiv c^{\prime}::\kappa$}}}}}}$ (CE:Transitive)
$\displaystyle\displaystyle{\hbox{\hskip
83.69008pt\vbox{\hbox{\hskip-83.69008pt\hbox{\hbox{$\displaystyle\displaystyle\Delta;\Psi;\Upsilon\vdash
c\equiv c^{\prime\prime}::\kappa$}\hskip
18.00003pt\hbox{\hbox{$\displaystyle\displaystyle\Delta;\Psi;\Upsilon\vdash
c^{\prime\prime}\equiv c^{\prime}::\kappa$}}}}\vbox{}}}\over\hbox{\hskip
36.93054pt\vbox{\vbox{}\hbox{\hskip-36.93054pt\hbox{\hbox{$\displaystyle\displaystyle\Delta;\Psi;\Upsilon\vdash
c\equiv c^{\prime}::\kappa$}}}}}}$ (CE:Prod)
$\displaystyle\displaystyle{\hbox{\hskip
87.32973pt\vbox{\hbox{\hskip-87.32973pt\hbox{\hbox{$\displaystyle\displaystyle\Delta;\Psi;\Upsilon\vdash
c_{1}\equiv c_{1}^{\prime}::\mathsf{Ty}$}\hskip
18.00003pt\hbox{\hbox{$\displaystyle\displaystyle\Delta;\Psi;\Upsilon\vdash
c_{2}\equiv c_{2}^{\prime}::\mathsf{Ty}$}}}}\vbox{}}}\over\hbox{\hskip
54.57968pt\vbox{\vbox{}\hbox{\hskip-54.57968pt\hbox{\hbox{$\displaystyle\displaystyle\Delta;\Psi;\Upsilon\vdash
c_{1}\times c_{2}\equiv c_{1}^{\prime}\times
c_{2}^{\prime}::\mathsf{Ty}$}}}}}}$ (CE:Sum)
$\displaystyle\displaystyle{\hbox{\hskip
87.32973pt\vbox{\hbox{\hskip-87.32973pt\hbox{\hbox{$\displaystyle\displaystyle\Delta;\Psi;\Upsilon\vdash
c_{1}\equiv c_{1}^{\prime}::\mathsf{Ty}$}\hskip
18.00003pt\hbox{\hbox{$\displaystyle\displaystyle\Delta;\Psi;\Upsilon\vdash
c_{2}\equiv c_{2}^{\prime}::\mathsf{Ty}$}}}}\vbox{}}}\over\hbox{\hskip
54.57968pt\vbox{\vbox{}\hbox{\hskip-54.57968pt\hbox{\hbox{$\displaystyle\displaystyle\Delta;\Psi;\Upsilon\vdash
c_{1}+c_{2}\equiv c_{1}^{\prime}+c_{2}^{\prime}::\mathsf{Ty}$}}}}}}$ (CE:Fut)
$\displaystyle\displaystyle{\hbox{\hskip
75.6571pt\vbox{\hbox{\hskip-75.65709pt\hbox{\hbox{$\displaystyle\displaystyle\Delta;\Psi;\Upsilon\vdash
c\equiv c^{\prime}::\mathsf{Ty}$}\hskip
18.00003pt\hbox{\hbox{$\displaystyle\displaystyle\Psi\vdash U\equiv
U^{\prime}:\blacklozenge$}}}}\vbox{}}}\over\hbox{\hskip
79.42905pt\vbox{\vbox{}\hbox{\hskip-79.42905pt\hbox{\hbox{$\displaystyle\displaystyle\Delta;\Psi;\Upsilon\vdash
c~{}\mathsf{future}[U]\equiv
c^{\prime}~{}\mathsf{future}[U^{\prime}]::\mathsf{Ty}$}}}}}}$ (CE:Lambda)
$\displaystyle\displaystyle{\hbox{\hskip
48.78891pt\vbox{\hbox{\hskip-48.78891pt\hbox{\hbox{$\displaystyle\displaystyle\Delta;\Psi,u:\mathcal{U};\Upsilon\vdash
c\equiv c^{\prime}::\mathsf{Ty}$}}}\vbox{}}}\over\hbox{\hskip
69.865pt\vbox{\vbox{}\hbox{\hskip-69.865pt\hbox{\hbox{$\displaystyle\displaystyle\Delta;\Psi;\Upsilon\vdash\lambda
u\\!:\\!\mathcal{U}.c\equiv\lambda
u\\!:\\!\mathcal{U}.c^{\prime}::\mathcal{U}\rightarrow\mathsf{Ty}$}}}}}}$
(CE:App) $\displaystyle\displaystyle{\hbox{\hskip
80.40712pt\vbox{\hbox{\hskip-80.4071pt\hbox{\hbox{$\displaystyle\displaystyle\Delta;\Psi;\Upsilon\vdash
c\equiv c^{\prime}::\mathcal{U}\rightarrow\mathsf{Ty}$}\hskip
18.00003pt\hbox{\hbox{$\displaystyle\displaystyle\Psi\vdash U\equiv
U^{\prime}:\mathcal{U}$}}}}\vbox{}}}\over\hbox{\hskip
49.40399pt\vbox{\vbox{}\hbox{\hskip-49.40399pt\hbox{\hbox{$\displaystyle\displaystyle\Delta;\Psi;\Upsilon\vdash
c~{}U\equiv c^{\prime}~{}U^{\prime}::\mathsf{Ty}$}}}}}}$ (CE:BetaEq)
$\displaystyle\displaystyle{\hbox{\hskip
72.83665pt\vbox{\hbox{\hskip-72.83664pt\hbox{\hbox{$\displaystyle\displaystyle\Delta;\Psi,u:\mathcal{U};\Upsilon\vdash
c::\mathsf{Ty}$}\hskip
18.00003pt\hbox{\hbox{$\displaystyle\displaystyle\cdot;\Psi\vdash
U:\mathcal{U}$}}}}\vbox{}}}\over\hbox{\hskip
73.17168pt\vbox{\vbox{}\hbox{\hskip-73.17168pt\hbox{\hbox{$\displaystyle\displaystyle\Delta;\Psi;\Upsilon\vdash(\lambda
u\\!:\\!\mathcal{U}.c)~{}U\equiv c[U/u]::\mathsf{Ty}$}}}}}}$ (CE:Rec)
$\displaystyle\displaystyle{\hbox{\hskip
102.98685pt\vbox{\hbox{\hskip-102.98685pt\hbox{\hbox{$\displaystyle\displaystyle\Delta;\Psi,u:\mathcal{U};\Upsilon,\alpha::\mathcal{U}\rightarrow\mathsf{Ty}\vdash
c\equiv c^{\prime}::\mathsf{Ty}$}\hskip
18.00003pt\hbox{\hbox{$\displaystyle\displaystyle\Psi\vdash U\equiv
U^{\prime}:\mathcal{U}$}}}}\vbox{}}}\over\hbox{\hskip
94.23944pt\vbox{\vbox{}\hbox{\hskip-94.23944pt\hbox{\hbox{$\displaystyle\displaystyle\Delta;\Psi;\Upsilon\vdash\mu(\alpha;u\\!:\\!\mathcal{U}.c;U)\equiv\mu(\alpha;u\\!:\\!\mathcal{U}.c^{\prime};U^{\prime})::\mathsf{Ty}$}}}}}}$
Figure 34. Type constructor equivalence rules.

(DW:Par) $\displaystyle\displaystyle{\hbox{\hskip
111.54013pt\vbox{\hbox{\hskip-111.54012pt\hbox{\hbox{$\displaystyle\displaystyle\Omega\rightsquigarrow\Omega_{1}\boxplus\Omega_{2}$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle\Delta;\Omega_{1};\Psi\vdash
G_{1}:*$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle\Delta;\Omega_{2};\Psi\vdash
G_{2}:*$}}}}}\vbox{}}}\over\hbox{\hskip
40.38467pt\vbox{\vbox{}\hbox{\hskip-40.38466pt\hbox{\hbox{$\displaystyle\displaystyle\Delta;\Omega;\Psi\vdash
G_{1}\mathbin{\otimes}G_{2}:*$}}}}}}$ (C:Par)
$\displaystyle\displaystyle{\hbox{\hskip
46.72398pt\vbox{\hbox{\hskip-46.72398pt\hbox{\hbox{$\displaystyle\displaystyle
e_{1}\Downarrow v_{1}\mid g_{1}$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle e_{2}\Downarrow v_{2}\mid
g_{2}$}}}}\vbox{}}}\over\hbox{\hskip
55.90454pt\vbox{\vbox{}\hbox{\hskip-55.90454pt\hbox{\hbox{$\displaystyle\displaystyle\mathsf{par}(e_{1},e_{2})\Downarrow(v_{1},v_{2})\mid
g_{1}\mathbin{\otimes}g_{2}$}}}}}}$ (S:Par)
$\displaystyle\displaystyle{\hbox{\hskip
139.08446pt\vbox{\hbox{\hskip-139.08444pt\hbox{\hbox{$\displaystyle\displaystyle\Omega\rightsquigarrow\Omega_{1}\boxplus\Omega_{2}$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle\Delta;\Omega_{1};\Psi;\Gamma\vdash
e_{1}:\tau_{1}\mid G_{1}$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle\Delta;\Omega_{2};\Psi;\Gamma\vdash
e_{2}:\tau_{2}\mid G_{2}$}}}}}\vbox{}}}\over\hbox{\hskip
79.81796pt\vbox{\vbox{}\hbox{\hskip-79.81795pt\hbox{\hbox{$\displaystyle\displaystyle\Delta;\Omega;\Psi;\Gamma\vdash\mathsf{par}(e_{1},e_{2}):\tau_{1}\times\tau_{2}\mid
G_{1}\mathbin{\otimes}G_{2}$}}}}}}$

$\displaystyle\begin{array}[]{l r l l}\\\
\mathit{Graph~{}Types}&G&\mathop{::=}&\dots\mid G\mathbin{\otimes}G\\\
\penalty 50\hskip 20.00003pt plus 0.5fil minus
5.0pt\mathit{Expressions}&e&\mathop{::=}&\dots\mid\mathsf{par}(e,e)\end{array}$

$\begin{array}[]{r l l
l}\mathsf{NBNF}(G_{1}\mathbin{\otimes}G_{2})&\triangleq&\mathsf{NBNF}(G_{1})\mathbin{\otimes}\mathsf{NBNF}(G_{2})\\\
\mathit{Exp}(G_{1}\mathbin{\otimes}G_{2})&\triangleq&\\{g_{1}^{\prime}\mathbin{\otimes}g_{2}^{\prime}\mid
g_{1}^{\prime}\in\mathit{Exp}(G_{1}),g_{2}^{\prime}\in\mathit{Exp}(G_{2})&\\\
(V_{1},E_{1},s_{1},t_{1})\mathbin{\otimes}(V_{2},E_{2},s_{2},t_{2})&\triangleq&(V_{1}\cup
V_{2}\cup\\{u_{1},u_{2}\\},E_{1}\cup
E_{2}\cup&u_{1},u_{2}~{}\mathsf{fresh},\\\
&&~{}~{}\\{(u_{1},s_{1}),(u_{1},s_{2}),(t_{1},u_{2}),(t_{2},u_{2})\\},u_{1},u_{2})&V_{1}\cap
V_{2}=\emptyset\\\ \end{array}$

Figure 35. Adding fork-join parallelism to $\lambda^{G\mu}$.

Figures 32, 33, and 34 give the full rules for graph type formation, VS
equivalence, and type constructor equivalence respectively. Figure 35 adds the
syntax and rules for a fork-join parallel expression and graph type. Fork-join
parallellism in $\lambda^{G\mu}$ functions similar to how it does in Muller
(2022). The expression $\mathsf{par}(e_{1},e_{2})$ executes $e_{1}$ and
$e_{2}$ in parallel, and this expression is given the graph type
$G_{1}\mathbin{\otimes}G_{2}$ where $e_{1}$ has graph type $G_{1}$ and $e_{2}$
has graph type $G_{2}$.

Lemma 9 shows that well-formed VSs, expressions, type constructors, and graph
types maintain their types and kinds when substituting any free variables
appropriately. In addition, substituting variables in equivalent VSs and type
constructors maintains their equivalence. When substituting VS variables found
in the affine context $\Omega$, we require that the term undergoing the
substitution and the VS being substituted are well-typed under two disjoint
contexts $\Omega_{1}$ and $\Omega_{2}$, and the resulting term is well-typed
under their conjoinment (any $\Omega$ where
$\Omega\rightsquigarrow\Omega_{1}\boxplus\Omega_{2}$). When substituting a VS
variable $u$ with a VS $U$ in expressions and graph types, there are two
distinct cases: $u$ is in both $\Omega$ and $\Psi$ and $U$ is well-typed under
a disjoint $\Omega^{\prime}$ and separately well-typed under $\Psi$, or $u$ is
only in $\Psi$ and $U$ is well-typed under $\Psi$ (when assigning types to
expressions and graph kinds to graph types, it never occurs that a variable is
only in $\Omega$). We make these cases separate so that substituting variables
in $\Psi$ does not cause vertices only found within $\Psi$ to appear within
future spawns, but variables in $\Psi$ that do not appear within future spawns
can be more freely substituted for. Since we always require that VSs are
either typed under an empty $\Omega$ or an empty $\Psi$ in the rules for other
judgements, we have two cases for substituting VS variables that reflect that:
either the variable is in $\Omega$ and $\Psi$ is empty, or vice-versa.

This substitution lemma requires Lemmas 7 and 8. Lemma 7 states that if a VS
$U$ is given a type $\mathcal{U}$ under some $\Omega$, and $\mathcal{U}$
splits into $\mathcal{U}_{1}$ and $\mathcal{U}_{2}$, then $\Omega$ must split
into some $\Omega_{1}$ and $\Omega_{2}$ where $U$ has type $\mathcal{U}_{1}$
under $\Omega_{1}$ and has type $\mathcal{U}_{2}$ under $\Omega_{2}$. Lemma 8
states that the affine restriction can be removed from a VS typing judgement
and that judgement still holds.

###### Lemma 0.

If $\Omega;\cdot\vdash U:\mathcal{U}$ and
$\mathcal{U}\rightsquigarrow\mathcal{U}_{1}\boxplus\mathcal{U}_{2}$ then there
exists an $\Omega_{1}$ and $\Omega_{2}$ such that
$\Omega\rightsquigarrow\Omega_{1}\boxplus\Omega_{2}$ and
$\Omega_{1};\cdot\vdash U:\mathcal{U}_{1}$ and $\Omega_{2};\cdot\vdash
U:\mathcal{U}_{2}$.

###### Proof.

By induction on the derivation of $\Omega;\cdot\vdash U:\mathcal{U}$. We prove
some representative cases.

  * •

U:OmegaVar. Then $U=u$ and $\Omega=\Omega^{\prime},u:\mathcal{U}$. Since
$\Omega^{\prime}\rightsquigarrow\Omega^{\prime}\boxplus\cdot$, by
OM:TypeSplit, $\Omega\rightsquigarrow\Omega^{\prime},u:\mathcal{U}_{1}\boxplus
u:\mathcal{U}_{2}$. Apply U:Omega twice.

  * •

U:Pair. Then $U=(U_{1},U_{2})$ and
$\mathcal{U}=\mathcal{U}_{3}^{\blacksquare}\times\mathcal{U}_{4}^{\blacksquare}$
and $\Omega\rightsquigarrow\Omega_{3}\boxplus\Omega_{4}$ and
$\Omega_{3};\cdot\vdash U_{1}:\mathcal{U}_{3}$ and $\Omega_{4};\cdot\vdash
U_{2}:\mathcal{U}_{4}$. By Lemma 1, there are seven cases:

    1. (1)

$\mathcal{U}_{3}^{\blacksquare}\times\mathcal{U}_{4}^{\square}\sqsubseteq\mathcal{U}_{1}$
and
$\mathcal{U}_{3}^{\square}\times\mathcal{U}_{4}^{\blacksquare}\sqsubseteq\mathcal{U}_{2}$.
By U:OnlyLeftPair, $\Omega_{3};\cdot\vdash
U:\mathcal{U}_{3}^{\blacksquare}\times\mathcal{U}_{4}^{\square}$. By
U:OnlyRightPair, $\Omega_{4};\cdot\vdash
U:\mathcal{U}_{3}^{\square}\times\mathcal{U}_{4}^{\blacksquare}$. Apply
U:Subtype twice.

    2. (2)

$\mathcal{U}_{3}^{\square}\times\mathcal{U}_{4}^{\blacksquare}\sqsubseteq\mathcal{U}_{1}$
and
$\mathcal{U}_{3}^{\blacksquare}\times\mathcal{U}_{4}^{\square}\sqsubseteq\mathcal{U}_{2}$.
By symmetry with the previous case.

    3. (3)

There exists $\mathcal{U}_{3}^{\prime}$ and $\mathcal{U}_{3}^{\prime\prime}$
such that
$\mathcal{U}_{3}\rightsquigarrow\mathcal{U}_{3}^{\prime}\boxplus\mathcal{U}_{3}^{\prime\prime}$
and
$\mathcal{U}_{3}^{\prime\blacksquare}\times\mathcal{U}_{4}^{\blacksquare}\sqsubseteq\mathcal{U}_{1}$
and
$\mathcal{U}_{3}^{\prime\prime\blacksquare}\times\mathcal{U}_{4}^{\square}\sqsubseteq\mathcal{U}_{2}$.
By induction, there exists $\Omega_{3}^{\prime}$ and
$\Omega_{3}^{\prime\prime}$ such that
$\Omega_{3}\rightsquigarrow\Omega_{3}^{\prime}\boxplus\Omega_{3}^{\prime\prime}$
and $\Omega_{3}^{\prime};\cdot\vdash U_{1}:\mathcal{U}_{3}^{\prime}$ and
$\Omega_{3}^{\prime\prime};\cdot\vdash U_{1}:\mathcal{U}_{3}^{\prime\prime}$.
By Lemma 3, there exists $\Omega^{\prime}$ such that
$\Omega\rightsquigarrow\Omega^{\prime}\boxplus\Omega_{3}^{\prime\prime}$ and
$\Omega^{\prime}\rightsquigarrow\Omega_{3}^{\prime}\boxplus\Omega_{4}$. By
U:Pair, $\Omega^{\prime};\cdot\vdash
U:\mathcal{U}_{3}^{\prime\blacksquare}\times\mathcal{U}_{4}^{\blacksquare}$.
Apply U:Subtype. By U:OnlyLeftPair, $\Omega_{3}^{\prime\prime};\cdot\vdash
U:\mathcal{U}_{3}^{\prime\prime\blacksquare}\times\mathcal{U}_{4}^{\square}$.
Apply U:Subtype.

    4. (4)

There exists $\mathcal{U}_{3}^{\prime}$ and $\mathcal{U}_{3}^{\prime\prime}$
such that
$\mathcal{U}_{3}\rightsquigarrow\mathcal{U}_{3}^{\prime}\boxplus\mathcal{U}_{3}^{\prime\prime}$
and
$\mathcal{U}_{3}^{\prime\blacksquare}\times\mathcal{U}_{4}^{\square}\sqsubseteq\mathcal{U}_{1}$
and
$\mathcal{U}_{3}^{\prime\prime\blacksquare}\times\mathcal{U}_{4}^{\blacksquare}\sqsubseteq\mathcal{U}_{2}$.
By symmetry with the previous case.

    5. (5)

There exists $\mathcal{U}_{4}^{\prime}$ and $\mathcal{U}_{4}^{\prime\prime}$
such that
$\mathcal{U}_{4}\rightsquigarrow\mathcal{U}_{4}^{\prime}\boxplus\mathcal{U}_{4}^{\prime\prime}$
and
$\mathcal{U}_{3}^{\blacksquare}\times\mathcal{U}_{4}^{\prime\blacksquare}\sqsubseteq\mathcal{U}_{1}$
and
$\mathcal{U}_{3}^{\square}\times\mathcal{U}_{4}^{\prime\prime\blacksquare}\sqsubseteq\mathcal{U}_{2}$.
By symmetry with the previous case.

    6. (6)

There exists $\mathcal{U}_{4}^{\prime}$ and $\mathcal{U}_{4}^{\prime\prime}$
such that
$\mathcal{U}_{4}\rightsquigarrow\mathcal{U}_{4}^{\prime}\boxplus\mathcal{U}_{4}^{\prime\prime}$
and
$\mathcal{U}_{3}^{\square}\times\mathcal{U}_{4}^{\prime\blacksquare}\sqsubseteq\mathcal{U}_{1}$
and
$\mathcal{U}_{3}^{\blacksquare}\times\mathcal{U}_{4}^{\prime\prime\blacksquare}\sqsubseteq\mathcal{U}_{2}$.
By symmetry with the previous case.

    7. (7)

There exists $\mathcal{U}_{3}^{\prime}$ and $\mathcal{U}_{3}^{\prime\prime}$
and $\mathcal{U}_{4}^{\prime}$ and $\mathcal{U}_{4}^{\prime\prime}$ such that
$\mathcal{U}_{3}\rightsquigarrow\mathcal{U}_{3}^{\prime}\boxplus\mathcal{U}_{3}^{\prime\prime}$
and
$\mathcal{U}_{4}\rightsquigarrow\mathcal{U}_{4}^{\prime}\boxplus\mathcal{U}_{4}^{\prime\prime}$
and
$\mathcal{U}_{3}^{\prime\blacksquare}\times\mathcal{U}_{4}^{\prime\blacksquare}\sqsubseteq\mathcal{U}_{1}$
and
$\mathcal{U}_{3}^{\prime\prime\blacksquare}\times\mathcal{U}_{4}^{\prime\prime\blacksquare}\sqsubseteq\mathcal{U}_{2}$.
By induction, there exists $\Omega_{3}^{\prime}$ and
$\Omega_{3}^{\prime\prime}$ such that
$\Omega_{3}\rightsquigarrow\Omega_{3}^{\prime}\boxplus\Omega_{3}^{\prime\prime}$
and $\Omega_{3}^{\prime};\cdot\vdash U_{1}:\mathcal{U}_{3}^{\prime}$ and
$\Omega_{3}^{\prime\prime};\cdot\vdash U_{1}:\mathcal{U}_{3}^{\prime\prime}$
and there exists $\Omega_{4}^{\prime}$ and $\Omega_{4}^{\prime\prime}$ such
that
$\Omega_{4}\rightsquigarrow\Omega_{4}^{\prime}\boxplus\Omega_{4}^{\prime\prime}$
and $\Omega_{4}^{\prime};\cdot\vdash U_{2}:\mathcal{U}_{4}^{\prime}$ and
$\Omega_{4}^{\prime\prime};\cdot\vdash U_{2}:\mathcal{U}_{4}^{\prime\prime}$.
By Lemma 3, there exists $\Omega^{\prime}$ and $\Omega^{\prime\prime}$ such
that $\Omega\rightsquigarrow\Omega^{\prime}\boxplus\Omega^{\prime\prime}$ and
$\Omega^{\prime}\rightsquigarrow\Omega_{3}^{\prime}\boxplus\Omega_{4}^{\prime}$
and
$\Omega^{\prime\prime}\rightsquigarrow\Omega_{3}^{\prime\prime}\boxplus\Omega_{4}^{\prime\prime}$.
By U:Pair, $\Omega^{\prime};\cdot\vdash
U:\mathcal{U}_{3}^{\prime\blacksquare}\times\mathcal{U}_{4}^{\prime\blacksquare}$.
Apply U:Subtype. By U:Pair, $\Omega^{\prime\prime};\cdot\vdash
U:\mathcal{U}_{3}^{\prime\prime\blacksquare}\times\mathcal{U}_{4}^{\prime\prime\blacksquare}$.
Apply U:Subtype.

  * •

U:OnlyLeftPair. Then $U=(U_{1},U_{2})$ and
$\mathcal{U}=\mathcal{U}_{3}^{\blacksquare}\times\mathcal{U}_{4}^{\square}$
and $\Omega;\cdot\vdash U_{1}:\mathcal{U}_{3}$ and $\cdot;\Psi\vdash
U_{2}:\mathcal{U}_{4}$. By Lemma 1, there exists $\mathcal{U}_{3}^{\prime}$
and $\mathcal{U}_{3}^{\prime\prime}$ such that
$\mathcal{U}_{3}\rightsquigarrow\mathcal{U}_{3}^{\prime}\boxplus\mathcal{U}_{3}^{\prime\prime}$
and
$\mathcal{U}_{3}^{\prime\blacksquare}\times\mathcal{U}_{4}^{\square}\sqsubseteq\mathcal{U}_{1}$
and
$\mathcal{U}_{3}^{\prime\prime\blacksquare}\times\mathcal{U}_{4}^{\square}\sqsubseteq\mathcal{U}_{2}$.
By induction, there exists $\Omega_{1}$ and $\Omega_{2}$ such that
$\Omega\rightsquigarrow\Omega_{1}\boxplus\Omega_{2}$ and
$\Omega_{1};\cdot\vdash U:\mathcal{U}_{3}^{\prime}$ and
$\Omega_{2};\cdot\vdash U:\mathcal{U}_{3}^{\prime\prime}$. By U:OnlyLeftPair,
$\Omega_{1};\cdot\vdash
U:\mathcal{U}_{3}^{\prime\blacksquare}\times\mathcal{U}_{4}^{\square}$. Apply
U:Subtype. By U:OnlyLeftPair, $\Omega_{2};\cdot\vdash
U:\mathcal{U}_{3}^{\prime\prime\blacksquare}\times\mathcal{U}_{4}^{\square}$.
Apply U:Subtype.

  * •

U:Fst. Then $U=\mathsf{fst}~{}U^{\prime}$ and $\Omega;\cdot\vdash
U^{\prime}:\mathcal{U}^{\blacksquare}\times\mathcal{U}_{3}^{a}$. By
US:SplitLeft,
$\mathcal{U}^{\blacksquare}\times\mathcal{U}_{3}^{a}\rightsquigarrow\mathcal{U}_{1}^{\blacksquare}\times\mathcal{U}_{3}^{a}\boxplus\mathcal{U}_{2}^{\blacksquare}\times\mathcal{U}_{3}^{\square}$.
By induction, there exists $\Omega_{1}$ and $\Omega_{2}$ such that
$\Omega\rightsquigarrow\Omega_{1}\boxplus\Omega_{2}$ and
$\Omega_{1};\cdot\vdash
U^{\prime}:\mathcal{U}_{1}^{\blacksquare}\times\mathcal{U}_{3}^{a}$ and
$\Omega_{2};\cdot\vdash
U^{\prime}:\mathcal{U}_{2}^{\blacksquare}\times\mathcal{U}_{3}^{\square}$.
Apply U:Fst twice.

  * •

U:Subtype. Then $\mathcal{U}^{\prime}\sqsubseteq\mathcal{U}$ and
$\Omega;\cdot\vdash U:\mathcal{U}^{\prime}$. By Lemma 2,
$\mathcal{U}^{\prime}\rightsquigarrow\mathcal{U}_{1}\boxplus\mathcal{U}_{2}$.
Apply induction.

∎

The proof for Lemma 8 is straightforward, so it is ommited.

###### Lemma 0.

If $\Omega;\cdot\vdash U:\mathcal{U}$ then $\cdot;\Omega\vdash U:\mathcal{U}$.

###### Lemma 0.

  1. (1)

If $\Delta;\Omega;\Psi;\Gamma,x:\tau^{\prime}\vdash e:\tau\mid G$ and
$\cdot;\cdot;\Psi;\cdot\vdash v:\tau^{\prime}\mid\bullet$ then
$\Delta;\Omega;\Psi;\Gamma\vdash e[v/x]:\tau\mid G$.

  2. (2)

If $\Delta;\Psi;\Upsilon,\alpha::\kappa^{\prime}\vdash c::\kappa$ and
$\Delta;\Psi;\Upsilon\vdash c^{\prime}::\kappa^{\prime}$ then
$\Delta;\Psi;\Upsilon\vdash c[c^{\prime}/\alpha]::\kappa$.

  3. (3)

If $\Delta,\gamma:\kappa_{G}^{\prime};\Omega;\Psi\vdash G:\kappa_{G}$ and
$\Delta;\cdot;\Psi\vdash G^{\prime}:\kappa_{G}^{\prime}$ then
$\Delta;\Omega;\Psi\vdash G[G^{\prime}/\gamma]:\kappa_{G}$.

  4. (4)

If $\Delta,\gamma:\kappa_{G};\Psi;\Upsilon\vdash c::\kappa$ and
$\Delta;\cdot;\Psi\vdash G:\kappa_{G}$ then $\Delta;\Psi;\Upsilon\vdash
c[G/\gamma]::\kappa$.

  5. (5)

If $\Delta,\gamma:\kappa_{G};\Psi;\Upsilon\vdash c_{1}\equiv c_{2}::\kappa$
and $\Delta;\cdot;\Psi\vdash G:\kappa_{G}$ then $\Delta;\Psi;\Upsilon\vdash
c_{1}[G/\gamma]\equiv c_{2}[G/\gamma]::\kappa$.

  6. (6)

If $\Delta,\gamma:\kappa_{G};\Omega;\Psi;\Gamma\vdash e:\tau\mid G$ and
$\Delta;\cdot;\Psi\vdash G^{\prime}:\kappa_{G}$ then
$\Delta;\Omega;\Psi;\Gamma[G^{\prime}/\gamma]\vdash
e:\tau[G^{\prime}/\gamma]\mid G[G^{\prime}/\gamma]$.

  7. (7)

If $\cdot;\Psi,u:\mathcal{U}^{\prime}\vdash U:\mathcal{U}$ and
$\cdot;\Psi\vdash U^{\prime}:\mathcal{U}^{\prime}$ then $\cdot;\Psi\vdash
U[U^{\prime}/u]:\mathcal{U}$.

  8. (8)

If $\Omega,u:\mathcal{U}^{\prime};\cdot\vdash U:\mathcal{U}$ and
$\Omega^{\prime};\cdot\vdash U^{\prime}:\mathcal{U}^{\prime}$ and
$\Omega^{\prime\prime}\rightsquigarrow\Omega\boxplus\Omega^{\prime}$ then
$\Omega^{\prime\prime};\cdot\vdash U[U^{\prime}/u]:\mathcal{U}$.

  9. (9)

If $\Delta;\Omega;\Psi,u:\mathcal{U}\vdash G:\kappa_{G}$ and $\cdot;\Psi\vdash
U:\mathcal{U}$ and $u\notin\Omega$ then $\Delta;\Omega;\Psi\vdash
G[U/u]:\kappa_{G}$.

  10. (10)

If $\Delta;\Omega,u:\mathcal{U};\Psi,u:\mathcal{U}^{\prime}\vdash
G:\kappa_{G}$ and $\Omega^{\prime};\cdot\vdash U:\mathcal{U}$ and
$\cdot;\Psi\vdash U:\mathcal{U}^{\prime}$ and
$\Omega^{\prime\prime}\rightsquigarrow\Omega\boxplus\Omega^{\prime}$ then
$\Delta;\Omega^{\prime\prime};\Psi\vdash G[U/u]:\kappa_{G}$.

  11. (11)

If $\Delta;\Psi,u:\mathcal{U};\Upsilon\vdash c::\kappa$ and $\cdot;\Psi\vdash
U:\mathcal{U}$ then $\Delta;\Psi;\Upsilon\vdash c[U/u]::\kappa$.

  12. (12)

If $\Psi,u:\mathcal{U}^{\prime}\vdash U_{1}\equiv U_{2}:\mathcal{U}$ and
$\cdot;\Psi\vdash U:\mathcal{U}^{\prime}$ then $\Psi\vdash U_{1}[U/u]\equiv
U_{2}[U/u]:\mathcal{U}$.

  13. (13)

If $\Delta;\Psi,u:\mathcal{U};\Upsilon\vdash c_{1}\equiv c_{2}::\kappa$ and
$\cdot;\Psi\vdash U:\mathcal{U}$ then $\Delta;\Psi;\Upsilon\vdash
c_{1}[U/u]\equiv c_{2}[U/u]::\kappa$.

  14. (14)

If $\Delta;\Omega;\Psi,u:\mathcal{U};\Gamma\vdash e:\tau\mid G$ and
$\cdot;\Psi\vdash U:\mathcal{U}$ and $u\notin\Omega$ then
$\Delta;\Omega;\Psi;\Gamma[U/u]\vdash e[U/u]:\tau[U/u]\mid G[U/u]$.

  15. (15)

If $\Delta;\Omega,u:\mathcal{U};\Psi,u:\mathcal{U}^{\prime};\Gamma\vdash
e:\tau\mid G$ and $\Omega^{\prime};\cdot\vdash U:\mathcal{U}$ and
$\cdot;\Psi\vdash U:\mathcal{U}^{\prime}$ and
$\Omega^{\prime\prime}\rightsquigarrow\Omega\boxplus\Omega^{\prime}$ then
$\Delta;\Omega^{\prime\prime};\Psi;\Gamma[U/u]\vdash e[U/u]:\tau[U/u]\mid
G[U/u]$.

###### Proof.

We show the interesting cases for all parts except (1), which is standard.

  1. (1)

By induction on the derivation of
$\Delta;\Omega;\Psi;\Gamma,x:\tau^{\prime}\vdash e:\tau\mid G$.

  2. (2)

By induction on the derivation of
$\Delta;\Psi;\Upsilon,\alpha::\kappa^{\prime}\vdash c::\kappa$.

     * •

K:Rec. Then $c=\mu(\alpha^{\prime};u\\!:\\!\mathcal{U}.c^{\prime\prime};U)$
and $\kappa=\mathsf{Ty}$ and
$\Delta;\Psi,u:\mathcal{U};\Upsilon,\alpha^{\prime}::\mathcal{U}\rightarrow\mathsf{Ty},\alpha::\kappa^{\prime}\vdash
c^{\prime\prime}::\mathsf{Ty}$. Since $\alpha^{\prime}$ is bound inside $c$,
$\alpha\neq\alpha^{\prime}$. By induction,
$\Delta;\Psi,u:\mathcal{U};\Upsilon,\alpha^{\prime}::\mathcal{U}\rightarrow\mathsf{Ty}\vdash
c^{\prime\prime}[c^{\prime}/\alpha]::\mathsf{Ty}$. Apply K:Rec.

  3. (3)

By induction on the derivation of
$\Delta,\gamma:\kappa_{G}^{\prime};\Omega;\Psi\vdash G:\kappa_{G}$.

     * •

DW:RecPi. Then $G=\mu\gamma^{\prime}.\Pi[u_{f};u_{t}].G^{\prime\prime}$ and
$\kappa_{G}=\Pi[u_{f}\\!:\\!\mathcal{U}_{f};u_{t}\\!:\\!\mathcal{U}_{t}].*$
and
$\Delta,\gamma^{\prime}:\Pi[u_{f}\\!:\\!\mathcal{U}_{f};u_{t}\\!:\\!\mathcal{U}_{t}].*,\gamma:\kappa_{G}^{\prime};u_{f}:\mathcal{U}_{f};\Psi,u_{f}:\mathcal{U}_{f},u_{t}:\mathcal{U}_{t}\vdash
G:*$. By induction,
$\Delta,\gamma^{\prime}:\Pi[u_{f}\\!:\\!\mathcal{U}_{f};u_{t}\\!:\\!\mathcal{U}_{t}].*;u_{f}:\mathcal{U}_{f};\Psi,u_{f}:\mathcal{U}_{f},u_{t}:\mathcal{U}_{t}\vdash
G^{\prime\prime}[G^{\prime}/\gamma]:*$. Apply DW:RecPi.

  4. (4)

By induction on the derivation of
$\Delta,\gamma:\kappa_{G};\Psi;\Upsilon\vdash c::\kappa$.

     * •

K:Fun. Then
$c=\Pi[u_{f}\\!:\\!\mathcal{U}_{f};u_{t}\\!:\\!\mathcal{U}_{t}].c_{1}\xrightarrow{G^{\prime}[u_{f};u_{t}]}c_{2}$
and
$\Delta,\gamma:\kappa_{G};\Psi,u_{f}:\mathcal{U}_{f},u_{t}:\mathcal{U}_{t};\Upsilon\vdash
c_{1}::\mathsf{Ty}$ and
$\Delta,\gamma:\kappa_{G};\Psi,u_{f}:\mathcal{U}_{f},u_{t}:\mathcal{U}_{t};\Upsilon\vdash
c_{2}::\mathsf{Ty}$ and $\Delta,\gamma:\kappa_{G};\cdot;\Psi\vdash
G^{\prime}:\Pi[u_{f}\\!:\\!\mathcal{U}_{f};u_{t}\\!:\\!\mathcal{U}_{t}].*$ and
$\kappa=\mathsf{Ty}$. By induction,
$\Delta;\Psi,u_{f}:\mathcal{U}_{f},u_{t}:\mathcal{U}_{t};\Upsilon\vdash
c_{1}[G/\gamma]::\mathsf{Ty}$ and
$\Delta;\Psi,u_{f}:\mathcal{U}_{f},u_{t}:\mathcal{U}_{t};\Upsilon\vdash
c_{2}[G/\gamma]::\mathsf{Ty}$. By part 3, $\Delta;\cdot;\Psi\vdash
G^{\prime}[G/\gamma]:\Pi[u_{f}\\!:\\!\mathcal{U}_{f};u_{t}\\!:\\!\mathcal{U}_{t}].*$.
Apply K:Fun.

  5. (5)

By induction on the derivation of
$\Delta,\gamma:\kappa_{G};\Psi;\Upsilon\vdash c_{1}\equiv c_{2}::\kappa$.

     * •

CE:Reflexive. Then $c_{1}=c_{2}$, and
$\Delta,\gamma:\kappa_{G};\Psi;\Upsilon\vdash c_{1}::\kappa$. By part 4,
$\Delta;\Psi;\Upsilon\vdash c_{1}[G/\gamma]::\kappa$. Apply CE:Reflexive.

     * •

CE:Prod. Then $c_{1}=c_{3}\times c_{4}$ and $c_{2}=c_{3}^{\prime}\times
c_{4}^{\prime}$ and $\kappa=\mathsf{Ty}$ and
$\Delta,\gamma:\kappa_{G};\Psi;\Upsilon\vdash c_{3}\equiv
c_{3}^{\prime}::\mathsf{Ty}$ and $\Delta,\gamma:\kappa_{G};\Psi;\Upsilon\vdash
c_{4}\equiv c_{4}^{\prime}::\mathsf{Ty}$. By induction,
$\Delta;\Psi;\Upsilon\vdash c_{3}[G/\gamma]\equiv
c_{3}^{\prime}[G/\gamma]::\mathsf{Ty}$ and $\Delta;\Psi;\Upsilon\vdash
c_{4}[G/\gamma]\equiv c_{4}^{\prime}[G/\gamma]::\mathsf{Ty}$. Apply CE:Prod.

  6. (6)

By induction on the derivation of
$\Delta,\gamma:\kappa_{G};\Omega;\Psi;\Gamma\vdash e:\tau\mid G$.

     * •

S:Fun. Then
$\tau=\Pi[u_{f}\\!:\\!\mathcal{U}_{f};u_{t}\\!:\\!\mathcal{U}_{t}].\tau_{1}\xrightarrow{(\mu\gamma^{\prime}.\Pi[u_{f}:\mathcal{U}_{f};u_{t}:\mathcal{U}_{t}].G^{\prime\prime})[u_{f};u_{t}]}\tau_{2}$
and $e=\mathsf{fun}[u_{f};u_{t}]~{}f~{}x=e^{\prime}$ and $G=\bullet$ and
$\Delta,\gamma:\kappa_{G},\gamma^{\prime}:\Pi[u_{f}\\!:\\!\mathcal{U}_{f};u_{t}\\!:\\!\mathcal{U}_{t}].*;u_{f}:\mathcal{U}_{f};\Psi,u_{f}:\mathcal{U}_{f},u_{t}:\mathcal{U}_{t};\Gamma,f:\Pi[u_{f}\\!:\\!\mathcal{U}_{f};u_{t}\\!:\\!\mathcal{U}_{t}].\tau_{1}\xrightarrow{\gamma^{\prime}[u_{f};u_{t}]}\tau_{2},x:\tau_{1}\vdash
e^{\prime}:\tau_{2}\mid G^{\prime\prime}$ and
$\Delta,\gamma:\kappa_{G};\Psi,u_{f}:\mathcal{U}_{f},u_{t}:\mathcal{U}_{t};\cdot\vdash\tau_{1}::\mathsf{Ty}$
and
$\Delta,\gamma:\kappa_{G};\Psi,u_{f}:\mathcal{U}_{f},u_{t}:\mathcal{U}_{t};\cdot\vdash\tau_{2}::\mathsf{Ty}$.
By induction,
$\Delta,\gamma^{\prime}:\Pi[u_{f}\\!:\\!\mathcal{U}_{f};u_{t}\\!:\\!\mathcal{U}_{t}].*;u_{f}:\mathcal{U}_{f};\Psi,u_{f}:\mathcal{U}_{f},u_{t}:\mathcal{U}_{t};\Gamma[G^{\prime}/\gamma],f:\Pi[u_{f}\\!:\\!\mathcal{U}_{f};u_{t}\\!:\\!\mathcal{U}_{t}].\tau_{1}[G^{\prime}/\gamma]\xrightarrow{\gamma^{\prime}[u_{f};u_{t}]}\tau_{2}[G^{\prime}/\gamma],x:\tau_{1}[G^{\prime}/\gamma]\vdash
e^{\prime}:\tau_{2}[G^{\prime}/\gamma]\mid
G^{\prime\prime}[G^{\prime}/\gamma]$. By part 4,
$\Delta;\Psi,u_{f}:\mathcal{U}_{f},u_{t}:\mathcal{U}_{t};\cdot\vdash\tau_{1}[G^{\prime}/\gamma]::\mathsf{Ty}$
and
$\Delta;\Psi,u_{f}:\mathcal{U}_{f},u_{t}:\mathcal{U}_{t};\cdot\vdash\tau_{2}[G^{\prime}/\gamma]::\mathsf{Ty}$.
Apply S:Fun.

     * •

S:Type-Eq. Then $\Delta,\gamma:\kappa_{G};\Omega;\Psi;\Gamma\vdash
e:\tau_{1}\mid G$ and
$\Delta,\gamma:\kappa_{G};\Psi;\cdot\vdash\tau_{1}\equiv\tau::\mathsf{Ty}$. By
induction, $\Delta;\Omega;\Psi;\Gamma[G^{\prime}/\gamma]\vdash
e:\tau_{1}[G^{\prime}/\gamma]\mid G[G^{\prime}/\gamma]$. By part 5,
$\Delta;\Psi;\cdot\vdash\tau_{1}[G^{\prime}/\gamma]\equiv\tau[G^{\prime}/\gamma]::\mathsf{Ty}$.
Apply S:Type-Eq.

     * •

S:App. Then $e={e_{1}[U_{f};U_{t}]}~{}e_{2}$ and
$\tau=\tau_{2}[U_{f}/u_{f}][U_{t}/u_{t}]$ and
$\Omega\rightsquigarrow\Omega_{1}\boxplus\Omega^{\prime}$ and
$\Omega^{\prime}\rightsquigarrow\Omega_{2}\boxplus\Omega_{3}$ and
$G_{1}\mathbin{\oplus}G_{2}\mathbin{\oplus}G_{3}[U_{f};U_{t}]$ and
$\Delta,\gamma:\kappa_{G};\Omega_{1};\Psi;\Gamma\vdash
e_{1}:\Pi[u_{f}\\!:\\!\mathcal{U}_{f};u_{t}\\!:\\!\mathcal{U}_{t}].\tau_{1}\xrightarrow{G_{3}[u_{f};u_{t}]}\tau_{2}\mid
G_{1}$ and $\Delta,\gamma:\kappa_{G};\Omega_{2};\Psi;\Gamma\vdash
e_{2}:\tau_{1}[U_{f}/u_{f}][U_{t}/u_{t}]\mid G_{2}$ and
$\Omega_{3};\cdot\vdash U_{f}:\mathcal{U}_{f}$ and $\cdot;\Psi\vdash
U_{f}:\mathcal{U}_{f}$ and $\cdot;\Psi\vdash U_{t}:\mathcal{U}_{t}$. By
induction, $\Delta;\Omega_{1};\Psi;\Gamma[G^{\prime}/\gamma]\vdash
e_{1}:\Pi[u_{f}\\!:\\!\mathcal{U}_{f};u_{t}\\!:\\!\mathcal{U}_{t}].\tau_{1}[G^{\prime}/\gamma]\xrightarrow{G_{3}[G^{\prime}/\gamma][u_{f};u_{t}]}\tau_{2}[G^{\prime}/\gamma]\mid
G_{1}[G^{\prime}/\gamma]$ and
$\Delta;\Omega_{2};\Psi;\Gamma[G^{\prime}/\gamma]\vdash
e_{2}:\tau_{1}[G^{\prime}/\gamma][U_{f}/u_{f}][U_{t}/u_{t}]\mid
G_{2}[G^{\prime}/\gamma]$.
Apply S:App.

  7. (7)

By induction on the derivation of $\cdot;\Psi,u:\mathcal{U}^{\prime}\vdash
U:\mathcal{U}$.

     * •

U:PsiVar. Then $U=u^{\prime}$ and $\Psi=\Psi^{\prime},u^{\prime}:\mathcal{U}$.
Since $u\neq u^{\prime}$, $u^{\prime}[U^{\prime}/u]=u^{\prime}$. Apply
U:PsiVar.

     * •

U:Pair. Then $U=(U_{1},U_{2})$ and
$\mathcal{U}=\mathcal{U}_{1}^{\blacksquare}\times\mathcal{U}_{2}^{\blacksquare}$
and $\cdot\rightsquigarrow\Omega_{1}\boxplus\Omega_{2}$ and
$\Omega_{1};\Psi,u:\mathcal{U}^{\prime}\vdash U_{1}:\mathcal{U}_{1}$ and
$\Omega_{2};\Psi,u:\mathcal{U}^{\prime}\vdash U_{2}:\mathcal{U}_{2}$. By
inversion on OM:Empty, $\Omega_{1}=\Omega_{2}=\cdot$. By induction,
$\cdot;\Psi\vdash U_{1}[U^{\prime}/u]:\mathcal{U}_{1}$ and $\cdot;\Psi\vdash
U_{2}[U^{\prime}/u]:\mathcal{U}_{2}$. Apply U:Pair.

     * •

U:OnlyLeftPair. Then $U=(U_{1},U_{2})$ and
$\mathcal{U}=\mathcal{U}_{1}^{\blacksquare}\times\mathcal{U}_{2}^{\square}$