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