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

theorem Th1: :: ORDINAL3:1  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 X c= succ X
proof end;

theorem :: ORDINAL3:2  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 succ X c= Y holds
X c= Y
proof end;

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

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

theorem :: ORDINAL3:5  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 in B iff succ A in succ B )
proof end;

theorem :: ORDINAL3:6  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 X c= A holds
union X is Ordinal
proof end;

theorem :: ORDINAL3:7  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 union (On X) is Ordinal
proof end;

theorem Th8: :: ORDINAL3:8  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 X c= A holds
On X = X
proof end;

theorem Th9: :: ORDINAL3:9  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 Th10: :: ORDINAL3: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 st A <> {} holds
{} in A
proof end;

theorem :: ORDINAL3:11  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 inf A = {}
proof end;

theorem :: ORDINAL3:12  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 inf {A} = A
proof end;

theorem :: ORDINAL3:13  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 X c= A holds
meet X is Ordinal
proof end;

registration
let A, B be Ordinal;
cluster A \/ B -> ordinal ;
coherence
A \/ B is ordinal
proof end;
cluster A /\ B -> ordinal ;
coherence
A /\ B is ordinal
proof end;
end;

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

theorem :: ORDINAL3:15  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 \/ B = A or A \/ B = B )
proof end;

theorem :: ORDINAL3:16  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 /\ B = A or A /\ B = B )
proof end;

theorem Th17: :: ORDINAL3:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being Ordinal st A in one holds
A = {}
proof end;

theorem :: ORDINAL3:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
one = {{} }
proof end;

theorem Th19: :: ORDINAL3:19  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
( not A c= one or A = {} or A = one )
proof end;

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

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

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

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

theorem Th24: :: ORDINAL3:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for B, C, D being Ordinal st B +^ C = B +^ D holds
C = D
proof end;

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

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

theorem Th27: :: ORDINAL3:27  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= A +^ B & B c= A +^ B )
proof end;

theorem :: ORDINAL3:28  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
( A in B +^ C & A in C +^ B )
proof end;

theorem Th29: :: ORDINAL3:29  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 st A +^ B = {} holds
( A = {} & B = {} )
proof end;

theorem Th30: :: ORDINAL3:30  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 st A c= B holds
ex C being Ordinal st B = A +^ C
proof end;

theorem Th31: :: ORDINAL3:31  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 st A in B holds
ex C being Ordinal st
( B = A +^ C & C <> {} )
proof end;

theorem Th32: :: ORDINAL3:32  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 st A <> {} & A is_limit_ordinal holds
B +^ A is_limit_ordinal
proof end;

theorem Th33: :: ORDINAL3:33  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 holds (A +^ B) +^ C = A +^ (B +^ C)
proof end;

theorem :: ORDINAL3:34  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
( not A *^ B = {} or A = {} or B = {} )
proof end;

theorem :: ORDINAL3:35  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 & C <> {} holds
( A in B *^ C & A in C *^ B )
proof end;

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

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

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

theorem Th39: :: ORDINAL3:39  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 <> {} holds
( A c= A *^ B & A c= B *^ A )
proof end;

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

theorem :: ORDINAL3:41  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 st A *^ B = one holds
( A = one & B = one )
proof end;

theorem Th42: :: ORDINAL3:42  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 holds
( not A in B +^ C or A in B or ex D being Ordinal st
( D in C & A = B +^ D ) )
proof end;

definition
let C be Ordinal;
let fi be Ordinal-Sequence;
canceled;
func C +^ fi -> Ordinal-Sequence means :Def2: :: ORDINAL3:def 2
( dom it = dom fi & ( for A being Ordinal st A in dom fi holds
it . A = C +^ (fi . A) ) );
existence
ex b1 being Ordinal-Sequence st
( dom b1 = dom fi & ( for A being Ordinal st A in dom fi holds
b1 . A = C +^ (fi . A) ) )
proof end;
uniqueness
for b1, b2 being Ordinal-Sequence st dom b1 = dom fi & ( for A being Ordinal st A in dom fi holds
b1 . A = C +^ (fi . A) ) & dom b2 = dom fi & ( for A being Ordinal st A in dom fi holds
b2 . A = C +^ (fi . A) ) holds
b1 = b2
proof end;
func fi +^ C -> Ordinal-Sequence means :: ORDINAL3:def 3
( dom it = dom fi & ( for A being Ordinal st A in dom fi holds
it . A = (fi . A) +^ C ) );
existence
ex b1 being Ordinal-Sequence st
( dom b1 = dom fi & ( for A being Ordinal st A in dom fi holds
b1 . A = (fi . A) +^ C ) )
proof end;
uniqueness
for b1, b2 being Ordinal-Sequence st dom b1 = dom fi & ( for A being Ordinal st A in dom fi holds
b1 . A = (fi . A) +^ C ) & dom b2 = dom fi & ( for A being Ordinal st A in dom fi holds
b2 . A = (fi . A) +^ C ) holds
b1 = b2
proof end;
func C *^ fi -> Ordinal-Sequence means :: ORDINAL3:def 4
( dom it = dom fi & ( for A being Ordinal st A in dom fi holds
it . A = C *^ (fi . A) ) );
existence
ex b1 being Ordinal-Sequence st
( dom b1 = dom fi & ( for A being Ordinal st A in dom fi holds
b1 . A = C *^ (fi . A) ) )
proof end;
uniqueness
for b1, b2 being Ordinal-Sequence st dom b1 = dom fi & ( for A being Ordinal st A in dom fi holds
b1 . A = C *^ (fi . A) ) & dom b2 = dom fi & ( for A being Ordinal st A in dom fi holds
b2 . A = C *^ (fi . A) ) holds
b1 = b2
proof end;
func fi *^ C -> Ordinal-Sequence means :Def5: :: ORDINAL3:def 5
( dom it = dom fi & ( for A being Ordinal st A in dom fi holds
it . A = (fi . A) *^ C ) );
existence
ex b1 being Ordinal-Sequence st
( dom b1 = dom fi & ( for A being Ordinal st A in dom fi holds
b1 . A = (fi . A) *^ C ) )
proof end;
uniqueness
for b1, b2 being Ordinal-Sequence st dom b1 = dom fi & ( for A being Ordinal st A in dom fi holds
b1 . A = (fi . A) *^ C ) & dom b2 = dom fi & ( for A being Ordinal st A in dom fi holds
b2 . A = (fi . A) *^ C ) holds
b1 = b2
proof end;
end;

:: deftheorem ORDINAL3:def 1 :
canceled;

:: deftheorem Def2 defines +^ ORDINAL3:def 2 :
for C being Ordinal
for fi, b3 being Ordinal-Sequence holds
( b3 = C +^ fi iff ( dom b3 = dom fi & ( for A being Ordinal st A in dom fi holds
b3 . A = C +^ (fi . A) ) ) );

:: deftheorem defines +^ ORDINAL3:def 3 :
for C being Ordinal
for fi, b3 being Ordinal-Sequence holds
( b3 = fi +^ C iff ( dom b3 = dom fi & ( for A being Ordinal st A in dom fi holds
b3 . A = (fi . A) +^ C ) ) );

:: deftheorem defines *^ ORDINAL3:def 4 :
for C being Ordinal
for fi, b3 being Ordinal-Sequence holds
( b3 = C *^ fi iff ( dom b3 = dom fi & ( for A being Ordinal st A in dom fi holds
b3 . A = C *^ (fi . A) ) ) );

:: deftheorem Def5 defines *^ ORDINAL3:def 5 :
for C being Ordinal
for fi, b3 being Ordinal-Sequence holds
( b3 = fi *^ C iff ( dom b3 = dom fi & ( for A being Ordinal st A in dom fi holds
b3 . A = (fi . A) *^ C ) ) );

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

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

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

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

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

theorem Th48: :: ORDINAL3:48  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 st A is_limit_ordinal holds
A *^ B is_limit_ordinal
proof end;

theorem Th49: :: ORDINAL3: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 *^ C & B is_limit_ordinal holds
ex D being Ordinal st
( D in B & A in D *^ C )
proof end;

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

theorem Th51: :: ORDINAL3:51  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for fi being Ordinal-Sequence
for C being Ordinal st {} <> dom fi holds
sup (C +^ fi) = C +^ (sup fi)
proof end;

theorem Th52: :: ORDINAL3:52  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for fi being Ordinal-Sequence
for C being Ordinal st {} <> dom fi & C <> {} & sup fi is_limit_ordinal holds
sup (fi *^ C) = (sup fi) *^ C
proof end;

theorem Th53: :: ORDINAL3: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 st B <> {} holds
union (A +^ B) = A +^ (union B)
proof end;

theorem Th54: :: ORDINAL3:54  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 holds (A +^ B) *^ C = (A *^ C) +^ (B *^ C)
proof end;

theorem Th55: :: ORDINAL3:55  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 st A <> {} holds
ex C, D being Ordinal st
( B = (C *^ A) +^ D & D in A )
proof end;

theorem Th56: :: ORDINAL3:56  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A, C1, D1, C2, D2 being Ordinal st (C1 *^ A) +^ D1 = (C2 *^ A) +^ D2 & D1 in A & D2 in A holds
( C1 = C2 & D1 = D2 )
proof end;

theorem Th57: :: ORDINAL3:57  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 one in B & A <> {} & A is_limit_ordinal holds
for fi being Ordinal-Sequence st dom fi = A & ( for C being Ordinal st C in A holds
fi . C = C *^ B ) holds
A *^ B = sup fi
proof end;

theorem :: ORDINAL3: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 holds (A *^ B) *^ C = A *^ (B *^ C)
proof end;

definition
let A, B be Ordinal;
func A -^ B -> Ordinal means :Def6: :: ORDINAL3:def 6
A = B +^ it if B c= A
otherwise it = {} ;
existence
( ( B c= A implies ex b1 being Ordinal st A = B +^ b1 ) & ( not B c= A implies ex b1 being Ordinal st b1 = {} ) ) by Th30;
uniqueness
for b1, b2 being Ordinal holds
( ( B c= A & A = B +^ b1 & A = B +^ b2 implies b1 = b2 ) & ( not B c= A & b1 = {} & b2 = {} implies b1 = b2 ) ) by Th24;
consistency
for b1 being Ordinal holds verum ;
func A div^ B -> Ordinal means :Def7: :: ORDINAL3:def 7
 ex C being Ordinal st
( A = (it *^ B) +^ C & C in B ) if B <> {}
otherwise it = {} ;
consistency
for b1 being Ordinal holds verum ;
existence
( ( B <> {} implies ex b1, C being Ordinal st
( A = (b1 *^ B) +^ C & C in B ) ) & ( not B <> {} implies ex b1 being Ordinal st b1 = {} ) ) by Th55;
uniqueness
for b1, b2 being Ordinal holds
( ( B <> {} & ex C being Ordinal st
( A = (b1 *^ B) +^ C & C in B ) & ex C being Ordinal st
( A = (b2 *^ B) +^ C & C in B ) implies b1 = b2 ) & ( not B <> {} & b1 = {} & b2 = {} implies b1 = b2 ) ) by Th56;
end;

:: deftheorem Def6 defines -^ ORDINAL3:def 6 :
for A, B, b3 being Ordinal holds
( ( B c= A implies ( b3 = A -^ B iff A = B +^ b3 ) ) & ( not B c= A implies ( b3 = A -^ B iff b3 = {} ) ) );

:: deftheorem Def7 defines div^ ORDINAL3:def 7 :
for A, B, b3 being Ordinal holds
( ( B <> {} implies ( b3 = A div^ B iff ex C being Ordinal st
( A = (b3 *^ B) +^ C & C in B ) ) ) & ( not B <> {} implies ( b3 = A div^ B iff b3 = {} ) ) );

definition
let A, B be Ordinal;
func A mod^ B -> Ordinal equals :: ORDINAL3:def 8
A -^ ((A div^ B) *^ B);
correctness
coherence
A -^ ((A div^ B) *^ B) is Ordinal;
;
end;

:: deftheorem defines mod^ ORDINAL3:def 8 :
for A, B being Ordinal holds A mod^ B = A -^ ((A div^ B) *^ B);

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

theorem :: ORDINAL3:60  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 st A in B holds
B = A +^ (B -^ A)
proof end;

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

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

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

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

theorem Th65: :: ORDINAL3:65  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 +^ B) -^ A = B
proof end;

theorem Th66: :: ORDINAL3:66  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 & ( C c= A or C in A ) holds
A -^ C in B -^ C
proof end;

theorem Th67: :: ORDINAL3:67  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 :: ORDINAL3:68  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 st A in B holds
( B -^ A <> {} & {} in B -^ A )
proof end;

theorem Th69: :: ORDINAL3:69  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 & {} -^ A = {} )
proof end;

theorem :: ORDINAL3:70  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 holds A -^ (B +^ C) = (A -^ B) -^ C
proof end;

theorem :: ORDINAL3:71  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 -^ B c= C -^ A
proof end;

theorem :: ORDINAL3:72  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 :: ORDINAL3:73  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 +^ C holds
A -^ B in C
proof end;

theorem :: ORDINAL3:74  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 +^ B in C holds
B in C -^ A
proof end;

theorem :: ORDINAL3:75  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 +^ (A -^ B)
proof end;

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

theorem Th77: :: ORDINAL3:77  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 div^ B) *^ B c= A
proof end;

theorem Th78: :: ORDINAL3:78  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 = ((A div^ B) *^ B) +^ (A mod^ B)
proof end;

theorem :: ORDINAL3:79  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A, B, C, D being Ordinal st A = (B *^ C) +^ D & D in C holds
( B = A div^ C & D = A mod^ C )
proof end;

theorem :: ORDINAL3:80  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 *^ C holds
( A div^ C in B & A mod^ C in C )
proof end;

theorem Th81: :: ORDINAL3:81  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 <> {} holds
(A *^ B) div^ B = A
proof end;

theorem :: ORDINAL3:82  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 *^ B) mod^ B = {}
proof end;

theorem :: ORDINAL3:83  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
( {} div^ A = {} & {} mod^ A = {} & A mod^ {} = A )
proof end;

theorem :: ORDINAL3:84  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 div^ one = A & A mod^ one = {} )
proof end;