:: by Adam Grabowski

::

:: Received June 27, 2017

:: Copyright (c) 2017 Association of Mizar Users

theorem Lemma3: :: FUZNORM1:6

for a, b, c being Element of [.0,1.] holds max (0,(((max (0,((a + b) - 1))) + c) - 1)) = max (0,((a + (max (0,((b + c) - 1)))) - 1))

proof end;

registration
end;

theorem MES57: :: FUZNORM1:17

for x, y, k being Real st k <= 0 holds

( k * (min (x,y)) = max ((k * x),(k * y)) & k * (max (x,y)) = min ((k * x),(k * y)) )

( k * (min (x,y)) = max ((k * x),(k * y)) & k * (max (x,y)) = min ((k * x),(k * y)) )

proof end;

definition

let A be real-membered set ;

let f be BinOp of A;

end;
let f be BinOp of A;

attr f is monotonic means :MonDef: :: FUZNORM1:def 1

for a, b, c, d being Element of A st a <= c & b <= d holds

f . (a,b) <= f . (c,d);

for a, b, c, d being Element of A st a <= c & b <= d holds

f . (a,b) <= f . (c,d);

attr f is with-1-identity means :IdDef: :: FUZNORM1:def 2

for a being Element of A holds f . (a,1) = a;

for a being Element of A holds f . (a,1) = a;

attr f is with-0-identity means :ZeroDef: :: FUZNORM1:def 4

for a being Element of A holds f . (a,0) = a;

for a being Element of A holds f . (a,0) = a;

attr f is with-0-annihilating means :: FUZNORM1:def 5

for a being Element of A holds f . (a,0) = 0 ;

for a being Element of A holds f . (a,0) = 0 ;

:: deftheorem MonDef defines monotonic FUZNORM1:def 1 :

for A being real-membered set

for f being BinOp of A holds

( f is monotonic iff for a, b, c, d being Element of A st a <= c & b <= d holds

f . (a,b) <= f . (c,d) );

for A being real-membered set

for f being BinOp of A holds

( f is monotonic iff for a, b, c, d being Element of A st a <= c & b <= d holds

f . (a,b) <= f . (c,d) );

:: deftheorem IdDef defines with-1-identity FUZNORM1:def 2 :

for A being real-membered set

for f being BinOp of A holds

( f is with-1-identity iff for a being Element of A holds f . (a,1) = a );

for A being real-membered set

for f being BinOp of A holds

( f is with-1-identity iff for a being Element of A holds f . (a,1) = a );

:: deftheorem defines with-1-annihilating FUZNORM1:def 3 :

for A being real-membered set

for f being BinOp of A holds

( f is with-1-annihilating iff for a being Element of A holds f . (a,1) = 1 );

for A being real-membered set

for f being BinOp of A holds

( f is with-1-annihilating iff for a being Element of A holds f . (a,1) = 1 );

:: deftheorem ZeroDef defines with-0-identity FUZNORM1:def 4 :

for A being real-membered set

for f being BinOp of A holds

( f is with-0-identity iff for a being Element of A holds f . (a,0) = a );

for A being real-membered set

for f being BinOp of A holds

( f is with-0-identity iff for a being Element of A holds f . (a,0) = a );

:: deftheorem defines with-0-annihilating FUZNORM1:def 5 :

for A being real-membered set

for f being BinOp of A holds

( f is with-0-annihilating iff for a being Element of A holds f . (a,0) = 0 );

for A being real-membered set

for f being BinOp of A holds

( f is with-0-annihilating iff for a being Element of A holds f . (a,0) = 0 );

definition

ex b_{1} being BinOp of [.0,1.] st

for a, b being Element of [.0,1.] holds b_{1} . (a,b) = min (a,b)

for b_{1}, b_{2} being BinOp of [.0,1.] st ( for a, b being Element of [.0,1.] holds b_{1} . (a,b) = min (a,b) ) & ( for a, b being Element of [.0,1.] holds b_{2} . (a,b) = min (a,b) ) holds

b_{1} = b_{2}
end;

func minnorm -> BinOp of [.0,1.] means :MinDef: :: FUZNORM1:def 6

for a, b being Element of [.0,1.] holds it . (a,b) = min (a,b);

existence for a, b being Element of [.0,1.] holds it . (a,b) = min (a,b);

ex b

for a, b being Element of [.0,1.] holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem MinDef defines minnorm FUZNORM1:def 6 :

for b_{1} being BinOp of [.0,1.] holds

( b_{1} = minnorm iff for a, b being Element of [.0,1.] holds b_{1} . (a,b) = min (a,b) );

for b

( b

registration

coherence

( minnorm is commutative & minnorm is associative & minnorm is monotonic & minnorm is with-1-identity )

end;
( minnorm is commutative & minnorm is associative & minnorm is monotonic & minnorm is with-1-identity )

proof end;

registration

ex b_{1} being BinOp of [.0,1.] st

( b_{1} is commutative & b_{1} is associative & b_{1} is monotonic & b_{1} is with-1-identity )
end;

cluster Relation-like [:[.0,1.],[.0,1.]:] -defined [.0,1.] -valued Function-like V26([:[.0,1.],[.0,1.]:]) V30([:[.0,1.],[.0,1.]:],[.0,1.]) commutative associative monotonic with-1-identity for Element of bool [:[:[.0,1.],[.0,1.]:],[.0,1.]:];

existence ex b

( b

proof end;

definition

ex b_{1} being BinOp of [.0,1.] st

for a, b being Element of [.0,1.] holds b_{1} . (a,b) = max (a,b)

for b_{1}, b_{2} being BinOp of [.0,1.] st ( for a, b being Element of [.0,1.] holds b_{1} . (a,b) = max (a,b) ) & ( for a, b being Element of [.0,1.] holds b_{2} . (a,b) = max (a,b) ) holds

b_{1} = b_{2}
end;

func maxnorm -> BinOp of [.0,1.] means :MaxDef: :: FUZNORM1:def 7

for a, b being Element of [.0,1.] holds it . (a,b) = max (a,b);

existence for a, b being Element of [.0,1.] holds it . (a,b) = max (a,b);

ex b

for a, b being Element of [.0,1.] holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem MaxDef defines maxnorm FUZNORM1:def 7 :

for b_{1} being BinOp of [.0,1.] holds

( b_{1} = maxnorm iff for a, b being Element of [.0,1.] holds b_{1} . (a,b) = max (a,b) );

for b

( b

registration

coherence

( maxnorm is commutative & maxnorm is associative & maxnorm is monotonic & maxnorm is with-0-identity )

end;
( maxnorm is commutative & maxnorm is associative & maxnorm is monotonic & maxnorm is with-0-identity )

proof end;

registration

ex b_{1} being BinOp of [.0,1.] st

( b_{1} is commutative & b_{1} is associative & b_{1} is monotonic & b_{1} is with-0-identity )
end;

cluster Relation-like [:[.0,1.],[.0,1.]:] -defined [.0,1.] -valued Function-like V26([:[.0,1.],[.0,1.]:]) V30([:[.0,1.],[.0,1.]:],[.0,1.]) commutative associative monotonic with-0-identity for Element of bool [:[:[.0,1.],[.0,1.]:],[.0,1.]:];

existence ex b

( b

proof end;

definition
end;

theorem NormIs0: :: FUZNORM1:18

for t being commutative monotonic with-1-identity BinOp of [.0,1.]

for a being Element of [.0,1.] holds t . (a,0) = 0

for a being Element of [.0,1.] holds t . (a,0) = 0

proof end;

theorem ConormIs1: :: FUZNORM1:19

for t being commutative monotonic with-0-identity BinOp of [.0,1.]

for a being Element of [.0,1.] holds t . (a,1) = 1

for a being Element of [.0,1.] holds t . (a,1) = 1

proof end;

registration

for b_{1} being commutative monotonic with-1-identity BinOp of [.0,1.] holds b_{1} is with-0-annihilating
by NormIs0;

for b_{1} being commutative monotonic with-0-identity BinOp of [.0,1.] holds b_{1} is with-1-annihilating
by ConormIs1;

end;

cluster Function-like V30([:[.0,1.],[.0,1.]:],[.0,1.]) commutative monotonic with-1-identity -> commutative monotonic with-1-identity with-0-annihilating for Element of bool [:[:[.0,1.],[.0,1.]:],[.0,1.]:];

coherence for b

cluster Function-like V30([:[.0,1.],[.0,1.]:],[.0,1.]) commutative monotonic with-0-identity -> commutative monotonic with-1-annihilating with-0-identity for Element of bool [:[:[.0,1.],[.0,1.]:],[.0,1.]:];

coherence for b

definition

ex b_{1} being BinOp of [.0,1.] st

for a, b being Element of [.0,1.] holds b_{1} . (a,b) = a * b

for b_{1}, b_{2} being BinOp of [.0,1.] st ( for a, b being Element of [.0,1.] holds b_{1} . (a,b) = a * b ) & ( for a, b being Element of [.0,1.] holds b_{2} . (a,b) = a * b ) holds

b_{1} = b_{2}
end;

func prodnorm -> BinOp of [.0,1.] means :ProdDef: :: FUZNORM1:def 8

for a, b being Element of [.0,1.] holds it . (a,b) = a * b;

existence for a, b being Element of [.0,1.] holds it . (a,b) = a * b;

ex b

for a, b being Element of [.0,1.] holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem ProdDef defines prodnorm FUZNORM1:def 8 :

for b_{1} being BinOp of [.0,1.] holds

( b_{1} = prodnorm iff for a, b being Element of [.0,1.] holds b_{1} . (a,b) = a * b );

for b

( b

registration

coherence

( prodnorm is commutative & prodnorm is associative & prodnorm is monotonic & prodnorm is with-1-identity )

end;
( prodnorm is commutative & prodnorm is associative & prodnorm is monotonic & prodnorm is with-1-identity )

proof end;

definition

ex b_{1} being BinOp of [.0,1.] st

for a, b being Element of [.0,1.] holds b_{1} . (a,b) = (a + b) - (a * b)

for b_{1}, b_{2} being BinOp of [.0,1.] st ( for a, b being Element of [.0,1.] holds b_{1} . (a,b) = (a + b) - (a * b) ) & ( for a, b being Element of [.0,1.] holds b_{2} . (a,b) = (a + b) - (a * b) ) holds

b_{1} = b_{2}
end;

func probsum_conorm -> BinOp of [.0,1.] means :ProbSumDef: :: FUZNORM1:def 9

for a, b being Element of [.0,1.] holds it . (a,b) = (a + b) - (a * b);

existence for a, b being Element of [.0,1.] holds it . (a,b) = (a + b) - (a * b);

ex b

for a, b being Element of [.0,1.] holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem ProbSumDef defines probsum_conorm FUZNORM1:def 9 :

for b_{1} being BinOp of [.0,1.] holds

( b_{1} = probsum_conorm iff for a, b being Element of [.0,1.] holds b_{1} . (a,b) = (a + b) - (a * b) );

for b

( b

definition

ex b_{1} being BinOp of [.0,1.] st

for a, b being Element of [.0,1.] holds b_{1} . (a,b) = max (0,((a + b) - 1))

for b_{1}, b_{2} being BinOp of [.0,1.] st ( for a, b being Element of [.0,1.] holds b_{1} . (a,b) = max (0,((a + b) - 1)) ) & ( for a, b being Element of [.0,1.] holds b_{2} . (a,b) = max (0,((a + b) - 1)) ) holds

b_{1} = b_{2}
end;

func Lukasiewicz_norm -> BinOp of [.0,1.] means :LukNorm: :: FUZNORM1:def 10

for a, b being Element of [.0,1.] holds it . (a,b) = max (0,((a + b) - 1));

existence for a, b being Element of [.0,1.] holds it . (a,b) = max (0,((a + b) - 1));

ex b

for a, b being Element of [.0,1.] holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem LukNorm defines Lukasiewicz_norm FUZNORM1:def 10 :

for b_{1} being BinOp of [.0,1.] holds

( b_{1} = Lukasiewicz_norm iff for a, b being Element of [.0,1.] holds b_{1} . (a,b) = max (0,((a + b) - 1)) );

for b

( b

registration

coherence

( Lukasiewicz_norm is commutative & Lukasiewicz_norm is associative & Lukasiewicz_norm is monotonic & Lukasiewicz_norm is with-1-identity )

end;
( Lukasiewicz_norm is commutative & Lukasiewicz_norm is associative & Lukasiewicz_norm is monotonic & Lukasiewicz_norm is with-1-identity )

proof end;

definition

ex b_{1} being BinOp of [.0,1.] st

for a, b being Element of [.0,1.] holds

( ( max (a,b) = 1 implies b_{1} . (a,b) = min (a,b) ) & ( max (a,b) <> 1 implies b_{1} . (a,b) = 0 ) )

for b_{1}, b_{2} being BinOp of [.0,1.] st ( for a, b being Element of [.0,1.] holds

( ( max (a,b) = 1 implies b_{1} . (a,b) = min (a,b) ) & ( max (a,b) <> 1 implies b_{1} . (a,b) = 0 ) ) ) & ( for a, b being Element of [.0,1.] holds

( ( max (a,b) = 1 implies b_{2} . (a,b) = min (a,b) ) & ( max (a,b) <> 1 implies b_{2} . (a,b) = 0 ) ) ) holds

b_{1} = b_{2}
end;

func drastic_norm -> BinOp of [.0,1.] means :Drastic2Def: :: FUZNORM1:def 11

for a, b being Element of [.0,1.] holds

( ( max (a,b) = 1 implies it . (a,b) = min (a,b) ) & ( max (a,b) <> 1 implies it . (a,b) = 0 ) );

existence for a, b being Element of [.0,1.] holds

( ( max (a,b) = 1 implies it . (a,b) = min (a,b) ) & ( max (a,b) <> 1 implies it . (a,b) = 0 ) );

ex b

for a, b being Element of [.0,1.] holds

( ( max (a,b) = 1 implies b

proof end;

uniqueness for b

( ( max (a,b) = 1 implies b

( ( max (a,b) = 1 implies b

b

proof end;

:: deftheorem Drastic2Def defines drastic_norm FUZNORM1:def 11 :

for b_{1} being BinOp of [.0,1.] holds

( b_{1} = drastic_norm iff for a, b being Element of [.0,1.] holds

( ( max (a,b) = 1 implies b_{1} . (a,b) = min (a,b) ) & ( max (a,b) <> 1 implies b_{1} . (a,b) = 0 ) ) );

for b

( b

( ( max (a,b) = 1 implies b

theorem DrasticDef: :: FUZNORM1:20

for a, b being Element of [.0,1.] holds

( ( a = 1 implies drastic_norm . (a,b) = b ) & ( b = 1 implies drastic_norm . (a,b) = a ) & ( a <> 1 & b <> 1 implies drastic_norm . (a,b) = 0 ) )

( ( a = 1 implies drastic_norm . (a,b) = b ) & ( b = 1 implies drastic_norm . (a,b) = a ) & ( a <> 1 & b <> 1 implies drastic_norm . (a,b) = 0 ) )

proof end;

registration

coherence

( drastic_norm is commutative & drastic_norm is associative & drastic_norm is with-1-identity & drastic_norm is monotonic )

end;
( drastic_norm is commutative & drastic_norm is associative & drastic_norm is with-1-identity & drastic_norm is monotonic )

proof end;

definition

ex b_{1} being BinOp of [.0,1.] st

for a, b being Element of [.0,1.] holds

( ( a + b > 1 implies b_{1} . (a,b) = min (a,b) ) & ( a + b <= 1 implies b_{1} . (a,b) = 0 ) )

for b_{1}, b_{2} being BinOp of [.0,1.] st ( for a, b being Element of [.0,1.] holds

( ( a + b > 1 implies b_{1} . (a,b) = min (a,b) ) & ( a + b <= 1 implies b_{1} . (a,b) = 0 ) ) ) & ( for a, b being Element of [.0,1.] holds

( ( a + b > 1 implies b_{2} . (a,b) = min (a,b) ) & ( a + b <= 1 implies b_{2} . (a,b) = 0 ) ) ) holds

b_{1} = b_{2}
end;

func nilmin_norm -> BinOp of [.0,1.] means :NilminDef: :: FUZNORM1:def 12

for a, b being Element of [.0,1.] holds

( ( a + b > 1 implies it . (a,b) = min (a,b) ) & ( a + b <= 1 implies it . (a,b) = 0 ) );

existence for a, b being Element of [.0,1.] holds

( ( a + b > 1 implies it . (a,b) = min (a,b) ) & ( a + b <= 1 implies it . (a,b) = 0 ) );

ex b

for a, b being Element of [.0,1.] holds

( ( a + b > 1 implies b

proof end;

uniqueness for b

( ( a + b > 1 implies b

( ( a + b > 1 implies b

b

proof end;

:: deftheorem NilminDef defines nilmin_norm FUZNORM1:def 12 :

for b_{1} being BinOp of [.0,1.] holds

( b_{1} = nilmin_norm iff for a, b being Element of [.0,1.] holds

( ( a + b > 1 implies b_{1} . (a,b) = min (a,b) ) & ( a + b <= 1 implies b_{1} . (a,b) = 0 ) ) );

for b

( b

( ( a + b > 1 implies b

registration

coherence

( nilmin_norm is commutative & nilmin_norm is associative & nilmin_norm is with-1-identity & nilmin_norm is monotonic )

end;
( nilmin_norm is commutative & nilmin_norm is associative & nilmin_norm is with-1-identity & nilmin_norm is monotonic )

proof end;

definition

ex b_{1} being BinOp of [.0,1.] st

for a, b being Element of [.0,1.] holds b_{1} . (a,b) = (a * b) / ((a + b) - (a * b))

for b_{1}, b_{2} being BinOp of [.0,1.] st ( for a, b being Element of [.0,1.] holds b_{1} . (a,b) = (a * b) / ((a + b) - (a * b)) ) & ( for a, b being Element of [.0,1.] holds b_{2} . (a,b) = (a * b) / ((a + b) - (a * b)) ) holds

b_{1} = b_{2}
end;

func Hamacher_norm -> BinOp of [.0,1.] means :HamDef: :: FUZNORM1:def 13

for a, b being Element of [.0,1.] holds it . (a,b) = (a * b) / ((a + b) - (a * b));

existence for a, b being Element of [.0,1.] holds it . (a,b) = (a * b) / ((a + b) - (a * b));

ex b

for a, b being Element of [.0,1.] holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem HamDef defines Hamacher_norm FUZNORM1:def 13 :

for b_{1} being BinOp of [.0,1.] holds

( b_{1} = Hamacher_norm iff for a, b being Element of [.0,1.] holds b_{1} . (a,b) = (a * b) / ((a + b) - (a * b)) );

for b

( b

registration

coherence

( Hamacher_norm is commutative & Hamacher_norm is associative & Hamacher_norm is with-1-identity & Hamacher_norm is monotonic )

end;
( Hamacher_norm is commutative & Hamacher_norm is associative & Hamacher_norm is with-1-identity & Hamacher_norm is monotonic )

proof end;

definition

ex b_{1} being BinOp of [.0,1.] st

for a, b being Element of [.0,1.] holds

( ( min (a,b) = 0 implies b_{1} . (a,b) = max (a,b) ) & ( min (a,b) <> 0 implies b_{1} . (a,b) = 1 ) )

for b_{1}, b_{2} being BinOp of [.0,1.] st ( for a, b being Element of [.0,1.] holds

( ( min (a,b) = 0 implies b_{1} . (a,b) = max (a,b) ) & ( min (a,b) <> 0 implies b_{1} . (a,b) = 1 ) ) ) & ( for a, b being Element of [.0,1.] holds

( ( min (a,b) = 0 implies b_{2} . (a,b) = max (a,b) ) & ( min (a,b) <> 0 implies b_{2} . (a,b) = 1 ) ) ) holds

b_{1} = b_{2}
end;

func drastic_conorm -> BinOp of [.0,1.] means :Drastic2CDef: :: FUZNORM1:def 14

for a, b being Element of [.0,1.] holds

( ( min (a,b) = 0 implies it . (a,b) = max (a,b) ) & ( min (a,b) <> 0 implies it . (a,b) = 1 ) );

existence for a, b being Element of [.0,1.] holds

( ( min (a,b) = 0 implies it . (a,b) = max (a,b) ) & ( min (a,b) <> 0 implies it . (a,b) = 1 ) );

ex b

for a, b being Element of [.0,1.] holds

( ( min (a,b) = 0 implies b

proof end;

uniqueness for b

( ( min (a,b) = 0 implies b

( ( min (a,b) = 0 implies b

b

proof end;

:: deftheorem Drastic2CDef defines drastic_conorm FUZNORM1:def 14 :

for b_{1} being BinOp of [.0,1.] holds

( b_{1} = drastic_conorm iff for a, b being Element of [.0,1.] holds

( ( min (a,b) = 0 implies b_{1} . (a,b) = max (a,b) ) & ( min (a,b) <> 0 implies b_{1} . (a,b) = 1 ) ) );

for b

( b

( ( min (a,b) = 0 implies b

definition

let t be BinOp of [.0,1.];

ex b_{1} being BinOp of [.0,1.] st

for a, b being Element of [.0,1.] holds b_{1} . (a,b) = 1 - (t . ((1 - a),(1 - b)))

for b_{1}, b_{2} being BinOp of [.0,1.] st ( for a, b being Element of [.0,1.] holds b_{1} . (a,b) = 1 - (t . ((1 - a),(1 - b))) ) & ( for a, b being Element of [.0,1.] holds b_{2} . (a,b) = 1 - (t . ((1 - a),(1 - b))) ) holds

b_{1} = b_{2}

end;
func conorm t -> BinOp of [.0,1.] means :CoDef: :: FUZNORM1:def 15

for a, b being Element of [.0,1.] holds it . (a,b) = 1 - (t . ((1 - a),(1 - b)));

existence for a, b being Element of [.0,1.] holds it . (a,b) = 1 - (t . ((1 - a),(1 - b)));

ex b

for a, b being Element of [.0,1.] holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem CoDef defines conorm FUZNORM1:def 15 :

for t, b_{2} being BinOp of [.0,1.] holds

( b_{2} = conorm t iff for a, b being Element of [.0,1.] holds b_{2} . (a,b) = 1 - (t . ((1 - a),(1 - b))) );

for t, b

( b

registration

let t be t-norm;

coherence

( conorm t is monotonic & conorm t is commutative & conorm t is associative & conorm t is with-0-identity )

end;
coherence

( conorm t is monotonic & conorm t is commutative & conorm t is associative & conorm t is with-0-identity )

proof end;

:: deftheorem defines <= FUZNORM1:def 16 :

for f1, f2 being BinOp of [.0,1.] holds

( f1 <= f2 iff for a, b being Element of [.0,1.] holds f1 . (a,b) <= f2 . (a,b) );

for f1, f2 being BinOp of [.0,1.] holds

( f1 <= f2 iff for a, b being Element of [.0,1.] holds f1 . (a,b) <= f2 . (a,b) );

definition

ex b_{1} being BinOp of [.0,1.] st

for a, b being Element of [.0,1.] holds

( ( a = b & b = 1 implies b_{1} . (a,b) = 1 ) & ( ( a <> 1 or b <> 1 ) implies b_{1} . (a,b) = ((a + b) - ((2 * a) * b)) / (1 - (a * b)) ) )

for b_{1}, b_{2} being BinOp of [.0,1.] st ( for a, b being Element of [.0,1.] holds

( ( a = b & b = 1 implies b_{1} . (a,b) = 1 ) & ( ( a <> 1 or b <> 1 ) implies b_{1} . (a,b) = ((a + b) - ((2 * a) * b)) / (1 - (a * b)) ) ) ) & ( for a, b being Element of [.0,1.] holds

( ( a = b & b = 1 implies b_{2} . (a,b) = 1 ) & ( ( a <> 1 or b <> 1 ) implies b_{2} . (a,b) = ((a + b) - ((2 * a) * b)) / (1 - (a * b)) ) ) ) holds

b_{1} = b_{2}
end;

func Hamacher_conorm -> BinOp of [.0,1.] means :HamCoDef: :: FUZNORM1:def 17

for a, b being Element of [.0,1.] holds

( ( a = b & b = 1 implies it . (a,b) = 1 ) & ( ( a <> 1 or b <> 1 ) implies it . (a,b) = ((a + b) - ((2 * a) * b)) / (1 - (a * b)) ) );

existence for a, b being Element of [.0,1.] holds

( ( a = b & b = 1 implies it . (a,b) = 1 ) & ( ( a <> 1 or b <> 1 ) implies it . (a,b) = ((a + b) - ((2 * a) * b)) / (1 - (a * b)) ) );

ex b

for a, b being Element of [.0,1.] holds

( ( a = b & b = 1 implies b

proof end;

uniqueness for b

( ( a = b & b = 1 implies b

( ( a = b & b = 1 implies b

b

proof end;

:: deftheorem HamCoDef defines Hamacher_conorm FUZNORM1:def 17 :

for b_{1} being BinOp of [.0,1.] holds

( b_{1} = Hamacher_conorm iff for a, b being Element of [.0,1.] holds

( ( a = b & b = 1 implies b_{1} . (a,b) = 1 ) & ( ( a <> 1 or b <> 1 ) implies b_{1} . (a,b) = ((a + b) - ((2 * a) * b)) / (1 - (a * b)) ) ) );

for b

( b

( ( a = b & b = 1 implies b

registration

coherence

( Hamacher_conorm is commutative & Hamacher_conorm is associative & Hamacher_conorm is with-0-identity & Hamacher_conorm is monotonic ) by CoHam;

end;
( Hamacher_conorm is commutative & Hamacher_conorm is associative & Hamacher_conorm is with-0-identity & Hamacher_conorm is monotonic ) by CoHam;

registration

coherence

( probsum_conorm is commutative & probsum_conorm is associative & probsum_conorm is with-0-identity & probsum_conorm is monotonic ) by ConormProd;

end;
( probsum_conorm is commutative & probsum_conorm is associative & probsum_conorm is with-0-identity & probsum_conorm is monotonic ) by ConormProd;

definition

ex b_{1} being BinOp of [.0,1.] st

for a, b being Element of [.0,1.] holds

( ( a + b < 1 implies b_{1} . (a,b) = max (a,b) ) & ( a + b >= 1 implies b_{1} . (a,b) = 1 ) )

for b_{1}, b_{2} being BinOp of [.0,1.] st ( for a, b being Element of [.0,1.] holds

( ( a + b < 1 implies b_{1} . (a,b) = max (a,b) ) & ( a + b >= 1 implies b_{1} . (a,b) = 1 ) ) ) & ( for a, b being Element of [.0,1.] holds

( ( a + b < 1 implies b_{2} . (a,b) = max (a,b) ) & ( a + b >= 1 implies b_{2} . (a,b) = 1 ) ) ) holds

b_{1} = b_{2}
end;

func nilmax_conorm -> BinOp of [.0,1.] means :NilmaxDef: :: FUZNORM1:def 18

for a, b being Element of [.0,1.] holds

( ( a + b < 1 implies it . (a,b) = max (a,b) ) & ( a + b >= 1 implies it . (a,b) = 1 ) );

existence for a, b being Element of [.0,1.] holds

( ( a + b < 1 implies it . (a,b) = max (a,b) ) & ( a + b >= 1 implies it . (a,b) = 1 ) );

ex b

for a, b being Element of [.0,1.] holds

( ( a + b < 1 implies b

proof end;

uniqueness for b

( ( a + b < 1 implies b

( ( a + b < 1 implies b

b

proof end;

:: deftheorem NilmaxDef defines nilmax_conorm FUZNORM1:def 18 :

for b_{1} being BinOp of [.0,1.] holds

( b_{1} = nilmax_conorm iff for a, b being Element of [.0,1.] holds

( ( a + b < 1 implies b_{1} . (a,b) = max (a,b) ) & ( a + b >= 1 implies b_{1} . (a,b) = 1 ) ) );

for b

( b

( ( a + b < 1 implies b

registration

coherence

( nilmax_conorm is commutative & nilmax_conorm is associative & nilmax_conorm is with-0-identity & nilmax_conorm is monotonic ) by ConormNilmin;

end;
( nilmax_conorm is commutative & nilmax_conorm is associative & nilmax_conorm is with-0-identity & nilmax_conorm is monotonic ) by ConormNilmin;

definition

ex b_{1} being BinOp of [.0,1.] st

for a, b being Element of [.0,1.] holds b_{1} . (a,b) = min ((a + b),1)

for b_{1}, b_{2} being BinOp of [.0,1.] st ( for a, b being Element of [.0,1.] holds b_{1} . (a,b) = min ((a + b),1) ) & ( for a, b being Element of [.0,1.] holds b_{2} . (a,b) = min ((a + b),1) ) holds

b_{1} = b_{2}
end;

func BoundedSum_conorm -> BinOp of [.0,1.] means :LukConorm: :: FUZNORM1:def 19

for a, b being Element of [.0,1.] holds it . (a,b) = min ((a + b),1);

existence for a, b being Element of [.0,1.] holds it . (a,b) = min ((a + b),1);

ex b

for a, b being Element of [.0,1.] holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem LukConorm defines BoundedSum_conorm FUZNORM1:def 19 :

for b_{1} being BinOp of [.0,1.] holds

( b_{1} = BoundedSum_conorm iff for a, b being Element of [.0,1.] holds b_{1} . (a,b) = min ((a + b),1) );

for b

( b

registration

coherence

( BoundedSum_conorm is commutative & BoundedSum_conorm is associative & BoundedSum_conorm is with-0-identity & BoundedSum_conorm is monotonic ) by ConormLukasiewicz;

end;
( BoundedSum_conorm is commutative & BoundedSum_conorm is associative & BoundedSum_conorm is with-0-identity & BoundedSum_conorm is monotonic ) by ConormLukasiewicz;