#|
Copyright (C) 1994 by Computational Logic, Inc. and Paolo Pecchiari.  All
Rights Reserved.
This script is hereby placed in the public domain, and therefore unlimited
editing and redistribution is permitted.
NO WARRANTY
Computational Logic, Inc. AND Paolo Pecchiari 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 Computational Logic, Inc. OR Paolo Pecchiari 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.
|#
; Events from CLI Technical Report 100, ``Interaction with the Boyer-Moore
; Theorem Prover: A Tutorial Study Using the Arithmetic-Geometric Mean
; Theorem,'' by Matt Kaufmann and Paolo Pecchiari.

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

Definition: prodlist (lst) = if listp (lst) then car (lst) ∗ prodlist (cdr (lst))

else 1 endif

Definition: sumlist (lst) = if listp (lst) then car (lst) + sumlist (cdr (lst))

else 0 endif

Definition: length (x)

= if listp (x) then 1 + length (cdr (x))

else 0 endif

Definition: maxlist (x) = if listp (x)

then if listp (cdr (x)) then max (car (x), maxlist (cdr (x)))

else fix (car (x)) endif else 0 endif

Definition: min (x, y) = if x < y then fix (x)

else fix (y) endif

Definition: minlist (x) = if listp (x)

then if listp (cdr (x)) then min (car (x), minlist (cdr (x)))

else fix (car (x)) endif else 0 endif

Definition: delete1 (elt, x) = if listp (x)

then if elt = car (x) then cdr (x)

else cons (car (x), delete1 (elt, cdr (x))) endif else x endif

Theorem: maxlist-delete1-rearrange (b ∈ x) → (maxlist (cons (b, delete1 (b, x))) = maxlist (x))

Event: Let us define the theory induction-fn-disables to consist of the following events: sumlist, times, length, minlist, maxlist, delete1, occurrences.

Theorem: max-greater-than-average (listp (x) ∧ (sumlist (x) ≥ (k ∗ length (x))) ∧ (fix (k) ≠ maxlist (x))) → (k < maxlist (x))

Theorem: min-less-than-average (listp (x) ∧ (sumlist (x) ≤ (k ∗ length (x))) ∧ (fix (k) ≠ minlist (x))) → (minlist (x) < k)

Theorem: times-monotone-1 (u ≮ v) → ((u ∗ y) ≮ (v ∗ y))

Theorem: lessp-times-preserved-in-first-arg ((a ≮ (u ∗ y)) ∧ (u ≮ v)) → (a ≮ (v ∗ y))

Theorem: minlist-main-property sumlist (x) ≮ (length (x) ∗ minlist (x))

Theorem: minlist-not-maxlist-implies-minlist-lessp-average-lemma (minlist (x) ≠ maxlist (x)) → ((minlist (x) ∗ length (x)) < sumlist (x))

Theorem: minlist-not-maxlist-implies-minlist-lessp-average (listp (x) ∧ (sumlist (x) = (k ∗ length (x))) ∧ (minlist (x) ≠ maxlist (x))) → (minlist (x) < fix (k))

Theorem: maxlist-main-property (length (x) ∗ maxlist (x)) ≮ sumlist (x)

Theorem: minlist-not-maxlist-implies-maxlist-greaterp-average-lemma (minlist (x) ≠ maxlist (x)) → (sumlist (x) < (maxlist (x) ∗ length (x)))

Theorem: minlist-not-maxlist-implies-maxlist-greaterp-average (listp (x) ∧ (sumlist (x) = (k ∗ length (x))) ∧ (minlist (x) ≠ maxlist (x))) → (fix (k) < maxlist (x))

Theorem: minlist-less-than-maxlist-minus-1 (listp (x) ∧ (sumlist (x) = (k ∗ length (x))) ∧ (minlist (x) ≠ maxlist (x))) → (minlist (x) < (maxlist (x) − 1))

Theorem: maxlist-delete1-leq maxlist (lst) ≮ maxlist (delete1 (a, lst))

Theorem: member-implies-maxlist-geq (a ∈ x) → (maxlist (x) ≮ a)

Theorem: delete1-preserves-maxlist-when-maxlist-occurs-more-than-once (1 < occurrences (maxlist (x), x)) → (maxlist (delete1 (any-element, x)) = maxlist (x))

Theorem: delete1-occurrences occurrences (a, delete1 (b, x)) = if (a = b) ∧ (b ∈ x) then occurrences (a, x) − 1

else occurrences (a, x) endif Theorem: occurrence-implies-listp (1 < occurrences (a, x)) → (listp (delete1 (a, x)) = t)

Theorem: maxlist-geq-minlist maxlist (x) ≮ minlist (x)

Theorem: induction-fn-help-2-max-occurs-twice-lemma-1 ((sumlist (x) = (k ∗ length (x))) ∧ (minlist (x) ≠ maxlist (x)) ∧ (1 < occurrences (maxlist (x), x))) → (maxlist (cons (maxlist (x) − 1,

cons (1 + minlist (x),

delete1 (maxlist (x), delete1 (minlist (x), x)))))

= maxlist (x))

Theorem: member-delete1 (a ∈ delete1 (b, c)) = if a = b then 1 < occurrences (b, c)

else a ∈ c endif

Theorem: member-implies-listp (a ∈ x) → listp (x)

Theorem: induction-fn-help-2-max-occurs-twice-lemma-2 ((sumlist (x) = (k ∗ length (x))) ∧ (minlist (x) ≠ maxlist (x)) ∧ (1 < occurrences (maxlist (x), x))) → ((occurrences (maxlist (x),

cons (maxlist (x) − 1,

cons (1 + minlist (x),

delete1 (maxlist (x), delete1 (minlist (x), x)))))

< occurrences (maxlist (x), x)) = t)

Event: Disable member-implies-listp.

Theorem: induction-fn-help-2-max-occurs-twice let x0 be cons (maxlist (x) − 1,

cons (1 + minlist (x),

delete1 (maxlist (x), delete1 (minlist (x), x))))

in ((sumlist (x) = (k ∗ length (x))) ∧ (minlist (x) ≠ maxlist (x)) ∧ (1 < occurrences (maxlist (x), x))) → ord-lessp (cons (1 + maxlist (x0 ), occurrences (maxlist (x0 ), x0 )),

cons (1 + maxlist (x), occurrences (maxlist (x), x))) endlet Theorem: maxlist-not-minlist-implies-listp (minlist (x) ≠ maxlist (x)) → listp (x)

Theorem: minlist-less-than-maxlist-minus-1-better ((sumlist (x) = (k ∗ length (x))) ∧ (minlist (x) ≠ maxlist (x))) → (minlist (x) < (maxlist (x) − 1))

Event: Disable minlist-less-than-maxlist-minus-1.

Theorem: maxlist-delete1-delete1 maxlist (delete1 (b, x)) ≮ maxlist (delete1 (b, delete1 (a, x)))

Theorem: member-maxlist (maxlist (z) ≠ 0) → (maxlist (z) ∈ z)

Theorem: lessp-maxlist-delete1-maxlist ((0 < maxlist (x)) ∧ (1 ≮ occurrences (maxlist (x), x))) → (maxlist (delete1 (maxlist (x), x)) < maxlist (x))

Theorem: induction-fn-help-2-max-occurs-once-main-lemma ((sumlist (x) = (k ∗ length (x))) ∧ (minlist (x) ≠ maxlist (x)) ∧ (1 ≮ occurrences (maxlist (x), x))) → ((maxlist (cons (maxlist (x) − 1,

cons (1 + minlist (x),

delete1 (maxlist (x), delete1 (minlist (x), x)))))

< maxlist (x)) = t)

Theorem: induction-fn-help-2-max-occurs-once let x0 be cons (maxlist (x) − 1,

cons (1 + minlist (x),

delete1 (maxlist (x), delete1 (minlist (x), x))))

in ((sumlist (x) = (k ∗ length (x))) ∧ (minlist (x) ≠ maxlist (x)) ∧ (1 ≮ occurrences (maxlist (x), x))) → ord-lessp (cons (1 + maxlist (x0 ), occurrences (maxlist (x0 ), x0 )),

cons (1 + maxlist (x), occurrences (maxlist (x), x))) endlet

Theorem: induction-fn-help-2 let x0 be cons (maxlist (x) − 1,

cons (1 + minlist (x),

delete1 (maxlist (x), delete1 (minlist (x), x))))

in ((sumlist (x) = (k ∗ length (x))) ∧ (minlist (x) ≠ maxlist (x))) → ord-lessp (cons (1 + maxlist (x0 ), occurrences (maxlist (x0 ), x0 )),

cons (1 + maxlist (x), occurrences (maxlist (x), x))) endlet

Event: Disable theory induction-fn-disables.

Definition: induction-fn (x, k) = if sumlist (x) ≠ (k ∗ length (x)) then t

elseif minlist (x) = maxlist (x) then t else induction-fn (cons (maxlist (x) − 1,

cons (1 + minlist (x),

delete1 (maxlist (x),

delete1 (minlist (x), x)))),

k) endif

Event: Enable theory induction-fn-disablesinduction-fn-disables.

Theorem: sumlist-delete1-plus-version (a + sumlist (delete1 (a, x))) = if a ∈ x then sumlist (x)

else a + sumlist (x) endif

Theorem: sumlist-delete1 sumlist (delete1 (a, x)) = if a ∈ x then sumlist (x) − a

else sumlist (x) endif

Theorem: maxlist-0-is-sumlist-0 (maxlist (x) = 0) = (sumlist (x) = 0)

Theorem: main-lemma-base-case-lemma-1 (minlist (x) = maxlist (x)) → (exp (minlist (x), length (x)) = prodlist (x))

Theorem: main-lemma-base-case-lemma-2-lemma (minlist (x) = maxlist (x)) → (sumlist (x) = (minlist (x) ∗ length (x)))

Theorem: main-lemma-base-case-lemma-2-hack (((k ∗ n) = sumlist) ∧ (n ≄ 0) ∧ ((n ∗ maxlist) = sumlist)) → (fix (k) = fix (maxlist))

Theorem: equal-length-0 (length (x) = 0) = (¬ listp (x))

Theorem: main-lemma-base-case-lemma-2 (listp (x) ∧ (sumlist (x) = (k ∗ length (x))) ∧ (minlist (x) = maxlist (x))) → (minlist (x) = fix (k))

Theorem: main-lemma-base-case ((sumlist (x) = (k ∗ length (x))) ∧ (minlist (x) = maxlist (x))) → (exp (k, length (x)) = prodlist (x))

Theorem: length-delete1 length (delete1 (a, x)) = if a ∈ x then length (x) − 1

else length (x) endif

Definition: numberp-listp (x) = if listp (x) then (car (x) ∈ N) ∧ numberp-listp (cdr (x))

else x = nil endif

Theorem: member-minlist (listp (x) ∧ numberp-listp (x)) → (minlist (x) ∈ x)

Theorem: numberp-listp-delete1 numberp-listp (x) → numberp-listp (delete1 (a, x))

Theorem: add1-plus-sub1-second (y ≄ 0) → ((1 + (x + (y − 1))) = (x + y))

Theorem: sumlist-geq-maxlist sumlist (x) ≮ maxlist (x)

Theorem: sumlist-geq-minlist sumlist (x) ≮ minlist (x)

Theorem: sumlist-geq-minlist-plus-maxlist (minlist (x) ≠ maxlist (x)) → (sumlist (x) ≮ (minlist (x) + maxlist (x)))

Event: Disable plus.

Theorem: plus-times-sub1-second (y ≄ 0) → ((x + (x ∗ (y − 1))) = (x ∗ y))

Event: Disable times.

Theorem: minlist-not-maxlist-implies-length-at-least-2 (minlist (x) ≠ maxlist (x)) → (1 < length (x))

Event: Disable plus-add1-arg1.

Event: Disable plus-add1-arg2.

Event: Disable times-add1.

Event: Disable maxlist-0-is-sumlist-0.

Theorem: times-prodlist-delete1 (a ∈ x) → ((a ∗ prodlist (delete1 (a, x))) = prodlist (x))

Theorem: product-of-modified-list-lemma ((min ≠ max) ∧ (min ∈ x) ∧ (max ∈ x)) → ((max ∗ min ∗ prodlist (delete1 (max, delete1 (min, x))))

= prodlist (x))

Event: Disable times-prodlist-delete1.

Theorem: product-of-modified-list-lemma-2 ((min < max) ∧ (max ≄ 0)) → (((1 + min) ∗ (max − 1) ∗ rest)

= ((min ∗ max ∗ rest) + ((max − (1 + min)) ∗ rest)))

Theorem: positive-implies-numberp (min < max) → (max ∈ N)

Theorem: product-of-modified-list ((min < max) ∧ (min ∈ x) ∧ (max ∈ x)) → let rest be prodlist (delete1 (max, delete1 (min, x)))

in

((1 + min) ∗ (max − 1) ∗ rest)

= (prodlist (x) + ((max − (1 + min)) ∗ rest)) endlet

Theorem: main-lemma let n be length (x) in (numberp-listp (x) ∧ (sumlist (x) = (k ∗ n))) → (exp (k, n) ≮ prodlist (x)) endlet Definition: scalar-product (scalar, lst) = if listp (lst)

then cons (scalar ∗ car (lst), scalar-product (scalar, cdr (lst))) else nil endif

Theorem: sumlist-scalar-product sumlist (scalar-product (scalar, lst)) = (scalar ∗ sumlist (lst))

Theorem: prodlist-scalar-product prodlist (scalar-product (scalar, lst)) = (exp (scalar, length (lst)) ∗ prodlist (lst))

Theorem: length-scalar-product length (scalar-product (n, a)) = length (a)

Theorem: numberp-listp-scalar-product numberp-listp (a) → numberp-listp (scalar-product (n, a))

Theorem: main numberp-listp (a) → let n be length (a)

in

exp (sumlist (a), n) ≥ (exp (n, n) ∗ prodlist (a)) endlet

Theorem: sumlist-for sumlist (a) = for x in a

sum x endfor

Theorem: prodlist-for prodlist (a) = for x in a

multiply x endfor

Theorem: main-again (numberp-listp (a) ∧ (n = length (a))) → (exp (for x in a

sum x endfor, n) ≥ (exp (n, n)

∗ for x in a multiply x endfor))

Index

add1-plus-sub1-second, 7

delete1, 2–8 delete1-occurrences, 3 delete1-preserves-maxlist-when-

maxlist-occurs-more-than-once, 3

equal-length-0, 6 exp, 6–9

induction-fn, 6 induction-fn-disables, 2 induction-fn-help-2, 5 induction-fn-help-2-max-occurs-

once, 5 once-main-lemma, 5

induction-fn-help-2-max-occurs-t wice, 4 wice-lemma-1, 4 wice-lemma-2, 4

length, 1–9 length-delete1, 7 length-scalar-product, 9 lessp-maxlist-delete1-maxlist, 5 lessp-times-preserved-in-first-

arg, 3

main, 9 main-again, 9 main-lemma, 8 main-lemma-base-case, 7 main-lemma-base-case-lemma-1, 6 main-lemma-base-case-lemma-2, 7 main-lemma-base-case-lemma-2-ha

ck, 6 main-lemma-base-case-lemma-2-le

mma, 6 max-greater-than-average, 2 maxlist, 2–8 maxlist-0-is-sumlist-0, 6 maxlist-delete1-delete1, 5 maxlist-delete1-leq, 3 maxlist-delete1-rearrange, 2 maxlist-geq-minlist, 4 maxlist-main-property, 3 maxlist-not-minlist-implies-listp, 5 member-delete1, 4 member-implies-listp, 4 member-implies-maxlist-geq, 3 member-maxlist, 5 member-minlist, 7 min, 2 min-less-than-average, 2 minlist, 2–8 minlist-less-than-maxlist-minus

-1, 3

-1-better, 5 minlist-main-property, 3 minlist-not-maxlist-implies-len

gth-at-least-2, 8 minlist-not-maxlist-implies-max

list-greaterp-average, 3

list-greaterp-average-lemma, 3 minlist-not-maxlist-implies-min

list-lessp-average, 3

list-lessp-average-lemma, 3

numberp-listp, 7–9 numberp-listp-delete1, 7 numberp-listp-scalar-product, 9

occurrence-implies-listp, 4 occurrences, 3–6

plus-times-sub1-second, 7 positive-implies-numberp, 8 prodlist, 1, 6–9 prodlist-for, 9 prodlist-scalar-product, 9 product-of-modified-list, 8 product-of-modified-list-lemma, 8 product-of-modified-list-lemma-

2, 8

scalar-product, 9 sumlist, 1–9 sumlist-delete1, 6 sumlist-delete1-plus-version, 6 sumlist-for, 9 sumlist-geq-maxlist, 7 sumlist-geq-minlist, 7 sumlist-geq-minlist-plus-maxlist, 7 sumlist-scalar-product, 9

times-monotone-1, 2 times-prodlist-delete1, 8