: Ez a feltétel jól láthatóan nem teljesül (sőt fordítva áll fenn). Mit lehet ilyenkor tenni? Vagy a -t, vagy a -t meg kell változtatni. A azonban a feladatot definiálja, azt nem változtathatjuk meg, a -t pedig mi választottuk úgy, hogy egy közbülső állapotot írjon le, ezért azt sem lenne szerencsés eldobni. Van azonban egy harmadik lehetőség is: keressünk egy olyan állítást, amelyre már teljesül, és oldjuk meg a feladatot egy olyan szekvenciával, amelynek második része egy olyan ciklus lesz, melynek előfeltétele a , az utófeltétele pedig , első fele pedig egy a -ból -be képező program (azaz alkalmazzuk a szekvencia levezetési szabályát). Legyen ez a állítás:

Könnyen látható, hogy ekkor fennáll. Most még keresnünk kell egy olyan programot, ami -ból -be jut. A értékadás megfelel ennek a kritériumnak, hiszen az értékadás leggyengébb előfeltételéről szóló tétel alapján:

.

: Ebből a feltételből meghatározhatjuk, hogy mi lesz a ciklusunk feltétele. Ehhez azt kell megnézni, hogy mikor következik az invariáns tulajdonságból az utófeltétel. A kettőt összehasonlítva észrevehetjük, hogy ez esetén van így. Tehát

, azaz .

: A feltétel teljesítéséhez keresnünk kell egy olyan – az állapottéren értelmezett – egészértékű függvényt, amely az invariáns és a ciklusfeltétel fennállása esetén pozitív. Mivel a változók is az állapottér függvényei, a terminálófüggvényt rajtuk keresztül fogjuk kifejezni. Vegyük észre, hogy ha ( miatt) és ( miatt), akkor értéke pozitív lesz. Legyen tehát:

.

: Mivel már van terminálófüggvényünk, vegyük előre a levezetési szabály utolsó feltételét, ami azt kívánja meg, hogy a ciklusmag csökkentse a terminálófüggvényt. Mivel az utófeltétel szerint értékét meg kell tartanunk, a terminálófüggvényt növelésével tudjuk csökkenteni. Mennyivel növeljük -t? Legalább 1-gyel. Ha egy kicsit előre tekintünk, és figyelembe vesszük, hogy a ciklusmagnak az invariánst meg kell tartania (ez a 4. pont), akkor látható, hogy -t legfeljebb 1-gyel növelhetjük meg. Tehát a értékadás csökkenti a terminálófüggvény értékét, ui:

.

: Meg kell még vizsgálnunk, hogy a értékadás jó lesz-e ciklusmagnak, azaz megtartja-e az invariánst. Írjuk fel a -hez tartozó leggyengébb előfeltételét:

Látható, hogy ez -ből nem következik. Jelöljük hát a fenti feltételt -vel, és legyen a ciklusmag egy olyan szekvencia, amelynek közbülső feltétele és második tagja a értékadás. Ekkor már nincs más dolgunk, mint találni egy olyan programot, ami -ből -be képez és értékét nem változtatja meg. Nézzük meg, hogy mi nem teljesül -ben: mivel ( ) és ( ), fennáll. értéke viszont nem jó, mert szerint csak -ig tartalmazza értékeinek összegét, szerint pedig már -ig kell. A fenti meggondolás alapján tehát növelése -gyel jó lesz, azaz:

.