:: The Operation of Addition of Relational Structures
:: by Katarzyna Romanowicz and Adam Grabowski
::
:: Received May 24, 2004
:: Copyright (c) 2004-2012 Association of Mizar Users


begin

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

begin

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
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
for R, S being RelStr st R is reflexive & S is reflexive holds
R [*] S is reflexive
proof end;

begin

theorem Th4: :: LATSUM_1:4
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
for R, S being non empty reflexive transitive antisymmetric with_suprema lower-bounded 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
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
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
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
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
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;