; Works as of 4/06/87 20:14:00

Event: Start with the initial nqthm theory.

Definition: min (x, y) = if x < y then x

else y endif

Definition: nth (i, l) = if i ≃ 0 then car (l)

else nth (i − 1, cdr (l)) endif

Definition: put (n, val, l) = if n ≃ 0 then cons (val, cdr (l))

else cons (car (l), put (n − 1, val, cdr (l))) endif

Theorem: nth-of-put nth (i, put (i, v, l)) = v

Theorem: nth-of-put-neq ((i ≠ j ) ∧ (i ∈ N) ∧ (j ∈ N)) → (nth (i, put (j , v, l)) = nth (i, l))

Definition: access (matrix, i, j ) = (¬ (¬ nth (j , nth (i, matrix))))

Event: Disable access.

Definition: length (lst) = if listp (lst) then 1 + length (cdr (lst))

else 0 endif

Definition: col (matrix) = length (car (matrix))

Event: Disable col.

Definition: zeroes (n) = if n ≃ 0 then nil

else cons (0, zeroes (n − 1)) endif Definition: segmentp (i, j , left, matrix) = if left ≃ 0 then t

else access (matrix, i, j ) ∧ segmentp (i, j − 1, left − 1, matrix) endif

Theorem: segmentp-access ((i ∈ N) ∧ (j ∈ N) ∧ segmentp (i, j , left, matrix) ∧ (k < left)) → access (matrix, i, j − k)

Definition: rectanglep (i, j , left, up, matrix) = if (left ≃ 0) ∨ (up ≃ 0) then t

else rectanglep (i − 1, j , left, up − 1, matrix) ∧ segmentp (i, j , left, matrix) endif

Theorem: rectanglep-access ((i ∈ N) ∧ (j ∈ N) ∧ (up ∈ N) ∧ (up ≠ 0) ∧ rectanglep (i, j , left, up, matrix) ∧ (k < left)) → access (matrix, i, j − k)

Definition: tsquarep (i, j , side, matrix) = (rectanglep (i, j , side, side, matrix)

∧ ((1 + i) ≮ side)

∧ ((1 + j ) ≮ side))

Event: Disable tsquarep.

Theorem: tsquarep-0 tsquarep (i, j , 0, matrix)

Theorem: segmentp-goes-down ((m ≮ n) ∧ segmentp (i, j , m, matrix)) → segmentp (i, j , n, matrix)

Theorem: rectanglep-goes-down ((m1 ≮ n1 ) ∧ (m2 ≮ n2 ) ∧ rectanglep (i, j , m1 , m2 , matrix)) → rectanglep (i, j , n1 , n2 , matrix)

Theorem: tsquarep-goes-down ((m ≮ n) ∧ tsquarep (i, j , m, matrix)) → tsquarep (i, j , n, matrix)

Definition: ok-c-before (i, j , c, matrix) = if j ≃ 0 then t

else tsquarep (i, j − 1, nth (j − 1, c), matrix) ∧ (¬ tsquarep (i, j − 1, 1 + nth (j − 1, c), matrix)) ∧ ok-c-before (i, j − 1, c, matrix) endif

Definition: ok-c-after (i, j , c, matrix) = if i ≃ 0 then t

elseif (1 + j ) < col (matrix)

then tsquarep (i − 1, 1 + j , nth (1 + j , c), matrix) ∧ (¬ tsquarep (i − 1, 1 + j , 1 + nth (1 + j , c), matrix)) ∧ ok-c-after (i, 1 + j , c, matrix)

else t endif

Definition: zero-tail (c, j , col) = if j < col then (nth (j , c) = 0) ∧ zero-tail (c, 1 + j , col)

else t endif

Definition: ok-c (i, j , c, matrix) = (ok-c-before (i, j , c, matrix)

∧ ok-c-after (i, j , c, matrix)

∧ if i ≃ 0 then zero-tail (c, j , col (matrix)) else tsquarep (i − 1, j , nth (j , c), matrix)

∧ (¬ tsquarep (i − 1, j , 1 + nth (j , c), matrix)) endif)

Theorem: put-preserves-ok-before ((i ∈ N) ∧ (j ∈ N) ∧ (k ∈ N) ∧ (j ≮ k)) → (ok-c-before (i, k, put (j , side, c), matrix) = ok-c-before (i, k, c, matrix))

Theorem: put-preserves-length (n < length (l)) → (length (put (n, val, l)) = length (l))

Theorem: put-preserves-ok-after ((i ∈ N) ∧ (j ∈ N) ∧ (k ∈ N) ∧ (j < k) ∧ (j < col (matrix))) → (ok-c-after (i, k, put (j , side, c), matrix) = ok-c-after (i, k, c, matrix))

Definition: next (i, j , col) = if (1 + j ) < col then cons (i, 1 + j )

else cons (1 + i, 0) endif

;;; We are headed next toward proving that the accumulating
;;; vector C has the OK-C property preserved by PUTting in
;;; a new entry which is appropriate, i.e. which is the size
;;; of the largest square submatrix with the current coordinate
;;; at the lower right corner.  First we prove PUT-PRESERVES-OK,
;;; which shows that this is the case when SIDE is that
;;; appropriate size.  Then we define the function TSQ-LOCAL
;;; which actually computes this SIDE, and show that it really
;;; does so.

Theorem: zero-tail-preserved (j < k) → (zero-tail (put (j , side, c), k, col) = zero-tail (c, k, col))

Theorem: put-preserves-ok-1 ((i ∈ N) ∧ (j ∈ N) ∧ ok-c (i, j , c, matrix) ∧ tsquarep (i, j , side, matrix) ∧ (¬ tsquarep (i, j , 1 + side, matrix)) ∧ ((1 + j ) < col (matrix))) → ok-c (car (next (i, j , col (matrix))),

cdr (next (i, j , col (matrix))), put (j , side, c), matrix)

Theorem: ok-c-before-property (ok-c-before (i, j , c, matrix) ∧ (k < j ) ∧ (k ∈ N)) → (tsquarep (i, k, nth (k, c), matrix)

∧ (¬ tsquarep (i, k, 1 + nth (k, c), matrix)))

Theorem: put-preserves-ok-2 ((i ∈ N) ∧ (j ∈ N) ∧ (k ∈ N) ∧ ok-c-before (i − 1, j , c, matrix) ∧ tsquarep (i − 1, j , side, matrix) ∧ (¬ tsquarep (i − 1, j , 1 + side, matrix)) ∧ (j = (col (matrix) − 1)) ∧ (col (matrix) ≠ 0)) → ok-c-after (i, k, put (j , side, c), matrix)

Theorem: put-preserves-ok ((i ∈ N) ∧ (j ∈ N)

∧ ok-c (i, j , c, matrix) ∧ tsquarep (i, j , side, matrix) ∧ (¬ tsquarep (i, j , 1 + side, matrix)) ∧ (j < col (matrix))) → ok-c (car (next (i, j , col (matrix))),

cdr (next (i, j , col (matrix))), put (j , side, c), matrix)

Definition: tsq-local (i, j , c, matrix) = if access (matrix, i, j )

then if j ≃ 0 then 1

elseif access (matrix, i − min (nth (j − 1, c), nth (j , c)), j − min (nth (j − 1, c), nth (j , c)))

then 1 + min (nth (j − 1, c), nth (j , c)) else min (nth (j − 1, c), nth (j , c)) endif

else 0 endif

Definition: update-c (i, j , c, matrix) = put (j , tsq-local (i, j , c, matrix), c)

; In order to prove the correctness of TSQ-LOCAL, we need to show
; that joining together appropriately nearby square submatrices
; results in a submatrix of appropriate size.  The lemmas
; TSQUAREP-JOIN-WITHOUT-CORNER-1 and -2 show that one gets a
; TSQAREP of the common size (cf. the statement of problem),
; while TSQUAREP-JOIN-WITH-CORNER gives a square of side one greater
; when the opposite corner has value TRUE.  Recall that the point
; now is to relieve the following two hypotheses of
; PUT-PRESERVES-OK, (TSQUAREP I J SIDE MATRIX) and
; (NOT (TSQUAREP I J (ADD1 SIDE) MATRIX)), where here SIDE is
; computed by UPDATE-C to be (TSQ-LOCAL I J C MATRIX).

Theorem: tsquarep-join-without-corner-1 (tsquarep (0, j − 1, side, matrix) ∧ access (matrix, 0, j )) → tsquarep (0, j , side, matrix)

Theorem: tsquarep-join-without-corner-2 ((i ∈ N) ∧ (i ≠ 0) ∧ tsquarep (i − 1, j , side, matrix) ∧ tsquarep (i, j − 1, side, matrix)

∧ access (matrix, i, j )) → tsquarep (i, j , side, matrix)

Theorem: segmentp-one-longer-base segmentp (i, j , 1, matrix) = access (matrix, i, j )

Theorem: segmentp-goes-down-special-case (segmentp (i, j − 1, left, matrix) ∧ access (matrix, i, j )) → segmentp (i, j , left, matrix)

Theorem: segmentp-one-longer ((i ∈ N) ∧ (j ∈ N) ∧ segmentp (i, j , left, matrix) ∧ access (matrix, i, j − left)) → segmentp (i, j , 1 + left, matrix)

Theorem: rectanglep-join-with-corner (rectanglep (i − 1, j , left, up, matrix) ∧ rectanglep (i, j − 1, left, up, matrix) ∧ access (matrix, i − up, j − left) ∧ (j ≮ left) ∧ (i ≮ up) ∧ (left ∈ N) ∧ (left ≠ 0) ∧ (up ∈ N) ∧ (up ≠ 0) ∧ access (matrix, i, j )) → rectanglep (i, j , 1 + left, 1 + up, matrix)

Theorem: tsquarep-join-with-corner (tsquarep (i − 1, j , side, matrix) ∧ tsquarep (i, j − 1, side, matrix) ∧ access (matrix, i − side, j − side) ∧ access (matrix, i, j ) ∧ (i ∈ N) ∧ (i ≠ 0) ∧ (j ∈ N) ∧ (j ≠ 0)) → tsquarep (i, j , 1 + side, matrix)

; So now finally we show that UPDATE-C yields the appropriate SIDE
; for the hypotheses of PUT-PRESERVES-OK by applying the joining
; lemmas above.  First, a useful lemma.

Theorem: ok-c-0 (ok-c (0, j , c, matrix) ∧ (j < col (matrix))) → (tsq-local (0, j , c, matrix)

= if access (matrix, 0, j ) then 1 else 0 endif)

Theorem: tsquarep-preserved-by-tsq-local-for-i-zero ((j ∈ N) ∧ ok-c (0, j , c, matrix) ∧ (j < col (matrix))) → tsquarep (0, j , tsq-local (0, j , c, matrix), matrix)

Theorem: tsq-local-tsquarep-bound-0 ((j ∈ N) ∧ ok-c (0, j , c, matrix) ∧ (j < col (matrix))) → (¬ tsquarep (0, j , 1 + tsq-local (0, j , c, matrix), matrix))

; For the case where I is non-zero in showing that TSQ-LOCAL has the
; desired property, the following lemma is useful.

Theorem: ok-c-main-property ((j ∈ N) ∧ (j ≠ 0) ∧ (i ∈ N) ∧ (i ≠ 0) ∧ ok-c (i, j , c, matrix)) → (tsquarep (i − 1, j , min (nth (j − 1, c), nth (j , c)), matrix)

∧ tsquarep (i, j − 1, min (nth (j − 1, c), nth (j , c)), matrix))

Theorem: tsquarep-preserved-by-tsq-local-for-i-non-zero ((j ∈ N) ∧ (i ∈ N) ∧ (i ≠ 0) ∧ ok-c (i, j , c, matrix) ∧ (j < col (matrix))) → tsquarep (i, j , tsq-local (i, j , c, matrix), matrix)

; It remains then to show that (add1 (tsq-local ...)) is too large a side
; in the non-zero case.

Theorem: access-i-non-numberp (i ∉ N) → (access (matrix, i, j ) = access (matrix, 0, j ))

Theorem: access-j-non-numberp (j ∉ N) → (access (matrix, i, j ) = access (matrix, i, 0))

Theorem: segmentp-gives-every-access (segmentp (i, j , left, matrix) ∧ (left1 < left)) → access (matrix, i, j − left1 )

Theorem: rectanglep-gives-every-access (rectanglep (i, j , left, up, matrix) ∧ (up1 < up) ∧ (left1 < left)) → access (matrix, i − up1 , j − left1 )

; and a clear corollary:

Theorem: tsquarep-gives-every-access (tsquarep (i, j , side, matrix) ∧ (side1 < side)) → access (matrix, i − side1 , j − side1 )

Theorem: ok-c-main-bound-property ((j ∈ N) ∧ (j ≠ 0) ∧ (i ∈ N) ∧ (i ≠ 0) ∧ ok-c (i, j , c, matrix) ∧ tsquarep (i − 1, j , 1 + min (nth (j − 1, c), nth (j , c)), matrix)) → (¬ tsquarep (i, j − 1, 1 + min (nth (j − 1, c), nth (j , c)), matrix))

Theorem: rectanglep-goes-down-in-i-and-up ((i ∈ N) ∧ (j ∈ N) ∧ rectanglep (i, j , left, 1 + up, matrix)) → rectanglep (i − 1, j , left, up, matrix)

Theorem: rectanglep-goes-down-in-j-and-left ((i ∈ N) ∧ (j ∈ N) ∧ rectanglep (i, j , 1 + left, up, matrix)) → rectanglep (i, j − 1, left, up, matrix)

Theorem: tsquarep-goes-down-in-coordinates-and-side ((i ∈ N) ∧ (i ≠ 0) ∧ (j ∈ N) ∧ (j ≠ 0) ∧ (side ∈ N) ∧ tsquarep (i, j , 1 + side, matrix)) → (tsquarep (i, j − 1, side, matrix) ∧ tsquarep (i − 1, j , side, matrix))

Theorem: tsq-local-tsquarep-bound-non-0 ((i ∈ N) ∧ (i ≠ 0) ∧ (j ∈ N) ∧ ok-c (i, j , c, matrix) ∧ (j < col (matrix))) → (¬ tsquarep (i, j , 1 + tsq-local (i, j , c, matrix), matrix))

; Here then is what we've been aiming at:

Theorem: update-c-preserves-ok-c ((i ∈ N) ∧ (j ∈ N) ∧ ok-c (i, j , c, matrix) ∧ (j < col (matrix))) → ok-c (car (next (i, j , col (matrix))),

cdr (next (i, j , col (matrix))), update-c (i, j , c, matrix), matrix)

Definition: update-acc (i, j , new, acc) = if car (acc) < new then list (new, i, j )

else acc endif

Definition: lex2 (l1 , l2 ) = ((car (l1 ) < car (l2 ))

∨ ((car (l1 ) = car (l2 )) ∧ (cadr (l1 ) < cadr (l2 ))))

Definition: tsq-rec (i, j , c, matrix, acc) = if lex2 (list (i, j ), list (length (matrix), 0))

then tsq-rec (car (next (i, j , col (matrix))), cdr (next (i, j , col (matrix))), update-c (i, j , c, matrix), matrix, update-acc (i, j , tsq-local (i, j , c, matrix), acc))

else acc endif

Definition: c-init (matrix) = zeroes (col (matrix) − 1)

Definition: previous (i, j , col) = if j ≃ 0

then if i ≃ 0 then cons (0, 0)

else cons (i − 1, col − 1) endif else cons (i, j − 1) endif

Theorem: previous-next ((i ∈ N) ∧ (j ∈ N) ∧ (j < col)) → (previous (car (next (i, j , col)), cdr (next (i, j , col)), col) = cons (i, j ))

Definition: bound (i, j , matrix, size)

= if (i ≃ 0) ∧ (j ≃ 0) then t

else (¬ tsquarep (car (previous (i, j , col (matrix))), cdr (previous (i, j , col (matrix))), 1 + size, matrix))

∧ bound (car (previous (i, j , col (matrix))), cdr (previous (i, j , col (matrix))), matrix, size) endif

Definition: in-matrix (i, j , matrix) = ((i ∈ N)

∧ (j ∈ N)

∧ (i < length (matrix)) ∧ (j < col (matrix)))

; The main lemma remaining on the way to
; INVARIANT-IS-PRESERVED-BY-CALL-OF-TSQ-REC is the following:

Theorem: bound-goes-up (bound (i, j , matrix, b) ∧ (b1 ≮ b)) → bound (i, j , matrix, b1 )

Theorem: lessp-update-acc ((car (update-acc (i, j , anything, acc)) < anything) = f) ∧ ((car (update-acc (i, j , anything, acc)) < car (acc)) = f)

Theorem: bound-preserved-by-update-acc ((i ∈ N) ∧ (j ∈ N) ∧ ok-c (i, j , c, matrix) ∧ (j < col (matrix)) ∧ bound (i, j , matrix, car (acc))) → bound (car (next (i, j , col (matrix))),

cdr (next (i, j , col (matrix))),

matrix,

car (update-acc (i, j , tsq-local (i, j , c, matrix), acc)))

Theorem: car-of-next-numberp (i ∈ N) → (car (next (i, j , col)) ∈ N)

Theorem: cdr-of-next-numberp cdr (next (i, j , col)) ∈ N Theorem: cdr-of-next-lessp (x < col) → ((cdr (next (i, j , col)) < col) = t)

Theorem: lex2-next lex2 (list (i, j ), list (car (next (i, j , col)), cdr (next (i, j , col))))

Theorem: lex2-transitivity (lex2 (x, y) ∧ lex2 (y, z)) → lex2 (x, z)

Definition: all-f (i, j , matrix) = if (i ≃ 0) ∧ (j ≃ 0) then t

else (¬ access (matrix, car (previous (i, j , col (matrix))), cdr (previous (i, j , col (matrix)))))

∧ all-f (car (previous (i, j , col (matrix))), cdr (previous (i, j , col (matrix))), matrix) endif

Definition: invariant (i, j , c, matrix, acc) = ((i ∈ N)

∧ (j ∈ N)

∧ in-matrix (cadr (acc), caddr (acc), matrix)

∧ (j < col (matrix)) ∧ ok-c (i, j , c, matrix) ∧ ((all-f (i, j , matrix) ∧ (acc = list (0, 0, 0)))

∨ tsquarep (cadr (acc), caddr (acc), car (acc), matrix)) ∧ (lex2 (cdr (acc), list (i, j ))

∨ ((i = 0) ∧ (j = 0) ∧ (acc = list (0, 0, 0)))) ∧ bound (i, j , matrix, car (acc)))

Theorem: invariant-is-preserved-by-call-of-tsq-rec (lex2 (list (i, j ), cons (length (matrix), '(0))) ∧ invariant (i, j , c, matrix, acc)) → invariant (car (next (i, j , col (matrix))),

cdr (next (i, j , col (matrix))), update-c (i, j , c, matrix), matrix, update-acc (i, j , tsq-local (i, j , c, matrix), acc))

Theorem: tsq-rec-correctness-from-invariant-base invariant (i, j , c, matrix, acc) → (tsquarep (cadr (acc), caddr (acc), car (acc), matrix)

∧ in-matrix (cadr (acc), caddr (acc), matrix)

∧ bound (i, j , matrix, car (acc)))

Theorem: bound-lex2 (bound (i, j , matrix, b) ∧ (i ∈ N) ∧ (j ∈ N) ∧ (i1 ∈ N) ∧ (j1 ∈ N) ∧ (j1 < col (matrix)) ∧ (¬ lex2 (list (i, j ), list (i1 , j1 )))) → bound (i1 , j1 , matrix, b)

Theorem: tsq-rec-correctness-from-invariant invariant (i, j , c, matrix, acc) → (tsquarep (cadr (tsq-rec (i, j , c, matrix, acc)),

caddr (tsq-rec (i, j , c, matrix, acc)), car (tsq-rec (i, j , c, matrix, acc)), matrix)

∧ in-matrix (cadr (tsq-rec (i, j , c, matrix, acc)), caddr (tsq-rec (i, j , c, matrix, acc)), matrix)

∧ bound (length (matrix), 0, matrix, car (tsq-rec (i, j , c, matrix, acc))))

Definition: tsq-i-coord (matrix) = cadr (tsq-rec (0, 0, c-init (matrix), matrix, list (0, 0, 0)))

Definition: tsq-j-coord (matrix) = caddr (tsq-rec (0, 0, c-init (matrix), matrix, list (0, 0, 0)))

Definition: tsq (matrix) = car (tsq-rec (0, 0, c-init (matrix), matrix, list (0, 0, 0)))

Theorem: zero-tail-zeroes-lemma nth (i, zeroes (n)) = 0

Theorem: zero-tail-zeroes zero-tail (zeroes (n), i, j )

Theorem: correctness-of-tsq ((length (matrix) ≠ 0) ∧ (col (matrix) ≠ 0)) → (tsquarep (tsq-i-coord (matrix), tsq-j-coord (matrix), tsq (matrix), matrix)

∧ in-matrix (tsq-i-coord (matrix), tsq-j-coord (matrix), matrix)

∧ bound (length (matrix), 0, matrix, tsq (matrix)))

Index

access, 1, 2, 5–8, 11 access-i-non-numberp, 7 access-j-non-numberp, 7 all-f, 11

bound, 9–12 bound-goes-up, 10 bound-lex2, 12 bound-preserved-by-update-acc, 10

c-init, 9, 12 car-of-next-numberp, 10 cdr-of-next-lessp, 11 cdr-of-next-numberp, 10 col, 1, 3–5, 7–12 correctness-of-tsq, 12

in-matrix, 10–12 invariant, 11, 12 invariant-is-preserved-by-call-

of-tsq-rec, 11

length, 1, 3, 9–12 lessp-update-acc, 10 lex2, 9, 11, 12 lex2-next, 11 lex2-transitivity, 11

min, 1, 5, 7, 8

next, 3–5, 9–11 nth, 1, 3–5, 7, 8, 12 nth-of-put, 1 nth-of-put-neq, 1

ok-c, 3–5, 7–11 ok-c-0, 7 ok-c-after, 3, 4 ok-c-before, 3, 4 ok-c-before-property, 4 ok-c-main-bound-property, 8 ok-c-main-property, 7 previous, 9–11 previous-next, 9 put, 1, 3–5 put-preserves-length, 3 put-preserves-ok, 4 put-preserves-ok-1, 4 put-preserves-ok-2, 4 put-preserves-ok-after, 3 put-preserves-ok-before, 3

rectanglep, 2, 6, 8 rectanglep-access, 2 rectanglep-gives-every-access, 8 rectanglep-goes-down, 2 rectanglep-goes-down-in-i-and-up, 8 rectanglep-goes-down-in-j-and-le

ft, 8 rectanglep-join-with-corner, 6

segmentp, 2, 6, 7 segmentp-access, 2 segmentp-gives-every-access, 7 segmentp-goes-down, 2 segmentp-goes-down-special-case, 6 segmentp-one-longer, 6 segmentp-one-longer-base, 6

tsq, 12 tsq-i-coord, 12 tsq-j-coord, 12 tsq-local, 5, 7–11 tsq-local-tsquarep-bound-0, 7 tsq-local-tsquarep-bound-non-0, 8 tsq-rec, 9, 12 tsq-rec-correctness-from-invari

ant, 12 ant-base, 11

tsquarep, 2–8, 10–12 tsquarep-0, 2 tsquarep-gives-every-access, 8 tsquarep-goes-down, 2 tsquarep-goes-down-in-coordinate

s-and-side, 8 tsquarep-join-with-corner, 6 tsquarep-join-without-corner-1, 5 tsquarep-join-without-corner-2, 5 tsquarep-preserved-by-tsq-local

-for-i-non-zero, 7 -for-i-zero, 7

update-acc, 9–11 update-c, 5, 9, 11 update-c-preserves-ok-c, 9

zero-tail, 3, 4, 12 zero-tail-preserved, 4 zero-tail-zeroes, 12 zero-tail-zeroes-lemma, 12 zeroes, 1, 9, 12