:: CIRCCOMB semantic presentation

definition

let S be ManySortedSign ;
mode Gate of S is Element of the OperSymbols of S;

end;

registration

let A be set ;
let f be Function;
cluster A --> f -> Function-yielding ;
coherence

proof end;

end;

Lm1: now

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

end;

Lm2: now

let S be non void ManySortedSign ; :: thesis:
let o be Gate of S; :: thesis:
not the OperSymbols of S is empty by MSUALG_1:def 5;
hence o in the OperSymbols of S ; :: thesis:

end;

registration

let f, g be non-empty Function;
cluster f +* g -> non-empty ;
coherence

proof end;

end;

definition

let A, B be set ;
let f be ManySortedSet of A;
let g be ManySortedSet of B;
:: original: +*
redefine func f +* g -> ManySortedSet of A \/ B;
coherence

proof end;

end;

theorem :: CIRCCOMB:1

canceled;

theorem Th2: :: CIRCCOMB:2

for f1, f2, g being Function st rng g c= dom f1 & rng g c= dom f2 & f1 tolerates f2 holds
f1 * g = f2 * g

proof end;

theorem Th3: :: CIRCCOMB:3

for A, B being set
for f being ManySortedSet of A
for g being ManySortedSet of B st f c= g holds
f # c= g #

proof end;

theorem Th4: :: CIRCCOMB:4

for X, Y, x, y being set holds
( X --> x tolerates Y --> y iff ( x = y or X misses Y ) )

proof end;

theorem Th5: :: CIRCCOMB:5

for f, g, h being Function st f tolerates g & g tolerates h & h tolerates f holds
f +* g tolerates h

proof end;

theorem Th6: :: CIRCCOMB:6

for X being set
for Y being non empty set
for p being FinSequence of X holds ((X --> Y) # ) . p = (len p) -tuples_on Y

proof end;

definition

let A be set ;
let f1, g1 be V3 ManySortedSet of A;
let B be set ;
let f2, g2 be V3 ManySortedSet of B;
let h1 be ManySortedFunction of f1,g1;
let h2 be ManySortedFunction of f2,g2;
:: original: +*
redefine func h1 +* h2 -> ManySortedFunction of f1 +* f2,g1 +* g2;
coherence

proof end;

end;

Lm3: for A, B being set
for f1, g1 being V3 ManySortedSet of A
for f2, g2 being V3 ManySortedSet of B
for h1 being ManySortedFunction of f1,g1
for h2 being ManySortedFunction of f2,g2 holds h1 +* h2 is ManySortedFunction of f1 +* f2,g1 +* g2
;

definition

let S1, S2 be ManySortedSign ;
pred S1 tolerates S2 means :: CIRCCOMB:def 1
( the Arity of S1 tolerates the Arity of S2 & the ResultSort of S1 tolerates the ResultSort of S2 );
reflexivity ;
symmetry ;

end;

:: deftheorem defines tolerates CIRCCOMB:def 1 :

definition

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

proof end;

uniqueness ;

end;

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

theorem Th7: :: CIRCCOMB:7

for S1, S2, S3 being non empty ManySortedSign st S1 tolerates S2 & S2 tolerates S3 & S3 tolerates S1 holds
S1 +* S2 tolerates S3

proof end;

theorem Th8: :: CIRCCOMB:8

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

proof end;

theorem Th9: :: CIRCCOMB:9

for S1, S2 being non empty ManySortedSign st S1 tolerates S2 holds
S1 +* S2 = S2 +* S1

proof end;

theorem :: CIRCCOMB:10

for S1, S2, S3 being non empty ManySortedSign holds (S1 +* S2) +* S3 = S1 +* (S2 +* S3)

proof end;

registration

cluster one-to-one set ;
existence

proof end;

end;

theorem :: CIRCCOMB:11

for f being one-to-one Function
for S1, S2 being non empty Circuit-like ManySortedSign st the ResultSort of S1 c= f & the ResultSort of S2 c= f holds
S1 +* S2 is Circuit-like

proof end;

theorem :: CIRCCOMB:12

for S1, S2 being non empty Circuit-like ManySortedSign st InnerVertices S1 misses InnerVertices S2 holds
S1 +* S2 is Circuit-like

proof end;

theorem Th13: :: CIRCCOMB:13

for S1, S2 being non empty ManySortedSign st ( not S1 is void or not S2 is void ) holds
not S1 +* S2 is void

proof end;

theorem :: CIRCCOMB:14

for S1, S2 being non empty finite ManySortedSign holds S1 +* S2 is finite

proof end;

registration

let S1 be non empty non void ManySortedSign ;
let S2 be non empty ManySortedSign ;
cluster S1 +* S2 -> non empty strict non void ;
coherence by Th13;
cluster S2 +* S1 -> non empty strict non void ;
coherence by Th13;

end;

theorem Th15: :: CIRCCOMB:15

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

proof end;

theorem Th16: :: CIRCCOMB:16

for S1, S2 being non empty ManySortedSign
for v2 being Vertex of S2 st v2 in InputVertices (S1 +* S2) holds
v2 in InputVertices S2

proof end;

theorem Th17: :: CIRCCOMB:17

for S1, S2 being non empty ManySortedSign st S1 tolerates S2 holds
for v1 being Vertex of S1 st v1 in InputVertices (S1 +* S2) holds
v1 in InputVertices S1

proof end;

theorem Th18: :: CIRCCOMB:18

for S1 being non empty ManySortedSign
for S2 being non empty non void ManySortedSign
for o2 being OperSymbol of S2
for o being OperSymbol of (S1 +* S2) st o2 = o holds
( the_arity_of o = the_arity_of o2 & the_result_sort_of o = the_result_sort_of o2 )

proof end;

theorem Th19: :: CIRCCOMB:19

for S1 being non empty ManySortedSign
for S2, S being non empty non void Circuit-like ManySortedSign st S = S1 +* S2 holds
for v2 being Vertex of S2 st v2 in InnerVertices S2 holds
for v being Vertex of S st v2 = v holds
( v in InnerVertices S & action_at v = action_at v2 )

proof end;

theorem Th20: :: CIRCCOMB:20

for S1 being non empty non void ManySortedSign
for S2 being non empty ManySortedSign st S1 tolerates S2 holds
for o1 being OperSymbol of S1
for o being OperSymbol of (S1 +* S2) st o1 = o holds
( the_arity_of o = the_arity_of o1 & the_result_sort_of o = the_result_sort_of o1 )

proof end;

theorem Th21: :: CIRCCOMB:21

for S1, S being non empty non void Circuit-like ManySortedSign
for S2 being non empty ManySortedSign st S1 tolerates S2 & S = S1 +* S2 holds
for v1 being Vertex of S1 st v1 in InnerVertices S1 holds
for v being Vertex of S st v1 = v holds
( v in InnerVertices S & action_at v = action_at v1 )

proof end;

definition

let S1, S2 be non empty ManySortedSign ;
let A1 be MSAlgebra of S1;
let A2 be MSAlgebra of S2;
pred A1 tolerates A2 means :Def3: :: CIRCCOMB:def 3
( S1 tolerates S2 & the Sorts of A1 tolerates the Sorts of A2 & the Charact of A1 tolerates the Charact of A2 );

end;

:: deftheorem Def3 defines tolerates CIRCCOMB:def 3 :

definition

let S1, S2 be non empty ManySortedSign ;
let A1 be non-empty MSAlgebra of S1;
let A2 be non-empty MSAlgebra of S2;
assume A1: the Sorts of A1 tolerates the Sorts of A2 ;
func A1 +* A2 -> strict non-empty MSAlgebra of S1 +* S2 means :Def4: :: CIRCCOMB:def 4
( the Sorts of it = the Sorts of A1 +* the Sorts of A2 & the Charact of it = the Charact of A1 +* the Charact of A2 );
uniqueness ;
existence

proof end;

end;

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

theorem :: CIRCCOMB:22

for S being non empty non void ManySortedSign
for A being MSAlgebra of S holds A tolerates A

proof end;

theorem Th23: :: CIRCCOMB:23

for S1, S2 being non empty non void ManySortedSign
for A1 being MSAlgebra of S1
for A2 being MSAlgebra of S2 st A1 tolerates A2 holds
A2 tolerates A1

proof end;

theorem :: CIRCCOMB:24

for S1, S2, S3 being non empty ManySortedSign
for A1 being non-empty MSAlgebra of S1
for A2 being non-empty MSAlgebra of S2
for A3 being MSAlgebra of S3 st A1 tolerates A2 & A2 tolerates A3 & A3 tolerates A1 holds
A1 +* A2 tolerates A3

proof end;

theorem :: CIRCCOMB:25

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

proof end;

theorem Th26: :: CIRCCOMB:26

for S1, S2 being non empty ManySortedSign
for A1 being non-empty MSAlgebra of S1
for A2 being non-empty MSAlgebra of S2 st A1 tolerates A2 holds
A1 +* A2 = A2 +* A1

proof end;

theorem :: CIRCCOMB:27

for S1, S2, S3 being non empty ManySortedSign
for A1 being non-empty MSAlgebra of S1
for A2 being non-empty MSAlgebra of S2
for A3 being non-empty MSAlgebra of S3 st the Sorts of A1 tolerates the Sorts of A2 & the Sorts of A2 tolerates the Sorts of A3 & the Sorts of A3 tolerates the Sorts of A1 holds
(A1 +* A2) +* A3 = A1 +* (A2 +* A3)

proof end;

theorem :: CIRCCOMB:28

for S1, S2 being non empty ManySortedSign
for A1 being non-empty locally-finite MSAlgebra of S1
for A2 being non-empty locally-finite MSAlgebra of S2 st the Sorts of A1 tolerates the Sorts of A2 holds
A1 +* A2 is locally-finite

proof end;

theorem Th29: :: CIRCCOMB:29

for f, g being non-empty Function
for x being Element of product f
for y being Element of product g holds x +* y in product (f +* g)

proof end;

theorem Th30: :: CIRCCOMB:30

for f, g being non-empty Function
for x being Element of product (f +* g) holds x | (dom g) in product g

proof end;

theorem Th31: :: CIRCCOMB:31

for f, g being non-empty Function st f tolerates g holds
for x being Element of product (f +* g) holds x | (dom f) in product f

proof end;

theorem :: CIRCCOMB:32

for S1, S2 being non empty ManySortedSign
for A1 being non-empty MSAlgebra of S1
for s1 being Element of product the Sorts of A1
for A2 being non-empty MSAlgebra of S2
for s2 being Element of product the Sorts of A2 st the Sorts of A1 tolerates the Sorts of A2 holds
s1 +* s2 in product the Sorts of (A1 +* A2)

proof end;

theorem :: CIRCCOMB:33

for S1, S2 being non empty ManySortedSign
for A1 being non-empty MSAlgebra of S1
for A2 being non-empty MSAlgebra of S2 st the Sorts of A1 tolerates the Sorts of A2 holds
for s being Element of product the Sorts of (A1 +* A2) holds
( s | the carrier of S1 in product the Sorts of A1 & s | the carrier of S2 in product the Sorts of A2 )

proof end;

theorem Th34: :: CIRCCOMB:34

for S1, S2 being non empty non void ManySortedSign
for A1 being non-empty MSAlgebra of S1
for A2 being non-empty MSAlgebra of S2 st the Sorts of A1 tolerates the Sorts of A2 holds
for o being OperSymbol of (S1 +* S2)
for o2 being OperSymbol of S2 st o = o2 holds
Den o,(A1 +* A2) = Den o2,A2

proof end;

theorem Th35: :: CIRCCOMB:35

for S1, S2 being non empty non void ManySortedSign
for A1 being non-empty MSAlgebra of S1
for A2 being non-empty MSAlgebra of S2 st the Sorts of A1 tolerates the Sorts of A2 & the Charact of A1 tolerates the Charact of A2 holds
for o being OperSymbol of (S1 +* S2)
for o1 being OperSymbol of S1 st o = o1 holds
Den o,(A1 +* A2) = Den o1,A1

proof end;

theorem Th36: :: CIRCCOMB:36

for S1, S2, S being non empty non void Circuit-like ManySortedSign st S = S1 +* S2 holds
for A1 being non-empty Circuit of S1
for A2 being non-empty Circuit of S2
for A being non-empty Circuit of S
for s being State of A
for s2 being State of A2 st s2 = s | the carrier of S2 holds
for g being Gate of S
for g2 being Gate of S2 st g = g2 holds
g depends_on_in s = g2 depends_on_in s2

proof end;

theorem Th37: :: CIRCCOMB:37

for S1, S2, S being non empty non void Circuit-like ManySortedSign st S = S1 +* S2 & S1 tolerates S2 holds
for A1 being non-empty Circuit of S1
for A2 being non-empty Circuit of S2
for A being non-empty Circuit of S
for s being State of A
for s1 being State of A1 st s1 = s | the carrier of S1 holds
for g being Gate of S
for g1 being Gate of S1 st g = g1 holds
g depends_on_in s = g1 depends_on_in s1

proof end;

theorem Th38: :: CIRCCOMB:38

for S1, S2, S being non empty non void Circuit-like ManySortedSign st S = S1 +* S2 holds
for A1 being non-empty Circuit of S1
for A2 being non-empty Circuit of S2
for A being non-empty Circuit of S st A1 tolerates A2 & A = A1 +* A2 holds
for s being State of A
for v being Vertex of S holds
( ( for s1 being State of A1 st s1 = s | the carrier of S1 & ( v in InnerVertices S1 or ( v in the carrier of S1 & v in InputVertices S ) ) holds
(Following s) . v = (Following s1) . v ) & ( for s2 being State of A2 st s2 = s | the carrier of S2 & ( v in InnerVertices S2 or ( v in the carrier of S2 & v in InputVertices S ) ) holds
(Following s) . v = (Following s2) . v ) )

proof end;

theorem Th39: :: CIRCCOMB:39

for S1, S2, S being non empty non void Circuit-like ManySortedSign st InnerVertices S1 misses InputVertices S2 & S = S1 +* S2 holds
for A1 being non-empty Circuit of S1
for A2 being non-empty Circuit of S2
for A being non-empty Circuit of S st A1 tolerates A2 & A = A1 +* A2 holds
for s being State of A
for s1 being State of A1
for s2 being State of A2 st s1 = s | the carrier of S1 & s2 = s | the carrier of S2 holds
Following s = (Following s1) +* (Following s2)

proof end;

theorem Th40: :: CIRCCOMB:40

for S1, S2, S being non empty non void Circuit-like ManySortedSign st InnerVertices S2 misses InputVertices S1 & S = S1 +* S2 holds
for A1 being non-empty Circuit of S1
for A2 being non-empty Circuit of S2
for A being non-empty Circuit of S st A1 tolerates A2 & A = A1 +* A2 holds
for s being State of A
for s1 being State of A1
for s2 being State of A2 st s1 = s | the carrier of S1 & s2 = s | the carrier of S2 holds
Following s = (Following s2) +* (Following s1)

proof end;

theorem :: CIRCCOMB:41

for S1, S2, S being non empty non void Circuit-like ManySortedSign st InputVertices S1 c= InputVertices S2 & S = S1 +* S2 holds
for A1 being non-empty Circuit of S1
for A2 being non-empty Circuit of S2
for A being non-empty Circuit of S st A1 tolerates A2 & A = A1 +* A2 holds
for s being State of A
for s1 being State of A1
for s2 being State of A2 st s1 = s | the carrier of S1 & s2 = s | the carrier of S2 holds
Following s = (Following s2) +* (Following s1)

proof end;

theorem :: CIRCCOMB:42

for S1, S2, S being non empty non void Circuit-like ManySortedSign st InputVertices S2 c= InputVertices S1 & S = S1 +* S2 holds
for A1 being non-empty Circuit of S1
for A2 being non-empty Circuit of S2
for A being non-empty Circuit of S st A1 tolerates A2 & A = A1 +* A2 holds
for s being State of A
for s1 being State of A1
for s2 being State of A2 st s1 = s | the carrier of S1 & s2 = s | the carrier of S2 holds
Following s = (Following s1) +* (Following s2)

proof end;

definition

let A, B be non empty set ;
let a be Element of A;
:: original: -->
redefine func B --> a -> Function of B,A;
coherence by FUNCOP_1:57;

end;

definition

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

proof end;

uniqueness

proof end;

end;

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

registration

let f be set ;
let p be FinSequence;
let x be set ;
cluster 1GateCircStr p,f,x -> non empty strict non void ;
coherence

proof end;

end;

theorem Th43: :: CIRCCOMB:43

for f, x being set
for p being FinSequence holds
( the Arity of (1GateCircStr p,f,x) = {[p,f]} --> p & the ResultSort of (1GateCircStr p,f,x) = {[p,f]} --> x )

proof end;

theorem :: CIRCCOMB:44

for f, x being set
for p being FinSequence
for g being Gate of (1GateCircStr p,f,x) holds
( g = [p,f] & the_arity_of g = p & the_result_sort_of g = x )

proof end;

theorem :: CIRCCOMB:45

for f, x being set
for p being FinSequence holds
( InputVertices (1GateCircStr p,f,x) = (rng p) \ {x} & InnerVertices (1GateCircStr p,f,x) = {x} )

proof end;

definition

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

proof end;

uniqueness

proof end;

end;

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

registration

let f be set ;
let p be FinSequence;
cluster 1GateCircStr p,f -> non empty strict non void ;
coherence

proof end;

end;

theorem :: CIRCCOMB:46

for f being set
for p being FinSequence holds 1GateCircStr p,f = 1GateCircStr p,f,[p,f]

proof end;

theorem Th47: :: CIRCCOMB:47

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

proof end;

theorem Th48: :: CIRCCOMB:48

for f being set
for p being FinSequence
for g being Gate of (1GateCircStr p,f) holds
( g = [p,f] & the_arity_of g = p & the_result_sort_of g = g )

proof end;

theorem Th49: :: CIRCCOMB:49

for f being set
for p being FinSequence holds
( InputVertices (1GateCircStr p,f) = rng p & InnerVertices (1GateCircStr p,f) = {[p,f]} )

proof end;

theorem :: CIRCCOMB:50

for f being set
for p being FinSequence
for x being set st x in rng p holds
the_rank_of x in the_rank_of [p,f]

proof end;

theorem Th51: :: CIRCCOMB:51

for f being set
for p, q being FinSequence holds 1GateCircStr p,f tolerates 1GateCircStr q,f

proof end;

definition

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

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 S be non empty ManySortedSign ;
let IT be MSAlgebra of S;
attr IT is gate`2=den means :Def10: :: CIRCCOMB:def 10
for g being set st g in the OperSymbols of S holds
g = [(g `1 ),(the Charact of IT . g)];

end;

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

definition

let IT be non empty ManySortedSign ;
attr IT is gate`2=den means :: CIRCCOMB:def 11
ex A being MSAlgebra of IT st A is gate`2=den;

end;

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

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

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

proof end;

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

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

provided

A1: for g being set
for p being Element of the carrier of F₁() * st g in the OperSymbols of F₁() & p = the Arity of F₁() . g holds
F₂(g,p) is Function of (len p) -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 S being non empty ManySortedSign holds
( S is unsplit iff for o being set st o in the OperSymbols of S holds
the ResultSort of S . o = o )

proof end;

theorem :: CIRCCOMB:53

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

proof end;

registration

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

proof end;

end;

theorem Th54: :: CIRCCOMB:54

for f being set
for p being FinSequence holds
( 1GateCircStr p,f is unsplit & 1GateCircStr p,f is gate`1=arity )

proof end;

registration

let f be set ;
let p be FinSequence;
cluster 1GateCircStr p,f -> 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 S1, S2 being non empty unsplit gate`1=arity ManySortedSign holds S1 tolerates S2

proof end;

theorem Th56: :: CIRCCOMB:56

for S1, S2 being non empty ManySortedSign
for A1 being MSAlgebra of S1
for A2 being MSAlgebra of S2 st A1 is gate`2=den & A2 is gate`2=den holds
the Charact of A1 tolerates the Charact of A2

proof end;

theorem Th57: :: CIRCCOMB:57

for S1, S2 being non empty unsplit ManySortedSign holds S1 +* S2 is unsplit

proof end;

registration

let S1, S2 be non empty unsplit ManySortedSign ;
cluster S1 +* S2 -> non empty strict Circuit-like unsplit ;
coherence by Th57;

end;

theorem Th58: :: CIRCCOMB:58

for S1, S2 being non empty gate`1=arity ManySortedSign holds S1 +* S2 is gate`1=arity

proof end;

registration

let S1, S2 be non empty gate`1=arity ManySortedSign ;
cluster S1 +* S2 -> non empty strict gate`1=arity ;
coherence by Th58;

end;

theorem Th59: :: CIRCCOMB:59

for S1, S2 being non empty ManySortedSign st S1 is gate`2isBoolean & S2 is gate`2isBoolean holds
S1 +* S2 is gate`2isBoolean

proof end;

definition

let n be Nat;
mode FinSeqLen of n -> FinSequence means :Def12: :: CIRCCOMB:def 12
len it = n;
existence

proof end;

end;

:: deftheorem Def12 defines FinSeqLen CIRCCOMB:def 12 :

definition

let n be Nat;
let X, Y be non empty set ;
let f be Function of n -tuples_on X,Y;
let p be FinSeqLen of n;
let x be set ;
assume A1: ( x in rng p implies X = Y ) ;
func 1GateCircuit p,f,x -> strict non-empty MSAlgebra of 1GateCircStr p,f,x means :: CIRCCOMB:def 13
( the Sorts of it = ((rng p) --> X) +* ({x} --> Y) & the Charact of it . [p,f] = f );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem defines 1GateCircuit CIRCCOMB:def 13 :

definition

let n be Nat;
let X be non empty set ;
let f be Function of n -tuples_on X,X;
let p be FinSeqLen of n;
func 1GateCircuit p,f -> strict non-empty MSAlgebra of 1GateCircStr p,f means :Def14: :: CIRCCOMB:def 14
( the Sorts of it = the carrier of (1GateCircStr p,f) --> X & the Charact of it . [p,f] = f );
existence

proof end;

uniqueness

proof end;

end;

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

theorem Th60: :: CIRCCOMB:60

for n being Nat
for X being non empty set
for f being Function of n -tuples_on X,X
for p being FinSeqLen of n holds
( 1GateCircuit p,f is gate`2=den & 1GateCircStr p,f is gate`2=den )

proof end;

registration

let n be Nat;
let X be non empty set ;
let f be Function of n -tuples_on X,X;
let p be FinSeqLen of n;
cluster 1GateCircuit p,f -> strict non-empty gate`2=den ;
coherence by Th60;
cluster 1GateCircStr p,f -> non empty strict non void Circuit-like unsplit gate`1=arity gate`2=den ;
coherence by Th60;

end;

theorem Th61: :: CIRCCOMB:61

for n being Nat
for p being FinSeqLen of n
for f being Function of n -tuples_on BOOLEAN , BOOLEAN holds 1GateCircStr p,f is gate`2isBoolean

proof end;

registration

let n be Nat;
let f be Function of n -tuples_on BOOLEAN , BOOLEAN ;
let p be FinSeqLen of n;
cluster 1GateCircStr p,f -> 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 S1, S2 be non empty gate`2isBoolean ManySortedSign ;
cluster S1 +* S2 -> non empty strict gate`2isBoolean gate`2=den ;
coherence by Th59;

end;

theorem Th62: :: CIRCCOMB:62

for n being Nat
for X being non empty set
for f being Function of n -tuples_on X,X
for p being FinSeqLen of n holds
( the Charact of (1GateCircuit p,f) = {[p,f]} --> f & ( for v being Vertex of (1GateCircStr p,f) holds the Sorts of (1GateCircuit p,f) . v = X ) )

proof end;

registration

let n be Nat;
let X be non empty finite set ;
let f be Function of n -tuples_on X,X;
let p be FinSeqLen of n;
cluster 1GateCircuit p,f -> strict non-empty locally-finite gate`2=den ;
coherence

proof end;

end;

theorem :: CIRCCOMB:63

for n being Nat
for X being non empty set
for f being Function of n -tuples_on X,X
for p, q being FinSeqLen of n holds 1GateCircuit p,f tolerates 1GateCircuit q,f

proof end;

theorem :: CIRCCOMB:64

for n being Nat
for X being non empty finite set
for f being Function of n -tuples_on X,X
for p being FinSeqLen of n
for s being State of (1GateCircuit p,f) holds (Following s) . [p,f] = f . (s * p)

proof end;

definition

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

end;

definition

let S be non empty ManySortedSign ;
let IT be MSAlgebra of S;
attr IT is Boolean means :Def15: :: CIRCCOMB:def 15
for v being Vertex of S holds the Sorts of IT . v = BOOLEAN ;

end;

:: deftheorem Def15 defines Boolean CIRCCOMB:def 15 :

theorem Th65: :: CIRCCOMB:65

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

proof end;

registration

let S be non empty ManySortedSign ;
cluster Boolean -> non-empty locally-finite MSAlgebra of S;
coherence

proof end;

end;

theorem :: CIRCCOMB:66

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

proof end;

theorem Th67: :: CIRCCOMB:67

for S1, S2 being non empty ManySortedSign
for A1 being MSAlgebra of S1
for A2 being MSAlgebra of S2 st A1 is Boolean & A2 is Boolean holds
the Sorts of A1 tolerates the Sorts of A2

proof end;

theorem Th68: :: CIRCCOMB:68

for S1, S2 being non empty unsplit gate`1=arity ManySortedSign
for A1 being MSAlgebra of S1
for A2 being MSAlgebra of S2 st A1 is Boolean & A1 is gate`2=den & A2 is Boolean & A2 is gate`2=den holds
A1 tolerates A2

proof end;

registration

let S be non empty ManySortedSign ;
cluster strict non-empty locally-finite Boolean MSAlgebra of S;
existence

proof end;

end;

theorem :: CIRCCOMB:69

for n being Nat
for f being Function of n -tuples_on BOOLEAN , BOOLEAN
for p being FinSeqLen of n holds 1GateCircuit p,f is Boolean

proof end;

theorem Th70: :: CIRCCOMB:70

for S1, S2 being non empty ManySortedSign
for A1 being Boolean MSAlgebra of S1
for A2 being Boolean MSAlgebra of S2 holds A1 +* A2 is Boolean

proof end;

theorem Th71: :: CIRCCOMB:71

for S1, S2 being non empty ManySortedSign
for A1 being non-empty MSAlgebra of S1
for A2 being non-empty MSAlgebra of S2 st A1 is gate`2=den & A2 is gate`2=den & the Sorts of A1 tolerates the Sorts of A2 holds
A1 +* A2 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 S be non empty gate`2isBoolean ManySortedSign ;
cluster strict non-empty locally-finite gate`2=den Boolean MSAlgebra of S;
existence

proof end;

end;

registration

let S1, S2 be non empty non void unsplit gate`2isBoolean ManySortedSign ;
let A1 be gate`2=den Boolean Circuit of S1;
let A2 be gate`2=den Boolean Circuit of S2;
cluster A1 +* A2 -> strict non-empty locally-finite gate`2=den Boolean ;
coherence

proof end;

end;

registration

let n be Nat;
let X be non empty finite set ;
let f be Function of n -tuples_on X,X;
let p be FinSeqLen of n;
cluster strict non-empty gate`2=den MSAlgebra of 1GateCircStr p,f;
existence

proof end;

end;

registration

end;

theorem :: CIRCCOMB:72

for S1, S2 being non empty non void unsplit gate`1=arity gate`2isBoolean ManySortedSign
for A1 being gate`2=den Boolean Circuit of S1
for A2 being gate`2=den Boolean Circuit of S2
for s being State of (A1 +* A2)
for v being Vertex of (S1 +* S2) holds
( ( for s1 being State of A1 st s1 = s | the carrier of S1 & ( v in InnerVertices S1 or ( v in the carrier of S1 & v in InputVertices (S1 +* S2) ) ) holds
(Following s) . v = (Following s1) . v ) & ( for s2 being State of A2 st s2 = s | the carrier of S2 & ( v in InnerVertices S2 or ( v in the carrier of S2 & v in InputVertices (S1 +* S2) ) ) holds
(Following s) . v = (Following s2) . v ) )

proof end;