The abstract of the Mizar article:

On the Calculus of Binary Arithmetics

by

Shunichi Kobayashi

Received August 23, 2003

MML identifier: BINARI_5

[ Mizar article, MML identifier index ]

environ

 vocabulary MARGREL1, ZF_LANG, BINARITH, PARTIT1, BVFUNC_1, BINARI_5;
 notation SUBSET_1, MARGREL1, BINARITH, BVFUNC_1;
 constructors BINARITH, XREAL_0, BVFUNC_1;
 clusters MARGREL1, BINARITH, BVFUNC_1;
 requirements SUBSET;


begin

definition
  let x, y be boolean set;
  func x 'nand' y equals
:: BINARI_5:def 1
   'not' (x '&' y);
  commutativity;
end;

definition
  let x, y be boolean set;
  cluster x 'nand' y -> boolean;
end;

definition
  let x, y be Element of BOOLEAN;
  redefine func x 'nand' y -> Element of BOOLEAN;
end;

definition
  let x, y be boolean set;
  func x 'nor' y equals
:: BINARI_5:def 2
   'not' (x 'or' y);
  commutativity;
end;

definition
  let x, y be boolean set;
  cluster x 'nor' y -> boolean;
end;

definition
  let x, y be Element of BOOLEAN;
  redefine func x 'nor' y -> Element of BOOLEAN;
end;

definition
  let x, y be boolean set;
  func x 'xnor' y equals
:: BINARI_5:def 3
   'not' (x 'xor' y);
  commutativity;
end;

definition
  let x, y be boolean set;
  cluster x 'xnor' y -> boolean;
end;

definition
  let x, y be Element of BOOLEAN;
  redefine func x 'xnor' y -> Element of BOOLEAN;
end;

 reserve x,y,z,w for boolean set;

theorem :: BINARI_5:1
TRUE 'nand' x = 'not' x;

theorem :: BINARI_5:2
FALSE 'nand' x = TRUE;

theorem :: BINARI_5:3
x 'nand' x = 'not' x &
'not' (x 'nand' x) = x;

theorem :: BINARI_5:4
'not' (x 'nand' y) = x '&' y;

theorem :: BINARI_5:5
x 'nand' 'not' x = TRUE &
'not' (x 'nand' 'not' x) = FALSE;

theorem :: BINARI_5:6
x 'nand' (y '&' z) = 'not' (x '&' y '&' z);

theorem :: BINARI_5:7
x 'nand' (y '&' z) = (x '&' y) 'nand' z;

theorem :: BINARI_5:8
x 'nand' (y 'or' z) = 'not' (x '&' y) '&' 'not' (x '&' z);

theorem :: BINARI_5:9
x 'nand' (y 'xor' z) = (x '&' y) 'eqv' (x '&' z);

theorem :: BINARI_5:10
TRUE 'nor' x = FALSE;

theorem :: BINARI_5:11
FALSE 'nor' x = 'not' x;

theorem :: BINARI_5:12
x 'nor' x = 'not' x &
'not' (x 'nor' x) = x;

theorem :: BINARI_5:13
'not' (x 'nor' y) = x 'or' y;

theorem :: BINARI_5:14
x 'nor' 'not' x = FALSE &
'not' (x 'nor' 'not' x) = TRUE;

theorem :: BINARI_5:15
x 'nor' (y '&' z) = 'not' (x 'or' y) 'or' 'not' (x 'or' z);

theorem :: BINARI_5:16
x 'nor' (y 'or' z) = 'not' (x 'or' y 'or' z);

theorem :: BINARI_5:17
TRUE 'xnor' x = x;

theorem :: BINARI_5:18
FALSE 'xnor' x = 'not' x;

theorem :: BINARI_5:19
x 'xnor' x = TRUE &
'not' (x 'xnor' x) = FALSE;

theorem :: BINARI_5:20
'not' (x 'xnor' y) = x 'xor' y;

theorem :: BINARI_5:21
x 'xnor' 'not' x = FALSE &
'not' (x 'xnor' 'not' x) = TRUE;

theorem :: BINARI_5:22
x '<' (y 'imp' z) iff x '&' y '<' z;

theorem :: BINARI_5:23
x 'eqv' y = (x 'imp' y) '&' (y 'imp' x);

theorem :: BINARI_5:24
x 'eqv' y = TRUE iff (x 'imp' y) = TRUE & (y 'imp' x) = TRUE;

theorem :: BINARI_5:25
(x 'imp' y)=TRUE & (y 'imp' x)=TRUE implies x = y;

theorem :: BINARI_5:26
(x 'imp' y)=TRUE & (y 'imp' z)=TRUE implies (x 'imp' z)=TRUE;

theorem :: BINARI_5:27
(x 'eqv' y)=TRUE & (y 'eqv' z)=TRUE implies (x 'eqv' z)=TRUE;

theorem :: BINARI_5:28
x 'imp' y = 'not' y 'imp' 'not' x;

theorem :: BINARI_5:29
x 'eqv' y = 'not' x 'eqv' 'not' y;

theorem :: BINARI_5:30
(x 'eqv' y)=TRUE & (z 'eqv' w)=TRUE implies ((x '&' z) 'eqv' (y '&' w))=TRUE;

theorem :: BINARI_5:31
(x 'eqv' y)=TRUE & (z 'eqv' w)=TRUE implies
(x 'imp' z) 'eqv' (y 'imp' w)=TRUE;

theorem :: BINARI_5:32
(x 'eqv' y)=TRUE & (z 'eqv' w)=TRUE implies
(x 'or' z) 'eqv' (y 'or' w)=TRUE;

theorem :: BINARI_5:33
(x 'eqv' y)=TRUE & (z 'eqv' w)=TRUE implies
((x 'eqv' z) 'eqv' (y 'eqv' w))=TRUE;

theorem :: BINARI_5:34
x=TRUE & (x 'imp' y)=TRUE implies y=TRUE;

theorem :: BINARI_5:35
y=TRUE implies (x 'imp' y)=TRUE;

theorem :: BINARI_5:36
('not' x)=TRUE implies (x 'imp' y)=TRUE;

theorem :: BINARI_5:37
x 'imp' x=TRUE;

theorem :: BINARI_5:38
(x 'imp' y)=TRUE & (x 'imp' 'not' y)=TRUE implies
'not' x=TRUE;

theorem :: BINARI_5:39
('not' x 'imp' x) 'imp' x = TRUE;

theorem :: BINARI_5:40
(x 'imp' y) 'imp' ('not' (y '&' z) 'imp' 'not' (x '&' z)) = TRUE;

theorem :: BINARI_5:41
(x 'imp' y) 'imp' ((y 'imp' z) 'imp' (x 'imp' z)) = TRUE;

theorem :: BINARI_5:42
(x 'imp' y)=TRUE implies ((y 'imp' z) 'imp' (x 'imp' z)) = TRUE;

theorem :: BINARI_5:43
y 'imp' (x 'imp' y) = TRUE;

theorem :: BINARI_5:44
((x 'imp' y) 'imp' z) 'imp' (y 'imp' z) = TRUE;

theorem :: BINARI_5:45
y 'imp' ((y 'imp' x) 'imp' x) = TRUE;

theorem :: BINARI_5:46
(z 'imp' (y 'imp' x)) 'imp' (y 'imp' (z 'imp' x)) = TRUE;

theorem :: BINARI_5:47
(y 'imp' z) 'imp' ((x 'imp' y) 'imp' (x 'imp' z)) = TRUE;

theorem :: BINARI_5:48
(y 'imp' (y 'imp' z)) 'imp' (y 'imp' z) = TRUE;

theorem :: BINARI_5:49
(x 'imp' (y 'imp' z)) 'imp' ((x 'imp' y) 'imp' (x 'imp' z)) = TRUE;

theorem :: BINARI_5:50
x=TRUE implies (x 'imp' y) 'imp' y=TRUE;

theorem :: BINARI_5:51
z 'imp' (y 'imp' x)=TRUE implies y 'imp' (z 'imp' x)=TRUE;

theorem :: BINARI_5:52
z 'imp' (y 'imp' x)=TRUE & y=TRUE implies z 'imp' x=TRUE;

theorem :: BINARI_5:53
z 'imp' (y 'imp' x)=TRUE & y=TRUE & z = TRUE implies x=TRUE;

theorem :: BINARI_5:54
y 'imp' (y 'imp' z)=TRUE implies y 'imp' z = TRUE;

theorem :: BINARI_5:55
(x 'imp' (y 'imp' z)) = TRUE implies
(x 'imp' y) 'imp' (x 'imp' z) = TRUE;