#|
Copyright (C) 1994 by Computational Logic, Inc.  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. 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 Computational Logic, Inc. 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: ramsey (p, q) = if p ≃ 0 then 1

elseif q ≃ 0 then 1

else ramsey (p − 1, q) + ramsey (p, q − 1) endif

Definition: related (i, j , pairs) = ((cons (i, j ) ∈ pairs) ∨ (cons (j , i) ∈ pairs))

Definition: partition (n, rest, pairs) = if listp (rest)

then if related (n, car (rest), pairs)

then cons (cons (car (rest), car (partition (n, cdr (rest), pairs))), cdr (partition (n, cdr (rest), pairs)))

else cons (car (partition (n, cdr (rest), pairs)),

cons (car (rest), cdr (partition (n, cdr (rest), pairs)))) endif

else cons (nil, nil) endif Definition: length (lst) = if listp (lst) then 1 + length (cdr (lst))

else 0 endif

Definition: wit (pairs, domain, p, q) = if listp (domain)

then if p ≃ 0 then cons (nil, 1) elseif q ≃ 0 then cons (nil, 2) elseif length (car (partition (car (domain), cdr (domain), pairs)))

< ramsey (p − 1, q) then if cdr (wit (pairs,

cdr (partition (car (domain), cdr (domain), pairs)), p, q − 1))

                = 1

then wit (pairs, cdr (partition (car (domain), cdr (domain), pairs)), p, q − 1) else cons (cons (car (domain),

car (wit (pairs,

cdr (partition (car (domain), cdr (domain), pairs)),

p,

q − 1))),

2) endif

elseif cdr (wit (pairs, car (partition (car (domain), cdr (domain), pairs)), p − 1, q))

              = 2

then wit (pairs, car (partition (car (domain), cdr (domain), pairs)), p − 1, q)

else cons (cons (car (domain),

car (wit (pairs,

car (partition (car (domain), cdr (domain), pairs)),

p − 1,

q))),

1) endif

else cons (nil, 1) endif

Definition: homogeneous1 (n, domain, pairs, flg) = if listp (domain)

then if flg = 1 then related (n, car (domain), pairs) else ¬ related (n, car (domain), pairs) endif ∧ homogeneous1 (n, cdr (domain), pairs, flg)

else t endif

Definition: homogeneous (domain, pairs, flg) = if listp (domain)

then homogeneous1 (car (domain), cdr (domain), pairs, flg) ∧ homogeneous (cdr (domain), pairs, flg)

else t endif

Definition: subsetp (x, y) = if x ≃ nil then t

elseif car (x) ∈ y then subsetp (cdr (x), y)

else f endif

Theorem: member-cons (a ∈ l) → (a ∈ cons (x, l))

Theorem: subsetp-cons subsetp (l, m) → subsetp (l, cons (a, m))

Theorem: subsetp-reflexivity subsetp (x, x)

Theorem: cdr-subsetp subsetp (cdr (x), x)

Theorem: member-subsetp ((x ∈ y) ∧ subsetp (y, z)) → (x ∈ z)

Theorem: subsetp-is-transitive (subsetp (x, y) ∧ subsetp (y, z)) → subsetp (x, z)

Theorem: subsetp-cdr-partition subsetp (cdr (partition (x, z, pairs)), z)

Theorem: subsetp-hom-set-domain-1 subsetp (car (wit (pairs, cdr (partition (x, z, pairs)), p, q)),

cdr (partition (x, z, pairs))) → subsetp (car (wit (pairs, cdr (partition (x, z, pairs)), p, q)), cons (x, z))

Theorem: subsetp-car-partition subsetp (car (partition (x, z, pairs)), z)

Theorem: subsetp-hom-set-domain-2 subsetp (car (wit (pairs, car (partition (x, z, pairs)), p, q)),

car (partition (x, z, pairs))) → subsetp (car (wit (pairs, car (partition (x, z, pairs)), p, q)), cons (x, z))

Theorem: subsetp-hom-set-domain subsetp (car (wit (pairs, domain, p, q)), domain)

Definition: good-hom-set (pairs, domain, p, q, flg) = (homogeneous (car (wit (pairs, domain, p, q)), pairs, flg)

∧ (length (car (wit (pairs, domain, p, q)))

≮ if flg = 1 then p else q endif))

Theorem: homogeneous1-subset (subsetp (x, domain) ∧ homogeneous1 (elt, domain, pairs, flg)) → homogeneous1 (elt, x, pairs, flg)

Theorem: homogeneous1-cdr-partition homogeneous1 (elt, cdr (partition (elt, dom, pairs)), pairs, 2)

Theorem: length-partition-1 length (z) = (length (car (partition (x, z, pairs)))

+ length (cdr (partition (x, z, pairs))))

Theorem: length-partition length (car (partition (x, z, pairs))) = (length (z) − length (cdr (partition (x, z, pairs))))

Theorem: ramsey-not-zero 0 < ramsey (p, q)

Theorem: homogeneous1-car-wit-cdr-partition homogeneous1 (elt, car (wit (pairs, cdr (partition (elt, dom, pairs)), p, q)), pairs, 2)

Theorem: homogeneous1-car-partition homogeneous1 (elt, car (partition (elt, dom, pairs)), pairs, 1)

Theorem: homogeneous1-car-wit-car-partition homogeneous1 (elt, car (wit (pairs, car (partition (elt, dom, pairs)), p, q)), pairs, 1)

Theorem: cdr-wit-is-1-or-2 (cdr (wit (pairs, dom, p, q)) ≠ 1) → (cdr (wit (pairs, dom, p, q)) = 2)

Theorem: wit-yields-good-hom-set (length (domain) ≮ ramsey (p, q)) → good-hom-set (pairs, domain, p, q, cdr (wit (pairs, domain, p, q)))

Definition: setp (x) = if listp (x) then (car (x) ∉ cdr (x)) ∧ setp (cdr (x))

else t endif

Theorem: setp-partition setp (x) → (setp (car (partition (a, x, pairs))) ∧ setp (cdr (partition (a, x, pairs))))

Theorem: not-member-car-wit-cdr-partition (z ∉ x) → (z ∉ car (wit (pairs, cdr (partition (z, x, pairs)), p, q)))

Theorem: not-member-car-wit-car-partition (z ∉ x) → (z ∉ car (wit (pairs, car (partition (z, x, pairs)), p, q)))

Theorem: setp-hom-set setp (domain) → setp (car (wit (pairs, domain, p, q)))

Theorem: ramsey-theorem-2 (ramsey (p, q) ≤ length (domain)) → (subsetp (car (wit (pairs, domain, p, q)), domain)

∧ good-hom-set (pairs, domain, p, q, cdr (wit (pairs, domain, p, q))) ∧ (setp (domain) → setp (car (wit (pairs, domain, p, q)))))

Index

cdr-subsetp, 3 cdr-wit-is-1-or-2, 5

good-hom-set, 4, 5

homogeneous, 3, 4 homogeneous1, 3–5 homogeneous1-car-partition, 4 homogeneous1-car-wit-car-partiti

on, 5 homogeneous1-car-wit-cdr-partiti

on, 4 homogeneous1-cdr-partition, 4 homogeneous1-subset, 4

length, 2, 4, 5 length-partition, 4 length-partition-1, 4

member-cons, 3 member-subsetp, 3

not-member-car-wit-car-partitio

n, 5 not-member-car-wit-cdr-partitio

n, 5

partition, 1–5

ramsey, 1, 2, 4, 5 ramsey-not-zero, 4 ramsey-theorem-2, 5 related, 1, 3

setp, 5 setp-hom-set, 5 setp-partition, 5 subsetp, 3–5 subsetp-car-partition, 4 subsetp-cdr-partition, 3 subsetp-cons, 3 subsetp-hom-set-domain, 4 subsetp-hom-set-domain-1, 4 subsetp-hom-set-domain-2, 4 subsetp-is-transitive, 3 subsetp-reflexivity, 3

wit, 2–5

wit-yields-good-hom-set, 5