Legyen 
egy tetszőleges
rendezett halmaz és 
egy
adott függvény. Legyen 
egy az egész számokon értelmezett logikai függvény. Határozzuk meg a
halmaz
felett az 
függvény maximumát és a halmaz egy olyan elemét, amelyen
a
maximumértékét felveszi.
|
|
|
|
|
|
Vegyük észre, hogy itt újra megengedhető az üres intervallum, és hogy ekkor az a válasz, hogy az
intervallumban nincs 
tulajdonságú elem. A levezetés az előzőkhöz hasonlóan:
|
|
|
|
,
,
,
a
értékadás csökkenti a terminálófüggvény értékét,
Írjuk fel a ciklusmag közbülső feltételét:
és 
összehasonlításával látható, hogy három fő lehetőség van:
: ekkor SKIP,
: ez az első 
tulajdonságú elem, tehát 
,
: ekkor a maximumkeresésnél megismert két eset lehetséges:
: ekkor 
,
: ekkor 
.
Tétel: Az alábbi struktogram formában megadott program megoldása a fent specifikált feladatnak:
Bizonyítás: A tétel a levezetési szabályokból, és a specifikáció tételéből a fenti meggondolások (levezetés) alapján következik. __