:: Preliminaries to Automatic Generation of Mizar Documentation for Circuits
:: by Grzegorz Bancerek and Adam Naumowicz
::
:: Received July 26, 2002
:: Copyright (c) 2002-2026 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;
definitions TARSKI, XBOOLE_0, RELAT_1, REWRITE1, MSAFREE2, CIRCUIT2, FINSET_1,
CIRCCOMB, FACIRC_1;
equalities TARSKI, RELAT_1, MSAFREE2;
expansions TARSKI, CIRCCOMB, FACIRC_1;
theorems CIRCCOMB, ZFMISC_1, TARSKI, XBOOLE_0, FINSEQ_1, FUNCT_1, FINSEQ_2,
CIRCUIT1, CARD_3, CIRCCMB2, FUNCOP_1, PBOOLE, FINSEQ_3, ENUMSET1,
FACIRC_1, ORDINAL2, FUNCT_4, FINSET_1, NAT_1, RELAT_1, MSUALG_1,
MSAFREE2, FUNCT_2, RELSET_1, CLASSES1, ORDINAL1, CIRCUIT2, XBOOLE_1,
XREAL_1, XXREAL_0, FINSEQ_4, VALUED_0, XXREAL_2, PARTFUN1, CARD_1,
XTUPLE_0;
schemes TARSKI, XBOOLE_0, FUNCT_2, NAT_1, REWRITE1, CLASSES1, RELAT_1;
begin :: Stabilizing circuits
theorem Th1:
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
proof
let S be non void Circuit-like non empty ManySortedSign;
let A be non-empty Circuit of S;
let s be State of A, x be set such that
A1: x in InputVertices S;
defpred P[Nat] means Following(s,$1).x = s.x;
A2: now
let n be Nat;
assume
A3: P[n];
Following(s,n+1).x = (Following Following(s,n)).x by FACIRC_1:12
.= s.x by A1,A3,CIRCUIT2:def 5;
hence P[n+1];
end;
A4: P[ 0 ] by FACIRC_1:11;
thus for n be Nat holds P[n] from NAT_1:sch 2(A4,A2);
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;
attr s is stabilizing means
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
:Def2:
for s being State of A holds s is stabilizing;
attr A is with_stabilization-limit means
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;
coherence
proof
let A be non-empty Circuit of S;
given n being Element of NAT such that
A1: for s being State of A holds Following(s,n) is stable;
let s be State of A;
take n;
thus thesis by A1;
end;
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
A1: s is stabilizing;
func Result s -> State of A means
:Def4:
it is stable & ex n being Element of NAT st it = Following(s,n);
existence
by A1;
uniqueness
proof
let s1,s2 be State of A;
assume that
A2: s1 is stable and
A3: ex n being Element of NAT st s1 = Following(s,n) and
A4: s2 is stable and
A5: ex n being Element of NAT st s2 = Following(s,n);
consider n1 being Element of NAT such that
A6: s1 = Following(s,n1) by A3;
consider n2 being Element of NAT such that
A7: s2 = Following(s,n2) by A5;
per cases;
suppose
n1<=n2;
hence thesis by A2,A6,A7,CIRCCMB2:4;
end;
suppose
n2<=n1;
hence thesis by A4,A6,A7,CIRCCMB2:4;
end;
end;
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
A1: s is stabilizing;
func stabilization-time s -> Element of NAT means
:Def5:
Following(s,it) is
stable & for n being Element of NAT st n < it holds not Following(s,n) is
stable;
existence
proof
defpred P[Nat] means Following(s,$1) is stable;
ex k being Element of NAT st P[k] by A1;
then
A2: ex k being Nat st P[k];
consider m being Nat such that
A3: P[m] & for n being Nat st P[n] holds m <= n from NAT_1:sch 5(A2);
reconsider m as Element of NAT by ORDINAL1:def 12;
take m;
thus thesis by A3;
end;
uniqueness
proof
let n1,n2 be Element of NAT such that
A4: Following(s,n1) is stable and
A5: ( for n being Element of NAT st n < n1 holds not Following(s,n) is
stable)& Following(s,n2) is stable and
A6: for n being Element of NAT st n < n2 holds not Following(s,n) is stable;
assume
A7: n1<>n2;
per cases by A7,XXREAL_0:1;
suppose
n1 < n2;
hence contradiction by A4,A6;
end;
suppose
n2 < n1;
hence contradiction by A5;
end;
end;
end;
theorem Th2:
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)
proof
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
A1: s is stabilizing;
Following(s,stabilization-time s) is stable by A1,Def5;
hence thesis by A1,Def4;
end;
theorem
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
proof
let S be non void Circuit-like non empty ManySortedSign;
let A be non-empty Circuit of S;
let s be State of A, n be Element of NAT;
assume
A1: Following(s,n) is stable;
then s is stabilizing;
hence thesis by A1,Def5;
end;
theorem Th4:
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)
proof
let S be non void Circuit-like non empty ManySortedSign;
let A be non-empty Circuit of S;
let s be State of A, n be Element of NAT;
assume
A1: Following(s,n) is stable;
then s is stabilizing;
hence thesis by A1,Def4;
end;
theorem Th5:
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
)
proof
let S be non void Circuit-like non empty ManySortedSign;
let A be non-empty Circuit of S;
let s be State of A, n be Element of NAT;
assume that
A1: s is stabilizing and
A2: n >= stabilization-time s;
Result s is stable by A1,Def4;
then Following(s, stabilization-time s) is stable by A1,Th2;
then Following(s,n) is stable by A2,CIRCCMB2:4;
hence thesis by Th4;
end;
theorem
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
proof
let S be non void Circuit-like non empty ManySortedSign;
let A be non-empty Circuit of S;
let s be State of A;
assume s is stabilizing;
then Result s = Following(s,stabilization-time s) by Th2;
hence thesis by Th1;
end;
theorem Th7:
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
proof
let S1,S2 be non void Circuit-like non empty ManySortedSign such that
A1: InputVertices S1 misses InnerVertices S2 & InputVertices S2 misses
InnerVertices S1;
let S be non void Circuit-like non empty ManySortedSign such that
A2: S=S1 +* S2;
let A1 be non-empty Circuit of S1;
let A2 be non-empty Circuit of S2;
assume
A3: A1 tolerates A2;
let A be non-empty Circuit of S such that
A4: A = A1 +* A2;
let s be State of A;
let s1 be State of A1;
let s2 be State of A2;
assume that
A5: s1=s|the carrier of S1 & s2=s|the carrier of S2 and
A6: s1 is stabilizing and
A7: s2 is stabilizing;
consider n1 being Element of NAT such that
A8: Following(s1,n1) is stable by A6;
consider n2 being Element of NAT such that
A9: Following(s2,n2) is stable by A7;
Following(s,max(n1,n2)) is stable by A1,A2,A3,A4,A5,A8,A9,CIRCCMB2:22;
hence thesis;
end;
theorem
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)
proof
let S1,S2 be non void Circuit-like non empty ManySortedSign such that
A1: InputVertices S1 misses InnerVertices S2 & InputVertices S2 misses
InnerVertices S1;
let S be non void Circuit-like non empty ManySortedSign such that
A2: S=S1 +* S2;
let A1 be non-empty Circuit of S1;
let A2 be non-empty Circuit of S2;
assume
A3: A1 tolerates A2;
let A be non-empty Circuit of S such that
A4: A = A1 +* A2;
let s be State of A;
let s1 be State of A1 such that
A5: s1=s|the carrier of S1 and
A6: s1 is stabilizing;
set st1=stabilization-time(s1);
let s2 be State of A2 such that
A7: s2=s|the carrier of S2 and
A8: s2 is stabilizing;
set st2=stabilization-time(s2);
A9: Following(s1,st1) is stable by A6,Def5;
A10: now
let n be Element of NAT such that
A11: n < max(st1,st2);
per cases;
suppose
st1<=st2;
then n < st2 by A11,XXREAL_0:def 10;
then not Following(s2,n) is stable by A8,Def5;
hence not Following(s,n) is stable by A1,A2,A3,A4,A5,A7,CIRCCMB2:23;
end;
suppose
st2<=st1;
then n < st1 by A11,XXREAL_0:def 10;
then not Following(s1,n) is stable by A6,Def5;
hence not Following(s,n) is stable by A1,A2,A3,A4,A5,A7,CIRCCMB2:23;
end;
end;
Following(s2,st2) is stable by A8,Def5;
then
A12: Following(s,max(st1,st2)) is stable by A1,A2,A3,A4,A5,A7,A9,CIRCCMB2:22;
s is stabilizing by A1,A2,A3,A4,A5,A6,A7,A8,Th7;
hence thesis by A12,A10,Def5;
end;
theorem Th9:
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
proof
let S1,S2 be non void Circuit-like non empty ManySortedSign such that
A1: InputVertices S1 misses InnerVertices S2;
let S be non void Circuit-like non empty ManySortedSign such that
A2: S = S1 +* S2;
let A1 be non-empty Circuit of S1;
let A2 be non-empty Circuit of S2;
assume
A3: A1 tolerates A2;
let A be non-empty Circuit of S such that
A4: A = A1 +* A2;
let s be State of A;
let s1 be State of A1 such that
A5: s1 = s|the carrier of S1 and
A6: s1 is stabilizing;
set n1 = stabilization-time s1;
A7: Following(s1,n1) is stable by A6,Def5;
let s2 be State of A2 such that
A8: s2 = Following(s, n1)|the carrier of S2 and
A9: s2 is stabilizing;
set n2 = stabilization-time s2;
Following(s2,n2) is stable by A9,Def5;
then Following(s,n1+n2) is stable by A1,A2,A3,A4,A5,A7,A8,CIRCCMB2:19;
hence thesis;
end;
theorem Th10:
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)
proof
let S1,S2 be non void Circuit-like non empty ManySortedSign such that
A1: InputVertices S1 misses InnerVertices S2;
let S be non void Circuit-like non empty ManySortedSign such that
A2: S=S1 +* S2;
let A1 be non-empty Circuit of S1;
let A2 be non-empty Circuit of S2;
assume
A3: A1 tolerates A2;
let A be non-empty Circuit of S such that
A4: A = A1 +* A2;
let s be State of A;
let s1 be State of A1 such that
A5: s1=s|the carrier of S1 and
A6: s1 is stabilizing;
set st1=stabilization-time(s1);
let s2 be State of A2 such that
A7: s2=Following(s,st1)|the carrier of S2 and
A8: s2 is stabilizing;
set st2=stabilization-time(s2);
A9: Following(s1,st1) is stable by A6,Def5;
A10: now
let n be Element of NAT such that
A11: n < st1+st2;
per cases;
suppose
st1 <= n;
then consider m being Nat such that
A12: n = st1+m by NAT_1:10;
reconsider m as Element of NAT by ORDINAL1:def 12;
m < st2 by A11,A12,XREAL_1:6;
then
A13: Following(s2,m) is not stable by A8,Def5;
Following(s1,st1) = Following(s,st1)|the carrier of S1 by A1,A2,A3,A4,A5,
CIRCCMB2:13;
then Following(s2,m) = Following(Following(s,st1),m)|the carrier of S2
by A1,A2,A3,A4,A7,A9,CIRCCMB2:18
.= Following(s,n)|the carrier of S2 by A12,FACIRC_1:13;
hence Following(s,n) is not stable by A2,A3,A4,A13,CIRCCMB2:17;
end;
suppose
n < st1;
then
A14: Following(s1,n) is not stable by A6,Def5;
Following(s,n)|the carrier of S1 = Following(s1,n) by A1,A2,A3,A4,A5,
CIRCCMB2:13;
hence Following(s,n) is not stable by A2,A3,A4,A14,CIRCCMB2:17;
end;
end;
Following(s2,st2) is stable by A8,Def5;
then
A15: Following(s,st1+st2) is stable by A1,A2,A3,A4,A5,A7,A9,CIRCCMB2:19;
s is stabilizing by A1,A2,A3,A4,A5,A6,A7,A8,Th9;
hence thesis by A15,A10,Def5;
end;
theorem
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
proof
let S1,S2,S be non void Circuit-like non empty ManySortedSign such that
A1: InputVertices S1 misses InnerVertices S2 & S = S1+*S2;
let A1 be non-empty Circuit of S1, A2 be non-empty Circuit of S2;
let A be non-empty Circuit of S such that
A2: A1 tolerates A2 & A = A1+*A2;
let s be State of A, s1 be State of A1 such that
A3: s1 = s|the carrier of S1 and
A4: s1 is stabilizing;
let s2 be State of A2 such that
A5: s2 = Following(s, stabilization-time s1)|the carrier of S2 & s2 is
stabilizing;
A6: stabilization-time s = (stabilization-time s1)+stabilization-time s2 by A1
,A2,A3,A4,A5,Th10;
thus (Result s)|the carrier of S1 = Following(s, stabilization-time s)|the
carrier of S1 by A1,A2,A3,A4,A5,Th2,Th9
.= Following(s1, stabilization-time s) by A1,A2,A3,CIRCCMB2:13
.= Result s1 by A4,A6,Th5,NAT_1:11;
end;
begin :: One-gate circuits
theorem Th12:
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
proof
let x be set, X be non empty finite set;
let n being Element of NAT;
let p being FinSeqLen of n;
let g be Function of n-tuples_on X, X;
let s be State of 1GateCircuit(p,g);
set S = 1GateCircStr(p,g), A=1GateCircuit(p,g);
A1: rng (s*p) c= X
proof
let o be object;
A2: rng s c= X
proof
reconsider tc = the carrier of S as non empty set;
let z be object;
reconsider tS = the Sorts of A as non-empty ManySortedSet of tc;
assume z in rng s;
then consider a being object such that
A3: a in dom s and
A4: z = s.a by FUNCT_1:def 3;
reconsider a as Vertex of S by A3,CIRCUIT1:3;
dom s = dom tS by CARD_3:9;
then s.a in (the Sorts of A).a by A3,CARD_3:9;
hence thesis by A4,CIRCCOMB:54;
end;
assume o in rng (s*p);
then o in rng s by FUNCT_1:14;
hence thesis by A2;
end;
A5: rng p c= dom s
proof
let o be object;
assume o in rng p;
then o in rng p \/ {[p,g]} by XBOOLE_0:def 3;
then o in the carrier of S by CIRCCOMB:def 6;
hence thesis by CIRCUIT1:3;
end;
then s*p is FinSequence by FINSEQ_1:16;
then reconsider sx=s*p as FinSequence of X by A1,FINSEQ_1:def 4;
len sx = len p by A5,FINSEQ_2:29
.= n by CARD_1:def 7;
hence thesis by FINSEQ_2:92;
end;
theorem Th13:
for x1,x2,x3,x4 being object holds rng <*x1,x2,x3,x4*> = {x1,x2,x3,x4}
proof
let x1,x2,x3,x4 be object;
for y being object holds y in {x1,x2,x3,x4} iff
ex x being object st x in dom
<*x1,x2,x3,x4*> & y = <*x1,x2,x3,x4*>.x
proof
let y be object;
thus y in {x1,x2,x3,x4} implies
ex x being object st x in dom <*x1,x2,x3,x4*>
& y = <*x1,x2,x3,x4*>.x
proof
A1: dom <*x1,x2,x3,x4*> = {1,2,3,4} by FINSEQ_1:89,FINSEQ_3:2;
assume
A2: y in {x1,x2,x3,x4};
per cases by A2,ENUMSET1:def 2;
suppose
A3: y=x1;
take 1;
thus 1 in dom <*x1,x2,x3,x4*> by A1,ENUMSET1:def 2;
thus thesis by A3;
end;
suppose
A4: y=x2;
take 2;
thus 2 in dom <*x1,x2,x3,x4*> by A1,ENUMSET1:def 2;
thus thesis by A4;
end;
suppose
A5: y=x3;
take 3;
thus 3 in dom <*x1,x2,x3,x4*> by A1,ENUMSET1:def 2;
thus thesis by A5;
end;
suppose
A6: y=x4;
take 4;
thus 4 in dom <*x1,x2,x3,x4*> by A1,ENUMSET1:def 2;
thus thesis by A6;
end;
end;
given x being object such that
A7: x in dom <*x1,x2,x3,x4*> and
A8: y = <*x1,x2,x3,x4*>.x;
x in Seg 4 by A7,FINSEQ_1:89;
then x=1 or x=2 or x=3 or x=4 by ENUMSET1:def 2,FINSEQ_3:2;
then
<*x1,x2,x3,x4*>.x = x1 or <*x1,x2,x3,x4*>.x = x2 or <*x1,x2,x3,x4*>.x
= x3 or <*x1,x2,x3,x4*>.x = x4;
hence thesis by A8,ENUMSET1:def 2;
end;
hence thesis by FUNCT_1:def 3;
end;
theorem Th14:
for x1,x2,x3,x4,x5 being object
holds rng <*x1,x2,x3,x4,x5*> = {x1, x2,x3,x4,x5}
proof
let x1,x2,x3,x4,x5 be object;
for y being object holds y in {x1,x2,x3,x4,x5} iff
ex x being object st x in
dom <*x1,x2,x3,x4,x5*> & y = <*x1,x2,x3,x4,x5*>.x
proof
let y be object;
thus y in {x1,x2,x3,x4,x5} implies
ex x being object st x in dom <*x1,x2,x3,
x4,x5*> & y = <*x1,x2,x3,x4,x5*>.x
proof
A1: dom <*x1,x2,x3,x4,x5*> = {1,2,3,4,5} by FINSEQ_1:89,FINSEQ_3:3;
assume
A2: y in {x1,x2,x3,x4,x5};
per cases by A2,ENUMSET1:def 3;
suppose
A3: y=x1;
take 1;
thus 1 in dom <*x1,x2,x3,x4,x5*> by A1,ENUMSET1:def 3;
thus thesis by A3;
end;
suppose
A4: y=x2;
take 2;
thus 2 in dom <*x1,x2,x3,x4,x5*> by A1,ENUMSET1:def 3;
thus thesis by A4;
end;
suppose
A5: y=x3;
take 3;
thus 3 in dom <*x1,x2,x3,x4,x5*> by A1,ENUMSET1:def 3;
thus thesis by A5;
end;
suppose
A6: y=x4;
take 4;
thus 4 in dom <*x1,x2,x3,x4,x5*> by A1,ENUMSET1:def 3;
thus thesis by A6;
end;
suppose
A7: y=x5;
take 5;
thus 5 in dom <*x1,x2,x3,x4,x5*> by A1,ENUMSET1:def 3;
thus thesis by A7;
end;
end;
given x being object such that
A8: x in dom <*x1,x2,x3,x4,x5*> and
A9: y = <*x1,x2,x3,x4,x5*>.x;
x in Seg 5 by A8,FINSEQ_1:89;
then x=1 or x=2 or x=3 or x=4 or x=5 by ENUMSET1:def 3,FINSEQ_3:3;
then
<*x1,x2,x3,x4,x5*>.x = x1 or <*x1,x2,x3,x4,x5*>.x = x2 or <*x1,x2,x3,
x4,x5*>.x = x3 or <*x1,x2,x3,x4,x5*>.x = x4 or <*x1,x2,x3,x4,x5*>.x = x5;
hence thesis by A9,ENUMSET1:def 3;
end;
hence thesis by FUNCT_1:def 3;
end;
definition
let S be ManySortedSign;
attr S is one-gate means
:Def6:
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
:Def7:
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;
coherence
proof
the carrier of 1GateCircStr(p,x) = (rng p) \/ {[p,x]} by CIRCCOMB:def 6;
hence thesis;
end;
end;
registration
cluster one-gate -> strict non void non empty unsplit gate`1=arity finite
for ManySortedSign;
coherence;
end;
registration
cluster one-gate -> gate`2=den for non empty ManySortedSign;
coherence;
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;
coherence;
end;
registration
cluster one-gate for ManySortedSign;
existence
proof
set X = the non empty finite set,n = the Element of NAT,p = the FinSeqLen of n,
f = the Function of n-tuples_on X,X;
take 1GateCircStr(p,f);
thus thesis;
end;
end;
registration
let S be one-gate ManySortedSign;
cluster one-gate -> strict non-empty for Circuit of S;
coherence;
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;
coherence;
end;
registration
let S be one-gate ManySortedSign;
cluster one-gate non-empty for Circuit of S;
existence
proof
consider 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 such that
A1: S = 1GateCircStr(p,f) by Def6;
reconsider A = 1GateCircuit(p,f) as finite-yielding MSAlgebra over S by A1;
take A;
thus thesis by A1;
end;
end;
definition
let S be one-gate ManySortedSign;
func Output S -> Vertex of S equals
union the carrier' of S;
coherence
proof
consider 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 such that
A1: S = 1GateCircStr(p,f) by Def6;
[p,f] in {[p,f]} by TARSKI:def 1;
then
A2: [p,f] in (rng p) \/ {[p,f]} by XBOOLE_0:def 3;
the carrier' of S = {[p,f]} by A1,CIRCCOMB:def 6;
then union the carrier' of S = [p,f] by ZFMISC_1:25;
hence thesis by A1,A2,CIRCCOMB:def 6;
end;
end;
registration
let S be one-gate ManySortedSign;
cluster Output S -> pair;
coherence
proof
consider 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 such that
A1: S = 1GateCircStr(p,f) by Def6;
the carrier' of S = {[p,f]} by A1,CIRCCOMB:def 6;
hence thesis by ZFMISC_1:25;
end;
end;
theorem Th15:
for S being one-gate ManySortedSign, p being FinSequence, x
being set st S = 1GateCircStr(p,x) holds Output S = [p,x]
proof
let S be one-gate ManySortedSign, p be FinSequence, x be set;
assume S = 1GateCircStr(p,x);
hence Output S = union {[p,x]} by CIRCCOMB:def 6
.= [p,x] by ZFMISC_1:25;
end;
theorem Th16:
for S being one-gate ManySortedSign holds InnerVertices S = { Output S}
proof
let S be one-gate ManySortedSign;
consider 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 such that
A1: S = 1GateCircStr(p,f) by Def6;
Output S = [p,f] by A1,Th15;
hence thesis by A1,CIRCCOMB:42;
end;
theorem
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)
proof
let S be one-gate ManySortedSign;
let A be one-gate Circuit of S;
let n be Element of NAT;
let X be finite non empty set;
let f be Function of n-tuples_on X, X, p be FinSeqLen of n such that
A1: A = 1GateCircuit(p,f);
consider X1 being non empty finite set, n1 being Element of NAT, p1 being
FinSeqLen of n1, f1 being Function of n1-tuples_on X1,X1 such that
A2: S = 1GateCircStr(p1,f1) and
A3: A = 1GateCircuit(p1,f1) by Def7;
{[p,f]} = the carrier' of 1GateCircStr(p,f) by CIRCCOMB:def 6
.= dom the Charact of 1GateCircuit(p1,f1) by A1,A3,PARTFUN1:def 2
.= the carrier' of 1GateCircStr(p1,f1) by PARTFUN1:def 2
.= {[p1,f1]} by CIRCCOMB:def 6;
then
A4: [p,f] = [p1,f1] by ZFMISC_1:3;
then p = p1 by XTUPLE_0:1;
hence thesis by A2,A4,XTUPLE_0:1;
end;
theorem
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)
proof
let n be Element of NAT;
let X be finite non empty set;
let f be Function of n-tuples_on X, X, p be FinSeqLen of n;
let s be State of 1GateCircuit(p,f);
Output 1GateCircStr(p,f) = [p,f] by Th15;
hence thesis by CIRCCOMB:56;
end;
theorem Th19:
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
proof
let S be one-gate ManySortedSign;
let A be one-gate Circuit of S;
let s be State of A;
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) by Def7;
hence thesis by CIRCCMB2:2;
end;
registration
let S be non void Circuit-like non empty ManySortedSign;
cluster one-gate -> with_stabilization-limit for non-empty Circuit of S;
coherence
proof
let A be non-empty Circuit of S;
assume
A1: A is one-gate;
then 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);
then reconsider S1=S as one-gate ManySortedSign;
reconsider A1=A as one-gate Circuit of S1 by A1;
take 1;
let s be State of A;
reconsider s1=s as State of A1;
Following s1 is stable by Th19;
hence thesis by FACIRC_1:14;
end;
end;
theorem Th20:
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
proof
let S be one-gate ManySortedSign;
let A be one-gate Circuit of S;
let s be State of A;
A1: Following s = Following(s,1) by FACIRC_1:14;
s is stabilizing & Following s is stable by Def2,Th19;
hence thesis by A1,Def4;
end;
theorem Th21:
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
proof
let S be one-gate ManySortedSign;
let A be one-gate Circuit of S;
let s be State of A;
Following s is stable by Th19;
then
A1: Following(s,1) is stable by FACIRC_1:14;
s is stabilizing by Def2;
hence thesis by A1,Def5;
end;
scheme
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()) proof
deffunc F(Element of 1-tuples_on X()) = f($1.1);
consider g being Function of 1-tuples_on X(), X() such that
A1: for a being Element of 1-tuples_on X() holds g.a = F(a) from FUNCT_2
:sch 4;
reconsider S = 1GateCircStr(<*x()*>,g) as one-gate ManySortedSign;
take S;
reconsider A = 1GateCircuit(<*x()*>,g) as one-gate Circuit of S;
take A;
rng <*x()*> = {x()} by FINSEQ_1:38;
hence InputVertices S = {x()} by CIRCCOMB:42;
let s be State of A;
reconsider sx = s*<*x()*> as Element of 1-tuples_on X() by Th12;
dom <*x()*> = Seg 1 by FINSEQ_1:38;
then
A2: 1 in dom <*x()*> by FINSEQ_1:1;
thus (Result s).Output S = (Following s).(Output S) by Th20
.= (Following s).[<*x()*>,g] by Th15
.= g.(s*<*x()*>) by CIRCCOMB:56
.= f(sx.1) by A1
.= f(s.(<*x()*>.1)) by A2,FUNCT_1:13
.= f(s.x());
end;
scheme
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()) proof
deffunc F(Element of 2-tuples_on X()) = f($1.1,$1.2);
consider g being Function of 2-tuples_on X(), X() such that
A1: for a being Element of 2-tuples_on X() holds g.a = F(a) from FUNCT_2
:sch 4;
reconsider S = 1GateCircStr(<*x1(),x2()*>,g) as one-gate ManySortedSign;
take S;
reconsider A = 1GateCircuit(<*x1(),x2()*>,g) as one-gate Circuit of S;
take A;
rng <*x1(),x2()*> = {x1(),x2()} by FINSEQ_2:127;
hence InputVertices S = {x1(),x2()} by CIRCCOMB:42;
let s be State of A;
reconsider sx = s*<*x1(),x2()*> as Element of 2-tuples_on X() by Th12;
A2: dom <*x1(),x2()*> = Seg 2 by FINSEQ_1:89;
then
A3: 1 in dom <*x1(),x2()*> by FINSEQ_1:1;
A4: 2 in dom <*x1(),x2()*> by A2,FINSEQ_1:1;
Result s = Following s by Th20;
hence (Result s).(Output S) = (Following s).[<*x1(),x2()*>,g] by Th15
.= g.(s*<*x1(),x2()*>) by CIRCCOMB:56
.= f(sx.1,sx.2) by A1
.= f(s.(<*x1(),x2()*>.1),sx.2) by A3,FUNCT_1:13
.= f(s.(<*x1(),x2()*>.1),s.(<*x1(),x2()*>.2)) by A4,FUNCT_1:13
.= f(s.x1(),s.(<*x1(),x2()*>.2))
.= f(s.x1(),s.x2());
end;
scheme
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()) proof
deffunc F(Element of 3-tuples_on X()) = f($1.1,$1.2,$1.3);
consider g being Function of 3-tuples_on X(), X() such that
A1: for a being Element of 3-tuples_on X() holds g.a = F(a) from FUNCT_2
:sch 4;
reconsider S = 1GateCircStr(<*x1(),x2(),x3()*>,g) as one-gate ManySortedSign;
take S;
reconsider A = 1GateCircuit(<*x1(),x2(),x3()*>,g) as one-gate Circuit of S;
take A;
rng <*x1(),x2(),x3()*> = {x1(),x2(),x3()} by FINSEQ_2:128;
hence InputVertices S = {x1(),x2(),x3()} by CIRCCOMB:42;
let s be State of A;
reconsider sx = s*<*x1(),x2(),x3()*> as Element of 3-tuples_on X() by Th12;
A2: dom <*x1(),x2(),x3()*> = Seg 3 by FINSEQ_1:89;
then
A3: 1 in dom <*x1(),x2(),x3()*> by FINSEQ_1:1;
A4: 3 in dom <*x1(),x2(),x3()*> by A2,FINSEQ_1:1;
A5: 2 in dom <*x1(),x2(),x3()*> by A2,FINSEQ_1:1;
Result s = Following s by Th20;
hence (Result s).(Output S) = (Following s).[<*x1(),x2(),x3()*>,g] by Th15
.= g.(s*<*x1(),x2(),x3()*>) by CIRCCOMB:56
.= f(sx.1,sx.2,sx.3) by A1
.= f(s.(<*x1(),x2(),x3()*>.1),sx.2,sx.3) by A3,FUNCT_1:13
.= f(s.x1(),sx.2,sx.3)
.= f(s.x1(),s.(<*x1(),x2(),x3()*>.2),sx.3) by A5,FUNCT_1:13
.= f(s.x1(),s.x2(),sx.3)
.= f(s.x1(),s.x2(),s.(<*x1(),x2(),x3()*>.3)) by A4,FUNCT_1:13
.= f(s.x1(),s.x2(),s.x3());
end;
scheme
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()) proof
deffunc F(Element of 4-tuples_on X()) = f($1.1,$1.2,$1.3,$1.4);
consider g being Function of 4-tuples_on X(), X() such that
A1: for a being Element of 4-tuples_on X() holds g.a = F(a) from FUNCT_2
:sch 4;
reconsider S = 1GateCircStr(<*x1(),x2(),x3(),x4()*>,g) as one-gate
ManySortedSign;
take S;
reconsider A = 1GateCircuit(<*x1(),x2(),x3(),x4()*>,g) as one-gate Circuit
of S;
take A;
rng <*x1(),x2(),x3(),x4()*> = {x1(),x2(),x3(),x4()} by Th13;
hence InputVertices S = {x1(),x2(),x3(),x4()} by CIRCCOMB:42;
let s be State of A;
reconsider sx = s*<*x1(),x2(),x3(),x4()*> as Element of 4-tuples_on X() by
Th12;
A2: dom <*x1(),x2(),x3(),x4()*> = Seg 4 by FINSEQ_1:89;
then
A3: 1 in dom <*x1(),x2(),x3(),x4()*> by FINSEQ_1:1;
A4: 3 in dom <*x1(),x2(),x3(),x4()*> by A2,FINSEQ_1:1;
A5: 2 in dom <*x1(),x2(),x3(),x4()*> by A2,FINSEQ_1:1;
A6: 4 in dom <*x1(),x2(),x3(),x4()*> by A2,FINSEQ_1:1;
Result s = Following s by Th20;
hence (Result s).(Output S) = (Following s).[<*x1(),x2(),x3(),x4()*>,g] by
Th15
.= g.(s*<*x1(),x2(),x3(),x4()*>) by CIRCCOMB:56
.= f(sx.1,sx.2,sx.3,sx.4) by A1
.= f(s.(<*x1(),x2(),x3(),x4()*>.1),sx.2,sx.3,sx.4) by A3,FUNCT_1:13
.= f(s.x1(),sx.2,sx.3,sx.4)
.= f(s.x1(),s.(<*x1(),x2(),x3(),x4()*>.2),sx.3,sx.4) by A5,FUNCT_1:13
.= f(s.x1(),s.x2(),sx.3,sx.4)
.= f(s.x1(),s.x2(),s.(<*x1(),x2(),x3(),x4()*>.3),sx.4) by A4,FUNCT_1:13
.= f(s.x1(),s.x2(),s.x3(),sx.4)
.= f(s.x1(),s.x2(),s.x3(),s.(<*x1(),x2(),x3(),x4()*>.4)) by A6,FUNCT_1:13
.= f(s.x1(),s.x2(),s.x3(),s.x4());
end;
scheme
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())
proof
deffunc F(Element of 5-tuples_on X()) = f($1.1,$1.2,$1.3,$1.4,$1.5);
consider g being Function of 5-tuples_on X(), X() such that
A1: for a being Element of 5-tuples_on X() holds g.a = F(a) from FUNCT_2
:sch 4;
reconsider S = 1GateCircStr(<*x1(),x2(),x3(),x4(),x5()*>,g) as one-gate
ManySortedSign;
take S;
reconsider A = 1GateCircuit(<*x1(),x2(),x3(),x4(),x5()*>,g) as one-gate
Circuit of S;
take A;
rng <*x1(),x2(),x3(),x4(),x5()*> = {x1(),x2(),x3(),x4(),x5()} by Th14;
hence InputVertices S = {x1(),x2(),x3(),x4(),x5()} by CIRCCOMB:42;
let s be State of A;
reconsider sx = s*<*x1(),x2(),x3(),x4(),x5()*> as Element of 5-tuples_on X()
by Th12;
A2: dom <*x1(),x2(),x3(),x4(),x5()*> = Seg 5 by FINSEQ_1:89;
then
A3: 1 in dom <*x1(),x2(),x3(),x4(),x5()*> by FINSEQ_1:1;
A4: 5 in dom <*x1(),x2(),x3(),x4(),x5()*> by A2,FINSEQ_1:1;
A5: 4 in dom <*x1(),x2(),x3(),x4(),x5()*> by A2,FINSEQ_1:1;
A6: 3 in dom <*x1(),x2(),x3(),x4(),x5()*> by A2,FINSEQ_1:1;
A7: 2 in dom <*x1(),x2(),x3(),x4(),x5()*> by A2,FINSEQ_1:1;
Result s = Following s by Th20;
hence (Result s).(Output S) = (Following s).[<*x1(),x2(),x3(),x4(),x5()*>,g]
by Th15
.= g.(s*<*x1(),x2(),x3(),x4(),x5()*>) by CIRCCOMB:56
.= f(sx.1,sx.2,sx.3,sx.4,sx.5) by A1
.= f(s.(<*x1(),x2(),x3(),x4(),x5()*>.1),sx.2,sx.3,sx.4,sx.5) by A3,
FUNCT_1:13
.= f(s.x1(),sx.2,sx.3,sx.4,sx.5)
.= f(s.x1(),s.(<*x1(),x2(),x3(),x4(),x5()*>.2),sx.3,sx.4,sx.5) by A7,
FUNCT_1:13
.= f(s.x1(),s.x2(),sx.3,sx.4,sx.5)
.= f(s.x1(),s.x2(),s.(<*x1(),x2(),x3(),x4(),x5()*>.3),sx.4,sx.5) by A6,
FUNCT_1:13
.= f(s.x1(),s.x2(),s.x3(),sx.4,sx.5)
.= f(s.x1(),s.x2(),s.x3(),s.(<*x1(),x2(),x3(),x4(),x5()*>.4),sx.5) by A5,
FUNCT_1:13
.= f(s.x1(),s.x2(),s.x3(),s.x4(),sx.5)
.= f(s.x1(),s.x2(),s.x3(),s.x4(),s.(<*x1(),x2(),x3(),x4(),x5()*>.5)) by A4,
FUNCT_1:13
.= f(s.x1(),s.x2(),s.x3(),s.x4(),s.x5());
end;
begin :: Mono-sorted circuits
theorem Th22:
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
proof
let X,Y be non empty set;
let n,m be Element of NAT;
assume that
A1: n<>0 and
A2: n-tuples_on X = m-tuples_on Y;
thus X=Y
proof
thus X c= Y
proof
let a be object;
assume a in X;
then n |-> a is Element of n-tuples_on X by FINSEQ_2:112;
then n |-> a in m-tuples_on Y by A2;
then n |-> a in { s where s is Element of Y*: len s = m } by
FINSEQ_2:def 4;
then ex s being Element of Y* st s = n |-> a & len s = m;
then
A3: rng (n |-> a) c= Y by FINSEQ_1:def 4;
n |-> a = (Seg n) --> a by FINSEQ_2:def 2;
then rng (n |-> a) = {a} by A1,FUNCOP_1:8;
then a in rng (n |-> a) by TARSKI:def 1;
hence thesis by A3;
end;
let a be object;
A4: m |-> a = (Seg m) --> a by FINSEQ_2:def 2;
assume a in Y;
then m |-> a is Element of m-tuples_on Y by FINSEQ_2:112;
then m |-> a in n-tuples_on X by A2;
then m |-> a in { s where s is Element of X*: len s = n } by FINSEQ_2:def 4
;
then
A5: ex s being Element of X* st s = m |-> a & len s = n;
then m=n by CARD_1:def 7;
then rng (m |-> a) = {a} by A1,A4,FUNCOP_1:8;
then
A6: a in rng (m |-> a) by TARSKI:def 1;
rng (m |-> a) c= X by A5,FINSEQ_1:def 4;
hence thesis by A6;
end;
thus thesis by A2,FINSEQ_2:110;
end;
theorem
for S1,S2 being non empty ManySortedSign for v being Vertex of S1
holds v is Vertex of S1+*S2
proof
let S1,S2 be non empty ManySortedSign;
let v be Vertex of S1;
v in (the carrier of S1) \/ (the carrier of S2) by XBOOLE_0:def 3;
hence thesis by CIRCCOMB:def 2;
end;
theorem
for S1,S2 being non empty ManySortedSign for v being Vertex of S2
holds v is Vertex of S1+*S2
proof
let S1,S2 be non empty ManySortedSign;
let v be Vertex of S2;
v in (the carrier of S1) \/ (the carrier of S2) by XBOOLE_0:def 3;
hence thesis by CIRCCOMB:def 2;
end;
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
: Def9:
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;
existence
proof
set p = the FinSeqLen of 1;
set f = the Function of 1-tuples_on X, X;
take 1GateCircStr(p,f);
set A = 1GateCircuit(p,f);
A1: the Sorts of A = (the carrier of 1GateCircStr(p,f))-->X by CIRCCOMB:def 13;
then the_value_of the Sorts of A = X by FUNCOP_1:79;
hence thesis by A1;
end;
end;
theorem Th25:
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
proof
let n be Element of NAT, X be non empty finite set;
let f be Function of n-tuples_on X, X;
let p being FinSeqLen of n;
take A = 1GateCircuit(p,f);
the Sorts of A = (the carrier of 1GateCircStr(p,f))-->X by CIRCCOMB:def 13;
hence thesis by FUNCOP_1:79;
end;
registration
let X be non empty finite set;
cluster strict one-gate for Signature of X;
existence
proof
set p = the FinSeqLen of 1;
set f = the Function of 1-tuples_on X, X;
1GateCircStr(p,f) is Signature of X by Th25;
hence thesis;
end;
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; :: redefines 1GateCircStr (CIRCCOMB, definition)
coherence by Th25;
end;
definition
let X be non empty finite set;
let S be Signature of X;
mode Circuit of X,S -> Circuit of S means
:Def10:
it is gate`2=den & the
Sorts of it is constant & the_value_of the Sorts of it = X;
existence
proof
ex A being Circuit of S st the Sorts of A is constant & the_value_of
the Sorts of A = X & A is gate`2=den by Def9;
hence thesis;
end;
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;
coherence
proof
let A be Circuit of X,S;
thus A is gate`2=den by Def10;
the Sorts of A is non empty constant & the_value_of the Sorts of A = X
by Def10;
then dom the Sorts of A = the carrier of S &
for i being object st i in dom
the Sorts of A holds (the Sorts of A).i is non empty by FUNCT_1:def 12
,PARTFUN1:def 2;
then the Sorts of A is non-empty by PBOOLE:def 13;
hence thesis by MSUALG_1:def 3;
end;
end;
theorem Th26:
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)
proof
let n be Element of NAT, X be non empty finite set;
let f be Function of n-tuples_on X, X;
let p being FinSeqLen of n;
set A = 1GateCircuit(p,f);
thus A is gate`2=den;
the Sorts of A = (the carrier of 1GateCircStr(p,f))-->X by CIRCCOMB:def 13;
hence the Sorts of A is constant & the_value_of the Sorts of A = X by
FUNCOP_1:79;
end;
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;
existence
proof
consider A being Circuit of S such that
A1: the Sorts of A is constant & the_value_of the Sorts of A = X and
A2: A is gate`2=den by Def9;
set B=the MSAlgebra of A;
the Sorts of A is finite-yielding by MSAFREE2:def 11;
then reconsider B as Circuit of S by MSAFREE2:def 11;
for g being set st g in the carrier' of S holds g = [g`1, (the Charact
of B).g] by A2;
then B is gate`2=den;
then reconsider B as Circuit of X,S by A1,Def10;
consider Y being non empty finite set, n being Element of NAT, p being
FinSeqLen of n, f being Function of n-tuples_on Y,Y such that
A3: S = 1GateCircStr(p,f) by Def6;
take B;
A4: dom the Arity of S = the carrier' of S by FUNCT_2:def 1;
dom the Sorts of A = the carrier of S by PARTFUN1:def 2;
then
A5: the Sorts of B = (the carrier of S) --> X by A1,FUNCOP_1:80;
set g=[p,f];
set C = 1GateCircuit(p,f);
g in {g} by TARSKI:def 1;
then
A6: g in the carrier' of S by A3,CIRCCOMB:def 6;
then
A7: g = [g`1, (the Charact of C).g] by A3,CIRCCOMB:def 10;
(the Arity of S).g in (the carrier of S)* by A6,FUNCT_2:5;
then reconsider
Ag = (the Arity of S).g as FinSequence of the carrier of S by
FINSEQ_1:def 11;
dom (the ResultSort of S) = the carrier' of S by FUNCT_2:def 1;
then
A8: ((the Sorts of B)*the ResultSort of S).g = (the Sorts of B).((the
ResultSort of S).g) by A6,FUNCT_1:13;
(the ResultSort of S).g in the carrier of S by A6,FUNCT_2:5;
then (the ResultSort of S).g in dom the Sorts of B by PARTFUN1:def 2;
then
A9: (the Sorts of B).((the ResultSort of S).g) = X by A1,FUNCT_1:def 12;
A10: g = [g`1, (the Charact of B).g] by A6,CIRCCOMB:def 10;
then dom ((the Charact of B).g) = dom f by XTUPLE_0:1;
then
A11: dom ((the Charact of B).g) = n-tuples_on Y by FUNCT_2:def 1;
(the Charact of B).g is Function of (((the Sorts of B)# )*the Arity
of S).g, ((the Sorts of B)*the ResultSort of S).g by A6,PBOOLE:def 15;
then
dom ((the Charact of B).g) = (((the Sorts of B)# )*the Arity of S ).g
by A6,FUNCT_2:def 1;
then
A12: dom ((the Charact of B).g) = ((the Sorts of B)# ).Ag by A6,A4,FUNCT_1:13
.= (len Ag)-tuples_on X by A5,CIRCCOMB:2;
per cases;
suppose
A13: n <> 0;
A14: now
let i be object;
assume i in the carrier' of S;
then i in {g} by A3,CIRCCOMB:def 6;
then i = g by TARSKI:def 1;
hence (the Charact of B).i = (the Charact of C).i by A10,A7,XTUPLE_0:1;
end;
X = Y by A11,A12,A13,Th22;
then the Sorts of B = the Sorts of 1GateCircuit(p,f) by A3,A5,
CIRCCOMB:def 13;
hence thesis by A3,A14,PBOOLE:3;
end;
suppose
A15: n = 0;
then n-tuples_on X = {<*>X} by FINSEQ_2:94
.= {<*>Y}
.= n-tuples_on Y by A15,FINSEQ_2:94;
then
A16: dom f = n-tuples_on X by FUNCT_2:def 1;
(the Charact of B).g is Function of (((the Sorts of B)# )*the Arity
of S).g, ((the Sorts of B)*the ResultSort of S).g by A6,PBOOLE:def 15;
then
A17: rng ((the Charact of B).g) c= ((the Sorts of B)*the ResultSort of S
). g by RELAT_1:def 19;
(the Charact of B).g = f by A10,XTUPLE_0:1;
then reconsider h=f as Function of n-tuples_on X,X by A8,A9,A17,A16,
FUNCT_2:2;
set D = 1GateCircuit(p,h);
A18: g = [g`1, (the Charact of D).g] by A3,A6,CIRCCOMB:def 10;
A19: now
let i be object;
assume i in the carrier' of S;
then i in {g} by A3,CIRCCOMB:def 6;
then i = g by TARSKI:def 1;
hence (the Charact of B).i = (the Charact of D).i by A10,A18,XTUPLE_0:1
;
end;
the Sorts of B = the Sorts of D by A3,A5,CIRCCOMB:def 13;
hence thesis by A3,A19,PBOOLE:3;
end;
end;
end;
registration
let X be non empty finite set;
let S be Signature of X;
cluster strict for Circuit of X,S;
existence
proof
consider A being Circuit of S such that
A1: the Sorts of A is constant & the_value_of the Sorts of A = X and
A2: A is gate`2=den by Def9;
set B=the MSAlgebra of A;
the Sorts of A is finite-yielding by MSAFREE2:def 11;
then reconsider B as Circuit of S by MSAFREE2:def 11;
for g being set st g in the carrier' of S holds g = [g`1, (the Charact
of B).g] by A2;
then B is gate`2=den;
then reconsider B as Circuit of X,S by A1,Def10;
take B;
thus thesis;
end;
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); :: redefines 1GateCircuit (CIRCCOMB, definition)
coherence by Th26;
end;
theorem Th27:
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
proof
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;
thus S1 tolerates S2 by CIRCCOMB:47;
the Sorts of A2 is constant & the_value_of the Sorts of A2 = X by Def10;
then
A1: the Sorts of A2 = (dom the Sorts of A2)-->X by FUNCOP_1:80;
the Sorts of A1 is constant & the_value_of the Sorts of A1 = X by Def10;
then the Sorts of A1 = (dom the Sorts of A1)-->X by FUNCOP_1:80;
hence the Sorts of A1 tolerates the Sorts of A2 by A1,FUNCOP_1:87;
thus thesis by CIRCCOMB:48;
end;
theorem Th28:
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
proof
let X be non empty finite set;
let S1,S2 be Signature of X;
A1: the carrier of S1+*S2 = (the carrier of S1) \/ the carrier of S2 by
CIRCCOMB:def 2;
let A1 be Circuit of X,S1;
let A2 be Circuit of X,S2;
A2: dom the Sorts of A1 = the carrier of S1 & dom the Sorts of A2 = the
carrier of S2 by PARTFUN1:def 2;
A3: the Sorts of A1 is finite-yielding & the Sorts of A2 is finite-yielding
by MSAFREE2:def 11;
A1 tolerates A2 by Th27;
then
A4: the Sorts of A1 tolerates the Sorts of A2;
then
A5: the Sorts of A1+*A2 = (the Sorts of A1)+*the Sorts of A2 by CIRCCOMB:def 4;
A1+*A2 is finite-yielding
proof
let i be object;
assume i in the carrier of S1+*S2;
then i in the carrier of S1 or i in the carrier of S2 by A1,XBOOLE_0:def 3;
then
i in the carrier of S1 & (the Sorts of A1+*A2).i = (the Sorts of A1).
i or i in the carrier of S2 & (the Sorts of A1+*A2).i = (the Sorts of A2).i by
A4,A5,A2,FUNCT_4:13,15;
hence thesis by A3;
end;
hence thesis;
end;
theorem Th29:
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
proof
let X be non empty finite set;
let S1,S2 be Signature of X;
A1: the carrier' of S1+*S2 = (the carrier' of S1)\/ the carrier' of S2 by
CIRCCOMB:def 2;
let A1 be Circuit of X,S1;
let A2 be Circuit of X,S2;
A2: dom the Charact of A1 = the carrier' of S1 & dom the Charact of A2 = the
carrier' of S2 by PARTFUN1:def 2;
A3: A1 tolerates A2 by Th27;
then the Sorts of A1 tolerates the Sorts of A2;
then
A4: the Charact of A1+*A2 = (the Charact of A1)+*the Charact of A2 by
CIRCCOMB:def 4;
A5: the Charact of A1 tolerates the Charact of A2 by A3;
A1+*A2 is gate`2=den
proof
let i be set;
assume i in the carrier' of S1+*S2;
then i in the carrier' of S1 or i in the carrier' of S2 by A1,
XBOOLE_0:def 3;
then
i in the carrier' of S1 & (the Charact of A1+*A2).i = (the Charact of
A1).i or i in the carrier' of S2 & (the Charact of A1+*A2).i = (the Charact of
A2).i by A5,A4,A2,FUNCT_4:13,15;
hence thesis by CIRCCOMB:def 10;
end;
hence thesis;
end;
theorem Th30:
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
proof
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;
reconsider A = A1+*A2 as Circuit of S1+*S2 by Th28;
A1: dom the Sorts of A1 = the carrier of S1 by PARTFUN1:def 2;
the Sorts of A1 is constant & the_value_of the Sorts of A1 = X by Def10;
then the Sorts of A1 = (dom the Sorts of A1)-->X by FUNCOP_1:80;
then
A2: the Sorts of A1 = [:dom the Sorts of A1,{X}:] by FUNCOP_1:def 2;
the Sorts of A2 is constant & the_value_of the Sorts of A2 = X by Def10;
then the Sorts of A2 = (dom the Sorts of A2)-->X by FUNCOP_1:80;
then
A3: the Sorts of A2 = [:dom the Sorts of A2,{X}:] by FUNCOP_1:def 2;
A1 tolerates A2 by Th27;
then
A4: the Sorts of A1 tolerates the Sorts of A2;
then the Sorts of A = (the Sorts of A1)+*(the Sorts of A2) by CIRCCOMB:def 4
.= (the Sorts of A1)\/(the Sorts of A2) by A4,FUNCT_4:30
.= [:(dom the Sorts of A1) \/ dom the Sorts of A2, {X}:] by A2,A3,
ZFMISC_1:97
.= ((the carrier of S1) \/ dom the Sorts of A2) --> X by A1,FUNCOP_1:def 2;
hence thesis by FUNCOP_1:79;
end;
registration
let S1,S2 be finite non empty ManySortedSign;
cluster S1+*S2 -> finite;
coherence
proof
the carrier of S1+*S2 = (the carrier of S1) \/ the carrier of S2 by
CIRCCOMB:def 2;
hence thesis;
end;
end;
registration
let X be non empty finite set;
let S1,S2 be Signature of X;
cluster S1+*S2 -> gate`2=den;
coherence
proof
consider A2 be Circuit of S2 such that
A1: the Sorts of A2 is constant & the_value_of the Sorts of A2 = X &
A2 is gate`2=den by Def9;
reconsider A2 as Circuit of X,S2 by A1,Def10;
consider A1 be Circuit of S1 such that
A2: the Sorts of A1 is constant & the_value_of the Sorts of A1 = X &
A1 is gate`2=den by Def9;
reconsider A1 as Circuit of X,S1 by A2,Def10;
A1+*A2 is gate`2=den by Th29;
hence thesis;
end;
end;
definition
let X be non empty finite set;
let S1,S2 be Signature of X;
redefine func S1+*S2 -> strict Signature of X; :: redefines +* (CIRCCOMB, definition)
coherence
proof
consider A2 being Circuit of S2 such that
A1: the Sorts of A2 is constant & the_value_of the Sorts of A2 = X &
A2 is gate`2=den by Def9;
reconsider A2 as Circuit of X,S2 by A1,Def10;
consider A1 being Circuit of S1 such that
A2: the Sorts of A1 is constant & the_value_of the Sorts of A1 = X &
A1 is gate`2=den by Def9;
reconsider A1 as Circuit of X,S1 by A2,Def10;
reconsider A = A1+*A2 as Circuit of S1+*S2 by Th28;
S1+*S2 is Signature of X
proof
take A;
thus the Sorts of A is constant & the_value_of the Sorts of A = X by Th30
;
thus thesis by Th29;
end;
hence thesis;
end;
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; :: redefines +* (CIRCCOMB, definition)
coherence
proof
A1: the Sorts of A1+*A2 is constant & the_value_of the Sorts of A1+*A2 = X
by Th30;
A1+*A2 is gate`2=den & A1+*A2 is Circuit of S1+*S2 by Th28,Th29;
hence thesis by A1,Def10;
end;
end;
theorem Th31:
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]
proof
let x,y be object;
{x} in { { x,y }, { x } } by TARSKI:def 2;
then
A1: the_rank_of {x} in the_rank_of { { x,y }, { x } } by CLASSES1:68;
x in {x} by TARSKI:def 1;
then the_rank_of x in the_rank_of {x} by CLASSES1:68;
hence the_rank_of x in the_rank_of [x,y] by A1,ORDINAL1:10;
{x,y} in { { x,y }, { x } } by TARSKI:def 2;
then
A2: the_rank_of {x,y} in the_rank_of { { x,y }, { x } } by CLASSES1:68;
y in {x,y} by TARSKI:def 2;
then the_rank_of y in the_rank_of {x,y} by CLASSES1:68;
hence thesis by A2,ORDINAL1:10;
end;
theorem Th32:
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
proof
let S be gate`2=den finite non void non empty unsplit gate`1=arity
ManySortedSign;
defpred P[object,object] means
$1 = $2 or $1 in the carrier' of S & $2 in proj2 $1`1;
consider R being Relation such that
A1: for a,b being object holds [a,b] in R iff a in the carrier of S & b in
the carrier of S & P[a,b] from RELAT_1:sch 1;
let A be non-empty Circuit of S such that
A2: A is gate`2=den;
A3: R is co-well_founded
proof
defpred P[object,object] means
ex x being set st x = $1 & $2 = the_rank_of x;
let Y be set;
assume that
Y c= field R and
A4: Y <> {};
set y = the Element of Y;
A5: for x,y,z being object st P[x,y] & P[x,z] holds y = z;
consider B being set such that
A6: for x being object holds x in B iff ex y being object st y in Y & P[y,x]
from TARSKI:sch 1(A5);
the_rank_of y in B by A4,A6;
then inf B in B by ORDINAL2:17;
then consider y being object such that
A7: y in Y and
A8: P[y,inf B] by A6;
reconsider y as set by TARSKI:1;
take y;
thus y in Y by A7;
let b be object;
assume that
A9: b in Y and
A10: y <> b & [y,b] in R;
the_rank_of b in B by A6,A9;
then
A11: inf B c= the_rank_of b by ORDINAL2:14;
y in the carrier' of S by A1,A10;
then y = [y`1, (the Charact of A).y] by A2;
then
A12: the_rank_of y`1 in the_rank_of y by Th31;
b in proj2 y`1 by A1,A10;
then consider c being object such that
A13: [c,b] in y`1 by XTUPLE_0:def 13;
A14: the_rank_of b in the_rank_of [c,b] by Th31;
the_rank_of [c,b] in the_rank_of y`1 by A13,CLASSES1:68;
hence contradiction by A8,A14,A12,A11,ORDINAL1:10;
end;
defpred A[object,object] means
ex n being Element of NAT st $2 = n & for s being
State of A, m being Element of NAT st m >= n holds Following(s,m).$1 =
Following(s,n).$1;
defpred P[object] means
$1 in the carrier of S implies ex n being Element of
NAT st for s being State of A, m being Element of NAT st m >= n holds Following
(s,m).$1 = Following(s,n).$1;
A15: rng R c= the carrier of S
proof
let o be object;
assume o in rng R;
then ex q being object st [q,o] in R by XTUPLE_0:def 13;
hence thesis by A1;
end;
A16: the carrier of S c= field R
proof
let o be object;
assume o in the carrier of S;
then [o,o] in R by A1;
hence thesis by RELAT_1:15;
end;
dom R c= the carrier of S
proof
let o be object;
assume o in dom R;
then ex q being object st [o,q] in R by XTUPLE_0:def 12;
hence thesis by A1;
end;
then
A17: dom R \/ rng R c= (the carrier of S) \/ the carrier of S by A15,
XBOOLE_1:13;
then
A18: the carrier of S = field R by A16,XBOOLE_0:def 10;
A19: for a being object
st for b being object st [a,b] in R & a <> b holds P[b]
holds P[a]
proof
defpred P[object,object] means
ex n being Element of NAT st $2 = n & for s being
State of A, m being Element of NAT st m >= n holds Following(s,m).$1 =
Following(s,n).$1;
let a be object;
defpred S[object] means a <> $1 & [a,$1] in R;
consider RS being set such that
A20: for b being object holds b in RS iff b in field R & S[b] from
XBOOLE_0:sch 1;
A21: RS c= the carrier of S
by A18,A20;
assume
A22: for b being object st [a,b] in R & a <> b holds P[b];
A23: for b being object st b in RS ex z being object st P[b,z]
proof
let b be object;
assume
A24: b in RS;
then a <> b & [a,b] in R by A20;
then ex n being Element of NAT st for s being State of A, m being
Element of NAT st m >= n holds Following(s,m).b = Following(s,n).b by A22,A21
,A24;
hence thesis;
end;
consider f being Function such that
A25: dom f = RS and
A26: for x being object st x in RS holds P[x,f.x] from CLASSES1:sch 1(A23);
assume
A27: a in the carrier of S;
per cases;
suppose
A28: RS <> {};
rng f c= NAT
proof
let o be object;
assume o in rng f;
then consider l being object such that
A29: l in dom f and
A30: o = f.l by FUNCT_1:def 3;
ex n being Element of NAT st f.l = n & for s being State of A, m
being Element of NAT st m >= n holds Following(s,m).l = Following(s,n). l by
A25,A26,A29;
hence thesis by A30;
end;
then reconsider
C = rng f as finite non empty Subset of NAT by A21,A25,A28,FINSET_1:8
,RELAT_1:38,41;
set b = the Element of RS;
a <> b & [a,b] in R by A20,A28;
then reconsider a1=a as Gate of S by A1;
reconsider mC = max C as Element of NAT by ORDINAL1:def 12;
take n = mC + 1;
let s be State of A;
let m be Element of NAT;
assume m >= n;
then consider k being Nat such that
A31: m = n + k by NAT_1:10;
reconsider k as Element of NAT by ORDINAL1:def 12;
A32: for x being set st x in rng the_arity_of a1 holds Following(s,mC)
is_stable_at x
proof
let x be set;
assume
A33: x in rng the_arity_of a1;
a1 = [(the Arity of S).a1, a1`2] by CIRCCOMB:def 8;
then
A34: a1 = [the_arity_of a1, a1`2] by MSUALG_1:def 1;
then the_rank_of x in the_rank_of a1 by A33,CLASSES1:82;
then
A35: x <> a;
rng the_arity_of a1 c= the carrier of S & x in proj2 a`1 by A33,A34,
FINSEQ_1:def 4;
then
A36: [a1,x] in R by A1,A27,A33;
then x in field R by RELAT_1:15;
then
A37: x in RS by A20,A35,A36;
then consider l being Element of NAT such that
A38: f.x = l and
A39: for s being State of A, m being Element of NAT st m >= l
holds Following(s,m).x = Following(s,l).x by A26;
l in rng f by A25,A37,A38,FUNCT_1:3;
then
A40: max C >= l by XXREAL_2:def 8;
now
let k be Nat;
A41: mC + k in NAT by ORDINAL1:def 12;
A42: mC + k >= max C by NAT_1:11;
thus (Following(Following(s,mC),k)).x
= Following(s,mC+k).x by FACIRC_1:13
.= Following(s,l).x by A39,A40,A42,XXREAL_0:2,A41
.= Following(s,mC).x by A39,A40;
end;
hence thesis;
end;
the_result_sort_of a1 = (the ResultSort of S).a1 by MSUALG_1:def 2
.= a by CIRCCOMB:44;
then Following Following(s,mC) is_stable_at a by A32,FACIRC_1:19;
then Following(s,n) is_stable_at a by FACIRC_1:12;
then Following(Following(s,n),k).a = Following(s,n).a;
hence thesis by A31,FACIRC_1:13;
end;
suppose
A43: RS = {};
take n=1;
let s be State of A;
let m be Element of NAT;
assume m >= n;
then consider k being Nat such that
A44: m = n + k by NAT_1:10;
reconsider k as Element of NAT by ORDINAL1:def 12;
A45: now
assume a in InnerVertices S;
then a in rng id the carrier' of S by CIRCCOMB:def 7;
then reconsider a1=a as Gate of S;
for x being set st x in rng the_arity_of a1 holds s is_stable_at x
proof
let x be set;
assume
A46: x in rng the_arity_of a1;
a1 = [(the Arity of S).a1, a1`2] by CIRCCOMB:def 8;
then
A47: a1 = [the_arity_of a1, a1`2] by MSUALG_1:def 1;
then the_rank_of x in the_rank_of a1 by A46,CLASSES1:82;
then
A48: x <> a;
rng the_arity_of a1 c= the carrier of S & x in proj2 a`1 by A46,A47,
FINSEQ_1:def 4;
then
A49: [a1,x] in R by A1,A27,A46;
then x in field R by RELAT_1:15;
hence thesis by A20,A43,A48,A49;
end;
then
A50: Following s is_stable_at the_result_sort_of a1 by FACIRC_1:19;
the_result_sort_of a1 = (the ResultSort of S).a1 by MSUALG_1:def 2
.= a1 by CIRCCOMB:44;
then Following(s,n) is_stable_at a1 by A50,FACIRC_1:14;
then Following(Following(s,n),k).a = Following(s,n).a;
hence thesis by A44,FACIRC_1:13;
end;
A51: now
assume a in InputVertices S;
then
A52: s is_stable_at a by FACIRC_1:18;
hence Following(s,m).a = s.a
.= Following(s,n).a by A52;
end;
the carrier of S = InputVertices S \/ InnerVertices S by XBOOLE_1:45;
hence thesis by A27,A51,A45,XBOOLE_0:def 3;
end;
end;
A53: for a being object st a in field R holds P[a]
from REWRITE1:sch 2(A3,A19 );
A54: for a being object st a in field R ex b being object st A[a,b]
proof
let a be object;
assume a in field R;
then ex n being Element of NAT st for s being State of A, m being Element
of NAT st m >= n holds Following(s,m).a = Following(s,n).a by A17,A53;
hence thesis;
end;
consider f being Function such that
A55: dom f = field R and
A56: for x being object st x in field R holds A[x,f.x] from CLASSES1:sch 1
(A54);
rng f c= NAT
proof
let o be object;
assume o in rng f;
then consider l being object such that
A57: l in dom f and
A58: o = f.l by FUNCT_1:def 3;
ex n being Element of NAT st f.l = n & for s being State of A, m
being Element of NAT st m >= n holds Following(s,m).l = Following(s,n). l by
A55,A56,A57;
hence thesis by A58;
end;
then reconsider C = rng f as finite non empty Subset of NAT by A18,A55,
FINSET_1:8,RELAT_1:38,41;
reconsider N = max C as Element of NAT by ORDINAL1:def 12;
take N;
let s be State of A;
A59: now
let x be object;
assume
A60: x in the carrier of S;
then consider n being Element of NAT such that
A61: f.x = n and
A62: for s being State of A, m being Element of NAT st m >= n holds
Following(s,m).x = Following(s,n).x by A16,A56;
n in C by A16,A55,A60,A61,FUNCT_1:3;
then
A63: N >= n by XXREAL_2:def 8;
then
A64: N+1 >= n by NAT_1:13;
thus Following(s,N).x = Following(s,n).x by A62,A63
.= Following(s,N+1).x by A62,A64
.= (Following Following(s,N)).x by FACIRC_1:12;
end;
dom Following(s,N) = the carrier of S & dom Following Following(s,N) =
the carrier of S by CIRCUIT1:3;
hence Following(s,N) = Following Following(s,N) by A59,FUNCT_1:2;
end;
registration
let X be non empty finite set;
let S be finite Signature of X;
cluster -> with_stabilization-limit for Circuit of X,S;
coherence by Th32;
end;
scheme
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 proof
deffunc f(Element of 1-tuples_on X()) = F($1.1);
consider f being Function of 1-tuples_on X(), X() such that
A1: for a being Element of 1-tuples_on X() holds f.a = f(a) from FUNCT_2
:sch 4;
hereby
take f;
let x be Element of X();
reconsider a = <*x*> as Element of 1-tuples_on X() by FINSEQ_2:98;
thus f.<*x*> = F(a.1) by A1
.= F(x);
end;
let f1,f2 be Function of 1-tuples_on X(), X() such that
A2: for x being Element of X() holds f1.<*x*> = F(x) and
A3: for x being Element of X() holds f2.<*x*> = F(x);
now
let a be Element of 1-tuples_on X();
consider x being Element of X() such that
A4: a = <*x*> by FINSEQ_2:97;
thus f1.a = F(x) by A2,A4
.= f2.a by A3,A4;
end;
hence thesis by FUNCT_2:63;
end;
scheme
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 proof
deffunc f(Element of 2-tuples_on X()) = F($1.1,$1.2);
consider f being Function of 2-tuples_on X(), X() such that
A1: for a being Element of 2-tuples_on X() holds f.a = f(a) from FUNCT_2
:sch 4;
hereby
take f;
let x,y be Element of X();
reconsider a = <*x,y*> as Element of 2-tuples_on X() by FINSEQ_2:101;
thus f.<*x,y*> = F(a.1,a.2) by A1
.= F(x,a.2)
.= F(x,y);
end;
let f1,f2 be Function of 2-tuples_on X(), X() such that
A2: for x,y being Element of X() holds f1.<*x,y*> = F(x,y) and
A3: for x,y being Element of X() holds f2.<*x,y*> = F(x,y);
now
let a be Element of 2-tuples_on X();
consider x,y being Element of X() such that
A4: a = <*x,y*> by FINSEQ_2:100;
thus f1.a = F(x,y) by A2,A4
.= f2.a by A3,A4;
end;
hence thesis by FUNCT_2:63;
end;
scheme
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 proof
deffunc f(Element of 3-tuples_on X()) = F($1.1,$1.2,$1.3);
consider f being Function of 3-tuples_on X(), X() such that
A1: for a being Element of 3-tuples_on X() holds f.a = f(a) from FUNCT_2
:sch 4;
hereby
take f;
let x,y,z be Element of X();
reconsider a = <*x,y,z*> as Element of 3-tuples_on X() by FINSEQ_2:104;
thus f.<*x,y,z*> = F(a.1,a.2,a.3) by A1
.= F(x,a.2,a.3)
.= F(x,y,a.3)
.= F(x,y,z);
end;
let f1,f2 be Function of 3-tuples_on X(), X() such that
A2: for x,y,z being Element of X() holds f1.<*x,y,z*> = F(x,y,z) and
A3: for x,y,z being Element of X() holds f2.<*x,y,z*> = F(x,y,z);
now
let a be Element of 3-tuples_on X();
consider x,y,z being Element of X() such that
A4: a = <*x,y,z*> by FINSEQ_2:103;
thus f1.a = F(x,y,z) by A2,A4
.= f2.a by A3,A4;
end;
hence thesis by FUNCT_2:63;
end;
theorem Th33:
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*>
proof
let f be Function;
let x1,x2,x3,x4 be set;
assume that
A1: x1 in dom f and
A2: x2 in dom f & x3 in dom f & x4 in dom f;
reconsider D = dom f, E = rng f as non empty set by A1,FUNCT_1:3;
rng <*x1,x2,x3,x4*> c= D
proof
let a be object;
assume a in rng <*x1,x2,x3,x4*>;
then a in {x1,x2,x3,x4} by Th13;
hence thesis by A1,A2,ENUMSET1:def 2;
end;
then reconsider p=<*x1,x2,x3,x4*> as FinSequence of D by FINSEQ_1:def 4;
reconsider g = f as Function of D,E by FUNCT_2:def 1,RELSET_1:4;
A3: dom(g*p) = dom p by FINSEQ_3:120;
A4: now
let k be Nat;
assume
A5: k in dom (g*p);
then
A6: k in Seg 4 by A3,FINSEQ_1:89;
per cases by A6,ENUMSET1:def 2,FINSEQ_3:2;
suppose
A7: k=1;
then p.k=x1;
then (g*p).k = g.x1 by A5,FINSEQ_3:120;
hence (g*p).k = <*f.x1,f.x2,f.x3,f.x4*>.k by A7;
end;
suppose
A8: k=2;
then p.k=x2;
then (g*p).k = g.x2 by A5,FINSEQ_3:120;
hence (g*p).k = <*f.x1,f.x2,f.x3,f.x4*>.k by A8;
end;
suppose
A9: k=3;
then p.k=x3;
then (g*p).k = g.x3 by A5,FINSEQ_3:120;
hence (g*p).k = <*f.x1,f.x2,f.x3,f.x4*>.k by A9;
end;
suppose
A10: k=4;
then p.k=x4;
then (g*p).k = g.x4 by A5,FINSEQ_3:120;
hence (g*p).k = <*f.x1,f.x2,f.x3,f.x4*>.k by A10;
end;
end;
dom (g*p) = Seg 4 by A3,FINSEQ_1:89
.= dom <*f.x1,f.x2,f.x3,f.x4*> by FINSEQ_1:89;
hence thesis by A4,FINSEQ_1:13;
end;
theorem Th34:
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*>
proof
let f be Function;
let x1,x2,x3,x4,x5 be set;
assume that
A1: x1 in dom f and
A2: x2 in dom f & x3 in dom f & x4 in dom f & x5 in dom f;
reconsider D = dom f, E = rng f as non empty set by A1,FUNCT_1:3;
rng <*x1,x2,x3,x4,x5*> c= D
proof
let a be object;
assume a in rng <*x1,x2,x3,x4,x5*>;
then a in {x1,x2,x3,x4,x5} by Th14;
hence thesis by A1,A2,ENUMSET1:def 3;
end;
then reconsider p=<*x1,x2,x3,x4,x5*> as FinSequence of D by FINSEQ_1:def 4;
reconsider g = f as Function of D,E by FUNCT_2:def 1,RELSET_1:4;
A3: dom(g*p) = dom p by FINSEQ_3:120;
A4: now
let k be Nat;
assume
A5: k in dom (g*p);
then
A6: k in Seg 5 by A3,FINSEQ_1:89;
per cases by A6,ENUMSET1:def 3,FINSEQ_3:3;
suppose
A7: k=1;
then p.k=x1;
then (g*p).k = g.x1 by A5,FINSEQ_3:120;
hence (g*p).k = <*f.x1,f.x2,f.x3,f.x4,f.x5*>.k by A7;
end;
suppose
A8: k=2;
then p.k=x2;
then (g*p).k = g.x2 by A5,FINSEQ_3:120;
hence (g*p).k = <*f.x1,f.x2,f.x3,f.x4,f.x5*>.k by A8;
end;
suppose
A9: k=3;
then p.k=x3;
then (g*p).k = g.x3 by A5,FINSEQ_3:120;
hence (g*p).k = <*f.x1,f.x2,f.x3,f.x4,f.x5*>.k by A9;
end;
suppose
A10: k=4;
then p.k=x4;
then (g*p).k = g.x4 by A5,FINSEQ_3:120;
hence (g*p).k = <*f.x1,f.x2,f.x3,f.x4,f.x5*>.k by A10;
end;
suppose
A11: k=5;
then p.k=x5;
then (g*p).k = g.x5 by A5,FINSEQ_3:120;
hence (g*p).k = <*f.x1,f.x2,f.x3,f.x4,f.x5*>.k by A11;
end;
end;
dom (g*p) = Seg 5 by A3,FINSEQ_1:89
.= dom <*f.x1,f.x2,f.x3,f.x4,f.x5*> by FINSEQ_1:89;
hence thesis by A4,FINSEQ_1:13;
end;
scheme
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
A1: 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)
proof
set S = 1GateCircStr(<*x1()*>,f());
let s be State of 1GateCircuit(<*x1()*>,f());
dom s = the carrier of S by CIRCUIT1:3
.= (rng <*x1()*>) \/ {[<*x1()*>,f()]} by CIRCCOMB:def 6
.= {x1()} \/ {[<*x1()*>,f()]} by FINSEQ_1:38
.= {x1(),[<*x1()*>,f()]} by ENUMSET1:1;
then
A2: x1() in dom s by TARSKI:def 2;
let a1 be Element of B();
assume a1 = s.x1();
then
A3: s*<*x1()*> = <*a1*> by A2,FINSEQ_2:34;
thus (Result s).Output S = (Following s).(Output S) by Th20
.= (Following s).[<*x1()*>,f()] by Th15
.= f().(s*<*x1()*>) by CIRCCOMB:56
.= F(a1) by A1,A3;
end;
scheme
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
A1: 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)
proof
set S = 1GateCircStr(<*x1(),x2()*>,f());
let s be State of 1GateCircuit(<*x1(),x2()*>,f());
dom s = the carrier of S by CIRCUIT1:3
.= (rng <*x1(),x2()*>) \/ {[<*x1(),x2()*>,f()]} by CIRCCOMB:def 6
.= {x1(),x2()} \/ {[<*x1(),x2()*>,f()]} by FINSEQ_2:127
.= {x1(),x2(),[<*x1(),x2()*>,f()]} by ENUMSET1:3;
then
A2: x1() in dom s & x2() in dom s by ENUMSET1:def 1;
let a1,a2 be Element of B();
assume a1 = s.x1() & a2 = s.x2();
then
A3: s*<*x1(),x2()*> = <*a1,a2*> by A2,FINSEQ_2:125;
thus (Result s).Output S = (Following s).(Output S) by Th20
.= (Following s).[<*x1(),x2()*>,f()] by Th15
.= f().(s*<*x1(),x2()*>) by CIRCCOMB:56
.= F(a1,a2) by A1,A3;
end;
scheme
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
A1: 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)
proof
set S = 1GateCircStr(<*x1(),x2(),x3()*>,f());
let s be State of 1GateCircuit(<*x1(),x2(),x3()*>,f());
A2: dom s = the carrier of S by CIRCUIT1:3
.= (rng <*x1(),x2(),x3()*>) \/ {[<*x1(),x2(),x3()*>,f()]} by CIRCCOMB:def 6
.= {x1(),x2(),x3()} \/ {[<*x1(),x2(),x3()*>,f()]} by FINSEQ_2:128
.= {x1(),x2(),x3(),[<*x1(),x2(),x3()*>,f()]} by ENUMSET1:6;
then
A3: x1() in dom s & x2() in dom s by ENUMSET1:def 2;
A4: x3() in dom s by A2,ENUMSET1:def 2;
let a1,a2,a3 be Element of B();
assume a1 = s.x1() & a2 = s.x2() & a3 = s.x3();
then
A5: s*<*x1(),x2(),x3()*> = <*a1,a2,a3*> by A3,A4,FINSEQ_2:126;
thus (Result s).Output S = (Following s).(Output S) by Th20
.= (Following s).[<*x1(),x2(),x3()*>,f()] by Th15
.= f().(s*<*x1(),x2(),x3()*>) by CIRCCOMB:56
.= F(a1,a2,a3) by A1,A5;
end;
scheme
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
A1: 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)
proof
set S = 1GateCircStr(<*x1(),x2(),x3(),x4()*>,f());
let s be State of 1GateCircuit(<*x1(),x2(),x3(),x4()*>,f());
A2: dom s = the carrier of S by CIRCUIT1:3
.= (rng <*x1(),x2(),x3(),x4()*>) \/ {[<*x1(),x2(),x3(),x4()*>,f()]} by
CIRCCOMB:def 6
.= {x1(),x2(),x3(),x4()} \/ {[<*x1(),x2(),x3(),x4()*>,f()]} by Th13
.= {[<*x1(),x2(),x3(),x4()*>,f()],x1(),x2(),x3(),x4()} by ENUMSET1:7;
then
A3: x1() in dom s & x2() in dom s by ENUMSET1:def 3;
A4: x3() in dom s & x4() in dom s by A2,ENUMSET1:def 3;
let a1,a2,a3,a4 be Element of B();
assume a1 = s.x1() & a2 = s.x2() & a3 = s.x3() & a4 = s.x4();
then
A5: s*<*x1(),x2(),x3(),x4()*> = <*a1,a2,a3,a4*> by A3,A4,Th33;
thus (Result s).Output S = (Following s).(Output S) by Th20
.= (Following s).[<*x1(),x2(),x3(),x4()*>,f()] by Th15
.= f().(s*<*x1(),x2(),x3(),x4()*>) by CIRCCOMB:56
.= F(a1,a2,a3,a4) by A1,A5;
end;
scheme
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
A1: 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)
proof
set S = 1GateCircStr(<*x1(),x2(),x3(),x4(),x5()*>,f());
let s be State of 1GateCircuit(<*x1(),x2(),x3(),x4(),x5()*>,f());
A2: dom s = the carrier of S by CIRCUIT1:3
.= (rng <*x1(),x2(),x3(),x4(),x5()*>) \/ {[<*x1(),x2(),x3(),x4(),x5()*>,
f()]} by CIRCCOMB:def 6
.= {x1(),x2(),x3(),x4(),x5()} \/ {[<*x1(),x2(),x3(),x4(),x5()*>,f()]} by
Th14
.= {x1(),x2(),x3(),x4(),x5(),[<*x1(),x2(),x3(),x4(),x5()*>,f()]} by
ENUMSET1:15;
then
A3: x1() in dom s & x2() in dom s by ENUMSET1:def 4;
A4: x5() in dom s by A2,ENUMSET1:def 4;
A5: x3() in dom s & x4() in dom s by A2,ENUMSET1:def 4;
let a1,a2,a3,a4,a5 be Element of B();
assume a1 = s.x1() & a2 = s.x2() & a3 = s.x3() & a4 = s.x4() & a5 = s.x5();
then
A6: s*<*x1(),x2(),x3(),x4(),x5()*> = <*a1,a2,a3,a4,a5*> by A3,A5,A4,Th34;
thus (Result s).Output S = (Following s).(Output S) by Th20
.= (Following s).[<*x1(),x2(),x3(),x4(),x5()*>,f()] by Th15
.= f().(s*<*x1(),x2(),x3(),x4(),x5()*>) by CIRCCOMB:56
.= F(a1,a2,a3,a4,a5) by A1,A6;
end;
begin :: Input of a compound circuit
theorem Th35:
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
proof
let n be Element of NAT, X be non empty finite set;
let f be Function of n-tuples_on X, X;
let p be FinSeqLen of n;
let S be Signature of X such that
A1: rng p c= the carrier of S and
A2: not Output 1GateCircStr(p,f) in InputVertices S;
A3: the carrier of S = (InputVertices S) \/ InnerVertices S by XBOOLE_1:45;
thus InputVertices (S +* 1GateCircStr(p,f)) = ((InputVertices S)\(
InnerVertices 1GateCircStr(p,f))) \/ ((InputVertices 1GateCircStr(p,f))\(
InnerVertices S)) by CIRCCMB2:5,CIRCCOMB:47
.= ((InputVertices S)\(InnerVertices 1GateCircStr(p,f))) \/ ((rng p)\(
InnerVertices S)) by CIRCCOMB:42
.= ((InputVertices S) \ {Output 1GateCircStr(p,f)}) \/ ((rng p)\(
InnerVertices S)) by Th16
.= (InputVertices S) \/ ((rng p)\(InnerVertices S)) by A2,ZFMISC_1:57
.= InputVertices S by A1,A3,XBOOLE_1:12,43;
end;
theorem Th36:
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
proof
let x1,x2 be set, X be non empty finite set, n be Element of NAT;
let f be Function of n-tuples_on X, X;
let p be FinSeqLen of n;
let S be Signature of X such that
A1: rng p = x1 \/ x2 and
A2: x1 c= the carrier of S and
A3: x2 misses InnerVertices S and
A4: not Output 1GateCircStr(p,f) in InputVertices S;
A5: the carrier of S = (InputVertices S) \/ InnerVertices S by XBOOLE_1:45;
thus InputVertices (S +* 1GateCircStr(p,f)) = ((InputVertices S)\(
InnerVertices 1GateCircStr(p,f))) \/ ((InputVertices 1GateCircStr(p,f))\(
InnerVertices S)) by CIRCCMB2:5,CIRCCOMB:47
.= ((InputVertices S)\(InnerVertices 1GateCircStr(p,f))) \/ ((rng p)\(
InnerVertices S)) by CIRCCOMB:42
.= ((InputVertices S)\(InnerVertices 1GateCircStr(p,f))) \/ ((x1\(
InnerVertices S)) \/ x2) by A1,A3,XBOOLE_1:87
.= ((InputVertices S)\(InnerVertices 1GateCircStr(p,f))) \/ (x1\(
InnerVertices S)) \/ x2 by XBOOLE_1:4
.= ((InputVertices S) \ {Output 1GateCircStr(p,f)}) \/ (x1\(
InnerVertices S)) \/ x2 by Th16
.= (InputVertices S) \/ (x1\(InnerVertices S)) \/ x2 by A4,ZFMISC_1:57
.= (InputVertices S) \/ x2 by A2,A5,XBOOLE_1:12,43;
end;
theorem Th37:
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
proof
let x1 be set, X be non empty finite set;
set p = <*x1*>;
let f be Function of 1-tuples_on X, X;
let S be Signature of X;
assume x1 in the carrier of S;
then {x1} c= the carrier of S by ZFMISC_1:31;
then rng p c= the carrier of S by FINSEQ_1:38;
hence thesis by Th35;
end;
theorem Th38:
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}
proof
let x1,x2 be set, X be non empty finite set;
set p = <*x1,x2*>;
let f be Function of 2-tuples_on X, X;
let S be Signature of X such that
A1: x1 in the carrier of S and
A2: not x2 in InnerVertices S;
A3: rng p = {x1,x2} by FINSEQ_2:127
.= {x1} \/ {x2} by ENUMSET1:1;
{x1} c= the carrier of S by A1,ZFMISC_1:31;
hence thesis by A2,A3,Th36,ZFMISC_1:50;
end;
theorem Th39:
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}
proof
let x1,x2 be set, X be non empty finite set;
set p = <*x1,x2*>;
let f be Function of 2-tuples_on X, X;
let S be Signature of X such that
A1: x2 in the carrier of S and
A2: not x1 in InnerVertices S;
A3: rng p = {x1,x2} by FINSEQ_2:127
.= {x1} \/ {x2} by ENUMSET1:1;
{x2} c= the carrier of S by A1,ZFMISC_1:31;
hence thesis by A2,A3,Th36,ZFMISC_1:50;
end;
theorem Th40:
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
proof
let x1,x2 be set, X be non empty finite set;
let f be Function of 2-tuples_on X, X;
A1: rng <*x1,x2*> = {x1,x2} by FINSEQ_2:127;
let S be Signature of X;
assume x1 in the carrier of S & x2 in the carrier of S;
then rng <*x1,x2*> c= the carrier of S by A1,ZFMISC_1:32;
hence thesis by Th35;
end;
theorem Th41:
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}
proof
let x1,x2,x3 be set, X be non empty finite set;
set p = <*x1,x2,x3*>;
let f be Function of 3-tuples_on X, X;
let S be Signature of X such that
A1: x1 in the carrier of S and
A2: ( not x2 in InnerVertices S)& not x3 in InnerVertices S;
A3: rng p = {x1,x2,x3} by FINSEQ_2:128
.= {x1} \/ {x2,x3} by ENUMSET1:2;
{x1} c= the carrier of S by A1,ZFMISC_1:31;
hence thesis by A2,A3,Th36,ZFMISC_1:51;
end;
theorem Th42:
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}
proof
let x1,x2,x3 be set, X be non empty finite set;
set p = <*x1,x2,x3*>;
let f be Function of 3-tuples_on X, X;
let S be Signature of X such that
A1: x2 in the carrier of S and
A2: ( not x1 in InnerVertices S)& not x3 in InnerVertices S;
A3: rng p = {x1,x2,x3} by FINSEQ_2:128
.= {x2,x1,x3} by ENUMSET1:58
.= {x2} \/ {x1,x3} by ENUMSET1:2;
{x2} c= the carrier of S by A1,ZFMISC_1:31;
hence thesis by A2,A3,Th36,ZFMISC_1:51;
end;
theorem Th43:
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}
proof
let x1,x2,x3 be set, X be non empty finite set;
set p = <*x1,x2,x3*>;
let f be Function of 3-tuples_on X, X;
let S be Signature of X such that
A1: x3 in the carrier of S and
A2: ( not x1 in InnerVertices S)& not x2 in InnerVertices S;
A3: rng p = {x1,x2,x3} by FINSEQ_2:128
.= {x1,x2} \/ {x3} by ENUMSET1:3;
{x3} c= the carrier of S by A1,ZFMISC_1:31;
hence thesis by A2,A3,Th36,ZFMISC_1:51;
end;
theorem Th44:
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}
proof
let x1,x2,x3 be set, X be non empty finite set;
set p = <*x1,x2,x3*>;
let f be Function of 3-tuples_on X, X;
let S be Signature of X such that
A1: x1 in the carrier of S & x2 in the carrier of S and
A2: not x3 in InnerVertices S;
A3: rng p = {x1,x2,x3} by FINSEQ_2:128
.= {x1,x2} \/ {x3} by ENUMSET1:3;
{x1,x2} c= the carrier of S by A1,ZFMISC_1:32;
hence thesis by A2,A3,Th36,ZFMISC_1:50;
end;
theorem Th45:
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}
proof
let x1,x2,x3 be set, X be non empty finite set;
set p = <*x1,x2,x3*>;
let f be Function of 3-tuples_on X, X;
let S be Signature of X such that
A1: x1 in the carrier of S & x3 in the carrier of S and
A2: not x2 in InnerVertices S;
A3: rng p = {x1,x2,x3} by FINSEQ_2:128
.= {x2,x1,x3} by ENUMSET1:58
.= {x2} \/ {x1,x3} by ENUMSET1:2;
{x1,x3} c= the carrier of S by A1,ZFMISC_1:32;
hence thesis by A2,A3,Th36,ZFMISC_1:50;
end;
theorem Th46:
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}
proof
let x1,x2,x3 be set, X be non empty finite set;
set p = <*x1,x2,x3*>;
let f be Function of 3-tuples_on X, X;
let S be Signature of X such that
A1: x2 in the carrier of S & x3 in the carrier of S and
A2: not x1 in InnerVertices S;
A3: rng p = {x1,x2,x3} by FINSEQ_2:128
.= {x1} \/ {x2,x3} by ENUMSET1:2;
{x2,x3} c= the carrier of S by A1,ZFMISC_1:32;
hence thesis by A2,A3,Th36,ZFMISC_1:50;
end;
theorem Th47:
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
proof
let x1,x2,x3 be set, X be non empty finite set;
let f be Function of 3-tuples_on X, X;
let S be Signature of X;
assume x1 in the carrier of S & x2 in the carrier of S & x3 in the carrier
of S; then
A1: {x1,x2} c= the carrier of S & {x3} c= the carrier of S by ZFMISC_1:31,32;
rng <*x1,x2,x3*> = {x1,x2,x3} by FINSEQ_2:128
.= {x1,x2} \/ {x3} by ENUMSET1:3;
hence thesis by A1,Th35,XBOOLE_1:8;
end;
begin :: Result of a compound circuit
theorem Th48:
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
proof
let X be non empty finite set;
let S be finite Signature of X;
let A be Circuit of X,S;
let n be Element of NAT, f be Function of n-tuples_on X, X;
let p be FinSeqLen of n such that
A1: not Output 1GateCircStr(p,f) in InputVertices S;
InnerVertices 1GateCircStr(p,f) = {Output 1GateCircStr(p,f)} by Th16;
then
A2: InputVertices S misses InnerVertices 1GateCircStr(p,f) by A1,ZFMISC_1:50;
let s be State of A +* 1GateCircuit(p,f);
let s9 be State of A such that
A3: s9 = s|the carrier of S;
A tolerates 1GateCircuit(p,f) by Th27;
then the Sorts of A tolerates the Sorts of 1GateCircuit(p,f);
then reconsider s1 = Following(s, stabilization-time s9)|the carrier of
1GateCircStr(p,f) as State of 1GateCircuit(p,f) by CIRCCOMB:26;
A4: stabilization-time s1 <= 1 by Th21;
s9 is stabilizing & s1 is stabilizing by Def2;
then
stabilization-time s = (stabilization-time s9)+stabilization-time s1 by A3,A2
,Th10,Th27;
hence thesis by A4,XREAL_1:6;
end;
scheme
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
A1: 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
A2: not Output 1GateCircStr(<*x1()*>,f()) in InputVertices S()
proof
set S = 1GateCircStr(<*x1()*>,f());
let s be State of C() +* 1GateCircuit(<*x1()*>,f());
let s9 be State of C() such that
A3: s9 = s|the carrier of S();
rng <*x1()*> = {x1()} by FINSEQ_1:38;
then
A4: InputVertices S = rng <*x1()*> & x1() in rng <*x1()*> by CIRCCOMB:42
,TARSKI:def 1; then
A5: x1() in InnerVertices S() or x1() in InputVertices S \ InnerVertices S
() by XBOOLE_0:def 5;
A6: s9 is stabilizing by Def2;
InnerVertices S = {Output S} by Th16;
then
A7: InputVertices S() misses InnerVertices S by A2,ZFMISC_1:50;
then
A8: Following(s, stabilization-time s9)|the carrier of S() = Following(s9,
stabilization-time s9) by A3,Th27,CIRCCMB2:13
.= Result s9 by A6,Th2;
S() tolerates S by CIRCCOMB:47;
then InputVertices (S()+*S) = (InputVertices S()) \/ (InputVertices S \
InnerVertices S()) by A7,FACIRC_1:4;
then
A9: x1() in InnerVertices S() or x1() in InputVertices (S()+*S) by A5,
XBOOLE_0:def 3;
let a1 be Element of B();
assume ( x1() in InnerVertices S() implies a1 = (Result s9).x1())&( not x1(
) in InnerVertices S() implies a1 = s.x1());
then
A10: a1 = Following(s, stabilization-time s9).x1() by A9,A8,Th1,FUNCT_1:49;
A11: s is stabilizing by Def2;
the carrier' of S = {[<*x1()*>,f()]} by CIRCCOMB:def 6;
then [<*x1()*>,f()] in {[<*x1()*>,f()]} & the carrier' of S()+*S = (the
carrier' of S())\/{[<*x1()*>,f()]} by CIRCCOMB:def 2,TARSKI:def 1;
then reconsider g = [<*x1()*>,f()] as Gate of S()+*S by XBOOLE_0:def 3;
A12: the_result_sort_of g = (the ResultSort of S()+*S).g by MSUALG_1:def 2
.= g by CIRCCOMB:44;
A13: g`2 = f();
the carrier of S()+*S = (the carrier of S()) \/ the carrier of S by
CIRCCOMB:def 2;
then
A14: x1() in the carrier of S()+*S by A4,XBOOLE_0:def 3;
A15: [<*x1()*>,f()] = Output S by Th15;
g = [(the Arity of S()+*S).g, g`2] by CIRCCOMB:def 8;
then
A16: <*x1()*> =(the Arity of S()+*S).g by XTUPLE_0:1
.= the_arity_of g by MSUALG_1:def 1;
dom Following(s, stabilization-time s9) = the carrier of S()+*S by CIRCUIT1:3
;
then
A17: Following(s, stabilization-time s9)*<*x1()*> = <*a1*> by A14,A10,
FINSEQ_2:34;
stabilization-time s <= 1+stabilization-time s9 by A2,A3,Th48;
hence (Result s).Output S = (Following(s, 1+stabilization-time s9)).Output S
by A11,Th5
.= (Following Following(s, stabilization-time s9)).g by A15,FACIRC_1:12
.= f().(Following(s, stabilization-time s9)*<*x1()*>) by A12,A16,A13,
FACIRC_1:34
.= F(a1) by A1,A17;
end;
scheme
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
A1: 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
A2: not Output 1GateCircStr(<*x1(),x2()*>,f()) in InputVertices S()
proof
set S = 1GateCircStr(<*x1(),x2()*>,f());
let s be State of C() +* 1GateCircuit(<*x1(),x2()*>,f());
let s9 be State of C() such that
A3: s9 = s|the carrier of S();
A4: s9 is stabilizing by Def2;
InnerVertices S = {Output S} by Th16;
then
A5: InputVertices S() misses InnerVertices S by A2,ZFMISC_1:50;
then
A6: Following(s, stabilization-time s9)|the carrier of S() = Following(s9,
stabilization-time s9) by A3,Th27,CIRCCMB2:13
.= Result s9 by A4,Th2;
the carrier' of S = {[<*x1(),x2()*>,f()]} by CIRCCOMB:def 6;
then
[<*x1(),x2()*>,f()] in {[<*x1(),x2()*>,f()]} & the carrier' of S()+*S =
(the carrier' of S())\/{[<*x1(),x2()*>,f()]} by CIRCCOMB:def 2,TARSKI:def 1;
then reconsider g = [<*x1(),x2()*>,f()] as Gate of S()+*S by XBOOLE_0:def 3;
let a1, a2 be Element of B() such that
A7: ( x1() in InnerVertices S() implies a1 = (Result s9).x1())&( not x1(
) in InnerVertices S() implies a1 = s.x1()) and
A8: ( x2() in InnerVertices S() implies a2 = (Result s9).x2())&( not x2(
) in InnerVertices S() implies a2 = s.x2());
A9: InputVertices S = rng <*x1(),x2()*> by CIRCCOMB:42;
S() tolerates S by CIRCCOMB:47;
then
A10: InputVertices (S()+*S) = (InputVertices S()) \/ (InputVertices S \
InnerVertices S()) by A5,FACIRC_1:4;
A11: rng <*x1(),x2()*> = {x1(),x2()} by FINSEQ_2:127;
then
A12: x2() in rng <*x1(),x2()*> by TARSKI:def 2;
then x2() in InnerVertices S() or x2() in InputVertices S \ InnerVertices S
() by A9,XBOOLE_0:def 5;
then x2() in InnerVertices S() or x2() in InputVertices (S()+*S) by A10,
XBOOLE_0:def 3;
then
A13: a2 = Following(s, stabilization-time s9).x2() by A8,A6,Th1,FUNCT_1:49;
A14: x1() in rng <*x1(),x2()*> by A11,TARSKI:def 2;
then x1() in InnerVertices S() or x1() in InputVertices S \ InnerVertices S
() by A9,XBOOLE_0:def 5;
then x1() in InnerVertices S() or x1() in InputVertices (S()+*S) by A10,
XBOOLE_0:def 3;
then
A15: a1 = Following(s, stabilization-time s9).x1() by A7,A6,Th1,FUNCT_1:49;
g = [(the Arity of S()+*S).g, g`2] by CIRCCOMB:def 8;
then
A16: <*x1(),x2()*> =(the Arity of S()+*S).g by XTUPLE_0:1
.= the_arity_of g by MSUALG_1:def 1;
A17: g`2 = f();
A18: the carrier of S()+*S = (the carrier of S()) \/ the carrier of S by
CIRCCOMB:def 2; then
A19: x2() in the carrier of S()+*S by A9,A12,XBOOLE_0:def 3;
A20: [<*x1(),x2()*>,f()] = Output S by Th15;
A21: s is stabilizing by Def2;
A22: dom Following(s, stabilization-time s9) = the carrier of S()+*S by
CIRCUIT1:3;
x1() in the carrier of S()+*S by A9,A14,A18,XBOOLE_0:def 3;
then
A23: Following(s, stabilization-time s9)*<*x1(),x2()*> = <*a1,a2*> by A19,A15
,A13,A22,FINSEQ_2:125;
A24: the_result_sort_of g = (the ResultSort of S()+*S).g by MSUALG_1:def 2
.= g by CIRCCOMB:44;
stabilization-time s <= 1+stabilization-time s9 by A2,A3,Th48;
hence (Result s).Output S = (Following(s, 1+stabilization-time s9)).Output S
by A21,Th5
.= (Following Following(s, stabilization-time s9)).g by A20,FACIRC_1:12
.= f().(Following(s, stabilization-time s9)*<*x1(),x2()*>) by A24,A16,A17,
FACIRC_1:34
.= F(a1,a2) by A1,A23;
end;
scheme
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
A1: 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
A2: not Output 1GateCircStr(<*x1(),x2(),x3()*>,f()) in InputVertices S()
proof
set S = 1GateCircStr(<*x1(),x2(),x3()*>,f());
let s be State of C() +* 1GateCircuit(<*x1(),x2(),x3()*>,f());
let s9 be State of C() such that
A3: s9 = s|the carrier of S();
A4: s9 is stabilizing by Def2;
InnerVertices S = {Output S} by Th16;
then
A5: InputVertices S() misses InnerVertices S by A2,ZFMISC_1:50;
then
A6: Following(s, stabilization-time s9)|the carrier of S() = Following(s9,
stabilization-time s9) by A3,Th27,CIRCCMB2:13
.= Result s9 by A4,Th2;
S() tolerates S by CIRCCOMB:47;
then
A7: InputVertices (S()+*S) = (InputVertices S()) \/ (InputVertices S \
InnerVertices S()) by A5,FACIRC_1:4;
the carrier' of S = {[<*x1(),x2(),x3()*>,f()]} by CIRCCOMB:def 6;
then [<*x1(),x2(),x3()*>,f()] in {[<*x1(),x2(),x3()*>,f()]} & the carrier'
of S() +*S = (the carrier' of S())\/{[<*x1(),x2(),x3()*>,f()]} by
CIRCCOMB:def 2,TARSKI:def 1;
then reconsider g = [<*x1(),x2(),x3()*>,f()] as Gate of S()+*S by
XBOOLE_0:def 3;
let a1, a2, a3 be Element of B() such that
A8: ( x1() in InnerVertices S() implies a1 = (Result s9).x1())&( not x1(
) in InnerVertices S() implies a1 = s.x1()) and
A9: ( x2() in InnerVertices S() implies a2 = (Result s9).x2())&( not x2(
) in InnerVertices S() implies a2 = s.x2()) and
A10: ( x3() in InnerVertices S() implies a3 = (Result s9).x3())&( not x3(
) in InnerVertices S() implies a3 = s.x3());
A11: InputVertices S = rng <*x1(),x2(),x3()*> by CIRCCOMB:42;
g = [(the Arity of S()+*S).g, g`2] by CIRCCOMB:def 8;
then
A12: <*x1(),x2(),x3()*> = (the Arity of S()+*S).g by XTUPLE_0:1
.= the_arity_of g by MSUALG_1:def 1;
A13: g`2 = f();
A14: s is stabilizing by Def2;
A15: the carrier of S()+*S = (the carrier of S()) \/ the carrier of S by
CIRCCOMB:def 2;
A16: rng <*x1(),x2(),x3()*> = {x1(),x2(),x3()} by FINSEQ_2:128;
then
A17: x3() in rng <*x1(),x2(),x3()*> by ENUMSET1:def 1;
then
A18: x3() in the carrier of S()+*S by A11,A15,XBOOLE_0:def 3;
x3() in InnerVertices S() or x3() in InputVertices S \ InnerVertices S
() by A11,A17,XBOOLE_0:def 5;
then x3() in InnerVertices S() or x3() in InputVertices (S()+*S) by A7,
XBOOLE_0:def 3;
then
A19: a3 = Following(s, stabilization-time s9).x3() by A10,A6,Th1,FUNCT_1:49;
A20: [<*x1(),x2(),x3()*>,f()] = Output S by Th15;
A21: dom Following(s, stabilization-time s9) = the carrier of S()+*S by
CIRCUIT1:3;
A22: x1() in rng <*x1(),x2(),x3()*> by A16,ENUMSET1:def 1;
then x1() in InnerVertices S() or x1() in InputVertices S \ InnerVertices S
() by A11,XBOOLE_0:def 5;
then x1() in InnerVertices S() or x1() in InputVertices (S()+*S) by A7,
XBOOLE_0:def 3;
then
A23: a1 = Following(s, stabilization-time s9).x1() by A8,A6,Th1,FUNCT_1:49;
A24: x2() in rng <*x1(),x2(),x3()*> by A16,ENUMSET1:def 1;
then
A25: x2() in the carrier of S()+*S by A11,A15,XBOOLE_0:def 3;
x2() in InnerVertices S() or x2() in InputVertices S \ InnerVertices S
() by A11,A24,XBOOLE_0:def 5;
then x2() in InnerVertices S() or x2() in InputVertices (S()+*S) by A7,
XBOOLE_0:def 3;
then
A26: a2 = Following(s, stabilization-time s9).x2() by A9,A6,Th1,FUNCT_1:49;
x1() in the carrier of S()+*S by A11,A22,A15,XBOOLE_0:def 3;
then
A27: Following(s, stabilization-time s9)*<*x1(),x2(),x3()*> = <*a1,a2,a3 *>
by A25,A18,A23,A26,A19,A21,FINSEQ_2:126;
A28: the_result_sort_of g = (the ResultSort of S()+*S).g by MSUALG_1:def 2
.= g by CIRCCOMB:44;
stabilization-time s <= 1+stabilization-time s9 by A2,A3,Th48;
hence (Result s).Output S = (Following(s, 1+stabilization-time s9)).Output S
by A14,Th5
.= (Following Following(s, stabilization-time s9)).g by A20,FACIRC_1:12
.= f().(Following(s, stabilization-time s9)*<*x1(),x2(),x3()*>) by A28,A12
,A13,FACIRC_1:34
.= F(a1,a2,a3) by A1,A27;
end;
scheme
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
A1: 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
A2: not Output 1GateCircStr(<*x1(),x2(),x3(),x4()*>,f()) in InputVertices S()
proof
set S = 1GateCircStr(<*x1(),x2(),x3(),x4()*>,f());
let s be State of C() +* 1GateCircuit(<*x1(),x2(),x3(),x4()*>,f());
let s9 be State of C() such that
A3: s9 = s|the carrier of S();
A4: s9 is stabilizing by Def2;
InnerVertices S = {Output S} by Th16;
then
A5: InputVertices S() misses InnerVertices S by A2,ZFMISC_1:50;
then
A6: Following(s, stabilization-time s9)|the carrier of S() = Following(s9,
stabilization-time s9) by A3,Th27,CIRCCMB2:13
.= Result s9 by A4,Th2;
S() tolerates S by CIRCCOMB:47;
then
A7: InputVertices (S()+*S) = (InputVertices S()) \/ (InputVertices S \
InnerVertices S()) by A5,FACIRC_1:4;
A8: [<*x1(),x2(),x3(),x4()*>,f()] = Output S by Th15;
A9: s is stabilizing by Def2;
A10: the carrier of S()+*S = (the carrier of S()) \/ the carrier of S by
CIRCCOMB:def 2;
the carrier' of S = {[<*x1(),x2(),x3(),x4()*>,f()]} by CIRCCOMB:def 6;
then [<*x1(),x2(),x3(),x4()*>,f()] in {[<*x1(),x2(),x3(),x4()*>,f()]} & the
carrier' of S()+*S = (the carrier' of S())\/{[<*x1(),x2(),x3(),x4() *>,f()]}
by CIRCCOMB:def 2,TARSKI:def 1;
then reconsider g = [<*x1(),x2(),x3(),x4()*>,f()] as Gate of S()+*S by
XBOOLE_0:def 3;
let a1, a2, a3, a4 be Element of B() such that
A11: ( x1() in InnerVertices S() implies a1 = (Result s9).x1())&( not x1(
) in InnerVertices S() implies a1 = s.x1()) and
A12: ( x2() in InnerVertices S() implies a2 = (Result s9).x2())&( not x2(
) in InnerVertices S() implies a2 = s.x2()) and
A13: ( x3() in InnerVertices S() implies a3 = (Result s9).x3())&( not x3(
) in InnerVertices S() implies a3 = s.x3()) and
A14: ( x4() in InnerVertices S() implies a4 = (Result s9).x4())&( not x4(
) in InnerVertices S() implies a4 = s.x4());
A15: InputVertices S = rng <*x1(),x2(),x3(),x4()*> by CIRCCOMB:42;
A16: rng <*x1(),x2(),x3(),x4()*> = {x1(),x2(),x3(),x4()} by Th13;
then
A17: x3() in rng <*x1(),x2(),x3(),x4()*> by ENUMSET1:def 2;
then
A18: x3() in the carrier of S()+*S by A15,A10,XBOOLE_0:def 3;
A19: x4() in rng <*x1(),x2(),x3(),x4()*> by A16,ENUMSET1:def 2;
then
A20: x4() in the carrier of S()+*S by A15,A10,XBOOLE_0:def 3;
A21: x1() in rng <*x1(),x2(),x3(),x4()*> by A16,ENUMSET1:def 2;
then
A22: x1() in the carrier of S()+*S by A15,A10,XBOOLE_0:def 3;
x3() in InnerVertices S() or x3() in InputVertices S \ InnerVertices S
() by A15,A17,XBOOLE_0:def 5;
then x3() in InnerVertices S() or x3() in InputVertices (S()+*S) by A7,
XBOOLE_0:def 3;
then
A23: a3 = Following(s, stabilization-time s9).x3() by A13,A6,Th1,FUNCT_1:49;
g = [(the Arity of S()+*S).g, g`2] by CIRCCOMB:def 8;
then
A24: <*x1(),x2(),x3(),x4()*> = (the Arity of S()+*S).g by XTUPLE_0:1
.= the_arity_of g by MSUALG_1:def 1;
A25: g`2 = f();
x1() in InnerVertices S() or x1() in InputVertices S \ InnerVertices S
() by A15,A21,XBOOLE_0:def 5;
then x1() in InnerVertices S() or x1() in InputVertices (S()+*S) by A7,
XBOOLE_0:def 3;
then
A26: a1 = Following(s, stabilization-time s9).x1() by A11,A6,Th1,FUNCT_1:49;
A27: x2() in rng <*x1(),x2(),x3(),x4()*> by A16,ENUMSET1:def 2;
then
A28: x2() in the carrier of S()+*S by A15,A10,XBOOLE_0:def 3;
x4() in InnerVertices S() or x4() in InputVertices S \ InnerVertices S
() by A15,A19,XBOOLE_0:def 5;
then x4() in InnerVertices S() or x4() in InputVertices (S()+*S) by A7,
XBOOLE_0:def 3;
then
A29: a4 = Following(s, stabilization-time s9).x4() by A14,A6,Th1,FUNCT_1:49;
x2() in InnerVertices S() or x2() in InputVertices S \ InnerVertices S
() by A15,A27,XBOOLE_0:def 5;
then x2() in InnerVertices S() or x2() in InputVertices (S()+*S) by A7,
XBOOLE_0:def 3;
then
A30: a2 = Following(s, stabilization-time s9).x2() by A12,A6,Th1,FUNCT_1:49;
dom Following(s, stabilization-time s9) = the carrier of S()+*S by CIRCUIT1:3
;
then
A31: Following(s, stabilization-time s9)*<*x1(),x2(),x3(),x4()*> = <*a1,a2,
a3,a4*> by A22,A28,A18,A20,A26,A30,A23,A29,Th33;
A32: the_result_sort_of g = (the ResultSort of S()+*S).g by MSUALG_1:def 2
.= g by CIRCCOMB:44;
stabilization-time s <= 1+stabilization-time s9 by A2,A3,Th48;
hence (Result s).Output S = (Following(s, 1+stabilization-time s9)).Output S
by A9,Th5
.= (Following Following(s, stabilization-time s9)).g by A8,FACIRC_1:12
.= f().(Following(s, stabilization-time s9)*<*x1(),x2(),x3(),x4()*>) by A32
,A24,A25,FACIRC_1:34
.= F(a1,a2,a3,a4) by A1,A31;
end;
scheme
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
A1: 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
A2: not Output 1GateCircStr(<*x1(),x2(),x3(),x4(),x5()*>,f()) in
InputVertices S()
proof
set S = 1GateCircStr(<*x1(),x2(),x3(),x4(),x5()*>,f());
let s be State of C() +* 1GateCircuit(<*x1(),x2(),x3(),x4(),x5()*>,f());
let s9 be State of C() such that
A3: s9 = s|the carrier of S();
A4: s9 is stabilizing by Def2;
InnerVertices S = {Output S} by Th16;
then
A5: InputVertices S() misses InnerVertices S by A2,ZFMISC_1:50;
then
A6: Following(s, stabilization-time s9)|the carrier of S() = Following(s9,
stabilization-time s9) by A3,Th27,CIRCCMB2:13
.= Result s9 by A4,Th2;
S() tolerates S by CIRCCOMB:47;
then
A7: InputVertices (S()+*S) = (InputVertices S()) \/ (InputVertices S \
InnerVertices S()) by A5,FACIRC_1:4;
A8: [<*x1(),x2(),x3(),x4(),x5()*>,f()] = Output S by Th15;
A9: s is stabilizing by Def2;
A10: the carrier of S()+*S = (the carrier of S()) \/ the carrier of S by
CIRCCOMB:def 2;
the carrier' of S = {[<*x1(),x2(),x3(),x4(),x5()*>,f()]} by CIRCCOMB:def 6;
then
[<*x1(),x2(),x3(),x4(),x5()*>,f()] in {[<*x1(),x2(),x3(),x4(),x5()*>, f
()]} & the carrier' of S()+*S = (the carrier' of S())\/{[<*x1(),x2(),x3(),x4()
,x5()*>,f()]} by CIRCCOMB:def 2,TARSKI:def 1;
then reconsider g = [<*x1(),x2(),x3(),x4(),x5()*>,f()] as Gate of S()+*S by
XBOOLE_0:def 3;
let a1, a2, a3, a4, a5 be Element of B() such that
A11: ( x1() in InnerVertices S() implies a1 = (Result s9).x1())&( not x1(
) in InnerVertices S() implies a1 = s.x1()) and
A12: ( x2() in InnerVertices S() implies a2 = (Result s9).x2())&( not x2(
) in InnerVertices S() implies a2 = s.x2()) and
A13: ( x3() in InnerVertices S() implies a3 = (Result s9).x3())&( not x3(
) in InnerVertices S() implies a3 = s.x3()) and
A14: ( x4() in InnerVertices S() implies a4 = (Result s9).x4())&( not x4(
) in InnerVertices S() implies a4 = s.x4()) and
A15: ( x5() in InnerVertices S() implies a5 = (Result s9).x5())&( not x5(
) in InnerVertices S() implies a5 = s.x5());
A16: InputVertices S = rng <*x1(),x2(),x3(),x4(),x5()*> by CIRCCOMB:42;
A17: rng <*x1(),x2(),x3(),x4(),x5()*> = {x1(),x2(),x3(),x4(),x5()} by Th14;
then
A18: x1() in rng <*x1(),x2(),x3(),x4(),x5()*> by ENUMSET1:def 3;
then
A19: x1() in the carrier of S()+*S by A16,A10,XBOOLE_0:def 3;
A20: x5() in rng <*x1(),x2(),x3(),x4(),x5()*> by A17,ENUMSET1:def 3;
then
A21: x5() in the carrier of S()+*S by A16,A10,XBOOLE_0:def 3;
x5() in InnerVertices S() or x5() in InputVertices S \ InnerVertices S
() by A16,A20,XBOOLE_0:def 5;
then x5() in InnerVertices S() or x5() in InputVertices (S()+*S) by A7,
XBOOLE_0:def 3;
then
A22: a5 = Following(s, stabilization-time s9).x5() by A15,A6,Th1,FUNCT_1:49;
A23: x4() in rng <*x1(),x2(),x3(),x4(),x5()*> by A17,ENUMSET1:def 3;
then
A24: x4() in the carrier of S()+*S by A16,A10,XBOOLE_0:def 3;
A25: x3() in rng <*x1(),x2(),x3(),x4(),x5()*> by A17,ENUMSET1:def 3;
then
A26: x3() in the carrier of S()+*S by A16,A10,XBOOLE_0:def 3;
x3() in InnerVertices S() or x3() in InputVertices S \ InnerVertices S
() by A16,A25,XBOOLE_0:def 5;
then x3() in InnerVertices S() or x3() in InputVertices (S()+*S) by A7,
XBOOLE_0:def 3;
then
A27: a3 = Following(s, stabilization-time s9).x3() by A13,A6,Th1,FUNCT_1:49;
A28: x2() in rng <*x1(),x2(),x3(),x4(),x5()*> by A17,ENUMSET1:def 3;
then
A29: x2() in the carrier of S()+*S by A16,A10,XBOOLE_0:def 3;
x1() in InnerVertices S() or x1() in InputVertices S \ InnerVertices S
() by A16,A18,XBOOLE_0:def 5;
then x1() in InnerVertices S() or x1() in InputVertices (S()+*S) by A7,
XBOOLE_0:def 3;
then
A30: a1 = Following(s, stabilization-time s9).x1() by A11,A6,Th1,FUNCT_1:49;
g = [(the Arity of S()+*S).g, g`2] by CIRCCOMB:def 8; then
A31: <*x1(),x2(),x3(),x4(),x5()*> = (the Arity of S()+*S).g by XTUPLE_0:1
.= the_arity_of g by MSUALG_1:def 1;
A32: g`2 = f();
x4() in InnerVertices S() or x4() in InputVertices S \ InnerVertices S
() by A16,A23,XBOOLE_0:def 5;
then x4() in InnerVertices S() or x4() in InputVertices (S()+*S) by A7,
XBOOLE_0:def 3;
then
A33: a4 = Following(s, stabilization-time s9).x4() by A14,A6,Th1,FUNCT_1:49;
x2() in InnerVertices S() or x2() in InputVertices S \ InnerVertices S
() by A16,A28,XBOOLE_0:def 5;
then x2() in InnerVertices S() or x2() in InputVertices (S()+*S) by A7,
XBOOLE_0:def 3;
then
A34: a2 = Following(s, stabilization-time s9).x2() by A12,A6,Th1,FUNCT_1:49;
dom Following(s, stabilization-time s9) = the carrier of S()+*S by CIRCUIT1:3
; then
A35: Following(s, stabilization-time s9)*<*x1(),x2(),x3(),x4(),x5()*> = <*a1
,a2,a3,a4,a5*> by A19,A29,A26,A24,A21,A30,A34,A27,A33,A22,Th34;
A36: the_result_sort_of g = (the ResultSort of S()+*S).g by MSUALG_1:def 2
.= g by CIRCCOMB:44;
stabilization-time s <= 1+stabilization-time s9 by A2,A3,Th48;
hence (Result s).Output S = (Following(s, 1+stabilization-time s9)).Output S
by A9,Th5
.= (Following Following(s, stabilization-time s9)).g by A8,FACIRC_1:12
.= f().(Following(s, stabilization-time s9)*<*x1(),x2(),x3(),x4(),x5()*>
) by A36,A31,A32,FACIRC_1:34
.= F(a1,a2,a3,a4,a5) by A1,A35;
end;
begin :: Inputs without pairs
definition
let S be non empty ManySortedSign;
attr S is with_nonpair_inputs means
: Def11:
InputVertices S is without_pairs;
end;
registration
cluster NAT -> without_pairs;
coherence;
let X be without_pairs set;
cluster -> without_pairs for Subset of X;
coherence
by FACIRC_1:def 2;
end;
registration
cluster natural-valued -> nonpair-yielding for Function;
coherence
proof
let f be Function;
assume f is natural-valued;
then
A1: rng f c= NAT by VALUED_0:def 6;
let x be set;
assume x in dom f;
then f.x in rng f by FUNCT_1:def 3;
hence thesis by A1;
end;
end;
registration
cluster one-to-one natural-valued for FinSequence;
existence
proof
set p = the one-to-one FinSequence of NAT;
take p;
thus thesis;
end;
end;
registration
let n be Element of NAT;
cluster one-to-one natural-valued for FinSeqLen of n;
existence
proof
set p = id Seg n;
A1: dom p = Seg n;
then rng p = Seg n & p is FinSequence by FINSEQ_1:def 2;
then reconsider p as one-to-one FinSequence of NAT by FINSEQ_1:def 4;
len p = n by A1,FINSEQ_1:def 3;
then reconsider p as FinSeqLen of n by CARD_1:def 7;
take p;
thus thesis;
end;
end;
registration
let p be nonpair-yielding FinSequence;
let f be set;
cluster 1GateCircStr(p,f) -> with_nonpair_inputs;
coherence
proof
InputVertices 1GateCircStr(p,f) = rng p by CIRCCOMB:42;
hence InputVertices 1GateCircStr(p,f) is without_pairs;
end;
end;
registration
cluster with_nonpair_inputs for one-gate ManySortedSign;
existence
proof
set n = the Element of NAT,X = the non empty finite set;
set f = the Function of n-tuples_on X, X;
set p = the natural-valued FinSeqLen of n;
take 1GateCircStr(p,f);
thus thesis;
end;
let X be non empty finite set;
cluster with_nonpair_inputs for one-gate Signature of X;
existence
proof
reconsider z=0 as Element of NAT;
set p = the natural-valued FinSeqLen of z;
set f = the Function of z-tuples_on X, X;
take 1GateCircStr(p,f);
thus thesis;
end;
end;
registration
let S be with_nonpair_inputs non empty ManySortedSign;
cluster InputVertices S -> without_pairs;
coherence by Def11;
end;
theorem
for S being with_nonpair_inputs non empty ManySortedSign for x being
Vertex of S st x is pair holds x in InnerVertices S
proof
let S be with_nonpair_inputs non empty ManySortedSign;
let x be Vertex of S;
the carrier of S = (InputVertices S) \/ InnerVertices S by XBOOLE_1:45;
then x in InputVertices S or x in InnerVertices S by XBOOLE_0:def 3;
hence thesis by FACIRC_1:def 2;
end;
registration
let S be unsplit gate`1=arity non empty ManySortedSign;
cluster InnerVertices S -> Relation-like;
coherence
proof
let x be object;
assume
A1: x in InnerVertices S;
InnerVertices S = the carrier' of S by FACIRC_1:37;
then x = [(the Arity of S).x, x`2] by A1,CIRCCOMB:def 8;
hence thesis;
end;
end;
registration
let S be unsplit gate`2=den non empty non void ManySortedSign;
cluster InnerVertices S -> Relation-like;
coherence
proof
let x be object;
consider A being MSAlgebra over S such that
A1: A is gate`2=den by CIRCCOMB:def 11;
assume x in InnerVertices S;
then reconsider g = x as Gate of S by FACIRC_1:37;
g = [g`1, (the Charact of A).g] by A1;
hence thesis;
end;
end;
registration
let S1,S2 be with_nonpair_inputs unsplit gate`1=arity non empty
ManySortedSign;
cluster S1+*S2 -> with_nonpair_inputs;
coherence
proof
S1 tolerates S2 by CIRCCOMB:47;
then InputVertices (S1+*S2) is Subset of (InputVertices S1) \/
InputVertices S2 by CIRCCOMB:11;
hence InputVertices (S1+*S2) is without_pairs;
end;
end;
theorem
for x being non pair set, R being Relation holds not x in R
proof
let x be non pair set;
not ex a,b being object st x = [a,b];
hence thesis by RELAT_1:def 1;
end;
theorem Th51:
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
proof
let x1 be set, X be non empty finite set;
let f be Function of 1-tuples_on X, X;
let S be with_nonpair_inputs Signature of X such that
A1: x1 in the carrier of S or x1 is non pair;
A2: not Output 1GateCircStr(<*x1*>, f) in InputVertices S by FACIRC_1:def 2;
per cases by A1;
suppose
x1 in the carrier of S;
hence InputVertices (S +* 1GateCircStr(<*x1*>, f)) is without_pairs by A2
,Th37;
end;
suppose
x1 is non pair;
then reconsider a = x1 as non pair set;
rng <*x1*> = {a} by FINSEQ_1:38;
hence InputVertices (S +* 1GateCircStr(<*x1*>, f)) is without_pairs;
end;
end;
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;
coherence by Th51;
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;
coherence;
end;
theorem Th52:
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
proof
let x1,x2 be set, X be non empty finite set;
let f be Function of 2-tuples_on X, X;
let S be with_nonpair_inputs Signature of X such that
A1: ( x1 in the carrier of S or x1 is non pair)&( x2 in the carrier of S
or x2 is non pair);
A2: not Output 1GateCircStr(<*x1,x2*>, f) in InputVertices S by FACIRC_1:def 2;
per cases by A1;
suppose
x1 in the carrier of S & x2 in the carrier of S or x1 in the
carrier of S & not x2 in InnerVertices S or x2 in the carrier of S & not x1 in
InnerVertices S;
then
InputVertices (S +* 1GateCircStr(<*x1,x2*>, f)) = InputVertices S or {
x2} is without_pairs & InputVertices (S +* 1GateCircStr(<*x1,x2*>, f)) = {x2}
\/ InputVertices S or {x1} is without_pairs & InputVertices (S +* 1GateCircStr(
<*x1,x2*>, f)) = {x1} \/ InputVertices S by A1,A2,Th38,Th39,Th40;
hence InputVertices (S +* 1GateCircStr(<*x1,x2*>, f)) is without_pairs;
end;
suppose
x1 is non pair & x2 is non pair;
then reconsider a = x1, b = x2 as non pair set;
rng <*x1,x2*> = {a,b} by FINSEQ_2:127;
hence InputVertices (S +* 1GateCircStr(<*x1,x2*>, f)) is without_pairs;
end;
end;
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;
coherence by Th52;
cluster S +* 1GateCircStr(<*n2,x1*>, f) -> with_nonpair_inputs;
coherence by Th52;
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;
coherence by Th52;
end;
theorem Th53:
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
proof
let x1,x2,x3 be set, X be non empty finite set;
let f be Function of 3-tuples_on X, X;
let S be with_nonpair_inputs Signature of X such that
A1: ( 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);
A2: not Output 1GateCircStr(<*x1,x2,x3*>, f) in InputVertices S by
FACIRC_1:def 2;
per cases by A1;
suppose
x1 in the carrier of S & x2 in the carrier of S & x3 in the
carrier of S or x1 in the carrier of S & not x2 in InnerVertices S & x3 in the
carrier of S or x2 in the carrier of S & not x1 in InnerVertices S & x3 in the
carrier of S or x1 in the carrier of S & x2 in the carrier of S & not x3 in
InnerVertices S or x1 in the carrier of S & not x2 in InnerVertices S & not x3
in InnerVertices S or x2 in the carrier of S & not x1 in InnerVertices S & not
x3 in InnerVertices S or not x1 in InnerVertices S & not x2 in InnerVertices S
& x3 in the carrier of S;
then InputVertices (S +* 1GateCircStr(<*x1,x2,x3*>, f)) = InputVertices S
or {x2} is without_pairs & InputVertices (S +* 1GateCircStr(<*x1,x2,x3*>, f)) =
{x2} \/ InputVertices S or {x1} is without_pairs & InputVertices (S +*
1GateCircStr(<*x1,x2,x3*>, f)) = {x1} \/ InputVertices S or {x3} is
without_pairs & InputVertices (S +* 1GateCircStr(<*x1,x2,x3*>, f)) = {x3} \/
InputVertices S or {x1,x2} is without_pairs & InputVertices (S +* 1GateCircStr(
<*x1,x2,x3*>, f)) = {x1,x2} \/ InputVertices S or {x2,x3} is without_pairs &
InputVertices (S +* 1GateCircStr(<*x1,x2,x3*>, f)) = {x2,x3} \/ InputVertices S
or {x1,x3} is without_pairs & InputVertices (S +* 1GateCircStr(<*x1,x2,x3*>, f)
) = {x1,x3} \/ InputVertices S by A1,A2,Th41,Th42,Th43,Th44,Th45,Th46,Th47;
hence InputVertices (S +* 1GateCircStr(<*x1,x2,x3*>, f)) is without_pairs;
end;
suppose
x1 is non pair & x2 is non pair & x3 is non pair;
then reconsider a = x1, b = x2, c = x3 as non pair set;
rng <*x1,x2,x3*> = {a,b,c} by FINSEQ_2:128;
hence InputVertices (S +* 1GateCircStr(<*x1,x2,x3*>, f)) is without_pairs;
end;
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, 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;
coherence by Th53;
cluster S +* 1GateCircStr(<*x1,n,x2*>, f) -> with_nonpair_inputs;
coherence by Th53;
cluster S +* 1GateCircStr(<*n,x1,x2*>, f) -> with_nonpair_inputs;
coherence by Th53;
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;
coherence by Th53;
cluster S +* 1GateCircStr(<*n1,x,n2*>, f) -> with_nonpair_inputs;
coherence by Th53;
cluster S +* 1GateCircStr(<*n1,n2,x*>, f) -> with_nonpair_inputs;
coherence by Th53;
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;
coherence by Th53;
end;