**Proof of Lemma 24**

Considering the semantics of specification triples, it is sufficient to
prove for every positive formula with
that for arbitrary *s* ,
follows from
positive,
and .We will prove this by induction on the structure of (positive) .
We write and .

First, assume that for some *R* : . Then:

Now assume that for no *R* : ; in particular, . We want to prove that also in that case . So assume , i.e.,
, and therefore
. The only participant *R*' that can have
is *B* .
From and we see that , and so
. Note further that . We now prove by induction on the structure of messages that
for all *M* :

If , , and ,

then

Since , and are also increase, the proofs for , , and are analogous.

**Proof of Lemma 28**

The proof is analogous to the proof of Lemma 24.
According to the semantics of specification triples, it is sufficient to
prove for every formula in that for arbitrary *s* ,
follows from safe,
and .For positive Lemma 24 ensures that
. For (where is positive)
we must prove that either
is positive, or under the
assumptions mentioned.
We prove this by induction on the structure of (positive) .Before embarging on the induction, note that formulas of
each of the forms , , and are invariant under the mapping
, so that we can skip them in the case
analysis.

Finally, the postponed
**Case**
Observe that
.
The first conjunct of this expression is positive, which is enough to prove our
claim. The second conjunct is not positive, hence we need to prove
separately.

According to the definition of , we can assume:

We have to prove:For all :

LetFor all :

For , we first observe
that *P*=*A* (only the sender's set has changed). We now prove
the following statement by induction on *M* :

If , , ,

and , then .

This proves by induction the claim

If , , ,which concludes Case of the induction of Lemma 28.

and , then .