:: Minimal Manysorted Signature for Partial Algebra
:: by Grzegorz Bancerek
::
:: Copyright (c) 1995-2018 Association of Mizar Users

Lm1: for p being FinSequence
for f being Function st dom f = dom p holds
f is FinSequence

proof end;

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

proof end;

registration
let X be with_non-empty_elements set ;
cluster -> non-empty for of ;
coherence
for b1 being FinSequence of X holds b1 is non-empty
proof end;
end;

registration
let A be non empty set ;
existence
ex b1 being PFuncFinSequence of A st
( b1 is homogeneous & b1 is quasi_total & b1 is non-empty & not b1 is empty )
proof end;
end;

registration
cluster non-empty -> non empty for UAStr ;
coherence
for b1 being UAStr st b1 is non-empty holds
not b1 is empty
proof end;
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 ) )
proof end;

theorem Th2: :: PUA2MSS1:2
for f, g being non-empty Function st product f = product g holds
f = g
proof end;

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
proof end;
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;

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 Th3: :: 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
proof end;

theorem Th4: :: 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 )
proof end;

theorem Th5: :: 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 )
proof end;

theorem Th6: :: 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
proof end;

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:]
proof end;

theorem Th8: :: PUA2MSS1:9
for X being non empty set
for P being a_partition of X holds { () where p is Element of P * : verum } is a_partition of X *
proof end;

theorem :: PUA2MSS1:10
for X being non empty set
for n being Element of NAT
for P being a_partition of X holds { () where p is Element of n -tuples_on P : verum } is a_partition of n -tuples_on X
proof end;

theorem Th10: :: 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
proof end;

theorem Th11: :: 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
proof end;

theorem Th12: :: PUA2MSS1:13
for X being set
for p being FinSequence of SmallestPartition X ex q being FinSequence of X st product p = {q}
proof end;

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 )
proof end;
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 ;
coherence
for b1 being IndexedPartition of X holds
( b1 is one-to-one & b1 is non-empty )
proof end;
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
proof end;
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
proof end;
end;

definition
let X be set ;
let P be IndexedPartition of X;
let x be object ;
assume A1: x in X ;
A2: union (rng P) = X by EQREL_1:def 4;
func P -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 )
proof end;
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
;
proof end;
end;

:: deftheorem Def3 defines -index_of PUA2MSS1:def 3 :
for X being set
for P being IndexedPartition of X
for x being object 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 Th13: :: 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
proof end;

theorem Th14: :: 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
proof end;

scheme :: PUA2MSS1:sch 1
IndRelationEx{ F1() -> non empty set , F2() -> non empty set , F3() -> 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 Nat
for R being Relation of F1(),F2() st R = F . i holds
F . (i + 1) = F5(R,i) ) )
proof end;

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
proof end;

scheme :: PUA2MSS1:sch 3
IndRelationUniq{ F1() -> non empty set , F2() -> non empty set , F3() -> 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 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 Nat
for R being Relation of F1(),F2() st R = F . i holds
F . (i + 1) = F5(R,i) ) ) holds
R1 = R2
proof end;

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 ) )
proof end;
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
proof end;
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 ;
coherence
( DomRel A is total & DomRel A is symmetric & DomRel A is transitive )
proof end;
end;

definition
let A be partial non-empty UAStr ;
let R be Relation of the carrier of A;
func R |^ 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 ) ) )
proof end;
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
proof end;
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 Nat;
func R |^ (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 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 Nat
for R being Relation of the carrier of A st R = F . i holds
F . (i + 1) = R |^ A ) )
proof end;
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 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 Nat
for R being Relation of the carrier of A st R = F . i holds
F . (i + 1) = R |^ A ) ) holds
b1 = b2
proof end;
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 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 Nat
for R being Relation of the carrier of A st R = F . i holds
F . (i + 1) = R |^ A ) ) );

theorem Th15: :: 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 )
proof end;

theorem Th16: :: PUA2MSS1:17
for A being partial non-empty UAStr
for i being Nat
for R being Relation of the carrier of A holds R |^ (A,(i + 1)) = (R |^ (A,i)) |^ A
proof end;

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)
proof end;

theorem Th18: :: 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 )
proof end;

theorem Th19: :: PUA2MSS1:20
for A being partial non-empty UAStr
for R being Relation of the carrier of A holds R |^ A c= R
proof end;

theorem Th20: :: 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 )
proof end;

definition
let A be partial non-empty UAStr ;
defpred S1[ set , set ] means for i being Element of NAT holds [$1,$2] in () |^ (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 () |^ (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 () |^ (A,i) )
proof end;
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 () |^ (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 () |^ (A,i) ) ) holds
b1 = b2
proof end;
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 () |^ (A,i) ) );

theorem Th21: :: PUA2MSS1:22
for A being partial non-empty UAStr holds LimDomRel A c= DomRel A
proof end;

registration
let A be partial non-empty UAStr ;
coherence
( LimDomRel A is total & LimDomRel A is symmetric & LimDomRel A is transitive )
proof end;
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_partitable_wrt P means :: PUA2MSS1:def 8
for p being FinSequence of P ex a being Element of P st f .: () c= a;
end;

:: deftheorem 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 .: () c= a );

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;

:: deftheorem 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
proof end;

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]
proof end;

theorem Th23: :: PUA2MSS1:24
for A being partial non-empty UAStr
for f being operation of A holds f is_exactly_partitable_wrt Class ()
proof end;

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
proof end;
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
proof end;
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 () is a_partition of A
proof end;

theorem Th25: :: 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
proof end;

theorem Th26: :: PUA2MSS1:27
for A being partial non-empty UAStr
for P being a_partition of A holds P is_finer_than Class ()
proof end;

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
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 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 Th27: :: 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
proof end;

theorem Th28: :: 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
proof end;

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;

:: 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 pred S1 is_rougher_than S2;
reflexivity
for S1 being non empty non void ManySortedSign holds (b1,b1)
proof end;
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
proof end;

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)) .: () 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)) .: () c= the ResultSort of b1 . [o,p] ) ) )
proof end;
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)) .: () 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)) .: () c= the ResultSort of b2 . [o,p] ) ) holds
b1 = b2
;
proof end;
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)) .: () 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 )
proof end;
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 func o 1 -> OperSymbol of A;
coherence
o 1 is OperSymbol of A
proof end;
:: original: 2
redefine func o 2 -> Element of P * ;
coherence
o 2 is Element of P *
proof end;
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;
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;

:: deftheorem 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 ;
pred A 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)
proof end;

theorem Th31: :: 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 * () = r & s in Q . o )
proof end;

theorem :: PUA2MSS1:33
for A being partial non-empty UAStr
for P being a_partition of A st P = Class () holds
for S being non empty non void ManySortedSign st A can_be_characterized_by S holds
MSSign (A,P) is_rougher_than S
proof end;