Combining of Multi Cell Circuits
JOURNAL OF FORMALIZED MATHEMATICS
V olume14,Released2002,Published2003
Inst.of Computer Science,Univ.of Bia?ystok
Combining of Multi Cell Circuits
Grzegorz Bancerek
Bia?ystok Technical University Shin’nosuke Yamaguchi Shinshu University
Nagano
Yasunari Shidama
Shinshu University
Nagano
Summary.In this article we continue the investigations from[10]and[2]of veri?ca-tion of a circuit design.We concentrate on the combination of multi cell circuits from given
cells(circuit modules).Namely,we formalize a design of the form
012n
and prove its stability.The formalization proposed consists in a series of schemes which al-
low to de?ne multi cells circuits and prove their properties.Our goal is to achive mathematical
formalization which will allow to verify designs of real circuits.
MML Identi?er:CIRCCMB2.
WWW:https://www.wendangku.net/doc/e65866735.html,/JFM/Vol14/circcmb2.html
The articles[14],[17],[1],[8],[18],[3],[5],[4],[6],[7],[9],[15],[16],[12],[11],[13],[10],and [2]provide the notation and terminology for this paper.
1.O NE G ATE C IRCUITS
Let n be a natural number,let f be a function from Boolean n into Boolean,and let p be a?nite sequence with length n.One can verify that1GateCircuit(p,f)is Boolean.
One can prove the following four propositions:
(1)Let X be a?nite non empty set,n be a natural number,p be a?nite sequence with length
n,f be a function from X n into X,o be an operation symbol of1GateCircStr(p,f),and s be
a state of1GateCircuit(p,f).Then o depends-on-in s=s·p.
1c Association of Mizar Users
(2)Let X be a?nite non empty set,n be a natural number,p be a?nite sequence with length
n,f be a function from X n into X,and s be a state of1GateCircuit(p,f).Then Following(s) is stable.
(3)Let S be a non void circuit-like non empty many sorted signature,A be a non-empty
circuit of S,and s be a state of A.If s is stable,then for every natural number n holds Following(s,n)=s.
(4)Let S be a non void circuit-like non empty many sorted signature,A be a non-empty circuit
of S,s be a state of A,and n1,n2be natural numbers.If Following(s,n1)is stable and n1≤n2, then Following(s,n2)=Following(s,n1).
2.D EFINING M ULTI C ELL C IRCUIT S TRUCTURES
In this article we present several logical schemes.The scheme CIRCCMB2’sch1deals with a non empty many sorted signature A,a set B,a ternary functor F yielding a non empty many sorted signature,and a binary functor G yielding a set,and states that:
There exist many sorted sets f,h indexed by N such that
(i)f(0)=A,
(ii)h(0)=B,and
(iii)for every natural number n and for every non empty many sorted signature S
and for every set x such that S=f(n)and x=h(n)holds f(n+1)=F(S,x,n)and
h(n+1)=G(x,n)
for all values of the parameters.
The scheme CIRCCMB2’sch2deals with a ternary functor F yielding a non empty many sorted signature,a binary functor G yielding a set,many sorted sets A,B indexed by N,and a ternary predicate P,and states that:
For every natural number n there exists a non empty many sorted signature S such
that S=A(n)and P[S,B(n),n]
provided the parameters meet the following requirements:
?There exists a non empty many sorted signature S and there exists a set x such that S=A(0)and x=B(0)and P[S,x,0],
?Let n be a natural number,S be a non empty many sorted signature,and x be a set.If S=A(n)and x=B(n),then A(n+1)=F(S,x,n)and B(n+1)=G(x,n),and ?Let n be a natural number,S be a non empty many sorted signature,and x be a set.If S=A(n)and x=B(n)and P[S,x,n],then P[F(S,x,n),G(x,n),n+1].
The scheme CIRCCMB2’sch3deals with a non empty many sorted signature A,a ternary func-tor F yielding a non empty many sorted signature,a binary functor G yielding a set,and many sorted sets B,C indexed by N,and states that:
For every natural number n and for every set x such that x=C(n)holds C(n+1)=
G(x,n)
provided the following requirements are met:
?B(0)=A,and
?Let n be a natural number,S be a non empty many sorted signature,and x be a set.If S=B(n)and x=C(n),then B(n+1)=F(S,x,n)and C(n+1)=G(x,n).
The scheme CIRCCMB2’sch4deals with a non empty many sorted signature A,a set B,a ternary functor F yielding a non empty many sorted signature,a binary functor G yielding a set, and a natural number C,and states that:
There exists a non empty many sorted signature S and there exist many sorted sets f,
h indexed by N such that
(i)S=f(C),
(ii)f(0)=A,
(iii)h(0)=B,and
(iv)for every natural number n and for every non empty many sorted signature S
and for every set x such that S=f(n)and x=h(n)holds f(n+1)=F(S,x,n)and
h(n+1)=G(x,n)
for all values of the parameters.
The scheme CIRCCMB2’sch5deals with a non empty many sorted signature A,a set B,a ternary functor F yielding a non empty many sorted signature,a binary functor G yielding a set, and a natural number C,and states that:
Let S1,S2be non empty many sorted signatures.Suppose that
(i)there exist many sorted sets f,h indexed by N such that S1=f(C)and f(0)=
A and h(0)=
B and for every natural number n and for every non empty many sorted
signature S and for every set x such that S=f(n)and x=h(n)holds f(n+1)=
F(S,x,n)and h(n+1)=G(x,n),and
(ii)there exist many sorted sets f,h indexed by N such that S2=f(C)and f(0)=
A and h(0)=
B and for every natural number n and for every non empty many sorted
signature S and for every set x such that S=f(n)and x=h(n)holds f(n+1)=
F(S,x,n)and h(n+1)=G(x,n).
Then S1=S2
for all values of the parameters.
The scheme CIRCCMB2’sch6deals with a non empty many sorted signature A,a set B,a ternary functor F yielding a non empty many sorted signature,a binary functor G yielding a set, and a natural number C,and states that:
(i)There exists a non empty many sorted signature S and there exist many sorted
sets f,h indexed by N such that S=f(C)and f(0)=A and h(0)=B and for every
natural number n and for every non empty many sorted signature S and for every set
x such that S=f(n)and x=h(n)holds f(n+1)=F(S,x,n)and h(n+1)=G(x,n),
and
(ii)for all non empty many sorted signatures S1,S2such that there exist many
sorted sets f,h indexed by N such that S1=f(C)and f(0)=A and h(0)=B
and for every natural number n and for every non empty many sorted signature S
and for every set x such that S=f(n)and x=h(n)holds f(n+1)=F(S,x,n)
and h(n+1)=G(x,n)and there exist many sorted sets f,h indexed by N such
that S2=f(C)and f(0)=A and h(0)=B and for every natural number n and for
every non empty many sorted signature S and for every set x such that S=f(n)and
x=h(n)holds f(n+1)=F(S,x,n)and h(n+1)=G(x,n)holds S1=S2
for all values of the parameters.
The scheme CIRCCMB2’sch7deals with a non empty many sorted signature A,a ternary func-tor F yielding a non empty many sorted signature,a set B,a binary functor G yielding a set,and a natural number C,and states that:
There exists an unsplit non void non empty non empty strict many sorted signature
S with arity held in gates and Boolean denotation held in gates and there exist many
sorted sets f,h indexed by N such that
(i)S=f(C),
(ii)f(0)=A,
(iii)h(0)=B,and
(iv)for every natural number n and for every non empty many sorted signature S
and for every set x such that S=f(n)and x=h(n)holds f(n+1)=F(S,x,n)and
h(n+1)=G(x,n)
provided the parameters have the following properties:
?A is unsplit,non void,non empty,and strict and has arity held in gates and Boolean denotation held in gates,and
?Let S be an unsplit non void strict non empty many sorted signature with arity held in gates and Boolean denotation held in gates,x be a set,and n be a natural number.
Then F(S,x,n)is unsplit,non void,non empty,and strict and has arity held in gates
and Boolean denotation held in gates.
The scheme CIRCCMB2’sch8deals with a non empty many sorted signature A,a binary functor F yielding an unsplit non void non empty many sorted signature with arity held in gates and Boolean denotation held in gates,a set B,a binary functor G yielding a set,and a natural number C,and states that:
There exists an unsplit non void non empty non empty strict many sorted signature
S with arity held in gates and Boolean denotation held in gates and there exist many
sorted sets f,h indexed by N such that
(i)S=f(C),
(ii)f(0)=A,
(iii)h(0)=B,and
(iv)for every natural number n and for every non empty many sorted signature S
and for every set x such that S=f(n)and x=h(n)holds f(n+1)=S+·F(x,n)and
h(n+1)=G(x,n)
provided the following requirement is met:
?A is unsplit,non void,non empty,and strict and has arity held in gates and Boolean denotation held in gates.
The scheme CIRCCMB2’sch9deals with a non empty many sorted signature A,a set B,a
ternary functor F yielding a non empty many sorted signature,a binary functor G yielding a set,
and a natural number C,and states that:
Let S1,S2be unsplit non void non empty strict non empty many sorted signatures
with arity held in gates and Boolean denotation held in gates.Suppose that
(i)there exist many sorted sets f,h indexed by N such that S1=f(C)and f(0)=
A and h(0)=
B and for every natural number n and for every non empty many sorted
signature S and for every set x such that S=f(n)and x=h(n)holds f(n+1)=
F(S,x,n)and h(n+1)=G(x,n),and
(ii)there exist many sorted sets f,h indexed by N such that S2=f(C)and f(0)=
A and h(0)=
B and for every natural number n and for every non empty many sorted
signature S and for every set x such that S=f(n)and x=h(n)holds f(n+1)=
F(S,x,n)and h(n+1)=G(x,n).
Then S1=S2
for all values of the parameters.
3.I NPUT OF M ULTI C ELL C IRCUIT
We now state several propositions:
(5)For all functions f,g such that f≈g holds rng(f+·g)=rng f∪rng g.
(6)For all non empty many sorted signatures S1,S2such that S1≈S2holds
InputVertices(S1+·S2)=(InputVertices(S1)\InnerVertices(S2))∪(InputVertices(S2)\InnerVertices(S1)).
(7)For every set X with no pairs and for every binary relation Y holds X\Y=X.
(8)For every binary relation X and for all sets Y,Z such that Z?Y and Y\Z has no pairs
holds X\Y=X\Z.
(9)For all sets X,Z and for every binary relation Y such that Z?Y and X\Z has no pairs
holds X\Y=X\Z.
Now we present two schemes.The scheme CIRCCMB2’sch10deals with an unsplit non void
non empty many sorted signature A with arity held in gates and Boolean denotation held in gates,
a unary functor F yielding a set,a many sorted set B indexed by N,a binary functor G yielding an
unsplit non void non empty many sorted signature with arity held in gates and Boolean denotation
held in gates,and a binary functor H yielding a set,and states that:
Let n be a natural number.Then there exist unsplit non void non empty many
sorted signatures S1,S2with arity held in gates and Boolean denotation held in gates
such that S1=F(n)and S2=F(n+1)and InputVertices(S2)=InputVertices(S1)∪
(InputVertices(G(B(n),n))\{B(n)})and InnerVertices(S1)is a binary relation and
InputVertices(S1)has no pairs
provided the parameters meet the following requirements:
?InnerVertices(A)is a binary relation,
?InputVertices(A)has no pairs,
?F(0)=A and B(0)∈InnerVertices(A),
?For every natural number n and for every set x holds InnerVertices(G(x,n))is a binary relation,
?For every natural number n and for every set x such that x=B(n)holds InputVertices(G(x,n))\ {x}has no pairs,and
?Let n be a natural number,S be a non empty many sorted signature,and x be a set.
Suppose S=F(n)and x=B(n).Then F(n+1)=S+·G(x,n)and B(n+1)=
H(x,n)and x∈InputVertices(G(x,n))and H(x,n)∈InnerVertices(G(x,n)).
The scheme CIRCCMB2’sch11deals with a unary functor F yielding an unsplit non void non empty many sorted signature with arity held in gates and Boolean denotation held in gates,a many sorted set A indexed by N,a binary functor G yielding an unsplit non void non empty many sorted signature with arity held in gates and Boolean denotation held in gates,and a binary functor H yielding a set,and states that:
For every natural number n holds InputVertices(F(n+1))=InputVertices(F(n))∪
(InputVertices(G(A(n),n))\{A(n)})and InnerVertices(F(n))is a binary relation
and InputVertices(F(n))has no pairs
provided the parameters have the following properties:
?InnerVertices(F(0))is a binary relation,
?InputVertices(F(0))has no pairs,
?A(0)∈InnerVertices(F(0)),
?For every natural number n and for every set x holds InnerVertices(G(x,n))is a binary relation,
?For every natural number n and for every set x such that x=A(n)holds InputVertices(G(x,n))\ {x}has no pairs,and
?Let n be a natural number,S be a non empty many sorted signature,and x be a set.
Suppose S=F(n)and x=A(n).Then F(n+1)=S+·G(x,n)and A(n+1)=
H(x,n)and x∈InputVertices(G(x,n))and H(x,n)∈InnerVertices(G(x,n)).
4.D EFINING M ULTI C ELL C IRCUITS
Now we present several schemes.The scheme CIRCCMB2’sch12deals with a non empty many sorted signature A,a non-empty algebra B over A,a set C,a ternary functor F yielding a non empty many sorted signature,a4-ary functor G yielding a set,and a binary functor H yielding a set,and states that:
There exist many sorted sets f,g,h indexed by N such that
(i)f(0)=A,
(ii)g(0)=B,
(iii)h(0)=C,and
(iv)for every natural number n and for every non empty many sorted signature S
and for every non-empty algebra A over S and for every set x such that S=f(n)and
A=g(n)and x=h(n)holds f(n+1)=F(S,x,n)and g(n+1)=G(S,A,x,n)and
h(n+1)=H(x,n)
for all values of the parameters.
The scheme CIRCCMB2’sch13deals with a ternary functor F yielding a non empty many sorted signature,a4-ary functor G yielding a set,a binary functor H yielding a set,many sorted sets A,B,C indexed by N,and a4-ary predicate P,and states that:
Let n be a natural number.Then there exists a non empty many sorted signature S
and there exists a non-empty algebra A over S such that S=A(n)and A=B(n)and
P[S,A,C(n),n]
provided the following conditions are met:
?There exists a non empty many sorted signature S and there exists a non-empty alge-bra A over S and there exists a set x such that S=A(0)and A=B(0)and x=C(0)
and P[S,A,x,0],
?Let n be a natural number,S be a non empty many sorted signature,A be a non-empty algebra over S,and x be a set.Suppose S=A(n)and A=B(n)and x=C(n).Then
A(n+1)=F(S,x,n)and B(n+1)=G(S,A,x,n)and C(n+1)=H(x,n),?Let n be a natural number,S be a non empty many sorted signature,A be a non-empty algebra over S,and x be a set.If S=A(n)and A=B(n)and x=C(n)and
P[S,A,x,n],then P[F(S,x,n),G(S,A,x,n),H(x,n),n+1],and
?Let S be a non empty many sorted signature,A be a non-empty algebra over S,x be a set,and n be a natural number.Then G(S,A,x,n)is a non-empty algebra over
F(S,x,n).
The scheme CIRCCMB2’sch14deals with a ternary functor F yielding a non empty many sorted signature,a4-ary functor G yielding a set,a binary functor H yielding a set,and many sorted sets A,B,C,D,E,F indexed by N,and states that:
A=B and C=D and E=F
provided the following conditions are satis?ed:
?There exists a non empty many sorted signature S and there exists a non-empty alge-bra A over S such that S=A(0)and A=C(0),
?A(0)=B(0)and C(0)=D(0)and E(0)=F(0),
?Let n be a natural number,S be a non empty many sorted signature,A be a non-empty algebra over S,and x be a set.Suppose S=A(n)and A=C(n)and x=E(n).Then
A(n+1)=F(S,x,n)and C(n+1)=G(S,A,x,n)and E(n+1)=H(x,n),?Let n be a natural number,S be a non empty many sorted signature,A be a non-empty algebra over S,and x be a set.Suppose S=B(n)and A=D(n)and x=F(n).Then
B(n+1)=F(S,x,n)and D(n+1)=G(S,A,x,n)and F(n+1)=H(x,n),and ?Let S be a non empty many sorted signature,A be a non-empty algebra over S,x be a set,and n be a natural number.Then G(S,A,x,n)is a non-empty algebra over
F(S,x,n).
The scheme CIRCCMB2’sch15deals with a non empty many sorted signature A,a non-empty algebra B over A,a ternary functor F yielding a non empty many sorted signature,a4-ary functor G yielding a set,a binary functor H yielding a set,and many sorted sets C,D,E indexed by N, and states that:
Let n be a natural number,S be a non empty many sorted signature,and x be a set.If
S=C(n)and x=E(n),then C(n+1)=F(S,x,n)and E(n+1)=H(x,n)
provided the parameters meet the following conditions:
?C(0)=A and D(0)=B,
?Let n be a natural number,S be a non empty many sorted signature,A be a non-empty algebra over S,and x be a set.Suppose S=C(n)and A=D(n)and x=E(n).Then
C(n+1)=F(S,x,n)and D(n+1)=G(S,A,x,n)and E(n+1)=H(x,n),and ?Let S be a non empty many sorted signature,A be a non-empty algebra over S,x be a set,and n be a natural number.Then G(S,A,x,n)is a non-empty algebra over
F(S,x,n).
The scheme CIRCCMB2’sch16deals with a non empty many sorted signature A,a non-empty algebra B over A,a set C,a ternary functor F yielding a non empty many sorted signature,a4-ary functor G yielding a set,a binary functor H yielding a set,and a natural number D,and states that: There exists a non empty many sorted signature S and there exists a non-empty alge-
bra A over S and there exist many sorted sets f,g,h indexed by N such that
(i)S=f(D),
(ii)A=g(D),
(iii)f(0)=A,
(iv)g(0)=B,
(v)h(0)=C,and
(vi)for every natural number n and for every non empty many sorted signature S
and for every non-empty algebra A over S and for every set x such that S=f(n)and
A=g(n)and x=h(n)holds f(n+1)=F(S,x,n)and g(n+1)=G(S,A,x,n)and
h(n+1)=H(x,n)
provided the following condition is satis?ed:
?Let S be a non empty many sorted signature,A be a non-empty algebra over S,x be a set,and n be a natural number.Then G(S,A,x,n)is a non-empty algebra over
F(S,x,n).
The scheme CIRCCMB2’sch17deals with non empty many sorted signatures A,B,a non-empty algebra C over A,a set D,a ternary functor F yielding a non empty many sorted signature, a4-ary functor G yielding a set,a binary functor H yielding a set,and a natural number E,and states that:
There exists a non-empty algebra A over B and there exist many sorted sets f,g,h
indexed by N such that
(i)B=f(E),
(ii)A=g(E),
(iii)f(0)=A,
(iv)g(0)=C,
(v)h(0)=D,and
(vi)for every natural number n and for every non empty many sorted signature S
and for every non-empty algebra A over S and for every set x such that S=f(n)and
A=g(n)and x=h(n)holds f(n+1)=F(S,x,n)and g(n+1)=G(S,A,x,n)and
h(n+1)=H(x,n)
provided the parameters meet the following conditions:
?There exist many sorted sets f,h indexed by N such that
(i)B=f(E),
(ii)f(0)=A,
(iii)h(0)=D,and
(iv)for every natural number n and for every non empty many sorted signature S
and for every set x such that S=f(n)and x=h(n)holds f(n+1)=F(S,x,n)and
h(n+1)=H(x,n),
and
?Let S be a non empty many sorted signature,A be a non-empty algebra over S,x be a set,and n be a natural number.Then G(S,A,x,n)is a non-empty algebra over
F(S,x,n).
The scheme CIRCCMB2’sch18deals with non empty many sorted signatures A,B,a non-empty algebra C over A,a set D,a ternary functor F yielding a non empty many sorted signature, a4-ary functor G yielding a set,a binary functor H yielding a set,and a natural number E,and states that:
Let A1,A2be non-empty algebras over B.Suppose that
(i)there exist many sorted sets f,g,h indexed by N such that B=f(E)and
A1=g(E)and f(0)=A and g(0)=C and h(0)=D and for every natural number
n and for every non empty many sorted signature S and for every non-empty algebra
A over S and for every set x such that S=f(n)and A=g(n)and x=h(n)holds
f(n+1)=F(S,x,n)and g(n+1)=G(S,A,x,n)and h(n+1)=H(x,n),and
(ii)there exist many sorted sets f,g,h indexed by N such that B=f(E)and
A2=g(E)and f(0)=A and g(0)=C and h(0)=D and for every natural number
n and for every non empty many sorted signature S and for every non-empty algebra
A over S and for every set x such that S=f(n)and A=g(n)and x=h(n)holds
f(n+1)=F(S,x,n)and g(n+1)=G(S,A,x,n)and h(n+1)=H(x,n).
Then A1=A2
provided the parameters satisfy the following condition:
?Let S be a non empty many sorted signature,A be a non-empty algebra over S,x be a set,and n be a natural number.Then G(S,A,x,n)is a non-empty algebra over
F(S,x,n).
The scheme CIRCCMB2’sch19deals with unsplit non void strict non empty many sorted signa-tures A,B with arity held in gates and Boolean denotation held in gates,a Boolean strict circuit C of A with denotation held in gates,a ternary functor F yielding a non empty many sorted signature, a4-ary functor G yielding a set,a set D,a binary functor H yielding a set,and a natural number E,and states that:
There exists a Boolean strict circuit A of B with denotation held in gates and there
exist many sorted sets f,g,h indexed by N such that
(i)B=f(E),
(ii)A=g(E),
(iii)f(0)=A,
(iv)g(0)=C,
(v)h(0)=D,and
(vi)for every natural number n and for every non empty many sorted signature S
and for every non-empty algebra A over S and for every set x such that S=f(n)and
A=g(n)and x=h(n)holds f(n+1)=F(S,x,n)and g(n+1)=G(S,A,x,n)and
h(n+1)=H(x,n)
provided the parameters satisfy the following conditions:
?Let S be an unsplit non void strict non empty many sorted signature with arity held in gates and Boolean denotation held in gates,x be a set,and n be a natural number.
Then F(S,x,n)is unsplit,non void,and strict and has arity held in gates and Boolean
denotation held in gates,
?There exist many sorted sets f,h indexed by N such that
(i)B=f(E),
(ii)f(0)=A,
(iii)h(0)=D,and
(iv)for every natural number n and for every non empty many sorted signature S
and for every set x such that S=f(n)and x=h(n)holds f(n+1)=F(S,x,n)and
h(n+1)=H(x,n),
?Let S be a non empty many sorted signature,A be a non-empty algebra over S,x be a set,and n be a natural number.Then G(S,A,x,n)is a non-empty algebra over
F(S,x,n),and
?Let S,S1be unsplit non void strict non empty many sorted signatures with arity held in gates and Boolean denotation held in gates,A be a Boolean strict circuit of
S with denotation held in gates,x be a set,and n be a natural number.Suppose
S1=F(S,x,n).Then G(S,A,x,n)is a Boolean strict circuit of S1with denotation
held in gates.
Let S be a non empty many sorted signature and let A be a set.Let us assume that A is a non-empty algebra over S.The functor MSAlg(A,S)yielding a non-empty algebra over S is de?ned as follows:
(Def.1)MSAlg(A,S)=A.
Now we present two schemes.The scheme CIRCCMB2’sch20deals with unsplit non void strict non empty many sorted signatures A,B with arity held in gates and Boolean denotation held in gates,a Boolean strict circuit C of A with denotation held in gates,a binary functor F yielding an unsplit non void non empty many sorted signature with arity held in gates and Boolean denotation held in gates,a binary functor G yielding a set,a set D,a binary functor H yielding a set,and a natural number E,and states that:
There exists a Boolean strict circuit A of B with denotation held in gates and there
exist many sorted sets f,g,h indexed by N such that
(i)B=f(E),
(ii)A=g(E),
(iii)f(0)=A,
(iv)g(0)=C,
(v)h(0)=D,and
(vi)for every natural number n and for every non empty many sorted signature S
and for every non-empty algebra A1over S and for every set x and for every non-
empty algebra A2over F(x,n)such that S=f(n)and A1=g(n)and x=h(n)and
A2=G(x,n)holds f(n+1)=S+·F(x,n)and g(n+1)=A1+·A2and h(n+1)=
H(x,n)
provided the parameters satisfy the following conditions:
?There exist many sorted sets f,h indexed by N such that
(i)B=f(E),
(ii)f(0)=A,
(iii)h(0)=D,and
(iv)for every natural number n and for every non empty many sorted signature S
and for every set x such that S=f(n)and x=h(n)holds f(n+1)=S+·F(x,n)and
h(n+1)=H(x,n),
and
?Let x be a set and n be a natural number.Then G(x,n)is a Boolean strict circuit of
F(x,n)with denotation held in gates.
The scheme CIRCCMB2’sch21deals with a non empty many sorted signature A,an unsplit non void strict non empty many sorted signature B with arity held in gates and Boolean denotation held in gates,a non-empty algebra C over A,a set D,a ternary functor F yielding a non empty many sorted signature,a4-ary functor G yielding a set,a binary functor H yielding a set,and a natural number E,and states that:
Let A1,A2be Boolean strict circuits of B with denotation held in gates.Suppose that
(i)there exist many sorted sets f,g,h indexed by N such that B=f(E)and
A1=g(E)and f(0)=A and g(0)=C and h(0)=D and for every natural number
n and for every non empty many sorted signature S and for every non-empty algebra
A over S and for every set x such that S=f(n)and A=g(n)and x=h(n)holds
f(n+1)=F(S,x,n)and g(n+1)=G(S,A,x,n)and h(n+1)=H(x,n),and
(ii)there exist many sorted sets f,g,h indexed by N such that B=f(E)and
A2=g(E)and f(0)=A and g(0)=C and h(0)=D and for every natural number
n and for every non empty many sorted signature S and for every non-empty algebra
A over S and for every set x such that S=f(n)and A=g(n)and x=h(n)holds
f(n+1)=F(S,x,n)and g(n+1)=G(S,A,x,n)and h(n+1)=H(x,n).
Then A1=A2
provided the following condition is met:
?Let S be a non empty many sorted signature,A be a non-empty algebra over S,x be a set,and n be a natural number.Then G(S,A,x,n)is a non-empty algebra over
F(S,x,n).
5.S TABILITY OF M ULTI C ELL C IRCUIT
We now state a number of propositions:
(10)Let S1,S2,S be non void circuit-like non empty many sorted signatures.Suppose
InnerVertices(S1)misses InputVertices(S2)and S=S1+·S2.Let C1be a non-empty circuit of S1,C2be a non-empty circuit of S2,and C be a non-empty circuit of S.Suppose C1≈C2 and C=C1+·C2.Let s2be a state of C2and s be a state of C.If s2=s the carrier of S2,then Following(s2)=Following(s) the carrier of S2.
(11)Let S1,S2,S be non void circuit-like non empty many sorted signatures.Suppose
InputVertices(S1)misses InnerVertices(S2)and S=S1+·S2.Let C1be a non-empty circuit of S1,C2be a non-empty circuit of S2,and C be a non-empty circuit of S.Suppose C1≈C2 and C=C1+·C2.Let s1be a state of C1and s be a state of C.If s1=s the carrier of S1,then Following(s1)=Following(s) the carrier of S1.
(12)Let S1,S2,S be non void circuit-like non empty many sorted signatures.Suppose S1≈
S2and InnerVertices(S1)misses InputVertices(S2)and S=S1+·S2.Let C1be a non-empty circuit of S1,C2be a non-empty circuit of S2,and C be a non-empty circuit of S.Suppose C1≈C2and C=C1+·C2.Let s1be a state of C1,s2be a state of C2,and s be a state of C.
Suppose s1=s the carrier of S1and s2=s the carrier of S2and s1is stable and s2is stable.
Then s is stable.
(13)Let S1,S2,S be non void circuit-like non empty many sorted signatures.Suppose S1≈
S2and InputVertices(S1)misses InnerVertices(S2)and S=S1+·S2.Let C1be a non-empty
circuit of S1,C2be a non-empty circuit of S2,and C be a non-empty circuit of S.Suppose C1≈C2and C=C1+·C2.Let s1be a state of C1,s2be a state of C2,and s be a state of C.
Suppose s1=s the carrier of S1and s2=s the carrier of S2and s1is stable and s2is stable.
Then s is stable.
(14)Let S1,S2,S be non void circuit-like non empty many sorted signatures.Suppose
InputVertices(S1)misses InnerVertices(S2)and S=S1+·S2.Let A1be a non-empty circuit of S1,A2be a non-empty circuit of S2,and A be a non-empty circuit of S.Suppose A1≈A2 and A=A1+·A2.Let s be a state of A and s1be a state of A1.Suppose s1=s the carrier of S1.Let n be a natural number.Then Following(s,n) the carrier of S1=Following(s1,n). (15)Let S1,S2,S be non void circuit-like non empty many sorted signatures.Suppose
InputVertices(S2)misses InnerVertices(S1)and S=S1+·S2.Let A1be a non-empty circuit of S1,A2be a non-empty circuit of S2,and A be a non-empty circuit of S.Suppose A1≈A2 and A=A1+·A2.Let s be a state of A and s2be a state of A2.Suppose s2=s the carrier of S2.Let n be a natural number.Then Following(s,n) the carrier of S2=Following(s2,n). (16)Let S1,S2,S be non void circuit-like non empty many sorted signatures.Suppose
InputVertices(S1)misses InnerVertices(S2)and S=S1+·S2.Let A1be a non-empty circuit of S1,A2be a non-empty circuit of S2,and A be a non-empty circuit of S.Suppose A1≈A2 and A=A1+·A2.Let s be a state of A and s1be a state of A1.Suppose s1=s the carrier of S1and s1is stable.Let s2be a state of A2.If s2=s the carrier of S2,then Following(s) the carrier of S2=Following(s2).
(17)Let S1,S2,S be non void circuit-like non empty many sorted signatures.Suppose S=
S1+·S2.Let A1be a non-empty circuit of S1,A2be a non-empty circuit of S2,and A be a non-empty circuit of S.Suppose A1≈A2and A=A1+·A2.Let s be a state of A and s1be
a state of A1.Suppose s1=s the carrier of S1and s1is stable.Let s2be a state of A2.If
s2=s the carrier of S2and s2is stable,then s is stable.
(18)Let S1,S2,S be non void circuit-like non empty many sorted signatures.Suppose S=
S1+·S2.Let A1be a non-empty circuit of S1,A2be a non-empty circuit of S2,and A be a non-empty circuit of S.Suppose A1≈A2and A=A1+·A2.Let s be a state of A.Suppose s is stable.Then
(i)for every state s1of A1such that s1=s the carrier of S1holds s1is stable,and
(ii)for every state s2of A2such that s2=s the carrier of S2holds s2is stable.
(19)Let S1,S2,S be non void circuit-like non empty many sorted signatures.Suppose
InputVertices(S1)misses InnerVertices(S2)and S=S1+·S2.Let A1be a non-empty circuit of S1,A2be a non-empty circuit of S2,and A be a non-empty circuit of S.Suppose A1≈A2 and A=A1+·A2.Let s1be a state of A1,s2be a state of A2,and s be a state of A.Suppose s1=s the carrier of S1and s2=s the carrier of S2and s1is stable.Let n be a natural number.
Then Following(s,n) the carrier of S2=Following(s2,n).
(20)Let S1,S2,S be non void circuit-like non empty many sorted signatures.Suppose
InputVertices(S1)misses InnerVertices(S2)and S=S1+·S2.Let A1be a non-empty cir-cuit of S1,A2be a non-empty circuit of S2,and A be a non-empty circuit of S.Suppose A1≈A2and A=A1+·A2.Let n1,n2be natural numbers,s be a state of A,s1be a state of A1,and s2be a state of A2.Suppose s1=s the carrier of S1and Following(s1,n1) is stable and s2=Following(s,n1) the carrier of S2and Following(s2,n2)is stable.Then Following(s,n1+n2)is stable.
(21)Let S1,S2,S be non void circuit-like non empty many sorted signatures.Suppose
InputVertices(S1)misses InnerVertices(S2)and S=S1+·S2.Let A1be a non-empty circuit of S1,A2be a non-empty circuit of S2,and A be a non-empty circuit of S.Suppose A1≈A2 and A=A1+·A2.Let n1,n2be natural numbers.Suppose for every state s of A1holds Following(s,n1)is stable and for every state s of A2holds Following(s,n2)is stable.Let s be a state of A.Then Following(s,n1+n2)is stable.
(22)Let S1,S2,S be non void circuit-like non empty many sorted signatures.Suppose
InputVertices(S1)misses InnerVertices(S2)and InputVertices(S2)misses InnerVertices(S1) and S=S1+·S2.Let A1be a non-empty circuit of S1,A2be a non-empty circuit of S2,and A be a non-empty circuit of S.Suppose A1≈A2and A=A1+·A2.Let s be a state of A and s1be a state of A1.Suppose s1=s the carrier of S1.Let s2be a state of A2.Suppose s2=s the carrier of S2.Let n be a natural number.Then Following(s,n)=Following(s1,n)+·Following(s2,n).
(23)Let S1,S2,S be non void circuit-like non empty many sorted signatures.Suppose
InputVertices(S1)misses InnerVertices(S2)and InputVertices(S2)misses InnerVertices(S1) and S=S1+·S2.Let A1be a non-empty circuit of S1,A2be a non-empty circuit of S2,and A be a non-empty circuit of S.Suppose A1≈A2and A=A1+·A2.Let n1,n2be natural numbers, s be a state of A,and s1be a state of A1.Suppose s1=s the carrier of S1.Let s2be a state of A2.Suppose s2=s the carrier of S2and Following(s1,n1)is stable and Following(s2,n2)is stable.Then Following(s,max(n1,n2))is stable.
(24)Let S1,S2,S be non void circuit-like non empty many sorted signatures.Suppose
InputVertices(S1)misses InnerVertices(S2)and InputVertices(S2)misses InnerVertices(S1) and S=S1+·S2.Let A1be a non-empty circuit of S1,A2be a non-empty circuit of S2,and A be a non-empty circuit of S.Suppose A1≈A2and A=A1+·A2.Let n be a natural number,s be a state of A,and s1be a state of A1.Suppose s1=s the carrier of S1.Let s2be a state of A2.Suppose s2=s the carrier of S2but Following(s1,n)is not stable or Following(s2,n)is not stable.Then Following(s,n)is not stable.
(25)Let S1,S2,S be non void circuit-like non empty many sorted signatures.Suppose
InputVertices(S1)misses InnerVertices(S2)and InputVertices(S2)misses InnerVertices(S1) and S=S1+·S2.Let A1be a non-empty circuit of S1,A2be a non-empty circuit of S2,and A be a non-empty circuit of S.Suppose A1≈A2and A=A1+·A2.Let n1,n2be natural num-bers.Suppose for every state s of A1holds Following(s,n1)is stable and for every state s of A2holds Following(s,n2)is stable.Let s be a state of A.Then Following(s,max(n1,n2))is stable.
The scheme CIRCCMB2’sch22deals with unsplit non void strict non empty many sorted sig-natures A,B with arity held in gates and Boolean denotation held in gates,a Boolean strict circuit C of A with denotation held in gates,a Boolean strict circuit D of B with denotation held in gates,
a binary functor F yielding an unsplit non void strict non empty many sorted signature with arity held in gates and Boolean denotation held in gates,a binary functor G yielding a set,a many sorted set E indexed by N,a set F,a binary functor H yielding a set,and a unary functor I yielding a natural number,and states that:
For every state s of D holds Following(s,I(0)+I(2)·I(1))is stable
provided the following requirements are met:
?Let x be a set and n be a natural number.Then G(x,n)is a Boolean strict circuit of
F(x,n)with denotation held in gates,
?For every state s of C holds Following(s,I(0))is stable,
?Let n be a natural number,x be a set,and A be a non-empty circuit of F(x,n).If x=E(n)and A=G(x,n),then for every state s of A holds Following(s,I(1))is
stable,
?There exist many sorted sets f,g indexed by N such that
(i)B=f(I(2)),
(ii)D=g(I(2)),
(iii)f(0)=A,
(iv)g(0)=C,
(v)E(0)=F,and
(vi)for every natural number n and for every non empty many sorted signature S
and for every non-empty algebra A1over S and for every set x and for every non-
empty algebra A2over F(x,n)such that S=f(n)and A1=g(n)and x=E(n)and
A2=G(x,n)holds f(n+1)=S+·F(x,n)and g(n+1)=A1+·A2and E(n+1)=
H(x,n),
?InnerVertices(A)is a binary relation and InputVertices(A)has no pairs,
?E(0)=F and F∈InnerVertices(A),
?For every natural number n and for every set x holds InnerVertices(F(x,n))is a binary relation,
?For every natural number n and for every set x such that x=E(n)holds InputVertices(F(x,n))\ {x}has no pairs,and
?For every natural number n and for every set x such that x=E(n)holds E(n+1)=
H(x,n)and x∈InputVertices(F(x,n))and H(x,n)∈InnerVertices(F(x,n)).
R EFERENCES
[1]Grzegorz Bancerek.The fundamental properties of natural numbers.Journal of Formalized Mathematics,1,1989.http://mizar.
org/JFM/Vol1/nat_1.html.
[2]Grzegorz Bancerek and Yatsuka Nakamura.Full adder circuit.Part I.Journal of Formalized Mathematics,7,1995.http://mizar.
org/JFM/Vol7/facirc_1.html.
[3]Czes?aw Byli′n ski.Functions and their basic properties.Journal of Formalized Mathematics,1,1989.https://www.wendangku.net/doc/e65866735.html,/JFM/Vol1/
funct_1.html.
[4]Czes?aw Byli′n ski.Functions from a set to a set.Journal of Formalized Mathematics,1,1989.https://www.wendangku.net/doc/e65866735.html,/JFM/Vol1/funct_
2.html.
[5]Czes?aw Byli′n ski.Partial functions.Journal of Formalized Mathematics,1,1989.https://www.wendangku.net/doc/e65866735.html,/JFM/Vol1/partfun1.html.
[6]Czes?aw Byli′n ski.Finite sequences and tuples of elements of a non-empty sets.Journal of Formalized Mathematics,2,1990.http:
//https://www.wendangku.net/doc/e65866735.html,/JFM/Vol2/finseq_2.html.
[7]Czes?aw Byli′n ski.The modi?cation of a function by a function and the iteration of the composition of a function.Journal of Formalized
Mathematics,2,1990.https://www.wendangku.net/doc/e65866735.html,/JFM/Vol2/funct_4.html.
[8]Agata Darmochwa?.Finite sets.Journal of Formalized Mathematics,1,1989.https://www.wendangku.net/doc/e65866735.html,/JFM/Vol1/finset_1.html.
[9]Jaros?aw Kotowicz.The limit of a real function at in?nity.Journal of Formalized Mathematics,2,1990.https://www.wendangku.net/doc/e65866735.html,/JFM/
Vol2/limfunc1.html.
[10]Yatsuka Nakamura and Grzegorz https://www.wendangku.net/doc/e65866735.html,bining of circuits.Journal of Formalized Mathematics,7,1995.https://www.wendangku.net/doc/e65866735.html,/
JFM/Vol7/circcomb.html.
[11]Yatsuka Nakamura,Piotr Rudnicki,Andrzej Trybulec,and Pauline N.Kawamoto.Introduction to circuits,I.Journal of Formalized
Mathematics,6,1994.https://www.wendangku.net/doc/e65866735.html,/JFM/Vol6/circuit1.html.
[12]Yatsuka Nakamura,Piotr Rudnicki,Andrzej Trybulec,and Pauline N.Kawamoto.Preliminaries to circuits,II.Journal of Formalized
Mathematics,6,1994.https://www.wendangku.net/doc/e65866735.html,/JFM/Vol6/msafree2.html.
[13]Yatsuka Nakamura,Piotr Rudnicki,Andrzej Trybulec,and Pauline N.Kawamoto.Introduction to circuits,II.Journal of Formalized
Mathematics,7,1995.https://www.wendangku.net/doc/e65866735.html,/JFM/Vol7/circuit2.html.
[14]Andrzej Trybulec.Tarski Grothendieck set theory.Journal of Formalized Mathematics,Axiomatics,1989.https://www.wendangku.net/doc/e65866735.html,/JFM/
Axiomatics/tarski.html.
[15]Andrzej Trybulec.Many-sorted sets.Journal of Formalized Mathematics,5,1993.https://www.wendangku.net/doc/e65866735.html,/JFM/Vol5/pboole.html.
[16]Andrzej Trybulec.Many sorted algebras.Journal of Formalized Mathematics,6,1994.https://www.wendangku.net/doc/e65866735.html,/JFM/Vol6/msualg_1.
html.
[17]Andrzej Trybulec.Subsets of real numbers.Journal of Formalized Mathematics,Addenda,2003.https://www.wendangku.net/doc/e65866735.html,/JFM/Addenda/
numbers.html.
[18]Edmund Woronowicz.Relations and their basic properties.Journal of Formalized Mathematics,1,1989.https://www.wendangku.net/doc/e65866735.html,/JFM/
Vol1/relat_1.html.
Received March22,2002
Published January2,2004