# The Hockey Stick Theorems in Pascal and Trinomial Triangles

Sima Mehri
Department of Mathematics
Sharif University of Technology
Tehran, Iran

###### Abstract

There are some theorems in the Pascal’s triangle which their figures resemble
to shoot a ball by hockey stick, so they are called hockey stick theorems. P.
Hilton and J. Pedersen, in the article ”Looking into Pascal Triangle,
Combinatorics, Arithmetic and Geometry”, have stated the little and big hockey
stick and puck theorems in the Pascal’s triangle. The big hockey stick theorem
is a special case of a general theorem which our goal is to introduce it. We
state a hockey stick theorem in the trinomial triangle too.

##  1 Introduction and Description of Results

The big hockey stick and puck theorem, stated in [Hilton1987] is:

######  Theorem 1.1 (Hilton1987).

(The Big Hockey Stick and Puck Theorem)

$\binom{n}{0}+\binom{n+2}{1}+\binom{n+4}{2}+\binom{n+6}{3}=\binom{n+7}{3}-\binom{n+6}{1}$

We have found the general form of above theorem in Pascal triangle as below.

######  Theorem 1.2.

(The Hockey Stick Theorem in Pascal Triangle)

$\sum_{i=0}^{k}\binom{n+2i}{i}=\sum_{j=0}^{\left\lfloor\frac{k}{2}\right\rfloor}\left(-1\right)^{j}\binom{n+2k-j+1}{k-2j}$
(1)

An example of this theorem is illustrated in Figure 1.

11211464116152015611828567056288117213535217115101051133111 Figure 1: Example
of Hocky-Stick:1+3+10+35=56-7

Now we wish to state the hockey stick theorem in trinomial triangle. First
using [3,4], we explain what is the trinomial triangle.

The trinomial triangle is a number triangle of trinomial coefficients. It can
be obtained by starting with a row containing a single ”1” and the next row
containing three 1s and then letting subsequent row elements be computed by
summing the elements above to the left, directly above, and above to the
right. We show the trinomial triangle in Figure 2. The trinomial coefficients
are placed as Figure 3. Following the notation of Andrews (1990) in
[Andrews1990], the trinomial coefficient $\binom{n}{k}_{2}$ with $n\geq 0$ and
$-n\leq k\leq n$, is given by the coefficient of $x^{n+k}$ in the expansion of
$(1+x+x^{2})^{n}$. Therefore,

$\binom{n}{k}_{2}=\binom{n}{-k}_{2}$

Equivalently, the trinomial coefficients are defined by

$(1+x+x^{-1})^{n}=\sum_{k=-n}^{k=n}\binom{n}{k}_{2}x^{k}$

We have proven the following theorem in this triangle:

######  Theorem 1.3.

(The Hockey Stick Theorem in The Trinomial Triangle)

$\sum_{i=0}^{k}\binom{n+i}{n}_{2}=\sum_{s=0}^{\lfloor\frac{k}{2}\rfloor}\left(-1\right)^{s}\binom{n+k+1}{n+2s+1}_{2}.$
(2)

For example see Figures 3 and 2.

1621509012614112690502161151530455145301551141016191610411367631123211111
Figure 2: Hockey Stick in Trinomial Triangle: $1+2+6+16+45=90-21+1$
$\binom{6}{-6}$$\binom{6}{-5}$$\binom{6}{-4}$$\binom{6}{-3}$$\binom{6}{-2}$$\binom{6}{-1}$$\binom{6}{0}$$\binom{6}{1}$$\binom{6}{2}$$\binom{6}{3}$$\binom{6}{4}$$\binom{6}{5}$$\binom{6}{6}$$\binom{5}{-5}$$\binom{5}{-4}$$\binom{5}{-3}$$\binom{5}{-2}$$\binom{5}{-1}$$\binom{5}{0}$$\binom{5}{1}$$\binom{5}{2}$$\binom{5}{3}$$\binom{5}{4}$$\binom{5}{5}$$\binom{4}{-4}$$\binom{4}{-3}$$\binom{4}{-2}$$\binom{4}{-1}$$\binom{4}{0}$$\binom{4}{1}$$\binom{4}{2}$$\binom{4}{3}$$\binom{4}{4}$$\binom{3}{-3}$$\binom{3}{-2}$$\binom{3}{-1}$$\binom{3}{0}$$\binom{3}{1}$$\binom{3}{2}$$\binom{3}{3}$$\binom{2}{-2}$$\binom{2}{-1}$$\binom{2}{0}$$\binom{2}{1}$$\binom{2}{2}$$\binom{1}{-1}$$\binom{1}{0}$$\binom{1}{1}$$\binom{0}{0}$
Figure 3: Trinomial Coefficients

##  2 Proof of Results

In the proof of both theorems, we use induction.

###### Proof.

(Theorem 1.2) We prove this theorem using induction on $k$. By the fact
$\binom{n}{n}=\binom{n+1}{n+1}=1$, statement is obvious for the base of
induction i.e. $k=1$. Now we assume that the statement for $k$ is true, then
the relation (1) would be correct. We wish to verify that it is correct for
the value $k+1$ too. We have

$\displaystyle\sum_{i=0}^{k+1}\binom{n+2i}{i}$
$\displaystyle=\binom{n+2k+2}{k+1}+\sum_{i=0}^{k}\binom{n+2i}{i}=\binom{n+2k+2}{k+1}+\sum_{j=0}^{\left\lfloor\frac{k}{2}\right\rfloor}\left(-1\right)^{j}\binom{n+2k-j+1}{k-2j}$
$\displaystyle=\left[\binom{n+2k+2}{k+1}+\binom{n+2k+1}{k}+\binom{n+2k+1}{k-1}\right]-$
$\displaystyle\quad-\left[\binom{n+2k+1}{k-1}+\binom{n+2k}{k-2}+\binom{n+2k}{k-3}\right]+$
$\displaystyle\quad\quad\vdots$
$\displaystyle\quad+(-1)^{\left\lfloor\frac{k}{2}\right\rfloor-1}\left[\binom{n+2k-\left\lfloor\frac{k}{2}\right\rfloor+3}{k-2\left\lfloor\frac{k}{2}\right\rfloor+3}+\binom{n+2k-\left\lfloor\frac{k}{2}\right\rfloor+2}{k-2\left\lfloor\frac{k}{2}\right\rfloor+2}+\binom{n+2k-\left\lfloor\frac{k}{2}\right\rfloor+2}{k-2\left\lfloor\frac{k}{2}\right\rfloor+1}\right]+$
$\displaystyle\quad+(-1)^{\left\lfloor\frac{k}{2}\right\rfloor}\left[\binom{n+2k-\left\lfloor\frac{k}{2}\right\rfloor+2}{k-2\left\lfloor\frac{k}{2}\right\rfloor+1}+\binom{n+2k-\left\lfloor\frac{k}{2}\right\rfloor+1}{k-2\left\lfloor\frac{k}{2}\right\rfloor}+\binom{n+2k-\left\lfloor\frac{k}{2}\right\rfloor+1}{k-2\left\lfloor\frac{k}{2}\right\rfloor-1}\right]+$
$\displaystyle\quad+(-1)^{\left\lfloor\frac{k}{2}\right\rfloor+1}\binom{n+2k-\left\lfloor\frac{k}{2}\right\rfloor+1}{k-2\left\lfloor\frac{k}{2}\right\rfloor-1}=$
using properties of Pascal triangle, we get
$\displaystyle=\left[\binom{n+2k+2}{k+1}+\binom{n+2k+2}{k}\right]-$
$\displaystyle\quad-\left[\binom{n+2k+1}{k-1}+\binom{n+2k+1}{k-2}\right]+$
$\displaystyle\quad\quad\vdots$
$\displaystyle\quad+(-1)^{\left\lfloor\frac{k}{2}\right\rfloor-1}\left[\binom{n+2k-\left\lfloor\frac{k}{2}\right\rfloor+3}{k-2\left\lfloor\frac{k}{2}\right\rfloor+3}+\binom{n+2k-\left\lfloor\frac{k}{2}\right\rfloor+3}{k-2\left\lfloor\frac{k}{2}\right\rfloor+2}\right]+$
$\displaystyle\quad+(-1)^{\left\lfloor\frac{k}{2}\right\rfloor}\left[\binom{n+2k-\left\lfloor\frac{k}{2}\right\rfloor+2}{k-2\left\lfloor\frac{k}{2}\right\rfloor+1}+\binom{n+2k-\left\lfloor\frac{k}{2}\right\rfloor+2}{k-2\left\lfloor\frac{k}{2}\right\rfloor}\right]+$
$\displaystyle\quad+(-1)^{\left\lfloor\frac{k}{2}\right\rfloor+1}\binom{n+2(k+1)-\left\lfloor\frac{k+1}{2}\right\rfloor+1}{k+1-2\left\lfloor\frac{k+1}{2}\right\rfloor}\mathbf{1}_{\left\\{k+1:even\right\\}}=$
$\displaystyle=\binom{n+2k+3}{k+1}-\binom{n+2k+2}{k-1}+\cdots+(-1)^{\left\lfloor\frac{k}{2}\right\rfloor}\binom{n+2k-\left\lfloor\frac{k}{2}\right\rfloor+3}{k-2\left\lfloor\frac{k}{2}\right\rfloor+1}+$
$\displaystyle\quad+(-1)^{\left\lfloor\frac{k+1}{2}\right\rfloor}\binom{n+2(k+1)-\left\lfloor\frac{k+1}{2}\right\rfloor+1}{k+1-2\left\lfloor\frac{k+1}{2}\right\rfloor}\mathbf{1}_{\left\\{k+1:even\right\\}}=$
$\displaystyle=\sum_{j=0}^{\left\lfloor\frac{k+1}{2}\right\rfloor}\left(-1\right)^{j}\binom{n+2(k+1)-j+1}{k+1-2j}$

The statement for $k+1$ is also true, and the proof is completed. ∎

###### Proof.

(Theorem 1.3) To prove this theorem similarly we use induction on $k$.
Considering the equation $\binom{n}{n}_{2}=\binom{n+1}{n+1}_{2}$ , the result
being immediate if $k=0$. Assuming that the statement for $k$ is true, then
the relation (2) would be correct. Now we intend to illustrate it is correct
for the value $k+1$ too. We have

$\displaystyle\sum_{i=0}^{k+1}\binom{n+i}{n}_{2}$
$\displaystyle=\binom{n+k+1}{n}_{2}+\sum_{i=0}^{k}\binom{n+i}{n}_{2}=\binom{n+k+1}{n}_{2}+\sum_{s=0}^{\left\lfloor\frac{k}{2}\right\rfloor}(-1)^{s}\binom{n+k+1}{n+2s+1}_{2}=$
$\displaystyle=\left[\binom{n+k+1}{n}_{2}+\binom{n+k+1}{n+1}_{2}+\binom{n+k+1}{n+2}_{2}\right]-$
$\displaystyle\quad-\left[\binom{n+k+1}{n+2}_{2}+\binom{n+k+1}{n+3}_{2}+\binom{n+k+1}{n+4}_{2}\right]+$
$\displaystyle\quad\quad\vdots$
$\displaystyle\quad+(-1)^{\left\lfloor\frac{k}{2}\right\rfloor-1}\left[\binom{n+k+1}{n+2\left\lfloor\frac{k}{2}\right\rfloor-2}_{2}+\binom{n+k+1}{n+2\left\lfloor\frac{k}{2}\right\rfloor-1}_{2}+\binom{n+k+1}{n+2\left\lfloor\frac{k}{2}\right\rfloor}_{2}\right]+$
$\displaystyle\quad+(-1)^{\left\lfloor\frac{k}{2}\right\rfloor}\left[\binom{n+k+1}{n+2\left\lfloor\frac{k}{2}\right\rfloor}_{2}+\binom{n+k+1}{n+2\left\lfloor\frac{k}{2}\right\rfloor+1}_{2}+\binom{n+k+1}{n+2\left\lfloor\frac{k}{2}\right\rfloor+2}_{2}\right]+$
$\displaystyle\quad+(-1)^{\left\lfloor\frac{k}{2}\right\rfloor+1}\binom{n+k+1}{n+2\left\lfloor\frac{k}{2}\right\rfloor+2}_{2}=$
using properties of the trinomial coefficients, we get
$\displaystyle=\sum_{s=0}^{\left\lfloor\frac{k}{2}\right\rfloor}(-1)^{s}\binom{n+k+2}{n+2s+1}_{2}+(-1)^{\left\lfloor\frac{k}{2}\right\rfloor+1}\binom{n+k+2}{n+2\left\lfloor\frac{k}{2}\right\rfloor+3}_{2}$
$\displaystyle=\sum_{s=0}^{\left\lfloor\frac{k+1}{2}\right\rfloor}(-1)^{s}\binom{n+k+2}{n+2s+1}_{2}$

The statement for $k+1$ is also true, and the proof is completed. ∎

The hockey stick theorem in the trinomial triangles has been proved. This
theorem can be translated in Pascal pyramid as follows :

$\sum_{i=0}^{k}\;\sum_{2r+s=2n+i}\binom{n+i}{r,s,r-n}=\sum_{j=0}^{\left\lfloor\frac{k}{2}\right\rfloor}\left(\left(-1\right)^{j}\sum_{2r+s=2n+k+2j+2}\binom{n+k+1}{r,s,r-n-2j-1}\right)$

Other similar theorems might be obtained for Pascal’s four dimensional and
even $n$-dimensional pyramid.

## References

  * [Andrews1990] G. Andrews, _Euler’s ’Exemplum Memorabile Inductionis Fallacis’ and Trinomial Coefficients_ J. Amer. Math. Soc. 3 (1990), 653-669.
  * [Hilton1987] P. Hilton and J. Pedersen, _Looking into Pascal Triangle, Combinatorics, Arithmetic and Geometry_ Mathematics Magazine, Vol. 60, No. 5 (Dec., 1987), 305-316.
  * [3] Eric W. Weisstein, _Trinomial Coefficient_ From MathWorld–A Wolfram Web Resource. http://mathworld.wolfram.com/TrinomialTriangle.html
  * [4] Eric W. Weisstein, _Trinomial Triangle_ From MathWorld–A Wolfram Web Resource. http://mathworld.wolfram.com/TrinomialTriangle.html


(and indeed, disjointness of histories and heaps are instances of
relations on the PCMs of histories and heaps,

Given a PCM $A$, relation $\gensep$ on $A$ is a
relation if it is:

* (unitary) $\pcmU_A \gensep \pcmU_A$

* (commutative) $x \gensep y$ iff $y \gensep x$

* (compatible) if $x \gensep y$ then $x \orth y$

* (unital) if $x \gensep y$ then $x \gensep \pcmU_A$

* (associative) if $x \gensep y$ and $(x \join y) \gensep z$ then $x \gensep (y
\join
and $y \gensep z$

For example, the relation $\orth_\islocked$ defined in
Section <ref> in clause (<ref>) on
page sep_J1, as

\[
x \orth_\islocked y = \begin{array}[t]{l}
(\fapp{\islocked}{x} \rightarrow \fapp{\lastkey}{y} < \fapp{\lastkey}{x})\, \wedge \\
(\fapp{\islocked}{y} \rightarrow \fapp{\lastkey}{x} < \fapp{\lastkey}{y}) \wedge x \orth y
\end{array}
\]

is a relation. The critical part of the proof is that of
associativity, which we briefly sketch. Let $x$, $y$ and $z$ be three
histories such that $x \orth_\islocked y$ and $(x \join y)
\orth_\islocked z$, and let the timestamps of their last entries be
$t_x$, $t_y$, and $t_z$, respectively. The interesting case is when
$x$ or $y$ end with a locking entry.

Without loss of generality, let $\fapp{\islocked}{x}$ hold, and thus
$\fapp{\lastval}{x} = \lockval$.

Then, by $x \orth_\islocked y$, the last entry of $y$ must be
$\unlockval$, and $t_y < t_x$. Similarly, by $(x \join y)
\orth_\islocked z$, the last entry of $z$ must be $\unlockval$ and
$t_z < t_x$. But then, trivially, $y \orth_\islocked z$, because both
$y$ and $z$ end with an $\unlockval$ entry. Similarly, $x
\orth_\islocked (y \join z)$, because $y \join z$ also ends with an
$\unlockval$ entry, and its last timestamp is $\mathsf{max}(t_y, t_z)
\leq t_y, t_z < t_x$.

The clauses (<ref>) and (<ref>) in
Section <ref> also arise as instances of relations, in a similar way.

Thus, ultimately, the invariant $\Jone = \eqref{eq:Invcond1} \wedge
\eqref{eq:Invcond2} \wedge \eqref{eq:Invcond3}$ can be defined as a
relation on the PCM $\aof{\CSL'}$.

*PCM morphisms. Now we can define morphisms between PCMs
as follows:

A PCM morphism $\phi : A \rightarrow B$ with a relation $\orth_\phi$ is a
partial function from $A$ to $B$ such that:

* $\fapp{\phi}{\pcmU_A} = \pcmU_B$

* if $x \orth_\phi y$, then $\fapp{\phi}{x}$, $\fapp{\phi}{y}$ exist, and $\fapp{\phi}{x}
\orth_B \fapp{\phi}{y}$, and $\fapp{\phi}(x \join y) = \fapp{\phi}{x} \join \fapp{\phi}{y}$

The morphism $\phi$ is total if $\orth_\phi$ equals $\orth_A$.

In Section <ref> we have silently used many PCM
morphisms, as the special symbols that we used to name the components
such as $\thepu$, $\thehist$, $\lkv$, $\theheap$, etc., are all PCM
morphisms.  For example, $\thehist$ and $\thepu$ in
Figure <ref> are projections out of the PCM $\aof{\Spin}$ into
the PCM of histories and permissions, respectively (and projections
out of tuples are morphisms). Then, $\fapp{\selfhist}{s}$ and
$\fapp{\otherhist}{s}$ are abbreviations for
$\papp{\thehist}{\fapp{\selfa}{s}}$ and
$\papp{\thehist}{\fapp{\othera}{s}}$ respectively, and similarly for

We can now define the notion of sub-PCMs as follows:

PCM $A$ is a sub-PCM of a PCM $B$ if there exists a total
PCM morphism $\pval : A \rightarrow B$ (injection) and a
morphism $\psub : B \rightarrow A$ (retraction), such that:

* $\papp{\psub}{\fapp{\pval}{a}} = a$

* if $b \orth_\psub \pcmU_B$ then $\papp{\pval}{\fapp{\psub}{b}} = b$

* if $(\fapp{\psub}{x}) \orth_A (\fapp{\psub}{y})$ then $x \orth_\psub y$

Property (1) says that $\pval$ is injective, i.e., if we coerce $a \in A$ into $\fapp{\pval}{a}$, we
can recover $a$ back by $\psub$, since no other element of $A$ maps by $\pval$ into
$\fapp{\pval}{a}$. The dual property (2) allows the same for a subset of $B$'s elements, that
are related by $\orth_\psub$ to $\pcmU_B$. Hence, intuitively, $A$ is in 1-1 correspondence with
that subset of $B$. Property (3) extends the correspondence to relations, i.e.,
$\orth_A$, when considered on images under $\psub$, implies (and hence, by properties of
morphisms, equals) $\orth_\psub$.

Definition <ref> says what it means for $A$ to be a sub-PCM
of $B$. The following lemma shows how to construct a sub-PCM of $B$
given a relation $\gensep$ on $B$.  We used this
construction in Section <ref> to obtain the PCM for the
resource $\CSL$ out of the PCM $\aof{\CSL'}$.

Given PCM $A$ and relation $\gensep$ on $A$, the set $\subpcm{A}{\gensep} =
\{x \in A \mid x \mathbin{\gensep} \pcmU_A\}$ forms a PCM under unit $\pcmU_A$, and join
operation defined as $x \join_{\subpcm{A}{\gensep}} y = x \join_A y$ if $x\mathbin{\gensep}	y$
and undefined otherwise. The PCM $\subpcm{A}{\gensep}$ is a sub-PCM	of $A$ under the
injection $\pval$ and retraction $\psub$ defined as	$\forall x \in \subpcm{A}{\gensep}\ldot
\papp{\pval}{x} = x$ and $\forall a \in A\ldot \papp{\psub}{a}=a$ if
$a\mathbin{\gensep}\pcmU_A$, and $\papp{\psub}{a}$ undefined otherwise. Moreover,
$\gensep = \orth_\psub = \orth_{\subpcm{A}{R}}$.

Using the above notation, the PCM of the resource $\CSL$ can be
defined formally as $\subpcm{\aof{\CSL'}}{\Jone}$.

We now have all the ingredients to formalizing the construction for
restricting a resource that we set out to define.

Let $R$ be an invariant relation on $\aof{V}$. The sub-resource
$\subjectivesub{V}{R}$ is defined with the same type, transitions and erasure as $V$, but with
the PCM and the state space defined as

* $\aof{\subjectivesub{V}{R}} = \subpcm{\aof{V}}{R}$

* $s \in \papp{\Sigma}{\subjectivesub{V}{R}}$ iff $s \in \papp{\Sigma}{V} \wedge
(\fapp{\selfa}{s}) \mathbin{R} (\fapp{\othera}{s})$

There is a generic resource morphism $\iota :
\morphtp{V}{\subjectivesub{V}{R}}$ that is inclusion on states
and identity on transitions.

For example, the resource $\CSL$ from Section <ref> is
the sub-resource of $\CSL'$ taken under the invariant $\Jone$, and the
resource morphism $\iota : \CSL' \rightarrow \CSL$ from
Section <ref> (page iota_morph), is the
generic morphism defined above.

*Algebraic properties.

We finish this section by providing some additional evidence that
relations and PCM morphisms compose, and have pleasant
mathematical properties. For example, the operations of morphism
composition and join come with the relations as follows.

\[
\begin{array}{r@{\ }c@{\ }lr@{\ }c@{\ }l}
\papp{(f \circ g)}{x} & \eqdef & \papp{f}{\fapp{g}{x}} & x \orth_{f \circ g} y & \eqdef & x \orth_g y \wedge \fapp{g}{x}\mathbin{\orth_f}\fapp{g}{y}\\
\papp{(f \join g)}{x} & \eqdef & \fapp{f}{x} \join \fapp{g}{x} & x \orth_{f \join g} y & \eqdef & x \orth_f y \wedge x \orth_g y \wedge
\fapp{f}{(x \join y)} \orth \fapp{g}{(x \join y)}
%\fapp{f}{x} \orth \fapp{g}{x} \orth \fapp{f}{y} \orth \fapp{g}{y}
\end{array}
\]

Or, given PCM morphisms $f$ and $g$, we can define relation that implements the PCM versions of the algebraic notions of
kernel (preimages of unit) and equalizer (values on
which two morphisms agree), as follows.

\[
\begin{array}{r@{\ }c@{\ }l}
x \mathbin{(\kernel{f})} y & \eqdef & x \orth_f y \wedge \fapp{f}{x}=\fapp{f}{y}=\pcmU\\
x \mathbin{(\eqlz{f}{g})} y & \eqdef & x \orth_f y \wedge x \orth_g y \wedge
\fapp{f}{x}=\fapp{g}{x}
\wedge \fapp{f}{y}=\fapp{g}{y}
\end{array}
\]

Importantly, the above are all relations, as we have
proved in the Coq files. Similarly, we can restrict a morphism to a
relation $R$, to define another PCM morphism.

\[
\papp{(\restrict{f}{R})}{x} \eqdef
\left\{\begin{array}{ll}
\fapp{f}{x}, & \mbox{if $x \mathbin{R} \pcmU$}\\
\mbox{undefined}, & \mbox{otherwise}
\end{array}\right.\quad \mbox{with}\quad
x \orth_{\restrict{f}{R}} y \eqdef x \orth_f y \wedge x \mathbin{R} y
\]

The import of the above abstract constructions is in the reduction of
proof burden. For example, a morphism equalizer is a relation by construction, so the user need not bother proving
compatibility for equalizers. The constructions also combine to
concisely state invariants and assertions. For example, the
relation that gives rise to $\Jone$, and is thus used to
construct the sub-resource $\CSL$, may be defined as the equalizer
$\eqlz{(\thepu \join \theauth)}{(\islocked' \circ \thehist)}$, where
$\islocked' : \hist \rightarrow O$ is the morphism defined on a
history $h$ as $\fapp{\islocked'}{h} =
\mathsf{if}\ \fapp{\islocked}{h}\ \mathsf{then}\ \own\ \mathsf{else}\ \nown$.

§ INDEXED MORPHISM FAMILIES

In this appendix, we show how the definitions of morphism and
$f$-simulations generalize to indexed families. When $X$ is the unit
type, we recover the morphism-related definitions from
Section <ref>.

An indexed family of morphisms $f : \morphtpX{V}{W}{X}$ (or just
family), consists of partial functions $f_\Sigma : X
\rightarrow \sigmaof{W} \rightharpoonup \sigmaof{V}$ (note the
contravariance), and $f_\Delta : X \rightarrow \transof{V}
\rightharpoonup \transof{W}$ on transitions, such that:

(1) (locality of $f_\Sigma$) there exits a
function $f_A : \aof{W} \rightarrow \aof{V}$ such that if
$\xmorpheq{s_v}{(s_w \zig p)}{f_\Sigma}{x}$, then $s_v = s'_v \zig
\papp{f_A}{p}$, and $\xmorpheq{s'_v \zag \papp{f_A}{p}}{(s_w \zag

(2) (locality of $f_\Delta$) if
$\papp{\fapp{f_\Delta}{x}}{s_w \zig p}\,{t} = t'$, then
$\papp{\fapp{f_\Delta}{x}}{s_w \zag p}\,{t} = t'$.

(3) (other-fixity)
if $\papp{\othera}{s_w} = \papp{\othera}{s'_w}$ and
$\fapp{\fapp{f_\Sigma}{x}}{s_w}$, $\fapp{\fapp{f_\Sigma}{x'}}{s'_w}$ exist, then
= \papp{\othera}{\fapp{\fapp{f_\Sigma}{x'}{s'_w}}}$.

(4) (injectivity on indices) if
$\fapp{\fapp{f_\Sigma}{x_1}}{s_{w_1}}$ and $\fapp{\fapp{f_\Sigma}{x_2}}{s_{w_2}}$
exist and $\fapp{\fapp{f_\Sigma}{x_1}}{s_{w_1}} =
\fapp{\fapp{f_\Sigma}{x_2}}{s_{w_2}}$, then $x_1 = x_2$.

In most of the properties of Definition <ref>, the index
$x$ is simply propagated unchanged. The only property where $x$ is
significant is the new property (4), which requires that
$\fapp{\fapp{f_\Sigma}{x}}{s_w}$ uniquely determines the index $x$. In
the $\Stack$ example in Section <ref>, it is easy to see
that the definition of $f_\Sigma$ satisfies this property, because
equal states have equal histories.

Given a morphism family $f : \morphtpX{V}{W}{X}$, an
$f$-simulation is a predicate $I$ on $X$ and $W$-states such

(1) if $\fapp{\fapp{I}{x}}{s_w}$, and
$\xmorpheq{s_v}{s_w}{f_\Sigma}{x}$, and $t\ s_v\ s'_v$, then there
exist $x'$, $t' = {f_\Delta}\ {x}\ {s_w}\ {t}$, and $s'_w$ such that
$\fapp{\fapp{I}{x'}}{s'_w}$ and
$\xmorpheq{s'_v}{s'_w}{f_\Sigma}{x'}$, and $t'\ s_w\ s'_w$.

(2) if $\fapp{\fapp{I}{x}}{s_w}$, and $s_v =
\fapp{\fapp{f_\Sigma}{x}}{s_w}$ exists, and $s_w \osteps[W]{} s'_w$,
then $\fapp{\fapp{I}{x}}{s'_w}$, and $s'_v =
\fapp{\fapp{f_\Sigma}{x}}{s'_w}$ exists, and $s_v \osteps[V]{}

Compared to Definition <ref>, property (1) allows that $x$
changes into $x'$ by a transition. In the $\Stack$ example in
Section <ref>, if we lift $e$ by using the index $x =
\mathsf{empty}$ (i.e., write $\mathsf{morph}\ \mathsf{empty}\ f\ e$),
then this index will evolve with $e$ taking the transitions of
$\Stack$ to track how $e$ changes the self history by adding the
entries for pushing 1 and 2. In property (2), the index $x$ simply

§ DENOTATIONAL SEMANTICS

Our semantic model largely relies on the denotational semantic of
action trees <cit.>. A tree implements
a finite partial approximation of one execution of a program. Thus, a
program of type $\mathsf{ST}\ V\ A$ will be denoted by a set of such
trees. The set may be infinite, as some behaviors (i.e., infinite
loops) can only be represented as an infinite set of converging
approximated executions. Because a program may contain multiple
executions, our denotational semantics can represent non-determinism
in the form of internal choice, though our language currently does not
make use of that feature.

An action tree is a generalization of the Brookes' notion of action
trace <cit.> in the following sense. Where action trace
semantics represent a program by a set of traces, we represent a
program with a set of trees. A tree differs from a trace in that a
trace is a sequence of actions and their results, whereas a tree
contains an action followed by a continuation which itself is a
tree parametrized wrt. the output of the action.

In this appendix, we first define the denotation of each of our
commands as a set of trees. Then we define the semantic behavior for
trees wrt. resource states, in a form of operational semantics for
trees, thus formalizing single execution of a program. Then we relate
this low-level operational semantics of trees to high-level
transitions of a resource by an $\mathsf{always}$ predicate
(Section <ref>) that ensures that a tree is resilient
to any amount of interference, and that all the operational steps by a
tree are safe.

The $\mathsf{always}$ predicate will be instrumental in defining the
$\vrf$-predicate transformer from Section <ref>, and from
there, in defining the type of Hoare triples
$\spec{P}\ A\ \spec{Q}@V$.

Both the $\mathsf{ST}\ V\ A$ type and the Hoare triple type will be
complete lattices of sets of trees, giving us a suitable
setting for modeling recursion.

The soundness of follows from showing that the lemmas
about the $\vrf$ predicate transformer listed in
Section <ref>, are satisfied by the denotations of the

We choose the Calculus of Inductive Constructions
() <cit.> as our meta logic.  This has
several important benefits.  First, we can define a shallow
embedding of our system into that allows us to program and
prove directly with the semantic objects, thus immediately
lifting to a full-blown programming language and verification system
with higher-order functions, abstract types, abstract predicates, and
a module system.  We also gain a powerful dependently-typed
$\lambda$-calculus, which we use to formalize all semantic definitions
and meta theory, including the definition of action trees by
iterated inductive definitions <cit.>,
specification-level functions, and programming-level higher-order

Finally, we were able to mechanize the entire semantics and meta theory
in the Coq proof assistant implementation of .

§.§ Action trees and program denotations

The type $\mathsf{tree}~V~A$ of ($A$-returning) action trees
is defined by the following iterated inductive definition.

\[
\small
\begin{array}{r@{\ }c@{\ }l}
\mathsf{tree}~V~A & \eqdef & \mathsf{Unfinished}\\
& \mid & \mathsf{Ret}\ (v \ty A)\\
& \mid & \mathsf{Act}~(a : \mathsf{action}~V~A)\\
& \mid & \mathsf{Seq}~(T \ty \mathsf{tree}~V~B)~(K \ty B \rightarrow \mathsf{tree}~V~A)\\
& \mid & \mathsf{Par}~(T_1 \ty \mathsf{tree}~V~B_1)\ (T_2 \ty \mathsf{tree}~V~B_2)\ \hbox{}\\
&      & \qquad \!(K \ty B_1 \times B_2 \rightarrow \mathsf{tree}~V~A)\\
& \mid & \mathsf{Morph}~(f : \morphtpX{W}{V}{X})~(x:X)~(T \ty \mathsf{tree}~W~A)
\end{array}
\]

Most of the constructors in Definition <ref> are

Since trees have finite depth, they can only approximate potentially
infinite computations, thus the $\mathsf{Unfinished}$ tree indicates
an incomplete approximation.

$\mathsf{Ret}\ v$ is a terminal computation that returns value

The constructor $\mathsf{Act}$ takes as a parameter an action $a :
\mathsf{action}~V~A$, as defined in Section <ref>.

$ \mathsf{Seq}~T~K$ sequentially composes a $B$-returning tree $T$
with a continuation $K$ that takes $T$'s return value and generates
the rest of the approximation.

$\mathsf{Par}\ T_1\ T_2\ K$ is the parallel composition of trees $T_1$
and $T_2$, and a continuation $K$ that takes the pair of their results
when they join.  's iterated inductive definition permits the
recursive occurrences of $\mathsf{tree}$ to be nonuniform
(e.g., $\mathsf{tree}\ B_i$ in $\mathsf{Par}$) and nested
(e.g., the positive occurrence of $\mathsf{tree}\ A$ in the
continuation). Since the function space includes case-analysis,
the continuation may branch upon the argument.

The $\mathsf{Morph}$ constructor embeds an index $x:X$, morphism $f :
\morphtpX{W}{V}{X}$, and tree $T \ty \mathsf{tree}~W~A$ for the
underlying computation. The constructor will denote $T$ should be
executed so that each of its actions is modified by $f$ with an index

We can now define the denotational model of our programs; that is the
type $\mathsf{ST}~V~A$ of sets of trees, containing

\[
\mathsf{ST}~V~A \eqdef \{e : \mathsf{set}~(\mathsf{tree}~V~A) \mid \mathsf{Unfinished} \in e\}
\]

The denotations of the various constructors combine the trees of the
individual denotations, as shown below.

\[
\small
\begin{array}{r@{\ }c@{\ }l}
\mathsf{ret}\ (r \ty A) & \eqdef & \{\mathsf{Unfinished}, \mathsf{Ret}~r\}
\\
x \leftarrow e_1; e_2 & \eqdef & \{\mathsf{Unfinished}\} \cup \hbox{}\\
& & \qquad \{\mathsf{Seq}~T_1~K \mid T_1 \in e_1 \wedge \forall x \ldot K~x \in e_2\}
\\
e_1 \parallel e_2 & \eqdef & \{\mathsf{Unfinished}\} \cup \hbox{}\\
& & \qquad \{\mathsf{Par}~T_1~T_2~\mathsf{Ret} \mid T_1 \in e_1 \wedge T_2 \in e_2\}
\\
\langle a\rangle & \eqdef & \{\mathsf{Unfinished}, \mathsf{Act}~a\}
\\
\mathsf{morph}~f~x~e & \eqdef & \{\mathsf{Unfinished}\} \cup
\{\mathsf{Morph}~f~x~T \mid T \in e\}
\end{array}
\]

The denotation of $\mathsf{ret}$ simply contains the trivial
$\mathsf{Ret}$ tree, in addition to $\mathsf{Unfinished}$, and
similarly in the case of $\langle a \rangle$. The trees for sequential
composition of $e_1$ and $e_2$ are obtained by pairing up the trees
from $e_1$ with those from $e_2$ using the $\mathsf{Seq}$ constructor,
and similarly for parallel composition and morphism application.

The denotations of composed programs motivate why we denote programs
by non-empty sets, i.e., why each denotation contains at least
$\mathsf{Unfinished}$. If we had a program $\mathsf{Empty}$ whose
denotation is the empty set, then the denotation of $x \leftarrow
\mathsf{Empty}; e'$, $\mathsf{Empty} \parallel e'$ and
$\mathsf{morph}~f~x~\mathsf{Empty}$ will all also be empty, thus
ignoring that the composed programs exhibit more behaviors. For
example, the parallel composition $\mathsf{Empty} \parallel e'$ should
be able to evaluate the right component $e'$, despite the left
component having no behaviors.

By including $\mathsf{Unfinished}$ in all the denotations, we ensure
that behaviors of the components are preserved in the composition. For
example, the parallel composition $\{\mathsf{Unfinished}\} \parallel
e'$ is denoted by the set:

\[
\{\mathsf{Unfinished}\} \cup
\{\mathsf{Par}~\mathsf{Unfinished}~T~\mathsf{Ret} \mid T \in e'\}
\]

which contains an image of each tree from $e'$, thus capturing the
behaviors of $e'$.

§.§ Operational semantics of action trees

The judgment for small-step operational semantics of action trees has
the form $\Delta \vdash \bar{x}, s_w, T_v \tsteps{\Path} \bar{x}',
s'_w, T'_v$ (Figure <ref>). We explain the components of
this judgment next.

First, the component $\Delta$ is a morphism context. This is a
sequence, potentially empty, of morphism families

\[
f_0 : \morphtpX{V_1}{W}{X_0},
f_1 : \morphtpX{V_2}{V_1}{X_1}, \ldots, f_n : \morphtpX{V}{V_n}{X_n}
\]

We say that $\Delta$ has resource type $V \rightarrow W$, and index
type $(X_0, \cdots, X_n)$. An empty context $\cdot$ has resource type
$V \rightarrow V$ for any $V$.

Second, the components $\bar{x}$ and $\bar{x}'$ are tuples, of type
$(X_0, \cdots, X_n)$, and we refer to them as indexes. Intuitively,
the morphism context records the morphisms under which a program
operates. For example, if we wrote a program of the form

\[\mathsf{morph}\ f_0\ x_0\ (\cdots (\mathsf{morph}\ f_n\ x_n\ e) \cdots),\]

it will be that the trees that comprise $e$ execute under the morphism
context $f_0, \ldots, f_n$, with an index tuple $(x_0, \ldots, x_n)$.

Third, the components $s_w$ and $s'_w$ are $W$-states, and $T_v, T'_v
: \mathsf{tree}~V~A$, for some type $A$. The meaning of the judgment
is that a tree $T_v$, when executed in a state $s_w$, under the
context of morphisms $\Delta$ produces a new state $s'_w$ and residual
tree $T'_v$, encoding what is left to execute. The resource of the
trees and the states disagree (the states use resource $W$, the trees
use $V$), but the morphism context $\Delta$ relates them as
follows. Whenever the head constructor of the tree is an action, the
action will first be morphed by applying all the morphisms in $\Delta$
in order, to the transitions that constitute the head action,
supplying along the way the projections out of $x$ to the
morphisms. This will produce a new index $x'$ and an action on
$W$-states, which can be applied to $s_w$ to obtain $s'_w$.

Fourth, the component $\Path$ is of $\pathtp$ type, identifying the
position in the tree where we want to make a reduction.

\[
\small
\begin{array}{r@{\ }c@{\ }l@{\ }c@{\ }l@{\ }c@{\ }l@{\ }c@{\ }l}
\pathtp & \eqdef & \ChoiceAct &|& \SeqRet &|& \SeqStep~(\Path : \pathtp) &|&   \\
&&               \ParRet &|& \ParL~(\Path : \pathtp) &|& \ParR~(\Path : \pathtp) &|& \\
&&               \MorphRet &|& \MorphStep~(\Path : \pathtp)
\end{array}
\label{eq:path}
\]

The key are the constructors $\ParL~\Path$ and $\ParR~\Path$. In a
tree which is a $\mathsf{Par}$ tree, these constructors identify that
we want to reduce in the left and right subtree, respectively,
iteratively following the path $\Path$. If the tree is not a
$\mathsf{Par}$ tree, then $\ParL$ and $\ParR$ constructors will not
form a good path; we define further below when a path is good for a
tree. The other path constructors identify positions in other kinds of
trees. For example, $\ChoiceAct$ identifies the head position in the
tree of the form $\mathsf{Act}(a)$, $\SeqRet$ identifies the head
position in the tree of the form $\mathsf{Seq}~(\mathsf{Ret}~v)~K$
(i.e., it identifies a position of a beta-reduction), $\SeqStep~\pi$
identifies a position in the tree $\mathsf{Seq}~T~K$, if $\pi$
identifies a position within $T$, etc. We do not paths for trees of
the form $\mathsf{Unfinished}$ and $\mathsf{Ret}~v$, because these do
not reduce.

In order to define the operational semantics on trees, we next require
a few auxiliary notions.  First, we need the relation
encoding the composition of the commutative diagrams below (each
commutative diagram is an instance of Figure <ref>(b), for
one of the morphisms $f_0$, $f_1$,…, $f_n$, in the context
$\Delta = f_0; f_1; \cdots; f_n$).

\[
\tikzcdset{arrow style=tikz, diagrams={>=stealth}}
\begin{tikzcd}
s'_v & s'_{n} \arrow[l, "f_{n\Sigma}\ x'_n", swap] & s'_{1} \arrow[l, dotted, dash] & {s'_w} \arrow[l, "f_{0\Sigma}\ x'_0", swap]
\arrow[dl, phantom, "\llcorner", very near start] \\
s_v \arrow[u, "t_v"] & s_{n} \arrow[l, "f_{n\Sigma}\ x_n"] \arrow [u, "t_n" description] & s_{1} \arrow[l, dotted, dash] \arrow[u, "t_1" description] & {s_w} \arrow[l, "f_{0\Sigma}\ x_0"] \arrow[u, "t_w = f_{0\Delta}\ x_0\ s_w\ t_1", swap]
\end{tikzcd}
\]

The relation captures that $t_v$ is morphed by iterating the state
component of the morphisms in $\Delta$, starting from the state $s_w$,
and passing along the elements of the tuple $\bar{x}$ or type $(X_0,
\cdots, X_n)$, until we reach the state $s_v$. Then transition $t_v$
is executed in $s_v$ to obtain $s'_v$, and the transition components
of the morphisms are ran backwards to obtain $t_w$, and the associated
end state $s'_w$. Formally:

\[
\small
\begin{array}{l}
\tsquare{\cdot}{()}{()}{s_v}{s'_v}{t_v}{s_w}{s'_w}{t_w} \eqdef \hbox{}\\
\qquad s_v = s_w \wedge s'_v = s'_w \wedge t_v = t_w\\
\tsquare{(f_0 : \morphtpX{V_1}{W}{X_0}), \Delta)}{(x_0, \bar{x})}{(x'_0, \bar{x}')}{}{}{}{}{}{}\\
\hspace{18mm}{s_v}~{s'_v}~{t_v}~{s_w}~{s'_w}~{t_w} \eqdef \hbox{}\\
\qquad\!\!\!\begin{array}[t]{l}
\exists s_{1}\ s'_{1}\ t_1\ldot \tsquare{\Delta}{\bar{x}}{\bar{x}'}{s_v}{s'_v}{t_v}{s_{1}}{s'_{1}}{t_1} \wedge \hbox{}\\
\xmorpheq{s_{1}}{s_w}{f_{0\Sigma}}{x_0} \wedge \xmorpheq{s'_{1}}{s'_w}{f_{0\Sigma}}{x'_0}
\end{array}
\end{array}
\]

We will often abbreviate $\mathsf{ComSquares}$, and write:

\[
\begin{array}{l}
\mathsf{unwind\_tr}\ \Delta\ \bar{x}\ \bar{x}'\ t_v\ s_w\ s'_w \eqdef \hbox{}\\
\quad \exists s_v\ s'_v\ t_w\ldot \tsquare{\Delta}{\bar{x}}{\bar{x}'}{s_v}{s'_v}{t_v}{s_w}{s'_w}{t_w}\\
\mathsf{unwind\_act}\ \Delta\ \bar{x}\ \bar{x}'\ a\ s_w\ s'_w\ v \eqdef \hbox{}\\
\quad \exists s_v\ s'_v\ t_v\ t_w\ldot \!\!\!\begin{array}[t]{l}
a\ s_v = (t_v, v) \wedge \hbox{}\\
\tsquare{\Delta}{\bar{x}}{\bar{x}'}{s_v}{s'_v}{t_v}{s_w}{s'_w}{t_w}
\end{array}
\end{array}
\]

Given a context $\Delta$, input indices $\bar{x}$, input state $s_w$
and input transition $t_v$, $\mathsf{unwind\_tr}$ “unwinds” the
transition, in the sense that it computes the output index $\bar{x}'$,
output state $s'_w$, obtained by the morphing iteratively by the
morphisms in $\Delta$. The abbreviation $\mathsf{unwind\_act}$ does
the same, but for input action $a : \mathsf{action}{V}{A}$. In the
process, $\mathsf{unwind\_act}$ also computes the return value $v$.

In the frequent cases where $\Delta$ is the empty context (and
correspondingly, $\bar{x}$ and $\bar{x}'$ are empty tuples $()$), we
will abbreviate the judgment from Figure <ref>, and simply
write $s, T \tsteps{\Path} s', T' $.

The operational semantics on trees in Figure <ref> may not
make a step on a tree for two different reasons. The first, benign,
reason is that the the chosen path $\Path$ does not actually determine
an action or a redex in the tree $T$. For example, we may have $T =
\mathsf{Unfinished}$ and $\Path = \mathsf{ParR}$. But we can choose
the right side of a parallel composition only in a tree whose head
constructor is $\mathsf{Par}$, which is not the case with
$\mathsf{Unfinished}$.  We consider such paths that do not determine
an action or a redex in a tree to be ill-formed.

The second reason arises when $\Path$ is actually well-formed. In that
case, the constructors of the path uniquely determine a number of
rules of the operational semantics that should be applied to step the
tree. However, the premises of the rules may not be satisfies. For
example, in the $\mathsf{ChoiceAct}$ rule, there may not exist a $v$
such that $\unwind~\Delta~\bar{x}~\bar{x}'~a~s~s'~v$.

To differentiate between these two different reasons, we first define
the notion of well-formed, or good path, for a given tree.

Let $T \ty \mathsf{tree}~V~A$ and $\Path$ be a path.  Then the
predicate $\mathsf{good}~T~\Path$ recognizes good paths for a
tree $T$ as follows:

\[
\small
\begin{array}{r@{\ }l@{}l@{}c@{}l}
\mathsf{good} & (\mathsf{Act}~a) & \ChoiceAct & ~\eqdef~ & \mathsf{true}
\\
\mathsf{good} & (\mathsf{Seq}~(\mathsf{Ret}~v)~\_) & \SeqRet & ~\eqdef~ & \mathsf{true}
\\
\mathsf{good} & (\mathsf{Seq}~T~\_) & \SeqRet~\Path & ~\eqdef~ & \mathsf{good}~T~\Path
\\
\mathsf{good} & (\mathsf{Par}~(\mathsf{Ret}~\_)~(\mathsf{Ret}~\_)~\_) & \ParRet & ~\eqdef~ & \mathsf{true}
\\
\mathsf{good} & (\mathsf{Par}~T_1~T_2~\_) & \ParL~\Path & ~\eqdef~ & \mathsf{good}~T_1~\Path
\\
\mathsf{good} & (\mathsf{Par}~T_1~T_2~\_) & \ParR~\Path & ~\eqdef~ & \mathsf{good}~T_2~\Path
\\
\mathsf{good} & (\mathsf{Morph}~f~x~(\mathsf{Ret}~\_)) & \MorphRet & ~\eqdef~ & \mathsf{true}
\\
\mathsf{good} & (\mathsf{Morph}~f~x~T) & \MorphStep~\Path & ~\eqdef~ & \mathsf{good}~T~\Path \\
\mathsf{good} & T & \Path & ~\eqdef~ & \mathsf{false} \text{~~otherwise}
\end{array}
\]

We say that a state $s$ is safe for the tree $T$ and path
$\Path$, written $s \in \tsafe~t~\Path$ if:

\[
\mathsf{good}~T~\Path \rightarrow \exists s'\ T'\ldot s, T \tsteps{\Path} s', T'
\]

Notice that in the above definition, the trees $\mathsf{Unfinished}$
and $\mathsf{Ret}\ v$ are safe for any path, simply because there are
no good paths for them, as such trees are terminal. On the other hand,
a tree $\mathsf{Act}~a$ does have a good path, namely $\ChoiceAct$,
but may be unsafe, if the action $a$ is not defined on input state
$s$. For example, the $a$ may be an action for reading from some
pointer $x$, but that pointer may not be allocated in the state $s$.

Safety of a tree will be an important property in the definition of
Hoare triples, where we will require that a precondition of a program
implies that the trees comprising the program's denotation are safe
for every path.

The following are several important lemmas about trees and their
operational semantics, which lift most of the properties of
transitions, to trees.

Let $\Delta : V \rightarrow W$, and $\Delta \vdash \bar{x}, s, T
\tsteps{\Path} \bar{x}', s', T'$. Then either the step corresponds to
an idle transition, that is, $(\bar{x}, s) = (\bar{x}', s')$, or there
exists a transition $a \in \transof{V}$, such that

Let $\Delta : V \rightarrow W$ and $\Delta \vdash \bar{x}, s, T
\tsteps{\Path} \bar{x}', s', T'$. Then $a_o(s) = a_o(s')$.

Let $\Delta : V \rightarrow W$ and $\Delta \vdash \bar{x}, s, T
\tsteps{\Path} \bar{x}', s', T'$. If $s \in \papp{\Sigma}{W}$ then $s'
\in \papp{\Sigma}{W}$.

Let $\Delta : V \rightarrow W$ and $\Delta \vdash \bar{x}, s, T
\tsteps{\Path} \bar{x}', s', T'$. Then $s^\top \osteps[W]{} s'^\top$.

Let $\Delta : V \rightarrow W$ and $\Delta \vdash \bar{x}, s, T
\tsteps{\Path} \bar{x}', s', T'$, and $\Delta \vdash \bar{x}, s, T
\tsteps{\Path} \bar{x}'', s'', T''$. Then $\bar{x}' = \bar{x}''$, $s'
= s''$ and $T' = T''$.

Let $\Delta : V \rightarrow W$ and $\Delta \vdash \bar{x}, (s \zig p),
T \tsteps{\Path} \bar{x}', s', T'$. Then there exists $s''$ such that
$s' = s''\zig p$, and $\Delta \vdash \bar{x}, (s \zag p), T
\tsteps{\Path} \bar{x}', (s'' \zag p), T'$.

If $s \zig p \in \tsafe~T~\Path$ then $s \zag p \in \tsafe~T~\Path$.

Let $s \zig p \in \tsafe~T~\Path$, and $s \zag p, T \tsteps{\Path} s',
T'$. Then there exists $s''$ such that $s' = s'' \zag p$ and $s \zig
p, T \tsteps{\Path}, s'' \zig p, T'$.

The following lemma is of crucial importance, as it relates stepping
with morphisms. In particular, it says that the steps of a tree are
uniquely determined, no matter the morphism under which it
appears. Intuitively, this holds because each transition that a tree
makes has a unique image under a morphism $f : \morphtpX{V}{W}{X}$.

Let $f : \morphtp{V}{W}{X}$ and $\xmorpheq{s_v}{s_w}{f}{x}$. Then the
following hold:

* if $s_v, T \tsteps{\Path} s'_v, T'$, then $\exists x'\ s'_w\ldot
\xmorpheq{s'_v}{s'_w}{f}{x'}$ and $f \vdash (x), s_w, T \tsteps{\Path}
(x'), s'_w, T'$.

* if $f \vdash (x), s_w, T \tsteps{\Path} (x'), s'_w, T'$, then
$\exists x'\ s'_v\ldot \xmorpheq{s'_v}{s'_w}{f}{x'}$ and $s_v, T
\tsteps{\Path} s'_v, T'$.

The first property of this lemma relies on the fact that for a step
over states in $V$, we can also find a step over related states in
$W$, i.e., that $f$ encodes a simulation. The second property relies
on the fact that $f$'s state component is a function in the
contravariant direction. Thus, for each $s_w$ there are unique $x$ and
$s_v$, such that $\xmorpheq{s_v}{s_w}{f}{x}$.

§.§ Predicate transformers

In this section we define a number of predicate transformers over
trees that ultimately lead to defining the $\vrf$ predicate
transformer on programs.

Let $T : \mathsf{tree}~V~A$, and $\Paths$ be a sequence of
paths. Also, let $X$ be an assertion over $V$-states and $V$-trees,
and $Q$ be an assertion over $A$-values and $V$-states. We define
the following predicate transformers:

\[
\small
\begin{array}{l}
\mathsf{always}^{\Paths}~T~X~s \eqdef \hbox{}\\
\qquad \mathsf{if}~\Paths = \Path :: \Paths'~\mathsf{then}~\hbox{}\\
\qquad\quad \forall s_2\ldot (s \osteps[V]{} s_2) \rightarrow \tsafe~T~\Path~s_2 \wedge X~s_2~T \wedge \hbox{}\\
\qquad\qquad \forall s_3~T'\ldot~~ (s_2, T \tsteps{\Path} s_3, T') \rightarrow
\mathsf{always}^{\Paths'}~T_2~X~s_3\\
\qquad \mathsf{else}~ \forall s_2\ldot (s \osteps[V]{} s_2) \rightarrow X~s_2~T
\\
\mathsf{always}~T~X~s \eqdef \forall \Paths\ldot \mathsf{always}^{\Paths}~T~X~s
\\\\
\mathsf{after}~T~Q \eqdef
\mathsf{always}~T~(\lambda~s'~T'\ldot\forall v\ldot T' = \mathsf{Ret}~v \rightarrow Q~v~s')
\end{array}
\]

The helper predicate $\mathsf{always}^{\Paths}~T~X~s$ expresses the
fact that starting from the state $s$, the tree $T$ remains safe and
the user-chosen predicate $X$ holds of all intermediate states and
trees obtained by evaluating $T$ in the state $s$ according to the
sequence of paths $\Paths$. The predicate $X$ remains valid under any
any environment steps of the resource $V$.

The predicate $\mathsf{always}~T~X~s$ quantifiers over the path
sequences. Thus, it expresses that $T$ is safe and $X$ holds after any
finite number of steps which can be taken by $T$ in $s$.

The predicate transformer $\mathsf{after}~T~Q$ encodes that $T$ is
safe for any number of steps; however, $Q\ v\ s'$ only holds if $T$
has been completely reduced to $\mathsf{Ret}\ v$ and state $s'$. In
other words $Q$ is a postcondition for $T$, as it is required to hold
only if, and after, $T$ has terminated.

Now we can define the $\vrf$ predicate transformer on programs, by
quantifying over all trees in the denotation of a program.

\[
\vrf~e~Q~s \eqdef \forall T\in e\ldot \mathsf{after}~T~Q~s
\]

This immediately gives us a way to define when a program $e$ has a
precondition $P$ and postcondition $Q$: when all the trees in $T$ have
a precondition $P$ and postcondition $Q$ according to the
$\mathsf{after}$ predicate, or equivalently, when

\[
\forall s \in \papp{\Sigma}{V}\ldot P\ s \rightarrow \vrf~e~Q~s
\]

which is the formulation we used in Section <ref> to define
the Hoare triples.

We can now state the following soundness theorem, each of whose three
components has been established in the Coq files.

* All the properties of $\vrf$ predicate transformer from
Section <ref> are valid.

* The sets $\mathsf{ST}~V~A$ and $\{P\}\ A\ \{Q\}$ are complete
lattices under subset ordering with the set
$\{\mathsf{Unfinished}\}$ as the bottom. Thus one can compute the
least fixed point of every monotone function by Knaster-Tarski

* All program constructors are monotone.

If $\mathsf{after}~T~(\lambda~s'\ldot\mathsf{True})$, then
$\mathsf{after}$ commutes with universal quantification:

\[
\mathsf{after}~T~(\lambda s' \ldot \forall a{:}A \ldot Q~a~s') \iff
\forall a{:}A\ldot \mathsf{after}~T~(\lambda s'\ldot Q~a~s')
\]

If $\mathsf{after}~T~Q_1$ and $\mathsf{after}~T~Q_2$ then
$\mathsf{after}~T~(Q_1 \bwedge Q_2)$.

The implication lemma allows us to strengthen the postcondition in the
predicate transformer.

If $\mathsf{after}~T~Q_1~s$ and $\forall s\ r\ldot \Sof{V}~s \rightarrow
Q_1~r~s \rightarrow Q_2~r~s$, then $\mathsf{after}~T~Q_2~s$.

Let $T_1 \ty \mathsf{tree}~V~B$, $Ks \ty B \to
\mathcal{P}(\mathsf{tree}~V~A)$ and $T_2 \in \{\mathsf{Seq}~T_1~K \mid
\forall x \ldot K~x \in Ks~x\}$. Then

\[
\mathsf{after}~T_1~(\lambda r~s\ldot \forall T \ldot T \in Ks~r \rightarrow \mathsf{after}~T~Q~s)~s_1 \rightarrow \mathsf{after}~T_2~Q~s_1.
\]

\[
(\mathsf{after}~T_1~Q_1) \bstar (\mathsf{after}~T_2~Q_2) \barrow
\mathsf{after}~(Par~T_1~T_2~\mathsf{Ret})~(\lambda r\ldot Q_1~r.1 \bstar Q_2~r.2)
\]

Let $f : \morphtpX{V}{W}{X}$ be a morphism family.
If $(s_v, s_w) \in f\ x$ and $\mathsf{after}~T~Q~s_v$ then
$\mathsf{after}~(\mathsf{Morph}~x~f~T)~(\lambda r~s'_w\ldot
\exists x'\ s'_v\ldot (s'_v, s'_w) \in f\ x' \wedge Q\ r\ s'_v \wedge x, s_w \msteps[f]{} x', s'_w)~s_w$.