Volume 7, 1995

University of Bialystok

Copyright (c) 1995 Association of Mizar Users

### The abstract of the Mizar article:

### Combining of Circuits

**by****Yatsuka Nakamura, and****Grzegorz Bancerek**- Received May 11, 1995
- MML identifier: CIRCCOMB

- [ Mizar article, MML identifier index ]

environ vocabulary MSUALG_1, FUNCT_1, FUNCOP_1, PRALG_1, RELAT_1, CARD_3, FINSEQ_1, FINSEQ_2, AMI_1, ZF_REFLE, FUNCT_4, BOOLE, PBOOLE, PARTFUN1, TDGROUP, MSAFREE2, FINSET_1, QC_LANG1, PRE_CIRC, CIRCUIT1, CLASSES1, MCART_1, MARGREL1, LATTICES, CIRCCOMB; notation TARSKI, XBOOLE_0, SUBSET_1, NUMBERS, NAT_1, MCART_1, RELAT_1, FUNCT_1, STRUCT_0, FINSEQ_1, FINSEQ_2, FINSET_1, FUNCT_2, FUNCOP_1, PARTFUN1, FUNCT_4, GROUP_1, CARD_3, CLASSES1, MARGREL1, PBOOLE, PRALG_1, MSUALG_1, PRE_CIRC, MSAFREE2, CIRCUIT1, CIRCUIT2; constructors MCART_1, CLASSES1, MARGREL1, PRALG_1, CIRCUIT1, CIRCUIT2; clusters RELSET_1, FUNCT_1, FINSET_1, PRVECT_1, PBOOLE, MSUALG_1, MSAFREE2, STRUCT_0, MSUALG_2, FINSEQ_2, CANTOR_1, MARGREL1, FUNCOP_1, ARYTM_3, ORDINAL1, XBOOLE_0, FRAENKEL, MEMBERED, ORDINAL2; requirements NUMERALS, BOOLE, SUBSET; begin :: Combining of ManySortedSign's definition let S be ManySortedSign; mode Gate of S is Element of the OperSymbols of S; end; definition let A be set; let f be Function; cluster A --> f -> Function-yielding; end; definition let f,g be non-empty Function; cluster f+*g -> non-empty; end; definition let A,B be set; let f be ManySortedSet of A; let g be ManySortedSet of B; redefine func f+*g -> ManySortedSet of A \/ B; end; theorem :: CIRCCOMB:1 for f1,f2, g1,g2 being Function st rng g1 c= dom f1 & rng g2 c= dom f2 & f1 tolerates f2 holds (f1+*f2)*(g1+*g2) = (f1*g1)+*(f2*g2); theorem :: CIRCCOMB:2 for f1,f2, g being Function st rng g c= dom f1 & rng g c= dom f2 & f1 tolerates f2 holds f1*g = f2*g; theorem :: CIRCCOMB:3 for A,B being set, f being ManySortedSet of A for g being ManySortedSet of B st f c= g holds f# c= g#; theorem :: CIRCCOMB:4 for X,Y,x,y being set holds X --> x tolerates Y --> y iff x = y or X misses Y; theorem :: CIRCCOMB:5 for f,g,h being Function st f tolerates g & g tolerates h & h tolerates f holds f+*g tolerates h; theorem :: CIRCCOMB:6 for X being set, Y being non empty set, p being FinSequence of X holds (X --> Y)#.p = (len p)-tuples_on Y; definition let A be set; let f1,g1 be non-empty ManySortedSet of A; let B be set; let f2,g2 be non-empty ManySortedSet of B; let h1 be ManySortedFunction of f1,g1; let h2 be ManySortedFunction of f2,g2; redefine func h1+*h2 -> ManySortedFunction of f1+*f2, g1+*g2; end; definition let S1,S2 be ManySortedSign; pred S1 tolerates S2 means :: CIRCCOMB:def 1 the Arity of S1 tolerates the Arity of S2 & the ResultSort of S1 tolerates the ResultSort of S2; reflexivity; symmetry; end; definition let S1,S2 be non empty ManySortedSign; func S1 +* S2 -> strict non empty ManySortedSign means :: CIRCCOMB:def 2 the carrier of it = (the carrier of S1) \/ (the carrier of S2) & the OperSymbols of it = (the OperSymbols of S1) \/ (the OperSymbols of S2) & the Arity of it = (the Arity of S1) +* (the Arity of S2) & the ResultSort of it = (the ResultSort of S1) +* (the ResultSort of S2); end; theorem :: CIRCCOMB:7 for S1,S2,S3 being non empty ManySortedSign st S1 tolerates S2 & S2 tolerates S3 & S3 tolerates S1 holds S1+*S2 tolerates S3; theorem :: CIRCCOMB:8 for S being non empty ManySortedSign holds S+*S = the ManySortedSign of S; theorem :: CIRCCOMB:9 for S1,S2 being non empty ManySortedSign st S1 tolerates S2 holds S1+*S2 = S2+*S1; theorem :: CIRCCOMB:10 for S1,S2,S3 being non empty ManySortedSign holds (S1+*S2)+*S3 = S1+*(S2+*S3); definition cluster one-to-one Function; end; theorem :: CIRCCOMB:11 for f being one-to-one Function for S1,S2 being Circuit-like (non empty ManySortedSign) st the ResultSort of S1 c= f & the ResultSort of S2 c= f holds S1+*S2 is Circuit-like; theorem :: CIRCCOMB:12 for S1,S2 being Circuit-like (non empty ManySortedSign) st InnerVertices S1 misses InnerVertices S2 holds S1+*S2 is Circuit-like; theorem :: CIRCCOMB:13 for S1,S2 being non empty ManySortedSign st S1 is not void or S2 is not void holds S1+*S2 is non void; theorem :: CIRCCOMB:14 for S1,S2 being finite non empty ManySortedSign holds S1+*S2 is finite; definition let S1 be non void non empty ManySortedSign; let S2 be non empty ManySortedSign; cluster S1 +* S2 -> non void; cluster S2 +* S1 -> non void; end; ::theorem :: for S1,S2 being monotonic (non void ManySortedSign) st :: InputVertices S1 misses InnerVertices S2 or :: InputVertices S2 misses InnerVertices S1 :: holds S1+*S2 is monotonic; theorem :: CIRCCOMB:15 for S1,S2 being non empty ManySortedSign st S1 tolerates S2 holds InnerVertices (S1+*S2) = (InnerVertices S1) \/ (InnerVertices S2) & InputVertices (S1+*S2) c= (InputVertices S1) \/ (InputVertices S2); theorem :: CIRCCOMB:16 for S1,S2 being non empty ManySortedSign for v2 being Vertex of S2 st v2 in InputVertices (S1+*S2) holds v2 in InputVertices S2; theorem :: CIRCCOMB:17 for S1,S2 being non empty ManySortedSign st S1 tolerates S2 for v1 being Vertex of S1 st v1 in InputVertices (S1+*S2) holds v1 in InputVertices S1; theorem :: CIRCCOMB:18 for S1 being non empty ManySortedSign, S2 being non void non empty ManySortedSign for o2 being OperSymbol of S2, o being OperSymbol of S1+*S2 st o2 = o holds the_arity_of o = the_arity_of o2 & the_result_sort_of o = the_result_sort_of o2; theorem :: CIRCCOMB:19 for S1 being non empty ManySortedSign, S2,S being Circuit-like non void (non empty ManySortedSign) st S = S1+*S2 for v2 being Vertex of S2 st v2 in InnerVertices S2 for v being Vertex of S st v2 = v holds v in InnerVertices S & action_at v = action_at v2; theorem :: CIRCCOMB:20 for S1 being non void non empty ManySortedSign, S2 being non empty ManySortedSign st S1 tolerates S2 for o1 being OperSymbol of S1, o being OperSymbol of S1+*S2 st o1 = o holds the_arity_of o = the_arity_of o1 & the_result_sort_of o = the_result_sort_of o1; theorem :: CIRCCOMB:21 for S1,S being Circuit-like non void (non empty ManySortedSign), S2 being non empty ManySortedSign st S1 tolerates S2 & S = S1+*S2 for v1 being Vertex of S1 st v1 in InnerVertices S1 for v being Vertex of S st v1 = v holds v in InnerVertices S & action_at v = action_at v1; begin :: Combining of Circuits definition let S1,S2 be non empty ManySortedSign; let A1 be MSAlgebra over S1; let A2 be MSAlgebra over S2; pred A1 tolerates A2 means :: CIRCCOMB:def 3 S1 tolerates S2 & the Sorts of A1 tolerates the Sorts of A2 & the Charact of A1 tolerates the Charact of A2; end; definition let S1,S2 be non empty ManySortedSign; let A1 be non-empty MSAlgebra over S1; let A2 be non-empty MSAlgebra over S2; assume the Sorts of A1 tolerates the Sorts of A2; func A1 +* A2 -> strict non-empty MSAlgebra over S1+*S2 means :: CIRCCOMB:def 4 the Sorts of it = (the Sorts of A1) +* (the Sorts of A2) & the Charact of it = (the Charact of A1) +* (the Charact of A2); end; theorem :: CIRCCOMB:22 for S being non void non empty ManySortedSign, A being MSAlgebra over S holds A tolerates A; theorem :: CIRCCOMB:23 for S1,S2 be non void non empty ManySortedSign for A1 be MSAlgebra over S1, A2 be MSAlgebra over S2 st A1 tolerates A2 holds A2 tolerates A1; theorem :: CIRCCOMB:24 for S1,S2,S3 being non empty ManySortedSign, A1 being non-empty MSAlgebra over S1, A2 being non-empty MSAlgebra over S2, A3 being MSAlgebra over S3 st A1 tolerates A2 & A2 tolerates A3 & A3 tolerates A1 holds A1+*A2 tolerates A3 ; theorem :: CIRCCOMB:25 for S being strict non empty ManySortedSign, A being non-empty MSAlgebra over S holds A+*A = the MSAlgebra of A; theorem :: CIRCCOMB:26 for S1,S2 being non empty ManySortedSign, A1 being non-empty MSAlgebra over S1, A2 being non-empty MSAlgebra over S2 st A1 tolerates A2 holds A1+*A2 = A2+*A1; theorem :: CIRCCOMB:27 for S1,S2,S3 being non empty ManySortedSign, A1 being non-empty MSAlgebra over S1, A2 being non-empty MSAlgebra over S2, A3 being non-empty MSAlgebra over S3 st the Sorts of A1 tolerates the Sorts of A2 & the Sorts of A2 tolerates the Sorts of A3 & the Sorts of A3 tolerates the Sorts of A1 holds (A1+*A2)+*A3 = A1+*(A2+*A3); theorem :: CIRCCOMB:28 for S1,S2 being non empty ManySortedSign for A1 being locally-finite non-empty MSAlgebra over S1 for A2 being locally-finite non-empty MSAlgebra over S2 st the Sorts of A1 tolerates the Sorts of A2 holds A1+*A2 is locally-finite; theorem :: CIRCCOMB:29 for f,g being non-empty Function, x being Element of product f, y being Element of product g holds x+*y in product (f+*g); theorem :: CIRCCOMB:30 for f,g being non-empty Function for x being Element of product (f+*g) holds x|dom g in product g; theorem :: CIRCCOMB:31 for f,g being non-empty Function st f tolerates g for x being Element of product (f+*g) holds x|dom f in product f; theorem :: CIRCCOMB:32 for S1,S2 being non empty ManySortedSign for A1 being non-empty MSAlgebra over S1, s1 being Element of product the Sorts of A1 for A2 being non-empty MSAlgebra over S2, s2 being Element of product the Sorts of A2 st the Sorts of A1 tolerates the Sorts of A2 holds s1+*s2 in product the Sorts of A1+*A2; theorem :: CIRCCOMB:33 for S1,S2 being non empty ManySortedSign for A1 being non-empty MSAlgebra over S1, A2 being non-empty MSAlgebra over S2 st the Sorts of A1 tolerates the Sorts of A2 for s being Element of product the Sorts of A1+*A2 holds s|the carrier of S1 in product the Sorts of A1 & s|the carrier of S2 in product the Sorts of A2; theorem :: CIRCCOMB:34 for S1,S2 being non void non empty ManySortedSign for A1 being non-empty MSAlgebra over S1, A2 being non-empty MSAlgebra over S2 st the Sorts of A1 tolerates the Sorts of A2 for o being OperSymbol of S1+*S2, o2 being OperSymbol of S2 st o = o2 holds Den(o, A1+*A2) = Den(o2, A2); theorem :: CIRCCOMB:35 for S1,S2 being non void non empty ManySortedSign for A1 being non-empty MSAlgebra over S1, A2 being non-empty MSAlgebra over S2 st the Sorts of A1 tolerates the Sorts of A2 & the Charact of A1 tolerates the Charact of A2 for o being OperSymbol of S1+*S2, o1 being OperSymbol of S1 st o = o1 holds Den(o, A1+*A2) = Den(o1, A1); theorem :: CIRCCOMB:36 for S1,S2,S being non void Circuit-like (non empty ManySortedSign) st S = S1+*S2 for A1 being non-empty Circuit of S1, A2 being non-empty Circuit of S2, A being non-empty Circuit of S for s being State of A, s2 being State of A2 st s2 = s|the carrier of S2 for g being Gate of S, g2 being Gate of S2 st g = g2 holds g depends_on_in s = g2 depends_on_in s2; theorem :: CIRCCOMB:37 for S1,S2,S being non void Circuit-like (non empty ManySortedSign) st S = S1+*S2 & S1 tolerates S2 for A1 being non-empty Circuit of S1, A2 being non-empty Circuit of S2, A being non-empty Circuit of S for s being State of A, s1 being State of A1 st s1 = s|the carrier of S1 for g being Gate of S, g1 being Gate of S1 st g = g1 holds g depends_on_in s = g1 depends_on_in s1; theorem :: CIRCCOMB:38 for S1,S2,S being non void Circuit-like (non empty ManySortedSign) st S = S1+*S2 for A1 being non-empty Circuit of S1, A2 being non-empty Circuit of S2 for A being non-empty Circuit of S st A1 tolerates A2 & A = A1+*A2 for s being State of A, v being Vertex of S holds (for s1 being State of A1 st s1 = s|the carrier of S1 holds v in InnerVertices S1 or v in the carrier of S1 & v in InputVertices S implies (Following s).v = (Following s1).v) & (for s2 being State of A2 st s2 = s|the carrier of S2 holds v in InnerVertices S2 or v in the carrier of S2 & v in InputVertices S implies (Following s).v = (Following s2).v); theorem :: CIRCCOMB:39 for S1,S2,S being non void Circuit-like (non empty ManySortedSign) st InnerVertices S1 misses InputVertices S2 & S = S1+*S2 for A1 being non-empty Circuit of S1, A2 being non-empty Circuit of S2 for A being non-empty Circuit of S st A1 tolerates A2 & A = A1+*A2 for s being State of A, s1 being State of A1, s2 being State of A2 st s1 = s|the carrier of S1 & s2 = s|the carrier of S2 holds Following s = (Following s1)+*(Following s2); theorem :: CIRCCOMB:40 for S1,S2,S being non void Circuit-like (non empty ManySortedSign) st InnerVertices S2 misses InputVertices S1 & S = S1+*S2 for A1 being non-empty Circuit of S1, A2 being non-empty Circuit of S2 for A being non-empty Circuit of S st A1 tolerates A2 & A = A1+*A2 for s being State of A, s1 being State of A1, s2 being State of A2 st s1 = s|the carrier of S1 & s2 = s|the carrier of S2 holds Following s = (Following s2)+*(Following s1); theorem :: CIRCCOMB:41 for S1,S2,S being non void Circuit-like (non empty ManySortedSign) st InputVertices S1 c= InputVertices S2 & S = S1+*S2 for A1 being non-empty Circuit of S1, A2 being non-empty Circuit of S2 for A being non-empty Circuit of S st A1 tolerates A2 & A = A1+*A2 for s being State of A, s1 being State of A1, s2 being State of A2 st s1 = s|the carrier of S1 & s2 = s|the carrier of S2 holds Following s = (Following s2)+*(Following s1); theorem :: CIRCCOMB:42 for S1,S2,S being non void Circuit-like (non empty ManySortedSign) st InputVertices S2 c= InputVertices S1 & S = S1+*S2 for A1 being non-empty Circuit of S1, A2 being non-empty Circuit of S2 for A being non-empty Circuit of S st A1 tolerates A2 & A = A1+*A2 for s being State of A, s1 being State of A1, s2 being State of A2 st s1 = s|the carrier of S1 & s2 = s|the carrier of S2 holds Following s = (Following s1)+*(Following s2); begin :: ManySortedSign with One Operation definition let A,B be non empty set; let a be Element of A; redefine func B --> a -> Function of B,A; end; definition let f be set; let p be FinSequence; let x be set; func 1GateCircStr(p,f,x) -> non void strict ManySortedSign means :: CIRCCOMB:def 5 the carrier of it = (rng p) \/ {x} & the OperSymbols of it = {[p,f]} & (the Arity of it).[p,f] = p & (the ResultSort of it).[p,f] = x; end; definition let f be set; let p be FinSequence; let x be set; cluster 1GateCircStr(p,f,x) -> non empty; end; theorem :: CIRCCOMB:43 for f,x being set, p being FinSequence holds the Arity of 1GateCircStr(p,f,x) = {[p,f]} --> p & the ResultSort of 1GateCircStr(p,f,x) = {[p,f]} --> x; theorem :: CIRCCOMB:44 for f,x being set, p being FinSequence for g being Gate of 1GateCircStr(p,f,x) holds g = [p,f] & the_arity_of g = p & the_result_sort_of g = x; theorem :: CIRCCOMB:45 for f,x being set, p being FinSequence holds InputVertices 1GateCircStr(p,f,x) = (rng p) \ {x} & InnerVertices 1GateCircStr(p,f,x) = {x}; definition let f be set; let p be FinSequence; func 1GateCircStr(p,f) -> non void strict ManySortedSign means :: CIRCCOMB:def 6 the carrier of it = (rng p) \/ {[p,f]} & the OperSymbols of it = {[p,f]} & (the Arity of it).[p,f] = p & (the ResultSort of it).[p,f] = [p,f]; end; definition let f be set; let p be FinSequence; cluster 1GateCircStr(p,f) -> non empty; end; theorem :: CIRCCOMB:46 for f being set, p being FinSequence holds 1GateCircStr(p,f) = 1GateCircStr(p,f,[p,f]); theorem :: CIRCCOMB:47 for f being set, p being FinSequence holds the Arity of 1GateCircStr(p,f) = {[p,f]} --> p & the ResultSort of 1GateCircStr(p,f) = {[p,f]} --> [p,f]; theorem :: CIRCCOMB:48 for f being set, p being FinSequence for g being Gate of 1GateCircStr(p,f) holds g = [p,f] & the_arity_of g = p & the_result_sort_of g = g; theorem :: CIRCCOMB:49 for f being set, p being FinSequence holds InputVertices 1GateCircStr(p,f) = rng p & InnerVertices 1GateCircStr(p,f) = {[p,f]}; theorem :: CIRCCOMB:50 for f being set, p being FinSequence for x being set st x in rng p holds the_rank_of x in the_rank_of [p,f]; theorem :: CIRCCOMB:51 for f being set, p,q being FinSequence holds 1GateCircStr(p,f) tolerates 1GateCircStr(q,f); begin :: Unsplit condition definition let IT be ManySortedSign; attr IT is unsplit means :: CIRCCOMB:def 7 the ResultSort of IT = id the OperSymbols of IT; attr IT is gate`1=arity means :: CIRCCOMB:def 8 for g being set st g in the OperSymbols of IT holds g = [(the Arity of IT).g, g`2]; attr IT is gate`2isBoolean means :: CIRCCOMB:def 9 for g being set st g in the OperSymbols of IT for p being FinSequence st p = (the Arity of IT).g ex f being Function of (len p)-tuples_on BOOLEAN, BOOLEAN st g = [g`1, f]; end; definition let S be non empty ManySortedSign; let IT be MSAlgebra over S; attr IT is gate`2=den means :: CIRCCOMB:def 10 for g being set st g in the OperSymbols of S holds g = [g`1, (the Charact of IT).g]; end; definition let IT be non empty ManySortedSign; attr IT is gate`2=den means :: CIRCCOMB:def 11 ex A being MSAlgebra over IT st A is gate`2=den; end; definition cluster gate`2isBoolean -> gate`2=den (non empty ManySortedSign); end; theorem :: CIRCCOMB:52 for S being non empty ManySortedSign holds S is unsplit iff for o being set st o in the OperSymbols of S holds (the ResultSort of S).o = o; theorem :: CIRCCOMB:53 for S being non empty ManySortedSign st S is unsplit holds the OperSymbols of S c= the carrier of S; definition cluster unsplit -> Circuit-like (non empty ManySortedSign); end; theorem :: CIRCCOMB:54 for f being set, p being FinSequence holds 1GateCircStr(p,f) is unsplit gate`1=arity; definition let f be set, p be FinSequence; cluster 1GateCircStr(p,f) -> unsplit gate`1=arity; end; definition cluster unsplit gate`1=arity non void strict non empty ManySortedSign; end; theorem :: CIRCCOMB:55 for S1,S2 being unsplit gate`1=arity non empty ManySortedSign holds S1 tolerates S2; theorem :: CIRCCOMB:56 for S1,S2 being non empty ManySortedSign, A1 being MSAlgebra over S1 for A2 being MSAlgebra over S2 st A1 is gate`2=den & A2 is gate`2=den holds the Charact of A1 tolerates the Charact of A2; theorem :: CIRCCOMB:57 for S1,S2 being unsplit non empty ManySortedSign holds S1+*S2 is unsplit; definition let S1,S2 be unsplit non empty ManySortedSign; cluster S1+*S2 -> unsplit; end; theorem :: CIRCCOMB:58 for S1,S2 being gate`1=arity non empty ManySortedSign holds S1+*S2 is gate`1=arity; definition let S1,S2 be gate`1=arity non empty ManySortedSign; cluster S1+*S2 -> gate`1=arity; end; theorem :: CIRCCOMB:59 for S1,S2 being non empty ManySortedSign st S1 is gate`2isBoolean & S2 is gate`2isBoolean holds S1+*S2 is gate`2isBoolean; begin :: One Gate Circuit definition let n be Nat; mode FinSeqLen of n -> FinSequence means :: CIRCCOMB:def 12 len it = n; end; definition let n be Nat; let X,Y be non empty set; let f be Function of n-tuples_on X, Y; let p be FinSeqLen of n; let x be set such that x in rng p implies X = Y; func 1GateCircuit(p,f,x) -> strict non-empty MSAlgebra over 1GateCircStr(p,f,x) means :: CIRCCOMB:def 13 the Sorts of it = ((rng p) --> X) +* ({x} --> Y) & (the Charact of it).[p,f] = f; end; definition let n be Nat; let X be non empty set; let f be Function of n-tuples_on X, X; let p be FinSeqLen of n; func 1GateCircuit(p,f) -> strict non-empty MSAlgebra over 1GateCircStr(p,f) means :: CIRCCOMB:def 14 the Sorts of it = (the carrier of 1GateCircStr(p,f)) --> X & (the Charact of it).[p,f] = f; end; theorem :: CIRCCOMB:60 for n being Nat, X being non empty set for f being Function of n-tuples_on X, X for p being FinSeqLen of n holds 1GateCircuit(p,f) is gate`2=den & 1GateCircStr(p,f) is gate`2=den; definition let n be Nat, X be non empty set; let f be Function of n-tuples_on X, X; let p be FinSeqLen of n; cluster 1GateCircuit(p,f) -> gate`2=den; cluster 1GateCircStr(p,f) -> gate`2=den; end; theorem :: CIRCCOMB:61 for n being Nat for p being FinSeqLen of n for f being Function of n-tuples_on BOOLEAN, BOOLEAN holds 1GateCircStr(p,f) is gate`2isBoolean; definition let n be Nat; let f be Function of n-tuples_on BOOLEAN, BOOLEAN; let p be FinSeqLen of n; cluster 1GateCircStr(p,f) -> gate`2isBoolean; end; definition cluster gate`2isBoolean non empty ManySortedSign; end; definition let S1,S2 be gate`2isBoolean non empty ManySortedSign; cluster S1+*S2 -> gate`2isBoolean; end; theorem :: CIRCCOMB:62 for n being Nat, X being non empty set, f being Function of n-tuples_on X, X for p being FinSeqLen of n holds the Charact of 1GateCircuit(p,f) = {[p,f]} --> f & for v being Vertex of 1GateCircStr(p,f) holds (the Sorts of 1GateCircuit(p,f)).v = X; definition let n be Nat; let X be non empty finite set; let f be Function of n-tuples_on X, X; let p be FinSeqLen of n; cluster 1GateCircuit(p,f) -> locally-finite; end; theorem :: CIRCCOMB:63 for n being Nat, X being non empty set, f being Function of n-tuples_on X, X, p,q being FinSeqLen of n holds 1GateCircuit(p,f) tolerates 1GateCircuit(q,f); theorem :: CIRCCOMB:64 for n being Nat, X being finite non empty set, f being Function of n-tuples_on X, X, p being FinSeqLen of n for s being State of 1GateCircuit(p,f) holds (Following s).[p,f] = f.(s*p); begin :: Boolean Circuits definition redefine func BOOLEAN -> finite non empty Subset of NAT; end; definition let S be non empty ManySortedSign; let IT be MSAlgebra over S; attr IT is Boolean means :: CIRCCOMB:def 15 for v being Vertex of S holds (the Sorts of IT).v = BOOLEAN; end; theorem :: CIRCCOMB:65 for S being non empty ManySortedSign, A being MSAlgebra over S holds A is Boolean iff the Sorts of A = (the carrier of S) --> BOOLEAN; definition let S be non empty ManySortedSign; cluster Boolean -> non-empty locally-finite MSAlgebra over S; end; theorem :: CIRCCOMB:66 for S being non empty ManySortedSign, A being MSAlgebra over S holds A is Boolean iff rng the Sorts of A c= {BOOLEAN}; theorem :: CIRCCOMB:67 for S1,S2 being non empty ManySortedSign for A1 being MSAlgebra over S1, A2 being MSAlgebra over S2 st A1 is Boolean & A2 is Boolean holds the Sorts of A1 tolerates the Sorts of A2 ; theorem :: CIRCCOMB:68 for S1,S2 being unsplit gate`1=arity non empty ManySortedSign for A1 being MSAlgebra over S1, A2 being MSAlgebra over S2 st A1 is Boolean gate`2=den & A2 is Boolean gate`2=den holds A1 tolerates A2; definition let S be non empty ManySortedSign; cluster Boolean (strict MSAlgebra over S); end; theorem :: CIRCCOMB:69 for n being Nat, f being Function of n-tuples_on BOOLEAN, BOOLEAN for p being FinSeqLen of n holds 1GateCircuit(p,f) is Boolean; theorem :: CIRCCOMB:70 for S1,S2 being non empty ManySortedSign for A1 be Boolean MSAlgebra over S1 for A2 be Boolean MSAlgebra over S2 holds A1+*A2 is Boolean; theorem :: CIRCCOMB:71 for S1,S2 being non empty ManySortedSign for A1 be non-empty MSAlgebra over S1, A2 be non-empty MSAlgebra over S2 st A1 is gate`2=den & A2 is gate`2=den & the Sorts of A1 tolerates the Sorts of A2 holds A1+*A2 is gate`2=den; definition cluster unsplit gate`1=arity gate`2=den gate`2isBoolean non void strict (non empty ManySortedSign); end; definition let S be gate`2isBoolean non empty ManySortedSign; cluster Boolean gate`2=den (strict MSAlgebra over S); end; definition let S1,S2 be unsplit gate`2isBoolean non void non empty ManySortedSign; let A1 be Boolean gate`2=den Circuit of S1; let A2 be Boolean gate`2=den Circuit of S2; cluster A1+*A2 -> Boolean gate`2=den; end; definition let n be Nat; let X be finite non empty set; let f be Function of n-tuples_on X, X; let p be FinSeqLen of n; cluster gate`2=den strict non-empty Circuit of 1GateCircStr(p,f); end; definition let n be Nat; let X be finite non empty set; let f be Function of n-tuples_on X, X; let p be FinSeqLen of n; cluster 1GateCircuit(p,f) -> gate`2=den; end; theorem :: CIRCCOMB:72 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 for s being State of A1+*A2, v being Vertex of S1+*S2 holds (for s1 being State of A1 st s1 = s|the carrier of S1 holds v in InnerVertices S1 or v in the carrier of S1 & v in InputVertices(S1+*S2) implies (Following s).v = (Following s1).v) & (for s2 being State of A2 st s2 = s|the carrier of S2 holds v in InnerVertices S2 or v in the carrier of S2 & v in InputVertices(S1+*S2) implies (Following s).v = (Following s2).v);

Back to top