environ
vocabularies HIDDEN, NUMBERS, XBOOLE_0, ORDERS_2, MSUALG_4, OSALG_1, RELAT_1, STRUCT_0, FUNCOP_1, PBOOLE, SUBSET_1, XXREAL_0, FUNCT_1, MSUALG_1, TARSKI, EQREL_1, NAT_1, MARGREL1, PARTFUN1, FINSEQ_1, ARYTM_3, ARYTM_1, ZFMISC_1, FINSEQ_5, CARD_1, RELAT_2, ORDINAL4, NATTRA_1, YELLOW15, SETFAM_1, COH_SP, YELLOW18, WAYBEL_0, CARD_3, MSUALG_3, WELLORD1, SEQM_3, OSALG_4;
notations HIDDEN, ZFMISC_1, TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, RELAT_2, FUNCT_1, RELSET_1, PARTFUN1, EQREL_1, SETFAM_1, XCMPLX_0, ORDERS_2, ORDERS_3, ORDINAL1, NUMBERS, FUNCT_2, FINSEQ_1, CARD_3, FINSEQ_2, FINSEQ_4, FINSEQ_5, FUNCOP_1, PBOOLE, STRUCT_0, WAYBEL_0, MSUALG_1, MSUALG_3, OSALG_1, OSALG_3, MSUALG_4, XXREAL_0;
definitions TARSKI, MSUALG_3, XBOOLE_0, OSALG_1, OSALG_3;
theorems XBOOLE_0, XBOOLE_1, FUNCT_1, FUNCT_2, PBOOLE, CARD_3, MSUALG_1, MSUALG_5, OSALG_1, OSALG_3, RELAT_2, ZFMISC_1, RELAT_1, RELSET_1, EQREL_1, MSUALG_3, MSUALG_6, MSAFREE, TARSKI, SYSREL, ORDERS_2, FINSEQ_1, FINSEQ_3, ENUMSET1, FINSEQ_5, INT_1, ORDERS_3, PARTFUN1, WAYBEL_0, GRFUNC_1, MSUALG_9, MSUALG_4, FINSEQ_2, ORDERS_1, FUNCOP_1, XREAL_1, XXREAL_0, XTUPLE_0;
schemes FUNCT_1, CLASSES1, NAT_1, FUNCT_2;
registrations SUBSET_1, RELAT_1, PARTFUN1, FUNCOP_1, XREAL_0, INT_1, FINSEQ_1, EQREL_1, FUNCT_1, PBOOLE, STRUCT_0, MSUALG_1, MSUALG_3, MSUALG_4, ORDERS_3, OSALG_1, ORDINAL1, CARD_3, TOLER_1, RELSET_1, FINSEQ_2;
constructors HIDDEN, REAL_1, NAT_1, NAT_D, EQREL_1, FINSEQ_4, FINSEQ_5, MSUALG_3, MSUALG_4, ORDERS_3, WAYBEL_0, OSALG_3, RELSET_1;
requirements HIDDEN, BOOLE, SUBSET, NUMERALS, REAL, ARITHM;
equalities XBOOLE_0;
expansions TARSKI, MSUALG_3, XBOOLE_0, OSALG_1, OSALG_3;
definition
let R be non
empty Poset;
existence
ex b1 being Equivalence_Relation of the carrier of R st
for x, y being object 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 ) ) ) )
uniqueness
for b1, b2 being Equivalence_Relation of the carrier of R st ( for x, y being object 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 object 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
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;
existence
ex b1 being Equivalence_Relation of ( the Sorts of A -carrier_of C) st
for x, y being object holds
( [x,y] in b1 iff ex s1 being Element of S st
( s1 in C & [x,y] in E . s1 ) )
uniqueness
for b1, b2 being Equivalence_Relation of ( the Sorts of A -carrier_of C) st ( for x, y being object 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 object holds
( [x,y] in b2 iff ex s1 being Element of S st
( s1 in C & [x,y] in E . s1 ) ) ) holds
b1 = b2
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;
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)
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
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
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
end;
definition
let S be
locally_directed OrderSortedSign;
let A be
non-empty OSAlgebra of
S;
let R be
OSCongruence of
A;
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)
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
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)
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
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;
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
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
end;
definition
let S be
locally_directed OrderSortedSign;
let U1 be
non-empty OSAlgebra of
S;
let R be
OSCongruence of
U1;
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)
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
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 s be
Element of
S;
assume that A1:
F is_homomorphism U1,
U2
and A2:
F is
order-sorted
;
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
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
end;
definition
let S be
locally_directed OrderSortedSign;
let U1,
U2 be
non-empty OSAlgebra of
S;
let F be
ManySortedFunction of
U1,
U2;
existence
ex b1 being ManySortedFunction of (QuotOSAlg (U1,(OSCng F))),U2 st
for s being Element of S holds b1 . s = OSHomQuot (F,s)
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
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 that A1:
F is_homomorphism U1,
U2
and A2:
F is
order-sorted
and A3:
R c= OSCng F
;
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
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
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;
existence
ex b1 being ManySortedFunction of (QuotOSAlg (U1,R)),U2 st
for s being Element of S holds b1 . s = OSHomQuot (F,R,s)
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
end;