Of course it&#x27;s proof by induction. You prove that it&#x27;s true for iteration N+1 if it was true for iteration N.  You prove that it was true for iteration 0.  Then you&#x27;re done.<p>Here&#x27;s how we did it in the Pascal-F verifier [1] around 1980.  This is the
simplest example - proving that all entries in an array are zero after the
array is initialized.<p><pre><code>    type tabix = 1..100;
    type tab = array [tabix] of integer;
    rule function allzero(a: tab; i,j: tabix): boolean; begin end;
    var table1: tab;
       i,j: tabix;
    ...
    for i := 1 to 100 do begin
        table1[i] := 0;
        assert(allzero(table1,1,i-1));
        state(allzero(table1,1,i));
    end;
    assert(allzero(a,1,100));
    ...
    assert(table1[j] = 0);   { table1[j] must be 0 }
</code></pre>
The loop invariant is<p><pre><code>    state(allzero(table1,1,i));
</code></pre>
which says that the predicate &quot;allzero&quot; is true for table1 from 1 to i.<p>&quot;allzero&quot; is defined in the Boyer-Moore theorem prover as a recursive function.<p><pre><code>    (defn allzero (a i j) 
        (if (lessp j i) 
            t 
            (and (allzero a (add1 i) j) (equal (selecta! a i) 0))))
</code></pre>
That&#x27;s a recursive function.  The prover is able to prove that it terminates.
&quot;(selecta! a i)&quot; is LISP for &quot;a[i]&quot; here.<p>We need three theorems about &quot;allzero&quot;.  First, that it&#x27;s vacuously true for j &lt; i:<p><pre><code>    (implies (and (arrayp! a)
                  (numberp i)
                  (numberp j)
                  (lessp j i))
             (allzero a i j)))
</code></pre>
Notation: &quot;arrayp!&quot; is true if the item is an array. &quot;numberp&quot; is true if it&#x27;s an integer.  &quot;lessp&quot;
is &quot;&lt;&quot;.<p>Then that it&#x27;s true for a single element if that element is zero:<p><pre><code>    (implies (and (arrayp! a)
                  (numberp i)
                  (numberp j)
                  (equal i j)
                  (equal (selecta! a i) 0))
             (allzero a i j))))
</code></pre>
And finally, the hard one, that if it&#x27;s true up to N, and a[N+1] is zero, it&#x27;s
true up to N+1.<p><pre><code>    (implies (and (arrayp! a)
                  (numberp i)
                  (numberp j)
                  (allzero a i j)
                  (equal (selecta! a (add1 j)) 0))
             (allzero a i (add1 j))))
</code></pre>
These are all proved, once, with the Boyer-Moore theorem prover. Once proven, they can be
used as rules by the much simpler and faster Oppen-Nelson prover built into the Pascal-F verifier.  Over time, you build up a library of such rules, which are applied automatically
by the fast prover.<p>This is 1980 technology; there&#x27;s been a lot of progress in the last 35 years. This ran on a 1 MIPS VAX 11&#x2F;780 and later on Sun II workstations.  Back then, it was very slow to do this. That&#x27;s a solved problem.  It&#x27;s still rather painful.  But it works.<p>[1] <a href="http:&#x2F;&#x2F;www.animats.com&#x2F;papers&#x2F;verifier&#x2F;verifiermanual.pdf" rel="nofollow">http:&#x2F;&#x2F;www.animats.com&#x2F;papers&#x2F;verifier&#x2F;verifiermanual.pdf</a>