Dear Russell: I think you miss what I am saying.

At 4/20/01, you wrote: >I disagree. The UD will have a particular way of generating (or >enumerating) the theorems of the FAS, such that it doesn't generate >the same theorem twice. The UD is [so it is said] generating all theorems. Some of these are no doubt not elegant. It does not generate proofs twice but may generate more than one proof of a given object. All this is not germane to the fact that it is doing all this by the only path [proof] - {its "particular way" as you say} that it has available. That makes this path elegant by default. Thus we have an algorithm - the generating FAS - generating a very simple object [so it is said] by an incredibly complex and elegant "particular way". Incredibly complex elegant proofs do not end in very simple objects. Hal