:: by Adam Grabowski

::

:: Received September 3, 2017

:: Copyright (c) 2017-2018 Association of Mizar Users

definition

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

end;
attr f is decreasing_on_1st means :DefDecr: :: FUZIMPL1:def 1

for x1, x2, y being Element of [.0,1.] st x1 <= x2 holds

f . (x1,y) >= f . (x2,y);

for x1, x2, y being Element of [.0,1.] st x1 <= x2 holds

f . (x1,y) >= f . (x2,y);

:: deftheorem DefDecr defines decreasing_on_1st FUZIMPL1:def 1 :

for f being BinOp of [.0,1.] holds

( f is decreasing_on_1st iff for x1, x2, y being Element of [.0,1.] st x1 <= x2 holds

f . (x1,y) >= f . (x2,y) );

for f being BinOp of [.0,1.] holds

( f is decreasing_on_1st iff for x1, x2, y being Element of [.0,1.] st x1 <= x2 holds

f . (x1,y) >= f . (x2,y) );

:: deftheorem DefIncr defines increasing_on_2nd FUZIMPL1:def 2 :

for f being BinOp of [.0,1.] holds

( f is increasing_on_2nd iff for x, y1, y2 being Element of [.0,1.] st y1 <= y2 holds

f . (x,y1) <= f . (x,y2) );

for f being BinOp of [.0,1.] holds

( f is increasing_on_2nd iff for x, y1, y2 being Element of [.0,1.] st y1 <= y2 holds

f . (x,y1) <= f . (x,y2) );

:: deftheorem Def00 defines 00-dominant FUZIMPL1:def 3 :

for f being BinOp of [.0,1.] holds

( f is 00-dominant iff f . (0,0) = 1 );

for f being BinOp of [.0,1.] holds

( f is 00-dominant iff f . (0,0) = 1 );

:: deftheorem Def11 defines 11-dominant FUZIMPL1:def 4 :

for f being BinOp of [.0,1.] holds

( f is 11-dominant iff f . (1,1) = 1 );

for f being BinOp of [.0,1.] holds

( f is 11-dominant iff f . (1,1) = 1 );

:: deftheorem Def10 defines 10-weak FUZIMPL1:def 5 :

for f being BinOp of [.0,1.] holds

( f is 10-weak iff f . (1,0) = 0 );

for f being BinOp of [.0,1.] holds

( f is 10-weak iff f . (1,0) = 0 );

:: deftheorem defines 01-dominant FUZIMPL1:def 6 :

for f being BinOp of [.0,1.] holds

( f is 01-dominant iff f . (0,1) = 1 );

for f being BinOp of [.0,1.] holds

( f is 01-dominant iff f . (0,1) = 1 );

:: Classical Implication

definition

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

end;
attr f is with_properties_of_fuzzy_implication means :: FUZIMPL1:def 7

( f is decreasing_on_1st & f is increasing_on_2nd & f is 00-dominant & f is 11-dominant & f is 10-weak );

( f is decreasing_on_1st & f is increasing_on_2nd & f is 00-dominant & f is 11-dominant & f is 10-weak );

attr f is with_properties_of_classical_implication means :: FUZIMPL1:def 8

( f is 00-dominant & f is 01-dominant & f is 11-dominant & f is 10-weak );

( f is 00-dominant & f is 01-dominant & f is 11-dominant & f is 10-weak );

:: deftheorem defines with_properties_of_fuzzy_implication FUZIMPL1:def 7 :

for f being BinOp of [.0,1.] holds

( f is with_properties_of_fuzzy_implication iff ( f is decreasing_on_1st & f is increasing_on_2nd & f is 00-dominant & f is 11-dominant & f is 10-weak ) );

for f being BinOp of [.0,1.] holds

( f is with_properties_of_fuzzy_implication iff ( f is decreasing_on_1st & f is increasing_on_2nd & f is 00-dominant & f is 11-dominant & f is 10-weak ) );

:: deftheorem defines with_properties_of_classical_implication FUZIMPL1:def 8 :

for f being BinOp of [.0,1.] holds

( f is with_properties_of_classical_implication iff ( f is 00-dominant & f is 01-dominant & f is 11-dominant & f is 10-weak ) );

for f being BinOp of [.0,1.] holds

( f is with_properties_of_classical_implication iff ( f is 00-dominant & f is 01-dominant & f is 11-dominant & f is 10-weak ) );

definition

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

for x, y being Element of [.0,1.] holds b_{1} . (x,y) = max ((1 - x),(min (x,y)))

for b_{1}, b_{2} being BinOp of [.0,1.] st ( for x, y being Element of [.0,1.] holds b_{1} . (x,y) = max ((1 - x),(min (x,y))) ) & ( for x, y being Element of [.0,1.] holds b_{2} . (x,y) = max ((1 - x),(min (x,y))) ) holds

b_{1} = b_{2}
end;

func I_{-1} -> BinOp of [.0,1.] means :I1Def: :: FUZIMPL1:def 9

for x, y being Element of [.0,1.] holds it . (x,y) = max ((1 - x),(min (x,y)));

existence for x, y being Element of [.0,1.] holds it . (x,y) = max ((1 - x),(min (x,y)));

ex b

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

proof end;

uniqueness for b

b

proof end;

:: deftheorem I1Def defines I_{-1} FUZIMPL1:def 9 :

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

( b_{1} = I_{-1} iff for x, y being Element of [.0,1.] holds b_{1} . (x,y) = max ((1 - x),(min (x,y))) );

for b

( b

registration

coherence

( I_{-1} is increasing_on_2nd & I_{-1} is 00-dominant & I_{-1} is 11-dominant & I_{-1} is 10-weak )

end;
( I_{-1} is increasing_on_2nd & I_{-1} is 00-dominant & I_{-1} is 11-dominant & I_{-1} is 10-weak )

proof end;

definition

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

for x, y being Element of [.0,1.] holds b_{1} . (x,y) = max (y,(min ((1 - x),(1 - y))))

for b_{1}, b_{2} being BinOp of [.0,1.] st ( for x, y being Element of [.0,1.] holds b_{1} . (x,y) = max (y,(min ((1 - x),(1 - y)))) ) & ( for x, y being Element of [.0,1.] holds b_{2} . (x,y) = max (y,(min ((1 - x),(1 - y)))) ) holds

b_{1} = b_{2}
end;

func I_{-2} -> BinOp of [.0,1.] means :I2Def: :: FUZIMPL1:def 10

for x, y being Element of [.0,1.] holds it . (x,y) = max (y,(min ((1 - x),(1 - y))));

existence for x, y being Element of [.0,1.] holds it . (x,y) = max (y,(min ((1 - x),(1 - y))));

ex b

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

proof end;

uniqueness for b

b

proof end;

:: deftheorem I2Def defines I_{-2} FUZIMPL1:def 10 :

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

( b_{1} = I_{-2} iff for x, y being Element of [.0,1.] holds b_{1} . (x,y) = max (y,(min ((1 - x),(1 - y)))) );

for b

( b

registration

coherence

( I_{-2} is decreasing_on_1st & I_{-2} is 00-dominant & I_{-2} is 11-dominant & I_{-2} is 10-weak )

end;
( I_{-2} is decreasing_on_1st & I_{-2} is 00-dominant & I_{-2} is 11-dominant & I_{-2} is 10-weak )

proof end;

definition

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

for x, y being Element of [.0,1.] holds

( ( y < 1 implies b_{1} . (x,y) = 0 ) & ( y = 1 implies b_{1} . (x,y) = 1 ) )

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

( ( y < 1 implies b_{1} . (x,y) = 0 ) & ( y = 1 implies b_{1} . (x,y) = 1 ) ) ) & ( for x, y being Element of [.0,1.] holds

( ( y < 1 implies b_{2} . (x,y) = 0 ) & ( y = 1 implies b_{2} . (x,y) = 1 ) ) ) holds

b_{1} = b_{2}
end;

func I_{-3} -> BinOp of [.0,1.] means :I3Def: :: FUZIMPL1:def 11

for x, y being Element of [.0,1.] holds

( ( y < 1 implies it . (x,y) = 0 ) & ( y = 1 implies it . (x,y) = 1 ) );

existence for x, y being Element of [.0,1.] holds

( ( y < 1 implies it . (x,y) = 0 ) & ( y = 1 implies it . (x,y) = 1 ) );

ex b

for x, y being Element of [.0,1.] holds

( ( y < 1 implies b

proof end;

uniqueness for b

( ( y < 1 implies b

( ( y < 1 implies b

b

proof end;

:: deftheorem I3Def defines I_{-3} FUZIMPL1:def 11 :

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

( b_{1} = I_{-3} iff for x, y being Element of [.0,1.] holds

( ( y < 1 implies b_{1} . (x,y) = 0 ) & ( y = 1 implies b_{1} . (x,y) = 1 ) ) );

for b

( b

( ( y < 1 implies b

registration

coherence

( I_{-3} is decreasing_on_1st & I_{-3} is increasing_on_2nd & not I_{-3} is 00-dominant & I_{-3} is 11-dominant & I_{-3} is 10-weak )

end;
( I_{-3} is decreasing_on_1st & I_{-3} is increasing_on_2nd & not I_{-3} is 00-dominant & I_{-3} is 11-dominant & I_{-3} is 10-weak )

proof end;

definition

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

for x, y being Element of [.0,1.] holds

( ( x = 0 implies b_{1} . (x,y) = 1 ) & ( x > 0 implies b_{1} . (x,y) = 0 ) )

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

( ( x = 0 implies b_{1} . (x,y) = 1 ) & ( x > 0 implies b_{1} . (x,y) = 0 ) ) ) & ( for x, y being Element of [.0,1.] holds

( ( x = 0 implies b_{2} . (x,y) = 1 ) & ( x > 0 implies b_{2} . (x,y) = 0 ) ) ) holds

b_{1} = b_{2}
end;

func I_{-4} -> BinOp of [.0,1.] means :I4Def: :: FUZIMPL1:def 12

for x, y being Element of [.0,1.] holds

( ( x = 0 implies it . (x,y) = 1 ) & ( x > 0 implies it . (x,y) = 0 ) );

existence for x, y being Element of [.0,1.] holds

( ( x = 0 implies it . (x,y) = 1 ) & ( x > 0 implies it . (x,y) = 0 ) );

ex b

for x, y being Element of [.0,1.] holds

( ( x = 0 implies b

proof end;

uniqueness for b

( ( x = 0 implies b

( ( x = 0 implies b

b

proof end;

:: deftheorem I4Def defines I_{-4} FUZIMPL1:def 12 :

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

( b_{1} = I_{-4} iff for x, y being Element of [.0,1.] holds

( ( x = 0 implies b_{1} . (x,y) = 1 ) & ( x > 0 implies b_{1} . (x,y) = 0 ) ) );

for b

( b

( ( x = 0 implies b

registration

coherence

( I_{-4} is decreasing_on_1st & I_{-4} is increasing_on_2nd & I_{-4} is 00-dominant & not I_{-4} is 11-dominant & I_{-4} is 10-weak )

end;
( I_{-4} is decreasing_on_1st & I_{-4} is increasing_on_2nd & I_{-4} is 00-dominant & not I_{-4} is 11-dominant & I_{-4} is 10-weak )

proof end;

definition

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

for x, y being Element of [.0,1.] holds b_{1} . (x,y) = 1

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

b_{1} = b_{2}
end;

func I_{-5} -> BinOp of [.0,1.] means :I5Def: :: FUZIMPL1:def 13

for x, y being Element of [.0,1.] holds it . (x,y) = 1;

existence for x, y being Element of [.0,1.] holds it . (x,y) = 1;

ex b

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

proof end;

uniqueness for b

b

proof end;

:: deftheorem I5Def defines I_{-5} FUZIMPL1:def 13 :

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

( b_{1} = I_{-5} iff for x, y being Element of [.0,1.] holds b_{1} . (x,y) = 1 );

for b

( b

registration

coherence

( I_{-5} is decreasing_on_1st & I_{-5} is increasing_on_2nd & I_{-5} is 00-dominant & I_{-5} is 11-dominant & not I_{-5} is 10-weak )

end;
( I_{-5} is decreasing_on_1st & I_{-5} is increasing_on_2nd & I_{-5} is 00-dominant & I_{-5} is 11-dominant & not I_{-5} is 10-weak )

proof end;

definition

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

for x, y being Element of [.0,1.] holds b_{1} . (x,y) = min (1,((1 - x) + y))

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

b_{1} = b_{2}
end;

func Lukasiewicz_implication -> BinOp of [.0,1.] means :Luk: :: FUZIMPL1:def 14

for x, y being Element of [.0,1.] holds it . (x,y) = min (1,((1 - x) + y));

existence for x, y being Element of [.0,1.] holds it . (x,y) = min (1,((1 - x) + y));

ex b

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

proof end;

uniqueness for b

b

proof end;

:: deftheorem Luk defines Lukasiewicz_implication FUZIMPL1:def 14 :

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

( b_{1} = Lukasiewicz_implication iff for x, y being Element of [.0,1.] holds b_{1} . (x,y) = min (1,((1 - x) + y)) );

for b

( b

registration

( Lukasiewicz_implication is decreasing_on_1st & Lukasiewicz_implication is increasing_on_2nd & Lukasiewicz_implication is 00-dominant & Lukasiewicz_implication is 11-dominant & Lukasiewicz_implication is 10-weak )
end;

cluster Lukasiewicz_implication -> decreasing_on_1st increasing_on_2nd 00-dominant 11-dominant 10-weak ;

coherence ( Lukasiewicz_implication is decreasing_on_1st & Lukasiewicz_implication is increasing_on_2nd & Lukasiewicz_implication is 00-dominant & Lukasiewicz_implication is 11-dominant & Lukasiewicz_implication is 10-weak )

proof end;

registration

ex b_{1} being BinOp of [.0,1.] st b_{1} is with_properties_of_fuzzy_implication
end;

cluster V1() V4([:[.0,1.],[.0,1.]:]) V5([.0,1.]) Function-like V29([:[.0,1.],[.0,1.]:],[.0,1.]) with_properties_of_fuzzy_implication for BinOp of ;

existence ex b

proof end;

registration

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

( b_{1} is decreasing_on_1st & b_{1} is increasing_on_2nd & b_{1} is 00-dominant & b_{1} is 11-dominant & b_{1} is 10-weak )
;

for b_{1} being BinOp of [.0,1.] st b_{1} is decreasing_on_1st & b_{1} is increasing_on_2nd & b_{1} is 00-dominant & b_{1} is 01-dominant & b_{1} is 11-dominant & b_{1} is 10-weak holds

b_{1} is with_properties_of_fuzzy_implication
;

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

( b_{1} is 00-dominant & b_{1} is 01-dominant & b_{1} is 11-dominant & b_{1} is 10-weak )
;

for b_{1} being BinOp of [.0,1.] st b_{1} is 00-dominant & b_{1} is 01-dominant & b_{1} is 11-dominant & b_{1} is 10-weak holds

b_{1} is with_properties_of_classical_implication
;

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

b_{1} is with_properties_of_classical_implication
end;

cluster Function-like V29([:[.0,1.],[.0,1.]:],[.0,1.]) with_properties_of_fuzzy_implication -> decreasing_on_1st increasing_on_2nd 00-dominant 11-dominant 10-weak for BinOp of ;

coherence for b

( b

cluster Function-like V29([:[.0,1.],[.0,1.]:],[.0,1.]) decreasing_on_1st increasing_on_2nd 00-dominant 11-dominant 10-weak 01-dominant -> with_properties_of_fuzzy_implication for BinOp of ;

coherence for b

b

cluster Function-like V29([:[.0,1.],[.0,1.]:],[.0,1.]) with_properties_of_classical_implication -> 00-dominant 11-dominant 10-weak 01-dominant for BinOp of ;

coherence for b

( b

cluster Function-like V29([:[.0,1.],[.0,1.]:],[.0,1.]) 00-dominant 11-dominant 10-weak 01-dominant -> with_properties_of_classical_implication for BinOp of ;

coherence for b

b

cluster Function-like V29([:[.0,1.],[.0,1.]:],[.0,1.]) with_properties_of_fuzzy_implication -> with_properties_of_classical_implication for BinOp of ;

coherence for b

b

proof end;

definition

mode Fuzzy_Implication is decreasing_on_1st increasing_on_2nd 00-dominant 11-dominant 10-weak BinOp of [.0,1.];

end;
definition

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

for x, y being Element of [.0,1.] holds

( ( x <= y implies b_{1} . (x,y) = 1 ) & ( x > y implies b_{1} . (x,y) = y ) )

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

( ( x <= y implies b_{1} . (x,y) = 1 ) & ( x > y implies b_{1} . (x,y) = y ) ) ) & ( for x, y being Element of [.0,1.] holds

( ( x <= y implies b_{2} . (x,y) = 1 ) & ( x > y implies b_{2} . (x,y) = y ) ) ) holds

b_{1} = b_{2}
end;

func Goedel_implication -> BinOp of [.0,1.] means :Goedel: :: FUZIMPL1:def 16

for x, y being Element of [.0,1.] holds

( ( x <= y implies it . (x,y) = 1 ) & ( x > y implies it . (x,y) = y ) );

existence for x, y being Element of [.0,1.] holds

( ( x <= y implies it . (x,y) = 1 ) & ( x > y implies it . (x,y) = y ) );

ex b

for x, y being Element of [.0,1.] holds

( ( x <= y implies b

proof end;

uniqueness for b

( ( x <= y implies b

( ( x <= y implies b

b

proof end;

:: deftheorem Goedel defines Goedel_implication FUZIMPL1:def 16 :

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

( b_{1} = Goedel_implication iff for x, y being Element of [.0,1.] holds

( ( x <= y implies b_{1} . (x,y) = 1 ) & ( x > y implies b_{1} . (x,y) = y ) ) );

for b

( b

( ( x <= y implies b

registration

coherence

( Goedel_implication is decreasing_on_1st & Goedel_implication is increasing_on_2nd & Goedel_implication is 00-dominant & Goedel_implication is 11-dominant & Goedel_implication is 10-weak )

end;
( Goedel_implication is decreasing_on_1st & Goedel_implication is increasing_on_2nd & Goedel_implication is 00-dominant & Goedel_implication is 11-dominant & Goedel_implication is 10-weak )

proof end;

definition

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

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

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

b_{1} = b_{2}
end;

func Reichenbach_implication -> BinOp of [.0,1.] means :Reichen: :: FUZIMPL1:def 17

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

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

ex b

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

proof end;

uniqueness for b

b

proof end;

:: deftheorem Reichen defines Reichenbach_implication FUZIMPL1:def 17 :

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

( b_{1} = Reichenbach_implication iff for x, y being Element of [.0,1.] holds b_{1} . (x,y) = (1 - x) + (x * y) );

for b

( b

registration

( Reichenbach_implication is decreasing_on_1st & Reichenbach_implication is increasing_on_2nd & Reichenbach_implication is 00-dominant & Reichenbach_implication is 11-dominant & Reichenbach_implication is 10-weak )
end;

cluster Reichenbach_implication -> decreasing_on_1st increasing_on_2nd 00-dominant 11-dominant 10-weak ;

coherence ( Reichenbach_implication is decreasing_on_1st & Reichenbach_implication is increasing_on_2nd & Reichenbach_implication is 00-dominant & Reichenbach_implication is 11-dominant & Reichenbach_implication is 10-weak )

proof end;

definition

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

for x, y being Element of [.0,1.] holds b_{1} . (x,y) = max ((1 - x),y)

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

b_{1} = b_{2}
end;

func Kleene-Dienes_implication -> BinOp of [.0,1.] means :Kleene: :: FUZIMPL1:def 18

for x, y being Element of [.0,1.] holds it . (x,y) = max ((1 - x),y);

existence for x, y being Element of [.0,1.] holds it . (x,y) = max ((1 - x),y);

ex b

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

proof end;

uniqueness for b

b

proof end;

:: deftheorem Kleene defines Kleene-Dienes_implication FUZIMPL1:def 18 :

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

( b_{1} = Kleene-Dienes_implication iff for x, y being Element of [.0,1.] holds b_{1} . (x,y) = max ((1 - x),y) );

for b

( b

registration

( Kleene-Dienes_implication is decreasing_on_1st & Kleene-Dienes_implication is increasing_on_2nd & Kleene-Dienes_implication is 00-dominant & Kleene-Dienes_implication is 11-dominant & Kleene-Dienes_implication is 10-weak )
end;

cluster Kleene-Dienes_implication -> decreasing_on_1st increasing_on_2nd 00-dominant 11-dominant 10-weak ;

coherence ( Kleene-Dienes_implication is decreasing_on_1st & Kleene-Dienes_implication is increasing_on_2nd & Kleene-Dienes_implication is 00-dominant & Kleene-Dienes_implication is 11-dominant & Kleene-Dienes_implication is 10-weak )

proof end;

definition

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

for x, y being Element of [.0,1.] holds

( ( x <= y implies b_{1} . (x,y) = 1 ) & ( x > y implies b_{1} . (x,y) = y / x ) )

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

( ( x <= y implies b_{1} . (x,y) = 1 ) & ( x > y implies b_{1} . (x,y) = y / x ) ) ) & ( for x, y being Element of [.0,1.] holds

( ( x <= y implies b_{2} . (x,y) = 1 ) & ( x > y implies b_{2} . (x,y) = y / x ) ) ) holds

b_{1} = b_{2}
end;

func Goguen_implication -> BinOp of [.0,1.] means :Goguen: :: FUZIMPL1:def 19

for x, y being Element of [.0,1.] holds

( ( x <= y implies it . (x,y) = 1 ) & ( x > y implies it . (x,y) = y / x ) );

existence for x, y being Element of [.0,1.] holds

( ( x <= y implies it . (x,y) = 1 ) & ( x > y implies it . (x,y) = y / x ) );

ex b

for x, y being Element of [.0,1.] holds

( ( x <= y implies b

proof end;

uniqueness for b

( ( x <= y implies b

( ( x <= y implies b

b

proof end;

:: deftheorem Goguen defines Goguen_implication FUZIMPL1:def 19 :

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

( b_{1} = Goguen_implication iff for x, y being Element of [.0,1.] holds

( ( x <= y implies b_{1} . (x,y) = 1 ) & ( x > y implies b_{1} . (x,y) = y / x ) ) );

for b

( b

( ( x <= y implies b

registration

coherence

( Goguen_implication is decreasing_on_1st & Goguen_implication is increasing_on_2nd & Goguen_implication is 00-dominant & Goguen_implication is 11-dominant & Goguen_implication is 10-weak )

end;
( Goguen_implication is decreasing_on_1st & Goguen_implication is increasing_on_2nd & Goguen_implication is 00-dominant & Goguen_implication is 11-dominant & Goguen_implication is 10-weak )

proof end;

definition

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

for x, y being Element of [.0,1.] holds

( ( x <= y implies b_{1} . (x,y) = 1 ) & ( x > y implies b_{1} . (x,y) = 0 ) )

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

( ( x <= y implies b_{1} . (x,y) = 1 ) & ( x > y implies b_{1} . (x,y) = 0 ) ) ) & ( for x, y being Element of [.0,1.] holds

( ( x <= y implies b_{2} . (x,y) = 1 ) & ( x > y implies b_{2} . (x,y) = 0 ) ) ) holds

b_{1} = b_{2}
end;

func Rescher_implication -> BinOp of [.0,1.] means :Rescher: :: FUZIMPL1:def 20

for x, y being Element of [.0,1.] holds

( ( x <= y implies it . (x,y) = 1 ) & ( x > y implies it . (x,y) = 0 ) );

existence for x, y being Element of [.0,1.] holds

( ( x <= y implies it . (x,y) = 1 ) & ( x > y implies it . (x,y) = 0 ) );

ex b

for x, y being Element of [.0,1.] holds

( ( x <= y implies b

proof end;

uniqueness for b

( ( x <= y implies b

( ( x <= y implies b

b

proof end;

:: deftheorem Rescher defines Rescher_implication FUZIMPL1:def 20 :

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

( b_{1} = Rescher_implication iff for x, y being Element of [.0,1.] holds

( ( x <= y implies b_{1} . (x,y) = 1 ) & ( x > y implies b_{1} . (x,y) = 0 ) ) );

for b

( b

( ( x <= y implies b

registration

( Rescher_implication is decreasing_on_1st & Rescher_implication is increasing_on_2nd & Rescher_implication is 00-dominant & Rescher_implication is 11-dominant & Rescher_implication is 10-weak )
end;

cluster Rescher_implication -> decreasing_on_1st increasing_on_2nd 00-dominant 11-dominant 10-weak ;

coherence ( Rescher_implication is decreasing_on_1st & Rescher_implication is increasing_on_2nd & Rescher_implication is 00-dominant & Rescher_implication is 11-dominant & Rescher_implication is 10-weak )

proof end;

definition

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

for x, y being Element of [.0,1.] holds

( ( x = y & y = 0 implies b_{1} . (x,y) = 1 ) & ( ( x > 0 or y > 0 ) implies b_{1} . (x,y) = y to_power x ) )

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

( ( x = y & y = 0 implies b_{1} . (x,y) = 1 ) & ( ( x > 0 or y > 0 ) implies b_{1} . (x,y) = y to_power x ) ) ) & ( for x, y being Element of [.0,1.] holds

( ( x = y & y = 0 implies b_{2} . (x,y) = 1 ) & ( ( x > 0 or y > 0 ) implies b_{2} . (x,y) = y to_power x ) ) ) holds

b_{1} = b_{2}
end;

func Yager_implication -> BinOp of [.0,1.] means :Yager: :: FUZIMPL1:def 21

for x, y being Element of [.0,1.] holds

( ( x = y & y = 0 implies it . (x,y) = 1 ) & ( ( x > 0 or y > 0 ) implies it . (x,y) = y to_power x ) );

existence for x, y being Element of [.0,1.] holds

( ( x = y & y = 0 implies it . (x,y) = 1 ) & ( ( x > 0 or y > 0 ) implies it . (x,y) = y to_power x ) );

ex b

for x, y being Element of [.0,1.] holds

( ( x = y & y = 0 implies b

proof end;

uniqueness for b

( ( x = y & y = 0 implies b

( ( x = y & y = 0 implies b

b

proof end;

:: deftheorem Yager defines Yager_implication FUZIMPL1:def 21 :

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

( b_{1} = Yager_implication iff for x, y being Element of [.0,1.] holds

( ( x = y & y = 0 implies b_{1} . (x,y) = 1 ) & ( ( x > 0 or y > 0 ) implies b_{1} . (x,y) = y to_power x ) ) );

for b

( b

( ( x = y & y = 0 implies b

registration

coherence

( Yager_implication is decreasing_on_1st & Yager_implication is increasing_on_2nd & Yager_implication is 00-dominant & Yager_implication is 11-dominant & Yager_implication is 10-weak )

end;
( Yager_implication is decreasing_on_1st & Yager_implication is increasing_on_2nd & Yager_implication is 00-dominant & Yager_implication is 11-dominant & Yager_implication is 10-weak )

proof end;

definition

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

for x, y being Element of [.0,1.] holds

( ( x < 1 implies b_{1} . (x,y) = 1 ) & ( x = 1 implies b_{1} . (x,y) = y ) )

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

( ( x < 1 implies b_{1} . (x,y) = 1 ) & ( x = 1 implies b_{1} . (x,y) = y ) ) ) & ( for x, y being Element of [.0,1.] holds

( ( x < 1 implies b_{2} . (x,y) = 1 ) & ( x = 1 implies b_{2} . (x,y) = y ) ) ) holds

b_{1} = b_{2}
end;

func Weber_implication -> BinOp of [.0,1.] means :Weber: :: FUZIMPL1:def 22

for x, y being Element of [.0,1.] holds

( ( x < 1 implies it . (x,y) = 1 ) & ( x = 1 implies it . (x,y) = y ) );

existence for x, y being Element of [.0,1.] holds

( ( x < 1 implies it . (x,y) = 1 ) & ( x = 1 implies it . (x,y) = y ) );

ex b

for x, y being Element of [.0,1.] holds

( ( x < 1 implies b

proof end;

uniqueness for b

( ( x < 1 implies b

( ( x < 1 implies b

b

proof end;

:: deftheorem Weber defines Weber_implication FUZIMPL1:def 22 :

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

( b_{1} = Weber_implication iff for x, y being Element of [.0,1.] holds

( ( x < 1 implies b_{1} . (x,y) = 1 ) & ( x = 1 implies b_{1} . (x,y) = y ) ) );

for b

( b

( ( x < 1 implies b

registration

coherence

( Weber_implication is decreasing_on_1st & Weber_implication is increasing_on_2nd & Weber_implication is 00-dominant & Weber_implication is 11-dominant & Weber_implication is 10-weak )

end;
( Weber_implication is decreasing_on_1st & Weber_implication is increasing_on_2nd & Weber_implication is 00-dominant & Weber_implication is 11-dominant & Weber_implication is 10-weak )

proof end;

definition

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

for x, y being Element of [.0,1.] holds

( ( x <= y implies b_{1} . (x,y) = 1 ) & ( x > y implies b_{1} . (x,y) = max ((1 - x),y) ) )

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

( ( x <= y implies b_{1} . (x,y) = 1 ) & ( x > y implies b_{1} . (x,y) = max ((1 - x),y) ) ) ) & ( for x, y being Element of [.0,1.] holds

( ( x <= y implies b_{2} . (x,y) = 1 ) & ( x > y implies b_{2} . (x,y) = max ((1 - x),y) ) ) ) holds

b_{1} = b_{2}
end;

func Fodor_implication -> BinOp of [.0,1.] means :Fodor: :: FUZIMPL1:def 23

for x, y being Element of [.0,1.] holds

( ( x <= y implies it . (x,y) = 1 ) & ( x > y implies it . (x,y) = max ((1 - x),y) ) );

existence for x, y being Element of [.0,1.] holds

( ( x <= y implies it . (x,y) = 1 ) & ( x > y implies it . (x,y) = max ((1 - x),y) ) );

ex b

for x, y being Element of [.0,1.] holds

( ( x <= y implies b

proof end;

uniqueness for b

( ( x <= y implies b

( ( x <= y implies b

b

proof end;

:: deftheorem Fodor defines Fodor_implication FUZIMPL1:def 23 :

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

( b_{1} = Fodor_implication iff for x, y being Element of [.0,1.] holds

( ( x <= y implies b_{1} . (x,y) = 1 ) & ( x > y implies b_{1} . (x,y) = max ((1 - x),y) ) ) );

for b

( b

( ( x <= y implies b

registration

coherence

( Fodor_implication is decreasing_on_1st & Fodor_implication is increasing_on_2nd & Fodor_implication is 00-dominant & Fodor_implication is 11-dominant & Fodor_implication is 10-weak )

end;
( Fodor_implication is decreasing_on_1st & Fodor_implication is increasing_on_2nd & Fodor_implication is 00-dominant & Fodor_implication is 11-dominant & Fodor_implication is 10-weak )

proof end;

definition

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

for x, y being Element of [.0,1.] holds

( ( ( x = 0 or y = 1 ) implies b_{1} . (x,y) = 1 ) & ( x > 0 & y < 1 implies b_{1} . (x,y) = 0 ) )

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

( ( ( x = 0 or y = 1 ) implies b_{1} . (x,y) = 1 ) & ( x > 0 & y < 1 implies b_{1} . (x,y) = 0 ) ) ) & ( for x, y being Element of [.0,1.] holds

( ( ( x = 0 or y = 1 ) implies b_{2} . (x,y) = 1 ) & ( x > 0 & y < 1 implies b_{2} . (x,y) = 0 ) ) ) holds

b_{1} = b_{2}
end;

func I_{0} -> BinOp of [.0,1.] means :I0Impl: :: FUZIMPL1:def 24

for x, y being Element of [.0,1.] holds

( ( ( x = 0 or y = 1 ) implies it . (x,y) = 1 ) & ( x > 0 & y < 1 implies it . (x,y) = 0 ) );

existence for x, y being Element of [.0,1.] holds

( ( ( x = 0 or y = 1 ) implies it . (x,y) = 1 ) & ( x > 0 & y < 1 implies it . (x,y) = 0 ) );

ex b

for x, y being Element of [.0,1.] holds

( ( ( x = 0 or y = 1 ) implies b

proof end;

uniqueness for b

( ( ( x = 0 or y = 1 ) implies b

( ( ( x = 0 or y = 1 ) implies b

b

proof end;

:: deftheorem I0Impl defines I_{0} FUZIMPL1:def 24 :

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

( b_{1} = I_{0} iff for x, y being Element of [.0,1.] holds

( ( ( x = 0 or y = 1 ) implies b_{1} . (x,y) = 1 ) & ( x > 0 & y < 1 implies b_{1} . (x,y) = 0 ) ) );

for b

( b

( ( ( x = 0 or y = 1 ) implies b

registration

coherence

( I_{0} is decreasing_on_1st & I_{0} is increasing_on_2nd & I_{0} is 00-dominant & I_{0} is 11-dominant & I_{0} is 10-weak )

end;
( I_{0} is decreasing_on_1st & I_{0} is increasing_on_2nd & I_{0} is 00-dominant & I_{0} is 11-dominant & I_{0} is 10-weak )

proof end;

definition

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

for x, y being Element of [.0,1.] holds

( ( ( x < 1 or y > 0 ) implies b_{1} . (x,y) = 1 ) & ( x = 1 & y = 0 implies b_{1} . (x,y) = 0 ) )

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

( ( ( x < 1 or y > 0 ) implies b_{1} . (x,y) = 1 ) & ( x = 1 & y = 0 implies b_{1} . (x,y) = 0 ) ) ) & ( for x, y being Element of [.0,1.] holds

( ( ( x < 1 or y > 0 ) implies b_{2} . (x,y) = 1 ) & ( x = 1 & y = 0 implies b_{2} . (x,y) = 0 ) ) ) holds

b_{1} = b_{2}
end;

func I_{1} -> BinOp of [.0,1.] means :I1Impl: :: FUZIMPL1:def 25

for x, y being Element of [.0,1.] holds

( ( ( x < 1 or y > 0 ) implies it . (x,y) = 1 ) & ( x = 1 & y = 0 implies it . (x,y) = 0 ) );

existence for x, y being Element of [.0,1.] holds

( ( ( x < 1 or y > 0 ) implies it . (x,y) = 1 ) & ( x = 1 & y = 0 implies it . (x,y) = 0 ) );

ex b

for x, y being Element of [.0,1.] holds

( ( ( x < 1 or y > 0 ) implies b

proof end;

uniqueness for b

( ( ( x < 1 or y > 0 ) implies b

( ( ( x < 1 or y > 0 ) implies b

b

proof end;

:: deftheorem I1Impl defines I_{1} FUZIMPL1:def 25 :

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

( b_{1} = I_{1} iff for x, y being Element of [.0,1.] holds

( ( ( x < 1 or y > 0 ) implies b_{1} . (x,y) = 1 ) & ( x = 1 & y = 0 implies b_{1} . (x,y) = 0 ) ) );

for b

( b

( ( ( x < 1 or y > 0 ) implies b

registration

coherence

( I_{1} is decreasing_on_1st & I_{1} is increasing_on_2nd & I_{1} is 00-dominant & I_{1} is 11-dominant & I_{1} is 10-weak )

end;
( I_{1} is decreasing_on_1st & I_{1} is increasing_on_2nd & I_{1} is 00-dominant & I_{1} is 11-dominant & I_{1} is 10-weak )

proof end;

definition

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

end;
attr f is satisfying_(LB) means :: FUZIMPL1:def 26

for y being Element of [.0,1.] holds f . (0,y) = 1;

for y being Element of [.0,1.] holds f . (0,y) = 1;

attr f is satisfying_(RB) means :: FUZIMPL1:def 27

for x being Element of [.0,1.] holds f . (x,1) = 1;

for x being Element of [.0,1.] holds f . (x,1) = 1;

:: deftheorem defines satisfying_(LB) FUZIMPL1:def 26 :

for f being BinOp of [.0,1.] holds

( f is satisfying_(LB) iff for y being Element of [.0,1.] holds f . (0,y) = 1 );

for f being BinOp of [.0,1.] holds

( f is satisfying_(LB) iff for y being Element of [.0,1.] holds f . (0,y) = 1 );

:: deftheorem defines satisfying_(RB) FUZIMPL1:def 27 :

for f being BinOp of [.0,1.] holds

( f is satisfying_(RB) iff for x being Element of [.0,1.] holds f . (x,1) = 1 );

for f being BinOp of [.0,1.] holds

( f is satisfying_(RB) iff for x being Element of [.0,1.] holds f . (x,1) = 1 );

registration

for b_{1} being Fuzzy_Implication holds

( b_{1} is satisfying_(LB) & b_{1} is satisfying_(RB) )
by LBProp, RBProp;

end;

cluster Function-like V29([:[.0,1.],[.0,1.]:],[.0,1.]) decreasing_on_1st increasing_on_2nd 00-dominant 11-dominant 10-weak -> satisfying_(LB) satisfying_(RB) for Fuzzy_Implication;

coherence for b

( b