fuzimpl1.miz



    begin

    theorem :: FUZIMPL1:1

    

     MaxMinIn01: for a,b be Element of [. 0 , 1.] holds ( max (b,( min ((1 - a),(1 - b))))) in [. 0 , 1.]

    proof

      let a,b be Element of [. 0 , 1.];

      

       a1: (1 - a) in [. 0 , 1.] & (1 - b) in [. 0 , 1.] by FUZNORM1: 7;

      ( max (b,( min ((1 - a),(1 - b))))) = b or ( max (b,( min ((1 - a),(1 - b))))) = ( min ((1 - a),(1 - b))) by XXREAL_0: 16;

      hence thesis by a1, FUZNORM1: 1;

    end;

    theorem :: FUZIMPL1:2

    

     LukaIn01: for a,b be Element of [. 0 , 1.] holds ( min (1,((1 - a) + b))) in [. 0 , 1.]

    proof

      let a,b be Element of [. 0 , 1.];

      

       A1: ( min (1,((1 - a) + b))) <= 1 by XXREAL_0: 17;

      (1 - a) in [. 0 , 1.] by FUZNORM1: 7;

      then (1 - a) >= 0 & b >= 0 by XXREAL_1: 1;

      then ( min (1,((1 - a) + b))) >= 0 by XXREAL_0: 20;

      hence thesis by A1, XXREAL_1: 1;

    end;

    theorem :: FUZIMPL1:3

    

     ReichenbachIn01: for a,b be Element of [. 0 , 1.] holds ((1 - a) + (a * b)) in [. 0 , 1.]

    proof

      let a,b be Element of [. 0 , 1.];

      (1 - a) in [. 0 , 1.] by FUZNORM1: 7;

      then

       A0: (1 - a) >= 0 by XXREAL_1: 1;

      (a * b) in [. 0 , 1.] by FUZNORM1: 3;

      then

       a1: (a * b) >= 0 by XXREAL_1: 1;

      b <= 1 by XXREAL_1: 1;

      then

       a2: (b - 1) <= (1 - 1) by XREAL_1: 9;

      a >= 0 by XXREAL_1: 1;

      then (a * (b - 1)) <= 0 by a2;

      then (1 + ((a * b) - a)) <= (1 + 0 ) by XREAL_1: 7;

      hence thesis by a1, A0, XXREAL_1: 1;

    end;

    theorem :: FUZIMPL1:4

    

     Max1In01: for a,b be Element of [. 0 , 1.] holds ( max ((1 - a),b)) in [. 0 , 1.]

    proof

      let a,b be Element of [. 0 , 1.];

      ( max ((1 - a),b)) = (1 - a) or ( max ((1 - a),b)) = b by XXREAL_0: 16;

      hence thesis by FUZNORM1: 7;

    end;

    theorem :: FUZIMPL1:5

    

     PowerIn01: for a,b be Element of [. 0 , 1.] st a > 0 or b > 0 holds (b to_power a) in [. 0 , 1.]

    proof

      let a,b be Element of [. 0 , 1.];

      

       YY: b <= 1 & b >= 0 by XXREAL_1: 1;

      

       XX: a >= 0 by XXREAL_1: 1;

      assume a > 0 or b > 0 ;

      per cases ;

        suppose

         S1: a > 0 & b <> 0 & b <> 1;

        then

         B1: a > 0 & b > 0 by XXREAL_1: 1;

        

         ZZ: b < 1 by S1, XXREAL_0: 1, YY;

        (b to_power a) < (b to_power 0 ) by POWER: 40, B1, ZZ;

        then

         A1: (b to_power a) <= 1 by POWER: 24;

        (b to_power a) > 0 by B1, POWER: 34;

        hence thesis by A1, XXREAL_1: 1;

      end;

        suppose

         S1: a > 0 & b <> 0 & b = 1;

        then

         A1: (b to_power a) <= 1 by POWER: 26;

        (b to_power a) > 0 by S1, POWER: 34;

        hence thesis by A1, XXREAL_1: 1;

      end;

        suppose

         B1: a > 0 & b = 0 ;

        then

         A1: (b to_power a) <= 1 by POWER:def 2;

        (b to_power a) >= 0 by POWER:def 2, B1;

        hence thesis by A1, XXREAL_1: 1;

      end;

        suppose

         B1: b > 0 & b <> 1;

        b <= 1 by XXREAL_1: 1;

        then (b to_power a) <= (1 to_power a) by XX, B1, HOLDER_1: 3;

        then

         A1: (b to_power a) <= 1 by POWER: 26;

        (b to_power a) > 0 by B1, POWER: 34;

        hence thesis by A1, XXREAL_1: 1;

      end;

        suppose

         B1: b > 0 & b = 1;

        then

         A1: (b to_power a) <= 1 by POWER: 26;

        (b to_power a) > 0 by B1, POWER: 34;

        hence thesis by A1, XXREAL_1: 1;

      end;

    end;

    theorem :: FUZIMPL1:6

    

     QuoIn01: for a,b be Element of [. 0 , 1.] st a > b holds (b / a) in [. 0 , 1.]

    proof

      let a,b be Element of [. 0 , 1.];

      assume

       A0: a > b;

      

       A2: 0 <= a <= 1 & 0 <= b <= 1 by XXREAL_1: 1;

      then (b / a) <= 1 by XREAL_1: 185, A0;

      hence thesis by A2, XXREAL_1: 1;

    end;

    begin

    definition

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

      :: FUZIMPL1:def1

      attr f is decreasing_on_1st means

      : DefDecr: for x1,x2,y be Element of [. 0 , 1.] st x1 <= x2 holds (f . (x1,y)) >= (f . (x2,y));

      :: FUZIMPL1:def2

      attr f is increasing_on_2nd means

      : DefIncr: for x,y1,y2 be Element of [. 0 , 1.] st y1 <= y2 holds (f . (x,y1)) <= (f . (x,y2));

      :: FUZIMPL1:def3

      attr f is 00-dominant means

      : Def00: (f . ( 0 , 0 )) = 1;

      :: FUZIMPL1:def4

      attr f is 11-dominant means

      : Def11: (f . (1,1)) = 1;

      :: FUZIMPL1:def5

      attr f is 10-weak means

      : Def10: (f . (1, 0 )) = 0 ;

      :: FUZIMPL1:def6

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

    end

    definition

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

      :: FUZIMPL1:def7

      attr f is with_properties_of_fuzzy_implication means f is decreasing_on_1st increasing_on_2nd 00-dominant 11-dominant 10-weak;

      :: FUZIMPL1:def8

      attr f is with_properties_of_classical_implication means f is 00-dominant 01-dominant 11-dominant 10-weak;

    end

    begin

    definition

      :: FUZIMPL1:def9

      func I_{-1} -> BinOp of [. 0 , 1.] means

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

      existence

      proof

        set A = [. 0 , 1.];

        deffunc F( Element of A, Element of A) = ( In (( max ((1 - $1),( min ($1,$2)))),A));

        ex f be Function of [:A, A:], A st for x be Element of A holds for y be Element of A holds (f . (x,y)) = F(x,y) from BINOP_1:sch 4;

        then

        consider f be BinOp of A such that

         A1: for x be Element of A holds for y be Element of A holds (f . (x,y)) = F(x,y);

        take f;

        let a,b be Element of [. 0 , 1.];

        

         A2: (f . (a,b)) = F(a,b) by A1;

        ( max ((1 - a),( min (a,b)))) = (1 - a) or ( max ((1 - a),( min (a,b)))) = ( min (a,b)) by XXREAL_0: 16;

        hence thesis by A2, SUBSET_1:def 8, FUZNORM1: 7, FUZNORM1: 1;

      end;

      uniqueness

      proof

        let f1,f2 be BinOp of [. 0 , 1.] such that

         A1: for a,b be Element of [. 0 , 1.] holds (f1 . (a,b)) = ( max ((1 - a),( min (a,b)))) and

         A2: for a,b be Element of [. 0 , 1.] holds (f2 . (a,b)) = ( max ((1 - a),( min (a,b))));

        

         A3: ( dom f1) = [: [. 0 , 1.], [. 0 , 1.]:] by FUNCT_2:def 1

        .= ( dom f2) by FUNCT_2:def 1;

        for x,y be object st [x, y] in ( dom f1) holds (f1 . (x,y)) = (f2 . (x,y))

        proof

          let x,y be object;

          assume [x, y] in ( dom f1);

          then

          reconsider xx = x, yy = y as Element of [. 0 , 1.] by ZFMISC_1: 87;

          (f1 . (xx,yy)) = ( max ((1 - xx),( min (xx,yy)))) by A1

          .= (f2 . (xx,yy)) by A2;

          hence thesis;

        end;

        hence thesis by A3, BINOP_1: 20;

      end;

    end

    registration

      cluster I_{-1} -> increasing_on_2nd 00-dominant 11-dominant 10-weak;

      coherence

      proof

        set f = I_{-1} ;

        

         b2: for x,y1,y2 be Element of [. 0 , 1.] st y1 <= y2 holds (f . (x,y1)) <= (f . (x,y2))

        proof

          let x,y1,y2 be Element of [. 0 , 1.];

          assume y1 <= y2;

          then

           y1: ( min (x,y1)) <= ( min (x,y2)) by XXREAL_0: 18;

          (f . (x,y1)) = ( max ((1 - x),( min (x,y1)))) & (f . (x,y2)) = ( max ((1 - x),( min (x,y2)))) by I1Def;

          hence thesis by y1, XXREAL_0: 26;

        end;

        

         S: 0 in [. 0 , 1.] & 1 in [. 0 , 1.] by XXREAL_1: 1;

        

        then

         T1: (f . ( 0 , 0 )) = ( max ((1 - 0 ),( min ( 0 , 0 )))) by I1Def

        .= 1 by XXREAL_0:def 10;

        

         T2: (f . (1, 0 )) = ( max ((1 - 1),( min (1, 0 )))) by S, I1Def

        .= ( max ( 0 , 0 )) by XXREAL_0:def 9

        .= 0 ;

        (f . (1,1)) = ( max ((1 - 1),( min (1,1)))) by S, I1Def

        .= 1 by XXREAL_0:def 10;

        hence thesis by b2, T1, T2;

      end;

    end

    definition

      :: FUZIMPL1:def10

      func I_{-2} -> BinOp of [. 0 , 1.] means

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

      existence

      proof

        set A = [. 0 , 1.];

        deffunc F( Element of A, Element of A) = ( In (( max ($2,( min ((1 - $1),(1 - $2))))),A));

        ex f be Function of [:A, A:], A st for x be Element of A holds for y be Element of A holds (f . (x,y)) = F(x,y) from BINOP_1:sch 4;

        then

        consider f be BinOp of A such that

         A1: for x be Element of A holds for y be Element of A holds (f . (x,y)) = F(x,y);

        take f;

        let a,b be Element of [. 0 , 1.];

        (f . (a,b)) = F(a,b) by A1;

        hence thesis by SUBSET_1:def 8, MaxMinIn01;

      end;

      uniqueness

      proof

        let f1,f2 be BinOp of [. 0 , 1.] such that

         A1: for a,b be Element of [. 0 , 1.] holds (f1 . (a,b)) = ( max (b,( min ((1 - a),(1 - b))))) and

         A2: for a,b be Element of [. 0 , 1.] holds (f2 . (a,b)) = ( max (b,( min ((1 - a),(1 - b)))));

        

         A3: ( dom f1) = [: [. 0 , 1.], [. 0 , 1.]:] by FUNCT_2:def 1

        .= ( dom f2) by FUNCT_2:def 1;

        for x,y be object st [x, y] in ( dom f1) holds (f1 . (x,y)) = (f2 . (x,y))

        proof

          let x,y be object;

          assume [x, y] in ( dom f1);

          then

          reconsider xx = x, yy = y as Element of [. 0 , 1.] by ZFMISC_1: 87;

          (f1 . (xx,yy)) = ( max (yy,( min ((1 - xx),(1 - yy))))) by A1

          .= (f2 . (xx,yy)) by A2;

          hence thesis;

        end;

        hence thesis by A3, BINOP_1: 20;

      end;

    end

    registration

      cluster I_{-2} -> decreasing_on_1st 00-dominant 11-dominant 10-weak;

      coherence

      proof

        set f = I_{-2} ;

        

         b1: for x1,x2,y be Element of [. 0 , 1.] st x1 <= x2 holds (f . (x1,y)) >= (f . (x2,y))

        proof

          let x1,x2,y be Element of [. 0 , 1.];

          assume

           Z1: x1 <= x2;

          

           Z2: (f . (x1,y)) = ( max (y,( min ((1 - x1),(1 - y))))) & (f . (x2,y)) = ( max (y,( min ((1 - x2),(1 - y))))) by I2Def;

          (1 - x1) >= (1 - x2) by Z1, XREAL_1: 13;

          then ( min ((1 - x1),(1 - y))) >= ( min ((1 - x2),(1 - y))) by XXREAL_0: 18;

          hence thesis by Z2, XXREAL_0: 26;

        end;

        

         S: 0 in [. 0 , 1.] & 1 in [. 0 , 1.] by XXREAL_1: 1;

        

        then

         T1: (f . ( 0 , 0 )) = ( max ( 0 ,( min ((1 - 0 ),(1 - 0 ))))) by I2Def

        .= 1 by XXREAL_0:def 10;

        

         T2: (f . (1, 0 )) = ( max ( 0 ,( min ((1 - 1),(1 - 0 ))))) by S, I2Def

        .= ( max ( 0 , 0 )) by XXREAL_0:def 9

        .= 0 ;

        (f . (1,1)) = ( max (1,( min ((1 - 1),(1 - 1))))) by S, I2Def

        .= 1 by XXREAL_0:def 10;

        hence thesis by b1, T1, T2;

      end;

    end

    definition

      :: FUZIMPL1:def11

      func I_{-3} -> BinOp of [. 0 , 1.] means

      : I3Def: for x,y be Element of [. 0 , 1.] holds (y < 1 implies (it . (x,y)) = 0 ) & (y = 1 implies (it . (x,y)) = 1);

      existence

      proof

        set C = [. 0 , 1.];

        defpred P[ Real, Real] means $2 < 1;

        deffunc F( Element of C, Element of C) = ( In ( 0 ,C));

        deffunc G( Element of C, Element of C) = ( In (1,C));

        ex f be Function of [:C, C:], C st for c be Element of C, d be Element of C st [c, d] in ( dom f) holds ( P[c, d] implies (f . [c, d]) = F(c,d)) & ( not P[c, d] implies (f . [c, d]) = G(c,d)) from SCHEME1:sch 21;

        then

        consider f be Function of [:C, C:], C such that

         A1: for c be Element of C, d be Element of C st [c, d] in ( dom f) holds ( P[c, d] implies (f . [c, d]) = F(c,d)) & ( not P[c, d] implies (f . [c, d]) = G(c,d));

        take f;

        

         A0: ( dom f) = [:C, C:] by FUNCT_2:def 1;

        let a,b be Element of C;

        

         AA: [a, b] in ( dom f) by A0, ZFMISC_1: 87;

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

        proof

          thus b < 1 implies (f . (a,b)) = 0

          proof

            assume b < 1;

            

            then (f . [a, b]) = F(a,b) by A1, AA

            .= 0 by SUBSET_1:def 8, XXREAL_1: 1;

            hence thesis;

          end;

          assume b = 1;

          

          then (f . [a, b]) = G(a,b) by A1, AA

          .= 1 by XXREAL_1: 1, SUBSET_1:def 8;

          hence thesis;

        end;

        hence thesis;

      end;

      uniqueness

      proof

        let f1,f2 be BinOp of [. 0 , 1.] such that

         A1: for a,b be Element of [. 0 , 1.] holds (b < 1 implies (f1 . (a,b)) = 0 ) & (b = 1 implies (f1 . (a,b)) = 1) and

         A2: for a,b be Element of [. 0 , 1.] holds (b < 1 implies (f2 . (a,b)) = 0 ) & (b = 1 implies (f2 . (a,b)) = 1);

        for a,b be set st a in [. 0 , 1.] & b in [. 0 , 1.] holds (f1 . (a,b)) = (f2 . (a,b))

        proof

          let a,b be set;

          assume a in [. 0 , 1.] & b in [. 0 , 1.];

          then

          reconsider aa = a, bb = b as Element of [. 0 , 1.];

          bb <= 1 by XXREAL_1: 1;

          per cases by XXREAL_0: 1;

            suppose

             B0: bb < 1;

            

            then (f1 . (aa,bb)) = 0 by A1

            .= (f2 . (aa,bb)) by A2, B0;

            hence thesis;

          end;

            suppose

             B1: bb = 1;

            

            then (f1 . (aa,bb)) = 1 by A1

            .= (f2 . (aa,bb)) by A2, B1;

            hence thesis;

          end;

        end;

        hence thesis by BINOP_1:def 21;

      end;

    end

    registration

      cluster I_{-3} -> decreasing_on_1st increasing_on_2nd non 00-dominant 11-dominant 10-weak;

      coherence

      proof

        set f = I_{-3} ;

        

         b1: for x1,x2,y be Element of [. 0 , 1.] st x1 <= x2 holds (f . (x1,y)) >= (f . (x2,y))

        proof

          let x1,x2,y be Element of [. 0 , 1.];

          

           SS: y <= 1 by XXREAL_1: 1;

          assume x1 <= x2;

          per cases ;

            suppose y = 1;

            then (f . (x1,y)) = 1 & (f . (x2,y)) = 1 by I3Def;

            hence thesis;

          end;

            suppose y <> 1;

            then y < 1 by SS, XXREAL_0: 1;

            then (f . (x1,y)) = 0 & (f . (x2,y)) = 0 by I3Def;

            hence thesis;

          end;

        end;

        

         b2: for x,y1,y2 be Element of [. 0 , 1.] st y1 <= y2 holds (f . (x,y1)) <= (f . (x,y2))

        proof

          let x,y1,y2 be Element of [. 0 , 1.];

          assume

           YY: y1 <= y2;

          per cases ;

            suppose

             Y0: y1 = 1;

            y2 >= 1 & y2 <= 1 by XXREAL_1: 1, Y0, YY;

            then y2 = 1 by XXREAL_0: 1;

            then (f . (x,y2)) = 1 by I3Def;

            hence thesis by XXREAL_1: 1;

          end;

            suppose

             Za: y1 <> 1 & y2 = 1;

            y1 <= 1 by XXREAL_1: 1;

            then y1 < 1 by Za, XXREAL_0: 1;

            then (f . (x,y1)) = 0 by I3Def;

            hence thesis by Za, I3Def;

          end;

            suppose

             Za: y1 <> 1 & y2 <> 1;

            y1 <= 1 & y2 <= 1 by XXREAL_1: 1;

            then y1 < 1 & y2 < 1 by Za, XXREAL_0: 1;

            then (f . (x,y1)) = 0 & (f . (x,y2)) = 0 by I3Def;

            hence thesis;

          end;

        end;

         0 in [. 0 , 1.] & 1 in [. 0 , 1.] by XXREAL_1: 1;

        hence thesis by b1, b2, I3Def;

      end;

    end

    definition

      :: FUZIMPL1:def12

      func I_{-4} -> BinOp of [. 0 , 1.] means

      : I4Def: for x,y be Element of [. 0 , 1.] holds (x = 0 implies (it . (x,y)) = 1) & (x > 0 implies (it . (x,y)) = 0 );

      existence

      proof

        set C = [. 0 , 1.];

        defpred P[ Real, Real] means $1 > 0 ;

        deffunc F( Element of C, Element of C) = ( In ( 0 ,C));

        deffunc G( Element of C, Element of C) = ( In (1,C));

        ex f be Function of [:C, C:], C st for c be Element of C, d be Element of C st [c, d] in ( dom f) holds ( P[c, d] implies (f . [c, d]) = F(c,d)) & ( not P[c, d] implies (f . [c, d]) = G(c,d)) from SCHEME1:sch 21;

        then

        consider f be Function of [:C, C:], C such that

         A1: for c be Element of C, d be Element of C st [c, d] in ( dom f) holds ( P[c, d] implies (f . [c, d]) = F(c,d)) & ( not P[c, d] implies (f . [c, d]) = G(c,d));

        take f;

        

         A0: ( dom f) = [:C, C:] by FUNCT_2:def 1;

        let a,b be Element of C;

        

         AA: [a, b] in ( dom f) by A0, ZFMISC_1: 87;

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

        proof

          thus a > 0 implies (f . (a,b)) = 0

          proof

            assume a > 0 ;

            

            then (f . [a, b]) = F(a,b) by A1, AA

            .= 0 by SUBSET_1:def 8, XXREAL_1: 1;

            hence thesis;

          end;

          assume a = 0 ;

          

          then (f . [a, b]) = G(a,b) by A1, AA

          .= 1 by XXREAL_1: 1, SUBSET_1:def 8;

          hence thesis;

        end;

        hence thesis;

      end;

      uniqueness

      proof

        let f1,f2 be BinOp of [. 0 , 1.] such that

         A1: for a,b be Element of [. 0 , 1.] holds (a = 0 implies (f1 . (a,b)) = 1) & (a > 0 implies (f1 . (a,b)) = 0 ) and

         A2: for a,b be Element of [. 0 , 1.] holds (a = 0 implies (f2 . (a,b)) = 1) & (a > 0 implies (f2 . (a,b)) = 0 );

        for a,b be set st a in [. 0 , 1.] & b in [. 0 , 1.] holds (f1 . (a,b)) = (f2 . (a,b))

        proof

          let a,b be set;

          assume a in [. 0 , 1.] & b in [. 0 , 1.];

          then

          reconsider aa = a, bb = b as Element of [. 0 , 1.];

          per cases by XXREAL_1: 1;

            suppose

             B0: aa > 0 ;

            

            then (f1 . (aa,bb)) = 0 by A1

            .= (f2 . (aa,bb)) by A2, B0;

            hence thesis;

          end;

            suppose

             B1: aa = 0 ;

            

            then (f1 . (aa,bb)) = 1 by A1

            .= (f2 . (aa,bb)) by A2, B1;

            hence thesis;

          end;

        end;

        hence thesis by BINOP_1:def 21;

      end;

    end

    registration

      cluster I_{-4} -> decreasing_on_1st increasing_on_2nd 00-dominant non 11-dominant 10-weak;

      coherence

      proof

        set f = I_{-4} ;

        

         b1: for x1,x2,y be Element of [. 0 , 1.] st x1 <= x2 holds (f . (x1,y)) >= (f . (x2,y))

        proof

          let x1,x2,y be Element of [. 0 , 1.];

          assume

           Z1: x1 <= x2;

          per cases ;

            suppose

             Z0: x2 = 0 ;

            then x1 = 0 by Z1, XXREAL_1: 1;

            hence thesis by Z0;

          end;

            suppose x2 <> 0 & x1 <> 0 ;

            then x1 > 0 & x2 > 0 by XXREAL_1: 1;

            then (f . (x2,y)) = 0 by I4Def;

            hence thesis by XXREAL_1: 1;

          end;

            suppose

             Z1: x2 <> 0 & x1 = 0 ;

            x2 >= 0 by XXREAL_1: 1;

            then (f . (x2,y)) = 0 by I4Def, Z1;

            hence thesis by Z1, I4Def;

          end;

        end;

        

         b2: for x,y1,y2 be Element of [. 0 , 1.] st y1 <= y2 holds (f . (x,y1)) <= (f . (x,y2))

        proof

          let x,y1,y2 be Element of [. 0 , 1.];

          

           SS: x >= 0 by XXREAL_1: 1;

          assume y1 <= y2;

          per cases ;

            suppose x = 0 ;

            then (f . (x,y1)) = 1 & (f . (x,y2)) = 1 by I4Def;

            hence thesis;

          end;

            suppose x <> 0 ;

            then (f . (x,y1)) = 0 & (f . (x,y2)) = 0 by I4Def, SS;

            hence thesis;

          end;

        end;

         0 in [. 0 , 1.] & 1 in [. 0 , 1.] by XXREAL_1: 1;

        hence thesis by b1, b2, I4Def;

      end;

    end

    definition

      :: FUZIMPL1:def13

      func I_{-5} -> BinOp of [. 0 , 1.] means

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

      existence

      proof

        set A = [. 0 , 1.];

        deffunc F( Element of A, Element of A) = ( In (1,A));

        ex f be Function of [:A, A:], A st for x be Element of A holds for y be Element of A holds (f . (x,y)) = F(x,y) from BINOP_1:sch 4;

        then

        consider f be BinOp of A such that

         A1: for x be Element of A holds for y be Element of A holds (f . (x,y)) = F(x,y);

        take f;

        let a,b be Element of [. 0 , 1.];

        (f . (a,b)) = F(a,b) by A1;

        hence thesis by SUBSET_1:def 8, XXREAL_1: 1;

      end;

      uniqueness

      proof

        let f1,f2 be BinOp of [. 0 , 1.] such that

         A1: for a,b be Element of [. 0 , 1.] holds (f1 . (a,b)) = 1 and

         A2: for a,b be Element of [. 0 , 1.] holds (f2 . (a,b)) = 1;

        

         A3: ( dom f1) = [: [. 0 , 1.], [. 0 , 1.]:] by FUNCT_2:def 1

        .= ( dom f2) by FUNCT_2:def 1;

        for x,y be object st [x, y] in ( dom f1) holds (f1 . (x,y)) = (f2 . (x,y))

        proof

          let x,y be object;

          assume [x, y] in ( dom f1);

          then

          reconsider xx = x, yy = y as Element of [. 0 , 1.] by ZFMISC_1: 87;

          (f1 . (xx,yy)) = 1 by A1

          .= (f2 . (xx,yy)) by A2;

          hence thesis;

        end;

        hence thesis by A3, BINOP_1: 20;

      end;

    end

    registration

      cluster I_{-5} -> decreasing_on_1st increasing_on_2nd 00-dominant 11-dominant non 10-weak;

      coherence

      proof

        set f = I_{-5} ;

        

         b1: for x1,x2,y be Element of [. 0 , 1.] st x1 <= x2 holds (f . (x1,y)) >= (f . (x2,y))

        proof

          let x1,x2,y be Element of [. 0 , 1.];

          assume x1 <= x2;

          (f . (x1,y)) = 1 & (f . (x2,y)) = 1 by I5Def;

          hence thesis;

        end;

        

         b2: for x,y1,y2 be Element of [. 0 , 1.] st y1 <= y2 holds (f . (x,y1)) <= (f . (x,y2))

        proof

          let x,y1,y2 be Element of [. 0 , 1.];

          assume y1 <= y2;

          (f . (x,y1)) = 1 & (f . (x,y2)) = 1 by I5Def;

          hence thesis;

        end;

         0 in [. 0 , 1.] & 1 in [. 0 , 1.] by XXREAL_1: 1;

        hence thesis by b1, b2, I5Def;

      end;

    end

    begin

    definition

      :: FUZIMPL1:def14

      func Lukasiewicz_implication -> BinOp of [. 0 , 1.] means

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

      existence

      proof

        set A = [. 0 , 1.];

        deffunc F( Element of A, Element of A) = ( In (( min (1,((1 - $1) + $2))),A));

        ex f be Function of [:A, A:], A st for x be Element of A holds for y be Element of A holds (f . (x,y)) = F(x,y) from BINOP_1:sch 4;

        then

        consider f be BinOp of A such that

         A1: for x be Element of A holds for y be Element of A holds (f . (x,y)) = F(x,y);

        take f;

        let a,b be Element of [. 0 , 1.];

        (f . (a,b)) = F(a,b) by A1;

        hence thesis by SUBSET_1:def 8, LukaIn01;

      end;

      uniqueness

      proof

        let f1,f2 be BinOp of [. 0 , 1.] such that

         A1: for a,b be Element of [. 0 , 1.] holds (f1 . (a,b)) = ( min (1,((1 - a) + b))) and

         A2: for a,b be Element of [. 0 , 1.] holds (f2 . (a,b)) = ( min (1,((1 - a) + b)));

        

         A3: ( dom f1) = [: [. 0 , 1.], [. 0 , 1.]:] by FUNCT_2:def 1

        .= ( dom f2) by FUNCT_2:def 1;

        for x,y be object st [x, y] in ( dom f1) holds (f1 . (x,y)) = (f2 . (x,y))

        proof

          let x,y be object;

          assume [x, y] in ( dom f1);

          then

          reconsider xx = x, yy = y as Element of [. 0 , 1.] by ZFMISC_1: 87;

          (f1 . (xx,yy)) = ( min (1,((1 - xx) + yy))) by A1

          .= (f2 . (xx,yy)) by A2;

          hence thesis;

        end;

        hence thesis by A3, BINOP_1: 20;

      end;

    end

    registration

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

      coherence

      proof

        set f = Lukasiewicz_implication ;

        

         A1: 0 in [. 0 , 1.] & 1 in [. 0 , 1.] by XXREAL_1: 1;

        

         b1: for x1,x2,y be Element of [. 0 , 1.] st x1 <= x2 holds (f . (x1,y)) >= (f . (x2,y))

        proof

          let x1,x2,y be Element of [. 0 , 1.];

          assume

           U1: x1 <= x2;

          

           U2: (f . (x1,y)) = ( min (1,((1 - x1) + y))) by Luk;

          

           U3: (f . (x2,y)) = ( min (1,((1 - x2) + y))) by Luk;

          (1 - x1) >= (1 - x2) by U1, XREAL_1: 13;

          then ((1 - x1) + y) >= ((1 - x2) + y) by XREAL_1: 7;

          hence thesis by U2, U3, XXREAL_0: 18;

        end;

        

         b3: for x,y1,y2 be Element of [. 0 , 1.] st y1 <= y2 holds (f . (x,y1)) <= (f . (x,y2))

        proof

          let x,y1,y2 be Element of [. 0 , 1.];

          assume y1 <= y2;

          then ((1 - x) + y1) <= ((1 - x) + y2) by XREAL_1: 7;

          then

           U1: ( min (1,((1 - x) + y2))) >= ( min (1,((1 - x) + y1))) by XXREAL_0: 18;

          (f . (x,y1)) = ( min (1,((1 - x) + y1))) by Luk;

          hence (f . (x,y1)) <= (f . (x,y2)) by U1, Luk;

        end;

        

         bb: ( min (1,((1 - 1) + 0 ))) = 0 by XXREAL_0:def 9;

        ( min (1,((1 - 0 ) + 0 ))) = 1;

        hence thesis by b1, b3, A1, Luk, bb;

      end;

    end

    registration

      cluster with_properties_of_fuzzy_implication for BinOp of [. 0 , 1.];

      existence

      proof

        take Lukasiewicz_implication ;

        thus thesis;

      end;

    end

    registration

      cluster with_properties_of_fuzzy_implication -> decreasing_on_1st increasing_on_2nd 00-dominant 11-dominant 10-weak for BinOp of [. 0 , 1.];

      coherence ;

      cluster decreasing_on_1st increasing_on_2nd 00-dominant 01-dominant 11-dominant 10-weak -> with_properties_of_fuzzy_implication for BinOp of [. 0 , 1.];

      coherence ;

      cluster with_properties_of_classical_implication -> 00-dominant 01-dominant 11-dominant 10-weak for BinOp of [. 0 , 1.];

      coherence ;

      cluster 00-dominant 01-dominant 11-dominant 10-weak -> with_properties_of_classical_implication for BinOp of [. 0 , 1.];

      coherence ;

      cluster with_properties_of_fuzzy_implication -> with_properties_of_classical_implication for BinOp of [. 0 , 1.];

      coherence

      proof

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

        assume

         A1: f is with_properties_of_fuzzy_implication;

        (f . ( 0 ,1)) = 1

        proof

          

           B1: 0 in [. 0 , 1.] & 1 in [. 0 , 1.] by XXREAL_1: 1;

          

           B2: f is increasing_on_2nd 00-dominant by A1;

          then

           B3: (f . ( 0 , 0 )) <= (f . ( 0 ,1)) by B1;

          reconsider e0 = 0 , e1 = 1 as Element of [. 0 , 1.] by XXREAL_1: 1;

          (f . (e0,e1)) <= 1 by XXREAL_1: 1;

          hence thesis by B2, B3, XXREAL_0: 1;

        end;

        then f is 01-dominant;

        hence thesis by A1;

      end;

    end

    definition

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

    end

    definition

      :: FUZIMPL1:def15

      func FI -> set equals the set of all f where f be Fuzzy_Implication;

      coherence ;

    end

    definition

      :: FUZIMPL1:def16

      func Goedel_implication -> BinOp of [. 0 , 1.] means

      : Goedel: for x,y be Element of [. 0 , 1.] holds (x <= y implies (it . (x,y)) = 1) & (x > y implies (it . (x,y)) = y);

      existence

      proof

        set C = [. 0 , 1.];

        defpred P[ Real, Real] means $1 <= $2;

        deffunc F( Element of C, Element of C) = ( In (1,C));

        deffunc G( Element of C, Element of C) = ( In ($2,C));

        ex f be Function of [:C, C:], C st for c be Element of C, d be Element of C st [c, d] in ( dom f) holds ( P[c, d] implies (f . [c, d]) = F(c,d)) & ( not P[c, d] implies (f . [c, d]) = G(c,d)) from SCHEME1:sch 21;

        then

        consider f be Function of [:C, C:], C such that

         A1: for c be Element of C, d be Element of C st [c, d] in ( dom f) holds ( P[c, d] implies (f . [c, d]) = F(c,d)) & ( not P[c, d] implies (f . [c, d]) = G(c,d));

        take f;

        

         A0: ( dom f) = [:C, C:] by FUNCT_2:def 1;

        let a,b be Element of C;

        

         AA: [a, b] in ( dom f) by A0, ZFMISC_1: 87;

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

        proof

          thus a <= b implies (f . (a,b)) = 1

          proof

            assume a <= b;

            

            then (f . [a, b]) = F(a,b) by A1, AA

            .= 1 by SUBSET_1:def 8, XXREAL_1: 1;

            hence thesis;

          end;

          assume a > b;

          

          then (f . [a, b]) = G(a,b) by A1, AA

          .= b by SUBSET_1:def 8;

          hence thesis;

        end;

        hence thesis;

      end;

      uniqueness

      proof

        let f1,f2 be BinOp of [. 0 , 1.] such that

         A1: for a,b be Element of [. 0 , 1.] holds (a <= b implies (f1 . (a,b)) = 1) & (a > b implies (f1 . (a,b)) = b) and

         A2: for a,b be Element of [. 0 , 1.] holds (a <= b implies (f2 . (a,b)) = 1) & (a > b implies (f2 . (a,b)) = b);

        for a,b be set st a in [. 0 , 1.] & b in [. 0 , 1.] holds (f1 . (a,b)) = (f2 . (a,b))

        proof

          let a,b be set;

          assume a in [. 0 , 1.] & b in [. 0 , 1.];

          then

          reconsider aa = a, bb = b as Element of [. 0 , 1.];

          per cases ;

            suppose

             B0: aa <= bb;

            

            then (f1 . (aa,bb)) = 1 by A1

            .= (f2 . (aa,bb)) by A2, B0;

            hence thesis;

          end;

            suppose

             B1: aa > bb;

            

            then (f1 . (aa,bb)) = bb by A1

            .= (f2 . (aa,bb)) by A2, B1;

            hence thesis;

          end;

        end;

        hence thesis by BINOP_1:def 21;

      end;

    end

    registration

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

      coherence

      proof

        set f = Goedel_implication ;

        

         a0: for x1,x2,y be Element of [. 0 , 1.] st x1 <= x2 holds (f . (x1,y)) >= (f . (x2,y))

        proof

          let x1,x2,y be Element of [. 0 , 1.];

          assume

           Z0: x1 <= x2;

          per cases ;

            suppose

             S1: x2 <= y;

            then

             S2: (f . (x2,y)) = 1 by Goedel;

            x1 <= y by S1, Z0, XXREAL_0: 2;

            hence (f . (x1,y)) >= (f . (x2,y)) by S2, Goedel;

          end;

            suppose x2 > y & x1 > y;

            then (f . (x2,y)) = y & (f . (x1,y)) = y by Goedel;

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

          end;

            suppose x2 > y & x1 <= y;

            then (f . (x2,y)) = y & (f . (x1,y)) = 1 by Goedel;

            hence (f . (x1,y)) >= (f . (x2,y)) by XXREAL_1: 1;

          end;

        end;

        

         aa: for x,y1,y2 be Element of [. 0 , 1.] st y1 <= y2 holds (f . (x,y1)) <= (f . (x,y2))

        proof

          let x,y1,y2 be Element of [. 0 , 1.];

          assume

           Z2: y1 <= y2;

          per cases ;

            suppose

             Z1: x <= y1;

            then

             Z3: (f . (x,y1)) = 1 by Goedel;

            x <= y2 by XXREAL_0: 2, Z1, Z2;

            hence thesis by Z3, Goedel;

          end;

            suppose x > y1 & x <= y2;

            then (f . (x,y1)) = y1 & (f . (x,y2)) = 1 by Goedel;

            hence thesis by XXREAL_1: 1;

          end;

            suppose x > y1 & x > y2;

            then (f . (x,y1)) = y1 & (f . (x,y2)) = y2 by Goedel;

            hence thesis by Z2;

          end;

        end;

         0 in [. 0 , 1.] & 1 in [. 0 , 1.] by XXREAL_1: 1;

        hence thesis by a0, aa, Goedel;

      end;

    end

    definition

      :: FUZIMPL1:def17

      func Reichenbach_implication -> BinOp of [. 0 , 1.] means

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

      existence

      proof

        set A = [. 0 , 1.];

        deffunc F( Element of A, Element of A) = ( In (((1 - $1) + ($1 * $2)),A));

        ex f be Function of [:A, A:], A st for x be Element of A holds for y be Element of A holds (f . (x,y)) = F(x,y) from BINOP_1:sch 4;

        then

        consider f be BinOp of A such that

         A1: for x be Element of A holds for y be Element of A holds (f . (x,y)) = F(x,y);

        take f;

        let a,b be Element of [. 0 , 1.];

        (f . (a,b)) = F(a,b) by A1;

        hence thesis by SUBSET_1:def 8, ReichenbachIn01;

      end;

      uniqueness

      proof

        let f1,f2 be BinOp of [. 0 , 1.] such that

         A1: for a,b be Element of [. 0 , 1.] holds (f1 . (a,b)) = ((1 - a) + (a * b)) and

         A2: for a,b be Element of [. 0 , 1.] holds (f2 . (a,b)) = ((1 - a) + (a * b));

        

         A3: ( dom f1) = [: [. 0 , 1.], [. 0 , 1.]:] by FUNCT_2:def 1

        .= ( dom f2) by FUNCT_2:def 1;

        for x,y be object st [x, y] in ( dom f1) holds (f1 . (x,y)) = (f2 . (x,y))

        proof

          let x,y be object;

          assume [x, y] in ( dom f1);

          then

          reconsider xx = x, yy = y as Element of [. 0 , 1.] by ZFMISC_1: 87;

          (f1 . (xx,yy)) = ((1 - xx) + (xx * yy)) by A1

          .= (f2 . (xx,yy)) by A2;

          hence thesis;

        end;

        hence thesis by A3, BINOP_1: 20;

      end;

    end

    registration

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

      coherence

      proof

        set f = Reichenbach_implication ;

        

         a0: for x1,x2,y be Element of [. 0 , 1.] st x1 <= x2 holds (f . (x1,y)) >= (f . (x2,y))

        proof

          let x1,x2,y be Element of [. 0 , 1.];

           0 <= y <= 1 by XXREAL_1: 1;

          then ( - 1) <= ( - y) by XREAL_1: 24;

          then

           zs: (1 + ( - 1)) <= (1 + ( - y)) by XREAL_1: 7;

          assume x1 <= x2;

          then ( - x2) <= ( - x1) by XREAL_1: 24;

          then (( - x2) * (1 - y)) <= (( - x1) * (1 - y)) by zs, XREAL_1: 64;

          then (1 + (( - x2) * (1 - y))) <= (1 + (( - x1) * (1 - y))) by XREAL_1: 7;

          then ((1 - x2) + (x2 * y)) <= ((1 - x1) + (x1 * y));

          then (f . (x2,y)) <= ((1 - x1) + (x1 * y)) by Reichen;

          hence thesis by Reichen;

        end;

        

         aa: for x,y1,y2 be Element of [. 0 , 1.] st y1 <= y2 holds (f . (x,y1)) <= (f . (x,y2))

        proof

          let x,y1,y2 be Element of [. 0 , 1.];

          

           P1: x >= 0 by XXREAL_1: 1;

          assume y1 <= y2;

          then (x * y1) <= (x * y2) by XREAL_1: 64, P1;

          then ((1 - x) + (x * y1)) <= ((1 - x) + (x * y2)) by XREAL_1: 7;

          then (f . (x,y1)) <= ((1 - x) + (x * y2)) by Reichen;

          hence thesis by Reichen;

        end;

        

         AA: 0 in [. 0 , 1.] & 1 in [. 0 , 1.] by XXREAL_1: 1;

        

        then

         A1: (f . ( 0 , 0 )) = ((1 - 0 ) + ( 0 * 0 )) by Reichen

        .= 1;

        

         A2: (f . (1,1)) = ((1 - 1) + (1 * 1)) by AA, Reichen

        .= 1;

        (f . (1, 0 )) = ((1 - 1) + (1 * 0 )) by AA, Reichen;

        hence thesis by A1, A2, a0, aa;

      end;

    end

    definition

      :: FUZIMPL1:def18

      func Kleene-Dienes_implication -> BinOp of [. 0 , 1.] means

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

      existence

      proof

        set A = [. 0 , 1.];

        deffunc F( Element of A, Element of A) = ( In (( max ((1 - $1),$2)),A));

        ex f be Function of [:A, A:], A st for x be Element of A holds for y be Element of A holds (f . (x,y)) = F(x,y) from BINOP_1:sch 4;

        then

        consider f be BinOp of A such that

         A1: for x be Element of A holds for y be Element of A holds (f . (x,y)) = F(x,y);

        take f;

        let a,b be Element of [. 0 , 1.];

        (f . (a,b)) = F(a,b) by A1;

        hence thesis by SUBSET_1:def 8, Max1In01;

      end;

      uniqueness

      proof

        let f1,f2 be BinOp of [. 0 , 1.] such that

         A1: for a,b be Element of [. 0 , 1.] holds (f1 . (a,b)) = ( max ((1 - a),b)) and

         A2: for a,b be Element of [. 0 , 1.] holds (f2 . (a,b)) = ( max ((1 - a),b));

        

         A3: ( dom f1) = [: [. 0 , 1.], [. 0 , 1.]:] by FUNCT_2:def 1

        .= ( dom f2) by FUNCT_2:def 1;

        for x,y be object st [x, y] in ( dom f1) holds (f1 . (x,y)) = (f2 . (x,y))

        proof

          let x,y be object;

          assume [x, y] in ( dom f1);

          then

          reconsider xx = x, yy = y as Element of [. 0 , 1.] by ZFMISC_1: 87;

          (f1 . (xx,yy)) = ( max ((1 - xx),yy)) by A1

          .= (f2 . (xx,yy)) by A2;

          hence thesis;

        end;

        hence thesis by A3, BINOP_1: 20;

      end;

    end

    registration

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

      coherence

      proof

        set f = Kleene-Dienes_implication ;

        

         a0: for x1,x2,y be Element of [. 0 , 1.] st x1 <= x2 holds (f . (x1,y)) >= (f . (x2,y))

        proof

          let x1,x2,y be Element of [. 0 , 1.];

          assume x1 <= x2;

          then ( - x2) <= ( - x1) by XREAL_1: 24;

          then (1 + ( - x2)) <= (1 + ( - x1)) by XREAL_1: 7;

          then ( max ((1 - x2),y)) <= ( max ((1 - x1),y)) by XXREAL_0: 26;

          then (f . (x2,y)) <= ( max ((1 - x1),y)) by Kleene;

          hence thesis by Kleene;

        end;

        

         aa: for x,y1,y2 be Element of [. 0 , 1.] st y1 <= y2 holds (f . (x,y1)) <= (f . (x,y2))

        proof

          let x,y1,y2 be Element of [. 0 , 1.];

          assume y1 <= y2;

          then ( max ((1 - x),y1)) <= ( max ((1 - x),y2)) by XXREAL_0: 26;

          then ( max ((1 - x),y1)) <= (f . (x,y2)) by Kleene;

          hence thesis by Kleene;

        end;

        

         AA: 0 in [. 0 , 1.] & 1 in [. 0 , 1.] by XXREAL_1: 1;

        

        then

         A1: (f . ( 0 , 0 )) = ( max ((1 - 0 ), 0 )) by Kleene

        .= 1 by XXREAL_0:def 10;

        

         A2: (f . (1,1)) = ( max ((1 - 1),1)) by AA, Kleene

        .= 1 by XXREAL_0:def 10;

        (f . (1, 0 )) = ( max ((1 - 1), 0 )) by AA, Kleene

        .= 0 ;

        hence thesis by A1, A2, a0, aa;

      end;

    end

    definition

      :: FUZIMPL1:def19

      func Goguen_implication -> BinOp of [. 0 , 1.] means

      : Goguen: for x,y be Element of [. 0 , 1.] holds (x <= y implies (it . (x,y)) = 1) & (x > y implies (it . (x,y)) = (y / x));

      existence

      proof

        set C = [. 0 , 1.];

        defpred P[ Real, Real] means $1 <= $2;

        deffunc F( Element of C, Element of C) = ( In (1,C));

        deffunc G( Element of C, Element of C) = ( In (($2 / $1),C));

        ex f be Function of [:C, C:], C st for c be Element of C, d be Element of C st [c, d] in ( dom f) holds ( P[c, d] implies (f . [c, d]) = F(c,d)) & ( not P[c, d] implies (f . [c, d]) = G(c,d)) from SCHEME1:sch 21;

        then

        consider f be Function of [:C, C:], C such that

         A1: for c be Element of C, d be Element of C st [c, d] in ( dom f) holds ( P[c, d] implies (f . [c, d]) = F(c,d)) & ( not P[c, d] implies (f . [c, d]) = G(c,d));

        take f;

        

         A0: ( dom f) = [:C, C:] by FUNCT_2:def 1;

        let a,b be Element of C;

        

         AA: [a, b] in ( dom f) by A0, ZFMISC_1: 87;

        (a <= b implies (f . (a,b)) = 1) & (a > b implies (f . (a,b)) = (b / a))

        proof

          thus a <= b implies (f . (a,b)) = 1

          proof

            assume a <= b;

            

            then (f . [a, b]) = F(a,b) by A1, AA

            .= 1 by SUBSET_1:def 8, XXREAL_1: 1;

            hence thesis;

          end;

          assume

           X0: a > b;

          

          then (f . [a, b]) = G(a,b) by A1, AA

          .= (b / a) by SUBSET_1:def 8, X0, QuoIn01;

          hence thesis;

        end;

        hence thesis;

      end;

      uniqueness

      proof

        let f1,f2 be BinOp of [. 0 , 1.] such that

         A1: for a,b be Element of [. 0 , 1.] holds (a <= b implies (f1 . (a,b)) = 1) & (a > b implies (f1 . (a,b)) = (b / a)) and

         A2: for a,b be Element of [. 0 , 1.] holds (a <= b implies (f2 . (a,b)) = 1) & (a > b implies (f2 . (a,b)) = (b / a));

        for a,b be set st a in [. 0 , 1.] & b in [. 0 , 1.] holds (f1 . (a,b)) = (f2 . (a,b))

        proof

          let a,b be set;

          assume a in [. 0 , 1.] & b in [. 0 , 1.];

          then

          reconsider aa = a, bb = b as Element of [. 0 , 1.];

          per cases ;

            suppose

             B0: aa <= bb;

            

            then (f1 . (aa,bb)) = 1 by A1

            .= (f2 . (aa,bb)) by A2, B0;

            hence thesis;

          end;

            suppose

             B1: aa > bb;

            

            then (f1 . (aa,bb)) = (bb / aa) by A1

            .= (f2 . (aa,bb)) by A2, B1;

            hence thesis;

          end;

        end;

        hence thesis by BINOP_1:def 21;

      end;

    end

    registration

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

      coherence

      proof

        set f = Goguen_implication ;

        

         a0: for x1,x2,y be Element of [. 0 , 1.] st x1 <= x2 holds (f . (x1,y)) >= (f . (x2,y))

        proof

          let x1,x2,y be Element of [. 0 , 1.];

          assume

           Z0: x1 <= x2;

          per cases ;

            suppose

             U1: x2 <= y;

            then x1 <= y by Z0, XXREAL_0: 2;

            then (f . (x1,y)) = 1 & (f . (x2,y)) = 1 by Goguen, U1;

            hence thesis;

          end;

            suppose x2 > y;

            then

             U2: (f . (x2,y)) = (y / x2) by Goguen;

            per cases ;

              suppose

               U5: x1 > y;

              then

               U3: (f . (x1,y)) = (y / x1) by Goguen;

              y >= 0 by XXREAL_1: 1;

              hence thesis by U2, U3, Z0, XREAL_1: 118, U5;

            end;

              suppose x1 <= y;

              then (f . (x1,y)) = 1 by Goguen;

              hence thesis by XXREAL_1: 1;

            end;

          end;

        end;

        

         aa: for x,y1,y2 be Element of [. 0 , 1.] st y1 <= y2 holds (f . (x,y1)) <= (f . (x,y2))

        proof

          let x,y1,y2 be Element of [. 0 , 1.];

          

           P1: x >= 0 by XXREAL_1: 1;

          assume

           Z2: y1 <= y2;

          per cases ;

            suppose

             P2: x <= y1;

            then x <= y2 by Z2, XXREAL_0: 2;

            then (f . (x,y1)) = 1 & (f . (x,y2)) = 1 by Goguen, P2;

            hence thesis;

          end;

            suppose x > y1;

            then

             P4: (f . (x,y1)) = (y1 / x) by Goguen;

            per cases ;

              suppose x <= y2;

              then (f . (x,y2)) = 1 by Goguen;

              hence thesis by XXREAL_1: 1;

            end;

              suppose x > y2;

              then (f . (x,y2)) = (y2 / x) by Goguen;

              hence thesis by P4, Z2, XREAL_1: 72, P1;

            end;

          end;

        end;

        

         AA: 0 in [. 0 , 1.] & 1 in [. 0 , 1.] by XXREAL_1: 1;

        (f . (1, 0 )) = ( 0 / 1) by AA, Goguen

        .= 0 ;

        hence thesis by a0, aa, AA, Goguen;

      end;

    end

    definition

      :: FUZIMPL1:def20

      func Rescher_implication -> BinOp of [. 0 , 1.] means

      : Rescher: for x,y be Element of [. 0 , 1.] holds (x <= y implies (it . (x,y)) = 1) & (x > y implies (it . (x,y)) = 0 );

      existence

      proof

        set C = [. 0 , 1.];

        defpred P[ Real, Real] means $1 <= $2;

        deffunc F( Element of C, Element of C) = ( In (1,C));

        deffunc G( Element of C, Element of C) = ( In ( 0 ,C));

        ex f be Function of [:C, C:], C st for c be Element of C, d be Element of C st [c, d] in ( dom f) holds ( P[c, d] implies (f . [c, d]) = F(c,d)) & ( not P[c, d] implies (f . [c, d]) = G(c,d)) from SCHEME1:sch 21;

        then

        consider f be Function of [:C, C:], C such that

         A1: for c be Element of C, d be Element of C st [c, d] in ( dom f) holds ( P[c, d] implies (f . [c, d]) = F(c,d)) & ( not P[c, d] implies (f . [c, d]) = G(c,d));

        take f;

        

         A0: ( dom f) = [:C, C:] by FUNCT_2:def 1;

        let a,b be Element of C;

        

         AA: [a, b] in ( dom f) by A0, ZFMISC_1: 87;

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

        proof

          thus a <= b implies (f . (a,b)) = 1

          proof

            assume a <= b;

            

            then (f . [a, b]) = F(a,b) by A1, AA

            .= 1 by SUBSET_1:def 8, XXREAL_1: 1;

            hence thesis;

          end;

          assume a > b;

          

          then (f . [a, b]) = G(a,b) by A1, AA

          .= 0 by XXREAL_1: 1, SUBSET_1:def 8;

          hence thesis;

        end;

        hence thesis;

      end;

      uniqueness

      proof

        let f1,f2 be BinOp of [. 0 , 1.] such that

         A1: for a,b be Element of [. 0 , 1.] holds (a <= b implies (f1 . (a,b)) = 1) & (a > b implies (f1 . (a,b)) = 0 ) and

         A2: for a,b be Element of [. 0 , 1.] holds (a <= b implies (f2 . (a,b)) = 1) & (a > b implies (f2 . (a,b)) = 0 );

        for a,b be set st a in [. 0 , 1.] & b in [. 0 , 1.] holds (f1 . (a,b)) = (f2 . (a,b))

        proof

          let a,b be set;

          assume a in [. 0 , 1.] & b in [. 0 , 1.];

          then

          reconsider aa = a, bb = b as Element of [. 0 , 1.];

          per cases ;

            suppose

             B0: aa <= bb;

            

            then (f1 . (aa,bb)) = 1 by A1

            .= (f2 . (aa,bb)) by A2, B0;

            hence thesis;

          end;

            suppose

             B1: aa > bb;

            

            then (f1 . (aa,bb)) = 0 by A1

            .= (f2 . (aa,bb)) by A2, B1;

            hence thesis;

          end;

        end;

        hence thesis by BINOP_1:def 21;

      end;

    end

    registration

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

      coherence

      proof

        set f = Rescher_implication ;

        

         b0: for x1,x2,y be Element of [. 0 , 1.] st x1 <= x2 holds (f . (x1,y)) >= (f . (x2,y))

        proof

          let x1,x2,y be Element of [. 0 , 1.];

          assume

           Z0: x1 <= x2;

          per cases ;

            suppose

             U1: x2 <= y;

            then x1 <= y by Z0, XXREAL_0: 2;

            then (f . (x1,y)) = 1 & (f . (x2,y)) = 1 by Rescher, U1;

            hence thesis;

          end;

            suppose x2 > y;

            then

             U2: (f . (x2,y)) = 0 by Rescher;

            thus thesis by U2, Rescher;

          end;

        end;

        

         ia: for x,y1,y2 be Element of [. 0 , 1.] st y1 <= y2 holds (f . (x,y1)) <= (f . (x,y2))

        proof

          let x,y1,y2 be Element of [. 0 , 1.];

          assume

           Z2: y1 <= y2;

          per cases ;

            suppose

             P2: x <= y1;

            then x <= y2 by Z2, XXREAL_0: 2;

            then (f . (x,y1)) = 1 & (f . (x,y2)) = 1 by Rescher, P2;

            hence thesis;

          end;

            suppose x > y1;

            then (f . (x,y1)) = 0 by Rescher;

            hence thesis by Rescher;

          end;

        end;

         0 in [. 0 , 1.] & 1 in [. 0 , 1.] by XXREAL_1: 1;

        hence thesis by b0, ia, Rescher;

      end;

    end

    definition

      :: FUZIMPL1:def21

      func Yager_implication -> BinOp of [. 0 , 1.] means

      : Yager: for x,y be Element of [. 0 , 1.] holds (x = y = 0 implies (it . (x,y)) = 1) & (x > 0 or y > 0 implies (it . (x,y)) = (y to_power x));

      existence

      proof

        set C = [. 0 , 1.];

        defpred P[ Real, Real] means $1 = $2 = 0 ;

        deffunc F( Element of C, Element of C) = ( In (1,C));

        deffunc G( Element of C, Element of C) = ( In (($2 to_power $1),C));

        ex f be Function of [:C, C:], C st for c be Element of C, d be Element of C st [c, d] in ( dom f) holds ( P[c, d] implies (f . [c, d]) = F(c,d)) & ( not P[c, d] implies (f . [c, d]) = G(c,d)) from SCHEME1:sch 21;

        then

        consider f be Function of [:C, C:], C such that

         A1: for c be Element of C, d be Element of C st [c, d] in ( dom f) holds ( P[c, d] implies (f . [c, d]) = F(c,d)) & ( not P[c, d] implies (f . [c, d]) = G(c,d));

        take f;

        

         A0: ( dom f) = [:C, C:] by FUNCT_2:def 1;

        let a,b be Element of C;

        

         AA: [a, b] in ( dom f) by A0, ZFMISC_1: 87;

        (a = b = 0 implies (f . (a,b)) = 1) & (a > 0 or b > 0 implies (f . (a,b)) = (b to_power a))

        proof

          thus a = b = 0 implies (f . (a,b)) = 1

          proof

            assume a = b = 0 ;

            

            then (f . [a, b]) = F(a,b) by A1, AA

            .= 1 by SUBSET_1:def 8, XXREAL_1: 1;

            hence thesis;

          end;

          assume

           X0: a > 0 or b > 0 ;

          then

           X1: (b to_power a) in C by PowerIn01;

           not P[a, b] by X0;

          

          then (f . [a, b]) = G(a,b) by A1, AA

          .= (b to_power a) by SUBSET_1:def 8, X1;

          hence thesis;

        end;

        hence thesis;

      end;

      uniqueness

      proof

        let f1,f2 be BinOp of [. 0 , 1.] such that

         A1: for a,b be Element of [. 0 , 1.] holds (a = b = 0 implies (f1 . (a,b)) = 1) & (a > 0 or b > 0 implies (f1 . (a,b)) = (b to_power a)) and

         A2: for a,b be Element of [. 0 , 1.] holds (a = b = 0 implies (f2 . (a,b)) = 1) & (a > 0 or b > 0 implies (f2 . (a,b)) = (b to_power a));

        for a,b be set st a in [. 0 , 1.] & b in [. 0 , 1.] holds (f1 . (a,b)) = (f2 . (a,b))

        proof

          let a,b be set;

          assume a in [. 0 , 1.] & b in [. 0 , 1.];

          then

          reconsider aa = a, bb = b as Element of [. 0 , 1.];

          aa > 0 or aa = 0 by XXREAL_1: 1;

          per cases by XXREAL_1: 1;

            suppose

             B0: aa = bb = 0 ;

            

            then (f1 . (aa,bb)) = 1 by A1

            .= (f2 . (aa,bb)) by A2, B0;

            hence thesis;

          end;

            suppose

             B1: aa > 0 or bb > 0 ;

            

            then (f1 . (aa,bb)) = (bb to_power aa) by A1

            .= (f2 . (aa,bb)) by A2, B1;

            hence thesis;

          end;

        end;

        hence thesis by BINOP_1:def 21;

      end;

    end

    registration

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

      coherence

      proof

        set f = Yager_implication ;

        

         ai: for x1,x2,y be Element of [. 0 , 1.] st x1 <= x2 holds (f . (x1,y)) >= (f . (x2,y))

        proof

          let x1,x2,y be Element of [. 0 , 1.];

          

           JI: 0 <= x1 & 0 <= x2 by XXREAL_1: 1;

          

           ZZ: 0 <= y <= 1 by XXREAL_1: 1;

          assume

           Z0: x1 <= x2;

          per cases ;

            suppose x2 = 0 & y = 0 ;

            hence thesis by JI, Z0;

          end;

            suppose x2 <> 0 & x1 = 0 & y = 0 ;

            then (f . (x1,y)) = 1 by Yager;

            hence thesis by XXREAL_1: 1;

          end;

            suppose

             U6: x2 <> 0 & x1 <> 0 & y = 0 ;

            then

             u6: x1 > 0 & x2 > 0 by XXREAL_1: 1;

            

             u2: (f . (x1,y)) = (y to_power x1) by Yager, U6, JI

            .= 0 by u6, U6, POWER:def 2;

            (f . (x2,y)) = (y to_power x2) by Yager, U6, JI

            .= 0 by JI, U6, POWER:def 2;

            hence thesis by u2;

          end;

            suppose

             za: y <> 0 ;

            then

             u2: (f . (x1,y)) = (y to_power x1) by ZZ, Yager;

            

             U2: (f . (x2,y)) = (y to_power x2) by Yager, za, ZZ;

            per cases ;

              suppose

               zz: x1 <> x2 & y <> 1;

               0 < y < 1 & x1 < x2 by zz, za, ZZ, Z0, XXREAL_0: 1;

              hence thesis by U2, u2, POWER: 40;

            end;

              suppose

               zz: x1 <> x2 & y = 1;

              1 >= (1 to_power x2) by POWER: 26;

              hence thesis by U2, u2, zz, POWER: 26;

            end;

              suppose x1 = x2;

              hence thesis;

            end;

          end;

        end;

        

         b0: for x,y1,y2 be Element of [. 0 , 1.] st y1 <= y2 holds (f . (x,y1)) <= (f . (x,y2))

        proof

          let x,y1,y2 be Element of [. 0 , 1.];

          assume

           Z2: y1 <= y2;

          per cases ;

            suppose

             P2: x = 0 & y2 = 0 ;

             0 <= y1 by XXREAL_1: 1;

            hence thesis by P2, Z2;

          end;

            suppose

             P8: x <> 0 ;

            

             su: x >= 0 & y2 >= 0 by XXREAL_1: 1;

            then

             P4: (f . (x,y2)) = (y2 to_power x) by Yager, P8;

            per cases ;

              suppose y1 = 0 & x = 0 ;

              hence thesis by P8;

            end;

              suppose y1 = 0 & x <> 0 ;

              then

               p4: (f . (x,y1)) = (y1 to_power x) by Yager, su;

              y1 >= 0 by XXREAL_1: 1;

              hence thesis by p4, P4, HOLDER_1: 3, Z2, su;

            end;

              suppose

               sy: y1 <> 0 ;

              y1 >= 0 by XXREAL_1: 1;

              then

               p4: (f . (x,y1)) = (y1 to_power x) by Yager, sy;

              y1 >= 0 by XXREAL_1: 1;

              hence thesis by p4, P4, HOLDER_1: 3, Z2, su;

            end;

          end;

            suppose

             P8: y2 <> 0 ;

            

             su: x >= 0 & y2 >= 0 by XXREAL_1: 1;

            then

             P4: (f . (x,y2)) = (y2 to_power x) by Yager, P8;

            per cases ;

              suppose

               pg: y1 = 0 & x = 0 ;

              then (f . (x,y1)) = 1 by Yager;

              hence thesis by P4, POWER: 24, pg;

            end;

              suppose y1 = 0 & x <> 0 ;

              then

               p4: (f . (x,y1)) = (y1 to_power x) by Yager, su;

              y1 >= 0 by XXREAL_1: 1;

              hence thesis by p4, P4, HOLDER_1: 3, Z2, su;

            end;

              suppose

               sy: y1 <> 0 ;

              y1 >= 0 by XXREAL_1: 1;

              then

               p4: (f . (x,y1)) = (y1 to_power x) by Yager, sy;

              y1 >= 0 by XXREAL_1: 1;

              hence thesis by p4, P4, HOLDER_1: 3, Z2, su;

            end;

          end;

        end;

        

         AA: 0 in [. 0 , 1.] & 1 in [. 0 , 1.] by XXREAL_1: 1;

        

         A2: (f . (1,1)) = (1 to_power 1) by AA, Yager

        .= 1 by POWER: 26;

        (f . (1, 0 )) = ( 0 to_power 1) by AA, Yager

        .= 0 by POWER:def 2;

        hence thesis by AA, A2, ai, b0, Yager;

      end;

    end

    definition

      :: FUZIMPL1:def22

      func Weber_implication -> BinOp of [. 0 , 1.] means

      : Weber: for x,y be Element of [. 0 , 1.] holds (x < 1 implies (it . (x,y)) = 1) & (x = 1 implies (it . (x,y)) = y);

      existence

      proof

        set C = [. 0 , 1.];

        defpred P[ Real, Real] means $1 < 1;

        deffunc F( Element of C, Element of C) = ( In (1,C));

        deffunc G( Element of C, Element of C) = ( In ($2,C));

        ex f be Function of [:C, C:], C st for c be Element of C, d be Element of C st [c, d] in ( dom f) holds ( P[c, d] implies (f . [c, d]) = F(c,d)) & ( not P[c, d] implies (f . [c, d]) = G(c,d)) from SCHEME1:sch 21;

        then

        consider f be Function of [:C, C:], C such that

         A1: for c be Element of C, d be Element of C st [c, d] in ( dom f) holds ( P[c, d] implies (f . [c, d]) = F(c,d)) & ( not P[c, d] implies (f . [c, d]) = G(c,d));

        take f;

        

         A0: ( dom f) = [:C, C:] by FUNCT_2:def 1;

        let a,b be Element of C;

        

         AA: [a, b] in ( dom f) by A0, ZFMISC_1: 87;

        (a < 1 implies (f . (a,b)) = 1) & (a = 1 implies (f . (a,b)) = b)

        proof

          thus a < 1 implies (f . (a,b)) = 1

          proof

            assume a < 1;

            

            then (f . [a, b]) = F(a,b) by A1, AA

            .= 1 by SUBSET_1:def 8, XXREAL_1: 1;

            hence thesis;

          end;

          assume

           X0: a = 1;

          (f . [a, b]) = G(a,b) by A1, AA, X0

          .= b by SUBSET_1:def 8;

          hence thesis;

        end;

        hence thesis;

      end;

      uniqueness

      proof

        let f1,f2 be BinOp of [. 0 , 1.] such that

         A1: for a,b be Element of [. 0 , 1.] holds (a < 1 implies (f1 . (a,b)) = 1) & (a = 1 implies (f1 . (a,b)) = b) and

         A2: for a,b be Element of [. 0 , 1.] holds (a < 1 implies (f2 . (a,b)) = 1) & (a = 1 implies (f2 . (a,b)) = b);

        for a,b be set st a in [. 0 , 1.] & b in [. 0 , 1.] holds (f1 . (a,b)) = (f2 . (a,b))

        proof

          let a,b be set;

          assume a in [. 0 , 1.] & b in [. 0 , 1.];

          then

          reconsider aa = a, bb = b as Element of [. 0 , 1.];

          aa <= 1 by XXREAL_1: 1;

          per cases by XXREAL_0: 1;

            suppose

             B0: aa < 1;

            

            then (f1 . (aa,bb)) = 1 by A1

            .= (f2 . (aa,bb)) by A2, B0;

            hence thesis;

          end;

            suppose

             B1: aa = 1;

            

            then (f1 . (aa,bb)) = bb by A1

            .= (f2 . (aa,bb)) by A2, B1;

            hence thesis;

          end;

        end;

        hence thesis by BINOP_1:def 21;

      end;

    end

    registration

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

      coherence

      proof

        set f = Weber_implication ;

        

         a0: for x1,x2,y be Element of [. 0 , 1.] st x1 <= x2 holds (f . (x1,y)) >= (f . (x2,y))

        proof

          let x1,x2,y be Element of [. 0 , 1.];

          assume

           Z0: x1 <= x2;

          per cases ;

            suppose

             U1: x2 < 1;

            then x1 < 1 by Z0, XXREAL_0: 2;

            then (f . (x1,y)) = 1 & (f . (x2,y)) = 1 by Weber, U1;

            hence thesis;

          end;

            suppose

             U6: x2 >= 1;

            x2 <= 1 by XXREAL_1: 1;

            then

             u2: x2 = 1 by XXREAL_0: 1, U6;

            per cases ;

              suppose x1 > y & x1 < 1;

              then (f . (x1,y)) = 1 by Weber;

              hence thesis by XXREAL_1: 1;

            end;

              suppose

               U5: x1 > y & x1 >= 1;

              x1 <= 1 by XXREAL_1: 1;

              hence thesis by u2, U5, XXREAL_0: 1;

            end;

              suppose x1 <= y & x1 < 1;

              then (f . (x1,y)) = 1 by Weber;

              hence thesis by XXREAL_1: 1;

            end;

              suppose

               IO: x1 <= y & x1 >= 1;

              x1 <= 1 by XXREAL_1: 1;

              hence thesis by u2, IO, XXREAL_0: 1;

            end;

          end;

        end;

        

         b0: for x,y1,y2 be Element of [. 0 , 1.] st y1 <= y2 holds (f . (x,y1)) <= (f . (x,y2))

        proof

          let x,y1,y2 be Element of [. 0 , 1.];

          

           P1: x >= 0 & x <= 1 by XXREAL_1: 1;

          assume

           Z2: y1 <= y2;

          per cases ;

            suppose x < 1;

            then (f . (x,y1)) = 1 & (f . (x,y2)) = 1 by Weber;

            hence thesis;

          end;

            suppose x >= 1;

            then

             SS: x = 1 by XXREAL_0: 1, P1;

            then (f . (x,y1)) = y1 by Weber;

            hence thesis by Z2, Weber, SS;

          end;

        end;

         0 in [. 0 , 1.] & 1 in [. 0 , 1.] by XXREAL_1: 1;

        hence thesis by a0, b0, Weber;

      end;

    end

    definition

      :: FUZIMPL1:def23

      func Fodor_implication -> BinOp of [. 0 , 1.] means

      : Fodor: for x,y be Element of [. 0 , 1.] holds (x <= y implies (it . (x,y)) = 1) & (x > y implies (it . (x,y)) = ( max ((1 - x),y)));

      existence

      proof

        set C = [. 0 , 1.];

        defpred P[ Real, Real] means $1 <= $2;

        deffunc F( Element of C, Element of C) = ( In (1,C));

        deffunc G( Element of C, Element of C) = ( In (( max ((1 - $1),$2)),C));

        ex f be Function of [:C, C:], C st for c be Element of C, d be Element of C st [c, d] in ( dom f) holds ( P[c, d] implies (f . [c, d]) = F(c,d)) & ( not P[c, d] implies (f . [c, d]) = G(c,d)) from SCHEME1:sch 21;

        then

        consider f be Function of [:C, C:], C such that

         A1: for c be Element of C, d be Element of C st [c, d] in ( dom f) holds ( P[c, d] implies (f . [c, d]) = F(c,d)) & ( not P[c, d] implies (f . [c, d]) = G(c,d));

        take f;

        

         A0: ( dom f) = [:C, C:] by FUNCT_2:def 1;

        let a,b be Element of C;

        

         AA: [a, b] in ( dom f) by A0, ZFMISC_1: 87;

        (a <= b implies (f . (a,b)) = 1) & (a > b implies (f . (a,b)) = ( max ((1 - a),b)))

        proof

          thus a <= b implies (f . (a,b)) = 1

          proof

            assume a <= b;

            

            then (f . [a, b]) = F(a,b) by A1, AA

            .= 1 by SUBSET_1:def 8, XXREAL_1: 1;

            hence thesis;

          end;

          assume a > b;

          

          then (f . [a, b]) = G(a,b) by A1, AA

          .= ( max ((1 - a),b)) by SUBSET_1:def 8, Max1In01;

          hence thesis;

        end;

        hence thesis;

      end;

      uniqueness

      proof

        let f1,f2 be BinOp of [. 0 , 1.] such that

         A1: for a,b be Element of [. 0 , 1.] holds (a <= b implies (f1 . (a,b)) = 1) & (a > b implies (f1 . (a,b)) = ( max ((1 - a),b))) and

         A2: for a,b be Element of [. 0 , 1.] holds (a <= b implies (f2 . (a,b)) = 1) & (a > b implies (f2 . (a,b)) = ( max ((1 - a),b)));

        for a,b be set st a in [. 0 , 1.] & b in [. 0 , 1.] holds (f1 . (a,b)) = (f2 . (a,b))

        proof

          let a,b be set;

          assume a in [. 0 , 1.] & b in [. 0 , 1.];

          then

          reconsider aa = a, bb = b as Element of [. 0 , 1.];

          per cases ;

            suppose

             B0: aa <= bb;

            

            then (f1 . (aa,bb)) = 1 by A1

            .= (f2 . (aa,bb)) by A2, B0;

            hence thesis;

          end;

            suppose

             B1: aa > bb;

            

            then (f1 . (aa,bb)) = ( max ((1 - aa),bb)) by A1

            .= (f2 . (aa,bb)) by A2, B1;

            hence thesis;

          end;

        end;

        hence thesis by BINOP_1:def 21;

      end;

    end

    registration

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

      coherence

      proof

        set f = Fodor_implication ;

        

         a0: for x1,x2,y be Element of [. 0 , 1.] st x1 <= x2 holds (f . (x1,y)) >= (f . (x2,y))

        proof

          let x1,x2,y be Element of [. 0 , 1.];

          assume

           Z0: x1 <= x2;

          per cases ;

            suppose

             U1: x2 <= y;

            then x1 <= y by Z0, XXREAL_0: 2;

            then (f . (x1,y)) = 1 & (f . (x2,y)) = 1 by Fodor, U1;

            hence thesis;

          end;

            suppose x2 > y;

            then

             U2: (f . (x2,y)) = ( max ((1 - x2),y)) by Fodor;

            per cases ;

              suppose x1 > y;

              then

               U3: (f . (x1,y)) = ( max ((1 - x1),y)) by Fodor;

              ( - x1) >= ( - x2) by Z0, XREAL_1: 24;

              then (1 + ( - x1)) >= (1 + ( - x2)) by XREAL_1: 7;

              hence thesis by U2, XXREAL_0: 26, U3;

            end;

              suppose x1 <= y;

              then (f . (x1,y)) = 1 by Fodor;

              hence thesis by XXREAL_1: 1;

            end;

          end;

        end;

        

         b0: for x,y1,y2 be Element of [. 0 , 1.] st y1 <= y2 holds (f . (x,y1)) <= (f . (x,y2))

        proof

          let x,y1,y2 be Element of [. 0 , 1.];

          assume

           Z2: y1 <= y2;

          per cases ;

            suppose

             P2: x <= y1;

            then x <= y2 by Z2, XXREAL_0: 2;

            then (f . (x,y1)) = 1 & (f . (x,y2)) = 1 by Fodor, P2;

            hence thesis;

          end;

            suppose x > y1;

            then

             P4: (f . (x,y1)) = ( max ((1 - x),y1)) by Fodor;

            per cases ;

              suppose x <= y2;

              then (f . (x,y2)) = 1 by Fodor;

              hence thesis by XXREAL_1: 1;

            end;

              suppose x > y2;

              then (f . (x,y2)) = ( max ((1 - x),y2)) by Fodor;

              hence thesis by P4, Z2, XXREAL_0: 26;

            end;

          end;

        end;

        

         AA: 0 in [. 0 , 1.] & 1 in [. 0 , 1.] by XXREAL_1: 1;

        

        then (f . (1, 0 )) = ( max ((1 - 1), 0 )) by Fodor

        .= 0 ;

        hence thesis by a0, b0, AA, Fodor;

      end;

    end

    begin

    definition

      :: FUZIMPL1:def24

      func I_{0} -> BinOp of [. 0 , 1.] means

      : I0Impl: for x,y be 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

      proof

        set C = [. 0 , 1.];

        defpred P[ Real, Real] means $1 = 0 or $2 = 1;

        deffunc F( Element of C, Element of C) = ( In (1,C));

        deffunc G( Element of C, Element of C) = ( In ( 0 ,C));

        ex f be Function of [:C, C:], C st for c be Element of C, d be Element of C st [c, d] in ( dom f) holds ( P[c, d] implies (f . [c, d]) = F(c,d)) & ( not P[c, d] implies (f . [c, d]) = G(c,d)) from SCHEME1:sch 21;

        then

        consider f be Function of [:C, C:], C such that

         A1: for c be Element of C, d be Element of C st [c, d] in ( dom f) holds ( P[c, d] implies (f . [c, d]) = F(c,d)) & ( not P[c, d] implies (f . [c, d]) = G(c,d));

        take f;

        

         A0: ( dom f) = [:C, C:] by FUNCT_2:def 1;

        let a,b be Element of C;

        

         AA: [a, b] in ( dom f) by A0, ZFMISC_1: 87;

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

        proof

          thus a = 0 or b = 1 implies (f . (a,b)) = 1

          proof

            assume a = 0 or b = 1;

            

            then (f . [a, b]) = F(a,b) by A1, AA

            .= 1 by SUBSET_1:def 8, XXREAL_1: 1;

            hence thesis;

          end;

          assume

           X0: a > 0 & b < 1;

          (f . [a, b]) = G(a,b) by A1, AA, X0

          .= 0 by SUBSET_1:def 8, XXREAL_1: 1;

          hence thesis;

        end;

        hence thesis;

      end;

      uniqueness

      proof

        let f1,f2 be BinOp of [. 0 , 1.] such that

         A1: for a,b be Element of [. 0 , 1.] holds (a = 0 or b = 1 implies (f1 . (a,b)) = 1) & (a > 0 & b < 1 implies (f1 . (a,b)) = 0 ) and

         A2: for a,b be Element of [. 0 , 1.] holds (a = 0 or b = 1 implies (f2 . (a,b)) = 1) & (a > 0 & b < 1 implies (f2 . (a,b)) = 0 );

        for a,b be set st a in [. 0 , 1.] & b in [. 0 , 1.] holds (f1 . (a,b)) = (f2 . (a,b))

        proof

          let a,b be set;

          assume a in [. 0 , 1.] & b in [. 0 , 1.];

          then

          reconsider aa = a, bb = b as Element of [. 0 , 1.];

          

           ST: 0 <= bb <= 1 by XXREAL_1: 1;

          per cases ;

            suppose

             B0: aa = 0 or bb = 1;

            

            then (f1 . (aa,bb)) = 1 by A1

            .= (f2 . (aa,bb)) by A2, B0;

            hence thesis;

          end;

            suppose aa <> 0 & bb <> 1;

            then

             B1: aa > 0 & bb < 1 by XXREAL_1: 1, ST, XXREAL_0: 1;

            

            then (f1 . (aa,bb)) = 0 by A1

            .= (f2 . (aa,bb)) by A2, B1;

            hence thesis;

          end;

        end;

        hence thesis by BINOP_1:def 21;

      end;

    end

    registration

      cluster I_{0} -> decreasing_on_1st increasing_on_2nd 00-dominant 11-dominant 10-weak;

      coherence

      proof

        set f = I_{0} ;

        

         b1: for x1,x2,y be Element of [. 0 , 1.] st x1 <= x2 holds (f . (x1,y)) >= (f . (x2,y))

        proof

          let x1,x2,y be Element of [. 0 , 1.];

          assume

           W0: x1 <= x2;

          per cases ;

            suppose x1 = 0 or y = 1;

            then (f . (x1,y)) = 1 by I0Impl;

            hence thesis by XXREAL_1: 1;

          end;

            suppose

             W1: x1 <> 0 & y <> 1;

            x1 >= 0 & y <= 1 by XXREAL_1: 1;

            then

             W2: x1 > 0 & y < 1 by W1, XXREAL_0: 1;

            then (f . (x1,y)) = 0 by I0Impl;

            hence thesis by I0Impl, W2, W0;

          end;

        end;

        

         b2: for x,y1,y2 be Element of [. 0 , 1.] st y1 <= y2 holds (f . (x,y1)) <= (f . (x,y2))

        proof

          let x,y1,y2 be Element of [. 0 , 1.];

          assume

           WW: y1 <= y2;

          per cases ;

            suppose y2 = 1 or x = 0 ;

            then (f . (x,y2)) = 1 by I0Impl;

            hence thesis by XXREAL_1: 1;

          end;

            suppose

             Ww: y2 <> 1 & x <> 0 ;

            

             wc: y2 <= 1 & x >= 0 by XXREAL_1: 1;

            then

             Wc: y2 < 1 & x > 0 by Ww, XXREAL_0: 1;

            then

             Wd: (f . (x,y2)) = 0 by I0Impl;

            y1 < 1 by WW, Wc, XXREAL_0: 2;

            hence thesis by Wd, wc, I0Impl, Ww;

          end;

        end;

         0 in [. 0 , 1.] & 1 in [. 0 , 1.] by XXREAL_1: 1;

        hence thesis by b1, b2, I0Impl;

      end;

    end

    definition

      :: FUZIMPL1:def25

      func I_{1} -> BinOp of [. 0 , 1.] means

      : I1Impl: for x,y be 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

      proof

        set C = [. 0 , 1.];

        defpred P[ Real, Real] means $1 < 1 or $2 > 0 ;

        deffunc F( Element of C, Element of C) = ( In (1,C));

        deffunc G( Element of C, Element of C) = ( In ( 0 ,C));

        ex f be Function of [:C, C:], C st for c be Element of C, d be Element of C st [c, d] in ( dom f) holds ( P[c, d] implies (f . [c, d]) = F(c,d)) & ( not P[c, d] implies (f . [c, d]) = G(c,d)) from SCHEME1:sch 21;

        then

        consider f be Function of [:C, C:], C such that

         A1: for c be Element of C, d be Element of C st [c, d] in ( dom f) holds ( P[c, d] implies (f . [c, d]) = F(c,d)) & ( not P[c, d] implies (f . [c, d]) = G(c,d));

        take f;

        

         A0: ( dom f) = [:C, C:] by FUNCT_2:def 1;

        let a,b be Element of C;

        

         AA: [a, b] in ( dom f) by A0, ZFMISC_1: 87;

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

        proof

          thus a < 1 or b > 0 implies (f . (a,b)) = 1

          proof

            assume a < 1 or b > 0 ;

            

            then (f . [a, b]) = F(a,b) by A1, AA

            .= 1 by SUBSET_1:def 8, XXREAL_1: 1;

            hence thesis;

          end;

          assume

           X0: a = 1 & b = 0 ;

          (f . [a, b]) = G(a,b) by A1, AA, X0

          .= 0 by SUBSET_1:def 8, XXREAL_1: 1;

          hence thesis;

        end;

        hence thesis;

      end;

      uniqueness

      proof

        let f1,f2 be BinOp of [. 0 , 1.] such that

         A1: for a,b be Element of [. 0 , 1.] holds (a < 1 or b > 0 implies (f1 . (a,b)) = 1) & (a = 1 & b = 0 implies (f1 . (a,b)) = 0 ) and

         A2: for a,b be Element of [. 0 , 1.] holds (a < 1 or b > 0 implies (f2 . (a,b)) = 1) & (a = 1 & b = 0 implies (f2 . (a,b)) = 0 );

        for a,b be set st a in [. 0 , 1.] & b in [. 0 , 1.] holds (f1 . (a,b)) = (f2 . (a,b))

        proof

          let a,b be set;

          assume a in [. 0 , 1.] & b in [. 0 , 1.];

          then

          reconsider aa = a, bb = b as Element of [. 0 , 1.];

          

           SS: 0 <= aa <= 1 by XXREAL_1: 1;

          per cases ;

            suppose

             B0: aa = 1 & bb = 0 ;

            

            then (f1 . (aa,bb)) = 0 by A1

            .= (f2 . (aa,bb)) by A2, B0;

            hence thesis;

          end;

            suppose aa <> 1 or bb <> 0 ;

            then

             B1: aa < 1 or bb > 0 by SS, XXREAL_1: 1, XXREAL_0: 1;

            

            then (f1 . (aa,bb)) = 1 by A1

            .= (f2 . (aa,bb)) by A2, B1;

            hence thesis;

          end;

        end;

        hence thesis by BINOP_1:def 21;

      end;

    end

    registration

      cluster I_{1} -> decreasing_on_1st increasing_on_2nd 00-dominant 11-dominant 10-weak;

      coherence

      proof

        set f = I_{1} ;

        

         b1: for x1,x2,y be Element of [. 0 , 1.] st x1 <= x2 holds (f . (x1,y)) >= (f . (x2,y))

        proof

          let x1,x2,y be Element of [. 0 , 1.];

          assume

           A0: x1 <= x2;

          per cases ;

            suppose x2 = 1 & y = 0 ;

            then (f . (x2,y)) = 0 by I1Impl;

            hence thesis by XXREAL_1: 1;

          end;

            suppose

             W1: x2 <> 1;

            x2 <= 1 by XXREAL_1: 1;

            then

             Y3: x2 < 1 by W1, XXREAL_0: 1;

            then

             Y2: (f . (x2,y)) = 1 by I1Impl;

            x1 < 1 by XXREAL_0: 2, A0, Y3;

            hence thesis by Y2, I1Impl;

          end;

            suppose

             W2: y <> 0 ;

            

             y4: y >= 0 by XXREAL_1: 1;

            (f . (x1,y)) = 1 by I1Impl, W2, y4;

            hence thesis by XXREAL_1: 1;

          end;

        end;

        

         b2: for x,y1,y2 be Element of [. 0 , 1.] st y1 <= y2 holds (f . (x,y1)) <= (f . (x,y2))

        proof

          let x,y1,y2 be Element of [. 0 , 1.];

          assume

           A0: y1 <= y2;

          per cases ;

            suppose y1 = 0 & x = 1;

            then (f . (x,y1)) = 0 by I1Impl;

            hence thesis by XXREAL_1: 1;

          end;

            suppose y1 <> 0 ;

            then

             A2: y1 > 0 by XXREAL_1: 1;

            then (f . (x,y1)) = 1 by I1Impl;

            hence thesis by I1Impl, A0, A2;

          end;

            suppose

             B1: x <> 1;

            x <= 1 by XXREAL_1: 1;

            then

             A2: x < 1 by B1, XXREAL_0: 1;

            then (f . (x,y1)) = 1 by I1Impl;

            hence thesis by A2, I1Impl;

          end;

        end;

         0 in [. 0 , 1.] & 1 in [. 0 , 1.] by XXREAL_1: 1;

        hence thesis by b1, b2, I1Impl;

      end;

    end

    definition

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

      :: FUZIMPL1:def26

      attr f is satisfying_(LB) means for y be Element of [. 0 , 1.] holds (f . ( 0 ,y)) = 1;

      :: FUZIMPL1:def27

      attr f is satisfying_(RB) means for x be Element of [. 0 , 1.] holds (f . (x,1)) = 1;

    end

    theorem :: FUZIMPL1:7

    

     LBProp: for fi be Fuzzy_Implication, y be Element of [. 0 , 1.] holds (fi . ( 0 ,y)) = 1

    proof

      let fi be Fuzzy_Implication, y be Element of [. 0 , 1.];

      

       A1: (fi . ( 0 , 0 )) = 1 by Def00;

      

       B1: 0 in [. 0 , 1.] by XXREAL_1: 1;

      reconsider z = 0 as Element of [. 0 , 1.] by XXREAL_1: 1;

       0 <= y by XXREAL_1: 1;

      then

       B2: (fi . ( 0 , 0 )) <= (fi . ( 0 ,y)) by DefIncr, B1;

      (fi . (z,y)) in [. 0 , 1.];

      then (fi . ( 0 ,y)) <= 1 by XXREAL_1: 1;

      hence thesis by XXREAL_0: 1, A1, B2;

    end;

    theorem :: FUZIMPL1:8

    

     RBProp: for fi be Fuzzy_Implication, x be Element of [. 0 , 1.] holds (fi . (x,1)) = 1

    proof

      let fi be Fuzzy_Implication, x be Element of [. 0 , 1.];

      

       A1: (fi . (1,1)) = 1 by Def11;

      

       B1: 1 in [. 0 , 1.] by XXREAL_1: 1;

      reconsider z = 1 as Element of [. 0 , 1.] by XXREAL_1: 1;

      x <= 1 by XXREAL_1: 1;

      then

       B2: (fi . (1,1)) <= (fi . (x,1)) by DefDecr, B1;

      (fi . (x,z)) in [. 0 , 1.];

      then (fi . (x,1)) <= 1 by XXREAL_1: 1;

      hence thesis by XXREAL_0: 1, A1, B2;

    end;

    registration

      cluster -> satisfying_(LB) satisfying_(RB) for Fuzzy_Implication;

      coherence by LBProp, RBProp;

    end

    theorem :: FUZIMPL1:9

    for fi be Fuzzy_Implication holds I_{0} <= fi

    proof

      let fi be Fuzzy_Implication;

      set f = I_{0} ;

      for x,y be Element of [. 0 , 1.] holds (f . (x,y)) <= (fi . (x,y))

      proof

        let x,y be Element of [. 0 , 1.];

        

         A0: x >= 0 & y <= 1 by XXREAL_1: 1;

        per cases ;

          suppose

           A1: x = 0 or y = 1;

          then (f . (x,y)) = 1 by LBProp, RBProp;

          hence thesis by LBProp, RBProp, A1;

        end;

          suppose x <> 0 & y <> 1;

          then x > 0 & y < 1 by A0, XXREAL_0: 1;

          then (f . (x,y)) = 0 by I0Impl;

          hence thesis by XXREAL_1: 1;

        end;

      end;

      hence thesis by FUZNORM1:def 16;

    end;

    theorem :: FUZIMPL1:10

    for fi be Fuzzy_Implication holds fi <= I_{1}

    proof

      let fi be Fuzzy_Implication;

      set f = I_{1} ;

      for x,y be Element of [. 0 , 1.] holds (f . (x,y)) >= (fi . (x,y))

      proof

        let x,y be Element of [. 0 , 1.];

        

         a0: x <= 1 & y >= 0 by XXREAL_1: 1;

        per cases ;

          suppose x <> 1 or y <> 0 ;

          then x < 1 or y > 0 by a0, XXREAL_0: 1;

          then (f . (x,y)) = 1 by I1Impl;

          hence thesis by XXREAL_1: 1;

        end;

          suppose

           Aa: x = 1 & y = 0 ;

          then (f . (x,y)) = 0 by I1Impl;

          hence thesis by Aa, Def10;

        end;

      end;

      hence thesis by FUZNORM1:def 16;

    end;