:: 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);