#|
Copyright (C) 1994 by 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
J Strother Moore PROVIDES 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 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.

Event: For efficiency, compile those definitions not yet compiled.

Event: Add the shell zn, with recognizer function symbol znp and 2 accessors: pos, with type restriction (one-of numberp) and default value zero; neg, with type restriction (one-of numberp) and default value zero.

Definition: zlessp (x, y) = ((pos (x) + neg (y)) < (neg (x) + pos (y)))

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

Definition: zmax (x, y) = if zlessp (x, y) then y

else x endif Definition: zmin (x, y) = if zlessp (x, y) then x

else y endif

Definition: zsub1 (x) = zn (pos (x), 1 + neg (x))

Definition: pzdifference (x, y) = ((pos (x) + neg (y)) − (neg (x) + pos (y)))

Definition: m1 (x, y, z) = if zlesseqp (x, y) then 0

else 1 endif

Definition: m2 (x, y, z) = pzdifference (zmax (x, zmax (y, z)), zmin (x, zmin (y, z)))

Definition: m3 (x, y, z) = pzdifference (x, zmin (x, zmin (y, z)))

Definition: tak0 (x, y, z) = if zlesseqp (x, y) then y

elseif zlesseqp (y, z) then z else x endif

Definition: m (x, y, z) = cons (m1 (x, y, z), cons (m2 (x, y, z), cons (m3 (x, y, z), nil)))

Theorem: tak0-satisfies-tak-equation tak0 (x, y, z) = if zlesseqp (x, y) then y

else tak0 (tak0 (zsub1 (x), y, z), tak0 (zsub1 (y), z, x), tak0 (zsub1 (z), x, y)) endif

Theorem: m1-lesseqp-0 (¬ zlesseqp (x, y)) → (m1 (x, y, z)

≮ m1 (tak0 (zsub1 (x), y, z), tak0 (zsub1 (y), z, x), tak0 (zsub1 (z), x, y)))

Theorem: m1-lesseqp-1 (¬ zlesseqp (x, y)) → (m1 (x, y, z) ≮ m1 (zsub1 (x), y, z))

Theorem: m1-lesseqp-2 (¬ zlesseqp (x, y)) → (m1 (x, y, z) ≮ m1 (zsub1 (y), z, x))

Theorem: m1-lesseqp-3 (¬ zlesseqp (x, y)) → (m1 (x, y, z) ≮ m1 (zsub1 (z), x, y))

Theorem: m2-lesseqp-0 (¬ zlesseqp (x, y)) → (m2 (x, y, z)

≮ m2 (tak0 (zsub1 (x), y, z), tak0 (zsub1 (y), z, x), tak0 (zsub1 (z), x, y)))

Theorem: m2-lesseqp-1 (¬ zlesseqp (x, y)) → (m2 (x, y, z) ≮ m2 (zsub1 (x), y, z))

Theorem: m2-lesseqp-2 ((¬ zlesseqp (x, y)) ∧ (m1 (zsub1 (y), z, x) = m1 (x, y, z))) → (m2 (x, y, z) ≮ m2 (zsub1 (y), z, x))

Theorem: m2-lesseqp-3 ((¬ zlesseqp (x, y)) ∧ (m1 (zsub1 (z), x, y) = m1 (x, y, z))) → (m2 (x, y, z) ≮ m2 (zsub1 (z), x, y))

Theorem: m3-lessp-0 ((¬ zlesseqp (x, y)) ∧ (m1 (tak0 (zsub1 (x), y, z), tak0 (zsub1 (y), z, x), tak0 (zsub1 (z), x, y))

= m1 (x, y, z))) → (m3 (tak0 (zsub1 (x), y, z), tak0 (zsub1 (y), z, x), tak0 (zsub1 (z), x, y))

< m3 (x, y, z))

Theorem: m3-lessp-1 ((¬ zlesseqp (x, y)) ∧ (m1 (zsub1 (x), y, z) = m1 (x, y, z))) → (m3 (zsub1 (x), y, z) < m3 (x, y, z))

Theorem: m3-lessp-2 ((¬ zlesseqp (x, y)) ∧ (m1 (zsub1 (y), z, x) = m1 (x, y, z))) → (m3 (zsub1 (y), z, x) < m3 (x, y, z))

Theorem: m3-lessp-3 ((¬ zlesseqp (x, y)) ∧ (m1 (zsub1 (z), x, y) = m1 (x, y, z))) → (m2 (zsub1 (z), x, y) < m2 (x, y, z))

Event: Disable zlessp.

Event: Disable m1.

Event: Disable m2.

Event: Disable m3.

Event: Disable tak0.

Event: Disable zsub1.

Definition: make-ordinal3 (x) = cons (cons (1 + car (x), 0), cons (1 + cadr (x), fix (caddr (x))))

Theorem: ordinalp-make-ordinal3 ordinalp (make-ordinal3 (x))

Definition: lex3 (x, y) = ord-lessp (make-ordinal3 (x), make-ordinal3 (y))

Theorem: m-goes-down-1 (¬ zlesseqp (x, y)) → lex3 (m (zsub1 (x), y, z), m (x, y, z))

Theorem: m-goes-down-2 (¬ zlesseqp (x, y)) → lex3 (m (zsub1 (y), z, x), m (x, y, z))

Theorem: m-goes-down-3 (¬ zlesseqp (x, y)) → lex3 (m (zsub1 (z), x, y), m (x, y, z))

Theorem: m-goes-down-0 (¬ zlesseqp (x, y)) → lex3 (m (tak0 (zsub1 (x), y, z), tak0 (zsub1 (y), z, x), tak0 (zsub1 (z), x, y)),

m (x, y, z))

Index

lex3, 4

m, 2, 4 m-goes-down-0, 4 m-goes-down-1, 4 m-goes-down-2, 4 m-goes-down-3, 4 m1, 2, 3 m1-lesseqp-0, 2 m1-lesseqp-1, 2 m1-lesseqp-2, 2 m1-lesseqp-3, 3 m2, 2, 3 m2-lesseqp-0, 3 m2-lesseqp-1, 3 m2-lesseqp-2, 3 m2-lesseqp-3, 3 m3, 2, 3 m3-lessp-0, 3 m3-lessp-1, 3 m3-lessp-2, 3 m3-lessp-3, 3 make-ordinal3, 4

neg, 1, 2

ordinalp-make-ordinal3, 4

pos, 1, 2 pzdifference, 2

tak0, 2–4 tak0-satisfies-tak-equation, 2

zlesseqp, 1–4 zlessp, 1, 2 zmax, 1, 2 zmin, 2 zn, 1, 2 zsub1, 2–4