:: On the Arithmetic of Boolean Values
:: by Library Committee
::
:: Received November 30, 2006
:: Copyright (c) 2006-2017 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, BOOLE;
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;