Theorems about leads-to
Technika dôkazov: indukcia vzhladom na pocet odvodení (dlzka dôkazu) = štrukturálna indukcia
Dôkaz. Základný prípad:
- predpokladajme p ensures false
- z nemoznosti pre ensures máme ?p
Indukcný krok: dva prípady
prípad 1:
p ? r, r ? q
p ? false / ?p, r ? false / ?r
Dôkaz (prípad 1): chceme ukázat, ze ?p
?q /* predpoklad q = false */
?r /* z r ? q, ?q a indukcnej hypotézy */
?p /* z p ? r, ?r a indukcnej hypotézy */
prípad 2:
??m: m ? W :: p’(m) ? q?
p = ??m: m ? W :: p’(m)?
Dôkaz (prípad 2):
??m: m ? W :: [p’(m) ? false] / ?p’(m)?
?q /* predpoklad */
??m: m ? W :: ?p’(m)? /* indukcný predpoklad */
???m: m ? W :: p’(m)? /* z predošlého */
?p /* z definície p */