:: CIRCCMB2 semantic presentation

registration
let c1 be Nat;
let c2 be Function of c1 -tuples_on BOOLEAN , BOOLEAN ;
let c3 be FinSeqLen of c1;
cluster 1GateCircuit a3,a2 -> Boolean ;
coherence
1GateCircuit c3,c2 is Boolean by CIRCCOMB:69;
end;

theorem Th1: :: CIRCCMB2:1
for b1 being non empty finite set
for b2 being Nat
for b3 being FinSeqLen of b2
for b4 being Function of b2 -tuples_on b1,b1
for b5 being OperSymbol of (1GateCircStr b3,b4)
for b6 being State of (1GateCircuit b3,b4) holds b5 depends_on_in b6 = b6 * b3
proof end;

theorem Th2: :: CIRCCMB2:2
for b1 being non empty finite set
for b2 being Nat
for b3 being FinSeqLen of b2
for b4 being Function of b2 -tuples_on b1,b1
for b5 being State of (1GateCircuit b3,b4) holds Following b5 is stable
proof end;

theorem Th3: :: CIRCCMB2:3
for b1 being non empty non void Circuit-like ManySortedSign
for b2 being non-empty Circuit of b1
for b3 being State of b2 st b3 is stable holds
for b4 being Nat holds Following b3,b4 = b3
proof end;

theorem Th4: :: CIRCCMB2:4
for b1 being non empty non void Circuit-like ManySortedSign
for b2 being non-empty Circuit of b1
for b3 being State of b2
for b4, b5 being Nat st Following b3,b4 is stable & b4 <= b5 holds
Following b3,b5 = Following b3,b4
proof end;

scheme :: CIRCCMB2:sch 1
s1{ F1() -> non empty ManySortedSign , F2() -> set , F3( set , set , set ) -> non empty ManySortedSign , F4( set , set ) -> set } :
ex b1, b2 being ManySortedSet of NAT st
( b1 . 0 = F1() & b2 . 0 = F2() & ( for b3 being Nat
for b4 being non empty ManySortedSign
for b5 being set st b4 = b1 . b3 & b5 = b2 . b3 holds
( b1 . (b3 + 1) = F3(b4,b5,b3) & b2 . (b3 + 1) = F4(b5,b3) ) ) )
proof end;

scheme :: CIRCCMB2:sch 2
s2{ F1( set , set , set ) -> non empty ManySortedSign , F2( set , set ) -> set , P1[ set , set , set ], F3() -> ManySortedSet of NAT , F4() -> ManySortedSet of NAT } :
for b1 being Nat ex b2 being non empty ManySortedSign st
( b2 = F3() . b1 & P1[b2,F4() . b1,b1] )
provided
E4: ex b1 being non empty ManySortedSign ex b2 being set st
( b1 = F3() . 0 & b2 = F4() . 0 & P1[b1,b2,0] ) and
E5: for b1 being Nat
for b2 being non empty ManySortedSign
for b3 being set st b2 = F3() . b1 & b3 = F4() . b1 holds
( F3() . (b1 + 1) = F1(b2,b3,b1) & F4() . (b1 + 1) = F2(b3,b1) ) and
E6: for b1 being Nat
for b2 being non empty ManySortedSign
for b3 being set st b2 = F3() . b1 & b3 = F4() . b1 & P1[b2,b3,b1] holds
P1[F1(b2,b3,b1),F2(b3,b1),b1 + 1]
proof end;

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

scheme :: CIRCCMB2:sch 3
s3{ F1() -> non empty ManySortedSign , F2( set , set , set ) -> non empty ManySortedSign , F3( set , set ) -> set , F4() -> ManySortedSet of NAT , F5() -> ManySortedSet of NAT } :
for b1 being Nat
for b2 being set st b2 = F5() . b1 holds
F5() . (b1 + 1) = F3(b2,b1)
provided
E4: F4() . 0 = F1() and
E5: for b1 being Nat
for b2 being non empty ManySortedSign
for b3 being set st b2 = F4() . b1 & b3 = F5() . b1 holds
( F4() . (b1 + 1) = F2(b2,b3,b1) & F5() . (b1 + 1) = F3(b3,b1) )
proof end;

scheme :: CIRCCMB2:sch 4
s4{ F1() -> non empty ManySortedSign , F2() -> set , F3( set , set , set ) -> non empty ManySortedSign , F4( set , set ) -> set , F5() -> Nat } :
ex b1 being non empty ManySortedSign ex b2, b3 being ManySortedSet of NAT st
( b1 = b2 . F5() & b2 . 0 = F1() & b3 . 0 = F2() & ( for b4 being Nat
for b5 being non empty ManySortedSign
for b6 being set st b5 = b2 . b4 & b6 = b3 . b4 holds
( b2 . (b4 + 1) = F3(b5,b6,b4) & b3 . (b4 + 1) = F4(b6,b4) ) ) )
proof end;

scheme :: CIRCCMB2:sch 5
s5{ F1() -> non empty ManySortedSign , F2() -> set , F3( set , set , set ) -> non empty ManySortedSign , F4( set , set ) -> set , F5() -> Nat } :
for b1, b2 being non empty ManySortedSign st ex b3, b4 being ManySortedSet of NAT st
( b1 = b3 . F5() & b3 . 0 = F1() & b4 . 0 = F2() & ( for b5 being Nat
for b6 being non empty ManySortedSign
for b7 being set st b6 = b3 . b5 & b7 = b4 . b5 holds
( b3 . (b5 + 1) = F3(b6,b7,b5) & b4 . (b5 + 1) = F4(b7,b5) ) ) ) & ex b3, b4 being ManySortedSet of NAT st
( b2 = b3 . F5() & b3 . 0 = F1() & b4 . 0 = F2() & ( for b5 being Nat
for b6 being non empty ManySortedSign
for b7 being set st b6 = b3 . b5 & b7 = b4 . b5 holds
( b3 . (b5 + 1) = F3(b6,b7,b5) & b4 . (b5 + 1) = F4(b7,b5) ) ) ) holds
b1 = b2
proof end;

scheme :: CIRCCMB2:sch 6
s6{ F1() -> non empty ManySortedSign , F2() -> set , F3( set , set , set ) -> non empty ManySortedSign , F4( set , set ) -> set , F5() -> Nat } :
( ex b1 being non empty ManySortedSign ex b2, b3 being ManySortedSet of NAT st
( b1 = b2 . F5() & b2 . 0 = F1() & b3 . 0 = F2() & ( for b4 being Nat
for b5 being non empty ManySortedSign
for b6 being set st b5 = b2 . b4 & b6 = b3 . b4 holds
( b2 . (b4 + 1) = F3(b5,b6,b4) & b3 . (b4 + 1) = F4(b6,b4) ) ) ) & ( for b1, b2 being non empty ManySortedSign st ex b3, b4 being ManySortedSet of NAT st
( b1 = b3 . F5() & b3 . 0 = F1() & b4 . 0 = F2() & ( for b5 being Nat
for b6 being non empty ManySortedSign
for b7 being set st b6 = b3 . b5 & b7 = b4 . b5 holds
( b3 . (b5 + 1) = F3(b6,b7,b5) & b4 . (b5 + 1) = F4(b7,b5) ) ) ) & ex b3, b4 being ManySortedSet of NAT st
( b2 = b3 . F5() & b3 . 0 = F1() & b4 . 0 = F2() & ( for b5 being Nat
for b6 being non empty ManySortedSign
for b7 being set st b6 = b3 . b5 & b7 = b4 . b5 holds
( b3 . (b5 + 1) = F3(b6,b7,b5) & b4 . (b5 + 1) = F4(b7,b5) ) ) ) holds
b1 = b2 ) )
proof end;

scheme :: CIRCCMB2:sch 7
s7{ F1() -> non empty ManySortedSign , F2( set , set , set ) -> non empty ManySortedSign , F3() -> set , F4( set , set ) -> set , F5() -> Nat } :
ex b1 being non empty strict non void unsplit gate`1=arity gate`2isBoolean ManySortedSign ex b2, b3 being ManySortedSet of NAT st
( b1 = b2 . F5() & b2 . 0 = F1() & b3 . 0 = F3() & ( for b4 being Nat
for b5 being non empty ManySortedSign
for b6 being set st b5 = b2 . b4 & b6 = b3 . b4 holds
( b2 . (b4 + 1) = F2(b5,b6,b4) & b3 . (b4 + 1) = F4(b6,b4) ) ) )
provided
E4: ( F1() is unsplit & F1() is gate`1=arity & F1() is gate`2isBoolean & not F1() is void & not F1() is empty & F1() is strict ) and
E5: for b1 being non empty strict non void unsplit gate`1=arity gate`2isBoolean ManySortedSign
for b2 being set
for b3 being Nat holds
( F2(b1,b2,b3) is unsplit & F2(b1,b2,b3) is gate`1=arity & F2(b1,b2,b3) is gate`2isBoolean & not F2(b1,b2,b3) is void & not F2(b1,b2,b3) is empty & F2(b1,b2,b3) is strict )
proof end;

scheme :: CIRCCMB2:sch 8
s8{ F1() -> non empty ManySortedSign , F2( set , set ) -> non empty non void unsplit gate`1=arity gate`2isBoolean ManySortedSign , F3() -> set , F4( set , set ) -> set , F5() -> Nat } :
ex b1 being non empty strict non void unsplit gate`1=arity gate`2isBoolean ManySortedSign ex b2, b3 being ManySortedSet of NAT st
( b1 = b2 . F5() & b2 . 0 = F1() & b3 . 0 = F3() & ( for b4 being Nat
for b5 being non empty ManySortedSign
for b6 being set st b5 = b2 . b4 & b6 = b3 . b4 holds
( b2 . (b4 + 1) = b5 +* F2(b6,b4) & b3 . (b4 + 1) = F4(b6,b4) ) ) )
provided
E4: ( 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
s9{ F1() -> non empty ManySortedSign , F2() -> set , F3( set , set , set ) -> non empty ManySortedSign , F4( set , set ) -> set , F5() -> Nat } :
for b1, b2 being non empty strict non void unsplit gate`1=arity gate`2isBoolean ManySortedSign st ex b3, b4 being ManySortedSet of NAT st
( b1 = b3 . F5() & b3 . 0 = F1() & b4 . 0 = F2() & ( for b5 being Nat
for b6 being non empty ManySortedSign
for b7 being set st b6 = b3 . b5 & b7 = b4 . b5 holds
( b3 . (b5 + 1) = F3(b6,b7,b5) & b4 . (b5 + 1) = F4(b7,b5) ) ) ) & ex b3, b4 being ManySortedSet of NAT st
( b2 = b3 . F5() & b3 . 0 = F1() & b4 . 0 = F2() & ( for b5 being Nat
for b6 being non empty ManySortedSign
for b7 being set st b6 = b3 . b5 & b7 = b4 . b5 holds
( b3 . (b5 + 1) = F3(b6,b7,b5) & b4 . (b5 + 1) = F4(b7,b5) ) ) ) holds
b1 = b2
proof end;

theorem Th5: :: CIRCCMB2:5
for b1, b2 being Function st b1 tolerates b2 holds
rng (b1 +* b2) = (rng b1) \/ (rng b2)
proof end;

theorem Th6: :: CIRCCMB2:6
for b1, b2 being non empty ManySortedSign st b1 tolerates b2 holds
InputVertices (b1 +* b2) = ((InputVertices b1) \ (InnerVertices b2)) \/ ((InputVertices b2) \ (InnerVertices b1))
proof end;

theorem Th7: :: CIRCCMB2:7
for b1 being without_pairs set
for b2 being Relation holds b1 \ b2 = b1
proof end;

theorem Th8: :: CIRCCMB2:8
for b1 being Relation
for b2, b3 being set st b3 c= b2 & not b2 \ b3 is with_pair holds
b1 \ b2 = b1 \ b3
proof end;

theorem Th9: :: CIRCCMB2:9
for b1, b2 being set
for b3 being Relation st b2 c= b3 & not b1 \ b2 is with_pair holds
b1 \ b3 = b1 \ b2
proof end;

scheme :: CIRCCMB2:sch 10
s10{ F1() -> non empty non void unsplit gate`1=arity gate`2isBoolean ManySortedSign , F2( set ) -> set , F3() -> ManySortedSet of NAT , F4( set , set ) -> non empty non void unsplit gate`1=arity gate`2isBoolean ManySortedSign , F5( set , set ) -> set } :
for b1 being Nat ex b2, b3 being non empty non void unsplit gate`1=arity gate`2isBoolean ManySortedSign st
( b2 = F2(b1) & b3 = F2((b1 + 1)) & InputVertices b3 = (InputVertices b2) \/ ((InputVertices F4((F3() . b1),b1)) \ {(F3() . b1)}) & InnerVertices b2 is Relation & not InputVertices b2 is with_pair )
provided
E8: InnerVertices F1() is Relation and
E9: not InputVertices F1() is with_pair and
E10: ( F2(0) = F1() & F3() . 0 in InnerVertices F1() ) and
E11: for b1 being Nat
for b2 being set holds InnerVertices F4(b2,b1) is Relation and
E12: for b1 being Nat
for b2 being set st b2 = F3() . b1 holds
not (InputVertices F4(b2,b1)) \ {b2} is with_pair and
E13: for b1 being Nat
for b2 being non empty ManySortedSign
for b3 being set st b2 = F2(b1) & b3 = F3() . b1 holds
( F2((b1 + 1)) = b2 +* F4(b3,b1) & F3() . (b1 + 1) = F5(b3,b1) & b3 in InputVertices F4(b3,b1) & F5(b3,b1) in InnerVertices F4(b3,b1) )
proof end;

scheme :: CIRCCMB2:sch 11
s11{ F1( set ) -> non empty non void unsplit gate`1=arity gate`2isBoolean ManySortedSign , F2() -> ManySortedSet of NAT , F3( set , set ) -> non empty non void unsplit gate`1=arity gate`2isBoolean ManySortedSign , F4( set , set ) -> set } :
for b1 being Nat holds
( InputVertices F1((b1 + 1)) = (InputVertices F1(b1)) \/ ((InputVertices F3((F2() . b1),b1)) \ {(F2() . b1)}) & InnerVertices F1(b1) is Relation & not InputVertices F1(b1) is with_pair )
provided
E8: InnerVertices F1(0) is Relation and
E9: not InputVertices F1(0) is with_pair and
E10: F2() . 0 in InnerVertices F1(0) and
E11: for b1 being Nat
for b2 being set holds InnerVertices F3(b2,b1) is Relation and
E12: for b1 being Nat
for b2 being set st b2 = F2() . b1 holds
not (InputVertices F3(b2,b1)) \ {b2} is with_pair and
E13: for b1 being Nat
for b2 being non empty ManySortedSign
for b3 being set st b2 = F1(b1) & b3 = F2() . b1 holds
( F1((b1 + 1)) = b2 +* F3(b3,b1) & F2() . (b1 + 1) = F4(b3,b1) & b3 in InputVertices F3(b3,b1) & F4(b3,b1) in InnerVertices F3(b3,b1) )
proof end;

scheme :: CIRCCMB2:sch 12
s12{ F1() -> non empty ManySortedSign , F2() -> non-empty MSAlgebra of F1(), F3() -> set , F4( set , set , set ) -> non empty ManySortedSign , F5( set , set , set , set ) -> set , F6( set , set ) -> set } :
ex b1, b2, b3 being ManySortedSet of NAT st
( b1 . 0 = F1() & b2 . 0 = F2() & b3 . 0 = F3() & ( for b4 being Nat
for b5 being non empty ManySortedSign
for b6 being non-empty MSAlgebra of b5
for b7 being set st b5 = b1 . b4 & b6 = b2 . b4 & b7 = b3 . b4 holds
( b1 . (b4 + 1) = F4(b5,b7,b4) & b2 . (b4 + 1) = F5(b5,b6,b7,b4) & b3 . (b4 + 1) = F6(b7,b4) ) ) )
proof end;

scheme :: CIRCCMB2:sch 13
s13{ F1( set , set , set ) -> non empty ManySortedSign , F2( set , set , set , set ) -> set , F3( set , set ) -> set , P1[ set , set , set , set ], F4() -> ManySortedSet of NAT , F5() -> ManySortedSet of NAT , F6() -> ManySortedSet of NAT } :
for b1 being Nat ex b2 being non empty ManySortedSign ex b3 being non-empty MSAlgebra of b2 st
( b2 = F4() . b1 & b3 = F5() . b1 & P1[b2,b3,F6() . b1,b1] )
provided
E8: ex b1 being non empty ManySortedSign ex b2 being non-empty MSAlgebra of b1ex b3 being set st
( b1 = F4() . 0 & b2 = F5() . 0 & b3 = F6() . 0 & P1[b1,b2,b3,0] ) and
E9: for b1 being Nat
for b2 being non empty ManySortedSign
for b3 being non-empty MSAlgebra of b2
for b4 being set st b2 = F4() . b1 & b3 = F5() . b1 & b4 = F6() . b1 holds
( F4() . (b1 + 1) = F1(b2,b4,b1) & F5() . (b1 + 1) = F2(b2,b3,b4,b1) & F6() . (b1 + 1) = F3(b4,b1) ) and
E10: for b1 being Nat
for b2 being non empty ManySortedSign
for b3 being non-empty MSAlgebra of b2
for b4 being set st b2 = F4() . b1 & b3 = F5() . b1 & b4 = F6() . b1 & P1[b2,b3,b4,b1] holds
P1[F1(b2,b4,b1),F2(b2,b3,b4,b1),F3(b4,b1),b1 + 1] and
E11: for b1 being non empty ManySortedSign
for b2 being non-empty MSAlgebra of b1
for b3 being set
for b4 being Nat holds F2(b1,b2,b3,b4) is non-empty MSAlgebra of F1(b1,b3,b4)
proof end;

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

scheme :: CIRCCMB2:sch 14
s14{ F1( set , set , set ) -> non empty ManySortedSign , F2( set , set , set , set ) -> set , F3( set , set ) -> set , 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
E8: ex b1 being non empty ManySortedSign ex b2 being non-empty MSAlgebra of b1 st
( b1 = F4() . 0 & b2 = F6() . 0 ) and
E9: ( F4() . 0 = F5() . 0 & F6() . 0 = F7() . 0 & F8() . 0 = F9() . 0 ) and
E10: for b1 being Nat
for b2 being non empty ManySortedSign
for b3 being non-empty MSAlgebra of b2
for b4 being set st b2 = F4() . b1 & b3 = F6() . b1 & b4 = F8() . b1 holds
( F4() . (b1 + 1) = F1(b2,b4,b1) & F6() . (b1 + 1) = F2(b2,b3,b4,b1) & F8() . (b1 + 1) = F3(b4,b1) ) and
E11: for b1 being Nat
for b2 being non empty ManySortedSign
for b3 being non-empty MSAlgebra of b2
for b4 being set st b2 = F5() . b1 & b3 = F7() . b1 & b4 = F9() . b1 holds
( F5() . (b1 + 1) = F1(b2,b4,b1) & F7() . (b1 + 1) = F2(b2,b3,b4,b1) & F9() . (b1 + 1) = F3(b4,b1) ) and
E12: for b1 being non empty ManySortedSign
for b2 being non-empty MSAlgebra of b1
for b3 being set
for b4 being Nat holds F2(b1,b2,b3,b4) is non-empty MSAlgebra of F1(b1,b3,b4)
proof end;

scheme :: CIRCCMB2:sch 15
s15{ F1() -> non empty ManySortedSign , F2() -> non-empty MSAlgebra of F1(), F3( set , set , set ) -> non empty ManySortedSign , F4( set , set , set , set ) -> set , F5( set , set ) -> set , F6() -> ManySortedSet of NAT , F7() -> ManySortedSet of NAT , F8() -> ManySortedSet of NAT } :
for b1 being Nat
for b2 being non empty ManySortedSign
for b3 being set st b2 = F6() . b1 & b3 = F8() . b1 holds
( F6() . (b1 + 1) = F3(b2,b3,b1) & F8() . (b1 + 1) = F5(b3,b1) )
provided
E8: ( F6() . 0 = F1() & F7() . 0 = F2() ) and
E9: for b1 being Nat
for b2 being non empty ManySortedSign
for b3 being non-empty MSAlgebra of b2
for b4 being set st b2 = F6() . b1 & b3 = F7() . b1 & b4 = F8() . b1 holds
( F6() . (b1 + 1) = F3(b2,b4,b1) & F7() . (b1 + 1) = F4(b2,b3,b4,b1) & F8() . (b1 + 1) = F5(b4,b1) ) and
E10: for b1 being non empty ManySortedSign
for b2 being non-empty MSAlgebra of b1
for b3 being set
for b4 being Nat holds F4(b1,b2,b3,b4) is non-empty MSAlgebra of F3(b1,b3,b4)
proof end;

scheme :: CIRCCMB2:sch 16
s16{ F1() -> non empty ManySortedSign , F2() -> non-empty MSAlgebra of F1(), F3() -> set , F4( set , set , set ) -> non empty ManySortedSign , F5( set , set , set , set ) -> set , F6( set , set ) -> set , F7() -> Nat } :
ex b1 being non empty ManySortedSign ex b2 being non-empty MSAlgebra of b1ex b3, b4, b5 being ManySortedSet of NAT st
( b1 = b3 . F7() & b2 = b4 . F7() & b3 . 0 = F1() & b4 . 0 = F2() & b5 . 0 = F3() & ( for b6 being Nat
for b7 being non empty ManySortedSign
for b8 being non-empty MSAlgebra of b7
for b9 being set st b7 = b3 . b6 & b8 = b4 . b6 & b9 = b5 . b6 holds
( b3 . (b6 + 1) = F4(b7,b9,b6) & b4 . (b6 + 1) = F5(b7,b8,b9,b6) & b5 . (b6 + 1) = F6(b9,b6) ) ) )
provided
E8: for b1 being non empty ManySortedSign
for b2 being non-empty MSAlgebra of b1
for b3 being set
for b4 being Nat holds F5(b1,b2,b3,b4) is non-empty MSAlgebra of F4(b1,b3,b4)
proof end;

scheme :: CIRCCMB2:sch 17
s17{ F1() -> non empty ManySortedSign , F2() -> non empty ManySortedSign , F3() -> non-empty MSAlgebra of F1(), F4() -> set , F5( set , set , set ) -> non empty ManySortedSign , F6( set , set , set , set ) -> set , F7( set , set ) -> set , F8() -> Nat } :
ex b1 being non-empty MSAlgebra of F2()ex b2, b3, b4 being ManySortedSet of NAT st
( F2() = b2 . F8() & b1 = b3 . F8() & b2 . 0 = F1() & b3 . 0 = F3() & b4 . 0 = F4() & ( for b5 being Nat
for b6 being non empty ManySortedSign
for b7 being non-empty MSAlgebra of b6
for b8 being set st b6 = b2 . b5 & b7 = b3 . b5 & b8 = b4 . b5 holds
( b2 . (b5 + 1) = F5(b6,b8,b5) & b3 . (b5 + 1) = F6(b6,b7,b8,b5) & b4 . (b5 + 1) = F7(b8,b5) ) ) )
provided
E8: ex b1, b2 being ManySortedSet of NAT st
( F2() = b1 . F8() & b1 . 0 = F1() & b2 . 0 = F4() & ( for b3 being Nat
for b4 being non empty ManySortedSign
for b5 being set st b4 = b1 . b3 & b5 = b2 . b3 holds
( b1 . (b3 + 1) = F5(b4,b5,b3) & b2 . (b3 + 1) = F7(b5,b3) ) ) ) and
E9: for b1 being non empty ManySortedSign
for b2 being non-empty MSAlgebra of b1
for b3 being set
for b4 being Nat holds F6(b1,b2,b3,b4) is non-empty MSAlgebra of F5(b1,b3,b4)
proof end;

scheme :: CIRCCMB2:sch 18
s18{ F1() -> non empty ManySortedSign , F2() -> non empty ManySortedSign , F3() -> non-empty MSAlgebra of F1(), F4() -> set , F5( set , set , set ) -> non empty ManySortedSign , F6( set , set , set , set ) -> set , F7( set , set ) -> set , F8() -> Nat } :
for b1, b2 being non-empty MSAlgebra of F2() st ex b3, b4, b5 being ManySortedSet of NAT st
( F2() = b3 . F8() & b1 = b4 . F8() & b3 . 0 = F1() & b4 . 0 = F3() & b5 . 0 = F4() & ( for b6 being Nat
for b7 being non empty ManySortedSign
for b8 being non-empty MSAlgebra of b7
for b9 being set st b7 = b3 . b6 & b8 = b4 . b6 & b9 = b5 . b6 holds
( b3 . (b6 + 1) = F5(b7,b9,b6) & b4 . (b6 + 1) = F6(b7,b8,b9,b6) & b5 . (b6 + 1) = F7(b9,b6) ) ) ) & ex b3, b4, b5 being ManySortedSet of NAT st
( F2() = b3 . F8() & b2 = b4 . F8() & b3 . 0 = F1() & b4 . 0 = F3() & b5 . 0 = F4() & ( for b6 being Nat
for b7 being non empty ManySortedSign
for b8 being non-empty MSAlgebra of b7
for b9 being set st b7 = b3 . b6 & b8 = b4 . b6 & b9 = b5 . b6 holds
( b3 . (b6 + 1) = F5(b7,b9,b6) & b4 . (b6 + 1) = F6(b7,b8,b9,b6) & b5 . (b6 + 1) = F7(b9,b6) ) ) ) holds
b1 = b2
provided
E8: for b1 being non empty ManySortedSign
for b2 being non-empty MSAlgebra of b1
for b3 being set
for b4 being Nat holds F6(b1,b2,b3,b4) is non-empty MSAlgebra of F5(b1,b3,b4)
proof end;

scheme :: CIRCCMB2:sch 19
s19{ F1() -> non empty strict non void unsplit gate`1=arity gate`2isBoolean ManySortedSign , F2() -> non empty strict non void unsplit gate`1=arity gate`2isBoolean ManySortedSign , F3() -> strict gate`2=den Boolean Circuit of F1(), F4( set , set , set ) -> non empty ManySortedSign , F5( set , set , set , set ) -> set , F6() -> set , F7( set , set ) -> set , F8() -> Nat } :
ex b1 being strict gate`2=den Boolean Circuit of F2()ex b2, b3, b4 being ManySortedSet of NAT st
( F2() = b2 . F8() & b1 = b3 . F8() & b2 . 0 = F1() & b3 . 0 = F3() & b4 . 0 = F6() & ( for b5 being Nat
for b6 being non empty ManySortedSign
for b7 being non-empty MSAlgebra of b6
for b8 being set st b6 = b2 . b5 & b7 = b3 . b5 & b8 = b4 . b5 holds
( b2 . (b5 + 1) = F4(b6,b8,b5) & b3 . (b5 + 1) = F5(b6,b7,b8,b5) & b4 . (b5 + 1) = F7(b8,b5) ) ) )
provided
E8: for b1 being non empty strict non void unsplit gate`1=arity gate`2isBoolean ManySortedSign
for b2 being set
for b3 being Nat holds
( F4(b1,b2,b3) is unsplit & F4(b1,b2,b3) is gate`1=arity & F4(b1,b2,b3) is gate`2isBoolean & not F4(b1,b2,b3) is void & F4(b1,b2,b3) is strict ) and
E9: ex b1, b2 being ManySortedSet of NAT st
( F2() = b1 . F8() & b1 . 0 = F1() & b2 . 0 = F6() & ( for b3 being Nat
for b4 being non empty ManySortedSign
for b5 being set st b4 = b1 . b3 & b5 = b2 . b3 holds
( b1 . (b3 + 1) = F4(b4,b5,b3) & b2 . (b3 + 1) = F7(b5,b3) ) ) ) and
E10: for b1 being non empty ManySortedSign
for b2 being non-empty MSAlgebra of b1
for b3 being set
for b4 being Nat holds F5(b1,b2,b3,b4) is non-empty MSAlgebra of F4(b1,b3,b4) and
E11: for b1, b2 being non empty strict non void unsplit gate`1=arity gate`2isBoolean ManySortedSign
for b3 being strict gate`2=den Boolean Circuit of b1
for b4 being set
for b5 being Nat st b2 = F4(b1,b4,b5) holds
F5(b1,b3,b4,b5) is strict gate`2=den Boolean Circuit of b2
proof end;

definition
let c1 be non empty ManySortedSign ;
let c2 be set ;
assume E8: c2 is non-empty MSAlgebra of c1 ;
func MSAlg c2,c1 -> non-empty MSAlgebra of a1 means :Def1: :: CIRCCMB2:def 1
a3 = a2;
existence
ex b1 being non-empty MSAlgebra of c1 st b1 = c2 by E8;
uniqueness
for b1, b2 being non-empty MSAlgebra of c1 st b1 = c2 & b2 = c2 holds
b1 = b2 ;
end;

:: deftheorem Def1 defines MSAlg CIRCCMB2:def 1 :
for b1 being non empty ManySortedSign
for b2 being set st b2 is non-empty MSAlgebra of b1 holds
for b3 being non-empty MSAlgebra of b1 holds
( b3 = MSAlg b2,b1 iff b3 = b2 );

scheme :: CIRCCMB2:sch 20
s20{ F1() -> non empty strict non void unsplit gate`1=arity gate`2isBoolean ManySortedSign , F2() -> non empty strict non void unsplit gate`1=arity gate`2isBoolean ManySortedSign , F3() -> strict gate`2=den Boolean Circuit of F1(), F4( set , set ) -> non empty non void unsplit gate`1=arity gate`2isBoolean ManySortedSign , F5( set , set ) -> set , F6() -> set , F7( set , set ) -> set , F8() -> Nat } :
ex b1 being strict gate`2=den Boolean Circuit of F2()ex b2, b3, b4 being ManySortedSet of NAT st
( F2() = b2 . F8() & b1 = b3 . F8() & b2 . 0 = F1() & b3 . 0 = F3() & b4 . 0 = F6() & ( for b5 being Nat
for b6 being non empty ManySortedSign
for b7 being non-empty MSAlgebra of b6
for b8 being set
for b9 being non-empty MSAlgebra of F4(b8,b5) st b6 = b2 . b5 & b7 = b3 . b5 & b8 = b4 . b5 & b9 = F5(b8,b5) holds
( b2 . (b5 + 1) = b6 +* F4(b8,b5) & b3 . (b5 + 1) = b7 +* b9 & b4 . (b5 + 1) = F7(b8,b5) ) ) )
provided
E9: ex b1, b2 being ManySortedSet of NAT st
( F2() = b1 . F8() & b1 . 0 = F1() & b2 . 0 = F6() & ( for b3 being Nat
for b4 being non empty ManySortedSign
for b5 being set st b4 = b1 . b3 & b5 = b2 . b3 holds
( b1 . (b3 + 1) = b4 +* F4(b5,b3) & b2 . (b3 + 1) = F7(b5,b3) ) ) ) and
E10: for b1 being set
for b2 being Nat holds F5(b1,b2) is strict gate`2=den Boolean Circuit of F4(b1,b2)
proof end;

scheme :: CIRCCMB2:sch 21
s21{ F1() -> non empty ManySortedSign , F2() -> non empty strict non void unsplit gate`1=arity gate`2isBoolean ManySortedSign , F3() -> non-empty MSAlgebra of F1(), F4() -> set , F5( set , set , set ) -> non empty ManySortedSign , F6( set , set , set , set ) -> set , F7( set , set ) -> set , F8() -> Nat } :
for b1, b2 being strict gate`2=den Boolean Circuit of F2() st ex b3, b4, b5 being ManySortedSet of NAT st
( F2() = b3 . F8() & b1 = b4 . F8() & b3 . 0 = F1() & b4 . 0 = F3() & b5 . 0 = F4() & ( for b6 being Nat
for b7 being non empty ManySortedSign
for b8 being non-empty MSAlgebra of b7
for b9 being set st b7 = b3 . b6 & b8 = b4 . b6 & b9 = b5 . b6 holds
( b3 . (b6 + 1) = F5(b7,b9,b6) & b4 . (b6 + 1) = F6(b7,b8,b9,b6) & b5 . (b6 + 1) = F7(b9,b6) ) ) ) & ex b3, b4, b5 being ManySortedSet of NAT st
( F2() = b3 . F8() & b2 = b4 . F8() & b3 . 0 = F1() & b4 . 0 = F3() & b5 . 0 = F4() & ( for b6 being Nat
for b7 being non empty ManySortedSign
for b8 being non-empty MSAlgebra of b7
for b9 being set st b7 = b3 . b6 & b8 = b4 . b6 & b9 = b5 . b6 holds
( b3 . (b6 + 1) = F5(b7,b9,b6) & b4 . (b6 + 1) = F6(b7,b8,b9,b6) & b5 . (b6 + 1) = F7(b9,b6) ) ) ) holds
b1 = b2
provided
E9: for b1 being non empty ManySortedSign
for b2 being non-empty MSAlgebra of b1
for b3 being set
for b4 being Nat holds F6(b1,b2,b3,b4) is non-empty MSAlgebra of F5(b1,b3,b4)
proof end;

theorem Th10: :: CIRCCMB2:10
for b1, b2, b3 being non empty non void Circuit-like ManySortedSign st InnerVertices b1 misses InputVertices b2 & b3 = b1 +* b2 holds
for b4 being non-empty Circuit of b1
for b5 being non-empty Circuit of b2
for b6 being non-empty Circuit of b3 st b4 tolerates b5 & b6 = b4 +* b5 holds
for b7 being State of b5
for b8 being State of b6 st b7 = b8 | the carrier of b2 holds
Following b7 = (Following b8) | the carrier of b2
proof end;

theorem Th11: :: CIRCCMB2:11
for b1, b2, b3 being non empty non void Circuit-like ManySortedSign st InputVertices b1 misses InnerVertices b2 & b3 = b1 +* b2 holds
for b4 being non-empty Circuit of b1
for b5 being non-empty Circuit of b2
for b6 being non-empty Circuit of b3 st b4 tolerates b5 & b6 = b4 +* b5 holds
for b7 being State of b4
for b8 being State of b6 st b7 = b8 | the carrier of b1 holds
Following b7 = (Following b8) | the carrier of b1
proof end;

theorem Th12: :: CIRCCMB2:12
for b1, b2, b3 being non empty non void Circuit-like ManySortedSign st b1 tolerates b2 & InnerVertices b1 misses InputVertices b2 & b3 = b1 +* b2 holds
for b4 being non-empty Circuit of b1
for b5 being non-empty Circuit of b2
for b6 being non-empty Circuit of b3 st b4 tolerates b5 & b6 = b4 +* b5 holds
for b7 being State of b4
for b8 being State of b5
for b9 being State of b6 st b7 = b9 | the carrier of b1 & b8 = b9 | the carrier of b2 & b7 is stable & b8 is stable holds
b9 is stable
proof end;

theorem Th13: :: CIRCCMB2:13
for b1, b2, b3 being non empty non void Circuit-like ManySortedSign st b1 tolerates b2 & InputVertices b1 misses InnerVertices b2 & b3 = b1 +* b2 holds
for b4 being non-empty Circuit of b1
for b5 being non-empty Circuit of b2
for b6 being non-empty Circuit of b3 st b4 tolerates b5 & b6 = b4 +* b5 holds
for b7 being State of b4
for b8 being State of b5
for b9 being State of b6 st b7 = b9 | the carrier of b1 & b8 = b9 | the carrier of b2 & b7 is stable & b8 is stable holds
b9 is stable
proof end;

theorem Th14: :: CIRCCMB2:14
for b1, b2, b3 being non empty non void Circuit-like ManySortedSign st InputVertices b1 misses InnerVertices b2 & b3 = b1 +* b2 holds
for b4 being non-empty Circuit of b1
for b5 being non-empty Circuit of b2
for b6 being non-empty Circuit of b3 st b4 tolerates b5 & b6 = b4 +* b5 holds
for b7 being State of b6
for b8 being State of b4 st b8 = b7 | the carrier of b1 holds
for b9 being Nat holds (Following b7,b9) | the carrier of b1 = Following b8,b9
proof end;

theorem Th15: :: CIRCCMB2:15
for b1, b2, b3 being non empty non void Circuit-like ManySortedSign st InputVertices b2 misses InnerVertices b1 & b3 = b1 +* b2 holds
for b4 being non-empty Circuit of b1
for b5 being non-empty Circuit of b2
for b6 being non-empty Circuit of b3 st b4 tolerates b5 & b6 = b4 +* b5 holds
for b7 being State of b6
for b8 being State of b5 st b8 = b7 | the carrier of b2 holds
for b9 being Nat holds (Following b7,b9) | the carrier of b2 = Following b8,b9
proof end;

theorem Th16: :: CIRCCMB2:16
for b1, b2, b3 being non empty non void Circuit-like ManySortedSign st InputVertices b1 misses InnerVertices b2 & b3 = b1 +* b2 holds
for b4 being non-empty Circuit of b1
for b5 being non-empty Circuit of b2
for b6 being non-empty Circuit of b3 st b4 tolerates b5 & b6 = b4 +* b5 holds
for b7 being State of b6
for b8 being State of b4 st b8 = b7 | the carrier of b1 & b8 is stable holds
for b9 being State of b5 st b9 = b7 | the carrier of b2 holds
(Following b7) | the carrier of b2 = Following b9
proof end;

theorem Th17: :: CIRCCMB2:17
for b1, b2, b3 being non empty non void Circuit-like ManySortedSign st b3 = b1 +* b2 holds
for b4 being non-empty Circuit of b1
for b5 being non-empty Circuit of b2
for b6 being non-empty Circuit of b3 st b4 tolerates b5 & b6 = b4 +* b5 holds
for b7 being State of b6
for b8 being State of b4 st b8 = b7 | the carrier of b1 & b8 is stable holds
for b9 being State of b5 st b9 = b7 | the carrier of b2 & b9 is stable holds
b7 is stable
proof end;

theorem Th18: :: CIRCCMB2:18
for b1, b2, b3 being non empty non void Circuit-like ManySortedSign st b3 = b1 +* b2 holds
for b4 being non-empty Circuit of b1
for b5 being non-empty Circuit of b2
for b6 being non-empty Circuit of b3 st b4 tolerates b5 & b6 = b4 +* b5 holds
for b7 being State of b6 st b7 is stable holds
( ( for b8 being State of b4 st b8 = b7 | the carrier of b1 holds
b8 is stable ) & ( for b8 being State of b5 st b8 = b7 | the carrier of b2 holds
b8 is stable ) )
proof end;

theorem Th19: :: CIRCCMB2:19
for b1, b2, b3 being non empty non void Circuit-like ManySortedSign st InputVertices b1 misses InnerVertices b2 & b3 = b1 +* b2 holds
for b4 being non-empty Circuit of b1
for b5 being non-empty Circuit of b2
for b6 being non-empty Circuit of b3 st b4 tolerates b5 & b6 = b4 +* b5 holds
for b7 being State of b4
for b8 being State of b5
for b9 being State of b6 st b7 = b9 | the carrier of b1 & b8 = b9 | the carrier of b2 & b7 is stable holds
for b10 being Nat holds (Following b9,b10) | the carrier of b2 = Following b8,b10
proof end;

theorem Th20: :: CIRCCMB2:20
for b1, b2, b3 being non empty non void Circuit-like ManySortedSign st InputVertices b1 misses InnerVertices b2 & b3 = b1 +* b2 holds
for b4 being non-empty Circuit of b1
for b5 being non-empty Circuit of b2
for b6 being non-empty Circuit of b3 st b4 tolerates b5 & b6 = b4 +* b5 holds
for b7, b8 being Nat
for b9 being State of b6
for b10 being State of b4
for b11 being State of b5 st b10 = b9 | the carrier of b1 & Following b10,b7 is stable & b11 = (Following b9,b7) | the carrier of b2 & Following b11,b8 is stable holds
Following b9,(b7 + b8) is stable
proof end;

theorem Th21: :: CIRCCMB2:21
for b1, b2, b3 being non empty non void Circuit-like ManySortedSign st InputVertices b1 misses InnerVertices b2 & b3 = b1 +* b2 holds
for b4 being non-empty Circuit of b1
for b5 being non-empty Circuit of b2
for b6 being non-empty Circuit of b3 st b4 tolerates b5 & b6 = b4 +* b5 holds
for b7, b8 being Nat st ( for b9 being State of b4 holds Following b9,b7 is stable ) & ( for b9 being State of b5 holds Following b9,b8 is stable ) holds
for b9 being State of b6 holds Following b9,(b7 + b8) is stable
proof end;

theorem Th22: :: CIRCCMB2:22
for b1, b2, b3 being non empty non void Circuit-like ManySortedSign st InputVertices b1 misses InnerVertices b2 & InputVertices b2 misses InnerVertices b1 & b3 = b1 +* b2 holds
for b4 being non-empty Circuit of b1
for b5 being non-empty Circuit of b2
for b6 being non-empty Circuit of b3 st b4 tolerates b5 & b6 = b4 +* b5 holds
for b7 being State of b6
for b8 being State of b4 st b8 = b7 | the carrier of b1 holds
for b9 being State of b5 st b9 = b7 | the carrier of b2 holds
for b10 being Nat holds Following b7,b10 = (Following b8,b10) +* (Following b9,b10)
proof end;

theorem Th23: :: CIRCCMB2:23
for b1, b2, b3 being non empty non void Circuit-like ManySortedSign st InputVertices b1 misses InnerVertices b2 & InputVertices b2 misses InnerVertices b1 & b3 = b1 +* b2 holds
for b4 being non-empty Circuit of b1
for b5 being non-empty Circuit of b2
for b6 being non-empty Circuit of b3 st b4 tolerates b5 & b6 = b4 +* b5 holds
for b7, b8 being Nat
for b9 being State of b6
for b10 being State of b4 st b10 = b9 | the carrier of b1 holds
for b11 being State of b5 st b11 = b9 | the carrier of b2 & Following b10,b7 is stable & Following b11,b8 is stable holds
Following b9,(max b7,b8) is stable
proof end;

theorem Th24: :: CIRCCMB2:24
for b1, b2, b3 being non empty non void Circuit-like ManySortedSign st InputVertices b1 misses InnerVertices b2 & InputVertices b2 misses InnerVertices b1 & b3 = b1 +* b2 holds
for b4 being non-empty Circuit of b1
for b5 being non-empty Circuit of b2
for b6 being non-empty Circuit of b3 st b4 tolerates b5 & b6 = b4 +* b5 holds
for b7 being Nat
for b8 being State of b6
for b9 being State of b4 st b9 = b8 | the carrier of b1 holds
for b10 being State of b5 st b10 = b8 | the carrier of b2 & ( not Following b9,b7 is stable or not Following b10,b7 is stable ) holds
not Following b8,b7 is stable
proof end;

theorem Th25: :: CIRCCMB2:25
for b1, b2, b3 being non empty non void Circuit-like ManySortedSign st InputVertices b1 misses InnerVertices b2 & InputVertices b2 misses InnerVertices b1 & b3 = b1 +* b2 holds
for b4 being non-empty Circuit of b1
for b5 being non-empty Circuit of b2
for b6 being non-empty Circuit of b3 st b4 tolerates b5 & b6 = b4 +* b5 holds
for b7, b8 being Nat st ( for b9 being State of b4 holds Following b9,b7 is stable ) & ( for b9 being State of b5 holds Following b9,b8 is stable ) holds
for b9 being State of b6 holds Following b9,(max b7,b8) is stable
proof end;

scheme :: CIRCCMB2:sch 22
s22{ F1() -> non empty strict non void unsplit gate`1=arity gate`2isBoolean ManySortedSign , F2() -> non empty strict non void 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( set , set ) -> non empty strict non void unsplit gate`1=arity gate`2isBoolean ManySortedSign , F6( set , set ) -> set , F7() -> ManySortedSet of NAT , F8() -> set , F9( set , set ) -> set , F10( Nat) -> Nat } :
for b1 being State of F4() holds Following b1,(F10(0) + (F10(2) * F10(1))) is stable
provided
E19: for b1 being set
for b2 being Nat holds F6(b1,b2) is strict gate`2=den Boolean Circuit of F5(b1,b2) and
E20: for b1 being State of F3() holds Following b1,F10(0) is stable and
E21: for b1 being Nat
for b2 being set
for b3 being non-empty Circuit of F5(b2,b1) st b2 = F7() . b1 & b3 = F6(b2,b1) holds
for b4 being State of b3 holds Following b4,F10(1) is stable and
E22: ex b1, b2 being ManySortedSet of NAT st
( F2() = b1 . F10(2) & F4() = b2 . F10(2) & b1 . 0 = F1() & b2 . 0 = F3() & F7() . 0 = F8() & ( for b3 being Nat
for b4 being non empty ManySortedSign
for b5 being non-empty MSAlgebra of b4
for b6 being set
for b7 being non-empty MSAlgebra of F5(b6,b3) st b4 = b1 . b3 & b5 = b2 . b3 & b6 = F7() . b3 & b7 = F6(b6,b3) holds
( b1 . (b3 + 1) = b4 +* F5(b6,b3) & b2 . (b3 + 1) = b5 +* b7 & F7() . (b3 + 1) = F9(b6,b3) ) ) ) and
E23: ( InnerVertices F1() is Relation & not InputVertices F1() is with_pair ) and
E24: ( F7() . 0 = F8() & F8() in InnerVertices F1() ) and
E25: for b1 being Nat
for b2 being set holds InnerVertices F5(b2,b1) is Relation and
E26: for b1 being Nat
for b2 being set st b2 = F7() . b1 holds
not (InputVertices F5(b2,b1)) \ {b2} is with_pair and
E27: for b1 being Nat
for b2 being set st b2 = F7() . b1 holds
( F7() . (b1 + 1) = F9(b2,b1) & b2 in InputVertices F5(b2,b1) & F9(b2,b1) in InnerVertices F5(b2,b1) )
proof end;