:: Order Sorted Algebras
:: by Josef Urban
::
:: Received September 19, 2002
:: Copyright (c) 2002-2021 Association of Mizar Users


:: TODO: constant ManySortedSet, constant OrderSortedSet,
:: constant -> order-sorted ManySortedSet of R
registration
let I be set ;
let f be ManySortedSet of I;
let p be FinSequence of I;
cluster p * f -> FinSequence-like ;
coherence
f * p is FinSequence-like
proof end;
end;

Lm1: for I being set
for f being ManySortedSet of I
for p being FinSequence of I holds
( dom (f * p) = dom p & len (f * p) = len p )
proof end;

definition
let S be non empty ManySortedSign ;
mode SortSymbol of S is Element of S;
end;

definition
let S be non empty ManySortedSign ;
mode OperSymbol of S is Element of the carrier' of S;
end;

:: Some structures
:: overloaded MSALGEBRA is modelled using an Equivalence_Relation
:: on carrier' ... partially hack enforced by previous articles,
:: partially can give more general treatment than the usual definition
definition
attr c1 is strict ;
struct OverloadedMSSign -> ManySortedSign ;
aggr OverloadedMSSign(# carrier, carrier', Overloading, Arity, ResultSort #) -> OverloadedMSSign ;
sel Overloading c1 -> Equivalence_Relation of the carrier' of c1;
end;

:: Order Sorted Signatures
definition
attr c1 is strict ;
struct RelSortedSign -> ManySortedSign , RelStr ;
aggr RelSortedSign(# carrier, InternalRel, carrier', Arity, ResultSort #) -> RelSortedSign ;
end;

definition
attr c1 is strict ;
struct OverloadedRSSign -> OverloadedMSSign , RelSortedSign ;
aggr OverloadedRSSign(# carrier, InternalRel, carrier', Overloading, Arity, ResultSort #) -> OverloadedRSSign ;
end;

:: following should be possible, but isn't:
:: set RS0 = RelSortedSign(#A,R,O,f,g #);
:: inheritance of attributes for structures does not work!!! :
:: RelStr(#A,R#) is reflexive does not imply that for RelSortedSign(...)
theorem Th1: :: OSALG_1:1
for A, O being non empty set
for R being Order of A
for Ol being Equivalence_Relation of O
for f being Function of O,(A *)
for g being Function of O,A holds
( not OverloadedRSSign(# A,R,O,Ol,f,g #) is empty & not OverloadedRSSign(# A,R,O,Ol,f,g #) is void & OverloadedRSSign(# A,R,O,Ol,f,g #) is reflexive & OverloadedRSSign(# A,R,O,Ol,f,g #) is transitive & OverloadedRSSign(# A,R,O,Ol,f,g #) is antisymmetric )
proof end;

registration
let A be non empty set ;
let R be Order of A;
let O be non empty set ;
let Ol be Equivalence_Relation of O;
let f be Function of O,(A *);
let g be Function of O,A;
cluster OverloadedRSSign(# A,R,O,Ol,f,g #) -> non empty reflexive transitive antisymmetric ;
coherence
( OverloadedRSSign(# A,R,O,Ol,f,g #) is strict & not OverloadedRSSign(# A,R,O,Ol,f,g #) is empty & OverloadedRSSign(# A,R,O,Ol,f,g #) is reflexive & OverloadedRSSign(# A,R,O,Ol,f,g #) is transitive & OverloadedRSSign(# A,R,O,Ol,f,g #) is antisymmetric ) by Th1;
end;

:: should be stated for nonoverloaded, but the inheritance is bad
definition
let S be OverloadedRSSign ;
attr S is order-sorted means :Def1: :: OSALG_1:def 1
( S is reflexive & S is transitive & S is antisymmetric );
end;

:: deftheorem Def1 defines order-sorted OSALG_1:def 1 :
for S being OverloadedRSSign holds
( S is order-sorted iff ( S is reflexive & S is transitive & S is antisymmetric ) );

registration
cluster order-sorted -> reflexive transitive antisymmetric for OverloadedRSSign ;
coherence
for b1 being OverloadedRSSign st b1 is order-sorted holds
( b1 is reflexive & b1 is transitive & b1 is antisymmetric ) ;
cluster non empty non void strict order-sorted for OverloadedRSSign ;
existence
ex b1 being OverloadedRSSign st
( b1 is strict & not b1 is empty & not b1 is void & b1 is order-sorted )
proof end;
end;

registration
cluster non empty non void for OverloadedMSSign ;
existence
ex b1 being OverloadedMSSign st
( not b1 is empty & not b1 is void )
proof end;
end;

definition
let S be non empty non void OverloadedMSSign ;
let x, y be OperSymbol of S;
pred x ~= y means :Def2: :: OSALG_1:def 2
[x,y] in the Overloading of S;
symmetry
for x, y being OperSymbol of S st [x,y] in the Overloading of S holds
[y,x] in the Overloading of S
proof end;
reflexivity
for x being OperSymbol of S holds [x,x] in the Overloading of S
proof end;
end;

:: deftheorem Def2 defines ~= OSALG_1:def 2 :
for S being non empty non void OverloadedMSSign
for x, y being OperSymbol of S holds
( x ~= y iff [x,y] in the Overloading of S );

:: remove when transitivity implemented
theorem Th2: :: OSALG_1:2
for S being non empty non void OverloadedMSSign
for o, o1, o2 being OperSymbol of S st o ~= o1 & o1 ~= o2 holds
o ~= o2
proof end;

:: with previous definition, equivalent funcs with same rank could exist
definition
let S be non empty non void OverloadedMSSign ;
attr S is discernable means :Def3: :: OSALG_1:def 3
 for x, y being OperSymbol of S st x ~= y & the_arity_of x = the_arity_of y & the_result_sort_of x = the_result_sort_of y holds
x = y;
attr S is op-discrete means :: OSALG_1:def 4
 the Overloading of S = id the carrier' of S;
end;

:: deftheorem Def3 defines discernable OSALG_1:def 3 :
for S being non empty non void OverloadedMSSign holds
( S is discernable iff for x, y being OperSymbol of S st x ~= y & the_arity_of x = the_arity_of y & the_result_sort_of x = the_result_sort_of y holds
x = y );

:: deftheorem defines op-discrete OSALG_1:def 4 :
for S being non empty non void OverloadedMSSign holds
( S is op-discrete iff the Overloading of S = id the carrier' of S );

theorem Th3: :: OSALG_1:3
for S being non empty non void OverloadedMSSign holds
( S is op-discrete iff for x, y being OperSymbol of S st x ~= y holds
x = y )
proof end;

theorem Th4: :: OSALG_1:4
for S being non empty non void OverloadedMSSign st S is op-discrete holds
S is discernable by Th3;

:: we require strictness here for simplicity, more interesting is whether
:: we could do a nonstrict version, keeping the remaining fields of S0;
definition
let S0 be non empty non void ManySortedSign ;
func OSSign S0 -> non empty non void strict order-sorted OverloadedRSSign means :Def5: :: OSALG_1:def 5
( the carrier of S0 = the carrier of it & id the carrier of S0 = the InternalRel of it & the carrier' of S0 = the carrier' of it & id the carrier' of S0 = the Overloading of it & the Arity of S0 = the Arity of it & the ResultSort of S0 = the ResultSort of it );
existence
ex b1 being non empty non void strict order-sorted OverloadedRSSign st
( the carrier of S0 = the carrier of b1 & id the carrier of S0 = the InternalRel of b1 & the carrier' of S0 = the carrier' of b1 & id the carrier' of S0 = the Overloading of b1 & the Arity of S0 = the Arity of b1 & the ResultSort of S0 = the ResultSort of b1 )
proof end;
uniqueness
for b1, b2 being non empty non void strict order-sorted OverloadedRSSign st the carrier of S0 = the carrier of b1 & id the carrier of S0 = the InternalRel of b1 & the carrier' of S0 = the carrier' of b1 & id the carrier' of S0 = the Overloading of b1 & the Arity of S0 = the Arity of b1 & the ResultSort of S0 = the ResultSort of b1 & the carrier of S0 = the carrier of b2 & id the carrier of S0 = the InternalRel of b2 & the carrier' of S0 = the carrier' of b2 & id the carrier' of S0 = the Overloading of b2 & the Arity of S0 = the Arity of b2 & the ResultSort of S0 = the ResultSort of b2 holds
b1 = b2 ;
end;

:: deftheorem Def5 defines OSSign OSALG_1:def 5 :
for S0 being non empty non void ManySortedSign
for b2 being non empty non void strict order-sorted OverloadedRSSign holds
( b2 = OSSign S0 iff ( the carrier of S0 = the carrier of b2 & id the carrier of S0 = the InternalRel of b2 & the carrier' of S0 = the carrier' of b2 & id the carrier' of S0 = the Overloading of b2 & the Arity of S0 = the Arity of b2 & the ResultSort of S0 = the ResultSort of b2 ) );

theorem Th5: :: OSALG_1:5
for S0 being non empty non void ManySortedSign holds
( OSSign S0 is discrete & OSSign S0 is op-discrete )
proof end;

registration
cluster non empty non void V67() reflexive transitive antisymmetric discrete strict order-sorted discernable op-discrete for OverloadedRSSign ;
existence
ex b1 being non empty non void strict order-sorted OverloadedRSSign st
( b1 is discrete & b1 is op-discrete & b1 is discernable )
proof end;
end;

registration
cluster non empty non void op-discrete -> non empty non void discernable for OverloadedRSSign ;
coherence
for b1 being non empty non void OverloadedRSSign st b1 is op-discrete holds
b1 is discernable by Th4;
end;

::FIXME: the order of this and the previous clusters cannot be exchanged!!
registration
let S0 be non empty non void ManySortedSign ;
cluster OSSign S0 -> non empty non void discrete strict order-sorted op-discrete ;
coherence
( OSSign S0 is discrete & OSSign S0 is op-discrete ) by Th5;
end;

definition
mode OrderSortedSign is non empty non void order-sorted discernable OverloadedRSSign ;
end;

:: this is mostly done in YELLOW_1, but getting the constructors work
:: could be major effort; I don't care now
definition
let S be non empty Poset;
let w1, w2 be Element of the carrier of S * ;
pred w1 <= w2 means :: OSALG_1:def 6
( len w1 = len w2 & ( for i being set st i in dom w1 holds
for s1, s2 being Element of S st s1 = w1 . i & s2 = w2 . i holds
s1 <= s2 ) );
reflexivity
for w1 being Element of the carrier of S * holds
( len w1 = len w1 & ( for i being set st i in dom w1 holds
for s1, s2 being Element of S st s1 = w1 . i & s2 = w1 . i holds
s1 <= s2 ) ) ;
end;

:: deftheorem defines <= OSALG_1:def 6 :
for S being non empty Poset
for w1, w2 being Element of the carrier of S * holds
( w1 <= w2 iff ( len w1 = len w2 & ( for i being set st i in dom w1 holds
for s1, s2 being Element of S st s1 = w1 . i & s2 = w2 . i holds
s1 <= s2 ) ) );

theorem Th6: :: OSALG_1:6
for S being non empty Poset
for w1, w2 being Element of the carrier of S * st w1 <= w2 & w2 <= w1 holds
w1 = w2
proof end;

theorem Th7: :: OSALG_1:7
for S being non empty Poset
for w1, w2 being Element of the carrier of S * st S is discrete & w1 <= w2 holds
w1 = w2
proof end;

theorem Th8: :: OSALG_1:8
for S being OrderSortedSign
for o1, o2 being OperSymbol of S st S is discrete & o1 ~= o2 & the_arity_of o1 <= the_arity_of o2 & the_result_sort_of o1 <= the_result_sort_of o2 holds
o1 = o2
proof end;

:: monotonicity of the signature
:: this doesnot extend to Overloading!
definition
let S be OrderSortedSign;
let o be OperSymbol of S;
attr o is monotone means :Def7: :: OSALG_1:def 7
 for o2 being OperSymbol of S st o ~= o2 & the_arity_of o <= the_arity_of o2 holds
the_result_sort_of o <= the_result_sort_of o2;
end;

:: deftheorem Def7 defines monotone OSALG_1:def 7 :
for S being OrderSortedSign
for o being OperSymbol of S holds
( o is monotone iff for o2 being OperSymbol of S st o ~= o2 & the_arity_of o <= the_arity_of o2 holds
the_result_sort_of o <= the_result_sort_of o2 );

definition
let S be OrderSortedSign;
attr S is monotone means :Def8: :: OSALG_1:def 8
 for o being OperSymbol of S holds o is monotone ;
end;

:: deftheorem Def8 defines monotone OSALG_1:def 8 :
for S being OrderSortedSign holds
( S is monotone iff for o being OperSymbol of S holds o is monotone );

theorem Th9: :: OSALG_1:9
for S being OrderSortedSign st S is op-discrete holds
S is monotone
proof end;

registration
cluster non empty non void V67() reflexive transitive antisymmetric order-sorted discernable monotone for OverloadedRSSign ;
existence
ex b1 being OrderSortedSign st b1 is monotone
proof end;
end;

registration
let S be monotone OrderSortedSign;
cluster monotone for Element of the carrier' of S;
existence
ex b1 being OperSymbol of S st b1 is monotone
proof end;
end;

registration
let S be monotone OrderSortedSign;
cluster -> monotone for Element of the carrier' of S;
coherence
for b1 being OperSymbol of S holds b1 is monotone by Def8;
end;

registration
cluster non empty non void order-sorted discernable op-discrete -> monotone for OverloadedRSSign ;
coherence
for b1 being OrderSortedSign st b1 is op-discrete holds
b1 is monotone by Th9;
end;

theorem :: OSALG_1:10
for S being OrderSortedSign
for o1, o2 being OperSymbol of S st S is monotone & the_arity_of o1 = {} & o1 ~= o2 & the_arity_of o2 = {} holds
o1 = o2
proof end;

:: least args,sort,rank,regularity for OperSymbol and
:: monotone OrderSortedSign
:: least bound for arguments
definition
let S be OrderSortedSign;
let o, o1 be OperSymbol of S;
let w1 be Element of the carrier of S * ;
pred o1 has_least_args_for o,w1 means :: OSALG_1:def 9
( o ~= o1 & w1 <= the_arity_of o1 & ( for o2 being OperSymbol of S st o ~= o2 & w1 <= the_arity_of o2 holds
the_arity_of o1 <= the_arity_of o2 ) );
pred o1 has_least_sort_for o,w1 means :: OSALG_1:def 10
( o ~= o1 & w1 <= the_arity_of o1 & ( for o2 being OperSymbol of S st o ~= o2 & w1 <= the_arity_of o2 holds
the_result_sort_of o1 <= the_result_sort_of o2 ) );
end;

:: deftheorem defines has_least_args_for OSALG_1:def 9 :
for S being OrderSortedSign
for o, o1 being OperSymbol of S
for w1 being Element of the carrier of S * holds
( o1 has_least_args_for o,w1 iff ( o ~= o1 & w1 <= the_arity_of o1 & ( for o2 being OperSymbol of S st o ~= o2 & w1 <= the_arity_of o2 holds
the_arity_of o1 <= the_arity_of o2 ) ) );

:: deftheorem defines has_least_sort_for OSALG_1:def 10 :
for S being OrderSortedSign
for o, o1 being OperSymbol of S
for w1 being Element of the carrier of S * holds
( o1 has_least_sort_for o,w1 iff ( o ~= o1 & w1 <= the_arity_of o1 & ( for o2 being OperSymbol of S st o ~= o2 & w1 <= the_arity_of o2 holds
the_result_sort_of o1 <= the_result_sort_of o2 ) ) );

definition
let S be OrderSortedSign;
let o, o1 be OperSymbol of S;
let w1 be Element of the carrier of S * ;
pred o1 has_least_rank_for o,w1 means :: OSALG_1:def 11
( o1 has_least_args_for o,w1 & o1 has_least_sort_for o,w1 );
end;

:: deftheorem defines has_least_rank_for OSALG_1:def 11 :
for S being OrderSortedSign
for o, o1 being OperSymbol of S
for w1 being Element of the carrier of S * holds
( o1 has_least_rank_for o,w1 iff ( o1 has_least_args_for o,w1 & o1 has_least_sort_for o,w1 ) );

definition
let S be OrderSortedSign;
let o be OperSymbol of S;
attr o is regular means :Def12: :: OSALG_1:def 12
( o is monotone & ( for w1 being Element of the carrier of S * st w1 <= the_arity_of o holds
ex o1 being OperSymbol of S st o1 has_least_args_for o,w1 ) );
end;

:: deftheorem Def12 defines regular OSALG_1:def 12 :
for S being OrderSortedSign
for o being OperSymbol of S holds
( o is regular iff ( o is monotone & ( for w1 being Element of the carrier of S * st w1 <= the_arity_of o holds
ex o1 being OperSymbol of S st o1 has_least_args_for o,w1 ) ) );

definition
let SM be monotone OrderSortedSign;
attr SM is regular means :Def13: :: OSALG_1:def 13
 for om being OperSymbol of SM holds om is regular ;
end;

:: deftheorem Def13 defines regular OSALG_1:def 13 :
for SM being monotone OrderSortedSign holds
( SM is regular iff for om being OperSymbol of SM holds om is regular );

theorem Th11: :: OSALG_1:11
for SM being monotone OrderSortedSign holds
( SM is regular iff for o being OperSymbol of SM
for w1 being Element of the carrier of SM * st w1 <= the_arity_of o holds
ex o1 being OperSymbol of SM st o1 has_least_rank_for o,w1 )
proof end;

theorem Th12: :: OSALG_1:12
for SM being monotone OrderSortedSign st SM is op-discrete holds
SM is regular
proof end;

registration
cluster non empty non void V67() reflexive transitive antisymmetric order-sorted discernable monotone regular for OverloadedRSSign ;
existence
ex b1 being monotone OrderSortedSign st b1 is regular
proof end;
end;

registration
cluster non empty non void order-sorted discernable op-discrete monotone -> monotone regular for OverloadedRSSign ;
coherence
for b1 being monotone OrderSortedSign st b1 is op-discrete holds
b1 is regular by Th12;
end;

registration
let SR be monotone regular OrderSortedSign;
cluster -> regular for Element of the carrier' of SR;
coherence
for b1 being OperSymbol of SR holds b1 is regular by Def13;
end;

theorem Th13: :: OSALG_1:13
for SR being monotone regular OrderSortedSign
for o, o3, o4 being OperSymbol of SR
for w1 being Element of the carrier of SR * st o3 has_least_args_for o,w1 & o4 has_least_args_for o,w1 holds
o3 = o4
proof end;

definition
let SR be monotone regular OrderSortedSign;
let o be OperSymbol of SR;
let w1 be Element of the carrier of SR * ;
assume A1: w1 <= the_arity_of o ;
func LBound (o,w1) -> OperSymbol of SR means :Def14: :: OSALG_1:def 14
it has_least_args_for o,w1;
existence
ex b1 being OperSymbol of SR st b1 has_least_args_for o,w1 by A1, Def12;
uniqueness
for b1, b2 being OperSymbol of SR st b1 has_least_args_for o,w1 & b2 has_least_args_for o,w1 holds
b1 = b2 by Th13;
end;

:: deftheorem Def14 defines LBound OSALG_1:def 14 :
for SR being monotone regular OrderSortedSign
for o being OperSymbol of SR
for w1 being Element of the carrier of SR * st w1 <= the_arity_of o holds
for b4 being OperSymbol of SR holds
( b4 = LBound (o,w1) iff b4 has_least_args_for o,w1 );

theorem Th14: :: OSALG_1:14
for SR being monotone regular OrderSortedSign
for o being OperSymbol of SR
for w1 being Element of the carrier of SR * st w1 <= the_arity_of o holds
LBound (o,w1) has_least_rank_for o,w1
proof end;

:: just to avoid on-the-spot casting in the examples
definition
let R be non empty Poset;
let z be non empty set ;
func ConstOSSet (R,z) -> ManySortedSet of the carrier of R equals :: OSALG_1:def 15
 the carrier of R --> z;
correctness
coherence
the carrier of R --> z is ManySortedSet of the carrier of R;
proof end;
end;

:: deftheorem defines ConstOSSet OSALG_1:def 15 :
for R being non empty Poset
for z being non empty set holds ConstOSSet (R,z) = the carrier of R --> z;

theorem Th15: :: OSALG_1:15
for R being non empty Poset
for z being non empty set holds
( ConstOSSet (R,z) is V8() & ( for s1, s2 being Element of R st s1 <= s2 holds
(ConstOSSet (R,z)) . s1 c= (ConstOSSet (R,z)) . s2 ) )
proof end;

definition
let R be non empty Poset;
let M be ManySortedSet of R;
attr M is order-sorted means :Def16: :: OSALG_1:def 16
 for s1, s2 being Element of R st s1 <= s2 holds
M . s1 c= M . s2;
end;

:: deftheorem Def16 defines order-sorted OSALG_1:def 16 :
for R being non empty Poset
for M being ManySortedSet of R holds
( M is order-sorted iff for s1, s2 being Element of R st s1 <= s2 holds
M . s1 c= M . s2 );

theorem Th16: :: OSALG_1:16
for R being non empty Poset
for z being non empty set holds ConstOSSet (R,z) is order-sorted by Th15;

registration
let R be non empty Poset;
cluster non empty Relation-like the carrier of R -defined Function-like V25( the carrier of R) order-sorted for set ;
existence
ex b1 being ManySortedSet of R st b1 is order-sorted
proof end;
end;

registration
let R be non empty Poset;
let z be non empty set ;
cluster ConstOSSet (R,z) -> order-sorted ;
coherence
ConstOSSet (R,z) is order-sorted by Th16;
end;

definition
let R be non empty Poset;
mode OrderSortedSet of R is order-sorted ManySortedSet of R;
end;

registration
let R be non empty Poset;
cluster non empty Relation-like V8() the carrier of R -defined Function-like V25( the carrier of R) order-sorted for set ;
existence
not for b1 being OrderSortedSet of R holds b1 is V8()
proof end;
end;

definition
let S be OrderSortedSign;
let M be MSAlgebra over S;
attr M is order-sorted means :Def17: :: OSALG_1:def 17
 for s1, s2 being SortSymbol of S st s1 <= s2 holds
the Sorts of M . s1 c= the Sorts of M . s2;
end;

:: deftheorem Def17 defines order-sorted OSALG_1:def 17 :
for S being OrderSortedSign
for M being MSAlgebra over S holds
( M is order-sorted iff for s1, s2 being SortSymbol of S st s1 <= s2 holds
the Sorts of M . s1 c= the Sorts of M . s2 );

theorem Th17: :: OSALG_1:17
for S being OrderSortedSign
for M being MSAlgebra over S holds
( M is order-sorted iff the Sorts of M is OrderSortedSet of S ) by Def16;

definition
let S be OrderSortedSign;
let z be non empty set ;
let CH be ManySortedFunction of ((ConstOSSet (S,z)) #) * the Arity of S,(ConstOSSet (S,z)) * the ResultSort of S;
func ConstOSA (S,z,CH) -> strict non-empty MSAlgebra over S means :Def18: :: OSALG_1:def 18
( the Sorts of it = ConstOSSet (S,z) & the Charact of it = CH );
existence
ex b1 being strict non-empty MSAlgebra over S st
( the Sorts of b1 = ConstOSSet (S,z) & the Charact of b1 = CH )
proof end;
uniqueness
for b1, b2 being strict non-empty MSAlgebra over S st the Sorts of b1 = ConstOSSet (S,z) & the Charact of b1 = CH & the Sorts of b2 = ConstOSSet (S,z) & the Charact of b2 = CH holds
b1 = b2 ;
end;

:: deftheorem Def18 defines ConstOSA OSALG_1:def 18 :
for S being OrderSortedSign
for z being non empty set
for CH being ManySortedFunction of ((ConstOSSet (S,z)) #) * the Arity of S,(ConstOSSet (S,z)) * the ResultSort of S
for b4 being strict non-empty MSAlgebra over S holds
( b4 = ConstOSA (S,z,CH) iff ( the Sorts of b4 = ConstOSSet (S,z) & the Charact of b4 = CH ) );

theorem Th18: :: OSALG_1:18
for S being OrderSortedSign
for z being non empty set
for CH being ManySortedFunction of ((ConstOSSet (S,z)) #) * the Arity of S,(ConstOSSet (S,z)) * the ResultSort of S holds ConstOSA (S,z,CH) is order-sorted
proof end;

registration
let S be OrderSortedSign;
cluster strict non-empty order-sorted for MSAlgebra over S;
existence
ex b1 being MSAlgebra over S st
( b1 is strict & b1 is non-empty & b1 is order-sorted )
proof end;
end;

registration
let S be OrderSortedSign;
let z be non empty set ;
let CH be ManySortedFunction of ((ConstOSSet (S,z)) #) * the Arity of S,(ConstOSSet (S,z)) * the ResultSort of S;
cluster ConstOSA (S,z,CH) -> strict non-empty order-sorted ;
coherence
ConstOSA (S,z,CH) is order-sorted by Th18;
end;

definition
let S be OrderSortedSign;
mode OSAlgebra of S is order-sorted MSAlgebra over S;
end;

theorem Th19: :: OSALG_1:19
for S being discrete OrderSortedSign
for M being MSAlgebra over S holds M is order-sorted by ORDERS_3:1;

registration
let S be discrete OrderSortedSign;
cluster -> order-sorted for MSAlgebra over S;
coherence
for b1 being MSAlgebra over S holds b1 is order-sorted by Th19;
end;

theorem Th20: :: OSALG_1:20
for S being OrderSortedSign
for w1, w2 being Element of the carrier of S *
for A being OSAlgebra of S st w1 <= w2 holds
( the Sorts of A #) . w1 c= ( the Sorts of A #) . w2
proof end;

:: canonical OSAlgebra for MSAlgebra
definition
let S0 be non empty non void ManySortedSign ;
let M be MSAlgebra over S0;
func OSAlg M -> strict OSAlgebra of OSSign S0 means :: OSALG_1:def 19
( the Sorts of it = the Sorts of M & the Charact of it = the Charact of M );
uniqueness
for b1, b2 being strict OSAlgebra of OSSign S0 st the Sorts of b1 = the Sorts of M & the Charact of b1 = the Charact of M & the Sorts of b2 = the Sorts of M & the Charact of b2 = the Charact of M holds
b1 = b2 ;
existence
ex b1 being strict OSAlgebra of OSSign S0 st
( the Sorts of b1 = the Sorts of M & the Charact of b1 = the Charact of M )
proof end;
end;

:: deftheorem defines OSAlg OSALG_1:def 19 :
for S0 being non empty non void ManySortedSign
for M being MSAlgebra over S0
for b3 being strict OSAlgebra of OSSign S0 holds
( b3 = OSAlg M iff ( the Sorts of b3 = the Sorts of M & the Charact of b3 = the Charact of M ) );

:: Element of A should mean Element of Union the Sorts of A here ...
:: MSAFREE3:def 1; Element of A,s is defined in MSUALG_6
theorem Th21: :: OSALG_1:21
for S being OrderSortedSign
for w1, w2, w3 being Element of the carrier of S * st w1 <= w2 & w2 <= w3 holds
w1 <= w3
proof end;

definition
let S be OrderSortedSign;
let o1, o2 be OperSymbol of S;
pred o1 <= o2 means :: OSALG_1:def 20
( o1 ~= o2 & the_arity_of o1 <= the_arity_of o2 & the_result_sort_of o1 <= the_result_sort_of o2 );
reflexivity
for o1 being OperSymbol of S holds
( o1 ~= o1 & the_arity_of o1 <= the_arity_of o1 & the_result_sort_of o1 <= the_result_sort_of o1 ) ;
end;

:: deftheorem defines <= OSALG_1:def 20 :
for S being OrderSortedSign
for o1, o2 being OperSymbol of S holds
( o1 <= o2 iff ( o1 ~= o2 & the_arity_of o1 <= the_arity_of o2 & the_result_sort_of o1 <= the_result_sort_of o2 ) );

theorem :: OSALG_1:22
for S being OrderSortedSign
for o1, o2 being OperSymbol of S st o1 <= o2 & o2 <= o1 holds
o1 = o2
proof end;

theorem :: OSALG_1:23
for S being OrderSortedSign
for o1, o2, o3 being OperSymbol of S st o1 <= o2 & o2 <= o3 holds
o1 <= o3 by Th2, Th21, ORDERS_2:3;

theorem Th24: :: OSALG_1:24
for S being OrderSortedSign
for o1, o2 being OperSymbol of S
for A being OSAlgebra of S st the_result_sort_of o1 <= the_result_sort_of o2 holds
Result (o1,A) c= Result (o2,A)
proof end;

theorem Th25: :: OSALG_1:25
for S being OrderSortedSign
for o1, o2 being OperSymbol of S
for A being OSAlgebra of S st the_arity_of o1 <= the_arity_of o2 holds
Args (o1,A) c= Args (o2,A)
proof end;

theorem :: OSALG_1:26
for S being OrderSortedSign
for o1, o2 being OperSymbol of S
for A being OSAlgebra of S st o1 <= o2 holds
( Args (o1,A) c= Args (o2,A) & Result (o1,A) c= Result (o2,A) ) by Th24, Th25;

:: OSAlgebra is monotone iff the interpretation of the same symbol on
:: widening sorts coincides
:: the definition would be nicer as function inclusion (see TEqMon)
:: without the restriction to Args(o1,A), but the permissiveness
:: of FUNCT_2:def 1 spoils that
definition
let S be OrderSortedSign;
let A be OSAlgebra of S;
attr A is monotone means :: OSALG_1:def 21
 for o1, o2 being OperSymbol of S st o1 <= o2 holds
(Den (o2,A)) | (Args (o1,A)) = Den (o1,A);
end;

:: deftheorem defines monotone OSALG_1:def 21 :
for S being OrderSortedSign
for A being OSAlgebra of S holds
( A is monotone iff for o1, o2 being OperSymbol of S st o1 <= o2 holds
(Den (o2,A)) | (Args (o1,A)) = Den (o1,A) );

theorem Th27: :: OSALG_1:27
for S being OrderSortedSign
for A being non-empty OSAlgebra of S holds
( A is monotone iff for o1, o2 being OperSymbol of S st o1 <= o2 holds
Den (o1,A) c= Den (o2,A) )
proof end;

theorem :: OSALG_1:28
for S being OrderSortedSign
for A being OSAlgebra of S st ( S is discrete or S is op-discrete ) holds
A is monotone
proof end;

:: TrivialOSA(S,z,z1) interprets all funcs as one constant
definition
let S be OrderSortedSign;
let z be non empty set ;
let z1 be Element of z;
func TrivialOSA (S,z,z1) -> strict OSAlgebra of S means :Def22: :: OSALG_1:def 22
( the Sorts of it = ConstOSSet (S,z) & ( for o being OperSymbol of S holds Den (o,it) = (Args (o,it)) --> z1 ) );
existence
ex b1 being strict OSAlgebra of S st
( the Sorts of b1 = ConstOSSet (S,z) & ( for o being OperSymbol of S holds Den (o,b1) = (Args (o,b1)) --> z1 ) )
proof end;
uniqueness
for b1, b2 being strict OSAlgebra of S st the Sorts of b1 = ConstOSSet (S,z) & ( for o being OperSymbol of S holds Den (o,b1) = (Args (o,b1)) --> z1 ) & the Sorts of b2 = ConstOSSet (S,z) & ( for o being OperSymbol of S holds Den (o,b2) = (Args (o,b2)) --> z1 ) holds
b1 = b2
proof end;
end;

:: deftheorem Def22 defines TrivialOSA OSALG_1:def 22 :
for S being OrderSortedSign
for z being non empty set
for z1 being Element of z
for b4 being strict OSAlgebra of S holds
( b4 = TrivialOSA (S,z,z1) iff ( the Sorts of b4 = ConstOSSet (S,z) & ( for o being OperSymbol of S holds Den (o,b4) = (Args (o,b4)) --> z1 ) ) );

theorem Th29: :: OSALG_1:29
for S being OrderSortedSign
for z being non empty set
for z1 being Element of z holds
( TrivialOSA (S,z,z1) is non-empty & TrivialOSA (S,z,z1) is monotone )
proof end;

registration
let S be OrderSortedSign;
cluster strict non-empty order-sorted monotone for MSAlgebra over S;
existence
ex b1 being OSAlgebra of S st
( b1 is monotone & b1 is strict & b1 is non-empty )
proof end;
end;

registration
let S be OrderSortedSign;
let z be non empty set ;
let z1 be Element of z;
cluster TrivialOSA (S,z,z1) -> strict non-empty monotone ;
coherence
( TrivialOSA (S,z,z1) is monotone & TrivialOSA (S,z,z1) is non-empty ) by Th29;
end;

definition
let S be OrderSortedSign;
func OperNames S -> non empty Subset-Family of the carrier' of S equals :: OSALG_1:def 23
 Class the Overloading of S;
coherence
Class the Overloading of S is non empty Subset-Family of the carrier' of S ;
end;

:: deftheorem defines OperNames OSALG_1:def 23 :
for S being OrderSortedSign holds OperNames S = Class the Overloading of S;

registration
let S be OrderSortedSign;
cluster -> non empty for Element of OperNames S;
coherence
for b1 being Element of OperNames S holds not b1 is empty
proof end;
end;

definition
let S be OrderSortedSign;
mode OperName of S is Element of OperNames S;
end;

definition
let S be OrderSortedSign;
let op1 be OperSymbol of S;
func Name op1 -> OperName of S equals :: OSALG_1:def 24
 Class ( the Overloading of S,op1);
coherence
Class ( the Overloading of S,op1) is OperName of S by EQREL_1:def 3;
end;

:: deftheorem defines Name OSALG_1:def 24 :
for S being OrderSortedSign
for op1 being OperSymbol of S holds Name op1 = Class ( the Overloading of S,op1);

theorem Th30: :: OSALG_1:30
for S being OrderSortedSign
for op1, op2 being OperSymbol of S holds
( op1 ~= op2 iff op2 in Class ( the Overloading of S,op1) )
proof end;

theorem Th31: :: OSALG_1:31
for S being OrderSortedSign
for op1, op2 being OperSymbol of S holds
( op1 ~= op2 iff Name op1 = Name op2 )
proof end;

theorem :: OSALG_1:32
for S being OrderSortedSign
for X being set holds
( X is OperName of S iff ex op1 being OperSymbol of S st X = Name op1 )
proof end;

definition
let S be OrderSortedSign;
let o be OperName of S;
:: original: Element
redefine mode Element of o -> OperSymbol of S;
coherence
for b1 being Element of o holds b1 is OperSymbol of S
proof end;
end;

theorem Th33: :: OSALG_1:33
for S being OrderSortedSign
for on being OperName of S
for op being OperSymbol of S holds
( op is Element of on iff Name op = on )
proof end;

theorem Th34: :: OSALG_1:34
for SR being monotone regular OrderSortedSign
for op1, op2 being OperSymbol of SR
for w being Element of the carrier of SR * st op1 ~= op2 & w <= the_arity_of op1 & w <= the_arity_of op2 holds
LBound (op1,w) = LBound (op2,w)
proof end;

definition
let SR be monotone regular OrderSortedSign;
let on be OperName of SR;
let w be Element of the carrier of SR * ;
assume A1: ex op being Element of on st w <= the_arity_of op ;
func LBound (on,w) -> Element of on means :: OSALG_1:def 25
 for op being Element of on st w <= the_arity_of op holds
it = LBound (op,w);
existence
ex b1 being Element of on st
for op being Element of on st w <= the_arity_of op holds
b1 = LBound (op,w)
proof end;
uniqueness
for b1, b2 being Element of on st ( for op being Element of on st w <= the_arity_of op holds
b1 = LBound (op,w) ) & ( for op being Element of on st w <= the_arity_of op holds
b2 = LBound (op,w) ) holds
b1 = b2
proof end;
end;

:: deftheorem defines LBound OSALG_1:def 25 :
for SR being monotone regular OrderSortedSign
for on being OperName of SR
for w being Element of the carrier of SR * st ex op being Element of on st w <= the_arity_of op holds
for b4 being Element of on holds
( b4 = LBound (on,w) iff for op being Element of on st w <= the_arity_of op holds
b4 = LBound (op,w) );

theorem :: OSALG_1:35
for S being monotone regular OrderSortedSign
for o being OperSymbol of S
for w1 being Element of the carrier of S * st w1 <= the_arity_of o holds
LBound (o,w1) <= o
proof end;