:: Minimal Manysorted Signature for Partial Algebra :: by Grzegorz Bancerek :: :: Received October 1, 1995 :: Copyright (c) 1995-2021 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 FINSEQ_1, FUNCT_1, RELAT_1, XBOOLE_0, TARSKI, SETFAM_1, UNIALG_1, FUNCT_2, PARTFUN1, SUBSET_1, NAT_1, STRUCT_0, CARD_3, MSUALG_1, UNIALG_2, EQREL_1, ZFMISC_1, NUMBERS, FINSEQ_2, PBOOLE, CARD_1, ARYTM_3, INCPROJ, ORDINAL4, RELAT_2, NEWTON, MCART_1, MARGREL1, PUA2MSS1; notations TARSKI, XBOOLE_0, ZFMISC_1, XTUPLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, NAT_1, SETFAM_1, RELAT_1, STRUCT_0, FUNCT_1, PBOOLE, RELSET_1, PARTFUN1, MCART_1, FINSEQ_1, FINSEQ_2, FUNCT_2, RELAT_2, EQREL_1, CARD_3, MARGREL1, MSUALG_1, UNIALG_1; constructors NAT_1, EQREL_1, MSUALG_1, RELSET_1, DOMAIN_1, MARGREL1, XTUPLE_0, NUMBERS; registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2, NAT_1, FINSEQ_1, EQREL_1, FINSEQ_2, CARD_3, STRUCT_0, UNIALG_1, MSUALG_1, ORDINAL1, CARD_1, RELSET_1, PBOOLE, MARGREL1, XTUPLE_0, XCMPLX_0; requirements NUMERALS, BOOLE, SUBSET, ARITHM; begin registration let X be with_non-empty_elements set; cluster -> non-empty for FinSequence of X; end; registration let A be non empty set; cluster homogeneous quasi_total non-empty non empty for PFuncFinSequence of A; end; registration cluster non-empty -> non empty for UAStr; end; theorem :: PUA2MSS1:1 for f,g being non-empty Function st product f c= product g holds dom f = dom g & for x being set st x in dom f holds f.x c= g.x; theorem :: PUA2MSS1:2 for f,g being non-empty Function st product f = product g holds f = g; definition let A be non empty set; let f be PFuncFinSequence of A; redefine func rng f -> Subset of PFuncs(A*, A); end; definition let A,B be non empty set; let S be non empty Subset of PFuncs(A, B); redefine mode Element of S -> PartFunc of A,B; end; definition let A be non-empty UAStr; mode OperSymbol of A is Element of dom the charact of A; mode operation of A is Element of rng the charact of A; end; definition let A be non-empty UAStr; let o be OperSymbol of A; func Den(o, A) -> operation of A equals :: PUA2MSS1:def 1 (the charact of A).o; end; begin :: Partitions ::$CT theorem :: PUA2MSS1:4 for X,Y being set st X is_finer_than Y for p being FinSequence of X ex q being FinSequence of Y st product p c= product q; theorem :: PUA2MSS1:5 for X being set, P,Q being a_partition of X for f being Function of P,Q st for a being set st a in P holds a c= f.a for p being FinSequence of P, q being FinSequence of Q holds product p c= product q iff f*p = q; theorem :: PUA2MSS1:6 for P being set, f being Function st rng f c= union P ex p being Function st dom p = dom f & rng p c= P & f in product p; theorem :: PUA2MSS1:7 for X be set, P being a_partition of X, f being FinSequence of X ex p being FinSequence of P st f in product p; theorem :: PUA2MSS1:8 for X,Y being non empty set for P being a_partition of X, Q being a_partition of Y holds the set of all [:p,q:] where p is Element of P, q is Element of Q is a_partition of [:X,Y:]; theorem :: PUA2MSS1:9 for X being non empty set for P being a_partition of X holds the set of all product p where p is Element of P* is a_partition of X*; theorem :: PUA2MSS1:10 for X being non empty set, n be Element of NAT for P being a_partition of X holds the set of all product p where p is Element of n-tuples_on P is a_partition of n-tuples_on X; theorem :: PUA2MSS1:11 for X being non empty set, Y be set st Y c= X for P being a_partition of X holds {a /\ Y where a is Element of P: a meets Y} is a_partition of Y; theorem :: PUA2MSS1:12 for f being non empty Function, P being a_partition of dom f holds the set of all f|a where a is Element of P is a_partition of f; theorem :: PUA2MSS1:13 for X being set, p being FinSequence of SmallestPartition X ex q being FinSequence of X st product p = {q}; definition let X be set; mode IndexedPartition of X -> Function means :: PUA2MSS1:def 2 rng it is a_partition of X & it is one-to-one; end; definition let X be set; let P be IndexedPartition of X; redefine func rng P -> a_partition of X; end; registration let X be set; cluster -> one-to-one non-empty for IndexedPartition of X; end; registration let X be non empty set; cluster -> non empty for IndexedPartition of X; end; definition let X be set, P be a_partition of X; redefine func id P -> IndexedPartition of X; end; definition let X be set; let P be IndexedPartition of X; let x be object; assume x in X; func P-index_of x -> set means :: PUA2MSS1:def 3 it in dom P & x in P.it; end; theorem :: PUA2MSS1:14 for X being set, P being non-empty Function st Union P = X & for x,y being set st x in dom P & y in dom P & x <> y holds P.x misses P.y holds P is IndexedPartition of X; theorem :: PUA2MSS1:15 for X,Y being non empty set, P being a_partition of Y for f being Function of X, P st P c= rng f & f is one-to-one holds f is IndexedPartition of Y; begin :: Relations generated by operations of partial algebra scheme :: PUA2MSS1:sch 1 IndRelationEx {A, B() -> non empty set, i() -> Nat, R0() -> (Relation of A(),B()), RR(set,set) -> Relation of A(),B()}: ex R being Relation of A(),B(), F being ManySortedSet of NAT st R = F.i() & F.0 = R0() & for i being Nat, R being Relation of A(),B() st R = F.i holds F.(i+1) = RR(R,i); scheme :: PUA2MSS1:sch 2 RelationUniq {A, B() -> non empty set, P[set,set]}: for R1, R2 being Relation of A(), B() st (for x being Element of A(), y being Element of B() holds [x,y] in R1 iff P[x,y]) & (for x being Element of A(), y being Element of B() holds [x,y] in R2 iff P[x,y]) holds R1 = R2; scheme :: PUA2MSS1:sch 3 IndRelationUniq {A, B() -> non empty set, i() -> Nat, R0() -> (Relation of A(),B()), RR(set,set) -> Relation of A(),B()}: for R1, R2 being Relation of A(),B() st (ex F being ManySortedSet of NAT st R1 = F.i() & F.0 = R0() & for i being Nat, R being Relation of A(),B() st R = F.i holds F.(i+1) = RR(R,i)) & (ex F being ManySortedSet of NAT st R2 = F.i() & F.0 = R0() & for i being Nat, R being Relation of A(),B() st R = F.i holds F.(i+1) = RR(R,i)) holds R1 = R2; definition let A be partial non-empty UAStr; func DomRel A -> Relation of the carrier of A means :: PUA2MSS1:def 4 for x,y being Element of A holds [x,y] in it iff for f being operation of A, p,q being FinSequence holds p^<*x*>^q in dom f iff p^<*y*>^q in dom f; end; registration let A be partial non-empty UAStr; cluster DomRel A -> total symmetric transitive; end; definition let A be non-empty partial UAStr; let R be Relation of the carrier of A; func R|^A -> Relation of the carrier of A means :: PUA2MSS1:def 5 for x,y being Element of A holds [x,y] in it iff [x,y] in R & for f being operation of A for p,q being FinSequence st p^<*x*>^q in dom f & p^<*y*>^q in dom f holds [f.(p^<*x*>^q), f.(p^<*y*>^q)] in R; end; definition let A be non-empty partial UAStr; let R be Relation of the carrier of A; let i be Nat; func R|^(A,i) -> Relation of the carrier of A means :: PUA2MSS1:def 6 ex F being ManySortedSet of NAT st it = F.i & F.0 = R & for i being Nat, R being Relation of the carrier of A st R = F.i holds F.(i+1) = R|^A; end; theorem :: PUA2MSS1:16 for A being non-empty partial UAStr, R being Relation of the carrier of A holds R|^(A,0) = R & R|^(A,1) = R|^A; theorem :: PUA2MSS1:17 for A being non-empty partial UAStr, i being Nat, R being Relation of the carrier of A holds R|^(A,i+1) = R|^(A,i)|^A; theorem :: PUA2MSS1:18 for A being non-empty partial UAStr, i,j being Element of NAT, R being Relation of the carrier of A holds R|^(A,i+j) = R|^(A,i)|^(A,j); theorem :: PUA2MSS1:19 for A being non-empty partial UAStr for R being Equivalence_Relation of the carrier of A st R c= DomRel A holds R|^A is total symmetric transitive; theorem :: PUA2MSS1:20 for A being non-empty partial UAStr for R being Relation of the carrier of A holds R|^A c= R; theorem :: PUA2MSS1:21 for A being non-empty partial UAStr for R being Equivalence_Relation of the carrier of A st R c= DomRel A for i being Element of NAT holds R|^(A,i) is total symmetric transitive; definition let A be non-empty partial UAStr; func LimDomRel A -> Relation of the carrier of A means :: PUA2MSS1:def 7 for x,y being Element of A holds [x,y] in it iff for i being Element of NAT holds [x,y] in (DomRel A)|^(A,i); end; theorem :: PUA2MSS1:22 for A being non-empty partial UAStr holds LimDomRel A c= DomRel A; registration let A be non-empty partial UAStr; cluster LimDomRel A -> total symmetric transitive; end; begin :: Partitability definition let X be non empty set; let f be PartFunc of X*, X; let P be a_partition of X; pred f is_partitable_wrt P means :: PUA2MSS1:def 8 for p being FinSequence of P ex a being Element of P st f.:product p c= a; end; definition let X be non empty set; let f be PartFunc of X*, X; let P be a_partition of X; pred f is_exactly_partitable_wrt P means :: PUA2MSS1:def 9 f is_partitable_wrt P & for p being FinSequence of P st product p meets dom f holds product p c= dom f; end; theorem :: PUA2MSS1:23 for A being non-empty partial UAStr for f being operation of A holds f is_exactly_partitable_wrt SmallestPartition the carrier of A; scheme :: PUA2MSS1:sch 4 FiniteTransitivity {x, y() -> FinSequence, P[set], R[set,set]}: P[y()] provided P[x()] and len x() = len y() and for p,q being FinSequence, z1,z2 being set st P[p^<*z1*>^q] & R[z1,z2] holds P[p^<*z2*>^q] and for i being Element of NAT st i in dom x() holds R[x().i, y().i]; theorem :: PUA2MSS1:24 for A being non-empty partial UAStr for f being operation of A holds f is_exactly_partitable_wrt Class LimDomRel A; definition let A be partial non-empty UAStr; mode a_partition of A -> a_partition of the carrier of A means :: PUA2MSS1:def 10 for f being operation of A holds f is_exactly_partitable_wrt it; end; definition let A be partial non-empty UAStr; mode IndexedPartition of A -> IndexedPartition of the carrier of A means :: PUA2MSS1:def 11 rng it is a_partition of A; end; definition let A be partial non-empty UAStr; let P be IndexedPartition of A; redefine func rng P -> a_partition of A; end; theorem :: PUA2MSS1:25 for A being non-empty partial UAStr holds Class LimDomRel A is a_partition of A; theorem :: PUA2MSS1:26 for X being non empty set, P being a_partition of X for p being FinSequence of P, q1,q2 being FinSequence, x,y being set st q1^<*x*>^q2 in product p & ex a being Element of P st x in a & y in a holds q1^<*y*>^q2 in product p; theorem :: PUA2MSS1:27 for A being partial non-empty UAStr, P being a_partition of A holds P is_finer_than Class LimDomRel A; begin :: Morphisms between manysorted signatures definition let S1,S2 be ManySortedSign; let f,g be Function; pred f,g form_morphism_between S1,S2 means :: PUA2MSS1:def 12 dom f = the carrier of S1 & dom g = the carrier' of S1 & rng f c= the carrier of S2 & rng g c= the carrier' of S2 & f*the ResultSort of S1 = (the ResultSort of S2)*g & for o being set, p being Function st o in the carrier' of S1 & p = (the Arity of S1).o holds f*p = (the Arity of S2).(g.o); end; theorem :: PUA2MSS1:28 for S being non void non empty ManySortedSign holds id the carrier of S, id the carrier' of S form_morphism_between S,S; theorem :: PUA2MSS1:29 for S1,S2,S3 being ManySortedSign for f1,f2, g1,g2 being Function st f1, g1 form_morphism_between S1,S2 & f2, g2 form_morphism_between S2,S3 holds f2*f1, g2*g1 form_morphism_between S1,S3; definition let S1,S2 be ManySortedSign; pred S1 is_rougher_than S2 means :: PUA2MSS1:def 13 ex f,g being Function st f,g form_morphism_between S2,S1 & rng f = the carrier of S1 & rng g = the carrier' of S1; end; definition let S1,S2 be non void non empty ManySortedSign; redefine pred S1 is_rougher_than S2; reflexivity; end; theorem :: PUA2MSS1:30 for S1,S2,S3 being ManySortedSign st S1 is_rougher_than S2 & S2 is_rougher_than S3 holds S1 is_rougher_than S3; begin :: Manysorted signature of partital algebra definition let A be partial non-empty UAStr; let P be a_partition of A; func MSSign(A,P) -> strict ManySortedSign means :: PUA2MSS1:def 14 the carrier of it = P & the carrier' of it = {[o,p] where o is OperSymbol of A, p is Element of P*: product p meets dom Den(o,A)} & for o being OperSymbol of A, p being Element of P* st product p meets dom Den(o,A) holds (the Arity of it).[o,p] = p & Den(o, A).:product p c= (the ResultSort of it).[o,p]; end; registration let A be partial non-empty UAStr; let P be a_partition of A; cluster MSSign(A,P) -> non empty non void; end; definition let A be partial non-empty UAStr; let P be a_partition of A; let o be OperSymbol of MSSign(A,P); redefine func o`1 -> OperSymbol of A; redefine func o`2 -> Element of P*; end; definition let A be partial non-empty UAStr; let S be non void non empty ManySortedSign; let G be MSAlgebra over S; let P be IndexedPartition of the carrier' of S; pred A can_be_characterized_by S,G,P means :: PUA2MSS1:def 15 the Sorts of G is IndexedPartition of A & dom P = dom the charact of A & for o being OperSymbol of A holds (the Charact of G)|(P.o) is IndexedPartition of Den(o, A); end; definition let A be partial non-empty UAStr; let S be non void non empty ManySortedSign; pred A can_be_characterized_by S means :: PUA2MSS1:def 16 ex G being MSAlgebra over S, P being IndexedPartition of the carrier' of S st A can_be_characterized_by S,G,P; end; theorem :: PUA2MSS1:31 for A being partial non-empty UAStr, P being a_partition of A holds A can_be_characterized_by MSSign(A, P); theorem :: PUA2MSS1:32 for A being partial non-empty UAStr for S being non void non empty ManySortedSign for G being MSAlgebra over S for Q being IndexedPartition of the carrier' of S st A can_be_characterized_by S,G,Q for o being OperSymbol of A, r being FinSequence of rng the Sorts of G st product r c= dom Den(o,A) ex s being OperSymbol of S st (the Sorts of G)*the_arity_of s = r & s in Q.o; theorem :: PUA2MSS1:33 for A being partial non-empty UAStr, P being a_partition of A st P = Class LimDomRel A for S being non void non empty ManySortedSign st A can_be_characterized_by S holds MSSign(A,P) is_rougher_than S;