:: CIRCCMB3 semantic presentation

theorem Th1: :: CIRCCMB3:1

for b₁ being non empty non void Circuit-like ManySortedSign
for b₂ being non-empty Circuit of b₁
for b₃ being State of b₂
for b₄ being set st b₄ in InputVertices b₁ holds
for b₅ being Nat holds (Following b₃,b₅) . b₄ = b₃ . b₄

proof end;

definition

let c₁ be non empty non void Circuit-like ManySortedSign ;
let c₂ be non-empty Circuit of c₁;
let c₃ be State of c₂;
attr a₃ is stabilizing means :Def1: :: CIRCCMB3:def 1
ex b₁ being Nat st Following a₃,b₁ is stable;

end;

:: deftheorem Def1 defines stabilizing CIRCCMB3:def 1 :

definition

let c₁ be non empty non void Circuit-like ManySortedSign ;
let c₂ be non-empty Circuit of c₁;
attr a₂ is stabilizing means :Def2: :: CIRCCMB3:def 2
for b₁ being State of a₂ holds b₁ is stabilizing;
attr a₂ is with_stabilization-limit means :: CIRCCMB3:def 3
ex b₁ being Nat st
for b₂ being State of a₂ holds Following b₂,b₁ is stable;

end;

:: deftheorem Def2 defines stabilizing CIRCCMB3:def 2 :

:: deftheorem Def3 defines with_stabilization-limit CIRCCMB3:def 3 :

registration

let c₁ be non empty non void Circuit-like ManySortedSign ;
cluster non-empty with_stabilization-limit -> non-empty stabilizing MSAlgebra of a₁;
coherence

proof end;

end;

definition

let c₁ be non empty non void Circuit-like ManySortedSign ;
let c₂ be non-empty Circuit of c₁;
let c₃ be State of c₂;
assume E4: c₃ is stabilizing ;
func Result c₃ -> State of a₂ means :Def4: :: CIRCCMB3:def 4
( a₄ is stable & ex b₁ being Nat st a₄ = Following a₃,b₁ );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def4 defines Result CIRCCMB3:def 4 :

definition

let c₁ be non empty non void Circuit-like ManySortedSign ;
let c₂ be non-empty Circuit of c₁;
let c₃ be State of c₂;
assume E5: c₃ is stabilizing ;
func stabilization-time c₃ -> Nat means :Def5: :: CIRCCMB3:def 5
( Following a₃,a₄ is stable & ( for b₁ being Nat st b₁ < a₄ holds
not Following a₃,b₁ is stable ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def5 defines stabilization-time CIRCCMB3:def 5 :

theorem Th2: :: CIRCCMB3:2

for b₁ being non empty non void Circuit-like ManySortedSign
for b₂ being non-empty Circuit of b₁
for b₃ being State of b₂ st b₃ is stabilizing holds
Result b₃ = Following b₃,(stabilization-time b₃)

proof end;

theorem Th3: :: CIRCCMB3:3

for b₁ being non empty non void Circuit-like ManySortedSign
for b₂ being non-empty Circuit of b₁
for b₃ being State of b₂
for b₄ being Nat st Following b₃,b₄ is stable holds
stabilization-time b₃ <= b₄

proof end;

theorem Th4: :: CIRCCMB3:4

for b₁ being non empty non void Circuit-like ManySortedSign
for b₂ being non-empty Circuit of b₁
for b₃ being State of b₂
for b₄ being Nat st Following b₃,b₄ is stable holds
Result b₃ = Following b₃,b₄

proof end;

theorem Th5: :: CIRCCMB3:5

for b₁ being non empty non void Circuit-like ManySortedSign
for b₂ being non-empty Circuit of b₁
for b₃ being State of b₂
for b₄ being Nat st b₃ is stabilizing & b₄ >= stabilization-time b₃ holds
Result b₃ = Following b₃,b₄

proof end;

theorem Th6: :: CIRCCMB3:6

for b₁ being non empty non void Circuit-like ManySortedSign
for b₂ being non-empty Circuit of b₁
for b₃ being State of b₂ st b₃ is stabilizing holds
for b₄ being set st b₄ in InputVertices b₁ holds
(Result b₃) . b₄ = b₃ . b₄

proof end;

theorem Th7: :: CIRCCMB3:7

canceled;

theorem Th8: :: CIRCCMB3:8

for b₁, b₂ being non empty non void Circuit-like ManySortedSign st InputVertices b₁ misses InnerVertices b₂ & InputVertices b₂ misses InnerVertices b₁ holds
for b₃ being non empty non void Circuit-like ManySortedSign st b₃ = b₁ +* b₂ holds
for b₄ being non-empty Circuit of b₁
for b₅ being non-empty Circuit of b₂ st b₄ tolerates b₅ holds
for b₆ being non-empty Circuit of b₃ st b₆ = b₄ +* b₅ holds
for b₇ being State of b₆
for b₈ being State of b₄
for b₉ being State of b₅ st b₈ = b₇ | the carrier of b₁ & b₉ = b₇ | the carrier of b₂ & b₈ is stabilizing & b₉ is stabilizing holds
b₇ is stabilizing

proof end;

theorem Th9: :: CIRCCMB3:9

for b₁, b₂ being non empty non void Circuit-like ManySortedSign st InputVertices b₁ misses InnerVertices b₂ & InputVertices b₂ misses InnerVertices b₁ holds
for b₃ being non empty non void Circuit-like ManySortedSign st b₃ = b₁ +* b₂ holds
for b₄ being non-empty Circuit of b₁
for b₅ being non-empty Circuit of b₂ st b₄ tolerates b₅ holds
for b₆ being non-empty Circuit of b₃ st b₆ = b₄ +* b₅ holds
for b₇ being State of b₆
for b₈ being State of b₄ st b₈ = b₇ | the carrier of b₁ & b₈ is stabilizing holds
for b₉ being State of b₅ st b₉ = b₇ | the carrier of b₂ & b₉ is stabilizing holds
stabilization-time b₇ = max (stabilization-time b₈),(stabilization-time b₉)

proof end;

theorem Th10: :: CIRCCMB3:10

for b₁, b₂ being non empty non void Circuit-like ManySortedSign st InputVertices b₁ misses InnerVertices b₂ holds
for b₃ being non empty non void Circuit-like ManySortedSign st b₃ = b₁ +* b₂ holds
for b₄ being non-empty Circuit of b₁
for b₅ being non-empty Circuit of b₂ st b₄ tolerates b₅ holds
for b₆ being non-empty Circuit of b₃ st b₆ = b₄ +* b₅ holds
for b₇ being State of b₆
for b₈ being State of b₄ st b₈ = b₇ | the carrier of b₁ & b₈ is stabilizing holds
for b₉ being State of b₅ st b₉ = (Following b₇,(stabilization-time b₈)) | the carrier of b₂ & b₉ is stabilizing holds
b₇ is stabilizing

proof end;

theorem Th11: :: CIRCCMB3:11

proof end;

theorem Th12: :: CIRCCMB3:12

for b₁, b₂, b₃ being non empty non void Circuit-like ManySortedSign st InputVertices b₁ misses InnerVertices b₂ & b₃ = b₁ +* b₂ holds
for b₄ being non-empty Circuit of b₁
for b₅ being non-empty Circuit of b₂
for b₆ being non-empty Circuit of b₃ st b₄ tolerates b₅ & b₆ = b₄ +* b₅ holds
for b₇ being State of b₆
for b₈ being State of b₄ st b₈ = b₇ | the carrier of b₁ & b₈ is stabilizing holds
for b₉ being State of b₅ st b₉ = (Following b₇,(stabilization-time b₈)) | the carrier of b₂ & b₉ is stabilizing holds
(Result b₇) | the carrier of b₁ = Result b₈

proof end;

theorem Th13: :: CIRCCMB3:13

for b₁ being set
for b₂ being non empty finite set
for b₃ being Nat
for b₄ being FinSeqLen of b₃
for b₅ being Function of b₃ -tuples_on b₂,b₂
for b₆ being State of (1GateCircuit b₄,b₅) holds b₆ * b₄ is Element of b₃ -tuples_on b₂

proof end;

theorem Th14: :: CIRCCMB3:14

for b₁, b₂, b₃, b₄ being set holds rng <*b₁,b₂,b₃,b₄*> = {b₁,b₂,b₃,b₄}

proof end;

theorem Th15: :: CIRCCMB3:15

for b₁, b₂, b₃, b₄, b₅ being set holds rng <*b₁,b₂,b₃,b₄,b₅*> = {b₁,b₂,b₃,b₄,b₅}

proof end;

definition

let c₁, c₂, c₃, c₄ be set ;
redefine func <* as <*c₁,c₂,c₃,c₄*> -> FinSeqLen of 4;
coherence

proof end;

let c₅ be set ;
redefine func <* as <*c₁,c₂,c₃,c₄,c₅*> -> FinSeqLen of 5;
coherence

proof end;

end;

definition

let c₁ be ManySortedSign ;
attr a₁ is one-gate means :Def6: :: CIRCCMB3:def 6
ex b₁ being non empty finite set ex b₂ being Natex b₃ being FinSeqLen of b₂ex b₄ being Function of b₂ -tuples_on b₁,b₁ st a₁ = 1GateCircStr b₃,b₄;

end;

:: deftheorem Def6 defines one-gate CIRCCMB3:def 6 :

definition

let c₁ be non empty ManySortedSign ;
let c₂ be MSAlgebra of c₁;
attr a₂ is one-gate means :Def7: :: CIRCCMB3:def 7
ex b₁ being non empty finite set ex b₂ being Natex b₃ being FinSeqLen of b₂ex b₄ being Function of b₂ -tuples_on b₁,b₁ st
( a₁ = 1GateCircStr b₃,b₄ & a₂ = 1GateCircuit b₃,b₄ );

end;

:: deftheorem Def7 defines one-gate CIRCCMB3:def 7 :

registration

let c₁ be FinSequence;
let c₂ be set ;
cluster 1GateCircStr a₁,a₂ -> finite ;
coherence

proof end;

end;

registration

cluster one-gate -> non empty finite strict non void unsplit gate`1=arity ManySortedSign ;
coherence

proof end;

end;

registration

cluster non empty one-gate -> non empty gate`2=den ManySortedSign ;
coherence

proof end;

end;

registration

let c₁ be non empty finite set ;
let c₂ be Nat;
let c₃ be FinSeqLen of c₂;
let c₄ be Function of c₂ -tuples_on c₁,c₁;
cluster 1GateCircStr a₃,a₄ -> finite one-gate ;
coherence by Def6;

end;

registration

cluster non empty finite strict non void unsplit gate`1=arity gate`2=den one-gate ManySortedSign ;
existence

proof end;

end;

registration

let c₁ be one-gate ManySortedSign ;
cluster one-gate -> strict non-empty MSAlgebra of a₁;
coherence

proof end;

end;

registration

let c₁ be non empty finite set ;
let c₂ be Nat;
let c₃ be FinSeqLen of c₂;
let c₄ be Function of c₂ -tuples_on c₁,c₁;
cluster 1GateCircuit a₃,a₄ -> one-gate ;
coherence by Def7;

end;

registration

let c₁ be one-gate ManySortedSign ;
cluster strict non-empty one-gate MSAlgebra of a₁;
existence

proof end;

end;

definition

let c₁ be one-gate ManySortedSign ;
func Output c₁ -> Vertex of a₁ equals :: CIRCCMB3:def 8
union the OperSymbols of a₁;
coherence

proof end;

end;

:: deftheorem Def8 defines Output CIRCCMB3:def 8 :

registration

let c₁ be one-gate ManySortedSign ;
cluster Output a₁ -> pair ;
coherence

proof end;

end;

theorem Th16: :: CIRCCMB3:16

for b₁ being one-gate ManySortedSign
for b₂ being FinSequence
for b₃ being set st b₁ = 1GateCircStr b₂,b₃ holds
Output b₁ = [b₂,b₃]

proof end;

theorem Th17: :: CIRCCMB3:17

for b₁ being one-gate ManySortedSign holds InnerVertices b₁ = {(Output b₁)}

proof end;

theorem Th18: :: CIRCCMB3:18

for b₁ being one-gate ManySortedSign
for b₂ being one-gate Circuit of b₁
for b₃ being Nat
for b₄ being non empty finite set
for b₅ being Function of b₃ -tuples_on b₄,b₄
for b₆ being FinSeqLen of b₃ st b₂ = 1GateCircuit b₆,b₅ holds
b₁ = 1GateCircStr b₆,b₅

proof end;

theorem Th19: :: CIRCCMB3:19

for b₁ being Nat
for b₂ being non empty finite set
for b₃ being Function of b₁ -tuples_on b₂,b₂
for b₄ being FinSeqLen of b₁
for b₅ being State of (1GateCircuit b₄,b₃) holds (Following b₅) . (Output (1GateCircStr b₄,b₃)) = b₃ . (b₅ * b₄)

proof end;

theorem Th20: :: CIRCCMB3:20

for b₁ being one-gate ManySortedSign
for b₂ being one-gate Circuit of b₁
for b₃ being State of b₂ holds Following b₃ is stable

proof end;

registration

let c₁ be non empty non void Circuit-like ManySortedSign ;
cluster non-empty one-gate -> non-empty stabilizing with_stabilization-limit MSAlgebra of a₁;
coherence

proof end;

end;

theorem Th21: :: CIRCCMB3:21

for b₁ being one-gate ManySortedSign
for b₂ being one-gate Circuit of b₁
for b₃ being State of b₂ holds Result b₃ = Following b₃

proof end;

theorem Th22: :: CIRCCMB3:22

for b₁ being one-gate ManySortedSign
for b₂ being one-gate Circuit of b₁
for b₃ being State of b₂ holds stabilization-time b₃ <= 1

proof end;

scheme :: CIRCCMB3:sch 1
s1{ F₁() -> set , F₂() -> non empty finite set , F₃( set ) -> Element of F₂() } :

ex b₁ being one-gate ManySortedSign ex b₂ being one-gate Circuit of b₁ st
( InputVertices b₁ = {F₁()} & ( for b₃ being State of b₂ holds (Result b₃) . (Output b₁) = F₃((b₃ . F₁())) ) )

proof end;

scheme :: CIRCCMB3:sch 2
s2{ F₁() -> set , F₂() -> set , F₃() -> non empty finite set , F₄( set , set ) -> Element of F₃() } :

ex b₁ being one-gate ManySortedSign ex b₂ being one-gate Circuit of b₁ st
( InputVertices b₁ = {F₁(),F₂()} & ( for b₃ being State of b₂ holds (Result b₃) . (Output b₁) = F₄((b₃ . F₁()),(b₃ . F₂())) ) )

proof end;

scheme :: CIRCCMB3:sch 3
s3{ F₁() -> set , F₂() -> set , F₃() -> set , F₄() -> non empty finite set , F₅( set , set , set ) -> Element of F₄() } :

ex b₁ being one-gate ManySortedSign ex b₂ being one-gate Circuit of b₁ st
( InputVertices b₁ = {F₁(),F₂(),F₃()} & ( for b₃ being State of b₂ holds (Result b₃) . (Output b₁) = F₅((b₃ . F₁()),(b₃ . F₂()),(b₃ . F₃())) ) )

proof end;

scheme :: CIRCCMB3:sch 4
s4{ F₁() -> set , F₂() -> set , F₃() -> set , F₄() -> set , F₅() -> non empty finite set , F₆( set , set , set , set ) -> Element of F₅() } :

ex b₁ being one-gate ManySortedSign ex b₂ being one-gate Circuit of b₁ st
( InputVertices b₁ = {F₁(),F₂(),F₃(),F₄()} & ( for b₃ being State of b₂ holds (Result b₃) . (Output b₁) = F₆((b₃ . F₁()),(b₃ . F₂()),(b₃ . F₃()),(b₃ . F₄())) ) )

proof end;

scheme :: CIRCCMB3:sch 5
s5{ F₁() -> set , F₂() -> set , F₃() -> set , F₄() -> set , F₅() -> set , F₆() -> non empty finite set , F₇( set , set , set , set , set ) -> Element of F₆() } :

ex b₁ being one-gate ManySortedSign ex b₂ being one-gate Circuit of b₁ st
( InputVertices b₁ = {F₁(),F₂(),F₃(),F₄(),F₅()} & ( for b₃ being State of b₂ holds (Result b₃) . (Output b₁) = F₇((b₃ . F₁()),(b₃ . F₂()),(b₃ . F₃()),(b₃ . F₄()),(b₃ . F₅())) ) )

proof end;

theorem Th23: :: CIRCCMB3:23

for b₁ being constant Function holds b₁ = (dom b₁) --> (the_value_of b₁)

proof end;

theorem Th24: :: CIRCCMB3:24

for b₁, b₂ being non empty set
for b₃, b₄ being Nat st b₃ <> 0 & b₃ -tuples_on b₁ = b₄ -tuples_on b₂ holds
( b₁ = b₂ & b₃ = b₄ )

proof end;

theorem Th25: :: CIRCCMB3:25

for b₁, b₂ being non empty ManySortedSign
for b₃ being Vertex of b₁ holds b₃ is Vertex of (b₁ +* b₂)

proof end;

theorem Th26: :: CIRCCMB3:26

for b₁, b₂ being non empty ManySortedSign
for b₃ being Vertex of b₂ holds b₃ is Vertex of (b₁ +* b₂)

proof end;

definition

let c₁ be non empty finite set ;
mode Signature of c₁ -> non empty non void unsplit gate`1=arity gate`2=den ManySortedSign means :Def9: :: CIRCCMB3:def 9
ex b₁ being Circuit of a₂ st
( the Sorts of b₁ is constant & the_value_of the Sorts of b₁ = a₁ & b₁ is gate`2=den );
existence

proof end;

end;

:: deftheorem Def9 defines Signature CIRCCMB3:def 9 :

theorem Th27: :: CIRCCMB3:27

for b₁ being Nat
for b₂ being non empty finite set
for b₃ being Function of b₁ -tuples_on b₂,b₂
for b₄ being FinSeqLen of b₁ holds 1GateCircStr b₄,b₃ is Signature of b₂

proof end;

registration

let c₁ be non empty finite set ;
cluster non empty finite strict non void unsplit gate`1=arity gate`2=den one-gate Signature of a₁;
existence

proof end;

end;

definition

let c₁ be Nat;
let c₂ be non empty finite set ;
let c₃ be Function of c₁ -tuples_on c₂,c₂;
let c₄ be FinSeqLen of c₁;
redefine func 1GateCircStr as 1GateCircStr c₄,c₃ -> strict Signature of a₂;
coherence by Th27;

end;

definition

let c₁ be non empty finite set ;
let c₂ be Signature of c₁;
mode Circuit of c₁,c₂ -> Circuit of a₂ means :Def10: :: CIRCCMB3:def 10
( a₃ is gate`2=den & the Sorts of a₃ is constant & the_value_of the Sorts of a₃ = a₁ );
existence

proof end;

end;

:: deftheorem Def10 defines Circuit CIRCCMB3:def 10 :

registration

let c₁ be non empty finite set ;
let c₂ be Signature of c₁;
cluster -> non-empty gate`2=den Circuit of a₁,a₂;
coherence

proof end;

end;

theorem Th28: :: CIRCCMB3:28

for b₁ being Nat
for b₂ being non empty finite set
for b₃ being Function of b₁ -tuples_on b₂,b₂
for b₄ being FinSeqLen of b₁ holds 1GateCircuit b₄,b₃ is Circuit of b₂, 1GateCircStr b₄,b₃

proof end;

registration

let c₁ be non empty finite set ;
let c₂ be one-gate Signature of c₁;
cluster strict non-empty gate`2=den stabilizing with_stabilization-limit one-gate Circuit of a₁,a₂;
existence

proof end;

end;

registration

let c₁ be non empty finite set ;
let c₂ be Signature of c₁;
cluster strict non-empty gate`2=den Circuit of a₁,a₂;
existence

proof end;

end;

definition

let c₁ be Nat;
let c₂ be non empty finite set ;
let c₃ be Function of c₁ -tuples_on c₂,c₂;
let c₄ be FinSeqLen of c₁;
redefine func 1GateCircuit as 1GateCircuit c₄,c₃ -> strict Circuit of a₂, 1GateCircStr a₄,a₃;
coherence by Th28;

end;

theorem Th29: :: CIRCCMB3:29

canceled;

theorem Th30: :: CIRCCMB3:30

for b₁ being non empty finite set
for b₂, b₃ being Signature of b₁
for b₄ being Circuit of b₁,b₂
for b₅ being Circuit of b₁,b₃ holds b₄ tolerates b₅

proof end;

theorem Th31: :: CIRCCMB3:31

for b₁ being non empty finite set
for b₂, b₃ being Signature of b₁
for b₄ being Circuit of b₁,b₂
for b₅ being Circuit of b₁,b₃ holds b₄ +* b₅ is Circuit of b₂ +* b₃

proof end;

theorem Th32: :: CIRCCMB3:32

for b₁ being non empty finite set
for b₂, b₃ being Signature of b₁
for b₄ being Circuit of b₁,b₂
for b₅ being Circuit of b₁,b₃ holds b₄ +* b₅ is gate`2=den

proof end;

theorem Th33: :: CIRCCMB3:33

for b₁ being non empty finite set
for b₂, b₃ being Signature of b₁
for b₄ being Circuit of b₁,b₂
for b₅ being Circuit of b₁,b₃ holds
( the Sorts of (b₄ +* b₅) is constant & the_value_of the Sorts of (b₄ +* b₅) = b₁ )

proof end;

registration

let c₁, c₂ be non empty finite ManySortedSign ;
cluster a₁ +* a₂ -> finite ;
coherence

proof end;

end;

registration

let c₁ be non empty finite set ;
let c₂, c₃ be Signature of c₁;
cluster a₂ +* a₃ -> gate`2=den ;
coherence

proof end;

end;

definition

let c₁ be non empty finite set ;
let c₂, c₃ be Signature of c₁;
redefine func +* as c₂ +* c₃ -> strict Signature of a₁;
coherence

proof end;

end;

definition

let c₁ be non empty finite set ;
let c₂, c₃ be Signature of c₁;
let c₄ be Circuit of c₁,c₂;
let c₅ be Circuit of c₁,c₃;
redefine func +* as c₄ +* c₅ -> strict Circuit of a₁,a₂ +* a₃;
coherence

proof end;

end;

theorem Th34: :: CIRCCMB3:34

for b₁, b₂ being set holds
( the_rank_of b₁ in the_rank_of [b₁,b₂] & the_rank_of b₂ in the_rank_of [b₁,b₂] )

proof end;

theorem Th35: :: CIRCCMB3:35

for b₁ being non empty finite non void unsplit gate`1=arity gate`2=den ManySortedSign
for b₂ being non-empty Circuit of b₁ st b₂ is gate`2=den holds
b₂ is with_stabilization-limit

proof end;

registration

let c₁ be non empty finite set ;
let c₂ be finite Signature of c₁;
cluster -> non-empty gate`2=den with_stabilization-limit Circuit of a₁,a₂;
coherence by Th35;

end;

scheme :: CIRCCMB3:sch 6
s6{ F₁() -> non empty set , F₂( set ) -> Element of F₁() } :

( ex b₁ being Function of 1 -tuples_on F₁(),F₁() st
for b₂ being Element of F₁() holds b₁ . <*b₂*> = F₂(b₂) & ( for b₁, b₂ being Function of 1 -tuples_on F₁(),F₁() st ( for b₃ being Element of F₁() holds b₁ . <*b₃*> = F₂(b₃) ) & ( for b₃ being Element of F₁() holds b₂ . <*b₃*> = F₂(b₃) ) holds
b₁ = b₂ ) )

proof end;

scheme :: CIRCCMB3:sch 7
s7{ F₁() -> non empty set , F₂( set , set ) -> Element of F₁() } :

( ex b₁ being Function of 2 -tuples_on F₁(),F₁() st
for b₂, b₃ being Element of F₁() holds b₁ . <*b₂,b₃*> = F₂(b₂,b₃) & ( for b₁, b₂ being Function of 2 -tuples_on F₁(),F₁() st ( for b₃, b₄ being Element of F₁() holds b₁ . <*b₃,b₄*> = F₂(b₃,b₄) ) & ( for b₃, b₄ being Element of F₁() holds b₂ . <*b₃,b₄*> = F₂(b₃,b₄) ) holds
b₁ = b₂ ) )

proof end;

scheme :: CIRCCMB3:sch 8
s8{ F₁() -> non empty set , F₂( set , set , set ) -> Element of F₁() } :

( ex b₁ being Function of 3 -tuples_on F₁(),F₁() st
for b₂, b₃, b₄ being Element of F₁() holds b₁ . <*b₂,b₃,b₄*> = F₂(b₂,b₃,b₄) & ( for b₁, b₂ being Function of 3 -tuples_on F₁(),F₁() st ( for b₃, b₄, b₅ being Element of F₁() holds b₁ . <*b₃,b₄,b₅*> = F₂(b₃,b₄,b₅) ) & ( for b₃, b₄, b₅ being Element of F₁() holds b₂ . <*b₃,b₄,b₅*> = F₂(b₃,b₄,b₅) ) holds
b₁ = b₂ ) )

proof end;

theorem Th36: :: CIRCCMB3:36

for b₁ being Function
for b₂ being set st b₂ in dom b₁ holds
b₁ * <*b₂*> = <*(b₁ . b₂)*>

proof end;

theorem Th37: :: CIRCCMB3:37

for b₁ being Function
for b₂, b₃, b₄, b₅ being set st b₂ in dom b₁ & b₃ in dom b₁ & b₄ in dom b₁ & b₅ in dom b₁ holds
b₁ * <*b₂,b₃,b₄,b₅*> = <*(b₁ . b₂),(b₁ . b₃),(b₁ . b₄),(b₁ . b₅)*>

proof end;

theorem Th38: :: CIRCCMB3:38

for b₁ being Function
for b₂, b₃, b₄, b₅, b₆ being set st b₂ in dom b₁ & b₃ in dom b₁ & b₄ in dom b₁ & b₅ in dom b₁ & b₆ in dom b₁ holds
b₁ * <*b₂,b₃,b₄,b₅,b₆*> = <*(b₁ . b₂),(b₁ . b₃),(b₁ . b₄),(b₁ . b₅),(b₁ . b₆)*>

proof end;

scheme :: CIRCCMB3:sch 9
s9{ F₁() -> set , F₂() -> non empty finite set , F₃( set ) -> Element of F₂(), F₄() -> Function of 1 -tuples_on F₂(),F₂() } :

for b₁ being State of (1GateCircuit <*F₁()*>,F₄())
for b₂ being Element of F₂() st b₂ = b₁ . F₁() holds
(Result b₁) . (Output (1GateCircStr <*F₁()*>,F₄())) = F₃(b₂)

provided

E37: for b₁ being Function of 1 -tuples_on F₂(),F₂() holds
( b₁ = F₄() iff for b₂ being Element of F₂() holds b₁ . <*b₂*> = F₃(b₂) )

proof end;

scheme :: CIRCCMB3:sch 10
s10{ F₁() -> set , F₂() -> set , F₃() -> non empty finite set , F₄( set , set ) -> Element of F₃(), F₅() -> Function of 2 -tuples_on F₃(),F₃() } :

for b₁ being State of (1GateCircuit <*F₁(),F₂()*>,F₅())
for b₂, b₃ being Element of F₃() st b₂ = b₁ . F₁() & b₃ = b₁ . F₂() holds
(Result b₁) . (Output (1GateCircStr <*F₁(),F₂()*>,F₅())) = F₄(b₂,b₃)

provided

E37: for b₁ being Function of 2 -tuples_on F₃(),F₃() holds
( b₁ = F₅() iff for b₂, b₃ being Element of F₃() holds b₁ . <*b₂,b₃*> = F₄(b₂,b₃) )

proof end;

scheme :: CIRCCMB3:sch 11
s11{ F₁() -> set , F₂() -> set , F₃() -> set , F₄() -> non empty finite set , F₅( set , set , set ) -> Element of F₄(), F₆() -> Function of 3 -tuples_on F₄(),F₄() } :

for b₁ being State of (1GateCircuit <*F₁(),F₂(),F₃()*>,F₆())
for b₂, b₃, b₄ being Element of F₄() st b₂ = b₁ . F₁() & b₃ = b₁ . F₂() & b₄ = b₁ . F₃() holds
(Result b₁) . (Output (1GateCircStr <*F₁(),F₂(),F₃()*>,F₆())) = F₅(b₂,b₃,b₄)

provided

E37: for b₁ being Function of 3 -tuples_on F₄(),F₄() holds
( b₁ = F₆() iff for b₂, b₃, b₄ being Element of F₄() holds b₁ . <*b₂,b₃,b₄*> = F₅(b₂,b₃,b₄) )

proof end;

scheme :: CIRCCMB3:sch 12
s12{ F₁() -> set , F₂() -> set , F₃() -> set , F₄() -> set , F₅() -> non empty finite set , F₆( set , set , set , set ) -> Element of F₅(), F₇() -> Function of 4 -tuples_on F₅(),F₅() } :

for b₁ being State of (1GateCircuit <*F₁(),F₂(),F₃(),F₄()*>,F₇())
for b₂, b₃, b₄, b₅ being Element of F₅() st b₂ = b₁ . F₁() & b₃ = b₁ . F₂() & b₄ = b₁ . F₃() & b₅ = b₁ . F₄() holds
(Result b₁) . (Output (1GateCircStr <*F₁(),F₂(),F₃(),F₄()*>,F₇())) = F₆(b₂,b₃,b₄,b₅)

provided

E37: for b₁ being Function of 4 -tuples_on F₅(),F₅() holds
( b₁ = F₇() iff for b₂, b₃, b₄, b₅ being Element of F₅() holds b₁ . <*b₂,b₃,b₄,b₅*> = F₆(b₂,b₃,b₄,b₅) )

proof end;

scheme :: CIRCCMB3:sch 13
s13{ F₁() -> set , F₂() -> set , F₃() -> set , F₄() -> set , F₅() -> set , F₆() -> non empty finite set , F₇( set , set , set , set , set ) -> Element of F₆(), F₈() -> Function of 5 -tuples_on F₆(),F₆() } :

for b₁ being State of (1GateCircuit <*F₁(),F₂(),F₃(),F₄(),F₅()*>,F₈())
for b₂, b₃, b₄, b₅, b₆ being Element of F₆() st b₂ = b₁ . F₁() & b₃ = b₁ . F₂() & b₄ = b₁ . F₃() & b₅ = b₁ . F₄() & b₆ = b₁ . F₅() holds
(Result b₁) . (Output (1GateCircStr <*F₁(),F₂(),F₃(),F₄(),F₅()*>,F₈())) = F₇(b₂,b₃,b₄,b₅,b₆)

provided

E37: for b₁ being Function of 5 -tuples_on F₆(),F₆() holds
( b₁ = F₈() iff for b₂, b₃, b₄, b₅, b₆ being Element of F₆() holds b₁ . <*b₂,b₃,b₄,b₅,b₆*> = F₇(b₂,b₃,b₄,b₅,b₆) )

proof end;

theorem Th39: :: CIRCCMB3:39

for b₁ being Nat
for b₂ being non empty finite set
for b₃ being Function of b₁ -tuples_on b₂,b₂
for b₄ being FinSeqLen of b₁
for b₅ being Signature of b₂ st rng b₄ c= the carrier of b₅ & not Output (1GateCircStr b₄,b₃) in InputVertices b₅ holds
InputVertices (b₅ +* (1GateCircStr b₄,b₃)) = InputVertices b₅

proof end;

theorem Th40: :: CIRCCMB3:40

for b₁, b₂ being set
for b₃ being non empty finite set
for b₄ being Nat
for b₅ being Function of b₄ -tuples_on b₃,b₃
for b₆ being FinSeqLen of b₄
for b₇ being Signature of b₃ st rng b₆ = b₁ \/ b₂ & b₁ c= the carrier of b₇ & b₂ misses InnerVertices b₇ & not Output (1GateCircStr b₆,b₅) in InputVertices b₇ holds
InputVertices (b₇ +* (1GateCircStr b₆,b₅)) = (InputVertices b₇) \/ b₂

proof end;

theorem Th41: :: CIRCCMB3:41

for b₁ being set
for b₂ being non empty finite set
for b₃ being Function of 1 -tuples_on b₂,b₂
for b₄ being Signature of b₂ st b₁ in the carrier of b₄ & not Output (1GateCircStr <*b₁*>,b₃) in InputVertices b₄ holds
InputVertices (b₄ +* (1GateCircStr <*b₁*>,b₃)) = InputVertices b₄

proof end;

theorem Th42: :: CIRCCMB3:42

for b₁, b₂ being set
for b₃ being non empty finite set
for b₄ being Function of 2 -tuples_on b₃,b₃
for b₅ being Signature of b₃ st b₁ in the carrier of b₅ & not b₂ in InnerVertices b₅ & not Output (1GateCircStr <*b₁,b₂*>,b₄) in InputVertices b₅ holds
InputVertices (b₅ +* (1GateCircStr <*b₁,b₂*>,b₄)) = (InputVertices b₅) \/ {b₂}

proof end;

theorem Th43: :: CIRCCMB3:43

for b₁, b₂ being set
for b₃ being non empty finite set
for b₄ being Function of 2 -tuples_on b₃,b₃
for b₅ being Signature of b₃ st b₂ in the carrier of b₅ & not b₁ in InnerVertices b₅ & not Output (1GateCircStr <*b₁,b₂*>,b₄) in InputVertices b₅ holds
InputVertices (b₅ +* (1GateCircStr <*b₁,b₂*>,b₄)) = (InputVertices b₅) \/ {b₁}

proof end;

theorem Th44: :: CIRCCMB3:44

for b₁, b₂ being set
for b₃ being non empty finite set
for b₄ being Function of 2 -tuples_on b₃,b₃
for b₅ being Signature of b₃ st b₁ in the carrier of b₅ & b₂ in the carrier of b₅ & not Output (1GateCircStr <*b₁,b₂*>,b₄) in InputVertices b₅ holds
InputVertices (b₅ +* (1GateCircStr <*b₁,b₂*>,b₄)) = InputVertices b₅

proof end;

theorem Th45: :: CIRCCMB3:45

for b₁, b₂, b₃ being set
for b₄ being non empty finite set
for b₅ being Function of 3 -tuples_on b₄,b₄
for b₆ being Signature of b₄ st b₁ in the carrier of b₆ & not b₂ in InnerVertices b₆ & not b₃ in InnerVertices b₆ & not Output (1GateCircStr <*b₁,b₂,b₃*>,b₅) in InputVertices b₆ holds
InputVertices (b₆ +* (1GateCircStr <*b₁,b₂,b₃*>,b₅)) = (InputVertices b₆) \/ {b₂,b₃}

proof end;

theorem Th46: :: CIRCCMB3:46

for b₁, b₂, b₃ being set
for b₄ being non empty finite set
for b₅ being Function of 3 -tuples_on b₄,b₄
for b₆ being Signature of b₄ st b₂ in the carrier of b₆ & not b₁ in InnerVertices b₆ & not b₃ in InnerVertices b₆ & not Output (1GateCircStr <*b₁,b₂,b₃*>,b₅) in InputVertices b₆ holds
InputVertices (b₆ +* (1GateCircStr <*b₁,b₂,b₃*>,b₅)) = (InputVertices b₆) \/ {b₁,b₃}

proof end;

theorem Th47: :: CIRCCMB3:47

for b₁, b₂, b₃ being set
for b₄ being non empty finite set
for b₅ being Function of 3 -tuples_on b₄,b₄
for b₆ being Signature of b₄ st b₃ in the carrier of b₆ & not b₁ in InnerVertices b₆ & not b₂ in InnerVertices b₆ & not Output (1GateCircStr <*b₁,b₂,b₃*>,b₅) in InputVertices b₆ holds
InputVertices (b₆ +* (1GateCircStr <*b₁,b₂,b₃*>,b₅)) = (InputVertices b₆) \/ {b₁,b₂}

proof end;

theorem Th48: :: CIRCCMB3:48

for b₁, b₂, b₃ being set
for b₄ being non empty finite set
for b₅ being Function of 3 -tuples_on b₄,b₄
for b₆ being Signature of b₄ st b₁ in the carrier of b₆ & b₂ in the carrier of b₆ & not b₃ in InnerVertices b₆ & not Output (1GateCircStr <*b₁,b₂,b₃*>,b₅) in InputVertices b₆ holds
InputVertices (b₆ +* (1GateCircStr <*b₁,b₂,b₃*>,b₅)) = (InputVertices b₆) \/ {b₃}

proof end;

theorem Th49: :: CIRCCMB3:49

for b₁, b₂, b₃ being set
for b₄ being non empty finite set
for b₅ being Function of 3 -tuples_on b₄,b₄
for b₆ being Signature of b₄ st b₁ in the carrier of b₆ & b₃ in the carrier of b₆ & not b₂ in InnerVertices b₆ & not Output (1GateCircStr <*b₁,b₂,b₃*>,b₅) in InputVertices b₆ holds
InputVertices (b₆ +* (1GateCircStr <*b₁,b₂,b₃*>,b₅)) = (InputVertices b₆) \/ {b₂}

proof end;

theorem Th50: :: CIRCCMB3:50

for b₁, b₂, b₃ being set
for b₄ being non empty finite set
for b₅ being Function of 3 -tuples_on b₄,b₄
for b₆ being Signature of b₄ st b₂ in the carrier of b₆ & b₃ in the carrier of b₆ & not b₁ in InnerVertices b₆ & not Output (1GateCircStr <*b₁,b₂,b₃*>,b₅) in InputVertices b₆ holds
InputVertices (b₆ +* (1GateCircStr <*b₁,b₂,b₃*>,b₅)) = (InputVertices b₆) \/ {b₁}

proof end;

theorem Th51: :: CIRCCMB3:51

for b₁, b₂, b₃ being set
for b₄ being non empty finite set
for b₅ being Function of 3 -tuples_on b₄,b₄
for b₆ being Signature of b₄ st b₁ in the carrier of b₆ & b₂ in the carrier of b₆ & b₃ in the carrier of b₆ & not Output (1GateCircStr <*b₁,b₂,b₃*>,b₅) in InputVertices b₆ holds
InputVertices (b₆ +* (1GateCircStr <*b₁,b₂,b₃*>,b₅)) = InputVertices b₆

proof end;

theorem Th52: :: CIRCCMB3:52

for b₁ being non empty finite set
for b₂ being finite Signature of b₁
for b₃ being Circuit of b₁,b₂
for b₄ being Nat
for b₅ being Function of b₄ -tuples_on b₁,b₁
for b₆ being FinSeqLen of b₄ st not Output (1GateCircStr b₆,b₅) in InputVertices b₂ holds
for b₇ being State of (b₃ +* (1GateCircuit b₆,b₅))
for b₈ being State of b₃ st b₈ = b₇ | the carrier of b₂ holds
stabilization-time b₇ <= 1 + (stabilization-time b₈)

proof end;

scheme :: CIRCCMB3:sch 14
s14{ F₁() -> set , F₂() -> non empty finite set , F₃( set ) -> Element of F₂(), F₄() -> finite Signature of F₂(), F₅() -> Circuit of F₂(),F₄(), F₆() -> Function of 1 -tuples_on F₂(),F₂() } :

for b₁ being State of (F₅() +* (1GateCircuit <*F₁()*>,F₆()))
for b₂ being State of F₅() st b₂ = b₁ | the carrier of F₄() holds
for b₃ being Element of F₂() st ( F₁() in InnerVertices F₄() implies b₃ = (Result b₂) . F₁() ) & ( not F₁() in InnerVertices F₄() implies b₃ = b₁ . F₁() ) holds
(Result b₁) . (Output (1GateCircStr <*F₁()*>,F₆())) = F₃(b₃)

provided

E51: for b₁ being Function of 1 -tuples_on F₂(),F₂() holds
( b₁ = F₆() iff for b₂ being Element of F₂() holds b₁ . <*b₂*> = F₃(b₂) ) and
E52: not Output (1GateCircStr <*F₁()*>,F₆()) in InputVertices F₄()

proof end;

scheme :: CIRCCMB3:sch 15
s15{ F₁() -> set , F₂() -> set , F₃() -> non empty finite set , F₄( set , set ) -> Element of F₃(), F₅() -> finite Signature of F₃(), F₆() -> Circuit of F₃(),F₅(), F₇() -> Function of 2 -tuples_on F₃(),F₃() } :

for b₁ being State of (F₆() +* (1GateCircuit <*F₁(),F₂()*>,F₇()))
for b₂ being State of F₆() st b₂ = b₁ | the carrier of F₅() holds
for b₃, b₄ being Element of F₃() st ( F₁() in InnerVertices F₅() implies b₃ = (Result b₂) . F₁() ) & ( not F₁() in InnerVertices F₅() implies b₃ = b₁ . F₁() ) & ( F₂() in InnerVertices F₅() implies b₄ = (Result b₂) . F₂() ) & ( not F₂() in InnerVertices F₅() implies b₄ = b₁ . F₂() ) holds
(Result b₁) . (Output (1GateCircStr <*F₁(),F₂()*>,F₇())) = F₄(b₃,b₄)

provided

E51: for b₁ being Function of 2 -tuples_on F₃(),F₃() holds
( b₁ = F₇() iff for b₂, b₃ being Element of F₃() holds b₁ . <*b₂,b₃*> = F₄(b₂,b₃) ) and
E52: not Output (1GateCircStr <*F₁(),F₂()*>,F₇()) in InputVertices F₅()

proof end;

scheme :: CIRCCMB3:sch 16
s16{ F₁() -> set , F₂() -> set , F₃() -> set , F₄() -> non empty finite set , F₅( set , set , set ) -> Element of F₄(), F₆() -> finite Signature of F₄(), F₇() -> Circuit of F₄(),F₆(), F₈() -> Function of 3 -tuples_on F₄(),F₄() } :

for b₁ being State of (F₇() +* (1GateCircuit <*F₁(),F₂(),F₃()*>,F₈()))
for b₂ being State of F₇() st b₂ = b₁ | the carrier of F₆() holds
for b₃, b₄, b₅ being Element of F₄() st ( F₁() in InnerVertices F₆() implies b₃ = (Result b₂) . F₁() ) & ( not F₁() in InnerVertices F₆() implies b₃ = b₁ . F₁() ) & ( F₂() in InnerVertices F₆() implies b₄ = (Result b₂) . F₂() ) & ( not F₂() in InnerVertices F₆() implies b₄ = b₁ . F₂() ) & ( F₃() in InnerVertices F₆() implies b₅ = (Result b₂) . F₃() ) & ( not F₃() in InnerVertices F₆() implies b₅ = b₁ . F₃() ) holds
(Result b₁) . (Output (1GateCircStr <*F₁(),F₂(),F₃()*>,F₈())) = F₅(b₃,b₄,b₅)

provided

E51: for b₁ being Function of 3 -tuples_on F₄(),F₄() holds
( b₁ = F₈() iff for b₂, b₃, b₄ being Element of F₄() holds b₁ . <*b₂,b₃,b₄*> = F₅(b₂,b₃,b₄) ) and
E52: not Output (1GateCircStr <*F₁(),F₂(),F₃()*>,F₈()) in InputVertices F₆()

proof end;

scheme :: CIRCCMB3:sch 17
s17{ F₁() -> set , F₂() -> set , F₃() -> set , F₄() -> set , F₅() -> non empty finite set , F₆( set , set , set , set ) -> Element of F₅(), F₇() -> finite Signature of F₅(), F₈() -> Circuit of F₅(),F₇(), F₉() -> Function of 4 -tuples_on F₅(),F₅() } :

for b₁ being State of (F₈() +* (1GateCircuit <*F₁(),F₂(),F₃(),F₄()*>,F₉()))
for b₂ being State of F₈() st b₂ = b₁ | the carrier of F₇() holds
for b₃, b₄, b₅, b₆ being Element of F₅() st ( F₁() in InnerVertices F₇() implies b₃ = (Result b₂) . F₁() ) & ( not F₁() in InnerVertices F₇() implies b₃ = b₁ . F₁() ) & ( F₂() in InnerVertices F₇() implies b₄ = (Result b₂) . F₂() ) & ( not F₂() in InnerVertices F₇() implies b₄ = b₁ . F₂() ) & ( F₃() in InnerVertices F₇() implies b₅ = (Result b₂) . F₃() ) & ( not F₃() in InnerVertices F₇() implies b₅ = b₁ . F₃() ) & ( F₄() in InnerVertices F₇() implies b₆ = (Result b₂) . F₄() ) & ( not F₄() in InnerVertices F₇() implies b₆ = b₁ . F₄() ) holds
(Result b₁) . (Output (1GateCircStr <*F₁(),F₂(),F₃(),F₄()*>,F₉())) = F₆(b₃,b₄,b₅,b₆)

provided

E51: for b₁ being Function of 4 -tuples_on F₅(),F₅() holds
( b₁ = F₉() iff for b₂, b₃, b₄, b₅ being Element of F₅() holds b₁ . <*b₂,b₃,b₄,b₅*> = F₆(b₂,b₃,b₄,b₅) ) and
E52: not Output (1GateCircStr <*F₁(),F₂(),F₃(),F₄()*>,F₉()) in InputVertices F₇()

proof end;

scheme :: CIRCCMB3:sch 18
s18{ F₁() -> set , F₂() -> set , F₃() -> set , F₄() -> set , F₅() -> set , F₆() -> non empty finite set , F₇( set , set , set , set , set ) -> Element of F₆(), F₈() -> finite Signature of F₆(), F₉() -> Circuit of F₆(),F₈(), F₁₀() -> Function of 5 -tuples_on F₆(),F₆() } :

for b₁ being State of (F₉() +* (1GateCircuit <*F₁(),F₂(),F₃(),F₄(),F₅()*>,F₁₀()))
for b₂ being State of F₉() st b₂ = b₁ | the carrier of F₈() holds
for b₃, b₄, b₅, b₆, b₇ being Element of F₆() st ( F₁() in InnerVertices F₈() implies b₃ = (Result b₂) . F₁() ) & ( not F₁() in InnerVertices F₈() implies b₃ = b₁ . F₁() ) & ( F₂() in InnerVertices F₈() implies b₄ = (Result b₂) . F₂() ) & ( not F₂() in InnerVertices F₈() implies b₄ = b₁ . F₂() ) & ( F₃() in InnerVertices F₈() implies b₅ = (Result b₂) . F₃() ) & ( not F₃() in InnerVertices F₈() implies b₅ = b₁ . F₃() ) & ( F₄() in InnerVertices F₈() implies b₆ = (Result b₂) . F₄() ) & ( not F₄() in InnerVertices F₈() implies b₆ = b₁ . F₄() ) & ( F₅() in InnerVertices F₈() implies b₇ = (Result b₂) . F₅() ) & ( not F₅() in InnerVertices F₈() implies b₇ = b₁ . F₅() ) holds
(Result b₁) . (Output (1GateCircStr <*F₁(),F₂(),F₃(),F₄(),F₅()*>,F₁₀())) = F₇(b₃,b₄,b₅,b₆,b₇)

provided

E51: for b₁ being Function of 5 -tuples_on F₆(),F₆() holds
( b₁ = F₁₀() iff for b₂, b₃, b₄, b₅, b₆ being Element of F₆() holds b₁ . <*b₂,b₃,b₄,b₅,b₆*> = F₇(b₂,b₃,b₄,b₅,b₆) ) and
E52: not Output (1GateCircStr <*F₁(),F₂(),F₃(),F₄(),F₅()*>,F₁₀()) in InputVertices F₈()

proof end;

definition

let c₁ be non empty ManySortedSign ;
attr a₁ is with_nonpair_inputs means :Def11: :: CIRCCMB3:def 11
not InputVertices a₁ is with_pair;

end;

:: deftheorem Def11 defines with_nonpair_inputs CIRCCMB3:def 11 :

registration

cluster NAT -> without_pairs ;
coherence

proof end;

let c₁ be without_pairs set ;
cluster -> without_pairs Element of bool a₁;
coherence

proof end;

end;

registration

cluster natural-yielding -> nonpair-yielding set ;
coherence

proof end;

end;

registration

cluster -> natural-yielding FinSequence of NAT ;
coherence

proof end;

end;

registration

cluster one-to-one nonpair-yielding natural-yielding set ;
existence

proof end;

end;

registration

let c₁ be Nat;
cluster one-to-one nonpair-yielding natural-yielding FinSeqLen of a₁;
existence

proof end;

end;

registration

let c₁ be nonpair-yielding FinSequence;
let c₂ be set ;
cluster 1GateCircStr a₁,a₂ -> finite with_nonpair_inputs ;
coherence

proof end;

end;

registration

cluster non empty finite strict non void unsplit gate`1=arity gate`2=den one-gate with_nonpair_inputs ManySortedSign ;
existence

proof end;

let c₁ be non empty finite set ;
cluster non empty finite strict non void unsplit gate`1=arity gate`2=den one-gate with_nonpair_inputs Signature of a₁;
existence

proof end;

end;

registration

let c₁ be non empty with_nonpair_inputs ManySortedSign ;
cluster InputVertices a₁ -> without_pairs ;
coherence by Def11;

end;

theorem Th53: :: CIRCCMB3:53

for b₁ being non empty with_nonpair_inputs ManySortedSign
for b₂ being Vertex of b₁ st b₂ is pair holds
b₂ in InnerVertices b₁

proof end;

registration

let c₁ be non empty unsplit gate`1=arity ManySortedSign ;
cluster InnerVertices a₁ -> Relation-like ;
coherence

proof end;

end;

registration

let c₁ be non empty non void unsplit gate`2=den ManySortedSign ;
cluster InnerVertices a₁ -> Relation-like ;
coherence

proof end;

end;

registration

let c₁, c₂ be non empty unsplit gate`1=arity with_nonpair_inputs ManySortedSign ;
cluster a₁ +* a₂ -> with_nonpair_inputs ;
coherence

proof end;

end;

theorem Th54: :: CIRCCMB3:54

for b₁ being non pair set
for b₂ being Relation holds not b₁ in b₂

proof end;

theorem Th55: :: CIRCCMB3:55

for b₁ being set
for b₂ being non empty finite set
for b₃ being Function of 1 -tuples_on b₂,b₂
for b₄ being with_nonpair_inputs Signature of b₂ st ( b₁ in the carrier of b₄ or not b₁ is pair ) holds
b₄ +* (1GateCircStr <*b₁*>,b₃) is with_nonpair_inputs

proof end;

registration

let c₁ be non empty finite set ;
let c₂ be with_nonpair_inputs Signature of c₁;
let c₃ be Vertex of c₂;
let c₄ be Function of 1 -tuples_on c₁,c₁;
cluster a₂ +* (1GateCircStr <*a₃*>,a₄) -> with_nonpair_inputs ;
coherence by Th55;

end;

registration

let c₁ be non empty finite set ;
let c₂ be with_nonpair_inputs Signature of c₁;
let c₃ be non pair set ;
let c₄ be Function of 1 -tuples_on c₁,c₁;
cluster a₂ +* (1GateCircStr <*a₃*>,a₄) -> gate`2=den with_nonpair_inputs ;
coherence ;

end;

Lemma53: for b₁ being non pair set holds not {b₁} is with_pair
;

Lemma54: for b₁, b₂ being without_pairs set holds not b₁ \/ b₂ is with_pair
;

theorem Th56: :: CIRCCMB3:56

for b₁, b₂ being set
for b₃ being non empty finite set
for b₄ being Function of 2 -tuples_on b₃,b₃
for b₅ being with_nonpair_inputs Signature of b₃ st ( b₁ in the carrier of b₅ or not b₁ is pair ) & ( b₂ in the carrier of b₅ or not b₂ is pair ) holds
b₅ +* (1GateCircStr <*b₁,b₂*>,b₄) is with_nonpair_inputs

proof end;

registration

let c₁ be non empty finite set ;
let c₂ be with_nonpair_inputs Signature of c₁;
let c₃ be Vertex of c₂;
let c₄ be non pair set ;
let c₅ be Function of 2 -tuples_on c₁,c₁;
cluster a₂ +* (1GateCircStr <*a₃,a₄*>,a₅) -> gate`2=den with_nonpair_inputs ;
coherence by Th56;
cluster a₂ +* (1GateCircStr <*a₄,a₃*>,a₅) -> gate`2=den with_nonpair_inputs ;
coherence by Th56;

end;

registration

let c₁ be non empty finite set ;
let c₂ be with_nonpair_inputs Signature of c₁;
let c₃, c₄ be Vertex of c₂;
let c₅ be Function of 2 -tuples_on c₁,c₁;
cluster a₂ +* (1GateCircStr <*a₃,a₄*>,a₅) -> gate`2=den with_nonpair_inputs ;
coherence by Th56;

end;

Lemma56: for b₁, b₂ being non pair set holds not {b₁,b₂} is with_pair
;

theorem Th57: :: CIRCCMB3:57

for b₁, b₂, b₃ being set
for b₄ being non empty finite set
for b₅ being Function of 3 -tuples_on b₄,b₄
for b₆ being with_nonpair_inputs Signature of b₄ st ( b₁ in the carrier of b₆ or not b₁ is pair ) & ( b₂ in the carrier of b₆ or not b₂ is pair ) & ( b₃ in the carrier of b₆ or not b₃ is pair ) holds
b₆ +* (1GateCircStr <*b₁,b₂,b₃*>,b₅) is with_nonpair_inputs

proof end;

registration

let c₁ be non empty finite set ;
let c₂ be with_nonpair_inputs Signature of c₁;
let c₃, c₄ be Vertex of c₂;
let c₅ be non pair set ;
let c₆ be Function of 3 -tuples_on c₁,c₁;
cluster a₂ +* (1GateCircStr <*a₃,a₄,a₅*>,a₆) -> gate`2=den with_nonpair_inputs ;
coherence by Th57;
cluster a₂ +* (1GateCircStr <*a₃,a₅,a₄*>,a₆) -> gate`2=den with_nonpair_inputs ;
coherence by Th57;
cluster a₂ +* (1GateCircStr <*a₅,a₃,a₄*>,a₆) -> gate`2=den with_nonpair_inputs ;
coherence by Th57;

end;

registration

let c₁ be non empty finite set ;
let c₂ be with_nonpair_inputs Signature of c₁;
let c₃ be Vertex of c₂;
let c₄, c₅ be non pair set ;
let c₆ be Function of 3 -tuples_on c₁,c₁;
cluster a₂ +* (1GateCircStr <*a₃,a₄,a₅*>,a₆) -> gate`2=den with_nonpair_inputs ;
coherence by Th57;
cluster a₂ +* (1GateCircStr <*a₄,a₃,a₅*>,a₆) -> gate`2=den with_nonpair_inputs ;
coherence by Th57;
cluster a₂ +* (1GateCircStr <*a₄,a₅,a₃*>,a₆) -> gate`2=den with_nonpair_inputs ;
coherence by Th57;

end;

registration

let c₁ be non empty finite set ;
let c₂ be with_nonpair_inputs Signature of c₁;
let c₃, c₄, c₅ be Vertex of c₂;
let c₆ be Function of 3 -tuples_on c₁,c₁;
cluster a₂ +* (1GateCircStr <*a₃,a₄,a₅*>,a₆) -> gate`2=den with_nonpair_inputs ;
coherence by Th57;

end;