:: CIRCCMB2 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

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:69;
end;

theorem Th1: :: CIRCCMB2:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Nat holds Following s,n = s
proof end;

theorem Th4: :: CIRCCMB2:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Nat st Following s,n1 is stable & n1 <= n2 holds
Following s,n2 = Following s,n1
proof end;

scheme :: CIRCCMB2:sch 1
CIRCCMB2'sch1{ F1() -> non empty ManySortedSign , F2() -> set , F3( set , set , set ) -> non empty ManySortedSign , F4( set , set ) -> set } :
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
CIRCCMB2'sch2{ F1( set , set , set ) -> non empty ManySortedSign , F2( set , set ) -> set , P1[ set , set , set ], 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[ set , set , set ] means verum;

scheme :: CIRCCMB2:sch 3
CIRCCMB2'sch3{ F1() -> non empty ManySortedSign , F2( set , set , set ) -> non empty ManySortedSign , F3( set , set ) -> set , 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
CIRCCMB2'sch4{ F1() -> non empty ManySortedSign , F2() -> set , F3( set , set , set ) -> non empty ManySortedSign , F4( set , set ) -> set , 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
CIRCCMB2'sch5{ F1() -> non empty ManySortedSign , F2() -> set , F3( set , set , set ) -> non empty ManySortedSign , F4( set , set ) -> set , 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
CIRCCMB2'sch6{ F1() -> non empty ManySortedSign , F2() -> set , F3( set , set , set ) -> non empty ManySortedSign , F4( set , set ) -> set , 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
CIRCCMB2'sch7{ F1() -> non empty ManySortedSign , F2( set , set , set ) -> non empty ManySortedSign , F3() -> set , F4( set , set ) -> set , F5() -> Nat } :
ex S being non empty strict non void 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 strict non void 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
CIRCCMB2'sch8{ 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 S being non empty strict non void 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
CIRCCMB2'sch9{ F1() -> non empty ManySortedSign , F2() -> set , F3( set , set , set ) -> non empty ManySortedSign , F4( set , set ) -> set , F5() -> Nat } :
for S1, S2 being non empty strict non void 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f, g being Function st f tolerates g holds
rng (f +* g) = (rng f) \/ (rng g)
proof end;

theorem Th6: :: CIRCCMB2:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Th7: :: CIRCCMB2:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being without_pairs set
for Y being Relation holds X \ Y = X
proof end;

theorem :: CIRCCMB2:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being Relation
for Y, Z being set st Z c= Y & not Y \ Z is with_pair holds
X \ Y = X \ Z
proof end;

theorem Th9: :: CIRCCMB2:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, Z being set
for Y being Relation st Z c= Y & not X \ Z is with_pair holds
X \ Y = X \ Z
proof end;

scheme :: CIRCCMB2:sch 10
CIRCCMB2'sch10{ 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 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 & not InputVertices S1 is with_pair )
provided
A1: InnerVertices F1() is Relation and
A2: not InputVertices F1() is with_pair 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
not (InputVertices F4(x,n)) \ {x} is with_pair 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
CIRCCMB2'sch11{ 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 n being Nat holds
( InputVertices F1((n + 1)) = (InputVertices F1(n)) \/ ((InputVertices F3((F2() . n),n)) \ {(F2() . n)}) & InnerVertices F1(n) is Relation & not InputVertices F1(n) is with_pair )
provided
A1: InnerVertices F1(0) is Relation and
A2: not InputVertices F1(0) is with_pair 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
not (InputVertices F3(x,n)) \ {x} is with_pair 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
CIRCCMB2'sch12{ 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 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 of 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
CIRCCMB2'sch13{ 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 n being Nat ex S being non empty ManySortedSign ex A being non-empty MSAlgebra of 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 of 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 of 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 of 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 of S
for x being set
for n being Nat holds F2(S,A,x,n) is non-empty MSAlgebra of F1(S,x,n)
proof end;

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

scheme :: CIRCCMB2:sch 14
CIRCCMB2'sch14{ 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
A1: ex S being non empty ManySortedSign ex A being non-empty MSAlgebra of 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 of 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 of 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 of S
for x being set
for n being Nat holds F2(S,A,x,n) is non-empty MSAlgebra of F1(S,x,n)
proof end;

scheme :: CIRCCMB2:sch 15
CIRCCMB2'sch15{ 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 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 of 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 of S
for x being set
for n being Nat holds F4(S,A,x,n) is non-empty MSAlgebra of F3(S,x,n)
proof end;

scheme :: CIRCCMB2:sch 16
CIRCCMB2'sch16{ 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 S being non empty ManySortedSign ex A being non-empty MSAlgebra of 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 of 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 of S
for x being set
for n being Nat holds F5(S,A,x,n) is non-empty MSAlgebra of F4(S,x,n)
proof end;

scheme :: CIRCCMB2:sch 17
CIRCCMB2'sch17{ 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 A being non-empty MSAlgebra 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 = F4() & ( for n being Nat
for S being non empty ManySortedSign
for A being non-empty MSAlgebra of 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 of S
for x being set
for n being Nat holds F6(S,A,x,n) is non-empty MSAlgebra of F5(S,x,n)
proof end;

scheme :: CIRCCMB2:sch 18
CIRCCMB2'sch18{ 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 A1, A2 being non-empty MSAlgebra 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 of 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 of 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 of S
for x being set
for n being Nat holds F6(S,A,x,n) is non-empty MSAlgebra of F5(S,x,n)
proof end;

scheme :: CIRCCMB2:sch 19
CIRCCMB2'sch19{ 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 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 of 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 strict non void 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 of S
for x being set
for n being Nat holds F5(S,A,x,n) is non-empty MSAlgebra of F4(S,x,n) and
A4: for S, S1 being non empty strict non void 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 set ;
assume A1: A is non-empty MSAlgebra of S ;
func MSAlg A,S -> non-empty MSAlgebra of S means :Def1: :: CIRCCMB2:def 1
it = A;
existence
ex b1 being non-empty MSAlgebra of S st b1 = A by A1;
uniqueness
for b1, b2 being non-empty MSAlgebra of 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 set st A is non-empty MSAlgebra of S holds
for b3 being non-empty MSAlgebra of S holds
( b3 = MSAlg A,S iff b3 = A );

scheme :: CIRCCMB2:sch 20
CIRCCMB2'sch20{ 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 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 of S
for x being set
for A2 being non-empty MSAlgebra of 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
CIRCCMB2'sch21{ 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 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 of 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 of 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 of S
for x being set
for n being Nat holds F6(S,A,x,n) is non-empty MSAlgebra of F5(S,x,n)
proof end;

theorem :: CIRCCMB2:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Th11: :: CIRCCMB2:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S1, S2, S being non empty non void Circuit-like ManySortedSign st S1 tolerates S2 & 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:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S1, S2, S being non empty non void Circuit-like ManySortedSign st S1 tolerates S2 & 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 Th14: :: CIRCCMB2:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Nat holds (Following s,n) | the carrier of S1 = Following s1,n
proof end;

theorem Th15: :: CIRCCMB2:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Th16: :: CIRCCMB2:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Th18: :: CIRCCMB2:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Th19: :: CIRCCMB2:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Th20: :: CIRCCMB2:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Th21: :: CIRCCMB2:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Th22: :: CIRCCMB2:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Nat holds Following s,n = (Following s1,n) +* (Following s2,n)
proof end;

theorem Th23: :: CIRCCMB2:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
CIRCCMB2'sch22{ 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 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 of S
for x being set
for A2 being non-empty MSAlgebra of 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 & not InputVertices F1() is with_pair ) 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
not (InputVertices F5(x,n)) \ {x} is with_pair 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;