#|
Copyright (C) 1994 by Robert S. Boyer.  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 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 Robert S. Boyer 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.

;   The floor of the square root. This definition is taken from Goodstein.

Definition: rt (x) = if x ≃ 0 then 0

elseif ((1 + rt (x − 1)) ∗ (1 + rt (x − 1))) = x then 1 + rt (x − 1)

else rt (x − 1) endif

Theorem: times-add1 (x ∗ (1 + y)) = (x + (x ∗ y))

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

Theorem: square-0 ((x ∗ x) = 0) = (x ≃ 0) Theorem: square-monotonic (b ≮ a) → ((b ∗ b) ≮ (a ∗ a)) Theorem: spec-for-rt (y ≮ (rt (y) ∗ rt (y))) ∧ (y < (1 + (rt (y) + (rt (y) + (rt (y) ∗ rt (y)))))) Theorem: rt-is-unique ((a ∈ N) ∧ ((a ∗ a) ≤ y) ∧ (y < ((1 + a) ∗ (1 + a)))) → (a = rt (y)) Theorem: ncons-lemma rt (u + ((u + v) ∗ (u + v))) = (u + v) Definition: ncar (x) = (x − (rt (x) ∗ rt (x))) Definition: ncdr (x) = (rt (x) − ncar (x)) Definition: ncons (i, j ) = (i + ((i + j ) ∗ (i + j ))) Theorem: ncar-ncons (i ∈ N) → (ncar (ncons (i, j )) = i) Theorem: ncdr-ncons (j ∈ N) → (ncdr (ncons (i, j )) = j ) Definition: ncadr (x) = ncar (ncdr (x)) Definition: ncaddr (x) = ncar (ncdr (ncdr (x))) Theorem: rt-lessp ((x ≄ 0) ∧ (x ≠ 1)) → (rt (x) < x)

;   I'm sure the system could prove this without the hint, but it would use
;   induction and this is the obvious way to do it.

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

Theorem: lessp-difference-1 ((a − b) < c) = if a < b then 0 < c

else a < (b + c) endif

Theorem: ncar-lesseqp x ≮ ncar (x)

Theorem: crock (x < (rt (x) − d)) = f

Theorem: ncdr-lesseqp x ≮ ncdr (x)

Theorem: ncdr-lessp ((fn ∈ N) ∧ (ncar (fn) ≠ 0) ∧ (ncar (fn) ≠ 1)) → (ncdr (fn) < fn)

Event: Disable ncar.

Event: Disable ncdr.

Definition: pr-apply (fn, arg) = if fn ∉ N then 0

elseif ncar (fn) = 0 then 0 elseif ncar (fn) = 1 then arg elseif ncar (fn) = 2 then 1 + arg elseif ncar (fn) = 3 then rt (arg) elseif ncar (fn) = 4 then if arg ≃ 0 then 0

else pr-apply (ncdr (fn), pr-apply (fn, arg − 1)) endif elseif ncar (fn) = 5 then pr-apply (ncadr (fn), arg) + pr-apply (ncaddr (fn), arg) elseif ncar (fn) = 6 then pr-apply (ncadr (fn), arg) − pr-apply (ncaddr (fn), arg) elseif ncar (fn) = 7 then pr-apply (ncadr (fn), arg) ∗ pr-apply (ncaddr (fn), arg) elseif ncar (fn) = 8 then pr-apply (ncadr (fn), pr-apply (ncaddr (fn), arg)) else 0 endif

Definition: non-pr-fn (x) = (1 + pr-apply (x, x))

Definition: counter-example-for (x) = fix (x)

Theorem: non-pr-functions-exist non-pr-fn (counter-example-for (fn)) ≠ pr-apply (fn, counter-example-for (fn))

Theorem: counter-example-for-numeric counter-example-for (x) ∈ N

Event: Disable pr-apply.

Definition: max2 (fn, i) = if i ≃ 0 then pr-apply (fn, i)

else max (pr-apply (fn, i), max2 (fn, i − 1)) endif

Definition: max1 (fn, i) = if fn ≃ 0 then max2 (fn, i)

else max (max2 (fn, i), max1 (fn − 1, i)) endif

Theorem: max2-gte max2 (i, j ) ≮ pr-apply (i, j )

Definition: exceed (j ) = (1 + max1 (j , j ))

Definition: exceed-at (i) = i

Theorem: max1-gte1 (fn ∈ N) → (max1 (j + fn, i) ≮ pr-apply (fn, i))

Theorem: max1-gte2 (fn ∈ N) → (max1 (j + fn, j + fn) ≮ pr-apply (fn, j + fn))

Theorem: exceed-is-bigger (fn ∈ N) → (pr-apply (fn, j + exceed-at (fn)) < exceed (j + exceed-at (fn)))

Index

counter-example-for, 3, 4 counter-example-for-numeric, 4 crock, 3

difference-0, 2

exceed, 4 exceed-at, 4 exceed-is-bigger, 4

lessp-difference-1, 3

max1, 4 max1-gte1, 4 max1-gte2, 4 max2, 4 max2-gte, 4

ncaddr, 2, 3 ncadr, 2, 3 ncar, 2, 3 ncar-lesseqp, 3 ncar-ncons, 2 ncdr, 2, 3 ncdr-lesseqp, 3 ncdr-lessp, 3 ncdr-ncons, 2 ncons, 2 ncons-lemma, 2 non-pr-fn, 3, 4 non-pr-functions-exist, 4

plus-add1, 1 pr-apply, 3, 4

rt, 1–3 rt-is-unique, 2 rt-lesseqp, 2 rt-lessp, 2

spec-for-rt, 2 square-0, 2 square-monotonic, 2

times-add1, 1