:: On the Calculus of Binary Arithmetics
::  by Shunichi Kobayashi
::
:: Received August 23, 2003
:: Copyright (c) 2003 Association of Mizar Users

environ

 vocabularies MARGREL1, ZF_LANG, BINARITH, PARTIT1, BINARI_5;
 notations SUBSET_1, XBOOLEAN, MARGREL1, BVFUNC_1;
 constructors XXREAL_0, BINARITH;
 registrations XBOOLEAN, MARGREL1;
 requirements ARITHM, BOOLE;
 definitions XBOOLEAN;
 theorems BVFUNC_1, XBOOLEAN;

begin

definition
  let x, y be Element of BOOLEAN;
  redefine func x 'nand' y -> Element of BOOLEAN;
  correctness
  proof
    x 'nand' y =FALSE or x 'nand' y = TRUE by XBOOLEAN:def 3;
    hence thesis;
  end;
end;

definition
  let x, y be Element of BOOLEAN;
  redefine func x 'nor' y -> Element of BOOLEAN;
  correctness
  proof
    x 'nor' y =FALSE or x 'nor' y = TRUE by XBOOLEAN:def 3;
    hence thesis;
  end;
end;

definition
  let x, y be boolean set;
  redefine
  canceled 2;
  func x <=> y equals

  'not' (x 'xor' y);
  correctness;
end;

definition
  let x, y be Element of BOOLEAN;
  redefine func x <=> y -> Element of BOOLEAN;
  correctness
  proof
    x <=> y =FALSE or x <=> y = TRUE by XBOOLEAN:def 3;
    hence thesis;
  end;
end;

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

theorem
  TRUE 'nand' x = 'not' x;

theorem
  FALSE 'nand' x = TRUE;

theorem
  x 'nand' x = 'not' x & 'not' (x 'nand' x) = x;

theorem
  'not' (x 'nand' y) = x '&' y;

theorem
  x 'nand' 'not' x = TRUE &
  'not' (x 'nand' 'not' x) = FALSE by XBOOLEAN:135,138;

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

theorem
  x 'nand' (y '&' z) = (x '&' y) 'nand' z;

canceled 2;

theorem
  TRUE 'nor' x = FALSE;

theorem
  FALSE 'nor' x = 'not' x;

theorem
  x 'nor' x = 'not' x & 'not' (x 'nor' x) = x;

theorem
  'not' (x 'nor' y) = x 'or' y;

theorem
  x 'nor' 'not' x = FALSE &
  'not' (x 'nor' 'not' x) = TRUE by XBOOLEAN:134,138;

canceled;

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

theorem
  TRUE <=> x = x;

theorem
  FALSE <=> x = 'not' x;

theorem
  x <=> x = TRUE & 'not' (x <=> x) = FALSE by XBOOLEAN:125,143;

theorem
  'not' (x <=> y) = x 'xor' y;

theorem
  x <=> 'not' x = FALSE & 'not' (x <=> 'not' x) = TRUE by XBOOLEAN:129,142;

theorem
  x <= (y => z) iff x '&' y <= z
proof
A1: x <= (y => z) implies x '&' y <= z
  proof
    assume x <= (y => z);
    then
A2: x => (y => z) = TRUE by BVFUNC_1:def 3;
    x => (y => z) = (x '&' y) => z;
    hence thesis by A2,BVFUNC_1:def 3;
  end;
  x '&' y <= z implies x <= (y => z)
  proof
    assume x '&' y <= z;
    then
A3: (x '&' y) => z = TRUE by BVFUNC_1:def 3;
    (x '&' y) => z = x => (y => z);
    hence thesis by A3,BVFUNC_1:def 3;
  end;
  hence thesis by A1;
end;

theorem
  x <=> y = (x => y) '&' (y => x);

canceled 4;

theorem
  x => y = 'not' y => 'not' x;

theorem
  x <=> y = 'not' x <=> 'not' y;

canceled 4;

theorem
  x=TRUE & (x => y)=TRUE implies y=TRUE;

theorem
  y=TRUE implies (x => y)=TRUE;

theorem
  ('not' x)=TRUE implies (x => y)=TRUE;

canceled 14;

theorem
  z => (y => x)=TRUE implies y => (z => x)=TRUE;

theorem
  z => (y => x)=TRUE & y=TRUE implies z => x=TRUE;

theorem
  z => (y => x)=TRUE & y=TRUE & z = TRUE implies x=TRUE;