:: CIRCCOMB semantic presentation

definition

let c₁ be ManySortedSign ;
mode Gate of a₁ is Element of the OperSymbols of a₁;

end;

registration

let c₁ be set ;
let c₂ be Function;
cluster a₁ --> a₂ -> Function-yielding ;
coherence

proof end;

end;

E1: now

let c₁ be Nat;
let c₂ be non empty set ;
thus product ((Seg c₁) --> c₂) = product (c₁ |-> c₂) by FINSEQ_2:def 2
.= c₁ -tuples_on c₂ by FUNCT_6:9 ;

end;

E2: now

let c₁ be non void ManySortedSign ;
let c₂ be Gate of c₁;
not the OperSymbols of c₁ is empty by MSUALG_1:def 5;
hence c₂ in the OperSymbols of c₁ ;

end;

registration

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

proof end;

end;

definition

let c₁, c₂ be set ;
let c₃ be ManySortedSet of c₁;
let c₄ be ManySortedSet of c₂;
redefine func +* as c₃ +* c₄ -> ManySortedSet of a₁ \/ a₂;
coherence

proof end;

end;

theorem Th1: :: CIRCCOMB:1

canceled;

theorem Th2: :: CIRCCOMB:2

for b₁, b₂, b₃ being Function st rng b₃ c= dom b₁ & rng b₃ c= dom b₂ & b₁ tolerates b₂ holds
b₁ * b₃ = b₂ * b₃

proof end;

theorem Th3: :: CIRCCOMB:3

for b₁, b₂ being set
for b₃ being ManySortedSet of b₁
for b₄ being ManySortedSet of b₂ st b₃ c= b₄ holds
b₃ # c= b₄ #

proof end;

theorem Th4: :: CIRCCOMB:4

for b₁, b₂, b₃, b₄ being set holds
( b₁ --> b₃ tolerates b₂ --> b₄ iff ( b₃ = b₄ or b₁ misses b₂ ) )

proof end;

theorem Th5: :: CIRCCOMB:5

for b₁, b₂, b₃ being Function st b₁ tolerates b₂ & b₂ tolerates b₃ & b₃ tolerates b₁ holds
b₁ +* b₂ tolerates b₃

proof end;

theorem Th6: :: CIRCCOMB:6

for b₁ being set
for b₂ being non empty set
for b₃ being FinSequence of b₁ holds ((b₁ --> b₂) # ) . b₃ = (len b₃) -tuples_on b₂

proof end;

definition

let c₁ be set ;
let c₂, c₃ be V3 ManySortedSet of c₁;
let c₄ be set ;
let c₅, c₆ be V3 ManySortedSet of c₄;
let c₇ be ManySortedFunction of c₂,c₃;
let c₈ be ManySortedFunction of c₅,c₆;
redefine func +* as c₇ +* c₈ -> ManySortedFunction of a₂ +* a₅,a₃ +* a₆;
coherence

proof end;

end;

Lemma8: for b₁, b₂ being set
for b₃, b₄ being V3 ManySortedSet of b₁
for b₅, b₆ being V3 ManySortedSet of b₂
for b₇ being ManySortedFunction of b₃,b₄
for b₈ being ManySortedFunction of b₅,b₆ holds b₇ +* b₈ is ManySortedFunction of b₃ +* b₅,b₄ +* b₆
;

definition

let c₁, c₂ be ManySortedSign ;
pred c₁ tolerates c₂ means :: CIRCCOMB:def 1
( the Arity of a₁ tolerates the Arity of a₂ & the ResultSort of a₁ tolerates the ResultSort of a₂ );
reflexivity ;
symmetry ;

end;

:: deftheorem Def1 defines tolerates CIRCCOMB:def 1 :

definition

let c₁, c₂ be non empty ManySortedSign ;
func c₁ +* c₂ -> non empty strict ManySortedSign means :Def2: :: CIRCCOMB:def 2
( the carrier of a₃ = the carrier of a₁ \/ the carrier of a₂ & the OperSymbols of a₃ = the OperSymbols of a₁ \/ the OperSymbols of a₂ & the Arity of a₃ = the Arity of a₁ +* the Arity of a₂ & the ResultSort of a₃ = the ResultSort of a₁ +* the ResultSort of a₂ );
existence

proof end;

uniqueness ;

end;

:: deftheorem Def2 defines +* CIRCCOMB:def 2 :

theorem Th7: :: CIRCCOMB:7

for b₁, b₂, b₃ being non empty ManySortedSign st b₁ tolerates b₂ & b₂ tolerates b₃ & b₃ tolerates b₁ holds
b₁ +* b₂ tolerates b₃

proof end;

theorem Th8: :: CIRCCOMB:8

for b₁ being non empty ManySortedSign holds b₁ +* b₁ = ManySortedSign(# the carrier of b₁,the OperSymbols of b₁,the Arity of b₁,the ResultSort of b₁ #)

proof end;

theorem Th9: :: CIRCCOMB:9

for b₁, b₂ being non empty ManySortedSign st b₁ tolerates b₂ holds
b₁ +* b₂ = b₂ +* b₁

proof end;

theorem Th10: :: CIRCCOMB:10

for b₁, b₂, b₃ being non empty ManySortedSign holds (b₁ +* b₂) +* b₃ = b₁ +* (b₂ +* b₃)

proof end;

registration

cluster one-to-one set ;
existence

proof end;

end;

theorem Th11: :: CIRCCOMB:11

for b₁ being one-to-one Function
for b₂, b₃ being non empty Circuit-like ManySortedSign st the ResultSort of b₂ c= b₁ & the ResultSort of b₃ c= b₁ holds
b₂ +* b₃ is Circuit-like

proof end;

theorem Th12: :: CIRCCOMB:12

for b₁, b₂ being non empty Circuit-like ManySortedSign st InnerVertices b₁ misses InnerVertices b₂ holds
b₁ +* b₂ is Circuit-like

proof end;

theorem Th13: :: CIRCCOMB:13

for b₁, b₂ being non empty ManySortedSign st ( not b₁ is void or not b₂ is void ) holds
not b₁ +* b₂ is void

proof end;

theorem Th14: :: CIRCCOMB:14

for b₁, b₂ being non empty finite ManySortedSign holds b₁ +* b₂ is finite

proof end;

registration

let c₁ be non empty non void ManySortedSign ;
let c₂ be non empty ManySortedSign ;
cluster a₁ +* a₂ -> non empty strict non void ;
coherence by Th13;
cluster a₂ +* a₁ -> non empty strict non void ;
coherence by Th13;

end;

theorem Th15: :: CIRCCOMB:15

for b₁, b₂ being non empty ManySortedSign st b₁ tolerates b₂ holds
( InnerVertices (b₁ +* b₂) = (InnerVertices b₁) \/ (InnerVertices b₂) & InputVertices (b₁ +* b₂) c= (InputVertices b₁) \/ (InputVertices b₂) )

proof end;

theorem Th16: :: CIRCCOMB:16

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

proof end;

theorem Th17: :: CIRCCOMB:17

for b₁, b₂ being non empty ManySortedSign st b₁ tolerates b₂ holds
for b₃ being Vertex of b₁ st b₃ in InputVertices (b₁ +* b₂) holds
b₃ in InputVertices b₁

proof end;

theorem Th18: :: CIRCCOMB:18

for b₁ being non empty ManySortedSign
for b₂ being non empty non void ManySortedSign
for b₃ being OperSymbol of b₂
for b₄ being OperSymbol of (b₁ +* b₂) st b₃ = b₄ holds
( the_arity_of b₄ = the_arity_of b₃ & the_result_sort_of b₄ = the_result_sort_of b₃ )

proof end;

theorem Th19: :: CIRCCOMB:19

for b₁ being non empty ManySortedSign
for b₂, b₃ being non empty non void Circuit-like ManySortedSign st b₃ = b₁ +* b₂ holds
for b₄ being Vertex of b₂ st b₄ in InnerVertices b₂ holds
for b₅ being Vertex of b₃ st b₄ = b₅ holds
( b₅ in InnerVertices b₃ & action_at b₅ = action_at b₄ )

proof end;

theorem Th20: :: CIRCCOMB:20

for b₁ being non empty non void ManySortedSign
for b₂ being non empty ManySortedSign st b₁ tolerates b₂ holds
for b₃ being OperSymbol of b₁
for b₄ being OperSymbol of (b₁ +* b₂) st b₃ = b₄ holds
( the_arity_of b₄ = the_arity_of b₃ & the_result_sort_of b₄ = the_result_sort_of b₃ )

proof end;

theorem Th21: :: CIRCCOMB:21

for b₁, b₂ being non empty non void Circuit-like ManySortedSign
for b₃ being non empty ManySortedSign st b₁ tolerates b₃ & b₂ = b₁ +* b₃ holds
for b₄ being Vertex of b₁ st b₄ in InnerVertices b₁ holds
for b₅ being Vertex of b₂ st b₄ = b₅ holds
( b₅ in InnerVertices b₂ & action_at b₅ = action_at b₄ )

proof end;

definition

let c₁, c₂ be non empty ManySortedSign ;
let c₃ be MSAlgebra of c₁;
let c₄ be MSAlgebra of c₂;
pred c₃ tolerates c₄ means :Def3: :: CIRCCOMB:def 3
( a₁ tolerates a₂ & the Sorts of a₃ tolerates the Sorts of a₄ & the Charact of a₃ tolerates the Charact of a₄ );

end;

:: deftheorem Def3 defines tolerates CIRCCOMB:def 3 :

definition

let c₁, c₂ be non empty ManySortedSign ;
let c₃ be non-empty MSAlgebra of c₁;
let c₄ be non-empty MSAlgebra of c₂;
assume E22: the Sorts of c₃ tolerates the Sorts of c₄ ;
func c₃ +* c₄ -> strict non-empty MSAlgebra of a₁ +* a₂ means :Def4: :: CIRCCOMB:def 4
( the Sorts of a₅ = the Sorts of a₃ +* the Sorts of a₄ & the Charact of a₅ = the Charact of a₃ +* the Charact of a₄ );
uniqueness ;
existence

proof end;

end;

:: deftheorem Def4 defines +* CIRCCOMB:def 4 :

theorem Th22: :: CIRCCOMB:22

for b₁ being non empty non void ManySortedSign
for b₂ being MSAlgebra of b₁ holds b₂ tolerates b₂

proof end;

theorem Th23: :: CIRCCOMB:23

for b₁, b₂ being non empty non void ManySortedSign
for b₃ being MSAlgebra of b₁
for b₄ being MSAlgebra of b₂ st b₃ tolerates b₄ holds
b₄ tolerates b₃

proof end;

theorem Th24: :: CIRCCOMB:24

for b₁, b₂, b₃ being non empty ManySortedSign
for b₄ being non-empty MSAlgebra of b₁
for b₅ being non-empty MSAlgebra of b₂
for b₆ being MSAlgebra of b₃ st b₄ tolerates b₅ & b₅ tolerates b₆ & b₆ tolerates b₄ holds
b₄ +* b₅ tolerates b₆

proof end;

theorem Th25: :: CIRCCOMB:25

for b₁ being non empty strict ManySortedSign
for b₂ being non-empty MSAlgebra of b₁ holds b₂ +* b₂ = MSAlgebra(# the Sorts of b₂,the Charact of b₂ #)

proof end;

theorem Th26: :: CIRCCOMB:26

for b₁, b₂ being non empty ManySortedSign
for b₃ being non-empty MSAlgebra of b₁
for b₄ being non-empty MSAlgebra of b₂ st b₃ tolerates b₄ holds
b₃ +* b₄ = b₄ +* b₃

proof end;

theorem Th27: :: CIRCCOMB:27

for b₁, b₂, b₃ being non empty ManySortedSign
for b₄ being non-empty MSAlgebra of b₁
for b₅ being non-empty MSAlgebra of b₂
for b₆ being non-empty MSAlgebra of b₃ st the Sorts of b₄ tolerates the Sorts of b₅ & the Sorts of b₅ tolerates the Sorts of b₆ & the Sorts of b₆ tolerates the Sorts of b₄ holds
(b₄ +* b₅) +* b₆ = b₄ +* (b₅ +* b₆)

proof end;

theorem Th28: :: CIRCCOMB:28

for b₁, b₂ being non empty ManySortedSign
for b₃ being non-empty locally-finite MSAlgebra of b₁
for b₄ being non-empty locally-finite MSAlgebra of b₂ st the Sorts of b₃ tolerates the Sorts of b₄ holds
b₃ +* b₄ is locally-finite

proof end;

theorem Th29: :: CIRCCOMB:29

for b₁, b₂ being non-empty Function
for b₃ being Element of product b₁
for b₄ being Element of product b₂ holds b₃ +* b₄ in product (b₁ +* b₂)

proof end;

theorem Th30: :: CIRCCOMB:30

for b₁, b₂ being non-empty Function
for b₃ being Element of product (b₁ +* b₂) holds b₃ | (dom b₂) in product b₂

proof end;

theorem Th31: :: CIRCCOMB:31

for b₁, b₂ being non-empty Function st b₁ tolerates b₂ holds
for b₃ being Element of product (b₁ +* b₂) holds b₃ | (dom b₁) in product b₁

proof end;

theorem Th32: :: CIRCCOMB:32

for b₁, b₂ being non empty ManySortedSign
for b₃ being non-empty MSAlgebra of b₁
for b₄ being Element of product the Sorts of b₃
for b₅ being non-empty MSAlgebra of b₂
for b₆ being Element of product the Sorts of b₅ st the Sorts of b₃ tolerates the Sorts of b₅ holds
b₄ +* b₆ in product the Sorts of (b₃ +* b₅)

proof end;

theorem Th33: :: CIRCCOMB:33

for b₁, b₂ being non empty ManySortedSign
for b₃ being non-empty MSAlgebra of b₁
for b₄ being non-empty MSAlgebra of b₂ st the Sorts of b₃ tolerates the Sorts of b₄ holds
for b₅ being Element of product the Sorts of (b₃ +* b₄) holds
( b₅ | the carrier of b₁ in product the Sorts of b₃ & b₅ | the carrier of b₂ in product the Sorts of b₄ )

proof end;

theorem Th34: :: CIRCCOMB:34

for b₁, b₂ being non empty non void ManySortedSign
for b₃ being non-empty MSAlgebra of b₁
for b₄ being non-empty MSAlgebra of b₂ st the Sorts of b₃ tolerates the Sorts of b₄ holds
for b₅ being OperSymbol of (b₁ +* b₂)
for b₆ being OperSymbol of b₂ st b₅ = b₆ holds
Den b₅,(b₃ +* b₄) = Den b₆,b₄

proof end;

theorem Th35: :: CIRCCOMB:35

for b₁, b₂ being non empty non void ManySortedSign
for b₃ being non-empty MSAlgebra of b₁
for b₄ being non-empty MSAlgebra of b₂ st the Sorts of b₃ tolerates the Sorts of b₄ & the Charact of b₃ tolerates the Charact of b₄ holds
for b₅ being OperSymbol of (b₁ +* b₂)
for b₆ being OperSymbol of b₁ st b₅ = b₆ holds
Den b₅,(b₃ +* b₄) = Den b₆,b₃

proof end;

theorem Th36: :: CIRCCOMB:36

for b₁, b₂, 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₂
for b₆ being non-empty Circuit of b₃
for b₇ being State of b₆
for b₈ being State of b₅ st b₈ = b₇ | the carrier of b₂ holds
for b₉ being Gate of b₃
for b₁₀ being Gate of b₂ st b₉ = b₁₀ holds
b₉ depends_on_in b₇ = b₁₀ depends_on_in b₈

proof end;

theorem Th37: :: CIRCCOMB:37

for b₁, b₂, b₃ being non empty non void Circuit-like ManySortedSign st b₃ = b₁ +* b₂ & b₁ tolerates 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₃
for b₇ being State of b₆
for b₈ being State of b₄ st b₈ = b₇ | the carrier of b₁ holds
for b₉ being Gate of b₃
for b₁₀ being Gate of b₁ st b₉ = b₁₀ holds
b₉ depends_on_in b₇ = b₁₀ depends_on_in b₈

proof end;

theorem Th38: :: CIRCCOMB:38

for b₁, b₂, 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₂
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 Vertex of b₃ holds
( ( for b₉ being State of b₄ st b₉ = b₇ | the carrier of b₁ & ( b₈ in InnerVertices b₁ or ( b₈ in the carrier of b₁ & b₈ in InputVertices b₃ ) ) holds
(Following b₇) . b₈ = (Following b₉) . b₈ ) & ( for b₉ being State of b₅ st b₉ = b₇ | the carrier of b₂ & ( b₈ in InnerVertices b₂ or ( b₈ in the carrier of b₂ & b₈ in InputVertices b₃ ) ) holds
(Following b₇) . b₈ = (Following b₉) . b₈ ) )

proof end;

theorem Th39: :: CIRCCOMB:39

for b₁, b₂, b₃ being non empty non void Circuit-like ManySortedSign st InnerVertices b₁ misses InputVertices 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₄
for b₉ being State of b₅ st b₈ = b₇ | the carrier of b₁ & b₉ = b₇ | the carrier of b₂ holds
Following b₇ = (Following b₈) +* (Following b₉)

proof end;

theorem Th40: :: CIRCCOMB:40

for b₁, b₂, b₃ being non empty non void Circuit-like ManySortedSign st InnerVertices b₂ misses InputVertices 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₄
for b₉ being State of b₅ st b₈ = b₇ | the carrier of b₁ & b₉ = b₇ | the carrier of b₂ holds
Following b₇ = (Following b₉) +* (Following b₈)

proof end;

theorem Th41: :: CIRCCOMB:41

for b₁, b₂, b₃ being non empty non void Circuit-like ManySortedSign st InputVertices b₁ c= InputVertices 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₄
for b₉ being State of b₅ st b₈ = b₇ | the carrier of b₁ & b₉ = b₇ | the carrier of b₂ holds
Following b₇ = (Following b₉) +* (Following b₈)

proof end;

theorem Th42: :: CIRCCOMB:42

for b₁, b₂, b₃ being non empty non void Circuit-like ManySortedSign st InputVertices b₂ c= InputVertices 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₄
for b₉ being State of b₅ st b₈ = b₇ | the carrier of b₁ & b₉ = b₇ | the carrier of b₂ holds
Following b₇ = (Following b₈) +* (Following b₉)

proof end;

definition

let c₁, c₂ be non empty set ;
let c₃ be Element of c₁;
redefine func --> as c₂ --> c₃ -> Function of a₂,a₁;
coherence by FUNCOP_1:57;

end;

definition

let c₁ be set ;
let c₂ be FinSequence;
let c₃ be set ;
func 1GateCircStr c₂,c₁,c₃ -> strict non void ManySortedSign means :Def5: :: CIRCCOMB:def 5
( the carrier of a₄ = (rng a₂) \/ {a₃} & the OperSymbols of a₄ = {[a₂,a₁]} & the Arity of a₄ . [a₂,a₁] = a₂ & the ResultSort of a₄ . [a₂,a₁] = a₃ );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def5 defines 1GateCircStr CIRCCOMB:def 5 :

registration

let c₁ be set ;
let c₂ be FinSequence;
let c₃ be set ;
cluster 1GateCircStr a₂,a₁,a₃ -> non empty strict non void ;
coherence

proof end;

end;

theorem Th43: :: CIRCCOMB:43

for b₁, b₂ being set
for b₃ being FinSequence holds
( the Arity of (1GateCircStr b₃,b₁,b₂) = {[b₃,b₁]} --> b₃ & the ResultSort of (1GateCircStr b₃,b₁,b₂) = {[b₃,b₁]} --> b₂ )

proof end;

theorem Th44: :: CIRCCOMB:44

for b₁, b₂ being set
for b₃ being FinSequence
for b₄ being Gate of (1GateCircStr b₃,b₁,b₂) holds
( b₄ = [b₃,b₁] & the_arity_of b₄ = b₃ & the_result_sort_of b₄ = b₂ )

proof end;

theorem Th45: :: CIRCCOMB:45

for b₁, b₂ being set
for b₃ being FinSequence holds
( InputVertices (1GateCircStr b₃,b₁,b₂) = (rng b₃) \ {b₂} & InnerVertices (1GateCircStr b₃,b₁,b₂) = {b₂} )

proof end;

definition

let c₁ be set ;
let c₂ be FinSequence;
func 1GateCircStr c₂,c₁ -> strict non void ManySortedSign means :Def6: :: CIRCCOMB:def 6
( the carrier of a₃ = (rng a₂) \/ {[a₂,a₁]} & the OperSymbols of a₃ = {[a₂,a₁]} & the Arity of a₃ . [a₂,a₁] = a₂ & the ResultSort of a₃ . [a₂,a₁] = [a₂,a₁] );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def6 defines 1GateCircStr CIRCCOMB:def 6 :

registration

let c₁ be set ;
let c₂ be FinSequence;
cluster 1GateCircStr a₂,a₁ -> non empty strict non void ;
coherence

proof end;

end;

theorem Th46: :: CIRCCOMB:46

for b₁ being set
for b₂ being FinSequence holds 1GateCircStr b₂,b₁ = 1GateCircStr b₂,b₁,[b₂,b₁]

proof end;

theorem Th47: :: CIRCCOMB:47

for b₁ being set
for b₂ being FinSequence holds
( the Arity of (1GateCircStr b₂,b₁) = {[b₂,b₁]} --> b₂ & the ResultSort of (1GateCircStr b₂,b₁) = {[b₂,b₁]} --> [b₂,b₁] )

proof end;

theorem Th48: :: CIRCCOMB:48

for b₁ being set
for b₂ being FinSequence
for b₃ being Gate of (1GateCircStr b₂,b₁) holds
( b₃ = [b₂,b₁] & the_arity_of b₃ = b₂ & the_result_sort_of b₃ = b₃ )

proof end;

theorem Th49: :: CIRCCOMB:49

for b₁ being set
for b₂ being FinSequence holds
( InputVertices (1GateCircStr b₂,b₁) = rng b₂ & InnerVertices (1GateCircStr b₂,b₁) = {[b₂,b₁]} )

proof end;

theorem Th50: :: CIRCCOMB:50

for b₁ being set
for b₂ being FinSequence
for b₃ being set st b₃ in rng b₂ holds
the_rank_of b₃ in the_rank_of [b₂,b₁]

proof end;

theorem Th51: :: CIRCCOMB:51

for b₁ being set
for b₂, b₃ being FinSequence holds 1GateCircStr b₂,b₁ tolerates 1GateCircStr b₃,b₁

proof end;

definition

let c₁ be ManySortedSign ;
attr a₁ is unsplit means :Def7: :: CIRCCOMB:def 7
the ResultSort of a₁ = id the OperSymbols of a₁;
attr a₁ is gate`1=arity means :Def8: :: CIRCCOMB:def 8
for b₁ being set st b₁ in the OperSymbols of a₁ holds
b₁ = [(the Arity of a₁ . b₁),(b₁ `2 )];
attr a₁ is gate`2isBoolean means :Def9: :: CIRCCOMB:def 9
for b₁ being set st b₁ in the OperSymbols of a₁ holds
for b₂ being FinSequence st b₂ = the Arity of a₁ . b₁ holds
ex b₃ being Function of (len b₂) -tuples_on BOOLEAN , BOOLEAN st b₁ = [(b₁ `1 ),b₃];

end;

:: deftheorem Def7 defines unsplit CIRCCOMB:def 7 :

:: deftheorem Def8 defines gate`1=arity CIRCCOMB:def 8 :

:: deftheorem Def9 defines gate`2isBoolean CIRCCOMB:def 9 :

definition

let c₁ be non empty ManySortedSign ;
let c₂ be MSAlgebra of c₁;
attr a₂ is gate`2=den means :Def10: :: CIRCCOMB:def 10
for b₁ being set st b₁ in the OperSymbols of a₁ holds
b₁ = [(b₁ `1 ),(the Charact of a₂ . b₁)];

end;

:: deftheorem Def10 defines gate`2=den CIRCCOMB:def 10 :

definition

let c₁ be non empty ManySortedSign ;
attr a₁ is gate`2=den means :: CIRCCOMB:def 11
ex b₁ being MSAlgebra of a₁ st b₁ is gate`2=den;

end;

:: deftheorem Def11 defines gate`2=den CIRCCOMB:def 11 :

scheme :: CIRCCOMB:sch 1
s1{ F₁() -> set , F₂() -> set , F₃() -> Function of F₁(),F₂(), F₄( set , set ) -> set } :

ex b₁ being ManySortedSet of F₁() st
for b₂ being set
for b₃ being Element of F₂() st b₂ in F₁() & b₃ = F₃() . b₂ holds
b₁ . b₂ = F₄(b₂,b₃)

proof end;

scheme :: CIRCCOMB:sch 2
s2{ F₁() -> non empty ManySortedSign , F₂( set , set ) -> set } :

ex b₁ being strict MSAlgebra of F₁() st
( the Sorts of b₁ = the carrier of F₁() --> BOOLEAN & ( for b₂ being set
for b₃ being Element of the carrier of F₁() * st b₂ in the OperSymbols of F₁() & b₃ = the Arity of F₁() . b₂ holds
the Charact of b₁ . b₂ = F₂(b₂,b₃) ) )

provided

E46: for b₁ being set
for b₂ being Element of the carrier of F₁() * st b₁ in the OperSymbols of F₁() & b₂ = the Arity of F₁() . b₁ holds
F₂(b₁,b₂) is Function of (len b₂) -tuples_on BOOLEAN , BOOLEAN

proof end;

registration

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

proof end;

end;

theorem Th52: :: CIRCCOMB:52

for b₁ being non empty ManySortedSign holds
( b₁ is unsplit iff for b₂ being set st b₂ in the OperSymbols of b₁ holds
the ResultSort of b₁ . b₂ = b₂ )

proof end;

theorem Th53: :: CIRCCOMB:53

for b₁ being non empty ManySortedSign st b₁ is unsplit holds
the OperSymbols of b₁ c= the carrier of b₁

proof end;

registration

cluster non empty unsplit -> non empty Circuit-like ManySortedSign ;
coherence

proof end;

end;

theorem Th54: :: CIRCCOMB:54

for b₁ being set
for b₂ being FinSequence holds
( 1GateCircStr b₂,b₁ is unsplit & 1GateCircStr b₂,b₁ is gate`1=arity )

proof end;

registration

let c₁ be set ;
let c₂ be FinSequence;
cluster 1GateCircStr a₂,a₁ -> non empty strict non void Circuit-like unsplit gate`1=arity ;
coherence by Th54;

end;

registration

cluster non empty strict non void Circuit-like unsplit gate`1=arity ManySortedSign ;
existence

proof end;

end;

theorem Th55: :: CIRCCOMB:55

for b₁, b₂ being non empty unsplit gate`1=arity ManySortedSign holds b₁ tolerates b₂

proof end;

theorem Th56: :: CIRCCOMB:56

for b₁, b₂ being non empty ManySortedSign
for b₃ being MSAlgebra of b₁
for b₄ being MSAlgebra of b₂ st b₃ is gate`2=den & b₄ is gate`2=den holds
the Charact of b₃ tolerates the Charact of b₄

proof end;

theorem Th57: :: CIRCCOMB:57

for b₁, b₂ being non empty unsplit ManySortedSign holds b₁ +* b₂ is unsplit

proof end;

registration

let c₁, c₂ be non empty unsplit ManySortedSign ;
cluster a₁ +* a₂ -> non empty strict Circuit-like unsplit ;
coherence by Th57;

end;

theorem Th58: :: CIRCCOMB:58

for b₁, b₂ being non empty gate`1=arity ManySortedSign holds b₁ +* b₂ is gate`1=arity

proof end;

registration

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

end;

theorem Th59: :: CIRCCOMB:59

for b₁, b₂ being non empty ManySortedSign st b₁ is gate`2isBoolean & b₂ is gate`2isBoolean holds
b₁ +* b₂ is gate`2isBoolean

proof end;

definition

let c₁ be Nat;
mode FinSeqLen of c₁ -> FinSequence means :Def12: :: CIRCCOMB:def 12
len a₂ = a₁;
existence

proof end;

end;

:: deftheorem Def12 defines FinSeqLen CIRCCOMB:def 12 :

definition

let c₁ be Nat;
let c₂, c₃ be non empty set ;
let c₄ be Function of c₁ -tuples_on c₂,c₃;
let c₅ be FinSeqLen of c₁;
let c₆ be set ;
assume E54: ( c₆ in rng c₅ implies c₂ = c₃ ) ;
func 1GateCircuit c₅,c₄,c₆ -> strict non-empty MSAlgebra of 1GateCircStr a₅,a₄,a₆ means :: CIRCCOMB:def 13
( the Sorts of a₇ = ((rng a₅) --> a₂) +* ({a₆} --> a₃) & the Charact of a₇ . [a₅,a₄] = a₄ );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def13 defines 1GateCircuit CIRCCOMB:def 13 :

definition

let c₁ be Nat;
let c₂ be non empty set ;
let c₃ be Function of c₁ -tuples_on c₂,c₂;
let c₄ be FinSeqLen of c₁;
func 1GateCircuit c₄,c₃ -> strict non-empty MSAlgebra of 1GateCircStr a₄,a₃ means :Def14: :: CIRCCOMB:def 14
( the Sorts of a₅ = the carrier of (1GateCircStr a₄,a₃) --> a₂ & the Charact of a₅ . [a₄,a₃] = a₃ );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def14 defines 1GateCircuit CIRCCOMB:def 14 :

theorem Th60: :: CIRCCOMB:60

for b₁ being Nat
for b₂ being non empty set
for b₃ being Function of b₁ -tuples_on b₂,b₂
for b₄ being FinSeqLen of b₁ holds
( 1GateCircuit b₄,b₃ is gate`2=den & 1GateCircStr b₄,b₃ is gate`2=den )

proof end;

registration

let c₁ be Nat;
let c₂ be non empty set ;
let c₃ be Function of c₁ -tuples_on c₂,c₂;
let c₄ be FinSeqLen of c₁;
cluster 1GateCircuit a₄,a₃ -> strict non-empty gate`2=den ;
coherence by Th60;
cluster 1GateCircStr a₄,a₃ -> non empty strict non void Circuit-like unsplit gate`1=arity gate`2=den ;
coherence by Th60;

end;

theorem Th61: :: CIRCCOMB:61

for b₁ being Nat
for b₂ being FinSeqLen of b₁
for b₃ being Function of b₁ -tuples_on BOOLEAN , BOOLEAN holds 1GateCircStr b₂,b₃ is gate`2isBoolean

proof end;

registration

let c₁ be Nat;
let c₂ be Function of c₁ -tuples_on BOOLEAN , BOOLEAN ;
let c₃ be FinSeqLen of c₁;
cluster 1GateCircStr a₃,a₂ -> non empty strict non void Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ;
coherence by Th61;

end;

registration

cluster non empty gate`2isBoolean gate`2=den ManySortedSign ;
existence

proof end;

end;

registration

let c₁, c₂ be non empty gate`2isBoolean ManySortedSign ;
cluster a₁ +* a₂ -> non empty strict gate`2isBoolean gate`2=den ;
coherence by Th59;

end;

theorem Th62: :: CIRCCOMB:62

for b₁ being Nat
for b₂ being non empty set
for b₃ being Function of b₁ -tuples_on b₂,b₂
for b₄ being FinSeqLen of b₁ holds
( the Charact of (1GateCircuit b₄,b₃) = {[b₄,b₃]} --> b₃ & ( for b₅ being Vertex of (1GateCircStr b₄,b₃) holds the Sorts of (1GateCircuit b₄,b₃) . b₅ = b₂ ) )

proof end;

registration

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₁;
cluster 1GateCircuit a₄,a₃ -> strict non-empty locally-finite gate`2=den ;
coherence

proof end;

end;

theorem Th63: :: CIRCCOMB:63

for b₁ being Nat
for b₂ being non empty set
for b₃ being Function of b₁ -tuples_on b₂,b₂
for b₄, b₅ being FinSeqLen of b₁ holds 1GateCircuit b₄,b₃ tolerates 1GateCircuit b₅,b₃

proof end;

theorem Th64: :: CIRCCOMB:64

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₅) . [b₄,b₃] = b₃ . (b₅ * b₄)

proof end;

definition

redefine func BOOLEAN as BOOLEAN -> non empty finite Subset of NAT ;
coherence by MARGREL1:def 12, ZFMISC_1:38;

end;

definition

let c₁ be non empty ManySortedSign ;
let c₂ be MSAlgebra of c₁;
attr a₂ is Boolean means :Def15: :: CIRCCOMB:def 15
for b₁ being Vertex of a₁ holds the Sorts of a₂ . b₁ = BOOLEAN ;

end;

:: deftheorem Def15 defines Boolean CIRCCOMB:def 15 :

theorem Th65: :: CIRCCOMB:65

for b₁ being non empty ManySortedSign
for b₂ being MSAlgebra of b₁ holds
( b₂ is Boolean iff the Sorts of b₂ = the carrier of b₁ --> BOOLEAN )

proof end;

registration

let c₁ be non empty ManySortedSign ;
cluster Boolean -> non-empty locally-finite MSAlgebra of a₁;
coherence

proof end;

end;

theorem Th66: :: CIRCCOMB:66

for b₁ being non empty ManySortedSign
for b₂ being MSAlgebra of b₁ holds
( b₂ is Boolean iff rng the Sorts of b₂ c= {BOOLEAN } )

proof end;

theorem Th67: :: CIRCCOMB:67

for b₁, b₂ being non empty ManySortedSign
for b₃ being MSAlgebra of b₁
for b₄ being MSAlgebra of b₂ st b₃ is Boolean & b₄ is Boolean holds
the Sorts of b₃ tolerates the Sorts of b₄

proof end;

theorem Th68: :: CIRCCOMB:68

for b₁, b₂ being non empty unsplit gate`1=arity ManySortedSign
for b₃ being MSAlgebra of b₁
for b₄ being MSAlgebra of b₂ st b₃ is Boolean & b₃ is gate`2=den & b₄ is Boolean & b₄ is gate`2=den holds
b₃ tolerates b₄

proof end;

registration

let c₁ be non empty ManySortedSign ;
cluster strict non-empty locally-finite Boolean MSAlgebra of a₁;
existence

proof end;

end;

theorem Th69: :: CIRCCOMB:69

for b₁ being Nat
for b₂ being Function of b₁ -tuples_on BOOLEAN , BOOLEAN
for b₃ being FinSeqLen of b₁ holds 1GateCircuit b₃,b₂ is Boolean

proof end;

theorem Th70: :: CIRCCOMB:70

for b₁, b₂ being non empty ManySortedSign
for b₃ being Boolean MSAlgebra of b₁
for b₄ being Boolean MSAlgebra of b₂ holds b₃ +* b₄ is Boolean

proof end;

theorem Th71: :: CIRCCOMB:71

for b₁, b₂ being non empty ManySortedSign
for b₃ being non-empty MSAlgebra of b₁
for b₄ being non-empty MSAlgebra of b₂ st b₃ is gate`2=den & b₄ is gate`2=den & the Sorts of b₃ tolerates the Sorts of b₄ holds
b₃ +* b₄ is gate`2=den

proof end;

registration

cluster non empty strict non void Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign ;
existence

proof end;

end;

registration

let c₁ be non empty gate`2isBoolean ManySortedSign ;
cluster strict non-empty locally-finite gate`2=den Boolean MSAlgebra of a₁;
existence

proof end;

end;

registration

let c₁, c₂ be non empty non void unsplit gate`2isBoolean ManySortedSign ;
let c₃ be gate`2=den Boolean Circuit of c₁;
let c₄ be gate`2=den Boolean Circuit of c₂;
cluster a₃ +* a₄ -> strict non-empty locally-finite gate`2=den Boolean ;
coherence

proof end;

end;

registration

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₁;
cluster strict non-empty gate`2=den MSAlgebra of 1GateCircStr a₄,a₃;
existence

proof end;

end;

registration

end;

theorem Th72: :: CIRCCOMB:72

for b₁, b₂ being non empty non void unsplit gate`1=arity gate`2isBoolean ManySortedSign
for b₃ being gate`2=den Boolean Circuit of b₁
for b₄ being gate`2=den Boolean Circuit of b₂
for b₅ being State of (b₃ +* b₄)
for b₆ being Vertex of (b₁ +* b₂) holds
( ( for b₇ being State of b₃ st b₇ = b₅ | the carrier of b₁ & ( b₆ in InnerVertices b₁ or ( b₆ in the carrier of b₁ & b₆ in InputVertices (b₁ +* b₂) ) ) holds
(Following b₅) . b₆ = (Following b₇) . b₆ ) & ( for b₇ being State of b₄ st b₇ = b₅ | the carrier of b₂ & ( b₆ in InnerVertices b₂ or ( b₆ in the carrier of b₂ & b₆ in InputVertices (b₁ +* b₂) ) ) holds
(Following b₅) . b₆ = (Following b₇) . b₆ ) )

proof end;