:: Preliminaries to Automatic Generation of Mizar Documentation for Circuits
:: by Grzegorz Bancerek and Adam Naumowicz
::
:: Received July 26, 2002
:: Copyright (c) 2002-2021 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, STRUCT_0, MSAFREE2, XBOOLE_0, MSUALG_1, RELAT_1,
CIRCUIT1, FSM_1, SUBSET_1, CIRCUIT2, FUNCT_1, ARYTM_3, CARD_1, XXREAL_0,
NAT_1, FUNCT_4, PARTFUN1, FINSET_1, CIRCCOMB, FINSEQ_2, TARSKI, PBOOLE,
GLIB_000, FINSEQ_1, NET_1, FACIRC_1, FUNCOP_1, CATALG_1, MCART_1,
ZFMISC_1, CLASSES1, REWRITE1, ORDINAL2, MARGREL1, VALUED_0, CIRCCMB3;
notations TARSKI, XBOOLE_0, XTUPLE_0, XFAMILY, SUBSET_1, ORDINAL1, NUMBERS,
ENUMSET1, ZFMISC_1, RELAT_1, FUNCT_1, PBOOLE, FINSET_1, ORDINAL2,
CLASSES1, FUNCT_2, XCMPLX_0, XXREAL_0, NAT_1, VALUED_0, PARTFUN1,
REWRITE1, FINSEQ_1, FINSEQ_2, FINSEQ_4, FINSEQOP, FUNCT_4, STRUCT_0,
MSUALG_1, FACIRC_1, MSAFREE2, CIRCUIT1, CIRCUIT2, CIRCCOMB, FUNCOP_1,
XXREAL_2, MCART_1;
constructors DOMAIN_1, ORDINAL2, CLASSES1, FINSEQOP, FINSEQ_4, LIMFUNC1,
REWRITE1, CIRCUIT1, CIRCUIT2, FACIRC_1, XXREAL_2, VALUED_0, RELSET_1,
XTUPLE_0, NUMBERS, XFAMILY;
registrations XBOOLE_0, RELAT_1, FUNCT_1, ORDINAL1, FUNCOP_1, FINSET_1,
XREAL_0, MEMBERED, FINSEQ_1, FINSEQ_2, CARD_3, SEQM_3, FINSEQ_4, PBOOLE,
STRUCT_0, MSUALG_1, CIRCCOMB, FACIRC_1, XXREAL_2, RELSET_1, XTUPLE_0,
NAT_1;
requirements BOOLE, SUBSET, NUMERALS, REAL;
begin :: Stabilizing circuits
theorem :: CIRCCMB3:1
for S being non void Circuit-like non empty ManySortedSign for
A being non-empty Circuit of S for s being State of A, x being set st x in
InputVertices S for n being Nat holds Following(s,n).x = s.x;
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;
attr s is stabilizing means
:: CIRCCMB3:def 1
ex n being Element of NAT st Following(s, n) is stable;
end;
definition
let S be non void Circuit-like non empty ManySortedSign;
let A be non-empty Circuit of S;
attr A is stabilizing means
:: CIRCCMB3:def 2
for s being State of A holds s is stabilizing;
attr A is with_stabilization-limit means
:: CIRCCMB3:def 3
ex n being Element of NAT st for s
being State of A holds Following(s,n) is stable;
end;
registration
let S be non void Circuit-like non empty ManySortedSign;
cluster with_stabilization-limit -> stabilizing for non-empty Circuit of S;
end;
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 such that
s is stabilizing;
func Result s -> State of A means
:: CIRCCMB3:def 4
it is stable & ex n being Element of NAT st it = Following(s,n);
end;
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 such that
s is stabilizing;
func stabilization-time s -> Element of NAT means
:: CIRCCMB3:def 5
Following(s,it) is
stable & for n being Element of NAT st n < it holds not Following(s,n) is
stable;
end;
theorem :: CIRCCMB3:2
for S being non void Circuit-like non empty ManySortedSign for
A being non-empty Circuit of S for s being State of A st s is stabilizing holds
Result s = Following(s,stabilization-time s);
theorem :: CIRCCMB3:3
for S being non void Circuit-like non empty ManySortedSign for A
being non-empty Circuit of S for s being State of A, n being Element of NAT st
Following(s,n) is stable holds stabilization-time s <= n;
theorem :: CIRCCMB3:4
for S being non void Circuit-like non empty ManySortedSign for
A being non-empty Circuit of S for s being State of A, n being Element of NAT
st Following(s,n) is stable holds Result s = Following(s, n);
theorem :: CIRCCMB3:5
for S being non void Circuit-like non empty ManySortedSign for
A being non-empty Circuit of S for s being State of A, n being Element of NAT
st s is stabilizing & n >= stabilization-time s holds Result s = Following(s, n
);
theorem :: CIRCCMB3:6
for S being non void Circuit-like non empty ManySortedSign for A
being non-empty Circuit of S for s being State of A st s is stabilizing for x
being set st x in InputVertices S holds (Result s).x = s.x;
theorem :: CIRCCMB3:7
for S1,S2 being non void Circuit-like non empty ManySortedSign
st InputVertices S1 misses InnerVertices S2 & InputVertices S2 misses
InnerVertices S1 for S being non void Circuit-like non empty ManySortedSign
st S=S1 +* S2 for A1 being non-empty Circuit of S1 for A2 being non-empty
Circuit of S2 st A1 tolerates A2 for A being non-empty Circuit of S st A = A1
+* A2 for s being State of A for s1 being State of A1 for s2 being State of A2
st s1=s|the carrier of S1 & s2=s|the carrier of S2 & s1 is stabilizing & s2 is
stabilizing holds s is stabilizing;
theorem :: CIRCCMB3:8
for S1,S2 being non void Circuit-like non empty ManySortedSign st
InputVertices S1 misses InnerVertices S2 & InputVertices S2 misses
InnerVertices S1 for S being non void Circuit-like non empty ManySortedSign
st S=S1 +* S2 for A1 being non-empty Circuit of S1 for A2 being non-empty
Circuit of S2 st A1 tolerates A2 for A being non-empty Circuit of S st A = A1
+* A2 for s being State of A for s1 being State of A1 st s1=s|the carrier of S1
& s1 is stabilizing for s2 being State of A2 st s2=s|the carrier of S2 & s2 is
stabilizing holds stabilization-time(s) = max (stabilization-time s1,
stabilization-time s2);
theorem :: CIRCCMB3:9
for S1,S2 being non void Circuit-like non empty ManySortedSign
st InputVertices S1 misses InnerVertices S2 for S being non void Circuit-like
non empty ManySortedSign st S=S1 +* S2 for A1 being non-empty Circuit of S1
for A2 being non-empty Circuit of S2 st A1 tolerates A2 for A being non-empty
Circuit of S st A = A1 +* A2 for s being State of A for s1 being State of A1 st
s1 = s|the carrier of S1 & s1 is stabilizing for s2 being State of A2 st s2 =
Following(s, stabilization-time s1)|the carrier of S2 & s2 is stabilizing holds
s is stabilizing;
theorem :: CIRCCMB3:10
for S1,S2 being non void Circuit-like non empty ManySortedSign
st InputVertices S1 misses InnerVertices S2 for S being non void Circuit-like
non empty ManySortedSign st S = S1+*S2 for A1 being non-empty Circuit of S1
for A2 being non-empty Circuit of S2 st A1 tolerates A2 for A being non-empty
Circuit of S st A = A1 +* A2 for s being State of A for s1 being State of A1 st
s1 = s|the carrier of S1 & s1 is stabilizing for s2 being State of A2 st s2 =
Following(s, stabilization-time s1)|the carrier of S2 & s2 is stabilizing holds
stabilization-time(s) = (stabilization-time s1)+(stabilization-time s2);
theorem :: CIRCCMB3:11
for S1,S2,S being non void Circuit-like non empty ManySortedSign st
InputVertices S1 misses InnerVertices 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 be State of A1
st s1 = s|the carrier of S1 & s1 is stabilizing for s2 being State of A2 st s2
= Following(s, stabilization-time s1)|the carrier of S2 & s2 is stabilizing
holds (Result s)|the carrier of S1 = Result s1;
begin :: One-gate circuits
theorem :: CIRCCMB3:12
for x being set, X being non empty finite set for n being
Element of NAT for p being FinSeqLen of n for g being Function of n-tuples_on X
, X for s being State of 1GateCircuit(p,g) holds s*p is Element of n-tuples_on
X;
theorem :: CIRCCMB3:13
for x1,x2,x3,x4 being object holds rng <*x1,x2,x3,x4*> = {x1,x2,x3,x4};
theorem :: CIRCCMB3:14
for x1,x2,x3,x4,x5 being object
holds rng <*x1,x2,x3,x4,x5*> = {x1, x2,x3,x4,x5};
definition
let S be ManySortedSign;
attr S is one-gate means
:: CIRCCMB3:def 6
ex X being non empty finite set, n being
Element of NAT, p being FinSeqLen of n, f being Function of n-tuples_on X,X st
S = 1GateCircStr(p,f);
end;
definition
let S be non empty ManySortedSign;
let A be MSAlgebra over S;
attr A is one-gate means
:: CIRCCMB3:def 7
ex X being non empty finite set, n being
Element of NAT, p being FinSeqLen of n, f being Function of n-tuples_on X,X st
S = 1GateCircStr(p,f) & A = 1GateCircuit(p,f);
end;
registration
let p being FinSequence, x be set;
cluster 1GateCircStr(p,x) -> finite;
end;
registration
cluster one-gate -> strict non void non empty unsplit gate`1=arity finite
for ManySortedSign;
end;
registration
cluster one-gate -> gate`2=den for non empty ManySortedSign;
end;
registration
let X be non empty finite set, n be Element of NAT, p be FinSeqLen of n, f
be Function of n-tuples_on X,X;
cluster 1GateCircStr(p,f) -> one-gate;
end;
registration
cluster one-gate for ManySortedSign;
end;
registration
let S be one-gate ManySortedSign;
cluster one-gate -> strict non-empty for Circuit of S;
end;
registration
let X be non empty finite set, n be Element of NAT, p be FinSeqLen of n, f
be Function of n-tuples_on X,X;
cluster 1GateCircuit(p,f) -> one-gate;
end;
registration
let S be one-gate ManySortedSign;
cluster one-gate non-empty for Circuit of S;
end;
definition
let S be one-gate ManySortedSign;
func Output S -> Vertex of S equals
:: CIRCCMB3:def 8
union the carrier' of S;
end;
registration
let S be one-gate ManySortedSign;
cluster Output S -> pair;
end;
theorem :: CIRCCMB3:15
for S being one-gate ManySortedSign, p being FinSequence, x
being set st S = 1GateCircStr(p,x) holds Output S = [p,x];
theorem :: CIRCCMB3:16
for S being one-gate ManySortedSign holds InnerVertices S = { Output S};
theorem :: CIRCCMB3:17
for S being one-gate ManySortedSign for A being one-gate Circuit of S
for n being Element of NAT for X being finite non empty set for f being
Function of n-tuples_on X, X, p being FinSeqLen of n st A = 1GateCircuit(p,f)
holds S = 1GateCircStr(p,f);
theorem :: CIRCCMB3:18
for n being Element of NAT for X being finite non empty set for 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).Output 1GateCircStr(p,f) = f.(s*p);
theorem :: CIRCCMB3:19
for S being one-gate ManySortedSign for A being one-gate Circuit
of S for s being State of A holds Following s is stable;
registration
let S be non void Circuit-like non empty ManySortedSign;
cluster one-gate -> with_stabilization-limit for non-empty Circuit of S;
end;
theorem :: CIRCCMB3:20
for S being one-gate ManySortedSign for A being one-gate Circuit
of S for s being State of A holds Result s = Following s;
theorem :: CIRCCMB3:21
for S being one-gate ManySortedSign for A being one-gate Circuit
of S for s being State of A holds stabilization-time s <= 1;
scheme :: CIRCCMB3:sch 1
OneGate1Ex {x()->object,X()->non empty finite set,f(object)->Element of X()}:
ex S being one-gate ManySortedSign, A being one-gate Circuit of S st
InputVertices S
= {x()} & for s being State of A holds (Result s).(Output S) = f(s.x());
scheme :: CIRCCMB3:sch 2
OneGate2Ex {x1,x2()->object,X()->non empty finite set,
f(object,object)->Element of X()}:
ex S being one-gate ManySortedSign, A being one-gate Circuit of S st
InputVertices S = {x1(),x2()} & for s being State of A holds (Result s).(Output
S) = f(s.x1(),s.x2());
scheme :: CIRCCMB3:sch 3
OneGate3Ex {x1,x2,x3()->object,X()->non empty finite set,
f(object,object,object)->
Element of X()}: ex S being one-gate ManySortedSign, A being one-gate Circuit
of S st InputVertices S = {x1(),x2(),x3()} & for s being State of A holds (
Result s).(Output S) = f(s.x1(),s.x2(),s.x3());
scheme :: CIRCCMB3:sch 4
OneGate4Ex {x1,x2,x3,x4()->object,X()->non empty finite set,
f(object,object,object,object)
->Element of X()}: ex S being one-gate ManySortedSign, A being one-gate Circuit
of S st InputVertices S = {x1(),x2(),x3(),x4()} & for s being State of A holds
(Result s).(Output S) = f(s.x1(),s.x2(),s.x3(),s.x4());
scheme :: CIRCCMB3:sch 5
OneGate5Ex {x1,x2,x3,x4,x5()->object,X()->non empty finite set,
f(object,object,object,object,object)->Element of X()}:
ex S being one-gate ManySortedSign, A being one-gate
Circuit of S st InputVertices S = {x1(),x2(),x3(),x4(),x5()} & for s being
State of A holds (Result s).(Output S) = f(s.x1(),s.x2(),s.x3(),s.x4(),s.x5());
begin :: Mono-sorted circuits
theorem :: CIRCCMB3:22
for X,Y being non empty set, n,m being Element of NAT st n<>0 &
n-tuples_on X = m-tuples_on Y holds X=Y & n=m;
theorem :: CIRCCMB3:23
for S1,S2 being non empty ManySortedSign for v being Vertex of S1
holds v is Vertex of S1+*S2;
theorem :: CIRCCMB3:24
for S1,S2 being non empty ManySortedSign for v being Vertex of S2
holds v is Vertex of S1+*S2;
definition
let X be non empty finite set;
mode Signature of X -> gate`2=den non void non empty unsplit gate`1=arity
ManySortedSign means
:: CIRCCMB3:def 9
ex A being Circuit of it st the Sorts of A is
constant & the_value_of the Sorts of A = X & A is gate`2=den;
end;
theorem :: CIRCCMB3:25
for n being Element of NAT, X being non empty finite set for f
being Function of n-tuples_on X, X for p being FinSeqLen of n holds
1GateCircStr(p,f) is Signature of X;
registration
let X be non empty finite set;
cluster strict one-gate for Signature of X;
end;
definition
let n be Element of NAT;
let X be non empty finite set;
let f be Function of n-tuples_on X, X;
let p be FinSeqLen of n;
redefine func 1GateCircStr(p,f) -> strict Signature of X;
end;
definition
let X be non empty finite set;
let S be Signature of X;
mode Circuit of X,S -> Circuit of S means
:: CIRCCMB3:def 10
it is gate`2=den & the
Sorts of it is constant & the_value_of the Sorts of it = X;
end;
registration
let X be non empty finite set;
let S be Signature of X;
cluster -> gate`2=den non-empty for Circuit of X,S;
end;
theorem :: CIRCCMB3:26
for n being Element of NAT, X being non empty finite set for f
being Function of n-tuples_on X, X for p being FinSeqLen of n holds
1GateCircuit(p,f) is Circuit of X, 1GateCircStr(p,f);
registration
let X be non empty finite set;
let S be one-gate Signature of X;
cluster strict one-gate for Circuit of X,S;
end;
registration
let X be non empty finite set;
let S be Signature of X;
cluster strict for Circuit of X,S;
end;
definition
let n be Element of NAT;
let X be non empty finite set;
let f be Function of n-tuples_on X, X;
let p be FinSeqLen of n;
redefine func 1GateCircuit(p,f) -> strict Circuit of X,1GateCircStr(p,f);
end;
theorem :: CIRCCMB3:27
for X being non empty finite set for S1, S2 being Signature of X
for A1 being Circuit of X,S1 for A2 being Circuit of X,S2 holds A1 tolerates A2
;
theorem :: CIRCCMB3:28
for X being non empty finite set for S1, S2 being Signature of X
for A1 being Circuit of X,S1 for A2 being Circuit of X,S2 holds A1+*A2 is
Circuit of S1+*S2;
theorem :: CIRCCMB3:29
for X being non empty finite set for S1, S2 being Signature of X
for A1 being Circuit of X,S1 for A2 being Circuit of X,S2 holds A1+*A2 is
gate`2=den;
theorem :: CIRCCMB3:30
for X being non empty finite set for S1, S2 being Signature of X
for A1 being Circuit of X,S1 for A2 being Circuit of X,S2 holds the Sorts of A1
+*A2 is constant & the_value_of the Sorts of A1+*A2 = X;
registration
let S1,S2 be finite non empty ManySortedSign;
cluster S1+*S2 -> finite;
end;
registration
let X be non empty finite set;
let S1,S2 be Signature of X;
cluster S1+*S2 -> gate`2=den;
end;
definition
let X be non empty finite set;
let S1,S2 be Signature of X;
redefine func S1+*S2 -> strict Signature of X;
end;
definition
let X be non empty finite set;
let S1,S2 be Signature of X;
let A1 be Circuit of X,S1;
let A2 be Circuit of X,S2;
redefine func A1+*A2 -> strict Circuit of X,S1+*S2;
end;
theorem :: CIRCCMB3:31
for x,y being object holds the_rank_of x in the_rank_of [x,y] &
the_rank_of y in the_rank_of [x,y];
theorem :: CIRCCMB3:32
for S being gate`2=den finite non void non empty unsplit
gate`1=arity ManySortedSign for A being non-empty Circuit of S st A is
gate`2=den holds A is with_stabilization-limit;
registration
let X be non empty finite set;
let S be finite Signature of X;
cluster -> with_stabilization-limit for Circuit of X,S;
end;
scheme :: CIRCCMB3:sch 6
1AryDef {X()-> non empty set,F(object) -> Element of X()}:
(ex f being Function
of 1-tuples_on X(), X() st for x being Element of X() holds f.<*x*> = F(x)) &
for f1,f2 being Function of 1-tuples_on X(), X() st (for x being Element of X()
holds f1.<*x*> = F(x)) & (for x being Element of X() holds f2.<*x*> = F(x))
holds f1 = f2;
scheme :: CIRCCMB3:sch 7
2AryDef {X()-> non empty set,F(object,object) -> Element of X()}:
(ex f being
Function of 2-tuples_on X(), X() st for x,y being Element of X() holds f.<*x,y
*> = F(x,y)) & for f1,f2 being Function of 2-tuples_on X(), X() st (for x,y
being Element of X() holds f1.<*x,y*> = F(x,y)) & (for x,y being Element of X()
holds f2.<*x,y*> = F(x,y)) holds f1 = f2;
scheme :: CIRCCMB3:sch 8
3AryDef {X()-> non empty set,F(object,object,object) -> Element of X()}:
(ex f being
Function of 3-tuples_on X(), X() st for x,y,z being Element of X() holds f.<*x,
y,z*> = F(x,y,z)) & for f1,f2 being Function of 3-tuples_on X(), X() st (for x,
y,z being Element of X() holds f1.<*x,y,z*> = F(x,y,z)) & (for x,y,z being
Element of X() holds f2.<*x,y,z*> = F(x,y,z)) holds f1 = f2;
theorem :: CIRCCMB3:33
for f being Function for x1,x2,x3,x4 being set st
x1 in dom f & x2 in dom f & x3 in dom f & x4 in dom f holds
f*<*x1,x2,x3,x4*> = <*f.x1,f.x2,f.x3,f.x4*>;
theorem :: CIRCCMB3:34
for f being Function for x1,x2,x3,x4,x5 being set st x1 in dom f
& x2 in dom f & x3 in dom f & x4 in dom f & x5 in dom f holds f*<*x1,x2,x3,x4,
x5*> = <*f.x1,f.x2,f.x3,f.x4,f.x5*>;
scheme :: CIRCCMB3:sch 9
OneGate1Result {x1()-> object, B()-> non empty finite set,
F(object)->Element of B
(), f() -> Function of 1-tuples_on B(), B()}: for s being State of 1GateCircuit
(<*x1()*>,f()) for a1 being Element of B() st a1 = s.x1() holds (Result s).
Output(1GateCircStr(<*x1()*>,f())) = F(a1)
provided
for g being Function of 1-tuples_on B(), B() holds g = f() iff for
a1 being Element of B() holds g.<*a1*> = F(a1);
scheme :: CIRCCMB3:sch 10
OneGate2Result {x1,x2()-> object, B()-> non empty finite set,
F(object,object)->
Element of B(), f() -> Function of 2-tuples_on B(), B()}: for s being State of
1GateCircuit(<*x1(),x2()*>,f()) for a1, a2 being Element of B() st a1 = s.x1()
& a2 = s.x2() holds (Result s).Output(1GateCircStr(<*x1(),x2()*>,f())) = F(a1,
a2)
provided
for g being Function of 2-tuples_on B(), B() holds g = f() iff for
a1,a2 being Element of B() holds g.<*a1,a2*> = F(a1,a2);
scheme :: CIRCCMB3:sch 11
OneGate3Result {x1,x2,x3()->object, B()-> non empty finite set,
F(object,object,object)
->Element of B(), f() -> Function of 3-tuples_on B(), B()}: for s being State
of 1GateCircuit(<*x1(),x2(),x3()*>,f()) for a1, a2, a3 being Element of B() st
a1 = s.x1() & a2 = s.x2() & a3 = s.x3() holds (Result s).Output(1GateCircStr(<*
x1(),x2(),x3()*>,f())) = F(a1,a2,a3)
provided
for g being Function of 3-tuples_on B(), B() holds g = f() iff for
a1,a2,a3 being Element of B() holds g.<*a1,a2,a3*> = F(a1,a2,a3);
scheme :: CIRCCMB3:sch 12
OneGate4Result {x1,x2,x3,x4()-> object, B()-> non empty finite set,
F(object,object,object,object)->Element of B(),
f() -> Function of 4-tuples_on B(), B()}: for s being
State of 1GateCircuit(<*x1(),x2(),x3(),x4()*>,f()) for a1, a2, a3, a4 being
Element of B() st a1 = s.x1() & a2 = s.x2() & a3 = s.x3() & a4 = s.x4() holds (
Result s).Output(1GateCircStr(<*x1(),x2(),x3(),x4()*>,f())) = F(a1,a2,a3,a4)
provided
for g being Function of 4-tuples_on B(), B() holds g = f() iff for
a1,a2,a3,a4 being Element of B() holds g.<*a1,a2,a3,a4*> = F(a1,a2,a3,a4);
scheme :: CIRCCMB3:sch 13
OneGate5Result {x1,x2,x3,x4,x5()-> object, B()-> non empty finite set,
F(object,object,object,object,object)->Element of B(),
f() -> Function of 5-tuples_on B(), B()}: for
s being State of 1GateCircuit(<*x1(),x2(),x3(),x4(),x5()*>,f()) for a1, a2, a3,
a4, a5 being Element of B() st a1 = s.x1() & a2 = s.x2() & a3 = s.x3() & a4 = s
.x4() & a5 = s.x5() holds (Result s).Output(1GateCircStr(<*x1(),x2(),x3(),x4(),
x5()*>,f())) = F(a1,a2,a3,a4,a5)
provided
for g being Function of 5-tuples_on B(), B() holds g = f() iff for
a1,a2,a3,a4,a5 being Element of B() holds g.<*a1,a2,a3,a4,a5*> = F(a1,a2,a3,a4,
a5);
begin :: Input of a compound circuit
theorem :: CIRCCMB3:35
for n being Element of NAT, X being non empty finite set for f
being Function of n-tuples_on X, X for p being FinSeqLen of n for S being
Signature of X st rng p c= the carrier of S & not Output 1GateCircStr(p,f) in
InputVertices S holds InputVertices (S +* 1GateCircStr(p,f)) = InputVertices S;
theorem :: CIRCCMB3:36
for X1,X2 being set, X being non empty finite set, n be Element
of NAT for f being Function of n-tuples_on X, X for p being FinSeqLen of n for
S being Signature of X st rng p = X1 \/ X2 & X1 c= the carrier of S & X2 misses
InnerVertices S & not Output 1GateCircStr(p,f) in InputVertices S holds
InputVertices (S +* 1GateCircStr(p,f)) = (InputVertices S) \/ X2;
theorem :: CIRCCMB3:37
for x1 being set, X being non empty finite set for f being
Function of 1-tuples_on X, X for S being Signature of X st x1 in the carrier of
S & not Output 1GateCircStr(<*x1*>,f) in InputVertices S holds InputVertices (S
+* 1GateCircStr(<*x1*>,f)) = InputVertices S;
theorem :: CIRCCMB3:38
for x1,x2 being set, X being non empty finite set for f being
Function of 2-tuples_on X, X for S being Signature of X st x1 in the carrier of
S & not x2 in InnerVertices S & not Output 1GateCircStr(<*x1,x2*>,f) in
InputVertices S holds InputVertices (S +* 1GateCircStr(<*x1,x2*>,f)) = (
InputVertices S) \/ {x2};
theorem :: CIRCCMB3:39
for x1,x2 being set, X being non empty finite set for f being
Function of 2-tuples_on X, X for S being Signature of X st x2 in the carrier of
S & not x1 in InnerVertices S & not Output 1GateCircStr(<*x1,x2*>,f) in
InputVertices S holds InputVertices (S +* 1GateCircStr(<*x1,x2*>,f)) = (
InputVertices S) \/ {x1};
theorem :: CIRCCMB3:40
for x1,x2 being set, X being non empty finite set for f being
Function of 2-tuples_on X, X for S being Signature of X st x1 in the carrier of
S & x2 in the carrier of S & not Output 1GateCircStr(<*x1,x2*>,f) in
InputVertices S holds InputVertices (S +* 1GateCircStr(<*x1,x2*>,f)) =
InputVertices S;
theorem :: CIRCCMB3:41
for x1,x2,x3 being set, X being non empty finite set for f being
Function of 3-tuples_on X, X for S being Signature of X st x1 in the carrier of
S & not x2 in InnerVertices S & not x3 in InnerVertices S & not Output
1GateCircStr(<*x1,x2,x3*>,f) in InputVertices S holds InputVertices (S +*
1GateCircStr(<*x1,x2,x3*>,f)) = (InputVertices S) \/ {x2,x3};
theorem :: CIRCCMB3:42
for x1,x2,x3 being set, X being non empty finite set for f being
Function of 3-tuples_on X, X for S being Signature of X st x2 in the carrier of
S & not x1 in InnerVertices S & not x3 in InnerVertices S & not Output
1GateCircStr(<*x1,x2,x3*>,f) in InputVertices S holds InputVertices (S +*
1GateCircStr(<*x1,x2,x3*>,f)) = (InputVertices S) \/ {x1,x3};
theorem :: CIRCCMB3:43
for x1,x2,x3 being set, X being non empty finite set for f being
Function of 3-tuples_on X, X for S being Signature of X st x3 in the carrier of
S & not x1 in InnerVertices S & not x2 in InnerVertices S & not Output
1GateCircStr(<*x1,x2,x3*>,f) in InputVertices S holds InputVertices (S +*
1GateCircStr(<*x1,x2,x3*>,f)) = (InputVertices S) \/ {x1,x2};
theorem :: CIRCCMB3:44
for x1,x2,x3 being set, X being non empty finite set for f being
Function of 3-tuples_on X, X for S being Signature of X st x1 in the carrier of
S & x2 in the carrier of S & not x3 in InnerVertices S & not Output
1GateCircStr(<*x1,x2,x3*>,f) in InputVertices S holds InputVertices (S +*
1GateCircStr(<*x1,x2,x3*>,f)) = (InputVertices S) \/ {x3};
theorem :: CIRCCMB3:45
for x1,x2,x3 being set, X being non empty finite set for f being
Function of 3-tuples_on X, X for S being Signature of X st x1 in the carrier of
S & x3 in the carrier of S & not x2 in InnerVertices S & not Output
1GateCircStr(<*x1,x2,x3*>,f) in InputVertices S holds InputVertices (S +*
1GateCircStr(<*x1,x2,x3*>,f)) = (InputVertices S) \/ {x2};
theorem :: CIRCCMB3:46
for x1,x2,x3 being set, X being non empty finite set for f being
Function of 3-tuples_on X, X for S being Signature of X st x2 in the carrier of
S & x3 in the carrier of S & not x1 in InnerVertices S & not Output
1GateCircStr(<*x1,x2,x3*>,f) in InputVertices S holds InputVertices (S +*
1GateCircStr(<*x1,x2,x3*>,f)) = (InputVertices S) \/ {x1};
theorem :: CIRCCMB3:47
for x1,x2,x3 being set, X being non empty finite set for f being
Function of 3-tuples_on X, X for S being Signature of X st x1 in the carrier of
S & x2 in the carrier of S & x3 in the carrier of S & not Output 1GateCircStr(
<*x1,x2,x3*>,f) in InputVertices S holds InputVertices (S +* 1GateCircStr(<*x1,
x2,x3*>,f)) = InputVertices S;
begin :: Result of a compound circuit
theorem :: CIRCCMB3:48
for X being non empty finite set for S being finite Signature of
X for A being Circuit of X,S for n being Element of NAT, f being Function of n
-tuples_on X, X for p being FinSeqLen of n st not Output 1GateCircStr(p,f) in
InputVertices S for s being State of A +* 1GateCircuit(p,f) for s9 being State
of A st s9 = s|the carrier of S holds stabilization-time s <= 1+
stabilization-time s9;
scheme :: CIRCCMB3:sch 14
Comb1CircResult {x1()-> object, B()-> non empty finite set,
F(object)->Element of B(),
S() -> finite Signature of B(), C() -> Circuit of B(), S(), f() ->
Function of 1-tuples_on B(), B()}: for s being State of C() +* 1GateCircuit(<*
x1()*>,f()) for s9 being State of C() st s9 = s|the carrier of S() for a1 being
Element of B() st (x1() in InnerVertices S() implies a1 = (Result s9).x1()) & (
not x1() in InnerVertices S() implies a1 = s.x1()) holds (Result s).Output
1GateCircStr(<*x1()*>,f()) = F(a1)
provided
for g being Function of 1-tuples_on B(), B() holds g = f() iff for
a1 being Element of B() holds g.<*a1*> = F(a1) and
not Output 1GateCircStr(<*x1()*>,f()) in InputVertices S();
scheme :: CIRCCMB3:sch 15
Comb2CircResult {x1,x2()-> object, B()-> non empty finite set,
F(object,object)->
Element of B(), S() -> finite Signature of B(), C() -> Circuit of B(), S(), f()
-> Function of 2-tuples_on B(), B()}: for s being State of C() +* 1GateCircuit(
<*x1(),x2()*>,f()) for s9 being State of C() st s9 = s|the carrier of S() for
a1, a2 being Element of B() st (x1() in InnerVertices S() implies a1 = (Result
s9).x1()) & (not x1() in InnerVertices S() implies a1 = s.x1()) & (x2() in
InnerVertices S() implies a2 = (Result s9).x2()) & (not x2() in InnerVertices S
() implies a2 = s.x2()) holds (Result s).Output(1GateCircStr(<*x1(),x2()*>,f())
) = F(a1,a2)
provided
for g being Function of 2-tuples_on B(), B() holds g = f() iff for
a1,a2 being Element of B() holds g.<*a1,a2*> = F(a1,a2) and
not Output 1GateCircStr(<*x1(),x2()*>,f()) in InputVertices S();
scheme :: CIRCCMB3:sch 16
Comb3CircResult {x1,x2,x3()-> object, B()-> non empty finite set,
F(object,object,object)->Element of B(),
S() -> finite Signature of B(), C() -> Circuit of B(), S(),
f() -> Function of 3-tuples_on B(), B()}: for s being State of C() +*
1GateCircuit(<*x1(),x2(),x3()*>,f()) for s9 being State of C() st s9 = s|the
carrier of S() for a1, a2, a3 being Element of B() st (x1() in InnerVertices S(
) implies a1 = (Result s9).x1()) & (not x1() in InnerVertices S() implies a1 =
s.x1()) & (x2() in InnerVertices S() implies a2 = (Result s9).x2()) & (not x2()
in InnerVertices S() implies a2 = s.x2()) & (x3() in InnerVertices S() implies
a3 = (Result s9).x3()) & (not x3() in InnerVertices S() implies a3 = s.x3())
holds (Result s).Output(1GateCircStr(<*x1(),x2(),x3()*>,f())) = F(a1,a2,a3)
provided
for g being Function of 3-tuples_on B(), B() holds g = f() iff for
a1,a2,a3 being Element of B() holds g.<*a1,a2,a3*> = F(a1,a2,a3) and
not Output 1GateCircStr(<*x1(),x2(),x3()*>,f()) in InputVertices S();
scheme :: CIRCCMB3:sch 17
Comb4CircResult {x1,x2,x3,x4()-> object, B()-> non empty finite set,
F(object,object,object,object)->Element of B(),
S() -> finite Signature of B(), C() -> Circuit of B()
, S(), f() -> Function of 4-tuples_on B(), B()}: for s being State of C() +*
1GateCircuit(<*x1(),x2(),x3(),x4()*>,f()) for s9 being State of C() st s9 = s|
the carrier of S() for a1, a2, a3, a4 being Element of B() st (x1() in
InnerVertices S() implies a1 = (Result s9).x1()) & (not x1() in InnerVertices S
() implies a1 = s.x1()) & (x2() in InnerVertices S() implies a2 = (Result s9).
x2()) & (not x2() in InnerVertices S() implies a2 = s.x2()) & (x3() in
InnerVertices S() implies a3 = (Result s9).x3()) & (not x3() in InnerVertices S
() implies a3 = s.x3()) & (x4() in InnerVertices S() implies a4 = (Result s9).
x4()) & (not x4() in InnerVertices S() implies a4 = s.x4()) holds (Result s).
Output(1GateCircStr(<*x1(),x2(),x3(),x4()*>,f())) = F(a1,a2,a3,a4)
provided
for g being Function of 4-tuples_on B(), B() holds g = f() iff for
a1,a2,a3,a4 being Element of B() holds g.<*a1,a2,a3,a4*> = F(a1,a2,a3,a4) and
not Output 1GateCircStr(<*x1(),x2(),x3(),x4()*>,f()) in InputVertices S();
scheme :: CIRCCMB3:sch 18
Comb5CircResult {x1,x2,x3,x4,x5()-> object, B()-> non empty finite set,
F(object,object,object,object,object)->Element of B(),
S() -> finite Signature of B(), C() ->
Circuit of B(), S(), f() -> Function of 5-tuples_on B(), B()}: for s being
State of C() +* 1GateCircuit(<*x1(),x2(),x3(),x4(),x5()*>,f()) for s9 being
State of C() st s9 = s|the carrier of S() for a1, a2, a3, a4, a5 being Element
of B() st (x1() in InnerVertices S() implies a1 = (Result s9).x1()) & (not x1()
in InnerVertices S() implies a1 = s.x1()) & (x2() in InnerVertices S() implies
a2 = (Result s9).x2()) & (not x2() in InnerVertices S() implies a2 = s.x2()) &
(x3() in InnerVertices S() implies a3 = (Result s9).x3()) & (not x3() in
InnerVertices S() implies a3 = s.x3()) & (x4() in InnerVertices S() implies a4
= (Result s9).x4()) & (not x4() in InnerVertices S() implies a4 = s.x4()) & (x5
() in InnerVertices S() implies a5 = (Result s9).x5()) & (not x5() in
InnerVertices S() implies a5 = s.x5()) holds (Result s).Output(1GateCircStr(<*
x1(),x2(),x3(),x4(),x5()*>,f())) = F(a1,a2,a3,a4,a5)
provided
for g being Function of 5-tuples_on B(), B() holds g = f() iff for
a1,a2,a3,a4,a5 being Element of B() holds g.<*a1,a2,a3,a4,a5*> = F(a1,a2,a3,a4,
a5) and
not Output 1GateCircStr(<*x1(),x2(),x3(),x4(),x5()*>,f()) in
InputVertices S();
begin :: Inputs without pairs
definition
let S be non empty ManySortedSign;
attr S is with_nonpair_inputs means
:: CIRCCMB3:def 11
InputVertices S is without_pairs;
end;
registration
cluster NAT -> without_pairs;
let X be without_pairs set;
cluster -> without_pairs for Subset of X;
end;
registration
cluster natural-valued -> nonpair-yielding for Function;
end;
registration
cluster one-to-one natural-valued for FinSequence;
end;
registration
let n be Element of NAT;
cluster one-to-one natural-valued for FinSeqLen of n;
end;
registration
let p be nonpair-yielding FinSequence;
let f be set;
cluster 1GateCircStr(p,f) -> with_nonpair_inputs;
end;
registration
cluster with_nonpair_inputs for one-gate ManySortedSign;
let X be non empty finite set;
cluster with_nonpair_inputs for one-gate Signature of X;
end;
registration
let S be with_nonpair_inputs non empty ManySortedSign;
cluster InputVertices S -> without_pairs;
end;
theorem :: CIRCCMB3:49
for S being with_nonpair_inputs non empty ManySortedSign for x being
Vertex of S st x is pair holds x in InnerVertices S;
registration
let S be unsplit gate`1=arity non empty ManySortedSign;
cluster InnerVertices S -> Relation-like;
end;
registration
let S be unsplit gate`2=den non empty non void ManySortedSign;
cluster InnerVertices S -> Relation-like;
end;
registration
let S1,S2 be with_nonpair_inputs unsplit gate`1=arity non empty
ManySortedSign;
cluster S1+*S2 -> with_nonpair_inputs;
end;
theorem :: CIRCCMB3:50
for x being non pair set, R being Relation holds not x in R;
theorem :: CIRCCMB3:51
for x1 being set, X being non empty finite set for f being
Function of 1-tuples_on X, X for S being with_nonpair_inputs Signature of X st
x1 in the carrier of S or x1 is non pair holds S +* 1GateCircStr(<*x1*>, f) is
with_nonpair_inputs;
registration
let X be non empty finite set;
let S be with_nonpair_inputs Signature of X;
let x1 be Vertex of S;
let f be Function of 1-tuples_on X, X;
cluster S +* 1GateCircStr(<*x1*>, f) -> with_nonpair_inputs;
end;
registration
let X be non empty finite set;
let S be with_nonpair_inputs Signature of X;
let x1 be non pair set;
let f be Function of 1-tuples_on X, X;
cluster S +* 1GateCircStr(<*x1*>, f) -> with_nonpair_inputs;
end;
theorem :: CIRCCMB3:52
for x1,x2 being set, X being non empty finite set for f being
Function of 2-tuples_on X, X for S being with_nonpair_inputs Signature of X st
(x1 in the carrier of S or x1 is non pair) & (x2 in the carrier of S or x2 is
non pair) holds S +* 1GateCircStr(<*x1,x2*>, f) is with_nonpair_inputs;
registration
let X be non empty finite set;
let S be with_nonpair_inputs Signature of X;
let x1 be Vertex of S, n2 be non pair set;
let f be Function of 2-tuples_on X, X;
cluster S +* 1GateCircStr(<*x1,n2*>, f) -> with_nonpair_inputs;
cluster S +* 1GateCircStr(<*n2,x1*>, f) -> with_nonpair_inputs;
end;
registration
let X be non empty finite set;
let S be with_nonpair_inputs Signature of X;
let x1,x2 be Vertex of S;
let f be Function of 2-tuples_on X, X;
cluster S +* 1GateCircStr(<*x1,x2*>, f) -> with_nonpair_inputs;
end;
theorem :: CIRCCMB3:53
for x1,x2,x3 being set, X being non empty finite set for f being
Function of 3-tuples_on X, X for S being with_nonpair_inputs Signature of X st
(x1 in the carrier of S or x1 is non pair) & (x2 in the carrier of S or x2 is
non pair) & (x3 in the carrier of S or x3 is non pair) holds S +* 1GateCircStr(
<*x1,x2,x3*>, f) is with_nonpair_inputs;
registration
let X be non empty finite set;
let S be with_nonpair_inputs Signature of X;
let x1,x2 be Vertex of S, n be non pair set;
let f be Function of 3-tuples_on X, X;
cluster S +* 1GateCircStr(<*x1,x2,n*>, f) -> with_nonpair_inputs;
cluster S +* 1GateCircStr(<*x1,n,x2*>, f) -> with_nonpair_inputs;
cluster S +* 1GateCircStr(<*n,x1,x2*>, f) -> with_nonpair_inputs;
end;
registration
let X be non empty finite set;
let S be with_nonpair_inputs Signature of X;
let x be Vertex of S, n1,n2 be non pair set;
let f be Function of 3-tuples_on X, X;
cluster S +* 1GateCircStr(<*x,n1,n2*>, f) -> with_nonpair_inputs;
cluster S +* 1GateCircStr(<*n1,x,n2*>, f) -> with_nonpair_inputs;
cluster S +* 1GateCircStr(<*n1,n2,x*>, f) -> with_nonpair_inputs;
end;
registration
let X be non empty finite set;
let S be with_nonpair_inputs Signature of X;
let x1,x2,x3 be Vertex of S;
let f be Function of 3-tuples_on X, X;
cluster S +* 1GateCircStr(<*x1,x2,x3*>, f) -> with_nonpair_inputs;
end;