#|
Copyright (C) 1994 by Robert S. Boyer and J Strother Moore.  All Rights
Reserved.
This script is hereby placed in the public domain, and therefore unlimited
editing and redistribution is permitted.
NO WARRANTY
Robert S. Boyer and J Strother Moore PROVIDE ABSOLUTELY NO WARRANTY.  THE
EVENT SCRIPT IS PROVIDED "AS IS" WITHOUT WARRANTY OF ANY KIND, EITHER EXPRESS
OR IMPLIED, INCLUDING, BUT NOT LIMITED TO, ANY IMPLIED WARRANTIES OF
MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE.  THE ENTIRE RISK AS TO
THE QUALITY AND PERFORMANCE OF THE SCRIPT IS WITH YOU.  SHOULD THE SCRIPT
PROVE DEFECTIVE, YOU ASSUME THE COST OF ALL NECESSARY SERVICING, REPAIR OR
CORRECTION.
IN NO EVENT WILL Robert S. Boyer or J Strother Moore BE LIABLE TO YOU FOR ANY
DAMAGES, ANY LOST PROFITS, LOST MONIES, OR OTHER SPECIAL, INCIDENTAL OR
CONSEQUENTIAL DAMAGES ARISING OUT OF THE USE OR INABILITY TO USE THIS SCRIPT
(INCLUDING BUT NOT LIMITED TO LOSS OF DATA OR DATA BEING RENDERED INACCURATE
OR LOSSES SUSTAINED BY THIRD PARTIES), EVEN IF YOU HAVE ADVISED US OF THE
POSSIBILITY OF SUCH DAMAGES, OR FOR ANY CLAIM BY ANY OTHER PARTY.
|#
; This is the list of verification conditions for a FORTRAN
; version of our fast string searching algorithm.  For the details
; of the algorithm, see the comment at the end of the file.  Boyer and Moore.
; This list of events has been further edited, for processing by
; DO-FILE, by (1) inserting the following NOTE-LIB, (2) commenting out
; each FORTRAN-COMMENT and following the comment with the
; corresponding macroexpansion, and (3) by commenting out each
; (COMMENT ...).

Event: Start with the library "fortran" using the compiled version.

; (FORTRAN-COMMENT FORTRAN)

Axiom: fortran t Event: Introduce the function symbol a$0 of 0 arguments. Event: Introduce the function symbol blk-delta1$0 of 0 arguments. Event: Introduce the function symbol blk-delta1$1 of 0 arguments. Event: Introduce the function symbol blk-delta1$2 of 0 arguments. Event: Introduce the function symbol blk-delta1$3 of 0 arguments. Event: Introduce the function symbol blk-delta1$4 of 0 arguments. Event: Introduce the function symbol c$0 of 0 arguments. Event: Introduce the function symbol c$1 of 0 arguments. Event: Introduce the function symbol c$2 of 0 arguments. Event: Introduce the function symbol c$3 of 0 arguments. Event: Introduce the function symbol c$4 of 0 arguments. Event: Introduce the function symbol i$1 of 0 arguments. Event: Introduce the function symbol i$2 of 0 arguments. Event: Introduce the function symbol i$3 of 0 arguments. Event: Introduce the function symbol i$4 of 0 arguments. Event: Introduce the function symbol maxi$0 of 0 arguments. Event: Introduce the function symbol asize& of 0 arguments. Axiom: asize&-numberp asize& ∈ N

Definition: delta1 (a, c, maxi) = if maxi ≃ 0 then 0

elseif c = elt1 (a, maxi) then 0 else 1 + delta1 (a, c, maxi − 1) endif

Definition: stringp (a, i, size) = if i ≃ 0 then t

else (elt1 (a, i) ∈ N)

∧ (elt1 (a, i) ≠ 0) ∧ (size ≮ elt1 (a, i)) ∧ stringp (a, i − 1, size) endif

Axiom: input-conditions

 '*1*true

Definition: global-hyps = ((asize& ≠ '0)

∧ (stringp (a$0, maxi$0, asize&)

∧ ((maxi$0 ≠ '0)

∧ (((1 + asize&)

< least-inexpressible-positive-integer) ∧ (((1 + maxi$0)

< least-inexpressible-positive-integer) ∧ (maxi$0 ∈ N))))))

Theorem: stringp-is-a-univ-quantifier (stringp (a, i, asize&) ∧ (j ≠ 0) ∧ (j ∈ N) ∧ (i ≮ j )) → ((elt1 (a, j ) ∈ N) ∧ (asize& ≮ elt1 (a, j )) ∧ (elt1 (a, j ) ≠ 0))

Theorem: input-definedness global-hyps → '*1*true

#| (COMMENT) |#
; (FORTRAN-COMMENT INPUT)

Axiom: input t

; (FORTRAN-COMMENT LOGICAL-IF-F)

Axiom: logical-if-f t

Axiom: assignment (i$1 = '1) ∧ ((c$1 = c$0) ∧ (blk-delta1$1 = blk-delta1$0))

Theorem: pass1-invrt global-hyps → (((i$1 ∈ N)

∧ ((i$1 ≠ '0)

∧ (((1 + asize&) ≮ i$1)
∧ (((j ∈ N) ∧ ((j ≠ '0) ∧ (j < i$1)))

→ (elt1 (blk-delta1$1, j ) = maxi$0)))))

∧ lex (cons (('2 + (asize& + maxi$0)) − i$1, 'nil), cons ('2 + (asize& + maxi$0), 'nil)))

#| (COMMENT INPUT F) |#

Event: Undo back through the event named ‘input’.

Axiom: paths-from-pass1-invrt ((j ∈ N) ∧ ((j ≠ '0) ∧ (j < i$1))) → (elt1 (blk-delta1$1, j ) = maxi$0)

Definition: path-hyps = (global-hyps

∧ ((i$1 ∈ N) ∧ ((i$1 ≠ '0) ∧ ((1 + asize&) ≮ i$1))))

Theorem: definedness path-hyps → znumberp (i$1)

#| (COMMENT PASS1-INVRT) |#
; (FORTRAN-COMMENT LOGICAL-IF-T)

Axiom: logical-if-t t

Axiom: effects-of-undefiner (c$2 = c$1) ∧ (blk-delta1$2 = blk-delta1$1)

; (FORTRAN-COMMENT LOGICAL-IF-F1)

Axiom: assignment1 (i$3 = '1) ∧ ((c$3 = c$2) ∧ (blk-delta1$3 = blk-delta1$2))

Theorem: pass2-invrt (i$1 ∧ (zgreaterp (i$1, asize&) ∧ path-hyps)) → (((i$3 ∈ N)

∧ ((i$3 ≠ '0)

∧ (((1 + maxi$0) ≮ i$3)
∧ (((j ≄ 0) ∧ (asize& ≮ j ))

→ (elt1 (blk-delta1$3, j )

= (delta1 (a$0, j , i$3 − 1) + (maxi$0

− (i$3 − 1))))))))

∧ lex (cons ((1 + maxi$0) − i$3, 'nil), cons (('2 + (asize& + maxi$0)) − i$1, 'nil)))

#| (COMMENT PASS1-INVRT T F) |#

Event: Undo back through the event named ‘logical-if-t’.

; (FORTRAN-COMMENT LOGICAL-IF-F1)

Axiom: logical-if-f1 t

Theorem: array-bounds-check-for-delta1 ((¬ zgreaterp (i$1, asize&)) ∧ path-hyps) → (('0 < i$1) ∧ (asize& ≮ i$1))

#| (COMMENT PASS1-INVRT F) |#

Axiom: assignment1 (i$2 = i$1) ∧ ((c$2 = c$1)

∧ (elt1 (blk-delta1$2, i)

= if i = i$1 then maxi$0 else elt1 (blk-delta1$1, i) endif))

Theorem: input-cond-of-zplus (almost-equal1 (blk-delta1$1, blk-delta1$2, '1, asize&, i$1, maxi$0) ∧ ((¬ zgreaterp (i$1, asize&)) ∧ path-hyps)) → expressible-znumberp (zplus (i$2, '1))

#| (COMMENT PASS1-INVRT F) |#

Axiom: assignment2 (i$3 = zplus (i$2, '1)) ∧ ((c$3 = c$2) ∧ (blk-delta1$3 = blk-delta1$2))

Theorem: pass1-invrt1 (almost-equal1 (blk-delta1$1, blk-delta1$2, '1, asize&, i$1, maxi$0) ∧ ((¬ zgreaterp (i$1, asize&)) ∧ path-hyps)) → (((i$3 ∈ N)

∧ ((i$3 ≠ '0)

∧ (((1 + asize&) ≮ i$3)
∧ (((j ∈ N) ∧ ((j ≠ '0) ∧ (j < i$3)))

→ (elt1 (blk-delta1$3, j ) = maxi$0)))))

∧ lex (cons (('2 + (asize& + maxi$0)) − i$3, 'nil), cons (('2 + (asize& + maxi$0)) − i$1, 'nil)))

#| (COMMENT PASS1-INVRT F) |#

Event: Undo back through the event named ‘paths-from-pass1-invrt’.

Axiom: paths-from-pass2-invrt ((j ≄ 0) ∧ (asize& ≮ j )) → (elt1 (blk-delta1$1, j )

= (delta1 (a$0, j , i$1 − 1) + (maxi$0 − (i$1 − 1))))

Definition: path-hyps = (global-hyps

∧ ((i$1 ∈ N) ∧ ((i$1 ≠ '0) ∧ ((1 + maxi$0) ≮ i$1))))

Theorem: definedness path-hyps → znumberp (i$1)

#| (COMMENT PASS2-INVRT) |#
; (FORTRAN-COMMENT LOGICAL-IF-T)

Axiom: logical-if-t t

Axiom: effects-of-undefiner (c$2 = c$1) ∧ (blk-delta1$2 = blk-delta1$1)

Theorem: output (i$1 ∧ (zgreaterp (i$1, maxi$0) ∧ path-hyps)) → (((c ∈ N) ∧ ((c ≠ '0) ∧ (asize& ≮ c)))

→ (elt1 (blk-delta1$2, c) = delta1 (a$0, c, maxi$0)))

#| (COMMENT PASS2-INVRT T) |#

Event: Undo back through the event named ‘logical-if-t’.

; (FORTRAN-COMMENT LOGICAL-IF-F1)

Axiom: logical-if-f1 t

Theorem: array-bounds-check-for-a ((¬ zgreaterp (i$1, maxi$0)) ∧ path-hyps) → (('0 < i$1) ∧ (maxi$0 ≮ i$1))

#| (COMMENT PASS2-INVRT F) |#

Theorem: definedness1 ((¬ zgreaterp (i$1, maxi$0)) ∧ path-hyps) → znumberp (elt1 (a$0, i$1))

#| (COMMENT PASS2-INVRT F) |#

Axiom: assignment1 (i$2 = i$1) ∧ ((c$2 = elt1 (a$0, i$1)) ∧ (blk-delta1$2 = blk-delta1$1))

Theorem: input-cond-of-zdifference ((¬ zgreaterp (i$1, maxi$0)) ∧ path-hyps) → expressible-znumberp (zdifference (maxi$0, i$2))

#| (COMMENT PASS2-INVRT F) |#

Theorem: array-bounds-check-for-delta1 ((¬ zgreaterp (i$1, maxi$0)) ∧ path-hyps) → (('0 < c$2) ∧ (asize& ≮ c$2))

#| (COMMENT PASS2-INVRT F) |#

Axiom: assignment2 (i$3 = i$2) ∧ ((c$3 = c$2)

∧ (elt1 (blk-delta1$3, i)

= if i = c$2 then zdifference (maxi$0, i$2) else elt1 (blk-delta1$2, i) endif))

Theorem: input-cond-of-zplus (almost-equal1 (blk-delta1$2,

blk-delta1$3,

             '1,

asize&, c$2, zdifference (maxi$0, i$2))

∧ ((¬ zgreaterp (i$1, maxi$0)) ∧ path-hyps)) → expressible-znumberp (zplus (i$3, '1))

#| (COMMENT PASS2-INVRT F) |#

Axiom: assignment3 (i$4 = zplus (i$3, '1)) ∧ ((c$4 = c$3) ∧ (blk-delta1$4 = blk-delta1$3))

Theorem: delta1-skip ((j ≠ elt1 (pat, i)) ∧ (i ≄ 0)) → (delta1 (pat, j , i) = (1 + delta1 (pat, j , i − 1)))

Theorem: pass2-invrt1 (almost-equal1 (blk-delta1$2,

blk-delta1$3,

             '1,

asize&, c$2, zdifference (maxi$0, i$2))

∧ ((¬ zgreaterp (i$1, maxi$0)) ∧ path-hyps)) → (((i$4 ∈ N)

∧ ((i$4 ≠ '0)

∧ (((1 + maxi$0) ≮ i$4)
∧ (((j ≄ 0) ∧ (asize& ≮ j ))

→ (elt1 (blk-delta1$4, j )

= (delta1 (a$0, j , i$4 − 1) + (maxi$0

− (i$4 − 1))))))))

∧ lex (cons ((1 + maxi$0) − i$4, 'nil), cons ((1 + maxi$0) − i$1, 'nil)))

#| (COMMENT PASS2-INVRT F) |#

Event: Undo back through the event named ‘paths-from-pass2-invrt’. Event: Undo back through the event named ‘fortran’.

; (FORTRAN-COMMENT FORTRAN)

Axiom: fortran t Event: Introduce the function symbol blk-delta1$1 of 0 arguments. Event: Introduce the function symbol blk-delta1$2 of 0 arguments. Event: Introduce the function symbol blk-delta1$3 of 0 arguments. Event: Introduce the function symbol blk-delta1$4 of 0 arguments. Event: Introduce the function symbol c$0 of 0 arguments. Event: Introduce the function symbol c$1 of 0 arguments. Event: Introduce the function symbol c$2 of 0 arguments. Event: Introduce the function symbol c$3 of 0 arguments. Event: Introduce the function symbol c$4 of 0 arguments. Event: Introduce the function symbol i$0 of 0 arguments. Event: Introduce the function symbol i$1 of 0 arguments. Event: Introduce the function symbol i$2 of 0 arguments. Event: Introduce the function symbol i$3 of 0 arguments.

Event: Introduce the function symbol i$4 of 0 arguments. Event: Introduce the function symbol j$0 of 0 arguments. Event: Introduce the function symbol j$1 of 0 arguments. Event: Introduce the function symbol j$2 of 0 arguments. Event: Introduce the function symbol j$3 of 0 arguments. Event: Introduce the function symbol j$4 of 0 arguments. Event: Introduce the function symbol nexti$0 of 0 arguments. Event: Introduce the function symbol nexti$1 of 0 arguments. Event: Introduce the function symbol nexti$2 of 0 arguments. Event: Introduce the function symbol nexti$3 of 0 arguments. Event: Introduce the function symbol nexti$4 of 0 arguments. Event: Introduce the function symbol pat$0 of 0 arguments. Event: Introduce the function symbol patlen$0 of 0 arguments. Event: Introduce the function symbol str$0 of 0 arguments. Event: Introduce the function symbol strlen$0 of 0 arguments. Event: Introduce the function symbol x$0 of 0 arguments. Event: Introduce the function symbol x$1 of 0 arguments. Event: Introduce the function symbol x$2 of 0 arguments.

Event: Introduce the function symbol x$3 of 0 arguments.

Event: Introduce the function symbol x$4 of 0 arguments.

Event: Introduce the function symbol asize& of 0 arguments.

Axiom: asize&-numberp asize& ∈ N

Definition: delta1 (a, c, maxi) = if maxi ≃ 0 then 0

elseif c = elt1 (a, maxi) then 0 else 1 + delta1 (a, c, maxi − 1) endif

Definition: stringp (a, i, size) = if i ≃ 0 then t

else (elt1 (a, i) ∈ N)

∧ (elt1 (a, i) ≠ 0) ∧ (size ≮ elt1 (a, i)) ∧ stringp (a, i − 1, size) endif

Theorem: stringp-is-a-univ-quantifier (stringp (a, i, asize&) ∧ (j ≠ 0) ∧ (j ∈ N) ∧ (i ≮ j )) → ((elt1 (a, j ) ∈ N) ∧ (asize& ≮ elt1 (a, j )) ∧ (elt1 (a, j ) ≠ 0))

Definition: match (pat, j , patlen, str, i, strlen) = if patlen < j then t

elseif strlen < i then f

else (elt1 (pat, j ) = elt1 (str, i))

∧ match (pat, 1 + j , patlen, str, 1 + i, strlen) endif

Definition: search (pat, str, patlen, strlen, i) = if strlen < i then 1 + strlen

elseif match (pat, 1, patlen, str, i, strlen) then i else search (pat, str, patlen, strlen, 1 + i) endif

Axiom: input-conditions

 '*1*true

Definition: global-hyps = ((asize& ≠ '0)

∧ (((1 + asize&) < least-inexpressible-positive-integer)

∧ (stringp (pat$0, patlen$0, asize&)

∧ (('0 < patlen$0)

∧ (stringp (str$0, strlen$0, asize&)

∧ (('0 < strlen$0)

∧ (((patlen$0

+ strlen$0)

< least-inexpressible-positive-integer) ∧ ((patlen$0 ∈ N)

∧ (strlen$0 ∈ N)))))))))

Theorem: search-non-zero (i ≄ 0) → (0 < search (pat, str, patlen, strlen, i))

Theorem: match-at-patlen (patlen < j ) → match (pat, j , patlen, str, i, strlen)

Theorem: match-at-strlen (strlen < i) → (match (pat, j , patlen, str, i, strlen) = (patlen < j ))

Theorem: match-needs-patlen-chars ((patlen ∈ N) ∧ (strlen ∈ N) ∧ (patlen ≮ j ) ∧ (strlen ≮ i) ∧ ((j + strlen) < (i + patlen))) → (¬ match (pat, j , patlen, str, i, strlen))

Theorem: search-boundary ((patlen ≄ 0) ∧ (strlen ∈ N) ∧ (strlen ≮ i) ∧ ((1 + strlen) < (patlen + search (pat, str, patlen, strlen, i)))) → (search (pat, str, patlen, strlen, i) = (1 + strlen))

Theorem: delta1-lesseqp-patlen patlen ≮ delta1 (pat, char, patlen)

Theorem: input-definedness global-hyps → '*1*true

#| (COMMENT) |#
; (FORTRAN-COMMENT INPUT)

Axiom: input t

Theorem: call-of-setup (patlen$0 ∧ global-hyps) → (stringp (pat$0, patlen$0, asize&)

∧ ((patlen$0 ≠ '0)

∧ ((patlen$0 ∈ N)
∧ (((1 + asize&)

< least-inexpressible-positive-integer)

∧ ((1 + patlen$0) < least-inexpressible-positive-integer)))))

#| (COMMENT INPUT) |#

Axiom: effects-of-setup (((c ∈ N) ∧ ((c ≠ '0) ∧ (asize& ≮ c))) → (elt1 (blk-delta1$1, c) = delta1 (pat$0, c, patlen$0))) ∧ ((i$1 = i$0)

∧ ((j$1 = j$0)

∧ ((c$1 = c$0)

∧ ((nexti$1 = nexti$0) ∧ (x$1 = x$0)))))

Axiom: assignment (i$2 = patlen$0) ∧ ((j$2 = j$1)

∧ ((c$2 = c$1)

∧ ((nexti$2 = nexti$1) ∧ ((x$2 = x$1)

∧ (blk-delta1$2 = blk-delta1$1)))))

Theorem: outer-invrt (patlen$0 ∧ global-hyps) → (((i$2 ∈ N)

∧ ((i$2 ≮ patlen$0)

∧ ((i$2
< (patlen$0

+ search (pat$0, str$0, patlen$0, strlen$0, '1)))

∧ (((c ∈ N) ∧ ((c ≠ '0) ∧ (asize& ≮ c)))

→ (elt1 (blk-delta1$2, c)

= delta1 (pat$0, c, patlen$0))))))

∧ lex (cons (('1 + (strlen$0 + patlen$0)) − i$2, cons (1 + patlen$0, 'nil)), cons ('1 + (strlen$0 + patlen$0), cons (1 + patlen$0, 'nil))))

#| (COMMENT INPUT) |#

Event: Undo back through the event named ‘input’.

Axiom: paths-from-outer-invrt ((c ∈ N) ∧ ((c ≠ '0) ∧ (asize& ≮ c))) → (elt1 (blk-delta1$1, c) = delta1 (pat$0, c, patlen$0))

Definition: path-hyps = (global-hyps

∧ ((i$1 ∈ N)

∧ ((i$1 ≮ patlen$0)
∧ (i$1
< (patlen$0

+ search (pat$0, str$0, patlen$0, strlen$0, '1))))))

Theorem: definedness path-hyps → znumberp (i$1)

#| (COMMENT OUTER-INVRT) |#
; (FORTRAN-COMMENT LOGICAL-IF-T)

Axiom: logical-if-t t

Theorem: input-cond-of-zplus (zgreaterp (i$1, strlen$0) ∧ path-hyps) → expressible-znumberp (zplus (strlen$0, '1))

#| (COMMENT OUTER-INVRT T) |#

Axiom: assignment1 (i$2 = i$1) ∧ ((j$2 = j$1)

∧ ((c$2 = c$1)

∧ ((nexti$2 = nexti$1)

∧ ((x$2 = zplus (strlen$0, '1)) ∧ (blk-delta1$2 = blk-delta1$1)))))

Theorem: output (zgreaterp (i$1, strlen$0) ∧ path-hyps) → (x$2 = search (pat$0, str$0, patlen$0, strlen$0, '1))

#| (COMMENT OUTER-INVRT T) |#

Event: Undo back through the event named ‘logical-if-t’.

; (FORTRAN-COMMENT LOGICAL-IF-F)

Axiom: logical-if-f t

Axiom: assignment1 (i$2 = i$1) ∧ ((j$2 = patlen$0)

∧ ((c$2 = c$1)

∧ ((nexti$2 = nexti$1) ∧ ((x$2 = x$1)

∧ (blk-delta1$2 = blk-delta1$1)))))

Theorem: input-cond-of-zplus ((¬ zgreaterp (i$1, strlen$0)) ∧ path-hyps) → expressible-znumberp (zplus ('1, i$2))

#| (COMMENT OUTER-INVRT F) |#

Axiom: assignment2 (i$3 = i$2) ∧ ((j$3 = j$2)

∧ ((c$3 = c$2)

∧ ((nexti$3 = zplus ('1, i$2)) ∧ ((x$3 = x$2)

∧ (blk-delta1$3 = blk-delta1$2)))))

(PROVE-LEMMA INNER-INVRT NIL
(IMPLIES
(AND (NOT (ZGREATERP (I$1) (STRLEN$0)))
(PATH-HYPS))
(AND
(AND
(NOT (LESSP (NEXTI$3) (ADD1 (PATLEN$0))))
(AND
(LESSP (NEXTI$3)
(ADD1 (PLUS (PATLEN$0)
(SEARCH (PAT$0)
(STR$0)
(PATLEN$0)
(STRLEN$0)
'1))))
(AND
(IMPLIES (AND (NUMBERP C)
(AND (NOT (EQUAL C '0))
(NOT (LESSP (ASIZE&) C))))
(EQUAL (ELT1 (BLK-DELTA1$3) C)
(DELTA1 (PAT$0) C (PATLEN$0))))
(AND
(NUMBERP (I$3))
(AND
(NOT (EQUAL (I$3) '0))
(AND
(NUMBERP (J$3))
(AND
(NOT (EQUAL (J$3) '0))
(AND
(NUMBERP (NEXTI$3))
(AND
(NOT (LESSP (PATLEN$0) (J$3)))
(AND
(NOT (LESSP (STRLEN$0) (I$3)))
(AND
(EQUAL (NEXTI$3)
(PLUS (ADD1 (PATLEN$0))
(DIFFERENCE (I$3) (J$3))))
(AND
(NOT (LESSP (ADD1 (STRLEN$0)) (NEXTI$3)))
(AND

(NOT (LESSP (I$3) (J$3)))
(AND (MATCH (PAT$0)
(ADD1 (J$3))
(PATLEN$0)
(STR$0)
(ADD1 (I$3))
(STRLEN$0))
(AND (NUMBERP (ELT1 (BLK-DELTA1$3)
             (ELT1 (STR$0) (I$3))))
(AND (NUMBERP (ELT1 (STR$0) (I$3)))
   (NUMBERP (ELT1 (PAT$0) (J$3)))))))))))))))))))
(LEX (CONS (DIFFERENCE (PLUS '1
  (PLUS (STRLEN$0) (PATLEN$0)))
(SUB1 (NEXTI$3)))
(CONS (J$3) 'NIL))
(CONS (DIFFERENCE (PLUS '1
  (PLUS (STRLEN$0) (PATLEN$0)))
(I$1))
(CONS (ADD1 (PATLEN$0)) 'NIL))))))
#| (COMMENT OUTER-INVRT F) |#

Event: Undo back through the event named ‘paths-from-outer-invrt’.

Axiom: paths-from-inner-invrt (((c ∈ N) ∧ ((c ≠ '0) ∧ (asize& ≮ c))) → (elt1 (blk-delta1$1, c) = delta1 (pat$0, c, patlen$0))) ∧ (nexti$1 = ((1 + patlen$0) + (i$1 − j$1)))

(DEFN PATH-HYPS NIL
(AND
(GLOBAL-HYPS)
(AND
(NOT (LESSP (NEXTI$1) (ADD1 (PATLEN$0))))
(AND
(LESSP (NEXTI$1)
(ADD1 (PLUS (PATLEN$0)
(SEARCH (PAT$0)
 (STR$0)
 (PATLEN$0)
 (STRLEN$0)

 '1))))
(AND
(NUMBERP (I$1))
(AND
(NOT (EQUAL (I$1) '0))
(AND
(NUMBERP (J$1))
(AND
(NOT (EQUAL (J$1) '0))
(AND
(NUMBERP (NEXTI$1))
(AND
(NOT (LESSP (PATLEN$0) (J$1)))
(AND
(NOT (LESSP (STRLEN$0) (I$1)))
(AND
(NOT (LESSP (ADD1 (STRLEN$0)) (NEXTI$1)))
(AND (NOT (LESSP (I$1) (J$1)))
(AND (MATCH (PAT$0)
(ADD1 (J$1))
(PATLEN$0)
(STR$0)
(ADD1 (I$1))
(STRLEN$0))
(AND (NUMBERP (ELT1 (BLK-DELTA1$1)
             (ELT1 (STR$0) (I$1))))
(AND (NUMBERP (ELT1 (STR$0) (I$1)))
   (NUMBERP (ELT1 (PAT$0) (J$1)))))))))))))))))))

Theorem: array-bounds-check-for-str path-hyps → (('0 < i$1) ∧ (strlen$0 ≮ i$1))

#| (COMMENT INNER-INVRT) |#

Theorem: definedness path-hyps → znumberp (elt1 (str$0, i$1))

#| (COMMENT INNER-INVRT) |#

Axiom: assignment1 (i$2 = i$1) ∧ ((j$2 = j$1)

∧ ((c$2 = elt1 (str$0, i$1))

∧ ((nexti$2 = nexti$1) ∧ ((x$2 = x$1)

∧ (blk-delta1$2 = blk-delta1$1)))))

Theorem: array-bounds-check-for-pat path-hyps → (('0 < j$2) ∧ (patlen$0 ≮ j$2))

#| (COMMENT INNER-INVRT) |#

Theorem: definedness1 path-hyps → znumberp (elt1 (pat$0, j$2))

#| (COMMENT INNER-INVRT) |#
; (FORTRAN-COMMENT LOGICAL-IF-T)

Axiom: logical-if-t t

Theorem: array-bounds-check-for-delta1 (zneqp (c$2, elt1 (pat$0, j$2)) ∧ path-hyps) → (('0 < c$2) ∧ (asize& ≮ c$2))

#| (COMMENT INNER-INVRT T) |#

Theorem: definedness2 (zneqp (c$2, elt1 (pat$0, j$2)) ∧ path-hyps) → znumberp (elt1 (blk-delta1$2, c$2))

#| (COMMENT INNER-INVRT T) |#

Theorem: input-cond-of-zplus (zneqp (c$2, elt1 (pat$0, j$2)) ∧ path-hyps) → expressible-znumberp (zplus (i$2, elt1 (blk-delta1$2, c$2)))

#| (COMMENT INNER-INVRT T) |#

Theorem: definedness3 (zneqp (c$2, elt1 (pat$0, j$2)) ∧ path-hyps) → znumberp (nexti$2)

#| (COMMENT INNER-INVRT T) |#

Axiom: assignment2 (i$3 = max0 (zplus (i$2, elt1 (blk-delta1$2, c$2)), nexti$2)) ∧ ((j$3 = j$2)

∧ ((c$3 = c$2)

∧ ((nexti$3 = nexti$2) ∧ ((x$3 = x$2)

∧ (blk-delta1$3 = blk-delta1$2)))))

Theorem: delta1-plus-j-lesseqp-patlen ((j ∈ N) ∧ (j ≠ 0) ∧ (patlen ≮ j )) → (patlen ≮ (j + delta1 (pat, elt1 (pat, j ), patlen)))

Theorem: difference-plus-id ((k + j ) − j ) = fix (k)

Theorem: match-implies-eq-chars (match (pat, j , patlen, str, k, strlen) ∧ (k ∈ N) ∧ (j ∈ N) ∧ (patlen ∈ N) ∧ (strlen ∈ N) ∧ (strlen ≮ k) ∧ (patlen ≮ j ) ∧ (k ≠ 0) ∧ (j ≠ 0) ∧ (l ∈ N) ∧ (l ≮ k) ∧ ((k + patlen) ≮ (j + l))) → (elt1 (str, l) = elt1 (pat, (j + l) − k))

Theorem: neq-chars-in-region-means-search-skips ((elt1 (str, i) ≠ elt1 (pat, j )) ∧ (i ∈ N) ∧ (i ≠ 0) ∧ (strlen ∈ N) ∧ (strlen ≮ i) ∧ (j ∈ N) ∧ (j ≠ 0) ∧ (patlen ∈ N) ∧ (patlen ≮ j ) ∧ (i ≮ j ) ∧ (k ∈ N) ∧ (k ≠ 0) ∧ (strlen ≮ k) ∧ ((search (pat, str, patlen, strlen, k) − 1) ≮ (i − j ))) → ((i − j ) < (search (pat, str, patlen, strlen, k) − 1))

Theorem: delta1-doesnt-go-beyond-end-of-match (match (pat, 1, patlen, str, k, strlen) ∧ (i ∈ N) ∧ (strlen ≮ i) ∧ (patlen ∈ N) ∧ (strlen ∈ N) ∧ (k ∈ N) ∧ (k ≠ 0) ∧ (i < (k + patlen))) → (((i + delta1 (pat, elt1 (str, i), patlen)) < (k + patlen))

= ((i < k) ∨ (i = k) ∨ (k < i)))

Event: Disable match-implies-eq-chars.

Theorem: delta1-doesnt-go-beyond-search ((elt1 (str, i) ≠ elt1 (pat, j )) ∧ (i ∈ N) ∧ (strlen ≮ i) ∧ (j ∈ N) ∧ (patlen ≮ j ) ∧ (patlen ∈ N) ∧ (strlen ∈ N) ∧ ((i − j ) < search (pat, str, patlen, strlen, k)) ∧ (strlen ≮ k) ∧ (i ≮ j ) ∧ (k ∈ N) ∧ (k ≠ 0)) → ((i + delta1 (pat, elt1 (str, i), patlen))

< (patlen + search (pat, str, patlen, strlen, k)))

Theorem: outer-invrt1 (zneqp (c$2, elt1 (pat$0, j$2)) ∧ path-hyps) → (((i$3 ∈ N)

∧ ((i$3 ≮ patlen$0)

∧ ((i$3
< (patlen$0

+ search (pat$0, str$0, patlen$0, strlen$0, '1)))

∧ (((c ∈ N) ∧ ((c ≠ '0) ∧ (asize& ≮ c))) → (elt1 (blk-delta1$3, c)

= delta1 (pat$0, c, patlen$0))))))

∧ lex (cons (('1 + (strlen$0 + patlen$0)) − i$3, cons (1 + patlen$0, 'nil)),

cons (('1 + (strlen$0 + patlen$0)) − (nexti$1 − 1), cons (j$1, 'nil))))

#| (COMMENT INNER-INVRT T) |#

Event: Undo back through the event named ‘logical-if-t’.

; (FORTRAN-COMMENT LOGICAL-IF-F)

Axiom: logical-if-f t

; (FORTRAN-COMMENT LOGICAL-IF-T)

Axiom: logical-if-t t

Theorem: first-match-is-search (match (pat, 1, patlen, str, i, strlen) ∧ (strlen ∈ N) ∧ (i ∈ N) ∧ (strlen ≮ i) ∧ (k ∈ N) ∧ (i ≮ k) ∧ (k ≠ 0) ∧ (search (pat, str, patlen, strlen, k) ≮ i)) → ((i = search (pat, str, patlen, strlen, k)) = t)

Axiom: assignment2 (i$3 = i$2) ∧ ((j$3 = j$2)

∧ ((c$3 = c$2)

∧ ((nexti$3 = nexti$2) ∧ ((x$3 = i$2)

∧ (blk-delta1$3 = blk-delta1$2)))))

Theorem: output (zeqp (j$2, '1) ∧ ((¬ zneqp (c$2, elt1 (pat$0, j$2))) ∧ path-hyps)) → (x$3 = search (pat$0, str$0, patlen$0, strlen$0, '1))

#| (COMMENT INNER-INVRT F T) |#

Event: Undo back through the event named ‘logical-if-t’.

; (FORTRAN-COMMENT LOGICAL-IF-F1)

Axiom: logical-if-f1 t

Theorem: input-cond-of-zdifference ((¬ zeqp (j$2, '1)) ∧ ((¬ zneqp (c$2, elt1 (pat$0, j$2))) ∧ path-hyps)) → expressible-znumberp (zdifference (j$2, '1))

#| (COMMENT INNER-INVRT F F) |#

Axiom: assignment2 (i$3 = i$2) ∧ ((j$3 = zdifference (j$2, '1))

∧ ((c$3 = c$2)

∧ ((nexti$3 = nexti$2) ∧ ((x$3 = x$2)

∧ (blk-delta1$3 = blk-delta1$2)))))

Theorem: input-cond-of-zdifference1 ((¬ zeqp (j$2, '1)) ∧ ((¬ zneqp (c$2, elt1 (pat$0, j$2))) ∧ path-hyps)) → expressible-znumberp (zdifference (i$3, '1))

#| (COMMENT INNER-INVRT F F) |#

Axiom: assignment3 (i$4 = zdifference (i$3, '1)) ∧ ((j$4 = j$3)

∧ ((c$4 = c$3)

∧ ((nexti$4 = nexti$3) ∧ ((x$4 = x$3)

∧ (blk-delta1$4 = blk-delta1$3)))))

Theorem: open-up-difference (x − 1) = (x − 1)

(PROVE-LEMMA INNER-INVRT1 NIL
 (IMPLIES
  (AND (NOT (ZEQP (J$2) '1))

(AND (NOT (ZNEQP (C$2) (ELT1 (PAT$0) (J$2))))
(PATH-HYPS)))
(AND
(AND
(NOT (LESSP (NEXTI$4) (ADD1 (PATLEN$0))))
(AND
(LESSP (NEXTI$4)
(ADD1 (PLUS (PATLEN$0)
            (SEARCH (PAT$0)
                    (STR$0)
                    (PATLEN$0)
                    (STRLEN$0)
                    '1))))
(AND
(IMPLIES (AND (NUMBERP C)
        (AND (NOT (EQUAL C '0))
             (NOT (LESSP (ASIZE&) C))))
   (EQUAL (ELT1 (BLK-DELTA1$4) C)
          (DELTA1 (PAT$0) C (PATLEN$0))))
(AND
(NUMBERP (I$4))
(AND
(NOT (EQUAL (I$4) '0))
(AND
(NUMBERP (J$4))
(AND
(NOT (EQUAL (J$4) '0))
(AND
(NUMBERP (NEXTI$4))
(AND
(NOT (LESSP (PATLEN$0) (J$4)))
(AND
 (NOT (LESSP (STRLEN$0) (I$4)))
 (AND
  (EQUAL (NEXTI$4)
         (PLUS (ADD1 (PATLEN$0))
               (DIFFERENCE (I$4) (J$4))))
  (AND
   (NOT (LESSP (ADD1 (STRLEN$0)) (NEXTI$4)))
   (AND
      (NOT (LESSP (I$4) (J$4)))
      (AND (MATCH (PAT$0)
                  (ADD1 (J$4))
                  (PATLEN$0)

                              (STR$0)
                              (ADD1 (I$4))
                              (STRLEN$0))
                       (AND (NUMBERP (ELT1 (BLK-DELTA1$4)
                                           (ELT1 (STR$0) (I$4))))
                            (AND (NUMBERP (ELT1 (STR$0) (I$4)))
                                 (NUMBERP (ELT1 (PAT$0) (J$4)))))))))))))))))))
   (LEX (CONS (DIFFERENCE (PLUS '1
                                (PLUS (STRLEN$0) (PATLEN$0)))
                          (SUB1 (NEXTI$4)))
              (CONS (J$4) 'NIL))
        (CONS (DIFFERENCE (PLUS '1
                                (PLUS (STRLEN$0) (PATLEN$0)))
                          (SUB1 (NEXTI$1)))
              (CONS (J$1) 'NIL))))))
#| (COMMENT INNER-INVRT F F) |#

Event: Undo back through the event named ‘paths-from-inner-invrt’.

Event: Undo back through the event named ‘fortran’.

#|

The correctness of the program depends upon the following events:
@BEGIN(GROUP)
@BEGIN(VERBATIM)
        Definition.
        (DELTA1 A C MAXI)
           =
        (IF (ZEROP MAXI)
            0
            (IF (EQUAL C (ELT1 A MAXI))
                0
                (ADD1 (DELTA1 A C (SUB1 MAXI)))))
@END(VERBATIM)
@END(GROUP)
@BEGIN(GROUP)
@BEGIN(VERBATIM)

        Definition.
        (STRINGP A I SIZE)
           =
        (IF (ZEROP I)
            T
            (AND (NUMBERP (ELT1 A I))
                 (NOT (EQUAL (ELT1 A I) 0))
                 (NOT (LESSP SIZE (ELT1 A I)))
                 (STRINGP A (SUB1 I) SIZE)))
@END(VERBATIM)
@END(GROUP)
@BEGIN(GROUP)
@BEGIN(VERBATIM)
        (FORTRAN-COMMENT USEFUL-LEMMAS)
@END(VERBATIM)
@END(GROUP)
@BEGIN(GROUP)
@BEGIN(VERBATIM)
        Definition.
        (MATCH PAT J PATLEN STR I STRLEN)
           =
        (IF (LESSP PATLEN J)
            T
            (IF (LESSP STRLEN I)
                F
                (AND (EQUAL (ELT1 PAT J) (ELT1 STR I))
                     (MATCH PAT
                            (ADD1 J)
                            PATLEN STR
                            (ADD1 I)
                            STRLEN))))
        Hint:  ((LESSP (DIFFERENCE (ADD1 PATLEN) J))
                (LESSP (DIFFERENCE (ADD1 STRLEN) I)))
@END(VERBATIM)
@END(GROUP)
@BEGIN(GROUP)
@BEGIN(VERBATIM)
        Definition.
        (SEARCH PAT STR PATLEN STRLEN I)
           =
        (IF (LESSP STRLEN I)

            (ADD1 STRLEN)
            (IF (MATCH PAT 1 PATLEN STR I STRLEN)
                I
                (SEARCH PAT STR PATLEN STRLEN
                        (ADD1 I))))
        Hint:  Consider the well-founded relation LESSP
               and the measure (DIFFERENCE (ADD1 STRLEN) I)
@END(VERBATIM)
@END(GROUP)
@BEGIN(GROUP)
@BEGIN(VERBATIM)
        (FORTRAN-COMMENT USEFUL-LEMMAS-ABOUT-SEARCHING)
@END(VERBATIM)
@END(GROUP)

Specification for routine SETUP
The input assertion:
(AND (STRINGP (A STATE)
(MAXI STATE)
(ASIZE&))
(NOT (EQUAL (MAXI STATE) 0))
(NUMBERP (MAXI STATE))
(LESSP (ADD1 (ASIZE&))
(LEAST-INEXPRESSIBLE-POSITIVE-INTEGER))
(LESSP (ADD1 (MAXI STATE))
(LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))

The output assertion:
(IMPLIES (AND (NUMBERP C)
(NOT (EQUAL C 0))
(NOT (LESSP (ASIZE&) C)))
(EQUAL (ELT1 (BLK-DELTA1 NEWSTATE) C)
  (DELTA1 (A STATE) C (MAXI STATE))))

Specification for routine FSRCH
The input assertion:
(AND (LESSP (ADD1 (ASIZE&))
       (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER))
(STRINGP (PAT STATE)
         (PATLEN STATE)
         (ASIZE&))
(NUMBERP (PATLEN STATE))
(LESSP 0 (PATLEN STATE))
(STRINGP (STR STATE)
         (STRLEN STATE)
         (ASIZE&))
(NUMBERP (STRLEN STATE))
(LESSP 0 (STRLEN STATE))
(LESSP (PLUS (PATLEN STATE) (STRLEN STATE))
       (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))

The output assertion:
(EQUAL (X NEWSTATE)
  (SEARCH (PAT STATE)
          (STR STATE)
          (PATLEN STATE)
          (STRLEN STATE)
          1))

INTEGER DELTA1
DIMENSION DELTA1(ASIZE&)
COMMON /BLK/DELTA1
END
SUBROUTINE SETUP(A, MAXI)
INTEGER DELTA1
INTEGER A
INTEGER MAXI
INTEGER I
INTEGER C
DIMENSION DELTA1(ASIZE&)
DIMENSION A(MAXI)
COMMON /BLK/DELTA1
DO 50 I = 1, ASIZE&
C     DOJUNK PASS1
DELTA1(I) = MAXI
50    CONTINUE
DO 100 I = 1, MAXI
C     DOJUNK PASS2
C = A(I)
DELTA1(C) = (MAXI - I)
100   CONTINUE
RETURN
END
SUBROUTINE FSRCH(PAT, STR, PATLEN, STRLEN, X)
INTEGER DELTA1
INTEGER MAX0
INTEGER PATLEN
INTEGER STRLEN
INTEGER PAT
INTEGER STR
INTEGER I
INTEGER J
INTEGER C
INTEGER NEXTI
INTEGER X
DIMENSION DELTA1(ASIZE&)
DIMENSION PAT(PATLEN)
DIMENSION STR(STRLEN)
COMMON /BLK/DELTA1
CALL SETUP(PAT, PATLEN)
I = PATLEN
200   CONTINUE

C     XXX INNER-TO-OUTER-HINTS
      CONTINUE
C     ASSERTION OUTER-INVRT
      IF ((I .GT. STRLEN)) GOTO 500
      J = PATLEN
      NEXTI = (1 + I)
300   CONTINUE
C     ASSERTION INNER-INVRT
      C = STR(I)
      IF ((C .NE. PAT(J))) GOTO 400
      IF ((J .EQ. 1)) GOTO 600
      J = (J - 1)
      I = (I - 1)
C     XXX INNER-TO-INNER-HINTS
      GOTO 300
400   I = MAX0((I + DELTA1(C)), NEXTI)
      GOTO 200
500   X = (STRLEN + 1)
      RETURN
600   CONTINUE
C     XXX INNER-TO-EXIT-HINTS
      X = I
      RETURN
      END

The XXX at USEFUL-LEMMAS.
@BEGIN(GROUP)
@BEGIN(VERBATIM)
        Theorem.  STRINGP-IS-A-UNIV-QUANTIFIER (rewrite):
        (IMPLIES (AND (STRINGP A I (ASIZE&))
                      (NOT (EQUAL J 0))
                      (NUMBERP J)
                      (NOT (LESSP I J)))
                 (AND (NUMBERP (ELT1 A J))
                      (NOT (LESSP (ASIZE&) (ELT1 A J)))
                      (NOT (EQUAL (ELT1 A J) 0))))
@END(VERBATIM)
@END(GROUP)

The XXX at USEFUL-LEMMAS-ABOUT-SEARCHING.
@BEGIN(GROUP)

@BEGIN(VERBATIM)
        Theorem.  SEARCH-NON-ZERO (rewrite):
        (IMPLIES (NOT (ZEROP I))
                 (LESSP 0
                        (SEARCH PAT STR PATLEN STRLEN I)))
@END(VERBATIM)
@END(GROUP)
@BEGIN(GROUP)
@BEGIN(VERBATIM)
        Theorem.  MATCH-AT-PATLEN (rewrite):
        (IMPLIES (LESSP PATLEN J)
                 (MATCH PAT J PATLEN STR I STRLEN))
@END(VERBATIM)
@END(GROUP)
@BEGIN(GROUP)
@BEGIN(VERBATIM)
        Theorem.  MATCH-AT-STRLEN (rewrite):
        (IMPLIES (LESSP STRLEN I)
                 (EQUAL (MATCH PAT J PATLEN STR I STRLEN)
                        (LESSP PATLEN J)))
@END(VERBATIM)
@END(GROUP)
@BEGIN(GROUP)
@BEGIN(VERBATIM)
        Theorem.  MATCH-NEEDS-PATLEN-CHARS (rewrite):
        (IMPLIES (AND (NUMBERP PATLEN)
                      (NUMBERP STRLEN)
                      (NOT (LESSP PATLEN J))
                      (NOT (LESSP STRLEN I))
                      (LESSP (PLUS J STRLEN)
                             (PLUS I PATLEN)))
                 (NOT (MATCH PAT J PATLEN STR I STRLEN)))
@END(VERBATIM)
@END(GROUP)
@BEGIN(GROUP)
@BEGIN(VERBATIM)
        Theorem.  SEARCH-BOUNDARY (rewrite):
        (IMPLIES
               (AND (NOT (ZEROP PATLEN))
                    (NUMBERP STRLEN)

                    (NOT (LESSP STRLEN I))
                    (LESSP (ADD1 STRLEN)
                           (PLUS PATLEN
                                 (SEARCH PAT STR PATLEN STRLEN I))))
               (EQUAL (SEARCH PAT STR PATLEN STRLEN I)
                      (ADD1 STRLEN)))
@END(VERBATIM)
@END(GROUP)
@BEGIN(GROUP)
@BEGIN(VERBATIM)
        Theorem.  DELTA1-LESSEQP-PATLEN (rewrite):
        (NOT (LESSP PATLEN
                    (DELTA1 PAT CHAR PATLEN)))
@END(VERBATIM)
@END(GROUP)

Hints for routine SETUP

The input clock:
        (LIST (PLUS 2 (ASIZE&) (MAXI (START))))
The DO junk named PASS1:
        ((TEST PASS1-INVRT))
The invariant and clock named PASS1-INVRT.
        (AND (NUMBERP (I STATE))
             (NOT (EQUAL (I STATE) 0))
             (NOT (LESSP (ADD1 (ASIZE&)) (I STATE)))
             (IMPLIES (AND (NUMBERP J)
                           (NOT (EQUAL J 0))
                           (LESSP J (I STATE)))
                      (EQUAL (ELT1 (BLK-DELTA1 STATE) J)
                             (MAXI (START)))))
        (LIST (DIFFERENCE (PLUS 2 (ASIZE&) (MAXI (START)))
                          (I STATE)))
The DO junk named PASS2:
        ((TEST PASS2-INVRT)
         (JUMP PASS2-TO-PASS2-HINT))
The invariant and clock named PASS2-INVRT.
        (AND (NUMBERP (I STATE))
             (NOT (EQUAL (I STATE) 0))
             (NOT (LESSP (ADD1 (MAXI (START)))
                         (I STATE)))
             (IMPLIES (AND (NOT (ZEROP J))
                           (NOT (LESSP (ASIZE&) J)))
                      (EQUAL (ELT1 (BLK-DELTA1 STATE) J)
                             (PLUS (DELTA1 (A (START))
                                           J
                                           (SUB1 (I STATE)))
                                   (DIFFERENCE (MAXI (START))
                                               (SUB1 (I STATE)))))))

        (LIST (DIFFERENCE (ADD1 (MAXI (START)))
                          (I STATE)))
The XXX named PASS2-TO-PASS2-HINT:
@BEGIN(GROUP)
@BEGIN(VERBATIM)
        Theorem.  DELTA1-SKIP (rewrite):
        (IMPLIES (AND (NOT (EQUAL J (ELT1 PAT I)))
                      (NOT (ZEROP I)))
                 (EQUAL (DELTA1 PAT J I)
                        (ADD1 (DELTA1 PAT J (SUB1 I)))))
@END(VERBATIM)
@END(GROUP)

Hints for routine FSRCH

The input clock:
        (LIST (PLUS 1
                    (STRLEN (START))
                    (PATLEN (START)))
              (ADD1 (PATLEN (START))))
The XXX named INNER-TO-OUTER-HINTS:
        Path encryption:
        ((INNER-INVRT T))
@BEGIN(GROUP)
@BEGIN(VERBATIM)
        Theorem.  DELTA1-PLUS-J-LESSEQP-PATLEN (rewrite):
        (IMPLIES
              (AND (NUMBERP J)
                   (NOT (EQUAL J 0))
                   (NOT (LESSP PATLEN J)))
              (NOT (LESSP PATLEN
                          (PLUS J
                                (DELTA1 PAT (ELT1 PAT J) PATLEN)))))
@END(VERBATIM)
@END(GROUP)
@BEGIN(GROUP)
@BEGIN(VERBATIM)
        Theorem.  DIFFERENCE-PLUS-ID (rewrite):
        (EQUAL (DIFFERENCE (PLUS K J) J)
               (FIX K))
@END(VERBATIM)
@END(GROUP)
@BEGIN(GROUP)
@BEGIN(VERBATIM)
        Theorem.  MATCH-IMPLIES-EQ-CHARS (rewrite):
        (IMPLIES (AND (MATCH PAT J PATLEN STR K STRLEN)
                      (NUMBERP K)
                      (NUMBERP J)
                      (NUMBERP PATLEN)
                      (NUMBERP STRLEN)
                      (NOT (LESSP STRLEN K))

     (NOT (LESSP PATLEN J))
     (NOT (EQUAL K 0))
     (NOT (EQUAL J 0))
     (NUMBERP L)
     (NOT (LESSP L K))
     (NOT (LESSP (PLUS K PATLEN) (PLUS J L))))
(EQUAL (ELT1 STR L)
       (ELT1 PAT (DIFFERENCE (PLUS J L) K))))
@END(VERBATIM)
@END(GROUP)
@BEGIN(GROUP)
@BEGIN(VERBATIM)
Theorem.  NEQ-CHARS-IN-REGION-MEANS-SEARCH-SKIPS (rewrite):
(IMPLIES
(AND (NOT (EQUAL (ELT1 STR I) (ELT1 PAT J)))
(NUMBERP I)
(NOT (EQUAL I 0))
(NUMBERP STRLEN)
(NOT (LESSP STRLEN I))
(NUMBERP J)
(NOT (EQUAL J 0))
(NUMBERP PATLEN)
(NOT (LESSP PATLEN J))
(NOT (LESSP I J))
(NUMBERP K)
(NOT (EQUAL K 0))
(NOT (LESSP STRLEN K))
(NOT (LESSP (SUB1 (SEARCH PAT STR PATLEN STRLEN K))
            (DIFFERENCE I J))))
(LESSP (DIFFERENCE I J)
  (SUB1 (SEARCH PAT STR PATLEN STRLEN K))))
@END(VERBATIM)
@END(GROUP)
@BEGIN(GROUP)
@BEGIN(VERBATIM)
Theorem.  DELTA1-DOESNT-GO-BEYOND-END-OF-MATCH (rewrite):
(IMPLIES
(AND (MATCH PAT 1 PATLEN STR K STRLEN)
   (NUMBERP I)
   (NOT (LESSP STRLEN I))
   (NUMBERP PATLEN)
   (NUMBERP STRLEN)

(NUMBERP K)
(NOT (EQUAL K 0))
(LESSP I (PLUS K PATLEN)))
(EQUAL (LESSP (PLUS I
             (DELTA1 PAT (ELT1 STR I) PATLEN))
       (PLUS K PATLEN))
(OR (LESSP I K)
    (EQUAL I K)
    (LESSP K I))))
@END(VERBATIM)
@END(GROUP)
@BEGIN(GROUP)
@BEGIN(VERBATIM)
Enable MATCH-IMPLIES-EQ-CHARS.
@END(VERBATIM)
@END(GROUP)
@BEGIN(GROUP)
@BEGIN(VERBATIM)
Theorem.  DELTA1-DOESNT-GO-BEYOND-SEARCH (rewrite):
(IMPLIES (AND (NOT (EQUAL (ELT1 STR I) (ELT1 PAT J)))
(NUMBERP I)
(NOT (LESSP STRLEN I))
(NUMBERP J)
(NOT (LESSP PATLEN J))
(NUMBERP PATLEN)
(NUMBERP STRLEN)
(LESSP (DIFFERENCE I J)
       (SEARCH PAT STR PATLEN STRLEN K))
(NOT (LESSP STRLEN K))
(NOT (LESSP I J))
(NUMBERP K)
(NOT (EQUAL K 0)))
(LESSP (PLUS I
        (DELTA1 PAT (ELT1 STR I) PATLEN))
  (PLUS PATLEN
        (SEARCH PAT STR PATLEN STRLEN K))))
@END(VERBATIM)
@END(GROUP)

The invariant and clock named OUTER-INVRT.

(AND (NUMBERP (I STATE))
(NOT (LESSP (I STATE) (PATLEN (START))))
(LESSP (I STATE)
       (PLUS (PATLEN (START))
             (SEARCH (PAT (START))
                     (STR (START))
                     (PATLEN (START))
                     (STRLEN (START))
                     1)))
(IMPLIES (AND (NUMBERP C)
              (NOT (EQUAL C 0))
              (NOT (LESSP (ASIZE&) C)))
         (EQUAL (ELT1 (BLK-DELTA1 STATE) C)
                (DELTA1 (PAT (START))
                        C
                        (PATLEN (START))))))
(LIST (DIFFERENCE (PLUS 1
                   (STRLEN (START))
                   (PATLEN (START)))
             (I STATE))
 (ADD1 (PATLEN (START))))
The invariant and clock named INNER-INVRT.
(AND (NOT (LESSP (NEXTI STATE)
            (ADD1 (PATLEN (START)))))
(LESSP (NEXTI STATE)
       (ADD1 (PLUS (PATLEN (START))
                   (SEARCH (PAT (START))
                           (STR (START))
                           (PATLEN (START))
                           (STRLEN (START))
                           1))))
(IMPLIES (AND (NUMBERP C)
              (NOT (EQUAL C 0))
              (NOT (LESSP (ASIZE&) C)))
         (EQUAL (ELT1 (BLK-DELTA1 STATE) C)
                (DELTA1 (PAT (START))
                        C
                        (PATLEN (START)))))
(NUMBERP (I STATE))
(NOT (EQUAL (I STATE) 0))

(NUMBERP (J STATE))
(NOT (EQUAL (J STATE) 0))
(NUMBERP (NEXTI STATE))
(NOT (LESSP (PATLEN (START)) (J STATE)))
(NOT (LESSP (STRLEN (START)) (I STATE)))
(EQUAL (NEXTI STATE)
       (PLUS (ADD1 (PATLEN (START)))
             (DIFFERENCE (I STATE) (J STATE))))
(NOT (LESSP (ADD1 (STRLEN (START)))
            (NEXTI STATE)))
(NOT (LESSP (I STATE) (J STATE)))
(MATCH (PAT (START))
       (ADD1 (J STATE))
       (PATLEN (START))
       (STR (START))
       (ADD1 (I STATE))
       (STRLEN (START)))
(NUMBERP (ELT1 (BLK-DELTA1 STATE)
               (ELT1 (STR (START)) (I STATE))))
(NUMBERP (ELT1 (STR (START)) (I STATE)))
(NUMBERP (ELT1 (PAT (START)) (J STATE))))
(LIST (DIFFERENCE (PLUS 1
                   (STRLEN (START))
                   (PATLEN (START)))
             (SUB1 (NEXTI STATE)))
 (J STATE))
The XXX named INNER-TO-INNER-HINTS:
@BEGIN(GROUP)
@BEGIN(VERBATIM)
Theorem.  OPEN-UP-DIFFERENCE (rewrite):
(EQUAL (DIFFERENCE X 1) (SUB1 X))
@END(VERBATIM)
@END(GROUP)

The XXX named INNER-TO-EXIT-HINTS:
@BEGIN(GROUP)
@BEGIN(VERBATIM)
Theorem.  FIRST-MATCH-IS-SEARCH (rewrite):
(IMPLIES (AND (MATCH PAT 1 PATLEN STR I STRLEN)
         (NUMBERP STRLEN)

(NUMBERP I)
(NOT (LESSP STRLEN I))
(NUMBERP K)
(NOT (LESSP I K))
(NOT (EQUAL K 0))
(NOT (LESSP (SEARCH PAT STR PATLEN STRLEN K)
            I)))
(EQUAL (EQUAL I
         (SEARCH PAT STR PATLEN STRLEN K))
  T))
@END(VERBATIM)
@END(GROUP)
|#

Index

a$0, 2, 3, 5–8 almost-equal1, 5, 6, 8 array-bounds-check-for-a, 7 array-bounds-check-for-delta1, 5, 7,

19 array-bounds-check-for-pat, 19 array-bounds-check-for-str, 18 asize&, 2–8, 11–14, 17, 19, 21 asize&-numberp, 3, 11 assignment, 4, 13 assignment1, 5, 7, 15, 18 assignment2, 6, 8, 15, 20, 22, 23 assignment3, 8, 23

blk-delta1$0, 2, 4 blk-delta1$1, 2, 4–7, 9, 13–15, 17,

19 blk-delta1$2, 2, 4–9, 13–15, 19, 20,

22, 23 blk-delta1$3, 2, 5, 6, 8, 9, 15, 20–23 blk-delta1$4, 2, 8, 9, 23

c$0, 2, 4, 9, 13 c$1, 2, 4–6, 9, 13, 15 c$2, 2, 4–9, 13, 15, 18–23 c$3, 2, 5, 6, 8, 9, 15, 20, 22, 23 c$4, 2, 8, 9, 23 call-of-setup, 13

definedness, 4, 6, 14, 18 definedness1, 7, 19 definedness2, 19 definedness3, 19 delta1, 3, 5–8, 11–14, 17, 20–22 delta1-doesnt-go-beyond-end-of-

match, 21 delta1-doesnt-go-beyond-search, 21 delta1-lesseqp-patlen, 12 delta1-plus-j-lesseqp-patlen, 20 delta1-skip, 8 difference-plus-id, 20 effects-of-setup, 13 effects-of-undefiner, 4, 6 elt1, 3–8, 11, 13, 14, 17–23 expressible-znumberp, 5, 7, 8, 14,

15, 19, 23

first-match-is-search, 22

fortran, 1, 9

global-hyps, 3, 4, 6, 12–14

i$0, 9, 13

i$1, 2, 4–9, 13–15, 17, 18

i$2, 2, 5–9, 13–15, 18–20, 22, 23 i$3, 2, 5, 6, 8, 9, 15, 20–23 i$4, 2, 8, 10, 23 input, 3, 13 input-cond-of-zdifference, 7, 23 input-cond-of-zdifference1, 23 input-cond-of-zplus, 5, 8, 14, 15, 19 input-conditions, 3, 11 input-definedness, 3, 12

j$0, 10, 13

j$1, 10, 13, 15, 17, 18, 22 j$2, 10, 13, 15, 18–23 j$3, 10, 15, 20, 22, 23 j$4, 10, 23

least-inexpressible-positive-inte

ger, 3, 12, 13 lex, 4–6, 8, 14, 22 logical-if-f, 4, 15, 22 logical-if-f1, 5, 7, 23 logical-if-t, 4, 6, 14, 19, 22

match, 11, 12, 20–22 match-at-patlen, 12 match-at-strlen, 12 match-implies-eq-chars, 20 match-needs-patlen-chars, 12 max0, 20 maxi$0, 2–8

neq-chars-in-region-means-searc

h-skips, 20 nexti$0, 10, 13 nexti$1, 10, 13, 15, 17, 19, 22 nexti$2, 10, 13, 15, 19, 20, 22, 23 nexti$3, 10, 15, 20, 22, 23 nexti$4, 10, 23

open-up-difference, 23 outer-invrt, 13 outer-invrt1, 21 output, 7, 15, 22

pass1-invrt, 4 pass1-invrt1, 6 pass2-invrt, 5 pass2-invrt1, 8 pat$0, 10, 12–15, 17, 19, 21–23 path-hyps, 4–8, 14, 15, 18, 19, 21–

23 paths-from-inner-invrt, 17 paths-from-outer-invrt, 14 paths-from-pass1-invrt, 4 paths-from-pass2-invrt, 6 patlen$0, 10, 12–15, 17, 19, 21, 22

search, 11–15, 20–22 search-boundary, 12 search-non-zero, 12 str$0, 10, 12–15, 18, 21, 22 stringp, 3, 11–13 stringp-is-a-univ-quantifier, 3, 11 strlen$0, 10, 12–15, 18, 21, 22

x$0, 10, 13 x$1, 10, 13, 15, 19 x$2, 10, 13, 15, 19, 20, 23 x$3, 11, 15, 20, 22, 23 x$4, 11, 23

zdifference, 7, 8, 23 zeqp, 22, 23 zgreaterp, 5–8, 14, 15 zneqp, 19, 21–23 znumberp, 4, 6, 7, 14, 18, 19 zplus, 5, 6, 8, 14, 15, 19, 20