From solovay@math.berkeley.edu Wed Nov 11 13:39:46 1998
Date: Tue, 10 Nov 1998 23:43:04 -0800 (PST)
From: "Robert M. Solovay" <solovay@math.berkeley.edu>
To: amathias@rasputin.uniandes.edu.co
Cc: solovay@math.berkeley.edu
Subject: Results

Adrian,

	Here is the printout of my calculation of the length of the
Bourbaki term for 1. If we do the original definition, I get approx.
4.524 * 10^{12}

	If we use the Kuratowski ordered pair, I get approx.

2.41 * 10^{54}

	This is big, but not nearly as big as the 2 * 10^{73} that you
claim. This is certainly related to the smaller estimate that I have
for the size of the Kuratowski ordered pair.

	I omitted some trivial lines from this printout where I "gave
the wrong commands to the genie".


USER(1): (setq p 0) ;;;[Doing the original Bourbaki definition where
                    ;;; ordered pair is a basic undefined notion.]
0

USER(3): (load "compute.cl")
; Loading ./compute.cl
T
USER(4): J_length
4523659424929
USER(5): (log J_length 10)
12.65549
USER(6): J_links
1179618517981
USER(7): (log J_links 10)
12.071742
USER(8): (setq p 1) ;;; Now use Kuratowski ordered pair

1

USER(10): (load "compute.cl")
; Loading ./compute.cl
T
USER(11): J_length
2409875496393137472149767527877436912979508338752092897
USER(12): (log J_length 10)
54.381996
USER(13): J_links
871880233733949069946182804910912227472430953034182177
USER(14): (log J_links 10)
53.940456