:: PUA2MSS1 semantic presentation

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, Y be non empty set ;
cluster non empty Relation of X,Y;
existence

proof end;

end;

registration

let X be with_non-empty_elements set ;
cluster -> non-empty FinSequence of X;
coherence

proof end;

end;

registration

let A be non empty set ;
cluster non empty non-empty homogeneous quasi_total FinSequence of PFuncs (A * ),A;
existence

proof end;

end;

registration

cluster non-empty -> non empty UAStr ;
coherence

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: rng
redefine func rng f -> Subset of (PFuncs (A * ),A);
coherence 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

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 by FUNCT_1:def 5;

end;

:: deftheorem defines Den PUA2MSS1:def 1 :

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

definition

let X be set ;
func SmallestPartition X -> a_partition of X equals :: PUA2MSS1:def 2
Class (id X);
correctness ;

end;

:: deftheorem defines SmallestPartition PUA2MSS1:def 2 :

theorem Th13: :: PUA2MSS1:13

for X being non empty set holds SmallestPartition X = { {x} where x is Element of X : verum }

proof end;

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

proof end;

end;

:: deftheorem Def3 defines IndexedPartition PUA2MSS1:def 3 :

definition

let X be set ;
let P be IndexedPartition of X;
:: original: rng
redefine func rng P -> a_partition of X;
coherence by Def3;

end;

registration

let X be set ;
cluster -> non-empty one-to-one IndexedPartition of X;
coherence

proof end;

end;

registration

let X be non empty set ;
cluster -> non empty non-empty one-to-one IndexedPartition of X;
coherence

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

proof end;

end;

definition

let X be set ;
let P be IndexedPartition of X;
let x be set ;
assume A1: x in X ;
then 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

proof end;

correctness

proof end;

end;

:: deftheorem Def4 defines -index_of PUA2MSS1:def 4 :

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;

scheme :: PUA2MSS1:sch 1
IndRelationEx{ F₁() -> non empty set , F₂() -> non empty set , F₃() -> 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 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₃() -> 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 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 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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def5 defines DomRel PUA2MSS1:def 5 :

registration

let A be partial non-empty UAStr ;
cluster DomRel A -> symmetric transitive total ;
coherence

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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def6 defines |^ PUA2MSS1:def 6 :

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 :Def7: :: PUA2MSS1:def 7
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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def7 defines |^ PUA2MSS1:def 7 :

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 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 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 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 ;
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 Nat holds [x,y] in (DomRel A) |^ A,i );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def8 defines LimDomRel PUA2MSS1:def 8 :

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 -> symmetric transitive total ;
coherence

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

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 :

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

proof end;

end;

:: deftheorem Def11 defines a_partition PUA2MSS1:def 11 :

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

proof end;

end;

:: deftheorem Def12 defines IndexedPartition PUA2MSS1:def 12 :

definition

let A be partial non-empty UAStr ;
let P be IndexedPartition of A;
:: original: rng
redefine func rng P -> a_partition of A;
coherence 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;

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 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
for 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;

:: deftheorem Def13 defines form_morphism_between PUA2MSS1:def 13 :

theorem Th29: :: PUA2MSS1:29

for S being non empty non void ManySortedSign holds id the carrier of S, id the OperSymbols 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 OperSymbols of S1 );

end;

:: deftheorem defines is_rougher_than PUA2MSS1:def 14 :

definition

let S1, S2 be non empty non void ManySortedSign ;
:: original: is_rougher_than
redefine pred S1 is_rougher_than S2;
reflexivity

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;

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

proof end;

correctness

proof end;

end;

:: deftheorem Def15 defines MSSign PUA2MSS1:def 15 :

registration

let A be partial non-empty UAStr ;
let P be a_partition of A;
cluster MSSign A,P -> non empty strict non void ;
coherence

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

proof end;

:: original: `2
redefine func o `2 -> Element of P * ;
coherence

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

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 OperSymbols of S st A can_be_characterized_by S,G,P;

end;

:: deftheorem defines can_be_characterized_by PUA2MSS1:def 17 :

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 OperSymbols 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;