:: Combining of Circuits :: by Yatsuka Nakamura and Grzegorz Bancerek :: :: Received May 11, 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 MSUALG_1, SUBSET_1, STRUCT_0, NUMBERS, XBOOLE_0, CARD_3, FINSEQ_1, FUNCOP_1, FINSEQ_2, PBOOLE, FUNCT_4, RELAT_1, PARTFUN1, FUNCT_1, TARSKI, MSAFREE2, FINSET_1, GLIB_000, MARGREL1, CIRCUIT1, FSM_1, CIRCUIT2, MCART_1, NAT_1, CARD_1, LATTICES, XBOOLEAN, CIRCCOMB; notations TARSKI, XBOOLE_0, XTUPLE_0, SUBSET_1, CARD_1, ORDINAL1, NUMBERS, MCART_1, RELAT_1, FUNCT_1, FINSEQ_1, FINSEQ_2, FINSET_1, FUNCT_2, FUNCOP_1, PARTFUN1, FUNCT_4, CARD_3, MARGREL1, PBOOLE, STRUCT_0, MSUALG_1, MSAFREE2, CIRCUIT1, CIRCUIT2; constructors MARGREL1, CIRCUIT1, CIRCUIT2, RELSET_1, XTUPLE_0, NUMBERS; registrations XBOOLE_0, RELAT_1, FUNCT_1, ORDINAL1, FUNCOP_1, FINSET_1, FINSEQ_1, MARGREL1, CARD_3, PBOOLE, STRUCT_0, MSUALG_1, MSUALG_2, MSAFREE2, FUNCT_4, RELSET_1, FINSEQ_2, XTUPLE_0; requirements NUMERALS, BOOLE, SUBSET; begin :: Combining of ManySortedSign's definition let S be ManySortedSign; mode Gate of S is Element of the carrier' of S; end; registration let A,B be set; let f be ManySortedSet of A; let g be ManySortedSet of B; cluster f+*g -> A \/ B-defined; end; registration let A,B be set; let f be ManySortedSet of A; let g be ManySortedSet of B; cluster f+*g -> total for A \/ B-defined Function; end; registration let A,B be set; cluster A .--> B -> {A}-defined; end; registration let A,B be set; cluster A .--> B -> total for {A}-defined Function; end; registration let A be set, B be non empty set; cluster A .--> B -> non-empty; end; theorem :: CIRCCOMB:1 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:2 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 carrier' of it = (the carrier' of S1) \/ (the carrier' 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:3 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:4 for S being non empty ManySortedSign holds S+*S = the ManySortedSign of S; theorem :: CIRCCOMB:5 for S1,S2 being non empty ManySortedSign st S1 tolerates S2 holds S1+*S2 = S2+*S1; theorem :: CIRCCOMB:6 for S1,S2,S3 being non empty ManySortedSign holds (S1+*S2)+*S3 = S1+*( S2+*S3 ); theorem :: CIRCCOMB:7 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:8 for S1,S2 being Circuit-like non empty ManySortedSign st InnerVertices S1 misses InnerVertices S2 holds S1+*S2 is Circuit-like; theorem :: CIRCCOMB:9 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:10 for S1,S2 being finite non empty ManySortedSign holds S1+*S2 is finite; registration 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:11 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:12 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:13 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:14 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:15 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:16 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:17 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:18 for S being non void non empty ManySortedSign, A being MSAlgebra over S holds A tolerates A; theorem :: CIRCCOMB:19 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:20 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:21 for S being strict non empty ManySortedSign, A being non-empty MSAlgebra over S holds A+*A = the MSAlgebra of A; theorem :: CIRCCOMB:22 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:23 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:24 for S1,S2 being non empty ManySortedSign for A1 being finite-yielding non-empty MSAlgebra over S1 for A2 being finite-yielding non-empty MSAlgebra over S2 st the Sorts of A1 tolerates the Sorts of A2 holds A1+*A2 is finite-yielding; theorem :: CIRCCOMB:25 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:26 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:27 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:28 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:29 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:30 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:31 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:32 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:33 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:34 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:35 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 f be object; let p be FinSequence; let x be object; func 1GateCircStr(p,f,x) -> non void strict ManySortedSign means :: CIRCCOMB:def 5 the carrier of it = (rng p) \/ {x} & the carrier' of it = {[p,f]} & (the Arity of it).[p,f] = p & (the ResultSort of it).[p,f] = x; end; registration let f be object; let p be FinSequence; let x be object; cluster 1GateCircStr(p,f,x) -> non empty; end; theorem :: CIRCCOMB:36 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:37 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:38 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 object; 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 carrier' of it = {[p,f]} & (the Arity of it).[p,f] = p & (the ResultSort of it).[p,f] = [p,f]; end; registration let f be object; let p be FinSequence; cluster 1GateCircStr(p,f) -> non empty; end; theorem :: CIRCCOMB:39 for f being set, p being FinSequence holds 1GateCircStr(p,f) = 1GateCircStr(p,f,[p,f]); theorem :: CIRCCOMB:40 for f being object, 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:41 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:42 for f being object, p being FinSequence holds InputVertices 1GateCircStr(p,f) = rng p & InnerVertices 1GateCircStr(p,f) = {[p,f]}; theorem :: CIRCCOMB:43 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 carrier' of IT; attr IT is gate`1=arity means :: CIRCCOMB:def 8 for g being set st g in the carrier' 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 carrier' 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 carrier' 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; scheme :: CIRCCOMB:sch 1 MSSLambdaWeak {A,B() -> set, g() -> Function of A(),B(), f(object,object) -> object}: ex f being ManySortedSet of A() st for a being set, b being Element of B() st a in A() & b = g().a holds f.a = f(a,b); scheme :: CIRCCOMB:sch 2 Lemma {S() -> non empty ManySortedSign, F(object,object) -> object}: ex A being strict MSAlgebra over S() st the Sorts of A = (the carrier of S()) --> BOOLEAN & for g being set, p being Element of (the carrier of S())* st g in the carrier' of S() & p = (the Arity of S()).g holds (the Charact of A).g = F(g,p) provided for g being set, p being Element of (the carrier of S())* st g in the carrier' of S() & p = (the Arity of S()).g holds F(g,p) is Function of (len p)-tuples_on BOOLEAN, BOOLEAN; registration cluster gate`2isBoolean -> gate`2=den for non empty ManySortedSign; end; theorem :: CIRCCOMB:44 for S being non empty ManySortedSign holds S is unsplit iff for o being object st o in the carrier' of S holds (the ResultSort of S).o = o; theorem :: CIRCCOMB:45 for S being non empty ManySortedSign st S is unsplit holds the carrier' of S c= the carrier of S; registration cluster unsplit -> Circuit-like for non empty ManySortedSign; end; theorem :: CIRCCOMB:46 for f being object, p being FinSequence holds 1GateCircStr(p,f) is unsplit gate`1=arity; registration let f be object, p be FinSequence; cluster 1GateCircStr(p,f) -> unsplit gate`1=arity; end; registration cluster unsplit gate`1=arity non void strict non empty for ManySortedSign; end; theorem :: CIRCCOMB:47 for S1,S2 being unsplit gate`1=arity non empty ManySortedSign holds S1 tolerates S2; theorem :: CIRCCOMB:48 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:49 for S1,S2 being unsplit non empty ManySortedSign holds S1+*S2 is unsplit; registration let S1,S2 be unsplit non empty ManySortedSign; cluster S1+*S2 -> unsplit; end; theorem :: CIRCCOMB:50 for S1,S2 being gate`1=arity non empty ManySortedSign holds S1+* S2 is gate`1=arity; registration let S1,S2 be gate`1=arity non empty ManySortedSign; cluster S1+*S2 -> gate`1=arity; end; theorem :: CIRCCOMB:51 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 is n-element FinSequence; 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 12 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 13 the Sorts of it = (the carrier of 1GateCircStr(p,f)) --> X & ( the Charact of it).[p,f] = f; end; theorem :: CIRCCOMB:52 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; registration 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:53 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; registration 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; registration cluster gate`2isBoolean non empty for ManySortedSign; end; registration let S1,S2 be gate`2isBoolean non empty ManySortedSign; cluster S1+*S2 -> gate`2isBoolean; end; theorem :: CIRCCOMB:54 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; registration 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) -> finite-yielding; end; theorem :: CIRCCOMB:55 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:56 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 -> Subset of NAT; :: coherence by MARGREL1:def 12,ZFMISC_1:38; :: end; definition let S be non empty ManySortedSign; let IT be MSAlgebra over S; attr IT is Boolean means :: CIRCCOMB:def 14 for v being Vertex of S holds (the Sorts of IT).v = BOOLEAN; end; theorem :: CIRCCOMB:57 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; registration let S be non empty ManySortedSign; cluster Boolean -> non-empty finite-yielding for MSAlgebra over S; end; theorem :: CIRCCOMB:58 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:59 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:60 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; registration let S be non empty ManySortedSign; cluster Boolean for strict MSAlgebra over S; end; theorem :: CIRCCOMB:61 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:62 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:63 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; registration cluster unsplit gate`1=arity gate`2=den gate`2isBoolean non void strict for non empty ManySortedSign; end; registration let S be gate`2isBoolean non empty ManySortedSign; cluster Boolean gate`2=den for strict MSAlgebra over S; end; registration 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; registration 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 for Circuit of 1GateCircStr(p,f); end; registration 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:64 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;