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


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 ;
coherence
1GateCircuit (p,f) is Boolean by CIRCCOMB:61;
end;

theorem Th1: :: CIRCCMB2:1
for X being non empty finite set
for 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
proof end;

theorem :: CIRCCMB2:2
for X being non empty finite set
for 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
proof end;

theorem Th3: :: CIRCCMB2:3
for S being non empty non void Circuit-like ManySortedSign
for A being non-empty Circuit of S
for s being State of A st s is stable holds
for n being natural Number holds Following (s,n) = s
proof end;

theorem Th4: :: CIRCCMB2:4
for S being non empty non void Circuit-like ManySortedSign
for A being non-empty Circuit of S
for s being State of A
for n1, n2 being natural Number st Following (s,n1) is stable & n1 <= n2 holds
Following (s,n2) = Following (s,n1)
proof end;

scheme :: CIRCCMB2:sch 1
CIRCCMB29sch1{ F1() -> non empty ManySortedSign , F2() -> object , F3( object , object , object ) -> non empty ManySortedSign , F4( object , object ) -> object } :
ex f, h being ManySortedSet of NAT st
( f . 0 = F1() & h . 0 = F2() & ( for n being Nat
for S being non empty ManySortedSign
for x being set st S = f . n & x = h . n holds
( f . (n + 1) = F3(S,x,n) & h . (n + 1) = F4(x,n) ) ) )
proof end;

scheme :: CIRCCMB2:sch 2
CIRCCMB29sch2{ F1( object , object , object ) -> non empty ManySortedSign , F2( object , object ) -> object , P1[ object , object , object ], F3() -> ManySortedSet of NAT , F4() -> ManySortedSet of NAT } :
for n being Nat ex S being non empty ManySortedSign st
( S = F3() . n & P1[S,F4() . n,n] )
provided
A1: ex S being non empty ManySortedSign ex x being set st
( S = F3() . 0 & x = F4() . 0 & P1[S,x, 0 ] ) and
A2: for n being Nat
for S being non empty ManySortedSign
for x being set st S = F3() . n & x = F4() . n holds
( F3() . (n + 1) = F1(S,x,n) & F4() . (n + 1) = F2(x,n) ) and
A3: for n being Nat
for S being non empty ManySortedSign
for x being set st S = F3() . n & x = F4() . n & P1[S,x,n] holds
P1[F1(S,x,n),F2(x,n),n + 1]
proof end;

defpred S1[ object , object , object ] means verum;

scheme :: CIRCCMB2:sch 3
CIRCCMB29sch3{ F1() -> non empty ManySortedSign , F2( object , object , object ) -> non empty ManySortedSign , F3( object , object ) -> object , F4() -> ManySortedSet of NAT , F5() -> ManySortedSet of NAT } :
for n being Nat
for x being set st x = F5() . n holds
F5() . (n + 1) = F3(x,n)
provided
A1: F4() . 0 = F1() and
A2: for n being Nat
for S being non empty ManySortedSign
for x being set st S = F4() . n & x = F5() . n holds
( F4() . (n + 1) = F2(S,x,n) & F5() . (n + 1) = F3(x,n) )
proof end;

scheme :: CIRCCMB2:sch 4
CIRCCMB29sch4{ F1() -> non empty ManySortedSign , F2() -> object , F3( object , object , object ) -> non empty ManySortedSign , F4( object , object ) -> object , F5() -> Nat } :
ex S being non empty ManySortedSign ex f, h being ManySortedSet of NAT st
( S = f . F5() & f . 0 = F1() & h . 0 = F2() & ( for n being Nat
for S being non empty ManySortedSign
for x being set st S = f . n & x = h . n holds
( f . (n + 1) = F3(S,x,n) & h . (n + 1) = F4(x,n) ) ) )
proof end;

scheme :: CIRCCMB2:sch 5
CIRCCMB29sch5{ F1() -> non empty ManySortedSign , F2() -> object , F3( object , object , object ) -> non empty ManySortedSign , F4( object , object ) -> object , F5() -> Nat } :
for S1, S2 being non empty ManySortedSign st ex f, h being ManySortedSet of NAT st
( S1 = f . F5() & f . 0 = F1() & h . 0 = F2() & ( for n being Nat
for S being non empty ManySortedSign
for x being set st S = f . n & x = h . n holds
( f . (n + 1) = F3(S,x,n) & h . (n + 1) = F4(x,n) ) ) ) & ex f, h being ManySortedSet of NAT st
( S2 = f . F5() & f . 0 = F1() & h . 0 = F2() & ( for n being Nat
for S being non empty ManySortedSign
for x being set st S = f . n & x = h . n holds
( f . (n + 1) = F3(S,x,n) & h . (n + 1) = F4(x,n) ) ) ) holds
S1 = S2
proof end;

scheme :: CIRCCMB2:sch 6
CIRCCMB29sch6{ F1() -> non empty ManySortedSign , F2() -> object , F3( object , object , object ) -> non empty ManySortedSign , F4( object , object ) -> object , F5() -> Nat } :
( ex S being non empty ManySortedSign ex f, h being ManySortedSet of NAT st
( S = f . F5() & f . 0 = F1() & h . 0 = F2() & ( for n being Nat
for S being non empty ManySortedSign
for x being set st S = f . n & x = h . n holds
( f . (n + 1) = F3(S,x,n) & h . (n + 1) = F4(x,n) ) ) ) & ( for S1, S2 being non empty ManySortedSign st ex f, h being ManySortedSet of NAT st
( S1 = f . F5() & f . 0 = F1() & h . 0 = F2() & ( for n being Nat
for S being non empty ManySortedSign
for x being set st S = f . n & x = h . n holds
( f . (n + 1) = F3(S,x,n) & h . (n + 1) = F4(x,n) ) ) ) & ex f, h being ManySortedSet of NAT st
( S2 = f . F5() & f . 0 = F1() & h . 0 = F2() & ( for n being Nat
for S being non empty ManySortedSign
for x being set st S = f . n & x = h . n holds
( f . (n + 1) = F3(S,x,n) & h . (n + 1) = F4(x,n) ) ) ) holds
S1 = S2 ) )
proof end;

scheme :: CIRCCMB2:sch 7
CIRCCMB29sch7{ F1() -> non empty ManySortedSign , F2( object , object , object ) -> non empty ManySortedSign , F3() -> object , F4( object , object ) -> object , F5() -> Nat } :
ex S being non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign ex f, h being ManySortedSet of NAT st
( S = f . F5() & f . 0 = F1() & h . 0 = F3() & ( for n being Nat
for S being non empty ManySortedSign
for x being set st S = f . n & x = h . n holds
( f . (n + 1) = F2(S,x,n) & h . (n + 1) = F4(x,n) ) ) )
provided
A1: ( F1() is unsplit & F1() is gate`1=arity & F1() is gate`2isBoolean & not F1() is void & not F1() is empty & F1() is strict ) and
A2: for S being non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign
for x being set
for n being Nat holds
( F2(S,x,n) is unsplit & F2(S,x,n) is gate`1=arity & F2(S,x,n) is gate`2isBoolean & not F2(S,x,n) is void & not F2(S,x,n) is empty & F2(S,x,n) is strict )
proof end;

scheme :: CIRCCMB2:sch 8
CIRCCMB29sch8{ F1() -> non empty ManySortedSign , F2( object , object ) -> non empty non void unsplit gate`1=arity gate`2isBoolean ManySortedSign , F3() -> object , F4( object , object ) -> object , F5() -> Nat } :
ex S being non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign ex f, h being ManySortedSet of NAT st
( S = f . F5() & f . 0 = F1() & h . 0 = F3() & ( for n being Nat
for S being non empty ManySortedSign
for x being set st S = f . n & x = h . n holds
( f . (n + 1) = S +* F2(x,n) & h . (n + 1) = F4(x,n) ) ) )
provided
A1: ( F1() is unsplit & F1() is gate`1=arity & F1() is gate`2isBoolean & not F1() is void & not F1() is empty & F1() is strict )
proof end;

scheme :: CIRCCMB2:sch 9
CIRCCMB29sch9{ F1() -> non empty ManySortedSign , F2() -> object , F3( object , object , object ) -> non empty ManySortedSign , F4( object , object ) -> object , F5() -> Nat } :
for S1, S2 being non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign st ex f, h being ManySortedSet of NAT st
( S1 = f . F5() & f . 0 = F1() & h . 0 = F2() & ( for n being Nat
for S being non empty ManySortedSign
for x being set st S = f . n & x = h . n holds
( f . (n + 1) = F3(S,x,n) & h . (n + 1) = F4(x,n) ) ) ) & ex f, h being ManySortedSet of NAT st
( S2 = f . F5() & f . 0 = F1() & h . 0 = F2() & ( for n being Nat
for S being non empty ManySortedSign
for x being set st S = f . n & x = h . n holds
( f . (n + 1) = F3(S,x,n) & h . (n + 1) = F4(x,n) ) ) ) holds
S1 = S2
proof end;

theorem Th5: :: 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))
proof end;

theorem Th6: :: CIRCCMB2:6
for X being without_pairs set
for Y being Relation holds X \ Y = X
proof end;

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

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

scheme :: CIRCCMB2:sch 10
CIRCCMB29sch10{ F1() -> non empty non void unsplit gate`1=arity gate`2isBoolean ManySortedSign , F2( object ) -> object , F3() -> ManySortedSet of NAT , F4( object , object ) -> non empty non void unsplit gate`1=arity gate`2isBoolean ManySortedSign , F5( object , object ) -> object } :
for n being Nat ex S1, S2 being non empty non void unsplit gate`1=arity gate`2isBoolean ManySortedSign st
( S1 = F2(n) & S2 = F2((n + 1)) & InputVertices S2 = (InputVertices S1) \/ ((InputVertices F4((F3() . n),n)) \ {(F3() . n)}) & InnerVertices S1 is Relation & InputVertices S1 is without_pairs )
provided
A1: InnerVertices F1() is Relation and
A2: InputVertices F1() is without_pairs and
A3: ( F2(0) = F1() & F3() . 0 in InnerVertices F1() ) and
A4: for n being Nat
for x being set holds InnerVertices F4(x,n) is Relation and
A5: for n being Nat
for x being set st x = F3() . n holds
(InputVertices F4(x,n)) \ {x} is without_pairs and
A6: for n being Nat
for S being non empty ManySortedSign
for x being set st S = F2(n) & x = F3() . n holds
( F2((n + 1)) = S +* F4(x,n) & F3() . (n + 1) = F5(x,n) & x in InputVertices F4(x,n) & F5(x,n) in InnerVertices F4(x,n) )
proof end;

scheme :: CIRCCMB2:sch 11
CIRCCMB29sch11{ F1( set ) -> non empty non void unsplit gate`1=arity gate`2isBoolean ManySortedSign , F2() -> ManySortedSet of NAT , F3( object , object ) -> non empty non void unsplit gate`1=arity gate`2isBoolean ManySortedSign , F4( object , object ) -> object } :
for n being Nat holds
( InputVertices F1((n + 1)) = (InputVertices F1(n)) \/ ((InputVertices F3((F2() . n),n)) \ {(F2() . n)}) & InnerVertices F1(n) is Relation & InputVertices F1(n) is without_pairs )
provided
A1: InnerVertices F1(0) is Relation and
A2: InputVertices F1(0) is without_pairs and
A3: F2() . 0 in InnerVertices F1(0) and
A4: for n being Nat
for x being set holds InnerVertices F3(x,n) is Relation and
A5: for n being Nat
for x being set st x = F2() . n holds
(InputVertices F3(x,n)) \ {x} is without_pairs and
A6: for n being Nat
for S being non empty ManySortedSign
for x being set st S = F1(n) & x = F2() . n holds
( F1((n + 1)) = S +* F3(x,n) & F2() . (n + 1) = F4(x,n) & x in InputVertices F3(x,n) & F4(x,n) in InnerVertices F3(x,n) )
proof end;

scheme :: CIRCCMB2:sch 12
CIRCCMB29sch12{ F1() -> non empty ManySortedSign , F2() -> non-empty MSAlgebra over F1(), F3() -> object , F4( object , object , object ) -> non empty ManySortedSign , F5( object , object , object , object ) -> object , F6( object , object ) -> object } :
ex f, g, h being ManySortedSet of NAT st
( f . 0 = F1() & g . 0 = F2() & h . 0 = F3() & ( for n being Nat
for S being non empty ManySortedSign
for 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) = F4(S,x,n) & g . (n + 1) = F5(S,A,x,n) & h . (n + 1) = F6(x,n) ) ) )
proof end;

scheme :: CIRCCMB2:sch 13
CIRCCMB29sch13{ F1( set , set , set ) -> non empty ManySortedSign , F2( object , object , object , object ) -> object , F3( object , object ) -> object , P1[ object , object , object , object ], F4() -> ManySortedSet of NAT , F5() -> ManySortedSet of NAT , F6() -> ManySortedSet of NAT } :
for n being Nat ex S being non empty ManySortedSign ex A being non-empty MSAlgebra over S st
( S = F4() . n & A = F5() . n & P1[S,A,F6() . n,n] )
provided
A1: ex S being non empty ManySortedSign ex A being non-empty MSAlgebra over S ex x being set st
( S = F4() . 0 & A = F5() . 0 & x = F6() . 0 & P1[S,A,x, 0 ] ) and
A2: for n being Nat
for S being non empty ManySortedSign
for A being non-empty MSAlgebra over S
for x being set st S = F4() . n & A = F5() . n & x = F6() . n holds
( F4() . (n + 1) = F1(S,x,n) & F5() . (n + 1) = F2(S,A,x,n) & F6() . (n + 1) = F3(x,n) ) and
A3: for n being Nat
for S being non empty ManySortedSign
for A being non-empty MSAlgebra over S
for x being set st S = F4() . n & A = F5() . n & x = F6() . n & P1[S,A,x,n] holds
P1[F1(S,x,n),F2(S,A,x,n),F3(x,n),n + 1] and
A4: for S being non empty ManySortedSign
for A being non-empty MSAlgebra over S
for x being set
for n being Nat holds F2(S,A,x,n) is non-empty MSAlgebra over F1(S,x,n)
proof end;

defpred S2[ object , object , object , object ] means verum;

scheme :: CIRCCMB2:sch 14
CIRCCMB29sch14{ F1( set , set , set ) -> non empty ManySortedSign , F2( object , object , object , object ) -> object , F3( object , object ) -> object , F4() -> ManySortedSet of NAT , F5() -> ManySortedSet of NAT , F6() -> ManySortedSet of NAT , F7() -> ManySortedSet of NAT , F8() -> ManySortedSet of NAT , F9() -> ManySortedSet of NAT } :
( F4() = F5() & F6() = F7() & F8() = F9() )
provided
A1: ex S being non empty ManySortedSign ex A being non-empty MSAlgebra over S st
( S = F4() . 0 & A = F6() . 0 ) and
A2: ( F4() . 0 = F5() . 0 & F6() . 0 = F7() . 0 & F8() . 0 = F9() . 0 ) and
A3: for n being Nat
for S being non empty ManySortedSign
for A being non-empty MSAlgebra over S
for x being set st S = F4() . n & A = F6() . n & x = F8() . n holds
( F4() . (n + 1) = F1(S,x,n) & F6() . (n + 1) = F2(S,A,x,n) & F8() . (n + 1) = F3(x,n) ) and
A4: for n being Nat
for S being non empty ManySortedSign
for A being non-empty MSAlgebra over S
for x being set st S = F5() . n & A = F7() . n & x = F9() . n holds
( F5() . (n + 1) = F1(S,x,n) & F7() . (n + 1) = F2(S,A,x,n) & F9() . (n + 1) = F3(x,n) ) and
A5: for S being non empty ManySortedSign
for A being non-empty MSAlgebra over S
for x being set
for n being Nat holds F2(S,A,x,n) is non-empty MSAlgebra over F1(S,x,n)
proof end;

scheme :: CIRCCMB2:sch 15
CIRCCMB29sch15{ F1() -> non empty ManySortedSign , F2() -> non-empty MSAlgebra over F1(), F3( object , object , object ) -> non empty ManySortedSign , F4( object , object , object , object ) -> object , F5( object , object ) -> object , F6() -> ManySortedSet of NAT , F7() -> ManySortedSet of NAT , F8() -> ManySortedSet of NAT } :
for n being Nat
for S being non empty ManySortedSign
for x being set st S = F6() . n & x = F8() . n holds
( F6() . (n + 1) = F3(S,x,n) & F8() . (n + 1) = F5(x,n) )
provided
A1: ( F6() . 0 = F1() & F7() . 0 = F2() ) and
A2: for n being Nat
for S being non empty ManySortedSign
for A being non-empty MSAlgebra over S
for x being set st S = F6() . n & A = F7() . n & x = F8() . n holds
( F6() . (n + 1) = F3(S,x,n) & F7() . (n + 1) = F4(S,A,x,n) & F8() . (n + 1) = F5(x,n) ) and
A3: for S being non empty ManySortedSign
for A being non-empty MSAlgebra over S
for x being set
for n being Nat holds F4(S,A,x,n) is non-empty MSAlgebra over F3(S,x,n)
proof end;

scheme :: CIRCCMB2:sch 16
CIRCCMB29sch16{ F1() -> non empty ManySortedSign , F2() -> non-empty MSAlgebra over F1(), F3() -> object , F4( object , object , object ) -> non empty ManySortedSign , F5( object , object , object , object ) -> object , F6( object , object ) -> object , F7() -> Nat } :
ex S being non empty ManySortedSign ex A being non-empty MSAlgebra over S ex f, g, h being ManySortedSet of NAT st
( S = f . F7() & A = g . F7() & f . 0 = F1() & g . 0 = F2() & h . 0 = F3() & ( for n being Nat
for S being non empty ManySortedSign
for 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) = F4(S,x,n) & g . (n + 1) = F5(S,A,x,n) & h . (n + 1) = F6(x,n) ) ) )
provided
A1: for S being non empty ManySortedSign
for A being non-empty MSAlgebra over S
for x being set
for n being Nat holds F5(S,A,x,n) is non-empty MSAlgebra over F4(S,x,n)
proof end;

scheme :: CIRCCMB2:sch 17
CIRCCMB29sch17{ F1() -> non empty ManySortedSign , F2() -> non empty ManySortedSign , F3() -> non-empty MSAlgebra over F1(), F4() -> object , F5( object , object , object ) -> non empty ManySortedSign , F6( object , object , object , object ) -> object , F7( object , object ) -> object , F8() -> Nat } :
ex A being non-empty MSAlgebra over F2() ex f, g, h being ManySortedSet of NAT st
( F2() = f . F8() & A = g . F8() & f . 0 = F1() & g . 0 = F3() & h . 0 = F4() & ( for n being Nat
for S being non empty ManySortedSign
for 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) = F5(S,x,n) & g . (n + 1) = F6(S,A,x,n) & h . (n + 1) = F7(x,n) ) ) )
provided
A1: ex f, h being ManySortedSet of NAT st
( F2() = f . F8() & f . 0 = F1() & h . 0 = F4() & ( for n being Nat
for S being non empty ManySortedSign
for x being set st S = f . n & x = h . n holds
( f . (n + 1) = F5(S,x,n) & h . (n + 1) = F7(x,n) ) ) ) and
A2: for S being non empty ManySortedSign
for A being non-empty MSAlgebra over S
for x being set
for n being Nat holds F6(S,A,x,n) is non-empty MSAlgebra over F5(S,x,n)
proof end;

scheme :: CIRCCMB2:sch 18
CIRCCMB29sch18{ F1() -> non empty ManySortedSign , F2() -> non empty ManySortedSign , F3() -> non-empty MSAlgebra over F1(), F4() -> object , F5( object , object , object ) -> non empty ManySortedSign , F6( object , object , object , object ) -> object , F7( object , object ) -> object , F8() -> Nat } :
for A1, A2 being non-empty MSAlgebra over F2() st ex f, g, h being ManySortedSet of NAT st
( F2() = f . F8() & A1 = g . F8() & f . 0 = F1() & g . 0 = F3() & h . 0 = F4() & ( for n being Nat
for S being non empty ManySortedSign
for 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) = F5(S,x,n) & g . (n + 1) = F6(S,A,x,n) & h . (n + 1) = F7(x,n) ) ) ) & ex f, g, h being ManySortedSet of NAT st
( F2() = f . F8() & A2 = g . F8() & f . 0 = F1() & g . 0 = F3() & h . 0 = F4() & ( for n being Nat
for S being non empty ManySortedSign
for 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) = F5(S,x,n) & g . (n + 1) = F6(S,A,x,n) & h . (n + 1) = F7(x,n) ) ) ) holds
A1 = A2
provided
A1: for S being non empty ManySortedSign
for A being non-empty MSAlgebra over S
for x being set
for n being Nat holds F6(S,A,x,n) is non-empty MSAlgebra over F5(S,x,n)
proof end;

scheme :: CIRCCMB2:sch 19
CIRCCMB29sch19{ F1() -> non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign , F2() -> non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign , F3() -> strict gate`2=den Boolean Circuit of F1(), F4( object , object , object ) -> non empty ManySortedSign , F5( object , object , object , object ) -> object , F6() -> object , F7( object , object ) -> object , F8() -> Nat } :
ex A being strict gate`2=den Boolean Circuit of F2() ex f, g, h being ManySortedSet of NAT st
( F2() = f . F8() & A = g . F8() & f . 0 = F1() & g . 0 = F3() & h . 0 = F6() & ( for n being Nat
for S being non empty ManySortedSign
for 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) = F4(S,x,n) & g . (n + 1) = F5(S,A,x,n) & h . (n + 1) = F7(x,n) ) ) )
provided
A1: for S being non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign
for x being set
for n being Nat holds
( F4(S,x,n) is unsplit & F4(S,x,n) is gate`1=arity & F4(S,x,n) is gate`2isBoolean & not F4(S,x,n) is void & F4(S,x,n) is strict ) and
A2: ex f, h being ManySortedSet of NAT st
( F2() = f . F8() & f . 0 = F1() & h . 0 = F6() & ( for n being Nat
for S being non empty ManySortedSign
for x being set st S = f . n & x = h . n holds
( f . (n + 1) = F4(S,x,n) & h . (n + 1) = F7(x,n) ) ) ) and
A3: for S being non empty ManySortedSign
for A being non-empty MSAlgebra over S
for x being set
for n being Nat holds F5(S,A,x,n) is non-empty MSAlgebra over F4(S,x,n) and
A4: for S, S1 being non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign
for A being strict gate`2=den Boolean Circuit of S
for x being set
for n being Nat st S1 = F4(S,x,n) holds
F5(S,A,x,n) is strict gate`2=den Boolean Circuit of S1
proof end;

definition
let S be non empty ManySortedSign ;
let A be object ;
assume A1: A is non-empty MSAlgebra over S ;
func MSAlg (A,S) -> non-empty MSAlgebra over S means :Def1: :: CIRCCMB2:def 1
it = A;
existence
ex b1 being non-empty MSAlgebra over S st b1 = A by A1;
uniqueness
for b1, b2 being non-empty MSAlgebra over S st b1 = A & b2 = A holds
b1 = b2 ;
end;

:: deftheorem Def1 defines MSAlg CIRCCMB2:def 1 :
for S being non empty ManySortedSign
for A being object st A is non-empty MSAlgebra over S holds
for b3 being non-empty MSAlgebra over S holds
( b3 = MSAlg (A,S) iff b3 = A );

scheme :: CIRCCMB2:sch 20
CIRCCMB29sch20{ F1() -> non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign , F2() -> non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign , F3() -> strict gate`2=den Boolean Circuit of F1(), F4( object , object ) -> non empty non void unsplit gate`1=arity gate`2isBoolean ManySortedSign , F5( object , object ) -> object , F6() -> object , F7( object , object ) -> object , F8() -> Nat } :
ex A being strict gate`2=den Boolean Circuit of F2() ex f, g, h being ManySortedSet of NAT st
( F2() = f . F8() & A = g . F8() & f . 0 = F1() & g . 0 = F3() & h . 0 = F6() & ( for n being Nat
for S being non empty ManySortedSign
for A1 being non-empty MSAlgebra over S
for x being set
for A2 being non-empty MSAlgebra over F4(x,n) st S = f . n & A1 = g . n & x = h . n & A2 = F5(x,n) holds
( f . (n + 1) = S +* F4(x,n) & g . (n + 1) = A1 +* A2 & h . (n + 1) = F7(x,n) ) ) )
provided
A1: ex f, h being ManySortedSet of NAT st
( F2() = f . F8() & f . 0 = F1() & h . 0 = F6() & ( for n being Nat
for S being non empty ManySortedSign
for x being set st S = f . n & x = h . n holds
( f . (n + 1) = S +* F4(x,n) & h . (n + 1) = F7(x,n) ) ) ) and
A2: for x being set
for n being Nat holds F5(x,n) is strict gate`2=den Boolean Circuit of F4(x,n)
proof end;

scheme :: CIRCCMB2:sch 21
CIRCCMB29sch21{ F1() -> non empty ManySortedSign , F2() -> non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign , F3() -> non-empty MSAlgebra over F1(), F4() -> object , F5( object , object , object ) -> non empty ManySortedSign , F6( object , object , object , object ) -> object , F7( object , object ) -> object , F8() -> Nat } :
for A1, A2 being strict gate`2=den Boolean Circuit of F2() st ex f, g, h being ManySortedSet of NAT st
( F2() = f . F8() & A1 = g . F8() & f . 0 = F1() & g . 0 = F3() & h . 0 = F4() & ( for n being Nat
for S being non empty ManySortedSign
for 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) = F5(S,x,n) & g . (n + 1) = F6(S,A,x,n) & h . (n + 1) = F7(x,n) ) ) ) & ex f, g, h being ManySortedSet of NAT st
( F2() = f . F8() & A2 = g . F8() & f . 0 = F1() & g . 0 = F3() & h . 0 = F4() & ( for n being Nat
for S being non empty ManySortedSign
for 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) = F5(S,x,n) & g . (n + 1) = F6(S,A,x,n) & h . (n + 1) = F7(x,n) ) ) ) holds
A1 = A2
provided
A1: for S being non empty ManySortedSign
for A being non-empty MSAlgebra over S
for x being set
for n being Nat holds F6(S,A,x,n) is non-empty MSAlgebra over F5(S,x,n)
proof end;

theorem :: CIRCCMB2:9
for S1, S2, S being non empty non void Circuit-like ManySortedSign st InnerVertices S1 misses InputVertices S2 & S = S1 +* S2 holds
for C1 being non-empty Circuit of S1
for C2 being non-empty Circuit of S2
for C being non-empty Circuit of S st C1 tolerates C2 & C = C1 +* C2 holds
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
proof end;

theorem Th10: :: CIRCCMB2:10
for S1, S2, S being non empty non void Circuit-like ManySortedSign st InputVertices S1 misses InnerVertices S2 & S = S1 +* S2 holds
for C1 being non-empty Circuit of S1
for C2 being non-empty Circuit of S2
for C being non-empty Circuit of S st C1 tolerates C2 & C = C1 +* C2 holds
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
proof end;

theorem :: CIRCCMB2:11
for S1, S2, S being non empty non void Circuit-like ManySortedSign st InnerVertices S1 misses InputVertices S2 & S = S1 +* S2 holds
for C1 being non-empty Circuit of S1
for C2 being non-empty Circuit of S2
for C being non-empty Circuit of S st C1 tolerates C2 & C = C1 +* C2 holds
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
proof end;

theorem :: CIRCCMB2:12
for S1, S2, S being non empty non void Circuit-like ManySortedSign st InputVertices S1 misses InnerVertices S2 & S = S1 +* S2 holds
for C1 being non-empty Circuit of S1
for C2 being non-empty Circuit of S2
for C being non-empty Circuit of S st C1 tolerates C2 & C = C1 +* C2 holds
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
proof end;

theorem Th13: :: CIRCCMB2:13
for S1, S2, S being non empty non void Circuit-like ManySortedSign st InputVertices S1 misses InnerVertices S2 & S = S1 +* S2 holds
for A1 being non-empty Circuit of S1
for A2 being non-empty Circuit of S2
for A being non-empty Circuit of S st A1 tolerates A2 & A = A1 +* A2 holds
for s being State of A
for s1 being State of A1 st s1 = s | the carrier of S1 holds
for n being natural Number holds (Following (s,n)) | the carrier of S1 = Following (s1,n)
proof end;

theorem Th14: :: CIRCCMB2:14
for S1, S2, S being non empty non void Circuit-like ManySortedSign st InputVertices S2 misses InnerVertices S1 & S = S1 +* S2 holds
for A1 being non-empty Circuit of S1
for A2 being non-empty Circuit of S2
for A being non-empty Circuit of S st A1 tolerates A2 & A = A1 +* A2 holds
for s being State of A
for s2 being State of A2 st s2 = s | the carrier of S2 holds
for n being Nat holds (Following (s,n)) | the carrier of S2 = Following (s2,n)
proof end;

theorem Th15: :: CIRCCMB2:15
for S1, S2, S being non empty non void Circuit-like ManySortedSign st InputVertices S1 misses InnerVertices S2 & S = S1 +* S2 holds
for A1 being non-empty Circuit of S1
for A2 being non-empty Circuit of S2
for A being non-empty Circuit of S st A1 tolerates A2 & A = A1 +* A2 holds
for s being State of A
for s1 being State of A1 st s1 = s | the carrier of S1 & s1 is stable holds
for s2 being State of A2 st s2 = s | the carrier of S2 holds
(Following s) | the carrier of S2 = Following s2
proof end;

theorem :: CIRCCMB2:16
for S1, S2, S being non empty non void Circuit-like ManySortedSign st S = S1 +* S2 holds
for A1 being non-empty Circuit of S1
for A2 being non-empty Circuit of S2
for A being non-empty Circuit of S st A1 tolerates A2 & A = A1 +* A2 holds
for s being State of A
for s1 being State of A1 st s1 = s | the carrier of S1 & s1 is stable holds
for s2 being State of A2 st s2 = s | the carrier of S2 & s2 is stable holds
s is stable
proof end;

theorem Th17: :: CIRCCMB2:17
for S1, S2, S being non empty non void Circuit-like ManySortedSign st S = S1 +* S2 holds
for A1 being non-empty Circuit of S1
for A2 being non-empty Circuit of S2
for A being non-empty Circuit of S st A1 tolerates A2 & A = A1 +* A2 holds
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 ) )
proof end;

theorem Th18: :: CIRCCMB2:18
for S1, S2, S being non empty non void Circuit-like ManySortedSign st InputVertices S1 misses InnerVertices S2 & S = S1 +* S2 holds
for A1 being non-empty Circuit of S1
for A2 being non-empty Circuit of S2
for A being non-empty Circuit of S st A1 tolerates A2 & A = A1 +* A2 holds
for s1 being State of A1
for s2 being State of A2
for s being State of A st s1 = s | the carrier of S1 & s2 = s | the carrier of S2 & s1 is stable holds
for n being Nat holds (Following (s,n)) | the carrier of S2 = Following (s2,n)
proof end;

theorem Th19: :: CIRCCMB2:19
for S1, S2, S being non empty non void Circuit-like ManySortedSign st InputVertices S1 misses InnerVertices S2 & S = S1 +* S2 holds
for A1 being non-empty Circuit of S1
for A2 being non-empty Circuit of S2
for A being non-empty Circuit of S st A1 tolerates A2 & A = A1 +* A2 holds
for n1, n2 being Nat
for s being State of A
for s1 being State of A1
for s2 being State of A2 st s1 = s | the carrier of S1 & 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
proof end;

theorem Th20: :: CIRCCMB2:20
for S1, S2, S being non empty non void Circuit-like ManySortedSign st InputVertices S1 misses InnerVertices S2 & S = S1 +* S2 holds
for A1 being non-empty Circuit of S1
for A2 being non-empty Circuit of S2
for A being non-empty Circuit of S st A1 tolerates A2 & A = A1 +* A2 holds
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 ) holds
for s being State of A holds Following (s,(n1 + n2)) is stable
proof end;

theorem Th21: :: CIRCCMB2:21
for S1, S2, S being non empty non void Circuit-like ManySortedSign st InputVertices S1 misses InnerVertices S2 & InputVertices S2 misses InnerVertices S1 & S = S1 +* S2 holds
for A1 being non-empty Circuit of S1
for A2 being non-empty Circuit of S2
for A being non-empty Circuit of S st A1 tolerates A2 & A = A1 +* A2 holds
for s being State of A
for s1 being State of A1 st s1 = s | the carrier of S1 holds
for s2 being State of A2 st s2 = s | the carrier of S2 holds
for n being natural Number holds Following (s,n) = (Following (s1,n)) +* (Following (s2,n))
proof end;

theorem Th22: :: CIRCCMB2:22
for S1, S2, S being non empty non void Circuit-like ManySortedSign st InputVertices S1 misses InnerVertices S2 & InputVertices S2 misses InnerVertices S1 & S = S1 +* S2 holds
for A1 being non-empty Circuit of S1
for A2 being non-empty Circuit of S2
for A being non-empty Circuit of S st A1 tolerates A2 & A = A1 +* A2 holds
for n1, n2 being Nat
for s being State of A
for s1 being State of A1 st s1 = s | the carrier of S1 holds
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
proof end;

theorem :: CIRCCMB2:23
for S1, S2, S being non empty non void Circuit-like ManySortedSign st InputVertices S1 misses InnerVertices S2 & InputVertices S2 misses InnerVertices S1 & S = S1 +* S2 holds
for A1 being non-empty Circuit of S1
for A2 being non-empty Circuit of S2
for A being non-empty Circuit of S st A1 tolerates A2 & A = A1 +* A2 holds
for n being Nat
for s being State of A
for s1 being State of A1 st s1 = s | the carrier of S1 holds
for s2 being State of A2 st s2 = s | the carrier of S2 & ( not Following (s1,n) is stable or not Following (s2,n) is stable ) holds
not Following (s,n) is stable
proof end;

theorem :: CIRCCMB2:24
for S1, S2, S being non empty non void Circuit-like ManySortedSign st InputVertices S1 misses InnerVertices S2 & InputVertices S2 misses InnerVertices S1 & S = S1 +* S2 holds
for A1 being non-empty Circuit of S1
for A2 being non-empty Circuit of S2
for A being non-empty Circuit of S st A1 tolerates A2 & A = A1 +* A2 holds
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 ) holds
for s being State of A holds Following (s,(max (n1,n2))) is stable
proof end;

scheme :: CIRCCMB2:sch 22
CIRCCMB29sch22{ F1() -> non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign , F2() -> non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign , F3() -> strict gate`2=den Boolean Circuit of F1(), F4() -> strict gate`2=den Boolean Circuit of F2(), F5( object , object ) -> non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign , F6( object , object ) -> object , F7() -> ManySortedSet of NAT , F8() -> object , F9( object , object ) -> object , F10( Nat) -> Nat } :
for s being State of F4() holds Following (s,(F10(0) + (F10(2) * F10(1)))) is stable
provided
A1: for x being set
for n being Nat holds F6(x,n) is strict gate`2=den Boolean Circuit of F5(x,n) and
A2: for s being State of F3() holds Following (s,F10(0)) is stable and
A3: for n being Nat
for x being set
for A being non-empty Circuit of F5(x,n) st x = F7() . n & A = F6(x,n) holds
for s being State of A holds Following (s,F10(1)) is stable and
A4: ex f, g being ManySortedSet of NAT st
( F2() = f . F10(2) & F4() = g . F10(2) & f . 0 = F1() & g . 0 = F3() & F7() . 0 = F8() & ( for n being Nat
for S being non empty ManySortedSign
for A1 being non-empty MSAlgebra over S
for x being set
for A2 being non-empty MSAlgebra over F5(x,n) st S = f . n & A1 = g . n & x = F7() . n & A2 = F6(x,n) holds
( f . (n + 1) = S +* F5(x,n) & g . (n + 1) = A1 +* A2 & F7() . (n + 1) = F9(x,n) ) ) ) and
A5: ( InnerVertices F1() is Relation & InputVertices F1() is without_pairs ) and
A6: ( F7() . 0 = F8() & F8() in InnerVertices F1() ) and
A7: for n being Nat
for x being set holds InnerVertices F5(x,n) is Relation and
A8: for n being Nat
for x being set st x = F7() . n holds
(InputVertices F5(x,n)) \ {x} is without_pairs and
A9: for n being Nat
for x being set st x = F7() . n holds
( F7() . (n + 1) = F9(x,n) & x in InputVertices F5(x,n) & F9(x,n) in InnerVertices F5(x,n) )
proof end;