Volume 7, 1995

University of Bialystok

Copyright (c) 1995 Association of Mizar Users

### The abstract of the Mizar article:

### Minimal Signature for Partial Algebra

**by****Grzegorz Bancerek**- Received October 1, 1995
- MML identifier: PUA2MSS1

- [ Mizar article, MML identifier index ]

environ vocabulary RELAT_1, FINSEQ_1, FUNCT_1, ZF_REFLE, AMI_1, BOOLE, PARTFUN1, UNIALG_1, FUNCT_2, CARD_3, MSUALG_1, UNIALG_2, EQREL_1, SETFAM_1, TARSKI, FINSEQ_2, PROB_1, PBOOLE, INCPROJ, RELAT_2, GROUP_1, MCART_1, PRALG_1, TDGROUP, QC_LANG1, PUA2MSS1; notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, NUMBERS, NAT_1, SETFAM_1, RELAT_1, STRUCT_0, RELSET_1, FUNCT_1, MCART_1, FINSEQ_1, FINSEQ_2, PARTFUN1, FUNCT_2, RELAT_2, EQREL_1, AMI_1, PROB_1, CARD_3, PBOOLE, MSUALG_1, UNIALG_1; constructors NAT_1, PRVECT_1, EQREL_1, AMI_1, MSUALG_1, PROB_1, MEMBERED, PARTFUN1, RELAT_1, RELAT_2; clusters SUBSET_1, STRUCT_0, RELSET_1, FUNCT_1, AMI_1, FINSEQ_1, FINSEQ_2, FINSEQ_5, UNIALG_1, PRVECT_1, MSUALG_1, MSAFREE, FSM_1, PARTFUN1, NAT_1, FRAENKEL, RELAT_1, EQREL_1, TOLER_1; requirements NUMERALS, BOOLE, SUBSET, ARITHM; begin definition let f be non-empty Function; cluster rng f -> with_non-empty_elements; end; definition let X,Y be non empty set; cluster non empty PartFunc of X,Y; end; definition let X be with_non-empty_elements set; cluster -> non-empty FinSequence of X; end; definition let A be non empty set; cluster homogeneous quasi_total non-empty non empty PFuncFinSequence of A; end; definition cluster non-empty -> non empty UAStr; end; definition let X be non empty with_non-empty_elements set; cluster -> non empty Element of X; 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 definition let X be set; cluster -> with_non-empty_elements a_partition of X; end; definition let X be set; let R be Equivalence_Relation of X; redefine func Class R -> a_partition of X; end; theorem :: PUA2MSS1:3 for X being set, P being a_partition of X, x,a,b being set st x in a & a in P & x in b & b in P holds a = b; 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 {[:p,q:] where p is Element of P, q is Element of Q: not contradiction} is a_partition of [:X,Y:]; theorem :: PUA2MSS1:9 for X being non empty set for P being a_partition of X holds {product p where p is Element of P*: not contradiction} is a_partition of X *; theorem :: PUA2MSS1:10 for X being non empty set, n be Nat for P being a_partition of X holds {product p where p is Element of n-tuples_on P: not contradiction} 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 {f|a where a is Element of P: not contradiction} is a_partition of f; definition let X be set; func SmallestPartition X -> a_partition of X equals :: PUA2MSS1:def 2 Class id X; end; theorem :: PUA2MSS1:13 for X being non empty set holds SmallestPartition X = {{x} where x is Element of X: not contradiction}; theorem :: PUA2MSS1:14 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 3 rng it is a_partition of X & it is one-to-one; end; definition let X be set; cluster -> one-to-one non-empty IndexedPartition of X; let P be IndexedPartition of X; redefine func rng P -> a_partition of X; end; definition let X be non empty set; cluster -> non empty 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 set; assume x in X; func P-index_of x -> set means :: PUA2MSS1:def 4 it in dom P & x in P.it; end; theorem :: PUA2MSS1:15 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:16 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 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 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 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 5 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; definition 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 6 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 7 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:17 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:18 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:19 for A being non-empty partial UAStr, i,j being Nat, R being Relation of the carrier of A holds R|^(A,i+j) = R|^(A,i)|^(A,j); theorem :: PUA2MSS1:20 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:21 for A being non-empty partial UAStr for R being Relation of the carrier of A holds R|^A c= R; theorem :: PUA2MSS1:22 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 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 8 for x,y being Element of A holds [x,y] in it iff for i being Nat holds [x,y] in (DomRel A)|^(A,i); end; theorem :: PUA2MSS1:23 for A being non-empty partial UAStr holds LimDomRel A c= DomRel A; definition 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 9 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 10 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:24 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 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 Nat st i in dom x() holds R[x().i, y().i]; theorem :: PUA2MSS1:25 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 11 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 12 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:26 for A being non-empty partial UAStr holds Class LimDomRel A is a_partition of A; theorem :: PUA2MSS1:27 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:28 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 13 dom f = the carrier of S1 & dom g = the OperSymbols of S1 & rng f c= the carrier of S2 & rng g c= the OperSymbols of S2 & f*the ResultSort of S1 = (the ResultSort of S2)*g & for o being set, p being Function st o in the OperSymbols of S1 & p = (the Arity of S1).o holds f*p = (the Arity of S2).(g.o); end; theorem :: PUA2MSS1:29 for S being non void non empty ManySortedSign holds id the carrier of S, id the OperSymbols of S form_morphism_between S,S; theorem :: PUA2MSS1:30 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 14 ex f,g being Function st f,g form_morphism_between S2,S1 & rng f = the carrier of S1 & rng g = the OperSymbols of S1; end; definition let S1,S2 be non void non empty ManySortedSign; redefine pred S1 is_rougher_than S2; reflexivity; end; theorem :: PUA2MSS1:31 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 15 the carrier of it = P & the OperSymbols 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; definition 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; 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 OperSymbols of S; pred A can_be_characterized_by S,G,P means :: PUA2MSS1:def 16 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 17 ex G being MSAlgebra over S, P being IndexedPartition of the OperSymbols of S st A can_be_characterized_by S,G,P; end; theorem :: PUA2MSS1:32 for A being partial non-empty UAStr, P being a_partition of A holds A can_be_characterized_by MSSign(A, P); theorem :: PUA2MSS1:33 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 OperSymbols 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:34 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;

Back to top