Theorems about FP
Teoréma: Pre kazdý predikát p platí: FP ? p is stable.
Dôkaz: Ak FP platí, tak dalším vykonávaním programu sa nemení jeho stav. Ak FP ? p, tak aj nadalej FP ? p, cize FP ? p is stable.
Dôsledok: p ? q / FP ? (p ? q)
Dôkaz:
FP ? ?q is stable /* teoréma o FP */
(t.j. FP ? ?q unless false)
p ? q /* predpoklad */
[q ? (FP ? ?q)] ? false = false
p ? FP ? ?q ? false /* PSP teoréma */
?(p ? FP ? ?q) /* nemoznost leads-to */
FP ? (p ? q)