:: FUZZY_1 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

theorem Th1: :: FUZZY_1:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y being set holds rng (chi x,y) c= [.0,1.]
proof end;

definition
let C be non empty set ;
mode Membership_Func of C -> PartFunc of C, REAL means :Def1: :: FUZZY_1:def 1
( dom it = C & rng it c= [.0,1.] );
existence
ex b1 being PartFunc of C, REAL st
( dom b1 = C & rng b1 c= [.0,1.] )
proof end;
end;

:: deftheorem Def1 defines Membership_Func FUZZY_1:def 1 :
for C being non empty set
for b2 being PartFunc of C, REAL holds
( b2 is Membership_Func of C iff ( dom b2 = C & rng b2 c= [.0,1.] ) );

theorem Th2: :: FUZZY_1:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being non empty set holds chi C,C is Membership_Func of C
proof end;

registration
let X be non empty set ;
cluster -> real-yielding Membership_Func of X;
coherence
for b1 being Membership_Func of X holds b1 is real-yielding
;
end;

definition
let f, g be real-yielding Function;
pred f is_less_than g means :Def2: :: FUZZY_1:def 2
( dom f c= dom g & ( for x being set st x in dom f holds
f . x <= g . x ) );
reflexivity
for f being real-yielding Function holds
( dom f c= dom f & ( for x being set st x in dom f holds
f . x <= f . x ) )
;
end;

:: deftheorem Def2 defines is_less_than FUZZY_1:def 2 :
for f, g being real-yielding Function holds
( f is_less_than g iff ( dom f c= dom g & ( for x being set st x in dom f holds
f . x <= g . x ) ) );

notation
let X be non empty set ;
let f, g be Membership_Func of X;
synonym f c= g for X is_less_than f;
end;

definition
let X be non empty set ;
let f, g be Membership_Func of X;
:: original: is_less_than
redefine pred f is_less_than g means :Def3: :: FUZZY_1:def 3
for x being Element of X holds f . x <= g . x;
compatibility
( f is_less_than g iff for x being Element of X holds f . x <= g . x )
proof end;
end;

:: deftheorem Def3 defines is_less_than FUZZY_1:def 3 :
for X being non empty set
for f, g being Membership_Func of X holds
( f is_less_than g iff for x being Element of X holds f . x <= g . x );

Lm1: for C being non empty set
for f, g being Membership_Func of C st g c= & f c= holds
f = g
proof end;

theorem :: FUZZY_1:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being non empty set
for f, g being Membership_Func of C holds
( f = g iff ( g c= & f c= ) ) by Lm1;

theorem :: FUZZY_1:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being non empty set
for f being Membership_Func of C holds f c= ;

theorem :: FUZZY_1:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being non empty set
for f, g, h being Membership_Func of C st g c= & h c= holds
h c= ;

definition
let C be non empty set ;
let h, g be Membership_Func of C;
func min h,g -> Membership_Func of C means :Def4: :: FUZZY_1:def 4
for c being Element of C holds it . c = min (h . c),(g . c);
existence
ex b1 being Membership_Func of C st
for c being Element of C holds b1 . c = min (h . c),(g . c)
proof end;
uniqueness
for b1, b2 being Membership_Func of C st ( for c being Element of C holds b1 . c = min (h . c),(g . c) ) & ( for c being Element of C holds b2 . c = min (h . c),(g . c) ) holds
b1 = b2
proof end;
idempotence
for h being Membership_Func of C
for c being Element of C holds h . c = min (h . c),(h . c)
;
commutativity
for b1, h, g being Membership_Func of C st ( for c being Element of C holds b1 . c = min (h . c),(g . c) ) holds
for c being Element of C holds b1 . c = min (g . c),(h . c)
;
end;

:: deftheorem Def4 defines min FUZZY_1:def 4 :
for C being non empty set
for h, g, b4 being Membership_Func of C holds
( b4 = min h,g iff for c being Element of C holds b4 . c = min (h . c),(g . c) );

definition
let C be non empty set ;
let h, g be Membership_Func of C;
func max h,g -> Membership_Func of C means :Def5: :: FUZZY_1:def 5
for c being Element of C holds it . c = max (h . c),(g . c);
existence
ex b1 being Membership_Func of C st
for c being Element of C holds b1 . c = max (h . c),(g . c)
proof end;
uniqueness
for b1, b2 being Membership_Func of C st ( for c being Element of C holds b1 . c = max (h . c),(g . c) ) & ( for c being Element of C holds b2 . c = max (h . c),(g . c) ) holds
b1 = b2
proof end;
idempotence
for h being Membership_Func of C
for c being Element of C holds h . c = max (h . c),(h . c)
;
commutativity
for b1, h, g being Membership_Func of C st ( for c being Element of C holds b1 . c = max (h . c),(g . c) ) holds
for c being Element of C holds b1 . c = max (g . c),(h . c)
;
end;

:: deftheorem Def5 defines max FUZZY_1:def 5 :
for C being non empty set
for h, g, b4 being Membership_Func of C holds
( b4 = max h,g iff for c being Element of C holds b4 . c = max (h . c),(g . c) );

definition
let C be non empty set ;
let h be Membership_Func of C;
func 1_minus h -> Membership_Func of C means :Def6: :: FUZZY_1:def 6
for c being Element of C holds it . c = 1 - (h . c);
existence
ex b1 being Membership_Func of C st
for c being Element of C holds b1 . c = 1 - (h . c)
proof end;
uniqueness
for b1, b2 being Membership_Func of C st ( for c being Element of C holds b1 . c = 1 - (h . c) ) & ( for c being Element of C holds b2 . c = 1 - (h . c) ) holds
b1 = b2
proof end;
involutiveness
for b1, b2 being Membership_Func of C st ( for c being Element of C holds b1 . c = 1 - (b2 . c) ) holds
for c being Element of C holds b2 . c = 1 - (b1 . c)
proof end;
end;

:: deftheorem Def6 defines 1_minus FUZZY_1:def 6 :
for C being non empty set
for h, b3 being Membership_Func of C holds
( b3 = 1_minus h iff for c being Element of C holds b3 . c = 1 - (h . c) );

theorem :: FUZZY_1:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being non empty set
for c being Element of C
for h, g being Membership_Func of C holds
( min (h . c),(g . c) = (min h,g) . c & max (h . c),(g . c) = (max h,g) . c ) by Def4, Def5;

theorem :: FUZZY_1:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being non empty set
for h, f, g being Membership_Func of C holds
( max h,h = h & min h,h = h & max h,h = min h,h & min f,g = min g,f & max f,g = max g,f ) ;

theorem Th8: :: FUZZY_1:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being non empty set
for f, g, h being Membership_Func of C holds
( max (max f,g),h = max f,(max g,h) & min (min f,g),h = min f,(min g,h) )
proof end;

theorem Th9: :: FUZZY_1:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being non empty set
for f, g being Membership_Func of C holds
( max f,(min f,g) = f & min f,(max f,g) = f )
proof end;

theorem Th10: :: FUZZY_1:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being non empty set
for f, g, h being Membership_Func of C holds
( min f,(max g,h) = max (min f,g),(min f,h) & max f,(min g,h) = min (max f,g),(max f,h) )
proof end;

theorem :: FUZZY_1:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being non empty set
for h being Membership_Func of C holds 1_minus (1_minus h) = h ;

theorem Th12: :: FUZZY_1:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being non empty set
for f, g being Membership_Func of C holds
( 1_minus (max f,g) = min (1_minus f),(1_minus g) & 1_minus (min f,g) = max (1_minus f),(1_minus g) )
proof end;

theorem Th13: :: FUZZY_1:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being non empty set holds chi {} ,C is Membership_Func of C
proof end;

definition
let C be non empty set ;
func EMF C -> Membership_Func of C equals :: FUZZY_1:def 7
chi {} ,C;
correctness
coherence
chi {} ,C is Membership_Func of C
;
by Th13;
end;

:: deftheorem defines EMF FUZZY_1:def 7 :
for C being non empty set holds EMF C = chi {} ,C;

definition
let C be non empty set ;
func UMF C -> Membership_Func of C equals :: FUZZY_1:def 8
chi C,C;
correctness
coherence
chi C,C is Membership_Func of C
;
by Th2;
end;

:: deftheorem defines UMF FUZZY_1:def 8 :
for C being non empty set holds UMF C = chi C,C;

theorem Th14: :: FUZZY_1:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being non empty set
for a, b being Element of REAL
for f being PartFunc of C, REAL st rng f c= [.a,b.] & a <= b holds
for x being Element of C st x in dom f holds
( a <= f . x & f . x <= b )
proof end;

theorem Th15: :: FUZZY_1:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being non empty set
for f being Membership_Func of C holds f c=
proof end;

theorem Th16: :: FUZZY_1:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being non empty set
for f being Membership_Func of C holds UMF C c=
proof end;

theorem Th17: :: FUZZY_1:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being non empty set
for x being Element of C
for h being Membership_Func of C holds
( (EMF C) . x <= h . x & h . x <= (UMF C) . x )
proof end;

theorem Th18: :: FUZZY_1:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being non empty set
for f, g being Membership_Func of C holds
( f c= & max f,g c= )
proof end;

theorem Th19: :: FUZZY_1:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being non empty set
for f being Membership_Func of C holds
( max f,(UMF C) = UMF C & min f,(UMF C) = f & max f,(EMF C) = f & min f,(EMF C) = EMF C )
proof end;

theorem Th20: :: FUZZY_1:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being non empty set
for f, h, g being Membership_Func of C st h c= & h c= holds
h c=
proof end;

theorem :: FUZZY_1:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being non empty set
for f, g, h being Membership_Func of C st g c= holds
max g,h c=
proof end;

theorem :: FUZZY_1:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being non empty set
for f, g, h, h1 being Membership_Func of C st g c= & h1 c= holds
max g,h1 c=
proof end;

theorem :: FUZZY_1:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being non empty set
for f, g being Membership_Func of C st g c= holds
max f,g = g
proof end;

theorem :: FUZZY_1:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being non empty set
for f, g being Membership_Func of C holds max f,g c=
proof end;

theorem Th25: :: FUZZY_1:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being non empty set
for h, f, g being Membership_Func of C st f c= & g c= holds
min f,g c=
proof end;

theorem Th26: :: FUZZY_1:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b, c, d being Element of REAL st a <= b & c <= d holds
min a,c <= min b,d
proof end;

theorem :: FUZZY_1:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b, c being Element of REAL st a <= b holds
min a,c <= min b,c by Th26;

theorem :: FUZZY_1:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being non empty set
for f, g, h being Membership_Func of C st g c= holds
min g,h c=
proof end;

theorem :: FUZZY_1:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being non empty set
for f, g, h, h1 being Membership_Func of C st g c= & h1 c= holds
min g,h1 c=
proof end;

theorem Th30: :: FUZZY_1:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being non empty set
for f, g being Membership_Func of C st g c= holds
min f,g = f
proof end;

theorem :: FUZZY_1:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being non empty set
for f, g, h being Membership_Func of C st g c= & h c= & min g,h = EMF C holds
f = EMF C
proof end;

theorem :: FUZZY_1:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being non empty set
for f, g, h being Membership_Func of C st max (min f,g),(min f,h) = f holds
max g,h c=
proof end;

theorem :: FUZZY_1:33  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being non empty set
for f, g, h being Membership_Func of C st g c= & min g,h = EMF C holds
min f,h = EMF C
proof end;

theorem :: FUZZY_1:34  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being non empty set
for f being Membership_Func of C st EMF C c= holds
f = EMF C
proof end;

theorem :: FUZZY_1:35  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being non empty set
for f, g being Membership_Func of C holds
( max f,g = EMF C iff ( f = EMF C & g = EMF C ) )
proof end;

theorem :: FUZZY_1:36  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being non empty set
for f, g, h being Membership_Func of C holds
( f = max g,h iff ( f c= & f c= & ( for h1 being Membership_Func of C st h1 c= & h1 c= holds
h1 c= ) ) )
proof end;

theorem :: FUZZY_1:37  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being non empty set
for f, g, h being Membership_Func of C holds
( f = min g,h iff ( g c= & h c= & ( for h1 being Membership_Func of C st g c= & h c= holds
f c= ) ) )
proof end;

theorem :: FUZZY_1:38  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being non empty set
for f, g, h being Membership_Func of C st max g,h c= & min f,h = EMF C holds
g c=
proof end;

Lm2: for C being non empty set
for f, g being Membership_Func of C st g c= holds
1_minus f c=
proof end;

theorem Th39: :: FUZZY_1:39  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being non empty set
for f, g being Membership_Func of C holds
( g c= iff 1_minus f c= )
proof end;

theorem :: FUZZY_1:40  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being non empty set
for f, g being Membership_Func of C holds
( 1_minus g c= iff 1_minus f c= )
proof end;

theorem :: FUZZY_1:41  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being non empty set
for f, g being Membership_Func of C holds 1_minus f c=
proof end;

theorem :: FUZZY_1:42  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being non empty set
for f, g being Membership_Func of C holds 1_minus (min f,g) c=
proof end;

theorem Th43: :: FUZZY_1:43  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being non empty set
for x being Element of C holds
( (EMF C) . x = 0 & (UMF C) . x = 1 ) by FUNCT_3:def 3;

theorem Th44: :: FUZZY_1:44  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being non empty set holds
( 1_minus (EMF C) = UMF C & 1_minus (UMF C) = EMF C )
proof end;

definition
let C be non empty set ;
let h, g be Membership_Func of C;
func h \+\ g -> Membership_Func of C equals :: FUZZY_1:def 9
max (min h,(1_minus g)),(min (1_minus h),g);
coherence
max (min h,(1_minus g)),(min (1_minus h),g) is Membership_Func of C
;
commutativity
for b1, h, g being Membership_Func of C st b1 = max (min h,(1_minus g)),(min (1_minus h),g) holds
b1 = max (min g,(1_minus h)),(min (1_minus g),h)
;
end;

:: deftheorem defines \+\ FUZZY_1:def 9 :
for C being non empty set
for h, g being Membership_Func of C holds h \+\ g = max (min h,(1_minus g)),(min (1_minus h),g);

theorem :: FUZZY_1:45  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being non empty set
for f being Membership_Func of C holds f \+\ (EMF C) = f
proof end;

theorem :: FUZZY_1:46  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being non empty set
for f being Membership_Func of C holds f \+\ (UMF C) = 1_minus f
proof end;

theorem :: FUZZY_1:47  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being non empty set
for f, g, h being Membership_Func of C holds min (min (max f,g),(max g,h)),(max h,f) = max (max (min f,g),(min g,h)),(min h,f)
proof end;

theorem :: FUZZY_1:48  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being non empty set
for f, g being Membership_Func of C holds 1_minus (f \+\ g) c=
proof end;

theorem :: FUZZY_1:49  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being non empty set
for f, g being Membership_Func of C holds max f,g c=
proof end;

theorem :: FUZZY_1:50  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being non empty set
for f being Membership_Func of C holds f \+\ f = min f,(1_minus f) ;

definition
let C be non empty set ;
let h, g be Membership_Func of C;
func ab_difMF h,g -> Membership_Func of C means :: FUZZY_1:def 10
for c being Element of C holds it . c = abs ((h . c) - (g . c));
existence
ex b1 being Membership_Func of C st
for c being Element of C holds b1 . c = abs ((h . c) - (g . c))
proof end;
uniqueness
for b1, b2 being Membership_Func of C st ( for c being Element of C holds b1 . c = abs ((h . c) - (g . c)) ) & ( for c being Element of C holds b2 . c = abs ((h . c) - (g . c)) ) holds
b1 = b2
proof end;
end;

:: deftheorem defines ab_difMF FUZZY_1:def 10 :
for C being non empty set
for h, g, b4 being Membership_Func of C holds
( b4 = ab_difMF h,g iff for c being Element of C holds b4 . c = abs ((h . c) - (g . c)) );