:: Minimal Manysorted Signature for Partial Algebra
:: by Grzegorz Bancerek
::
:: Received October 1, 1995
:: Copyright (c) 1995-2011 Association of Mizar Users

begin

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 FinSequence of X;
coherence
for b₁ being FinSequence of X holds b₁ is non-empty

proof end;

end;

registration

let A be non empty set ;
cluster non empty Relation-like non-empty NAT -defined PFuncs ((A *),A) -valued Function-like V38() countable FinSequence-like FinSubsequence-like homogeneous quasi_total FinSequence of PFuncs ((A *),A);
existence
ex b₁ being PFuncFinSequence of A st
( b₁ is homogeneous & b₁ is quasi_total & b₁ is non-empty & not b₁ is empty )

proof end;

end;

registration

cluster non-empty -> non empty UAStr ;
coherence
for b₁ being UAStr st b₁ is non-empty holds
not b₁ 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 b₁ being Element of S holds b₁ 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 5;

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 Th3: :: PUA2MSS1:3

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

proof end;

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

proof end;

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 )

proof end;

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 )

proof end;

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

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 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 *

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 { (product p) where p is Element of n -tuples_on P : verum } is a_partition of n -tuples_on X

proof end;

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

proof end;

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

proof end;

theorem :: PUA2MSS1:13

canceled;

theorem Th14: :: PUA2MSS1:14

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 ;
canceled;
mode IndexedPartition of X -> Function means :Def3: :: PUA2MSS1:def 3
( rng it is a_partition of X & it is one-to-one );
existence
ex b₁ being Function st
( rng b₁ is a_partition of X & b₁ is one-to-one )

proof end;

end;

:: deftheorem PUA2MSS1:def 2 :
canceled;

:: deftheorem Def3 defines IndexedPartition PUA2MSS1:def 3 :
for X being set
for b₂ being Function holds
( b₂ is IndexedPartition of X iff ( rng b₂ is a_partition of X & b₂ 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 Def3;

end;

registration

let X be set ;
cluster -> non-empty one-to-one IndexedPartition of X;
coherence
for b₁ being IndexedPartition of X holds
( b₁ is one-to-one & b₁ is non-empty )

proof end;

end;

registration

let X be non empty set ;
cluster -> non empty IndexedPartition of X;
coherence
for b₁ being IndexedPartition of X holds not b₁ 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 set ;
assume A1: x in X ;
A2: union (rng P) = X by EQREL_1:def 6;
func P -index_of x -> set means :Def4: :: PUA2MSS1:def 4
( it in dom P & x in P . it );
existence
ex b₁ being set st
( b₁ in dom P & x in P . b₁ )

proof end;

correctness
uniqueness
for b₁, b₂ being set st b₁ in dom P & x in P . b₁ & b₂ in dom P & x in P . b₂ holds
b₁ = b₂;

proof end;

end;

:: deftheorem Def4 defines -index_of PUA2MSS1:def 4 :
for X being set
for P being IndexedPartition of X
for x being set st x in X holds
for b₄ being set holds
( b₄ = P -index_of x iff ( b₄ in dom P & x in P . b₄ ) );

theorem Th15: :: PUA2MSS1:15

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 Th16: :: PUA2MSS1:16

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;

begin

scheme :: PUA2MSS1:sch 1
IndRelationEx{ F₁() -> non empty set , F₂() -> non empty set , F₃() -> Element of NAT , F₄() -> Relation of F₁(),F₂(), F₅( set , set ) -> Relation of F₁(),F₂() } :

ex R being Relation of F₁(),F₂() ex F being ManySortedSet of NAT st
( R = F . F₃() & F . 0 = F₄() & ( for i being Element of NAT
for R being Relation of F₁(),F₂() st R = F . i holds
F . (i + 1) = F₅(R,i) ) )

proof end;

scheme :: PUA2MSS1:sch 2
RelationUniq{ F₁() -> non empty set , F₂() -> non empty set , P₁[ set , set ] } :

for R1, R2 being Relation of F₁(),F₂() st ( for x being Element of F₁()
for y being Element of F₂() holds
( [x,y] in R1 iff P₁[x,y] ) ) & ( for x being Element of F₁()
for y being Element of F₂() holds
( [x,y] in R2 iff P₁[x,y] ) ) holds
R1 = R2

proof end;

scheme :: PUA2MSS1:sch 3
IndRelationUniq{ F₁() -> non empty set , F₂() -> non empty set , F₃() -> Element of NAT , F₄() -> Relation of F₁(),F₂(), F₅( set , set ) -> Relation of F₁(),F₂() } :

for R1, R2 being Relation of F₁(),F₂() st ex F being ManySortedSet of NAT st
( R1 = F . F₃() & F . 0 = F₄() & ( for i being Element of NAT
for R being Relation of F₁(),F₂() st R = F . i holds
F . (i + 1) = F₅(R,i) ) ) & ex F being ManySortedSet of NAT st
( R2 = F . F₃() & F . 0 = F₄() & ( for i being Element of NAT
for R being Relation of F₁(),F₂() st R = F . i holds
F . (i + 1) = F₅(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 :Def5: :: PUA2MSS1:def 5
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 b₁ being Relation of the carrier of A st
for x, y being Element of A holds
( [x,y] in b₁ 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 b₁, b₂ being Relation of the carrier of A st ( for x, y being Element of A holds
( [x,y] in b₁ 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 b₂ 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
b₁ = b₂

proof end;

end;

:: deftheorem Def5 defines DomRel PUA2MSS1:def 5 :
for A being partial non-empty UAStr
for b₂ being Relation of the carrier of A holds
( b₂ = DomRel A iff for x, y being Element of A holds
( [x,y] in b₂ 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 )

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 :Def6: :: 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 ) ) );
existence
ex b₁ being Relation of the carrier of A st
for x, y being Element of A holds
( [x,y] in b₁ 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 b₁, b₂ being Relation of the carrier of A st ( for x, y being Element of A holds
( [x,y] in b₁ 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 b₂ 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
b₁ = b₂

proof end;

end;

:: deftheorem Def6 defines |^ PUA2MSS1:def 6 :
for A being partial non-empty UAStr
for R, b₃ being Relation of the carrier of A holds
( b₃ = R |^ A iff for x, y being Element of A holds
( [x,y] in b₃ 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 ;
func R |^ (A,i) -> Relation of the carrier of A means :Def7: :: PUA2MSS1:def 7
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 b₁ being Relation of the carrier of A ex F being ManySortedSet of NAT st
( b₁ = 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 ) )

proof end;

uniqueness
for b₁, b₂ being Relation of the carrier of A st ex F being ManySortedSet of NAT st
( b₁ = 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
( b₂ = 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
b₁ = b₂

proof end;

end;

:: deftheorem Def7 defines |^ PUA2MSS1:def 7 :
for A being partial non-empty UAStr
for R being Relation of the carrier of A
for i being Element of NAT
for b₄ being Relation of the carrier of A holds
( b₄ = R |^ (A,i) iff ex F being ManySortedSet of NAT st
( b₄ = 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 Th17: :: PUA2MSS1:17

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 Th18: :: PUA2MSS1:18

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

proof end;

theorem :: PUA2MSS1:19

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 Th20: :: PUA2MSS1:20

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 Th21: :: PUA2MSS1:21

for A being partial non-empty UAStr
for R being Relation of the carrier of A holds R |^ A c= R

proof end;

theorem Th22: :: PUA2MSS1:22

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 S₁[ 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 :Def8: :: PUA2MSS1:def 8
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 b₁ being Relation of the carrier of A st
for x, y being Element of A holds
( [x,y] in b₁ iff for i being Element of NAT holds [x,y] in (DomRel A) |^ (A,i) )

proof end;

uniqueness
for b₁, b₂ being Relation of the carrier of A st ( for x, y being Element of A holds
( [x,y] in b₁ 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 b₂ iff for i being Element of NAT holds [x,y] in (DomRel A) |^ (A,i) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def8 defines LimDomRel PUA2MSS1:def 8 :
for A being partial non-empty UAStr
for b₂ being Relation of the carrier of A holds
( b₂ = LimDomRel A iff for x, y being Element of A holds
( [x,y] in b₂ iff for i being Element of NAT holds [x,y] in (DomRel A) |^ (A,i) ) );

theorem Th23: :: PUA2MSS1:23

for A being partial non-empty UAStr holds LimDomRel A c= DomRel A

proof end;

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 )

proof end;

end;

begin

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 :Def9: :: PUA2MSS1:def 9
for p being FinSequence of P ex a being Element of P st f .: (product p) c= a;

end;

:: deftheorem Def9 defines is_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_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;
pred f is_exactly_partitable_wrt P means :Def10: :: 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;

:: deftheorem Def10 defines is_exactly_partitable_wrt PUA2MSS1:def 10 :
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:24

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{ F₁() -> FinSequence, F₂() -> FinSequence, P₁[ set ], P₂[ set , set ] } :

P₁[F₂()]

provided

A1: P₁[F₁()] and
A2: len F₁() = len F₂() and
A3: for p, q being FinSequence
for z1, z2 being set st P₁[(p ^ <*z1*>) ^ q] & P₂[z1,z2] holds
P₁[(p ^ <*z2*>) ^ q] and
A4: for i being Element of NAT st i in dom F₁() holds
P₂[F₁() . i,F₂() . i]

proof end;

theorem Th25: :: PUA2MSS1:25

for A being partial non-empty UAStr
for f being operation of A holds f is_exactly_partitable_wrt Class (LimDomRel A)

proof end;

definition

let A be partial non-empty UAStr ;
mode a_partition of A -> a_partition of the carrier of A means :Def11: :: PUA2MSS1:def 11
for f being operation of A holds f is_exactly_partitable_wrt it;
existence
ex b₁ being a_partition of the carrier of A st
for f being operation of A holds f is_exactly_partitable_wrt b₁

proof end;

end;

:: deftheorem Def11 defines a_partition PUA2MSS1:def 11 :
for A being partial non-empty UAStr
for b₂ being a_partition of the carrier of A holds
( b₂ is a_partition of A iff for f being operation of A holds f is_exactly_partitable_wrt b₂ );

definition

let A be partial non-empty UAStr ;
mode IndexedPartition of A -> IndexedPartition of the carrier of A means :Def12: :: PUA2MSS1:def 12
rng it is a_partition of A;
existence
ex b₁ being IndexedPartition of the carrier of A st rng b₁ is a_partition of A

proof end;

end;

:: deftheorem Def12 defines IndexedPartition PUA2MSS1:def 12 :
for A being partial non-empty UAStr
for b₂ being IndexedPartition of the carrier of A holds
( b₂ is IndexedPartition of A iff rng b₂ 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 Def12;

end;

theorem :: PUA2MSS1:26

for A being partial non-empty UAStr holds Class (LimDomRel A) is a_partition of A

proof end;

theorem Th27: :: PUA2MSS1:27

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 Th28: :: PUA2MSS1:28

for A being partial non-empty UAStr
for P being a_partition of A holds P is_finer_than Class (LimDomRel A)

proof end;

begin

definition

let S1, S2 be ManySortedSign ;
let f, g be Function;
pred f,g form_morphism_between S1,S2 means :Def13: :: PUA2MSS1:def 13
( 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 Def13 defines form_morphism_between PUA2MSS1:def 13 :
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 Th29: :: PUA2MSS1:29

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 Th30: :: 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

proof end;

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 carrier' of S1 );

end;

:: deftheorem defines is_rougher_than PUA2MSS1:def 14 :
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 S1 is_rougher_than S1

proof end;

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

proof end;

begin

definition

let A be partial non-empty UAStr ;
let P be a_partition of A;
func MSSign (A,P) -> strict ManySortedSign means :Def15: :: PUA2MSS1:def 15
( 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 b₁ being strict ManySortedSign st
( the carrier of b₁ = P & the carrier' of b₁ = { [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 b₁ . [o,p] = p & (Den (o,A)) .: (product p) c= the ResultSort of b₁ . [o,p] ) ) )

proof end;

correctness
uniqueness
for b₁, b₂ being strict ManySortedSign st the carrier of b₁ = P & the carrier' of b₁ = { [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 b₁ . [o,p] = p & (Den (o,A)) .: (product p) c= the ResultSort of b₁ . [o,p] ) ) & the carrier of b₂ = P & the carrier' of b₂ = { [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 b₂ . [o,p] = p & (Den (o,A)) .: (product p) c= the ResultSort of b₂ . [o,p] ) ) holds
b₁ = b₂;

proof end;

end;

:: deftheorem Def15 defines MSSign PUA2MSS1:def 15 :
for A being partial non-empty UAStr
for P being a_partition of A
for b₃ being strict ManySortedSign holds
( b₃ = MSSign (A,P) iff ( the carrier of b₃ = P & the carrier' of b₃ = { [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 b₃ . [o,p] = p & (Den (o,A)) .: (product p) c= the ResultSort of b₃ . [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 of S;
let P be IndexedPartition of the carrier' of S;
pred A can_be_characterized_by S,G,P means :Def16: :: 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;

:: deftheorem Def16 defines can_be_characterized_by PUA2MSS1:def 16 :
for A being partial non-empty UAStr
for S being non empty non void ManySortedSign
for G being MSAlgebra of 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 17
ex G being MSAlgebra of 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 17 :
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 of S ex P being IndexedPartition of the carrier' of S st A can_be_characterized_by S,G,P );

theorem :: PUA2MSS1:32

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 Th33: :: PUA2MSS1:33

for A being partial non-empty UAStr
for S being non empty non void ManySortedSign
for G being MSAlgebra of 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 )

proof end;

theorem :: PUA2MSS1:34

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

proof end;