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

definition
mode Chain -> RelStr means :Def1: :: ORDERS_4:def 1
( it is non empty connected Poset or it is empty );
existence
ex b1 being RelStr st
( b1 is non empty connected Poset or b1 is empty )
proof end;
end;

:: deftheorem Def1 defines Chain ORDERS_4:def 1 :
for b1 being RelStr holds
( b1 is Chain iff ( b1 is non empty connected Poset or b1 is empty ) );

registration
cluster empty -> reflexive transitive antisymmetric RelStr ;
coherence
for b1 being RelStr st b1 is empty holds
( b1 is reflexive & b1 is transitive & b1 is antisymmetric )
proof end;
end;

registration
cluster -> reflexive transitive antisymmetric Chain ;
coherence
for b1 being Chain holds
( b1 is reflexive & b1 is transitive & b1 is antisymmetric )
proof end;
end;

registration
cluster non empty reflexive transitive antisymmetric Chain ;
existence
not for b1 being Chain holds b1 is empty
proof end;
end;

registration
cluster non empty -> non empty reflexive transitive antisymmetric connected Chain ;
coherence
for b1 being non empty Chain holds b1 is connected by Def1;
end;

definition
let L be 1-sorted ;
attr L is countable means :Def2: :: ORDERS_4:def 2
the carrier of L is countable;
end;

:: deftheorem Def2 defines countable ORDERS_4:def 2 :
for L being 1-sorted holds
( L is countable iff the carrier of L is countable );

registration
cluster non empty reflexive transitive antisymmetric connected finite Chain ;
existence
ex b1 being Chain st
( b1 is finite & not b1 is empty )
proof end;
end;

registration
cluster reflexive transitive antisymmetric countable Chain ;
existence
ex b1 being Chain st b1 is countable
proof end;
end;

registration
let A be non empty connected RelStr ;
cluster non empty full -> non empty connected SubRelStr of A;
correctness
coherence
for b1 being non empty SubRelStr of A st b1 is full holds
b1 is connected;
proof end;
end;

registration
let A be finite RelStr ;
cluster -> finite SubRelStr of A;
correctness
coherence
for b1 being SubRelStr of A holds b1 is finite;
proof end;
end;

theorem Th1: :: ORDERS_4:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n, m being Nat st n <= m holds
InclPoset n is full SubRelStr of InclPoset m
proof end;

definition
let L be RelStr ;
let A, B be set ;
pred A,B form_upper_lower_partition_of L means :Def3: :: ORDERS_4:def 3
( A \/ B = the carrier of L & ( for a, b being Element of L st a in A & b in B holds
a < b ) );
end;

:: deftheorem Def3 defines form_upper_lower_partition_of ORDERS_4:def 3 :
for L being RelStr
for A, B being set holds
( A,B form_upper_lower_partition_of L iff ( A \/ B = the carrier of L & ( for a, b being Element of L st a in A & b in B holds
a < b ) ) );

theorem Th2: :: ORDERS_4:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being RelStr
for A, B being set st A,B form_upper_lower_partition_of L holds
A misses B
proof end;

theorem Th3: :: ORDERS_4:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty antisymmetric upper-bounded RelStr holds the carrier of L \ {(Top L)},{(Top L)} form_upper_lower_partition_of L
proof end;

theorem Th4: :: ORDERS_4:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L1, L2 being RelStr
for f being Function of L1,L2 st f is isomorphic holds
( ( the carrier of L1 <> {} implies the carrier of L2 <> {} ) & ( the carrier of L2 <> {} implies the carrier of L1 <> {} ) & ( the carrier of L2 <> {} or the carrier of L1 = {} ) & ( the carrier of L1 = {} implies the carrier of L2 = {} ) & ( the carrier of L2 = {} implies the carrier of L1 = {} ) )
proof end;

theorem Th5: :: ORDERS_4:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L1, L2 being antisymmetric RelStr
for A1, B1 being Subset of L1 st A1,B1 form_upper_lower_partition_of L1 holds
for A2, B2 being Subset of L2 st A2,B2 form_upper_lower_partition_of L2 holds
for f being Function of (subrelstr A1),(subrelstr A2) st f is isomorphic holds
for g being Function of (subrelstr B1),(subrelstr B2) st g is isomorphic holds
ex h being Function of L1,L2 st
( h = f +* g & h is isomorphic )
proof end;

theorem :: ORDERS_4:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being finite Chain
for n being Nat st Card the carrier of A = n holds
A, InclPoset n are_isomorphic
proof end;