:: by Adam Grabowski

::

:: Received September 29, 2018

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

notation

synonym I_LK for Lukasiewicz_implication ;

synonym I_GD for Goedel_implication ;

synonym I_RC for Reichenbach_implication ;

synonym I_KD for Kleene-Dienes_implication ;

synonym I_GG for Goguen_implication ;

synonym I_RS for Rescher_implication ;

synonym I_YG for Yager_implication ;

synonym I_WB for Weber_implication ;

synonym I_FD for Fodor_implication ;

end;
synonym I_GD for Goedel_implication ;

synonym I_RC for Reichenbach_implication ;

synonym I_KD for Kleene-Dienes_implication ;

synonym I_GG for Goguen_implication ;

synonym I_RS for Rescher_implication ;

synonym I_YG for Yager_implication ;

synonym I_WB for Weber_implication ;

synonym I_FD for Fodor_implication ;

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 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 ) )

( 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

((#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)

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 ) )

( ( 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)) ) )

( ( 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: I_KD <= I_RC

proof end;

Lemma112: I_RC <= I_LK

proof end;

Lemma113: I_LK <= I_WB

proof end;

theorem :: FUZIMPL2:7

Lemma121: I_RS <= I_GD

proof end;

Lemma122: I_GD <= I_GG

proof end;

Lemma123: I_GG <= I_LK

proof end;

theorem :: FUZIMPL2:8

Lemma132: I_RC <= I_LK

proof end;

Lemma141: I_KD <= I_FD

proof end;

Lemma142: I_FD <= I_LK

proof end;

theorem :: FUZIMPL2:10

Lemma151: I_RS <= I_GD

proof end;

Lemma152: I_GD <= I_FD

proof end;

Lemma153: I_FD <= I_LK

proof end;

theorem :: FUZIMPL2:11

definition

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

end;
attr I is satisfying_(NP) means :: FUZIMPL2:def 1

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

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)));

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;

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 );

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

( I . (x,y) = 1 iff x <= y );

:: 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 );

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))) );

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 );

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 ) );

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

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

synonym satisfying_(NC) I for 01-dominant ;

synonym satisfying_(I1) I for decreasing_on_1st ;

synonym satisfying_(I2) I for increasing_on_2nd ;

synonym satisfying_(I3) I for 00-dominant ;

synonym satisfying_(I4) I for 11-dominant ;

synonym satisfying_(I5) I for 10-weak ;

end;
synonym satisfying_(NC) I for 01-dominant ;

synonym satisfying_(I1) I for decreasing_on_1st ;

synonym satisfying_(I2) I for increasing_on_2nd ;

synonym satisfying_(I3) I for 00-dominant ;

synonym satisfying_(I4) I for 11-dominant ;

synonym satisfying_(I5) I for 10-weak ;

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) )

( I is satisfying_(I3) & I is satisfying_(NC) )

proof end;

registration

for b_{1} being BinOp of [.0,1.] st b_{1} is satisfying_(LB) holds

( b_{1} is satisfying_(I3) & b_{1} is satisfying_(NC) )
by LemmaXA;

end;

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 b

( b

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) )

( I is satisfying_(I4) & I is satisfying_(NC) )

proof end;

registration

for b_{1} being BinOp of [.0,1.] st b_{1} is satisfying_(RB) holds

( b_{1} is satisfying_(I4) & b_{1} is satisfying_(NC) )
by LemmaVA;

end;

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 b

( b

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) )

( I is satisfying_(I4) & I is satisfying_(I5) )

proof end;

registration

for b_{1} being BinOp of [.0,1.] st b_{1} is satisfying_(NP) holds

( b_{1} is satisfying_(I4) & b_{1} is satisfying_(I5) )
by LemmaWA;

end;

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 b

( b

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) )

( I is satisfying_(I3) & I is satisfying_(I4) )

proof end;

registration

for b_{1} being BinOp of [.0,1.] st b_{1} is satisfying_(IP) holds

( b_{1} is satisfying_(I3) & b_{1} is satisfying_(I4) )
by LemmaZA;

end;

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 b

( b

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) )

( 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

for b_{1} being BinOp of [.0,1.] st b_{1} is satisfying_(OP) holds

( b_{1} is satisfying_(I3) & b_{1} is satisfying_(I4) & b_{1} is satisfying_(NC) & b_{1} is satisfying_(LB) & b_{1} is satisfying_(RB) & b_{1} is satisfying_(IP) )
by LemmaAA;

end;

cluster Function-like V29(K17([.0,1.],[.0,1.]),[.0,1.]) satisfying_(OP) -> satisfying_(I3) satisfying_(I4) satisfying_(NC) satisfying_(LB) satisfying_(RB) satisfying_(IP) for Element of K16(K17(K17([.0,1.],[.0,1.]),[.0,1.]));

coherence for b

( b

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) )

( 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

for b_{1} being BinOp of [.0,1.] st b_{1} is satisfying_(EP) & b_{1} is satisfying_(OP) holds

( b_{1} is satisfying_(I1) & b_{1} is satisfying_(I5) & b_{1} is satisfying_(NP) )
by LemmaAB;

end;

cluster Function-like V29(K17([.0,1.],[.0,1.]),[.0,1.]) satisfying_(EP) satisfying_(OP) -> satisfying_(I1) satisfying_(I5) satisfying_(NP) for Element of K16(K17(K17([.0,1.],[.0,1.]),[.0,1.]));

coherence for b

( b

registration

coherence

( I_LK is satisfying_(NP) & I_LK is satisfying_(EP) & I_LK is satisfying_(IP) & I_LK is satisfying_(OP) )

( I_GD is satisfying_(NP) & I_GD is satisfying_(EP) & I_GD is satisfying_(IP) & I_GD is satisfying_(OP) )

( I_RC is satisfying_(NP) & I_RC is satisfying_(EP) & not I_RC is satisfying_(IP) & not I_RC is satisfying_(OP) )

( I_KD is satisfying_(NP) & I_KD is satisfying_(EP) & not I_KD is satisfying_(IP) & not I_KD is satisfying_(OP) )

( I_GG is satisfying_(NP) & I_GG is satisfying_(EP) & I_GG is satisfying_(IP) & I_GG is satisfying_(OP) )

( not I_RS is satisfying_(NP) & not I_RS is satisfying_(EP) & I_RS is satisfying_(IP) & I_RS is satisfying_(OP) )

( I_YG is satisfying_(NP) & I_YG is satisfying_(EP) & not I_YG is satisfying_(IP) & not I_YG is satisfying_(OP) )

( I_WB is satisfying_(NP) & I_WB is satisfying_(EP) & I_WB is satisfying_(IP) & not I_WB is satisfying_(OP) )

( I_FD is satisfying_(NP) & I_FD is satisfying_(EP) & I_FD is satisfying_(IP) & I_FD is satisfying_(OP) )

end;
( I_LK is satisfying_(NP) & I_LK is satisfying_(EP) & I_LK is satisfying_(IP) & I_LK is satisfying_(OP) )

proof end;

coherence ( I_GD is satisfying_(NP) & I_GD is satisfying_(EP) & I_GD is satisfying_(IP) & I_GD is satisfying_(OP) )

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 ( I_GG is satisfying_(NP) & I_GG is satisfying_(EP) & I_GG is satisfying_(IP) & I_GG is satisfying_(OP) )

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 ( I_WB is satisfying_(NP) & I_WB is satisfying_(EP) & I_WB is satisfying_(IP) & not I_WB is satisfying_(OP) )

proof end;

coherence ( I_FD is satisfying_(NP) & I_FD is satisfying_(EP) & I_FD is satisfying_(IP) & I_FD is satisfying_(OP) )

proof 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) )

( not I_{1} is satisfying_(NP) & I_{1} is satisfying_(EP) & I_{1} is satisfying_(IP) & not I_{1} is satisfying_(OP) )

end;
( 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;