BVFUNC25

:: Propositional Calculus for Boolean Valued Functions, {VII}
::  by Shunichi Kobayashi
::
:: Received February 6, 2003
:: Copyright (c) 2003-2026 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies XBOOLE_0, MARGREL1, XBOOLEAN, BVFUNC_1, PARTIT1, FUNCT_1,
      SUBSET_1, RELAT_1, TARSKI;
 notations TARSKI, XBOOLE_0, SUBSET_1, XBOOLEAN, RELAT_1, FUNCT_1, FUNCT_2,
      BVFUNC_1, MARGREL1;
 constructors BVFUNC_1, RELSET_1;
 registrations XBOOLE_0, FUNCT_2, XBOOLEAN, MARGREL1, RELSET_1;
 requirements SUBSET, BOOLE;
 definitions TARSKI, FUNCT_2, MARGREL1;
 theorems BVFUNC_1, BVFUNC_4, BVFUNC_5, BVFUNC_6, FUNCT_1, FUNCT_2, MARGREL1,
      XBOOLEAN, PARTFUN1;
 schemes FUNCT_1;

begin

reserve Y for non empty set,
  a,b,c,d for Function of Y,BOOLEAN;

theorem Th1:
  'not' (a 'imp' b) = a '&' 'not' b
proof
  thus 'not' (a 'imp' b)='not' ('not' a 'or' b) by BVFUNC_4:8
    .='not' 'not' a '&' 'not' b by BVFUNC_1:13
    .=a '&' 'not' b;
end;

theorem Th2:
  a 'imp' b = 'not' b 'imp' 'not' a
proof
  (a 'imp' b) 'imp' ('not' b 'imp' 'not' a)=I_el(Y) by BVFUNC_5:32;
  then
A1: a 'imp' b '<' 'not' b 'imp' 'not' a by BVFUNC_1:16;
  ('not' b 'imp' 'not' a) 'imp' (a 'imp' b)=I_el(Y) by BVFUNC_5:31;
  then ('not' b 'imp' 'not' a) '<' (a 'imp' b) by BVFUNC_1:16;
  hence thesis by A1,BVFUNC_1:15;
end;

theorem
  a 'eqv' b = 'not' a 'eqv' 'not' b
proof
  thus 'not' a 'eqv' 'not' b =('not' a 'imp' 'not' b) '&' ('not' b 'imp' 'not'
  a) by BVFUNC_4:7
    .=(b 'imp' a) '&' ('not' b 'imp' 'not' a) by Th2
    .=(b 'imp' a) '&' (a 'imp' b) by Th2
    .=a 'eqv' b by BVFUNC_4:7;
end;

theorem Th4:
  a 'imp' b = a 'imp' (a '&' b)
proof
  a 'imp' (a '&' b)='not' a 'or' (a '&' b) by BVFUNC_4:8
    .=('not' a 'or' a) '&' ('not' a 'or' b) by BVFUNC_1:11
    .=I_el(Y) '&' ('not' a 'or' b) by BVFUNC_4:6
    .='not' a 'or' b by BVFUNC_1:6;
  hence thesis by BVFUNC_4:8;
end;

theorem
  a 'eqv' b = (a 'or' b) 'imp' (a '&' b)
proof
  thus (a 'or' b) 'imp' (a '&' b) =(a 'imp' (a '&' b)) '&' (b 'imp' (a '&' b))
  by BVFUNC_6:51
    .=(a 'imp' b) '&' (b 'imp' (a '&' b)) by Th4
    .=(a 'imp' b) '&' (b 'imp' a) by Th4
    .=a 'eqv' b by BVFUNC_4:7;
end;

theorem
  a 'eqv' 'not' a = O_el(Y)
proof
  thus a 'eqv' 'not' a =(a 'imp' 'not' a) '&' ('not' a 'imp' a) by BVFUNC_4:7
    .=('not' a 'or' 'not' a) '&' ('not' a 'imp' a) by BVFUNC_4:8
    .='not' a '&' ('not' 'not' a 'or' a) by BVFUNC_4:8
    .=O_el(Y) by BVFUNC_4:5;
end;

theorem
  a 'imp' (b 'imp' c) = b 'imp' (a 'imp' c)
proof
  thus a 'imp' (b 'imp' c) ='not' a 'or' (b 'imp' c) by BVFUNC_4:8
    .='not' a 'or' ('not' b 'or' c) by BVFUNC_4:8
    .='not' b 'or' ('not' a 'or' c) by BVFUNC_1:8
    .='not' b 'or' (a 'imp' c) by BVFUNC_4:8
    .=b 'imp' (a 'imp' c) by BVFUNC_4:8;
end;

theorem
  a 'imp' (b 'imp' c) = (a 'imp' b) 'imp' (a 'imp' c)
proof
  thus (a 'imp' b) 'imp' (a 'imp' c) =(a 'imp' b) 'imp' ('not' a 'or' c) by
BVFUNC_4:8
    .='not' (a 'imp' b) 'or' ('not' a 'or' c) by BVFUNC_4:8
    .='not' ('not' a 'or' b) 'or' ('not' a 'or' c) by BVFUNC_4:8
    .=('not' 'not' a '&' 'not' b) 'or' ('not' a 'or' c) by BVFUNC_1:13
    .=((a '&' 'not' b) 'or' 'not' a) 'or' c by BVFUNC_1:8
    .=((a 'or' 'not' a) '&' ('not' b 'or' 'not' a)) 'or' c by BVFUNC_1:11
    .=(I_el(Y) '&' ('not' b 'or' 'not' a)) 'or' c by BVFUNC_4:6
    .=('not' a 'or' 'not' b) 'or' c by BVFUNC_1:6
    .='not' a 'or' ('not' b 'or' c) by BVFUNC_1:8
    .='not' a 'or' (b 'imp' c) by BVFUNC_4:8
    .=a 'imp' (b 'imp' c) by BVFUNC_4:8;
end;

theorem
  a 'eqv' b = a 'xor' 'not' b
proof
  'not' (a 'xor' b) = 'not' 'not' (a 'eqv' b) by BVFUNC_6:85;
  hence thesis by BVFUNC_6:90;
end;

theorem Th11:
  a '&' (b 'xor' c) = a '&' b 'xor' a '&' c
proof
A1: a '&' b 'xor' a '&' c =('not' (a '&' b) '&' (a '&' c)) 'or' ((a '&' b)
  '&' 'not' (a '&' c)) by BVFUNC_4:9
    .=(('not' a 'or' 'not' b) '&' (a '&' c)) 'or' ((a '&' b) '&' 'not' (a
  '&' c)) by BVFUNC_1:14
    .=((a '&' c) '&' ('not' a 'or' 'not' b)) 'or' ((a '&' b) '&' ('not' a
  'or' 'not' c)) by BVFUNC_1:14
    .=(((a '&' c) '&' 'not' a) 'or' ((a '&' c) '&' 'not' b)) 'or' ((a '&' b)
  '&' ('not' a 'or' 'not' c)) by BVFUNC_1:12
    .=(((a '&' c) '&' 'not' a) 'or' ((a '&' c) '&' 'not' b)) 'or' (((a '&' b
  ) '&' 'not' a) 'or' ((a '&' b) '&' 'not' c)) by BVFUNC_1:12
    .=((a '&' c) '&' 'not' a) 'or' (((a '&' c) '&' 'not' b) 'or' (((a '&' b)
  '&' 'not' c) 'or' ((a '&' b) '&' 'not' a))) by BVFUNC_1:8
    .=((a '&' c) '&' 'not' a) 'or' ((((a '&' c) '&' 'not' b) 'or' ((a '&' b)
  '&' 'not' c)) 'or' ((a '&' b) '&' 'not' a)) by BVFUNC_1:8
    .=(((a '&' c) '&' 'not' a) 'or' ((a '&' b) '&' 'not' a)) 'or' (((a '&' c
  ) '&' 'not' b) 'or' ((a '&' b) '&' 'not' c)) by BVFUNC_1:8;
A2: ((c '&' a) '&' 'not' a) 'or' ((b '&' a) '&' 'not' a) =(c '&' (a '&'
  'not' a)) 'or' ((b '&' a) '&' 'not' a) by BVFUNC_1:4
    .=(c '&' (a '&' 'not' a)) 'or' (b '&' (a '&' 'not' a)) by BVFUNC_1:4
    .=(c '&' O_el(Y)) 'or' (b '&' (a '&' 'not' a)) by BVFUNC_4:5
    .=(c '&' O_el(Y)) 'or' (b '&' O_el(Y)) by BVFUNC_4:5
    .=O_el(Y) 'or' (b '&' O_el(Y)) by BVFUNC_1:5
    .=O_el(Y) 'or' O_el(Y) by BVFUNC_1:5
    .=O_el(Y);
  a '&' (b 'xor' c) =a '&' (('not' b '&' c) 'or' (b '&' 'not' c)) by BVFUNC_4:9
    .=(a '&' ('not' b '&' c)) 'or' (a '&' (b '&' 'not' c)) by BVFUNC_1:12
    .=((a '&' c) '&' 'not' b) 'or' (a '&' (b '&' 'not' c)) by BVFUNC_1:4
    .=((a '&' c) '&' 'not' b) 'or' ((a '&' b) '&' 'not' c) by BVFUNC_1:4;
  hence thesis by A1,A2,BVFUNC_1:9;
end;

theorem Th12:
  a 'eqv' b = 'not' (a 'xor' b)
proof
  'not' (a 'xor' b) = 'not' 'not' (a 'eqv' b) by BVFUNC_6:85;
  hence thesis;
end;

theorem Th13:
  a 'xor' a = O_el(Y)
proof
  thus a 'xor' a =('not' a '&' a) 'or' (a '&' 'not' a) by BVFUNC_4:9
    .=O_el(Y) by BVFUNC_4:5;
end;

theorem Th14:
  a 'xor' 'not' a = I_el(Y)
proof
  thus a 'xor' 'not' a =('not' a '&' 'not' a) 'or' (a '&' 'not' 'not' a) by
BVFUNC_4:9
    .=I_el(Y) by BVFUNC_4:6;
end;

theorem Red1:
  (a 'imp' b) 'imp' (b 'imp' a) = b 'imp' a
proof
  (a 'imp' b) 'imp' (b 'imp' a) =('not' a 'or' b) 'imp' (b 'imp' a) by
BVFUNC_4:8
    .=('not' a 'or' b) 'imp' ('not' b 'or' a) by BVFUNC_4:8
    .='not' ('not' a 'or' b) 'or' ('not' b 'or' a) by BVFUNC_4:8
    .=('not' 'not' a '&' 'not' b) 'or' ('not' b 'or' a) by BVFUNC_1:13
    .=((a '&' 'not' b) 'or' 'not' b) 'or' a by BVFUNC_1:8
    .=((a 'or' 'not' b) '&' ('not' b 'or' 'not' b)) 'or' a by BVFUNC_1:11
    .=((a 'or' 'not' b) 'or' a) '&' ('not' b 'or' a) by BVFUNC_1:11
    .=('not' b 'or' (a 'or' a)) '&' ('not' b 'or' a) by BVFUNC_1:8
    .=('not' b 'or' a);
  hence thesis by BVFUNC_4:8;
end;

registration let Y,a,b;
  reduce (a 'imp' b) 'imp' (b 'imp' a) to b 'imp' a;
  reducibility by Red1;
end;

theorem Th15:
  (a 'or' b) '&' ('not' a 'or' 'not' b) = ('not' a '&' b) 'or' (a '&' 'not' b)
proof
  a 'xor' b = ('not' a '&' b) 'or' (a '&' 'not' b) by BVFUNC_4:9;
  hence thesis by BVFUNC_6:86;
end;

theorem Th16:
  (a '&' b) 'or' ('not' a '&' 'not' b) = ('not' a 'or' b) '&' (a 'or' 'not' b)
proof
  thus (a '&' b) 'or' ('not' a '&' 'not' b) =('not' a 'or' b) '&' ('not' 'not'
  a 'or' 'not' b) by Th15
    .=('not' a 'or' b) '&' (a 'or' 'not' b);
end;

theorem
  a 'xor' (b 'xor' c) = (a 'xor' b) 'xor' c
proof
A1: (a 'xor' b) 'xor' c =(('not' a '&' b) 'or' (a '&' 'not' b)) 'xor' c by
BVFUNC_4:9
    .=('not' (('not' a '&' b) 'or' (a '&' 'not' b)) '&' c) 'or' ((('not' a
  '&' b) 'or' (a '&' 'not' b)) '&' 'not' c) by BVFUNC_4:9
    .=(('not' ('not' a '&' b) '&' 'not' (a '&' 'not' b)) '&' c) 'or' (((
  'not' a '&' b) 'or' (a '&' 'not' b)) '&' 'not' c) by BVFUNC_1:13
    .=((('not' 'not' a 'or' 'not' b) '&' 'not' (a '&' 'not' b)) '&' c) 'or'
  ((('not' a '&' b) 'or' (a '&' 'not' b)) '&' 'not' c) by BVFUNC_1:14
    .=(((a 'or' 'not' b) '&' ('not' a 'or' 'not' 'not' b)) '&' c) 'or' (((
  'not' a '&' b) 'or' (a '&' 'not' b)) '&' 'not' c) by BVFUNC_1:14
    .=(((a 'or' 'not' b) '&' ('not' a 'or' b)) '&' c) 'or' (('not' a '&' b
  '&' 'not' c) 'or' (a '&' 'not' b '&' 'not' c)) by BVFUNC_1:12
    .=(((a '&' b) 'or' ('not' a '&' 'not' b)) '&' c) 'or' (('not' a '&' b
  '&' 'not' c) 'or' (a '&' 'not' b '&' 'not' c)) by Th16
    .=((a '&' b '&' c) 'or' ('not' a '&' 'not' b '&' c)) 'or' (('not' a '&'
  b '&' 'not' c) 'or' (a '&' 'not' b '&' 'not' c)) by BVFUNC_1:12
    .=(a '&' b '&' c) 'or' ((a '&' 'not' b '&' 'not' c) 'or' ('not' a '&' b
  '&' 'not' c)) 'or' ('not' a '&' 'not' b '&' c) by BVFUNC_1:8
    .=(a '&' b '&' c) 'or' (a '&' 'not' b '&' 'not' c) 'or' ('not' a '&' b
  '&' 'not' c) 'or' ('not' a '&' 'not' b '&' c) by BVFUNC_1:8;
  a 'xor' (b 'xor' c) =('not' a '&' (b 'xor' c)) 'or' (a '&' 'not' (b
  'xor' c)) by BVFUNC_4:9
    .=('not' a '&' (('not' b '&' c) 'or' (b '&' 'not' c))) 'or' (a '&' 'not'
  (b 'xor' c)) by BVFUNC_4:9
    .=('not' a '&' (('not' b '&' c) 'or' (b '&' 'not' c))) 'or' (a '&' 'not'
  (('not' b '&' c) 'or' (b '&' 'not' c))) by BVFUNC_4:9
    .=(('not' a '&' ('not' b '&' c)) 'or' ('not' a '&' (b '&' 'not' c)))
  'or' (a '&' 'not' (('not' b '&' c) 'or' (b '&' 'not' c))) by BVFUNC_1:12
    .=(('not' a '&' ('not' b '&' c)) 'or' ('not' a '&' (b '&' 'not' c)))
'or' (a '&' (('not' ('not' b '&' c)) '&' ('not' (b '&' 'not' c)))) by
BVFUNC_1:13
    .=(('not' a '&' ('not' b '&' c)) 'or' ('not' a '&' (b '&' 'not' c)))
  'or' (a '&' ((('not' 'not' b 'or' 'not' c)) '&' ('not' (b '&' 'not' c)))) by
BVFUNC_1:14
    .=(('not' a '&' ('not' b '&' c)) 'or' ('not' a '&' (b '&' 'not' c)))
'or' (a '&' ((b 'or' 'not' c) '&' (('not' b 'or' 'not' 'not' c)))) by
BVFUNC_1:14
    .=(('not' a '&' ('not' b '&' c)) 'or' ('not' a '&' (b '&' 'not' c)))
  'or' (a '&' ((b '&' c) 'or' ('not' b '&' 'not' c))) by Th16
    .=(('not' a '&' ('not' b '&' c)) 'or' ('not' a '&' (b '&' 'not' c)))
  'or' ((a '&' (b '&' c)) 'or' (a '&' ('not' b '&' 'not' c))) by BVFUNC_1:12
    .=(('not' a '&' 'not' b '&' c) 'or' ('not' a '&' (b '&' 'not' c))) 'or'
  ((a '&' (b '&' c)) 'or' (a '&' ('not' b '&' 'not' c))) by BVFUNC_1:4
    .=(('not' a '&' 'not' b '&' c) 'or' ('not' a '&' b '&' 'not' c)) 'or' ((
  a '&' (b '&' c)) 'or' (a '&' ('not' b '&' 'not' c))) by BVFUNC_1:4
    .=(('not' a '&' 'not' b '&' c) 'or' ('not' a '&' b '&' 'not' c)) 'or' ((
  a '&' b '&' c) 'or' (a '&' ('not' b '&' 'not' c))) by BVFUNC_1:4
    .=((a '&' b '&' c) 'or' (a '&' 'not' b '&' 'not' c)) 'or' (('not' a '&'
  b '&' 'not' c) 'or' ('not' a '&' 'not' b '&' c)) by BVFUNC_1:4
    .=(a '&' b '&' c) 'or' (a '&' 'not' b '&' 'not' c) 'or' ('not' a '&' b
  '&' 'not' c) 'or' ('not' a '&' 'not' b '&' c) by BVFUNC_1:8;
  hence thesis by A1;
end;

theorem
  a 'eqv' (b 'eqv' c) = (a 'eqv' b) 'eqv' c
proof
A1: (a 'eqv' b) 'eqv' c =((a 'eqv' b) 'imp' c) '&' (c 'imp' (a 'eqv' b)) by
BVFUNC_4:7
    .=(((a 'imp' b) '&' (b 'imp' a)) 'imp' c) '&' (c 'imp' (a 'eqv' b)) by
BVFUNC_4:7
    .=(((a 'imp' b) '&' (b 'imp' a)) 'imp' c) '&' (c 'imp' ((a 'imp' b) '&'
  (b 'imp' a))) by BVFUNC_4:7
    .=((('not' a 'or' b) '&' (b 'imp' a)) 'imp' c) '&' (c 'imp' ((a 'imp' b)
  '&' (b 'imp' a))) by BVFUNC_4:8
    .=((('not' a 'or' b) '&' ('not' b 'or' a)) 'imp' c) '&' (c 'imp' ((a
  'imp' b) '&' (b 'imp' a))) by BVFUNC_4:8
    .=('not' (('not' a 'or' b) '&' ('not' b 'or' a)) 'or' c) '&' (c 'imp' ((
  a 'imp' b) '&' (b 'imp' a))) by BVFUNC_4:8
    .=('not' (('not' a 'or' b) '&' ('not' b 'or' a)) 'or' c) '&' ('not' c
  'or' ((a 'imp' b) '&' (b 'imp' a))) by BVFUNC_4:8
    .=('not' (('not' a 'or' b) '&' ('not' b 'or' a)) 'or' c) '&' ('not' c
  'or' (('not' a 'or' b) '&' (b 'imp' a))) by BVFUNC_4:8
    .=('not' (('not' a 'or' b) '&' ('not' b 'or' a)) 'or' c) '&' ('not' c
  'or' (('not' a 'or' b) '&' ('not' b 'or' a))) by BVFUNC_4:8
    .=(('not' ('not' a 'or' b) 'or' 'not' ('not' b 'or' a)) 'or' c) '&' (
  'not' c 'or' (('not' a 'or' b) '&' ('not' b 'or' a))) by BVFUNC_1:14
    .=((('not' 'not' a '&' 'not' b) 'or' 'not' ('not' b 'or' a)) 'or' c) '&'
  ('not' c 'or' (('not' a 'or' b) '&' ('not' b 'or' a))) by BVFUNC_1:13
    .=(((a '&' 'not' b) 'or' ('not' 'not' b '&' 'not' a)) 'or' c) '&' ('not'
  c 'or' (('not' a 'or' b) '&' ('not' b 'or' a))) by BVFUNC_1:13
    .=(((a 'or' b) '&' ('not' a 'or' 'not' b)) 'or' c) '&' ('not' c 'or' ((
  'not' a 'or' b) '&' ('not' b 'or' a))) by Th15
    .=(((a 'or' b) 'or' c) '&' (('not' a 'or' 'not' b) 'or' c)) '&' ('not' c
  'or' (('not' a 'or' b) '&' ('not' b 'or' a))) by BVFUNC_1:11
    .=((a 'or' b 'or' c) '&' ('not' a 'or' 'not' b 'or' c)) '&' ((a 'or'
  'not' b 'or' 'not' c) '&' ('not' a 'or' b 'or' 'not' c)) by BVFUNC_1:11
    .=(a 'or' b 'or' c) '&' ((a 'or' 'not' b 'or' 'not' c) '&' ('not' a 'or'
  b 'or' 'not' c)) '&' ('not' a 'or' 'not' b 'or' c) by BVFUNC_1:4
    .=(a 'or' b 'or' c) '&' (a 'or' 'not' b 'or' 'not' c) '&' ('not' a 'or'
  b 'or' 'not' c) '&' ('not' a 'or' 'not' b 'or' c) by BVFUNC_1:4;
  a 'eqv' (b 'eqv' c) =(a 'imp' (b 'eqv' c)) '&' ((b 'eqv' c) 'imp' a) by
BVFUNC_4:7
    .=(a 'imp' ((b 'imp' c) '&' (c 'imp' b))) '&' ((b 'eqv' c) 'imp' a) by
BVFUNC_4:7
    .=(a 'imp' ((b 'imp' c) '&' (c 'imp' b))) '&' (((b 'imp' c) '&' (c 'imp'
  b)) 'imp' a) by BVFUNC_4:7
    .=('not' a 'or' ((b 'imp' c) '&' (c 'imp' b))) '&' (((b 'imp' c) '&' (c
  'imp' b)) 'imp' a) by BVFUNC_4:8
    .=('not' a 'or' (('not' b 'or' c) '&' (c 'imp' b))) '&' (((b 'imp' c)
  '&' (c 'imp' b)) 'imp' a) by BVFUNC_4:8
    .=('not' a 'or' (('not' b 'or' c) '&' ('not' c 'or' b))) '&' (((b 'imp'
  c) '&' (c 'imp' b)) 'imp' a) by BVFUNC_4:8
    .=('not' a 'or' (('not' b 'or' c) '&' ('not' c 'or' b))) '&' ((('not' b
  'or' c) '&' (c 'imp' b)) 'imp' a) by BVFUNC_4:8
    .=('not' a 'or' (('not' b 'or' c) '&' ('not' c 'or' b))) '&' ((('not' b
  'or' c) '&' ('not' c 'or' b)) 'imp' a) by BVFUNC_4:8
    .=('not' a 'or' (('not' b 'or' c) '&' ('not' c 'or' b))) '&' ('not' ((
  'not' b 'or' c) '&' ('not' c 'or' b)) 'or' a) by BVFUNC_4:8
    .=('not' a 'or' (('not' b 'or' c) '&' ('not' c 'or' b))) '&' (('not' (
  'not' b 'or' c)) 'or' ('not' ('not' c 'or' b)) 'or' a) by BVFUNC_1:14
    .=('not' a 'or' (('not' b 'or' c) '&' ('not' c 'or' b))) '&' ((('not'
  'not' b '&' 'not' c)) 'or' ('not' ('not' c 'or' b)) 'or' a) by BVFUNC_1:13
    .=('not' a 'or' (('not' b 'or' c) '&' ('not' c 'or' b))) '&' (((b '&'
  'not' c)) 'or' (('not' 'not' c '&' 'not' b)) 'or' a) by BVFUNC_1:13
    .=('not' a 'or' (('not' b 'or' c) '&' ('not' c 'or' b))) '&' (((b 'or' c
  ) '&' ('not' b 'or' 'not' c)) 'or' a) by Th15
    .=(('not' a 'or' ('not' b 'or' c)) '&' ('not' a 'or' ('not' c 'or' b)))
  '&' (((b 'or' c) '&' ('not' b 'or' 'not' c)) 'or' a) by BVFUNC_1:11
    .=(('not' a 'or' 'not' b 'or' c) '&' ('not' a 'or' (b 'or' 'not' c)))
  '&' (((b 'or' c) '&' ('not' b 'or' 'not' c)) 'or' a) by BVFUNC_1:8
    .=(('not' a 'or' 'not' b 'or' c) '&' ('not' a 'or' b 'or' 'not' c)) '&'
  (((b 'or' c) '&' ('not' b 'or' 'not' c)) 'or' a) by BVFUNC_1:8
    .=(('not' a 'or' 'not' b 'or' c) '&' ('not' a 'or' b 'or' 'not' c)) '&'
  ((a 'or' (b 'or' c)) '&' (a 'or' ('not' b 'or' 'not' c))) by BVFUNC_1:11
    .=(('not' a 'or' 'not' b 'or' c) '&' ('not' a 'or' b 'or' 'not' c)) '&'
  ((a 'or' b 'or' c) '&' (a 'or' ('not' b 'or' 'not' c))) by BVFUNC_1:8
    .=(('not' a 'or' 'not' b 'or' c) '&' ('not' a 'or' b 'or' 'not' c)) '&'
  ((a 'or' b 'or' c) '&' (a 'or' 'not' b 'or' 'not' c)) by BVFUNC_1:8
    .=((a 'or' b 'or' c) '&' (a 'or' 'not' b 'or' 'not' c)) '&' ('not' a
  'or' b 'or' 'not' c) '&' ('not' a 'or' 'not' b 'or' c) by BVFUNC_1:4;
  hence thesis by A1;
end;

theorem
  'not' 'not' a 'imp' a = I_el(Y) by BVFUNC_5:7;

theorem
  ((a 'imp' b) '&' a) 'imp' b = I_el(Y)
proof
  ((a 'imp' b) '&' a) 'imp' b = (a '&' b) 'imp' b by BVFUNC_6:56;
  hence thesis by BVFUNC_6:40;
end;

theorem Th21:
  a 'imp' ('not' a 'imp' a) = I_el(Y)
proof
  a 'imp' ('not' a 'imp' a) ='not' a 'or' ('not' a 'imp' a) by BVFUNC_4:8
    .='not' a 'or' ('not' 'not' a 'or' a) by BVFUNC_4:8
    .='not' a 'or' a;
  hence thesis by BVFUNC_4:6;
end;

theorem
  ('not' a 'imp' a) 'eqv' a = I_el(Y)
proof
  ('not' a 'imp' a) 'eqv' a = (('not' a 'imp' a) 'imp' a) '&' (a 'imp' (
  'not' a 'imp' a)) by BVFUNC_4:7
    .= I_el(Y) '&' (a 'imp' ('not' a 'imp' a)) by BVFUNC_5:11
    .= (a 'imp' ('not' a 'imp' a)) by BVFUNC_1:6;
  hence thesis by Th21;
end;

theorem
  a 'or' (a 'imp' b) = I_el(Y)
proof
  a 'or' (a 'imp' b) =a 'or' ('not' a 'or' b) by BVFUNC_4:8
    .=(a 'or' 'not' a) 'or' b by BVFUNC_1:8
    .=I_el(Y) 'or' b by BVFUNC_4:6;
  hence thesis by BVFUNC_1:10;
end;

theorem
  (a 'imp' b) 'or' (c 'imp' a) = I_el(Y)
proof
  (a 'imp' b) 'or' (c 'imp' a) =('not' a 'or' b) 'or' (c 'imp' a) by BVFUNC_4:8
    .=('not' a 'or' b) 'or' ('not' c 'or' a) by BVFUNC_4:8
    .='not' c 'or' (a 'or' ('not' a 'or' b)) by BVFUNC_1:8
    .='not' c 'or' ((a 'or' 'not' a) 'or' b) by BVFUNC_1:8
    .='not' c 'or' (I_el(Y) 'or' b) by BVFUNC_4:6
    .='not' c 'or' I_el(Y) by BVFUNC_1:10;
  hence thesis by BVFUNC_1:10;
end;

theorem
  (a 'imp' b) 'or' ('not' a 'imp' b) = I_el(Y)
proof
  (a 'imp' b) 'or' ('not' a 'imp' b) =('not' a 'or' b) 'or' ('not' a 'imp'
  b) by BVFUNC_4:8
    .=('not' a 'or' b) 'or' ('not' 'not' a 'or' b) by BVFUNC_4:8
    .=b 'or' ('not' a 'or' (a 'or' b)) by BVFUNC_1:8
    .=b 'or' (('not' a 'or' a) 'or' b) by BVFUNC_1:8
    .=b 'or' (I_el(Y) 'or' b) by BVFUNC_4:6
    .=b 'or' I_el(Y) by BVFUNC_1:10;
  hence thesis by BVFUNC_1:10;
end;

theorem
  (a 'imp' b) 'or' (a 'imp' 'not' b) = I_el(Y)
proof
  (a 'imp' b) 'or' (a 'imp' 'not' b) =('not' a 'or' b) 'or' (a 'imp' 'not'
  b) by BVFUNC_4:8
    .=('not' a 'or' b) 'or' ('not' a 'or' 'not' b) by BVFUNC_4:8
    .='not' a 'or' (b 'or' ('not' b 'or' 'not' a)) by BVFUNC_1:8
    .='not' a 'or' ((b 'or' 'not' b) 'or' 'not' a) by BVFUNC_1:8
    .='not' a 'or' (I_el(Y) 'or' 'not' a) by BVFUNC_4:6
    .='not' a 'or' I_el(Y) by BVFUNC_1:10;
  hence thesis by BVFUNC_1:10;
end;

theorem
  'not' a 'imp' ('not' b 'eqv' (b 'imp' a)) = I_el(Y)
proof
  'not' a 'imp' ('not' b 'eqv' (b 'imp' a)) ='not' 'not' a 'or' ('not' b
  'eqv' (b 'imp' a)) by BVFUNC_4:8
    .=a 'or' (('not' b 'imp' (b 'imp' a)) '&' ((b 'imp' a) 'imp' 'not' b))
  by BVFUNC_4:7
    .=a 'or' (('not' 'not' b 'or' (b 'imp' a)) '&' ((b 'imp' a) 'imp' 'not'
  b)) by BVFUNC_4:8
    .=a 'or' ((b 'or' ('not' b 'or' a)) '&' ((b 'imp' a) 'imp' 'not' b)) by
BVFUNC_4:8
    .=a 'or' (((b 'or' 'not' b) 'or' a) '&' ((b 'imp' a) 'imp' 'not' b)) by
BVFUNC_1:8
    .=a 'or' ((I_el(Y) 'or' a) '&' ((b 'imp' a) 'imp' 'not' b)) by BVFUNC_4:6
    .=a 'or' (I_el(Y) '&' ((b 'imp' a) 'imp' 'not' b)) by BVFUNC_1:10
    .=a 'or' ((b 'imp' a) 'imp' 'not' b) by BVFUNC_1:6
    .=a 'or' (('not' b 'or' a) 'imp' 'not' b) by BVFUNC_4:8
    .=a 'or' ('not' ('not' b 'or' a) 'or' 'not' b) by BVFUNC_4:8
    .=a 'or' (('not' 'not' b '&' 'not' a) 'or' 'not' b) by BVFUNC_1:13
    .=a 'or' ((b 'or' 'not' b) '&' ('not' a 'or' 'not' b)) by BVFUNC_1:11
    .=a 'or' (I_el(Y) '&' ('not' a 'or' 'not' b)) by BVFUNC_4:6
    .=a 'or' ('not' a 'or' 'not' b) by BVFUNC_1:6
    .=(a 'or' 'not' a) 'or' 'not' b by BVFUNC_1:8
    .=I_el(Y) 'or' 'not' b by BVFUNC_4:6;
  hence thesis by BVFUNC_1:10;
end;

theorem
  (a 'imp' b) 'imp' (((a 'imp' c) 'imp' b) 'imp' b) = I_el(Y)
proof
  (a 'imp' b) 'imp' (((a 'imp' c) 'imp' b) 'imp' b) ='not' (a 'imp' b)
  'or' (((a 'imp' c) 'imp' b) 'imp' b) by BVFUNC_4:8
    .='not' ('not' a 'or' b) 'or' (((a 'imp' c) 'imp' b) 'imp' b) by BVFUNC_4:8
    .=('not' 'not' a '&' 'not' b) 'or' (((a 'imp' c) 'imp' b) 'imp' b) by
BVFUNC_1:13
    .=(a '&' 'not' b) 'or' ('not' ((a 'imp' c) 'imp' b) 'or' b) by BVFUNC_4:8
    .=(a '&' 'not' b) 'or' ('not' (('not' a 'or' c) 'imp' b) 'or' b) by
BVFUNC_4:8
    .=(a '&' 'not' b) 'or' ('not' ('not' ('not' a 'or' c) 'or' b) 'or' b) by
BVFUNC_4:8
    .=(a '&' 'not' b) 'or' ('not' (('not' 'not' a '&' 'not' c) 'or' b) 'or'
  b) by BVFUNC_1:13
    .=(a '&' 'not' b) 'or' (('not' (a '&' 'not' c) '&' 'not' b) 'or' b) by
BVFUNC_1:13
    .=(a '&' 'not' b) 'or' ((('not' a 'or' 'not' 'not' c) '&' 'not' b) 'or'
  b) by BVFUNC_1:14
    .=(a '&' 'not' b) 'or' ((('not' a 'or' c) 'or' b) '&' ('not' b 'or' b))
  by BVFUNC_1:11
    .=(a '&' 'not' b) 'or' ((('not' a 'or' c) 'or' b) '&' I_el(Y)) by
BVFUNC_4:6
    .=(a '&' 'not' b) 'or' (('not' a 'or' c) 'or' b) by BVFUNC_1:6
    .=((a '&' 'not' b) 'or' b) 'or' ('not' a 'or' c) by BVFUNC_1:8
    .=((a 'or' b) '&' ('not' b 'or' b)) 'or' ('not' a 'or' c) by BVFUNC_1:11
    .=((a 'or' b) '&' I_el(Y)) 'or' ('not' a 'or' c) by BVFUNC_4:6
    .=(a 'or' b) 'or' ('not' a 'or' c) by BVFUNC_1:6
    .=b 'or' (a 'or' ('not' a 'or' c)) by BVFUNC_1:8
    .=b 'or' ((a 'or' 'not' a) 'or' c) by BVFUNC_1:8
    .=b 'or' (I_el(Y) 'or' c) by BVFUNC_4:6
    .=b 'or' I_el(Y) by BVFUNC_1:10;
  hence thesis by BVFUNC_1:10;
end;

theorem
  a 'imp' b = a 'eqv' (a '&' b)
proof
  a 'eqv' (a '&' b) =(a 'imp' (a '&' b)) '&' ((a '&' b) 'imp' a) by BVFUNC_4:7
    .=('not' a 'or' (a '&' b)) '&' ((a '&' b) 'imp' a) by BVFUNC_4:8
    .=('not' a 'or' (a '&' b)) '&' ('not' (a '&' b) 'or' a) by BVFUNC_4:8
    .=(('not' a 'or' a) '&' ('not' a 'or' b)) '&' ('not' (a '&' b) 'or' a)
  by BVFUNC_1:11
    .=(I_el(Y) '&' ('not' a 'or' b)) '&' ('not' (a '&' b) 'or' a) by BVFUNC_4:6
    .=('not' a 'or' b) '&' ('not' (a '&' b) 'or' a) by BVFUNC_1:6
    .=('not' a 'or' b) '&' (('not' a 'or' 'not' b) 'or' a) by BVFUNC_1:14
    .=('not' a 'or' b) '&' ('not' b 'or' ('not' a 'or' a)) by BVFUNC_1:8
    .=('not' a 'or' b) '&' ('not' b 'or' I_el(Y)) by BVFUNC_4:6
    .=('not' a 'or' b) '&' I_el(Y) by BVFUNC_1:10
    .='not' a 'or' b by BVFUNC_1:6;
  hence thesis by BVFUNC_4:8;
end;

theorem
  a 'imp' b=I_el(Y) & b 'imp' a=I_el(Y) iff a=b
proof
  (a 'eqv' b)=I_el(Y) iff (a 'imp' b)=I_el(Y) & (b 'imp' a)=I_el(Y) by
BVFUNC_4:10;
  hence thesis by BVFUNC_1:17;
end;

theorem
  a = 'not' a 'imp' a
proof
  ('not' a 'imp' a) 'imp' a = I_el(Y) by BVFUNC_5:11;
  then
A1: ('not' a 'imp' a) '<' a by BVFUNC_1:16;
  a 'imp' ('not' a 'imp' a) = I_el(Y) by Th21;
  then a '<' ('not' a 'imp' a) by BVFUNC_1:16;
  hence thesis by A1,BVFUNC_1:15;
end;

theorem Th32:
  a 'imp' ((a 'imp' b) 'imp' a) = I_el(Y)
proof
  thus a 'imp' ((a 'imp' b) 'imp' a) ='not' a 'or' ((a 'imp' b) 'imp' a) by
BVFUNC_4:8
    .='not' a 'or' ('not' (a 'imp' b) 'or' a) by BVFUNC_4:8
    .='not' a 'or' ('not' ('not' a 'or' b) 'or' a) by BVFUNC_4:8
    .='not' a 'or' (('not' 'not' a '&' 'not' b) 'or' a) by BVFUNC_1:13
    .=('not' a 'or' a) 'or' (a '&' 'not' b) by BVFUNC_1:8
    .=I_el(Y) 'or' (a '&' 'not' b) by BVFUNC_4:6
    .=I_el(Y) by BVFUNC_1:10;
end;

theorem
  a = (a 'imp' b) 'imp' a
proof
  ((a 'imp' b) 'imp' a) 'imp' a = I_el(Y) by BVFUNC_6:100;
  then
A1: ((a 'imp' b) 'imp' a) '<' a by BVFUNC_1:16;
  a 'imp' ((a 'imp' b) 'imp' a) = I_el(Y) by Th32;
  then a '<' ((a 'imp' b) 'imp' a) by BVFUNC_1:16;
  hence thesis by A1,BVFUNC_1:15;
end;

theorem
  a = (b 'imp' a) '&' ('not' b 'imp' a)
proof
  a=(a 'or' b) '&' (a 'or' 'not' b) by BVFUNC_6:80
    .=(a 'or' 'not' 'not' b) '&' (b 'imp' a) by BVFUNC_4:8
    .=('not' b 'imp' a) '&' (b 'imp' a) by BVFUNC_4:8;
  hence thesis;
end;

theorem
  a '&' b = 'not' (a 'imp' 'not' b)
proof
  'not'( a 'imp' 'not' b) 'imp' (a '&' b)=I_el(Y) by BVFUNC_6:35;
  then
A1: 'not'( a 'imp' 'not' b) '<' (a '&' b) by BVFUNC_1:16;
  (a '&' b) 'imp' 'not'( a 'imp' 'not' b)=I_el(Y) by BVFUNC_6:34;
  then (a '&' b) '<' 'not'( a 'imp' 'not' b) by BVFUNC_1:16;
  hence thesis by A1,BVFUNC_1:15;
end;

theorem
  a 'or' b = 'not' a 'imp' b
proof
  thus 'not' a 'imp' b ='not' 'not' a 'or' b by BVFUNC_4:8
    .=a 'or' b;
end;

theorem
  a 'or' b = (a 'imp' b) 'imp' b
proof
  thus (a 'imp' b) 'imp' b ='not' (a 'imp' b) 'or' b by BVFUNC_4:8
    .='not' ('not' a 'or' b) 'or' b by BVFUNC_4:8
    .=('not' 'not' a '&' 'not' b) 'or' b by BVFUNC_1:13
    .=(a 'or' b) '&' ('not' b 'or' b) by BVFUNC_1:11
    .=(a 'or' b) '&' I_el(Y) by BVFUNC_4:6
    .= a 'or' b by BVFUNC_1:6;
end;

theorem
  (a 'imp' b) 'imp' (a 'imp' a) = I_el(Y)
proof
  thus (a 'imp' b) 'imp' (a 'imp' a)=(a 'imp' b) 'imp' I_el(Y) by BVFUNC_5:7
    .=I_el(Y) by BVFUNC_6:62;
end;

theorem
  (a 'imp' (b 'imp' c)) 'imp' ((d 'imp' b) 'imp' (a 'imp' (d 'imp' c)))
  = I_el ( Y )
proof
  thus (a 'imp' (b 'imp' c)) 'imp' ((d 'imp' b) 'imp' (a 'imp' (d 'imp' c))) =
  'not' (a 'imp' (b 'imp' c)) 'or' ((d 'imp' b) 'imp' (a 'imp' (d 'imp' c)))
by BVFUNC_4:8
    .='not' ('not' a 'or' (b 'imp' c)) 'or' ((d 'imp' b) 'imp' (a 'imp' (d
  'imp' c))) by BVFUNC_4:8
    .='not' ('not' a 'or' ('not' b 'or' c)) 'or' ((d 'imp' b) 'imp' (a 'imp'
  (d 'imp' c))) by BVFUNC_4:8
    .='not' ('not' a 'or' ('not' b 'or' c)) 'or' ('not' (d 'imp' b) 'or' (a
  'imp' (d 'imp' c))) by BVFUNC_4:8
    .='not' ('not' a 'or' ('not' b 'or' c)) 'or' ('not' ('not' d 'or' b)
  'or' (a 'imp' (d 'imp' c))) by BVFUNC_4:8
    .='not' ('not' a 'or' ('not' b 'or' c)) 'or' ('not' ('not' d 'or' b)
  'or' ('not' a 'or' (d 'imp' c))) by BVFUNC_4:8
    .='not' ('not' a 'or' ('not' b 'or' c)) 'or' ('not' ('not' d 'or' b)
  'or' ('not' a 'or' ('not' d 'or' c))) by BVFUNC_4:8
    .=('not' 'not' a '&' 'not' ('not' b 'or' c)) 'or' ('not' ('not' d 'or' b
  ) 'or' ('not' a 'or' ('not' d 'or' c))) by BVFUNC_1:13
    .=('not' 'not' a '&' ('not' 'not' b '&' 'not' c)) 'or' ('not' ('not' d
  'or' b) 'or' ('not' a 'or' ('not' d 'or' c))) by BVFUNC_1:13
    .=(a '&' ('not' 'not' b '&' 'not' c)) 'or' (('not' 'not' d '&' 'not' b)
  'or' ('not' a 'or' ('not' d 'or' c))) by BVFUNC_1:13
    .=(a '&' (b '&' 'not' c)) 'or' (((d '&' 'not' b) 'or' 'not' a) 'or' (
  'not' d 'or' c)) by BVFUNC_1:8
    .=((a '&' (b '&' 'not' c)) 'or' ('not' a 'or' (d '&' 'not' b))) 'or' (
  'not' d 'or' c) by BVFUNC_1:8
    .=(((a '&' (b '&' 'not' c)) 'or' 'not' a) 'or' (d '&' 'not' b)) 'or' (
  'not' d 'or' c) by BVFUNC_1:8
    .=(((a 'or' 'not' a) '&' ((b '&' 'not' c) 'or' 'not' a)) 'or' (d '&'
  'not' b)) 'or' ('not' d 'or' c) by BVFUNC_1:11
    .=((I_el(Y) '&' ((b '&' 'not' c) 'or' 'not' a)) 'or' (d '&' 'not' b))
  'or' ('not' d 'or' c) by BVFUNC_4:6
    .=(((b '&' 'not' c) 'or' 'not' a) 'or' (d '&' 'not' b)) 'or' ('not' d
  'or' c) by BVFUNC_1:6
    .=((b '&' 'not' c) 'or' 'not' a) 'or' ((d '&' 'not' b) 'or' ('not' d
  'or' c)) by BVFUNC_1:8
    .=((b '&' 'not' c) 'or' 'not' a) 'or' ((('not' b '&' d) 'or' 'not' d)
  'or' c) by BVFUNC_1:8
    .=((b '&' 'not' c) 'or' 'not' a) 'or' ((('not' b 'or' 'not' d) '&' (d
  'or' 'not' d)) 'or' c) by BVFUNC_1:11
    .=((b '&' 'not' c) 'or' 'not' a) 'or' ((('not' b 'or' 'not' d) '&' I_el(
  Y)) 'or' c) by BVFUNC_4:6
    .=((b '&' 'not' c) 'or' 'not' a) 'or' (('not' b 'or' 'not' d) 'or' c) by
BVFUNC_1:6
    .='not' a 'or' (('not' c '&' b) 'or' (('not' b 'or' 'not' d) 'or' c)) by
BVFUNC_1:8
    .='not' a 'or' ((('not' c '&' b) 'or' ('not' b 'or' 'not' d)) 'or' c) by
BVFUNC_1:8
    .='not' a 'or' (((('not' c '&' b) 'or' 'not' b) 'or' 'not' d) 'or' c) by
BVFUNC_1:8
    .='not' a 'or' (((('not' c 'or' 'not' b) '&' (b 'or' 'not' b)) 'or'
  'not' d) 'or' c) by BVFUNC_1:11
    .='not' a 'or' (((('not' c 'or' 'not' b) '&' I_el(Y)) 'or' 'not' d) 'or'
  c) by BVFUNC_4:6
    .='not' a 'or' ((('not' b 'or' 'not' c) 'or' 'not' d) 'or' c) by BVFUNC_1:6
    .='not' a 'or' (('not' b 'or' ('not' c 'or' 'not' d)) 'or' c) by BVFUNC_1:8
    .='not' a 'or' ('not' b 'or' (('not' d 'or' 'not' c) 'or' c)) by BVFUNC_1:8
    .='not' a 'or' ('not' b 'or' ('not' d 'or' ('not' c 'or' c))) by BVFUNC_1:8
    .='not' a 'or' ('not' b 'or' ('not' d 'or' I_el(Y))) by BVFUNC_4:6
    .='not' a 'or' ('not' b 'or' I_el(Y)) by BVFUNC_1:10
    .='not' a 'or' I_el(Y) by BVFUNC_1:10
    .=I_el(Y) by BVFUNC_1:10;
end;

theorem
  (((a 'imp' b) '&' a) '&' c) 'imp' b = I_el(Y)
proof
  thus (((a 'imp' b) '&' a) '&' c) 'imp' b =((('not' a 'or' b) '&' a) '&' c)
  'imp' b by BVFUNC_4:8
    .=((('not' a '&' a) 'or' (b '&' a)) '&' c) 'imp' b by BVFUNC_1:12
    .=((O_el(Y) 'or' (b '&' a)) '&' c) 'imp' b by BVFUNC_4:5
    .=((b '&' a) '&' c) 'imp' b by BVFUNC_1:9
    .='not' ((b '&' a) '&' c) 'or' b by BVFUNC_4:8
    .=('not' (b '&' a) 'or' 'not' c) 'or' b by BVFUNC_1:14
    .=(('not' b 'or' 'not' a) 'or' 'not' c) 'or' b by BVFUNC_1:14
    .=(b 'or' ('not' b 'or' 'not' a)) 'or' 'not' c by BVFUNC_1:8
    .=((b 'or' 'not' b) 'or' 'not' a) 'or' 'not' c by BVFUNC_1:8
    .=(I_el(Y) 'or' 'not' a) 'or' 'not' c by BVFUNC_4:6
    .=I_el(Y) 'or' 'not' c by BVFUNC_1:10
    .=I_el(Y)by BVFUNC_1:10;
end;

theorem
  (b 'imp' c) 'imp' ((a '&' b) 'imp' c) = I_el(Y)
proof
  thus (b 'imp' c) 'imp' ((a '&' b) 'imp' c) ='not' (b 'imp' c) 'or' ((a '&' b
  ) 'imp' c) by BVFUNC_4:8
    .='not' ('not' b 'or' c) 'or' ((a '&' b) 'imp' c) by BVFUNC_4:8
    .='not' ('not' b 'or' c) 'or' ('not' (a '&' b) 'or' c) by BVFUNC_4:8
    .=('not' 'not' b '&' 'not' c) 'or' ('not' (a '&' b) 'or' c) by BVFUNC_1:13
    .=(b '&' 'not' c) 'or' (('not' a 'or' 'not' b) 'or' c) by BVFUNC_1:14
    .=((b '&' 'not' c) 'or' c) 'or' ('not' a 'or' 'not' b) by BVFUNC_1:8
    .=((b 'or' c) '&' ('not' c 'or' c)) 'or' ('not' a 'or' 'not' b) by
BVFUNC_1:11
    .=((b 'or' c) '&' I_el(Y)) 'or' ('not' a 'or' 'not' b) by BVFUNC_4:6
    .=('not' a 'or' 'not' b) 'or' (b 'or' c) by BVFUNC_1:6
    .=(('not' a 'or' 'not' b) 'or' b) 'or' c by BVFUNC_1:8
    .=('not' a 'or' ('not' b 'or' b)) 'or' c by BVFUNC_1:8
    .=('not' a 'or' I_el(Y)) 'or' c by BVFUNC_4:6
    .=I_el(Y) 'or' c by BVFUNC_1:10
    .=I_el(Y) by BVFUNC_1:10;
end;

theorem
  ((a '&' b) 'imp' c) 'imp' ((a '&' b) 'imp' (c '&' b)) = I_el(Y)
proof
  ((a '&' b) 'imp' c) 'imp' ((a '&' b) 'imp' (c '&' b)) =('not' (a '&' b)
  'or' c) 'imp' ((a '&' b) 'imp' (c '&' b)) by BVFUNC_4:8
    .='not' ('not' (a '&' b) 'or' c) 'or' ((a '&' b) 'imp' (c '&' b)) by
BVFUNC_4:8
    .='not' ('not' (a '&' b) 'or' c) 'or' ('not' (a '&' b) 'or' (c '&' b))
  by BVFUNC_4:8
    .=('not' 'not' (a '&' b) '&' 'not' c) 'or' ('not' (a '&' b) 'or' (c '&'
  b)) by BVFUNC_1:13
    .=((a '&' b) '&' 'not' c) 'or' (('not' a 'or' 'not' b) 'or' (c '&' b))
  by BVFUNC_1:14
    .=((a '&' b) '&' 'not' c) 'or' ('not' a 'or' ('not' b 'or' (b '&' c)))
  by BVFUNC_1:8
    .=((a '&' b) '&' 'not' c) 'or' ('not' a 'or' (('not' b 'or' b) '&' (
  'not' b 'or' c))) by BVFUNC_1:11
    .=((a '&' b) '&' 'not' c) 'or' ('not' a 'or' (I_el(Y) '&' ('not' b 'or'
  c))) by BVFUNC_4:6
    .=((a '&' b) '&' 'not' c) 'or' ('not' a 'or' ('not' b 'or' c)) by
BVFUNC_1:6
    .=(((a '&' b) '&' 'not' c) 'or' 'not' a) 'or' ('not' b 'or' c) by
BVFUNC_1:8
    .=(((a '&' b) 'or' 'not' a) '&' ('not' c 'or' 'not' a)) 'or' ('not' b
  'or' c) by BVFUNC_1:11
    .=(((a 'or' 'not' a) '&' (b 'or' 'not' a)) '&' ('not' c 'or' 'not' a))
  'or' ('not' b 'or' c) by BVFUNC_1:11
    .=((I_el(Y) '&' (b 'or' 'not' a)) '&' ('not' c 'or' 'not' a)) 'or' (
  'not' b 'or' c) by BVFUNC_4:6
    .=((b 'or' 'not' a) '&' ('not' c 'or' 'not' a)) 'or' ('not' b 'or' c) by
BVFUNC_1:6
    .=(((b 'or' 'not' a) '&' ('not' c 'or' 'not' a)) 'or' c) 'or' 'not' b by
BVFUNC_1:8
    .=(((b 'or' 'not' a) 'or' c) '&' (('not' c 'or' 'not' a) 'or' c)) 'or'
  'not' b by BVFUNC_1:11
    .=(((b 'or' 'not' a) 'or' c) '&' ('not' a 'or' ('not' c 'or' c))) 'or'
  'not' b by BVFUNC_1:8
    .=(((b 'or' 'not' a) 'or' c) '&' ('not' a 'or' I_el(Y))) 'or' 'not' b by
BVFUNC_4:6
    .=(((b 'or' 'not' a) 'or' c) '&' I_el(Y)) 'or' 'not' b by BVFUNC_1:10
    .=((b 'or' 'not' a) 'or' c) 'or' 'not' b by BVFUNC_1:6
    .=('not' b 'or' (b 'or' 'not' a)) 'or' c by BVFUNC_1:8
    .=(('not' b 'or' b) 'or' 'not' a) 'or' c by BVFUNC_1:8
    .=(I_el(Y) 'or' 'not' a) 'or' c by BVFUNC_4:6
    .=I_el(Y) 'or' c by BVFUNC_1:10;
  hence thesis by BVFUNC_1:10;
end;

theorem
  (a 'imp' b) 'imp' ((a '&' c) 'imp' (b '&' c)) = I_el(Y)
   by BVFUNC_1:16,BVFUNC_6:112;

theorem
  (a 'imp' b) '&' (a '&' c) 'imp' (b '&' c) = I_el(Y)
proof
  (a 'imp' b) '&' (a '&' c) 'imp' (b '&' c) =((a 'imp' b) '&' a) '&' c
  'imp' (b '&' c) by BVFUNC_1:4
    .=(a '&' b) '&' c 'imp' (b '&' c) by BVFUNC_6:56
    .=a '&' (b '&' c) 'imp' (b '&' c) by BVFUNC_1:4;
  hence thesis by BVFUNC_6:38;
end;

theorem
  a '&' (a 'imp' b) '&' (b 'imp' c) '<' c
proof
  (a '&' (a 'imp' b) '&' (b 'imp' c)) 'imp' c ='not' (a '&' (a 'imp' b)
  '&' (b 'imp' c)) 'or' c by BVFUNC_4:8
    .='not' (a '&' b '&' (b 'imp' c)) 'or' c by BVFUNC_6:56
    .='not' (a '&' (b '&' (b 'imp' c))) 'or' c by BVFUNC_1:4
    .='not' (a '&' (b '&' c)) 'or' c by BVFUNC_6:56
    .='not' ((a '&' b) '&' c) 'or' c by BVFUNC_1:4
    .=('not' (a '&' b) 'or' 'not' c) 'or' c by BVFUNC_1:14
    .='not' (a '&' b) 'or' ('not' c 'or' c) by BVFUNC_1:8
    .='not' (a '&' b) 'or' I_el(Y) by BVFUNC_4:6
    .= I_el(Y) by BVFUNC_1:10;
  hence thesis by BVFUNC_1:16;
end;

theorem
  (a 'or' b) '&' (a 'imp' c) '&' (b 'imp' c) '<' ('not' a 'imp' (b 'or' c))
proof
  (a 'or' b) '&' (a 'imp' c) '&' (b 'imp' c) 'imp' ('not' a 'imp' (b 'or'
c ) ) ='not' ((a 'or' b) '&' (a 'imp' c) '&' (b 'imp' c)) 'or' ('not' a 'imp' (
  b 'or' c)) by BVFUNC_4:8
    .='not' ((a 'or' b) '&' ('not' a 'or' c) '&' (b 'imp' c)) 'or' ('not' a
  'imp' (b 'or' c)) by BVFUNC_4:8
    .='not' ((a 'or' b) '&' ('not' a 'or' c) '&' ('not' b 'or' c)) 'or' (
  'not' a 'imp' (b 'or' c)) by BVFUNC_4:8
    .='not' ((a 'or' b) '&' ('not' a 'or' c) '&' ('not' b 'or' c)) 'or' (
  'not' 'not' a 'or' (b 'or' c)) by BVFUNC_4:8
    .=('not' ((a 'or' b) '&' ('not' a 'or' c)) 'or' 'not' ('not' b 'or' c))
  'or' ('not' 'not' a 'or' (b 'or' c)) by BVFUNC_1:14
    .=('not' ((a 'or' b) '&' ('not' a 'or' c)) 'or' ('not' 'not' b '&' 'not'
  c)) 'or' ('not' 'not' a 'or' (b 'or' c)) by BVFUNC_1:13
    .=(('not' (a 'or' b) 'or' 'not' ('not' a 'or' c)) 'or' (b '&' 'not' c))
  'or' ('not' 'not' a 'or' (b 'or' c)) by BVFUNC_1:14
    .=((('not' a '&' 'not' b) 'or' 'not' ('not' a 'or' c)) 'or' (b '&' 'not'
  c)) 'or' (a 'or' (b 'or' c)) by BVFUNC_1:13
    .=((('not' a '&' 'not' b) 'or' ('not' 'not' a '&' 'not' c)) 'or' (b '&'
  'not' c)) 'or' (a 'or' (b 'or' c)) by BVFUNC_1:13
    .=((('not' a 'or' (a '&' 'not' c)) '&' ('not' b 'or' (a '&' 'not' c)))
  'or' (b '&' 'not' c)) 'or' (a 'or' (b 'or' c)) by BVFUNC_1:11
    .=(((('not' a 'or' a) '&' ('not' a 'or' 'not' c)) '&' ('not' b 'or' (a
  '&' 'not' c))) 'or' (b '&' 'not' c)) 'or' (a 'or' (b 'or' c)) by BVFUNC_1:11
    .=(((I_el(Y) '&' ('not' a 'or' 'not' c)) '&' ('not' b 'or' (a '&' 'not'
  c))) 'or' (b '&' 'not' c)) 'or' (a 'or' (b 'or' c)) by BVFUNC_4:6
    .=((('not' a 'or' 'not' c) '&' ('not' b 'or' (a '&' 'not' c))) 'or' (b
  '&' 'not' c)) 'or' (a 'or' (b 'or' c)) by BVFUNC_1:6
    .=(((('not' a 'or' 'not' c) '&' 'not' b) 'or' (('not' a 'or' 'not' c)
  '&' (a '&' 'not' c))) 'or' (b '&' 'not' c)) 'or' (a 'or' (b 'or' c)) by
BVFUNC_1:12
    .=(((('not' a 'or' 'not' c) '&' 'not' b) 'or' ((('not' a 'or' 'not' c)
'&' a) '&' 'not' c)) 'or' (b '&' 'not' c)) 'or' (a 'or' (b 'or' c)) by
BVFUNC_1:4
    .=(((('not' a 'or' 'not' c) '&' 'not' b) 'or' ((('not' a '&' a) 'or' (
'not' c '&' a)) '&' 'not' c)) 'or' (b '&' 'not' c)) 'or' (a 'or' (b 'or' c))
by BVFUNC_1:12
    .=(((('not' a 'or' 'not' c) '&' 'not' b) 'or' ((O_el(Y) 'or' ('not' c
  '&' a)) '&' 'not' c)) 'or' (b '&' 'not' c)) 'or' (a 'or' (b 'or' c)) by
BVFUNC_4:5
    .=(((('not' a 'or' 'not' c) '&' 'not' b) 'or' (('not' c '&' a) '&' 'not'
  c)) 'or' (b '&' 'not' c)) 'or' (a 'or' (b 'or' c)) by BVFUNC_1:9
    .=((('not' c '&' a) '&' 'not' c) 'or' ((('not' a 'or' 'not' c) '&' 'not'
  b) 'or' (b '&' 'not' c))) 'or' (a 'or' (b 'or' c)) by BVFUNC_1:8
    .=((('not' c '&' a) '&' 'not' c) 'or' ((('not' a 'or' 'not' c) '&' 'not'
  b) 'or' (b '&' 'not' c))) 'or' (c 'or' (a 'or' b)) by BVFUNC_1:8
    .=((((('not' a 'or' 'not' c) '&' 'not' b) 'or' (b '&' 'not' c)) 'or' ((
  'not' c '&' a) '&' 'not' c)) 'or' c) 'or' (a 'or' b) by BVFUNC_1:8
    .=(((('not' a 'or' 'not' c) '&' 'not' b) 'or' (b '&' 'not' c)) 'or' (((
  'not' c '&' a) '&' 'not' c) 'or' c)) 'or' (a 'or' b) by BVFUNC_1:8
    .=(((('not' a 'or' 'not' c) '&' 'not' b) 'or' (b '&' 'not' c)) 'or' (((
  'not' c '&' a) 'or' c) '&' ('not' c 'or' c))) 'or' (a 'or' b) by BVFUNC_1:11
    .=(((('not' a 'or' 'not' c) '&' 'not' b) 'or' (b '&' 'not' c)) 'or' (((
  'not' c '&' a) 'or' c) '&' I_el(Y))) 'or' (a 'or' b) by BVFUNC_4:6
    .=(((('not' a 'or' 'not' c) '&' 'not' b) 'or' (b '&' 'not' c)) 'or' (((
  'not' c '&' a) 'or' c))) 'or' (a 'or' b) by BVFUNC_1:6
    .=(((('not' a 'or' 'not' c) '&' 'not' b) 'or' (b '&' 'not' c)) 'or' (((
  'not' c 'or' c) '&' (a 'or' c)))) 'or' (a 'or' b) by BVFUNC_1:11
    .=(((('not' a 'or' 'not' c) '&' 'not' b) 'or' (b '&' 'not' c)) 'or' ((
  I_el(Y) '&' (a 'or' c)))) 'or' (a 'or' b) by BVFUNC_4:6
    .=(((('not' a 'or' 'not' c) '&' 'not' b) 'or' (b '&' 'not' c)) 'or' (a
  'or' c)) 'or' (a 'or' b) by BVFUNC_1:6
    .=((('not' a 'or' 'not' c) '&' 'not' b) 'or' ((b '&' 'not' c) 'or' (c
  'or' a))) 'or' (a 'or' b) by BVFUNC_1:8
    .=((('not' a 'or' 'not' c) '&' 'not' b) 'or' (((b '&' 'not' c) 'or' c)
  'or' a)) 'or' (a 'or' b) by BVFUNC_1:8
    .=((('not' a 'or' 'not' c) '&' 'not' b) 'or' (((b 'or' c) '&' ('not' c
  'or' c)) 'or' a)) 'or' (a 'or' b) by BVFUNC_1:11
    .=((('not' a 'or' 'not' c) '&' 'not' b) 'or' (((b 'or' c) '&' I_el(Y))
  'or' a)) 'or' (a 'or' b) by BVFUNC_4:6
    .=((('not' a 'or' 'not' c) '&' 'not' b) 'or' ((b 'or' c)'or' a)) 'or' (a
  'or' b) by BVFUNC_1:6
    .=((('not' a 'or' 'not' c) '&' 'not' b) 'or' (b 'or' (c 'or' a))) 'or' (
  a 'or' b) by BVFUNC_1:8
    .=(((('not' a 'or' 'not' c) '&' 'not' b) 'or' b) 'or' (c 'or' a)) 'or' (
  a 'or' b) by BVFUNC_1:8
    .=(((('not' a 'or' 'not' c) 'or' b) '&' ('not' b 'or' b)) 'or' (c 'or' a
  )) 'or' (a 'or' b) by BVFUNC_1:11
    .=(((('not' a 'or' 'not' c) 'or' b) '&' I_el(Y)) 'or' (c 'or' a)) 'or' (
  a 'or' b) by BVFUNC_4:6
    .=((('not' a 'or' 'not' c) 'or' b) 'or' (c 'or' a)) 'or' (a 'or' b) by
BVFUNC_1:6
    .=(((('not' a 'or' 'not' c) 'or' b) 'or' c) 'or' a) 'or' (a 'or' b) by
BVFUNC_1:8
    .=(((('not' a 'or' 'not' c) 'or' c) 'or' b) 'or' a) 'or' (a 'or' b) by
BVFUNC_1:8
    .=((('not' a 'or' ('not' c 'or' c)) 'or' b) 'or' a) 'or' (a 'or' b) by
BVFUNC_1:8
    .=((('not' a 'or' I_el(Y)) 'or' b) 'or' a) 'or' (a 'or' b) by BVFUNC_4:6
    .=((I_el(Y) 'or' b) 'or' a) 'or' (a 'or' b) by BVFUNC_1:10
    .=(I_el(Y) 'or' a) 'or' (a 'or' b) by BVFUNC_1:10
    .=I_el(Y) 'or' (a 'or' b) by BVFUNC_1:10
    .= I_el(Y) by BVFUNC_1:10;
  hence thesis by BVFUNC_1:16;
end;

begin :: from BVFUNC26

reserve Y for non empty set,
  a,b,c for Function of Y,BOOLEAN;

definition
  let p,q be boolean-valued Function;
  func p 'nand' q -> Function means
  :Def1:
  dom it = dom p /\ dom q & for x
  being set st x in dom it holds it.x = (p.x) 'nand' (q.x);
  existence
  proof
    deffunc F(object) = (p.$1) 'nand' (q.$1);
    consider s being Function such that
A1: dom s = dom p /\ dom q & for x being object st x in dom p /\ dom q
    holds s.x = F(x) from FUNCT_1:sch 3;
    take s;
    thus thesis by A1;
  end;
  uniqueness
  proof
    let s1,s2 be Function such that
A2: dom s1 = dom p /\ dom q and
A3: for x being set st x in dom s1 holds s1.x = (p.x) 'nand' (q.x) and
A4: dom s2 = dom p /\ dom q and
A5: for x being set st x in dom s2 holds s2.x = (p.x) 'nand' (q.x);
    for x being object st x in dom s1 holds s1.x = s2.x
    proof
      let x be object;
      assume
A6:   x in dom s1;
      then s1.x = (p.x) 'nand' (q.x) by A3;
      hence thesis by A2,A4,A5,A6;
    end;
    hence thesis by A2,A4,FUNCT_1:2;
  end;
  commutativity;
  func p 'nor' q -> Function means
  :Def2:
  dom it = dom p /\ dom q & for x
  being set st x in dom it holds it.x = (p.x) 'nor' (q.x);
  existence
  proof
    deffunc F(object) = (p.$1) 'nor' (q.$1);
    consider s being Function such that
A7: dom s = dom p /\ dom q &
for x being object st x in dom p /\ dom q
    holds s.x = F(x) from FUNCT_1:sch 3;
    take s;
    thus thesis by A7;
  end;
  uniqueness
  proof
    let s1,s2 be Function such that
A8: dom s1 = dom p /\ dom q and
A9: for x being set st x in dom s1 holds s1.x = (p.x) 'nor' (q.x) and
A10: dom s2 = dom p /\ dom q and
A11: for x being set st x in dom s2 holds s2.x = (p.x) 'nor' (q.x);
    for x being object st x in dom s1 holds s1.x = s2.x
    proof
      let x be object;
      assume
A12:  x in dom s1;
      then s1.x = (p.x) 'nor' (q.x) by A9;
      hence thesis by A8,A10,A11,A12;
    end;
    hence thesis by A8,A10,FUNCT_1:2;
  end;
  commutativity;
end;

registration
  let p,q be boolean-valued Function;
  cluster p 'nand' q -> boolean-valued;
  coherence
  proof
    let x be object;
    assume x in rng (p 'nand' q);
    then consider y being object such that
A1: y in dom (p 'nand' q) & x = (p 'nand' q).y by FUNCT_1:def 3;
    x = (p.y) 'nand' (q.y) by A1,Def1;
    then x = FALSE or x = TRUE by XBOOLEAN:def 3;
    hence thesis;
  end;
  cluster p 'nor' q -> boolean-valued;
  coherence
  proof
    let x be object;
    assume x in rng(p 'nor' q);
    then consider y being object such that
A2: y in dom(p 'nor' q) & x = (p 'nor' q).y by FUNCT_1:def 3;
    x = (p.y) 'nor' (q.y) by A2,Def2;
    then x = FALSE or x = TRUE by XBOOLEAN:def 3;
    hence thesis;
  end;
end;

definition
  let A be non empty set;
  let p,q be Function of A,BOOLEAN;
  redefine func p 'nand' q -> Function of A,BOOLEAN means  :: redefines 'nand' (BVFUNC25, definition)
  :Def3:
  for x being Element of A holds it.x = (p.x) 'nand' (q.x);
  coherence
  proof
    dom p = A & dom q = A by PARTFUN1:def 2; then
A1: dom(p 'nand' q) = A /\ A by Def1
      .= A;
    rng (p 'nand' q) c= BOOLEAN by MARGREL1:def 16;
    hence thesis by A1,FUNCT_2:2;
  end;
  compatibility
  proof
    let IT be Function of A,BOOLEAN;
A2: dom IT = A by FUNCT_2:def 1;
    hereby
      assume
A3:   IT = p 'nand' q;
      let x be Element of A;
      dom p = A & dom q = A by FUNCT_2:def 1;
      then dom(p 'nand' q) = A /\ A by Def1
        .= A;
      hence IT.x = (p.x) 'nand' (q.x) by A3,Def1;
    end;
A4: dom q = A by FUNCT_2:def 1;
A5: dom IT = A /\ A by FUNCT_2:def 1
      .= dom p /\ dom q by A4,FUNCT_2:def 1;
    assume for x being Element of A holds IT.x = (p.x) 'nand' (q.x);
    then
    for x being set st x in dom IT holds IT.x = (p.x) 'nand' (q.x) by A2;
    hence thesis by A5,Def1;
  end;
  redefine func p 'nor' q -> Function of A,BOOLEAN means  :: redefines 'nor' (BVFUNC25, definition)
  :Def4:
  for x being Element of A holds it.x = (p.x) 'nor' (q.x);
  coherence
  proof
    dom p = A & dom q = A by PARTFUN1:def 2; then
A6: dom (p 'nor' q) = A /\ A by Def2
      .= A;
    rng(p 'nor' q) c= BOOLEAN by MARGREL1:def 16;
    hence thesis by A6,FUNCT_2:2;
  end;
  compatibility
  proof
    let IT be Function of A,BOOLEAN;
A7: dom IT = A by FUNCT_2:def 1;
    hereby
      assume
A8:   IT = p 'nor' q;
      let x be Element of A;
      dom p = A & dom q = A by FUNCT_2:def 1;
      then dom(p 'nor' q) = A /\ A by Def2
        .= A;
      hence IT.x = (p.x) 'nor' (q.x) by A8,Def2;
    end;
A9: dom q = A by FUNCT_2:def 1;
A10:dom IT = A /\ A by FUNCT_2:def 1
      .= dom p /\ dom q by A9,FUNCT_2:def 1;
    assume for x being Element of A holds IT.x = (p.x) 'nor' (q.x); then
    for x being set st x in dom IT holds IT.x = (p.x) 'nor' (q.x) by A7;
    hence thesis by A10,Def2;
  end;
end;

definition let Y;
  let a,b be Function of Y,BOOLEAN;
  redefine func a 'nand' b -> Function of Y,BOOLEAN;  :: redefines 'nand' (BVFUNC25, definition)
  coherence
  proof
    a 'nand' b is Function of Y,BOOLEAN;
    hence thesis;
  end;
  redefine func a 'nor' b -> Function of Y,BOOLEAN;  :: redefines 'nor' (BVFUNC25, definition)
  coherence
  proof
    a 'nor' b is Function of Y,BOOLEAN;
    hence thesis;
  end;
end;

theorem th1:
  a 'nand' b = 'not' (a '&' b)
proof
    let x be Element of Y;
    thus ('not' (a '&' b)).x = 'not' (a '&' b).x by MARGREL1:def 19
      .= 'not' (a.x '&' b.x) by MARGREL1:def 20
      .= 'not' ('not' (a.x 'nand' b.x)) by BVFUNC_1:46
      .= (a 'nand' b).x by Def3;
end;

theorem Th2:
  a 'nor' b = 'not' (a 'or' b)
proof
  let x be Element of Y;
  thus ('not' (a 'or' b)).x = 'not' (a 'or' b).x by MARGREL1:def 19
      .= 'not' ((a).x 'or' (b).x) by BVFUNC_1:def 4
      .= 'not' 'not' (a.x 'nor' b.x) by BVFUNC_1:53
      .= (a 'nor' b).x by Def4;
end;

theorem Th3:
  I_el(Y) 'nand' a = 'not' a
proof
  I_el(Y) 'nand' a = 'not' (I_el(Y) '&' a) by th1;
  hence thesis by BVFUNC_1:6;
end;

theorem Th4:
  O_el(Y) 'nand' a = I_el(Y)
proof
  O_el(Y) 'nand' a = 'not' (O_el(Y) '&' a) & O_el(Y) '&' a = O_el(Y) by th1,
BVFUNC_1:5;
  hence thesis by BVFUNC_1:2;
end;

theorem
  O_el(Y) 'nand' O_el(Y) = I_el(Y) & O_el(Y) 'nand' I_el(Y) = I_el(Y) &
  I_el(Y) 'nand' I_el(Y) = O_el(Y)
proof
  thus O_el(Y) 'nand' O_el(Y) = I_el(Y) by Th4;
  thus O_el(Y) 'nand' I_el(Y) = I_el(Y) by Th4;
  thus I_el(Y) 'nand' I_el(Y) = 'not' I_el(Y) by Th3
    .= O_el(Y) by BVFUNC_1:2;
end;

theorem
  a 'nand' a = 'not' a & 'not' (a 'nand' a) = a
proof
  a 'nand' a = 'not' (a '&' a) by th1
    .= 'not' a;
  hence thesis;
end;

theorem
  'not' (a 'nand' b) = a '&' b
proof
  'not' (a 'nand' b) = 'not' 'not' (a '&' b) by th1;
  hence thesis;
end;

theorem
  a 'nand' 'not' a = I_el(Y) & 'not' (a 'nand' 'not' a) = O_el(Y)
proof
  a 'nand' 'not' a = 'not' (a '&' 'not' a) by th1
    .= 'not' O_el(Y) by BVFUNC_4:5
    .= I_el(Y) by BVFUNC_1:2;
  hence thesis by BVFUNC_1:2;
end;

theorem Th9:
  a 'nand' (b '&' c) = 'not' (a '&' b '&' c)
proof
  a 'nand' (b '&' c) = 'not' (a '&' (b '&' c)) by th1;
  hence thesis by BVFUNC_1:4;
end;

theorem Th10:
  a 'nand' (b '&' c) = (a '&' b) 'nand' c
proof
  (a '&' b) 'nand' c = 'not' (a '&' b '&' c) by th1;
  hence thesis by Th9;
end;

theorem th11:
  a 'nand' (b 'or' c) = 'not' (a '&' b) '&' 'not' (a '&' c)
proof
  thus a 'nand' (b 'or' c) = 'not' (a '&' (b 'or' c)) by th1
    .= 'not' (a '&' b 'or' a '&' c) by BVFUNC_1:12
    .= 'not' (a '&' b) '&' 'not' (a '&' c) by BVFUNC_1:13;
end;

theorem
  a 'nand' (b 'xor' c) = (a '&' b) 'eqv' (a '&' c)
proof
  thus a 'nand' (b 'xor' c) = 'not' (a '&' (b 'xor' c)) by th1
    .= 'not' ((a '&' b) 'xor' (a '&' c)) by Th11
    .= 'not' 'not' ((a '&' b) 'eqv' (a '&' c)) by BVFUNC_6:85
    .= (a '&' b) 'eqv' (a '&' c);
end;

theorem
  a 'nand' (b 'nand' c) = 'not' a 'or' (b '&' c) & a 'nand' (b 'nand' c)
  = a 'imp' (b '&' c)
proof
  a 'nand' (b 'nand' c) = 'not' (a '&' (b 'nand' c)) by th1
    .= 'not' (a '&' 'not' (b '&' c)) by th1
    .= 'not' a 'or' 'not' 'not' (b '&' c) by BVFUNC_1:14
    .= 'not' a 'or' (b '&' c);
  hence thesis by BVFUNC_4:8;
end;

theorem
  a 'nand' (b 'nor' c) = 'not' a 'or' b 'or' c & a 'nand' (b 'nor' c) =
  a 'imp' (b 'or' c)
proof
A1: a 'nand' (b 'nor' c) = 'not' (a '&' (b 'nor' c)) by th1
    .= 'not' (a '&' 'not' (b 'or' c)) by Th2
    .= 'not' a 'or' 'not' 'not' (b 'or' c) by BVFUNC_1:14
    .= 'not' a 'or' b 'or' c by BVFUNC_1:8;
  then a 'nand' (b 'nor' c) = 'not' a 'or' (b 'or' c) by BVFUNC_1:8;
  hence thesis by A1,BVFUNC_4:8;
end;

theorem
  a 'nand' (b 'eqv' c) = a 'imp' (b 'xor' c)
proof
  a 'nand' (b 'eqv' c) = 'not' (a '&' (b 'eqv' c)) by th1
    .= ('not' a) 'or' 'not' (b 'eqv' c) by BVFUNC_1:14
    .= ('not' a) 'or' 'not' 'not' (b 'xor' c) by Th12
    .= ('not' a) 'or' (b 'xor' c);
  hence thesis by BVFUNC_4:8;
end;

theorem
  a 'nand' (a '&' b) = a 'nand' b
proof
  a 'nand' (a '&' b) = (a '&' a) 'nand' b by Th10;
  hence thesis;
end;

theorem
  a 'nand' (a 'or' b) = 'not' a '&' 'not' (a '&' b)
proof
  thus a 'nand' (a 'or' b) = 'not' (a '&' a) '&' 'not' (a '&' b) by th11
    .= 'not' a '&' 'not' (a '&' b);
end;

theorem
  a 'nand' (a 'eqv' b) = a 'imp' (a 'xor' b)
proof
  a 'nand' (a 'eqv' b) = 'not' (a '&' (a 'eqv' b)) by th1
    .= 'not' a 'or' 'not' (a 'eqv' b) by BVFUNC_1:14
    .= 'not' a 'or' 'not' 'not' (a 'xor' b) by Th12
    .= 'not' a 'or' (a 'xor' b);
  hence thesis by BVFUNC_4:8;
end;

theorem
  a 'nand' (a 'nand' b) = 'not' a 'or' b & a 'nand' (a 'nand' b) = a 'imp' b
proof
  a 'nand' (a 'nand' b) = 'not' (a '&' (a 'nand' b)) by th1
    .= 'not' (a '&' 'not' (a '&' b)) by th1
    .= ('not' a) 'or' ('not' 'not' (a '&' b)) by BVFUNC_1:14
    .= ('not' a 'or' a) '&' ('not' a 'or' b) by BVFUNC_1:11
    .= I_el(Y) '&' ('not' a 'or' b) by BVFUNC_4:6
    .= 'not' a 'or' b by BVFUNC_1:6;
  hence thesis by BVFUNC_4:8;
end;

theorem
  a 'nand' (a 'nor' b) = I_el(Y)
proof
  thus a 'nand' (a 'nor' b) = 'not' (a '&' (a 'nor' b)) by th1
    .= 'not' (a '&' 'not' (a 'or' b)) by Th2
    .= ('not' a) 'or' ('not' 'not' (a 'or' b)) by BVFUNC_1:14
    .= ('not' a) 'or' a 'or' b by BVFUNC_1:8
    .= I_el(Y) 'or' b by BVFUNC_4:6
    .= I_el(Y) by BVFUNC_1:10;
end;

theorem
  a 'nand' (a 'eqv' b) = 'not' a 'or' 'not' b
proof
  thus a 'nand' (a 'eqv' b) = 'not' (a '&' (a 'eqv' b)) by th1
    .= 'not' (a '&' 'not' (a 'xor' b)) by Th12
    .= ('not' a) 'or' ('not' 'not' (a 'xor' b)) by BVFUNC_1:14
    .= ('not' a) 'or' ((a 'or' b) '&' ('not' a 'or' 'not' b))
      by BVFUNC_6:86
    .= (('not' a) 'or' (a 'or' b)) '&' (('not' a) 'or' ('not' a 'or' 'not' b
  )) by BVFUNC_1:11
    .= (('not' a) 'or' a 'or' b) '&' (('not' a) 'or' ('not' a 'or' 'not' b))
  by BVFUNC_1:8
    .= (I_el(Y) 'or' b) '&' (('not' a) 'or' ('not' a 'or' 'not' b)) by
BVFUNC_4:6
    .= I_el(Y) '&' (('not' a) 'or' ('not' a 'or' 'not' b)) by BVFUNC_1:10
    .= ('not' a) 'or' ('not' a 'or' 'not' b) by BVFUNC_1:6
    .= ('not' a) 'or' 'not' a 'or' 'not' b by BVFUNC_1:8
    .= 'not' a 'or' 'not' b;
end;

theorem
  a '&' b = (a 'nand' b) 'nand' (a 'nand' b)
proof
  thus (a 'nand' b) 'nand' (a 'nand' b) = 'not' ((a 'nand' b) '&' (a 'nand' b)
  ) by th1
    .= (a '&' b) 'or' 'not' 'not' (a '&' b) by th1
    .= (a '&' b);
end;

theorem
  (a 'nand' b) 'nand' (a 'nand' c) = a '&' (b 'or' c)
proof
  thus (a 'nand' b) 'nand' (a 'nand' c) = 'not' ((a 'nand' b) '&' (a 'nand' c)
  ) by th1
    .= 'not' ('not' (a '&' b) '&' (a 'nand' c)) by th1
    .= 'not' ('not' (a '&' b) '&' 'not' (a '&' c)) by th1
    .= 'not' 'not' (a '&' b) 'or' 'not' 'not' (a '&' c) by BVFUNC_1:14
    .= a '&' (b 'or' c) by BVFUNC_1:12;
end;

theorem Th24:
  a 'nand' (b 'imp' c) = ('not' a 'or' b) '&' 'not' (a '&' c)
proof
  thus a 'nand' (b 'imp' c) = 'not' (a '&' (b 'imp' c)) by th1
    .= 'not' (a '&' ('not' b 'or' c)) by BVFUNC_4:8
    .= 'not' ((a '&' 'not' b) 'or' (a '&' c)) by BVFUNC_1:12
    .= 'not' (a '&' 'not' b) '&' 'not' (a '&' c) by BVFUNC_1:13
    .= (('not' a) 'or' ('not' 'not' b)) '&' 'not' (a '&' c) by BVFUNC_1:14
    .= ('not' a 'or' b) '&' 'not' (a '&' c);
end;

theorem
  a 'nand' (a 'imp' b) = 'not' (a '&' b)
proof
  thus a 'nand' (a 'imp' b) = ('not' a 'or' a) '&' 'not' (a '&' b) by Th24
    .= I_el(Y) '&' 'not' (a '&' b) by BVFUNC_4:6
    .= 'not' (a '&' b) by BVFUNC_1:6;
end;

theorem Th26:
  I_el(Y) 'nor' a = O_el(Y)
proof
  thus I_el(Y) 'nor' a = 'not' (I_el(Y) 'or' a) by Th2
    .= 'not' I_el(Y) by BVFUNC_1:10
    .= O_el(Y) by BVFUNC_1:2;
end;

theorem Th27:
  O_el(Y) 'nor' a = 'not' a
proof
  thus O_el(Y) 'nor' a = 'not' (O_el(Y) 'or' a) by Th2
    .= 'not' a by BVFUNC_1:9;
end;

theorem
  O_el(Y) 'nor' O_el(Y) = I_el(Y) & O_el(Y) 'nor' I_el(Y) = O_el(Y) &
  I_el(Y) 'nor' I_el(Y) = O_el(Y)
proof
  thus O_el(Y) 'nor' O_el(Y) = 'not' O_el(Y) by Th27
    .= I_el(Y) by BVFUNC_1:2;
  thus O_el(Y) 'nor' I_el(Y) = O_el(Y) by Th26;
  thus thesis by Th26;
end;

theorem
  a 'nor' a = 'not' a & 'not' (a 'nor' a) = a
proof
  a 'nor' a = 'not' (a 'or' a) by Th2
    .= 'not' a;
  hence thesis;
end;

theorem
  'not' (a 'nor' b) = a 'or' b
proof
  'not' (a 'nor' b) = 'not' 'not' (a 'or' b) by Th2;
  hence thesis;
end;

theorem
  a 'nor' 'not' a = O_el(Y) & 'not' (a 'nor' 'not' a) = I_el(Y)
proof
  a 'nor' 'not' a = 'not' (a 'or' 'not' a) by Th2
    .= 'not' I_el(Y) by BVFUNC_4:6
    .= O_el(Y) by BVFUNC_1:2;
  hence thesis by BVFUNC_1:2;
end;

theorem
  'not' a '&' (a 'xor' b) = 'not' a '&' b
proof
  thus ('not' a) '&' (a 'xor' b) = ('not' a) '&' (('not' a '&' b) 'or' (a '&'
  'not' b)) by BVFUNC_4:9
    .= (('not' a) '&' ('not' a '&' b)) 'or' (('not' a) '&' (a '&' 'not' b))
  by BVFUNC_1:12
    .= ('not' a '&' 'not' a '&' b) 'or' (('not' a) '&' (a '&' 'not' b)) by
BVFUNC_1:4
    .= ('not' a '&' b) 'or' ('not' a '&' a '&' 'not' b) by BVFUNC_1:4
    .= ('not' a '&' b) 'or' (O_el(Y) '&' 'not' b) by BVFUNC_4:5
    .= ('not' a '&' b) 'or' O_el(Y) by BVFUNC_1:5
    .= 'not' a '&' b by BVFUNC_1:9;
end;

theorem Th33:
  a 'nor' (b '&' c) = 'not' (a 'or' b) 'or' 'not' (a 'or' c)
proof
  a 'nor' (b '&' c) = 'not' (a 'or' (b '&' c)) by Th2
    .= 'not' ((a 'or' b) '&' (a 'or' c)) by BVFUNC_1:11;
  hence thesis by BVFUNC_1:14;
end;

theorem Th34:
  a 'nor' (b 'or' c) = 'not' (a 'or' b 'or' c)
proof
  thus a 'nor' (b 'or' c) = 'not' (a 'or' (b 'or' c)) by Th2
    .= 'not' (a 'or' b 'or' c) by BVFUNC_1:8;
end;

theorem Th35:
  a 'nor' (b 'eqv' c) = ('not' a) '&' (b 'xor' c)
proof
  thus a 'nor' (b 'eqv' c) = 'not' (a 'or' (b 'eqv' c)) by Th2
    .= ('not' a) '&' ('not' (b 'eqv' c)) by BVFUNC_1:13
    .= ('not' a) '&' ('not' 'not' (b 'xor' c)) by Th12
    .= ('not' a) '&' (b 'xor' c);
end;

theorem Th36:
  a 'nor' (b 'imp' c) = 'not' a '&' b '&' 'not' c
proof
  thus a 'nor' (b 'imp' c) = 'not' (a 'or' (b 'imp' c)) by Th2
    .= ('not' a) '&' ('not' (b 'imp' c)) by BVFUNC_1:13
    .= ('not' a) '&' (b '&' 'not' c) by Th1
    .= 'not' a '&' b '&' 'not' c by BVFUNC_1:4;
end;

theorem Th37:
  a 'nor' (b 'nand' c) = 'not' a '&' b '&' c
proof
  thus a 'nor' (b 'nand' c) = 'not' (a 'or' (b 'nand' c)) by Th2
    .= 'not' (a 'or' 'not' (b '&' c)) by th1
    .= 'not' a '&' 'not' 'not' (b '&' c) by BVFUNC_1:13
    .= 'not' a '&' b '&' c by BVFUNC_1:4;
end;

theorem Th38:
  a 'nor' (b 'nor' c) = 'not' a '&' (b 'or' c)
proof
  thus a 'nor' (b 'nor' c) = 'not' (a 'or' (b 'nor' c)) by Th2
    .= 'not' (a 'or' 'not' (b 'or' c)) by Th2
    .= 'not' a '&' 'not' 'not' (b 'or' c) by BVFUNC_1:13
    .= 'not' a '&' (b 'or' c);
end;

theorem
  a 'nor' (a '&' b) = 'not' (a '&' (a 'or' b))
proof
  thus a 'nor' (a '&' b) = 'not' (a 'or' a) 'or' 'not' (a 'or' b) by Th33
    .= 'not' (a '&' (a 'or' b)) by BVFUNC_1:14;
end;

theorem
  a 'nor' (a 'or' b) = 'not' (a 'or' b)
proof
  thus a 'nor' (a 'or' b) = 'not' (a 'or' a 'or' b) by Th34
    .= 'not' (a 'or' b);
end;

theorem
  a 'nor' (a 'eqv' b) = 'not' a '&' b
proof
  thus a 'nor' (a 'eqv' b) = ('not' a) '&' (a 'xor' b) by Th35
    .= ('not' a) '&' (('not' a '&' b) 'or' (a '&' 'not' b)) by BVFUNC_4:9
    .= ('not' a) '&' ('not' a '&' b) 'or' ('not' a) '&' (a '&' 'not' b) by
BVFUNC_1:12
    .= ('not' a) '&' ('not' a '&' b) 'or' ('not' a '&' a '&' 'not' b) by
BVFUNC_1:4
    .= ('not' a) '&' ('not' a '&' b) 'or' (O_el(Y) '&' 'not' b) by BVFUNC_4:5
    .= ('not' a) '&' ('not' a '&' b) 'or' O_el(Y) by BVFUNC_1:5
    .= ('not' a) '&' ('not' a '&' b) by BVFUNC_1:9
    .= ('not' a) '&' ('not' a) '&' b by BVFUNC_1:4
    .= 'not' a '&' b;
end;

theorem
  a 'nor' (a 'imp' b) = O_el(Y)
proof
  thus a 'nor' (a 'imp' b) = 'not' a '&' a '&' 'not' b by Th36
    .= O_el(Y) '&' 'not' b by BVFUNC_4:5
    .= O_el(Y) by BVFUNC_1:5;
end;

theorem
  a 'nor' (a 'nand' b) = O_el(Y)
proof
  thus a 'nor' (a 'nand' b) = 'not' a '&' a '&' b by Th37
    .= O_el(Y) '&' b by BVFUNC_4:5
    .= O_el(Y) by BVFUNC_1:5;
end;

theorem
  a 'nor' (a 'nor' b) = 'not' a '&' b
proof
  thus a 'nor' (a 'nor' b) = 'not' a '&' (a 'or' b) by Th38
    .= ('not' a '&' a) 'or' ('not' a '&' b) by BVFUNC_1:12
    .= O_el(Y) 'or' ('not' a '&' b) by BVFUNC_4:5
    .= 'not' a '&' b by BVFUNC_1:9;
end;

theorem
  O_el(Y) 'eqv' O_el(Y) = I_el(Y)
proof
  thus O_el(Y) 'eqv' O_el(Y) = 'not' (O_el(Y) 'xor' O_el(Y)) by Th12
    .= 'not' O_el(Y) by Th13
    .= I_el(Y) by BVFUNC_1:2;
end;

theorem
  O_el(Y) 'eqv' I_el(Y) = O_el(Y)
proof
  thus O_el(Y) 'eqv' I_el(Y) = 'not' (O_el(Y) 'xor' I_el(Y)) by Th12
    .= 'not' (O_el(Y) 'xor' 'not' O_el(Y)) by BVFUNC_1:2
    .= 'not' I_el(Y) by Th14
    .= O_el(Y) by BVFUNC_1:2;
end;

theorem
  I_el(Y) 'eqv' I_el(Y) = I_el(Y)
proof
  thus I_el(Y) 'eqv' I_el(Y) = 'not' (I_el(Y) 'xor' I_el(Y)) by Th12
    .= 'not' 'not' I_el(Y) by BVFUNC_6:87
    .= I_el(Y);
end;

theorem
  a 'eqv' a = I_el(Y) & 'not' (a 'eqv' a) = O_el(Y)
proof
  a 'eqv' a = 'not' (a 'xor' a) by Th12
    .= 'not' O_el(Y) by Th13
    .= I_el(Y) by BVFUNC_1:2;
  hence thesis by BVFUNC_1:2;
end;

theorem
  a 'eqv' (a 'or' b) = a 'or' 'not' b
proof
  thus a 'eqv' (a 'or' b) = 'not' (a 'xor' (a 'or' b)) by Th12
    .= 'not' (('not' a '&' (a 'or' b)) 'or' (a '&' 'not' (a 'or' b))) by
BVFUNC_4:9
    .= 'not' (('not' a '&' a 'or' 'not' a '&' b) 'or' (a '&' 'not' (a 'or' b
  ))) by BVFUNC_1:12
    .= 'not' ((O_el(Y) 'or' 'not' a '&' b) 'or' (a '&' 'not' (a 'or' b))) by
BVFUNC_4:5
    .= 'not' (('not' a '&' b) 'or' (a '&' 'not' (a 'or' b))) by BVFUNC_1:9
    .= 'not' (('not' a '&' b) 'or' (a '&' ('not' a '&' 'not' b))) by
BVFUNC_1:13
    .= 'not' (('not' a '&' b) 'or' (a '&' 'not' a '&' 'not' b)) by BVFUNC_1:4
    .= 'not' (('not' a '&' b) 'or' (O_el(Y) '&' 'not' b)) by BVFUNC_4:5
    .= 'not' (('not' a '&' b) 'or' O_el(Y)) by BVFUNC_1:5
    .= 'not' ('not' a '&' b) by BVFUNC_1:9
    .= 'not' 'not' a 'or' 'not' b by BVFUNC_1:14
    .= a 'or' 'not' b;
end;

theorem Th50:
  a '&' (b 'nand' c) = (a '&' 'not' b) 'or' (a '&' 'not' c)
proof
  thus a '&' (b 'nand' c) =a '&' 'not' (b '&' c) by th1
    .=a '&' ('not' b 'or' 'not' c) by BVFUNC_1:14
    .=(a '&' 'not' b) 'or' (a '&' 'not' c) by BVFUNC_1:12;
end;

theorem Th51:
  a 'or' (b 'nand' c) = a 'or' 'not' b 'or' 'not' c
proof
  thus a 'or' (b 'nand' c) =a 'or' 'not' (b '&' c) by th1
    .=a 'or' ('not' b 'or' 'not' c) by BVFUNC_1:14
    .=a 'or' 'not' b 'or' 'not' c by BVFUNC_1:8;
end;

theorem Th52:
  a 'xor' (b 'nand' c) = ('not' a '&' 'not' (b '&' c)) 'or' (a '&' b '&' c)
proof
  thus a 'xor' (b 'nand' c) =a 'xor' 'not' (b '&' c) by th1
    .=('not' a '&' 'not' (b '&' c)) 'or' (a '&' 'not' 'not' (b '&' c)) by
BVFUNC_4:9
    .=('not' a '&' 'not' (b '&' c)) 'or' (a '&' b '&' c) by BVFUNC_1:4;
end;

theorem Th53:
  a 'eqv' (b 'nand' c) = (a '&' 'not' (b '&' c)) 'or' ('not' a '&' b '&' c)
proof
  thus a 'eqv' (b 'nand' c) =a 'eqv' 'not' (b '&' c) by th1
    .=(a '&' 'not' (b '&' c)) 'or' ('not' a '&' 'not' 'not' (b '&' c)) by
BVFUNC_6:92
    .=(a '&' 'not' (b '&' c)) 'or' ('not' a '&' b '&' c) by BVFUNC_1:4;
end;

theorem Th54:
  a 'imp' (b 'nand' c) = 'not' (a '&' b '&' c)
proof
  thus a 'imp' (b 'nand' c) =a 'imp' 'not' (b '&' c) by th1
    .='not' a 'or' 'not' (b '&' c) by BVFUNC_4:8
    .='not' (a '&' (b '&' c)) by BVFUNC_1:14
    .='not' (a '&' b '&' c) by BVFUNC_1:4;
end;

theorem
  a 'nor' (b 'nand' c) = 'not' (a 'or' 'not' b 'or' 'not' c)
proof
  thus a 'nor' (b 'nand' c) =a 'nor' 'not' (b '&' c) by th1
    .='not' (a 'or' 'not' (b '&' c)) by Th2
    .='not' (a 'or' ('not' b 'or' 'not' c)) by BVFUNC_1:14
    .='not' (a 'or' 'not' b 'or' 'not' c) by BVFUNC_1:8;
end;

theorem
  a '&' (a 'nand' b) = a '&' 'not' b
proof
  thus a '&' (a 'nand' b) =(a '&' 'not' a) 'or' (a '&' 'not' b) by Th50
    .=O_el(Y) 'or' (a '&' 'not' b) by BVFUNC_4:5
    .=a '&' 'not' b by BVFUNC_1:9;
end;

theorem
  a 'or' (a 'nand' b) = I_el(Y)
proof
  thus a 'or' (a 'nand' b) =a 'or' 'not' a 'or' 'not' b by Th51
    .=I_el(Y) 'or' 'not' b by BVFUNC_4:6
    .=I_el(Y) by BVFUNC_1:10;
end;

theorem
  a 'xor' (a 'nand' b) = 'not' a 'or' b
proof
  thus a 'xor' (a 'nand' b) =('not' a '&' 'not' (a '&' b)) 'or' (a '&' a '&' b
  ) by Th52
    .=('not' a 'or' (a '&' b)) '&' ('not' (a '&' b) 'or' (a '&' b)) by
BVFUNC_1:11
    .=('not' a 'or' (a '&' b)) '&' I_el(Y) by BVFUNC_4:6
    .='not' a 'or' (a '&' b) by BVFUNC_1:6
    .=('not' a 'or' a) '&' ('not' a 'or' b) by BVFUNC_1:11
    .=I_el(Y) '&' ('not' a 'or' b) by BVFUNC_4:6
    .='not' a 'or' b by BVFUNC_1:6;
end;

theorem
  a 'eqv' (a 'nand' b) = a '&' 'not' b
proof
  thus a 'eqv' (a 'nand' b) =(a '&' 'not' (a '&' b)) 'or' ('not' a '&' a '&' b
  ) by Th53
    .=(a '&' 'not' (a '&' b)) 'or' (O_el(Y) '&' b) by BVFUNC_4:5
    .=(a '&' 'not' (a '&' b)) 'or' O_el(Y) by BVFUNC_1:5
    .=(a '&' 'not' (a '&' b)) by BVFUNC_1:9
    .=(a '&' ('not' a 'or' 'not' b)) by BVFUNC_1:14
    .=(a '&' 'not' a) 'or' (a '&' 'not' b) by BVFUNC_1:12
    .=O_el(Y) 'or' (a '&' 'not' b) by BVFUNC_4:5
    .=a '&' 'not' b by BVFUNC_1:9;
end;

theorem
  a 'imp' (a 'nand' b) = 'not' (a '&' b)
proof
  thus a 'imp' (a 'nand' b) ='not' (a '&' a '&' b) by Th54
    .='not' (a '&' b);
end;

theorem Th61:
  a '&' (b 'nor' c) = a '&' 'not' b '&' 'not' c
proof
  thus a '&' (b 'nor' c) =a '&' 'not' (b 'or' c) by Th2
    .=a '&' ('not' b '&' 'not' c) by BVFUNC_1:13
    .=a '&' 'not' b '&' 'not' c by BVFUNC_1:4;
end;

theorem Th62:
  a 'or' (b 'nor' c) = (a 'or' 'not' b) '&' (a 'or' 'not' c)
proof
  thus a 'or' (b 'nor' c) =a 'or' 'not' (b 'or' c) by Th2
    .=a 'or' ('not' b '&' 'not' c) by BVFUNC_1:13
    .=(a 'or' 'not' b) '&' (a 'or' 'not' c) by BVFUNC_1:11;
end;

theorem Th63:
  a 'xor' (b 'nor' c) = (a 'or' 'not' (b 'or' c)) '&' ('not' a 'or' b 'or' c)
proof
  thus a 'xor' (b 'nor' c) =a 'xor' 'not' (b 'or' c) by Th2
    .=(a 'or' 'not' (b 'or' c)) '&' ('not' a 'or' 'not' 'not' (b 'or' c)) by
BVFUNC_6:86
    .=(a 'or' 'not' (b 'or' c)) '&' ('not' a 'or' b 'or' c) by BVFUNC_1:8;
end;

theorem Th64:
  a 'eqv' (b 'nor' c) = (a 'or' b 'or' c) '&' ('not' a 'or' 'not' (b 'or' c))
proof
  thus a 'eqv' (b 'nor' c) =a 'eqv' 'not' (b 'or' c) by Th2
    .=(a 'or' 'not' 'not' (b 'or' c)) '&' ('not' a 'or' 'not' (b 'or' c))
      by BVFUNC_6:91
    .=(a 'or' b 'or' c) '&' ('not' a 'or' 'not' (b 'or' c)) by BVFUNC_1:8;
end;

theorem Th65:
  a 'imp' (b 'nor' c) = 'not' (a '&' (b 'or' c))
proof
  thus a 'imp' (b 'nor' c) =a 'imp' 'not' (b 'or' c) by Th2
    .='not' a 'or' 'not' (b 'or' c) by BVFUNC_4:8
    .='not' (a '&' (b 'or' c)) by BVFUNC_1:14;
end;

theorem
  a 'nand' (b 'nor' c) = 'not' a 'or' b 'or' c
proof
  thus a 'nand' (b 'nor' c) =a 'nand' 'not' (b 'or' c) by Th2
    .='not' (a '&' 'not' (b 'or' c)) by th1
    .='not' a 'or' 'not' 'not' (b 'or' c) by BVFUNC_1:14
    .='not' a 'or' b 'or' c by BVFUNC_1:8;
end;

theorem
  a '&' (a 'nor' b) = O_el(Y)
proof
  thus a '&' (a 'nor' b) =a '&' 'not' a '&' 'not' b by Th61
    .=O_el(Y) '&' 'not' b by BVFUNC_4:5
    .=O_el(Y) by BVFUNC_1:5;
end;

theorem
  a 'or' (a 'nor' b) = a 'or' 'not' b
proof
  thus a 'or' (a 'nor' b) =(a 'or' 'not' a) '&' (a 'or' 'not' b) by Th62
    .=I_el(Y) '&' (a 'or' 'not' b) by BVFUNC_4:6
    .=a 'or' 'not' b by BVFUNC_1:6;
end;

theorem
  a 'xor' (a 'nor' b) = a 'or' 'not' b
proof
  thus a 'xor' (a 'nor' b) =(a 'or' 'not' (a 'or' b)) '&' ('not' a 'or' a 'or'
  b) by Th63
    .=(a 'or' 'not' (a 'or' b)) '&' (I_el(Y) 'or' b) by BVFUNC_4:6
    .=(a 'or' 'not' (a 'or' b)) '&' I_el(Y) by BVFUNC_1:10
    .=a 'or' 'not' (a 'or' b) by BVFUNC_1:6
    .=a 'or' ('not' a '&' 'not' b) by BVFUNC_1:13
    .=(a 'or' 'not' a) '&' (a 'or' 'not' b) by BVFUNC_1:11
    .=I_el(Y) '&' (a 'or' 'not' b) by BVFUNC_4:6
    .=a 'or' 'not' b by BVFUNC_1:6;
end;

theorem
  a 'eqv' (a 'nor' b) = 'not' a '&' b
proof
  thus a 'eqv' (a 'nor' b) =(a 'or' a 'or' b) '&' ('not' a 'or' 'not' (a 'or'
  b)) by Th64
    .=((a 'or' b) '&' 'not' a) 'or' ((a 'or' b) '&' 'not' (a 'or' b)) by
BVFUNC_1:12
    .=((a 'or' b) '&' 'not' a) 'or' O_el(Y) by BVFUNC_4:5
    .=(a 'or' b) '&' 'not' a by BVFUNC_1:9
    .=(a '&' 'not' a) 'or' (b '&' 'not' a) by BVFUNC_1:12
    .=O_el(Y) 'or' (b '&' 'not' a) by BVFUNC_4:5
    .='not' a '&' b by BVFUNC_1:9;
end;

theorem
  a 'imp' (a 'nor' b) = 'not' (a 'or' a '&' b)
proof
  thus a 'imp' (a 'nor' b) ='not' (a '&' (a 'or' b)) by Th65
    .='not' (a '&' a 'or' a '&' b) by BVFUNC_1:12
    .='not' (a 'or' a '&' b);
end;