:: XBOOLEAN semantic presentation 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 proof let x be number ; ::_thesis: ( x is boolean implies x is natural ) assume ( x = FALSE or x = TRUE ) ; :: according to XBOOLEAN:def_3 ::_thesis: x is natural hence x is natural ; ::_thesis: verum end; end; definition let p be boolean number ; func 'not' p -> boolean number equals :: XBOOLEAN:def 4 1 - p; coherence 1 - p is boolean number proof ( p = FALSE or p = TRUE ) by Def3; hence 1 - p is boolean number by Def3; ::_thesis: verum end; 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 proof let p be boolean number ; ::_thesis: p = p * p ( p = FALSE or p = TRUE ) by Def3; hence p = p * p ; ::_thesis: verum end; 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 proof ( p = FALSE or p = TRUE ) by Def3; hence p '&' q is boolean ; ::_thesis: verum end; 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 proof let p, q be boolean number ; ::_thesis: p '&' (p '&' q) = p '&' q ( p = FALSE or p = TRUE ) by Def3; hence p '&' (p '&' q) = p '&' q ; ::_thesis: verum end; 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 proof let p, q be boolean number ; ::_thesis: p 'or' (p 'or' q) = p 'or' q ( p = FALSE or p = TRUE ) by Def3; hence p 'or' (p 'or' q) = p 'or' q ; ::_thesis: verum end; theorem :: XBOOLEAN:5 for p, q being boolean number holds p 'or' (p '&' q) = p proof let p, q be boolean number ; ::_thesis: p 'or' (p '&' q) = p ( p = FALSE or p = TRUE ) by Def3; hence p 'or' (p '&' q) = p ; ::_thesis: verum end; theorem :: XBOOLEAN:6 for p, q being boolean number holds p '&' (p 'or' q) = p proof let p, q be boolean number ; ::_thesis: p '&' (p 'or' q) = p ( p = FALSE or p = TRUE ) by Def3; hence p '&' (p 'or' q) = p ; ::_thesis: verum end; theorem :: XBOOLEAN:7 for p, q being boolean number holds p '&' (p 'or' q) = p 'or' (p '&' q) proof let p, q be boolean number ; ::_thesis: p '&' (p 'or' q) = p 'or' (p '&' q) ( p = FALSE or p = TRUE ) by Def3; hence p '&' (p 'or' q) = p 'or' (p '&' q) ; ::_thesis: verum end; theorem :: XBOOLEAN:8 for p, q, r being boolean number holds p '&' (q 'or' r) = (p '&' q) 'or' (p '&' r) proof let p, q, r be boolean number ; ::_thesis: p '&' (q 'or' r) = (p '&' q) 'or' (p '&' r) ( p = FALSE or p = TRUE ) by Def3; hence p '&' (q 'or' r) = (p '&' q) 'or' (p '&' r) ; ::_thesis: verum end; theorem :: XBOOLEAN:9 for p, q, r being boolean number holds p 'or' (q '&' r) = (p 'or' q) '&' (p 'or' r) proof let p, q, r be boolean number ; ::_thesis: p 'or' (q '&' r) = (p 'or' q) '&' (p 'or' r) ( p = FALSE or p = TRUE ) by Def3; hence p 'or' (q '&' r) = (p 'or' q) '&' (p 'or' r) ; ::_thesis: verum end; 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) proof let p, q, r be boolean number ; ::_thesis: ((p '&' q) 'or' (q '&' r)) 'or' (r '&' p) = ((p 'or' q) '&' (q 'or' r)) '&' (r 'or' p) A1: ( q = FALSE or q = TRUE ) by Def3; ( p = FALSE or p = TRUE ) by Def3; hence ((p '&' q) 'or' (q '&' r)) 'or' (r '&' p) = ((p 'or' q) '&' (q 'or' r)) '&' (r 'or' p) by A1; ::_thesis: verum end; theorem :: XBOOLEAN:11 for p, q being boolean number holds p '&' (('not' p) 'or' q) = p '&' q proof let p, q be boolean number ; ::_thesis: p '&' (('not' p) 'or' q) = p '&' q ( p = FALSE or p = TRUE ) by Def3; hence p '&' (('not' p) 'or' q) = p '&' q ; ::_thesis: verum end; theorem :: XBOOLEAN:12 for p, q being boolean number holds p 'or' (('not' p) '&' q) = p 'or' q proof let p, q be boolean number ; ::_thesis: p 'or' (('not' p) '&' q) = p 'or' q ( p = FALSE or p = TRUE ) by Def3; hence p 'or' (('not' p) '&' q) = p 'or' q ; ::_thesis: verum end; theorem :: XBOOLEAN:13 for p, q being boolean number holds p => (p => q) = p => q proof let p, q be boolean number ; ::_thesis: p => (p => q) = p => q ( p = FALSE or p = TRUE ) by Def3; hence p => (p => q) = p => q ; ::_thesis: verum end; theorem :: XBOOLEAN:14 for p, q being boolean number holds p '&' (p => q) = p '&' q proof let p, q be boolean number ; ::_thesis: p '&' (p => q) = p '&' q ( p = FALSE or p = TRUE ) by Def3; hence p '&' (p => q) = p '&' q ; ::_thesis: verum end; theorem :: XBOOLEAN:15 for p, q being boolean number holds p => (p '&' q) = p => q proof let p, q be boolean number ; ::_thesis: p => (p '&' q) = p => q ( p = FALSE or p = TRUE ) by Def3; hence p => (p '&' q) = p => q ; ::_thesis: verum end; theorem :: XBOOLEAN:16 for p, q being boolean number holds p '&' ('not' (p => q)) = p '&' ('not' q) proof let p, q be boolean number ; ::_thesis: p '&' ('not' (p => q)) = p '&' ('not' q) ( p = FALSE or p = TRUE ) by Def3; hence p '&' ('not' (p => q)) = p '&' ('not' q) ; ::_thesis: verum end; theorem :: XBOOLEAN:17 for p, q being boolean number holds ('not' p) 'or' (p => q) = p => q proof let p, q be boolean number ; ::_thesis: ('not' p) 'or' (p => q) = p => q ( p = FALSE or p = TRUE ) by Def3; hence ('not' p) 'or' (p => q) = p => q ; ::_thesis: verum end; theorem :: XBOOLEAN:18 for p, q being boolean number holds ('not' p) '&' (p => q) = ('not' p) 'or' (('not' p) '&' q) proof let p, q be boolean number ; ::_thesis: ('not' p) '&' (p => q) = ('not' p) 'or' (('not' p) '&' q) ( p = FALSE or p = TRUE ) by Def3; hence ('not' p) '&' (p => q) = ('not' p) 'or' (('not' p) '&' q) ; ::_thesis: verum end; theorem :: XBOOLEAN:19 for p, q, r being boolean number holds (p <=> q) <=> r = p <=> (q <=> r) proof let p, q, r be boolean number ; ::_thesis: (p <=> q) <=> r = p <=> (q <=> r) ( q = FALSE or q = TRUE ) by Def3; hence (p <=> q) <=> r = p <=> (q <=> r) ; ::_thesis: verum end; theorem :: XBOOLEAN:20 for p, q being boolean number holds p '&' (p <=> q) = p '&' q proof let p, q be boolean number ; ::_thesis: p '&' (p <=> q) = p '&' q ( p = FALSE or p = TRUE ) by Def3; hence p '&' (p <=> q) = p '&' q ; ::_thesis: verum end; theorem :: XBOOLEAN:21 for p, q being boolean number holds ('not' p) '&' (p <=> q) = ('not' p) '&' ('not' q) proof let p, q be boolean number ; ::_thesis: ('not' p) '&' (p <=> q) = ('not' p) '&' ('not' q) ( p = FALSE or p = TRUE ) by Def3; hence ('not' p) '&' (p <=> q) = ('not' p) '&' ('not' q) ; ::_thesis: verum end; 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) proof let p, q, r be boolean number ; ::_thesis: p 'or' (q <=> r) = ((p 'or' ('not' q)) 'or' r) '&' ((p 'or' ('not' r)) 'or' q) ( p = FALSE or p = TRUE ) by Def3; hence p 'or' (q <=> r) = ((p 'or' ('not' q)) 'or' r) '&' ((p 'or' ('not' r)) 'or' q) ; ::_thesis: verum end; theorem :: XBOOLEAN:24 for p, q being boolean number holds ('not' p) '&' (p <=> q) = (('not' p) '&' ('not' q)) '&' (('not' p) 'or' q) proof let p, q be boolean number ; ::_thesis: ('not' p) '&' (p <=> q) = (('not' p) '&' ('not' q)) '&' (('not' p) 'or' q) ( p = FALSE or p = TRUE ) by Def3; hence ('not' p) '&' (p <=> q) = (('not' p) '&' ('not' q)) '&' (('not' p) 'or' q) ; ::_thesis: verum end; 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 proof let p, q be boolean number ; ::_thesis: p => (p <=> q) = p => q ( p = FALSE or p = TRUE ) by Def3; hence p => (p <=> q) = p => q ; ::_thesis: verum end; theorem :: XBOOLEAN:27 for p, q being boolean number holds p => (p <=> q) = p => (p => q) proof let p, q be boolean number ; ::_thesis: p => (p <=> q) = p => (p => q) ( p = FALSE or p = TRUE ) by Def3; hence p => (p <=> q) = p => (p => q) ; ::_thesis: verum end; theorem :: XBOOLEAN:28 for p, q being boolean number holds p 'or' (p <=> q) = q => p proof let p, q be boolean number ; ::_thesis: p 'or' (p <=> q) = q => p ( p = FALSE or p = TRUE ) by Def3; hence p 'or' (p <=> q) = q => p ; ::_thesis: verum end; theorem :: XBOOLEAN:29 for p, q being boolean number holds ('not' p) 'or' (p <=> q) = p => q proof let p, q be boolean number ; ::_thesis: ('not' p) 'or' (p <=> q) = p => q ( p = FALSE or p = TRUE ) by Def3; hence ('not' p) 'or' (p <=> q) = p => q ; ::_thesis: verum end; 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)) proof let p, q, r be boolean number ; ::_thesis: p => (q <=> r) = ((('not' p) 'or' ('not' q)) 'or' r) '&' ((('not' p) 'or' q) 'or' ('not' r)) ( p = FALSE or p = TRUE ) by Def3; hence p => (q <=> r) = ((('not' p) 'or' ('not' q)) 'or' r) '&' ((('not' p) 'or' q) 'or' ('not' r)) ; ::_thesis: verum end; 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 proof let p, q be boolean number ; ::_thesis: p 'nor' (p '&' q) = 'not' p ( p = FALSE or p = TRUE ) by Def3; hence p 'nor' (p '&' q) = 'not' p ; ::_thesis: verum end; theorem :: XBOOLEAN:33 for p, q being boolean number holds p 'nor' (p 'or' q) = ('not' p) '&' ('not' q) proof let p, q be boolean number ; ::_thesis: p 'nor' (p 'or' q) = ('not' p) '&' ('not' q) ( p = FALSE or p = TRUE ) by Def3; hence p 'nor' (p 'or' q) = ('not' p) '&' ('not' q) ; ::_thesis: verum end; theorem :: XBOOLEAN:34 for p, q being boolean number holds p 'nor' (p 'nor' q) = ('not' p) '&' q proof let p, q be boolean number ; ::_thesis: p 'nor' (p 'nor' q) = ('not' p) '&' q ( p = FALSE or p = TRUE ) by Def3; hence p 'nor' (p 'nor' q) = ('not' p) '&' q ; ::_thesis: verum end; theorem :: XBOOLEAN:35 for p, q being boolean number holds p 'nor' (p '&' q) = 'not' p proof let p, q be boolean number ; ::_thesis: p 'nor' (p '&' q) = 'not' p ( p = FALSE or p = TRUE ) by Def3; hence p 'nor' (p '&' q) = 'not' p ; ::_thesis: verum end; theorem :: XBOOLEAN:36 for p, q being boolean number holds p 'nor' (p 'or' q) = p 'nor' q proof let p, q be boolean number ; ::_thesis: p 'nor' (p 'or' q) = p 'nor' q ( p = FALSE or p = TRUE ) by Def3; hence p 'nor' (p 'or' q) = p 'nor' q ; ::_thesis: verum end; theorem :: XBOOLEAN:37 for p, q being boolean number holds ('not' p) '&' (p 'nor' q) = p 'nor' q proof let p, q be boolean number ; ::_thesis: ('not' p) '&' (p 'nor' q) = p 'nor' q ( p = FALSE or p = TRUE ) by Def3; hence ('not' p) '&' (p 'nor' q) = p 'nor' q ; ::_thesis: verum end; theorem :: XBOOLEAN:38 for p, q, r being boolean number holds p 'or' (q 'nor' r) = (p 'or' ('not' q)) '&' (p 'or' ('not' r)) proof let p, q, r be boolean number ; ::_thesis: p 'or' (q 'nor' r) = (p 'or' ('not' q)) '&' (p 'or' ('not' r)) ( p = FALSE or p = TRUE ) by Def3; hence p 'or' (q 'nor' r) = (p 'or' ('not' q)) '&' (p 'or' ('not' r)) ; ::_thesis: verum end; theorem :: XBOOLEAN:39 for p, q, r being boolean number holds p 'nor' (q 'nor' r) = (('not' p) '&' q) 'or' (('not' p) '&' r) proof let p, q, r be boolean number ; ::_thesis: p 'nor' (q 'nor' r) = (('not' p) '&' q) 'or' (('not' p) '&' r) ( p = FALSE or p = TRUE ) by Def3; hence p 'nor' (q 'nor' r) = (('not' p) '&' q) 'or' (('not' p) '&' r) ; ::_thesis: verum end; theorem :: XBOOLEAN:40 for p, q, r being boolean number holds p 'nor' (q '&' r) = ('not' (p 'or' q)) 'or' ('not' (p 'or' r)) proof let p, q, r be boolean number ; ::_thesis: p 'nor' (q '&' r) = ('not' (p 'or' q)) 'or' ('not' (p 'or' r)) ( p = FALSE or p = TRUE ) by Def3; hence p 'nor' (q '&' r) = ('not' (p 'or' q)) 'or' ('not' (p 'or' r)) ; ::_thesis: verum end; theorem :: XBOOLEAN:41 for p, q, r being boolean number holds p '&' (q 'nor' r) = (p '&' ('not' q)) '&' ('not' r) proof let p, q, r be boolean number ; ::_thesis: p '&' (q 'nor' r) = (p '&' ('not' q)) '&' ('not' r) thus p '&' (q 'nor' r) = p '&' (('not' q) '&' ('not' r)) .= (p '&' ('not' q)) '&' ('not' r) ; ::_thesis: verum end; theorem :: XBOOLEAN:42 for p, q being boolean number holds p => (p 'nor' q) = 'not' p proof let p, q be boolean number ; ::_thesis: p => (p 'nor' q) = 'not' p ( p = FALSE or p = TRUE ) by Def3; hence p => (p 'nor' q) = 'not' p ; ::_thesis: verum end; theorem :: XBOOLEAN:43 for p, q, r being boolean number holds p => (q 'nor' r) = (p => ('not' q)) '&' (p => ('not' r)) proof let p, q, r be boolean number ; ::_thesis: p => (q 'nor' r) = (p => ('not' q)) '&' (p => ('not' r)) ( p = FALSE or p = TRUE ) by Def3; hence p => (q 'nor' r) = (p => ('not' q)) '&' (p => ('not' r)) ; ::_thesis: verum end; theorem :: XBOOLEAN:44 for p, q being boolean number holds p 'or' (p 'nor' q) = q => p proof let p, q be boolean number ; ::_thesis: p 'or' (p 'nor' q) = q => p ( p = FALSE or p = TRUE ) by Def3; hence p 'or' (p 'nor' q) = q => p ; ::_thesis: verum end; theorem :: XBOOLEAN:45 for p, q, r being boolean number holds p 'or' (q 'nor' r) = (q => p) '&' (r => p) proof let p, q, r be boolean number ; ::_thesis: p 'or' (q 'nor' r) = (q => p) '&' (r => p) ( p = FALSE or p = TRUE ) by Def3; hence p 'or' (q 'nor' r) = (q => p) '&' (r => p) ; ::_thesis: verum end; 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)) proof let p, q, r be boolean number ; ::_thesis: p => (q 'nor' r) = (('not' p) 'or' ('not' q)) '&' (('not' p) 'or' ('not' r)) ( p = FALSE or p = TRUE ) by Def3; hence p => (q 'nor' r) = (('not' p) 'or' ('not' q)) '&' (('not' p) 'or' ('not' r)) ; ::_thesis: verum end; theorem :: XBOOLEAN:47 for p, q being boolean number holds p 'nor' (p <=> q) = ('not' p) '&' q proof let p, q be boolean number ; ::_thesis: p 'nor' (p <=> q) = ('not' p) '&' q ( p = FALSE or p = TRUE ) by Def3; hence p 'nor' (p <=> q) = ('not' p) '&' q ; ::_thesis: verum end; theorem :: XBOOLEAN:48 for p, q being boolean number holds ('not' p) '&' (p <=> q) = p 'nor' q proof let p, q be boolean number ; ::_thesis: ('not' p) '&' (p <=> q) = p 'nor' q ( p = FALSE or p = TRUE ) by Def3; hence ('not' p) '&' (p <=> q) = p 'nor' q ; ::_thesis: verum end; 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)) proof let p, q, r be boolean number ; ::_thesis: p 'nor' (q <=> r) = 'not' (((p 'or' ('not' q)) 'or' r) '&' ((p 'or' ('not' r)) 'or' q)) ( p = FALSE or p = TRUE ) by Def3; hence p 'nor' (q <=> r) = 'not' (((p 'or' ('not' q)) 'or' r) '&' ((p 'or' ('not' r)) 'or' q)) ; ::_thesis: verum end; theorem :: XBOOLEAN:50 for p, q being boolean number holds p <=> q = (p '&' q) 'or' (p 'nor' q) proof let p, q be boolean number ; ::_thesis: p <=> q = (p '&' q) 'or' (p 'nor' q) ( p = FALSE or p = TRUE ) by Def3; hence p <=> q = (p '&' q) 'or' (p 'nor' q) ; ::_thesis: verum end; 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) proof let p, q be boolean number ; ::_thesis: p '&' (p 'nand' q) = p '&' ('not' q) ( p = FALSE or p = TRUE ) by Def3; hence p '&' (p 'nand' q) = p '&' ('not' q) ; ::_thesis: verum end; theorem :: XBOOLEAN:53 for p, q being boolean number holds p 'nand' (p '&' q) = 'not' (p '&' q) proof let p, q be boolean number ; ::_thesis: p 'nand' (p '&' q) = 'not' (p '&' q) ( p = FALSE or p = TRUE ) by Def3; hence p 'nand' (p '&' q) = 'not' (p '&' q) ; ::_thesis: verum end; theorem :: XBOOLEAN:54 for p, q, r being boolean number holds p 'nand' (q 'nand' r) = (('not' p) 'or' q) '&' (('not' p) 'or' r) proof let p, q, r be boolean number ; ::_thesis: p 'nand' (q 'nand' r) = (('not' p) 'or' q) '&' (('not' p) 'or' r) ( p = FALSE or p = TRUE ) by Def3; hence p 'nand' (q 'nand' r) = (('not' p) 'or' q) '&' (('not' p) 'or' r) ; ::_thesis: verum end; theorem :: XBOOLEAN:55 for p, q, r being boolean number holds p 'nand' (q 'or' r) = ('not' (p '&' q)) '&' ('not' (p '&' r)) proof let p, q, r be boolean number ; ::_thesis: p 'nand' (q 'or' r) = ('not' (p '&' q)) '&' ('not' (p '&' r)) ( p = FALSE or p = TRUE ) by Def3; hence p 'nand' (q 'or' r) = ('not' (p '&' q)) '&' ('not' (p '&' r)) ; ::_thesis: verum end; theorem :: XBOOLEAN:56 for p, q being boolean number holds p => (p 'nand' q) = p 'nand' q proof let p, q be boolean number ; ::_thesis: p => (p 'nand' q) = p 'nand' q ( p = FALSE or p = TRUE ) by Def3; hence p => (p 'nand' q) = p 'nand' q ; ::_thesis: verum end; theorem :: XBOOLEAN:57 for p, q being boolean number holds p 'nand' (p 'nand' q) = p => q proof let p, q be boolean number ; ::_thesis: p 'nand' (p 'nand' q) = p => q ( p = FALSE or p = TRUE ) by Def3; hence p 'nand' (p 'nand' q) = p => q ; ::_thesis: verum end; theorem :: XBOOLEAN:58 for p, q, r being boolean number holds p 'nand' (q 'nand' r) = (p => q) '&' (p => r) proof let p, q, r be boolean number ; ::_thesis: p 'nand' (q 'nand' r) = (p => q) '&' (p => r) ( p = FALSE or p = TRUE ) by Def3; hence p 'nand' (q 'nand' r) = (p => q) '&' (p => r) ; ::_thesis: verum end; theorem :: XBOOLEAN:59 for p, q being boolean number holds p 'nand' (p => q) = 'not' (p '&' q) proof let p, q be boolean number ; ::_thesis: p 'nand' (p => q) = 'not' (p '&' q) ( p = FALSE or p = TRUE ) by Def3; hence p 'nand' (p => q) = 'not' (p '&' q) ; ::_thesis: verum end; theorem :: XBOOLEAN:60 for p, q, r being boolean number holds p 'nand' (q => r) = (p => q) '&' (p => ('not' r)) proof let p, q, r be boolean number ; ::_thesis: p 'nand' (q => r) = (p => q) '&' (p => ('not' r)) ( p = FALSE or p = TRUE ) by Def3; hence p 'nand' (q => r) = (p => q) '&' (p => ('not' r)) ; ::_thesis: verum end; theorem :: XBOOLEAN:61 for p, q being boolean number holds ('not' p) 'or' (p 'nand' q) = p 'nand' q proof let p, q be boolean number ; ::_thesis: ('not' p) 'or' (p 'nand' q) = p 'nand' q ( p = FALSE or p = TRUE ) by Def3; hence ('not' p) 'or' (p 'nand' q) = p 'nand' q ; ::_thesis: verum end; theorem :: XBOOLEAN:62 for p, q, r being boolean number holds p 'nand' (q => r) = (('not' p) 'or' q) '&' (('not' p) 'or' ('not' r)) proof let p, q, r be boolean number ; ::_thesis: p 'nand' (q => r) = (('not' p) 'or' q) '&' (('not' p) 'or' ('not' r)) ( p = FALSE or p = TRUE ) by Def3; hence p 'nand' (q => r) = (('not' p) 'or' q) '&' (('not' p) 'or' ('not' r)) ; ::_thesis: verum end; theorem :: XBOOLEAN:63 for p, q being boolean number holds ('not' p) '&' (p 'nand' q) = ('not' p) 'or' (('not' p) '&' ('not' q)) proof let p, q be boolean number ; ::_thesis: ('not' p) '&' (p 'nand' q) = ('not' p) 'or' (('not' p) '&' ('not' q)) ( p = FALSE or p = TRUE ) by Def3; hence ('not' p) '&' (p 'nand' q) = ('not' p) 'or' (('not' p) '&' ('not' q)) ; ::_thesis: verum end; theorem :: XBOOLEAN:64 for p, q, r being boolean number holds p '&' (q 'nand' r) = (p '&' ('not' q)) 'or' (p '&' ('not' r)) proof let p, q, r be boolean number ; ::_thesis: p '&' (q 'nand' r) = (p '&' ('not' q)) 'or' (p '&' ('not' r)) ( p = FALSE or p = TRUE ) by Def3; hence p '&' (q 'nand' r) = (p '&' ('not' q)) 'or' (p '&' ('not' r)) ; ::_thesis: verum end; theorem :: XBOOLEAN:65 for p, q being boolean number holds p 'nand' (p <=> q) = 'not' (p '&' q) proof let p, q be boolean number ; ::_thesis: p 'nand' (p <=> q) = 'not' (p '&' q) ( p = FALSE or p = TRUE ) by Def3; hence p 'nand' (p <=> q) = 'not' (p '&' q) ; ::_thesis: verum end; 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 proof let p, q, r be boolean number ; ::_thesis: p 'nand' (q 'nor' r) = (('not' p) 'or' q) 'or' r thus p 'nand' (q 'nor' r) = ('not' p) 'or' (q 'or' r) .= (('not' p) 'or' q) 'or' r ; ::_thesis: verum end; theorem :: XBOOLEAN:68 for p, q being boolean number holds (p '\' q) '\' q = p '\' q proof let p, q be boolean number ; ::_thesis: (p '\' q) '\' q = p '\' q ( q = FALSE or q = TRUE ) by Def3; hence (p '\' q) '\' q = p '\' q ; ::_thesis: verum end; theorem :: XBOOLEAN:69 for p, q being boolean number holds p '&' (p '\' q) = p '\' q proof let p, q be boolean number ; ::_thesis: p '&' (p '\' q) = p '\' q ( p = FALSE or p = TRUE ) by Def3; hence p '&' (p '\' q) = p '\' q ; ::_thesis: verum end; theorem :: XBOOLEAN:70 for p, q being boolean number holds p 'nor' (p <=> q) = q '\' p proof let p, q be boolean number ; ::_thesis: p 'nor' (p <=> q) = q '\' p ( p = FALSE or p = TRUE ) by Def3; hence p 'nor' (p <=> q) = q '\' p ; ::_thesis: verum end; theorem :: XBOOLEAN:71 for p, q being boolean number holds p 'nor' (p 'nor' q) = q '\' p proof let p, q be boolean number ; ::_thesis: p 'nor' (p 'nor' q) = q '\' p ( p = FALSE or p = TRUE ) by Def3; hence p 'nor' (p 'nor' q) = q '\' p ; ::_thesis: verum end; theorem :: XBOOLEAN:72 for p, q being boolean number holds p 'xor' (p 'xor' q) = q proof let p, q be boolean number ; ::_thesis: p 'xor' (p 'xor' q) = q ( p = FALSE or p = TRUE ) by Def3; hence p 'xor' (p 'xor' q) = q ; ::_thesis: verum end; theorem :: XBOOLEAN:73 for p, q, r being boolean number holds (p 'xor' q) 'xor' r = p 'xor' (q 'xor' r) proof let p, q, r be boolean number ; ::_thesis: (p 'xor' q) 'xor' r = p 'xor' (q 'xor' r) ( q = FALSE or q = TRUE ) by Def3; hence (p 'xor' q) 'xor' r = p 'xor' (q 'xor' r) ; ::_thesis: verum end; theorem :: XBOOLEAN:74 for p, q being boolean number holds 'not' (p 'xor' q) = ('not' p) 'xor' q proof let p, q be boolean number ; ::_thesis: 'not' (p 'xor' q) = ('not' p) 'xor' q ( p = FALSE or p = TRUE ) by Def3; hence 'not' (p 'xor' q) = ('not' p) 'xor' q ; ::_thesis: verum end; theorem :: XBOOLEAN:75 for p, q, r being boolean number holds p '&' (q 'xor' r) = (p '&' q) 'xor' (p '&' r) proof let p, q, r be boolean number ; ::_thesis: p '&' (q 'xor' r) = (p '&' q) 'xor' (p '&' r) ( p = FALSE or p = TRUE ) by Def3; hence p '&' (q 'xor' r) = (p '&' q) 'xor' (p '&' r) ; ::_thesis: verum end; theorem :: XBOOLEAN:76 for p, q being boolean number holds p '&' (p 'xor' q) = p '&' ('not' q) proof let p, q be boolean number ; ::_thesis: p '&' (p 'xor' q) = p '&' ('not' q) ( p = FALSE or p = TRUE ) by Def3; hence p '&' (p 'xor' q) = p '&' ('not' q) ; ::_thesis: verum end; theorem :: XBOOLEAN:77 for p, q being boolean number holds p 'xor' (p '&' q) = p '&' ('not' q) proof let p, q be boolean number ; ::_thesis: p 'xor' (p '&' q) = p '&' ('not' q) ( p = FALSE or p = TRUE ) by Def3; hence p 'xor' (p '&' q) = p '&' ('not' q) ; ::_thesis: verum end; theorem :: XBOOLEAN:78 for p, q being boolean number holds ('not' p) '&' (p 'xor' q) = ('not' p) '&' q proof let p, q be boolean number ; ::_thesis: ('not' p) '&' (p 'xor' q) = ('not' p) '&' q ( p = FALSE or p = TRUE ) by Def3; hence ('not' p) '&' (p 'xor' q) = ('not' p) '&' q ; ::_thesis: verum end; theorem :: XBOOLEAN:79 for p, q being boolean number holds p 'or' (p 'xor' q) = p 'or' q proof let p, q be boolean number ; ::_thesis: p 'or' (p 'xor' q) = p 'or' q ( p = FALSE or p = TRUE ) by Def3; hence p 'or' (p 'xor' q) = p 'or' q ; ::_thesis: verum end; theorem :: XBOOLEAN:80 for p, q being boolean number holds p 'or' (('not' p) 'xor' q) = p 'or' ('not' q) proof let p, q be boolean number ; ::_thesis: p 'or' (('not' p) 'xor' q) = p 'or' ('not' q) ( p = FALSE or p = TRUE ) by Def3; hence p 'or' (('not' p) 'xor' q) = p 'or' ('not' q) ; ::_thesis: verum end; theorem :: XBOOLEAN:81 for p, q being boolean number holds p 'xor' (('not' p) '&' q) = p 'or' q proof let p, q be boolean number ; ::_thesis: p 'xor' (('not' p) '&' q) = p 'or' q ( p = FALSE or p = TRUE ) by Def3; hence p 'xor' (('not' p) '&' q) = p 'or' q ; ::_thesis: verum end; theorem :: XBOOLEAN:82 for p, q being boolean number holds p 'xor' (p 'or' q) = ('not' p) '&' q proof let p, q be boolean number ; ::_thesis: p 'xor' (p 'or' q) = ('not' p) '&' q ( p = FALSE or p = TRUE ) by Def3; hence p 'xor' (p 'or' q) = ('not' p) '&' q ; ::_thesis: verum end; 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))) proof let p, q, r be boolean number ; ::_thesis: p 'xor' (q '&' r) = (p 'or' (q '&' r)) '&' (('not' p) 'or' ('not' (q '&' r))) ( p = FALSE or p = TRUE ) by Def3; hence p 'xor' (q '&' r) = (p 'or' (q '&' r)) '&' (('not' p) 'or' ('not' (q '&' r))) ; ::_thesis: verum end; theorem :: XBOOLEAN:84 for p, q being boolean number holds ('not' p) 'xor' (p => q) = p '&' q proof let p, q be boolean number ; ::_thesis: ('not' p) 'xor' (p => q) = p '&' q ( p = FALSE or p = TRUE ) by Def3; hence ('not' p) 'xor' (p => q) = p '&' q ; ::_thesis: verum end; theorem :: XBOOLEAN:85 for p, q being boolean number holds p => (p 'xor' q) = ('not' p) 'or' ('not' q) proof let p, q be boolean number ; ::_thesis: p => (p 'xor' q) = ('not' p) 'or' ('not' q) ( p = FALSE or p = TRUE ) by Def3; hence p => (p 'xor' q) = ('not' p) 'or' ('not' q) ; ::_thesis: verum end; theorem :: XBOOLEAN:86 for p, q being boolean number holds p 'xor' (p => q) = ('not' p) 'or' ('not' q) proof let p, q be boolean number ; ::_thesis: p 'xor' (p => q) = ('not' p) 'or' ('not' q) ( p = FALSE or p = TRUE ) by Def3; hence p 'xor' (p => q) = ('not' p) 'or' ('not' q) ; ::_thesis: verum end; theorem :: XBOOLEAN:87 for p, q being boolean number holds ('not' p) 'xor' (q => p) = (p '&' (p 'or' ('not' q))) 'or' (('not' p) '&' q) proof let p, q be boolean number ; ::_thesis: ('not' p) 'xor' (q => p) = (p '&' (p 'or' ('not' q))) 'or' (('not' p) '&' q) ( p = FALSE or p = TRUE ) by Def3; hence ('not' p) 'xor' (q => p) = (p '&' (p 'or' ('not' q))) 'or' (('not' p) '&' q) ; ::_thesis: verum end; theorem :: XBOOLEAN:88 for p, q being boolean number holds p 'xor' (p <=> q) = 'not' q proof let p, q be boolean number ; ::_thesis: p 'xor' (p <=> q) = 'not' q ( p = FALSE or p = TRUE ) by Def3; hence p 'xor' (p <=> q) = 'not' q ; ::_thesis: verum end; theorem :: XBOOLEAN:89 for p, q being boolean number holds ('not' p) 'xor' (p <=> q) = q proof let p, q be boolean number ; ::_thesis: ('not' p) 'xor' (p <=> q) = q ( p = FALSE or p = TRUE ) by Def3; hence ('not' p) 'xor' (p <=> q) = q ; ::_thesis: verum end; theorem :: XBOOLEAN:90 for p, q being boolean number holds p 'nor' (p 'xor' q) = ('not' p) '&' ('not' q) proof let p, q be boolean number ; ::_thesis: p 'nor' (p 'xor' q) = ('not' p) '&' ('not' q) ( p = FALSE or p = TRUE ) by Def3; hence p 'nor' (p 'xor' q) = ('not' p) '&' ('not' q) ; ::_thesis: verum end; theorem :: XBOOLEAN:91 for p, q being boolean number holds p 'nor' (p 'xor' q) = p 'nor' q proof let p, q be boolean number ; ::_thesis: p 'nor' (p 'xor' q) = p 'nor' q ( p = FALSE or p = TRUE ) by Def3; hence p 'nor' (p 'xor' q) = p 'nor' q ; ::_thesis: verum end; theorem :: XBOOLEAN:92 for p, q being boolean number holds p 'xor' (p 'nor' q) = q => p proof let p, q be boolean number ; ::_thesis: p 'xor' (p 'nor' q) = q => p ( p = FALSE or p = TRUE ) by Def3; hence p 'xor' (p 'nor' q) = q => p ; ::_thesis: verum end; theorem :: XBOOLEAN:93 for p, q being boolean number holds p 'nand' (p 'xor' q) = p => q proof let p, q be boolean number ; ::_thesis: p 'nand' (p 'xor' q) = p => q ( p = FALSE or p = TRUE ) by Def3; hence p 'nand' (p 'xor' q) = p => q ; ::_thesis: verum end; theorem :: XBOOLEAN:94 for p, q being boolean number holds p 'xor' (p 'nand' q) = p => q proof let p, q be boolean number ; ::_thesis: p 'xor' (p 'nand' q) = p => q ( p = FALSE or p = TRUE ) by Def3; hence p 'xor' (p 'nand' q) = p => q ; ::_thesis: verum end; theorem :: XBOOLEAN:95 for p, q being boolean number holds p 'xor' (p => q) = p 'nand' q proof let p, q be boolean number ; ::_thesis: p 'xor' (p => q) = p 'nand' q ( p = FALSE or p = TRUE ) by Def3; hence p 'xor' (p => q) = p 'nand' q ; ::_thesis: verum end; theorem :: XBOOLEAN:96 for p, q, r being boolean number holds p 'nand' (q 'xor' r) = (p '&' q) <=> (p '&' r) proof let p, q, r be boolean number ; ::_thesis: p 'nand' (q 'xor' r) = (p '&' q) <=> (p '&' r) ( p = FALSE or p = TRUE ) by Def3; hence p 'nand' (q 'xor' r) = (p '&' q) <=> (p '&' r) ; ::_thesis: verum end; theorem :: XBOOLEAN:97 for p, q being boolean number holds p 'xor' (p '&' q) = p '\' q proof let p, q be boolean number ; ::_thesis: p 'xor' (p '&' q) = p '\' q ( p = FALSE or p = TRUE ) by Def3; hence p 'xor' (p '&' q) = p '\' q ; ::_thesis: verum end; theorem :: XBOOLEAN:98 for p, q being boolean number holds p '&' (p 'xor' q) = p '\' q proof let p, q be boolean number ; ::_thesis: p '&' (p 'xor' q) = p '\' q ( p = FALSE or p = TRUE ) by Def3; hence p '&' (p 'xor' q) = p '\' q ; ::_thesis: verum end; theorem :: XBOOLEAN:99 for p, q being boolean number holds ('not' p) '&' (p 'xor' q) = q '\' p proof let p, q be boolean number ; ::_thesis: ('not' p) '&' (p 'xor' q) = q '\' p ( p = FALSE or p = TRUE ) by Def3; hence ('not' p) '&' (p 'xor' q) = q '\' p ; ::_thesis: verum end; theorem :: XBOOLEAN:100 for p, q being boolean number holds p 'xor' (p 'or' q) = q '\' p proof let p, q be boolean number ; ::_thesis: p 'xor' (p 'or' q) = q '\' p ( p = FALSE or p = TRUE ) by Def3; hence p 'xor' (p 'or' q) = q '\' p ; ::_thesis: verum end; begin theorem :: XBOOLEAN:101 for p, q being boolean number st p '&' q = TRUE holds ( p = TRUE & q = TRUE ) proof let p, q be boolean number ; ::_thesis: ( p '&' q = TRUE implies ( p = TRUE & q = TRUE ) ) ( p = FALSE or p = TRUE ) by Def3; hence ( p '&' q = TRUE implies ( p = TRUE & q = TRUE ) ) ; ::_thesis: verum end; theorem :: XBOOLEAN:102 for p being boolean number holds 'not' (p '&' ('not' p)) = TRUE proof let p be boolean number ; ::_thesis: 'not' (p '&' ('not' p)) = TRUE ( p = FALSE or p = TRUE ) by Def3; hence 'not' (p '&' ('not' p)) = TRUE ; ::_thesis: verum end; theorem :: XBOOLEAN:103 for p being boolean number holds p => p = TRUE proof let p be boolean number ; ::_thesis: p => p = TRUE ( p = FALSE or p = TRUE ) by Def3; hence p => p = TRUE ; ::_thesis: verum end; theorem :: XBOOLEAN:104 for p, q being boolean number holds p => (q => p) = TRUE proof let p, q be boolean number ; ::_thesis: p => (q => p) = TRUE ( p = FALSE or p = TRUE ) by Def3; hence p => (q => p) = TRUE ; ::_thesis: verum end; theorem :: XBOOLEAN:105 for p, q being boolean number holds p => ((p => q) => q) = TRUE proof let p, q be boolean number ; ::_thesis: p => ((p => q) => q) = TRUE A1: ( q = FALSE or q = TRUE ) by Def3; ( p = FALSE or p = TRUE ) by Def3; hence p => ((p => q) => q) = TRUE by A1; ::_thesis: verum end; theorem :: XBOOLEAN:106 for p, q, r being boolean number holds (p => q) => ((q => r) => (p => r)) = TRUE proof let p, q, r be boolean number ; ::_thesis: (p => q) => ((q => r) => (p => r)) = TRUE A1: ( q = FALSE or q = TRUE ) by Def3; A2: ( p = FALSE or p = TRUE ) by Def3; ( r = FALSE or r = TRUE ) by Def3; hence (p => q) => ((q => r) => (p => r)) = TRUE by A1, A2; ::_thesis: verum end; theorem :: XBOOLEAN:107 for p, q, r being boolean number holds (p => q) => ((r => p) => (r => q)) = TRUE proof let p, q, r be boolean number ; ::_thesis: (p => q) => ((r => p) => (r => q)) = TRUE A1: ( q = FALSE or q = TRUE ) by Def3; A2: ( p = FALSE or p = TRUE ) by Def3; ( r = FALSE or r = TRUE ) by Def3; hence (p => q) => ((r => p) => (r => q)) = TRUE by A1, A2; ::_thesis: verum end; theorem :: XBOOLEAN:108 for p, q being boolean number holds (p => (p => q)) => (p => q) = TRUE proof let p, q be boolean number ; ::_thesis: (p => (p => q)) => (p => q) = TRUE A1: ( q = FALSE or q = TRUE ) by Def3; ( p = FALSE or p = TRUE ) by Def3; hence (p => (p => q)) => (p => q) = TRUE by A1; ::_thesis: verum end; theorem :: XBOOLEAN:109 for p, q, r being boolean number holds (p => (q => r)) => ((p => q) => (p => r)) = TRUE proof let p, q, r be boolean number ; ::_thesis: (p => (q => r)) => ((p => q) => (p => r)) = TRUE A1: ( q = FALSE or q = TRUE ) by Def3; A2: ( p = FALSE or p = TRUE ) by Def3; ( r = FALSE or r = TRUE ) by Def3; hence (p => (q => r)) => ((p => q) => (p => r)) = TRUE by A1, A2; ::_thesis: verum end; theorem :: XBOOLEAN:110 for p, q, r being boolean number holds (p => (q => r)) => (q => (p => r)) = TRUE proof let p, q, r be boolean number ; ::_thesis: (p => (q => r)) => (q => (p => r)) = TRUE A1: ( q = FALSE or q = TRUE ) by Def3; A2: ( p = FALSE or p = TRUE ) by Def3; ( r = FALSE or r = TRUE ) by Def3; hence (p => (q => r)) => (q => (p => r)) = TRUE by A1, A2; ::_thesis: verum end; theorem :: XBOOLEAN:111 for p, q, r being boolean number holds ((p => q) => r) => (q => r) = TRUE proof let p, q, r be boolean number ; ::_thesis: ((p => q) => r) => (q => r) = TRUE A1: ( q = FALSE or q = TRUE ) by Def3; ( r = FALSE or r = TRUE ) by Def3; hence ((p => q) => r) => (q => r) = TRUE by A1; ::_thesis: verum end; theorem :: XBOOLEAN:112 for p being boolean number holds (TRUE => p) => p = TRUE proof let p be boolean number ; ::_thesis: (TRUE => p) => p = TRUE ( p = FALSE or p = TRUE ) by Def3; hence (TRUE => p) => p = TRUE ; ::_thesis: verum end; theorem :: XBOOLEAN:113 for p, q, r being boolean number st p => q = TRUE holds (q => r) => (p => r) = TRUE proof let p, q, r be boolean number ; ::_thesis: ( p => q = TRUE implies (q => r) => (p => r) = TRUE ) ( r = FALSE or r = TRUE ) by Def3; hence ( p => q = TRUE implies (q => r) => (p => r) = TRUE ) ; ::_thesis: verum end; theorem :: XBOOLEAN:114 for p, q being boolean number st p => (p => q) = TRUE holds p => q = TRUE proof let p, q be boolean number ; ::_thesis: ( p => (p => q) = TRUE implies p => q = TRUE ) ( q = FALSE or q = TRUE ) by Def3; hence ( p => (p => q) = TRUE implies p => q = TRUE ) ; ::_thesis: verum end; theorem :: XBOOLEAN:115 for p, q, r being boolean number st p => (q => r) = TRUE holds (p => q) => (p => r) = TRUE proof let p, q, r be boolean number ; ::_thesis: ( p => (q => r) = TRUE implies (p => q) => (p => r) = TRUE ) ( p = FALSE or p = TRUE ) by Def3; hence ( p => (q => r) = TRUE implies (p => q) => (p => r) = TRUE ) ; ::_thesis: verum end; theorem :: XBOOLEAN:116 for p, q being boolean number st p => q = TRUE & q => p = TRUE holds p = q proof let p, q be boolean number ; ::_thesis: ( p => q = TRUE & q => p = TRUE implies p = q ) ( p = FALSE or p = TRUE ) by Def3; hence ( p => q = TRUE & q => p = TRUE implies p = q ) ; ::_thesis: verum end; theorem :: XBOOLEAN:117 for p, q, r being boolean number st p => q = TRUE & q => r = TRUE holds p => r = TRUE proof let p, q, r be boolean number ; ::_thesis: ( p => q = TRUE & q => r = TRUE implies p => r = TRUE ) ( p = FALSE or p = TRUE ) by Def3; hence ( p => q = TRUE & q => r = TRUE implies p => r = TRUE ) ; ::_thesis: verum end; theorem :: XBOOLEAN:118 for p being boolean number holds (('not' p) => p) => p = TRUE proof let p be boolean number ; ::_thesis: (('not' p) => p) => p = TRUE ( p = FALSE or p = TRUE ) by Def3; hence (('not' p) => p) => p = TRUE ; ::_thesis: verum end; 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 proof let p, q be boolean number ; ::_thesis: ( p => q = TRUE & p => ('not' q) = TRUE implies 'not' p = TRUE ) ( p = FALSE or p = TRUE ) by Def3; hence ( p => q = TRUE & p => ('not' q) = TRUE implies 'not' p = TRUE ) ; ::_thesis: verum end; theorem :: XBOOLEAN:121 for p, q, r being boolean number holds (p => q) => (('not' (q '&' r)) => ('not' (p '&' r))) = TRUE proof let p, q, r be boolean number ; ::_thesis: (p => q) => (('not' (q '&' r)) => ('not' (p '&' r))) = TRUE A1: ( q = FALSE or q = TRUE ) by Def3; A2: ( p = FALSE or p = TRUE ) by Def3; ( r = FALSE or r = TRUE ) by Def3; hence (p => q) => (('not' (q '&' r)) => ('not' (p '&' r))) = TRUE by A1, A2; ::_thesis: verum end; theorem :: XBOOLEAN:122 for p, q being boolean number holds p 'or' (p => q) = TRUE proof let p, q be boolean number ; ::_thesis: p 'or' (p => q) = TRUE ( p = FALSE or p = TRUE ) by Def3; hence p 'or' (p => q) = TRUE ; ::_thesis: verum end; theorem :: XBOOLEAN:123 for p, q being boolean number holds p => (p 'or' q) = TRUE proof let p, q be boolean number ; ::_thesis: p => (p 'or' q) = TRUE ( p = FALSE or p = TRUE ) by Def3; hence p => (p 'or' q) = TRUE ; ::_thesis: verum end; theorem :: XBOOLEAN:124 for q, p being boolean number holds ('not' q) 'or' ((q => p) => p) = TRUE proof let q, p be boolean number ; ::_thesis: ('not' q) 'or' ((q => p) => p) = TRUE A1: ( q = FALSE or q = TRUE ) by Def3; ( p = FALSE or p = TRUE ) by Def3; hence ('not' q) 'or' ((q => p) => p) = TRUE by A1; ::_thesis: verum end; theorem :: XBOOLEAN:125 for p being boolean number holds p <=> p = TRUE proof let p be boolean number ; ::_thesis: p <=> p = TRUE ( p = FALSE or p = TRUE ) by Def3; hence p <=> p = TRUE ; ::_thesis: verum end; theorem :: XBOOLEAN:126 for p, q, r being boolean number holds (((p <=> q) <=> r) <=> p) <=> (q <=> r) = TRUE proof let p, q, r be boolean number ; ::_thesis: (((p <=> q) <=> r) <=> p) <=> (q <=> r) = TRUE A1: ( q = FALSE or q = TRUE ) by Def3; A2: ( p = FALSE or p = TRUE ) by Def3; ( r = FALSE or r = TRUE ) by Def3; hence (((p <=> q) <=> r) <=> p) <=> (q <=> r) = TRUE by A1, A2; ::_thesis: verum end; theorem :: XBOOLEAN:127 for p, q, r being boolean number st p <=> q = TRUE & q <=> r = TRUE holds p <=> r = TRUE proof let p, q, r be boolean number ; ::_thesis: ( p <=> q = TRUE & q <=> r = TRUE implies p <=> r = TRUE ) ( p = FALSE or p = TRUE ) by Def3; hence ( p <=> q = TRUE & q <=> r = TRUE implies p <=> r = TRUE ) ; ::_thesis: verum end; theorem :: XBOOLEAN:128 for p, q, r, s being boolean number st p <=> q = TRUE & r <=> s = TRUE holds (p <=> r) <=> (q <=> s) = TRUE proof let p, q, r, s be boolean number ; ::_thesis: ( p <=> q = TRUE & r <=> s = TRUE implies (p <=> r) <=> (q <=> s) = TRUE ) ( p = FALSE or p = TRUE ) by Def3; hence ( p <=> q = TRUE & r <=> s = TRUE implies (p <=> r) <=> (q <=> s) = TRUE ) ; ::_thesis: verum end; theorem :: XBOOLEAN:129 for p being boolean number holds 'not' (p <=> ('not' p)) = TRUE proof let p be boolean number ; ::_thesis: 'not' (p <=> ('not' p)) = TRUE ( p = FALSE or p = TRUE ) by Def3; hence 'not' (p <=> ('not' p)) = TRUE ; ::_thesis: verum end; theorem :: XBOOLEAN:130 for p, q, r, s being boolean number st p <=> q = TRUE & r <=> s = TRUE holds (p '&' r) <=> (q '&' s) = TRUE proof let p, q, r, s be boolean number ; ::_thesis: ( p <=> q = TRUE & r <=> s = TRUE implies (p '&' r) <=> (q '&' s) = TRUE ) ( p = FALSE or p = TRUE ) by Def3; hence ( p <=> q = TRUE & r <=> s = TRUE implies (p '&' r) <=> (q '&' s) = TRUE ) ; ::_thesis: verum end; 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 proof let p, q, r, s be boolean number ; ::_thesis: ( p <=> q = TRUE & r <=> s = TRUE implies (p 'or' r) <=> (q 'or' s) = TRUE ) ( p = FALSE or p = TRUE ) by Def3; hence ( p <=> q = TRUE & r <=> s = TRUE implies (p 'or' r) <=> (q 'or' s) = TRUE ) ; ::_thesis: verum end; theorem :: XBOOLEAN:132 for p, q being boolean number holds ( p <=> q = TRUE iff ( p => q = TRUE & q => p = TRUE ) ) proof let p, q be boolean number ; ::_thesis: ( p <=> q = TRUE iff ( p => q = TRUE & q => p = TRUE ) ) ( p = FALSE or p = TRUE ) by Def3; hence ( p <=> q = TRUE iff ( p => q = TRUE & q => p = TRUE ) ) ; ::_thesis: verum end; theorem :: XBOOLEAN:133 for p, q, r, s being boolean number st p <=> q = TRUE & r <=> s = TRUE holds (p => r) <=> (q => s) = TRUE proof let p, q, r, s be boolean number ; ::_thesis: ( p <=> q = TRUE & r <=> s = TRUE implies (p => r) <=> (q => s) = TRUE ) ( p = FALSE or p = TRUE ) by Def3; hence ( p <=> q = TRUE & r <=> s = TRUE implies (p => r) <=> (q => s) = TRUE ) ; ::_thesis: verum end; theorem :: XBOOLEAN:134 for p being boolean number holds 'not' (p 'nor' ('not' p)) = TRUE proof let p be boolean number ; ::_thesis: 'not' (p 'nor' ('not' p)) = TRUE ( p = FALSE or p = TRUE ) by Def3; hence 'not' (p 'nor' ('not' p)) = TRUE ; ::_thesis: verum end; theorem :: XBOOLEAN:135 for p being boolean number holds p 'nand' ('not' p) = TRUE proof let p be boolean number ; ::_thesis: p 'nand' ('not' p) = TRUE ( p = FALSE or p = TRUE ) by Def3; hence p 'nand' ('not' p) = TRUE ; ::_thesis: verum end; theorem :: XBOOLEAN:136 for p, q being boolean number holds p 'or' (p 'nand' q) = TRUE proof let p, q be boolean number ; ::_thesis: p 'or' (p 'nand' q) = TRUE ( p = FALSE or p = TRUE ) by Def3; hence p 'or' (p 'nand' q) = TRUE ; ::_thesis: verum end; theorem :: XBOOLEAN:137 for p, q being boolean number holds p 'nand' (p 'nor' q) = TRUE proof let p, q be boolean number ; ::_thesis: p 'nand' (p 'nor' q) = TRUE ( p = FALSE or p = TRUE ) by Def3; hence p 'nand' (p 'nor' q) = TRUE ; ::_thesis: verum end; theorem :: XBOOLEAN:138 for p being boolean number holds p '&' ('not' p) = FALSE proof let p be boolean number ; ::_thesis: p '&' ('not' p) = FALSE ( p = FALSE or p = TRUE ) by Def3; hence p '&' ('not' p) = FALSE ; ::_thesis: verum end; 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 ) proof let p, q be boolean number ; ::_thesis: ( not p '&' q = FALSE or p = FALSE or q = FALSE ) ( p = FALSE or p = TRUE ) by Def3; hence ( not p '&' q = FALSE or p = FALSE or q = FALSE ) ; ::_thesis: verum end; theorem :: XBOOLEAN:141 for p being boolean number holds 'not' (p => p) = FALSE proof let p be boolean number ; ::_thesis: 'not' (p => p) = FALSE ( p = FALSE or p = TRUE ) by Def3; hence 'not' (p => p) = FALSE ; ::_thesis: verum end; theorem :: XBOOLEAN:142 for p being boolean number holds p <=> ('not' p) = FALSE proof let p be boolean number ; ::_thesis: p <=> ('not' p) = FALSE ( p = FALSE or p = TRUE ) by Def3; hence p <=> ('not' p) = FALSE ; ::_thesis: verum end; theorem :: XBOOLEAN:143 for p being boolean number holds 'not' (p <=> p) = FALSE proof let p be boolean number ; ::_thesis: 'not' (p <=> p) = FALSE ( p = FALSE or p = TRUE ) by Def3; hence 'not' (p <=> p) = FALSE ; ::_thesis: verum end; theorem :: XBOOLEAN:144 for p, q being boolean number holds p '&' (p 'nor' q) = FALSE proof let p, q be boolean number ; ::_thesis: p '&' (p 'nor' q) = FALSE ( p = FALSE or p = TRUE ) by Def3; hence p '&' (p 'nor' q) = FALSE ; ::_thesis: verum end; theorem :: XBOOLEAN:145 for p, q being boolean number holds p 'nor' (p => q) = FALSE proof let p, q be boolean number ; ::_thesis: p 'nor' (p => q) = FALSE ( p = FALSE or p = TRUE ) by Def3; hence p 'nor' (p => q) = FALSE ; ::_thesis: verum end; theorem :: XBOOLEAN:146 for p, q being boolean number holds p 'nor' (p 'nand' q) = FALSE proof let p, q be boolean number ; ::_thesis: p 'nor' (p 'nand' q) = FALSE ( p = FALSE or p = TRUE ) by Def3; hence p 'nor' (p 'nand' q) = FALSE ; ::_thesis: verum end; theorem :: XBOOLEAN:147 for p being boolean number holds p 'xor' p = FALSE proof let p be boolean number ; ::_thesis: p 'xor' p = FALSE ( p = FALSE or p = TRUE ) by Def3; hence p 'xor' p = FALSE ; ::_thesis: verum end;