fuznorm1.miz



    begin

    registration

      cluster [. 0 , 1.] -> non empty;

      coherence by XXREAL_1: 1;

    end

    theorem :: FUZNORM1:1

    

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

    proof

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

      ( min (a,b)) = a or ( min (a,b)) = b by XXREAL_0: 15;

      hence thesis;

    end;

    theorem :: FUZNORM1:2

    

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

    proof

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

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

      hence thesis;

    end;

    theorem :: FUZNORM1:3

    

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

    proof

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

      

       A0: 1 >= a >= 0 & 1 >= b >= 0 by XXREAL_1: 1;

      then 1 >= (a * b) by XREAL_1: 160;

      hence thesis by XXREAL_1: 1, A0;

    end;

    theorem :: FUZNORM1:4

    

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

    proof

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

      

       A1: ( max ( 0 ,((a + b) - 1))) >= 0 by XXREAL_0: 25;

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

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

      then

       A2: ((a + b) - 1) <= (2 - 1) by XREAL_1: 9;

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

      hence thesis by A1, XXREAL_1: 1, A2;

    end;

    theorem :: FUZNORM1:5

    

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

    proof

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

      

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

      

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

      ( min (1,(a + b))) = 1 or ( min (1,(a + b))) = (a + b) by XXREAL_0: 15;

      hence thesis by A1, XXREAL_1: 1, A2;

    end;

    theorem :: FUZNORM1:6

    

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

    proof

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

      

       A1: 0 <= a & 0 <= b & 0 <= c by XXREAL_1: 1;

      

       zz: (c - 0 ) <= 1 by XXREAL_1: 1;

      then (c - 1) <= 0 by XREAL_1: 12;

      then

       y2: ((c - 1) + ((a + b) - 1)) <= ( 0 + ((a + b) - 1)) by XREAL_1: 6;

      per cases ;

        suppose

         Z0: 0 <= ((a + b) - 1) & 0 <= ((b + c) - 1);

        then

         Z1: ( max ( 0 ,((a + b) - 1))) = ((a + b) - 1) by XXREAL_0:def 10;

        ( max ( 0 ,((b + c) - 1))) = ((b + c) - 1) by Z0, XXREAL_0:def 10;

        hence thesis by Z1;

      end;

        suppose

         Z0: 0 > ((a + b) - 1) & 0 <= ((b + c) - 1);

        then

         Z1: ( max ( 0 ,((a + b) - 1))) = 0 by XXREAL_0:def 10;

        

         Z2: ( max ( 0 ,((b + c) - 1))) = ((b + c) - 1) by Z0, XXREAL_0:def 10;

        ( max ( 0 ,((( max ( 0 ,((a + b) - 1))) + c) - 1))) = 0 by zz, XXREAL_0:def 10, Z1, XREAL_1: 12

        .= ( max ( 0 ,((a + ( max ( 0 ,((b + c) - 1)))) - 1))) by Z2, y2, Z0, XXREAL_0:def 10;

        hence thesis;

      end;

        suppose

         Z0: 0 > ((a + b) - 1) & 0 > ((b + c) - 1);

        then

         Z3: (c - 1) < 0 & (a - 1) < 0 by XREAL_1: 9, A1, XREAL_1: 31;

        

         Z1: ( max ( 0 ,((a + b) - 1))) = 0 by Z0, XXREAL_0:def 10;

        

         Z2: ( max ( 0 ,((b + c) - 1))) = 0 by Z0, XXREAL_0:def 10;

        ( max ( 0 ,((( max ( 0 ,((a + b) - 1))) + c) - 1))) = 0 by Z3, XXREAL_0:def 10, Z1

        .= ( max ( 0 ,((a + ( max ( 0 ,((b + c) - 1)))) - 1))) by Z2, Z3, XXREAL_0:def 10;

        hence thesis;

      end;

        suppose

         Z0: 0 <= ((a + b) - 1) & 0 > ((b + c) - 1);

        

         ds: (a - 0 ) <= 1 by XXREAL_1: 1;

        then (a - 1) <= 0 by XREAL_1: 12;

        then

         sb: ((a - 1) + ((b + c) - 1)) <= ( 0 + 0 ) by Z0;

        

         Z1: ( max ( 0 ,((a + b) - 1))) = ((a + b) - 1) by Z0, XXREAL_0:def 10;

        ( max ( 0 ,((( max ( 0 ,((a + b) - 1))) + c) - 1))) = 0 by sb, XXREAL_0:def 10, Z1

        .= ( max ( 0 ,((a + 0 ) - 1))) by XXREAL_0:def 10, XREAL_1: 12, ds

        .= ( max ( 0 ,((a + ( max ( 0 ,((b + c) - 1)))) - 1))) by Z0, XXREAL_0:def 10;

        hence thesis;

      end;

    end;

    theorem :: FUZNORM1:7

    

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

    proof

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

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

      then (1 - 1) <= (1 - a) <= (1 - 0 ) by XREAL_1: 13;

      hence thesis by XXREAL_1: 1;

    end;

    theorem :: FUZNORM1:8

    

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

    proof

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

      

       S1: (1 - b) in [. 0 , 1.] by OpIn01;

      then (a * (1 - b)) in [. 0 , 1.] by Lemma1;

      then

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

      

       a0: b >= 0 by XXREAL_1: 1;

      

       S2: a <= 1 & b <= 1 by XXREAL_1: 1;

       0 <= (1 - b) <= 1 by S1, XXREAL_1: 1;

      then (a * (1 - b)) <= (1 * (1 - b)) by S2, XREAL_1: 64;

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

      hence thesis by XXREAL_1: 1, a0, B1;

    end;

    theorem :: FUZNORM1:9

    

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

    proof

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

      

       A1: (a * b) in [. 0 , 1.] by Lemma1;

      ((a + b) - (a * b)) in [. 0 , 1.] by abMinab01;

      then

       A2: ((a + b) - (a * b)) >= 0 by XXREAL_1: 1;

      

       T0: (a * b) >= 0 by A1, XXREAL_1: 1;

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

      then

       S1: (a * b) <= a by XREAL_1: 153;

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

      then (a * b) <= b by XREAL_1: 153;

      then ((a * b) + (a * b)) <= (a + b) by S1, XREAL_1: 7;

      then (a * b) <= ((a + b) - (a * b)) by XREAL_1: 19;

      then ((a * b) / ((a + b) - (a * b))) <= 1 by XREAL_1: 183, T0;

      hence thesis by T0, A2, XXREAL_1: 1;

    end;

    theorem :: FUZNORM1:10

    

     DiffMax: for a,b be Element of [. 0 , 1.] st ( max (a,b)) <> 1 holds a <> 1 & b <> 1

    proof

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

      assume

       A1: ( max (a,b)) <> 1;

      

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

      assume a = 1 or b = 1;

      per cases ;

        suppose a = 1;

        hence thesis by A1, A2, XXREAL_0:def 10;

      end;

        suppose b = 1;

        hence thesis by A1, A2, XXREAL_0:def 10;

      end;

    end;

    theorem :: FUZNORM1:11

    

     Lemacik: for x,y be Element of [. 0 , 1.] holds (x * y) = (x + y) implies x = 0

    proof

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

      assume (x * y) = (x + y);

      then

       z1: (y * (1 - x)) = ( - x);

      assume x <> 0 ;

      then 0 < x <= 1 by XXREAL_1: 1;

      then

       A4: ( - x) < ( - 0 ) by XREAL_1: 25;

      (1 - x) in [. 0 , 1.] by OpIn01;

      then

       A2: 0 <= (1 - x) & (1 - x) <= 1 by XXREAL_1: 1;

      y < 0 by A4, A2, z1;

      hence thesis by XXREAL_1: 1;

    end;

    theorem :: FUZNORM1:12

    

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

    proof

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

      per cases ;

        suppose

         A1: a <= b;

        then ( min ((1 - a),(1 - b))) = (1 - b) by XXREAL_0:def 9, XREAL_1: 10;

        hence thesis by A1, XXREAL_0:def 10;

      end;

        suppose

         A1: a > b;

        then ( min ((1 - a),(1 - b))) = (1 - a) by XXREAL_0:def 9, XREAL_1: 10;

        hence thesis by A1, XXREAL_0:def 10;

      end;

    end;

    theorem :: FUZNORM1:13

    

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

    proof

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

      per cases ;

        suppose

         A1: (a + b) <= 1;

        then

         A2: ((a + b) - (a + b)) <= (1 - (a + b)) by XREAL_1: 9;

        ( min ((a + b),1)) = (1 - ((1 - a) - b)) by A1, XXREAL_0:def 9

        .= (1 - ( max ( 0 ,(((1 - a) + (1 - b)) - 1)))) by A2, XXREAL_0:def 10;

        hence thesis;

      end;

        suppose

         A1: (a + b) > 1;

        then

         A2: ((a + b) - (a + b)) > (1 - (a + b)) by XREAL_1: 9;

        ( min ((a + b),1)) = (1 - 0 ) by A1, XXREAL_0:def 9

        .= (1 - ( max ( 0 ,(((1 - a) + (1 - b)) - 1)))) by A2, XXREAL_0:def 10;

        hence thesis;

      end;

    end;

    theorem :: FUZNORM1:14

    

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

    proof

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

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

      then

       S1: (a * b) <= a by XREAL_1: 153;

      

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

      then (a * b) <= b by XREAL_1: 153;

      then ((a * b) + (a * b)) <= (a + b) by S1, XREAL_1: 7;

      then

       S5: ((a * b) - (a * b)) <= (((a + b) - (a * b)) - (a * b)) by XREAL_1: 9, XREAL_1: 19;

      (1 - b) in [. 0 , 1.] by OpIn01;

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

      then (a * (1 - b)) <= (1 * (1 - b)) by S2, XREAL_1: 64;

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

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

      then

       B9: (((a + b) - ((2 * a) * b)) / (1 - (a * b))) <= 1 by XREAL_1: 183, S5;

      (a * b) in [. 0 , 1.] by Lemma1;

      then (a * b) <= 1 by XXREAL_1: 1;

      then (1 - (a * b)) >= (1 - 1) by XREAL_1: 10;

      hence thesis by XXREAL_1: 1, B9, S5;

    end;

    registration

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

      let a,b be Real;

      cluster (f . (a,b)) -> real;

      coherence

      proof

        per cases ;

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

          then (f . (a,b)) in [. 0 , 1.] by BINOP_1: 17;

          hence thesis;

        end;

          suppose not a in [. 0 , 1.] or not b in [. 0 , 1.];

          then not [a, b] in ( dom f) by ZFMISC_1: 87;

          hence thesis by FUNCT_1:def 2;

        end;

      end;

    end

    theorem :: FUZNORM1:15

    

     NormIn01: for a,b be Real, t be BinOp of [. 0 , 1.] holds (t . (a,b)) in [. 0 , 1.]

    proof

      let a,b be Real;

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

      per cases ;

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

        then [a, b] in [: [. 0 , 1.], [. 0 , 1.]:] by ZFMISC_1: 87;

        hence thesis by FUNCT_2: 5;

      end;

        suppose not a in [. 0 , 1.] or not b in [. 0 , 1.];

        then not [a, b] in ( dom t) by ZFMISC_1: 87;

        then (t . [a, b]) = 0 by FUNCT_1:def 2;

        hence thesis by XXREAL_1: 1;

      end;

    end;

    theorem :: FUZNORM1:16

    

     CoIn01: for f be BinOp of [. 0 , 1.], a,b be Real holds (1 - (f . ((1 - a),(1 - b)))) in [. 0 , 1.]

    proof

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

      let a,b be Real;

      per cases ;

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

        then

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

        (f . ((1 - aa),(1 - bb))) in [. 0 , 1.] by NormIn01;

        hence thesis by OpIn01;

      end;

        suppose not a in [. 0 , 1.] or not b in [. 0 , 1.];

        (f . ((1 - a),(1 - b))) in [. 0 , 1.] by NormIn01;

        hence thesis by OpIn01;

      end;

    end;

    theorem :: FUZNORM1:17

    

     MES57: for x,y,k be Real st k <= 0 holds (k * ( min (x,y))) = ( max ((k * x),(k * y))) & (k * ( max (x,y))) = ( min ((k * x),(k * y)))

    proof

      let x,y,k be Real;

      assume

       A1: k <= 0 ;

      hereby

        per cases by XXREAL_0: 16;

          suppose ( max (x,y)) = x;

          then

           A2: y <= x by XXREAL_0:def 10;

          then ( max ((k * x),(k * y))) = (k * y) by XXREAL_0:def 10, A1, XREAL_1: 65;

          hence (k * ( min (x,y))) = ( max ((k * x),(k * y))) by A2, XXREAL_0:def 9;

        end;

          suppose ( max (x,y)) = y;

          then

           A3: x <= y by XXREAL_0:def 10;

          then ( max ((k * x),(k * y))) = (k * x) by XXREAL_0:def 10, A1, XREAL_1: 65;

          hence (k * ( min (x,y))) = ( max ((k * x),(k * y))) by A3, XXREAL_0:def 9;

        end;

      end;

      per cases by XXREAL_0: 15;

        suppose ( min (x,y)) = x;

        then

         A4: x <= y by XXREAL_0:def 9;

        then ( min ((k * x),(k * y))) = (k * y) by XXREAL_0:def 9, A1, XREAL_1: 65;

        hence thesis by A4, XXREAL_0:def 10;

      end;

        suppose ( min (x,y)) = y;

        then

         A5: y <= x by XXREAL_0:def 9;

        then ( min ((k * y),(k * x))) = (k * x) by XXREAL_0:def 9, A1, XREAL_1: 65;

        hence thesis by A5, XXREAL_0:def 10;

      end;

    end;

    begin

    definition

      let A be real-membered set;

      let f be BinOp of A;

      :: FUZNORM1:def1

      attr f is monotonic means

      : MonDef: for a,b,c,d be Element of A st a <= c & b <= d holds (f . (a,b)) <= (f . (c,d));

      :: FUZNORM1:def2

      attr f is with-1-identity means

      : IdDef: for a be Element of A holds (f . (a,1)) = a;

      :: FUZNORM1:def3

      attr f is with-1-annihilating means for a be Element of A holds (f . (a,1)) = 1;

      :: FUZNORM1:def4

      attr f is with-0-identity means

      : ZeroDef: for a be Element of A holds (f . (a, 0 )) = a;

      :: FUZNORM1:def5

      attr f is with-0-annihilating means for a be Element of A holds (f . (a, 0 )) = 0 ;

    end

    scheme :: FUZNORM1:sch1

    ExBinOp { A() -> non empty real-membered set , F( Real, Real) -> set } :

ex f be BinOp of A() st for a,b be Element of A() holds (f . (a,b)) = F(a,b)

      provided

       A2: for a,b be Element of A() holds F(a,b) in A();

      set A = A();

      deffunc F( Element of A, Element of A) = ( In (F($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 A;

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

      hence thesis by SUBSET_1:def 8, A2;

    end;

    definition

      :: FUZNORM1:def6

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

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

      existence

      proof

        set A = [. 0 , 1.];

        deffunc F( Element of A, Element of A) = ( In (( 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;

        ( min (a,b)) = a or ( min (a,b)) = b by XXREAL_0: 15;

        hence thesis by A2, SUBSET_1:def 8;

      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 (a,b)) and

         A2: for a,b be Element of [. 0 , 1.] holds (f2 . (a,b)) = ( 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)) = ( min (xx,yy)) by A1

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

          hence thesis;

        end;

        hence thesis by A3, BINOP_1: 20;

      end;

    end

    registration

      cluster minnorm -> commutative associative monotonic with-1-identity;

      coherence

      proof

        set f = minnorm ;

        

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

        proof

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

          (f . (a,b)) = ( min (a,b)) by MinDef

          .= (f . (b,a)) by MinDef;

          hence thesis;

        end;

        

         AA: for a,b,c be Element of [. 0 , 1.] holds (f . ((f . (a,b)),c)) = (f . (a,(f . (b,c))))

        proof

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

          

           a2: ( min (a,b)) = a or ( min (a,b)) = b by XXREAL_0: 15;

          

           a3: ( min (b,c)) = b or ( min (b,c)) = c by XXREAL_0: 15;

          (f . ((f . (a,b)),c)) = (f . (( min (a,b)),c)) by MinDef

          .= ( min (( min (a,b)),c)) by MinDef, a2

          .= ( min (a,( min (b,c)))) by XXREAL_0: 33

          .= (f . (a,( min (b,c)))) by a3, MinDef

          .= (f . (a,(f . (b,c)))) by MinDef;

          hence thesis;

        end;

        

         D1: for a,b,c,d be Element of [. 0 , 1.] st a <= c & b <= d holds (f . (a,b)) <= (f . (c,d))

        proof

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

          assume a <= c & b <= d;

          then ( min (a,b)) <= ( min (c,d)) by XXREAL_0: 18;

          then ( min (a,b)) <= (f . (c,d)) by MinDef;

          hence thesis by MinDef;

        end;

        for a be Element of [. 0 , 1.] holds (f . (a,1)) = a

        proof

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

          

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

          a <= 1 by XXREAL_1: 1;

          then ( min (a,1)) = a by XXREAL_0:def 9;

          hence thesis by MinDef, T1;

        end;

        hence thesis by BINOP_1:def 2, BINOP_1:def 3, A1, AA, D1;

      end;

    end

    registration

      cluster commutative associative monotonic with-1-identity for BinOp of [. 0 , 1.];

      existence

      proof

        take minnorm ;

        thus thesis;

      end;

    end

    definition

      mode t-norm is commutative associative monotonic with-1-identity BinOp of [. 0 , 1.];

    end

    definition

      :: FUZNORM1:def7

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

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

      existence

      proof

        set A = [. 0 , 1.];

        deffunc F( Element of A, Element of A) = ( In (( max ($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 (a,b)) = a or ( max (a,b)) = b by XXREAL_0: 16;

        hence thesis by A2, SUBSET_1:def 8;

      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 (a,b)) and

         A2: for a,b be Element of [. 0 , 1.] holds (f2 . (a,b)) = ( max (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 (xx,yy)) by A1

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

          hence thesis;

        end;

        hence thesis by A3, BINOP_1: 20;

      end;

    end

    registration

      cluster maxnorm -> commutative associative monotonic with-0-identity;

      coherence

      proof

        set f = maxnorm ;

        

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

        proof

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

          (f . (a,b)) = ( max (a,b)) by MaxDef

          .= (f . (b,a)) by MaxDef;

          hence thesis;

        end;

        

         DD: for a,b,c be Element of [. 0 , 1.] holds (f . ((f . (a,b)),c)) = (f . (a,(f . (b,c))))

        proof

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

          

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

          

           a3: ( max (b,c)) = b or ( max (b,c)) = c by XXREAL_0: 16;

          (f . ((f . (a,b)),c)) = (f . (( max (a,b)),c)) by MaxDef

          .= ( max (( max (a,b)),c)) by MaxDef, a2

          .= ( max (a,( max (b,c)))) by XXREAL_0: 34

          .= (f . (a,( max (b,c)))) by a3, MaxDef

          .= (f . (a,(f . (b,c)))) by MaxDef;

          hence thesis;

        end;

        

         D1: for a,b,c,d be Element of [. 0 , 1.] st a <= c & b <= d holds (f . (a,b)) <= (f . (c,d))

        proof

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

          assume a <= c & b <= d;

          then ( max (a,b)) <= ( max (c,d)) by XXREAL_0: 26;

          then ( max (a,b)) <= (f . (c,d)) by MaxDef;

          hence thesis by MaxDef;

        end;

        for a be Element of [. 0 , 1.] holds (f . (a, 0 )) = a

        proof

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

          

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

          a >= 0 by XXREAL_1: 1;

          then ( max (a, 0 )) = a by XXREAL_0:def 10;

          hence thesis by MaxDef, T1;

        end;

        hence thesis by BINOP_1:def 2, BINOP_1:def 3, A1, DD, D1;

      end;

    end

    registration

      cluster commutative associative monotonic with-0-identity for BinOp of [. 0 , 1.];

      existence

      proof

        take maxnorm ;

        thus thesis;

      end;

    end

    definition

      mode t-conorm is commutative associative monotonic with-0-identity BinOp of [. 0 , 1.];

    end

    theorem :: FUZNORM1:18

    

     NormIs0: for t be commutative monotonic with-1-identity BinOp of [. 0 , 1.] holds for a be Element of [. 0 , 1.] holds (t . (a, 0 )) = 0

    proof

      let t be commutative monotonic with-1-identity BinOp of [. 0 , 1.];

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

      

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

      

      then

       T3: (t . (1, 0 )) = (t . ( 0 ,1)) by BINOP_1:def 2

      .= 0 by T0, IdDef;

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

      proof

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

        (t . (a, 0 )) in [. 0 , 1.] by NormIn01;

        then

         T4: 0 <= (t . (a, 0 )) by XXREAL_1: 1;

        a <= 1 by XXREAL_1: 1;

        hence thesis by T4, T0, MonDef, T3;

      end;

      hence thesis;

    end;

    theorem :: FUZNORM1:19

    

     ConormIs1: for t be commutative monotonic with-0-identity BinOp of [. 0 , 1.] holds for a be Element of [. 0 , 1.] holds (t . (a,1)) = 1

    proof

      let t be commutative monotonic with-0-identity BinOp of [. 0 , 1.];

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

      

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

      

      then

       T3: (t . ( 0 ,1)) = (t . (1, 0 )) by BINOP_1:def 2

      .= 1 by T0, ZeroDef;

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

      proof

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

        (t . (a,1)) in [. 0 , 1.] by NormIn01;

        then

         T4: (t . (a,1)) <= 1 by XXREAL_1: 1;

         0 <= a by XXREAL_1: 1;

        then 1 <= (t . (a,1)) by T0, MonDef, T3;

        hence thesis by XXREAL_0: 1, T4;

      end;

      hence thesis;

    end;

    registration

      cluster -> with-0-annihilating for commutative monotonic with-1-identity BinOp of [. 0 , 1.];

      coherence by NormIs0;

      cluster -> with-1-annihilating for commutative monotonic with-0-identity BinOp of [. 0 , 1.];

      coherence by ConormIs1;

    end

    begin

    definition

      :: FUZNORM1:def8

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

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

      existence

      proof

        set A = [. 0 , 1.];

        deffunc F( Element of A, Element of A) = ( In (($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, Lemma1;

      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)) = (a * b) and

         A2: for a,b be Element of [. 0 , 1.] holds (f2 . (a,b)) = (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)) = (xx * yy) by A1

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

          hence thesis;

        end;

        hence thesis by A3, BINOP_1: 20;

      end;

    end

    registration

      cluster prodnorm -> commutative associative monotonic with-1-identity;

      coherence

      proof

        set f = prodnorm ;

        

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

        proof

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

          (f . (a,b)) = (a * b) by ProdDef

          .= (f . (b,a)) by ProdDef;

          hence thesis;

        end;

        

         C1: for a,b,c be Element of [. 0 , 1.] holds (f . ((f . (a,b)),c)) = (f . (a,(f . (b,c))))

        proof

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

          

           A2: (a * b) in [. 0 , 1.] by Lemma1;

          

           A3: (b * c) in [. 0 , 1.] by Lemma1;

          (f . ((f . (a,b)),c)) = (f . ((a * b),c)) by ProdDef

          .= ((a * b) * c) by ProdDef, A2

          .= (a * (b * c))

          .= (f . (a,(b * c))) by A3, ProdDef

          .= (f . (a,(f . (b,c)))) by ProdDef;

          hence thesis;

        end;

        

         D1: for a,b,c,d be Element of [. 0 , 1.] st a <= c & b <= d holds (f . (a,b)) <= (f . (c,d))

        proof

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

          

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

          assume a <= c & b <= d;

          then (a * b) <= (c * d) by B1, XREAL_1: 66;

          then (a * b) <= (f . (c,d)) by ProdDef;

          hence thesis by ProdDef;

        end;

        

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

        for a be Element of [. 0 , 1.] holds (f . (a,1)) = a

        proof

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

          (a * 1) = a;

          hence thesis by ProdDef, T1;

        end;

        hence thesis by BINOP_1:def 2, BINOP_1:def 3, A1, C1, D1;

      end;

    end

    definition

      :: FUZNORM1:def9

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

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

      existence

      proof

        set A = [. 0 , 1.];

        deffunc F( Element of A, Element of A) = ( In ((($1 + $2) - ($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, abMinab01;

      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)) = ((a + b) - (a * b)) and

         A2: for a,b be Element of [. 0 , 1.] holds (f2 . (a,b)) = ((a + b) - (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)) = ((xx + yy) - (xx * yy)) by A1

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

          hence thesis;

        end;

        hence thesis by A3, BINOP_1: 20;

      end;

    end

    definition

      :: FUZNORM1:def10

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

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

      existence

      proof

        set A = [. 0 , 1.];

        deffunc F( Element of A, Element of A) = ( In (( max ( 0 ,(($1 + $2) - 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.];

        reconsider aa = a, bb = b as Element of A;

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

        hence thesis by SUBSET_1:def 8, Lemma2;

      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 ( 0 ,((a + b) - 1))) and

         A2: for a,b be Element of [. 0 , 1.] holds (f2 . (a,b)) = ( max ( 0 ,((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)) = ( max ( 0 ,((xx + yy) - 1))) by A1

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

          hence thesis;

        end;

        hence thesis by A3, BINOP_1: 20;

      end;

    end

    registration

      cluster Lukasiewicz_norm -> commutative associative monotonic with-1-identity;

      coherence

      proof

        set f = Lukasiewicz_norm ;

        

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

        proof

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

          (f . (a,b)) = ( max ( 0 ,((a + b) - 1))) by LukNorm

          .= (f . (b,a)) by LukNorm;

          hence thesis;

        end;

        

         C1: for a,b,c be Element of [. 0 , 1.] holds (f . ((f . (a,b)),c)) = (f . (a,(f . (b,c))))

        proof

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

          set B = ( max ( 0 ,((a + b) - 1)));

          set C = ( max ( 0 ,((b + c) - 1)));

          

           G1: B in [. 0 , 1.] by Lemma2;

          

           G2: C in [. 0 , 1.] by Lemma2;

          (f . ((f . (a,b)),c)) = (f . (B,c)) by LukNorm

          .= ( max ( 0 ,((B + c) - 1))) by LukNorm, G1

          .= ( max ( 0 ,((a + C) - 1))) by Lemma3

          .= (f . (a,C)) by LukNorm, G2

          .= (f . (a,(f . (b,c)))) by LukNorm;

          hence thesis;

        end;

        

         D1: for a,b,c,d be Element of [. 0 , 1.] st a <= c & b <= d holds (f . (a,b)) <= (f . (c,d))

        proof

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

          assume a <= c & b <= d;

          then (a + b) <= (c + d) by XREAL_1: 7;

          then ((a + b) - 1) <= ((c + d) - 1) by XREAL_1: 9;

          then ( max ( 0 ,((a + b) - 1))) <= ( max ( 0 ,((c + d) - 1))) by XXREAL_0: 26;

          then ( max ( 0 ,((a + b) - 1))) <= (f . (c,d)) by LukNorm;

          hence thesis by LukNorm;

        end;

        for a be Element of [. 0 , 1.] holds (f . (a,1)) = a

        proof

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

          

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

          

           T2: 0 <= a by XXREAL_1: 1;

          (f . (a,1)) = ( max ( 0 ,((a + 1) - 1))) by LukNorm, T1

          .= a by T2, XXREAL_0:def 10;

          hence thesis;

        end;

        hence thesis by BINOP_1:def 2, BINOP_1:def 3, A1, C1, D1;

      end;

    end

    definition

      :: FUZNORM1:def11

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

      : Drastic2Def: for a,b be Element of [. 0 , 1.] holds (( max (a,b)) = 1 implies (it . (a,b)) = ( min (a,b))) & (( max (a,b)) <> 1 implies (it . (a,b)) = 0 );

      existence

      proof

        set C = [. 0 , 1.];

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

        deffunc F( Element of C, Element of C) = ( In (( min ($1,$2)),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;

        

         cc: ( min (a,b)) = a or ( min (a,b)) = b by XXREAL_0: 15;

        

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

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

        proof

          thus ( max (a,b)) = 1 implies (f . (a,b)) = ( min (a,b))

          proof

            assume ( max (a,b)) = 1;

            then a = 1 or b = 1 by XXREAL_0: 16;

            

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

            .= ( min (a,b)) by SUBSET_1:def 8, cc;

            hence thesis;

          end;

          assume

           B0: ( max (a,b)) <> 1;

          a <> 1 & b <> 1

          proof

            assume a = 1 or b = 1;

            per cases ;

              suppose

               Z1: a = 1;

              then b <= a by XXREAL_1: 1;

              hence thesis by B0, XXREAL_0:def 10, Z1;

            end;

              suppose

               Z1: b = 1;

              then a <= b by XXREAL_1: 1;

              hence thesis by B0, XXREAL_0:def 10, Z1;

            end;

          end;

          

          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 (( max (a,b)) = 1 implies (f1 . (a,b)) = ( min (a,b))) & (( max (a,b)) <> 1 implies (f1 . (a,b)) = 0 ) and

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

          per cases ;

            suppose

             B0: ( max (aa,bb)) = 1;

            

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

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

            hence thesis;

          end;

            suppose

             B1: ( max (aa,bb)) <> 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

    theorem :: FUZNORM1:20

    

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

    proof

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

      

       A1: b <= 1 & a <= 1 by XXREAL_1: 1;

      thus a = 1 implies ( drastic_norm . (a,b)) = b

      proof

        assume

         B1: a = 1;

        then ( max (a,b)) = 1 by A1, XXREAL_0:def 10;

        

        then ( drastic_norm . (a,b)) = ( min (a,b)) by Drastic2Def

        .= b by XXREAL_0:def 9, A1, B1;

        hence thesis;

      end;

      thus b = 1 implies ( drastic_norm . (a,b)) = a

      proof

        assume

         B1: b = 1;

        then ( max (a,b)) = 1 by A1, XXREAL_0:def 10;

        

        then ( drastic_norm . (a,b)) = ( min (a,b)) by Drastic2Def

        .= a by XXREAL_0:def 9, A1, B1;

        hence thesis;

      end;

      assume a <> 1 & b <> 1;

      then ( max (a,b)) <> 1 by XXREAL_0: 16;

      hence thesis by Drastic2Def;

    end;

    registration

      cluster drastic_norm -> commutative associative with-1-identity monotonic;

      coherence

      proof

        set f = drastic_norm ;

        

         FF: for a,b be Element of [. 0 , 1.] holds (f . (a,b)) = (f . (b,a))

        proof

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

          per cases ;

            suppose

             A1: a = 1;

            then (f . (a,b)) = b by DrasticDef;

            hence thesis by A1, DrasticDef;

          end;

            suppose

             A1: b = 1;

            then (f . (b,a)) = a by DrasticDef;

            hence thesis by A1, DrasticDef;

          end;

            suppose a <> 1 & b <> 1;

            then (f . (a,b)) = 0 & (f . (b,a)) = 0 by DrasticDef;

            hence thesis;

          end;

        end;

        

         TT: for a be Element of [. 0 , 1.] holds (f . (a,1)) = a

        proof

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

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

          hence thesis by DrasticDef;

        end;

        

         D1: for a,b,c,d be Element of [. 0 , 1.] st a <= c & b <= d holds (f . (a,b)) <= (f . (c,d))

        proof

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

          

           B2: (f . (c,d)) >= 0 by XXREAL_1: 1;

          assume

           S1: a <= c & b <= d;

          per cases ;

            suppose

             S0: a = 1;

            c <= 1 by XXREAL_1: 1;

            then (f . (c,d)) = d by DrasticDef, S0, S1, XXREAL_0: 1;

            hence thesis by S1, DrasticDef, S0;

          end;

            suppose

             S0: b = 1;

            d <= 1 by XXREAL_1: 1;

            then (f . (c,d)) = c by DrasticDef, S0, S1, XXREAL_0: 1;

            hence thesis by S1, DrasticDef, S0;

          end;

            suppose b <> 1 & a <> 1;

            hence thesis by B2, DrasticDef;

          end;

        end;

        

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

        

         BU: for a be Element of [. 0 , 1.] holds (f . (a, 0 )) = 0

        proof

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

          

           H2: 0 <= a by XXREAL_1: 1;

          per cases ;

            suppose ( max (a, 0 )) = 1;

            

            then (f . (a, 0 )) = ( min (a, 0 )) by Drastic2Def, H1

            .= 0 by H2, XXREAL_0:def 9;

            hence thesis;

          end;

            suppose ( max (a, 0 )) <> 1;

            hence thesis by Drastic2Def, H1;

          end;

        end;

        for a,b,c be Element of [. 0 , 1.] holds (f . (a,(f . (b,c)))) = (f . ((f . (a,b)),c))

        proof

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

          

           Z4: ( min (a,b)) in [. 0 , 1.] by MinIn01;

          

           EE: ( min (b,c)) in [. 0 , 1.] by MinIn01;

          per cases ;

            suppose

             Z1: ( max (a,b)) = 1 & ( max (b,c)) = 1;

            then

             K1: a = 1 or b = 1 by XXREAL_0: 16;

            ( max (a,c)) in [. 0 , 1.] by MaxIn01;

            then

             U2: ( max (a,c)) <= 1 by XXREAL_1: 1;

            

             Z2: (f . (b,c)) = ( min (b,c)) by Drastic2Def, Z1;

            

             UU: ( max (a,( min (b,c)))) = ( min (( max (a,b)),( max (a,c)))) by XXREAL_0: 39

            .= ( max (a,c)) by U2, XXREAL_0:def 9, Z1;

            per cases ;

              suppose

               HU: ( max (a,c)) = 1;

              

               U2: ( max (( min (a,b)),c)) = ( min (( max (a,c)),( max (b,c)))) by XXREAL_0: 39

              .= 1 by Z1, HU;

              (f . (a,(f . (b,c)))) = (f . (a,( min (b,c)))) by Drastic2Def, Z1

              .= ( min (a,( min (b,c)))) by Drastic2Def, HU, UU, EE

              .= ( min (( min (a,b)),c)) by XXREAL_0: 33

              .= (f . (( min (a,b)),c)) by U2, Drastic2Def, Z4

              .= (f . ((f . (a,b)),c)) by Drastic2Def, Z1;

              hence thesis;

            end;

              suppose

               HU: ( max (a,c)) <> 1;

              then a <= b by XXREAL_1: 1, K1, DiffMax;

              then

               K3: ( min (a,b)) = a by XXREAL_0:def 9;

              

               U1: (f . (a,b)) = ( min (a,b)) by Drastic2Def, Z1;

              (f . (a,(f . (b,c)))) = 0 by Drastic2Def, HU, UU, Z2

              .= (f . ((f . (a,b)),c)) by U1, K3, HU, Drastic2Def;

              hence thesis;

            end;

          end;

            suppose

             Z1: ( max (a,b)) = 1 & ( max (b,c)) <> 1;

            then

             z1: a = 1 or b = 1 by XXREAL_0: 16;

            ( max (b,c)) in [. 0 , 1.] by MaxIn01;

            then

             W1: ( max (b,c)) <= 1 by XXREAL_1: 1;

            

             za: b <> 1

            proof

              assume b = 1;

              then ( max (b,c)) >= 1 by XXREAL_0: 25;

              hence thesis by Z1, XXREAL_0: 1, W1;

            end;

            c <= 1 by XXREAL_1: 1;

            then

             z3: ( max (a,c)) = 1 by z1, za, XXREAL_0:def 10;

            

             qq: ( max (( min (a,b)),c)) = ( min (( max (a,c)),( max (b,c)))) by XXREAL_0: 39

            .= ( max (b,c)) by W1, z3, XXREAL_0:def 9;

            (f . (b,c)) = 0 by Drastic2Def, Z1;

            

            then (f . (a,(f . (b,c)))) = 0 by BU

            .= (f . (( min (a,b)),c)) by qq, Z1, Drastic2Def, Z4

            .= (f . ((f . (a,b)),c)) by Drastic2Def, Z1;

            hence thesis;

          end;

            suppose

             Z1: ( max (a,b)) <> 1 & ( max (b,c)) = 1;

            then

             z1: c = 1 or b = 1 by XXREAL_0: 16;

            ( max (a,b)) in [. 0 , 1.] by MaxIn01;

            then

             w1: ( max (a,b)) <= 1 by XXREAL_1: 1;

            

             zz: b <> 1

            proof

              assume b = 1;

              then ( max (a,b)) >= 1 by XXREAL_0: 25;

              hence thesis by Z1, w1, XXREAL_0: 1;

            end;

            

             Z2: (f . (b,c)) = ( min (b,c)) by Drastic2Def, Z1;

            

             Y1: (f . (a,b)) = 0 by Drastic2Def, Z1;

            b <= c by XXREAL_1: 1, zz, z1;

            then (f . (b,c)) = b by Z2, XXREAL_0:def 9;

            

            then (f . (a,(f . (b,c)))) = 0 by Drastic2Def, Z1

            .= (f . (c, 0 )) by BU

            .= (f . ((f . (a,b)),c)) by Y1, FF;

            hence thesis;

          end;

            suppose

             Z1: ( max (a,b)) <> 1 & ( max (b,c)) <> 1;

            then

             Z2: (f . (b,c)) = 0 by Drastic2Def;

            

             Z3: (f . (a,b)) = 0 by Drastic2Def, Z1;

            (f . (a,(f . (b,c)))) = 0 by BU, Z2

            .= (f . (c, 0 )) by BU

            .= (f . ((f . (a,b)),c)) by Z3, FF;

            hence thesis;

          end;

        end;

        hence thesis by FF, TT, D1, BINOP_1:def 3, BINOP_1:def 2;

      end;

    end

    definition

      :: FUZNORM1:def12

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

      : NilminDef: for a,b be Element of [. 0 , 1.] holds ((a + b) > 1 implies (it . (a,b)) = ( min (a,b))) & ((a + b) <= 1 implies (it . (a,b)) = 0 );

      existence

      proof

        set C = [. 0 , 1.];

        defpred P[ Real, Real] means ($1 + $2) > 1;

        deffunc F( Element of C, Element of C) = ( In (( min ($1,$2)),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;

        

         cc: ( min (a,b)) = a or ( min (a,b)) = b by XXREAL_0: 15;

        

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

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

        proof

          thus (a + b) > 1 implies (f . (a,b)) = ( min (a,b))

          proof

            assume (a + b) > 1;

            

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

            .= ( min (a,b)) by SUBSET_1:def 8, cc;

            hence thesis;

          end;

          assume (a + b) <= 1;

          

          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) > 1 implies (f1 . (a,b)) = ( min (a,b))) & ((a + b) <= 1 implies (f1 . (a,b)) = 0 ) and

         A2: for a,b be Element of [. 0 , 1.] holds ((a + b) > 1 implies (f2 . (a,b)) = ( min (a,b))) & ((a + 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.];

          per cases ;

            suppose

             B0: (aa + bb) > 1;

            

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

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

            hence thesis;

          end;

            suppose

             B1: (aa + bb) <= 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 nilmin_norm -> commutative associative with-1-identity monotonic;

      coherence

      proof

        set f = nilmin_norm ;

        

         FF: for a,b be Element of [. 0 , 1.] holds (f . (a,b)) = (f . (b,a))

        proof

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

          per cases ;

            suppose

             A1: (a + b) > 1;

            

            hence (f . (a,b)) = ( min (a,b)) by NilminDef

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

          end;

            suppose (a + b) <= 1;

            then (f . (a,b)) = 0 & (f . (b,a)) = 0 by NilminDef;

            hence thesis;

          end;

        end;

        

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

        

         TT: for a be Element of [. 0 , 1.] holds (f . (a,1)) = a

        proof

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

          

           U4: 0 <= a <= 1 by XXREAL_1: 1;

          per cases ;

            suppose (a + 1) > 1;

            

            then (f . (a,1)) = ( min (a,1)) by NilminDef, U1

            .= a by U4, XXREAL_0:def 9;

            hence thesis;

          end;

            suppose

             U2: (a + 1) <= 1;

            then a <= (1 - 1) by XREAL_1: 19;

            then a = 0 by XXREAL_1: 1;

            hence thesis by NilminDef, U2, U1;

          end;

        end;

        

         D1: for a,b,c,d be Element of [. 0 , 1.] st a <= c & b <= d holds (f . (a,b)) <= (f . (c,d))

        proof

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

          assume

           S1: a <= c & b <= d;

          per cases ;

            suppose

             S0: (a + b) > 1;

            then

             Sa: (f . (a,b)) = ( min (a,b)) by NilminDef;

            (a + b) <= (c + d) by S1, XREAL_1: 7;

            then (c + d) > 1 by S0, XXREAL_0: 2;

            then (f . (c,d)) = ( min (c,d)) by NilminDef;

            hence thesis by S1, Sa, XXREAL_0: 18;

          end;

            suppose (a + b) <= 1;

            then (f . (a,b)) = 0 by NilminDef;

            hence thesis by XXREAL_1: 1;

          end;

        end;

        

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

        

         BU: for a be Element of [. 0 , 1.] holds (f . (a, 0 )) = 0

        proof

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

          per cases ;

            suppose (a + 0 ) > 1;

            hence thesis by XXREAL_1: 1;

          end;

            suppose (a + 0 ) <= 1;

            hence thesis by NilminDef, H1;

          end;

        end;

        for a,b,c be Element of [. 0 , 1.] holds (f . (a,(f . (b,c)))) = (f . ((f . (a,b)),c))

        proof

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

          

           EE: ( min (b,c)) in [. 0 , 1.] by MinIn01;

          

           U3: ( min (a,b)) in [. 0 , 1.] by MinIn01;

          per cases ;

            suppose

             Z1: (a + b) > 1 & (b + c) > 1;

            then

             Z2: (f . (b,c)) = ( min (b,c)) by NilminDef;

            per cases ;

              suppose

               HU: (a + c) > 1;

              then

               W6: (a + ( min (b,c))) > 1 by Z1, XXREAL_0: 15;

              

               W7: (c + ( min (a,b))) > 1 by HU, Z1, XXREAL_0: 15;

              (f . (a,(f . (b,c)))) = (f . (a,( min (b,c)))) by Z1, NilminDef

              .= ( min (a,( min (b,c)))) by NilminDef, EE, W6

              .= ( min (( min (a,b)),c)) by XXREAL_0: 33

              .= (f . (( min (a,b)),c)) by NilminDef, U3, W7

              .= (f . ((f . (a,b)),c)) by NilminDef, Z1;

              hence thesis;

            end;

              suppose

               HU: (a + c) <= 1;

              (a + ( min (b,c))) <= (a + c) by XREAL_1: 6, XXREAL_0: 17;

              then

               W1: (a + ( min (b,c))) <= 1 by HU, XXREAL_0: 2;

              (c + ( min (a,b))) <= (a + c) by XREAL_1: 6, XXREAL_0: 17;

              then

               W2: (c + ( min (a,b))) <= 1 by HU, XXREAL_0: 2;

              

               U1: (f . (a,b)) = ( min (a,b)) by NilminDef, Z1;

              (f . (a,(f . (b,c)))) = 0 by W1, NilminDef, Z2

              .= (f . ((f . (a,b)),c)) by U1, W2, NilminDef;

              hence thesis;

            end;

          end;

            suppose

             Z1: (a + b) > 1 & (b + c) <= 1;

            then

             Z2: (f . (a,b)) = ( min (a,b)) by NilminDef;

            per cases ;

              suppose (a + c) <= 1;

              then

               G2: (( min (a,b)) + c) <= 1 by Z1, XXREAL_0: 15;

              (f . (b,c)) = 0 by NilminDef, Z1;

              

              then (f . (a,(f . (b,c)))) = 0 by BU

              .= (f . ((f . (a,b)),c)) by Z2, NilminDef, G2;

              hence thesis;

            end;

              suppose

               hh: (a + c) > 1;

              

               g4: (( min (a,b)) + c) = ( min ((a + c),(b + c))) by FUZZY_2: 42

              .= (b + c) by XXREAL_0:def 9, hh, XXREAL_0: 2, Z1;

              (f . (b,c)) = 0 by NilminDef, Z1;

              hence thesis by Z2, g4, BU;

            end;

          end;

            suppose

             Z1: (a + b) <= 1 & (b + c) > 1;

            then

             Z2: (f . (b,c)) = ( min (b,c)) by NilminDef;

            

             ZZ: (f . (a,b)) = 0 by NilminDef, Z1;

            per cases ;

              suppose (a + c) <= 1;

              then

               G2: (( min (b,c)) + a) <= 1 by Z1, XXREAL_0: 15;

              (f . ((f . (a,b)),c)) = (f . ( 0 ,c)) by Z1, NilminDef

              .= (f . (c, 0 )) by FF, H1

              .= 0 by BU

              .= (f . (a,(f . (b,c)))) by Z2, NilminDef, G2;

              hence thesis;

            end;

              suppose

               g5: (a + c) > 1;

              

               g4: (( min (c,b)) + a) = ( min ((c + a),(b + a))) by FUZZY_2: 42

              .= (a + b) by XXREAL_0:def 9, g5, XXREAL_0: 2, Z1;

              (f . (a,(f . (b,c)))) = (f . (a,( min (b,c)))) by NilminDef, Z1

              .= 0 by NilminDef, g4, Z1

              .= (f . (c, 0 )) by BU

              .= (f . ((f . (a,b)),c)) by ZZ, FF;

              hence thesis;

            end;

          end;

            suppose

             Z1: (a + b) <= 1 & (b + c) <= 1;

            then

             Z2: (f . (b,c)) = 0 by NilminDef;

            

             Z3: (f . (a,b)) = 0 by NilminDef, Z1;

            (f . (a,(f . (b,c)))) = 0 by BU, Z2

            .= (f . (c, 0 )) by BU

            .= (f . ((f . (a,b)),c)) by Z3, FF;

            hence thesis;

          end;

        end;

        hence thesis by FF, TT, D1, BINOP_1:def 3, BINOP_1:def 2;

      end;

    end

    definition

      :: FUZNORM1:def13

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

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

      existence

      proof

        set A = [. 0 , 1.];

        deffunc F( Element of A, Element of A) = ( In ((($1 * $2) / (($1 + $2) - ($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);

        reconsider ff = f as BinOp of [. 0 , 1.];

        take ff;

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

        reconsider aa = a, bb = b as Element of A;

        (ff . (a,b)) = F(aa,bb) by A1;

        hence thesis by SUBSET_1:def 8, HamIn01;

      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)) = ((a * b) / ((a + b) - (a * b))) and

         A2: for a,b be Element of [. 0 , 1.] holds (f2 . (a,b)) = ((a * b) / ((a + b) - (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.];

          (f1 . (aa,bb)) = ((aa * bb) / ((aa + bb) - (aa * bb))) by A1

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

          hence thesis;

        end;

        hence thesis by BINOP_1:def 21;

      end;

    end

    registration

      cluster Hamacher_norm -> commutative associative with-1-identity monotonic;

      coherence

      proof

        set f = Hamacher_norm ;

        

         FF: for a,b be Element of [. 0 , 1.] holds (f . (a,b)) = (f . (b,a))

        proof

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

          (f . (a,b)) = ((a * b) / ((a + b) - (a * b))) by HamDef

          .= (f . (b,a)) by HamDef;

          hence thesis;

        end;

        

         TT: for a be Element of [. 0 , 1.] holds (f . (a,1)) = a

        proof

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

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

          then (f . (a,1)) = ((a * 1) / ((a + 1) - (a * 1))) by HamDef;

          hence thesis;

        end;

        

         D1: for a,b,c,d be Element of [. 0 , 1.] st a <= c & b <= d holds (f . (a,b)) <= (f . (c,d))

        proof

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

          

           JJ: 0 <= a & 0 <= b & 0 <= c & 0 <= d by XXREAL_1: 1;

          

           B2: (f . (c,d)) >= 0 by XXREAL_1: 1;

          assume

           S1: a <= c & b <= d;

          

           D1: (f . (a,b)) = ((a * b) / ((a + b) - (a * b))) by HamDef;

          

           D2: (f . (c,d)) = ((c * d) / ((c + d) - (c * d))) by HamDef;

          

           d2: (f . (a,d)) = ((a * d) / ((a + d) - (a * d))) by HamDef;

          set A = ((a + b) - (a * b)), B = ((c + d) - (c * d));

          per cases ;

            suppose A = 0 ;

            hence thesis by B2, XCMPLX_1: 49, D1;

          end;

            suppose

             DD: B = 0 ;

            reconsider ad = ((a + d) - (a * d)), ab = ((a + b) - (a * b)) as Element of [. 0 , 1.] by abMinab01;

            reconsider B as Element of [. 0 , 1.] by abMinab01;

            (1 - a) in [. 0 , 1.] by OpIn01;

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

            then (b * (1 - a)) <= (d * (1 - a)) by S1, XREAL_1: 64;

            then

             w0: ((b * (1 - a)) + a) <= ((d * (1 - a)) + a) by XREAL_1: 6;

            (1 - d) in [. 0 , 1.] by OpIn01;

            then (1 - d) >= 0 by XXREAL_1: 1;

            then (a * (1 - d)) <= (c * (1 - d)) by S1, XREAL_1: 64;

            then

             WC: ((a * (1 - d)) + d) <= ((c * (1 - d)) + d) by XREAL_1: 6;

            then

             de: ab = 0 by XXREAL_1: 1, DD, w0;

            

             dg: ad >= 0 by XXREAL_1: 1;

            

             hf: ad = 0 by DD, WC, XXREAL_1: 1;

            

             df: ((f . (a,d)) - (f . (a,b))) = (((a * d) / ad) - 0 ) by XCMPLX_1: 49, de, D1, d2

            .= ((a * d) / ad);

            

             WA: (f . (a,b)) <= ((f . (a,d)) - 0 ) by XREAL_1: 11, df, dg, JJ;

            ((f . (c,d)) - (f . (a,d))) = (((c * d) / B) - 0 ) by XCMPLX_1: 49, hf, d2, D2

            .= 0 by XCMPLX_1: 49, DD;

            hence thesis by WA;

          end;

            suppose A <> 0 & B <> 0 ;

            

            then

             D8: ((f . (c,d)) - (f . (a,b))) = (((A * (c * d)) - (B * (a * b))) / (A * B)) by XCMPLX_1: 130, D1, D2

            .= ((((a * c) * (d - b)) + ((b * d) * (c - a))) / (A * B));

            A in [. 0 , 1.] & B in [. 0 , 1.] by abMinab01;

            then

             d6: A >= 0 & B >= 0 by XXREAL_1: 1;

            b <= (d - 0 ) by S1;

            then

             D3: (d - b) >= 0 by XREAL_1: 11;

            a <= (c - 0 ) by S1;

            then (c - a) >= 0 by XREAL_1: 11;

            then (((f . (c,d)) - (f . (a,b))) + (f . (a,b))) >= ( 0 + (f . (a,b))) by XREAL_1: 6, d6, D8, JJ, D3;

            hence thesis;

          end;

        end;

        

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

        

         BU: for a be Element of [. 0 , 1.] holds (f . (a, 0 )) = 0

        proof

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

          (f . (a, 0 )) = ((a * 0 ) / ((a + 0 ) - (a * 0 ))) by HamDef, H1;

          hence thesis;

        end;

        for a,b,c be Element of [. 0 , 1.] holds (f . (a,(f . (b,c)))) = (f . ((f . (a,b)),c))

        proof

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

          

           J1: (f . (a,b)) = ((a * b) / ((a + b) - (a * b))) by HamDef;

          

           J2: (f . (b,c)) = ((b * c) / ((b + c) - (b * c))) by HamDef;

          reconsider bc = ((b * c) / ((b + c) - (b * c))) as Element of [. 0 , 1.] by HamIn01;

          set ab = ((a * b) / ((a + b) - (a * b)));

          set bb = ((b + c) - (b * c));

          set AB = ((a + b) - (a * b));

          per cases ;

            suppose

             Z1: a <> 0 & b <> 0 & c <> 0 ;

            then

             P1: (a * b) <> 0 by XCMPLX_1: 6;

            

             j3: ab in [. 0 , 1.] by HamIn01;

            per cases ;

              suppose ab = 0 ;

              then AB = 0 by XCMPLX_1: 50, P1;

              hence thesis by Z1, Lemacik;

            end;

              suppose

               T1: bc = 0 ;

              (b * c) <> 0 by Z1, XCMPLX_1: 6;

              then ((b + c) - (b * c)) = 0 by T1, XCMPLX_1: 50;

              hence thesis by Z1, Lemacik;

            end;

              suppose ab <> 0 & bc <> 0 ;

              then

               f1: AB <> 0 & bb <> 0 by XCMPLX_1: 49;

              

               WA: ((a * bc) * ((ab + c) - (ab * c))) = (((a * (b * c)) / bb) * (c + (((a * b) / AB) - (((a * b) / AB) * c)))) by XCMPLX_1: 74

              .= (((a * (b * c)) / bb) * (((c * AB) / AB) + (((a * b) / AB) * (1 - c)))) by XCMPLX_1: 89, f1

              .= (((a * (b * c)) / bb) * (((c * AB) / AB) + (((a * b) * (1 - c)) / AB))) by XCMPLX_1: 74

              .= (((a * (b * c)) / bb) * (((c * AB) + ((a * b) * (1 - c))) / AB)) by XCMPLX_1: 62

              .= (((a * (b * c)) * ((c * AB) + ((a * b) * (1 - c)))) / (AB * bb)) by XCMPLX_1: 76

              .= ((((a * b) * c) / AB) * (((a * bb) + ((b * c) * (1 - a))) / bb)) by XCMPLX_1: 76

              .= ((((a * b) * c) / AB) * (((a * bb) / bb) + (((b * c) * (1 - a)) / bb))) by XCMPLX_1: 62

              .= ((((a * b) * c) / AB) * (((a * bb) / bb) + (((b * c) / bb) * (1 - a)))) by XCMPLX_1: 74

              .= ((((a * b) / AB) * c) * (((a * bb) / bb) + (((b * c) / bb) * (1 - a)))) by XCMPLX_1: 74

              .= ((((a * b) / AB) * c) * (a + (((b * c) / bb) * (1 - a)))) by XCMPLX_1: 89, f1

              .= ((ab * c) * ((a + bc) - (a * bc)));

              per cases ;

                suppose that

                 f2: ((a + bc) - (a * bc)) <> 0 and

                 f3: ((ab + c) - (ab * c)) <> 0 ;

                (f . (a,(f . (b,c)))) = ((a * bc) / ((a + bc) - (a * bc))) by HamDef, J2

                .= ((ab * c) / ((ab + c) - (ab * c))) by WA, XCMPLX_1: 94, f2, f3

                .= (f . ((f . (a,b)),c)) by J1, HamDef;

                hence thesis;

              end;

                suppose ((a + bc) - (a * bc)) = 0 ;

                hence thesis by Z1, Lemacik;

              end;

                suppose ((ab + c) - (ab * c)) = 0 ;

                hence thesis by Z1, Lemacik, j3;

              end;

            end;

          end;

            suppose

             Z1: a <> 0 & b <> 0 & c = 0 ;

            

            then (f . (a,(f . (b,c)))) = (f . (a, 0 )) by BU

            .= 0 by BU

            .= (f . ((f . (a,b)),c)) by BU, Z1;

            hence thesis;

          end;

            suppose

             Z1: a = 0 & b <> 0 ;

            (f . (a,(f . (b,c)))) = (f . ((f . (b,c)),a)) by FF

            .= 0 by BU, Z1

            .= (f . (c, 0 )) by BU

            .= (f . ( 0 ,c)) by FF, H1

            .= (f . ((f . (b,a)),c)) by BU, Z1

            .= (f . ((f . (a,b)),c)) by FF;

            hence thesis;

          end;

            suppose

             Z1: a <> 0 & b = 0 ;

            then

             z1: (f . (a,b)) = 0 by BU;

            (f . (b,c)) = (f . (c,b)) by FF

            .= 0 by Z1, BU;

            

            then (f . (a,(f . (b,c)))) = 0 by BU

            .= (f . (c, 0 )) by BU

            .= (f . ((f . (a,b)),c)) by FF, z1;

            hence thesis;

          end;

            suppose

             Z1: a = 0 & b = 0 ;

            

            then

             Z2: (f . (a,b)) = (( 0 * 0 ) / (( 0 + 0 ) - ( 0 * 0 ))) by HamDef

            .= 0 ;

            (f . (b,c)) = ((b * c) / ((b + c) - (b * c))) by HamDef;

            hence thesis by Z2, Z1;

          end;

        end;

        hence thesis by FF, TT, D1, BINOP_1:def 3, BINOP_1:def 2;

      end;

    end

    begin

    definition

      :: FUZNORM1:def14

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

      : Drastic2CDef: for a,b be Element of [. 0 , 1.] holds (( min (a,b)) = 0 implies (it . (a,b)) = ( max (a,b))) & (( min (a,b)) <> 0 implies (it . (a,b)) = 1);

      existence

      proof

        set C = [. 0 , 1.];

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

        deffunc F( Element of C, Element of C) = ( In (( max ($1,$2)),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;

        

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

        

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

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

        proof

          thus ( min (a,b)) = 0 implies (f . (a,b)) = ( max (a,b))

          proof

            assume ( min (a,b)) = 0 ;

            then a = 0 or b = 0 by XXREAL_0: 15;

            

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

            .= ( max (a,b)) by SUBSET_1:def 8, cc;

            hence thesis;

          end;

          assume

           B0: ( min (a,b)) <> 0 ;

          a <> 0 & b <> 0

          proof

            assume a = 0 or b = 0 ;

            per cases ;

              suppose

               Z1: a = 0 ;

              then b >= a by XXREAL_1: 1;

              hence thesis by B0, XXREAL_0:def 9, Z1;

            end;

              suppose

               Z1: b = 0 ;

              then a >= b by XXREAL_1: 1;

              hence thesis by B0, XXREAL_0:def 9, Z1;

            end;

          end;

          

          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 (( min (a,b)) = 0 implies (f1 . (a,b)) = ( max (a,b))) & (( min (a,b)) <> 0 implies (f1 . (a,b)) = 1) and

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

          per cases ;

            suppose

             B0: ( min (aa,bb)) = 0 ;

            

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

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

            hence thesis;

          end;

            suppose

             B1: ( min (aa,bb)) <> 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

    begin

    definition

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

      :: FUZNORM1:def15

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

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

      existence

      proof

        reconsider A = [. 0 , 1.] as non empty real-membered set;

        deffunc F( Element of A, Element of A) = ( In ((1 - (t . ((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);

        reconsider ff = f as BinOp of [. 0 , 1.];

        take ff;

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

        reconsider aa = a, bb = b as Element of A;

        (ff . (a,b)) = F(aa,bb) by A1;

        hence thesis by SUBSET_1:def 8, CoIn01;

      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 - (t . ((1 - a),(1 - b)))) and

         A2: for a,b be Element of [. 0 , 1.] holds (f2 . (a,b)) = (1 - (t . ((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)) = (1 - (t . ((1 - xx),(1 - yy)))) by A1

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

          hence thesis;

        end;

        hence thesis by A3, BINOP_1: 20;

      end;

    end

    registration

      let t be t-norm;

      cluster ( conorm t) -> monotonic commutative associative with-0-identity;

      coherence

      proof

        set f = ( conorm t);

        

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

        proof

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

          

           A2: (1 - a) in [. 0 , 1.] & (1 - b) in [. 0 , 1.] by OpIn01;

          (f . (a,b)) = (1 - (t . ((1 - a),(1 - b)))) by CoDef

          .= (1 - (t . ((1 - b),(1 - a)))) by A2, BINOP_1:def 2

          .= (f . (b,a)) by CoDef;

          hence thesis;

        end;

        

         C1: for a,b,c be Element of [. 0 , 1.] holds (f . ((f . (a,b)),c)) = (f . (a,(f . (b,c))))

        proof

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

          

           A2: (1 - a) in [. 0 , 1.] & (1 - b) in [. 0 , 1.] & (1 - c) in [. 0 , 1.] by OpIn01;

          set A = (1 - (t . ((1 - a),(1 - b))));

          

           H1: A in [. 0 , 1.] by CoIn01;

          set C = (1 - (t . ((1 - b),(1 - c))));

          

           H2: C in [. 0 , 1.] by CoIn01;

          (f . ((f . (a,b)),c)) = (f . ((1 - (t . ((1 - a),(1 - b)))),c)) by CoDef

          .= (1 - (t . ((1 - A),(1 - c)))) by CoDef, H1

          .= (1 - (t . ((1 - a),(1 - C)))) by BINOP_1:def 3, A2

          .= (f . (a,C)) by CoDef, H2

          .= (f . (a,(f . (b,c)))) by CoDef;

          hence thesis;

        end;

        

         D1: for a,b,c,d be Element of [. 0 , 1.] st a <= c & b <= d holds (f . (a,b)) <= (f . (c,d))

        proof

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

          

           A2: (1 - a) in [. 0 , 1.] & (1 - b) in [. 0 , 1.] & (1 - c) in [. 0 , 1.] & (1 - d) in [. 0 , 1.] by OpIn01;

          assume a <= c & b <= d;

          then (1 - c) <= (1 - a) & (1 - d) <= (1 - b) by XREAL_1: 10;

          then (t . ((1 - a),(1 - b))) >= (t . ((1 - c),(1 - d))) by A2, MonDef;

          then (1 - (t . ((1 - a),(1 - b)))) <= (1 - (t . ((1 - c),(1 - d)))) by XREAL_1: 10;

          then (f . (a,b)) <= (1 - (t . ((1 - c),(1 - d)))) by CoDef;

          hence thesis by CoDef;

        end;

        for a be Element of [. 0 , 1.] holds (f . (a, 0 )) = a

        proof

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

          

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

          (1 - a) in [. 0 , 1.] by OpIn01;

          then (t . ((1 - a),1)) = (1 - a) by IdDef;

          then (1 - (t . ((1 - a),(1 - 0 )))) = a;

          hence thesis by CoDef, T1;

        end;

        hence thesis by A1, BINOP_1:def 2, BINOP_1:def 3, D1, C1;

      end;

    end

    theorem :: FUZNORM1:21

     maxnorm = ( conorm minnorm )

    proof

      for a,b be Element of [. 0 , 1.] holds ( maxnorm . (a,b)) = (1 - ( minnorm . ((1 - a),(1 - b))))

      proof

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

        

         A1: (1 - a) in [. 0 , 1.] & (1 - b) in [. 0 , 1.] by OpIn01;

        set e1 = ( - 1);

        

         A2: ( - ( max ((e1 * ( - a)),(e1 * ( - b))))) = ( - (e1 * ( min (( - a),( - b))))) by MES57

        .= ( min (( - a),( - b)));

        

         A3: ( min ((1 + ( - a)),(1 + ( - b)))) = (1 + ( min (( - a),( - b)))) by FUZZY_2: 42

        .= (1 - ( max (a,b))) by A2;

        ( maxnorm . (a,b)) = (1 - ( min ((1 - a),(1 - b)))) by A3, MaxDef

        .= (1 - ( minnorm . ((1 - a),(1 - b)))) by A1, MinDef;

        hence thesis;

      end;

      hence thesis by CoDef;

    end;

    theorem :: FUZNORM1:22

    for t be BinOp of [. 0 , 1.] holds ( conorm ( conorm t)) = t

    proof

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

      set tt = ( conorm ( conorm t));

      for a,b be Element of [. 0 , 1.] holds (t . (a,b)) = (tt . (a,b))

      proof

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

        

         A1: (1 - a) in [. 0 , 1.] & (1 - b) in [. 0 , 1.] by OpIn01;

        (tt . (a,b)) = (1 - (( conorm t) . ((1 - a),(1 - b)))) by CoDef

        .= (1 - (1 - (t . ((1 - (1 - a)),(1 - (1 - b)))))) by CoDef, A1;

        hence thesis;

      end;

      hence thesis by BINOP_1: 2;

    end;

    begin

    definition

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

      :: FUZNORM1:def16

      pred f1 <= f2 means for a,b be Element of [. 0 , 1.] holds (f1 . (a,b)) <= (f2 . (a,b));

    end

    theorem :: FUZNORM1:23

    for t be t-norm holds drastic_norm <= t

    proof

      let t be t-norm;

      set f1 = drastic_norm ;

      for a,b be Element of [. 0 , 1.] holds (f1 . (a,b)) <= (t . (a,b))

      proof

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

        per cases ;

          suppose

           A2: a = 1;

          reconsider aa = 1, bb = b as Element of [. 0 , 1.] by XXREAL_1: 1;

          (t . (aa,bb)) = (t . (bb,aa)) by BINOP_1:def 2

          .= b by IdDef;

          hence thesis by DrasticDef, A2;

        end;

          suppose

           A2: b = 1;

          reconsider aa = a, bb = 1 as Element of [. 0 , 1.] by XXREAL_1: 1;

          (f1 . (aa,bb)) = aa by DrasticDef;

          hence thesis by A2, IdDef;

        end;

          suppose

           A2: a <> 1 & b <> 1;

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

          (f1 . (aa,bb)) = 0 by DrasticDef, A2;

          hence thesis by XXREAL_1: 1;

        end;

      end;

      hence thesis;

    end;

    theorem :: FUZNORM1:24

    for t be t-norm holds t <= minnorm

    proof

      let t be t-norm;

      set f1 = minnorm ;

      for a,b be Element of [. 0 , 1.] holds (t . (a,b)) <= (f1 . (a,b))

      proof

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

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

        

         A1: (f1 . (a,b)) = ( min (aa,bb)) by MinDef;

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

        aa <= 1 by XXREAL_1: 1;

        then (t . (aa,bb)) <= (t . (cc,bb)) by MonDef;

        then (t . (aa,bb)) <= (t . (bb,cc)) by BINOP_1:def 2;

        then

         A3: (t . (aa,bb)) <= bb by IdDef;

        bb <= 1 by XXREAL_1: 1;

        then (t . (aa,bb)) <= (t . (aa,cc)) by MonDef;

        then (t . (aa,bb)) <= aa by IdDef;

        hence thesis by A1, XXREAL_0: 20, A3;

      end;

      hence thesis;

    end;

    theorem :: FUZNORM1:25

    for t1,t2 be t-norm st t1 <= t2 holds ( conorm t2) <= ( conorm t1)

    proof

      let t1,t2 be t-norm;

      set c1 = ( conorm t1), c2 = ( conorm t2);

      assume

       A1: t1 <= t2;

      for a,b be Element of [. 0 , 1.] holds (c2 . (a,b)) <= (c1 . (a,b))

      proof

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

        (1 - a) in [. 0 , 1.] & (1 - b) in [. 0 , 1.] by OpIn01;

        then (1 - (t2 . ((1 - a),(1 - b)))) <= (1 - (t1 . ((1 - a),(1 - b)))) by A1, XREAL_1: 10;

        then (1 - (t2 . ((1 - a),(1 - b)))) <= (c1 . (a,b)) by CoDef;

        hence thesis by CoDef;

      end;

      hence thesis;

    end;

    begin

    definition

      :: FUZNORM1:def17

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

      : HamCoDef: for a,b be Element of [. 0 , 1.] holds (a = b = 1 implies (it . (a,b)) = 1) & (a <> 1 or b <> 1 implies (it . (a,b)) = (((a + b) - ((2 * a) * b)) / (1 - (a * b))));

      existence

      proof

        set C = [. 0 , 1.];

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

        defpred P[ set, set] means $1 = 1 & $2 = 1;

        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]) = G(c,d)) & ( not P[c, d] implies (f . [c, d]) = F(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]) = G(c,d)) & ( not P[c, d] implies (f . [c, d]) = F(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 = 1 implies (f . (a,b)) = 1) & (a <> 1 or b <> 1 implies (f . (a,b)) = (((a + b) - ((2 * a) * b)) / (1 - (a * b))))

        proof

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

          proof

            assume a = b = 1;

            

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

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

            hence thesis;

          end;

          assume a <> 1 or b <> 1;

          

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

          .= (((a + b) - ((2 * a) * b)) / (1 - (a * b))) by SUBSET_1:def 8, HamCoIn01;

          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 = 1 implies (f1 . (a,b)) = 1) & (a <> 1 or b <> 1 implies (f1 . (a,b)) = (((a + b) - ((2 * a) * b)) / (1 - (a * b)))) and

         A2: for a,b be Element of [. 0 , 1.] holds (a = b = 1 implies (f2 . (a,b)) = 1) & (a <> 1 or b <> 1 implies (f2 . (a,b)) = (((a + b) - ((2 * a) * b)) / (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 = 1;

            

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

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

            hence thesis;

          end;

            suppose

             B1: aa <> 1 or bb <> 1;

            

            then (f1 . (aa,bb)) = (((aa + bb) - ((2 * aa) * bb)) / (1 - (aa * bb))) by A1

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

            hence thesis;

          end;

        end;

        hence thesis by BINOP_1:def 21;

      end;

    end

    theorem :: FUZNORM1:26

    

     CoHam: ( conorm Hamacher_norm ) = Hamacher_conorm

    proof

      set dn = ( conorm Hamacher_norm );

      set dc = Hamacher_conorm ;

      for a,b be Element of [. 0 , 1.] holds (dc . (a,b)) = (1 - ( Hamacher_norm . ((1 - a),(1 - b))))

      proof

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

        

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

        

         A3: (1 - a) in [. 0 , 1.] & (1 - b) in [. 0 , 1.] by OpIn01;

        

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

        per cases ;

          suppose

           Aa: a <> 1 or b <> 1;

          then

           AA: (1 - (a * b)) <> 0 by WE, XREAL_1: 150;

          (dc . (a,b)) = (((a + b) - ((2 * a) * b)) / (1 - (a * b))) by HamCoDef, Aa

          .= (((1 * (((1 - a) + (1 - b)) - ((1 - a) * (1 - b)))) - ((1 - a) * (1 - b))) / (((1 - a) + (1 - b)) - ((1 - a) * (1 - b))))

          .= (1 - (((1 - a) * (1 - b)) / (((1 - a) + (1 - b)) - ((1 - a) * (1 - b))))) by XCMPLX_1: 127, AA

          .= (1 - ( Hamacher_norm . ((1 - a),(1 - b)))) by HamDef, A3;

          hence thesis;

        end;

          suppose

           T1: a = b = 1;

          

          then ( Hamacher_norm . ((1 - a),(1 - b))) = (( 0 * 0 ) / (( 0 + 0 ) - ( 0 * 0 ))) by HamDef, AB

          .= 0 ;

          hence thesis by T1, HamCoDef;

        end;

      end;

      hence thesis by CoDef;

    end;

    registration

      cluster Hamacher_conorm -> commutative associative with-0-identity monotonic;

      coherence by CoHam;

    end

    theorem :: FUZNORM1:27

    ( conorm drastic_norm ) = drastic_conorm

    proof

      set dn = ( conorm drastic_norm );

      set dc = drastic_conorm ;

      for a,b be Element of [. 0 , 1.] holds (dc . (a,b)) = (1 - ( drastic_norm . ((1 - a),(1 - b))))

      proof

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

        

         A3: (1 - a) in [. 0 , 1.] & (1 - b) in [. 0 , 1.] by OpIn01;

        then

         we: (1 - a) <= 1 & (1 - b) <= 1 by XXREAL_1: 1;

        

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

        per cases ;

          suppose

           A0: a = 0 & b = 0 ;

          then

           A1: ( min (a,b)) = 0 ;

          

           A2: ( max ((1 - a),(1 - b))) = 1 by A0;

          (dc . (a,b)) = ( max (a,b)) by Drastic2CDef, A1

          .= (1 - ( min ((1 - a),(1 - b)))) by A0

          .= (1 - ( drastic_norm . ((1 - a),(1 - b)))) by Drastic2Def, A2, A3;

          hence thesis;

        end;

          suppose

           BB: a <> 0 & b <> 0 ;

          then

           B0: ( min (a,b)) <> 0 by XXREAL_0: 15;

          (1 - a) <> 1 & (1 - b) <> 1 by BB;

          then

           B1: ( max ((1 - a),(1 - b))) <> 1 by XXREAL_0: 16;

          (dc . (a,b)) = (1 - 0 ) by Drastic2CDef, B0

          .= (1 - ( drastic_norm . ((1 - a),(1 - b)))) by Drastic2Def, B1, A3;

          hence thesis;

        end;

          suppose

           BB: b <> 0 & a = 0 ;

          then

           B0: ( min (a,b)) = 0 by WE, XXREAL_0:def 9;

          

           B1: ( min ((1 - a),(1 - b))) = (1 - b) by we, XXREAL_0:def 9, BB;

          

           B8: ( max ((1 - a),(1 - b))) = 1 by XXREAL_0:def 10, we, BB;

          (dc . (a,b)) = ( max (a,b)) by Drastic2CDef, B0

          .= (1 - ( min ((1 - a),(1 - b)))) by B1, BB, XXREAL_0:def 10, WE

          .= (1 - ( drastic_norm . ((1 - a),(1 - b)))) by Drastic2Def, A3, B8;

          hence thesis;

        end;

          suppose

           BB: a <> 0 & b = 0 ;

          then

           B0: ( min (a,b)) = 0 by WE, XXREAL_0:def 9;

          

           B1: ( min ((1 - a),(1 - b))) = (1 - a) by we, XXREAL_0:def 9, BB;

          

           B8: ( max ((1 - a),(1 - b))) = 1 by XXREAL_0:def 10, we, BB;

          (dc . (a,b)) = ( max (a,b)) by Drastic2CDef, B0

          .= (1 - ( min ((1 - a),(1 - b)))) by B1, BB, XXREAL_0:def 10, WE

          .= (1 - ( drastic_norm . ((1 - a),(1 - b)))) by Drastic2Def, A3, B8;

          hence thesis;

        end;

      end;

      hence thesis by CoDef;

    end;

    theorem :: FUZNORM1:28

    

     ConormProd: ( conorm prodnorm ) = probsum_conorm

    proof

      set dn = ( conorm prodnorm );

      set dc = probsum_conorm ;

      for a,b be Element of [. 0 , 1.] holds (dc . (a,b)) = (1 - ( prodnorm . ((1 - a),(1 - b))))

      proof

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

        

         A3: (1 - a) in [. 0 , 1.] & (1 - b) in [. 0 , 1.] by OpIn01;

        (dc . (a,b)) = ((a + b) - (a * b)) by ProbSumDef

        .= (1 - ((1 - a) * (1 - b)))

        .= (1 - ( prodnorm . ((1 - a),(1 - b)))) by ProdDef, A3;

        hence thesis;

      end;

      hence thesis by CoDef;

    end;

    registration

      cluster probsum_conorm -> commutative associative with-0-identity monotonic;

      coherence by ConormProd;

    end

    definition

      :: FUZNORM1:def18

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

      : NilmaxDef: for a,b be Element of [. 0 , 1.] holds ((a + b) < 1 implies (it . (a,b)) = ( max (a,b))) & ((a + b) >= 1 implies (it . (a,b)) = 1);

      existence

      proof

        set C = [. 0 , 1.];

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

        deffunc F( Element of C, Element of C) = ( In (( max ($1,$2)),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;

        

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

        

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

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

        proof

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

          proof

            assume (a + b) < 1;

            

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

            .= ( max (a,b)) by SUBSET_1:def 8, cc;

            hence thesis;

          end;

          assume (a + 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 ((a + b) < 1 implies (f1 . (a,b)) = ( max (a,b))) & ((a + b) >= 1 implies (f1 . (a,b)) = 1) and

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

          per cases ;

            suppose

             B0: (aa + bb) < 1;

            

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

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

            hence thesis;

          end;

            suppose

             B1: (aa + 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

    theorem :: FUZNORM1:29

    

     ConormNilmin: ( conorm nilmin_norm ) = nilmax_conorm

    proof

      set dn = ( conorm nilmin_norm );

      set dc = nilmax_conorm ;

      for a,b be Element of [. 0 , 1.] holds (dc . (a,b)) = (1 - ( nilmin_norm . ((1 - a),(1 - b))))

      proof

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

        

         A3: (1 - a) in [. 0 , 1.] & (1 - b) in [. 0 , 1.] by OpIn01;

        per cases ;

          suppose

           W0: (a + b) < 1;

          then (2 - (a + b)) > (2 - 1) by XREAL_1: 10;

          then

           W1: ((1 - a) + (1 - b)) > 1;

          (dc . (a,b)) = ( max (a,b)) by NilmaxDef, W0

          .= (1 - ( min ((1 - a),(1 - b)))) by MaxMin

          .= (1 - ( nilmin_norm . ((1 - a),(1 - b)))) by NilminDef, A3, W1;

          hence thesis;

        end;

          suppose

           W0: (a + b) >= 1;

          then (2 - (a + b)) <= (2 - 1) by XREAL_1: 10;

          then

           W1: ((1 - a) + (1 - b)) <= 1;

          (dc . (a,b)) = (1 - 0 ) by NilmaxDef, W0

          .= (1 - ( nilmin_norm . ((1 - a),(1 - b)))) by NilminDef, A3, W1;

          hence thesis;

        end;

      end;

      hence thesis by CoDef;

    end;

    registration

      cluster nilmax_conorm -> commutative associative with-0-identity monotonic;

      coherence by ConormNilmin;

    end

    definition

      :: FUZNORM1:def19

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

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

      existence

      proof

        reconsider A = [. 0 , 1.] as non empty real-membered set;

        deffunc F( Element of A, Element of A) = ( In (( min (($1 + $2),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);

        reconsider ff = f as BinOp of [. 0 , 1.];

        take ff;

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

        reconsider aa = a, bb = b as Element of A;

        (ff . (a,b)) = F(aa,bb) by A1;

        hence thesis by SUBSET_1:def 8, Lemma2a;

      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 ((a + b),1)) and

         A2: for a,b be Element of [. 0 , 1.] holds (f2 . (a,b)) = ( min ((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)) = ( min ((xx + yy),1)) by A1

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

          hence thesis;

        end;

        hence thesis by A3, BINOP_1: 20;

      end;

    end

    theorem :: FUZNORM1:30

    

     ConormLukasiewicz: ( conorm Lukasiewicz_norm ) = BoundedSum_conorm

    proof

      set dn = ( conorm Lukasiewicz_norm );

      set dc = BoundedSum_conorm ;

      for a,b be Element of [. 0 , 1.] holds (dc . (a,b)) = (1 - ( Lukasiewicz_norm . ((1 - a),(1 - b))))

      proof

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

        

         A3: (1 - a) in [. 0 , 1.] & (1 - b) in [. 0 , 1.] by OpIn01;

        (dc . (a,b)) = ( min ((a + b),1)) by LukConorm

        .= (1 - ( max ( 0 ,(((1 - a) + (1 - b)) - 1)))) by LukasiDual

        .= (1 - ( Lukasiewicz_norm . ((1 - a),(1 - b)))) by LukNorm, A3;

        hence thesis;

      end;

      hence thesis by CoDef;

    end;

    registration

      cluster BoundedSum_conorm -> commutative associative with-0-identity monotonic;

      coherence by ConormLukasiewicz;

    end

    theorem :: FUZNORM1:31

    for t be t-conorm holds maxnorm <= t

    proof

      let t be t-conorm;

      set f1 = maxnorm ;

      for a,b be Element of [. 0 , 1.] holds (f1 . (a,b)) <= (t . (a,b))

      proof

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

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

        

         A1: (f1 . (a,b)) = ( max (aa,bb)) by MaxDef;

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

        aa >= 0 by XXREAL_1: 1;

        then (t . (aa,bb)) >= (t . (cc,bb)) by MonDef;

        then (t . (aa,bb)) >= (t . (bb,cc)) by BINOP_1:def 2;

        then

         A3: (t . (aa,bb)) >= bb by ZeroDef;

        bb >= 0 by XXREAL_1: 1;

        then (t . (aa,bb)) >= (t . (aa,cc)) by MonDef;

        then (t . (aa,bb)) >= aa by ZeroDef;

        hence thesis by A1, XXREAL_0: 28, A3;

      end;

      hence thesis;

    end;

    theorem :: FUZNORM1:32

    for t be t-conorm holds t <= drastic_conorm

    proof

      let t be t-conorm;

      set f1 = drastic_conorm ;

      for a,b be Element of [. 0 , 1.] holds (f1 . (a,b)) >= (t . (a,b))

      proof

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

        per cases by XXREAL_0: 15;

          suppose

           A2: a = 0 ;

          then

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

          aa <= bb by XXREAL_1: 1;

          then ( min (aa,bb)) = 0 by XXREAL_0:def 9;

          then

           A3: (f1 . (aa,bb)) = ( max (aa,bb)) by Drastic2CDef;

          (t . (aa,bb)) = (t . (bb,aa)) by BINOP_1:def 2

          .= b by ZeroDef;

          hence thesis by A2, A3, XXREAL_0: 25;

        end;

          suppose

           A2: b = 0 ;

          then

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

          aa >= bb by XXREAL_1: 1;

          then ( min (aa,bb)) = 0 by XXREAL_0:def 9;

          then

           A3: (f1 . (aa,bb)) = ( max (aa,bb)) by Drastic2CDef;

          (t . (aa,bb)) = a by ZeroDef;

          hence thesis by A2, A3, XXREAL_0: 25;

        end;

          suppose

           aa: ( min (a,b)) <> 0 ;

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

          (f1 . (aa,bb)) = 1 by Drastic2CDef, aa;

          hence thesis by XXREAL_1: 1;

        end;

      end;

      hence thesis;

    end;