begin
deffunc H1( Element of BOOLEAN , Element of BOOLEAN ) -> Element of BOOLEAN = $1 '&' $2;
definition
existence
ex b1 being Function of (2 -tuples_on BOOLEAN),BOOLEAN st
for x, y being Element of BOOLEAN holds b1 . <*x,y*> = x '&' y
uniqueness
for b1, b2 being Function of (2 -tuples_on BOOLEAN),BOOLEAN st ( for x, y being Element of BOOLEAN holds b1 . <*x,y*> = x '&' y ) & ( for x, y being Element of BOOLEAN holds b2 . <*x,y*> = x '&' y ) holds
b1 = b2
existence
ex b1 being Function of (2 -tuples_on BOOLEAN),BOOLEAN st
for x, y being Element of BOOLEAN holds b1 . <*x,y*> = ('not' x) '&' y
uniqueness
for b1, b2 being Function of (2 -tuples_on BOOLEAN),BOOLEAN st ( for x, y being Element of BOOLEAN holds b1 . <*x,y*> = ('not' x) '&' y ) & ( for x, y being Element of BOOLEAN holds b2 . <*x,y*> = ('not' x) '&' y ) holds
b1 = b2
existence
ex b1 being Function of (2 -tuples_on BOOLEAN),BOOLEAN st
for x, y being Element of BOOLEAN holds b1 . <*x,y*> = ('not' x) '&' ('not' y)
uniqueness
for b1, b2 being Function of (2 -tuples_on BOOLEAN),BOOLEAN st ( for x, y being Element of BOOLEAN holds b1 . <*x,y*> = ('not' x) '&' ('not' y) ) & ( for x, y being Element of BOOLEAN holds b2 . <*x,y*> = ('not' x) '&' ('not' y) ) holds
b1 = b2
end;
definition
existence
ex b1 being Function of (2 -tuples_on BOOLEAN),BOOLEAN st
for x, y being Element of BOOLEAN holds b1 . <*x,y*> = 'not' (x '&' y)
uniqueness
for b1, b2 being Function of (2 -tuples_on BOOLEAN),BOOLEAN st ( for x, y being Element of BOOLEAN holds b1 . <*x,y*> = 'not' (x '&' y) ) & ( for x, y being Element of BOOLEAN holds b2 . <*x,y*> = 'not' (x '&' y) ) holds
b1 = b2
existence
ex b1 being Function of (2 -tuples_on BOOLEAN),BOOLEAN st
for x, y being Element of BOOLEAN holds b1 . <*x,y*> = 'not' (('not' x) '&' y)
uniqueness
for b1, b2 being Function of (2 -tuples_on BOOLEAN),BOOLEAN st ( for x, y being Element of BOOLEAN holds b1 . <*x,y*> = 'not' (('not' x) '&' y) ) & ( for x, y being Element of BOOLEAN holds b2 . <*x,y*> = 'not' (('not' x) '&' y) ) holds
b1 = b2
existence
ex b1 being Function of (2 -tuples_on BOOLEAN),BOOLEAN st
for x, y being Element of BOOLEAN holds b1 . <*x,y*> = 'not' (('not' x) '&' ('not' y))
uniqueness
for b1, b2 being Function of (2 -tuples_on BOOLEAN),BOOLEAN st ( for x, y being Element of BOOLEAN holds b1 . <*x,y*> = 'not' (('not' x) '&' ('not' y)) ) & ( for x, y being Element of BOOLEAN holds b2 . <*x,y*> = 'not' (('not' x) '&' ('not' y)) ) holds
b1 = b2
end;
definition
existence
ex b1 being Function of (2 -tuples_on BOOLEAN),BOOLEAN st
for x, y being Element of BOOLEAN holds b1 . <*x,y*> = x 'or' y
uniqueness
for b1, b2 being Function of (2 -tuples_on BOOLEAN),BOOLEAN st ( for x, y being Element of BOOLEAN holds b1 . <*x,y*> = x 'or' y ) & ( for x, y being Element of BOOLEAN holds b2 . <*x,y*> = x 'or' y ) holds
b1 = b2
existence
ex b1 being Function of (2 -tuples_on BOOLEAN),BOOLEAN st
for x, y being Element of BOOLEAN holds b1 . <*x,y*> = ('not' x) 'or' y
uniqueness
for b1, b2 being Function of (2 -tuples_on BOOLEAN),BOOLEAN st ( for x, y being Element of BOOLEAN holds b1 . <*x,y*> = ('not' x) 'or' y ) & ( for x, y being Element of BOOLEAN holds b2 . <*x,y*> = ('not' x) 'or' y ) holds
b1 = b2
existence
ex b1 being Function of (2 -tuples_on BOOLEAN),BOOLEAN st
for x, y being Element of BOOLEAN holds b1 . <*x,y*> = ('not' x) 'or' ('not' y)
uniqueness
for b1, b2 being Function of (2 -tuples_on BOOLEAN),BOOLEAN st ( for x, y being Element of BOOLEAN holds b1 . <*x,y*> = ('not' x) 'or' ('not' y) ) & ( for x, y being Element of BOOLEAN holds b2 . <*x,y*> = ('not' x) 'or' ('not' y) ) holds
b1 = b2
end;
definition
existence
ex b1 being Function of (2 -tuples_on BOOLEAN),BOOLEAN st
for x, y being Element of BOOLEAN holds b1 . <*x,y*> = 'not' (x 'or' y)
uniqueness
for b1, b2 being Function of (2 -tuples_on BOOLEAN),BOOLEAN st ( for x, y being Element of BOOLEAN holds b1 . <*x,y*> = 'not' (x 'or' y) ) & ( for x, y being Element of BOOLEAN holds b2 . <*x,y*> = 'not' (x 'or' y) ) holds
b1 = b2
existence
ex b1 being Function of (2 -tuples_on BOOLEAN),BOOLEAN st
for x, y being Element of BOOLEAN holds b1 . <*x,y*> = 'not' (('not' x) 'or' y)
uniqueness
for b1, b2 being Function of (2 -tuples_on BOOLEAN),BOOLEAN st ( for x, y being Element of BOOLEAN holds b1 . <*x,y*> = 'not' (('not' x) 'or' y) ) & ( for x, y being Element of BOOLEAN holds b2 . <*x,y*> = 'not' (('not' x) 'or' y) ) holds
b1 = b2
existence
ex b1 being Function of (2 -tuples_on BOOLEAN),BOOLEAN st
for x, y being Element of BOOLEAN holds b1 . <*x,y*> = 'not' (('not' x) 'or' ('not' y))
uniqueness
for b1, b2 being Function of (2 -tuples_on BOOLEAN),BOOLEAN st ( for x, y being Element of BOOLEAN holds b1 . <*x,y*> = 'not' (('not' x) 'or' ('not' y)) ) & ( for x, y being Element of BOOLEAN holds b2 . <*x,y*> = 'not' (('not' x) 'or' ('not' y)) ) holds
b1 = b2
end;
definition
existence
ex b1 being Function of (2 -tuples_on BOOLEAN),BOOLEAN st
for x, y being Element of BOOLEAN holds b1 . <*x,y*> = x 'xor' y
uniqueness
for b1, b2 being Function of (2 -tuples_on BOOLEAN),BOOLEAN st ( for x, y being Element of BOOLEAN holds b1 . <*x,y*> = x 'xor' y ) & ( for x, y being Element of BOOLEAN holds b2 . <*x,y*> = x 'xor' y ) holds
b1 = b2
existence
ex b1 being Function of (2 -tuples_on BOOLEAN),BOOLEAN st
for x, y being Element of BOOLEAN holds b1 . <*x,y*> = ('not' x) 'xor' y
uniqueness
for b1, b2 being Function of (2 -tuples_on BOOLEAN),BOOLEAN st ( for x, y being Element of BOOLEAN holds b1 . <*x,y*> = ('not' x) 'xor' y ) & ( for x, y being Element of BOOLEAN holds b2 . <*x,y*> = ('not' x) 'xor' y ) holds
b1 = b2
existence
ex b1 being Function of (2 -tuples_on BOOLEAN),BOOLEAN st
for x, y being Element of BOOLEAN holds b1 . <*x,y*> = ('not' x) 'xor' ('not' y)
uniqueness
for b1, b2 being Function of (2 -tuples_on BOOLEAN),BOOLEAN st ( for x, y being Element of BOOLEAN holds b1 . <*x,y*> = ('not' x) 'xor' ('not' y) ) & ( for x, y being Element of BOOLEAN holds b2 . <*x,y*> = ('not' x) 'xor' ('not' y) ) holds
b1 = b2
end;
theorem
(
and2 . <*0,0*> = 0 &
and2 . <*0,1*> = 0 &
and2 . <*1,0*> = 0 &
and2 . <*1,1*> = 1 &
and2a . <*0,0*> = 0 &
and2a . <*0,1*> = 1 &
and2a . <*1,0*> = 0 &
and2a . <*1,1*> = 0 &
and2b . <*0,0*> = 1 &
and2b . <*0,1*> = 0 &
and2b . <*1,0*> = 0 &
and2b . <*1,1*> = 0 )
theorem
(
or2 . <*0,0*> = 0 &
or2 . <*0,1*> = 1 &
or2 . <*1,0*> = 1 &
or2 . <*1,1*> = 1 &
or2a . <*0,0*> = 1 &
or2a . <*0,1*> = 1 &
or2a . <*1,0*> = 0 &
or2a . <*1,1*> = 1 &
or2b . <*0,0*> = 1 &
or2b . <*0,1*> = 1 &
or2b . <*1,0*> = 1 &
or2b . <*1,1*> = 0 )
definition
existence
ex b1 being Function of (3 -tuples_on BOOLEAN),BOOLEAN st
for x, y, z being Element of BOOLEAN holds b1 . <*x,y,z*> = (x '&' y) '&' z
uniqueness
for b1, b2 being Function of (3 -tuples_on BOOLEAN),BOOLEAN st ( for x, y, z being Element of BOOLEAN holds b1 . <*x,y,z*> = (x '&' y) '&' z ) & ( for x, y, z being Element of BOOLEAN holds b2 . <*x,y,z*> = (x '&' y) '&' z ) holds
b1 = b2
existence
ex b1 being Function of (3 -tuples_on BOOLEAN),BOOLEAN st
for x, y, z being Element of BOOLEAN holds b1 . <*x,y,z*> = (('not' x) '&' y) '&' z
uniqueness
for b1, b2 being Function of (3 -tuples_on BOOLEAN),BOOLEAN st ( for x, y, z being Element of BOOLEAN holds b1 . <*x,y,z*> = (('not' x) '&' y) '&' z ) & ( for x, y, z being Element of BOOLEAN holds b2 . <*x,y,z*> = (('not' x) '&' y) '&' z ) holds
b1 = b2
existence
ex b1 being Function of (3 -tuples_on BOOLEAN),BOOLEAN st
for x, y, z being Element of BOOLEAN holds b1 . <*x,y,z*> = (('not' x) '&' ('not' y)) '&' z
uniqueness
for b1, b2 being Function of (3 -tuples_on BOOLEAN),BOOLEAN st ( for x, y, z being Element of BOOLEAN holds b1 . <*x,y,z*> = (('not' x) '&' ('not' y)) '&' z ) & ( for x, y, z being Element of BOOLEAN holds b2 . <*x,y,z*> = (('not' x) '&' ('not' y)) '&' z ) holds
b1 = b2
existence
ex b1 being Function of (3 -tuples_on BOOLEAN),BOOLEAN st
for x, y, z being Element of BOOLEAN holds b1 . <*x,y,z*> = (('not' x) '&' ('not' y)) '&' ('not' z)
uniqueness
for b1, b2 being Function of (3 -tuples_on BOOLEAN),BOOLEAN st ( for x, y, z being Element of BOOLEAN holds b1 . <*x,y,z*> = (('not' x) '&' ('not' y)) '&' ('not' z) ) & ( for x, y, z being Element of BOOLEAN holds b2 . <*x,y,z*> = (('not' x) '&' ('not' y)) '&' ('not' z) ) holds
b1 = b2
end;
definition
existence
ex b1 being Function of (3 -tuples_on BOOLEAN),BOOLEAN st
for x, y, z being Element of BOOLEAN holds b1 . <*x,y,z*> = 'not' ((x '&' y) '&' z)
uniqueness
for b1, b2 being Function of (3 -tuples_on BOOLEAN),BOOLEAN st ( for x, y, z being Element of BOOLEAN holds b1 . <*x,y,z*> = 'not' ((x '&' y) '&' z) ) & ( for x, y, z being Element of BOOLEAN holds b2 . <*x,y,z*> = 'not' ((x '&' y) '&' z) ) holds
b1 = b2
existence
ex b1 being Function of (3 -tuples_on BOOLEAN),BOOLEAN st
for x, y, z being Element of BOOLEAN holds b1 . <*x,y,z*> = 'not' ((('not' x) '&' y) '&' z)
uniqueness
for b1, b2 being Function of (3 -tuples_on BOOLEAN),BOOLEAN st ( for x, y, z being Element of BOOLEAN holds b1 . <*x,y,z*> = 'not' ((('not' x) '&' y) '&' z) ) & ( for x, y, z being Element of BOOLEAN holds b2 . <*x,y,z*> = 'not' ((('not' x) '&' y) '&' z) ) holds
b1 = b2
existence
ex b1 being Function of (3 -tuples_on BOOLEAN),BOOLEAN st
for x, y, z being Element of BOOLEAN holds b1 . <*x,y,z*> = 'not' ((('not' x) '&' ('not' y)) '&' z)
uniqueness
for b1, b2 being Function of (3 -tuples_on BOOLEAN),BOOLEAN st ( for x, y, z being Element of BOOLEAN holds b1 . <*x,y,z*> = 'not' ((('not' x) '&' ('not' y)) '&' z) ) & ( for x, y, z being Element of BOOLEAN holds b2 . <*x,y,z*> = 'not' ((('not' x) '&' ('not' y)) '&' z) ) holds
b1 = b2
existence
ex b1 being Function of (3 -tuples_on BOOLEAN),BOOLEAN st
for x, y, z being Element of BOOLEAN holds b1 . <*x,y,z*> = 'not' ((('not' x) '&' ('not' y)) '&' ('not' z))
uniqueness
for b1, b2 being Function of (3 -tuples_on BOOLEAN),BOOLEAN st ( for x, y, z being Element of BOOLEAN holds b1 . <*x,y,z*> = 'not' ((('not' x) '&' ('not' y)) '&' ('not' z)) ) & ( for x, y, z being Element of BOOLEAN holds b2 . <*x,y,z*> = 'not' ((('not' x) '&' ('not' y)) '&' ('not' z)) ) holds
b1 = b2
end;
definition
existence
ex b1 being Function of (3 -tuples_on BOOLEAN),BOOLEAN st
for x, y, z being Element of BOOLEAN holds b1 . <*x,y,z*> = (x 'or' y) 'or' z
uniqueness
for b1, b2 being Function of (3 -tuples_on BOOLEAN),BOOLEAN st ( for x, y, z being Element of BOOLEAN holds b1 . <*x,y,z*> = (x 'or' y) 'or' z ) & ( for x, y, z being Element of BOOLEAN holds b2 . <*x,y,z*> = (x 'or' y) 'or' z ) holds
b1 = b2
existence
ex b1 being Function of (3 -tuples_on BOOLEAN),BOOLEAN st
for x, y, z being Element of BOOLEAN holds b1 . <*x,y,z*> = (('not' x) 'or' y) 'or' z
uniqueness
for b1, b2 being Function of (3 -tuples_on BOOLEAN),BOOLEAN st ( for x, y, z being Element of BOOLEAN holds b1 . <*x,y,z*> = (('not' x) 'or' y) 'or' z ) & ( for x, y, z being Element of BOOLEAN holds b2 . <*x,y,z*> = (('not' x) 'or' y) 'or' z ) holds
b1 = b2
existence
ex b1 being Function of (3 -tuples_on BOOLEAN),BOOLEAN st
for x, y, z being Element of BOOLEAN holds b1 . <*x,y,z*> = (('not' x) 'or' ('not' y)) 'or' z
uniqueness
for b1, b2 being Function of (3 -tuples_on BOOLEAN),BOOLEAN st ( for x, y, z being Element of BOOLEAN holds b1 . <*x,y,z*> = (('not' x) 'or' ('not' y)) 'or' z ) & ( for x, y, z being Element of BOOLEAN holds b2 . <*x,y,z*> = (('not' x) 'or' ('not' y)) 'or' z ) holds
b1 = b2
existence
ex b1 being Function of (3 -tuples_on BOOLEAN),BOOLEAN st
for x, y, z being Element of BOOLEAN holds b1 . <*x,y,z*> = (('not' x) 'or' ('not' y)) 'or' ('not' z)
uniqueness
for b1, b2 being Function of (3 -tuples_on BOOLEAN),BOOLEAN st ( for x, y, z being Element of BOOLEAN holds b1 . <*x,y,z*> = (('not' x) 'or' ('not' y)) 'or' ('not' z) ) & ( for x, y, z being Element of BOOLEAN holds b2 . <*x,y,z*> = (('not' x) 'or' ('not' y)) 'or' ('not' z) ) holds
b1 = b2
end;
definition
existence
ex b1 being Function of (3 -tuples_on BOOLEAN),BOOLEAN st
for x, y, z being Element of BOOLEAN holds b1 . <*x,y,z*> = 'not' ((x 'or' y) 'or' z)
uniqueness
for b1, b2 being Function of (3 -tuples_on BOOLEAN),BOOLEAN st ( for x, y, z being Element of BOOLEAN holds b1 . <*x,y,z*> = 'not' ((x 'or' y) 'or' z) ) & ( for x, y, z being Element of BOOLEAN holds b2 . <*x,y,z*> = 'not' ((x 'or' y) 'or' z) ) holds
b1 = b2
existence
ex b1 being Function of (3 -tuples_on BOOLEAN),BOOLEAN st
for x, y, z being Element of BOOLEAN holds b1 . <*x,y,z*> = 'not' ((('not' x) 'or' y) 'or' z)
uniqueness
for b1, b2 being Function of (3 -tuples_on BOOLEAN),BOOLEAN st ( for x, y, z being Element of BOOLEAN holds b1 . <*x,y,z*> = 'not' ((('not' x) 'or' y) 'or' z) ) & ( for x, y, z being Element of BOOLEAN holds b2 . <*x,y,z*> = 'not' ((('not' x) 'or' y) 'or' z) ) holds
b1 = b2
existence
ex b1 being Function of (3 -tuples_on BOOLEAN),BOOLEAN st
for x, y, z being Element of BOOLEAN holds b1 . <*x,y,z*> = 'not' ((('not' x) 'or' ('not' y)) 'or' z)
uniqueness
for b1, b2 being Function of (3 -tuples_on BOOLEAN),BOOLEAN st ( for x, y, z being Element of BOOLEAN holds b1 . <*x,y,z*> = 'not' ((('not' x) 'or' ('not' y)) 'or' z) ) & ( for x, y, z being Element of BOOLEAN holds b2 . <*x,y,z*> = 'not' ((('not' x) 'or' ('not' y)) 'or' z) ) holds
b1 = b2
existence
ex b1 being Function of (3 -tuples_on BOOLEAN),BOOLEAN st
for x, y, z being Element of BOOLEAN holds b1 . <*x,y,z*> = 'not' ((('not' x) 'or' ('not' y)) 'or' ('not' z))
uniqueness
for b1, b2 being Function of (3 -tuples_on BOOLEAN),BOOLEAN st ( for x, y, z being Element of BOOLEAN holds b1 . <*x,y,z*> = 'not' ((('not' x) 'or' ('not' y)) 'or' ('not' z)) ) & ( for x, y, z being Element of BOOLEAN holds b2 . <*x,y,z*> = 'not' ((('not' x) 'or' ('not' y)) 'or' ('not' z)) ) holds
b1 = b2
end;
definition
existence
ex b1 being Function of (3 -tuples_on BOOLEAN),BOOLEAN st
for x, y, z being Element of BOOLEAN holds b1 . <*x,y,z*> = (x 'xor' y) 'xor' z
uniqueness
for b1, b2 being Function of (3 -tuples_on BOOLEAN),BOOLEAN st ( for x, y, z being Element of BOOLEAN holds b1 . <*x,y,z*> = (x 'xor' y) 'xor' z ) & ( for x, y, z being Element of BOOLEAN holds b2 . <*x,y,z*> = (x 'xor' y) 'xor' z ) holds
b1 = b2
end;
theorem
for
x,
y,
z being
Element of
BOOLEAN holds
(
and3 . <*x,y,z*> = (x '&' y) '&' z &
and3a . <*x,y,z*> = (('not' x) '&' y) '&' z &
and3b . <*x,y,z*> = (('not' x) '&' ('not' y)) '&' z &
and3c . <*x,y,z*> = (('not' x) '&' ('not' y)) '&' ('not' z) )
by Def16, Def17, Def18, Def19;
theorem
for
x,
y,
z being
Element of
BOOLEAN holds
(
nand3 . <*x,y,z*> = 'not' ((x '&' y) '&' z) &
nand3a . <*x,y,z*> = 'not' ((('not' x) '&' y) '&' z) &
nand3b . <*x,y,z*> = 'not' ((('not' x) '&' ('not' y)) '&' z) &
nand3c . <*x,y,z*> = 'not' ((('not' x) '&' ('not' y)) '&' ('not' z)) )
by Def20, Def21, Def22, Def23;
theorem
for
x,
y,
z being
Element of
BOOLEAN holds
(
or3 . <*x,y,z*> = (x 'or' y) 'or' z &
or3a . <*x,y,z*> = (('not' x) 'or' y) 'or' z &
or3b . <*x,y,z*> = (('not' x) 'or' ('not' y)) 'or' z &
or3c . <*x,y,z*> = (('not' x) 'or' ('not' y)) 'or' ('not' z) )
by Def24, Def25, Def26, Def27;
theorem
for
x,
y,
z being
Element of
BOOLEAN holds
(
nor3 . <*x,y,z*> = 'not' ((x 'or' y) 'or' z) &
nor3a . <*x,y,z*> = 'not' ((('not' x) 'or' y) 'or' z) &
nor3b . <*x,y,z*> = 'not' ((('not' x) 'or' ('not' y)) 'or' z) &
nor3c . <*x,y,z*> = 'not' ((('not' x) 'or' ('not' y)) 'or' ('not' z)) )
by Def28, Def29, Def30, Def31;
theorem
for
x,
y,
z being
Element of
BOOLEAN holds
(
and3 . <*x,y,z*> = nor3c . <*x,y,z*> &
and3a . <*x,y,z*> = nor3b . <*z,y,x*> &
and3b . <*x,y,z*> = nor3a . <*z,y,x*> &
and3c . <*x,y,z*> = nor3 . <*x,y,z*> )
theorem
for
x,
y,
z being
Element of
BOOLEAN holds
(
or3 . <*x,y,z*> = nand3c . <*x,y,z*> &
or3a . <*x,y,z*> = nand3b . <*z,y,x*> &
or3b . <*x,y,z*> = nand3a . <*z,y,x*> &
or3c . <*x,y,z*> = nand3 . <*x,y,z*> )
theorem
(
and3 . <*0,0,0*> = 0 &
and3 . <*0,0,1*> = 0 &
and3 . <*0,1,0*> = 0 &
and3 . <*0,1,1*> = 0 &
and3 . <*1,0,0*> = 0 &
and3 . <*1,0,1*> = 0 &
and3 . <*1,1,0*> = 0 &
and3 . <*1,1,1*> = 1 )
theorem
(
and3a . <*0,0,0*> = 0 &
and3a . <*0,0,1*> = 0 &
and3a . <*0,1,0*> = 0 &
and3a . <*0,1,1*> = 1 &
and3a . <*1,0,0*> = 0 &
and3a . <*1,0,1*> = 0 &
and3a . <*1,1,0*> = 0 &
and3a . <*1,1,1*> = 0 )
theorem
(
and3b . <*0,0,0*> = 0 &
and3b . <*0,0,1*> = 1 &
and3b . <*0,1,0*> = 0 &
and3b . <*0,1,1*> = 0 &
and3b . <*1,0,0*> = 0 &
and3b . <*1,0,1*> = 0 &
and3b . <*1,1,0*> = 0 &
and3b . <*1,1,1*> = 0 )
theorem
(
and3c . <*0,0,0*> = 1 &
and3c . <*0,0,1*> = 0 &
and3c . <*0,1,0*> = 0 &
and3c . <*0,1,1*> = 0 &
and3c . <*1,0,0*> = 0 &
and3c . <*1,0,1*> = 0 &
and3c . <*1,1,0*> = 0 &
and3c . <*1,1,1*> = 0 )
theorem
(
or3 . <*0,0,0*> = 0 &
or3 . <*0,0,1*> = 1 &
or3 . <*0,1,0*> = 1 &
or3 . <*0,1,1*> = 1 &
or3 . <*1,0,0*> = 1 &
or3 . <*1,0,1*> = 1 &
or3 . <*1,1,0*> = 1 &
or3 . <*1,1,1*> = 1 )
theorem
(
or3a . <*0,0,0*> = 1 &
or3a . <*0,0,1*> = 1 &
or3a . <*0,1,0*> = 1 &
or3a . <*0,1,1*> = 1 &
or3a . <*1,0,0*> = 0 &
or3a . <*1,0,1*> = 1 &
or3a . <*1,1,0*> = 1 &
or3a . <*1,1,1*> = 1 )
theorem
(
or3b . <*0,0,0*> = 1 &
or3b . <*0,0,1*> = 1 &
or3b . <*0,1,0*> = 1 &
or3b . <*0,1,1*> = 1 &
or3b . <*1,0,0*> = 1 &
or3b . <*1,0,1*> = 1 &
or3b . <*1,1,0*> = 0 &
or3b . <*1,1,1*> = 1 )
theorem
(
or3c . <*0,0,0*> = 1 &
or3c . <*0,0,1*> = 1 &
or3c . <*0,1,0*> = 1 &
or3c . <*0,1,1*> = 1 &
or3c . <*1,0,0*> = 1 &
or3c . <*1,0,1*> = 1 &
or3c . <*1,1,0*> = 1 &
or3c . <*1,1,1*> = 0 )
theorem
(
xor3 . <*0,0,0*> = 0 &
xor3 . <*0,0,1*> = 1 &
xor3 . <*0,1,0*> = 1 &
xor3 . <*0,1,1*> = 0 &
xor3 . <*1,0,0*> = 1 &
xor3 . <*1,0,1*> = 0 &
xor3 . <*1,1,0*> = 0 &
xor3 . <*1,1,1*> = 1 )
begin
:: Preliminaries
::---------------------------------------------------------------------------