Porovnanie dvoch neklesajúcich postupností 2
Z invariantu I mozno odvodit invariant
To pouzijeme na zjednodušenie FP
Máme teda 2 moznosti:
1. u = N ? v = N: z invariantu I f a g majú rovnakú mnozinu prvkov
2. u < N ? v < N
FP ? (f[u] ? f[u + 1]) ?
? (g[v] ? g[v + 1]) ?
? (f[u + 1] ? g[v + 1])
Predpokladajme f[u + 1] < g[v + 1]; potom
g[v] = f[u] /* z I */
f[u] < f[u + 1] /* z FP */
g[v] < f[u + 1] < g[v + 1], teda f[u + 1] nie je medzi prvkami gcka, lebo g je neklesajúca
{ f[i] | 0 ? i ? N } ? { g[i] | 0 ? i ? N }
teda f a g nemajú rovnakú mnozinu prvkov
FP ? I ?
[u = N ? v = N] ?
[u = N ? { f[i] | 0 ? i ? N } = { g[i] | 0 ? i ? N }]
dá sa ukázat, ze FP sa dosiahne