fuzimpl3.miz



    begin

    theorem :: FUZIMPL3:1

    

     LemmaImp: for x,r be Real st 0 <= x <= 1 & r > ( - 1) holds ((x * r) + 1) > 0

    proof

      let x,r be Real;

      assume

       AA: 0 <= x <= 1 & r > ( - 1);

      per cases ;

        suppose r < 0 ;

        then r <= (r * x) by XREAL_1: 152, AA;

        then ( - 1) < (r * x) by XXREAL_0: 2, AA;

        then ((x * r) + 1) > (( - 1) + 1) by XREAL_1: 8;

        hence thesis;

      end;

        suppose r >= 0 ;

        hence thesis by AA;

      end;

    end;

    theorem :: FUZIMPL3:2

    

     Wazne1: for z be Real st z in [. 0 , 1.] & z <> 0 holds ex w be Element of [. 0 , 1.] st w < z

    proof

      let z be Real;

      assume

       A1: z in [. 0 , 1.] & z <> 0 ;

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

      take w;

      thus thesis by A1, XXREAL_1: 1;

    end;

    theorem :: FUZIMPL3:3

    

     Wazne2: for z be Real st z in [. 0 , 1.] & z <> 1 holds ex w be Element of [. 0 , 1.] st w > z

    proof

      let z be Real;

      assume

       A1: z in [. 0 , 1.] & z <> 1;

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

      take w;

      1 >= z by A1, XXREAL_1: 1;

      hence thesis by A1, XXREAL_0: 1;

    end;

    registration

      cluster bijective increasing for UnOp of [. 0 , 1.];

      existence

      proof

        reconsider f = ( id [. 0 , 1.]) as UnOp of [. 0 , 1.];

        take f;

        thus f is bijective;

        thus f is increasing;

      end;

    end

    registration

      cluster bijective non-decreasing -> increasing for UnOp of [. 0 , 1.];

      coherence ;

      cluster bijective increasing -> non-decreasing for UnOp of [. 0 , 1.];

      coherence ;

    end

    registration

      let f be bijective increasing UnOp of [. 0 , 1.];

      cluster (f " ) -> real-valued Function-like;

      coherence ;

    end

    registration

      let f be bijective increasing UnOp of [. 0 , 1.];

      cluster ((f | [. 0 , 1.]) " ) -> real-valued;

      coherence ;

    end

    

     RF220: for h be REAL -defined real-valued Function, Y be set holds (h | Y) is increasing iff for r1,r2 be Real st r1 in (Y /\ ( dom h)) & r2 in (Y /\ ( dom h)) & r1 < r2 holds (h . r1) < (h . r2)

    proof

      let h be REAL -defined real-valued Function, Y be set;

      thus (h | Y) is increasing implies for r1,r2 be Real st r1 in (Y /\ ( dom h)) & r2 in (Y /\ ( dom h)) & r1 < r2 holds (h . r2) > (h . r1)

      proof

        assume

         A1: (h | Y) is increasing;

        let r1,r2 be Real such that

         A2: r1 in (Y /\ ( dom h)) and

         A3: r2 in (Y /\ ( dom h)) and

         A4: r1 < r2;

        

         A5: r2 in ( dom (h | Y)) by A3, RELAT_1: 61;

        then

         A6: ((h | Y) . r2) = (h . r2) by FUNCT_1: 47;

        

         A7: r1 in ( dom (h | Y)) by A2, RELAT_1: 61;

        then ((h | Y) . r1) = (h . r1) by FUNCT_1: 47;

        hence thesis by A1, A4, A7, A5, A6;

      end;

      assume

       A8: for r1,r2 be Real st r1 in (Y /\ ( dom h)) & r2 in (Y /\ ( dom h)) & r1 < r2 holds (h . r1) < (h . r2);

      let r1,r2 be ExtReal;

      assume that

       A9: r1 in ( dom (h | Y)) & r2 in ( dom (h | Y)) and

       A10: r1 < r2;

      

       aa: ( dom (h | Y)) c= REAL by RELAT_1:def 18;

      

       A11: ((h | Y) . r1) = (h . r1) & ((h | Y) . r2) = (h . r2) by A9, FUNCT_1: 47;

      r1 in (Y /\ ( dom h)) & r2 in (Y /\ ( dom h)) by A9, RELAT_1: 61;

      hence thesis by A11, A8, A10, aa, A9;

    end;

    theorem :: FUZIMPL3:4

    for f be one-to-one UnOp of [. 0 , 1.], d be Element of [. 0 , 1.] st d in ( rng f) holds ((f " ) . d) in ( dom f)

    proof

      let f be one-to-one UnOp of [. 0 , 1.], d be Element of [. 0 , 1.];

      set X = [. 0 , 1.];

      reconsider fX = (f | X) as PartFunc of X, X;

      assume

       a1: d in ( rng f);

      

       YZ: ( dom f) = ( rng (f " )) by FUNCT_1: 33;

      reconsider dd = d as Element of REAL ;

      ( dom (f " )) = ( rng f) by FUNCT_1: 33;

      hence thesis by YZ, FUNCT_1: 3, a1;

    end;

    

     Cosik1: for f be bijective UnOp of [. 0 , 1.] holds ((f | [. 0 , 1.]) " ) is REAL -defined

    proof

      let f be bijective UnOp of [. 0 , 1.];

      ( dom (f " )) = ( rng f) by FUNCT_1: 33;

      hence thesis by RELAT_1:def 18, RELAT_1:def 19;

    end;

    

     FC9: for f be bijective increasing UnOp of [. 0 , 1.] holds (((f | [. 0 , 1.]) " ) | (f .: [. 0 , 1.])) is increasing

    proof

      let f be bijective increasing UnOp of [. 0 , 1.];

      set X = [. 0 , 1.];

      assume that

       A2: not (((f | X) " ) | (f .: X)) is increasing;

      

       BB: ((f | X) " ) is REAL -defined by Cosik1;

      consider r1,r2 be Real such that

       A3: r1 in ((f .: X) /\ ( dom ((f | X) " ))) and

       A4: r2 in ((f .: X) /\ ( dom ((f | X) " ))) and

       A5: r1 < r2 and

       A6: (((f | X) " ) . r1) >= (((f | X) " ) . r2) by A2, RF220, BB;

      

       BB: ( rng (f | X)) c= X by RELAT_1:def 19;

      

       a1: ( rng f) c= [. 0 , 1.] by RELAT_1:def 19;

      

       b2: ( dom f) = ( rng (f " )) by FUNCT_1: 33;

      

       b1: ( rng f) = ( dom (f " )) by FUNCT_1: 33;

      then

       a5: ( dom ((f | X) " )) = [. 0 , 1.] by FUNCT_2:def 1;

      

       A7: (f .: X) = ( rng (f | X)) by RELAT_1: 115;

      then

       A8: r1 in ( rng (f | X)) by A3, XBOOLE_0:def 4;

      

       A9: r2 in ( rng (f | X)) by A4, A7, XBOOLE_0:def 4;

      

       A10: ((f | X) | X) is increasing;

      now

        per cases ;

          suppose (((f | X) " ) . r1) = (((f | X) " ) . r2);

          

          then r1 = ((f | X) . (((f | X) " ) . r2)) by A8, FUNCT_1: 35

          .= r2 by A9, FUNCT_1: 35;

          hence contradiction by A5;

        end;

          suppose

           A11: (((f | X) " ) . r1) <> (((f | X) " ) . r2);

          reconsider d = r2 as Element of [. 0 , 1.] by BB, A9;

          set c = (((f | X) " ) . d);

          

           a4: ( rng ((f | X) " )) c= X by b2, RELAT_1:def 19;

          c in ( rng ((f | X) " )) by a5, FUNCT_1: 3;

          then

          reconsider c as Element of [. 0 , 1.] by a4;

          

           F1: r2 in ( rng f) & c = ((f " ) . r2) implies c in ( dom f) by PARTFUN2: 60;

          reconsider rr1 = r1 as Element of [. 0 , 1.] by A8, a1;

          

           aa: rr1 in ( rng f) implies ((f " ) . rr1) in ( dom f) by PARTFUN2: 60;

          (((f | X) " ) . r2) < (((f | X) " ) . r1) by A6, A11, XXREAL_0: 1;

          then ((f | X) . (((f | X) " ) . r2)) < ((f | X) . (((f | X) " ) . r1)) by A10, aa, A4, A7, XBOOLE_0:def 4, F1, A3;

          then r2 < ((f | X) . (((f | X) " ) . r1)) by A9, FUNCT_1: 35;

          hence contradiction by A5, A8, FUNCT_1: 35;

        end;

      end;

      hence contradiction;

    end;

    theorem :: FUZIMPL3:5

    

     LemmaIncreas: for f be bijective increasing UnOp of [. 0 , 1.] holds (f " ) is increasing

    proof

      set X = [. 0 , 1.];

      let f be bijective increasing UnOp of [. 0 , 1.];

      

       A2: (((f | X) " ) | (f .: X)) is increasing by FC9;

      

       A3: ( dom f) = X & ( rng f) = X by FUNCT_2:def 1, FUNCT_2:def 3;

      (f .: X) = X by RELAT_1: 113, A3;

      hence thesis by A2;

    end;

    registration

      let f be bijective increasing UnOp of [. 0 , 1.];

      cluster (f " ) -> increasing;

      coherence by LemmaIncreas;

    end

    theorem :: FUZIMPL3:6

    

     Rosnie: for f be UnOp of [. 0 , 1.] holds f is non-decreasing iff for a,b be Element of [. 0 , 1.] st a <= b holds (f . a) <= (f . b)

    proof

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

      ( dom f) = [. 0 , 1.] by FUNCT_2:def 1;

      hence f is non-decreasing implies for a,b be Element of [. 0 , 1.] st a <= b holds (f . a) <= (f . b);

      assume

       B1: for a,b be Element of [. 0 , 1.] st a <= b holds (f . a) <= (f . b);

      let e1,e2 be ExtReal;

      assume

       B2: e1 in ( dom f) & e2 in ( dom f) & e1 <= e2;

      then

      reconsider ee1 = e1, ee2 = e2 as Element of [. 0 , 1.] by FUNCT_2:def 1;

      ee1 <= ee2 by B2;

      hence thesis by B1;

    end;

    theorem :: FUZIMPL3:7

    

     NonInc: for f be UnOp of [. 0 , 1.] holds f is non-increasing iff for a,b be Element of [. 0 , 1.] st a <= b holds (f . a) >= (f . b)

    proof

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

      ( dom f) = [. 0 , 1.] by FUNCT_2:def 1;

      hence f is non-increasing implies for a,b be Element of [. 0 , 1.] st a <= b holds (f . a) >= (f . b);

      assume

       B1: for a,b be Element of [. 0 , 1.] st a <= b holds (f . a) >= (f . b);

      let e1,e2 be ExtReal;

      assume

       B2: e1 in ( dom f) & e2 in ( dom f) & e1 <= e2;

      then

      reconsider ee1 = e1, ee2 = e2 as Element of [. 0 , 1.] by FUNCT_2:def 1;

      ee1 <= ee2 by B2;

      hence thesis by B1;

    end;

    theorem :: FUZIMPL3:8

    

     Decreas: for f be UnOp of [. 0 , 1.] holds f is decreasing iff for a,b be Element of [. 0 , 1.] st a < b holds (f . a) > (f . b)

    proof

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

      ( dom f) = [. 0 , 1.] by FUNCT_2:def 1;

      hence f is decreasing implies for a,b be Element of [. 0 , 1.] st a < b holds (f . a) > (f . b);

      assume

       B1: for a,b be Element of [. 0 , 1.] st a < b holds (f . a) > (f . b);

      let e1,e2 be ExtReal;

      assume

       B2: e1 in ( dom f) & e2 in ( dom f) & e1 < e2;

      then

      reconsider ee1 = e1, ee2 = e2 as Element of [. 0 , 1.] by FUNCT_2:def 1;

      ee1 < ee2 by B2;

      hence thesis by B1;

    end;

    theorem :: FUZIMPL3:9

    

     RosnieI: for f be UnOp of [. 0 , 1.] holds f is increasing iff for a,b be Element of [. 0 , 1.] st a < b holds (f . a) < (f . b)

    proof

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

      ( dom f) = [. 0 , 1.] by FUNCT_2:def 1;

      hence f is increasing implies for a,b be Element of [. 0 , 1.] st a < b holds (f . a) < (f . b);

      assume

       B1: for a,b be Element of [. 0 , 1.] st a < b holds (f . a) < (f . b);

      let e1,e2 be ExtReal;

      assume

       B2: e1 in ( dom f) & e2 in ( dom f) & e1 < e2;

      then

      reconsider ee1 = e1, ee2 = e2 as Element of [. 0 , 1.] by FUNCT_2:def 1;

      ee1 < ee2 by B2;

      hence thesis by B1;

    end;

    theorem :: FUZIMPL3:10

    

     LemmaBound: for f be increasing bijective UnOp of [. 0 , 1.] holds (f . 0 ) = 0 & (f . 1) = 1

    proof

      let f be increasing bijective UnOp of [. 0 , 1.];

      

       KK: (f . 0 ) = 0

      proof

        set y = (f . 0 );

        set X = [. 0 , 1.];

        

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

        reconsider y as Element of [. 0 , 1.] by XXREAL_1: 1, FUNCT_2: 5;

        assume

         H0: (f . 0 ) <> 0 ;

        

         I3: ( rng f) = X by FUNCT_2:def 3;

        reconsider z = ((f " ) . 0 ) as Element of [. 0 , 1.] by XXREAL_1: 1, FUNCT_2: 5;

        

         L1: (f . z) = 0 by FUNCT_1: 35, I3, K1;

        then

        consider zz be Element of [. 0 , 1.] such that

         L2: zz < z by Wazne1, H0;

        (f . zz) < (f . z) by L2, RosnieI;

        hence contradiction by L1, XXREAL_1: 1;

      end;

      (f . 1) = 1

      proof

        set X = [. 0 , 1.];

        

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

        reconsider y = (f . 1) as Element of [. 0 , 1.] by XXREAL_1: 1, FUNCT_2: 5;

        assume

         H0: (f . 1) <> 1;

        

         I3: ( rng f) = X by FUNCT_2:def 3;

        reconsider z = ((f " ) . 1) as Element of [. 0 , 1.] by XXREAL_1: 1, FUNCT_2: 5;

        

         L1: (f . z) = 1 by FUNCT_1: 35, I3, K1;

        then

        consider zz be Element of [. 0 , 1.] such that

         L2: zz > z by Wazne2, H0;

        (f . zz) > (f . z) by L2, RosnieI;

        hence contradiction by L1, XXREAL_1: 1;

      end;

      hence thesis by KK;

    end;

    registration

      let f be bijective increasing UnOp of [. 0 , 1.];

      cluster (f " ) -> bijective increasing;

      coherence ;

    end

    begin

    definition

      :: FUZIMPL3:def1

      func Theta -> set equals the set of all f where f be bijective increasing UnOp of [. 0 , 1.];

      coherence ;

    end

    definition

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

      let h be bijective increasing UnOp of [. 0 , 1.];

      :: FUZIMPL3:def2

      func ConjImpl (f,h) -> BinOp of [. 0 , 1.] means

      : BIDef: for x1,x2 be Element of [. 0 , 1.] holds (it . (x1,x2)) = ((h " ) . (f . ((h . x1),(h . x2))));

      existence

      proof

        deffunc F( Real, Real) = ((h " ) . (f . ((h . $1),(h . $2))));

        

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

        proof

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

          ((h " ) . (f . ((h . a),(h . b)))) in [. 0 , 1.];

          hence thesis;

        end;

        ex f be BinOp of [. 0 , 1.] st for a,b be Element of [. 0 , 1.] holds (f . (a,b)) = F(a,b) from FUZNORM1:sch 1( A1);

        hence thesis;

      end;

      uniqueness

      proof

        deffunc F( Real, Real) = ((h " ) . (f . ((h . $1),(h . $2))));

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

        for o1,o2 be BinOp of A st (for a,b be Element of A holds (o1 . (a,b)) = F(a,b)) & (for a,b be Element of A holds (o2 . (a,b)) = F(a,b)) holds o1 = o2 from BINOP_2:sch 2;

        hence thesis;

      end;

    end

    definition

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

      :: FUZIMPL3:def3

      pred f,g are_conjugate means ex h be bijective increasing UnOp of [. 0 , 1.] st g = ( ConjImpl (f,h));

    end

    registration

      let I be Fuzzy_Implication, f be bijective non-decreasing UnOp of [. 0 , 1.];

      cluster ( ConjImpl (I,f)) -> decreasing_on_1st increasing_on_2nd 00-dominant 11-dominant 10-weak;

      coherence

      proof

        set g = ( ConjImpl (I,f));

        set X = [. 0 , 1.];

        

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

        proof

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

          set h = (((f | X) " ) | (f .: X));

          

           U1: X = ( dom f) by FUNCT_2:def 1;

          ( rng f) = X by FUNCT_2:def 3;

          then

           Z8: h = ((f " ) | X) by U1, RELAT_1: 113;

          reconsider h as UnOp of [. 0 , 1.] by Z8;

          

           a0: ( dom f) = [. 0 , 1.] by FUNCT_2:def 1;

          assume x1 <= x2;

          then

           B1: (f . x1) <= (f . x2) by a0, VALUED_0:def 15;

          

           A1: (g . (x1,y)) = ((f " ) . (I . ((f . x1),(f . y)))) by BIDef;

          

           T1: (g . (x2,y)) = ((f " ) . (I . ((f . x2),(f . y)))) by BIDef;

          (I . ((f . x1),(f . y))) >= (I . ((f . x2),(f . y))) by B1, FUZIMPL1:def 1;

          hence thesis by A1, T1, Rosnie;

        end;

        

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

        proof

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

          assume

           WW: y1 <= y2;

          reconsider h = (f " ) as UnOp of [. 0 , 1.];

          ( dom f) = [. 0 , 1.] by FUNCT_2:def 1;

          then

           B1: (f . y1) <= (f . y2) by WW, VALUED_0:def 15;

          

           A1: (g . (x,y2)) = ((f " ) . (I . ((f . x),(f . y2)))) by BIDef;

          

           T1: (g . (x,y1)) = ((f " ) . (I . ((f . x),(f . y1)))) by BIDef;

          (I . ((f . x),(f . y1))) <= (I . ((f . x),(f . y2))) by B1, FUZIMPL1:def 2;

          hence thesis by A1, T1, Rosnie;

        end;

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

        

         H2: (f . 0 ) = 0 by LemmaBound;

        

         H3: (f . 1) = 1 by LemmaBound;

        

         H5: ((f " ) . 0 ) = 0 by LemmaBound;

        

         v3: (g . (x1,x1)) = ((f " ) . (I . ((f . x1),(f . x1)))) by BIDef

        .= ((f " ) . 1) by FUZIMPL1:def 3, H2

        .= 1 by LemmaBound;

        

         v4: (g . (x2,x2)) = ((f " ) . (I . ((f . x2),(f . x2)))) by BIDef

        .= ((f " ) . 1) by FUZIMPL1:def 4, H3

        .= 1 by LemmaBound;

        (g . (x2,x1)) = ((f " ) . (I . ((f . x2),(f . x1)))) by BIDef

        .= 0 by H5, FUZIMPL1:def 5, H2, H3;

        hence thesis by V1, v2, v3, v4;

      end;

    end

    theorem :: FUZIMPL3:11

    for I be Fuzzy_Implication, f be bijective increasing UnOp of [. 0 , 1.] holds ( ConjImpl (I,f)) is Fuzzy_Implication;

    registration

      cluster satisfying_(NP) satisfying_(OP) satisfying_(EP) satisfying_(IP) for Fuzzy_Implication;

      existence

      proof

        take I_LK ;

        thus thesis;

      end;

    end

    theorem :: FUZIMPL3:12

    

     Prop136a: for I be Fuzzy_Implication, f be bijective increasing UnOp of [. 0 , 1.] st I is satisfying_(NP) holds ( ConjImpl (I,f)) is satisfying_(NP)

    proof

      let I be Fuzzy_Implication, f be bijective increasing UnOp of [. 0 , 1.];

      assume

       B0: I is satisfying_(NP);

      set g = ( ConjImpl (I,f));

      

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

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

      (g . (1,y)) = ((f " ) . (I . ((f . 1),(f . y)))) by A0, BIDef

      .= ((f " ) . (I . (1,(f . y)))) by LemmaBound

      .= ((f " ) . (f . y)) by B0, FUZIMPL2:def 1;

      hence thesis by FUNCT_2: 26;

    end;

    theorem :: FUZIMPL3:13

    

     Prop136b: for I be Fuzzy_Implication, f be bijective increasing UnOp of [. 0 , 1.] st I is satisfying_(EP) holds ( ConjImpl (I,f)) is satisfying_(EP)

    proof

      let I be Fuzzy_Implication, f be bijective increasing UnOp of [. 0 , 1.];

      assume

       B0: I is satisfying_(EP);

      set g = ( ConjImpl (I,f));

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

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

      then

       BB: (I . ((f . y),(f . z))) in ( rng f) by FUNCT_2:def 3;

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

      then

       B2: (I . ((f . x),(f . z))) in ( rng f) by FUNCT_2:def 3;

      (g . (x,(g . (y,z)))) = (g . (x,((f " ) . (I . ((f . y),(f . z)))))) by BIDef

      .= ((f " ) . (I . ((f . x),(f . ((f " ) . (I . ((f . y),(f . z)))))))) by BIDef

      .= ((f " ) . (I . ((f . x),(I . ((f . y),(f . z)))))) by FUNCT_1: 35, BB

      .= ((f " ) . (I . ((f . y),(I . ((f . x),(f . z)))))) by B0, FUZIMPL2:def 2

      .= ((f " ) . (I . ((f . y),(f . ((f " ) . (I . ((f . x),(f . z)))))))) by B2, FUNCT_1: 35

      .= (g . (y,((f " ) . (I . ((f . x),(f . z)))))) by BIDef

      .= (g . (y,(g . (x,z)))) by BIDef;

      hence thesis;

    end;

    theorem :: FUZIMPL3:14

    

     Prop136c: for I be Fuzzy_Implication, f be bijective increasing UnOp of [. 0 , 1.] st I is satisfying_(IP) holds ( ConjImpl (I,f)) is satisfying_(IP)

    proof

      let I be Fuzzy_Implication, f be bijective increasing UnOp of [. 0 , 1.];

      assume

       B0: I is satisfying_(IP);

      set g = ( ConjImpl (I,f));

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

      (g . (x,x)) = ((f " ) . (I . ((f . x),(f . x)))) by BIDef

      .= ((f " ) . 1) by FUZIMPL2:def 3, B0

      .= 1 by LemmaBound;

      hence thesis;

    end;

    theorem :: FUZIMPL3:15

    

     Prop136d: for I be Fuzzy_Implication, f be bijective increasing UnOp of [. 0 , 1.] st I is satisfying_(OP) holds ( ConjImpl (I,f)) is satisfying_(OP)

    proof

      let I be Fuzzy_Implication, f be bijective increasing UnOp of [. 0 , 1.];

      assume

       B0: I is satisfying_(OP);

      set g = ( ConjImpl (I,f));

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

      

       b3: ( rng f) = [. 0 , 1.] by FUNCT_2:def 3;

      

       b4: ( dom f) = [. 0 , 1.] by FUNCT_2:def 1;

      thus (g . (x,y)) = 1 implies x <= y

      proof

        assume (g . (x,y)) = 1;

        then ((f " ) . (I . ((f . x),(f . y)))) = 1 by BIDef;

        then (f . ((f " ) . (I . ((f . x),(f . y))))) = 1 by LemmaBound;

        then (I . ((f . x),(f . y))) = 1 by FUNCT_1: 35, b3;

        then (f . x) <= (f . y) by FUZIMPL2:def 4, B0;

        then ((f " ) . (f . x)) <= ((f " ) . (f . y)) by Rosnie;

        then x <= ((f " ) . (f . y)) by b4, FUNCT_1: 34;

        hence thesis by b4, FUNCT_1: 34;

      end;

      assume x <= y;

      then (f . x) <= (f . y) by Rosnie;

      then (I . ((f . x),(f . y))) = 1 by FUZIMPL2:def 4, B0;

      then ((f " ) . (I . ((f . x),(f . y)))) = 1 by LemmaBound;

      hence thesis by BIDef;

    end;

    registration

      let I be satisfying_(NP) Fuzzy_Implication, f be bijective increasing UnOp of [. 0 , 1.];

      cluster ( ConjImpl (I,f)) -> satisfying_(NP);

      coherence by Prop136a;

    end

    registration

      let I be satisfying_(EP) Fuzzy_Implication, f be bijective increasing UnOp of [. 0 , 1.];

      cluster ( ConjImpl (I,f)) -> satisfying_(EP);

      coherence by Prop136b;

    end

    registration

      let I be satisfying_(IP) Fuzzy_Implication, f be bijective increasing UnOp of [. 0 , 1.];

      cluster ( ConjImpl (I,f)) -> satisfying_(IP);

      coherence by Prop136c;

    end

    registration

      let I be satisfying_(OP) Fuzzy_Implication, f be bijective increasing UnOp of [. 0 , 1.];

      cluster ( ConjImpl (I,f)) -> satisfying_(OP);

      coherence by Prop136d;

    end

    theorem :: FUZIMPL3:16

    for I be Fuzzy_Implication, f be bijective increasing UnOp of [. 0 , 1.] holds ( ConjImpl (I,f)) = (((f " ) * I) * [:f, f:])

    proof

      let I be Fuzzy_Implication, f be bijective increasing UnOp of [. 0 , 1.];

      set g = ( ConjImpl (I,f));

      ( dom g) = [: [. 0 , 1.], [. 0 , 1.]:] by FUNCT_2:def 1;

      then

       A1: ( dom g) = ( dom (((f " ) * I) * [:f, f:])) by FUNCT_2:def 1;

      

       C2: ( dom f) = [. 0 , 1.] by FUNCT_2:def 1;

      for x be object st x in ( dom g) holds (g . x) = ((((f " ) * I) * [:f, f:]) . x)

      proof

        let x be object;

        assume x in ( dom g);

        then

         W1: x in [: [. 0 , 1.], [. 0 , 1.]:] by FUNCT_2:def 1;

        then

        consider x1,x2 be object such that

         C0: x1 in [. 0 , 1.] & x2 in [. 0 , 1.] & x = [x1, x2] by ZFMISC_1:def 2;

        reconsider x1, x2 as Element of [. 0 , 1.] by C0;

        

         D1: x in ( dom [:f, f:]) by W1, FUNCT_2:def 1;

        

         X2: ( dom I) = [: [. 0 , 1.], [. 0 , 1.]:] by FUNCT_2:def 1;

         [(f . x1), (f . x2)] in [: [. 0 , 1.], [. 0 , 1.]:] by ZFMISC_1: 87;

        then ( [:f, f:] . (x1,x2)) in ( dom I) by X2;

        then

         D2: ( [:f, f:] . x) in ( dom I) by C0, BINOP_1:def 1;

        (g . x) = (g . (x1,x2)) by C0, BINOP_1:def 1

        .= ((f " ) . (I . ((f . x1),(f . x2)))) by BIDef

        .= ((f " ) . (I . [(f . x1), (f . x2)])) by BINOP_1:def 1

        .= ((f " ) . (I . ( [:f, f:] . (x1,x2)))) by C2, FUNCT_3:def 8

        .= ((f " ) . (I . ( [:f, f:] . x))) by C0, BINOP_1:def 1

        .= (((f " ) * I) . ( [:f, f:] . x)) by FUNCT_1: 13, D2

        .= ((((f " ) * I) * [:f, f:]) . x) by FUNCT_1: 13, D1;

        hence thesis;

      end;

      hence thesis by A1, FUNCT_1: 2;

    end;

    begin

    definition

      let N be UnOp of [. 0 , 1.];

      :: FUZIMPL3:def4

      attr N is satisfying_(N1) means

      : N1Def: (N . 0 ) = 1 & (N . 1) = 0 ;

      :: FUZIMPL3:def5

      attr N is satisfying_(N2) means

      : N2Def: N is non-increasing;

    end

    definition

      :: FUZIMPL3:def6

      func N_CC -> UnOp of [. 0 , 1.] means

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

      existence

      proof

        deffunc F( Real) = (1 - $1);

        

         A1: for a be Element of [. 0 , 1.] holds F(a) in [. 0 , 1.] by FUZNORM1: 7;

        ex f be UnOp of [. 0 , 1.] st for a be Element of [. 0 , 1.] holds (f . a) = F(a) from FUNCT_2:sch 8( A1);

        hence thesis;

      end;

      uniqueness

      proof

        deffunc F( Real) = (1 - $1);

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

        for o1,o2 be UnOp of A st (for a be Element of A holds (o1 . a) = F(a)) & (for a be Element of A holds (o2 . a) = F(a)) holds o1 = o2 from LMOD_7:sch 2;

        hence thesis;

      end;

    end

    registration

      cluster N_CC -> satisfying_(N1) satisfying_(N2);

      coherence

      proof

        set g = N_CC ;

        

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

        

        then

         T1: (g . 0 ) = (1 - 0 ) by NDef

        .= 1;

        

         a1: (g . 1) = (1 - 1) by T0, NDef

        .= 0 ;

        for a,b be Element of [. 0 , 1.] st a <= b holds (g . a) >= (g . b)

        proof

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

          assume

           Y0: a <= b;

          (g . a) = (1 - a) & (g . b) = (1 - b) by NDef;

          hence thesis by Y0, XREAL_1: 13;

        end;

        hence thesis by a1, NonInc, T1;

      end;

    end

    registration

      cluster N_CC -> bijective decreasing;

      coherence

      proof

        set f = N_CC ;

        

         B1: [. 0 , 1.] c= ( rng f)

        proof

          let x be object;

          assume x in [. 0 , 1.];

          then

          reconsider xx = x as Element of [. 0 , 1.];

          set y = (1 - xx);

          

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

          then

           B2: y in ( dom f) by FUNCT_2:def 1;

          (f . y) = (1 - y) by NDef, B3

          .= xx;

          hence thesis by B2, FUNCT_1:def 3;

        end;

        

         a0: ( rng f) c= [. 0 , 1.] by RELAT_1:def 19;

        for x1,x2 be object st x1 in ( dom f) & x2 in ( dom f) & (f . x1) = (f . x2) holds x1 = x2

        proof

          let x1,x2 be object;

          assume

           A1: x1 in ( dom f) & x2 in ( dom f) & (f . x1) = (f . x2);

          then

          reconsider xx1 = x1, xx2 = x2 as Element of [. 0 , 1.] by FUNCT_2:def 1;

          (f . xx1) = (1 - xx1) & (f . xx2) = (1 - xx2) by NDef;

          then (1 - xx1) = (1 - xx2) by A1;

          hence thesis;

        end;

        then f is one-to-one onto by a0, FUNCT_1:def 4, FUNCT_2:def 3, B1, XBOOLE_0:def 10;

        hence f is bijective;

        for a,b be Element of [. 0 , 1.] st a < b holds (f . a) > (f . b)

        proof

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

          assume

           S0: a < b;

          

           S1: (f . a) = (1 - a) & (f . b) = (1 - b) by NDef;

          ( - a) > ( - b) by S0, XREAL_1: 24;

          hence thesis by S1, XREAL_1: 6;

        end;

        hence f is decreasing by Decreas;

      end;

    end

    registration

      cluster bijective decreasing for UnOp of [. 0 , 1.];

      existence

      proof

        take f = N_CC ;

        thus thesis;

      end;

    end

    registration

      cluster satisfying_(N1) satisfying_(N2) for UnOp of [. 0 , 1.];

      existence

      proof

        take N_CC ;

        thus thesis;

      end;

    end

    definition

      mode Fuzzy_Negation is satisfying_(N1) satisfying_(N2) UnOp of [. 0 , 1.];

    end

    definition

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

      :: FUZIMPL3:def7

      attr f is continuous means ex g be Function of I[01] , I[01] st f = g & g is continuous;

    end

    definition

      let N be UnOp of [. 0 , 1.];

      :: FUZIMPL3:def8

      attr N is involutive means for x be Element of [. 0 , 1.] holds (N . (N . x)) = x;

    end

    definition

      let N be UnOp of [. 0 , 1.];

      :: FUZIMPL3:def9

      attr N is satisfying_(N3) means N is decreasing;

      :: FUZIMPL3:def10

      attr N is satisfying_(N4) means N is continuous;

      :: FUZIMPL3:def11

      attr N is satisfying_(N5) means N is involutive;

    end

    definition

      let N be UnOp of [. 0 , 1.];

      :: FUZIMPL3:def12

      attr N is negation-strict means N is satisfying_(N3) satisfying_(N4);

    end

    definition

      let N be UnOp of [. 0 , 1.];

      :: FUZIMPL3:def13

      attr N is negation-strong means N is satisfying_(N5);

      :: FUZIMPL3:def14

      attr N is non-vanishing means for x be Element of [. 0 , 1.] holds (N . x) = 0 iff x = 1;

      :: FUZIMPL3:def15

      attr N is non-filling means for x be Element of [. 0 , 1.] holds (N . x) = 1 iff x = 0 ;

    end

    begin

    theorem :: FUZIMPL3:17

    for f be decreasing bijective UnOp of [. 0 , 1.] holds (f . 0 ) = 1 & (f . 1) = 0

    proof

      let f be decreasing bijective UnOp of [. 0 , 1.];

      

       KK: (f . 0 ) = 1

      proof

        set y = (f . 0 );

        set X = [. 0 , 1.];

        

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

        reconsider y as Element of [. 0 , 1.] by XXREAL_1: 1, FUNCT_2: 5;

        assume

         H0: (f . 0 ) <> 1;

        

         I3: ( rng f) = X by FUNCT_2:def 3;

        reconsider z = ((f " ) . 1) as Element of [. 0 , 1.] by XXREAL_1: 1, FUNCT_2: 5;

        

         L1: (f . z) = 1 by FUNCT_1: 35, I3, K1;

        then

        consider zz be Element of [. 0 , 1.] such that

         L2: zz < z by Wazne1, H0;

        (f . zz) > (f . z) by L2, Decreas;

        hence contradiction by L1, XXREAL_1: 1;

      end;

      (f . 1) = 0

      proof

        set X = [. 0 , 1.];

        

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

        reconsider y = (f . 1) as Element of [. 0 , 1.] by XXREAL_1: 1, FUNCT_2: 5;

        assume

         H0: (f . 1) <> 0 ;

        

         I3: ( rng f) = X by FUNCT_2:def 3;

        reconsider z = ((f " ) . 0 ) as Element of [. 0 , 1.] by XXREAL_1: 1, FUNCT_2: 5;

        

         L1: (f . z) = 0 by FUNCT_1: 35, I3, K1;

        then

        consider zz be Element of [. 0 , 1.] such that

         L2: zz > z by Wazne2, H0;

        (f . zz) < (f . z) by L2, Decreas;

        hence contradiction by L1, XXREAL_1: 1;

      end;

      hence thesis by KK;

    end;

    definition

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

      :: FUZIMPL3:def16

      func FNegation I -> UnOp of [. 0 , 1.] means

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

      existence

      proof

        deffunc F( Real) = (I . ($1, 0 ));

        

         A1: for a be Element of [. 0 , 1.] holds F(a) in [. 0 , 1.] by FUZNORM1: 15;

        ex f be UnOp of [. 0 , 1.] st for a be Element of [. 0 , 1.] holds (f . a) = F(a) from FUNCT_2:sch 8( A1);

        hence thesis;

      end;

      uniqueness

      proof

        deffunc F( Real) = (I . ($1, 0 ));

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

        for o1,o2 be UnOp of A st (for a be Element of A holds (o1 . a) = F(a)) & (for a be Element of A holds (o2 . a) = F(a)) holds o1 = o2 from LMOD_7:sch 2;

        hence thesis;

      end;

    end

    registration

      let I be satisfying_(I1) satisfying_(I3) satisfying_(I5) BinOp of [. 0 , 1.];

      cluster ( FNegation I) -> satisfying_(N1) satisfying_(N2);

      coherence

      proof

        set g = ( FNegation I);

        

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

        

        then

         T1: (g . 0 ) = (I . ( 0 , 0 )) by FNeg

        .= 1 by FUZIMPL1:def 3;

        

         a1: (g . 1) = (I . (1, 0 )) by T0, FNeg

        .= 0 by FUZIMPL1:def 5;

        for a,b be Element of [. 0 , 1.] st a <= b holds (g . a) >= (g . b)

        proof

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

          assume

           Y0: a <= b;

          (g . a) = (I . (a, 0 )) & (g . b) = (I . (b, 0 )) by FNeg;

          hence thesis by Y0, T0, FUZIMPL1:def 1;

        end;

        hence thesis by a1, T1, NonInc;

      end;

    end

    theorem :: FUZIMPL3:18

    for I be Fuzzy_Implication holds ( FNegation I) is Fuzzy_Negation;

    begin

    definition

      :: FUZIMPL3:def17

      func NegationD1 -> UnOp of [. 0 , 1.] means

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

      existence

      proof

        defpred C[ object] means $1 = 0 ;

        deffunc F( object) = 1;

        deffunc G( object) = 0 ;

        

         A1: for x be object st x in [. 0 , 1.] holds ( C[x] implies F(x) in [. 0 , 1.]) & ( not C[x] implies G(x) in [. 0 , 1.]) by XXREAL_1: 1;

        ex f be Function of [. 0 , 1.], [. 0 , 1.] st for x be object st x in [. 0 , 1.] holds ( C[x] implies (f . x) = F(x)) & ( not C[x] implies (f . x) = G(x)) from FUNCT_2:sch 5( A1);

        then

        consider f be Function of [. 0 , 1.], [. 0 , 1.] such that

         B1: for x be object st x in [. 0 , 1.] holds ( C[x] implies (f . x) = F(x)) & ( not C[x] implies (f . x) = G(x));

        take f;

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

        thus x = 0 implies (f . x) = 1 by B1;

        assume x <> 0 ;

        hence thesis by B1;

      end;

      uniqueness

      proof

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

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

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

        for x be Element of [. 0 , 1.] holds (f1 . x) = (f2 . x)

        proof

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

          per cases ;

            suppose

             D1: x = 0 ;

            

            hence (f1 . x) = 1 by A1

            .= (f2 . x) by D1, A2;

          end;

            suppose

             D1: x <> 0 ;

            

            hence (f1 . x) = 0 by A1

            .= (f2 . x) by D1, A2;

          end;

        end;

        hence thesis by FUNCT_2: 63;

      end;

      :: FUZIMPL3:def18

      func NegationD2 -> UnOp of [. 0 , 1.] means

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

      existence

      proof

        defpred C[ object] means $1 = 1;

        deffunc F( object) = 0 ;

        deffunc G( object) = 1;

        

         A1: for x be object st x in [. 0 , 1.] holds ( C[x] implies F(x) in [. 0 , 1.]) & ( not C[x] implies G(x) in [. 0 , 1.]) by XXREAL_1: 1;

        ex f be Function of [. 0 , 1.], [. 0 , 1.] st for x be object st x in [. 0 , 1.] holds ( C[x] implies (f . x) = F(x)) & ( not C[x] implies (f . x) = G(x)) from FUNCT_2:sch 5( A1);

        then

        consider f be Function of [. 0 , 1.], [. 0 , 1.] such that

         B1: for x be object st x in [. 0 , 1.] holds ( C[x] implies (f . x) = F(x)) & ( not C[x] implies (f . x) = G(x));

        take f;

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

        thus x = 1 implies (f . x) = 0 by B1;

        assume x <> 1;

        hence thesis by B1;

      end;

      uniqueness

      proof

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

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

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

        for x be Element of [. 0 , 1.] holds (f1 . x) = (f2 . x)

        proof

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

          per cases ;

            suppose

             D1: x = 1;

            

            hence (f1 . x) = 0 by A1

            .= (f2 . x) by D1, A2;

          end;

            suppose

             D1: x <> 1;

            

            hence (f1 . x) = 1 by A1

            .= (f2 . x) by D1, A2;

          end;

        end;

        hence thesis by FUNCT_2: 63;

      end;

    end

    definition

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

      :: FUZIMPL3:def19

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

    end

    registration

      cluster NegationD1 -> satisfying_(N1) satisfying_(N2);

      coherence

      proof

        set f = NegationD1 ;

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

        hence f is satisfying_(N1) by D1Def;

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

        proof

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

          assume

           B2: x <= y;

          per cases ;

            suppose x = 0 ;

            then (f . x) = 1 by D1Def;

            hence thesis by XXREAL_1: 1;

          end;

            suppose

             B1: x <> 0 ;

            then

             B3: (f . x) = 0 by D1Def;

            x > 0 by B1, XXREAL_1: 1;

            hence thesis by B3, D1Def, B2;

          end;

        end;

        hence thesis by NonInc;

      end;

      cluster NegationD2 -> satisfying_(N1) satisfying_(N2);

      coherence

      proof

        set f = NegationD2 ;

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

        hence f is satisfying_(N1) by D2Def;

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

        proof

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

          assume

           B2: x <= y;

          per cases ;

            suppose y = 1;

            then (f . y) = 0 by D2Def;

            hence thesis by XXREAL_1: 1;

          end;

            suppose

             B1: y <> 1;

            then

             B3: (f . y) = 1 by D2Def;

            y <= 1 by XXREAL_1: 1;

            then y < 1 by B1, XXREAL_0: 1;

            hence thesis by B3, D2Def, B2;

          end;

        end;

        hence thesis by NonInc;

      end;

    end

    theorem :: FUZIMPL3:19

    for N be Fuzzy_Negation holds NegationD1 <= N <= NegationD2

    proof

      set f = NegationD1 ;

      set g = NegationD2 ;

      let N be Fuzzy_Negation;

      thus f <= N

      proof

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

        per cases ;

          suppose

           A1: x = 0 ;

          then (f . x) = 1 by D1Def;

          hence thesis by A1, N1Def;

        end;

          suppose x <> 0 ;

          then (f . x) = 0 by D1Def;

          hence thesis by XXREAL_1: 1;

        end;

      end;

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

      per cases ;

        suppose

         A1: x = 1;

        then (N . x) = 0 by N1Def;

        hence thesis by A1, D2Def;

      end;

        suppose x <> 1;

        then (g . x) = 1 by D2Def;

        hence thesis by XXREAL_1: 1;

      end;

    end;

    begin

    theorem :: FUZIMPL3:20

    ( FNegation I_LK ) = N_CC

    proof

      set I = I_LK ;

      set f = ( FNegation I);

      set g = N_CC ;

      

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

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

      proof

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

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

        then

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

        (f . x) = (I . (x, 0 )) by FNeg

        .= ( min (1,((1 - x) + 0 ))) by A1, FUZIMPL1:def 14

        .= (1 - x) by A2, XXREAL_0:def 9

        .= (g . x) by NDef;

        hence thesis;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: FUZIMPL3:21

    ( FNegation I_GD ) = NegationD1

    proof

      set I = I_GD ;

      set f = ( FNegation I);

      set g = NegationD1 ;

      

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

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

      proof

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

        per cases ;

          suppose

           B1: x <= 0 ;

          then

           B2: x = 0 by XXREAL_1: 1;

          (f . x) = (I . (x, 0 )) by FNeg

          .= 1 by FUZIMPL1:def 16, B1, A1

          .= (g . x) by D1Def, B2;

          hence thesis;

        end;

          suppose

           B1: x > 0 ;

          (f . x) = (I . (x, 0 )) by FNeg

          .= 0 by A1, B1, FUZIMPL1:def 16

          .= (g . x) by D1Def, B1;

          hence thesis;

        end;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: FUZIMPL3:22

    ( FNegation I_RC ) = N_CC

    proof

      set I = I_RC ;

      set f = ( FNegation I);

      set g = N_CC ;

      

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

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

      proof

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

        (f . x) = (I . (x, 0 )) by FNeg

        .= ((1 - x) + (x * 0 )) by FUZIMPL1:def 17, A1

        .= (g . x) by NDef;

        hence thesis;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: FUZIMPL3:23

    ( FNegation I_KD ) = N_CC

    proof

      set I = I_KD ;

      set f = ( FNegation I);

      set g = N_CC ;

      

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

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

      proof

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

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

        then

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

        (f . x) = (I . (x, 0 )) by FNeg

        .= ( max ((1 - x), 0 )) by FUZIMPL1:def 18, A1

        .= (1 - x) by A2, XXREAL_0:def 10

        .= (g . x) by NDef;

        hence thesis;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: FUZIMPL3:24

    ( FNegation I_GG ) = NegationD1

    proof

      set I = I_GG ;

      set f = ( FNegation I);

      set g = NegationD1 ;

      

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

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

      proof

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

        per cases ;

          suppose

           B1: x <= 0 ;

          then

           B2: x = 0 by XXREAL_1: 1;

          (f . x) = (I . (x, 0 )) by FNeg

          .= 1 by FUZIMPL1:def 19, B1, A1

          .= (g . x) by D1Def, B2;

          hence thesis;

        end;

          suppose

           B1: x > 0 ;

          (f . x) = (I . (x, 0 )) by FNeg

          .= ( 0 / x) by A1, B1, FUZIMPL1:def 19

          .= (g . x) by D1Def, B1;

          hence thesis;

        end;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: FUZIMPL3:25

    ( FNegation I_RS ) = NegationD1

    proof

      set I = I_RS ;

      set f = ( FNegation I);

      set g = NegationD1 ;

      

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

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

      proof

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

        per cases ;

          suppose

           B1: x <= 0 ;

          then

           B2: x = 0 by XXREAL_1: 1;

          (f . x) = (I . (x, 0 )) by FNeg

          .= 1 by FUZIMPL1:def 20, B1, A1

          .= (g . x) by D1Def, B2;

          hence thesis;

        end;

          suppose

           B1: x > 0 ;

          (f . x) = (I . (x, 0 )) by FNeg

          .= 0 by A1, B1, FUZIMPL1:def 20

          .= (g . x) by D1Def, B1;

          hence thesis;

        end;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: FUZIMPL3:26

    ( FNegation I_YG ) = NegationD1

    proof

      set I = I_YG ;

      set f = ( FNegation I);

      set g = NegationD1 ;

      

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

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

      proof

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

        per cases ;

          suppose x <= 0 ;

          then

           B2: x = 0 by XXREAL_1: 1;

          (f . x) = (I . (x, 0 )) by FNeg

          .= 1 by FUZIMPL1:def 21, B2

          .= (g . x) by D1Def, B2;

          hence thesis;

        end;

          suppose

           B1: x > 0 ;

          (f . x) = (I . (x, 0 )) by FNeg

          .= ( 0 to_power x) by A1, B1, FUZIMPL1:def 21

          .= 0 by B1, POWER:def 2

          .= (g . x) by D1Def, B1;

          hence thesis;

        end;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: FUZIMPL3:27

    ( FNegation I_WB ) = NegationD2

    proof

      set I = I_WB ;

      set f = ( FNegation I);

      set g = NegationD2 ;

      

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

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

      proof

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

        x <= 1 by XXREAL_1: 1;

        per cases by XXREAL_0: 1;

          suppose

           B1: x < 1;

          (f . x) = (I . (x, 0 )) by FNeg

          .= 1 by FUZIMPL1:def 22, B1, A1

          .= (g . x) by D2Def, B1;

          hence thesis;

        end;

          suppose

           B1: x = 1;

          (f . x) = (I . (x, 0 )) by FNeg

          .= 0 by A1, B1, FUZIMPL1:def 22

          .= (g . x) by D2Def, B1;

          hence thesis;

        end;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: FUZIMPL3:28

    ( FNegation I_FD ) = N_CC

    proof

      set I = I_FD ;

      set f = ( FNegation I);

      set g = N_CC ;

      

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

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

      proof

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

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

        then

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

        per cases ;

          suppose x <= 0 ;

          then

           B2: x = 0 by XXREAL_1: 1;

          (f . x) = (I . (x, 0 )) by FNeg

          .= (1 - x) by FUZIMPL1:def 23, B2

          .= (g . x) by NDef;

          hence thesis;

        end;

          suppose

           B1: x > 0 ;

          (f . x) = (I . (x, 0 )) by FNeg

          .= ( max ((1 - x), 0 )) by A1, B1, FUZIMPL1:def 23

          .= (1 - x) by XXREAL_0:def 10, A2

          .= (g . x) by NDef;

          hence thesis;

        end;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: FUZIMPL3:29

    for I be satisfying_(EP) satisfying_(OP) BinOp of [. 0 , 1.] holds ( FNegation I) is Fuzzy_Negation;

    theorem :: FUZIMPL3:30

    

     Prop1417ii: for I be satisfying_(EP) satisfying_(OP) BinOp of [. 0 , 1.] holds for x be Element of [. 0 , 1.] holds x <= (( FNegation I) . (( FNegation I) . x))

    proof

      let I be satisfying_(EP) satisfying_(OP) BinOp of [. 0 , 1.];

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

      set f = ( FNegation I);

      

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

      (f . x) in [. 0 , 1.];

      then

       A2: (I . (x, 0 )) in [. 0 , 1.] by FNeg;

      

      then

       a7: (I . (x,(I . ((I . (x, 0 )), 0 )))) = (I . ((I . (x, 0 )),(I . (x, 0 )))) by A1, FUZIMPL2:def 2

      .= 1 by A2, FUZIMPL2:def 3;

      (I . ((I . (x, 0 )), 0 )) = (I . ((f . x), 0 )) by FNeg

      .= (f . (f . x)) by FNeg;

      hence thesis by a7, FUZIMPL2:def 4;

    end;

    theorem :: FUZIMPL3:31

    for I be satisfying_(EP) satisfying_(OP) BinOp of [. 0 , 1.] holds ((( FNegation I) * ( FNegation I)) * ( FNegation I)) = ( FNegation I)

    proof

      let I be satisfying_(EP) satisfying_(OP) BinOp of [. 0 , 1.];

      set f = ( FNegation I);

      now

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

        f is non-increasing by N2Def;

        then

         R2: (f . (f . (f . x))) <= (f . x) by NonInc, Prop1417ii;

        

         v1: (f . x) = (I . (x, 0 )) by FNeg;

        

         v2: (I . ((I . ((I . (x, 0 )), 0 )), 0 )) = (I . ((I . ((f . x), 0 )), 0 )) by FNeg

        .= (I . ((f . (f . x)), 0 )) by FNeg

        .= (f . (f . (f . x))) by FNeg;

        

         vz: (f . (f . x)) = (I . ((I . (x, 0 )), 0 )) by FNeg, v1;

        

         r1: ( dom (f * f)) = [. 0 , 1.] by FUNCT_2:def 1;

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

        

        then (I . ((I . (x, 0 )),(I . ((I . ((I . (x, 0 )), 0 )), 0 )))) = (I . ((I . ((I . (x, 0 )), 0 )),(I . ((I . (x, 0 )), 0 )))) by FUZIMPL2:def 2, vz, v1

        .= 1 by vz, FUZIMPL2:def 3;

        then (f . x) <= (I . ((I . ((f . x), 0 )), 0 )) by v1, v2, FUZIMPL2:def 4;

        then (f . x) <= (I . ((f . (f . x)), 0 )) by FNeg;

        then (f . x) <= (f . (f . (f . x))) by FNeg;

        then (f . x) = (f . (f . (f . x))) by R2, XXREAL_0: 1;

        

        then (f . x) = (f . ((f * f) . x)) by r1, FUNCT_1: 12

        .= ((f * (f * f)) . x) by FUNCT_1: 13, r1;

        hence (((f * f) * f) . x) = (f . x) by RELAT_1: 36;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    begin

    definition

      let x,l be Real;

      :: FUZIMPL3:def20

      attr l is x _greater means

      : GreatDef: l > x;

    end

    registration

      cluster ( - 1) _greater for Real;

      existence

      proof

        take 0 ;

        thus thesis;

      end;

    end

    definition

      let l be Real;

      assume

       A0: l > ( - 1);

      :: FUZIMPL3:def21

      func SugenoNegation l -> UnOp of [. 0 , 1.] means

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

      existence

      proof

        deffunc F( Real) = ((1 - $1) / (1 + (l * $1)));

        

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

        proof

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

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

          then

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

          

           B3: a >= 0 by XXREAL_1: 1;

          then (l * a) >= (( - 1) * a) by A0, XREAL_1: 64;

          then

           b1: (1 + (l * a)) >= (1 - (1 * a)) by XREAL_1: 6;

          (( - 1) * a) <= (l * a) by A0, B3, XREAL_1: 64;

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

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

          hence thesis by B2, b1, XXREAL_1: 1;

        end;

        ex f be UnOp of [. 0 , 1.] st for a be Element of [. 0 , 1.] holds (f . a) = F(a) from FUNCT_2:sch 8( A1);

        hence thesis;

      end;

      uniqueness

      proof

        deffunc F( Real) = ((1 - $1) / (1 + (l * $1)));

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

        for o1,o2 be UnOp of A st (for a be Element of A holds (o1 . a) = F(a)) & (for a be Element of A holds (o2 . a) = F(a)) holds o1 = o2 from LMOD_7:sch 2;

        hence thesis;

      end;

    end

    theorem :: FUZIMPL3:32

     N_CC = ( SugenoNegation 0 )

    proof

      set f = N_CC , g = ( SugenoNegation 0 );

      for x be object st x in [. 0 , 1.] holds (f . x) = (g . x)

      proof

        let x be object;

        assume x in [. 0 , 1.];

        then

        reconsider xx = x as Element of [. 0 , 1.];

        (g . xx) = ((1 - xx) / (1 + ( 0 * xx))) by DefSugeno

        .= (f . xx) by NDef;

        hence thesis;

      end;

      hence thesis by FUNCT_2: 12;

    end;

    registration

      let r be ( - 1) _greater Real;

      cluster ( SugenoNegation r) -> satisfying_(N1) satisfying_(N2);

      coherence

      proof

        set f = ( SugenoNegation r);

        

         AA: r > ( - 1) by GreatDef;

        

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

        

        then

         AJ: (f . 0 ) = ((1 - 0 ) / (1 + (r * 0 ))) by DefSugeno, AA

        .= 1;

        (f . 1) = ((1 - 1) / (1 + (r * 1))) by DefSugeno, AA, AB

        .= 0 ;

        hence f is satisfying_(N1) by AJ;

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

        proof

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

          assume

           B2: x <= y;

          set m = ((1 + (r * x)) * (1 + (r * y)));

          

           t1: (y - x) >= (x - x) by B2, XREAL_1: 6;

          

           St: (1 + r) > (1 + ( - 1)) by GreatDef, XREAL_1: 6;

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

          then

           S2: (1 + (r * x)) > 0 by LemmaImp, GreatDef;

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

          then

           S1: (1 + (r * y)) > 0 by LemmaImp, GreatDef;

          

           R1: (f . x) = ((1 - x) / (1 + (r * x))) by DefSugeno, AA

          .= (((1 - x) * (1 + (r * y))) / ((1 + (r * x)) * (1 + (r * y)))) by XCMPLX_1: 91, S1;

          

           R2: (f . y) = ((1 - y) / (1 + (r * y))) by DefSugeno, AA

          .= (((1 - y) * (1 + (r * x))) / ((1 + (r * x)) * (1 + (r * y)))) by XCMPLX_1: 91, S2;

          ((f . x) - (f . y)) = (((y - x) * (1 + r)) / m) by R1, R2;

          then (((f . x) - (f . y)) + (f . y)) >= ( 0 + (f . y)) by S1, XREAL_1: 6, t1, St, S2;

          hence thesis;

        end;

        hence thesis by NonInc;

      end;

    end

    begin

    definition

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

      let h be bijective increasing UnOp of [. 0 , 1.];

      :: FUZIMPL3:def22

      func ConjNeg (f,h) -> UnOp of [. 0 , 1.] means

      : CNDef: for x be Element of [. 0 , 1.] holds (it . x) = ((h " ) . (f . (h . x)));

      existence

      proof

        deffunc F( Real) = ((h " ) . (f . (h . $1)));

        

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

        proof

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

          ((h " ) . (f . (h . a))) in [. 0 , 1.];

          hence thesis;

        end;

        ex f be UnOp of [. 0 , 1.] st for a be Element of [. 0 , 1.] holds (f . a) = F(a) from FUNCT_2:sch 8( A1);

        hence thesis;

      end;

      uniqueness

      proof

        deffunc F( Real) = ((h " ) . (f . (h . $1)));

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

        for o1,o2 be UnOp of A st (for a be Element of A holds (o1 . a) = F(a)) & (for a be Element of A holds (o2 . a) = F(a)) holds o1 = o2 from LMOD_7:sch 2;

        hence thesis;

      end;

    end

    theorem :: FUZIMPL3:33

    for I be Fuzzy_Negation, f be bijective increasing UnOp of [. 0 , 1.] holds ( ConjNeg (I,f)) = (((f " ) * I) * f)

    proof

      let I be Fuzzy_Negation, f be bijective increasing UnOp of [. 0 , 1.];

      set g = ( ConjNeg (I,f));

      

       AA: ( dom f) = [. 0 , 1.] by FUNCT_2:def 1;

      

       A0: ( dom g) = [. 0 , 1.] by FUNCT_2:def 1;

      

       A1: ( dom g) = ( dom (((f " ) * I) * f)) by A0, FUNCT_2:def 1;

      for x be object st x in ( dom g) holds (g . x) = ((((f " ) * I) * f) . x)

      proof

        let x be object;

        assume x in ( dom g);

        then

        reconsider x as Element of [. 0 , 1.] by FUNCT_2:def 1;

        (f . x) in [. 0 , 1.];

        then

         AB: (f . x) in ( dom I) by FUNCT_2:def 1;

        (g . x) = ((f " ) . (I . (f . x))) by CNDef

        .= (((f " ) * I) . (f . x)) by FUNCT_1: 13, AB

        .= ((((f " ) * I) * f) . x) by FUNCT_1: 13, AA;

        hence thesis;

      end;

      hence thesis by A1, FUNCT_1: 2;

    end;

    definition

      let f,g be UnOp of [. 0 , 1.];

      :: FUZIMPL3:def23

      pred f,g are_conjugate means ex h be bijective increasing UnOp of [. 0 , 1.] st g = ( ConjNeg (f,h));

    end

    registration

      let N be Fuzzy_Negation, h be bijective increasing UnOp of [. 0 , 1.];

      cluster ( ConjNeg (N,h)) -> satisfying_(N1) satisfying_(N2);

      coherence

      proof

        set CN = ( ConjNeg (N,h));

        

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

        

        then

         A0: (CN . 0 ) = ((h " ) . (N . (h . 0 ))) by CNDef

        .= ((h " ) . (N . 0 )) by LemmaBound

        .= ((h " ) . 1) by N1Def

        .= 1 by LemmaBound;

        

         A1: (CN . 1) = ((h " ) . (N . (h . 1))) by AA, CNDef

        .= ((h " ) . (N . 1)) by LemmaBound

        .= ((h " ) . 0 ) by N1Def

        .= 0 by LemmaBound;

        for a,b be Element of [. 0 , 1.] st a <= b holds (CN . a) >= (CN . b)

        proof

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

          assume a <= b;

          then (h . a) <= (h . b) by Rosnie;

          then

           B1: (N . (h . a)) >= (N . (h . b)) by N2Def, NonInc;

          

           B2: (CN . a) = ((h " ) . (N . (h . a))) by CNDef;

          (CN . b) = ((h " ) . (N . (h . b))) by CNDef;

          hence thesis by Rosnie, B1, B2;

        end;

        hence thesis by A0, A1, NonInc;

      end;

    end

    theorem :: FUZIMPL3:34

    for I be Fuzzy_Implication, h be bijective increasing UnOp of [. 0 , 1.] holds ( ConjNeg (( FNegation I),h)) = ( FNegation ( ConjImpl (I,h)))

    proof

      let I be Fuzzy_Implication, h be bijective increasing UnOp of [. 0 , 1.];

      set f = ( ConjNeg (( FNegation I),h));

      set g = ( FNegation ( ConjImpl (I,h)));

      

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

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

      proof

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

        (f . x) = ((h " ) . (( FNegation I) . (h . x))) by CNDef

        .= ((h " ) . (I . ((h . x), 0 ))) by FNeg

        .= ((h " ) . (I . ((h . x),(h . 0 )))) by LemmaBound

        .= (( ConjImpl (I,h)) . (x, 0 )) by AA, BIDef

        .= (g . x) by FNeg;

        hence thesis;

      end;

      hence thesis by FUNCT_2: 63;

    end;