system permits manipulation of data preserving their uniqueness. With
recovery/promotion, instead, we can use normal code designed to work on
conventional shared data, and then recover uniqueness.

An alternative approach to modifiers to restrict the usage of references is
that of _ownership_ , based on _enforcing invariants_ rather than deriving
properties. We refer to the recent work of Milano et al. (2022) for an up-to-
date survey. The Rust language, considering its “safe” features (Jung et al.,
2018), belongs to this family as well, and uses ownership for memory
management. In Rust, all references which support mutation are required to be
affine, thus ensuring a unique entry point to a portion of mutable memory.
This relies on a relationship between linearity and uniqueness recently
clarified by Marshall et al. (2022), which proposes a linear calculus with
modalities for non-linearity and uniqueness with a somewhat dual behaviour. In
our approach, instead, the capsule concept models an efficient _ownership
transfer_. In other words, when an object $\mathit{x}$ is “owned” by
$\mathit{y}$, it remains always true that $\mathit{y}$ can only be accessed
through $\mathit{x}$, whereas the capsule notion is dynamic: a capsule can be
“opened”, that is, assigned to a standard reference and modified, since we can
always recover the capsule guarantee.151515Other work in the literature
supports ownership transfer, see, e.g., Müller and Rudich (2007) and Clarke
and Wrigstad (2003), however not of the whole reachable object graph..

We also mention that, whereas in this paper all properties are _deep_ , that
is, inherited by the reachable object graph, most ownership approaches allows
one to distinguish subparts of the reachable object graph that are referred to
but not logically owned. This viewpoint has some advantages, for example Rust
uses ownership to control deallocation without a garbage collector.

##  8\. Conclusion

The main achievement of this paper is to show that sharing and mutation can be
tracked by a coeffect system, thus reconciling two distinct views in the
literature on type systems for mutability control: substructural type systems,
and graph-theoretic properties on heaps. Specifically, the contributions of
the paper are the following:

  * •

a minimal framework formalizing ingredients of coeffect systems

  * •

a coeffect system, for an imperative Java-like calculus, where coeffects
express _links_ among variables and with the final result introduced by the
execution

  * •

an enhanced type system modeling complex features for uniqueness and
immutability.

The enhanced type system (Sect. 5) cleanly integrates and formalizes language
designs by Giannini et al. (2019b) and Giannini et al. (2019a), as detailed
below:

  * •

Giannini et al. (2019b) supports promotion through a very complex type system;
moreover, sharing of two variables/parameters cannot be prevented, as, e.g.,
in the example on page 6.

  * •

Giannini et al. (2019a) has a more refined tracking of sharing allowing us to
express this example, but does not handle immutability.

  * •

In both works, significant properties are expressed and proved with respect to
a non-standard reduction model where memory is encoded in the language itself.

Each of the contributions of the paper opens interesting research directions.
The minimal framework we defined, modeling coeffect contexts as modules,
includes structural coeffect systems, where the coeffect of each variable can
be computed independently (that is, the module operators are defined
pointwise), and coeffect systems such as those in this paper, which can be
considered _quasi-structural_. Indeed, coeffects cannot be computed per-
variable (notably, the sum and multiplication operator of the module are _not_
defined pointwise), but can still be expressed by annotations on single
variables. This also shows a difference with existing graded type systems
explicitly derived from bounded linear logic, which generally consider purely
structural (that is, computable per-variable) grades.161616 This corresponds
to a free module, while the module of sharing coeffects is not free (just a
retraction of a free one).. In future work we plan to develop the metatheory
of the framework, and to investigate its appropriateness both for other quasi-
structural cases, and for coeffects which are truly _flat_ , that is, cannot
be expressed on a per-variable basis. This could be coupled with the design of
a $\lambda$-calculus with a generic module-based coeffect system,
substantially revising (Petricek et al., 2014).

In the type system in Sect. 5, coeffects and modifiers are distinct, yet
interacting, features. We will investigate a framework where modifiers, or,
more generally, _capabilities_ (Haller and Odersky, 2010; Gordon et al., 2012;
Gordon, 2020), are formalized as graded modal types, which are, roughly, types
annotated with coeffects (grades) (Brunel et al., 2014; Orchard et al., 2019;
Dal Lago and Gavazzo, 2022), thus providing a formal foundation for the
“capability” notion in the literature. A related interesting question is which
kinds of modifier/capability can be expressed _purely_ as coeffects. The read-
only property, for instance, could be expressed by enriching the sharing
coeffect with a Read/Write component (Read by default), so that in a field
assignment, variables connected to res in the context of the left-hand
expression are marked as Write.

Concerning the specific type system in Sect. 5, additional features are
necessary to have a more realistic language. Two important examples are:
suitable syntactic sugar for coeffect annotations in method types and
relaxation of coeffects when redefining methods in the presence of
inheritance.

Finally, an interesting objective in the context of Java-like languages is to
allow variables (notably, method parameters) to be annotated by user-defined
coeffects, written by the programmer by extending a predefined abstract class,
in the same way user-defined exceptions extend the Exception predefined class.
This approach would be partly similar to that of Granule (Orchard et al.,
2019), where, however, coeffects cannot be extended by the programmer. A first
step in this direction is presented by Bianchini et al. (2022).

## References

  * (1)
  * Abel and Bernardy (2020) Andreas Abel and Jean-Philippe Bernardy. 2020.  A unified view of modalities in type systems.  _Proceedings of ACM on Programming Languages_ 4, ICFP (2020), 90:1–90:28.  https://doi.org/10.1145/3408972
  * Almeida (1997) Paulo Sérgio Almeida. 1997\.  Balloon Types: Controlling Sharing of State in Data Types. In _European Conference on Object-Oriented Programming, ECOOP 1997_ _(Lecture Notes in Computer Science, Vol. 1241)_. Springer, 32–59.
  * Atkey (2018) Robert Atkey. 2018\.  Syntax and Semantics of Quantitative Type Theory. In _IEEE Symposium on Logic in Computer Science, LICS 2018_ , Anuj Dawar and Erich Grädel (Eds.). ACM Press, 56–65.  https://doi.org/10.1145/3209108.3209189
  * Bianchini et al. (2022) Riccardo Bianchini, Francesco Dagnino, Paola Giannini, and Elena Zucca. 2022.  A Java-like calculus with user-defined coeffects. In _ICTCS’22 - Italian Conf. on Theoretical Computer Science_.  To appear.
  * Boyland (2010) John Boyland. 2010\.  Semantics of Fractional Permissions with Nesting.  _ACM Transactions on Programming Languages and Systems_ 32, 6 (2010).
  * Breuvart and Pagani (2015) Flavien Breuvart and Michele Pagani. 2015.  Modelling Coeffects in the Relational Semantics of Linear Logic. In _24th EACSL Annual Conference on Computer Science Logic, CSL 2015_ _(LIPIcs, Vol. 41)_ , Stephan Kreutzer (Ed.). Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 567–581.  https://doi.org/10.4230/LIPIcs.CSL.2015.567
  * Brunel et al. (2014) Aloïs Brunel, Marco Gaboardi, Damiano Mazza, and Steve Zdancewic. 2014.  A Core Quantitative Coeffect Calculus. In _European Symposium on Programming, ESOP 2013_ _(Lecture Notes in Computer Science, Vol. 8410)_ , Zhong Shao (Ed.). Springer, 351–370.  https://doi.org/10.1007/978-3-642-54833-8_19
  * Castegren and Wrigstad (2016) Elias Castegren and Tobias Wrigstad. 2016.  Reference Capabilities for Concurrency Control. In _European Conference on Object-Oriented Programming, ECOOP 2016_ _(LIPIcs, Vol. 56)_ , Shriram Krishnamurthi and Benjamin S. Lerner (Eds.). Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 5:1–5:26.
  * Choudhury et al. (2021) Pritam Choudhury, Harley Eades III, Richard A. Eisenberg, and Stephanie Weirich. 2021.  A graded dependent type system with a usage-aware semantics.  _Proceedings of ACM on Programming Languages_ 5, POPL (2021), 1–32.  https://doi.org/10.1145/3434331
  * Clarke and Wrigstad (2003) David Clarke and Tobias Wrigstad. 2003.  External Uniqueness is Unique Enough. In _European Conference on Object-Oriented Programming, ECOOP 2003_ _(Lecture Notes in Computer Science, Vol. 2473)_ , Luca Cardelli (Ed.). Springer, 176–200.
  * Clebsch (2017) Sylvan Clebsch. 2017\.  _’Pony’: co-designing a type system and a runtime_.  Ph.D. Dissertation. Imperial College London, UK.  https://ethos.bl.uk/OrderDetails.do?uin=uk.bl.ethos.769552
  * Clebsch et al. (2015) Sylvan Clebsch, Sophia Drossopoulou, Sebastian Blessing, and Andy McNeil. 2015.  Deny capabilities for safe, fast actors. In _International Workshop on Programming Based on Actors, Agents, and Decentralized Control, AGERE! 2015_ , Elisa Gonzalez Boix, Philipp Haller, Alessandro Ricci, and Carlos Varela (Eds.). ACM Press, 1–12.
  * Dal Lago and Gavazzo (2022) Ugo Dal Lago and Francesco Gavazzo. 2022.  A relational theory of effects and coeffects.  _Proceedings of ACM on Programming Languages_ 6, POPL (2022), 1–28.  https://doi.org/10.1145/3498692
  * Dietl et al. (2007) Werner Dietl, Sophia Drossopoulou, and Peter Müller. 2007\.  Generic Universe Types. In _European Conference on Object-Oriented Programming, ECOOP 2007_ _(Lecture Notes in Computer Science, Vol. 4609)_ , Erik Ernst (Ed.). Springer, 28–53.
  * Gaboardi et al. (2016) Marco Gaboardi, Shin-ya Katsumata, Dominic A. Orchard, Flavien Breuvart, and Tarmo Uustalu. 2016\.  Combining effects and coeffects via grading. In _ACM International Conference on Functional Programming, ICFP 2016_ , Jacques Garrigue, Gabriele Keller, and Eijiro Sumii (Eds.). ACM Press, 476–489.  https://doi.org/10.1145/2951913.2951939
  * Ghica and Smith (2014) Dan R. Ghica and Alex I. Smith. 2014.  Bounded Linear Types in a Resource Semiring. In _European Symposium on Programming, ESOP 2013_ _(Lecture Notes in Computer Science, Vol. 8410)_ , Zhong Shao (Ed.). Springer, 331–350.  https://doi.org/10.1007/978-3-642-54833-8_18
  * Giannini et al. (2019a) Paola Giannini, Tim Richter, Marco Servetto, and Elena Zucca. 2019a.  Tracing sharing in an imperative pure calculus.  _Science of Computer Programming_ 172 (2019), 180–202.  https://doi.org/10.1016/j.scico.2018.11.007 Extended version, CoRR, https://arxiv.org/abs/1803.05838.
  * Giannini et al. (2019b) Paola Giannini, Marco Servetto, Elena Zucca, and James Cone. 2019b.  Flexible recovery of uniqueness and immutability.  _Theoretical Computer Science_ 764 (2019), 145–172.  https://doi.org/10.1016/j.tcs.2018.09.001 Extended version, CoRR, https://arxiv.org/abs/1807.00137.
  * Gordon (2020) Colin S. Gordon. 2020\.  Designing with Static Capabilities and Effects: Use, Mention, and Invariants (Pearl). In _European Conference on Object-Oriented Programming, ECOOP 2020_ _(LIPIcs, Vol. 166)_ , Robert Hirschfeld and Tobias Pape (Eds.). Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 10:1–10:25.  https://doi.org/10.4230/LIPIcs.ECOOP.2020.10
  * Gordon et al. (2012) Colin S. Gordon, Matthew J. Parkinson, Jared Parsons, Aleks Bromfield, and Joe Duffy. 2012\.  Uniqueness and reference immutability for safe parallelism. In _ACM Symp. on Object-Oriented Programming: Systems, Languages and Applications 2012_ , Gary T. Leavens and Matthew B. Dwyer (Eds.). ACM Press, 21–40.
  * Haller and Odersky (2010) Philipp Haller and Martin Odersky. 2010.  Capabilities for uniqueness and borrowing. In _European Conference on Object-Oriented Programming, ECOOP 2010_ _(Lecture Notes in Computer Science, Vol. 6183)_ , Theo D’Hondt (Ed.). Springer, 354–378.
  * Hogg (1991) John Hogg. 1991\.  Islands: Aliasing Protection in Object-oriented Languages. In _ACM Symp. on Object-Oriented Programming: Systems, Languages and Applications 1991_ , Andreas Paepcke (Ed.). ACM Press, 271–285.
  * Igarashi et al. (1999) Atsushi Igarashi, Benjamin C. Pierce, and Philip Wadler. 1999\.  Featherweight Java: A Minimal Core Calculus for Java and GJ. In _ACM Symp. on Object-Oriented Programming: Systems, Languages and Applications 1999_. ACM Press, 132–146.  https://doi.org/10.1145/320384.320395
  * Jung et al. (2018) Ralf Jung, Jacques-Henri Jourdan, Robbert Krebbers, and Derek Dreyer. 2018.  RustBelt: securing the foundations of the rust programming language.  _Proceedings of ACM on Programming Languages_ 2, POPL (2018), 66:1–66:34.  https://doi.org/10.1145/3158154
  * Marshall et al. (2022) Daniel Marshall, Michael Vollmer, and Dominic Orchard. 2022\.  Linearity and Uniqueness: An Entente Cordiale. In _European Symposium on Programming, ESOP 2022_ _(Lecture Notes in Computer Science, Vol. 13240)_ , Ilya Sergey (Ed.). Springer, 346–375.  https://doi.org/10.1007/978-3-030-99336-8_13
  * McBride (2016) Conor McBride. 2016\.  I Got Plenty o’ Nuttin’. In _A List of Successes That Can Change the World - Essays Dedicated to Philip Wadler on the Occasion of His 60th Birthday_ _(Lecture Notes in Computer Science, Vol. 9600)_ , Sam Lindley, Conor McBride, Philip W. Trinder, and Donald Sannella (Eds.). Springer, 207–233.  https://doi.org/10.1007/978-3-319-30936-1_12
  * Milano et al. (2022) Mae Milano, Andrew C. Meyers, and Joshua Turcotti. 2022\.  A Flexible Type System for Fearless Concurrency.  To appear.
  * Müller and Rudich (2007) Peter Müller and Arsenii Rudich. 2007.  Ownership transfer in universe types. In _ACM Symp. on Object-Oriented Programming: Systems, Languages and Applications 2007_ , Richard P. Gabriel, David F. Bacon, Cristina Videira Lopes, and Guy L. Steele Jr. (Eds.). ACM Press, 461–478.
  * Orchard et al. (2019) Dominic Orchard, Vilem-Benjamin Liepelt, and Harley Eades III. 2019.  Quantitative program reasoning with graded modal types.  _Proceedings of ACM on Programming Languages_ 3, ICFP (2019), 110:1–110:30.  https://doi.org/10.1145/3341714
  * Petricek et al. (2013) Tomas Petricek, Dominic A. Orchard, and Alan Mycroft. 2013\.  Coeffects: Unified Static Analysis of Context-Dependence. In _Automata, Languages and Programming, ICALP 2013_ _(Lecture Notes in Computer Science, Vol. 7966)_ , Fedor V. Fomin, Rusins Freivalds, Marta Z. Kwiatkowska, and David Peleg (Eds.). Springer, 385–397.  https://doi.org/10.1007/978-3-642-39212-2_35
  * Petricek et al. (2014) Tomas Petricek, Dominic A. Orchard, and Alan Mycroft. 2014\.  Coeffects: a calculus of context-dependent computation. In _ACM International Conference on Functional Programming, ICFP 2014_ , Johan Jeuring and Manuel M. T. Chakravarty (Eds.). ACM Press, 123–135.  https://doi.org/10.1145/2628136.2628160
  * Servetto et al. (2013) Marco Servetto, David J. Pearce, Lindsay Groves, and Alex Potanin. 2013.  Balloon Types for Safe Parallelisation over Arbitrary Object Graphs. In _WODET 2014 - Workshop on Determinism and Correctness in Parallel Programming_.
  * Wood and Atkey (2022) James Wood and Robert Atkey. 2022.  A Framework for Substructural Type Systems. In _European Symposium on Programming, ESOP 2022_ _(Lecture Notes in Computer Science, Vol. 13240)_ , Ilya Sergey (Ed.). Springer, 376–402.  https://doi.org/10.1007/978-3-030-99336-8_14

##  Appendix A Proof of Theorem 4.3

###### Definition A.1.

$\Gamma\blacktriangleleft\Gamma^{\prime}$ if

  1. (1)

$\Gamma^{\prime}={\Gamma}$ or

  2. (2)

$\Gamma^{\prime}=\\{\ell\\}\times\Gamma$ with $\ell$ fresh

###### Lemma A.2.

If ${\cal D}:\Gamma\vdash{\mathit{e}}:\mathit{T}$, then there is a
subderivation ${\cal D}^{\prime}:\Gamma^{\prime}\vdash{\mathit{e}}:\mathit{T}$
of ${\cal D}$ ending with a syntax-directed rule and
$\Gamma^{\prime}\blacktriangleleft\Gamma$

###### Proof.

By induction on ${\cal D}:\Gamma\vdash{\mathit{e}}:\mathit{T}$

:

if ${\cal D}$ ends with a syntax-directed rule then $\Gamma^{\prime}=\Gamma$
and ${\cal D}={\cal D}^{\prime}$. If ${\cal D}$ ends with rule (t-prim) we
have $\Gamma=\\{\ell\\}\times\Delta$ with $\ell$ fresh and so
$\Delta\blacktriangleleft\Gamma$ where $\Delta\vdash{\mathit{e}}:\mathit{T}$.
By induction hypothesis on the premise we have a subderivation ${\cal
D}^{\prime}:\Gamma^{\prime}\vdash{\mathit{e}}:\mathit{T}$ ending with a
syntax-directed rule and $\Gamma^{\prime}\blacktriangleleft\Delta$. We have 2
cases:

  * •:

$\Gamma^{\prime}=\Delta$: by this and by $\Delta\blacktriangleleft\Gamma$ we
obtain $\Gamma^{\prime}\blacktriangleleft\Gamma$, that is, the thesis

  * •:

$\Delta=\\{\ell^{\prime}\\}\times\Gamma^{\prime}$ with $\ell^{\prime}$ fresh:
by this and $\Gamma=\\{\ell\\}\times\Delta$ we obtain
$\Gamma=\\{\ell\\}\times\\{\ell^{\prime}\\}\times\Gamma^{\prime}=\\{\ell^{\prime}\\}\times\Gamma^{\prime}$
so we have $\Gamma^{\prime}\blacktriangleleft\Gamma$ and so the thesis

∎

###### Lemma A.3 (Inversion).

If $\Gamma\vdash\mathit{e}:\mathit{T}$ then exists a context $\Gamma^{\prime}$
such that $\Gamma^{\prime}\blacktriangleleft\Gamma$ and
$\Gamma^{\prime}\vdash\mathit{e}:\mathit{T}$ and the following properties
holds:

  1. (1)

If $\mathit{e}=\mathit{x}$ then
$\Gamma^{\prime}=\emptyset\times\Gamma^{\prime\prime}+\mathit{x}:_{\\{\mathsf{res}\\}}\mathit{T}$

  2. (2)

If $\mathit{e}=\mathit{k}$, then $\mathit{T}=\mathit{P}_{\mathit{k}}$.

  3. (3)

If $\mathit{e}=\mathit{e}\texttt{.}\mathit{f}_{i}$, then
$\Gamma^{\prime}\vdash\mathit{e}:\mathit{C}$ and
$\mathsf{fields}(\mathit{C})=\mathit{T}_{1}\
\mathit{f}_{1}\texttt{;}\ldots\mathit{T}_{n}\ \mathit{f}_{n}\texttt{;}$ and
$\mathit{T}_{i}=\mathit{T}$.

  4. (4)

If
$\mathit{e}=\mathit{e}\texttt{.}\mathit{f}_{i}\texttt{=}\,\mathit{e}^{\prime}$
then $\Gamma_{1}\vdash\mathit{e}:\mathit{C}$ and
$\mathsf{fields}(\mathit{C})=\mathit{T}_{1}\
\mathit{f}_{1}\texttt{;}\ldots\mathit{T}_{n}\ \mathit{f}_{n}\texttt{;}$ and
$\mathit{T}_{i}=\mathit{T}$ and
$\Gamma_{2}\vdash\mathit{e}^{\prime}:\mathit{T}_{i}$ with
$\Gamma^{\prime}=\Gamma_{1}+\Gamma_{2}$.

  5. (5)

If
$\mathit{e}={\texttt{new}\,\mathit{C}(\mathit{e}_{1},\ldots,\mathit{e}_{n})}{\mathit{C}}$,
then we have $\mathsf{fields}(\mathit{C})=\mathit{T}_{1}\
\mathit{f}_{1}\texttt{;}\ldots\mathit{T}_{n}\ \mathit{f}_{n}\texttt{;}$ and
$\Gamma_{i}\vdash\mathit{e}_{i}:\mathit{T}_{i}$ for all $i\in 1..n$ and
$\Gamma=\Gamma_{1}+\ldots+\Gamma_{n}$.

  6. (6)

If
$\mathit{e}=\mathit{e}_{0}.\mathit{m}(\mathit{e}_{1},\ldots,\mathit{e}_{n})$,
then $\Gamma_{0}\vdash\mathit{e}_{0}:\mathit{C}$ and
${\mathsf{mtype}(\mathit{C},\mathit{m})}=\mathit{X}_{\texttt{this}},\mathit{T}_{1}^{\mathit{X}_{1}}\ldots\mathit{T}_{n}^{\mathit{X}_{n}}\rightarrow\mathit{T}$
and $\Gamma_{i}\vdash\mathit{e}_{i}:\mathit{T}_{i}$ for all $i\in 1..n$ and
$\Gamma^{\prime}=(\mathit{X}_{\texttt{this}}\times\Gamma_{0})+(\mathit{X}_{1}\times\Gamma_{1})+\ldots+(\mathit{X}_{n}\times\Gamma_{n})$.

  7. (7)

If
$\mathit{e}=\\{\mathit{T}\,\mathit{x}=\mathit{e}\texttt{;}\,\mathit{e}^{\prime}\\}$
then $\Gamma^{\prime}=(\mathit{X}+\\{\ell\\})\times\Gamma_{1}+\Gamma_{2}$
where $\ell$ is fresh and $\Gamma_{1}\vdash\mathit{e}:\mathit{T}$ and
$\Gamma_{2},\mathit{x}:_{\mathit{X}}\mathit{T}^{\prime}\vdash\mathit{e}^{\prime}:\mathit{T}^{\prime}$.

###### Proof.

  1. (1)

If ${\cal D}:\Gamma\vdash\mathit{x}:\mathit{T}$ then, by Lemma A.2, we know
that exists a derivation ${\cal
D}^{\prime}:\Gamma^{\prime}\vdash{\mathit{x}}:\mathit{T}$ subderivation of
${\cal D}$ ending with a syntax-directed rule and
$\Gamma^{\prime}\blacktriangleleft\Gamma$. Since the last applied rule in
${\cal D}^{\prime}$ must be (t-var), we have
$\Gamma^{\prime}=\emptyset\times\Gamma^{\prime\prime}+\mathit{x}:_{\\{\mathsf{res}\\}}\mathit{T}\mathrel{\hat{\subseteq}}\mathit{x}:_{\\{\mathsf{res}\\}}\mathit{T}$

  2. (2)

If $\Gamma\vdash\mathit{k}:\mathit{T}$ then the last applied rule can be
(t-const) or (t-prim). In both cases we have the thesis

  3. (3)

If ${\cal D}:\Gamma\vdash\mathit{e}\texttt{.}\mathit{f}_{i}:\mathit{T}$ then,
by Lemma A.2, we know that exists a derivation ${\cal
D}^{\prime}:\Gamma^{\prime}\vdash{\mathit{e}\texttt{.}\mathit{f}_{i}}:\mathit{T}$
subderivation of ${\cal D}$ ending with a syntax-directed rule and
$\Gamma^{\prime}\blacktriangleleft\Gamma$. Since the last applied rule in
${\cal D}^{\prime}$ must be (t-access) we have that
$\Gamma^{\prime}\vdash\mathit{e}:\mathit{C}$ with
$\mathsf{fields}(\mathit{C})=\mathit{T}_{1}\
\mathit{f}_{1}\texttt{;}\ldots\mathit{T}_{n}\ \mathit{f}_{n}\texttt{;}$ and
$\mathit{T}_{i}=\mathit{T}$

  4. (4)

If ${\cal
D}:\Gamma\vdash\mathit{e}\texttt{.}\mathit{f}_{i}\texttt{=}\,\mathit{e}^{\prime}:\mathit{T}$
then, by Lemma A.2, we know that exists a derivation ${\cal
D}^{\prime}:\Gamma^{\prime}\vdash{\mathit{e}\texttt{.}\mathit{f}_{i}\texttt{=}\,\mathit{e}^{\prime}}:\mathit{T}$
subderivation of ${\cal D}$ ending with a syntax-directed rule and
$\Gamma^{\prime}\blacktriangleleft\Gamma$. Since the last applied rule in
${\cal D}^{\prime}$ must be (t-assign), we have that
$\Gamma^{\prime}=\Delta_{1}+\Delta_{2}$ such that
$\Delta_{1}\vdash\mathit{e}:\mathit{C}$ and
$\Delta_{2}\vdash\mathit{e}^{\prime}:\mathit{T}_{i}$ with
$\mathsf{fields}(\mathit{C})=\mathit{T}_{1}\
\mathit{f}_{1}\texttt{;}\ldots\mathit{T}_{n}\ \mathit{f}_{n}\texttt{;}$ and
$\mathit{T}_{i}=\mathit{T}$

  5. (5)

If ${\cal
D}:\Gamma\vdash{\texttt{new}\,\mathit{C}(\mathit{e}_{1},\ldots,\mathit{e}_{n})}:\mathit{C}$
then, since the last applied rule in ${\cal D}$ must be (t-new), we have that
$\Gamma=\Delta_{1}+...+\Delta_{n}$ such that
$\mathsf{fields}(\mathit{C})=\mathit{T}_{1}\
\mathit{f}_{1}\texttt{;}\ldots\mathit{T}_{n}\ \mathit{f}_{n}\texttt{;}$ and
$\Delta_{i}\vdash\mathit{e}_{i}:\mathit{T}_{i}$ for all $i\in 1..n$.

  6. (6)

If ${\cal
D}:\Gamma\vdash\mathit{e}_{0}.\mathit{m}(\mathit{e}_{1},\ldots,\mathit{e}_{n}):\mathit{T}$
then, by Lemma A.2, we know that exists a derivation ${\cal
D}^{\prime}:\Gamma^{\prime}\vdash\mathit{e}_{0}.\mathit{m}(\mathit{e}_{1},\ldots,\mathit{e}_{n}):\mathit{T}$
subderivation of ${\cal D}$ ending with a syntax-directed rule and
$\Gamma^{\prime}\blacktriangleleft\Gamma$. Since the last applied rule in
${\cal D}^{\prime}$ must be (t-invk), we have
$\Delta_{0}\vdash\mathit{e}_{0}:\mathit{C}$,
${\mathsf{mtype}(\mathit{C},\mathit{m})}=\mathit{X}_{\texttt{this}},\mathit{T}_{1}^{\mathit{X}_{1}}\ldots\mathit{T}_{n}^{\mathit{X}_{n}}\rightarrow\mathit{T}$
and $\Delta_{i}\vdash\mathit{e}_{i}:\mathit{T}_{i}$ for all $i\in 1..n$ and
$\Gamma^{\prime}=(\mathit{X}_{\texttt{this}}\times\Delta_{0})+(\mathit{X}_{1}\times\Delta_{1})+\ldots+(\mathit{X}_{n}\times\Delta_{n})$.

  7. (7)

If ${\cal
D}:\Gamma\vdash\\{\mathit{T}\,\mathit{x}=\mathit{e}\texttt{;}\,\mathit{e}^{\prime}\\}:\mathit{T}^{\prime}$
then, by Lemma A.2, we know that exists a derivation ${\cal
D}^{\prime}:\Gamma^{\prime}\vdash\\{\mathit{T}\,\mathit{x}=\mathit{e}\texttt{;}\,\mathit{e}^{\prime}\\}:\mathit{T}$
subderivation of ${\cal D}$ ending with a syntax-directed rule and
$\Gamma^{\prime}\blacktriangleleft\Gamma$. Since the last applied rule in
${\cal D}^{\prime}$ must be (t-block), we have
$\Gamma^{\prime}=(\mathit{X}+\\{\ell\\})\times\Delta^{\prime}+\Gamma^{\prime\prime}$
where $\ell$ is fresh $\Delta^{\prime}\vdash\mathit{e}:\mathit{T}$ and
$\Gamma^{\prime\prime},\mathit{x}:_{\mathit{X}}\mathit{T}^{\prime}\vdash\mathit{e}^{\prime}:\mathit{T}^{\prime}$.

∎

###### Lemma A.4.

If $\Gamma$ is a closed context then, for all
$\mathit{x},\mathit{y}\in\mathsf{dom}(\Gamma)$,
$\mathsf{coeff}(\Gamma,\mathit{x})\cap\mathsf{coeff}(\Gamma,\mathit{y})\neq\emptyset$
implies $\mathsf{coeff}(\Gamma,\mathit{x})=\mathsf{coeff}(\Gamma,\mathit{y})$.

###### Proof.

Immediate from the definition of ${\\_}^{\star}$. ∎

###### Lemma A.5.

Let $\Gamma$ be a closed context and
$\Delta=\Gamma,\mathit{x}:_{\mathit{X}}\mathit{T}$. Then, for all
$\mathit{y}\in\mathsf{dom}(\Delta)$, we have

$\mathsf{coeff}({\Delta}^{\star},\mathit{y})=\begin{cases}\bigcup\\{\mathsf{coeff}(\Delta,\mathit{z})\mid\mathsf{coeff}(\Delta,\mathit{z})\cap\mathit{X}\neq\emptyset\\}&\mathsf{coeff}(\Delta,\mathit{y})\cap\mathit{X}\neq\emptyset\\\
\mathsf{coeff}(\Delta,\mathit{y})&\text{otherwise}\end{cases}$

###### Proof.

Suppose
$\Gamma=\mathit{x}_{1}:_{\mathit{X}_{1}}\mathit{T}_{1},\ldots,\mathit{x}_{n}:_{\mathit{X}_{n}}\mathit{T}_{n}$
with $n\geq 0$,
$\mathit{x}:_{\mathit{X}}\mathit{T}=\mathit{x}_{n+1}:_{\mathit{X}_{n+1}}\mathit{T}_{n+1}$
and set
$\Theta=x_{1}:_{\mathit{Y}_{1}}\mathit{T}_{1},\ldots,\mathit{x}_{n+1}:_{\mathit{Y}_{n+1}}\mathit{T}_{n+1}$,
where for all $i\in 1..n+1$, we have

$\mathit{Y}_{i}=\begin{cases}\bigcup\\{\mathit{X}_{j}\mid j\in
1..n+1,\mathit{X}_{j}\cap\mathit{X}_{n+1}\neq\emptyset\\}&\mathit{X}_{i}\cap\mathit{X}_{n+1}\neq\emptyset\\\
\mathit{X}_{i}&\text{otherwise}\end{cases}$

The inequality $\Theta\hat{\subseteq}{\Delta}^{\star}$ is trivial by
definition of ${\\_}^{\star}$. We know that $\Delta\subseteq\Theta$, so to get
the other direction, we just have to show that $\Theta$ is closed. To this
end, let $i\in 1..n+1$, $\ell_{1}\in\mathit{Y}_{i}$ and
$\ell_{1},\ell_{2}\in\mathit{Y}_{j}$ for some $j\in 1..n+1$, then we have to
prove that $\ell_{2}\in\mathit{Y}_{i}$. We distinguish to cases.

  * •

If $\mathit{X}_{j}\cap\mathit{X}_{n+1}=\emptyset$, then
$\mathit{Y}_{j}=\mathit{X}_{j}$. We observe that
$\ell_{1}\notin\mathit{X}_{k}$ for any $k\in 1..n+1$ such that
$\mathit{X}_{k}\cap\mathit{X}_{n+1}\neq\emptyset$. This is obvious for
$k=n+1$, as it is against the assumption
$\mathit{X}_{j}\cap\mathit{X}_{n+1}=\emptyset$. For $k\in 1..n$, since
$\Gamma$ is closed, by Lemma A.4, we would bet
$\mathit{X}_{j}=\mathit{X}_{k}$, and so
$\mathit{X}_{j}\cap\mathit{X}_{n+1}\neq\emptyset$, which is again a
contraddiction. This implies that
$\mathit{X}_{i}\cap\mathit{X}_{n+1}=\emptyset$ and so
$\mathit{Y}_{i}=\mathit{X}_{i}$. Therefore, applying again Lemma A.4, we get
$\mathit{Y}_{i}=\mathit{X}_{i}=\mathit{X}_{j}=\mathit{Y}_{j}$, thus
$\ell_{2}\in\mathit{Y}_{i}$, as needed.

  * •

If $\mathit{X}_{j}\cap\mathit{X}_{n+1}\neq\emptyset$, then we have
$\mathit{Y}_{j}=\bigcup\\{\mathit{X}_{k}\mid k\in
1..n+1,\mathit{X}_{k}\cap\mathit{X}_{n+1}\neq\emptyset\\}$, hence
$\ell_{1}\in\mathit{X}_{h}$ for some $h\in 1..n+1$ such that
$\mathit{X}_{h}\cap\mathit{X}_{n+1}\neq\emptyset$. By a argument similar to
the previous point, we get that
$\mathit{X}_{i}\cap\mathit{X}_{n+1}\neq\emptyset$, hence, by definition,
$\mathit{Y}_{i}=\mathit{Y}_{j}$ that proves the thesis.

∎

###### Lemma A.6.

[Inversion for context] If $\Gamma\vdash{\cal{E}}[\mathit{e}]:\mathit{T}$,
then for some $\Gamma^{\prime},\Delta$,
$\mathit{x}\not\in\mathsf{dom}(\Gamma)$, $\mathit{X}$ and
$\mathit{T}^{\prime}$, $\Gamma=(\mathit{X}\times\Delta)+\Gamma^{\prime}$,
$\Gamma^{\prime}+\mathit{x}:_{\mathit{X}}\mathit{T}^{\prime}\vdash{\cal{E}}[\mathit{x}]:\mathit{T}$
and $\Delta\vdash\mathit{e}:\mathit{T}^{\prime}$.

###### Proof.

The proof is by induction on ${\cal{E}}$. We only show some cases, the others
are analogous.

${\cal{E}}=[\ ]$:

Just take $\Gamma^{\prime}=\emptyset$,
$\mathit{x}\not\in\mathsf{dom}(\Gamma)$, $\mathit{X}=\\{\mathsf{res}\\}$,
$\mathit{T}^{\prime}=\mathit{T}$ and $\Delta=\Gamma$.

${\cal{E}}={\cal{E}}^{\prime}\texttt{.}\mathit{f}\texttt{=}\,\mathit{e}^{\prime}$:

By Lemma A.3(4) we have a context $\Gamma^{\prime}$ such that
$\Gamma^{\prime}\blacktriangleleft\Gamma$,
$\Gamma_{1}+\Gamma_{2}=\Gamma^{\prime}$,
$\Gamma_{1}\vdash{\cal{E}}^{\prime}[\mathit{e}]:\mathit{C}$ and
$\Gamma_{2}\vdash\mathit{e}^{\prime}:\mathit{T}$. By induction hypothesis we
know that for some $\Gamma^{\prime\prime},\Delta$,
$\mathit{x}\not\in\mathsf{dom}(\Gamma)$, $\mathit{X}$ and
$\mathit{T}^{\prime}$,
$\Gamma_{1}=(\mathit{X}\times\Delta)+\Gamma^{\prime\prime}$,
$\Gamma^{\prime\prime}+\mathit{x}:_{\mathit{X}}\mathit{T}^{\prime}\vdash{\cal{E}}^{\prime}[\mathit{x}]:\mathit{C}$
and $\Delta\vdash\mathit{e}:\mathit{T}^{\prime}$. We can assume
$\mathit{x}\notin\mathsf{dom}(\Gamma)$ (doing a step of renaming if needed).
We get
$\Gamma_{1}+\Gamma_{2}=(\mathit{X}\times\Delta)+\Gamma^{\prime\prime}+\Gamma_{2}=\Gamma^{\prime}$
and
$(\Gamma_{2}+\Gamma^{\prime\prime})+\mathit{x}:_{\mathit{X}}\mathit{T}^{\prime}\vdash{\cal{E}}^{\prime}[\mathit{x}]\texttt{.}\mathit{f}\texttt{=}\,\mathit{e}^{\prime}:\mathit{T}$.
We have two cases:

  * •:

$\mathit{T}=\mathit{C}$ We know that the last rule applied to derive
$\Gamma\vdash{\cal{E}}[\mathit{e}]:\mathit{T}$ is (t-assign), so
$\Gamma=\Gamma_{1}+\Gamma_{2}=\Gamma^{\prime}$, so we have the thesis

  * •:

$\mathit{T}=\mathit{P}$ We have two cases. If $\Gamma=\Gamma^{\prime}$ we have
the same situation as above so we have the thesis. If
$\Gamma=\\{\ell\\}\times\Gamma^{\prime}$ then we have
$\Gamma=\\{\ell\\}\times((\mathit{X}\times\Delta)+\Gamma^{\prime\prime}+\Gamma_{2})=((\\{\ell\\}\times\mathit{X})\times\Delta)+\\{\ell\\}\times(\Gamma^{\prime\prime}+\Gamma_{2})$.
We can apply rule (t-prim) to
$(\Gamma_{2}+\Gamma^{\prime\prime})+\mathit{x}:_{\mathit{X}}\mathit{T}^{\prime}\vdash{\cal{E}}^{\prime}[\mathit{x}]\texttt{.}\mathit{f}\texttt{=}\,\mathit{e}^{\prime}:\mathit{T}$
to obtain
$\\{\ell\\}\times((\Gamma_{2}+\Gamma^{\prime\prime})+\mathit{x}:_{\mathit{X}}\mathit{T}^{\prime})\vdash{\cal{E}}^{\prime}[\mathit{x}]\texttt{.}\mathit{f}\texttt{=}\,\mathit{e}^{\prime}:\mathit{T}$.
We know
$\\{\ell\\}\times((\Gamma_{2}+\Gamma^{\prime\prime})+\mathit{x}:_{\mathit{X}}\mathit{T}^{\prime})=\\{\ell\\}\times(\Gamma_{2}+\Gamma^{\prime\prime})+\mathit{x}:_{\\{\ell\\}\times\mathit{X}}\mathit{T}^{\prime}$.

${\cal{E}}=\\{\mathit{T}^{\prime}\,\mathit{x}={\cal{E}}^{\prime}\texttt{;}\,\mathit{e}^{\prime}\\}$:

By Lemma A.3(7) we have a context $\Gamma^{\prime}$ such that
$\Gamma^{\prime}\blacktriangleleft\Gamma$,

$\Gamma^{\prime}=(\mathit{X}+\\{\ell\\})\times\Gamma_{1}+\Gamma_{2}$ where
$\ell$ is fresh and
$\Gamma_{1}\vdash{\cal{E}}^{\prime}[\mathit{e}]:\mathit{T}$ and
$\Gamma_{2},\mathit{x}:_{\mathit{X}}\mathit{T}^{\prime}\vdash\mathit{e}^{\prime}:\mathit{T}^{\prime}$.

By induction hypothesis we know that for some $\Gamma^{\prime\prime},\Delta$,
$\mathit{y}\not\in\mathsf{dom}(\Gamma)$, $\mathit{Y}$ and
$\mathit{T}^{\prime}$,
$\Gamma_{1}=(\mathit{Y}\times\Delta)+\Gamma^{\prime\prime}$,
$\Gamma^{\prime\prime}+\mathit{y}:_{\mathit{Y}}\mathit{T}^{\prime}\vdash{\cal{E}}^{\prime}[\mathit{y}]:\mathit{C}$
and $\Delta\vdash\mathit{e}:\mathit{T}^{\prime}$. We can assume
$\mathit{y}\notin\mathsf{dom}(\Gamma)$ (doing a step of renaming if needed).
We get
$(\mathit{X}+\\{\ell\\})\times\Gamma_{1}+\Gamma_{2}=(\mathit{X}+\\{\ell\\})\times((\mathit{Y}\times\Delta)+\Gamma^{\prime\prime})+\Gamma_{2}=(((\mathit{X}+\\{\ell\\})\times\mathit{Y})\times\Delta)+((\mathit{X}+\\{\ell\\})\times\Gamma^{\prime\prime})+\Gamma_{2}=\Gamma^{\prime}$.
By rule (t-block) we have
$((\mathit{X}+\\{\ell\\})\times\Gamma^{\prime\prime})+\Gamma_{2}+\mathit{y}:_{((\mathit{X}+\\{\ell\\})\times\mathit{Y})}\mathit{T}^{\prime}\vdash{\cal{E}}[\mathit{y}]:\mathit{T}$.
We have two cases:

  * •:

$\mathit{T}=\mathit{C}$ We know that the last rule applied to derive
$\Gamma\vdash{\cal{E}}[\mathit{e}]:\mathit{T}$ is (t-block), so
$\Gamma=(\mathit{X}+\\{\ell\\})\times\Gamma_{1}+\Gamma_{2}=\Gamma^{\prime}$,
so we have the thesis

  * •:

$\mathit{T}=\mathit{P}$ We have two cases. If $\Gamma=\Gamma^{\prime}$ we have
the same situation as above so we have the thesis. If
$\Gamma=\\{\ell^{\prime}\\}\times\Gamma^{\prime}$ then we have
$\Gamma=\\{\ell^{\prime}\\}\times((\mathit{X}+\\{\ell\\})\times\Gamma_{1}+\Gamma_{2})=(\\{\ell^{\prime}\\}\times(\mathit{X}+\\{\ell\\})\times\Gamma_{1})+\\{\ell^{\prime}\\}\times\Gamma_{2}=(((\\{\ell^{\prime}\\}\times(\mathit{X}+\\{\ell\\})\times\mathit{Y})\times\Delta)+((\\{\ell^{\prime}\\}\times(\mathit{X}+\\{\ell\\})\times\Gamma^{\prime\prime})+\\{\ell^{\prime}\\}\times\Gamma_{2}$.
We can apply rule (t-prim) to
$((\mathit{X}+\\{\ell\\})\times\Gamma^{\prime\prime})+\Gamma_{2}+\mathit{y}:_{((\mathit{X}+\\{\ell\\})\times\mathit{Y})}\mathit{T}^{\prime}\vdash{\cal{E}}[\mathit{y}]:\mathit{T}$
to obtain
$\\{\ell^{\prime}\\}\times(((\mathit{X}+\\{\ell\\})\times\Gamma^{\prime\prime})+\Gamma_{2}+\mathit{y}:_{((\mathit{X}+\\{\ell\\})\times\mathit{Y})}\mathit{T}^{\prime})\vdash{\cal{E}}[\mathit{y}]:\mathit{T}$.
We know
$\\{\ell^{\prime}\\}\times(((\mathit{X}+\\{\ell\\})\times\Gamma^{\prime\prime})+\Gamma_{2}+\mathit{y}:_{((\mathit{X}+\\{\ell\\})\times\mathit{Y})}\mathit{T}^{\prime})=(\\{\ell^{\prime}\\}\times(\mathit{X}+\\{\ell\\})\times\Gamma^{\prime\prime})+\\{\ell^{\prime}\\}\times\Gamma_{2}+\mathit{y}:_{(\\{\ell^{\prime}\\}\times(\mathit{X}+\\{\ell\\})\times\mathit{Y})}\mathit{T}^{\prime}$
By
$(\\{\ell^{\prime}\\}\times(\mathit{X}+\\{\ell\\})\times\Gamma^{\prime\prime})+\\{\ell^{\prime}\\}\times\Gamma_{2}+\mathit{y}:_{(\\{\ell^{\prime}\\}\times(\mathit{X}+\\{\ell\\})\times\mathit{Y})}\mathit{T}^{\prime}\vdash{\cal{E}}[\mathit{y}]:\mathit{T}$
we obtain the thesis.

∎

###### Lemma A.7.

If $\Delta\vdash\mathit{e}:\mathit{T}$ and
$\Gamma+\mathit{x}:_{\mathit{X}}\mathit{T}\vdash{\cal{E}}[\mathit{x}]:\mathit{T}^{\prime}$,
with $\mathit{x}\notin\mathsf{dom}(\Gamma)$, then
$\Gamma+\mathit{X}\times\Delta\vdash{\cal{E}}[\mathit{e}]:\mathit{T}^{\prime}$.

###### Proof.

By induction on the derivation of
$\Gamma+\mathit{x}:_{\mathit{X}}\mathit{T}\vdash{\cal{E}}[\mathit{x}]:\mathit{T}^{\prime}$.
∎

###### Lemma A.8.

Let $\Gamma$ a closed context and
$\Delta=\sum_{\mathit{x}\in\mathsf{dom}(\Delta)}\mathit{x}:_{\mathit{X}}\mathit{T}_{\mathit{x}}$
and such that $\mathsf{dom}(\Delta)\subseteq\mathsf{dom}(\Gamma)$ and
$\mathsf{links}(\Gamma)\cap\mathsf{links}(\Delta)=\\{\mathsf{res}\\}$. We have
2 cases:

  * •

$\mathsf{res}\notin\mathit{X}$
For all $\mathit{y}\in\mathsf{dom}(\Gamma)$, if exists
$\mathit{x}\in\mathsf{dom}(\Delta)$ such that
$\mathsf{coeff}(\Gamma,\mathit{y})\cap\mathsf{coeff}(\Gamma,\mathit{x})\neq\emptyset$
then
$\mathsf{coeff}(\Gamma+\Delta,\mathit{y})=\mathit{X}+\sum_{\mathit{x}\in\Delta}\mathsf{coeff}(\Gamma,\mathit{x})$,
otherwise
$\mathsf{coeff}(\Gamma+\Delta,\mathit{y})=\mathsf{coeff}(\Gamma,\mathit{y})$.

  * •

$\mathsf{res}\in\mathit{X}$
We define $\mathit{Y}=\mathsf{coeff}(\Gamma,\mathit{z})$ if
$\mathsf{res}\in\mathsf{coeff}(\Gamma,\mathit{z})$ and
$\mathit{z}\in\mathsf{dom}(\Gamma)$. For all
$\mathit{y}\in\mathsf{dom}(\Gamma)$, if exists
$\mathit{x}\in\mathsf{dom}(\Delta)$ such that
$\mathsf{coeff}(\Gamma,\mathit{y})\cap\mathsf{coeff}(\Gamma,\mathit{x})\neq\emptyset$
or $\mathsf{res}\in\mathsf{coeff}(\Gamma,\mathit{y})$ then
$\mathsf{coeff}(\Gamma+\Delta,\mathit{y})=\mathit{X}+\sum_{\mathit{x}\in\Delta}\mathsf{coeff}(\Gamma,\mathit{x})+\mathit{Y}$,
otherwise
$\mathsf{coeff}(\Gamma+\Delta,\mathit{y})=\mathsf{coeff}(\Gamma,\mathit{y})$.

###### Proof.

∎

###### Lemma A.9.

Let $\Gamma{\upharpoonright}\Delta=\Delta$.

  1. (1)

$(\mathit{X}\times\Gamma){\upharpoonright}(\mathit{X}\times\Delta)=\mathit{X}\times\Delta$

  2. (2)

If
$\mathsf{links}(\Theta)\cap(\mathsf{links}(\Delta)\cup\mathsf{links}(\Gamma))=\\{\mathsf{res}\\}$
or
$\mathsf{links}(\Theta)\cap(\mathsf{links}(\Delta)\cup\mathsf{links}(\Gamma))=\\{\mathsf{res}\\}\cup\mathit{X}$
where exists $\mathit{x}\in\mathsf{dom}(\Delta)$ such that
$\mathsf{coeff}(\Delta,\mathit{x})=\mathit{X}$ and
$\mathsf{dom}(\Theta)\subseteq\mathsf{dom}(\Delta)$, then
$(\Gamma+\Theta){\upharpoonright}(\Delta+\Theta)=\Delta+\Theta$.

###### Proof.

  1. (1)

Let $\mathit{x}\in\mathsf{dom}(\Delta)$ and
$\mathsf{coeff}(\Gamma,\mathit{x})=\mathit{X}_{\Gamma}$ and
$\mathsf{coeff}(\Delta,\mathit{x})=\mathit{X}_{\Delta}$. By definition of
$\Gamma{\upharpoonright}\Delta$ and $\Gamma{\upharpoonright}\Delta=\Delta$, we
have that $\mathit{X}_{\Gamma}\cap\mathsf{links}(\Delta)=\mathit{X}_{\Delta}$.
Let $\mathit{Y}$ be such that
$\mathsf{coeff}(\mathit{X}\times\Gamma,\mathit{x})=\mathit{Y}$, then
$\mathit{Y}=\mathit{X}\triangleleft\mathit{X}_{\Gamma}$. We want to prove that
$\mathit{Y}\cap\mathsf{links}(\mathit{X}\triangleleft{\Delta})=\mathit{X}\triangleleft\mathit{X}_{\Delta}$.
Consider two cases: $\mathsf{res}\not\in\mathit{X}_{\Gamma}$ and
$\mathsf{res}\in\mathit{X}_{\Gamma}$.
In the first case $\mathit{Y}=\mathit{X}_{\Gamma}$ and
$\mathit{Y}\cap(\mathsf{links}(\mathit{X}\triangleleft{\Delta}))=\mathit{Y}\cap\mathsf{links}(\Delta)=\mathit{X}_{\Delta}$.
Moreover, since $\mathsf{res}\not\in\mathit{X}_{\Delta}$ we have
$\mathit{X}\triangleleft\mathit{X}_{\Delta}=\mathit{X}_{\Delta}$. Therefore,
$\mathit{Y}\cap(\mathsf{links}(\mathit{X}\triangleleft{\Delta}))=\mathit{X}\triangleleft\mathit{X}_{\Delta}$.
In the second case
$\mathit{Y}=\mathit{X}\cup(\mathit{X}_{\Gamma}-\\{\mathsf{res}\\})$ and since
$\mathsf{res}\in\mathit{X}_{\Delta}$ we have
$\mathit{X}\triangleleft\mathit{X}_{\Delta}=\mathit{X}\cup(\mathit{X}_{\Delta}-\\{\mathsf{res}\\})$.
From $\mathit{X}_{\Gamma}\cap\mathsf{links}(\Delta)=\mathit{X}_{\Delta}$ we
get
$(\mathit{X}_{\Gamma}-\\{\mathsf{res}\\})\cap\mathsf{links}(\Delta)=\mathit{X}_{\Delta}-\\{\mathsf{res}\\}$.
Note that
$\mathit{X}\subseteq\mathsf{links}(\mathit{X}\triangleleft{\Delta})$.
Therefore
$\mathit{Y}\cap(\mathsf{links}(\mathit{X}\triangleleft{\Delta}))=\mathit{X}\cup(\mathit{X}_{\Delta}-\\{\mathsf{res}\\})$
which proves the result.

  2. (2)

We know $\Theta=\hat{\cup}_{i=0}^{n}\Theta_{i}$, where for all $i\in[1...n]$,
in $\Theta_{i}$ all variables have the same coeffect $\mathit{X}_{i}$ and, for
all $j,k\in[1...n]$ and $j\neq k$,
$\mathsf{links}(\Theta_{j})\cap\mathsf{links}(\Theta_{k})=\\{\mathsf{res}\\}$.
To obtain the thesis therefore we just need to prove that the property holds
summing one $\Theta_{i}$ at a time, since $\Gamma+\Theta$ and $\Delta+\Theta$
can be obtained summing iteratively the $\Theta_{i}$s. It suffices to prove
the thesis only for the first sum. By $\Gamma{\upharpoonright}\Delta=\Delta$
we have that for all $\mathit{x}\in\mathsf{dom}(\Delta)$,
$\mathsf{coeff}(\Gamma,\mathit{x})=\mathit{Z}\cup\mathsf{coeff}(\Delta,\mathit{x})$,
where $\mathit{Z}\cap\mathsf{links}(\Delta)=\emptyset$. By Lemma A.8 we have
two cases for $\Gamma+\Theta_{i}$ and $\Delta+\Theta_{i}$:

     * •

$\mathsf{res}\notin\mathit{X}_{i}$
For all $\mathit{y}\in\mathsf{dom}(\Gamma)$, if exists
$\mathit{x}\in\mathsf{dom}(\Theta_{i})$ such that
$\mathsf{coeff}(\Gamma,\mathit{y})\cap\mathsf{coeff}(\Gamma,\mathit{x})\neq\emptyset$
then
$\mathsf{coeff}(\Gamma+\Theta_{i},\mathit{y})=\mathit{X}+\sum_{\mathit{x}\in\Theta_{i}}\mathsf{coeff}(\Gamma,\mathit{x})=\mathit{X}+\sum_{\mathit{x}\in\Theta_{i}}(\mathsf{coeff}(\Delta,\mathit{x})\cup\mathit{Z}_{\mathit{x}})$,
otherwise
$\mathsf{coeff}(\Gamma+\Theta_{i},\mathit{y})=\mathsf{coeff}(\Gamma,\mathit{y})=\mathit{Z}_{\mathit{y}}\cup\mathsf{coeff}(\Delta,\mathit{y})$.
For all $\mathit{y}\in\mathsf{dom}(\Delta)$, if exists
$\mathit{x}\in\mathsf{dom}(\Theta_{i})$ such that
$\mathsf{coeff}(\Delta,\mathit{y})\cap\mathsf{coeff}(\Delta,\mathit{x})\neq\emptyset$
then
$\mathsf{coeff}(\Delta+\Theta_{i},\mathit{y})=\mathit{X}+\sum_{\mathit{x}\in\Theta_{i}}\mathsf{coeff}(\Delta,\mathit{x})$,
otherwise
$\mathsf{coeff}(\Delta+\Theta_{i},\mathit{y})=\mathsf{coeff}(\Delta,\mathit{y})$.
By $\Gamma{\upharpoonright}\Delta=\Delta$ we have that, for all
$\mathit{x},\mathit{y}\in\mathsf{dom}(\Delta)$,
$\mathsf{coeff}(\Gamma,\mathit{x})\cap\mathsf{coeff}(\Gamma,\mathit{y})\neq\emptyset$
if and only if
$\mathsf{coeff}(\Delta,\mathit{x})\cap\mathsf{coeff}(\Delta,\mathit{y})\neq\emptyset$.
By these considerations we derive that, for all
$\mathit{x}\in\mathsf{dom}(\Gamma)$,
$\mathsf{coeff}(\Gamma+\Theta_{i},\mathit{x})\cap\mathsf{links}(\Delta+\Theta_{i})=\mathsf{coeff}(\Delta+\Theta_{i},$),
that is,
$\Gamma+\Theta_{i}{\upharpoonright}\Delta+\Theta_{i}=\Delta+\Theta_{i}$.

     * •

$\mathsf{res}\in\mathit{X}_{i}$
We define $\mathit{Y}=\mathsf{coeff}(\Gamma,\mathit{z})$ if
$\mathsf{res}\in\mathsf{coeff}(\Gamma,\mathit{z})$ and
$\mathit{z}\in\mathsf{dom}(\Gamma)$. For all
$\mathit{y}\in\mathsf{dom}(\Gamma)$, if exists
$\mathit{x}\in\mathsf{dom}(\Theta_{i})$ such that
$\mathsf{coeff}(\Gamma,\mathit{y})\cap\mathsf{coeff}(\Gamma,\mathit{x})\neq\emptyset$
or $\mathsf{res}\in\mathsf{coeff}(\Gamma,\mathit{y})$ then
$\mathsf{coeff}(\Gamma+\Theta_{i},\mathit{y})=\mathit{X}\cup\sum_{\mathit{x}\in\Theta_{i}}\mathsf{coeff}(\Gamma,\mathit{x})\cup\mathit{Y}=\mathit{X}\cup\sum_{\mathit{x}\in\Theta_{i}}(\mathsf{coeff}(\Delta,\mathit{x})\cup\mathit{Z}_{\mathit{x}})\cup\mathit{Y}$,
otherwise
$\mathsf{coeff}(\Gamma+\Theta_{i},\mathit{y})=\mathsf{coeff}(\Gamma,\mathit{y})=\mathit{Z}_{\mathit{y}}\cup\mathsf{coeff}(\Delta,\mathit{y})$.
We define $\mathit{Y}=\mathsf{coeff}(\Delta,\mathit{z})$ if
$\mathsf{res}\in\mathsf{coeff}(\Delta,\mathit{z})$ and
$\mathit{z}\in\mathsf{dom}(\Delta)$. For all
$\mathit{y}\in\mathsf{dom}(\Delta)$, if exists
$\mathit{x}\in\mathsf{dom}(\Theta_{i})$ such that
$\mathsf{coeff}(\Delta,\mathit{y})\cap\mathsf{coeff}(\Delta,\mathit{x})\neq\emptyset$
or $\mathsf{res}\in\mathsf{coeff}(\Theta_{i},\mathit{y})$ then
$\mathsf{coeff}(\Delta+\Theta_{i},\mathit{y})=\mathit{X}+\sum_{\mathit{x}\in\Theta_{i}}\mathsf{coeff}(\Delta,\mathit{x})+\mathit{Y}$,
otherwise
$\mathsf{coeff}(\Gamma+\Theta_{i},\mathit{y})=\mathsf{coeff}(\Gamma,\mathit{y})$.
By $\Gamma{\upharpoonright}\Delta=\Delta$ we have that, for all
$\mathit{x},\mathit{y}\in\mathsf{dom}(\Delta)$,
$\mathsf{coeff}(\Gamma,\mathit{x})\cap\mathsf{coeff}(\Gamma,\mathit{y})\neq\emptyset$
if and only if
$\mathsf{coeff}(\Delta,\mathit{x})\cap\mathsf{coeff}(\Delta,\mathit{y})\neq\emptyset$.
By these considerations we derive that, for all
$\mathit{x}\in\mathsf{dom}(\Gamma)$,
$\mathsf{coeff}(\Gamma+\Theta_{i},\mathit{x})\cap\mathsf{links}(\Delta+\Theta_{i})=\mathsf{coeff}(\Delta+\Theta_{i},$),
that is,
$\Gamma+\Theta_{i}{\upharpoonright}\Delta+\Theta_{i}=\Delta+\Theta_{i}$.

∎

###### Lemma A.10 (Substitution).

If $\Delta\vdash\mathit{e}^{\prime}:\mathit{T}^{\prime}$ and
$\Gamma,\mathit{x}:_{\mathit{X}}\mathit{T}^{\prime}\vdash\mathit{e}:\mathit{T}$
and $\Delta^{\prime}$ is $\Delta$ with fresh renamed links, then
$\Gamma^{\prime}\vdash\mathit{e}[\mathit{e}^{\prime}/\mathit{x}]:\mathit{T}$
with $\Gamma^{\prime}$ such that
$\Gamma^{\prime}\mathrel{\hat{\subseteq}}\mathit{X}\mathrel{\triangleleft}\Delta^{\prime}+\Gamma$.

###### Proof.

By induction on the derivation of
$\Gamma,\mathit{x}:_{\mathit{X}}\mathit{T}^{\prime}\vdash\mathit{e}:\mathit{T}$

(t-var):

We know that $\Gamma=\emptyset$ and $\mathit{X}=\\{\mathsf{res}\\}$, hence the
thesis follows from the hypothesis
$\Delta\vdash\mathit{e}^{\prime}:\mathit{T}^{\prime}$, as
$\emptyset+\\{\mathsf{res}\\}\times\Delta=\Delta$ and
$\mathit{x}[\mathit{e}^{\prime}/\mathit{x}]=\mathit{e}^{\prime}$.

(t-invk):

We know that
$\mathit{e}=\mathit{e}_{0}.\mathit{m}(\mathit{e}_{1},\ldots,\mathit{e}_{n})$,
$\Gamma\mathrel{\hat{\subseteq}}+_{0\leq i\leq
n}\mathit{X}_{i}\times\Gamma_{i}$ and $\mathit{X}\supseteq\cup_{0\leq i\leq
n}\mathit{X}_{i}\triangleleft\mathit{X}_{i}^{\prime}$, where
$\Gamma_{i},\mathit{x}:_{\mathit{X}_{i}^{\prime}}\mathit{T}^{\prime}\vdash\mathit{e}_{i}:\mathit{C}_{i}$
($0\leq i\leq n$) and
${\mathsf{mtype}(\mathit{C}_{0},\mathit{m})}=\mathit{X}_{0},\mathit{T}_{1}^{\mathit{X}_{1}}\ldots\mathit{T}_{n}^{\mathit{X}_{n}}\rightarrow\mathit{T}$.
By induction hypothesis we obtain
$\Gamma_{i}+(\mathit{X}_{i}^{\prime}\times\Delta^{\prime})\vdash\mathit{e}_{i}[\mathit{e}/\mathit{x}]:\mathit{T}_{i}$
($0\leq i\leq n$). Applying rule (t-invk) we obtain

$+_{0\leq i\leq
n}\mathit{X}_{i}\times(\Gamma_{i}+\mathit{X}^{\prime}_{i}\times\Delta^{\prime})\vdash\mathit{e}_{0}.\mathit{m}(\mathit{e}_{1},\ldots,\mathit{e}_{n})[\mathit{e}/\mathit{x}]:\mathit{T}$

Moreover, $+_{0\leq i\leq
n}\mathit{X}_{i}\times(\Gamma_{i}+\mathit{X}^{\prime}_{i}\times\Delta^{\prime})=+_{0\leq
i\leq
n}(\mathit{X}_{i}\times\Gamma_{i})+(\mathit{X}_{i}\triangleleft\mathit{X}_{i}^{\prime})\times\Delta^{\prime}$
and
$+_{0\leq i\leq
n}(\mathit{X}_{i}\triangleleft\mathit{X}_{i}^{\prime})\times\Delta^{\prime}=(\cup_{0\leq
i\leq
n}\mathit{X}_{i}\triangleleft\mathit{X}_{i}^{\prime})\times\Delta^{\prime}$.

We want to show that $+_{0\leq i\leq
n}(\mathit{X}_{i}\times\Gamma_{i})+(\cup_{0\leq i\leq
n}\mathit{X}_{i}\triangleleft\mathit{X}_{i}^{\prime}\times\Delta^{\prime})\mathrel{\hat{\subseteq}}\mathit{X}\mathrel{\triangleleft}\Delta^{\prime}+\Gamma$.
Knowing that $\Gamma\mathrel{\hat{\subseteq}}+_{0\leq i\leq
n}\mathit{X}_{i}\times\Gamma_{i}$ and $\mathit{X}\supseteq\cup_{0\leq i\leq
n}\mathit{X}_{i}\triangleleft\mathit{X}_{i}^{\prime}$ we derive $+_{0\leq
i\leq n}(\mathit{X}_{i}\times\Gamma_{i})+(\cup_{0\leq i\leq
n}\mathit{X}_{i}\triangleleft\mathit{X}_{i}^{\prime}\times\Delta^{\prime})\mathrel{\hat{\subseteq}}\mathit{X}\mathrel{\triangleleft}\Delta^{\prime}+\Gamma$.

(t-new):

We know that
$\mathit{e}=\texttt{new}\;\mathit{C}\texttt{(}\mathit{e}_{1},\ldots,\mathit{e}_{n}\texttt{)}$,
$\Gamma\mathrel{\hat{\subseteq}}+_{1\leq i\leq n}\Gamma_{i}$ and
$\mathit{X}\supseteq\cup_{1\leq i\leq n}\mathit{X}_{i}$ and
$\Gamma_{i},\mathit{x}:_{\mathit{X}_{i}}\mathit{T}^{\prime}\vdash\mathit{e}_{i}:\mathit{T}_{i}$
($1\leq i\leq n$). By inductive hypothesis
$\Gamma_{i}+(\mathit{X}_{i}\times\Delta^{\prime})\vdash\mathit{e}_{i}[\mathit{e}^{\prime}/\mathit{x}]:\mathit{T}_{i}$,
($1\leq i\leq n$). Applying rule (t-new) we obtain $+_{1\leq i\leq
n}\Gamma_{i}+(\mathit{X}_{i}\times\Delta^{\prime})\vdash\texttt{new}\;\mathit{C}\texttt{(}\mathit{e}_{1},\ldots,\mathit{e}_{n}\texttt{)}[\mathit{e}^{\prime}/\mathit{x}]:\mathit{T}_{1}$.

We know $+_{1\leq i\leq
n}\Gamma_{i}+(\mathit{X}_{i}\times\Delta^{\prime})=+_{1\leq i\leq
n}\Gamma_{i}++_{1\leq i\leq n}(\mathit{X}_{i}\times\Delta^{\prime})=+_{1\leq
i\leq n}\Gamma_{i}+(\cup_{1\leq i\leq n}\mathit{X}_{i}\times\Delta^{\prime})$.

We want to show that $+_{1\leq i\leq n}\Gamma_{i}+(\cup_{1\leq i\leq
n}\mathit{X}_{i}\times\Delta^{\prime})\mathrel{\hat{\subseteq}}\mathit{X}\mathrel{\triangleleft}\Delta^{\prime}+\Gamma$.
By $\mathit{X}\supseteq\cup_{1\leq i\leq n}\mathit{X}_{i}$ and
$\Gamma\mathrel{\hat{\subseteq}}+_{1\leq i\leq n}\Gamma_{i}$ we derive
$\mathit{X}\mathrel{\triangleleft}\Delta^{\prime}+\Gamma\mathrel{\hat{\subseteq}}+_{1\leq
i\leq n}\Gamma_{i}+(\cup_{1\leq i\leq n}\mathit{X}_{i}\times\Delta^{\prime})$.

(t-block):

By assumptions we know that
$\mathit{e}={\\{\mathit{T}\,\mathit{x}=\mathit{e}_{1}\texttt{;}\,\mathit{e}_{2}\\}}$,
$\Gamma_{1},\mathit{x}:_{\mathit{X}_{1}}\mathit{T}^{\prime}\vdash\mathit{e}_{1}:\mathit{T}^{\prime\prime}$
and
$\Gamma_{2},\mathit{x}:_{\mathit{X}_{2}}\mathit{T}^{\prime},\mathit{y}:_{\mathit{Y}}\mathit{T}^{\prime\prime}\vdash\mathit{e}_{2}:\mathit{T}$
and

$\Gamma,\mathit{x}:_{\mathit{X}}\mathit{T}^{\prime}=(\mathit{Y}\cup\\{\ell\\})\times(\Gamma_{1},\mathit{x}:_{\mathit{X}_{1}}\mathit{T}^{\prime})+(\Gamma_{2},\mathit{x}:_{\mathit{X}_{2}}\mathit{T}^{\prime})$

where $\ell$ is fresh. Then, in particular, we have
$\Gamma\mathrel{\hat{\subseteq}}(\mathit{Y}\cup\\{\ell\\})\times\Gamma_{1}+\Gamma_{2}$
and
$\mathit{X}\supseteq(\mathit{Y}\cup\\{\ell\\})\triangleleft\mathit{X}_{1}\cup\mathit{X}_{2}$.
We want to prove that
$\Gamma^{\prime}\vdash\\{\mathit{T}\,\mathit{x}=\mathit{e}_{1}\texttt{;}\,\mathit{e}_{2}\\}[\mathit{e}^{\prime}/\mathit{x}]:\mathit{T}$
where

$\Gamma^{\prime}=((\mathit{Y}\cup\\{\ell\\})\triangleleft\mathit{X}_{1}\cup\mathit{X}_{2})\times\Delta^{\prime}+(\mathit{Y}\cup\\{\ell\\})\times\Gamma_{1}+\Gamma_{2}$

then the thesis will follow by subsumption. By induction hypothesis, we get
$\Gamma_{1}+\mathit{X}_{1}\times\Delta^{\prime}\vdash\mathit{e}_{1}[\mathit{e}^{\prime}/\mathit{x}]:\mathit{T}^{\prime\prime}$
and
$(\Gamma_{2},\mathit{y}:_{\mathit{Y}}\mathit{T}^{\prime\prime})+\mathit{X}_{2}\times\Delta^{\prime}\vdash\mathit{e}_{2}[\mathit{e}^{\prime}/\mathit{x}]:\mathit{T}$.
By definition of $+$ we have
$(\Gamma_{2},\mathit{y}:_{\mathit{Y}}\mathit{T}^{\prime\prime})+\mathit{X}_{2}\times\Delta^{\prime}={(\Gamma_{2}+\mathit{X}_{2}\times\Delta^{\prime},\mathit{y}:_{\mathit{Y}}\mathit{T}^{\prime\prime})}^{\star}=\Theta,\mathit{y}:_{\mathit{Y}^{\prime}}\mathit{T}^{\prime\prime}$
for some $\Theta$ and $\mathit{Y}^{\prime}$. By Lemma A.5 we know that
$\mathit{Y}^{\prime}$ is the union of all coeffects in
$\Gamma_{2}+\mathit{X}_{2}\times\Delta^{\prime}$ that are not disjoint from
$\mathit{Y}$.

Then, applying rule (t-block), we derive
$\Gamma^{\prime\prime}\vdash\\{\mathit{T}^{\prime\prime}\,\mathit{y}=\mathit{e}_{1}\texttt{;}\,\mathit{e}_{2}\\}[\mathit{e}/\mathit{x}]:\mathit{T}$
with

$\Gamma^{\prime\prime}={(\mathit{Y}^{\prime}\cup\\{\ell\\})\times(\Gamma_{1}+\mathit{X}_{1}\times\Delta^{\prime})+\Gamma_{2}+\mathit{X}_{2}\times\Delta^{\prime}}$

Since $\mathit{Y}\subseteq\mathit{Y}^{\prime}$, we have

$\Gamma^{\prime\prime}=\mathit{Y}^{\prime}\times(\Gamma_{1}+\mathit{X}_{1}\times\Delta^{\prime})+(\mathit{Y}\cup\\{\ell\\})\times(\Gamma_{1}+\mathit{X}_{1}\times\Delta^{\prime})+\Gamma_{2}+\mathit{X}_{2}\times\Delta^{\prime}$

Since the links in $\Delta^{\prime}$ are fresh, we have that
$\mathit{X}_{2}\times\Delta^{\prime}=\mathit{X}_{2}\triangleleft\Delta^{\prime}$,
that is,
$\mathit{X}_{2}\cap\mathsf{links}(\Delta^{\prime})\subseteq\\{\mathsf{res}\\}$
so $\mathit{X}_{2}\times\Delta^{\prime}$ is equal to $\Delta^{\prime}$ except
that in coeffects $\mathsf{res}$ is replaced with links in $\mathit{X}_{2}$.
Moreover, by Lemma A.4 $\mathit{X}_{2}=\mathit{Y}$ or
$\mathit{X}_{2}\cap\mathit{Y}=\emptyset$. Therefore, for all
$\mathit{z}\in\mathsf{dom}(\mathit{X}_{2}\times\Delta^{\prime})$, either
$\mathit{Y}\subseteq\mathsf{coeff}(\mathit{X}_{2}\times\Delta^{\prime},\mathit{z})$
or
$\mathit{Y}\cap\mathsf{coeff}(\mathit{X}_{2}\times\Delta^{\prime},\mathit{z})=\emptyset$.
Applying Lemma A.5 we get
$\Theta=\Gamma_{2}+\mathit{X}_{2}\times\Delta^{\prime}$ and
$\mathit{Y}^{\prime}=\mathsf{coeff}(\Theta,\mathit{z})$ if
$\mathit{Y}\subseteq\mathsf{coeff}(\Theta,\mathit{z})$ for all
$\mathit{z}\in\mathsf{dom}(\Theta)$. For all
$\mathit{z}\in\mathsf{dom}(\Gamma_{1}+\mathit{X}_{1}\times\Delta^{\prime})$
such that
$\mathsf{res}\in\mathsf{coeff}(\Gamma_{1}+\mathit{X}_{1}\times\Delta^{\prime},\mathit{z})$,
we have that
$\mathit{Y}\subseteq\mathsf{coeff}((\mathit{Y}\cup\\{\ell\\})\times(\Gamma_{1}+\mathit{X}_{1}\times\Delta^{\prime}),\mathit{z})$.
Since
$(\mathit{Y}\cup\\{\ell\\})\times(\Gamma_{1}+\mathit{X}_{1}\times\Delta^{\prime})+\Gamma_{2}+\mathit{X}_{2}\times\Delta^{\prime}$
is closed and $\mathit{Y}^{\prime}$ is the union of all coeffects in
$\Gamma_{2}+\mathit{X}_{2}\times\Delta^{\prime}$ that are not disjoint from
$\mathit{Y}$ we get that
$\mathit{Y}\subseteq\mathsf{coeff}((\mathit{Y}\cup\\{\ell\\})\times(\Gamma_{1}+\mathit{X}_{1}\times\Delta^{\prime}),\mathit{z})$
implies
$\mathit{Y}^{\prime}\subseteq\mathsf{coeff}((\mathit{Y}\cup\\{\ell\\})\times(\Gamma_{1}+\mathit{X}_{1}\times\Delta^{\prime})+\Gamma_{2}+\mathit{X}_{2}\times\Delta^{\prime},\mathit{z})$.

On the other hand, if
$\mathsf{res}\not\in\mathsf{coeff}(\Gamma_{1}+\mathit{X}_{1}\times\Delta^{\prime},\mathit{z})$,
then
$\mathsf{coeff}(\mathit{Y}^{\prime}\mathrel{\hat{\triangleleft}}(\Gamma_{1}+\mathit{X}_{1}\times\Delta^{\prime}),\mathit{z})=\mathsf{coeff}(\Gamma_{1}+\mathit{X}_{1}\times\Delta^{\prime},\mathit{z})$.
Therefore

$\mathit{Y}^{\prime}\mathrel{\hat{\triangleleft}}(\Gamma_{1}+\mathit{X}_{1}\times\Delta^{\prime})\mathrel{\hat{\subseteq}}(\mathit{Y}\cup\\{\ell\\})\times(\Gamma_{1}+\mathit{X}_{1}\times\Delta^{\prime})+\Gamma_{2}+\mathit{X}_{2}\times\Delta^{\prime}$

and so
$\Gamma^{\prime\prime}=(\mathit{Y}\cup\\{\ell\\})\times(\Gamma_{1}+\mathit{X}_{1}\times\Delta^{\prime})+\Gamma_{2}+\mathit{X}_{2}\times\Delta^{\prime}$.

Finally

$\begin{array}[]{lcl}\Gamma^{\prime\prime}&=&(\mathit{Y}\cup\\{\ell\\})\times(\Gamma_{1}+\mathit{X}_{1}\times\Delta^{\prime})+\Gamma_{2}+\mathit{X}_{2}\times\Delta^{\prime}\\\
&=&((\mathit{Y}\cup\\{\ell\\})\times\mathit{X}_{1})\times\Delta^{\prime}+\mathit{X}_{2}\times\Delta^{\prime}+(\mathit{Y}\cup\\{\ell\\})\times\Gamma_{1}+\Gamma_{2}\\\
&=&((\mathit{Y}\cup\\{\ell\\})\triangleleft\mathit{X}_{1}\cup\mathit{X}_{2})\times\Delta^{\prime}+(\mathit{Y}\cup\\{\ell\\})\times\Gamma_{1}+\Gamma_{2}\\\
\end{array}$

We want to show that
$((\mathit{Y}\cup\\{\ell\\})\triangleleft\mathit{X}_{1}\cup\mathit{X}_{2})\times\Delta^{\prime}+(\mathit{Y}\cup\\{\ell\\})\times\Gamma_{1}+\Gamma_{2}\mathrel{\hat{\subseteq}}\mathit{X}\times\Delta^{\prime}+\Gamma$.
Since
$\mathit{X}\supseteq(\mathit{Y}\cup\\{\ell\\})\triangleleft\mathit{X}_{1}\cup\mathit{X}_{2}$
and
$\Gamma\mathrel{\hat{\subseteq}}(\mathit{Y}\cup\\{\ell\\})\times\Gamma_{1}+\Gamma_{2}$
we derive
$((\mathit{Y}\cup\\{\ell\\})\triangleleft\mathit{X}_{1}\cup\mathit{X}_{2})\times\Delta^{\prime}+(\mathit{Y}\cup\\{\ell\\})\times\Gamma_{1}+\Gamma_{2}\mathrel{\hat{\subseteq}}\mathit{X}\times\Delta^{\prime}+\Gamma$.

∎

###### Proof of Theorem 4.3.

If $\Gamma^{\prime}\vdash\mathit{e}{\mid}\mu:\mathit{T}$, we have
$\Gamma^{\prime}=\Gamma_{1}^{\prime}+\Gamma_{2}$,
$\Gamma_{1}^{\prime}\vdash\mathit{e}:\mathit{T}$ and $\Gamma_{2}\vdash\mu$. We
know that $\Gamma_{2}=\Gamma_{\mu}+\Theta$, where
$\Gamma_{\mu}=\mathit{x}_{1}:_{\\{\ell_{1}\\}}\mathit{T}_{1},\ldots,\mathit{x}_{n}:_{\\{\ell_{n}\\}}\mathit{T}_{n}$,
$\Theta=\sum_{i=1}^{n}\ell_{i}\times\Theta_{i}$,
$\Theta_{i}\vdash\mu(\mathit{x}_{i}):\mathit{T}_{u}$ and
$\ell_{1},\ldots,\ell_{n}$ are fresh links. We also know that
$\Gamma_{2}=\Gamma_{\mu}+\Theta$, where
$\Gamma_{\mu}=\mathit{x}_{1}:_{\\{\ell_{1}\\}}\mathit{T}_{1},\ldots,\mathit{x}_{n}:_{\\{\ell_{n}\\}}\mathit{T}_{n}$,
$\Theta=\sum_{i=1}^{n}\ell_{i}\times\Theta_{i}$,
$\Theta_{i}\vdash\mu(\mathit{x}_{i}):\mathit{T}_{u}$ and
$\ell_{1},\ldots,\ell_{n}$ are fresh links. We also know that by Lemma A.2
$\Gamma_{1}\vdash\mathit{e}:\mathit{T}$ with
$\Gamma_{1}\blacktriangleleft\Gamma_{1}^{\prime}$. In the proof below we prove
the theorem with as hypothesis $\Gamma\vdash\mathit{e}{\mid}\mu:\mathit{T}$
where $\Gamma=\Gamma_{1}+\Gamma_{2}$ obtaining that
$\Delta\vdash\mathit{e}^{\prime}{\mid}\mu^{\prime}:\mathit{T}$ and
$\Gamma+\Delta{\upharpoonright}\Gamma=\Gamma$. We also know that
$\Delta=\Gamma_{3}+\Gamma_{4}$ and $\Gamma_{3}\vdash\mathit{e}:\mathit{T}$ and
$\Gamma_{4}\vdash\mu^{\prime}$. If $\Gamma_{1}=\Gamma_{1}^{\prime}$ we have
also the thesis. If $\Gamma_{1}^{\prime}=\\{\ell\\}\times\Gamma_{1}$ then we
can apply the same non syntx directed rules applied to
$\Gamma_{1}\vdash\mathit{e}:\mathit{T}$ obtaining
$\\{\ell\\}\mathrel{\triangleleft}\Gamma_{3}\vdash\mathit{e}^{\prime}:\mathit{T}$
and so, since $\mathsf{res}\notin\mathsf{links}(\Gamma_{4})$,
$\\{\ell\\}\mathrel{\triangleleft}\Delta\vdash\mathit{e}{\mid}\mu:\mathit{T}$.
By Lemma A.9 we have that
$\\{\ell\\}\times(\Gamma+\Delta){\upharpoonright}\\{\ell\\}\times\Gamma=\\{\ell\\}\times\Gamma$,
that is, the thesis. The proof is by induction on the reduction relation.

(field-access):

We know that
$\mathit{x}\texttt{.}\mathit{f}_{k}{\mid}\mu\rightarrow\mathit{v}_{k}{\mid}\mu$,
hence $\mathit{e}=\mathit{x}\texttt{.}\mathit{f}_{k}$,
$\mathit{e}^{\prime}=\mathit{v}_{k}$ and $\mu^{\prime}=\mu$. We know that
$\mu(\mathit{x})=\texttt{new}\;\mathit{C}\texttt{(}\mathit{v}_{1},\ldots,\mathit{v}_{k},\ldots,\mathit{v}_{m}\texttt{)}$
with k $\in 1..m$. Since $\mathit{x}\in\mathsf{dom}(\mu)$ we know exists an
$h\in 1..n$ such that $\mathit{x}=\mathit{x}_{h}$ and so
$\Theta_{h}\vdash\mu(\mathit{x}):\mathit{T}_{h}$. By Lemma A.3(5) we know that
$\Theta_{h}=\sum_{i=1}^{m}\Theta^{\prime}_{i}$ such that
$\Theta^{\prime}_{i}\vdash\mathit{v}_{i}:\mathit{T}_{i}$. By this
consideration we derive that
$\Theta^{\prime}_{k}\vdash\mathit{v}_{k}:\mathit{T}_{k}$. We know that
$\Gamma\mathrel{\hat{\subseteq}}\\{\ell_{h}\\}\times\Theta_{h}\mathrel{\hat{\subseteq}}\\{\ell_{h}\\}\triangleleft\Theta_{h}$.
For all $\mathit{y}\in\mathsf{dom}(\Theta_{h})$ we know
$\mathsf{coeff}(\\{\ell_{h}\\}\triangleleft\Theta_{h},\mathit{y})$ =
$(\mathsf{coeff}(\Theta_{h},\mathit{y})\setminus\\{\mathsf{res}\\})\cup\\{\ell_{h}\\}$
if $\mathsf{res}\in\mathsf{coeff}(\Theta_{h},\mathit{y})$,
$\mathsf{coeff}(\\{\ell_{h}\\}\triangleleft\Theta_{h},\mathit{y})=\mathsf{coeff}(\Theta_{h},\mathit{y})$
otherwise. We know that
$\\{\mathsf{res},\ell_{h}\\}\subseteq\mathsf{coeff}(\Gamma,\mathit{x})$, so,
since $\Gamma$ is closed and
$\Gamma\mathrel{\hat{\subseteq}}\\{\ell_{h}\\}\triangleleft\Theta_{h}$, for
all $\mathit{y}\in\mathsf{dom}(\\{\ell_{h}\\}\triangleleft\Theta_{h})$,
$\ell_{h}\in\mathsf{coeff}(\\{\ell_{h}\\}\triangleleft\Theta_{h},\mathit{y})$
implies $\mathsf{res}\in\mathsf{coeff}(\Gamma,\mathit{y})$ and so
$\mathsf{coeff}(\Gamma,\mathit{y})\supseteq(\mathsf{coeff}(\Theta_{h},\mathit{y})\setminus\\{\mathsf{res}\\})\cup\\{\ell_{h}\\}\cup\\{\mathsf{res}\\}\supseteq\mathsf{coeff}(\Theta_{h},\mathit{y})$.
By these considerations we derive that
$\Gamma\mathrel{\hat{\subseteq}}\Theta_{h}$. We can apply rule (t-conf)
obtaining
$\Gamma_{2}+\Theta^{\prime}_{k}\vdash\mathit{v}_{k}{\mid}\mu^{\prime}:\mathit{T}_{k}$.
Since $\Gamma=\Gamma+\Gamma_{2}+\Theta^{\prime}_{k}$ we have
$(\Gamma+\Gamma_{2}+\Theta^{\prime}_{k}){\upharpoonright}\Gamma=\Gamma{\upharpoonright}\Gamma=\Gamma$
we have the thesis.

(field-assign):

We know that
$\mathit{x}\texttt{.}\mathit{f}_{k}\texttt{=}\,\mathit{v}{\mid}\mu\rightarrow\mathit{v}{\mid}\mu^{\mathit{x}.k=\mathit{v}}$,
hence $\mathit{e}=\mathit{x}\texttt{.}\mathit{f}_{k}\texttt{=}\,\mathit{v}$,
$\mathit{e}^{\prime}=\mathit{v}$ and
$\mu^{\prime}=\mu^{\mathit{x}.k=\mathit{v}}$. By Lemma A.3(4), we get
$\Gamma_{1}=\Delta_{1}+\Delta_{2}$, $\Delta_{1}\vdash\mathit{x}:\mathit{C}$,
$\Delta_{2}\vdash\mathit{v}:\mathit{T}$, and
$\mathsf{fields}(\mathit{C})=S_{1}\ \mathit{f}_{1}\texttt{;},\ldots,S_{m}\
\mathit{f}_{m}\texttt{;}$ with $k\in 1..m$. Again by Lemma A.3(1), we get
$\Delta_{1}=\mathit{x}:_{\\{\mathsf{res}\\}}\mathit{C}$. We know that
$\mu(\mathit{z})=\mu^{\prime}(\mathit{z})$ for all
$\mathit{z}\in\mathsf{dom}(\mu)\setminus\\{\mathit{x}\\}$ and
$\mu(\mathit{x})=\texttt{new}\;\mathit{C}\texttt{(}\mathit{v}_{1},\ldots,\mathit{v}_{m}\texttt{)}$
and
$\mu^{\prime}(\mathit{x})=\texttt{new}\;\mathit{C}\texttt{(}\mathit{v}_{1},\ldots,\mathit{v}_{k-1},\mathit{v},\mathit{v}_{k+1},\ldots,\mathit{v}_{m}\texttt{)}$.
Since $\mathit{x}\in\mathsf{dom}(\mu)$, there is $h\in 1..n$ such that
$\mathit{x}=\mathit{x}_{h}$ and so
$\Theta_{h}\vdash\mu(\mathit{x}):\mathit{T}_{h}$ holds, with
$\mathit{T}_{h}=\mathit{C}$. Applying Lemma A.3(5), we derive that
$\Theta_{h}=\Sigma_{i=1}^{m}\Theta^{\prime}_{i}$ and
$\Theta^{\prime}_{i}\vdash\mathit{v}_{i}:S_{i}$, for all $i\in 1..m$. By these
considerations and applying rule (t-new) we obtain
$\Sigma_{i=1}^{k-1}\Theta^{\prime}_{i}+\Delta_{2}+\Sigma_{i=k+1}^{m}\Theta^{\prime}_{i}\vdash\texttt{new}\;\mathit{C}\texttt{(}\mathit{v}_{1},\ldots,\mathit{v}_{k-1},\mathit{v},\mathit{v}_{k+1},\ldots,\mathit{v}_{m}\texttt{)}:\mathit{C}$.

Applying rule (t-mem) we can type memory $\mu^{\prime}$, deriving
$\Gamma_{\mu}+(\sum_{i=1}^{h-1}\\{\ell_{i}\\}\times\Theta_{i})+(\\{\ell_{h}\\}\times(\Sigma_{i=1}^{k-1}\Theta^{\prime}_{i}+\Delta_{2}+\Sigma_{i=k+1}^{m}\Theta^{\prime}_{i}))+(\sum_{i=h+1}^{n}\\{\ell_{i}\\}\times\Theta_{i})\vdash\mu^{\prime}$
with $\mathsf{coeff}(\Gamma_{\mu},\mathit{x})=\\{\ell_{\mathit{x}}\\}$. We
know
$\Gamma_{\mu}+(\sum_{i=1}^{h-1}\\{\ell_{i}\\}\times\Theta_{i})+(\\{\ell_{h}\\}\times(\Sigma_{i=1}^{k-1}\Theta^{\prime}_{i}+\Delta_{2}+\Sigma_{i=k+1}^{m}\Theta^{\prime}_{i}))+(\sum_{i=h+1}^{n}\\{\ell_{i}\\}\times\Theta_{i})=\Gamma_{\mu}+(\sum_{i=1}^{h-1}\\{\ell_{i}\\}\times\Theta_{i})+\\{\ell_{h}\\}\times\Sigma_{i=1}^{k-1}\Theta^{\prime}_{i}+\\{\ell_{h}\\}\mathrel{\triangleleft}\Delta_{2}+\\{\ell_{h}\\}\mathrel{\triangleleft}\Sigma_{i=k+1}^{m}\Theta^{\prime}_{i}+(\sum_{i=h+1}^{n}\\{\ell_{i}\\}\times\Theta_{i})$.
We have two cases for all $\mathit{y}\in\mathsf{dom}(\Delta_{2})$:

  * •:

$\mathsf{res}\in\mathsf{coeff}(\Delta_{2},\mathit{y})$
We have
$\mathsf{coeff}(\\{\ell_{h}\\}\triangleleft\Delta_{2},\mathit{y})=(\mathsf{coeff}(\Delta_{2},\mathit{y})\setminus\\{\mathsf{res}\\})\cup\\{\ell_{h}\\}$.
We have
$\\{\mathsf{res},\ell_{h}\\}\subseteq\mathsf{coeff}(\Gamma,\mathit{x})$, and,
since $\Gamma\mathrel{\hat{\subseteq}}\Delta_{2}$ we know
$\mathsf{coeff}(\Gamma,\mathit{y})\supseteq\mathsf{coeff}(\Delta_{2},\mathit{y})$
and in particular $\mathsf{res}\in\mathsf{coeff}(\Gamma,\mathit{y})$. By the
fact that $\Gamma$ is closed we know that
$\ell_{h}\in\mathsf{coeff}(\Gamma,\mathit{y})$. We can also conclude that
$\mathsf{coeff}(\Gamma,\mathit{y})\supseteq\mathsf{coeff}(\Delta_{2},\mathit{y})\cup\\{\ell_{h}\\}\supseteq(\mathsf{coeff}(\Delta_{2},\mathit{y})\setminus\\{\mathsf{res}\\})\cup\\{\ell_{h}\\}$.

  * •:

$\mathsf{res}\notin\mathsf{coeff}(\Delta_{2},\mathit{y})$
We have
$\mathsf{coeff}(\\{\ell_{h}\\}\triangleleft\Delta_{2},\mathit{y})=\mathsf{coeff}(\Delta_{2},\mathit{y})$.
Since $\Gamma\mathrel{\hat{\subseteq}}\Delta_{2}$ we derive
$\mathsf{coeff}(\Gamma,\mathit{y})\supseteq\mathsf{coeff}(\Delta_{2},\mathit{y})$.

By these two considerations we have that
$\\{\ell_{h}\\}\triangleleft\Delta_{2}\mathrel{\hat{\subseteq}}\Gamma$, so
$\\{\ell_{h}\\}\mathrel{\triangleleft}\Delta_{2}\mathrel{\hat{\subseteq}}\Gamma$.

Since $\Gamma_{\mu}\mathrel{\hat{\subseteq}}\Gamma$,
$(\sum_{i=1}^{h-1}\\{\ell_{i}\\}\times\Theta_{i})\mathrel{\hat{\subseteq}}\Gamma$,
$\\{\ell_{h}\\}\times\Sigma_{i=1}^{k-1}\Theta^{\prime}_{i}\mathrel{\hat{\subseteq}}\Gamma$,
$\\{\ell_{h}\\}\mathrel{\triangleleft}\Delta_{2}\mathrel{\hat{\subseteq}}\Gamma$,$\\{\ell_{h}\\}\mathrel{\triangleleft}\Sigma_{i=k+1}^{m}\Theta^{\prime}_{i}\mathrel{\hat{\subseteq}}\Gamma$,
$(\sum_{i=h+1}^{n}\\{\ell_{i}\\}\times\Theta_{i})\mathrel{\hat{\subseteq}}\Gamma$.
We derive
$\Gamma_{\mu}+(\sum_{i=1}^{h-1}\\{\ell_{i}\\}\times\Theta_{i})+\\{\ell_{h}\\}\times\Sigma_{i=1}^{k-1}\Theta^{\prime}_{i}+\\{\ell_{h}\\}\mathrel{\triangleleft}\Delta_{2}+\\{\ell_{h}\\}\mathrel{\triangleleft}\Sigma_{i=k+1}^{m}\Theta^{\prime}_{i}+(\sum_{i=h+1}^{n}\\{\ell_{i}\\}\times\Theta_{i})\mathrel{\hat{\subseteq}}\Gamma$.
Applying rule (t-conf), we obtain
$\Delta=\Gamma_{\mu}+(\sum_{i=1}^{h-1}\\{\ell_{i}\\}\times\Theta_{i})+\\{\ell_{h}\\}\times\Sigma_{i=1}^{k-1}\Theta^{\prime}_{i}+\\{\ell_{h}\\}\mathrel{\triangleleft}\Delta_{2}+\\{\ell_{h}\\}\mathrel{\triangleleft}\Sigma_{i=k+1}^{m}\Theta^{\prime}_{i}+(\sum_{i=h+1}^{n}\\{\ell_{i}\\}\times\Theta_{i})+\Delta_{2}$.
We know that $\Gamma+\Delta=\Gamma$. By the fact that
$\Delta+\Gamma{\upharpoonright}\Gamma=\Gamma{\upharpoonright}\Gamma=\Gamma$ we
obtain the thesis.

(new):

We know that
${\texttt{new}\,\mathit{C}(\mathit{v}_{1},\ldots,\mathit{v}_{n})}{\mid}\mu\rightarrow\mathit{x}{\mid}\mu[{\texttt{new}\,\mathit{C}(\mathit{v}_{1},\ldots,\mathit{v}_{n})}/\mathit{x}]$
with $\mathit{x}\not\in\mathsf{dom}(\mu)$ hence
$\mathit{e}={\texttt{new}\,\mathit{C}(\mathit{v}_{1},\ldots,\mathit{v}_{n})}$,
$\mathit{e}^{\prime}=\mathit{x}$ and
$\mu^{\prime}=\mu[{\texttt{new}\,\mathit{C}(\mathit{v}_{1},\ldots,\mathit{v}_{n})}/\mathit{x}]$.
Since we have $\mu(\mathit{y})=\mu^{\prime}(\mathit{y})$ for all
$\mathit{y}\in\mathsf{dom}(\mu)$ and
$\mathsf{dom}(\mu^{\prime})=\mathsf{dom}(\mu)\cup\\{\mathit{x}\\}$ and
$\mu^{\prime}(\mathit{x})={\texttt{new}\,\mathit{C}(\mathit{v}_{1},\ldots,\mathit{v}_{n})}$
we can apply rule (t-mem) deriving
$\Gamma_{\mu}+\mathit{x}:_{\ell_{m+1}}\mathit{C}+\Theta+(\ell_{m+1}\times\Gamma_{1})\vdash\mu^{\prime}$
, where $\Gamma_{1}\vdash\mu^{\prime}(\mathit{x}):\mathit{C}$, $\ell_{m+1}$
fresh and $\ell_{m+1}\notin\mathsf{links}(\Gamma)$. By rule (t-var) we know
$\mathit{x}:_{\\{\mathsf{res}\\}}\mathit{C}\vdash\mathit{x}:\mathit{C}$. By
rule (t-conf) we derive
$\Delta=\Gamma_{\mu}+\mathit{x}:_{\\{\ell_{m+1}\\}}\mathit{C}+\Theta+(\\{\ell_{m+1}\\}\times\Gamma_{1})+\mathit{x}:_{\\{\mathsf{res}\\}}\mathit{C}$
and
$\Gamma_{\mu}+\mathit{x}:_{\\{\ell_{m+1}\\}}\mathit{C}+\Theta+(\\{\ell_{m+1}\\}\times\Gamma_{1})+\mathit{x}:_{\\{\mathsf{res}\\}}\mathit{C}\vdash\mathit{x}{\mid}\mu^{\prime}:\mathit{C}$.
We know
$\Gamma+\Delta=\Gamma_{\mu}+\mathit{x}:_{\\{\ell_{m+1}\\}}\mathit{C}+\Theta+(\\{\ell_{m+1}\\}\times\Gamma_{1})+\mathit{x}:_{\\{\mathsf{res}\\}}\mathit{C}+\Gamma=\Gamma+\mathit{x}:_{\\{\mathsf{res},\ell_{m+1}\\}}\mathit{C}+(\\{\ell_{m+1}\\}\times\Gamma_{1})$.
We know that $\ell_{m+1}\notin\mathsf{coeff}(\Gamma,\mathit{y})$ for all
$\mathit{y}\in\mathsf{dom}(\Gamma)$ and we know that, since $\Gamma$ is
closed, $\mathsf{res}\in\mathsf{coeff}(\Gamma,\mathit{y})$ and
$\mathsf{res}\in\mathsf{coeff}(\Gamma,\mathit{z})$ implies
$\mathsf{coeff}(\Gamma,\mathit{y})=\mathsf{coeff}(\Gamma,\mathit{z})$ for all
$\mathit{y},\mathit{z}\in\mathsf{dom}(\Gamma)$. We also know that
$\mathit{x}\notin\mathsf{dom}(\Gamma)$, so
$\Gamma+\mathit{x}:_{\\{\ell_{m+1},\mathsf{res}\\}}\mathit{C}$ =
${(\Gamma,\mathit{x}:_{\\{\ell_{m+1},\mathsf{res}\\}}\mathit{C})}^{\star}=\Gamma^{\prime},\mathit{x}:_{\mathit{X}}\mathit{C}$.
By Lemma A.5 and by the observations above we have 2 cases for all
$\mathit{y}\in\mathsf{dom}(\Gamma)$:

  * •:

$\mathsf{res}\notin\mathsf{coeff}(\Gamma,\mathit{y})$ implies
$\mathsf{coeff}(\Gamma^{\prime},\mathit{y})=\mathsf{coeff}(\Gamma,\mathit{y})$

  * •:

$\mathsf{res}\in\mathsf{coeff}(\Gamma,\mathit{y})$ implies
$\mathsf{coeff}(\Gamma^{\prime},\mathit{y})=\mathsf{coeff}(\Gamma,\mathit{y})\cup\\{\ell_{m+1},\mathsf{res}\\}=\mathsf{coeff}(\Gamma,\mathit{y})\cup\\{\ell_{m+1}\\}$

We know
$\Gamma_{1}\mathrel{\hat{\subseteq}}\Gamma\mathrel{\hat{\subseteq}}\Gamma^{\prime}$
and
$(\Gamma^{\prime},\mathit{x}:_{\mathit{X}}\mathit{C})+(\\{\ell_{m+1}\\}\times\Gamma_{1})=(\Gamma^{\prime},\mathit{x}:_{\mathit{X}}\mathit{C})+(\\{\ell_{m+1}\\}\triangleleft\Gamma_{1})$.

If $\mathsf{res}\in\mathsf{coeff}(\Gamma_{1},\mathit{y})$ then
$\mathsf{coeff}(\\{\ell_{m+1}\\}\triangleleft\Gamma_{1},\mathit{y})=(\mathsf{coeff}(\Gamma_{1},\mathit{y})\setminus\\{\mathsf{res}\\})\cup\\{\ell_{m+1}\\}$
and, since $\mathsf{res}\in\mathsf{coeff}(\Gamma,\mathit{y})$,
$\mathsf{coeff}(\Gamma^{\prime},\mathit{y})=\mathsf{coeff}(\Gamma,\mathit{y})\cup\\{\ell_{m+1}\\}\supseteq\mathsf{coeff}(\Gamma_{1},\mathit{y})\cup\\{\ell_{m+1}\\}$
for all $\mathit{y}\in\mathsf{dom}(\Gamma_{1})$. if
$\mathsf{res}\notin\mathsf{coeff}(\Gamma_{1},\mathit{y})$ then
$\mathsf{coeff}(\\{\ell_{m+1}\\}\triangleleft\Gamma_{1},\mathit{y})=\mathsf{coeff}(\Gamma_{1},\mathit{y})\subseteq\mathsf{coeff}(\Gamma^{\prime},\mathit{y})$
for all $\mathit{y}\in\mathsf{dom}(\Gamma_{1})$. By these observations we can
conclude that
$(\Gamma^{\prime},\mathit{x}:_{\mathit{X}}\mathit{C})+(\\{\ell_{m+1}\triangleleft\Gamma_{1}\\})=\Gamma^{\prime},\mathit{x}:_{\mathit{X}}\mathit{C}=\Gamma+\Delta$.
By the fact that $\ell_{m+1}\notin\mathsf{links}(\Gamma)$ and
$\mathsf{coeff}(\Gamma+\Delta,\mathit{z})=\mathsf{coeff}(\Gamma,\mathit{z})$
or
$\mathsf{coeff}(\Gamma+\Delta,\mathit{z})=\mathsf{coeff}(\Gamma,\mathit{z})\cup\\{\ell_{m+1}\\}$
for all $\mathit{z}\in\mathsf{dom}(\Gamma)$ we derive that
$(\Gamma+\Delta){\upharpoonright}\Gamma=\Gamma$, that is, the thesis.

(ctx):

We have $\mathit{e}={\cal{E}}[\mathit{e}_{1}]$ and
$\mathit{e}^{\prime}={\cal{E}}[\mathit{e}^{\prime}_{1}]$ and
${\mathit{e}_{1}{\mid}\mu\rightarrow\mathit{e}_{1}^{\prime}{\mid}\mu^{\prime}}$.
By Lemma A.6, $\Gamma_{1}=\Delta_{1}+\mathit{X}\times\Delta_{2}$,
$\Delta_{1}+\mathit{x}:_{\mathit{X}}\mathit{T}^{\prime}\vdash{\cal{E}}[\mathit{x}]:\mathit{T}$
and $\Delta_{2}\vdash\mathit{e}_{1}:\mathit{T}^{\prime}$ and we can impose
that if $\ell\in\mathsf{coeff}(\Delta_{1},\mathit{x})$ and $\ell\in\mathit{X}$
then $\mathsf{coeff}(\Delta_{1},\mathit{x})=\mathit{X}$. We get
$\Gamma=\Gamma_{1}+\Gamma_{2}=\Delta_{1}+\mathit{X}\times\Delta_{2}+\Gamma_{2}$
and, since $\mathsf{res}\notin\mathsf{coeff}(\Gamma_{2},\mathit{y})$ for every
$\mathit{y}\in\mathsf{dom}(\Gamma_{2})$ by rule (t-mem) we have
$\Gamma_{2}=\mathit{X}\times\Gamma_{2}$, hence
$\Gamma=\Delta_{1}+\mathit{X}\times(\Delta_{2}+\Gamma_{2})$. We set
$\Gamma^{\prime}=\Delta_{2}+\Gamma_{2}$. By induction hypothesis, we get
$\Delta^{\prime}\vdash\mathit{e}_{1}^{\prime}{\mid}\mu^{\prime}:\mathit{T}^{\prime}$
with
$\Delta^{\prime}+\Gamma^{\prime}{\upharpoonright}\Gamma^{\prime}=\Gamma^{\prime}$.
By rule (t-conf), we know that
$\Delta^{\prime}=\Delta^{\prime}_{1}+\Delta^{\prime}_{2}$ with
$\Delta^{\prime}_{1}\vdash\mathit{e}_{1}^{\prime}:\mathit{T}^{\prime}$ and
$\Delta^{\prime}_{2}\vdash\mu^{\prime}$. By Lemma A.7, we get
$\Delta_{1}+\mathit{X}\times\Delta^{\prime}_{1}\vdash{\cal{E}}[\mathit{e}_{1}^{\prime}]:\mathit{T}$
and so
$\Delta_{1}+\mathit{X}\times\Delta^{\prime}_{1}+\Delta^{\prime}_{2}\vdash{\cal{E}}[\mathit{e}_{1}^{\prime}]{\mid}\mu^{\prime}:\mathit{T}$.
We have
$\Delta=\Delta_{1}+\mathit{X}\times\Delta^{\prime}_{1}+\Delta^{\prime}_{2}=\Delta_{1}+\mathit{X}\times\Delta^{\prime}_{1}+\mathit{X}\times\Delta^{\prime}_{2}=\Delta_{1}+\mathit{X}\times\Delta^{\prime}$.
We get the thesis, that is, $\Delta+\Gamma{\upharpoonright}\Gamma=\Gamma$, by
Lemma A.9, since
$\mathsf{links}(\Delta_{1})\cap(\mathsf{links}(\mathit{X}\mathrel{\triangleleft}(\Delta^{\prime}+\Gamma^{\prime}))\cup\mathsf{links}(\mathit{X}\mathrel{\triangleleft}\Gamma^{\prime}))=\\{\mathsf{res}\\}$
or
$\mathsf{links}(\Delta_{1})\cap(\mathsf{links}(\mathit{X}\mathrel{\triangleleft}(\Delta^{\prime}+\Gamma^{\prime}))\cup\mathsf{links}(\mathit{X}\mathrel{\triangleleft}\Gamma^{\prime}))=\\{\mathsf{res}\\}\cup\mathit{X}$
if exists $\mathit{x}\in\mathsf{dom}(\Delta)$ such that
$\mathsf{coeff}(\Delta,\mathit{x})=\mathit{X}$
$\mathsf{dom}(\Delta_{1})\subseteq\mathsf{dom}(\Gamma_{\mathsf{res}})\subseteq\mathsf{dom}(\mathit{X}\times\Gamma^{\prime})$.

(block):

$\\{\mathit{T}\,\mathit{x}=\mathit{v}\texttt{;}\,\mathit{e}\\}{\mid}\mu\rightarrow\mathit{e}[\mathit{v}/\mathit{x}]{\mid}\mu$
Applying Lemma A.3(7) we obtain
$\Gamma^{\prime},\mathit{x}:_{\mathit{X}}\mathit{T}\vdash\mathit{e}:\mathit{T}^{\prime}$
and $\Sigma\vdash\mathit{v}:\mathit{T}$ such that
$\Gamma_{1}=(\mathit{X}\cup\\{\ell\\})\times\Sigma+\Gamma^{\prime}$. If
$\mathit{v}$ is a reference then by Lemma A.3(1) we know
$\Sigma=\mathit{x}:_{\\{\mathsf{res}\\}}\mathit{T}$ otherwise if $\mathit{v}$
is a primitive value then we know by (t-primitive) $\Sigma=\emptyset$.
Applying Lemma A.10 we obtain
$\Gamma^{\prime\prime}\vdash\mathit{e}[\mathit{v}/\mathit{x}]:\mathit{T}^{\prime}$
and
$\Gamma^{\prime\prime}\mathrel{\hat{\subseteq}}(\mathit{X}\cup\\{\ell\\})\times\Sigma+\Gamma^{\prime}$.
Knowing that $\Gamma^{\prime\prime}+\Gamma_{2}+\Gamma=\Delta+\Gamma=\Gamma$ we
obtain $\Gamma{\upharpoonright}\Gamma=\Gamma$,that is, the thesis.

∎

##  Appendix B Proof of Theorem 5.2

###### Definition B.1.

$\Gamma\blacktriangleleft\Gamma^{\prime}$ if

  1. (1)

$\Gamma^{\prime}={\Gamma}$ or

  2. (2)

$\Gamma^{\prime}=\Gamma[\sigma]$ or

  3. (3)

$\Gamma^{\prime}=\\{\ell\\}\times\Gamma$ with $\ell$ fresh, or

  4. (4)

$\Gamma^{\prime}=\\{\ell\\}\times\Gamma[\sigma]$ with $\ell$ fresh.

###### Lemma B.2.

If ${\cal D}:\Gamma\vdash{\mathit{e}}:\mathit{T}$, then there is a
subderivation ${\cal
D}^{\prime}:\Gamma^{\prime}\vdash{\mathit{e}}:\mathit{T}^{\prime}$ of ${\cal
D}$ ending with a syntax-directed rule and
$\Gamma^{\prime}\blacktriangleleft\Gamma$

###### Lemma B.3.

If for all $\mathit{x}\in(\mathsf{dom}(\Gamma)\cap\mathsf{dom}(\Delta))$,
$\mathsf{modif}(\Gamma,\mathit{x})\leq\mathsf{modif}(\Delta,\mathit{x})$ then
for all $\mathit{x}\in(\mathsf{dom}(\Gamma)\cap\mathsf{dom}(\Delta))$,
$\mathsf{modif}(\Gamma[\sigma],\mathit{x})\leq\mathsf{modif}(\Delta[\sigma],\mathit{x})$.

###### Proof.

We consider only type contexts for terms, so modifiers can be only
imm,$\mathsf{mut}$ and $\sigma$. We also consider
$\mathit{x}:_{\mathit{X}}\mathit{T}^{\textsc{m}}\in\Gamma$ and
$\mathit{x}:_{\mathit{X}^{\prime}}\mathit{T}^{\textsc{m}^{\prime}}\in\Delta$.
We have 3 cases:

  * •

$\textsc{m}=\textsc{m}^{\prime}$
Immediate

  * •

$\textsc{m}=\sigma$ and $\textsc{m}^{\prime}=\texttt{imm}$
We know $\sigma[\sigma^{\prime}]=\sigma$ and
$\texttt{imm}[\sigma^{\prime}]=\texttt{imm}$, so we have the thesis

  * •

$\textsc{m}=\sigma$ and $\textsc{m}^{\prime}=\mathsf{mut}$
We know $\sigma[\sigma^{\prime}]=\sigma$ and
$\mathsf{mut}[\sigma^{\prime}]=\sigma^{\prime}$, so we have the thesis

∎

###### Lemma B.4.

Let $\Gamma,\Delta\vdash\mu$ where,
$\Delta=\mathit{x}_{1}:_{\mathit{X}}\mathit{C}_{1}^{\sigma},\ldots,\mathit{x}_{n}:_{\mathit{X}}\mathit{C}_{n}^{\sigma}$
and, for all $\mathit{x}\in\mathsf{dom}(\Gamma)$,
$\mathsf{coeff}(\Gamma,\mathit{x})\cap\mathit{X}=\emptyset$. Let
$\textsc{m}\notin\\{\mathsf{read},\mathsf{caps}\\}$ be a modifier and
$\Theta=\mathit{x}_{1}:_{\mathit{X}_{1}}\mathit{C}_{1}^{\textsc{m}},\ldots,\mathit{x}_{n}:_{\mathit{X}_{n}}\mathit{C}_{n}^{\textsc{m}}$
be such that

  * •

$\textsc{m}=\texttt{imm}$ implies $\mathit{X}_{i}=\\{\ell_{i}\\}$, with
$\ell_{i}$ fresh for all $i\in 1..n$.

  * •

$\textsc{m}\neq\texttt{imm}$ implies $\mathit{X}_{i}=\mathit{X}$ for all $i\in
1..n$.

Then, $\Gamma,\Theta\vdash\mu$ holds.

###### Lemma B.5.

Let $\Gamma+\Gamma_{\mu}\vdash\mu$, where

  * •

$\Gamma_{\\!\mu}=\sum_{\mathit{z}\in\mathsf{dom}(\mu)}\mathit{z}:_{\\{\ell_{\mathit{z}}\\}}\mathit{C}_{z}^{\textsc{m}_{\mathit{z}}}$
with $\ell_{\mathit{z}}$ fresh for all $\mathit{z}\in\mathsf{dom}(\mu)$;

  * •

$\Gamma=\sum_{\mathit{z}\in\mathsf{dom}(\mu)}\\{\ell_{\mathit{z}}\\}\mathrel{\triangleleft}\Gamma_{\mathit{z}}$
where
$\Gamma_{\mathit{z}}\Vdash\mu(\mathit{z}):\mathit{C}_{\mathit{z}}^{\textsc{m}_{\mathit{z}}}$
for all $\mathit{z}\in\mathsf{dom}(\mu)$;

  * •

$\mathit{x},\mathit{y}\in\mathsf{dom}(\mu)$ and
$\mu(\mathit{x})=[\mathit{v}_{1},\ldots,\mathit{v}_{m}]^{\mathit{C}_{\mathit{x}}}$,
$\mathsf{fields}(\mathit{C}_{\mathit{x}})=\mathit{T}_{1}\
\mathit{f}_{1}\texttt{;}\ldots\mathit{T}_{m}\ \mathit{f}_{m}\texttt{;}$,
$\Gamma_{\mathit{x}}=\sum_{j=1}^{m}\Gamma^{\prime}_{j}$,
$\Gamma^{\prime}_{j}\Vdash\mathit{v}_{j}:\mathit{T}_{j}[\textsc{m}_{\mathit{x}}]$,
for all $j\in 1...m$, and
$\mathit{T}_{i}[\textsc{m}_{\mathit{x}}]=\mathit{C}_{\mathit{y}}^{\textsc{m}_{\mathit{y}}}$
and
$\Gamma^{\prime}_{i}=\mathit{y}^{\prime}:_{\mathit{Y}}\mathit{C}_{\mathit{y}}^{\textsc{m}_{\mathit{y}}}$
for some $i\in 1...m$.

Let $\Delta$ be such that
$\Delta=\\{\ell_{\mathit{x}}\\}\mathrel{\triangleleft}\Delta_{\mathit{x}}+\sum_{\mathit{z}\in\mathsf{dom}(\mu)\setminus\\{\mathit{x}\\}}\\{\ell_{\mathit{z}}\\}\mathrel{\triangleleft}\Gamma_{\mathit{z}}$
with
$\Delta_{\mathit{x}}=\mathit{y}:_{\mathit{Y}}\mathit{C}_{\mathit{y}}^{\textsc{m}_{\mathit{y}}}+\sum_{j=1}^{i-1}\Gamma^{\prime}_{j}+\sum_{j=i+1}^{m}\Gamma^{\prime}_{j}$.
Then, $\Delta+\Gamma_{\mu}\vdash\mu^{\mathit{x}.i=\mathit{y}}$ holds and
$\mathsf{modif}(\Gamma+\Gamma_{\mu},\mathit{z})=\mathsf{modif}(\Delta+\Gamma_{\mu},\mathit{z})$
for all $\mathit{z}\in\mathsf{dom}(\mu)$

###### Proof of Theorem 5.2.

Since the proof for condition
$(\Gamma^{\prime}+\Delta^{\prime}){\upharpoonright}\Gamma^{\prime}=\Gamma^{\prime}$,
for $\Gamma^{\prime}=\mathsf{erase}(\Gamma)$ and
$\Delta^{\prime}=\mathsf{erase}(\Delta)$ is analogous to the proof for Theorem
4.3 in this proof we focus on the condition for all
$\mathit{x}\in\mathsf{dom}(\Gamma)$,
$\mathsf{modif}(\Gamma,\mathit{x})\leq\mathsf{modif}(\Delta,\mathit{x})$ . If
$\Gamma\vdash\mathit{e}{\mid}\mu:\mathit{T}$, we have
$\Gamma=\Gamma_{1}+\Gamma_{2}$, $\Gamma_{1}\vdash\mathit{e}:\mathit{T}$ and
$\Gamma_{2}\vdash\mu$. We also know that $\Gamma_{2}=\Gamma_{\mu}+\Theta$,
where
$\Gamma_{\mu}=\mathit{x}_{1}:_{\\{\ell_{1}\\}}\mathit{T}_{1},\ldots,\mathit{x}_{n}:_{\\{\ell_{n}\\}}\mathit{T}_{n}$,
$\Theta=\sum_{i=1}^{n}\ell_{i}\times\Theta_{i}$,
$\Theta_{i}\vdash\mu(\mathit{x}_{i}):\mathit{T}_{u}$ and
$\ell_{1},\ldots,\ell_{n}$ are fresh links. The proof is by induction on the
reduction relation.

(field-assign):

By Lemma B.2 and rule (t-assign) we have
$\Gamma_{1}^{\prime\prime}\vdash\mathit{x}:\mathit{T}_{i}$ and
$\Gamma_{2}^{\prime\prime}\vdash\mathit{v}:\mathit{T}_{i}$ such that
$\Gamma_{1}^{\prime\prime}+\Gamma_{2}^{\prime\prime}\blacktriangleleft\Gamma_{1}$
with $\mathsf{fields}(\mathit{C})=\mathit{T}_{1}\
\mathit{f}_{1}\texttt{;}\ldots\mathit{T}_{n}\ \mathit{f}_{n}\texttt{;}i\in
1..n$. We have two interesting cases considering $\mathit{v}=\mathit{y}$:

  * •:

$\mathit{T}_{i}=\mathit{D}^{\texttt{imm}}$
Since $\Gamma_{2}^{\prime\prime}\vdash\mathit{y}:\mathit{D}^{\texttt{imm}}$ we
know that
$\mathsf{modif}(\Gamma_{2}^{\prime\prime},\mathit{y})\neq\mathsf{mut}$ and so
$\mathsf{modif}(\Gamma,\mathit{y})\neq\mathsf{mut}$. By rule (t-var) we have
$\mathit{y}:_{\mathit{Y}}\mathit{D}^{\texttt{imm}}\vdash\mathit{y}:\mathit{D}^{\texttt{imm}}$.
By applying the same non syntax directed rules applied to
$\Gamma_{1}^{\prime\prime}+\Gamma_{2}^{\prime\prime}\vdash\mathit{x}\texttt{.}\mathit{f}_{i}\texttt{=}\,\mathit{y}:\mathit{D}^{\texttt{imm}}$
we have
$\mathit{y}:_{\mathit{Y}}\mathit{D}^{\texttt{imm}}\vdash\mathit{y}:\mathit{T}$.
We have two cases:

    * –:

$\mathsf{modif}(\Gamma,\mathit{y})=\texttt{imm}$
By Lemma B.5 and applying rule (t-conf) we have the thesis

    * –:

$\mathsf{modif}(\Gamma,\mathit{y})=\sigma$
By Lemma B.4 applied to variables with coeffect
$\mathsf{coeff}(\Gamma_{2},\mathit{y})$ and with $\textsc{m}=\texttt{imm}$, by
Lemma B.5 and by applying rule (t-conf) we have the thesis

  * •:

$\mathit{T}_{i}=\mathit{D}^{\mathsf{mut}}$
Since $\Gamma_{1}^{\prime\prime}\vdash\mathit{x}:\mathit{C}^{\mathsf{mut}}$
and $\Gamma_{2}^{\prime\prime}\vdash\mathit{y}:\mathit{D}^{\mathsf{mut}}$ we
know that
$\mathsf{modif}(\Gamma_{1}^{\prime\prime},\mathit{x})\neq\mathsf{mut}$ and
$\mathsf{modif}(\Gamma_{2}^{\prime\prime},\mathit{y})\neq\texttt{imm}$ and so
$\mathsf{modif}(\Gamma,\mathit{x})\neq\texttt{imm}$ and
$\mathsf{modif}(\Gamma,\mathit{y})\neq\texttt{imm}$. We have 4 cases:

    * –:

$\mathsf{modif}(\Gamma,\mathit{x})=\mathsf{mut}$ and
$\mathsf{modif}(\Gamma,\mathit{y})=\mathsf{mut}$
We can apply the same non syntax directed rules applied to
$\Gamma_{1}^{\prime\prime}+\Gamma_{2}^{\prime\prime}\vdash\mathit{x}\texttt{.}\mathit{f}_{i}\texttt{=}\,\mathit{y}:\mathit{D}^{\texttt{imm}}$
to $\Gamma_{2}^{\prime\prime}\vdash\mathit{v}:\mathit{T}_{i}$. By Lemma B.5
and applying rule (t-conf) we have the thesis

    * –:

$\mathsf{modif}(\Gamma,\mathit{x})=\mathsf{mut}$ and
$\mathsf{modif}(\Gamma,\mathit{y})=\sigma$
We know by Lemma B.2 and rule (t-var) that
$\mathit{x}:_{\mathit{X}^{\prime\prime}}\mathit{T}^{\prime\prime}\vdash\mathit{x}:\mathit{T}^{\prime\prime}$.
We can apply rule (t-var) and the same non syntax-directed rules applied to
$\mathit{x}$ on $\mathit{y}$ to obtain
$\mathit{y}:_{\mathit{X}^{\prime}}\mathit{D}^{\mathsf{modif}(\Gamma_{1}^{\prime\prime}+\Gamma_{2}^{\prime\prime},\mathit{x})}\vdash\mathit{y}:\mathit{D}^{\mathsf{mut}}$.
If we apply the same non syntax-directed rules applied to
$\Gamma_{1}^{\prime\prime}+\Gamma_{2}^{\prime\prime}\vdash\mathit{x}\texttt{.}\mathit{f}_{i}\texttt{=}\,\mathit{y}:\mathit{T}_{i}$
we have
$\mathit{y}:_{\mathit{X}}\mathit{D}^{\mathsf{mut}}\vdash\mathit{y}:\mathit{T}$.
By Lemma B.4 applied to variables with coeffect
$\mathsf{coeff}(\Gamma_{2},\mathit{y})$ and with $\textsc{m}=\mathsf{mut}$, by
Lemma B.5 and applying rule (t-conf) we have the thesis.

    * –:

$\mathsf{modif}(\Gamma,\mathit{x})=\sigma$ and
$\mathsf{modif}(\Gamma,\mathit{y})=\sigma^{\prime}$
Reasoning similar to that above. We also apply Lemma B.4 with
$\textsc{m}=\sigma$

    * –:

$\mathsf{modif}(\Gamma,\mathit{x})=\sigma$ and
$\mathsf{modif}(\Gamma,\mathit{y})=\mathsf{mut}$
We can apply the same non syntax-directed rules applied to
$\Gamma_{1}^{\prime\prime}+\Gamma_{2}^{\prime\prime}\vdash\mathit{x}\texttt{.}\mathit{f}_{i}\texttt{=}\,\mathit{y}:\mathit{T}_{i}$
to $\Gamma_{2}^{\prime\prime}\vdash\mathit{y}:\mathit{T}_{i}$ to have
$\mathit{y}:_{\mathit{Y}}\mathit{D}^{\mathsf{mut}}\vdash\mathit{y}:\mathit{T}$.
By Lemma B.4 applied to variables with coeffect
$\mathsf{coeff}(\Gamma_{2},\mathit{x})$ and with $\textsc{m}=\mathsf{mut}$, by
Lemma B.5 and applying rule (t-conf) we have the thesis.

(block):

We have
$\\{\mathit{T}^{\prime}\,\mathit{x}=\mathit{v}\texttt{;}\,\mathit{e}\\}$. By
Lemma B.2 and rule (t-block) we have a contexts
$(\mathit{X}\cup\\{\ell\\})\times\Gamma_{1}^{\prime\prime}+\Gamma_{2}^{\prime\prime}\blacktriangleleft\Gamma_{1}$
such that
$(\mathit{X}\cup\\{\ell\\})\times\Gamma_{1}^{\prime\prime}+\Gamma_{2}^{\prime\prime}\vdash\\{\mathit{T}^{\prime}\,\mathit{x}=\mathit{v}\texttt{;}\,\mathit{e}\\}:\mathit{T}$,
$\Gamma_{1}^{\prime\prime}\vdash\mathit{v}:\mathit{T}^{\prime}$ and
$\Gamma_{2}^{\prime\prime},\mathit{x}:_{\mathit{X}}\mathit{T}^{\prime}\vdash\mathit{e}:\mathit{T}$.
By Lemma A.10 we have that
$\Delta^{\prime\prime}\vdash\mathit{e}^{\prime}[\mathit{v}/\mathit{x}]:\mathit{T}$
with
$\Delta^{\prime\prime}\mathrel{\hat{\subseteq}}\mathit{X}\times\Gamma_{1}^{\prime}+\Gamma_{2}^{\prime\prime}\mathrel{\hat{\subseteq}}(\mathit{X}\cup\\{\ell\\})\times\Gamma_{1}^{\prime\prime}+\Gamma_{2}^{\prime\prime}$.
By applying the same non syntax directed rules applied to
$(\mathit{X}\cup\\{\ell\\})\times\Gamma_{1}^{\prime\prime}+\Gamma_{2}^{\prime\prime}\vdash\\{\mathit{T}^{\prime}\,\mathit{x}=\mathit{v}\texttt{;}\,\mathit{e}\\}:\mathit{T}$
since
$\Delta^{\prime\prime}\mathrel{\hat{\subseteq}}(\mathit{X}\cup\\{\ell\\})\times\Gamma_{1}^{\prime\prime}+\Gamma_{2}^{\prime\prime}$
we have the thesis.

(field-access):

We know that
$\mathit{x}\texttt{.}\mathit{f}{\mid}\mu\rightarrow\mathit{v}{\mid}\mu$, hence
$\mathit{e}=\mathit{x}\texttt{.}\mathit{f}$, $\mathit{e}^{\prime}=\mathit{v}$.
By Lemma B.2 and rule (t-field-access) we have
$\Gamma^{\prime\prime}\vdash\mathit{x}\texttt{.}\mathit{f}_{i}:\mathit{T}_{i}[\textsc{m}]$
and $\Gamma^{\prime\prime}\vdash\mathit{x}:\mathit{C}^{\textsc{m}}$ such that
$\Gamma^{\prime\prime}\blacktriangleleft\Gamma_{1}$ and
$\mathit{T}^{\prime}=\mathit{T}_{i}[\textsc{m}]\leq\mathit{T}$ with
$\mathsf{fields}(\mathit{C})=\mathit{T}_{1}\
\mathit{f}_{1}\texttt{;}\ldots\mathit{T}_{n}\ \mathit{f}_{n}\texttt{;}i\in
1..n$. We have two interesting cases:

  * •:

$\mathit{T}_{i}=\mathit{D}^{\texttt{imm}}$
By rule (t-var) we can derive
$\mathit{y}:_{\mathit{X}^{\prime}}\mathit{D}^{\texttt{imm}}\vdash\mathit{y}:\mathit{D}^{\texttt{imm}}$.
Since $\mathit{T}=\mathit{T}_{i}[\textsc{m}]=\mathit{D}^{\texttt{imm}}$ we
know that to
$\Gamma^{\prime\prime}\vdash\mathit{x}\texttt{.}\mathit{f}_{i}:\mathit{D}^{\texttt{imm}}$
is not applied rule (t-caps), so, if we apply to
$\mathit{y}:_{\mathit{X}}\mathit{D}^{\texttt{imm}}\vdash\mathit{y}:\mathit{D}^{\texttt{imm}}$
the same non syntax-directed rules applied to
$\Gamma^{\prime\prime}\vdash\mathit{x}\texttt{.}\mathit{f}_{i}:\mathit{D}^{\texttt{imm}}$
we obtain
$\mathit{y}:_{\mathit{X}}\mathit{D}^{\texttt{imm}}\vdash\mathit{y}:\mathit{T}$,
where $\mathit{X}=\mathsf{coeff}(\Gamma_{1},\mathit{x})$. By rule (t-mem) and
(t-obj) we have
$\Delta_{1}+\cdots+\Delta_{n}\Vdash[\mathit{v}_{1},\ldots,\mathit{v}_{n}]^{\mathit{C}}:\mathit{C}^{\textsc{m}^{\prime}}$
and $\Delta_{i}\Vdash\mathit{v}_{i}:\mathit{T}_{i}[\textsc{m}^{\prime}]$ where
$\mu(\mathit{x})=[\mathit{v}_{1},\ldots,\mathit{v}_{n}]^{\mathit{C}}$,
$\mathsf{fields}(\mathit{C})=\mathit{T}_{1}\
\mathit{f}_{1}\texttt{;}\ldots\mathit{T}_{n}\ \mathit{f}_{n}\texttt{;}$ and
exists $i$ such that $\mathit{v}_{i}=\mathit{y}$. Since
$\mathit{T}_{i}=\mathit{D}^{\texttt{imm}}$ we know
$\mathit{T}_{i}[\textsc{m}]=\mathit{D}^{\texttt{imm}}$ and
$\Gamma_{i}\Vdash\mathit{y}:\mathit{D}^{\texttt{imm}}$.By rule (t-imm-ref) we
obtain $\Delta_{i}=\mathit{y}:_{\\{\ell\\}}\mathit{D}^{\texttt{imm}}$ with
$\ell$ fresh. Since memory does not change applying rule (t-conf) we obtain
the thesis.

  * •:

$\mathit{T}_{i}=\mathit{D}^{\mathsf{mut}}$
We know by Lemma B.2 and rule (t-var) that
$\mathit{x}:_{\mathit{X}^{\prime\prime}}\mathit{T}^{\prime\prime}\vdash\mathit{x}:\mathit{T}^{\prime\prime}$
and
$\Gamma^{\prime\prime}=\mathit{x}:_{\mathit{X}^{\prime}}\mathit{C}^{\textsc{m}^{\prime}}$.
We can apply rule (t-var) and the same non syntax-directed rules applied to
$\mathit{x}$ on $\mathit{y}$ to obtain
$\mathit{y}:_{\mathit{X}^{\prime}}\mathit{T}_{i}[\textsc{m}^{\prime}]\vdash\mathit{y}:\mathit{T}_{i}[\textsc{m}]$.
If we apply the same non syntax-directed rules applied to
$\Gamma^{\prime\prime}\vdash\mathit{x}\texttt{.}\mathit{f}_{i}:\mathit{T}_{i}[\textsc{m}]$
we have
$\mathit{y}:_{\mathit{X}}\mathit{T}_{i}[\textsc{m}^{\prime\prime}]\vdash\mathit{y}:\mathit{T}$.
We know
$\mathsf{modif}(\Gamma,\mathit{x})=\mathsf{modif}(\mathit{y}:_{\mathit{X}}\mathit{T}_{i}[\textsc{m}^{\prime\prime}],\mathit{y})=\textsc{m}^{\prime\prime}$
and $\mathsf{coeff}(\Gamma_{1},\mathit{x})=\mathit{X}$. By rule (t-mem) and
(t-obj) we have
$\Delta_{1}+\cdots+\Delta_{n}\Vdash[\mathit{v}_{1},\ldots,\mathit{v}_{n}]^{\mathit{C}}:\mathit{C}^{\textsc{m}^{\prime\prime}}$
and $\Delta_{i}\Vdash\mathit{v}_{i}:\mathit{T}_{i}[\textsc{m}^{\prime\prime}]$
where $\mu(\mathit{x})=[\mathit{v}_{1},\ldots,\mathit{v}_{n}]^{\mathit{C}}$,
$\mathsf{fields}(\mathit{C})=\mathit{T}_{1}\
\mathit{f}_{1}\texttt{;}\ldots\mathit{T}_{n}\ \mathit{f}_{n}\texttt{;}$ and
exists $i$ such that $\mathit{v}_{i}=\mathit{y}$. By rule (t-imm-ref) we
obtain
$\Delta_{i}=\mathit{y}:_{\\{\ell\\}}\mathit{T}_{i}[\textsc{m}^{\prime\prime}]$
with $\ell$ fresh. Since memory does not change applying rule (t-conf) we
obtain the thesis.

(ctx):

We have $\mathit{e}={\cal{E}}[\mathit{e}_{1}]$ and
$\mathit{e}^{\prime}={\cal{E}}[\mathit{e}^{\prime}_{1}]$ and
${\mathit{e}_{1}{\mid}\mu\rightarrow\mathit{e}_{1}^{\prime}{\mid}\mu^{\prime}}$
and $\Gamma_{1}\vdash{\cal{E}}[\mathit{e}_{1}]:\mathit{T}$.

We prove the thesis by induction on evaluation context ${\cal{E}}$ and we show
only the relevant cases:

  * •:

${\cal{E}}=[\ ]$ We know that
$\Gamma\vdash{\cal{E}}[\mathit{e}_{1}]{\mid}\mu:\mathit{T}$ and that
${\cal{E}}[\mathit{e}_{1}]=\mathit{e}_{1}$, so
$\Gamma\vdash\mathit{e}_{1}{\mid}\mu:\mathit{T}$. Applying the primary
induction hypothesis to
${\mathit{e}_{1}{\mid}\mu\rightarrow\mathit{e}_{1}^{\prime}{\mid}\mu^{\prime}}$
and $\Gamma\vdash\mathit{e}_{1}{\mid}\mu:\mathit{T}$ and by knowing that
${\cal{E}}[\mathit{e}^{\prime}_{1}]=\mathit{e}^{\prime}_{1}$ we obtain the
thesis.

  * •:

${\cal{E}}={\cal{E}}^{\prime}\texttt{.}\mathit{f}\texttt{=}\,\mathit{e}^{\prime}$
By Lemma B.2 we know that exists a context $\Gamma_{1}^{\prime}$ such that
$\Gamma_{1}^{\prime}\blacktriangleleft\Gamma_{1}$ and a derivation ${\cal
D}^{\prime}:\Gamma_{1}^{\prime}\vdash{\cal{E}}[\mathit{e}_{1}]:\mathit{T}^{\prime}$
ending with a syntax directed rule. We know that the last applied rule in
${\cal D}^{\prime}$ must be (t-assign), so we know
$\Gamma_{1}^{\prime}=\Gamma_{1}^{\prime\prime}+\Gamma_{2}^{\prime\prime}$ such
that
$\Gamma_{1}^{\prime\prime}\vdash{\cal{E}}^{\prime}[\mathit{e}_{1}]:\mathit{C}^{\mathsf{mut}}$
and $\Gamma_{2}^{\prime\prime}\vdash\mathit{e}^{\prime}:\mathit{T}_{i}$ with
$\mathsf{fields}(\mathit{C})=\mathit{T}_{1}\
\mathit{f}_{1}\texttt{;}\ldots\mathit{T}_{n}\ \mathit{f}_{n}\texttt{;}$ and
$i\in 1..n$. We can apply rule (t-conf) to obtain
$\Gamma_{1}^{\prime\prime}+\Gamma_{2}\vdash{\cal{E}}^{\prime}[\mathit{e}_{1}]{\mid}\mu:\mathit{C}^{\mathsf{mut}}$.
By (ctx) we have
${{\cal{E}}^{\prime}[\mathit{e}_{1}]{\mid}\mu\rightarrow{\cal{E}}^{\prime}[\mathit{e}^{\prime}_{1}]{\mid}\mu^{\prime}}$.
By secondary induction hypothesis on this and on
$\Gamma_{1}^{\prime\prime}+\Gamma_{2}\vdash{\cal{E}}^{\prime}[\mathit{e}_{1}]{\mid}\mu:\mathit{C}^{\mathsf{mut}}$
we have that
$\Theta^{\prime}\vdash{\cal{E}}^{\prime}[\mathit{e}^{\prime}_{1}]{\mid}\mu^{\prime}:\mathit{C}^{\mathsf{mut}}$
such that

    * –:

$(\mathsf{erase}(\Gamma_{1}^{\prime\prime}+\Gamma_{2})+\mathsf{erase}(\Theta^{\prime})){\upharpoonright}\mathsf{erase}(\Gamma_{1}^{\prime\prime}+\Gamma_{2})=\mathsf{erase}(\Gamma_{1}^{\prime\prime}+\Gamma_{2})$,

    * –:

for all $\mathit{x}\in\mathsf{dom}(\Gamma_{1}^{\prime\prime}+\Gamma_{2})$,
$\mathsf{modif}(\Gamma_{1}^{\prime\prime}+\Gamma_{2},\mathit{x})\leq\mathsf{modif}(\Theta^{\prime},\mathit{x})$

By rule (t-conf) we have
$\Theta^{\prime}=\Delta^{\prime}_{1}+\Gamma^{\prime}_{2}$ such that
$\Delta^{\prime}_{1}\vdash{\cal{E}}^{\prime}[\mathit{e}^{\prime}_{1}]:\mathit{T}^{\prime}$
and $\Gamma^{\prime}_{2}\vdash\mu^{\prime}$. By rule (t-assign) we have
$\Delta^{\prime}_{1}+\Delta_{2}\vdash{\cal{E}}[e^{\prime}_{1}]:\mathit{T}^{\prime}$.
We can prove that

    * –:

for all
$\mathit{x}\in(\mathsf{dom}(\Gamma^{\prime}_{1})\cap\mathsf{dom}(\Delta^{\prime}_{1}+\Delta_{2}))$,
$\mathsf{modif}(\Gamma^{\prime}_{1},\mathit{x})\leq\mathsf{modif}(\Delta^{\prime}_{1}+\Delta_{2},\mathit{x})$

Applying the same non syntax directed rules applied to
$\Gamma_{1}^{\prime}\vdash{\cal{E}}[\mathit{e}_{1}]:\mathit{T}^{\prime}$ and
rule (t-conf), by the lemma Lemma B.3 we obtain the thesis.

  * •:

${\cal{E}}=\\{\mathit{T}_{\mathit{x}}\,\mathit{x}={\cal{E}}^{\prime}\texttt{;}\,\mathit{e}^{\prime}\\}$
By Lemma B.2 we know that exists a context $\Gamma_{1}^{\prime}$ such that
$\Gamma_{1}^{\prime}\blacktriangleleft\Gamma_{1}$ and a derivation ${\cal
D}^{\prime}:\Gamma_{1}^{\prime}\vdash{\cal{E}}[\mathit{e}_{1}]:\mathit{T}^{\prime}$
ending with a syntax directed rule. We know that the last applied rule in
${\cal D}^{\prime}$ must be (t-block), so we know
$\Gamma_{1}^{\prime}=((\mathit{X}\cup\\{\ell\\})\times\Gamma_{1}^{\prime\prime})\oplus\Gamma_{2}^{\prime\prime}$
such that
$\Gamma_{1}^{\prime\prime}\vdash{\cal{E}}^{\prime}[\mathit{e}_{1}]:\mathit{T}_{\mathit{x}}$
and
$\Gamma_{2}^{\prime\prime},\mathit{x}:_{\mathit{X}}\mathit{T}_{\mathit{x}}\vdash\mathit{e}^{\prime}:\mathit{T}_{i}$.
We can apply rule (t-conf) to obtain
$\Gamma_{1}^{\prime\prime}+\Gamma_{2}\vdash{\cal{E}}^{\prime}[\mathit{e}_{1}]{\mid}\mu:\mathit{T}_{\mathit{x}}$.
By (ctx) we have
${{\cal{E}}^{\prime}[\mathit{e}_{1}]{\mid}\mu\rightarrow{\cal{E}}^{\prime}[\mathit{e}^{\prime}_{1}]{\mid}\mu^{\prime}}$.
By secondary induction hypothesis on this and on
$\Gamma_{1}^{\prime\prime}+\Gamma_{2}\vdash{\cal{E}}^{\prime}[\mathit{e}_{1}]{\mid}\mu:\mathit{T}_{z}$
we have that
$\Theta^{\prime}\vdash{\cal{E}}^{\prime}[\mathit{e}^{\prime}_{1}]{\mid}\mu^{\prime}:\mathit{T}_{z}$
such that

    * –:

$(\mathsf{erase}(\Gamma_{1}^{\prime\prime}+\Gamma_{2})+\mathsf{erase}(\Theta^{\prime})){\upharpoonright}\mathsf{erase}(\Gamma_{1}^{\prime\prime}+\Gamma_{2})=\mathsf{erase}(\Gamma_{1}^{\prime\prime}+\Gamma_{2})$,

    * –:

for all $\mathit{x}\in\mathsf{dom}(\Gamma_{1}^{\prime\prime}+\Gamma_{2})$,
$\mathsf{modif}(\Gamma_{1}^{\prime\prime}+\Gamma_{2},\mathit{x})\leq\mathsf{modif}(\Theta^{\prime},\mathit{x})$

By rule (t-conf) we have
$\Theta^{\prime}=\Delta^{\prime}_{1}+\Gamma^{\prime}_{2}$ such that
$\Delta^{\prime}_{1}\vdash{\cal{E}}^{\prime}[\mathit{e}^{\prime}_{1}]:\mathit{T}^{\prime}$
and $\Gamma^{\prime}_{2}\vdash\mu^{\prime}$. By rule (t-block) we have
$((\mathit{X}\cup\\{\ell\\})\times\Delta^{\prime}_{1})\oplus\Gamma_{2}^{\prime\prime}\vdash{\cal{E}}[e^{\prime}_{1}]:\mathit{T}^{\prime}$.
We can prove that

    * –:

for all
$\mathit{x}\in(\mathsf{dom}(\Gamma^{\prime}_{1})\cap\mathsf{dom}(((\mathit{X}\cup\\{\ell\\})\times\Delta^{\prime}_{1})\oplus\Gamma_{2}^{\prime\prime}))$,
$\mathsf{modif}(\Gamma^{\prime}_{1},\mathit{x})\leq\mathsf{modif}(((\mathit{X}\cup\\{\ell\\})\times\Delta^{\prime}_{1})\oplus\Gamma_{2}^{\prime\prime},\mathit{x})$

Applying the same non syntax directed rules applied to
$\Gamma_{1}^{\prime}\vdash{\cal{E}}[\mathit{e}_{1}]:\mathit{T}^{\prime}$ and
rule (t-conf), by the lemma Lemma B.3 we obtain the thesis.

∎

##  Appendix C Module of fixpoints

###### Definition C.1 (Idempotent).

A homomorphism $\beta\colon\mathcal{M}\rightarrow\mathcal{M}$ is _idempotent_
if $\beta\circ\beta=\beta$.

Let $\beta\colon\mathcal{M}\rightarrow\mathcal{M}$ be an idempotent
homomorphism on the $\mathcal{R}$-module $\mathcal{M}$, and consider the
subset ${M_{\beta}=\\{u\in M\mid\beta(u)=u\\}}$ of fixpoints of $\beta$.
Define the following operations, for all $u,v\in M_{\beta}$ and $r\in R$:

$u+^{\beta}v:=\beta(u+v)\qquad\mathbf{0}^{\beta}:=\beta(\mathbf{0})\qquad
r\times^{\beta}u:=\beta(r\times u)$

We can prove the following result

###### Proposition C.2.

$\mathcal{M}_{\beta}=\langle
M_{\beta},\preceq,+^{\beta},\mathbf{0}^{\beta},\times^{\beta}\rangle$ is an
$\mathcal{R}$-module.

###### Proof.

All the operations are trivially well-defined as $\beta$ is idempotent.
Moreover, note that, since $\beta$ is an homomorphism, we have
$\mathbf{0}^{\beta}=\beta(\mathbf{0})=\mathbf{0}$. We check the module axioms.

$\displaystyle\text{associativity of }+^{\beta}$ $\displaystyle
u+^{\beta}(v+^{\beta}w)$
$\displaystyle=\beta(u+\beta(v+w))=\beta(\beta(u)+\beta(v+w))$
$\displaystyle\preceq\beta(\beta(u+v+w))=\beta(u+v+w)$
$\displaystyle=\beta(\beta(u)+\beta(v)+w)\preceq\beta(\beta(u+v)+w)$
$\displaystyle=(u+^{\beta}v)+^{\beta}w$ $\displaystyle(u+^{\beta}v)+^{\beta}w$
$\displaystyle=\beta(\beta(u+v)+w)=\beta(\beta(u+v)+\beta(w))$
$\displaystyle\preceq\beta(\beta(u+v+w))=\beta(u+v+w)$
$\displaystyle=\beta(u+\beta(v)+\beta(w))\preceq\beta(u+\beta(v+w))$
$\displaystyle=u+^{\beta}(v+^{\beta}w)$ $\displaystyle\text{commutativity of
}+^{\beta}$ $\displaystyle u+^{\beta}v$
$\displaystyle=\beta(u+v)=\beta(v+u)=v+^{\beta}u$
$\displaystyle\text{neutrality of }\mathbf{0}^{\beta}$ $\displaystyle
u+^{\beta}\mathbf{0}^{\beta}$
$\displaystyle=\beta(u+\beta(\mathbf{0}))=\beta(u+\mathbf{0})=\beta(u)=u$
$\displaystyle\text{linearity of }\times^{\beta}$ $\displaystyle
r\times^{\beta}(u+^{\beta}v)$
$\displaystyle=\beta(r\times\beta(u+v))=\beta(\beta(r\times(u+v)))$
$\displaystyle=\beta(r\times(u+v))=\beta(r\times u+r\times v)$
$\displaystyle=\beta(r\times\beta(u)+r\times\beta(v))=\beta(\beta(r\times
u)+\beta(r\times v))$
$\displaystyle=r\times^{\beta}u+^{\beta}r\times^{\beta}v$ $\displaystyle
r\times^{\beta}\mathbf{0}^{\beta}$
$\displaystyle=\beta(r\times\beta(\mathbf{0}))=\beta(r\times\mathbf{0})=\beta(\mathbf{0})=\mathbf{0}^{\beta}$
$\displaystyle(r+s)\times^{\beta}u$ $\displaystyle=\beta((r+s)\times
u)=\beta(r\times u+s\times u)$
$\displaystyle=\beta(r\times\beta(u)+s\times\beta(u))=\beta(\beta(r\times
u)+\beta(s\times u))$
$\displaystyle=r\times^{\beta}u+^{\beta}s\times^{\beta}u$ $\displaystyle
0\times^{\beta}u$ $\displaystyle=\beta(0\times
u)=\beta(\mathbf{0})=\mathbf{0}^{\beta}$ $\displaystyle(r\times
s)\times^{\beta}u$ $\displaystyle=\beta((r\times s)\times
u)=\beta(r\times(s\times u))$
$\displaystyle=\beta(r\times(s\times\beta(u))=\beta(r\times\beta(s\times u))$
$\displaystyle=r\times^{\beta}(s\times^{\beta}u)$ $\displaystyle
1\times^{\beta}u$ $\displaystyle=\beta(1\times u)=\beta(u)=u$

∎