:: MSUALG_6 semantic presentation

definition

let c₁ be non empty ManySortedSign ;
let c₂ be MSAlgebra of c₁;
let c₃ be SortSymbol of c₁;
mode Element of a₂,a₃ is Element of the Sorts of a₂ . a₃;

end;

definition

let c₁ be set ;
let c₂ be ManySortedSet of c₁;
let c₃, c₄ be ManySortedFunction of c₂,c₂;
redefine func ** as c₄ ** c₃ -> ManySortedFunction of a₂,a₂;
coherence

proof end;

end;

theorem Th1: :: MSUALG_6:1

for b₁ being non empty non void ManySortedSign
for b₂ being MSAlgebra of b₁
for b₃ being OperSymbol of b₁
for b₄ being set st b₄ in Args b₃,b₂ holds
b₄ is Function

proof end;

theorem Th2: :: MSUALG_6:2

for b₁ being non empty non void ManySortedSign
for b₂ being MSAlgebra of b₁
for b₃ being OperSymbol of b₁
for b₄ being Function st b₄ in Args b₃,b₂ holds
( dom b₄ = dom (the_arity_of b₃) & ( for b₅ being set st b₅ in dom (the_arity_of b₃) holds
b₄ . b₅ in the Sorts of b₂ . ((the_arity_of b₃) /. b₅) ) )

proof end;

definition

let c₁ be non empty non void ManySortedSign ;
let c₂ be MSAlgebra of c₁;
attr a₂ is feasible means :Def1: :: MSUALG_6:def 1
for b₁ being OperSymbol of a₁ st Args b₁,a₂ <> {} holds
Result b₁,a₂ <> {} ;

end;

:: deftheorem Def1 defines feasible MSUALG_6:def 1 :

theorem Th3: :: MSUALG_6:3

for b₁ being non empty non void ManySortedSign
for b₂ being OperSymbol of b₁
for b₃ being MSAlgebra of b₁ holds
( Args b₂,b₃ <> {} iff for b₄ being Nat st b₄ in dom (the_arity_of b₂) holds
the Sorts of b₃ . ((the_arity_of b₂) /. b₄) <> {} )

proof end;

registration

let c₁ be non empty non void ManySortedSign ;
cluster non-empty -> feasible MSAlgebra of a₁;
coherence

proof end;

end;

registration

let c₁ be non empty non void ManySortedSign ;
cluster non-empty feasible MSAlgebra of a₁;
existence

proof end;

end;

definition

let c₁ be non empty non void ManySortedSign ;
let c₂ be MSAlgebra of c₁;
mode Endomorphism of c₂ -> ManySortedFunction of a₂,a₂ means :Def2: :: MSUALG_6:def 2
a₃ is_homomorphism a₂,a₂;
existence

proof end;

end;

:: deftheorem Def2 defines Endomorphism MSUALG_6:def 2 :

theorem Th4: :: MSUALG_6:4

for b₁ being non empty non void ManySortedSign
for b₂ being MSAlgebra of b₁ holds id the Sorts of b₂ is Endomorphism of b₂

proof end;

theorem Th5: :: MSUALG_6:5

for b₁ being non empty non void ManySortedSign
for b₂ being MSAlgebra of b₁
for b₃, b₄ being ManySortedFunction of b₂,b₂
for b₅ being OperSymbol of b₁
for b₆ being Element of Args b₅,b₂ st b₆ in Args b₅,b₂ holds
b₄ # (b₃ # b₆) = (b₄ ** b₃) # b₆

proof end;

theorem Th6: :: MSUALG_6:6

for b₁ being non empty non void ManySortedSign
for b₂ being MSAlgebra of b₁
for b₃, b₄ being Endomorphism of b₂ holds b₄ ** b₃ is Endomorphism of b₂

proof end;

definition

let c₁ be non empty non void ManySortedSign ;
let c₂ be MSAlgebra of c₁;
let c₃, c₄ be Endomorphism of c₂;
redefine func ** as c₄ ** c₃ -> Endomorphism of a₂;
coherence by Th6;

end;

definition

let c₁ be non empty non void ManySortedSign ;
func TranslationRel c₁ -> Relation of the carrier of a₁ means :Def3: :: MSUALG_6:def 3
for b₁, b₂ being SortSymbol of a₁ holds
( [b₁,b₂] in a₂ iff ex b₃ being OperSymbol of a₁ st
( the_result_sort_of b₃ = b₂ & ex b₄ being Nat st
( b₄ in dom (the_arity_of b₃) & (the_arity_of b₃) /. b₄ = b₁ ) ) );
existence

proof end;

correctness

proof end;

end;

:: deftheorem Def3 defines TranslationRel MSUALG_6:def 3 :

theorem Th7: :: MSUALG_6:7

for b₁ being non empty non void ManySortedSign
for b₂ being OperSymbol of b₁
for b₃ being MSAlgebra of b₁
for b₄ being Function st b₄ in Args b₂,b₃ holds
for b₅ being Nat
for b₆ being Element of b₃,((the_arity_of b₂) /. b₅) holds b₄ +* b₅,b₆ in Args b₂,b₃

proof end;

theorem Th8: :: MSUALG_6:8

for b₁ being non empty non void ManySortedSign
for b₂, b₃ being MSAlgebra of b₁
for b₄ being ManySortedFunction of b₂,b₃
for b₅ being OperSymbol of b₁ st Args b₅,b₂ <> {} & Args b₅,b₃ <> {} holds
for b₆ being Nat st b₆ in dom (the_arity_of b₅) holds
for b₇ being Element of b₂,((the_arity_of b₅) /. b₆) holds (b₄ . ((the_arity_of b₅) /. b₆)) . b₇ in the Sorts of b₃ . ((the_arity_of b₅) /. b₆)

proof end;

theorem Th9: :: MSUALG_6:9

for b₁ being non empty non void ManySortedSign
for b₂ being OperSymbol of b₁
for b₃ being Nat st b₃ in dom (the_arity_of b₂) holds
for b₄, b₅ being MSAlgebra of b₁
for b₆ being ManySortedFunction of b₄,b₅
for b₇, b₈ being Element of Args b₂,b₄ st b₇ in Args b₂,b₄ & b₆ # b₇ in Args b₂,b₅ holds
for b₉, b₁₀, b₁₁ being Function st b₉ = b₇ & b₁₀ = b₆ # b₇ & b₁₁ = b₆ # b₈ holds
for b₁₂ being Element of b₄,((the_arity_of b₂) /. b₃) st b₈ = b₉ +* b₃,b₁₂ holds
( b₁₁ . b₃ = (b₆ . ((the_arity_of b₂) /. b₃)) . b₁₂ & b₆ # b₈ = b₁₀ +* b₃,(b₁₁ . b₃) )

proof end;

definition

let c₁ be non empty non void ManySortedSign ;
let c₂ be OperSymbol of c₁;
let c₃ be Nat;
let c₄ be MSAlgebra of c₁;
let c₅ be Function;
func transl c₂,c₃,c₅,c₄ -> Function means :Def4: :: MSUALG_6:def 4
( dom a₆ = the Sorts of a₄ . ((the_arity_of a₂) /. a₃) & ( for b₁ being set st b₁ in the Sorts of a₄ . ((the_arity_of a₂) /. a₃) holds
a₆ . b₁ = (Den a₂,a₄) . (a₅ +* a₃,b₁) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def4 defines transl MSUALG_6:def 4 :

theorem Th10: :: MSUALG_6:10

for b₁ being non empty non void ManySortedSign
for b₂ being OperSymbol of b₁
for b₃ being Nat st b₃ in dom (the_arity_of b₂) holds
for b₄ being feasible MSAlgebra of b₁
for b₅ being Function st b₅ in Args b₂,b₄ holds
transl b₂,b₃,b₅,b₄ is Function of the Sorts of b₄ . ((the_arity_of b₂) /. b₃),the Sorts of b₄ . (the_result_sort_of b₂)

proof end;

definition

let c₁ be non empty non void ManySortedSign ;
let c₂, c₃ be SortSymbol of c₁;
let c₄ be MSAlgebra of c₁;
let c₅ be Function;
pred c₅ is_e.translation_of c₄,c₂,c₃ means :Def5: :: MSUALG_6:def 5
ex b₁ being OperSymbol of a₁ st
( the_result_sort_of b₁ = a₃ & ex b₂ being Nat st
( b₂ in dom (the_arity_of b₁) & (the_arity_of b₁) /. b₂ = a₂ & ex b₃ being Function st
( b₃ in Args b₁,a₄ & a₅ = transl b₁,b₂,b₃,a₄ ) ) );

end;

:: deftheorem Def5 defines is_e.translation_of MSUALG_6:def 5 :

theorem Th11: :: MSUALG_6:11

for b₁ being non empty non void ManySortedSign
for b₂, b₃ being SortSymbol of b₁
for b₄ being feasible MSAlgebra of b₁
for b₅ being Function st b₅ is_e.translation_of b₄,b₂,b₃ holds
( b₅ is Function of the Sorts of b₄ . b₂,the Sorts of b₄ . b₃ & the Sorts of b₄ . b₂ <> {} & the Sorts of b₄ . b₃ <> {} )

proof end;

theorem Th12: :: MSUALG_6:12

for b₁ being non empty non void ManySortedSign
for b₂, b₃ being SortSymbol of b₁
for b₄ being MSAlgebra of b₁
for b₅ being Function st b₅ is_e.translation_of b₄,b₂,b₃ holds
[b₂,b₃] in TranslationRel b₁

proof end;

theorem Th13: :: MSUALG_6:13

for b₁ being non empty non void ManySortedSign
for b₂, b₃ being SortSymbol of b₁
for b₄ being non-empty MSAlgebra of b₁ st [b₂,b₃] in TranslationRel b₁ holds
ex b₅ being Function st b₅ is_e.translation_of b₄,b₂,b₃

proof end;

theorem Th14: :: MSUALG_6:14

for b₁ being non empty non void ManySortedSign
for b₂ being feasible MSAlgebra of b₁
for b₃, b₄ being SortSymbol of b₁ st TranslationRel b₁ reduces b₃,b₄ holds
for b₅ being RedSequence of TranslationRel b₁
for b₆ being Function-yielding FinSequence st len b₅ = (len b₆) + 1 & b₃ = b₅ . 1 & b₄ = b₅ . (len b₅) & ( for b₇ being Nat
for b₈ being Function
for b₉, b₁₀ being SortSymbol of b₁ st b₇ in dom b₆ & b₈ = b₆ . b₇ & b₉ = b₅ . b₇ & b₁₀ = b₅ . (b₇ + 1) holds
b₈ is_e.translation_of b₂,b₉,b₁₀ ) holds
( compose b₆,(the Sorts of b₂ . b₃) is Function of the Sorts of b₂ . b₃,the Sorts of b₂ . b₄ & ( b₆ <> {} implies ( the Sorts of b₂ . b₃ <> {} & the Sorts of b₂ . b₄ <> {} ) ) )

proof end;

definition

let c₁ be non empty non void ManySortedSign ;
let c₂ be non-empty MSAlgebra of c₁;
let c₃, c₄ be SortSymbol of c₁;
assume E19: TranslationRel c₁ reduces c₃,c₄ ;
mode Translation of c₂,c₃,c₄ -> Function of the Sorts of a₂ . a₃,the Sorts of a₂ . a₄ means :Def6: :: MSUALG_6:def 6
ex b₁ being RedSequence of TranslationRel a₁ex b₂ being Function-yielding FinSequence st
( a₅ = compose b₂,(the Sorts of a₂ . a₃) & len b₁ = (len b₂) + 1 & a₃ = b₁ . 1 & a₄ = b₁ . (len b₁) & ( for b₃ being Nat
for b₄ being Function
for b₅, b₆ being SortSymbol of a₁ st b₃ in dom b₂ & b₄ = b₂ . b₃ & b₅ = b₁ . b₃ & b₆ = b₁ . (b₃ + 1) holds
b₄ is_e.translation_of a₂,b₅,b₆ ) );
existence

proof end;

end;

:: deftheorem Def6 defines Translation MSUALG_6:def 6 :

theorem Th15: :: MSUALG_6:15

for b₁ being non empty non void ManySortedSign
for b₂ being non-empty MSAlgebra of b₁
for b₃, b₄ being SortSymbol of b₁ st TranslationRel b₁ reduces b₃,b₄ holds
for b₅ being RedSequence of TranslationRel b₁
for b₆ being Function-yielding FinSequence st len b₅ = (len b₆) + 1 & b₃ = b₅ . 1 & b₄ = b₅ . (len b₅) & ( for b₇ being Nat
for b₈ being Function
for b₉, b₁₀ being SortSymbol of b₁ st b₇ in dom b₆ & b₈ = b₆ . b₇ & b₉ = b₅ . b₇ & b₁₀ = b₅ . (b₇ + 1) holds
b₈ is_e.translation_of b₂,b₉,b₁₀ ) holds
compose b₆,(the Sorts of b₂ . b₃) is Translation of b₂,b₃,b₄

proof end;

theorem Th16: :: MSUALG_6:16

for b₁ being non empty non void ManySortedSign
for b₂ being non-empty MSAlgebra of b₁
for b₃ being SortSymbol of b₁ holds id (the Sorts of b₂ . b₃) is Translation of b₂,b₃,b₃

proof end;

theorem Th17: :: MSUALG_6:17

for b₁ being non empty non void ManySortedSign
for b₂ being non-empty MSAlgebra of b₁
for b₃, b₄ being SortSymbol of b₁
for b₅ being Function st b₅ is_e.translation_of b₂,b₃,b₄ holds
( TranslationRel b₁ reduces b₃,b₄ & b₅ is Translation of b₂,b₃,b₄ )

proof end;

theorem Th18: :: MSUALG_6:18

for b₁ being non empty non void ManySortedSign
for b₂ being non-empty MSAlgebra of b₁
for b₃, b₄, b₅ being SortSymbol of b₁ st TranslationRel b₁ reduces b₃,b₄ & TranslationRel b₁ reduces b₄,b₅ holds
for b₆ being Translation of b₂,b₃,b₄
for b₇ being Translation of b₂,b₄,b₅ holds b₇ * b₆ is Translation of b₂,b₃,b₅

proof end;

theorem Th19: :: MSUALG_6:19

for b₁ being non empty non void ManySortedSign
for b₂ being non-empty MSAlgebra of b₁
for b₃, b₄, b₅ being SortSymbol of b₁ st TranslationRel b₁ reduces b₃,b₄ holds
for b₆ being Translation of b₂,b₃,b₄
for b₇ being Function st b₇ is_e.translation_of b₂,b₄,b₅ holds
b₇ * b₆ is Translation of b₂,b₃,b₅

proof end;

theorem Th20: :: MSUALG_6:20

for b₁ being non empty non void ManySortedSign
for b₂ being non-empty MSAlgebra of b₁
for b₃, b₄, b₅ being SortSymbol of b₁ st TranslationRel b₁ reduces b₄,b₅ holds
for b₆ being Function st b₆ is_e.translation_of b₂,b₃,b₄ holds
for b₇ being Translation of b₂,b₄,b₅ holds b₇ * b₆ is Translation of b₂,b₃,b₅

proof end;

scheme :: MSUALG_6:sch 1
s1{ F₁() -> non empty non void ManySortedSign , F₂() -> non-empty MSAlgebra of F₁(), P₁[ set , set , set ] } :

for b₁, b₂ being SortSymbol of F₁() st TranslationRel F₁() reduces b₁,b₂ holds
for b₃ being Translation of F₂(),b₁,b₂ holds P₁[b₃,b₁,b₂]

provided

E24: for b₁ being SortSymbol of F₁() holds P₁[ id (the Sorts of F₂() . b₁),b₁,b₁] and
E25: for b₁, b₂, b₃ being SortSymbol of F₁() st TranslationRel F₁() reduces b₁,b₂ holds
for b₄ being Translation of F₂(),b₁,b₂ st P₁[b₄,b₁,b₂] holds
for b₅ being Function st b₅ is_e.translation_of F₂(),b₂,b₃ holds
P₁[b₅ * b₄,b₁,b₃]

proof end;

theorem Th21: :: MSUALG_6:21

for b₁ being non empty non void ManySortedSign
for b₂, b₃ being non-empty MSAlgebra of b₁
for b₄ being ManySortedFunction of b₂,b₃ st b₄ is_homomorphism b₂,b₃ holds
for b₅ being OperSymbol of b₁
for b₆ being Nat st b₆ in dom (the_arity_of b₅) holds
for b₇ being Element of Args b₅,b₂ holds (b₄ . (the_result_sort_of b₅)) * (transl b₅,b₆,b₇,b₂) = (transl b₅,b₆,(b₄ # b₇),b₃) * (b₄ . ((the_arity_of b₅) /. b₆))

proof end;

theorem Th22: :: MSUALG_6:22

for b₁ being non empty non void ManySortedSign
for b₂ being non-empty MSAlgebra of b₁
for b₃ being Endomorphism of b₂
for b₄ being OperSymbol of b₁
for b₅ being Nat st b₅ in dom (the_arity_of b₄) holds
for b₆ being Element of Args b₄,b₂ holds (b₃ . (the_result_sort_of b₄)) * (transl b₄,b₅,b₆,b₂) = (transl b₄,b₅,(b₃ # b₆),b₂) * (b₃ . ((the_arity_of b₄) /. b₅))

proof end;

theorem Th23: :: MSUALG_6:23

for b₁ being non empty non void ManySortedSign
for b₂, b₃ being non-empty MSAlgebra of b₁
for b₄ being ManySortedFunction of b₂,b₃ st b₄ is_homomorphism b₂,b₃ holds
for b₅, b₆ being SortSymbol of b₁
for b₇ being Function st b₇ is_e.translation_of b₂,b₅,b₆ holds
ex b₈ being Function of the Sorts of b₃ . b₅,the Sorts of b₃ . b₆ st
( b₈ is_e.translation_of b₃,b₅,b₆ & b₈ * (b₄ . b₅) = (b₄ . b₆) * b₇ )

proof end;

theorem Th24: :: MSUALG_6:24

for b₁ being non empty non void ManySortedSign
for b₂ being non-empty MSAlgebra of b₁
for b₃ being Endomorphism of b₂
for b₄, b₅ being SortSymbol of b₁
for b₆ being Function st b₆ is_e.translation_of b₂,b₄,b₅ holds
ex b₇ being Function of the Sorts of b₂ . b₄,the Sorts of b₂ . b₅ st
( b₇ is_e.translation_of b₂,b₄,b₅ & b₇ * (b₃ . b₄) = (b₃ . b₅) * b₆ )

proof end;

theorem Th25: :: MSUALG_6:25

for b₁ being non empty non void ManySortedSign
for b₂, b₃ being non-empty MSAlgebra of b₁
for b₄ being ManySortedFunction of b₂,b₃ st b₄ is_homomorphism b₂,b₃ holds
for b₅, b₆ being SortSymbol of b₁ st TranslationRel b₁ reduces b₅,b₆ holds
for b₇ being Translation of b₂,b₅,b₆ ex b₈ being Translation of b₃,b₅,b₆ st b₈ * (b₄ . b₅) = (b₄ . b₆) * b₇

proof end;

theorem Th26: :: MSUALG_6:26

for b₁ being non empty non void ManySortedSign
for b₂ being non-empty MSAlgebra of b₁
for b₃ being Endomorphism of b₂
for b₄, b₅ being SortSymbol of b₁ st TranslationRel b₁ reduces b₄,b₅ holds
for b₆ being Translation of b₂,b₄,b₅ ex b₇ being Translation of b₂,b₄,b₅ st b₇ * (b₃ . b₄) = (b₃ . b₅) * b₆

proof end;

definition

let c₁ be non empty non void ManySortedSign ;
let c₂ be MSAlgebra of c₁;
let c₃ be ManySortedRelation of c₂;
attr a₃ is compatible means :Def7: :: MSUALG_6:def 7
for b₁ being OperSymbol of a₁
for b₂, b₃ being Function st b₂ in Args b₁,a₂ & b₃ in Args b₁,a₂ & ( for b₄ being Nat st b₄ in dom (the_arity_of b₁) holds
[(b₂ . b₄),(b₃ . b₄)] in a₃ . ((the_arity_of b₁) /. b₄) ) holds
[((Den b₁,a₂) . b₂),((Den b₁,a₂) . b₃)] in a₃ . (the_result_sort_of b₁);
attr a₃ is invariant means :Def8: :: MSUALG_6:def 8
for b₁, b₂ being SortSymbol of a₁
for b₃ being Function st b₃ is_e.translation_of a₂,b₁,b₂ holds
for b₄, b₅ being set st [b₄,b₅] in a₃ . b₁ holds
[(b₃ . b₄),(b₃ . b₅)] in a₃ . b₂;
attr a₃ is stable means :Def9: :: MSUALG_6:def 9
for b₁ being Endomorphism of a₂
for b₂ being SortSymbol of a₁
for b₃, b₄ being set st [b₃,b₄] in a₃ . b₂ holds
[((b₁ . b₂) . b₃),((b₁ . b₂) . b₄)] in a₃ . b₂;

end;

:: deftheorem Def7 defines compatible MSUALG_6:def 7 :

:: deftheorem Def8 defines invariant MSUALG_6:def 8 :

:: deftheorem Def9 defines stable MSUALG_6:def 9 :

theorem Th27: :: MSUALG_6:27

for b₁ being non empty non void ManySortedSign
for b₂ being non-empty MSAlgebra of b₁
for b₃ being MSEquivalence-like ManySortedRelation of b₂ holds
( b₃ is compatible iff b₃ is MSCongruence of b₂ )

proof end;

theorem Th28: :: MSUALG_6:28

for b₁ being non empty non void ManySortedSign
for b₂ being non-empty MSAlgebra of b₁
for b₃ being ManySortedRelation of b₂ holds
( b₃ is invariant iff for b₄, b₅ being SortSymbol of b₁ st TranslationRel b₁ reduces b₄,b₅ holds
for b₆ being Translation of b₂,b₄,b₅
for b₇, b₈ being set st [b₇,b₈] in b₃ . b₄ holds
[(b₆ . b₇),(b₆ . b₈)] in b₃ . b₅ )

proof end;

registration

let c₁ be non empty non void ManySortedSign ;
let c₂ be non-empty MSAlgebra of c₁;
cluster MSEquivalence-like invariant -> MSEquivalence-like compatible ManySortedRelation of the Sorts of a₂,the Sorts of a₂;
coherence

proof end;

cluster MSEquivalence-like compatible -> MSEquivalence-like invariant ManySortedRelation of the Sorts of a₂,the Sorts of a₂;
coherence

proof end;

end;

registration

let c₁ be non empty set ;
cluster id a₁ -> non empty ;
coherence ;

end;

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

ex b₁ being ManySortedRelation of F₂() st
for b₂ being Element of F₁()
for b₃, b₄ being Element of F₂() . b₂ holds
( [b₃,b₄] in b₁ . b₂ iff P₁[b₂,b₃,b₄] )

proof end;

scheme :: MSUALG_6:sch 3
s3{ F₁() -> set , F₂() -> ManySortedSet of F₁(), F₃( set ) -> set } :

( ex b₁ being ManySortedRelation of F₂() st
for b₂ being set st b₂ in F₁() holds
b₁ . b₂ = F₃(b₂) & ( for b₁, b₂ being ManySortedRelation of F₂() st ( for b₃ being set st b₃ in F₁() holds
b₁ . b₃ = F₃(b₃) ) & ( for b₃ being set st b₃ in F₁() holds
b₂ . b₃ = F₃(b₃) ) holds
b₁ = b₂ ) )

provided

E32: for b₁ being set st b₁ in F₁() holds
F₃(b₁) is Relation of F₂() . b₁,F₂() . b₁

proof end;

definition

let c₁ be set ;
let c₂ be ManySortedSet of c₁;
func id c₁,c₂ -> ManySortedRelation of a₂ means :Def10: :: MSUALG_6:def 10
for b₁ being set st b₁ in a₁ holds
a₃ . b₁ = id (a₂ . b₁);
correctness

proof end;

end;

:: deftheorem Def10 defines id MSUALG_6:def 10 :

registration

let c₁ be non empty non void ManySortedSign ;
let c₂ be non-empty MSAlgebra of c₁;
cluster MSEquivalence-like -> V3 ManySortedRelation of the Sorts of a₂,the Sorts of a₂;
coherence

proof end;

end;

registration

let c₁ be non empty non void ManySortedSign ;
let c₂ be non-empty MSAlgebra of c₁;
cluster V3 MSEquivalence-like compatible invariant stable ManySortedRelation of the Sorts of a₂,the Sorts of a₂;
existence

proof end;

end;

scheme :: MSUALG_6:sch 4
s4{ F₁() -> non empty non void ManySortedSign , F₂() -> non-empty MSAlgebra of F₁(), P₁[ set , set , set ], P₂[ set ], F₃() -> ManySortedRelation of F₂(), F₄() -> ManySortedRelation of F₂() } :

( P₂[F₄()] & F₃() c= F₄() & ( for b₁ being ManySortedRelation of F₂() st P₂[b₁] & F₃() c= b₁ holds
F₄() c= b₁ ) )

provided

E33: for b₁ being ManySortedRelation of F₂() holds
( P₂[b₁] iff for b₂, b₃ being SortSymbol of F₁()
for b₄ being Function of the Sorts of F₂() . b₂,the Sorts of F₂() . b₃ st P₁[b₄,b₂,b₃] holds
for b₅, b₆ being set st [b₅,b₆] in b₁ . b₂ holds
[(b₄ . b₅),(b₄ . b₆)] in b₁ . b₃ ) and
E34: for b₁, b₂, b₃ being SortSymbol of F₁()
for b₄ being Function of the Sorts of F₂() . b₁,the Sorts of F₂() . b₂
for b₅ being Function of the Sorts of F₂() . b₂,the Sorts of F₂() . b₃ st P₁[b₄,b₁,b₂] & P₁[b₅,b₂,b₃] holds
P₁[b₅ * b₄,b₁,b₃] and
E35: for b₁ being SortSymbol of F₁() holds P₁[ id (the Sorts of F₂() . b₁),b₁,b₁] and
E36: for b₁ being SortSymbol of F₁()
for b₂, b₃ being Element of F₂(),b₁ holds
( [b₂,b₃] in F₄() . b₁ iff ex b₄ being SortSymbol of F₁()ex b₅ being Function of the Sorts of F₂() . b₄,the Sorts of F₂() . b₁ex b₆, b₇ being Element of F₂(),b₄ st
( P₁[b₅,b₄,b₁] & [b₆,b₇] in F₃() . b₄ & b₂ = b₅ . b₆ & b₃ = b₅ . b₇ ) )

proof end;

E33: now

let c₁ be non empty non void ManySortedSign ;
let c₂ be non-empty MSAlgebra of c₁;
let c₃, c₄ be ManySortedRelation of c₂;
defpred S₁[ ManySortedRelation of c₂] means a₁ is invariant;
defpred S₂[ Function, SortSymbol of c₁, SortSymbol of c₁] means ( TranslationRel c₁ reduces a₂,a₃ & a₁ is Translation of c₂,a₂,a₃ );
assume E34: for b₁ being SortSymbol of c₁
for b₂, b₃ being Element of c₂,b₁ holds
( [b₂,b₃] in c₄ . b₁ iff ex b₄ being SortSymbol of c₁ex b₅ being Function of the Sorts of c₂ . b₄,the Sorts of c₂ . b₁ex b₆, b₇ being Element of c₂,b₄ st
( S₂[b₅,b₄,b₁] & [b₆,b₇] in c₃ . b₄ & b₂ = b₅ . b₆ & b₃ = b₅ . b₇ ) ) ;

E35: now

let c₅ be ManySortedRelation of c₂;
thus ( S₁[c₅] implies for b₁, b₂ being SortSymbol of c₁
for b₃ being Function of the Sorts of c₂ . b₁,the Sorts of c₂ . b₂ st S₂[b₃,b₁,b₂] holds
for b₄, b₅ being set st [b₄,b₅] in c₅ . b₁ holds
[(b₃ . b₄),(b₃ . b₅)] in c₅ . b₂ ) by Th28;
assume for b₁, b₂ being SortSymbol of c₁
for b₃ being Function of the Sorts of c₂ . b₁,the Sorts of c₂ . b₂ st S₂[b₃,b₁,b₂] holds
for b₄, b₅ being set st [b₄,b₅] in c₅ . b₁ holds
[(b₃ . b₄),(b₃ . b₅)] in c₅ . b₂ ;
then for b₁, b₂ being SortSymbol of c₁ st TranslationRel c₁ reduces b₁,b₂ holds
for b₃ being Translation of c₂,b₁,b₂
for b₄, b₅ being set st [b₄,b₅] in c₅ . b₁ holds
[(b₃ . b₄),(b₃ . b₅)] in c₅ . b₂ ;
hence S₁[c₅] by Th28;

end;

E36: for b₁, b₂, b₃ being SortSymbol of c₁
for b₄ being Function of the Sorts of c₂ . b₁,the Sorts of c₂ . b₂
for b₅ being Function of the Sorts of c₂ . b₂,the Sorts of c₂ . b₃ st S₂[b₄,b₁,b₂] & S₂[b₅,b₂,b₃] holds
S₂[b₅ * b₄,b₁,b₃] by Th18, REWRITE1:17;
E37: for b₁ being SortSymbol of c₁ holds S₂[ id (the Sorts of c₂ . b₁),b₁,b₁] by Th16, REWRITE1:13;
thus ( S₁[c₄] & c₃ c= c₄ & ( for b₁ being ManySortedRelation of c₂ st S₁[b₁] & c₃ c= b₁ holds
c₄ c= b₁ ) ) from MSUALG_6:sch 4(E35, E36, E37, E34);

end;

definition

let c₁ be non empty non void ManySortedSign ;
let c₂ be non-empty MSAlgebra of c₁;
let c₃ be ManySortedRelation of the Sorts of c₂;
func InvCl c₃ -> invariant ManySortedRelation of a₂ means :Def11: :: MSUALG_6:def 11
( a₃ c= a₄ & ( for b₁ being invariant ManySortedRelation of a₂ st a₃ c= b₁ holds
a₄ c= b₁ ) );
uniqueness

proof end;

existence

proof end;

end;

:: deftheorem Def11 defines InvCl MSUALG_6:def 11 :

theorem Th29: :: MSUALG_6:29

for b₁ being non empty non void ManySortedSign
for b₂ being non-empty MSAlgebra of b₁
for b₃ being ManySortedRelation of the Sorts of b₂
for b₄ being SortSymbol of b₁
for b₅, b₆ being Element of b₂,b₄ holds
( [b₅,b₆] in (InvCl b₃) . b₄ iff ex b₇ being SortSymbol of b₁ex b₈, b₉ being Element of b₂,b₇ex b₁₀ being Translation of b₂,b₇,b₄ st
( TranslationRel b₁ reduces b₇,b₄ & [b₈,b₉] in b₃ . b₇ & b₅ = b₁₀ . b₈ & b₆ = b₁₀ . b₉ ) )

proof end;

theorem Th30: :: MSUALG_6:30

for b₁ being non empty non void ManySortedSign
for b₂ being non-empty MSAlgebra of b₁
for b₃ being stable ManySortedRelation of b₂ holds InvCl b₃ is stable

proof end;

E37: now

let c₁ be non empty non void ManySortedSign ;
let c₂ be non-empty MSAlgebra of c₁;
let c₃, c₄ be ManySortedRelation of c₂;
defpred S₁[ ManySortedRelation of c₂] means a₁ is stable;
defpred S₂[ Function, SortSymbol of c₁, SortSymbol of c₁] means ( a₂ = a₃ & ex b₁ being Endomorphism of c₂ st a₁ = b₁ . a₂ );
assume E38: for b₁ being SortSymbol of c₁
for b₂, b₃ being Element of c₂,b₁ holds
( [b₂,b₃] in c₄ . b₁ iff ex b₄ being SortSymbol of c₁ex b₅ being Function of the Sorts of c₂ . b₄,the Sorts of c₂ . b₁ex b₆, b₇ being Element of c₂,b₄ st
( S₂[b₅,b₄,b₁] & [b₆,b₇] in c₃ . b₄ & b₂ = b₅ . b₆ & b₃ = b₅ . b₇ ) ) ;
E39: for b₁ being ManySortedRelation of c₂ holds
( S₁[b₁] iff for b₂, b₃ being SortSymbol of c₁
for b₄ being Function of the Sorts of c₂ . b₂,the Sorts of c₂ . b₃ st S₂[b₄,b₂,b₃] holds
for b₅, b₆ being set st [b₅,b₆] in b₁ . b₂ holds
[(b₄ . b₅),(b₄ . b₆)] in b₁ . b₃ )

proof

let c₅ be ManySortedRelation of c₂;
thus ( c₅ is stable implies for b₁, b₂ being SortSymbol of c₁
for b₃ being Function of the Sorts of c₂ . b₁,the Sorts of c₂ . b₂ st b₁ = b₂ & ex b₄ being Endomorphism of c₂ st b₃ = b₄ . b₁ holds
for b₄, b₅ being set st [b₄,b₅] in c₅ . b₁ holds
[(b₃ . b₄),(b₃ . b₅)] in c₅ . b₂ ) by Def9;
assume E40: for b₁, b₂ being SortSymbol of c₁
for b₃ being Function of the Sorts of c₂ . b₁,the Sorts of c₂ . b₂ st S₂[b₃,b₁,b₂] holds
for b₄, b₅ being set st [b₄,b₅] in c₅ . b₁ holds
[(b₃ . b₄),(b₃ . b₅)] in c₅ . b₂ ;
thus c₅ is stable

proof

let c₆ be Endomorphism of c₂; :: according to MSUALG_6:def 9
let c₇ be SortSymbol of c₁;
thus for b₁, b₂ being set st [b₁,b₂] in c₅ . c₇ holds
[((c₆ . c₇) . b₁),((c₆ . c₇) . b₂)] in c₅ . c₇ by E40;

end;

E40: for b₁, b₂, b₃ being SortSymbol of c₁
for b₄ being Function of the Sorts of c₂ . b₁,the Sorts of c₂ . b₂
for b₅ being Function of the Sorts of c₂ . b₂,the Sorts of c₂ . b₃ st S₂[b₄,b₁,b₂] & S₂[b₅,b₂,b₃] holds
S₂[b₅ * b₄,b₁,b₃]

proof

let c₅, c₆, c₇ be SortSymbol of c₁;
let c₈ be Function of the Sorts of c₂ . c₅,the Sorts of c₂ . c₆;
let c₉ be Function of the Sorts of c₂ . c₆,the Sorts of c₂ . c₇;
assume E41: c₅ = c₆ ;
given c₁₀ being Endomorphism of c₂ such that E42: c₈ = c₁₀ . c₅ ;
assume E43: c₆ = c₇ ;
given c₁₁ being Endomorphism of c₂ such that E44: c₉ = c₁₁ . c₆ ;
thus c₅ = c₇ by E41, E43;
reconsider c₁₂ = c₁₁ ** c₁₀ as Endomorphism of c₂ ;
take c₁₂ ;
thus c₉ * c₈ = c₁₂ . c₅ by E41, E42, E44, MSUALG_3:2;

end;

E41: for b₁ being SortSymbol of c₁ holds S₂[ id (the Sorts of c₂ . b₁),b₁,b₁]

proof

let c₅ be SortSymbol of c₁;
thus c₅ = c₅ ;
reconsider c₆ = id the Sorts of c₂ as Endomorphism of c₂ by Th4;
take c₆ ;
thus id (the Sorts of c₂ . c₅) = c₆ . c₅ by MSUALG_3:def 1;

end;

thus ( S₁[c₄] & c₃ c= c₄ & ( for b₁ being ManySortedRelation of c₂ st S₁[b₁] & c₃ c= b₁ holds
c₄ c= b₁ ) ) from MSUALG_6:sch 4(E39, E40, E41, E38);

end;

definition

let c₁ be non empty non void ManySortedSign ;
let c₂ be non-empty MSAlgebra of c₁;
let c₃ be ManySortedRelation of the Sorts of c₂;
func StabCl c₃ -> stable ManySortedRelation of a₂ means :Def12: :: MSUALG_6:def 12
( a₃ c= a₄ & ( for b₁ being stable ManySortedRelation of a₂ st a₃ c= b₁ holds
a₄ c= b₁ ) );
uniqueness

proof end;

existence

proof end;

end;

:: deftheorem Def12 defines StabCl MSUALG_6:def 12 :

theorem Th31: :: MSUALG_6:31

for b₁ being non empty non void ManySortedSign
for b₂ being non-empty MSAlgebra of b₁
for b₃ being ManySortedRelation of the Sorts of b₂
for b₄ being SortSymbol of b₁
for b₅, b₆ being Element of b₂,b₄ holds
( [b₅,b₆] in (StabCl b₃) . b₄ iff ex b₇, b₈ being Element of b₂,b₄ex b₉ being Endomorphism of b₂ st
( [b₇,b₈] in b₃ . b₄ & b₅ = (b₉ . b₄) . b₇ & b₆ = (b₉ . b₄) . b₈ ) )

proof end;

theorem Th32: :: MSUALG_6:32

for b₁ being non empty non void ManySortedSign
for b₂ being non-empty MSAlgebra of b₁
for b₃ being ManySortedRelation of the Sorts of b₂ holds InvCl (StabCl b₃) is stable by Th30;

definition

let c₁ be non empty non void ManySortedSign ;
let c₂ be non-empty MSAlgebra of c₁;
let c₃ be ManySortedRelation of the Sorts of c₂;
func TRS c₃ -> invariant stable ManySortedRelation of a₂ means :Def13: :: MSUALG_6:def 13
( a₃ c= a₄ & ( for b₁ being invariant stable ManySortedRelation of a₂ st a₃ c= b₁ holds
a₄ c= b₁ ) );
uniqueness

proof end;

existence

proof end;

end;

:: deftheorem Def13 defines TRS MSUALG_6:def 13 :

registration

let c₁ be non empty non void ManySortedSign ;
let c₂ be non-empty MSAlgebra of c₁;
let c₃ be V3 ManySortedRelation of c₂;
cluster InvCl a₃ -> V3 invariant ;
coherence

proof end;

cluster StabCl a₃ -> V3 stable ;
coherence

proof end;

cluster TRS a₃ -> V3 invariant stable ;
coherence

proof end;

end;

theorem Th33: :: MSUALG_6:33

for b₁ being non empty non void ManySortedSign
for b₂ being non-empty MSAlgebra of b₁
for b₃ being invariant ManySortedRelation of b₂ holds InvCl b₃ = b₃

proof end;

theorem Th34: :: MSUALG_6:34

for b₁ being non empty non void ManySortedSign
for b₂ being non-empty MSAlgebra of b₁
for b₃ being stable ManySortedRelation of b₂ holds StabCl b₃ = b₃

proof end;

theorem Th35: :: MSUALG_6:35

for b₁ being non empty non void ManySortedSign
for b₂ being non-empty MSAlgebra of b₁
for b₃ being invariant stable ManySortedRelation of b₂ holds TRS b₃ = b₃

proof end;

theorem Th36: :: MSUALG_6:36

for b₁ being non empty non void ManySortedSign
for b₂ being non-empty MSAlgebra of b₁
for b₃ being ManySortedRelation of the Sorts of b₂ holds
( StabCl b₃ c= TRS b₃ & InvCl b₃ c= TRS b₃ & StabCl (InvCl b₃) c= TRS b₃ )

proof end;

theorem Th37: :: MSUALG_6:37

for b₁ being non empty non void ManySortedSign
for b₂ being non-empty MSAlgebra of b₁
for b₃ being ManySortedRelation of the Sorts of b₂ holds InvCl (StabCl b₃) = TRS b₃

proof end;

theorem Th38: :: MSUALG_6:38

for b₁ being non empty non void ManySortedSign
for b₂ being non-empty MSAlgebra of b₁
for b₃ being ManySortedRelation of the Sorts of b₂
for b₄ being SortSymbol of b₁
for b₅, b₆ being Element of b₂,b₄ holds
( [b₅,b₆] in (TRS b₃) . b₄ iff ex b₇ being SortSymbol of b₁ st
( TranslationRel b₁ reduces b₇,b₄ & ex b₈, b₉ being Element of b₂,b₇ex b₁₀ being Endomorphism of b₂ex b₁₁ being Translation of b₂,b₇,b₄ st
( [b₈,b₉] in b₃ . b₇ & b₅ = b₁₁ . ((b₁₀ . b₇) . b₈) & b₆ = b₁₁ . ((b₁₀ . b₇) . b₉) ) ) )

proof end;

theorem Th39: :: MSUALG_6:39

for b₁ being set
for b₂, b₃ being Relation of b₁ st ( for b₄, b₅ being set st b₄ in b₁ & b₅ in b₁ holds
( [b₄,b₅] in b₃ iff b₄,b₅ are_convertible_wrt b₂ ) ) holds
( b₃ is total & b₃ is symmetric & b₃ is transitive )

proof end;

theorem Th40: :: MSUALG_6:40

for b₁ being set
for b₂ being Relation of b₁
for b₃ being Equivalence_Relation of b₁ st b₂ c= b₃ holds
for b₄, b₅ being set st b₄ in b₁ & b₅ in b₁ & b₄,b₅ are_convertible_wrt b₂ holds
[b₄,b₅] in b₃

proof end;

theorem Th41: :: MSUALG_6:41

for b₁ being non empty set
for b₂ being Relation of b₁
for b₃, b₄ being Element of b₁ holds
( [b₃,b₄] in EqCl b₂ iff b₃,b₄ are_convertible_wrt b₂ )

proof end;

theorem Th42: :: MSUALG_6:42

for b₁ being non empty set
for b₂ being V3 ManySortedSet of b₁
for b₃ being ManySortedRelation of b₂
for b₄ being Element of b₁
for b₅, b₆ being Element of b₂ . b₄ holds
( [b₅,b₆] in (EqCl b₃) . b₄ iff b₅,b₆ are_convertible_wrt b₃ . b₄ )

proof end;

definition

let c₁ be non empty non void ManySortedSign ;
let c₂ be non-empty MSAlgebra of c₁;
mode EquationalTheory of a₂ is MSEquivalence-like invariant stable ManySortedRelation of a₂;
let c₃ be ManySortedRelation of c₂;
func EqCl c₃,c₂ -> MSEquivalence-like ManySortedRelation of a₂ equals :: MSUALG_6:def 14
EqCl a₃;
coherence by MSUALG_4:def 5;

end;

:: deftheorem Def14 defines EqCl MSUALG_6:def 14 :

theorem Th43: :: MSUALG_6:43

for b₁ being non empty non void ManySortedSign
for b₂ being non-empty MSAlgebra of b₁
for b₃ being ManySortedRelation of b₂ holds b₃ c= EqCl b₃,b₂

proof end;

theorem Th44: :: MSUALG_6:44

for b₁ being non empty non void ManySortedSign
for b₂ being non-empty MSAlgebra of b₁
for b₃ being ManySortedRelation of b₂
for b₄ being MSEquivalence-like ManySortedRelation of b₂ st b₃ c= b₄ holds
EqCl b₃,b₂ c= b₄

proof end;

theorem Th45: :: MSUALG_6:45

for b₁ being non empty non void ManySortedSign
for b₂ being non-empty MSAlgebra of b₁
for b₃ being stable ManySortedRelation of b₂
for b₄ being SortSymbol of b₁
for b₅, b₆ being Element of b₂,b₄ st b₅,b₆ are_convertible_wrt b₃ . b₄ holds
for b₇ being Endomorphism of b₂ holds (b₇ . b₄) . b₅,(b₇ . b₄) . b₆ are_convertible_wrt b₃ . b₄

proof end;

theorem Th46: :: MSUALG_6:46

for b₁ being non empty non void ManySortedSign
for b₂ being non-empty MSAlgebra of b₁
for b₃ being stable ManySortedRelation of b₂ holds EqCl b₃,b₂ is stable

proof end;

registration

let c₁ be non empty non void ManySortedSign ;
let c₂ be non-empty MSAlgebra of c₁;
let c₃ be stable ManySortedRelation of c₂;
cluster EqCl a₃,a₂ -> V3 MSEquivalence-like stable ;
coherence by Th46;

end;

theorem Th47: :: MSUALG_6:47

for b₁ being non empty non void ManySortedSign
for b₂ being non-empty MSAlgebra of b₁
for b₃ being invariant ManySortedRelation of b₂
for b₄, b₅ being SortSymbol of b₁
for b₆, b₇ being Element of b₂,b₄ st b₆,b₇ are_convertible_wrt b₃ . b₄ holds
for b₈ being Function st b₈ is_e.translation_of b₂,b₄,b₅ holds
b₈ . b₆,b₈ . b₇ are_convertible_wrt b₃ . b₅

proof end;

theorem Th48: :: MSUALG_6:48

for b₁ being non empty non void ManySortedSign
for b₂ being non-empty MSAlgebra of b₁
for b₃ being invariant ManySortedRelation of b₂ holds EqCl b₃,b₂ is invariant

proof end;

registration

let c₁ be non empty non void ManySortedSign ;
let c₂ be non-empty MSAlgebra of c₁;
let c₃ be invariant ManySortedRelation of c₂;
cluster EqCl a₃,a₂ -> V3 MSEquivalence-like compatible invariant ;
coherence by Th48;

end;

theorem Th49: :: MSUALG_6:49

for b₁ being non empty set
for b₂ being V3 ManySortedSet of b₁
for b₃, b₄ being ManySortedRelation of b₂ st ( for b₅ being Element of b₁
for b₆, b₇ being Element of b₂ . b₅ holds
( [b₆,b₇] in b₄ . b₅ iff b₆,b₇ are_convertible_wrt b₃ . b₅ ) ) holds
b₄ is MSEquivalence_Relation-like

proof end;

theorem Th50: :: MSUALG_6:50

for b₁ being non empty non void ManySortedSign
for b₂ being non-empty MSAlgebra of b₁
for b₃, b₄ being ManySortedRelation of b₂ st ( for b₅ being SortSymbol of b₁
for b₆, b₇ being Element of b₂,b₅ holds
( [b₆,b₇] in b₄ . b₅ iff b₆,b₇ are_convertible_wrt (TRS b₃) . b₅ ) ) holds
b₄ is EquationalTheory of b₂

proof end;

theorem Th51: :: MSUALG_6:51

for b₁ being non empty set
for b₂ being V3 ManySortedSet of b₁
for b₃ being ManySortedRelation of b₂
for b₄ being MSEquivalence_Relation-like ManySortedRelation of b₂ st b₃ c= b₄ holds
for b₅ being Element of b₁
for b₆, b₇ being Element of b₂ . b₅ st b₆,b₇ are_convertible_wrt b₃ . b₅ holds
[b₆,b₇] in b₄ . b₅

proof end;

definition

let c₁ be non empty non void ManySortedSign ;
let c₂ be non-empty MSAlgebra of c₁;
let c₃ be ManySortedRelation of the Sorts of c₂;
func EqTh c₃ -> EquationalTheory of a₂ means :Def15: :: MSUALG_6:def 15
( a₃ c= a₄ & ( for b₁ being EquationalTheory of a₂ st a₃ c= b₁ holds
a₄ c= b₁ ) );
uniqueness

proof end;

existence

proof end;

end;

:: deftheorem Def15 defines EqTh MSUALG_6:def 15 :

theorem Th52: :: MSUALG_6:52

for b₁ being non empty non void ManySortedSign
for b₂ being non-empty MSAlgebra of b₁
for b₃ being ManySortedRelation of b₂ holds
( EqCl b₃,b₂ c= EqTh b₃ & InvCl b₃ c= EqTh b₃ & StabCl b₃ c= EqTh b₃ & TRS b₃ c= EqTh b₃ )

proof end;

theorem Th53: :: MSUALG_6:53

for b₁ being non empty non void ManySortedSign
for b₂ being non-empty MSAlgebra of b₁
for b₃ being ManySortedRelation of b₂
for b₄ being SortSymbol of b₁
for b₅, b₆ being Element of b₂,b₄ holds
( [b₅,b₆] in (EqTh b₃) . b₄ iff b₅,b₆ are_convertible_wrt (TRS b₃) . b₄ )

proof end;

theorem Th54: :: MSUALG_6:54

for b₁ being non empty non void ManySortedSign
for b₂ being non-empty MSAlgebra of b₁
for b₃ being ManySortedRelation of b₂ holds EqTh b₃ = EqCl (TRS b₃),b₂

proof end;