Theorems about leads-to 3
Progress-Safety-Progress (PSP) theorem:
p ? q, r unless b / p ? r ? (q ? r) ? b
Dôkaz. Základný prípad:
- p ensures q, r unless b
- treba ukázat, ze p ? r ? (q ? r) ? b
- z konjunkcie pre ensures a zoslabenia pravej strany
- Indukcný krok (tranzitivita):
- p ? q’, q’ ? q, r unless b
- p ? r ? (q’ ? r) ? b /* (a) */
- p ? q’ ? (q ? r) ? b /* (b) */
- Dôkaz: cancellation na (a) a (b)
- (disjunkcia):
- ??m: m ? W :: p’(m) ? q?
- p = ??m: m ? W :: p’(m)?
- r unless b
- ??m: m ? W :: p’(m) ? r ? (q ? r) ? b? /* (c) */
- Dôkaz: z disjunkcie na (c):
- ??m: m ? W :: p’(m) ? r ? ? (q ? r) ? b
- ??m: m ? W :: p’(m)? ? r ? (q ? r) ? b
- p ? r ? (q ? r) ? b /* z definície p a predošlého */