The abstract of the Mizar article:

Algebra of Normal Forms

by

Andrzej Trybulec

Received October 5, 1990

MML identifier: NORMFORM

[ Mizar article, MML identifier index ]

environ

 vocabulary BOOLE, FINSUB_1, MCART_1, BINOP_1, FUNCT_1, SETWISEO, RELAT_1,
      FINSET_1, FINSEQ_1, LATTICES, NORMFORM;
 notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, MCART_1, RELAT_1, FUNCT_2,
      FINSET_1, BINOP_1, DOMAIN_1, FINSUB_1, SETWISEO, STRUCT_0, LATTICES;
 constructors FINSET_1, BINOP_1, DOMAIN_1, SETWISEO, LATTICES, PARTFUN1,
      MEMBERED, XBOOLE_0;
 clusters FINSUB_1, LATTICES, RELSET_1, SUBSET_1, MEMBERED, ZFMISC_1, XBOOLE_0;
 requirements SUBSET, BOOLE;


begin

:: A u x i l i a r y   t h e o r e m s



:: Part 1. BOOLEan operations on pairs & relations between pairs

reserve A, B for non empty preBoolean set,
        x, y for Element of [:A,B:];

definition let A,B,x,y;
 pred x c= y means
:: NORMFORM:def 1
   x`1 c= y`1 & x`2 c= y`2;
 reflexivity;
 func x \/ y -> Element of [:A, B:] equals
:: NORMFORM:def 2
  [x`1 \/ y`1, x`2 \/ y`2];
  commutativity;
  idempotence;
 func x /\ y -> Element of [:A, B:] equals
:: NORMFORM:def 3
 [x`1 /\ y`1, x`2 /\ y`2];
  commutativity;
  idempotence;
 func x \ y -> Element of [:A, B:] equals
:: NORMFORM:def 4
  [x`1 \ y`1, x`2 \ y`2];
 func x \+\ y -> Element of [:A, B:] equals
:: NORMFORM:def 5
  [x`1 \+\ y`1, x`2 \+\ y`2];
  commutativity;
end;

reserve X for set,
        a,b,c for Element of [:A,B:];

canceled 3;

theorem :: NORMFORM:4
 a c= b & b c= a implies a = b;

theorem :: NORMFORM:5
 a c= b & b c= c implies a c= c;

canceled 4;

theorem :: NORMFORM:10
  (a \/ b)`1 = a`1 \/ b`1 & (a \/ b)`2 = a`2 \/ b`2;

theorem :: NORMFORM:11
  (a /\ b)`1 = a`1 /\ b`1 & (a /\ b)`2 = a`2 /\ b`2;

theorem :: NORMFORM:12
  (a \ b)`1 = a`1 \ b`1 & (a \ b)`2 = a`2 \ b`2;

theorem :: NORMFORM:13
    (a \+\ b)`1 = a`1 \+\ b`1 & (a \+\ b)`2 = a`2 \+\ b`2;

canceled 2;

theorem :: NORMFORM:16
  (a \/ b) \/ c = a \/ (b \/ c);

canceled 2;

theorem :: NORMFORM:19
    (a /\ b) /\ c = a /\ (b /\ c);

theorem :: NORMFORM:20
  a /\ (b \/ c) = a /\ b \/ a /\ c;

theorem :: NORMFORM:21
  a \/ (b /\ a) = a;

theorem :: NORMFORM:22
  a /\ (b \/ a) = a;

canceled;

theorem :: NORMFORM:24
    a \/ (b /\ c) = (a \/ b) /\ (a \/ c);

theorem :: NORMFORM:25
  a c= c & b c= c implies a \/ b c= c;

theorem :: NORMFORM:26
  a c= a \/ b & b c= a \/ b;

theorem :: NORMFORM:27
    a = a \/ b implies b c= a;

theorem :: NORMFORM:28
  a c= b implies c \/ a c= c \/ b & a \/ c c= b \/ c;

theorem :: NORMFORM:29
    a\b \/ b = a \/ b;

theorem :: NORMFORM:30
    a \ b c= c implies a c= b \/ c;

theorem :: NORMFORM:31
    a c= b \/ c implies a \ c c= b;

reserve a for Element of [:Fin X, Fin X:];

 definition let A be set;
  func FinPairUnion A -> BinOp of [:Fin A, Fin A:] means
:: NORMFORM:def 6
 for x,y being Element of [:Fin A, Fin A:] holds
        it.(x,y) = x \/ y;
 end;

reserve A for set;

definition let X be non empty set, A be set;
 let B be Element of Fin X; let f be Function of X, [:Fin A, Fin A:];
  func FinPairUnion(B,f) -> Element of [:Fin A, Fin A:] equals
:: NORMFORM:def 7
 FinPairUnion A $$(B,f);
end;

definition let A be set;
 cluster FinPairUnion A -> commutative idempotent associative;
end;

canceled 3;

theorem :: NORMFORM:35
   for X being non empty set for f being Function of X, [:Fin A,Fin A:]
  for B being Element of Fin X
   for x being Element of X st x in B holds f.x c= FinPairUnion(B,f);

theorem :: NORMFORM:36
 [{}.A, {}.A] is_a_unity_wrt FinPairUnion A;

theorem :: NORMFORM:37
 FinPairUnion A has_a_unity;

theorem :: NORMFORM:38
 the_unity_wrt FinPairUnion A = [{}.A, {}.A];

theorem :: NORMFORM:39
 for x being Element of [:Fin A, Fin A:] holds
  the_unity_wrt FinPairUnion A c= x;

theorem :: NORMFORM:40
   for X being non empty set
  for f being (Function of X,[:Fin A,Fin A:]), B being (Element of Fin X)
  for c being Element of [:Fin A, Fin A:] st
   for x being Element of X st x in B holds f.x c= c
    holds FinPairUnion(B,f) c= c;

theorem :: NORMFORM:41
   for X being non empty set, B being Element of Fin X
  for f,g being Function of X,[:Fin A,Fin A:] st f|B = g|B
   holds FinPairUnion(B,f) = FinPairUnion(B,g);

:: Part 2. Disjoint pairs of finite sets

definition let X;
 func DISJOINT_PAIRS(X) -> Subset of [:Fin X, Fin X:] equals
:: NORMFORM:def 8
 { a : a`1 misses a`2 };
end;

definition let X;
 cluster DISJOINT_PAIRS(X) -> non empty;
end;

theorem :: NORMFORM:42
 for y being Element of [:Fin X, Fin X:]
      holds y in DISJOINT_PAIRS X iff y`1 misses y`2;

 reserve x,y for Element of [:Fin X, Fin X:],
         a,b for Element of DISJOINT_PAIRS X;

theorem :: NORMFORM:43
    y in DISJOINT_PAIRS X & x in DISJOINT_PAIRS X implies
   (y \/ x in DISJOINT_PAIRS X iff y`1 /\ x`2 \/ x`1 /\ y`2 = {});

theorem :: NORMFORM:44
    a`1 misses a`2;

theorem :: NORMFORM:45
  x c= b implies x is Element of DISJOINT_PAIRS X;

theorem :: NORMFORM:46
 not (ex x being set st x in a`1 & x in a`2);

theorem :: NORMFORM:47
   not a \/ b in DISJOINT_PAIRS X implies
  ex p being Element of X st
   p in a`1 & p in b`2 or p in b`1 & p in a`2;

canceled;

theorem :: NORMFORM:49
   x`1 misses x`2 implies x is Element of DISJOINT_PAIRS X;

theorem :: NORMFORM:50
for V,W being set st V c= a`1 & W c= a`2
    holds [V,W] is Element of DISJOINT_PAIRS X;

 reserve A for set,
         x for Element of [:Fin A, Fin A:],
         a,b,c,d,s,t for Element of DISJOINT_PAIRS A,
         B,C,D for Element of Fin DISJOINT_PAIRS A;

definition let A;
  func Normal_forms_on A -> Subset of Fin DISJOINT_PAIRS A equals
:: NORMFORM:def 9
  { B : a in B & b in B & a c= b implies a = b};
end;

definition let A;
  cluster Normal_forms_on A -> non empty;
end;

 reserve K,L,M for Element of Normal_forms_on A;

theorem :: NORMFORM:51
  {} in Normal_forms_on A;

theorem :: NORMFORM:52
  B in Normal_forms_on A & a in B & b in B & a c= b implies a = b;

theorem :: NORMFORM:53
 (for a,b st a in B & b in B & a c= b holds a = b)
         implies B in Normal_forms_on A;

definition let A,B;
  func mi B -> Element of Normal_forms_on A equals
:: NORMFORM:def 10
  { t : s in B & s c= t iff s = t };
 let C;
  func B^C -> Element of Fin DISJOINT_PAIRS A equals
:: NORMFORM:def 11
  DISJOINT_PAIRS A /\ { s \/ t: s in B & t in C };
end;

canceled;

theorem :: NORMFORM:55
 x in B^C implies ex b,c st b in B & c in C & x = b \/ c;

theorem :: NORMFORM:56
 b in B & c in C & b \/ c in DISJOINT_PAIRS A implies b \/ c in B^C;

canceled;

theorem :: NORMFORM:58
  a in mi B implies a in B & (b in B & b c= a implies b = a);

theorem :: NORMFORM:59
    a in mi B implies a in B;

theorem :: NORMFORM:60
    a in mi B & b in B & b c= a implies b = a;

theorem :: NORMFORM:61
  a in B & (for b st b in B & b c= a holds b = a) implies a in mi B;

definition let A be non empty set;
 let B be non empty Subset of A;
 let O be BinOp of B;
 let a,b be Element of B;
 redefine func O.(a,b) -> Element of B;
end;

canceled 2;

theorem :: NORMFORM:64
  mi B c= B;

theorem :: NORMFORM:65
  b in B implies ex c st c c= b & c in mi B;

theorem :: NORMFORM:66
  mi K = K;

theorem :: NORMFORM:67
 mi (B \/ C) c= mi B \/ C;

theorem :: NORMFORM:68
 mi(mi B \/ C) = mi (B \/ C);

theorem :: NORMFORM:69
    mi(B \/ mi C) = mi (B \/ C);

theorem :: NORMFORM:70
 B c= C implies B ^ D c= C ^ D;

theorem :: NORMFORM:71
 mi(B ^ C) c= mi B ^ C;

theorem :: NORMFORM:72
 B^C = C^B;

theorem :: NORMFORM:73
 B c= C implies D ^ B c= D ^ C;

theorem :: NORMFORM:74
 mi(mi B ^ C) = mi (B ^ C);

theorem :: NORMFORM:75
 mi(B ^ mi C) = mi (B ^ C);

theorem :: NORMFORM:76
 K^(L^M) = K^L^M;

theorem :: NORMFORM:77
 K^(L \/ M) = K^L \/ K^M;

theorem :: NORMFORM:78
 B c= B ^ B;

theorem :: NORMFORM:79
 mi(K ^ K) = mi K;

definition let A;
 canceled 2;

 func NormForm A -> strict LattStr means
:: NORMFORM:def 14
  the carrier of it = Normal_forms_on A &
  for B, C being Element of Normal_forms_on A holds
    (the L_join of it).(B, C) = mi (B \/ C) &
    (the L_meet of it).(B, C) = mi (B^C);
 end;

definition let A;
  cluster NormForm A -> non empty;
end;

reserve K, L, M for Element of Normal_forms_on A;

definition let A;
  cluster NormForm A -> Lattice-like;
end;

definition let A;
  cluster NormForm A -> distributive lower-bounded;
end;

canceled 5;

theorem :: NORMFORM:85
   {} is Element of NormForm A;

theorem :: NORMFORM:86
   Bottom NormForm A = {};