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