:: by Josef Urban

::

:: Received September 19, 2002

:: Copyright (c) 2002-2021 Association of Mizar Users

registration

let R be non empty Poset;

ex b_{1} being OrderSortedSet of R st b_{1} is Relation-yielding

end;
cluster Relation-like the carrier of R -defined non empty Function-like total Relation-yielding order-sorted for set ;

existence ex b

proof end;

:: this is a stronger condition for relation than just being order-sorted

definition

let R be non empty Poset;

let A, B be ManySortedSet of the carrier of R;

let IT be ManySortedRelation of A,B;

end;
let A, B be ManySortedSet of the carrier of R;

let IT be ManySortedRelation of A,B;

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

for R being non empty Poset

for A, B being ManySortedSet of the carrier of R

for IT being ManySortedRelation of A,B holds

( IT is os-compatible iff for s1, s2 being Element of R st s1 <= s2 holds

for x, y being set st x in A . s1 & y in B . s1 holds

( [x,y] in IT . s1 iff [x,y] in IT . s2 ) );

for R being non empty Poset

for A, B being ManySortedSet of the carrier of R

for IT being ManySortedRelation of A,B holds

( IT is os-compatible iff for s1, s2 being Element of R st s1 <= s2 holds

for x, y being set st x in A . s1 & y in B . s1 holds

( [x,y] in IT . s1 iff [x,y] in IT . s2 ) );

registration

let R be non empty Poset;

let A, B be ManySortedSet of the carrier of R;

ex b_{1} being ManySortedRelation of A,B st b_{1} is os-compatible

end;
let A, B be ManySortedSet of the carrier of R;

cluster Relation-like the carrier of R -defined non empty Function-like total Relation-yielding os-compatible for ManySortedRelation of A,B;

existence ex b

proof end;

definition

let R be non empty Poset;

let A, B be ManySortedSet of the carrier of R;

mode OrderSortedRelation of A,B is os-compatible ManySortedRelation of A,B;

end;
let A, B be ManySortedSet of the carrier of R;

mode OrderSortedRelation of A,B is os-compatible ManySortedRelation of A,B;

theorem Th1: :: OSALG_4:1

for R being non empty Poset

for A, B being ManySortedSet of the carrier of R

for OR being ManySortedRelation of A,B st OR is os-compatible holds

OR is OrderSortedSet of R

for A, B being ManySortedSet of the carrier of R

for OR being ManySortedRelation of A,B st OR is os-compatible holds

OR is OrderSortedSet of R

proof end;

registration

let R be non empty Poset;

let A, B be ManySortedSet of R;

coherence

for b_{1} being ManySortedRelation of A,B st b_{1} is os-compatible holds

b_{1} is order-sorted
by Th1;

end;
let A, B be ManySortedSet of R;

coherence

for b

b

definition

let R be non empty Poset;

let A be ManySortedSet of the carrier of R;

mode OrderSortedRelation of A is OrderSortedRelation of A,A;

end;
let A be ManySortedSet of the carrier of R;

mode OrderSortedRelation of A is OrderSortedRelation of A,A;

definition

let S be OrderSortedSign;

let U1 be OSAlgebra of S;

ex b_{1} being ManySortedRelation of U1 st b_{1} is os-compatible

end;
let U1 be OSAlgebra of S;

mode OrderSortedRelation of U1 -> ManySortedRelation of U1 means :Def2: :: OSALG_4:def 2

it is os-compatible ;

existence it is os-compatible ;

ex b

proof end;

:: deftheorem Def2 defines OrderSortedRelation OSALG_4:def 2 :

for S being OrderSortedSign

for U1 being OSAlgebra of S

for b_{3} being ManySortedRelation of U1 holds

( b_{3} is OrderSortedRelation of U1 iff b_{3} is os-compatible );

for S being OrderSortedSign

for U1 being OSAlgebra of S

for b

( b

:: REVISE: the definition of ManySorted diagonal from MSUALG_6

:: should be moved to MSUALG_4; the "compatible" attr from MSUALG_6

:: should replace the MSCongruence-like

:: should be moved to MSUALG_4; the "compatible" attr from MSUALG_6

:: should replace the MSCongruence-like

registration

let S be OrderSortedSign;

let U1 be OSAlgebra of S;

ex b_{1} being OrderSortedRelation of U1 st b_{1} is MSEquivalence-like

end;
let U1 be OSAlgebra of S;

cluster Relation-like the carrier of S -defined non empty Function-like total Relation-yielding MSEquivalence-like for OrderSortedRelation of U1;

existence ex b

proof end;

:: REVISE: we need the fact that id has the type,

:: the original prf can be simplified

:: the original prf can be simplified

registration

let S be OrderSortedSign;

let U1 be non-empty OSAlgebra of S;

ex b_{1} being MSEquivalence-like OrderSortedRelation of U1 st b_{1} is MSCongruence-like

end;
let U1 be non-empty OSAlgebra of S;

cluster Relation-like the carrier of S -defined non empty Function-like total Relation-yielding MSEquivalence-like MSCongruence-like for OrderSortedRelation of U1;

existence ex b

proof end;

definition

let S be OrderSortedSign;

let U1 be non-empty OSAlgebra of S;

mode OSCongruence of U1 is MSEquivalence-like MSCongruence-like OrderSortedRelation of U1;

end;
let U1 be non-empty OSAlgebra of S;

mode OSCongruence of U1 is MSEquivalence-like MSCongruence-like OrderSortedRelation of U1;

:: TODO: a smooth transition between Relations and Graphs would

:: be useful here, the FinSequence approach seemed to me faster than

:: transitive closure of R \/ R" .. maybe not, can be later a theorem

:: all could be done generally for reflexive (or with small

:: modification even non reflexive) Relations

:: I found ex post that attributes disconnected and connected defined

:: in ORDERS_3 have st. in common here, but the theory there is not developed

:: suggested improvements: f connects x,y; x is_connected_with y;

:: connected iff for x,y holds x is_connected_with y

:: finally I found this is the EqCl from MSUALG_5 - should be merged

:: be useful here, the FinSequence approach seemed to me faster than

:: transitive closure of R \/ R" .. maybe not, can be later a theorem

:: all could be done generally for reflexive (or with small

:: modification even non reflexive) Relations

:: I found ex post that attributes disconnected and connected defined

:: in ORDERS_3 have st. in common here, but the theory there is not developed

:: suggested improvements: f connects x,y; x is_connected_with y;

:: connected iff for x,y holds x is_connected_with y

:: finally I found this is the EqCl from MSUALG_5 - should be merged

definition

let R be non empty Poset;

ex b_{1} being Equivalence_Relation of the carrier of R st

for x, y being object holds

( [x,y] in b_{1} iff ( x in the carrier of R & y in the carrier of R & ex p being FinSequence of the carrier of R st

( 1 < len p & p . 1 = x & p . (len p) = y & ( for n being Nat st 2 <= n & n <= len p & not [(p . n),(p . (n - 1))] in the InternalRel of R holds

[(p . (n - 1)),(p . n)] in the InternalRel of R ) ) ) )

for b_{1}, b_{2} being Equivalence_Relation of the carrier of R st ( for x, y being object holds

( [x,y] in b_{1} iff ( x in the carrier of R & y in the carrier of R & ex p being FinSequence of the carrier of R st

( 1 < len p & p . 1 = x & p . (len p) = y & ( for n being Nat st 2 <= n & n <= len p & not [(p . n),(p . (n - 1))] in the InternalRel of R holds

[(p . (n - 1)),(p . n)] in the InternalRel of R ) ) ) ) ) & ( for x, y being object holds

( [x,y] in b_{2} iff ( x in the carrier of R & y in the carrier of R & ex p being FinSequence of the carrier of R st

( 1 < len p & p . 1 = x & p . (len p) = y & ( for n being Nat st 2 <= n & n <= len p & not [(p . n),(p . (n - 1))] in the InternalRel of R holds

[(p . (n - 1)),(p . n)] in the InternalRel of R ) ) ) ) ) holds

b_{1} = b_{2}

end;
func Path_Rel R -> Equivalence_Relation of the carrier of R means :Def3: :: OSALG_4:def 3

for x, y being object holds

( [x,y] in it iff ( x in the carrier of R & y in the carrier of R & ex p being FinSequence of the carrier of R st

( 1 < len p & p . 1 = x & p . (len p) = y & ( for n being Nat st 2 <= n & n <= len p & not [(p . n),(p . (n - 1))] in the InternalRel of R holds

[(p . (n - 1)),(p . n)] in the InternalRel of R ) ) ) );

existence for x, y being object holds

( [x,y] in it iff ( x in the carrier of R & y in the carrier of R & ex p being FinSequence of the carrier of R st

( 1 < len p & p . 1 = x & p . (len p) = y & ( for n being Nat st 2 <= n & n <= len p & not [(p . n),(p . (n - 1))] in the InternalRel of R holds

[(p . (n - 1)),(p . n)] in the InternalRel of R ) ) ) );

ex b

for x, y being object holds

( [x,y] in b

( 1 < len p & p . 1 = x & p . (len p) = y & ( for n being Nat st 2 <= n & n <= len p & not [(p . n),(p . (n - 1))] in the InternalRel of R holds

[(p . (n - 1)),(p . n)] in the InternalRel of R ) ) ) )

proof end;

uniqueness for b

( [x,y] in b

( 1 < len p & p . 1 = x & p . (len p) = y & ( for n being Nat st 2 <= n & n <= len p & not [(p . n),(p . (n - 1))] in the InternalRel of R holds

[(p . (n - 1)),(p . n)] in the InternalRel of R ) ) ) ) ) & ( for x, y being object holds

( [x,y] in b

( 1 < len p & p . 1 = x & p . (len p) = y & ( for n being Nat st 2 <= n & n <= len p & not [(p . n),(p . (n - 1))] in the InternalRel of R holds

[(p . (n - 1)),(p . n)] in the InternalRel of R ) ) ) ) ) holds

b

proof end;

:: deftheorem Def3 defines Path_Rel OSALG_4:def 3 :

for R being non empty Poset

for b_{2} being Equivalence_Relation of the carrier of R holds

( b_{2} = Path_Rel R iff for x, y being object holds

( [x,y] in b_{2} iff ( x in the carrier of R & y in the carrier of R & ex p being FinSequence of the carrier of R st

( 1 < len p & p . 1 = x & p . (len p) = y & ( for n being Nat st 2 <= n & n <= len p & not [(p . n),(p . (n - 1))] in the InternalRel of R holds

[(p . (n - 1)),(p . n)] in the InternalRel of R ) ) ) ) );

for R being non empty Poset

for b

( b

( [x,y] in b

( 1 < len p & p . 1 = x & p . (len p) = y & ( for n being Nat st 2 <= n & n <= len p & not [(p . n),(p . (n - 1))] in the InternalRel of R holds

[(p . (n - 1)),(p . n)] in the InternalRel of R ) ) ) ) );

:: again, should be defined for Relations probably

definition

let R be non empty Poset;

let s1, s2 be Element of R;

reflexivity

for s1 being Element of R holds [s1,s1] in Path_Rel R

for s1, s2 being Element of R st [s1,s2] in Path_Rel R holds

[s2,s1] in Path_Rel R

end;
let s1, s2 be Element of R;

reflexivity

for s1 being Element of R holds [s1,s1] in Path_Rel R

proof end;

symmetry for s1, s2 being Element of R st [s1,s2] in Path_Rel R holds

[s2,s1] in Path_Rel R

proof end;

:: deftheorem defines ~= OSALG_4:def 4 :

for R being non empty Poset

for s1, s2 being Element of R holds

( s1 ~= s2 iff [s1,s2] in Path_Rel R );

for R being non empty Poset

for s1, s2 being Element of R holds

( s1 ~= s2 iff [s1,s2] in Path_Rel R );

:: do for Relations

definition
end;

:: deftheorem defines Components OSALG_4:def 5 :

for R being non empty Poset holds Components R = Class (Path_Rel R);

for R being non empty Poset holds Components R = Class (Path_Rel R);

registration

let R be non empty Poset;

coherence

for b_{1} being Element of Components R holds not b_{1} is empty

end;
coherence

for b

proof end;

definition

let R be non empty Poset;

let s1 be Element of R;

correctness

coherence

Class ((Path_Rel R),s1) is Component of R;

by EQREL_1:def 3;

end;
let s1 be Element of R;

correctness

coherence

Class ((Path_Rel R),s1) is Component of R;

by EQREL_1:def 3;

:: deftheorem defines CComp OSALG_4:def 6 :

for R being non empty Poset

for s1 being Element of R holds CComp s1 = Class ((Path_Rel R),s1);

for R being non empty Poset

for s1 being Element of R holds CComp s1 = Class ((Path_Rel R),s1);

definition

let R be non empty Poset;

let A be ManySortedSet of the carrier of R;

let C be Component of R;

coherence

union { (A . s) where s is Element of R : s in C } is set ;

;

end;
let A be ManySortedSet of the carrier of R;

let C be Component of R;

func A -carrier_of C -> set equals :: OSALG_4:def 7

union { (A . s) where s is Element of R : s in C } ;

correctness union { (A . s) where s is Element of R : s in C } ;

coherence

union { (A . s) where s is Element of R : s in C } is set ;

;

:: deftheorem defines -carrier_of OSALG_4:def 7 :

for R being non empty Poset

for A being ManySortedSet of the carrier of R

for C being Component of R holds A -carrier_of C = union { (A . s) where s is Element of R : s in C } ;

for R being non empty Poset

for A being ManySortedSet of the carrier of R

for C being Component of R holds A -carrier_of C = union { (A . s) where s is Element of R : s in C } ;

theorem Th5: :: OSALG_4:5

for R being non empty Poset

for A being ManySortedSet of the carrier of R

for s being Element of R

for x being set st x in A . s holds

x in A -carrier_of (CComp s)

for A being ManySortedSet of the carrier of R

for s being Element of R

for x being set st x in A . s holds

x in A -carrier_of (CComp s)

proof end;

definition

let R be non empty Poset;

end;
attr R is locally_directed means :Def8: :: OSALG_4:def 8

for C being Component of R holds C is directed ;

for C being Component of R holds C is directed ;

:: deftheorem Def8 defines locally_directed OSALG_4:def 8 :

for R being non empty Poset holds

( R is locally_directed iff for C being Component of R holds C is directed );

for R being non empty Poset holds

( R is locally_directed iff for C being Component of R holds C is directed );

:: the system could generate this one from the following

registration

ex b_{1} being OrderSortedSign st b_{1} is locally_directed
end;

cluster non empty non void V80() reflexive transitive antisymmetric order-sorted discernable locally_directed for OverloadedRSSign ;

existence ex b

proof end;

registration

for b_{1} being non empty Poset st b_{1} is discrete holds

b_{1} is locally_directed
by Th8;

end;

cluster non empty reflexive transitive antisymmetric discrete -> non empty locally_directed for RelStr ;

coherence for b

b

registration

let S be non empty locally_directed Poset;

coherence

for b_{1} being Component of S holds b_{1} is directed
by Def8;

end;
coherence

for b

:: Much of what follows can be done generally for OrderSortedRelations

:: of OrderSortedSets (and not just OrderSortedRelations of OSAlgebras),

:: unfortunately, multiple inheritence would be needed to widen the

:: latter to the former

:: Classes on connected components

:: of OrderSortedSets (and not just OrderSortedRelations of OSAlgebras),

:: unfortunately, multiple inheritence would be needed to widen the

:: latter to the former

:: Classes on connected components

definition

let S be locally_directed OrderSortedSign;

let A be OSAlgebra of S;

let E be MSEquivalence-like OrderSortedRelation of A;

let C be Component of S;

ex b_{1} being Equivalence_Relation of ( the Sorts of A -carrier_of C) st

for x, y being object holds

( [x,y] in b_{1} iff ex s1 being Element of S st

( s1 in C & [x,y] in E . s1 ) )

for b_{1}, b_{2} being Equivalence_Relation of ( the Sorts of A -carrier_of C) st ( for x, y being object holds

( [x,y] in b_{1} iff ex s1 being Element of S st

( s1 in C & [x,y] in E . s1 ) ) ) & ( for x, y being object holds

( [x,y] in b_{2} iff ex s1 being Element of S st

( s1 in C & [x,y] in E . s1 ) ) ) holds

b_{1} = b_{2}

end;
let A be OSAlgebra of S;

let E be MSEquivalence-like OrderSortedRelation of A;

let C be Component of S;

func CompClass (E,C) -> Equivalence_Relation of ( the Sorts of A -carrier_of C) means :Def9: :: OSALG_4:def 9

for x, y being object holds

( [x,y] in it iff ex s1 being Element of S st

( s1 in C & [x,y] in E . s1 ) );

existence for x, y being object holds

( [x,y] in it iff ex s1 being Element of S st

( s1 in C & [x,y] in E . s1 ) );

ex b

for x, y being object holds

( [x,y] in b

( s1 in C & [x,y] in E . s1 ) )

proof end;

uniqueness for b

( [x,y] in b

( s1 in C & [x,y] in E . s1 ) ) ) & ( for x, y being object holds

( [x,y] in b

( s1 in C & [x,y] in E . s1 ) ) ) holds

b

proof end;

:: deftheorem Def9 defines CompClass OSALG_4:def 9 :

for S being locally_directed OrderSortedSign

for A being OSAlgebra of S

for E being MSEquivalence-like OrderSortedRelation of A

for C being Component of S

for b_{5} being Equivalence_Relation of ( the Sorts of A -carrier_of C) holds

( b_{5} = CompClass (E,C) iff for x, y being object holds

( [x,y] in b_{5} iff ex s1 being Element of S st

( s1 in C & [x,y] in E . s1 ) ) );

for S being locally_directed OrderSortedSign

for A being OSAlgebra of S

for E being MSEquivalence-like OrderSortedRelation of A

for C being Component of S

for b

( b

( [x,y] in b

( s1 in C & [x,y] in E . s1 ) ) );

:: we could give a name to Class CompClass(E,C)

:: restriction of Class CompClass(E,C) to A.s1

:: restriction of Class CompClass(E,C) to A.s1

definition

let S be locally_directed OrderSortedSign;

let A be OSAlgebra of S;

let E be MSEquivalence-like OrderSortedRelation of A;

let s1 be Element of S;

ex b_{1} being Subset of (Class (CompClass (E,(CComp s1)))) st

for z being set holds

( z in b_{1} iff ex x being set st

( x in the Sorts of A . s1 & z = Class ((CompClass (E,(CComp s1))),x) ) )

for b_{1}, b_{2} being Subset of (Class (CompClass (E,(CComp s1)))) st ( for z being set holds

( z in b_{1} iff ex x being set st

( x in the Sorts of A . s1 & z = Class ((CompClass (E,(CComp s1))),x) ) ) ) & ( for z being set holds

( z in b_{2} iff ex x being set st

( x in the Sorts of A . s1 & z = Class ((CompClass (E,(CComp s1))),x) ) ) ) holds

b_{1} = b_{2}

end;
let A be OSAlgebra of S;

let E be MSEquivalence-like OrderSortedRelation of A;

let s1 be Element of S;

func OSClass (E,s1) -> Subset of (Class (CompClass (E,(CComp s1)))) means :Def10: :: OSALG_4:def 10

for z being set holds

( z in it iff ex x being set st

( x in the Sorts of A . s1 & z = Class ((CompClass (E,(CComp s1))),x) ) );

existence for z being set holds

( z in it iff ex x being set st

( x in the Sorts of A . s1 & z = Class ((CompClass (E,(CComp s1))),x) ) );

ex b

for z being set holds

( z in b

( x in the Sorts of A . s1 & z = Class ((CompClass (E,(CComp s1))),x) ) )

proof end;

uniqueness for b

( z in b

( x in the Sorts of A . s1 & z = Class ((CompClass (E,(CComp s1))),x) ) ) ) & ( for z being set holds

( z in b

( x in the Sorts of A . s1 & z = Class ((CompClass (E,(CComp s1))),x) ) ) ) holds

b

proof end;

:: deftheorem Def10 defines OSClass OSALG_4:def 10 :

for S being locally_directed OrderSortedSign

for A being OSAlgebra of S

for E being MSEquivalence-like OrderSortedRelation of A

for s1 being Element of S

for b_{5} being Subset of (Class (CompClass (E,(CComp s1)))) holds

( b_{5} = OSClass (E,s1) iff for z being set holds

( z in b_{5} iff ex x being set st

( x in the Sorts of A . s1 & z = Class ((CompClass (E,(CComp s1))),x) ) ) );

for S being locally_directed OrderSortedSign

for A being OSAlgebra of S

for E being MSEquivalence-like OrderSortedRelation of A

for s1 being Element of S

for b

( b

( z in b

( x in the Sorts of A . s1 & z = Class ((CompClass (E,(CComp s1))),x) ) ) );

registration

let S be locally_directed OrderSortedSign;

let A be non-empty OSAlgebra of S;

let E be MSEquivalence-like OrderSortedRelation of A;

let s1 be Element of S;

coherence

not OSClass (E,s1) is empty

end;
let A be non-empty OSAlgebra of S;

let E be MSEquivalence-like OrderSortedRelation of A;

let s1 be Element of S;

coherence

not OSClass (E,s1) is empty

proof end;

theorem Th10: :: OSALG_4:10

for S being locally_directed OrderSortedSign

for A being OSAlgebra of S

for E being MSEquivalence-like OrderSortedRelation of A

for s1, s2 being Element of S st s1 <= s2 holds

OSClass (E,s1) c= OSClass (E,s2)

for A being OSAlgebra of S

for E being MSEquivalence-like OrderSortedRelation of A

for s1, s2 being Element of S st s1 <= s2 holds

OSClass (E,s1) c= OSClass (E,s2)

proof end;

:: finally, this is analogy of the Many-Sorted Class E for order-sorted E

:: this definition should work for order-sorted MSCongruence too

:: if non-empty not needed, prove the following cluster

:: this definition should work for order-sorted MSCongruence too

:: if non-empty not needed, prove the following cluster

definition

let S be locally_directed OrderSortedSign;

let A be OSAlgebra of S;

let E be MSEquivalence-like OrderSortedRelation of A;

ex b_{1} being OrderSortedSet of S st

for s1 being Element of S holds b_{1} . s1 = OSClass (E,s1)

for b_{1}, b_{2} being OrderSortedSet of S st ( for s1 being Element of S holds b_{1} . s1 = OSClass (E,s1) ) & ( for s1 being Element of S holds b_{2} . s1 = OSClass (E,s1) ) holds

b_{1} = b_{2}

end;
let A be OSAlgebra of S;

let E be MSEquivalence-like OrderSortedRelation of A;

func OSClass E -> OrderSortedSet of S means :Def11: :: OSALG_4:def 11

for s1 being Element of S holds it . s1 = OSClass (E,s1);

existence for s1 being Element of S holds it . s1 = OSClass (E,s1);

ex b

for s1 being Element of S holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def11 defines OSClass OSALG_4:def 11 :

for S being locally_directed OrderSortedSign

for A being OSAlgebra of S

for E being MSEquivalence-like OrderSortedRelation of A

for b_{4} being OrderSortedSet of S holds

( b_{4} = OSClass E iff for s1 being Element of S holds b_{4} . s1 = OSClass (E,s1) );

for S being locally_directed OrderSortedSign

for A being OSAlgebra of S

for E being MSEquivalence-like OrderSortedRelation of A

for b

( b

registration

let S be locally_directed OrderSortedSign;

let A be non-empty OSAlgebra of S;

let E be MSEquivalence-like OrderSortedRelation of A;

coherence

OSClass E is non-empty

end;
let A be non-empty OSAlgebra of S;

let E be MSEquivalence-like OrderSortedRelation of A;

coherence

OSClass E is non-empty

proof end;

:: order-sorted equiv of Class(R,x)

definition

let S be locally_directed OrderSortedSign;

let U1 be non-empty OSAlgebra of S;

let E be MSEquivalence-like OrderSortedRelation of U1;

let s be Element of S;

let x be Element of the Sorts of U1 . s;

coherence

Class ((CompClass (E,(CComp s))),x) is Element of OSClass (E,s);

by Def10;

end;
let U1 be non-empty OSAlgebra of S;

let E be MSEquivalence-like OrderSortedRelation of U1;

let s be Element of S;

let x be Element of the Sorts of U1 . s;

func OSClass (E,x) -> Element of OSClass (E,s) equals :: OSALG_4:def 12

Class ((CompClass (E,(CComp s))),x);

correctness Class ((CompClass (E,(CComp s))),x);

coherence

Class ((CompClass (E,(CComp s))),x) is Element of OSClass (E,s);

by Def10;

:: deftheorem defines OSClass OSALG_4:def 12 :

for S being locally_directed OrderSortedSign

for U1 being non-empty OSAlgebra of S

for E being MSEquivalence-like OrderSortedRelation of U1

for s being Element of S

for x being Element of the Sorts of U1 . s holds OSClass (E,x) = Class ((CompClass (E,(CComp s))),x);

for S being locally_directed OrderSortedSign

for U1 being non-empty OSAlgebra of S

for E being MSEquivalence-like OrderSortedRelation of U1

for s being Element of S

for x being Element of the Sorts of U1 . s holds OSClass (E,x) = Class ((CompClass (E,(CComp s))),x);

theorem :: OSALG_4:11

for R being non empty locally_directed Poset

for x, y being Element of R st ex z being Element of R st

( z <= x & z <= y ) holds

ex u being Element of R st

( x <= u & y <= u )

for x, y being Element of R st ex z being Element of R st

( z <= x & z <= y ) holds

ex u being Element of R st

( x <= u & y <= u )

proof end;

theorem Th12: :: OSALG_4:12

for S being locally_directed OrderSortedSign

for U1 being non-empty OSAlgebra of S

for E being MSEquivalence-like OrderSortedRelation of U1

for s being Element of S

for x, y being Element of the Sorts of U1 . s holds

( OSClass (E,x) = OSClass (E,y) iff [x,y] in E . s )

for U1 being non-empty OSAlgebra of S

for E being MSEquivalence-like OrderSortedRelation of U1

for s being Element of S

for x, y being Element of the Sorts of U1 . s holds

( OSClass (E,x) = OSClass (E,y) iff [x,y] in E . s )

proof end;

theorem :: OSALG_4:13

for S being locally_directed OrderSortedSign

for U1 being non-empty OSAlgebra of S

for E being MSEquivalence-like OrderSortedRelation of U1

for s1, s2 being Element of S

for x being Element of the Sorts of U1 . s1 st s1 <= s2 holds

for y being Element of the Sorts of U1 . s2 st y = x holds

OSClass (E,x) = OSClass (E,y) by Th4;

for U1 being non-empty OSAlgebra of S

for E being MSEquivalence-like OrderSortedRelation of U1

for s1, s2 being Element of S

for x being Element of the Sorts of U1 . s1 st s1 <= s2 holds

for y being Element of the Sorts of U1 . s2 st y = x holds

OSClass (E,x) = OSClass (E,y) by Th4;

:: multiclasses

definition

let S be locally_directed OrderSortedSign;

let o be Element of the carrier' of S;

let A be non-empty OSAlgebra of S;

let R be OSCongruence of A;

let x be Element of Args (o,A);

ex b_{1} being Element of product ((OSClass R) * (the_arity_of o)) st

for n being Nat st n in dom (the_arity_of o) holds

ex y being Element of the Sorts of A . ((the_arity_of o) /. n) st

( y = x . n & b_{1} . n = OSClass (R,y) )

for b_{1}, b_{2} being Element of product ((OSClass R) * (the_arity_of o)) st ( for n being Nat st n in dom (the_arity_of o) holds

ex y being Element of the Sorts of A . ((the_arity_of o) /. n) st

( y = x . n & b_{1} . n = OSClass (R,y) ) ) & ( for n being Nat st n in dom (the_arity_of o) holds

ex y being Element of the Sorts of A . ((the_arity_of o) /. n) st

( y = x . n & b_{2} . n = OSClass (R,y) ) ) holds

b_{1} = b_{2}

end;
let o be Element of the carrier' of S;

let A be non-empty OSAlgebra of S;

let R be OSCongruence of A;

let x be Element of Args (o,A);

func R #_os x -> Element of product ((OSClass R) * (the_arity_of o)) means :Def13: :: OSALG_4:def 13

for n being Nat st n in dom (the_arity_of o) holds

ex y being Element of the Sorts of A . ((the_arity_of o) /. n) st

( y = x . n & it . n = OSClass (R,y) );

existence for n being Nat st n in dom (the_arity_of o) holds

ex y being Element of the Sorts of A . ((the_arity_of o) /. n) st

( y = x . n & it . n = OSClass (R,y) );

ex b

for n being Nat st n in dom (the_arity_of o) holds

ex y being Element of the Sorts of A . ((the_arity_of o) /. n) st

( y = x . n & b

proof end;

uniqueness for b

ex y being Element of the Sorts of A . ((the_arity_of o) /. n) st

( y = x . n & b

ex y being Element of the Sorts of A . ((the_arity_of o) /. n) st

( y = x . n & b

b

proof end;

:: deftheorem Def13 defines #_os OSALG_4:def 13 :

for S being locally_directed OrderSortedSign

for o being Element of the carrier' of S

for A being non-empty OSAlgebra of S

for R being OSCongruence of A

for x being Element of Args (o,A)

for b_{6} being Element of product ((OSClass R) * (the_arity_of o)) holds

( b_{6} = R #_os x iff for n being Nat st n in dom (the_arity_of o) holds

ex y being Element of the Sorts of A . ((the_arity_of o) /. n) st

( y = x . n & b_{6} . n = OSClass (R,y) ) );

for S being locally_directed OrderSortedSign

for o being Element of the carrier' of S

for A being non-empty OSAlgebra of S

for R being OSCongruence of A

for x being Element of Args (o,A)

for b

( b

ex y being Element of the Sorts of A . ((the_arity_of o) /. n) st

( y = x . n & b

:: the quotient will be different for order-sorted;

:: this def seems ok for order-sorted

:: this def seems ok for order-sorted

definition

let S be locally_directed OrderSortedSign;

let o be Element of the carrier' of S;

let A be non-empty OSAlgebra of S;

let R be OSCongruence of A;

ex b_{1} being Function of (( the Sorts of A * the ResultSort of S) . o),(((OSClass R) * the ResultSort of S) . o) st

for x being Element of the Sorts of A . (the_result_sort_of o) holds b_{1} . x = OSClass (R,x)

for b_{1}, b_{2} being Function of (( the Sorts of A * the ResultSort of S) . o),(((OSClass R) * the ResultSort of S) . o) st ( for x being Element of the Sorts of A . (the_result_sort_of o) holds b_{1} . x = OSClass (R,x) ) & ( for x being Element of the Sorts of A . (the_result_sort_of o) holds b_{2} . x = OSClass (R,x) ) holds

b_{1} = b_{2}

ex b_{1} being Function of ((( the Sorts of A #) * the Arity of S) . o),((((OSClass R) #) * the Arity of S) . o) st

for x being Element of Args (o,A) holds b_{1} . x = R #_os x

for b_{1}, b_{2} being Function of ((( the Sorts of A #) * the Arity of S) . o),((((OSClass R) #) * the Arity of S) . o) st ( for x being Element of Args (o,A) holds b_{1} . x = R #_os x ) & ( for x being Element of Args (o,A) holds b_{2} . x = R #_os x ) holds

b_{1} = b_{2}

end;
let o be Element of the carrier' of S;

let A be non-empty OSAlgebra of S;

let R be OSCongruence of A;

func OSQuotRes (R,o) -> Function of (( the Sorts of A * the ResultSort of S) . o),(((OSClass R) * the ResultSort of S) . o) means :Def14: :: OSALG_4:def 14

for x being Element of the Sorts of A . (the_result_sort_of o) holds it . x = OSClass (R,x);

existence for x being Element of the Sorts of A . (the_result_sort_of o) holds it . x = OSClass (R,x);

ex b

for x being Element of the Sorts of A . (the_result_sort_of o) holds b

proof end;

uniqueness for b

b

proof end;

func OSQuotArgs (R,o) -> Function of ((( the Sorts of A #) * the Arity of S) . o),((((OSClass R) #) * the Arity of S) . o) means :: OSALG_4:def 15

for x being Element of Args (o,A) holds it . x = R #_os x;

existence for x being Element of Args (o,A) holds it . x = R #_os x;

ex b

for x being Element of Args (o,A) holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def14 defines OSQuotRes OSALG_4:def 14 :

for S being locally_directed OrderSortedSign

for o being Element of the carrier' of S

for A being non-empty OSAlgebra of S

for R being OSCongruence of A

for b_{5} being Function of (( the Sorts of A * the ResultSort of S) . o),(((OSClass R) * the ResultSort of S) . o) holds

( b_{5} = OSQuotRes (R,o) iff for x being Element of the Sorts of A . (the_result_sort_of o) holds b_{5} . x = OSClass (R,x) );

for S being locally_directed OrderSortedSign

for o being Element of the carrier' of S

for A being non-empty OSAlgebra of S

for R being OSCongruence of A

for b

( b

:: deftheorem defines OSQuotArgs OSALG_4:def 15 :

for S being locally_directed OrderSortedSign

for o being Element of the carrier' of S

for A being non-empty OSAlgebra of S

for R being OSCongruence of A

for b_{5} being Function of ((( the Sorts of A #) * the Arity of S) . o),((((OSClass R) #) * the Arity of S) . o) holds

( b_{5} = OSQuotArgs (R,o) iff for x being Element of Args (o,A) holds b_{5} . x = R #_os x );

for S being locally_directed OrderSortedSign

for o being Element of the carrier' of S

for A being non-empty OSAlgebra of S

for R being OSCongruence of A

for b

( b

definition

let S be locally_directed OrderSortedSign;

let A be non-empty OSAlgebra of S;

let R be OSCongruence of A;

ex b_{1} being ManySortedFunction of the Sorts of A * the ResultSort of S,(OSClass R) * the ResultSort of S st

for o being OperSymbol of S holds b_{1} . o = OSQuotRes (R,o)

for b_{1}, b_{2} being ManySortedFunction of the Sorts of A * the ResultSort of S,(OSClass R) * the ResultSort of S st ( for o being OperSymbol of S holds b_{1} . o = OSQuotRes (R,o) ) & ( for o being OperSymbol of S holds b_{2} . o = OSQuotRes (R,o) ) holds

b_{1} = b_{2}

ex b_{1} being ManySortedFunction of ( the Sorts of A #) * the Arity of S,((OSClass R) #) * the Arity of S st

for o being OperSymbol of S holds b_{1} . o = OSQuotArgs (R,o)

for b_{1}, b_{2} being ManySortedFunction of ( the Sorts of A #) * the Arity of S,((OSClass R) #) * the Arity of S st ( for o being OperSymbol of S holds b_{1} . o = OSQuotArgs (R,o) ) & ( for o being OperSymbol of S holds b_{2} . o = OSQuotArgs (R,o) ) holds

b_{1} = b_{2}

end;
let A be non-empty OSAlgebra of S;

let R be OSCongruence of A;

func OSQuotRes R -> ManySortedFunction of the Sorts of A * the ResultSort of S,(OSClass R) * the ResultSort of S means :: OSALG_4:def 16

for o being OperSymbol of S holds it . o = OSQuotRes (R,o);

existence for o being OperSymbol of S holds it . o = OSQuotRes (R,o);

ex b

for o being OperSymbol of S holds b

proof end;

uniqueness for b

b

proof end;

func OSQuotArgs R -> ManySortedFunction of ( the Sorts of A #) * the Arity of S,((OSClass R) #) * the Arity of S means :: OSALG_4:def 17

for o being OperSymbol of S holds it . o = OSQuotArgs (R,o);

existence for o being OperSymbol of S holds it . o = OSQuotArgs (R,o);

ex b

for o being OperSymbol of S holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem defines OSQuotRes OSALG_4:def 16 :

for S being locally_directed OrderSortedSign

for A being non-empty OSAlgebra of S

for R being OSCongruence of A

for b_{4} being ManySortedFunction of the Sorts of A * the ResultSort of S,(OSClass R) * the ResultSort of S holds

( b_{4} = OSQuotRes R iff for o being OperSymbol of S holds b_{4} . o = OSQuotRes (R,o) );

for S being locally_directed OrderSortedSign

for A being non-empty OSAlgebra of S

for R being OSCongruence of A

for b

( b

:: deftheorem defines OSQuotArgs OSALG_4:def 17 :

for S being locally_directed OrderSortedSign

for A being non-empty OSAlgebra of S

for R being OSCongruence of A

for b_{4} being ManySortedFunction of ( the Sorts of A #) * the Arity of S,((OSClass R) #) * the Arity of S holds

( b_{4} = OSQuotArgs R iff for o being OperSymbol of S holds b_{4} . o = OSQuotArgs (R,o) );

for S being locally_directed OrderSortedSign

for A being non-empty OSAlgebra of S

for R being OSCongruence of A

for b

( b

theorem Th14: :: OSALG_4:14

for S being locally_directed OrderSortedSign

for o being Element of the carrier' of S

for A being non-empty OSAlgebra of S

for R being OSCongruence of A

for x being set st x in (((OSClass R) #) * the Arity of S) . o holds

ex a being Element of Args (o,A) st x = R #_os a

for o being Element of the carrier' of S

for A being non-empty OSAlgebra of S

for R being OSCongruence of A

for x being set st x in (((OSClass R) #) * the Arity of S) . o holds

ex a being Element of Args (o,A) st x = R #_os a

proof end;

definition

let S be locally_directed OrderSortedSign;

let o be Element of the carrier' of S;

let A be non-empty OSAlgebra of S;

let R be OSCongruence of A;

ex b_{1} being Function of ((((OSClass R) #) * the Arity of S) . o),(((OSClass R) * the ResultSort of S) . o) st

for a being Element of Args (o,A) st R #_os a in (((OSClass R) #) * the Arity of S) . o holds

b_{1} . (R #_os a) = ((OSQuotRes (R,o)) * (Den (o,A))) . a

for b_{1}, b_{2} being Function of ((((OSClass R) #) * the Arity of S) . o),(((OSClass R) * the ResultSort of S) . o) st ( for a being Element of Args (o,A) st R #_os a in (((OSClass R) #) * the Arity of S) . o holds

b_{1} . (R #_os a) = ((OSQuotRes (R,o)) * (Den (o,A))) . a ) & ( for a being Element of Args (o,A) st R #_os a in (((OSClass R) #) * the Arity of S) . o holds

b_{2} . (R #_os a) = ((OSQuotRes (R,o)) * (Den (o,A))) . a ) holds

b_{1} = b_{2}

end;
let o be Element of the carrier' of S;

let A be non-empty OSAlgebra of S;

let R be OSCongruence of A;

func OSQuotCharact (R,o) -> Function of ((((OSClass R) #) * the Arity of S) . o),(((OSClass R) * the ResultSort of S) . o) means :Def18: :: OSALG_4:def 18

for a being Element of Args (o,A) st R #_os a in (((OSClass R) #) * the Arity of S) . o holds

it . (R #_os a) = ((OSQuotRes (R,o)) * (Den (o,A))) . a;

existence for a being Element of Args (o,A) st R #_os a in (((OSClass R) #) * the Arity of S) . o holds

it . (R #_os a) = ((OSQuotRes (R,o)) * (Den (o,A))) . a;

ex b

for a being Element of Args (o,A) st R #_os a in (((OSClass R) #) * the Arity of S) . o holds

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def18 defines OSQuotCharact OSALG_4:def 18 :

for S being locally_directed OrderSortedSign

for o being Element of the carrier' of S

for A being non-empty OSAlgebra of S

for R being OSCongruence of A

for b_{5} being Function of ((((OSClass R) #) * the Arity of S) . o),(((OSClass R) * the ResultSort of S) . o) holds

( b_{5} = OSQuotCharact (R,o) iff for a being Element of Args (o,A) st R #_os a in (((OSClass R) #) * the Arity of S) . o holds

b_{5} . (R #_os a) = ((OSQuotRes (R,o)) * (Den (o,A))) . a );

for S being locally_directed OrderSortedSign

for o being Element of the carrier' of S

for A being non-empty OSAlgebra of S

for R being OSCongruence of A

for b

( b

b

definition

let S be locally_directed OrderSortedSign;

let A be non-empty OSAlgebra of S;

let R be OSCongruence of A;

ex b_{1} being ManySortedFunction of ((OSClass R) #) * the Arity of S,(OSClass R) * the ResultSort of S st

for o being OperSymbol of S holds b_{1} . o = OSQuotCharact (R,o)

for b_{1}, b_{2} being ManySortedFunction of ((OSClass R) #) * the Arity of S,(OSClass R) * the ResultSort of S st ( for o being OperSymbol of S holds b_{1} . o = OSQuotCharact (R,o) ) & ( for o being OperSymbol of S holds b_{2} . o = OSQuotCharact (R,o) ) holds

b_{1} = b_{2}

end;
let A be non-empty OSAlgebra of S;

let R be OSCongruence of A;

func OSQuotCharact R -> ManySortedFunction of ((OSClass R) #) * the Arity of S,(OSClass R) * the ResultSort of S means :Def19: :: OSALG_4:def 19

for o being OperSymbol of S holds it . o = OSQuotCharact (R,o);

existence for o being OperSymbol of S holds it . o = OSQuotCharact (R,o);

ex b

for o being OperSymbol of S holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def19 defines OSQuotCharact OSALG_4:def 19 :

for S being locally_directed OrderSortedSign

for A being non-empty OSAlgebra of S

for R being OSCongruence of A

for b_{4} being ManySortedFunction of ((OSClass R) #) * the Arity of S,(OSClass R) * the ResultSort of S holds

( b_{4} = OSQuotCharact R iff for o being OperSymbol of S holds b_{4} . o = OSQuotCharact (R,o) );

for S being locally_directed OrderSortedSign

for A being non-empty OSAlgebra of S

for R being OSCongruence of A

for b

( b

definition

let S be locally_directed OrderSortedSign;

let U1 be non-empty OSAlgebra of S;

let R be OSCongruence of U1;

MSAlgebra(# (OSClass R),(OSQuotCharact R) #) is OSAlgebra of S by OSALG_1:17;

end;
let U1 be non-empty OSAlgebra of S;

let R be OSCongruence of U1;

func QuotOSAlg (U1,R) -> OSAlgebra of S equals :: OSALG_4:def 20

MSAlgebra(# (OSClass R),(OSQuotCharact R) #);

coherence MSAlgebra(# (OSClass R),(OSQuotCharact R) #);

MSAlgebra(# (OSClass R),(OSQuotCharact R) #) is OSAlgebra of S by OSALG_1:17;

:: deftheorem defines QuotOSAlg OSALG_4:def 20 :

for S being locally_directed OrderSortedSign

for U1 being non-empty OSAlgebra of S

for R being OSCongruence of U1 holds QuotOSAlg (U1,R) = MSAlgebra(# (OSClass R),(OSQuotCharact R) #);

for S being locally_directed OrderSortedSign

for U1 being non-empty OSAlgebra of S

for R being OSCongruence of U1 holds QuotOSAlg (U1,R) = MSAlgebra(# (OSClass R),(OSQuotCharact R) #);

:: we could note that for discrete the QuotOSAlg and QuotMsAlg are equal

registration

let S be locally_directed OrderSortedSign;

let U1 be non-empty OSAlgebra of S;

let R be OSCongruence of U1;

coherence

( QuotOSAlg (U1,R) is strict & QuotOSAlg (U1,R) is non-empty ) by MSUALG_1:def 3;

end;
let U1 be non-empty OSAlgebra of S;

let R be OSCongruence of U1;

coherence

( QuotOSAlg (U1,R) is strict & QuotOSAlg (U1,R) is non-empty ) by MSUALG_1:def 3;

definition

let S be locally_directed OrderSortedSign;

let U1 be non-empty OSAlgebra of S;

let R be OSCongruence of U1;

let s be Element of S;

ex b_{1} being Function of ( the Sorts of U1 . s),(OSClass (R,s)) st

for x being Element of the Sorts of U1 . s holds b_{1} . x = OSClass (R,x)

for b_{1}, b_{2} being Function of ( the Sorts of U1 . s),(OSClass (R,s)) st ( for x being Element of the Sorts of U1 . s holds b_{1} . x = OSClass (R,x) ) & ( for x being Element of the Sorts of U1 . s holds b_{2} . x = OSClass (R,x) ) holds

b_{1} = b_{2}

end;
let U1 be non-empty OSAlgebra of S;

let R be OSCongruence of U1;

let s be Element of S;

func OSNat_Hom (U1,R,s) -> Function of ( the Sorts of U1 . s),(OSClass (R,s)) means :Def21: :: OSALG_4:def 21

for x being Element of the Sorts of U1 . s holds it . x = OSClass (R,x);

existence for x being Element of the Sorts of U1 . s holds it . x = OSClass (R,x);

ex b

for x being Element of the Sorts of U1 . s holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def21 defines OSNat_Hom OSALG_4:def 21 :

for S being locally_directed OrderSortedSign

for U1 being non-empty OSAlgebra of S

for R being OSCongruence of U1

for s being Element of S

for b_{5} being Function of ( the Sorts of U1 . s),(OSClass (R,s)) holds

( b_{5} = OSNat_Hom (U1,R,s) iff for x being Element of the Sorts of U1 . s holds b_{5} . x = OSClass (R,x) );

for S being locally_directed OrderSortedSign

for U1 being non-empty OSAlgebra of S

for R being OSCongruence of U1

for s being Element of S

for b

( b

definition

let S be locally_directed OrderSortedSign;

let U1 be non-empty OSAlgebra of S;

let R be OSCongruence of U1;

ex b_{1} being ManySortedFunction of U1,(QuotOSAlg (U1,R)) st

for s being Element of S holds b_{1} . s = OSNat_Hom (U1,R,s)

for b_{1}, b_{2} being ManySortedFunction of U1,(QuotOSAlg (U1,R)) st ( for s being Element of S holds b_{1} . s = OSNat_Hom (U1,R,s) ) & ( for s being Element of S holds b_{2} . s = OSNat_Hom (U1,R,s) ) holds

b_{1} = b_{2}

end;
let U1 be non-empty OSAlgebra of S;

let R be OSCongruence of U1;

func OSNat_Hom (U1,R) -> ManySortedFunction of U1,(QuotOSAlg (U1,R)) means :Def22: :: OSALG_4:def 22

for s being Element of S holds it . s = OSNat_Hom (U1,R,s);

existence for s being Element of S holds it . s = OSNat_Hom (U1,R,s);

ex b

for s being Element of S holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def22 defines OSNat_Hom OSALG_4:def 22 :

for S being locally_directed OrderSortedSign

for U1 being non-empty OSAlgebra of S

for R being OSCongruence of U1

for b_{4} being ManySortedFunction of U1,(QuotOSAlg (U1,R)) holds

( b_{4} = OSNat_Hom (U1,R) iff for s being Element of S holds b_{4} . s = OSNat_Hom (U1,R,s) );

for S being locally_directed OrderSortedSign

for U1 being non-empty OSAlgebra of S

for R being OSCongruence of U1

for b

( b

theorem :: OSALG_4:15

for S being locally_directed OrderSortedSign

for U1 being non-empty OSAlgebra of S

for R being OSCongruence of U1 holds

( OSNat_Hom (U1,R) is_epimorphism U1, QuotOSAlg (U1,R) & OSNat_Hom (U1,R) is order-sorted )

for U1 being non-empty OSAlgebra of S

for R being OSCongruence of U1 holds

( OSNat_Hom (U1,R) is_epimorphism U1, QuotOSAlg (U1,R) & OSNat_Hom (U1,R) is order-sorted )

proof end;

theorem Th16: :: OSALG_4:16

for S being locally_directed OrderSortedSign

for U1, U2 being non-empty OSAlgebra of S

for F being ManySortedFunction of U1,U2 st F is_homomorphism U1,U2 & F is order-sorted holds

MSCng F is OSCongruence of U1

for U1, U2 being non-empty OSAlgebra of S

for F being ManySortedFunction of U1,U2 st F is_homomorphism U1,U2 & F is order-sorted holds

MSCng F is OSCongruence of U1

proof end;

:: just a casting func, currently no other way how to employ the type system

definition

let S be locally_directed OrderSortedSign;

let U1, U2 be non-empty OSAlgebra of S;

let F be ManySortedFunction of U1,U2;

assume A1: ( F is_homomorphism U1,U2 & F is order-sorted ) ;

correctness

coherence

MSCng F is OSCongruence of U1;

by A1, Th16;

end;
let U1, U2 be non-empty OSAlgebra of S;

let F be ManySortedFunction of U1,U2;

assume A1: ( F is_homomorphism U1,U2 & F is order-sorted ) ;

correctness

coherence

MSCng F is OSCongruence of U1;

by A1, Th16;

:: deftheorem Def23 defines OSCng OSALG_4:def 23 :

for S being locally_directed OrderSortedSign

for U1, U2 being non-empty OSAlgebra of S

for F being ManySortedFunction of U1,U2 st F is_homomorphism U1,U2 & F is order-sorted holds

OSCng F = MSCng F;

for S being locally_directed OrderSortedSign

for U1, U2 being non-empty OSAlgebra of S

for F being ManySortedFunction of U1,U2 st F is_homomorphism U1,U2 & F is order-sorted holds

OSCng F = MSCng F;

definition

let S be locally_directed OrderSortedSign;

let U1, U2 be non-empty OSAlgebra of S;

let F be ManySortedFunction of U1,U2;

let s be Element of S;

assume that

A1: F is_homomorphism U1,U2 and

A2: F is order-sorted ;

ex b_{1} being Function of ( the Sorts of (QuotOSAlg (U1,(OSCng F))) . s),( the Sorts of U2 . s) st

for x being Element of the Sorts of U1 . s holds b_{1} . (OSClass ((OSCng F),x)) = (F . s) . x

for b_{1}, b_{2} being Function of ( the Sorts of (QuotOSAlg (U1,(OSCng F))) . s),( the Sorts of U2 . s) st ( for x being Element of the Sorts of U1 . s holds b_{1} . (OSClass ((OSCng F),x)) = (F . s) . x ) & ( for x being Element of the Sorts of U1 . s holds b_{2} . (OSClass ((OSCng F),x)) = (F . s) . x ) holds

b_{1} = b_{2}

end;
let U1, U2 be non-empty OSAlgebra of S;

let F be ManySortedFunction of U1,U2;

let s be Element of S;

assume that

A1: F is_homomorphism U1,U2 and

A2: F is order-sorted ;

func OSHomQuot (F,s) -> Function of ( the Sorts of (QuotOSAlg (U1,(OSCng F))) . s),( the Sorts of U2 . s) means :Def24: :: OSALG_4:def 24

for x being Element of the Sorts of U1 . s holds it . (OSClass ((OSCng F),x)) = (F . s) . x;

existence for x being Element of the Sorts of U1 . s holds it . (OSClass ((OSCng F),x)) = (F . s) . x;

ex b

for x being Element of the Sorts of U1 . s holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def24 defines OSHomQuot OSALG_4:def 24 :

for S being locally_directed OrderSortedSign

for U1, U2 being non-empty OSAlgebra of S

for F being ManySortedFunction of U1,U2

for s being Element of S st F is_homomorphism U1,U2 & F is order-sorted holds

for b_{6} being Function of ( the Sorts of (QuotOSAlg (U1,(OSCng F))) . s),( the Sorts of U2 . s) holds

( b_{6} = OSHomQuot (F,s) iff for x being Element of the Sorts of U1 . s holds b_{6} . (OSClass ((OSCng F),x)) = (F . s) . x );

for S being locally_directed OrderSortedSign

for U1, U2 being non-empty OSAlgebra of S

for F being ManySortedFunction of U1,U2

for s being Element of S st F is_homomorphism U1,U2 & F is order-sorted holds

for b

( b

:: this seems a bit too permissive, but same as the original

:: we should assume F order-sorted probably

:: we should assume F order-sorted probably

definition

let S be locally_directed OrderSortedSign;

let U1, U2 be non-empty OSAlgebra of S;

let F be ManySortedFunction of U1,U2;

ex b_{1} being ManySortedFunction of (QuotOSAlg (U1,(OSCng F))),U2 st

for s being Element of S holds b_{1} . s = OSHomQuot (F,s)

for b_{1}, b_{2} being ManySortedFunction of (QuotOSAlg (U1,(OSCng F))),U2 st ( for s being Element of S holds b_{1} . s = OSHomQuot (F,s) ) & ( for s being Element of S holds b_{2} . s = OSHomQuot (F,s) ) holds

b_{1} = b_{2}

end;
let U1, U2 be non-empty OSAlgebra of S;

let F be ManySortedFunction of U1,U2;

func OSHomQuot F -> ManySortedFunction of (QuotOSAlg (U1,(OSCng F))),U2 means :Def25: :: OSALG_4:def 25

for s being Element of S holds it . s = OSHomQuot (F,s);

existence for s being Element of S holds it . s = OSHomQuot (F,s);

ex b

for s being Element of S holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def25 defines OSHomQuot OSALG_4:def 25 :

for S being locally_directed OrderSortedSign

for U1, U2 being non-empty OSAlgebra of S

for F being ManySortedFunction of U1,U2

for b_{5} being ManySortedFunction of (QuotOSAlg (U1,(OSCng F))),U2 holds

( b_{5} = OSHomQuot F iff for s being Element of S holds b_{5} . s = OSHomQuot (F,s) );

for S being locally_directed OrderSortedSign

for U1, U2 being non-empty OSAlgebra of S

for F being ManySortedFunction of U1,U2

for b

( b

theorem Th17: :: OSALG_4:17

for S being locally_directed OrderSortedSign

for U1, U2 being non-empty OSAlgebra of S

for F being ManySortedFunction of U1,U2 st F is_homomorphism U1,U2 & F is order-sorted holds

( OSHomQuot F is_monomorphism QuotOSAlg (U1,(OSCng F)),U2 & OSHomQuot F is order-sorted )

for U1, U2 being non-empty OSAlgebra of S

for F being ManySortedFunction of U1,U2 st F is_homomorphism U1,U2 & F is order-sorted holds

( OSHomQuot F is_monomorphism QuotOSAlg (U1,(OSCng F)),U2 & OSHomQuot F is order-sorted )

proof end;

theorem Th18: :: OSALG_4:18

for S being locally_directed OrderSortedSign

for U1, U2 being non-empty OSAlgebra of S

for F being ManySortedFunction of U1,U2 st F is_epimorphism U1,U2 & F is order-sorted holds

OSHomQuot F is_isomorphism QuotOSAlg (U1,(OSCng F)),U2

for U1, U2 being non-empty OSAlgebra of S

for F being ManySortedFunction of U1,U2 st F is_epimorphism U1,U2 & F is order-sorted holds

OSHomQuot F is_isomorphism QuotOSAlg (U1,(OSCng F)),U2

proof end;

theorem :: OSALG_4:19

for S being locally_directed OrderSortedSign

for U1, U2 being non-empty OSAlgebra of S

for F being ManySortedFunction of U1,U2 st F is_epimorphism U1,U2 & F is order-sorted holds

QuotOSAlg (U1,(OSCng F)),U2 are_isomorphic

for U1, U2 being non-empty OSAlgebra of S

for F being ManySortedFunction of U1,U2 st F is_epimorphism U1,U2 & F is order-sorted holds

QuotOSAlg (U1,(OSCng F)),U2 are_isomorphic

proof end;

:: monotone OSCongruence ... monotonicity is properly stronger

:: than MSCongruence, so we define it more broadly and prove the

:: ccluster then, however if used for other things than OSCongruences

:: the name of the attribute should be changed

:: this condition is nontrivial only for nonmonotone osas (see further),

:: where Den(o1,U1).x1 can differ from Den(o2,U2).x1

:: is OK for constants ... their Args is always {{}}, so o1 <= o2

:: implies for them [Den(o1,U1).{},Den(o2,U1).{}] in R

:: than MSCongruence, so we define it more broadly and prove the

:: ccluster then, however if used for other things than OSCongruences

:: the name of the attribute should be changed

:: this condition is nontrivial only for nonmonotone osas (see further),

:: where Den(o1,U1).x1 can differ from Den(o2,U2).x1

:: is OK for constants ... their Args is always {{}}, so o1 <= o2

:: implies for them [Den(o1,U1).{},Den(o2,U1).{}] in R

definition

let S be OrderSortedSign;

let U1 be non-empty OSAlgebra of S;

let R be MSEquivalence-like OrderSortedRelation of U1;

end;
let U1 be non-empty OSAlgebra of S;

let R be MSEquivalence-like OrderSortedRelation of U1;

attr R is monotone means :Def26: :: OSALG_4:def 26

for o1, o2 being OperSymbol of S st o1 <= o2 holds

for x1 being Element of Args (o1,U1)

for x2 being Element of Args (o2,U1) st ( for y being Nat st y in dom x1 holds

[(x1 . y),(x2 . y)] in R . ((the_arity_of o2) /. y) ) holds

[((Den (o1,U1)) . x1),((Den (o2,U1)) . x2)] in R . (the_result_sort_of o2);

for o1, o2 being OperSymbol of S st o1 <= o2 holds

for x1 being Element of Args (o1,U1)

for x2 being Element of Args (o2,U1) st ( for y being Nat st y in dom x1 holds

[(x1 . y),(x2 . y)] in R . ((the_arity_of o2) /. y) ) holds

[((Den (o1,U1)) . x1),((Den (o2,U1)) . x2)] in R . (the_result_sort_of o2);

:: deftheorem Def26 defines monotone OSALG_4:def 26 :

for S being OrderSortedSign

for U1 being non-empty OSAlgebra of S

for R being MSEquivalence-like OrderSortedRelation of U1 holds

( R is monotone iff for o1, o2 being OperSymbol of S st o1 <= o2 holds

for x1 being Element of Args (o1,U1)

for x2 being Element of Args (o2,U1) st ( for y being Nat st y in dom x1 holds

[(x1 . y),(x2 . y)] in R . ((the_arity_of o2) /. y) ) holds

[((Den (o1,U1)) . x1),((Den (o2,U1)) . x2)] in R . (the_result_sort_of o2) );

for S being OrderSortedSign

for U1 being non-empty OSAlgebra of S

for R being MSEquivalence-like OrderSortedRelation of U1 holds

( R is monotone iff for o1, o2 being OperSymbol of S st o1 <= o2 holds

for x1 being Element of Args (o1,U1)

for x2 being Element of Args (o2,U1) st ( for y being Nat st y in dom x1 holds

[(x1 . y),(x2 . y)] in R . ((the_arity_of o2) /. y) ) holds

[((Den (o1,U1)) . x1),((Den (o2,U1)) . x2)] in R . (the_result_sort_of o2) );

theorem Th20: :: OSALG_4:20

for S being OrderSortedSign

for U1 being non-empty OSAlgebra of S holds [| the Sorts of U1, the Sorts of U1|] is OSCongruence of U1

for U1 being non-empty OSAlgebra of S holds [| the Sorts of U1, the Sorts of U1|] is OSCongruence of U1

proof end;

theorem Th21: :: OSALG_4:21

for S being OrderSortedSign

for U1 being non-empty OSAlgebra of S

for R being OSCongruence of U1 st R = [| the Sorts of U1, the Sorts of U1|] holds

R is monotone

for U1 being non-empty OSAlgebra of S

for R being OSCongruence of U1 st R = [| the Sorts of U1, the Sorts of U1|] holds

R is monotone

proof end;

registration

let S be OrderSortedSign;

let U1 be non-empty OSAlgebra of S;

ex b_{1} being OSCongruence of U1 st b_{1} is monotone

end;
let U1 be non-empty OSAlgebra of S;

cluster Relation-like the carrier of S -defined non empty Function-like total Relation-yielding MSEquivalence-like MSCongruence-like monotone for OrderSortedRelation of U1;

existence ex b

proof end;

registration

let S be OrderSortedSign;

let U1 be non-empty OSAlgebra of S;

ex b_{1} being MSEquivalence-like OrderSortedRelation of U1 st b_{1} is monotone

end;
let U1 be non-empty OSAlgebra of S;

cluster Relation-like the carrier of S -defined non empty Function-like total Relation-yielding MSEquivalence-like monotone for OrderSortedRelation of U1;

existence ex b

proof end;

theorem Th22: :: OSALG_4:22

for S being OrderSortedSign

for U1 being non-empty OSAlgebra of S

for R being MSEquivalence-like monotone OrderSortedRelation of U1 holds R is MSCongruence-like

for U1 being non-empty OSAlgebra of S

for R being MSEquivalence-like monotone OrderSortedRelation of U1 holds R is MSCongruence-like

proof end;

registration

let S be OrderSortedSign;

let U1 be non-empty OSAlgebra of S;

for b_{1} being MSEquivalence-like OrderSortedRelation of U1 st b_{1} is monotone holds

b_{1} is MSCongruence-like
by Th22;

end;
let U1 be non-empty OSAlgebra of S;

cluster MSEquivalence-like monotone -> MSEquivalence-like MSCongruence-like for OrderSortedRelation of U1;

coherence for b

b

theorem Th23: :: OSALG_4:23

for S being OrderSortedSign

for U1 being non-empty monotone OSAlgebra of S

for R being OSCongruence of U1 holds R is monotone

for U1 being non-empty monotone OSAlgebra of S

for R being OSCongruence of U1 holds R is monotone

proof end;

registration

let S be OrderSortedSign;

let U1 be non-empty monotone OSAlgebra of S;

coherence

for b_{1} being OSCongruence of U1 holds b_{1} is monotone
by Th23;

end;
let U1 be non-empty monotone OSAlgebra of S;

coherence

for b

:: monotonicity of quotient by monotone oscongruence

registration

let S be locally_directed OrderSortedSign;

let U1 be non-empty OSAlgebra of S;

let R be monotone OSCongruence of U1;

coherence

QuotOSAlg (U1,R) is monotone

end;
let U1 be non-empty OSAlgebra of S;

let R be monotone OSCongruence of U1;

coherence

QuotOSAlg (U1,R) is monotone

proof end;

theorem :: OSALG_4:24

for S being locally_directed OrderSortedSign

for U1 being non-empty OSAlgebra of S

for U2 being non-empty monotone OSAlgebra of S

for F being ManySortedFunction of U1,U2 st F is_homomorphism U1,U2 & F is order-sorted holds

OSCng F is monotone

for U1 being non-empty OSAlgebra of S

for U2 being non-empty monotone OSAlgebra of S

for F being ManySortedFunction of U1,U2 st F is_homomorphism U1,U2 & F is order-sorted holds

OSCng F is monotone

proof end;

:: these are a bit more general versions of OSHomQuot, that

:: I need for OSAFREE; more proper way how to do this is restating

:: the MSUALG_9 quotient theorems for OSAs, but that's more work

:: I need for OSAFREE; more proper way how to do this is restating

:: the MSUALG_9 quotient theorems for OSAs, but that's more work

definition

let S be locally_directed OrderSortedSign;

let U1, U2 be non-empty OSAlgebra of S;

let F be ManySortedFunction of U1,U2;

let R be OSCongruence of U1;

let s be Element of S;

assume that

A1: F is_homomorphism U1,U2 and

A2: F is order-sorted and

A3: R c= OSCng F ;

ex b_{1} being Function of ( the Sorts of (QuotOSAlg (U1,R)) . s),( the Sorts of U2 . s) st

for x being Element of the Sorts of U1 . s holds b_{1} . (OSClass (R,x)) = (F . s) . x

for b_{1}, b_{2} being Function of ( the Sorts of (QuotOSAlg (U1,R)) . s),( the Sorts of U2 . s) st ( for x being Element of the Sorts of U1 . s holds b_{1} . (OSClass (R,x)) = (F . s) . x ) & ( for x being Element of the Sorts of U1 . s holds b_{2} . (OSClass (R,x)) = (F . s) . x ) holds

b_{1} = b_{2}

end;
let U1, U2 be non-empty OSAlgebra of S;

let F be ManySortedFunction of U1,U2;

let R be OSCongruence of U1;

let s be Element of S;

assume that

A1: F is_homomorphism U1,U2 and

A2: F is order-sorted and

A3: R c= OSCng F ;

func OSHomQuot (F,R,s) -> Function of ( the Sorts of (QuotOSAlg (U1,R)) . s),( the Sorts of U2 . s) means :Def27: :: OSALG_4:def 27

for x being Element of the Sorts of U1 . s holds it . (OSClass (R,x)) = (F . s) . x;

existence for x being Element of the Sorts of U1 . s holds it . (OSClass (R,x)) = (F . s) . x;

ex b

for x being Element of the Sorts of U1 . s holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def27 defines OSHomQuot OSALG_4:def 27 :

for S being locally_directed OrderSortedSign

for U1, U2 being non-empty OSAlgebra of S

for F being ManySortedFunction of U1,U2

for R being OSCongruence of U1

for s being Element of S st F is_homomorphism U1,U2 & F is order-sorted & R c= OSCng F holds

for b_{7} being Function of ( the Sorts of (QuotOSAlg (U1,R)) . s),( the Sorts of U2 . s) holds

( b_{7} = OSHomQuot (F,R,s) iff for x being Element of the Sorts of U1 . s holds b_{7} . (OSClass (R,x)) = (F . s) . x );

for S being locally_directed OrderSortedSign

for U1, U2 being non-empty OSAlgebra of S

for F being ManySortedFunction of U1,U2

for R being OSCongruence of U1

for s being Element of S st F is_homomorphism U1,U2 & F is order-sorted & R c= OSCng F holds

for b

( b

:: this seems a bit too permissive, but same as the original

:: we should assume F order-sorted probably

:: we should assume F order-sorted probably

definition

let S be locally_directed OrderSortedSign;

let U1, U2 be non-empty OSAlgebra of S;

let F be ManySortedFunction of U1,U2;

let R be OSCongruence of U1;

ex b_{1} being ManySortedFunction of (QuotOSAlg (U1,R)),U2 st

for s being Element of S holds b_{1} . s = OSHomQuot (F,R,s)

for b_{1}, b_{2} being ManySortedFunction of (QuotOSAlg (U1,R)),U2 st ( for s being Element of S holds b_{1} . s = OSHomQuot (F,R,s) ) & ( for s being Element of S holds b_{2} . s = OSHomQuot (F,R,s) ) holds

b_{1} = b_{2}

end;
let U1, U2 be non-empty OSAlgebra of S;

let F be ManySortedFunction of U1,U2;

let R be OSCongruence of U1;

func OSHomQuot (F,R) -> ManySortedFunction of (QuotOSAlg (U1,R)),U2 means :Def28: :: OSALG_4:def 28

for s being Element of S holds it . s = OSHomQuot (F,R,s);

existence for s being Element of S holds it . s = OSHomQuot (F,R,s);

ex b

for s being Element of S holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def28 defines OSHomQuot OSALG_4:def 28 :

for S being locally_directed OrderSortedSign

for U1, U2 being non-empty OSAlgebra of S

for F being ManySortedFunction of U1,U2

for R being OSCongruence of U1

for b_{6} being ManySortedFunction of (QuotOSAlg (U1,R)),U2 holds

( b_{6} = OSHomQuot (F,R) iff for s being Element of S holds b_{6} . s = OSHomQuot (F,R,s) );

for S being locally_directed OrderSortedSign

for U1, U2 being non-empty OSAlgebra of S

for F being ManySortedFunction of U1,U2

for R being OSCongruence of U1

for b

( b

theorem :: OSALG_4:25

for S being locally_directed OrderSortedSign

for U1, U2 being non-empty OSAlgebra of S

for F being ManySortedFunction of U1,U2

for R being OSCongruence of U1 st F is_homomorphism U1,U2 & F is order-sorted & R c= OSCng F holds

( OSHomQuot (F,R) is_homomorphism QuotOSAlg (U1,R),U2 & OSHomQuot (F,R) is order-sorted )

for U1, U2 being non-empty OSAlgebra of S

for F being ManySortedFunction of U1,U2

for R being OSCongruence of U1 st F is_homomorphism U1,U2 & F is order-sorted & R c= OSCng F holds

( OSHomQuot (F,R) is_homomorphism QuotOSAlg (U1,R),U2 & OSHomQuot (F,R) is order-sorted )

proof end;