:: FUZZY_2 semantic presentation

theorem Th1: :: FUZZY_2:1

for b₁ being non empty set
for b₂ being Element of b₁
for b₃ being Membership_Func of b₁ holds
( 0 <= b₃ . b₂ & b₃ . b₂ <= 1 )

proof end;

theorem Th2: :: FUZZY_2:2

for b₁ being non empty set
for b₂, b₃, b₄ being Membership_Func of b₁ st b₃ c= holds
max b₂,(min b₄,b₃) = min (max b₂,b₄),b₃

proof end;

definition

let c₁ be non empty set ;
let c₂, c₃ be Membership_Func of c₁;
func c₂ \ c₃ -> Membership_Func of a₁ equals :: FUZZY_2:def 1
min a₂,(1_minus a₃);
correctness ;

end;

:: deftheorem Def1 defines \ FUZZY_2:def 1 :

theorem Th3: :: FUZZY_2:3

for b₁ being non empty set
for b₂, b₃ being Membership_Func of b₁ holds 1_minus (b₂ \ b₃) = max (1_minus b₂),b₃

proof end;

theorem Th4: :: FUZZY_2:4

for b₁ being non empty set
for b₂, b₃, b₄ being Membership_Func of b₁ st b₃ c= holds
b₃ \ b₄ c=

proof end;

theorem Th5: :: FUZZY_2:5

for b₁ being non empty set
for b₂, b₃, b₄ being Membership_Func of b₁ st b₃ c= holds
b₄ \ b₂ c=

proof end;

theorem Th6: :: FUZZY_2:6

for b₁ being non empty set
for b₂, b₃, b₄, b₅ being Membership_Func of b₁ st b₃ c= & b₅ c= holds
b₃ \ b₄ c=

proof end;

theorem Th7: :: FUZZY_2:7

for b₁ being non empty set
for b₂, b₃ being Membership_Func of b₁ holds b₂ c= by FUZZY_1:18;

theorem Th8: :: FUZZY_2:8

for b₁ being non empty set
for b₂, b₃ being Membership_Func of b₁ holds b₂ \+\ b₃ c= by FUZZY_1:18;

theorem Th9: :: FUZZY_2:9

for b₁ being non empty set
for b₂ being Membership_Func of b₁ holds b₂ \ (EMF b₁) = b₂

proof end;

theorem Th10: :: FUZZY_2:10

for b₁ being non empty set
for b₂ being Membership_Func of b₁ holds (EMF b₁) \ b₂ = EMF b₁ by FUZZY_1:19;

theorem Th11: :: FUZZY_2:11

for b₁ being non empty set
for b₂, b₃ being Membership_Func of b₁ holds b₂ \ (min b₂,b₃) c=

proof end;

theorem Th12: :: FUZZY_2:12

for b₁ being non empty set
for b₂, b₃ being Membership_Func of b₁ holds b₂ c=

proof end;

theorem Th13: :: FUZZY_2:13

for b₁ being non empty set
for b₂, b₃ being Membership_Func of b₁ holds max b₂,b₃ c=

proof end;

theorem Th14: :: FUZZY_2:14

for b₁ being non empty set
for b₂, b₃, b₄ being Membership_Func of b₁ holds b₂ \ (b₃ \ b₄) = max (b₂ \ b₃),(min b₂,b₄)

proof end;

theorem Th15: :: FUZZY_2:15

for b₁ being non empty set
for b₂, b₃ being Membership_Func of b₁ holds b₂ \ (b₂ \ b₃) c=

proof end;

theorem Th16: :: FUZZY_2:16

for b₁ being non empty set
for b₂, b₃ being Membership_Func of b₁ holds (max b₂,b₃) \ b₃ c=

proof end;

theorem Th17: :: FUZZY_2:17

for b₁ being non empty set
for b₂, b₃, b₄ being Membership_Func of b₁ holds b₂ \ (max b₃,b₄) = min (b₂ \ b₃),(b₂ \ b₄)

proof end;

theorem Th18: :: FUZZY_2:18

for b₁ being non empty set
for b₂, b₃, b₄ being Membership_Func of b₁ holds b₂ \ (min b₃,b₄) = max (b₂ \ b₃),(b₂ \ b₄)

proof end;

theorem Th19: :: FUZZY_2:19

for b₁ being non empty set
for b₂, b₃, b₄ being Membership_Func of b₁ holds (b₂ \ b₃) \ b₄ = b₂ \ (max b₃,b₄)

proof end;

theorem Th20: :: FUZZY_2:20

for b₁ being non empty set
for b₂, b₃ being Membership_Func of b₁ holds (max b₂,b₃) \ (min b₂,b₃) c=

proof end;

theorem Th21: :: FUZZY_2:21

for b₁ being non empty set
for b₂, b₃, b₄ being Membership_Func of b₁ holds (max b₂,b₃) \ b₄ = max (b₂ \ b₄),(b₃ \ b₄) by FUZZY_1:10;

theorem Th22: :: FUZZY_2:22

for b₁ being non empty set
for b₂, b₃, b₄ being Membership_Func of b₁ st b₄ c= & b₄ c= holds
b₄ c=

proof end;

theorem Th23: :: FUZZY_2:23

for b₁ being non empty set
for b₂, b₃, b₄ being Membership_Func of b₁ holds min b₂,(b₃ \ b₄) = (min b₂,b₃) \ b₄ by FUZZY_1:8;

theorem Th24: :: FUZZY_2:24

for b₁ being non empty set
for b₂, b₃, b₄ being Membership_Func of b₁ holds (min b₂,b₃) \ (min b₂,b₄) c=

proof end;

theorem Th25: :: FUZZY_2:25

for b₁ being non empty set
for b₂, b₃ being Membership_Func of b₁ holds (max b₂,b₃) \ (min b₂,b₃) c=

proof end;

theorem Th26: :: FUZZY_2:26

for b₁ being non empty set
for b₂, b₃ being Membership_Func of b₁ holds 1_minus (b₂ \+\ b₃) c=

proof end;

theorem Th27: :: FUZZY_2:27

for b₁ being non empty set
for b₂, b₃, b₄ being Membership_Func of b₁ holds (b₂ \+\ b₃) \ b₄ = max (b₂ \ (max b₃,b₄)),(b₃ \ (max b₂,b₄))

proof end;

theorem Th28: :: FUZZY_2:28

for b₁ being non empty set
for b₂, b₃, b₄ being Membership_Func of b₁ holds b₂ \ (b₃ \+\ b₄) c=

proof end;

theorem Th29: :: FUZZY_2:29

for b₁ being non empty set
for b₂, b₃ being Membership_Func of b₁ st b₃ c= holds
b₃ c=

proof end;

theorem Th30: :: FUZZY_2:30

for b₁ being non empty set
for b₂, b₃ being Membership_Func of b₁ holds max b₂,b₃ c=

proof end;

theorem Th31: :: FUZZY_2:31

for b₁ being non empty set
for b₂, b₃ being Membership_Func of b₁ st b₂ \ b₃ = EMF b₁ holds
b₃ c=

proof end;

theorem Th32: :: FUZZY_2:32

for b₁ being non empty set
for b₂, b₃ being Membership_Func of b₁ st min b₂,b₃ = EMF b₁ holds
b₂ \ b₃ = b₂

proof end;

definition

let c₁ be non empty set ;
let c₂, c₃ be Membership_Func of c₁;
func c₂ * c₃ -> Membership_Func of a₁ means :Def2: :: FUZZY_2:def 2
for b₁ being Element of a₁ holds a₄ . b₁ = (a₂ . b₁) * (a₃ . b₁);
existence

proof end;

uniqueness

proof end;

commutativity ;

end;

:: deftheorem Def2 defines * FUZZY_2:def 2 :

definition

let c₁ be non empty set ;
let c₂, c₃ be Membership_Func of c₁;
func c₂ ++ c₃ -> Membership_Func of a₁ means :Def3: :: FUZZY_2:def 3
for b₁ being Element of a₁ holds a₄ . b₁ = ((a₂ . b₁) + (a₃ . b₁)) - ((a₂ . b₁) * (a₃ . b₁));
existence

proof end;

uniqueness

proof end;

commutativity ;

end;

:: deftheorem Def3 defines ++ FUZZY_2:def 3 :

theorem Th33: :: FUZZY_2:33

for b₁ being non empty set
for b₂ being Membership_Func of b₁ holds
( b₂ c= & b₂ ++ b₂ c= )

proof end;

theorem Th34: :: FUZZY_2:34

for b₁ being non empty set
for b₂, b₃, b₄ being Membership_Func of b₁ holds (b₂ * b₃) * b₄ = b₂ * (b₃ * b₄)

proof end;

theorem Th35: :: FUZZY_2:35

for b₁ being non empty set
for b₂, b₃, b₄ being Membership_Func of b₁ holds (b₂ ++ b₃) ++ b₄ = b₂ ++ (b₃ ++ b₄)

proof end;

theorem Th36: :: FUZZY_2:36

for b₁ being non empty set
for b₂, b₃ being Membership_Func of b₁ holds
( b₂ c= & b₂ ++ (b₂ * b₃) c= )

proof end;

theorem Th37: :: FUZZY_2:37

for b₁ being non empty set
for b₂, b₃, b₄ being Membership_Func of b₁ holds (b₂ * b₃) ++ (b₂ * b₄) c=

proof end;

theorem Th38: :: FUZZY_2:38

for b₁ being non empty set
for b₂, b₃, b₄ being Membership_Func of b₁ holds b₂ ++ (b₃ * b₄) c=

proof end;

theorem Th39: :: FUZZY_2:39

for b₁ being non empty set
for b₂, b₃ being Membership_Func of b₁ holds 1_minus (b₂ * b₃) = (1_minus b₂) ++ (1_minus b₃)

proof end;

theorem Th40: :: FUZZY_2:40

for b₁ being non empty set
for b₂, b₃ being Membership_Func of b₁ holds 1_minus (b₂ ++ b₃) = (1_minus b₂) * (1_minus b₃)

proof end;

theorem Th41: :: FUZZY_2:41

for b₁ being non empty set
for b₂, b₃ being Membership_Func of b₁ holds b₂ ++ b₃ = 1_minus ((1_minus b₂) * (1_minus b₃))

proof end;

theorem Th42: :: FUZZY_2:42

for b₁ being non empty set
for b₂ being Membership_Func of b₁ holds
( b₂ * (EMF b₁) = EMF b₁ & b₂ * (UMF b₁) = b₂ )

proof end;

theorem Th43: :: FUZZY_2:43

for b₁ being non empty set
for b₂ being Membership_Func of b₁ holds
( b₂ ++ (EMF b₁) = b₂ & b₂ ++ (UMF b₁) = UMF b₁ )

proof end;

theorem Th44: :: FUZZY_2:44

for b₁ being non empty set
for b₂, b₃ being Membership_Func of b₁ holds min b₂,b₃ c=

proof end;

theorem Th45: :: FUZZY_2:45

for b₁ being non empty set
for b₂, b₃ being Membership_Func of b₁ holds b₂ ++ b₃ c=

proof end;

Lemma10: for b₁, b₂, b₃ being Real st 0 <= b₃ holds
b₃ * (min b₁,b₂) = min (b₃ * b₁),(b₃ * b₂)

proof end;

Lemma11: for b₁, b₂, b₃ being Real st 0 <= b₃ holds
b₃ * (max b₁,b₂) = max (b₃ * b₁),(b₃ * b₂)

proof end;

theorem Th46: :: FUZZY_2:46

for b₁, b₂, b₃ being Real st 0 <= b₃ holds
( b₃ * (max b₁,b₂) = max (b₃ * b₁),(b₃ * b₂) & b₃ * (min b₁,b₂) = min (b₃ * b₁),(b₃ * b₂) ) by Lemma10, Lemma11;

theorem Th47: :: FUZZY_2:47

for b₁, b₂, b₃ being Real holds
( b₃ + (max b₁,b₂) = max (b₃ + b₁),(b₃ + b₂) & b₃ + (min b₁,b₂) = min (b₃ + b₁),(b₃ + b₂) )

proof end;

theorem Th48: :: FUZZY_2:48

for b₁ being non empty set
for b₂, b₃, b₄ being Membership_Func of b₁ holds b₂ * (max b₃,b₄) = max (b₂ * b₃),(b₂ * b₄)

proof end;

theorem Th49: :: FUZZY_2:49

for b₁ being non empty set
for b₂, b₃, b₄ being Membership_Func of b₁ holds b₂ * (min b₃,b₄) = min (b₂ * b₃),(b₂ * b₄)

proof end;

theorem Th50: :: FUZZY_2:50

for b₁ being non empty set
for b₂, b₃, b₄ being Membership_Func of b₁ holds b₂ ++ (max b₃,b₄) = max (b₂ ++ b₃),(b₂ ++ b₄)

proof end;

theorem Th51: :: FUZZY_2:51

for b₁ being non empty set
for b₂, b₃, b₄ being Membership_Func of b₁ holds b₂ ++ (min b₃,b₄) = min (b₂ ++ b₃),(b₂ ++ b₄)

proof end;

theorem Th52: :: FUZZY_2:52

for b₁ being non empty set
for b₂, b₃, b₄ being Membership_Func of b₁ holds max b₂,(b₃ * b₄) c=

proof end;

theorem Th53: :: FUZZY_2:53

for b₁ being non empty set
for b₂, b₃, b₄ being Membership_Func of b₁ holds min b₂,(b₃ * b₄) c=

proof end;

theorem Th54: :: FUZZY_2:54

for b₁ being non empty set
for b₂ being Element of b₁
for b₃, b₄ being Membership_Func of b₁ holds (b₃ ++ b₄) . b₂ = 1 - ((1 - (b₃ . b₂)) * (1 - (b₄ . b₂)))

proof end;

theorem Th55: :: FUZZY_2:55

for b₁ being non empty set
for b₂, b₃, b₄ being Membership_Func of b₁ holds (max b₂,b₃) ++ (max b₂,b₄) c=

proof end;

theorem Th56: :: FUZZY_2:56

for b₁ being non empty set
for b₂, b₃, b₄ being Membership_Func of b₁ holds (min b₂,b₃) ++ (min b₂,b₄) c=

proof end;