defined(a,i,j) and defined(a[j+1]) implies defined(a,i,j+1)

is a theorem. It looks like this in Boyer-Moore theory:

    (PROVE-LEMMA arraytrue-extend-upward-rule (REWRITE) 
        (IMPLIES (AND (EQUAL (arraytrue A I J) T) 
                 (EQUAL (alltrue (selecta A (ADD1 J))) T)) 
                 (EQUAL (arraytrue A I (ADD1 J)) T)))

     Name the conjecture *1.


     We will try to prove it by induction.  There are three plausible

inductions. They merge into two likely candidate inductions. However, only one is unflawed. We will induct according to the following scheme:

      (AND (IMPLIES (LESSP J I) (p A I J))
           (IMPLIES (AND (NOT (LESSP J I))
                         (p A (ADD1 I) J))
                    (p A I J))).

Linear arithmetic informs us that the measure (DIFFERENCE (ADD1 J) I) decreases according to the well-founded relation LESSP in each induction step of the scheme. The above induction scheme leads to three new formulas:

    Case 3. (IMPLIES (AND (LESSP J I)
                          (ARRAYTRUE A I J)
                          (EQUAL (ALLTRUE (SELECTA A (ADD1 J)))
                                 T))
                     (ARRAYTRUE A I (ADD1 J))),

which simplifies, rewriting with ARRAYTRUE-VOID-RULE and SUB1-ADD1, and opening up ARRAYTRUE and LESSP, to the following eight new conjectures:

...

That finishes the proof of *1. Q.E.D.

"arraytrue" is defined recursively:

    (DEFN arraytrue (A I J) 
        (IF (LESSP J I) T                          -- the null case is true
            (AND (EQUAL (alltrue (selecta A I)) T) -- next element is true
                 (arraytrue A (ADD1 I) J)))        -- and rest of array is alltrue

And yes, there's a machine proof that this terminates.