* [37] Reinhard Munz, Fabienne Eigner, Matteo Maffei, Paul Francis, and Deepak Garg.  Unitrax: Protecting data privacy with discoverable biases.  In Lujo Bauer and Ralf Küsters, editors, Principles of Security and Trust, pages 278–299, Cham, 2018. Springer International Publishing.
  * [38] Chaya Nayak.  New privacy-protected facebook data for independent research on social media’s impact on democracy, Feb 2020.
  * [39] Joseph P Near, David Darais, Chike Abuah, Tim Stevens, Pranav Gaddamadugu, Lun Wang, Neel Somani, Mu Zhang, Nikhil Sharma, Alex Shan, et al.  Duet: an expressive higher-order language and linear type system for statically enforcing differential privacy.  Proceedings of the ACM on Programming Languages, 3(OOPSLA):1–30, 2019.
  * [40] Jason Reed and Benjamin C Pierce.  Distance makes the types grow stronger: a calculus for differential privacy.  In Proceedings of the 15th ACM SIGPLAN international conference on Functional programming, pages 157–168, 2010.
  * [41] Ryan M. Rogers, Salil P. Vadhan, Aaron Roth, and Jonathan Ullman.  Privacy odometers and filters: Pay-as-you-go composition.  In Daniel D. Lee, Masashi Sugiyama, Ulrike von Luxburg, Isabelle Guyon, and Roman Garnett, editors, Advances in Neural Information Processing Systems 29: Annual Conference on Neural Information Processing Systems 2016, December 5-10, 2016, Barcelona, Spain, pages 1921–1929, 2016.
  * [42] Andrei Sabelfeld and David Sands.  A per model of secure information flow in sequential programs.  In S. Doaitse Swierstra, editor, Programming Languages and Systems, pages 40–58, Berlin, Heidelberg, 1999. Springer Berlin Heidelberg.
  * [43] T. Sato, G. Barthe, M. Gaboardi, J. Hsu, and S. Katsumata.  Approximate span liftings: Compositional semantics for relaxations of differential privacy.  In 2019 34th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pages 1–14, June 2019.
  * [44] J. Vaidya, B. Shafiq, A. Basu, and Y. Hong.  Differentially private naive bayes classification.  In 2013 IEEE/WIC/ACM International Joint Conferences on Web Intelligence (WI) and Intelligent Agent Technologies (IAT), volume 1, pages 571–576, 2013.
  * [45] Yuxin Wang, Zeyu Ding, Daniel Kifer, and Danfeng Zhang.  Checkdp: An automated and integrated approach for proving differential privacy or finding precise counterexamples.  In Proceedings of the 2020 ACM SIGSAC Conference on Computer and Communications Security, pages 919–938, 2020.
  * [46] Yuxin Wang, Zeyu Ding, Guanhong Wang, Daniel Kifer, and Danfeng Zhang.  Proving differential privacy with shadow execution.  In Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, pages 655–669, 2019.
  * [47] Royce J. Wilson, Celia Yuxin Zhang, William Lam, Damien Desfontaines, Daniel Simmons-Marengo, and Bryant Gipson.  Differentially private SQL with bounded user contribution.  CoRR, abs/1909.01917, 2019.
  * [48] Royce J Wilson, Celia Yuxing Zhang, William Lam, Damien Desfontaines, Daniel Simmons-Marengo, and Bryant Gipson.  Differentially private sql with bounded user contribution.  Proceedings on Privacy Enhancing Technologies, 2020(2), 2020.
  * [49] Daniel Winograd-Cort, Andreas Haeberlen, Aaron Roth, and Benjamin C. Pierce.  A framework for adaptive differential privacy.  Proc. ACM Program. Lang., 1(ICFP):10:1–10:29, 2017.
  * [50] Dan Zhang, Ryan McKenna, Ios Kotsogiannis, Michael Hay, Ashwin Machanavajjhala, and Gerome Miklau.  Ektelo: A framework for defining differentially-private computations.  In Proceedings of the 2018 International Conference on Management of Data, pages 115–130, 2018.
  * [51] Danfeng Zhang and Daniel Kifer.  Lightdp: towards automating differential privacy proofs.  In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, pages 888–901, 2017.
  * [52] Hengchu Zhang, Edo Roth, Andreas Haeberlen, Benjamin C Pierce, and Aaron Roth.  Fuzzi: A three-level logic for differential privacy.  Proceedings of the ACM on Programming Languages, 3(ICFP):1–28, 2019\.
  * [53] Úlfar Erlingsson, Vasyl Pihur, and Aleksandra Korolova.  Rappor: Randomized aggregatable privacy-preserving ordinal response.  In Proceedings of the 21st ACM Conference on Computer and Communications Security, Scottsdale, Arizona, 2014.

##  Appendix A Lemmas, Theorems & Proofs

######  Lemma A.1 (Plus Respects).

If $\mathit{r_{1}\sim_{m}^{r}r_{2}}$ Then
$\mathit{(r_{1}+r_{3})\sim_{m}^{r}(r_{2}+r_{3})}$.

###### Proof.

By unfolding definitions and simple arithmetic. ∎

######  Lemma A.2 (Times Respects).

If $\mathit{r_{1}\sim_{m}^{r}r_{2}}$ then $\mathit{(r_{1}\times
r_{3})\sim_{m}^{r_{3}r}(r_{2}\times r_{3})}$.

###### Proof.

By unfolding definitions and simple arithmetic. ∎

######  Lemma A.3 (Triangle).

If $\mathit{r_{1}\sim^{r_{A}}_{m_{A}}r_{2}}$ and
$\mathit{r_{2}\sim^{r_{B}}_{m_{B}}r_{3}}$ then
$\mathit{r_{1}\sim^{r_{A}+r_{B}}_{m_{A}\sqcup m_{B}}r_{3}}$.

###### Proof.

By unfolding definitions, simple arithmetic, and the standard triangle
inequality property for real numbers. ∎

######  Lemma A.4 (Real Metric Weakening).

If $\mathit{r_{1}\sim^{r}mr_{2}}$, $\mathit{r\leq r^{\prime}}$ and
$\mathit{m\sqsubseteq m^{\prime}}$ then
$\mathit{r_{1}\sim^{r^{\prime}}_{m^{\prime}}r_{2}}$.

###### Proof.

By unfolding definitions and simple arithmetic. ∎

######  Lemma A.5 (Step-index Weakening).

For $\mathit{n^{\prime}\leq n}$: (1): If
$\mathit{\rho_{1}\sim_{n}^{\Sigma}\rho_{2}}$ then
$\mathit{\rho_{1}\sim_{n^{\prime}}^{\Sigma}\rho_{2}}$; (2): If
$\mathit{\sigma_{1}\sim_{n}^{\Sigma}\sigma_{2}}$ then
$\mathit{\sigma_{1}\sim_{n^{\prime}}^{\Sigma}\sigma_{2}}$; and (3): If
$\mathit{\rho_{1},\sigma_{1},e_{1}\sim_{n}^{\Sigma}\rho_{2},\sigma_{2},e_{2}}$
then
$\mathit{\rho_{1},\sigma_{1},e_{1}\sim_{n^{\prime}}^{\Sigma}\rho_{2},\sigma_{2},e_{2}}$.

###### Proof.

By mutual induction on $\mathit{n}$ for all three properties, and additionally
case analysis on $\mathit{e_{1}}$ and $\mathit{e_{2}}$ for property (3). ∎

######  Theorem A.6 (Metric Preservation).

  * If: | $\mathit{\rho_{1}\sim_{n}^{\Sigma}\rho_{2}}$ | (H1)
---|---|---
And: | $\mathit{\sigma_{1}\sim_{n}^{\Sigma}\sigma_{2}}$ | (H2)
Then: | $\mathit{\rho_{1},\sigma_{1},e\sim_{n}^{\Sigma}\rho_{2},\sigma_{2},e}$ |

  *   * That is, either $\mathit{n=0}$ or $\mathit{n=n^{\prime}+1}$ and…

  *   * If: | $\mathit{n_{1}\leq n^{\prime}}$ | (H3)
---|---|---
And: | $\mathit{\rho_{1}\vdash\mathrlap{\raisebox{-5.0pt}{\color[rgb]{0.5,0.5,0.5}$\llcorner$}}\mathrlap{\raisebox{6.0pt}{\color[rgb]{0.5,0.5,0.5}$\ulcorner$}}\hskip 2.0pt\vphantom{\underset{x}{\overset{X}{X}}}\sigma_{1},e\hskip 2.0pt\mathllap{\raisebox{-5.0pt}{\color[rgb]{0.5,0.5,0.5}$\lrcorner$}}\mathllap{\raisebox{6.0pt}{\color[rgb]{0.5,0.5,0.5}$\urcorner$}}\vphantom{\underset{x}{\overset{X}{X}}}\Downarrow_{n_{1}}\mathrlap{\raisebox{-5.0pt}{\color[rgb]{0.5,0.5,0.5}$\llcorner$}}\mathrlap{\raisebox{6.0pt}{\color[rgb]{0.5,0.5,0.5}$\ulcorner$}}\hskip 2.0pt\vphantom{\underset{x}{\overset{X}{X}}}\sigma_{1}^{\prime},v_{1}\hskip 2.0pt\mathllap{\raisebox{-5.0pt}{\color[rgb]{0.5,0.5,0.5}$\lrcorner$}}\mathllap{\raisebox{6.0pt}{\color[rgb]{0.5,0.5,0.5}$\urcorner$}}\vphantom{\underset{x}{\overset{X}{X}}}}$ | (H4)
And: | $\mathit{\rho_{2}\vdash\mathrlap{\raisebox{-5.0pt}{\color[rgb]{0.5,0.5,0.5}$\llcorner$}}\mathrlap{\raisebox{6.0pt}{\color[rgb]{0.5,0.5,0.5}$\ulcorner$}}\hskip 2.0pt\vphantom{\underset{x}{\overset{X}{X}}}\sigma_{2},e\hskip 2.0pt\mathllap{\raisebox{-5.0pt}{\color[rgb]{0.5,0.5,0.5}$\lrcorner$}}\mathllap{\raisebox{6.0pt}{\color[rgb]{0.5,0.5,0.5}$\urcorner$}}\vphantom{\underset{x}{\overset{X}{X}}}\Downarrow_{n_{2}}\mathrlap{\raisebox{-5.0pt}{\color[rgb]{0.5,0.5,0.5}$\llcorner$}}\mathrlap{\raisebox{6.0pt}{\color[rgb]{0.5,0.5,0.5}$\ulcorner$}}\hskip 2.0pt\vphantom{\underset{x}{\overset{X}{X}}}\sigma_{2}^{\prime},v_{2}\hskip 2.0pt\mathllap{\raisebox{-5.0pt}{\color[rgb]{0.5,0.5,0.5}$\lrcorner$}}\mathllap{\raisebox{6.0pt}{\color[rgb]{0.5,0.5,0.5}$\urcorner$}}\vphantom{\underset{x}{\overset{X}{X}}}}$ | (H5)
Then: | $\mathit{n_{1}=n_{2}}$ | (C1)
And: | $\mathit{\sigma_{1}^{\prime}\sim^{\Sigma}_{n^{\prime}-n_{1}}\sigma_{2}^{\prime}}$ | (C2)
And: | $\mathit{v_{1}\sim^{\Sigma}_{n^{\prime}-n_{1}}v_{2}}$ | (C3)

###### Proof.

See detailed proof later in this section. ∎

######  Corollary A.6.1 (Sound Dynamic Analysis for Sensitivity).

If: |  $\mathit{n_{1}<n}$, $\mathit{n_{2}<n}$ and $\mathit{n_{3}<n}$ | (H1)
---|---|---
And: | $\mathit{\rho\sim_{n}^{\\{o\mapsto\infty\\}}\rho_{1}}$ | (H2)
And: | $\mathit{\rho\vdash\mathrlap{\raisebox{-5.0pt}{\color[rgb]{0.5,0.5,0.5}$\llcorner$}}\mathrlap{\raisebox{6.0pt}{\color[rgb]{0.5,0.5,0.5}$\ulcorner$}}\hskip 2.0pt\vphantom{\underset{x}{\overset{X}{X}}}\varnothing,e\hskip 2.0pt\mathllap{\raisebox{-5.0pt}{\color[rgb]{0.5,0.5,0.5}$\lrcorner$}}\mathllap{\raisebox{6.0pt}{\color[rgb]{0.5,0.5,0.5}$\urcorner$}}\vphantom{\underset{x}{\overset{X}{X}}}\Downarrow_{n_{1}}\mathrlap{\raisebox{-5.0pt}{\color[rgb]{0.5,0.5,0.5}$\llcorner$}}\mathrlap{\raisebox{6.0pt}{\color[rgb]{0.5,0.5,0.5}$\ulcorner$}}\hskip 2.0pt\vphantom{\underset{x}{\overset{X}{X}}}\sigma,r@_{m}^{\Sigma}\hskip 2.0pt\mathllap{\raisebox{-5.0pt}{\color[rgb]{0.5,0.5,0.5}$\lrcorner$}}\mathllap{\raisebox{6.0pt}{\color[rgb]{0.5,0.5,0.5}$\urcorner$}}\vphantom{\underset{x}{\overset{X}{X}}}}$ | (H3)
And: | $\mathit{\rho_{1}\sim^{\Sigma^{\prime}}_{n}\rho_{2}}$ | (H4)
And: | $\mathit{\rho_{1}\vdash\mathrlap{\raisebox{-5.0pt}{\color[rgb]{0.5,0.5,0.5}$\llcorner$}}\mathrlap{\raisebox{6.0pt}{\color[rgb]{0.5,0.5,0.5}$\ulcorner$}}\hskip 2.0pt\vphantom{\underset{x}{\overset{X}{X}}}\varnothing,e\hskip 2.0pt\mathllap{\raisebox{-5.0pt}{\color[rgb]{0.5,0.5,0.5}$\lrcorner$}}\mathllap{\raisebox{6.0pt}{\color[rgb]{0.5,0.5,0.5}$\urcorner$}}\vphantom{\underset{x}{\overset{X}{X}}}\Downarrow_{n_{2}}\mathrlap{\raisebox{-5.0pt}{\color[rgb]{0.5,0.5,0.5}$\llcorner$}}\mathrlap{\raisebox{6.0pt}{\color[rgb]{0.5,0.5,0.5}$\ulcorner$}}\hskip 2.0pt\vphantom{\underset{x}{\overset{X}{X}}}\sigma_{1},r_{1}@^{\Sigma_{1}}_{m_{1}}\hskip 2.0pt\mathllap{\raisebox{-5.0pt}{\color[rgb]{0.5,0.5,0.5}$\lrcorner$}}\mathllap{\raisebox{6.0pt}{\color[rgb]{0.5,0.5,0.5}$\urcorner$}}\vphantom{\underset{x}{\overset{X}{X}}}}$ | (H5)
And: | $\mathit{\rho_{2}\vdash\mathrlap{\raisebox{-5.0pt}{\color[rgb]{0.5,0.5,0.5}$\llcorner$}}\mathrlap{\raisebox{6.0pt}{\color[rgb]{0.5,0.5,0.5}$\ulcorner$}}\hskip 2.0pt\vphantom{\underset{x}{\overset{X}{X}}}\varnothing,e\hskip 2.0pt\mathllap{\raisebox{-5.0pt}{\color[rgb]{0.5,0.5,0.5}$\lrcorner$}}\mathllap{\raisebox{6.0pt}{\color[rgb]{0.5,0.5,0.5}$\urcorner$}}\vphantom{\underset{x}{\overset{X}{X}}}\Downarrow_{n_{3}}\mathrlap{\raisebox{-5.0pt}{\color[rgb]{0.5,0.5,0.5}$\llcorner$}}\mathrlap{\raisebox{6.0pt}{\color[rgb]{0.5,0.5,0.5}$\ulcorner$}}\hskip 2.0pt\vphantom{\underset{x}{\overset{X}{X}}}\sigma_{2},r_{2}@^{\Sigma_{2}}_{m_{2}}\hskip 2.0pt\mathllap{\raisebox{-5.0pt}{\color[rgb]{0.5,0.5,0.5}$\lrcorner$}}\mathllap{\raisebox{6.0pt}{\color[rgb]{0.5,0.5,0.5}$\urcorner$}}\vphantom{\underset{x}{\overset{X}{X}}}}$ | (H6)
Then: | $\mathit{r_{1}\sim^{\Sigma^{\prime}\mathord{\cdotp}\Sigma}_{m_{1}}r_{2}}$ | (C1)

###### Proof.

  * By  (Metric Preservation)., (H2), (H1), (H3) and (H5) we have $\mathit{\Sigma_{1}=\Sigma}$ and $\mathit{m_{1}=m}$.

  * By  (Metric Preservation)., (H4), (H1), (H5) and (H6) we have proved the goal (C1).

∎

###### Proof of  (Metric Preservation)..

By strong induction on $\mathit{n}$ and case analysis on $\mathit{e}$:

  * -

    * Case $\mathit{n=0}$: Trivial by definition.

  * -

    * Case $\mathit{n=n+1}$ and $\mathit{e=x}$:

    * By inversion on (H4) and (H5) we have: $\mathit{n_{1}=n_{2}=0}$, $\mathit{\sigma_{1}^{\prime}=\sigma_{1}}$, $\mathit{\sigma_{2}^{\prime}=\sigma_{2}}$, $\mathit{v_{1}=\rho_{1}(x)}$ and $\mathit{v_{2}=\rho_{2}(x)}$. To show: (C1): $\mathit{0=0}$; (C2): $\mathit{\sigma_{1}\sim_{n}^{\Sigma}\sigma_{2}}$; and (C3): $\mathit{\rho_{1}(x)\sim_{n}^{\Sigma}\rho_{2}(x)}$. (C1) is trivial. (C2) is immediate by (H2). (C3) is immediate by (H1).

  * -

    * Case $\mathit{n=n+1}$ and $\mathit{e=r}$:

    * By inversion on (H4) and (H5) we have $\mathit{n_{1}=n_{2}=0}$, $\mathit{v_{1}=v_{2}=r@_{{{\color[rgb]{0.340625,0.1125,0.471875}\texttt{disc}}}}^{{\textbf{Z}}}}$, $\mathit{\sigma_{1}^{\prime}=\sigma_{1}}$ and $\mathit{\sigma_{2}^{\prime}=\sigma_{2}}$. To show: (C1): $\mathit{0=0}$; (C2): $\mathit{\sigma_{1}\sim_{n}^{\Sigma}\sigma_{2}}$; and (C3): $\mathit{r\sim_{{{\color[rgb]{0.340625,0.1125,0.471875}\texttt{disc}}}}^{0}r}$. (C1) is trivial. (C2) is immediate by (H2). (C3) is immediate by definition of relation $\mathit{\sim_{m}^{r}}$.

  * -

    * Case $\mathit{n=n+1}$ and $\mathit{e=e_{1}+e_{2}}$:

    * By inversion on (H4) and (H5) we have:

    *<EMAIL_ADDRESS>}\rho_{1}&{}\vdash{}&\mathrlap{\raisebox{-5.0pt}{\color[rgb]{0.5,0.5,0.5}$\llcorner$}}\mathrlap{\raisebox{6.0pt}{\color[rgb]{0.5,0.5,0.5}$\ulcorner$}}\hskip 2.0pt\vphantom{\underset{x}{\overset{X}{X}}}\sigma_{1}&{},{}&e_{1}\hskip 2.0pt\mathllap{\raisebox{-5.0pt}{\color[rgb]{0.5,0.5,0.5}$\lrcorner$}}\mathllap{\raisebox{6.0pt}{\color[rgb]{0.5,0.5,0.5}$\urcorner$}}\vphantom{\underset{x}{\overset{X}{X}}}&{}\Downarrow_{n_{11}}{}&\mathrlap{\raisebox{-5.0pt}{\color[rgb]{0.5,0.5,0.5}$\llcorner$}}\mathrlap{\raisebox{6.0pt}{\color[rgb]{0.5,0.5,0.5}$\ulcorner$}}\hskip 2.0pt\vphantom{\underset{x}{\overset{X}{X}}}\sigma_{1}^{\prime}&{},{}&r_{11}@^{\Sigma_{11}}_{m_{11}}\hskip 2.0pt\mathllap{\raisebox{-5.0pt}{\color[rgb]{0.5,0.5,0.5}$\lrcorner$}}\mathllap{\raisebox{6.0pt}{\color[rgb]{0.5,0.5,0.5}$\urcorner$}}\vphantom{\underset{x}{\overset{X}{X}}}\hfil\hskip 10.00002pt&{{\color[rgb]{0,0,0}\textnormal{{{(H4.1)}}}}}\cr\rho_{1}&{}\vdash{}&\mathrlap{\raisebox{-5.0pt}{\color[rgb]{0.5,0.5,0.5}$\llcorner$}}\mathrlap{\raisebox{6.0pt}{\color[rgb]{0.5,0.5,0.5}$\ulcorner$}}\hskip 2.0pt\vphantom{\underset{x}{\overset{X}{X}}}\sigma_{1}^{\prime}&{},{}&e_{2}\hskip 2.0pt\mathllap{\raisebox{-5.0pt}{\color[rgb]{0.5,0.5,0.5}$\lrcorner$}}\mathllap{\raisebox{6.0pt}{\color[rgb]{0.5,0.5,0.5}$\urcorner$}}\vphantom{\underset{x}{\overset{X}{X}}}&{}\Downarrow_{n_{12}}{}&\mathrlap{\raisebox{-5.0pt}{\color[rgb]{0.5,0.5,0.5}$\llcorner$}}\mathrlap{\raisebox{6.0pt}{\color[rgb]{0.5,0.5,0.5}$\ulcorner$}}\hskip 2.0pt\vphantom{\underset{x}{\overset{X}{X}}}\sigma_{1}^{\prime\prime}&{},{}&r_{12}@^{\Sigma_{12}}_{m_{12}}\hskip 2.0pt\mathllap{\raisebox{-5.0pt}{\color[rgb]{0.5,0.5,0.5}$\lrcorner$}}\mathllap{\raisebox{6.0pt}{\color[rgb]{0.5,0.5,0.5}$\urcorner$}}\vphantom{\underset{x}{\overset{X}{X}}}\hfil\hskip 10.00002pt&{{\color[rgb]{0,0,0}\textnormal{{{(H4.2)}}}}}\cr\rho_{2}&{}\vdash{}&\mathrlap{\raisebox{-5.0pt}{\color[rgb]{0.5,0.5,0.5}$\llcorner$}}\mathrlap{\raisebox{6.0pt}{\color[rgb]{0.5,0.5,0.5}$\ulcorner$}}\hskip 2.0pt\vphantom{\underset{x}{\overset{X}{X}}}\sigma_{2}&{},{}&e_{1}\hskip 2.0pt\mathllap{\raisebox{-5.0pt}{\color[rgb]{0.5,0.5,0.5}$\lrcorner$}}\mathllap{\raisebox{6.0pt}{\color[rgb]{0.5,0.5,0.5}$\urcorner$}}\vphantom{\underset{x}{\overset{X}{X}}}&{}\Downarrow_{n_{21}}{}&\mathrlap{\raisebox{-5.0pt}{\color[rgb]{0.5,0.5,0.5}$\llcorner$}}\mathrlap{\raisebox{6.0pt}{\color[rgb]{0.5,0.5,0.5}$\ulcorner$}}\hskip 2.0pt\vphantom{\underset{x}{\overset{X}{X}}}\sigma_{2}^{\prime}&{},{}&r_{21}@^{\Sigma_{21}}_{m_{21}}\hskip 2.0pt\mathllap{\raisebox{-5.0pt}{\color[rgb]{0.5,0.5,0.5}$\lrcorner$}}\mathllap{\raisebox{6.0pt}{\color[rgb]{0.5,0.5,0.5}$\urcorner$}}\vphantom{\underset{x}{\overset{X}{X}}}\hfil\hskip 10.00002pt&{{\color[rgb]{0,0,0}\textnormal{{{(H5.1)}}}}}\cr\rho_{2}&{}\vdash{}&\mathrlap{\raisebox{-5.0pt}{\color[rgb]{0.5,0.5,0.5}$\llcorner$}}\mathrlap{\raisebox{6.0pt}{\color[rgb]{0.5,0.5,0.5}$\ulcorner$}}\hskip 2.0pt\vphantom{\underset{x}{\overset{X}{X}}}\sigma_{2}^{\prime}&{},{}&e_{2}\hskip 2.0pt\mathllap{\raisebox{-5.0pt}{\color[rgb]{0.5,0.5,0.5}$\lrcorner$}}\mathllap{\raisebox{6.0pt}{\color[rgb]{0.5,0.5,0.5}$\urcorner$}}\vphantom{\underset{x}{\overset{X}{X}}}&{}\Downarrow_{n_{22}}{}&\mathrlap{\raisebox{-5.0pt}{\color[rgb]{0.5,0.5,0.5}$\llcorner$}}\mathrlap{\raisebox{6.0pt}{\color[rgb]{0.5,0.5,0.5}$\ulcorner$}}\hskip 2.0pt\vphantom{\underset{x}{\overset{X}{X}}}\sigma_{2}^{\prime\prime}&{},{}&r_{22}@^{\Sigma_{22}}_{m_{22}}\hskip 2.0pt\mathllap{\raisebox{-5.0pt}{\color[rgb]{0.5,0.5,0.5}$\lrcorner$}}\mathllap{\raisebox{6.0pt}{\color[rgb]{0.5,0.5,0.5}$\urcorner$}}\vphantom{\underset{x}{\overset{X}{X}}}\hfil\hskip 10.00002pt&{{\color[rgb]{0,0,0}\textnormal{{{(H5.2)}}}}}\end{array}}$

    * and we also have: $\mathit{n_{1}=n_{11}+n_{12}}$, $\mathit{n_{2}=n_{21}+n_{22}}$, $\mathit{\sigma_{1}^{\prime}=\sigma_{1}^{\prime\prime}}$, $\mathit{\sigma_{2}^{\prime}=\sigma_{2}^{\prime\prime}}$, $\mathit{v_{1}=(r_{11}+r_{12})@^{\Sigma_{11}+\Sigma_{12}}_{m_{11}\sqcup m_{12}}}$ and $\mathit{v_{2}=(r_{21}+r_{22})@^{\Sigma_{21}+\Sigma_{22}}_{m_{21}\sqcup m_{22}}}$. By IH ($\mathit{n=n}$ decreasing), (H1), (H2), (H3), (H4.1) and (H5.1) we have: $\mathit{n_{11}=n_{21}}$ (IH.1.C1); $\mathit{\sigma_{1}^{\prime}\sim^{\Sigma}_{n-n_{11}}\sigma_{2}^{\prime}}$ (IH.1.C2); and $\mathit{r_{11}@^{\Sigma_{11}}_{m_{11}}\sim^{\Sigma}_{n-n_{11}}r_{21}@^{\Sigma_{21}}_{m_{21}}}$ (IH.1.C3). By unfolding the definition in (IH.1.C3), we have: $\mathit{\Sigma_{11}=\Sigma_{21}}$ (IH.1.C3.1); $\mathit{m_{11}=m_{21}}$ (IH.1.C3.2); and $\mathit{r_{11}\sim^{\Sigma\mathord{\cdotp}\Sigma_{11}}_{m_{11}}r_{21}}$ (IH.1.C3.3). Note the following facts: $\mathit{n_{12}\leq n-n_{11}}$ (F1); and $\mathit{\rho_{1}\sim^{\Sigma}_{n-n_{11}}}$ (F2). (F1) follows from (H3) and $\mathit{n_{1}=n_{11}+n_{12}}$. (F2) follows from (H1) and  (Step-index Weakening)..1. By IH ($\mathit{n=n-n_{11}}$ decreasing), (F2), (IH.1.C2), (F1), (H4.2) and (H5.2) we have: $\mathit{n_{12}=n_{22}}$ (IH.2.C1); $\mathit{\sigma_{1}^{\prime\prime}\sim^{\Sigma}_{n-n_{11}-n_{12}}\sigma_{2}^{\prime\prime}}$ (IH.2.C2); and $\mathit{r_{12}@^{\Sigma_{12}}_{m_{12}}\sim^{\Sigma}_{n_{11}-n_{12}}r_{22}@^{\Sigma_{22}}_{m_{22}}}$ (IH.2.C3). By unfolding the definition in (IH.2.C3), we have: $\mathit{\Sigma_{12}=\Sigma_{22}}$ (IH.2.C3.1); $\mathit{m_{12}=m_{22}}$ (IH.2.C3.2); and $\mathit{r_{12}\sim^{\Sigma\mathord{\cdotp}\Sigma_{12}}_{m_{12}}r_{22}}$ (IH.2.C3.3). To show: (C1): $\mathit{n_{11}+n_{12}=n_{21}+n_{22}}$; (C2): $\mathit{\sigma_{1}^{\prime\prime}\sim^{\Sigma}_{n-n_{11}-n_{12}}\sigma_{2}^{\prime\prime}}$; and (C3): $\mathit{(r_{11}+r_{12})@^{\Sigma_{11}+\Sigma_{12}}_{m_{11}\sqcup m_{12}}\sim^{\Sigma}_{n-n_{11}-n_{12}}(r_{21}+r_{22})@^{\Sigma_{21}+\Sigma_{22}}_{m_{21}\sqcup m_{22}}}$. (C1) is immediate from (IH.1.C1) and (IH.2.C1). (C2) is immediate from (IH.2.C2). To show (C3) we must show: (C3.1): $\mathit{\Sigma_{11}+\Sigma_{12}=\Sigma_{21}+\Sigma_{22}}$; (C3.2): $\mathit{m_{11}\sqcup m_{12}=m_{21}\sqcup m_{22}}$; and (C3.3): $\mathit{(r_{11}+r_{12})\sim^{\Sigma\mathord{\cdotp}(\Sigma_{11}+\Sigma_{12})}_{m_{11}\sqcup m_{12}}(r_{21}+r_{22})}$. (C3.1) is immediate from (IH.1.C3.1) and (IH.2.C3.1). (C3.2) is immediate from (IH.1.C3.2) and (IH.2.C3.2). (C3.3) holds as follows: By  (Plus Respects)., (IH.1.C3.3) and (IH.2.C3.3): $\mathit{(r_{11}+r_{12})\sim^{\Sigma\mathord{\cdotp}\Sigma_{11}}_{m_{11}}(r_{21}+r_{12})\sim^{\Sigma\mathord{\cdotp}\Sigma_{12}}_{m_{12}}(r_{21}+r_{22})}$. By  (Triangle).: $\mathit{(r_{11}+r_{12})\sim^{\Sigma\mathord{\cdotp}\Sigma_{11}+\Sigma\mathord{\cdotp}\Sigma_{12}}_{m_{11}\sqcup m_{12}}(r_{21}+r_{22})}$. By basic algebra: $\mathit{(r_{11}+r_{12})\sim^{\Sigma\mathord{\cdotp}(\Sigma_{11}+\Sigma_{12})}_{m_{11}\sqcup m_{12}}(r_{21}+r_{22})}$ We have shown the goal.

  * -

    * Case $\mathit{n=n+1}$ and $\mathit{e=e_{1}\ltimes e_{2}}$:

    * By inversion on (H4) and (H5) we have:

    *<EMAIL_ADDRESS>}\rho_{1}&{}\vdash{}&\mathrlap{\raisebox{-5.0pt}{\color[rgb]{0.5,0.5,0.5}$\llcorner$}}\mathrlap{\raisebox{6.0pt}{\color[rgb]{0.5,0.5,0.5}$\ulcorner$}}\hskip 2.0pt\vphantom{\underset{x}{\overset{X}{X}}}\sigma_{1}&{},{}&e_{1}\hskip 2.0pt\mathllap{\raisebox{-5.0pt}{\color[rgb]{0.5,0.5,0.5}$\lrcorner$}}\mathllap{\raisebox{6.0pt}{\color[rgb]{0.5,0.5,0.5}$\urcorner$}}\vphantom{\underset{x}{\overset{X}{X}}}&{}\Downarrow_{n_{11}}{}&\mathrlap{\raisebox{-5.0pt}{\color[rgb]{0.5,0.5,0.5}$\llcorner$}}\mathrlap{\raisebox{6.0pt}{\color[rgb]{0.5,0.5,0.5}$\ulcorner$}}\hskip 2.0pt\vphantom{\underset{x}{\overset{X}{X}}}\sigma_{1}^{\prime}&{},{}&r_{11}@^{{\textbf{Z}}}_{m_{11}}\hskip 2.0pt\mathllap{\raisebox{-5.0pt}{\color[rgb]{0.5,0.5,0.5}$\lrcorner$}}\mathllap{\raisebox{6.0pt}{\color[rgb]{0.5,0.5,0.5}$\urcorner$}}\vphantom{\underset{x}{\overset{X}{X}}}\hfil\hskip 10.00002pt&{{\color[rgb]{0,0,0}\textnormal{{{(H4.1)}}}}}\cr\rho_{1}&{}\vdash{}&\mathrlap{\raisebox{-5.0pt}{\color[rgb]{0.5,0.5,0.5}$\llcorner$}}\mathrlap{\raisebox{6.0pt}{\color[rgb]{0.5,0.5,0.5}$\ulcorner$}}\hskip 2.0pt\vphantom{\underset{x}{\overset{X}{X}}}\sigma_{1}^{\prime}&{},{}&e_{2}\hskip 2.0pt\mathllap{\raisebox{-5.0pt}{\color[rgb]{0.5,0.5,0.5}$\lrcorner$}}\mathllap{\raisebox{6.0pt}{\color[rgb]{0.5,0.5,0.5}$\urcorner$}}\vphantom{\underset{x}{\overset{X}{X}}}&{}\Downarrow_{n_{12}}{}&\mathrlap{\raisebox{-5.0pt}{\color[rgb]{0.5,0.5,0.5}$\llcorner$}}\mathrlap{\raisebox{6.0pt}{\color[rgb]{0.5,0.5,0.5}$\ulcorner$}}\hskip 2.0pt\vphantom{\underset{x}{\overset{X}{X}}}\sigma_{1}^{\prime\prime}&{},{}&r_{12}@^{{\textbf{Z}}}_{m_{12}}\hskip 2.0pt\mathllap{\raisebox{-5.0pt}{\color[rgb]{0.5,0.5,0.5}$\lrcorner$}}\mathllap{\raisebox{6.0pt}{\color[rgb]{0.5,0.5,0.5}$\urcorner$}}\vphantom{\underset{x}{\overset{X}{X}}}\hfil\hskip 10.00002pt&{{\color[rgb]{0,0,0}\textnormal{{{(H4.2)}}}}}\cr\rho_{2}&{}\vdash{}&\mathrlap{\raisebox{-5.0pt}{\color[rgb]{0.5,0.5,0.5}$\llcorner$}}\mathrlap{\raisebox{6.0pt}{\color[rgb]{0.5,0.5,0.5}$\ulcorner$}}\hskip 2.0pt\vphantom{\underset{x}{\overset{X}{X}}}\sigma_{2}&{},{}&e_{1}\hskip 2.0pt\mathllap{\raisebox{-5.0pt}{\color[rgb]{0.5,0.5,0.5}$\lrcorner$}}\mathllap{\raisebox{6.0pt}{\color[rgb]{0.5,0.5,0.5}$\urcorner$}}\vphantom{\underset{x}{\overset{X}{X}}}&{}\Downarrow_{n_{21}}{}&\mathrlap{\raisebox{-5.0pt}{\color[rgb]{0.5,0.5,0.5}$\llcorner$}}\mathrlap{\raisebox{6.0pt}{\color[rgb]{0.5,0.5,0.5}$\ulcorner$}}\hskip 2.0pt\vphantom{\underset{x}{\overset{X}{X}}}\sigma_{2}^{\prime}&{},{}&r_{21}@^{\Sigma_{1}}_{m_{21}}\hskip 2.0pt\mathllap{\raisebox{-5.0pt}{\color[rgb]{0.5,0.5,0.5}$\lrcorner$}}\mathllap{\raisebox{6.0pt}{\color[rgb]{0.5,0.5,0.5}$\urcorner$}}\vphantom{\underset{x}{\overset{X}{X}}}\hfil\hskip 10.00002pt&{{\color[rgb]{0,0,0}\textnormal{{{(H5.1)}}}}}\cr\rho_{2}&{}\vdash{}&\mathrlap{\raisebox{-5.0pt}{\color[rgb]{0.5,0.5,0.5}$\llcorner$}}\mathrlap{\raisebox{6.0pt}{\color[rgb]{0.5,0.5,0.5}$\ulcorner$}}\hskip 2.0pt\vphantom{\underset{x}{\overset{X}{X}}}\sigma_{2}^{\prime}&{},{}&e_{2}\hskip 2.0pt\mathllap{\raisebox{-5.0pt}{\color[rgb]{0.5,0.5,0.5}$\lrcorner$}}\mathllap{\raisebox{6.0pt}{\color[rgb]{0.5,0.5,0.5}$\urcorner$}}\vphantom{\underset{x}{\overset{X}{X}}}&{}\Downarrow_{n_{22}}{}&\mathrlap{\raisebox{-5.0pt}{\color[rgb]{0.5,0.5,0.5}$\llcorner$}}\mathrlap{\raisebox{6.0pt}{\color[rgb]{0.5,0.5,0.5}$\ulcorner$}}\hskip 2.0pt\vphantom{\underset{x}{\overset{X}{X}}}\sigma_{2}^{\prime\prime}&{},{}&r_{22}@^{\Sigma_{2}}_{m_{22}}\hskip 2.0pt\mathllap{\raisebox{-5.0pt}{\color[rgb]{0.5,0.5,0.5}$\lrcorner$}}\mathllap{\raisebox{6.0pt}{\color[rgb]{0.5,0.5,0.5}$\urcorner$}}\vphantom{\underset{x}{\overset{X}{X}}}\hfil\hskip 10.00002pt&{{\color[rgb]{0,0,0}\textnormal{{{(H5.2)}}}}}\end{array}}$

    * and we also have: $\mathit{n_{1}=n_{11}+n_{12}}$, $\mathit{n_{2}=n_{21}+n_{22}}$, $\mathit{\sigma_{1}^{\prime}=\sigma_{1}^{\prime\prime}}$, $\mathit{\sigma_{2}^{\prime}=\sigma_{2}^{\prime\prime}}$, $\mathit{v_{1}=(r_{11}\times r_{12})@^{r_{11}\Sigma_{12}}_{m_{12}}}$ and $\mathit{v_{2}=(r_{21}\times r_{22})@^{r_{21}\Sigma_{22}}_{m_{22}}}$. By IH ($\mathit{n=n}$ decreasing), (H1), (H2), (H3), (H4.1) and (H5.1) we have: $\mathit{n_{11}=n_{21}}$ (IH.1.C1); $\mathit{\sigma_{1}^{\prime}\sim^{\Sigma}_{n-n_{11}}\sigma_{2}^{\prime}}$ (IH.1.C2); and $\mathit{r_{11}@^{\Sigma_{11}}_{m_{11}}\sim^{\Sigma}_{n-n_{11}-n_{12}}r_{21}@^{\Sigma_{21}}_{m_{21}}}$ (IH.1.C3). By unfolding the definition in (IH.1.C3), we have: $\mathit{\Sigma_{11}=\Sigma_{21}}$ (IH.1.C3.1); $\mathit{m_{11}=m_{21}}$ (IH.1.C3.2); and $\mathit{r_{11}\sim^{0}_{m_{11}}r_{21}}$ (IH.1.C3.3). As a consequence of (IH.1.C3), we have: $\mathit{r_{11}=r_{21}}$. Note the following facts: $\mathit{n_{12}\leq n-n_{11}}$ (F1); and $\mathit{\rho_{1}\sim^{\Sigma}_{n-n_{11}}}$ (F2). (F1) follows from (H3) and $\mathit{n_{1}=n_{11}+n_{12}}$. (F2) follows from (H1) and  (Step-index Weakening)..1. By IH ($\mathit{n=n-n_{11}}$ decreasing), (F2), (IH.1.C2), (F1), (H4.2) and (H5.2) we have: $\mathit{n_{12}=n_{22}}$ (IH.2.C1); $\mathit{\sigma_{1}^{\prime\prime}\sim^{\Sigma}_{n-n_{11}-n_{12}}\sigma_{2}^{\prime\prime}}$ (IH.2.C2); and $\mathit{r_{12}@^{\Sigma_{12}}_{m_{12}}\sim^{\Sigma}_{n_{11}-n_{12}}r_{22}@^{\Sigma_{22}}_{m_{22}}}$ (IH.2.C3). By unfolding the definition in (IH.2.C3), we have: $\mathit{\Sigma_{12}=\Sigma_{22}}$ (IH.2.C3.1); $\mathit{m_{12}=m_{22}}$ (IH.2.C3.2); and $\mathit{r_{12}\sim^{\Sigma\mathord{\cdotp}\Sigma_{12}}_{m_{12}}r_{22}}$ (IH.2.C3.3). To show: (C1): $\mathit{n_{11}+n_{12}=n_{21}+n_{22}}$; (C2): $\mathit{\sigma_{1}^{\prime\prime}\sim^{\Sigma}_{n-n_{11}-n_{12}}\sigma_{2}^{\prime\prime}}$; and (C3): $\mathit{(r_{11}\times r_{12})@^{r_{11}\Sigma_{12}}_{m_{12}}\sim^{\Sigma}_{n-n_{11}-n_{12}}(r_{21}\times r_{22})@^{(r_{21}\Sigma_{22})}_{m_{22}}}$. (C1) is immediate from (IH.1.C1) and (IH.2.C1). (C2) is immediate from (IH.2.C2). To show (C3) we must show: (C3.1): $\mathit{r_{11}\Sigma_{12}=r_{21}\Sigma_{22}}$; (C3.2): $\mathit{m_{12}=m_{22}}$; and (C3.3): $\mathit{(r_{11}\times r_{12})\sim^{\Sigma\mathord{\cdotp}r_{11}\Sigma_{12}}_{m_{12}}(r_{21}\times r_{22})}$. (C3) holds as follows: (C3.1) is immediate from $\mathit{r_{11}=r_{21}}$ and (IH.2.C3.1). (C3.2) is immediate from (IH.2.C3.2). (C3.3) holds as follows: By  (Times Respects)., $\mathit{r_{11}=r_{21}}$ and (IH.2.C3.3): $\mathit{(r_{11}\times r_{12})=(r_{21}\times r_{12})\sim^{r_{11}(\Sigma\mathord{\cdotp}\Sigma_{11})}_{m_{21}}(r_{21}\times r_{22})}$. By basic algebra: $\mathit{(r_{11}\times r_{12})=(r_{21}\times r_{12})\sim^{\Sigma\mathord{\cdotp}r_{11}\Sigma_{11}}_{m_{21}}(r_{21}\times r_{22})}$. We have shown the goal.

  * -

    * Case $\mathit{n=n+1}$ and $\mathit{e=e_{1}\rtimes e_{2}}$: Analogous to previous case.

  * -

    * Case $\mathit{n=n+1}$ and $\mathit{e={{\color[rgb]{0.340625,0.1125,0.471875}\texttt{if0}}}(e_{1})\\{e_{2}\\}\\{e_{3}\\}}$:

    * By inversion on (H4) and (H5) we have 4 subcases, each which induce:

    *<EMAIL_ADDRESS>}\rho_{1}&{}\vdash{}&\mathrlap{\raisebox{-5.0pt}{\color[rgb]{0.5,0.5,0.5}$\llcorner$}}\mathrlap{\raisebox{6.0pt}{\color[rgb]{0.5,0.5,0.5}$\ulcorner$}}\hskip 2.0pt\vphantom{\underset{x}{\overset{X}{X}}}\sigma_{1}&{},{}&e_{1}\hskip 2.0pt\mathllap{\raisebox{-5.0pt}{\color[rgb]{0.5,0.5,0.5}$\lrcorner$}}\mathllap{\raisebox{6.0pt}{\color[rgb]{0.5,0.5,0.5}$\urcorner$}}\vphantom{\underset{x}{\overset{X}{X}}}&{}\Downarrow_{n_{11}}{}&\mathrlap{\raisebox{-5.0pt}{\color[rgb]{0.5,0.5,0.5}$\llcorner$}}\mathrlap{\raisebox{6.0pt}{\color[rgb]{0.5,0.5,0.5}$\ulcorner$}}\hskip 2.0pt\vphantom{\underset{x}{\overset{X}{X}}}\sigma_{1}^{\prime}&{},{}&r_{1}@^{{\textbf{Z}}}_{m_{1}}\hskip 2.0pt\mathllap{\raisebox{-5.0pt}{\color[rgb]{0.5,0.5,0.5}$\lrcorner$}}\mathllap{\raisebox{6.0pt}{\color[rgb]{0.5,0.5,0.5}$\urcorner$}}\vphantom{\underset{x}{\overset{X}{X}}}\hfil\hskip 10.00002pt&{{\color[rgb]{0,0,0}\textnormal{{{(H4.1)}}}}}\cr\rho_{2}&{}\vdash{}&\mathrlap{\raisebox{-5.0pt}{\color[rgb]{0.5,0.5,0.5}$\llcorner$}}\mathrlap{\raisebox{6.0pt}{\color[rgb]{0.5,0.5,0.5}$\ulcorner$}}\hskip 2.0pt\vphantom{\underset{x}{\overset{X}{X}}}\sigma_{2}&{},{}&e_{1}\hskip 2.0pt\mathllap{\raisebox{-5.0pt}{\color[rgb]{0.5,0.5,0.5}$\lrcorner$}}\mathllap{\raisebox{6.0pt}{\color[rgb]{0.5,0.5,0.5}$\urcorner$}}\vphantom{\underset{x}{\overset{X}{X}}}&{}\Downarrow_{n_{21}}{}&\mathrlap{\raisebox{-5.0pt}{\color[rgb]{0.5,0.5,0.5}$\llcorner$}}\mathrlap{\raisebox{6.0pt}{\color[rgb]{0.5,0.5,0.5}$\ulcorner$}}\hskip 2.0pt\vphantom{\underset{x}{\overset{X}{X}}}\sigma_{2}^{\prime}&{},{}&r_{2}@^{{\textbf{Z}}}_{m_{2}}\hskip 2.0pt\mathllap{\raisebox{-5.0pt}{\color[rgb]{0.5,0.5,0.5}$\lrcorner$}}\mathllap{\raisebox{6.0pt}{\color[rgb]{0.5,0.5,0.5}$\urcorner$}}\vphantom{\underset{x}{\overset{X}{X}}}\hfil\hskip 10.00002pt&{{\color[rgb]{0,0,0}\textnormal{{{(H5.1)}}}}}\end{array}}$

    * By IH ($\mathit{n=n}$ decreasing), (H1), (H2), (H3), (H4.1) and (H5.1) we have: $\mathit{n_{11}=n_{21}}$ (IH.1.C1); $\mathit{\sigma_{1}^{\prime}\sim^{\Sigma}_{n-n_{11}}\sigma_{2}^{\prime}}$ (IH.1.C2); and $\mathit{r_{1}\sim^{0}_{m_{1}\sqcap m_{2}}r_{2}}$ (IH.1.C3). As a consequence of (IH.1.C3), we have: $\mathit{r_{1}=r_{2}}$. The 4 subcases initially are for: (1): $\mathit{r_{1}=0}$ and $\mathit{r_{2}=0}$; (2): $\mathit{r_{1}=0}$ and $\mathit{r_{2}\neq 0}$; (3): $\mathit{r_{1}\neq 0}$ and $\mathit{r_{2}=0}$; and (4): $\mathit{r_{1}\neq 0}$ and $\mathit{r_{2}\neq 0}$. However 2 are absurd given $\mathit{r_{1}=r_{2}}$, so these 4 subcases collapse to 2:

    *       * -

        * Subcase $\mathit{r_{1}=r_{2}=0}$:

        * From prior inversion on (H4) and (H5) and fact $\mathit{r_{1}=r_{2}=0}$, we also have:

        *<EMAIL_ADDRESS>}\rho_{1}&{}\vdash{}&\mathrlap{\raisebox{-5.0pt}{\color[rgb]{0.5,0.5,0.5}$\llcorner$}}\mathrlap{\raisebox{6.0pt}{\color[rgb]{0.5,0.5,0.5}$\ulcorner$}}\hskip 2.0pt\vphantom{\underset{x}{\overset{X}{X}}}\sigma_{1}^{\prime}&{},{}&e_{2}\hskip 2.0pt\mathllap{\raisebox{-5.0pt}{\color[rgb]{0.5,0.5,0.5}$\lrcorner$}}\mathllap{\raisebox{6.0pt}{\color[rgb]{0.5,0.5,0.5}$\urcorner$}}\vphantom{\underset{x}{\overset{X}{X}}}&{}\Downarrow_{n_{12}}{}&\mathrlap{\raisebox{-5.0pt}{\color[rgb]{0.5,0.5,0.5}$\llcorner$}}\mathrlap{\raisebox{6.0pt}{\color[rgb]{0.5,0.5,0.5}$\ulcorner$}}\hskip 2.0pt\vphantom{\underset{x}{\overset{X}{X}}}\sigma_{1}^{\prime\prime}&{},{}&v_{1}\hskip 2.0pt\mathllap{\raisebox{-5.0pt}{\color[rgb]{0.5,0.5,0.5}$\lrcorner$}}\mathllap{\raisebox{6.0pt}{\color[rgb]{0.5,0.5,0.5}$\urcorner$}}\vphantom{\underset{x}{\overset{X}{X}}}\hfil\hskip 10.00002pt&{{\color[rgb]{0,0,0}\textnormal{{{(H4.2)}}}}}\cr\rho_{2}&{}\vdash{}&\mathrlap{\raisebox{-5.0pt}{\color[rgb]{0.5,0.5,0.5}$\llcorner$}}\mathrlap{\raisebox{6.0pt}{\color[rgb]{0.5,0.5,0.5}$\ulcorner$}}\hskip 2.0pt\vphantom{\underset{x}{\overset{X}{X}}}\sigma_{2}^{\prime}&{},{}&e_{2}\hskip 2.0pt\mathllap{\raisebox{-5.0pt}{\color[rgb]{0.5,0.5,0.5}$\lrcorner$}}\mathllap{\raisebox{6.0pt}{\color[rgb]{0.5,0.5,0.5}$\urcorner$}}\vphantom{\underset{x}{\overset{X}{X}}}&{}\Downarrow_{n_{22}}{}&\mathrlap{\raisebox{-5.0pt}{\color[rgb]{0.5,0.5,0.5}$\llcorner$}}\mathrlap{\raisebox{6.0pt}{\color[rgb]{0.5,0.5,0.5}$\ulcorner$}}\hskip 2.0pt\vphantom{\underset{x}{\overset{X}{X}}}\sigma_{2}^{\prime\prime}&{},{}&v_{2}\hskip 2.0pt\mathllap{\raisebox{-5.0pt}{\color[rgb]{0.5,0.5,0.5}$\lrcorner$}}\mathllap{\raisebox{6.0pt}{\color[rgb]{0.5,0.5,0.5}$\urcorner$}}\vphantom{\underset{x}{\overset{X}{X}}}\hfil\hskip 10.00002pt&{{\color[rgb]{0,0,0}\textnormal{{{(H5.2)}}}}}\end{array}}$

        * and we also have: $\mathit{n_{1}=n_{11}+n_{12}}$, $\mathit{n_{2}=n_{21}+n_{22}}$, $\mathit{\sigma_{1}^{\prime}=\sigma_{1}^{\prime\prime}}$, $\mathit{\sigma_{2}^{\prime}=\sigma_{2}^{\prime\prime}}$, $\mathit{v_{1}=v_{1}}$ and $\mathit{v_{2}=v_{2}}$. We continue reasoning in a generic way outside this subcase…

      * -

        * Subcase $\mathit{r_{1}\neq 0}$ and $\mathit{r_{2}\neq 0}$:

        * From prior inversion on (H4) and (H5) and fact $\mathit{r_{1}=r_{2}\neq 0}$, we also have:

        *<EMAIL_ADDRESS>}\rho_{1}&{}\vdash{}&\mathrlap{\raisebox{-5.0pt}{\color[rgb]{0.5,0.5,0.5}$\llcorner$}}\mathrlap{\raisebox{6.0pt}{\color[rgb]{0.5,0.5,0.5}$\ulcorner$}}\hskip 2.0pt\vphantom{\underset{x}{\overset{X}{X}}}\sigma_{1}^{\prime}&{},{}&e_{3}\hskip 2.0pt\mathllap{\raisebox{-5.0pt}{\color[rgb]{0.5,0.5,0.5}$\lrcorner$}}\mathllap{\raisebox{6.0pt}{\color[rgb]{0.5,0.5,0.5}$\urcorner$}}\vphantom{\underset{x}{\overset{X}{X}}}&{}\Downarrow_{n_{12}}{}&\mathrlap{\raisebox{-5.0pt}{\color[rgb]{0.5,0.5,0.5}$\llcorner$}}\mathrlap{\raisebox{6.0pt}{\color[rgb]{0.5,0.5,0.5}$\ulcorner$}}\hskip 2.0pt\vphantom{\underset{x}{\overset{X}{X}}}\sigma_{1}^{\prime\prime}&{},{}&v_{1}\hskip 2.0pt\mathllap{\raisebox{-5.0pt}{\color[rgb]{0.5,0.5,0.5}$\lrcorner$}}\mathllap{\raisebox{6.0pt}{\color[rgb]{0.5,0.5,0.5}$\urcorner$}}\vphantom{\underset{x}{\overset{X}{X}}}\hfil\hskip 10.00002pt&{{\color[rgb]{0,0,0}\textnormal{{{(H4.2)}}}}}\cr\rho_{2}&{}\vdash{}&\mathrlap{\raisebox{-5.0pt}{\color[rgb]{0.5,0.5,0.5}$\llcorner$}}\mathrlap{\raisebox{6.0pt}{\color[rgb]{0.5,0.5,0.5}$\ulcorner$}}\hskip 2.0pt\vphantom{\underset{x}{\overset{X}{X}}}\sigma_{2}^{\prime}&{},{}&e_{3}\hskip 2.0pt\mathllap{\raisebox{-5.0pt}{\color[rgb]{0.5,0.5,0.5}$\lrcorner$}}\mathllap{\raisebox{6.0pt}{\color[rgb]{0.5,0.5,0.5}$\urcorner$}}\vphantom{\underset{x}{\overset{X}{X}}}&{}\Downarrow_{n_{22}}{}&\mathrlap{\raisebox{-5.0pt}{\color[rgb]{0.5,0.5,0.5}$\llcorner$}}\mathrlap{\raisebox{6.0pt}{\color[rgb]{0.5,0.5,0.5}$\ulcorner$}}\hskip 2.0pt\vphantom{\underset{x}{\overset{X}{X}}}\sigma_{2}^{\prime\prime}&{},{}&v_{2}\hskip 2.0pt\mathllap{\raisebox{-5.0pt}{\color[rgb]{0.5,0.5,0.5}$\lrcorner$}}\mathllap{\raisebox{6.0pt}{\color[rgb]{0.5,0.5,0.5}$\urcorner$}}\vphantom{\underset{x}{\overset{X}{X}}}\hfil\hskip 10.00002pt&{{\color[rgb]{0,0,0}\textnormal{{{(H5.2)}}}}}\end{array}}$

        * and we also have: $\mathit{n_{1}=n_{11}+n_{12}}$ $\mathit{n_{2}=n_{21}+n_{22}}$ $\mathit{\sigma_{1}^{\prime}=\sigma_{1}^{\prime\prime}}$ $\mathit{\sigma_{2}^{\prime}=\sigma_{2}^{\prime\prime}}$ $\mathit{v_{1}=v_{1}}$ $\mathit{v_{2}=v_{2}}$ We continue reasoning in a generic way outside this subcase…

    * Note the following facts: $\mathit{n_{12}\leq n-n_{11}}$ (F1); and $\mathit{\rho_{1}\sim^{\Sigma}_{n-n_{11}}}$ (F2). (F1) follows from (H3) and $\mathit{n_{1}=n_{11}+n_{12}}$. (F2) follows from (H1) and  (Step-index Weakening)..1. By IH ($\mathit{n=n-n_{11}}$ decreasing), (F2), (IH.1.C2), (F1), (H4.2) and (H5.2) we have: $\mathit{n_{21}=n_{22}}$ (IH.2.C1); $\mathit{\sigma_{1}^{\prime\prime}\sim^{\Sigma}_{n-n_{11}-n_{21}}\sigma_{2}^{\prime\prime}}$ (IH.2.C2); and $\mathit{v_{1}\sim^{\Sigma}_{n-n_{11}-n_{21}}v_{2}}$ (IH.2.C3). To show: (C1): $\mathit{n_{11}+n_{12}=n_{21}+n_{22}}$; (C2): $\mathit{\sigma_{1}^{\prime\prime}\sim^{\Sigma}_{n-n_{11}-n_{12}}\sigma_{2}^{\prime\prime}}$; and (C3): $\mathit{v_{1}\sim^{\Sigma}_{n-n_{11}-n_{12}}v_{2}}$. (C1) is immediate from (IH.1.C1) and (IH.2.C1). (C2) is immediate from (IH.2.C2). (C3) is immediate from (IH.2.C3)

  * -

    * Case $\mathit{n=n+1}$ and $\mathit{e=\langle e_{1},e_{2}\rangle}$:

    * By inversion on (H4) and (H5) we have:

    *<EMAIL_ADDRESS>}\rho_{1}&{}\vdash{}&\mathrlap{\raisebox{-5.0pt}{\color[rgb]{0.5,0.5,0.5}$\llcorner$}}\mathrlap{\raisebox{6.0pt}{\color[rgb]{0.5,0.5,0.5}$\ulcorner$}}\hskip 2.0pt\vphantom{\underset{x}{\overset{X}{X}}}\sigma_{1}&{},{}&e_{1}\hskip 2.0pt\mathllap{\raisebox{-5.0pt}{\color[rgb]{0.5,0.5,0.5}$\lrcorner$}}\mathllap{\raisebox{6.0pt}{\color[rgb]{0.5,0.5,0.5}$\urcorner$}}\vphantom{\underset{x}{\overset{X}{X}}}&{}\Downarrow_{n_{11}}{}&\mathrlap{\raisebox{-5.0pt}{\color[rgb]{0.5,0.5,0.5}$\llcorner$}}\mathrlap{\raisebox{6.0pt}{\color[rgb]{0.5,0.5,0.5}$\ulcorner$}}\hskip 2.0pt\vphantom{\underset{x}{\overset{X}{X}}}\sigma_{1}^{\prime}&{},{}&v_{11}\hskip 2.0pt\mathllap{\raisebox{-5.0pt}{\color[rgb]{0.5,0.5,0.5}$\lrcorner$}}\mathllap{\raisebox{6.0pt}{\color[rgb]{0.5,0.5,0.5}$\urcorner$}}\vphantom{\underset{x}{\overset{X}{X}}}\hfil\hskip 10.00002pt&{{\color[rgb]{0,0,0}\textnormal{{{(H4.1)}}}}}\cr\rho_{1}&{}\vdash{}&\mathrlap{\raisebox{-5.0pt}{\color[rgb]{0.5,0.5,0.5}$\llcorner$}}\mathrlap{\raisebox{6.0pt}{\color[rgb]{0.5,0.5,0.5}$\ulcorner$}}\hskip 2.0pt\vphantom{\underset{x}{\overset{X}{X}}}\sigma_{1}^{\prime}&{},{}&e_{2}\hskip 2.0pt\mathllap{\raisebox{-5.0pt}{\color[rgb]{0.5,0.5,0.5}$\lrcorner$}}\mathllap{\raisebox{6.0pt}{\color[rgb]{0.5,0.5,0.5}$\urcorner$}}\vphantom{\underset{x}{\overset{X}{X}}}&{}\Downarrow_{n_{12}}{}&\mathrlap{\raisebox{-5.0pt}{\color[rgb]{0.5,0.5,0.5}$\llcorner$}}\mathrlap{\raisebox{6.0pt}{\color[rgb]{0.5,0.5,0.5}$\ulcorner$}}\hskip 2.0pt\vphantom{\underset{x}{\overset{X}{X}}}\sigma_{1}^{\prime\prime}&{},{}&v_{12}\hskip 2.0pt\mathllap{\raisebox{-5.0pt}{\color[rgb]{0.5,0.5,0.5}$\lrcorner$}}\mathllap{\raisebox{6.0pt}{\color[rgb]{0.5,0.5,0.5}$\urcorner$}}\vphantom{\underset{x}{\overset{X}{X}}}\hfil\hskip 10.00002pt&{{\color[rgb]{0,0,0}\textnormal{{{(H4.2)}}}}}\cr\rho_{2}&{}\vdash{}&\mathrlap{\raisebox{-5.0pt}{\color[rgb]{0.5,0.5,0.5}$\llcorner$}}\mathrlap{\raisebox{6.0pt}{\color[rgb]{0.5,0.5,0.5}$\ulcorner$}}\hskip 2.0pt\vphantom{\underset{x}{\overset{X}{X}}}\sigma_{2}&{},{}&e_{1}\hskip 2.0pt\mathllap{\raisebox{-5.0pt}{\color[rgb]{0.5,0.5,0.5}$\lrcorner$}}\mathllap{\raisebox{6.0pt}{\color[rgb]{0.5,0.5,0.5}$\urcorner$}}\vphantom{\underset{x}{\overset{X}{X}}}&{}\Downarrow_{n_{21}}{}&\mathrlap{\raisebox{-5.0pt}{\color[rgb]{0.5,0.5,0.5}$\llcorner$}}\mathrlap{\raisebox{6.0pt}{\color[rgb]{0.5,0.5,0.5}$\ulcorner$}}\hskip 2.0pt\vphantom{\underset{x}{\overset{X}{X}}}\sigma_{2}^{\prime}&{},{}&v_{21}\hskip 2.0pt\mathllap{\raisebox{-5.0pt}{\color[rgb]{0.5,0.5,0.5}$\lrcorner$}}\mathllap{\raisebox{6.0pt}{\color[rgb]{0.5,0.5,0.5}$\urcorner$}}\vphantom{\underset{x}{\overset{X}{X}}}\hfil\hskip 10.00002pt&{{\color[rgb]{0,0,0}\textnormal{{{(H5.1)}}}}}\cr\rho_{2}&{}\vdash{}&\mathrlap{\raisebox{-5.0pt}{\color[rgb]{0.5,0.5,0.5}$\llcorner$}}\mathrlap{\raisebox{6.0pt}{\color[rgb]{0.5,0.5,0.5}$\ulcorner$}}\hskip 2.0pt\vphantom{\underset{x}{\overset{X}{X}}}\sigma_{2}^{\prime}&{},{}&e_{2}\hskip 2.0pt\mathllap{\raisebox{-5.0pt}{\color[rgb]{0.5,0.5,0.5}$\lrcorner$}}\mathllap{\raisebox{6.0pt}{\color[rgb]{0.5,0.5,0.5}$\urcorner$}}\vphantom{\underset{x}{\overset{X}{X}}}&{}\Downarrow_{n_{22}}{}&\mathrlap{\raisebox{-5.0pt}{\color[rgb]{0.5,0.5,0.5}$\llcorner$}}\mathrlap{\raisebox{6.0pt}{\color[rgb]{0.5,0.5,0.5}$\ulcorner$}}\hskip 2.0pt\vphantom{\underset{x}{\overset{X}{X}}}\sigma_{2}^{\prime\prime}&{},{}&v_{22}\hskip 2.0pt\mathllap{\raisebox{-5.0pt}{\color[rgb]{0.5,0.5,0.5}$\lrcorner$}}\mathllap{\raisebox{6.0pt}{\color[rgb]{0.5,0.5,0.5}$\urcorner$}}\vphantom{\underset{x}{\overset{X}{X}}}\hfil\hskip 10.00002pt&{{\color[rgb]{0,0,0}\textnormal{{{(H5.2)}}}}}\end{array}}$

    * and we also have: $\mathit{n_{1}=n_{11}+n_{12}}$, $\mathit{n_{2}=n_{21}+n_{22}}$, $\mathit{\sigma_{1}^{\prime}=\sigma_{1}^{\prime\prime}}$, $\mathit{\sigma_{2}^{\prime}=\sigma_{2}^{\prime\prime}}$, $\mathit{v_{1}=\langle v_{11},v_{12}\rangle}$ and $\mathit{v_{2}=\langle v_{21},v_{22}\rangle}$. By IH ($\mathit{n=n}$ decreasing), (H1), (H2), (H3), (H4.1) and (H5.1) we have: $\mathit{n_{11}=n_{21}}$ (IH.1.C1); $\mathit{\sigma_{1}^{\prime}\sim^{\Sigma}_{n-n_{11}}\sigma_{2}^{\prime}}$ (IH.1.C2); and $\mathit{v_{11}\sim^{\Sigma}_{n-n_{11}}v_{21}}$ (IH.1.C3). Note the following facts: $\mathit{n_{12}\leq n-n_{11}}$ (F1); and $\mathit{\rho_{1}\sim^{\Sigma}_{n-n_{11}}}$ (F2). (F1) follows from (H3) and $\mathit{n_{1}=n_{11}+n_{12}}$. (F2) follows from (H1) and  (Step-index Weakening)..1. By IH ($\mathit{n=n-n_{11}}$ decreasing), (F2), (IH.1.C2), (F1), (H4.2) and (H5.2) we have: $\mathit{n_{12}=n_{22}}$ (IH.2.C1); $\mathit{\sigma_{1}^{\prime\prime}\sim^{\Sigma}_{n-n_{11}-n_{12}}\sigma_{2}^{\prime\prime}}$ (IH.2.C2); and $\mathit{v_{12}\sim^{\Sigma}_{n-n_{11}-n_{12}}v_{22}}$ (IH.2.C3). To show: (C1): $\mathit{n_{11}+n_{12}=n_{21}+n_{22}}$; (C2): $\mathit{\sigma_{1}^{\prime\prime}\sim^{\Sigma}_{n-n_{11}-n_{12}}\sigma_{2}^{\prime\prime}}$; and (C3): $\mathit{\langle v_{11},v_{12}\rangle\sim^{\Sigma}_{n-n_{11}-n_{12}}\langle v_{21},v_{22}\rangle}$. (C1) is immediate from (IH.1.C1) and (IH.2.C1). (C2) is immediate from (IH.2.C2). (C3) is immediate from (IH.1.C3) and (IH.2.C3).

  * -

    * Case $\mathit{n=n+1}$ and $\mathit{e=\pi_{i}(e)}$:

    * By inversion on (H4) and (H5) we have:

    *<EMAIL_ADDRESS>}\rho_{1}&{}\vdash{}&\mathrlap{\raisebox{-5.0pt}{\color[rgb]{0.5,0.5,0.5}$\llcorner$}}\mathrlap{\raisebox{6.0pt}{\color[rgb]{0.5,0.5,0.5}$\ulcorner$}}\hskip 2.0pt\vphantom{\underset{x}{\overset{X}{X}}}\sigma_{1}&{},{}&e\hskip 2.0pt\mathllap{\raisebox{-5.0pt}{\color[rgb]{0.5,0.5,0.5}$\lrcorner$}}\mathllap{\raisebox{6.0pt}{\color[rgb]{0.5,0.5,0.5}$\urcorner$}}\vphantom{\underset{x}{\overset{X}{X}}}&{}\Downarrow_{n_{1}}{}&\mathrlap{\raisebox{-5.0pt}{\color[rgb]{0.5,0.5,0.5}$\llcorner$}}\mathrlap{\raisebox{6.0pt}{\color[rgb]{0.5,0.5,0.5}$\ulcorner$}}\hskip 2.0pt\vphantom{\underset{x}{\overset{X}{X}}}\sigma_{1}^{\prime}&{},{}&\langle v_{11},v_{12}\rangle\hskip 2.0pt\mathllap{\raisebox{-5.0pt}{\color[rgb]{0.5,0.5,0.5}$\lrcorner$}}\mathllap{\raisebox{6.0pt}{\color[rgb]{0.5,0.5,0.5}$\urcorner$}}\vphantom{\underset{x}{\overset{X}{X}}}\hfil\hskip 10.00002pt&{{\color[rgb]{0,0,0}\textnormal{{{(H4.1)}}}}}\cr\rho_{2}&{}\vdash{}&\mathrlap{\raisebox{-5.0pt}{\color[rgb]{0.5,0.5,0.5}$\llcorner$}}\mathrlap{\raisebox{6.0pt}{\color[rgb]{0.5,0.5,0.5}$\ulcorner$}}\hskip 2.0pt\vphantom{\underset{x}{\overset{X}{X}}}\sigma_{2}&{},{}&e\hskip 2.0pt\mathllap{\raisebox{-5.0pt}{\color[rgb]{0.5,0.5,0.5}$\lrcorner$}}\mathllap{\raisebox{6.0pt}{\color[rgb]{0.5,0.5,0.5}$\urcorner$}}\vphantom{\underset{x}{\overset{X}{X}}}&{}\Downarrow_{n_{2}}{}&\mathrlap{\raisebox{-5.0pt}{\color[rgb]{0.5,0.5,0.5}$\llcorner$}}\mathrlap{\raisebox{6.0pt}{\color[rgb]{0.5,0.5,0.5}$\ulcorner$}}\hskip 2.0pt\vphantom{\underset{x}{\overset{X}{X}}}\sigma_{2}^{\prime}&{},{}&\langle v_{21},v_{22}\rangle\hskip 2.0pt\mathllap{\raisebox{-5.0pt}{\color[rgb]{0.5,0.5,0.5}$\lrcorner$}}\mathllap{\raisebox{6.0pt}{\color[rgb]{0.5,0.5,0.5}$\urcorner$}}\vphantom{\underset{x}{\overset{X}{X}}}\hfil\hskip 10.00002pt&{{\color[rgb]{0,0,0}\textnormal{{{(H5.1)}}}}}\end{array}}$

    * and we also have: $\mathit{n_{1}=n_{1}}$, $\mathit{n_{2}=n_{2}}$, $\mathit{\sigma_{1}^{\prime}=\sigma_{1}^{\prime}}$, $\mathit{\sigma_{2}^{\prime}=\sigma_{2}^{\prime}}$, $\mathit{v_{1}=v_{1i}}$ and $\mathit{v_{2}=v_{2i}}$. By IH ($\mathit{n=n}$ decreasing), (H1), (H2), (H3), (H4.1) and (H5.1) we have: $\mathit{n_{1}=n_{2}}$ (IH.1.C1); $\mathit{\sigma_{1}^{\prime}\sim^{\Sigma}_{n-n_{1}}\sigma_{2}^{\prime}}$ (IH.1.C2); and $\mathit{\langle v_{11},v_{12}\rangle\sim^{\Sigma}_{n-n_{1}}\langle v_{21},v_{22}\rangle}$ (IH.1.C3). To show: (C1): $\mathit{n_{1}=n_{2}}$; (C2): $\mathit{\sigma_{1}^{\prime}\sim^{\Sigma}_{n-n_{1}}\sigma_{2}^{\prime}}$; and (C3): $\mathit{v_{1n^{\prime}}\sim^{\Sigma}_{n-n_{1}}v_{2n^{\prime}}}$. (C1) is immediate from (IH.1.C1). (C2) is immediate from (IH.1.C2). (C3) is immediate from (IH.1.C3).

  * -

    * Case $\mathit{n=n+1}$ and $\mathit{e=\lambda x.\hskip 3.30002pte}$: By inversion on (H4) and (H5) we have: $\mathit{n_{1}=0}$, $\mathit{n_{2}=0}$, $\mathit{\sigma_{1}^{\prime}=\sigma_{1}}$, $\mathit{\sigma_{2}^{\prime}=\sigma_{2}}$, $\mathit{v_{1}=\langle\lambda x.\hskip 3.30002pte\mathrel{|}\rho_{1}\rangle}$ and $\mathit{v_{2}=\langle\lambda x.\hskip 3.30002pte\mathrel{|}\rho_{2}\rangle}$. To show: (C1): $\mathit{0=0}$; (C2): $\mathit{\sigma_{1}\sim_{n}^{\Sigma}\sigma_{2}}$; and (C3): $\mathit{\langle\lambda x.\hskip 3.30002pte\mathrel{|}\rho_{1}\rangle\sim_{n}^{\Sigma}\langle\lambda x.\hskip 3.30002pte\mathrel{|}\rho_{2}\rangle}$. (C1) is trivial. (C2) is immediate from (H2). (C3) holds as follows: Unfolding the definition, we must show: (C3): $\mathit{\begin{array}[t]{lrl }&{}{}\hfil&\forall n^{\prime}\leq n,v_{1},v_{2},\sigma_{1}^{\prime},\sigma_{2}^{\prime}.\hskip 3.30002pt\sigma_{1}^{\prime}\sim_{n^{\prime}}^{\Sigma}\sigma_{2}^{\prime}\hskip 3.30002pt\wedge\hskip 3.30002ptv_{1}\sim_{n^{\prime}}^{\Sigma}v_{2}\cr&{}\Rightarrow{}&\sigma_{1}^{\prime},\\{x\mapsto v_{1}\\}\uplus\rho_{1},e\sim_{n^{\prime}}^{\Sigma}\sigma_{2}^{\prime},\\{x\mapsto v_{2}\\}\uplus\rho_{2},e\end{array}}$. To show (C3), we assume: $\mathit{\sigma_{1}^{\prime}\sim_{n^{\prime}}^{\Sigma}\sigma_{2}^{\prime}}$ (C3.H1); and $\mathit{v_{1}\sim_{n^{\prime}}^{\Sigma}v_{2}}$ (C3.H2). And we must show: (C3.1): $\mathit{\sigma_{1}^{\prime},\\{x\mapsto v_{1}\\}\uplus\rho_{1},e\sim_{n^{\prime}}^{\Sigma}\sigma_{2}^{\prime},\\{x\mapsto v_{2}\\}\uplus\rho_{2},e}$. Note the following facts: $\mathit{\rho_{1}\sim_{n^{\prime}}^{\Sigma}\rho_{1}}$ (F1); and $\mathit{\\{x\mapsto v_{1}\\}\uplus\rho_{1}\sim_{n^{\prime}}^{\Sigma}\\{x\mapsto v_{2}\\}\uplus\rho_{2}}$ (F2). (F1) holds from H1 and  (Step-index Weakening)..1. (F2) holds from (F1), (C3.H2) and the definition of $\mathit{\rho\sim_{n^{\prime}}^{\Sigma}\rho}$. (C3.1) then holds by IH ($\mathit{n=n^{\prime}}$ decreasing), $\mathit{F2}$ and $\mathit{C3.H1}$.

  * -

    * Case $\mathit{n=n+1}$ and $\mathit{e=e_{1}(e_{2})}$:

    * By inversion on (H4) and (H5) we have:

    *<EMAIL_ADDRESS>}\rho_{1}&{}\vdash{}&\mathrlap{\raisebox{-5.0pt}{\color[rgb]{0.5,0.5,0.5}$\llcorner$}}\mathrlap{\raisebox{6.0pt}{\color[rgb]{0.5,0.5,0.5}$\ulcorner$}}\hskip 2.0pt\vphantom{\underset{x}{\overset{X}{X}}}\sigma_{1}&{},{}&e_{1}\hskip 2.0pt\mathllap{\raisebox{-5.0pt}{\color[rgb]{0.5,0.5,0.5}$\lrcorner$}}\mathllap{\raisebox{6.0pt}{\color[rgb]{0.5,0.5,0.5}$\urcorner$}}\vphantom{\underset{x}{\overset{X}{X}}}&{}\Downarrow_{n_{11}}{}&\mathrlap{\raisebox{-5.0pt}{\color[rgb]{0.5,0.5,0.5}$\llcorner$}}\mathrlap{\raisebox{6.0pt}{\color[rgb]{0.5,0.5,0.5}$\ulcorner$}}\hskip 2.0pt\vphantom{\underset{x}{\overset{X}{X}}}\sigma_{1}^{\prime}&{},{}&\langle\lambda x.\hskip 3.30002pte_{1}^{\prime}\mathrel{|}\rho_{1}^{\prime}\rangle\hskip 2.0pt\mathllap{\raisebox{-5.0pt}{\color[rgb]{0.5,0.5,0.5}$\lrcorner$}}\mathllap{\raisebox{6.0pt}{\color[rgb]{0.5,0.5,0.5}$\urcorner$}}\vphantom{\underset{x}{\overset{X}{X}}}\hfil\hskip 10.00002pt&{{\color[rgb]{0,0,0}\textnormal{{{(H4.1)}}}}}\cr\rho_{1}&{}\vdash{}&\mathrlap{\raisebox{-5.0pt}{\color[rgb]{0.5,0.5,0.5}$\llcorner$}}\mathrlap{\raisebox{6.0pt}{\color[rgb]{0.5,0.5,0.5}$\ulcorner$}}\hskip 2.0pt\vphantom{\underset{x}{\overset{X}{X}}}\sigma_{1}^{\prime}&{},{}&e_{2}\hskip 2.0pt\mathllap{\raisebox{-5.0pt}{\color[rgb]{0.5,0.5,0.5}$\lrcorner$}}\mathllap{\raisebox{6.0pt}{\color[rgb]{0.5,0.5,0.5}$\urcorner$}}\vphantom{\underset{x}{\overset{X}{X}}}&{}\Downarrow_{n_{12}}{}&\mathrlap{\raisebox{-5.0pt}{\color[rgb]{0.5,0.5,0.5}$\llcorner$}}\mathrlap{\raisebox{6.0pt}{\color[rgb]{0.5,0.5,0.5}$\ulcorner$}}\hskip 2.0pt\vphantom{\underset{x}{\overset{X}{X}}}\sigma_{1}^{\prime\prime}&{},{}&v_{1}\hskip 2.0pt\mathllap{\raisebox{-5.0pt}{\color[rgb]{0.5,0.5,0.5}$\lrcorner$}}\mathllap{\raisebox{6.0pt}{\color[rgb]{0.5,0.5,0.5}$\urcorner$}}\vphantom{\underset{x}{\overset{X}{X}}}\hfil\hskip 10.00002pt&{{\color[rgb]{0,0,0}\textnormal{{{(H4.2)}}}}}\cr\\{x\mapsto v_{1}\\}\uplus\rho_{1}^{\prime}&{}\vdash{}&\mathrlap{\raisebox{-5.0pt}{\color[rgb]{0.5,0.5,0.5}$\llcorner$}}\mathrlap{\raisebox{6.0pt}{\color[rgb]{0.5,0.5,0.5}$\ulcorner$}}\hskip 2.0pt\vphantom{\underset{x}{\overset{X}{X}}}\sigma_{2}^{\prime\prime}&{},{}&e_{1}^{\prime}\hskip 2.0pt\mathllap{\raisebox{-5.0pt}{\color[rgb]{0.5,0.5,0.5}$\lrcorner$}}\mathllap{\raisebox{6.0pt}{\color[rgb]{0.5,0.5,0.5}$\urcorner$}}\vphantom{\underset{x}{\overset{X}{X}}}&{}\Downarrow_{n_{13}}{}&\mathrlap{\raisebox{-5.0pt}{\color[rgb]{0.5,0.5,0.5}$\llcorner$}}\mathrlap{\raisebox{6.0pt}{\color[rgb]{0.5,0.5,0.5}$\ulcorner$}}\hskip 2.0pt\vphantom{\underset{x}{\overset{X}{X}}}\sigma_{1}^{\prime\prime\prime}&{},{}&v_{1}^{\prime}\hskip 2.0pt\mathllap{\raisebox{-5.0pt}{\color[rgb]{0.5,0.5,0.5}$\lrcorner$}}\mathllap{\raisebox{6.0pt}{\color[rgb]{0.5,0.5,0.5}$\urcorner$}}\vphantom{\underset{x}{\overset{X}{X}}}\hfil\hskip 10.00002pt&{{\color[rgb]{0,0,0}\textnormal{{{(H4.3)}}}}}\cr\rho_{2}&{}\vdash{}&\mathrlap{\raisebox{-5.0pt}{\color[rgb]{0.5,0.5,0.5}$\llcorner$}}\mathrlap{\raisebox{6.0pt}{\color[rgb]{0.5,0.5,0.5}$\ulcorner$}}\hskip 2.0pt\vphantom{\underset{x}{\overset{X}{X}}}\sigma_{2}&{},{}&e_{1}\hskip 2.0pt\mathllap{\raisebox{-5.0pt}{\color[rgb]{0.5,0.5,0.5}$\lrcorner$}}\mathllap{\raisebox{6.0pt}{\color[rgb]{0.5,0.5,0.5}$\urcorner$}}\vphantom{\underset{x}{\overset{X}{X}}}&{}\Downarrow_{n_{21}}{}&\mathrlap{\raisebox{-5.0pt}{\color[rgb]{0.5,0.5,0.5}$\llcorner$}}\mathrlap{\raisebox{6.0pt}{\color[rgb]{0.5,0.5,0.5}$\ulcorner$}}\hskip 2.0pt\vphantom{\underset{x}{\overset{X}{X}}}\sigma_{2}^{\prime}&{},{}&\langle\lambda x.\hskip 3.30002pte_{2}^{\prime}\mathrel{|}\rho_{2}^{\prime}\rangle\hskip 2.0pt\mathllap{\raisebox{-5.0pt}{\color[rgb]{0.5,0.5,0.5}$\lrcorner$}}\mathllap{\raisebox{6.0pt}{\color[rgb]{0.5,0.5,0.5}$\urcorner$}}\vphantom{\underset{x}{\overset{X}{X}}}\hfil\hskip 10.00002pt&{{\color[rgb]{0,0,0}\textnormal{{{(H5.1)}}}}}\cr\rho_{2}&{}\vdash{}&\mathrlap{\raisebox{-5.0pt}{\color[rgb]{0.5,0.5,0.5}$\llcorner$}}\mathrlap{\raisebox{6.0pt}{\color[rgb]{0.5,0.5,0.5}$\ulcorner$}}\hskip 2.0pt\vphantom{\underset{x}{\overset{X}{X}}}\sigma_{2}^{\prime}&{},{}&e_{2}\hskip 2.0pt\mathllap{\raisebox{-5.0pt}{\color[rgb]{0.5,0.5,0.5}$\lrcorner$}}\mathllap{\raisebox{6.0pt}{\color[rgb]{0.5,0.5,0.5}$\urcorner$}}\vphantom{\underset{x}{\overset{X}{X}}}&{}\Downarrow_{n_{22}}{}&\mathrlap{\raisebox{-5.0pt}{\color[rgb]{0.5,0.5,0.5}$\llcorner$}}\mathrlap{\raisebox{6.0pt}{\color[rgb]{0.5,0.5,0.5}$\ulcorner$}}\hskip 2.0pt\vphantom{\underset{x}{\overset{X}{X}}}\sigma_{2}^{\prime\prime}&{},{}&v_{2}\hskip 2.0pt\mathllap{\raisebox{-5.0pt}{\color[rgb]{0.5,0.5,0.5}$\lrcorner$}}\mathllap{\raisebox{6.0pt}{\color[rgb]{0.5,0.5,0.5}$\urcorner$}}\vphantom{\underset{x}{\overset{X}{X}}}\hfil\hskip 10.00002pt&{{\color[rgb]{0,0,0}\textnormal{{{(H5.2)}}}}}\cr\\{x\mapsto v_{2}\\}\uplus\rho_{2}^{\prime}&{}\vdash{}&\mathrlap{\raisebox{-5.0pt}{\color[rgb]{0.5,0.5,0.5}$\llcorner$}}\mathrlap{\raisebox{6.0pt}{\color[rgb]{0.5,0.5,0.5}$\ulcorner$}}\hskip 2.0pt\vphantom{\underset{x}{\overset{X}{X}}}\sigma_{2}^{\prime\prime}&{},{}&e_{2}^{\prime}\hskip 2.0pt\mathllap{\raisebox{-5.0pt}{\color[rgb]{0.5,0.5,0.5}$\lrcorner$}}\mathllap{\raisebox{6.0pt}{\color[rgb]{0.5,0.5,0.5}$\urcorner$}}\vphantom{\underset{x}{\overset{X}{X}}}&{}\Downarrow_{n_{23}}{}&\mathrlap{\raisebox{-5.0pt}{\color[rgb]{0.5,0.5,0.5}$\llcorner$}}\mathrlap{\raisebox{6.0pt}{\color[rgb]{0.5,0.5,0.5}$\ulcorner$}}\hskip 2.0pt\vphantom{\underset{x}{\overset{X}{X}}}\sigma_{2}^{\prime\prime\prime}&{},{}&v_{2}^{\prime}\hskip 2.0pt\mathllap{\raisebox{-5.0pt}{\color[rgb]{0.5,0.5,0.5}$\lrcorner$}}\mathllap{\raisebox{6.0pt}{\color[rgb]{0.5,0.5,0.5}$\urcorner$}}\vphantom{\underset{x}{\overset{X}{X}}}\hfil\hskip 10.00002pt&{{\color[rgb]{0,0,0}\textnormal{{{(H5.3)}}}}}\end{array}}$

    * and we also have: $\mathit{n_{1}=n_{11}+n_{12}+n_{13}+1}$, $\mathit{n_{2}=n_{21}+n_{22}+n_{23}+1}$, $\mathit{\sigma_{1}^{\prime}=\sigma_{1}^{\prime\prime\prime}}$, $\mathit{\sigma_{2}^{\prime}=\sigma_{2}^{\prime\prime\prime}}$, $\mathit{v_{1}=v_{1}^{\prime}}$ and $\mathit{v_{2}=v_{2}^{\prime}}$. By IH ($\mathit{n=n}$ decreasing), (H1), (H2), (H3), (H4.1) and (H5.1) we have: $\mathit{n_{11}=n_{21}}$ (IH.1.C1); $\mathit{\sigma_{1}^{\prime}\sim^{\Sigma}_{n-n_{11}}\sigma_{2}^{\prime}}$ (IH.1.C2); and $\mathit{\langle\lambda x.\hskip 3.30002pte_{1}^{\prime}\mathrel{|}\rho_{1}^{\prime}\sim^{\Sigma}_{n-n_{11}}v_{21}}$ (IH.1.C3). Note the following facts: $\mathit{n_{12}\leq n-n_{11}}$ (F1); and $\mathit{\rho_{1}\sim^{\Sigma}_{n-n_{11}}}$ (F2). (F1) follows from (H3) and $\mathit{n_{1}=n_{11}+n_{12}+n_{13}+1}$. (F2) follows from (H1) and  (Step-index Weakening)..1. By IH ($\mathit{n=n-n_{11}}$ decreasing), (H2), (IH.1.C2), (F1), (H4.2) and (H5.2) we have: $\mathit{n_{12}=n_{22}}$ (IH.2.C1); $\mathit{\sigma_{1}^{\prime\prime}\sim^{\Sigma}_{n-n_{11}-n_{12}}\sigma_{2}^{\prime\prime}}$ (IH.2.C2); and $\mathit{v_{1}\sim^{\Sigma}_{n-n_{11}-n_{12}}v_{2}}$ (IH.2.C3). Note the following facts, each of which follow from (H3) and $\mathit{n_{1}=n_{11}+n_{12}+n_{13}+1}$: $\mathit{n_{13}\leq n-n_{11}-n_{12}}$ (F3); and $\mathit{n-n_{11}-n_{12}-n_{13}>0}$ (F4). Also note the following facts which follow from (IH.1.C3), (IH.2.C2), (IH.2.C3), (F3) and (F4): $\mathit{n_{13}=n_{23}}$ (F4.C1); $\mathit{\sigma_{1}^{\prime\prime\prime}\sim^{\Sigma}_{n-n_{11}-n_{12}-n_{13}-1}\sigma_{2}^{\prime\prime\prime}}$ (F4.C2); and $\mathit{v_{1}^{\prime}\sim^{\sigma}_{n-n_{11}-n_{12}-n_{13}-1}v_{2}^{\prime}}$ (F4.C3). To show: (C1): $\mathit{n_{11}+n_{12}+n_{13}+1=n_{21}+n_{22}+n_{23}+1}$; (C2): $\mathit{\sigma_{1}^{\prime\prime\prime}\sim^{\Sigma}_{n-n_{11}-n_{12}-n_{13}-1}\sigma_{2}^{\prime\prime\prime}}$; and (C3): $\mathit{v_{1}^{\prime}\sim^{\Sigma}_{n-n_{11}-n_{12}-n_{13}-1}v_{2}^{\prime}}$. (C1) is immediate from (IH.1.C1), (IH.2.C1) and (F4.C1). (C2) is immediate from (F4.C2) and  (Step-index Weakening)..2. (C3) is immediate from (F4.C3) and  (Step-index Weakening)..3.

  * -

    * Case $\mathit{n=n+1}$ and $\mathit{e={{\color[rgb]{0.340625,0.1125,0.471875}\texttt{ref}}}(e)}$:

    * By inversion on (H4) and (H5) we have:

    *<EMAIL_ADDRESS>}\rho_{1}&{}\vdash{}&\mathrlap{\raisebox{-5.0pt}{\color[rgb]{0.5,0.5,0.5}$\llcorner$}}\mathrlap{\raisebox{6.0pt}{\color[rgb]{0.5,0.5,0.5}$\ulcorner$}}\hskip 2.0pt\vphantom{\underset{x}{\overset{X}{X}}}\sigma_{1}&{},{}&e\hskip 2.0pt\mathllap{\raisebox{-5.0pt}{\color[rgb]{0.5,0.5,0.5}$\lrcorner$}}\mathllap{\raisebox{6.0pt}{\color[rgb]{0.5,0.5,0.5}$\urcorner$}}\vphantom{\underset{x}{\overset{X}{X}}}&{}\Downarrow_{n_{1}}{}&\mathrlap{\raisebox{-5.0pt}{\color[rgb]{0.5,0.5,0.5}$\llcorner$}}\mathrlap{\raisebox{6.0pt}{\color[rgb]{0.5,0.5,0.5}$\ulcorner$}}\hskip 2.0pt\vphantom{\underset{x}{\overset{X}{X}}}\sigma_{1}^{\prime}&{},{}&v_{1}\hskip 2.0pt\mathllap{\raisebox{-5.0pt}{\color[rgb]{0.5,0.5,0.5}$\lrcorner$}}\mathllap{\raisebox{6.0pt}{\color[rgb]{0.5,0.5,0.5}$\urcorner$}}\vphantom{\underset{x}{\overset{X}{X}}}\hfil\hskip 10.00002pt&{{\color[rgb]{0,0,0}\textnormal{{{(H4.1)}}}}}\cr\lx@intercol\hfil\ell_{1}\lx@intercol&{}={}&\lx@intercol{\text{alloc}}({\text{dom}}(\sigma_{1}^{\prime}))\hfil\lx@intercol&{{\color[rgb]{0,0,0}\textnormal{{{(H4.2)}}}}}\cr\rho_{2}&{}\vdash{}&\mathrlap{\raisebox{-5.0pt}{\color[rgb]{0.5,0.5,0.5}$\llcorner$}}\mathrlap{\raisebox{6.0pt}{\color[rgb]{0.5,0.5,0.5}$\ulcorner$}}\hskip 2.0pt\vphantom{\underset{x}{\overset{X}{X}}}\sigma_{2}&{},{}&e\hskip 2.0pt\mathllap{\raisebox{-5.0pt}{\color[rgb]{0.5,0.5,0.5}$\lrcorner$}}\mathllap{\raisebox{6.0pt}{\color[rgb]{0.5,0.5,0.5}$\urcorner$}}\vphantom{\underset{x}{\overset{X}{X}}}&{}\Downarrow_{n_{2}}{}&\mathrlap{\raisebox{-5.0pt}{\color[rgb]{0.5,0.5,0.5}$\llcorner$}}\mathrlap{\raisebox{6.0pt}{\color[rgb]{0.5,0.5,0.5}$\ulcorner$}}\hskip 2.0pt\vphantom{\underset{x}{\overset{X}{X}}}\sigma_{2}^{\prime}&{},{}&v_{2}\hskip 2.0pt\mathllap{\raisebox{-5.0pt}{\color[rgb]{0.5,0.5,0.5}$\lrcorner$}}\mathllap{\raisebox{6.0pt}{\color[rgb]{0.5,0.5,0.5}$\urcorner$}}\vphantom{\underset{x}{\overset{X}{X}}}\hfil\hskip 10.00002pt&{{\color[rgb]{0,0,0}\textnormal{{{(H5.1)}}}}}\cr\lx@intercol\hfil\ell_{2}\lx@intercol&{}={}&\lx@intercol{\text{alloc}}({\text{dom}}(\sigma_{2}^{\prime}))\hfil\lx@intercol&{{\color[rgb]{0,0,0}\textnormal{{{(H4.2)}}}}}\end{array}}$

    * and we also have: $\mathit{n_{1}=n_{1}}$, $\mathit{n_{2}=n_{2}}$, $\mathit{\sigma_{1}^{\prime}=\\{\ell\mapsto v_{1}\\}\uplus\sigma_{1}^{\prime}}$, $\mathit{\sigma_{2}^{\prime}=\\{\ell\mapsto v_{2}\\}\uplus\sigma_{2}^{\prime}}$, $\mathit{v_{1}=\ell_{1}}$ and $\mathit{v_{2}=\ell_{2}}$. By IH ($\mathit{n=n}$ decreasing), (H1), (H2), (H3), (H4.1) and (H5.1) we have: $\mathit{n_{1}=n_{2}}$ (IH.1.C1); $\mathit{\sigma_{1}^{\prime}\sim^{\Sigma}_{n-n_{1}}\sigma_{2}^{\prime}}$ (IH.1.C2); and $\mathit{v_{1}\sim^{\Sigma}_{n-n_{1}}v_{2}}$ (IH.1.C3). Because $\mathit{\sigma_{1}\sim^{\Sigma}_{n-n_{1}}\sigma_{2}^{\prime}}$, we know $\mathit{{\text{dom}}(\sigma_{1})={\text{dom}}(\sigma_{2})}$ and therefore $\mathit{\ell_{1}=\ell_{2}}$. To show: (C1): $\mathit{n_{1}=n_{2}}$; (C2): $\mathit{\\{\ell\mapsto v_{1}\\}\uplus\sigma_{1}^{\prime}\sim^{\Sigma}_{n-n_{1}}\\{\ell\mapsto v_{2}\\}\uplus\sigma_{2}^{\prime}}$; and (C3): $\mathit{\ell_{1}\sim^{\Sigma}_{n-n_{1}}\ell_{2}}$. (C1) is immediate from (IH.1.C1). (C2) is immediate from (IH.1.C2), (IH.1.C3) and the definition of $\mathit{\sigma\sim_{n}^{\Sigma}\sigma}$. (C3) is immediate by definition of $\mathit{v\sim_{n}^{\Sigma}v}$ and $\mathit{\ell_{1}=\ell_{2}}$.

  * -

    * Case $\mathit{n=n+1}$ and $\mathit{e={!}e}$:

    * By inversion on (H4) and (H5) we have:

    *<EMAIL_ADDRESS>}\rho_{1}&{}\vdash{}&\mathrlap{\raisebox{-5.0pt}{\color[rgb]{0.5,0.5,0.5}$\llcorner$}}\mathrlap{\raisebox{6.0pt}{\color[rgb]{0.5,0.5,0.5}$\ulcorner$}}\hskip 2.0pt\vphantom{\underset{x}{\overset{X}{X}}}\sigma_{1}&{},{}&e\hskip 2.0pt\mathllap{\raisebox{-5.0pt}{\color[rgb]{0.5,0.5,0.5}$\lrcorner$}}\mathllap{\raisebox{6.0pt}{\color[rgb]{0.5,0.5,0.5}$\urcorner$}}\vphantom{\underset{x}{\overset{X}{X}}}&{}\Downarrow_{n_{1}}{}&\mathrlap{\raisebox{-5.0pt}{\color[rgb]{0.5,0.5,0.5}$\llcorner$}}\mathrlap{\raisebox{6.0pt}{\color[rgb]{0.5,0.5,0.5}$\ulcorner$}}\hskip 2.0pt\vphantom{\underset{x}{\overset{X}{X}}}\sigma_{1}^{\prime}&{},{}&\ell_{1}\hskip 2.0pt\mathllap{\raisebox{-5.0pt}{\color[rgb]{0.5,0.5,0.5}$\lrcorner$}}\mathllap{\raisebox{6.0pt}{\color[rgb]{0.5,0.5,0.5}$\urcorner$}}\vphantom{\underset{x}{\overset{X}{X}}}\hfil\hskip 10.00002pt&{{\color[rgb]{0,0,0}\textnormal{{{(H4.1)}}}}}\cr\rho_{2}&{}\vdash{}&\mathrlap{\raisebox{-5.0pt}{\color[rgb]{0.5,0.5,0.5}$\llcorner$}}\mathrlap{\raisebox{6.0pt}{\color[rgb]{0.5,0.5,0.5}$\ulcorner$}}\hskip 2.0pt\vphantom{\underset{x}{\overset{X}{X}}}\sigma_{2}&{},{}&e\hskip 2.0pt\mathllap{\raisebox{-5.0pt}{\color[rgb]{0.5,0.5,0.5}$\lrcorner$}}\mathllap{\raisebox{6.0pt}{\color[rgb]{0.5,0.5,0.5}$\urcorner$}}\vphantom{\underset{x}{\overset{X}{X}}}&{}\Downarrow_{n_{2}}{}&\mathrlap{\raisebox{-5.0pt}{\color[rgb]{0.5,0.5,0.5}$\llcorner$}}\mathrlap{\raisebox{6.0pt}{\color[rgb]{0.5,0.5,0.5}$\ulcorner$}}\hskip 2.0pt\vphantom{\underset{x}{\overset{X}{X}}}\sigma_{2}^{\prime}&{},{}&\ell_{2}\hskip 2.0pt\mathllap{\raisebox{-5.0pt}{\color[rgb]{0.5,0.5,0.5}$\lrcorner$}}\mathllap{\raisebox{6.0pt}{\color[rgb]{0.5,0.5,0.5}$\urcorner$}}\vphantom{\underset{x}{\overset{X}{X}}}\hfil\hskip 10.00002pt&{{\color[rgb]{0,0,0}\textnormal{{{(H5.1)}}}}}\end{array}}$

    * and we also have: $\mathit{n_{1}=n_{1}}$, $\mathit{n_{2}=n_{2}}$, $\mathit{\sigma_{1}^{\prime}=\sigma_{1}^{\prime}}$, $\mathit{\sigma_{2}^{\prime}=\sigma_{2}^{\prime}}$, $\mathit{v_{1}=\sigma_{1}^{\prime}(\ell_{1})}$ and $\mathit{v_{2}=\sigma_{2}^{\prime}(\ell_{2})}$. By IH ($\mathit{n=n}$ decreasing), (H1), (H2), (H3), (H4.1) and (H5.1) we have: $\mathit{n_{1}=n_{2}}$ (IH.1.C1); $\mathit{\sigma_{1}^{\prime}\sim^{\Sigma}_{n-n_{1}}\sigma_{2}^{\prime}}$ (IH.1.C2); and $\mathit{\ell_{1}\sim^{\Sigma}_{n-n_{1}}\ell_{2}}$ (IH.1.C3). Because $\mathit{\ell_{1}\sim^{\Sigma}_{n-n_{1}}\ell_{2}}$, we know $\mathit{\ell_{1}=\ell_{2}}$ by definition of $\mathit{v\sim_{n}^{\Sigma}v}$. To show: (C1): $\mathit{n_{1}=n_{2}}$; (C2): $\mathit{\sigma_{1}^{\prime}\sim^{\Sigma}_{n-n_{1}}\sigma_{2}^{\prime}}$; and (C3): $\mathit{\sigma_{1}^{\prime}(\ell_{1})\sim^{\Sigma}_{n-n_{1}}\sigma_{2}^{\prime}(\ell_{2})}$. (C1) is immediate from (IH.1.C1). (C2) is immediate from (IH.1.C2). (C3) is immediate from (IH.1.C2) and $\mathit{\ell_{1}=\ell_{2}}$.

  * -

    * Case $\mathit{n=n+1}$ and $\mathit{e=e_{1}\leftarrow e_{2}}$:

    * By inversion on (H4) and (H5) we have:

    *<EMAIL_ADDRESS>}\rho_{1}&{}\vdash{}&\mathrlap{\raisebox{-5.0pt}{\color[rgb]{0.5,0.5,0.5}$\llcorner$}}\mathrlap{\raisebox{6.0pt}{\color[rgb]{0.5,0.5,0.5}$\ulcorner$}}\hskip 2.0pt\vphantom{\underset{x}{\overset{X}{X}}}\sigma_{1}&{},{}&e_{1}\hskip 2.0pt\mathllap{\raisebox{-5.0pt}{\color[rgb]{0.5,0.5,0.5}$\lrcorner$}}\mathllap{\raisebox{6.0pt}{\color[rgb]{0.5,0.5,0.5}$\urcorner$}}\vphantom{\underset{x}{\overset{X}{X}}}&{}\Downarrow_{n_{11}}{}&\mathrlap{\raisebox{-5.0pt}{\color[rgb]{0.5,0.5,0.5}$\llcorner$}}\mathrlap{\raisebox{6.0pt}{\color[rgb]{0.5,0.5,0.5}$\ulcorner$}}\hskip 2.0pt\vphantom{\underset{x}{\overset{X}{X}}}\sigma_{1}^{\prime}&{},{}&\ell_{1}\hskip 2.0pt\mathllap{\raisebox{-5.0pt}{\color[rgb]{0.5,0.5,0.5}$\lrcorner$}}\mathllap{\raisebox{6.0pt}{\color[rgb]{0.5,0.5,0.5}$\urcorner$}}\vphantom{\underset{x}{\overset{X}{X}}}\hfil\hskip 10.00002pt&{{\color[rgb]{0,0,0}\textnormal{{{(H4.1)}}}}}\cr\rho_{1}&{}\vdash{}&\mathrlap{\raisebox{-5.0pt}{\color[rgb]{0.5,0.5,0.5}$\llcorner$}}\mathrlap{\raisebox{6.0pt}{\color[rgb]{0.5,0.5,0.5}$\ulcorner$}}\hskip 2.0pt\vphantom{\underset{x}{\overset{X}{X}}}\sigma_{1}^{\prime}&{},{}&e_{2}\hskip 2.0pt\mathllap{\raisebox{-5.0pt}{\color[rgb]{0.5,0.5,0.5}$\lrcorner$}}\mathllap{\raisebox{6.0pt}{\color[rgb]{0.5,0.5,0.5}$\urcorner$}}\vphantom{\underset{x}{\overset{X}{X}}}&{}\Downarrow_{n_{12}}{}&\mathrlap{\raisebox{-5.0pt}{\color[rgb]{0.5,0.5,0.5}$\llcorner$}}\mathrlap{\raisebox{6.0pt}{\color[rgb]{0.5,0.5,0.5}$\ulcorner$}}\hskip 2.0pt\vphantom{\underset{x}{\overset{X}{X}}}\sigma_{1}^{\prime\prime}&{},{}&\ell_{2}\hskip 2.0pt\mathllap{\raisebox{-5.0pt}{\color[rgb]{0.5,0.5,0.5}$\lrcorner$}}\mathllap{\raisebox{6.0pt}{\color[rgb]{0.5,0.5,0.5}$\urcorner$}}\vphantom{\underset{x}{\overset{X}{X}}}\hfil\hskip 10.00002pt&{{\color[rgb]{0,0,0}\textnormal{{{(H4.2)}}}}}\cr\rho_{2}&{}\vdash{}&\mathrlap{\raisebox{-5.0pt}{\color[rgb]{0.5,0.5,0.5}$\llcorner$}}\mathrlap{\raisebox{6.0pt}{\color[rgb]{0.5,0.5,0.5}$\ulcorner$}}\hskip 2.0pt\vphantom{\underset{x}{\overset{X}{X}}}\sigma_{2}&{},{}&e_{1}\hskip 2.0pt\mathllap{\raisebox{-5.0pt}{\color[rgb]{0.5,0.5,0.5}$\lrcorner$}}\mathllap{\raisebox{6.0pt}{\color[rgb]{0.5,0.5,0.5}$\urcorner$}}\vphantom{\underset{x}{\overset{X}{X}}}&{}\Downarrow_{n_{21}}{}&\mathrlap{\raisebox{-5.0pt}{\color[rgb]{0.5,0.5,0.5}$\llcorner$}}\mathrlap{\raisebox{6.0pt}{\color[rgb]{0.5,0.5,0.5}$\ulcorner$}}\hskip 2.0pt\vphantom{\underset{x}{\overset{X}{X}}}\sigma_{2}^{\prime}&{},{}&v_{1}\hskip 2.0pt\mathllap{\raisebox{-5.0pt}{\color[rgb]{0.5,0.5,0.5}$\lrcorner$}}\mathllap{\raisebox{6.0pt}{\color[rgb]{0.5,0.5,0.5}$\urcorner$}}\vphantom{\underset{x}{\overset{X}{X}}}\hfil\hskip 10.00002pt&{{\color[rgb]{0,0,0}\textnormal{{{(H5.1)}}}}}\cr\rho_{2}&{}\vdash{}&\mathrlap{\raisebox{-5.0pt}{\color[rgb]{0.5,0.5,0.5}$\llcorner$}}\mathrlap{\raisebox{6.0pt}{\color[rgb]{0.5,0.5,0.5}$\ulcorner$}}\hskip 2.0pt\vphantom{\underset{x}{\overset{X}{X}}}\sigma_{2}^{\prime}&{},{}&e_{2}\hskip 2.0pt\mathllap{\raisebox{-5.0pt}{\color[rgb]{0.5,0.5,0.5}$\lrcorner$}}\mathllap{\raisebox{6.0pt}{\color[rgb]{0.5,0.5,0.5}$\urcorner$}}\vphantom{\underset{x}{\overset{X}{X}}}&{}\Downarrow_{n_{22}}{}&\mathrlap{\raisebox{-5.0pt}{\color[rgb]{0.5,0.5,0.5}$\llcorner$}}\mathrlap{\raisebox{6.0pt}{\color[rgb]{0.5,0.5,0.5}$\ulcorner$}}\hskip 2.0pt\vphantom{\underset{x}{\overset{X}{X}}}\sigma_{2}^{\prime\prime}&{},{}&v_{2}\hskip 2.0pt\mathllap{\raisebox{-5.0pt}{\color[rgb]{0.5,0.5,0.5}$\lrcorner$}}\mathllap{\raisebox{6.0pt}{\color[rgb]{0.5,0.5,0.5}$\urcorner$}}\vphantom{\underset{x}{\overset{X}{X}}}\hfil\hskip 10.00002pt&{{\color[rgb]{0,0,0}\textnormal{{{(H5.2)}}}}}\end{array}}$

    * and we also have: $\mathit{n_{1}=n_{11}+n_{12}}$, $\mathit{n_{2}=n_{21}+n_{22}}$, $\mathit{\sigma_{1}^{\prime}=\sigma_{1}^{\prime\prime}}$, $\mathit{\sigma_{2}^{\prime}=\sigma_{2}^{\prime\prime}}$, $\mathit{v_{1}=v_{1}}$ and $\mathit{v_{2}=v_{2}}$. By IH ($\mathit{n=n}$ decreasing), (H1), (H2), (H3), (H4.1) and (H5.1) we have: $\mathit{n_{11}=n_{21}}$ (IH.1.C1); $\mathit{\sigma_{1}^{\prime}\sim^{\Sigma}_{n-n_{11}}\sigma_{2}^{\prime}}$ (IH.1.C2); and $\mathit{\ell_{1}\sim^{\Sigma}_{n-n_{11}}\ell_{2}}$ (IH.1.C3). Because $\mathit{\ell_{1}\sim^{\Sigma}_{n-n_{11}}\ell_{2}}$ we know $\mathit{\ell_{1}=\ell_{2}}$. Note the following facts: $\mathit{n_{12}\leq n-n_{11}}$ (F1); and $\mathit{\rho_{1}\sim^{\Sigma}_{n-n_{11}}}$ (F2). (F1) follows from (H3) and $\mathit{n_{1}=n_{11}+n_{12}}$. (F2) follows from (H1) and  (Step-index Weakening)..1. By IH ($\mathit{n=n-n_{11}}$ decreasing), (F2), (IH.1.C2), (F1), (H4.2) and (H5.2) we have: $\mathit{n_{12}=n_{22}}$ (IH.2.C1); $\mathit{\sigma_{1}^{\prime\prime}\sim^{\Sigma}_{n-n_{11}-n_{12}}\sigma_{2}^{\prime\prime}}$ (IH.2.C2); and $\mathit{v_{1}\sim^{\Sigma}_{n-n_{11}-n_{12}}v_{2}}$ (IH.2.C3). To show: (C1): $\mathit{n_{11}+n_{12}=n_{21}+n_{22}}$; (C2): $\mathit{\sigma_{1}^{\prime\prime}[\ell\mapsto v_{1}]\sim^{\Sigma}_{n-n_{11}-n_{12}}\sigma_{2}^{\prime\prime}[\ell\mapsto v_{2}]}$; and (C3): $\mathit{v_{1}\sim^{\Sigma}_{n-n_{11}-n_{12}}v_{2}}$. (C1) is immediate from (IH.1.C1) and (IH.2.C1). (C2) is immediate from (IH.2.C2) and (IH.2.C3). (C3) is immediate from (IH.2.C3).

∎

##  Appendix B Additional Case Studies

###  B-A MWEM with Pandas

The MWEM algorithm [29] constructs a differentially private synthetic dataset
that approximates a real dataset. MWEM produces competitive privacy bounds by
utilizing a combination of the exponential mechanism, Laplacian/Gaussian
noise, and the multiplicative weights update rule. The algorithm uses these
mechanisms iteratively, providing a tight analysis of privacy leakage via
composition. The inputs to the MWEM are as follows: some uniform or random
distribution over a domain ($syn\\_data$), some sensitive dataset
($age\\_counts$), a query workload, a number of iterations $\mathit{i}$, and a
privacy budget $\mathit{\epsilon}$. The algorithm works by, at each iteration:

  * •

privately selecting a query from the query workload (using the exponential
mechanism) whose result on the synthetic dataset greatly differs from the real
dataset

⬇

for t in range(i):

q = exponential(q_workload,score_fn,eps/(2*i))

…

  * •

and then privately using the query result on the real dataset to adjust the
synthetic dataset towards the truth using the multiplicative weights update
rule

⬇

for t in range(i):

…

syn_data = mwem_step(q, age_counts, syn_data)

We present a modified, adaptive MWEM algorithm (Figure 5) which privately
halts execution if the error of the synthetic dataset reaches an acceptably
low level before the entire privacy budget is exceeded, conserving the
remainder of the budget for other private analyses.

⬇

def mwem_step(query, real_data, syn_data):

lower, upper = query

sm = [v for k, v in syn_data.items()]

total = np.sum(sm)

q_ans = range_query(real_data, lower, upper)

real = dduo.renyi_gauss(|$\alpha$|=alpha,|$\epsilon$|=eps,q_ans,sens)

syn = range_query(syn_data, lower, upper)

l = [(k, mwem_update(k, x, lower, upper,

real, syn, total))

for k, x in syn_data.items()]

return dict(l)

\parwith dduo.RenyiFilter(alpha,20.0):

with dduo.RenyiOdometer((alpha,2.0)) as odo:

while stable < stability_thresh:

e = err(age_counts,curr_syn)

curr_noisy_err=dduo.renyi_gauss(|$\alpha$|=alpha,|$\epsilon$|=1.0,e)

if (curr_noisy_err < thresh):

stable += step

else:

stable = 0

for t in range(iterations):

q = exponential(q_workload,score_fn,eps/(2*i))

curr_syn = mwem_step(q,age_counts,curr_syn)

\paracc = dduo.renyi_gauss(alpha, eps_acc,

accuracy(age_counts,curr_syn))

print(f"final accuracy: {acc}")

⬇

Odometer_|$(\alpha,\epsilon)$|(|$\\{ \textit{data.csv} \mapsto(10.0, 0.5)\\}
$|)

final accuracy: 0.703

Figure 5: MWEM with Pandas

###  B-B DiffPrivLib

DiffPrivLib is library for experimenting with analytics and machine learning
with differential privacy in Python by IBM. It provides a comprehensive suite
of differentially private mechanisms, tools, and machine learning models.
While DiffPrivLib provides several mechanisms, models and tools for developing
private applications, as well as a basic privacy accountant, it lacks the
ability to perform a tight privacy analysis in the context of more
sophisticated forms of composition with dynamic and adaptive privacy tracking.
Via integration with DDuo we are able to gain these abilities with minimal
changes to library and program code. Figure 6 shows an example of a modified
DiffPrivLib program: a private naive Bayes classifier run on the standard iris
dataset. The original program has been modified with DDuo hooks to detect
sensitivity violations and track privacy cost. We also present a DDuo
instrumented example of differentially private logistic regression with
DiffPrivLib (Figure 7). Both of these programs have been modified to perform
_adaptively_ private clipping. Over several iterations, clipping parameters
are gradually modified to optimize model accuracy. This form of control flow
on probabilistic values is only sound following the adaptive composition
strategies that DDuo provides. In order to preserve the privacy budget, such
hyperparameter optimization procedures should normally be run on artificial
datasets based on domain knowledge. The changes required for the integration
with the DiffPrivLib library consist of 15 lines of DDuo instrumentation code.

⬇

from dduo import sklearn as sk

from dduo import DiffPrivLib as dpl

with dduo.AdvEdOdometer() as odo:

while noisy_acc < thresh or iters < max_iters:

prev_bounds = bounds

bounds = update_bounds(bounds)

clf = dpl.GNB(bounds=bounds, epsilon=epsilon)

clf.fit(X_train, y_train)

prev_acc = noisy_acc

accuracy = dpl.score(y_test, clf.predict(X_test))

noisy_acc = dduo.gauss(epsilon_acc,delta,accuracy)

if noisy_acc < prev_acc:

bounds = prev_bounds

iters += 1

dduo.print_privacy_cost()

⬇

Odometer_|$(\epsilon,\delta)$|(|$\\{ \textit{data.csv} \mapsto(0.82,
0.0035)\\} $|)

Figure 6: DiffPrivLib: Naive Bayes Classification

⬇

from dduo import sklearn as sk

from dduo import DiffPrivLib as dpl

with dduo.AdvEdOdometer() as odo:

while noisy_acc < thresh or norm > 0.0:

dp_clf = dpl.LogisticRegression(epsilon=epsilon,

data_norm = norm)

dp_clf.fit(X_train, y_train)

accuracy = dp_clf.score(X_test, y_test)

noisy_acc = dduo.gauss(epsilon_acc,delta,accuracy)

norm -= step

dduo.print_privacy_cost()

⬇

Odometer_|$(\epsilon,\delta)$|(|$\\{ \textit{data.csv} \mapsto(0.53,
0.0015)\\} $|)

Figure 7: DiffPrivLib: Logistic Regression


Digital Twin of a Network and Operating Environment Using Augmented Reality

Haoshuo Chen(1), Xiaonan Xu(3), Jesse E. Simsarian(1), Mijail Szczerban(1),

Rob Harby(2), Roland Ryf(1), Mikael Mazur(1), Lauren Dallachiesa(1), Nicolas
K. Fontaine(1), John Cloonan(2), Jim Sandoz(2), David T. Neilson(1)

(1) Nokia Bell Labs, 600 Mountain Ave., Murray Hill, NJ 07974, USA

(2) Nokia, 600 Mountain Ave., Murray Hill, NJ 07974, USA

(3) Aberdeen, NJ 07747, USA

<EMAIL_ADDRESS>
###### Abstract

We demonstrate the digital twin of a network, network elements, and operating
environment using machine learning. We achieve network card failure
localization and remote collaboration over 86 km of fiber using augmented
reality.

##  1 Introduction

A network digital twin is a simulation model of a communication system and its
operating environment that enables applications such as the monitoring of
network operations in real time, predictive maintenance, and testing “what if”
scenarios before implementation on a production network. Recent work on
digital twins of optical networks has developed accurate simulation and
machine-learning (ML) models of the fiber transmission system [1]. There has
been an increased awareness that communication networks are physical systems
that interact with and can be used to sense the environment [2], motivating
the digital-twin model to include the operating environment. Adding the
physical and environmental information has multiple benefits, including
improved physical connectivity visibility, a better understanding of shared
risk groups, and a better facility security analysis.

In this work, we demonstrate an optical network digital twin model based on a
graph neural network (GNN) [3] with novel capabilities enabled by models of
the physical network elements themselves as well as the operating environment.
The network operators interact with the digital twin in real time using a
distributed augmented reality (AR) application empowered with ML through
remote computing. The AR application relies on a low-latency connection to a
remote edge server that performs multiple computational functions. By using a
3-dimensional (3D) map of the network surroundings, 3D models of the network
elements, and fault localization on the optical network, we show that the
digital twin enables automated guidance of an on-site operator to a network
element with a failure condition. When the operator views the network element
with AR, a distributed ML-based image classification algorithm indicates the
card that has the root-cause alarm condition. Finally, the AR application
allows a real-time interactive collaboration session with a second operator
remotely connected to a node after 86 km of fiber propagation so that
knowledge can be shared across central and dispersed locations. Within the AR
session, both operators can manipulate 3D computer-automated design (CAD)
models of the network element and card as virtual 3D holograms, thereby
enabling collaborative maintenance operations inside a metaverse [4].

Fig. 1: a) Optical network topology, b) 3D digital model of a network element,
c) image of the network environment and d) 3D mapping of the network
environment.

##  2 Digital Twin of the Network and Its Operating Environment

We construct a digital twin representation of an optical transport network and
the laboratory environment, encompassing the network topology, network
equipment 3D models, and a 3D map of the environment. Fig. 1a is a diagram of
the optical network consisting of six commercial Nokia 1830 PSS optical
transport nodes (TNs) with flexgrid reconfigurable optical add-drop
multiplexers (ROADMs). Wavelength (WL) paths and fiber lengths are indicated
in the figure. Fig. 1b shows an AR image of a computer-generated downsized
virtual hologram of one of the PSS-32 shelves of node TN1. The hologram was
generated from 3D CAD models of the network element. Fig. 1c is a photograph
of the surrounding environment of the network, and Fig. 1d is a 3D map of the
same location created with a Microsoft HoloLens 2 AR headset (ARH) [5].

Fig. 2: a) Experiment setup for remote AR collaboration, b) illustration of
ML-based fault localization, c) top-view 2D map of the network surroundings
with virtual navigation markers, and d) image of navigation guidance taken
directly through the display of the local (on-site) ARH at the P2 location.

Figure 2a shows a diagram of the equipment used for the AR remote
collaboration experiment. The optical transport nodes TN1 and TN2 are the same
nodes as shown in the optical network diagram of Fig. 1a and wavelength WL1 is
used to carry traffic between the nodes for the experiment. WL1 has a line
rate of 200 Gbit/s using 8-QAM modulation format and a low bit-error ratio in
both directions. Two Centec V586 Openflow (OF) version 1.3 switches with 10G
and 100G interfaces connect to 100G client interfaces on D5X500 flexible
bitrate transponders at TN1 and TN2 that generate and terminate WL1. An
instance of the Open Network Operating System (ONOS) [6] software-defined
network (SDN) controller controls the OF switches. Wi-Fi access points (APs)
connect the local and remote AR headsets to the network with 2.5G connections
to the OF switches at the local and remote sites, respectively. A 100G path
through the network carries both the AR traffic from the local ARH to a remote
server as well as a constant bitrate (CBR) stream from a 100G interface of a
Spirent SPT-N12U traffic generator (TG) that produces bi-directional
competition to the AR traffic.

On-demand computing is enabled using a remote server that is equipped with an
NVIDIA RTX A6000 graphics processing unit. The server assigns tasks to clients
with AR capabilities, processes the requests from the clients through ML
models, and synchronizes the operations between the clients. In the
experiment, WL2 experiences frame losses and three severe network card alarms,
as illustrated in Fig. 2b. The figure illustrates the various card-level
network elements such as optical transponder (OT), line amplifier (LA),
wavelength selective switch (WSS), array amplifier (AA), multicast switch
(MCS), and fiber span. A fault localization model [3], which employs GNNs and
natural language processing, is executed on the remote server and successfully
identifies the optical transponder of WL2 as the source of the failure by
collecting the alarms from the network elements and utilizing the network
connectivity graph, as illustrated in Fig. 2b. The AR applications were
developed using Unity, OpenXR, and mixed reality toolkit [7]. An on-site
(local) operator wearing an ARH uses a hand-operated menu to choose between
applications, set up parameters such as the server IP address, and connect or
disconnect from the remote server.

###  2.1 Lab navigation

We developed an AR-based lab navigation application to assist network
operators in efficiently navigating to their desired destination, e.g., a rack
containing a failed network card. A top view of the 2D lab map is presented in
Fig. 2c, where a path from the starting point (P1) to the rack containing the
failed transponder (P4) is indicated by a series of blue virtual directional
arrows and the destination is marked by a virtual red flag. The on-site ARH
operator receives the coordinates of the arrows and the flag from the remote
server, which calculates the path using the A-star path-finding algorithm [8]
based on the environment’s 3D map of Fig. 1d. Each rack has two network
equipment shelves, and the height of the flag serves as an indication of the
targeted shelf level. Fig. 2(d) shows an AR navigation image captured directly
through the display of the local ARH at the P2 location along the navigation
path.

###  2.2 Network card identification

After locating the shelf, the next step is to indicate to the operator the
network cards with alarms and identify the root-cause of failure. Fig. 3a
shows a diagram of the process for network card identification and indication
to the operator through ML-based computation at the remote server. The
computation uses the object detection model YoloV7 [9], which was fine-tuned
using 824 captured images in order to detect and classify 11 different types
of network cards and 2 different shelves. We employ the trainable bag-of-
freebies method [10] to improve accuracy and reduce the size of the training
dataset. The webcam of the ARH captures images at a rate of 5 frames per
second, which are sent to the remote server. YoloV7 outputs the name of the
detected card, a bounding box that encompasses the card, and a confidence
score. A higher confidence score indicates the likelihood that the box
contains the object, with a maximum score of 1. The coordinates of the
bounding boxes provide the relative positions of the detected cards. Using the
card arrangement information retrieved from the network element database,
cards with alarms can be determined. This information is then sent back to the
ARH with additional color coding to indicate the nature of the alarm. Cards
with a failure requiring replacement are indicated in red, while cards with an
alarm that are not the main source of failure are indicated in blue. The
bounding boxes, along with the card model names and confidence scores, are
displayed on the ARH. In the case of the shelf in Fig. 3a, the flexible-
bitrate OT card (model: D5X500Q) is determined to be the main source of
failure with a confidence score of 85%, and the LA card (model: ASWG) is also
detected as having an alarm, but the GNN ML model of the network determines
that it is not the root cause of the alarm. Note that the shelf image in Fig.
3a contains four of the same LAs that are not indicated as faulty by the
remote server computation. Due to the knowledge of card positions, the LA with
the alarm, which is rightmost among the four, has been successfully
identified.

We tested the robustness of the remote classification computation to network
congestion by introducing CBR competition to the AR traffic with the traffic
generator shown in Fig 2a. We use the OpenFlow [11] meter table to prioritize
the AR traffic, which restricts the maximum rate of the competing traffic to
90 Gb/s of the 100 Gb/s total. Fig. 3b shows the maximum bitrate between the
on-site ARH and the remote edge server and the total round-trip latency for
the identification result, which is caused by the ML inference time of YoloV7
on the server and the network round-trip time over 86 km of single-mode fiber
and the Wi-Fi link. With prioritization of the AR traffic, we measured a
maximum of 330 Mb/s bitrate with iPerf [12], and $<$35 ms total round-trip
latency for the card identification result. Fig. 3c shows histograms of the ML
inference time and network round-trip data transfer time.

###  2.3 Interactive remote collaboration

We developed a remote collaboration application so that a local network
operator can collaborate in real time with a remote expert. For example, the
local operator can receive guidance for the process of replacing the network
card by manually manipulating the virtual 3D models of the transport system
cards and shelf that are generated as 3D images in the virtual environments of
both the operator and remote expert. The remote edge server synchronizes the
position and orientation of the digital 3D models for both participants. Fig.
3d shows an AR image in which the expert utilizes mid-air drawing of red
circles to indicate the locations of the two latches that must be released
prior to removing the card and demonstrates the card-replacement procedure to
the local operator. The application also supports real-time voice and video
communication between the two headsets.

Fig. 3: a) Diagram of the process for network card identification using remote
edge computing, b) maximum bitrate and object identification round-trip
latency with and without CBR traffic metering, c) histogram of ML inference
and network data round-trip times for object identification with CBR metering,
d) image of AR-assisted remote collaboration for card replacement

##  3 Conclusion

In this work, we demonstrate a digital twin of a network, network elements,
and operating environment utilizing ML and remote edge computation. Through
interaction in an AR virtual environment, the digital twin enabled indoor
navigation, network card failure identification and localization, and remote
collaboration over an 86-km optical link. These innovations demonstrate the
potential of AR and ML in network management and maintenance.

Supplemental video: https://youtu.be/RJMDRjCIBFI

## References

  * [1] Q. Zhuge, “AI-Driven Digital Twin for Optical Networks,” in Proc. ECOC’22, paper Mo3a.1, 2022.
  * [2] G.A. Wellbrock et. al., “First Field Trial of Sensing Vehicle Speed, Density, and…,” Proc. OFC 2019, paper Th4C.7.
  * [3] X. Xu et. al., “Optical Network Diagnostics Using Graph Neural Networks…,” Proc. OFC 2023, paper M3G.5.
  * [4] A. Schäfer et al., “A Survey on Synchronous Augmented, Virtual, and…,” ACM Computing Surveys, 55(6), 116, 2022.
  * [5] https://www.microsoft.com/en-us/hololens/hardware
  * [6] https://opennetworking.org/onos/
  * [7] https://unity.com/ https://www.khronos.org/openxr/ https://github.com/microsoft/MixedRealityToolkit-Unity
  * [8] P.E. Hart et. al., “A Formal Basis for the Heuristic…,” IEEE Trans. Syst. Man Cybern. Syst., 4(2), pp.100-107, 1968.
  * [9] C. Wang et. al., “YOLOv7: Trainable Bag-of-Freebies Sets New State-of-The-Art for…,” arXiv:2207.02696, 2022.
  * [10] Z. Zhang et. al., “Bag of Freebies for Training Object Detection Neural Networks,” arXiv:1902.04103, 2019.
  * [11] https://opennetworking.org/wp-content/uploads/2013/04/openflow-spec-v1.3.1.pdf
  * [12] https://iperf.fr/