XBOOLEAN

:: On the Arithmetic of Boolean Values
::  by Library Committee
::
:: Received November 30, 2006
:: Copyright (c) 2006-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 CARD_1, ORDINAL1, ARYTM_1, RELAT_1, XBOOLEAN;
 notations ORDINAL1, NUMBERS, XCMPLX_0;
 constructors XCMPLX_0, ORDINAL1, NUMBERS;
 registrations XCMPLX_0, ORDINAL1;
 requirements SUBSET, NUMERALS, ARITHM;

begin

definition
  func FALSE -> object equals
  0;
  coherence;
  func TRUE -> object equals
  1;
  coherence;
end;

definition
  let p be object;
  attr p is boolean means
  :Def3:
  p = FALSE or p = TRUE;
end;

registration
  cluster FALSE -> boolean;
  coherence;
  cluster TRUE -> boolean;
  coherence;
  cluster boolean for object;
  existence by Def3;
  cluster boolean -> natural for object;
  coherence;
end;

reserve p,q,r,s for boolean object;

definition
  let p;
  func 'not' p -> boolean object equals
  1 - p;
  coherence
  proof
    p = FALSE or p = TRUE by Def3;
    hence thesis by Def3;
  end;
  involutiveness;
  let q;
  func p '&' q -> object equals
  p*q;
  correctness;
  commutativity;
  idempotence
  proof
    let p;
    p = FALSE or p = TRUE by Def3;
    hence thesis;
  end;
end;

registration
  let p,q;
  cluster p '&' q -> boolean;
  coherence
  proof
    p = FALSE or p = TRUE by Def3;
    hence thesis;
  end;
end;

definition
  let p,q;
  func p 'or' q -> object equals
  'not' ('not' p '&' 'not' q);
  coherence;
  commutativity;
  idempotence;
end;

definition
  let p,q;
  func p => q -> object equals
  'not' p 'or' q;
  coherence;
end;

registration
  let p,q;
  cluster p 'or' q -> boolean;
  coherence;
  cluster p => q -> boolean;
  coherence;
end;

definition
  let p,q;
  func p <=> q -> object equals
  (p => q) '&' (q => p);
  coherence;
  commutativity;
end;

registration
  let p,q;
  cluster p <=> q -> boolean;
  coherence;
end;

definition
  let p,q;
  func p 'nand' q -> object equals
  'not'(p '&' q);
  coherence;
  commutativity;
  func p 'nor' q -> object equals
  'not'(p 'or' q);
  coherence;
  commutativity;
  func p 'xor' q -> object equals
  'not'(p <=> q);
  coherence;
  commutativity;
  func p '\' q -> object equals
  p '&' 'not' q;
  coherence;
end;

registration
  let p,q;
  cluster p 'nand' q -> boolean;
  coherence;
  cluster p 'nor' q -> boolean;
  coherence;
  cluster p 'xor' q -> boolean;
  coherence;
  cluster p '\' q -> boolean;
  coherence;
end;

begin

theorem
  p '&' p = p;

theorem
  p '&' (p '&' q) = p '&' q
proof
  p = FALSE or p = TRUE by Def3;
  hence thesis;
end;

theorem
  p 'or' p = p;

theorem
  p 'or' (p 'or' q) = p 'or' q
proof
  p = FALSE or p = TRUE by Def3;
  hence thesis;
end;

theorem
  p 'or' p '&' q = p
proof
  p = FALSE or p = TRUE by Def3;
  hence thesis;
end;

theorem
  p '&' (p 'or' q) = p
proof
  p = FALSE or p = TRUE by Def3;
  hence thesis;
end;

theorem
  p '&' (p 'or' q) = p 'or' (p '&' q)
proof
  p = FALSE or p = TRUE by Def3;
  hence thesis;
end;

theorem
  p '&' (q 'or' r) = p '&' q 'or' p '&' r
proof
  p = FALSE or p = TRUE by Def3;
  hence thesis;
end;

theorem
  p 'or' q '&' r = (p 'or' q) '&' (p 'or' r)
proof
  p = FALSE or p = TRUE by Def3;
  hence thesis;
end;

theorem
  p '&' q 'or' q '&' r 'or' r '&' p = (p 'or' q) '&' (q 'or' r) '&' (r 'or' p)
proof
A1: q = FALSE or q = TRUE by Def3;
  p = FALSE or p = TRUE by Def3;
  hence thesis by A1;
end;

theorem
  p '&' ('not' p 'or' q) = p '&' q
proof
  p = FALSE or p = TRUE by Def3;
  hence thesis;
end;

theorem
  p 'or' 'not' p '&' q = p 'or' q
proof
  p = FALSE or p = TRUE by Def3;
  hence thesis;
end;

theorem
  p => (p => q) = p => q
proof
  p = FALSE or p = TRUE by Def3;
  hence thesis;
end;

theorem
  p '&' (p => q) = p '&' q
proof
  p = FALSE or p = TRUE by Def3;
  hence thesis;
end;

theorem
  p => (p '&' q) = p => q
proof
  p = FALSE or p = TRUE by Def3;
  hence thesis;
end;

theorem
  p '&' 'not' (p => q) = p '&' 'not' q
proof
  p = FALSE or p = TRUE by Def3;
  hence thesis;
end;

theorem
  'not' p 'or' (p => q) = p => q
proof
  p = FALSE or p = TRUE by Def3;
  hence thesis;
end;

theorem
  'not' p '&' (p => q) = 'not' p 'or' 'not' p '&' q
proof
  p = FALSE or p = TRUE by Def3;
  hence thesis;
end;

theorem
  p <=> q <=> r = p <=> (q <=> r)
proof
  q = FALSE or q = TRUE by Def3;
  hence thesis;
end;

theorem
  p '&' (p <=> q) = p '&' q
proof
  p = FALSE or p = TRUE by Def3;
  hence thesis;
end;

theorem
  'not' p '&' (p <=> q) ='not' p '&' 'not' q
proof
  p = FALSE or p = TRUE by Def3;
  hence thesis;
end;

theorem
  p '&' (q <=> r) = p '&' ('not' q 'or' r) '&' ('not' r 'or' q);

theorem
  p 'or' (q <=> r) = (p 'or' 'not' q 'or' r) '&' (p 'or' 'not' r 'or' q)
proof
  p = FALSE or p = TRUE by Def3;
  hence thesis;
end;

theorem
  'not' p '&' (p <=> q) =('not' p '&' 'not' q) '&' ('not' p 'or' q)
proof
  p = FALSE or p = TRUE by Def3;
  hence thesis;
end;

theorem
  'not' p '&' (q <=> r) = 'not' p '&' ('not' q 'or' r) '&' ('not' r 'or' q);

theorem
  p => (p <=> q) = p => q
proof
  p = FALSE or p = TRUE by Def3;
  hence thesis;
end;

theorem
  p => (p <=> q) = p => (p => q)
proof
  p = FALSE or p = TRUE by Def3;
  hence thesis;
end;

theorem
  p 'or' (p <=> q) = q => p
proof
  p = FALSE or p = TRUE by Def3;
  hence thesis;
end;

theorem
  'not' p 'or' (p <=> q) = p => q
proof
  p = FALSE or p = TRUE by Def3;
  hence thesis;
end;

theorem
  p => (q <=> r) = ('not' p 'or' 'not' q 'or' r) '&' ('not' p 'or' q
  'or' 'not' r)
proof
  p = FALSE or p = TRUE by Def3;
  hence thesis;
end;

theorem
  p 'nor' p = 'not' p;

theorem
  p 'nor' (p '&' q) = 'not' p
proof
  p = FALSE or p = TRUE by Def3;
  hence thesis;
end;

theorem
  p 'nor' (p 'or' q) = 'not' p '&' 'not' q
proof
  p = FALSE or p = TRUE by Def3;
  hence thesis;
end;

theorem
  p 'nor' (p 'nor' q) = 'not' p '&' q
proof
  p = FALSE or p = TRUE by Def3;
  hence thesis;
end;

theorem
  p 'nor' (p '&' q) = 'not' p
proof
  p = FALSE or p = TRUE by Def3;
  hence thesis;
end;

theorem
  p 'nor' (p 'or' q) = p 'nor' q
proof
  p = FALSE or p = TRUE by Def3;
  hence thesis;
end;

theorem
  'not' p '&' (p 'nor' q) = p 'nor' q
proof
  p = FALSE or p = TRUE by Def3;
  hence thesis;
end;

theorem
  p 'or' (q 'nor' r) = (p 'or' 'not' q) '&' (p 'or' 'not' r)
proof
  p = FALSE or p = TRUE by Def3;
  hence thesis;
end;

theorem
  p 'nor' (q 'nor' r) = 'not' p '&' q 'or' 'not' p '&' r
proof
  p = FALSE or p = TRUE by Def3;
  hence thesis;
end;

theorem
  p 'nor' (q '&' r) = 'not' (p 'or' q) 'or' 'not' (p 'or' r)
proof
  p = FALSE or p = TRUE by Def3;
  hence thesis;
end;

theorem
  p '&' (q 'nor' r) = p '&' 'not' q '&' 'not' r
proof
  thus p '&' (q 'nor' r) = p '&' ('not' q '&' 'not' r)
    .= p '&' 'not' q '&' 'not' r;
end;

theorem
  p => (p 'nor' q) = 'not' p
proof
  p = FALSE or p = TRUE by Def3;
  hence thesis;
end;

theorem
  p => (q 'nor' r) = (p => 'not' q) '&' (p => 'not' r)
proof
  p = FALSE or p = TRUE by Def3;
  hence thesis;
end;

theorem
  p 'or' (p 'nor' q) = q => p
proof
  p = FALSE or p = TRUE by Def3;
  hence thesis;
end;

theorem
  p 'or' (q 'nor' r) = (q => p) '&' (r => p)
proof
  p = FALSE or p = TRUE by Def3;
  hence thesis;
end;

theorem
  p => (q 'nor' r) = ('not' p 'or' 'not' q) '&' ('not' p 'or' 'not' r)
proof
  p = FALSE or p = TRUE by Def3;
  hence thesis;
end;

theorem
  p 'nor' (p <=> q) = 'not' p '&' q
proof
  p = FALSE or p = TRUE by Def3;
  hence thesis;
end;

theorem
  'not' p '&' (p <=> q) = p 'nor' q
proof
  p = FALSE or p = TRUE by Def3;
  hence thesis;
end;

theorem
  p 'nor' (q <=> r) = 'not' ((p 'or' 'not' q 'or' r) '&' (p 'or' 'not' r
  'or' q))
proof
  p = FALSE or p = TRUE by Def3;
  hence thesis;
end;

theorem
  p <=> q = p '&' q 'or' (p 'nor' q)
proof
  p = FALSE or p = TRUE by Def3;
  hence thesis;
end;

theorem
  p 'nand' p = 'not' p;

theorem
  p '&' (p 'nand' q) = p '&' 'not' q
proof
  p = FALSE or p = TRUE by Def3;
  hence thesis;
end;

theorem
  p 'nand' (p '&' q) = 'not' (p '&' q)
proof
  p = FALSE or p = TRUE by Def3;
  hence thesis;
end;

theorem
  p 'nand' (q 'nand' r) = ('not' p 'or' q) '&' ('not' p 'or' r)
proof
  p = FALSE or p = TRUE by Def3;
  hence thesis;
end;

theorem
  p 'nand' (q 'or' r) = 'not' (p '&' q) '&' 'not' (p '&' r)
proof
  p = FALSE or p = TRUE by Def3;
  hence thesis;
end;

theorem
  p => (p 'nand' q) = p 'nand' q
proof
  p = FALSE or p = TRUE by Def3;
  hence thesis;
end;

theorem
  p 'nand' (p 'nand' q) = p => q
proof
  p = FALSE or p = TRUE by Def3;
  hence thesis;
end;

theorem
  p 'nand' (q 'nand' r) = (p => q) '&' (p => r)
proof
  p = FALSE or p = TRUE by Def3;
  hence thesis;
end;

theorem
  p 'nand' (p => q) = 'not' (p '&' q)
proof
  p = FALSE or p = TRUE by Def3;
  hence thesis;
end;

theorem
  p 'nand' (q => r) = (p => q) '&' (p => 'not' r)
proof
  p = FALSE or p = TRUE by Def3;
  hence thesis;
end;

theorem
  'not' p 'or' (p 'nand' q) = p 'nand' q
proof
  p = FALSE or p = TRUE by Def3;
  hence thesis;
end;

theorem
  p 'nand' (q => r) = ('not' p 'or' q) '&' ('not' p 'or' 'not' r)
proof
  p = FALSE or p = TRUE by Def3;
  hence thesis;
end;

theorem
  'not' p '&' (p 'nand' q) = 'not' p 'or' 'not' p '&' 'not' q
proof
  p = FALSE or p = TRUE by Def3;
  hence thesis;
end;

theorem
  p '&' (q 'nand' r) = p '&' 'not' q 'or' p '&' 'not' r
proof
  p = FALSE or p = TRUE by Def3;
  hence thesis;
end;

theorem
  p 'nand' (p <=> q) = 'not' (p '&' q)
proof
  p = FALSE or p = TRUE by Def3;
  hence thesis;
end;

::p 'nand' q

theorem
  p 'nand' (q <=> r) = 'not' (p '&' ('not' q 'or' r) '&' ('not' r 'or' q ));

theorem
  p 'nand' (q 'nor' r) = 'not' p 'or' q 'or' r
proof
  thus p 'nand' (q 'nor' r) = 'not' p 'or' (q 'or' r) .= 'not' p 'or' q 'or' r;
end;

theorem
  p '\' q '\' q = p '\' q
proof
  q = FALSE or q = TRUE by Def3;
  hence thesis;
end;

theorem
  p '&' (p '\' q) = p '\' q
proof
  p = FALSE or p = TRUE by Def3;
  hence thesis;
end;

theorem
  p 'nor' (p <=> q) = q '\' p
proof
  p = FALSE or p = TRUE by Def3;
  hence thesis;
end;

theorem
  p 'nor' (p 'nor' q) = q '\' p
proof
  p = FALSE or p = TRUE by Def3;
  hence thesis;
end;

theorem
  p 'xor' (p 'xor' q) = q
proof
  p = FALSE or p = TRUE by Def3;
  hence thesis;
end;

theorem
  (p 'xor' q) 'xor' r = p 'xor' (q 'xor' r)
proof
  q = FALSE or q = TRUE by Def3;
  hence thesis;
end;

theorem
  'not' (p 'xor' q) = 'not' p 'xor' q
proof
  p = FALSE or p = TRUE by Def3;
  hence thesis;
end;

theorem
  p '&' (q 'xor' r) = (p '&' q) 'xor' (p '&' r)
proof
  p = FALSE or p = TRUE by Def3;
  hence thesis;
end;

theorem
  p '&' (p 'xor' q) = p '&' 'not' q
proof
  p = FALSE or p = TRUE by Def3;
  hence thesis;
end;

theorem
  p 'xor' (p '&' q) = p '&' 'not' q
proof
  p = FALSE or p = TRUE by Def3;
  hence thesis;
end;

theorem
  'not' p '&' (p 'xor' q) ='not' p '&' q
proof
  p = FALSE or p = TRUE by Def3;
  hence thesis;
end;

theorem
  p 'or' (p 'xor' q) = p 'or' q
proof
  p = FALSE or p = TRUE by Def3;
  hence thesis;
end;

theorem
  p 'or' ('not' p 'xor' q) =p 'or' 'not' q
proof
  p = FALSE or p = TRUE by Def3;
  hence thesis;
end;

::q => p

theorem
  p 'xor' ('not' p '&' q) = p 'or' q
proof
  p = FALSE or p = TRUE by Def3;
  hence thesis;
end;

theorem
  p 'xor' (p 'or' q) = 'not' p '&' q
proof
  p = FALSE or p = TRUE by Def3;
  hence thesis;
end;

theorem
  p 'xor' (q '&' r) = (p 'or' (q '&' r)) '&' ('not' p 'or' 'not' (q '&' r))
proof
  p = FALSE or p = TRUE by Def3;
  hence thesis;
end;

theorem
  'not' p 'xor' (p => q) = p '&' q
proof
  p = FALSE or p = TRUE by Def3;
  hence thesis;
end;

theorem
  p => (p 'xor' q) = 'not' p 'or' 'not' q
proof
  p = FALSE or p = TRUE by Def3;
  hence thesis;
end;

theorem
  p 'xor' (p => q) = 'not' p 'or' 'not' q
proof
  p = FALSE or p = TRUE by Def3;
  hence thesis;
end;

theorem
  'not' p 'xor' (q => p) = (p '&' (p 'or' 'not' q)) 'or' ('not' p '&' q)
proof
  p = FALSE or p = TRUE by Def3;
  hence thesis;
end;

theorem
  p 'xor' (p <=> q) = 'not' q
proof
  p = FALSE or p = TRUE by Def3;
  hence thesis;
end;

theorem
  'not' p 'xor' (p <=> q) = q
proof
  p = FALSE or p = TRUE by Def3;
  hence thesis;
end;

theorem
  p 'nor' (p 'xor' q) = 'not' p '&' 'not' q
proof
  p = FALSE or p = TRUE by Def3;
  hence thesis;
end;

theorem
  p 'nor' (p 'xor' q) = p 'nor' q
proof
  p = FALSE or p = TRUE by Def3;
  hence thesis;
end;

theorem
  p 'xor' (p 'nor' q) = q => p
proof
  p = FALSE or p = TRUE by Def3;
  hence thesis;
end;

theorem
  p 'nand' (p 'xor' q) = p => q
proof
  p = FALSE or p = TRUE by Def3;
  hence thesis;
end;

theorem
  p 'xor' (p 'nand' q) = p => q
proof
  p = FALSE or p = TRUE by Def3;
  hence thesis;
end;

theorem
  p 'xor' (p => q) = p 'nand' q
proof
  p = FALSE or p = TRUE by Def3;
  hence thesis;
end;

theorem
  p 'nand' (q 'xor' r) = (p '&' q) <=> (p '&' r)
proof
  p = FALSE or p = TRUE by Def3;
  hence thesis;
end;

theorem
  p 'xor' (p '&' q) = p '\' q
proof
  p = FALSE or p = TRUE by Def3;
  hence thesis;
end;

theorem
  p '&' (p 'xor' q) = p '\' q
proof
  p = FALSE or p = TRUE by Def3;
  hence thesis;
end;

theorem
  'not' p '&' (p 'xor' q) = q '\' p
proof
  p = FALSE or p = TRUE by Def3;
  hence thesis;
end;

theorem
  p 'xor' (p 'or' q) = q '\' p
proof
  p = FALSE or p = TRUE by Def3;
  hence thesis;
end;

begin

theorem
  p '&' q = TRUE implies p = TRUE & q = TRUE
proof
  p = FALSE or p = TRUE by Def3;
  hence thesis;
end;

theorem
  'not'(p '&' 'not' p) = TRUE
proof
  p = FALSE or p = TRUE by Def3;
  hence thesis;
end;

theorem
  p => p = TRUE
proof
  p = FALSE or p = TRUE by Def3;
  hence thesis;
end;

theorem
  p => (q => p) = TRUE
proof
  p = FALSE or p = TRUE by Def3;
  hence thesis;
end;

theorem
  p => ((p => q) => q) = TRUE
proof
A1: q = FALSE or q = TRUE by Def3;
  p = FALSE or p = TRUE by Def3;
  hence thesis by A1;
end;

theorem
  (p => q) => ((q => r) => (p => r)) = TRUE
proof
A1: q = FALSE or q = TRUE by Def3;
A2: p = FALSE or p = TRUE by Def3;
  r = FALSE or r = TRUE by Def3;
  hence thesis by A1,A2;
end;

theorem
  (p => q) => ((r => p) => (r => q)) = TRUE
proof
A1: q = FALSE or q = TRUE by Def3;
A2: p = FALSE or p = TRUE by Def3;
  r = FALSE or r = TRUE by Def3;
  hence thesis by A1,A2;
end;

theorem
  (p => (p => q)) => (p => q) = TRUE
proof
A1: q = FALSE or q = TRUE by Def3;
  p = FALSE or p = TRUE by Def3;
  hence thesis by A1;
end;

theorem
  (p => (q => r)) => ((p => q) => (p => r)) = TRUE
proof
A1: q = FALSE or q = TRUE by Def3;
A2: p = FALSE or p = TRUE by Def3;
  r = FALSE or r = TRUE by Def3;
  hence thesis by A1,A2;
end;

theorem
  (p => (q => r)) => (q => (p => r)) = TRUE
proof
A1: q = FALSE or q = TRUE by Def3;
A2: p = FALSE or p = TRUE by Def3;
  r = FALSE or r = TRUE by Def3;
  hence thesis by A1,A2;
end;

theorem
  ((p => q) => r) => (q => r) = TRUE
proof
A1: q = FALSE or q = TRUE by Def3;
  r = FALSE or r = TRUE by Def3;
  hence thesis by A1;
end;

theorem
  (TRUE => p) => p = TRUE
proof
  p = FALSE or p = TRUE by Def3;
  hence thesis;
end;

theorem
  p => q = TRUE implies (q => r) => (p => r) = TRUE
proof
  r = FALSE or r = TRUE by Def3;
  hence thesis;
end;

theorem
  p => (p => q) = TRUE implies p => q = TRUE
proof
  q = FALSE or q = TRUE by Def3;
  hence thesis;
end;

theorem
  p => (q => r) = TRUE implies (p => q) => (p =>r) = TRUE
proof
  p = FALSE or p = TRUE by Def3;
  hence thesis;
end;

theorem
  p => q = TRUE & q => p = TRUE implies p = q
proof
  p = FALSE or p = TRUE by Def3;
  hence thesis;
end;

theorem
  p => q = TRUE & q => r = TRUE implies p => r = TRUE
proof
  p = FALSE or p = TRUE by Def3;
  hence thesis;
end;

theorem
  ('not' p => p) => p = TRUE
proof
  p = FALSE or p = TRUE by Def3;
  hence thesis;
end;

theorem
  'not' p = TRUE implies p => q = TRUE;

theorem
  p => q = TRUE & p => 'not' q = TRUE implies 'not' p = TRUE
proof
  p = FALSE or p = TRUE by Def3;
  hence thesis;
end;

theorem
  (p => q) => ('not' (q '&' r) => 'not' (p '&' r)) = TRUE
proof
A1: q = FALSE or q = TRUE by Def3;
A2: p = FALSE or p = TRUE by Def3;
  r = FALSE or r = TRUE by Def3;
  hence thesis by A1,A2;
end;

theorem
  p 'or' (p => q) = TRUE
proof
  p = FALSE or p = TRUE by Def3;
  hence thesis;
end;

theorem
  p => (p 'or' q) = TRUE
proof
  p = FALSE or p = TRUE by Def3;
  hence thesis;
end;

theorem
  'not' q 'or' (q => p => p) = TRUE
proof
A1: q = FALSE or q = TRUE by Def3;
  p = FALSE or p = TRUE by Def3;
  hence thesis by A1;
end;

theorem
  p <=> p = TRUE
proof
  p = FALSE or p = TRUE by Def3;
  hence thesis;
end;

theorem
  p <=> q <=> r <=> p <=> (q <=> r) = TRUE
proof
A1: q = FALSE or q = TRUE by Def3;
A2: p = FALSE or p = TRUE by Def3;
  r = FALSE or r = TRUE by Def3;
  hence thesis by A1,A2;
end;

theorem
  p <=> q = TRUE & q <=> r = TRUE implies p <=> r = TRUE
proof
  p = FALSE or p = TRUE by Def3;
  hence thesis;
end;

theorem
  p <=> q = TRUE & r <=> s = TRUE implies (p <=> r) <=> (q <=> s) = TRUE
proof
  p = FALSE or p = TRUE by Def3;
  hence thesis;
end;

theorem
  'not' (p <=> 'not' p) = TRUE
proof
  p = FALSE or p = TRUE by Def3;
  hence thesis;
end;

theorem
  p <=> q = TRUE & r <=> s = TRUE implies (p '&' r) <=> (q '&' s) = TRUE
proof
  p = FALSE or p = TRUE by Def3;
  hence thesis;
end;

theorem
  p <=> q = TRUE & r <=> s = TRUE implies (p 'or' r) <=> (q 'or' s) = TRUE
proof
  p = FALSE or p = TRUE by Def3;
  hence thesis;
end;

theorem
  p <=> q = TRUE iff p => q = TRUE & q => p = TRUE
proof
  p = FALSE or p = TRUE by Def3;
  hence thesis;
end;

theorem
  p <=> q = TRUE & r <=> s = TRUE implies (p => r) <=> (q => s) = TRUE
proof
  p = FALSE or p = TRUE by Def3;
  hence thesis;
end;

theorem
  'not' (p 'nor' 'not' p) = TRUE
proof
  p = FALSE or p = TRUE by Def3;
  hence thesis;
end;

theorem
  p 'nand' 'not' p = TRUE
proof
  p = FALSE or p = TRUE by Def3;
  hence thesis;
end;

theorem
  p 'or' (p 'nand' q) = TRUE
proof
  p = FALSE or p = TRUE by Def3;
  hence thesis;
end;

theorem
  p 'nand' (p 'nor' q) = TRUE
proof
  p = FALSE or p = TRUE by Def3;
  hence thesis;
end;

theorem
  p '&' 'not' p = FALSE
proof
  p = FALSE or p = TRUE by Def3;
  hence thesis;
end;

theorem
  p '&' p = FALSE implies p = FALSE;

theorem
  p '&' q = FALSE implies p = FALSE or q = FALSE;

theorem
  'not' (p => p) = FALSE
proof
  p = FALSE or p = TRUE by Def3;
  hence thesis;
end;

theorem
  p <=> 'not' p = FALSE
proof
  p = FALSE or p = TRUE by Def3;
  hence thesis;
end;

theorem
  'not'(p <=> p) = FALSE
proof
  p = FALSE or p = TRUE by Def3;
  hence thesis;
end;

theorem
  p '&' (p 'nor' q) = FALSE
proof
  p = FALSE or p = TRUE by Def3;
  hence thesis;
end;

theorem
  p 'nor' (p => q) = FALSE
proof
  p = FALSE or p = TRUE by Def3;
  hence thesis;
end;

theorem
  p 'nor' (p 'nand' q) = FALSE
proof
  p = FALSE or p = TRUE by Def3;
  hence thesis;
end;

theorem
  p 'xor' p = FALSE
proof
  p = FALSE or p = TRUE by Def3;
  hence thesis;
end;