#|
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.
|#

Event: Start with the initial nqthm theory.

Definition: logicalp (x) = ((x = true) ∨ (x = false))

Definition: expt (i, j ) = if j ≃ 0 then 1

else i ∗ expt (i, j − 1) endif

Definition: znumberp (x) = (negativep (x) ∨ (x ∈ N))

Definition: zzero = zero

Definition: zplus (x, y) = if negativep (x) then if negativep (y) then − (negative-guts (x) + negative-guts (y))

elseif y < negative-guts (x) then − (negative-guts (x) − y) else y − negative-guts (x) endif

elseif negativep (y) then if x < negative-guts (y) then − (negative-guts (y) − x)

else x − negative-guts (y) endif else x + y endif

Definition: zdifference (x, y) = if negativep (x)

then if negativep (y)

then if negative-guts (y) < negative-guts (x)

then − (negative-guts (x) − negative-guts (y)) else negative-guts (y) − negative-guts (x) endif

else − (negative-guts (x) + y) endif elseif negativep (y) then x + negative-guts (y) elseif x < y then − (y − x) else x − y endif

Definition: ztimes (x, y) = if negativep (x)

then if negativep (y) then negative-guts (x) ∗ negative-guts (y)

else − (negative-guts (x) ∗ y) endif elseif negativep (y) then − (x ∗ negative-guts (y)) else x ∗ y endif

Definition: zquotient (x, y) = if negativep (x)

then if negativep (y) then negative-guts (x) ÷ negative-guts (y)

else − (negative-guts (x) ÷ y) endif elseif negativep (y) then − (x ÷ negative-guts (y)) else x ÷ y endif

Definition: zexptz (i, j ) = if j ≃ 0 then 1

else ztimes (i, zexptz (i, j − 1)) endif

Definition: znormalize (x) = if negativep (x)

then if negative-guts (x) = 0 then 0

else x endif else fix (x) endif

Definition: zeqp (x, y) = (znormalize (x) = znormalize (y))

Definition: zneqp (x, y) = (¬ zeqp (x, y))

Definition: zlessp (x, y) = if negativep (x)

then if negativep (y) then negative-guts (y) < negative-guts (x) else ¬ ((negative-guts (x) = 0) ∧ (y ≃ 0)) endif

elseif negativep (y) then f

else x < y endif

Definition: zlesseqp (x, y) = (¬ zlessp (y, x))

Definition: zgreaterp (x, y) = zlessp (y, x)

Definition: zgreatereqp (x, y) = (¬ zlessp (x, y))

Conservative Axiom: integer-size (least-inexpressible-positive-integer ∈ N) ∧ negativep (greatest-inexpressible-negative-integer) ∧ (200 < negative-guts (greatest-inexpressible-negative-integer)) ∧ (200 < least-inexpressible-positive-integer)

Simultaneously, we introduce the new function symbols greatest-inexpressible-negative-integer and least-inexpressible-positive-integer.

Definition: expressible-znumberp (x) = (zlessp (greatest-inexpressible-negative-integer, x)

∧ zlessp (x, least-inexpressible-positive-integer))

Definition: iabs (i) = if negativep (i) then negative-guts (i)

else fix (i) endif

Definition: mod (x, y) = zdifference (x, ztimes (y, zquotient (x, y)))

Definition: max0 (i, j ) = if zlessp (i, j ) then j

else i endif Definition: min0 (i, j ) = if zlessp (i, j ) then i

else j endif

Definition: isign (i, j ) = if negativep (j ) then ztimes (-1, iabs (i))

else iabs (i) endif

Definition: idim (i, j ) = zdifference (i, min0 (i, j ))

;;; In the old FORTRAN xxx we used UNDEF for all occurrences of the
;;; substring FORTRAN-UNDEF below.  However, in the quantifier version
;;; of the logic, UNDEF is a function name set up in the bootstrap.
;;; To avoid conflict we have changed the name here.  However, it is
;;; possible that vcs mention UNDEF -- not just the function DEFINEDP
;;; which is still around here.  If so, the vcg will have be to be
;;; changed should we decide to support it.

Event: Add the shell fortran-undef , with recognizer function symbol fortranundefined and 1 accessor: fortran-undef-guts, with type restriction (none-of) and default value zero.

Definition: definedp (x) = (¬ fortran-undefined (x))

Event: Introduce the function symbol elt1 of 2 arguments.

Event: Introduce the function symbol elt2 of 3 arguments.

Event: Introduce the function symbol elt3 of 4 arguments.

Definition: lex (l1 , l2 ) = if (l1 ≃ nil) ∨ (l2 ≃ nil) then f

else (car (l1 ) < car (l2 )) ∨ ((car (l1 ) = car (l2 )) ∧ lex (cdr (l1 ), cdr (l2 ))) endif

Event: Introduce the function symbol rnumberp of one argument.

Event: Introduce the function symbol dnumberp of one argument.

Event: Introduce the function symbol cnumberp of one argument. Event: Introduce the function symbol rzero of 0 arguments. Event: Introduce the function symbol dzero of 0 arguments. Event: Introduce the function symbol czero of 0 arguments. Event: Introduce the function symbol expressible-rnumberp of one argument. Event: Introduce the function symbol expressible-dnumberp of one argument. Event: Introduce the function symbol expressible-cnumberp of one argument. Event: Introduce the function symbol rplus of 2 arguments. Event: Introduce the function symbol rtimes of 2 arguments. Event: Introduce the function symbol rdifference of 2 arguments. Event: Introduce the function symbol rquotient of 2 arguments. Event: Introduce the function symbol rlessp of 2 arguments. Event: Introduce the function symbol rlesseqp of 2 arguments. Event: Introduce the function symbol reqp of 2 arguments. Event: Introduce the function symbol rneqp of 2 arguments. Event: Introduce the function symbol rgreatereqp of 2 arguments. Event: Introduce the function symbol rgreaterp of 2 arguments. Event: Introduce the function symbol dplus of 2 arguments.

Event: Introduce the function symbol dtimes of 2 arguments. Event: Introduce the function symbol ddifference of 2 arguments. Event: Introduce the function symbol dquotient of 2 arguments. Event: Introduce the function symbol dlessp of 2 arguments. Event: Introduce the function symbol dlesseqp of 2 arguments. Event: Introduce the function symbol deqp of 2 arguments. Event: Introduce the function symbol dneqp of 2 arguments. Event: Introduce the function symbol dgreatereqp of 2 arguments. Event: Introduce the function symbol dgreaterp of 2 arguments. Event: Introduce the function symbol cplus of 2 arguments. Event: Introduce the function symbol ctimes of 2 arguments. Event: Introduce the function symbol cdifference of 2 arguments. Event: Introduce the function symbol cquotient of 2 arguments. Event: Introduce the function symbol ceqp of 2 arguments. Event: Introduce the function symbol cneqp of 2 arguments. Event: Introduce the function symbol rexptz of 2 arguments. Event: Introduce the function symbol dexptz of 2 arguments. Event: Introduce the function symbol cexptz of 2 arguments.

Event: Introduce the function symbol rexptr of 2 arguments. Event: Introduce the function symbol rexptd of 2 arguments. Event: Introduce the function symbol dexptr of 2 arguments. Event: Introduce the function symbol dexptd of 2 arguments. Event: Introduce the function symbol abs of one argument. Event: Introduce the function symbol dabs of one argument. Event: Introduce the function symbol aint of one argument. Event: Introduce the function symbol int of one argument. Event: Introduce the function symbol idint of one argument. Event: Introduce the function symbol amod of 2 arguments. Event: Introduce the function symbol amax0 of 2 arguments. Event: Introduce the function symbol amax1 of 2 arguments. Event: Introduce the function symbol max1 of 2 arguments. Event: Introduce the function symbol dmax1 of 2 arguments. Event: Introduce the function symbol amin0 of 2 arguments. Event: Introduce the function symbol amin1 of 2 arguments. Event: Introduce the function symbol min1 of 2 arguments. Event: Introduce the function symbol dmin1 of 2 arguments.

Event: Introduce the function symbol float of one argument. Event: Introduce the function symbol ifix of one argument. Event: Introduce the function symbol sign of 2 arguments. Event: Introduce the function symbol dsign of 2 arguments. Event: Introduce the function symbol dim of 2 arguments. Event: Introduce the function symbol sngl of one argument. Event: Introduce the function symbol real of one argument. Event: Introduce the function symbol aimag of one argument. Event: Introduce the function symbol dble of one argument. Event: Introduce the function symbol cmplx of 2 arguments. Event: Introduce the function symbol conjg of one argument. Event: Introduce the function symbol exp of one argument. Event: Introduce the function symbol dexp of one argument. Event: Introduce the function symbol cexp of one argument. Event: Introduce the function symbol alog of one argument. Event: Introduce the function symbol dlog of one argument. Event: Introduce the function symbol clog of one argument. Event: Introduce the function symbol alog10 of one argument.

Event: Introduce the function symbol dlog10 of one argument. Event: Introduce the function symbol sin of one argument. Event: Introduce the function symbol dsin of one argument. Event: Introduce the function symbol csin of one argument. Event: Introduce the function symbol cos of one argument. Event: Introduce the function symbol dcos of one argument. Event: Introduce the function symbol ccos of one argument. Event: Introduce the function symbol tanh of one argument. Event: Introduce the function symbol sqrt of one argument. Event: Introduce the function symbol dsqrt of one argument. Event: Introduce the function symbol csqrt of one argument. Event: Introduce the function symbol atan of one argument. Event: Introduce the function symbol datan of one argument. Event: Introduce the function symbol atan2 of 2 arguments. Event: Introduce the function symbol datan2 of 2 arguments. Event: Introduce the function symbol dmod of 2 arguments. Event: Introduce the function symbol cabs of one argument. Definition: almost-equal1 (a1 , a2 , u, v, i, e) = if (v ≃ 0) ∨ (v < u) then t

else if v = i then elt1 (a2 , v) = e else elt1 (a2 , v) = elt1 (a1 , v) endif ∧ almost-equal1 (a1 , a2 , u, v − 1, i, e) endif

Theorem: plus-0 (x + 0) = fix (x)

Theorem: plus-non-numberp (y ∉ N) → ((x + y) = fix (x))

Theorem: plus-add1 (x + (1 + y)) = if y ∈ N then 1 + (x + y)

else 1 + x endif

Theorem: commutativity2-of-plus (x + (y + z)) = (y + (x + z))

Theorem: commutativity-of-plus (x + y) = (y + x)

Theorem: associativity-of-plus ((x + y) + z) = (x + (y + z))

Theorem: times-0 (x ∗ 0) = 0

Theorem: times-non-numberp (y ∉ N) → ((x ∗ y) = 0)

Theorem: distributivity-of-times-over-plus (x ∗ (y + z)) = ((x ∗ y) + (x ∗ z))

Theorem: times-add1 (x ∗ (1 + y)) = if y ∈ N then x + (x ∗ y)

else fix (x) endif

Theorem: commutativity2-of-times (x ∗ (y ∗ z)) = (y ∗ (x ∗ z))

Theorem: commutativity-of-times (x ∗ y) = (y ∗ x)

Theorem: associativity-of-times ((x ∗ y) ∗ z) = (x ∗ (y ∗ z))

Theorem: equal-times-0 ((x ∗ y) = 0) = ((x ≃ 0) ∨ (y ≃ 0))

Theorem: equal-lessp ((x < y) = z) = if x < y then t = z

else f = z endif

Theorem: almost-equal1-in-range ((elt1 (a2 , j ) ≠ w) ∧ (w = if j = i then e

else elt1 (a1 , j ) endif)

∧ (u ≄ 0) ∧ (j ≮ u) ∧ (v ≮ j )) → (¬ almost-equal1 (a1 , a2 , u, v, i, e))

Theorem: almost-equal1-in-range-opened-up ((elt1 (a2 , j ) ≠ w) ∧ (w = if j = i then e

else elt1 (a1 , j ) endif)

∧ (u ≄ 0) ∧ (u ≤ j ) ∧ (j ≤ v) ∧ (v ≄ 0) ∧ (v ≮ u) ∧ (v ≠ i) ∧ (elt1 (a2 , v) = elt1 (a1 , v))) → (¬ almost-equal1 (a1 , a2 , u, v − 1, i, e))

Theorem: almost-equal1-contracts (almost-equal1 (a1 , a2 , u, v, i, e) ∧ (u ≄ 0) ∧ (x ≮ u) ∧ (v ≮ y)) → almost-equal1 (a1 , a2 , x, y, i, e)

Event: Make the library "fortran" and compile it.

Index

abs, 7 aimag, 8 aint, 7 almost-equal1, 9–11 almost-equal1-contracts, 11 almost-equal1-in-range, 11 almost-equal1-in-range-opened-up, 11 alog, 8 alog10, 8 amax0, 7 amax1, 7 amin0, 7 amin1, 7 amod, 7 associativity-of-plus, 10 associativity-of-times, 11 atan, 9 atan2, 9

cabs, 9 ccos, 9 cdifference, 6 ceqp, 6 cexp, 8 cexptz, 6 clog, 8 cmplx, 8 cneqp, 6 cnumberp, 5 commutativity-of-plus, 10 commutativity-of-times, 10 commutativity2-of-plus, 10 commutativity2-of-times, 10 conjg, 8 cos, 9 cplus, 6 cquotient, 6 csin, 9 csqrt, 9 ctimes, 6 czero, 5 dabs, 7 datan, 9 datan2, 9 dble, 8 dcos, 9 ddifference, 6 definedp, 4 deqp, 6 dexp, 8 dexptd, 7 dexptr, 7 dexptz, 6 dgreatereqp, 6 dgreaterp, 6 dim, 8 distributivity-of-times-over-pl

us, 10 dlesseqp, 6 dlessp, 6 dlog, 8 dlog10, 9 dmax1, 7 dmin1, 7 dmod, 9 dneqp, 6 dnumberp, 4 dplus, 5 dquotient, 6 dsign, 8 dsin, 9 dsqrt, 9 dtimes, 6 dzero, 5

elt1, 4, 10, 11

elt2, 4 elt3, 4 equal-lessp, 11 equal-times-0, 11 exp, 8 expressible-cnumberp, 5 expressible-dnumberp, 5 expressible-rnumberp, 5 expressible-znumberp, 3 expt, 1

float, 8 fortran-undef, 4 fortran-undefined, 4

greatest-inexpressible-negative -integer, 3

iabs, 3, 4 idim, 4 idint, 7 ifix, 8 int, 7 integer-size, 3 isign, 4

least-inexpressible-positive-inte

ger, 3 lex, 4 logicalp, 1

max0, 3 max1, 7 min0, 4 min1, 7 mod, 3

plus-0, 10 plus-add1, 10 plus-non-numberp, 10

rdifference, 5 real, 8 reqp, 5 rexptd, 7 rexptr, 7 rexptz, 6 rgreatereqp, 5 rgreaterp, 5 rlesseqp, 5 rlessp, 5 rneqp, 5 rnumberp, 4 rplus, 5 rquotient, 5 rtimes, 5 rzero, 5

sign, 8 sin, 9 sngl, 8 sqrt, 9

tanh, 9 times-0, 10 times-add1, 10 times-non-numberp, 10

zdifference, 2–4

zeqp, 3 zexptz, 2 zgreatereqp, 3 zgreaterp, 3 zlesseqp, 3 zlessp, 3, 4 zneqp, 3 znormalize, 2, 3 znumberp, 1 zplus, 1 zquotient, 2, 3 ztimes, 2–4 zzero, 1