Pr-1st-1.1-m10-Slajd53

Dowód twierdzenia 10.3

Wykazaliśmy zatem, że w chwili $\tau ^{x}$, dla każdego procesu $P_{i}\in {\mathcal {P}}$ spełnione są warunki C1, C2 i C3, a więc predykat zakończenia statycznego w chwili $\tau ^{x}$ jest prawdziwy ($Sterm({\mathcal {P}}[\tau ^{x}]=True$ ). Ponieważ predykat ten jest stabilny, więc również dla każdego $\tau >\tau ^{x}$, w tym również dla $\tau _{i}^{k+1}$, $Sterm({\mathcal {P}}[\tau ^{x}]=True$.

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