:: Natural Addition of Ordinals
::  by Sebastian Koch
:: 
:: Received May 27, 2019
:: Copyright (c) 2019-2021 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies NUMBERS, ORDINAL1, ORDINAL2, TARSKI, XBOOLE_0, CARD_1, FINSET_1,
      AFINSQ_1, ORDINAL4, RELAT_1, FUNCT_1, VALUED_0, SUBSET_1, ARYTM_3, NAT_1,
      XXREAL_0, ORDINAL3, FINSEQ_1, ORDINAL5, WELLORD2, STRUCT_0, ORDERS_2,
      ORDERS_5, PRGCOR_2, PARTFUN1, ARYTM_1, XCMPLX_0, FUNCOP_1, CARD_2,
      RFINSEQ, MATHMORP, ORDINAL7;
 notations TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, PARTFUN1,
      WELLORD2, FUNCOP_1, ORDINAL2, ORDINAL3, FINSET_1, CARD_1, ORDERS_1,
      CARD_3, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, NAT_1, VALUED_0, CARD_2,
      NAT_D, ORDINAL4, FINSEQ_1, NEWTON, RFINSEQ, AFINSQ_1, AFINSQ_2, ORDINAL5,
      ORDINAL6, STRUCT_0, ORDERS_2, ORDERS_5;
 constructors NEWTON, NAT_1, AFINSQ_1, ORDINAL3, CARD_3, NUMBERS, ORDINAL5,
      ORDINAL6, WELLORD2, STRUCT_0, ORDERS_1, ORDERS_2, ORDERS_5, RELAT_2,
      VALUED_0, FINSEQ_1, PARTFUN1, RELAT_1, FUNCT_1, XXREAL_0, RELSET_1,
      FUNCOP_1, NAT_D, XREAL_0, CARD_1, CARD_2, ABIAN, ENUMSET1, AFINSQ_2,
      RFINSEQ;
 registrations XBOOLE_0, RELAT_1, FUNCT_1, ORDINAL1, NAT_1, XREAL_0, ORDINAL2,
      ORDINAL4, CARD_1, CARD_LAR, AFINSQ_1, FINSET_1, ORDINAL5, ORDINAL6,
      ORDERS_2, ORDERS_5, VALUED_0, FINSEQ_1, FUNCOP_1, MSAFREE5, ORDINAL3,
      AFINSQ_2;
 requirements SUBSET, BOOLE, NUMERALS, ARITHM, REAL;


begin :: Preliminaries

:: into ORDINAL1 ?
theorem :: ORDINAL7:1
  for X being set holds X /\ succ X = X;

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

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

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

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

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

:: 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;

registration
  cluster infinite for Ordinal-Sequence;
end;

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

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

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

:: into ORDINAL5 ?
theorem :: 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;

:: into ORDINAL5 ?
registration
  cluster decreasing -> one-to-one for Ordinal-Sequence;
end;

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

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

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

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

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

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

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

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

:: into ORDINAL5 ?
theorem :: 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;

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

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

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

registration
  cluster natural-valued -> Ordinal-yielding for Sequence;
end;

registration
  cluster limit_ordinal -> zero for Nat;
  cluster non limit_ordinal for Ordinal;
end;

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

begin :: About the Cantor Normal Form

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

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

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

:: this implies ORDINAL5:68
theorem :: 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;

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

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

registration
  cluster non zero -> Cantor-component for Nat;
end;

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

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

registration
  let a be non empty Ordinal, m be non zero Nat;
  cluster <% exp(omega,a), m %> -> Cantor-normal-form;
  let n be non zero Nat;
  cluster <% n *^ exp(omega,a), m %> -> Cantor-normal-form;
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;

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

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

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

:: closure of ordinal addition
theorem :: 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);

theorem :: ORDINAL7:28
  for A being finite Ordinal-Sequence, 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);

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

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

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

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

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

registration
  let A be empty Ordinal-Sequence, b be Ordinal;
  cluster b -exponent A -> empty;
end;

registration
  let A be non empty Ordinal-Sequence, b be Ordinal;
  cluster b -exponent A -> non empty;
end;

registration
  let A be finite Ordinal-Sequence, b be Ordinal;
  cluster b -exponent A -> finite;
end;

registration
  let A be infinite Ordinal-Sequence, b be Ordinal;
  cluster b -exponent A -> infinite;
end;

theorem :: ORDINAL7:33
  for a, b being Ordinal holds b -exponent <% a %> = <% b -exponent a %>;

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

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

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

registration
  let A be Cantor-normal-form Ordinal-Sequence;
  cluster omega -exponent A -> decreasing;
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);

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

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

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

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

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

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

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

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

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

registration
  let c be Cantor-component Ordinal;
  cluster omega -leading_coeff c -> natural non empty;
end;

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

definition
  let A be Ordinal-Sequence, b be Ordinal;
  func b -leading_coeff A -> Ordinal-Sequence means
:: ORDINAL7:def 3

  dom it = dom A &
  for a being object st a in dom A holds it.a = b -leading_coeff(A.a);
end;

registration
  let A be empty Ordinal-Sequence, b be Ordinal;
  cluster b -leading_coeff A -> empty;
end;

registration
  let A be non empty Ordinal-Sequence, b be Ordinal;
  cluster b -leading_coeff A -> non empty;
end;

registration
  let A be finite Ordinal-Sequence, b be Ordinal;
  cluster b -leading_coeff A -> finite;
end;

registration
  let A be infinite Ordinal-Sequence, b be Ordinal;
  cluster b -leading_coeff A -> infinite;
end;

theorem :: ORDINAL7:47
  for a, b being Ordinal
  holds b -leading_coeff <% a %> = <% b -leading_coeff a %>;

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

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

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

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

registration
  let A be Cantor-normal-form Ordinal-Sequence;
  cluster omega -leading_coeff A -> natural-valued non-empty;
end;

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

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

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

theorem :: 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;

definition
  let a be Ordinal;
  func CantorNF a -> Cantor-normal-form Ordinal-Sequence means
:: ORDINAL7:def 4

  Sum^ it = a;
end;

registration
  let a be Ordinal;
  reduce Sum^ CantorNF a to a;
end;

registration
  let A be Cantor-normal-form Ordinal-Sequence;
  reduce CantorNF Sum^ A to A;
end;

theorem :: ORDINAL7:55
  CantorNF {} = {};

registration
  let a be empty Ordinal;
  cluster CantorNF a -> empty;
end;

registration
  let a be non empty Ordinal;
  cluster CantorNF a -> non empty;
end;

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

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

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

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

theorem :: ORDINAL7:60
  for a being non empty Ordinal, b being Ordinal, 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) %>;

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

theorem :: ORDINAL7:62
  for a being non empty Ordinal, b being Ordinal, 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;

begin :: Natural Addition of Ordinals

definition
  let a, b be Ordinal;
  func a (+) b -> Ordinal means
:: 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))));
  commutativity;
end;

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

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

theorem :: ORDINAL7:65
  for a, b being Ordinal, 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)));

theorem :: ORDINAL7:66
  for a, b being Ordinal, 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)));

theorem :: ORDINAL7:67
  for a, b being Ordinal, 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)));

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

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

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

theorem :: 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);

theorem :: 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;

theorem :: ORDINAL7:73
  for a, b being Ordinal, 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);

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

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

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

registration
  let n, m be Nat;
  identify n (+) m with n + m;
end;

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

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

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

registration
  let a be non empty Ordinal, b be Ordinal;
  cluster a (+) b -> non empty;
end;

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

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

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

theorem :: ORDINAL7:80
  for a, b being Ordinal, 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);

theorem :: ORDINAL7:81
  for a, b being Ordinal
  st rng(omega -exponent CantorNF a) = rng(omega -exponent CantorNF b)
  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
;

theorem :: 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);

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);

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

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

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

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

:: closure of natural addition
theorem :: 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);

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

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

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

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

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

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

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

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

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

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