Journal of Formalized Mathematics
Volume 14, 2002
University of Bialystok
Copyright (c) 2002 Association of Mizar Users

### Combining of Multi Cell Circuits

by
Grzegorz Bancerek,
Shin'nosuke Yamaguchi, and
Yasunari Shidama

MML identifier: CIRCCMB2
[ Mizar article, MML identifier index ]

```environ

vocabulary BOOLE, MCART_1, COMMACAT, AMI_1, FINSEQ_2, RELAT_1, FUNCT_1,
PARTFUN1, FUNCT_4, ZF_REFLE, QC_LANG1, PBOOLE, MSUALG_1, MSAFREE2,
LATTICES, FINSET_1, SQUARE_1, CIRCUIT1, CIRCUIT2, CIRCCOMB, FACIRC_1,
MARGREL1;
notation TARSKI, XBOOLE_0, NUMBERS, XREAL_0, NAT_1, MCART_1, COMMACAT,
FINSET_1, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2, FINSEQ_2, FUNCT_4,
LIMFUNC1, PBOOLE, STRUCT_0, MSUALG_1, MSAFREE2, CIRCUIT1, CIRCUIT2,
CIRCCOMB, FACIRC_1;
constructors COMMACAT, LIMFUNC1, CIRCUIT1, CIRCUIT2, FACIRC_1;
clusters RELAT_1, RELSET_1, FUNCT_1, MSUALG_1, STRUCT_0, PRE_CIRC, CIRCCOMB,
FACIRC_1, MEMBERED, NUMBERS, ORDINAL2;
requirements NUMERALS, SUBSET, BOOLE, ARITHM;

begin :: One gate circuits

definition
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 Nat 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 Nat
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 ::CircSch0
{S0() -> non empty ManySortedSign, o0()-> set,
S(set,set,set) -> non empty ManySortedSign,
o(set,set) -> set}:
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
{S(set,set,set) -> non empty ManySortedSign,
o(set,set) -> set, P[set,set,set],
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
{S0() -> non empty ManySortedSign, S(set,set,set) -> non empty ManySortedSign,
o(set,set) -> set, 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
{S0() -> non empty ManySortedSign, o0()-> set,
S(set,set,set) -> non empty ManySortedSign,
o(set,set) -> set, 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
{S0() -> non empty ManySortedSign, o0()-> set,
S(set,set,set) -> non empty ManySortedSign,
o(set,set) -> set, 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
{S0() -> non empty ManySortedSign, o0()-> set,
S(set,set,set) -> non empty ManySortedSign,
o(set,set) -> set, 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
{S0() -> non empty ManySortedSign, S(set,set,set) -> non empty ManySortedSign,
o0()-> set, o(set,set) -> set, 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
{S0() -> non empty ManySortedSign,
S(set,set) -> unsplit gate`1=arity gate`2isBoolean non void non empty
ManySortedSign,
o0()-> set, o(set,set) -> set, 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
{S0() -> non empty ManySortedSign, o0()-> set,
S(set,set,set) -> non empty ManySortedSign,
o(set,set) -> set, 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 :: Input of Many Cell Circuit

theorem :: CIRCCMB2:5
for f,g being Function st f tolerates g
holds rng (f+*g) = (rng f)\/(rng g);

theorem :: CIRCCMB2:6
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:7
for X being without_pairs set, Y being Relation
holds X \ Y = X;

theorem :: CIRCCMB2:8
for X being Relation, Y, Z being set st Z c= Y & Y \ Z is without_pairs
holds X \ Y = X \ Z;

theorem :: CIRCCMB2:9
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
{S0() -> unsplit gate`1=arity gate`2isBoolean non void non empty
ManySortedSign,
f(set) -> set, h() -> ManySortedSet of NAT,
S(set,set) -> unsplit gate`1=arity gate`2isBoolean non void non empty
ManySortedSign,
o(set,set) -> set}:
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
{Sn(set) -> unsplit gate`1=arity gate`2isBoolean non void non empty
ManySortedSign,
h() -> ManySortedSet of NAT,
S(set,set) -> unsplit gate`1=arity gate`2isBoolean non void non empty
ManySortedSign,
o(set,set) -> set}:
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 :: CircSch2
{S0() -> non empty ManySortedSign,
A0() -> non-empty MSAlgebra over S0(), o0()-> set,
S(set,set,set) -> non empty ManySortedSign, A(set,set,set,set) -> set,
o(set,set) -> set}:
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
{S(set,set,set) -> non empty ManySortedSign, A(set,set,set,set) -> set,
o(set,set) -> set, P[set,set,set,set],
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
{S(set,set,set) -> non empty ManySortedSign, A(set,set,set,set) -> set,
o(set,set) -> set,
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
{S0() -> non empty ManySortedSign, A0() -> non-empty MSAlgebra over S0(),
S(set,set,set) -> non empty ManySortedSign, A(set,set,set,set) -> set,
o(set,set) -> set,
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
{S0() -> non empty ManySortedSign,
A0() -> non-empty MSAlgebra over S0(), o0()-> set,
S(set,set,set) -> non empty ManySortedSign, A(set,set,set,set) -> set,
o(set,set) -> set, 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
{S0,Sn() -> non empty ManySortedSign, A0() -> non-empty MSAlgebra over S0(),
o0()-> set,
S(set,set,set) -> non empty ManySortedSign, A(set,set,set,set) -> set,
o(set,set) -> set, 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
{S0,Sn() -> non empty ManySortedSign, A0() -> non-empty MSAlgebra over S0(),
o0()-> set,
S(set,set,set) -> non empty ManySortedSign, A(set,set,set,set) -> set,
o(set,set) -> set, 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 :: attrCircuitExSch
{S0, Sn() -> unsplit gate`1=arity gate`2isBoolean non void strict
non empty ManySortedSign,
A0() -> Boolean gate`2=den strict Circuit of S0(),
S(set,set,set) -> non empty ManySortedSign,
A(set,set,set,set) -> set,
o0()-> set, o(set,set) -> set, 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 set 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
{S0, Sn() -> unsplit gate`1=arity gate`2isBoolean non void strict
non empty ManySortedSign,
A0() -> Boolean gate`2=den strict Circuit of S0(),
S(set,set) -> unsplit gate`1=arity gate`2isBoolean non void non empty
ManySortedSign,
A(set,set) -> set,
o0()-> set, o(set,set) -> set, 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
{S0() -> non empty ManySortedSign,
Sn() -> unsplit gate`1=arity gate`2isBoolean non void strict
non empty ManySortedSign,
A0() -> non-empty MSAlgebra over S0(), o0()-> set,
S(set,set,set) -> non empty ManySortedSign, A(set,set,set,set) -> set,
o(set,set) -> set, 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:10
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:11
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:12
for S1,S2,S being non void Circuit-like (non empty ManySortedSign)
st S1 tolerates S2 & 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:13
for S1,S2,S being non void Circuit-like (non empty ManySortedSign)
st S1 tolerates S2 & 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:14
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 Nat
holds Following(s, n)|the carrier of S1 = Following(s1, n);

theorem :: CIRCCMB2:15
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:16
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: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
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:18
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: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 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: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
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:21
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: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 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 Nat holds
Following(s, n) = Following(s1, n)+*Following(s2, n);

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 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: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 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:25
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
{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(set,set) -> unsplit gate`1=arity gate`2isBoolean non void strict
non empty ManySortedSign,
A(set,set) -> set,
h() -> ManySortedSet of NAT,
o0()-> set, o(set,set) -> set, 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);
```