Copyright (c) 1995 Association of Mizar Users
environ
vocabulary MSUALG_1, FUNCT_1, FUNCOP_1, PRALG_1, RELAT_1, CARD_3, FINSEQ_1,
FINSEQ_2, AMI_1, ZF_REFLE, FUNCT_4, BOOLE, PBOOLE, PARTFUN1, TDGROUP,
MSAFREE2, FINSET_1, QC_LANG1, PRE_CIRC, CIRCUIT1, CLASSES1, MCART_1,
MARGREL1, LATTICES, CIRCCOMB;
notation TARSKI, XBOOLE_0, SUBSET_1, NUMBERS, NAT_1, MCART_1, RELAT_1,
FUNCT_1, STRUCT_0, FINSEQ_1, FINSEQ_2, FINSET_1, FUNCT_2, FUNCOP_1,
PARTFUN1, FUNCT_4, GROUP_1, CARD_3, CLASSES1, MARGREL1, PBOOLE, PRALG_1,
MSUALG_1, PRE_CIRC, MSAFREE2, CIRCUIT1, CIRCUIT2;
constructors MCART_1, CLASSES1, MARGREL1, PRALG_1, CIRCUIT1, CIRCUIT2;
clusters RELSET_1, FUNCT_1, FINSET_1, PRVECT_1, PBOOLE, MSUALG_1, MSAFREE2,
STRUCT_0, MSUALG_2, FINSEQ_2, CANTOR_1, MARGREL1, FUNCOP_1, ARYTM_3,
ORDINAL1, XBOOLE_0, FRAENKEL, MEMBERED, ORDINAL2;
requirements NUMERALS, BOOLE, SUBSET;
definitions TARSKI, PARTFUN1, MSUALG_1, PRALG_1, PRE_CIRC, MSAFREE2, STRUCT_0,
RELAT_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, FUNCT_6,
PRE_CIRC, MSAFREE2, CIRCUIT1, CIRCUIT2, MARGREL1, MCART_1, CARD_3,
ORDINAL1, CLASSES1, GROUP_1, LANG1, MONOID_1, RELSET_1, XBOOLE_0,
XBOOLE_1;
schemes FUNCT_1;
begin :: Combining of ManySortedSign's
definition let S be ManySortedSign;
mode Gate of S is Element of the OperSymbols of S;
end;
definition let A be set; let f be Function;
cluster A --> f -> Function-yielding;
coherence
proof set g = A --> f;
A1: dom (A --> f) = A by FUNCOP_1:19;
g is Function-yielding
proof let a be set; assume a in dom g; hence g.a is Function by A1,
FUNCOP_1:13;
end;
hence thesis;
end;
end;
Lm1:
now let i be Nat, X be non empty set;
thus product ((Seg i) --> X) = product (i |-> X) by FINSEQ_2:def 2
.= i-tuples_on X by FUNCT_6:9;
end;
Lm2:
now let S be non void ManySortedSign;
let o be Gate of S;
the OperSymbols of S is non empty by MSUALG_1:def 5;
hence o in the OperSymbols of S;
end;
definition
let f,g be non-empty Function;
cluster f+*g -> non-empty;
coherence
proof set h = f+*g;
A1: dom (f+*g) = dom f \/ dom g by FUNCT_4:def 1;
h is non-empty
proof assume {} in rng h;
then consider x being set such that
A2: x in dom (f+*g) & {} = h.x by FUNCT_1:def 5;
(x in dom f or x in dom g) & (not x in dom g or x in dom g)
by A1,A2,XBOOLE_0:def 2;
then {} = f.x & x in dom f or {} = g.x & x in dom g
by A1,A2,FUNCT_4:def 1;
then {} in rng f or {} in rng g by FUNCT_1:def 5;
hence thesis by RELAT_1:def 9;
end;
hence thesis;
end;
end;
definition
let A,B be set;
let f be ManySortedSet of A;
let g be ManySortedSet of B;
redefine func f+*g -> ManySortedSet of A \/ B;
coherence
proof dom f = A & dom g = B by PBOOLE:def 3;
then dom (f+*g) = A \/ B by FUNCT_4:def 1;
hence thesis by PBOOLE:def 3;
end;
end;
theorem Th1:
for f1,f2, g1,g2 being Function st
rng g1 c= dom f1 & rng g2 c= dom f2 & f1 tolerates f2
holds (f1+*f2)*(g1+*g2) = (f1*g1)+*(f2*g2)
proof let f1,f2, g1,g2 be Function; assume
A1: rng g1 c= dom f1 & rng g2 c= dom f2 & f1 tolerates f2;
then rng (g1+*g2) c= (rng g1) \/ rng g2 & dom (f1+*f2) = (dom f1) \/ dom
f2 &
(rng g1) \/ rng g2 c= (dom f1) \/ dom f2 by FUNCT_4:18,def 1,XBOOLE_1:13;
then rng (g1+*g2) c= dom (f1+*f2) by XBOOLE_1:1;
then A2: dom ((f1+*f2)*(g1+*g2)) = dom (g1+*g2) by RELAT_1:46
.= (dom g1) \/ dom g2 by FUNCT_4:def 1;
A3: dom (f1*g1) = dom g1 & dom (f2*g2) = dom g2 by A1,RELAT_1:46;
then A4: dom ((f1*g1)+*(f2*g2)) = (dom g1) \/ dom g2 by FUNCT_4:def 1;
now let x be set; assume
A5: x in (dom g1) \/ dom g2;
then A6: ((f1+*f2)*(g1+*g2)).x = (f1+*f2).((g1+*g2).x) by A2,FUNCT_1:22;
(x in dom g1 or x in dom g2) & (not x in dom g2 or x in dom g2)
by A5,XBOOLE_0:def 2;
then (g1+*g2).x = g1.x & ((f1*g1)+*(f2*g2)).x = (f1*g1).x &
(f1*g1).x = f1.(g1.x) & g1.x in rng g1 &
(g1.x in rng g1 implies g1.x in dom f1) or
(g1+*g2).x = g2.x & ((f1*g1)+*(f2*g2)).x = (f2*g2).x &
(f2*g2).x = f2.(g2.x) & g2.x in rng g2 &
(g2.x in rng g2 implies g2.x in dom f2)
by A1,A3,A5,FUNCT_1:22,def 5,FUNCT_4:def 1;
hence ((f1+*f2)*(g1+*g2)).x = ((f1*g1)+*(f2*g2)).x
by A1,A6,FUNCT_4:14,16;
end;
hence thesis by A2,A4,FUNCT_1:9;
end;
theorem Th2:
for f1,f2, g being Function st
rng g c= dom f1 & rng g c= dom f2 & f1 tolerates f2
holds f1*g = f2*g
proof let f1,f2, g be Function; assume
A1: rng g c= dom f1 & rng g c= dom f2 & f1 tolerates f2;
then A2: dom (f1*g) = dom g & dom (f2*g) = dom g by RELAT_1:46;
now let x be set; assume x in dom g;
then A3: g.x in rng g & (f1*g).x = f1.(g.x) & (f2*g).x = f2.(g.x)
by A2,FUNCT_1:22,def 5;
then g.x in (dom f1) /\ (dom f2) by A1,XBOOLE_0:def 3;
hence (f1*g).x = (f2*g).x by A1,A3,PARTFUN1:def 6;
end;
hence thesis by A2,FUNCT_1:9;
end;
theorem Th3:
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;
now let z be set; assume
A2: z in f#;
then consider x,y being set such that
A3: [x,y] = z by RELAT_1:def 1;
A4: dom f = A & dom g = B & dom (f# ) = A* & dom (g# ) = B*
by PBOOLE:def 3;
then reconsider x as Element of A* by A2,A3,RELAT_1:def 4;
A5: dom f c= dom g by A1,RELAT_1:25;
rng x c= A by FINSEQ_1:def 4;
then rng x c= B by A4,A5,XBOOLE_1:1;
then x is FinSequence of B by FINSEQ_1:def 4;
then reconsider x' = x as Element of B* by FINSEQ_1:def 11;
A6: rng x c= A & rng x' c= B & f tolerates g
by A1,FINSEQ_1:def 4,PARTFUN1:135;
y = f#.x by A2,A3,FUNCT_1:8
.= product (f*x) by MSUALG_1:def 3
.= product (g*x') by A4,A6,Th2
.= g#.x' by MSUALG_1:def 3;
hence z in g# by A3,A4,FUNCT_1:8;
end;
hence thesis by TARSKI:def 3;
end;
theorem Th4:
for X,Y,x,y being set holds X --> x tolerates Y --> y iff x = y or X misses Y
proof let X,Y,x,y be set;
set f = X --> x, g = Y --> y;
A1: dom f = X & dom g = Y by FUNCOP_1:19;
thus f tolerates g implies x = y or X misses Y
proof assume that
A2: for z being set st z in dom f /\ dom g holds f.z = g.z and
A3: x <> y;
assume X meets Y;
then consider z be set such that A4: z in X & z in Y by XBOOLE_0:3;
z in X /\ Y & f.z = x & g.z = y by A4,FUNCOP_1:13,XBOOLE_0:def 3;
hence thesis by A1,A2,A3;
end;
assume
A5: x = y or X misses Y;
let z be set; assume z in dom f /\ dom g;
then z in X & z in Y by A1,XBOOLE_0:def 3;
then f.z = x & g.z = y & x = y by A5,FUNCOP_1:13,XBOOLE_0:3;
hence thesis;
end;
theorem Th5:
for f,g,h being Function st f tolerates g & g tolerates h & h tolerates f
holds f+*g tolerates h
proof let f,g,h be Function such that
A1: f tolerates g & g tolerates h & h tolerates f;
let x be set; assume x in (dom (f+*g)) /\ dom h;
then x in dom (f+*g) & x in dom h by XBOOLE_0:def 3;
then (x in dom f or x in dom g) & x in dom h by FUNCT_4:13;
then x in (dom h) /\ dom f & (f+*g).x = f.x or
x in (dom g) /\ dom h & (f+*g).x = g.x by A1,FUNCT_4:14,16,XBOOLE_0:def 3;
hence thesis by A1,PARTFUN1:def 6;
end;
theorem Th6:
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:168 .= dom p by RELAT_1:169;
p in X* by FINSEQ_1:def 11;
hence (X --> Y)#.p = product ((X --> Y)*p) by MSUALG_1:def 3
.= product (p"X --> Y) by FUNCOP_1:25
.= 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 f1 = A & dom g1 = A & dom h1 = A &
dom f2 = B & dom g2 = B & dom h2 = B by PBOOLE:def 3;
h is Function-yielding
proof let x be set; assume
x in dom h;
then A2: x in A \/ B by PBOOLE:def 3;
then (x in A or x in B) & (not x in B or x in B) by XBOOLE_0:def 2;
then h.x = h1.x & h1.x is Function or h.x = h2.x & h2.x is Function
by A1,A2,FUNCT_4:def 1,MSUALG_1:def 2;
hence thesis;
end;
then reconsider h as ManySortedFunction of A \/ B;
h is ManySortedFunction of f, g
proof let x be set; assume
A3: x in A \/ B;
then (x in A or x in B) & (not x in B or x in B) by XBOOLE_0:def 2;
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 A1,A3,FUNCT_4:def 1,MSUALG_1:def 2;
hence thesis;
end;
hence thesis;
end;
end;
Lm3:
for A,B be set
for f1,g1 be non-empty ManySortedSet of A
for f2,g2 be non-empty ManySortedSet of B
for h1 be ManySortedFunction of f1,g1
for h2 be ManySortedFunction of f2,g2 holds
h1+*h2 is ManySortedFunction of f1+*f2, g1+*g2;
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 OperSymbols of it = (the OperSymbols of S1) \/ (the OperSymbols 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
A1: dom the Arity of S1 = the OperSymbols of S1 &
dom the Arity of S2 = the OperSymbols of S2 by FUNCT_2:def 1;
A2: dom the ResultSort of S1 = the OperSymbols of S1 &
dom the ResultSort of S2 = the OperSymbols of S2 by FUNCT_2:def 1;
reconsider CARR = (the carrier of S1) \/ (the carrier of S2) as
non empty set;
set OPER = (the OperSymbols of S1) \/ (the OperSymbols of S2);
set ARITY = (the Arity of S1) +* (the Arity of S2);
set RESULT = (the ResultSort of S1) +* (the ResultSort of S2);
the carrier of S1 c= CARR & the carrier of S2 c= CARR by XBOOLE_1:7;
then (the carrier of S1)* c= CARR* & (the carrier of S2)* c= CARR* &
rng (the Arity of S1) c= (the carrier of S1)* &
rng (the Arity of S2) c= (the carrier of S2)*
by LANG1:19,RELSET_1:12;
then rng (the Arity of S1) c= CARR* &
rng (the Arity of S2) c= CARR* by XBOOLE_1:1;
then rng ARITY c= rng (the Arity of S1) \/ rng (the Arity of S2) &
rng (the Arity of S1) \/ rng (the Arity of S2) c= CARR*
by FUNCT_4:18,XBOOLE_1:8;
then dom ARITY = OPER & rng ARITY c= CARR* by A1,FUNCT_4:def 1,XBOOLE_1:1;
then reconsider ARITY as Function of OPER, CARR* by FUNCT_2:def 1,RELSET_1:
11;
rng (the ResultSort of S1) c= the carrier of S1 &
rng (the ResultSort of S2) c= the carrier of S2 &
the carrier of S1 c= CARR & the carrier of S2 c= CARR
by RELSET_1:12,XBOOLE_1:7;
then rng (the ResultSort of S1) c= CARR &
rng (the ResultSort of S2) c= CARR by XBOOLE_1:1;
then rng RESULT c= rng (the ResultSort of S1) \/ rng (the ResultSort of S2
) &
rng (the ResultSort of S1) \/ rng (the ResultSort of S2) c= CARR
by FUNCT_4:18,XBOOLE_1:8;
then dom RESULT = OPER & rng RESULT c= CARR by A2,FUNCT_4:def 1,XBOOLE_1:1
;
then reconsider RESULT as Function of OPER, CARR by FUNCT_2:def 1,RELSET_1:
11;
take ManySortedSign(#CARR, OPER, ARITY, RESULT#);
thus thesis;
end;
uniqueness;
end;
theorem Th7:
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 &
the ResultSort of S1 tolerates the ResultSort of S2 and
A2: the Arity of S2 tolerates the Arity of S3 &
the ResultSort of S2 tolerates the ResultSort of S3 and
A3: the Arity of S3 tolerates the Arity of S1 &
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,A2,A3,Th5;
the ResultSort of S1+*S2 = (the ResultSort of S1)+*the ResultSort of S2
by Def2;
hence thesis by A1,A2,A3,Th5;
end;
theorem Th8:
for S being non empty ManySortedSign holds S+*S = the ManySortedSign of S
proof let S be non empty ManySortedSign;
the carrier of S = (the carrier of S) \/ the carrier of S &
the OperSymbols of S = (the OperSymbols of S) \/ the OperSymbols of S &
the Arity of S = (the Arity of S)+*the Arity of S &
the ResultSort of S = (the ResultSort of S)+*the ResultSort of S;
hence thesis by Def2;
end;
theorem Th9:
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
the Arity of S1 tolerates the Arity of S2 &
the ResultSort of S1 tolerates the ResultSort of S2;
then (the Arity of S1)+*the Arity of S2 = (the Arity of S2)+*the Arity of
S1 &
(the ResultSort of S1)+*the ResultSort of S2
= (the ResultSort of S2)+*the ResultSort of S1 by FUNCT_4:35;
then the carrier of S = (the carrier of S1) \/ (the carrier of S2) &
the OperSymbols of S = (the OperSymbols of S1) \/ (the OperSymbols of S2)&
the Arity of S = (the Arity of S2) +* (the Arity of S1) &
the ResultSort of S = (the ResultSort of S2) +* (the ResultSort of S1)
by Def2;
hence thesis by Def2;
end;
theorem Th10:
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 S12'3 = S12+*S3, S1'23 = S1+*S23;
A1:the carrier of S12 = (the carrier of S1) \/ (the carrier of S2) &
the OperSymbols of S12 = (the OperSymbols of S1) \/ the OperSymbols of S2&
the Arity of S12 = (the Arity of S1) +* (the Arity of S2) &
the ResultSort of S12 = (the ResultSort of S1)+*the ResultSort of S2
by Def2;
A2:the carrier of S23 = (the carrier of S2) \/ (the carrier of S3) &
the OperSymbols of S23 = (the OperSymbols of S2) \/ the OperSymbols of S3&
the Arity of S23 = (the Arity of S2) +* (the Arity of S3) &
the ResultSort of S23 = (the ResultSort of S2)+*the ResultSort of S3
by Def2;
A3: the carrier of S12'3 = (the carrier of S12) \/ (the carrier of S3) &
the OperSymbols of S12'3 =
(the OperSymbols of S12) \/ the OperSymbols of S3 &
the Arity of S12'3 = (the Arity of S12) +* (the Arity of S3) &
the ResultSort of S12'3 = (the ResultSort of S12)+*the ResultSort of S3
by Def2;
the carrier of S1'23 = (the carrier of S1) \/ (the carrier of S23) &
the OperSymbols of S1'23 =
(the OperSymbols of S1) \/ the OperSymbols of S23 &
the Arity of S1'23 = (the Arity of S1) +* (the Arity of S23) &
the ResultSort of S1'23 = (the ResultSort of S1)+*the ResultSort of S23
by Def2;
then the carrier of S12'3 = the carrier of S1'23 &
the OperSymbols of S12'3 = the OperSymbols of S1'23 &
the Arity of S12'3 = the Arity of S1'23 &
the ResultSort of S12'3 = the ResultSort of S1'23
by A1,A2,A3,FUNCT_4:15,XBOOLE_1:4;
hence thesis;
end;
definition
cluster one-to-one Function;
existence proof reconsider f = {} as Function;
take f; thus thesis; end;
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 & the ResultSort of S2 c= f;
set r1 = the ResultSort of S1, r2 =the ResultSort of S2;
let S be non void non empty ManySortedSign; assume
A2: S = S1+*S2;
set r = the ResultSort of S;
let o1, o2 be Gate of S; assume
A3: the_result_sort_of o1 = the_result_sort_of o2;
A4: the_result_sort_of o1 = (the ResultSort of S).o1 &
the_result_sort_of o2 = (the ResultSort of S).o2 by MSUALG_1:def 7;
A5: r = r1+*r2 & dom r = the OperSymbols of S by A2,Def2,FUNCT_2:def 1;
r1+*r2 c= r1 \/ r2 & r1 \/ r2 c= f by A1,FUNCT_4:30,XBOOLE_1:8;
then A6: r1+*r2 c= f & o1 in dom r & o2 in dom r by A5,Lm2,XBOOLE_1:1;
then r.o1 = f.o1 & r.o2 = f.o2 & dom r c= dom f by A5,GRFUNC_1:8;
hence o1 = o2 by A3,A4,A6,FUNCT_1:def 8;
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;
let S be non void non empty ManySortedSign; assume
A2: S = S1+*S2;
set r = the ResultSort of S;
set r1 = the ResultSort of S1, r2 = the ResultSort of S2;
let o1, o2 be Gate of S; assume
A3: the_result_sort_of o1 = the_result_sort_of o2;
A4: the_result_sort_of o1 = r.o1 &
the_result_sort_of o2 = r.o2 by MSUALG_1:def 7;
A5: r = r1+*r2 & dom r = the OperSymbols of S &
dom r1 = the OperSymbols of S1 & dom r2 = the OperSymbols of S2
by A2,Def2,FUNCT_2:def 1;
A6: InnerVertices S1 = rng r1 & InnerVertices S2 = rng r2 by MSAFREE2:def 3;
A7: o1 in the OperSymbols of S & o2 in the OperSymbols of S &
the OperSymbols of S = (the OperSymbols of S1) \/ the OperSymbols of S2
by A2,Def2,Lm2;
then (not o1 in the OperSymbols of S2 & o1 in the OperSymbols of S1 or
o1 in the OperSymbols of S2) &
(not o2 in the OperSymbols of S2 & o2 in the OperSymbols of S1 or
o2 in the OperSymbols of S2) by XBOOLE_0:def 2;
then A8: (r.o1 = r1.o1 & r1.o1 in rng r1 & o1 in the OperSymbols of S1 or
r.o1 = r2.o1 & r2.o1 in rng r2 & o1 in the OperSymbols of S2) &
(r.o2 = r1.o2 & r1.o2 in rng r1 & o2 in the OperSymbols of S1 or
r.o2 = r2.o2 & r2.o2 in rng r2 & o2 in the OperSymbols of S2)
by A5,A7,FUNCT_1:def 5,FUNCT_4:def 1;
per cases by A1,A3,A4,A6,A8,XBOOLE_0:3;
suppose
A9: r.o1 = r1.o1 & o1 in the OperSymbols of S1 &
r.o2 = r1.o2 & o2 in the OperSymbols of S1;
then reconsider S = S1 as non void Circuit-like (non empty ManySortedSign)
by MSUALG_1:def 5;
reconsider p1 = o1, p2 = o2 as Gate of S by A9;
the_result_sort_of p1 = r1.p1 & the_result_sort_of p2 = r1.p2
by MSUALG_1:def 7;
hence o1 = o2 by A3,A4,A9,MSAFREE2:def 6;
suppose
A10: r.o1 = r2.o1 & o1 in the OperSymbols of S2 &
r.o2 = r2.o2 & o2 in the OperSymbols of S2;
then reconsider S = S2 as non void Circuit-like (non empty ManySortedSign)
by MSUALG_1:def 5;
reconsider p1 = o1, p2 = o2 as Gate of S by A10;
the_result_sort_of p1 = r2.p1 & the_result_sort_of p2 = r2.p2
by MSUALG_1:def 7;
hence o1 = o2 by A3,A4,A10,MSAFREE2:def 6;
end;
theorem Th13:
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;
consider o1 being Gate of S1, o2 being Gate of S2;
assume S1 is not void or S2 is not void;
then (o1 in the OperSymbols of S1 or o2 in the OperSymbols of S2) &
the OperSymbols of S1+*S2 =
(the OperSymbols of S1) \/ the OperSymbols of S2 by Def2,Lm2;
hence the OperSymbols of S1+*S2 <> {} by XBOOLE_0:def 2;
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 by GROUP_1:def 13;
the carrier of S1+*S2 = C1 \/ C2 by Def2;
hence S1+*S2 is finite by GROUP_1:def 13;
end;
definition
let S1 be non void non empty ManySortedSign;
let S2 be non empty ManySortedSign;
cluster S1 +* S2 -> non void;
coherence by Th13;
cluster S2 +* S1 -> non void;
coherence by Th13;
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 Th15:
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
A1: the Arity of S1 tolerates the Arity of S2 & R1 tolerates R2;
set S = S1+*S2, R = the ResultSort of S;
A2: R = R1+*R2 & the carrier of S = (the carrier of S1) \/ the carrier of S2
by Def2;
then R1 c= R by A1,FUNCT_4:29;
then rng R1 c= rng R & rng R2 c= rng R by A2,FUNCT_4:19,RELAT_1:25;
then A3: rng R c= (rng R1) \/ (rng R2) & (rng R1) \/ (rng R2) c= rng R
by A2,FUNCT_4:18,XBOOLE_1:8;
then A4: rng R = (rng R1) \/ (rng R2) by XBOOLE_0:def 10;
InnerVertices S1 = rng R1 & InnerVertices S2 = rng R2 &
InnerVertices S = rng R by MSAFREE2:def 3;
hence InnerVertices S = (InnerVertices S1) \/ (InnerVertices S2)
by A3,XBOOLE_0:def 10;
let x be set; assume x in InputVertices S;
then x in (the carrier of S) \ rng R by MSAFREE2:def 2;
then x in the carrier of S & not x in rng R by XBOOLE_0:def 4;
then (x in the carrier of S1 or x in the carrier of S2) &
not x in rng R1 & not x in rng R2 by A2,A4,XBOOLE_0:def 2;
then x in (the carrier of S1) \ rng R1 or
x in (the carrier of S2) \ rng R2 by XBOOLE_0:def 4;
then x in InputVertices S1 or x in InputVertices S2 by MSAFREE2:def 2;
hence thesis by XBOOLE_0:def 2;
end;
theorem Th16:
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;
R = R1+*R2 by Def2;
then A1: rng R2 c= rng R by FUNCT_4:19;
let v2 be Vertex of S2; assume v2 in InputVertices S;
then v2 in (the carrier of S) \ rng R by MSAFREE2:def 2;
then not v2 in rng R2 by A1,XBOOLE_0:def 4;
then v2 in (the carrier of S2) \ rng R2 by XBOOLE_0:def 4;
hence thesis by MSAFREE2:def 2;
end;
theorem Th17:
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
A1: the Arity of S1 tolerates the Arity of S2 &
the ResultSort of S1 tolerates the ResultSort of S2;
set R1 = the ResultSort of S1, R2 = the ResultSort of S2;
set S = S1+*S2, R = the ResultSort of S;
R = R1+*R2 by Def2;
then R1 c= R by A1,FUNCT_4:29;
then A2: rng R1 c= rng R by RELAT_1:25;
let v1 be Vertex of S1; assume v1 in InputVertices S;
then v1 in (the carrier of S) \ rng R by MSAFREE2:def 2;
then not v1 in rng R1 by A2,XBOOLE_0:def 4;
then v1 in (the carrier of S1) \ rng R1 by XBOOLE_0:def 4;
hence thesis by MSAFREE2:def 2;
end;
theorem Th18:
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 OperSymbols of S2 &
dom the ResultSort of S2 = the OperSymbols of S2 &
o2 in the OperSymbols of S2 by Lm2,FUNCT_2:def 1;
A3: the Arity of S1+*S2 = (the Arity of S1)+*(the Arity of S2) &
the ResultSort of S1+*S2 = (the ResultSort of S1)+*(the ResultSort of S2)
by Def2;
thus the_arity_of o = (the Arity of S1+*S2).o by MSUALG_1:def 6
.= (the Arity of S2).o2 by A1,A2,A3,FUNCT_4:14
.= the_arity_of o2 by MSUALG_1:def 6;
thus the_result_sort_of o = (the ResultSort of S1+*S2).o by MSUALG_1:def 7
.= (the ResultSort of S2).o2 by A1,A2,A3,FUNCT_4:14
.= the_result_sort_of o2 by MSUALG_1:def 7;
end;
theorem Th19:
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;
let v be Vertex of S such that
A3: v2 = v;
the ResultSort of S = (the ResultSort of S1)+*the ResultSort of S2 &
InnerVertices S2 = rng the ResultSort of S2 &
InnerVertices S = rng the ResultSort of S by A1,Def2,MSAFREE2:def 3;
then A4: InnerVertices S2 c= InnerVertices S by FUNCT_4:19;
hence v in InnerVertices S by A2,A3;
A5: the_result_sort_of action_at v2 = v2 &
the_result_sort_of action_at v = v by A2,A3,A4,MSAFREE2:def 7;
the OperSymbols of S = (the OperSymbols of S1) \/ the OperSymbols of S2 &
action_at v2 in the OperSymbols of S2 by A1,Def2,Lm2;
then reconsider o = action_at v2 as OperSymbol of S by XBOOLE_0:def 2;
v = the_result_sort_of o by A1,A3,A5,Th18;
hence thesis by A2,A3,A4,MSAFREE2:def 7;
end;
theorem Th20:
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 &
the ResultSort of S1 tolerates the ResultSort of S2;
let o1 be OperSymbol of S1, o be OperSymbol of S1+*S2; assume
A2: o1 = o;
A3: dom the Arity of S1 = the OperSymbols of S1 &
dom the ResultSort of S1 = the OperSymbols of S1 &
o1 in the OperSymbols of S1 by Lm2,FUNCT_2:def 1;
A4: the Arity of S1+*S2 = (the Arity of S1)+*(the Arity of S2) &
the ResultSort of S1+*S2 = (the ResultSort of S1)+*(the ResultSort of S2)
by Def2;
thus the_arity_of o = (the Arity of S1+*S2).o by MSUALG_1:def 6
.= (the Arity of S1).o1 by A1,A2,A3,A4,FUNCT_4:16
.= the_arity_of o1 by MSUALG_1:def 6;
thus the_result_sort_of o = (the ResultSort of S1+*S2).o by MSUALG_1:def 7
.= (the ResultSort of S1).o1 by A1,A2,A3,A4,FUNCT_4:16
.= the_result_sort_of o1 by MSUALG_1:def 7;
end;
theorem Th21:
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,Th15;
hence A5: v in InnerVertices S by A3,A4,XBOOLE_0:def 2;
then A6: the_result_sort_of action_at v1 = v1 &
the_result_sort_of action_at v = v by A3,MSAFREE2:def 7;
the OperSymbols of S = (the OperSymbols of S1) \/ the OperSymbols of S2 &
action_at v1 in the OperSymbols of S1 by A2,Def2,Lm2;
then reconsider o = action_at v1 as OperSymbol of S by XBOOLE_0:def 2;
v = the_result_sort_of o by A1,A2,A4,A6,Th20;
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 :Def3:
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 S = S1+*S2;
A2: the carrier of S = (the carrier of S1) \/ (the carrier of S2) &
the OperSymbols of S = (the OperSymbols of S1) \/ (the OperSymbols of S2)&
the Arity of S = (the Arity of S1) +* (the Arity of S2) &
the ResultSort of S = (the ResultSort of S1) +* (the ResultSort of S2)
by Def2;
reconsider SORTS = (the Sorts of A1)+*the Sorts of A2
as non-empty ManySortedSet of the carrier of S1+*S2 by Def2;
set SA1 = the Sorts of A1, SA2 = the Sorts of A2;
set I = the carrier of S,
I1 = the carrier of S1, I2 = the carrier of S2;
set SA12 = SA1#+*(SA2# );
set CHARACT = (the Charact of A1) +* (the Charact of A2);
A3: CHARACT is ManySortedFunction of
(SA1#*the Arity of S1)+*(SA2#*the Arity of S2),
(SA1*the ResultSort of S1)+*(SA2*the ResultSort of S2) by Lm3;
A4: dom (SA1# ) = I1* & dom (SA2# ) = I2* & dom SA1 = I1 & dom SA2 = I2 &
dom (SORTS# ) = I* & dom SORTS = I by PBOOLE:def 3;
A5: rng the Arity of S1 c= I1* & rng the Arity of S2 c= I2* &
rng the Arity of S c= I* &
rng the ResultSort of S1 c= I1 & rng the ResultSort of S2 c= I2
by RELSET_1:12;
then A6: (rng the Arity of S1) \/ rng the Arity of S2 c= I1* \/ (I2*
) by XBOOLE_1:13;
SORTS = SA1 \/ SA2 by A1,FUNCT_4:31;
then A7: SA1 c= SORTS & SA2 c= SORTS by XBOOLE_1:7;
A8: SA1# tolerates SA2#
proof let x be set; assume
A9: x in (dom (SA1# )) /\ dom (SA2# );
then reconsider i1 = x as Element of I1* by A4,XBOOLE_0:def 3;
reconsider i2 = x as Element of I2* by A4,A9,XBOOLE_0:def 3;
A10: rng i1 c= I1 & rng i2 c= I2 by FINSEQ_1:def 4;
thus SA1#.x = product (SA1*i1) by MSUALG_1:def 3
.= product (SA2*i2) by A1,A4,A10,Th2
.= SA2#.x by MSUALG_1:def 3;
end;
then SA12 = SA1# \/ (SA2# ) & SA1# c= SORTS# & SA2# c= SORTS#
by A7,Th3,FUNCT_4:31;
then SA12 c= SORTS# by XBOOLE_1:8;
then A11: SA12 tolerates SORTS# by PARTFUN1:135;
rng the Arity of S c= (rng the Arity of S1) \/ rng the Arity of S2 &
dom SA12 = I1* \/ (I2* ) by A2,FUNCT_4:18,PBOOLE:def 3;
then A12: rng the Arity of S c= dom SA12 by A6,XBOOLE_1:1;
(SA1#+*(SA2# ))*((the Arity of S1)+*the Arity of S2) =
(SA1#*the Arity of S1)+*(SA2#*the Arity of S2) &
(SA1+*SA2)*((the ResultSort of S1)+*the ResultSort of S2) =
(SA1*the ResultSort of S1)+*(SA2*the ResultSort of S2)
by A1,A4,A5,A8,Th1;
then reconsider CHARACT as ManySortedFunction of
SORTS#*the Arity of S, SORTS*the ResultSort of S by A2,A3,A4,A5,A11,A12,
Th2;
reconsider A = MSAlgebra(#SORTS, CHARACT#) as
strict non-empty MSAlgebra over S by MSUALG_1:def 8;
take A; thus thesis;
end;
end;
theorem
for S being non void non empty ManySortedSign,
A being MSAlgebra over S holds A tolerates A
proof let S be non void non empty ManySortedSign, A be MSAlgebra over S;
thus S tolerates S; thus thesis;
end;
theorem Th23:
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
proof let S1,S2 be non void non empty ManySortedSign;
let A1 be MSAlgebra over S1;
let A2 be MSAlgebra over S2;
assume S1 tolerates S2 & the Sorts of A1 tolerates the Sorts of A2 &
the Charact of A1 tolerates the Charact of A2;
hence S2 tolerates S1 & the Sorts of A2 tolerates the Sorts of A1 &
the Charact of A2 tolerates the Charact of A1;
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 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 & the Sorts of A1 tolerates the Sorts of A2 &
the Charact of A1 tolerates the Charact of A2 and
A2: S2 tolerates S3 & the Sorts of A2 tolerates the Sorts of A3 &
the Charact of A2 tolerates the Charact of A3 and
A3: S3 tolerates S1 & the Sorts of A3 tolerates the Sorts of A1 &
the Charact of A3 tolerates the Charact of A1;
thus S1+*S2 tolerates S3 by A1,A2,A3,Th7;
the Sorts of A1+*A2 = (the Sorts of A1)+*the Sorts of A2 by A1,Def4;
hence the Sorts of A1+*A2 tolerates the Sorts of A3 by A1,A2,A3,Th5;
the Charact of A1+*A2 = (the Charact of A1)+*the Charact of A2
by A1,Def4;
hence thesis by A1,A2,A3,Th5;
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 A' = the MSAlgebra of A;
set SA = the Sorts of A', CA = the Charact of A';
set SAA = the Sorts of A+*A, CAA = the Charact of A+*A;
SA = SA+*SA & CA = CA+*CA;
then A+*A = MSAlgebra(#SAA, CAA#) & A' = MSAlgebra(#SA, CA#) & S = S+*S &
SAA = SA & CAA = CA by Def4,Th8;
hence thesis;
end;
theorem Th26:
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
A1: S1 tolerates S2 & the Sorts of A1 tolerates the Sorts of A2 &
the Charact of A1 tolerates the Charact of A2;
then (the Sorts of A1)+*the Sorts of A2 = (the Sorts of A2)+*the Sorts of
A1 &
(the Charact of A1)+*the Charact of A2
= (the Charact of A2)+*the Charact of A1 by FUNCT_4:35;
then S1+*S2 = S2+*S1 & the Sorts of A2 tolerates the Sorts of A1 &
the Sorts of A = (the Sorts of A2) +* (the Sorts of A1) &
the Charact of A = (the Charact of A2) +* (the Charact of A1)
by A1,Def4,Th9;
hence thesis by 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 s1 = the Sorts of A1, s2 = the Sorts of A2, s3 = the Sorts of A3;
set A12 = A1+*A2, A23 = A2+*A3;
set A12'3 = A12+*A3, A1'23 = A1+*A23;
A4: the Sorts of A12 = (the Sorts of A1) +* (the Sorts of A2) &
the Charact of A12 = (the Charact of A1) +* (the Charact of A2)
by A1,Def4;
A5: the Sorts of A23 = (the Sorts of A2) +* (the Sorts of A3) &
the Charact of A23 = (the Charact of A2) +* (the Charact of A3)
by A2,Def4;
the Sorts of A12 tolerates the Sorts of A3
proof let x be set; assume x in (dom the Sorts of A12) /\ dom s3;
then x in dom the Sorts of A12 & x in dom s3 by XBOOLE_0:def 3;
then (x in dom s1 or x in dom s2) & x in dom s3 by A4,FUNCT_4:13;
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,FUNCT_4:14,16,XBOOLE_0
:def 3;
hence thesis by A2,A3,A4,PARTFUN1:def 6;
end;
then A6: the Sorts of A12'3 = (the Sorts of A12) +* (the Sorts of A3) &
the Charact of A12'3 = (the Charact of A12) +* (the Charact of A3)
by Def4;
the Sorts of A1 tolerates the Sorts of A23
proof let x be set; assume x in (dom s1) /\ dom the Sorts of A23;
then x in dom the Sorts of A23 & x in dom s1 by XBOOLE_0:def 3;
then (x in dom s2 or x in dom s3) & x in dom s1 by A5,FUNCT_4:13;
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,FUNCT_4:14,16,XBOOLE_0:def 3;
hence thesis by A1,A3,A5,PARTFUN1:def 6;
end;
then the Sorts of A1'23 = (the Sorts of A1) +* (the Sorts of A23) &
the Charact of A1'23 = (the Charact of A1) +* (the Charact of A23)
by Def4;
then the Sorts of A12'3 = the Sorts of A1'23 &
the Charact of A12'3 = the Charact of A1'23 by A4,A5,A6,FUNCT_4:15;
hence thesis by Th10;
end;
theorem
for S1,S2 being non empty ManySortedSign
for A1 being locally-finite non-empty MSAlgebra over S1
for A2 being locally-finite non-empty MSAlgebra over S2 st
the Sorts of A1 tolerates the Sorts of A2 holds A1+*A2 is locally-finite
proof let S1,S2 be non empty ManySortedSign;
let A1 be locally-finite non-empty MSAlgebra over S1,
A2 be locally-finite non-empty MSAlgebra over S2 such that
A1: the Sorts of A1 tolerates the Sorts of A2;
set A = A1+*A2;
let x be set; assume x in the carrier of S1+*S2;
then reconsider x as Vertex of S1+*S2;
set SA = the Sorts of A, SA1 = the Sorts of A1, SA2 = the Sorts of A2;
A2: dom SA = the carrier of S1+*S2 & dom SA1 = the carrier of S1 &
dom SA2 = the carrier of S2 by PBOOLE:def 3;
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 2;
SA = SA1+*SA2 & SA1 is locally-finite & SA2 is locally-finite
by A1,Def4,MSAFREE2:def 11;
then SA.x = SA1.x & SA1.x is finite or SA.x = SA2.x & SA2.x is finite
by A1,A2,A3,FUNCT_4:14,16,PRE_CIRC:def 3;
hence thesis;
end;
theorem Th29:
for f,g being non-empty Function, x being Element of product f,
y being Element of product g holds x+*y in product (f+*g)
proof let f,g be non-empty Function, x be Element of product f;
let y be Element of product g;
A1: dom x = dom f & dom y = dom g by CARD_3:18;
then A2: dom (x+*y) = dom f \/ dom g & dom (f+*g) = dom f \/
dom g by FUNCT_4:def 1;
now let z be set; assume
A3: z in dom (f+*g);
then z in dom g or not z in dom g & z in dom f by A2,XBOOLE_0:def 2;
then (x+*y).z = x.z & (f+*g).z = f.z & x.z in f.z or
(x+*y).z = y.z & (f+*g).z = g.z & y.z in g.z
by A1,A2,A3,CARD_3:18,FUNCT_4:def 1;
hence (x+*y).z in (f+*g).z;
end;
hence x+*y in product (f+*g) by A2,CARD_3:18;
end;
theorem Th30:
for f,g being non-empty Function
for x being Element of product (f+*g) holds x|dom g in product g
proof let f,g be non-empty Function;
let x be Element of product (f+*g);
A1: dom x = dom (f+*g) & dom (f+*g) = dom f \/ dom g
by CARD_3:18,FUNCT_4:def 1;
then A2: dom g c= dom x by XBOOLE_1:7;
then A3: dom (x|dom g) = dom g by RELAT_1:91;
now let z be set; assume
z in dom (x|dom g);
then (x|dom g).z = x.z & z in dom (f+*g) & (f+*g).z = g.z
by A1,A2,A3,FUNCT_1:70,FUNCT_4:14;
hence (x|dom g).z in g.z by CARD_3:18;
end;
hence x|dom g in product g by A3,CARD_3:18;
end;
theorem Th31:
for f,g being non-empty Function st f tolerates g
for x being Element of product (f+*g) holds x|dom f in product f
proof let f,g be non-empty Function such that
A1: f tolerates g;
let x be Element of product (f+*g);
A2: dom x = dom (f+*g) & dom (f+*g) = dom f \/ dom g
by CARD_3:18,FUNCT_4:def 1;
then A3: dom f c= dom x by XBOOLE_1:7;
then A4: dom (x|dom f) = dom f by RELAT_1:91;
now let z be set; assume
z in dom (x|dom f);
then (x|dom f).z = x.z & z in dom (f+*g) & (f+*g).z = f.z
by A1,A2,A3,A4,FUNCT_1:70,FUNCT_4:16;
hence (x|dom f).z in f.z by CARD_3:18;
end;
hence x|dom f in product f by A4,CARD_3:18;
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 Th29;
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;
assume
A1: the Sorts of A1 tolerates the Sorts of A2;
then A2: the Sorts of A1+*A2 = (the Sorts of A1)+*the Sorts of A2 by Def4;
dom the Sorts of A1 = the carrier of S1 &
dom the Sorts of A2 = the carrier of S2 by PBOOLE:def 3;
hence thesis by A1,A2,Th30,Th31;
end;
theorem Th34:
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; assume
the Sorts of A1 tolerates the Sorts of A2;
then A1: the Charact of A1+*A2 = (the Charact of A1)+*the Charact of A2 by
Def4;
set A = A1+*A2;
let o be OperSymbol of S1+*S2, o2 be OperSymbol of S2; assume
A2: o = o2;
A3: dom the Charact of A2 = the OperSymbols of S2 by PBOOLE:def 3;
A4: o2 in the OperSymbols of S2 by Lm2;
thus Den(o, A) = (the Charact of A).o by MSUALG_1:def 11
.= (the Charact of A2).o2 by A1,A2,A3,A4,FUNCT_4:14
.= Den(o2, A2) by MSUALG_1:def 11;
end;
theorem Th35:
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;
assume the Sorts of A1 tolerates the Sorts of A2;
then A1: the Charact of A1+*A2 = (the Charact of A1)+*the Charact of A2 by
Def4;
assume
A2: the Charact of A1 tolerates the Charact of A2;
set A = A1+*A2;
let o be OperSymbol of S1+*S2, o1 be OperSymbol of S1; assume
A3: o = o1;
A4: dom the Charact of A1 = the OperSymbols of S1 by PBOOLE:def 3;
A5: o1 in the OperSymbols of S1 by Lm2;
thus Den(o, A) = (the Charact of A).o by MSUALG_1:def 11
.= (the Charact of A1).o1 by A1,A2,A3,A4,A5,FUNCT_4:16
.= Den(o1, A1) by MSUALG_1:def 11;
end;
theorem Th36:
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;
(rng the_arity_of o2)|the_arity_of o2 = the_arity_of o2 &
rng the_arity_of o2 c= the carrier of S2 by FINSEQ_1:def 4,RELAT_1:125;
then (the carrier of S2)|the_arity_of o2 c= the_arity_of o2 &
the_arity_of o2 c= (the carrier of S2)|the_arity_of o2
by RELAT_1:117,131;
then A4: (the carrier of S2)|the_arity_of o2 = the_arity_of o2 by XBOOLE_0:def
10;
thus o depends_on_in s = s*the_arity_of o by CIRCUIT1:def 3
.= s*the_arity_of o2 by A1,A3,Th18
.= s2*the_arity_of o2 by A2,A4,MONOID_1:2
.= o2 depends_on_in s2 by CIRCUIT1:def 3;
end;
theorem Th37:
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;
(rng the_arity_of o1)|the_arity_of o1 = the_arity_of o1 &
rng the_arity_of o1 c= the carrier of S1 by FINSEQ_1:def 4,RELAT_1:125;
then (the carrier of S1)|the_arity_of o1 c= the_arity_of o1 &
the_arity_of o1 c= (the carrier of S1)|the_arity_of o1
by RELAT_1:117,131;
then A5: (the carrier of S1)|the_arity_of o1 = the_arity_of o1 by XBOOLE_0:def
10;
thus o depends_on_in s = s*the_arity_of o by CIRCUIT1:def 3
.= s*the_arity_of o1 by A1,A2,A4,Th20
.= s1*the_arity_of o1 by A3,A5,MONOID_1:2
.= o1 depends_on_in s1 by CIRCUIT1:def 3;
end;
theorem Th38:
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 & the Sorts of A1 tolerates the Sorts of A2 &
the Charact of A1 tolerates the Charact of A2 and
A3: A = A1+*A2;
let s be State of A, v be Vertex of S;
hereby let s1 be State of A1 such that
A4: s1 = s|the carrier of S1;
A5: now assume v in InnerVertices S1;
then reconsider v1 = v as Element of InnerVertices S1;
A6: action_at v = action_at v1 & v1 in InnerVertices S by A1,A2,Th21;
then A7: (Following s).v = (Den (action_at v, A)).(action_at v depends_on_in
s) &
(Following s1).v1 =
(Den (action_at v1, A1)).(action_at v1 depends_on_in s1)
by CIRCUIT2:def 5;
Den (action_at v1, A1) = Den (action_at v, A) by A1,A2,A3,A6,Th35;
hence (Following s).v = (Following s1).v by A1,A2,A4,A6,A7,Th37;
end;
now assume
A8: v in the carrier of S1 & v in InputVertices S;
then reconsider v1 = v as Vertex of S1;
v1 in InputVertices S1 by A1,A2,A8,Th17;
then A9: (Following s).v = s.v & (Following s1).v1 = s1.v1 by A8,CIRCUIT2:def
5;
dom s1 = the carrier of S1 by CIRCUIT1:4;
hence (Following s).v = (Following s1).v by A4,A9,FUNCT_1:70;
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 A5;
end;
let s2 be State of A2 such that
A10: s2 = s|the carrier of S2;
A11: now assume v in InnerVertices S2;
then reconsider v2 = v as Element of InnerVertices S2;
A12: action_at v = action_at v2 & v2 in InnerVertices S by A1,Th19;
then A13: (Following s).v = (Den (action_at v, A)).(action_at v depends_on_in
s) &
(Following s2).v2 =
(Den (action_at v2, A2)).(action_at v2 depends_on_in s2)
by CIRCUIT2:def 5;
Den (action_at v2, A2) = Den (action_at v, A) by A1,A2,A3,A12,Th34;
hence (Following s).v = (Following s2).v by A1,A10,A12,A13,Th36;
end;
now assume
A14: v in the carrier of S2 & v in InputVertices S;
then reconsider v2 = v as Vertex of S2;
v2 in InputVertices S2 by A1,A14,Th16;
then A15: (Following s).v = s.v & (Following s2).v2 = s2.v2 by A14,CIRCUIT2:
def 5;
dom s2 = the carrier of S2 by CIRCUIT1:4;
hence (Following s).v = (Following s2).v by A10,A15,FUNCT_1:70;
end;
hence thesis by A11;
end;
theorem Th39:
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
A1: InnerVertices S1 misses InputVertices S2 & S = S1+*S2;
then A2: the carrier of S = (the carrier of S1) \/ the carrier of S2 by 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
A3: A1 tolerates A2 and
A4: A = A1+*A2;
let s be State of A, s1 be State of A1, s2 be State of A2 such that
A5: s1 = s|the carrier of S1 & s2 = s|the carrier of S2;
A6: dom Following s = the carrier of S & dom Following s1 = the carrier of S1
&
dom Following s2 = the carrier of S2 by CIRCUIT1:4;
now let x be set; assume x in (dom Following s1) \/ dom Following s2;
then reconsider v = x as Vertex of S by A1,A6,Def2;
hereby assume x in dom Following s2;
then reconsider v2 = x as Vertex of S2 by CIRCUIT1:4;
InputVertices S2 \/ InnerVertices S2 = the carrier of S2
by MSAFREE2:3;
then A7: v2 in InnerVertices S2 or v2 in InputVertices S2 by XBOOLE_0:def 2
;
now assume v2 in InputVertices S2;
then v2 in (the carrier of S2) \ rng the ResultSort of S2 &
not v2 in InnerVertices S1 by A1,MSAFREE2:def 2,XBOOLE_0:3;
then A8: not v2 in rng the ResultSort of S2 &
not v2 in rng the ResultSort of S1 by MSAFREE2:def 3,XBOOLE_0:def 4;
the ResultSort of S = (the ResultSort of S1)+*the ResultSort of S2
by A1,Def2;
then rng the ResultSort of S c=
(rng the ResultSort of S1) \/ rng the ResultSort of S2
by FUNCT_4:18;
then not v in rng the ResultSort of S by A8,XBOOLE_0:def 2;
then v in (the carrier of S) \ rng the ResultSort of S by XBOOLE_0:def
4;
hence v in InputVertices S by MSAFREE2:def 2;
end;
then v in InnerVertices S2 or v in the carrier of S2 & v in
InputVertices S
by A7;
hence (Following s).x = (Following s2).x by A1,A3,A4,A5,Th38;
end;
assume
A9: not x in dom Following s2;
then reconsider v1 = v as Vertex of S1 by A2,A6,XBOOLE_0:def 2;
InputVertices S1 \/ InnerVertices S1 = the carrier of S1
by MSAFREE2:3;
then A10: v1 in InnerVertices S1 or v1 in InputVertices S1 by XBOOLE_0:def 2
;
rng the ResultSort of S2 c= the carrier of S2
by RELSET_1:12;
then A11: not v1 in rng the ResultSort of S2 by A6,A9;
now assume v1 in InputVertices S1;
then v1 in (the carrier of S1) \ rng the ResultSort of S1
by MSAFREE2:def 2;
then A12: not v1 in rng the ResultSort of S1 by XBOOLE_0:def 4;
the ResultSort of S = (the ResultSort of S1)+*the ResultSort of S2
by A1,Def2;
then rng the ResultSort of S c=
(rng the ResultSort of S1) \/ rng the ResultSort of S2
by FUNCT_4:18;
then not v in rng the ResultSort of S by A11,A12,XBOOLE_0:def 2;
then v in (the carrier of S) \ rng the ResultSort of S by XBOOLE_0:def
4;
hence v in InputVertices S by MSAFREE2:def 2;
end;
hence (Following s).x = (Following s1).x by A1,A3,A4,A5,A10,Th38;
end;
hence Following s = (Following s1)+*(Following s2)
by A2,A6,FUNCT_4:def 1;
end;
theorem Th40:
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 & 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: A1 tolerates A2 and
A3: A = A1+*A2;
S1 tolerates S2 by A2,Def3;
then S = S2+*S1 & A = A2+*A1 & A2 tolerates A1 by A1,A2,A3,Th9,Th23,Th26;
hence thesis by A1,Th39;
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) such that
A1: InputVertices S1 c= InputVertices S2;
InputVertices S2 misses InnerVertices S2 by MSAFREE2:4;
then InnerVertices S2 misses InputVertices S1 by A1,XBOOLE_1:63;
hence thesis by Th40;
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) such that
A1: InputVertices S2 c= InputVertices S1;
InputVertices S1 misses InnerVertices S1 by MSAFREE2:4;
then InnerVertices S1 misses InputVertices S2 by A1,XBOOLE_1:63;
hence thesis by Th39;
end;
begin :: ManySortedSign with One Operation
definition
let A,B be non empty set;
let a be Element of A;
redefine func B --> a -> Function of B,A;
coherence by FUNCOP_1:57;
end;
definition
let f be set;
let p be FinSequence;
let x be set;
func 1GateCircStr(p,f,x) -> non void strict ManySortedSign means:
Def5:
the carrier of it = (rng p) \/ {x} &
the OperSymbols of it = {[p,f]} &
(the Arity of it).[p,f] = p &
(the ResultSort of it).[p,f] = x;
existence
proof
A1: x in {x} by TARSKI:def 1;
reconsider C = (rng p) \/ {x} as non empty set;
reconsider ox = x as Element of C by A1,XBOOLE_0:def 2;
set pf = [p,f];
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 A = {pf} --> pp as Function of {pf}, C*;
reconsider R = {pf} --> ox as Function of {pf}, C;
reconsider S = ManySortedSign(#C, {pf}, A, R#) as
non void strict ManySortedSign by MSUALG_1:def 5;
take S;
pf in {pf} by TARSKI:def 1;
hence thesis by FUNCOP_1:13;
end;
uniqueness
proof let S1,S2 be non void strict ManySortedSign; assume
A2: not thesis;
then dom the Arity of S1 = {[p,f]} & dom the Arity of S2 = {[p,f]} &
dom the ResultSort of S1 = {[p,f]} & dom the ResultSort of S2 = {[p,f]}
by FUNCT_2:def 1;
then the Arity of S1 = {[[p,f],p]} & the Arity of S2 = {[[p,f],p]} &
the ResultSort of S1 = {[[p,f],x]} &
the ResultSort of S2 = {[[p,f],x]} by A2,GRFUNC_1:18;
hence thesis by A2;
end;
end;
definition
let f be set;
let p be FinSequence;
let x be set;
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 Th43:
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);
A1: the OperSymbols of S = {[p,f]} &
(the Arity of S).[p,f] = p &
(the ResultSort of S).[p,f] = x by Def5;
then A2: dom the Arity of S = {[p,f]} & dom the ResultSort of S = {[p,f]}
by FUNCT_2:def 1;
for x being set st x in {[p,f]} holds (the Arity of S).x = p
by A1,TARSKI:def 1;
hence the Arity of S = {[p,f]} --> p by A2,FUNCOP_1:17;
for y being set st y in {[p,f]} holds (the ResultSort of S).y = x
by A1,TARSKI:def 1;
hence thesis by A2,FUNCOP_1:17;
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 OperSymbols of S = {[p,f]} &
(the Arity of S).[p,f] = p &
(the ResultSort of S).[p,f] = x by Def5;
hence o = [p,f] by TARSKI:def 1;
hence thesis by A1,MSUALG_1:def 6,def 7;
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 OperSymbols of 1GateCircStr(p,f,x) is non empty &
the ResultSort of 1GateCircStr(p,f,x) = {[p,f]} --> x
by Th43,MSUALG_1:def 5;
then A1: rng the ResultSort of 1GateCircStr(p,f,x) = {x} by FUNCOP_1:14;
the carrier of 1GateCircStr(p,f,x) = (rng p) \/ {x} by Def5;
then InputVertices 1GateCircStr(p,f,x) = ((rng p) \/ {x}) \ {x}
by A1,MSAFREE2:def 2;
hence thesis by A1,MSAFREE2:def 3,XBOOLE_1:40;
end;
definition
let f be set;
let p be FinSequence;
func 1GateCircStr(p,f) -> non void strict ManySortedSign means:
Def6:
the carrier of it = (rng p) \/ {[p,f]} &
the OperSymbols 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;
definition
let f be set;
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);
the carrier of S = (rng p) \/ {[p,f]} &
the OperSymbols of S = {[p,f]} &
(the Arity of S).[p,f] = p &
(the ResultSort of S).[p,f] = [p,f] by Def6;
hence thesis by Def5;
end;
theorem Th47:
for f being set, 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, p be FinSequence; set S = 1GateCircStr(p,f);
A1: the OperSymbols of S = {[p,f]} &
(the Arity of S).[p,f] = p &
(the ResultSort of S).[p,f] = [p,f] by Def6;
then A2: dom the Arity of S = {[p,f]} & dom the ResultSort of S = {[p,f]}
by FUNCT_2:def 1;
for x being set st x in {[p,f]} holds (the Arity of S).x = p
by A1,TARSKI:def 1;
hence the Arity of 1GateCircStr(p,f) = {[p,f]} --> p by A2,FUNCOP_1:17;
for x being set st x in {[p,f]} holds (the ResultSort of S).x = [p,f]
by A1,TARSKI:def 1;
hence thesis by A2,FUNCOP_1:17;
end;
theorem Th48:
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);
A1: the OperSymbols of S = {[p,f]} &
(the Arity of S).[p,f] = p &
(the ResultSort of S).[p,f] = [p,f] by Def6;
hence o = [p,f] by TARSKI:def 1;
hence thesis by A1,MSUALG_1:def 6,def 7;
end;
theorem Th49:
for f being set, p being FinSequence holds
InputVertices 1GateCircStr(p,f) = rng p &
InnerVertices 1GateCircStr(p,f) = {[p,f]}
proof let f be set; let p be FinSequence;
the OperSymbols of 1GateCircStr(p,f) is non empty &
the ResultSort of 1GateCircStr(p,f) = {[p,f]} --> [p,f]
by Th47,MSUALG_1:def 5;
then A1: rng the ResultSort of 1GateCircStr(p,f) = {[p,f]} by FUNCOP_1:14;
A2: the carrier of 1GateCircStr(p,f) = (rng p) \/ {[p,f]} by Def6;
A3: now assume [p,f] in rng p; then consider x being set such that
A4: [x,[p,f]] in p by RELAT_1:def 5;
p in {p,f} & {p,f} in {{p,f},{p}} & {{p,f},{p}} = [p,f] &
[p,f] in {x,[p,f]} & {x,[p,f]} in {{x,[p,f]},{x}} &
{{x,[p,f]},{x}} = [x,[p,f]] by TARSKI:def 2,def 5;
hence contradiction by A4,ORDINAL1:5;
end;
A5: InputVertices 1GateCircStr(p,f) = ((rng p) \/ {[p,f]}) \ {[p,f]}
by A1,A2,MSAFREE2:def 2;
hence InputVertices 1GateCircStr(p,f) c= rng p by XBOOLE_1:43;
thus rng p c= InputVertices 1GateCircStr(p,f)
proof let x be set; assume x in rng p;
then not x in {[p,f]} & x in
(rng p) \/ {[p,f]} by A3,TARSKI:def 1,XBOOLE_0:def 2;
hence thesis by A5,XBOOLE_0:def 4;
end;
thus thesis by A1,MSAFREE2:def 3;
end;
theorem
for f being set, p being FinSequence
for x being set st x in rng p holds the_rank_of x in the_rank_of [p,f]
proof let f be set; let p be FinSequence;
let y be set; assume y in rng p; then consider x being set such that
A1: [x,y] in p by RELAT_1:def 5;
p in {p,f} & {p,f} in {{p,f},{p}} & {{p,f},{p}} = [p,f] &
y in {x,y} & {x,y} in {{x,y},{x}} & {{x,y},{x}} = [x,y]
by TARSKI:def 2,def 5;
then the_rank_of y in the_rank_of {x,y} &
the_rank_of {x,y} in the_rank_of [x,y] &
the_rank_of p in the_rank_of {p,f} &
the_rank_of {p,f} in the_rank_of [p,f] by CLASSES1:76;
then A2: the_rank_of y in the_rank_of [x,y] &
the_rank_of [x,y] in the_rank_of p &
the_rank_of p in the_rank_of [p,f] by A1,CLASSES1:76,ORDINAL1:19;
then the_rank_of y in the_rank_of p by ORDINAL1:19;
hence thesis by A2,ORDINAL1:19;
end;
theorem Th51:
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: the Arity of S1 = {[p,f]} --> p & the Arity of S2 = {[q,f]} --> q by Th47;
A2: the ResultSort of S1 = {[p,f]} --> [p,f] &
the ResultSort of S2 = {[q,f]} --> [q,f] by Th47;
A3: [p,f] <> [q,f] implies {[p,f]} misses {[q,f]} by ZFMISC_1:17;
hence the Arity of S1 tolerates the Arity of S2 by A1,Th4,ZFMISC_1:33;
thus thesis by A2,A3,Th4;
end;
begin :: Unsplit condition
definition let IT be ManySortedSign;
attr IT is unsplit means:
Def7:
the ResultSort of IT = id the OperSymbols of IT;
attr IT is gate`1=arity means:
Def8:
for g being set st g in the OperSymbols 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 OperSymbols 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:
Def10:
for g being set st g in the OperSymbols 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;
_MSSLambdaWeak {A,B() -> set, g() -> Function of A(),B(), f(set,set) -> set}:
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(set) = f($1,g().$1);
consider f being Function such that
A1: dom f = A() and
A2: for a being set st a in A() holds f.a = F(a) from Lambda;
reconsider f as ManySortedSet of A() by A1,PBOOLE:def 3;
take f;
thus thesis by A2;
end;
Lemma {S() -> non empty ManySortedSign, F(set,set) -> set}:
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 OperSymbols 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 OperSymbols 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;
deffunc G(set,set) = F($1,$2);
consider CHARACT being ManySortedSet of the OperSymbols of S such that
A2: for o being set, p being Element of (the carrier of S)* st
o in the OperSymbols of S & p = (the Arity of S).o holds
CHARACT.o = G(o,p) from _MSSLambdaWeak;
A3: dom CHARACT = the OperSymbols of S &
dom the Arity of S = the OperSymbols of S &
dom the ResultSort of S = the OperSymbols of S by FUNCT_2:def 1,PBOOLE:def
3;
CHARACT is Function-yielding
proof let x be set; assume
A4: x in dom CHARACT;
then reconsider o = x as Gate of S by PBOOLE:def 3;
reconsider p = (the Arity of S).o as Element of (the carrier of S)*
by A3,A4,FUNCT_2:7;
CHARACT.x = F(o,p) by A2,A3,A4;
hence thesis by A1,A3,A4;
end;
then reconsider CHARACT as ManySortedFunction of the OperSymbols of S;
now let i be set; assume
A5: i in the OperSymbols 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 A5,FUNCT_2:7;
reconsider v = (the ResultSort of S).o as Vertex of S
by A5,FUNCT_2:7;
SORTS.v = BOOLEAN by FUNCOP_1:13;
then CHARACT.i = F(o,p) & (SORTS#*the Arity of S).i = SORTS#.p &
SORTS#.p = (len p)-tuples_on BOOLEAN &
(SORTS*the ResultSort of S).i = BOOLEAN
by A2,A3,A5,Th6,FUNCT_1:23;
hence CHARACT.i is Function of
(SORTS#*the Arity of S).i, (SORTS*the ResultSort of S).i by A1,A5;
end;
then reconsider CHARACT as ManySortedFunction of
SORTS#*the Arity of S, SORTS*the ResultSort of S by MSUALG_1:def 2;
take MSAlgebra(#SORTS, CHARACT#); thus thesis by A2;
end;
definition
cluster gate`2isBoolean -> gate`2=den (non empty ManySortedSign);
coherence
proof let S be non empty ManySortedSign; assume
A1: for g being set st g in the OperSymbols 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];
deffunc F(set,set) = $1`2;
A2: now let g be set, p be Element of (the carrier of S)*; assume
g in the OperSymbols of S & p = (the Arity of S).g;
then consider f being Function of (len p)-tuples_on BOOLEAN, BOOLEAN such
that
A3: g = [g`1,f] by A1;
thus F(g,p) is Function of (len p)-tuples_on BOOLEAN, BOOLEAN by A3,
MCART_1:7;
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 OperSymbols 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
A5: g in the OperSymbols of S;
then reconsider p = (the Arity of S).g as Element of (the carrier of S)*
by FUNCT_2:7;
consider f being Function of (len p)-tuples_on BOOLEAN, BOOLEAN such that
A6: g = [g`1,f] by A1,A5;
f = g`2 by A6,MCART_1:7;
hence thesis by A4,A5,A6;
end;
end;
theorem Th52:
for S being non empty ManySortedSign holds S is unsplit iff
for o being set st o in the OperSymbols of S holds
(the ResultSort of S).o = o
proof let S be non empty ManySortedSign;
hereby assume S is unsplit;
then the ResultSort of S = id the OperSymbols of S by Def7;
hence for o being set st o in the OperSymbols of S holds
(the ResultSort of S).o = o by FUNCT_1:34;
end;
A1: dom the ResultSort of S = the OperSymbols of S by FUNCT_2:def 1;
assume for o being set st o in the OperSymbols of S holds
(the ResultSort of S).o = o;
hence the ResultSort of S = id the OperSymbols of S by A1,FUNCT_1:34;
end;
theorem
for S being non empty ManySortedSign st S is unsplit holds
the OperSymbols of S c= the carrier of S
proof let S be non empty ManySortedSign; assume
A1: S is unsplit;
let x be set; assume
A2: x in the OperSymbols of S;
then (the ResultSort of S).x = x by A1,Th52;
hence thesis by A2,FUNCT_2:7;
end;
definition
cluster unsplit -> Circuit-like (non empty ManySortedSign);
coherence
proof let S be non empty ManySortedSign such that
A1: the ResultSort of S = id the OperSymbols of S;
let S' be non void non empty ManySortedSign such that
A2: S' = S;
let o1,o2 be Gate of S';
the_result_sort_of o1 = (the ResultSort of S).o1 &
o1 in the OperSymbols of S & o2 in the OperSymbols of S &
the_result_sort_of o2 = (the ResultSort of S).o2
by A2,Lm2,MSUALG_1:def 7;
then the_result_sort_of o1 = o1 & the_result_sort_of o2 = o2
by A1,FUNCT_1:34;
hence thesis;
end;
end;
theorem Th54:
for f being set, p being FinSequence holds
1GateCircStr(p,f) is unsplit gate`1=arity
proof let f be set, p be FinSequence; set S = 1GateCircStr(p,f);
A1: the OperSymbols of S = {[p,f]} & (the ResultSort of S).[p,f] = [p,f]
by Def6;
then A2: dom the ResultSort of S = {[p,f]} by FUNCT_2:def 1;
now let x be set; assume x in {[p,f]};
then x = [p,f] by TARSKI:def 1;
hence (the ResultSort of S).x = x by Def6;
end;
hence the ResultSort of S = id the OperSymbols of S by A1,A2,FUNCT_1:34;
let g be set; assume g in the OperSymbols of S;
then A3: g = [p,f] by A1,TARSKI:def 1;
then (the Arity of S).g = p by Def6;
hence thesis by A3,MCART_1:7;
end;
definition
let f be set, p be FinSequence;
cluster 1GateCircStr(p,f) -> unsplit gate`1=arity;
coherence by Th54;
end;
definition
cluster unsplit gate`1=arity non void strict non empty ManySortedSign;
existence
proof consider f being set, p being FinSequence;
take 1GateCircStr(p,f);
thus thesis;
end;
end;
theorem Th55:
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 set; assume x in dom A1 /\ dom A2;
then x in dom A1 & x in dom A2 by XBOOLE_0:def 3;
then x in the OperSymbols of S1 & x in the OperSymbols of S2
by FUNCT_2:def 1;
then x = [A1.x, x`2] & x = [A2.x, x`2] by Def8;
hence thesis by ZFMISC_1:33;
end;
let x be set; assume x in dom R1 /\ dom R2;
then x in dom R1 & x in dom R2 by XBOOLE_0:def 3;
then x in the OperSymbols of S1 & x in the OperSymbols of S2
by FUNCT_2:def 1;
then R1.x = x & R2.x = x by Th52;
hence thesis;
end;
theorem Th56:
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 & A2 is gate`2=den;
set C1 = the Charact of A1, C2 = the Charact of A2;
let x be set; assume x in dom C1 /\ dom C2;
then x in dom C1 & x in dom C2 by XBOOLE_0:def 3;
then x in the OperSymbols of S1 & x in
the OperSymbols of S2 by PBOOLE:def 3;
then x = [x`1, C1.x] & x = [x`1, C2.x] by A1,Def10;
hence thesis by ZFMISC_1:33;
end;
theorem Th57:
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 OperSymbols of S = (the OperSymbols of S1) \/ the OperSymbols of S2 &
the ResultSort of S = (the ResultSort of S1)+*the ResultSort of S2
by Def2;
the ResultSort of S1 = id the OperSymbols of S1 &
the ResultSort of S2 = id the OperSymbols of S2 by Def7;
hence the ResultSort of S = id the OperSymbols of S by A1,FUNCT_4:23;
end;
definition
let S1,S2 be unsplit non empty ManySortedSign;
cluster S1+*S2 -> unsplit;
coherence by Th57;
end;
theorem Th58:
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;
A1: the OperSymbols of S = (the OperSymbols of S1) \/ the OperSymbols of S2 &
the Arity of S = (the Arity of S1)+*the Arity of S2 by Def2;
let g be set; assume
A2: g in the OperSymbols of S;
then reconsider g as Gate of S;
A3: g in the OperSymbols of S1 or g in the OperSymbols of S2 by A1,A2,XBOOLE_0
:def 2;
A4: dom the Arity of S = the OperSymbols of S &
dom the Arity of S1 = the OperSymbols of S1 &
dom the Arity of S2 = the OperSymbols of S2 by FUNCT_2:def 1;
A5: now assume
A6: not g in the OperSymbols of S2;
then reconsider g1 = g as Gate of S1 by A1,A2,XBOOLE_0:def 2;
thus g = [(the Arity of S1).g1, g`2] by A3,A6,Def8
.= [(the Arity of S).g, g`2] by A1,A2,A4,A6,FUNCT_4:def 1;
end;
now assume
A7: g in the OperSymbols of S2;
then reconsider g2 = g as Gate of S2;
thus g = [(the Arity of S2).g2, g`2] by A7,Def8
.= [(the Arity of S).g, g`2] by A1,A2,A4,A7,FUNCT_4:def 1;
end;
hence thesis by A5;
end;
definition
let S1,S2 be gate`1=arity non empty ManySortedSign;
cluster S1+*S2 -> gate`1=arity;
coherence by Th58;
end;
theorem Th59:
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
A1: S1 is gate`2isBoolean & S2 is gate`2isBoolean;
A2: the OperSymbols of S = (the OperSymbols of S1) \/ the OperSymbols of S2 &
the Arity of S = (the Arity of S1)+*the Arity of S2 by Def2;
let g be set; assume
A3: g in the OperSymbols of S;
let p be FinSequence such that
A4: p = (the Arity of S).g;
reconsider g as Gate of S by A3;
A5: g in the OperSymbols of S1 or g in the OperSymbols of S2 by A2,A3,XBOOLE_0
:def 2;
A6: dom the Arity of S = the OperSymbols of S &
dom the Arity of S1 = the OperSymbols of S1 &
dom the Arity of S2 = the OperSymbols of S2 by FUNCT_2:def 1;
A7: now assume
A8: not g in the OperSymbols of S2;
then reconsider g1 = g as Gate of S1 by A2,A3,XBOOLE_0:def 2;
(the Arity of S1).g1 = p by A2,A3,A4,A6,A8,FUNCT_4:def 1;
hence thesis by A1,A5,A8,Def9;
end;
now assume
A9: g in the OperSymbols of S2;
then reconsider g2 = g as Gate of S2;
(the Arity of S2).g2 = p by A2,A3,A4,A6,A9,FUNCT_4:def 1;
hence thesis by A1,A9,Def9;
end;
hence thesis by A7;
end;
begin :: One Gate Circuit
definition let n be Nat;
mode FinSeqLen of n -> FinSequence means:
Def12:
len it = n;
existence
proof consider X being non empty set;
consider p being Element of n-tuples_on X;
take p; thus thesis by FINSEQ_2:109;
end;
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 set S = 1GateCircStr(p,f,x);
set g1 = (rng p) --> X, g2 = {x} --> Y;
set SORTS = g1 +* g2;
set CHARACT = (the OperSymbols of S) --> f;
A2: the carrier of S = (rng p) \/ {x} &
the OperSymbols of S = {[p,f]} &
(the Arity of S).[p,f] = p &
(the ResultSort of S).[p,f] = x by Def5;
A3: x in {x} & dom ({x} --> Y) = {x} & dom ((rng p) --> X) = rng p
by FUNCOP_1:19,TARSKI:def 1;
then A4: SORTS.x = ({x} --> Y).x by FUNCT_4:14 .= Y by A3,FUNCOP_1:13;
reconsider SORTS as non-empty ManySortedSet of the carrier of S by Def5;
A5: dom the Arity of S = {[p,f]} & dom the ResultSort of S = {[p,f]}
by A2,FUNCT_2:def 1;
A6: len p = n by Def12;
rng p c= the carrier of S by A2,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
;
p is FinSequence of rng p by FINSEQ_1:def 4;
then reconsider p' = p as Element of (rng p)* by FINSEQ_1:def 11;
g1 tolerates g2
proof let y be set; assume A7: y in dom g1 /\ dom g2;
then y in {x} & y in rng p by A3,XBOOLE_0:def 3;
then x = y & g1.y = X & g2.y = Y by FUNCOP_1:13,TARSKI:def 1;
hence g1.y = g2.y by A1,A3,A7,XBOOLE_0:def 3;
end;
then g1 c= SORTS by FUNCT_4:29;
then g1# c= SORTS# & dom (g1# ) = (rng p)* by Th3,PBOOLE:def 3;
then A8: g1#.p' = SORTS#.pp by GRFUNC_1:8;
now let i be set; assume
A9: i in the OperSymbols of S;
then i = [p,f] by A2,TARSKI:def 1;
then CHARACT.i = f & (SORTS#*the Arity of S).i = SORTS#.p &
SORTS#.pp = n-tuples_on X & (SORTS*the ResultSort of S).i = Y
by A2,A4,A5,A6,A8,A9,Th6,FUNCOP_1:13,FUNCT_1:23;
hence CHARACT.i is Function of
(SORTS#*the Arity of S).i, (SORTS*the ResultSort of S).i;
end;
then reconsider CHARACT as ManySortedFunction of
SORTS#*the Arity of S, SORTS*the ResultSort of S by MSUALG_1:def 2;
reconsider A = MSAlgebra(#SORTS, CHARACT#) as
non-empty strict MSAlgebra over 1GateCircStr(p,f,x) by MSUALG_1:def 8;
take A;
[p,f] in {[p,f]} by TARSKI:def 1;
hence thesis by A2,FUNCOP_1:13;
end;
uniqueness
proof set S = 1GateCircStr(p,f,x);
let A1,A2 be strict non-empty MSAlgebra over S such that
A10: not thesis;
the OperSymbols of S = {[p,f]} by Def5;
then dom the Charact of A1 = {[p,f]} & dom the Charact of A2 = {[p,f]}
by PBOOLE:def 3;
then the Charact of A1 = {[[p,f],f]} & the Charact of A2 = {[[p,f],f]}
by A10,GRFUNC_1:18;
hence thesis by A10;
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:
Def14:
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 OperSymbols of S) --> f;
A1: the carrier of S = (rng p) \/ {[p,f]} &
the OperSymbols of S = {[p,f]} &
(the Arity of S).[p,f] = p &
(the ResultSort of S).[p,f] = [p,f] by Def6;
A2: [p,f] in {[p,f]} by TARSKI:def 1;
then [p,f] in the carrier of S by A1,XBOOLE_0:def 2;
then A3: SORTS.[p,f] = X by FUNCOP_1:13;
A4: dom the Arity of S = {[p,f]} & dom the ResultSort of S = {[p,f]}
by A1,FUNCT_2:def 1;
A5: len p = n by Def12;
rng p c= the carrier of S by A1,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
;
now let i be set; assume
A6: i in the OperSymbols of S;
then i = [p,f] by A1,TARSKI:def 1;
then CHARACT.i = f & (SORTS#*the Arity of S).i = SORTS#.p &
SORTS#.pp = n-tuples_on X & (SORTS*the ResultSort of S).i = X
by A1,A3,A4,A5,A6,Th6,FUNCOP_1:13,FUNCT_1:23;
hence CHARACT.i is Function of
(SORTS#*the Arity of S).i, (SORTS*the ResultSort of S).i;
end;
then reconsider CHARACT as ManySortedFunction of
SORTS#*the Arity of S, SORTS*the ResultSort of S by MSUALG_1:def 2;
reconsider A = MSAlgebra(#SORTS, CHARACT#) as
non-empty strict MSAlgebra over 1GateCircStr(p,f) by MSUALG_1:def 8;
take A;
thus thesis by A1,A2,FUNCOP_1:13;
end;
uniqueness
proof set S = 1GateCircStr(p,f);
let A1,A2 be strict non-empty MSAlgebra over S such that
A7: not thesis;
the OperSymbols of S = {[p,f]} by Def6;
then dom the Charact of A1 = {[p,f]} & dom the Charact of A2 = {[p,f]}
by PBOOLE:def 3;
then the Charact of A1 = {[[p,f],f]} & the Charact of A2 = {[[p,f],f]}
by A7,GRFUNC_1:18;
hence thesis by A7;
end;
end;
theorem Th60:
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 OperSymbols of 1GateCircStr(p,f);
then A2: g = [p,f] by Th48;
hence g = [g`1, f] by MCART_1:7
.= [g`1, (the Charact of 1GateCircuit(p,f)).g] by A2,Def14;
end;
take 1GateCircuit(p,f); thus thesis by A1;
end;
definition
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 Th60;
cluster 1GateCircStr(p,f) -> gate`2=den;
coherence by Th60;
end;
theorem Th61:
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 let n be Nat; set X = BOOLEAN;
let p be FinSeqLen of n; let f be Function of n-tuples_on X, X;
let g be set; assume
g in the OperSymbols of 1GateCircStr(p,f);
then A1: g = [p,f] & (the Arity of 1GateCircStr(p,f)).[p,f] = p & len p = n
by Def6,Def12,Th48;
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 A1;
take f; thus thesis by A1,MCART_1:7;
end;
definition
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 Th61;
end;
definition
cluster gate`2isBoolean non empty ManySortedSign;
existence
proof consider n being Nat;
consider f being Function of n-tuples_on BOOLEAN, BOOLEAN;
consider p being FinSeqLen of n;
take 1GateCircStr(p,f); thus thesis;
end;
end;
definition
let S1,S2 be gate`2isBoolean non empty ManySortedSign;
cluster S1+*S2 -> gate`2isBoolean;
coherence by Th59;
end;
theorem Th62:
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 OperSymbols of S = {[p,f]} by Def6;
then A1: dom the Charact of A = {[p,f]} by PBOOLE:def 3;
(the Charact of A).[p,f] = f by Def14;
then for x being set st x in {[p,f]} holds (the Charact of A).x = f
by TARSKI:def 1;
hence the Charact of A = {[p,f]} --> f by A1,FUNCOP_1:17;
let v be Vertex of S;
the Sorts of A = (the carrier of S) --> X by Def14;
hence thesis by FUNCOP_1:13;
end;
definition 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) -> locally-finite;
coherence
proof set S = 1GateCircStr(p,f);
let i be set; assume i in the carrier of S; hence thesis by Th62;
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;
thus 1GateCircStr(p,f) tolerates 1GateCircStr(q,f) by Th51;
set S1 = 1GateCircStr(p,f), S2 = 1GateCircStr(q,f);
set A1 = 1GateCircuit(p,f), A2 = 1GateCircuit(q,f);
the Sorts of A1 = (the carrier of S1) --> X &
the Sorts of A2 = (the carrier of S2) --> X by Def14;
hence the Sorts of A1 tolerates the Sorts of A2 by Th4;
the Charact of A1 = {[p,f]} --> f & the Charact of A2 = {[q,f]} --> f
by Th62;
hence thesis by Th4;
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 Th49;
then reconsider v = [p,f] as Element of IV by TARSKI:def 1;
the OperSymbols of S = {[p,f]} by Def6;
then reconsider o = [p,f] as Gate of S by TARSKI:def 1;
A1: (Following s).v = (Den (action_at v, A)).(action_at v depends_on_in s)
by CIRCUIT2:def 5;
the_result_sort_of o = (the ResultSort of S).o by MSUALG_1:def 7
.= v by Def6;
then A2: action_at v = o by MSAFREE2:def 7;
A3: Den(o,A) = (the Charact of A).o by MSUALG_1:def 11;
the_arity_of o = (the Arity of S).o by MSUALG_1:def 6 .= p by Def6;
then o depends_on_in s = s*p by CIRCUIT1:def 3;
hence (Following s).[p,f] = f.(s*p) by A1,A2,A3,Def14;
end;
begin :: Boolean Circuits
definition
redefine func BOOLEAN -> finite non empty 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:
Def15:
for v being Vertex of S holds (the Sorts of IT).v = BOOLEAN;
end;
theorem Th65:
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 PBOOLE:def 3;
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 set st v in the carrier of S holds
(the Sorts of A).v = BOOLEAN;
hence thesis by A1,FUNCOP_1:17;
end;
assume
A2: the Sorts of A = (the carrier of S) --> BOOLEAN;
let v be Vertex of S; thus thesis by A2,FUNCOP_1:13;
end;
definition
let S be non empty ManySortedSign;
cluster Boolean -> non-empty locally-finite 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 Th65;
hence A is non-empty by MSUALG_1:def 8;
let v be set; assume v in the carrier of S; hence thesis by A1,Def15;
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;
A1: dom the Sorts of A = the carrier of S by PBOOLE:def 3;
hereby assume A is Boolean;
then the Sorts of A = (the carrier of S) --> BOOLEAN by Th65;
hence rng the Sorts of A c= {BOOLEAN} by FUNCOP_1:19;
end;
assume
A2: rng the Sorts of A c= {BOOLEAN};
let v be Vertex of S;
(the Sorts of A).v in rng the Sorts of A by A1,FUNCT_1:def 5;
hence thesis by A2,TARSKI:def 1;
end;
theorem Th67:
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 A1 is Boolean & A2 is Boolean;
then the Sorts of A1 = (the carrier of S1) --> BOOLEAN &
the Sorts of A2 = (the carrier of S2) --> BOOLEAN by Th65;
hence thesis by Th4;
end;
theorem Th68:
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
proof let S1,S2 be unsplit gate`1=arity non empty ManySortedSign;
let A1 be MSAlgebra over S1, A2 be MSAlgebra over S2;
assume A1 is Boolean gate`2=den & A2 is Boolean gate`2=den;
hence S1 tolerates S2 & the Sorts of A1 tolerates the Sorts of A2 &
the Charact of A1 tolerates the Charact of A2 by Th55,Th56,Th67;
end;
definition let S be non empty ManySortedSign;
cluster Boolean (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 OperSymbols 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 OperSymbols 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:13;
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);
A1: the Sorts of A = (the carrier of S) --> BOOLEAN by Def14;
let v be Vertex of S; thus thesis by A1,FUNCOP_1:13;
end;
theorem Th70:
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: the Sorts of A1 = (the carrier of S1) --> BOOLEAN &
the Sorts of A2 = (the carrier of S2) --> BOOLEAN by Th65;
then A2: the Sorts of A1 tolerates the Sorts of A2 by Th4;
then A3: the Sorts of A = (the Sorts of A1)+*the Sorts of A2 by Def4;
A4: dom the Sorts of A1 = the carrier of S1 &
dom the Sorts of A2 = the carrier of S2 by PBOOLE:def 3;
let x be Vertex of S;
the carrier of S = (the carrier of S1) \/ the carrier of S2
by Def2;
then x in the carrier of S1 or x in the carrier of S2 by XBOOLE_0:def 2;
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 A1,A2,A3,A4,FUNCOP_1:13,FUNCT_4:14,16;
hence (the Sorts of A).x = BOOLEAN;
end;
theorem Th71:
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 & A2 is gate`2=den and
A2: the Sorts of A1 tolerates the Sorts of A2;
A3: the Charact of A = (the Charact of A1)+*the Charact of A2 by A2,Def4;
A4: dom the Charact of A1 = the OperSymbols of S1 &
dom the Charact of A2 = the OperSymbols of S2 by PBOOLE:def 3;
A5: the Charact of A1 tolerates the Charact of A2 by A1,Th56;
let g be set; assume
A6: g in the OperSymbols of S;
the OperSymbols of S = (the OperSymbols of S1) \/ the OperSymbols of S2
by Def2;
then g in the OperSymbols of S1 or g in the OperSymbols of S2 by A6,
XBOOLE_0:def 2
;
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,A3,A4,A5,Def10,FUNCT_4:14,16;
hence g = [g`1, (the Charact of A).g];
end;
definition
cluster unsplit gate`1=arity gate`2=den gate`2isBoolean non void
strict (non empty ManySortedSign);
existence
proof consider f being Function of 1-tuples_on BOOLEAN, BOOLEAN;
consider p being FinSeqLen of 1;
take 1GateCircStr(p,f);
thus thesis;
end;
end;
definition
let S be gate`2isBoolean non empty ManySortedSign;
cluster Boolean gate`2=den (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
g in the OperSymbols of S & p = (the Arity of S).g;
then consider f being Function of (len p)-tuples_on BOOLEAN, BOOLEAN such
that
A2: g = [g`1, f] by Def9;
thus F(g,p) is Function of (len p)-tuples_on BOOLEAN, BOOLEAN by A2,
MCART_1:7;
end;
consider A being strict MSAlgebra over S such that
A3: 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 OperSymbols 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
proof let v be Vertex of S;
thus thesis by A3,FUNCOP_1:13;
end;
let g be set; assume
A4: g in the OperSymbols of S;
then reconsider p = (the Arity of S).g as Element of (the carrier of S)*
by FUNCT_2:7;
consider f being Function of (len p)-tuples_on BOOLEAN, BOOLEAN such that
A5: g = [g`1, f] by A4,Def9;
g`2 = f by A5,MCART_1:7;
hence thesis by A3,A4,A5;
end;
end;
definition
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 Th67;
hence thesis by Th70,Th71;
end;
end;
definition 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 Circuit of 1GateCircStr(p,f);
existence proof take 1GateCircuit(p,f); thus thesis; end;
end;
definition 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 Th68;
hence thesis by Th38;
end;