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 {𝒫}$ spełnione są warunki C1, C2 i C3, a więc predykat zakończenia statycznego w chwili ${\tau }^x$ jest prawdziwy ($Sterm({𝒫}[{\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({𝒫}[{\tau }^x]=True$.

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