begin
theorem Th001:
theorem Th65:
theorem ThS1:
theorem ThS2:
:: deftheorem defines decreasing ORDINAL5:def 1 :
:: deftheorem ND defines non-decreasing ORDINAL5:def 2 :
:: deftheorem defines non-increasing ORDINAL5:def 3 :
theorem ThO:
theorem ThND:
theorem
theorem Th003:
theorem Th002:
theorem
theorem Th005:
theorem Th006:
begin
:: deftheorem KNUTH defines |^|^ ORDINAL5:def 4 :
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 :
theorem ThE0:
:: deftheorem FEGT defines first_epsilon_greater_than ORDINAL5:def 6 :
theorem
theorem
theorem Th20:
theorem Th21:
theorem Th22:
theorem Th23:
theorem Th24:
:: deftheorem EPSILON2 defines epsilon_ ORDINAL5:def 7 :
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 :
theorem Th50:
theorem Th51:
theorem Th59:
theorem Th52:
theorem Th53:
:: deftheorem CC defines Cantor-component ORDINAL5:def 9 :
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 :
theorem Th41:
theorem Th42:
theorem Th43a:
theorem Th43b:
theorem Th43c:
theorem Th43:
theorem Th43d:
:: deftheorem CNF defines Cantor-normal-form ORDINAL5:def 11 :
theorem
theorem Th44:
theorem Th46:
theorem
theorem Th45:
theorem