:: by Andrzej Trybulec

::

:: Received October 5, 1990

:: Copyright (c) 1990-2016 Association of Mizar Users

definition

let A, B be non empty preBoolean set ;

let x, y be Element of [:A,B:];

reflexivity

for x being Element of [:A,B:] holds

( x `1 c= x `1 & x `2 c= x `2 ) ;

correctness

coherence

[((x `1) \/ (y `1)),((x `2) \/ (y `2))] is Element of [:A,B:];

;

commutativity

for b_{1}, x, y being Element of [:A,B:] st b_{1} = [((x `1) \/ (y `1)),((x `2) \/ (y `2))] holds

b_{1} = [((y `1) \/ (x `1)),((y `2) \/ (x `2))]
;

idempotence

for x being Element of [:A,B:] holds x = [((x `1) \/ (x `1)),((x `2) \/ (x `2))] by MCART_1:21;

correctness

coherence

[((x `1) /\ (y `1)),((x `2) /\ (y `2))] is Element of [:A,B:];

;

commutativity

for b_{1}, x, y being Element of [:A,B:] st b_{1} = [((x `1) /\ (y `1)),((x `2) /\ (y `2))] holds

b_{1} = [((y `1) /\ (x `1)),((y `2) /\ (x `2))]
;

idempotence

for x being Element of [:A,B:] holds x = [((x `1) /\ (x `1)),((x `2) /\ (x `2))] by MCART_1:21;

correctness

coherence

[((x `1) \ (y `1)),((x `2) \ (y `2))] is Element of [:A,B:];

;

coherence

[((x `1) \+\ (y `1)),((x `2) \+\ (y `2))] is Element of [:A,B:];

;

commutativity

for b_{1}, x, y being Element of [:A,B:] st b_{1} = [((x `1) \+\ (y `1)),((x `2) \+\ (y `2))] holds

b_{1} = [((y `1) \+\ (x `1)),((y `2) \+\ (x `2))]
;

end;
let x, y be Element of [:A,B:];

reflexivity

for x being Element of [:A,B:] holds

( x `1 c= x `1 & x `2 c= x `2 ) ;

correctness

coherence

[((x `1) \/ (y `1)),((x `2) \/ (y `2))] is Element of [:A,B:];

;

commutativity

for b

b

idempotence

for x being Element of [:A,B:] holds x = [((x `1) \/ (x `1)),((x `2) \/ (x `2))] by MCART_1:21;

correctness

coherence

[((x `1) /\ (y `1)),((x `2) /\ (y `2))] is Element of [:A,B:];

;

commutativity

for b

b

idempotence

for x being Element of [:A,B:] holds x = [((x `1) /\ (x `1)),((x `2) /\ (x `2))] by MCART_1:21;

correctness

coherence

[((x `1) \ (y `1)),((x `2) \ (y `2))] is Element of [:A,B:];

;

func x \+\ y -> Element of [:A,B:] equals :: NORMFORM:def 5

[((x `1) \+\ (y `1)),((x `2) \+\ (y `2))];

correctness [((x `1) \+\ (y `1)),((x `2) \+\ (y `2))];

coherence

[((x `1) \+\ (y `1)),((x `2) \+\ (y `2))] is Element of [:A,B:];

;

commutativity

for b

b

:: deftheorem defines c= NORMFORM:def 1 :

for A, B being non empty preBoolean set

for x, y being Element of [:A,B:] holds

( x c= y iff ( x `1 c= y `1 & x `2 c= y `2 ) );

for A, B being non empty preBoolean set

for x, y being Element of [:A,B:] holds

( x c= y iff ( x `1 c= y `1 & x `2 c= y `2 ) );

:: deftheorem defines \/ NORMFORM:def 2 :

for A, B being non empty preBoolean set

for x, y being Element of [:A,B:] holds x \/ y = [((x `1) \/ (y `1)),((x `2) \/ (y `2))];

for A, B being non empty preBoolean set

for x, y being Element of [:A,B:] holds x \/ y = [((x `1) \/ (y `1)),((x `2) \/ (y `2))];

:: deftheorem defines /\ NORMFORM:def 3 :

for A, B being non empty preBoolean set

for x, y being Element of [:A,B:] holds x /\ y = [((x `1) /\ (y `1)),((x `2) /\ (y `2))];

for A, B being non empty preBoolean set

for x, y being Element of [:A,B:] holds x /\ y = [((x `1) /\ (y `1)),((x `2) /\ (y `2))];

:: deftheorem defines \ NORMFORM:def 4 :

for A, B being non empty preBoolean set

for x, y being Element of [:A,B:] holds x \ y = [((x `1) \ (y `1)),((x `2) \ (y `2))];

for A, B being non empty preBoolean set

for x, y being Element of [:A,B:] holds x \ y = [((x `1) \ (y `1)),((x `2) \ (y `2))];

:: deftheorem defines \+\ NORMFORM:def 5 :

for A, B being non empty preBoolean set

for x, y being Element of [:A,B:] holds x \+\ y = [((x `1) \+\ (y `1)),((x `2) \+\ (y `2))];

for A, B being non empty preBoolean set

for x, y being Element of [:A,B:] holds x \+\ y = [((x `1) \+\ (y `1)),((x `2) \+\ (y `2))];

theorem Th1: :: NORMFORM:1

for A, B being non empty preBoolean set

for a, b being Element of [:A,B:] st a c= b & b c= a holds

a = b

for a, b being Element of [:A,B:] st a c= b & b c= a holds

a = b

proof end;

theorem Th2: :: NORMFORM:2

for A, B being non empty preBoolean set

for a, b, c being Element of [:A,B:] st a c= b & b c= c holds

a c= c

for a, b, c being Element of [:A,B:] st a c= b & b c= c holds

a c= c

proof end;

theorem Th3: :: NORMFORM:3

for A, B being non empty preBoolean set

for a, b, c being Element of [:A,B:] holds (a \/ b) \/ c = a \/ (b \/ c)

for a, b, c being Element of [:A,B:] holds (a \/ b) \/ c = a \/ (b \/ c)

proof end;

theorem :: NORMFORM:4

for A, B being non empty preBoolean set

for a, b, c being Element of [:A,B:] holds (a /\ b) /\ c = a /\ (b /\ c)

for a, b, c being Element of [:A,B:] holds (a /\ b) /\ c = a /\ (b /\ c)

proof end;

theorem Th5: :: NORMFORM:5

for A, B being non empty preBoolean set

for a, b, c being Element of [:A,B:] holds a /\ (b \/ c) = (a /\ b) \/ (a /\ c)

for a, b, c being Element of [:A,B:] holds a /\ (b \/ c) = (a /\ b) \/ (a /\ c)

proof end;

theorem :: NORMFORM:8

for A, B being non empty preBoolean set

for a, b, c being Element of [:A,B:] holds a \/ (b /\ c) = (a \/ b) /\ (a \/ c)

for a, b, c being Element of [:A,B:] holds a \/ (b /\ c) = (a \/ b) /\ (a \/ c)

proof end;

theorem :: NORMFORM:11

theorem :: NORMFORM:13

for A, B being non empty preBoolean set

for a, b being Element of [:A,B:] holds (a \ b) \/ b = a \/ b

for a, b being Element of [:A,B:] holds (a \ b) \/ b = a \/ b

proof end;

theorem :: NORMFORM:14

theorem :: NORMFORM:15

definition

let A be set ;

ex b_{1} being BinOp of [:(Fin A),(Fin A):] st

for x, y being Element of [:(Fin A),(Fin A):] holds b_{1} . (x,y) = x \/ y

for b_{1}, b_{2} being BinOp of [:(Fin A),(Fin A):] st ( for x, y being Element of [:(Fin A),(Fin A):] holds b_{1} . (x,y) = x \/ y ) & ( for x, y being Element of [:(Fin A),(Fin A):] holds b_{2} . (x,y) = x \/ y ) holds

b_{1} = b_{2}

end;
func FinPairUnion A -> BinOp of [:(Fin A),(Fin A):] means :Def6: :: NORMFORM:def 6

for x, y being Element of [:(Fin A),(Fin A):] holds it . (x,y) = x \/ y;

existence for x, y being Element of [:(Fin A),(Fin A):] holds it . (x,y) = x \/ y;

ex b

for x, y being Element of [:(Fin A),(Fin A):] holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def6 defines FinPairUnion NORMFORM:def 6 :

for A being set

for b_{2} being BinOp of [:(Fin A),(Fin A):] holds

( b_{2} = FinPairUnion A iff for x, y being Element of [:(Fin A),(Fin A):] holds b_{2} . (x,y) = x \/ y );

for A being set

for b

( b

definition

let X be non empty set ;

let A be set ;

let B be Element of Fin X;

let f be Function of X,[:(Fin A),(Fin A):];

coherence

(FinPairUnion A) $$ (B,f) is Element of [:(Fin A),(Fin A):];

;

end;
let 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);

correctness (FinPairUnion A) $$ (B,f);

coherence

(FinPairUnion A) $$ (B,f) is Element of [:(Fin A),(Fin A):];

;

:: deftheorem defines FinPairUnion NORMFORM:def 7 :

for X being non empty set

for A being set

for B being Element of Fin X

for f being Function of X,[:(Fin A),(Fin A):] holds FinPairUnion (B,f) = (FinPairUnion A) $$ (B,f);

for X being non empty set

for A being set

for B being Element of Fin X

for f being Function of X,[:(Fin A),(Fin A):] holds FinPairUnion (B,f) = (FinPairUnion A) $$ (B,f);

Lm1: for A being set holds FinPairUnion A is idempotent

proof end;

Lm2: for A being set holds FinPairUnion A is commutative

proof end;

Lm3: for A being set holds FinPairUnion A is associative

proof end;

registration

let A be set ;

coherence

( FinPairUnion A is commutative & FinPairUnion A is idempotent & FinPairUnion A is associative ) by Lm1, Lm2, Lm3;

end;
coherence

( FinPairUnion A is commutative & FinPairUnion A is idempotent & FinPairUnion A is associative ) by Lm1, Lm2, Lm3;

theorem :: NORMFORM:16

for A being set

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)

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)

proof end;

theorem Th20: :: NORMFORM:20

for A being set

for x being Element of [:(Fin A),(Fin A):] holds the_unity_wrt (FinPairUnion A) c= x

for x being Element of [:(Fin A),(Fin A):] holds the_unity_wrt (FinPairUnion A) c= x

proof end;

theorem :: NORMFORM:21

for A being set

for X being non empty set

for f being Function of X,[:(Fin A),(Fin A):]

for 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

for X being non empty set

for f being Function of X,[:(Fin A),(Fin A):]

for 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

proof end;

theorem :: NORMFORM:22

for A being set

for X being non empty set

for 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)

for X being non empty set

for 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)

proof end;

:: Part 2. Disjoint pairs of finite sets

definition

let X be set ;

{ a where a is Element of [:(Fin X),(Fin X):] : a `1 misses a `2 } is Subset of [:(Fin X),(Fin X):]

end;
func DISJOINT_PAIRS X -> Subset of [:(Fin X),(Fin X):] equals :: NORMFORM:def 8

{ a where a is Element of [:(Fin X),(Fin X):] : a `1 misses a `2 } ;

coherence { a where a is Element of [:(Fin X),(Fin X):] : a `1 misses a `2 } ;

{ a where a is Element of [:(Fin X),(Fin X):] : a `1 misses a `2 } is Subset of [:(Fin X),(Fin X):]

proof end;

:: deftheorem defines DISJOINT_PAIRS NORMFORM:def 8 :

for X being set holds DISJOINT_PAIRS X = { a where a is Element of [:(Fin X),(Fin X):] : a `1 misses a `2 } ;

for X being set holds DISJOINT_PAIRS X = { a where a is Element of [:(Fin X),(Fin X):] : a `1 misses a `2 } ;

theorem Th23: :: NORMFORM:23

for X being set

for y being Element of [:(Fin X),(Fin X):] holds

( y in DISJOINT_PAIRS X iff y `1 misses y `2 )

for y being Element of [:(Fin X),(Fin X):] holds

( y in DISJOINT_PAIRS X iff y `1 misses y `2 )

proof end;

theorem :: NORMFORM:24

for X being set

for x, y being Element of [:(Fin X),(Fin X):] st y in DISJOINT_PAIRS X & x in DISJOINT_PAIRS X holds

( y \/ x in DISJOINT_PAIRS X iff ((y `1) /\ (x `2)) \/ ((x `1) /\ (y `2)) = {} )

for x, y being Element of [:(Fin X),(Fin X):] st y in DISJOINT_PAIRS X & x in DISJOINT_PAIRS X holds

( y \/ x in DISJOINT_PAIRS X iff ((y `1) /\ (x `2)) \/ ((x `1) /\ (y `2)) = {} )

proof end;

theorem :: NORMFORM:25

theorem Th26: :: NORMFORM:26

for X being set

for x being Element of [:(Fin X),(Fin X):]

for b being Element of DISJOINT_PAIRS X st x c= b holds

x is Element of DISJOINT_PAIRS X

for x being Element of [:(Fin X),(Fin X):]

for b being Element of DISJOINT_PAIRS X st x c= b holds

x is Element of DISJOINT_PAIRS X

proof end;

theorem Th27: :: NORMFORM:27

for X being set

for a being Element of DISJOINT_PAIRS X

for x being set holds

( not x in a `1 or not x in a `2 ) by Th23, XBOOLE_0:3;

for a being Element of DISJOINT_PAIRS X

for x being set holds

( not x in a `1 or not x in a `2 ) by Th23, XBOOLE_0:3;

theorem :: NORMFORM:28

for X being set

for a, b being Element of DISJOINT_PAIRS X st not a \/ b in DISJOINT_PAIRS X holds

ex p being Element of X st

( ( p in a `1 & p in b `2 ) or ( p in b `1 & p in a `2 ) )

for a, b being Element of DISJOINT_PAIRS X st not a \/ b in DISJOINT_PAIRS X holds

ex p being Element of X st

( ( p in a `1 & p in b `2 ) or ( p in b `1 & p in a `2 ) )

proof end;

theorem :: NORMFORM:29

theorem :: NORMFORM:30

for X being set

for a being Element of DISJOINT_PAIRS X

for V, W being set st V c= a `1 & W c= a `2 holds

[V,W] is Element of DISJOINT_PAIRS X

for a being Element of DISJOINT_PAIRS X

for V, W being set st V c= a `1 & W c= a `2 holds

[V,W] is Element of DISJOINT_PAIRS X

proof end;

Lm4: for A being set holds {} in { B where B is Element of Fin (DISJOINT_PAIRS A) : for a, b being Element of DISJOINT_PAIRS A st a in B & b in B & a c= b holds

a = b }

proof end;

definition

let A be set ;

{ B where B is Element of Fin (DISJOINT_PAIRS A) : for a, b being Element of DISJOINT_PAIRS A st a in B & b in B & a c= b holds

a = b } is Subset of (Fin (DISJOINT_PAIRS A))

end;
func Normal_forms_on A -> Subset of (Fin (DISJOINT_PAIRS A)) equals :: NORMFORM:def 9

{ B where B is Element of Fin (DISJOINT_PAIRS A) : for a, b being Element of DISJOINT_PAIRS A st a in B & b in B & a c= b holds

a = b } ;

coherence { B where B is Element of Fin (DISJOINT_PAIRS A) : for a, b being Element of DISJOINT_PAIRS A st a in B & b in B & a c= b holds

a = b } ;

{ B where B is Element of Fin (DISJOINT_PAIRS A) : for a, b being Element of DISJOINT_PAIRS A st a in B & b in B & a c= b holds

a = b } is Subset of (Fin (DISJOINT_PAIRS A))

proof end;

:: deftheorem defines Normal_forms_on NORMFORM:def 9 :

for A being set holds Normal_forms_on A = { B where B is Element of Fin (DISJOINT_PAIRS A) : for a, b being Element of DISJOINT_PAIRS A st a in B & b in B & a c= b holds

a = b } ;

for A being set holds Normal_forms_on A = { B where B is Element of Fin (DISJOINT_PAIRS A) : for a, b being Element of DISJOINT_PAIRS A st a in B & b in B & a c= b holds

a = b } ;

theorem Th32: :: NORMFORM:32

for A being set

for a, b being Element of DISJOINT_PAIRS A

for B being Element of Fin (DISJOINT_PAIRS A) st B in Normal_forms_on A & a in B & b in B & a c= b holds

a = b

for a, b being Element of DISJOINT_PAIRS A

for B being Element of Fin (DISJOINT_PAIRS A) st B in Normal_forms_on A & a in B & b in B & a c= b holds

a = b

proof end;

theorem Th33: :: NORMFORM:33

for A being set

for B being Element of Fin (DISJOINT_PAIRS A) st ( for a, b being Element of DISJOINT_PAIRS A st a in B & b in B & a c= b holds

a = b ) holds

B in Normal_forms_on A ;

for B being Element of Fin (DISJOINT_PAIRS A) st ( for a, b being Element of DISJOINT_PAIRS A st a in B & b in B & a c= b holds

a = b ) holds

B in Normal_forms_on A ;

definition

let A be set ;

let B be Element of Fin (DISJOINT_PAIRS A);

{ t where t is Element of DISJOINT_PAIRS A : for s being Element of DISJOINT_PAIRS A holds

( ( s in B & s c= t ) iff s = t ) } is Element of Normal_forms_on A

;

let C be Element of Fin (DISJOINT_PAIRS A);

(DISJOINT_PAIRS A) /\ { (s \/ t) where s, t is Element of DISJOINT_PAIRS A : ( s in B & t in C ) } is Element of Fin (DISJOINT_PAIRS A)

;

end;
let B be Element of Fin (DISJOINT_PAIRS A);

func mi B -> Element of Normal_forms_on A equals :: NORMFORM:def 10

{ t where t is Element of DISJOINT_PAIRS A : for s being Element of DISJOINT_PAIRS A holds

( ( s in B & s c= t ) iff s = t ) } ;

coherence { t where t is Element of DISJOINT_PAIRS A : for s being Element of DISJOINT_PAIRS A holds

( ( s in B & s c= t ) iff s = t ) } ;

{ t where t is Element of DISJOINT_PAIRS A : for s being Element of DISJOINT_PAIRS A holds

( ( s in B & s c= t ) iff s = t ) } is Element of Normal_forms_on A

proof end;

correctness ;

let C be Element of Fin (DISJOINT_PAIRS A);

func B ^ C -> Element of Fin (DISJOINT_PAIRS A) equals :: NORMFORM:def 11

(DISJOINT_PAIRS A) /\ { (s \/ t) where s, t is Element of DISJOINT_PAIRS A : ( s in B & t in C ) } ;

coherence (DISJOINT_PAIRS A) /\ { (s \/ t) where s, t is Element of DISJOINT_PAIRS A : ( s in B & t in C ) } ;

(DISJOINT_PAIRS A) /\ { (s \/ t) where s, t is Element of DISJOINT_PAIRS A : ( s in B & t in C ) } is Element of Fin (DISJOINT_PAIRS A)

proof end;

correctness ;

:: deftheorem defines mi NORMFORM:def 10 :

for A being set

for B being Element of Fin (DISJOINT_PAIRS A) holds mi B = { t where t is Element of DISJOINT_PAIRS A : for s being Element of DISJOINT_PAIRS A holds

( ( s in B & s c= t ) iff s = t ) } ;

for A being set

for B being Element of Fin (DISJOINT_PAIRS A) holds mi B = { t where t is Element of DISJOINT_PAIRS A : for s being Element of DISJOINT_PAIRS A holds

( ( s in B & s c= t ) iff s = t ) } ;

:: deftheorem defines ^ NORMFORM:def 11 :

for A being set

for B, C being Element of Fin (DISJOINT_PAIRS A) holds B ^ C = (DISJOINT_PAIRS A) /\ { (s \/ t) where s, t is Element of DISJOINT_PAIRS A : ( s in B & t in C ) } ;

for A being set

for B, C being Element of Fin (DISJOINT_PAIRS A) holds B ^ C = (DISJOINT_PAIRS A) /\ { (s \/ t) where s, t is Element of DISJOINT_PAIRS A : ( s in B & t in C ) } ;

theorem Th34: :: NORMFORM:34

for A being set

for x being Element of [:(Fin A),(Fin A):]

for B, C being Element of Fin (DISJOINT_PAIRS A) st x in B ^ C holds

ex b, c being Element of DISJOINT_PAIRS A st

( b in B & c in C & x = b \/ c )

for x being Element of [:(Fin A),(Fin A):]

for B, C being Element of Fin (DISJOINT_PAIRS A) st x in B ^ C holds

ex b, c being Element of DISJOINT_PAIRS A st

( b in B & c in C & x = b \/ c )

proof end;

theorem Th35: :: NORMFORM:35

for A being set

for b, c being Element of DISJOINT_PAIRS A

for B, C being Element of Fin (DISJOINT_PAIRS A) st b in B & c in C & b \/ c in DISJOINT_PAIRS A holds

b \/ c in B ^ C

for b, c being Element of DISJOINT_PAIRS A

for B, C being Element of Fin (DISJOINT_PAIRS A) st b in B & c in C & b \/ c in DISJOINT_PAIRS A holds

b \/ c in B ^ C

proof end;

theorem Th36: :: NORMFORM:36

for A being set

for a, b being Element of DISJOINT_PAIRS A

for B being Element of Fin (DISJOINT_PAIRS A) st a in mi B holds

( a in B & ( b in B & b c= a implies b = a ) )

for a, b being Element of DISJOINT_PAIRS A

for B being Element of Fin (DISJOINT_PAIRS A) st a in mi B holds

( a in B & ( b in B & b c= a implies b = a ) )

proof end;

theorem :: NORMFORM:37

for A being set

for a being Element of DISJOINT_PAIRS A

for B being Element of Fin (DISJOINT_PAIRS A) st a in mi B holds

a in B by Th36;

for a being Element of DISJOINT_PAIRS A

for B being Element of Fin (DISJOINT_PAIRS A) st a in mi B holds

a in B by Th36;

theorem :: NORMFORM:38

theorem Th39: :: NORMFORM:39

for A being set

for a being Element of DISJOINT_PAIRS A

for B being Element of Fin (DISJOINT_PAIRS A) st a in B & ( for b being Element of DISJOINT_PAIRS A st b in B & b c= a holds

b = a ) holds

a in mi B

for a being Element of DISJOINT_PAIRS A

for B being Element of Fin (DISJOINT_PAIRS A) st a in B & ( for b being Element of DISJOINT_PAIRS A st b in B & b c= a holds

b = a ) holds

a in mi B

proof end;

Lm5: for A being set

for B, C being Element of Fin (DISJOINT_PAIRS A) st ( for a being Element of DISJOINT_PAIRS A st a in B holds

a in C ) holds

B c= C

proof end;

theorem Th41: :: NORMFORM:41

for A being set

for b being Element of DISJOINT_PAIRS A

for B being Element of Fin (DISJOINT_PAIRS A) st b in B holds

ex c being Element of DISJOINT_PAIRS A st

( c c= b & c in mi B )

for b being Element of DISJOINT_PAIRS A

for B being Element of Fin (DISJOINT_PAIRS A) st b in B holds

ex c being Element of DISJOINT_PAIRS A st

( c c= b & c in mi B )

proof end;

theorem Th44: :: NORMFORM:44

for A being set

for B, C being Element of Fin (DISJOINT_PAIRS A) holds mi ((mi B) \/ C) = mi (B \/ C)

for B, C being Element of Fin (DISJOINT_PAIRS A) holds mi ((mi B) \/ C) = mi (B \/ C)

proof end;

theorem :: NORMFORM:45

Lm6: for A being set

for a being Element of DISJOINT_PAIRS A

for B, C being Element of Fin (DISJOINT_PAIRS A) st a in B ^ C holds

ex b being Element of DISJOINT_PAIRS A st

( b c= a & b in (mi B) ^ C )

proof end;

theorem Th53: :: NORMFORM:53

for A being set

for K, L, M being Element of Normal_forms_on A holds K ^ (L \/ M) = (K ^ L) \/ (K ^ M)

for K, L, M being Element of Normal_forms_on A holds K ^ (L \/ M) = (K ^ L) \/ (K ^ M)

proof end;

Lm7: for A being set

for a being Element of DISJOINT_PAIRS A

for B, C being Element of Fin (DISJOINT_PAIRS A) st a in B ^ C holds

ex c being Element of DISJOINT_PAIRS A st

( c in C & c c= a )

proof end;

Lm8: for A being set

for K, L being Element of Normal_forms_on A holds mi ((K ^ L) \/ L) = mi L

proof end;

definition

let A be set ;

ex b_{1} being strict LattStr st

( the carrier of b_{1} = Normal_forms_on A & ( for B, C being Element of Normal_forms_on A holds

( the L_join of b_{1} . (B,C) = mi (B \/ C) & the L_meet of b_{1} . (B,C) = mi (B ^ C) ) ) )

for b_{1}, b_{2} being strict LattStr st the carrier of b_{1} = Normal_forms_on A & ( for B, C being Element of Normal_forms_on A holds

( the L_join of b_{1} . (B,C) = mi (B \/ C) & the L_meet of b_{1} . (B,C) = mi (B ^ C) ) ) & the carrier of b_{2} = Normal_forms_on A & ( for B, C being Element of Normal_forms_on A holds

( the L_join of b_{2} . (B,C) = mi (B \/ C) & the L_meet of b_{2} . (B,C) = mi (B ^ C) ) ) holds

b_{1} = b_{2}

end;
func NormForm A -> strict LattStr means :Def12: :: NORMFORM:def 12

( 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) ) ) );

existence ( 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) ) ) );

ex b

( the carrier of b

( the L_join of b

proof end;

uniqueness for b

( the L_join of b

( the L_join of b

b

proof end;

:: deftheorem Def12 defines NormForm NORMFORM:def 12 :

for A being set

for b_{2} being strict LattStr holds

( b_{2} = NormForm A iff ( the carrier of b_{2} = Normal_forms_on A & ( for B, C being Element of Normal_forms_on A holds

( the L_join of b_{2} . (B,C) = mi (B \/ C) & the L_meet of b_{2} . (B,C) = mi (B ^ C) ) ) ) );

for A being set

for b

( b

( the L_join of b

Lm9: for A being set

for a, b being Element of (NormForm A) holds a "\/" b = b "\/" a

proof end;

Lm10: for A being set

for a, b, c being Element of (NormForm A) holds a "\/" (b "\/" c) = (a "\/" b) "\/" c

proof end;

Lm11: for A being set

for K, L being Element of Normal_forms_on A holds the L_join of (NormForm A) . (( the L_meet of (NormForm A) . (K,L)),L) = L

proof end;

Lm12: for A being set

for a, b being Element of (NormForm A) holds (a "/\" b) "\/" b = b

proof end;

Lm13: for A being set

for a, b being Element of (NormForm A) holds a "/\" b = b "/\" a

proof end;

Lm14: for A being set

for a, b, c being Element of (NormForm A) holds a "/\" (b "/\" c) = (a "/\" b) "/\" c

proof end;

Lm15: for A being set

for K, L, M being Element of Normal_forms_on A holds the L_meet of (NormForm A) . (K,( the L_join of (NormForm A) . (L,M))) = the L_join of (NormForm A) . (( the L_meet of (NormForm A) . (K,L)),( the L_meet of (NormForm A) . (K,M)))

proof end;

Lm16: for A being set

for a, b being Element of (NormForm A) holds a "/\" (a "\/" b) = a

proof end;

registration
end;