:: by Grzegorz Bancerek

::

:: Received October 1, 1995

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

coherence

for b_{1} being FinSequence of X holds b_{1} is non-empty

end;
coherence

for b

proof end;

registration

let A be non empty set ;

ex b_{1} being PFuncFinSequence of A st

( b_{1} is homogeneous & b_{1} is quasi_total & b_{1} is non-empty & not b_{1} is empty )

end;
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 PFuncFinSequence of A;

existence ex b

( b

proof end;

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

( dom f = dom g & ( for x being set st x in dom f holds

f . x c= g . x ) )

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

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_{1} being Element of S holds b_{1} is PartFunc of A,B

end;
let S be non empty Subset of (PFuncs (A,B));

:: original: Element

redefine mode Element of S -> PartFunc of A,B;

coherence

for b

proof 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;
mode OperSymbol of A is Element of dom the charact of A;

mode operation of A is Element of rng the charact of A;

definition

let A be non-empty UAStr ;

let o be OperSymbol of A;

correctness

coherence

the charact of A . o is operation of A;

by FUNCT_1:def 3;

end;
let o be OperSymbol of A;

correctness

coherence

the charact of A . o is operation of A;

by FUNCT_1:def 3;

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

for A being non-empty UAStr

for o being OperSymbol of A holds Den (o,A) = the charact of A . o;

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

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 )

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 )

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

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

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 *

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

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

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

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}

for p being FinSequence of SmallestPartition X ex q being FinSequence of X st product p = {q}

proof end;

definition

let X be set ;

ex b_{1} being Function st

( rng b_{1} is a_partition of X & b_{1} is one-to-one )

end;
mode IndexedPartition of X -> Function means :Def2: :: PUA2MSS1:def 2

( rng it is a_partition of X & it is one-to-one );

existence ( rng it is a_partition of X & it is one-to-one );

ex b

( rng b

proof end;

:: deftheorem Def2 defines IndexedPartition PUA2MSS1:def 2 :

for X being set

for b_{2} being Function holds

( b_{2} is IndexedPartition of X iff ( rng b_{2} is a_partition of X & b_{2} is one-to-one ) );

for X being set

for b

( b

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

registration

let X be set ;

coherence

for b_{1} being IndexedPartition of X holds

( b_{1} is one-to-one & b_{1} is non-empty )

end;
coherence

for b

( b

proof end;

registration

let X be non empty set ;

coherence

for b_{1} being IndexedPartition of X holds not b_{1} is empty

end;
coherence

for b

proof 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

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

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;

existence

ex b_{1} being set st

( b_{1} in dom P & x in P . b_{1} )

uniqueness

for b_{1}, b_{2} being set st b_{1} in dom P & x in P . b_{1} & b_{2} in dom P & x in P . b_{2} holds

b_{1} = b_{2};

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

existence

ex b

( b

proof end;

correctness uniqueness

for b

b

proof 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 b_{4} being set holds

( b_{4} = P -index_of x iff ( b_{4} in dom P & x in P . b_{4} ) );

for X being set

for P being IndexedPartition of X

for x being object st x in X holds

for b

( b

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

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

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_{1}() -> non empty set , F_{2}() -> non empty set , F_{3}() -> Nat, F_{4}() -> Relation of F_{1}(),F_{2}(), F_{5}( set , set ) -> Relation of F_{1}(),F_{2}() } :

IndRelationEx{ F

ex R being Relation of F_{1}(),F_{2}() ex F being ManySortedSet of NAT st

( R = F . F_{3}() & F . 0 = F_{4}() & ( for i being Nat

for R being Relation of F_{1}(),F_{2}() st R = F . i holds

F . (i + 1) = F_{5}(R,i) ) )

( R = F . F

for R being Relation of F

F . (i + 1) = F

proof end;

scheme :: PUA2MSS1:sch 2

RelationUniq{ F_{1}() -> non empty set , F_{2}() -> non empty set , P_{1}[ set , set ] } :

RelationUniq{ F

for R1, R2 being Relation of F_{1}(),F_{2}() st ( for x being Element of F_{1}()

for y being Element of F_{2}() holds

( [x,y] in R1 iff P_{1}[x,y] ) ) & ( for x being Element of F_{1}()

for y being Element of F_{2}() holds

( [x,y] in R2 iff P_{1}[x,y] ) ) holds

R1 = R2

for y being Element of F

( [x,y] in R1 iff P

for y being Element of F

( [x,y] in R2 iff P

R1 = R2

proof end;

scheme :: PUA2MSS1:sch 3

IndRelationUniq{ F_{1}() -> non empty set , F_{2}() -> non empty set , F_{3}() -> Nat, F_{4}() -> Relation of F_{1}(),F_{2}(), F_{5}( set , set ) -> Relation of F_{1}(),F_{2}() } :

IndRelationUniq{ F

for R1, R2 being Relation of F_{1}(),F_{2}() st ex F being ManySortedSet of NAT st

( R1 = F . F_{3}() & F . 0 = F_{4}() & ( for i being Nat

for R being Relation of F_{1}(),F_{2}() st R = F . i holds

F . (i + 1) = F_{5}(R,i) ) ) & ex F being ManySortedSet of NAT st

( R2 = F . F_{3}() & F . 0 = F_{4}() & ( for i being Nat

for R being Relation of F_{1}(),F_{2}() st R = F . i holds

F . (i + 1) = F_{5}(R,i) ) ) holds

R1 = R2

( R1 = F . F

for R being Relation of F

F . (i + 1) = F

( R2 = F . F

for R being Relation of F

F . (i + 1) = F

R1 = R2

proof end;

definition

let A be partial non-empty UAStr ;

ex b_{1} being Relation of the carrier of A st

for x, y being Element of A holds

( [x,y] in b_{1} 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 b_{1}, b_{2} being Relation of the carrier of A st ( for x, y being Element of A holds

( [x,y] in b_{1} 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_{2} 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_{1} = b_{2}

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

ex b

for x, y being Element of A holds

( [x,y] in b

for p, q being FinSequence holds

( (p ^ <*x*>) ^ q in dom f iff (p ^ <*y*>) ^ q in dom f ) )

proof end;

uniqueness for b

( [x,y] in b

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

for p, q being FinSequence holds

( (p ^ <*x*>) ^ q in dom f iff (p ^ <*y*>) ^ q in dom f ) ) ) holds

b

proof end;

:: deftheorem Def4 defines DomRel PUA2MSS1:def 4 :

for A being partial non-empty UAStr

for b_{2} being Relation of the carrier of A holds

( b_{2} = DomRel A iff for x, y being Element of A holds

( [x,y] in b_{2} 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 A being partial non-empty UAStr

for b

( b

( [x,y] in b

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 )

end;
coherence

( DomRel A is total & DomRel A is symmetric & DomRel A is transitive )

proof end;

definition

let A be partial non-empty UAStr ;

let R be Relation of the carrier of A;

ex b_{1} being Relation of the carrier of A st

for x, y being Element of A holds

( [x,y] in b_{1} 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 b_{1}, b_{2} being Relation of the carrier of A st ( for x, y being Element of A holds

( [x,y] in b_{1} 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_{2} 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_{1} = b_{2}

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

ex b

for x, y being Element of A holds

( [x,y] in b

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

( [x,y] in b

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

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

proof end;

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

for A being partial non-empty UAStr

for R, b_{3} being Relation of the carrier of A holds

( b_{3} = R |^ A iff for x, y being Element of A holds

( [x,y] in b_{3} 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 A being partial non-empty UAStr

for R, b

( b

( [x,y] in b

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;

ex b_{1} being Relation of the carrier of A ex F being ManySortedSet of NAT st

( b_{1} = 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 ) )

for b_{1}, b_{2} being Relation of the carrier of A st ex F being ManySortedSet of NAT st

( b_{1} = 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

( b_{2} = 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

b_{1} = b_{2}

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

ex b

( b

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

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

for R being Relation of the carrier of A st R = F . i holds

F . (i + 1) = R |^ A ) ) holds

b

proof 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 b_{4} being Relation of the carrier of A holds

( b_{4} = R |^ (A,i) iff ex F being ManySortedSet of NAT st

( b_{4} = 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 ) ) );

for A being partial non-empty UAStr

for R being Relation of the carrier of A

for i being Nat

for b

( b

( b

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 )

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

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)

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 )

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

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_{1}[ set , set ] means for i being Element of NAT holds [$1,$2] in (DomRel A) |^ (A,i);

ex b_{1} being Relation of the carrier of A st

for x, y being Element of A holds

( [x,y] in b_{1} iff for i being Element of NAT holds [x,y] in (DomRel A) |^ (A,i) )

for b_{1}, b_{2} being Relation of the carrier of A st ( for x, y being Element of A holds

( [x,y] in b_{1} 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_{2} iff for i being Element of NAT holds [x,y] in (DomRel A) |^ (A,i) ) ) holds

b_{1} = b_{2}

end;
defpred S

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

ex b

for x, y being Element of A holds

( [x,y] in b

proof end;

uniqueness for b

( [x,y] in b

( [x,y] in b

b

proof end;

:: deftheorem Def7 defines LimDomRel PUA2MSS1:def 7 :

for A being partial non-empty UAStr

for b_{2} being Relation of the carrier of A holds

( b_{2} = LimDomRel A iff for x, y being Element of A holds

( [x,y] in b_{2} iff for i being Element of NAT holds [x,y] in (DomRel A) |^ (A,i) ) );

for A being partial non-empty UAStr

for b

( b

( [x,y] in b

registration

let A be partial non-empty UAStr ;

coherence

( LimDomRel A is total & LimDomRel A is symmetric & LimDomRel A is transitive )

end;
coherence

( LimDomRel A is total & LimDomRel A is symmetric & LimDomRel A is transitive )

proof end;

definition

let X be non empty set ;

let f be PartFunc of (X *),X;

let P be a_partition of X;

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

for p being FinSequence of P ex a being Element of P st f .: (product p) c= a;

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

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;

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

( f is_partitable_wrt P & ( for p being FinSequence of P st product p meets dom f holds

product p c= dom f ) );

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

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

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_{1}() -> FinSequence, F_{2}() -> FinSequence, P_{1}[ set ], P_{2}[ set , set ] } :

provided

FiniteTransitivity{ F

provided

A1:
P_{1}[F_{1}()]
and

A2: len F_{1}() = len F_{2}()
and

A3: for p, q being FinSequence

for z1, z2 being set st P_{1}[(p ^ <*z1*>) ^ q] & P_{2}[z1,z2] holds

P_{1}[(p ^ <*z2*>) ^ q]
and

A4: for i being Element of NAT st i in dom F_{1}() holds

P_{2}[F_{1}() . i,F_{2}() . i]

A2: len F

A3: for p, q being FinSequence

for z1, z2 being set st P

P

A4: for i being Element of NAT st i in dom F

P

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)

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 ;

ex b_{1} being a_partition of the carrier of A st

for f being operation of A holds f is_exactly_partitable_wrt b_{1}

end;
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 for f being operation of A holds f is_exactly_partitable_wrt it;

ex b

for f being operation of A holds f is_exactly_partitable_wrt b

proof end;

:: deftheorem Def10 defines a_partition PUA2MSS1:def 10 :

for A being partial non-empty UAStr

for b_{2} being a_partition of the carrier of A holds

( b_{2} is a_partition of A iff for f being operation of A holds f is_exactly_partitable_wrt b_{2} );

for A being partial non-empty UAStr

for b

( b

definition

let A be partial non-empty UAStr ;

ex b_{1} being IndexedPartition of the carrier of A st rng b_{1} is a_partition of A

end;
mode IndexedPartition of A -> IndexedPartition of the carrier of A means :Def11: :: PUA2MSS1:def 11

rng it is a_partition of A;

existence rng it is a_partition of A;

ex b

proof end;

:: deftheorem Def11 defines IndexedPartition PUA2MSS1:def 11 :

for A being partial non-empty UAStr

for b_{2} being IndexedPartition of the carrier of A holds

( b_{2} is IndexedPartition of A iff rng b_{2} is a_partition of A );

for A being partial non-empty UAStr

for b

( b

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

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

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)

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;

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

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

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

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

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 ;

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

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

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

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 (b_{1},b_{1})

end;
:: original: is_rougher_than

redefine pred S1 is_rougher_than S2;

reflexivity

for S1 being non empty non void ManySortedSign holds (b

proof 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

S1 is_rougher_than S3

proof end;

definition

let A be partial non-empty UAStr ;

let P be a_partition of A;

ex b_{1} being strict ManySortedSign st

( the carrier of b_{1} = P & the carrier' of b_{1} = { [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_{1} . [o,p] = p & (Den (o,A)) .: (product p) c= the ResultSort of b_{1} . [o,p] ) ) )

uniqueness

for b_{1}, b_{2} being strict ManySortedSign st the carrier of b_{1} = P & the carrier' of b_{1} = { [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_{1} . [o,p] = p & (Den (o,A)) .: (product p) c= the ResultSort of b_{1} . [o,p] ) ) & the carrier of b_{2} = P & the carrier' of b_{2} = { [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_{2} . [o,p] = p & (Den (o,A)) .: (product p) c= the ResultSort of b_{2} . [o,p] ) ) holds

b_{1} = b_{2};

end;
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 ( 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] ) ) );

ex b

( the carrier of b

for p being Element of P * st product p meets dom (Den (o,A)) holds

( the Arity of b

proof end;

correctness uniqueness

for b

for p being Element of P * st product p meets dom (Den (o,A)) holds

( the Arity of b

for p being Element of P * st product p meets dom (Den (o,A)) holds

( the Arity of b

b

proof end;

:: deftheorem Def14 defines MSSign PUA2MSS1:def 14 :

for A being partial non-empty UAStr

for P being a_partition of A

for b_{3} being strict ManySortedSign holds

( b_{3} = MSSign (A,P) iff ( the carrier of b_{3} = P & the carrier' of b_{3} = { [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_{3} . [o,p] = p & (Den (o,A)) .: (product p) c= the ResultSort of b_{3} . [o,p] ) ) ) );

for A being partial non-empty UAStr

for P being a_partition of A

for b

( b

for p being Element of P * st product p meets dom (Den (o,A)) holds

( the Arity of b

registration

let A be partial non-empty UAStr ;

let P be a_partition of A;

coherence

( not MSSign (A,P) is empty & not MSSign (A,P) is void )

end;
let P be a_partition of A;

coherence

( not MSSign (A,P) is empty & not MSSign (A,P) is void )

proof 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

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

coherence

o `2 is Element of P *

end;
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: `2redefine func o `2 -> Element of P * ;

coherence

o `2 is Element of P *

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

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

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

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

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 ;

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

ex G being MSAlgebra over S ex P being IndexedPartition of the carrier' of S st A can_be_characterized_by S,G,P;

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

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)

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 * (the_arity_of s) = r & s in Q . o )

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 )

proof end;

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

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;