Pr-1st-1.1-m10-Slajd70

Dowód warunku C5 (3)

Dowód warunku C5 (c.d .)

Ponieważ dla każdego <math<Q_i</math>, $vSentNo_{i}[j][\tau _{i}^{k}]=vSentNo_{i}[j][\tau ^{x}]$ różnica między rzeczywistym zbiorem ${\mathcal {IT}}_{i}[\tau ^{x}]$ a jego aproksymacją ${\mathcal {AIT}}_{i}[\tau _{i}^{k+1}]$, może wynikać tylko z dotarcia pewnych wiadomości do procesów docelowych. Wówczas jednak odpowiedni nadawcy zostaną uwzględnieni w zbiorze ${\mathcal {AV}}_{i}$. Tak więc, biorąc pod uwagę C6 możemy wnosić, że:

$({\mathcal {AV}}_{i}\cup {\mathcal {IT}}_{i})[\tau ^{x}]\subseteq ({\mathcal {AV}}_{i}\cup {\mathcal {AIT}}_{i})[\tau _{i}^{k+1}]$

Dalej, z monotoniczności predykatu $activate_{i}$ wynika, że dla każdego</math>Q_i</math>:

$\neg activate_{i}({\mathcal {AV}}_{i}\cup {\mathcal {AIT}}_{i})[\tau _{i}^{k+1}]\Rightarrow \neg activate_{i}({\mathcal {AV}}_{i}\cup {\mathcal {IT}}_{i})[\tau ^{x}]$

Oznacza to, że warunek C5 jest spełniony.

<< Poprzedni slajd | Spis treści | Następny slajd >>