# Delna pravilnost

    s = 0
    k = 0
    a = 1
    { n ≥ 0, s = 0, k = 0, a = 1 }
    I: { (n-1)*s = a-1 }
    while k <= n:
        { (n-1)*s = a-1 }
        { (n-1)*(s+a-a) = a-1 }
        s = s + a
        { (n-1)*(s-a) = a-1 }
        { (n-1)*s - (n-1)*a = a-1 }
        { (n-1)*s = n*a-1 }
        a = a * n
        { (n-1)*s = a-1 }
        { (n-1)*s = a-1 }
        k = k + 1
        { (n-1)*s = a-1 }
    { (n-1)*s = a-1 }

# Popolna pravilnost

    s = 0
    k = 0
    a = 1
    { n-k = d, k - 1 ≤ n }
    while k <= n:
        { n-k = d, n-k ≥ -1, k ≤ n }
        s = s + a
        a = a * n
        { n - (k+1-1) = d, k+1-1 ≤ n }
        k = k + 1
        { n-(k-1) = d, k-1 ≤ n }
        { n-k = d-1, n-k ≥ -1 }
    # količina n-k se je zmanjšala in je omejena navzdol, torej velja popolna pravilnost