:: 2's Complement Circuit. Part I. Boolean Operators and 2's
:: Complement Circuit Properties
:: by Katsumi Wasaki and Pauline N. Kawamoto
::
:: Received October 25, 1996
:: Copyright (c) 1996-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies CIRCCOMB, STRUCT_0, XBOOLE_0, MSUALG_1, LATTICES, CIRCUIT1,
FSM_1, GLIB_000, FUNCT_1, SUBSET_1, MARGREL1, XBOOLEAN, FINSEQ_2,
FINSEQ_1, CARD_1, FACIRC_1, MSAFREE2, FUNCT_4, RELAT_1, CIRCUIT2,
TWOSCOMP;
notations TARSKI, XBOOLE_0, XTUPLE_0, SUBSET_1, RELAT_1, FUNCT_1, FUNCT_2,
ORDINAL1, NUMBERS, FINSEQ_1, STRUCT_0, MARGREL1, FINSEQ_2, BINARITH,
MSUALG_1, MSAFREE2, CIRCUIT1, CIRCUIT2, CIRCCOMB, FACIRC_1;
constructors BINARITH, CIRCUIT1, CIRCUIT2, FACIRC_1, RELSET_1, XTUPLE_0,
NUMBERS;
registrations RELSET_1, XBOOLEAN, MARGREL1, CARD_3, CIRCCOMB, FACIRC_1,
ORDINAL1, FINSEQ_1, FUNCT_1, MSAFREE2;
requirements NUMERALS, SUBSET, BOOLE, ARITHM;
definitions CIRCUIT2;
equalities XBOOLEAN;
theorems TARSKI, ENUMSET1, BINARITH, FUNCT_1, FINSEQ_2, CIRCUIT1, CIRCUIT2,
CIRCCOMB, FACIRC_1, XBOOLE_0, XBOOLE_1;
schemes FACIRC_1;
begin :: Boolean Operators
::---------------------------------------------------------------------------
:: Preliminaries
::---------------------------------------------------------------------------
definition
let S be unsplit non void non empty ManySortedSign;
let A be Boolean Circuit of S;
let s be State of A;
let v be Vertex of S;
redefine func s.v -> Element of BOOLEAN; :: redefines . (FUNCT_1, definition)
coherence
proof
s.v in (the Sorts of A).v by CIRCUIT1:4;
hence thesis;
end;
end;
::---------------------------------------------------------------------------
:: Boolean Operations : 2,3-Input and*, nand*, or*, nor*, xor*
::---------------------------------------------------------------------------
:: 2-Input Operators
deffunc U(Element of BOOLEAN,Element of BOOLEAN) = $1 '&' $2;
notation
synonym and2 for '&';
end;
::$CD
definition
func and2a -> Function of 2-tuples_on BOOLEAN, BOOLEAN means
: Def1:
for x,y being Element of BOOLEAN holds it.<*x,y*> = 'not' x '&' y;
existence
proof
deffunc U(Element of BOOLEAN,Element of BOOLEAN) = 'not' $1 '&' $2;
thus ex t being Function of 2-tuples_on BOOLEAN, BOOLEAN st for x,y being
Element of BOOLEAN holds t.<*x,y*> = U(x,y) from FACIRC_1:sch 1;
end;
uniqueness
proof
deffunc U(Element of BOOLEAN,Element of BOOLEAN) = 'not' $1 '&' $2;
thus for t1,t2 being Function of 2-tuples_on BOOLEAN, BOOLEAN st (for x,y
being Element of BOOLEAN holds t1.<*x,y*> = U(x,y)) & (for x,y being Element of
BOOLEAN holds t2.<*x,y*> = U(x,y)) holds t1 = t2 from FACIRC_1:sch 2;
end;
end;
::$CD
definition
func nand2 -> Function of 2-tuples_on BOOLEAN, BOOLEAN means
: Def2:
for x,y being Element of BOOLEAN holds it.<*x,y*> = 'not' (x '&' y);
existence
proof
deffunc U(Element of BOOLEAN,Element of BOOLEAN) = 'not' ($1 '&' $2);
thus ex t being Function of 2-tuples_on BOOLEAN, BOOLEAN st for x,y being
Element of BOOLEAN holds t.<*x,y*> = U(x,y) from FACIRC_1:sch 1;
end;
uniqueness
proof
deffunc U(Element of BOOLEAN,Element of BOOLEAN) = 'not' ($1 '&' $2);
thus for t1,t2 being Function of 2-tuples_on BOOLEAN, BOOLEAN st (for x,y
being Element of BOOLEAN holds t1.<*x,y*> = U(x,y)) & (for x,y being Element of
BOOLEAN holds t2.<*x,y*> = U(x,y)) holds t1 = t2 from FACIRC_1:sch 2;
end;
func nand2a -> Function of 2-tuples_on BOOLEAN, BOOLEAN means
: Def3:
for x, y being Element of BOOLEAN holds it.<*x,y*> = 'not' ('not' x '&' y);
existence
proof
deffunc U(Element of BOOLEAN,Element of BOOLEAN) = 'not' ('not' $1 '&' $2);
thus ex t being Function of 2-tuples_on BOOLEAN, BOOLEAN st for x,y being
Element of BOOLEAN holds t.<*x,y*> = U(x,y) from FACIRC_1:sch 1;
end;
uniqueness
proof
deffunc U(Element of BOOLEAN,Element of BOOLEAN) = 'not' ('not' $1 '&' $2);
thus for t1,t2 being Function of 2-tuples_on BOOLEAN, BOOLEAN st (for x,y
being Element of BOOLEAN holds t1.<*x,y*> = U(x,y)) & (for x,y being Element of
BOOLEAN holds t2.<*x,y*> = U(x,y)) holds t1 = t2 from FACIRC_1:sch 2;
end;
end;
notation
synonym or2 for 'or';
end;
Lm1:
for x,y being Element of BOOLEAN
holds or2.<*x,y*> = 'not' ('not' x '&' 'not' y)
proof let x,y being Element of BOOLEAN;
thus or2.<*x,y*> = x 'or' y by FACIRC_1:def 5
.= 'not' ('not' x '&' 'not' y);
end;
::$CD 2
definition
func or2a -> Function of 2-tuples_on BOOLEAN, BOOLEAN means
: Def4:
for x,y being Element of BOOLEAN holds it.<*x,y*> = 'not' x 'or' y;
existence
proof
deffunc U(Element of BOOLEAN,Element of BOOLEAN) = 'not' $1 'or' $2;
thus ex t being Function of 2-tuples_on BOOLEAN, BOOLEAN st for x,y being
Element of BOOLEAN holds t.<*x,y*> = U(x,y) from FACIRC_1:sch 1;
end;
uniqueness
proof
deffunc U(Element of BOOLEAN,Element of BOOLEAN) = 'not' $1 'or' $2;
thus for t1,t2 being Function of 2-tuples_on BOOLEAN, BOOLEAN st (for x,y
being Element of BOOLEAN holds t1.<*x,y*> = U(x,y)) & (for x,y being Element of
BOOLEAN holds t2.<*x,y*> = U(x,y)) holds t1 = t2 from FACIRC_1:sch 2;
end;
end;
Lm2:
for x,y being Element of BOOLEAN holds nand2.<*x,y*> = 'not' x 'or' 'not' y
by Def2;
::$CD
definition
func nor2 -> Function of 2-tuples_on BOOLEAN, BOOLEAN means
:Def5:
for x,y being Element of BOOLEAN holds it.<*x,y*> = 'not' (x 'or' y);
existence
proof
deffunc U(Element of BOOLEAN,Element of BOOLEAN) = 'not' ($1 'or' $2);
thus ex t being Function of 2-tuples_on BOOLEAN, BOOLEAN st for x,y being
Element of BOOLEAN holds t.<*x,y*> = U(x,y) from FACIRC_1:sch 1;
end;
uniqueness
proof
deffunc U(Element of BOOLEAN,Element of BOOLEAN) = 'not' ($1 'or' $2);
thus for t1,t2 being Function of 2-tuples_on BOOLEAN, BOOLEAN st (for x,y
being Element of BOOLEAN holds t1.<*x,y*> = U(x,y)) & (for x,y being Element of
BOOLEAN holds t2.<*x,y*> = U(x,y)) holds t1 = t2 from FACIRC_1:sch 2;
end;
func nor2a -> Function of 2-tuples_on BOOLEAN, BOOLEAN means
:Def6:
for x,y being Element of BOOLEAN holds it.<*x,y*> = 'not' ('not' x 'or' y);
existence
proof
deffunc U(Element of BOOLEAN,Element of BOOLEAN) = 'not' ('not' $1 'or' $2
);
thus ex t being Function of 2-tuples_on BOOLEAN, BOOLEAN st for x,y being
Element of BOOLEAN holds t.<*x,y*> = U(x,y) from FACIRC_1:sch 1;
end;
uniqueness
proof
deffunc U(Element of BOOLEAN,Element of BOOLEAN) = 'not' ('not' $1 'or' $2
);
thus for t1,t2 being Function of 2-tuples_on BOOLEAN, BOOLEAN st (for x,y
being Element of BOOLEAN holds t1.<*x,y*> = U(x,y)) & (for x,y being Element of
BOOLEAN holds t2.<*x,y*> = U(x,y)) holds t1 = t2 from FACIRC_1:sch 2;
end;
end;
Lm3:
for x,y being Element of BOOLEAN holds nor2.<*x,y*> = 'not' x '&' 'not' y
proof let x,y be Element of BOOLEAN;
thus nor2.<*x,y*> = 'not' ( x 'or' y) by Def5
.= 'not' x '&' 'not' y;
end;
notation
synonym xor2 for 'xor';
end;
Lm4:
for x,y being Element of BOOLEAN
holds and2.<*x,y*> = 'not' ('not' x 'or' 'not' y) by FACIRC_1:def 6;
::$CD 2
definition
func xor2a -> Function of 2-tuples_on BOOLEAN, BOOLEAN means
: Def7:
for x, y being Element of BOOLEAN holds it.<*x,y*> = 'not' x 'xor' y;
existence
proof
deffunc U(Element of BOOLEAN,Element of BOOLEAN) = 'not' $1 'xor' $2;
thus ex t being Function of 2-tuples_on BOOLEAN, BOOLEAN st for x,y being
Element of BOOLEAN holds t.<*x,y*> = U(x,y) from FACIRC_1:sch 1;
end;
uniqueness
proof
deffunc U(Element of BOOLEAN,Element of BOOLEAN) = 'not' $1 'xor' $2;
thus for t1,t2 being Function of 2-tuples_on BOOLEAN, BOOLEAN st (for x,y
being Element of BOOLEAN holds t1.<*x,y*> = U(x,y)) & (for x,y being Element of
BOOLEAN holds t2.<*x,y*> = U(x,y)) holds t1 = t2 from FACIRC_1:sch 2;
end;
func xor2b -> Function of 2-tuples_on BOOLEAN, BOOLEAN means
: Def8:
for x, y being Element of BOOLEAN holds it.<*x,y*> = 'not' x 'xor' 'not' y;
existence
proof
deffunc U(Element of BOOLEAN,Element of BOOLEAN) = 'not' $1 'xor' 'not' $2;
thus ex t being Function of 2-tuples_on BOOLEAN, BOOLEAN st for x,y being
Element of BOOLEAN holds t.<*x,y*> = U(x,y) from FACIRC_1:sch 1;
end;
uniqueness
proof
deffunc U(Element of BOOLEAN,Element of BOOLEAN) = 'not' $1 'xor' 'not' $2;
thus for t1,t2 being Function of 2-tuples_on BOOLEAN, BOOLEAN st (for x,y
being Element of BOOLEAN holds t1.<*x,y*> = U(x,y)) & (for x,y being Element of
BOOLEAN holds t2.<*x,y*> = U(x,y)) holds t1 = t2 from FACIRC_1:sch 2;
end;
end;
theorem
for x,y being Element of BOOLEAN holds and2.<*x,y*> = x '&' y & and2a.
<*x,y*> = 'not' x '&' y & nor2.<*x,y*> = 'not' x '&' 'not' y
by FACIRC_1:def 6,Def1,Lm3;
theorem
for x,y being Element of BOOLEAN holds nand2.<*x,y*> = 'not' (x '&' y)
& nand2a.<*x,y*> = 'not' ('not' x '&' y) & or2.<*x,y*> = 'not' ('not' x '&'
'not' y) by Def2,Def3,Lm1;
theorem
for x,y being Element of BOOLEAN holds or2.<*x,y*> = x 'or' y & or2a.
<*x,y*> = 'not' x 'or' y & nand2.<*x,y*> = 'not' x 'or' 'not' y
by FACIRC_1:def 5,Def4
,Lm2;
theorem
for x,y being Element of BOOLEAN holds nor2.<*x,y*> = 'not' (x 'or' y)
& nor2a.<*x,y*> = 'not' ('not' x 'or' y) & and2.<*x,y*> = 'not' ('not' x 'or'
'not' y) by Def5,Def6,Lm4;
theorem
for x,y being Element of BOOLEAN holds xor2.<*x,y*> = x 'xor' y &
xor2a.<*x,y*> = 'not' x 'xor' y & xor2b.<*x,y*> = 'not' x 'xor' 'not' y by
FACIRC_1:def 4,Def7,Def8;
theorem
for x,y being Element of BOOLEAN holds and2a.<*x,y*> = nor2a.<*y,x*>
proof
let x,y be Element of BOOLEAN;
thus and2a.<*x,y*> = 'not' ('not' 'not' x 'or' 'not' y) by Def1
.= nor2a.<*y,x*> by Def6;
end;
theorem
for x,y being Element of BOOLEAN holds or2a.<*x,y*> = nand2a.<*y,x*>
proof
let x,y be Element of BOOLEAN;
thus or2a.<*x,y*> = 'not' x 'or' y by Def4
.= nand2a.<*y,x*> by Def3;
end;
theorem
for x,y being Element of BOOLEAN holds xor2b.<*x,y*> = xor2.<*x,y*>
proof
let x,y be Element of BOOLEAN;
thus xor2b.<*x,y*> = 'not' x 'xor' 'not' y by Def8
.= x 'xor' y
.= xor2.<*x,y*> by FACIRC_1:def 4;
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 & nor2.
<*0,0*>=1 & nor2.<*0,1*>=0 & nor2.<*1,0*>=0 & nor2.<*1,1*>=0
proof
thus and2.<*0,0*> = FALSE '&' FALSE by FACIRC_1:def 6
.= 0;
thus and2.<*0,1*> = FALSE '&' TRUE by FACIRC_1:def 6
.= 0;
thus and2.<*1,0*> = TRUE '&' FALSE by FACIRC_1:def 6
.= 0;
thus and2.<*1,1*> = TRUE '&' TRUE by FACIRC_1:def 6
.= 1;
thus and2a.<*0,0*> = 'not' FALSE '&' FALSE by Def1
.= 0;
thus and2a.<*0,1*> = 'not' FALSE '&' TRUE by Def1
.= 1;
thus and2a.<*1,0*> = 'not' TRUE '&' FALSE by Def1
.= 0;
thus and2a.<*1,1*> = 'not' TRUE '&' TRUE by Def1
.= 0;
thus nor2.<*0,0*> = TRUE '&' 'not' FALSE by Lm3
.= 1;
thus nor2.<*0,1*> = 'not' FALSE '&' 'not' TRUE by Lm3
.= 0;
thus nor2.<*1,0*> = 'not' TRUE '&' 'not' FALSE by Lm3
.= 0;
thus nor2.<*1,1*> = FALSE '&' 'not' TRUE by Lm3
.= 0;
end;
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 &
nand2.<*0,0*>=1 &
nand2.<*0,1*>=1 & nand2.<*1,0*>=1 & nand2.<*1,1*>=0
proof
thus or2.<*0,0*> = FALSE 'or' FALSE by FACIRC_1:def 5
.= 0;
thus or2.<*0,1*> = FALSE 'or' TRUE by FACIRC_1:def 5
.= 1;
thus or2.<*1,0*> = TRUE 'or' FALSE by FACIRC_1:def 5
.= 1;
thus or2.<*1,1*> = TRUE 'or' TRUE by FACIRC_1:def 5
.= 1;
thus or2a.<*0,0*> = TRUE 'or' FALSE by Def4
.= 1;
thus or2a.<*0,1*> = 'not' FALSE 'or' TRUE by Def4
.= 1;
thus or2a.<*1,0*> = 'not' TRUE 'or' FALSE by Def4
.= 0;
thus or2a.<*1,1*> = 'not' TRUE 'or' TRUE by Def4
.= 1;
thus nand2.<*0,0*> = TRUE 'or' 'not' FALSE by Lm2
.= 1;
thus nand2.<*0,1*> = TRUE 'or' 'not' TRUE by Lm2
.= 1;
thus nand2.<*1,0*> = 'not' TRUE 'or' TRUE by Lm2
.= 1;
thus nand2.<*1,1*> = FALSE 'or' 'not' TRUE by Lm2
.= 0;
end;
theorem
xor2.<*0,0*>=0 & xor2.<*0,1*>=1 & xor2.<*1,0*>=1 & xor2.<*1,1*>=0 &
xor2a.<*0,0*>=1 & xor2a.<*0,1*>=0 & xor2a.<*1,0*>=0 & xor2a.<*1,1*>=1
proof
thus xor2.<*0,0*> = FALSE 'xor' FALSE by FACIRC_1:def 4
.= 0;
thus xor2.<*0,1*> = FALSE 'xor' TRUE by FACIRC_1:def 4
.= 1;
thus xor2.<*1,0*> = TRUE 'xor' FALSE by FACIRC_1:def 4
.= 1;
thus xor2.<*1,1*> = TRUE 'xor' TRUE by FACIRC_1:def 4
.= 0;
thus xor2a.<*0,0*> = 'not' FALSE 'xor' FALSE by Def7
.= 1;
thus xor2a.<*0,1*> = 'not' FALSE 'xor' TRUE by Def7
.= 0;
thus xor2a.<*1,0*> = 'not' TRUE 'xor' FALSE by Def7
.= 0;
thus xor2a.<*1,1*> = 'not' TRUE 'xor' TRUE by Def7
.= 1;
end;
:: 3-Input Operators
definition
func and3 -> Function of 3-tuples_on BOOLEAN, BOOLEAN means
: Def9:
for x,y ,z being Element of BOOLEAN holds it.<*x,y,z*> = x '&' y '&' z;
existence
proof
deffunc U(Element of BOOLEAN,Element of BOOLEAN,Element of BOOLEAN) = $1
'&' $2 '&' $3;
thus ex t being Function of 3-tuples_on BOOLEAN, BOOLEAN st for x,y,z
being Element of BOOLEAN holds t.<*x,y,z*> = U(x,y,z) from FACIRC_1:sch 4;
end;
uniqueness
proof
deffunc U(Element of BOOLEAN,Element of BOOLEAN,Element of BOOLEAN) = $1
'&' $2 '&' $3;
thus for t1,t2 being Function of 3-tuples_on BOOLEAN, BOOLEAN st (for x,y,
z being Element of BOOLEAN holds t1.<*x,y,z*> = U(x,y,z)) & (for x,y,z being
Element of BOOLEAN holds t2.<*x,y,z*> = U(x,y,z)) holds t1 = t2 from FACIRC_1:
sch 5;
end;
func and3a -> Function of 3-tuples_on BOOLEAN, BOOLEAN means
: Def10:
for x, y,z being Element of BOOLEAN holds it.<*x,y,z*> = 'not' x '&' y '&' z;
existence
proof
deffunc U(Element of BOOLEAN,Element of BOOLEAN,Element of BOOLEAN) =
'not' $1 '&' $2 '&' $3;
thus ex t being Function of 3-tuples_on BOOLEAN, BOOLEAN st for x,y,z
being Element of BOOLEAN holds t.<*x,y,z*> = U(x,y,z) from FACIRC_1:sch 4;
end;
uniqueness
proof
deffunc U(Element of BOOLEAN,Element of BOOLEAN,Element of BOOLEAN) =
'not' $1 '&' $2 '&' $3;
thus for t1,t2 being Function of 3-tuples_on BOOLEAN, BOOLEAN st (for x,y,
z being Element of BOOLEAN holds t1.<*x,y,z*> = U(x,y,z)) & (for x,y,z being
Element of BOOLEAN holds t2.<*x,y,z*> = U(x,y,z)) holds t1 = t2 from FACIRC_1:
sch 5;
end;
func and3b -> Function of 3-tuples_on BOOLEAN, BOOLEAN means
: Def11:
for x,
y,z being Element of BOOLEAN holds it.<*x,y,z*> = 'not' x '&' 'not' y '&' z;
existence
proof
deffunc U(Element of BOOLEAN,Element of BOOLEAN,Element of BOOLEAN) =
'not' $1 '&' 'not' $2 '&' $3;
thus ex t being Function of 3-tuples_on BOOLEAN, BOOLEAN st for x,y,z
being Element of BOOLEAN holds t.<*x,y,z*> = U(x,y,z) from FACIRC_1:sch 4;
end;
uniqueness
proof
deffunc U(Element of BOOLEAN,Element of BOOLEAN,Element of BOOLEAN) =
'not' $1 '&' 'not' $2 '&' $3;
thus for t1,t2 being Function of 3-tuples_on BOOLEAN, BOOLEAN st (for x,y,
z being Element of BOOLEAN holds t1.<*x,y,z*> = U(x,y,z)) & (for x,y,z being
Element of BOOLEAN holds t2.<*x,y,z*> = U(x,y,z)) holds t1 = t2 from FACIRC_1:
sch 5;
end;
end;
::$CD
definition
func nand3 -> Function of 3-tuples_on BOOLEAN, BOOLEAN means
: Def12:
for x,
y,z being Element of BOOLEAN holds it.<*x,y,z*> = 'not' (x '&' y '&' z);
existence
proof
deffunc U(Element of BOOLEAN,Element of BOOLEAN,Element of BOOLEAN) =
'not' ($1 '&' $2 '&' $3);
thus ex t being Function of 3-tuples_on BOOLEAN, BOOLEAN st for x,y,z
being Element of BOOLEAN holds t.<*x,y,z*> = U(x,y,z) from FACIRC_1:sch 4;
end;
uniqueness
proof
deffunc U(Element of BOOLEAN,Element of BOOLEAN,Element of BOOLEAN) =
'not' ($1 '&' $2 '&' $3);
thus for t1,t2 being Function of 3-tuples_on BOOLEAN, BOOLEAN st (for x,y,
z being Element of BOOLEAN holds t1.<*x,y,z*> = U(x,y,z)) & (for x,y,z being
Element of BOOLEAN holds t2.<*x,y,z*> = U(x,y,z)) holds t1 = t2 from FACIRC_1:
sch 5;
end;
func nand3a -> Function of 3-tuples_on BOOLEAN, BOOLEAN means
: Def13:
for x
,y,z being Element of BOOLEAN holds it.<*x,y,z*> = 'not' ('not' x '&' y '&' z);
existence
proof
deffunc U(Element of BOOLEAN,Element of BOOLEAN,Element of BOOLEAN) =
'not' ('not' $1 '&' $2 '&' $3);
thus ex t being Function of 3-tuples_on BOOLEAN, BOOLEAN st for x,y,z
being Element of BOOLEAN holds t.<*x,y,z*> = U(x,y,z) from FACIRC_1:sch 4;
end;
uniqueness
proof
deffunc U(Element of BOOLEAN,Element of BOOLEAN,Element of BOOLEAN) =
'not' ('not' $1 '&' $2 '&' $3);
thus for t1,t2 being Function of 3-tuples_on BOOLEAN, BOOLEAN st (for x,y,
z being Element of BOOLEAN holds t1.<*x,y,z*> = U(x,y,z)) & (for x,y,z being
Element of BOOLEAN holds t2.<*x,y,z*> = U(x,y,z)) holds t1 = t2 from FACIRC_1:
sch 5;
end;
func nand3b -> Function of 3-tuples_on BOOLEAN, BOOLEAN means
: Def14:
for x
,y,z being Element of BOOLEAN holds it.<*x,y,z*> = 'not' ('not' x '&' 'not' y
'&' z);
existence
proof
deffunc U(Element of BOOLEAN,Element of BOOLEAN,Element of BOOLEAN) =
'not' ('not' $1 '&' 'not' $2 '&' $3);
thus ex t being Function of 3-tuples_on BOOLEAN, BOOLEAN st for x,y,z
being Element of BOOLEAN holds t.<*x,y,z*> = U(x,y,z) from FACIRC_1:sch 4;
end;
uniqueness
proof
deffunc U(Element of BOOLEAN,Element of BOOLEAN,Element of BOOLEAN) =
'not' ('not' $1 '&' 'not' $2 '&' $3);
thus for t1,t2 being Function of 3-tuples_on BOOLEAN, BOOLEAN st (for x,y,
z being Element of BOOLEAN holds t1.<*x,y,z*> = U(x,y,z)) & (for x,y,z being
Element of BOOLEAN holds t2.<*x,y,z*> = U(x,y,z)) holds t1 = t2 from FACIRC_1:
sch 5;
end;
end;
Lm5:
for x,y,z being Element of BOOLEAN
holds or3.<*x,y,z*> = 'not' ('not' x '&' 'not' y '&' 'not' z)
proof let x,y,z being Element of BOOLEAN;
thus or3.<*x,y,z*> = x 'or' y 'or' z by FACIRC_1:def 7
.= 'not' ('not' x '&' 'not' y '&' 'not' z);
end;
::$CD 2
definition
func or3a -> Function of 3-tuples_on BOOLEAN, BOOLEAN means
: Def15:
for x,y
,z being Element of BOOLEAN holds it.<*x,y,z*> = 'not' x 'or' y 'or' z;
existence
proof
deffunc U(Element of BOOLEAN,Element of BOOLEAN,Element of BOOLEAN) =
'not' $1 'or' $2 'or' $3;
thus ex t being Function of 3-tuples_on BOOLEAN, BOOLEAN st for x,y,z
being Element of BOOLEAN holds t.<*x,y,z*> = U(x,y,z) from FACIRC_1:sch 4;
end;
uniqueness
proof
deffunc U(Element of BOOLEAN,Element of BOOLEAN,Element of BOOLEAN) =
'not' $1 'or' $2 'or' $3;
thus for t1,t2 being Function of 3-tuples_on BOOLEAN, BOOLEAN st (for x,y,
z being Element of BOOLEAN holds t1.<*x,y,z*> = U(x,y,z)) & (for x,y,z being
Element of BOOLEAN holds t2.<*x,y,z*> = U(x,y,z)) holds t1 = t2 from FACIRC_1:
sch 5;
end;
func or3b -> Function of 3-tuples_on BOOLEAN, BOOLEAN means
: Def16:
for x,y
,z being Element of BOOLEAN holds it.<*x,y,z*> = 'not' x 'or' 'not' y 'or' z;
existence
proof
deffunc U(Element of BOOLEAN,Element of BOOLEAN,Element of BOOLEAN) =
'not' $1 'or' 'not' $2 'or' $3;
thus ex t being Function of 3-tuples_on BOOLEAN, BOOLEAN st for x,y,z
being Element of BOOLEAN holds t.<*x,y,z*> = U(x,y,z) from FACIRC_1:sch 4;
end;
uniqueness
proof
deffunc U(Element of BOOLEAN,Element of BOOLEAN,Element of BOOLEAN) =
'not' $1 'or' 'not' $2 'or' $3;
thus for t1,t2 being Function of 3-tuples_on BOOLEAN, BOOLEAN st (for x,y,
z being Element of BOOLEAN holds t1.<*x,y,z*> = U(x,y,z)) & (for x,y,z being
Element of BOOLEAN holds t2.<*x,y,z*> = U(x,y,z)) holds t1 = t2 from FACIRC_1:
sch 5;
end;
end;
Lm6:
for x,y,z being Element of BOOLEAN
holds nand3.<*x,y,z*> = 'not' x 'or' 'not' y 'or' 'not' z by Def12;
::$CD
definition
func nor3 -> Function of 3-tuples_on BOOLEAN, BOOLEAN means
: Def17:
for x,y
,z being Element of BOOLEAN holds it.<*x,y,z*> = 'not' (x 'or' y 'or' z);
existence
proof
deffunc U(Element of BOOLEAN,Element of BOOLEAN,Element of BOOLEAN) =
'not' ($1 'or' $2 'or' $3);
thus ex t being Function of 3-tuples_on BOOLEAN, BOOLEAN st for x,y,z
being Element of BOOLEAN holds t.<*x,y,z*> = U(x,y,z) from FACIRC_1:sch 4;
end;
uniqueness
proof
deffunc U(Element of BOOLEAN,Element of BOOLEAN,Element of BOOLEAN) =
'not' ($1 'or' $2 'or' $3);
thus for t1,t2 being Function of 3-tuples_on BOOLEAN, BOOLEAN st (for x,y,
z being Element of BOOLEAN holds t1.<*x,y,z*> = U(x,y,z)) & (for x,y,z being
Element of BOOLEAN holds t2.<*x,y,z*> = U(x,y,z)) holds t1 = t2 from FACIRC_1:
sch 5;
end;
func nor3a -> Function of 3-tuples_on BOOLEAN, BOOLEAN means
: Def18:
for x,
y,z being Element of BOOLEAN holds it.<*x,y,z*> = 'not' ('not' x 'or' y 'or' z)
;
existence
proof
deffunc U(Element of BOOLEAN,Element of BOOLEAN,Element of BOOLEAN) =
'not' ('not' $1 'or' $2 'or' $3);
thus ex t being Function of 3-tuples_on BOOLEAN, BOOLEAN st for x,y,z
being Element of BOOLEAN holds t.<*x,y,z*> = U(x,y,z) from FACIRC_1:sch 4;
end;
uniqueness
proof
deffunc U(Element of BOOLEAN,Element of BOOLEAN,Element of BOOLEAN) =
'not' ('not' $1 'or' $2 'or' $3);
thus for t1,t2 being Function of 3-tuples_on BOOLEAN, BOOLEAN st (for x,y,
z being Element of BOOLEAN holds t1.<*x,y,z*> = U(x,y,z)) & (for x,y,z being
Element of BOOLEAN holds t2.<*x,y,z*> = U(x,y,z)) holds t1 = t2 from FACIRC_1:
sch 5;
end;
func nor3b -> Function of 3-tuples_on BOOLEAN, BOOLEAN means
: Def19:
for x,
y,z being Element of BOOLEAN holds it.<*x,y,z*> = 'not' ('not' x 'or' 'not' y
'or' z);
existence
proof
deffunc U(Element of BOOLEAN,Element of BOOLEAN,Element of BOOLEAN) =
'not' ('not' $1 'or' 'not' $2 'or' $3);
thus ex t being Function of 3-tuples_on BOOLEAN, BOOLEAN st for x,y,z
being Element of BOOLEAN holds t.<*x,y,z*> = U(x,y,z) from FACIRC_1:sch 4;
end;
uniqueness
proof
deffunc U(Element of BOOLEAN,Element of BOOLEAN,Element of BOOLEAN) =
'not' ('not' $1 'or' 'not' $2 'or' $3);
thus for t1,t2 being Function of 3-tuples_on BOOLEAN, BOOLEAN st (for x,y,
z being Element of BOOLEAN holds t1.<*x,y,z*> = U(x,y,z)) & (for x,y,z being
Element of BOOLEAN holds t2.<*x,y,z*> = U(x,y,z)) holds t1 = t2 from FACIRC_1:
sch 5;
end;
end;
Lm7:
for x,y,z being Element of BOOLEAN
holds nor3.<*x,y,z*> = 'not' x '&' 'not' y '&' 'not' z
proof let x,y,z be Element of BOOLEAN;
thus nor3.<*x,y,z*> = 'not' (x 'or' y 'or' z) by Def17
.= 'not' x '&' 'not' y '&' 'not' z;
end;
Lm8:
for x,y,z being Element of BOOLEAN
holds and3.<*x,y,z*> = 'not' ('not' x 'or' 'not' y 'or' 'not' z) by Def9;
::$CD
definition
func xor3 -> Function of 3-tuples_on BOOLEAN, BOOLEAN means
: Def20:
for x,y ,z being Element of BOOLEAN holds it.<*x,y,z*> = x 'xor' y 'xor' z;
existence
proof
deffunc U(Element of BOOLEAN,Element of BOOLEAN,Element of BOOLEAN) = $1
'xor' $2 'xor' $3;
thus ex t being Function of 3-tuples_on BOOLEAN, BOOLEAN st for x,y,z
being Element of BOOLEAN holds t.<*x,y,z*> = U(x,y,z) from FACIRC_1:sch 4;
end;
uniqueness
proof
deffunc U(Element of BOOLEAN,Element of BOOLEAN,Element of BOOLEAN) = $1
'xor' $2 'xor' $3;
thus for t1,t2 being Function of 3-tuples_on BOOLEAN, BOOLEAN st (for x,y,
z being Element of BOOLEAN holds t1.<*x,y,z*> = U(x,y,z)) & (for x,y,z being
Element of BOOLEAN holds t2.<*x,y,z*> = U(x,y,z)) holds t1 = t2 from FACIRC_1:
sch 5;
end;
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 & nor3.<*x,y,z*> = 'not' x '&' 'not' y '&' 'not' z by Def9,Def10
,Def11,Lm7;
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) & or3.<*x,y,z*>='not' ('not' x '&' 'not' y
'&' 'not' z) by Def12,Def13,Def14,Lm5;
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 & nand3.<*x,y,z*> = 'not' x 'or' 'not' y 'or' 'not' z
by FACIRC_1:def 7
,Def15,Def16,Lm6;
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) & and3.<*x,y,z*>='not' ('not' x 'or' 'not'
y 'or' 'not' z) by Def17,Def18,Def19,Lm8;
theorem
for x,y,z being Element of BOOLEAN holds
and3a.<*x,y,z*> = nor3b.<*z,y,x*> & and3b.<*x,y,z*> = nor3a.<*z,y,x*>
proof
let x,y,z be Element of BOOLEAN;
thus and3a.<*x,y,z*> = 'not' ('not' 'not' ('not' 'not' x 'or' 'not' y) 'or'
'not' z) by Def10
.= 'not' (('not' z 'or' 'not' y) 'or' x)
.= nor3b.<*z,y,x*> by Def19;
thus and3b.<*x,y,z*> = 'not' ('not' 'not' ('not' 'not' x 'or' 'not' 'not' y)
'or' 'not' z) by Def11
.= 'not' (('not' z 'or' y) 'or' x)
.= nor3a.<*z,y,x*> by Def18;
end;
theorem
for x,y,z being Element of BOOLEAN holds
or3a.<*x,y,z*> = nand3b.<*z,y,x*> & or3b.<*x,y,z*> = nand3a.<*z,y,x*>
proof
let x,y,z be Element of BOOLEAN;
thus or3a.<*x,y,z*> = 'not' x 'or' y 'or' z by Def15
.= 'not' ('not' z '&' 'not' y '&' x)
.= nand3b.<*z,y,x*> by Def14;
thus or3b.<*x,y,z*> = 'not' x 'or' 'not' y 'or' z by Def16
.= 'not' ('not' z '&' y '&' x)
.= nand3a.<*z,y,x*> by Def13;
end;
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
proof
thus and3.<*0,0,0*> = FALSE '&' FALSE '&' FALSE by Def9
.= 0;
thus and3.<*0,0,1*> = FALSE '&' FALSE '&' TRUE by Def9
.= 0;
thus and3.<*0,1,0*> = FALSE '&' TRUE '&' FALSE by Def9
.= 0;
thus and3.<*0,1,1*> = FALSE '&' TRUE by Def9
.= 0;
thus and3.<*1,0,0*> = TRUE '&' FALSE '&' FALSE by Def9
.= 0;
thus and3.<*1,0,1*> = FALSE '&' TRUE by Def9
.= 0;
thus and3.<*1,1,0*> = TRUE '&' TRUE '&' FALSE by Def9
.= 0;
thus and3.<*1,1,1*> = TRUE '&' TRUE by Def9
.= 1;
end;
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
proof
thus and3a.<*0,0,0*> = 'not' FALSE '&' FALSE '&' FALSE by Def10
.= 0;
thus and3a.<*0,0,1*> = 'not' FALSE '&' FALSE '&' TRUE by Def10
.= 0;
thus and3a.<*0,1,0*> = 'not' FALSE '&' TRUE '&' FALSE by Def10
.= 0;
thus and3a.<*0,1,1*> = ('not' FALSE '&' TRUE) '&' TRUE by Def10
.= 1;
thus and3a.<*1,0,0*> = 'not' TRUE '&' FALSE '&' FALSE by Def10
.= 0;
thus and3a.<*1,0,1*> = 'not' TRUE '&' FALSE '&' TRUE by Def10
.= 0;
thus and3a.<*1,1,0*> = 'not' TRUE '&' TRUE '&' FALSE by Def10
.= 0;
thus and3a.<*1,1,1*> = 'not' TRUE '&' TRUE by Def10
.= 0;
end;
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
proof
thus and3b.<*0,0,0*> = 'not' FALSE '&' 'not' FALSE '&' FALSE by Def11
.= 0;
thus and3b.<*0,0,1*> = TRUE '&' 'not' FALSE '&' TRUE by Def11
.= 1;
thus and3b.<*0,1,0*> = 'not' FALSE '&' 'not' TRUE '&' FALSE by Def11
.= 0;
thus and3b.<*0,1,1*> = 'not' FALSE '&' 'not' TRUE '&' TRUE by Def11
.= 0;
thus and3b.<*1,0,0*> = 'not' TRUE '&' 'not' FALSE '&' FALSE by Def11
.= 0;
thus and3b.<*1,0,1*> = 'not' TRUE '&' 'not' FALSE '&' TRUE by Def11
.= 0;
thus and3b.<*1,1,0*> = 'not' TRUE '&' 'not' TRUE '&' FALSE by Def11
.= 0;
thus and3b.<*1,1,1*> = FALSE '&' 'not' TRUE '&' TRUE by Def11
.= 0;
end;
theorem
nor3.<*0,0,0*>=1 & nor3.<*0,0,1*>=0 & nor3.<*0,1,0*>=0 & nor3.<*0,
1,1*>=0 & nor3.<*1,0,0*>=0 & nor3.<*1,0,1*>=0 & nor3.<*1,1,0*>=0 & nor3.<*1
,1,1*>=0
proof
thus nor3.<*0,0,0*> = TRUE '&' 'not' FALSE '&' 'not' FALSE by Lm7
.= 1;
thus nor3.<*0,0,1*> = 'not' FALSE '&' 'not' FALSE '&' 'not' TRUE by Lm7
.= 0;
thus nor3.<*0,1,0*> = 'not' FALSE '&' 'not' TRUE '&' 'not' FALSE by Lm7
.= 0;
thus nor3.<*0,1,1*> = 'not' FALSE '&' 'not' TRUE '&' FALSE by Lm7
.= 0;
thus nor3.<*1,0,0*> = 'not' TRUE '&' 'not' FALSE '&' 'not' FALSE by Lm7
.= 0;
thus nor3.<*1,0,1*> = 'not' TRUE '&' 'not' FALSE '&' FALSE by Lm7
.= 0;
thus nor3.<*1,1,0*> = FALSE '&' 'not' TRUE '&' 'not' FALSE by Lm7
.= 0;
thus nor3.<*1,1,1*> = 'not' TRUE '&' 'not' TRUE '&' FALSE by Lm7
.= 0;
end;
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
proof
thus or3.<*0,0,0*> = FALSE 'or' FALSE by FACIRC_1:def 7
.= 0;
thus or3.<*0,0,1*> = FALSE 'or' FALSE 'or' TRUE by FACIRC_1:def 7
.= 1;
thus or3.<*0,1,0*> = TRUE 'or' FALSE by FACIRC_1:def 7
.= 1;
thus or3.<*0,1,1*> = FALSE 'or' TRUE 'or' TRUE by FACIRC_1:def 7
.= 1;
thus or3.<*1,0,0*> = TRUE 'or' FALSE by FACIRC_1:def 7
.= 1;
thus or3.<*1,0,1*> = TRUE 'or' FALSE 'or' TRUE by FACIRC_1:def 7
.= 1;
thus or3.<*1,1,0*> = TRUE 'or' TRUE 'or' FALSE by FACIRC_1:def 7
.= 1;
thus or3.<*1,1,1*> = TRUE 'or' TRUE 'or' TRUE by FACIRC_1:def 7
.= 1;
end;
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
proof
thus or3a.<*0,0,0*> = 'not' FALSE 'or' FALSE by Def15
.= 1;
thus or3a.<*0,0,1*> = 'not' FALSE 'or' FALSE 'or' TRUE by Def15
.= 1;
thus or3a.<*0,1,0*> = 'not' FALSE 'or' TRUE 'or' FALSE by Def15
.= 1;
thus or3a.<*0,1,1*> = 'not' FALSE 'or' TRUE 'or' TRUE by Def15
.= 1;
thus or3a.<*1,0,0*> = 'not' TRUE 'or' FALSE by Def15
.= 0;
thus or3a.<*1,0,1*> = 'not' TRUE 'or' FALSE 'or' TRUE by Def15
.= 1;
thus or3a.<*1,1,0*> = TRUE 'or' FALSE by Def15
.= 1;
thus or3a.<*1,1,1*> = 'not' TRUE 'or' TRUE 'or' TRUE by Def15
.= 1;
end;
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
proof
thus or3b.<*0,0,0*> = TRUE 'or' 'not' FALSE 'or' FALSE by Def16
.= 1;
thus or3b.<*0,0,1*> = 'not' FALSE 'or' 'not' FALSE 'or' TRUE by Def16
.= 1;
thus or3b.<*0,1,0*> = 'not' FALSE 'or' 'not' TRUE by Def16
.= 1;
thus or3b.<*0,1,1*> = 'not' FALSE 'or' 'not' TRUE 'or' TRUE by Def16
.= 1;
thus or3b.<*1,0,0*> = 'not' TRUE 'or' 'not' FALSE by Def16
.= 1;
thus or3b.<*1,0,1*> = 'not' TRUE 'or' 'not' FALSE 'or' TRUE by Def16
.= 1;
thus or3b.<*1,1,0*> = 'not' TRUE 'or' 'not' TRUE by Def16
.= 0;
thus or3b.<*1,1,1*> = 'not' TRUE 'or' 'not' TRUE 'or' TRUE by Def16
.= 1;
end;
theorem
nand3.<*0,0,0*> = 1 & nand3.<*0,0,1*> = 1 & nand3.<*0,1,0*> = 1 & nand3.<*
0,1,1*> = 1 & nand3.<*1,0,0*> = 1 & nand3.<*1,0,1*> = 1 &
nand3.<*1,1,0*> = 1 & nand3.<*1,1,1*> = 0
proof
thus nand3.<*0,0,0*> = 'not' FALSE 'or' 'not' FALSE 'or' TRUE by Lm6
.= 1;
thus nand3.<*0,0,1*> = 'not' FALSE 'or' 'not' FALSE 'or' FALSE by Lm6
.= 1;
thus nand3.<*0,1,0*> = 'not' FALSE 'or' 'not' TRUE 'or' TRUE by Lm6
.= 1;
thus nand3.<*0,1,1*> = TRUE 'or' 'not' TRUE 'or' 'not' TRUE by Lm6
.= 1;
thus nand3.<*1,0,0*> = 'not' TRUE 'or' 'not' FALSE 'or' TRUE by Lm6
.= 1;
thus nand3.<*1,0,1*> = 'not' TRUE 'or' TRUE 'or' 'not' TRUE by Lm6
.= 1;
thus nand3.<*1,1,0*> = 'not' TRUE 'or' 'not' TRUE 'or' TRUE by Lm6
.= 1;
thus nand3.<*1,1,1*> = FALSE 'or' 'not' TRUE 'or' 'not' TRUE by Lm6
.= 0;
end;
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
proof
thus xor3.<*0,0,0*> = FALSE 'xor' FALSE by Def20
.= 0;
thus xor3.<*0,0,1*> = FALSE 'xor' FALSE 'xor' TRUE by Def20
.= 1;
thus xor3.<*0,1,0*> = 1 by Def20,BINARITH:13;
thus xor3.<*0,1,1*> = TRUE 'xor' TRUE by Def20,BINARITH:13
.= 0;
thus xor3.<*1,0,0*> = 1 by Def20,BINARITH:13;
thus xor3.<*1,0,1*> = TRUE 'xor' TRUE by Def20,BINARITH:13
.= 0;
thus xor3.<*1,1,0*> = TRUE 'xor' TRUE 'xor' FALSE by Def20
.= 0;
thus xor3.<*1,1,1*> = TRUE 'xor' TRUE 'xor' TRUE by Def20
.= 1;
end;
begin :: 2's Complement Circuit Properties
::---------------------------------------------------------------------------
:: 1bit 2's Complement Circuit (Complementor + Incrementor)
::---------------------------------------------------------------------------
:: Complementor
definition
let x,b be set;
func CompStr(x,b) -> unsplit gate`1=arity gate`2isBoolean non void strict
non empty ManySortedSign equals
1GateCircStr(<*x,b*>,xor2a);
correctness;
end;
definition
let x,b be set;
func CompCirc(x,b) -> strict Boolean gate`2=den Circuit of CompStr(x,b)
equals
1GateCircuit(x,b,xor2a);
coherence;
end;
definition
let x,b be set;
func CompOutput(x,b) -> Element of InnerVertices CompStr(x,b) equals
[<*x,b
*>,xor2a];
coherence by FACIRC_1:47;
end;
:: Incrementor
definition
let x,b be set;
func IncrementStr(x,b) -> unsplit gate`1=arity gate`2isBoolean non void
strict non empty ManySortedSign equals
1GateCircStr(<*x,b*>,and2a);
correctness;
end;
definition
let x,b be set;
func IncrementCirc(x,b) -> strict Boolean gate`2=den Circuit of IncrementStr
(x,b) equals
1GateCircuit(x,b,and2a);
coherence;
end;
definition
let x,b be set;
func IncrementOutput(x,b) -> Element of InnerVertices IncrementStr(x,b)
equals
[<*x,b*>,and2a];
coherence by FACIRC_1:47;
end;
:: 2's-BitComplementor
definition
let x,b be set;
func BitCompStr(x,b) -> unsplit gate`1=arity gate`2isBoolean non void strict
non empty ManySortedSign equals
CompStr(x,b) +* IncrementStr(x,b);
correctness;
end;
definition
let x,b be set;
func BitCompCirc(x,b) -> strict Boolean gate`2=den Circuit of BitCompStr(x,b
) equals
CompCirc(x,b) +* IncrementCirc(x,b);
coherence;
end;
theorem Th27:
for x,b being non pair set holds the carrier of CompStr(x,b) = {
x,b} \/ {[<*x,b*>,xor2a]}
proof
let x,b be non pair set;
set p = <*x,b*>;
rng p = {x,b} by FINSEQ_2:127;
hence thesis by CIRCCOMB:def 6;
end;
theorem
for x,b being non pair set holds [<*x,b*>,xor2a] in InnerVertices
CompStr(x,b)
proof
let x,b be non pair set;
InnerVertices CompStr(x,b) = {[<*x,b*>,xor2a]} by CIRCCOMB:42;
hence thesis by TARSKI:def 1;
end;
theorem
for x,b being non pair set holds x in InputVertices CompStr(x,b) & b
in InputVertices CompStr(x,b)
proof
let x,b be non pair set;
InputVertices CompStr(x,b) = {x,b} by FACIRC_1:40;
hence thesis by TARSKI:def 2;
end;
theorem
for x,b being non pair set holds InputVertices CompStr(x,b) is without_pairs
proof
let x,b be non pair set;
InputVertices CompStr(x,b) = {x,b} by FACIRC_1:40;
hence thesis;
end;
theorem Th31:
for x,b being non pair set holds the carrier of IncrementStr(x,b
) = {x,b} \/ {[<*x,b*>,and2a]}
proof
let x,b be non pair set;
set p = <*x,b*>;
rng p = {x,b} by FINSEQ_2:127;
hence thesis by CIRCCOMB:def 6;
end;
theorem
for x,b being non pair set holds [<*x,b*>,and2a] in InnerVertices
IncrementStr(x,b)
proof
let x,b be non pair set;
InnerVertices IncrementStr(x,b) = {[<*x,b*>,and2a]} by CIRCCOMB:42;
hence thesis by TARSKI:def 1;
end;
theorem
for x,b being non pair set holds x in InputVertices IncrementStr(x,b)
& b in InputVertices IncrementStr(x,b)
proof
let x,b be non pair set;
InputVertices IncrementStr(x,b) = {x,b} by FACIRC_1:40;
hence thesis by TARSKI:def 2;
end;
theorem
for x,b being non pair set holds InputVertices IncrementStr(x,b) is
without_pairs
proof
let x,b be non pair set;
InputVertices IncrementStr(x,b) = {x,b} by FACIRC_1:40;
hence thesis;
end;
:: 2's-BitComplementor
theorem
for x,b being non pair set holds InnerVertices BitCompStr(x,b) is Relation
proof
let x,b be non pair set;
set S1 = CompStr(x,b);
set S2 = IncrementStr(x,b);
InnerVertices S1 is Relation & InnerVertices S2 is Relation by FACIRC_1:38;
hence thesis by FACIRC_1:3;
end;
theorem Th36:
for x,b being non pair set holds x in the carrier of BitCompStr(
x,b) & b in the carrier of BitCompStr(x,b) & [<*x,b*>,xor2a] in the carrier of
BitCompStr(x,b) & [<*x,b*>,and2a] in the carrier of BitCompStr(x,b)
proof
let x,b be non pair set;
set p = <*x,b*>;
set S1 = CompStr(x,b);
set S2 = IncrementStr(x,b);
A1: [p,xor2a] in the carrier of S1 & [p,and2a] in the carrier of S2 by
FACIRC_1:43;
x in the carrier of S1 & b in the carrier of S1 by FACIRC_1:43;
hence thesis by A1,FACIRC_1:20;
end;
theorem Th37:
for x,b being non pair set holds the carrier of BitCompStr(x,b)
= {x,b} \/ {[<*x,b*>,xor2a],[<*x,b*>,and2a]}
proof
let x,b be non pair set;
set p = <*x,b*>;
set S1 = CompStr(x,b);
set S2 = IncrementStr(x,b);
the carrier of S1 = {x,b} \/ {[p,xor2a]} & the carrier of S2 = {x,b} \/
{[p, and2a]} by Th27,Th31;
then
the carrier of BitCompStr(x,b) = ({x,b} \/ {[p,xor2a]}) \/ ({x,b} \/ {[p
,and2a]}) by CIRCCOMB:def 2
.= {x,b} \/ ({x,b} \/ {[p,xor2a]}) \/ {[p,and2a]} by XBOOLE_1:4
.= ({x,b} \/ {x,b}) \/ {[p,xor2a]} \/ {[p,and2a]} by XBOOLE_1:4
.= {x,b} \/ ({[p,xor2a]} \/ {[p,and2a]}) by XBOOLE_1:4
.= {x,b} \/ {[p,xor2a],[p,and2a]} by ENUMSET1:1;
hence thesis;
end;
theorem Th38:
for x,b being non pair set holds InnerVertices BitCompStr(x,b) =
{[<*x,b*>,xor2a],[<*x,b*>,and2a]}
proof
let x,b be non pair set;
set p = <*x,b*>;
set S1 = CompStr(x,b);
set S2 = IncrementStr(x,b);
set S = BitCompStr(x,b);
A1: InnerVertices S1 = {[p,xor2a]} & InnerVertices S2 = {[p,and2a]} by
CIRCCOMB:42;
InnerVertices S = (InnerVertices S1) \/ InnerVertices S2 by FACIRC_1:27
.= {[p,xor2a], [p,and2a]} by A1,ENUMSET1:1;
hence thesis;
end;
theorem Th39:
for x,b being non pair set holds [<*x,b*>,xor2a] in
InnerVertices BitCompStr(x,b) & [<*x,b*>,and2a] in InnerVertices BitCompStr(x,b
)
proof
let x,b be non pair set;
InnerVertices BitCompStr(x,b) = {[<*x,b*>,xor2a],[<*x,b*>,and2a]} by Th38;
hence thesis by TARSKI:def 2;
end;
theorem Th40:
for x,b being non pair set holds InputVertices BitCompStr(x,b) = {x,b}
proof
let x,b be non pair set;
set S1 = CompStr(x,b);
set S2 = IncrementStr(x,b);
set S = BitCompStr(x,b);
A1: InputVertices S1 = {x,b} & InputVertices S2 = {x,b} by FACIRC_1:40;
InnerVertices S1 is Relation & InnerVertices S2 is Relation by FACIRC_1:38;
then InputVertices S = {x,b} \/ {x,b} by A1,FACIRC_1:7
.= {x,b};
hence thesis;
end;
theorem Th41:
for x,b being non pair set holds x in InputVertices BitCompStr(x
,b) & b in InputVertices BitCompStr(x,b)
proof
let x,b be non pair set;
InputVertices BitCompStr(x,b) = {x,b} by Th40;
hence thesis by TARSKI:def 2;
end;
theorem
for x,b being non pair set holds InputVertices BitCompStr(x,b) is
without_pairs
proof
let x,b be non pair set;
InputVertices BitCompStr(x,b) = {x,b} by Th40;
hence thesis;
end;
::------------------------------------------------------------------------
:: for s being State of BitCompCirc(x,b) holds (Following s) is stable
::------------------------------------------------------------------------
theorem Th43:
for x,b being non pair set for s being State of CompCirc(x,b)
holds (Following s).CompOutput(x,b) = xor2a.<*s.x,s.b*> & (Following s).x = s.x
& (Following s).b = s.b
proof
let x,b be non pair set;
let s be State of CompCirc(x,b);
set p = <*x,b*>;
set S = CompStr(x,b);
A1: dom s = the carrier of S & x in the carrier of S by CIRCUIT1:3,FACIRC_1:43;
A2: b in the carrier of S by FACIRC_1:43;
InnerVertices S = the carrier' of S by FACIRC_1:37;
hence (Following s).CompOutput(x,b) = xor2a.(s*p) by FACIRC_1:35
.= xor2a.<*s.x,s.b*> by A1,A2,FINSEQ_2:125;
InputVertices S = {x,b} by FACIRC_1:40;
then x in InputVertices S & b in InputVertices S by TARSKI:def 2;
hence thesis by CIRCUIT2:def 5;
end;
theorem
for x,b being non pair set for s being State of CompCirc(x,b) for a1,
a2 being Element of BOOLEAN st a1 = s.x & a2 = s.b holds (Following s).
CompOutput(x,b) = 'not' a1 'xor' a2 & (Following s).x = a1 & (Following s).b =
a2
proof
let x,b be non pair set;
let s be State of CompCirc(x,b);
let a1,a2 be Element of BOOLEAN;
assume
A1: a1 = s.x & a2 = s.b;
thus (Following s).CompOutput(x,b) = xor2a.<*s.x,s.b*> by Th43
.= 'not' a1 'xor' a2 by A1,Def7;
thus thesis by A1,Th43;
end;
theorem Th45:
for x,b being non pair set for s being State of BitCompCirc(x,b)
holds (Following s).CompOutput(x,b) = xor2a.<*s.x,s.b*> & (Following s).x = s.x
& (Following s).b = s.b
proof
let x,b be non pair set;
let s be State of BitCompCirc(x,b);
set p = <*x,b*>;
set S = BitCompStr(x,b);
A1: dom s = the carrier of S & x in the carrier of S by Th36,CIRCUIT1:3;
A2: b in the carrier of S by Th36;
InnerVertices S = the carrier' of S by FACIRC_1:37;
hence (Following s).CompOutput(x,b) = xor2a.(s*p) by Th39,FACIRC_1:35
.= xor2a.<*s.x,s.b*> by A1,A2,FINSEQ_2:125;
x in InputVertices S & b in InputVertices S by Th41;
hence thesis by CIRCUIT2:def 5;
end;
theorem Th46:
for x,b being non pair set for s being State of BitCompCirc(x,b)
for a1,a2 being Element of BOOLEAN st a1 = s.x & a2 = s.b holds (Following s).
CompOutput(x,b) = 'not' a1 'xor' a2 & (Following s).x = a1 & (Following s).b =
a2
proof
let x,b be non pair set;
let s be State of BitCompCirc(x,b);
let a1,a2 be Element of BOOLEAN;
assume
A1: a1 = s.x & a2 = s.b;
thus (Following s).CompOutput(x,b) = xor2a.<*s.x,s.b*> by Th45
.= 'not' a1 'xor' a2 by A1,Def7;
thus thesis by A1,Th45;
end;
theorem Th47:
for x,b being non pair set for s being State of IncrementCirc(x,
b) holds (Following s).IncrementOutput(x,b) = and2a.<*s.x,s.b*> & (Following s)
.x = s.x & (Following s).b = s.b
proof
let x,b be non pair set;
let s be State of IncrementCirc(x,b);
set p = <*x,b*>;
set S = IncrementStr(x,b);
A1: dom s = the carrier of S & x in the carrier of S by CIRCUIT1:3,FACIRC_1:43;
A2: b in the carrier of S by FACIRC_1:43;
InnerVertices S = the carrier' of S by FACIRC_1:37;
hence (Following s).IncrementOutput(x,b) = and2a.(s*p) by FACIRC_1:35
.= and2a.<*s.x,s.b*> by A1,A2,FINSEQ_2:125;
InputVertices S = {x,b} by FACIRC_1:40;
then x in InputVertices S & b in InputVertices S by TARSKI:def 2;
hence thesis by CIRCUIT2:def 5;
end;
theorem
for x,b being non pair set for s being State of IncrementCirc(x,b) for
a1,a2 being Element of BOOLEAN st a1 = s.x & a2 = s.b holds (Following s).
IncrementOutput(x,b) = 'not' a1 '&' a2 & (Following s).x = a1 & (Following s).b
= a2
proof
let x,b be non pair set;
let s be State of IncrementCirc(x,b);
let a1,a2 be Element of BOOLEAN;
assume
A1: a1 = s.x & a2 = s.b;
thus (Following s).IncrementOutput(x,b) = and2a.<*s.x,s.b*> by Th47
.= 'not' a1 '&' a2 by A1,Def1;
thus thesis by A1,Th47;
end;
theorem Th49:
for x,b being non pair set for s being State of BitCompCirc(x,b)
holds (Following s).IncrementOutput(x,b) = and2a.<*s.x,s.b*> & (Following s).x
= s.x & (Following s).b = s.b
proof
let x,b be non pair set;
let s be State of BitCompCirc(x,b);
set p = <*x,b*>;
set S = BitCompStr(x,b);
A1: dom s = the carrier of S & x in the carrier of S by Th36,CIRCUIT1:3;
A2: b in the carrier of S by Th36;
InnerVertices S = the carrier' of S by FACIRC_1:37;
hence (Following s).IncrementOutput(x,b) = and2a.(s*p) by Th39,FACIRC_1:35
.= and2a.<*s.x,s.b*> by A1,A2,FINSEQ_2:125;
InputVertices S = {x,b} by Th40;
then x in InputVertices S & b in InputVertices S by TARSKI:def 2;
hence thesis by CIRCUIT2:def 5;
end;
theorem Th50:
for x,b being non pair set for s being State of BitCompCirc(x,b)
for a1,a2 being Element of BOOLEAN st a1 = s.x & a2 = s.b holds (Following s).
IncrementOutput(x,b) = 'not' a1 '&' a2 & (Following s).x = a1 & (Following s).b
= a2
proof
let x,b be non pair set;
let s be State of BitCompCirc(x,b);
let a1,a2 be Element of BOOLEAN;
assume
A1: a1 = s.x & a2 = s.b;
thus (Following s).IncrementOutput(x,b) = and2a.<*s.x,s.b*> by Th49
.= 'not' a1 '&' a2 by A1,Def1;
thus thesis by A1,Th49;
end;
theorem
for x,b being non pair set for s being State of BitCompCirc(x,b) holds
(Following s).CompOutput(x,b) = xor2a.<*s.x,s.b*> & (Following s).
IncrementOutput(x,b) = and2a.<*s.x,s.b*> & (Following s).x = s.x & (Following s
).b = s.b by Th45,Th49;
theorem
for x,b being non pair set for s being State of BitCompCirc(x,b) for
a1,a2 being Element of BOOLEAN st a1 = s.x & a2 = s.b holds (Following s).
CompOutput(x,b) = 'not' a1 'xor' a2 & (Following s).IncrementOutput(x,b) =
'not' a1 '&' a2 & (Following s).x = a1 & (Following s).b = a2 by Th46,Th50;
theorem
for x,b being non pair set for s being State of BitCompCirc(x,b) holds
(Following s) is stable
proof
let x,b be non pair set;
set p = <*x,b*>;
set S = BitCompStr(x,b);
let s be State of BitCompCirc(x,b);
set s1 = Following s, s2 = Following s1;
A1: the carrier of S = {x,b} \/ {[p,xor2a],[p,and2a]} by Th37;
A2: now
let a be object;
A3: s1.[p,xor2a] = s1.CompOutput(x,b) .= xor2a.<*s.x, s.b*> by Th45;
assume a in the carrier of S;
then a in {x,b} or a in {[p,xor2a],[p,and2a]} by A1,XBOOLE_0:def 3;
then
A4: a = x or a = b or a = [p,xor2a] or a = [p,and2a] by TARSKI:def 2;
A5: s2.[p,and2a] = s2.IncrementOutput(x,b) .= and2a.<*s1.x, s1.b*> by Th49;
A6: s2.[p,xor2a] = s2.CompOutput(x,b) .= xor2a.<*s1.x, s1.b*> by Th45;
A7: s1.[p,and2a] = s1.IncrementOutput(x,b) .= and2a.<*s.x, s.b*> by Th49;
s1.x = s.x by Th45;
hence s2.a = s1.a by A4,A3,A7,A6,A5,Th45;
end;
dom s1 = the carrier of S & dom s2 = the carrier of S by CIRCUIT1:3;
hence Following s = Following Following s by A2,FUNCT_1:2;
end;
theorem
for x,y being Element of BOOLEAN holds nor2.<*x,y*> = 'not' x '&' 'not' y
by Lm3;
theorem
for x,y being Element of BOOLEAN
holds or2.<*x,y*> = 'not' ('not' x '&' 'not' y) by Lm1;
theorem
for x,y being Element of BOOLEAN
holds and2.<*x,y*> = 'not' ('not' x 'or' 'not' y) by Lm4;
theorem
for x,y being Element of BOOLEAN holds nand2.<*x,y*> = 'not' x 'or' 'not' y
by Lm2;
theorem
for x,y,z being Element of BOOLEAN
holds nor3.<*x,y,z*> = 'not' x '&' 'not' y '&' 'not' z by Lm7;
theorem
for x,y,z being Element of BOOLEAN
holds or3.<*x,y,z*> = 'not' ('not' x '&' 'not' y '&' 'not' z) by Lm5;
theorem
for x,y,z being Element of BOOLEAN
holds nand3.<*x,y,z*> = 'not' x 'or' 'not' y 'or' 'not' z by Lm6;
theorem
for x,y,z being Element of BOOLEAN
holds and3.<*x,y,z*> = 'not' ('not' x 'or' 'not' y 'or' 'not' z) by Lm8;