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