Lambda the Ultimate

I have written a paper to show how natural numbers without
any conceptual limitation (i.e. arbitrarily sized) can be implemented
and verified in Modern Eiffel. The fact that the implementation is
highly inefficient to execute is accepted. The implementation
shall serve as a model on how to implement inductively defined
data types in Modern Eiffel and on how to proof important
properties of the implemented functions.

Many correctness proof are given in full detail. Modern
Eiffel's proof engine can derive all these proofs
mechanically. The developer just has to state the properties.