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