:: by Josef Urban

::

:: Received September 19, 2002

:: Copyright (c) 2002-2017 Association of Mizar Users

registration

let I be set ;

let f be ManySortedSet of I;

let p be FinSequence of I;

coherence

f * p is FinSequence-like

end;
let f be ManySortedSet of I;

let p be FinSequence of I;

coherence

f * p is FinSequence-like

proof 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
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

:: 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 c_{1} is strict ;

struct OverloadedMSSign -> ManySortedSign ;

aggr OverloadedMSSign(# carrier, carrier', Overloading, Arity, ResultSort #) -> OverloadedMSSign ;

sel Overloading c_{1} -> Equivalence_Relation of the carrier' of c_{1};

end;
struct OverloadedMSSign -> ManySortedSign ;

aggr OverloadedMSSign(# carrier, carrier', Overloading, Arity, ResultSort #) -> OverloadedMSSign ;

sel Overloading c

:: Order Sorted Signatures

definition

attr c_{1} is strict ;

struct RelSortedSign -> ManySortedSign , RelStr ;

aggr RelSortedSign(# carrier, InternalRel, carrier', Arity, ResultSort #) -> RelSortedSign ;

end;
struct RelSortedSign -> ManySortedSign , RelStr ;

aggr RelSortedSign(# carrier, InternalRel, carrier', Arity, ResultSort #) -> RelSortedSign ;

definition

attr c_{1} is strict ;

struct OverloadedRSSign -> OverloadedMSSign , RelSortedSign ;

aggr OverloadedRSSign(# carrier, InternalRel, carrier', Overloading, Arity, ResultSort #) -> OverloadedRSSign ;

end;
struct OverloadedRSSign -> OverloadedMSSign , RelSortedSign ;

aggr OverloadedRSSign(# carrier, InternalRel, carrier', Overloading, Arity, ResultSort #) -> OverloadedRSSign ;

:: 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(...)

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

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;

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

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;

:: should be stated for nonoverloaded, but the inheritance is bad

definition

let S be OverloadedRSSign ;

end;
attr S is order-sorted means :Def1: :: OSALG_1:def 1

( S is reflexive & S is transitive & S is antisymmetric );

( S is reflexive & S is transitive & S is antisymmetric );

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

for S being OverloadedRSSign holds

( S is order-sorted iff ( S is reflexive & S is transitive & S is antisymmetric ) );

registration

coherence

for b_{1} being OverloadedRSSign st b_{1} is order-sorted holds

( b_{1} is reflexive & b_{1} is transitive & b_{1} is antisymmetric )
;

existence

ex b_{1} being OverloadedRSSign st

( b_{1} is strict & not b_{1} is empty & not b_{1} is void & b_{1} is order-sorted )

end;
for b

( b

existence

ex b

( b

proof end;

registration
end;

definition

let S be non empty non void OverloadedMSSign ;

let x, y be OperSymbol 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

for x being OperSymbol of S holds [x,x] in the Overloading of S

end;
let x, y be OperSymbol 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;

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

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

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 ;

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

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

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

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 )

( S is op-discrete iff for x, y being OperSymbol of S st x ~= y holds

x = y )

proof end;

:: we require strictness here for simplicity, more interesting is whether

:: we could do a nonstrict version, keeping the remaining fields of S0;

:: we could do a nonstrict version, keeping the remaining fields of S0;

definition

let S0 be non empty non void ManySortedSign ;

ex b_{1} being non empty non void strict order-sorted OverloadedRSSign st

( the carrier of S0 = the carrier of b_{1} & id the carrier of S0 = the InternalRel of b_{1} & the carrier' of S0 = the carrier' of b_{1} & id the carrier' of S0 = the Overloading of b_{1} & the Arity of S0 = the Arity of b_{1} & the ResultSort of S0 = the ResultSort of b_{1} )

for b_{1}, b_{2} being non empty non void strict order-sorted OverloadedRSSign st the carrier of S0 = the carrier of b_{1} & id the carrier of S0 = the InternalRel of b_{1} & the carrier' of S0 = the carrier' of b_{1} & id the carrier' of S0 = the Overloading of b_{1} & the Arity of S0 = the Arity of b_{1} & the ResultSort of S0 = the ResultSort of b_{1} & the carrier of S0 = the carrier of b_{2} & id the carrier of S0 = the InternalRel of b_{2} & the carrier' of S0 = the carrier' of b_{2} & id the carrier' of S0 = the Overloading of b_{2} & the Arity of S0 = the Arity of b_{2} & the ResultSort of S0 = the ResultSort of b_{2} holds

b_{1} = b_{2}
;

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

ex b

( the carrier of S0 = the carrier of b

proof end;

uniqueness for b

b

:: deftheorem Def5 defines OSSign OSALG_1:def 5 :

for S0 being non empty non void ManySortedSign

for b_{2} being non empty non void strict order-sorted OverloadedRSSign holds

( b_{2} = OSSign S0 iff ( the carrier of S0 = the carrier of b_{2} & id the carrier of S0 = the InternalRel of b_{2} & the carrier' of S0 = the carrier' of b_{2} & id the carrier' of S0 = the Overloading of b_{2} & the Arity of S0 = the Arity of b_{2} & the ResultSort of S0 = the ResultSort of b_{2} ) );

for S0 being non empty non void ManySortedSign

for b

( b

theorem Th5: :: OSALG_1:5

for S0 being non empty non void ManySortedSign holds

( OSSign S0 is discrete & OSSign S0 is op-discrete )

( OSSign S0 is discrete & OSSign S0 is op-discrete )

proof end;

registration

ex b_{1} being non empty non void strict order-sorted OverloadedRSSign st

( b_{1} is discrete & b_{1} is op-discrete & b_{1} is discernable )
end;

cluster non empty non void V67() reflexive transitive antisymmetric discrete strict order-sorted discernable op-discrete for OverloadedRSSign ;

existence ex b

( b

proof end;

registration

coherence

for b_{1} being non empty non void OverloadedRSSign st b_{1} is op-discrete holds

b_{1} is discernable
by Th4;

end;
for b

b

::FIXME: the order of this and the previous clusters cannot be exchanged!!

registration

let S0 be non empty non void ManySortedSign ;

coherence

( OSSign S0 is discrete & OSSign S0 is op-discrete ) by Th5;

end;
coherence

( OSSign S0 is discrete & OSSign S0 is op-discrete ) by Th5;

definition
end;

:: this is mostly done in YELLOW_1, but getting the constructors work

:: could be major effort; I don't care now

:: 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 * ;

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

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

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

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

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

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

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!

:: this doesnot extend to Overloading!

definition

let S be OrderSortedSign;

let o be OperSymbol of S;

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

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;

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

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

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

for S being OrderSortedSign holds

( S is monotone iff for o being OperSymbol of S holds o is monotone );

registration

ex b_{1} being OrderSortedSign st b_{1} is monotone
end;

cluster non empty non void V67() reflexive transitive antisymmetric order-sorted discernable monotone for OverloadedRSSign ;

existence ex b

proof end;

registration

let S be monotone OrderSortedSign;

existence

ex b_{1} being OperSymbol of S st b_{1} is monotone

end;
existence

ex b

proof end;

registration

let S be monotone OrderSortedSign;

coherence

for b_{1} being OperSymbol of S holds b_{1} is monotone
by Def8;

end;
coherence

for b

registration
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

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

:: 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 * ;

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

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

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

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

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

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

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

( o1 has_least_args_for o,w1 & o1 has_least_sort_for o,w1 );

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

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;

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

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

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

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;

end;
attr SM is regular means :Def13: :: OSALG_1:def 13

for om being OperSymbol of SM holds om is regular ;

for om being OperSymbol of SM holds om is regular ;

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

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 )

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

registration

ex b_{1} being monotone OrderSortedSign st b_{1} is regular
end;

cluster non empty non void V67() reflexive transitive antisymmetric order-sorted discernable monotone regular for OverloadedRSSign ;

existence ex b

proof end;

registration

for b_{1} being monotone OrderSortedSign st b_{1} is op-discrete holds

b_{1} is regular
by Th12;

end;

cluster non empty non void order-sorted discernable op-discrete monotone -> monotone regular for OverloadedRSSign ;

coherence for b

b

registration

let SR be monotone regular OrderSortedSign;

coherence

for b_{1} being OperSymbol of SR holds b_{1} is regular
by Def13;

end;
coherence

for b

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

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 ;

existence

ex b_{1} being OperSymbol of SR st b_{1} has_least_args_for o,w1
by A1, Def12;

uniqueness

for b_{1}, b_{2} being OperSymbol of SR st b_{1} has_least_args_for o,w1 & b_{2} has_least_args_for o,w1 holds

b_{1} = b_{2}
by Th13;

end;
let o be OperSymbol of SR;

let w1 be Element of the carrier of SR * ;

assume A1: w1 <= the_arity_of o ;

existence

ex b

uniqueness

for b

b

:: 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 b_{4} being OperSymbol of SR holds

( b_{4} = LBound (o,w1) iff b_{4} has_least_args_for o,w1 );

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 b

( b

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

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 ;

coherence

the carrier of R --> z is ManySortedSet of the carrier of R;

end;
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 the carrier of R --> z;

coherence

the carrier of R --> z is ManySortedSet of the carrier of R;

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

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

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;

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

for s1, s2 being Element of R st s1 <= s2 holds

M . s1 c= M . s2;

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

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;

for z being non empty set holds ConstOSSet (R,z) is order-sorted by Th15;

registration

let R be non empty Poset;

ex b_{1} being ManySortedSet of R st b_{1} is order-sorted

end;
cluster non empty Relation-like the carrier of R -defined Function-like V25( the carrier of R) order-sorted for set ;

existence ex b

proof end;

registration

let R be non empty Poset;

let z be non empty set ;

coherence

ConstOSSet (R,z) is order-sorted by Th16;

end;
let z be non empty set ;

coherence

ConstOSSet (R,z) is order-sorted by Th16;

definition
end;

registration

let R be non empty Poset;

not for b_{1} being OrderSortedSet of R holds b_{1} is V8()

end;
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 b

proof end;

definition

let S be OrderSortedSign;

let M be MSAlgebra over S;

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

for s1, s2 being SortSymbol of S st s1 <= s2 holds

the Sorts of M . s1 c= the Sorts of M . s2;

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

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;

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;

ex b_{1} being strict non-empty MSAlgebra over S st

( the Sorts of b_{1} = ConstOSSet (S,z) & the Charact of b_{1} = CH )

for b_{1}, b_{2} being strict non-empty MSAlgebra over S st the Sorts of b_{1} = ConstOSSet (S,z) & the Charact of b_{1} = CH & the Sorts of b_{2} = ConstOSSet (S,z) & the Charact of b_{2} = CH holds

b_{1} = b_{2}
;

end;
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 ( the Sorts of it = ConstOSSet (S,z) & the Charact of it = CH );

ex b

( the Sorts of b

proof end;

uniqueness for b

b

:: 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 b_{4} being strict non-empty MSAlgebra over S holds

( b_{4} = ConstOSA (S,z,CH) iff ( the Sorts of b_{4} = ConstOSSet (S,z) & the Charact of b_{4} = CH ) );

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 b

( b

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

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;

existence

ex b_{1} being MSAlgebra over S st

( b_{1} is strict & b_{1} is non-empty & b_{1} is order-sorted )

end;
existence

ex b

( b

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

coherence

ConstOSA (S,z,CH) is order-sorted by Th18;

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

coherence

ConstOSA (S,z,CH) is order-sorted by Th18;

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;

for M being MSAlgebra over S holds M is order-sorted by ORDERS_3:1;

registration

let S be discrete OrderSortedSign;

coherence

for b_{1} being MSAlgebra over S holds b_{1} is order-sorted
by Th19;

end;
coherence

for b

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

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;

for b_{1}, b_{2} being strict OSAlgebra of OSSign S0 st the Sorts of b_{1} = the Sorts of M & the Charact of b_{1} = the Charact of M & the Sorts of b_{2} = the Sorts of M & the Charact of b_{2} = the Charact of M holds

b_{1} = b_{2}
;

existence

ex b_{1} being strict OSAlgebra of OSSign S0 st

( the Sorts of b_{1} = the Sorts of M & the Charact of b_{1} = the Charact of M )

end;
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 ( the Sorts of it = the Sorts of M & the Charact of it = the Charact of M );

for b

b

existence

ex b

( the Sorts of b

proof end;

:: deftheorem defines OSAlg OSALG_1:def 19 :

for S0 being non empty non void ManySortedSign

for M being MSAlgebra over S0

for b_{3} being strict OSAlgebra of OSSign S0 holds

( b_{3} = OSAlg M iff ( the Sorts of b_{3} = the Sorts of M & the Charact of b_{3} = the Charact of M ) );

for S0 being non empty non void ManySortedSign

for M being MSAlgebra over S0

for b

( b

:: 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

:: 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

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;

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;
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 ( o1 ~= o2 & the_arity_of o1 <= the_arity_of o2 & the_result_sort_of o1 <= the_result_sort_of o2 );

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

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

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

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)

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)

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

:: 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

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

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

for o1, o2 being OperSymbol of S st o1 <= o2 holds

(Den (o2,A)) | (Args (o1,A)) = Den (o1,A);

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

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

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

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;

ex b_{1} being strict OSAlgebra of S st

( the Sorts of b_{1} = ConstOSSet (S,z) & ( for o being OperSymbol of S holds Den (o,b_{1}) = (Args (o,b_{1})) --> z1 ) )

for b_{1}, b_{2} being strict OSAlgebra of S st the Sorts of b_{1} = ConstOSSet (S,z) & ( for o being OperSymbol of S holds Den (o,b_{1}) = (Args (o,b_{1})) --> z1 ) & the Sorts of b_{2} = ConstOSSet (S,z) & ( for o being OperSymbol of S holds Den (o,b_{2}) = (Args (o,b_{2})) --> z1 ) holds

b_{1} = b_{2}

end;
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 ( the Sorts of it = ConstOSSet (S,z) & ( for o being OperSymbol of S holds Den (o,it) = (Args (o,it)) --> z1 ) );

ex b

( the Sorts of b

proof end;

uniqueness for b

b

proof 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 b_{4} being strict OSAlgebra of S holds

( b_{4} = TrivialOSA (S,z,z1) iff ( the Sorts of b_{4} = ConstOSSet (S,z) & ( for o being OperSymbol of S holds Den (o,b_{4}) = (Args (o,b_{4})) --> z1 ) ) );

for S being OrderSortedSign

for z being non empty set

for z1 being Element of z

for b

( b

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 )

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;

existence

ex b_{1} being OSAlgebra of S st

( b_{1} is monotone & b_{1} is strict & b_{1} is non-empty )

end;
existence

ex b

( b

proof end;

registration

let S be OrderSortedSign;

let z be non empty set ;

let z1 be Element of z;

coherence

( TrivialOSA (S,z,z1) is monotone & TrivialOSA (S,z,z1) is non-empty ) by Th29;

end;
let z be non empty set ;

let z1 be Element of z;

coherence

( TrivialOSA (S,z,z1) is monotone & TrivialOSA (S,z,z1) is non-empty ) by Th29;

definition

let S be OrderSortedSign;

Class the Overloading of S is non empty Subset-Family of the carrier' of S ;

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

Class the Overloading of S is non empty Subset-Family of the carrier' of S ;

:: deftheorem defines OperNames OSALG_1:def 23 :

for S being OrderSortedSign holds OperNames S = Class the Overloading of S;

for S being OrderSortedSign holds OperNames S = Class the Overloading of S;

registration

let S be OrderSortedSign;

coherence

for b_{1} being Element of OperNames S holds not b_{1} is empty

end;
coherence

for b

proof end;

definition

let S be OrderSortedSign;

let op1 be OperSymbol of S;

coherence

Class ( the Overloading of S,op1) is OperName of S by EQREL_1:def 3;

end;
let op1 be OperSymbol of S;

coherence

Class ( the Overloading of S,op1) is OperName of S by EQREL_1:def 3;

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

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

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 )

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 )

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 b_{1} being Element of o holds b_{1} is OperSymbol of S

end;
let o be OperName of S;

:: original: Element

redefine mode Element of o -> OperSymbol of S;

coherence

for b

proof 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 )

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)

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 ;

ex b_{1} being Element of on st

for op being Element of on st w <= the_arity_of op holds

b_{1} = LBound (op,w)

for b_{1}, b_{2} being Element of on st ( for op being Element of on st w <= the_arity_of op holds

b_{1} = LBound (op,w) ) & ( for op being Element of on st w <= the_arity_of op holds

b_{2} = LBound (op,w) ) holds

b_{1} = b_{2}

end;
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 for op being Element of on st w <= the_arity_of op holds

it = LBound (op,w);

ex b

for op being Element of on st w <= the_arity_of op holds

b

proof end;

uniqueness for b

b

b

b

proof 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 b_{4} being Element of on holds

( b_{4} = LBound (on,w) iff for op being Element of on st w <= the_arity_of op holds

b_{4} = LBound (op,w) );

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 b

( b

b

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

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;

:: constant -> order-sorted ManySortedSet of R