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

::

:: Received March 22, 2002

:: Copyright (c) 2002-2019 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;

coherence

1GateCircuit (p,f) is Boolean by CIRCCOMB:61;

end;
let f be Function of (n -tuples_on BOOLEAN),BOOLEAN;

let p be FinSeqLen of n;

coherence

1GateCircuit (p,f) is Boolean by CIRCCOMB:61;

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

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

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

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)

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{ F_{1}() -> non empty ManySortedSign , F_{2}() -> object , F_{3}( object , object , object ) -> non empty ManySortedSign , F_{4}( object , object ) -> object } :

CIRCCMB29sch1{ F

ex f, h being ManySortedSet of NAT st

( f . 0 = F_{1}() & h . 0 = F_{2}() & ( 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) = F_{3}(S,x,n) & h . (n + 1) = F_{4}(x,n) ) ) )

( f . 0 = F

for S being non empty ManySortedSign

for x being set st S = f . n & x = h . n holds

( f . (n + 1) = F

proof end;

scheme :: CIRCCMB2:sch 2

CIRCCMB29sch2{ F_{1}( object , object , object ) -> non empty ManySortedSign , F_{2}( object , object ) -> object , P_{1}[ object , object , object ], F_{3}() -> ManySortedSet of NAT , F_{4}() -> ManySortedSet of NAT } :

provided

CIRCCMB29sch2{ F

provided

A1:
ex S being non empty ManySortedSign ex x being set st

( S = F_{3}() . 0 & x = F_{4}() . 0 & P_{1}[S,x, 0 ] )
and

A2: for n being Nat

for S being non empty ManySortedSign

for x being set st S = F_{3}() . n & x = F_{4}() . n holds

( F_{3}() . (n + 1) = F_{1}(S,x,n) & F_{4}() . (n + 1) = F_{2}(x,n) )
and

A3: for n being Nat

for S being non empty ManySortedSign

for x being set st S = F_{3}() . n & x = F_{4}() . n & P_{1}[S,x,n] holds

P_{1}[F_{1}(S,x,n),F_{2}(x,n),n + 1]

( S = F

A2: for n being Nat

for S being non empty ManySortedSign

for x being set st S = F

( F

A3: for n being Nat

for S being non empty ManySortedSign

for x being set st S = F

P

proof end;

defpred S

scheme :: CIRCCMB2:sch 3

CIRCCMB29sch3{ F_{1}() -> non empty ManySortedSign , F_{2}( object , object , object ) -> non empty ManySortedSign , F_{3}( object , object ) -> object , F_{4}() -> ManySortedSet of NAT , F_{5}() -> ManySortedSet of NAT } :

provided

CIRCCMB29sch3{ F

provided

A1:
F_{4}() . 0 = F_{1}()
and

A2: for n being Nat

for S being non empty ManySortedSign

for x being set st S = F_{4}() . n & x = F_{5}() . n holds

( F_{4}() . (n + 1) = F_{2}(S,x,n) & F_{5}() . (n + 1) = F_{3}(x,n) )

A2: for n being Nat

for S being non empty ManySortedSign

for x being set st S = F

( F

proof end;

scheme :: CIRCCMB2:sch 4

CIRCCMB29sch4{ F_{1}() -> non empty ManySortedSign , F_{2}() -> object , F_{3}( object , object , object ) -> non empty ManySortedSign , F_{4}( object , object ) -> object , F_{5}() -> Nat } :

CIRCCMB29sch4{ F

ex S being non empty ManySortedSign ex f, h being ManySortedSet of NAT st

( S = f . F_{5}() & f . 0 = F_{1}() & h . 0 = F_{2}() & ( 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) = F_{3}(S,x,n) & h . (n + 1) = F_{4}(x,n) ) ) )

( S = f . F

for S being non empty ManySortedSign

for x being set st S = f . n & x = h . n holds

( f . (n + 1) = F

proof end;

scheme :: CIRCCMB2:sch 5

CIRCCMB29sch5{ F_{1}() -> non empty ManySortedSign , F_{2}() -> object , F_{3}( object , object , object ) -> non empty ManySortedSign , F_{4}( object , object ) -> object , F_{5}() -> Nat } :

CIRCCMB29sch5{ F

for S1, S2 being non empty ManySortedSign st ex f, h being ManySortedSet of NAT st

( S1 = f . F_{5}() & f . 0 = F_{1}() & h . 0 = F_{2}() & ( 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) = F_{3}(S,x,n) & h . (n + 1) = F_{4}(x,n) ) ) ) & ex f, h being ManySortedSet of NAT st

( S2 = f . F_{5}() & f . 0 = F_{1}() & h . 0 = F_{2}() & ( 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) = F_{3}(S,x,n) & h . (n + 1) = F_{4}(x,n) ) ) ) holds

S1 = S2

( S1 = f . F

for S being non empty ManySortedSign

for x being set st S = f . n & x = h . n holds

( f . (n + 1) = F

( S2 = f . F

for S being non empty ManySortedSign

for x being set st S = f . n & x = h . n holds

( f . (n + 1) = F

S1 = S2

proof end;

scheme :: CIRCCMB2:sch 6

CIRCCMB29sch6{ F_{1}() -> non empty ManySortedSign , F_{2}() -> object , F_{3}( object , object , object ) -> non empty ManySortedSign , F_{4}( object , object ) -> object , F_{5}() -> Nat } :

CIRCCMB29sch6{ F

( ex S being non empty ManySortedSign ex f, h being ManySortedSet of NAT st

( S = f . F_{5}() & f . 0 = F_{1}() & h . 0 = F_{2}() & ( 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) = F_{3}(S,x,n) & h . (n + 1) = F_{4}(x,n) ) ) ) & ( for S1, S2 being non empty ManySortedSign st ex f, h being ManySortedSet of NAT st

( S1 = f . F_{5}() & f . 0 = F_{1}() & h . 0 = F_{2}() & ( 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) = F_{3}(S,x,n) & h . (n + 1) = F_{4}(x,n) ) ) ) & ex f, h being ManySortedSet of NAT st

( S2 = f . F_{5}() & f . 0 = F_{1}() & h . 0 = F_{2}() & ( 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) = F_{3}(S,x,n) & h . (n + 1) = F_{4}(x,n) ) ) ) holds

S1 = S2 ) )

( S = f . F

for S being non empty ManySortedSign

for x being set st S = f . n & x = h . n holds

( f . (n + 1) = F

( S1 = f . F

for S being non empty ManySortedSign

for x being set st S = f . n & x = h . n holds

( f . (n + 1) = F

( S2 = f . F

for S being non empty ManySortedSign

for x being set st S = f . n & x = h . n holds

( f . (n + 1) = F

S1 = S2 ) )

proof end;

scheme :: CIRCCMB2:sch 7

CIRCCMB29sch7{ F_{1}() -> non empty ManySortedSign , F_{2}( object , object , object ) -> non empty ManySortedSign , F_{3}() -> object , F_{4}( object , object ) -> object , F_{5}() -> Nat } :

CIRCCMB29sch7{ F

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 . F_{5}() & f . 0 = F_{1}() & h . 0 = F_{3}() & ( 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) = F_{2}(S,x,n) & h . (n + 1) = F_{4}(x,n) ) ) )

provided( S = f . F

for S being non empty ManySortedSign

for x being set st S = f . n & x = h . n holds

( f . (n + 1) = F

A1:
( F_{1}() is unsplit & F_{1}() is gate`1=arity & F_{1}() is gate`2isBoolean & not F_{1}() is void & not F_{1}() is empty & F_{1}() 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

( F_{2}(S,x,n) is unsplit & F_{2}(S,x,n) is gate`1=arity & F_{2}(S,x,n) is gate`2isBoolean & not F_{2}(S,x,n) is void & not F_{2}(S,x,n) is empty & F_{2}(S,x,n) is strict )

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

( F

proof end;

scheme :: CIRCCMB2:sch 8

CIRCCMB29sch8{ F_{1}() -> non empty ManySortedSign , F_{2}( object , object ) -> non empty non void unsplit gate`1=arity gate`2isBoolean ManySortedSign , F_{3}() -> object , F_{4}( object , object ) -> object , F_{5}() -> Nat } :

CIRCCMB29sch8{ F

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 . F_{5}() & f . 0 = F_{1}() & h . 0 = F_{3}() & ( 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 +* F_{2}(x,n) & h . (n + 1) = F_{4}(x,n) ) ) )

provided( S = f . F

for S being non empty ManySortedSign

for x being set st S = f . n & x = h . n holds

( f . (n + 1) = S +* F

A1:
( F_{1}() is unsplit & F_{1}() is gate`1=arity & F_{1}() is gate`2isBoolean & not F_{1}() is void & not F_{1}() is empty & F_{1}() is strict )

proof end;

scheme :: CIRCCMB2:sch 9

CIRCCMB29sch9{ F_{1}() -> non empty ManySortedSign , F_{2}() -> object , F_{3}( object , object , object ) -> non empty ManySortedSign , F_{4}( object , object ) -> object , F_{5}() -> Nat } :

CIRCCMB29sch9{ F

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 . F_{5}() & f . 0 = F_{1}() & h . 0 = F_{2}() & ( 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) = F_{3}(S,x,n) & h . (n + 1) = F_{4}(x,n) ) ) ) & ex f, h being ManySortedSet of NAT st

( S2 = f . F_{5}() & f . 0 = F_{1}() & h . 0 = F_{2}() & ( 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) = F_{3}(S,x,n) & h . (n + 1) = F_{4}(x,n) ) ) ) holds

S1 = S2

( S1 = f . F

for S being non empty ManySortedSign

for x being set st S = f . n & x = h . n holds

( f . (n + 1) = F

( S2 = f . F

for S being non empty ManySortedSign

for x being set st S = f . n & x = h . n holds

( f . (n + 1) = F

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

InputVertices (S1 +* S2) = ((InputVertices S1) \ (InnerVertices S2)) \/ ((InputVertices S2) \ (InnerVertices S1))

proof end;

scheme :: CIRCCMB2:sch 10

CIRCCMB29sch10{ F_{1}() -> non empty non void unsplit gate`1=arity gate`2isBoolean ManySortedSign , F_{2}( object ) -> object , F_{3}() -> ManySortedSet of NAT , F_{4}( object , object ) -> non empty non void unsplit gate`1=arity gate`2isBoolean ManySortedSign , F_{5}( object , object ) -> object } :

CIRCCMB29sch10{ F

for n being Nat ex S1, S2 being non empty non void unsplit gate`1=arity gate`2isBoolean ManySortedSign st

( S1 = F_{2}(n) & S2 = F_{2}((n + 1)) & InputVertices S2 = (InputVertices S1) \/ ((InputVertices F_{4}((F_{3}() . n),n)) \ {(F_{3}() . n)}) & InnerVertices S1 is Relation & InputVertices S1 is without_pairs )

provided( S1 = F

A1:
InnerVertices F_{1}() is Relation
and

A2: InputVertices F_{1}() is without_pairs
and

A3: ( F_{2}(0) = F_{1}() & F_{3}() . 0 in InnerVertices F_{1}() )
and

A4: for n being Nat

for x being set holds InnerVertices F_{4}(x,n) is Relation
and

A5: for n being Nat

for x being set st x = F_{3}() . n holds

(InputVertices F_{4}(x,n)) \ {x} is without_pairs
and

A6: for n being Nat

for S being non empty ManySortedSign

for x being set st S = F_{2}(n) & x = F_{3}() . n holds

( F_{2}((n + 1)) = S +* F_{4}(x,n) & F_{3}() . (n + 1) = F_{5}(x,n) & x in InputVertices F_{4}(x,n) & F_{5}(x,n) in InnerVertices F_{4}(x,n) )

A2: InputVertices F

A3: ( F

A4: for n being Nat

for x being set holds InnerVertices F

A5: for n being Nat

for x being set st x = F

(InputVertices F

A6: for n being Nat

for S being non empty ManySortedSign

for x being set st S = F

( F

proof end;

scheme :: CIRCCMB2:sch 11

CIRCCMB29sch11{ F_{1}( set ) -> non empty non void unsplit gate`1=arity gate`2isBoolean ManySortedSign , F_{2}() -> ManySortedSet of NAT , F_{3}( object , object ) -> non empty non void unsplit gate`1=arity gate`2isBoolean ManySortedSign , F_{4}( object , object ) -> object } :

CIRCCMB29sch11{ F

for n being Nat holds

( InputVertices F_{1}((n + 1)) = (InputVertices F_{1}(n)) \/ ((InputVertices F_{3}((F_{2}() . n),n)) \ {(F_{2}() . n)}) & InnerVertices F_{1}(n) is Relation & InputVertices F_{1}(n) is without_pairs )

provided( InputVertices F

A1:
InnerVertices F_{1}(0) is Relation
and

A2: InputVertices F_{1}(0) is without_pairs
and

A3: F_{2}() . 0 in InnerVertices F_{1}(0)
and

A4: for n being Nat

for x being set holds InnerVertices F_{3}(x,n) is Relation
and

A5: for n being Nat

for x being set st x = F_{2}() . n holds

(InputVertices F_{3}(x,n)) \ {x} is without_pairs
and

A6: for n being Nat

for S being non empty ManySortedSign

for x being set st S = F_{1}(n) & x = F_{2}() . n holds

( F_{1}((n + 1)) = S +* F_{3}(x,n) & F_{2}() . (n + 1) = F_{4}(x,n) & x in InputVertices F_{3}(x,n) & F_{4}(x,n) in InnerVertices F_{3}(x,n) )

A2: InputVertices F

A3: F

A4: for n being Nat

for x being set holds InnerVertices F

A5: for n being Nat

for x being set st x = F

(InputVertices F

A6: for n being Nat

for S being non empty ManySortedSign

for x being set st S = F

( F

proof end;

scheme :: CIRCCMB2:sch 12

CIRCCMB29sch12{ F_{1}() -> non empty ManySortedSign , F_{2}() -> non-empty MSAlgebra over F_{1}(), F_{3}() -> object , F_{4}( object , object , object ) -> non empty ManySortedSign , F_{5}( object , object , object , object ) -> object , F_{6}( object , object ) -> object } :

CIRCCMB29sch12{ F

ex f, g, h being ManySortedSet of NAT st

( f . 0 = F_{1}() & g . 0 = F_{2}() & h . 0 = F_{3}() & ( 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) = F_{4}(S,x,n) & g . (n + 1) = F_{5}(S,A,x,n) & h . (n + 1) = F_{6}(x,n) ) ) )

( f . 0 = F

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) = F

proof end;

scheme :: CIRCCMB2:sch 13

CIRCCMB29sch13{ F_{1}( set , set , set ) -> non empty ManySortedSign , F_{2}( object , object , object , object ) -> object , F_{3}( object , object ) -> object , P_{1}[ object , object , object , object ], F_{4}() -> ManySortedSet of NAT , F_{5}() -> ManySortedSet of NAT , F_{6}() -> ManySortedSet of NAT } :

CIRCCMB29sch13{ F

for n being Nat ex S being non empty ManySortedSign ex A being non-empty MSAlgebra over S st

( S = F_{4}() . n & A = F_{5}() . n & P_{1}[S,A,F_{6}() . n,n] )

provided( S = F

A1:
ex S being non empty ManySortedSign ex A being non-empty MSAlgebra over S ex x being set st

( S = F_{4}() . 0 & A = F_{5}() . 0 & x = F_{6}() . 0 & P_{1}[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 = F_{4}() . n & A = F_{5}() . n & x = F_{6}() . n holds

( F_{4}() . (n + 1) = F_{1}(S,x,n) & F_{5}() . (n + 1) = F_{2}(S,A,x,n) & F_{6}() . (n + 1) = F_{3}(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 = F_{4}() . n & A = F_{5}() . n & x = F_{6}() . n & P_{1}[S,A,x,n] holds

P_{1}[F_{1}(S,x,n),F_{2}(S,A,x,n),F_{3}(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 F_{2}(S,A,x,n) is non-empty MSAlgebra over F_{1}(S,x,n)

( S = F

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 = F

( F

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 = F

P

A4: for S being non empty ManySortedSign

for A being non-empty MSAlgebra over S

for x being set

for n being Nat holds F

proof end;

defpred S

scheme :: CIRCCMB2:sch 14

CIRCCMB29sch14{ F_{1}( set , set , set ) -> non empty ManySortedSign , F_{2}( object , object , object , object ) -> object , F_{3}( object , object ) -> object , F_{4}() -> ManySortedSet of NAT , F_{5}() -> ManySortedSet of NAT , F_{6}() -> ManySortedSet of NAT , F_{7}() -> ManySortedSet of NAT , F_{8}() -> ManySortedSet of NAT , F_{9}() -> ManySortedSet of NAT } :

provided

CIRCCMB29sch14{ F

provided

A1:
ex S being non empty ManySortedSign ex A being non-empty MSAlgebra over S st

( S = F_{4}() . 0 & A = F_{6}() . 0 )
and

A2: ( F_{4}() . 0 = F_{5}() . 0 & F_{6}() . 0 = F_{7}() . 0 & F_{8}() . 0 = F_{9}() . 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 = F_{4}() . n & A = F_{6}() . n & x = F_{8}() . n holds

( F_{4}() . (n + 1) = F_{1}(S,x,n) & F_{6}() . (n + 1) = F_{2}(S,A,x,n) & F_{8}() . (n + 1) = F_{3}(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 = F_{5}() . n & A = F_{7}() . n & x = F_{9}() . n holds

( F_{5}() . (n + 1) = F_{1}(S,x,n) & F_{7}() . (n + 1) = F_{2}(S,A,x,n) & F_{9}() . (n + 1) = F_{3}(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 F_{2}(S,A,x,n) is non-empty MSAlgebra over F_{1}(S,x,n)

( S = F

A2: ( F

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 = F

( F

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 = F

( F

A5: for S being non empty ManySortedSign

for A being non-empty MSAlgebra over S

for x being set

for n being Nat holds F

proof end;

scheme :: CIRCCMB2:sch 15

CIRCCMB29sch15{ F_{1}() -> non empty ManySortedSign , F_{2}() -> non-empty MSAlgebra over F_{1}(), F_{3}( object , object , object ) -> non empty ManySortedSign , F_{4}( object , object , object , object ) -> object , F_{5}( object , object ) -> object , F_{6}() -> ManySortedSet of NAT , F_{7}() -> ManySortedSet of NAT , F_{8}() -> ManySortedSet of NAT } :

CIRCCMB29sch15{ F

for n being Nat

for S being non empty ManySortedSign

for x being set st S = F_{6}() . n & x = F_{8}() . n holds

( F_{6}() . (n + 1) = F_{3}(S,x,n) & F_{8}() . (n + 1) = F_{5}(x,n) )

providedfor S being non empty ManySortedSign

for x being set st S = F

( F

A1:
( F_{6}() . 0 = F_{1}() & F_{7}() . 0 = F_{2}() )
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 = F_{6}() . n & A = F_{7}() . n & x = F_{8}() . n holds

( F_{6}() . (n + 1) = F_{3}(S,x,n) & F_{7}() . (n + 1) = F_{4}(S,A,x,n) & F_{8}() . (n + 1) = F_{5}(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 F_{4}(S,A,x,n) is non-empty MSAlgebra over F_{3}(S,x,n)

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 = F

( F

A3: for S being non empty ManySortedSign

for A being non-empty MSAlgebra over S

for x being set

for n being Nat holds F

proof end;

scheme :: CIRCCMB2:sch 16

CIRCCMB29sch16{ F_{1}() -> non empty ManySortedSign , F_{2}() -> non-empty MSAlgebra over F_{1}(), F_{3}() -> object , F_{4}( object , object , object ) -> non empty ManySortedSign , F_{5}( object , object , object , object ) -> object , F_{6}( object , object ) -> object , F_{7}() -> Nat } :

CIRCCMB29sch16{ F

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 . F_{7}() & A = g . F_{7}() & f . 0 = F_{1}() & g . 0 = F_{2}() & h . 0 = F_{3}() & ( 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) = F_{4}(S,x,n) & g . (n + 1) = F_{5}(S,A,x,n) & h . (n + 1) = F_{6}(x,n) ) ) )

provided( S = f . F

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) = F

A1:
for S being non empty ManySortedSign

for A being non-empty MSAlgebra over S

for x being set

for n being Nat holds F_{5}(S,A,x,n) is non-empty MSAlgebra over F_{4}(S,x,n)

for A being non-empty MSAlgebra over S

for x being set

for n being Nat holds F

proof end;

scheme :: CIRCCMB2:sch 17

CIRCCMB29sch17{ F_{1}() -> non empty ManySortedSign , F_{2}() -> non empty ManySortedSign , F_{3}() -> non-empty MSAlgebra over F_{1}(), F_{4}() -> object , F_{5}( object , object , object ) -> non empty ManySortedSign , F_{6}( object , object , object , object ) -> object , F_{7}( object , object ) -> object , F_{8}() -> Nat } :

CIRCCMB29sch17{ F

ex A being non-empty MSAlgebra over F_{2}() ex f, g, h being ManySortedSet of NAT st

( F_{2}() = f . F_{8}() & A = g . F_{8}() & f . 0 = F_{1}() & g . 0 = F_{3}() & h . 0 = F_{4}() & ( 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) = F_{5}(S,x,n) & g . (n + 1) = F_{6}(S,A,x,n) & h . (n + 1) = F_{7}(x,n) ) ) )

provided( F

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) = F

A1:
ex f, h being ManySortedSet of NAT st

( F_{2}() = f . F_{8}() & f . 0 = F_{1}() & h . 0 = F_{4}() & ( 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) = F_{5}(S,x,n) & h . (n + 1) = F_{7}(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 F_{6}(S,A,x,n) is non-empty MSAlgebra over F_{5}(S,x,n)

( F

for S being non empty ManySortedSign

for x being set st S = f . n & x = h . n holds

( f . (n + 1) = F

A2: for S being non empty ManySortedSign

for A being non-empty MSAlgebra over S

for x being set

for n being Nat holds F

proof end;

scheme :: CIRCCMB2:sch 18

CIRCCMB29sch18{ F_{1}() -> non empty ManySortedSign , F_{2}() -> non empty ManySortedSign , F_{3}() -> non-empty MSAlgebra over F_{1}(), F_{4}() -> object , F_{5}( object , object , object ) -> non empty ManySortedSign , F_{6}( object , object , object , object ) -> object , F_{7}( object , object ) -> object , F_{8}() -> Nat } :

CIRCCMB29sch18{ F

for A1, A2 being non-empty MSAlgebra over F_{2}() st ex f, g, h being ManySortedSet of NAT st

( F_{2}() = f . F_{8}() & A1 = g . F_{8}() & f . 0 = F_{1}() & g . 0 = F_{3}() & h . 0 = F_{4}() & ( 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) = F_{5}(S,x,n) & g . (n + 1) = F_{6}(S,A,x,n) & h . (n + 1) = F_{7}(x,n) ) ) ) & ex f, g, h being ManySortedSet of NAT st

( F_{2}() = f . F_{8}() & A2 = g . F_{8}() & f . 0 = F_{1}() & g . 0 = F_{3}() & h . 0 = F_{4}() & ( 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) = F_{5}(S,x,n) & g . (n + 1) = F_{6}(S,A,x,n) & h . (n + 1) = F_{7}(x,n) ) ) ) holds

A1 = A2

provided( F

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) = F

( F

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) = F

A1 = A2

A1:
for S being non empty ManySortedSign

for A being non-empty MSAlgebra over S

for x being set

for n being Nat holds F_{6}(S,A,x,n) is non-empty MSAlgebra over F_{5}(S,x,n)

for A being non-empty MSAlgebra over S

for x being set

for n being Nat holds F

proof end;

scheme :: CIRCCMB2:sch 19

CIRCCMB29sch19{ F_{1}() -> non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign , F_{2}() -> non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign , F_{3}() -> strict gate`2=den Boolean Circuit of F_{1}(), F_{4}( object , object , object ) -> non empty ManySortedSign , F_{5}( object , object , object , object ) -> object , F_{6}() -> object , F_{7}( object , object ) -> object , F_{8}() -> Nat } :

CIRCCMB29sch19{ F

ex A being strict gate`2=den Boolean Circuit of F_{2}() ex f, g, h being ManySortedSet of NAT st

( F_{2}() = f . F_{8}() & A = g . F_{8}() & f . 0 = F_{1}() & g . 0 = F_{3}() & h . 0 = F_{6}() & ( 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) = F_{4}(S,x,n) & g . (n + 1) = F_{5}(S,A,x,n) & h . (n + 1) = F_{7}(x,n) ) ) )

provided( F

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) = F

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

( F_{4}(S,x,n) is unsplit & F_{4}(S,x,n) is gate`1=arity & F_{4}(S,x,n) is gate`2isBoolean & not F_{4}(S,x,n) is void & F_{4}(S,x,n) is strict )
and

A2: ex f, h being ManySortedSet of NAT st

( F_{2}() = f . F_{8}() & f . 0 = F_{1}() & h . 0 = F_{6}() & ( 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) = F_{4}(S,x,n) & h . (n + 1) = F_{7}(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 F_{5}(S,A,x,n) is non-empty MSAlgebra over F_{4}(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 = F_{4}(S,x,n) holds

F_{5}(S,A,x,n) is strict gate`2=den Boolean Circuit of S1

for x being set

for n being Nat holds

( F

A2: ex f, h being ManySortedSet of NAT st

( F

for S being non empty ManySortedSign

for x being set st S = f . n & x = h . n holds

( f . (n + 1) = F

A3: for S being non empty ManySortedSign

for A being non-empty MSAlgebra over S

for x being set

for n being Nat holds F

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 = F

F

proof end;

definition

let S be non empty ManySortedSign ;

let A be object ;

assume A1: A is non-empty MSAlgebra over S ;

existence

ex b_{1} being non-empty MSAlgebra over S st b_{1} = A
by A1;

uniqueness

for b_{1}, b_{2} being non-empty MSAlgebra over S st b_{1} = A & b_{2} = A holds

b_{1} = b_{2}
;

end;
let A be object ;

assume A1: A is non-empty MSAlgebra over S ;

existence

ex b

uniqueness

for b

b

:: 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 b_{3} being non-empty MSAlgebra over S holds

( b_{3} = MSAlg (A,S) iff b_{3} = A );

for S being non empty ManySortedSign

for A being object st A is non-empty MSAlgebra over S holds

for b

( b

scheme :: CIRCCMB2:sch 20

CIRCCMB29sch20{ F_{1}() -> non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign , F_{2}() -> non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign , F_{3}() -> strict gate`2=den Boolean Circuit of F_{1}(), F_{4}( object , object ) -> non empty non void unsplit gate`1=arity gate`2isBoolean ManySortedSign , F_{5}( object , object ) -> object , F_{6}() -> object , F_{7}( object , object ) -> object , F_{8}() -> Nat } :

CIRCCMB29sch20{ F

ex A being strict gate`2=den Boolean Circuit of F_{2}() ex f, g, h being ManySortedSet of NAT st

( F_{2}() = f . F_{8}() & A = g . F_{8}() & f . 0 = F_{1}() & g . 0 = F_{3}() & h . 0 = F_{6}() & ( 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 F_{4}(x,n) st S = f . n & A1 = g . n & x = h . n & A2 = F_{5}(x,n) holds

( f . (n + 1) = S +* F_{4}(x,n) & g . (n + 1) = A1 +* A2 & h . (n + 1) = F_{7}(x,n) ) ) )

provided( F

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 F

( f . (n + 1) = S +* F

A1:
ex f, h being ManySortedSet of NAT st

( F_{2}() = f . F_{8}() & f . 0 = F_{1}() & h . 0 = F_{6}() & ( 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 +* F_{4}(x,n) & h . (n + 1) = F_{7}(x,n) ) ) )
and

A2: for x being set

for n being Nat holds F_{5}(x,n) is strict gate`2=den Boolean Circuit of F_{4}(x,n)

( F

for S being non empty ManySortedSign

for x being set st S = f . n & x = h . n holds

( f . (n + 1) = S +* F

A2: for x being set

for n being Nat holds F

proof end;

scheme :: CIRCCMB2:sch 21

CIRCCMB29sch21{ F_{1}() -> non empty ManySortedSign , F_{2}() -> non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign , F_{3}() -> non-empty MSAlgebra over F_{1}(), F_{4}() -> object , F_{5}( object , object , object ) -> non empty ManySortedSign , F_{6}( object , object , object , object ) -> object , F_{7}( object , object ) -> object , F_{8}() -> Nat } :

CIRCCMB29sch21{ F

for A1, A2 being strict gate`2=den Boolean Circuit of F_{2}() st ex f, g, h being ManySortedSet of NAT st

( F_{2}() = f . F_{8}() & A1 = g . F_{8}() & f . 0 = F_{1}() & g . 0 = F_{3}() & h . 0 = F_{4}() & ( 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) = F_{5}(S,x,n) & g . (n + 1) = F_{6}(S,A,x,n) & h . (n + 1) = F_{7}(x,n) ) ) ) & ex f, g, h being ManySortedSet of NAT st

( F_{2}() = f . F_{8}() & A2 = g . F_{8}() & f . 0 = F_{1}() & g . 0 = F_{3}() & h . 0 = F_{4}() & ( 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) = F_{5}(S,x,n) & g . (n + 1) = F_{6}(S,A,x,n) & h . (n + 1) = F_{7}(x,n) ) ) ) holds

A1 = A2

provided( F

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) = F

( F

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) = F

A1 = A2

A1:
for S being non empty ManySortedSign

for A being non-empty MSAlgebra over S

for x being set

for n being Nat holds F_{6}(S,A,x,n) is non-empty MSAlgebra over F_{5}(S,x,n)

for A being non-empty MSAlgebra over S

for x being set

for n being Nat holds F

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

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

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

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

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)

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)

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

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

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

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)

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

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

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

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

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

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

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{ F_{1}() -> non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign , F_{2}() -> non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign , F_{3}() -> strict gate`2=den Boolean Circuit of F_{1}(), F_{4}() -> strict gate`2=den Boolean Circuit of F_{2}(), F_{5}( object , object ) -> non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign , F_{6}( object , object ) -> object , F_{7}() -> ManySortedSet of NAT , F_{8}() -> object , F_{9}( object , object ) -> object , F_{10}( Nat) -> Nat } :

provided

CIRCCMB29sch22{ F

provided

A1:
for x being set

for n being Nat holds F_{6}(x,n) is strict gate`2=den Boolean Circuit of F_{5}(x,n)
and

A2: for s being State of F_{3}() holds Following (s,F_{10}(0)) is stable
and

A3: for n being Nat

for x being set

for A being non-empty Circuit of F_{5}(x,n) st x = F_{7}() . n & A = F_{6}(x,n) holds

for s being State of A holds Following (s,F_{10}(1)) is stable
and

A4: ex f, g being ManySortedSet of NAT st

( F_{2}() = f . F_{10}(2) & F_{4}() = g . F_{10}(2) & f . 0 = F_{1}() & g . 0 = F_{3}() & F_{7}() . 0 = F_{8}() & ( 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 F_{5}(x,n) st S = f . n & A1 = g . n & x = F_{7}() . n & A2 = F_{6}(x,n) holds

( f . (n + 1) = S +* F_{5}(x,n) & g . (n + 1) = A1 +* A2 & F_{7}() . (n + 1) = F_{9}(x,n) ) ) )
and

A5: ( InnerVertices F_{1}() is Relation & InputVertices F_{1}() is without_pairs )
and

A6: ( F_{7}() . 0 = F_{8}() & F_{8}() in InnerVertices F_{1}() )
and

A7: for n being Nat

for x being set holds InnerVertices F_{5}(x,n) is Relation
and

A8: for n being Nat

for x being set st x = F_{7}() . n holds

(InputVertices F_{5}(x,n)) \ {x} is without_pairs
and

A9: for n being Nat

for x being set st x = F_{7}() . n holds

( F_{7}() . (n + 1) = F_{9}(x,n) & x in InputVertices F_{5}(x,n) & F_{9}(x,n) in InnerVertices F_{5}(x,n) )

for n being Nat holds F

A2: for s being State of F

A3: for n being Nat

for x being set

for A being non-empty Circuit of F

for s being State of A holds Following (s,F

A4: ex f, g being ManySortedSet of NAT st

( F

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 F

( f . (n + 1) = S +* F

A5: ( InnerVertices F

A6: ( F

A7: for n being Nat

for x being set holds InnerVertices F

A8: for n being Nat

for x being set st x = F

(InputVertices F

A9: for n being Nat

for x being set st x = F

( F

proof end;