:: ORDINAL2 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

scheme :: ORDINAL2:sch 1
OrdinalInd{ P1[ Ordinal] } :
for A being Ordinal holds P1[A]
provided
A1: P1[ {} ] and
A2: for A being Ordinal st P1[A] holds
P1[ succ A] and
A3: for A being Ordinal st A <> {} & A is_limit_ordinal & ( for B being Ordinal st B in A holds
P1[B] ) holds
P1[A]
proof end;

theorem Th1: :: ORDINAL2:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A, B being Ordinal holds
( A c= B iff succ A c= succ B )
proof end;

theorem Th2: :: ORDINAL2:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being Ordinal holds union (succ A) = A
proof end;

theorem :: ORDINAL2:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being Ordinal holds succ A c= bool A
proof end;

theorem :: ORDINAL2:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
{} is_limit_ordinal
proof end;

theorem Th5: :: ORDINAL2:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being Ordinal holds union A c= A
proof end;

definition
let L be T-Sequence;
func last L -> set equals :: ORDINAL2:def 1
L . (union (dom L));
coherence
L . (union (dom L)) is set ;
end;

:: deftheorem defines last ORDINAL2:def 1 :
for L being T-Sequence holds last L = L . (union (dom L));

theorem :: ORDINAL2:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th7: :: ORDINAL2:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being Ordinal
for L being T-Sequence st dom L = succ A holds
last L = L . A by Th2;

definition
let X be set ;
func On X -> set means :Def2: :: ORDINAL2:def 2
for x being set holds
( x in it iff ( x in X & x is Ordinal ) );
existence
ex b1 being set st
for x being set holds
( x in b1 iff ( x in X & x is Ordinal ) )
proof end;
uniqueness
for b1, b2 being set st ( for x being set holds
( x in b1 iff ( x in X & x is Ordinal ) ) ) & ( for x being set holds
( x in b2 iff ( x in X & x is Ordinal ) ) ) holds
b1 = b2
proof end;
func Lim X -> set means :Def3: :: ORDINAL2:def 3
for x being set holds
( x in it iff ( x in X & ex A being Ordinal st
( x = A & A is_limit_ordinal ) ) );
existence
ex b1 being set st
for x being set holds
( x in b1 iff ( x in X & ex A being Ordinal st
( x = A & A is_limit_ordinal ) ) )
proof end;
uniqueness
for b1, b2 being set st ( for x being set holds
( x in b1 iff ( x in X & ex A being Ordinal st
( x = A & A is_limit_ordinal ) ) ) ) & ( for x being set holds
( x in b2 iff ( x in X & ex A being Ordinal st
( x = A & A is_limit_ordinal ) ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def2 defines On ORDINAL2:def 2 :
for X, b2 being set holds
( b2 = On X iff for x being set holds
( x in b2 iff ( x in X & x is Ordinal ) ) );

:: deftheorem Def3 defines Lim ORDINAL2:def 3 :
for X, b2 being set holds
( b2 = Lim X iff for x being set holds
( x in b2 iff ( x in X & ex A being Ordinal st
( x = A & A is_limit_ordinal ) ) ) );

theorem :: ORDINAL2:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: ORDINAL2:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set holds On X c= X
proof end;

theorem Th10: :: ORDINAL2:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being Ordinal holds On A = A
proof end;

theorem Th11: :: ORDINAL2:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, Y being set st X c= Y holds
On X c= On Y
proof end;

theorem :: ORDINAL2:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: ORDINAL2:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set holds Lim X c= X
proof end;

theorem :: ORDINAL2:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, Y being set st X c= Y holds
Lim X c= Lim Y
proof end;

theorem :: ORDINAL2:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set holds Lim X c= On X
proof end;

theorem Th16: :: ORDINAL2:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being Ordinal ex A being Ordinal st
( D in A & A is_limit_ordinal )
proof end;

theorem Th17: :: ORDINAL2:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set st ( for x being set st x in X holds
x is Ordinal ) holds
meet X is Ordinal
proof end;

definition
func one -> non empty Ordinal equals :: ORDINAL2:def 4
 succ {} ;
correctness
coherence
succ {} is non empty Ordinal;
;
end;

:: deftheorem defines one ORDINAL2:def 4 :
one = succ {} ;

definition
func omega -> set means :Def5: :: ORDINAL2:def 5
( {} in it & it is_limit_ordinal & it is ordinal & ( for A being Ordinal st {} in A & A is_limit_ordinal holds
it c= A ) );
existence
ex b1 being set st
( {} in b1 & b1 is_limit_ordinal & b1 is ordinal & ( for A being Ordinal st {} in A & A is_limit_ordinal holds
b1 c= A ) )
proof end;
uniqueness
for b1, b2 being set st {} in b1 & b1 is_limit_ordinal & b1 is ordinal & ( for A being Ordinal st {} in A & A is_limit_ordinal holds
b1 c= A ) & {} in b2 & b2 is_limit_ordinal & b2 is ordinal & ( for A being Ordinal st {} in A & A is_limit_ordinal holds
b2 c= A ) holds
b1 = b2
proof end;
end;

:: deftheorem Def5 defines omega ORDINAL2:def 5 :
for b1 being set holds
( b1 = omega iff ( {} in b1 & b1 is_limit_ordinal & b1 is ordinal & ( for A being Ordinal st {} in A & A is_limit_ordinal holds
b1 c= A ) ) );

registration
cluster omega -> ordinal non empty ;
coherence
( not omega is empty & omega is ordinal ) by Def5;
end;

registration
cluster being_limit_ordinal set ;
existence
ex b1 being Ordinal st b1 is being_limit_ordinal
proof end;
end;

definition
let X be set ;
func inf X -> Ordinal equals :: ORDINAL2:def 6
 meet (On X);
coherence
meet (On X) is Ordinal
proof end;
func sup X -> Ordinal means :Def7: :: ORDINAL2:def 7
( On X c= it & ( for A being Ordinal st On X c= A holds
it c= A ) );
existence
ex b1 being Ordinal st
( On X c= b1 & ( for A being Ordinal st On X c= A holds
b1 c= A ) )
proof end;
uniqueness
for b1, b2 being Ordinal st On X c= b1 & ( for A being Ordinal st On X c= A holds
b1 c= A ) & On X c= b2 & ( for A being Ordinal st On X c= A holds
b2 c= A ) holds
b1 = b2
proof end;
end;

:: deftheorem defines inf ORDINAL2:def 6 :
for X being set holds inf X = meet (On X);

:: deftheorem Def7 defines sup ORDINAL2:def 7 :
for X being set
for b2 being Ordinal holds
( b2 = sup X iff ( On X c= b2 & ( for A being Ordinal st On X c= A holds
b2 c= A ) ) );

theorem :: ORDINAL2:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: ORDINAL2:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
( {} in omega & omega is_limit_ordinal & ( for A being Ordinal st {} in A & A is_limit_ordinal holds
omega c= A ) ) by Def5;

theorem :: ORDINAL2:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: ORDINAL2:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: ORDINAL2:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being Ordinal
for X being set st A in X holds
inf X c= A
proof end;

theorem :: ORDINAL2:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being Ordinal
for X being set st On X <> {} & ( for A being Ordinal st A in X holds
D c= A ) holds
D c= inf X
proof end;

theorem :: ORDINAL2:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being Ordinal
for X, Y being set st A in X & X c= Y holds
inf Y c= inf X
proof end;

theorem :: ORDINAL2:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being Ordinal
for X being set st A in X holds
inf X in X
proof end;

theorem Th26: :: ORDINAL2:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being Ordinal holds sup A = A
proof end;

theorem Th27: :: ORDINAL2:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being Ordinal
for X being set st A in X holds
A in sup X
proof end;

theorem Th28: :: ORDINAL2:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being Ordinal
for X being set st ( for A being Ordinal st A in X holds
A in D ) holds
sup X c= D
proof end;

theorem :: ORDINAL2:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being Ordinal
for X being set st A in sup X holds
ex B being Ordinal st
( B in X & A c= B )
proof end;

theorem :: ORDINAL2:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, Y being set st X c= Y holds
sup X c= sup Y
proof end;

theorem :: ORDINAL2:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being Ordinal holds sup {A} = succ A
proof end;

theorem :: ORDINAL2:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set holds inf X c= sup X
proof end;

scheme :: ORDINAL2:sch 2
TSLambda{ F1() -> Ordinal, F2( Ordinal) -> set } :
ex L being T-Sequence st
( dom L = F1() & ( for A being Ordinal st A in F1() holds
L . A = F2(A) ) )
proof end;

definition
let f be Function;
attr f is Ordinal-yielding means :Def8: :: ORDINAL2:def 8
 ex A being Ordinal st rng f c= A;
end;

:: deftheorem Def8 defines Ordinal-yielding ORDINAL2:def 8 :
for f being Function holds
( f is Ordinal-yielding iff ex A being Ordinal st rng f c= A );

registration
cluster Ordinal-yielding set ;
existence
ex b1 being T-Sequence st b1 is Ordinal-yielding
proof end;
end;

definition
mode Ordinal-Sequence is Ordinal-yielding T-Sequence;
end;

registration
let A be Ordinal;
cluster -> Ordinal-yielding T-Sequence of A;
coherence
for b1 being T-Sequence of A holds b1 is Ordinal-yielding
proof end;
end;

registration
let L be Ordinal-Sequence;
let A be Ordinal;
cluster L | A -> Ordinal-yielding ;
coherence
L | A is Ordinal-yielding
proof end;
end;

theorem :: ORDINAL2:33  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th34: :: ORDINAL2:34  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being Ordinal
for fi being Ordinal-Sequence st A in dom fi holds
fi . A is Ordinal
proof end;

registration
let f be Ordinal-Sequence;
let a be Ordinal;
cluster f . a -> ordinal ;
coherence
f . a is ordinal
proof end;
end;

scheme :: ORDINAL2:sch 3
OSLambda{ F1() -> Ordinal, F2( Ordinal) -> Ordinal } :
ex fi being Ordinal-Sequence st
( dom fi = F1() & ( for A being Ordinal st A in F1() holds
fi . A = F2(A) ) )
proof end;

scheme :: ORDINAL2:sch 4
TSUniq1{ F1() -> Ordinal, F2() -> set , F3( Ordinal, set ) -> set , F4( Ordinal, T-Sequence) -> set , F5() -> T-Sequence, F6() -> T-Sequence } :
F5() = F6()
provided
A1: dom F5() = F1() and
A2: ( {} in F1() implies F5() . {} = F2() ) and
A3: for A being Ordinal st succ A in F1() holds
F5() . (succ A) = F3(A,(F5() . A)) and
A4: for A being Ordinal st A in F1() & A <> {} & A is_limit_ordinal holds
F5() . A = F4(A,(F5() | A)) and
A5: dom F6() = F1() and
A6: ( {} in F1() implies F6() . {} = F2() ) and
A7: for A being Ordinal st succ A in F1() holds
F6() . (succ A) = F3(A,(F6() . A)) and
A8: for A being Ordinal st A in F1() & A <> {} & A is_limit_ordinal holds
F6() . A = F4(A,(F6() | A))
proof end;

scheme :: ORDINAL2:sch 5
TSExist1{ F1() -> Ordinal, F2() -> set , F3( Ordinal, set ) -> set , F4( Ordinal, T-Sequence) -> set } :
ex L being T-Sequence st
( dom L = F1() & ( {} in F1() implies L . {} = F2() ) & ( for A being Ordinal st succ A in F1() holds
L . (succ A) = F3(A,(L . A)) ) & ( for A being Ordinal st A in F1() & A <> {} & A is_limit_ordinal holds
L . A = F4(A,(L | A)) ) )
proof end;

scheme :: ORDINAL2:sch 6
TSResult{ F1() -> T-Sequence, F2( Ordinal) -> set , F3() -> Ordinal, F4() -> set , F5( Ordinal, set ) -> set , F6( Ordinal, T-Sequence) -> set } :
for A being Ordinal st A in dom F1() holds
F1() . A = F2(A)
provided
A1: for A being Ordinal
for x being set holds
( x = F2(A) iff ex L being T-Sequence st
( x = last L & dom L = succ A & L . {} = F4() & ( for C being Ordinal st succ C in succ A holds
L . (succ C) = F5(C,(L . C)) ) & ( for C being Ordinal st C in succ A & C <> {} & C is_limit_ordinal holds
L . C = F6(C,(L | C)) ) ) ) and
A2: dom F1() = F3() and
A3: ( {} in F3() implies F1() . {} = F4() ) and
A4: for A being Ordinal st succ A in F3() holds
F1() . (succ A) = F5(A,(F1() . A)) and
A5: for A being Ordinal st A in F3() & A <> {} & A is_limit_ordinal holds
F1() . A = F6(A,(F1() | A))
proof end;

scheme :: ORDINAL2:sch 7
TSDef{ F1() -> Ordinal, F2() -> set , F3( Ordinal, set ) -> set , F4( Ordinal, T-Sequence) -> set } :
( ex x being set ex L being T-Sequence st
( x = last L & dom L = succ F1() & L . {} = F2() & ( for C being Ordinal st succ C in succ F1() holds
L . (succ C) = F3(C,(L . C)) ) & ( for C being Ordinal st C in succ F1() & C <> {} & C is_limit_ordinal holds
L . C = F4(C,(L | C)) ) ) & ( for x1, x2 being set st ex L being T-Sequence st
( x1 = last L & dom L = succ F1() & L . {} = F2() & ( for C being Ordinal st succ C in succ F1() holds
L . (succ C) = F3(C,(L . C)) ) & ( for C being Ordinal st C in succ F1() & C <> {} & C is_limit_ordinal holds
L . C = F4(C,(L | C)) ) ) & ex L being T-Sequence st
( x2 = last L & dom L = succ F1() & L . {} = F2() & ( for C being Ordinal st succ C in succ F1() holds
L . (succ C) = F3(C,(L . C)) ) & ( for C being Ordinal st C in succ F1() & C <> {} & C is_limit_ordinal holds
L . C = F4(C,(L | C)) ) ) holds
x1 = x2 ) )
proof end;

scheme :: ORDINAL2:sch 8
TSResult0{ F1( Ordinal) -> set , F2() -> set , F3( Ordinal, set ) -> set , F4( Ordinal, T-Sequence) -> set } :
F1({} ) = F2()
provided
A1: for A being Ordinal
for x being set holds
( x = F1(A) iff ex L being T-Sequence st
( x = last L & dom L = succ A & L . {} = F2() & ( for C being Ordinal st succ C in succ A holds
L . (succ C) = F3(C,(L . C)) ) & ( for C being Ordinal st C in succ A & C <> {} & C is_limit_ordinal holds
L . C = F4(C,(L | C)) ) ) )
proof end;

scheme :: ORDINAL2:sch 9
TSResultS{ F1() -> set , F2( Ordinal, set ) -> set , F3( Ordinal, T-Sequence) -> set , F4( Ordinal) -> set } :
for A being Ordinal holds F4((succ A)) = F2(A,F4(A))
provided
A1: for A being Ordinal
for x being set holds
( x = F4(A) iff ex L being T-Sequence st
( x = last L & dom L = succ A & L . {} = F1() & ( for C being Ordinal st succ C in succ A holds
L . (succ C) = F2(C,(L . C)) ) & ( for C being Ordinal st C in succ A & C <> {} & C is_limit_ordinal holds
L . C = F3(C,(L | C)) ) ) )
proof end;

scheme :: ORDINAL2:sch 10
TSResultL{ F1() -> T-Sequence, F2() -> Ordinal, F3( Ordinal) -> set , F4() -> set , F5( Ordinal, set ) -> set , F6( Ordinal, T-Sequence) -> set } :
F3(F2()) = F6(F2(),F1())
provided
A1: for A being Ordinal
for x being set holds
( x = F3(A) iff ex L being T-Sequence st
( x = last L & dom L = succ A & L . {} = F4() & ( for C being Ordinal st succ C in succ A holds
L . (succ C) = F5(C,(L . C)) ) & ( for C being Ordinal st C in succ A & C <> {} & C is_limit_ordinal holds
L . C = F6(C,(L | C)) ) ) ) and
A2: ( F2() <> {} & F2() is_limit_ordinal ) and
A3: dom F1() = F2() and
A4: for A being Ordinal st A in F2() holds
F1() . A = F3(A)
proof end;

scheme :: ORDINAL2:sch 11
OSExist{ F1() -> Ordinal, F2() -> Ordinal, F3( Ordinal, Ordinal) -> Ordinal, F4( Ordinal, T-Sequence) -> Ordinal } :
ex fi being Ordinal-Sequence st
( dom fi = F1() & ( {} in F1() implies fi . {} = F2() ) & ( for A being Ordinal st succ A in F1() holds
fi . (succ A) = F3(A,(fi . A)) ) & ( for A being Ordinal st A in F1() & A <> {} & A is_limit_ordinal holds
fi . A = F4(A,(fi | A)) ) )
proof end;

scheme :: ORDINAL2:sch 12
OSResult{ F1() -> Ordinal-Sequence, F2( Ordinal) -> Ordinal, F3() -> Ordinal, F4() -> Ordinal, F5( Ordinal, Ordinal) -> Ordinal, F6( Ordinal, T-Sequence) -> Ordinal } :
for A being Ordinal st A in dom F1() holds
F1() . A = F2(A)
provided
A1: for A, B being Ordinal holds
( B = F2(A) iff ex fi being Ordinal-Sequence st
( B = last fi & dom fi = succ A & fi . {} = F4() & ( for C being Ordinal st succ C in succ A holds
fi . (succ C) = F5(C,(fi . C)) ) & ( for C being Ordinal st C in succ A & C <> {} & C is_limit_ordinal holds
fi . C = F6(C,(fi | C)) ) ) ) and
A2: dom F1() = F3() and
A3: ( {} in F3() implies F1() . {} = F4() ) and
A4: for A being Ordinal st succ A in F3() holds
F1() . (succ A) = F5(A,(F1() . A)) and
A5: for A being Ordinal st A in F3() & A <> {} & A is_limit_ordinal holds
F1() . A = F6(A,(F1() | A))
proof end;

scheme :: ORDINAL2:sch 13
OSDef{ F1() -> Ordinal, F2() -> Ordinal, F3( Ordinal, Ordinal) -> Ordinal, F4( Ordinal, T-Sequence) -> Ordinal } :
( ex A being Ordinal ex fi being Ordinal-Sequence st
( A = last fi & dom fi = succ F1() & fi . {} = F2() & ( for C being Ordinal st succ C in succ F1() holds
fi . (succ C) = F3(C,(fi . C)) ) & ( for C being Ordinal st C in succ F1() & C <> {} & C is_limit_ordinal holds
fi . C = F4(C,(fi | C)) ) ) & ( for A1, A2 being Ordinal st ex fi being Ordinal-Sequence st
( A1 = last fi & dom fi = succ F1() & fi . {} = F2() & ( for C being Ordinal st succ C in succ F1() holds
fi . (succ C) = F3(C,(fi . C)) ) & ( for C being Ordinal st C in succ F1() & C <> {} & C is_limit_ordinal holds
fi . C = F4(C,(fi | C)) ) ) & ex fi being Ordinal-Sequence st
( A2 = last fi & dom fi = succ F1() & fi . {} = F2() & ( for C being Ordinal st succ C in succ F1() holds
fi . (succ C) = F3(C,(fi . C)) ) & ( for C being Ordinal st C in succ F1() & C <> {} & C is_limit_ordinal holds
fi . C = F4(C,(fi | C)) ) ) holds
A1 = A2 ) )
proof end;

scheme :: ORDINAL2:sch 14
OSResult0{ F1( Ordinal) -> Ordinal, F2() -> Ordinal, F3( Ordinal, Ordinal) -> Ordinal, F4( Ordinal, T-Sequence) -> Ordinal } :
F1({} ) = F2()
provided
A1: for A, B being Ordinal holds
( B = F1(A) iff ex fi being Ordinal-Sequence st
( B = last fi & dom fi = succ A & fi . {} = F2() & ( for C being Ordinal st succ C in succ A holds
fi . (succ C) = F3(C,(fi . C)) ) & ( for C being Ordinal st C in succ A & C <> {} & C is_limit_ordinal holds
fi . C = F4(C,(fi | C)) ) ) )
proof end;

scheme :: ORDINAL2:sch 15
OSResultS{ F1() -> Ordinal, F2( Ordinal, Ordinal) -> Ordinal, F3( Ordinal, T-Sequence) -> Ordinal, F4( Ordinal) -> Ordinal } :
for A being Ordinal holds F4((succ A)) = F2(A,F4(A))
provided
A1: for A, B being Ordinal holds
( B = F4(A) iff ex fi being Ordinal-Sequence st
( B = last fi & dom fi = succ A & fi . {} = F1() & ( for C being Ordinal st succ C in succ A holds
fi . (succ C) = F2(C,(fi . C)) ) & ( for C being Ordinal st C in succ A & C <> {} & C is_limit_ordinal holds
fi . C = F3(C,(fi | C)) ) ) )
proof end;

scheme :: ORDINAL2:sch 16
OSResultL{ F1() -> Ordinal-Sequence, F2() -> Ordinal, F3( Ordinal) -> Ordinal, F4() -> Ordinal, F5( Ordinal, Ordinal) -> Ordinal, F6( Ordinal, T-Sequence) -> Ordinal } :
F3(F2()) = F6(F2(),F1())
provided
A1: for A, B being Ordinal holds
( B = F3(A) iff ex fi being Ordinal-Sequence st
( B = last fi & dom fi = succ A & fi . {} = F4() & ( for C being Ordinal st succ C in succ A holds
fi . (succ C) = F5(C,(fi . C)) ) & ( for C being Ordinal st C in succ A & C <> {} & C is_limit_ordinal holds
fi . C = F6(C,(fi | C)) ) ) ) and
A2: ( F2() <> {} & F2() is_limit_ordinal ) and
A3: dom F1() = F2() and
A4: for A being Ordinal st A in F2() holds
F1() . A = F3(A)
proof end;

definition
let L be T-Sequence;
func sup L -> Ordinal equals :: ORDINAL2:def 9
 sup (rng L);
correctness
coherence
sup (rng L) is Ordinal;
;
func inf L -> Ordinal equals :: ORDINAL2:def 10
 inf (rng L);
correctness
coherence
inf (rng L) is Ordinal;
;
end;

:: deftheorem defines sup ORDINAL2:def 9 :
for L being T-Sequence holds sup L = sup (rng L);

:: deftheorem defines inf ORDINAL2:def 10 :
for L being T-Sequence holds inf L = inf (rng L);

theorem :: ORDINAL2:35  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being T-Sequence holds
( sup L = sup (rng L) & inf L = inf (rng L) ) ;

definition
let L be T-Sequence;
func lim_sup L -> Ordinal means :: ORDINAL2:def 11
 ex fi being Ordinal-Sequence st
( it = inf fi & dom fi = dom L & ( for A being Ordinal st A in dom L holds
fi . A = sup (rng (L | ((dom L) \ A))) ) );
existence
ex b1 being Ordinal ex fi being Ordinal-Sequence st
( b1 = inf fi & dom fi = dom L & ( for A being Ordinal st A in dom L holds
fi . A = sup (rng (L | ((dom L) \ A))) ) )
proof end;
uniqueness
for b1, b2 being Ordinal st ex fi being Ordinal-Sequence st
( b1 = inf fi & dom fi = dom L & ( for A being Ordinal st A in dom L holds
fi . A = sup (rng (L | ((dom L) \ A))) ) ) & ex fi being Ordinal-Sequence st
( b2 = inf fi & dom fi = dom L & ( for A being Ordinal st A in dom L holds
fi . A = sup (rng (L | ((dom L) \ A))) ) ) holds
b1 = b2
proof end;
func lim_inf L -> Ordinal means :: ORDINAL2:def 12
 ex fi being Ordinal-Sequence st
( it = sup fi & dom fi = dom L & ( for A being Ordinal st A in dom L holds
fi . A = inf (rng (L | ((dom L) \ A))) ) );
existence
ex b1 being Ordinal ex fi being Ordinal-Sequence st
( b1 = sup fi & dom fi = dom L & ( for A being Ordinal st A in dom L holds
fi . A = inf (rng (L | ((dom L) \ A))) ) )
proof end;
uniqueness
for b1, b2 being Ordinal st ex fi being Ordinal-Sequence st
( b1 = sup fi & dom fi = dom L & ( for A being Ordinal st A in dom L holds
fi . A = inf (rng (L | ((dom L) \ A))) ) ) & ex fi being Ordinal-Sequence st
( b2 = sup fi & dom fi = dom L & ( for A being Ordinal st A in dom L holds
fi . A = inf (rng (L | ((dom L) \ A))) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem defines lim_sup ORDINAL2:def 11 :
for L being T-Sequence
for b2 being Ordinal holds
( b2 = lim_sup L iff ex fi being Ordinal-Sequence st
( b2 = inf fi & dom fi = dom L & ( for A being Ordinal st A in dom L holds
fi . A = sup (rng (L | ((dom L) \ A))) ) ) );

:: deftheorem defines lim_inf ORDINAL2:def 12 :
for L being T-Sequence
for b2 being Ordinal holds
( b2 = lim_inf L iff ex fi being Ordinal-Sequence st
( b2 = sup fi & dom fi = dom L & ( for A being Ordinal st A in dom L holds
fi . A = inf (rng (L | ((dom L) \ A))) ) ) );

definition
let A be Ordinal;
let fi be Ordinal-Sequence;
pred A is_limes_of fi means :Def13: :: ORDINAL2:def 13
 ex B being Ordinal st
( B in dom fi & ( for C being Ordinal st B c= C & C in dom fi holds
fi . C = {} ) ) if A = {}
otherwise for B, C being Ordinal st B in A & A in C holds
ex D being Ordinal st
( D in dom fi & ( for E being Ordinal st D c= E & E in dom fi holds
( B in fi . E & fi . E in C ) ) );
consistency
verum ;
end;

:: deftheorem Def13 defines is_limes_of ORDINAL2:def 13 :
for A being Ordinal
for fi being Ordinal-Sequence holds
( ( A = {} implies ( A is_limes_of fi iff ex B being Ordinal st
( B in dom fi & ( for C being Ordinal st B c= C & C in dom fi holds
fi . C = {} ) ) ) ) & ( not A = {} implies ( A is_limes_of fi iff for B, C being Ordinal st B in A & A in C holds
ex D being Ordinal st
( D in dom fi & ( for E being Ordinal st D c= E & E in dom fi holds
( B in fi . E & fi . E in C ) ) ) ) ) );

definition
let fi be Ordinal-Sequence;
given A being Ordinal such that A1: A is_limes_of fi ;
func lim fi -> Ordinal means :Def14: :: ORDINAL2:def 14
it is_limes_of fi;
existence
ex b1 being Ordinal st b1 is_limes_of fi by A1;
uniqueness
for b1, b2 being Ordinal st b1 is_limes_of fi & b2 is_limes_of fi holds
b1 = b2
proof end;
end;

:: deftheorem Def14 defines lim ORDINAL2:def 14 :
for fi being Ordinal-Sequence st ex A being Ordinal st A is_limes_of fi holds
for b2 being Ordinal holds
( b2 = lim fi iff b2 is_limes_of fi );

definition
let A be Ordinal;
let fi be Ordinal-Sequence;
func lim A,fi -> Ordinal equals :: ORDINAL2:def 15
 lim (fi | A);
correctness
coherence
lim (fi | A) is Ordinal;
;
end;

:: deftheorem defines lim ORDINAL2:def 15 :
for A being Ordinal
for fi being Ordinal-Sequence holds lim A,fi = lim (fi | A);

definition
let L be Ordinal-Sequence;
attr L is increasing means :: ORDINAL2:def 16
for A, B being Ordinal st A in B & B in dom L holds
L . A in L . B;
attr L is continuous means :: ORDINAL2:def 17
for A, B being Ordinal st A in dom L & A <> {} & A is_limit_ordinal & B = L . A holds
B is_limes_of L | A;
end;

:: deftheorem defines increasing ORDINAL2:def 16 :
for L being Ordinal-Sequence holds
( L is increasing iff for A, B being Ordinal st A in B & B in dom L holds
L . A in L . B );

:: deftheorem defines continuous ORDINAL2:def 17 :
for L being Ordinal-Sequence holds
( L is continuous iff for A, B being Ordinal st A in dom L & A <> {} & A is_limit_ordinal & B = L . A holds
B is_limes_of L | A );

definition
let A, B be Ordinal;
func A +^ B -> Ordinal means :Def18: :: ORDINAL2:def 18
 ex fi being Ordinal-Sequence st
( it = last fi & dom fi = succ B & fi . {} = A & ( for C being Ordinal st succ C in succ B holds
fi . (succ C) = succ (fi . C) ) & ( for C being Ordinal st C in succ B & C <> {} & C is_limit_ordinal holds
fi . C = sup (fi | C) ) );
correctness
existence
ex b1 being Ordinal ex fi being Ordinal-Sequence st
( b1 = last fi & dom fi = succ B & fi . {} = A & ( for C being Ordinal st succ C in succ B holds
fi . (succ C) = succ (fi . C) ) & ( for C being Ordinal st C in succ B & C <> {} & C is_limit_ordinal holds
fi . C = sup (fi | C) ) );
uniqueness
for b1, b2 being Ordinal st ex fi being Ordinal-Sequence st
( b1 = last fi & dom fi = succ B & fi . {} = A & ( for C being Ordinal st succ C in succ B holds
fi . (succ C) = succ (fi . C) ) & ( for C being Ordinal st C in succ B & C <> {} & C is_limit_ordinal holds
fi . C = sup (fi | C) ) ) & ex fi being Ordinal-Sequence st
( b2 = last fi & dom fi = succ B & fi . {} = A & ( for C being Ordinal st succ C in succ B holds
fi . (succ C) = succ (fi . C) ) & ( for C being Ordinal st C in succ B & C <> {} & C is_limit_ordinal holds
fi . C = sup (fi | C) ) ) holds
b1 = b2;
proof end;
end;

:: deftheorem Def18 defines +^ ORDINAL2:def 18 :
for A, B, b3 being Ordinal holds
( b3 = A +^ B iff ex fi being Ordinal-Sequence st
( b3 = last fi & dom fi = succ B & fi . {} = A & ( for C being Ordinal st succ C in succ B holds
fi . (succ C) = succ (fi . C) ) & ( for C being Ordinal st C in succ B & C <> {} & C is_limit_ordinal holds
fi . C = sup (fi | C) ) ) );

definition
let A, B be Ordinal;
func A *^ B -> Ordinal means :Def19: :: ORDINAL2:def 19
 ex fi being Ordinal-Sequence st
( it = last fi & dom fi = succ A & fi . {} = {} & ( for C being Ordinal st succ C in succ A holds
fi . (succ C) = (fi . C) +^ B ) & ( for C being Ordinal st C in succ A & C <> {} & C is_limit_ordinal holds
fi . C = union (sup (fi | C)) ) );
correctness
existence
ex b1 being Ordinal ex fi being Ordinal-Sequence st
( b1 = last fi & dom fi = succ A & fi . {} = {} & ( for C being Ordinal st succ C in succ A holds
fi . (succ C) = (fi . C) +^ B ) & ( for C being Ordinal st C in succ A & C <> {} & C is_limit_ordinal holds
fi . C = union (sup (fi | C)) ) );
uniqueness
for b1, b2 being Ordinal st ex fi being Ordinal-Sequence st
( b1 = last fi & dom fi = succ A & fi . {} = {} & ( for C being Ordinal st succ C in succ A holds
fi . (succ C) = (fi . C) +^ B ) & ( for C being Ordinal st C in succ A & C <> {} & C is_limit_ordinal holds
fi . C = union (sup (fi | C)) ) ) & ex fi being Ordinal-Sequence st
( b2 = last fi & dom fi = succ A & fi . {} = {} & ( for C being Ordinal st succ C in succ A holds
fi . (succ C) = (fi . C) +^ B ) & ( for C being Ordinal st C in succ A & C <> {} & C is_limit_ordinal holds
fi . C = union (sup (fi | C)) ) ) holds
b1 = b2;
proof end;
end;

:: deftheorem Def19 defines *^ ORDINAL2:def 19 :
for A, B, b3 being Ordinal holds
( b3 = A *^ B iff ex fi being Ordinal-Sequence st
( b3 = last fi & dom fi = succ A & fi . {} = {} & ( for C being Ordinal st succ C in succ A holds
fi . (succ C) = (fi . C) +^ B ) & ( for C being Ordinal st C in succ A & C <> {} & C is_limit_ordinal holds
fi . C = union (sup (fi | C)) ) ) );

definition
let A, B be Ordinal;
func exp A,B -> Ordinal means :Def20: :: ORDINAL2:def 20
 ex fi being Ordinal-Sequence st
( it = last fi & dom fi = succ B & fi . {} = one & ( for C being Ordinal st succ C in succ B holds
fi . (succ C) = A *^ (fi . C) ) & ( for C being Ordinal st C in succ B & C <> {} & C is_limit_ordinal holds
fi . C = lim (fi | C) ) );
correctness
existence
ex b1 being Ordinal ex fi being Ordinal-Sequence st
( b1 = last fi & dom fi = succ B & fi . {} = one & ( for C being Ordinal st succ C in succ B holds
fi . (succ C) = A *^ (fi . C) ) & ( for C being Ordinal st C in succ B & C <> {} & C is_limit_ordinal holds
fi . C = lim (fi | C) ) );
uniqueness
for b1, b2 being Ordinal st ex fi being Ordinal-Sequence st
( b1 = last fi & dom fi = succ B & fi . {} = one & ( for C being Ordinal st succ C in succ B holds
fi . (succ C) = A *^ (fi . C) ) & ( for C being Ordinal st C in succ B & C <> {} & C is_limit_ordinal holds
fi . C = lim (fi | C) ) ) & ex fi being Ordinal-Sequence st
( b2 = last fi & dom fi = succ B & fi . {} = one & ( for C being Ordinal st succ C in succ B holds
fi . (succ C) = A *^ (fi . C) ) & ( for C being Ordinal st C in succ B & C <> {} & C is_limit_ordinal holds
fi . C = lim (fi | C) ) ) holds
b1 = b2;
proof end;
end;

:: deftheorem Def20 defines exp ORDINAL2:def 20 :
for A, B, b3 being Ordinal holds
( b3 = exp A,B iff ex fi being Ordinal-Sequence st
( b3 = last fi & dom fi = succ B & fi . {} = one & ( for C being Ordinal st succ C in succ B holds
fi . (succ C) = A *^ (fi . C) ) & ( for C being Ordinal st C in succ B & C <> {} & C is_limit_ordinal holds
fi . C = lim (fi | C) ) ) );

theorem :: ORDINAL2:36  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: ORDINAL2:37  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: ORDINAL2:38  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: ORDINAL2:39  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: ORDINAL2:40  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: ORDINAL2:41  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: ORDINAL2:42  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: ORDINAL2:43  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th44: :: ORDINAL2:44  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being Ordinal holds A +^ {} = A
proof end;

theorem Th45: :: ORDINAL2:45  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A, B being Ordinal holds A +^ (succ B) = succ (A +^ B)
proof end;

theorem Th46: :: ORDINAL2:46  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for B, A being Ordinal st B <> {} & B is_limit_ordinal holds
for fi being Ordinal-Sequence st dom fi = B & ( for C being Ordinal st C in B holds
fi . C = A +^ C ) holds
A +^ B = sup fi
proof end;

theorem Th47: :: ORDINAL2:47  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being Ordinal holds {} +^ A = A
proof end;

theorem :: ORDINAL2:48  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being Ordinal holds A +^ one = succ A
proof end;

theorem Th49: :: ORDINAL2:49  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A, B, C being Ordinal st A in B holds
C +^ A in C +^ B
proof end;

theorem Th50: :: ORDINAL2:50  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A, B, C being Ordinal st A c= B holds
C +^ A c= C +^ B
proof end;

theorem Th51: :: ORDINAL2:51  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A, B, C being Ordinal st A c= B holds
A +^ C c= B +^ C
proof end;

theorem Th52: :: ORDINAL2:52  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being Ordinal holds {} *^ A = {}
proof end;

theorem Th53: :: ORDINAL2:53  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for B, A being Ordinal holds (succ B) *^ A = (B *^ A) +^ A
proof end;

theorem Th54: :: ORDINAL2:54  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for B, A being Ordinal st B <> {} & B is_limit_ordinal holds
for fi being Ordinal-Sequence st dom fi = B & ( for C being Ordinal st C in B holds
fi . C = C *^ A ) holds
B *^ A = union (sup fi)
proof end;

theorem Th55: :: ORDINAL2:55  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being Ordinal holds A *^ {} = {}
proof end;

theorem Th56: :: ORDINAL2:56  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being Ordinal holds
( one *^ A = A & A *^ one = A )
proof end;

theorem Th57: :: ORDINAL2:57  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C, A, B being Ordinal st C <> {} & A in B holds
A *^ C in B *^ C
proof end;

theorem :: ORDINAL2:58  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A, B, C being Ordinal st A c= B holds
A *^ C c= B *^ C
proof end;

theorem :: ORDINAL2:59  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A, B, C being Ordinal st A c= B holds
C *^ A c= C *^ B
proof end;

theorem Th60: :: ORDINAL2:60  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being Ordinal holds exp A,{} = one
proof end;

theorem Th61: :: ORDINAL2:61  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A, B being Ordinal holds exp A,(succ B) = A *^ (exp A,B)
proof end;

theorem Th62: :: ORDINAL2:62  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for B, A being Ordinal st B <> {} & B is_limit_ordinal holds
for fi being Ordinal-Sequence st dom fi = B & ( for C being Ordinal st C in B holds
fi . C = exp A,C ) holds
exp A,B = lim fi
proof end;

theorem :: ORDINAL2:63  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being Ordinal holds
( exp A,one = A & exp one ,A = one )
proof end;

definition
let A be set ;
attr A is natural means :Def21: :: ORDINAL2:def 21
A in omega ;
end;

:: deftheorem Def21 defines natural ORDINAL2:def 21 :
for A being set holds
( A is natural iff A in omega );

theorem :: ORDINAL2:64  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: ORDINAL2:65  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being Ordinal ex B, C being Ordinal st
( B is_limit_ordinal & C is natural & A = B +^ C )
proof end;

registration
let X be set ;
let o be Ordinal;
cluster X --> o -> Ordinal-yielding ;
coherence
X --> o is Ordinal-yielding
proof end;
end;