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