:: Combining of Multi Cell Circuits
:: by Grzegorz Bancerek , Shin'nosuke Yamaguchi and Yasunari Shidama
::
:: Received March 22, 2002
:: Copyright (c) 2002-2021 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NAT_1, FUNCT_1, FINSEQ_2, MARGREL1, CIRCCOMB, LATTICES, FINSET_1,
XBOOLE_0, MSUALG_1, FSM_1, CIRCUIT1, RELAT_1, CIRCUIT2, STRUCT_0,
MSAFREE2, GLIB_000, ARYTM_3, CARD_1, XXREAL_0, PBOOLE, NUMBERS, MCART_1,
FUNCT_4, PARTFUN1, FACIRC_1, TARSKI, ORDINAL1;
notations TARSKI, XBOOLE_0, ORDINAL1, NUMBERS, XCMPLX_0, XFAMILY, XXREAL_0,
NAT_1, XTUPLE_0, MCART_1, FINSET_1, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2,
FINSEQ_2, FUNCT_4, PBOOLE, MARGREL1, STRUCT_0, MSUALG_1, MSAFREE2,
CIRCUIT1, CIRCUIT2, CIRCCOMB, FACIRC_1;
constructors LIMFUNC1, CIRCUIT1, CIRCUIT2, FACIRC_1, NAT_1, RELSET_1,
XTUPLE_0, XFAMILY;
registrations RELAT_1, FUNCT_1, ORDINAL1, XREAL_0, CARD_3, STRUCT_0, CIRCCOMB,
FACIRC_1, NAT_1, MARGREL1, CARD_1, XTUPLE_0;
requirements NUMERALS, SUBSET, BOOLE, ARITHM;
begin :: One gate circuits
registration
let n be Nat;
let f be Function of n-tuples_on BOOLEAN, BOOLEAN;
let p be FinSeqLen of n;
cluster 1GateCircuit(p,f) -> Boolean;
end;
theorem :: CIRCCMB2:1
for X being finite non empty set, n being Nat for p being
FinSeqLen of n for f being Function of n-tuples_on X, X for o being OperSymbol
of 1GateCircStr(p,f) for s being State of 1GateCircuit(p,f) holds o
depends_on_in s = s*p;
theorem :: CIRCCMB2:2
for X being finite non empty set, n being Nat for p being FinSeqLen of
n for f being Function of n-tuples_on X, X for s being State of 1GateCircuit(p,
f) holds Following s is stable;
theorem :: CIRCCMB2:3
for S being non void Circuit-like non empty ManySortedSign for
A being non-empty Circuit of S for s being State of A st s is stable
for n being natural Number holds Following(s, n) = s;
theorem :: CIRCCMB2:4
for S being non void Circuit-like non empty ManySortedSign for
A being non-empty Circuit of S for s being State of A,
n1, n2 being natural Number st Following(s, n1) is stable & n1 <= n2
holds Following(s, n2) = Following(s, n1);
begin :: Defining Many Cell Circuit Structures
scheme :: CIRCCMB2:sch 1
CIRCCMB29sch1 {S0() -> non empty ManySortedSign, o0()-> object,
S(object,object,object)-> non empty ManySortedSign,
o(object,object) -> object}:
ex f,h being ManySortedSet of
NAT st f.0 = S0() & h.0 = o0() & for n being Nat, S being non empty
ManySortedSign, x being set st S = f.n & x = h.n holds f.(n+1) = S(S,x,n) & h.(
n+1) = o(x,n);
scheme :: CIRCCMB2:sch 2 ::CircSch1
CIRCCMB29sch2 {S(object,object,object) -> non empty ManySortedSign,
o(object,object) -> object, P[object,object,object],
f,h() -> ManySortedSet of NAT}:
for n being Nat ex S being
non empty ManySortedSign st S = f().n & P[S,h().n,n]
provided
ex S being non empty ManySortedSign, x being set st S = f().0 & x =
h().0 & P[S, x, 0] and
for n being Nat, S being non empty ManySortedSign, x being set st S
= f().n & x = h().n holds f().(n+1) = S(S,x,n) & h().(n+1) = o(x,n) and
for n being Nat, S being non empty ManySortedSign, x being set st S
= f().n & x = h().n & P[S,x,n] holds P[S(S,x,n), o(x,n), n+1];
scheme :: CIRCCMB2:sch 3 :: CircSchR0
CIRCCMB29sch3 {S0() -> non empty ManySortedSign,
S(object,object,object) -> non empty ManySortedSign,
o(object,object) -> object, f,h() -> ManySortedSet of NAT}: for n being
Nat, x being set st x = h().n holds h().(n+1) = o(x,n)
provided
f().0 = S0() and
for n being Nat, S being non empty ManySortedSign, x being set st S
= f().n & x = h().n holds f().(n+1) = S(S,x,n) & h().(n+1) = o(x,n);
scheme :: CIRCCMB2:sch 4 :: CircStrExSch
CIRCCMB29sch4 {S0() -> non empty ManySortedSign, o0()-> object,
S(object,object,object) -> non empty ManySortedSign,
o(object,object) -> object, n() -> Nat}:
ex S being non
empty ManySortedSign, f,h being ManySortedSet of NAT st S = f.n() & f.0 = S0()
& h.0 = o0() & for n being Nat, S being non empty ManySortedSign, x being set
st S = f.n & x = h.n holds f.(n+1) = S(S,x,n) & h.(n+1) = o(x,n);
scheme :: CIRCCMB2:sch 5 :: CircStrUniqSch
CIRCCMB29sch5 {S0() -> non empty ManySortedSign, o0()-> object,
S(object,object,object) -> non empty ManySortedSign,
o(object,object) -> object, n() -> Nat}:
for S1,S2 being non empty ManySortedSign
st (ex f,h being ManySortedSet of NAT st S1 = f.n() &
f.0 = S0() & h.0 = o0() & for n being Nat, S being non empty ManySortedSign, x
being set st S = f.n & x = h.n holds f.(n+1) = S(S,x,n) & h.(n+1) = o(x,n)) & (
ex f,h being ManySortedSet of NAT st S2 = f.n() & f.0 = S0() & h.0 = o0() & for
n being Nat, S being non empty ManySortedSign, x being set st S = f.n & x = h.n
holds f.(n+1) = S(S,x,n) & h.(n+1) = o(x,n)) holds S1 = S2;
scheme :: CIRCCMB2:sch 6 :: CircStrDefSch
CIRCCMB29sch6 {S0() -> non empty ManySortedSign, o0()-> object,
S(object,object,object) -> non empty ManySortedSign,
o(object,object) -> object, n() -> Nat}: (ex S being non
empty ManySortedSign, f,h being ManySortedSet of NAT st S = f.n() & f.0 = S0()
& h.0 = o0() & for n being Nat, S being non empty ManySortedSign, x being set
st S = f.n & x = h.n holds f.(n+1) = S(S,x,n) & h.(n+1) = o(x,n)) & for S1,S2
being non empty ManySortedSign st (ex f,h being ManySortedSet of NAT st S1 = f.
n() & f.0 = S0() & h.0 = o0() & for n being Nat, S being non empty
ManySortedSign, x being set st S = f.n & x = h.n holds f.(n+1) = S(S,x,n) & h.(
n+1) = o(x,n)) & (ex f,h being ManySortedSet of NAT st S2 = f.n() & f.0 = S0()
& h.0 = o0() & for n being Nat, S being non empty ManySortedSign, x being set
st S = f.n & x = h.n holds f.(n+1) = S(S,x,n) & h.(n+1) = o(x,n)) holds S1 = S2
;
scheme :: CIRCCMB2:sch 7 :: attrCircStrExSch
CIRCCMB29sch7 {S0() -> non empty ManySortedSign,
S(object,object,object) -> non empty
ManySortedSign, o0()-> object, o(object,object) -> object, n() -> Nat}:
ex S being unsplit
gate`1=arity gate`2isBoolean non void non empty non empty strict ManySortedSign
, f,h being ManySortedSet of NAT st S = f.n() & f.0 = S0() & h.0 = o0() & for n
being Nat, S being non empty ManySortedSign, x being set st S = f.n & x = h.n
holds f.(n+1) = S(S,x,n) & h.(n+1) = o(x,n)
provided
S0() is unsplit gate`1=arity gate`2isBoolean non void non empty strict and
for S being unsplit gate`1=arity gate`2isBoolean non void strict non
empty ManySortedSign, x being set, n being Nat holds S(S,x,n) is unsplit
gate`1=arity gate`2isBoolean non void non empty strict;
scheme :: CIRCCMB2:sch 8 :: ManyCellCircStrExSch
CIRCCMB29sch8 {S0() -> non empty ManySortedSign, S(object,object) -> unsplit
gate`1=arity gate`2isBoolean non void non empty ManySortedSign,
o0()-> object, o(object,object) -> object, n() -> Nat}:
ex S being unsplit gate`1=arity gate`2isBoolean
non void non empty non empty strict ManySortedSign, f,h being ManySortedSet of
NAT st S = f.n() & f.0 = S0() & h.0 = o0() & for n being Nat, S being non empty
ManySortedSign, x being set st S = f.n & x = h.n holds f.(n+1) = S +* S(x,n) &
h.(n+1) = o(x,n)
provided
S0() is unsplit gate`1=arity gate`2isBoolean non void non empty strict;
scheme :: CIRCCMB2:sch 9 :: attrCircStrUniqSch
CIRCCMB29sch9 {S0() -> non empty ManySortedSign, o0()-> object,
S(object,object,object) -> non empty ManySortedSign,
o(object,object) -> object,
n() -> Nat}:
for S1,S2 being
unsplit gate`1=arity gate`2isBoolean non void non empty strict non empty
ManySortedSign st (ex f,h being ManySortedSet of NAT st S1 = f.n() & f.0 = S0()
& h.0 = o0() & for n being Nat, S being non empty ManySortedSign, x being set
st S = f.n & x = h.n holds f.(n+1) = S(S,x,n) & h.(n+1) = o(x,n)) & (ex f,h
being ManySortedSet of NAT st S2 = f.n() & f.0 = S0() & h.0 = o0() & for n
being Nat, S being non empty ManySortedSign, x being set st S = f.n & x = h.n
holds f.(n+1) = S(S,x,n) & h.(n+1) = o(x,n)) holds S1 = S2;
begin
theorem :: CIRCCMB2:5
for S1,S2 being non empty ManySortedSign st S1 tolerates S2 holds
InputVertices (S1+*S2) = ((InputVertices S1)\(InnerVertices S2)) \/ ((
InputVertices S2)\(InnerVertices S1));
theorem :: CIRCCMB2:6
for X being without_pairs set, Y being Relation holds X \ Y = X;
theorem :: CIRCCMB2:7
for X being Relation, Y, Z being set st Z c= Y & Y \ Z is
without_pairs holds X \ Y = X \ Z;
theorem :: CIRCCMB2:8
for X,Z being set, Y being Relation st Z c= Y & X \ Z is
without_pairs holds X \ Y = X \ Z;
scheme :: CIRCCMB2:sch 10 :: InputOfManyCellCircStr
CIRCCMB29sch10 {S0() -> unsplit gate`1=arity gate`2isBoolean non void non
empty ManySortedSign, f(object) -> object, h() -> ManySortedSet of NAT,
S(object,object) ->
unsplit gate`1=arity gate`2isBoolean non void non empty ManySortedSign,
o(object,object) -> object}: for n being Nat
ex S1,S2 being unsplit gate`1=arity
gate`2isBoolean non void non empty ManySortedSign st S1 = f(n) & S2 = f(n+1) &
InputVertices S2 = (InputVertices S1)\/((InputVertices S(h().n,n)) \ {h().n}) &
InnerVertices S1 is Relation & InputVertices S1 is without_pairs
provided
InnerVertices S0() is Relation and
InputVertices S0() is without_pairs and
f(0) = S0() & h().0 in InnerVertices S0() and
for n being Nat, x being set holds InnerVertices S(x,n) is Relation and
for n being Nat, x being set st x = h().n holds (InputVertices S(x,n
)) \ {x} is without_pairs and
for n being Nat, S being non empty ManySortedSign, x being set st S
= f(n) & x = h().n holds f(n+1) = S +* S(x,n) & h().(n+1) = o(x,n) & x in
InputVertices S(x,n) & o(x,n) in InnerVertices S(x,n);
scheme :: CIRCCMB2:sch 11 :: InputOfManyCellCircStr
CIRCCMB29sch11 {Sn(set) -> unsplit gate`1=arity gate`2isBoolean non void non
empty ManySortedSign, h() -> ManySortedSet of NAT,
S(object,object) -> unsplit
gate`1=arity gate`2isBoolean non void non empty ManySortedSign,
o(object,object) -> object}:
for n being Nat holds InputVertices Sn(n+1) = (InputVertices Sn(n))\/((
InputVertices S(h().(n),n)) \ {h().(n)}) & InnerVertices Sn(n) is Relation &
InputVertices Sn(n) is without_pairs
provided
InnerVertices Sn(0) is Relation and
InputVertices Sn(0) is without_pairs and
h().(0) in InnerVertices Sn(0) and
for n being Nat, x being set holds InnerVertices S(x,n) is Relation and
for n being Nat, x being set st x = h().(n) holds (InputVertices S(x
,n)) \ {x} is without_pairs and
for n being Nat, S being non empty ManySortedSign, x being set st S
= Sn(n) & x = h().(n) holds Sn(n+1) = S +* S(x,n) & h().(n+1) = o(x,n) & x in
InputVertices S(x,n) & o(x,n) in InnerVertices S(x,n);
begin :: Defining Many Cell Circuits
scheme :: CIRCCMB2:sch 12
CIRCCMB29sch12 {S0() -> non empty ManySortedSign, A0() -> non-empty
MSAlgebra over S0(), o0()-> object,
S(object,object,object) -> non empty ManySortedSign,
A(object,object,object,object) -> object,
o(object,object) -> object}:
ex f,g,h being ManySortedSet of
NAT st f.0 = S0() & g.0 = A0() & h.0 = o0() & for n being Nat, S being non
empty ManySortedSign, A being non-empty MSAlgebra over S for x being set st S =
f.n & A = g.n & x = h.n holds f.(n+1) = S(S,x,n) & g.(n+1) = A(S,A,x,n) & h.(n+
1) = o(x,n);
scheme :: CIRCCMB2:sch 13 :: CircSch3
CIRCCMB29sch13 {S(set,set,set) -> non empty ManySortedSign,
A(object,object,object,object) -> object,
o(object,object) -> object,
P[object,object,object,object],
f,g,h() -> ManySortedSet of NAT}:
for n being Nat ex S being non empty ManySortedSign, A being non-empty
MSAlgebra over S st S = f().n & A = g().n & P[S,A,h().n,n]
provided
ex S being non empty ManySortedSign, A being non-empty MSAlgebra
over S, x being set st S = f().0 & A = g().0 & x = h().0 & P[S, A, x, 0] and
for n being Nat, S being non empty ManySortedSign, A being non-empty
MSAlgebra over S for x being set st S = f().n & A = g().n & x = h().n holds f()
.(n+1) = S(S,x,n) & g().(n+1) = A(S,A,x,n) & h().(n+1) = o(x,n) and
for n being Nat, S being non empty ManySortedSign, A being non-empty
MSAlgebra over S for x being set st S = f().n & A = g().n & x = h().n & P[S,A,x
,n] holds P[S(S,x,n), A(S,A,x,n), o(x,n), n+1] and
for S being non empty ManySortedSign, A being non-empty MSAlgebra
over S for x being set, n being Nat holds A(S,A,x,n) is non-empty MSAlgebra
over S(S,x,n);
scheme :: CIRCCMB2:sch 14 :: CircSchU2
CIRCCMB29sch14 {S(set,set,set) -> non empty ManySortedSign,
A(object,object,object,object) -> object,
o(object,object) -> object,
f1,f2, g1,g2, h1,h2() -> ManySortedSet of NAT}:
f1() = f2() & g1() = g2() & h1() = h2()
provided
ex S being non empty ManySortedSign, A being non-empty MSAlgebra
over S st S = f1().0 & A = g1().0 and
f1().0 = f2().0 & g1().0 = g2().0 & h1().0 = h2().0 and
for n being Nat, S being non empty ManySortedSign, A being non-empty
MSAlgebra over S for x being set st S = f1().n & A = g1().n & x = h1().n holds
f1().(n+1) = S(S,x,n) & g1().(n+1) = A(S,A,x,n) & h1().(n+1) = o(x,n) and
for n being Nat, S being non empty ManySortedSign, A being non-empty
MSAlgebra over S for x being set st S = f2().n & A = g2().n & x = h2().n holds
f2().(n+1) = S(S,x,n) & g2().(n+1) = A(S,A,x,n) & h2().(n+1) = o(x,n) and
for S being non empty ManySortedSign, A being non-empty MSAlgebra
over S for x being set, n being Nat holds A(S,A,x,n) is non-empty MSAlgebra
over S(S,x,n);
scheme :: CIRCCMB2:sch 15 :: CircSchR2
CIRCCMB29sch15 {S0() -> non empty ManySortedSign, A0() -> non-empty
MSAlgebra over S0(), S(object,object,object) -> non empty ManySortedSign,
A(object,object,object,object) -> object, o(object,object) -> object,
f,g,h() -> ManySortedSet of NAT}: for n being
Nat, S being non empty ManySortedSign, x being set st S = f().n & x = h().n
holds f().(n+1) = S(S,x,n) & h().(n+1) = o(x,n)
provided
f().0 = S0() & g().0 = A0() and
for n being Nat, S being non empty ManySortedSign, A being non-empty
MSAlgebra over S for x being set st S = f().n & A = g().n & x = h().n holds f()
.(n+1) = S(S,x,n) & g().(n+1) = A(S,A,x,n) & h().(n+1) = o(x,n) and
for S being non empty ManySortedSign, A being non-empty MSAlgebra
over S for x being set, n being Nat holds A(S,A,x,n) is non-empty MSAlgebra
over S(S,x,n);
scheme :: CIRCCMB2:sch 16 :: CircuitExSch1
CIRCCMB29sch16 {S0() -> non empty ManySortedSign, A0() -> non-empty
MSAlgebra over S0(), o0()-> object,
S(object,object,object) -> non empty ManySortedSign,
A(object,object,object,object) -> object, o(object,object) -> object,
n() -> Nat}: ex S being non empty
ManySortedSign, A being non-empty MSAlgebra over S, f,g,h being ManySortedSet
of NAT st S = f.n() & A = g.n() & f.0 = S0() & g.0 = A0() & h.0 = o0() & for n
being Nat, S being non empty ManySortedSign, A being non-empty MSAlgebra over S
for x being set st S = f.n & A = g.n & x = h.n holds f.(n+1) = S(S,x,n) & g.(n+
1) = A(S,A,x,n) & h.(n+1) = o(x,n)
provided
for S being non empty ManySortedSign, A being non-empty MSAlgebra
over S for x being set, n being Nat holds A(S,A,x,n) is non-empty MSAlgebra
over S(S,x,n);
scheme :: CIRCCMB2:sch 17 :: CircuitExSch2
CIRCCMB29sch17 {S0,Sn() -> non empty ManySortedSign, A0() -> non-empty
MSAlgebra over S0(), o0()-> object,
S(object,object,object) -> non empty ManySortedSign,
A(object,object,object,object) -> object,
o(object,object) -> object, n() -> Nat}: ex A being non-empty
MSAlgebra over Sn(), f,g,h being ManySortedSet of NAT st Sn() = f.n() & A = g.n
() & f.0 = S0() & g.0 = A0() & h.0 = o0() & for n being Nat, S being non empty
ManySortedSign, A being non-empty MSAlgebra over S for x being set st S = f.n &
A = g.n & x = h.n holds f.(n+1) = S(S,x,n) & g.(n+1) = A(S,A,x,n) & h.(n+1) = o
(x,n)
provided
ex f,h being ManySortedSet of NAT st Sn() = f.n() & f.0 = S0() & h.0
= o0() & for n being Nat, S being non empty ManySortedSign, x being set st S =
f.n & x = h.n holds f.(n+1) = S(S,x,n) & h.(n+1) = o(x,n) and
for S being non empty ManySortedSign, A being non-empty MSAlgebra
over S for x being set, n being Nat holds A(S,A,x,n) is non-empty MSAlgebra
over S(S,x,n);
scheme :: CIRCCMB2:sch 18 :: CircuitUniqSch
CIRCCMB29sch18 {S0,Sn() -> non empty ManySortedSign, A0() -> non-empty
MSAlgebra over S0(), o0()-> object,
S(object,object,object) -> non empty ManySortedSign,
A(object,object,object,object) -> object,
o(object,object) -> object, n() -> Nat}:
for A1,A2 being
non-empty MSAlgebra over Sn() st (ex f,g,h being ManySortedSet of NAT st Sn() =
f.n() & A1 = g.n() & f.0 = S0() & g.0 = A0() & h.0 = o0() & for n being Nat, S
being non empty ManySortedSign, A being non-empty MSAlgebra over S for x being
set st S = f.n & A = g.n & x = h.n holds f.(n+1) = S(S,x,n) & g.(n+1) = A(S,A,x
,n) & h.(n+1) = o(x,n)) & (ex f,g,h being ManySortedSet of NAT st Sn() = f.n()
& A2 = g.n() & f.0 = S0() & g.0 = A0() & h.0 = o0() & for n being Nat, S being
non empty ManySortedSign, A being non-empty MSAlgebra over S for x being set st
S = f.n & A = g.n & x = h.n holds f.(n+1) = S(S,x,n) & g.(n+1) = A(S,A,x,n) & h
.(n+1) = o(x,n)) holds A1 = A2
provided
for S being non empty ManySortedSign, A being non-empty MSAlgebra
over S for x being set, n being Nat holds A(S,A,x,n) is non-empty MSAlgebra
over S(S,x,n);
scheme :: CIRCCMB2:sch 19
CIRCCMB29sch19 {S0, Sn() -> unsplit gate`1=arity gate`2isBoolean non void
strict non empty ManySortedSign, A0() -> Boolean gate`2=den strict Circuit of
S0(), S(object,object,object) -> non empty ManySortedSign,
A(object,object,object,object) -> object, o0()-> object,
o(object,object) -> object, n() -> Nat}:
ex A being Boolean gate`2=den strict
Circuit of Sn(), f,g,h being ManySortedSet of NAT st Sn() = f.n() & A = g.n() &
f.0 = S0() & g.0 = A0() & h.0 = o0() & for n being Nat, S being non empty
ManySortedSign, A being non-empty MSAlgebra over S for x being set st S = f.n &
A = g.n & x = h.n holds f.(n+1) = S(S,x,n) & g.(n+1) = A(S,A,x,n) & h.(n+1) = o
(x,n)
provided
for S being unsplit gate`1=arity gate`2isBoolean non void strict non
empty ManySortedSign, x being set, n being Nat holds S(S,x,n) is unsplit
gate`1=arity gate`2isBoolean non void strict and
ex f,h being ManySortedSet of NAT st Sn() = f.n() & f.0 = S0() & h.0
= o0() & for n being Nat, S being non empty ManySortedSign, x being set st S =
f.n & x = h.n holds f.(n+1) = S(S,x,n) & h.(n+1) = o(x,n) and
for S being non empty ManySortedSign, A being non-empty MSAlgebra
over S for x being set, n being Nat holds A(S,A,x,n) is non-empty MSAlgebra
over S(S,x,n) and
for S,S1 being unsplit gate`1=arity gate`2isBoolean non void strict
non empty ManySortedSign, A being Boolean gate`2=den strict Circuit of S for x
being set, n being Nat st S1 = S(S,x,n) holds A(S,A,x,n) is Boolean gate`2=den
strict Circuit of S1;
definition
let S be non empty ManySortedSign;
let A be object such that
A is non-empty MSAlgebra over S;
func MSAlg(A,S) -> non-empty MSAlgebra over S means
:: CIRCCMB2:def 1
it = A;
end;
scheme :: CIRCCMB2:sch 20 :: ManyCellCircuitExSch
CIRCCMB29sch20 {S0, Sn() -> unsplit gate`1=arity gate`2isBoolean non void
strict non empty ManySortedSign, A0() -> Boolean gate`2=den strict Circuit of
S0(),
S(object,object) -> unsplit gate`1=arity gate`2isBoolean non void non empty
ManySortedSign, A(object,object) -> object, o0()-> object,
o(object,object) -> object, n() -> Nat}:
ex A being Boolean gate`2=den strict Circuit of Sn(), f,g,h being ManySortedSet
of NAT st Sn() = f.n() & A = g.n() & f.0 = S0() & g.0 = A0() & h.0 = o0() & for
n being Nat, S being non empty ManySortedSign, A1 being non-empty MSAlgebra
over S for x being set, A2 being non-empty MSAlgebra over S(x,n) st S = f.n &
A1 = g.n & x = h.n & A2 = A(x,n) holds f.(n+1) = S +* S(x,n) & g.(n+1) = A1 +*
A2 & h.(n+1) = o(x,n)
provided
ex f,h being ManySortedSet of NAT st Sn() = f.n() & f.0 = S0() & h.0
= o0() & for n being Nat, S being non empty ManySortedSign, x being set st S =
f.n & x = h.n holds f.(n+1) = S +* S(x,n) & h.(n+1) = o(x,n) and
for x being set, n being Nat holds A(x,n) is Boolean gate`2=den
strict Circuit of S(x,n);
scheme :: CIRCCMB2:sch 21 :: attrCircuitUniqSch
CIRCCMB29sch21 {S0() -> non empty ManySortedSign, Sn() -> unsplit
gate`1=arity gate`2isBoolean non void strict non empty ManySortedSign, A0() ->
non-empty MSAlgebra over S0(), o0()-> object,
S(object,object,object) -> non empty ManySortedSign,
A(object,object,object,object) -> object,
o(object,object) -> object, n() -> Nat}:
for A1,A2 being Boolean gate`2=den strict Circuit of Sn() st
(ex f,g,h being
ManySortedSet of NAT st Sn() = f.n() & A1 = g.n() & f.0 = S0() & g.0 = A0() & h
.0 = o0() & for n being Nat, S being non empty ManySortedSign, A being
non-empty MSAlgebra over S for x being set st S = f.n & A = g.n & x = h.n holds
f.(n+1) = S(S,x,n) & g.(n+1) = A(S,A,x,n) & h.(n+1) = o(x,n)) & (ex f,g,h being
ManySortedSet of NAT st Sn() = f.n() & A2 = g.n() & f.0 = S0() & g.0 = A0() & h
.0 = o0() & for n being Nat, S being non empty ManySortedSign, A being
non-empty MSAlgebra over S for x being set st S = f.n & A = g.n & x = h.n holds
f.(n+1) = S(S,x,n) & g.(n+1) = A(S,A,x,n) & h.(n+1) = o(x,n)) holds A1 = A2
provided
for S being non empty ManySortedSign, A being non-empty MSAlgebra
over S for x being set, n being Nat holds A(S,A,x,n) is non-empty MSAlgebra
over S(S,x,n);
begin :: Correctness of Many Cell Circuit
theorem :: CIRCCMB2:9
for S1,S2,S being non void Circuit-like non empty ManySortedSign st
InnerVertices S1 misses InputVertices S2 & S = S1+*S2 for C1 being non-empty
Circuit of S1, C2 being non-empty Circuit of S2 for C being non-empty Circuit
of S st C1 tolerates C2 & C = C1+*C2 for s2 being State of C2 for s being State
of C st s2 = s|the carrier of S2 holds Following s2 = (Following s)|the carrier
of S2;
theorem :: CIRCCMB2:10
for S1,S2,S being non void Circuit-like non empty
ManySortedSign st InputVertices S1 misses InnerVertices S2 & S = S1+*S2 for C1
being non-empty Circuit of S1, C2 being non-empty Circuit of S2 for C being
non-empty Circuit of S st C1 tolerates C2 & C = C1+*C2 for s1 being State of C1
for s being State of C st s1 = s|the carrier of S1 holds Following s1 = (
Following s)|the carrier of S1;
theorem :: CIRCCMB2:11
for S1,S2,S being non void Circuit-like non empty ManySortedSign st
InnerVertices S1 misses InputVertices S2 & S = S1+*S2 for C1 being non-empty
Circuit of S1, C2 being non-empty Circuit of S2 for C being non-empty Circuit
of S st C1 tolerates C2 & C = C1+*C2 for s1 being State of C1 for s2 being
State of C2 for s being State of C st s1 = s|the carrier of S1 & s2 = s|the
carrier of S2 & s1 is stable & s2 is stable holds s is stable;
theorem :: CIRCCMB2:12
for S1,S2,S being non void Circuit-like non empty ManySortedSign st
InputVertices S1 misses InnerVertices S2 & S = S1+*S2 for C1 being non-empty
Circuit of S1, C2 being non-empty Circuit of S2 for C being non-empty Circuit
of S st C1 tolerates C2 & C = C1+*C2 for s1 being State of C1 for s2 being
State of C2 for s being State of C st s1 = s|the carrier of S1 & s2 = s|the
carrier of S2 & s1 is stable & s2 is stable holds s is stable;
theorem :: CIRCCMB2:13
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
for n being natural Number holds
Following(s, n)|the carrier of S1 = Following(s1, n);
theorem :: CIRCCMB2:14
for S1,S2,S being non void Circuit-like non empty
ManySortedSign st InputVertices S2 misses InnerVertices S1 & S = S1+*S2 for A1
being non-empty Circuit of S1, A2 being non-empty Circuit of S2 for A being
non-empty Circuit of S st A1 tolerates A2 & A = A1+*A2 for s being State of A,
s2 be State of A2 st s2 = s|the carrier of S2 for n being Nat holds Following(s
, n)|the carrier of S2 = Following(s2, n);
theorem :: CIRCCMB2:15
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
for s1 being State of A1 st s1 = s|the carrier of S1 & s1 is stable for s2
being State of A2 st s2 = s|the carrier of S2 holds (Following s)|the carrier
of S2 = Following s2;
theorem :: CIRCCMB2:16
for S1,S2,S being non void Circuit-like non empty ManySortedSign st
S = S1+*S2 for A1 being non-empty Circuit of S1, A2 being non-empty Circuit of
S2 for A being non-empty Circuit of S st A1 tolerates A2 & A = A1+*A2 for s
being State of A for s1 being State of A1 st s1 = s|the carrier of S1 & s1 is
stable for s2 being State of A2 st s2 = s|the carrier of S2 & s2 is stable
holds s is stable;
theorem :: CIRCCMB2:17
for S1,S2,S being non void Circuit-like non empty
ManySortedSign st S = S1+*S2 for A1 being non-empty Circuit of S1, A2 being
non-empty Circuit of S2 for A being non-empty Circuit of S st A1 tolerates A2 &
A = A1+*A2 for s being State of A st s is stable holds (for s1 being State of
A1 st s1 = s|the carrier of S1 holds s1 is stable) & (for s2 being State of A2
st s2 = s|the carrier of S2 holds s2 is stable);
theorem :: CIRCCMB2:18
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 s1 being State of A1
, s2 being State of A2, s being State of A st s1 = s|the carrier of S1 & s2 = s
|the carrier of S2 & s1 is stable for n being Nat holds Following(s, n)|the
carrier of S2 = Following(s2, n);
theorem :: CIRCCMB2:19
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 n1,n2 being Nat for
s being State of A for s1 being State of A1, s2 being State of A2 st s1 = s|the
carrier of S1 & Following(s1, n1) is stable & s2 = Following(s, n1)|the carrier
of S2 & Following(s2, n2) is stable holds Following(s, n1+n2) is stable;
theorem :: CIRCCMB2:20
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 n1,n2 being Nat st (
for s being State of A1 holds Following(s, n1) is stable) & (for s being State
of A2 holds Following(s, n2) is stable) for s being State of A holds Following(
s, n1+n2) is stable;
theorem :: CIRCCMB2:21
for S1,S2,S being non void Circuit-like non empty
ManySortedSign st InputVertices S1 misses InnerVertices S2 & InputVertices S2
misses InnerVertices S1 & S = S1+*S2 for A1 being non-empty Circuit of S1, A2
being non-empty Circuit of S2 for A being non-empty Circuit of S st A1
tolerates A2 & A = A1+*A2 for s being State of A for s1 being State of A1 st s1
= s|the carrier of S1 for s2 being State of A2 st s2 = s|the carrier of S2
for n being natural Number holds
Following(s, n) = Following(s1, n)+*Following(s2, n);
theorem :: CIRCCMB2:22
for S1,S2,S being non void Circuit-like non empty
ManySortedSign st InputVertices S1 misses InnerVertices S2 & InputVertices S2
misses InnerVertices S1 & S = S1+*S2 for A1 being non-empty Circuit of S1, A2
being non-empty Circuit of S2 for A being non-empty Circuit of S st A1
tolerates A2 & A = A1+*A2 for n1,n2 being Nat, s being State of A for s1 being
State of A1 st s1 = s|the carrier of S1 for s2 being State of A2 st s2 = s|the
carrier of S2 & Following(s1, n1) is stable & Following(s2, n2) is stable holds
Following(s, max(n1,n2)) is stable;
theorem :: CIRCCMB2:23
for S1,S2,S being non void Circuit-like non empty ManySortedSign st
InputVertices S1 misses InnerVertices S2 & InputVertices S2 misses
InnerVertices S1 & S = S1+*S2 for A1 being non-empty Circuit of S1, A2 being
non-empty Circuit of S2 for A being non-empty Circuit of S st A1 tolerates A2 &
A = A1+*A2 for n being Nat, s being State of A for s1 being State of A1 st s1 =
s|the carrier of S1 for s2 being State of A2 st s2 = s|the carrier of S2 & (
Following(s1, n) is not stable or Following(s2, n) is not stable) holds
Following(s, n) is not stable;
theorem :: CIRCCMB2:24
for S1,S2,S being non void Circuit-like non empty ManySortedSign st
InputVertices S1 misses InnerVertices S2 & InputVertices S2 misses
InnerVertices S1 & S = S1+*S2 for A1 being non-empty Circuit of S1, A2 being
non-empty Circuit of S2 for A being non-empty Circuit of S st A1 tolerates A2 &
A = A1+*A2 for n1,n2 being Nat st (for s being State of A1 holds Following(s,
n1) is stable) & (for s being State of A2 holds Following(s, n2) is stable) for
s being State of A holds Following(s, max(n1,n2)) is stable;
scheme :: CIRCCMB2:sch 22
CIRCCMB29sch22 {S0, Sn() -> unsplit gate`1=arity gate`2isBoolean non void
strict non empty ManySortedSign, A0() -> Boolean gate`2=den strict Circuit of
S0(), An() -> Boolean gate`2=den strict Circuit of Sn(),
S(object,object) -> unsplit
gate`1=arity gate`2isBoolean non void strict non empty ManySortedSign,
A(object,object) -> object, h() -> ManySortedSet of NAT,
o0()-> object, o(object,object) -> object, n(Nat)-> Nat}:
for s being State of An() holds Following(s, n(0)+n(2)*n(1)) is stable
provided
for x being set, n being Nat holds A(x,n) is Boolean gate`2=den
strict Circuit of S(x,n) and
for s being State of A0() holds Following(s, n(0)) is stable and
for n being Nat, x being set for A being non-empty Circuit of S(x,n)
st x = h().(n) & A = A(x,n) for s being State of A holds Following(s, n(1)) is
stable and
ex f,g being ManySortedSet of NAT st Sn() = f.n(2) & An() = g.n(2) &
f.0 = S0() & g.0 = A0() & h().0 = o0() & for n being Nat, S being non empty
ManySortedSign, A1 being non-empty MSAlgebra over S for x being set, A2 being
non-empty MSAlgebra over S(x,n) st S = f.n & A1 = g.n & x = h().n & A2 = A(x,n)
holds f.(n+1) = S +* S(x,n) & g.(n+1) = A1 +* A2 & h().(n+1) = o(x,n) and
InnerVertices S0() is Relation & InputVertices S0() is without_pairs and
h().0 = o0() & o0() in InnerVertices S0() and
for n being Nat, x being set holds InnerVertices S(x,n) is Relation and
for n being Nat, x being set st x = h().(n) holds (InputVertices S(x
,n)) \ {x} is without_pairs and
for n being Nat, x being set st x = h().(n) holds h().(n+1) = o(x,n)
& x in InputVertices S(x,n) & o(x,n) in InnerVertices S(x,n);