:: Natural Addition of Ordinals
:: by Sebastian Koch
::
:: Received May 27, 2019
:: Copyright (c) 2019-2021 Association of Mizar Users


:: into ORDINAL1 ?
theorem Th1: :: ORDINAL7:1
for X being set holds X /\ (succ X) = X
proof end;

:: into ORDINAL2 ?
registration
let A be increasing Ordinal-Sequence;
let a be Ordinal;
cluster A | a -> increasing ;
coherence
A | a is increasing
proof end;
end;

Lm1: succ 0 = 1
;

Lm2: succ (succ 0) = 2
;

:: into ORDINAL2 ?
theorem Th2: :: ORDINAL7:2
for a being Ordinal holds a +^ a = 2 *^ a
proof end;

:: into ORDINAL2 ?
theorem :: ORDINAL7:3
for a, b being Ordinal st 1 in a & a in b holds
b +^ a in a *^ b
proof end;

:: into ORDINAL2 ?
theorem Th4: :: ORDINAL7:4
for a being Ordinal holds a *^ a = exp (a,2)
proof end;

:: into ORDINAL4 ?
theorem :: ORDINAL7:5
for a, b being Ordinal st 1 in a & a in b holds
a *^ b in exp (b,a)
proof end;

:: a |^|^ 2 = exp(a, a) is ORDINAL5:18
:: into ORDINAL5 ?
theorem :: ORDINAL7:6
for a, b being Ordinal st 1 in a & a in b holds
exp (b,a) in b |^|^ a
proof end;

registration
cluster Relation-like Function-like Sequence-like infinite Ordinal-yielding for set ;
existence
ex b1 being Ordinal-Sequence st b1 is infinite
proof end;
end;

Th9: for A, B being Sequence holds rng (A ^ B) = (rng A) \/ (rng B)
by ORDINAL4:2;

:: into ORDINAL4 ?
theorem Th10: :: ORDINAL7:7
for A, B being Sequence st A ^ B is Ordinal-yielding holds
( A is Ordinal-yielding & B is Ordinal-yielding )
proof end;

Th13: for D being set
for p being FinSequence of D
for n being Nat holds
( n + 1 in dom p iff n in dom (FS2XFS p) )

by AFINSQ_1:94;

Th15: for D being set
for p being FinSequence of D holds rng p = rng (FS2XFS p)

by AFINSQ_1:96;

Th19: for D being set
for p being one-to-one XFinSequence of D
for n being Nat holds rng (p | n) misses rng (p /^ n)

by AFINSQ_2:87;

:: into ORDINAL5 ?
:: corrolary from theorem above
theorem Th21: :: ORDINAL7:8
for a, b being Ordinal st a in b holds
b -exponent a = 0
proof end;

:: into ORDINAL5 ?
theorem Th22: :: ORDINAL7:9
for a, b, c being Ordinal st a c= c holds
b -exponent a c= b -exponent c
proof end;

:: into ORDINAL5 ?
theorem Th23: :: ORDINAL7:10
for a, b, c being Ordinal st 0 in a & 1 in b & a in exp (b,c) holds
b -exponent a in c
proof end;

:: into ORDINAL5 ?
registration
cluster Relation-like Function-like Sequence-like Ordinal-yielding decreasing -> one-to-one for set ;
coherence
for b1 being Ordinal-Sequence st b1 is decreasing holds
b1 is one-to-one
proof end;
end;

:: into ORDINAL5 ?
registration
let A be decreasing Sequence;
let a be Ordinal;
cluster A | a -> decreasing ;
coherence
A | a is decreasing
proof end;
end;

:: into ORDINAL5 ?
registration
let A be non-decreasing Sequence;
let a be Ordinal;
cluster A | a -> non-decreasing ;
coherence
A | a is non-decreasing
proof end;
end;

:: into ORDINAL5 ?
registration
let A be non-increasing Sequence;
let a be Ordinal;
cluster A | a -> non-increasing ;
coherence
A | a is non-increasing
proof end;
end;

:: into ORDINAL5 ?
theorem Th24: :: ORDINAL7:11
for A, B being finite Ordinal-Sequence holds Sum^ (A ^ B) = (Sum^ A) +^ (Sum^ B)
proof end;

:: into ORDINAL5 ?
theorem Th25: :: ORDINAL7:12
for a, b being Ordinal holds Sum^ <%a,b%> = a +^ b
proof end;

:: into ORDINAL5 ?
registration
let A be non-empty non empty finite Ordinal-Sequence;
cluster Sum^ A -> non empty ;
coherence
not Sum^ A is empty
proof end;
let B be finite Ordinal-Sequence;
cluster Sum^ (A ^ B) -> non empty ;
coherence
not Sum^ (A ^ B) is empty
proof end;
cluster Sum^ (B ^ A) -> non empty ;
coherence
not Sum^ (B ^ A) is empty
proof end;
end;

:: into ORDINAL5 ?
theorem Th26: :: ORDINAL7:13
for a being Ordinal
for n being Nat holds Sum^ (n --> a) = n *^ a
proof end;

Lm5: for n being Nat holds succ n = n + 1
proof end;

:: into ORDINAL5 ?
theorem Th27: :: ORDINAL7:14
for A being finite Ordinal-Sequence
for a being Ordinal holds Sum^ (A | a) c= Sum^ A
proof end;

:: into ORDINAL5 ?
theorem Th28: :: ORDINAL7:15
for A, B being finite Ordinal-Sequence st dom A c= dom B & ( for a being object st a in dom A holds
A . a c= B . a ) holds
Sum^ A c= Sum^ B
proof end;

:: into ORDINAL5 ?
:: the mirror theorem of ORDINAL5:67
theorem Th29: :: ORDINAL7:16
for A being Cantor-normal-form Ordinal-Sequence st A <> {} holds
ex B being Cantor-normal-form Ordinal-Sequence ex a being Cantor-component Ordinal st A = B ^ <%a%>
proof end;

:: into ORDINAL5 ?
registration
let A be Cantor-normal-form Ordinal-Sequence;
let n be Nat;
cluster A | n -> Cantor-normal-form ;
coherence
A | n is Cantor-normal-form
proof end;
end;

:: into ORDINAL5 or AFINSQ_2 ?
registration
let A be Cantor-normal-form Ordinal-Sequence;
let n be Nat;
cluster A /^ n -> Cantor-normal-form ;
coherence
A /^ n is Cantor-normal-form
proof end;
end;

registration
cluster Relation-like Function-like Sequence-like natural-valued -> Ordinal-yielding for set ;
coherence
for b1 being Sequence st b1 is natural-valued holds
b1 is Ordinal-yielding
proof end;
end;

registration
cluster limit_ordinal natural -> zero for set ;
coherence
for b1 being Nat st b1 is limit_ordinal holds
b1 is zero
;
cluster epsilon-transitive epsilon-connected ordinal non limit_ordinal V72() for set ;
existence
not for b1 being Ordinal holds b1 is limit_ordinal
proof end;
end;

registration
let n, m be Nat;
identify n \/ m with max (n,m);
correctness
compatibility
n \/ m = max (n,m)
;
proof end;
identify n /\ m with min (n,m);
correctness
compatibility
n /\ m = min (n,m)
;
proof end;
end;

:: absorption law of ordinal numbers
theorem Th30: :: ORDINAL7:17
for a, b being Ordinal holds
( a +^ b = b iff omega *^ a c= b )
proof end;

theorem Th31: :: ORDINAL7:18
for A being non empty Cantor-normal-form Ordinal-Sequence
for a being object st a in dom A holds
omega -exponent (last A) c= omega -exponent (A . a)
proof end;

theorem Th32: :: ORDINAL7:19
for A being non empty Cantor-normal-form Ordinal-Sequence
for a being object st a in dom A holds
omega -exponent (A . a) c= omega -exponent (A . 0)
proof end;

:: this implies ORDINAL5:68
theorem Th33: :: ORDINAL7:20
for A, B being non empty Cantor-normal-form Ordinal-Sequence st omega -exponent (B . 0) in omega -exponent (last A) holds
A ^ B is Cantor-normal-form
proof end;

Lm6: for A being decreasing Ordinal-Sequence
for n being Nat st len A = n + 1 holds
rng (A | n) = (rng A) \ {(A . n)}

proof end;

Lm7: for A, B being decreasing Ordinal-Sequence
for n being Nat st len A = n + 1 & rng A = rng B holds
A . n = B . n

proof end;

theorem Th34: :: ORDINAL7:21
for A, B being decreasing Ordinal-Sequence st rng A = rng B holds
A = B
proof end;

registration
let a be Ordinal;
cluster exp (omega,a) -> Cantor-component ;
coherence
exp (omega,a) is Cantor-component
proof end;
let n be non zero Nat;
cluster n *^ (exp (omega,a)) -> Cantor-component ;
coherence
n *^ (exp (omega,a)) is Cantor-component
proof end;
end;

registration
cluster natural non zero -> Cantor-component for set ;
coherence
for b1 being Nat st not b1 is zero holds
b1 is Cantor-component
proof end;
end;

registration
let c be Cantor-component Ordinal;
cluster <%c%> -> Cantor-normal-form ;
coherence
<%c%> is Cantor-normal-form
proof end;
end;

theorem Th35: :: ORDINAL7:22
for c, d being Cantor-component Ordinal st omega -exponent d in omega -exponent c holds
<%c,d%> is Cantor-normal-form
proof end;

Lm8: for a being non empty Ordinal
for n, m being non zero Nat holds <%(n *^ (exp (omega,a))),m%> is Cantor-normal-form

proof end;

registration
let a be non empty Ordinal;
let m be non zero Nat;
cluster <%(exp (omega,a)),m%> -> Cantor-normal-form ;
coherence
<%(exp (omega,a)),m%> is Cantor-normal-form
proof end;
let n be non zero Nat;
cluster <%(n *^ (exp (omega,a))),m%> -> Cantor-normal-form ;
coherence
<%(n *^ (exp (omega,a))),m%> is Cantor-normal-form
by Lm8;
end;

theorem :: ORDINAL7:23
for c, d, e being Cantor-component Ordinal st omega -exponent d in omega -exponent c & omega -exponent e in omega -exponent d holds
<%c,d,e%> is Cantor-normal-form
proof end;

theorem Th37: :: ORDINAL7:24
for A being non empty Cantor-normal-form Ordinal-Sequence
for b being Ordinal
for n being non zero Nat st b in omega -exponent (last A) holds
A ^ <%(n *^ (exp (omega,b)))%> is Cantor-normal-form
proof end;

theorem :: ORDINAL7:25
for A being non empty Cantor-normal-form Ordinal-Sequence
for b being Ordinal
for n being non zero Nat st omega -exponent (last A) <> 0 holds
A ^ <%n%> is Cantor-normal-form
proof end;

:: variant of ORDINAL5:68
theorem Th39: :: ORDINAL7:26
for A being non empty Cantor-normal-form Ordinal-Sequence
for b being Ordinal
for n being non zero Nat st omega -exponent (A . 0) in b holds
<%(n *^ (exp (omega,b)))%> ^ A is Cantor-normal-form
proof end;

:: closure of ordinal addition
theorem Th40: :: ORDINAL7:27
for a1, a2, b being Ordinal st a1 in exp (omega,b) & a2 in exp (omega,b) holds
a1 +^ a2 in exp (omega,b)
proof end;

theorem Th41: :: ORDINAL7:28
for A being finite Ordinal-Sequence
for b being Ordinal st ( for a being Ordinal st a in dom A holds
A . a in exp (omega,b) ) holds
Sum^ A in exp (omega,b)
proof end;

:: variant of ORDINAL5:7
theorem Th42: :: ORDINAL7:29
for a, b being Ordinal
for n being Nat st a in exp (omega,b) holds
n *^ a in exp (omega,b)
proof end;

theorem Th43: :: ORDINAL7:30
for A being finite Ordinal-Sequence
for a being Ordinal st <%a%> ^ A is Cantor-normal-form holds
Sum^ A in exp (omega,(omega -exponent a))
proof end;

theorem Th44: :: ORDINAL7:31
for A being Cantor-normal-form Ordinal-Sequence holds omega -exponent (Sum^ A) = omega -exponent (A . 0)
proof end;

theorem Th45: :: ORDINAL7:32
for A, B being Cantor-normal-form Ordinal-Sequence st Sum^ A = Sum^ B holds
A = B
proof end;

definition
let A be Ordinal-Sequence;
let b be Ordinal;
func b -exponent A -> Ordinal-Sequence means :Def1: :: ORDINAL7:def 1
( dom it = dom A & ( for a being object st a in dom A holds
it . a = b -exponent (A . a) ) );
existence
ex b1 being Ordinal-Sequence st
( dom b1 = dom A & ( for a being object st a in dom A holds
b1 . a = b -exponent (A . a) ) )
proof end;
uniqueness
for b1, b2 being Ordinal-Sequence st dom b1 = dom A & ( for a being object st a in dom A holds
b1 . a = b -exponent (A . a) ) & dom b2 = dom A & ( for a being object st a in dom A holds
b2 . a = b -exponent (A . a) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines -exponent ORDINAL7:def 1 :
for A being Ordinal-Sequence
for b being Ordinal
for b3 being Ordinal-Sequence holds
( b3 = b -exponent A iff ( dom b3 = dom A & ( for a being object st a in dom A holds
b3 . a = b -exponent (A . a) ) ) );

registration
let A be empty Ordinal-Sequence;
let b be Ordinal;
cluster b -exponent A -> empty ;
coherence
b -exponent A is empty
proof end;
end;

registration
let A be non empty Ordinal-Sequence;
let b be Ordinal;
cluster b -exponent A -> non empty ;
coherence
not b -exponent A is empty
proof end;
end;

registration
let A be finite Ordinal-Sequence;
let b be Ordinal;
cluster b -exponent A -> finite ;
coherence
b -exponent A is finite
proof end;
end;

registration
let A be infinite Ordinal-Sequence;
let b be Ordinal;
cluster b -exponent A -> infinite ;
coherence
not b -exponent A is finite
proof end;
end;

theorem Th46: :: ORDINAL7:33
for a, b being Ordinal holds b -exponent <%a%> = <%(b -exponent a)%>
proof end;

theorem Th47: :: ORDINAL7:34
for A, B being Ordinal-Sequence
for b being Ordinal holds b -exponent (A ^ B) = (b -exponent A) ^ (b -exponent B)
proof end;

theorem Th48: :: ORDINAL7:35
for A being Ordinal-Sequence
for b, c being Ordinal holds b -exponent (A | c) = (b -exponent A) | c
proof end;

theorem Th49: :: ORDINAL7:36
for A being finite Ordinal-Sequence
for b being Ordinal
for n being Nat holds b -exponent (A /^ n) = (b -exponent A) /^ n
proof end;

registration
let A be Cantor-normal-form Ordinal-Sequence;
cluster omega -exponent A -> decreasing ;
coherence
omega -exponent A is decreasing
proof end;
end;

theorem :: ORDINAL7:37
for A, B being Ordinal-Sequence st A ^ B is Cantor-normal-form holds
rng (omega -exponent A) misses rng (omega -exponent B)
proof end;

theorem Th51: :: ORDINAL7:38
for A being Cantor-normal-form Ordinal-Sequence holds
( 0 in rng (omega -exponent A) iff ( A <> {} & omega -exponent (last A) = 0 ) )
proof end;

definition
let a, b be Ordinal;
func b -leading_coeff a -> Ordinal equals :: ORDINAL7:def 2
a div^ (exp (b,(b -exponent a)));
coherence
a div^ (exp (b,(b -exponent a))) is Ordinal
;
end;

:: deftheorem defines -leading_coeff ORDINAL7:def 2 :
for a, b being Ordinal holds b -leading_coeff a = a div^ (exp (b,(b -exponent a)));

:: This is the undefined case. One could have set the value simply to 0
:: in case that b = 0 just as well.
theorem Th52: :: ORDINAL7:39
for a being Ordinal holds 0 -leading_coeff a = a
proof end;

:: this means that a = a *^ exp(1,0)
theorem Th53: :: ORDINAL7:40
for a being Ordinal holds 1 -leading_coeff a = a
proof end;

:: this means that 0 = 0 *^ exp(b,0)
theorem :: ORDINAL7:41
for b being Ordinal holds b -leading_coeff 0 = 0 by ORDINAL3:70;

:: this means that a = a *^ exp(b,0)
theorem Th55: :: ORDINAL7:42
for a, b being Ordinal st a in b holds
b -leading_coeff a = a
proof end;

:: this means that 1 = 1 *^ exp(b,0)
theorem :: ORDINAL7:43
for b being Ordinal holds b -leading_coeff 1 = 1
proof end;

theorem Th57: :: ORDINAL7:44
for a, b, c being Ordinal st c in b holds
b -leading_coeff (c *^ (exp (b,a))) = c
proof end;

theorem :: ORDINAL7:45
for a, b being Ordinal st 1 in b holds
b -leading_coeff (exp (b,a)) = 1
proof end;

registration
let c be Cantor-component Ordinal;
cluster omega -leading_coeff c -> non empty natural ;
coherence
( omega -leading_coeff c is natural & not omega -leading_coeff c is empty )
proof end;
end;

theorem Th59: :: ORDINAL7:46
for c being Cantor-component Ordinal holds c = (omega -leading_coeff c) *^ (exp (omega,(omega -exponent c)))
proof end;

definition
let A be Ordinal-Sequence;
let b be Ordinal;
func b -leading_coeff A -> Ordinal-Sequence means :Def3: :: ORDINAL7:def 3
( dom it = dom A & ( for a being object st a in dom A holds
it . a = b -leading_coeff (A . a) ) );
existence
ex b1 being Ordinal-Sequence st
( dom b1 = dom A & ( for a being object st a in dom A holds
b1 . a = b -leading_coeff (A . a) ) )
proof end;
uniqueness
for b1, b2 being Ordinal-Sequence st dom b1 = dom A & ( for a being object st a in dom A holds
b1 . a = b -leading_coeff (A . a) ) & dom b2 = dom A & ( for a being object st a in dom A holds
b2 . a = b -leading_coeff (A . a) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def3 defines -leading_coeff ORDINAL7:def 3 :
for A being Ordinal-Sequence
for b being Ordinal
for b3 being Ordinal-Sequence holds
( b3 = b -leading_coeff A iff ( dom b3 = dom A & ( for a being object st a in dom A holds
b3 . a = b -leading_coeff (A . a) ) ) );

registration
let A be empty Ordinal-Sequence;
let b be Ordinal;
cluster b -leading_coeff A -> empty ;
coherence
b -leading_coeff A is empty
proof end;
end;

registration
let A be non empty Ordinal-Sequence;
let b be Ordinal;
cluster b -leading_coeff A -> non empty ;
coherence
not b -leading_coeff A is empty
proof end;
end;

registration
let A be finite Ordinal-Sequence;
let b be Ordinal;
cluster b -leading_coeff A -> finite ;
coherence
b -leading_coeff A is finite
proof end;
end;

registration
let A be infinite Ordinal-Sequence;
let b be Ordinal;
cluster b -leading_coeff A -> infinite ;
coherence
not b -leading_coeff A is finite
proof end;
end;

theorem Th60: :: ORDINAL7:47
for a, b being Ordinal holds b -leading_coeff <%a%> = <%(b -leading_coeff a)%>
proof end;

theorem :: ORDINAL7:48
for A, B being Ordinal-Sequence
for b being Ordinal holds b -leading_coeff (A ^ B) = (b -leading_coeff A) ^ (b -leading_coeff B)
proof end;

theorem :: ORDINAL7:49
for A being Ordinal-Sequence
for b, c being Ordinal holds b -leading_coeff (A | c) = (b -leading_coeff A) | c
proof end;

theorem :: ORDINAL7:50
for A being finite Ordinal-Sequence
for b being Ordinal
for n being Nat holds b -leading_coeff (A /^ n) = (b -leading_coeff A) /^ n
proof end;

registration
let A be Cantor-normal-form Ordinal-Sequence;
let a be object ;
cluster (omega -leading_coeff A) . a -> natural ;
coherence
(omega -leading_coeff A) . a is natural
proof end;
end;

registration
let A be Cantor-normal-form Ordinal-Sequence;
cluster omega -leading_coeff A -> non-empty natural-valued ;
coherence
( omega -leading_coeff A is natural-valued & omega -leading_coeff A is non-empty )
proof end;
end;

theorem Th64: :: ORDINAL7:51
for A being Cantor-normal-form Ordinal-Sequence
for a being object st a in dom A holds
A . a = (omega -leading_coeff (A . a)) *^ (exp (omega,(omega -exponent (A . a))))
proof end;

theorem Th65: :: ORDINAL7:52
for A being Cantor-normal-form Ordinal-Sequence
for a being object st a in dom A holds
A . a = ((omega -leading_coeff A) . a) *^ (exp (omega,((omega -exponent A) . a)))
proof end;

theorem Th66: :: ORDINAL7:53
for A being decreasing Ordinal-Sequence
for B being non-empty natural-valued Ordinal-Sequence st dom A = dom B holds
ex C being Cantor-normal-form Ordinal-Sequence st
( omega -exponent C = A & omega -leading_coeff C = B )
proof end;

theorem Th67: :: ORDINAL7:54
for A, B being Cantor-normal-form Ordinal-Sequence st omega -exponent A = omega -exponent B & omega -leading_coeff A = omega -leading_coeff B holds
A = B
proof end;

definition
let a be Ordinal;
func CantorNF a -> Cantor-normal-form Ordinal-Sequence means :Def4: :: ORDINAL7:def 4
Sum^ it = a;
existence
ex b1 being Cantor-normal-form Ordinal-Sequence st Sum^ b1 = a
by ORDINAL5:69;
uniqueness
for b1, b2 being Cantor-normal-form Ordinal-Sequence st Sum^ b1 = a & Sum^ b2 = a holds
b1 = b2
by Th45;
end;

:: deftheorem Def4 defines CantorNF ORDINAL7:def 4 :
for a being Ordinal
for b2 being Cantor-normal-form Ordinal-Sequence holds
( b2 = CantorNF a iff Sum^ b2 = a );

registration
let a be Ordinal;
reduce Sum^ (CantorNF a) to a;
correctness
reducibility
Sum^ (CantorNF a) = a
;
by Def4;
end;

registration
let A be Cantor-normal-form Ordinal-Sequence;
reduce CantorNF (Sum^ A) to A;
correctness
reducibility
CantorNF (Sum^ A) = A
;
by Def4;
end;

theorem :: ORDINAL7:55
CantorNF {} = {} by ORDINAL5:52;

registration
let a be empty Ordinal;
cluster CantorNF a -> empty Cantor-normal-form ;
coherence
CantorNF a is empty
by ORDINAL5:52;
end;

registration
let a be non empty Ordinal;
cluster CantorNF a -> non empty Cantor-normal-form ;
coherence
not CantorNF a is empty
by ORDINAL5:52;
end;

theorem Th69: :: ORDINAL7:56
for a being Ordinal
for n being non zero Nat holds CantorNF (n *^ (exp (omega,a))) = <%(n *^ (exp (omega,a)))%>
proof end;

theorem Th70: :: ORDINAL7:57
for a being Cantor-component Ordinal holds CantorNF a = <%a%>
proof end;

theorem Th71: :: ORDINAL7:58
for n being non zero Nat holds CantorNF n = <%n%>
proof end;

theorem :: ORDINAL7:59
for a being non empty Ordinal
for n, m being non zero Nat holds CantorNF ((n *^ (exp (omega,a))) +^ m) = <%(n *^ (exp (omega,a))),m%>
proof end;

theorem Th73: :: ORDINAL7:60
for a being non empty Ordinal
for b being Ordinal
for n being non zero Nat st b in omega -exponent (last (CantorNF a)) holds
CantorNF (a +^ (n *^ (exp (omega,b)))) = (CantorNF a) ^ <%(n *^ (exp (omega,b)))%>
proof end;

theorem :: ORDINAL7:61
for a being non empty Ordinal
for n being non zero Nat st omega -exponent (last (CantorNF a)) <> 0 holds
CantorNF (a +^ n) = (CantorNF a) ^ <%n%>
proof end;

theorem :: ORDINAL7:62
for a being non empty Ordinal
for b being Ordinal
for n being non zero Nat st omega -exponent ((CantorNF a) . 0) in b holds
CantorNF ((n *^ (exp (omega,b))) +^ a) = <%(n *^ (exp (omega,b)))%> ^ (CantorNF a)
proof end;

definition
let a, b be Ordinal;
func a (+) b -> Ordinal means :Def5: :: ORDINAL7:def 5
ex C being Cantor-normal-form Ordinal-Sequence st
( it = Sum^ C & rng (omega -exponent C) = (rng (omega -exponent (CantorNF a))) \/ (rng (omega -exponent (CantorNF b))) & ( for d being object st d in dom C holds
( ( omega -exponent (C . d) in (rng (omega -exponent (CantorNF a))) \ (rng (omega -exponent (CantorNF b))) implies omega -leading_coeff (C . d) = (omega -leading_coeff (CantorNF a)) . (((omega -exponent (CantorNF a)) ") . (omega -exponent (C . d))) ) & ( omega -exponent (C . d) in (rng (omega -exponent (CantorNF b))) \ (rng (omega -exponent (CantorNF a))) implies omega -leading_coeff (C . d) = (omega -leading_coeff (CantorNF b)) . (((omega -exponent (CantorNF b)) ") . (omega -exponent (C . d))) ) & ( omega -exponent (C . d) in (rng (omega -exponent (CantorNF a))) /\ (rng (omega -exponent (CantorNF b))) implies omega -leading_coeff (C . d) = ((omega -leading_coeff (CantorNF a)) . (((omega -exponent (CantorNF a)) ") . (omega -exponent (C . d)))) + ((omega -leading_coeff (CantorNF b)) . (((omega -exponent (CantorNF b)) ") . (omega -exponent (C . d)))) ) ) ) );
existence
ex b1 being Ordinal ex C being Cantor-normal-form Ordinal-Sequence st
( b1 = Sum^ C & rng (omega -exponent C) = (rng (omega -exponent (CantorNF a))) \/ (rng (omega -exponent (CantorNF b))) & ( for d being object st d in dom C holds
( ( omega -exponent (C . d) in (rng (omega -exponent (CantorNF a))) \ (rng (omega -exponent (CantorNF b))) implies omega -leading_coeff (C . d) = (omega -leading_coeff (CantorNF a)) . (((omega -exponent (CantorNF a)) ") . (omega -exponent (C . d))) ) & ( omega -exponent (C . d) in (rng (omega -exponent (CantorNF b))) \ (rng (omega -exponent (CantorNF a))) implies omega -leading_coeff (C . d) = (omega -leading_coeff (CantorNF b)) . (((omega -exponent (CantorNF b)) ") . (omega -exponent (C . d))) ) & ( omega -exponent (C . d) in (rng (omega -exponent (CantorNF a))) /\ (rng (omega -exponent (CantorNF b))) implies omega -leading_coeff (C . d) = ((omega -leading_coeff (CantorNF a)) . (((omega -exponent (CantorNF a)) ") . (omega -exponent (C . d)))) + ((omega -leading_coeff (CantorNF b)) . (((omega -exponent (CantorNF b)) ") . (omega -exponent (C . d)))) ) ) ) )
proof end;
uniqueness
for b1, b2 being Ordinal st ex C being Cantor-normal-form Ordinal-Sequence st
( b1 = Sum^ C & rng (omega -exponent C) = (rng (omega -exponent (CantorNF a))) \/ (rng (omega -exponent (CantorNF b))) & ( for d being object st d in dom C holds
( ( omega -exponent (C . d) in (rng (omega -exponent (CantorNF a))) \ (rng (omega -exponent (CantorNF b))) implies omega -leading_coeff (C . d) = (omega -leading_coeff (CantorNF a)) . (((omega -exponent (CantorNF a)) ") . (omega -exponent (C . d))) ) & ( omega -exponent (C . d) in (rng (omega -exponent (CantorNF b))) \ (rng (omega -exponent (CantorNF a))) implies omega -leading_coeff (C . d) = (omega -leading_coeff (CantorNF b)) . (((omega -exponent (CantorNF b)) ") . (omega -exponent (C . d))) ) & ( omega -exponent (C . d) in (rng (omega -exponent (CantorNF a))) /\ (rng (omega -exponent (CantorNF b))) implies omega -leading_coeff (C . d) = ((omega -leading_coeff (CantorNF a)) . (((omega -exponent (CantorNF a)) ") . (omega -exponent (C . d)))) + ((omega -leading_coeff (CantorNF b)) . (((omega -exponent (CantorNF b)) ") . (omega -exponent (C . d)))) ) ) ) ) & ex C being Cantor-normal-form Ordinal-Sequence st
( b2 = Sum^ C & rng (omega -exponent C) = (rng (omega -exponent (CantorNF a))) \/ (rng (omega -exponent (CantorNF b))) & ( for d being object st d in dom C holds
( ( omega -exponent (C . d) in (rng (omega -exponent (CantorNF a))) \ (rng (omega -exponent (CantorNF b))) implies omega -leading_coeff (C . d) = (omega -leading_coeff (CantorNF a)) . (((omega -exponent (CantorNF a)) ") . (omega -exponent (C . d))) ) & ( omega -exponent (C . d) in (rng (omega -exponent (CantorNF b))) \ (rng (omega -exponent (CantorNF a))) implies omega -leading_coeff (C . d) = (omega -leading_coeff (CantorNF b)) . (((omega -exponent (CantorNF b)) ") . (omega -exponent (C . d))) ) & ( omega -exponent (C . d) in (rng (omega -exponent (CantorNF a))) /\ (rng (omega -exponent (CantorNF b))) implies omega -leading_coeff (C . d) = ((omega -leading_coeff (CantorNF a)) . (((omega -exponent (CantorNF a)) ") . (omega -exponent (C . d)))) + ((omega -leading_coeff (CantorNF b)) . (((omega -exponent (CantorNF b)) ") . (omega -exponent (C . d)))) ) ) ) ) holds
b1 = b2
proof end;
commutativity
for b1, a, b being Ordinal st ex C being Cantor-normal-form Ordinal-Sequence st
( b1 = Sum^ C & rng (omega -exponent C) = (rng (omega -exponent (CantorNF a))) \/ (rng (omega -exponent (CantorNF b))) & ( for d being object st d in dom C holds
( ( omega -exponent (C . d) in (rng (omega -exponent (CantorNF a))) \ (rng (omega -exponent (CantorNF b))) implies omega -leading_coeff (C . d) = (omega -leading_coeff (CantorNF a)) . (((omega -exponent (CantorNF a)) ") . (omega -exponent (C . d))) ) & ( omega -exponent (C . d) in (rng (omega -exponent (CantorNF b))) \ (rng (omega -exponent (CantorNF a))) implies omega -leading_coeff (C . d) = (omega -leading_coeff (CantorNF b)) . (((omega -exponent (CantorNF b)) ") . (omega -exponent (C . d))) ) & ( omega -exponent (C . d) in (rng (omega -exponent (CantorNF a))) /\ (rng (omega -exponent (CantorNF b))) implies omega -leading_coeff (C . d) = ((omega -leading_coeff (CantorNF a)) . (((omega -exponent (CantorNF a)) ") . (omega -exponent (C . d)))) + ((omega -leading_coeff (CantorNF b)) . (((omega -exponent (CantorNF b)) ") . (omega -exponent (C . d)))) ) ) ) ) holds
ex C being Cantor-normal-form Ordinal-Sequence st
( b1 = Sum^ C & rng (omega -exponent C) = (rng (omega -exponent (CantorNF b))) \/ (rng (omega -exponent (CantorNF a))) & ( for d being object st d in dom C holds
( ( omega -exponent (C . d) in (rng (omega -exponent (CantorNF b))) \ (rng (omega -exponent (CantorNF a))) implies omega -leading_coeff (C . d) = (omega -leading_coeff (CantorNF b)) . (((omega -exponent (CantorNF b)) ") . (omega -exponent (C . d))) ) & ( omega -exponent (C . d) in (rng (omega -exponent (CantorNF a))) \ (rng (omega -exponent (CantorNF b))) implies omega -leading_coeff (C . d) = (omega -leading_coeff (CantorNF a)) . (((omega -exponent (CantorNF a)) ") . (omega -exponent (C . d))) ) & ( omega -exponent (C . d) in (rng (omega -exponent (CantorNF b))) /\ (rng (omega -exponent (CantorNF a))) implies omega -leading_coeff (C . d) = ((omega -leading_coeff (CantorNF b)) . (((omega -exponent (CantorNF b)) ") . (omega -exponent (C . d)))) + ((omega -leading_coeff (CantorNF a)) . (((omega -exponent (CantorNF a)) ") . (omega -exponent (C . d)))) ) ) ) )
proof end;
end;

:: deftheorem Def5 defines (+) ORDINAL7:def 5 :
for a, b, b3 being Ordinal holds
( b3 = a (+) b iff ex C being Cantor-normal-form Ordinal-Sequence st
( b3 = Sum^ C & rng (omega -exponent C) = (rng (omega -exponent (CantorNF a))) \/ (rng (omega -exponent (CantorNF b))) & ( for d being object st d in dom C holds
( ( omega -exponent (C . d) in (rng (omega -exponent (CantorNF a))) \ (rng (omega -exponent (CantorNF b))) implies omega -leading_coeff (C . d) = (omega -leading_coeff (CantorNF a)) . (((omega -exponent (CantorNF a)) ") . (omega -exponent (C . d))) ) & ( omega -exponent (C . d) in (rng (omega -exponent (CantorNF b))) \ (rng (omega -exponent (CantorNF a))) implies omega -leading_coeff (C . d) = (omega -leading_coeff (CantorNF b)) . (((omega -exponent (CantorNF b)) ") . (omega -exponent (C . d))) ) & ( omega -exponent (C . d) in (rng (omega -exponent (CantorNF a))) /\ (rng (omega -exponent (CantorNF b))) implies omega -leading_coeff (C . d) = ((omega -leading_coeff (CantorNF a)) . (((omega -exponent (CantorNF a)) ") . (omega -exponent (C . d)))) + ((omega -leading_coeff (CantorNF b)) . (((omega -exponent (CantorNF b)) ") . (omega -exponent (C . d)))) ) ) ) ) );

theorem Th76: :: ORDINAL7:63
for a, b being Ordinal holds rng (omega -exponent (CantorNF (a (+) b))) = (rng (omega -exponent (CantorNF a))) \/ (rng (omega -exponent (CantorNF b)))
proof end;

theorem Th77: :: ORDINAL7:64
for a, b being Ordinal holds dom (CantorNF a) c= dom (CantorNF (a (+) b))
proof end;

theorem Th78: :: ORDINAL7:65
for a, b being Ordinal
for d being object st d in dom (CantorNF (a (+) b)) & omega -exponent ((CantorNF (a (+) b)) . d) in (rng (omega -exponent (CantorNF a))) \ (rng (omega -exponent (CantorNF b))) holds
omega -leading_coeff ((CantorNF (a (+) b)) . d) = (omega -leading_coeff (CantorNF a)) . (((omega -exponent (CantorNF a)) ") . (omega -exponent ((CantorNF (a (+) b)) . d)))
proof end;

theorem Th79: :: ORDINAL7:66
for a, b being Ordinal
for d being object st d in dom (CantorNF (a (+) b)) & omega -exponent ((CantorNF (a (+) b)) . d) in (rng (omega -exponent (CantorNF b))) \ (rng (omega -exponent (CantorNF a))) holds
omega -leading_coeff ((CantorNF (a (+) b)) . d) = (omega -leading_coeff (CantorNF b)) . (((omega -exponent (CantorNF b)) ") . (omega -exponent ((CantorNF (a (+) b)) . d))) by Th78;

theorem Th80: :: ORDINAL7:67
for a, b being Ordinal
for d being object st d in dom (CantorNF (a (+) b)) & omega -exponent ((CantorNF (a (+) b)) . d) in (rng (omega -exponent (CantorNF a))) /\ (rng (omega -exponent (CantorNF b))) holds
omega -leading_coeff ((CantorNF (a (+) b)) . d) = ((omega -leading_coeff (CantorNF a)) . (((omega -exponent (CantorNF a)) ") . (omega -exponent ((CantorNF (a (+) b)) . d)))) + ((omega -leading_coeff (CantorNF b)) . (((omega -exponent (CantorNF b)) ") . (omega -exponent ((CantorNF (a (+) b)) . d))))
proof end;

theorem Th81: :: ORDINAL7:68
for a, b, c being Ordinal holds (a (+) b) (+) c = a (+) (b (+) c)
proof end;

theorem Th82: :: ORDINAL7:69
for a being Ordinal holds a (+) 0 = a
proof end;

theorem Th83: :: ORDINAL7:70
for a, b being Ordinal
for n being Nat st omega -exponent a c= b holds
(n *^ (exp (omega,b))) (+) a = (n *^ (exp (omega,b))) +^ a
proof end;

theorem Th84: :: ORDINAL7:71
for A, B being finite Ordinal-Sequence st A ^ B is Cantor-normal-form holds
(Sum^ A) (+) (Sum^ B) = (Sum^ A) +^ (Sum^ B)
proof end;

theorem Th85: :: ORDINAL7:72
for a, b being Ordinal st ( a <> 0 implies omega -exponent b in omega -exponent (last (CantorNF a)) ) holds
a (+) b = a +^ b
proof end;

theorem Th86: :: ORDINAL7:73
for a, b being Ordinal
for n being Nat st ( a <> 0 implies b c= omega -exponent (last (CantorNF a)) ) holds
a (+) (n *^ (exp (omega,b))) = a +^ (n *^ (exp (omega,b)))
proof end;

theorem :: ORDINAL7:74
for a being Ordinal
for n, m being Nat holds (n *^ (exp (omega,a))) (+) (m *^ (exp (omega,a))) = (n + m) *^ (exp (omega,a))
proof end;

theorem Th88: :: ORDINAL7:75
for a being Ordinal
for n being Nat holds a (+) n = a +^ n
proof end;

theorem Th89: :: ORDINAL7:76
for n, m being Nat holds n (+) m = n + m
proof end;

registration
let n, m be Nat;
identify n (+) m with n + m;
correctness
compatibility
n (+) m = n + m
;
by Th89;
end;

theorem Th90: :: ORDINAL7:77
for a being Ordinal holds a (+) 1 = succ a
proof end;

theorem :: ORDINAL7:78
for a, b being Ordinal holds a (+) (succ b) = succ (a (+) b)
proof end;

registration
let a be empty Ordinal;
cluster a (+) a -> empty ;
coherence
a (+) a is empty
;
end;

registration
let a be non empty Ordinal;
let b be Ordinal;
cluster a (+) b -> non empty ;
coherence
not a (+) b is empty
proof end;
end;

theorem Th92: :: ORDINAL7:79
for a being Ordinal holds
( a is limit_ordinal iff not 0 in rng (omega -exponent (CantorNF a)) )
proof end;

registration
let a, b be limit_ordinal Ordinal;
cluster a (+) b -> limit_ordinal ;
coherence
a (+) b is limit_ordinal
proof end;
end;

registration
let a be Ordinal;
let b be non limit_ordinal Ordinal;
cluster a (+) b -> non limit_ordinal ;
coherence
not a (+) b is limit_ordinal
proof end;
end;

theorem :: ORDINAL7:80
for a, b being Ordinal
for n being non zero Nat st n *^ (exp (omega,b)) c= a & a in (n + 1) *^ (exp (omega,b)) holds
(CantorNF a) . 0 = n *^ (exp (omega,b))
proof end;

theorem :: ORDINAL7:81
for a, b being Ordinal st rng (omega -exponent (CantorNF a)) = rng (omega -exponent (CantorNF b)) holds
for c being Ordinal st c in dom (CantorNF a) holds
(omega -leading_coeff (CantorNF (a (+) b))) . c = ((omega -leading_coeff (CantorNF a)) . c) + ((omega -leading_coeff (CantorNF b)) . c)
proof end;

theorem Th95: :: ORDINAL7:82
for a, b being Ordinal holds
( ( omega -exponent ((CantorNF (a (+) b)) . 0) in rng (omega -exponent (CantorNF a)) implies omega -exponent ((CantorNF (a (+) b)) . 0) = (omega -exponent (CantorNF a)) . 0 ) & ( omega -exponent ((CantorNF (a (+) b)) . 0) in rng (omega -exponent (CantorNF b)) implies omega -exponent ((CantorNF (a (+) b)) . 0) = (omega -exponent (CantorNF b)) . 0 ) )
proof end;

theorem :: ORDINAL7:83
for a, b being Ordinal holds
( ( omega -exponent ((CantorNF (a (+) b)) . 0) in (rng (omega -exponent (CantorNF a))) \ (rng (omega -exponent (CantorNF b))) implies (CantorNF (a (+) b)) . 0 = (CantorNF a) . 0 ) & ( omega -exponent ((CantorNF (a (+) b)) . 0) in (rng (omega -exponent (CantorNF b))) \ (rng (omega -exponent (CantorNF a))) implies (CantorNF (a (+) b)) . 0 = (CantorNF b) . 0 ) & ( omega -exponent ((CantorNF (a (+) b)) . 0) in (rng (omega -exponent (CantorNF a))) /\ (rng (omega -exponent (CantorNF b))) implies (CantorNF (a (+) b)) . 0 = ((CantorNF a) . 0) +^ ((CantorNF b) . 0) ) )
proof end;

theorem Th97: :: ORDINAL7:84
for a, b being Ordinal
for x being object holds (omega -exponent (CantorNF a)) . x c= (omega -exponent (CantorNF (a (+) b))) . x
proof end;

theorem Th98: :: ORDINAL7:85
for a, b being Ordinal
for x being object holds (CantorNF a) . x c= (CantorNF (a (+) b)) . x
proof end;

theorem Th99: :: ORDINAL7:86
for a, b being Ordinal holds a c= a (+) b
proof end;

theorem Th100: :: ORDINAL7:87
for a, b being Ordinal holds omega -exponent (a (+) b) = (omega -exponent a) \/ (omega -exponent b)
proof end;

:: closure of natural addition
theorem Th101: :: ORDINAL7:88
for a, b, c being Ordinal st a in exp (omega,c) & b in exp (omega,c) holds
a (+) b in exp (omega,c)
proof end;

Lm9: for a being Ordinal
for n being Nat holds (n *^ (exp (omega,a))) +^ (exp (omega,a)) = (n *^ (exp (omega,a))) (+) (exp (omega,a))

proof end;

scheme :: ORDINAL7:sch 1
OrdinalCNFIndA{ P1[ non empty Ordinal] } :
for a being non empty Ordinal holds P1[a]
provided
A1: for a being Ordinal
for n being non zero Nat holds P1[n *^ (exp (omega,a))] and
A2: for a being Ordinal
for b being non empty Ordinal
for n being non zero Nat st P1[b] & not a in rng (omega -exponent (CantorNF b)) holds
P1[b (+) (n *^ (exp (omega,a)))]
proof end;

scheme :: ORDINAL7:sch 2
OrdinalCNFIndB{ P1[ non empty Ordinal] } :
for a being non empty Ordinal holds P1[a]
provided
A1: for a being Ordinal holds P1[ exp (omega,a)] and
A2: for a being Ordinal
for n being non zero Nat st P1[n *^ (exp (omega,a))] holds
P1[(n + 1) *^ (exp (omega,a))] and
A3: for a being Ordinal
for b being non empty Ordinal
for n being non zero Nat st P1[b] & not a in rng (omega -exponent (CantorNF b)) holds
P1[b (+) (n *^ (exp (omega,a)))]
proof end;

scheme :: ORDINAL7:sch 3
OrdinalCNFIndC{ P1[ non empty Ordinal] } :
for a being non empty Ordinal holds P1[a]
provided
A1: for a being Ordinal holds P1[ exp (omega,a)] and
A2: for a being Ordinal
for b being non empty Ordinal st P1[b] holds
P1[b (+) (exp (omega,a))]
proof end;

theorem Th102: :: ORDINAL7:89
for a, b being Ordinal st omega -exponent a in omega -exponent b holds
a in exp (omega,(omega -exponent b))
proof end;

theorem Th103: :: ORDINAL7:90
for a, b being non empty Ordinal holds
( omega *^ a c= b iff omega -exponent a in omega -exponent b )
proof end;

theorem :: ORDINAL7:91
for a, b being Ordinal st omega -exponent a in omega -exponent b holds
b -^ a = b
proof end;

theorem :: ORDINAL7:92
for a, b being Ordinal holds a +^ b c= a (+) b
proof end;

:: cancelling rule for natural addition
theorem :: ORDINAL7:93
for a, b, c being Ordinal st a (+) b = a (+) c holds
b = c
proof end;

Lm10: for A being Cantor-normal-form Ordinal-Sequence holds omega -exponent A is XFinSequence of sup (omega -exponent A)
proof end;

Lm11: for a being non empty Ordinal
for b, c being Ordinal st b in c & (CantorNF b) . 0 <> (CantorNF c) . 0 holds
a (+) b in a (+) c

proof end;

:: monotonicity of natural addition
theorem Th107: :: ORDINAL7:94
for a, b, c being Ordinal st b in c holds
a (+) b in a (+) c
proof end;

theorem :: ORDINAL7:95
for a, b, c being Ordinal st b c= c holds
a (+) b c= a (+) c
proof end;