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.