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>, $vSentN{o}_i[j][{\tau }_i^k]=vSentN{o}_i[j][{\tau }^x]$ różnica między rzeczywistym zbiorem ${{ℐ}{𝒯}}_i[{\tau }^x]$ a jego aproksymacją ${{𝒜}{ℐ}{𝒯}}_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 ${{𝒜}{𝒱}}_i$. Tak więc, biorąc pod uwagę C6 możemy wnosić, że:

$({{𝒜}{𝒱}}_i\cup {{ℐ}{𝒯}}_i)[{\tau }^x]\subseteq ({{𝒜}{𝒱}}_i\cup {{𝒜}{ℐ}{𝒯}}_i)[{\tau }_i^{k+1}]$

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

$\mathrm{\neg }activat{e}_i({{𝒜}{𝒱}}_i\cup {{𝒜}{ℐ}{𝒯}}_i)[{\tau }_i^{k+1}]\Rightarrow \mathrm{\neg }activat{e}_i({{𝒜}{𝒱}}_i\cup {{ℐ}{𝒯}}_i)[{\tau }^x]$

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

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