:: Combining of Circuits
:: by Yatsuka Nakamura and Grzegorz Bancerek
::
:: Received May 11, 1995
:: Copyright (c) 1995-2019 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;