C T McBride wrote: > a simple diagonalization argument shows > that the system's own normalization function (terminating, by definition) > cannot be coded within the system itself. I would be interested in seeing this. Could you elaborate, or point us to a link where this is spelled out? Sam Moelius