:: Combining of Circuits
:: by Yatsuka Nakamura and Grzegorz Bancerek
::
:: Received May 11, 1995
:: Copyright (c) 1995-2012 Association of Mizar Users


begin

definition
let S be ManySortedSign ;
mode Gate of S is Element of the carrier' of S;
end;

Lm1: now :: thesis: for i being Element of NAT
for X being non empty set holds product ((Seg i) --> X) = i -tuples_on X
let i be Element of NAT ; :: thesis: for X being non empty set holds product ((Seg i) --> X) = i -tuples_on X
let X be non empty set ; :: thesis: product ((Seg i) --> X) = i -tuples_on X
thus product ((Seg i) --> X) = product (i |-> X) by FINSEQ_2:def 2
.= i -tuples_on X by FINSEQ_3:131 ; :: thesis: verum
end;

registration
let A, B be set ;
let f be ManySortedSet of A;
let g be ManySortedSet of B;
cluster f +* g -> A \/ B -defined ;
coherence
f +* g is A \/ B -defined
proof end;
end;

registration
let A, B be set ;
let f be ManySortedSet of A;
let g be ManySortedSet of B;
cluster f +* g -> A \/ B -defined total for A \/ B -defined Function;
coherence
for b1 being A \/ B -defined Function st b1 = f +* g holds
b1 is total
proof end;
end;

registration
let A, B be set ;
cluster A .--> B -> {A} -defined ;
coherence
A .--> B is {A} -defined ;
end;

registration
let A, B be set ;
cluster A .--> B -> {A} -defined total for {A} -defined Function;
coherence
for b1 being {A} -defined Function st b1 = A .--> B holds
b1 is total ;
end;

registration
let A be set ;
let B be non empty set ;
cluster A .--> B -> V2() ;
coherence
A .--> B is non-empty ;
end;

theorem Th1: :: CIRCCOMB:1
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 Th2: :: CIRCCOMB:2
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 V2() ManySortedSet of A;
let B be set ;
let f2, g2 be V2() 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
h1 +* h2 is ManySortedFunction of f1 +* f2,g1 +* g2
proof end;
end;

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
for S1 being ManySortedSign holds
( the Arity of S1 tolerates the Arity of S1 & the ResultSort of S1 tolerates the ResultSort of S1 ) ;
symmetry
for S1, S2 being ManySortedSign st the Arity of S1 tolerates the Arity of S2 & the ResultSort of S1 tolerates the ResultSort of S2 holds
( the Arity of S2 tolerates the Arity of S1 & the ResultSort of S2 tolerates the ResultSort of S1 ) ;
end;

:: deftheorem defines tolerates CIRCCOMB:def 1 :
for S1, S2 being ManySortedSign holds
( S1 tolerates S2 iff ( the Arity of S1 tolerates the Arity of S2 & the ResultSort of S1 tolerates the ResultSort of S2 ) );

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 carrier' of it = the carrier' of S1 \/ the carrier' 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
ex b1 being non empty strict ManySortedSign st
( the carrier of b1 = the carrier of S1 \/ the carrier of S2 & the carrier' of b1 = the carrier' of S1 \/ the carrier' of S2 & the Arity of b1 = the Arity of S1 +* the Arity of S2 & the ResultSort of b1 = the ResultSort of S1 +* the ResultSort of S2 )
proof end;
uniqueness
for b1, b2 being non empty strict ManySortedSign st the carrier of b1 = the carrier of S1 \/ the carrier of S2 & the carrier' of b1 = the carrier' of S1 \/ the carrier' of S2 & the Arity of b1 = the Arity of S1 +* the Arity of S2 & the ResultSort of b1 = the ResultSort of S1 +* the ResultSort of S2 & the carrier of b2 = the carrier of S1 \/ the carrier of S2 & the carrier' of b2 = the carrier' of S1 \/ the carrier' of S2 & the Arity of b2 = the Arity of S1 +* the Arity of S2 & the ResultSort of b2 = the ResultSort of S1 +* the ResultSort of S2 holds
b1 = b2 ;
end;

:: deftheorem Def2 defines +* CIRCCOMB:def 2 :
for S1, S2 being non empty ManySortedSign
for b3 being non empty strict ManySortedSign holds
( b3 = S1 +* S2 iff ( the carrier of b3 = the carrier of S1 \/ the carrier of S2 & the carrier' of b3 = the carrier' of S1 \/ the carrier' of S2 & the Arity of b3 = the Arity of S1 +* the Arity of S2 & the ResultSort of b3 = the ResultSort of S1 +* the ResultSort of S2 ) );

theorem Th3: :: CIRCCOMB:3
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 :: CIRCCOMB:4
for S being non empty ManySortedSign holds S +* S = ManySortedSign(# the carrier of S, the carrier' of S, the Arity of S, the ResultSort of S #)
proof end;

theorem Th5: :: CIRCCOMB:5
for S1, S2 being non empty ManySortedSign st S1 tolerates S2 holds
S1 +* S2 = S2 +* S1
proof end;

theorem :: CIRCCOMB:6
for S1, S2, S3 being non empty ManySortedSign holds (S1 +* S2) +* S3 = S1 +* (S2 +* S3)
proof end;

theorem :: CIRCCOMB:7
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:8
for S1, S2 being non empty Circuit-like ManySortedSign st InnerVertices S1 misses InnerVertices S2 holds
S1 +* S2 is Circuit-like
proof end;

theorem Th9: :: CIRCCOMB:9
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:10
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 non void strict ;
coherence
not S1 +* S2 is void by Th9;
cluster S2 +* S1 -> non empty non void strict ;
coherence
not S2 +* S1 is void by Th9;
end;

::theorem
:: for S1,S2 being monotonic (non void ManySortedSign) st
:: InputVertices S1 misses InnerVertices S2 or
:: InputVertices S2 misses InnerVertices S1
:: holds S1+*S2 is monotonic;
theorem Th11: :: CIRCCOMB:11
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 Th12: :: CIRCCOMB:12
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 Th13: :: CIRCCOMB:13
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 Th14: :: CIRCCOMB:14
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 Th15: :: CIRCCOMB:15
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 Th16: :: CIRCCOMB:16
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 Th17: :: CIRCCOMB:17
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;

begin

definition
let S1, S2 be non empty ManySortedSign ;
let A1 be MSAlgebra over S1;
let A2 be MSAlgebra over 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 :
for S1, S2 being non empty ManySortedSign
for A1 being MSAlgebra over S1
for A2 being MSAlgebra over S2 holds
( A1 tolerates A2 iff ( S1 tolerates S2 & the Sorts of A1 tolerates the Sorts of A2 & the Charact of A1 tolerates the Charact of A2 ) );

definition
let S1, S2 be non empty ManySortedSign ;
let A1 be non-empty MSAlgebra over S1;
let A2 be non-empty MSAlgebra over S2;
assume A1: the Sorts of A1 tolerates the Sorts of A2 ;
func A1 +* A2 -> strict non-empty MSAlgebra over 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
for b1, b2 being strict non-empty MSAlgebra over S1 +* S2 st the Sorts of b1 = the Sorts of A1 +* the Sorts of A2 & the Charact of b1 = the Charact of A1 +* the Charact of A2 & the Sorts of b2 = the Sorts of A1 +* the Sorts of A2 & the Charact of b2 = the Charact of A1 +* the Charact of A2 holds
b1 = b2 ;
existence
ex b1 being strict non-empty MSAlgebra over S1 +* S2 st
( the Sorts of b1 = the Sorts of A1 +* the Sorts of A2 & the Charact of b1 = the Charact of A1 +* the Charact of A2 )
proof end;
end;

:: deftheorem Def4 defines +* CIRCCOMB:def 4 :
for S1, S2 being non empty ManySortedSign
for A1 being non-empty MSAlgebra over S1
for A2 being non-empty MSAlgebra over S2 st the Sorts of A1 tolerates the Sorts of A2 holds
for b5 being strict non-empty MSAlgebra over S1 +* S2 holds
( b5 = A1 +* A2 iff ( the Sorts of b5 = the Sorts of A1 +* the Sorts of A2 & the Charact of b5 = the Charact of A1 +* the Charact of A2 ) );

theorem :: CIRCCOMB:18
for S being non empty non void ManySortedSign
for A being MSAlgebra over S holds A tolerates A
proof end;

theorem Th19: :: CIRCCOMB:19
for S1, S2 being non empty non void ManySortedSign
for A1 being MSAlgebra over S1
for A2 being MSAlgebra over S2 st A1 tolerates A2 holds
A2 tolerates A1
proof end;

theorem :: CIRCCOMB:20
for S1, S2, S3 being non empty ManySortedSign
for A1 being non-empty MSAlgebra over S1
for A2 being non-empty MSAlgebra over S2
for A3 being MSAlgebra over S3 st A1 tolerates A2 & A2 tolerates A3 & A3 tolerates A1 holds
A1 +* A2 tolerates A3
proof end;

theorem :: CIRCCOMB:21
for S being non empty strict ManySortedSign
for A being non-empty MSAlgebra over S holds A +* A = MSAlgebra(# the Sorts of A, the Charact of A #)
proof end;

theorem Th22: :: CIRCCOMB:22
for S1, S2 being non empty ManySortedSign
for A1 being non-empty MSAlgebra over S1
for A2 being non-empty MSAlgebra over S2 st A1 tolerates A2 holds
A1 +* A2 = A2 +* A1
proof end;

theorem :: CIRCCOMB:23
for S1, S2, S3 being non empty ManySortedSign
for A1 being non-empty MSAlgebra over S1
for A2 being non-empty MSAlgebra over S2
for A3 being non-empty MSAlgebra over 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:24
for S1, S2 being non empty ManySortedSign
for A1 being non-empty finite-yielding MSAlgebra over S1
for A2 being non-empty finite-yielding MSAlgebra over S2 st the Sorts of A1 tolerates the Sorts of A2 holds
A1 +* A2 is finite-yielding
proof end;

theorem :: CIRCCOMB:25
for S1, S2 being non empty ManySortedSign
for A1 being non-empty MSAlgebra over S1
for s1 being Element of product the Sorts of A1
for A2 being non-empty MSAlgebra over 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:26
for S1, S2 being non empty ManySortedSign
for A1 being non-empty MSAlgebra over S1
for A2 being non-empty MSAlgebra over 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 Th27: :: CIRCCOMB:27
for S1, S2 being non empty non void ManySortedSign
for A1 being non-empty MSAlgebra over S1
for A2 being non-empty MSAlgebra over 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 Th28: :: CIRCCOMB:28
for S1, S2 being non empty non void ManySortedSign
for A1 being non-empty MSAlgebra over S1
for A2 being non-empty MSAlgebra over 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 Th29: :: CIRCCOMB:29
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 Th30: :: CIRCCOMB:30
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 Th31: :: CIRCCOMB:31
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 Th32: :: CIRCCOMB:32
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 Th33: :: CIRCCOMB:33
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:34
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:35
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;

begin

definition
let f be set ;
let p be FinSequence;
let x be set ;
func 1GateCircStr (p,f,x) -> non void strict ManySortedSign means :Def5: :: CIRCCOMB:def 5
( the carrier of it = (rng p) \/ {x} & the carrier' of it = {[p,f]} & the Arity of it . [p,f] = p & the ResultSort of it . [p,f] = x );
existence
ex b1 being non void strict ManySortedSign st
( the carrier of b1 = (rng p) \/ {x} & the carrier' of b1 = {[p,f]} & the Arity of b1 . [p,f] = p & the ResultSort of b1 . [p,f] = x )
proof end;
uniqueness
for b1, b2 being non void strict ManySortedSign st the carrier of b1 = (rng p) \/ {x} & the carrier' of b1 = {[p,f]} & the Arity of b1 . [p,f] = p & the ResultSort of b1 . [p,f] = x & the carrier of b2 = (rng p) \/ {x} & the carrier' of b2 = {[p,f]} & the Arity of b2 . [p,f] = p & the ResultSort of b2 . [p,f] = x holds
b1 = b2
proof end;
end;

:: deftheorem Def5 defines 1GateCircStr CIRCCOMB:def 5 :
for f being set
for p being FinSequence
for x being set
for b4 being non void strict ManySortedSign holds
( b4 = 1GateCircStr (p,f,x) iff ( the carrier of b4 = (rng p) \/ {x} & the carrier' of b4 = {[p,f]} & the Arity of b4 . [p,f] = p & the ResultSort of b4 . [p,f] = x ) );

registration
let f be set ;
let p be FinSequence;
let x be set ;
cluster 1GateCircStr (p,f,x) -> non empty non void strict ;
coherence
not 1GateCircStr (p,f,x) is empty
proof end;
end;

theorem Th36: :: CIRCCOMB:36
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:37
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:38
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) -> non void strict ManySortedSign means :Def6: :: CIRCCOMB:def 6
( the carrier of it = (rng p) \/ {[p,f]} & the carrier' of it = {[p,f]} & the Arity of it . [p,f] = p & the ResultSort of it . [p,f] = [p,f] );
existence
ex b1 being non void strict ManySortedSign st
( the carrier of b1 = (rng p) \/ {[p,f]} & the carrier' of b1 = {[p,f]} & the Arity of b1 . [p,f] = p & the ResultSort of b1 . [p,f] = [p,f] )
proof end;
uniqueness
for b1, b2 being non void strict ManySortedSign st the carrier of b1 = (rng p) \/ {[p,f]} & the carrier' of b1 = {[p,f]} & the Arity of b1 . [p,f] = p & the ResultSort of b1 . [p,f] = [p,f] & the carrier of b2 = (rng p) \/ {[p,f]} & the carrier' of b2 = {[p,f]} & the Arity of b2 . [p,f] = p & the ResultSort of b2 . [p,f] = [p,f] holds
b1 = b2
proof end;
end;

:: deftheorem Def6 defines 1GateCircStr CIRCCOMB:def 6 :
for f being set
for p being FinSequence
for b3 being non void strict ManySortedSign holds
( b3 = 1GateCircStr (p,f) iff ( the carrier of b3 = (rng p) \/ {[p,f]} & the carrier' of b3 = {[p,f]} & the Arity of b3 . [p,f] = p & the ResultSort of b3 . [p,f] = [p,f] ) );

registration
let f be set ;
let p be FinSequence;
cluster 1GateCircStr (p,f) -> non empty non void strict ;
coherence
not 1GateCircStr (p,f) is empty
proof end;
end;

theorem :: CIRCCOMB:39
for f being set
for p being FinSequence holds 1GateCircStr (p,f) = 1GateCircStr (p,f,[p,f])
proof end;

theorem Th40: :: CIRCCOMB:40
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 Th41: :: CIRCCOMB:41
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 Th42: :: CIRCCOMB:42
for f being set
for p being FinSequence holds
( InputVertices (1GateCircStr (p,f)) = rng p & InnerVertices (1GateCircStr (p,f)) = {[p,f]} )
proof end;

theorem Th43: :: CIRCCOMB:43
for f being set
for p, q being FinSequence holds 1GateCircStr (p,f) tolerates 1GateCircStr (q,f)
proof end;

begin

definition
let IT be ManySortedSign ;
attr IT is unsplit means :Def7: :: CIRCCOMB:def 7
 the ResultSort of IT = id the carrier' of IT;
attr IT is gate`1=arity means :Def8: :: CIRCCOMB:def 8
 for g being set st g in the carrier' 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 carrier' 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 :
for IT being ManySortedSign holds
( IT is unsplit iff the ResultSort of IT = id the carrier' of IT );

:: deftheorem Def8 defines gate`1=arity CIRCCOMB:def 8 :
for IT being ManySortedSign holds
( IT is gate`1=arity iff for g being set st g in the carrier' of IT holds
g = [( the Arity of IT . g),(g `2)] );

:: deftheorem Def9 defines gate`2isBoolean CIRCCOMB:def 9 :
for IT being ManySortedSign holds
( IT is gate`2isBoolean iff for g being set st g in the carrier' 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] );

definition
let S be non empty ManySortedSign ;
let IT be MSAlgebra over S;
attr IT is gate`2=den means :Def10: :: CIRCCOMB:def 10
 for g being set st g in the carrier' of S holds
g = [(g `1),( the Charact of IT . g)];
end;

:: deftheorem Def10 defines gate`2=den CIRCCOMB:def 10 :
for S being non empty ManySortedSign
for IT being MSAlgebra over S holds
( IT is gate`2=den iff for g being set st g in the carrier' of S holds
g = [(g `1),( the Charact of IT . g)] );

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

:: deftheorem defines gate`2=den CIRCCOMB:def 11 :
for IT being non empty ManySortedSign holds
( IT is gate`2=den iff ex A being MSAlgebra over IT st A is gate`2=den );

scheme :: CIRCCOMB:sch 1
MSSLambdaWeak{ F1() -> set , F2() -> set , F3() -> Function of F1(),F2(), F4( set , set ) -> set } :
ex f being ManySortedSet of F1() st
for a being set
for b being Element of F2() st a in F1() & b = F3() . a holds
f . a = F4(a,b)
proof end;

scheme :: CIRCCOMB:sch 2
Lemma{ F1() -> non empty ManySortedSign , F2( set , set ) -> set } :
ex A being strict MSAlgebra over F1() st
( the Sorts of A = the carrier of F1() --> BOOLEAN & ( for g being set
for p being Element of the carrier of F1() * st g in the carrier' of F1() & p = the Arity of F1() . g holds
the Charact of A . g = F2(g,p) ) )
provided
A1: for g being set
for p being Element of the carrier of F1() * st g in the carrier' of F1() & p = the Arity of F1() . g holds
F2(g,p) is Function of ((len p) -tuples_on BOOLEAN),BOOLEAN
proof end;

registration
cluster non empty gate`2isBoolean -> non empty gate`2=den for ManySortedSign ;
coherence
for b1 being non empty ManySortedSign st b1 is gate`2isBoolean holds
b1 is gate`2=den
proof end;
end;

theorem Th44: :: CIRCCOMB:44
for S being non empty ManySortedSign holds
( S is unsplit iff for o being set st o in the carrier' of S holds
the ResultSort of S . o = o )
proof end;

theorem :: CIRCCOMB:45
for S being non empty ManySortedSign st S is unsplit holds
the carrier' of S c= the carrier of S
proof end;

registration
cluster non empty unsplit -> non empty Circuit-like for ManySortedSign ;
coherence
for b1 being non empty ManySortedSign st b1 is unsplit holds
b1 is Circuit-like
proof end;
end;

theorem Th46: :: CIRCCOMB:46
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 void strict unsplit gate`1=arity ;
coherence
( 1GateCircStr (p,f) is unsplit & 1GateCircStr (p,f) is gate`1=arity ) by Th46;
end;

registration
cluster non empty non void strict unsplit gate`1=arity for ManySortedSign ;
existence
ex b1 being ManySortedSign st
( b1 is unsplit & b1 is gate`1=arity & not b1 is void & b1 is strict & not b1 is empty )
proof end;
end;

theorem Th47: :: CIRCCOMB:47
for S1, S2 being non empty unsplit gate`1=arity ManySortedSign holds S1 tolerates S2
proof end;

theorem Th48: :: CIRCCOMB:48
for S1, S2 being non empty ManySortedSign
for A1 being MSAlgebra over S1
for A2 being MSAlgebra over 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 Th49: :: CIRCCOMB:49
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 unsplit ;
coherence
S1 +* S2 is unsplit by Th49;
end;

theorem Th50: :: CIRCCOMB:50
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
S1 +* S2 is gate`1=arity by Th50;
end;

theorem Th51: :: CIRCCOMB:51
for S1, S2 being non empty ManySortedSign st S1 is gate`2isBoolean & S2 is gate`2isBoolean holds
S1 +* S2 is gate`2isBoolean
proof end;

begin

definition
let n be Nat;
mode FinSeqLen of n is n -element FinSequence;
end;

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 B1: ( x in rng p implies X = Y ) ;
func 1GateCircuit (p,f,x) -> strict non-empty MSAlgebra over 1GateCircStr (p,f,x) means :: CIRCCOMB:def 12
( the Sorts of it = ((rng p) --> X) +* (x .--> Y) & the Charact of it . [p,f] = f );
existence
ex b1 being strict non-empty MSAlgebra over 1GateCircStr (p,f,x) st
( the Sorts of b1 = ((rng p) --> X) +* (x .--> Y) & the Charact of b1 . [p,f] = f )
proof end;
uniqueness
for b1, b2 being strict non-empty MSAlgebra over 1GateCircStr (p,f,x) st the Sorts of b1 = ((rng p) --> X) +* (x .--> Y) & the Charact of b1 . [p,f] = f & the Sorts of b2 = ((rng p) --> X) +* (x .--> Y) & the Charact of b2 . [p,f] = f holds
b1 = b2
proof end;
end;

:: deftheorem defines 1GateCircuit CIRCCOMB:def 12 :
for n being Nat
for X, Y being non empty set
for f being Function of (n -tuples_on X),Y
for p being FinSeqLen of n
for x being set st ( x in rng p implies X = Y ) holds
for b7 being strict non-empty MSAlgebra over 1GateCircStr (p,f,x) holds
( b7 = 1GateCircuit (p,f,x) iff ( the Sorts of b7 = ((rng p) --> X) +* (x .--> Y) & the Charact of b7 . [p,f] = f ) );

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 over 1GateCircStr (p,f) means :Def13: :: CIRCCOMB:def 13
( the Sorts of it = the carrier of (1GateCircStr (p,f)) --> X & the Charact of it . [p,f] = f );
existence
ex b1 being strict non-empty MSAlgebra over 1GateCircStr (p,f) st
( the Sorts of b1 = the carrier of (1GateCircStr (p,f)) --> X & the Charact of b1 . [p,f] = f )
proof end;
uniqueness
for b1, b2 being strict non-empty MSAlgebra over 1GateCircStr (p,f) st the Sorts of b1 = the carrier of (1GateCircStr (p,f)) --> X & the Charact of b1 . [p,f] = f & the Sorts of b2 = the carrier of (1GateCircStr (p,f)) --> X & the Charact of b2 . [p,f] = f holds
b1 = b2
proof end;
end;

:: deftheorem Def13 defines 1GateCircuit CIRCCOMB:def 13 :
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
for b5 being strict non-empty MSAlgebra over 1GateCircStr (p,f) holds
( b5 = 1GateCircuit (p,f) iff ( the Sorts of b5 = the carrier of (1GateCircStr (p,f)) --> X & the Charact of b5 . [p,f] = f ) );

theorem Th52: :: CIRCCOMB:52
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
1GateCircuit (p,f) is gate`2=den by Th52;
cluster 1GateCircStr (p,f) -> non void strict gate`2=den ;
coherence
1GateCircStr (p,f) is gate`2=den by Th52;
end;

theorem Th53: :: CIRCCOMB:53
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 void strict gate`2isBoolean ;
coherence
1GateCircStr (p,f) is gate`2isBoolean by Th53;
end;

registration
cluster non empty gate`2isBoolean for ManySortedSign ;
existence
ex b1 being ManySortedSign st
( b1 is gate`2isBoolean & not b1 is empty )
proof end;
end;

registration
let S1, S2 be non empty gate`2isBoolean ManySortedSign ;
cluster S1 +* S2 -> non empty strict gate`2isBoolean ;
coherence
S1 +* S2 is gate`2isBoolean by Th51;
end;

theorem Th54: :: CIRCCOMB:54
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 finite-yielding ;
coherence
1GateCircuit (p,f) is finite-yielding
proof end;
end;

theorem :: CIRCCOMB:55
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:56
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;

begin

:: definition
:: redefine func BOOLEAN -> Subset of NAT;
:: coherence by MARGREL1:def 12,ZFMISC_1:38;
:: end;
definition
let S be non empty ManySortedSign ;
let IT be MSAlgebra over S;
attr IT is Boolean means :Def14: :: CIRCCOMB:def 14
 for v being Vertex of S holds the Sorts of IT . v = BOOLEAN ;
end;

:: deftheorem Def14 defines Boolean CIRCCOMB:def 14 :
for S being non empty ManySortedSign
for IT being MSAlgebra over S holds
( IT is Boolean iff for v being Vertex of S holds the Sorts of IT . v = BOOLEAN );

theorem Th57: :: CIRCCOMB:57
for S being non empty ManySortedSign
for A being MSAlgebra over 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 finite-yielding for MSAlgebra over S;
coherence
for b1 being MSAlgebra over S st b1 is Boolean holds
( b1 is non-empty & b1 is finite-yielding )
proof end;
end;

theorem :: CIRCCOMB:58
for S being non empty ManySortedSign
for A being MSAlgebra over S holds
( A is Boolean iff rng the Sorts of A c= {BOOLEAN} )
proof end;

theorem Th59: :: CIRCCOMB:59
for S1, S2 being non empty ManySortedSign
for A1 being MSAlgebra over S1
for A2 being MSAlgebra over S2 st A1 is Boolean & A2 is Boolean holds
the Sorts of A1 tolerates the Sorts of A2
proof end;

theorem Th60: :: CIRCCOMB:60
for S1, S2 being non empty unsplit gate`1=arity ManySortedSign
for A1 being MSAlgebra over S1
for A2 being MSAlgebra over 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 Boolean for MSAlgebra over S;
existence
ex b1 being strict MSAlgebra over S st b1 is Boolean
proof end;
end;

theorem :: CIRCCOMB:61
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 Th62: :: CIRCCOMB:62
for S1, S2 being non empty ManySortedSign
for A1 being Boolean MSAlgebra over S1
for A2 being Boolean MSAlgebra over S2 holds A1 +* A2 is Boolean
proof end;

theorem Th63: :: CIRCCOMB:63
for S1, S2 being non empty ManySortedSign
for A1 being non-empty MSAlgebra over S1
for A2 being non-empty MSAlgebra over 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 non void V65() strict unsplit gate`1=arity gate`2isBoolean gate`2=den for ManySortedSign ;
existence
ex b1 being non empty ManySortedSign st
( b1 is unsplit & b1 is gate`1=arity & b1 is gate`2=den & b1 is gate`2isBoolean & not b1 is void & b1 is strict )
proof end;
end;

registration
let S be non empty gate`2isBoolean ManySortedSign ;
cluster strict gate`2=den Boolean for MSAlgebra over S;
existence
ex b1 being strict MSAlgebra over S st
( b1 is Boolean & b1 is gate`2=den )
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 gate`2=den Boolean ;
coherence
( A1 +* A2 is Boolean & A1 +* A2 is gate`2=den )
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 finite-yielding gate`2=den for MSAlgebra over 1GateCircStr (p,f);
existence
ex b1 being Circuit of 1GateCircStr (p,f) st
( b1 is gate`2=den & b1 is strict & b1 is non-empty )
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 1GateCircuit (p,f) -> strict non-empty gate`2=den ;
coherence
1GateCircuit (p,f) is gate`2=den ;
end;

theorem :: CIRCCOMB:64
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;