:: Full Adder Circuit. Part { I }
:: by Grzegorz Bancerek and Yatsuka Nakamura
::
:: Received August 10, 1995
:: Copyright (c) 1995-2021 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 NUMBERS, XBOOLE_0, CARD_1, NAT_1, SUBSET_1, ARYTM_3, RELAT_1,
FUNCT_1, FINSEQ_1, CIRCCOMB, FINSEQ_2, MSUALG_1, PARTFUN1, MSAFREE2,
FUNCT_4, TARSKI, STRUCT_0, MARGREL1, XBOOLEAN, CIRCUIT1, FSM_1, CIRCUIT2,
CARD_3, GLIB_000, LATTICES, MCART_1, FINSET_1, CLASSES1, FACIRC_1,
ORDINAL1;
notations TARSKI, XBOOLE_0, ENUMSET1, XTUPLE_0, XFAMILY, SUBSET_1, ORDINAL1,
NUMBERS, XCMPLX_0, MCART_1, RELAT_1, CARD_1, STRUCT_0, FUNCT_1, FUNCT_2,
FINSEQ_1, FINSET_1, FINSEQ_2, FUNCT_4, MARGREL1, BINARITH, CARD_3,
CLASSES1, PARTFUN1, MSUALG_1, MSAFREE2, CIRCUIT1, CIRCUIT2, CIRCCOMB,
XXREAL_0, NAT_1;
constructors ENUMSET1, XXREAL_0, NAT_1, CLASSES1, BINARITH, CIRCUIT1,
CIRCUIT2, CIRCCOMB, RELSET_1, BINOP_1, WELLORD2, DOMAIN_1, XTUPLE_0,
NUMBERS, VALUED_0, XFAMILY;
registrations XBOOLE_0, RELAT_1, FUNCT_1, ORDINAL1, XXREAL_0, FINSEQ_1,
FINSEQ_2, CARD_3, STRUCT_0, MSUALG_1, CIRCCOMB, NAT_1, XCMPLX_0,
MSAFREE2, MARGREL1, FINSET_1, XTUPLE_0;
requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
begin :: Pairs, Set Without Pairs, and Nonpair-yielding Functions
registration
cluster pair -> non empty for set;
end;
registration
cluster non pair for object;
end;
registration
cluster -> non pair for Nat;
end;
definition
::$CD
let IT be set;
attr IT is with_pair means
:: FACIRC_1:def 2
ex x being pair object st x in IT;
end;
notation
let IT be set;
antonym IT is without_pairs for IT is with_pair;
end;
registration
cluster empty -> without_pairs for set;
let x be non pair object;
cluster {x} -> without_pairs;
let y be non pair object;
cluster {x,y} -> without_pairs;
let z be non pair object;
cluster {x,y,z} -> without_pairs;
end;
registration
cluster without_pairs for non empty set;
end;
registration
let X, Y be without_pairs set;
cluster X \/ Y -> without_pairs;
end;
registration
let X be without_pairs set, Y be set;
cluster X \ Y -> without_pairs;
cluster X /\ Y -> without_pairs;
cluster Y /\ X -> without_pairs;
end;
registration
let x be pair object;
cluster {x} -> Relation-like;
let y be pair object;
cluster {x,y} -> Relation-like;
let z be pair object;
cluster {x,y,z} -> Relation-like;
end;
registration
cluster without_pairs Relation-like -> empty for set;
end;
definition
let IT be Function;
attr IT is nonpair-yielding means
:: FACIRC_1:def 3
for x being set st x in dom IT holds IT.x is non pair;
end;
registration
let x be non pair object;
cluster <*x*> -> nonpair-yielding;
let y be non pair object;
cluster <*x,y*> -> nonpair-yielding;
let z be non pair object;
cluster <*x,y,z*> -> nonpair-yielding;
end;
theorem :: FACIRC_1:1
for f being Function st f is nonpair-yielding holds rng f is without_pairs;
registration
let n be Nat;
cluster one-to-one nonpair-yielding for FinSeqLen of n;
end;
registration
cluster one-to-one nonpair-yielding for FinSequence;
end;
registration
let f be nonpair-yielding Function;
cluster rng f -> without_pairs;
end;
theorem :: FACIRC_1:2
for S1,S2 being non empty ManySortedSign st S1 tolerates S2 &
InnerVertices S1 is Relation & InnerVertices S2 is Relation holds InnerVertices
(S1+*S2) is Relation;
theorem :: FACIRC_1:3
for S1,S2 being unsplit gate`1=arity non empty ManySortedSign st
InnerVertices S1 is Relation & InnerVertices S2 is Relation holds InnerVertices
(S1+*S2) is Relation;
theorem :: FACIRC_1:4
for S1,S2 being non empty ManySortedSign st S1 tolerates S2 &
InnerVertices S2 misses InputVertices S1 holds InputVertices S1 c=
InputVertices (S1+*S2) & InputVertices (S1+*S2) = (InputVertices S1) \/ (
InputVertices S2 \ InnerVertices S1);
theorem :: FACIRC_1:5
for X,R being set st X is without_pairs & R is Relation holds X misses R;
theorem :: FACIRC_1:6
for S1,S2 being unsplit gate`1=arity non empty ManySortedSign st
InputVertices S1 is without_pairs & InnerVertices S2 is Relation holds
InputVertices S1 c= InputVertices (S1+*S2) & InputVertices (S1+*S2) = (
InputVertices S1) \/ (InputVertices S2 \ InnerVertices S1);
theorem :: FACIRC_1:7
for S1,S2 being unsplit gate`1=arity non empty ManySortedSign st
InputVertices S1 is without_pairs & InnerVertices S1 is Relation &
InputVertices S2 is without_pairs & InnerVertices S2 is Relation holds
InputVertices (S1+*S2) = (InputVertices S1) \/ (InputVertices S2);
theorem :: FACIRC_1:8
for S1,S2 being non empty ManySortedSign st S1 tolerates S2 &
InputVertices S1 is without_pairs & InputVertices S2 is without_pairs holds
InputVertices (S1+*S2) is without_pairs;
theorem :: FACIRC_1:9
for S1,S2 being unsplit gate`1=arity non empty ManySortedSign st
InputVertices S1 is without_pairs & InputVertices S2 is without_pairs holds
InputVertices (S1+*S2) is without_pairs;
begin :: Boolean Operations
definition
let i be Nat, D be non empty set;
mode Tuple of i,D is Element of i-tuples_on D;
end;
scheme :: FACIRC_1:sch 1
2AryBooleEx {F(set,set) -> Element of BOOLEAN}: ex f being Function of 2
-tuples_on BOOLEAN, BOOLEAN st for x,y being Element of BOOLEAN holds f.<*x,y*>
= F(x,y);
scheme :: FACIRC_1:sch 2
2AryBooleUniq {F(set,set) -> Element of BOOLEAN}: for f1,f2 being Function
of 2-tuples_on BOOLEAN, BOOLEAN st (for x,y being Element of BOOLEAN holds f1.
<*x,y*> = F(x,y)) & (for x,y being Element of BOOLEAN holds f2.<*x,y*> = F(x,y)
) holds f1 = f2;
scheme :: FACIRC_1:sch 3
2AryBooleDef {F(set,set) -> Element of BOOLEAN}: (ex f being Function of 2
-tuples_on BOOLEAN, BOOLEAN st for x,y being Element of BOOLEAN holds f.<*x,y*>
= F(x,y)) & for f1,f2 being Function of 2-tuples_on BOOLEAN, BOOLEAN st (for x,
y being Element of BOOLEAN holds f1.<*x,y*> = F(x,y)) & (for x,y being Element
of BOOLEAN holds f2.<*x,y*> = F(x,y)) holds f1 = f2;
scheme :: FACIRC_1:sch 4
3AryBooleEx {F(set,set,set) -> Element of BOOLEAN}: ex f being Function of 3
-tuples_on BOOLEAN, BOOLEAN st for x,y,z being Element of BOOLEAN holds f.<*x,y
,z*> = F(x,y,z);
scheme :: FACIRC_1:sch 5
3AryBooleUniq {F(set,set,set) -> Element of BOOLEAN}: for f1,f2 being
Function of 3-tuples_on BOOLEAN, BOOLEAN st (for x,y,z being Element of BOOLEAN
holds f1.<*x,y,z*> = F(x,y,z)) & (for x,y,z being Element of BOOLEAN holds f2.
<*x,y,z*> = F(x,y,z)) holds f1 = f2;
scheme :: FACIRC_1:sch 6
3AryBooleDef {F(set,set,set) -> Element of BOOLEAN}: (ex f being Function of
3-tuples_on BOOLEAN, BOOLEAN st for x,y,z being Element of BOOLEAN holds f.<*x,
y,z*> = F(x,y,z)) & for f1,f2 being Function of 3-tuples_on BOOLEAN, BOOLEAN st
(for x,y,z being Element of BOOLEAN holds f1.<*x,y,z*> = F(x,y,z)) & (for x,y,z
being Element of BOOLEAN holds f2.<*x,y,z*> = F(x,y,z)) holds f1 = f2;
definition
func 'xor' -> Function of 2-tuples_on BOOLEAN, BOOLEAN means
:: FACIRC_1:def 4
for x,y being Element of BOOLEAN holds it.<*x,y*> = x 'xor' y;
func 'or' -> Function of 2-tuples_on BOOLEAN, BOOLEAN means
:: FACIRC_1:def 5
for x,y being Element of BOOLEAN holds it.<*x,y*> = x 'or' y;
func '&' -> Function of 2-tuples_on BOOLEAN, BOOLEAN means
:: FACIRC_1:def 6
for x,y being Element of BOOLEAN holds it.<*x,y*> = x '&' y;
end;
definition
func or3 -> Function of 3-tuples_on BOOLEAN, BOOLEAN means
:: FACIRC_1:def 7
for x,y,z being Element of BOOLEAN holds it.<*x,y,z*> = x 'or' y 'or' z;
end;
begin :: Computation and Stabilizable
theorem :: FACIRC_1:10
for S being Circuit-like non void non empty ManySortedSign for
A being non-empty Circuit of S for s being State of A, g being Gate of S holds
(Following s).the_result_sort_of g = Den(g, A).(s*the_arity_of g);
definition
let S be non void Circuit-like non empty ManySortedSign;
let A be non-empty Circuit of S;
let s be State of A;
let n be natural Number;
func Following(s,n) -> State of A means
:: FACIRC_1:def 8
ex f being sequence of product the Sorts of A st it = f.n & f.0 = s &
for n being Nat holds f.(n+1) = Following f.n;
end;
theorem :: FACIRC_1:11
for S being Circuit-like non void non empty ManySortedSign for
A being non-empty Circuit of S, s being State of A holds Following(s,0) = s;
theorem :: FACIRC_1:12
for S being Circuit-like non void non empty ManySortedSign for
A being non-empty Circuit of S, s being State of A for n being Nat holds
Following(s,n+1) = Following Following(s,n);
theorem :: FACIRC_1:13
for S being Circuit-like non void non empty ManySortedSign for
A being non-empty Circuit of S, s being State of A for n,m being Nat holds
Following(s,n+m) = Following(Following(s,n),m);
theorem :: FACIRC_1:14
for S being non void Circuit-like non empty ManySortedSign for
A being non-empty Circuit of S, s being State of A holds Following(s,1) =
Following s;
theorem :: FACIRC_1:15
for S being non void Circuit-like non empty ManySortedSign for
A being non-empty Circuit of S, s being State of A holds Following(s,2) =
Following Following s;
theorem :: FACIRC_1:16
for S being Circuit-like non void non empty ManySortedSign for
A being non-empty Circuit of S, s being State of A for n being Nat holds
Following(s,n+1) = Following(Following s, n);
definition
let S be non void Circuit-like non empty ManySortedSign;
let A be non-empty Circuit of S;
let s be State of A;
let x be object;
pred s is_stable_at x means
:: FACIRC_1:def 9
for n being Nat holds (Following(s,n)).x = s.x;
end;
theorem :: FACIRC_1:17
for S being non void Circuit-like non empty ManySortedSign for A
being non-empty Circuit of S, s being State of A for x being set st s
is_stable_at x for n being Nat holds Following(s,n) is_stable_at x;
theorem :: FACIRC_1:18
for S being non void Circuit-like non empty ManySortedSign for A
being non-empty Circuit of S, s being State of A for x being set st x in
InputVertices S holds s is_stable_at x;
theorem :: FACIRC_1:19
for S being non void Circuit-like non empty ManySortedSign for
A being non-empty Circuit of S, s being State of A for g being Gate of S st for
x being set st x in rng the_arity_of g holds s is_stable_at x holds Following s
is_stable_at the_result_sort_of g;
begin :: Combined Circuits
theorem :: FACIRC_1:20
for S1,S2 being non empty ManySortedSign, v being Vertex of S1
holds v in the carrier of S1+*S2 & v in the carrier of S2+*S1;
theorem :: FACIRC_1:21
for S1,S2 being unsplit gate`1=arity non empty ManySortedSign
for x being set st x in InnerVertices S1 holds x in InnerVertices (S1+*S2) & x
in InnerVertices (S2+*S1);
theorem :: FACIRC_1:22
for S1,S2 being non empty ManySortedSign for x being set st x in
InnerVertices S2 holds x in InnerVertices (S1+*S2);
theorem :: FACIRC_1:23
for S1,S2 being unsplit gate`1=arity non empty ManySortedSign holds S1
+*S2 = S2+*S1;
theorem :: FACIRC_1:24
for S1,S2 being unsplit gate`1=arity gate`2isBoolean non void non
empty ManySortedSign for A1 being Boolean gate`2=den Circuit of S1 for A2 being
Boolean gate`2=den Circuit of S2 holds A1+*A2 = A2+*A1;
theorem :: FACIRC_1:25
for S1,S2,S3 be unsplit gate`1=arity gate`2isBoolean non void
non empty ManySortedSign for A1 being Boolean Circuit of S1, A2 being Boolean
Circuit of S2 for A3 being Boolean Circuit of S3 holds (A1+*A2)+*A3 = A1+*(A2+*
A3);
theorem :: FACIRC_1:26
for S1,S2 being unsplit gate`1=arity gate`2isBoolean non void
non empty ManySortedSign for A1 being Boolean gate`2=den non-empty Circuit of
S1 for A2 being Boolean gate`2=den non-empty Circuit of S2 for s being State of
A1+*A2 holds s|the carrier of S1 is State of A1 & s|the carrier of S2 is State
of A2;
theorem :: FACIRC_1:27
for S1,S2 being unsplit gate`1=arity non empty ManySortedSign
holds InnerVertices (S1+*S2) = (InnerVertices S1) \/ InnerVertices S2;
theorem :: FACIRC_1:28
for S1,S2 being unsplit gate`1=arity gate`2isBoolean non void
non empty ManySortedSign st InnerVertices S2 misses InputVertices S1 for A1
being Boolean gate`2=den Circuit of S1 for A2 being Boolean gate`2=den Circuit
of S2 for s being State of A1+*A2, s1 being State of A1 st s1 = s|the carrier
of S1 holds (Following s)|the carrier of S1 = Following s1;
theorem :: FACIRC_1:29
for S1,S2 being unsplit gate`1=arity gate`2isBoolean non void
non empty ManySortedSign st InnerVertices S1 misses InputVertices S2 for A1
being Boolean gate`2=den Circuit of S1 for A2 being Boolean gate`2=den Circuit
of S2 for s being State of A1+*A2, s2 being State of A2 st s2 = s|the carrier
of S2 holds (Following s)|the carrier of S2 = Following s2;
theorem :: FACIRC_1:30
for S1,S2 being unsplit gate`1=arity gate`2isBoolean non void
non empty ManySortedSign st InnerVertices S2 misses InputVertices S1 for A1
being Boolean gate`2=den Circuit of S1 for A2 being Boolean gate`2=den Circuit
of S2 for s being State of A1+*A2, s1 being State of A1 st s1 = s|the carrier
of S1 for n being Nat holds Following(s,n)|the carrier of S1 = Following(s1,n);
theorem :: FACIRC_1:31
for S1,S2 being unsplit gate`1=arity gate`2isBoolean non void
non empty ManySortedSign st InnerVertices S1 misses InputVertices S2 for A1
being Boolean gate`2=den Circuit of S1 for A2 being Boolean gate`2=den Circuit
of S2 for s being State of A1+*A2, s2 being State of A2 st s2 = s|the carrier
of S2 for n being Nat holds Following(s,n)|the carrier of S2 = Following(s2,n);
theorem :: FACIRC_1:32
for S1,S2 being unsplit gate`1=arity gate`2isBoolean non void
non empty ManySortedSign st InnerVertices S2 misses InputVertices S1 for A1
being Boolean gate`2=den Circuit of S1 for A2 being Boolean gate`2=den Circuit
of S2 for s being State of A1+*A2, s1 being State of A1 st s1 = s|the carrier
of S1 holds for v being set st v in the carrier of S1 for n being Nat holds (
Following(s,n)).v = (Following(s1,n)).v;
theorem :: FACIRC_1:33
for S1,S2 being unsplit gate`1=arity gate`2isBoolean non void
non empty ManySortedSign st InnerVertices S1 misses InputVertices S2 for A1
being Boolean gate`2=den Circuit of S1 for A2 being Boolean gate`2=den Circuit
of S2 for s being State of A1+*A2, s2 being State of A2 st s2 = s|the carrier
of S2 holds for v being set st v in the carrier of S2 for n being Nat holds (
Following(s,n)).v = (Following(s2,n)).v;
registration
let S be gate`2=den non void non empty ManySortedSign;
let g be Gate of S;
cluster g`2 -> Function-like Relation-like for set;
end;
theorem :: FACIRC_1:34
for S being gate`2=den Circuit-like non void non empty
ManySortedSign for A being non-empty Circuit of S st A is gate`2=den for s
being State of A, g being Gate of S holds (Following s).the_result_sort_of g =
g`2.(s*the_arity_of g);
theorem :: FACIRC_1:35
for S being gate`1=arity gate`2isBoolean unsplit non void non
empty ManySortedSign for A being Boolean gate`2=den non-empty Circuit of S for
s being State of A, p being FinSequence, f being Function st [p,f] in the
carrier' of S holds (Following s).[p,f] = f.(s*p);
theorem :: FACIRC_1:36
for S being gate`1=arity gate`2isBoolean unsplit non void non empty
ManySortedSign for A being Boolean gate`2=den non-empty Circuit of S for s
being State of A, p being FinSequence, f being Function st [p,f] in the
carrier' of S & for x being set st x in rng p holds s is_stable_at x holds
Following s is_stable_at [p,f];
theorem :: FACIRC_1:37
for S being unsplit non empty ManySortedSign holds InnerVertices
S = the carrier' of S;
begin :: One Gate Circuit
theorem :: FACIRC_1:38
for f being set, p being FinSequence holds InnerVertices
1GateCircStr(p,f) is Relation;
theorem :: FACIRC_1:39
for f being set, p being nonpair-yielding FinSequence holds
InputVertices 1GateCircStr(p,f) is without_pairs;
theorem :: FACIRC_1:40
for f,x,y being object holds InputVertices 1GateCircStr(
<*x,y*>,f) = {x,y};
theorem :: FACIRC_1:41
for f being set, x,y being non pair object holds InputVertices
1GateCircStr(<*x,y*>,f) is without_pairs;
theorem :: FACIRC_1:42
for f,x,y,z being object holds InputVertices
1GateCircStr(<*x,y,z*>,f) = {x,y,z};
theorem :: FACIRC_1:43
for x,y,f being object holds x in the carrier of 1GateCircStr(<*x,y
*>,f) & y in the carrier of 1GateCircStr(<*x,y*>,f) & [<*x,y*>,f] in the
carrier of 1GateCircStr(<*x,y*>,f);
theorem :: FACIRC_1:44
for x,y,z,f being object holds x in the carrier of 1GateCircStr(<*x
,y,z*>,f) & y in the carrier of 1GateCircStr(<*x,y,z*>,f) & z in the carrier of
1GateCircStr(<*x,y,z*>,f);
theorem :: FACIRC_1:45
for f,x being set, p being FinSequence holds x in the carrier of
1GateCircStr(p,f,x) & for y being set st y in rng p holds y in the carrier of
1GateCircStr(p,f,x);
theorem :: FACIRC_1:46
for f,x being set, p being FinSequence holds 1GateCircStr(p,f,x) is
gate`1=arity Circuit-like;
theorem :: FACIRC_1:47
for p being FinSequence, f be set holds [p,f] in InnerVertices
1GateCircStr(p,f);
definition
let x,y be object;
let f be Function of 2-tuples_on BOOLEAN, BOOLEAN;
func 1GateCircuit(x,y,f) -> Boolean gate`2=den strict Circuit of
1GateCircStr(<*x,y*>, f) equals
:: FACIRC_1:def 10
1GateCircuit(<*x,y*> qua FinSeqLen of 2, f);
end;
reserve x,y,z,c for object,
f for Function of 2-tuples_on BOOLEAN, BOOLEAN;
theorem :: FACIRC_1:48
for X being finite non empty set, f being Function of 2
-tuples_on X, X for s being State of 1GateCircuit(<*x,y*>,f) holds (Following s
).[<*x,y*>, f] = f.<*s.x, s.y*> & (Following s).x = s.x & (Following s).y = s.y
;
theorem :: FACIRC_1:49
for X being finite non empty set, f being Function of 2
-tuples_on X, X for s being State of 1GateCircuit(<*x,y*>,f) holds Following s
is stable;
theorem :: FACIRC_1:50
for s being State of 1GateCircuit(x,y,f) holds (Following s).[<*x,y*>,
f] = f.<*s.x, s.y*> & (Following s).x = s.x & (Following s).y = s.y;
theorem :: FACIRC_1:51
for s being State of 1GateCircuit(x,y,f) holds Following s is stable;
definition
let x,y,z be object;
let f be Function of 3-tuples_on BOOLEAN, BOOLEAN;
func 1GateCircuit(x,y,z,f) -> Boolean gate`2=den strict Circuit of
1GateCircStr(<*x,y,z*>, f) equals
:: FACIRC_1:def 11
1GateCircuit(<*x,y,z*>, f);
end;
theorem :: FACIRC_1:52
for X being finite non empty set, f being Function of 3
-tuples_on X, X for s being State of 1GateCircuit(<*x,y,z*>,f) holds (Following
s).[<*x,y,z*>, f] = f.<*s.x, s.y, s.z*> & (Following s).x = s.x & (Following s)
.y = s.y & (Following s).z = s.z;
theorem :: FACIRC_1:53
for X being finite non empty set, f being Function of 3
-tuples_on X, X for s being State of 1GateCircuit(<*x,y,z*>,f) holds Following
s is stable;
theorem :: FACIRC_1:54
for f being Function of 3-tuples_on BOOLEAN, BOOLEAN for s being State
of 1GateCircuit(x,y,z,f) holds (Following s).[<*x,y,z*>, f] = f.<*s.x, s.y, s.z
*> & (Following s).x = s.x & (Following s).y = s.y & (Following s).z = s.z;
theorem :: FACIRC_1:55
for f being Function of 3-tuples_on BOOLEAN, BOOLEAN for s being State
of 1GateCircuit(x,y,z,f) holds Following s is stable;
begin :: Two Gates Circuit
definition
let x,y,c be object;
let f be Function of 2-tuples_on BOOLEAN, BOOLEAN;
func 2GatesCircStr(x,y,c,f) -> unsplit gate`1=arity gate`2isBoolean non void
strict non empty ManySortedSign equals
:: FACIRC_1:def 12
1GateCircStr(<*x,y*>, f) +* 1GateCircStr
(<*[<*x,y*>, f], c*>, f);
end;
definition
let x,y,c be object;
let f be Function of 2-tuples_on BOOLEAN, BOOLEAN;
func 2GatesCircOutput(x,y,c,f) -> Element of InnerVertices 2GatesCircStr(x,y
,c,f) equals
:: FACIRC_1:def 13
[<*[<*x,y*>, f], c*>, f];
end;
registration
let x,y,c be object;
let f be Function of 2-tuples_on BOOLEAN, BOOLEAN;
cluster 2GatesCircOutput(x,y,c,f) -> pair;
end;
theorem :: FACIRC_1:56
InnerVertices 2GatesCircStr(x,y,c,f) = {[<*x,y*>, f],
2GatesCircOutput(x,y,c,f)};
theorem :: FACIRC_1:57
c <> [<*x,y*>, f] implies InputVertices 2GatesCircStr(x,y,c,f) = {x,y,c};
definition
let x,y,c be object;
let f be Function of 2-tuples_on BOOLEAN, BOOLEAN;
func 2GatesCircuit(x,y,c,f) -> strict Boolean gate`2=den Circuit of
2GatesCircStr(x,y,c,f) equals
:: FACIRC_1:def 14
1GateCircuit(x,y, f) +* 1GateCircuit([<*x,y*>, f], c, f);
end;
theorem :: FACIRC_1:58
InnerVertices 2GatesCircStr(x,y,c,f) is Relation;
theorem :: FACIRC_1:59
for x,y,c being non pair object
holds InputVertices 2GatesCircStr(x,y,c,f) is without_pairs;
theorem :: FACIRC_1:60
x in the carrier of 2GatesCircStr(x,y,c,f) & y in the carrier of
2GatesCircStr(x,y,c,f) & c in the carrier of 2GatesCircStr(x,y,c,f);
theorem :: FACIRC_1:61
[<*x,y*>,f] in the carrier of 2GatesCircStr(x,y,c,f) & [<*[<*x,y*>,f],
c*>, f] in the carrier of 2GatesCircStr(x,y,c,f);
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;
end;
reserve s for State of 2GatesCircuit(x,y,c,f);
theorem :: FACIRC_1:62
c <> [<*x,y*>, f] implies (Following(s,2)).2GatesCircOutput(x,y,
c,f) = f.<*f.<*s.x, s.y*>, s.c*> & (Following(s,2)).[<*x,y*>,f] = f.<*s.x, s.y
*> & (Following(s,2)).x = s.x & (Following(s,2)).y = s.y & (Following(s,2)).c =
s.c;
theorem :: FACIRC_1:63
c <> [<*x,y*>, f] implies Following(s,2) is stable;
theorem :: FACIRC_1:64
c <> [<*x,y*>, 'xor'] implies for s being State of 2GatesCircuit
(x,y,c,'xor') for a1,a2,a3 being Element of BOOLEAN st a1 = s.x & a2 = s.y & a3
= s.c holds (Following(s,2)).2GatesCircOutput(x,y,c,'xor') = a1 'xor' a2 'xor'
a3;
theorem :: FACIRC_1:65
c <> [<*x,y*>, 'or'] implies for s being State of 2GatesCircuit(x,y,c,
'or') for a1,a2,a3 being Element of BOOLEAN st a1 = s.x & a2 = s.y & a3 = s.c
holds (Following(s,2)).2GatesCircOutput(x,y,c,'or') = a1 'or' a2 'or' a3;
theorem :: FACIRC_1:66
c <> [<*x,y*>, '&'] implies for s being State of 2GatesCircuit(x,y,c,
'&') for a1,a2,a3 being Element of BOOLEAN st a1 = s.x & a2 = s.y & a3 = s.c
holds (Following(s,2)).2GatesCircOutput(x,y,c,'&') = a1 '&' a2 '&' a3;
begin :: Bit Adder Circuit
definition
let x,y,c be object;
func BitAdderOutput(x,y,c) -> Element of InnerVertices 2GatesCircStr(x,y,c,
'xor') equals
:: FACIRC_1:def 15
2GatesCircOutput(x,y,c, 'xor');
end;
definition
let x,y,c be object;
func BitAdderCirc(x,y,c) -> strict Boolean gate`2=den Circuit of
2GatesCircStr(x,y,c, 'xor') equals
:: FACIRC_1:def 16
2GatesCircuit(x,y,c, 'xor');
end;
definition
let x,y,c be object;
func MajorityIStr(x,y,c) -> unsplit gate`1=arity gate`2isBoolean non void
strict non empty ManySortedSign equals
:: FACIRC_1:def 17
1GateCircStr(<*x,y*>, '&') +*
1GateCircStr(<*y,c*>, '&') +* 1GateCircStr(<*c,x*>, '&');
end;
definition
let x,y,c be object;
func MajorityStr(x,y,c) -> unsplit gate`1=arity gate`2isBoolean non void
strict non empty ManySortedSign equals
:: FACIRC_1:def 18
MajorityIStr(x,y,c) +* 1GateCircStr(<*[
<*x,y*>, '&'], [<*y,c*>, '&'], [<*c,x*>, '&']*>, or3);
end;
definition
let x,y,c be object;
func MajorityICirc(x,y,c) -> strict Boolean gate`2=den Circuit of
MajorityIStr(x,y,c) equals
:: FACIRC_1:def 19
1GateCircuit(x,y, '&') +* 1GateCircuit(y,c, '&') +*
1GateCircuit(c,x, '&');
end;
theorem :: FACIRC_1:67
InnerVertices MajorityStr(x,y,c) is Relation;
theorem :: FACIRC_1:68
for x,y,c being non pair object holds InputVertices MajorityStr(x,y
,c) is without_pairs;
theorem :: FACIRC_1:69
for s being State of MajorityICirc(x,y,c), a,b being Element of
BOOLEAN st a = s.x & b = s.y holds (Following s).[<*x,y*>, '&'] = a '&' b;
theorem :: FACIRC_1:70
for s being State of MajorityICirc(x,y,c), a,b being Element of
BOOLEAN st a = s.y & b = s.c holds (Following s).[<*y,c*>, '&'] = a '&' b;
theorem :: FACIRC_1:71
for s being State of MajorityICirc(x,y,c), a,b being Element of
BOOLEAN st a = s.c & b = s.x holds (Following s).[<*c,x*>, '&'] = a '&' b;
definition
let x,y,c be object;
func MajorityOutput(x,y,c) -> Element of InnerVertices MajorityStr(x,y,c)
equals
:: FACIRC_1:def 20
[<*[<*x,y*>, '&'], [<*y,c*>, '&'], [<*c,x*>, '&']*>, or3];
end;
definition
let x,y,c be object;
func MajorityCirc(x,y,c) -> strict Boolean gate`2=den Circuit of MajorityStr
(x,y,c) equals
:: FACIRC_1:def 21
MajorityICirc(x,y,c) +* 1GateCircuit([<*x,y*>, '&'], [<*y,c*>,
'&'], [<*c,x*>, '&'], or3);
end;
theorem :: FACIRC_1:72
x in the carrier of MajorityStr(x,y,c) & y in the carrier of
MajorityStr(x,y,c) & c in the carrier of MajorityStr(x,y,c);
theorem :: FACIRC_1:73
[<*x,y*>,'&'] in InnerVertices MajorityStr(x,y,c) & [<*y,c*>,'&'
] in InnerVertices MajorityStr(x,y,c) & [<*c,x*>,'&'] in InnerVertices
MajorityStr(x,y,c);
theorem :: FACIRC_1:74
for x,y,c being non pair object holds x in InputVertices
MajorityStr(x,y,c) & y in InputVertices MajorityStr(x,y,c) & c in InputVertices
MajorityStr(x,y,c);
theorem :: FACIRC_1:75
for x,y,c being non pair object holds InputVertices MajorityStr(x,y
,c) = {x,y,c} & InnerVertices MajorityStr(x,y,c) = {[<*x,y*>,'&'], [<*y,c*>,'&'
], [<*c,x*>,'&']} \/ {MajorityOutput(x,y,c)};
theorem :: FACIRC_1:76
for x,y,c being non pair object for s being State of MajorityCirc(x,y,c)
for a1,a2 being Element of BOOLEAN st a1 = s.x & a2 = s.y holds (Following s).[
<*x,y*>,'&'] = a1 '&' a2;
theorem :: FACIRC_1:77
for x,y,c being non pair object for s being State of MajorityCirc(x,y,c)
for a2,a3 being Element of BOOLEAN st a2 = s.y & a3 = s.c holds (Following s).[
<*y,c*>,'&'] = a2 '&' a3;
theorem :: FACIRC_1:78
for x,y,c being non pair object for s being State of MajorityCirc(x,y,c)
for a1,a3 being Element of BOOLEAN st a1 = s.x & a3 = s.c holds (Following s).[
<*c,x*>,'&'] = a3 '&' a1;
theorem :: FACIRC_1:79
for x,y,c being non pair object for s being State of MajorityCirc(x
,y,c) for a1,a2,a3 being Element of BOOLEAN st a1 = s.[<*x,y*>,'&'] & a2 = s.[
<*y,c*>,'&'] & a3 = s.[<*c,x*>,'&'] holds (Following s).MajorityOutput(x,y,c) =
a1 'or' a2 'or' a3;
theorem :: FACIRC_1:80
for x,y,c being non pair object for s being State of MajorityCirc(x,y,c)
for a1,a2 being Element of BOOLEAN st a1 = s.x & a2 = s.y holds (Following(s,2)
).[<*x,y*>,'&'] = a1 '&' a2;
theorem :: FACIRC_1:81
for x,y,c being non pair object for s being State of MajorityCirc(x,y,c)
for a2,a3 being Element of BOOLEAN st a2 = s.y & a3 = s.c holds (Following(s,2)
).[<*y,c*>,'&'] = a2 '&' a3;
theorem :: FACIRC_1:82
for x,y,c being non pair object for s being State of MajorityCirc(x,y,c)
for a1,a3 being Element of BOOLEAN st a1 = s.x & a3 = s.c holds (Following(s,2)
).[<*c,x*>,'&'] = a3 '&' a1;
theorem :: FACIRC_1:83
for x,y,c being non pair object for s being State of MajorityCirc(x,y,c)
for a1,a2,a3 being Element of BOOLEAN st a1 = s.x & a2 = s.y & a3 = s.c holds (
Following(s,2)).MajorityOutput(x,y,c) = a1 '&' a2 'or' a2 '&' a3 'or' a3 '&' a1
;
theorem :: FACIRC_1:84
for x,y,c being non pair object for s being State of MajorityCirc(x
,y,c) holds Following(s,2) is stable;
definition
let x,y,c be object;
func BitAdderWithOverflowStr(x,y,c) -> unsplit gate`1=arity gate`2isBoolean
non void strict non empty ManySortedSign equals
:: FACIRC_1:def 22
2GatesCircStr(x,y,c, 'xor') +*
MajorityStr(x,y,c);
end;
theorem :: FACIRC_1:85
for x,y,c being non pair object holds InputVertices
BitAdderWithOverflowStr(x,y,c) = {x,y,c};
theorem :: FACIRC_1:86
for x,y,c being non pair object holds InnerVertices
BitAdderWithOverflowStr(x,y,c) = {[<*x,y*>, 'xor'], 2GatesCircOutput(x,y,c,
'xor')} \/ {[<*x,y*>,'&'], [<*y,c*>,'&'], [<*c,x*>,'&']} \/ {MajorityOutput(x,y
,c)};
theorem :: FACIRC_1:87
for S being non empty ManySortedSign st S = BitAdderWithOverflowStr(x,
y,c ) holds x in the carrier of S & y in the carrier of S & c in the carrier of
S;
definition
let x,y,c be object;
func BitAdderWithOverflowCirc(x,y,c) -> strict Boolean gate`2=den Circuit of
BitAdderWithOverflowStr(x,y,c) equals
:: FACIRC_1:def 23
BitAdderCirc(x,y,c) +* MajorityCirc(x,y,c
);
end;
theorem :: FACIRC_1:88
InnerVertices BitAdderWithOverflowStr(x,y,c) is Relation;
theorem :: FACIRC_1:89
for x,y,c being non pair object holds InputVertices
BitAdderWithOverflowStr(x,y,c) is without_pairs;
theorem :: FACIRC_1:90
BitAdderOutput(x,y,c) in InnerVertices BitAdderWithOverflowStr(x,y,c)
& MajorityOutput(x,y,c) in InnerVertices BitAdderWithOverflowStr(x,y,c)
;
theorem :: FACIRC_1:91
for x,y,c being non pair object for s being State of
BitAdderWithOverflowCirc(x,y,c) for a1,a2,a3 being Element of BOOLEAN st a1 = s
.x & a2 = s.y & a3 = s.c holds (Following(s,2)).BitAdderOutput(x,y,c) = a1
'xor' a2 'xor' a3 & (Following(s,2)).MajorityOutput(x,y,c) = a1 '&' a2 'or' a2
'&' a3 'or' a3 '&' a1;
theorem :: FACIRC_1:92
for x,y,c being non pair object for s being State of
BitAdderWithOverflowCirc(x,y,c) holds Following(s,2) is stable;