הקלט: מספר NUM בן n ספרות.

טענה: לאחר i איטרציות של הלולאה. sum מכיל את סכום i הספרות
הימניות ביותר ו NUM מכיל את n-i הספרות השמאליות ביותר של הקלט.

נוכיח באינדוקציה על i:

בסיס:
כאשר i=0 עוד לא נעשתה שום איטרציה, sum מאותחל לאפס ועל כן
באמת מכיל את סכום אפס הספרות הראשונות. וNUM מכיל את כל המספר
כלומר n מתוך n ספרות שמאליות ביותר. QED

צעד:
נניח כי הטענה נכונה עבור i=k כלשהוא, נוכיח כי הטענה נכונה
עבור i=k+1, כלומר: נניח לאחר k איטרציות sum מכיל את סכום k הספרות
הימניות ביותר, וNUM מכיל את n-k הספרות השמאליות ביותר של הקלט.

הוכחת הצעד:
בלולאה אנו מבצעים:
SUM=SUM+NUM mod 10
NUM mod 10 הוא הספרה הימנית ביותר בNUM שמכיל n-k ספרות שמאליות כלומר
הספרה הימנית ביותר בו היא הספרה הk+1 מהקלט. על פי ההנחה
SUM מכיל את סכום k הספרות הימניות ביותר לאחר פעולה זאת יכיל
את סכום k+1 הספרות הימניות ביותר.
אז אנו מבצעים:
SUM = SUM div 10 כלומר הסר מSUM ספרה אחת מימין היו בSUM
n-k ספרות שמאליות ביותר כעת יהיו בו n-(k+1)
a ספרות שמאליות ביותר.
QED

הוכחנו הטענה לכל i מכאן לאחר n איטרציות sum יכיל את סכום
כל n הספרות.
נותר לבדוק את תנאי העצירה. הלולאה עוצרת כאשר num=0
ואכן לאחר n איטרציות NUM מכיל את n-n=0 הספרות השמאליות ביותר
כלומר אפס ספרות כלומר מכיל אפס. וכן לכל i<n
NUM מכיל n-i>0 ספרות ולכן שונה מאפס.
QED