:: NORMFORM semantic presentation

definition

let c₁, c₂ be non empty preBoolean set ;
let c₃, c₄ be Element of [:c₁,c₂:];
pred c₃ c= c₄ means :: NORMFORM:def 1
( a₃ `1 c= a₄ `1 & a₃ `2 c= a₄ `2 );
reflexivity ;
func c₃ \/ c₄ -> Element of [:a₁,a₂:] equals :: NORMFORM:def 2
[((a₃ `1 ) \/ (a₄ `1 )),((a₃ `2 ) \/ (a₄ `2 ))];
correctness ;
commutativity ;
idempotence by MCART_1:23;
func c₃ /\ c₄ -> Element of [:a₁,a₂:] equals :: NORMFORM:def 3
[((a₃ `1 ) /\ (a₄ `1 )),((a₃ `2 ) /\ (a₄ `2 ))];
correctness ;
commutativity ;
idempotence by MCART_1:23;
func c₃ \ c₄ -> Element of [:a₁,a₂:] equals :: NORMFORM:def 4
[((a₃ `1 ) \ (a₄ `1 )),((a₃ `2 ) \ (a₄ `2 ))];
correctness ;
func c₃ \+\ c₄ -> Element of [:a₁,a₂:] equals :: NORMFORM:def 5
[((a₃ `1 ) \+\ (a₄ `1 )),((a₃ `2 ) \+\ (a₄ `2 ))];
correctness ;
commutativity ;

end;

:: deftheorem Def1 defines c= NORMFORM:def 1 :

:: deftheorem Def2 defines \/ NORMFORM:def 2 :

:: deftheorem Def3 defines /\ NORMFORM:def 3 :

:: deftheorem Def4 defines \ NORMFORM:def 4 :

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

theorem Th1: :: NORMFORM:1

canceled;

theorem Th2: :: NORMFORM:2

canceled;

theorem Th3: :: NORMFORM:3

canceled;

theorem Th4: :: NORMFORM:4

for b₁, b₂ being non empty preBoolean set
for b₃, b₄ being Element of [:b₁,b₂:] st b₃ c= b₄ & b₄ c= b₃ holds
b₃ = b₄

proof end;

theorem Th5: :: NORMFORM:5

for b₁, b₂ being non empty preBoolean set
for b₃, b₄, b₅ being Element of [:b₁,b₂:] st b₃ c= b₄ & b₄ c= b₅ holds
b₃ c= b₅

proof end;

theorem Th6: :: NORMFORM:6

canceled;

theorem Th7: :: NORMFORM:7

canceled;

theorem Th8: :: NORMFORM:8

canceled;

theorem Th9: :: NORMFORM:9

canceled;

theorem Th10: :: NORMFORM:10

for b₁, b₂ being non empty preBoolean set
for b₃, b₄ being Element of [:b₁,b₂:] holds
( (b₃ \/ b₄) `1 = (b₃ `1 ) \/ (b₄ `1 ) & (b₃ \/ b₄) `2 = (b₃ `2 ) \/ (b₄ `2 ) ) by MCART_1:7;

theorem Th11: :: NORMFORM:11

for b₁, b₂ being non empty preBoolean set
for b₃, b₄ being Element of [:b₁,b₂:] holds
( (b₃ /\ b₄) `1 = (b₃ `1 ) /\ (b₄ `1 ) & (b₃ /\ b₄) `2 = (b₃ `2 ) /\ (b₄ `2 ) ) by MCART_1:7;

theorem Th12: :: NORMFORM:12

for b₁, b₂ being non empty preBoolean set
for b₃, b₄ being Element of [:b₁,b₂:] holds
( (b₃ \ b₄) `1 = (b₃ `1 ) \ (b₄ `1 ) & (b₃ \ b₄) `2 = (b₃ `2 ) \ (b₄ `2 ) ) by MCART_1:7;

theorem Th13: :: NORMFORM:13

for b₁, b₂ being non empty preBoolean set
for b₃, b₄ being Element of [:b₁,b₂:] holds
( (b₃ \+\ b₄) `1 = (b₃ `1 ) \+\ (b₄ `1 ) & (b₃ \+\ b₄) `2 = (b₃ `2 ) \+\ (b₄ `2 ) ) by MCART_1:7;

theorem Th14: :: NORMFORM:14

canceled;

theorem Th15: :: NORMFORM:15

canceled;

theorem Th16: :: NORMFORM:16

for b₁, b₂ being non empty preBoolean set
for b₃, b₄, b₅ being Element of [:b₁,b₂:] holds (b₃ \/ b₄) \/ b₅ = b₃ \/ (b₄ \/ b₅)

proof end;

theorem Th17: :: NORMFORM:17

canceled;

theorem Th18: :: NORMFORM:18

canceled;

theorem Th19: :: NORMFORM:19

for b₁, b₂ being non empty preBoolean set
for b₃, b₄, b₅ being Element of [:b₁,b₂:] holds (b₃ /\ b₄) /\ b₅ = b₃ /\ (b₄ /\ b₅)

proof end;

theorem Th20: :: NORMFORM:20

for b₁, b₂ being non empty preBoolean set
for b₃, b₄, b₅ being Element of [:b₁,b₂:] holds b₃ /\ (b₄ \/ b₅) = (b₃ /\ b₄) \/ (b₃ /\ b₅)

proof end;

theorem Th21: :: NORMFORM:21

for b₁, b₂ being non empty preBoolean set
for b₃, b₄ being Element of [:b₁,b₂:] holds b₃ \/ (b₄ /\ b₃) = b₃

proof end;

theorem Th22: :: NORMFORM:22

for b₁, b₂ being non empty preBoolean set
for b₃, b₄ being Element of [:b₁,b₂:] holds b₃ /\ (b₄ \/ b₃) = b₃

proof end;

theorem Th23: :: NORMFORM:23

canceled;

theorem Th24: :: NORMFORM:24

for b₁, b₂ being non empty preBoolean set
for b₃, b₄, b₅ being Element of [:b₁,b₂:] holds b₃ \/ (b₄ /\ b₅) = (b₃ \/ b₄) /\ (b₃ \/ b₅)

proof end;

theorem Th25: :: NORMFORM:25

for b₁, b₂ being non empty preBoolean set
for b₃, b₄, b₅ being Element of [:b₁,b₂:] st b₃ c= b₄ & b₅ c= b₄ holds
b₃ \/ b₅ c= b₄

proof end;

theorem Th26: :: NORMFORM:26

for b₁, b₂ being non empty preBoolean set
for b₃, b₄ being Element of [:b₁,b₂:] holds
( b₃ c= b₃ \/ b₄ & b₄ c= b₃ \/ b₄ )

proof end;

theorem Th27: :: NORMFORM:27

for b₁, b₂ being non empty preBoolean set
for b₃, b₄ being Element of [:b₁,b₂:] st b₃ = b₃ \/ b₄ holds
b₄ c= b₃ by Th26;

theorem Th28: :: NORMFORM:28

for b₁, b₂ being non empty preBoolean set
for b₃, b₄, b₅ being Element of [:b₁,b₂:] st b₃ c= b₄ holds
( b₅ \/ b₃ c= b₅ \/ b₄ & b₃ \/ b₅ c= b₄ \/ b₅ )

proof end;

theorem Th29: :: NORMFORM:29

for b₁, b₂ being non empty preBoolean set
for b₃, b₄ being Element of [:b₁,b₂:] holds (b₃ \ b₄) \/ b₄ = b₃ \/ b₄

proof end;

theorem Th30: :: NORMFORM:30

for b₁, b₂ being non empty preBoolean set
for b₃, b₄, b₅ being Element of [:b₁,b₂:] st b₃ \ b₄ c= b₅ holds
b₃ c= b₄ \/ b₅

proof end;

theorem Th31: :: NORMFORM:31

for b₁, b₂ being non empty preBoolean set
for b₃, b₄, b₅ being Element of [:b₁,b₂:] st b₃ c= b₄ \/ b₅ holds
b₃ \ b₅ c= b₄

proof end;

definition

let c₁ be set ;
func FinPairUnion c₁ -> BinOp of [:(Fin a₁),(Fin a₁):] means :Def6: :: NORMFORM:def 6
for b₁, b₂ being Element of [:(Fin a₁),(Fin a₁):] holds a₂ . b₁,b₂ = b₁ \/ b₂;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def6 defines FinPairUnion NORMFORM:def 6 :

definition

let c₁ be non empty set ;
let c₂ be set ;
let c₃ be Element of Fin c₁;
let c₄ be Function of c₁,[:(Fin c₂),(Fin c₂):];
func FinPairUnion c₃,c₄ -> Element of [:(Fin a₂),(Fin a₂):] equals :: NORMFORM:def 7
(FinPairUnion a₂) $$ a₃,a₄;
correctness ;

end;

:: deftheorem Def7 defines FinPairUnion NORMFORM:def 7 :

Lemma14: for b₁ being set holds FinPairUnion b₁ is idempotent

proof end;

Lemma15: for b₁ being set holds FinPairUnion b₁ is commutative

proof end;

Lemma16: for b₁ being set holds FinPairUnion b₁ is associative

proof end;

registration

let c₁ be set ;
cluster FinPairUnion a₁ -> commutative associative idempotent ;
coherence by Lemma14, Lemma15, Lemma16;

end;

theorem Th32: :: NORMFORM:32

canceled;

theorem Th33: :: NORMFORM:33

canceled;

theorem Th34: :: NORMFORM:34

canceled;

theorem Th35: :: NORMFORM:35

for b₁ being set
for b₂ being non empty set
for b₃ being Function of b₂,[:(Fin b₁),(Fin b₁):]
for b₄ being Element of Fin b₂
for b₅ being Element of b₂ st b₅ in b₄ holds
b₃ . b₅ c= FinPairUnion b₄,b₃

proof end;

theorem Th36: :: NORMFORM:36

for b₁ being set holds [({}. b₁),({}. b₁)] is_a_unity_wrt FinPairUnion b₁

proof end;

theorem Th37: :: NORMFORM:37

for b₁ being set holds FinPairUnion b₁ has_a_unity

proof end;

theorem Th38: :: NORMFORM:38

for b₁ being set holds the_unity_wrt (FinPairUnion b₁) = [({}. b₁),({}. b₁)]

proof end;

theorem Th39: :: NORMFORM:39

for b₁ being set
for b₂ being Element of [:(Fin b₁),(Fin b₁):] holds the_unity_wrt (FinPairUnion b₁) c= b₂

proof end;

theorem Th40: :: NORMFORM:40

for b₁ being set
for b₂ being non empty set
for b₃ being Function of b₂,[:(Fin b₁),(Fin b₁):]
for b₄ being Element of Fin b₂
for b₅ being Element of [:(Fin b₁),(Fin b₁):] st ( for b₆ being Element of b₂ st b₆ in b₄ holds
b₃ . b₆ c= b₅ ) holds
FinPairUnion b₄,b₃ c= b₅

proof end;

theorem Th41: :: NORMFORM:41

for b₁ being set
for b₂ being non empty set
for b₃ being Element of Fin b₂
for b₄, b₅ being Function of b₂,[:(Fin b₁),(Fin b₁):] st b₄ | b₃ = b₅ | b₃ holds
FinPairUnion b₃,b₄ = FinPairUnion b₃,b₅

proof end;

definition

let c₁ be set ;
func DISJOINT_PAIRS c₁ -> Subset of [:(Fin a₁),(Fin a₁):] equals :: NORMFORM:def 8
{ b₁ where B is Element of [:(Fin a₁),(Fin a₁):] : b₁ `1 misses b₁ `2 } ;
coherence

proof end;

end;

:: deftheorem Def8 defines DISJOINT_PAIRS NORMFORM:def 8 :

registration

let c₁ be set ;
cluster DISJOINT_PAIRS a₁ -> non empty ;
coherence

proof end;

end;

theorem Th42: :: NORMFORM:42

for b₁ being set
for b₂ being Element of [:(Fin b₁),(Fin b₁):] holds
( b₂ in DISJOINT_PAIRS b₁ iff b₂ `1 misses b₂ `2 )

proof end;

theorem Th43: :: NORMFORM:43

for b₁ being set
for b₂, b₃ being Element of [:(Fin b₁),(Fin b₁):] st b₂ in DISJOINT_PAIRS b₁ & b₃ in DISJOINT_PAIRS b₁ holds
( b₂ \/ b₃ in DISJOINT_PAIRS b₁ iff ((b₂ `1 ) /\ (b₃ `2 )) \/ ((b₃ `1 ) /\ (b₂ `2 )) = {} )

proof end;

theorem Th44: :: NORMFORM:44

for b₁ being set
for b₂ being Element of DISJOINT_PAIRS b₁ holds b₂ `1 misses b₂ `2 by Th42;

theorem Th45: :: NORMFORM:45

for b₁ being set
for b₂ being Element of [:(Fin b₁),(Fin b₁):]
for b₃ being Element of DISJOINT_PAIRS b₁ st b₂ c= b₃ holds
b₂ is Element of DISJOINT_PAIRS b₁

proof end;

theorem Th46: :: NORMFORM:46

for b₁ being set
for b₂ being Element of DISJOINT_PAIRS b₁
for b₃ being set holds
( not b₃ in b₂ `1 or not b₃ in b₂ `2 )

proof end;

theorem Th47: :: NORMFORM:47

for b₁ being set
for b₂, b₃ being Element of DISJOINT_PAIRS b₁ st not b₂ \/ b₃ in DISJOINT_PAIRS b₁ holds
ex b₄ being Element of b₁ st
( ( b₄ in b₂ `1 & b₄ in b₃ `2 ) or ( b₄ in b₃ `1 & b₄ in b₂ `2 ) )

proof end;

theorem Th48: :: NORMFORM:48

canceled;

theorem Th49: :: NORMFORM:49

for b₁ being set
for b₂ being Element of [:(Fin b₁),(Fin b₁):] st b₂ `1 misses b₂ `2 holds
b₂ is Element of DISJOINT_PAIRS b₁ by Th42;

theorem Th50: :: NORMFORM:50

for b₁ being set
for b₂ being Element of DISJOINT_PAIRS b₁
for b₃, b₄ being set st b₃ c= b₂ `1 & b₄ c= b₂ `2 holds
[b₃,b₄] is Element of DISJOINT_PAIRS b₁

proof end;

Lemma24: for b₁ being set holds {} in { b₂ where B is Element of Fin (DISJOINT_PAIRS b₁) : for b₁, b₂ being Element of DISJOINT_PAIRS b₁ st b₃ in b₂ & b₄ in b₂ & b₃ c= b₄ holds
b₃ = b₄ }

proof end;

definition

let c₁ be set ;
func Normal_forms_on c₁ -> Subset of (Fin (DISJOINT_PAIRS a₁)) equals :: NORMFORM:def 9
{ b₁ where B is Element of Fin (DISJOINT_PAIRS a₁) : for b₁, b₂ being Element of DISJOINT_PAIRS a₁ st b₂ in b₁ & b₃ in b₁ & b₂ c= b₃ holds
b₂ = b₃ } ;
coherence

proof end;

end;

:: deftheorem Def9 defines Normal_forms_on NORMFORM:def 9 :

registration

let c₁ be set ;
cluster Normal_forms_on a₁ -> non empty ;
coherence by Lemma24;

end;

theorem Th51: :: NORMFORM:51

for b₁ being set holds {} in Normal_forms_on b₁ by Lemma24;

theorem Th52: :: NORMFORM:52

for b₁ being set
for b₂, b₃ being Element of DISJOINT_PAIRS b₁
for b₄ being Element of Fin (DISJOINT_PAIRS b₁) st b₄ in Normal_forms_on b₁ & b₂ in b₄ & b₃ in b₄ & b₂ c= b₃ holds
b₂ = b₃

proof end;

theorem Th53: :: NORMFORM:53

for b₁ being set
for b₂ being Element of Fin (DISJOINT_PAIRS b₁) st ( for b₃, b₄ being Element of DISJOINT_PAIRS b₁ st b₃ in b₂ & b₄ in b₂ & b₃ c= b₄ holds
b₃ = b₄ ) holds
b₂ in Normal_forms_on b₁ ;

definition

let c₁ be set ;
let c₂ be Element of Fin (DISJOINT_PAIRS c₁);
func mi c₂ -> Element of Normal_forms_on a₁ equals :: NORMFORM:def 10
{ b₁ where B is Element of DISJOINT_PAIRS a₁ : for b₁ being Element of DISJOINT_PAIRS a₁ holds
( ( b₂ in a₂ & b₂ c= b₁ ) iff b₂ = b₁ ) } ;
coherence

proof end;

correctness ;
let c₃ be Element of Fin (DISJOINT_PAIRS c₁);
func c₂ ^ c₃ -> Element of Fin (DISJOINT_PAIRS a₁) equals :: NORMFORM:def 11
(DISJOINT_PAIRS a₁) /\ { (b₁ \/ b₂) where B is Element of DISJOINT_PAIRS a₁, B is Element of DISJOINT_PAIRS a₁ : ( b₁ in a₂ & b₂ in a₃ ) } ;
coherence

proof end;

correctness ;

end;

:: deftheorem Def10 defines mi NORMFORM:def 10 :

:: deftheorem Def11 defines ^ NORMFORM:def 11 :

theorem Th54: :: NORMFORM:54

canceled;

theorem Th55: :: NORMFORM:55

for b₁ being set
for b₂ being Element of [:(Fin b₁),(Fin b₁):]
for b₃, b₄ being Element of Fin (DISJOINT_PAIRS b₁) st b₂ in b₃ ^ b₄ holds
ex b₅, b₆ being Element of DISJOINT_PAIRS b₁ st
( b₅ in b₃ & b₆ in b₄ & b₂ = b₅ \/ b₆ )

proof end;

theorem Th56: :: NORMFORM:56

for b₁ being set
for b₂, b₃ being Element of DISJOINT_PAIRS b₁
for b₄, b₅ being Element of Fin (DISJOINT_PAIRS b₁) st b₂ in b₄ & b₃ in b₅ & b₂ \/ b₃ in DISJOINT_PAIRS b₁ holds
b₂ \/ b₃ in b₄ ^ b₅

proof end;

theorem Th57: :: NORMFORM:57

canceled;

theorem Th58: :: NORMFORM:58

for b₁ being set
for b₂, b₃ being Element of DISJOINT_PAIRS b₁
for b₄ being Element of Fin (DISJOINT_PAIRS b₁) st b₂ in mi b₄ holds
( b₂ in b₄ & ( b₃ in b₄ & b₃ c= b₂ implies b₃ = b₂ ) )

proof end;

theorem Th59: :: NORMFORM:59

for b₁ being set
for b₂ being Element of DISJOINT_PAIRS b₁
for b₃ being Element of Fin (DISJOINT_PAIRS b₁) st b₂ in mi b₃ holds
b₂ in b₃ by Th58;

theorem Th60: :: NORMFORM:60

for b₁ being set
for b₂, b₃ being Element of DISJOINT_PAIRS b₁
for b₄ being Element of Fin (DISJOINT_PAIRS b₁) st b₂ in mi b₄ & b₃ in b₄ & b₃ c= b₂ holds
b₃ = b₂ by Th58;

theorem Th61: :: NORMFORM:61

for b₁ being set
for b₂ being Element of DISJOINT_PAIRS b₁
for b₃ being Element of Fin (DISJOINT_PAIRS b₁) st b₂ in b₃ & ( for b₄ being Element of DISJOINT_PAIRS b₁ st b₄ in b₃ & b₄ c= b₂ holds
b₄ = b₂ ) holds
b₂ in mi b₃

proof end;

definition

let c₁ be non empty set ;
let c₂ be non empty Subset of c₁;
let c₃ be BinOp of c₂;
let c₄, c₅ be Element of c₂;
redefine func . as c₃ . c₄,c₅ -> Element of a₂;
coherence

proof end;

end;

Lemma32: for b₁ being set
for b₂, b₃ being Element of Fin (DISJOINT_PAIRS b₁) st ( for b₄ being Element of DISJOINT_PAIRS b₁ st b₄ in b₂ holds
b₄ in b₃ ) holds
b₂ c= b₃

proof end;

theorem Th62: :: NORMFORM:62

canceled;

theorem Th63: :: NORMFORM:63

canceled;

theorem Th64: :: NORMFORM:64

for b₁ being set
for b₂ being Element of Fin (DISJOINT_PAIRS b₁) holds mi b₂ c= b₂

proof end;

theorem Th65: :: NORMFORM:65

for b₁ being set
for b₂ being Element of DISJOINT_PAIRS b₁
for b₃ being Element of Fin (DISJOINT_PAIRS b₁) st b₂ in b₃ holds
ex b₄ being Element of DISJOINT_PAIRS b₁ st
( b₄ c= b₂ & b₄ in mi b₃ )

proof end;

theorem Th66: :: NORMFORM:66

for b₁ being set
for b₂ being Element of Normal_forms_on b₁ holds mi b₂ = b₂

proof end;

theorem Th67: :: NORMFORM:67

for b₁ being set
for b₂, b₃ being Element of Fin (DISJOINT_PAIRS b₁) holds mi (b₂ \/ b₃) c= (mi b₂) \/ b₃

proof end;

theorem Th68: :: NORMFORM:68

for b₁ being set
for b₂, b₃ being Element of Fin (DISJOINT_PAIRS b₁) holds mi ((mi b₂) \/ b₃) = mi (b₂ \/ b₃)

proof end;

theorem Th69: :: NORMFORM:69

for b₁ being set
for b₂, b₃ being Element of Fin (DISJOINT_PAIRS b₁) holds mi (b₂ \/ (mi b₃)) = mi (b₂ \/ b₃) by Th68;

theorem Th70: :: NORMFORM:70

for b₁ being set
for b₂, b₃, b₄ being Element of Fin (DISJOINT_PAIRS b₁) st b₂ c= b₃ holds
b₂ ^ b₄ c= b₃ ^ b₄

proof end;

Lemma39: for b₁ being set
for b₂ being Element of DISJOINT_PAIRS b₁
for b₃, b₄ being Element of Fin (DISJOINT_PAIRS b₁) st b₂ in b₃ ^ b₄ holds
ex b₅ being Element of DISJOINT_PAIRS b₁ st
( b₅ c= b₂ & b₅ in (mi b₃) ^ b₄ )

proof end;

theorem Th71: :: NORMFORM:71

for b₁ being set
for b₂, b₃ being Element of Fin (DISJOINT_PAIRS b₁) holds mi (b₂ ^ b₃) c= (mi b₂) ^ b₃

proof end;

theorem Th72: :: NORMFORM:72

for b₁ being set
for b₂, b₃ being Element of Fin (DISJOINT_PAIRS b₁) holds b₂ ^ b₃ = b₃ ^ b₂

proof end;

theorem Th73: :: NORMFORM:73

for b₁ being set
for b₂, b₃, b₄ being Element of Fin (DISJOINT_PAIRS b₁) st b₂ c= b₃ holds
b₄ ^ b₂ c= b₄ ^ b₃

proof end;

theorem Th74: :: NORMFORM:74

for b₁ being set
for b₂, b₃ being Element of Fin (DISJOINT_PAIRS b₁) holds mi ((mi b₂) ^ b₃) = mi (b₂ ^ b₃)

proof end;

theorem Th75: :: NORMFORM:75

for b₁ being set
for b₂, b₃ being Element of Fin (DISJOINT_PAIRS b₁) holds mi (b₂ ^ (mi b₃)) = mi (b₂ ^ b₃)

proof end;

theorem Th76: :: NORMFORM:76

for b₁ being set
for b₂, b₃, b₄ being Element of Normal_forms_on b₁ holds b₂ ^ (b₃ ^ b₄) = (b₂ ^ b₃) ^ b₄

proof end;

theorem Th77: :: NORMFORM:77

for b₁ being set
for b₂, b₃, b₄ being Element of Normal_forms_on b₁ holds b₂ ^ (b₃ \/ b₄) = (b₂ ^ b₃) \/ (b₂ ^ b₄)

proof end;

Lemma47: for b₁ being set
for b₂ being Element of DISJOINT_PAIRS b₁
for b₃, b₄ being Element of Fin (DISJOINT_PAIRS b₁) st b₂ in b₃ ^ b₄ holds
ex b₅ being Element of DISJOINT_PAIRS b₁ st
( b₅ in b₄ & b₅ c= b₂ )

proof end;

Lemma48: for b₁ being set
for b₂, b₃ being Element of Normal_forms_on b₁ holds mi ((b₂ ^ b₃) \/ b₃) = mi b₃

proof end;

theorem Th78: :: NORMFORM:78

for b₁ being set
for b₂ being Element of Fin (DISJOINT_PAIRS b₁) holds b₂ c= b₂ ^ b₂

proof end;

theorem Th79: :: NORMFORM:79

for b₁ being set
for b₂ being Element of Normal_forms_on b₁ holds mi (b₂ ^ b₂) = mi b₂

proof end;

definition

let c₁ be set ;
canceled;
canceled;
func NormForm c₁ -> strict LattStr means :Def14: :: NORMFORM:def 14
( the carrier of a₂ = Normal_forms_on a₁ & ( for b₁, b₂ being Element of Normal_forms_on a₁ holds
( the L_join of a₂ . b₁,b₂ = mi (b₁ \/ b₂) & the L_meet of a₂ . b₁,b₂ = mi (b₁ ^ b₂) ) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def12 NORMFORM:def 12 :

:: deftheorem Def13 NORMFORM:def 13 :

:: deftheorem Def14 defines NormForm NORMFORM:def 14 :

registration

let c₁ be set ;
cluster NormForm a₁ -> non empty strict ;
coherence

proof end;

end;

Lemma52: for b₁ being set
for b₂, b₃ being Element of (NormForm b₁) holds b₂ "\/" b₃ = b₃ "\/" b₂

proof end;

Lemma53: for b₁ being set
for b₂, b₃, b₄ being Element of (NormForm b₁) holds b₂ "\/" (b₃ "\/" b₄) = (b₂ "\/" b₃) "\/" b₄

proof end;

Lemma54: for b₁ being set
for b₂, b₃ being Element of Normal_forms_on b₁ holds the L_join of (NormForm b₁) . (the L_meet of (NormForm b₁) . b₂,b₃),b₃ = b₃

proof end;

Lemma55: for b₁ being set
for b₂, b₃ being Element of (NormForm b₁) holds (b₂ "/\" b₃) "\/" b₃ = b₃

proof end;

Lemma56: for b₁ being set
for b₂, b₃ being Element of (NormForm b₁) holds b₂ "/\" b₃ = b₃ "/\" b₂

proof end;

Lemma57: for b₁ being set
for b₂, b₃, b₄ being Element of (NormForm b₁) holds b₂ "/\" (b₃ "/\" b₄) = (b₂ "/\" b₃) "/\" b₄

proof end;

Lemma58: for b₁ being set
for b₂, b₃, b₄ being Element of Normal_forms_on b₁ holds the L_meet of (NormForm b₁) . b₂,(the L_join of (NormForm b₁) . b₃,b₄) = the L_join of (NormForm b₁) . (the L_meet of (NormForm b₁) . b₂,b₃),(the L_meet of (NormForm b₁) . b₂,b₄)

proof end;

Lemma59: for b₁ being set
for b₂, b₃ being Element of (NormForm b₁) holds b₂ "/\" (b₂ "\/" b₃) = b₂

proof end;

registration

let c₁ be set ;
cluster NormForm a₁ -> non empty strict Lattice-like ;
coherence

proof end;

end;

registration

let c₁ be set ;
cluster NormForm a₁ -> non empty strict Lattice-like distributive lower-bounded ;
coherence

proof end;

end;

theorem Th80: :: NORMFORM:80

canceled;

theorem Th81: :: NORMFORM:81

canceled;

theorem Th82: :: NORMFORM:82

canceled;

theorem Th83: :: NORMFORM:83

canceled;

theorem Th84: :: NORMFORM:84

canceled;

theorem Th85: :: NORMFORM:85

for b₁ being set holds {} is Element of (NormForm b₁)

proof end;

theorem Th86: :: NORMFORM:86

for b₁ being set holds Bottom (NormForm b₁) = {}

proof end;