:: OSALG_4 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

registration
let R be non empty Poset;
cluster Relation-yielding ManySortedSet of the carrier of R;
existence
ex b1 being OrderSortedSet of R st b1 is Relation-yielding
proof end;
end;

definition
let R be non empty Poset;
let A, B be ManySortedSet of the carrier of R;
let IT be ManySortedRelation of A,B;
attr IT is os-compatible means :Def1: :: OSALG_4:def 1
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 );
end;

:: deftheorem Def1 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 ) );

registration
let R be non empty Poset;
let A, B be ManySortedSet of the carrier of R;
cluster os-compatible ManySortedRelation of A,B;
existence
ex b1 being ManySortedRelation of A,B st b1 is os-compatible
proof end;
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;

theorem Th1: :: OSALG_4:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

registration
let R be non empty Poset;
let A, B be ManySortedSet of R;
cluster os-compatible -> order-sorted ManySortedRelation of A,B;
coherence
for b1 being ManySortedRelation of A,B st b1 is os-compatible holds
b1 is order-sorted
by Th1;
end;

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;

definition
let S be OrderSortedSign;
let U1 be OSAlgebra of S;
canceled;
mode OrderSortedRelation of U1 -> ManySortedRelation of U1 means :Def3: :: OSALG_4:def 3
it is os-compatible;
existence
ex b1 being ManySortedRelation of U1 st b1 is os-compatible
proof end;
end;

:: deftheorem OSALG_4:def 2 :
canceled;

:: deftheorem Def3 defines OrderSortedRelation OSALG_4:def 3 :
for S being OrderSortedSign
for U1 being OSAlgebra of S
for b3 being ManySortedRelation of U1 holds
( b3 is OrderSortedRelation of U1 iff b3 is os-compatible );

registration
let S be OrderSortedSign;
let U1 be OSAlgebra of S;
cluster MSEquivalence-like OrderSortedRelation of U1;
existence
ex b1 being OrderSortedRelation of U1 st b1 is MSEquivalence-like
proof end;
end;

registration
let S be OrderSortedSign;
let U1 be non-empty OSAlgebra of S;
cluster MSEquivalence-like MSCongruence-like OrderSortedRelation of U1;
existence
ex b1 being MSEquivalence-like OrderSortedRelation of U1 st b1 is MSCongruence-like
proof end;
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;

definition
let R be non empty Poset;
func Path_Rel R -> Equivalence_Relation of the carrier of R means :Def4: :: OSALG_4:def 4
for x, y being set 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
ex b1 being Equivalence_Relation of the carrier of R st
for x, y being set holds
( [x,y] in b1 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 ) ) ) )
proof end;
uniqueness
for b1, b2 being Equivalence_Relation of the carrier of R st ( for x, y being set holds
( [x,y] in b1 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 set holds
( [x,y] in b2 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
b1 = b2
proof end;
end;

:: deftheorem Def4 defines Path_Rel OSALG_4:def 4 :
for R being non empty Poset
for b2 being Equivalence_Relation of the carrier of R holds
( b2 = Path_Rel R iff for x, y being set holds
( [x,y] in b2 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 ) ) ) ) );

theorem Th2: :: OSALG_4:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for R being non empty Poset
for s1, s2 being Element of R st s1 <= s2 holds
[s1,s2] in Path_Rel R
proof end;

definition
let R be non empty Poset;
let s1, s2 be Element of R;
pred s1 ~= s2 means :Def5: :: OSALG_4:def 5
[s1,s2] in Path_Rel 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;
end;

:: deftheorem Def5 defines ~= OSALG_4:def 5 :
for R being non empty Poset
for s1, s2 being Element of R holds
( s1 ~= s2 iff [s1,s2] in Path_Rel R );

theorem :: OSALG_4:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for R being non empty Poset
for s1, s2, s3 being Element of R st s1 ~= s2 & s2 ~= s3 holds
s1 ~= s3
proof end;

definition
let R be non empty Poset;
func Components R -> non empty Subset-Family of R equals :: OSALG_4:def 6
Class (Path_Rel R);
coherence
Class (Path_Rel R) is non empty Subset-Family of R
;
end;

:: deftheorem defines Components OSALG_4:def 6 :
for R being non empty Poset holds Components R = Class (Path_Rel R);

registration
let R be non empty Poset;
cluster -> non empty Element of Components R;
coherence
for b1 being Element of Components R holds not b1 is empty
proof end;
end;

definition
let R be non empty Poset;
mode Component of R is Element of Components R;
end;

definition
let R be non empty Poset;
let s1 be Element of R;
canceled;
func CComp s1 -> Component of R equals :: OSALG_4:def 8
Class (Path_Rel R),s1;
correctness
coherence
Class (Path_Rel R),s1 is Component of R
;
by EQREL_1:def 5;
end;

:: deftheorem OSALG_4:def 7 :
canceled;

:: deftheorem defines CComp OSALG_4:def 8 :
for R being non empty Poset
for s1 being Element of R holds CComp s1 = Class (Path_Rel R),s1;

theorem Th4: :: OSALG_4:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for R being non empty Poset
for s1 being Element of R holds s1 in CComp s1 by EQREL_1:28;

theorem Th5: :: OSALG_4:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for R being non empty Poset
for s1, s2 being Element of R st s1 <= s2 holds
CComp s1 = CComp s2
proof end;

definition
let R be non empty Poset;
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 9
union { (A . s) where s is Element of R : s in C } ;
correctness
coherence
union { (A . s) where s is Element of R : s in C } is set
;
;
end;

:: deftheorem defines -carrier_of OSALG_4:def 9 :
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 Th6: :: OSALG_4:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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)
proof end;

definition
let R be non empty Poset;
attr R is locally_directed means :Def10: :: OSALG_4:def 10
for C being Component of R holds C is directed;
end;

:: deftheorem Def10 defines locally_directed OSALG_4:def 10 :
for R being non empty Poset holds
( R is locally_directed iff for C being Component of R holds C is directed );

theorem Th7: :: OSALG_4:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for R being non empty discrete Poset
for x, y being Element of R st [x,y] in Path_Rel R holds
x = y
proof end;

theorem Th8: :: OSALG_4:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for R being non empty discrete Poset
for C being Component of R ex x being Element of R st C = {x}
proof end;

theorem Th9: :: OSALG_4:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for R being non empty discrete Poset holds R is locally_directed
proof end;

registration
cluster non empty locally_directed RelStr ;
existence
ex b1 being non empty Poset st b1 is locally_directed
proof end;
end;

registration
cluster locally_directed OverloadedRSSign ;
existence
ex b1 being OrderSortedSign st b1 is locally_directed
proof end;
end;

registration
cluster non empty discrete -> non empty locally_directed RelStr ;
coherence
for b1 being non empty Poset st b1 is discrete holds
b1 is locally_directed
by Th9;
end;

registration
let S be non empty locally_directed Poset;
cluster -> non empty directed Element of Components S;
coherence
for b1 being Component of S holds b1 is directed
by Def10;
end;

theorem Th10: :: OSALG_4:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
{} is Equivalence_Relation of {}
proof end;

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;
func CompClass E,C -> Equivalence_Relation of the Sorts of A -carrier_of C means :Def11: :: OSALG_4:def 11
for x, y being set holds
( [x,y] in it iff ex s1 being Element of S st
( s1 in C & [x,y] in E . s1 ) );
existence
ex b1 being Equivalence_Relation of the Sorts of A -carrier_of C st
for x, y being set holds
( [x,y] in b1 iff ex s1 being Element of S st
( s1 in C & [x,y] in E . s1 ) )
proof end;
uniqueness
for b1, b2 being Equivalence_Relation of the Sorts of A -carrier_of C st ( for x, y being set holds
( [x,y] in b1 iff ex s1 being Element of S st
( s1 in C & [x,y] in E . s1 ) ) ) & ( for x, y being set holds
( [x,y] in b2 iff ex s1 being Element of S st
( s1 in C & [x,y] in E . s1 ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def11 defines CompClass 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 C being Component of S
for b5 being Equivalence_Relation of the Sorts of A -carrier_of C holds
( b5 = CompClass E,C iff for x, y being set holds
( [x,y] in b5 iff ex s1 being Element of S st
( s1 in C & [x,y] in E . 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;
func OSClass E,s1 -> Subset of (Class (CompClass E,(CComp s1))) means :Def12: :: OSALG_4:def 12
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
ex b1 being Subset of (Class (CompClass E,(CComp s1))) st
for z being set holds
( z in b1 iff ex x being set st
( x in the Sorts of A . s1 & z = Class (CompClass E,(CComp s1)),x ) )
proof end;
uniqueness
for b1, b2 being Subset of (Class (CompClass E,(CComp s1))) st ( for z being set holds
( z in b1 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 b2 iff ex x being set st
( x in the Sorts of A . s1 & z = Class (CompClass E,(CComp s1)),x ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def12 defines OSClass OSALG_4:def 12 :
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 b5 being Subset of (Class (CompClass E,(CComp s1))) holds
( b5 = OSClass E,s1 iff for z being set holds
( z in b5 iff ex x being set st
( 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;
cluster OSClass E,s1 -> non empty ;
coherence
not OSClass E,s1 is empty
proof end;
end;

theorem Th11: :: OSALG_4:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

definition
let S be locally_directed OrderSortedSign;
let A be OSAlgebra of S;
let E be MSEquivalence-like OrderSortedRelation of A;
func OSClass E -> OrderSortedSet of S means :Def13: :: OSALG_4:def 13
for s1 being Element of S holds it . s1 = OSClass E,s1;
existence
ex b1 being OrderSortedSet of S st
for s1 being Element of S holds b1 . s1 = OSClass E,s1
proof end;
uniqueness
for b1, b2 being OrderSortedSet of S st ( for s1 being Element of S holds b1 . s1 = OSClass E,s1 ) & ( for s1 being Element of S holds b2 . s1 = OSClass E,s1 ) holds
b1 = b2
proof end;
end;

:: deftheorem Def13 defines OSClass OSALG_4:def 13 :
for S being locally_directed OrderSortedSign
for A being OSAlgebra of S
for E being MSEquivalence-like OrderSortedRelation of A
for b4 being OrderSortedSet of S holds
( b4 = OSClass E iff for s1 being Element of S holds b4 . s1 = OSClass E,s1 );

registration
let S be locally_directed OrderSortedSign;
let A be non-empty OSAlgebra of S;
let E be MSEquivalence-like OrderSortedRelation of A;
cluster OSClass E -> V2 ;
coherence
OSClass E is non-empty
proof end;
end;

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;
func OSClass E,x -> Element of OSClass E,s equals :: OSALG_4:def 14
Class (CompClass E,(CComp s)),x;
correctness
coherence
Class (CompClass E,(CComp s)),x is Element of OSClass E,s
;
by Def12;
end;

:: deftheorem defines OSClass OSALG_4:def 14 :
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:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 )
proof end;

theorem Th13: :: OSALG_4:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 )
proof end;

theorem Th14: :: OSALG_4:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

definition
let S be locally_directed OrderSortedSign;
let o be Element of the OperSymbols 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 :Def15: :: OSALG_4:def 15
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
ex b1 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 & b1 . n = OSClass R,y )
proof end;
uniqueness
for b1, b2 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 & b1 . 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 & b2 . n = OSClass R,y ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def15 defines #_os OSALG_4:def 15 :
for S being locally_directed OrderSortedSign
for o being Element of the OperSymbols 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 b6 being Element of product ((OSClass R) * (the_arity_of o)) holds
( b6 = 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 & b6 . n = OSClass R,y ) );

definition
let S be locally_directed OrderSortedSign;
let o be Element of the OperSymbols 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 :Def16: :: OSALG_4:def 16
for x being Element of the Sorts of A . (the_result_sort_of o) holds it . x = OSClass R,x;
existence
ex b1 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 b1 . x = OSClass R,x
proof end;
uniqueness
for b1, b2 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 b1 . x = OSClass R,x ) & ( for x being Element of the Sorts of A . (the_result_sort_of o) holds b2 . x = OSClass R,x ) holds
b1 = b2
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 17
for x being Element of Args o,A holds it . x = R #_os x;
existence
ex b1 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 b1 . x = R #_os x
proof end;
uniqueness
for b1, b2 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 b1 . x = R #_os x ) & ( for x being Element of Args o,A holds b2 . x = R #_os x ) holds
b1 = b2
proof end;
end;

:: deftheorem Def16 defines OSQuotRes OSALG_4:def 16 :
for S being locally_directed OrderSortedSign
for o being Element of the OperSymbols of S
for A being non-empty OSAlgebra of S
for R being OSCongruence of A
for b5 being Function of (the Sorts of A * the ResultSort of S) . o,((OSClass R) * the ResultSort of S) . o holds
( b5 = OSQuotRes R,o iff for x being Element of the Sorts of A . (the_result_sort_of o) holds b5 . x = OSClass R,x );

:: deftheorem defines OSQuotArgs OSALG_4:def 17 :
for S being locally_directed OrderSortedSign
for o being Element of the OperSymbols of S
for A being non-empty OSAlgebra of S
for R being OSCongruence of A
for b5 being Function of ((the Sorts of A # ) * the Arity of S) . o,(((OSClass R) # ) * the Arity of S) . o holds
( b5 = OSQuotArgs R,o iff for x being Element of Args o,A holds b5 . x = R #_os x );

definition
let S be locally_directed OrderSortedSign;
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 18
for o being OperSymbol of S holds it . o = OSQuotRes R,o;
existence
ex b1 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 b1 . o = OSQuotRes R,o
proof end;
uniqueness
for b1, b2 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 b1 . o = OSQuotRes R,o ) & ( for o being OperSymbol of S holds b2 . o = OSQuotRes R,o ) holds
b1 = b2
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 19
for o being OperSymbol of S holds it . o = OSQuotArgs R,o;
existence
ex b1 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 b1 . o = OSQuotArgs R,o
proof end;
uniqueness
for b1, b2 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 b1 . o = OSQuotArgs R,o ) & ( for o being OperSymbol of S holds b2 . o = OSQuotArgs R,o ) holds
b1 = b2
proof end;
end;

:: deftheorem defines OSQuotRes OSALG_4:def 18 :
for S being locally_directed OrderSortedSign
for A being non-empty OSAlgebra of S
for R being OSCongruence of A
for b4 being ManySortedFunction of the Sorts of A * the ResultSort of S,(OSClass R) * the ResultSort of S holds
( b4 = OSQuotRes R iff for o being OperSymbol of S holds b4 . o = OSQuotRes R,o );

:: deftheorem defines OSQuotArgs 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 b4 being ManySortedFunction of (the Sorts of A # ) * the Arity of S,((OSClass R) # ) * the Arity of S holds
( b4 = OSQuotArgs R iff for o being OperSymbol of S holds b4 . o = OSQuotArgs R,o );

theorem Th15: :: OSALG_4:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being locally_directed OrderSortedSign
for o being Element of the OperSymbols 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 OperSymbols 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 :Def20: :: OSALG_4:def 20
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
ex b1 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
b1 . (R #_os a) = ((OSQuotRes R,o) * (Den o,A)) . a
proof end;
uniqueness
for b1, b2 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
b1 . (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
b2 . (R #_os a) = ((OSQuotRes R,o) * (Den o,A)) . a ) holds
b1 = b2
proof end;
end;

:: deftheorem Def20 defines OSQuotCharact OSALG_4:def 20 :
for S being locally_directed OrderSortedSign
for o being Element of the OperSymbols of S
for A being non-empty OSAlgebra of S
for R being OSCongruence of A
for b5 being Function of (((OSClass R) # ) * the Arity of S) . o,((OSClass R) * the ResultSort of S) . o holds
( b5 = 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
b5 . (R #_os a) = ((OSQuotRes R,o) * (Den o,A)) . a );

definition
let S be locally_directed OrderSortedSign;
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 :Def21: :: OSALG_4:def 21
for o being OperSymbol of S holds it . o = OSQuotCharact R,o;
existence
ex b1 being ManySortedFunction of ((OSClass R) # ) * the Arity of S,(OSClass R) * the ResultSort of S st
for o being OperSymbol of S holds b1 . o = OSQuotCharact R,o
proof end;
uniqueness
for b1, b2 being ManySortedFunction of ((OSClass R) # ) * the Arity of S,(OSClass R) * the ResultSort of S st ( for o being OperSymbol of S holds b1 . o = OSQuotCharact R,o ) & ( for o being OperSymbol of S holds b2 . o = OSQuotCharact R,o ) holds
b1 = b2
proof end;
end;

:: deftheorem Def21 defines OSQuotCharact OSALG_4:def 21 :
for S being locally_directed OrderSortedSign
for A being non-empty OSAlgebra of S
for R being OSCongruence of A
for b4 being ManySortedFunction of ((OSClass R) # ) * the Arity of S,(OSClass R) * the ResultSort of S holds
( b4 = OSQuotCharact R iff for o being OperSymbol of S holds b4 . o = OSQuotCharact R,o );

definition
let S be locally_directed OrderSortedSign;
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 22
MSAlgebra(# (OSClass R),(OSQuotCharact R) #);
coherence
MSAlgebra(# (OSClass R),(OSQuotCharact R) #) is OSAlgebra of S
by OSALG_1:17;
end;

:: deftheorem defines QuotOSAlg OSALG_4:def 22 :
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) #);

registration
let S be locally_directed OrderSortedSign;
let U1 be non-empty OSAlgebra of S;
let R be OSCongruence of U1;
cluster QuotOSAlg U1,R -> strict non-empty ;
coherence
( QuotOSAlg U1,R is strict & QuotOSAlg U1,R is non-empty )
by MSUALG_1:def 8;
end;

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;
func OSNat_Hom U1,R,s -> Function of the Sorts of U1 . s, OSClass R,s means :Def23: :: OSALG_4:def 23
for x being Element of the Sorts of U1 . s holds it . x = OSClass R,x;
existence
ex b1 being Function of the Sorts of U1 . s, OSClass R,s st
for x being Element of the Sorts of U1 . s holds b1 . x = OSClass R,x
proof end;
uniqueness
for b1, b2 being Function of the Sorts of U1 . s, OSClass R,s st ( for x being Element of the Sorts of U1 . s holds b1 . x = OSClass R,x ) & ( for x being Element of the Sorts of U1 . s holds b2 . x = OSClass R,x ) holds
b1 = b2
proof end;
end;

:: deftheorem Def23 defines OSNat_Hom OSALG_4:def 23 :
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 b5 being Function of the Sorts of U1 . s, OSClass R,s holds
( b5 = OSNat_Hom U1,R,s iff for x being Element of the Sorts of U1 . s holds b5 . x = OSClass R,x );

definition
let S be locally_directed OrderSortedSign;
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 :Def24: :: OSALG_4:def 24
for s being Element of S holds it . s = OSNat_Hom U1,R,s;
existence
ex b1 being ManySortedFunction of U1,(QuotOSAlg U1,R) st
for s being Element of S holds b1 . s = OSNat_Hom U1,R,s
proof end;
uniqueness
for b1, b2 being ManySortedFunction of U1,(QuotOSAlg U1,R) st ( for s being Element of S holds b1 . s = OSNat_Hom U1,R,s ) & ( for s being Element of S holds b2 . s = OSNat_Hom U1,R,s ) holds
b1 = b2
proof end;
end;

:: deftheorem Def24 defines OSNat_Hom OSALG_4:def 24 :
for S being locally_directed OrderSortedSign
for U1 being non-empty OSAlgebra of S
for R being OSCongruence of U1
for b4 being ManySortedFunction of U1,(QuotOSAlg U1,R) holds
( b4 = OSNat_Hom U1,R iff for s being Element of S holds b4 . s = OSNat_Hom U1,R,s );

theorem :: OSALG_4:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 )
proof end;

theorem Th17: :: OSALG_4:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

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 ) ;
func OSCng F -> OSCongruence of U1 equals :Def25: :: OSALG_4:def 25
MSCng F;
correctness
coherence
MSCng F is OSCongruence of U1
;
by A1, Th17;
end;

:: deftheorem Def25 defines OSCng 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 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 A1: ( F is_homomorphism U1,U2 & F is order-sorted ) ;
func OSHomQuot F,s -> Function of the Sorts of (QuotOSAlg U1,(OSCng F)) . s,the Sorts of U2 . s means :Def26: :: OSALG_4:def 26
for x being Element of the Sorts of U1 . s holds it . (OSClass (OSCng F),x) = (F . s) . x;
existence
ex b1 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 b1 . (OSClass (OSCng F),x) = (F . s) . x
proof end;
uniqueness
for b1, b2 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 b1 . (OSClass (OSCng F),x) = (F . s) . x ) & ( for x being Element of the Sorts of U1 . s holds b2 . (OSClass (OSCng F),x) = (F . s) . x ) holds
b1 = b2
proof end;
end;

:: deftheorem Def26 defines OSHomQuot OSALG_4:def 26 :
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 b6 being Function of the Sorts of (QuotOSAlg U1,(OSCng F)) . s,the Sorts of U2 . s holds
( b6 = OSHomQuot F,s iff for x being Element of the Sorts of U1 . s holds b6 . (OSClass (OSCng F),x) = (F . s) . x );

definition
let S be locally_directed OrderSortedSign;
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 :Def27: :: OSALG_4:def 27
for s being Element of S holds it . s = OSHomQuot F,s;
existence
ex b1 being ManySortedFunction of (QuotOSAlg U1,(OSCng F)),U2 st
for s being Element of S holds b1 . s = OSHomQuot F,s
proof end;
uniqueness
for b1, b2 being ManySortedFunction of (QuotOSAlg U1,(OSCng F)),U2 st ( for s being Element of S holds b1 . s = OSHomQuot F,s ) & ( for s being Element of S holds b2 . s = OSHomQuot F,s ) holds
b1 = b2
proof end;
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 b5 being ManySortedFunction of (QuotOSAlg U1,(OSCng F)),U2 holds
( b5 = OSHomQuot F iff for s being Element of S holds b5 . s = OSHomQuot F,s );

theorem Th18: :: OSALG_4:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 )
proof end;

theorem Th19: :: OSALG_4:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem :: OSALG_4:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

definition
let S be OrderSortedSign;
let U1 be non-empty OSAlgebra of S;
let R be MSEquivalence-like OrderSortedRelation of U1;
attr R is monotone means :Def28: :: OSALG_4:def 28
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);
end;

:: deftheorem Def28 defines monotone OSALG_4:def 28 :
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 Th21: :: OSALG_4:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem Th22: :: OSALG_4:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

registration
let S be OrderSortedSign;
let U1 be non-empty OSAlgebra of S;
cluster monotone OrderSortedRelation of U1;
existence
ex b1 being OSCongruence of U1 st b1 is monotone
proof end;
end;

registration
let S be OrderSortedSign;
let U1 be non-empty OSAlgebra of S;
cluster MSEquivalence-like monotone OrderSortedRelation of U1;
existence
ex b1 being MSEquivalence-like OrderSortedRelation of U1 st b1 is monotone
proof end;
end;

theorem Th23: :: OSALG_4:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

registration
let S be OrderSortedSign;
let U1 be non-empty OSAlgebra of S;
cluster MSEquivalence-like monotone -> MSEquivalence-like MSCongruence-like OrderSortedRelation of U1;
coherence
for b1 being MSEquivalence-like OrderSortedRelation of U1 st b1 is monotone holds
b1 is MSCongruence-like
by Th23;
end;

theorem Th24: :: OSALG_4:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being OrderSortedSign
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;
cluster -> monotone OrderSortedRelation of U1;
coherence
for b1 being OSCongruence of U1 holds b1 is monotone
by Th24;
end;

registration
let S be locally_directed OrderSortedSign;
let U1 be non-empty OSAlgebra of S;
let R be monotone OSCongruence of U1;
cluster QuotOSAlg U1,R -> strict non-empty monotone ;
coherence
QuotOSAlg U1,R is monotone
proof end;
end;

theorem :: OSALG_4:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: OSALG_4:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

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 A1: ( F is_homomorphism U1,U2 & F is order-sorted & R c= OSCng F ) ;
func OSHomQuot F,R,s -> Function of the Sorts of (QuotOSAlg U1,R) . s,the Sorts of U2 . s means :Def29: :: OSALG_4:def 29
for x being Element of the Sorts of U1 . s holds it . (OSClass R,x) = (F . s) . x;
existence
ex b1 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 b1 . (OSClass R,x) = (F . s) . x
proof end;
uniqueness
for b1, b2 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 b1 . (OSClass R,x) = (F . s) . x ) & ( for x being Element of the Sorts of U1 . s holds b2 . (OSClass R,x) = (F . s) . x ) holds
b1 = b2
proof end;
end;

:: deftheorem Def29 defines OSHomQuot OSALG_4:def 29 :
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 b7 being Function of the Sorts of (QuotOSAlg U1,R) . s,the Sorts of U2 . s holds
( b7 = OSHomQuot F,R,s iff for x being Element of the Sorts of U1 . s holds b7 . (OSClass R,x) = (F . s) . x );

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;
func OSHomQuot F,R -> ManySortedFunction of (QuotOSAlg U1,R),U2 means :Def30: :: OSALG_4:def 30
for s being Element of S holds it . s = OSHomQuot F,R,s;
existence
ex b1 being ManySortedFunction of (QuotOSAlg U1,R),U2 st
for s being Element of S holds b1 . s = OSHomQuot F,R,s
proof end;
uniqueness
for b1, b2 being ManySortedFunction of (QuotOSAlg U1,R),U2 st ( for s being Element of S holds b1 . s = OSHomQuot F,R,s ) & ( for s being Element of S holds b2 . s = OSHomQuot F,R,s ) holds
b1 = b2
proof end;
end;

:: deftheorem Def30 defines OSHomQuot OSALG_4:def 30 :
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 b6 being ManySortedFunction of (QuotOSAlg U1,R),U2 holds
( b6 = OSHomQuot F,R iff for s being Element of S holds b6 . s = OSHomQuot F,R,s );

theorem :: OSALG_4:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 )
proof end;