:: 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;
clusterf +* g -> A \/ B -defined ;
coherence
 f +* g is A \/ B -defined
proofend;
end;

registration
let A, B be set ;
let f be ManySortedSet of A;
let g be ManySortedSet of B;
clusterf +* 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
proofend;
end;

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

registration
let A, B be set ;
clusterA .--> 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 ;
clusterA .--> 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 #
proofend;

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
proofend;

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 funch1 +* h2 ->  ManySortedFunction of f1 +* f2,g1 +* g2;
coherence
 h1 +* h2 is ManySortedFunction of f1 +* f2,g1 +* g2
proofend;
end;

definition
let S1, S2 be ManySortedSign ;
predS1 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 ;
funcS1 +* 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 )
proofend;
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
proofend;

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 #)
proofend;

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

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

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
proofend;

theorem :: CIRCCOMB:8
for S1, S2 being non empty Circuit-like ManySortedSign st InnerVertices S1 misses InnerVertices S2 holds
S1 +* S2 is Circuit-like
proofend;

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
proofend;

theorem :: CIRCCOMB:10
for S1, S2 being non empty finite ManySortedSign holds S1 +* S2 is finite
proofend;

registration
let S1 be non empty non void ManySortedSign ;
let S2 be non empty ManySortedSign ;
clusterS1 +* S2 ->  non empty non void strict ;
coherence
 not S1 +* S2 is void by Th9;
clusterS2 +* 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) )
proofend;

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
proofend;

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
proofend;

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 )
proofend;

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 )
proofend;

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 )
proofend;

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 )
proofend;

begin

definition
let S1, S2 be non empty ManySortedSign ;
let A1 be MSAlgebra over S1;
let A2 be MSAlgebra over S2;
predA1 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 ;
funcA1 +* 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 )
proofend;
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
proofend;

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
proofend;

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
proofend;

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 #)
proofend;

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
proofend;

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)
proofend;

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
proofend;

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)
proofend;

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 )
proofend;

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)
proofend;

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)
proofend;

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
proofend;

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
proofend;

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 ) )
proofend;

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)
proofend;

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)
proofend;

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)
proofend;

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)
proofend;

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 )
proofend;
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
proofend;
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
proofend;
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 )
proofend;

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 )
proofend;

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} )
proofend;

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] )
proofend;
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
proofend;
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
proofend;
end;

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

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] )
proofend;

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 )
proofend;

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]} )
proofend;

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

begin

definition
let IT be ManySortedSign ;
attrIT is unsplit  means :Def7: :: CIRCCOMB:def 7
 the ResultSort of IT = id the carrier' of IT;
attrIT 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)];
attrIT 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;
attrIT 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 ;
attrIT 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)
proofend;

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
proofend;

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
proofend;
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 )
proofend;

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

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
proofend;
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 )
proofend;

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 )
proofend;
end;

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

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
proofend;

theorem Th49: :: CIRCCOMB:49
for S1, S2 being non empty unsplit ManySortedSign holds S1 +* S2 is unsplit
proofend;

registration
let S1, S2 be non empty unsplit ManySortedSign ;
clusterS1 +* 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
proofend;

registration
let S1, S2 be non empty gate`1=arity ManySortedSign ;
clusterS1 +* 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
proofend;

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 )
proofend;
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
proofend;
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 )
proofend;
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
proofend;
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 )
proofend;

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
proofend;

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 )
proofend;
end;

registration
let S1, S2 be non empty gate`2isBoolean ManySortedSign ;
clusterS1 +* 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 ) )
proofend;

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
proofend;
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)
proofend;

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)
proofend;

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;
attrIT 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 )
proofend;

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 )
proofend;
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} )
proofend;

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
proofend;

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
proofend;

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
proofend;
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
proofend;

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
proofend;

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
proofend;

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 )
proofend;
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 )
proofend;
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;
clusterA1 +* A2 ->  strict non-empty gate`2=den Boolean ;
coherence
 ( A1 +* A2 is Boolean & A1 +* A2 is gate`2=den )
proofend;
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 )
proofend;
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 ) )
proofend;