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