[Axiom-mail] all sorts of proof

[root]

re: Proof thesis.

Many thanks.

I'm looking into the sorting algorithms used in the algebra.
I've found 4 types: explicit where the code exists 
under the name "sort", exports where the implementation is
inherited, embeded where the code exists inline and implicit
where the sorting occurs by construction (e.g. a new item is
always added "in order" at each function call).

I'm muttering and puzzling over ways to prove the 4 kinds.
Even the explicit case involves inherited functions from
other domains. There is no such thing as a simple job.

Tim