Indukcný princíp pre leads-to
W ? dobre zalozená (well founded) mnozina
- relácia usporiadania ?
- kazdá podmnozina má najmenší prvok
(nemôzeme reláciou ? klesat do nekonecna)
metrika M: States ? W
- States: stavy programu
- M(S) nahradíme iba M, ak S je jasné z kontextu
??m: m ? W :: p ? M = m ? (p ? M ? m) ? q ? / p ? q
Z kazdého stavu kde platí p program dosiahne stav, v ktorom platí q alebo dosiahne stav, v ktorom p platí a hodnota M je nizšia.
Kedze hodnota M nemôze klesat donekonecna, urcite raz musí platit q (q holds eventually).