PUA2MSS1: Minimal Manysorted Signature for Partial Algebra

proof end;

end;

registration

let A be non empty set ;

cluster Relation-like non-empty NAT -defined PFuncs ((A *),A) -valued non empty Function-like V50() FinSequence-like FinSubsequence-like countable homogeneous quasi_total for FinSequence of PFuncs ((A *),A);

proof end;

end;

registration

cluster non-empty -> non empty for UAStr ;

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

end;

:: deftheorem defines Den PUA2MSS1:def 1 :

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 { (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 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 );

proof end;

end;

:: deftheorem Def2 defines IndexedPartition PUA2MSS1:def 2 :

definition

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

end;

registration

let X be set ;

cluster -> non-empty one-to-one for IndexedPartition of X;

proof end;

end;

registration

let X be non empty set ;

cluster -> non empty for IndexedPartition of X;

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

proof end;

correctness

proof end;

end;

:: deftheorem Def3 defines -index_of PUA2MSS1:def 3 :

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{ 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 :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 ) );

proof end;

proof end;

end;

:: deftheorem Def4 defines DomRel PUA2MSS1:def 4 :

registration

let A be partial non-empty UAStr ;

cluster DomRel A -> total symmetric 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 ) ) );

proof end;

proof end;

end;

:: deftheorem Def5 defines |^ PUA2MSS1:def 5 :

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

proof end;

proof end;

end;

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

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

proof end;

proof end;

end;

:: deftheorem Def7 defines LimDomRel PUA2MSS1:def 7 :

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 ;

cluster LimDomRel A -> total symmetric 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 .: (product p) c= a;

end;

:: deftheorem defines is_partitable_wrt PUA2MSS1:def 8 :

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 :

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{ 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 Th23: :: PUA2MSS1:24

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 :Def10: :: PUA2MSS1:def 10
for f being operation of A holds f is_exactly_partitable_wrt it;

proof end;

end;

:: deftheorem Def10 defines a_partition PUA2MSS1:def 10 :

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;

proof end;

end;

:: deftheorem Def11 defines IndexedPartition PUA2MSS1:def 11 :

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

end;

theorem :: PUA2MSS1:25

for A being partial non-empty UAStr holds Class (LimDomRel A) 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 (LimDomRel A)

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 :

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 :

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: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)) .: (product p) c= the ResultSort of it . [o,p] ) ) );

proof end;

correctness

proof end;

end;

:: deftheorem Def14 defines MSSign PUA2MSS1:def 14 :

registration

let A be partial non-empty UAStr ;
let P be a_partition of A;

cluster MSSign (A,P) -> non empty non void strict ;