:: Epsilon Numbers and Cantor Normal Form
:: by Grzegorz Bancerek
::
:: Received October 20, 2009
:: Copyright (c) 2009-2012 Association of Mizar Users


begin

theorem Th1: :: ORDINAL5:1
for a, b being ordinal number holds
( not a c= succ b or a c= b or a = succ b )
proof end;

registration
cluster NAT -> limit_ordinal ;
coherence
omega is limit_ordinal
;
cluster empty -> empty Ordinal-yielding for set ;
coherence
for b1 being empty set holds b1 is Ordinal-yielding
proof end;
end;

registration
cluster Relation-like Function-like non empty T-Sequence-like finite for set ;
existence
ex b1 being T-Sequence st
( not b1 is empty & b1 is finite )
proof end;
end;

registration
let f be T-Sequence;
let g be non empty T-Sequence;
cluster f ^ g -> non empty ;
coherence
not f ^ g is empty
proof end;
cluster g ^ f -> non empty ;
coherence
not g ^ f is empty
proof end;
end;

theorem Th2: :: ORDINAL5:2
for a, b being ordinal number
for S being T-Sequence st dom S = a +^ b holds
ex S1, S2 being T-Sequence st
( S = S1 ^ S2 & dom S1 = a & dom S2 = b )
proof end;

theorem Th3: :: ORDINAL5:3
for S1, S2 being T-Sequence holds
( rng S1 c= rng (S1 ^ S2) & rng S2 c= rng (S1 ^ S2) )
proof end;

theorem Th4: :: ORDINAL5:4
for S1, S2 being T-Sequence st S1 ^ S2 is Ordinal-yielding holds
( S1 is Ordinal-yielding & S2 is Ordinal-yielding )
proof end;

definition
let f be T-Sequence;
attr f is decreasing means :: ORDINAL5:def 1
for a, b being ordinal number st a in b & b in dom f holds
f . b in f . a;
attr f is non-decreasing means :Def2: :: ORDINAL5:def 2
for a, b being ordinal number st a in b & b in dom f holds
f . a c= f . b;
attr f is non-increasing means :: ORDINAL5:def 3
for a, b being ordinal number st a in b & b in dom f holds
f . b c= f . a;
end;

:: deftheorem defines decreasing ORDINAL5:def 1 :
for f being T-Sequence holds
( f is decreasing iff for a, b being ordinal number st a in b & b in dom f holds
f . b in f . a );

:: deftheorem Def2 defines non-decreasing ORDINAL5:def 2 :
for f being T-Sequence holds
( f is non-decreasing iff for a, b being ordinal number st a in b & b in dom f holds
f . a c= f . b );

:: deftheorem defines non-increasing ORDINAL5:def 3 :
for f being T-Sequence holds
( f is non-increasing iff for a, b being ordinal number st a in b & b in dom f holds
f . b c= f . a );

registration
cluster Relation-like Function-like T-Sequence-like Ordinal-yielding increasing -> non-decreasing for set ;
coherence
for b1 being Ordinal-Sequence st b1 is increasing holds
b1 is non-decreasing
proof end;
cluster Relation-like Function-like T-Sequence-like Ordinal-yielding decreasing -> non-increasing for set ;
coherence
for b1 being Ordinal-Sequence st b1 is decreasing holds
b1 is non-increasing
proof end;
end;

theorem Th5: :: ORDINAL5:5
for f being T-Sequence holds
( f is infinite iff omega c= dom f )
proof end;

registration
cluster Relation-like Function-like T-Sequence-like decreasing -> finite for set ;
coherence
for b1 being T-Sequence st b1 is decreasing holds
b1 is finite
proof end;
cluster empty -> empty increasing decreasing for set ;
coherence
for b1 being empty set holds
( b1 is decreasing & b1 is increasing )
proof end;
end;

registration
let a be ordinal number ;
cluster <%a%> -> Ordinal-yielding ;
coherence
<%a%> is Ordinal-yielding
proof end;
end;

registration
let a be ordinal number ;
cluster <%a%> -> increasing decreasing ;
coherence
( <%a%> is decreasing & <%a%> is increasing )
proof end;
end;

registration
cluster Relation-like Function-like non empty T-Sequence-like finite Ordinal-yielding increasing decreasing non-decreasing non-increasing for set ;
existence
ex b1 being Ordinal-Sequence st
( b1 is decreasing & b1 is increasing & b1 is non-decreasing & b1 is non-increasing & b1 is finite & not b1 is empty )
proof end;
end;

theorem Th6: :: ORDINAL5:6
for f being non-decreasing Ordinal-Sequence st not dom f is empty holds
Union f is_limes_of f
proof end;

theorem :: ORDINAL5:7
for a, b being ordinal number
for n being Nat st a in b holds
n *^ (exp (omega,a)) in exp (omega,b)
proof end;

theorem Th8: :: ORDINAL5:8
for a being ordinal number
for f being Ordinal-Sequence st 0 in a & ( for b being ordinal number st b in dom f holds
f . b = exp (a,b) ) holds
f is non-decreasing
proof end;

theorem Th9: :: ORDINAL5:9
for a, b being ordinal number st a is limit_ordinal & 0 in b holds
exp (a,b) is limit_ordinal
proof end;

theorem :: ORDINAL5:10
for a being ordinal number
for f being Ordinal-Sequence st 1 in a & ( for b being ordinal number st b in dom f holds
f . b = exp (a,b) ) holds
f is increasing
proof end;

theorem Th11: :: ORDINAL5:11
for a, b being ordinal number
for x being set st 0 in a & not b is empty & b is limit_ordinal holds
( x in exp (a,b) iff ex c being ordinal number st
( c in b & x in exp (a,c) ) )
proof end;

theorem Th12: :: ORDINAL5:12
for a, b, c being ordinal number st 0 in a & exp (a,b) in exp (a,c) holds
b in c
proof end;

begin

definition
let a, b be Ordinal;
func a |^|^ b -> Ordinal means :Def4: :: ORDINAL5:def 4
ex phi being Ordinal-Sequence st
( it = last phi & dom phi = succ b & phi . {} = 1 & ( for c being Ordinal st succ c in succ b holds
phi . (succ c) = exp (a,(phi . c)) ) & ( for c being Ordinal st c in succ b & c <> {} & c is limit_ordinal holds
phi . c = lim (phi | c) ) );
correctness
existence
ex b1 being Ordinal ex phi being Ordinal-Sequence st
( b1 = last phi & dom phi = succ b & phi . {} = 1 & ( for c being Ordinal st succ c in succ b holds
phi . (succ c) = exp (a,(phi . c)) ) & ( for c being Ordinal st c in succ b & c <> {} & c is limit_ordinal holds
phi . c = lim (phi | c) ) )
;
uniqueness
for b1, b2 being Ordinal st ex phi being Ordinal-Sequence st
( b1 = last phi & dom phi = succ b & phi . {} = 1 & ( for c being Ordinal st succ c in succ b holds
phi . (succ c) = exp (a,(phi . c)) ) & ( for c being Ordinal st c in succ b & c <> {} & c is limit_ordinal holds
phi . c = lim (phi | c) ) ) & ex phi being Ordinal-Sequence st
( b2 = last phi & dom phi = succ b & phi . {} = 1 & ( for c being Ordinal st succ c in succ b holds
phi . (succ c) = exp (a,(phi . c)) ) & ( for c being Ordinal st c in succ b & c <> {} & c is limit_ordinal holds
phi . c = lim (phi | c) ) ) holds
b1 = b2
;
proof end;
end;

:: deftheorem Def4 defines |^|^ ORDINAL5:def 4 :
for a, b, b3 being Ordinal holds
( b3 = a |^|^ b iff ex phi being Ordinal-Sequence st
( b3 = last phi & dom phi = succ b & phi . {} = 1 & ( for c being Ordinal st succ c in succ b holds
phi . (succ c) = exp (a,(phi . c)) ) & ( for c being Ordinal st c in succ b & c <> {} & c is limit_ordinal holds
phi . c = lim (phi | c) ) ) );

theorem Th13: :: ORDINAL5:13
for a being ordinal number holds a |^|^ 0 = 1
proof end;

theorem Th14: :: ORDINAL5:14
for a, b being ordinal number holds a |^|^ (succ b) = exp (a,(a |^|^ b))
proof end;

theorem Th15: :: ORDINAL5:15
for b, a being ordinal number st b <> {} & b is limit_ordinal holds
for phi being Ordinal-Sequence st dom phi = b & ( for c being ordinal number st c in b holds
phi . c = a |^|^ c ) holds
a |^|^ b = lim phi
proof end;

theorem Th16: :: ORDINAL5:16
for a being ordinal number holds a |^|^ 1 = a
proof end;

theorem Th17: :: ORDINAL5:17
for a being ordinal number holds 1 |^|^ a = 1
proof end;

theorem Th18: :: ORDINAL5:18
for a being ordinal number holds a |^|^ 2 = exp (a,a)
proof end;

theorem :: ORDINAL5:19
for a being ordinal number holds a |^|^ 3 = exp (a,(exp (a,a)))
proof end;

theorem :: ORDINAL5:20
for n being Nat holds
( 0 |^|^ (2 * n) = 1 & 0 |^|^ ((2 * n) + 1) = 0 )
proof end;

theorem Th21: :: ORDINAL5:21
for a, b, c being ordinal number st a c= b & 0 in c holds
c |^|^ a c= c |^|^ b
proof end;

theorem :: ORDINAL5:22
for a being ordinal number
for f being Ordinal-Sequence st 0 in a & ( for b being ordinal number st b in dom f holds
f . b = a |^|^ b ) holds
f is non-decreasing
proof end;

theorem Th23: :: ORDINAL5:23
for a, b being ordinal number st 0 in a & 0 in b holds
a c= a |^|^ b
proof end;

theorem Th24: :: ORDINAL5:24
for a being ordinal number
for m, n being Nat st 1 in a & m < n holds
a |^|^ m in a |^|^ n
proof end;

:: theorem :: false a |^|^ succ omega = a |^|^ omega for a > 0
:: 1 in c & a in b implies c |^|^ a in c |^|^ b
theorem Th25: :: ORDINAL5:25
for a being ordinal number
for f being Ordinal-Sequence st 1 in a & dom f c= omega & ( for b being ordinal number st b in dom f holds
f . b = a |^|^ b ) holds
f is increasing
proof end;

theorem Th26: :: ORDINAL5:26
for a, b being ordinal number st 1 in a & 1 in b holds
a in a |^|^ b
proof end;

theorem Th27: :: ORDINAL5:27
for n, k being Nat holds exp (n,k) = n |^ k
proof end;

registration
let n, k be Nat;
cluster exp (n,k) -> natural ;
coherence
exp (n,k) is natural
proof end;
end;

registration
let n, k be Nat;
cluster n |^|^ k -> natural ;
coherence
n |^|^ k is natural
proof end;
end;

theorem Th28: :: ORDINAL5:28
for n, k being Nat st n > 1 holds
n |^|^ k > k
proof end;

theorem :: ORDINAL5:29
for n being Nat st n > 1 holds
n |^|^ omega = omega
proof end;

theorem Th30: :: ORDINAL5:30
for a being ordinal number st 1 in a holds
a |^|^ omega is limit_ordinal
proof end;

theorem Th31: :: ORDINAL5:31
for a being ordinal number st 0 in a holds
exp (a,(a |^|^ omega)) = a |^|^ omega
proof end;

theorem :: ORDINAL5:32
for a, b being ordinal number st 0 in a & omega c= b holds
a |^|^ b = a |^|^ omega
proof end;

begin

Lm1: {} in omega
by ORDINAL1:def 11;

scheme :: ORDINAL5:sch 1
CriticalNumber2{ F1() -> Ordinal, F2() -> Ordinal-Sequence, F3( Ordinal) -> Ordinal } :
( F1() c= Union F2() & F3((Union F2())) = Union F2() & ( for b being ordinal number st F1() c= b & F3(b) = b holds
Union F2() c= b ) )
provided
A1: for a, b being ordinal number st a in b holds
F3(a) in F3(b) and
A2: for a being ordinal number st not a is empty & a is limit_ordinal holds
for phi being Ordinal-Sequence st dom phi = a & ( for b being ordinal number st b in a holds
phi . b = F3(b) ) holds
F3(a) is_limes_of phi and
A3: ( dom F2() = omega & F2() . 0 = F1() ) and
A4: for a being ordinal number st a in omega holds
F2() . (succ a) = F3((F2() . a))
proof end;

scheme :: ORDINAL5:sch 2
CriticalNumber3{ F1() -> Ordinal, F2( Ordinal) -> Ordinal } :
ex a being ordinal number st
( F1() in a & F2(a) = a )
provided
A1: for a, b being ordinal number st a in b holds
F2(a) in F2(b) and
A2: for a being ordinal number st not a is empty & a is limit_ordinal holds
for phi being Ordinal-Sequence st dom phi = a & ( for b being ordinal number st b in a holds
phi . b = F2(b) ) holds
F2(a) is_limes_of phi
proof end;

begin

definition
let a be ordinal number ;
attr a is epsilon means :Def5: :: ORDINAL5:def 5
exp (omega,a) = a;
end;

:: deftheorem Def5 defines epsilon ORDINAL5:def 5 :
for a being ordinal number holds
( a is epsilon iff exp (omega,a) = a );

theorem Th33: :: ORDINAL5:33
for a being ordinal number ex b being ordinal number st
( a in b & b is epsilon )
proof end;

registration
cluster epsilon-transitive epsilon-connected ordinal epsilon for set ;
existence
ex b1 being ordinal number st b1 is epsilon
proof end;
end;

definition
let a be Ordinal;
func first_epsilon_greater_than a -> epsilon Ordinal means :Def6: :: ORDINAL5:def 6
( a in it & ( for b being epsilon Ordinal st a in b holds
it c= b ) );
existence
ex b1 being epsilon Ordinal st
( a in b1 & ( for b being epsilon Ordinal st a in b holds
b1 c= b ) )
proof end;
uniqueness
for b1, b2 being epsilon Ordinal st a in b1 & ( for b being epsilon Ordinal st a in b holds
b1 c= b ) & a in b2 & ( for b being epsilon Ordinal st a in b holds
b2 c= b ) holds
b1 = b2
proof end;
end;

:: deftheorem Def6 defines first_epsilon_greater_than ORDINAL5:def 6 :
for a being Ordinal
for b2 being epsilon Ordinal holds
( b2 = first_epsilon_greater_than a iff ( a in b2 & ( for b being epsilon Ordinal st a in b holds
b2 c= b ) ) );

theorem :: ORDINAL5:34
for a, b being ordinal number st a c= b holds
first_epsilon_greater_than a c= first_epsilon_greater_than b
proof end;

theorem :: ORDINAL5:35
for a, b being ordinal number st a in b & b in first_epsilon_greater_than a holds
first_epsilon_greater_than b = first_epsilon_greater_than a
proof end;

theorem Th36: :: ORDINAL5:36
first_epsilon_greater_than 0 = omega |^|^ omega
proof end;

theorem Th37: :: ORDINAL5:37
for e being epsilon Ordinal holds omega in e
proof end;

registration
cluster ordinal epsilon -> non empty limit_ordinal for set ;
coherence
for b1 being Ordinal st b1 is epsilon holds
( not b1 is empty & b1 is limit_ordinal )
proof end;
end;

theorem Th38: :: ORDINAL5:38
for e being epsilon Ordinal holds exp (omega,(exp (e,omega))) = exp (e,(exp (e,omega)))
proof end;

theorem Th39: :: ORDINAL5:39
for n being Nat
for e being epsilon Ordinal st 0 in n holds
e |^|^ (n + 2) = exp (omega,(e |^|^ (n + 1)))
proof end;

theorem Th40: :: ORDINAL5:40
for e being epsilon Ordinal holds first_epsilon_greater_than e = e |^|^ omega
proof end;

definition
let a be Ordinal;
:: equals omega |^|^ exp(omega, 1+^a); :: wg wikipedii, ale to nie prawda
func epsilon_ a -> Ordinal means :Def7: :: ORDINAL5:def 7
ex phi being Ordinal-Sequence st
( it = last phi & dom phi = succ a & phi . {} = omega |^|^ omega & ( for b being Ordinal st succ b in succ a holds
phi . (succ b) = (phi . b) |^|^ omega ) & ( for c being Ordinal st c in succ a & c <> {} & c is limit_ordinal holds
phi . c = lim (phi | c) ) );
correctness
existence
ex b1 being Ordinal ex phi being Ordinal-Sequence st
( b1 = last phi & dom phi = succ a & phi . {} = omega |^|^ omega & ( for b being Ordinal st succ b in succ a holds
phi . (succ b) = (phi . b) |^|^ omega ) & ( for c being Ordinal st c in succ a & c <> {} & c is limit_ordinal holds
phi . c = lim (phi | c) ) )
;
uniqueness
for b1, b2 being Ordinal st ex phi being Ordinal-Sequence st
( b1 = last phi & dom phi = succ a & phi . {} = omega |^|^ omega & ( for b being Ordinal st succ b in succ a holds
phi . (succ b) = (phi . b) |^|^ omega ) & ( for c being Ordinal st c in succ a & c <> {} & c is limit_ordinal holds
phi . c = lim (phi | c) ) ) & ex phi being Ordinal-Sequence st
( b2 = last phi & dom phi = succ a & phi . {} = omega |^|^ omega & ( for b being Ordinal st succ b in succ a holds
phi . (succ b) = (phi . b) |^|^ omega ) & ( for c being Ordinal st c in succ a & c <> {} & c is limit_ordinal holds
phi . c = lim (phi | c) ) ) holds
b1 = b2
;
proof end;
end;

:: deftheorem Def7 defines epsilon_ ORDINAL5:def 7 :
for a, b2 being Ordinal holds
( b2 = epsilon_ a iff ex phi being Ordinal-Sequence st
( b2 = last phi & dom phi = succ a & phi . {} = omega |^|^ omega & ( for b being Ordinal st succ b in succ a holds
phi . (succ b) = (phi . b) |^|^ omega ) & ( for c being Ordinal st c in succ a & c <> {} & c is limit_ordinal holds
phi . c = lim (phi | c) ) ) );

theorem Th41: :: ORDINAL5:41
epsilon_ 0 = omega |^|^ omega
proof end;

theorem Th42: :: ORDINAL5:42
for a being ordinal number holds epsilon_ (succ a) = (epsilon_ a) |^|^ omega
proof end;

theorem Th43: :: ORDINAL5:43
for b being ordinal number st b <> {} & b is limit_ordinal holds
for phi being Ordinal-Sequence st dom phi = b & ( for c being ordinal number st c in b holds
phi . c = epsilon_ c ) holds
epsilon_ b = lim phi
proof end;

theorem Th44: :: ORDINAL5:44
for a, b being ordinal number st a in b holds
epsilon_ a in epsilon_ b
proof end;

theorem Th45: :: ORDINAL5:45
for phi being Ordinal-Sequence st ( for c being ordinal number st c in dom phi holds
phi . c = epsilon_ c ) holds
phi is increasing
proof end;

theorem Th46: :: ORDINAL5:46
for b being ordinal number st b <> {} & b is limit_ordinal holds
for phi being Ordinal-Sequence st dom phi = b & ( for c being ordinal number st c in b holds
phi . c = epsilon_ c ) holds
epsilon_ b = Union phi
proof end;

theorem Th47: :: ORDINAL5:47
for b being ordinal number
for x being set st not b is empty & b is limit_ordinal holds
( x in epsilon_ b iff ex c being ordinal number st
( c in b & x in epsilon_ c ) )
proof end;

theorem Th48: :: ORDINAL5:48
for a being ordinal number holds a c= epsilon_ a
proof end;

theorem Th49: :: ORDINAL5:49
for X being non empty set st ( for x being set st x in X holds
( x is epsilon Ordinal & ex e being epsilon Ordinal st
( x in e & e in X ) ) ) holds
union X is epsilon Ordinal
proof end;

theorem Th50: :: ORDINAL5:50
for X being non empty set st ( for x being set st x in X holds
x is epsilon Ordinal ) & ( for a being ordinal number st a in X holds
first_epsilon_greater_than a in X ) holds
union X is epsilon Ordinal
proof end;

registration
let a be ordinal number ;
cluster epsilon_ a -> epsilon ;
coherence
epsilon_ a is epsilon
proof end;
end;

:: WP: The ordinal indexing of epsilon numbers
theorem :: ORDINAL5:51
for a being ordinal number st a is epsilon holds
ex b being ordinal number st a = epsilon_ b
proof end;

begin

definition
let A be finite Ordinal-Sequence;
func Sum^ A -> Ordinal means :Def8: :: ORDINAL5:def 8
ex f being Ordinal-Sequence st
( it = last f & dom f = succ (dom A) & f . 0 = 0 & ( for n being Nat st n in dom A holds
f . (n + 1) = (f . n) +^ (A . n) ) );
correctness
existence
ex b1 being Ordinal ex f being Ordinal-Sequence st
( b1 = last f & dom f = succ (dom A) & f . 0 = 0 & ( for n being Nat st n in dom A holds
f . (n + 1) = (f . n) +^ (A . n) ) )
;
uniqueness
for b1, b2 being Ordinal st ex f being Ordinal-Sequence st
( b1 = last f & dom f = succ (dom A) & f . 0 = 0 & ( for n being Nat st n in dom A holds
f . (n + 1) = (f . n) +^ (A . n) ) ) & ex f being Ordinal-Sequence st
( b2 = last f & dom f = succ (dom A) & f . 0 = 0 & ( for n being Nat st n in dom A holds
f . (n + 1) = (f . n) +^ (A . n) ) ) holds
b1 = b2
;
proof end;
end;

:: deftheorem Def8 defines Sum^ ORDINAL5:def 8 :
for A being finite Ordinal-Sequence
for b2 being Ordinal holds
( b2 = Sum^ A iff ex f being Ordinal-Sequence st
( b2 = last f & dom f = succ (dom A) & f . 0 = 0 & ( for n being Nat st n in dom A holds
f . (n + 1) = (f . n) +^ (A . n) ) ) );

theorem Th52: :: ORDINAL5:52
Sum^ {} = 0
proof end;

theorem Th53: :: ORDINAL5:53
for a being ordinal number holds Sum^ <%a%> = a
proof end;

theorem Th54: :: ORDINAL5:54
for a being ordinal number
for A being finite Ordinal-Sequence holds Sum^ (A ^ <%a%>) = (Sum^ A) +^ a
proof end;

theorem Th55: :: ORDINAL5:55
for a being ordinal number
for A being finite Ordinal-Sequence holds Sum^ (<%a%> ^ A) = a +^ (Sum^ A)
proof end;

theorem Th56: :: ORDINAL5:56
for A being finite Ordinal-Sequence holds A . 0 c= Sum^ A
proof end;

definition
let a be ordinal number ;
attr a is Cantor-component means :Def9: :: ORDINAL5:def 9
ex b being ordinal number ex n being Nat st
( 0 in n & a = n *^ (exp (omega,b)) );
end;

:: deftheorem Def9 defines Cantor-component ORDINAL5:def 9 :
for a being ordinal number holds
( a is Cantor-component iff ex b being ordinal number ex n being Nat st
( 0 in n & a = n *^ (exp (omega,b)) ) );

registration
cluster ordinal Cantor-component -> non empty for set ;
coherence
for b1 being Ordinal st b1 is Cantor-component holds
not b1 is empty
proof end;
end;

registration
cluster epsilon-transitive epsilon-connected ordinal Cantor-component for set ;
existence
ex b1 being Ordinal st b1 is Cantor-component
proof end;
end;

definition
let a, b be ordinal number ;
func b -exponent a -> Ordinal means :Def10: :: ORDINAL5:def 10
( exp (b,it) c= a & ( for c being ordinal number st exp (b,c) c= a holds
c c= it ) ) if ( 1 in b & 0 in a )
otherwise it = 0 ;
existence
( ( 1 in b & 0 in a implies ex b1 being Ordinal st
( exp (b,b1) c= a & ( for c being ordinal number st exp (b,c) c= a holds
c c= b1 ) ) ) & ( ( not 1 in b or not 0 in a ) implies ex b1 being Ordinal st b1 = 0 ) )
proof end;
uniqueness
for b1, b2 being Ordinal holds
( ( 1 in b & 0 in a & exp (b,b1) c= a & ( for c being ordinal number st exp (b,c) c= a holds
c c= b1 ) & exp (b,b2) c= a & ( for c being ordinal number st exp (b,c) c= a holds
c c= b2 ) implies b1 = b2 ) & ( ( not 1 in b or not 0 in a ) & b1 = 0 & b2 = 0 implies b1 = b2 ) )
proof end;
consistency
for b1 being Ordinal holds verum
;
end;

:: deftheorem Def10 defines -exponent ORDINAL5:def 10 :
for a, b being ordinal number
for b3 being Ordinal holds
( ( 1 in b & 0 in a implies ( b3 = b -exponent a iff ( exp (b,b3) c= a & ( for c being ordinal number st exp (b,c) c= a holds
c c= b3 ) ) ) ) & ( ( not 1 in b or not 0 in a ) implies ( b3 = b -exponent a iff b3 = 0 ) ) );

Lm2: 0 in 1
by NAT_1:44;

theorem Th57: :: ORDINAL5:57
for b, a being ordinal number st 1 in b holds
a in exp (b,(succ (b -exponent a)))
proof end;

theorem Th58: :: ORDINAL5:58
for b, a being ordinal number
for n being Nat st 0 in n & n in b holds
b -exponent (n *^ (exp (b,a))) = a
proof end;

theorem Th59: :: ORDINAL5:59
for a, b, c being ordinal number st 0 in a & 1 in b & c = b -exponent a holds
a div^ (exp (b,c)) in b
proof end;

theorem Th60: :: ORDINAL5:60
for a, b, c being ordinal number st 0 in a & 1 in b & c = b -exponent a holds
0 in a div^ (exp (b,c))
proof end;

theorem Th61: :: ORDINAL5:61
for b, a, c being ordinal number st b <> 0 holds
a mod^ (exp (b,c)) in exp (b,c)
proof end;

theorem Th62: :: ORDINAL5:62
for a being ordinal number st 0 in a holds
ex n being Nat ex c being ordinal number st
( a = (n *^ (exp (omega,(omega -exponent a)))) +^ c & 0 in n & c in exp (omega,(omega -exponent a)) )
proof end;

theorem Th63: :: ORDINAL5:63
for c, b, a being ordinal number st 1 in c & c -exponent b in c -exponent a holds
b in a
proof end;

definition
let A be Ordinal-Sequence;
attr A is Cantor-normal-form means :Def11: :: ORDINAL5:def 11
( ( for a being ordinal number st a in dom A holds
A . a is Cantor-component ) & ( for a, b being ordinal number st a in b & b in dom A holds
omega -exponent (A . b) in omega -exponent (A . a) ) );
end;

:: deftheorem Def11 defines Cantor-normal-form ORDINAL5:def 11 :
for A being Ordinal-Sequence holds
( A is Cantor-normal-form iff ( ( for a being ordinal number st a in dom A holds
A . a is Cantor-component ) & ( for a, b being ordinal number st a in b & b in dom A holds
omega -exponent (A . b) in omega -exponent (A . a) ) ) );

registration
cluster Relation-like Function-like empty T-Sequence-like Ordinal-yielding -> Cantor-normal-form for set ;
coherence
for b1 being Ordinal-Sequence st b1 is empty holds
b1 is Cantor-normal-form
proof end;
cluster Relation-like Function-like T-Sequence-like Ordinal-yielding Cantor-normal-form -> decreasing for set ;
coherence
for b1 being Ordinal-Sequence st b1 is Cantor-normal-form holds
b1 is decreasing
proof end;
end;

theorem :: ORDINAL5:64
for A being Cantor-normal-form Ordinal-Sequence st Sum^ A = 0 holds
A = {}
proof end;

theorem Th65: :: ORDINAL5:65
for b being ordinal number
for n being Nat st 0 in n holds
<%(n *^ (exp (omega,b)))%> is Cantor-normal-form
proof end;

registration
cluster Relation-like Function-like non empty T-Sequence-like Ordinal-yielding Cantor-normal-form for set ;
existence
ex b1 being Ordinal-Sequence st
( not b1 is empty & b1 is Cantor-normal-form )
proof end;
end;

theorem Th66: :: ORDINAL5:66
for A, B being Ordinal-Sequence st A ^ B is Cantor-normal-form holds
( A is Cantor-normal-form & B is Cantor-normal-form )
proof end;

theorem :: ORDINAL5:67
for A being Cantor-normal-form Ordinal-Sequence st A <> {} holds
ex c being Cantor-component Ordinal ex B being Cantor-normal-form Ordinal-Sequence st A = <%c%> ^ B
proof end;

theorem Th68: :: ORDINAL5:68
for A being non empty Cantor-normal-form Ordinal-Sequence
for c being Cantor-component Ordinal st omega -exponent (A . 0) in omega -exponent c holds
<%c%> ^ A is Cantor-normal-form
proof end;

:: WP: Existence of Cantor Normal Form for ordinal numbers
theorem :: ORDINAL5:69
for a being ordinal number ex A being Cantor-normal-form Ordinal-Sequence st a = Sum^ A
proof end;