begin
:: deftheorem Def1 defines os-compatible OSALG_4:def 1 :
theorem Th1:
:: deftheorem OSALG_4:def 2 :
canceled;
:: deftheorem Def3 defines OrderSortedRelation OSALG_4:def 3 :
definition
let R be non
empty Poset;
func Path_Rel R -> Equivalence_Relation of
means :
Def4:
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 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 ) ) ) )
uniqueness
for b1, b2 being Equivalence_Relation of 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
end;
:: deftheorem Def4 defines Path_Rel OSALG_4:def 4 :
theorem Th2:
:: deftheorem Def5 defines ~= OSALG_4:def 5 :
theorem
:: deftheorem defines Components OSALG_4:def 6 :
:: deftheorem OSALG_4:def 7 :
canceled;
:: deftheorem defines CComp OSALG_4:def 8 :
theorem
canceled;
theorem Th5:
:: deftheorem defines -carrier_of OSALG_4:def 9 :
theorem Th6:
:: deftheorem Def10 defines locally_directed OSALG_4:def 10 :
theorem Th7:
theorem Th8:
theorem Th9:
theorem Th10:
definition
let S be
locally_directed OrderSortedSign;
let A be
OSAlgebra of ;
let E be
MSEquivalence-like OrderSortedRelation of
A;
let C be
Component of
S;
func CompClass E,
C -> Equivalence_Relation of
means :
Def11:
for
x,
y being
set holds
(
[x,y] in it iff ex
s1 being
Element of st
(
s1 in C &
[x,y] in E . s1 ) );
existence
ex b1 being Equivalence_Relation of st
for x, y being set holds
( [x,y] in b1 iff ex s1 being Element of st
( s1 in C & [x,y] in E . s1 ) )
uniqueness
for b1, b2 being Equivalence_Relation of st ( for x, y being set holds
( [x,y] in b1 iff ex s1 being Element of 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 st
( s1 in C & [x,y] in E . s1 ) ) ) holds
b1 = b2
end;
:: deftheorem Def11 defines CompClass OSALG_4:def 11 :
definition
let S be
locally_directed OrderSortedSign;
let A be
OSAlgebra of ;
let E be
MSEquivalence-like OrderSortedRelation of
A;
let s1 be
Element of ;
func OSClass E,
s1 -> Subset of
means :
Def12:
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 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 ) )
uniqueness
for b1, b2 being Subset of 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
end;
:: deftheorem Def12 defines OSClass OSALG_4:def 12 :
theorem Th11:
:: deftheorem Def13 defines OSClass OSALG_4:def 13 :
:: deftheorem defines OSClass OSALG_4:def 14 :
theorem
theorem Th13:
theorem
begin
:: deftheorem Def15 defines #_os OSALG_4:def 15 :
definition
let S be
locally_directed OrderSortedSign;
let o be
Element of the
carrier' of
S;
let A be
non-empty OSAlgebra of
non-empty ;
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:
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
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
func OSQuotArgs R,
o -> Function of
((the Sorts of A # ) * the Arity of S) . o,
(((OSClass R) # ) * the Arity of S) . o means
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
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;
:: deftheorem Def16 defines OSQuotRes OSALG_4:def 16 :
:: deftheorem defines OSQuotArgs OSALG_4:def 17 :
definition
let S be
locally_directed OrderSortedSign;
let A be
non-empty OSAlgebra of
non-empty ;
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
for
o being
OperSymbol of 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 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 holds b1 . o = OSQuotRes R,o ) & ( for o being OperSymbol of holds b2 . o = OSQuotRes R,o ) holds
b1 = b2
func OSQuotArgs R -> ManySortedFunction of
(the Sorts of A # ) * the
Arity of
S,
((OSClass R) # ) * the
Arity of
S means
for
o being
OperSymbol of 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 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 holds b1 . o = OSQuotArgs R,o ) & ( for o being OperSymbol of holds b2 . o = OSQuotArgs R,o ) holds
b1 = b2
end;
:: deftheorem defines OSQuotRes OSALG_4:def 18 :
:: deftheorem defines OSQuotArgs OSALG_4:def 19 :
theorem Th15:
definition
let S be
locally_directed OrderSortedSign;
let o be
Element of the
carrier' of
S;
let A be
non-empty OSAlgebra of
non-empty ;
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:
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
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;
:: deftheorem Def20 defines OSQuotCharact OSALG_4:def 20 :
:: deftheorem Def21 defines OSQuotCharact OSALG_4:def 21 :
:: deftheorem defines QuotOSAlg OSALG_4:def 22 :
definition
let S be
locally_directed OrderSortedSign;
let U1 be
non-empty OSAlgebra of
non-empty ;
let R be
OSCongruence of
U1;
let s be
Element of ;
func OSNat_Hom U1,
R,
s -> Function of the
Sorts of
U1 . s,
OSClass R,
s means :
Def23:
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
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
end;
:: deftheorem Def23 defines OSNat_Hom OSALG_4:def 23 :
definition
let S be
locally_directed OrderSortedSign;
let U1 be
non-empty OSAlgebra of
non-empty ;
let R be
OSCongruence of
U1;
func OSNat_Hom U1,
R -> ManySortedFunction of ,
U1 means :
Def24:
for
s being
Element of holds
it . s = OSNat_Hom U1,
R,
s;
existence
ex b1 being ManySortedFunction of ,U1 st
for s being Element of holds b1 . s = OSNat_Hom U1,R,s
uniqueness
for b1, b2 being ManySortedFunction of ,U1 st ( for s being Element of holds b1 . s = OSNat_Hom U1,R,s ) & ( for s being Element of holds b2 . s = OSNat_Hom U1,R,s ) holds
b1 = b2
end;
:: deftheorem Def24 defines OSNat_Hom OSALG_4:def 24 :
theorem
theorem Th17:
:: deftheorem Def25 defines OSCng OSALG_4:def 25 :
definition
let S be
locally_directed OrderSortedSign;
let U1,
U2 be
non-empty OSAlgebra of
non-empty ;
let F be
ManySortedFunction of ,
U1;
let s be
Element of ;
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 :
Def26:
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
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;
:: deftheorem Def26 defines OSHomQuot OSALG_4:def 26 :
definition
let S be
locally_directed OrderSortedSign;
let U1,
U2 be
non-empty OSAlgebra of
non-empty ;
let F be
ManySortedFunction of ,
U1;
func OSHomQuot F -> ManySortedFunction of ,
(QuotOSAlg U1,(OSCng F)) means :
Def27:
for
s being
Element of holds
it . s = OSHomQuot F,
s;
existence
ex b1 being ManySortedFunction of ,(QuotOSAlg U1,(OSCng F)) st
for s being Element of holds b1 . s = OSHomQuot F,s
uniqueness
for b1, b2 being ManySortedFunction of ,(QuotOSAlg U1,(OSCng F)) st ( for s being Element of holds b1 . s = OSHomQuot F,s ) & ( for s being Element of holds b2 . s = OSHomQuot F,s ) holds
b1 = b2
end;
:: deftheorem Def27 defines OSHomQuot OSALG_4:def 27 :
theorem Th18:
theorem Th19:
theorem
:: deftheorem Def28 defines monotone OSALG_4:def 28 :
theorem Th21:
theorem Th22:
theorem Th23:
theorem Th24:
theorem
canceled;
theorem
definition
let S be
locally_directed OrderSortedSign;
let U1,
U2 be
non-empty OSAlgebra of
non-empty ;
let F be
ManySortedFunction of ,
U1;
let R be
OSCongruence of
U1;
let s be
Element of ;
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 :
Def29:
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
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;
:: deftheorem Def29 defines OSHomQuot OSALG_4:def 29 :
definition
let S be
locally_directed OrderSortedSign;
let U1,
U2 be
non-empty OSAlgebra of
non-empty ;
let F be
ManySortedFunction of ,
U1;
let R be
OSCongruence of
U1;
func OSHomQuot F,
R -> ManySortedFunction of ,
(QuotOSAlg U1,R) means :
Def30:
for
s being
Element of holds
it . s = OSHomQuot F,
R,
s;
existence
ex b1 being ManySortedFunction of ,(QuotOSAlg U1,R) st
for s being Element of holds b1 . s = OSHomQuot F,R,s
uniqueness
for b1, b2 being ManySortedFunction of ,(QuotOSAlg U1,R) st ( for s being Element of holds b1 . s = OSHomQuot F,R,s ) & ( for s being Element of holds b2 . s = OSHomQuot F,R,s ) holds
b1 = b2
end;
:: deftheorem Def30 defines OSHomQuot OSALG_4:def 30 :
theorem