:: CIRCCOMB semantic presentation

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
proof
A1: dom g = B by PARTFUN1:def_2;
 dom f = A by PARTFUN1:def_2;
then  dom (f +* g) = A \/ B by A1, FUNCT_4:def_1;
hence  f +* g is A \/ B -defined by RELAT_1:def_18; ::_thesis: verum
end;
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
proof
A1: dom g = B by PARTFUN1:def_2;
 dom f = A by PARTFUN1:def_2;
then  dom (f +* g) = A \/ B by A1, FUNCT_4:def_1;
hence  for b1 being A \/ B -defined Function st b1 = f +* g holds
b1 is total by PARTFUN1:def_2; ::_thesis: verum
end;
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 #
proof
let A, B be set ; ::_thesis: for f being ManySortedSet of A
for g being ManySortedSet of B st f c= g holds
f # c= g #
let f be ManySortedSet of A; ::_thesis: for g being ManySortedSet of B st f c= g holds
f # c= g #
let g be ManySortedSet of B; ::_thesis: ( f c= g implies f # c= g # )
assume A1: f c= g ; ::_thesis: f # c= g #
now__::_thesis:_for_z_being_set_st_z_in_f_#_holds_
z_in_g_#
A2: dom f c= dom g by A1, RELAT_1:11;
A3: dom g = B by PARTFUN1:def_2;
A4: dom (g #) = B * by PARTFUN1:def_2;
let z be set ; ::_thesis: ( z in f # implies z in g # )
A5: dom f = A by PARTFUN1:def_2;
assume A6: z in f # ; ::_thesis: z in g #
then consider x, y being set  such that
A7: [x,y] = z by RELAT_1:def_1;
 dom (f #) = A * by PARTFUN1:def_2;
then reconsider x = x as Element of A * by A6, A7, XTUPLE_0:def_12;
A8: rng x c= A by FINSEQ_1:def_4;
 rng x c= A by FINSEQ_1:def_4;
then  rng x c= B by A5, A3, A2, XBOOLE_1:1;
then  x is FinSequence of B by FINSEQ_1:def_4;
then reconsider x9 = x as Element of B * by FINSEQ_1:def_11;
A9: rng x9 c= B by FINSEQ_1:def_4;
y = (f #) . x by A6, A7, FUNCT_1:1
.= product (f * x) by FINSEQ_2:def_5
.= product (g * x9) by A1, A5, A3, A8, A9, PARTFUN1:54, PARTFUN1:79
.= (g #) . x9 by FINSEQ_2:def_5 ;
hence  z in g # by A7, A4, FUNCT_1:1; ::_thesis: verum
end;
hence  f # c= g # by TARSKI:def_3; ::_thesis: verum
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
let X be set ; ::_thesis: for Y being non empty set
for p being FinSequence of X holds ((X --> Y) #) . p = (len p) -tuples_on Y
let Y be non empty set ; ::_thesis: for p being FinSequence of X holds ((X --> Y) #) . p = (len p) -tuples_on Y
let p be FinSequence of X; ::_thesis: ((X --> Y) #) . p = (len p) -tuples_on Y
 rng p c= X by FINSEQ_1:def_4;
then  (rng p) /\ X = rng p by XBOOLE_1:28;
then A1: p " X = p " (rng p) by RELAT_1:133
.= dom p by RELAT_1:134 ;
 p in X * by FINSEQ_1:def_11;
hence ((X --> Y) #) . p = product ((X --> Y) * p) by FINSEQ_2:def_5
.= product ((p " X) --> Y) by FUNCOP_1:19
.= product ((Seg (len p)) --> Y) by A1, FINSEQ_1:def_3
.= (len p) -tuples_on Y by Lm1 ;
::_thesis: verum
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 funch1 +* h2 ->  ManySortedFunction of f1 +* f2,g1 +* g2;
coherence
 h1 +* h2 is ManySortedFunction of f1 +* f2,g1 +* g2
proof
set f = f1 +* f2;
set g = g1 +* g2;
set h = h1 +* h2;
A1: dom g1 = A by PARTFUN1:def_2;
A2: dom f2 = B by PARTFUN1:def_2;
A3: dom g2 = B by PARTFUN1:def_2;
A4: dom h2 = B by PARTFUN1:def_2;
A5: dom h1 = A by PARTFUN1:def_2;
reconsider h = h1 +* h2 as ManySortedFunction of A \/ B ;
A6: dom f1 = A by PARTFUN1:def_2;
 h is ManySortedFunction of f1 +* f2,g1 +* g2
proof
let x be set ; :: according to PBOOLE:def_15 ::_thesis: ( not x in A \/ B or h . x is Element of K19(K20(((f1 +* f2) . x),((g1 +* g2) . x))) )
A7: ( not x in B or x in B ) ;
assume A8: x in A \/ B ; ::_thesis: h . x is Element of K19(K20(((f1 +* f2) . x),((g1 +* g2) . x)))
then  ( x in A or x in B ) by XBOOLE_0:def_3;
then  ( ( h . x = h1 . x & h1 . x is Function of (f1 . x),(g1 . x) & (f1 +* f2) . x = f1 . x & (g1 +* g2) . x = g1 . x ) or ( h . x = h2 . x & h2 . x is Function of (f2 . x),(g2 . x) & (f1 +* f2) . x = f2 . x & (g1 +* g2) . x = g2 . x ) ) by A6, A1, A5, A2, A3, A4, A8, A7, FUNCT_4:def_1, PBOOLE:def_15;
hence  h . x is Element of K19(K20(((f1 +* f2) . x),((g1 +* g2) . x))) ; ::_thesis: verum
end;
hence  h1 +* h2 is ManySortedFunction of f1 +* f2,g1 +* g2 ; ::_thesis: verum
end;
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 )
proof
set RESULT = the ResultSort of S1 +* the ResultSort of S2;
set ARITY = the Arity of S1 +* the Arity of S2;
set OPER = the carrier' of S1 \/ the carrier' of S2;
reconsider CARR = the carrier of S1 \/ the carrier of S2 as non empty set ;
A1: dom the ResultSort of S2 = the carrier' of S2 by FUNCT_2:def_1;
 dom the ResultSort of S1 = the carrier' of S1 by FUNCT_2:def_1;
then A2: dom ( the ResultSort of S1 +* the ResultSort of S2) = the carrier' of S1 \/ the carrier' of S2 by A1, FUNCT_4:def_1;
A3: the carrier of S1 c= CARR by XBOOLE_1:7;
A4: the carrier of S2 c= CARR by XBOOLE_1:7;
 rng the ResultSort of S2 c= the carrier of S2 by RELAT_1:def_19;
then A5: rng the ResultSort of S2 c= CARR by A4, XBOOLE_1:1;
 rng the ResultSort of S1 c= the carrier of S1 by RELAT_1:def_19;
then  rng the ResultSort of S1 c= CARR by A3, XBOOLE_1:1;
then A6: (rng the ResultSort of S1) \/ (rng the ResultSort of S2) c= CARR by A5, XBOOLE_1:8;
 rng ( the ResultSort of S1 +* the ResultSort of S2) c= (rng the ResultSort of S1) \/ (rng the ResultSort of S2) by FUNCT_4:17;
then  rng ( the ResultSort of S1 +* the ResultSort of S2) c= CARR by A6, XBOOLE_1:1;
then reconsider RESULT = the ResultSort of S1 +* the ResultSort of S2 as Function of ( the carrier' of S1 \/ the carrier' of S2),CARR by A2, FUNCT_2:def_1, RELSET_1:4;
A7: dom the Arity of S2 = the carrier' of S2 by FUNCT_2:def_1;
 dom the Arity of S1 = the carrier' of S1 by FUNCT_2:def_1;
then A8: dom ( the Arity of S1 +* the Arity of S2) = the carrier' of S1 \/ the carrier' of S2 by A7, FUNCT_4:def_1;
A9: rng the Arity of S1 c= the carrier of S1 * by RELAT_1:def_19;
A10: rng the Arity of S2 c= the carrier of S2 * by RELAT_1:def_19;
 the carrier of S2 * c= CARR * by FINSEQ_1:62, XBOOLE_1:7;
then A11: rng the Arity of S2 c= CARR * by A10, XBOOLE_1:1;
 the carrier of S1 * c= CARR * by FINSEQ_1:62, XBOOLE_1:7;
then  rng the Arity of S1 c= CARR * by A9, XBOOLE_1:1;
then A12: (rng the Arity of S1) \/ (rng the Arity of S2) c= CARR * by A11, XBOOLE_1:8;
 rng ( the Arity of S1 +* the Arity of S2) c= (rng the Arity of S1) \/ (rng the Arity of S2) by FUNCT_4:17;
then  rng ( the Arity of S1 +* the Arity of S2) c= CARR * by A12, XBOOLE_1:1;
then reconsider ARITY = the Arity of S1 +* the Arity of S2 as Function of ( the carrier' of S1 \/ the carrier' of S2),(CARR *) by A8, FUNCT_2:def_1, RELSET_1:4;
take  ManySortedSign(# CARR,( the carrier' of S1 \/ the carrier' of S2),ARITY,RESULT #) ; ::_thesis: ( the carrier of ManySortedSign(# CARR,( the carrier' of S1 \/ the carrier' of S2),ARITY,RESULT #) = the carrier of S1 \/ the carrier of S2 & the carrier' of ManySortedSign(# CARR,( the carrier' of S1 \/ the carrier' of S2),ARITY,RESULT #) = the carrier' of S1 \/ the carrier' of S2 & the Arity of ManySortedSign(# CARR,( the carrier' of S1 \/ the carrier' of S2),ARITY,RESULT #) = the Arity of S1 +* the Arity of S2 & the ResultSort of ManySortedSign(# CARR,( the carrier' of S1 \/ the carrier' of S2),ARITY,RESULT #) = the ResultSort of S1 +* the ResultSort of S2 )
thus  ( the carrier of ManySortedSign(# CARR,( the carrier' of S1 \/ the carrier' of S2),ARITY,RESULT #) = the carrier of S1 \/ the carrier of S2 & the carrier' of ManySortedSign(# CARR,( the carrier' of S1 \/ the carrier' of S2),ARITY,RESULT #) = the carrier' of S1 \/ the carrier' of S2 & the Arity of ManySortedSign(# CARR,( the carrier' of S1 \/ the carrier' of S2),ARITY,RESULT #) = the Arity of S1 +* the Arity of S2 & the ResultSort of ManySortedSign(# CARR,( the carrier' of S1 \/ the carrier' of S2),ARITY,RESULT #) = the ResultSort of S1 +* the ResultSort of S2 ) ; ::_thesis: verum
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
let S1, S2, S3 be non empty ManySortedSign ; ::_thesis: ( S1 tolerates S2 & S2 tolerates S3 & S3 tolerates S1 implies S1 +* S2 tolerates S3 )
assume that
A1: the Arity of S1 tolerates the Arity of S2 and
A2: the ResultSort of S1 tolerates the ResultSort of S2 and
A3: the Arity of S2 tolerates the Arity of S3 and
A4: the ResultSort of S2 tolerates the ResultSort of S3 and
A5: the Arity of S3 tolerates the Arity of S1 and
A6: the ResultSort of S3 tolerates the ResultSort of S1 ; :: according to CIRCCOMB:def_1 ::_thesis: S1 +* S2 tolerates S3
 the Arity of (S1 +* S2) = the Arity of S1 +* the Arity of S2 by Def2;
hence  the Arity of (S1 +* S2) tolerates the Arity of S3 by A1, A3, A5, FUNCT_4:125; :: according to CIRCCOMB:def_1 ::_thesis: the ResultSort of (S1 +* S2) tolerates the ResultSort of S3
 the ResultSort of (S1 +* S2) = the ResultSort of S1 +* the ResultSort of S2 by Def2;
hence  the ResultSort of (S1 +* S2) tolerates the ResultSort of S3 by A2, A4, A6, FUNCT_4:125; ::_thesis: verum
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
let S be non empty ManySortedSign ; ::_thesis: S +* S = ManySortedSign(# the carrier of S, the carrier' of S, the Arity of S, the ResultSort of S #)
A1: the carrier' of S = the carrier' of S \/ the carrier' of S ;
A2: the Arity of S = the Arity of S +* the Arity of S ;
A3: the ResultSort of S = the ResultSort of S +* the ResultSort of S ;
 the carrier of S = the carrier of S \/ the carrier of S ;
hence  S +* S = ManySortedSign(# the carrier of S, the carrier' of S, the Arity of S, the ResultSort of S #) by A1, A2, A3, Def2; ::_thesis: verum
end;

theorem Th5: :: CIRCCOMB:5
for S1, S2 being non empty ManySortedSign st S1 tolerates S2 holds
S1 +* S2 = S2 +* S1
proof
let S1, S2 be non empty ManySortedSign ; ::_thesis: ( S1 tolerates S2 implies S1 +* S2 = S2 +* S1 )
set S = S1 +* S2;
assume that
A1: the Arity of S1 tolerates the Arity of S2 and
A2: the ResultSort of S1 tolerates the ResultSort of S2 ; :: according to CIRCCOMB:def_1 ::_thesis: S1 +* S2 = S2 +* S1
A3: the carrier' of (S1 +* S2) = the carrier' of S1 \/ the carrier' of S2 by Def2;
 the ResultSort of S1 +* the ResultSort of S2 = the ResultSort of S2 +* the ResultSort of S1 by A2, FUNCT_4:34;
then A4: the ResultSort of (S1 +* S2) = the ResultSort of S2 +* the ResultSort of S1 by Def2;
 the Arity of S1 +* the Arity of S2 = the Arity of S2 +* the Arity of S1 by A1, FUNCT_4:34;
then A5: the Arity of (S1 +* S2) = the Arity of S2 +* the Arity of S1 by Def2;
 the carrier of (S1 +* S2) = the carrier of S1 \/ the carrier of S2 by Def2;
hence  S1 +* S2 = S2 +* S1 by A3, A5, A4, Def2; ::_thesis: verum
end;

theorem :: CIRCCOMB:6
for S1, S2, S3 being non empty ManySortedSign holds (S1 +* S2) +* S3 = S1 +* (S2 +* S3)
proof
let S1, S2, S3 be non empty ManySortedSign ; ::_thesis: (S1 +* S2) +* S3 = S1 +* (S2 +* S3)
set S12 = S1 +* S2;
set S23 = S2 +* S3;
set S1293 = (S1 +* S2) +* S3;
set S1923 = S1 +* (S2 +* S3);
A1: the carrier of (S2 +* S3) = the carrier of S2 \/ the carrier of S3 by Def2;
A2: the carrier of ((S1 +* S2) +* S3) = the carrier of (S1 +* S2) \/ the carrier of S3 by Def2;
A3: the carrier of (S1 +* (S2 +* S3)) = the carrier of S1 \/ the carrier of (S2 +* S3) by Def2;
 the carrier of (S1 +* S2) = the carrier of S1 \/ the carrier of S2 by Def2;
then A4: the carrier of ((S1 +* S2) +* S3) = the carrier of (S1 +* (S2 +* S3)) by A1, A2, A3, XBOOLE_1:4;
A5: the carrier' of (S2 +* S3) = the carrier' of S2 \/ the carrier' of S3 by Def2;
A6: the carrier' of ((S1 +* S2) +* S3) = the carrier' of (S1 +* S2) \/ the carrier' of S3 by Def2;
A7: the Arity of (S2 +* S3) = the Arity of S2 +* the Arity of S3 by Def2;
A8: the Arity of (S1 +* (S2 +* S3)) = the Arity of S1 +* the Arity of (S2 +* S3) by Def2;
A9: the carrier' of (S1 +* (S2 +* S3)) = the carrier' of S1 \/ the carrier' of (S2 +* S3) by Def2;
 the carrier' of (S1 +* S2) = the carrier' of S1 \/ the carrier' of S2 by Def2;
then A10: the carrier' of ((S1 +* S2) +* S3) = the carrier' of (S1 +* (S2 +* S3)) by A5, A6, A9, XBOOLE_1:4;
A11: the ResultSort of (S1 +* (S2 +* S3)) = the ResultSort of S1 +* the ResultSort of (S2 +* S3) by Def2;
A12: the ResultSort of ((S1 +* S2) +* S3) = the ResultSort of (S1 +* S2) +* the ResultSort of S3 by Def2;
A13: the Arity of ((S1 +* S2) +* S3) = the Arity of (S1 +* S2) +* the Arity of S3 by Def2;
 the Arity of (S1 +* S2) = the Arity of S1 +* the Arity of S2 by Def2;
then A14: the Arity of ((S1 +* S2) +* S3) = the Arity of (S1 +* (S2 +* S3)) by A7, A13, A8, FUNCT_4:14;
A15: the ResultSort of (S2 +* S3) = the ResultSort of S2 +* the ResultSort of S3 by Def2;
 the ResultSort of (S1 +* S2) = the ResultSort of S1 +* the ResultSort of S2 by Def2;
hence  (S1 +* S2) +* S3 = S1 +* (S2 +* S3) by A15, A12, A11, A4, A10, A14, FUNCT_4:14; ::_thesis: verum
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
let f be one-to-one Function; ::_thesis: 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
let S1, S2 be non empty Circuit-like ManySortedSign ; ::_thesis: ( the ResultSort of S1 c= f & the ResultSort of S2 c= f implies S1 +* S2 is Circuit-like )
assume that
A1: the ResultSort of S1 c= f and
A2: the ResultSort of S2 c= f ; ::_thesis: S1 +* S2 is Circuit-like
let S be non empty non void ManySortedSign ; :: according to MSAFREE2:def_6 ::_thesis: ( not S = S1 +* S2 or for b1, b2 being Element of the carrier' of S holds
( not the_result_sort_of b1 = the_result_sort_of b2 or b1 = b2 ) )
set r1 = the ResultSort of S1;
set r2 = the ResultSort of S2;
set r = the ResultSort of S;
A3: the ResultSort of S1 +* the ResultSort of S2 c= the ResultSort of S1 \/ the ResultSort of S2 by FUNCT_4:29;
assume  S = S1 +* S2 ; ::_thesis: for b1, b2 being Element of the carrier' of S holds
( not the_result_sort_of b1 = the_result_sort_of b2 or b1 = b2 )
then A4: the ResultSort of S = the ResultSort of S1 +* the ResultSort of S2 by Def2;
 the ResultSort of S1 \/ the ResultSort of S2 c= f by A1, A2, XBOOLE_1:8;
then A5: the ResultSort of S1 +* the ResultSort of S2 c= f by A3, XBOOLE_1:1;
then A6: dom the ResultSort of S c= dom f by A4, GRFUNC_1:2;
let o1, o2 be Gate of S; ::_thesis: ( not the_result_sort_of o1 = the_result_sort_of o2 or o1 = o2 )
A7: dom the ResultSort of S = the carrier' of S by FUNCT_2:def_1;
then A8: o1 in dom the ResultSort of S ;
A9: o2 in dom the ResultSort of S by A7;
assume A10: the_result_sort_of o1 = the_result_sort_of o2 ; ::_thesis: o1 = o2
A11: the ResultSort of S . o2 = f . o2 by A4, A7, A5, GRFUNC_1:2;
 the ResultSort of S . o1 = f . o1 by A4, A7, A5, GRFUNC_1:2;
hence  o1 = o2 by A10, A8, A9, A11, A6, FUNCT_1:def_4; ::_thesis: verum
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
let S1, S2 be non empty Circuit-like ManySortedSign ; ::_thesis: ( InnerVertices S1 misses InnerVertices S2 implies S1 +* S2 is Circuit-like )
assume A1: InnerVertices S1 misses InnerVertices S2 ; ::_thesis: S1 +* S2 is Circuit-like
set r1 = the ResultSort of S1;
set r2 = the ResultSort of S2;
let S be non empty non void ManySortedSign ; :: according to MSAFREE2:def_6 ::_thesis: ( not S = S1 +* S2 or for b1, b2 being Element of the carrier' of S holds
( not the_result_sort_of b1 = the_result_sort_of b2 or b1 = b2 ) )
set r = the ResultSort of S;
A2: dom the ResultSort of S1 = the carrier' of S1 by FUNCT_2:def_1;
assume A3: S = S1 +* S2 ; ::_thesis: for b1, b2 being Element of the carrier' of S holds
( not the_result_sort_of b1 = the_result_sort_of b2 or b1 = b2 )
then A4: the ResultSort of S = the ResultSort of S1 +* the ResultSort of S2 by Def2;
A5: dom the ResultSort of S2 = the carrier' of S2 by FUNCT_2:def_1;
let o1, o2 be Gate of S; ::_thesis: ( not the_result_sort_of o1 = the_result_sort_of o2 or o1 = o2 )
A6: the carrier' of S = the carrier' of S1 \/ the carrier' of S2 by A3, Def2;
then  ( ( not o1 in the carrier' of S2 & o1 in the carrier' of S1 ) or o1 in the carrier' of S2 ) by XBOOLE_0:def_3;
then A7: ( ( the ResultSort of S . o1 = the ResultSort of S1 . o1 & the ResultSort of S1 . o1 in rng the ResultSort of S1 & o1 in the carrier' of S1 ) or ( the ResultSort of S . o1 = the ResultSort of S2 . o1 & the ResultSort of S2 . o1 in rng the ResultSort of S2 & o1 in the carrier' of S2 ) ) by A4, A2, A5, A6, FUNCT_1:def_3, FUNCT_4:def_1;
 ( ( not o2 in the carrier' of S2 & o2 in the carrier' of S1 ) or o2 in the carrier' of S2 ) by A6, XBOOLE_0:def_3;
then A8: ( ( the ResultSort of S . o2 = the ResultSort of S1 . o2 & the ResultSort of S1 . o2 in rng the ResultSort of S1 & o2 in the carrier' of S1 ) or ( the ResultSort of S . o2 = the ResultSort of S2 . o2 & the ResultSort of S2 . o2 in rng the ResultSort of S2 & o2 in the carrier' of S2 ) ) by A4, A2, A5, A6, FUNCT_1:def_3, FUNCT_4:def_1;
assume A9: the_result_sort_of o1 = the_result_sort_of o2 ; ::_thesis: o1 = o2
percases ( ( the ResultSort of S . o1 = the ResultSort of S1 . o1 & o1 in the carrier' of S1 & the ResultSort of S . o2 = the ResultSort of S1 . o2 & o2 in the carrier' of S1 ) or ( the ResultSort of S . o1 = the ResultSort of S2 . o1 & o1 in the carrier' of S2 & the ResultSort of S . o2 = the ResultSort of S2 . o2 & o2 in the carrier' of S2 ) ) by A1, A9, A7, A8, XBOOLE_0:3;
supposeA10: ( the ResultSort of S . o1 = the ResultSort of S1 . o1 & o1 in the carrier' of S1 & the ResultSort of S . o2 = the ResultSort of S1 . o2 & o2 in the carrier' of S1 ) ; ::_thesis: o1 = o2
then reconsider S = S1 as non empty non void Circuit-like ManySortedSign ;
reconsider p1 = o1, p2 = o2 as Gate of S by A10;
A11: the_result_sort_of p2 = the ResultSort of S1 . p2 ;
 the_result_sort_of p1 = the ResultSort of S1 . p1 ;
hence  o1 = o2 by A9, A10, A11, MSAFREE2:def_6; ::_thesis: verum
end;
supposeA12: ( the ResultSort of S . o1 = the ResultSort of S2 . o1 & o1 in the carrier' of S2 & the ResultSort of S . o2 = the ResultSort of S2 . o2 & o2 in the carrier' of S2 ) ; ::_thesis: o1 = o2
then reconsider S = S2 as non empty non void Circuit-like ManySortedSign ;
reconsider p1 = o1, p2 = o2 as Gate of S by A12;
A13: the_result_sort_of p2 = the ResultSort of S2 . p2 ;
 the_result_sort_of p1 = the ResultSort of S2 . p1 ;
hence  o1 = o2 by A9, A12, A13, MSAFREE2:def_6; ::_thesis: verum
end;
end;
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
let S1, S2 be non empty ManySortedSign ; ::_thesis: ( ( not S1 is void or not S2 is void ) implies not S1 +* S2 is void )
assume A1: ( not S1 is void or not S2 is void ) ; ::_thesis: not S1 +* S2 is void
 the carrier' of (S1 +* S2) = the carrier' of S1 \/ the carrier' of S2 by Def2;
hence  not the carrier' of (S1 +* S2) is empty by A1; :: according to STRUCT_0:def_13 ::_thesis: verum
end;

theorem :: CIRCCOMB:10
for S1, S2 being non empty finite ManySortedSign holds S1 +* S2 is finite
proof
let S1, S2 be non empty finite ManySortedSign ; ::_thesis: S1 +* S2 is finite
reconsider C1 = the carrier of S1, C2 = the carrier of S2 as finite set ;
 the carrier of (S1 +* S2) = C1 \/ C2 by Def2;
hence  S1 +* S2 is finite ; ::_thesis: verum
end;

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 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
let S1, S2 be non empty ManySortedSign ; ::_thesis: ( S1 tolerates S2 implies ( InnerVertices (S1 +* S2) = (InnerVertices S1) \/ (InnerVertices S2) & InputVertices (S1 +* S2) c= (InputVertices S1) \/ (InputVertices S2) ) )
set R1 = the ResultSort of S1;
set R2 = the ResultSort of S2;
assume that
 the Arity of S1 tolerates the Arity of S2 and
A1: the ResultSort of S1 tolerates the ResultSort of S2 ; :: according to CIRCCOMB:def_1 ::_thesis: ( InnerVertices (S1 +* S2) = (InnerVertices S1) \/ (InnerVertices S2) & InputVertices (S1 +* S2) c= (InputVertices S1) \/ (InputVertices S2) )
set S = S1 +* S2;
set R = the ResultSort of (S1 +* S2);
A2: the ResultSort of (S1 +* S2) = the ResultSort of S1 +* the ResultSort of S2 by Def2;
then  the ResultSort of S1 c= the ResultSort of (S1 +* S2) by A1, FUNCT_4:28;
then A3: rng the ResultSort of S1 c= rng the ResultSort of (S1 +* S2) by RELAT_1:11;
 rng the ResultSort of S2 c= rng the ResultSort of (S1 +* S2) by A2, FUNCT_4:18;
then A4: (rng the ResultSort of S1) \/ (rng the ResultSort of S2) c= rng the ResultSort of (S1 +* S2) by A3, XBOOLE_1:8;
A5: rng the ResultSort of (S1 +* S2) c= (rng the ResultSort of S1) \/ (rng the ResultSort of S2) by A2, FUNCT_4:17;
hence  InnerVertices (S1 +* S2) = (InnerVertices S1) \/ (InnerVertices S2) by A4, XBOOLE_0:def_10; ::_thesis: InputVertices (S1 +* S2) c= (InputVertices S1) \/ (InputVertices S2)
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in InputVertices (S1 +* S2) or x in (InputVertices S1) \/ (InputVertices S2) )
assume A6: x in InputVertices (S1 +* S2) ; ::_thesis: x in (InputVertices S1) \/ (InputVertices S2)
then A7: not x in rng the ResultSort of (S1 +* S2) by XBOOLE_0:def_5;
A8: rng the ResultSort of (S1 +* S2) = (rng the ResultSort of S1) \/ (rng the ResultSort of S2) by A5, A4, XBOOLE_0:def_10;
then A9: not x in rng the ResultSort of S2 by A7, XBOOLE_0:def_3;
 the carrier of (S1 +* S2) = the carrier of S1 \/ the carrier of S2 by Def2;
then A10: ( x in the carrier of S1 or x in the carrier of S2 ) by A6, XBOOLE_0:def_3;
 not x in rng the ResultSort of S1 by A8, A7, XBOOLE_0:def_3;
then  ( x in the carrier of S1 \ (rng the ResultSort of S1) or x in the carrier of S2 \ (rng the ResultSort of S2) ) by A10, A9, XBOOLE_0:def_5;
hence  x in (InputVertices S1) \/ (InputVertices S2) by XBOOLE_0:def_3; ::_thesis: verum
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
let S1, S2 be non empty ManySortedSign ; ::_thesis: for v2 being Vertex of S2 st v2 in InputVertices (S1 +* S2) holds
v2 in InputVertices S2
set R1 = the ResultSort of S1;
set R2 = the ResultSort of S2;
set S = S1 +* S2;
set R = the ResultSort of (S1 +* S2);
let v2 be Vertex of S2; ::_thesis: ( v2 in InputVertices (S1 +* S2) implies v2 in InputVertices S2 )
 the ResultSort of (S1 +* S2) = the ResultSort of S1 +* the ResultSort of S2 by Def2;
then A1: rng the ResultSort of S2 c= rng the ResultSort of (S1 +* S2) by FUNCT_4:18;
assume  v2 in InputVertices (S1 +* S2) ; ::_thesis: v2 in InputVertices S2
then  not v2 in rng the ResultSort of S2 by A1, XBOOLE_0:def_5;
hence  v2 in InputVertices S2 by XBOOLE_0:def_5; ::_thesis: verum
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
let S1, S2 be non empty ManySortedSign ; ::_thesis: ( S1 tolerates S2 implies for v1 being Vertex of S1 st v1 in InputVertices (S1 +* S2) holds
v1 in InputVertices S1 )
assume that
 the Arity of S1 tolerates the Arity of S2 and
A1: the ResultSort of S1 tolerates the ResultSort of S2 ; :: according to CIRCCOMB:def_1 ::_thesis: for v1 being Vertex of S1 st v1 in InputVertices (S1 +* S2) holds
v1 in InputVertices S1
set S = S1 +* S2;
set R = the ResultSort of (S1 +* S2);
set R1 = the ResultSort of S1;
set R2 = the ResultSort of S2;
 the ResultSort of (S1 +* S2) = the ResultSort of S1 +* the ResultSort of S2 by Def2;
then  the ResultSort of S1 c= the ResultSort of (S1 +* S2) by A1, FUNCT_4:28;
then A2: rng the ResultSort of S1 c= rng the ResultSort of (S1 +* S2) by RELAT_1:11;
let v1 be Vertex of S1; ::_thesis: ( v1 in InputVertices (S1 +* S2) implies v1 in InputVertices S1 )
assume  v1 in InputVertices (S1 +* S2) ; ::_thesis: v1 in InputVertices S1
then  not v1 in rng the ResultSort of S1 by A2, XBOOLE_0:def_5;
hence  v1 in InputVertices S1 by XBOOLE_0:def_5; ::_thesis: verum
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
let S1 be non empty ManySortedSign ; ::_thesis: 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 )
let S2 be non empty non void ManySortedSign ; ::_thesis: 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 )
let o2 be OperSymbol of S2; ::_thesis: 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 )
let o be OperSymbol of (S1 +* S2); ::_thesis: ( o2 = o implies ( the_arity_of o = the_arity_of o2 & the_result_sort_of o = the_result_sort_of o2 ) )
assume A1: o2 = o ; ::_thesis: ( the_arity_of o = the_arity_of o2 & the_result_sort_of o = the_result_sort_of o2 )
A2: dom the Arity of S2 = the carrier' of S2 by FUNCT_2:def_1;
 the Arity of (S1 +* S2) = the Arity of S1 +* the Arity of S2 by Def2;
hence  the_arity_of o = the_arity_of o2 by A1, A2, FUNCT_4:13; ::_thesis: the_result_sort_of o = the_result_sort_of o2
A3: dom the ResultSort of S2 = the carrier' of S2 by FUNCT_2:def_1;
 the ResultSort of (S1 +* S2) = the ResultSort of S1 +* the ResultSort of S2 by Def2;
hence  the_result_sort_of o = the_result_sort_of o2 by A1, A3, FUNCT_4:13; ::_thesis: verum
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
let S1 be non empty ManySortedSign ; ::_thesis: 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 )
let S2, S be non empty non void Circuit-like ManySortedSign ; ::_thesis: ( S = S1 +* S2 implies 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 ) )
assume A1: S = S1 +* S2 ; ::_thesis: 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 )
let v2 be Vertex of S2; ::_thesis: ( v2 in InnerVertices S2 implies for v being Vertex of S st v2 = v holds
( v in InnerVertices S & action_at v = action_at v2 ) )
assume A2: v2 in InnerVertices S2 ; ::_thesis: for v being Vertex of S st v2 = v holds
( v in InnerVertices S & action_at v = action_at v2 )
 the carrier' of S = the carrier' of S1 \/ the carrier' of S2 by A1, Def2;
then reconsider o = action_at v2 as OperSymbol of S by XBOOLE_0:def_3;
let v be Vertex of S; ::_thesis: ( v2 = v implies ( v in InnerVertices S & action_at v = action_at v2 ) )
assume A3: v2 = v ; ::_thesis: ( v in InnerVertices S & action_at v = action_at v2 )
 the ResultSort of S = the ResultSort of S1 +* the ResultSort of S2 by A1, Def2;
then A4: InnerVertices S2 c= InnerVertices S by FUNCT_4:18;
hence  v in InnerVertices S by A2, A3; ::_thesis: action_at v = action_at v2
 the_result_sort_of (action_at v2) = v2 by A2, MSAFREE2:def_7;
then  v = the_result_sort_of o by A1, A3, Th14;
hence  action_at v = action_at v2 by A2, A3, A4, MSAFREE2:def_7; ::_thesis: verum
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
let S1 be non empty non void ManySortedSign ; ::_thesis: 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 )
let S2 be non empty ManySortedSign ; ::_thesis: ( S1 tolerates S2 implies 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 ) )
assume that
A1: the Arity of S1 tolerates the Arity of S2 and
A2: the ResultSort of S1 tolerates the ResultSort of S2 ; :: according to CIRCCOMB:def_1 ::_thesis: 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 )
let o1 be OperSymbol of S1; ::_thesis: 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 )
let o be OperSymbol of (S1 +* S2); ::_thesis: ( o1 = o implies ( the_arity_of o = the_arity_of o1 & the_result_sort_of o = the_result_sort_of o1 ) )
assume A3: o1 = o ; ::_thesis: ( the_arity_of o = the_arity_of o1 & the_result_sort_of o = the_result_sort_of o1 )
A4: dom the Arity of S1 = the carrier' of S1 by FUNCT_2:def_1;
 the Arity of (S1 +* S2) = the Arity of S1 +* the Arity of S2 by Def2;
hence  the_arity_of o = the_arity_of o1 by A1, A3, A4, FUNCT_4:15; ::_thesis: the_result_sort_of o = the_result_sort_of o1
A5: dom the ResultSort of S1 = the carrier' of S1 by FUNCT_2:def_1;
 the ResultSort of (S1 +* S2) = the ResultSort of S1 +* the ResultSort of S2 by Def2;
hence  the_result_sort_of o = the_result_sort_of o1 by A2, A3, A5, FUNCT_4:15; ::_thesis: verum
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
let S1, S be non empty non void Circuit-like ManySortedSign ; ::_thesis: 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 )
let S2 be non empty ManySortedSign ; ::_thesis: ( S1 tolerates S2 & S = S1 +* S2 implies 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 ) )
assume that
A1: S1 tolerates S2 and
A2: S = S1 +* S2 ; ::_thesis: 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 )
let v1 be Vertex of S1; ::_thesis: ( v1 in InnerVertices S1 implies for v being Vertex of S st v1 = v holds
( v in InnerVertices S & action_at v = action_at v1 ) )
assume A3: v1 in InnerVertices S1 ; ::_thesis: for v being Vertex of S st v1 = v holds
( v in InnerVertices S & action_at v = action_at v1 )
let v be Vertex of S; ::_thesis: ( v1 = v implies ( v in InnerVertices S & action_at v = action_at v1 ) )
assume A4: v1 = v ; ::_thesis: ( v in InnerVertices S & action_at v = action_at v1 )
 InnerVertices S = (InnerVertices S1) \/ (InnerVertices S2) by A1, A2, Th11;
hence A5: v in InnerVertices S by A3, A4, XBOOLE_0:def_3; ::_thesis: action_at v = action_at v1
 the carrier' of S = the carrier' of S1 \/ the carrier' of S2 by A2, Def2;
then reconsider o = action_at v1 as OperSymbol of S by XBOOLE_0:def_3;
 the_result_sort_of (action_at v1) = v1 by A3, MSAFREE2:def_7;
then  v = the_result_sort_of o by A1, A2, A4, Th16;
hence  action_at v = action_at v1 by A5, MSAFREE2:def_7; ::_thesis: verum
end;

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 )
proof
set CHARACT = the Charact of A1 +* the Charact of A2;
set SA1 = the Sorts of A1;
set SA2 = the Sorts of A2;
set S = S1 +* S2;
set I = the carrier of (S1 +* S2);
set I1 = the carrier of S1;
set I2 = the carrier of S2;
set SA12 = ( the Sorts of A1 #) +* ( the Sorts of A2 #);
A2: dom ( the Sorts of A2 #) = the carrier of S2 * by PARTFUN1:def_2;
A3: the ResultSort of (S1 +* S2) = the ResultSort of S1 +* the ResultSort of S2 by Def2;
A4: rng the ResultSort of S2 c= the carrier of S2 by RELAT_1:def_19;
A5: dom the Sorts of A2 = the carrier of S2 by PARTFUN1:def_2;
 the carrier of (S1 +* S2) = the carrier of S1 \/ the carrier of S2 by Def2;
then reconsider SORTS = the Sorts of A1 +* the Sorts of A2 as V2() ManySortedSet of the carrier of (S1 +* S2) ;
A6: dom (SORTS #) = the carrier of (S1 +* S2) * by PARTFUN1:def_2;
A7: SORTS = the Sorts of A1 \/ the Sorts of A2 by A1, FUNCT_4:30;
then A8: the Sorts of A2 # c= SORTS # by Th1, XBOOLE_1:7;
A9: dom (( the Sorts of A1 #) +* ( the Sorts of A2 #)) = ( the carrier of S1 *) \/ ( the carrier of S2 *) by PARTFUN1:def_2;
A10: dom the Sorts of A1 = the carrier of S1 by PARTFUN1:def_2;
 rng the ResultSort of S1 c= the carrier of S1 by RELAT_1:def_19;
then A11: ( the Sorts of A1 +* the Sorts of A2) * ( the ResultSort of S1 +* the ResultSort of S2) = ( the Sorts of A1 * the ResultSort of S1) +* ( the Sorts of A2 * the ResultSort of S2) by A1, A10, A5, A4, FUNCT_4:69;
A12: rng the Arity of S2 c= the carrier of S2 * by RELAT_1:def_19;
A13: dom ( the Sorts of A1 #) = the carrier of S1 * by PARTFUN1:def_2;
A14: the Sorts of A1 # tolerates the Sorts of A2 #
proof
let x be set ; :: according to PARTFUN1:def_4 ::_thesis: ( not x in (proj1 ( the Sorts of A1 #)) /\ (proj1 ( the Sorts of A2 #)) or ( the Sorts of A1 #) . x = ( the Sorts of A2 #) . x )
assume A15: x in (dom ( the Sorts of A1 #)) /\ (dom ( the Sorts of A2 #)) ; ::_thesis: ( the Sorts of A1 #) . x = ( the Sorts of A2 #) . x
then reconsider i1 = x as Element of the carrier of S1 * by A13, XBOOLE_0:def_4;
reconsider i2 = x as Element of the carrier of S2 * by A2, A15, XBOOLE_0:def_4;
A16: rng i1 c= the carrier of S1 by FINSEQ_1:def_4;
A17: rng i2 c= the carrier of S2 by FINSEQ_1:def_4;
thus ( the Sorts of A1 #) . x = product ( the Sorts of A1 * i1) by FINSEQ_2:def_5
.= product ( the Sorts of A2 * i2) by A1, A10, A5, A16, A17, PARTFUN1:79
.= ( the Sorts of A2 #) . x by FINSEQ_2:def_5 ; ::_thesis: verum
end;
then A18: ( the Sorts of A1 #) +* ( the Sorts of A2 #) = ( the Sorts of A1 #) \/ ( the Sorts of A2 #) by FUNCT_4:30;
 the Sorts of A1 # c= SORTS # by A7, Th1, XBOOLE_1:7;
then A19: ( the Sorts of A1 #) +* ( the Sorts of A2 #) c= SORTS # by A18, A8, XBOOLE_1:8;
A20: the carrier' of (S1 +* S2) = the carrier' of S1 \/ the carrier' of S2 by Def2;
A21: rng the Arity of (S1 +* S2) c= the carrier of (S1 +* S2) * by RELAT_1:def_19;
A22: rng the Arity of S1 c= the carrier of S1 * by RELAT_1:def_19;
then A23: (rng the Arity of S1) \/ (rng the Arity of S2) c= ( the carrier of S1 *) \/ ( the carrier of S2 *) by A12, XBOOLE_1:13;
A24: the Arity of (S1 +* S2) = the Arity of S1 +* the Arity of S2 by Def2;
then  rng the Arity of (S1 +* S2) c= (rng the Arity of S1) \/ (rng the Arity of S2) by FUNCT_4:17;
then A25: rng the Arity of (S1 +* S2) c= dom (( the Sorts of A1 #) +* ( the Sorts of A2 #)) by A23, A9, XBOOLE_1:1;
A26: ( the Sorts of A1 #) +* ( the Sorts of A2 #) tolerates SORTS # by A19, PARTFUN1:54;
A27: (( the Sorts of A1 #) +* ( the Sorts of A2 #)) * ( the Arity of S1 +* the Arity of S2) = (( the Sorts of A1 #) * the Arity of S1) +* (( the Sorts of A2 #) * the Arity of S2) by A13, A2, A22, A12, A14, FUNCT_4:69;
reconsider CHARACT = the Charact of A1 +* the Charact of A2 as ManySortedFunction of (SORTS #) * the Arity of (S1 +* S2),SORTS * the ResultSort of (S1 +* S2) by A20, A24, A3, A6, A21, A25, A11, A26, A27, PARTFUN1:79;
reconsider A = MSAlgebra(# SORTS,CHARACT #) as strict non-empty MSAlgebra over S1 +* S2 by MSUALG_1:def_3;
take  A ; ::_thesis: ( the Sorts of A = the Sorts of A1 +* the Sorts of A2 & the Charact of A = the Charact of A1 +* the Charact of A2 )
thus  ( the Sorts of A = the Sorts of A1 +* the Sorts of A2 & the Charact of A = the Charact of A1 +* the Charact of A2 ) ; ::_thesis: verum
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
let S be non empty non void ManySortedSign ; ::_thesis: for A being MSAlgebra over S holds A tolerates A
let A be MSAlgebra over S; ::_thesis: A tolerates A
thus  S tolerates S ; :: according to CIRCCOMB:def_3 ::_thesis: ( the Sorts of A tolerates the Sorts of A & the Charact of A tolerates the Charact of A )
thus  ( the Sorts of A tolerates the Sorts of A & the Charact of A tolerates the Charact of A ) ; ::_thesis: verum
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
let S1, S2 be non empty non void ManySortedSign ; ::_thesis: for A1 being MSAlgebra over S1
for A2 being MSAlgebra over S2 st A1 tolerates A2 holds
A2 tolerates A1
let A1 be MSAlgebra over S1; ::_thesis: for A2 being MSAlgebra over S2 st A1 tolerates A2 holds
A2 tolerates A1
let A2 be MSAlgebra over S2; ::_thesis: ( A1 tolerates A2 implies A2 tolerates A1 )
assume that
A1: S1 tolerates S2 and
A2: the Sorts of A1 tolerates the Sorts of A2 and
A3: the Charact of A1 tolerates the Charact of A2 ; :: according to CIRCCOMB:def_3 ::_thesis: A2 tolerates A1
thus  ( S2 tolerates S1 & the Sorts of A2 tolerates the Sorts of A1 & the Charact of A2 tolerates the Charact of A1 ) by A1, A2, A3; :: according to CIRCCOMB:def_3 ::_thesis: verum
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
let S1, S2, S3 be non empty ManySortedSign ; ::_thesis: 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
let A1 be non-empty MSAlgebra over S1; ::_thesis: 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
let A2 be non-empty MSAlgebra over S2; ::_thesis: for A3 being MSAlgebra over S3 st A1 tolerates A2 & A2 tolerates A3 & A3 tolerates A1 holds
A1 +* A2 tolerates A3
let A3 be MSAlgebra over S3; ::_thesis: ( A1 tolerates A2 & A2 tolerates A3 & A3 tolerates A1 implies A1 +* A2 tolerates A3 )
assume that
A1: S1 tolerates S2 and
A2: the Sorts of A1 tolerates the Sorts of A2 and
A3: the Charact of A1 tolerates the Charact of A2 and
A4: S2 tolerates S3 and
A5: the Sorts of A2 tolerates the Sorts of A3 and
A6: the Charact of A2 tolerates the Charact of A3 and
A7: S3 tolerates S1 and
A8: the Sorts of A3 tolerates the Sorts of A1 and
A9: the Charact of A3 tolerates the Charact of A1 ; :: according to CIRCCOMB:def_3 ::_thesis: A1 +* A2 tolerates A3
thus  S1 +* S2 tolerates S3 by A1, A4, A7, Th3; :: according to CIRCCOMB:def_3 ::_thesis: ( the Sorts of (A1 +* A2) tolerates the Sorts of A3 & the Charact of (A1 +* A2) tolerates the Charact of A3 )
 the Sorts of (A1 +* A2) = the Sorts of A1 +* the Sorts of A2 by A2, Def4;
hence  the Sorts of (A1 +* A2) tolerates the Sorts of A3 by A2, A5, A8, FUNCT_4:125; ::_thesis: the Charact of (A1 +* A2) tolerates the Charact of A3
 the Charact of (A1 +* A2) = the Charact of A1 +* the Charact of A2 by A2, Def4;
hence  the Charact of (A1 +* A2) tolerates the Charact of A3 by A3, A6, A9, FUNCT_4:125; ::_thesis: verum
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
let S be non empty strict ManySortedSign ; ::_thesis: for A being non-empty MSAlgebra over S holds A +* A = MSAlgebra(# the Sorts of A, the Charact of A #)
let A be non-empty MSAlgebra over S; ::_thesis: A +* A = MSAlgebra(# the Sorts of A, the Charact of A #)
set A9 = MSAlgebra(# the Sorts of A, the Charact of A #);
set SA = the Sorts of MSAlgebra(# the Sorts of A, the Charact of A #);
set CA = the Charact of MSAlgebra(# the Sorts of A, the Charact of A #);
set SAA = the Sorts of (A +* A);
set CAA = the Charact of (A +* A);
 the Charact of MSAlgebra(# the Sorts of A, the Charact of A #) = the Charact of MSAlgebra(# the Sorts of A, the Charact of A #) +* the Charact of MSAlgebra(# the Sorts of A, the Charact of A #) ;
then A1: the Charact of (A +* A) = the Charact of MSAlgebra(# the Sorts of A, the Charact of A #) by Def4;
 the Sorts of MSAlgebra(# the Sorts of A, the Charact of A #) = the Sorts of MSAlgebra(# the Sorts of A, the Charact of A #) +* the Sorts of MSAlgebra(# the Sorts of A, the Charact of A #) ;
then  the Sorts of (A +* A) = the Sorts of MSAlgebra(# the Sorts of A, the Charact of A #) by Def4;
hence  A +* A = MSAlgebra(# the Sorts of A, the Charact of A #) by A1; ::_thesis: verum
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
let S1, S2 be non empty ManySortedSign ; ::_thesis: 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
let A1 be non-empty MSAlgebra over S1; ::_thesis: for A2 being non-empty MSAlgebra over S2 st A1 tolerates A2 holds
A1 +* A2 = A2 +* A1
let A2 be non-empty MSAlgebra over S2; ::_thesis: ( A1 tolerates A2 implies A1 +* A2 = A2 +* A1 )
set A = A1 +* A2;
assume that
A1: S1 tolerates S2 and
A2: the Sorts of A1 tolerates the Sorts of A2 and
A3: the Charact of A1 tolerates the Charact of A2 ; :: according to CIRCCOMB:def_3 ::_thesis: A1 +* A2 = A2 +* A1
 the Sorts of A1 +* the Sorts of A2 = the Sorts of A2 +* the Sorts of A1 by A2, FUNCT_4:34;
then A4: the Sorts of (A1 +* A2) = the Sorts of A2 +* the Sorts of A1 by A2, Def4;
 the Charact of A1 +* the Charact of A2 = the Charact of A2 +* the Charact of A1 by A3, FUNCT_4:34;
then A5: the Charact of (A1 +* A2) = the Charact of A2 +* the Charact of A1 by A2, Def4;
 S1 +* S2 = S2 +* S1 by A1, Th5;
hence  A1 +* A2 = A2 +* A1 by A2, A4, A5, Def4; ::_thesis: verum
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
let S1, S2, S3 be non empty ManySortedSign ; ::_thesis: 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)
let A1 be non-empty MSAlgebra over S1; ::_thesis: 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)
let A2 be non-empty MSAlgebra over S2; ::_thesis: 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)
let A3 be non-empty MSAlgebra over S3; ::_thesis: ( 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 implies (A1 +* A2) +* A3 = A1 +* (A2 +* A3) )
assume that
A1: the Sorts of A1 tolerates the Sorts of A2 and
A2: the Sorts of A2 tolerates the Sorts of A3 and
A3: the Sorts of A3 tolerates the Sorts of A1 ; ::_thesis: (A1 +* A2) +* A3 = A1 +* (A2 +* A3)
set A12 = A1 +* A2;
set A23 = A2 +* A3;
A4: the Charact of (A1 +* A2) = the Charact of A1 +* the Charact of A2 by A1, Def4;
set A1293 = (A1 +* A2) +* A3;
set A1923 = A1 +* (A2 +* A3);
set s1 = the Sorts of A1;
set s2 = the Sorts of A2;
set s3 = the Sorts of A3;
A5: the Sorts of (A2 +* A3) = the Sorts of A2 +* the Sorts of A3 by A2, Def4;
A6: the Sorts of A1 tolerates the Sorts of (A2 +* A3)
proof
let x be set ; :: according to PARTFUN1:def_4 ::_thesis: ( not x in (proj1 the Sorts of A1) /\ (proj1 the Sorts of (A2 +* A3)) or the Sorts of A1 . x = the Sorts of (A2 +* A3) . x )
assume A7: x in (dom the Sorts of A1) /\ (dom the Sorts of (A2 +* A3)) ; ::_thesis: the Sorts of A1 . x = the Sorts of (A2 +* A3) . x
then  x in dom the Sorts of (A2 +* A3) by XBOOLE_0:def_4;
then A8: ( x in dom the Sorts of A2 or x in dom the Sorts of A3 ) by A5, FUNCT_4:12;
 x in dom the Sorts of A1 by A7, XBOOLE_0:def_4;
then  ( ( x in (dom the Sorts of A1) /\ (dom the Sorts of A2) & ( the Sorts of A2 +* the Sorts of A3) . x = the Sorts of A2 . x ) or ( x in (dom the Sorts of A3) /\ (dom the Sorts of A1) & ( the Sorts of A2 +* the Sorts of A3) . x = the Sorts of A3 . x ) ) by A2, A8, FUNCT_4:13, FUNCT_4:15, XBOOLE_0:def_4;
hence  the Sorts of A1 . x = the Sorts of (A2 +* A3) . x by A1, A3, A5, PARTFUN1:def_4; ::_thesis: verum
end;
then A9: the Sorts of (A1 +* (A2 +* A3)) = the Sorts of A1 +* the Sorts of (A2 +* A3) by Def4;
A10: the Charact of (A2 +* A3) = the Charact of A2 +* the Charact of A3 by A2, Def4;
A11: the Charact of (A1 +* (A2 +* A3)) = the Charact of A1 +* the Charact of (A2 +* A3) by A6, Def4;
A12: the Sorts of (A1 +* A2) = the Sorts of A1 +* the Sorts of A2 by A1, Def4;
A13: the Sorts of (A1 +* A2) tolerates the Sorts of A3
proof
let x be set ; :: according to PARTFUN1:def_4 ::_thesis: ( not x in (proj1 the Sorts of (A1 +* A2)) /\ (proj1 the Sorts of A3) or the Sorts of (A1 +* A2) . x = the Sorts of A3 . x )
assume A14: x in (dom the Sorts of (A1 +* A2)) /\ (dom the Sorts of A3) ; ::_thesis: the Sorts of (A1 +* A2) . x = the Sorts of A3 . x
then  x in dom the Sorts of (A1 +* A2) by XBOOLE_0:def_4;
then A15: ( x in dom the Sorts of A1 or x in dom the Sorts of A2 ) by A12, FUNCT_4:12;
 x in dom the Sorts of A3 by A14, XBOOLE_0:def_4;
then  ( ( x in (dom the Sorts of A3) /\ (dom the Sorts of A1) & ( the Sorts of A1 +* the Sorts of A2) . x = the Sorts of A1 . x ) or ( x in (dom the Sorts of A2) /\ (dom the Sorts of A3) & ( the Sorts of A1 +* the Sorts of A2) . x = the Sorts of A2 . x ) ) by A1, A15, FUNCT_4:13, FUNCT_4:15, XBOOLE_0:def_4;
hence  the Sorts of (A1 +* A2) . x = the Sorts of A3 . x by A2, A3, A12, PARTFUN1:def_4; ::_thesis: verum
end;
then  the Charact of ((A1 +* A2) +* A3) = the Charact of (A1 +* A2) +* the Charact of A3 by Def4;
then A16: the Charact of ((A1 +* A2) +* A3) = the Charact of (A1 +* (A2 +* A3)) by A4, A10, A11, FUNCT_4:14;
 the Sorts of ((A1 +* A2) +* A3) = the Sorts of (A1 +* A2) +* the Sorts of A3 by A13, Def4;
then  the Sorts of ((A1 +* A2) +* A3) = the Sorts of (A1 +* (A2 +* A3)) by A12, A5, A9, FUNCT_4:14;
hence  (A1 +* A2) +* A3 = A1 +* (A2 +* A3) by A16; ::_thesis: verum
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
let S1, S2 be non empty ManySortedSign ; ::_thesis: 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
let A1 be non-empty finite-yielding MSAlgebra over S1; ::_thesis: 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
let A2 be non-empty finite-yielding MSAlgebra over S2; ::_thesis: ( the Sorts of A1 tolerates the Sorts of A2 implies A1 +* A2 is finite-yielding )
assume A1: the Sorts of A1 tolerates the Sorts of A2 ; ::_thesis: A1 +* A2 is finite-yielding
let x be set ; :: according to FINSET_1:def_5,MSAFREE2:def_11 ::_thesis: ( not x in the carrier of (S1 +* S2) or the Sorts of (A1 +* A2) . x is finite )
set A = A1 +* A2;
set SA = the Sorts of (A1 +* A2);
set SA1 = the Sorts of A1;
set SA2 = the Sorts of A2;
A2: dom the Sorts of A1 = the carrier of S1 by PARTFUN1:def_2;
A3: the Sorts of A1 is V31() by MSAFREE2:def_11;
assume  x in the carrier of (S1 +* S2) ; ::_thesis: the Sorts of (A1 +* A2) . x is finite
then reconsider x = x as Vertex of (S1 +* S2) ;
A4: dom the Sorts of A2 = the carrier of S2 by PARTFUN1:def_2;
 the carrier of (S1 +* S2) = the carrier of S1 \/ the carrier of S2 by Def2;
then A5: ( x in the carrier of S1 or x in the carrier of S2 ) by XBOOLE_0:def_3;
A6: the Sorts of A2 is V31() by MSAFREE2:def_11;
 the Sorts of (A1 +* A2) = the Sorts of A1 +* the Sorts of A2 by A1, Def4;
then  ( ( the Sorts of (A1 +* A2) . x = the Sorts of A1 . x & the Sorts of A1 . x is finite ) or ( the Sorts of (A1 +* A2) . x = the Sorts of A2 . x & the Sorts of A2 . x is finite ) ) by A1, A2, A4, A5, A3, A6, FUNCT_4:13, FUNCT_4:15;
hence  the Sorts of (A1 +* A2) . x is finite ; ::_thesis: verum
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
let S1, S2 be non empty ManySortedSign ; ::_thesis: 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)
let A1 be non-empty MSAlgebra over S1; ::_thesis: 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)
let s1 be Element of product the Sorts of A1; ::_thesis: 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)
let A2 be non-empty MSAlgebra over S2; ::_thesis: 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)
let s2 be Element of product the Sorts of A2; ::_thesis: ( the Sorts of A1 tolerates the Sorts of A2 implies s1 +* s2 in product the Sorts of (A1 +* A2) )
assume  the Sorts of A1 tolerates the Sorts of A2 ; ::_thesis: s1 +* s2 in product the Sorts of (A1 +* A2)
then  the Sorts of (A1 +* A2) = the Sorts of A1 +* the Sorts of A2 by Def4;
hence  s1 +* s2 in product the Sorts of (A1 +* A2) by CARD_3:97; ::_thesis: verum
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
let S1, S2 be non empty ManySortedSign ; ::_thesis: 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 )
let A1 be non-empty MSAlgebra over S1; ::_thesis: 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 )
let A2 be non-empty MSAlgebra over S2; ::_thesis: ( the Sorts of A1 tolerates the Sorts of A2 implies 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 ) )
A1: dom the Sorts of A1 = the carrier of S1 by PARTFUN1:def_2;
A2: dom the Sorts of A2 = the carrier of S2 by PARTFUN1:def_2;
assume A3: the Sorts of A1 tolerates the Sorts of A2 ; ::_thesis: 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 )
then  the Sorts of (A1 +* A2) = the Sorts of A1 +* the Sorts of A2 by Def4;
hence  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 ) by A3, A1, A2, CARD_3:98, CARD_3:99; ::_thesis: verum
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
let S1, S2 be non empty non void ManySortedSign ; ::_thesis: 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)
let A1 be non-empty MSAlgebra over S1; ::_thesis: 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)
let A2 be non-empty MSAlgebra over S2; ::_thesis: ( the Sorts of A1 tolerates the Sorts of A2 implies for o being OperSymbol of (S1 +* S2)
for o2 being OperSymbol of S2 st o = o2 holds
Den (o,(A1 +* A2)) = Den (o2,A2) )
A1: dom the Charact of A2 = the carrier' of S2 by PARTFUN1:def_2;
assume  the Sorts of A1 tolerates the Sorts of A2 ; ::_thesis: for o being OperSymbol of (S1 +* S2)
for o2 being OperSymbol of S2 st o = o2 holds
Den (o,(A1 +* A2)) = Den (o2,A2)
then A2: the Charact of (A1 +* A2) = the Charact of A1 +* the Charact of A2 by Def4;
let o be OperSymbol of (S1 +* S2); ::_thesis: for o2 being OperSymbol of S2 st o = o2 holds
Den (o,(A1 +* A2)) = Den (o2,A2)
let o2 be OperSymbol of S2; ::_thesis: ( o = o2 implies Den (o,(A1 +* A2)) = Den (o2,A2) )
assume  o = o2 ; ::_thesis: Den (o,(A1 +* A2)) = Den (o2,A2)
hence  Den (o,(A1 +* A2)) = Den (o2,A2) by A2, A1, FUNCT_4:13; ::_thesis: verum
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
let S1, S2 be non empty non void ManySortedSign ; ::_thesis: 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)
let A1 be non-empty MSAlgebra over S1; ::_thesis: 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)
let A2 be non-empty MSAlgebra over S2; ::_thesis: ( the Sorts of A1 tolerates the Sorts of A2 & the Charact of A1 tolerates the Charact of A2 implies for o being OperSymbol of (S1 +* S2)
for o1 being OperSymbol of S1 st o = o1 holds
Den (o,(A1 +* A2)) = Den (o1,A1) )
A1: dom the Charact of A1 = the carrier' of S1 by PARTFUN1:def_2;
assume  the Sorts of A1 tolerates the Sorts of A2 ; ::_thesis: ( not the Charact of A1 tolerates the Charact of A2 or for o being OperSymbol of (S1 +* S2)
for o1 being OperSymbol of S1 st o = o1 holds
Den (o,(A1 +* A2)) = Den (o1,A1) )
then A2: the Charact of (A1 +* A2) = the Charact of A1 +* the Charact of A2 by Def4;
assume A3: the Charact of A1 tolerates the Charact of A2 ; ::_thesis: for o being OperSymbol of (S1 +* S2)
for o1 being OperSymbol of S1 st o = o1 holds
Den (o,(A1 +* A2)) = Den (o1,A1)
let o be OperSymbol of (S1 +* S2); ::_thesis: for o1 being OperSymbol of S1 st o = o1 holds
Den (o,(A1 +* A2)) = Den (o1,A1)
let o1 be OperSymbol of S1; ::_thesis: ( o = o1 implies Den (o,(A1 +* A2)) = Den (o1,A1) )
assume  o = o1 ; ::_thesis: Den (o,(A1 +* A2)) = Den (o1,A1)
hence  Den (o,(A1 +* A2)) = Den (o1,A1) by A2, A3, A1, FUNCT_4:15; ::_thesis: verum
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
let S1, S2, S be non empty non void Circuit-like ManySortedSign ; ::_thesis: ( S = S1 +* S2 implies 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 )
assume A1: S = S1 +* S2 ; ::_thesis: 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
let A1 be non-empty Circuit of S1; ::_thesis: 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
let A2 be non-empty Circuit of S2; ::_thesis: 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
let A be non-empty Circuit of S; ::_thesis: 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
let s be State of A; ::_thesis: 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
let s2 be State of A2; ::_thesis: ( s2 = s | the carrier of S2 implies 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 )
assume A2: s2 = s | the carrier of S2 ; ::_thesis: 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
let o be OperSymbol of S; ::_thesis: for g2 being Gate of S2 st o = g2 holds
o depends_on_in s = g2 depends_on_in s2
let o2 be OperSymbol of S2; ::_thesis: ( o = o2 implies o depends_on_in s = o2 depends_on_in s2 )
assume A3: o = o2 ; ::_thesis: o depends_on_in s = o2 depends_on_in s2
A4: the carrier of S2 |` (the_arity_of o2) = the_arity_of o2 ;
thus o depends_on_in s = s * (the_arity_of o) by CIRCUIT1:def_3
.= s * (the_arity_of o2) by A1, A3, Th14
.= s2 * (the_arity_of o2) by A2, A4, MONOID_1:1
.= o2 depends_on_in s2 by CIRCUIT1:def_3 ; ::_thesis: verum
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
let S1, S2, S be non empty non void Circuit-like ManySortedSign ; ::_thesis: ( S = S1 +* S2 & S1 tolerates S2 implies 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 )
assume that
A1: S = S1 +* S2 and
A2: S1 tolerates S2 ; ::_thesis: 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
let A1 be non-empty Circuit of S1; ::_thesis: 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
let A2 be non-empty Circuit of S2; ::_thesis: 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
let A be non-empty Circuit of S; ::_thesis: 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
let s be State of A; ::_thesis: 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
let s1 be State of A1; ::_thesis: ( s1 = s | the carrier of S1 implies 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 )
assume A3: s1 = s | the carrier of S1 ; ::_thesis: 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
let o be Gate of S; ::_thesis: for g1 being Gate of S1 st o = g1 holds
o depends_on_in s = g1 depends_on_in s1
let o1 be Gate of S1; ::_thesis: ( o = o1 implies o depends_on_in s = o1 depends_on_in s1 )
assume A4: o = o1 ; ::_thesis: o depends_on_in s = o1 depends_on_in s1
A5: the carrier of S1 |` (the_arity_of o1) = the_arity_of o1 ;
thus o depends_on_in s = s * (the_arity_of o) by CIRCUIT1:def_3
.= s * (the_arity_of o1) by A1, A2, A4, Th16
.= s1 * (the_arity_of o1) by A3, A5, MONOID_1:1
.= o1 depends_on_in s1 by CIRCUIT1:def_3 ; ::_thesis: verum
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
let S1, S2, S be non empty non void Circuit-like ManySortedSign ; ::_thesis: ( S = S1 +* S2 implies 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 ) ) )
assume A1: S = S1 +* S2 ; ::_thesis: 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 ) )
let A1 be non-empty Circuit of S1; ::_thesis: 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 ) )
let A2 be non-empty Circuit of S2; ::_thesis: 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 ) )
let A be non-empty Circuit of S; ::_thesis: ( A1 tolerates A2 & A = A1 +* A2 implies 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 ) ) )
assume that
A2: S1 tolerates S2 and
A3: the Sorts of A1 tolerates the Sorts of A2 and
A4: the Charact of A1 tolerates the Charact of A2 and
A5: A = A1 +* A2 ; :: according to CIRCCOMB:def_3 ::_thesis: 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 ) )
let s be State of A; ::_thesis: 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 ) )
let v be Vertex of S; ::_thesis: ( ( 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 ) )
hereby  ::_thesis: 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
let s1 be State of A1; ::_thesis: ( s1 = s | the carrier of S1 & ( v in InnerVertices S1 or ( v in the carrier of S1 & v in InputVertices S ) ) implies (Following s) . v = (Following s1) . v )
assume A6: s1 = s | the carrier of S1 ; ::_thesis: ( ( v in InnerVertices S1 or ( v in the carrier of S1 & v in InputVertices S ) ) implies (Following s) . v = (Following s1) . v )
A7: now__::_thesis:_(_v_in_InnerVertices_S1_implies_(Following_s)_._v_=_(Following_s1)_._v_)
assume  v in InnerVertices S1 ; ::_thesis: (Following s) . v = (Following s1) . v
then reconsider v1 = v as Element of InnerVertices S1 ;
A8: (Following s1) . v1 = (Den ((action_at v1),A1)) . ((action_at v1) depends_on_in s1) by CIRCUIT2:def_5;
 v1 in InnerVertices S by A1, A2, Th17;
then A9: (Following s) . v = (Den ((action_at v),A)) . ((action_at v) depends_on_in s) by CIRCUIT2:def_5;
A10: action_at v = action_at v1 by A1, A2, Th17;
then  Den ((action_at v1),A1) = Den ((action_at v),A) by A1, A3, A4, A5, Th28;
hence  (Following s) . v = (Following s1) . v by A1, A2, A6, A10, A9, A8, Th30; ::_thesis: verum
end;
now__::_thesis:_(_v_in_the_carrier_of_S1_&_v_in_InputVertices_S_implies_(Following_s)_._v_=_(Following_s1)_._v_)
assume that
A11: v in the carrier of S1 and
A12: v in InputVertices S ; ::_thesis: (Following s) . v = (Following s1) . v
reconsider v1 = v as Vertex of S1 by A11;
 v1 in InputVertices S1 by A1, A2, A12, Th13;
then A13: (Following s1) . v1 = s1 . v1 by CIRCUIT2:def_5;
A14: dom s1 = the carrier of S1 by CIRCUIT1:3;
 (Following s) . v = s . v by A12, CIRCUIT2:def_5;
hence  (Following s) . v = (Following s1) . v by A6, A13, A14, FUNCT_1:47; ::_thesis: verum
end;
hence  ( ( v in InnerVertices S1 or ( v in the carrier of S1 & v in InputVertices S ) ) implies (Following s) . v = (Following s1) . v ) by A7; ::_thesis: verum
end;
let s2 be State of A2; ::_thesis: ( s2 = s | the carrier of S2 & ( v in InnerVertices S2 or ( v in the carrier of S2 & v in InputVertices S ) ) implies (Following s) . v = (Following s2) . v )
assume A15: s2 = s | the carrier of S2 ; ::_thesis: ( ( not v in InnerVertices S2 & not ( v in the carrier of S2 & v in InputVertices S ) ) or (Following s) . v = (Following s2) . v )
A16: now__::_thesis:_(_v_in_InnerVertices_S2_implies_(Following_s)_._v_=_(Following_s2)_._v_)
assume  v in InnerVertices S2 ; ::_thesis: (Following s) . v = (Following s2) . v
then reconsider v2 = v as Element of InnerVertices S2 ;
A17: (Following s2) . v2 = (Den ((action_at v2),A2)) . ((action_at v2) depends_on_in s2) by CIRCUIT2:def_5;
 v2 in InnerVertices S by A1, Th15;
then A18: (Following s) . v = (Den ((action_at v),A)) . ((action_at v) depends_on_in s) by CIRCUIT2:def_5;
A19: action_at v = action_at v2 by A1, Th15;
then  Den ((action_at v2),A2) = Den ((action_at v),A) by A1, A3, A5, Th27;
hence  (Following s) . v = (Following s2) . v by A1, A15, A19, A18, A17, Th29; ::_thesis: verum
end;
now__::_thesis:_(_v_in_the_carrier_of_S2_&_v_in_InputVertices_S_implies_(Following_s)_._v_=_(Following_s2)_._v_)
assume that
A20: v in the carrier of S2 and
A21: v in InputVertices S ; ::_thesis: (Following s) . v = (Following s2) . v
reconsider v2 = v as Vertex of S2 by A20;
 v2 in InputVertices S2 by A1, A21, Th12;
then A22: (Following s2) . v2 = s2 . v2 by CIRCUIT2:def_5;
A23: dom s2 = the carrier of S2 by CIRCUIT1:3;
 (Following s) . v = s . v by A21, CIRCUIT2:def_5;
hence  (Following s) . v = (Following s2) . v by A15, A22, A23, FUNCT_1:47; ::_thesis: verum
end;
hence  ( ( not v in InnerVertices S2 & not ( v in the carrier of S2 & v in InputVertices S ) ) or (Following s) . v = (Following s2) . v ) by A16; ::_thesis: verum
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
let S1, S2, S be non empty non void Circuit-like ManySortedSign ; ::_thesis: ( InnerVertices S1 misses InputVertices S2 & S = S1 +* S2 implies 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) )
assume that
A1: InnerVertices S1 misses InputVertices S2 and
A2: S = S1 +* S2 ; ::_thesis: 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)
A3: the carrier of S = the carrier of S1 \/ the carrier of S2 by A2, Def2;
let A1 be non-empty Circuit of S1; ::_thesis: 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)
let A2 be non-empty Circuit of S2; ::_thesis: 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)
let A be non-empty Circuit of S; ::_thesis: ( A1 tolerates A2 & A = A1 +* A2 implies 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) )
assume that
A4: A1 tolerates A2 and
A5: A = A1 +* A2 ; ::_thesis: 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)
let s be State of A; ::_thesis: 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)
let s1 be State of A1; ::_thesis: 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)
let s2 be State of A2; ::_thesis: ( s1 = s | the carrier of S1 & s2 = s | the carrier of S2 implies Following s = (Following s1) +* (Following s2) )
assume that
A6: s1 = s | the carrier of S1 and
A7: s2 = s | the carrier of S2 ; ::_thesis: Following s = (Following s1) +* (Following s2)
A8: dom (Following s2) = the carrier of S2 by CIRCUIT1:3;
A9: dom (Following s1) = the carrier of S1 by CIRCUIT1:3;
A10: now__::_thesis:_for_x_being_set_st_x_in_(dom_(Following_s1))_\/_(dom_(Following_s2))_holds_
(_(_x_in_dom_(Following_s2)_implies_(Following_s)_._x_=_(Following_s2)_._x_)_&_(_not_x_in_dom_(Following_s2)_implies_(Following_s)_._x_=_(Following_s1)_._x_)_)
let x be set ; ::_thesis: ( x in (dom (Following s1)) \/ (dom (Following s2)) implies ( ( x in dom (Following s2) implies (Following s) . x = (Following s2) . x ) & ( not x in dom (Following s2) implies (Following s) . x = (Following s1) . x ) ) )
assume  x in (dom (Following s1)) \/ (dom (Following s2)) ; ::_thesis: ( ( x in dom (Following s2) implies (Following s) . x = (Following s2) . x ) & ( not x in dom (Following s2) implies (Following s) . x = (Following s1) . x ) )
then reconsider v = x as Vertex of S by A2, A9, A8, Def2;
hereby  ::_thesis: ( not x in dom (Following s2) implies (Following s) . x = (Following s1) . x )
assume  x in dom (Following s2) ; ::_thesis: (Following s) . x = (Following s2) . x
then reconsider v2 = x as Vertex of S2 by CIRCUIT1:3;
A11: now__::_thesis:_(_v2_in_InputVertices_S2_implies_v_in_InputVertices_S_)
 the ResultSort of S = the ResultSort of S1 +* the ResultSort of S2 by A2, Def2;
then A12: rng the ResultSort of S c= (rng the ResultSort of S1) \/ (rng the ResultSort of S2) by FUNCT_4:17;
assume A13: v2 in InputVertices S2 ; ::_thesis: v in InputVertices S
then A14: not v2 in rng the ResultSort of S2 by XBOOLE_0:def_5;
 not v2 in rng the ResultSort of S1 by A1, A13, XBOOLE_0:3;
then  not v in rng the ResultSort of S by A14, A12, XBOOLE_0:def_3;
hence  v in InputVertices S by XBOOLE_0:def_5; ::_thesis: verum
end;
 (InputVertices S2) \/ (InnerVertices S2) = the carrier of S2 by XBOOLE_1:45;
then  ( v2 in InnerVertices S2 or v2 in InputVertices S2 ) by XBOOLE_0:def_3;
then  ( v in InnerVertices S2 or ( v in the carrier of S2 & v in InputVertices S ) ) by A11;
hence  (Following s) . x = (Following s2) . x by A2, A4, A5, A7, Th31; ::_thesis: verum
end;
assume A15: not x in dom (Following s2) ; ::_thesis: (Following s) . x = (Following s1) . x
then reconsider v1 = v as Vertex of S1 by A3, A8, XBOOLE_0:def_3;
 rng the ResultSort of S2 c= the carrier of S2 by RELAT_1:def_19;
then A16: not v1 in rng the ResultSort of S2 by A8, A15;
A17: now__::_thesis:_(_v1_in_InputVertices_S1_implies_v_in_InputVertices_S_)
assume  v1 in InputVertices S1 ; ::_thesis: v in InputVertices S
then A18: not v1 in rng the ResultSort of S1 by XBOOLE_0:def_5;
 the ResultSort of S = the ResultSort of S1 +* the ResultSort of S2 by A2, Def2;
then  rng the ResultSort of S c= (rng the ResultSort of S1) \/ (rng the ResultSort of S2) by FUNCT_4:17;
then  not v in rng the ResultSort of S by A16, A18, XBOOLE_0:def_3;
hence  v in InputVertices S by XBOOLE_0:def_5; ::_thesis: verum
end;
 (InputVertices S1) \/ (InnerVertices S1) = the carrier of S1 by XBOOLE_1:45;
then  ( v1 in InnerVertices S1 or v1 in InputVertices S1 ) by XBOOLE_0:def_3;
hence  (Following s) . x = (Following s1) . x by A2, A4, A5, A6, A17, Th31; ::_thesis: verum
end;
 dom (Following s) = the carrier of S by CIRCUIT1:3;
hence  Following s = (Following s1) +* (Following s2) by A3, A9, A8, A10, FUNCT_4:def_1; ::_thesis: verum
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
let S1, S2, S be non empty non void Circuit-like ManySortedSign ; ::_thesis: ( InnerVertices S2 misses InputVertices S1 & S = S1 +* S2 implies 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) )
assume that
A1: InnerVertices S2 misses InputVertices S1 and
A2: S = S1 +* S2 ; ::_thesis: 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)
let A1 be non-empty Circuit of S1; ::_thesis: 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)
let A2 be non-empty Circuit of S2; ::_thesis: 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)
let A be non-empty Circuit of S; ::_thesis: ( A1 tolerates A2 & A = A1 +* A2 implies 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) )
assume that
A3: A1 tolerates A2 and
A4: A = A1 +* A2 ; ::_thesis: 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)
 S1 tolerates S2 by A3, Def3;
then A5: S = S2 +* S1 by A2, Th5;
 A = A2 +* A1 by A3, A4, Th22;
hence  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) by A1, A3, A5, Th19, Th32; ::_thesis: verum
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
let S1, S2, S be non empty non void Circuit-like ManySortedSign ; ::_thesis: ( InputVertices S1 c= InputVertices S2 & S = S1 +* S2 implies 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) )
assume  InputVertices S1 c= InputVertices S2 ; ::_thesis: ( not S = S1 +* S2 or 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) )
then  InnerVertices S2 misses InputVertices S1 by XBOOLE_1:63, XBOOLE_1:79;
hence  ( not S = S1 +* S2 or 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) ) by Th33; ::_thesis: verum
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
let S1, S2, S be non empty non void Circuit-like ManySortedSign ; ::_thesis: ( InputVertices S2 c= InputVertices S1 & S = S1 +* S2 implies 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) )
assume  InputVertices S2 c= InputVertices S1 ; ::_thesis: ( not S = S1 +* S2 or 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) )
then  InnerVertices S1 misses InputVertices S2 by XBOOLE_1:63, XBOOLE_1:79;
hence  ( not S = S1 +* S2 or 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) ) by Th32; ::_thesis: verum
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
set pf = [p,f];
reconsider C = (rng p) \/ {x} as non empty set ;
 x in {x} by TARSKI:def_1;
then reconsider ox = x as Element of C by XBOOLE_0:def_3;
 rng p c= C by XBOOLE_1:7;
then  p is FinSequence of C by FINSEQ_1:def_4;
then reconsider pp = p as Element of C * by FINSEQ_1:def_11;
reconsider R = {[p,f]} --> ox as Function of {[p,f]},C ;
reconsider A = {[p,f]} --> pp as Function of {[p,f]},(C *) ;
reconsider S = ManySortedSign(# C,{[p,f]},A,R #) as non void strict ManySortedSign ;
take  S ; ::_thesis: ( the carrier of S = (rng p) \/ {x} & the carrier' of S = {[p,f]} & the Arity of S . [p,f] = p & the ResultSort of S . [p,f] = x )
 [p,f] in {[p,f]} by TARSKI:def_1;
hence  ( the carrier of S = (rng p) \/ {x} & the carrier' of S = {[p,f]} & the Arity of S . [p,f] = p & the ResultSort of S . [p,f] = x ) by FUNCOP_1:7; ::_thesis: verum
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
let S1, S2 be non void strict ManySortedSign ; ::_thesis: ( the carrier of S1 = (rng p) \/ {x} & the carrier' of S1 = {[p,f]} & the Arity of S1 . [p,f] = p & the ResultSort of S1 . [p,f] = x & the carrier of S2 = (rng p) \/ {x} & the carrier' of S2 = {[p,f]} & the Arity of S2 . [p,f] = p & the ResultSort of S2 . [p,f] = x implies S1 = S2 )
assume A1: ( the carrier of S1 = (rng p) \/ {x} & the carrier' of S1 = {[p,f]} & the Arity of S1 . [p,f] = p & the ResultSort of S1 . [p,f] = x & the carrier of S2 = (rng p) \/ {x} & the carrier' of S2 = {[p,f]} & the Arity of S2 . [p,f] = p & the ResultSort of S2 . [p,f] = x & not S1 = S2 ) ; ::_thesis: contradiction
then  dom the Arity of S1 = {[p,f]} by FUNCT_2:def_1;
then A2: the Arity of S1 = {[[p,f],p]} by A1, GRFUNC_1:7;
 dom the ResultSort of S1 = {[p,f]} by A1, FUNCT_2:def_1;
then A3: the ResultSort of S1 = {[[p,f],x]} by A1, GRFUNC_1:7;
 dom the Arity of S2 = {[p,f]} by A1, FUNCT_2:def_1;
then A4: the Arity of S2 = {[[p,f],p]} by A1, GRFUNC_1:7;
 dom the ResultSort of S2 = {[p,f]} by A1, FUNCT_2:def_1;
hence  contradiction by A1, A2, A4, A3, GRFUNC_1:7; ::_thesis: verum
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
 the carrier of (1GateCircStr (p,f,x)) = (rng p) \/ {x} by Def5;
hence  not the carrier of (1GateCircStr (p,f,x)) is empty ; :: according to STRUCT_0:def_1 ::_thesis: verum
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
let f, x be set ; ::_thesis: 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 )
let p be FinSequence; ::_thesis: ( the Arity of (1GateCircStr (p,f,x)) = (p,f) .--> p & the ResultSort of (1GateCircStr (p,f,x)) = (p,f) .--> x )
set S = 1GateCircStr (p,f,x);
 the Arity of (1GateCircStr (p,f,x)) . [p,f] = p by Def5;
then A1: for x being set st x in {[p,f]} holds
the Arity of (1GateCircStr (p,f,x)) . x = p by TARSKI:def_1;
A2: the carrier' of (1GateCircStr (p,f,x)) = {[p,f]} by Def5;
then  dom the Arity of (1GateCircStr (p,f,x)) = {[p,f]} by FUNCT_2:def_1;
hence  the Arity of (1GateCircStr (p,f,x)) = (p,f) .--> p by A1, FUNCOP_1:11; ::_thesis: the ResultSort of (1GateCircStr (p,f,x)) = (p,f) .--> x
 the ResultSort of (1GateCircStr (p,f,x)) . [p,f] = x by Def5;
then A3: for y being set st y in {[p,f]} holds
the ResultSort of (1GateCircStr (p,f,x)) . y = x by TARSKI:def_1;
 dom the ResultSort of (1GateCircStr (p,f,x)) = {[p,f]} by A2, FUNCT_2:def_1;
hence  the ResultSort of (1GateCircStr (p,f,x)) = (p,f) .--> x by A3, FUNCOP_1:11; ::_thesis: verum
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
let f, x be set ; ::_thesis: 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 )
let p be FinSequence; ::_thesis: for g being Gate of (1GateCircStr (p,f,x)) holds
( g = [p,f] & the_arity_of g = p & the_result_sort_of g = x )
set S = 1GateCircStr (p,f,x);
let o be Gate of (1GateCircStr (p,f,x)); ::_thesis: ( o = [p,f] & the_arity_of o = p & the_result_sort_of o = x )
A1: the ResultSort of (1GateCircStr (p,f,x)) . [p,f] = x by Def5;
A2: the carrier' of (1GateCircStr (p,f,x)) = {[p,f]} by Def5;
hence  o = [p,f] by TARSKI:def_1; ::_thesis: ( the_arity_of o = p & the_result_sort_of o = x )
 the Arity of (1GateCircStr (p,f,x)) . [p,f] = p by Def5;
hence  ( the_arity_of o = p & the_result_sort_of o = x ) by A2, A1, TARSKI:def_1; ::_thesis: verum
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
let f, x be set ; ::_thesis: for p being FinSequence holds
( InputVertices (1GateCircStr (p,f,x)) = (rng p) \ {x} & InnerVertices (1GateCircStr (p,f,x)) = {x} )
let p be FinSequence; ::_thesis: ( InputVertices (1GateCircStr (p,f,x)) = (rng p) \ {x} & InnerVertices (1GateCircStr (p,f,x)) = {x} )
 the ResultSort of (1GateCircStr (p,f,x)) = (p,f) .--> x by Th36;
then A1: rng the ResultSort of (1GateCircStr (p,f,x)) = {x} by FUNCOP_1:8;
 the carrier of (1GateCircStr (p,f,x)) = (rng p) \/ {x} by Def5;
hence  ( InputVertices (1GateCircStr (p,f,x)) = (rng p) \ {x} & InnerVertices (1GateCircStr (p,f,x)) = {x} ) by A1, XBOOLE_1:40; ::_thesis: verum
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
take  1GateCircStr (p,f,[p,f]) ; ::_thesis: ( the carrier of (1GateCircStr (p,f,[p,f])) = (rng p) \/ {[p,f]} & the carrier' of (1GateCircStr (p,f,[p,f])) = {[p,f]} & the Arity of (1GateCircStr (p,f,[p,f])) . [p,f] = p & the ResultSort of (1GateCircStr (p,f,[p,f])) . [p,f] = [p,f] )
thus  ( the carrier of (1GateCircStr (p,f,[p,f])) = (rng p) \/ {[p,f]} & the carrier' of (1GateCircStr (p,f,[p,f])) = {[p,f]} & the Arity of (1GateCircStr (p,f,[p,f])) . [p,f] = p & the ResultSort of (1GateCircStr (p,f,[p,f])) . [p,f] = [p,f] ) by Def5; ::_thesis: verum
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
let S1, S2 be non void strict ManySortedSign ; ::_thesis: ( the carrier of S1 = (rng p) \/ {[p,f]} & the carrier' of S1 = {[p,f]} & the Arity of S1 . [p,f] = p & the ResultSort of S1 . [p,f] = [p,f] & the carrier of S2 = (rng p) \/ {[p,f]} & the carrier' of S2 = {[p,f]} & the Arity of S2 . [p,f] = p & the ResultSort of S2 . [p,f] = [p,f] implies S1 = S2 )
assume A1: ( the carrier of S1 = (rng p) \/ {[p,f]} & the carrier' of S1 = {[p,f]} & the Arity of S1 . [p,f] = p & the ResultSort of S1 . [p,f] = [p,f] & the carrier of S2 = (rng p) \/ {[p,f]} & the carrier' of S2 = {[p,f]} & the Arity of S2 . [p,f] = p & the ResultSort of S2 . [p,f] = [p,f] & not S1 = S2 ) ; ::_thesis: contradiction
then  S1 = 1GateCircStr (p,f,[p,f]) by Def5;
hence  contradiction by A1, Def5; ::_thesis: verum
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
 the carrier of (1GateCircStr (p,f)) = (rng p) \/ {[p,f]} by Def6;
hence  not the carrier of (1GateCircStr (p,f)) is empty ; :: according to STRUCT_0:def_1 ::_thesis: verum
end;
end;

theorem :: CIRCCOMB:39
for f being set
for p being FinSequence holds 1GateCircStr (p,f) = 1GateCircStr (p,f,[p,f])
proof
let f be set ; ::_thesis: for p being FinSequence holds 1GateCircStr (p,f) = 1GateCircStr (p,f,[p,f])
let p be FinSequence; ::_thesis: 1GateCircStr (p,f) = 1GateCircStr (p,f,[p,f])
set S = 1GateCircStr (p,f);
A1: the carrier' of (1GateCircStr (p,f)) = {[p,f]} by Def6;
A2: the Arity of (1GateCircStr (p,f)) . [p,f] = p by Def6;
A3: the ResultSort of (1GateCircStr (p,f)) . [p,f] = [p,f] by Def6;
 the carrier of (1GateCircStr (p,f)) = (rng p) \/ {[p,f]} by Def6;
hence  1GateCircStr (p,f) = 1GateCircStr (p,f,[p,f]) by A1, A2, A3, Def5; ::_thesis: verum
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
let f be set ; ::_thesis: for p being FinSequence holds
( the Arity of (1GateCircStr (p,f)) = (p,f) .--> p & the ResultSort of (1GateCircStr (p,f)) = (p,f) .--> [p,f] )
let p be FinSequence; ::_thesis: ( the Arity of (1GateCircStr (p,f)) = (p,f) .--> p & the ResultSort of (1GateCircStr (p,f)) = (p,f) .--> [p,f] )
set S = 1GateCircStr (p,f);
 the Arity of (1GateCircStr (p,f)) . [p,f] = p by Def6;
then A1: for x being set st x in {[p,f]} holds
the Arity of (1GateCircStr (p,f)) . x = p by TARSKI:def_1;
A2: the carrier' of (1GateCircStr (p,f)) = {[p,f]} by Def6;
then  dom the Arity of (1GateCircStr (p,f)) = {[p,f]} by FUNCT_2:def_1;
hence  the Arity of (1GateCircStr (p,f)) = (p,f) .--> p by A1, FUNCOP_1:11; ::_thesis: the ResultSort of (1GateCircStr (p,f)) = (p,f) .--> [p,f]
 the ResultSort of (1GateCircStr (p,f)) . [p,f] = [p,f] by Def6;
then A3: for x being set st x in {[p,f]} holds
the ResultSort of (1GateCircStr (p,f)) . x = [p,f] by TARSKI:def_1;
 dom the ResultSort of (1GateCircStr (p,f)) = {[p,f]} by A2, FUNCT_2:def_1;
hence  the ResultSort of (1GateCircStr (p,f)) = (p,f) .--> [p,f] by A3, FUNCOP_1:11; ::_thesis: verum
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
let f be set ; ::_thesis: 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 )
let p be FinSequence; ::_thesis: for g being Gate of (1GateCircStr (p,f)) holds
( g = [p,f] & the_arity_of g = p & the_result_sort_of g = g )
set S = 1GateCircStr (p,f);
let o be Gate of (1GateCircStr (p,f)); ::_thesis: ( o = [p,f] & the_arity_of o = p & the_result_sort_of o = o )
 the carrier' of (1GateCircStr (p,f)) = {[p,f]} by Def6;
hence  o = [p,f] by TARSKI:def_1; ::_thesis: ( the_arity_of o = p & the_result_sort_of o = o )
hence  ( the_arity_of o = p & the_result_sort_of o = o ) by Def6; ::_thesis: verum
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
let f be set ; ::_thesis: for p being FinSequence holds
( InputVertices (1GateCircStr (p,f)) = rng p & InnerVertices (1GateCircStr (p,f)) = {[p,f]} )
let p be FinSequence; ::_thesis: ( InputVertices (1GateCircStr (p,f)) = rng p & InnerVertices (1GateCircStr (p,f)) = {[p,f]} )
A1: the ResultSort of (1GateCircStr (p,f)) = (p,f) .--> [p,f] by Th40;
then A2: rng the ResultSort of (1GateCircStr (p,f)) = {[p,f]} by FUNCOP_1:8;
A3: the carrier of (1GateCircStr (p,f)) = (rng p) \/ {[p,f]} by Def6;
hence  InputVertices (1GateCircStr (p,f)) c= rng p by A2, XBOOLE_1:43; :: according to XBOOLE_0:def_10 ::_thesis: ( rng p c= InputVertices (1GateCircStr (p,f)) & InnerVertices (1GateCircStr (p,f)) = {[p,f]} )
A4: now__::_thesis:_not_[p,f]_in_rng_p
assume  [p,f] in rng p ; ::_thesis: contradiction
then consider x being set  such that
A5: [x,[p,f]] in p by XTUPLE_0:def_13;
A6: {x,[p,f]} in {{x,[p,f]},{x}} by TARSKI:def_2;
A7: {p,f} in {{p,f},{p}} by TARSKI:def_2;
A8: p in {p,f} by TARSKI:def_2;
 [p,f] in {x,[p,f]} by TARSKI:def_2;
hence  contradiction by A5, A8, A7, A6, XREGULAR:9; ::_thesis: verum
end;
thus  rng p c= InputVertices (1GateCircStr (p,f)) ::_thesis: InnerVertices (1GateCircStr (p,f)) = {[p,f]}
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng p or x in InputVertices (1GateCircStr (p,f)) )
assume A9: x in rng p ; ::_thesis: x in InputVertices (1GateCircStr (p,f))
then A10: x in (rng p) \/ {[p,f]} by XBOOLE_0:def_3;
 not x in {[p,f]} by A4, A9, TARSKI:def_1;
hence  x in InputVertices (1GateCircStr (p,f)) by A2, A3, A10, XBOOLE_0:def_5; ::_thesis: verum
end;
thus  InnerVertices (1GateCircStr (p,f)) = {[p,f]} by A1, FUNCOP_1:8; ::_thesis: verum
end;

theorem Th43: :: CIRCCOMB:43
for f being set
for p, q being FinSequence holds 1GateCircStr (p,f) tolerates 1GateCircStr (q,f)
proof
let f be set ; ::_thesis: for p, q being FinSequence holds 1GateCircStr (p,f) tolerates 1GateCircStr (q,f)
let p, q be FinSequence; ::_thesis: 1GateCircStr (p,f) tolerates 1GateCircStr (q,f)
set S1 = 1GateCircStr (p,f);
set S2 = 1GateCircStr (q,f);
A1: ( [p,f] <> [q,f] implies {[p,f]} misses {[q,f]} ) by ZFMISC_1:11;
A2: the Arity of (1GateCircStr (q,f)) = (q,f) .--> q by Th40;
 the Arity of (1GateCircStr (p,f)) = (p,f) .--> p by Th40;
hence  the Arity of (1GateCircStr (p,f)) tolerates the Arity of (1GateCircStr (q,f)) by A2, A1, FUNCOP_1:87, XTUPLE_0:1; :: according to CIRCCOMB:def_1 ::_thesis: the ResultSort of (1GateCircStr (p,f)) tolerates the ResultSort of (1GateCircStr (q,f))
A3: the ResultSort of (1GateCircStr (q,f)) = (q,f) .--> [q,f] by Th40;
 the ResultSort of (1GateCircStr (p,f)) = (p,f) .--> [p,f] by Th40;
hence  the ResultSort of (1GateCircStr (p,f)) tolerates the ResultSort of (1GateCircStr (q,f)) by A3, A1, FUNCOP_1:87; ::_thesis: verum
end;

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)
proof
deffunc H1( set ) ->  set = F4($1,(F3() . $1));
consider f being Function such that
A1: dom f = F1() and
A2: for a being set st a in F1() holds
f . a = H1(a) from FUNCT_1:sch_3();
reconsider f = f as ManySortedSet of F1() by A1, PARTFUN1:def_2, RELAT_1:def_18;
take  f ; ::_thesis: for a being set
for b being Element of F2() st a in F1() & b = F3() . a holds
f . a = F4(a,b)
thus  for a being set
for b being Element of F2() st a in F1() & b = F3() . a holds
f . a = F4(a,b) by A2; ::_thesis: verum
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
set S = F1();
set SORTS = the carrier of F1() --> BOOLEAN;
consider CHARACT being ManySortedSet of the carrier' of F1() such that
A2: for o being set
for p being Element of the carrier of F1() * st o in the carrier' of F1() & p = the Arity of F1() . o holds
CHARACT . o = F2(o,p) from CIRCCOMB:sch_1();
A3: dom CHARACT = the carrier' of F1() by PARTFUN1:def_2;
 CHARACT is Function-yielding
proof
let x be set ; :: according to FUNCOP_1:def_6 ::_thesis: ( not x in proj1 CHARACT or CHARACT . x is set )
assume A4: x in dom CHARACT ; ::_thesis: CHARACT . x is set
then reconsider o = x as Gate of F1() by PARTFUN1:def_2;
reconsider p = the Arity of F1() . o as Element of the carrier of F1() * by A3, A4, FUNCT_2:5;
 CHARACT . x = F2(o,p) by A2, A3, A4;
hence  CHARACT . x is set by A1, A3, A4; ::_thesis: verum
end;
then reconsider CHARACT = CHARACT as ManySortedFunction of the carrier' of F1() ;
A5: dom the ResultSort of F1() = the carrier' of F1() by FUNCT_2:def_1;
A6: dom the Arity of F1() = the carrier' of F1() by FUNCT_2:def_1;
now__::_thesis:_for_i_being_set_st_i_in_the_carrier'_of_F1()_holds_
CHARACT_._i_is_Function_of_((((_the_carrier_of_F1()_-->_BOOLEAN)_#)_*_the_Arity_of_F1())_._i),(((_the_carrier_of_F1()_-->_BOOLEAN)_*_the_ResultSort_of_F1())_._i)
let i be set ; ::_thesis: ( i in the carrier' of F1() implies CHARACT . i is Function of (((( the carrier of F1() --> BOOLEAN) #) * the Arity of F1()) . i),((( the carrier of F1() --> BOOLEAN) * the ResultSort of F1()) . i) )
assume A7: i in the carrier' of F1() ; ::_thesis: CHARACT . i is Function of (((( the carrier of F1() --> BOOLEAN) #) * the Arity of F1()) . i),((( the carrier of F1() --> BOOLEAN) * the ResultSort of F1()) . i)
then reconsider o = i as Gate of F1() ;
reconsider p = the Arity of F1() . o as Element of the carrier of F1() * by A7, FUNCT_2:5;
A8: ((( the carrier of F1() --> BOOLEAN) #) * the Arity of F1()) . i = (( the carrier of F1() --> BOOLEAN) #) . p by A6, A7, FUNCT_1:13;
reconsider v = the ResultSort of F1() . o as Vertex of F1() by A7, FUNCT_2:5;
 ( the carrier of F1() --> BOOLEAN) . v = BOOLEAN by FUNCOP_1:7;
then A9: (( the carrier of F1() --> BOOLEAN) * the ResultSort of F1()) . i = BOOLEAN by A5, A7, FUNCT_1:13;
A10: (( the carrier of F1() --> BOOLEAN) #) . p = (len p) -tuples_on BOOLEAN by Th2;
 CHARACT . i = F2(o,p) by A2, A7;
hence  CHARACT . i is Function of (((( the carrier of F1() --> BOOLEAN) #) * the Arity of F1()) . i),((( the carrier of F1() --> BOOLEAN) * the ResultSort of F1()) . i) by A1, A7, A8, A10, A9; ::_thesis: verum
end;
then reconsider CHARACT = CHARACT as ManySortedFunction of (( the carrier of F1() --> BOOLEAN) #) * the Arity of F1(),( the carrier of F1() --> BOOLEAN) * the ResultSort of F1() by PBOOLE:def_15;
take  MSAlgebra(# ( the carrier of F1() --> BOOLEAN),CHARACT #) ; ::_thesis: ( the Sorts of MSAlgebra(# ( the carrier of F1() --> BOOLEAN),CHARACT #) = 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 MSAlgebra(# ( the carrier of F1() --> BOOLEAN),CHARACT #) . g = F2(g,p) ) )
thus  ( the Sorts of MSAlgebra(# ( the carrier of F1() --> BOOLEAN),CHARACT #) = 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 MSAlgebra(# ( the carrier of F1() --> BOOLEAN),CHARACT #) . g = F2(g,p) ) ) by A2; ::_thesis: verum
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
deffunc H1( set , set ) ->  set = c1 `2 ;
let S be non empty ManySortedSign ; ::_thesis: ( S is gate`2isBoolean implies S is gate`2=den )
assume A1: for g being set st g in the carrier' of S holds
for p being FinSequence st p = the Arity of S . g holds
ex f being Function of ((len p) -tuples_on BOOLEAN),BOOLEAN st g = [(g `1),f] ; :: according to CIRCCOMB:def_9 ::_thesis: S is gate`2=den
A2: now__::_thesis:_for_g_being_set_
for_p_being_Element_of_the_carrier_of_S_*_st_g_in_the_carrier'_of_S_&_p_=_the_Arity_of_S_._g_holds_
H1(g,p)_is_Function_of_((len_p)_-tuples_on_BOOLEAN),BOOLEAN
let g be set ; ::_thesis: for p being Element of the carrier of S * st g in the carrier' of S & p = the Arity of S . g holds
H1(g,p) is Function of ((len p) -tuples_on BOOLEAN),BOOLEAN
let p be Element of the carrier of S * ; ::_thesis: ( g in the carrier' of S & p = the Arity of S . g implies H1(g,p) is Function of ((len p) -tuples_on BOOLEAN),BOOLEAN )
assume that
A3: g in the carrier' of S and
A4: p = the Arity of S . g ; ::_thesis: H1(g,p) is Function of ((len p) -tuples_on BOOLEAN),BOOLEAN
 ex f being Function of ((len p) -tuples_on BOOLEAN),BOOLEAN st g = [(g `1),f] by A1, A3, A4;
hence  H1(g,p) is Function of ((len p) -tuples_on BOOLEAN),BOOLEAN by MCART_1:7; ::_thesis: verum
end;
consider A being strict MSAlgebra over S such that
A5: ( the Sorts of A = the carrier of S --> BOOLEAN & ( for g being set
for p being Element of the carrier of S * st g in the carrier' of S & p = the Arity of S . g holds
the Charact of A . g = H1(g,p) ) ) from CIRCCOMB:sch_2(A2);
take  A ; :: according to CIRCCOMB:def_11 ::_thesis: A is gate`2=den
let g be set ; :: according to CIRCCOMB:def_10 ::_thesis: ( g in the carrier' of S implies g = [(g `1),( the Charact of A . g)] )
assume A6: g in the carrier' of S ; ::_thesis: g = [(g `1),( the Charact of A . g)]
then reconsider p = the Arity of S . g as Element of the carrier of S * by FUNCT_2:5;
consider f being Function of ((len p) -tuples_on BOOLEAN),BOOLEAN such that
A7: g = [(g `1),f] by A1, A6;
 f = g `2 by A7, MCART_1:7;
hence  g = [(g `1),( the Charact of A . g)] by A5, A6, A7; ::_thesis: verum
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
let S be non empty ManySortedSign ; ::_thesis: ( S is unsplit iff for o being set st o in the carrier' of S holds
the ResultSort of S . o = o )
hereby  ::_thesis: ( ( for o being set st o in the carrier' of S holds
the ResultSort of S . o = o ) implies S is unsplit )
assume  S is unsplit ; ::_thesis: for o being set st o in the carrier' of S holds
the ResultSort of S . o = o
then  the ResultSort of S = id the carrier' of S by Def7;
hence  for o being set st o in the carrier' of S holds
the ResultSort of S . o = o by FUNCT_1:17; ::_thesis: verum
end;
assume A1: for o being set st o in the carrier' of S holds
the ResultSort of S . o = o ; ::_thesis: S is unsplit
 dom the ResultSort of S = the carrier' of S by FUNCT_2:def_1;
hence  the ResultSort of S = id the carrier' of S by A1, FUNCT_1:17; :: according to CIRCCOMB:def_7 ::_thesis: verum
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
let S be non empty ManySortedSign ; ::_thesis: ( S is unsplit implies the carrier' of S c= the carrier of S )
assume A1: S is unsplit ; ::_thesis: the carrier' of S c= the carrier of S
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier' of S or x in the carrier of S )
assume A2: x in the carrier' of S ; ::_thesis: x in the carrier of S
then  the ResultSort of S . x = x by A1, Th44;
hence  x in the carrier of S by A2, FUNCT_2:5; ::_thesis: verum
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
let S be non empty ManySortedSign ; ::_thesis: ( S is unsplit implies S is Circuit-like )
assume A1: the ResultSort of S = id the carrier' of S ; :: according to CIRCCOMB:def_7 ::_thesis: S is Circuit-like
let S9 be non empty non void ManySortedSign ; :: according to MSAFREE2:def_6 ::_thesis: ( not S9 = S or for b1, b2 being Element of the carrier' of S9 holds
( not the_result_sort_of b1 = the_result_sort_of b2 or b1 = b2 ) )
assume A2: S9 = S ; ::_thesis: for b1, b2 being Element of the carrier' of S9 holds
( not the_result_sort_of b1 = the_result_sort_of b2 or b1 = b2 )
let o1, o2 be Gate of S9; ::_thesis: ( not the_result_sort_of o1 = the_result_sort_of o2 or o1 = o2 )
 the_result_sort_of o1 = o1 by A1, A2, FUNCT_1:17;
hence  ( not the_result_sort_of o1 = the_result_sort_of o2 or o1 = o2 ) by A1, A2, FUNCT_1:17; ::_thesis: verum
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
let f be set ; ::_thesis: for p being FinSequence holds
( 1GateCircStr (p,f) is unsplit & 1GateCircStr (p,f) is gate`1=arity )
let p be FinSequence; ::_thesis: ( 1GateCircStr (p,f) is unsplit & 1GateCircStr (p,f) is gate`1=arity )
set S = 1GateCircStr (p,f);
A1: now__::_thesis:_for_x_being_set_st_x_in_{[p,f]}_holds_
the_ResultSort_of_(1GateCircStr_(p,f))_._x_=_x
let x be set ; ::_thesis: ( x in {[p,f]} implies the ResultSort of (1GateCircStr (p,f)) . x = x )
assume  x in {[p,f]} ; ::_thesis: the ResultSort of (1GateCircStr (p,f)) . x = x
then  x = [p,f] by TARSKI:def_1;
hence  the ResultSort of (1GateCircStr (p,f)) . x = x by Def6; ::_thesis: verum
end;
A2: the carrier' of (1GateCircStr (p,f)) = {[p,f]} by Def6;
then  dom the ResultSort of (1GateCircStr (p,f)) = {[p,f]} by FUNCT_2:def_1;
hence  the ResultSort of (1GateCircStr (p,f)) = id the carrier' of (1GateCircStr (p,f)) by A2, A1, FUNCT_1:17; :: according to CIRCCOMB:def_7 ::_thesis: 1GateCircStr (p,f) is gate`1=arity
let g be set ; :: according to CIRCCOMB:def_8 ::_thesis: ( g in the carrier' of (1GateCircStr (p,f)) implies g = [( the Arity of (1GateCircStr (p,f)) . g),(g `2)] )
assume  g in the carrier' of (1GateCircStr (p,f)) ; ::_thesis: g = [( the Arity of (1GateCircStr (p,f)) . g),(g `2)]
then A3: g = [p,f] by A2, TARSKI:def_1;
then  the Arity of (1GateCircStr (p,f)) . g = p by Def6;
hence  g = [( the Arity of (1GateCircStr (p,f)) . g),(g `2)] by A3, MCART_1:7; ::_thesis: verum
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
set f = the set ;
set p = the FinSequence;
take  1GateCircStr ( the FinSequence, the set ) ; ::_thesis: ( 1GateCircStr ( the FinSequence, the set ) is unsplit & 1GateCircStr ( the FinSequence, the set ) is gate`1=arity & not 1GateCircStr ( the FinSequence, the set ) is void & 1GateCircStr ( the FinSequence, the set ) is strict & not 1GateCircStr ( the FinSequence, the set ) is empty )
thus  ( 1GateCircStr ( the FinSequence, the set ) is unsplit & 1GateCircStr ( the FinSequence, the set ) is gate`1=arity & not 1GateCircStr ( the FinSequence, the set ) is void & 1GateCircStr ( the FinSequence, the set ) is strict & not 1GateCircStr ( the FinSequence, the set ) is empty ) ; ::_thesis: verum
end;
end;

theorem Th47: :: CIRCCOMB:47
for S1, S2 being non empty unsplit gate`1=arity ManySortedSign holds S1 tolerates S2
proof
let S1, S2 be non empty unsplit gate`1=arity ManySortedSign ; ::_thesis: S1 tolerates S2
set A1 = the Arity of S1;
set A2 = the Arity of S2;
set R1 = the ResultSort of S1;
set R2 = the ResultSort of S2;
thus  the Arity of S1 tolerates the Arity of S2 :: according to CIRCCOMB:def_1 ::_thesis: the ResultSort of S1 tolerates the ResultSort of S2
proof
let x be set ; :: according to PARTFUN1:def_4 ::_thesis: ( not x in (proj1 the Arity of S1) /\ (proj1 the Arity of S2) or the Arity of S1 . x = the Arity of S2 . x )
assume A1: x in (dom the Arity of S1) /\ (dom the Arity of S2) ; ::_thesis: the Arity of S1 . x = the Arity of S2 . x
then  x in dom the Arity of S2 by XBOOLE_0:def_4;
then  x in the carrier' of S2 by FUNCT_2:def_1;
then A2: x = [( the Arity of S2 . x),(x `2)] by Def8;
 x in dom the Arity of S1 by A1, XBOOLE_0:def_4;
then  x in the carrier' of S1 by FUNCT_2:def_1;
then  x = [( the Arity of S1 . x),(x `2)] by Def8;
hence  the Arity of S1 . x = the Arity of S2 . x by A2, XTUPLE_0:1; ::_thesis: verum
end;
let x be set ; :: according to PARTFUN1:def_4 ::_thesis: ( not x in (proj1 the ResultSort of S1) /\ (proj1 the ResultSort of S2) or the ResultSort of S1 . x = the ResultSort of S2 . x )
assume A3: x in (dom the ResultSort of S1) /\ (dom the ResultSort of S2) ; ::_thesis: the ResultSort of S1 . x = the ResultSort of S2 . x
then  x in dom the ResultSort of S1 by XBOOLE_0:def_4;
then  x in the carrier' of S1 by FUNCT_2:def_1;
then A4: the ResultSort of S1 . x = x by Th44;
 x in dom the ResultSort of S2 by A3, XBOOLE_0:def_4;
then  x in the carrier' of S2 by FUNCT_2:def_1;
hence  the ResultSort of S1 . x = the ResultSort of S2 . x by A4, Th44; ::_thesis: verum
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
let S1, S2 be non empty ManySortedSign ; ::_thesis: 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
let A1 be MSAlgebra over S1; ::_thesis: 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
let A2 be MSAlgebra over S2; ::_thesis: ( A1 is gate`2=den & A2 is gate`2=den implies the Charact of A1 tolerates the Charact of A2 )
assume that
A1: A1 is gate`2=den and
A2: A2 is gate`2=den ; ::_thesis: the Charact of A1 tolerates the Charact of A2
let x be set ; :: according to PARTFUN1:def_4 ::_thesis: ( not x in (proj1 the Charact of A1) /\ (proj1 the Charact of A2) or the Charact of A1 . x = the Charact of A2 . x )
set C1 = the Charact of A1;
set C2 = the Charact of A2;
assume A3: x in (dom the Charact of A1) /\ (dom the Charact of A2) ; ::_thesis: the Charact of A1 . x = the Charact of A2 . x
then  x in dom the Charact of A2 by XBOOLE_0:def_4;
then  x in the carrier' of S2 by PARTFUN1:def_2;
then A4: x = [(x `1),( the Charact of A2 . x)] by A2, Def10;
 x in dom the Charact of A1 by A3, XBOOLE_0:def_4;
then  x in the carrier' of S1 by PARTFUN1:def_2;
then  x = [(x `1),( the Charact of A1 . x)] by A1, Def10;
hence  the Charact of A1 . x = the Charact of A2 . x by A4, XTUPLE_0:1; ::_thesis: verum
end;

theorem Th49: :: CIRCCOMB:49
for S1, S2 being non empty unsplit ManySortedSign holds S1 +* S2 is unsplit
proof
let S1, S2 be non empty unsplit ManySortedSign ; ::_thesis: S1 +* S2 is unsplit
set S = S1 +* S2;
A1: the ResultSort of (S1 +* S2) = the ResultSort of S1 +* the ResultSort of S2 by Def2;
A2: the ResultSort of S1 = id the carrier' of S1 by Def7;
A3: the ResultSort of S2 = id the carrier' of S2 by Def7;
 the carrier' of (S1 +* S2) = the carrier' of S1 \/ the carrier' of S2 by Def2;
hence  the ResultSort of (S1 +* S2) = id the carrier' of (S1 +* S2) by A1, A2, A3, FUNCT_4:22; :: according to CIRCCOMB:def_7 ::_thesis: verum
end;

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
proof
let S1, S2 be non empty gate`1=arity ManySortedSign ; ::_thesis: S1 +* S2 is gate`1=arity
set S = S1 +* S2;
let g be set ; :: according to CIRCCOMB:def_8 ::_thesis: ( g in the carrier' of (S1 +* S2) implies g = [( the Arity of (S1 +* S2) . g),(g `2)] )
A1: dom the Arity of S1 = the carrier' of S1 by FUNCT_2:def_1;
A2: the Arity of (S1 +* S2) = the Arity of S1 +* the Arity of S2 by Def2;
assume A3: g in the carrier' of (S1 +* S2) ; ::_thesis: g = [( the Arity of (S1 +* S2) . g),(g `2)]
then reconsider g = g as Gate of (S1 +* S2) ;
A4: dom the Arity of S2 = the carrier' of S2 by FUNCT_2:def_1;
A5: the carrier' of (S1 +* S2) = the carrier' of S1 \/ the carrier' of S2 by Def2;
then A6: ( g in the carrier' of S1 or g in the carrier' of S2 ) by A3, XBOOLE_0:def_3;
A7: now__::_thesis:_(_not_g_in_the_carrier'_of_S2_implies_g_=_[(_the_Arity_of_(S1_+*_S2)_._g),(g_`2)]_)
assume A8: not g in the carrier' of S2 ; ::_thesis: g = [( the Arity of (S1 +* S2) . g),(g `2)]
then reconsider g1 = g as Gate of S1 by A5, A3, XBOOLE_0:def_3;
thus g = [( the Arity of S1 . g1),(g `2)] by A6, A8, Def8
.= [( the Arity of (S1 +* S2) . g),(g `2)] by A5, A2, A3, A1, A4, A8, FUNCT_4:def_1 ; ::_thesis: verum
end;
now__::_thesis:_(_g_in_the_carrier'_of_S2_implies_g_=_[(_the_Arity_of_(S1_+*_S2)_._g),(g_`2)]_)
assume A9: g in the carrier' of S2 ; ::_thesis: g = [( the Arity of (S1 +* S2) . g),(g `2)]
then reconsider g2 = g as Gate of S2 ;
thus g = [( the Arity of S2 . g2),(g `2)] by A9, Def8
.= [( the Arity of (S1 +* S2) . g),(g `2)] by A5, A2, A1, A4, A9, FUNCT_4:def_1 ; ::_thesis: verum
end;
hence  g = [( the Arity of (S1 +* S2) . g),(g `2)] by A7; ::_thesis: verum
end;

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
proof
let S1, S2 be non empty ManySortedSign ; ::_thesis: ( S1 is gate`2isBoolean & S2 is gate`2isBoolean implies S1 +* S2 is gate`2isBoolean )
set S = S1 +* S2;
assume that
A1: S1 is gate`2isBoolean and
A2: S2 is gate`2isBoolean ; ::_thesis: S1 +* S2 is gate`2isBoolean
let g be set ; :: according to CIRCCOMB:def_9 ::_thesis: ( g in the carrier' of (S1 +* S2) implies for p being FinSequence st p = the Arity of (S1 +* S2) . g holds
ex f being Function of ((len p) -tuples_on BOOLEAN),BOOLEAN st g = [(g `1),f] )
assume A3: g in the carrier' of (S1 +* S2) ; ::_thesis: for p being FinSequence st p = the Arity of (S1 +* S2) . g holds
ex f being Function of ((len p) -tuples_on BOOLEAN),BOOLEAN st g = [(g `1),f]
let p be FinSequence; ::_thesis: ( p = the Arity of (S1 +* S2) . g implies ex f being Function of ((len p) -tuples_on BOOLEAN),BOOLEAN st g = [(g `1),f] )
assume A4: p = the Arity of (S1 +* S2) . g ; ::_thesis: ex f being Function of ((len p) -tuples_on BOOLEAN),BOOLEAN st g = [(g `1),f]
reconsider g = g as Gate of (S1 +* S2) by A3;
A5: dom the Arity of S1 = the carrier' of S1 by FUNCT_2:def_1;
A6: the Arity of (S1 +* S2) = the Arity of S1 +* the Arity of S2 by Def2;
A7: dom the Arity of S2 = the carrier' of S2 by FUNCT_2:def_1;
A8: the carrier' of (S1 +* S2) = the carrier' of S1 \/ the carrier' of S2 by Def2;
then A9: ( g in the carrier' of S1 or g in the carrier' of S2 ) by A3, XBOOLE_0:def_3;
A10: now__::_thesis:_(_not_g_in_the_carrier'_of_S2_implies_ex_f_being_Function_of_((len_p)_-tuples_on_BOOLEAN),BOOLEAN_st_g_=_[(g_`1),f]_)
assume A11: not g in the carrier' of S2 ; ::_thesis: ex f being Function of ((len p) -tuples_on BOOLEAN),BOOLEAN st g = [(g `1),f]
then reconsider g1 = g as Gate of S1 by A8, A3, XBOOLE_0:def_3;
 the Arity of S1 . g1 = p by A8, A6, A3, A4, A5, A7, A11, FUNCT_4:def_1;
hence  ex f being Function of ((len p) -tuples_on BOOLEAN),BOOLEAN st g = [(g `1),f] by A1, A9, A11, Def9; ::_thesis: verum
end;
now__::_thesis:_(_g_in_the_carrier'_of_S2_implies_ex_f_being_Function_of_((len_p)_-tuples_on_BOOLEAN),BOOLEAN_st_g_=_[(g_`1),f]_)
assume A12: g in the carrier' of S2 ; ::_thesis: ex f being Function of ((len p) -tuples_on BOOLEAN),BOOLEAN st g = [(g `1),f]
then reconsider g2 = g as Gate of S2 ;
 the Arity of S2 . g2 = p by A8, A6, A4, A5, A7, A12, FUNCT_4:def_1;
hence  ex f being Function of ((len p) -tuples_on BOOLEAN),BOOLEAN st g = [(g `1),f] by A2, A12, Def9; ::_thesis: verum
end;
hence  ex f being Function of ((len p) -tuples_on BOOLEAN),BOOLEAN st g = [(g `1),f] by A10; ::_thesis: verum
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
 p is FinSequence of rng p by FINSEQ_1:def_4;
then reconsider p9 = p as Element of (rng p) * by FINSEQ_1:def_11;
set g1 = (rng p) --> X;
set g2 = x .--> Y;
set S = 1GateCircStr (p,f,x);
set SORTS = ((rng p) --> X) +* (x .--> Y);
set CHARACT = the carrier' of (1GateCircStr (p,f,x)) --> f;
A1: dom (x .--> Y) = {x} by FUNCOP_1:13;
A2: x in {x} by TARSKI:def_1;
then A3: (((rng p) --> X) +* (x .--> Y)) . x = (x .--> Y) . x by A1, FUNCT_4:13
.= Y by A2, FUNCOP_1:7 ;
A4: the carrier of (1GateCircStr (p,f,x)) = (rng p) \/ {x} by Def5;
then reconsider SORTS = ((rng p) --> X) +* (x .--> Y) as V2() ManySortedSet of the carrier of (1GateCircStr (p,f,x)) ;
 rng p c= the carrier of (1GateCircStr (p,f,x)) by A4, XBOOLE_1:7;
then  p is FinSequence of the carrier of (1GateCircStr (p,f,x)) by FINSEQ_1:def_4;
then reconsider pp = p as Element of the carrier of (1GateCircStr (p,f,x)) * by FINSEQ_1:def_11;
A5: dom (((rng p) --> X) #) = (rng p) * by PARTFUN1:def_2;
A6: dom ((rng p) --> X) = rng p by FUNCOP_1:13;
 (rng p) --> X tolerates x .--> Y
proof
let y be set ; :: according to PARTFUN1:def_4 ::_thesis: ( not y in (proj1 ((rng p) --> X)) /\ (proj1 (x .--> Y)) or ((rng p) --> X) . y = (x .--> Y) . y )
assume A7: y in (dom ((rng p) --> X)) /\ (dom (x .--> Y)) ; ::_thesis: ((rng p) --> X) . y = (x .--> Y) . y
then  y in rng p by A6, XBOOLE_0:def_4;
then A8: ((rng p) --> X) . y = X by FUNCOP_1:7;
A9: y in {x} by A1, A7, XBOOLE_0:def_4;
then  x = y by TARSKI:def_1;
hence  ((rng p) --> X) . y = (x .--> Y) . y by B1, A6, A7, A9, A8, FUNCOP_1:7, XBOOLE_0:def_4; ::_thesis: verum
end;
then  (rng p) --> X c= SORTS by FUNCT_4:28;
then  ((rng p) --> X) # c= SORTS # by Th1;
then A10: (((rng p) --> X) #) . p9 = (SORTS #) . pp by A5, GRFUNC_1:2;
A11: the carrier' of (1GateCircStr (p,f,x)) = {[p,f]} by Def5;
then A12: dom the ResultSort of (1GateCircStr (p,f,x)) = {[p,f]} by FUNCT_2:def_1;
A13: the ResultSort of (1GateCircStr (p,f,x)) . [p,f] = x by Def5;
A14: the Arity of (1GateCircStr (p,f,x)) . [p,f] = p by Def5;
A15: len p = n by CARD_1:def_7;
A16: dom the Arity of (1GateCircStr (p,f,x)) = {[p,f]} by A11, FUNCT_2:def_1;
now__::_thesis:_for_i_being_set_st_i_in_the_carrier'_of_(1GateCircStr_(p,f,x))_holds_
(_the_carrier'_of_(1GateCircStr_(p,f,x))_-->_f)_._i_is_Function_of_(((SORTS_#)_*_the_Arity_of_(1GateCircStr_(p,f,x)))_._i),((SORTS_*_the_ResultSort_of_(1GateCircStr_(p,f,x)))_._i)
let i be set ; ::_thesis: ( i in the carrier' of (1GateCircStr (p,f,x)) implies ( the carrier' of (1GateCircStr (p,f,x)) --> f) . i is Function of (((SORTS #) * the Arity of (1GateCircStr (p,f,x))) . i),((SORTS * the ResultSort of (1GateCircStr (p,f,x))) . i) )
A17: (SORTS #) . pp = n -tuples_on X by A15, A10, Th2;
assume A18: i in the carrier' of (1GateCircStr (p,f,x)) ; ::_thesis: ( the carrier' of (1GateCircStr (p,f,x)) --> f) . i is Function of (((SORTS #) * the Arity of (1GateCircStr (p,f,x))) . i),((SORTS * the ResultSort of (1GateCircStr (p,f,x))) . i)
then A19: i = [p,f] by A11, TARSKI:def_1;
then A20: ((SORTS #) * the Arity of (1GateCircStr (p,f,x))) . i = (SORTS #) . p by A11, A14, A16, A18, FUNCT_1:13;
 (SORTS * the ResultSort of (1GateCircStr (p,f,x))) . i = Y by A11, A13, A3, A12, A18, A19, FUNCT_1:13;
hence  ( the carrier' of (1GateCircStr (p,f,x)) --> f) . i is Function of (((SORTS #) * the Arity of (1GateCircStr (p,f,x))) . i),((SORTS * the ResultSort of (1GateCircStr (p,f,x))) . i) by A18, A20, A17, FUNCOP_1:7; ::_thesis: verum
end;
then reconsider CHARACT = the carrier' of (1GateCircStr (p,f,x)) --> f as ManySortedFunction of (SORTS #) * the Arity of (1GateCircStr (p,f,x)),SORTS * the ResultSort of (1GateCircStr (p,f,x)) by PBOOLE:def_15;
reconsider A = MSAlgebra(# SORTS,CHARACT #) as strict non-empty MSAlgebra over 1GateCircStr (p,f,x) by MSUALG_1:def_3;
take  A ; ::_thesis: ( the Sorts of A = ((rng p) --> X) +* (x .--> Y) & the Charact of A . [p,f] = f )
 [p,f] in {[p,f]} by TARSKI:def_1;
hence  ( the Sorts of A = ((rng p) --> X) +* (x .--> Y) & the Charact of A . [p,f] = f ) by A11, FUNCOP_1:7; ::_thesis: verum
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
set S = 1GateCircStr (p,f,x);
let A1, A2 be strict non-empty MSAlgebra over 1GateCircStr (p,f,x); ::_thesis: ( the Sorts of A1 = ((rng p) --> X) +* (x .--> Y) & the Charact of A1 . [p,f] = f & the Sorts of A2 = ((rng p) --> X) +* (x .--> Y) & the Charact of A2 . [p,f] = f implies A1 = A2 )
assume A21: ( the Sorts of A1 = ((rng p) --> X) +* (x .--> Y) & the Charact of A1 . [p,f] = f & the Sorts of A2 = ((rng p) --> X) +* (x .--> Y) & the Charact of A2 . [p,f] = f & not A1 = A2 ) ; ::_thesis: contradiction
A22: the carrier' of (1GateCircStr (p,f,x)) = {[p,f]} by Def5;
then  dom the Charact of A1 = {[p,f]} by PARTFUN1:def_2;
then A23: the Charact of A1 = {[[p,f],f]} by A21, GRFUNC_1:7;
 dom the Charact of A2 = {[p,f]} by A22, PARTFUN1:def_2;
hence  contradiction by A21, A23, GRFUNC_1:7; ::_thesis: verum
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
set S = 1GateCircStr (p,f);
set SORTS = the carrier of (1GateCircStr (p,f)) --> X;
set CHARACT = the carrier' of (1GateCircStr (p,f)) --> f;
A1: len p = n by CARD_1:def_7;
A2: the Arity of (1GateCircStr (p,f)) . [p,f] = p by Def6;
A3: the ResultSort of (1GateCircStr (p,f)) . [p,f] = [p,f] by Def6;
A4: the carrier' of (1GateCircStr (p,f)) = {[p,f]} by Def6;
then A5: dom the ResultSort of (1GateCircStr (p,f)) = {[p,f]} by FUNCT_2:def_1;
A6: the carrier of (1GateCircStr (p,f)) = (rng p) \/ {[p,f]} by Def6;
then  rng p c= the carrier of (1GateCircStr (p,f)) by XBOOLE_1:7;
then  p is FinSequence of the carrier of (1GateCircStr (p,f)) by FINSEQ_1:def_4;
then reconsider pp = p as Element of the carrier of (1GateCircStr (p,f)) * by FINSEQ_1:def_11;
A7: [p,f] in {[p,f]} by TARSKI:def_1;
then  [p,f] in the carrier of (1GateCircStr (p,f)) by A6, XBOOLE_0:def_3;
then A8: ( the carrier of (1GateCircStr (p,f)) --> X) . [p,f] = X by FUNCOP_1:7;
A9: dom the Arity of (1GateCircStr (p,f)) = {[p,f]} by A4, FUNCT_2:def_1;
now__::_thesis:_for_i_being_set_st_i_in_the_carrier'_of_(1GateCircStr_(p,f))_holds_
(_the_carrier'_of_(1GateCircStr_(p,f))_-->_f)_._i_is_Function_of_((((_the_carrier_of_(1GateCircStr_(p,f))_-->_X)_#)_*_the_Arity_of_(1GateCircStr_(p,f)))_._i),(((_the_carrier_of_(1GateCircStr_(p,f))_-->_X)_*_the_ResultSort_of_(1GateCircStr_(p,f)))_._i)
let i be set ; ::_thesis: ( i in the carrier' of (1GateCircStr (p,f)) implies ( the carrier' of (1GateCircStr (p,f)) --> f) . i is Function of (((( the carrier of (1GateCircStr (p,f)) --> X) #) * the Arity of (1GateCircStr (p,f))) . i),((( the carrier of (1GateCircStr (p,f)) --> X) * the ResultSort of (1GateCircStr (p,f))) . i) )
A10: (( the carrier of (1GateCircStr (p,f)) --> X) #) . pp = n -tuples_on X by A1, Th2;
assume A11: i in the carrier' of (1GateCircStr (p,f)) ; ::_thesis: ( the carrier' of (1GateCircStr (p,f)) --> f) . i is Function of (((( the carrier of (1GateCircStr (p,f)) --> X) #) * the Arity of (1GateCircStr (p,f))) . i),((( the carrier of (1GateCircStr (p,f)) --> X) * the ResultSort of (1GateCircStr (p,f))) . i)
then A12: i = [p,f] by A4, TARSKI:def_1;
then A13: ((( the carrier of (1GateCircStr (p,f)) --> X) #) * the Arity of (1GateCircStr (p,f))) . i = (( the carrier of (1GateCircStr (p,f)) --> X) #) . p by A4, A2, A9, A11, FUNCT_1:13;
 (( the carrier of (1GateCircStr (p,f)) --> X) * the ResultSort of (1GateCircStr (p,f))) . i = X by A4, A3, A8, A5, A11, A12, FUNCT_1:13;
hence  ( the carrier' of (1GateCircStr (p,f)) --> f) . i is Function of (((( the carrier of (1GateCircStr (p,f)) --> X) #) * the Arity of (1GateCircStr (p,f))) . i),((( the carrier of (1GateCircStr (p,f)) --> X) * the ResultSort of (1GateCircStr (p,f))) . i) by A11, A13, A10, FUNCOP_1:7; ::_thesis: verum
end;
then reconsider CHARACT = the carrier' of (1GateCircStr (p,f)) --> f as ManySortedFunction of (( the carrier of (1GateCircStr (p,f)) --> X) #) * the Arity of (1GateCircStr (p,f)),( the carrier of (1GateCircStr (p,f)) --> X) * the ResultSort of (1GateCircStr (p,f)) by PBOOLE:def_15;
reconsider A = MSAlgebra(# ( the carrier of (1GateCircStr (p,f)) --> X),CHARACT #) as strict non-empty MSAlgebra over 1GateCircStr (p,f) by MSUALG_1:def_3;
take  A ; ::_thesis: ( the Sorts of A = the carrier of (1GateCircStr (p,f)) --> X & the Charact of A . [p,f] = f )
thus  ( the Sorts of A = the carrier of (1GateCircStr (p,f)) --> X & the Charact of A . [p,f] = f ) by A4, A7, FUNCOP_1:7; ::_thesis: verum
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
set S = 1GateCircStr (p,f);
let A1, A2 be strict non-empty MSAlgebra over 1GateCircStr (p,f); ::_thesis: ( the Sorts of A1 = the carrier of (1GateCircStr (p,f)) --> X & the Charact of A1 . [p,f] = f & the Sorts of A2 = the carrier of (1GateCircStr (p,f)) --> X & the Charact of A2 . [p,f] = f implies A1 = A2 )
assume A14: ( the Sorts of A1 = the carrier of (1GateCircStr (p,f)) --> X & the Charact of A1 . [p,f] = f & the Sorts of A2 = the carrier of (1GateCircStr (p,f)) --> X & the Charact of A2 . [p,f] = f & not A1 = A2 ) ; ::_thesis: contradiction
A15: the carrier' of (1GateCircStr (p,f)) = {[p,f]} by Def6;
then  dom the Charact of A1 = {[p,f]} by PARTFUN1:def_2;
then A16: the Charact of A1 = {[[p,f],f]} by A14, GRFUNC_1:7;
 dom the Charact of A2 = {[p,f]} by A15, PARTFUN1:def_2;
hence  contradiction by A14, A16, GRFUNC_1:7; ::_thesis: verum
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
let n be Nat; ::_thesis: 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 )
let X be non empty set ; ::_thesis: 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 )
let f be Function of (n -tuples_on X),X; ::_thesis: for p being FinSeqLen of n holds
( 1GateCircuit (p,f) is gate`2=den & 1GateCircStr (p,f) is gate`2=den )
let p be FinSeqLen of n; ::_thesis: ( 1GateCircuit (p,f) is gate`2=den & 1GateCircStr (p,f) is gate`2=den )
thus A1: 1GateCircuit (p,f) is gate`2=den ::_thesis: 1GateCircStr (p,f) is gate`2=den
proof
let g be set ; :: according to CIRCCOMB:def_10 ::_thesis: ( g in the carrier' of (1GateCircStr (p,f)) implies g = [(g `1),( the Charact of (1GateCircuit (p,f)) . g)] )
assume  g in the carrier' of (1GateCircStr (p,f)) ; ::_thesis: g = [(g `1),( the Charact of (1GateCircuit (p,f)) . g)]
then A2: g = [p,f] by Th41;
hence g = [(g `1),f] by MCART_1:7
.= [(g `1),( the Charact of (1GateCircuit (p,f)) . g)] by A2, Def13 ;
::_thesis: verum
end;
take  1GateCircuit (p,f) ; :: according to CIRCCOMB:def_11 ::_thesis: 1GateCircuit (p,f) is gate`2=den
thus  1GateCircuit (p,f) is gate`2=den by A1; ::_thesis: verum
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
set X = BOOLEAN ;
let n be Nat; ::_thesis: for p being FinSeqLen of n
for f being Function of (n -tuples_on BOOLEAN),BOOLEAN holds 1GateCircStr (p,f) is gate`2isBoolean
let p be FinSeqLen of n; ::_thesis: for f being Function of (n -tuples_on BOOLEAN),BOOLEAN holds 1GateCircStr (p,f) is gate`2isBoolean
let f be Function of (n -tuples_on BOOLEAN),BOOLEAN; ::_thesis: 1GateCircStr (p,f) is gate`2isBoolean
let g be set ; :: according to CIRCCOMB:def_9 ::_thesis: ( g in the carrier' of (1GateCircStr (p,f)) implies for p being FinSequence st p = the Arity of (1GateCircStr (p,f)) . g holds
ex f being Function of ((len p) -tuples_on BOOLEAN),BOOLEAN st g = [(g `1),f] )
A1: len p = n by CARD_1:def_7;
A2: the Arity of (1GateCircStr (p,f)) . [p,f] = p by Def6;
assume  g in the carrier' of (1GateCircStr (p,f)) ; ::_thesis: for p being FinSequence st p = the Arity of (1GateCircStr (p,f)) . g holds
ex f being Function of ((len p) -tuples_on BOOLEAN),BOOLEAN st g = [(g `1),f]
then A3: g = [p,f] by Th41;
let q be FinSequence; ::_thesis: ( q = the Arity of (1GateCircStr (p,f)) . g implies ex f being Function of ((len q) -tuples_on BOOLEAN),BOOLEAN st g = [(g `1),f] )
assume  q = the Arity of (1GateCircStr (p,f)) . g ; ::_thesis: ex f being Function of ((len q) -tuples_on BOOLEAN),BOOLEAN st g = [(g `1),f]
then reconsider f = f as Function of ((len q) -tuples_on BOOLEAN),BOOLEAN by A3, A2, A1;
take  f ; ::_thesis: g = [(g `1),f]
thus  g = [(g `1),f] by A3, MCART_1:7; ::_thesis: verum
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
set p = the FinSeqLen of 0 ;
set f = the Function of (0 -tuples_on BOOLEAN),BOOLEAN;
take  1GateCircStr ( the FinSeqLen of 0 , the Function of (0 -tuples_on BOOLEAN),BOOLEAN) ; ::_thesis: ( 1GateCircStr ( the FinSeqLen of 0 , the Function of (0 -tuples_on BOOLEAN),BOOLEAN) is gate`2isBoolean & not 1GateCircStr ( the FinSeqLen of 0 , the Function of (0 -tuples_on BOOLEAN),BOOLEAN) is empty )
thus  ( 1GateCircStr ( the FinSeqLen of 0 , the Function of (0 -tuples_on BOOLEAN),BOOLEAN) is gate`2isBoolean & not 1GateCircStr ( the FinSeqLen of 0 , the Function of (0 -tuples_on BOOLEAN),BOOLEAN) is empty ) ; ::_thesis: verum
end;
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 ) )
proof
let n be Nat; ::_thesis: 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 ) )
let X be non empty set ; ::_thesis: 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 ) )
let f be Function of (n -tuples_on X),X; ::_thesis: 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 ) )
let p be FinSeqLen of n; ::_thesis: ( 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 ) )
set S = 1GateCircStr (p,f);
set A = 1GateCircuit (p,f);
 the Charact of (1GateCircuit (p,f)) . [p,f] = f by Def13;
then A1: for x being set st x in {[p,f]} holds
the Charact of (1GateCircuit (p,f)) . x = f by TARSKI:def_1;
 the carrier' of (1GateCircStr (p,f)) = {[p,f]} by Def6;
then  dom the Charact of (1GateCircuit (p,f)) = {[p,f]} by PARTFUN1:def_2;
hence  the Charact of (1GateCircuit (p,f)) = (p,f) .--> f by A1, FUNCOP_1:11; ::_thesis: for v being Vertex of (1GateCircStr (p,f)) holds the Sorts of (1GateCircuit (p,f)) . v = X
let v be Vertex of (1GateCircStr (p,f)); ::_thesis: the Sorts of (1GateCircuit (p,f)) . v = X
 the Sorts of (1GateCircuit (p,f)) = the carrier of (1GateCircStr (p,f)) --> X by Def13;
hence  the Sorts of (1GateCircuit (p,f)) . v = X by FUNCOP_1:7; ::_thesis: verum
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
let i be set ; :: according to FINSET_1:def_5,MSAFREE2:def_11 ::_thesis: ( not i in the carrier of (1GateCircStr (p,f)) or the Sorts of (1GateCircuit (p,f)) . i is finite )
set S = 1GateCircStr (p,f);
assume  i in the carrier of (1GateCircStr (p,f)) ; ::_thesis: the Sorts of (1GateCircuit (p,f)) . i is finite
hence  the Sorts of (1GateCircuit (p,f)) . i is finite by Th54; ::_thesis: verum
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
let n be Nat; ::_thesis: 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)
let X be non empty set ; ::_thesis: 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)
let f be Function of (n -tuples_on X),X; ::_thesis: for p, q being FinSeqLen of n holds 1GateCircuit (p,f) tolerates 1GateCircuit (q,f)
let p, q be FinSeqLen of n; ::_thesis: 1GateCircuit (p,f) tolerates 1GateCircuit (q,f)
set S1 = 1GateCircStr (p,f);
set S2 = 1GateCircStr (q,f);
set A1 = 1GateCircuit (p,f);
set A2 = 1GateCircuit (q,f);
thus  1GateCircStr (p,f) tolerates 1GateCircStr (q,f) by Th43; :: according to CIRCCOMB:def_3 ::_thesis: ( the Sorts of (1GateCircuit (p,f)) tolerates the Sorts of (1GateCircuit (q,f)) & the Charact of (1GateCircuit (p,f)) tolerates the Charact of (1GateCircuit (q,f)) )
A1: the Sorts of (1GateCircuit (q,f)) = the carrier of (1GateCircStr (q,f)) --> X by Def13;
 the Sorts of (1GateCircuit (p,f)) = the carrier of (1GateCircStr (p,f)) --> X by Def13;
hence  the Sorts of (1GateCircuit (p,f)) tolerates the Sorts of (1GateCircuit (q,f)) by A1, FUNCOP_1:87; ::_thesis: the Charact of (1GateCircuit (p,f)) tolerates the Charact of (1GateCircuit (q,f))
A2: the Charact of (1GateCircuit (q,f)) = (q,f) .--> f by Th54;
 the Charact of (1GateCircuit (p,f)) = (p,f) .--> f by Th54;
hence  the Charact of (1GateCircuit (p,f)) tolerates the Charact of (1GateCircuit (q,f)) by A2, FUNCOP_1:87; ::_thesis: verum
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
let n be Nat; ::_thesis: 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)
let X be non empty finite set ; ::_thesis: 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)
let f be Function of (n -tuples_on X),X; ::_thesis: for p being FinSeqLen of n
for s being State of (1GateCircuit (p,f)) holds (Following s) . [p,f] = f . (s * p)
let p be FinSeqLen of n; ::_thesis: for s being State of (1GateCircuit (p,f)) holds (Following s) . [p,f] = f . (s * p)
let s be State of (1GateCircuit (p,f)); ::_thesis: (Following s) . [p,f] = f . (s * p)
set S = 1GateCircStr (p,f);
set A = 1GateCircuit (p,f);
set IV = InnerVertices (1GateCircStr (p,f));
 InnerVertices (1GateCircStr (p,f)) = {[p,f]} by Th42;
then reconsider v = [p,f] as Element of InnerVertices (1GateCircStr (p,f)) by TARSKI:def_1;
 the carrier' of (1GateCircStr (p,f)) = {[p,f]} by Def6;
then reconsider o = [p,f] as Gate of (1GateCircStr (p,f)) by TARSKI:def_1;
 the_result_sort_of o = v by Def6;
then A1: action_at v = o by MSAFREE2:def_7;
 the_arity_of o = p by Def6;
then A2: o depends_on_in s = s * p by CIRCUIT1:def_3;
 (Following s) . v = (Den ((action_at v),(1GateCircuit (p,f)))) . ((action_at v) depends_on_in s) by CIRCUIT2:def_5;
hence  (Following s) . [p,f] = f . (s * p) by A1, A2, Def13; ::_thesis: verum
end;

begin

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 )
proof
let S be non empty ManySortedSign ; ::_thesis: for A being MSAlgebra over S holds
( A is Boolean iff the Sorts of A = the carrier of S --> BOOLEAN )
let A be MSAlgebra over S; ::_thesis: ( A is Boolean iff the Sorts of A = the carrier of S --> BOOLEAN )
A1: dom the Sorts of A = the carrier of S by PARTFUN1:def_2;
thus  ( A is Boolean implies the Sorts of A = the carrier of S --> BOOLEAN ) ::_thesis: ( the Sorts of A = the carrier of S --> BOOLEAN implies A is Boolean )
proof
assume  for v being Vertex of S holds the Sorts of A . v = BOOLEAN ; :: according to CIRCCOMB:def_14 ::_thesis: the Sorts of A = the carrier of S --> BOOLEAN
then  for v being set st v in the carrier of S holds
the Sorts of A . v = BOOLEAN ;
hence  the Sorts of A = the carrier of S --> BOOLEAN by A1, FUNCOP_1:11; ::_thesis: verum
end;
assume A2: the Sorts of A = the carrier of S --> BOOLEAN ; ::_thesis: A is Boolean
let v be Vertex of S; :: according to CIRCCOMB:def_14 ::_thesis: the Sorts of A . v = BOOLEAN
thus  the Sorts of A . v = BOOLEAN by A2, FUNCOP_1:7; ::_thesis: verum
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
let A be MSAlgebra over S; ::_thesis: ( A is Boolean implies ( A is non-empty & A is finite-yielding ) )
assume A1: A is Boolean ; ::_thesis: ( A is non-empty & A is finite-yielding )
then  the Sorts of A = the carrier of S --> BOOLEAN by Th57;
hence  A is non-empty by MSUALG_1:def_3; ::_thesis: A is finite-yielding
let v be set ; :: according to FINSET_1:def_5,MSAFREE2:def_11 ::_thesis: ( not v in the carrier of S or the Sorts of A . v is finite )
thus  ( not v in the carrier of S or the Sorts of A . v is finite ) by A1, Def14; ::_thesis: verum
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
let S be non empty ManySortedSign ; ::_thesis: for A being MSAlgebra over S holds
( A is Boolean iff rng the Sorts of A c= {BOOLEAN} )
let A be MSAlgebra over S; ::_thesis: ( A is Boolean iff rng the Sorts of A c= {BOOLEAN} )
hereby  ::_thesis: ( rng the Sorts of A c= {BOOLEAN} implies A is Boolean )
assume  A is Boolean ; ::_thesis: rng the Sorts of A c= {BOOLEAN}
then  the Sorts of A = the carrier of S --> BOOLEAN by Th57;
hence  rng the Sorts of A c= {BOOLEAN} by FUNCOP_1:13; ::_thesis: verum
end;
assume A1: rng the Sorts of A c= {BOOLEAN} ; ::_thesis: A is Boolean
let v be Vertex of S; :: according to CIRCCOMB:def_14 ::_thesis: the Sorts of A . v = BOOLEAN
 dom the Sorts of A = the carrier of S by PARTFUN1:def_2;
then  the Sorts of A . v in rng the Sorts of A by FUNCT_1:def_3;
hence  the Sorts of A . v = BOOLEAN by A1, TARSKI:def_1; ::_thesis: verum
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
let S1, S2 be non empty ManySortedSign ; ::_thesis: 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
let A1 be MSAlgebra over S1; ::_thesis: for A2 being MSAlgebra over S2 st A1 is Boolean & A2 is Boolean holds
the Sorts of A1 tolerates the Sorts of A2
let A2 be MSAlgebra over S2; ::_thesis: ( A1 is Boolean & A2 is Boolean implies the Sorts of A1 tolerates the Sorts of A2 )
assume that
A1: A1 is Boolean and
A2: A2 is Boolean ; ::_thesis: the Sorts of A1 tolerates the Sorts of A2
A3: the Sorts of A2 = the carrier of S2 --> BOOLEAN by A2, Th57;
 the Sorts of A1 = the carrier of S1 --> BOOLEAN by A1, Th57;
hence  the Sorts of A1 tolerates the Sorts of A2 by A3, FUNCOP_1:87; ::_thesis: verum
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
let S1, S2 be non empty unsplit gate`1=arity ManySortedSign ; ::_thesis: 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
let A1 be MSAlgebra over S1; ::_thesis: 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
let A2 be MSAlgebra over S2; ::_thesis: ( A1 is Boolean & A1 is gate`2=den & A2 is Boolean & A2 is gate`2=den implies A1 tolerates A2 )
assume that
A1: ( A1 is Boolean & A1 is gate`2=den ) and
A2: ( A2 is Boolean & A2 is gate`2=den ) ; ::_thesis: A1 tolerates A2
thus  ( S1 tolerates S2 & the Sorts of A1 tolerates the Sorts of A2 & the Charact of A1 tolerates the Charact of A2 ) by A1, A2, Th47, Th48, Th59; :: according to CIRCCOMB:def_3 ::_thesis: verum
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
deffunc H1( set , Element of the carrier of S * ) ->  Element of K19(K20(((len c2) -tuples_on BOOLEAN),BOOLEAN)) = ((len c2) -tuples_on BOOLEAN) --> FALSE;
A1: for g being set
for p being Element of the carrier of S * st g in the carrier' of S & p = the Arity of S . g holds
H1(g,p) is Function of ((len p) -tuples_on BOOLEAN),BOOLEAN ;
consider A being strict MSAlgebra over S such that
A2: ( the Sorts of A = the carrier of S --> BOOLEAN & ( for g being set
for p being Element of the carrier of S * st g in the carrier' of S & p = the Arity of S . g holds
the Charact of A . g = H1(g,p) ) ) from CIRCCOMB:sch_2(A1);
take  A ; ::_thesis: A is Boolean
let v be Vertex of S; :: according to CIRCCOMB:def_14 ::_thesis: the Sorts of A . v = BOOLEAN
thus  the Sorts of A . v = BOOLEAN by A2, FUNCOP_1:7; ::_thesis: verum
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
let n be Nat; ::_thesis: for f being Function of (n -tuples_on BOOLEAN),BOOLEAN
for p being FinSeqLen of n holds 1GateCircuit (p,f) is Boolean
let f be Function of (n -tuples_on BOOLEAN),BOOLEAN; ::_thesis: for p being FinSeqLen of n holds 1GateCircuit (p,f) is Boolean
let p be FinSeqLen of n; ::_thesis: 1GateCircuit (p,f) is Boolean
set S = 1GateCircStr (p,f);
set A = 1GateCircuit (p,f);
let v be Vertex of (1GateCircStr (p,f)); :: according to CIRCCOMB:def_14 ::_thesis: the Sorts of (1GateCircuit (p,f)) . v = BOOLEAN
 the Sorts of (1GateCircuit (p,f)) = the carrier of (1GateCircStr (p,f)) --> BOOLEAN by Def13;
hence  the Sorts of (1GateCircuit (p,f)) . v = BOOLEAN by FUNCOP_1:7; ::_thesis: verum
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
let S1, S2 be non empty ManySortedSign ; ::_thesis: for A1 being Boolean MSAlgebra over S1
for A2 being Boolean MSAlgebra over S2 holds A1 +* A2 is Boolean
let A1 be Boolean MSAlgebra over S1; ::_thesis: for A2 being Boolean MSAlgebra over S2 holds A1 +* A2 is Boolean
let A2 be Boolean MSAlgebra over S2; ::_thesis: A1 +* A2 is Boolean
set A = A1 +* A2;
set S = S1 +* S2;
A1: dom the Sorts of A1 = the carrier of S1 by PARTFUN1:def_2;
let x be Vertex of (S1 +* S2); :: according to CIRCCOMB:def_14 ::_thesis: the Sorts of (A1 +* A2) . x = BOOLEAN
A2: dom the Sorts of A2 = the carrier of S2 by PARTFUN1:def_2;
 the carrier of (S1 +* S2) = the carrier of S1 \/ the carrier of S2 by Def2;
then A3: ( x in the carrier of S1 or x in the carrier of S2 ) by XBOOLE_0:def_3;
A4: the Sorts of A2 = the carrier of S2 --> BOOLEAN by Th57;
A5: the Sorts of A1 = the carrier of S1 --> BOOLEAN by Th57;
then A6: the Sorts of A1 tolerates the Sorts of A2 by A4, FUNCOP_1:87;
then  the Sorts of (A1 +* A2) = the Sorts of A1 +* the Sorts of A2 by Def4;
then  ( ( the Sorts of (A1 +* A2) . x = the Sorts of A1 . x & the Sorts of A1 . x = BOOLEAN ) or ( the Sorts of (A1 +* A2) . x = the Sorts of A2 . x & the Sorts of A2 . x = BOOLEAN ) ) by A5, A4, A6, A1, A2, A3, FUNCOP_1:7, FUNCT_4:13, FUNCT_4:15;
hence  the Sorts of (A1 +* A2) . x = BOOLEAN ; ::_thesis: verum
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
let S1, S2 be non empty ManySortedSign ; ::_thesis: 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
let A1 be non-empty MSAlgebra over S1; ::_thesis: 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
let A2 be non-empty MSAlgebra over S2; ::_thesis: ( A1 is gate`2=den & A2 is gate`2=den & the Sorts of A1 tolerates the Sorts of A2 implies A1 +* A2 is gate`2=den )
set A = A1 +* A2;
set S = S1 +* S2;
assume that
A1: A1 is gate`2=den and
A2: A2 is gate`2=den and
A3: the Sorts of A1 tolerates the Sorts of A2 ; ::_thesis: A1 +* A2 is gate`2=den
A4: the Charact of (A1 +* A2) = the Charact of A1 +* the Charact of A2 by A3, Def4;
let g be set ; :: according to CIRCCOMB:def_10 ::_thesis: ( g in the carrier' of (S1 +* S2) implies g = [(g `1),( the Charact of (A1 +* A2) . g)] )
A5: dom the Charact of A1 = the carrier' of S1 by PARTFUN1:def_2;
A6: dom the Charact of A2 = the carrier' of S2 by PARTFUN1:def_2;
A7: the carrier' of (S1 +* S2) = the carrier' of S1 \/ the carrier' of S2 by Def2;
assume  g in the carrier' of (S1 +* S2) ; ::_thesis: g = [(g `1),( the Charact of (A1 +* A2) . g)]
then A8: ( g in the carrier' of S1 or g in the carrier' of S2 ) by A7, XBOOLE_0:def_3;
 the Charact of A1 tolerates the Charact of A2 by A1, A2, Th48;
then  ( ( the Charact of (A1 +* A2) . g = the Charact of A1 . g & [(g `1),( the Charact of A1 . g)] = g ) or ( the Charact of (A1 +* A2) . g = the Charact of A2 . g & [(g `1),( the Charact of A2 . g)] = g ) ) by A1, A2, A4, A5, A6, A8, Def10, FUNCT_4:13, FUNCT_4:15;
hence  g = [(g `1),( the Charact of (A1 +* A2) . g)] ; ::_thesis: verum
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
set p = the FinSeqLen of 1;
set f = the Function of (1 -tuples_on BOOLEAN),BOOLEAN;
take  1GateCircStr ( the FinSeqLen of 1, the Function of (1 -tuples_on BOOLEAN),BOOLEAN) ; ::_thesis: ( 1GateCircStr ( the FinSeqLen of 1, the Function of (1 -tuples_on BOOLEAN),BOOLEAN) is unsplit & 1GateCircStr ( the FinSeqLen of 1, the Function of (1 -tuples_on BOOLEAN),BOOLEAN) is gate`1=arity & 1GateCircStr ( the FinSeqLen of 1, the Function of (1 -tuples_on BOOLEAN),BOOLEAN) is gate`2=den & 1GateCircStr ( the FinSeqLen of 1, the Function of (1 -tuples_on BOOLEAN),BOOLEAN) is gate`2isBoolean & not 1GateCircStr ( the FinSeqLen of 1, the Function of (1 -tuples_on BOOLEAN),BOOLEAN) is void & 1GateCircStr ( the FinSeqLen of 1, the Function of (1 -tuples_on BOOLEAN),BOOLEAN) is strict )
thus  ( 1GateCircStr ( the FinSeqLen of 1, the Function of (1 -tuples_on BOOLEAN),BOOLEAN) is unsplit & 1GateCircStr ( the FinSeqLen of 1, the Function of (1 -tuples_on BOOLEAN),BOOLEAN) is gate`1=arity & 1GateCircStr ( the FinSeqLen of 1, the Function of (1 -tuples_on BOOLEAN),BOOLEAN) is gate`2=den & 1GateCircStr ( the FinSeqLen of 1, the Function of (1 -tuples_on BOOLEAN),BOOLEAN) is gate`2isBoolean & not 1GateCircStr ( the FinSeqLen of 1, the Function of (1 -tuples_on BOOLEAN),BOOLEAN) is void & 1GateCircStr ( the FinSeqLen of 1, the Function of (1 -tuples_on BOOLEAN),BOOLEAN) is strict ) ; ::_thesis: verum
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
deffunc H1( set , set ) ->  set = S `2 ;
A1: now__::_thesis:_for_g_being_set_
for_p_being_Element_of_the_carrier_of_S_*_st_g_in_the_carrier'_of_S_&_p_=_the_Arity_of_S_._g_holds_
H1(g,p)_is_Function_of_((len_p)_-tuples_on_BOOLEAN),BOOLEAN
let g be set ; ::_thesis: for p being Element of the carrier of S * st g in the carrier' of S & p = the Arity of S . g holds
H1(g,p) is Function of ((len p) -tuples_on BOOLEAN),BOOLEAN
let p be Element of the carrier of S * ; ::_thesis: ( g in the carrier' of S & p = the Arity of S . g implies H1(g,p) is Function of ((len p) -tuples_on BOOLEAN),BOOLEAN )
assume that
A2: g in the carrier' of S and
A3: p = the Arity of S . g ; ::_thesis: H1(g,p) is Function of ((len p) -tuples_on BOOLEAN),BOOLEAN
 ex f being Function of ((len p) -tuples_on BOOLEAN),BOOLEAN st g = [(g `1),f] by A2, A3, Def9;
hence  H1(g,p) is Function of ((len p) -tuples_on BOOLEAN),BOOLEAN by MCART_1:7; ::_thesis: verum
end;
consider A being strict MSAlgebra over S such that
A4: ( the Sorts of A = the carrier of S --> BOOLEAN & ( for g being set
for p being Element of the carrier of S * st g in the carrier' of S & p = the Arity of S . g holds
the Charact of A . g = H1(g,p) ) ) from CIRCCOMB:sch_2(A1);
take  A ; ::_thesis: ( A is Boolean & A is gate`2=den )
thus  A is Boolean ::_thesis: A is gate`2=den
proof
let v be Vertex of S; :: according to CIRCCOMB:def_14 ::_thesis: the Sorts of A . v = BOOLEAN
thus  the Sorts of A . v = BOOLEAN by A4, FUNCOP_1:7; ::_thesis: verum
end;
let g be set ; :: according to CIRCCOMB:def_10 ::_thesis: ( g in the carrier' of S implies g = [(g `1),( the Charact of A . g)] )
assume A5: g in the carrier' of S ; ::_thesis: g = [(g `1),( the Charact of A . g)]
then reconsider p = the Arity of S . g as Element of the carrier of S * by FUNCT_2:5;
consider f being Function of ((len p) -tuples_on BOOLEAN),BOOLEAN such that
A6: g = [(g `1),f] by A5, Def9;
 g `2 = f by A6, MCART_1:7;
hence  g = [(g `1),( the Charact of A . g)] by A4, A5, A6; ::_thesis: verum
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;
clusterA1 +* A2 ->  strict non-empty gate`2=den Boolean ;
coherence
 ( A1 +* A2 is Boolean & A1 +* A2 is gate`2=den )
proof
 the Sorts of A1 tolerates the Sorts of A2 by Th59;
hence  ( A1 +* A2 is Boolean & A1 +* A2 is gate`2=den ) by Th62, Th63; ::_thesis: verum
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
take  1GateCircuit (p,f) ; ::_thesis: ( 1GateCircuit (p,f) is gate`2=den & 1GateCircuit (p,f) is strict & 1GateCircuit (p,f) is non-empty )
thus  ( 1GateCircuit (p,f) is gate`2=den & 1GateCircuit (p,f) is strict & 1GateCircuit (p,f) is non-empty ) ; ::_thesis: verum
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
let S1, S2 be non empty non void unsplit gate`1=arity gate`2isBoolean ManySortedSign ; ::_thesis: 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 ) )
let A1 be gate`2=den Boolean Circuit of S1; ::_thesis: 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 ) )
let A2 be gate`2=den Boolean Circuit of S2; ::_thesis: 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 ) )
 A1 tolerates A2 by Th60;
hence  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 ) ) by Th31; ::_thesis: verum
end;