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


begin

:: 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;
clusterp * f ->  FinSequence-like ;
coherence
 f * p is FinSequence-like
proofend;
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 )
proofend;

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
attrc1 is strict ;
struct OverloadedMSSign  ->  ManySortedSign ;
aggrOverloadedMSSign(# carrier, carrier', Overloading, Arity, ResultSort #) ->  OverloadedMSSign ;
sel Overloading c1 ->  Equivalence_Relation of the carrier' of c1;
end;

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

definition
attrc1 is strict ;
struct OverloadedRSSign  ->  OverloadedMSSign , RelSortedSign ;
aggrOverloadedRSSign(# 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 )
proofend;

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;

begin

:: should be stated for nonoverloaded, but the inheritance is bad
definition
let S be OverloadedRSSign ;
attrS 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 ) by Def1;
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 )
proofend;
end;

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

definition
let S be non empty non void OverloadedMSSign ;
let x, y be OperSymbol of S;
predx ~= 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
proofend;
reflexivity
 for x being OperSymbol of S holds [x,x] in the Overloading of S
proofend;
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
proofend;

:: with previous definition, equivalent funcs with same rank could exist
definition
let S be non empty non void OverloadedMSSign ;
attrS 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;
attrS is op-discrete  means :Def4: :: 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 Def4 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 )
proofend;

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

begin

:: 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 )
proofend;
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 )
proofend;

registration
cluster non empty non void V64() 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 )
proofend;
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 * ;
predw1 <= w2 means :Def6: :: OSALG_1:def 6
( len w1 = len w2 &amp; ( for i being set st i in dom w1 holds
for s1, s2 being Element of S st s1 = w1 . i &amp; s2 = w2 . i holds
s1 <= s2 ) );
reflexivity
 for w1 being Element of the carrier of S * holds
( len w1 = len w1 &amp; ( for i being set st i in dom w1 holds
for s1, s2 being Element of S st s1 = w1 . i &amp; s2 = w1 . i holds
s1 <= s2 ) ) ;
end;

:: deftheorem Def6 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 &amp; ( for i being set st i in dom w1 holds
for s1, s2 being Element of S st s1 = w1 . i &amp; 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 &amp; w2 <= w1 holds
w1 = w2
proofend;

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 &amp; w1 <= w2 holds
w1 = w2
proofend;

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

:: monotonicity of the signature
:: this doesnot extend to Overloading!
definition
let S be OrderSortedSign;
let o be OperSymbol of S;
attro is monotone  means :Def7: :: OSALG_1:def 7
 for o2 being OperSymbol of S st o ~= o2 &amp; 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 &amp; the_arity_of o <= the_arity_of o2 holds
the_result_sort_of o <= the_result_sort_of o2 );

definition
let S be OrderSortedSign;
attrS 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
proofend;

registration
cluster non empty non void V64() reflexive transitive antisymmetric order-sorted discernable monotone for OverloadedRSSign ;
existence
 ex b1 being OrderSortedSign st b1 is monotone
proofend;
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
proofend;
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 &amp; the_arity_of o1 = {} &amp; o1 ~= o2 &amp; the_arity_of o2 = {} holds
o1 = o2
proofend;

:: 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 * ;
predo1 has_least_args_for o,w1 means :Def9: :: OSALG_1:def 9
( o ~= o1 &amp; w1 <= the_arity_of o1 &amp; ( for o2 being OperSymbol of S st o ~= o2 &amp; w1 <= the_arity_of o2 holds
the_arity_of o1 <= the_arity_of o2 ) );
predo1 has_least_sort_for o,w1 means :Def10: :: OSALG_1:def 10
( o ~= o1 &amp; w1 <= the_arity_of o1 &amp; ( for o2 being OperSymbol of S st o ~= o2 &amp; w1 <= the_arity_of o2 holds
the_result_sort_of o1 <= the_result_sort_of o2 ) );
end;

:: deftheorem Def9 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 &amp; w1 <= the_arity_of o1 &amp; ( for o2 being OperSymbol of S st o ~= o2 &amp; w1 <= the_arity_of o2 holds
the_arity_of o1 <= the_arity_of o2 ) ) );

:: deftheorem Def10 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 &amp; w1 <= the_arity_of o1 &amp; ( for o2 being OperSymbol of S st o ~= o2 &amp; 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 * ;
predo1 has_least_rank_for o,w1 means :Def11: :: OSALG_1:def 11
( o1 has_least_args_for o,w1 &amp; o1 has_least_sort_for o,w1 );
end;

:: deftheorem Def11 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 &amp; o1 has_least_sort_for o,w1 ) );

definition
let S be OrderSortedSign;
let o be OperSymbol of S;
attro is regular  means :Def12: :: OSALG_1:def 12
( o is monotone &amp; ( 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 &amp; ( 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;
attrSM 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 )
proofend;

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

registration
cluster non empty non void V64() reflexive transitive antisymmetric order-sorted discernable monotone regular for OverloadedRSSign ;
existence
 ex b1 being monotone OrderSortedSign st b1 is regular
proofend;
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 o3, o, o4 being OperSymbol of SR
for w1 being Element of the carrier of SR * st o3 has_least_args_for o,w1 &amp; o4 has_least_args_for o,w1 holds
o3 = o4
proofend;

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 &amp; 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
proofend;

:: 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;
proofend;
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() &amp; ( for s1, s2 being Element of R st s1 <= s2 holds
(ConstOSSet (R,z)) . s1 c= (ConstOSSet (R,z)) . s2 ) )
proofend;

definition
let R be non empty Poset;
let M be ManySortedSet of R;
attrM 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
proofend;

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
proofend;
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()
proofend;
end;

definition
let S be OrderSortedSign;
let M be MSAlgebra over S;
attrM 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 )
proofend;

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) &amp; the Charact of it = CH );
existence
 ex b1 being strict non-empty MSAlgebra over S st
( the Sorts of b1 = ConstOSSet (S,z) &amp; the Charact of b1 = CH )
proofend;
uniqueness
 for b1, b2 being strict non-empty MSAlgebra over S st the Sorts of b1 = ConstOSSet (S,z) &amp; the Charact of b1 = CH &amp; the Sorts of b2 = ConstOSSet (S,z) &amp; 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) &amp; 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
proofend;

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 &amp; b1 is non-empty &amp; b1 is order-sorted )
proofend;
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
proofend;

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
proofend;

:: 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 &amp; 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 &amp; the Charact of b1 = the Charact of M &amp; the Sorts of b2 = the Sorts of M &amp; 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 &amp; the Charact of b1 = the Charact of M )
proofend;
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 &amp; 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 &amp; w2 <= w3 holds
w1 <= w3
proofend;

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

:: deftheorem Def20 defines <= OSALG_1:def_20_:_
 for S being OrderSortedSign
for o1, o2 being OperSymbol of S holds
( o1 <= o2 iff ( o1 ~= o2 &amp; the_arity_of o1 <= the_arity_of o2 &amp; 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 &amp; o2 <= o1 holds
o1 = o2
proofend;

theorem :: OSALG_1:23
for S being OrderSortedSign
for o1, o2, o3 being OperSymbol of S st o1 <= o2 &amp; o2 <= o3 holds
o1 <= o3
proofend;

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)
proofend;

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)
proofend;

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) &amp; Result (o1,A) c= Result (o2,A) )
proofend;

:: 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;
attrA is monotone  means :Def21: :: 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 Def21 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) )
proofend;

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
proofend;

:: 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) &amp; ( 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) &amp; ( for o being OperSymbol of S holds Den (o,b1) = (Args (o,b1)) --> z1 ) )
proofend;
uniqueness
 for b1, b2 being strict OSAlgebra of S st the Sorts of b1 = ConstOSSet (S,z) &amp; ( for o being OperSymbol of S holds Den (o,b1) = (Args (o,b1)) --> z1 ) &amp; the Sorts of b2 = ConstOSSet (S,z) &amp; ( for o being OperSymbol of S holds Den (o,b2) = (Args (o,b2)) --> z1 ) holds
b1 = b2
proofend;
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) &amp; ( 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 &amp; TrivialOSA (S,z,z1) is monotone )
proofend;

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 &amp; b1 is strict &amp; b1 is non-empty )
proofend;
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 &amp; 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
proofend;
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) )
proofend;

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

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 )
proofend;

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
proofend;
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 )
proofend;

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 &amp; w <= the_arity_of op1 &amp; w <= the_arity_of op2 holds
LBound (op1,w) = LBound (op2,w)
proofend;

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)
proofend;
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) ) &amp; ( for op being Element of on st w <= the_arity_of op holds
b2 = LBound (op,w) ) holds
b1 = b2
proofend;
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
proofend;