Legyen , és . Legyenek tetszőleges véges, nem üres halmazok ( ). .

Legyen , amely felbontható tulajdonságok sorozatára az alábbi módon:

A feladat annak eldöntése, hogy létezik-e olyan elem -ban, amelyre teljesül a feltétel, és ha igen, adjunk meg egy ilyen elemet.

Számozzuk meg elemeit az alábbi módon: Minden halmaz elemeit számozzuk meg nullától -ig. Ezután minden eleméhez van egy rendezett -es, amelyre , ahol . Ezen megszámozás egy lexikografikus rendezést definiál -n.

Legyen . Ekkor a fenti megszámozás egy bijekciót létesít és között. Jelölje ezt az leképezést .

Vegyük észre, hogy az halmaz elemei felfoghatók vegyesalapú számrendszerben felírt számként is. Ez alapján egy -es számértéke:

A bevezetett jelölésekkel a feladatot újra specifikáljuk, és most már megkövetelhetjük azt is, hogy ha létezik keresett tulajdonságú elem, akkor az első ilyet adjuk meg:

Ha nem használjuk ki a speciális tulajdonságait, akkor a fenti feldat megoldható lineáris kereséssel, a intervallumon. Vizsgáljuk meg, hogy hogyan használhatnánk ki specialitását!

Ha igaz és pedig hamis, akkor minden olyan -re, amelynek első komponense megegyezik első komponensével, is hamis lesz. Ezért ha az -edik pozíció után a csak nullákat tartalmaz, akkor a keresésben nagyobbat léphetünk, és növelhetjük -t az -edik pozíción.

Az algoritmus még egyszerűbbé tehető, ha a -t kiegészítjük egy túlcsordulás bittel, amelynek 1 értéke azt jelzi, hogy értéke már nem növelhető.

Terjesszük ki az függvényt az alábbi módon:

,

A fenti meggondolások másik következménye, hogy célszerű egy olyan művelet bevezetése is amely amellett, hogy -t eldönti, azt a legkisebb indexet is megadja, amelyre hamis.

Ez a feladat visszavezethető lineáris keresés 2.8-ra.

A program levezetéséhez a már bemutatott specifikációt használjuk. Legyen az invariáns tulajdonság:

Megjegyezzük, hogy a visszalépéses kereséshez hasonlóan több visszalépéses technikát alkalmazó algoritmus is levezethető, például a visszalépéses számlálás: