:: OSALG_1 semantic presentation
begin
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
proof
rng p c= I ;
then rng p c= dom f by PARTFUN1:def_2;
then dom (f * p) = dom p by RELAT_1:27
.= Seg (len p) by FINSEQ_1:def_3 ;
hence f * p is FinSequence-like by FINSEQ_1:def_2; ::_thesis: verum
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
let I be set ; ::_thesis: for f being ManySortedSet of I
for p being FinSequence of I holds
( dom (f * p) = dom p & len (f * p) = len p )
let f be ManySortedSet of I; ::_thesis: for p being FinSequence of I holds
( dom (f * p) = dom p & len (f * p) = len p )
let p be FinSequence of I; ::_thesis: ( dom (f * p) = dom p & len (f * p) = len p )
reconsider q = f * p as FinSequence ;
rng p c= I ;
then rng p c= dom f by PARTFUN1:def_2;
then len q = len p by FINSEQ_2:29;
hence ( dom (f * p) = dom p & len (f * p) = len p ) by FINSEQ_3:29; ::_thesis: verum
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;
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;
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;
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
let A, O be non empty set ; ::_thesis: 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 )
let R be Order of A; ::_thesis: 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 )
let Ol be Equivalence_Relation of O; ::_thesis: 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 )
let f be Function of O,(A *); ::_thesis: 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 )
let g be Function of O,A; ::_thesis: ( 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 )
set RS0 = OverloadedRSSign(# A,R,O,Ol,f,g #);
A1: field the InternalRel of OverloadedRSSign(# A,R,O,Ol,f,g #) = the carrier of OverloadedRSSign(# A,R,O,Ol,f,g #) by ORDERS_1:12;
then A2: the InternalRel of OverloadedRSSign(# A,R,O,Ol,f,g #) is_antisymmetric_in the carrier of OverloadedRSSign(# A,R,O,Ol,f,g #) by RELAT_2:def_12;
( the InternalRel of OverloadedRSSign(# A,R,O,Ol,f,g #) is_reflexive_in the carrier of OverloadedRSSign(# A,R,O,Ol,f,g #) & the InternalRel of OverloadedRSSign(# A,R,O,Ol,f,g #) is_transitive_in the carrier of OverloadedRSSign(# A,R,O,Ol,f,g #) ) by A1, RELAT_2:def_9, RELAT_2:def_16;
hence ( 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 ) by A2, ORDERS_2:def_2, ORDERS_2:def_3, ORDERS_2:def_4; ::_thesis: verum
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;
begin
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 )
proof
set A = the non empty set ;
set R = the Order of the non empty set ;
set O = the non empty set ;
set Ol = the Equivalence_Relation of the non empty set ;
set f = the Function of the non empty set ,( the non empty set *);
set g = the Function of the non empty set , the non empty set ;
take OverloadedRSSign(# the non empty set , the Order of the non empty set , the non empty set , the Equivalence_Relation of the non empty set , the Function of the non empty set ,( the non empty set *), the Function of the non empty set , the non empty set #) ; ::_thesis: ( OverloadedRSSign(# the non empty set , the Order of the non empty set , the non empty set , the Equivalence_Relation of the non empty set , the Function of the non empty set ,( the non empty set *), the Function of the non empty set , the non empty set #) is strict & not OverloadedRSSign(# the non empty set , the Order of the non empty set , the non empty set , the Equivalence_Relation of the non empty set , the Function of the non empty set ,( the non empty set *), the Function of the non empty set , the non empty set #) is empty & not OverloadedRSSign(# the non empty set , the Order of the non empty set , the non empty set , the Equivalence_Relation of the non empty set , the Function of the non empty set ,( the non empty set *), the Function of the non empty set , the non empty set #) is void & OverloadedRSSign(# the non empty set , the Order of the non empty set , the non empty set , the Equivalence_Relation of the non empty set , the Function of the non empty set ,( the non empty set *), the Function of the non empty set , the non empty set #) is order-sorted )
thus ( OverloadedRSSign(# the non empty set , the Order of the non empty set , the non empty set , the Equivalence_Relation of the non empty set , the Function of the non empty set ,( the non empty set *), the Function of the non empty set , the non empty set #) is strict & not OverloadedRSSign(# the non empty set , the Order of the non empty set , the non empty set , the Equivalence_Relation of the non empty set , the Function of the non empty set ,( the non empty set *), the Function of the non empty set , the non empty set #) is empty & not OverloadedRSSign(# the non empty set , the Order of the non empty set , the non empty set , the Equivalence_Relation of the non empty set , the Function of the non empty set ,( the non empty set *), the Function of the non empty set , the non empty set #) is void & OverloadedRSSign(# the non empty set , the Order of the non empty set , the non empty set , the Equivalence_Relation of the non empty set , the Function of the non empty set ,( the non empty set *), the Function of the non empty set , the non empty set #) is order-sorted ) by Def1; ::_thesis: verum
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
set X = the non empty non void OverloadedRSSign ;
take the non empty non void OverloadedRSSign ; ::_thesis: ( not the non empty non void OverloadedRSSign is empty & not the non empty non void OverloadedRSSign is void )
thus ( not the non empty non void OverloadedRSSign is empty & not the non empty non void OverloadedRSSign is void ) ; ::_thesis: verum
end;
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
proof
let x, y be OperSymbol of S; ::_thesis: ( [x,y] in the Overloading of S implies [y,x] in the Overloading of S )
field the Overloading of S = the carrier' of S by ORDERS_1:12;
then the Overloading of S is_symmetric_in the carrier' of S by RELAT_2:def_11;
hence ( [x,y] in the Overloading of S implies [y,x] in the Overloading of S ) by RELAT_2:def_3; ::_thesis: verum
end;
reflexivity
for x being OperSymbol of S holds [x,x] in the Overloading of S
proof
let x be OperSymbol of S; ::_thesis: [x,x] in the Overloading of S
field the Overloading of S = the carrier' of S by ORDERS_1:12;
then the Overloading of S is_reflexive_in the carrier' of S by RELAT_2:def_9;
hence [x,x] in the Overloading of S by RELAT_2:def_1; ::_thesis: verum
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 );
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
let S be non empty non void OverloadedMSSign ; ::_thesis: for o, o1, o2 being OperSymbol of S st o ~= o1 & o1 ~= o2 holds
o ~= o2
let o, o1, o2 be OperSymbol of S; ::_thesis: ( o ~= o1 & o1 ~= o2 implies o ~= o2 )
field the Overloading of S = the carrier' of S by ORDERS_1:12;
then A1: the Overloading of S is_transitive_in the carrier' of S by RELAT_2:def_16;
assume ( o ~= o1 & o1 ~= o2 ) ; ::_thesis: o ~= o2
then ( [o,o1] in the Overloading of S & [o1,o2] in the Overloading of S ) by Def2;
then [o,o2] in the Overloading of S by A1, RELAT_2:def_8;
hence o ~= o2 by Def2; ::_thesis: verum
end;
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 )
proof
let S be non empty non void OverloadedMSSign ; ::_thesis: ( S is op-discrete iff for x, y being OperSymbol of S st x ~= y holds
x = y )
set d = id the carrier' of S;
set opss = the carrier' of S;
set ol = the Overloading of S;
thus ( S is op-discrete implies for x, y being OperSymbol of S st x ~= y holds
x = y ) ::_thesis: ( ( for x, y being OperSymbol of S st x ~= y holds
x = y ) implies S is op-discrete )
proof
assume A1: S is op-discrete ; ::_thesis: for x, y being OperSymbol of S st x ~= y holds
x = y
let x, y be OperSymbol of S; ::_thesis: ( x ~= y implies x = y )
assume x ~= y ; ::_thesis: x = y
then [x,y] in the Overloading of S by Def2;
then [x,y] in id the carrier' of S by A1, Def4;
hence x = y by RELAT_1:def_10; ::_thesis: verum
end;
assume A2: for x, y being OperSymbol of S st x ~= y holds
x = y ; ::_thesis: S is op-discrete
now__::_thesis:_for_x,_y_being_set_holds_
(_(_[x,y]_in_the_Overloading_of_S_implies_(_x_in_the_carrier'_of_S_&_x_=_y_)_)_&_(_x_in_the_carrier'_of_S_&_x_=_y_implies_[x,y]_in_the_Overloading_of_S_)_)
let x, y be set ; ::_thesis: ( ( [x,y] in the Overloading of S implies ( x in the carrier' of S & x = y ) ) & ( x in the carrier' of S & x = y implies [x,y] in the Overloading of S ) )
thus ( [x,y] in the Overloading of S implies ( x in the carrier' of S & x = y ) ) ::_thesis: ( x in the carrier' of S & x = y implies [x,y] in the Overloading of S )
proof
assume A3: [x,y] in the Overloading of S ; ::_thesis: ( x in the carrier' of S & x = y )
then ex x1, y1 being set st
( [x,y] = [x1,y1] & x1 in the carrier' of S & y1 in the carrier' of S ) by RELSET_1:2;
then reconsider x2 = x, y2 = y as OperSymbol of S by XTUPLE_0:1;
x2 ~= y2 by A3, Def2;
hence ( x in the carrier' of S & x = y ) by A2; ::_thesis: verum
end;
assume ( x in the carrier' of S & x = y ) ; ::_thesis: [x,y] in the Overloading of S
hence [x,y] in the Overloading of S by Def2; ::_thesis: verum
end;
hence the Overloading of S = id the carrier' of S by RELAT_1:def_10; :: according to OSALG_1:def_4 ::_thesis: verum
end;
theorem Th4: :: OSALG_1:4
for S being non empty non void OverloadedMSSign st S is op-discrete holds
S is discernable
proof
let S be non empty non void OverloadedMSSign ; ::_thesis: ( S is op-discrete implies S is discernable )
assume A1: S is op-discrete ; ::_thesis: S is discernable
let x, y be OperSymbol of S; :: according to OSALG_1:def_3 ::_thesis: ( x ~= y & the_arity_of x = the_arity_of y & the_result_sort_of x = the_result_sort_of y implies x = y )
thus ( x ~= y & the_arity_of x = the_arity_of y & the_result_sort_of x = the_result_sort_of y implies x = y ) by A1, Th3; ::_thesis: verum
end;
begin
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
set s = OverloadedRSSign(# the carrier of S0,(id the carrier of S0), the carrier' of S0,(id the carrier' of S0), the Arity of S0, the ResultSort of S0 #);
reconsider s1 = OverloadedRSSign(# the carrier of S0,(id the carrier of S0), the carrier' of S0,(id the carrier' of S0), the Arity of S0, the ResultSort of S0 #) as non empty non void strict order-sorted OverloadedRSSign by Def1;
take s1 ; ::_thesis: ( the carrier of S0 = the carrier of s1 & id the carrier of S0 = the InternalRel of s1 & the carrier' of S0 = the carrier' of s1 & id the carrier' of S0 = the Overloading of s1 & the Arity of S0 = the Arity of s1 & the ResultSort of S0 = the ResultSort of s1 )
thus ( the carrier of S0 = the carrier of s1 & id the carrier of S0 = the InternalRel of s1 & the carrier' of S0 = the carrier' of s1 & id the carrier' of S0 = the Overloading of s1 & the Arity of S0 = the Arity of s1 & the ResultSort of S0 = the ResultSort of s1 ) ; ::_thesis: verum
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
let S0 be non empty non void ManySortedSign ; ::_thesis: ( OSSign S0 is discrete & OSSign S0 is op-discrete )
set s = OSSign S0;
set ol = the Overloading of (OSSign S0);
( the carrier of S0 = the carrier of (OSSign S0) & id the carrier of S0 = the InternalRel of (OSSign S0) ) by Def5;
hence OSSign S0 is discrete by ORDERS_3:def_1; ::_thesis: OSSign S0 is op-discrete
A1: the Overloading of (OSSign S0) = id the carrier' of S0 by Def5;
now__::_thesis:_for_x,_y_being_OperSymbol_of_(OSSign_S0)_st_x_~=_y_holds_
x_=_y
let x, y be OperSymbol of (OSSign S0); ::_thesis: ( x ~= y implies x = y )
assume x ~= y ; ::_thesis: x = y
then [x,y] in the Overloading of (OSSign S0) by Def2;
hence x = y by A1, RELAT_1:def_10; ::_thesis: verum
end;
hence OSSign S0 is op-discrete by Th3; ::_thesis: verum
end;
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 )
proof
set S0 = the non empty non void ManySortedSign ;
take s = OSSign the non empty non void ManySortedSign ; ::_thesis: ( s is discrete & s is op-discrete & s is discernable )
thus ( s is discrete & s is op-discrete ) by Th5; ::_thesis: s is discernable
hence s is discernable by Th4; ::_thesis: verum
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;
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;
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 & ( 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 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 & ( 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
let S be non empty Poset; ::_thesis: for w1, w2 being Element of the carrier of S * st w1 <= w2 & w2 <= w1 holds
w1 = w2
let w1, w2 be Element of the carrier of S * ; ::_thesis: ( w1 <= w2 & w2 <= w1 implies w1 = w2 )
assume that
A1: w1 <= w2 and
A2: w2 <= w1 ; ::_thesis: w1 = w2
len w1 = len w2 by A1, Def6;
then A3: dom w1 = dom w2 by FINSEQ_3:29;
for i being set st i in dom w1 holds
w1 . i = w2 . i
proof
let i be set ; ::_thesis: ( i in dom w1 implies w1 . i = w2 . i )
assume A4: i in dom w1 ; ::_thesis: w1 . i = w2 . i
reconsider s3 = w1 . i, s4 = w2 . i as Element of S by A3, A4, PARTFUN1:4;
( s3 <= s4 & s4 <= s3 ) by A1, A2, A3, A4, Def6;
hence w1 . i = w2 . i by ORDERS_2:2; ::_thesis: verum
end;
hence w1 = w2 by A3, FUNCT_1:2; ::_thesis: verum
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
let S be non empty Poset; ::_thesis: for w1, w2 being Element of the carrier of S * st S is discrete & w1 <= w2 holds
w1 = w2
let w1, w2 be Element of the carrier of S * ; ::_thesis: ( S is discrete & w1 <= w2 implies w1 = w2 )
assume that
A1: S is discrete and
A2: w1 <= w2 ; ::_thesis: w1 = w2
reconsider S1 = S as non empty discrete Poset by A1;
len w1 = len w2 by A2, Def6;
then A3: dom w1 = dom w2 by FINSEQ_3:29;
for i being set st i in dom w1 holds
w1 . i = w2 . i
proof
let i be set ; ::_thesis: ( i in dom w1 implies w1 . i = w2 . i )
assume A4: i in dom w1 ; ::_thesis: w1 . i = w2 . i
reconsider s3 = w1 . i, s4 = w2 . i as Element of S by A3, A4, PARTFUN1:4;
reconsider s5 = s3, s6 = s4 as Element of S1 ;
s3 <= s4 by A2, A4, Def6;
then s5 = s6 by ORDERS_3:1;
hence w1 . i = w2 . i ; ::_thesis: verum
end;
hence w1 = w2 by A3, FUNCT_1:2; ::_thesis: verum
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
let S be OrderSortedSign; ::_thesis: 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
let o1, o2 be OperSymbol of S; ::_thesis: ( S is discrete & o1 ~= o2 & the_arity_of o1 <= the_arity_of o2 & the_result_sort_of o1 <= the_result_sort_of o2 implies o1 = o2 )
assume A1: S is discrete ; ::_thesis: ( not o1 ~= o2 or not the_arity_of o1 <= the_arity_of o2 or not the_result_sort_of o1 <= the_result_sort_of o2 or o1 = o2 )
then reconsider S1 = S as discrete OrderSortedSign ;
reconsider s1 = the_result_sort_of o1, s2 = the_result_sort_of o2 as SortSymbol of S1 ;
assume that
A2: o1 ~= o2 and
A3: the_arity_of o1 <= the_arity_of o2 and
A4: the_result_sort_of o1 <= the_result_sort_of o2 ; ::_thesis: o1 = o2
A5: s1 = s2 by A4, ORDERS_3:1;
the_arity_of o1 = the_arity_of o2 by A1, A3, Th7;
hence o1 = o2 by A2, A5, Def3; ::_thesis: verum
end;
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 & 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;
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
proof
let S be OrderSortedSign; ::_thesis: ( S is op-discrete implies S is monotone )
set ol = the Overloading of S;
assume S is op-discrete ; ::_thesis: S is monotone
then A1: the Overloading of S = id the carrier' of S by Def4;
let o be OperSymbol of S; :: according to OSALG_1:def_8 ::_thesis: o is monotone
let o2 be OperSymbol of S; :: according to OSALG_1:def_7 ::_thesis: ( o ~= o2 & the_arity_of o <= the_arity_of o2 implies the_result_sort_of o <= the_result_sort_of o2 )
assume o ~= o2 ; ::_thesis: ( not the_arity_of o <= the_arity_of o2 or the_result_sort_of o <= the_result_sort_of o2 )
then [o,o2] in the Overloading of S by Def2;
hence ( not the_arity_of o <= the_arity_of o2 or the_result_sort_of o <= the_result_sort_of o2 ) by A1, RELAT_1:def_10; ::_thesis: verum
end;
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
proof
set S = the op-discrete OrderSortedSign;
take the op-discrete OrderSortedSign ; ::_thesis: the op-discrete OrderSortedSign is monotone
thus the op-discrete OrderSortedSign is monotone by Th9; ::_thesis: verum
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
set o = the OperSymbol of S;
take the OperSymbol of S ; ::_thesis: the OperSymbol of S is monotone
thus the OperSymbol of S is monotone by Def8; ::_thesis: verum
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
let S be OrderSortedSign; ::_thesis: for o1, o2 being OperSymbol of S st S is monotone & the_arity_of o1 = {} & o1 ~= o2 & the_arity_of o2 = {} holds
o1 = o2
let o1, o2 be OperSymbol of S; ::_thesis: ( S is monotone & the_arity_of o1 = {} & o1 ~= o2 & the_arity_of o2 = {} implies o1 = o2 )
assume that
A1: S is monotone and
A2: ( the_arity_of o1 = {} & o1 ~= o2 & the_arity_of o2 = {} ) ; ::_thesis: o1 = o2
( the_result_sort_of o1 <= the_result_sort_of o2 & the_result_sort_of o2 <= the_result_sort_of o1 ) by A1, A2, Def7;
then the_result_sort_of o1 = the_result_sort_of o2 by ORDERS_2:2;
hence o1 = o2 by A2, Def3; ::_thesis: verum
end;
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 & 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 ) );
predo1 has_least_sort_for o,w1 means :Def10: :: 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 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 & 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 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 & 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 * ;
predo1 has_least_rank_for o,w1 means :Def11: :: OSALG_1:def 11
( o1 has_least_args_for o,w1 & 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 & 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 & ( 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;
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 )
proof
let SM be monotone OrderSortedSign; ::_thesis: ( 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 )
hereby ::_thesis: ( ( 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 ) implies SM is regular )
assume A1: SM is regular ; ::_thesis: 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
let o be OperSymbol of SM; ::_thesis: 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
let w1 be Element of the carrier of SM * ; ::_thesis: ( w1 <= the_arity_of o implies ex o1 being OperSymbol of SM st o1 has_least_rank_for o,w1 )
assume A2: w1 <= the_arity_of o ; ::_thesis: ex o1 being OperSymbol of SM st o1 has_least_rank_for o,w1
o is regular by A1, Def13;
then consider o1 being OperSymbol of SM such that
A3: o1 has_least_args_for o,w1 by A2, Def12;
take o1 = o1; ::_thesis: o1 has_least_rank_for o,w1
o1 has_least_sort_for o,w1
proof
thus A4: ( o ~= o1 & w1 <= the_arity_of o1 ) by A3, Def9; :: according to OSALG_1:def_10 ::_thesis: for o2 being OperSymbol of SM st o ~= o2 & w1 <= the_arity_of o2 holds
the_result_sort_of o1 <= the_result_sort_of o2
let o2 be OperSymbol of SM; ::_thesis: ( o ~= o2 & w1 <= the_arity_of o2 implies the_result_sort_of o1 <= the_result_sort_of o2 )
assume that
A5: o ~= o2 and
A6: w1 <= the_arity_of o2 ; ::_thesis: the_result_sort_of o1 <= the_result_sort_of o2
A7: o1 ~= o2 by A4, A5, Th2;
the_arity_of o1 <= the_arity_of o2 by A3, A5, A6, Def9;
hence the_result_sort_of o1 <= the_result_sort_of o2 by A7, Def7; ::_thesis: verum
end;
hence o1 has_least_rank_for o,w1 by A3, Def11; ::_thesis: verum
end;
assume A8: 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 ; ::_thesis: SM is regular
let o be OperSymbol of SM; :: according to OSALG_1:def_13 ::_thesis: o is regular
thus o is monotone ; :: according to OSALG_1:def_12 ::_thesis: 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_args_for o,w1
let w1 be Element of the carrier of SM * ; ::_thesis: ( w1 <= the_arity_of o implies ex o1 being OperSymbol of SM st o1 has_least_args_for o,w1 )
assume w1 <= the_arity_of o ; ::_thesis: ex o1 being OperSymbol of SM st o1 has_least_args_for o,w1
then consider o1 being OperSymbol of SM such that
A9: o1 has_least_rank_for o,w1 by A8;
take o1 ; ::_thesis: o1 has_least_args_for o,w1
thus o1 has_least_args_for o,w1 by A9, Def11; ::_thesis: verum
end;
theorem Th12: :: OSALG_1:12
for SM being monotone OrderSortedSign st SM is op-discrete holds
SM is regular
proof
let SM be monotone OrderSortedSign; ::_thesis: ( SM is op-discrete implies SM is regular )
assume A1: SM is op-discrete ; ::_thesis: SM is regular
let om be OperSymbol of SM; :: according to OSALG_1:def_13 ::_thesis: om is regular
thus om is monotone ; :: according to OSALG_1:def_12 ::_thesis: for w1 being Element of the carrier of SM * st w1 <= the_arity_of om holds
ex o1 being OperSymbol of SM st o1 has_least_args_for om,w1
let wm1 be Element of the carrier of SM * ; ::_thesis: ( wm1 <= the_arity_of om implies ex o1 being OperSymbol of SM st o1 has_least_args_for om,wm1 )
assume A2: wm1 <= the_arity_of om ; ::_thesis: ex o1 being OperSymbol of SM st o1 has_least_args_for om,wm1
om has_least_args_for om,wm1
proof
thus ( om ~= om & wm1 <= the_arity_of om ) by A2; :: according to OSALG_1:def_9 ::_thesis: for o2 being OperSymbol of SM st om ~= o2 & wm1 <= the_arity_of o2 holds
the_arity_of om <= the_arity_of o2
let om2 be OperSymbol of SM; ::_thesis: ( om ~= om2 & wm1 <= the_arity_of om2 implies the_arity_of om <= the_arity_of om2 )
assume that
A3: om ~= om2 and
wm1 <= the_arity_of om2 ; ::_thesis: the_arity_of om <= the_arity_of om2
thus the_arity_of om <= the_arity_of om2 by A1, A3, Th3; ::_thesis: verum
end;
hence ex o1 being OperSymbol of SM st o1 has_least_args_for om,wm1 ; ::_thesis: verum
end;
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
proof
set SM = the op-discrete OrderSortedSign;
take the op-discrete OrderSortedSign ; ::_thesis: the op-discrete OrderSortedSign is regular
thus the op-discrete OrderSortedSign is regular by Th12; ::_thesis: verum
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 o3, o, 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
let SR be monotone regular OrderSortedSign; ::_thesis: 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 & o4 has_least_args_for o,w1 holds
o3 = o4
let o3, o, o4 be OperSymbol of SR; ::_thesis: 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
let w1 be Element of the carrier of SR * ; ::_thesis: ( o3 has_least_args_for o,w1 & o4 has_least_args_for o,w1 implies o3 = o4 )
assume that
A1: o3 has_least_args_for o,w1 and
A2: o4 has_least_args_for o,w1 ; ::_thesis: o3 = o4
A3: o ~= o3 by A1, Def9;
A4: o ~= o4 by A2, Def9;
then A5: o3 ~= o4 by A3, Th2;
w1 <= the_arity_of o3 by A1, Def9;
then A6: the_arity_of o4 <= the_arity_of o3 by A2, A3, Def9;
then A7: the_result_sort_of o4 <= the_result_sort_of o3 by A5, Def7;
w1 <= the_arity_of o4 by A2, Def9;
then A8: the_arity_of o3 <= the_arity_of o4 by A1, A4, Def9;
then A9: the_arity_of o3 = the_arity_of o4 by A6, Th6;
the_result_sort_of o3 <= the_result_sort_of o4 by A5, A8, Def7;
then the_result_sort_of o3 = the_result_sort_of o4 by A7, ORDERS_2:2;
hence o3 = o4 by A5, A9, Def3; ::_thesis: verum
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
let SR be monotone regular OrderSortedSign; ::_thesis: 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
let o be OperSymbol of SR; ::_thesis: 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
let w1 be Element of the carrier of SR * ; ::_thesis: ( w1 <= the_arity_of o implies LBound (o,w1) has_least_rank_for o,w1 )
assume A1: w1 <= the_arity_of o ; ::_thesis: LBound (o,w1) has_least_rank_for o,w1
then consider o1 being OperSymbol of SR such that
A2: o1 has_least_rank_for o,w1 by Th11;
o1 has_least_args_for o,w1 by A2, Def11;
hence LBound (o,w1) has_least_rank_for o,w1 by A1, A2, Def14; ::_thesis: verum
end;
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
the carrier of R = dom ( the carrier of R --> z) by FUNCT_2:def_1;
hence the carrier of R --> z is ManySortedSet of the carrier of R by PARTFUN1:def_2; ::_thesis: verum
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
let R be non empty Poset; ::_thesis: 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 ) )
let z be non empty set ; ::_thesis: ( 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 ) )
set x = ConstOSSet (R,z);
set D = the carrier of R --> z;
for s being set st s in the carrier of R holds
not (ConstOSSet (R,z)) . s is empty by FUNCOP_1:7;
hence ConstOSSet (R,z) is V8() by PBOOLE:def_13; ::_thesis: for s1, s2 being Element of R st s1 <= s2 holds
(ConstOSSet (R,z)) . s1 c= (ConstOSSet (R,z)) . s2
let s1, s2 be Element of R; ::_thesis: ( s1 <= s2 implies (ConstOSSet (R,z)) . s1 c= (ConstOSSet (R,z)) . s2 )
( the carrier of R --> z) . s1 = z by FUNCOP_1:7
.= ( the carrier of R --> z) . s2 by FUNCOP_1:7 ;
hence ( s1 <= s2 implies (ConstOSSet (R,z)) . s1 c= (ConstOSSet (R,z)) . s2 ) ; ::_thesis: verum
end;
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
proof
let R be non empty Poset; ::_thesis: for z being non empty set holds ConstOSSet (R,z) is order-sorted
let z be non empty set ; ::_thesis: ConstOSSet (R,z) is order-sorted
set x = ConstOSSet (R,z);
for s1, s2 being Element of R st s1 <= s2 holds
(ConstOSSet (R,z)) . s1 c= (ConstOSSet (R,z)) . s2 by Th15;
hence ConstOSSet (R,z) is order-sorted by Def16; ::_thesis: verum
end;
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
set z = the non empty set ;
take ConstOSSet (R, the non empty set ) ; ::_thesis: ConstOSSet (R, the non empty set ) is order-sorted
thus ConstOSSet (R, the non empty set ) is order-sorted by Th16; ::_thesis: verum
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
take ConstOSSet (R,1) ; ::_thesis: ConstOSSet (R,1) is V8()
thus ConstOSSet (R,1) is V8() by Th15; ::_thesis: verum
end;
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 )
proof
let S be OrderSortedSign; ::_thesis: for M being MSAlgebra over S holds
( M is order-sorted iff the Sorts of M is OrderSortedSet of S )
let M be MSAlgebra over S; ::_thesis: ( M is order-sorted iff the Sorts of M is OrderSortedSet of S )
set So = the Sorts of M;
reconsider So1 = the Sorts of M as ManySortedSet of S ;
thus ( M is order-sorted implies the Sorts of M is OrderSortedSet of S ) ::_thesis: ( the Sorts of M is OrderSortedSet of S implies M is order-sorted )
proof
assume A1: M is order-sorted ; ::_thesis: the Sorts of M is OrderSortedSet of S
So1 is order-sorted
proof
let s1 be SortSymbol of S; :: according to OSALG_1:def_16 ::_thesis: for s2 being Element of S st s1 <= s2 holds
So1 . s1 c= So1 . s2
let s2 be SortSymbol of S; ::_thesis: ( s1 <= s2 implies So1 . s1 c= So1 . s2 )
thus ( s1 <= s2 implies So1 . s1 c= So1 . s2 ) by A1, Def17; ::_thesis: verum
end;
hence the Sorts of M is OrderSortedSet of S ; ::_thesis: verum
end;
assume A2: the Sorts of M is OrderSortedSet of S ; ::_thesis: M is order-sorted
let s1 be SortSymbol of S; :: according to OSALG_1:def_17 ::_thesis: for s2 being SortSymbol of S st s1 <= s2 holds
the Sorts of M . s1 c= the Sorts of M . s2
let s2 be SortSymbol of S; ::_thesis: ( s1 <= s2 implies the Sorts of M . s1 c= the Sorts of M . s2 )
thus ( s1 <= s2 implies the Sorts of M . s1 c= the Sorts of M . s2 ) by A2, Def16; ::_thesis: verum
end;
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
for i being set st i in the carrier of S holds
not (ConstOSSet (S,z)) . i is empty by FUNCOP_1:7;
then ConstOSSet (S,z) is V8() by PBOOLE:def_13;
then reconsider T = MSAlgebra(# (ConstOSSet (S,z)),CH #) as strict non-empty MSAlgebra over S by MSUALG_1:def_3;
take T ; ::_thesis: ( the Sorts of T = ConstOSSet (S,z) & the Charact of T = CH )
thus ( the Sorts of T = ConstOSSet (S,z) & the Charact of T = CH ) ; ::_thesis: verum
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
let S be OrderSortedSign; ::_thesis: 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
let z be non empty set ; ::_thesis: 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
let CH be ManySortedFunction of ((ConstOSSet (S,z)) #) * the Arity of S,(ConstOSSet (S,z)) * the ResultSort of S; ::_thesis: ConstOSA (S,z,CH) is order-sorted
the Sorts of (ConstOSA (S,z,CH)) = ConstOSSet (S,z) by Def18;
hence ConstOSA (S,z,CH) is order-sorted by Th17; ::_thesis: verum
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
set z = the non empty set ;
set CH = the ManySortedFunction of ((ConstOSSet (S, the non empty set )) #) * the Arity of S,(ConstOSSet (S, the non empty set )) * the ResultSort of S;
take ConstOSA (S, the non empty set , the ManySortedFunction of ((ConstOSSet (S, the non empty set )) #) * the Arity of S,(ConstOSSet (S, the non empty set )) * the ResultSort of S) ; ::_thesis: ( ConstOSA (S, the non empty set , the ManySortedFunction of ((ConstOSSet (S, the non empty set )) #) * the Arity of S,(ConstOSSet (S, the non empty set )) * the ResultSort of S) is strict & ConstOSA (S, the non empty set , the ManySortedFunction of ((ConstOSSet (S, the non empty set )) #) * the Arity of S,(ConstOSSet (S, the non empty set )) * the ResultSort of S) is non-empty & ConstOSA (S, the non empty set , the ManySortedFunction of ((ConstOSSet (S, the non empty set )) #) * the Arity of S,(ConstOSSet (S, the non empty set )) * the ResultSort of S) is order-sorted )
thus ( ConstOSA (S, the non empty set , the ManySortedFunction of ((ConstOSSet (S, the non empty set )) #) * the Arity of S,(ConstOSSet (S, the non empty set )) * the ResultSort of S) is strict & ConstOSA (S, the non empty set , the ManySortedFunction of ((ConstOSSet (S, the non empty set )) #) * the Arity of S,(ConstOSSet (S, the non empty set )) * the ResultSort of S) is non-empty & ConstOSA (S, the non empty set , the ManySortedFunction of ((ConstOSSet (S, the non empty set )) #) * the Arity of S,(ConstOSSet (S, the non empty set )) * the ResultSort of S) is order-sorted ) by Th18; ::_thesis: verum
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
proof
let S be discrete OrderSortedSign; ::_thesis: for M being MSAlgebra over S holds M is order-sorted
let M be MSAlgebra over S; ::_thesis: M is order-sorted
let s1, s2 be SortSymbol of S; :: according to OSALG_1:def_17 ::_thesis: ( s1 <= s2 implies the Sorts of M . s1 c= the Sorts of M . s2 )
assume s1 <= s2 ; ::_thesis: the Sorts of M . s1 c= the Sorts of M . s2
hence the Sorts of M . s1 c= the Sorts of M . s2 by ORDERS_3:1; ::_thesis: verum
end;
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
let S be OrderSortedSign; ::_thesis: 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
let w1, w2 be Element of the carrier of S * ; ::_thesis: for A being OSAlgebra of S st w1 <= w2 holds
( the Sorts of A #) . w1 c= ( the Sorts of A #) . w2
let A be OSAlgebra of S; ::_thesis: ( w1 <= w2 implies ( the Sorts of A #) . w1 c= ( the Sorts of A #) . w2 )
set iw1 = the Sorts of A * w1;
set iw2 = the Sorts of A * w2;
assume A1: w1 <= w2 ; ::_thesis: ( the Sorts of A #) . w1 c= ( the Sorts of A #) . w2
then A2: len w1 = len w2 by Def6;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in ( the Sorts of A #) . w1 or x in ( the Sorts of A #) . w2 )
assume x in ( the Sorts of A #) . w1 ; ::_thesis: x in ( the Sorts of A #) . w2
then x in product ( the Sorts of A * w1) by FINSEQ_2:def_5;
then consider g being Function such that
A3: x = g and
A4: dom g = dom ( the Sorts of A * w1) and
A5: for y being set st y in dom ( the Sorts of A * w1) holds
g . y in ( the Sorts of A * w1) . y by CARD_3:def_5;
A6: dom ( the Sorts of A * w1) = dom w1 by Lm1
.= dom w2 by A2, FINSEQ_3:29
.= dom ( the Sorts of A * w2) by Lm1 ;
for y being set st y in dom ( the Sorts of A * w2) holds
g . y in ( the Sorts of A * w2) . y
proof
let y be set ; ::_thesis: ( y in dom ( the Sorts of A * w2) implies g . y in ( the Sorts of A * w2) . y )
assume A7: y in dom ( the Sorts of A * w2) ; ::_thesis: g . y in ( the Sorts of A * w2) . y
A8: y in dom w1 by A6, A7, Lm1;
then A9: ( the Sorts of A * w1) . y = the Sorts of A . (w1 . y) by FUNCT_1:13;
A10: y in dom w2 by A7, Lm1;
then A11: ( the Sorts of A * w2) . y = the Sorts of A . (w2 . y) by FUNCT_1:13;
reconsider s1 = w1 . y, s2 = w2 . y as SortSymbol of S by A8, A10, PARTFUN1:4;
s1 <= s2 by A1, A8, Def6;
then A12: the Sorts of A . (w1 . y) c= the Sorts of A . (w2 . y) by Def17;
g . y in ( the Sorts of A * w1) . y by A5, A6, A7;
hence g . y in ( the Sorts of A * w2) . y by A9, A11, A12; ::_thesis: verum
end;
then g in product ( the Sorts of A * w2) by A4, A6, CARD_3:def_5;
hence x in ( the Sorts of A #) . w2 by A3, FINSEQ_2:def_5; ::_thesis: verum
end;
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
set S1 = OSSign S0;
set s0 = the Sorts of M;
set c0 = the Charact of M;
A1: the carrier of S0 = the carrier of (OSSign S0) by Def5;
then reconsider s1 = the Sorts of M as ManySortedSet of (OSSign S0) ;
( the Arity of S0 = the Arity of (OSSign S0) & the ResultSort of (OSSign S0) = the ResultSort of S0 ) by Def5;
then reconsider c1 = the Charact of M as ManySortedFunction of (s1 #) * the Arity of (OSSign S0),s1 * the ResultSort of (OSSign S0) by A1, Def5;
MSAlgebra(# s1,c1 #) is order-sorted ;
hence 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 ) ; ::_thesis: verum
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 ) );
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
let S be OrderSortedSign; ::_thesis: for w1, w2, w3 being Element of the carrier of S * st w1 <= w2 & w2 <= w3 holds
w1 <= w3
let w1, w2, w3 be Element of the carrier of S * ; ::_thesis: ( w1 <= w2 & w2 <= w3 implies w1 <= w3 )
assume that
A1: w1 <= w2 and
A2: w2 <= w3 ; ::_thesis: w1 <= w3
A3: len w1 = len w2 by A1, Def6;
then A4: dom w1 = dom w2 by FINSEQ_3:29;
A5: len w2 = len w3 by A2, Def6;
then A6: dom w2 = dom w3 by FINSEQ_3:29;
for i being set st i in dom w1 holds
for s1, s2 being SortSymbol of S st s1 = w1 . i & s2 = w3 . i holds
s1 <= s2
proof
let i be set ; ::_thesis: ( i in dom w1 implies for s1, s2 being SortSymbol of S st s1 = w1 . i & s2 = w3 . i holds
s1 <= s2 )
assume A7: i in dom w1 ; ::_thesis: for s1, s2 being SortSymbol of S st s1 = w1 . i & s2 = w3 . i holds
s1 <= s2
reconsider s3 = w1 . i, s4 = w2 . i, s5 = w3 . i as SortSymbol of S by A4, A6, A7, PARTFUN1:4;
A8: ( s3 <= s4 & s4 <= s5 ) by A1, A2, A4, A7, Def6;
let s1, s2 be SortSymbol of S; ::_thesis: ( s1 = w1 . i & s2 = w3 . i implies s1 <= s2 )
assume ( s1 = w1 . i & s2 = w3 . i ) ; ::_thesis: s1 <= s2
hence s1 <= s2 by A8, ORDERS_2:3; ::_thesis: verum
end;
hence w1 <= w3 by A3, A5, Def6; ::_thesis: verum
end;
definition
let S be OrderSortedSign;
let o1, o2 be OperSymbol of S;
predo1 <= o2 means :Def20: :: 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 Def20 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
let S be OrderSortedSign; ::_thesis: for o1, o2 being OperSymbol of S st o1 <= o2 & o2 <= o1 holds
o1 = o2
let o1, o2 be OperSymbol of S; ::_thesis: ( o1 <= o2 & o2 <= o1 implies o1 = o2 )
assume that
A1: o1 <= o2 and
A2: o2 <= o1 ; ::_thesis: o1 = o2
( the_result_sort_of o1 <= the_result_sort_of o2 & the_result_sort_of o2 <= the_result_sort_of o1 ) by A1, A2, Def20;
then A3: the_result_sort_of o1 = the_result_sort_of o2 by ORDERS_2:2;
( the_arity_of o1 <= the_arity_of o2 & the_arity_of o2 <= the_arity_of o1 ) by A1, A2, Def20;
then A4: the_arity_of o1 = the_arity_of o2 by Th6;
o1 ~= o2 by A1, Def20;
hence o1 = o2 by A4, A3, Def3; ::_thesis: verum
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
proof
let S be OrderSortedSign; ::_thesis: for o1, o2, o3 being OperSymbol of S st o1 <= o2 & o2 <= o3 holds
o1 <= o3
let o1, o2, o3 be OperSymbol of S; ::_thesis: ( o1 <= o2 & o2 <= o3 implies o1 <= o3 )
assume A1: ( o1 <= o2 & o2 <= o3 ) ; ::_thesis: o1 <= o3
then ( o1 ~= o2 & o2 ~= o3 ) by Def20;
hence o1 ~= o3 by Th2; :: according to OSALG_1:def_20 ::_thesis: ( the_arity_of o1 <= the_arity_of o3 & the_result_sort_of o1 <= the_result_sort_of o3 )
( the_arity_of o1 <= the_arity_of o2 & the_arity_of o2 <= the_arity_of o3 ) by A1, Def20;
hence the_arity_of o1 <= the_arity_of o3 by Th21; ::_thesis: the_result_sort_of o1 <= the_result_sort_of o3
( the_result_sort_of o1 <= the_result_sort_of o2 & the_result_sort_of o2 <= the_result_sort_of o3 ) by A1, Def20;
hence the_result_sort_of o1 <= the_result_sort_of o3 by ORDERS_2:3; ::_thesis: verum
end;
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
let S be OrderSortedSign; ::_thesis: 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)
let o1, o2 be OperSymbol of S; ::_thesis: 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)
let A be OSAlgebra of S; ::_thesis: ( the_result_sort_of o1 <= the_result_sort_of o2 implies Result (o1,A) c= Result (o2,A) )
reconsider M = the Sorts of A as OrderSortedSet of S by Th17;
A1: Result (o2,A) = ( the Sorts of A * the ResultSort of S) . o2 by MSUALG_1:def_5
.= the Sorts of A . ( the ResultSort of S . o2) by FUNCT_2:15
.= the Sorts of A . (the_result_sort_of o2) by MSUALG_1:def_2 ;
assume the_result_sort_of o1 <= the_result_sort_of o2 ; ::_thesis: Result (o1,A) c= Result (o2,A)
then A2: M . (the_result_sort_of o1) c= M . (the_result_sort_of o2) by Def16;
Result (o1,A) = ( the Sorts of A * the ResultSort of S) . o1 by MSUALG_1:def_5
.= the Sorts of A . ( the ResultSort of S . o1) by FUNCT_2:15
.= the Sorts of A . (the_result_sort_of o1) by MSUALG_1:def_2 ;
hence Result (o1,A) c= Result (o2,A) by A2, A1; ::_thesis: verum
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
let S be OrderSortedSign; ::_thesis: 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)
let o1, o2 be OperSymbol of S; ::_thesis: for A being OSAlgebra of S st the_arity_of o1 <= the_arity_of o2 holds
Args (o1,A) c= Args (o2,A)
let A be OSAlgebra of S; ::_thesis: ( the_arity_of o1 <= the_arity_of o2 implies Args (o1,A) c= Args (o2,A) )
reconsider M = the Sorts of A as OrderSortedSet of S by Th17;
A1: (M #) . (the_arity_of o1) = (M #) . ( the Arity of S . o1) by MSUALG_1:def_1
.= ((M #) * the Arity of S) . o1 by FUNCT_2:15
.= Args (o1,A) by MSUALG_1:def_4 ;
A2: (M #) . (the_arity_of o2) = (M #) . ( the Arity of S . o2) by MSUALG_1:def_1
.= ((M #) * the Arity of S) . o2 by FUNCT_2:15
.= Args (o2,A) by MSUALG_1:def_4 ;
assume the_arity_of o1 <= the_arity_of o2 ; ::_thesis: Args (o1,A) c= Args (o2,A)
hence Args (o1,A) c= Args (o2,A) by A1, A2, Th20; ::_thesis: verum
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) )
proof
let S be OrderSortedSign; ::_thesis: 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) )
let o1, o2 be OperSymbol of S; ::_thesis: for A being OSAlgebra of S st o1 <= o2 holds
( Args (o1,A) c= Args (o2,A) & Result (o1,A) c= Result (o2,A) )
let A be OSAlgebra of S; ::_thesis: ( o1 <= o2 implies ( Args (o1,A) c= Args (o2,A) & Result (o1,A) c= Result (o2,A) ) )
assume o1 <= o2 ; ::_thesis: ( Args (o1,A) c= Args (o2,A) & Result (o1,A) c= Result (o2,A) )
then ( the_arity_of o1 <= the_arity_of o2 & the_result_sort_of o1 <= the_result_sort_of o2 ) by Def20;
hence ( Args (o1,A) c= Args (o2,A) & Result (o1,A) c= Result (o2,A) ) by Th24, Th25; ::_thesis: verum
end;
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) )
proof
let S be OrderSortedSign; ::_thesis: 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) )
let A be non-empty OSAlgebra of S; ::_thesis: ( A is monotone iff for o1, o2 being OperSymbol of S st o1 <= o2 holds
Den (o1,A) c= Den (o2,A) )
hereby ::_thesis: ( ( for o1, o2 being OperSymbol of S st o1 <= o2 holds
Den (o1,A) c= Den (o2,A) ) implies A is monotone )
assume A1: A is monotone ; ::_thesis: for o1, o2 being OperSymbol of S st o1 <= o2 holds
Den (o1,A) c= Den (o2,A)
let o1, o2 be OperSymbol of S; ::_thesis: ( o1 <= o2 implies Den (o1,A) c= Den (o2,A) )
assume o1 <= o2 ; ::_thesis: Den (o1,A) c= Den (o2,A)
then (Den (o2,A)) | (Args (o1,A)) = Den (o1,A) by A1, Def21;
hence Den (o1,A) c= Den (o2,A) by RELAT_1:59; ::_thesis: verum
end;
assume A2: for o1, o2 being OperSymbol of S st o1 <= o2 holds
Den (o1,A) c= Den (o2,A) ; ::_thesis: A is monotone
let o1 be OperSymbol of S; :: according to OSALG_1:def_21 ::_thesis: for o2 being OperSymbol of S st o1 <= o2 holds
(Den (o2,A)) | (Args (o1,A)) = Den (o1,A)
let o2 be OperSymbol of S; ::_thesis: ( o1 <= o2 implies (Den (o2,A)) | (Args (o1,A)) = Den (o1,A) )
assume A3: o1 <= o2 ; ::_thesis: (Den (o2,A)) | (Args (o1,A)) = Den (o1,A)
dom (Den (o1,A)) = Args (o1,A) by FUNCT_2:def_1;
hence (Den (o2,A)) | (Args (o1,A)) = (Den (o1,A)) | (Args (o1,A)) by A2, A3, GRFUNC_1:27
.= Den (o1,A) ;
::_thesis: verum
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
let S be OrderSortedSign; ::_thesis: for A being OSAlgebra of S st ( S is discrete or S is op-discrete ) holds
A is monotone
let A be OSAlgebra of S; ::_thesis: ( ( S is discrete or S is op-discrete ) implies A is monotone )
assume A1: ( S is discrete or S is op-discrete ) ; ::_thesis: A is monotone
let o1 be OperSymbol of S; :: according to OSALG_1:def_21 ::_thesis: for o2 being OperSymbol of S st o1 <= o2 holds
(Den (o2,A)) | (Args (o1,A)) = Den (o1,A)
let o2 be OperSymbol of S; ::_thesis: ( o1 <= o2 implies (Den (o2,A)) | (Args (o1,A)) = Den (o1,A) )
assume that
A2: o1 ~= o2 and
A3: ( the_arity_of o1 <= the_arity_of o2 & the_result_sort_of o1 <= the_result_sort_of o2 ) ; :: according to OSALG_1:def_20 ::_thesis: (Den (o2,A)) | (Args (o1,A)) = Den (o1,A)
o1 = o2
proof
percases ( S is discrete or S is op-discrete ) by A1;
suppose S is discrete ; ::_thesis: o1 = o2
hence o1 = o2 by A2, A3, Th8; ::_thesis: verum
end;
suppose S is op-discrete ; ::_thesis: o1 = o2
hence o1 = o2 by A2, Th3; ::_thesis: verum
end;
end;
end;
hence (Den (o2,A)) | (Args (o1,A)) = Den (o1,A) by RELSET_1:19; ::_thesis: verum
end;
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
set c = ConstOSSet (S,z);
deffunc H1( Element of the carrier' of S) -> Element of K10(K11(((((ConstOSSet (S,z)) #) * the Arity of S) . $1),{z1})) = ((((ConstOSSet (S,z)) #) * the Arity of S) . $1) --> z1;
consider ch2 being Function such that
A1: ( dom ch2 = the carrier' of S & ( for x being Element of the carrier' of S holds ch2 . x = H1(x) ) ) from FUNCT_1:sch_4();
reconsider ch4 = ch2 as ManySortedSet of the carrier' of S by A1, PARTFUN1:def_2, RELAT_1:def_18;
for i being set st i in the carrier' of S holds
ch4 . i is Function of ((((ConstOSSet (S,z)) #) * the Arity of S) . i),(((ConstOSSet (S,z)) * the ResultSort of S) . i)
proof
let i be set ; ::_thesis: ( i in the carrier' of S implies ch4 . i is Function of ((((ConstOSSet (S,z)) #) * the Arity of S) . i),(((ConstOSSet (S,z)) * the ResultSort of S) . i) )
assume i in the carrier' of S ; ::_thesis: ch4 . i is Function of ((((ConstOSSet (S,z)) #) * the Arity of S) . i),(((ConstOSSet (S,z)) * the ResultSort of S) . i)
then reconsider o = i as OperSymbol of S ;
the ResultSort of S . o in the carrier of S ;
then A2: o in the ResultSort of S " the carrier of S by FUNCT_2:38;
((ConstOSSet (S,z)) * the ResultSort of S) . o = (( the ResultSort of S " the carrier of S) --> z) . o by FUNCOP_1:19
.= z by A2, FUNCOP_1:7 ;
then A3: {z1} c= ((ConstOSSet (S,z)) * the ResultSort of S) . i by ZFMISC_1:31;
ch4 . i = H1(o) by A1;
hence ch4 . i is Function of ((((ConstOSSet (S,z)) #) * the Arity of S) . i),(((ConstOSSet (S,z)) * the ResultSort of S) . i) by A3, FUNCT_2:7; ::_thesis: verum
end;
then reconsider ch3 = ch4 as ManySortedFunction of ((ConstOSSet (S,z)) #) * the Arity of S,(ConstOSSet (S,z)) * the ResultSort of S by PBOOLE:def_15;
take T = ConstOSA (S,z,ch3); ::_thesis: ( the Sorts of T = ConstOSSet (S,z) & ( for o being OperSymbol of S holds Den (o,T) = (Args (o,T)) --> z1 ) )
thus A4: the Sorts of T = ConstOSSet (S,z) by Def18; ::_thesis: for o being OperSymbol of S holds Den (o,T) = (Args (o,T)) --> z1
let o be OperSymbol of S; ::_thesis: Den (o,T) = (Args (o,T)) --> z1
Den (o,T) = the Charact of T . o by MSUALG_1:def_6
.= ch3 . o by Def18
.= ((((ConstOSSet (S,z)) #) * the Arity of S) . o) --> z1 by A1
.= (Args (o,T)) --> z1 by A4, MSUALG_1:def_4 ;
hence Den (o,T) = (Args (o,T)) --> z1 ; ::_thesis: verum
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
let T1, T2 be strict OSAlgebra of S; ::_thesis: ( the Sorts of T1 = ConstOSSet (S,z) & ( for o being OperSymbol of S holds Den (o,T1) = (Args (o,T1)) --> z1 ) & the Sorts of T2 = ConstOSSet (S,z) & ( for o being OperSymbol of S holds Den (o,T2) = (Args (o,T2)) --> z1 ) implies T1 = T2 )
assume that
A5: the Sorts of T1 = ConstOSSet (S,z) and
A6: for o being OperSymbol of S holds Den (o,T1) = (Args (o,T1)) --> z1 ; ::_thesis: ( not the Sorts of T2 = ConstOSSet (S,z) or ex o being OperSymbol of S st not Den (o,T2) = (Args (o,T2)) --> z1 or T1 = T2 )
assume that
A7: the Sorts of T2 = ConstOSSet (S,z) and
A8: for o being OperSymbol of S holds Den (o,T2) = (Args (o,T2)) --> z1 ; ::_thesis: T1 = T2
now__::_thesis:_for_o1_being_set_st_o1_in_the_carrier'_of_S_holds_
the_Charact_of_T1_._o1_=_the_Charact_of_T2_._o1
let o1 be set ; ::_thesis: ( o1 in the carrier' of S implies the Charact of T1 . o1 = the Charact of T2 . o1 )
assume o1 in the carrier' of S ; ::_thesis: the Charact of T1 . o1 = the Charact of T2 . o1
then reconsider o = o1 as OperSymbol of S ;
thus the Charact of T1 . o1 = Den (o,T1) by MSUALG_1:def_6
.= (Args (o,T1)) --> z1 by A6
.= ((((ConstOSSet (S,z)) #) * the Arity of S) . o) --> z1 by A5, MSUALG_1:def_4
.= (Args (o,T2)) --> z1 by A7, MSUALG_1:def_4
.= Den (o,T2) by A8
.= the Charact of T2 . o1 by MSUALG_1:def_6 ; ::_thesis: verum
end;
hence T1 = T2 by A5, A7, PBOOLE:3; ::_thesis: verum
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
let S be OrderSortedSign; ::_thesis: 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 )
let z be non empty set ; ::_thesis: for z1 being Element of z holds
( TrivialOSA (S,z,z1) is non-empty & TrivialOSA (S,z,z1) is monotone )
let z1 be Element of z; ::_thesis: ( TrivialOSA (S,z,z1) is non-empty & TrivialOSA (S,z,z1) is monotone )
set A = TrivialOSA (S,z,z1);
the Sorts of (TrivialOSA (S,z,z1)) = ConstOSSet (S,z) by Def22;
then A1: the Sorts of (TrivialOSA (S,z,z1)) is V8() by Th15;
hence TrivialOSA (S,z,z1) is non-empty by MSUALG_1:def_3; ::_thesis: TrivialOSA (S,z,z1) is monotone
reconsider A1 = TrivialOSA (S,z,z1) as non-empty OSAlgebra of S by A1, MSUALG_1:def_3;
for o1, o2 being OperSymbol of S st o1 <= o2 holds
Den (o1,A1) c= Den (o2,A1)
proof
let o1, o2 be OperSymbol of S; ::_thesis: ( o1 <= o2 implies Den (o1,A1) c= Den (o2,A1) )
A2: Args (o1,(TrivialOSA (S,z,z1))) = (( the Sorts of (TrivialOSA (S,z,z1)) #) * the Arity of S) . o1 by MSUALG_1:def_4
.= ( the Sorts of (TrivialOSA (S,z,z1)) #) . ( the Arity of S . o1) by FUNCT_2:15
.= ( the Sorts of (TrivialOSA (S,z,z1)) #) . (the_arity_of o1) by MSUALG_1:def_1 ;
A3: Args (o2,(TrivialOSA (S,z,z1))) = (( the Sorts of (TrivialOSA (S,z,z1)) #) * the Arity of S) . o2 by MSUALG_1:def_4
.= ( the Sorts of (TrivialOSA (S,z,z1)) #) . ( the Arity of S . o2) by FUNCT_2:15
.= ( the Sorts of (TrivialOSA (S,z,z1)) #) . (the_arity_of o2) by MSUALG_1:def_1 ;
assume o1 <= o2 ; ::_thesis: Den (o1,A1) c= Den (o2,A1)
then A4: the_arity_of o1 <= the_arity_of o2 by Def20;
( Den (o1,(TrivialOSA (S,z,z1))) = (Args (o1,(TrivialOSA (S,z,z1)))) --> z1 & Den (o2,(TrivialOSA (S,z,z1))) = (Args (o2,(TrivialOSA (S,z,z1)))) --> z1 ) by Def22;
hence Den (o1,A1) c= Den (o2,A1) by A4, A2, A3, Th20, FUNCT_4:4; ::_thesis: verum
end;
hence TrivialOSA (S,z,z1) is monotone by Th27; ::_thesis: verum
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
set z = the non empty set ;
set z1 = the Element of the non empty set ;
take TrivialOSA (S, the non empty set , the Element of the non empty set ) ; ::_thesis: ( TrivialOSA (S, the non empty set , the Element of the non empty set ) is monotone & TrivialOSA (S, the non empty set , the Element of the non empty set ) is strict & TrivialOSA (S, the non empty set , the Element of the non empty set ) is non-empty )
thus ( TrivialOSA (S, the non empty set , the Element of the non empty set ) is monotone & TrivialOSA (S, the non empty set , the Element of the non empty set ) is strict & TrivialOSA (S, the non empty set , the Element of the non empty set ) is non-empty ) by Th29; ::_thesis: verum
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
let X be Element of OperNames S; ::_thesis: not X is empty
ex x being set st
( x in the carrier' of S & X = Class ( the Overloading of S,x) ) by EQREL_1:def_3;
hence not X is empty by EQREL_1:20; ::_thesis: verum
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
let S be OrderSortedSign; ::_thesis: for op1, op2 being OperSymbol of S holds
( op1 ~= op2 iff op2 in Class ( the Overloading of S,op1) )
let op1, op2 be OperSymbol of S; ::_thesis: ( op1 ~= op2 iff op2 in Class ( the Overloading of S,op1) )
( op1 ~= op2 iff [op2,op1] in the Overloading of S ) by Def2;
hence ( op1 ~= op2 iff op2 in Class ( the Overloading of S,op1) ) by EQREL_1:19; ::_thesis: verum
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
let S be OrderSortedSign; ::_thesis: for op1, op2 being OperSymbol of S holds
( op1 ~= op2 iff Name op1 = Name op2 )
let op1, op2 be OperSymbol of S; ::_thesis: ( op1 ~= op2 iff Name op1 = Name op2 )
( op2 in Class ( the Overloading of S,op1) iff Class ( the Overloading of S,op1) = Class ( the Overloading of S,op2) ) by EQREL_1:23;
hence ( op1 ~= op2 iff Name op1 = Name op2 ) by Th30; ::_thesis: verum
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
let S be OrderSortedSign; ::_thesis: for X being set holds
( X is OperName of S iff ex op1 being OperSymbol of S st X = Name op1 )
let X be set ; ::_thesis: ( X is OperName of S iff ex op1 being OperSymbol of S st X = Name op1 )
hereby ::_thesis: ( ex op1 being OperSymbol of S st X = Name op1 implies X is OperName of S )
assume X is OperName of S ; ::_thesis: ex x1 being OperSymbol of S st X = Name x1
then consider x being set such that
A1: x in the carrier' of S and
A2: X = Class ( the Overloading of S,x) by EQREL_1:def_3;
reconsider x1 = x as OperSymbol of S by A1;
take x1 = x1; ::_thesis: X = Name x1
thus X = Name x1 by A2; ::_thesis: verum
end;
given op1 being OperSymbol of S such that A3: X = Name op1 ; ::_thesis: X is OperName of S
thus X is OperName of S by A3; ::_thesis: verum
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
let x be Element of o; ::_thesis: x is OperSymbol of S
thus x is OperSymbol of S ; ::_thesis: verum
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
let S be OrderSortedSign; ::_thesis: for on being OperName of S
for op being OperSymbol of S holds
( op is Element of on iff Name op = on )
let on be OperName of S; ::_thesis: for op being OperSymbol of S holds
( op is Element of on iff Name op = on )
let op1 be OperSymbol of S; ::_thesis: ( op1 is Element of on iff Name op1 = on )
hereby ::_thesis: ( Name op1 = on implies op1 is Element of on )
assume op1 is Element of on ; ::_thesis: Name op1 = on
then reconsider op = op1 as Element of on ;
( ex op2 being set st
( op2 in the carrier' of S & on = Class ( the Overloading of S,op2) ) & Name op = Class ( the Overloading of S,op) ) by EQREL_1:def_3;
hence Name op1 = on by EQREL_1:23; ::_thesis: verum
end;
assume Name op1 = on ; ::_thesis: op1 is Element of on
hence op1 is Element of on by EQREL_1:20; ::_thesis: verum
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
let SR be monotone regular OrderSortedSign; ::_thesis: 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)
let op1, op2 be OperSymbol of SR; ::_thesis: 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)
let w be Element of the carrier of SR * ; ::_thesis: ( op1 ~= op2 & w <= the_arity_of op1 & w <= the_arity_of op2 implies LBound (op1,w) = LBound (op2,w) )
assume that
A1: op1 ~= op2 and
A2: w <= the_arity_of op1 and
A3: w <= the_arity_of op2 ; ::_thesis: LBound (op1,w) = LBound (op2,w)
set Lo1 = LBound (op1,w);
set Lo2 = LBound (op2,w);
A4: LBound (op1,w) has_least_args_for op1,w by A2, Def14;
then A5: op1 ~= LBound (op1,w) by Def9;
A6: LBound (op2,w) has_least_args_for op2,w by A3, Def14;
then A7: for o2 being OperSymbol of SR st op2 ~= o2 & w <= the_arity_of o2 holds
the_arity_of (LBound (op2,w)) <= the_arity_of o2 by Def9;
op2 ~= LBound (op2,w) by A6, Def9;
then A8: op1 ~= LBound (op2,w) by A1, Th2;
then A9: LBound (op1,w) ~= LBound (op2,w) by A5, Th2;
w <= the_arity_of (LBound (op1,w)) by A4, Def9;
then A10: the_arity_of (LBound (op2,w)) <= the_arity_of (LBound (op1,w)) by A1, A5, A7, Th2;
then A11: the_result_sort_of (LBound (op2,w)) <= the_result_sort_of (LBound (op1,w)) by A9, Def7;
w <= the_arity_of (LBound (op2,w)) by A6, Def9;
then A12: the_arity_of (LBound (op1,w)) <= the_arity_of (LBound (op2,w)) by A4, A8, Def9;
then A13: the_arity_of (LBound (op1,w)) = the_arity_of (LBound (op2,w)) by A10, Th6;
the_result_sort_of (LBound (op1,w)) <= the_result_sort_of (LBound (op2,w)) by A9, A12, Def7;
then the_result_sort_of (LBound (op1,w)) = the_result_sort_of (LBound (op2,w)) by A11, ORDERS_2:2;
hence LBound (op1,w) = LBound (op2,w) by A9, A13, Def3; ::_thesis: verum
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
consider op being Element of on such that
A2: w <= the_arity_of op by A1;
set Lo = LBound (op,w);
LBound (op,w) has_least_args_for op,w by A2, Def14;
then op ~= LBound (op,w) by Def9;
then A3: Name op = Name (LBound (op,w)) by Th31;
then A4: Name (LBound (op,w)) = on by Th33;
then reconsider Lo = LBound (op,w) as Element of on by Th33;
take Lo ; ::_thesis: for op being Element of on st w <= the_arity_of op holds
Lo = LBound (op,w)
let op1 be Element of on; ::_thesis: ( w <= the_arity_of op1 implies Lo = LBound (op1,w) )
assume A5: w <= the_arity_of op1 ; ::_thesis: Lo = LBound (op1,w)
Name op1 = on by Th33;
then op1 ~= op by A3, A4, Th31;
hence Lo = LBound (op1,w) by A2, A5, Th34; ::_thesis: verum
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
let op1, op2 be Element of on; ::_thesis: ( ( for op being Element of on st w <= the_arity_of op holds
op1 = LBound (op,w) ) & ( for op being Element of on st w <= the_arity_of op holds
op2 = LBound (op,w) ) implies op1 = op2 )
assume that
A6: for op3 being Element of on st w <= the_arity_of op3 holds
op1 = LBound (op3,w) and
A7: for op3 being Element of on st w <= the_arity_of op3 holds
op2 = LBound (op3,w) ; ::_thesis: op1 = op2
consider op being Element of on such that
A8: w <= the_arity_of op by A1;
op1 = LBound (op,w) by A8, A6;
hence op1 = op2 by A8, A7; ::_thesis: verum
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
let S be monotone regular OrderSortedSign; ::_thesis: 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
let o be OperSymbol of S; ::_thesis: for w1 being Element of the carrier of S * st w1 <= the_arity_of o holds
LBound (o,w1) <= o
let w1 be Element of the carrier of S * ; ::_thesis: ( w1 <= the_arity_of o implies LBound (o,w1) <= o )
assume A1: w1 <= the_arity_of o ; ::_thesis: LBound (o,w1) <= o
set lo = LBound (o,w1);
A2: LBound (o,w1) has_least_rank_for o,w1 by A1, Th14;
then LBound (o,w1) has_least_sort_for o,w1 by Def11;
then A3: the_result_sort_of (LBound (o,w1)) <= the_result_sort_of o by A1, Def10;
A4: LBound (o,w1) has_least_args_for o,w1 by A2, Def11;
then A5: o ~= LBound (o,w1) by Def9;
the_arity_of (LBound (o,w1)) <= the_arity_of o by A1, A4, Def9;
hence LBound (o,w1) <= o by A5, A3, Def20; ::_thesis: verum
end;