:: Minimal Manysorted Signature for Partial Algebra :: by Grzegorz Bancerek :: :: Received October 1, 1995 :: Copyright (c) 1995-2012 Association of Mizar Users begin Lm1: for p being FinSequence for f being Function st dom f = dom p holds f is FinSequence proofend; Lm2: for X being set for Y being non empty set for p being FinSequence of X for f being Function of X,Y holds f * p is FinSequence of Y proofend; registration let X be with_non-empty_elements set ; cluster -> non-empty for FinSequence of X; coherence for b1 being FinSequence of X holds b1 is non-empty proofend; end; registration let A be non empty set ; cluster non empty Relation-like non-empty NAT -defined PFuncs ((A *),A) -valued Function-like V44() FinSequence-like FinSubsequence-like countable homogeneous quasi_total for FinSequence of PFuncs ((A *),A); existence ex b1 being PFuncFinSequence of A st ( b1 is homogeneous & b1 is quasi_total & b1 is non-empty & not b1 is empty ) proofend; end; registration cluster non-empty -> non empty for UAStr ; coherence for b1 being UAStr st b1 is non-empty holds not b1 is empty proofend; end; theorem Th1: :: 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 ) ) proofend; theorem Th2: :: PUA2MSS1:2 for f, g being non-empty Function st product f = product g holds f = g proofend; definition let A be non empty set ; let f be PFuncFinSequence of A; :: original:proj2 redefine func rng f -> Subset of (PFuncs ((A *),A)); coherence proj2 f is Subset of (PFuncs ((A *),A)) by FINSEQ_1:def_4; end; definition let A, B be non empty set ; let S be non empty Subset of (PFuncs (A,B)); :: original:Element redefine mode Element of S -> PartFunc of A,B; coherence for b1 being Element of S holds b1 is PartFunc of A,B proofend; 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; correctness coherence the charact of A . o is operation of A; by FUNCT_1:def_3; end; :: deftheorem defines Den PUA2MSS1:def_1_:_ for A being non-empty UAStr for o being OperSymbol of A holds Den (o,A) = the charact of A . o; begin theorem :: PUA2MSS1:3 canceled; Lm3: for X being set for P being a_partition of X for x, a, b being set st x in a & a in P & x in b & b in P holds a = b by EQREL_1:70; theorem Th4: :: PUA2MSS1:4 for X, Y being set st X is_finer_than Y holds for p being FinSequence of X ex q being FinSequence of Y st product p c= product q proofend; theorem Th5: :: PUA2MSS1:5 for X being set for 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 ) holds for p being FinSequence of P for q being FinSequence of Q holds ( product p c= product q iff f * p = q ) proofend; theorem Th6: :: PUA2MSS1:6 for P being set for f being Function st rng f c= union P holds ex p being Function st ( dom p = dom f & rng p c= P & f in product p ) proofend; theorem Th7: :: PUA2MSS1:7 for X being set for P being a_partition of X for f being FinSequence of X ex p being FinSequence of P st f in product p proofend; theorem :: PUA2MSS1:8 for X, Y being non empty set for P being a_partition of X for Q being a_partition of Y holds { [:p,q:] where p is Element of P, q is Element of Q : verum } is a_partition of [:X,Y:] proofend; theorem Th9: :: PUA2MSS1:9 for X being non empty set for P being a_partition of X holds { (product p) where p is Element of P * : verum } is a_partition of X * proofend; theorem :: PUA2MSS1:10 for X being non empty set for n being Element of NAT for P being a_partition of X holds { (product p) where p is Element of n -tuples_on P : verum } is a_partition of n -tuples_on X proofend; theorem Th11: :: PUA2MSS1:11 for X being non empty set for Y being set st Y c= X holds for P being a_partition of X holds { (a /\ Y) where a is Element of P : a meets Y } is a_partition of Y proofend; theorem Th12: :: PUA2MSS1:12 for f being non empty Function for P being a_partition of dom f holds { (f | a) where a is Element of P : verum } is a_partition of f proofend; theorem Th13: :: PUA2MSS1:13 for X being set for p being FinSequence of SmallestPartition X ex q being FinSequence of X st product p = {q} proofend; definition let X be set ; mode IndexedPartition of X -> Function means :Def2: :: PUA2MSS1:def 2 ( rng it is a_partition of X & it is one-to-one ); existence ex b1 being Function st ( rng b1 is a_partition of X & b1 is one-to-one ) proofend; end; :: deftheorem Def2 defines IndexedPartition PUA2MSS1:def_2_:_ for X being set for b2 being Function holds ( b2 is IndexedPartition of X iff ( rng b2 is a_partition of X & b2 is one-to-one ) ); definition let X be set ; let P be IndexedPartition of X; :: original:proj2 redefine func rng P -> a_partition of X; coherence proj2 P is a_partition of X by Def2; end; registration let X be set ; cluster -> non-empty one-to-one for IndexedPartition of X; coherence for b1 being IndexedPartition of X holds ( b1 is one-to-one & b1 is non-empty ) proofend; end; registration let X be non empty set ; cluster -> non empty for IndexedPartition of X; coherence for b1 being IndexedPartition of X holds not b1 is empty proofend; end; definition let X be set ; let P be a_partition of X; :: original:id redefine func id P -> IndexedPartition of X; coherence id P is IndexedPartition of X proofend; end; definition let X be set ; let P be IndexedPartition of X; let x be set ; assume A1: x in X ; A2: union (rng P) = X by EQREL_1:def_4; funcP -index_of x -> set means :Def3: :: PUA2MSS1:def 3 ( it in dom P & x in P . it ); existence ex b1 being set st ( b1 in dom P & x in P . b1 ) proofend; correctness uniqueness for b1, b2 being set st b1 in dom P & x in P . b1 & b2 in dom P & x in P . b2 holds b1 = b2; proofend; end; :: deftheorem Def3 defines -index_of PUA2MSS1:def_3_:_ for X being set for P being IndexedPartition of X for x being set st x in X holds for b4 being set holds ( b4 = P -index_of x iff ( b4 in dom P & x in P . b4 ) ); theorem Th14: :: PUA2MSS1:14 for X being set for 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 proofend; theorem Th15: :: PUA2MSS1:15 for X, Y being non empty set for 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 proofend; begin scheme :: PUA2MSS1:sch 1 IndRelationEx{ F1() -> non empty set , F2() -> non empty set , F3() -> Element of NAT , F4() -> Relation of F1(),F2(), F5( set , set ) -> Relation of F1(),F2() } : ex R being Relation of F1(),F2() ex F being ManySortedSet of NAT st ( R = F . F3() & F . 0 = F4() & ( for i being Element of NAT for R being Relation of F1(),F2() st R = F . i holds F . (i + 1) = F5(R,i) ) ) proofend; scheme :: PUA2MSS1:sch 2 RelationUniq{ F1() -> non empty set , F2() -> non empty set , P1[ set , set ] } : for R1, R2 being Relation of F1(),F2() st ( for x being Element of F1() for y being Element of F2() holds ( [x,y] in R1 iff P1[x,y] ) ) & ( for x being Element of F1() for y being Element of F2() holds ( [x,y] in R2 iff P1[x,y] ) ) holds R1 = R2 proofend; scheme :: PUA2MSS1:sch 3 IndRelationUniq{ F1() -> non empty set , F2() -> non empty set , F3() -> Element of NAT , F4() -> Relation of F1(),F2(), F5( set , set ) -> Relation of F1(),F2() } : for R1, R2 being Relation of F1(),F2() st ex F being ManySortedSet of NAT st ( R1 = F . F3() & F . 0 = F4() & ( for i being Element of NAT for R being Relation of F1(),F2() st R = F . i holds F . (i + 1) = F5(R,i) ) ) & ex F being ManySortedSet of NAT st ( R2 = F . F3() & F . 0 = F4() & ( for i being Element of NAT for R being Relation of F1(),F2() st R = F . i holds F . (i + 1) = F5(R,i) ) ) holds R1 = R2 proofend; definition let A be partial non-empty UAStr ; func DomRel A -> Relation of the carrier of A means :Def4: :: PUA2MSS1:def 4 for x, y being Element of A holds ( [x,y] in it iff for f being operation of A for p, q being FinSequence holds ( (p ^ <*x*>) ^ q in dom f iff (p ^ <*y*>) ^ q in dom f ) ); existence ex b1 being Relation of the carrier of A st for x, y being Element of A holds ( [x,y] in b1 iff for f being operation of A for p, q being FinSequence holds ( (p ^ <*x*>) ^ q in dom f iff (p ^ <*y*>) ^ q in dom f ) ) proofend; uniqueness for b1, b2 being Relation of the carrier of A st ( for x, y being Element of A holds ( [x,y] in b1 iff for f being operation of A for p, q being FinSequence holds ( (p ^ <*x*>) ^ q in dom f iff (p ^ <*y*>) ^ q in dom f ) ) ) & ( for x, y being Element of A holds ( [x,y] in b2 iff for f being operation of A for p, q being FinSequence holds ( (p ^ <*x*>) ^ q in dom f iff (p ^ <*y*>) ^ q in dom f ) ) ) holds b1 = b2 proofend; end; :: deftheorem Def4 defines DomRel PUA2MSS1:def_4_:_ for A being partial non-empty UAStr for b2 being Relation of the carrier of A holds ( b2 = DomRel A iff for x, y being Element of A holds ( [x,y] in b2 iff for f being operation of A for p, q being FinSequence holds ( (p ^ <*x*>) ^ q in dom f iff (p ^ <*y*>) ^ q in dom f ) ) ); registration let A be partial non-empty UAStr ; cluster DomRel A -> total symmetric transitive ; coherence ( DomRel A is total & DomRel A is symmetric & DomRel A is transitive ) proofend; end; definition let A be partial non-empty UAStr ; let R be Relation of the carrier of A; funcR |^ A -> Relation of the carrier of A means :Def5: :: 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 ) ) ); existence ex b1 being Relation of the carrier of A st for x, y being Element of A holds ( [x,y] in b1 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 ) ) ) proofend; uniqueness for b1, b2 being Relation of the carrier of A st ( for x, y being Element of A holds ( [x,y] in b1 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 ) ) ) ) & ( for x, y being Element of A holds ( [x,y] in b2 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 ) ) ) ) holds b1 = b2 proofend; end; :: deftheorem Def5 defines |^ PUA2MSS1:def_5_:_ for A being partial non-empty UAStr for R, b3 being Relation of the carrier of A holds ( b3 = R |^ A iff for x, y being Element of A holds ( [x,y] in b3 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 ) ) ) ); definition let A be partial non-empty UAStr ; let R be Relation of the carrier of A; let i be Element of NAT ; funcR |^ (A,i) -> Relation of the carrier of A means :Def6: :: PUA2MSS1:def 6 ex F being ManySortedSet of NAT st ( it = F . i & F . 0 = R & ( for i being Element of NAT for R being Relation of the carrier of A st R = F . i holds F . (i + 1) = R |^ A ) ); existence ex b1 being Relation of the carrier of A ex F being ManySortedSet of NAT st ( b1 = F . i & F . 0 = R & ( for i being Element of NAT for R being Relation of the carrier of A st R = F . i holds F . (i + 1) = R |^ A ) ) proofend; uniqueness for b1, b2 being Relation of the carrier of A st ex F being ManySortedSet of NAT st ( b1 = F . i & F . 0 = R & ( for i being Element of NAT for R being Relation of the carrier of A st R = F . i holds F . (i + 1) = R |^ A ) ) & ex F being ManySortedSet of NAT st ( b2 = F . i & F . 0 = R & ( for i being Element of NAT for R being Relation of the carrier of A st R = F . i holds F . (i + 1) = R |^ A ) ) holds b1 = b2 proofend; end; :: deftheorem Def6 defines |^ PUA2MSS1:def_6_:_ for A being partial non-empty UAStr for R being Relation of the carrier of A for i being Element of NAT for b4 being Relation of the carrier of A holds ( b4 = R |^ (A,i) iff ex F being ManySortedSet of NAT st ( b4 = F . i & F . 0 = R & ( for i being Element of NAT for R being Relation of the carrier of A st R = F . i holds F . (i + 1) = R |^ A ) ) ); theorem Th16: :: PUA2MSS1:16 for A being partial non-empty UAStr for R being Relation of the carrier of A holds ( R |^ (A,0) = R & R |^ (A,1) = R |^ A ) proofend; theorem Th17: :: PUA2MSS1:17 for A being partial non-empty UAStr for i being Element of NAT for R being Relation of the carrier of A holds R |^ (A,(i + 1)) = (R |^ (A,i)) |^ A proofend; theorem :: PUA2MSS1:18 for A being partial non-empty UAStr for i, j being Element of NAT for R being Relation of the carrier of A holds R |^ (A,(i + j)) = (R |^ (A,i)) |^ (A,j) proofend; theorem Th19: :: PUA2MSS1:19 for A being partial non-empty UAStr for R being Equivalence_Relation of the carrier of A st R c= DomRel A holds ( R |^ A is total & R |^ A is symmetric & R |^ A is transitive ) proofend; theorem Th20: :: PUA2MSS1:20 for A being partial non-empty UAStr for R being Relation of the carrier of A holds R |^ A c= R proofend; theorem Th21: :: PUA2MSS1:21 for A being partial non-empty UAStr for R being Equivalence_Relation of the carrier of A st R c= DomRel A holds for i being Element of NAT holds ( R |^ (A,i) is total & R |^ (A,i) is symmetric & R |^ (A,i) is transitive ) proofend; definition let A be partial non-empty UAStr ; defpred S1[ set , set ] means for i being Element of NAT holds [$1,$2] in (DomRel A) |^ (A,i); func LimDomRel A -> Relation of the carrier of A means :Def7: :: 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) ); existence ex b1 being Relation of the carrier of A st for x, y being Element of A holds ( [x,y] in b1 iff for i being Element of NAT holds [x,y] in (DomRel A) |^ (A,i) ) proofend; uniqueness for b1, b2 being Relation of the carrier of A st ( for x, y being Element of A holds ( [x,y] in b1 iff for i being Element of NAT holds [x,y] in (DomRel A) |^ (A,i) ) ) & ( for x, y being Element of A holds ( [x,y] in b2 iff for i being Element of NAT holds [x,y] in (DomRel A) |^ (A,i) ) ) holds b1 = b2 proofend; end; :: deftheorem Def7 defines LimDomRel PUA2MSS1:def_7_:_ for A being partial non-empty UAStr for b2 being Relation of the carrier of A holds ( b2 = LimDomRel A iff for x, y being Element of A holds ( [x,y] in b2 iff for i being Element of NAT holds [x,y] in (DomRel A) |^ (A,i) ) ); theorem Th22: :: PUA2MSS1:22 for A being partial non-empty UAStr holds LimDomRel A c= DomRel A proofend; registration let A be partial non-empty UAStr ; cluster LimDomRel A -> total symmetric transitive ; coherence ( LimDomRel A is total & LimDomRel A is symmetric & LimDomRel A is transitive ) proofend; end; begin definition let X be non empty set ; let f be PartFunc of (X *),X; let P be a_partition of X; predf is_partitable_wrt P means :Def8: :: PUA2MSS1:def 8 for p being FinSequence of P ex a being Element of P st f .: (product p) c= a; end; :: deftheorem Def8 defines is_partitable_wrt PUA2MSS1:def_8_:_ for X being non empty set for f being PartFunc of (X *),X for P being a_partition of X holds ( f is_partitable_wrt P iff for p being FinSequence of P ex a being Element of P st f .: (product p) c= a ); definition let X be non empty set ; let f be PartFunc of (X *),X; let P be a_partition of X; predf is_exactly_partitable_wrt P means :Def9: :: 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; :: deftheorem Def9 defines is_exactly_partitable_wrt PUA2MSS1:def_9_:_ for X being non empty set for f being PartFunc of (X *),X for P being a_partition of X holds ( f is_exactly_partitable_wrt P iff ( f is_partitable_wrt P & ( for p being FinSequence of P st product p meets dom f holds product p c= dom f ) ) ); theorem :: PUA2MSS1:23 for A being partial non-empty UAStr for f being operation of A holds f is_exactly_partitable_wrt SmallestPartition the carrier of A proofend; scheme :: PUA2MSS1:sch 4 FiniteTransitivity{ F1() -> FinSequence, F2() -> FinSequence, P1[ set ], P2[ set , set ] } : P1[F2()] provided A1: P1[F1()] and A2: len F1() = len F2() and A3: for p, q being FinSequence for z1, z2 being set st P1[(p ^ <*z1*>) ^ q] & P2[z1,z2] holds P1[(p ^ <*z2*>) ^ q] and A4: for i being Element of NAT st i in dom F1() holds P2[F1() . i,F2() . i] proofend; theorem Th24: :: PUA2MSS1:24 for A being partial non-empty UAStr for f being operation of A holds f is_exactly_partitable_wrt Class (LimDomRel A) proofend; definition let A be partial non-empty UAStr ; mode a_partition of A -> a_partition of the carrier of A means :Def10: :: PUA2MSS1:def 10 for f being operation of A holds f is_exactly_partitable_wrt it; existence ex b1 being a_partition of the carrier of A st for f being operation of A holds f is_exactly_partitable_wrt b1 proofend; end; :: deftheorem Def10 defines a_partition PUA2MSS1:def_10_:_ for A being partial non-empty UAStr for b2 being a_partition of the carrier of A holds ( b2 is a_partition of A iff for f being operation of A holds f is_exactly_partitable_wrt b2 ); definition let A be partial non-empty UAStr ; mode IndexedPartition of A -> IndexedPartition of the carrier of A means :Def11: :: PUA2MSS1:def 11 rng it is a_partition of A; existence ex b1 being IndexedPartition of the carrier of A st rng b1 is a_partition of A proofend; end; :: deftheorem Def11 defines IndexedPartition PUA2MSS1:def_11_:_ for A being partial non-empty UAStr for b2 being IndexedPartition of the carrier of A holds ( b2 is IndexedPartition of A iff rng b2 is a_partition of A ); definition let A be partial non-empty UAStr ; let P be IndexedPartition of A; :: original:proj2 redefine func rng P -> a_partition of A; coherence proj2 P is a_partition of A by Def11; end; theorem :: PUA2MSS1:25 for A being partial non-empty UAStr holds Class (LimDomRel A) is a_partition of A proofend; theorem Th26: :: PUA2MSS1:26 for X being non empty set for P being a_partition of X for p being FinSequence of P for q1, q2 being FinSequence for 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 proofend; theorem Th27: :: PUA2MSS1:27 for A being partial non-empty UAStr for P being a_partition of A holds P is_finer_than Class (LimDomRel A) proofend; begin definition let S1, S2 be ManySortedSign ; let f, g be Function; predf,g form_morphism_between S1,S2 means :Def12: :: 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 for 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; :: deftheorem Def12 defines form_morphism_between PUA2MSS1:def_12_:_ for S1, S2 being ManySortedSign for f, g being Function holds ( f,g form_morphism_between S1,S2 iff ( 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 for 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) ) ) ); theorem Th28: :: PUA2MSS1:28 for S being non empty non void ManySortedSign holds id the carrier of S, id the carrier' of S form_morphism_between S,S proofend; theorem Th29: :: 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 proofend; definition let S1, S2 be ManySortedSign ; predS1 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; :: deftheorem defines is_rougher_than PUA2MSS1:def_13_:_ for S1, S2 being ManySortedSign holds ( S1 is_rougher_than S2 iff 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 ) ); definition let S1, S2 be non empty non void ManySortedSign ; :: original:is_rougher_than redefine predS1 is_rougher_than S2; reflexivity for S1 being non empty non void ManySortedSign holds (b1,b1) proofend; 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 proofend; begin definition let A be partial non-empty UAStr ; let P be a_partition of A; func MSSign (A,P) -> strict ManySortedSign means :Def14: :: 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 for 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] ) ) ); existence ex b1 being strict ManySortedSign st ( the carrier of b1 = P & the carrier' of b1 = { [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 for p being Element of P * st product p meets dom (Den (o,A)) holds ( the Arity of b1 . [o,p] = p & (Den (o,A)) .: (product p) c= the ResultSort of b1 . [o,p] ) ) ) proofend; correctness uniqueness for b1, b2 being strict ManySortedSign st the carrier of b1 = P & the carrier' of b1 = { [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 for p being Element of P * st product p meets dom (Den (o,A)) holds ( the Arity of b1 . [o,p] = p & (Den (o,A)) .: (product p) c= the ResultSort of b1 . [o,p] ) ) & the carrier of b2 = P & the carrier' of b2 = { [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 for p being Element of P * st product p meets dom (Den (o,A)) holds ( the Arity of b2 . [o,p] = p & (Den (o,A)) .: (product p) c= the ResultSort of b2 . [o,p] ) ) holds b1 = b2; proofend; end; :: deftheorem Def14 defines MSSign PUA2MSS1:def_14_:_ for A being partial non-empty UAStr for P being a_partition of A for b3 being strict ManySortedSign holds ( b3 = MSSign (A,P) iff ( the carrier of b3 = P & the carrier' of b3 = { [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 for p being Element of P * st product p meets dom (Den (o,A)) holds ( the Arity of b3 . [o,p] = p & (Den (o,A)) .: (product p) c= the ResultSort of b3 . [o,p] ) ) ) ); registration let A be partial non-empty UAStr ; let P be a_partition of A; cluster MSSign (A,P) -> non empty non void strict ; coherence ( not MSSign (A,P) is empty & not MSSign (A,P) is void ) proofend; end; definition let A be partial non-empty UAStr ; let P be a_partition of A; let o be OperSymbol of (MSSign (A,P)); :: original:`1 redefine funco `1 -> OperSymbol of A; coherence o `1 is OperSymbol of A proofend; :: original:`2 redefine funco `2 -> Element of P * ; coherence o `2 is Element of P * proofend; end; definition let A be partial non-empty UAStr ; let S be non empty non void ManySortedSign ; let G be MSAlgebra over S; let P be IndexedPartition of the carrier' of S; predA can_be_characterized_by S,G,P means :Def15: :: 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; :: deftheorem Def15 defines can_be_characterized_by PUA2MSS1:def_15_:_ for A being partial non-empty UAStr for S being non empty non void ManySortedSign for G being MSAlgebra over S for P being IndexedPartition of the carrier' of S holds ( A can_be_characterized_by S,G,P iff ( 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) ) ) ); definition let A be partial non-empty UAStr ; let S be non empty non void ManySortedSign ; predA can_be_characterized_by S means :: PUA2MSS1:def 16 ex G being MSAlgebra over S ex P being IndexedPartition of the carrier' of S st A can_be_characterized_by S,G,P; end; :: deftheorem defines can_be_characterized_by PUA2MSS1:def_16_:_ for A being partial non-empty UAStr for S being non empty non void ManySortedSign holds ( A can_be_characterized_by S iff ex G being MSAlgebra over S ex P being IndexedPartition of the carrier' of S st A can_be_characterized_by S,G,P ); theorem :: PUA2MSS1:31 for A being partial non-empty UAStr for P being a_partition of A holds A can_be_characterized_by MSSign (A,P) proofend; theorem Th32: :: PUA2MSS1:32 for A being partial non-empty UAStr for S being non empty non void 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 holds for o being OperSymbol of A for r being FinSequence of rng the Sorts of G st product r c= dom (Den (o,A)) holds ex s being OperSymbol of S st ( the Sorts of G * (the_arity_of s) = r & s in Q . o ) proofend; theorem :: PUA2MSS1:33 for A being partial non-empty UAStr for P being a_partition of A st P = Class (LimDomRel A) holds for S being non empty non void ManySortedSign st A can_be_characterized_by S holds MSSign (A,P) is_rougher_than S proofend;