:: OSALG_4 semantic presentation

registration

let c₁ be non empty Poset;
cluster Relation-yielding ManySortedSet of the carrier of a₁;
existence

proof end;

end;

definition

let c₁ be non empty Poset;
let c₂, c₃ be ManySortedSet of the carrier of c₁;
let c₄ be ManySortedRelation of c₂,c₃;
attr a₄ is os-compatible means :Def1: :: OSALG_4:def 1
for b₁, b₂ being Element of a₁ st b₁ <= b₂ holds
for b₃, b₄ being set st b₃ in a₂ . b₁ & b₄ in a₃ . b₁ holds
( [b₃,b₄] in a₄ . b₁ iff [b₃,b₄] in a₄ . b₂ );

end;

:: deftheorem Def1 defines os-compatible OSALG_4:def 1 :

registration

let c₁ be non empty Poset;
let c₂, c₃ be ManySortedSet of the carrier of c₁;
cluster os-compatible ManySortedRelation of a₂,a₃;
existence

proof end;

end;

definition

let c₁ be non empty Poset;
let c₂, c₃ be ManySortedSet of the carrier of c₁;
mode OrderSortedRelation of a₂,a₃ is os-compatible ManySortedRelation of a₂,a₃;

end;

theorem Th1: :: OSALG_4:1

for b₁ being non empty Poset
for b₂, b₃ being ManySortedSet of the carrier of b₁
for b₄ being ManySortedRelation of b₂,b₃ st b₄ is os-compatible holds
b₄ is OrderSortedSet of b₁

proof end;

registration

let c₁ be non empty Poset;
let c₂, c₃ be ManySortedSet of c₁;
cluster os-compatible -> order-sorted ManySortedRelation of a₂,a₃;
coherence by Th1;

end;

definition

let c₁ be non empty Poset;
let c₂ be ManySortedSet of the carrier of c₁;
mode OrderSortedRelation of a₂ is OrderSortedRelation of a₂,a₂;

end;

definition

let c₁ be OrderSortedSign;
let c₂ be OSAlgebra of c₁;
canceled;
mode OrderSortedRelation of c₂ -> ManySortedRelation of a₂ means :Def3: :: OSALG_4:def 3
a₃ is os-compatible;
existence

proof end;

end;

:: deftheorem Def2 OSALG_4:def 2 :

:: deftheorem Def3 defines OrderSortedRelation OSALG_4:def 3 :

registration

let c₁ be OrderSortedSign;
let c₂ be OSAlgebra of c₁;
cluster MSEquivalence-like OrderSortedRelation of a₂;
existence

proof end;

end;

registration

let c₁ be OrderSortedSign;
let c₂ be non-empty OSAlgebra of c₁;
cluster MSEquivalence-like MSCongruence-like OrderSortedRelation of a₂;
existence

proof end;

end;

definition

let c₁ be OrderSortedSign;
let c₂ be non-empty OSAlgebra of c₁;
mode OSCongruence of a₂ is MSEquivalence-like MSCongruence-like OrderSortedRelation of a₂;

end;

definition

let c₁ be non empty Poset;
func Path_Rel c₁ -> Equivalence_Relation of the carrier of a₁ means :Def4: :: OSALG_4:def 4
for b₁, b₂ being set holds
( [b₁,b₂] in a₂ iff ( b₁ in the carrier of a₁ & b₂ in the carrier of a₁ & ex b₃ being FinSequence of the carrier of a₁ st
( 1 < len b₃ & b₃ . 1 = b₁ & b₃ . (len b₃) = b₂ & ( for b₄ being Nat st 2 <= b₄ & b₄ <= len b₃ & not [(b₃ . b₄),(b₃ . (b₄ - 1))] in the InternalRel of a₁ holds
[(b₃ . (b₄ - 1)),(b₃ . b₄)] in the InternalRel of a₁ ) ) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def4 defines Path_Rel OSALG_4:def 4 :

theorem Th2: :: OSALG_4:2

for b₁ being non empty Poset
for b₂, b₃ being Element of b₁ st b₂ <= b₃ holds
[b₂,b₃] in Path_Rel b₁

proof end;

definition

let c₁ be non empty Poset;
let c₂, c₃ be Element of c₁;
pred c₂ ~= c₃ means :Def5: :: OSALG_4:def 5
[a₂,a₃] in Path_Rel a₁;
reflexivity

proof end;

symmetry

proof end;

end;

:: deftheorem Def5 defines ~= OSALG_4:def 5 :

theorem Th3: :: OSALG_4:3

for b₁ being non empty Poset
for b₂, b₃, b₄ being Element of b₁ st b₂ ~= b₃ & b₃ ~= b₄ holds
b₂ ~= b₄

proof end;

definition

let c₁ be non empty Poset;
func Components c₁ -> non empty Subset-Family of a₁ equals :: OSALG_4:def 6
Class (Path_Rel a₁);
coherence ;

end;

:: deftheorem Def6 defines Components OSALG_4:def 6 :

registration

let c₁ be non empty Poset;
cluster -> non empty Element of Components a₁;
coherence

proof end;

end;

definition

let c₁ be non empty Poset;
mode Component of a₁ is Element of Components a₁;

end;

definition

let c₁ be non empty Poset;
let c₂ be Element of c₁;
canceled;
func CComp c₂ -> Component of a₁ equals :: OSALG_4:def 8
Class (Path_Rel a₁),a₂;
correctness by EQREL_1:def 5;

end;

:: deftheorem Def7 OSALG_4:def 7 :

:: deftheorem Def8 defines CComp OSALG_4:def 8 :

theorem Th4: :: OSALG_4:4

for b₁ being non empty Poset
for b₂ being Element of b₁ holds b₂ in CComp b₂ by EQREL_1:28;

theorem Th5: :: OSALG_4:5

for b₁ being non empty Poset
for b₂, b₃ being Element of b₁ st b₂ <= b₃ holds
CComp b₂ = CComp b₃

proof end;

definition

let c₁ be non empty Poset;
let c₂ be ManySortedSet of the carrier of c₁;
let c₃ be Component of c₁;
func c₂ -carrier_of c₃ -> set equals :: OSALG_4:def 9
union { (a₂ . b₁) where B is Element of a₁ : b₁ in a₃ } ;
correctness ;

end;

:: deftheorem Def9 defines -carrier_of OSALG_4:def 9 :

theorem Th6: :: OSALG_4:6

for b₁ being non empty Poset
for b₂ being ManySortedSet of the carrier of b₁
for b₃ being Element of b₁
for b₄ being set st b₄ in b₂ . b₃ holds
b₄ in b₂ -carrier_of (CComp b₃)

proof end;

definition

let c₁ be non empty Poset;
attr a₁ is locally_directed means :Def10: :: OSALG_4:def 10
for b₁ being Component of a₁ holds b₁ is directed;

end;

:: deftheorem Def10 defines locally_directed OSALG_4:def 10 :

theorem Th7: :: OSALG_4:7

for b₁ being non empty discrete Poset
for b₂, b₃ being Element of b₁ st [b₂,b₃] in Path_Rel b₁ holds
b₂ = b₃

proof end;

theorem Th8: :: OSALG_4:8

for b₁ being non empty discrete Poset
for b₂ being Component of b₁ ex b₃ being Element of b₁ st b₂ = {b₃}

proof end;

theorem Th9: :: OSALG_4:9

for b₁ being non empty discrete Poset holds b₁ is locally_directed

proof end;

registration

cluster non empty locally_directed RelStr ;
existence

proof end;

end;

registration

cluster locally_directed OverloadedRSSign ;
existence

proof end;

end;

registration

cluster non empty discrete -> non empty locally_directed RelStr ;
coherence by Th9;

end;

registration

let c₁ be non empty locally_directed Poset;
cluster -> non empty directed Element of Components a₁;
coherence by Def10;

end;

theorem Th10: :: OSALG_4:10

{} is Equivalence_Relation of {}

proof end;

definition

let c₁ be locally_directed OrderSortedSign;
let c₂ be OSAlgebra of c₁;
let c₃ be MSEquivalence-like OrderSortedRelation of c₂;
let c₄ be Component of c₁;
func CompClass c₃,c₄ -> Equivalence_Relation of the Sorts of a₂ -carrier_of a₄ means :Def11: :: OSALG_4:def 11
for b₁, b₂ being set holds
( [b₁,b₂] in a₅ iff ex b₃ being Element of a₁ st
( b₃ in a₄ & [b₁,b₂] in a₃ . b₃ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def11 defines CompClass OSALG_4:def 11 :

definition

let c₁ be locally_directed OrderSortedSign;
let c₂ be OSAlgebra of c₁;
let c₃ be MSEquivalence-like OrderSortedRelation of c₂;
let c₄ be Element of c₁;
func OSClass c₃,c₄ -> Subset of (Class (CompClass a₃,(CComp a₄))) means :Def12: :: OSALG_4:def 12
for b₁ being set holds
( b₁ in a₅ iff ex b₂ being set st
( b₂ in the Sorts of a₂ . a₄ & b₁ = Class (CompClass a₃,(CComp a₄)),b₂ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def12 defines OSClass OSALG_4:def 12 :

registration

proof end;

end;

theorem Th11: :: OSALG_4:11

for b₁ being locally_directed OrderSortedSign
for b₂ being OSAlgebra of b₁
for b₃ being MSEquivalence-like OrderSortedRelation of b₂
for b₄, b₅ being Element of b₁ st b₄ <= b₅ holds
OSClass b₃,b₄ c= OSClass b₃,b₅

proof end;

definition

let c₁ be locally_directed OrderSortedSign;
let c₂ be OSAlgebra of c₁;
let c₃ be MSEquivalence-like OrderSortedRelation of c₂;
func OSClass c₃ -> OrderSortedSet of a₁ means :Def13: :: OSALG_4:def 13
for b₁ being Element of a₁ holds a₄ . b₁ = OSClass a₃,b₁;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def13 defines OSClass OSALG_4:def 13 :

registration

let c₁ be locally_directed OrderSortedSign;
let c₂ be non-empty OSAlgebra of c₁;
let c₃ be MSEquivalence-like OrderSortedRelation of c₂;
cluster OSClass a₃ -> V2 ;
coherence

proof end;

end;

definition

let c₁ be locally_directed OrderSortedSign;
let c₂ be non-empty OSAlgebra of c₁;
let c₃ be MSEquivalence-like OrderSortedRelation of c₂;
let c₄ be Element of c₁;
let c₅ be Element of the Sorts of c₂ . c₄;
func OSClass c₃,c₅ -> Element of OSClass a₃,a₄ equals :: OSALG_4:def 14
Class (CompClass a₃,(CComp a₄)),a₅;
correctness by Def12;

end;

:: deftheorem Def14 defines OSClass OSALG_4:def 14 :

theorem Th12: :: OSALG_4:12

for b₁ being non empty locally_directed Poset
for b₂, b₃ being Element of b₁ st ex b₄ being Element of b₁ st
( b₄ <= b₂ & b₄ <= b₃ ) holds
ex b₄ being Element of b₁ st
( b₂ <= b₄ & b₃ <= b₄ )

proof end;

theorem Th13: :: OSALG_4:13

for b₁ being locally_directed OrderSortedSign
for b₂ being non-empty OSAlgebra of b₁
for b₃ being MSEquivalence-like OrderSortedRelation of b₂
for b₄ being Element of b₁
for b₅, b₆ being Element of the Sorts of b₂ . b₄ holds
( OSClass b₃,b₅ = OSClass b₃,b₆ iff [b₅,b₆] in b₃ . b₄ )

proof end;

theorem Th14: :: OSALG_4:14

for b₁ being locally_directed OrderSortedSign
for b₂ being non-empty OSAlgebra of b₁
for b₃ being MSEquivalence-like OrderSortedRelation of b₂
for b₄, b₅ being Element of b₁
for b₆ being Element of the Sorts of b₂ . b₄ st b₄ <= b₅ holds
for b₇ being Element of the Sorts of b₂ . b₅ st b₇ = b₆ holds
OSClass b₃,b₆ = OSClass b₃,b₇

proof end;

definition

let c₁ be locally_directed OrderSortedSign;
let c₂ be Element of the OperSymbols of c₁;
let c₃ be non-empty OSAlgebra of c₁;
let c₄ be OSCongruence of c₃;
let c₅ be Element of Args c₂,c₃;
func c₄ #_os c₅ -> Element of product ((OSClass a₄) * (the_arity_of a₂)) means :Def15: :: OSALG_4:def 15
for b₁ being Nat st b₁ in dom (the_arity_of a₂) holds
ex b₂ being Element of the Sorts of a₃ . ((the_arity_of a₂) /. b₁) st
( b₂ = a₅ . b₁ & a₆ . b₁ = OSClass a₄,b₂ );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def15 defines #_os OSALG_4:def 15 :

definition

let c₁ be locally_directed OrderSortedSign;
let c₂ be Element of the OperSymbols of c₁;
let c₃ be non-empty OSAlgebra of c₁;
let c₄ be OSCongruence of c₃;
func OSQuotRes c₄,c₂ -> Function of (the Sorts of a₃ * the ResultSort of a₁) . a₂,((OSClass a₄) * the ResultSort of a₁) . a₂ means :Def16: :: OSALG_4:def 16
for b₁ being Element of the Sorts of a₃ . (the_result_sort_of a₂) holds a₅ . b₁ = OSClass a₄,b₁;
existence

proof end;

uniqueness

proof end;

func OSQuotArgs c₄,c₂ -> Function of ((the Sorts of a₃ # ) * the Arity of a₁) . a₂,(((OSClass a₄) # ) * the Arity of a₁) . a₂ means :: OSALG_4:def 17
for b₁ being Element of Args a₂,a₃ holds a₅ . b₁ = a₄ #_os b₁;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def16 defines OSQuotRes OSALG_4:def 16 :

:: deftheorem Def17 defines OSQuotArgs OSALG_4:def 17 :

definition

let c₁ be locally_directed OrderSortedSign;
let c₂ be non-empty OSAlgebra of c₁;
let c₃ be OSCongruence of c₂;
func OSQuotRes c₃ -> ManySortedFunction of the Sorts of a₂ * the ResultSort of a₁,(OSClass a₃) * the ResultSort of a₁ means :: OSALG_4:def 18
for b₁ being OperSymbol of a₁ holds a₄ . b₁ = OSQuotRes a₃,b₁;
existence

proof end;

uniqueness

proof end;

func OSQuotArgs c₃ -> ManySortedFunction of (the Sorts of a₂ # ) * the Arity of a₁,((OSClass a₃) # ) * the Arity of a₁ means :: OSALG_4:def 19
for b₁ being OperSymbol of a₁ holds a₄ . b₁ = OSQuotArgs a₃,b₁;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def18 defines OSQuotRes OSALG_4:def 18 :

:: deftheorem Def19 defines OSQuotArgs OSALG_4:def 19 :

theorem Th15: :: OSALG_4:15

for b₁ being locally_directed OrderSortedSign
for b₂ being Element of the OperSymbols of b₁
for b₃ being non-empty OSAlgebra of b₁
for b₄ being OSCongruence of b₃
for b₅ being set st b₅ in (((OSClass b₄) # ) * the Arity of b₁) . b₂ holds
ex b₆ being Element of Args b₂,b₃ st b₅ = b₄ #_os b₆

proof end;

definition

let c₁ be locally_directed OrderSortedSign;
let c₂ be Element of the OperSymbols of c₁;
let c₃ be non-empty OSAlgebra of c₁;
let c₄ be OSCongruence of c₃;
func OSQuotCharact c₄,c₂ -> Function of (((OSClass a₄) # ) * the Arity of a₁) . a₂,((OSClass a₄) * the ResultSort of a₁) . a₂ means :Def20: :: OSALG_4:def 20
for b₁ being Element of Args a₂,a₃ st a₄ #_os b₁ in (((OSClass a₄) # ) * the Arity of a₁) . a₂ holds
a₅ . (a₄ #_os b₁) = ((OSQuotRes a₄,a₂) * (Den a₂,a₃)) . b₁;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def20 defines OSQuotCharact OSALG_4:def 20 :

definition

let c₁ be locally_directed OrderSortedSign;
let c₂ be non-empty OSAlgebra of c₁;
let c₃ be OSCongruence of c₂;
func OSQuotCharact c₃ -> ManySortedFunction of ((OSClass a₃) # ) * the Arity of a₁,(OSClass a₃) * the ResultSort of a₁ means :Def21: :: OSALG_4:def 21
for b₁ being OperSymbol of a₁ holds a₄ . b₁ = OSQuotCharact a₃,b₁;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def21 defines OSQuotCharact OSALG_4:def 21 :

definition

let c₁ be locally_directed OrderSortedSign;
let c₂ be non-empty OSAlgebra of c₁;
let c₃ be OSCongruence of c₂;
func QuotOSAlg c₂,c₃ -> OSAlgebra of a₁ equals :: OSALG_4:def 22
MSAlgebra(# (OSClass a₃),(OSQuotCharact a₃) #);
coherence by OSALG_1:17;

end;

:: deftheorem Def22 defines QuotOSAlg OSALG_4:def 22 :

registration

let c₁ be locally_directed OrderSortedSign;
let c₂ be non-empty OSAlgebra of c₁;
let c₃ be OSCongruence of c₂;
cluster QuotOSAlg a₂,a₃ -> strict non-empty ;
coherence by MSUALG_1:def 8;

end;

definition

let c₁ be locally_directed OrderSortedSign;
let c₂ be non-empty OSAlgebra of c₁;
let c₃ be OSCongruence of c₂;
let c₄ be Element of c₁;
func OSNat_Hom c₂,c₃,c₄ -> Function of the Sorts of a₂ . a₄, OSClass a₃,a₄ means :Def23: :: OSALG_4:def 23
for b₁ being Element of the Sorts of a₂ . a₄ holds a₅ . b₁ = OSClass a₃,b₁;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def23 defines OSNat_Hom OSALG_4:def 23 :

definition

let c₁ be locally_directed OrderSortedSign;
let c₂ be non-empty OSAlgebra of c₁;
let c₃ be OSCongruence of c₂;
func OSNat_Hom c₂,c₃ -> ManySortedFunction of a₂,(QuotOSAlg a₂,a₃) means :Def24: :: OSALG_4:def 24
for b₁ being Element of a₁ holds a₄ . b₁ = OSNat_Hom a₂,a₃,b₁;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def24 defines OSNat_Hom OSALG_4:def 24 :

theorem Th16: :: OSALG_4:16

for b₁ being locally_directed OrderSortedSign
for b₂ being non-empty OSAlgebra of b₁
for b₃ being OSCongruence of b₂ holds
( OSNat_Hom b₂,b₃ is_epimorphism b₂, QuotOSAlg b₂,b₃ & OSNat_Hom b₂,b₃ is order-sorted )

proof end;

theorem Th17: :: OSALG_4:17

for b₁ being locally_directed OrderSortedSign
for b₂, b₃ being non-empty OSAlgebra of b₁
for b₄ being ManySortedFunction of b₂,b₃ st b₄ is_homomorphism b₂,b₃ & b₄ is order-sorted holds
MSCng b₄ is OSCongruence of b₂

proof end;

definition

let c₁ be locally_directed OrderSortedSign;
let c₂, c₃ be non-empty OSAlgebra of c₁;
let c₄ be ManySortedFunction of c₂,c₃;
assume E29: ( c₄ is_homomorphism c₂,c₃ & c₄ is order-sorted ) ;
func OSCng c₄ -> OSCongruence of a₂ equals :Def25: :: OSALG_4:def 25
MSCng a₄;
correctness by E29, Th17;

end;

:: deftheorem Def25 defines OSCng OSALG_4:def 25 :

definition

let c₁ be locally_directed OrderSortedSign;
let c₂, c₃ be non-empty OSAlgebra of c₁;
let c₄ be ManySortedFunction of c₂,c₃;
let c₅ be Element of c₁;
assume E30: ( c₄ is_homomorphism c₂,c₃ & c₄ is order-sorted ) ;
func OSHomQuot c₄,c₅ -> Function of the Sorts of (QuotOSAlg a₂,(OSCng a₄)) . a₅,the Sorts of a₃ . a₅ means :Def26: :: OSALG_4:def 26
for b₁ being Element of the Sorts of a₂ . a₅ holds a₆ . (OSClass (OSCng a₄),b₁) = (a₄ . a₅) . b₁;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def26 defines OSHomQuot OSALG_4:def 26 :

definition

let c₁ be locally_directed OrderSortedSign;
let c₂, c₃ be non-empty OSAlgebra of c₁;
let c₄ be ManySortedFunction of c₂,c₃;
func OSHomQuot c₄ -> ManySortedFunction of (QuotOSAlg a₂,(OSCng a₄)),a₃ means :Def27: :: OSALG_4:def 27
for b₁ being Element of a₁ holds a₅ . b₁ = OSHomQuot a₄,b₁;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def27 defines OSHomQuot OSALG_4:def 27 :

theorem Th18: :: OSALG_4:18

proof end;

theorem Th19: :: OSALG_4:19

for b₁ being locally_directed OrderSortedSign
for b₂, b₃ being non-empty OSAlgebra of b₁
for b₄ being ManySortedFunction of b₂,b₃ st b₄ is_epimorphism b₂,b₃ & b₄ is order-sorted holds
OSHomQuot b₄ is_isomorphism QuotOSAlg b₂,(OSCng b₄),b₃

proof end;

theorem Th20: :: OSALG_4:20

proof end;

definition

let c₁ be OrderSortedSign;
let c₂ be non-empty OSAlgebra of c₁;
let c₃ be MSEquivalence-like OrderSortedRelation of c₂;
attr a₃ is monotone means :Def28: :: OSALG_4:def 28
for b₁, b₂ being OperSymbol of a₁ st b₁ <= b₂ holds
for b₃ being Element of Args b₁,a₂
for b₄ being Element of Args b₂,a₂ st ( for b₅ being Nat st b₅ in dom 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₂);

end;

:: deftheorem Def28 defines monotone OSALG_4:def 28 :

theorem Th21: :: OSALG_4:21

for b₁ being OrderSortedSign
for b₂ being non-empty OSAlgebra of b₁ holds [|the Sorts of b₂,the Sorts of b₂|] is OSCongruence of b₂

proof end;

theorem Th22: :: OSALG_4:22

for b₁ being OrderSortedSign
for b₂ being non-empty OSAlgebra of b₁
for b₃ being OSCongruence of b₂ st b₃ = [|the Sorts of b₂,the Sorts of b₂|] holds
b₃ is monotone

proof end;

registration

let c₁ be OrderSortedSign;
let c₂ be non-empty OSAlgebra of c₁;
cluster monotone OrderSortedRelation of a₂;
existence

proof end;

end;

registration

let c₁ be OrderSortedSign;
let c₂ be non-empty OSAlgebra of c₁;
cluster MSEquivalence-like monotone OrderSortedRelation of a₂;
existence

proof end;

end;

theorem Th23: :: OSALG_4:23

for b₁ being OrderSortedSign
for b₂ being non-empty OSAlgebra of b₁
for b₃ being MSEquivalence-like monotone OrderSortedRelation of b₂ holds b₃ is MSCongruence-like

proof end;

registration

let c₁ be OrderSortedSign;
let c₂ be non-empty OSAlgebra of c₁;
cluster MSEquivalence-like monotone -> MSEquivalence-like MSCongruence-like OrderSortedRelation of a₂;
coherence by Th23;

end;

theorem Th24: :: OSALG_4:24

for b₁ being OrderSortedSign
for b₂ being non-empty monotone OSAlgebra of b₁
for b₃ being OSCongruence of b₂ holds b₃ is monotone

proof end;

registration

let c₁ be OrderSortedSign;
let c₂ be non-empty monotone OSAlgebra of c₁;
cluster -> monotone OrderSortedRelation of a₂;
coherence by Th24;

end;

registration

let c₁ be locally_directed OrderSortedSign;
let c₂ be non-empty OSAlgebra of c₁;
let c₃ be monotone OSCongruence of c₂;
cluster QuotOSAlg a₂,a₃ -> strict non-empty monotone ;
coherence

proof end;

end;

theorem Th25: :: OSALG_4:25

canceled;

theorem Th26: :: OSALG_4:26

for b₁ being locally_directed OrderSortedSign
for b₂ being non-empty OSAlgebra of b₁
for b₃ being non-empty monotone OSAlgebra of b₁
for b₄ being ManySortedFunction of b₂,b₃ st b₄ is_homomorphism b₂,b₃ & b₄ is order-sorted holds
OSCng b₄ is monotone

proof end;

definition

let c₁ be locally_directed OrderSortedSign;
let c₂, c₃ be non-empty OSAlgebra of c₁;
let c₄ be ManySortedFunction of c₂,c₃;
let c₅ be OSCongruence of c₂;
let c₆ be Element of c₁;
assume E39: ( c₄ is_homomorphism c₂,c₃ & c₄ is order-sorted & c₅ c= OSCng c₄ ) ;
func OSHomQuot c₄,c₅,c₆ -> Function of the Sorts of (QuotOSAlg a₂,a₅) . a₆,the Sorts of a₃ . a₆ means :Def29: :: OSALG_4:def 29
for b₁ being Element of the Sorts of a₂ . a₆ holds a₇ . (OSClass a₅,b₁) = (a₄ . a₆) . b₁;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def29 defines OSHomQuot OSALG_4:def 29 :

definition

let c₁ be locally_directed OrderSortedSign;
let c₂, c₃ be non-empty OSAlgebra of c₁;
let c₄ be ManySortedFunction of c₂,c₃;
let c₅ be OSCongruence of c₂;
func OSHomQuot c₄,c₅ -> ManySortedFunction of (QuotOSAlg a₂,a₅),a₃ means :Def30: :: OSALG_4:def 30
for b₁ being Element of a₁ holds a₆ . b₁ = OSHomQuot a₄,a₅,b₁;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def30 defines OSHomQuot OSALG_4:def 30 :

theorem Th27: :: OSALG_4:27

for b₁ being locally_directed OrderSortedSign
for b₂, b₃ being non-empty OSAlgebra of b₁
for b₄ being ManySortedFunction of b₂,b₃
for b₅ being OSCongruence of b₂ st b₄ is_homomorphism b₂,b₃ & b₄ is order-sorted & b₅ c= OSCng b₄ holds
( OSHomQuot b₄,b₅ is_homomorphism QuotOSAlg b₂,b₅,b₃ & OSHomQuot b₄,b₅ is order-sorted )

proof end;