#|
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 version of our
; majority vote 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 boole$0 of 0 arguments. Event: Introduce the function symbol boole$1 of 0 arguments. Event: Introduce the function symbol boole$2 of 0 arguments. Event: Introduce the function symbol boole$3 of 0 arguments. Event: Introduce the function symbol boole$4 of 0 arguments. Event: Introduce the function symbol boole$5 of 0 arguments. Event: Introduce the function symbol boole$6 of 0 arguments. Event: Introduce the function symbol boole$7 of 0 arguments. Event: Introduce the function symbol boole$8 of 0 arguments. Event: Introduce the function symbol cand$0 of 0 arguments. Event: Introduce the function symbol cand$1 of 0 arguments. Event: Introduce the function symbol cand$2 of 0 arguments. Event: Introduce the function symbol cand$3 of 0 arguments. Event: Introduce the function symbol cand$4 of 0 arguments. Event: Introduce the function symbol cand$5 of 0 arguments. Event: Introduce the function symbol cand$6 of 0 arguments. Event: Introduce the function symbol cand$7 of 0 arguments.

Event: Introduce the function symbol cand$8 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 i$5 of 0 arguments. Event: Introduce the function symbol i$6 of 0 arguments. Event: Introduce the function symbol i$7 of 0 arguments. Event: Introduce the function symbol i$8 of 0 arguments. Event: Introduce the function symbol k$1 of 0 arguments. Event: Introduce the function symbol k$2 of 0 arguments. Event: Introduce the function symbol k$3 of 0 arguments. Event: Introduce the function symbol k$4 of 0 arguments. Event: Introduce the function symbol k$5 of 0 arguments. Event: Introduce the function symbol k$6 of 0 arguments. Event: Introduce the function symbol k$7 of 0 arguments. Event: Introduce the function symbol k$8 of 0 arguments.

Event: Introduce the function symbol n$0 of 0 arguments.

Definition: cnt (x, a, i, n) = if (n ≃ 0) ∨ (n < i) then 0

elseif zeqp (x, elt1 (a, n)) then 1 + cnt (x, a, i, n − 1)

else cnt (x, a, i, n − 1) endif

Axiom: input-conditions (('0 < j ) ∧ ((n$0 ≮ j ) ∧ (¬ negativep (elt1 (a, j ))))) → (elt1 (a, j ) ∈ N)

Definition: global-hyps = ((n$0 ≠ '0)

∧ (((1 + n$0) < least-inexpressible-positive-integer) ∧ (n$0 ∈ N)))

Theorem: plus-1 (1 + x) = (1 + x)

Theorem: difference-0 (x ≮ y) → ((y − x) = 0)

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

Theorem: lessp-x-1 (x < 1) = (x ≃ 0)

Theorem: lessp-remainder2 ((x mod y) < y) = (y ≄ 0)

Theorem: remainder-quotient-elim ((y ≄ 0) ∧ (x ∈ N)) → (((x mod y) + (y ∗ (x ÷ y))) = x)

Theorem: quotient-by-2-bound x ≮ (x ÷ 2)

Theorem: lessp-quotient-rewrite ((n ÷ 2) < m) = (n < (m + m))

Theorem: znormalize-zero (x ∈ N) → ((znormalize (x) = 0) = (x = 0))

Event: Disable znormalize.

Theorem: cnt-bound n ≮ cnt (x, a, 1, n)

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

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

Axiom: input t

Axiom: assignment (boole$1 = boole$0) ∧ ((cand$1 = cand$0) ∧ ((i$1 = i$0) ∧ (k$1 = '0)))

; (FORTRAN-COMMENT LOGICAL-IF-F)

Axiom: logical-if-f t

Axiom: assignment1 (boole$2 = boole$1) ∧ ((cand$2 = cand$1) ∧ ((i$2 = '1) ∧ (k$2 = k$1)))

; (FORTRAN-COMMENT LOGICAL-IF-T)

Axiom: logical-if-t t

Axiom: effects-of-undefiner (boole$3 = boole$2) ∧ ((cand$3 = cand$2) ∧ (k$3 = k$2))

; (FORTRAN-COMMENT LOGICAL-IF-T1)

Axiom: logical-if-t1 t

Axiom: assignment2 (boole$4 = '*1*false) ∧ ((cand$4 = cand$3) ∧ ((i$4 = i$3) ∧ (k$4 = k$3)))

Theorem: output (zeqp (k$3, '0) ∧ (i$2 ∧ (zgreaterp (i$2, n$0) ∧ global-hyps))) → (((boole$4 = '*1*true) ∨ (boole$4 = '*1*false))

∧ if boole$4

then znumberp (cand$4)

∧ ((n$0 ÷ '2) < cnt (cand$4, a$0, '1, n$0)) else (n$0 ÷ '2) ≮ cnt (x, a$0, '1, n$0) endif)

#| (COMMENT INPUT F T T) |#

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

; (FORTRAN-COMMENT LOGICAL-IF-F1)

Axiom: logical-if-f1 t

Axiom: assignment2 (boole$4 = '*1*true) ∧ ((cand$4 = cand$3) ∧ ((i$4 = i$3) ∧ (k$4 = k$3)))

Theorem: input-cond-of-zquotient ((¬ zeqp (k$3, '0)) ∧ (i$2 ∧ (zgreaterp (i$2, n$0) ∧ global-hyps))) → ((¬ zeqp ('2, '0)) ∧ expressible-znumberp (zquotient (n$0, '2)))

#| (COMMENT INPUT F T F) |#
; (FORTRAN-COMMENT LOGICAL-IF-T1)

Axiom: logical-if-t1 t

Theorem: output (zgreaterp (k$4, zquotient (n$0, '2)) ∧ ((¬ zeqp (k$3, '0))

∧ (i$2 ∧ (zgreaterp (i$2, n$0) ∧ global-hyps)))) → (((boole$4 = '*1*true) ∨ (boole$4 = '*1*false))

∧ if boole$4

then znumberp (cand$4)

∧ ((n$0 ÷ '2) < cnt (cand$4, a$0, '1, n$0)) else (n$0 ÷ '2) ≮ cnt (x, a$0, '1, n$0) endif)

#| (COMMENT INPUT F T F T) |#

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

; (FORTRAN-COMMENT LOGICAL-IF-F2)

Axiom: logical-if-f2 t Axiom: assignment3 (boole$5 = boole$4) ∧ ((cand$5 = cand$4) ∧ ((i$5 = i$4) ∧ (k$5 = '0)))

; (FORTRAN-COMMENT LOGICAL-IF-F3)

Axiom: logical-if-f3 t

Axiom: assignment4 (boole$6 = boole$5) ∧ ((cand$6 = cand$5) ∧ ((i$6 = '1) ∧ (k$6 = k$5)))

; (FORTRAN-COMMENT LOGICAL-IF-T1)

Axiom: logical-if-t1 t

Axiom: effects-of-undefiner1 (boole$7 = boole$6) ∧ ((cand$7 = cand$6) ∧ (k$7 = k$6))

Axiom: assignment5 (boole$8 = '*1*false) ∧ ((cand$8 = cand$7) ∧ ((i$8 = i$7) ∧ (k$8 = k$7)))

Theorem: output (i$6 ∧ (zgreaterp (i$6, n$0)

∧ ((¬ zgreaterp (k$4, zquotient (n$0, '2)))

∧ ((¬ zeqp (k$3, '0))

∧ (i$2

∧ (zgreaterp (i$2, n$0) ∧ global-hyps))))))

→ (((boole$8 = '*1*true) ∨ (boole$8 = '*1*false))

∧ if boole$8

then znumberp (cand$8)

∧ ((n$0 ÷ '2) < cnt (cand$8, a$0, '1, n$0)) else (n$0 ÷ '2) ≮ cnt (x, a$0, '1, n$0) endif)

#| (COMMENT INPUT F T F F F T) |#

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

; (FORTRAN-COMMENT LOGICAL-IF-F4)

Axiom: logical-if-f4 t

Theorem: array-bounds-check-for-a ((¬ zgreaterp (i$6, n$0)) ∧ ((¬ zgreaterp (k$4, zquotient (n$0, '2)))

∧ ((¬ zeqp (k$3, '0))

∧ (i$2 ∧ (zgreaterp (i$2, n$0) ∧ global-hyps)))))

→ (('0 < i$6) ∧ (n$0 ≮ i$6))

#| (COMMENT INPUT F T F F F F) |#

Theorem: definedness ((¬ zgreaterp (i$6, n$0)) ∧ ((¬ zgreaterp (k$4, zquotient (n$0, '2)))

∧ ((¬ zeqp (k$3, '0))

∧ (i$2 ∧ (zgreaterp (i$2, n$0) ∧ global-hyps)))))

→ znumberp (cand$6)

#| (COMMENT INPUT F T F F F F) |#

Theorem: definedness1 ((¬ zgreaterp (i$6, n$0)) ∧ ((¬ zgreaterp (k$4, zquotient (n$0, '2)))

∧ ((¬ zeqp (k$3, '0))

∧ (i$2 ∧ (zgreaterp (i$2, n$0) ∧ global-hyps)))))

→ znumberp (elt1 (a$0, i$6))

#| (COMMENT INPUT F T F F F F) |#
; (FORTRAN-COMMENT LOGICAL-IF-T1)

Axiom: logical-if-t1 t

Theorem: phase2-invrt (zneqp (cand$6, elt1 (a$0, i$6)) ∧ ((¬ zgreaterp (i$6, n$0))

∧ ((¬ zgreaterp (k$4, zquotient (n$0, '2)))

∧ ((¬ zeqp (k$3, '0))

∧ (i$2

∧ (zgreaterp (i$2, n$0) ∧ global-hyps))))))

→ (((i$6 ∈ N)

∧ ((i$6 ≠ '0)

∧ ((boole$6 = '*1*true) ∧ ((n$0 ≮ i$6)

∧ (((¬ negativep (cand$6)) → (cand$6 ∈ N)) ∧ ((zneqp (x, cand$6) → (n$0

                                ≮ ('2

∗ cnt (x,

a$0,

                                           '1,

n$0))))

∧ ((n$0

                                ≮ ('2

∗ cnt (cand$6, a$0,

                                           '1,

i$6)))

∧ (k$6

= cnt (cand$6, a$0,

                                          '1,

i$6)))))))))

∧ lex (cons ((1 + n$0) − i$6, 'nil), cons (1 + (1 + (n$0 + n$0)), 'nil)))

#| (COMMENT INPUT F T F F F F T) |#

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

; (FORTRAN-COMMENT LOGICAL-IF-F5)

Axiom: logical-if-f5 t

Theorem: input-cond-of-zplus ((¬ zneqp (cand$6, elt1 (a$0, i$6))) ∧ ((¬ zgreaterp (i$6, n$0))

∧ ((¬ zgreaterp (k$4, zquotient (n$0, '2)))

∧ ((¬ zeqp (k$3, '0))

∧ (i$2

∧ (zgreaterp (i$2, n$0) ∧ global-hyps))))))

→ expressible-znumberp (zplus (k$6, '1))

#| (COMMENT INPUT F T F F F F F) |#

Axiom: assignment5 (boole$7 = boole$6) ∧ ((cand$7 = cand$6) ∧ ((i$7 = i$6) ∧ (k$7 = zplus (k$6, '1))))

Theorem: input-cond-of-zquotient1 ((¬ zneqp (cand$6, elt1 (a$0, i$6))) ∧ ((¬ zgreaterp (i$6, n$0))

∧ ((¬ zgreaterp (k$4, zquotient (n$0, '2)))

∧ ((¬ zeqp (k$3, '0))

∧ (i$2

∧ (zgreaterp (i$2, n$0) ∧ global-hyps))))))

→ ((¬ zeqp ('2, '0)) ∧ expressible-znumberp (zquotient (n$0, '2)))

#| (COMMENT INPUT F T F F F F F) |#
; (FORTRAN-COMMENT LOGICAL-IF-T1)

Axiom: logical-if-t1 t

Theorem: output (zgreaterp (k$7, zquotient (n$0, '2)) ∧ ((¬ zneqp (cand$6, elt1 (a$0, i$6)))

∧ ((¬ zgreaterp (i$6, n$0))

∧ ((¬ zgreaterp (k$4, zquotient (n$0, '2)))

∧ ((¬ zeqp (k$3, '0))

∧ (i$2

∧ (zgreaterp (i$2, n$0)

∧ global-hyps)))))))

→ (((boole$7 = '*1*true) ∨ (boole$7 = '*1*false))

∧ if boole$7

then znumberp (cand$7)

∧ ((n$0 ÷ '2) < cnt (cand$7, a$0, '1, n$0)) else (n$0 ÷ '2) ≮ cnt (x, a$0, '1, n$0) endif)

#| (COMMENT INPUT F T F F F F F T) |#

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

; (FORTRAN-COMMENT LOGICAL-IF-F6)

Axiom: logical-if-f6 t

Theorem: phase2-invrt ((¬ zgreaterp (k$7, zquotient (n$0, '2))) ∧ ((¬ zneqp (cand$6, elt1 (a$0, i$6)))

∧ ((¬ zgreaterp (i$6, n$0))

∧ ((¬ zgreaterp (k$4, zquotient (n$0, '2)))

∧ ((¬ zeqp (k$3, '0))

∧ (i$2

∧ (zgreaterp (i$2, n$0)

∧ global-hyps)))))))

→ (((i$7 ∈ N)

∧ ((i$7 ≠ '0)

∧ ((boole$7 = '*1*true) ∧ ((n$0 ≮ i$7)

∧ (((¬ negativep (cand$7)) → (cand$7 ∈ N)) ∧ ((zneqp (x, cand$7) → (n$0

                                ≮ ('2

∗ cnt (x,

a$0,

                                           '1,

n$0))))

∧ ((n$0

                                ≮ ('2

∗ cnt (cand$7, a$0,

                                           '1,

i$7)))

∧ (k$7

= cnt (cand$7, a$0,

                                          '1,

i$7)))))))))

∧ lex (cons ((1 + n$0) − i$7, 'nil), cons (1 + (1 + (n$0 + n$0)), 'nil)))

#| (COMMENT INPUT F T F F F F F F) |#

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

; (FORTRAN-COMMENT LOGICAL-IF-F1)

; (FORTRAN-COMMENT LOGICAL-IF-T)

Axiom: logical-if-t t

Theorem: array-bounds-check-for-a (zeqp (k$2, '0) ∧ ((¬ zgreaterp (i$2, n$0)) ∧ global-hyps)) → (('0 < i$2) ∧ (n$0 ≮ i$2))

#| (COMMENT INPUT F F T) |#

Theorem: definedness (zeqp (k$2, '0) ∧ ((¬ zgreaterp (i$2, n$0)) ∧ global-hyps)) → znumberp (elt1 (a$0, i$2))

#| (COMMENT INPUT F F T) |#

Axiom: assignment2 (boole$3 = boole$2) ∧ ((cand$3 = elt1 (a$0, i$2)) ∧ ((i$3 = i$2) ∧ (k$3 = k$2)))

Axiom: assignment3 (boole$4 = boole$3) ∧ ((cand$4 = cand$3) ∧ ((i$4 = i$3) ∧ (k$4 = '1)))

(PROVE-LEMMA PHASE1-INVRT NIL
 (IMPLIES
  (AND (ZEQP (K$2) '0)
       (AND (NOT (ZGREATERP (I$2) (N$0)))
            (GLOBAL-HYPS)))
  (AND
   (AND
    (NUMBERP (I$4))
    (AND
     (NOT (EQUAL (I$4) '0))
     (AND
      (NUMBERP (K$4))
      (AND
       (NOT (LESSP (I$4) (K$4)))

       (AND
        (NOT (LESSP (N$0) (I$4)))
        (AND
         (IMPLIES (NOT (NEGATIVEP (CAND$4)))
                  (NUMBERP (CAND$4)))
         (AND
          (NOT (LESSP (CNT (CAND$4) (A$0) '1 (I$4))
                      (K$4)))
          (AND
           (IMPLIES
                  (ZEQP X (CAND$4))
                  (NOT (LESSP (PLUS (I$4) (K$4))
                              (TIMES '2 (CNT X (A$0) '1 (I$4))))))
           (IMPLIES
            (ZNEQP X (CAND$4))
            (NOT
             (LESSP
                   (I$4)
                   (PLUS (K$4)
                         (TIMES '2
                                (CNT X (A$0) '1 (I$4)))))))))))))))
   (LEX (CONS (ADD1 (PLUS (N$0)
                          (DIFFERENCE (ADD1 (N$0)) (I$4))))
              'NIL)
        (CONS (ADD1 (ADD1 (PLUS (N$0) (N$0))))
              'NIL)))))
#| (COMMENT INPUT F F T) |#

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

; (FORTRAN-COMMENT LOGICAL-IF-F2)

Axiom: logical-if-f2 t

Theorem: array-bounds-check-for-a ((¬ zeqp (k$2, '0)) ∧ ((¬ zgreaterp (i$2, n$0)) ∧ global-hyps)) → (('0 < i$2) ∧ (n$0 ≮ i$2))

#| (COMMENT INPUT F F F) |#

Theorem: definedness ((¬ zeqp (k$2, '0)) ∧ ((¬ zgreaterp (i$2, n$0)) ∧ global-hyps)) → znumberp (cand$2)

#| (COMMENT INPUT F F F) |#

Theorem: definedness1 ((¬ zeqp (k$2, '0)) ∧ ((¬ zgreaterp (i$2, n$0)) ∧ global-hyps)) → znumberp (elt1 (a$0, i$2))

#| (COMMENT INPUT F F F) |#
; (FORTRAN-COMMENT LOGICAL-IF-T)

Axiom: logical-if-t t

Theorem: input-cond-of-zplus (zeqp (cand$2, elt1 (a$0, i$2)) ∧ ((¬ zeqp (k$2, '0)) ∧ ((¬ zgreaterp (i$2, n$0)) ∧ global-hyps))) → expressible-znumberp (zplus (k$2, '1))

#| (COMMENT INPUT F F F T) |#

Axiom: assignment2 (boole$3 = boole$2) ∧ ((cand$3 = cand$2) ∧ ((i$3 = i$2) ∧ (k$3 = zplus (k$2, '1))))

(PROVE-LEMMA PHASE1-INVRT NIL
 (IMPLIES
  (AND (ZEQP (CAND$2) (ELT1 (A$0) (I$2)))
       (AND (NOT (ZEQP (K$2) '0))
            (AND (NOT (ZGREATERP (I$2) (N$0)))
                 (GLOBAL-HYPS))))
  (AND
   (AND
    (NUMBERP (I$3))
    (AND
     (NOT (EQUAL (I$3) '0))
     (AND
      (NUMBERP (K$3))

      (AND
       (NOT (LESSP (I$3) (K$3)))
       (AND
        (NOT (LESSP (N$0) (I$3)))
        (AND
         (IMPLIES (NOT (NEGATIVEP (CAND$3)))
                  (NUMBERP (CAND$3)))
         (AND
          (NOT (LESSP (CNT (CAND$3) (A$0) '1 (I$3))
                      (K$3)))
          (AND
           (IMPLIES
                  (ZEQP X (CAND$3))
                  (NOT (LESSP (PLUS (I$3) (K$3))
                              (TIMES '2 (CNT X (A$0) '1 (I$3))))))
           (IMPLIES
            (ZNEQP X (CAND$3))
            (NOT
             (LESSP
                   (I$3)
                   (PLUS (K$3)
                         (TIMES '2
                                (CNT X (A$0) '1 (I$3)))))))))))))))
   (LEX (CONS (ADD1 (PLUS (N$0)
                          (DIFFERENCE (ADD1 (N$0)) (I$3))))
              'NIL)
        (CONS (ADD1 (ADD1 (PLUS (N$0) (N$0))))
              'NIL)))))
#| (COMMENT INPUT F F F T) |#

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

; (FORTRAN-COMMENT LOGICAL-IF-F3)

Axiom: logical-if-f3 t

Theorem: input-cond-of-zdifference ((¬ zeqp (cand$2, elt1 (a$0, i$2))) ∧ ((¬ zeqp (k$2, '0)) ∧ ((¬ zgreaterp (i$2, n$0)) ∧ global-hyps))) → expressible-znumberp (zdifference (k$2, '1))

#| (COMMENT INPUT F F F F) |#

Axiom: assignment2 (boole$3 = boole$2) ∧ ((cand$3 = cand$2)

∧ ((i$3 = i$2) ∧ (k$3 = zdifference (k$2, '1))))

(PROVE-LEMMA PHASE1-INVRT NIL
 (IMPLIES
  (AND (NOT (ZEQP (CAND$2) (ELT1 (A$0) (I$2))))
       (AND (NOT (ZEQP (K$2) '0))
            (AND (NOT (ZGREATERP (I$2) (N$0)))
                 (GLOBAL-HYPS))))
  (AND
   (AND
    (NUMBERP (I$3))
    (AND
     (NOT (EQUAL (I$3) '0))
     (AND
      (NUMBERP (K$3))
      (AND
       (NOT (LESSP (I$3) (K$3)))
       (AND
        (NOT (LESSP (N$0) (I$3)))
        (AND
         (IMPLIES (NOT (NEGATIVEP (CAND$3)))
                  (NUMBERP (CAND$3)))
         (AND
          (NOT (LESSP (CNT (CAND$3) (A$0) '1 (I$3))
                      (K$3)))
          (AND
           (IMPLIES
                  (ZEQP X (CAND$3))
                  (NOT (LESSP (PLUS (I$3) (K$3))
                              (TIMES '2 (CNT X (A$0) '1 (I$3))))))
           (IMPLIES
            (ZNEQP X (CAND$3))
            (NOT
             (LESSP
                   (I$3)
                   (PLUS (K$3)

                         (TIMES '2
                                (CNT X (A$0) '1 (I$3)))))))))))))))
   (LEX (CONS (ADD1 (PLUS (N$0)
                          (DIFFERENCE (ADD1 (N$0)) (I$3))))
              'NIL)
        (CONS (ADD1 (ADD1 (PLUS (N$0) (N$0))))
              'NIL)))))
#| (COMMENT INPUT F F F F) |#

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

Axiom: paths-from-phase1-invrt (zeqp (x, cand$1) → ((i$1 + k$1) ≮ ('2 ∗ cnt (x, a$0, '1, i$1)))) ∧ (zneqp (x, cand$1) → (i$1 ≮ (k$1 + ('2 ∗ cnt (x, a$0, '1, i$1)))))

Definition: path-hyps = (global-hyps

∧ ((i$1 ∈ N)

∧ ((i$1 ≠ '0)
∧ ((k$1 ∈ N)
∧ ((i$1 ≮ k$1)
∧ ((n$0 ≮ i$1)

∧ (((¬ negativep (cand$1)) → (cand$1 ∈ N))

∧ (cnt (cand$1,

a$0,

                                     '1,

i$1) ≮ k$1))))))))

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

#| (COMMENT PHASE1-INVRT) |#

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

#| (COMMENT PHASE1-INVRT) |#

Axiom: assignment3 (boole$2 = boole$1) ∧ ((cand$2 = cand$1) ∧ ((i$2 = zplus (i$1, '1)) ∧ (k$2 = k$1)))

; (FORTRAN-COMMENT LOGICAL-IF-T)

Axiom: logical-if-t t

Axiom: effects-of-undefiner (boole$3 = boole$2) ∧ ((cand$3 = cand$2) ∧ (k$3 = k$2))

Theorem: definedness3 (i$2 ∧ (zgreaterp (i$2, n$0) ∧ path-hyps)) → znumberp (k$3)

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

Axiom: logical-if-t1 t

Axiom: assignment4 (boole$4 = '*1*false) ∧ ((cand$4 = cand$3) ∧ ((i$4 = i$3) ∧ (k$4 = k$3)))

Theorem: compound-invrt (k$1 = 0) → (i$1 ≮ (2 ∗ cnt (x, a$0, 1, i$1)))

Theorem: output (zeqp (k$3, '0) ∧ (i$2 ∧ (zgreaterp (i$2, n$0) ∧ path-hyps))) → (((boole$4 = '*1*true) ∨ (boole$4 = '*1*false))

∧ if boole$4

then znumberp (cand$4)

∧ ((n$0 ÷ '2) < cnt (cand$4, a$0, '1, n$0)) else (n$0 ÷ '2) ≮ cnt (x, a$0, '1, n$0) endif)

#| (COMMENT PHASE1-INVRT T T) |#

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

; (FORTRAN-COMMENT LOGICAL-IF-F4)

Axiom: logical-if-f4 t Axiom: assignment4 (boole$4 = '*1*true) ∧ ((cand$4 = cand$3) ∧ ((i$4 = i$3) ∧ (k$4 = k$3)))

Theorem: input-cond-of-zquotient ((¬ zeqp (k$3, '0)) ∧ (i$2 ∧ (zgreaterp (i$2, n$0) ∧ path-hyps))) → ((¬ zeqp ('2, '0)) ∧ expressible-znumberp (zquotient (n$0, '2)))

#| (COMMENT PHASE1-INVRT T F) |#
; (FORTRAN-COMMENT LOGICAL-IF-T1)

Axiom: logical-if-t1 t

Theorem: output (zgreaterp (k$4, zquotient (n$0, '2)) ∧ ((¬ zeqp (k$3, '0))

∧ (i$2 ∧ (zgreaterp (i$2, n$0) ∧ path-hyps)))) → (((boole$4 = '*1*true) ∨ (boole$4 = '*1*false))

∧ if boole$4

then znumberp (cand$4)

∧ ((n$0 ÷ '2) < cnt (cand$4, a$0, '1, n$0)) else (n$0 ÷ '2) ≮ cnt (x, a$0, '1, n$0) endif)

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

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

; (FORTRAN-COMMENT LOGICAL-IF-F5)

Axiom: logical-if-f5 t

Axiom: assignment5 (boole$5 = boole$4) ∧ ((cand$5 = cand$4) ∧ ((i$5 = i$4) ∧ (k$5 = '0)))

; (FORTRAN-COMMENT LOGICAL-IF-F6)

Axiom: logical-if-f6 t

Axiom: assignment6 (boole$6 = boole$5) ∧ ((cand$6 = cand$5) ∧ ((i$6 = '1) ∧ (k$6 = k$5)))

; (FORTRAN-COMMENT LOGICAL-IF-T1)

Axiom: logical-if-t1 t

Axiom: effects-of-undefiner1 (boole$7 = boole$6) ∧ ((cand$7 = cand$6) ∧ (k$7 = k$6))

Axiom: assignment7 (boole$8 = '*1*false) ∧ ((cand$8 = cand$7) ∧ ((i$8 = i$7) ∧ (k$8 = k$7)))

Theorem: output (i$6 ∧ (zgreaterp (i$6, n$0)

∧ ((¬ zgreaterp (k$4, zquotient (n$0, '2)))

∧ ((¬ zeqp (k$3, '0))

∧ (i$2 ∧ (zgreaterp (i$2, n$0) ∧ path-hyps))))))

→ (((boole$8 = '*1*true) ∨ (boole$8 = '*1*false))

∧ if boole$8

then znumberp (cand$8)

∧ ((n$0 ÷ '2) < cnt (cand$8, a$0, '1, n$0)) else (n$0 ÷ '2) ≮ cnt (x, a$0, '1, n$0) endif)

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

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

; (FORTRAN-COMMENT LOGICAL-IF-F7)

Axiom: logical-if-f7 t

Theorem: array-bounds-check-for-a1 ((¬ zgreaterp (i$6, n$0)) ∧ ((¬ zgreaterp (k$4, zquotient (n$0, '2)))

∧ ((¬ zeqp (k$3, '0))

∧ (i$2 ∧ (zgreaterp (i$2, n$0) ∧ path-hyps)))))

→ (('0 < i$6) ∧ (n$0 ≮ i$6))

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

Theorem: definedness4 ((¬ zgreaterp (i$6, n$0)) ∧ ((¬ zgreaterp (k$4, zquotient (n$0, '2)))

∧ ((¬ zeqp (k$3, '0))

∧ (i$2 ∧ (zgreaterp (i$2, n$0) ∧ path-hyps)))))

→ znumberp (cand$6)

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

Theorem: definedness5 ((¬ zgreaterp (i$6, n$0)) ∧ ((¬ zgreaterp (k$4, zquotient (n$0, '2)))

∧ ((¬ zeqp (k$3, '0))

∧ (i$2 ∧ (zgreaterp (i$2, n$0) ∧ path-hyps)))))

→ znumberp (elt1 (a$0, i$6))

#| (COMMENT PHASE1-INVRT T F F F F) |#
; (FORTRAN-COMMENT LOGICAL-IF-T1)

Axiom: logical-if-t1 t

Theorem: phase2-invrt (zneqp (cand$6, elt1 (a$0, i$6)) ∧ ((¬ zgreaterp (i$6, n$0))

∧ ((¬ zgreaterp (k$4, zquotient (n$0, '2)))

∧ ((¬ zeqp (k$3, '0))

∧ (i$2 ∧ (zgreaterp (i$2, n$0) ∧ path-hyps))))))

→ (((i$6 ∈ N)

∧ ((i$6 ≠ '0)

∧ ((boole$6 = '*1*true) ∧ ((n$0 ≮ i$6)

∧ (((¬ negativep (cand$6)) → (cand$6 ∈ N)) ∧ ((zneqp (x, cand$6) → (n$0

                                ≮ ('2

∗ cnt (x, a$0,

                                           '1,

n$0))))

∧ ((n$0

                                ≮ ('2

∗ cnt (cand$6, a$0,

                                           '1,

i$6)))

∧ (k$6

= cnt (cand$6, a$0,

                                          '1,

i$6)))))))))

∧ lex (cons ((1 + n$0) − i$6, 'nil), cons (1 + (n$0 + ((1 + n$0) − i$1)), 'nil)))

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

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

; (FORTRAN-COMMENT LOGICAL-IF-F8)

Axiom: logical-if-f8 t

Theorem: input-cond-of-zplus1 ((¬ zneqp (cand$6, elt1 (a$0, i$6))) ∧ ((¬ zgreaterp (i$6, n$0))

∧ ((¬ zgreaterp (k$4, zquotient (n$0, '2)))

∧ ((¬ zeqp (k$3, '0))

∧ (i$2 ∧ (zgreaterp (i$2, n$0) ∧ path-hyps))))))

→ expressible-znumberp (zplus (k$6, '1))

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

Axiom: assignment7 (boole$7 = boole$6) ∧ ((cand$7 = cand$6) ∧ ((i$7 = i$6) ∧ (k$7 = zplus (k$6, '1))))

Theorem: input-cond-of-zquotient1 ((¬ zneqp (cand$6, elt1 (a$0, i$6))) ∧ ((¬ zgreaterp (i$6, n$0))

∧ ((¬ zgreaterp (k$4, zquotient (n$0, '2)))

∧ ((¬ zeqp (k$3, '0))

∧ (i$2 ∧ (zgreaterp (i$2, n$0) ∧ path-hyps))))))

→ ((¬ zeqp ('2, '0)) ∧ expressible-znumberp (zquotient (n$0, '2)))

#| (COMMENT PHASE1-INVRT T F F F F F) |#
; (FORTRAN-COMMENT LOGICAL-IF-T1)

Axiom: logical-if-t1 t

Theorem: output (zgreaterp (k$7, zquotient (n$0, '2)) ∧ ((¬ zneqp (cand$6, elt1 (a$0, i$6)))

∧ ((¬ zgreaterp (i$6, n$0))

∧ ((¬ zgreaterp (k$4, zquotient (n$0, '2)))

∧ ((¬ zeqp (k$3, '0))

∧ (i$2

∧ (zgreaterp (i$2, n$0)

∧ path-hyps)))))))

→ (((boole$7 = '*1*true) ∨ (boole$7 = '*1*false))

∧ if boole$7

then znumberp (cand$7)

∧ ((n$0 ÷ '2) < cnt (cand$7, a$0, '1, n$0)) else (n$0 ÷ '2) ≮ cnt (x, a$0, '1, n$0) endif)

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

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

; (FORTRAN-COMMENT LOGICAL-IF-F9)

Axiom: logical-if-f9 t

Theorem: phase2-invrt ((¬ zgreaterp (k$7, zquotient (n$0, '2))) ∧ ((¬ zneqp (cand$6, elt1 (a$0, i$6)))

∧ ((¬ zgreaterp (i$6, n$0))

∧ ((¬ zgreaterp (k$4, zquotient (n$0, '2)))

∧ ((¬ zeqp (k$3, '0))

∧ (i$2

∧ (zgreaterp (i$2, n$0)

∧ path-hyps)))))))

→ (((i$7 ∈ N)

∧ ((i$7 ≠ '0)

∧ ((boole$7 = '*1*true) ∧ ((n$0 ≮ i$7)

∧ (((¬ negativep (cand$7)) → (cand$7 ∈ N)) ∧ ((zneqp (x, cand$7) → (n$0

                                ≮ ('2

∗ cnt (x,

a$0,

                                           '1,

n$0))))

∧ ((n$0

                                ≮ ('2

∗ cnt (cand$7, a$0,

                                           '1,

i$7)))

∧ (k$7

= cnt (cand$7, a$0,

                                          '1,

i$7)))))))))

∧ lex (cons ((1 + n$0) − i$7, 'nil), cons (1 + (n$0 + ((1 + n$0) − i$1)), 'nil)))

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

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

; (FORTRAN-COMMENT LOGICAL-IF-F4)

Axiom: logical-if-f4 t

Theorem: definedness3 ((¬ zgreaterp (i$2, n$0)) ∧ path-hyps) → znumberp (k$2)

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

Axiom: logical-if-t t

Theorem: array-bounds-check-for-a1 (zeqp (k$2, '0) ∧ ((¬ zgreaterp (i$2, n$0)) ∧ path-hyps)) → (('0 < i$2) ∧ (n$0 ≮ i$2))

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

Theorem: definedness4 (zeqp (k$2, '0) ∧ ((¬ zgreaterp (i$2, n$0)) ∧ path-hyps)) → znumberp (elt1 (a$0, i$2))

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

Axiom: assignment4 (boole$3 = boole$2) ∧ ((cand$3 = elt1 (a$0, i$2)) ∧ ((i$3 = i$2) ∧ (k$3 = k$2)))

Axiom: assignment5 (boole$4 = boole$3) ∧ ((cand$4 = cand$3) ∧ ((i$4 = i$3) ∧ (k$4 = '1)))

Theorem: compound-invrt (k$1 = 0) → (i$1 ≮ (2 ∗ cnt (x, a$0, 1, i$1)))

(PROVE-LEMMA PHASE1-INVRT1 NIL
 (IMPLIES
  (AND (ZEQP (K$2) '0)
       (AND (NOT (ZGREATERP (I$2) (N$0)))
            (PATH-HYPS)))
  (AND
   (AND
    (NUMBERP (I$4))
    (AND
     (NOT (EQUAL (I$4) '0))
     (AND
      (NUMBERP (K$4))
      (AND
       (NOT (LESSP (I$4) (K$4)))
       (AND
        (NOT (LESSP (N$0) (I$4)))
        (AND
         (IMPLIES (NOT (NEGATIVEP (CAND$4)))
                  (NUMBERP (CAND$4)))
         (AND
          (NOT (LESSP (CNT (CAND$4) (A$0) '1 (I$4))
                      (K$4)))

          (AND
           (IMPLIES
                  (ZEQP X (CAND$4))
                  (NOT (LESSP (PLUS (I$4) (K$4))
                              (TIMES '2 (CNT X (A$0) '1 (I$4))))))
           (IMPLIES
            (ZNEQP X (CAND$4))
            (NOT
             (LESSP
                   (I$4)
                   (PLUS (K$4)
                         (TIMES '2
                                (CNT X (A$0) '1 (I$4)))))))))))))))
   (LEX (CONS (ADD1 (PLUS (N$0)
                          (DIFFERENCE (ADD1 (N$0)) (I$4))))
              'NIL)
        (CONS (ADD1 (PLUS (N$0)
                          (DIFFERENCE (ADD1 (N$0)) (I$1))))
              'NIL)))))
#| (COMMENT PHASE1-INVRT F T) |#

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

; (FORTRAN-COMMENT LOGICAL-IF-F5)

Axiom: logical-if-f5 t

Theorem: array-bounds-check-for-a1 ((¬ zeqp (k$2, '0)) ∧ ((¬ zgreaterp (i$2, n$0)) ∧ path-hyps)) → (('0 < i$2) ∧ (n$0 ≮ i$2))

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

Theorem: definedness4 ((¬ zeqp (k$2, '0)) ∧ ((¬ zgreaterp (i$2, n$0)) ∧ path-hyps)) → znumberp (cand$2)

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

Theorem: definedness5 ((¬ zeqp (k$2, '0)) ∧ ((¬ zgreaterp (i$2, n$0)) ∧ path-hyps)) → znumberp (elt1 (a$0, i$2))

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

Axiom: logical-if-t t

Theorem: input-cond-of-zplus1 (zeqp (cand$2, elt1 (a$0, i$2)) ∧ ((¬ zeqp (k$2, '0)) ∧ ((¬ zgreaterp (i$2, n$0)) ∧ path-hyps))) → expressible-znumberp (zplus (k$2, '1))

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

Axiom: assignment4 (boole$3 = boole$2) ∧ ((cand$3 = cand$2) ∧ ((i$3 = i$2) ∧ (k$3 = zplus (k$2, '1))))

(PROVE-LEMMA PHASE1-INVRT1 NIL
 (IMPLIES
  (AND (ZEQP (CAND$2) (ELT1 (A$0) (I$2)))
       (AND (NOT (ZEQP (K$2) '0))
            (AND (NOT (ZGREATERP (I$2) (N$0)))
                 (PATH-HYPS))))
  (AND
   (AND
    (NUMBERP (I$3))
    (AND
     (NOT (EQUAL (I$3) '0))
     (AND
      (NUMBERP (K$3))
      (AND
       (NOT (LESSP (I$3) (K$3)))
       (AND
        (NOT (LESSP (N$0) (I$3)))
        (AND
         (IMPLIES (NOT (NEGATIVEP (CAND$3)))
                  (NUMBERP (CAND$3)))
         (AND
          (NOT (LESSP (CNT (CAND$3) (A$0) '1 (I$3))
                      (K$3)))
          (AND

           (IMPLIES
                  (ZEQP X (CAND$3))
                  (NOT (LESSP (PLUS (I$3) (K$3))
                              (TIMES '2 (CNT X (A$0) '1 (I$3))))))
           (IMPLIES
            (ZNEQP X (CAND$3))
            (NOT
             (LESSP
                   (I$3)
                   (PLUS (K$3)
                         (TIMES '2
                                (CNT X (A$0) '1 (I$3)))))))))))))))
   (LEX (CONS (ADD1 (PLUS (N$0)
                          (DIFFERENCE (ADD1 (N$0)) (I$3))))
              'NIL)
        (CONS (ADD1 (PLUS (N$0)
                          (DIFFERENCE (ADD1 (N$0)) (I$1))))
              'NIL)))))
#| (COMMENT PHASE1-INVRT F F T) |#

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

; (FORTRAN-COMMENT LOGICAL-IF-F6)

Axiom: logical-if-f6 t

Theorem: input-cond-of-zdifference1 ((¬ zeqp (cand$2, elt1 (a$0, i$2))) ∧ ((¬ zeqp (k$2, '0)) ∧ ((¬ zgreaterp (i$2, n$0)) ∧ path-hyps))) → expressible-znumberp (zdifference (k$2, '1))

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

Axiom: assignment4 (boole$3 = boole$2) ∧ ((cand$3 = cand$2)

∧ ((i$3 = i$2) ∧ (k$3 = zdifference (k$2, '1))))

(PROVE-LEMMA PHASE1-INVRT1 NIL

(IMPLIES
(AND (NOT (ZEQP (CAND$2) (ELT1 (A$0) (I$2))))
(AND (NOT (ZEQP (K$2) '0))
     (AND (NOT (ZGREATERP (I$2) (N$0)))
          (PATH-HYPS))))
(AND
(AND
(NUMBERP (I$3))
(AND
(NOT (EQUAL (I$3) '0))
(AND
(NUMBERP (K$3))
(AND
(NOT (LESSP (I$3) (K$3)))
(AND
 (NOT (LESSP (N$0) (I$3)))
 (AND
  (IMPLIES (NOT (NEGATIVEP (CAND$3)))
           (NUMBERP (CAND$3)))
  (AND
   (NOT (LESSP (CNT (CAND$3) (A$0) '1 (I$3))
               (K$3)))
   (AND
    (IMPLIES
           (ZEQP X (CAND$3))
           (NOT (LESSP (PLUS (I$3) (K$3))
                       (TIMES '2 (CNT X (A$0) '1 (I$3))))))
    (IMPLIES
     (ZNEQP X (CAND$3))
     (NOT
      (LESSP
            (I$3)
            (PLUS (K$3)
                  (TIMES '2
                         (CNT X (A$0) '1 (I$3)))))))))))))))
(LEX (CONS (ADD1 (PLUS (N$0)
                   (DIFFERENCE (ADD1 (N$0)) (I$3))))
       'NIL)
 (CONS (ADD1 (PLUS (N$0)
                   (DIFFERENCE (ADD1 (N$0)) (I$1))))
       'NIL)))))
#| (COMMENT PHASE1-INVRT F F F) |#

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

Axiom: paths-from-phase2-invrt (boole$1 = '*1*true) ∧ ((zneqp (x, cand$1) → (n$0 ≮ ('2 ∗ cnt (x, a$0, '1, n$0))))

∧ (k$1 = cnt (cand$1, a$0, '1, i$1)))

Definition: path-hyps = (global-hyps

∧ ((i$1 ∈ N)

∧ ((i$1 ≠ '0)
∧ ((n$0 ≮ i$1)

∧ (((¬ negativep (cand$1)) → (cand$1 ∈ N))

∧ (n$0

                         ≮ ('2

∗ cnt (cand$1, a$0,

                                    '1,

i$1))))))))

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

#| (COMMENT PHASE2-INVRT) |#

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

#| (COMMENT PHASE2-INVRT) |#

Axiom: assignment3 (boole$2 = boole$1) ∧ ((cand$2 = cand$1) ∧ ((i$2 = zplus (i$1, '1)) ∧ (k$2 = k$1)))

; (FORTRAN-COMMENT LOGICAL-IF-T)

Axiom: logical-if-t t

Axiom: effects-of-undefiner (boole$3 = boole$2) ∧ ((cand$3 = cand$2) ∧ (k$3 = k$2))

Axiom: assignment4 (boole$4 = '*1*false) ∧ ((cand$4 = cand$3) ∧ ((i$4 = i$3) ∧ (k$4 = k$3)))

Theorem: zeqp-is-a-congruence-relation-wrt-cnt-arg-1 (znormalize (x) = znormalize (y)) → (cnt (x, a, i, j ) ≮ cnt (y, a, i, j ))

Theorem: phase-2-hint (n$0 ≮ (cnt (cand$1, a$0, 1, n$0) + cnt (cand$1, a$0, 1, n$0))) → (n$0 ≮ (cnt (x, a$0, 1, n$0) + cnt (x, a$0, 1, n$0)))

Theorem: output (i$2 ∧ (zgreaterp (i$2, n$0) ∧ path-hyps)) → (((boole$4 = '*1*true) ∨ (boole$4 = '*1*false))

∧ if boole$4

then znumberp (cand$4)

∧ ((n$0 ÷ '2) < cnt (cand$4, a$0, '1, n$0)) else (n$0 ÷ '2) ≮ cnt (x, a$0, '1, n$0) endif)

#| (COMMENT PHASE2-INVRT T) |#

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

; (FORTRAN-COMMENT LOGICAL-IF-F4)

Axiom: logical-if-f4 t

Theorem: array-bounds-check-for-a1 ((¬ zgreaterp (i$2, n$0)) ∧ path-hyps) → (('0 < i$2) ∧ (n$0 ≮ i$2))

#| (COMMENT PHASE2-INVRT F) |#

Theorem: definedness3 ((¬ zgreaterp (i$2, n$0)) ∧ path-hyps) → znumberp (cand$2)

#| (COMMENT PHASE2-INVRT F) |#

Theorem: definedness4 ((¬ zgreaterp (i$2, n$0)) ∧ path-hyps) → znumberp (elt1 (a$0, i$2))

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

Axiom: logical-if-t t

Theorem: phase2-invrt1 (zneqp (cand$2, elt1 (a$0, i$2)) ∧ ((¬ zgreaterp (i$2, n$0)) ∧ path-hyps)) → (((i$2 ∈ N)

∧ ((i$2 ≠ '0)

∧ ((boole$2 = '*1*true) ∧ ((n$0 ≮ i$2)

∧ (((¬ negativep (cand$2)) → (cand$2 ∈ N)) ∧ ((zneqp (x, cand$2) → (n$0

                                ≮ ('2

∗ cnt (x,

a$0,

                                           '1,

n$0))))

∧ ((n$0

                                ≮ ('2

∗ cnt (cand$2, a$0,

                                           '1,

i$2)))

∧ (k$2

= cnt (cand$2, a$0,

                                          '1,

i$2)))))))))

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

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

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

; (FORTRAN-COMMENT LOGICAL-IF-F5)

Axiom: logical-if-f5 t Theorem: definedness5 ((¬ zneqp (cand$2, elt1 (a$0, i$2))) ∧ ((¬ zgreaterp (i$2, n$0)) ∧ path-hyps)) → znumberp (k$2)

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

Theorem: input-cond-of-zplus1 ((¬ zneqp (cand$2, elt1 (a$0, i$2))) ∧ ((¬ zgreaterp (i$2, n$0)) ∧ path-hyps)) → expressible-znumberp (zplus (k$2, '1))

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

Axiom: assignment4 (boole$3 = boole$2) ∧ ((cand$3 = cand$2) ∧ ((i$3 = i$2) ∧ (k$3 = zplus (k$2, '1))))

Theorem: cnt-grows ((i$1 < n) ∧ zeqp (x, elt1 (a, 1 + i$1))) → (cnt (x, a, 1, i$1) < cnt (x, a, 1, n))

Theorem: input-cond-of-zquotient ((¬ zneqp (cand$2, elt1 (a$0, i$2))) ∧ ((¬ zgreaterp (i$2, n$0)) ∧ path-hyps)) → ((¬ zeqp ('2, '0)) ∧ expressible-znumberp (zquotient (n$0, '2)))

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

Axiom: logical-if-t t

Theorem: output (zgreaterp (k$3, zquotient (n$0, '2)) ∧ ((¬ zneqp (cand$2, elt1 (a$0, i$2)))

∧ ((¬ zgreaterp (i$2, n$0)) ∧ path-hyps))) → (((boole$3 = '*1*true) ∨ (boole$3 = '*1*false))

∧ if boole$3

then znumberp (cand$3)

∧ ((n$0 ÷ '2) < cnt (cand$3, a$0, '1, n$0)) else (n$0 ÷ '2) ≮ cnt (x, a$0, '1, n$0) endif)

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

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

; (FORTRAN-COMMENT LOGICAL-IF-F6)

Axiom: logical-if-f6 t

Theorem: phase2-invrt1 ((¬ zgreaterp (k$3, zquotient (n$0, '2))) ∧ ((¬ zneqp (cand$2, elt1 (a$0, i$2)))

∧ ((¬ zgreaterp (i$2, n$0)) ∧ path-hyps))) → (((i$3 ∈ N)

∧ ((i$3 ≠ '0)

∧ ((boole$3 = '*1*true) ∧ ((n$0 ≮ i$3)

∧ (((¬ negativep (cand$3)) → (cand$3 ∈ N)) ∧ ((zneqp (x, cand$3) → (n$0

                                ≮ ('2

∗ cnt (x,

a$0,

                                           '1,

n$0))))

∧ ((n$0

                                ≮ ('2

∗ cnt (cand$3, a$0,

                                           '1,

i$3)))

∧ (k$3

= cnt (cand$3, a$0,

                                          '1,

i$3)))))))))

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

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

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

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

#|
The correctness of the program depends upon the following events:
@BEGIN(GROUP)
@BEGIN(VERBATIM)
        Definition.
        (CNT X A I N)
           =
        (IF (OR (ZEROP N) (LESSP N I))
            0
            (IF (ZEQP X (ELT1 A N))
                (ADD1 (CNT X A I (SUB1 N)))
                (CNT X A I (SUB1 N))))
@END(VERBATIM)
@END(GROUP)
@BEGIN(GROUP)
@BEGIN(VERBATIM)
        (FORTRAN-COMMENT USEFUL-LEMMAS)
@END(VERBATIM)
@END(GROUP)

Specification for routine MJRTY
The input assertion:
(AND (IMPLIES (AND (LESSP 0 J)
              (NOT (LESSP (N STATE) J))
              (NOT (NEGATIVEP (ELT1 A J))))
         (NUMBERP (ELT1 A J)))
(NUMBERP (N STATE))
(NOT (EQUAL (N STATE) 0))
(LESSP (ADD1 (N STATE))
       (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))

The output assertion:
(AND (OR (EQUAL (BOOLE NEWSTATE) (TRUE))
    (EQUAL (BOOLE NEWSTATE) (FALSE)))
(IF (BOOLE NEWSTATE)
    (AND (ZNUMBERP (CAND NEWSTATE))
         (LESSP (QUOTIENT (N STATE) 2)
                (CNT (CAND NEWSTATE)
                     (A STATE)
                     1
                     (N STATE))))
    (NOT (LESSP (QUOTIENT (N STATE) 2)
                (CNT X (A STATE) 1 (N STATE))))))

END
SUBROUTINE MJRTY(A, N, BOOLE, CAND)
INTEGER N
INTEGER A
LOGICAL BOOLE
INTEGER CAND
INTEGER I
INTEGER K
DIMENSION A(N)
K = 0
C     THE FOLLOWING DO IMPLEMENTS THE PAIRING PHASE. CAND IS THE CURRENT
C     LY LEADING CANDIDATE AND K IS THE NUMBER OF UNPAIRED VOTES FOR CAN
C     D.
DO 100 I = 1, N
C     DOJUNK PHASE1-HINT
IF ((K .EQ. 0)) GOTO 50
IF ((CAND .EQ. A(I))) GOTO 75
K = (K - 1)
GOTO 100
50    CAND = A(I)
K = 1
C     XXX PHASE1-INVRT-F-T
GOTO 100
75    K = (K + 1)
100   CONTINUE
IF ((K .EQ. 0)) GOTO 300
BOOLE = .TRUE.
IF ((K .GT. (N / 2))) RETURN
C     WE NOW ENTER THE COUNTING PHASE. BOOLE IS SET TO TRUE IN ANTICIPAT
C     ION OF FINDING CAND IN THE MAJORITY. K IS USED AS THE RUNNING TALL
C     Y FOR CAND. WE EXIT AS SOON AS K EXCEEDS N/2.
K = 0
DO 200 I = 1, N
C     DOJUNK PHASE2
IF ((CAND .NE. A(I))) GOTO 200
K = (K + 1)
C     XXX OUTPUT-HINT
IF ((K .GT. (N / 2))) RETURN
200   CONTINUE
300   BOOLE = .FALSE.
C     XXX HINT-FOR-PHASE1-INVRT-T-T
C     XXX HINT-FOR-PHASE2-INVRT-T
RETURN

      END

The XXX at USEFUL-LEMMAS.
@BEGIN(GROUP)
@BEGIN(VERBATIM)
        Theorem.  PLUS-1 (rewrite):
        (EQUAL (PLUS 1 X) (ADD1 X))
@END(VERBATIM)
@END(GROUP)
@BEGIN(GROUP)
@BEGIN(VERBATIM)
        Theorem.  DIFFERENCE-0 (rewrite):
        (IMPLIES (NOT (LESSP X Y))
                 (EQUAL (DIFFERENCE Y X) 0))
@END(VERBATIM)
@END(GROUP)
@BEGIN(GROUP)
@BEGIN(VERBATIM)
        Theorem.  DIFFERENCE-1 (rewrite):
        (EQUAL (DIFFERENCE X 1) (SUB1 X))
@END(VERBATIM)
@END(GROUP)
@BEGIN(GROUP)
@BEGIN(VERBATIM)
        Theorem.  LESSP-X-1 (rewrite):
        (EQUAL (LESSP X 1) (ZEROP X))
@END(VERBATIM)
@END(GROUP)
@BEGIN(GROUP)
@BEGIN(VERBATIM)
        Theorem.  LESSP-REMAINDER2 (rewrite and generalize):
        (EQUAL (LESSP (REMAINDER X Y) Y)
               (NOT (ZEROP Y)))
@END(VERBATIM)
@END(GROUP)
@BEGIN(GROUP)
@BEGIN(VERBATIM)
        Theorem.  REMAINDER-QUOTIENT-ELIM (elimination):

        (IMPLIES (AND (NOT (ZEROP Y)) (NUMBERP X))
                 (EQUAL (PLUS (REMAINDER X Y)
                              (TIMES Y (QUOTIENT X Y)))
                        X))
@END(VERBATIM)
@END(GROUP)
@BEGIN(GROUP)
@BEGIN(VERBATIM)
        Theorem.  QUOTIENT-BY-2-BOUND (rewrite):
        (NOT (LESSP X (QUOTIENT X 2)))
@END(VERBATIM)
@END(GROUP)
@BEGIN(GROUP)
@BEGIN(VERBATIM)
        Theorem.  LESSP-QUOTIENT-REWRITE (rewrite):
        (EQUAL (LESSP (QUOTIENT N 2) M)
               (LESSP N (PLUS M M)))
@END(VERBATIM)
@END(GROUP)
@BEGIN(GROUP)
@BEGIN(VERBATIM)
        Theorem.  ZNORMALIZE-ZERO (rewrite):
        (IMPLIES (NUMBERP X)
                 (EQUAL (EQUAL (ZNORMALIZE X) 0)
                        (EQUAL X 0)))
@END(VERBATIM)
@END(GROUP)
@BEGIN(GROUP)
@BEGIN(VERBATIM)
        Enable ZNORMALIZE.
@END(VERBATIM)
@END(GROUP)
@BEGIN(GROUP)
@BEGIN(VERBATIM)
        Theorem.  CNT-BOUND (rewrite):
        (NOT (LESSP N (CNT X A 1 N)))
@END(VERBATIM)
@END(GROUP)

40

Hints for routine MJRTY

The input clock:
(LIST (ADD1 (ADD1 (PLUS (N (START)) (N (START))))))
The DO junk named PHASE1-HINT:
((BUMP PHASE1-INVRT))
The invariant and clock named PHASE1-INVRT.
(AND
(NUMBERP (I STATE))
(NOT (EQUAL (I STATE) 0))
(NUMBERP (K STATE))
(NOT (LESSP (I STATE) (K STATE)))
(NOT (LESSP (N (START)) (I STATE)))
(IMPLIES (NOT (NEGATIVEP (CAND STATE)))
         (NUMBERP (CAND STATE)))
(NOT (LESSP (CNT (CAND STATE)
                 (A STATE)
                 1
                 (I STATE))
            (K STATE)))
(IMPLIES
       (ZEQP X (CAND STATE))
       (NOT (LESSP (PLUS (I STATE) (K STATE))
                   (TIMES 2
                          (CNT X (A STATE) 1 (I STATE))))))
(IMPLIES
 (ZNEQP X (CAND STATE))
 (NOT
    (LESSP (I STATE)
           (PLUS (K STATE)
                 (TIMES 2
                        (CNT X (A STATE) 1 (I STATE))))))))
(LIST (ADD1 (PLUS (N (START))
                 (DIFFERENCE (ADD1 (N (START)))
                             (I STATE)))))
The XXX named PHASE1-INVRT-F-T:

Path encryption:
((PHASE1-INVRT F T))
@BEGIN(GROUP)
@BEGIN(VERBATIM)
Theorem.  COMPOUND-INVRT (rewrite):
(IMPLIES (EQUAL (K$1) 0)
        (NOT (LESSP (I$1)
                    (TIMES 2 (CNT X (A$0) 1 (I$1))))))
Hints:  Consider:
        PATHS-FROM-PHASE1-INVRT
       Enable  PATHS-FROM-PHASE1-INVRT
@END(VERBATIM)
@END(GROUP)

The DO junk named PHASE2:
((BUMP PHASE2-INVRT))
The invariant and clock named PHASE2-INVRT.
(AND
(NUMBERP (I STATE))
(NOT (EQUAL (I STATE) 0))
(EQUAL (BOOLE STATE) (TRUE))
(NOT (LESSP (N (START)) (I STATE)))
(IMPLIES (NOT (NEGATIVEP (CAND STATE)))
         (NUMBERP (CAND STATE)))
(IMPLIES
     (ZNEQP X (CAND STATE))
     (NOT (LESSP (N (START))
                 (TIMES 2
                        (CNT X (A STATE) 1 (N (START)))))))
(NOT (LESSP (N (START))
            (TIMES 2
                   (CNT (CAND STATE)
                        (A STATE)
                        1
                        (I STATE)))))
(EQUAL (K STATE)
       (CNT (CAND STATE)
            (A STATE)
            1
            (I STATE))))

(LIST (DIFFERENCE (ADD1 (N (START)))
                  (I STATE)))
The XXX named OUTPUT-HINT:
Path encryption:
((PHASE2-INVRT F F))
@BEGIN(GROUP)
@BEGIN(VERBATIM)
Theorem.  CNT-GROWS (rewrite):
(IMPLIES (AND (LESSP (I$1) N)
              (ZEQP X (ELT1 A (ADD1 (I$1)))))
         (LESSP (CNT X A 1 (I$1))
                (CNT X A 1 N)))
Hint:  Induct as for (PLUS N I).
@END(VERBATIM)
@END(GROUP)

The XXX named HINT-FOR-PHASE1-INVRT-T-T:
Path encryption:
((PHASE1-INVRT T T))
@BEGIN(GROUP)
@BEGIN(VERBATIM)
Theorem.  COMPOUND-INVRT (rewrite):
(IMPLIES (EQUAL (K$1) 0)
         (NOT (LESSP (I$1)
                     (TIMES 2 (CNT X (A$0) 1 (I$1))))))
Hints:  Consider:
         PATHS-FROM-PHASE1-INVRT
        Enable PATHS-FROM-PHASE1-INVRT
@END(VERBATIM)
@END(GROUP)

The XXX named HINT-FOR-PHASE2-INVRT-T:
Path encryption:
((PHASE2-INVRT T))
@BEGIN(GROUP)
@BEGIN(VERBATIM)
Theorem.  ZEQP-IS-A-CONGRUENCE-RELATION-WRT-CNT-ARG-1 (rewrite):
(IMPLIES (EQUAL (ZNORMALIZE X) (ZNORMALIZE Y))

                 (NOT (LESSP (CNT X A I J) (CNT Y A I J))))
@END(VERBATIM)
@END(GROUP)
@BEGIN(GROUP)
@BEGIN(VERBATIM)
        Theorem.  PHASE-2-HINT (rewrite):
        (IMPLIES (NOT (LESSP (N$0)
                             (PLUS (CNT (CAND$1) (A$0) 1 (N$0))
                                   (CNT (CAND$1) (A$0) 1 (N$0)))))
                 (NOT (LESSP (N$0)
                             (PLUS (CNT X (A$0) 1 (N$0))
                                   (CNT X (A$0) 1 (N$0))))))
        Hints:  Consider:
                 PATHS-FROM-PHASE2-INVRT
                Enable PATHS-FROM-PHASE2-INVRT
@END(VERBATIM)
@END(GROUP)
|#

Index

a$0, 2, 5–12, 14, 15, 17–28, 30–34 array-bounds-check-for-a, 8, 12, 13 array-bounds-check-for-a1, 20, 24, 26,

31 assignment, 5 assignment1, 5 assignment2, 5, 6, 12, 14, 16 assignment3, 7, 12, 18, 30 assignment4, 7, 18, 19, 25, 27, 28,

31, 33 assignment5, 7, 10, 19, 25 assignment6, 19 assignment7, 20, 22

boole$0, 2, 5 boole$1, 2, 5, 18, 30 boole$2, 2, 5, 12, 14, 16, 18, 25, 27,

28, 30, 32, 33 boole$3, 2, 5, 12, 14, 16, 18, 25, 27,

28, 30, 33, 34 boole$4, 2, 5–7, 12, 18, 19, 25, 31 boole$5, 2, 7, 19 boole$6, 2, 7, 9, 10, 19–22 boole$7, 2, 7, 10, 11, 20, 22, 23 boole$8, 2, 7, 20

cand$0, 2, 5 cand$1, 2, 5, 17, 18, 30, 31 cand$2, 2, 5, 14–16, 18, 26–28, 30–

34 cand$3, 2, 5, 6, 12, 14, 16, 18, 19,

25, 27, 28, 30, 31, 33, 34 cand$4, 2, 5–7, 12, 18, 19, 25, 31 cand$5, 2, 7, 19 cand$6, 2, 7–11, 19–23 cand$7, 2, 7, 10, 11, 20, 22–24 cand$8, 3, 7, 20 cnt, 4–7, 9–11, 17–25, 30–34 cnt-bound, 5 cnt-grows, 33 compound-invrt, 18, 25 definedness, 8, 12, 14 definedness1, 8, 14 definedness2, 17, 30 definedness3, 18, 24, 31 definedness4, 21, 25, 26, 31 definedness5, 21, 26, 33 difference-0, 4 difference-1, 4

effects-of-undefiner, 5, 18, 30 effects-of-undefiner1, 7, 20 elt1, 4, 8–12, 14, 15, 21–23, 25–28,

31–34 expressible-znumberp, 6, 9, 10, 14,

15, 17, 19, 22, 27, 28, 30, 33

fortran, 1

global-hyps, 4–15, 17, 30

i$0, 3, 5

i$1, 3, 5, 17, 18, 22, 24, 25, 30, 32–

34 i$2, 3, 5–16, 18–28, 30–34 i$3, 3, 5, 6, 12, 14, 16, 18, 19, 25, 27, 28, 31, 33, 34

i$4, 3, 5–7, 12, 18, 19, 25, 31

i$5, 3, 7, 19

i$6, 3, 7–11, 19–23

i$7, 3, 7, 10, 11, 20, 22–24

i$8, 3, 7, 20 input, 5 input-cond-of-zdifference, 15 input-cond-of-zdifference1, 28 input-cond-of-zplus, 9, 14, 17, 30 input-cond-of-zplus1, 22, 27, 33 input-cond-of-zquotient, 6, 19, 33 input-cond-of-zquotient1, 10, 22 input-conditions, 4 input-definedness, 5 k$1, 3, 5, 17, 18, 25, 30 k$2, 3, 5, 12–16, 18, 24–28, 30, 32,

33 k$3, 3, 5–12, 14, 16, 18–23, 25, 27,

28, 30, 31, 33, 34 k$4, 3, 5–12, 18–23, 25, 31 k$5, 3, 7, 19 k$6, 3, 7, 9, 10, 19, 20, 22 k$7, 3, 7, 10, 11, 20, 22–24 k$8, 3, 7, 20

least-inexpressible-positive-inte

ger, 4 lessp-quotient-rewrite, 4 lessp-remainder2, 4 lessp-x-1, 4 lex, 9, 11, 22, 24, 32, 34 logical-if-f, 5 logical-if-f1, 6, 12 logical-if-f2, 6, 13 logical-if-f3, 7, 15 logical-if-f4, 8, 18, 24, 31 logical-if-f5, 9, 19, 26, 32 logical-if-f6, 11, 19, 28, 34 logical-if-f7, 20 logical-if-f8, 22 logical-if-f9, 23 logical-if-t, 5, 12, 14, 18, 24, 27, 30,

32, 33 logical-if-t1, 5–8, 10, 18–21, 23

n$0, 4–15, 17–28, 30–34

output, 5–7, 10, 18–20, 23, 31, 33

path-hyps, 17–28, 30–34 paths-from-phase1-invrt, 17 paths-from-phase2-invrt, 30 phase-2-hint, 31 phase2-invrt, 8, 11, 21, 23 phase2-invrt1, 32, 34 plus-1, 4

quotient-by-2-bound, 4 remainder-quotient-elim, 4

zdifference, 15, 16, 28 zeqp, 4–15, 17–28, 33 zeqp-is-a-congruence-relation-w

rt-cnt-arg-1, 31 zgreaterp, 5–15, 18–28, 31–34 zneqp, 8–11, 17, 21–24, 30, 32–34 znormalize, 4, 31 znormalize-zero, 4 znumberp, 5–8, 10, 12, 14, 17–21, 23–26, 30, 31, 33 zplus, 9, 10, 14, 17, 18, 22, 27, 30,

33 zquotient, 6–11, 19–23, 33, 34