:: On the Arithmetic of Boolean Values :: by Library Committee :: :: Received November 30, 2006 :: Copyright (c) 2006-2021 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 :: XBOOLEAN:def 1 0; func TRUE -> object equals :: XBOOLEAN:def 2 1; end; definition let p be object; attr p is boolean means :: XBOOLEAN:def 3 p = FALSE or p = TRUE; end; registration cluster FALSE -> boolean; cluster TRUE -> boolean; cluster boolean for object; cluster boolean -> natural for object; end; reserve p,q,r,s for boolean object; definition let p; func 'not' p -> boolean object equals :: XBOOLEAN:def 4 1 - p; involutiveness; let q; func p '&' q -> object equals :: XBOOLEAN:def 5 p*q; commutativity; idempotence; end; registration let p,q; cluster p '&' q -> boolean; end; definition let p,q; func p 'or' q -> object equals :: XBOOLEAN:def 6 'not' ('not' p '&' 'not' q); commutativity; idempotence; end; definition let p,q; func p => q -> object equals :: XBOOLEAN:def 7 'not' p 'or' q; end; registration let p,q; cluster p 'or' q -> boolean; cluster p => q -> boolean; end; definition let p,q; func p <=> q -> object equals :: XBOOLEAN:def 8 (p => q) '&' (q => p); commutativity; end; registration let p,q; cluster p <=> q -> boolean; end; definition let p,q; func p 'nand' q -> object equals :: XBOOLEAN:def 9 'not'(p '&' q); commutativity; func p 'nor' q -> object equals :: XBOOLEAN:def 10 'not'(p 'or' q); commutativity; func p 'xor' q -> object equals :: XBOOLEAN:def 11 'not'(p <=> q); commutativity; func p '\' q -> object equals :: XBOOLEAN:def 12 p '&' 'not' q; end; registration let p,q; cluster p 'nand' q -> boolean; cluster p 'nor' q -> boolean; cluster p 'xor' q -> boolean; cluster p '\' q -> boolean; end; begin theorem :: XBOOLEAN:1 p '&' p = p; theorem :: XBOOLEAN:2 p '&' (p '&' q) = p '&' q; theorem :: XBOOLEAN:3 p 'or' p = p; theorem :: XBOOLEAN:4 p 'or' (p 'or' q) = p 'or' q; theorem :: XBOOLEAN:5 p 'or' p '&' q = p; theorem :: XBOOLEAN:6 p '&' (p 'or' q) = p; theorem :: XBOOLEAN:7 p '&' (p 'or' q) = p 'or' (p '&' q); theorem :: XBOOLEAN:8 p '&' (q 'or' r) = p '&' q 'or' p '&' r; theorem :: XBOOLEAN:9 p 'or' q '&' r = (p 'or' q) '&' (p 'or' r); theorem :: XBOOLEAN:10 p '&' q 'or' q '&' r 'or' r '&' p = (p 'or' q) '&' (q 'or' r) '&' (r 'or' p); theorem :: XBOOLEAN:11 p '&' ('not' p 'or' q) = p '&' q; theorem :: XBOOLEAN:12 p 'or' 'not' p '&' q = p 'or' q; theorem :: XBOOLEAN:13 p => (p => q) = p => q; theorem :: XBOOLEAN:14 p '&' (p => q) = p '&' q; theorem :: XBOOLEAN:15 p => (p '&' q) = p => q; theorem :: XBOOLEAN:16 p '&' 'not' (p => q) = p '&' 'not' q; theorem :: XBOOLEAN:17 'not' p 'or' (p => q) = p => q; theorem :: XBOOLEAN:18 'not' p '&' (p => q) = 'not' p 'or' 'not' p '&' q; theorem :: XBOOLEAN:19 p <=> q <=> r = p <=> (q <=> r); theorem :: XBOOLEAN:20 p '&' (p <=> q) = p '&' q; theorem :: XBOOLEAN:21 'not' p '&' (p <=> q) ='not' p '&' 'not' q; theorem :: XBOOLEAN:22 p '&' (q <=> r) = p '&' ('not' q 'or' r) '&' ('not' r 'or' q); theorem :: XBOOLEAN:23 p 'or' (q <=> r) = (p 'or' 'not' q 'or' r) '&' (p 'or' 'not' r 'or' q); theorem :: XBOOLEAN:24 'not' p '&' (p <=> q) =('not' p '&' 'not' q) '&' ('not' p 'or' q); theorem :: XBOOLEAN:25 'not' p '&' (q <=> r) = 'not' p '&' ('not' q 'or' r) '&' ('not' r 'or' q); theorem :: XBOOLEAN:26 p => (p <=> q) = p => q; theorem :: XBOOLEAN:27 p => (p <=> q) = p => (p => q); theorem :: XBOOLEAN:28 p 'or' (p <=> q) = q => p; theorem :: XBOOLEAN:29 'not' p 'or' (p <=> q) = p => q; theorem :: XBOOLEAN:30 p => (q <=> r) = ('not' p 'or' 'not' q 'or' r) '&' ('not' p 'or' q 'or' 'not' r); theorem :: XBOOLEAN:31 p 'nor' p = 'not' p; theorem :: XBOOLEAN:32 p 'nor' (p '&' q) = 'not' p; theorem :: XBOOLEAN:33 p 'nor' (p 'or' q) = 'not' p '&' 'not' q; theorem :: XBOOLEAN:34 p 'nor' (p 'nor' q) = 'not' p '&' q; theorem :: XBOOLEAN:35 p 'nor' (p '&' q) = 'not' p; theorem :: XBOOLEAN:36 p 'nor' (p 'or' q) = p 'nor' q; theorem :: XBOOLEAN:37 'not' p '&' (p 'nor' q) = p 'nor' q; theorem :: XBOOLEAN:38 p 'or' (q 'nor' r) = (p 'or' 'not' q) '&' (p 'or' 'not' r); theorem :: XBOOLEAN:39 p 'nor' (q 'nor' r) = 'not' p '&' q 'or' 'not' p '&' r; theorem :: XBOOLEAN:40 p 'nor' (q '&' r) = 'not' (p 'or' q) 'or' 'not' (p 'or' r); theorem :: XBOOLEAN:41 p '&' (q 'nor' r) = p '&' 'not' q '&' 'not' r; theorem :: XBOOLEAN:42 p => (p 'nor' q) = 'not' p; theorem :: XBOOLEAN:43 p => (q 'nor' r) = (p => 'not' q) '&' (p => 'not' r); theorem :: XBOOLEAN:44 p 'or' (p 'nor' q) = q => p; theorem :: XBOOLEAN:45 p 'or' (q 'nor' r) = (q => p) '&' (r => p); theorem :: XBOOLEAN:46 p => (q 'nor' r) = ('not' p 'or' 'not' q) '&' ('not' p 'or' 'not' r); theorem :: XBOOLEAN:47 p 'nor' (p <=> q) = 'not' p '&' q; theorem :: XBOOLEAN:48 'not' p '&' (p <=> q) = p 'nor' q; theorem :: XBOOLEAN:49 p 'nor' (q <=> r) = 'not' ((p 'or' 'not' q 'or' r) '&' (p 'or' 'not' r 'or' q)); theorem :: XBOOLEAN:50 p <=> q = p '&' q 'or' (p 'nor' q); theorem :: XBOOLEAN:51 p 'nand' p = 'not' p; theorem :: XBOOLEAN:52 p '&' (p 'nand' q) = p '&' 'not' q; theorem :: XBOOLEAN:53 p 'nand' (p '&' q) = 'not' (p '&' q); theorem :: XBOOLEAN:54 p 'nand' (q 'nand' r) = ('not' p 'or' q) '&' ('not' p 'or' r); theorem :: XBOOLEAN:55 p 'nand' (q 'or' r) = 'not' (p '&' q) '&' 'not' (p '&' r); theorem :: XBOOLEAN:56 p => (p 'nand' q) = p 'nand' q; theorem :: XBOOLEAN:57 p 'nand' (p 'nand' q) = p => q; theorem :: XBOOLEAN:58 p 'nand' (q 'nand' r) = (p => q) '&' (p => r); theorem :: XBOOLEAN:59 p 'nand' (p => q) = 'not' (p '&' q); theorem :: XBOOLEAN:60 p 'nand' (q => r) = (p => q) '&' (p => 'not' r); theorem :: XBOOLEAN:61 'not' p 'or' (p 'nand' q) = p 'nand' q; theorem :: XBOOLEAN:62 p 'nand' (q => r) = ('not' p 'or' q) '&' ('not' p 'or' 'not' r); theorem :: XBOOLEAN:63 'not' p '&' (p 'nand' q) = 'not' p 'or' 'not' p '&' 'not' q; theorem :: XBOOLEAN:64 p '&' (q 'nand' r) = p '&' 'not' q 'or' p '&' 'not' r; theorem :: XBOOLEAN:65 p 'nand' (p <=> q) = 'not' (p '&' q); ::p 'nand' q theorem :: XBOOLEAN:66 p 'nand' (q <=> r) = 'not' (p '&' ('not' q 'or' r) '&' ('not' r 'or' q )); theorem :: XBOOLEAN:67 p 'nand' (q 'nor' r) = 'not' p 'or' q 'or' r; theorem :: XBOOLEAN:68 p '\' q '\' q = p '\' q; theorem :: XBOOLEAN:69 p '&' (p '\' q) = p '\' q; theorem :: XBOOLEAN:70 p 'nor' (p <=> q) = q '\' p; theorem :: XBOOLEAN:71 p 'nor' (p 'nor' q) = q '\' p; theorem :: XBOOLEAN:72 p 'xor' (p 'xor' q) = q; theorem :: XBOOLEAN:73 (p 'xor' q) 'xor' r = p 'xor' (q 'xor' r); theorem :: XBOOLEAN:74 'not' (p 'xor' q) = 'not' p 'xor' q; theorem :: XBOOLEAN:75 p '&' (q 'xor' r) = (p '&' q) 'xor' (p '&' r); theorem :: XBOOLEAN:76 p '&' (p 'xor' q) = p '&' 'not' q; theorem :: XBOOLEAN:77 p 'xor' (p '&' q) = p '&' 'not' q; theorem :: XBOOLEAN:78 'not' p '&' (p 'xor' q) ='not' p '&' q; theorem :: XBOOLEAN:79 p 'or' (p 'xor' q) = p 'or' q; theorem :: XBOOLEAN:80 p 'or' ('not' p 'xor' q) =p 'or' 'not' q; ::q => p theorem :: XBOOLEAN:81 p 'xor' ('not' p '&' q) = p 'or' q; theorem :: XBOOLEAN:82 p 'xor' (p 'or' q) = 'not' p '&' q; theorem :: XBOOLEAN:83 p 'xor' (q '&' r) = (p 'or' (q '&' r)) '&' ('not' p 'or' 'not' (q '&' r)); theorem :: XBOOLEAN:84 'not' p 'xor' (p => q) = p '&' q; theorem :: XBOOLEAN:85 p => (p 'xor' q) = 'not' p 'or' 'not' q; theorem :: XBOOLEAN:86 p 'xor' (p => q) = 'not' p 'or' 'not' q; theorem :: XBOOLEAN:87 'not' p 'xor' (q => p) = (p '&' (p 'or' 'not' q)) 'or' ('not' p '&' q); theorem :: XBOOLEAN:88 p 'xor' (p <=> q) = 'not' q; theorem :: XBOOLEAN:89 'not' p 'xor' (p <=> q) = q; theorem :: XBOOLEAN:90 p 'nor' (p 'xor' q) = 'not' p '&' 'not' q; theorem :: XBOOLEAN:91 p 'nor' (p 'xor' q) = p 'nor' q; theorem :: XBOOLEAN:92 p 'xor' (p 'nor' q) = q => p; theorem :: XBOOLEAN:93 p 'nand' (p 'xor' q) = p => q; theorem :: XBOOLEAN:94 p 'xor' (p 'nand' q) = p => q; theorem :: XBOOLEAN:95 p 'xor' (p => q) = p 'nand' q; theorem :: XBOOLEAN:96 p 'nand' (q 'xor' r) = (p '&' q) <=> (p '&' r); theorem :: XBOOLEAN:97 p 'xor' (p '&' q) = p '\' q; theorem :: XBOOLEAN:98 p '&' (p 'xor' q) = p '\' q; theorem :: XBOOLEAN:99 'not' p '&' (p 'xor' q) = q '\' p; theorem :: XBOOLEAN:100 p 'xor' (p 'or' q) = q '\' p; begin theorem :: XBOOLEAN:101 p '&' q = TRUE implies p = TRUE & q = TRUE; theorem :: XBOOLEAN:102 'not'(p '&' 'not' p) = TRUE; theorem :: XBOOLEAN:103 p => p = TRUE; theorem :: XBOOLEAN:104 p => (q => p) = TRUE; theorem :: XBOOLEAN:105 p => ((p => q) => q) = TRUE; theorem :: XBOOLEAN:106 (p => q) => ((q => r) => (p => r)) = TRUE; theorem :: XBOOLEAN:107 (p => q) => ((r => p) => (r => q)) = TRUE; theorem :: XBOOLEAN:108 (p => (p => q)) => (p => q) = TRUE; theorem :: XBOOLEAN:109 (p => (q => r)) => ((p => q) => (p => r)) = TRUE; theorem :: XBOOLEAN:110 (p => (q => r)) => (q => (p => r)) = TRUE; theorem :: XBOOLEAN:111 ((p => q) => r) => (q => r) = TRUE; theorem :: XBOOLEAN:112 (TRUE => p) => p = TRUE; theorem :: XBOOLEAN:113 p => q = TRUE implies (q => r) => (p => r) = TRUE; theorem :: XBOOLEAN:114 p => (p => q) = TRUE implies p => q = TRUE; theorem :: XBOOLEAN:115 p => (q => r) = TRUE implies (p => q) => (p =>r) = TRUE; theorem :: XBOOLEAN:116 p => q = TRUE & q => p = TRUE implies p = q; theorem :: XBOOLEAN:117 p => q = TRUE & q => r = TRUE implies p => r = TRUE; theorem :: XBOOLEAN:118 ('not' p => p) => p = TRUE; theorem :: XBOOLEAN:119 'not' p = TRUE implies p => q = TRUE; theorem :: XBOOLEAN:120 p => q = TRUE & p => 'not' q = TRUE implies 'not' p = TRUE; theorem :: XBOOLEAN:121 (p => q) => ('not' (q '&' r) => 'not' (p '&' r)) = TRUE; theorem :: XBOOLEAN:122 p 'or' (p => q) = TRUE; theorem :: XBOOLEAN:123 p => (p 'or' q) = TRUE; theorem :: XBOOLEAN:124 'not' q 'or' (q => p => p) = TRUE; theorem :: XBOOLEAN:125 p <=> p = TRUE; theorem :: XBOOLEAN:126 p <=> q <=> r <=> p <=> (q <=> r) = TRUE; theorem :: XBOOLEAN:127 p <=> q = TRUE & q <=> r = TRUE implies p <=> r = TRUE; theorem :: XBOOLEAN:128 p <=> q = TRUE & r <=> s = TRUE implies (p <=> r) <=> (q <=> s) = TRUE; theorem :: XBOOLEAN:129 'not' (p <=> 'not' p) = TRUE; theorem :: XBOOLEAN:130 p <=> q = TRUE & r <=> s = TRUE implies (p '&' r) <=> (q '&' s) = TRUE; theorem :: XBOOLEAN:131 p <=> q = TRUE & r <=> s = TRUE implies (p 'or' r) <=> (q 'or' s) = TRUE; theorem :: XBOOLEAN:132 p <=> q = TRUE iff p => q = TRUE & q => p = TRUE; theorem :: XBOOLEAN:133 p <=> q = TRUE & r <=> s = TRUE implies (p => r) <=> (q => s) = TRUE; theorem :: XBOOLEAN:134 'not' (p 'nor' 'not' p) = TRUE; theorem :: XBOOLEAN:135 p 'nand' 'not' p = TRUE; theorem :: XBOOLEAN:136 p 'or' (p 'nand' q) = TRUE; theorem :: XBOOLEAN:137 p 'nand' (p 'nor' q) = TRUE; theorem :: XBOOLEAN:138 p '&' 'not' p = FALSE; theorem :: XBOOLEAN:139 p '&' p = FALSE implies p = FALSE; theorem :: XBOOLEAN:140 p '&' q = FALSE implies p = FALSE or q = FALSE; theorem :: XBOOLEAN:141 'not' (p => p) = FALSE; theorem :: XBOOLEAN:142 p <=> 'not' p = FALSE; theorem :: XBOOLEAN:143 'not'(p <=> p) = FALSE; theorem :: XBOOLEAN:144 p '&' (p 'nor' q) = FALSE; theorem :: XBOOLEAN:145 p 'nor' (p => q) = FALSE; theorem :: XBOOLEAN:146 p 'nor' (p 'nand' q) = FALSE; theorem :: XBOOLEAN:147 p 'xor' p = FALSE;