begin
theorem Th1:
:: deftheorem Def1 defines stabilizing CIRCCMB3:def 1 :
:: deftheorem Def2 defines stabilizing CIRCCMB3:def 2 :
:: deftheorem defines with_stabilization-limit CIRCCMB3:def 3 :
:: deftheorem Def4 defines Result CIRCCMB3:def 4 :
:: deftheorem Def5 defines stabilization-time CIRCCMB3:def 5 :
theorem Th2:
theorem
theorem Th4:
theorem Th5:
theorem
theorem
canceled;
theorem Th8:
theorem
theorem Th10:
theorem Th11:
theorem
begin
theorem Th13:
theorem Th14:
for
x1,
x2,
x3,
x4 being
set holds
rng <*x1,x2,x3,x4*> = {x1,x2,x3,x4}
theorem Th15:
for
x1,
x2,
x3,
x4,
x5 being
set holds
rng <*x1,x2,x3,x4,x5*> = {x1,x2,x3,x4,x5}
:: deftheorem Def6 defines one-gate CIRCCMB3:def 6 :
:: deftheorem Def7 defines one-gate CIRCCMB3:def 7 :
:: deftheorem defines Output CIRCCMB3:def 8 :
theorem Th16:
theorem Th17:
theorem
theorem
theorem Th20:
theorem Th21:
theorem Th22:
scheme
OneGate5Ex{
F1()
-> set ,
F2()
-> set ,
F3()
-> set ,
F4()
-> set ,
F5()
-> set ,
F6()
-> non
empty finite set ,
F7(
set ,
set ,
set ,
set ,
set )
-> Element of
F6() } :
begin
theorem
canceled;
theorem Th24:
theorem
theorem
:: deftheorem Def9 defines Signature CIRCCMB3:def 9 :
theorem Th27:
:: deftheorem Def10 defines Circuit CIRCCMB3:def 10 :
theorem Th28:
theorem
canceled;
theorem Th30:
theorem Th31:
theorem Th32:
theorem Th33:
theorem Th34:
theorem Th35:
scheme
2AryDef{
F1()
-> non
empty set ,
F2(
set ,
set )
-> Element of
F1() } :
( ex
f being
Function of 2
-tuples_on F1(),
F1() st
for
x,
y being
Element of
F1() holds
f . <*x,y*> = F2(
x,
y) & ( for
f1,
f2 being
Function of 2
-tuples_on F1(),
F1() st ( for
x,
y being
Element of
F1() holds
f1 . <*x,y*> = F2(
x,
y) ) & ( for
x,
y being
Element of
F1() holds
f2 . <*x,y*> = F2(
x,
y) ) holds
f1 = f2 ) )
scheme
3AryDef{
F1()
-> non
empty set ,
F2(
set ,
set ,
set )
-> Element of
F1() } :
( ex
f being
Function of 3
-tuples_on F1(),
F1() st
for
x,
y,
z being
Element of
F1() holds
f . <*x,y,z*> = F2(
x,
y,
z) & ( for
f1,
f2 being
Function of 3
-tuples_on F1(),
F1() st ( for
x,
y,
z being
Element of
F1() holds
f1 . <*x,y,z*> = F2(
x,
y,
z) ) & ( for
x,
y,
z being
Element of
F1() holds
f2 . <*x,y,z*> = F2(
x,
y,
z) ) holds
f1 = f2 ) )
theorem Th36:
theorem Th37:
theorem Th38:
for
f being
Function for
x1,
x2,
x3,
x4,
x5 being
set st
x1 in dom f &
x2 in dom f &
x3 in dom f &
x4 in dom f &
x5 in dom f holds
f * <*x1,x2,x3,x4,x5*> = <*(f . x1),(f . x2),(f . x3),(f . x4),(f . x5)*>
scheme
OneGate4Result{
F1()
-> set ,
F2()
-> set ,
F3()
-> set ,
F4()
-> set ,
F5()
-> non
empty finite set ,
F6(
set ,
set ,
set ,
set )
-> Element of
F5(),
F7()
-> Function of 4
-tuples_on F5(),
F5() } :
for
s being
State of
for
a1,
a2,
a3,
a4 being
Element of
F5() st
a1 = s . F1() &
a2 = s . F2() &
a3 = s . F3() &
a4 = s . F4() holds
(Result s) . (Output (1GateCircStr <*F1(),F2(),F3(),F4()*>,F7())) = F6(
a1,
a2,
a3,
a4)
provided
A1:
for
g being
Function of 4
-tuples_on F5(),
F5() holds
(
g = F7() iff for
a1,
a2,
a3,
a4 being
Element of
F5() holds
g . <*a1,a2,a3,a4*> = F6(
a1,
a2,
a3,
a4) )
scheme
OneGate5Result{
F1()
-> set ,
F2()
-> set ,
F3()
-> set ,
F4()
-> set ,
F5()
-> set ,
F6()
-> non
empty finite set ,
F7(
set ,
set ,
set ,
set ,
set )
-> Element of
F6(),
F8()
-> Function of 5
-tuples_on F6(),
F6() } :
for
s being
State of
for
a1,
a2,
a3,
a4,
a5 being
Element of
F6() st
a1 = s . F1() &
a2 = s . F2() &
a3 = s . F3() &
a4 = s . F4() &
a5 = s . F5() holds
(Result s) . (Output (1GateCircStr <*F1(),F2(),F3(),F4(),F5()*>,F8())) = F7(
a1,
a2,
a3,
a4,
a5)
provided
A1:
for
g being
Function of 5
-tuples_on F6(),
F6() holds
(
g = F8() iff for
a1,
a2,
a3,
a4,
a5 being
Element of
F6() holds
g . <*a1,a2,a3,a4,a5*> = F7(
a1,
a2,
a3,
a4,
a5) )
begin
theorem Th39:
theorem Th40:
theorem Th41:
theorem Th42:
theorem Th43:
theorem Th44:
theorem Th45:
for
x1,
x2,
x3 being
set for
X being non
empty finite set for
f being
Function of 3
-tuples_on X,
X for
S being
Signature of
X st
x1 in the
carrier of
S & not
x2 in InnerVertices S & not
x3 in InnerVertices S & not
Output (1GateCircStr <*x1,x2,x3*>,f) in InputVertices S holds
InputVertices (S +* (1GateCircStr <*x1,x2,x3*>,f)) = (InputVertices S) \/ {x2,x3}
theorem Th46:
for
x1,
x2,
x3 being
set for
X being non
empty finite set for
f being
Function of 3
-tuples_on X,
X for
S being
Signature of
X st
x2 in the
carrier of
S & not
x1 in InnerVertices S & not
x3 in InnerVertices S & not
Output (1GateCircStr <*x1,x2,x3*>,f) in InputVertices S holds
InputVertices (S +* (1GateCircStr <*x1,x2,x3*>,f)) = (InputVertices S) \/ {x1,x3}
theorem Th47:
for
x1,
x2,
x3 being
set for
X being non
empty finite set for
f being
Function of 3
-tuples_on X,
X for
S being
Signature of
X st
x3 in the
carrier of
S & not
x1 in InnerVertices S & not
x2 in InnerVertices S & not
Output (1GateCircStr <*x1,x2,x3*>,f) in InputVertices S holds
InputVertices (S +* (1GateCircStr <*x1,x2,x3*>,f)) = (InputVertices S) \/ {x1,x2}
theorem Th48:
theorem Th49:
theorem Th50:
theorem Th51:
begin
theorem Th52:
scheme
Comb3CircResult{
F1()
-> set ,
F2()
-> set ,
F3()
-> set ,
F4()
-> non
empty finite set ,
F5(
set ,
set ,
set )
-> Element of
F4(),
F6()
-> finite Signature of
F4(),
F7()
-> Circuit of
F4(),
F6(),
F8()
-> Function of 3
-tuples_on F4(),
F4() } :
provided
A1:
for
g being
Function of 3
-tuples_on F4(),
F4() holds
(
g = F8() iff for
a1,
a2,
a3 being
Element of
F4() holds
g . <*a1,a2,a3*> = F5(
a1,
a2,
a3) )
and A2:
not
Output (1GateCircStr <*F1(),F2(),F3()*>,F8()) in InputVertices F6()
scheme
Comb4CircResult{
F1()
-> set ,
F2()
-> set ,
F3()
-> set ,
F4()
-> set ,
F5()
-> non
empty finite set ,
F6(
set ,
set ,
set ,
set )
-> Element of
F5(),
F7()
-> finite Signature of
F5(),
F8()
-> Circuit of
F5(),
F7(),
F9()
-> Function of 4
-tuples_on F5(),
F5() } :
for
s being
State of
for
s' being
State of st
s' = s | the
carrier of
F7() holds
for
a1,
a2,
a3,
a4 being
Element of
F5() st (
F1()
in InnerVertices F7() implies
a1 = (Result s') . F1() ) & ( not
F1()
in InnerVertices F7() implies
a1 = s . F1() ) & (
F2()
in InnerVertices F7() implies
a2 = (Result s') . F2() ) & ( not
F2()
in InnerVertices F7() implies
a2 = s . F2() ) & (
F3()
in InnerVertices F7() implies
a3 = (Result s') . F3() ) & ( not
F3()
in InnerVertices F7() implies
a3 = s . F3() ) & (
F4()
in InnerVertices F7() implies
a4 = (Result s') . F4() ) & ( not
F4()
in InnerVertices F7() implies
a4 = s . F4() ) holds
(Result s) . (Output (1GateCircStr <*F1(),F2(),F3(),F4()*>,F9())) = F6(
a1,
a2,
a3,
a4)
provided
A1:
for
g being
Function of 4
-tuples_on F5(),
F5() holds
(
g = F9() iff for
a1,
a2,
a3,
a4 being
Element of
F5() holds
g . <*a1,a2,a3,a4*> = F6(
a1,
a2,
a3,
a4) )
and A2:
not
Output (1GateCircStr <*F1(),F2(),F3(),F4()*>,F9()) in InputVertices F7()
scheme
Comb5CircResult{
F1()
-> set ,
F2()
-> set ,
F3()
-> set ,
F4()
-> set ,
F5()
-> set ,
F6()
-> non
empty finite set ,
F7(
set ,
set ,
set ,
set ,
set )
-> Element of
F6(),
F8()
-> finite Signature of
F6(),
F9()
-> Circuit of
F6(),
F8(),
F10()
-> Function of 5
-tuples_on F6(),
F6() } :
for
s being
State of
for
s' being
State of st
s' = s | the
carrier of
F8() holds
for
a1,
a2,
a3,
a4,
a5 being
Element of
F6() st (
F1()
in InnerVertices F8() implies
a1 = (Result s') . F1() ) & ( not
F1()
in InnerVertices F8() implies
a1 = s . F1() ) & (
F2()
in InnerVertices F8() implies
a2 = (Result s') . F2() ) & ( not
F2()
in InnerVertices F8() implies
a2 = s . F2() ) & (
F3()
in InnerVertices F8() implies
a3 = (Result s') . F3() ) & ( not
F3()
in InnerVertices F8() implies
a3 = s . F3() ) & (
F4()
in InnerVertices F8() implies
a4 = (Result s') . F4() ) & ( not
F4()
in InnerVertices F8() implies
a4 = s . F4() ) & (
F5()
in InnerVertices F8() implies
a5 = (Result s') . F5() ) & ( not
F5()
in InnerVertices F8() implies
a5 = s . F5() ) holds
(Result s) . (Output (1GateCircStr <*F1(),F2(),F3(),F4(),F5()*>,F10())) = F7(
a1,
a2,
a3,
a4,
a5)
provided
A1:
for
g being
Function of 5
-tuples_on F6(),
F6() holds
(
g = F10() iff for
a1,
a2,
a3,
a4,
a5 being
Element of
F6() holds
g . <*a1,a2,a3,a4,a5*> = F7(
a1,
a2,
a3,
a4,
a5) )
and A2:
not
Output (1GateCircStr <*F1(),F2(),F3(),F4(),F5()*>,F10()) in InputVertices F8()
begin
:: deftheorem Def11 defines with_nonpair_inputs CIRCCMB3:def 11 :
theorem
theorem
theorem Th55:
theorem Th56:
theorem Th57:
registration
let X be non
empty finite set ;
let S be
with_nonpair_inputs Signature of
X;
let x1,
x2 be
Vertex of ;
let n be non
pair set ;
let f be
Function of 3
-tuples_on X,
X;
cluster S +* (1GateCircStr <*x1,x2,n*>,f) -> with_nonpair_inputs ;
coherence
S +* (1GateCircStr <*x1,x2,n*>,f) is with_nonpair_inputs
by Th57;
cluster S +* (1GateCircStr <*x1,n,x2*>,f) -> with_nonpair_inputs ;
coherence
S +* (1GateCircStr <*x1,n,x2*>,f) is with_nonpair_inputs
by Th57;
cluster S +* (1GateCircStr <*n,x1,x2*>,f) -> with_nonpair_inputs ;
coherence
S +* (1GateCircStr <*n,x1,x2*>,f) is with_nonpair_inputs
by Th57;
end;
registration
let X be non
empty finite set ;
let S be
with_nonpair_inputs Signature of
X;
let x be
Vertex of ;
let n1,
n2 be non
pair set ;
let f be
Function of 3
-tuples_on X,
X;
cluster S +* (1GateCircStr <*x,n1,n2*>,f) -> with_nonpair_inputs ;
coherence
S +* (1GateCircStr <*x,n1,n2*>,f) is with_nonpair_inputs
by Th57;
cluster S +* (1GateCircStr <*n1,x,n2*>,f) -> with_nonpair_inputs ;
coherence
S +* (1GateCircStr <*n1,x,n2*>,f) is with_nonpair_inputs
by Th57;
cluster S +* (1GateCircStr <*n1,n2,x*>,f) -> with_nonpair_inputs ;
coherence
S +* (1GateCircStr <*n1,n2,x*>,f) is with_nonpair_inputs
by Th57;
end;