[mizar] Looking for co-author for ordinal article

[Sebastian Koch <skoch02@students.uni-mainz.de>]

Hello there dear MIZAR enthusiasts!

I'm currently working on the article ORDINAL7 as a continuation of late 
Bancerek's ORDINAL5. Basically I'm defining a functor for the 
Cantor-normal-form of a given ordinal and then the "natural" addition of 
ordinals via the components of their Cantor-normal-forms + a few 
properties. I'm currently at about 1800 lines and I'm looking for a 
co-author.

While proving the uniqueness of the CNF of an ordinal I got stuck and it 
seems like 1) I can't prove it with what the MML provides and 2) I'm not 
really good at transfinite induction. My knowledge of ordinals is 
self-taught and I could really use some expert, mainly to finish/fix the 
uniqueness proof. While we're at it, we could also add some basic 
ordinal theorems the MML seems to lack if you are interested, for 
example the additive closure "for a, b, c st a in exp(omega,c) & b in 
exp(omega,c) holds a +^ b in exp(omega,c)", the multiplicative closure, 
that multiplication of two ordinals is greater than their sum most of 
the time and the same for exponentation/multiplication.

If you are interested, please contact me under 
skoch02@students.uni-mainz.de .


Best regards
Sebastian Koch