Environmental Bisimulations for Probabilistic Higher-order Languages Environmental Bisimulations for Probabilistic Higher-order Languages

Proof. The proof is by induction on $n$.

For the case $n=0$, the two properties above are immediate consequences of the definition of $\, \mathcal {R}\,$.

For the inductive case, if $Y\, \mathcal {R}\,^{n+1}_{(M,N)} Z$ then either $Y\, \mathcal {R}\,^{n}_{(M,N)} Z$, and the result follows by the inductive hypothesis, or $Y= \sup S$ for $S=\lbrace Y_{k}\rbrace _{k \ge 0}$ a set of formal sums such that $Y_{k} \, \mathcal {R}\,^{n}_{(M,N)}Z$ for all $k$ and $Y_{k}\le _{{\rm {\tt apx}}}Y_{k+1}$. As a consequence, there is a sequence $Y^{\prime }_{k}$ such that $Y_{0}=Y^{\prime }_{0}$ and $Y_{k+1}=Y_{k}+Y^{\prime }_{k+1}$, i.e., $Y_{k}=\sum _{0 \le h \le k}Y^{\prime }_{h}$. Hence, it follows from $Y= \sup S$ that $Y= \sum _{k\ge 0} Y^{\prime }_{k}$.

The first item follows by the inductive hypothesis, since $Y$ is the supremum of $S$ and $Y_{k} \in S$ implies ${{\tt weight}} (Y_{k}) \le {{\tt weight}} (Z)$. As to the second item, we have $Y\bullet C[M]=\sup \lbrace Y_{k}\bullet C[M]\rbrace =\sum _{k \ge 0} Y^{\prime }_{k}\bullet C[M]$. We want to prove that if for some formal sum $X$ then .

If then, by the definition of the multi-step reduction relation (which guarantees that only a finite number of terms are evaluated in the formal sum), there is an $m\ge 0$ such that and $X=X^{\prime }+\,{{\tt val}}{(\sum _{k\gt m} Y^{\prime }_{k}\bullet C[M])}$.

For any $m^{\prime }\ge 0$, we have

Proof. We prove by induction on the length $n$ of the reduction that $M \, \mathcal {R}\,N$ and imply . If $Y= \emptyset ,$ then the result follows by the third set of ${\mathcal {S}}^{\prime }$. Suppose that $Y\ne \emptyset$. If $n=0,$ then we have two cases:

• $C=[\cdot ]$ and $M$ is a value. Then and since $\, \mathcal {R}\,$ is a finite-step simulation, we have , which implies that they are in $\mathrel {\mathcal {S}}^{\prime }_{(M,N)}$ as well.
  
• $C=\lambda x. C^{\prime }$. Then , by the first set of $\mathrel {\mathcal {S}}^{\prime }$.
  

Suppose now that .

• $C=[\cdot ]$ and . The result follows from the fact that $\, \mathcal {R}\,$ is a finite-step simulation, as in the first case of $n=0$.
  
• $C=C_{1} \oplus C_{2}$ and . Then , and $Y= { \frac{1}{2}};{Y_{1}}+ { \frac{1}{2}};{Y_{2}}$. We have and it follows from the inductive hypothesis on $n_{1}$ and $n_{2}$ that and . Hence, .
  
• $C=C_{1} C_{2}$. Then implies , where . Since $n_{1} \le n$ (by $Y\ne \emptyset$), we can apply the inductive hypothesis and derive , i.e., $Y_{1}= \sum _{j}{r_{j}}{\cdot }{Y^{\prime }_{j}}$ and for $Y^{\prime }_{j} \mathrel {\mathcal {S}}^{\prime }_{(M,N)} Z^{\prime }_{j}$. Hence, implies , with $\sum _{j}{n^{\prime }_{j}}=n_{2}$ and $Y= \sum _{j}{r_{j}}{\cdot }{Y^{\prime \prime }_{j}}$, and .
  Since $\,{{\tt lift}}{(\,{{\tt lift}}{(\, \mathcal {R}\,)}\,)}\,=\,{{\tt lift}}{(\, \mathcal {R}\,)}\,$ for any relation $\, \mathcal {R}$, the result follows if we can prove that for every $j\,$ implies . If $Y^{\prime }_{j} \mathrel {\mathcal {S}}^{\prime }_{(M,N)} Z^{\prime }_{j}$, then either $Y_{j}^{\prime }=\emptyset$ and the result trivially follows, or one of these cases hold:
  
  • $Y^{\prime }_{j}={{1};{\lambda x. C^{\prime }[M]}}$ and $Z^{\prime }_{j}= {{1};{\lambda x. C^{\prime }[N]}}$. Hence, either $Y^{\prime \prime }_{j} = \emptyset$, in which case the result follows by the third set of ${\mathcal {S}}^{\prime }$, or , with $n^{\prime \prime }_{j} \le n$. Terms and $C^{\prime }[N] \lbrace C_{2}[N]\!/\!x\rbrace$ are, respectively, of the form $C^{\prime \prime }[M]$ and $C^{\prime \prime }[N]$, so we can apply the inductive hypothesis to derive $ Y^{\prime \prime }_{j} \,{{\tt lift}}{(\mathrel {\mathcal {S}}^{\prime }_{(M,N)})}\, {Z^{\prime }_{j}\bullet C_{2} [N]}$.
    
  • $Y^{\prime }_{j}\, \mathcal {R}\,_{(M,N)} Z^{\prime }_{j}$. It is easy to check that iff for some ${Y^{\prime \prime \prime }_{j} \le _{{\rm {\tt apx}}}Y^{\prime }_{j} }$. Since $\, \mathcal {R}\,$ is finite-step simulation saturated by approximants, implies , and the result follows from $\, \mathcal {R}\,_{(M,N)} \subseteq \,{{\tt lift}}{(\mathrel {\mathcal {S}}^{\prime }_{(M,N)})}$.
    

Proof.

1. For the left to right inequality (i.e., ), we prove that implies for some $Z\le _{{\rm {\tt apx}}}Z^{\prime }$. Since implies and for some $Z^{\prime \prime }$. By definition , so we derive for some $Z^{\prime }$ such that $Z\le _{{\rm {\tt apx}}}Z^{\prime }$.
   For the converse inequality, we analogously prove that implies for some $Z\le _{{\rm {\tt apx}}}Z^{\prime }$. Since relations $\Longrightarrow$ and are small-step and finitary, although could have an infinite support (i.e., be a sum of infinitely many values) only a finite number of $\beta$-reductions substituting $N$ in a value of can be performed in the reduction . Hence, there is some formal sum $Z^{\prime \prime }$ with finite support such that and . This implies that for some $Z^{\prime \prime \prime }$ such that $Z^{\prime \prime } \le _{{\rm {\tt apx}}}Z^{\prime \prime \prime }$, which in turn implies for some $Z^{\prime }$ such that $Z\le _{{\rm {\tt apx}}}Z^{\prime }$.
   
2. The left to right inequality (i.e., ) follows trivially, since implies for some $Z^{\prime }$ such that $Z\le _{{\rm {\tt apx}}}Z^{\prime }$.
   To prove , we show that implies that there is a sequence of formal sums $\lbrace {Z}_{j}\rbrace _{j\ge 0}$ (for $j$ ranging over natural numbers) ordered with respect to $\le _{{\rm {\tt apx}}}$ such that for every $j$, and with $\sup \lbrace Z_{j}\rbrace _{j\ge 0}= Z$. Hence, the result follows, since
   
   and since for every $Z$ we have , we derive
   
   Hence, it remains to prove that implies that there is a (infinite) sequence of formal sums $\lbrace {Z}_{j}\rbrace _{j\ge 0}$ ordered with respect to $\le _{{\rm {\tt apx}}}$ such that for every $j$, and with $\sup \lbrace Z_{j}\rbrace _{j\ge 0}= Z$. Let $Y= \sum _{i \in I}{p_{i}};{\lambda x. P_{i}}$ and . It follows by the definition of that there is a finite $I^{\prime }\subseteq I$ and a formal sum $Z^{\prime }$ such that and (only a finite number of steps can be taken, and thus only a finite number of summands can move). Hence, by allowing all and only the summands with index $i \in I^{\prime }$ to perform the $\beta$-reduction substituting $N$ in $P_{i}$, we derive . Then, by allowing one at a time the summands of $Y$ with index $i \in I\backslash I^{\prime }$ to perform the $\beta$-reduction substituting $N$ in $P_{i}$, we obtain a sequence $\lbrace {Z}_{j}\rbrace _{j\ge 0}$, that starts from $Z_{0}=Z^{\prime }$ and progressively adds to it the values in one by one. This sequence is ordered with respect to $\le _{{\rm {\tt apx}}}$, it is such that for every $j$, and it has $\sup \lbrace Z_{j}\rbrace _{j\ge 0}= Z$.
   

Proof. We prove that $M \mathrel {\mathcal {R}}N$ and imply , by induction on $n$. If $Y= \emptyset ,$ then the result holds by the last set of ${\mathcal {R}}^{\prime }$. Suppose that $Y\ne \emptyset$. If $n=0,$ then we have two cases:

• $C=[\cdot ]$ and $M$ is a value. Then and we have .
  
• $C=\lambda x. C^{\prime }$. Then .
  

Suppose now that .

• $C=[\cdot ]$ and . The result follows from the fact that $\, \mathcal {R}\,$ is a finite-step simulation up-to lifting and context, as in the first case of $n=0$.
  
• $C=C_{1} \oplus C_{2}$ and . Then , with $n_{1}+n_{2}\le n$ and $Y= { \frac{1}{2}};{Y_{1}}+ { \frac{1}{2}};{Y_{2}}$. We have and it follows from the inductive hypothesis on $n_{1}$ and $n_{2}$ that and . Hence, we derive .
  
• $C=C_{1} C_{2}$. Then implies , where . Since $n_{1} \le n$ (by $Y\ne \emptyset$), we can apply the inductive hypothesis and derive , i.e., $Y_{1}= \sum _{j}{r_{j}}{\cdot }{Y^{\prime }_{j}}$ and for $Y^{\prime }_{j} {\mathcal {R}}^{\prime }_{(M,N)} Z^{\prime }_{j}$. Hence, implies , with $\sum _{j}{n^{\prime }_{j}}=n_{2}$ and $Y= \sum _{j}{r_{j}}{\cdot }{Y^{\prime \prime }_{j}}$, and
  
  Since $\,{{\tt lift}}{(\,{{\tt lift}}{(\, \mathcal {R}\,)}\,)}\,=\,{{\tt lift}}{(\, \mathcal {R}\,)}\,$ for any relation $\, \mathcal {R}$, the result follows if we can prove that for every $j\,$ implies . If $Y^{\prime }_{j} \mathrel {\mathcal {R}}^{\prime }_{(M,N)} Z^{\prime }_{j},$ then one of the following cases holds:
  
  • $Y^{\prime }_{j}={{1};{\lambda x. C^{\prime }[M]}}$ and $Z^{\prime }_{j}= {{1};{\lambda x. C^{\prime }[N]}}$. Hence, either $Y^{\prime \prime }_{j} = \emptyset$, in which case the result follows by the last set of ${\mathcal {R}}^{\prime }$, or , with $n^{\prime \prime }_{j} \le n$. Terms and are, respectively, of the form $C^{\prime \prime }[M]$ and $C^{\prime \prime }[N]$, and we can apply the inductive hypothesis to derive .
    
  • $Y^{\prime }_{j} \le _{{\rm {\tt apx}}}X\, \mathcal {R}\,_{(M,N)} Z^{\prime }_{j}$. If $Y^{\prime }_{j} C_{2}[M] \Longrightarrow Y^{\prime \prime }_{j}$, then there is a $X^{\prime }$ such that and $Y^{\prime \prime }_{j} \le _{{\rm {\tt apx}}}X^{\prime }$, for some $n^{\prime \prime }_{j}\le n^{\prime }_{j}$. It is easy to check that there exists a $X^{\prime \prime }$ such that and $X^{\prime } \le _{{\rm {\tt apx}}}X^{\prime \prime }$, for some $n^{\prime \prime \prime }_{j} \lt n^{\prime \prime }_{j}$. Since $X\, \mathcal {R}\,_{(M,N)} Z^{\prime }_{j}$, there are two cases:
    
    • $X\bullet C_{2}[M] \Longrightarrow F$ and $Z^{\prime }_{j}\bullet C_{2} [N] \Longrightarrow G$ with $F\,{{\tt lift}}{({{\tt dirac}}{({(M,N)}^{{\star }})})}\, G$.
      Hence, with $X^{\prime \prime } \le _{{\rm {\tt apx}}}X^{\prime \prime \prime }$, for some $n^{\prime \prime \prime \prime }_{j}\le n^{\prime \prime \prime }_{j} \lt n$. We can apply the inductive hypothesis to the pairs in ${{(M,N)}^{{\star }}}$ whose projections, respectively, compose $F$ and $G$ through the lifting, and derive . It follows from $Y^{\prime \prime }_{j} \le _{{\rm {\tt apx}}}X^{\prime \prime \prime }$ that .
      
    • .
      As $Y^{\prime \prime }_{j} \le _{{\rm {\tt apx}}}X^{\prime \prime }$, we then derive , since $\,{{\tt lift}}{(\mathrel {\mathcal {R}}^{\prime }_{(M,N)})}\,$ is saturated by approximants.
      
  • the result is immediate if $Y^{\prime }_{j} =\emptyset$.
    

Proof. We first prove (*). Let $P=P_{1}, P_{2},\ldots,P_{k}=P^{\prime }$ be such that for every $i$, for $1 \le i \lt k$, there are a context $C_{i}$ and tuples $\widetilde{P_{i}}, \widetilde{P^{\prime }_{i}}$ with $P_{i}= C_{i}[\widetilde{P_{i}}]$ and $P_{i+1}=C_{i}[\widetilde{P^{\prime }_{i}}]=C_{i+1}[\widetilde{P}_{i+1}]$ and . Suppose that . We prove by induction on $k$ that for every $i$ such that $1 \le i \lt k$, we have and $m_{i} \ge m_{i+1}$ and .

The result is trivial for $k=1$. Suppose that $k=k^{\prime }+1$. The result follows from the inductive hypothesis and from

• if $C=[\cdot ],$ then the result immediately follows by .
  
• $C=C_{1}\oplus C_{2}$. Then there are $Y_{1},Y_{2}$ such that $Y= { \frac{1}{2}};{Y_{1}}+{ \frac{1}{2}};{Y_{2}}$ and $C_{i}[\widetilde{P}] \Longrightarrow _{m_{i}} Y_{i}$ for $i =1,2$ and $m_{i} \lt m+1$. The result follows from the inductive hypothesis
  
• $C= C_{1} C_{2}$. If $C_{1}[\widetilde{P}]$ is a value, then, by the definition of , $C_{1}[\widetilde{P}^{\prime }]$ is exactly the same value. Then the terms resulting after the $\beta$-reduction are in , and we conclude by the inductive hypothesis.
  If then we can apply the inductive hypothesis to $m_{i}$ and the result follows.
  

We can now prove (**) by showing by induction on $n$ that and imply .

Let , $P^{\prime }=C[M]$ and $Q=C[N]$. If $n=0$ and $Y\ne \emptyset ,$ then $P$ is a value, $Y={1};{P}$ and by (*) $P^{\prime }$ is a value too, with . We have two cases:

• $C=[\cdot ]$, with ${P^{\prime }=M}$ a value, and $Q=N$.
  By the definition of $\mathrel {\mathrel {{\mathcal {T}}_{(M,N)}}}$, we have and it follows from that .
  
• $P^{\prime }=\lambda x. C^{\prime }[M]$ and $Q=\lambda x. C^{\prime }[N]$.
  Then .
  

If then by (*), we have with $m \le n+1$ and . Suppose that $Y^{\prime } \ne \emptyset$. We have three cases:

• $C=[\cdot ]$. If then . For any term relations ${\mathcal {S}},{\mathcal {S}}^{\prime }$, we have
  
  • ${{\tt liftd}}{({\mathcal {S}})}\,{{\tt dirac}}{({\mathcal {S}}^{\prime })} \subseteq {{\tt disliftd}}({{\mathcal {S}}{\mathcal {S}}^{\prime }})$
    
  • $\le _{{\rm {\tt apx}}}{{\tt disliftd}}({\mathrel {\mathrel {{\mathcal {T}}_{(M,N)}}}})$ $\subseteq$ ${{\tt disliftd}}({\mathrel {\mathrel {{\mathcal {T}}_{(M,N)}}}}) \le _{{\rm {\tt apx}}}$
    
  Hence, we derive .
  
• $C=C_{1}+C_{2}$. Then there are $Y_{1},Y_{2}$ such that $Y^{\prime }= { \frac{1}{2}};{Y_{1}}+{ \frac{1}{2}};{Y_{2}}$ and $C_{i}[M] \Longrightarrow _{m_{i}} Y_{i}$ for $i =1,2$ and $m_{i} \le n$. By the inductive hypothesis, we have
  
  As $\,{{\tt lift}}{({{\tt disliftd}}({\cdot }))}\,= {{\tt disliftd}}({\cdot })$ and $\,{{\tt liftd}}{({\mathcal {S}})}\,{{\tt disliftd}}({{\mathcal {S}}^{\prime }})$ $\subseteq$ ${{\tt disliftd}}({{\mathcal {S}}{\mathcal {S}}^{\prime }})$ for any ${\mathcal {S}}$ and ${\mathcal {S}}^{\prime }$, from , we derive
  
  
  
• $C= C_{1} C_{2}$. We consider two cases:
  
  • $C_{1}[M]=M$ and $M=\lambda x. M^{\prime }$ and $N= \lambda x. N^{\prime }$ are values.
    Then $M \mathrel {\mathrel {{\mathcal {T}}_{(M,N)}}}N$, and we have iff , with $m^{\prime } \lt m \le n+1$ and , where (note that here the determinism of the reduction to $F$ is used to guarantee that and that $m^{\prime } \lt m \le n+1$). Hence, we have , with either (which implies $Y_{i} {{\tt dirac}}{(\mathrel {{\mathcal {R}}_{(M,N)}})}Z_{i}$) or and for and $m_{i} \le m^{\prime } \lt n+1$, and by applying the inductive hypothesis, we derive $Y_{i} {{\tt disliftd}}({\mathrel {{\mathcal {R}}_{(M,N)}}}) \le _{{\rm {\tt apx}}}Z_{i}$. Therefore, , and the result follows.
    
  • $C_{1}[M]=\lambda x. C^{\prime }_{1}[M]$ and $C_{1}[N]=\lambda x. C^{\prime }_{1}[N]$.
    We can apply the inductive hypothesis to to derive
    
    then we have , which implies the result.
    

Proof. We have the three cases below:

• If $\lambda x. P_{i}= \lambda x. C^{\prime }[M, \widetilde{V}_{i}]$ and $\lambda x. Q_{j}=\lambda x. C^{\prime }[N, \widetilde{W}_{j}]$ for some location-free context $C^{\prime }$, then there is a location-free context $C^{\prime \prime }$ such that
  
  and the first item holds.
  
• If there is an $r$ such that $\lambda x. P_{i}= (\widetilde{V}^{\prime }_{i})_{r}$ and $\lambda x. Q_{j}=(\widetilde{W}^{\prime }_{j})_{r}$ for some
  \[ \mathbf {Y}^{\prime }= \sum _{i}{p_{i}};{s_{i} ;\widetilde{V}^{\prime }_{i}} \mathrel {{\mathcal {R}}_{(M,N)}} \sum _{j}{q_{j}};{t_{j};\widetilde{W}^{\prime }_{j}} =\mathbf {Z}^{\prime }, \]
  such that $(\mathbf {Y}^{\prime },\mathbf {Z}^{\prime }) \le _{{\rm {\tt cce}}(M,N)}(\mathbf {Y},\mathbf {Z})$, then it follows from the fact that ${\mathcal {R}}$ is a finite-step simulation that implies
  
  Since implies
  
  we derive
  
  
  
• If $\lambda x. P_{i}= M$ and $\lambda x. Q_{j}= N,$ then $M$ and $N$ are values and by clause (2g) applied to $\mathrel {{\mathcal {R}}_{(M,N)}}$,
  \[ \sum _{i}{p_{i}};{s_{i};\widetilde{V}^{\prime }_{i}, M} \mathrel {{\mathcal {R}}_{(M,N)}} \sum _{j}{q_{j}};{t_{j};\widetilde{W}^{\prime }_{j}, N,} \]
  for some $( \sum _{i}{p_{i}};{s_{i};\widetilde{V}^{\prime }_{i}}, \sum _{j}{q_{j}};{t_{j};\widetilde{W}^{\prime }_{j}}) \le _{{\rm {\tt cce}}(M,N)}(\mathbf {Y},\mathbf {Z})$. By clause (2b) applied to $\mathrel {{\mathcal {R}}_{(M,N)}}$, from we derive
  
  
  By the assumptions $\lambda x. P_{i}= M$ and $\lambda x. Q_{j}= N$ there are already columns in the dynamic environments of $\mathbf {Y}$ and $\mathbf {Z}$ composed by $M$ and $N,$ respectively; thus,
  
  from which the result follows.
  

Proof. Suppose that $\mathbf {Y}= \sum _{i}{p_{i}};{s_{i};\widetilde{V}_{i}} \mathrel {\mathcal {R}_{(M,N)}^{{\rm {\tt cce}}}} \sum _{j}{q_{j}};{t_{j};\widetilde{W}_{j}}=\mathbf {Z}$, with $\mathbf {Y}^{\prime }= \sum _{i}{p_{i}};{s_{i};\widetilde{V}^{\prime }_{i}}$ and $ \mathbf {Z}^{\prime }= \sum _{j}{q_{j}};{t_{j};\widetilde{W}^{\prime }_{j}}$ related by $\mathrel {{\mathcal {R}}_{(M,N)}}$ and such that $(\mathbf {Y}^{\prime },\mathbf {Z}^{\prime }) \le _{{\rm {\tt cce}}(M,N)}(\mathbf {Y},\mathbf {Z})$.

We prove by induction on $n$ and then by induction on the structure of $C$ that

implies .

(In the proof, we sometimes assume that $\widetilde{V}_{i}=\widetilde{V}^{\prime }_{i},\widetilde{V}^{\prime \prime }_{i}$ and $\widetilde{W}_{j}=\widetilde{W}^{\prime }_{j},\widetilde{W}^{\prime \prime }_{j}$. This does not affect the results, since the context closure of environments allows us to permute the columns in the formal sums.)

If $\mathbf {W}= \emptyset ,$ then the result follows by the fact that ${\mathcal {R}}$ is saturated by $\emptyset$. Suppose that $\mathbf {W}\ne \emptyset$ and $n=0$. We have one of the following cases:

• $C=[\cdot ]_{1}$ and $M$ is a value. Then,
  
  and we derive
  
  
  
• $C \ne [\cdot ]_{1}$ and for every $i,j$, $C[M,\widetilde{V}_{i}]$ and $C[N,\widetilde{W}_{j}]$ are values. Then it follows from the definition of $\le _{{\rm {\tt cce}}(M,N)}$ that
  
  
  

Suppose now that , with $\mathbf {W}\ne \emptyset$. We have the following cases:

• $C=[\cdot ]_{1}$ and $M$ is not a value. Then the result follows analogously to the $n=0$ case.
  
• $C=C_{1}\oplus C_{2}$. In this case implies
  \[ \sum _{i}{p_{i}};{ s_{i} ;\widetilde{V}_{i}};{(C_{1} \oplus C_{2})[M,\widetilde{V}_{i}]} \longrightarrow \frac{1}{2}\cdot \sum _{i}{p_{i}};{ s_{i} ;\widetilde{V}_{i}};{C_{1} [M,\widetilde{V}_{i}]} + \frac{1}{2} \sum _{i}{p_{i}};{ s_{i} ;\widetilde{V}_{i}};{C_{2}[M,\widetilde{V}_{i}],} \]
  and $\mathbf {W}= \frac{1}{2}\cdot \mathbf {W}_{1} + \frac{1}{2}\cdot \mathbf {W}_{2}$, with , for $h=1,2$ and $n_{h} \le n$. Since
  
  we can apply the inductive hypothesis to $n_{1}$ and $n_{2}$ and derive
  
  The result follows from $\,{{\tt lift}}{(\,{{\tt lift}}{({\mathcal {R}})}\,)}\,=\,{{\tt lift}}{({\mathcal {R}})}$.
  
• $C=C_{1} C_{2}$.
  Suppose that there exists some $i$ such that ${C_{1} [M,\widetilde{V}_{i}]}$ is not a value, and such that ${C_{1} [M,\widetilde{V}_{i}]}$ performs some small steps in the reduction leading to $\mathbf {W}$. Hence, there is a set $I^{\prime } \subseteq I$ such that
  
  with $n_{1} \gt 1$ and
  
  We have
  
  for . Then we can apply the inductive hypothesis to $n_{1}$ and derive
  \[ \sum _{i \in I^{\prime },k}{p_{i,k}};{s_{i,k} ;\widetilde{V}_{i},V_{i,k}} \,{{\tt lift}}{\big(\!\ge _{{\rm {\tt env}}}\big(\!\mathrel {\mathcal {R}_{(M,N)}^{{\rm {\tt cce}}}}\!\big)\big)}\, \sum _{j \in J^{\prime },h}{q_{j,h}};{t_{j,h};\widetilde{W}_{j},W_{j,h} }, \]
  which is equivalent to saying
  \[ \left( \sum _{i \in I^{\prime },k}{p_{i,k}};{s_{i,k} ;\widetilde{V}_{i},V_{i,k}}, \sum _{j \in J^{\prime },h}{q_{j,h}};{t_{j,h};\widetilde{W}_{j},W_{j,h} }\right) \le _{{\tt lift}}\le _{{\rm {\tt env}}}\lbrace (\mathbf {Y}_{g}, \mathbf {Z}_{g})\rbrace _{g} \subseteq \mathrel {\mathcal {R}_{(M,N)}^{{\rm {\tt cce}}}}, \]
  with $\mathbf {Y}_{g}= \sum _{i,k \in I_{g}}{p^{\prime }_{i,k}};{s_{i,k} ;\widetilde{V}_{i,k}},$ and $\mathbf {Z}_{g}= \sum _{j,h \in J_{g}}{q^{\prime }_{j,h}};{t_{j,h};\widetilde{W}_{j,h}}$ such that for every $g$ there is a context $C_{g}$ such that for all $i,k \in I_{g}$ and for all $j,h \in J_{g}$, we have $V_{i,k} C_{2}[M,\widetilde{V}_{i}]= C_{g}[M, \widetilde{V}_{i,k}]$ and $W_{j,h} C_{2}[N,\widetilde{W}_{j}]= C_{g}[N, \widetilde{W}_{j,h}]$.
  If then for every $g$ there is a $\mathbf {W}_{g}$ such that and $\sum _{g} n^{\prime }_{g}=n_{2}$ and
  
  By the inductive hypothesis on each of the $n^{\prime }_{g}$, we derive
  
  from which the result follows by $\,{{\tt lift}}{(\ge _{{\rm {\tt env}}}(\,{{\tt lift}}{(\ge _{{\rm {\tt env}}}({\mathcal {R}}))}\,))}\,=\,{{\tt lift}}{(\ge _{{\rm {\tt env}}}({\mathcal {R}}))}\,$.
  We now consider the case when no $C_{1}[M, \widetilde{V}_{i}]$ contributes to the multi-step reduction to $\mathbf {W}$. If there exist some $i$ such that ${C_{2} [M,\widetilde{V}_{i}]}$ contributes to the multi-step reduction to $\mathbf {W}$, then we can derive the result using the same reasoning as above.
  Otherwise, there is a set $I^{\prime } \subseteq I$ such that $C_{1} [M,\widetilde{V}_{i}]$ and $C_{2} [M,\widetilde{V}_{i}]$ are values for every $i \in I^{\prime }$, and
  
  with $n_{1}\le n+1$ and $n_{2} \le n$.
  Suppose that $C_{1}[N,\widetilde{W}_{j}] = \lambda x. Q_{j}$ is a value, for all $j$, and $C_{2}[N,\widetilde{W}_{j}]$ is a value. Then,
  
  Since ${\mathcal {R}}$ is saturated by approximants,
  \[ \sum _{i \in I^{\prime }}{p_{i}};{s_{i} ;\widetilde{V}_{i}} \mathrel {\mathcal {R}_{(M,N)}^{{\rm {\tt cce}}}} \sum _{j}{q_{j}};{t_{j};\widetilde{W}_{j}}, \]
  which implies, by Lemma 63, that one of the following holds:
  
  • there is a context $C^{\prime }$ such that
    
    and
    
    Then, we can apply the inductive hypothesis on the reduction
    
    and derive the result.
    
  • for any $\mathbf {W}^{\prime }$, if , then
    
    Then, we have
    
    and the result follows by $\ge _{{\rm {\tt env}}}{\,{{\tt lift}}{({\mathcal {R}})}\,} \subseteq \,{{\tt lift}}{(\ge _{{\rm {\tt env}}}({\mathcal {R}}))}\,$.
    
  It remains to consider the case when $C_{1}[N,\widetilde{W}_{j}]$ or $C_{2}[N,\widetilde{W}_{j}]$ are not values for some $j$. If $C_{1}[N,\widetilde{W}_{j}]$ is not a value for some $j,$ then $C_{1}=[\cdot ]_{1}$ and $N$ is not a value. Suppose $C_{2}[N,\widetilde{W}_{j}]$ is a value for all $j$. Then, we have
  
  for . Since ${\mathcal {R}}$ is a finite-step simulation saturated by approximants, by clause (2g), we derive
  \[ \sum _{i \in I^{\prime }}{p_{i}};{s_{i} ;\widetilde{V}^{\prime }_{i}, \lambda x. P_{i}} \,{{\tt lift}}{(\mathrel {{\mathcal {R}}_{(M,N)}})}\, \sum _{j \in J^{\prime },h}{q_{j,h}};{t_{j,h};\widetilde{W}^{\prime }_{j},\lambda x. Q_{j,h} }, \]
  which implies
  \[ \sum _{i \in I^{\prime }}{p_{i}};{s_{i} ;\widetilde{V}_{i}, \lambda x. P_{i}} \,{{\tt lift}}{\big(\!\mathrel {\mathcal {R}_{(M,N)}^{{\rm {\tt cce}}}}\!\big)}\, \sum _{j \in J^{\prime },h}{q_{j,h}};{t_{j,h};\widetilde{W}_{j},\lambda x. Q_{j,h} }. \]
  Then,
  \[ \left( \sum _{i \in I^{\prime }}{p_{i}};{s_{i} ;\widetilde{V}_{i}, \lambda x. P_{i}} , \sum _{j \in J^{\prime },h}{q_{j,h}};{t_{j,h};\widetilde{W}_{j},\lambda x. Q_{j,h} }\right) \le _{{\tt lift}}\lbrace (\mathbf {Y}_{g}, \mathbf {Z}_{g})\rbrace _{g} \subseteq \mathrel {\mathcal {R}_{(M,N)}^{{\rm {\tt cce}}}}, \]
  with $\mathbf {Y}_{g}= \sum _{i\in I_{g}}{p^{\prime }_{i}};{s_{i} ;\widetilde{V}_{i}, \lambda x. P_{i}}$ and $\mathbf {Z}_{g}= \sum _{j,h\in J_{g}}{q^{\prime }_{j,h}};{t_{j,h};\widetilde{W}_{j},\lambda x. Q_{j,h}},$ such that for every $g$, we have
  \[ \sum _{i\in I_{g}}{p^{\prime }_{i}};{ s_{i} ;\widetilde{V}_{i}, \lambda x. P_{i}};{\lambda x. P_{i} C_{2}[M,\widetilde{V}_{i}]} \]
  and
  \[ \sum _{j,h\in J_{g}}{q^{\prime }_{j,h}};{ t_{j,h};\widetilde{W}_{j},\lambda x. Q_{j,h}};{\lambda x. Q_{j,h} C_{2}[N,\widetilde{W}_{j}],} \]
  which satisfy the premises of Lemma 63. Then, we can proceed as in the previous case and derive that implies
  
  from which the result follows.
  Finally, if there are some $j$ such that $C_{2}[N,\widetilde{W}_{j}]$ is not a value, then we can proceed as in the previous case, exploiting clause (2g) on ${\mathcal {R}}_{(M,N)}$ to evaluate $N$ in argument position as well.
  
• case $C=! C^{\prime }$.
  The interesting case is when $C^{\prime }[M,\widetilde{V}_{i}]$ does not contribute to the reduction, for every $i$ (otherwise, we can apply the inductive hypothesis analogously to the application case), i.e., there is a subset $I^{\prime } \subseteq I$, such that
  \[ \sum _{i \in I^{\prime }}{p_{i}};{ s_{i} ;\widetilde{V}_{i}};{!C^{\prime }[M,\widetilde{V}_{i}]}= \sum _{i \in I^{\prime }}{p_{i}};{ s_{i} ;\widetilde{V}_{i}};{!l_{i}} \Longrightarrow _{n+1} \sum _{i \in I^{\prime }}{p_{i}};{s_{i} ;\widetilde{V}_{i},s_{i}(l_{i}).} \]
  
  Since ${\mathcal {R}}$ is saturated by approximants, $ \sum _{i \in I^{\prime }}{p_{i}};{s_{i} ;\widetilde{V}^{\prime }_{i}} \mathrel {{\mathcal {R}}_{(M,N)}} \sum _{j}{q_{j}};{t_{j};\widetilde{W}^{\prime }_{j}}$.
  Since contexts are location-free, there are two cases:
  
  • $C^{\prime }[M,\widetilde{V}_{i}] \in \widetilde{V}^{\prime }_{i}$. Then, $C^{\prime }[N,\widetilde{W}_{j}]=l^{\prime }_{j} \in \widetilde{W}^{\prime }_{j}$ and by clause (2c) on ${\mathcal {R}}$, we have
    \[ \sum _{i \in I^{\prime }}{p_{i}};{s_{i} ;\widetilde{V}^{\prime }_{i}, s_{i}(l_{i})} \,{{\tt lift}}{(\mathrel {{\mathcal {R}}_{(M,N)}})}\, \sum _{j}{q_{j}};{t_{j};\widetilde{W}^{\prime }_{j}, t_{i}(l^{\prime }_{j}),} \]
    and the result follows from
    
    
    
  • $C=[\cdot ]_{1}$ and $M=l$.
    Suppose that $N=l^{\prime }$. Then by clause (2g), we have
    \[ \sum _{i \in I^{\prime }}{p_{i}};{s_{i} ;\widetilde{V}^{\prime }_{i},M} \mathrel {{\mathcal {R}}_{(M,N)}} \sum _{j}{q_{j}};{t_{j};\widetilde{W}^{\prime }_{j}, N,} \]
    and by clause (2c)
    \[ \sum _{i \in I^{\prime }}{p_{i}};{s_{i} ;\widetilde{V}^{\prime }_{i},M, s_{i}(l_{i})} \,{{\tt lift}}{(\mathrel {{\mathcal {R}}_{(M,N)}})}\, \sum _{j}{q_{j}};{t_{j};\widetilde{W}^{\prime }_{j}, N, t_{j}(l^{\prime }_{j}).} \]
    Then,
    \[ \sum _{i \in I^{\prime }}{p_{i}};{s_{i} ;\widetilde{V}_{i}, s_{i}(l_{i})} \,{{\tt lift}}{\big(\!\ge _{{\rm {\tt env}}}\big(\!\mathrel {\mathcal {R}_{(M,N)}^{{\rm {\tt cce}}}}\!\big)\big)}\, \sum _{j}{q_{j}};{t_{j};\widetilde{W}_{j}, t_{j}(l^{\prime }_{j}).} \]
    The case when $N$ is not a value follows analogously.
    
• $C=C_{1}:=C_{2}$.
  Again, the interesting case is when for every $i$ neither $C_{1}[M,\widetilde{V}_{i}]$ nor $C_{2}[M,\widetilde{V}_{i}]$ contributes to the reduction, i.e., there is a subset $I \subseteq I^{\prime }$ such that
  
  
  As above, since ${\mathcal {R}}$ is saturated by approximants, $ \sum _{i \in I^{\prime }}{p_{i}};{s_{i} ;\widetilde{V}^{\prime }_{i}} \mathrel {{\mathcal {R}}_{(M,N)}} \sum _{j}{q_{j}};{t_{j};\widetilde{W}^{\prime }_{j}}$ and, since contexts are location-free, there are two cases:
  
  • $C_{1}[M,\widetilde{V}_{i}] \in \widetilde{V}^{\prime }_{i}$. Then $C_{1}[N,\widetilde{W}_{j}]=l^{\prime }_{j} \in \widetilde{W}^{\prime }_{j}$. Suppose that $C_{2}[N,\widetilde{W}_{j}]=U_{j}$ is a value for every $j$. Then $(\lbrace T_{i}\rbrace _{i}, \lbrace U_{j}\rbrace _{j}) \in (\lbrace M,\widetilde{V}^{\prime }_{i}\rbrace _{i}, \lbrace N,\widetilde{W}^{\prime }_{j}\rbrace _{j})^{\widehat{\star }}$ and by clause (2c) on ${\mathcal {R}}$, we have
    \[ \sum _{i \in I^{\prime }}{p_{i}};{s_{i}[l_{i} \rightarrow T_{i}];\widetilde{V}^{\prime }_{i}} \,{{\tt lift}}{(\mathrel {{\mathcal {R}}_{(M,N)}})}\, \sum _{j}{q_{j}};{t_{j}[l^{\prime }_{j} \rightarrow U_{j}];\widetilde{W}^{\prime }_{j}}, \]
    and the result follows.
    If $C_{2}[N,\widetilde{W}_{j}]$ is not a value for some $j,$ then $C_{2}[M,\widetilde{V}_{j}]=M$ and $C_{2}[N,\widetilde{W}_{j}]=N$. Then, we derive from clause (2g) that
    
    and we can derive, as in the previous case, that
    \[ \sum _{i \in I^{\prime }}{p_{i}};{s_{i}[l_{i} \rightarrow M];\widetilde{V}^{\prime }_{i},M} \,{{\tt lift}}{(\mathrel {{\mathcal {R}}_{(M,N)}})}\, \sum _{j,h}{q_{j}};{t_{j}[l^{\prime }_{j} \rightarrow U_{j,h}];\widetilde{W}^{\prime }_{j},U_{j,h}}, \]
    from which the result follows.
    
  • $C=[\cdot ]_{1}$ and $M=l$.
    Suppose that $N=l^{\prime }$ and $C_{2}[N,\widetilde{W}_{j}]=U_{j}$ is a value for every $j$. Then, $(\lbrace T_{i}\rbrace _{i}, \lbrace U_{j}\rbrace _{j}) \in (\lbrace M,\widetilde{V}^{\prime }_{i}\rbrace _{i}, \lbrace N,\widetilde{W}^{\prime }_{j}\rbrace _{j})^{\widehat{\star }}$. Then by clause (2g), we have
    \[ \sum _{i \in I^{\prime }}{p_{i}};{s_{i} ;\widetilde{V}^{\prime }_{i},M} \mathrel {{\mathcal {R}}_{(M,N)}} \sum _{j}{q_{j}};{t_{j};\widetilde{W}^{\prime }_{j}, N,} \]
    and by clause (2c) on ${\mathcal {R}}$, we have
    \[ \sum _{i \in I^{\prime }}{p_{i}};{s_{i}[l \rightarrow T_{i}];\widetilde{V}^{\prime }_{i},M} \,{{\tt lift}}{(\mathrel {{\mathcal {R}}_{(M,N)}})}\, \sum _{j}{q_{j}};{t_{j}[l^{\prime } \rightarrow U_{j}];\widetilde{W}^{\prime }_{j},N,} \]
    and the result follows.
    If $N$ or $C_{2}[N,\widetilde{W}_{j}]$ are not values, then we proceed analogously to the previous cases, by proving that we can add to the environment the values they evaluate to while staying in relation $\mathrel {{\mathcal {R}}_{(M,N)}}$.
    
• $C=({\boldsymbol \nu } \,x\:{:=} C_{1}) {C_{2}}$, with $C_{2}$ a context with free variable $x$.
  We consider the case when
  
  and $C_{1}[M,\widetilde{V}_{i}]=U_{j}$ is a value for every $j$, thus
  
  for $(\lbrace T_{i}\rbrace _{i}, \lbrace U_{j}\rbrace _{j}) \in (\lbrace M,\widetilde{V}^{\prime }_{i}\rbrace _{i}, \lbrace N,\widetilde{W}^{\prime }_{j}\rbrace _{j})^{\widehat{\star }}$ and for locations $(\lbrace l_{i}\rbrace _{i}, \lbrace k_{j}\rbrace _{j}),$ which are $(\lbrace s_{i}\rbrace _{i}, \lbrace t_{j}\rbrace _{j})$-fresh. By clauses (2d) and (2c), we have
  \[ \sum _{i \in I^{\prime }}{p_{i}};{s_{i}[l_{i} \rightarrow T_{i}];\widetilde{V}^{\prime }_{i},l_{i}} \mathrel {{\mathcal {R}}_{(M,N)}} \sum _{j}{q_{j}};{t_{j}[k_{j} \rightarrow U_{j}];\widetilde{W}^{\prime }_{j},k_{j}}, \]
  which implies
  
  Then the result follows from the inductive hypothesis on $n_{2}$.
  
• case $C=\:{{\rm {\tt if}}}\:\ C_{1}\ \:{{\rm {\tt then}}}\:\ C_{2}\ \:{{\rm {\tt else}}}\:\ C_{3}$ and case $C={\tt op}(C_{1}, \ldots ,C_m)$.
  The result follows from the fact that $\mathrel {\mathcal {R}_{(M,N)}^{{\rm {\tt cce}}}}$ satisfies clause (2e) for constants and then from the inductive hypothesis.
  
• $C=(C_{1},\ldots,C_{m})$.
  Since the multi-step reduction to $\mathbf {W}$ has length strictly greater than one, there is some $z$ such that $1 \le z \le m$ and some $i$ such that $C_{z}[M,\widetilde{V}_{i}]$ contributes to the multi-step reduction to $\mathbf {W}$. Then, we can apply the inductive hypothesis on the contexts to $C_{z}$ and derive that
  
  for $n^{\prime } \le n+1$ implies
  
  i.e.,
  \[ \left( \sum _{i \in I^{\prime },k}{p_{i,k}};{s_{i,k} ;\widetilde{V}_{i},V_{i,k}}, \sum _{j \in J^{\prime },h}{q_{j,h}};{t_{j,h};\widetilde{W}_{j},W_{j,h} }\right) \le _{{\tt lift}}\le _{{\rm {\tt env}}}\lbrace (\mathbf {Y}_{g}, \mathbf {Z}_{g})\rbrace _{g} \subseteq \mathrel {\mathcal {R}_{(M,N)}^{{\rm {\tt cce}}}}, \]
  with $\mathbf {Y}_{g}= \sum _{i,k \in I_{g}}{p^{\prime }_{i,k}};{s_{i,k} ;\widetilde{V}_{i,k}}$ and $\mathbf {Z}_{g}= \sum _{j,h \in J_{g}}{q^{\prime }_{j,h}};{t_{j,h};\widetilde{W}_{j,h}},$ and for every $g$ there is a context $C_{g}$ such that for every $i,k \in I_{g}$ and $j,h \in J_{g}$:
  
  (where the substitution only concerns the specific instance of $C_{z}[M,\widetilde{V}_{i}]$ in $C_{z}[M,\widetilde{V}_{i}]$ that occurs as the $z$th element of the tuple $C[M,\widetilde{V}_{i}]$, and the same for $C_{z}[N,\widetilde{W}_{i}]$). Finally, we derive the result by applying the inductive hypothesis on the number of reductions from
  \[ \sum _{i,k \in I_{g}}{p^{\prime }_{i,k}};{ s_{i,k} ;\widetilde{V}_{i,k}};{C_{g}[M,\widetilde{V}_{i,k}]}. \]
  
  
• $C= \#_{z}(C^{\prime })$.
  We consider the case when $C^{\prime }[M,\widetilde{V}_{i}]=(V_{i,1},\ldots,V_{i,m})$ is a value for every $i$ and
  \[ \begin{array}{l} \displaystyle\sum _{i \in I}{p_{i}};{ s_{i} ;\widetilde{V}_{i}};{\#_{z}(C^{\prime }[M,\widetilde{V}_{i}])} \longrightarrow \mathbf {W}= \displaystyle\sum _{i \in I}{p_{i}};{s_{i} ;\widetilde{V}_{i},V_{i,z}}. \end{array} \]
  We have three cases:
  
  • $C^{\prime }[M,\widetilde{V}_{i}]=(V_{i,1},\ldots,V_{i,m}) \in \widetilde{V}^{\prime }_{i}$.
    Then $C^{\prime }[N,\widetilde{W}_{j}]=(U_{j,1},\ldots,U_{j,m})\in \widetilde{W}^{\prime }_{j}$, and we have, by clause (2f) on ${\mathcal {R}}$,
    \[ \sum _{i }{p_{i}};{s_{i};\widetilde{V}^{\prime }_{i}, V_{i,1},\ldots,V_{i,m}} \,{{\tt lift}}{(\mathrel {{\mathcal {R}}_{(M,N)}})}\, \sum _{j}{q_{j}};{t_{j};\widetilde{W}^{\prime }_{j}, U_{j,1},\ldots,U_{j,m} }. \]
    Therefore,
    
    
    
  • $C^{\prime }[M,\widetilde{V}_{i}]=(C_{1}[M,\widetilde{V}_{i}],\ldots, C_{m}[M,\widetilde{V}_{i}])$ and $C^{\prime }[N,\widetilde{W}_{j}]=(C_{1}[N,\widetilde{W}_{j}],\ldots, C_{m}[N,\widetilde{W}_{j}])$.
    The result directly follows from the definition of the preorder $\le _{{\rm {\tt cce}}(M,N)}$.
    
  • $C^{\prime }=[\cdot ]_{1}$.
    The result follows from clauses (2g) and (2f) for ${\mathcal {R}}$.
    

Proof. We can assume that the relation $\mathrel {{\mathcal {R}}_{(M,N)}}$ is closed by $\lbrace \widetilde{l}\rbrace$ , i.e., each location $l \in \lbrace \widetilde{l}\rbrace$ occurs in corresponding columns in the dynamic environment of the formal sums (formally: for any $\mathbf {Y},\mathbf {Z}$ in the relation and for every $l \in \lbrace \widetilde{l}\rbrace$ there is an index $r$, for $ 1\le r \le |\mathbf {Y}|$, such that both and are tuples composed by location $l$). This assumption simplifies our proof, while not affecting the results. Indeed, we can eliminate all the pairs that do not satisfy the requirement of $\lbrace \widetilde{l}\rbrace$-closure, and we still have a finite-step $\lbrace \widetilde{l}\rbrace$-simulation saturated by approximants.

The proof exploits the fact that if $\mathrel {{\mathcal {R}}_{(M,N)}}$ is closed by $\lbrace \widetilde{l}\rbrace ,$ then $\mathrel {\mathcal {R}_{(M,N)}^{{\rm {\tt cce}}}}$ is closed by $\lbrace \widetilde{l}\rbrace$ and, for any $C$ such that ${\tt Loc}(C) \subseteq \lbrace \widetilde{l}\rbrace$, if it holds that $ \sum _{i}{p_{i}};{s_{i};\widetilde{V}_{i}} \mathrel {\mathcal {R}_{(M,N)}^{{\rm {\tt cce}}}} \sum _{j}{q_{j}};{t_{j};\widetilde{W}_{j}}$ and $(\lbrace T_{i}\rbrace _{i}, \lbrace U_{j}\rbrace _{j})$ $\in$ $ (\lbrace C[M],\widetilde{V}_{i}\rbrace _{i}, \lbrace C[N],\widetilde{W}_{j}\rbrace _{j})^{\widehat{\star }}$, then $(\lbrace T_{i}\rbrace _{i}, \lbrace U_{j}\rbrace _{j})$ $\in$ $ (\lbrace M,\widetilde{V}_{i}\rbrace _{i}, \lbrace N,\widetilde{W}_{j}\rbrace _{j})^{\widehat{\star }}$, since the locations in $\lbrace \widetilde{l}\rbrace$ are guaranteed to occur at corresponding columns in $\lbrace \widetilde{V}_{i}\rbrace _{i}$ and $\lbrace \widetilde{W}_{j}\rbrace _{j}$ and then $C$ can be turned into a location-free context.

The condition (2a) on the weights is immediately satisfied by the definition of $\mathrel {\mathcal {R}_{(M,N)}^{{\rm {\tt cce}}}}$, since ${\mathcal {R}}$ is a simulation.

Then, we prove that the conditions from (2b) to (2g) of finite-step simulation up-to lifting and environment are satisfied by ${\mathcal {S}}$. Suppose that $\mathbf {Y}= \sum _{i}{p_{i}};{s_{i};\widetilde{V}_{i}} \mathrel {{\mathcal {S}}_{(C[M],C[N])}} \sum _{j}{q_{j}};{t_{j};\widetilde{W}_{j}}=\mathbf {Z}$ with $\mathbf {Y}^{\prime }= \sum _{i}{p_{i}};{s_{i};\widetilde{V}^{\prime }_{i}} , \mathbf {Z}^{\prime }= \sum _{j}{q_{j}};{t_{j};\widetilde{W}^{\prime }_{j}}$ related by $\mathrel {{\mathcal {R}}_{(M,N)}}$ and such that $(\mathbf {Y}^{\prime },\mathbf {Z}^{\prime }) \le _{{\rm {\tt cce}}(M,N)}(\mathbf {Y},\mathbf {Z})$.

• for all $r$, if $(\widetilde{V}_{i})_{r}= \lambda x. M_{i}$ and $(\widetilde{W}_{j})_{r}=\lambda x. N_{j}$ then
  for all $(\lbrace T_{i}\rbrace _{i}, \lbrace U_{j}\rbrace _{j})$ $\in$ $ (\lbrace C[M],\widetilde{V}_{i}\rbrace _{i}, \lbrace C[N],\widetilde{W}_{j}\rbrace _{j})^{\widehat{\star }}$,
  if then
  
  
  

  Proof. We have three cases:

  • if $(\widetilde{V}_{i})_{r}= \lambda x. C^{\prime }[M, \widetilde{V}^{\prime }_{i}]$ and $(\widetilde{W}_{j})_{r}=\lambda x. C^{\prime }[N, \widetilde{W}^{\prime }_{j}]$ for some location-free context $C^{\prime }$ then, since $\mathrel {{\mathcal {R}}_{(M,N)}}$ is closed with respect to $\widetilde{l}$, there is a location-free context $C^{\prime \prime }$ such that
    
    
    and we derive the result by Lemma 64.
    
  • if $(\widetilde{V}_{i})_{r}= (\widetilde{V}^{\prime }_{i})_{r^{\prime }}$ and $(\widetilde{W}_{j})_{r}=(\widetilde{W}^{\prime }_{j})_{r^{\prime }}$ for some $r^{\prime }$, then, since $\mathrel {{\mathcal {R}}_{(M,N)}}$ is closed with respect to $\widetilde{l}$, there is a location-free context $C^{\prime \prime }$ such that
    
    Since $\mathrel {{\mathcal {R}}_{(M,N)}}$ is a finite-step simulation,
    
    implies , which in turn implies the result analogously to Lemma 63.
    
  • if $(\widetilde{V}_{i})_{r}= M$ and $(\widetilde{W}_{j})_{r}= N,$ then $M$ and $N$ are values, and by clause (2g) applied to $\mathrel {{\mathcal {R}}_{(M,N)}}$, we have
    \[ \sum _{i}{p_{i}};{s_{i};\widetilde{V}^{\prime }_{i}, M} \,{{\tt lift}}{(\mathrel {{\mathcal {R}}_{(M,N)}})}\, \sum _{j}{q_{j}};{t_{j};\widetilde{W}^{\prime }_{j}, N.} \]
    Hence, by clause (2b) applied to $\mathrel {{\mathcal {R}}_{(M,N)}}$, we have
    
    which implies , which in turn implies the result (see the proof of Lemma 63).
    

  
  
• for all $r$, if $(\widetilde{V}_{i})_{r}= l_{i}$ and $(\widetilde{W}_{j})_{r}= k_{j}$ then
  • $ \sum _{i}{p_{i}};{s_{i};\widetilde{V}_{i},s_{i}(l_{i})}\,{{\tt lift}}{(\mathrel {{\mathcal {S}}_{(C[M],C[N])}})}\, \sum _{j}{q_{j}};{t_{j};\widetilde{W}_{j},t_{j}(k_{j})}$,
    
  • for all $(\lbrace T_{i}\rbrace _{i}, \lbrace U_{j}\rbrace _{j}) \in (\lbrace C[M],\widetilde{V}_{i}\rbrace _{i}, \lbrace C[N],\widetilde{W}_{j}\rbrace _{j})^{\widehat{\star }}$, we have
    \[ { \sum _{i}{p_{i}};{{s_{i}} [ {l_{i}} \rightarrow {T_{i}}];\widetilde{V}_{i}}} \mathrel {{\mathcal {S}}_{(C[M],C[N])}} { \sum _{j}{q_{j}};{{t_{j}} [ {k_{j}} \rightarrow {U_{j}}];\widetilde{W}_{j}}}\, . \]
    
    
  
  

  Proof. Since contexts used in $\le _{{\rm {\tt cce}}(M,N)}$ are location-free and $\mathrel {{\mathcal {R}}_{(M,N)}}$ is closed with respect to the locations in $\widetilde{l}$ (and thereby the locations in $C[M],C[N]$ are in the dynamic environment of the formal sums in $\mathrel {{\mathcal {R}}_{(M,N)}}$ in corresponding columns), there is $r^{\prime }$ such that $(\widetilde{V}^{\prime }_{i})_{r^{\prime }}=l_{i}$ and $(\widetilde{W}^{\prime }_{j})_{r^{\prime }}=k_{j}$, then:

  • $ \sum _{i}{p_{i}};{s_{i};\widetilde{V}^{\prime }_{i},s_{i}(l_{i})}\,{{\tt lift}}{(\mathrel {{\mathcal {R}}_{(M,N)}})}\, \sum _{j}{q_{j}};{t_{j};\widetilde{W}^{\prime }_{j},t_{j}(k_{j})},$ and we have
    \[ \sum _{i}{p_{i}};{s_{i};\widetilde{V}_{i},s_{i}(l_{i})}\,{{\tt lift}}{\big(\mathrel {\mathcal {R}_{(M,N)}^{{\rm {\tt cce}}}}\big)}\, \sum _{j}{q_{j}};{t_{j};\widetilde{W}_{j},t_{j}(k_{j})}, \]
    from which the result follows.
    
  • by $(\lbrace T_{i}\rbrace _{i}, \lbrace U_{j}\rbrace _{j}) \in (\lbrace M,\widetilde{V}^{\prime }_{i}\rbrace _{i}, \lbrace N,\widetilde{W}^{\prime }_{j}\rbrace _{j})^{\widehat{\star }}$ we derive
    \[ { \sum _{i}{p_{i}};{{s_{i}} [ {l_{i}} \rightarrow {T_{i}}];\widetilde{V}^{\prime }_{i}}} \mathrel {{\mathcal {R}}_{(M,N)}} { \sum _{j}{q_{j}};{{t_{j}} [ {k_{j}} \rightarrow {U_{j}}];\widetilde{W}^{\prime }_{j}}}\,, \]
    which implies
    
    
    

  
  
• for any $(\lbrace s_{i}\rbrace _{i}, \lbrace t_{j}\rbrace _{j})$-fresh locations $(\lbrace l_{i}\rbrace _{i}, \lbrace k_{j}\rbrace _{j})$,
  and for all $(\lbrace T_{i}\rbrace _{i}, \lbrace U_{j}\rbrace _{j})$ $\in$ $ (\lbrace C[M],\widetilde{V}_{i}\rbrace _{i}, \lbrace C[N],\widetilde{W}_{j}\rbrace _{j})^{\widehat{\star }}$,
  \[ \sum _{i}{p_{i}};{{s_{i}} [ {l_{i}} \rightarrow {T_i}];\widetilde{V}_{i}, l_{i}} \mathrel {{\mathcal {S}}_{(C[M],C[N])}} \sum _{j}{q_{j}};{{t_{j}} [ {k_{j}} \rightarrow {U_j}];\widetilde{W}_{j}, k_{j}}. \]
  
  

  Proof. The result follows from $(\lbrace T_{i}\rbrace _{i}, \lbrace U_{j}\rbrace _{j})$ $\in$ $(\lbrace M,\widetilde{V}^{\prime }_{i}\rbrace _{i}, \lbrace N,\widetilde{W}^{\prime }_{j}\rbrace _{j})^{\widehat{\star }}$ as in the previous clause, by exploiting clause () on ${\mathcal {R}}$.

  
  
• for all $r$, if $(\widetilde{V}_{i})_{r}= c_{i}$ and $(\widetilde{W}_{j})_{r}= c_{j}$ then all constants in the two columns are the same (i.e., there is $c_a$ with $c_i=c_j=c_a$ for all $i,j$).
  

  Proof. For every $r$, there are three cases: either and for some $r^{\prime }$, in which case both columns are composed by the same constant, since ${\mathcal {R}}$ is a finite-step simulation; or the value-context is a constant and ; or the constants are, respectively, $M$ and $N$, in which case

  \[ \sum _{i}{p_{i}};{s_{i};\widetilde{V}^{\prime }_{i}},{M}\,{{\tt lift}}{(\mathrel {{\mathcal {R}}_{(M,N)}})}\, \sum _{j}{q_{j}};{t_{j};\widetilde{W}^{\prime }_{j}},{N} \]

  (by clause (2g)) and thus they have to be the same constant, otherwise ${\mathcal {R}}$ would not respect condition (2e).

  
  
• for all $r$, if $(\widetilde{V}_{i})_{r}=(V_{i,1},\ldots, V_{i,n})$ and $(\widetilde{W}_{j})_{r}=(W_{j,1},\ldots,W_{j,n})$ then
  \[ \begin{array}{lc} \displaystyle \sum _{i}{p_{i}};{s_{i};\widetilde{V}_{i},V_{i,1},\ldots, V_{i,n}} \,{{\tt lift}}{(\mathrel {{\mathcal {S}}_{(C[M],C[N])}})}\, \displaystyle\sum _{j}{q_{j}};{t_{j};\widetilde{W}_{j},W_{j,1},\ldots,W_{j,n}}. \end{array} \]
  
  

  Proof. If and for some $r^{\prime },$ then it follows from the definition of ${\mathcal {R}}$ that

  \[ \sum _{i}{p_{i}};{s_{i};\widetilde{V}_{i},V_{i,1},\ldots, V_{i,n}} \,{{\tt lift}}{(\mathrel {{\mathcal {S}}_{(C[M],C[N])}})}\, \sum _{j}{q_{j}};{t_{j};\widetilde{W}_{j},W_{j,1},\ldots,W_{j,n}}. \]

  Otherwise, for every $1 \le h \le n$, we have $(\lbrace V_{i,h}\rbrace _{i}, \lbrace U_{j,h}\rbrace _{j}) \in (\lbrace M,\widetilde{V}^{\prime }_{i}\rbrace _{i}, \lbrace N,\widetilde{W}^{\prime }_{j}\rbrace _{j})^{\widehat{\star }}$, which implies

  \[ (\mathbf {Y}^{\prime },\mathbf {Z}^{\prime }) \le _{{\rm {\tt cce}}(M,N)}\left( \sum _{i}{p_{i}};{s_{i};\widetilde{V}_{i},V_{i,1},\ldots, V_{i,n}}, \sum _{j}{q_{j}};{t_{j};\widetilde{W}_{j},W_{j,1},\ldots,W_{j,n}}\right), \]

  i.e., the formal sums are in relation $\,{{\tt lift}}{(\mathrel {{\mathcal {S}}_{(C[M],C[N])}})}$.

  Finally, if $(\widetilde{V}_{i})_{r}=M$ and $(\widetilde{W}_{j})_{r}=N,$ then the clause follows as in the previous cases from $ \sum _{i}{p_{i}};{s_{i};\widetilde{V}^{\prime }_{i}},{M}\,{{\tt lift}}{(\mathrel {{\mathcal {R}}_{(M,N)}})}\, \sum _{j}{q_{j}};{t_{j};\widetilde{W}^{\prime }_{j}},{N}$, by clause ().

  
  
• .
  

  Proof. Since $\mathrel {{\mathcal {R}}_{(M,N)}}$ is closed with respect to $\widetilde{l}$, there is a location-free context $C^{\prime }$ such that

  \[ \begin{array}{l}\mathbf {Y} ; C[M]= \mathbf {Y} ; C^{\prime }[M,\mathbf {Y}],\\ \mathbf {Z} ; C[N]= \mathbf {Z} ; C^{\prime }[N,\mathbf {Z}], \end{array} \]

  and the result follows from Lemma 64.

  
  

Proof. If $\mathbf {Y}= \sum _{i}{p_{i}};{s_{i};V^{i}_{1},\ldots,V^{i}_{n}}\mathrel {{\mathcal {R}}_{(M,N)}} \sum _{j}{q_{j}};{t_{j};W^{j}_{1},\ldots,W^{j}_{n}}=\mathbf {Z},$ then they are first-order consistent environment formal sums and there are $C,s$ such that and and ${\tt Loc}(C) \subseteq \lbrace \widetilde{l}\rbrace = {\tt Loc}(M) \cup {\tt Loc}(N)$.

Let $C^{\prime }$ be any context with $ {\tt Loc}(C) \subseteq \lbrace \widetilde{l}\rbrace ={\tt Loc}(M) \cup {\tt Loc}(N)$ and let

We have

If and are first-order consistent, then we can conclude, by the definition of $\, \mathcal {R}$, that