:: MSINST_1 semantic presentation

definition

let c₁ be non empty set ;
func MSSCat c₁ -> non empty strict AltCatStr means :Def1: :: MSINST_1:def 1
( the carrier of a₂ = MSS_set a₁ & ( for b₁, b₂ being Element of MSS_set a₁ holds the Arrows of a₂ . b₁,b₂ = MSS_morph b₁,b₂ ) & ( for b₁, b₂, b₃ being object of a₂ st b₁ in MSS_set a₁ & b₂ in MSS_set a₁ & b₃ in MSS_set a₁ holds
for b₄, b₅, b₆, b₇ being Function st [b₄,b₅] in the Arrows of a₂ . b₁,b₂ & [b₆,b₇] in the Arrows of a₂ . b₂,b₃ holds
(the Comp of a₂ . b₁,b₂,b₃) . [b₆,b₇],[b₄,b₅] = [(b₆ * b₄),(b₇ * b₅)] ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def1 defines MSSCat MSINST_1:def 1 :

registration

let c₁ be non empty set ;
cluster MSSCat a₁ -> non empty transitive strict associative with_units ;
coherence

proof end;

end;

theorem Th1: :: MSINST_1:1

for b₁ being non empty set
for b₂ being category st b₂ = MSSCat b₁ holds
for b₃ being object of b₂ holds b₃ is non empty non void ManySortedSign

proof end;

registration

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

proof end;

end;

definition

let c₁ be non empty non void ManySortedSign ;
let c₂ be non empty set ;
func MSAlg_set c₁,c₂ -> set means :Def2: :: MSINST_1:def 2
for b₁ being set holds
( b₁ in a₃ iff ex b₂ being strict feasible MSAlgebra of a₁ st
( b₁ = b₂ & ( for b₃ being Component of the Sorts of b₂ holds b₃ c= a₂ ) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def2 defines MSAlg_set MSINST_1:def 2 :

registration

let c₁ be non empty non void ManySortedSign ;
let c₂ be non empty set ;
cluster MSAlg_set a₁,a₂ -> non empty ;
coherence

proof end;

end;

theorem Th2: :: MSINST_1:2

for b₁ being non empty set
for b₂ being non empty non void ManySortedSign
for b₃ being MSAlgebra of b₂ st b₃ in MSAlg_set b₂,b₁ holds
( the Sorts of b₃ in Funcs the carrier of b₂,(bool b₁) & the Charact of b₃ in Funcs the OperSymbols of b₂,(PFuncs (PFuncs NAT ,b₁),b₁) )

proof end;

theorem Th3: :: MSINST_1:3

for b₁ being non empty non void ManySortedSign
for b₂ being OperSymbol of b₁
for b₃, b₄ being MSAlgebra of b₁ st the Sorts of b₃ is_transformable_to the Sorts of b₄ & Args b₂,b₃ <> {} holds
Args b₂,b₄ <> {}

proof end;

theorem Th4: :: MSINST_1:4

for b₁ being non empty non void ManySortedSign
for b₂ being OperSymbol of b₁
for b₃, b₄, b₅ being feasible MSAlgebra of b₁
for b₆ being ManySortedFunction of b₃,b₄
for b₇ being ManySortedFunction of b₄,b₅
for b₈ being Element of Args b₂,b₃ st Args b₂,b₃ <> {} & the Sorts of b₃ is_transformable_to the Sorts of b₄ & the Sorts of b₄ is_transformable_to the Sorts of b₅ holds
ex b₉ being ManySortedFunction of b₃,b₅ st
( b₉ = b₇ ** b₆ & b₉ # b₈ = b₇ # (b₆ # b₈) )

proof end;

theorem Th5: :: MSINST_1:5

for b₁ being non empty non void ManySortedSign
for b₂, b₃, b₄ being feasible MSAlgebra of b₁
for b₅ being ManySortedFunction of b₂,b₃
for b₆ being ManySortedFunction of b₃,b₄ st the Sorts of b₂ is_transformable_to the Sorts of b₃ & the Sorts of b₃ is_transformable_to the Sorts of b₄ & b₅ is_homomorphism b₂,b₃ & b₆ is_homomorphism b₃,b₄ holds
ex b₇ being ManySortedFunction of b₂,b₄ st
( b₇ = b₆ ** b₅ & b₇ is_homomorphism b₂,b₄ )

proof end;

definition

let c₁ be non empty non void ManySortedSign ;
let c₂ be non empty set ;
let c₃, c₄ be set ;
assume E7: ( c₃ in MSAlg_set c₁,c₂ & c₄ in MSAlg_set c₁,c₂ ) ;
func MSAlg_morph c₁,c₂,c₃,c₄ -> set means :Def3: :: MSINST_1:def 3
for b₁ being set holds
( b₁ in a₅ iff ex b₂, b₃ being strict feasible MSAlgebra of a₁ex b₄ being ManySortedFunction of b₂,b₃ st
( b₂ = a₃ & b₃ = a₄ & b₄ = b₁ & the Sorts of b₂ is_transformable_to the Sorts of b₃ & b₄ is_homomorphism b₂,b₃ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def3 defines MSAlg_morph MSINST_1:def 3 :

definition

let c₁ be non empty non void ManySortedSign ;
let c₂ be non empty set ;
func MSAlgCat c₁,c₂ -> non empty strict AltCatStr means :Def4: :: MSINST_1:def 4
( the carrier of a₃ = MSAlg_set a₁,a₂ & ( for b₁, b₂ being Element of MSAlg_set a₁,a₂ holds the Arrows of a₃ . b₁,b₂ = MSAlg_morph a₁,a₂,b₁,b₂ ) & ( for b₁, b₂, b₃ being object of a₃
for b₄, b₅ being Function-yielding Function st b₄ in the Arrows of a₃ . b₁,b₂ & b₅ in the Arrows of a₃ . b₂,b₃ holds
(the Comp of a₃ . b₁,b₂,b₃) . b₅,b₄ = b₅ ** b₄ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def4 defines MSAlgCat MSINST_1:def 4 :

registration

let c₁ be non empty non void ManySortedSign ;
let c₂ be non empty set ;
cluster MSAlgCat a₁,a₂ -> non empty transitive strict associative with_units ;
coherence

proof end;

end;

theorem Th6: :: MSINST_1:6

for b₁ being non empty set
for b₂ being non empty non void ManySortedSign
for b₃ being category st b₃ = MSAlgCat b₂,b₁ holds
for b₄ being object of b₃ holds b₄ is strict feasible MSAlgebra of b₂

proof end;