Theorems about leads-to 2
Dôkaz:
p ? q /* predpoklad */,
p ensures q /* z predpokladu */
p ? q /* z definície leads-to */
Disjunkcná veta (všeobecná): pre lubovolnú mnozinu W platí
??m: m ? W :: p(m) ? q(m)? /
/ ??m: m ? W :: p(m)? ? ??m: m ? W :: q(m)?
Dôkaz: z predikátového poctu a implikacnou vetou
??m: m ? W :: q(m) ? ??n: n ? W :: q(n)??
??m: m ? W :: q(m) ? ??n: n ? W :: q(n)??
??m: m ? W :: p(m) ? q(m)? /* predpoklad */
/* z tranzitivity predchádzajúcich: */
??m: m ? W :: p(m) ? ??n: n ? W :: q(n)??
/* napokon z disjunkcie: */
??m: m ? W :: p(m)? ? ??m: m ? W :: q(m)?
Cancellation
p ? q ? b, b ? r / p ? q ? r
Dôkaz:
b ? r /* predpoklad */
q ? q /* triviálne */
q ? b ? q ? r /* disjunkcia */
p ? q ? r /* z predpokladu p ? q ? b */