Volume 7, 1995

University of Bialystok

Copyright (c) 1995 Association of Mizar Users

### The abstract of the Mizar article:

### Full Adder Circuit. Part I

**by****Grzegorz Bancerek, and****Yatsuka Nakamura**- Received August 10, 1995
- MML identifier: FACIRC_1

- [ Mizar article, MML identifier index ]

environ vocabulary BOOLE, RELAT_1, FUNCT_1, FINSEQ_1, CIRCCOMB, FINSEQ_2, MSUALG_1, PARTFUN1, MSAFREE2, FUNCT_4, MARGREL1, MIDSP_3, BINARITH, ZF_LANG, AMI_1, ZF_REFLE, CIRCUIT1, QC_LANG1, CARD_3, LATTICES, MCART_1, FINSET_1, CIRCUIT2, CLASSES1, FACIRC_1; notation TARSKI, XBOOLE_0, ENUMSET1, SUBSET_1, NUMBERS, XREAL_0, NAT_1, MCART_1, RELAT_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, MIDSP_3; constructors MCART_1, BINARITH, CLASSES1, CIRCUIT1, CIRCUIT2, CIRCCOMB, ENUMSET1; clusters NUMBERS, SUBSET_1, STRUCT_0, RELAT_1, FUNCT_1, RELSET_1, FINSEQ_2, PRVECT_1, MSUALG_1, PRE_CIRC, CIRCCOMB, FINSEQ_1, XREAL_0, ARYTM_3, ORDINAL1, ZFMISC_1, ORDINAL2; requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM; begin :: Pairs, Set Without Pairs, and Nonpair-yielding Functions definition let IT be set; attr IT is pair means :: FACIRC_1:def 1 ex x,y being set st IT = [x,y]; end; definition cluster pair -> non empty set; end; definition let x,y be set; cluster [x,y] -> pair; end; definition cluster pair set; cluster non pair set; end; definition cluster -> non pair Nat; end; definition let IT be set; attr IT is with_pair means :: FACIRC_1:def 2 ex x being pair set st x in IT; antonym IT is without_pairs; end; definition cluster empty -> without_pairs set; let x be non pair set; cluster {x} -> without_pairs; let y be non pair set; cluster {x,y} -> without_pairs; let z be non pair set; cluster {x,y,z} -> without_pairs; end; definition cluster without_pairs (non empty set); end; definition let X, Y be without_pairs set; cluster X \/ Y -> without_pairs; end; definition 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; definition let x be pair set; cluster {x} -> Relation-like; let y be pair set; cluster {x,y} -> Relation-like; let z be pair set; cluster {x,y,z} -> Relation-like; end; definition cluster without_pairs Relation-like -> empty 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; definition let x be non pair set; cluster <*x*> -> nonpair-yielding; let y be non pair set; cluster <*x,y*> -> nonpair-yielding; let z be non pair set; 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; definition let n be Nat; cluster one-to-one nonpair-yielding FinSeqLen of n; end; definition cluster one-to-one nonpair-yielding FinSequence; end; definition 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 scheme 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 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 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 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 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 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; definition let x be set; redefine func <*x*> -> FinSeqLen of 1; let y be set; func <*x,y*> -> FinSeqLen of 2; let z be set; func <*x,y,z*> -> FinSeqLen of 3; end; definition let n,m be Nat; let p be FinSeqLen of n; let q be FinSeqLen of m; redefine func p^q -> FinSeqLen of n+m; end; begin 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 Nat; func Following(s,n) -> State of A means :: FACIRC_1:def 8 ex f being Function of NAT, 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 set; 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; definition let S be gate`2=den non void (non empty ManySortedSign); let g be Gate of S; cluster g`2 -> Function-like Relation-like; 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 OperSymbols 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 OperSymbols 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 OperSymbols 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 being set, x,y being set holds InputVertices 1GateCircStr(<*x,y*>,f) = {x,y}; theorem :: FACIRC_1:41 for f being set, x,y being non pair set holds InputVertices 1GateCircStr(<*x,y*>,f) is without_pairs; theorem :: FACIRC_1:42 for f being set, x,y,z being set holds InputVertices 1GateCircStr(<*x,y,z*>,f) = {x,y,z}; theorem :: FACIRC_1:43 for x,y,f being set 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 set 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 set; 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*>, f); end; reserve x,y,z,c for set, 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 set; 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 set; 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 set; 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; definition let x,y,c be set; 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 set; 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 set 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 set; 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 set; 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 set; 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 set; 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 set; 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 set 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 set; 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 set; 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 set 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 set 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 set 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 set 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 set 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 set 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 set 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 set 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 set 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 set 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 set for s being State of MajorityCirc(x,y,c) holds Following(s,2) is stable; definition let x,y,c be set; 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 set holds InputVertices BitAdderWithOverflowStr(x,y,c) = {x,y,c}; theorem :: FACIRC_1:86 for x,y,c being non pair set 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 set; 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 set 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 set 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 set for s being State of BitAdderWithOverflowCirc(x,y,c) holds Following(s,2) is stable;

Back to top