Pr-1st-1.1-m10-Slajd53: Różnice pomiędzy wersjami
Z Studia Informatyczne
Przejdź do nawigacjiPrzejdź do wyszukiwania
Nie podano opisu zmian |
m Zastępowanie tekstu – „<math> ” na „<math>” |
||
| Linia 6: | Linia 6: | ||
Wykazaliśmy zatem, że w chwili <math>\tau ^x</math>, dla każdego procesu <math>P_i \in \mathcal{P}</math> spełnione są warunki C1, C2 i C3, a więc predykat zakończenia statycznego w chwili <math>\tau ^x</math> jest prawdziwy | Wykazaliśmy zatem, że w chwili <math>\tau ^x</math>, dla każdego procesu <math>P_i \in \mathcal{P}</math> spełnione są warunki C1, C2 i C3, a więc predykat zakończenia statycznego w chwili <math>\tau ^x</math> jest prawdziwy | ||
(<math>Sterm(\mathcal{P}[\tau ^x] = True</math> ). Ponieważ predykat ten jest stabilny, więc również dla każdego | (<math>Sterm(\mathcal{P}[\tau ^x] = True</math> ). Ponieważ predykat ten jest stabilny, więc również dla każdego | ||
<math> \tau > \tau ^x</math>, w tym również dla | <math>\tau > \tau ^x</math>, w tym również dla | ||
<math>\tau _i^{k+1}</math>, <math>Sterm(\mathcal{P}[\tau ^x] = True</math>. | <math>\tau _i^{k+1}</math>, <math>Sterm(\mathcal{P}[\tau ^x] = True</math>. | ||
[[Pr-1st-1.1-m10-Slajd52 | << Poprzedni slajd]] | [[Pr-1st-1.1-m10-toc|Spis treści ]] | [[Pr-1st-1.1-m10-Slajd54 | Następny slajd >>]] | [[Pr-1st-1.1-m10-Slajd52 | << Poprzedni slajd]] | [[Pr-1st-1.1-m10-toc|Spis treści ]] | [[Pr-1st-1.1-m10-Slajd54 | Następny slajd >>]] | ||
Aktualna wersja na dzień 22:14, 11 wrz 2023
Dowód twierdzenia 10.3
Wykazaliśmy zatem, że w chwili , dla każdego procesu spełnione są warunki C1, C2 i C3, a więc predykat zakończenia statycznego w chwili jest prawdziwy
( ). Ponieważ predykat ten jest stabilny, więc również dla każdego
, w tym również dla
, .
