:: The Operation of Addition of Relational Structures
::  by Katarzyna Romanowicz and Adam Grabowski
::
:: Received May 24, 2004
:: Copyright (c) 2004-2021 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies XBOOLE_0, ORDERS_2, PARTFUN1, STRUCT_0, FINSEQ_1, RELAT_1,
      TARSKI, RELAT_2, SUBSET_1, XXREAL_0, LATTICE3, WAYBEL_0, EQREL_1,
      LATTICES;
 notations XBOOLE_0, TARSKI, SUBSET_1, RELSET_1, RELAT_2, STRUCT_0, ORDERS_2,
      YELLOW_0, WAYBEL_0, LATTICE3;
 constructors LATTICE3, WAYBEL_0, RELSET_1;
 registrations XBOOLE_0, RELSET_1, STRUCT_0, WAYBEL_0;
 requirements SUBSET, BOOLE;


begin

theorem :: LATSUM_1:1
  for x, y, A, B being set st x in A \/ B & y in A \/ B holds x in A \ B
  & y in A \ B or x in B & y in B or x in A \ B & y in B or x in B & y in A \ B
;

definition
  let R, S be RelStr;
  pred R tolerates S means
:: 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;

begin

definition
  let R, S be RelStr; :: Wronski Sum Operation
  func R [*] S -> strict RelStr means
:: 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);
end;

registration
  let R be RelStr, S be non empty RelStr;
  cluster R [*] S -> non empty;
end;

registration
  let R be non empty RelStr, S be RelStr;
  cluster R [*] S -> non empty;
end;

theorem :: 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;

theorem :: LATSUM_1:3
  for R, S being RelStr st R is reflexive & S is reflexive holds R
  [*] S is reflexive;

begin

theorem :: LATSUM_1:4  :: theorem 3.1 (vii)
  for R, S being RelStr, 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;

theorem :: LATSUM_1:5  :: theorem 3.1 (viii)
  for R, S being RelStr, 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;

theorem :: LATSUM_1:6  :: a version of 3.1 (vii, viii - left to right)
  for R, S being RelStr, a, b being object 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);

theorem :: LATSUM_1:7
  for R, S being non empty RelStr, x being Element of R [*] S holds x in
  the carrier of R or x in (the carrier of S) \ (the carrier of R);

theorem :: LATSUM_1:8  :: theorem 3.1 (vii)
  for R, S being non empty RelStr for x, y being Element of R, a, b
  being Element of R [*] S st x = a & y = b & R tolerates S & R is transitive
  holds x <= y iff a <= b;

theorem :: LATSUM_1:9  :: theorem 3.1 (viii)
  for R, S being non empty RelStr, a, b being Element of R [*] S, c
, d being Element of S st a = c & b = d & R tolerates S & S is transitive holds
  a <= b iff c <= d;

theorem :: LATSUM_1:10
  for R, S being antisymmetric reflexive transitive with_suprema
  non empty RelStr for x being set st x in the carrier of R holds x is Element
  of R [*] S;

theorem :: LATSUM_1:11
  for R, S being antisymmetric reflexive transitive with_suprema non
empty RelStr for x being set st x in the carrier of S holds x is Element of R
  [*] S;

theorem :: 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;

theorem :: 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;

theorem :: LATSUM_1:14
  for R, S being antisymmetric reflexive transitive with_suprema non
empty 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);

theorem :: LATSUM_1:15
  for R, S being non empty RelStr, a, b being Element of R, 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;

theorem :: LATSUM_1:16
  for R being antisymmetric reflexive transitive with_suprema non
  empty RelStr, D being lower directed Subset of R for x, y being Element of R
  st x in D & y in D holds x "\/" y in D;

theorem :: LATSUM_1:17
  for R, S being RelStr, 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;

theorem :: LATSUM_1:18  :: theorem 3.1 (xi)
  for R, S being RelStr, 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;

theorem :: LATSUM_1:19 :: theorem 3.1 (vi)
  for R, S being antisymmetric reflexive transitive with_suprema non
  empty RelStr for x, y being Element of R, a, b being Element of S st (the
  carrier of R) /\ (the carrier of S) is lower directed 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;

theorem :: LATSUM_1:20
  for R, S being lower-bounded antisymmetric reflexive transitive
with_suprema non empty RelStr st (the carrier of R) /\ (the carrier of S) is
  non empty lower directed Subset of S holds Bottom S in the carrier of R;

theorem :: LATSUM_1:21
  for R, S being RelStr, 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;

theorem :: LATSUM_1:22 :: theorem 1 (ix)
  for x, y being set, 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 holds x
in the carrier of R & y in the carrier of R or x in the carrier of S & y in the
  carrier of S or x in (the carrier of R) \ (the carrier of S) & y in (the
  carrier of S) \ (the carrier of R);

theorem :: LATSUM_1:23 :: theorem 3.1 (x)
  for R, S being RelStr, 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;

theorem :: LATSUM_1:24 :: theorem 3.1 (xii)
  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 antisymmetric & S is transitive
  antisymmetric holds R [*] S is antisymmetric;

theorem :: LATSUM_1:25 :: theorem 3.1 (xiii)
  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;