:: PUA2MSS1 semantic presentation

Lemma1: for b₁ being FinSequence
for b₂ being Function st dom b₂ = dom b₁ holds
b₂ is FinSequence

proof end;

Lemma2: for b₁ being set
for b₂ being non empty set
for b₃ being FinSequence of b₁
for b₄ being Function of b₁,b₂ holds b₄ * b₃ is FinSequence of b₂

proof end;

registration

let c₁, c₂ be non empty set ;
cluster non empty Relation of a₁,a₂;
existence

proof end;

end;

registration

let c₁ be with_non-empty_elements set ;
cluster -> non-empty FinSequence of a₁;
coherence

proof end;

end;

registration

let c₁ 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 b₁, b₂ being non-empty Function st product b₁ c= product b₂ holds
( dom b₁ = dom b₂ & ( for b₃ being set st b₃ in dom b₁ holds
b₁ . b₃ c= b₂ . b₃ ) )

proof end;

theorem Th2: :: PUA2MSS1:2

for b₁, b₂ being non-empty Function st product b₁ = product b₂ holds
b₁ = b₂

proof end;

definition

let c₁ be non empty set ;
let c₂ be PFuncFinSequence of c₁;
redefine func rng as rng c₂ -> Subset of (PFuncs (a₁ * ),a₁);
coherence by FINSEQ_1:def 4;

end;

definition

let c₁, c₂ be non empty set ;
let c₃ be non empty Subset of (PFuncs c₁,c₂);
redefine mode Element as Element of c₃ -> PartFunc of a₁,a₂;
coherence

proof end;

end;

definition

let c₁ 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 c₁ be non-empty UAStr ;
let c₂ be OperSymbol of c₁;
func Den c₂,c₁ -> operation of a₁ equals :: PUA2MSS1:def 1
the charact of a₁ . a₂;
correctness by FUNCT_1:def 5;

end;

:: deftheorem Def1 defines Den PUA2MSS1:def 1 :

theorem Th3: :: PUA2MSS1:3

for b₁ being set
for b₂ being a_partition of b₁
for b₃, b₄, b₅ being set st b₃ in b₄ & b₄ in b₂ & b₃ in b₅ & b₅ in b₂ holds
b₄ = b₅

proof end;

theorem Th4: :: PUA2MSS1:4

for b₁, b₂ being set st b₁ is_finer_than b₂ holds
for b₃ being FinSequence of b₁ ex b₄ being FinSequence of b₂ st product b₃ c= product b₄

proof end;

theorem Th5: :: PUA2MSS1:5

for b₁ being set
for b₂, b₃ being a_partition of b₁
for b₄ being Function of b₂,b₃ st ( for b₅ being set st b₅ in b₂ holds
b₅ c= b₄ . b₅ ) holds
for b₅ being FinSequence of b₂
for b₆ being FinSequence of b₃ holds
( product b₅ c= product b₆ iff b₄ * b₅ = b₆ )

proof end;

theorem Th6: :: PUA2MSS1:6

for b₁ being set
for b₂ being Function st rng b₂ c= union b₁ holds
ex b₃ being Function st
( dom b₃ = dom b₂ & rng b₃ c= b₁ & b₂ in product b₃ )

proof end;

theorem Th7: :: PUA2MSS1:7

for b₁ being set
for b₂ being a_partition of b₁
for b₃ being FinSequence of b₁ ex b₄ being FinSequence of b₂ st b₃ in product b₄

proof end;

theorem Th8: :: PUA2MSS1:8

for b₁, b₂ being non empty set
for b₃ being a_partition of b₁
for b₄ being a_partition of b₂ holds { [:b₅,b₆:] where B is Element of b₃, B is Element of b₄ : verum } is a_partition of [:b₁,b₂:]

proof end;

theorem Th9: :: PUA2MSS1:9

for b₁ being non empty set
for b₂ being a_partition of b₁ holds { (product b₃) where B is Element of b₂ * : verum } is a_partition of b₁ *

proof end;

theorem Th10: :: PUA2MSS1:10

for b₁ being non empty set
for b₂ being Nat
for b₃ being a_partition of b₁ holds { (product b₄) where B is Element of b₂ -tuples_on b₃ : verum } is a_partition of b₂ -tuples_on b₁

proof end;

theorem Th11: :: PUA2MSS1:11

for b₁ being non empty set
for b₂ being set st b₂ c= b₁ holds
for b₃ being a_partition of b₁ holds { (b₄ /\ b₂) where B is Element of b₃ : b₄ meets b₂ } is a_partition of b₂

proof end;

theorem Th12: :: PUA2MSS1:12

for b₁ being non empty Function
for b₂ being a_partition of dom b₁ holds { (b₁ | b₃) where B is Element of b₂ : verum } is a_partition of b₁

proof end;

definition

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

end;

:: deftheorem Def2 defines SmallestPartition PUA2MSS1:def 2 :

theorem Th13: :: PUA2MSS1:13

for b₁ being non empty set holds SmallestPartition b₁ = { {b₂} where B is Element of b₁ : verum }

proof end;

theorem Th14: :: PUA2MSS1:14

for b₁ being set
for b₂ being FinSequence of SmallestPartition b₁ ex b₃ being FinSequence of b₁ st product b₂ = {b₃}

proof end;

definition

let c₁ be set ;
mode IndexedPartition of c₁ -> Function means :Def3: :: PUA2MSS1:def 3
( rng a₂ is a_partition of a₁ & a₂ is one-to-one );
existence

proof end;

end;

:: deftheorem Def3 defines IndexedPartition PUA2MSS1:def 3 :

definition

let c₁ be set ;
let c₂ be IndexedPartition of c₁;
redefine func rng as rng c₂ -> a_partition of a₁;
coherence by Def3;

end;

registration

let c₁ be set ;
cluster -> non-empty one-to-one IndexedPartition of a₁;
coherence

proof end;

end;

registration

let c₁ be non empty set ;
cluster -> non empty non-empty one-to-one IndexedPartition of a₁;
coherence

proof end;

end;

definition

let c₁ be set ;
let c₂ be a_partition of c₁;
redefine func id as id c₂ -> IndexedPartition of a₁;
coherence

proof end;

end;

definition

let c₁ be set ;
let c₂ be IndexedPartition of c₁;
let c₃ be set ;
assume E16: c₃ in c₁ ;
then E17: union (rng c₂) = c₁ by EQREL_1:def 6;
func c₂ -index_of c₃ -> set means :Def4: :: PUA2MSS1:def 4
( a₄ in dom a₂ & a₃ in a₂ . a₄ );
existence

proof end;

correctness

proof end;

end;

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

theorem Th15: :: PUA2MSS1:15

for b₁ being set
for b₂ being non-empty Function st Union b₂ = b₁ & ( for b₃, b₄ being set st b₃ in dom b₂ & b₄ in dom b₂ & b₃ <> b₄ holds
b₂ . b₃ misses b₂ . b₄ ) holds
b₂ is IndexedPartition of b₁

proof end;

theorem Th16: :: PUA2MSS1:16

for b₁, b₂ being non empty set
for b₃ being a_partition of b₂
for b₄ being Function of b₁,b₃ st b₃ c= rng b₄ & b₄ is one-to-one holds
b₄ is IndexedPartition of b₂

proof end;

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

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

proof end;

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

for b₁, b₂ being Relation of F₁(),F₂() st ( for b₃ being Element of F₁()
for b₄ being Element of F₂() holds
( [b₃,b₄] in b₁ iff P₁[b₃,b₄] ) ) & ( for b₃ being Element of F₁()
for b₄ being Element of F₂() holds
( [b₃,b₄] in b₂ iff P₁[b₃,b₄] ) ) holds
b₁ = b₂

proof end;

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

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

proof end;

definition

let c₁ be partial non-empty UAStr ;
func DomRel c₁ -> Relation of the carrier of a₁ means :Def5: :: PUA2MSS1:def 5
for b₁, b₂ being Element of a₁ holds
( [b₁,b₂] in a₂ iff for b₃ being operation of a₁
for b₄, b₅ being FinSequence holds
( (b₄ ^ <*b₁*>) ^ b₅ in dom b₃ iff (b₄ ^ <*b₂*>) ^ b₅ in dom b₃ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def5 defines DomRel PUA2MSS1:def 5 :

registration

let c₁ be partial non-empty UAStr ;
cluster DomRel a₁ -> symmetric transitive total ;
coherence

proof end;

end;

definition

let c₁ be partial non-empty UAStr ;
let c₂ be Relation of the carrier of c₁;
func c₂ |^ c₁ -> Relation of the carrier of a₁ means :Def6: :: PUA2MSS1:def 6
for b₁, b₂ being Element of a₁ holds
( [b₁,b₂] in a₃ iff ( [b₁,b₂] in a₂ & ( for b₃ being operation of a₁
for b₄, b₅ being FinSequence st (b₄ ^ <*b₁*>) ^ b₅ in dom b₃ & (b₄ ^ <*b₂*>) ^ b₅ in dom b₃ holds
[(b₃ . ((b₄ ^ <*b₁*>) ^ b₅)),(b₃ . ((b₄ ^ <*b₂*>) ^ b₅))] in a₂ ) ) );
existence

proof end;

uniqueness

proof end;

end;

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

definition

let c₁ be partial non-empty UAStr ;
let c₂ be Relation of the carrier of c₁;
let c₃ be Nat;
func c₂ |^ c₁,c₃ -> Relation of the carrier of a₁ means :Def7: :: PUA2MSS1:def 7
ex b₁ being ManySortedSet of NAT st
( a₄ = b₁ . a₃ & b₁ . 0 = a₂ & ( for b₂ being Nat
for b₃ being Relation of the carrier of a₁ st b₃ = b₁ . b₂ holds
b₁ . (b₂ + 1) = b₃ |^ a₁ ) );
existence

proof end;

uniqueness

proof end;

end;

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

theorem Th17: :: PUA2MSS1:17

for b₁ being partial non-empty UAStr
for b₂ being Relation of the carrier of b₁ holds
( b₂ |^ b₁,0 = b₂ & b₂ |^ b₁,1 = b₂ |^ b₁ )

proof end;

theorem Th18: :: PUA2MSS1:18

for b₁ being partial non-empty UAStr
for b₂ being Nat
for b₃ being Relation of the carrier of b₁ holds b₃ |^ b₁,(b₂ + 1) = (b₃ |^ b₁,b₂) |^ b₁

proof end;

theorem Th19: :: PUA2MSS1:19

for b₁ being partial non-empty UAStr
for b₂, b₃ being Nat
for b₄ being Relation of the carrier of b₁ holds b₄ |^ b₁,(b₂ + b₃) = (b₄ |^ b₁,b₂) |^ b₁,b₃

proof end;

theorem Th20: :: PUA2MSS1:20

for b₁ being partial non-empty UAStr
for b₂ being Equivalence_Relation of the carrier of b₁ st b₂ c= DomRel b₁ holds
( b₂ |^ b₁ is total & b₂ |^ b₁ is symmetric & b₂ |^ b₁ is transitive )

proof end;

theorem Th21: :: PUA2MSS1:21

for b₁ being partial non-empty UAStr
for b₂ being Relation of the carrier of b₁ holds b₂ |^ b₁ c= b₂

proof end;

theorem Th22: :: PUA2MSS1:22

for b₁ being partial non-empty UAStr
for b₂ being Equivalence_Relation of the carrier of b₁ st b₂ c= DomRel b₁ holds
for b₃ being Nat holds
( b₂ |^ b₁,b₃ is total & b₂ |^ b₁,b₃ is symmetric & b₂ |^ b₁,b₃ is transitive )

proof end;

definition

let c₁ be partial non-empty UAStr ;
func LimDomRel c₁ -> Relation of the carrier of a₁ means :Def8: :: PUA2MSS1:def 8
for b₁, b₂ being Element of a₁ holds
( [b₁,b₂] in a₂ iff for b₃ being Nat holds [b₁,b₂] in (DomRel a₁) |^ a₁,b₃ );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def8 defines LimDomRel PUA2MSS1:def 8 :

theorem Th23: :: PUA2MSS1:23

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

proof end;

registration

let c₁ be partial non-empty UAStr ;
cluster LimDomRel a₁ -> symmetric transitive total ;
coherence

proof end;

end;

definition

let c₁ be non empty set ;
let c₂ be PartFunc of c₁ * ,c₁;
let c₃ be a_partition of c₁;
pred c₂ is_partitable_wrt c₃ means :Def9: :: PUA2MSS1:def 9
for b₁ being FinSequence of a₃ ex b₂ being Element of a₃ st a₂ .: (product b₁) c= b₂;

end;

:: deftheorem Def9 defines is_partitable_wrt PUA2MSS1:def 9 :

definition

let c₁ be non empty set ;
let c₂ be PartFunc of c₁ * ,c₁;
let c₃ be a_partition of c₁;
pred c₂ is_exactly_partitable_wrt c₃ means :Def10: :: PUA2MSS1:def 10
( a₂ is_partitable_wrt a₃ & ( for b₁ being FinSequence of a₃ st product b₁ meets dom a₂ holds
product b₁ c= dom a₂ ) );

end;

:: deftheorem Def10 defines is_exactly_partitable_wrt PUA2MSS1:def 10 :

theorem Th24: :: PUA2MSS1:24

for b₁ being partial non-empty UAStr
for b₂ being operation of b₁ holds b₂ is_exactly_partitable_wrt SmallestPartition the carrier of b₁

proof end;

scheme :: PUA2MSS1:sch 4
s4{ F₁() -> FinSequence, F₂() -> FinSequence, P₁[ set ], P₂[ set , set ] } :

P₁[F₂()]

provided

E31: P₁[F₁()] and
E32: len F₁() = len F₂() and
E33: for b₁, b₂ being FinSequence
for b₃, b₄ being set st P₁[(b₁ ^ <*b₃*>) ^ b₂] & P₂[b₃,b₄] holds
P₁[(b₁ ^ <*b₄*>) ^ b₂] and
E34: for b₁ being Nat st b₁ in dom F₁() holds
P₂[F₁() . b₁,F₂() . b₁]

proof end;

theorem Th25: :: PUA2MSS1:25

for b₁ being partial non-empty UAStr
for b₂ being operation of b₁ holds b₂ is_exactly_partitable_wrt Class (LimDomRel b₁)

proof end;

definition

let c₁ be partial non-empty UAStr ;
mode a_partition of c₁ -> a_partition of the carrier of a₁ means :Def11: :: PUA2MSS1:def 11
for b₁ being operation of a₁ holds b₁ is_exactly_partitable_wrt a₂;
existence

proof end;

end;

:: deftheorem Def11 defines a_partition PUA2MSS1:def 11 :

definition

let c₁ be partial non-empty UAStr ;
mode IndexedPartition of c₁ -> IndexedPartition of the carrier of a₁ means :Def12: :: PUA2MSS1:def 12
rng a₂ is a_partition of a₁;
existence

proof end;

end;

:: deftheorem Def12 defines IndexedPartition PUA2MSS1:def 12 :

definition

let c₁ be partial non-empty UAStr ;
let c₂ be IndexedPartition of c₁;
redefine func rng as rng c₂ -> a_partition of a₁;
coherence by Def12;

end;

theorem Th26: :: PUA2MSS1:26

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

proof end;

theorem Th27: :: PUA2MSS1:27

for b₁ being non empty set
for b₂ being a_partition of b₁
for b₃ being FinSequence of b₂
for b₄, b₅ being FinSequence
for b₆, b₇ being set st (b₄ ^ <*b₆*>) ^ b₅ in product b₃ & ex b₈ being Element of b₂ st
( b₆ in b₈ & b₇ in b₈ ) holds
(b₄ ^ <*b₇*>) ^ b₅ in product b₃

proof end;

theorem Th28: :: PUA2MSS1:28

for b₁ being partial non-empty UAStr
for b₂ being a_partition of b₁ holds b₂ is_finer_than Class (LimDomRel b₁)

proof end;

definition

let c₁, c₂ be ManySortedSign ;
let c₃, c₄ be Function;
pred c₃,c₄ form_morphism_between c₁,c₂ means :Def13: :: PUA2MSS1:def 13
( dom a₃ = the carrier of a₁ & dom a₄ = the OperSymbols of a₁ & rng a₃ c= the carrier of a₂ & rng a₄ c= the OperSymbols of a₂ & a₃ * the ResultSort of a₁ = the ResultSort of a₂ * a₄ & ( for b₁ being set
for b₂ being Function st b₁ in the OperSymbols of a₁ & b₂ = the Arity of a₁ . b₁ holds
a₃ * b₂ = the Arity of a₂ . (a₄ . b₁) ) );

end;

:: deftheorem Def13 defines form_morphism_between PUA2MSS1:def 13 :

theorem Th29: :: PUA2MSS1:29

for b₁ being non empty non void ManySortedSign holds id the carrier of b₁, id the OperSymbols of b₁ form_morphism_between b₁,b₁

proof end;

theorem Th30: :: PUA2MSS1:30

for b₁, b₂, b₃ being ManySortedSign
for b₄, b₅, b₆, b₇ being Function st b₄,b₆ form_morphism_between b₁,b₂ & b₅,b₇ form_morphism_between b₂,b₃ holds
b₅ * b₄,b₇ * b₆ form_morphism_between b₁,b₃

proof end;

definition

let c₁, c₂ be ManySortedSign ;
pred c₁ is_rougher_than c₂ means :: PUA2MSS1:def 14
ex b₁, b₂ being Function st
( b₁,b₂ form_morphism_between a₂,a₁ & rng b₁ = the carrier of a₁ & rng b₂ = the OperSymbols of a₁ );

end;

:: deftheorem Def14 defines is_rougher_than PUA2MSS1:def 14 :

definition

let c₁, c₂ be non empty non void ManySortedSign ;
redefine pred is_rougher_than as c₁ is_rougher_than c₂;
reflexivity

proof end;

end;

theorem Th31: :: PUA2MSS1:31

for b₁, b₂, b₃ being ManySortedSign st b₁ is_rougher_than b₂ & b₂ is_rougher_than b₃ holds
b₁ is_rougher_than b₃

proof end;

definition

let c₁ be partial non-empty UAStr ;
let c₂ be a_partition of c₁;
func MSSign c₁,c₂ -> strict ManySortedSign means :Def15: :: PUA2MSS1:def 15
( the carrier of a₃ = a₂ & the OperSymbols of a₃ = { [b₁,b₂] where B is OperSymbol of a₁, B is Element of a₂ * : product b₂ meets dom (Den b₁,a₁) } & ( for b₁ being OperSymbol of a₁
for b₂ being Element of a₂ * st product b₂ meets dom (Den b₁,a₁) holds
( the Arity of a₃ . [b₁,b₂] = b₂ & (Den b₁,a₁) .: (product b₂) c= the ResultSort of a₃ . [b₁,b₂] ) ) );
existence

proof end;

correctness

proof end;

end;

:: deftheorem Def15 defines MSSign PUA2MSS1:def 15 :

registration

let c₁ be partial non-empty UAStr ;
let c₂ be a_partition of c₁;
cluster MSSign a₁,a₂ -> non empty strict non void ;
coherence

proof end;

end;

definition

let c₁ be partial non-empty UAStr ;
let c₂ be a_partition of c₁;
let c₃ be OperSymbol of (MSSign c₁,c₂);
redefine func `1 as c₃ `1 -> OperSymbol of a₁;
coherence

proof end;

redefine func `2 as c₃ `2 -> Element of a₂ * ;
coherence

proof end;

end;

definition

let c₁ be partial non-empty UAStr ;
let c₂ be non empty non void ManySortedSign ;
let c₃ be MSAlgebra of c₂;
let c₄ be IndexedPartition of the OperSymbols of c₂;
pred c₁ can_be_characterized_by c₂,c₃,c₄ means :Def16: :: PUA2MSS1:def 16
( the Sorts of a₃ is IndexedPartition of a₁ & dom a₄ = dom the charact of a₁ & ( for b₁ being OperSymbol of a₁ holds the Charact of a₃ | (a₄ . b₁) is IndexedPartition of Den b₁,a₁ ) );

end;

:: deftheorem Def16 defines can_be_characterized_by PUA2MSS1:def 16 :

definition

let c₁ be partial non-empty UAStr ;
let c₂ be non empty non void ManySortedSign ;
pred c₁ can_be_characterized_by c₂ means :: PUA2MSS1:def 17
ex b₁ being MSAlgebra of a₂ex b₂ being IndexedPartition of the OperSymbols of a₂ st a₁ can_be_characterized_by a₂,b₁,b₂;

end;

:: deftheorem Def17 defines can_be_characterized_by PUA2MSS1:def 17 :

theorem Th32: :: PUA2MSS1:32

for b₁ being partial non-empty UAStr
for b₂ being a_partition of b₁ holds b₁ can_be_characterized_by MSSign b₁,b₂

proof end;

theorem Th33: :: PUA2MSS1:33

for b₁ being partial non-empty UAStr
for b₂ being non empty non void ManySortedSign
for b₃ being MSAlgebra of b₂
for b₄ being IndexedPartition of the OperSymbols of b₂ st b₁ can_be_characterized_by b₂,b₃,b₄ holds
for b₅ being OperSymbol of b₁
for b₆ being FinSequence of rng the Sorts of b₃ st product b₆ c= dom (Den b₅,b₁) holds
ex b₇ being OperSymbol of b₂ st
( the Sorts of b₃ * (the_arity_of b₇) = b₆ & b₇ in b₄ . b₅ )

proof end;

theorem Th34: :: PUA2MSS1:34

for b₁ being partial non-empty UAStr
for b₂ being a_partition of b₁ st b₂ = Class (LimDomRel b₁) holds
for b₃ being non empty non void ManySortedSign st b₁ can_be_characterized_by b₃ holds
MSSign b₁,b₂ is_rougher_than b₃

proof end;