:: Combining of Circuits
:: by Yatsuka Nakamura and Grzegorz Bancerek
::
:: Received May 11, 1995
:: Copyright (c) 1995-2017 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies MSUALG_1, SUBSET_1, STRUCT_0, NUMBERS, XBOOLE_0, CARD_3,
FINSEQ_1, FUNCOP_1, FINSEQ_2, PBOOLE, FUNCT_4, RELAT_1, PARTFUN1,
FUNCT_1, TARSKI, MSAFREE2, FINSET_1, GLIB_000, MARGREL1, CIRCUIT1, FSM_1,
CIRCUIT2, MCART_1, NAT_1, CARD_1, LATTICES, XBOOLEAN, CIRCCOMB;
notations TARSKI, XBOOLE_0, XTUPLE_0, SUBSET_1, CARD_1, ORDINAL1, NUMBERS,
MCART_1, RELAT_1, FUNCT_1, FINSEQ_1, FINSEQ_2, FINSET_1, FUNCT_2,
FUNCOP_1, PARTFUN1, FUNCT_4, CARD_3, MARGREL1, PBOOLE, STRUCT_0,
MSUALG_1, MSAFREE2, CIRCUIT1, CIRCUIT2;
constructors MARGREL1, CIRCUIT1, CIRCUIT2, RELSET_1, XTUPLE_0, NUMBERS;
registrations XBOOLE_0, RELAT_1, FUNCT_1, ORDINAL1, FUNCOP_1, FINSET_1,
FINSEQ_1, MARGREL1, CARD_3, PBOOLE, STRUCT_0, MSUALG_1, MSUALG_2,
MSAFREE2, FUNCT_4, RELSET_1, FINSEQ_2, XTUPLE_0;
requirements NUMERALS, BOOLE, SUBSET;
definitions TARSKI, PARTFUN1, FINSET_1, MSAFREE2, STRUCT_0, XBOOLE_0,
FUNCOP_1, PBOOLE;
equalities TARSKI, MSUALG_1, MSAFREE2, FUNCOP_1, MARGREL1;
expansions TARSKI, PARTFUN1, MSUALG_1, XBOOLE_0;
theorems TARSKI, ZFMISC_1, FINSEQ_1, FINSEQ_2, MSUALG_1, FUNCT_1, FUNCT_2,
FUNCT_4, PBOOLE, GRFUNC_1, FUNCOP_1, PARTFUN1, RELAT_1, MSAFREE2,
CIRCUIT1, CIRCUIT2, CARD_3, MONOID_1, RELSET_1, XBOOLE_0, XBOOLE_1,
CARD_1, FINSEQ_3, XTUPLE_0, XREGULAR;
schemes FUNCT_1;
begin :: Combining of ManySortedSign's
definition
let S be ManySortedSign;
mode Gate of S is Element of the carrier' of S;
end;
Lm1: now
let i be Element of NAT, X be non empty set;
thus product ((Seg i) --> X) = product (i |-> X) by FINSEQ_2:def 2
.= i-tuples_on X by FINSEQ_3:131;
end;
registration
let A,B be set;
let f be ManySortedSet of A;
let g be ManySortedSet of B;
cluster f+*g -> A \/ B-defined;
coherence
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 thesis by RELAT_1:def 18;
end;
end;
registration
let A,B be set;
let f be ManySortedSet of A;
let g be ManySortedSet of B;
cluster f+*g -> total for A \/ B-defined Function;
coherence
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 thesis;
end;
end;
registration
let A,B be set;
cluster A .--> B -> {A}-defined;
coherence;
end;
registration
let A,B be set;
cluster A .--> B -> total for {A}-defined Function;
coherence;
end;
registration
let A be set, B be non empty set;
cluster A .--> B -> non-empty;
coherence;
end;
theorem Th1:
for A,B being set, 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, f be ManySortedSet of A;
let g be ManySortedSet of B;
assume
A1: f c= 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 object;
A5: dom f = A by PARTFUN1:def 2;
assume
A6: z in f#;
then consider x,y being object such that
A7: [x,y] = z by RELAT_1:def 1;
dom (f# ) = A* by PARTFUN1:def 2;
then reconsider 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;
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,79
.= g#.x9 by FINSEQ_2:def 5;
hence z in g# by A7,A4,FUNCT_1:1;
end;
theorem Th2:
for X being set, Y being non empty set, p being FinSequence of X
holds (X --> Y)#.p = (len p)-tuples_on Y
proof
let X be set, Y be non empty set, p be FinSequence of X;
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;
end;
definition
let A be set;
let f1,g1 be non-empty ManySortedSet of A;
let B be set;
let f2,g2 be non-empty ManySortedSet of B;
let h1 be ManySortedFunction of f1,g1;
let h2 be ManySortedFunction of f2,g2;
redefine func h1+*h2 -> ManySortedFunction of f1+*f2, g1+*g2;
coherence
proof
set f = f1+*f2, g = g1+*g2, 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 as ManySortedFunction of A \/ B;
A6: dom f1 = A by PARTFUN1:def 2;
h is ManySortedFunction of f, g
proof
let x be object;
A7: not x in B or x in B;
assume
A8: x in A \/ B;
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 & f.x = f1.x & g.x = g1
.x or h.x = h2.x & h2.x is Function of f2.x, g2.x & f.x = f2.x & g.x = g2.x by
A6,A1,A5,A2,A3,A4,A8,A7,FUNCT_4:def 1,PBOOLE:def 15;
hence thesis;
end;
hence thesis;
end;
end;
definition
let S1,S2 be ManySortedSign;
pred S1 tolerates S2 means
the Arity of S1 tolerates the Arity of S2 & the
ResultSort of S1 tolerates the ResultSort of S2;
reflexivity;
symmetry;
end;
definition
let S1,S2 be non empty ManySortedSign;
func S1 +* S2 -> strict non empty ManySortedSign means
:Def2:
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
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 RESULT = OPER 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;
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;
then
A6: rng (the ResultSort of S1) \/ rng (the ResultSort of S2) c= CARR by A5,
XBOOLE_1:8;
rng RESULT c= rng (the ResultSort of S1) \/ rng (the ResultSort of S2
) by FUNCT_4:17;
then rng RESULT c= CARR by A6;
then reconsider RESULT as Function of OPER, 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 ARITY = OPER 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;
(the carrier of S1)* c= CARR* by FINSEQ_1:62,XBOOLE_1:7;
then rng (the Arity of S1) c= CARR* by A9;
then
A12: rng (the Arity of S1) \/ rng (the Arity of S2) c= CARR* by A11,XBOOLE_1:8;
rng ARITY c= rng (the Arity of S1) \/ rng (the Arity of S2) by FUNCT_4:17;
then rng ARITY c= CARR* by A12;
then reconsider ARITY as Function of OPER, CARR* by A8,FUNCT_2:def 1
,RELSET_1:4;
take ManySortedSign(#CARR, OPER, ARITY, RESULT#);
thus thesis;
end;
uniqueness;
end;
theorem Th3:
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 such 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;
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;
the ResultSort of S1+*S2 = (the ResultSort of S1)+*the ResultSort of S2
by Def2;
hence thesis by A2,A4,A6,FUNCT_4:125;
end;
theorem
for S being non empty ManySortedSign holds S+*S = the ManySortedSign of S
proof
let S be non empty ManySortedSign;
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 thesis by A1,A2,A3,Def2;
end;
theorem Th5:
for S1,S2 being non empty ManySortedSign st S1 tolerates S2 holds
S1+*S2 = S2+*S1
proof
let S1,S2 be non empty ManySortedSign;
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;
A3: the carrier' of S = (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 S = (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 S = (the Arity of S2) +* (the Arity of S1) by Def2;
the carrier of S = (the carrier of S1) \/ (the carrier of S2) by Def2;
hence thesis by A3,A5,A4,Def2;
end;
theorem
for S1,S2,S3 being non empty ManySortedSign holds (S1+*S2)+*S3 = S1+*(
S2+*S3 )
proof
let S1,S2,S3 be non empty ManySortedSign;
set S12 = S1+*S2, S23 = S2+*S3;
set S1293 = S12+*S3, S1923 = S1+*S23;
A1: the carrier of S23 = (the carrier of S2) \/ (the carrier of S3) by Def2;
A2: the carrier of S1293 = (the carrier of S12) \/ (the carrier of S3) by Def2;
A3: the carrier of S1923 = (the carrier of S1) \/ (the carrier of S23) by Def2;
the carrier of S12 = (the carrier of S1) \/ (the carrier of S2) by Def2;
then
A4: the carrier of S1293 = the carrier of S1923 by A1,A2,A3,XBOOLE_1:4;
A5: the carrier' of S23 = (the carrier' of S2) \/ the carrier' of S3 by Def2;
A6: the carrier' of S1293 = (the carrier' of S12) \/ the carrier' of S3 by Def2
;
A7: the Arity of S23 = (the Arity of S2) +* (the Arity of S3) by Def2;
A8: the Arity of S1923 = (the Arity of S1) +* (the Arity of S23) by Def2;
A9: the carrier' of S1923 = (the carrier' of S1) \/ the carrier' of S23 by Def2
;
the carrier' of S12 = (the carrier' of S1) \/ the carrier' of S2 by Def2;
then
A10: the carrier' of S1293 = the carrier' of S1923 by A5,A6,A9,XBOOLE_1:4;
A11: the ResultSort of S1923 = (the ResultSort of S1)+*the ResultSort of S23
by Def2;
A12: the ResultSort of S1293 = (the ResultSort of S12)+*the ResultSort of S3
by Def2;
A13: the Arity of S1293 = (the Arity of S12) +* (the Arity of S3) by Def2;
the Arity of S12 = (the Arity of S1) +* (the Arity of S2) by Def2;
then
A14: the Arity of S1293 = the Arity of S1923 by A7,A13,A8,FUNCT_4:14;
A15: the ResultSort of S23 = (the ResultSort of S2)+*the ResultSort of S3 by
Def2;
the ResultSort of S12 = (the ResultSort of S1)+*the ResultSort of S2 by Def2;
hence thesis by A15,A12,A11,A4,A10,A14,FUNCT_4:14;
end;
theorem
for f being one-to-one Function for S1,S2 being Circuit-like non
empty 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;
let S1,S2 be Circuit-like non empty ManySortedSign such that
A1: the ResultSort of S1 c= f and
A2: the ResultSort of S2 c= f;
let S be non void non empty ManySortedSign;
set r1 = the ResultSort of S1, r2 =the ResultSort of S2;
set r = the ResultSort of S;
A3: r1+*r2 c= r1 \/ r2 by FUNCT_4:29;
assume S = S1+*S2;
then
A4: r = r1+*r2 by Def2;
r1 \/ r2 c= f by A1,A2,XBOOLE_1:8;
then
A5: r1+*r2 c= f by A3;
then
A6: dom r c= dom f by A4,GRFUNC_1:2;
let o1, o2 be Gate of S;
A7: dom r = the carrier' of S by FUNCT_2:def 1;
then
A8: o1 in dom r;
A9: o2 in dom r by A7;
assume
A10: the_result_sort_of o1 = the_result_sort_of o2;
A11: r.o2 = f.o2 by A4,A7,A5,GRFUNC_1:2;
r.o1 = f.o1 by A4,A7,A5,GRFUNC_1:2;
hence thesis by A10,A8,A9,A11,A6,FUNCT_1:def 4;
end;
theorem
for S1,S2 being Circuit-like non empty ManySortedSign st
InnerVertices S1 misses InnerVertices S2 holds S1+*S2 is Circuit-like
proof
let S1,S2 be Circuit-like non empty ManySortedSign;
assume
A1: InnerVertices S1 misses InnerVertices S2;
set r1 = the ResultSort of S1, r2 = the ResultSort of S2;
let S be non void non empty ManySortedSign;
set r = the ResultSort of S;
A2: dom r1 = the carrier' of S1 by FUNCT_2:def 1;
assume
A3: S = S1+*S2;
then
A4: r = r1+*r2 by Def2;
A5: dom r2 = the carrier' of S2 by FUNCT_2:def 1;
let o1, o2 be Gate of S;
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: r.o1 = r1.o1 & r1.o1 in rng r1 & o1 in the carrier' of S1 or r.o1 = r2.
o1 & r2.o1 in rng r2 & 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: r.o2 = r1.o2 & r1.o2 in rng r1 & o2 in the carrier' of S1 or r.o2 = r2.
o2 & r2.o2 in rng r2 & 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;
per cases by A1,A9,A7,A8,XBOOLE_0:3;
suppose
A10: r.o1 = r1.o1 & o1 in the carrier' of S1 & r.o2 = r1.o2 & o2 in
the carrier' of S1;
then reconsider
S = S1 as non void Circuit-like non empty ManySortedSign;
reconsider p1 = o1, p2 = o2 as Gate of S by A10;
A11: the_result_sort_of p2 = r1.p2;
the_result_sort_of p1 = r1.p1;
hence thesis by A9,A10,A11,MSAFREE2:def 6;
end;
suppose
A12: r.o1 = r2.o1 & o1 in the carrier' of S2 & r.o2 = r2.o2 & o2 in
the carrier' of S2;
then reconsider
S = S2 as non void Circuit-like non empty ManySortedSign;
reconsider p1 = o1, p2 = o2 as Gate of S by A12;
A13: the_result_sort_of p2 = r2.p2;
the_result_sort_of p1 = r2.p1;
hence thesis by A9,A12,A13,MSAFREE2:def 6;
end;
end;
theorem Th9:
for S1,S2 being non empty ManySortedSign st S1 is not void or S2
is not void holds S1+*S2 is non void
proof
let S1,S2 be non empty ManySortedSign;
assume
A1: S1 is not void or S2 is not void;
the carrier' of S1+*S2 = (the carrier' of S1) \/ the carrier' of S2 by Def2;
hence the carrier' of S1+*S2 is non empty by A1;
end;
theorem
for S1,S2 being finite non empty ManySortedSign holds S1+*S2 is finite
proof
let S1,S2 be finite non empty ManySortedSign;
reconsider C1 = the carrier of S1, C2 = the carrier of S2 as finite set;
the carrier of S1+*S2 = C1 \/ C2 by Def2;
hence thesis;
end;
registration
let S1 be non void non empty ManySortedSign;
let S2 be non empty ManySortedSign;
cluster S1 +* S2 -> non void;
coherence by Th9;
cluster S2 +* S1 -> non void;
coherence by Th9;
end;
::theorem
:: for S1,S2 being monotonic (non void ManySortedSign) st
:: InputVertices S1 misses InnerVertices S2 or
:: InputVertices S2 misses InnerVertices S1
:: holds S1+*S2 is monotonic;
theorem Th11:
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;
set R1 = the ResultSort of S1, R2 = the ResultSort of S2;
assume that
the Arity of S1 tolerates the Arity of S2 and
A1: R1 tolerates R2;
set S = S1+*S2, R = the ResultSort of S;
A2: R = R1+*R2 by Def2;
then R1 c= R by A1,FUNCT_4:28;
then
A3: rng R1 c= rng R by RELAT_1:11;
rng R2 c= rng R by A2,FUNCT_4:18;
then
A4: (rng R1) \/ (rng R2) c= rng R by A3,XBOOLE_1:8;
A5: rng R c= (rng R1) \/ (rng R2) by A2,FUNCT_4:17;
hence InnerVertices S = (InnerVertices S1) \/ (InnerVertices S2) by A4;
let x be object;
assume
A6: x in InputVertices S;
then
A7: not x in rng R by XBOOLE_0:def 5;
A8: rng R = (rng R1) \/ (rng R2) by A5,A4;
then
A9: not x in rng R2 by A7,XBOOLE_0:def 3;
the carrier of S = (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 R1 by A8,A7,XBOOLE_0:def 3;
then x in (the carrier of S1) \ rng R1 or x in (the carrier of S2) \ rng R2
by A10,A9,XBOOLE_0:def 5;
hence thesis by XBOOLE_0:def 3;
end;
theorem Th12:
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;
set R1 = the ResultSort of S1, R2 = the ResultSort of S2;
set S = S1+*S2, R = the ResultSort of S;
let v2 be Vertex of S2;
R = R1+*R2 by Def2;
then
A1: rng R2 c= rng R by FUNCT_4:18;
assume v2 in InputVertices S;
then not v2 in rng R2 by A1,XBOOLE_0:def 5;
hence thesis by XBOOLE_0:def 5;
end;
theorem Th13:
for S1,S2 being non empty ManySortedSign st S1 tolerates S2 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 such that
the Arity of S1 tolerates the Arity of S2 and
A1: the ResultSort of S1 tolerates the ResultSort of S2;
set S = S1+*S2, R = the ResultSort of S;
set R1 = the ResultSort of S1, R2 = the ResultSort of S2;
R = R1+*R2 by Def2;
then R1 c= R by A1,FUNCT_4:28;
then
A2: rng R1 c= rng R by RELAT_1:11;
let v1 be Vertex of S1;
assume v1 in InputVertices S;
then not v1 in rng R1 by A2,XBOOLE_0:def 5;
hence thesis by XBOOLE_0:def 5;
end;
theorem Th14:
for S1 being non empty ManySortedSign, S2 being non void non
empty ManySortedSign for o2 being OperSymbol of S2, 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;
let S2 be non void non empty ManySortedSign;
let o2 be OperSymbol of S2, o be OperSymbol of S1+*S2;
assume
A1: o2 = o;
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;
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 thesis by A1,A3,FUNCT_4:13;
end;
theorem Th15:
for S1 being non empty ManySortedSign, S2,S being Circuit-like
non void non empty ManySortedSign st S = S1+*S2 for v2 being Vertex of S2 st
v2 in InnerVertices S2 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, S2,S be Circuit-like non void non empty
ManySortedSign such that
A1: S = S1+*S2;
let v2 be Vertex of S2 such that
A2: v2 in InnerVertices S2;
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 such that
A3: v2 = v;
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;
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 thesis by A2,A3,A4,MSAFREE2:def 7;
end;
theorem Th16:
for S1 being non void non empty ManySortedSign, S2 being non
empty ManySortedSign st S1 tolerates S2 for o1 being OperSymbol of S1, 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 void non empty ManySortedSign, S2 be non empty ManySortedSign
such that
A1: the Arity of S1 tolerates the Arity of S2 and
A2: the ResultSort of S1 tolerates the ResultSort of S2;
let o1 be OperSymbol of S1, o be OperSymbol of S1+*S2;
assume
A3: o1 = o;
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;
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 thesis by A2,A3,A5,FUNCT_4:15;
end;
theorem Th17:
for S1,S being Circuit-like non void non empty ManySortedSign,
S2 being non empty ManySortedSign st S1 tolerates S2 & S = S1+*S2 for v1 being
Vertex of S1 st v1 in InnerVertices S1 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 Circuit-like non void non empty ManySortedSign, S2 be non
empty ManySortedSign such that
A1: S1 tolerates S2 and
A2: S = S1+*S2;
let v1 be Vertex of S1 such that
A3: v1 in InnerVertices S1;
let v be Vertex of S such that
A4: v1 = v;
InnerVertices S = (InnerVertices S1) \/ (InnerVertices S2) by A1,A2,Th11;
hence
A5: v in InnerVertices S by A3,A4,XBOOLE_0:def 3;
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 thesis by A5,MSAFREE2:def 7;
end;
begin :: Combining of Circuits
definition
let S1,S2 be non empty ManySortedSign;
let A1 be MSAlgebra over S1;
let A2 be MSAlgebra over S2;
pred A1 tolerates A2 means
S1 tolerates S2 & the Sorts of A1
tolerates the Sorts of A2 & the Charact of A1 tolerates the Charact of A2;
end;
definition
let S1,S2 be non empty ManySortedSign;
let A1 be non-empty MSAlgebra over S1;
let A2 be non-empty MSAlgebra over S2;
assume
A1: the Sorts of A1 tolerates the Sorts of A2;
func A1 +* A2 -> strict non-empty MSAlgebra over S1+*S2 means
:Def4:
the Sorts of it = (the Sorts of A1) +* (the Sorts of A2) &
the Charact of it = (the Charact of A1) +* (the Charact of A2);
uniqueness;
existence
proof
set CHARACT = (the Charact of A1) +* (the Charact of A2);
set SA1 = the Sorts of A1, SA2 = the Sorts of A2;
set S = S1+*S2;
set I = the carrier of S, I1 = the carrier of S1, I2 = the carrier of S2;
set SA12 = SA1#+*(SA2# );
A2: dom (SA2# ) = I2* by PARTFUN1:def 2;
A3: the ResultSort of S = (the ResultSort of S1) +* (the ResultSort of S2)
by Def2;
A4: rng the ResultSort of S2 c= I2 by RELAT_1:def 19;
A5: dom SA2 = I2 by PARTFUN1:def 2;
the carrier of S = (the carrier of S1) \/ (the carrier of S2) by Def2;
then reconsider SORTS = (the Sorts of A1)+*the Sorts of A2 as non-empty
ManySortedSet of the carrier of S1+*S2;
A6: dom (SORTS# ) = I* by PARTFUN1:def 2;
A7: SORTS = SA1 \/ SA2 by A1,FUNCT_4:30;
then
A8: SA2# c= SORTS# by Th1,XBOOLE_1:7;
A9: dom SA12 = I1* \/ (I2* ) by PARTFUN1:def 2;
A10: dom SA1 = I1 by PARTFUN1:def 2;
rng the ResultSort of S1 c= I1 by RELAT_1:def 19;
then
A11: (SA1+*SA2)*((the ResultSort of S1)+*the ResultSort of S2) = (SA1*the
ResultSort of S1)+*(SA2*the ResultSort of S2) by A1,A10,A5,A4,FUNCT_4:69;
A12: rng the Arity of S2 c= I2* by RELAT_1:def 19;
A13: dom (SA1# ) = I1* by PARTFUN1:def 2;
A14: SA1# tolerates SA2#
proof
let x be object;
assume
A15: x in (dom (SA1# )) /\ dom (SA2# );
then reconsider i1 = x as Element of I1* by A13,XBOOLE_0:def 4;
reconsider i2 = x as Element of I2* by A2,A15,XBOOLE_0:def 4;
A16: rng i1 c= I1 by FINSEQ_1:def 4;
A17: rng i2 c= I2 by FINSEQ_1:def 4;
thus SA1#.x = product (SA1*i1) by FINSEQ_2:def 5
.= product (SA2*i2) by A1,A10,A5,A16,A17,PARTFUN1:79
.= SA2#.x by FINSEQ_2:def 5;
end;
then
A18: SA12 = SA1# \/ (SA2# ) by FUNCT_4:30;
SA1# c= SORTS# by A7,Th1,XBOOLE_1:7;
then
A19: SA12 c= SORTS# by A18,A8,XBOOLE_1:8;
A20: the carrier' of S = (the carrier' of S1) \/ (the carrier' of S2) by Def2;
A21: rng the Arity of S c= I* by RELAT_1:def 19;
A22: rng the Arity of S1 c= I1* by RELAT_1:def 19;
then
A23: (rng the Arity of S1) \/ rng the Arity of S2 c= I1* \/ (I2* ) by A12,
XBOOLE_1:13;
A24: the Arity of S = (the Arity of S1) +* (the Arity of S2) by Def2;
then
rng the Arity of S c= (rng the Arity of S1) \/ rng the Arity of S2 by
FUNCT_4:17;
then
A25: rng the Arity of S c= dom SA12 by A23,A9;
A26: SA12 tolerates SORTS# by A19,PARTFUN1:54;
A27: (SA1#+*(SA2# ))*((the Arity of S1)+*the Arity of S2)
= (SA1#*the Arity of S1)+*(SA2#*the Arity of S2)
by A13,A2,A22,A12,A14,FUNCT_4:69;
reconsider
CHARACT as ManySortedFunction
of SORTS#*the Arity of S, SORTS*the ResultSort of S
by A20,A24,A3,A6,A21,A25,A11,A26,A27,PARTFUN1:79;
reconsider A = MSAlgebra(#SORTS, CHARACT#) as strict non-empty MSAlgebra
over S by MSUALG_1:def 3;
take A;
thus thesis;
end;
end;
theorem
for S being non void non empty ManySortedSign, A being MSAlgebra over
S holds A tolerates A;
theorem Th19:
for S1,S2 be non void non empty ManySortedSign for A1 be
MSAlgebra over S1, A2 be MSAlgebra over S2 st A1 tolerates A2 holds A2
tolerates A1;
theorem
for S1,S2,S3 being non empty ManySortedSign, A1 being non-empty
MSAlgebra over S1, A2 being non-empty MSAlgebra over S2, 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;
let A1 be non-empty MSAlgebra over S1, A2 be non-empty MSAlgebra over S2, A3
be MSAlgebra over S3 such 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;
thus S1+*S2 tolerates S3 by A1,A4,A7,Th3;
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;
the Charact of A1+*A2 = (the Charact of A1)+*the Charact of A2 by A2,Def4;
hence thesis by A3,A6,A9,FUNCT_4:125;
end;
theorem
for S being strict non empty ManySortedSign, A being non-empty
MSAlgebra over S holds A+*A = the MSAlgebra of A
proof
let S be strict non empty ManySortedSign, A be non-empty MSAlgebra over S;
set A9 = the MSAlgebra of A;
set SA = the Sorts of A9, CA = the Charact of A9;
set SAA = the Sorts of A+*A, CAA = the Charact of A+*A;
CA = CA+*CA;
then
A1: CAA = CA by Def4;
SA = SA+*SA;
then SAA = SA by Def4;
hence thesis by A1;
end;
theorem Th22:
for S1,S2 being non empty ManySortedSign, A1 being non-empty
MSAlgebra over S1, A2 being non-empty MSAlgebra over S2 st A1 tolerates A2
holds A1+*A2 = A2+*A1
proof
let S1,S2 be non empty ManySortedSign;
let A1 be non-empty MSAlgebra over S1, A2 be non-empty MSAlgebra over S2;
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;
(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 A = (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 A = (the Charact of A2) +* (the Charact of A1) by A2,Def4;
S1+*S2 = S2+*S1 by A1,Th5;
hence thesis by A2,A4,A5,Def4;
end;
theorem
for S1,S2,S3 being non empty ManySortedSign, A1 being non-empty
MSAlgebra over S1, A2 being non-empty MSAlgebra over S2, 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, A1 be non-empty MSAlgebra over S1,
A2 be non-empty MSAlgebra over S2, A3 be non-empty MSAlgebra over S3 such 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;
set A12 = A1+*A2, A23 = A2+*A3;
A4: the Charact of A12 = (the Charact of A1) +* (the Charact of A2) by A1,Def4;
set A1293 = A12+*A3, A1923 = A1+*A23;
set s1 = the Sorts of A1, s2 = the Sorts of A2, s3 = the Sorts of A3;
A5: the Sorts of A23 = (the Sorts of A2) +* (the Sorts of A3) by A2,Def4;
A6: the Sorts of A1 tolerates the Sorts of A23
proof
let x be object;
assume
A7: x in (dom s1) /\ dom the Sorts of A23;
then x in dom the Sorts of A23 by XBOOLE_0:def 4;
then
A8: x in dom s2 or x in dom s3 by A5,FUNCT_4:12;
x in dom s1 by A7,XBOOLE_0:def 4;
then x in (dom s1) /\ dom s2 & (s2+*s3).x = s2.x or x in (dom s3) /\ dom
s1 & (s2+*s3).x = s3.x by A2,A8,FUNCT_4:13,15,XBOOLE_0:def 4;
hence thesis by A1,A3,A5;
end;
then
A9: the Sorts of A1923 = (the Sorts of A1) +* (the Sorts of A23) by Def4;
A10: the Charact of A23 = (the Charact of A2) +* (the Charact of A3) by A2,Def4
;
A11: the Charact of A1923 = (the Charact of A1) +* (the Charact of A23) by A6
,Def4;
A12: the Sorts of A12 = (the Sorts of A1) +* (the Sorts of A2) by A1,Def4;
A13: the Sorts of A12 tolerates the Sorts of A3
proof
let x be object;
assume
A14: x in (dom the Sorts of A12) /\ dom s3;
then x in dom the Sorts of A12 by XBOOLE_0:def 4;
then
A15: x in dom s1 or x in dom s2 by A12,FUNCT_4:12;
x in dom s3 by A14,XBOOLE_0:def 4;
then x in (dom s3) /\ dom s1 & (s1+*s2).x = s1.x or x in (dom s2) /\ dom
s3 & (s1+*s2).x = s2.x by A1,A15,FUNCT_4:13,15,XBOOLE_0:def 4;
hence thesis by A2,A3,A12;
end;
then the Charact of A1293 = (the Charact of A12) +* (the Charact of A3) by
Def4;
then
A16: the Charact of A1293 = the Charact of A1923 by A4,A10,A11,FUNCT_4:14;
the Sorts of A1293 = (the Sorts of A12) +* (the Sorts of A3) by A13,Def4;
then the Sorts of A1293 = the Sorts of A1923 by A12,A5,A9,FUNCT_4:14;
hence thesis by A16;
end;
theorem
for S1,S2 being non empty ManySortedSign for A1 being finite-yielding
non-empty MSAlgebra over S1 for A2 being finite-yielding non-empty 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;
let A1 be finite-yielding non-empty MSAlgebra over S1, A2 be finite-yielding
non-empty MSAlgebra over S2 such that
A1: the Sorts of A1 tolerates the Sorts of A2;
let x be object;
set A = A1+*A2;
set SA = the Sorts of A, SA1 = the Sorts of A1, SA2 = the Sorts of A2;
A2: dom SA1 = the carrier of S1 by PARTFUN1:def 2;
A3: SA1 is finite-yielding by MSAFREE2:def 11;
assume x in the carrier of S1+*S2;
then reconsider x as Vertex of S1+*S2;
A4: dom SA2 = 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: SA2 is finite-yielding by MSAFREE2:def 11;
SA = SA1+*SA2 by A1,Def4;
then
SA.x = SA1.x & SA1.x is finite or SA.x = SA2.x & SA2.x is finite by A1,A2,A4
,A5,A3,A6,FUNCT_4:13,15;
hence thesis;
end;
theorem
for S1,S2 being non empty ManySortedSign for A1 being non-empty
MSAlgebra over S1, s1 being Element of product the Sorts of A1 for A2 being
non-empty MSAlgebra over S2, 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;
let A1 be non-empty MSAlgebra over S1;
let s1 be Element of product ((the Sorts of A1) qua non-empty ManySortedSet
of the carrier of S1);
let A2 be non-empty MSAlgebra over S2;
let s2 be Element of product ((the Sorts of A2) qua non-empty ManySortedSet
of the carrier of S2);
assume the Sorts of A1 tolerates the Sorts of A2;
then the Sorts of A1+*A2 = (the Sorts of A1)+*the Sorts of A2 by Def4;
hence thesis by CARD_3:97;
end;
theorem
for S1,S2 being non empty ManySortedSign for A1 being non-empty
MSAlgebra over S1, A2 being non-empty MSAlgebra over S2 st the Sorts of A1
tolerates the Sorts of A2 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;
let A1 be non-empty MSAlgebra over S1;
let A2 be non-empty MSAlgebra over S2;
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;
then the Sorts of A1+*A2 = (the Sorts of A1)+*the Sorts of A2 by Def4;
hence thesis by A3,A1,A2,CARD_3:98,99;
end;
theorem Th27:
for S1,S2 being non void non empty ManySortedSign for A1 being
non-empty MSAlgebra over S1, A2 being non-empty MSAlgebra over S2 st the Sorts
of A1 tolerates the Sorts of A2 for o being OperSymbol of S1+*S2, o2 being
OperSymbol of S2 st o = o2 holds Den(o, A1+*A2) = Den(o2, A2)
proof
let S1,S2 be non void non empty ManySortedSign;
let A1 be non-empty MSAlgebra over S1, A2 be non-empty MSAlgebra over S2;
A1: dom the Charact of A2 = the carrier' of S2 by PARTFUN1:def 2;
assume the Sorts of A1 tolerates the Sorts of 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, o2 be OperSymbol of S2;
assume o = o2;
hence thesis by A2,A1,FUNCT_4:13;
end;
theorem Th28:
for S1,S2 being non void non empty ManySortedSign for A1 being
non-empty MSAlgebra over S1, 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
for o being OperSymbol of S1+*S2, o1 being OperSymbol of S1 st o = o1 holds Den
(o, A1+*A2) = Den(o1, A1)
proof
let S1,S2 be non void non empty ManySortedSign;
let A1 be non-empty MSAlgebra over S1, A2 be non-empty MSAlgebra over S2;
A1: dom the Charact of A1 = the carrier' of S1 by PARTFUN1:def 2;
assume the Sorts of A1 tolerates the Sorts of A2;
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;
let o be OperSymbol of S1+*S2, o1 be OperSymbol of S1;
assume o = o1;
hence thesis by A2,A3,A1,FUNCT_4:15;
end;
theorem Th29:
for S1,S2,S being non void Circuit-like non empty
ManySortedSign st S = S1+*S2 for A1 being non-empty Circuit of S1, A2 being
non-empty Circuit of S2, A being non-empty Circuit of S for s being State of A,
s2 being State of A2 st s2 = s|the carrier of S2 for g being Gate of S, 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 void Circuit-like non empty ManySortedSign such that
A1: S = S1+*S2;
let A1 be non-empty Circuit of S1, A2 be non-empty Circuit of S2;
let A be non-empty Circuit of S;
let s be State of A, s2 be State of A2 such that
A2: s2 = s|the carrier of S2;
let o be OperSymbol of S, o2 be OperSymbol of S2 such that
A3: o = o2;
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;
end;
theorem Th30:
for S1,S2,S being non void Circuit-like non empty
ManySortedSign st S = S1+*S2 & S1 tolerates S2 for A1 being non-empty Circuit
of S1, A2 being non-empty Circuit of S2, A being non-empty Circuit of S for s
being State of A, s1 being State of A1 st s1 = s|the carrier of S1 for g being
Gate of S, 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 void Circuit-like non empty ManySortedSign such that
A1: S = S1+*S2 and
A2: S1 tolerates S2;
let A1 be non-empty Circuit of S1, A2 be non-empty Circuit of S2;
let A be non-empty Circuit of S;
let s be State of A, s1 be State of A1 such that
A3: s1 = s|the carrier of S1;
let o be Gate of S, o1 be Gate of S1 such that
A4: o = o1;
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;
end;
theorem Th31:
for S1,S2,S being non void Circuit-like non empty
ManySortedSign st S = S1+*S2 for A1 being non-empty Circuit of S1, A2 being
non-empty Circuit of S2 for A being non-empty Circuit of S st A1 tolerates A2 &
A = A1+*A2 for s being State of A, v being Vertex of S holds (for s1 being
State of A1 st s1 = s|the carrier of S1 holds v in InnerVertices S1 or v in the
carrier of S1 & v in InputVertices S implies (Following s).v = (Following s1).v
) & (for s2 being State of A2 st s2 = s|the carrier of S2 holds v in
InnerVertices S2 or v in the carrier of S2 & v in InputVertices S implies (
Following s).v = (Following s2).v)
proof
let S1,S2,S be non void Circuit-like non empty ManySortedSign such that
A1: S = S1+*S2;
let A1 be non-empty Circuit of S1, A2 be non-empty Circuit of S2;
let A be non-empty Circuit of S such 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;
let s be State of A, v be Vertex of S;
hereby
let s1 be State of A1 such that
A6: s1 = s|the carrier of S1;
A7: now
assume v in InnerVertices S1;
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;
end;
now
assume that
A11: v in the carrier of S1 and
A12: v in InputVertices S;
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;
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;
end;
let s2 be State of A2 such that
A15: s2 = s|the carrier of S2;
A16: now
assume v in InnerVertices S2;
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;
end;
now
assume that
A20: v in the carrier of S2 and
A21: v in InputVertices S;
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;
end;
hence thesis by A16;
end;
theorem Th32:
for S1,S2,S being non void Circuit-like non empty
ManySortedSign st InnerVertices S1 misses InputVertices S2 & S = S1+*S2 for A1
being non-empty Circuit of S1, A2 being non-empty Circuit of S2 for A being
non-empty Circuit of S st A1 tolerates A2 & A = A1+*A2 for s being State of A,
s1 being State of A1, 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 void Circuit-like non empty ManySortedSign;
assume that
A1: InnerVertices S1 misses InputVertices S2 and
A2: S = S1+*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, A2 be non-empty Circuit of S2;
let A be non-empty Circuit of S such that
A4: A1 tolerates A2 and
A5: A = A1+*A2;
let s be State of A, s1 be State of A1, s2 be State of A2 such that
A6: s1 = s|the carrier of S1 and
A7: s2 = s|the carrier of 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
let x be object;
assume x in (dom Following s1) \/ dom Following s2;
then reconsider v = x as Vertex of S by A2,A9,A8,Def2;
hereby
assume x in dom Following s2;
then reconsider v2 = x as Vertex of S2 by CIRCUIT1:3;
A11: now
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;
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;
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;
end;
assume
A15: not x in dom Following s2;
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
assume v1 in InputVertices S1;
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;
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;
end;
dom Following s = the carrier of S by CIRCUIT1:3;
hence thesis by A3,A9,A8,A10,FUNCT_4:def 1;
end;
theorem Th33:
for S1,S2,S being non void Circuit-like non empty
ManySortedSign st InnerVertices S2 misses InputVertices S1 & S = S1+*S2 for A1
being non-empty Circuit of S1, A2 being non-empty Circuit of S2 for A being
non-empty Circuit of S st A1 tolerates A2 & A = A1+*A2 for s being State of A,
s1 being State of A1, 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 void Circuit-like non empty ManySortedSign such that
A1: InnerVertices S2 misses InputVertices S1 and
A2: S = S1+*S2;
let A1 be non-empty Circuit of S1, A2 be non-empty Circuit of S2;
let A be non-empty Circuit of S such that
A3: A1 tolerates A2 and
A4: A = A1+*A2;
S1 tolerates S2 by A3;
then
A5: S = S2+*S1 by A2,Th5;
A = A2+*A1 by A3,A4,Th22;
hence thesis by A1,A3,A5,Th19,Th32;
end;
theorem
for S1,S2,S being non void Circuit-like non empty ManySortedSign st
InputVertices S1 c= InputVertices S2 & S = S1+*S2 for A1 being non-empty
Circuit of S1, A2 being non-empty Circuit of S2 for A being non-empty Circuit
of S st A1 tolerates A2 & A = A1+*A2 for s being State of A, s1 being State of
A1, 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 void Circuit-like non empty ManySortedSign;
assume InputVertices S1 c= InputVertices S2;
then InnerVertices S2 misses InputVertices S1 by XBOOLE_1:63,79;
hence thesis by Th33;
end;
theorem
for S1,S2,S being non void Circuit-like non empty ManySortedSign st
InputVertices S2 c= InputVertices S1 & S = S1+*S2 for A1 being non-empty
Circuit of S1, A2 being non-empty Circuit of S2 for A being non-empty Circuit
of S st A1 tolerates A2 & A = A1+*A2 for s being State of A, s1 being State of
A1, 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 void Circuit-like non empty ManySortedSign;
assume InputVertices S2 c= InputVertices S1;
then InnerVertices S1 misses InputVertices S2 by XBOOLE_1:63,79;
hence thesis by Th32;
end;
begin :: ManySortedSign with One Operation
definition
let f be object;
let p be FinSequence;
let x be object;
func 1GateCircStr(p,f,x) -> non void strict ManySortedSign means
: Def5:
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
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 = {pf} --> ox as Function of {pf}, C;
reconsider A = {pf} --> pp as Function of {pf}, C*;
reconsider S = ManySortedSign(#C, {pf}, A, R#) as non void strict
ManySortedSign;
take S;
pf in {pf} by TARSKI:def 1;
hence thesis by FUNCOP_1:7;
end;
uniqueness
proof
let S1,S2 be non void strict ManySortedSign;
assume
A1: not thesis;
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 thesis by A1,A2,A4,A3,GRFUNC_1:7;
end;
end;
registration
let f be object;
let p be FinSequence;
let x be object;
cluster 1GateCircStr(p,f,x) -> non empty;
coherence
proof
the carrier of 1GateCircStr(p,f,x) = rng p \/ {x} by Def5;
hence the carrier of 1GateCircStr(p,f,x) is non empty;
end;
end;
theorem Th36:
for f,x being set, 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, p be FinSequence;
set S = 1GateCircStr(p,f,x);
(the Arity of S).[p,f] = p by Def5;
then
A1: for x being object st x in {[p,f]} holds (the Arity of S).x = p by
TARSKI:def 1;
A2: the carrier' of S = {[p,f]} by Def5;
then dom the Arity of S = {[p,f]} by FUNCT_2:def 1;
hence the Arity of S = (p,f) .--> p by A1,FUNCOP_1:11;
(the ResultSort of S).[p,f] = x by Def5;
then
A3: for y being object st y in {[p,f]} holds (the ResultSort of S).y = x by
TARSKI:def 1;
dom the ResultSort of S = {[p,f]} by A2,FUNCT_2:def 1;
hence thesis by A3,FUNCOP_1:11;
end;
theorem
for f,x being set, 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, p be FinSequence;
set S = 1GateCircStr(p,f,x);
let o be Gate of 1GateCircStr(p,f,x);
A1: (the ResultSort of S).[p,f] = x by Def5;
A2: the carrier' of S = {[p,f]} by Def5;
hence o = [p,f] by TARSKI:def 1;
(the Arity of S).[p,f] = p by Def5;
hence thesis by A2,A1,TARSKI:def 1;
end;
theorem
for f,x being set, p being FinSequence holds InputVertices
1GateCircStr(p,f,x) = (rng p) \ {x} & InnerVertices 1GateCircStr(p,f,x) = {x}
proof
let f,x be set;
let p be FinSequence;
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 thesis by A1,XBOOLE_1:40;
end;
definition
let f be object;
let p be FinSequence;
func 1GateCircStr(p,f) -> non void strict ManySortedSign means
: Def6:
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
proof
take 1GateCircStr(p,f, [p,f]);
thus thesis by Def5;
end;
uniqueness
proof
let S1,S2 be non void strict ManySortedSign;
assume
A1: not thesis;
then S1 = 1GateCircStr(p,f, [p,f]) by Def5;
hence thesis by A1,Def5;
end;
end;
registration
let f be object;
let p be FinSequence;
cluster 1GateCircStr(p,f) -> non empty;
coherence
proof
the carrier of 1GateCircStr(p,f) = rng p \/ {[p,f]} by Def6;
hence the carrier of 1GateCircStr(p,f) is non empty;
end;
end;
theorem
for f being set, p being FinSequence holds 1GateCircStr(p,f) =
1GateCircStr(p,f,[p,f])
proof
let f be set, p be FinSequence;
set S = 1GateCircStr(p,f);
A1: the carrier' of S = {[p,f]} by Def6;
A2: (the Arity of S).[p,f] = p by Def6;
A3: (the ResultSort of S).[p,f] = [p,f] by Def6;
the carrier of S = (rng p) \/ {[p,f]} by Def6;
hence thesis by A1,A2,A3,Def5;
end;
theorem Th40:
for f being object, 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 object, p be FinSequence;
set S = 1GateCircStr(p,f);
(the Arity of S).[p,f] = p by Def6;
then
A1: for x being object st x in {[p,f]} holds (the Arity of S).x = p by
TARSKI:def 1;
A2: the carrier' of S = {[p,f]} by Def6;
then dom the Arity of S = {[p,f]} by FUNCT_2:def 1;
hence the Arity of 1GateCircStr(p,f) = (p,f) .--> p by A1,FUNCOP_1:11;
(the ResultSort of S).[p,f] = [p,f] by Def6;
then
A3: for x being object st x in {[p,f]} holds (the ResultSort of S).x = [p,f]
by TARSKI:def 1;
dom the ResultSort of S = {[p,f]} by A2,FUNCT_2:def 1;
hence thesis by A3,FUNCOP_1:11;
end;
theorem Th41:
for f being set, 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, p be FinSequence;
set S = 1GateCircStr(p,f);
let o be Gate of 1GateCircStr(p,f);
the carrier' of S = {[p,f]} by Def6;
hence o = [p,f] by TARSKI:def 1;
hence thesis by Def6;
end;
theorem Th42:
for f being object, p being FinSequence holds InputVertices
1GateCircStr(p,f) = rng p & InnerVertices 1GateCircStr(p,f) = {[p,f]}
proof
let f be object;
let p be FinSequence;
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;
A4: now
assume [p,f] in rng p;
then consider x being object 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;
end;
thus rng p c= InputVertices 1GateCircStr(p,f)
proof
let x be object;
assume
A9: x in rng p;
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 thesis by A2,A3,A10,XBOOLE_0:def 5;
end;
thus thesis by A1,FUNCOP_1:8;
end;
theorem Th43:
for f being set, p,q being FinSequence holds 1GateCircStr(p,f)
tolerates 1GateCircStr(q,f)
proof
let f be set, p,q be FinSequence;
set S1 = 1GateCircStr(p,f), S2 = 1GateCircStr(q,f);
A1: [p,f] <> [q,f] implies {[p,f]} misses {[q,f]} by ZFMISC_1:11;
A2: the Arity of S2 = (q,f) .--> q by Th40;
the Arity of S1 = (p,f) .--> p by Th40;
hence the Arity of S1 tolerates the Arity of S2
by A2,A1,FUNCOP_1:87,XTUPLE_0:1;
A3: the ResultSort of S2 = (q,f) .--> [q,f] by Th40;
the ResultSort of S1 = (p,f) .--> [p,f] by Th40;
hence thesis by A3,A1,FUNCOP_1:87;
end;
begin :: Unsplit condition
definition
let IT be ManySortedSign;
attr IT is unsplit means
: Def7:
the ResultSort of IT = id the carrier' of IT;
attr IT is gate`1=arity means
: Def8:
for g being set st g in the carrier'
of IT holds g = [(the Arity of IT).g, g`2];
attr IT is gate`2isBoolean means
: Def9:
for g being set st g in the
carrier' of IT for p being FinSequence st p = (the Arity of IT).g ex f being
Function of (len p)-tuples_on BOOLEAN, BOOLEAN st g = [g`1, f];
end;
definition
let S be non empty ManySortedSign;
let IT be MSAlgebra over S;
attr IT is gate`2=den means
for g being set st g in the carrier' of
S holds g = [g`1, (the Charact of IT).g];
end;
definition
let IT be non empty ManySortedSign;
attr IT is gate`2=den means
ex A being MSAlgebra over IT st A is gate`2=den;
end;
scheme
MSSLambdaWeak {A,B() -> set, g() -> Function of A(),B(),
f(object,object) -> object}:
ex f being ManySortedSet of A() st for a being set, b being Element of B() st a
in A() & b = g().a holds f.a = f(a,b) proof
deffunc F(object) = f($1,g().$1);
consider f being Function such that
A1: dom f = A() and
A2: for a being object st a in A() holds f.a = F(a) from FUNCT_1:sch 3;
reconsider f as ManySortedSet of A() by A1,PARTFUN1:def 2,RELAT_1:def 18;
take f;
thus thesis by A2;
end;
scheme
Lemma {S() -> non empty ManySortedSign, F(object,object) -> object}:
ex A being
strict MSAlgebra over S() st the Sorts of A = (the carrier of S()) --> BOOLEAN
& for g being set, 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 = F(g,p)
provided
A1: for g being set, p being Element of (the carrier of S())* st g in
the carrier' of S() & p = (the Arity of S()).g holds F(g,p) is Function of (len
p)-tuples_on BOOLEAN, BOOLEAN
proof
set S = S(), SORTS = (the carrier of S) --> BOOLEAN;
consider CHARACT being ManySortedSet of the carrier' of S such that
A2: for o being set, p being Element of (the carrier of S)* st o in the
carrier' of S & p = (the Arity of S).o holds CHARACT.o = F(o,p) from
MSSLambdaWeak;
A3: dom CHARACT = the carrier' of S by PARTFUN1:def 2;
CHARACT is Function-yielding
proof
let x be object;
assume
A4: x in dom CHARACT;
then reconsider o = x as Gate of S by PARTFUN1:def 2;
reconsider p = (the Arity of S).o as Element of (the carrier of S)* by A3
,A4,FUNCT_2:5;
CHARACT.x = F(o,p) by A2,A3,A4;
hence thesis by A1,A3,A4;
end;
then reconsider CHARACT as ManySortedFunction of the carrier' of S;
A5: dom the ResultSort of S = the carrier' of S by FUNCT_2:def 1;
A6: dom the Arity of S = the carrier' of S by FUNCT_2:def 1;
now
let i be object;
assume
A7: i in the carrier' of S;
then reconsider o = i as Gate of S;
reconsider p = (the Arity of S).o as Element of (the carrier of S)* by A7,
FUNCT_2:5;
A8: (SORTS#*the Arity of S).i = SORTS#.p by A6,A7,FUNCT_1:13;
reconsider v = (the ResultSort of S).o as Vertex of S by A7,FUNCT_2:5;
SORTS.v = BOOLEAN by FUNCOP_1:7;
then
A9: (SORTS*the ResultSort of S).i = BOOLEAN by A5,A7,FUNCT_1:13;
A10: SORTS#.p = (len p)-tuples_on BOOLEAN by Th2;
CHARACT.i = F(o,p) by A2,A7;
hence CHARACT.i is Function of (SORTS#*the Arity of S).i, (SORTS*the
ResultSort of S).i by A1,A7,A8,A10,A9;
end;
then reconsider
CHARACT as ManySortedFunction of SORTS#*the Arity of S, SORTS*the
ResultSort of S by PBOOLE:def 15;
take MSAlgebra(#SORTS, CHARACT#);
thus thesis by A2;
end;
registration
cluster gate`2isBoolean -> gate`2=den for non empty ManySortedSign;
coherence
proof
deffunc F(object,object) = $1`2;
let S be non empty ManySortedSign;
assume
A1: for g being set st g in the carrier' of S for p being FinSequence
st p = (the Arity of S).g ex f being Function of (len p)-tuples_on BOOLEAN,
BOOLEAN st g = [g`1,f];
A2: now
let g be set, p be Element of (the carrier of S)*;
assume that
A3: g in the carrier' of S and
A4: p = (the Arity of S).g;
ex f being Function of (len p)-tuples_on BOOLEAN, BOOLEAN st g = [g
`1,f] by A1,A3,A4;
hence F(g,p) is Function of (len p)-tuples_on BOOLEAN, BOOLEAN;
end;
consider A being strict MSAlgebra over S such that
A5: the Sorts of A = (the carrier of S) --> BOOLEAN & for g being set,
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 = F(g,p) from Lemma(A2);
take A;
let g be set;
assume
A6: g in the carrier' of S;
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;
hence thesis by A5,A6,A7;
end;
end;
theorem Th44:
for S being non empty ManySortedSign holds S is unsplit iff for
o being object st o in the carrier' of S holds (the ResultSort of S).o = o
proof
let S be non empty ManySortedSign;
thus S is unsplit implies
for o being object st o in the carrier' of S holds
(the ResultSort of S).o = o by FUNCT_1:17;
assume
A1: for o being object st o in the carrier' of S holds (the ResultSort of S
).o = o;
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;
end;
theorem
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;
assume
A1: S is unsplit;
let x be object;
assume
A2: x in the carrier' of S;
then (the ResultSort of S).x = x by A1,Th44;
hence thesis by A2,FUNCT_2:5;
end;
registration
cluster unsplit -> Circuit-like for non empty ManySortedSign;
coherence
proof
let S be non empty ManySortedSign such that
A1: the ResultSort of S = id the carrier' of S;
let S9 be non void non empty ManySortedSign such that
A2: S9 = S;
let o1,o2 be Gate of S9;
thus thesis by A1,A2,FUNCT_1:17;
end;
end;
theorem Th46:
for f being object, p being FinSequence holds 1GateCircStr(p,f) is
unsplit gate`1=arity
proof
let f be object, p be FinSequence;
set S = 1GateCircStr(p,f);
A1: now
let x be object;
assume x in {[p,f]};
then x = [p,f] by TARSKI:def 1;
hence (the ResultSort of S).x = x by Def6;
end;
A2: the carrier' of S = {[p,f]} by Def6;
then dom the ResultSort of S = {[p,f]} by FUNCT_2:def 1;
hence the ResultSort of S = id the carrier' of S by A2,A1,FUNCT_1:17;
let g be set;
assume g in the carrier' of S;
then
A3: g = [p,f] by A2,TARSKI:def 1;
then (the Arity of S).g = p by Def6;
hence thesis by A3;
end;
registration
let f be object, p be FinSequence;
cluster 1GateCircStr(p,f) -> unsplit gate`1=arity;
coherence by Th46;
end;
registration
cluster unsplit gate`1=arity non void strict non empty for ManySortedSign;
existence
proof
set f = the set,p = the FinSequence;
take 1GateCircStr(p,f);
thus thesis;
end;
end;
theorem Th47:
for S1,S2 being unsplit gate`1=arity non empty ManySortedSign
holds S1 tolerates S2
proof
let S1,S2 be unsplit gate`1=arity non empty ManySortedSign;
set A1 = the Arity of S1, A2 = the Arity of S2;
set R1 = the ResultSort of S1, R2 = the ResultSort of S2;
thus A1 tolerates A2
proof
let x be object;
assume
A1: x in dom A1 /\ dom A2;
then x in dom A2 by XBOOLE_0:def 4;
then x in the carrier' of S2 by FUNCT_2:def 1;
then
A2: x = [A2.x, x`2] by Def8;
x in dom A1 by A1,XBOOLE_0:def 4;
then x in the carrier' of S1 by FUNCT_2:def 1;
then x = [A1.x, x`2] by Def8;
hence thesis by A2,XTUPLE_0:1;
end;
let x be object;
assume
A3: x in dom R1 /\ dom R2;
then x in dom R1 by XBOOLE_0:def 4;
then x in the carrier' of S1 by FUNCT_2:def 1;
then
A4: R1.x = x by Th44;
x in dom R2 by A3,XBOOLE_0:def 4;
then x in the carrier' of S2 by FUNCT_2:def 1;
hence thesis by A4,Th44;
end;
theorem Th48:
for S1,S2 being non empty ManySortedSign, 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;
let A1 be MSAlgebra over S1, A2 be MSAlgebra over S2 such that
A1: A1 is gate`2=den and
A2: A2 is gate`2=den;
let x be object;
set C1 = the Charact of A1, C2 = the Charact of A2;
assume
A3: x in dom C1 /\ dom C2;
then x in dom C2 by XBOOLE_0:def 4;
then x in the carrier' of S2 by PARTFUN1:def 2;
then
A4: x = [x`1, C2.x] by A2;
x in dom C1 by A3,XBOOLE_0:def 4;
then x in the carrier' of S1 by PARTFUN1:def 2;
then x = [x`1, C1.x] by A1;
hence thesis by A4,XTUPLE_0:1;
end;
theorem Th49:
for S1,S2 being unsplit non empty ManySortedSign holds S1+*S2 is unsplit
proof
let S1,S2 be unsplit non empty ManySortedSign;
set S = S1+*S2;
A1: the ResultSort of S = (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 S = (the carrier' of S1) \/ the carrier' of S2 by Def2;
hence the ResultSort of S = id the carrier' of S by A1,A2,A3,FUNCT_4:22;
end;
registration
let S1,S2 be unsplit non empty ManySortedSign;
cluster S1+*S2 -> unsplit;
coherence by Th49;
end;
theorem Th50:
for S1,S2 being gate`1=arity non empty ManySortedSign holds S1+*
S2 is gate`1=arity
proof
let S1,S2 be gate`1=arity non empty ManySortedSign;
set S = S1+*S2;
let g be set;
A1: dom the Arity of S1 = the carrier' of S1 by FUNCT_2:def 1;
A2: the Arity of S = (the Arity of S1)+*the Arity of S2 by Def2;
assume
A3: g in the carrier' of S;
then reconsider g as Gate of S;
A4: dom the Arity of S2 = the carrier' of S2 by FUNCT_2:def 1;
A5: the carrier' of S = (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
assume
A8: not g in the carrier' of S2;
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 S).g, g`2] by A5,A2,A3,A1,A4,A8,FUNCT_4:def 1;
end;
now
assume
A9: g in the carrier' of S2;
then reconsider g2 = g as Gate of S2;
thus g = [(the Arity of S2).g2, g`2] by A9,Def8
.= [(the Arity of S).g, g`2] by A5,A2,A1,A4,A9,FUNCT_4:def 1;
end;
hence thesis by A7;
end;
registration
let S1,S2 be gate`1=arity non empty ManySortedSign;
cluster S1+*S2 -> gate`1=arity;
coherence by Th50;
end;
theorem Th51:
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;
set S = S1+*S2;
assume that
A1: S1 is gate`2isBoolean and
A2: S2 is gate`2isBoolean;
let g be set;
assume
A3: g in the carrier' of S;
let p be FinSequence such that
A4: p = (the Arity of S).g;
reconsider g as Gate of S by A3;
A5: dom the Arity of S1 = the carrier' of S1 by FUNCT_2:def 1;
A6: the Arity of S = (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 S = (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
assume
A11: not g in the carrier' of S2;
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 thesis by A1,A9,A11;
end;
now
assume
A12: g in the carrier' of S2;
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 thesis by A2,A12;
end;
hence thesis by A10;
end;
begin :: One Gate Circuit
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 such that
A1: x in rng p implies X = Y;
func 1GateCircuit(p,f,x) -> strict non-empty MSAlgebra over 1GateCircStr(p,f
,x) means
the Sorts of it = ((rng p) --> X) +* (x .--> Y) & (the Charact of it)
.[p,f] = f;
existence
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, g2 = x .--> Y;
set S = 1GateCircStr(p,f,x);
set SORTS = g1 +* g2;
set CHARACT = (the carrier' of S) --> f;
A2: dom (x .--> Y) = {x} by FUNCOP_1:13;
A3: x in {x} by TARSKI:def 1;
then
A4: SORTS.x = (x .--> Y).x by A2,FUNCT_4:13
.= Y by A3,FUNCOP_1:7;
A5: the carrier of S = (rng p) \/ {x} by Def5;
then reconsider SORTS as non-empty ManySortedSet of the carrier of S;
rng p c= the carrier of S by A5,XBOOLE_1:7;
then p is FinSequence of the carrier of S by FINSEQ_1:def 4;
then reconsider pp = p as Element of (the carrier of S)* by FINSEQ_1:def 11
;
A6: dom (g1# ) = (rng p)* by PARTFUN1:def 2;
A7: dom ((rng p) --> X) = rng p by FUNCOP_1:13;
g1 tolerates g2
proof
let y be object;
assume
A8: y in dom g1 /\ dom g2;
then y in rng p by A7,XBOOLE_0:def 4;
then
A9: g1.y = X by FUNCOP_1:7;
A10: y in {x} by A2,A8,XBOOLE_0:def 4;
then x = y by TARSKI:def 1;
hence thesis by A1,A7,A8,A10,A9,FUNCOP_1:7,XBOOLE_0:def 4;
end;
then g1 c= SORTS by FUNCT_4:28;
then g1# c= SORTS# by Th1;
then
A11: g1#.p9 = SORTS#.pp by A6,GRFUNC_1:2;
A12: the carrier' of S = {[p,f]} by Def5;
then
A13: dom the ResultSort of S = {[p,f]} by FUNCT_2:def 1;
A14: (the ResultSort of S).[p,f] = x by Def5;
A15: (the Arity of S).[p,f] = p by Def5;
A16: len p = n by CARD_1:def 7;
A17: dom the Arity of S = {[p,f]} by A12,FUNCT_2:def 1;
now
let i be object;
A18: SORTS#.pp = n-tuples_on X by A16,A11,Th2;
assume
A19: i in the carrier' of S;
then
A20: i = [p,f] by A12,TARSKI:def 1;
then
A21: (SORTS#*the Arity of S).i = SORTS#.p by A12,A15,A17,A19,FUNCT_1:13;
(SORTS*the ResultSort of S).i = Y by A12,A14,A4,A13,A19,A20,FUNCT_1:13;
hence CHARACT.i is Function of (SORTS#*the Arity of S).i, (SORTS*the
ResultSort of S).i by A19,A21,A18,FUNCOP_1:7;
end;
then reconsider
CHARACT as ManySortedFunction of SORTS#*the Arity of S, SORTS*
the ResultSort of S by PBOOLE:def 15;
reconsider A = MSAlgebra(#SORTS, CHARACT#) as non-empty strict MSAlgebra
over 1GateCircStr(p,f,x) by MSUALG_1:def 3;
take A;
[p,f] in {[p,f]} by TARSKI:def 1;
hence thesis by A12,FUNCOP_1:7;
end;
uniqueness
proof
set S = 1GateCircStr(p,f,x);
let A1,A2 be strict non-empty MSAlgebra over S such that
A22: not thesis;
A23: the carrier' of S = {[p,f]} by Def5;
then dom the Charact of A1 = {[p,f]} by PARTFUN1:def 2;
then
A24: the Charact of A1 = {[[p,f],f]} by A22,GRFUNC_1:7;
dom the Charact of A2 = {[p,f]} by A23,PARTFUN1:def 2;
hence thesis by A22,A24,GRFUNC_1:7;
end;
end;
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:
the Sorts of it = (the carrier of 1GateCircStr(p,f)) --> X & (
the Charact of it).[p,f] = f;
existence
proof
set S = 1GateCircStr(p,f);
set SORTS = (the carrier of S) --> X;
set CHARACT = (the carrier' of S) --> f;
A1: len p = n by CARD_1:def 7;
A2: (the Arity of S).[p,f] = p by Def6;
A3: (the ResultSort of S).[p,f] = [p,f] by Def6;
A4: the carrier' of S = {[p,f]} by Def6;
then
A5: dom the ResultSort of S = {[p,f]} by FUNCT_2:def 1;
A6: the carrier of S = (rng p) \/ {[p,f]} by Def6;
then rng p c= the carrier of S by XBOOLE_1:7;
then p is FinSequence of the carrier of S by FINSEQ_1:def 4;
then reconsider pp = p as Element of (the carrier of S)* by FINSEQ_1:def 11
;
A7: [p,f] in {[p,f]} by TARSKI:def 1;
then [p,f] in the carrier of S by A6,XBOOLE_0:def 3;
then
A8: SORTS.[p,f] = X by FUNCOP_1:7;
A9: dom the Arity of S = {[p,f]} by A4,FUNCT_2:def 1;
now
let i be object;
A10: SORTS#.pp = n-tuples_on X by A1,Th2;
assume
A11: i in the carrier' of S;
then
A12: i = [p,f] by A4,TARSKI:def 1;
then
A13: (SORTS#*the Arity of S).i = SORTS#.p by A4,A2,A9,A11,FUNCT_1:13;
(SORTS*the ResultSort of S).i = X by A4,A3,A8,A5,A11,A12,FUNCT_1:13;
hence CHARACT.i is Function of (SORTS#*the Arity of S).i, (SORTS*the
ResultSort of S).i by A11,A13,A10,FUNCOP_1:7;
end;
then reconsider
CHARACT as ManySortedFunction of SORTS#*the Arity of S, SORTS*
the ResultSort of S by PBOOLE:def 15;
reconsider A = MSAlgebra(#SORTS, CHARACT#) as non-empty strict MSAlgebra
over 1GateCircStr(p,f) by MSUALG_1:def 3;
take A;
thus thesis by A4,A7,FUNCOP_1:7;
end;
uniqueness
proof
set S = 1GateCircStr(p,f);
let A1,A2 be strict non-empty MSAlgebra over S such that
A14: not thesis;
A15: the carrier' of S = {[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 thesis by A14,A16,GRFUNC_1:7;
end;
end;
theorem Th52:
for n being Nat, 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;
let X be non empty set;
let f be Function of n-tuples_on X, X;
let p be FinSeqLen of n;
thus
A1: 1GateCircuit(p,f) is gate`2=den
proof
let g be set;
assume g in the carrier' of 1GateCircStr(p,f);
then
A2: g = [p,f] by Th41;
hence g = [g`1, f]
.= [g`1, (the Charact of 1GateCircuit(p,f)).g] by A2,Def13;
end;
take 1GateCircuit(p,f);
thus thesis by A1;
end;
registration
let n be Nat, 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) -> gate`2=den;
coherence by Th52;
cluster 1GateCircStr(p,f) -> gate`2=den;
coherence by Th52;
end;
theorem Th53:
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;
let p be FinSeqLen of n;
let f be Function of n-tuples_on X, X;
let g be set;
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);
then
A3: g = [p,f] by Th41;
let q be FinSequence;
assume q = (the Arity of 1GateCircStr(p,f)).g;
then reconsider f as Function of (len q)-tuples_on X, X by A3,A2,A1;
take f;
thus thesis by A3;
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) -> gate`2isBoolean;
coherence by Th53;
end;
registration
cluster gate`2isBoolean non empty for ManySortedSign;
existence
proof
set p = the FinSeqLen of 0;
set f = the Function of 0-tuples_on BOOLEAN, BOOLEAN;
take 1GateCircStr(p,f);
thus thesis;
end;
end;
registration
let S1,S2 be gate`2isBoolean non empty ManySortedSign;
cluster S1+*S2 -> gate`2isBoolean;
coherence by Th51;
end;
theorem Th54:
for n being Nat, X being non empty set, 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, X be non empty set, f be Function of n-tuples_on X, X;
let p be FinSeqLen of n;
set S = 1GateCircStr(p,f), A = 1GateCircuit(p,f);
(the Charact of A).[p,f] = f by Def13;
then
A1: for x being object st x in {[p,f]} holds (the Charact of A).x = f by
TARSKI:def 1;
the carrier' of S = {[p,f]} by Def6;
then dom the Charact of A = {[p,f]} by PARTFUN1:def 2;
hence the Charact of A = (p,f) .--> f by A1,FUNCOP_1:11;
let v be Vertex of S;
the Sorts of A = (the carrier of S) --> X by Def13;
hence thesis by FUNCOP_1:7;
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) -> finite-yielding;
coherence
proof
let i be object;
set S = 1GateCircStr(p,f);
assume i in the carrier of S;
hence thesis by Th54;
end;
end;
theorem
for n being Nat, X being non empty set, f being Function of n
-tuples_on X, X, p,q being FinSeqLen of n holds 1GateCircuit(p,f) tolerates
1GateCircuit(q,f)
proof
let n be Nat, X be non empty set, f be Function of n-tuples_on X, X;
let p,q be FinSeqLen of n;
set S1 = 1GateCircStr(p,f), S2 = 1GateCircStr(q,f);
set A1 = 1GateCircuit(p,f), A2 = 1GateCircuit(q,f);
thus 1GateCircStr(p,f) tolerates 1GateCircStr(q,f) by Th43;
A1: the Sorts of A2 = (the carrier of S2) --> X by Def13;
the Sorts of A1 = (the carrier of S1) --> X by Def13;
hence the Sorts of A1 tolerates the Sorts of A2 by A1,FUNCOP_1:87;
A2: the Charact of A2 = (q,f) .--> f by Th54;
the Charact of A1 = (p,f) .--> f by Th54;
hence thesis by A2,FUNCOP_1:87;
end;
theorem
for n being Nat, X being finite non empty set, f being Function of n
-tuples_on X, X, 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;
let X be non empty finite set;
let f be Function of n-tuples_on X, X;
let p be FinSeqLen of n;
let s be State of 1GateCircuit(p,f);
set S = 1GateCircStr(p,f), A = 1GateCircuit(p,f);
set IV = InnerVertices S;
IV = {[p,f]} by Th42;
then reconsider v = [p,f] as Element of IV by TARSKI:def 1;
the carrier' of S = {[p,f]} by Def6;
then reconsider o = [p,f] as Gate of S 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, A)).(action_at v depends_on_in s)
by CIRCUIT2:def 5;
hence thesis by A1,A2,Def13;
end;
begin :: Boolean Circuits
:: definition
:: redefine func BOOLEAN -> Subset of NAT;
:: coherence by MARGREL1:def 12,ZFMISC_1:38;
:: end;
definition
let S be non empty ManySortedSign;
let IT be MSAlgebra over S;
attr IT is Boolean means
for v being Vertex of S holds (the Sorts of IT).v = BOOLEAN;
end;
theorem Th57:
for S being non empty ManySortedSign, 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, A be MSAlgebra over S;
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
proof
assume for v being Vertex of S holds (the Sorts of A).v = BOOLEAN;
then for v being object st v in the carrier of S
holds (the Sorts of A).v = BOOLEAN;
hence thesis by A1,FUNCOP_1:11;
end;
assume
A2: the Sorts of A = (the carrier of S) --> BOOLEAN;
let v be Vertex of S;
thus thesis by A2,FUNCOP_1:7;
end;
registration
let S be non empty ManySortedSign;
cluster Boolean -> non-empty finite-yielding for MSAlgebra over S;
coherence
proof
let A be MSAlgebra over S;
assume
A1: A is Boolean;
then the Sorts of A = (the carrier of S) --> BOOLEAN by Th57;
hence A is non-empty;
let v be object;
thus thesis by A1;
end;
end;
theorem
for S being non empty ManySortedSign, A being MSAlgebra over S holds A
is Boolean iff rng the Sorts of A c= {BOOLEAN}
proof
let S be non empty ManySortedSign, A be MSAlgebra over S;
hereby
assume A is 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;
end;
assume
A1: rng the Sorts of A c= {BOOLEAN};
let v be Vertex of S;
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 thesis by A1,TARSKI:def 1;
end;
theorem Th59:
for S1,S2 being non empty ManySortedSign for A1 being MSAlgebra
over S1, 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;
let A1 be MSAlgebra over S1, A2 be MSAlgebra over S2;
assume that
A1: A1 is Boolean and
A2: A2 is Boolean;
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 thesis by A3,FUNCOP_1:87;
end;
theorem Th60:
for S1,S2 being unsplit gate`1=arity non empty ManySortedSign
for A1 being MSAlgebra over S1, A2 being MSAlgebra over S2 st A1 is Boolean
gate`2=den & A2 is Boolean gate`2=den holds A1 tolerates A2
by Th47,Th48,Th59;
registration
let S be non empty ManySortedSign;
cluster Boolean for strict MSAlgebra over S;
existence
proof
deffunc F(set,Element of (the carrier of S)*) = ((len $2)-tuples_on
BOOLEAN) --> FALSE;
A1: for g being set, p being Element of (the carrier of S)* st g in the
carrier' of S & p = (the Arity of S).g holds F(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,
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 = F(g,p) from Lemma(A1);
take A;
let v be Vertex of S;
thus thesis by A2,FUNCOP_1:7;
end;
end;
theorem
for n being Nat, 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, f be Function of n-tuples_on BOOLEAN, BOOLEAN;
let p be FinSeqLen of n;
set S = 1GateCircStr(p,f), A = 1GateCircuit(p,f);
let v be Vertex of S;
the Sorts of A = (the carrier of S) --> BOOLEAN by Def13;
hence thesis by FUNCOP_1:7;
end;
theorem Th62:
for S1,S2 being non empty ManySortedSign for A1 be Boolean
MSAlgebra over S1 for A2 be Boolean MSAlgebra over S2 holds A1+*A2 is Boolean
proof
let S1,S2 be non empty ManySortedSign;
let A1 be Boolean MSAlgebra over S1;
let A2 be Boolean MSAlgebra over S2;
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 S;
A2: dom the Sorts of A2 = the carrier of S2 by PARTFUN1:def 2;
the carrier of S = (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 A = (the Sorts of A1)+*the Sorts of A2 by Def4;
then
(the Sorts of A).x = (the Sorts of A1).x & (the Sorts of A1).x = BOOLEAN
or (the Sorts of A).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,15;
hence thesis;
end;
theorem Th63:
for S1,S2 being non empty ManySortedSign for A1 be non-empty
MSAlgebra over S1, A2 be 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;
let A1 be non-empty MSAlgebra over S1;
let A2 be non-empty MSAlgebra over S2;
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;
A4: the Charact of A = (the Charact of A1)+*the Charact of A2 by A3,Def4;
let g be set;
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 S = (the carrier' of S1) \/ the carrier' of S2 by Def2;
assume g in the carrier' of S;
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 A).g = (the Charact of A1).g & [g`1, (the Charact of A1
).g] = g or (the Charact of A).g = (the Charact of A2).g & [g`1, (the Charact
of A2).g] = g by A1,A2,A4,A5,A6,A8,FUNCT_4:13,15;
hence thesis;
end;
registration
cluster unsplit gate`1=arity gate`2=den gate`2isBoolean non void strict for
non
empty ManySortedSign;
existence
proof
set p = the FinSeqLen of 1;
set f = the Function of 1-tuples_on BOOLEAN, BOOLEAN;
take 1GateCircStr(p,f);
thus thesis;
end;
end;
registration
let S be gate`2isBoolean non empty ManySortedSign;
cluster Boolean gate`2=den for strict MSAlgebra over S;
existence
proof
deffunc F(set,set) = $1`2;
A1: now
let g be set, p be Element of (the carrier of S)*;
assume that
A2: g in the carrier' of S and
A3: p = (the Arity of S).g;
ex f being Function of (len p)-tuples_on BOOLEAN, BOOLEAN st g = [g
`1, f] by A2,A3,Def9;
hence F(g,p) is Function of (len p)-tuples_on BOOLEAN, BOOLEAN;
end;
consider A being strict MSAlgebra over S such that
A4: the Sorts of A = (the carrier of S) --> BOOLEAN & for g being set,
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 = F(g,p) from Lemma(A1);
take A;
thus A is Boolean
by A4,FUNCOP_1:7;
let g be set;
assume
A5: g in the carrier' of S;
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;
hence thesis by A4,A5,A6;
end;
end;
registration
let S1,S2 be unsplit gate`2isBoolean non void non empty ManySortedSign;
let A1 be Boolean gate`2=den Circuit of S1;
let A2 be Boolean gate`2=den Circuit of S2;
cluster A1+*A2 -> Boolean gate`2=den;
coherence
proof
the Sorts of A1 tolerates the Sorts of A2 by Th59;
hence thesis by Th62,Th63;
end;
end;
registration
let n be Nat;
let X be finite non empty set;
let f be Function of n-tuples_on X, X;
let p be FinSeqLen of n;
cluster gate`2=den strict non-empty for Circuit of 1GateCircStr(p,f);
existence
proof
take 1GateCircuit(p,f);
thus thesis;
end;
end;
registration
let n be Nat;
let X be finite non empty set;
let f be Function of n-tuples_on X, X;
let p be FinSeqLen of n;
cluster 1GateCircuit(p,f) -> gate`2=den;
coherence;
end;
theorem
for S1,S2 being unsplit gate`1=arity gate`2isBoolean non void non
empty ManySortedSign for A1 being Boolean gate`2=den Circuit of S1 for A2 being
Boolean gate`2=den Circuit of S2 for s being State of A1+*A2, v being Vertex of
S1+*S2 holds (for s1 being State of A1 st s1 = s|the carrier of S1 holds v in
InnerVertices S1 or v in the carrier of S1 & v in InputVertices(S1+*S2) implies
(Following s).v = (Following s1).v) & for s2 being State of A2 st s2 = s|the
carrier of S2 holds v in InnerVertices S2 or v in the carrier of S2 & v in
InputVertices(S1+*S2) implies (Following s).v = (Following s2).v
proof
let S1,S2 be unsplit gate`1=arity gate`2isBoolean non void non empty
ManySortedSign;
let A1 be Boolean gate`2=den Circuit of S1;
let A2 be Boolean gate`2=den Circuit of S2;
A1 tolerates A2 by Th60;
hence thesis by Th31;
end;