The Mizar article:

Propositional Calculus for Boolean Valued Functions. Part IV

by
Shunichi Kobayashi

Received April 23, 1999

Copyright (c) 1999 Association of Mizar Users

MML identifier: BVFUNC_8
[ MML identifier index ]


environ

 vocabulary FUNCT_2, MARGREL1, BVFUNC_1, ZF_LANG, FUNCT_1, RELAT_1, BINARITH,
      PARTIT1;
 notation TARSKI, XBOOLE_0, SUBSET_1, MARGREL1, VALUAT_1, RELAT_1, FUNCT_1,
      FRAENKEL, BINARITH, BVFUNC_1;
 constructors BINARITH, BVFUNC_1;
 clusters MARGREL1, VALUAT_1, BINARITH, FRAENKEL;
 requirements SUBSET, BOOLE;
 definitions BVFUNC_1;
 theorems FUNCT_1, FUNCT_2, MARGREL1, BINARITH, BVFUNC_1, BVFUNC_4, VALUAT_1;

begin

::Chap. 1  Propositional Calculus

reserve Y for non empty set;

theorem for a,b,c,d being Element of Funcs(Y,BOOLEAN) holds
a 'imp' (b '&' c '&' d) = (a 'imp' b) '&' (a 'imp' c) '&' (a 'imp' d)
proof
  let a,b,c,d be Element of Funcs(Y,BOOLEAN);
  A1:for x being Element of Y holds
   Pj(a 'imp' (b '&' c '&' d),x) =
   Pj((a 'imp' b) '&' (a 'imp' c) '&' (a 'imp' d),x)
  proof
    let x be Element of Y;
      Pj((a 'imp' b) '&' (a 'imp' c) '&' (a 'imp' d),x)
   =Pj((a 'imp' b) '&' (a 'imp' c),x) '&' Pj(a 'imp' d,x) by VALUAT_1:def 6
  .=Pj(a 'imp' b,x) '&' Pj(a 'imp' c,x) '&' Pj(a 'imp' d,x) by VALUAT_1:def 6
  .=('not' Pj(a,x) 'or' Pj(b,x)) '&' Pj(a 'imp' c,x) '&' Pj(a 'imp' d,x)
   by BVFUNC_1:def 11
  .=('not' Pj(a,x) 'or' Pj(b,x)) '&' ('not'
Pj(a,x) 'or' Pj(c,x)) '&' Pj(a 'imp' d,x)
   by BVFUNC_1:def 11
  .=('not' Pj(a,x) 'or' Pj(b,x)) '&' ('not' Pj(a,x) 'or' Pj(c,x)) '&'
    ('not' Pj(a,x) 'or' Pj(d,x))
   by BVFUNC_1:def 11
  .=('not' Pj(a,x) 'or' (Pj(b,x) '&' Pj(c,x))) '&' ('not' Pj(a,x) 'or' Pj(d,x))
   by BINARITH:23
  .='not' Pj(a,x) 'or' (Pj(b,x) '&' Pj(c,x) '&' Pj(d,x))
   by BINARITH:23
  .='not' Pj(a,x) 'or' (Pj(b '&' c,x) '&' Pj(d,x)) by VALUAT_1:def 6
  .='not' Pj(a,x) 'or' (Pj(b '&' c '&' d,x)) by VALUAT_1:def 6
  .=Pj(a 'imp' (b '&' c '&' d),x) by BVFUNC_1:def 11;
    hence thesis;
  end;
  consider k3 being Function such that
    A2: (a 'imp' (b '&' c '&' d))=k3 & dom k3=Y & rng k3 c= BOOLEAN
                     by FUNCT_2:def 2;
  consider k4 being Function such that
    A3: (a 'imp' b) '&' (a 'imp' c) '&' (a 'imp' d)=
        k4 & dom k4=Y & rng k4 c= BOOLEAN
                     by FUNCT_2:def 2;
     Y=dom k3 & Y=dom k4 & (for u being set
            st u in Y holds k3.u=k4.u)by A1,A2,A3;
  hence thesis by A2,A3,FUNCT_1:9;
end;

theorem for a,b,c,d being Element of Funcs(Y,BOOLEAN) holds
a 'imp' (b 'or' c 'or' d) = (a 'imp' b) 'or' (a 'imp' c) 'or' (a 'imp' d)
proof
  let a,b,c,d be Element of Funcs(Y,BOOLEAN);
  A1:for x being Element of Y holds
   Pj(a 'imp' (b 'or' c 'or' d),x) =
   Pj((a 'imp' b) 'or' (a 'imp' c) 'or' (a 'imp' d),x)
  proof
    let x be Element of Y;
      Pj((a 'imp' b) 'or' (a 'imp' c) 'or' (a 'imp' d),x)
   =Pj((a 'imp' b) 'or' (a 'imp' c),x) 'or' Pj(a 'imp' d,x)
   by BVFUNC_1:def 7
  .=Pj(a 'imp' b,x) 'or' Pj(a 'imp' c,x) 'or' Pj(a 'imp' d,x)
   by BVFUNC_1:def 7
  .=('not' Pj(a,x) 'or' Pj(b,x)) 'or' Pj(a 'imp' c,x) 'or' Pj(a 'imp' d,x)
   by BVFUNC_1:def 11
  .=('not' Pj(a,x) 'or' Pj(b,x)) 'or' ('not' Pj(a,x) 'or' Pj(c,x)) 'or'
    Pj(a 'imp' d,x)
   by BVFUNC_1:def 11
  .=('not' Pj(a,x) 'or' Pj(b,x)) 'or' ('not' Pj(a,x) 'or' Pj(c,x))
    'or' ('not' Pj(a,x) 'or' Pj(d,x))
   by BVFUNC_1:def 11
  .=(('not' Pj(a,x) 'or' ('not' Pj(a,x) 'or' Pj(b,x))) 'or' Pj(c,x))
    'or' ('not' Pj(a,x) 'or' Pj(d,x)) by BINARITH:20
  .=((('not' Pj(a,x) 'or' 'not' Pj(a,x)) 'or' Pj(b,x)) 'or' Pj(c,x))
    'or' ('not' Pj(a,x) 'or' Pj(d,x))
   by BINARITH:20
  .=(('not' Pj(a,x) 'or' Pj(b,x)) 'or' Pj(c,x))
    'or' ('not' Pj(a,x) 'or' Pj(d,x))
   by BINARITH:21
  .=('not' Pj(a,x) 'or' (Pj(b,x) 'or' Pj(c,x)))
    'or' ('not' Pj(a,x) 'or' Pj(d,x))
   by BINARITH:20
  .=('not' Pj(a,x) 'or' Pj(b 'or' c,x)) 'or' ('not' Pj(a,x) 'or' Pj(d,x))
   by BVFUNC_1:def 7
  .=('not' Pj(a,x) 'or' ('not'
Pj(a,x) 'or' Pj(b 'or' c,x))) 'or' Pj(d,x) by BINARITH:20
  .=(('not' Pj(a,x) 'or' 'not' Pj(a,x)) 'or' Pj(b 'or' c,x)) 'or' Pj(d,x)
   by BINARITH:20
  .=('not' Pj(a,x) 'or' Pj(b 'or' c,x)) 'or' Pj(d,x)
   by BINARITH:21
  .='not' Pj(a,x) 'or' (Pj(b 'or' c,x) 'or' Pj(d,x))
   by BINARITH:20
  .='not' Pj(a,x) 'or' Pj(b 'or' c 'or' d,x)
   by BVFUNC_1:def 7
  .=Pj(a 'imp' (b 'or' c 'or' d),x) by BVFUNC_1:def 11;
    hence thesis;
  end;
  consider k3 being Function such that
    A2: (a 'imp' (b 'or' c 'or' d))=k3 & dom k3=Y & rng k3 c= BOOLEAN
                     by FUNCT_2:def 2;
  consider k4 being Function such that
    A3: (a 'imp' b) 'or' (a 'imp' c) 'or' (a 'imp' d)=
        k4 & dom k4=Y & rng k4 c= BOOLEAN
                     by FUNCT_2:def 2;
     Y=dom k3 & Y=dom k4 & (for u being set
            st u in Y holds k3.u=k4.u)by A1,A2,A3;
  hence thesis by A2,A3,FUNCT_1:9;
end;

theorem for a,b,c,d being Element of Funcs(Y,BOOLEAN) holds
(a '&' b '&' c) 'imp' d = (a 'imp' d) 'or' (b 'imp' d) 'or' (c 'imp' d)
proof
  let a,b,c,d be Element of Funcs(Y,BOOLEAN);
  A1:for x being Element of Y holds
   Pj((a '&' b '&' c) 'imp' d,x) =
   Pj((a 'imp' d) 'or' (b 'imp' d) 'or' (c 'imp' d),x)
  proof
    let x be Element of Y;
      Pj((a 'imp' d) 'or' (b 'imp' d) 'or' (c 'imp' d),x)
   =Pj((a 'imp' d) 'or' (b 'imp' d),x) 'or' Pj(c 'imp' d,x)
   by BVFUNC_1:def 7
  .=Pj(a 'imp' d,x) 'or' Pj(b 'imp' d,x) 'or' Pj(c 'imp' d,x)
   by BVFUNC_1:def 7
  .=('not' Pj(a,x) 'or' Pj(d,x)) 'or' Pj(b 'imp' d,x) 'or' Pj(c 'imp' d,x)
   by BVFUNC_1:def 11
  .=('not' Pj(a,x) 'or' Pj(d,x)) 'or' ('not' Pj(b,x) 'or' Pj(d,x))
    'or' Pj(c 'imp' d,x)
   by BVFUNC_1:def 11
  .=('not' Pj(a,x) 'or' Pj(d,x)) 'or' ('not' Pj(b,x) 'or' Pj(d,x))
    'or' ('not' Pj(c,x) 'or' Pj(d,x))
   by BVFUNC_1:def 11
  .=(('not' Pj(a,x) 'or' (Pj(d,x) 'or' 'not' Pj(b,x))) 'or' Pj(d,x))
    'or' ('not' Pj(c,x) 'or' Pj(d,x))
   by BINARITH:20
  .=(('not' Pj(a,x) 'or' 'not' Pj(b,x)) 'or' Pj(d,x)) 'or' Pj(d,x)
    'or' ('not' Pj(c,x) 'or' Pj(d,x))
   by BINARITH:20
  .=('not' Pj(a,x) 'or' 'not' Pj(b,x)) 'or' (Pj(d,x) 'or' Pj(d,x))
    'or' ('not' Pj(c,x) 'or' Pj(d,x))
   by BINARITH:20
  .=('not' Pj(a,x) 'or' 'not' Pj(b,x)) 'or' Pj(d,x)
    'or' ('not' Pj(c,x) 'or' Pj(d,x))
   by BINARITH:21
  .=('not'( Pj(a,x) '&' Pj(b,x)) 'or' Pj(d,x)) 'or'
  ('not' Pj(c,x) 'or' Pj(d,x))
   by BINARITH:9
  .=('not'( Pj(a,x) '&' Pj(b,x)) 'or' (Pj(d,x) 'or' 'not'
  Pj(c,x))) 'or' Pj(d,x)
   by BINARITH:20
  .=(('not'( Pj(a,x) '&' Pj(b,x)) 'or' 'not' Pj(c,x)) 'or'
  Pj(d,x)) 'or' Pj(d,x) by BINARITH:20
  .=('not'( Pj(a,x) '&' Pj(b,x)) 'or' 'not' Pj(c,x)) 'or'
  (Pj(d,x) 'or' Pj(d,x)) by BINARITH:20
  .=('not'( Pj(a,x) '&' Pj(b,x)) 'or' 'not' Pj(c,x)) 'or' Pj(d,x)
   by BINARITH:21
  .='not'( Pj(a,x) '&' Pj(b,x) '&' Pj(c,x)) 'or' Pj(d,x) by BINARITH:9
  .='not'( Pj(a '&' b,x) '&' Pj(c,x)) 'or' Pj(d,x) by VALUAT_1:def 6
  .='not' Pj(a '&' b '&' c,x) 'or' Pj(d,x) by VALUAT_1:def 6
  .=Pj((a '&' b '&' c) 'imp' d,x) by BVFUNC_1:def 11;
    hence thesis;
  end;
  consider k3 being Function such that
    A2: ((a '&' b '&' c) 'imp' d)=k3 & dom k3=Y & rng k3 c= BOOLEAN
                     by FUNCT_2:def 2;
  consider k4 being Function such that
    A3: (a 'imp' d) 'or' (b 'imp' d) 'or' (c 'imp' d)
        =k4 & dom k4=Y & rng k4 c= BOOLEAN
                     by FUNCT_2:def 2;
     Y=dom k3 & Y=dom k4 & (for u being set
            st u in Y holds k3.u=k4.u)by A1,A2,A3;
  hence thesis by A2,A3,FUNCT_1:9;
end;

theorem for a,b,c,d being Element of Funcs(Y,BOOLEAN) holds
(a 'or' b 'or' c) 'imp' d = (a 'imp' d) '&' (b 'imp' d) '&' (c 'imp' d)
proof
  let a,b,c,d be Element of Funcs(Y,BOOLEAN);
  A1:for x being Element of Y holds
   Pj((a 'or' b 'or' c) 'imp' d,x) =
   Pj((a 'imp' d) '&' (b 'imp' d) '&' (c 'imp' d),x)
  proof
    let x be Element of Y;
      Pj((a 'imp' d) '&' (b 'imp' d) '&' (c 'imp' d),x)
   =Pj((a 'imp' d) '&' (b 'imp' d),x) '&' Pj(c 'imp' d,x)
   by VALUAT_1:def 6
  .=Pj(a 'imp' d,x) '&' Pj(b 'imp' d,x) '&' Pj(c 'imp' d,x)
   by VALUAT_1:def 6
  .=('not' Pj(a,x) 'or' Pj(d,x)) '&' Pj(b 'imp' d,x) '&' Pj(c 'imp' d,x)
   by BVFUNC_1:def 11
  .=('not' Pj(a,x) 'or' Pj(d,x)) '&' ('not'
Pj(b,x) 'or' Pj(d,x)) '&' Pj(c 'imp' d,x)
   by BVFUNC_1:def 11
  .=(Pj(d,x) 'or' 'not' Pj(a,x)) '&' ('not' Pj(b,x) 'or' Pj(d,x))
    '&' ('not' Pj(c,x) 'or' Pj(d,x)) by BVFUNC_1:def 11
  .=(Pj(d,x) 'or' ('not' Pj(a,x) '&' 'not' Pj(b,x)))
    '&' ('not' Pj(c,x) 'or' Pj(d,x))
   by BINARITH:23
  .=('not'( Pj(a,x) 'or' Pj(b,x)) 'or' Pj(d,x))
    '&' ('not' Pj(c,x) 'or' Pj(d,x))
   by BINARITH:10
  .=(Pj(d,x) 'or' 'not' Pj(a 'or' b,x)) '&' ('not' Pj(c,x) 'or' Pj(d,x)) by
BVFUNC_1:def 7
  .=Pj(d,x) 'or' ('not' Pj(a 'or' b,x) '&' 'not' Pj(c,x))
   by BINARITH:23
  .=('not'( Pj(a 'or' b,x) 'or' Pj(c,x))) 'or' Pj(d,x)
   by BINARITH:10
  .='not' Pj(a 'or' b 'or' c,x) 'or' Pj(d,x)
   by BVFUNC_1:def 7
  .=Pj((a 'or' b 'or' c) 'imp' d,x) by BVFUNC_1:def 11;
    hence thesis;
  end;
  consider k3 being Function such that
    A2: ((a 'or' b 'or' c) 'imp' d)=k3 & dom k3=Y & rng k3 c= BOOLEAN
                     by FUNCT_2:def 2;
  consider k4 being Function such that
    A3: (a 'imp' d) '&' (b 'imp' d) '&' (c 'imp' d)
        =k4 & dom k4=Y & rng k4 c= BOOLEAN
                     by FUNCT_2:def 2;
     Y=dom k3 & Y=dom k4 & (for u being set
            st u in Y holds k3.u=k4.u)by A1,A2,A3;
  hence thesis by A2,A3,FUNCT_1:9;
end;

theorem for a,b,c being Element of Funcs(Y,BOOLEAN) holds
(a 'imp' b) '&' (b 'imp' c) '&' (c 'imp' a) =
(a 'imp' b) '&' (b 'imp' c) '&' (c 'imp' a) '&'
(b 'imp' a) '&' (a 'imp' c)
proof
  let a,b,c be Element of Funcs(Y,BOOLEAN);
  A1:for x being Element of Y holds
   Pj((a 'imp' b) '&' (b 'imp' c) '&' (c 'imp' a),x) =
   Pj((a 'imp' b) '&' (b 'imp' c) '&' (c 'imp' a) '&'
      (b 'imp' a) '&' (a 'imp' c),x)
  proof
    let x be Element of Y;
      (a 'imp' b) '&' (b 'imp' c) '&' (c 'imp' a)
   =('not' a 'or' b) '&' (b 'imp' c) '&' (c 'imp' a) by BVFUNC_4:8
  .=('not' a 'or' b) '&' ('not' b 'or' c) '&' (c 'imp' a) by BVFUNC_4:8
  .=('not' a 'or' b) '&' ('not' b 'or' c) '&' ('not' c 'or' a) by BVFUNC_4:8
  .=(('not' a '&' ('not' b 'or' c) 'or' b '&' ('not' b 'or' c))) '&' ('not'
c 'or' a)
   by BVFUNC_1:15
  .=(('not' a '&' ('not' b 'or' c) 'or'
  (b '&' 'not' b 'or' b '&' c))) '&' ('not' c 'or' a)
   by BVFUNC_1:15
  .=(('not' a '&' ('not' b 'or' c) 'or' (O_el(Y) 'or' b '&' c))) '&' ('not'
c 'or' a)
   by BVFUNC_4:5
  .=(('not' a '&' ('not' b 'or' c) 'or' (b '&' c))) '&' ('not' c 'or' a)
   by BVFUNC_1:12
  .=(('not' a 'or' (b '&' c)) '&' (('not' b 'or' c)
  'or' (b '&' c))) '&' ('not' c 'or' a)
   by BVFUNC_1:14
  .=((('not' a 'or' b) '&' ('not' a 'or' c)) '&' (('not'
b 'or' c) 'or' (b '&' c)))
    '&' ('not' c 'or' a)
   by BVFUNC_1:14
  .=((('not' a 'or' b) '&' ('not' a 'or' c)) '&'
    ((('not' b 'or' c) 'or' b) '&' (('not' b 'or' c) 'or' c)))
    '&' ('not' c 'or' a)
   by BVFUNC_1:14
  .=((('not' a 'or' b) '&' ('not' a 'or' c)) '&'
    ((c 'or' ('not' b 'or' b)) '&' (('not' b 'or' c) 'or' c)))
    '&' ('not' c 'or' a)
   by BVFUNC_1:11
  .=((('not' a 'or' b) '&' ('not' a 'or' c)) '&'
    ((c 'or' I_el(Y)) '&' (('not' b 'or' c) 'or' c)))
    '&' ('not' c 'or' a)
   by BVFUNC_4:6
  .=((('not' a 'or' b) '&' ('not' a 'or' c)) '&'
    (I_el(Y) '&' (('not' b 'or' c) 'or' c)))
    '&' ('not' c 'or' a)
   by BVFUNC_1:13
  .=((('not' a 'or' b) '&' ('not' a 'or' c)) '&'
    (('not' b 'or' c) 'or' c))
    '&' ('not' c 'or' a)
   by BVFUNC_1:9
  .=((('not' a 'or' b) '&' ('not' a 'or' c)) '&'
    ('not' b 'or' (c 'or' c)))
    '&' ('not' c 'or' a)
   by BVFUNC_1:11
  .=((('not' a 'or' b) '&' ('not' a 'or' c)) '&' ('not' b 'or' c))
    '&' ('not' c 'or' a)
   by BVFUNC_1:10
  .=(('not' a 'or' b) '&' ('not' a 'or' c)) '&' (('not' b 'or' c)
    '&' ('not' c 'or' a))
   by BVFUNC_1:7
  .=(('not' a 'or' b) '&' ('not' a 'or' c)) '&'
    (('not' b '&' ('not' c 'or' a)) 'or' (c '&' ('not' c 'or' a)))
   by BVFUNC_1:15
  .=(('not' a 'or' b) '&' ('not' a 'or' c)) '&'
    (('not' b '&' ('not' c 'or' a)) 'or' ((c '&' 'not' c 'or' c '&' a)))
   by BVFUNC_1:15
  .=(('not' a 'or' b) '&' ('not' a 'or' c)) '&'
    (('not' b '&' ('not' c 'or' a)) 'or' ((O_el(Y) 'or' c '&' a)))
   by BVFUNC_4:5
  .=(('not' a 'or' b) '&' ('not' a 'or' c)) '&'
    (('not' b '&' ('not' c 'or' a)) 'or' (c '&' a))
   by BVFUNC_1:12
  .=(('not' a 'or' b) '&' ('not' a 'or' c)) '&'
    (('not' b 'or' (c '&' a)) '&' (('not' c 'or' a) 'or' (c '&' a)))
   by BVFUNC_1:14
  .=(('not' a 'or' b) '&' ('not' a 'or' c)) '&'
    ((('not' b 'or' c) '&' ('not' b 'or' a)) '&' (('not'
c 'or' a) 'or' (c '&' a)))
   by BVFUNC_1:14
  .= (('not' a 'or' c) '&' ('not' a 'or' b)) '&'
    ((('not' b 'or' a) '&' ('not' b 'or' c)) '&'
     ((('not' c 'or' a) 'or' c) '&' (('not' c 'or' a) 'or' a)))
   by BVFUNC_1:14
  .= (('not' a 'or' c) '&' ('not' a 'or' b)) '&'
    ((('not' b 'or' a) '&' ('not' b 'or' c)) '&'
     ((a 'or' ('not' c 'or' c)) '&' (('not' c 'or' a) 'or' a)))
   by BVFUNC_1:11
  .= (('not' a 'or' c) '&' ('not' a 'or' b)) '&'
    ((('not' b 'or' a) '&' ('not' b 'or' c)) '&'
     ((a 'or' I_el(Y)) '&' (('not' c 'or' a) 'or' a)))
   by BVFUNC_4:6
  .= (('not' a 'or' c) '&' ('not' a 'or' b)) '&'
    ((('not' b 'or' a) '&' ('not' b 'or' c)) '&'
     (I_el(Y) '&' (('not' c 'or' a) 'or' a)))
   by BVFUNC_1:13
  .= (('not' a 'or' c) '&' ('not' a 'or' b)) '&'
    ((('not' b 'or' a) '&' ('not' b 'or' c)) '&'
     (('not' c 'or' a) 'or' a))
   by BVFUNC_1:9
  .= (('not' a 'or' c) '&' ('not' a 'or' b)) '&'
    ((('not' b 'or' a) '&' ('not' b 'or' c)) '&'
     ('not' c 'or' (a 'or' a)))
   by BVFUNC_1:11
  .= (('not' a 'or' c) '&' ('not' a 'or' b)) '&'
     ((('not' b 'or' a) '&' ('not' b 'or' c)) '&' ('not' c 'or' a))
   by BVFUNC_1:10
  .= ((('not' a 'or' c) '&' ('not' a 'or' b)) '&' (('not' b 'or' a) '&' ('not'
b 'or' c)))
     '&' ('not' c 'or' a)
   by BVFUNC_1:7
  .= (((('not' a 'or' b) '&' ('not' a 'or' c)) '&' ('not' b 'or' a)) '&' ('not'
b 'or' c))
     '&' ('not' c 'or' a)
   by BVFUNC_1:7
  .= (((('not' b 'or' a) '&' ('not' a 'or' c)) '&' ('not' a 'or' b)) '&' ('not'
b 'or' c))
     '&' ('not' c 'or' a)
   by BVFUNC_1:7
  .= ((('not' b 'or' a) '&' ('not' a 'or' c)) '&' (('not' a 'or' b) '&' ('not'
b 'or' c)))
     '&' ('not' c 'or' a)
   by BVFUNC_1:7
  .= (('not' b 'or' a) '&' ('not' a 'or' c)) '&'
     ((('not' a 'or' b) '&' ('not' b 'or' c)) '&' ('not' c 'or' a))
   by BVFUNC_1:7
  .= ('not' b 'or' a) '&'
     (('not' a 'or' b) '&' ('not' b 'or' c) '&' ('not' c 'or' a)) '&'
     ('not' a 'or' c)
   by BVFUNC_1:7
  .= (a 'imp' b) '&' ('not' b 'or' c) '&' ('not' c 'or' a) '&'
     ('not' b 'or' a) '&' ('not' a 'or' c)
   by BVFUNC_4:8
  .= (a 'imp' b) '&' (b 'imp' c) '&' ('not' c 'or' a) '&'
     ('not' b 'or' a) '&' ('not' a 'or' c)
   by BVFUNC_4:8
  .= (a 'imp' b) '&' (b 'imp' c) '&' (c 'imp' a) '&'
     ('not' b 'or' a) '&' ('not' a 'or' c)
   by BVFUNC_4:8
  .= (a 'imp' b) '&' (b 'imp' c) '&' (c 'imp' a) '&'
     (b 'imp' a) '&' ('not' a 'or' c)
   by BVFUNC_4:8
  .=(a 'imp' b) '&' (b 'imp' c) '&' (c 'imp' a) '&'
    (b 'imp' a) '&' (a 'imp' c) by BVFUNC_4:8;
    hence thesis;
  end;
  consider k3 being Function such that
    A2: ((a 'imp' b) '&' (b 'imp' c) '&' (c 'imp' a))=
    k3 & dom k3=Y & rng k3 c= BOOLEAN
                     by FUNCT_2:def 2;
  consider k4 being Function such that
    A3: (a 'imp' b) '&' (b 'imp' c) '&' (c 'imp' a) '&' (b 'imp' a) '&'
        (a 'imp' c)=k4 & dom k4=Y & rng k4 c= BOOLEAN
                     by FUNCT_2:def 2;
     Y=dom k3 & Y=dom k4 & (for u being set
            st u in Y holds k3.u=k4.u)by A1,A2,A3;
  hence ((a 'imp' b) '&' (b 'imp' c) '&' (c 'imp' a))=
  (a 'imp' b) '&' (b 'imp' c) '&' (c 'imp' a) '&'
  (b 'imp' a) '&' (a 'imp' c) by A2,A3,FUNCT_1:9;
end;

theorem for a,b being Element of Funcs(Y,BOOLEAN) holds
a = (a '&' b) 'or' (a '&' 'not' b)
proof
  let a,b be Element of Funcs(Y,BOOLEAN);
  A1:for x being Element of Y holds
   Pj(a,x) = Pj((a '&' b) 'or' (a '&' 'not' b),x)
  proof
    let x be Element of Y;
      Pj((a '&' b) 'or' (a '&' 'not' b),x)
   =Pj(a '&' (b 'or' 'not' b),x) by BVFUNC_1:15
  .=Pj(a '&' I_el(Y),x) by BVFUNC_4:6
  .=Pj(a,x) by BVFUNC_1:9;
    hence thesis;
  end;
  consider k3 being Function such that
    A2: (a)=k3 & dom k3=Y & rng k3 c= BOOLEAN
                     by FUNCT_2:def 2;
  consider k4 being Function such that
    A3: (a '&' b) 'or' (a '&' 'not' b)
        =k4 & dom k4=Y & rng k4 c= BOOLEAN
                     by FUNCT_2:def 2;
     Y=dom k3 & Y=dom k4 & (for u being set
            st u in Y holds k3.u=k4.u)by A1,A2,A3;
  hence thesis by A2,A3,FUNCT_1:9;
end;

theorem for a,b being Element of Funcs(Y,BOOLEAN) holds
a = (a 'or' b) '&' (a 'or' 'not' b)
proof
  let a,b be Element of Funcs(Y,BOOLEAN);
  A1:for x being Element of Y holds
   Pj(a,x) = Pj((a 'or' b) '&' (a 'or' 'not' b),x)
  proof
    let x be Element of Y;
      Pj((a 'or' b) '&' (a 'or' 'not' b),x)
   =Pj(a 'or' (b '&' 'not' b),x) by BVFUNC_1:14
  .=Pj(a 'or' O_el(Y),x) by BVFUNC_4:5
  .=Pj(a,x) by BVFUNC_1:12;
    hence thesis;
  end;
  consider k3 being Function such that
    A2: (a)=k3 & dom k3=Y & rng k3 c= BOOLEAN
                     by FUNCT_2:def 2;
  consider k4 being Function such that
    A3: (a 'or' b) '&' (a 'or' 'not' b)
        =k4 & dom k4=Y & rng k4 c= BOOLEAN
                     by FUNCT_2:def 2;
     Y=dom k3 & Y=dom k4 & (for u being set
            st u in Y holds k3.u=k4.u)by A1,A2,A3;
  hence thesis by A2,A3,FUNCT_1:9;
end;

theorem for a,b,c being Element of Funcs(Y,BOOLEAN) holds
a = (a '&' b '&' c) 'or' (a '&' b '&' 'not' c) 'or'
    (a '&' 'not' b '&' c) 'or' (a '&' 'not' b '&' 'not' c)
proof
  let a,b,c be Element of Funcs(Y,BOOLEAN);
  A1:for x being Element of Y holds
   Pj(a,x) = Pj((a '&' b '&' c) 'or' (a '&' b '&' 'not' c) 'or'
                (a '&' 'not' b '&' c) 'or' (a '&' 'not' b '&' 'not' c),x)
  proof
    let x be Element of Y;
      Pj((a '&' b '&' c) 'or' (a '&' b '&' 'not' c) 'or'
       (a '&' 'not' b '&' c) 'or' (a '&' 'not' b '&' 'not' c),x)
   =Pj(((a '&' b) '&' (c 'or' 'not' c)) 'or'
       (a '&' 'not' b '&' c) 'or' (a '&' 'not' b '&' 'not' c),x)
   by BVFUNC_1:15
  .=Pj(((a '&' b) '&' I_el(Y)) 'or'
       (a '&' 'not' b '&' c) 'or' (a '&' 'not' b '&' 'not' c),x)
   by BVFUNC_4:6
  .=Pj((a '&' b) 'or'
       (a '&' 'not' b '&' c) 'or' (a '&' 'not' b '&' 'not' c),x)
   by BVFUNC_1:9
  .=Pj((a '&' b) 'or'
       ((a '&' 'not' b '&' c) 'or' (a '&' 'not' b '&' 'not' c)),x)
   by BVFUNC_1:11
  .=Pj((a '&' b) 'or' ((a '&' 'not' b) '&' (c 'or' 'not' c)),x)
   by BVFUNC_1:15
  .=Pj((a '&' b) 'or' ((a '&' 'not' b) '&' I_el(Y)),x)
   by BVFUNC_4:6
  .=Pj((a '&' b) 'or' (a '&' 'not' b),x)
   by BVFUNC_1:9
  .=Pj(a '&' (b 'or' 'not' b),x) by BVFUNC_1:15
  .=Pj(a '&' I_el(Y),x) by BVFUNC_4:6
  .=Pj(a,x) by BVFUNC_1:9;
    hence thesis;
  end;
  consider k3 being Function such that
    A2: (a)=k3 & dom k3=Y & rng k3 c= BOOLEAN
                     by FUNCT_2:def 2;
  consider k4 being Function such that
    A3: (a '&' b '&' c) 'or' (a '&' b '&' 'not' c) 'or' (a '&' 'not' b '&' c)
        'or' (a '&' 'not' b '&' 'not' c)=
        k4 & dom k4=Y & rng k4 c= BOOLEAN
                     by FUNCT_2:def 2;
     Y=dom k3 & Y=dom k4 & (for u being set
            st u in Y holds k3.u=k4.u)by A1,A2,A3;
  hence (a)=(a '&' b '&' c) 'or' (a '&' b '&' 'not' c)
        'or' (a '&' 'not' b '&' c) 'or' (a '&' 'not' b '&' 'not' c) by A2,A3,
FUNCT_1:9;
end;

theorem for a,b,c being Element of Funcs(Y,BOOLEAN) holds
a = (a 'or' b 'or' c) '&' (a 'or' b 'or' 'not' c) '&'
    (a 'or' 'not' b 'or' c) '&' (a 'or' 'not' b 'or' 'not' c)
proof
  let a,b,c be Element of Funcs(Y,BOOLEAN);
  A1:for x being Element of Y holds
   Pj(a,x) = Pj((a 'or' b 'or' c) '&' (a 'or' b 'or' 'not' c) '&'
                (a 'or' 'not' b 'or' c) '&' (a 'or' 'not' b 'or' 'not' c),x)
  proof
    let x be Element of Y;
      Pj((a 'or' b 'or' c) '&' (a 'or' b 'or' 'not' c) '&'
      (a 'or' 'not' b 'or' c) '&' (a 'or' 'not' b 'or' 'not' c),x)
   =Pj(((a 'or' b) 'or' (c '&' 'not' c)) '&'
      (a 'or' 'not' b 'or' c) '&' (a 'or' 'not' b 'or' 'not' c),x)
   by BVFUNC_1:14
  .=Pj(((a 'or' b) 'or' O_el(Y)) '&'
      (a 'or' 'not' b 'or' c) '&' (a 'or' 'not' b 'or' 'not' c),x)
   by BVFUNC_4:5
  .=Pj((a 'or' b) '&'
      (a 'or' 'not' b 'or' c) '&' (a 'or' 'not' b 'or' 'not' c),x)
   by BVFUNC_1:12
  .=Pj((a 'or' b) '&'
       ((a 'or' 'not' b 'or' c) '&' (a 'or' 'not' b 'or' 'not' c)),x)
   by BVFUNC_1:7
  .=Pj((a 'or' b) '&' ((a 'or' 'not' b) 'or' (c '&' 'not' c)),x)
   by BVFUNC_1:14
  .=Pj((a 'or' b) '&' ((a 'or' 'not' b) 'or' O_el(Y)),x)
   by BVFUNC_4:5
  .=Pj((a 'or' b) '&' (a 'or' 'not' b),x)
   by BVFUNC_1:12
  .=Pj(a 'or' (b '&' 'not' b),x)
   by BVFUNC_1:14
  .=Pj(a 'or' O_el(Y),x) by BVFUNC_4:5
  .=Pj(a,x) by BVFUNC_1:12;
    hence thesis;
  end;
  consider k3 being Function such that
    A2: (a)=k3 & dom k3=Y & rng k3 c= BOOLEAN
                     by FUNCT_2:def 2;
  consider k4 being Function such that
A3: (a 'or' b 'or' c) '&' (a 'or' b 'or' 'not' c) '&' (a 'or' 'not' b 'or' c)
 '&' (a 'or' 'not' b 'or' 'not' c)=k4 & dom k4=Y & rng k4 c= BOOLEAN
                     by FUNCT_2:def 2;
     Y=dom k3 & Y=dom k4 & (for u being set
            st u in Y holds k3.u=k4.u)by A1,A2,A3;
  hence (a)=(a 'or' b 'or' c) '&' (a 'or' b 'or' 'not' c)
   '&' (a 'or' 'not' b 'or' c) '&' (a 'or' 'not' b 'or' 'not' c) by A2,A3,
FUNCT_1:9;
end;

theorem for a,b being Element of Funcs(Y,BOOLEAN) holds
a '&' b = a '&' ('not' a 'or' b)
proof
  let a,b be Element of Funcs(Y,BOOLEAN);
  A1:for x being Element of Y holds
   Pj(a '&' b,x) =
   Pj(a '&' ('not' a 'or' b),x)
  proof
    let x be Element of Y;
      Pj(a '&' ('not' a 'or' b),x)
   =Pj(a,x) '&' Pj('not' a 'or' b,x)
   by VALUAT_1:def 6
  .=Pj(a,x) '&' (Pj('not' a,x) 'or' Pj(b,x))
   by BVFUNC_1:def 7
  .=Pj(a,x) '&' Pj('not' a,x) 'or' Pj(a,x) '&' Pj(b,x)
   by BINARITH:22
  .=Pj(a,x) '&' 'not' Pj(a,x) 'or' Pj(a,x) '&' Pj(b,x)
   by VALUAT_1:def 5
  .=FALSE 'or' Pj(a,x) '&' Pj(b,x)
   by MARGREL1:46
  .=Pj(a,x) '&' Pj(b,x)
   by BINARITH:7
  .=Pj(a '&' b,x) by VALUAT_1:def 6;
    hence thesis;
  end;
  consider k3 being Function such that
    A2: (a '&' b)=k3 & dom k3=Y & rng k3 c= BOOLEAN
                     by FUNCT_2:def 2;
  consider k4 being Function such that
    A3: a '&' ('not' a 'or' b)
        =k4 & dom k4=Y & rng k4 c= BOOLEAN
                     by FUNCT_2:def 2;
     Y=dom k3 & Y=dom k4 & (for u being set
            st u in Y holds k3.u=k4.u)by A1,A2,A3;
  hence thesis by A2,A3,FUNCT_1:9;
end;

theorem for a,b being Element of Funcs(Y,BOOLEAN) holds
a 'or' b = a 'or' ('not' a '&' b)
proof
  let a,b be Element of Funcs(Y,BOOLEAN);
  A1:for x being Element of Y holds
   Pj(a 'or' b,x) =
   Pj(a 'or' ('not' a '&' b),x)
  proof
    let x be Element of Y;
      Pj(a 'or' ('not' a '&' b),x)
   =Pj(a,x) 'or' Pj('not' a '&' b,x)
   by BVFUNC_1:def 7
  .=Pj(a,x) 'or' (Pj('not' a,x) '&' Pj(b,x))
   by VALUAT_1:def 6
  .=(Pj(a,x) 'or' Pj('not' a,x)) '&' (Pj(a,x) 'or' Pj(b,x))
   by BINARITH:23
  .=(Pj(a,x) 'or' 'not' Pj(a,x)) '&' (Pj(a,x) 'or' Pj(b,x))
   by VALUAT_1:def 5
  .=TRUE '&' (Pj(a,x) 'or' Pj(b,x))
   by BINARITH:18
  .=Pj(a,x) 'or' Pj(b,x)
   by MARGREL1:50
  .=Pj(a 'or' b,x) by BVFUNC_1:def 7;
    hence thesis;
  end;
  consider k3 being Function such that
    A2: (a 'or' b)=k3 & dom k3=Y & rng k3 c= BOOLEAN
                     by FUNCT_2:def 2;
  consider k4 being Function such that
    A3: a 'or' ('not' a '&' b)
        =k4 & dom k4=Y & rng k4 c= BOOLEAN
                     by FUNCT_2:def 2;
     Y=dom k3 & Y=dom k4 & (for u being set
            st u in Y holds k3.u=k4.u)by A1,A2,A3;
  hence thesis by A2,A3,FUNCT_1:9;
end;

theorem for a,b being Element of Funcs(Y,BOOLEAN) holds
a 'xor' b = 'not'( a 'eqv' b)
proof
  let a,b be Element of Funcs(Y,BOOLEAN);
  A1:for x being Element of Y holds
   Pj(a 'xor' b,x) = Pj('not'( a 'eqv' b),x)
  proof
    let x be Element of Y;
      Pj(a 'xor' b,x)
   =Pj(('not' a '&' b) 'or' (a '&' 'not' b),x)
   by BVFUNC_4:9
  .=Pj('not' 'not'( ('not' a '&' b) 'or' (a '&' 'not' b)),x)
   by BVFUNC_1:4
  .=Pj('not'('not'('not' a '&' b) '&' 'not'( a '&' 'not' b)),x)
   by BVFUNC_1:16
  .=Pj('not'( ('not' 'not' a 'or' 'not' b) '&' 'not'( a '&' 'not' b)),x)
   by BVFUNC_1:17
  .=Pj('not'( ('not' 'not' a 'or' 'not' b) '&' ('not' a 'or' 'not' 'not' b)),x)
   by BVFUNC_1:17
  .=Pj('not'( (a 'or' 'not' b) '&' ('not' a 'or' 'not' 'not' b)),x)
   by BVFUNC_1:4
  .=Pj('not'( (a 'or' 'not' b) '&' ('not' a 'or' b)),x)
   by BVFUNC_1:4
  .=Pj('not'( (b 'imp' a) '&' ('not' a 'or' b)),x)
   by BVFUNC_4:8
  .=Pj('not'( (b 'imp' a) '&' (a 'imp' b)),x)
   by BVFUNC_4:8
  .=Pj('not'( a 'eqv' b),x) by BVFUNC_4:7;
    hence thesis;
  end;
  consider k3 being Function such that
    A2: (a 'xor' b)=k3 & dom k3=Y & rng k3 c= BOOLEAN
                     by FUNCT_2:def 2;
  consider k4 being Function such that
    A3: 'not'( a 'eqv' b)
        =k4 & dom k4=Y & rng k4 c= BOOLEAN
                     by FUNCT_2:def 2;
     Y=dom k3 & Y=dom k4 & (for u being set
            st u in Y holds k3.u=k4.u)by A1,A2,A3;
  hence thesis by A2,A3,FUNCT_1:9;
end;

theorem for a,b being Element of Funcs(Y,BOOLEAN) holds
a 'xor' b = (a 'or' b) '&' ('not' a 'or' 'not' b)
proof
  let a,b be Element of Funcs(Y,BOOLEAN);
  A1:for x being Element of Y holds
   Pj(a 'xor' b,x) = Pj((a 'or' b) '&' ('not' a 'or' 'not' b),x)
  proof
    let x be Element of Y;
      Pj((a 'or' b) '&' ('not' a 'or' 'not' b),x)
   =Pj(a 'or' b,x) '&' Pj('not' a 'or' 'not' b,x) by VALUAT_1:def 6
  .=(Pj(a,x) 'or' Pj(b,x)) '&' Pj('not' a 'or' 'not' b,x) by BVFUNC_1:def 7
  .=(Pj(a,x) 'or' Pj(b,x)) '&' (Pj('not' a,x) 'or' Pj('not'
b,x)) by BVFUNC_1:def 7
  .=(Pj('not' a,x) '&' (Pj(a,x) 'or' Pj(b,x))) 'or'
    ((Pj(a,x) 'or' Pj(b,x)) '&' Pj('not' b,x)) by BINARITH:22
  .=(Pj('not' a,x) '&' Pj(a,x) 'or' Pj('not' a,x) '&' Pj(b,x)) 'or'
    (Pj('not' b,x) '&' (Pj(a,x) 'or' Pj(b,x)))
   by BINARITH:22
  .=(Pj('not' a,x) '&' Pj(a,x) 'or' Pj('not' a,x) '&' Pj(b,x)) 'or'
    (Pj('not' b,x) '&' Pj(a,x) 'or' Pj('not' b,x) '&' Pj(b,x))
   by BINARITH:22
  .=('not' Pj(a,x) '&' Pj(a,x) 'or' Pj('not' a,x) '&' Pj(b,x)) 'or'
    (Pj('not' b,x) '&' Pj(a,x) 'or' Pj('not' b,x) '&' Pj(b,x))
   by VALUAT_1:def 5
  .=('not' Pj(a,x) '&' Pj(a,x) 'or' Pj('not' a,x) '&' Pj(b,x)) 'or'
    (Pj('not' b,x) '&' Pj(a,x) 'or' 'not' Pj(b,x) '&' Pj(b,x))
   by VALUAT_1:def 5
  .=(FALSE 'or' Pj('not' a,x) '&' Pj(b,x)) 'or'
    (Pj('not' b,x) '&' Pj(a,x) 'or' 'not' Pj(b,x) '&' Pj(b,x))
   by MARGREL1:46
  .=(FALSE 'or' Pj('not' a,x) '&' Pj(b,x)) 'or'
    (Pj('not' b,x) '&' Pj(a,x) 'or' FALSE)
   by MARGREL1:46
  .=(Pj('not' a,x) '&' Pj(b,x)) 'or'
    (Pj('not' b,x) '&' Pj(a,x) 'or' FALSE)
   by BINARITH:7
  .=(Pj('not' a,x) '&' Pj(b,x)) 'or' (Pj(a,x) '&' Pj('not' b,x)) by BINARITH:7
  .=Pj('not' a '&' b,x) 'or' (Pj(a,x) '&' Pj('not' b,x))
   by VALUAT_1:def 6
  .=Pj('not' a '&' b,x) 'or' Pj(a '&' 'not' b,x)
   by VALUAT_1:def 6
  .=Pj('not' a '&' b 'or' a '&' 'not' b,x)
   by BVFUNC_1:def 7
  .=Pj(a 'xor' b,x) by BVFUNC_4:9;
    hence thesis;
  end;
  consider k3 being Function such that
    A2: (a 'xor' b)=k3 & dom k3=Y & rng k3 c= BOOLEAN
                     by FUNCT_2:def 2;
  consider k4 being Function such that
    A3: (a 'or' b) '&' ('not' a 'or' 'not' b)
        =k4 & dom k4=Y & rng k4 c= BOOLEAN
                     by FUNCT_2:def 2;
     Y=dom k3 & Y=dom k4 & (for u being set
            st u in Y holds k3.u=k4.u)by A1,A2,A3;
  hence thesis by A2,A3,FUNCT_1:9;
end;

theorem for a being Element of Funcs(Y,BOOLEAN) holds
a 'xor' I_el(Y) = 'not' a
proof
  let a be Element of Funcs(Y,BOOLEAN);
  A1:for x being Element of Y holds
   Pj(a 'xor' I_el(Y),x) = Pj('not' a,x)
  proof
    let x be Element of Y;
      Pj(a 'xor' I_el(Y),x)
   =Pj(('not' a '&' I_el(Y)) 'or' (a '&' 'not' I_el(Y)),x) by BVFUNC_4:9
  .=Pj(('not' a '&' I_el(Y)) 'or' (a '&' O_el(Y)),x) by BVFUNC_1:5
  .=Pj(('not' a '&' I_el(Y)) 'or' O_el(Y),x) by BVFUNC_1:8
  .=Pj('not' a '&' I_el(Y),x) by BVFUNC_1:12
  .=Pj('not' a,x) by BVFUNC_1:9;
    hence thesis;
  end;
  consider k3 being Function such that
    A2: (a 'xor' I_el(Y))=k3 & dom k3=Y & rng k3 c= BOOLEAN
                     by FUNCT_2:def 2;
  consider k4 being Function such that
    A3: 'not' a
        =k4 & dom k4=Y & rng k4 c= BOOLEAN
                     by FUNCT_2:def 2;
     Y=dom k3 & Y=dom k4 & (for u being set
            st u in Y holds k3.u=k4.u)by A1,A2,A3;
  hence thesis by A2,A3,FUNCT_1:9;
end;

theorem for a being Element of Funcs(Y,BOOLEAN) holds
a 'xor' O_el(Y) = a
proof
  let a be Element of Funcs(Y,BOOLEAN);
  A1:for x being Element of Y holds
   Pj(a 'xor' O_el(Y),x) = Pj(a,x)
  proof
    let x be Element of Y;
      Pj(a 'xor' O_el(Y),x)
   =Pj(('not' a '&' O_el(Y)) 'or' (a '&' 'not' O_el(Y)),x) by BVFUNC_4:9
  .=Pj(('not' a '&' O_el(Y)) 'or' (a '&' I_el(Y)),x) by BVFUNC_1:5
  .=Pj(('not' a '&' O_el(Y)) 'or' a,x) by BVFUNC_1:9
  .=Pj(O_el(Y) 'or' a,x) by BVFUNC_1:8
  .=Pj(a,x) by BVFUNC_1:12;
    hence thesis;
  end;
  consider k3 being Function such that
    A2: (a 'xor' O_el(Y))=k3 & dom k3=Y & rng k3 c= BOOLEAN
                     by FUNCT_2:def 2;
  consider k4 being Function such that
    A3: a
        =k4 & dom k4=Y & rng k4 c= BOOLEAN
                     by FUNCT_2:def 2;
     Y=dom k3 & Y=dom k4 & (for u being set
            st u in Y holds k3.u=k4.u)by A1,A2,A3;
  hence thesis by A2,A3,FUNCT_1:9;
end;

theorem for a,b being Element of Funcs(Y,BOOLEAN) holds
a 'xor' b = 'not' a 'xor' 'not' b
proof
  let a,b be Element of Funcs(Y,BOOLEAN);
  A1:for x being Element of Y holds
   Pj(a 'xor' b,x) = Pj('not' a 'xor' 'not' b,x)
  proof
    let x be Element of Y;
      Pj('not' a 'xor' 'not' b,x)
   =Pj(('not' 'not' a '&' 'not' b) 'or' ('not' a '&' 'not' 'not' b),x)
   by BVFUNC_4:9
  .=Pj((a '&' 'not' b) 'or' ('not' a '&' 'not' 'not' b),x) by BVFUNC_1:4
  .=Pj((a '&' 'not' b) 'or' ('not' a '&' b),x) by BVFUNC_1:4
  .=Pj(a 'xor' b,x) by BVFUNC_4:9;
    hence thesis;
  end;
  consider k3 being Function such that
    A2: (a 'xor' b)=k3 & dom k3=Y & rng k3 c= BOOLEAN
                     by FUNCT_2:def 2;
  consider k4 being Function such that
    A3: 'not' a 'xor' 'not' b
        =k4 & dom k4=Y & rng k4 c= BOOLEAN
                     by FUNCT_2:def 2;
     Y=dom k3 & Y=dom k4 & (for u being set
            st u in Y holds k3.u=k4.u)by A1,A2,A3;
  hence thesis by A2,A3,FUNCT_1:9;
end;

theorem for a,b being Element of Funcs(Y,BOOLEAN) holds
'not'( a 'xor' b) = a 'xor' 'not' b
proof
  let a,b be Element of Funcs(Y,BOOLEAN);
  A1:for x being Element of Y holds
   Pj('not'( a 'xor' b),x) = Pj(a 'xor' 'not' b,x)
  proof
    let x be Element of Y;
      Pj('not'( a 'xor' b),x)
   =Pj('not'( ('not' a '&' b) 'or' (a '&' 'not' b)),x) by BVFUNC_4:9
  .=Pj(('not'('not' a '&' b) '&' 'not'( a '&' 'not' b)),x) by BVFUNC_1:16
  .=Pj((('not' 'not' a 'or' 'not' b) '&' 'not'( a '&' 'not' b)),x)
  by BVFUNC_1:17
  .=Pj((('not' 'not' a 'or' 'not' b) '&' ('not' a 'or' 'not' 'not'
b)),x) by BVFUNC_1:17
  .=Pj(((a 'or' 'not' b) '&' ('not' a 'or' 'not' 'not' b)),x) by BVFUNC_1:4
  .=Pj(((a 'or' 'not' b) '&' ('not' a 'or' b)),x) by BVFUNC_1:4
  .=Pj(((a 'or' 'not' b) '&' 'not' a 'or' (a 'or' 'not'
b) '&' b),x) by BVFUNC_1:15
  .=Pj(((a '&' 'not' a 'or' 'not' b '&' 'not' a) 'or' (a 'or' 'not'
b) '&' b),x) by BVFUNC_1:15
  .=Pj(((O_el(Y) 'or' 'not' b '&' 'not' a) 'or' (a 'or' 'not'
b) '&' b),x) by BVFUNC_4:5
  .=Pj((('not' b '&' 'not' a) 'or' (a 'or' 'not' b) '&' b),x) by BVFUNC_1:12
  .=Pj((('not' b '&' 'not' a) 'or' (a '&' b 'or' 'not' b '&' b)),x)
  by BVFUNC_1:15
  .=Pj((('not' b '&' 'not' a) 'or' (a '&' b 'or' O_el(Y))),x) by BVFUNC_4:5
  .=Pj(('not' b '&' 'not' a) 'or' (a '&' b),x) by BVFUNC_1:12
  .=Pj(('not' a '&' 'not' b) 'or' (a '&' 'not' 'not' b),x) by BVFUNC_1:4
  .=Pj(a 'xor' 'not' b,x) by BVFUNC_4:9;
    hence thesis;
  end;
  consider k3 being Function such that
    A2: ('not'( a 'xor' b))=k3 & dom k3=Y & rng k3 c= BOOLEAN
                     by FUNCT_2:def 2;
  consider k4 being Function such that
    A3: a 'xor' 'not' b
        =k4 & dom k4=Y & rng k4 c= BOOLEAN
                     by FUNCT_2:def 2;
     Y=dom k3 & Y=dom k4 & (for u being set
            st u in Y holds k3.u=k4.u)by A1,A2,A3;
  hence thesis by A2,A3,FUNCT_1:9;
end;

theorem Th18: for a,b being Element of Funcs(Y,BOOLEAN) holds
a 'eqv' b = (a 'or' 'not' b) '&' ('not' a 'or' b)
proof
  let a,b be Element of Funcs(Y,BOOLEAN);
  A1:for x being Element of Y holds
   Pj(a 'eqv' b,x) = Pj((a 'or' 'not' b) '&' ('not' a 'or' b),x)
  proof
    let x be Element of Y;
      Pj((a 'or' 'not' b) '&' ('not' a 'or' b),x)
   =Pj((a 'or' 'not' b) '&' (a 'imp' b),x) by BVFUNC_4:8
  .=Pj((a 'imp' b) '&' (b 'imp' a),x) by BVFUNC_4:8
  .=Pj(a 'eqv' b,x) by BVFUNC_4:7;
    hence thesis;
  end;
  consider k3 being Function such that
    A2: (a 'eqv' b)=k3 & dom k3=Y & rng k3 c= BOOLEAN
                     by FUNCT_2:def 2;
  consider k4 being Function such that
    A3: (a 'or' 'not' b) '&' ('not' a 'or' b)
        =k4 & dom k4=Y & rng k4 c= BOOLEAN
                     by FUNCT_2:def 2;
     Y=dom k3 & Y=dom k4 & (for u being set
            st u in Y holds k3.u=k4.u)by A1,A2,A3;
  hence thesis by A2,A3,FUNCT_1:9;
end;

theorem for a,b being Element of Funcs(Y,BOOLEAN) holds
a 'eqv' b = (a '&' b) 'or' ('not' a '&' 'not' b)
proof
  let a,b be Element of Funcs(Y,BOOLEAN);
  A1:for x being Element of Y holds
   Pj(a 'eqv' b,x) = Pj((a '&' b) 'or' ('not' a '&' 'not' b),x)
  proof
    let x be Element of Y;
      Pj((a '&' b) 'or' ('not' a '&' 'not' b),x)
   =Pj(((a '&' b) 'or' 'not' a) '&' ((a '&' b) 'or' 'not' b),x)
   by BVFUNC_1:14
  .=Pj(((a 'or' 'not' a) '&' (b 'or' 'not' a)) '&' ((a '&' b) 'or' 'not' b),x)
   by BVFUNC_1:14
  .=Pj(((a 'or' 'not' a) '&' (b 'or' 'not' a)) '&'
       ((a 'or' 'not' b) '&' (b 'or' 'not' b)),x)
   by BVFUNC_1:14
  .=Pj((I_el(Y) '&' (b 'or' 'not' a)) '&'
       ((a 'or' 'not' b) '&' (b 'or' 'not' b)),x)
   by BVFUNC_4:6
  .=Pj((I_el(Y) '&' (b 'or' 'not' a)) '&'
       ((a 'or' 'not' b) '&' I_el(Y)),x)
   by BVFUNC_4:6
  .=Pj((b 'or' 'not' a) '&'
       ((a 'or' 'not' b) '&' I_el(Y)),x)
   by BVFUNC_1:9
  .=Pj((b 'or' 'not' a) '&' (a 'or' 'not' b),x)
   by BVFUNC_1:9
  .=Pj(a 'eqv' b,x) by Th18;
    hence thesis;
  end;
  consider k3 being Function such that
    A2: (a 'eqv' b)=k3 & dom k3=Y & rng k3 c= BOOLEAN
                     by FUNCT_2:def 2;
  consider k4 being Function such that
    A3: (a '&' b) 'or' ('not' a '&' 'not' b)
        =k4 & dom k4=Y & rng k4 c= BOOLEAN
                     by FUNCT_2:def 2;
     Y=dom k3 & Y=dom k4 & (for u being set
            st u in Y holds k3.u=k4.u)by A1,A2,A3;
  hence thesis by A2,A3,FUNCT_1:9;
end;

theorem for a being Element of Funcs(Y,BOOLEAN) holds
a 'eqv' I_el(Y) = a
proof
  let a be Element of Funcs(Y,BOOLEAN);
  A1:for x being Element of Y holds
   Pj(a 'eqv' I_el(Y),x) = Pj(a,x)
  proof
    let x be Element of Y;
      Pj(a 'eqv' I_el(Y),x)
   =Pj((a 'imp' I_el(Y)) '&' (I_el(Y) 'imp' a),x)
   by BVFUNC_4:7
  .=Pj(('not' a 'or' I_el(Y)) '&' (I_el(Y) 'imp' a),x)
   by BVFUNC_4:8
  .=Pj(('not' a 'or' I_el(Y)) '&' ('not' I_el(Y) 'or' a),x)
   by BVFUNC_4:8
  .=Pj(I_el(Y) '&' ('not' I_el(Y) 'or' a),x)
   by BVFUNC_1:13
  .=Pj(I_el(Y) '&' (O_el(Y) 'or' a),x)
   by BVFUNC_1:5
  .=Pj(I_el(Y) '&' a,x)
   by BVFUNC_1:12
  .=Pj(a,x) by BVFUNC_1:9;
    hence thesis;
  end;
  consider k3 being Function such that
    A2: (a 'eqv' I_el(Y))=k3 & dom k3=Y & rng k3 c= BOOLEAN
                     by FUNCT_2:def 2;
  consider k4 being Function such that
    A3: a
        =k4 & dom k4=Y & rng k4 c= BOOLEAN
                     by FUNCT_2:def 2;
     Y=dom k3 & Y=dom k4 & (for u being set
            st u in Y holds k3.u=k4.u)by A1,A2,A3;
  hence thesis by A2,A3,FUNCT_1:9;
end;

theorem for a being Element of Funcs(Y,BOOLEAN) holds
a 'eqv' O_el(Y) = 'not' a
proof
  let a be Element of Funcs(Y,BOOLEAN);
  A1:for x being Element of Y holds
   Pj(a 'eqv' O_el(Y),x) = Pj('not' a,x)
  proof
    let x be Element of Y;
      Pj(a 'eqv' O_el(Y),x)
   =Pj((a 'imp' O_el(Y)) '&' (O_el(Y) 'imp' a),x)
   by BVFUNC_4:7
  .=Pj(('not' a 'or' O_el(Y)) '&' (O_el(Y) 'imp' a),x)
   by BVFUNC_4:8
  .=Pj(('not' a 'or' O_el(Y)) '&' ('not' O_el(Y) 'or' a),x)
   by BVFUNC_4:8
  .=Pj('not' a '&' ('not' O_el(Y) 'or' a),x)
   by BVFUNC_1:12
  .=Pj('not' a '&' (I_el(Y) 'or' a),x)
   by BVFUNC_1:5
  .=Pj('not' a '&' I_el(Y),x)
   by BVFUNC_1:13
  .=Pj('not' a,x) by BVFUNC_1:9;
    hence thesis;
  end;
  consider k3 being Function such that
    A2: (a 'eqv' O_el(Y))=k3 & dom k3=Y & rng k3 c= BOOLEAN
                     by FUNCT_2:def 2;
  consider k4 being Function such that
    A3: 'not' a
        =k4 & dom k4=Y & rng k4 c= BOOLEAN
                     by FUNCT_2:def 2;
     Y=dom k3 & Y=dom k4 & (for u being set
            st u in Y holds k3.u=k4.u)by A1,A2,A3;
  hence thesis by A2,A3,FUNCT_1:9;
end;

theorem for a,b being Element of Funcs(Y,BOOLEAN) holds
'not'( a 'eqv' b) = (a 'eqv' 'not' b)
proof
  let a,b be Element of Funcs(Y,BOOLEAN);
  A1:for x being Element of Y holds
   Pj('not'( a 'eqv' b),x) = Pj(a 'eqv' 'not' b,x)
  proof
    let x be Element of Y;
      Pj('not'( a 'eqv' b),x)
   =Pj('not'( (a 'imp' b) '&' (b 'imp' a)),x) by BVFUNC_4:7
  .=Pj('not'( ('not' a 'or' b) '&' (b 'imp' a)),x) by BVFUNC_4:8
  .=Pj('not'( ('not' a 'or' b) '&' ('not' b 'or' a)),x) by BVFUNC_4:8
  .=Pj('not'('not' a 'or' b) 'or' 'not'('not' b 'or' a),x) by BVFUNC_1:17
  .=Pj(('not' 'not' a '&' 'not' b) 'or' 'not'('not' b 'or' a),x) by BVFUNC_1:16
  .=Pj(('not' 'not' a '&' 'not' b) 'or' ('not' 'not' b '&' 'not' a),x)
  by BVFUNC_1:16
  .=Pj((a '&' 'not' b) 'or' ('not' 'not' b '&' 'not' a),x) by BVFUNC_1:4
  .=Pj((a '&' 'not' b) 'or' (b '&' 'not' a),x) by BVFUNC_1:4
  .=Pj(((a '&' 'not' b) 'or' b) '&' ((a '&' 'not' b) 'or' 'not'
a),x) by BVFUNC_1:14
  .=Pj(((a 'or' b) '&' ('not' b 'or' b)) '&' ((a '&' 'not' b) 'or' 'not' a),x)
   by BVFUNC_1:14
  .=Pj(((a 'or' b) '&' ('not' b 'or' b)) '&'
       ((a 'or' 'not' a) '&' ('not' b 'or' 'not' a)),x) by BVFUNC_1:14
  .=Pj(((a 'or' b) '&' I_el(Y)) '&'
       ((a 'or' 'not' a) '&' ('not' b 'or' 'not' a)),x) by BVFUNC_4:6
  .=Pj(((a 'or' b) '&' I_el(Y)) '&'
       (I_el(Y) '&' ('not' b 'or' 'not' a)),x) by BVFUNC_4:6
  .=Pj((a 'or' b) '&' (I_el(Y) '&' ('not' b 'or' 'not' a)),x) by BVFUNC_1:9
  .=Pj((a 'or' b) '&' ('not' b 'or' 'not' a),x) by BVFUNC_1:9
  .=Pj(('not' a 'or' 'not' b) '&' ('not' 'not' b 'or' a),x) by BVFUNC_1:4
  .=Pj(('not' a 'or' 'not' b) '&' ('not' b 'imp' a),x) by BVFUNC_4:8
  .=Pj((a 'imp' 'not' b) '&' ('not' b 'imp' a),x) by BVFUNC_4:8
  .=Pj(a 'eqv' 'not' b,x) by BVFUNC_4:7;
    hence thesis;
  end;
  consider k3 being Function such that
    A2: ('not'( a 'eqv' b))=k3 & dom k3=Y & rng k3 c= BOOLEAN
                     by FUNCT_2:def 2;
  consider k4 being Function such that
    A3: (a 'eqv' 'not' b)
        =k4 & dom k4=Y & rng k4 c= BOOLEAN
                     by FUNCT_2:def 2;
     Y=dom k3 & Y=dom k4 & (for u being set
            st u in Y holds k3.u=k4.u)by A1,A2,A3;
  hence thesis by A2,A3,FUNCT_1:9;
end;

theorem for a,b being Element of Funcs(Y,BOOLEAN) holds
'not' a '<' (a 'imp' b) 'eqv' 'not' a
proof
  let a,b be Element of Funcs(Y,BOOLEAN);
    let z be Element of Y;
    assume A1:Pj('not' a,z)=TRUE;
    then 'not' Pj(a,z)=TRUE by VALUAT_1:def 5;
    then A2:Pj(a,z)=FALSE by MARGREL1:41;
      Pj((a 'imp' b) 'eqv' 'not' a,z)
   =Pj(('not' a 'or' b) 'eqv' 'not' a,z) by BVFUNC_4:8
  .=Pj((('not' a 'or' b) 'imp' 'not' a) '&' ('not' a 'imp' ('not'
a 'or' b)),z) by BVFUNC_4:7
  .=Pj(('not'('not' a 'or' b) 'or' 'not' a) '&' ('not' a 'imp' ('not'
a 'or' b)),z) by BVFUNC_4:8
  .=Pj(('not'('not' a 'or' b) 'or' 'not' a) '&' ('not' 'not' a 'or' ('not'
a 'or' b)),z) by BVFUNC_4:8
  .=Pj('not'('not' a 'or' b) 'or' 'not' a,z) '&' Pj('not' 'not' a 'or' ('not'
a 'or' b),z)
   by VALUAT_1:def 6
  .=(Pj('not'('not' a 'or' b),z) 'or' Pj('not' a,z)) '&'
  Pj('not' 'not' a 'or' ('not' a 'or' b),z)
   by BVFUNC_1:def 7
  .=('not' Pj('not' a 'or' b,z) 'or' Pj('not' a,z)) '&'
  Pj('not' 'not' a 'or' ('not'
a 'or' b),z)
   by VALUAT_1:def 5
  .=('not'( Pj('not' a,z) 'or' Pj(b,z)) 'or' Pj('not' a,z)) '&' Pj('not' 'not'
a 'or' ('not' a 'or' b),z)
   by BVFUNC_1:def 7
  .=('not'('not' Pj(a,z) 'or' Pj(b,z)) 'or' Pj('not' a,z)) '&' Pj('not' 'not'
a 'or' ('not' a 'or' b),z)
   by VALUAT_1:def 5
  .=(('not' 'not' Pj(a,z) '&' 'not' Pj(b,z)) 'or' Pj('not' a,z)) '&'
  Pj('not' 'not'
a 'or' ('not' a 'or' b),z)
   by BINARITH:10
  .=((Pj(a,z) '&' 'not' Pj(b,z)) 'or' Pj('not' a,z)) '&'
  Pj('not' 'not' a 'or' (
'not' a 'or' b),z)
   by MARGREL1:40
  .=((Pj(a,z) '&' 'not' Pj(b,z)) 'or' Pj('not' a,z)) '&'
     (Pj('not' 'not' a,z) 'or' Pj('not' a 'or' b,z))
   by BVFUNC_1:def 7
  .=((Pj(a,z) '&' 'not' Pj(b,z)) 'or' Pj('not' a,z)) '&'
    (Pj('not' 'not' a,z) 'or' (Pj('not' a,z) 'or' Pj(b,z)))
   by BVFUNC_1:def 7
  .=((Pj(a,z) '&' 'not' Pj(b,z)) 'or' Pj('not' a,z)) '&'
    (Pj('not' 'not' a,z) 'or' ('not' Pj(a,z) 'or' Pj(b,z)))
   by VALUAT_1:def 5
  .=((Pj(a,z) '&' 'not' Pj(b,z)) 'or' Pj('not' a,z)) '&'
    (Pj(a,z) 'or' ('not' Pj(a,z) 'or' Pj(b,z)))
   by BVFUNC_1:4
  .=((Pj(a,z) '&' 'not' Pj(b,z)) 'or' Pj('not' a,z)) '&'
    (Pj(a,z) 'or' (Pj('not' a,z) 'or' Pj(b,z)))
   by VALUAT_1:def 5
  .=TRUE '&' (FALSE 'or' (TRUE 'or' Pj(b,z)))
   by A1,A2,BINARITH:19
  .=FALSE 'or' (TRUE 'or' Pj(b,z))
   by MARGREL1:50
  .=(TRUE 'or' Pj(b,z))
   by BINARITH:7
  .=TRUE by BINARITH:19;
    hence thesis;
end;

theorem for a,b being Element of Funcs(Y,BOOLEAN) holds
'not' a '<' (b 'imp' a) 'eqv' 'not' b
proof
  let a,b be Element of Funcs(Y,BOOLEAN);
    let z be Element of Y;
    assume Pj('not' a,z)=TRUE;
    then A1: 'not' Pj(a,z)=TRUE by VALUAT_1:def 5;
      Pj((b 'imp' a) 'eqv' 'not' b,z)
   =Pj(('not' b 'or' a) 'eqv' 'not' b,z) by BVFUNC_4:8
  .=Pj((('not' b 'or' a) 'imp' 'not' b) '&' ('not' b 'imp' ('not'
b 'or' a)),z) by BVFUNC_4:7
  .=Pj(('not'('not' b 'or' a) 'or' 'not' b) '&' ('not' b 'imp' ('not'
b 'or' a)),z) by BVFUNC_4:8
  .=Pj(('not'('not' b 'or' a) 'or' 'not' b) '&' ('not' 'not' b 'or' ('not'
b 'or' a)),z) by BVFUNC_4:8
  .=Pj('not'('not' b 'or' a) 'or' 'not' b,z) '&' Pj('not' 'not' b 'or' ('not'
b 'or' a),z)
   by VALUAT_1:def 6
  .=(Pj('not'('not' b 'or' a),z) 'or' Pj('not' b,z)) '&'
  Pj('not' 'not' b 'or' ('not' b 'or' a),z)
   by BVFUNC_1:def 7
  .=('not' Pj('not' b 'or' a,z) 'or' Pj('not' b,z)) '&'
  Pj('not' 'not' b 'or' ('not'
b 'or' a),z)
   by VALUAT_1:def 5
  .=('not'( Pj('not' b,z) 'or' Pj(a,z)) 'or' Pj('not' b,z)) '&' Pj('not' 'not'
b 'or' ('not' b 'or' a),z)
   by BVFUNC_1:def 7
  .=('not'('not' Pj(b,z) 'or' Pj(a,z)) 'or' Pj('not' b,z)) '&' Pj('not' 'not'
b 'or' ('not' b 'or' a),z)
   by VALUAT_1:def 5
  .=(('not' 'not' Pj(b,z) '&' 'not' Pj(a,z)) 'or' Pj('not' b,z)) '&'
  Pj('not' 'not'
b 'or' ('not' b 'or' a),z)
   by BINARITH:10
  .=((Pj(b,z) '&' 'not' Pj(a,z)) 'or' Pj('not' b,z)) '&'
  Pj('not' 'not' b 'or' (
'not' b 'or' a),z)
   by MARGREL1:40
  .=((Pj(b,z) '&' 'not' Pj(a,z)) 'or' Pj('not' b,z)) '&' (Pj('not' 'not'
b,z) 'or' Pj('not' b 'or' a,z))
   by BVFUNC_1:def 7
  .=((Pj(b,z) '&' 'not' Pj(a,z)) 'or' Pj('not' b,z)) '&'
    (Pj('not' 'not' b,z) 'or' (Pj('not' b,z) 'or' Pj(a,z))) by BVFUNC_1:def 7
  .=((Pj(b,z) '&' 'not' Pj(a,z)) 'or' Pj('not' b,z)) '&'
    (Pj('not' 'not' b,z) 'or' ('not' Pj(b,z) 'or' Pj(a,z))) by VALUAT_1:def 5
  .=((Pj(b,z) '&' 'not' Pj(a,z)) 'or' Pj('not' b,z)) '&'
    (Pj(b,z) 'or' ('not' Pj(b,z) 'or' Pj(a,z))) by BVFUNC_1:4
  .=((TRUE '&' Pj(b,z)) 'or' Pj('not' b,z)) '&'
    (Pj(b,z) 'or' ('not' Pj(b,z) 'or' FALSE)) by A1,MARGREL1:41
  .=(Pj(b,z) 'or' Pj('not' b,z)) '&'
    (Pj(b,z) 'or' ('not' Pj(b,z) 'or' FALSE)) by MARGREL1:50
  .=(Pj(b,z) 'or' 'not' Pj(b,z)) '&'
    (Pj(b,z) 'or' ('not' Pj(b,z) 'or' FALSE)) by VALUAT_1:def 5
  .=TRUE '&' (Pj(b,z) 'or' ('not' Pj(b,z) 'or' FALSE)) by BINARITH:18
  .=Pj(b,z) 'or' ('not' Pj(b,z) 'or' FALSE) by MARGREL1:50
  .=Pj(b,z) 'or' 'not' Pj(b,z) 'or' FALSE by BINARITH:20
  .=TRUE 'or' FALSE by BINARITH:18
  .=TRUE by BINARITH:19;
    hence thesis;
end;

theorem for a,b being Element of Funcs(Y,BOOLEAN) holds
a '<' (a 'or' b) 'eqv' (b 'or' a) 'eqv' a
proof
  let a,b be Element of Funcs(Y,BOOLEAN);
    let z be Element of Y;
    assume A1:Pj(a,z)=TRUE;
A2:Pj((a 'or' b) 'eqv' (b 'or' a),z)
   =Pj(((a 'or' b) 'imp' (a 'or' b)) '&' ((a 'or' b) 'imp' (a 'or' b)),z)
   by BVFUNC_4:7
  .=Pj((a 'or' b) 'imp' (a 'or' b),z) '&' Pj((a 'or' b) 'imp' (a 'or' b),z)
   by VALUAT_1:def 6
  .=Pj((a 'or' b) 'imp' (a 'or' b),z)
   by BINARITH:16
  .=Pj('not'( a 'or' b) 'or' (a 'or' b),z)
   by BVFUNC_4:8
  .=Pj(I_el(Y),z) by BVFUNC_4:6
  .=TRUE by BVFUNC_1:def 14;
      Pj((a 'or' b) 'eqv' (b 'or' a) 'eqv' a,z)
   =Pj((((a 'or' b) 'eqv' (a 'or' b)) 'imp' a) '&'
       (a 'imp' ((a 'or' b) 'eqv' (a 'or' b))),z) by BVFUNC_4:7
  .=Pj(((a 'or' b) 'eqv' (a 'or' b)) 'imp' a,z) '&'
    Pj(a 'imp' ((a 'or' b) 'eqv' (a 'or' b)),z)
   by VALUAT_1:def 6
  .=Pj('not'( (a 'or' b) 'eqv' (a 'or' b)) 'or' a,z) '&'
    Pj(a 'imp' ((a 'or' b) 'eqv' (a 'or' b)),z)
   by BVFUNC_4:8
  .=Pj('not'( (a 'or' b) 'eqv' (a 'or' b)) 'or' a,z) '&'
    Pj('not' a 'or' ((a 'or' b) 'eqv' (a 'or' b)),z)
   by BVFUNC_4:8
  .=(Pj('not'( (a 'or' b) 'eqv' (a 'or' b)),z) 'or' Pj(a,z)) '&'
    Pj('not' a 'or' ((a 'or' b) 'eqv' (a 'or' b)),z)
   by BVFUNC_1:def 7
  .=(Pj('not'( (a 'or' b) 'eqv' (a 'or' b)),z) 'or' Pj(a,z)) '&'
    (Pj('not' a,z) 'or' Pj((a 'or' b) 'eqv' (a 'or' b),z))
   by BVFUNC_1:def 7
  .=('not' Pj((a 'or' b) 'eqv' (a 'or' b),z) 'or' Pj(a,z)) '&'
    (Pj('not' a,z) 'or' Pj((a 'or' b) 'eqv' (a 'or' b),z)) by VALUAT_1:def 5
  .=(FALSE 'or' Pj(a,z)) '&' (Pj('not' a,z) 'or' TRUE) by A2,MARGREL1:41
  .=Pj(a,z) '&' (Pj('not' a,z) 'or' TRUE) by BINARITH:7
  .=Pj(a,z) '&' TRUE by BINARITH:19
  .=TRUE by A1,MARGREL1:50;
    hence thesis;
end;

theorem for a being Element of Funcs(Y,BOOLEAN) holds
a 'imp' ('not' a 'eqv' 'not' a) = I_el(Y)
proof
  let a be Element of Funcs(Y,BOOLEAN);
    for x being Element of Y holds
   Pj(a 'imp' ('not' a 'eqv' 'not' a),x) = TRUE
  proof
    let x be Element of Y;
      Pj(a 'imp' ('not' a 'eqv' 'not' a),x)
   =Pj('not' a 'or' ('not' a 'eqv' 'not' a),x) by BVFUNC_4:8
  .=Pj('not' a 'or' (('not' a 'imp' 'not' a) '&' ('not' a 'imp' 'not'
a)),x) by BVFUNC_4:7
  .=Pj('not' a 'or' ('not' a 'imp' 'not' a),x) by BVFUNC_1:6
  .=Pj('not' a 'or' ('not' 'not' a 'or' 'not' a),x) by BVFUNC_4:8
  .=Pj('not' a 'or' I_el(Y),x) by BVFUNC_4:6
  .=Pj(I_el(Y),x) by BVFUNC_1:13
  .=TRUE by BVFUNC_1:def 14;
    hence thesis;
  end;
  hence thesis by BVFUNC_1:def 14;
end;

theorem for a,b being Element of Funcs(Y,BOOLEAN) holds
((a 'imp' b) 'imp' a) 'imp' a = I_el(Y)
proof
  let a,b be Element of Funcs(Y,BOOLEAN);
    for x being Element of Y holds
   Pj(((a 'imp' b) 'imp' a) 'imp' a,x) = TRUE
  proof
    let x be Element of Y;
      Pj(((a 'imp' b) 'imp' a) 'imp' a,x)
   =Pj('not'( (a 'imp' b) 'imp' a) 'or' a,x) by BVFUNC_4:8
  .=Pj('not'('not'( a 'imp' b) 'or' a) 'or' a,x) by BVFUNC_4:8
  .=Pj('not'('not'('not' a 'or' b) 'or' a) 'or' a,x) by BVFUNC_4:8
  .=Pj('not'( ('not' 'not' a '&' 'not' b) 'or' a) 'or' a,x) by BVFUNC_1:16
  .=Pj('not'( (a '&' 'not' b) 'or' a) 'or' a,x) by BVFUNC_1:4
  .=Pj('not'( ((a 'or' a) '&' ('not' b 'or' a))) 'or' a,x) by BVFUNC_1:14
  .=Pj('not'( a '&' ('not' b 'or' a)) 'or' a,x) by BVFUNC_1:10
  .=Pj(('not' a 'or' 'not'('not' b 'or' a)) 'or' a,x) by BVFUNC_1:17
  .=Pj(('not' a 'or' ('not' 'not' b '&' 'not' a)) 'or' a,x) by BVFUNC_1:16
  .=Pj(('not' a 'or' (b '&' 'not' a)) 'or' a,x) by BVFUNC_1:4
  .=Pj((('not' a 'or' b) '&' ('not' a 'or' 'not' a)) 'or' a,x) by BVFUNC_1:14
  .=Pj((('not' a 'or' b) '&' 'not' a) 'or' a,x) by BVFUNC_1:10
  .=Pj((('not' a 'or' b) 'or' a) '&' ('not' a 'or' a),x) by BVFUNC_1:14
  .=Pj((('not' a 'or' b) 'or' a) '&' I_el(Y),x) by BVFUNC_4:6
  .=Pj(('not' a 'or' b) 'or' a,x) by BVFUNC_1:9
  .=Pj(b 'or' ('not' a 'or' a),x) by BVFUNC_1:11
  .=Pj(b 'or' I_el(Y),x) by BVFUNC_4:6
  .=Pj(I_el(Y),x) by BVFUNC_1:13
  .=TRUE by BVFUNC_1:def 14;
    hence thesis;
  end;
  hence thesis by BVFUNC_1:def 14;
end;

theorem for a,b,c,d being Element of Funcs(Y,BOOLEAN) holds
((a 'imp' c) '&' (b 'imp' d)) '&'
('not' c 'or' 'not' d) 'imp' ('not' a 'or' 'not' b)=I_el(Y)
proof
  let a,b,c,d be Element of Funcs(Y,BOOLEAN);
    for x being Element of Y holds
   Pj(((a 'imp' c) '&' (b 'imp' d)) '&'
      ('not' c 'or' 'not' d) 'imp' ('not' a 'or' 'not' b),x) = TRUE
  proof
    let x be Element of Y;
      ((a 'imp' c) '&' (b 'imp' d)) '&' ('not' c 'or' 'not' d)
    'imp' ('not' a 'or'
'not' b)
   ='not'( ((a 'imp' c) '&' (b 'imp' d)) '&' ('not' c 'or' 'not' d))
   'or' ('not'
a 'or' 'not' b)
   by BVFUNC_4:8
  .='not'( (('not' a 'or' c) '&' (b 'imp' d)) '&' ('not' c 'or' 'not' d))
  'or' ('not' a 'or' 'not' b)
   by BVFUNC_4:8
  .='not'( (('not' a 'or' c) '&' ('not' b 'or' d)) '&' ('not' c 'or' 'not'
d)) 'or' ('not' a 'or' 'not' b)
   by BVFUNC_4:8
  .=('not'( ('not' a 'or' c) '&' ('not' b 'or' d)) 'or'
  'not'('not' c 'or' 'not'
d)) 'or' ('not' a 'or' 'not' b)
   by BVFUNC_1:17
  .=(('not'('not' a 'or' c) 'or' 'not'('not' b 'or' d)) 'or' 'not'('not' c 'or'
'not' d)) 'or' ('not' a 'or' 'not' b)
   by BVFUNC_1:17
  .=((('not' 'not' a '&' 'not' c) 'or' 'not'('not' b 'or' d)) 'or' 'not'('not'
c 'or' 'not' d)) 'or' ('not' a 'or' 'not' b)
   by BVFUNC_1:16
  .=(((a '&' 'not' c) 'or' 'not'('not' b 'or' d)) 'or' 'not'('not' c 'or' 'not'
d)) 'or' ('not' a 'or' 'not' b)
   by BVFUNC_1:4
  .=(((a '&' 'not' c) 'or' ('not' 'not' b '&' 'not' d)) 'or' 'not'('not' c 'or'
'not' d)) 'or' ('not' a 'or' 'not' b)
   by BVFUNC_1:16
  .=(((a '&' 'not' c) 'or' (b '&' 'not' d)) 'or' 'not'('not' c 'or' 'not'
d)) 'or' ('not' a 'or' 'not' b)
   by BVFUNC_1:4
  .=(((a '&' 'not' c) 'or' (b '&' 'not' d)) 'or' ('not' 'not' c '&' 'not' 'not'
d)) 'or' ('not' a 'or' 'not' b)
   by BVFUNC_1:16
  .=(((a '&' 'not' c) 'or' (b '&' 'not' d)) 'or'
  (c '&' 'not' 'not' d)) 'or' ('not'
a 'or' 'not' b)
   by BVFUNC_1:4
  .=(((a '&' 'not' c) 'or' (b '&' 'not' d)) 'or' (c '&' d)) 'or' ('not' a 'or'
'not' b)
   by BVFUNC_1:4
  .=((a '&' 'not' c) 'or' ((b '&' 'not' d) 'or' (c '&' d))) 'or' ('not' a 'or'
'not' b)
   by BVFUNC_1:11
  .=((a '&' 'not' c) 'or' ((b 'or' (c '&' d)) '&' ('not' d 'or' (c '&' d))))
    'or' ('not' a 'or' 'not' b)
   by BVFUNC_1:14
  .=((a '&' 'not' c) 'or' ((b 'or' (c '&' d)) '&' (('not' d 'or' c) '&' ('not'
d 'or' d))))
    'or' ('not' a 'or' 'not' b)
   by BVFUNC_1:14
  .=((a '&' 'not' c) 'or' ((b 'or' (c '&' d)) '&' (('not'
d 'or' c) '&' I_el(Y))))
    'or' ('not' a 'or' 'not' b) by BVFUNC_4:6
  .=((a '&' 'not' c) 'or' ((b 'or' (c '&' d)) '&' ('not' d 'or' c)))
    'or' ('not' a 'or' 'not' b) by BVFUNC_1:9
  .=((b 'or' (c '&' d)) '&' ('not' d 'or' c)) 'or'
    ((a '&' 'not' c) 'or' ('not' a 'or' 'not' b)) by BVFUNC_1:11
  .=((b 'or' (c '&' d)) '&' ('not' d 'or' c)) 'or'
    ((a 'or' ('not' a 'or' 'not' b)) '&' ('not' c 'or' ('not' a 'or' 'not'
b))) by BVFUNC_1:14
  .=((b 'or' (c '&' d)) '&' ('not' d 'or' c)) 'or'
    (((a 'or' 'not' a) 'or' 'not' b) '&' ('not' c 'or' ('not' a 'or' 'not'
b))) by BVFUNC_1:11
  .=((b 'or' (c '&' d)) '&' ('not' d 'or' c)) 'or'
    ((I_el(Y) 'or' 'not' b) '&' ('not' c 'or' ('not' a 'or' 'not'
b))) by BVFUNC_4:6
  .=((b 'or' (c '&' d)) '&' ('not' d 'or' c)) 'or'
    (I_el(Y) '&' ('not' c 'or' ('not' a 'or' 'not' b))) by BVFUNC_1:13
  .=((b 'or' (c '&' d)) '&' ('not' d 'or' c)) 'or' ('not' c 'or' ('not' a 'or'
'not' b))
   by BVFUNC_1:9
  .=((b 'or' (c '&' d)) 'or' ('not' c 'or' ('not' a 'or' 'not' b))) '&'
    (('not' d 'or' c) 'or' ('not' c 'or' ('not' a 'or' 'not' b)))
    by BVFUNC_1:14
  .=((b 'or' (c '&' d)) 'or' ('not' c 'or' ('not' a 'or' 'not' b))) '&'
    ((('not' d 'or' c) 'or' 'not' c) 'or' ('not' a 'or' 'not' b))
    by BVFUNC_1:11
  .=((b 'or' (c '&' d)) 'or' ('not' c 'or' ('not' a 'or' 'not' b))) '&'
    (('not' d 'or' (c 'or' 'not' c)) 'or' ('not' a 'or' 'not' b))
    by BVFUNC_1:11
  .=((b 'or' (c '&' d)) 'or' ('not' c 'or' ('not' a 'or' 'not' b))) '&'
    (('not' d 'or' I_el(Y)) 'or' ('not' a 'or' 'not' b)) by BVFUNC_4:6
  .=((b 'or' (c '&' d)) 'or' ('not' c 'or' ('not' a 'or' 'not' b))) '&'
    (I_el(Y) 'or' ('not' a 'or' 'not' b)) by BVFUNC_1:13
  .=((b 'or' (c '&' d)) 'or' ('not' c 'or' ('not' a 'or' 'not' b))) '&'
    I_el(Y) by BVFUNC_1:13
  .=(b 'or' (c '&' d)) 'or' ('not' c 'or' ('not' a 'or' 'not' b)) by BVFUNC_1:9
  .=(c '&' d) 'or' (b 'or' ('not' c 'or' ('not' a 'or' 'not' b)))
  by BVFUNC_1:11
  .=(c '&' d) 'or' ((b 'or' ('not' b 'or' 'not' a)) 'or' 'not' c)
  by BVFUNC_1:11
  .=(c '&' d) 'or' (((b 'or' 'not' b) 'or' 'not' a) 'or' 'not' c)
  by BVFUNC_1:11
  .=(c '&' d) 'or' ((I_el(Y) 'or' 'not' a) 'or' 'not' c) by BVFUNC_4:6
  .=(c '&' d) 'or' (I_el(Y) 'or' 'not' c) by BVFUNC_1:13
  .=(c '&' d) 'or' I_el(Y) by BVFUNC_1:13
  .=I_el(Y) by BVFUNC_1:13;
    hence thesis by BVFUNC_1:def 14;
  end;
  hence thesis by BVFUNC_1:def 14;
end;

theorem for a,b,c being Element of Funcs(Y,BOOLEAN) holds
(a 'imp' b) 'imp' ((a 'imp' (b 'imp' c)) 'imp' (a 'imp' c)) = I_el(Y)
proof
  let a,b,c be Element of Funcs(Y,BOOLEAN);
    for x being Element of Y holds
   Pj((a 'imp' b) 'imp' ((a 'imp' (b 'imp' c)) 'imp' (a 'imp' c)),x)=TRUE
  proof
    let x be Element of Y;
  (a 'imp' b) 'imp' ((a 'imp' (b 'imp' c)) 'imp' (a 'imp' c))
   ='not'
(a 'imp' b) 'or' ((a 'imp' (b 'imp' c)) 'imp' (a 'imp' c)) by BVFUNC_4:8
  .='not'('not'
a 'or' b) 'or' ((a 'imp' (b 'imp' c)) 'imp' (a 'imp' c)) by BVFUNC_4:8
  .='not'('not' a 'or' b) 'or' (('not'
a 'or' (b 'imp' c)) 'imp' (a 'imp' c)) by BVFUNC_4:8
  .='not'('not' a 'or' b) 'or' (('not' a 'or' ('not'
b 'or' c)) 'imp' (a 'imp' c)) by BVFUNC_4:8
  .='not'('not' a 'or' b) 'or' (('not' a 'or' ('not' b 'or' c)) 'imp' ('not'
a 'or' c)) by BVFUNC_4:8
  .='not'('not' a 'or' b) 'or' ('not'('not' a 'or'
  ('not' b 'or' c)) 'or' ('not'
a 'or' c)) by BVFUNC_4:8
  .=('not' 'not' a '&' 'not' b) 'or' ('not'('not' a 'or'
  ('not' b 'or' c)) 'or' (
'not' a 'or' c)) by BVFUNC_1:16
  .=('not' 'not' a '&' 'not' b) 'or' (('not' 'not' a '&' 'not'('not'
b 'or' c)) 'or' ('not' a 'or' c)) by BVFUNC_1:16
  .=('not' 'not' a '&' 'not' b) 'or' (('not' 'not' a '&'
  ('not' 'not' b '&' 'not'
c)) 'or' ('not' a 'or' c)) by BVFUNC_1:16
  .=(a '&' 'not' b) 'or' (('not' 'not' a '&' ('not' 'not' b
  '&' 'not' c)) 'or' ('not'
a 'or' c)) by BVFUNC_1:4
  .=(a '&' 'not' b) 'or' ((a '&' ('not' 'not' b '&' 'not' c)) 'or' ('not'
a 'or' c)) by BVFUNC_1:4
  .=(a '&' 'not' b) 'or' ((a '&' (b '&' 'not' c)) 'or' ('not'
a 'or' c)) by BVFUNC_1:4
  .=(a '&' 'not' b) 'or'
    ((a 'or' ('not' a 'or' c)) '&' ((b '&' 'not' c) 'or' ('not'
a 'or' c))) by BVFUNC_1:14
  .=(a '&' 'not' b) 'or'
    (((a 'or' 'not' a) 'or' c) '&' ((b '&' 'not' c) 'or' ('not'
a 'or' c))) by BVFUNC_1:11
  .=(a '&' 'not' b) 'or'
    ((I_el(Y) 'or' c) '&' ((b '&' 'not' c) 'or' ('not' a 'or' c)))
    by BVFUNC_4:6
  .=(a '&' 'not' b) 'or'
    (I_el(Y) '&' ((b '&' 'not' c) 'or' ('not' a 'or' c))) by BVFUNC_1:13
  .=(a '&' 'not' b) 'or'
    ((b '&' 'not' c) 'or' ('not' a 'or' c)) by BVFUNC_1:9
  .=(a '&' 'not' b) 'or'
    ((b 'or' ('not' a 'or' c)) '&' ('not' c 'or' ('not' a 'or' c)))
    by BVFUNC_1:14
  .=(a '&' 'not' b) 'or'
    ((b 'or' ('not' a 'or' c)) '&' (('not' c 'or' c) 'or' 'not' a))
    by BVFUNC_1:11
  .=(a '&' 'not' b) 'or'
    ((b 'or' ('not' a 'or' c)) '&' (I_el(Y) 'or' 'not' a)) by BVFUNC_4:6
  .=(a '&' 'not' b) 'or'
    ((b 'or' ('not' a 'or' c)) '&' I_el(Y)) by BVFUNC_1:13
  .=(a '&' 'not' b) 'or' (b 'or' ('not' a 'or' c)) by BVFUNC_1:9
  .=(a 'or' (b 'or' ('not' a 'or' c))) '&' ('not' b 'or' (b 'or' ('not'
a 'or' c)))
   by BVFUNC_1:14
  .=(a 'or' (b 'or' ('not' a 'or' c))) '&' (('not' b 'or' b) 'or' ('not'
a 'or' c))
   by BVFUNC_1:11
  .=(a 'or' (b 'or' ('not' a 'or' c))) '&' (I_el(Y) 'or' ('not' a 'or' c))
   by BVFUNC_4:6
  .=(a 'or' (b 'or' ('not' a 'or' c))) '&' I_el(Y) by BVFUNC_1:13
  .=a 'or' (b 'or' ('not' a 'or' c)) by BVFUNC_1:9
  .=a 'or' (('not' a 'or' b) 'or' c) by BVFUNC_1:11
  .=a 'or' ('not' a 'or' b) 'or' c by BVFUNC_1:11
  .=(a 'or' 'not' a) 'or' b 'or' c by BVFUNC_1:11
  .=I_el(Y) 'or' b 'or' c by BVFUNC_4:6
  .=I_el(Y) 'or' c by BVFUNC_1:13
  .=I_el(Y) by BVFUNC_1:13;
    hence thesis by BVFUNC_1:def 14;
  end;
  hence thesis by BVFUNC_1:def 14;
end;

Back to top