[[[
Show that a formal system of lisp complexity
H_lisp (FAS) = N cannot enable us to exhibit
an elegant S-expression of size greater than N + 410.
An elegant lisp expression is one with the property
that no smaller S-expression has the same value.
Setting: formal axiomatic system is never-ending
lisp expression that displays elegant S-expressions.
]]]
[Here is the key expression.]
define expression
let (examine x)
if atom x false
if < n size car x car x
(examine cdr x)
let fas 'display ^ 10 430 [insert FAS here preceeded by ']
let n + 410 size fas
let t 0
let (loop)
let v try t fas nil
let s (examine caddr v)
if s eval s
if = success car v failure
let t + t 1
(loop)
(loop)
[Size expression.]
size expression
[Run expression & show that it knows its own size
and can find something bigger than it is.]
eval expression
[Here it fails to find anything bigger than it is.]
let (examine x)
if atom x false
if < n size car x car x
(examine cdr x)
let fas 'display ^ 10 429 [insert FAS here preceeded by ']
let n + 410 size fas
let t 0
let (loop)
let v try t fas nil
let s (examine caddr v)
if s eval s
if = success car v failure
let t + t 1
(loop)
(loop)