:: 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;