:: Fundamental Properties of Fuzzy Implications
::
:: Copyright (c) 2018-2021 Association of Mizar Users

notation end;

Lemma00: for x, y being Element of [.0,1.] holds (x * y) + ((1 - x) * 1) in [.y,1.]
proof end;

LemmaHalf: (1 / 2) to_power (1 / 2) <> 1
proof end;

theorem :: FUZIMPL2:1
#R 1 = (AffineMap (1,0)) |
proof end;

theorem LemmaAffine: :: FUZIMPL2:2
for a, b being Real holds
( AffineMap (a,b) is_differentiable_on REAL & ( for x being Real holds diff ((AffineMap (a,b)),x) = a ) )
proof end;

theorem :: FUZIMPL2:3
for x, y being Element of [.0,1.] st 0 < x & x < 1 & 0 < y & y < 1 holds
((#R x) + (AffineMap ((- x),(x - 1)))) | ].0,1.[ is increasing
proof end;

theorem :: FUZIMPL2:4
for x being Element of [.0,1.]
for u being Real st u in ].0,1.] holds
((#R x) + (AffineMap ((- x),(x - 1)))) . u = (((u to_power x) - 1) + x) - (x * u)
proof end;

theorem Lemma01: :: FUZIMPL2:5
for x, y being Element of [.0,1.] holds
( ( x <= y implies I_LK . (x,y) = 1 ) & ( x > y implies I_LK . (x,y) = (1 - x) + y ) )
proof end;

theorem :: FUZIMPL2:6
for x, y being Element of [.0,1.] holds
( ( x = 0 implies I_GG . (x,y) = 1 ) & ( x > 0 implies I_GG . (x,y) = min (1,(y / x)) ) )
proof end;

Lemma03: for x, y being Element of [.0,1.] holds max ((1 - x),y) in [.0,1.]
proof end;

Lemma11: for x, y being Element of [.0,1.] st x <> 0 holds
y <= y / x

proof end;

Lemacik1: for x, y being Element of [.0,1.] st x > y holds
(1 - x) + y >= y / x

proof end;

Lemma111:
proof end;

Lemma112:
proof end;

Lemma113:
proof end;

theorem :: FUZIMPL2:7

Lemma121:
proof end;

Lemma122:
proof end;

Lemma123:
proof end;

theorem :: FUZIMPL2:8

Lemma132:
proof end;

theorem :: FUZIMPL2:9

Lemma141:
proof end;

Lemma142:
proof end;

theorem :: FUZIMPL2:10

Lemma151:
proof end;

Lemma152:
proof end;

Lemma153:
proof end;

theorem :: FUZIMPL2:11

definition
let I be BinOp of [.0,1.];
attr I is satisfying_(NP) means :: FUZIMPL2:def 1
for y being Element of [.0,1.] holds I . (1,y) = y;
attr I is satisfying_(EP) means :: FUZIMPL2:def 2
for x, y, z being Element of [.0,1.] holds I . (x,(I . (y,z))) = I . (y,(I . (x,z)));
attr I is satisfying_(IP) means :: FUZIMPL2:def 3
for x being Element of [.0,1.] holds I . (x,x) = 1;
attr I is satisfying_(OP) means :: FUZIMPL2:def 4
for x, y being Element of [.0,1.] holds
( I . (x,y) = 1 iff x <= y );
end;

:: deftheorem defines satisfying_(NP) FUZIMPL2:def 1 :
for I being BinOp of [.0,1.] holds
( I is satisfying_(NP) iff for y being Element of [.0,1.] holds I . (1,y) = y );

:: deftheorem defines satisfying_(EP) FUZIMPL2:def 2 :
for I being BinOp of [.0,1.] holds
( I is satisfying_(EP) iff for x, y, z being Element of [.0,1.] holds I . (x,(I . (y,z))) = I . (y,(I . (x,z))) );

:: deftheorem defines satisfying_(IP) FUZIMPL2:def 3 :
for I being BinOp of [.0,1.] holds
( I is satisfying_(IP) iff for x being Element of [.0,1.] holds I . (x,x) = 1 );

:: deftheorem defines satisfying_(OP) FUZIMPL2:def 4 :
for I being BinOp of [.0,1.] holds
( I is satisfying_(OP) iff for x, y being Element of [.0,1.] holds
( I . (x,y) = 1 iff x <= y ) );

notation end;

theorem LemmaXA: :: FUZIMPL2:12
for I being BinOp of [.0,1.] st I is satisfying_(LB) holds
( I is satisfying_(I3) & I is satisfying_(NC) )
proof end;

registration
cluster Function-like V29(K17([.0,1.],[.0,1.]),[.0,1.]) satisfying_(LB) -> satisfying_(I3) satisfying_(NC) for Element of K16(K17(K17([.0,1.],[.0,1.]),[.0,1.]));
coherence
for b1 being BinOp of [.0,1.] st b1 is satisfying_(LB) holds
( b1 is satisfying_(I3) & b1 is satisfying_(NC) )
by LemmaXA;
end;

theorem LemmaVA: :: FUZIMPL2:13
for I being BinOp of [.0,1.] st I is satisfying_(RB) holds
( I is satisfying_(I4) & I is satisfying_(NC) )
proof end;

registration
cluster Function-like V29(K17([.0,1.],[.0,1.]),[.0,1.]) satisfying_(RB) -> satisfying_(I4) satisfying_(NC) for Element of K16(K17(K17([.0,1.],[.0,1.]),[.0,1.]));
coherence
for b1 being BinOp of [.0,1.] st b1 is satisfying_(RB) holds
( b1 is satisfying_(I4) & b1 is satisfying_(NC) )
by LemmaVA;
end;

theorem LemmaWA: :: FUZIMPL2:14
for I being BinOp of [.0,1.] st I is satisfying_(NP) holds
( I is satisfying_(I4) & I is satisfying_(I5) )
proof end;

registration
cluster Function-like V29(K17([.0,1.],[.0,1.]),[.0,1.]) satisfying_(NP) -> satisfying_(I4) satisfying_(I5) for Element of K16(K17(K17([.0,1.],[.0,1.]),[.0,1.]));
coherence
for b1 being BinOp of [.0,1.] st b1 is satisfying_(NP) holds
( b1 is satisfying_(I4) & b1 is satisfying_(I5) )
by LemmaWA;
end;

theorem LemmaZA: :: FUZIMPL2:15
for I being BinOp of [.0,1.] st I is satisfying_(IP) holds
( I is satisfying_(I3) & I is satisfying_(I4) )
proof end;

registration
cluster Function-like V29(K17([.0,1.],[.0,1.]),[.0,1.]) satisfying_(IP) -> satisfying_(I3) satisfying_(I4) for Element of K16(K17(K17([.0,1.],[.0,1.]),[.0,1.]));
coherence
for b1 being BinOp of [.0,1.] st b1 is satisfying_(IP) holds
( b1 is satisfying_(I3) & b1 is satisfying_(I4) )
by LemmaZA;
end;

theorem LemmaAA: :: FUZIMPL2:16
for I being BinOp of [.0,1.] st I is satisfying_(OP) holds
( I is satisfying_(I3) & I is satisfying_(I4) & I is satisfying_(NC) & I is satisfying_(LB) & I is satisfying_(RB) & I is satisfying_(IP) )
proof end;

registration
coherence
for b1 being BinOp of [.0,1.] st b1 is satisfying_(OP) holds
( b1 is satisfying_(I3) & b1 is satisfying_(I4) & b1 is satisfying_(NC) & b1 is satisfying_(LB) & b1 is satisfying_(RB) & b1 is satisfying_(IP) )
by LemmaAA;
end;

theorem LemmaAB: :: FUZIMPL2:17
for I being BinOp of [.0,1.] st I is satisfying_(EP) & I is satisfying_(OP) holds
( I is satisfying_(I1) & I is satisfying_(I3) & I is satisfying_(I4) & I is satisfying_(I5) & I is satisfying_(LB) & I is satisfying_(RB) & I is satisfying_(NC) & I is satisfying_(NP) & I is satisfying_(IP) )
proof end;

registration
coherence
for b1 being BinOp of [.0,1.] st b1 is satisfying_(EP) & b1 is satisfying_(OP) holds
( b1 is satisfying_(I1) & b1 is satisfying_(I5) & b1 is satisfying_(NP) )
by LemmaAB;
end;

registration
coherence
proof end;
coherence
proof end;
coherence
( I_RC is satisfying_(NP) & I_RC is satisfying_(EP) & not I_RC is satisfying_(IP) & not I_RC is satisfying_(OP) )
proof end;
coherence
( I_KD is satisfying_(NP) & I_KD is satisfying_(EP) & not I_KD is satisfying_(IP) & not I_KD is satisfying_(OP) )
proof end;
coherence
proof end;
coherence
( not I_RS is satisfying_(NP) & not I_RS is satisfying_(EP) & I_RS is satisfying_(IP) & I_RS is satisfying_(OP) )
proof end;
coherence
( I_YG is satisfying_(NP) & I_YG is satisfying_(EP) & not I_YG is satisfying_(IP) & not I_YG is satisfying_(OP) )
proof end;
coherence
proof end;
coherence
proof end;
end;

registration
coherence
( not I_{0} is satisfying_(NP) & I_{0} is satisfying_(EP) & not I_{0} is satisfying_(IP) & not I_{0} is satisfying_(OP) )
proof end;
coherence
( not I_{1} is satisfying_(NP) & I_{1} is satisfying_(EP) & I_{1} is satisfying_(IP) & not I_{1} is satisfying_(OP) )
proof end;
end;