begin
theorem Th001:
theorem Th65:
theorem ThS1:
theorem ThS2:
:: 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 ND 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 );
theorem ThO:
theorem ThND:
theorem
theorem Th003:
theorem Th002:
theorem
theorem Th005:
theorem Th006:
begin
:: deftheorem KNUTH 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 Th0:
theorem Th1:
theorem Th2:
theorem Th3:
theorem Th4:
theorem Th39:
theorem
theorem
theorem Th5:
theorem
theorem Th6:
theorem Th7:
theorem Th8:
theorem Th9:
theorem LemExp:
theorem ThA1:
for
n,
k being
Nat st
n > 1 holds
n |^|^ k > k
theorem
theorem Th11:
theorem Th12:
theorem
begin
Lm1:
{} in omega
by ORDINAL1:def 12;
begin
:: deftheorem EPSILON defines epsilon ORDINAL5:def 5 :
for a being ordinal number holds
( a is epsilon iff exp omega ,a = a );
theorem ThE0:
:: deftheorem FEGT 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
theorem
theorem Th20:
theorem Th21:
theorem Th22:
theorem Th23:
theorem Th24:
:: deftheorem EPSILON2 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 Th30:
theorem Th31:
theorem Th32:
theorem Th33:
theorem Th34:
theorem Th35:
theorem Th38:
theorem Th39:
theorem Th37:
theorem Th36:
theorem
begin
:: deftheorem SUM 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 Th50:
theorem Th51:
theorem Th59:
theorem Th52:
theorem Th53:
:: deftheorem CC 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 natural number st
( 0 in n & a = n *^ (exp omega ,b) ) );
definition
let a,
b be
ordinal number ;
func b -exponent a -> Ordinal means :
EXP:
(
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 ) )
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 ) )
consistency
for b1 being Ordinal holds verum
;
end;
:: deftheorem EXP 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 ) ) );
Lem0:
0 in 1
by NAT_1:45;
theorem Th41:
theorem Th42:
theorem Th43a:
theorem Th43b:
theorem Th43c:
theorem Th43:
theorem Th43d:
:: deftheorem CNF 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) ) ) );
theorem
theorem Th44:
theorem Th46:
theorem
theorem Th45:
theorem