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

theorem :: LATSUM_1:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y, A, B being set st x in A \/ B & y in A \/ B & not ( x in A \ B & y in A \ B ) & not ( x in B & y in B ) & not ( x in A \ B & y in B ) holds
( x in B & y in A \ B )
proof end;

definition
let R, S be RelStr ;
pred R tolerates S means :Def1: :: LATSUM_1:def 1
for x, y being set st x in the carrier of R /\ the carrier of S & y in the carrier of R /\ the carrier of S holds
( [x,y] in the InternalRel of R iff [x,y] in the InternalRel of S );
end;

:: deftheorem Def1 defines tolerates LATSUM_1:def 1 :
for R, S being RelStr holds
( R tolerates S iff for x, y being set st x in the carrier of R /\ the carrier of S & y in the carrier of R /\ the carrier of S holds
( [x,y] in the InternalRel of R iff [x,y] in the InternalRel of S ) );

definition
let R, S be RelStr ;
func R [*] S -> strict RelStr means :Def2: :: LATSUM_1:def 2
( the carrier of it = the carrier of R \/ the carrier of S & the InternalRel of it = (the InternalRel of R \/ the InternalRel of S) \/ (the InternalRel of R * the InternalRel of S) );
existence
ex b1 being strict RelStr st
( the carrier of b1 = the carrier of R \/ the carrier of S & the InternalRel of b1 = (the InternalRel of R \/ the InternalRel of S) \/ (the InternalRel of R * the InternalRel of S) )
proof end;
uniqueness
for b1, b2 being strict RelStr st the carrier of b1 = the carrier of R \/ the carrier of S & the InternalRel of b1 = (the InternalRel of R \/ the InternalRel of S) \/ (the InternalRel of R * the InternalRel of S) & the carrier of b2 = the carrier of R \/ the carrier of S & the InternalRel of b2 = (the InternalRel of R \/ the InternalRel of S) \/ (the InternalRel of R * the InternalRel of S) holds
b1 = b2
;
end;

:: deftheorem Def2 defines [*] LATSUM_1:def 2 :
for R, S being RelStr
for b3 being strict RelStr holds
( b3 = R [*] S iff ( the carrier of b3 = the carrier of R \/ the carrier of S & the InternalRel of b3 = (the InternalRel of R \/ the InternalRel of S) \/ (the InternalRel of R * the InternalRel of S) ) );

registration
let R be RelStr ;
let S be non empty RelStr ;
cluster R [*] S -> non empty strict ;
coherence
not R [*] S is empty
proof end;
end;

registration
let R be non empty RelStr ;
let S be RelStr ;
cluster R [*] S -> non empty strict ;
coherence
not R [*] S is empty
proof end;
end;

theorem Th2: :: LATSUM_1:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for R, S being RelStr holds
( the InternalRel of R c= the InternalRel of (R [*] S) & the InternalRel of S c= the InternalRel of (R [*] S) )
proof end;

theorem Th3: :: LATSUM_1:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for R, S being RelStr st R is reflexive & S is reflexive holds
R [*] S is reflexive
proof end;

theorem Th4: :: LATSUM_1:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for R, S being RelStr
for a, b being set st [a,b] in the InternalRel of (R [*] S) & a in the carrier of R & b in the carrier of R & R tolerates S & R is transitive holds
[a,b] in the InternalRel of R
proof end;

theorem Th5: :: LATSUM_1:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for R, S being RelStr
for a, b being set st [a,b] in the InternalRel of (R [*] S) & a in the carrier of S & b in the carrier of S & R tolerates S & S is transitive holds
[a,b] in the InternalRel of S
proof end;

theorem Th6: :: LATSUM_1:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for R, S being RelStr
for a, b being set holds
( ( [a,b] in the InternalRel of R implies [a,b] in the InternalRel of (R [*] S) ) & ( [a,b] in the InternalRel of S implies [a,b] in the InternalRel of (R [*] S) ) )
proof end;

theorem :: LATSUM_1:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for R, S being non empty RelStr
for x being Element of (R [*] S) holds
( x in the carrier of R or x in the carrier of S \ the carrier of R )
proof end;

theorem Th8: :: LATSUM_1:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for R, S being non empty RelStr
for x, y being Element of R
for a, b being Element of (R [*] S) st x = a & y = b & R tolerates S & R is transitive holds
( x <= y iff a <= b )
proof end;

theorem Th9: :: LATSUM_1:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for R, S being non empty RelStr
for a, b being Element of (R [*] S)
for c, d being Element of S st a = c & b = d & R tolerates S & S is transitive holds
( a <= b iff c <= d )
proof end;

theorem Th10: :: LATSUM_1:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for R, S being non empty reflexive transitive antisymmetric with_suprema RelStr
for x being set st x in the carrier of R holds
x is Element of (R [*] S)
proof end;

theorem :: LATSUM_1:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for R, S being non empty reflexive transitive antisymmetric with_suprema RelStr
for x being set st x in the carrier of S holds
x is Element of (R [*] S)
proof end;

theorem Th12: :: LATSUM_1:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for R, S being non empty RelStr
for x being set st x in the carrier of R /\ the carrier of S holds
x is Element of R
proof end;

theorem Th13: :: LATSUM_1:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for R, S being non empty RelStr
for x being set st x in the carrier of R /\ the carrier of S holds
x is Element of S
proof end;

theorem :: LATSUM_1:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for R, S being non empty reflexive transitive antisymmetric with_suprema RelStr
for x, y being Element of (R [*] S) st x in the carrier of R & y in the carrier of S & R tolerates S holds
( x <= y iff ex a being Element of (R [*] S) st
( a in the carrier of R /\ the carrier of S & x <= a & a <= y ) )
proof end;

theorem Th15: :: LATSUM_1:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for R, S being non empty RelStr
for a, b being Element of R
for c, d being Element of S st a = c & b = d & R tolerates S & R is transitive & S is transitive holds
( a <= b iff c <= d )
proof end;

theorem Th16: :: LATSUM_1:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for R being non empty reflexive transitive antisymmetric with_suprema RelStr
for D being directed lower Subset of R
for x, y being Element of R st x in D & y in D holds
x "\/" y in D
proof end;

theorem Th17: :: LATSUM_1:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for R, S being RelStr
for a, b being set st the carrier of R /\ the carrier of S is upper Subset of R & [a,b] in the InternalRel of (R [*] S) & a in the carrier of S holds
b in the carrier of S
proof end;

theorem Th18: :: LATSUM_1:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for R, S being RelStr
for a, b being Element of (R [*] S) st the carrier of R /\ the carrier of S is upper Subset of R & a <= b & a in the carrier of S holds
b in the carrier of S
proof end;

theorem :: LATSUM_1:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for R, S being non empty reflexive transitive antisymmetric with_suprema RelStr
for x, y being Element of R
for a, b being Element of S st the carrier of R /\ the carrier of S is directed lower Subset of S & the carrier of R /\ the carrier of S is upper Subset of R & R tolerates S & x = a & y = b holds
x "\/" y = a "\/" b
proof end;

theorem :: LATSUM_1:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for R, S being non empty reflexive transitive antisymmetric lower-bounded with_suprema RelStr st the carrier of R /\ the carrier of S is non empty directed lower Subset of S holds
Bottom S in the carrier of R
proof end;

theorem Th21: :: LATSUM_1:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for R, S being RelStr
for a, b being set st the carrier of R /\ the carrier of S is lower Subset of S & [a,b] in the InternalRel of (R [*] S) & b in the carrier of R holds
a in the carrier of R
proof end;

theorem :: LATSUM_1:22  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
for R, S being RelStr st [x,y] in the InternalRel of (R [*] S) & the carrier of R /\ the carrier of S is upper Subset of R & not ( x in the carrier of R & y in the carrier of R ) & not ( x in the carrier of S & y in the carrier of S ) holds
( x in the carrier of R \ the carrier of S & y in the carrier of S \ the carrier of R )
proof end;

theorem :: LATSUM_1:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for R, S being RelStr
for a, b being Element of (R [*] S) st the carrier of R /\ the carrier of S is lower Subset of S & a <= b & b in the carrier of R holds
a in the carrier of R
proof end;

theorem :: LATSUM_1:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for R, S being RelStr st R tolerates S & the carrier of R /\ the carrier of S is upper Subset of R & the carrier of R /\ the carrier of S is lower Subset of S & R is transitive & R is antisymmetric & S is transitive & S is antisymmetric holds
R [*] S is antisymmetric
proof end;

theorem :: LATSUM_1:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for R, S being RelStr st the carrier of R /\ the carrier of S is upper Subset of R & the carrier of R /\ the carrier of S is lower Subset of S & R tolerates S & R is transitive & S is transitive holds
R [*] S is transitive
proof end;