:: Free Order Sorted Universal Algebra :: by Josef Urban :: :: Received September 19, 2002 :: Copyright (c) 2002-2021 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies OSALG_1, MSUALG_2, OSALG_2, MSUALG_1, TARSKI, STRUCT_0, RELAT_1, SEQM_3, PBOOLE, MSUALG_3, REALSET1, ZFMISC_1, XBOOLE_0, CARD_3, MSAFREE, SUBSET_1, FINSEQ_1, MARGREL1, FUNCT_1, XXREAL_0, PARTFUN1, LANG1, TDGROUP, DTCONSTR, TREES_3, TREES_4, NAT_1, TREES_2, OSALG_4, CARD_5, NATTRA_1, CARD_LAR, QC_LANG1, EQREL_1, RELAT_2, MSUALG_4, COH_SP, MCART_1, UNIALG_2, MEMBER_1, FUNCT_7, OSAFREE; notations TARSKI, XBOOLE_0, ZFMISC_1, XTUPLE_0, SUBSET_1, ORDINAL1, RELAT_1, RELSET_1, FUNCT_1, MCART_1, PARTFUN1, FUNCT_2, FINSEQ_1, FINSEQ_2, PBOOLE, RELAT_2, TREES_2, CARD_3, EQREL_1, STRUCT_0, LANG1, TREES_3, TREES_4, DTCONSTR, ORDERS_2, ORDERS_3, MSUALG_1, MSUALG_2, MSUALG_3, MSUALG_4, OSALG_1, OSALG_2, OSALG_3, OSALG_4, MSAFREE, FUNCT_7; constructors NAT_1, FINSEQOP, FUNCT_7, MSUALG_3, MSAFREE, ORDERS_3, OSALG_2, OSALG_3, OSALG_4, RELSET_1, XTUPLE_0, NUMBERS; registrations XBOOLE_0, SUBSET_1, RELAT_1, ORDINAL1, PARTFUN1, FUNCOP_1, FUNCT_1, PBOOLE, TREES_2, TREES_3, STRUCT_0, DTCONSTR, MSUALG_1, MSUALG_3, MSAFREE, MSUALG_4, MSUALG_9, OSALG_1, OSALG_4, RELSET_1, FINSEQ_1, XTUPLE_0; requirements BOOLE, SUBSET; begin reserve S for OrderSortedSign; :: REVISE: should rather be attribute :: changing to MSSubset and its OSCl, to make free algebras easier :: no good way how to retypeOSCL into OSSubset now? definition let S be OrderSortedSign, U0 be OSAlgebra of S; mode OSGeneratorSet of U0 -> MSSubset of U0 means :: OSAFREE:def 1 for O being OSSubset of U0 st O = OSCl it holds the Sorts of GenOSAlg(O) = the Sorts of U0; end; theorem :: OSAFREE:1 for S be OrderSortedSign, U0 be strict non-empty OSAlgebra of S, A be MSSubset of U0 holds A is OSGeneratorSet of U0 iff for O being OSSubset of U0 st O = OSCl A holds GenOSAlg(O) = U0; :: renaming to osfree - if OSGeneratorSet and GeneratorSet become :: attributes, Mizar would be puzzled :: we do this for monotone osas only, though more general approach is possible definition let S; let U0 be monotone OSAlgebra of S; let IT be OSGeneratorSet of U0; attr IT is osfree means :: OSAFREE:def 2 for U1 be monotone non-empty OSAlgebra of S for f be ManySortedFunction of IT,the Sorts of U1 ex h be ManySortedFunction of U0,U1 st h is_homomorphism U0,U1 & h is order-sorted & h || IT = f; end; definition let S be OrderSortedSign; let IT be monotone OSAlgebra of S; attr IT is osfree means :: OSAFREE:def 3 ex G being OSGeneratorSet of IT st G is osfree; end; begin :: :: Construction of Free Order Sorted Algebras for Given Signature :: definition let S be OrderSortedSign, X be ManySortedSet of S; func OSREL(X) -> Relation of ([:the carrier' of S,{the carrier of S}:] \/ Union (coprod X)), (([:the carrier' of S,{the carrier of S}:] \/ Union (coprod X))*) means :: OSAFREE:def 4 for a be Element of [:the carrier' of S,{the carrier of S}:] \/ Union (coprod X), b be Element of ([:the carrier' of S,{the carrier of S}:] \/ Union (coprod X))* holds [a,b] in it iff a in [:the carrier' of S,{the carrier of S}:] & for o be OperSymbol of S st [o,the carrier of S] = a holds len b = len (the_arity_of o) & for x be set st x in dom b holds (b.x in [:the carrier' of S,{the carrier of S}:] implies for o1 be OperSymbol of S st [o1,the carrier of S] = b.x holds (the_result_sort_of o1) <= (the_arity_of o)/.x) & (b. x in Union (coprod X) implies ex i being Element of S st i <= (the_arity_of o) /.x & b.x in coprod(i,X)); end; reserve S for OrderSortedSign, X for ManySortedSet of S, o for OperSymbol of S , b for Element of ([:the carrier' of S,{the carrier of S}:] \/ Union (coprod X ))*; theorem :: OSAFREE:2 [[o,the carrier of S],b] in OSREL(X) iff len b = len ( the_arity_of o) & for x be set st x in dom b holds (b.x in [:the carrier' of S, {the carrier of S}:] implies for o1 be OperSymbol of S st [o1,the carrier of S] = b.x holds (the_result_sort_of o1) <= (the_arity_of o)/.x) & (b.x in Union ( coprod X) implies ex i being Element of S st i <= (the_arity_of o)/.x & b.x in coprod(i,X)); definition let S be OrderSortedSign, X be ManySortedSet of S; func DTConOSA(X) -> DTConstrStr equals :: OSAFREE:def 5 DTConstrStr (# [:the carrier' of S,{ the carrier of S}:] \/ Union (coprod X), OSREL(X) #); end; registration let S be OrderSortedSign, X be ManySortedSet of S; cluster DTConOSA(X) -> strict non empty; end; theorem :: OSAFREE:3 for S be OrderSortedSign, X be non-empty ManySortedSet of S holds NonTerminals(DTConOSA(X)) = [:the carrier' of S,{the carrier of S}:] & Terminals (DTConOSA(X)) = Union (coprod X); reserve x for set; registration let S be OrderSortedSign, X be non-empty ManySortedSet of S; cluster DTConOSA(X) -> with_terminals with_nonterminals with_useful_nonterminals; end; theorem :: OSAFREE:4 for S be OrderSortedSign, X be non-empty ManySortedSet of S, t be set holds t in Terminals DTConOSA(X) iff ex s be Element of S, x be set st x in X.s & t = [x,s]; :: have to rename definition let S be OrderSortedSign, X be non-empty ManySortedSet of S, o be OperSymbol of S; func OSSym(o,X) ->Symbol of DTConOSA(X) equals :: OSAFREE:def 6 [o,the carrier of S]; end; :: originally FreeSort, but it is not a good name in order-sorted context definition let S be OrderSortedSign, X be non-empty ManySortedSet of S, s be Element of S; func ParsedTerms(X,s) -> Subset of TS(DTConOSA(X)) equals :: OSAFREE:def 7 {a where a is Element of TS(DTConOSA(X)): (ex s1 being Element of S, x be object st s1 <= s & x in X.s1 & a = root-tree [x,s1]) or ex o be OperSymbol of S st [o,the carrier of S] = a.{} & the_result_sort_of o <= s}; end; registration let S be OrderSortedSign, X be non-empty ManySortedSet of S, s be Element of S; cluster ParsedTerms(X,s) -> non empty; end; definition let S be OrderSortedSign, X be non-empty ManySortedSet of S; func ParsedTerms(X) -> OrderSortedSet of S means :: OSAFREE:def 8 for s be Element of S holds it.s = ParsedTerms(X,s); end; registration let S be OrderSortedSign, X be non-empty ManySortedSet of S; cluster ParsedTerms(X) -> non-empty; end; theorem :: OSAFREE:5 for S be OrderSortedSign, X be non-empty ManySortedSet of S, o be OperSymbol of S, x be set st x in ((ParsedTerms X)# * (the Arity of S)).o holds x is FinSequence of TS(DTConOSA(X)); theorem :: OSAFREE:6 for S be OrderSortedSign, X be non-empty ManySortedSet of S, o be OperSymbol of S, p be FinSequence of TS(DTConOSA(X)) holds p in ((ParsedTerms X )# * (the Arity of S)).o iff dom p = dom (the_arity_of o) & for n be Nat st n in dom p holds p.n in ParsedTerms(X,(the_arity_of o)/.n); theorem :: OSAFREE:7 for S be OrderSortedSign, X be non-empty ManySortedSet of S, o be OperSymbol of S, p be FinSequence of TS(DTConOSA(X)) holds OSSym(o,X) ==> roots p iff p in ((ParsedTerms X)# * (the Arity of S)).o; theorem :: OSAFREE:8 for S be OrderSortedSign, X be non-empty ManySortedSet of S holds union rng (ParsedTerms X) = TS (DTConOSA(X)); definition let S be OrderSortedSign, X be non-empty ManySortedSet of S, o be OperSymbol of S; func PTDenOp(o,X) -> Function of ((ParsedTerms X)# * (the Arity of S)).o, (( ParsedTerms X) * (the ResultSort of S)).o means :: OSAFREE:def 9 for p be FinSequence of TS(DTConOSA(X)) st OSSym(o,X) ==> roots p holds it.p = (OSSym(o,X))-tree p; end; definition let S be OrderSortedSign, X be non-empty ManySortedSet of S; func PTOper(X) -> ManySortedFunction of (ParsedTerms X)# * (the Arity of S), (ParsedTerms X) * (the ResultSort of S) means :: OSAFREE:def 10 for o be OperSymbol of S holds it.o = PTDenOp(o,X); end; definition let S be OrderSortedSign, X be non-empty ManySortedSet of S; func ParsedTermsOSA(X) -> OSAlgebra of S equals :: OSAFREE:def 11 MSAlgebra (# ParsedTerms(X), PTOper(X) #); end; registration let S be OrderSortedSign, X be non-empty ManySortedSet of S; cluster ParsedTermsOSA(X) -> strict non-empty; end; definition let S be OrderSortedSign; let X be non-empty ManySortedSet of S; let o be OperSymbol of S; redefine func OSSym(o, X) -> NonTerminal of DTConOSA X; end; theorem :: OSAFREE:9 for S being OrderSortedSign, X being non-empty ManySortedSet of S , s being Element of S holds (the Sorts of ParsedTermsOSA(X)).s = {a where a is Element of TS(DTConOSA(X)): (ex s1 being Element of S, x be object st s1 <= s & x in X.s1 & a = root-tree [x,s1]) or ex o be OperSymbol of S st [o,the carrier of S] = a.{} & the_result_sort_of o <= s}; theorem :: OSAFREE:10 for S being OrderSortedSign, X being non-empty ManySortedSet of S, s,s1 being Element of S, x being set st x in X.s holds root-tree [x,s] is Element of TS DTConOSA(X) & ( for z being set holds [z,the carrier of S] <> ( root-tree [x,s]).{} ) & ( root-tree [x,s] in (the Sorts of ParsedTermsOSA(X)). s1 iff s <= s1 ); theorem :: OSAFREE:11 for S being OrderSortedSign, X being non-empty ManySortedSet of S, t being Element of TS (DTConOSA X), o being OperSymbol of S st t.{} = [o,the carrier of S] holds (ex p being SubtreeSeq of OSSym(o,X) st t = OSSym(o,X)-tree p & OSSym(o,X) ==> roots p & p in Args(o,ParsedTermsOSA(X)) & t = Den(o, ParsedTermsOSA(X)).p ) & ( for s2 being Element of S, x being set holds t <> root-tree [x,s2] ) & for s1 being Element of S holds t in (the Sorts of ParsedTermsOSA(X)).s1 iff the_result_sort_of o <= s1; theorem :: OSAFREE:12 for S being OrderSortedSign, X being non-empty ManySortedSet of S, nt being Symbol of DTConOSA(X), ts being FinSequence of TS(DTConOSA(X)) st nt ==> roots ts holds nt in NonTerminals DTConOSA(X) & nt-tree ts in TS DTConOSA(X) & ex o being OperSymbol of S st nt = [o,the carrier of S] & ts in Args(o,ParsedTermsOSA(X)) & nt-tree ts = Den(o,ParsedTermsOSA(X)).ts & for s1 being Element of S holds nt-tree ts in (the Sorts of ParsedTermsOSA(X)).s1 iff the_result_sort_of o <= s1; :: Element of Args is FinSequence (if clusters MSUALG_9) theorem :: OSAFREE:13 for S being OrderSortedSign, X being non-empty ManySortedSet of S, o be OperSymbol of S, x being FinSequence holds x in Args(o,ParsedTermsOSA(X )) iff x is FinSequence of TS(DTConOSA(X)) & OSSym(o,X) ==> roots x; :: this should be done more generally for leastsorted osas (and :: then remove the LeastSorts func), however, it is better here :: to have it defined for terms (and not Elements of osa) definition let S be OrderSortedSign, X be non-empty ManySortedSet of S, t be Element of TS DTConOSA(X); func LeastSort t -> SortSymbol of S means :: OSAFREE:def 12 t in (the Sorts of ParsedTermsOSA(X)).it & for s1 being Element of S st t in (the Sorts of ParsedTermsOSA(X)).s1 holds it <= s1; end; :: REVISE: the clusters needed to make the def from MSAFREE3 work :: are too demanding, make it more easily accessible (or include :: the clusters if it is too hard) definition let S be non empty non void ManySortedSign; let A be non-empty MSAlgebra over S; mode Element of A is Element of Union the Sorts of A; end; theorem :: OSAFREE:14 for S being OrderSortedSign, X being non-empty ManySortedSet of S, x being set holds x is Element of ParsedTermsOSA(X) iff x is Element of TS DTConOSA(X); theorem :: OSAFREE:15 for S being OrderSortedSign, X being non-empty ManySortedSet of S, s be Element of S, x being set st x in (the Sorts of ParsedTermsOSA(X)).s holds x is Element of TS DTConOSA(X); theorem :: OSAFREE:16 for S being OrderSortedSign, X being non-empty ManySortedSet of S, s being Element of S, x being set st x in X.s for t being Element of TS DTConOSA( X) st t = root-tree [x,s] holds LeastSort t = s; theorem :: OSAFREE:17 for S being OrderSortedSign, X being non-empty ManySortedSet of S, o be OperSymbol of S, x being Element of Args(o,ParsedTermsOSA(X)) holds for t being Element of TS DTConOSA(X) st t = Den(o,ParsedTermsOSA(X)).x holds LeastSort t = the_result_sort_of o; :: WHY is this necessary??? bug? registration let S be OrderSortedSign, X be non-empty ManySortedSet of S; let o2 be OperSymbol of S; cluster Args(o2,ParsedTermsOSA(X)) -> non empty; end; :: REVISE: was probably needed for casting, but try if :: LeastSort * x does the work and if so, remove this definition let S be locally_directed OrderSortedSign, X be non-empty ManySortedSet of S , x be FinSequence of TS DTConOSA(X); func LeastSorts x -> Element of (the carrier of S)* means :: OSAFREE:def 13 dom it = dom x & for y being Nat st y in dom x holds ex t being Element of TS DTConOSA(X ) st t = x.y & it.y = LeastSort t; end; :: all these should be generalized to any leastsorted osa theorem :: OSAFREE:18 for S be locally_directed OrderSortedSign, X be non-empty ManySortedSet of S, o be OperSymbol of S, x be FinSequence of TS DTConOSA(X) holds LeastSorts x <= the_arity_of o iff x in Args(o,ParsedTermsOSA(X)); registration cluster locally_directed regular for monotone OrderSortedSign; end; :: just casting funcs necessary for the usage of schemes definition let S be locally_directed regular monotone OrderSortedSign, X be non-empty ManySortedSet of S, o be OperSymbol of S, x be FinSequence of TS DTConOSA(X); assume OSSym(LBound(o,LeastSorts x),X) ==> roots x; func pi(o,x) -> Element of TS DTConOSA(X) equals :: OSAFREE:def 14 OSSym(LBound(o, LeastSorts x),X)-tree x; end; definition let S be locally_directed OrderSortedSign, X be non-empty ManySortedSet of S , t be Symbol of DTConOSA(X); assume ex p be FinSequence st t ==> p; func @(X,t) -> OperSymbol of S means :: OSAFREE:def 15 [it,the carrier of S] = t; end; definition let S be OrderSortedSign, X be non-empty ManySortedSet of S; let t be Symbol of DTConOSA(X); assume t in Terminals DTConOSA(X); func pi t -> Element of TS(DTConOSA(X)) equals :: OSAFREE:def 16 root-tree t; end; :: the least monotone OSCongruence definition let S be locally_directed OrderSortedSign, X be non-empty ManySortedSet of S; func LCongruence X -> monotone OSCongruence of ParsedTermsOSA(X) means :: OSAFREE:def 17 for R be monotone OSCongruence of ParsedTermsOSA(X) holds it c= R; end; definition let S be locally_directed OrderSortedSign, X be non-empty ManySortedSet of S; func FreeOSA(X) -> strict non-empty monotone OSAlgebra of S equals :: OSAFREE:def 18 QuotOSAlg (ParsedTermsOSA(X),LCongruence(X)); end; :: now we need an explicit description of a sufficiently small :: monotone OSCongruence on PTA; the PTCongruence turns out to :: be LCongruence on regular signatures, and is also used to describe :: minimal terms there :: just casting funcs necessary for the usage of schemes, :: remove when Frankel behaves better definition let S be OrderSortedSign, X be non-empty ManySortedSet of S; let t be Symbol of DTConOSA(X); func @ t -> Subset of [:TS(DTConOSA(X)), the carrier of S:] equals :: OSAFREE:def 19 {[ root-tree t,s1] where s1 is Element of S: ex s be Element of S, x be set st x in X.s & t = [x,s] & s <= s1}; end; definition let S be OrderSortedSign, X be non-empty ManySortedSet of S; let nt be Symbol of DTConOSA(X), x be FinSequence of bool [:TS(DTConOSA(X)), the carrier of S:]; func @ (nt,x) -> Subset of [:TS(DTConOSA(X)), the carrier of S:] equals :: OSAFREE:def 20 {[ Den(o2,ParsedTermsOSA(X)).x2,s3] where o2 is OperSymbol of S, x2 is Element of Args(o2,ParsedTermsOSA(X)), s3 is Element of S : ( ex o1 being OperSymbol of S st nt = [o1,the carrier of S] & o1 ~= o2 & len the_arity_of o1 = len the_arity_of o2 & the_result_sort_of o1 <= s3 & the_result_sort_of o2 <= s3) & ex w3 being Element of (the carrier of S)* st dom w3 = dom x & for y being Nat st y in dom x holds [x2.y,w3/.y] in x.y }; end; :: a bit technical, to create the PTCongruence definition let S be locally_directed OrderSortedSign, X be non-empty ManySortedSet of S; func PTClasses X -> Function of TS(DTConOSA(X)), bool [:TS(DTConOSA(X)), the carrier of S:] means :: OSAFREE:def 21 (for t being Symbol of DTConOSA(X) st t in Terminals DTConOSA(X) holds it.(root-tree t) = @(t) ) & for nt being Symbol of DTConOSA(X), ts being FinSequence of TS(DTConOSA(X)) st nt ==> roots ts holds it.(nt-tree ts) = @(nt,it * ts); end; theorem :: OSAFREE:19 for S be locally_directed OrderSortedSign, X be non-empty ManySortedSet of S, t being Element of TS DTConOSA(X) holds ( for s being Element of S holds t in (the Sorts of ParsedTermsOSA(X)).s iff [t,s] in ( PTClasses X).t ) & for s being Element of S, y being Element of TS(DTConOSA X) holds [y,s] in (PTClasses X).t implies [t,s] in (PTClasses X).y; :: switched to have easier prooving theorem :: OSAFREE:20 for S be locally_directed OrderSortedSign, X be non-empty ManySortedSet of S, t being Element of TS DTConOSA(X), s being Element of S holds ( ex y being Element of TS(DTConOSA X) st [y,s] in (PTClasses X).t ) implies [t,s] in (PTClasses X).t; theorem :: OSAFREE:21 for S be locally_directed OrderSortedSign, X be non-empty ManySortedSet of S, x,y being Element of TS DTConOSA(X), s1,s2 being Element of S st s1 <= s2 & x in (the Sorts of ParsedTermsOSA(X)).s1 & y in (the Sorts of ParsedTermsOSA(X)).s1 holds [y,s1] in (PTClasses X).x iff [y,s2] in (PTClasses X).x; theorem :: OSAFREE:22 for S be locally_directed OrderSortedSign, X be non-empty ManySortedSet of S, x,y,z being Element of TS DTConOSA(X), s being Element of S holds [y,s] in (PTClasses X).x & [z,s] in (PTClasses X).y implies [x,s] in ( PTClasses X).z; definition let S be locally_directed OrderSortedSign, X be non-empty ManySortedSet of S; func PTCongruence(X) -> MSEquivalence-like OrderSortedRelation of ParsedTermsOSA(X) means :: OSAFREE:def 22 for i being set st i in the carrier of S holds it.i = {[x,y] where x,y is Element of TS(DTConOSA(X)): [x,i] in (PTClasses X).y }; end; theorem :: OSAFREE:23 for S be locally_directed OrderSortedSign, X be non-empty ManySortedSet of S, x,y,s being object st [x,s] in (PTClasses X).y holds x in TS DTConOSA(X) & y in TS DTConOSA(X) & s in the carrier of S; theorem :: OSAFREE:24 for S be locally_directed OrderSortedSign, X be non-empty ManySortedSet of S, C be Component of S, x,y being object holds [x,y] in CompClass (PTCongruence X,C) iff ex s1 being Element of S st s1 in C & [x,s1] in ( PTClasses X).y; theorem :: OSAFREE:25 for S be locally_directed OrderSortedSign, X be non-empty ManySortedSet of S, s be Element of S, x be Element of (the Sorts of ParsedTermsOSA(X)).s holds OSClass(PTCongruence X,x) = proj1((PTClasses X).x) ; :: more explicit description of PTCongruence theorem :: OSAFREE:26 for S being locally_directed OrderSortedSign, X being non-empty ManySortedSet of S, R being ManySortedRelation of ParsedTermsOSA(X) holds R = PTCongruence(X) iff ( for s1,s2 being Element of S, x being object st x in X.s1 holds ( s1 <= s2 implies [root-tree [x,s1],root-tree[x,s1]] in R.s2 ) & for y being object holds ( [root-tree [x,s1],y] in R.s2 or [y,root-tree [x,s1]] in R.s2) implies s1 <= s2 & y = root-tree [x,s1] ) & for o1,o2 being OperSymbol of S, x1 being Element of Args(o1,ParsedTermsOSA(X)), x2 being Element of Args(o2, ParsedTermsOSA(X)), s3 being Element of S holds [Den(o1,ParsedTermsOSA(X)).x1, Den(o2,ParsedTermsOSA(X)).x2] in R.s3 iff o1 ~= o2 & len the_arity_of o1 = len the_arity_of o2 & the_result_sort_of o1 <= s3 & the_result_sort_of o2 <= s3 & ex w3 being Element of (the carrier of S)* st dom w3 = dom x1 & for y being Nat st y in dom w3 holds [x1.y,x2.y] in R.(w3/.y); :: the minimality for regular oss is done later theorem :: OSAFREE:27 for S be locally_directed OrderSortedSign, X be non-empty ManySortedSet of S holds PTCongruence(X) is monotone; :: MSCongruence-like is ensured by the OSALG_4 cluster registration let S be locally_directed OrderSortedSign, X be non-empty ManySortedSet of S; cluster PTCongruence(X) -> monotone; end; definition let S be locally_directed OrderSortedSign, X be non-empty ManySortedSet of S , s be Element of S; func PTVars(s,X) -> Subset of (the Sorts of ParsedTermsOSA(X)).s means :: OSAFREE:def 23 for x be object holds x in it iff ex a be object st a in X.s & x = root-tree [a,s]; end; registration let S be locally_directed OrderSortedSign, X be non-empty ManySortedSet of S , s be Element of S; cluster PTVars(s,X) -> non empty; end; theorem :: OSAFREE:28 for S be locally_directed OrderSortedSign, X be non-empty ManySortedSet of S, s be Element of S holds PTVars(s,X) = { root-tree t where t is Symbol of DTConOSA(X): t in Terminals DTConOSA(X) & t`2 = s}; definition let S be locally_directed OrderSortedSign, X be non-empty ManySortedSet of S; func PTVars(X) -> MSSubset of ParsedTermsOSA(X) means :: OSAFREE:def 24 for s be Element of S holds it.s = PTVars(s,X); end; theorem :: OSAFREE:29 for S be locally_directed OrderSortedSign, X be non-empty ManySortedSet of S holds PTVars(X) is non-empty; definition let S be locally_directed OrderSortedSign, X be non-empty ManySortedSet of S , s be Element of S; func OSFreeGen(s,X) -> Subset of (the Sorts of FreeOSA(X)).s means :: OSAFREE:def 25 for x be object holds x in it iff ex a be object st a in X.s & x = (OSNat_Hom( ParsedTermsOSA(X),LCongruence(X)).s).(root-tree [a,s]); end; registration let S be locally_directed OrderSortedSign, X be non-empty ManySortedSet of S , s be Element of S; cluster OSFreeGen(s,X) -> non empty; end; theorem :: OSAFREE:30 for S be locally_directed OrderSortedSign, X be non-empty ManySortedSet of S, s be Element of S holds OSFreeGen(s,X) = { (OSNat_Hom( ParsedTermsOSA(X),LCongruence(X)).s).root-tree t where t is Symbol of DTConOSA( X): t in Terminals DTConOSA(X) & t`2 = s}; definition let S be locally_directed OrderSortedSign, X be non-empty ManySortedSet of S; func OSFreeGen(X) -> OSGeneratorSet of FreeOSA(X) means :: OSAFREE:def 26 for s be Element of S holds it.s = OSFreeGen(s,X); end; theorem :: OSAFREE:31 for S be locally_directed OrderSortedSign, X be non-empty ManySortedSet of S holds OSFreeGen(X) is non-empty; registration let S be locally_directed OrderSortedSign, X be non-empty ManySortedSet of S; cluster OSFreeGen(X) -> non-empty; end; definition let S be locally_directed OrderSortedSign, X be non-empty ManySortedSet of S , R be OSCongruence of ParsedTermsOSA(X), t be Element of TS DTConOSA(X); func OSClass(R,t) -> Element of OSClass(R,LeastSort t) means :: OSAFREE:def 27 for s being Element of S, x being Element of (the Sorts of ParsedTermsOSA(X)).s st t = x holds it = OSClass(R,x); end; theorem :: OSAFREE:32 for S be locally_directed OrderSortedSign, X be non-empty ManySortedSet of S, R be OSCongruence of ParsedTermsOSA(X), t be Element of TS DTConOSA(X) holds t in OSClass(R,t); theorem :: OSAFREE:33 for S be locally_directed OrderSortedSign, X be non-empty ManySortedSet of S, s be Element of S, t being Element of TS DTConOSA(X), x,x1 being set st x in X.s & t = root-tree [x,s] holds x1 in OSClass(PTCongruence(X) ,t) iff x1 = t; theorem :: OSAFREE:34 for S be locally_directed OrderSortedSign, X be non-empty ManySortedSet of S, R be OSCongruence of ParsedTermsOSA(X), t1,t2 be Element of TS DTConOSA(X) holds t2 in OSClass(R,t1) iff OSClass(R,t1) = OSClass(R,t2); theorem :: OSAFREE:35 for S be locally_directed OrderSortedSign, X be non-empty ManySortedSet of S, R1,R2 be OSCongruence of ParsedTermsOSA(X), t be Element of TS DTConOSA(X) holds R1 c= R2 implies OSClass(R1,t) c= OSClass(R2,t); theorem :: OSAFREE:36 for S be locally_directed OrderSortedSign, X be non-empty ManySortedSet of S, s be Element of S, t being Element of TS DTConOSA(X), x,x1 being set st x in X.s & t = root-tree [x,s] holds x1 in OSClass(LCongruence(X), t) iff x1 = t; definition let S be locally_directed OrderSortedSign, X be non-empty ManySortedSet of S , A be non-empty ManySortedSet of the carrier of S, F be ManySortedFunction of PTVars(X), A, t be Symbol of DTConOSA(X); assume t in Terminals (DTConOSA(X)); func pi(F,A,t) -> Element of Union A means :: OSAFREE:def 28 for f be Function st f = F.(t`2) holds it = f.(root-tree t); end; theorem :: OSAFREE:37 for S be locally_directed OrderSortedSign, X be non-empty ManySortedSet of S, U1 be monotone non-empty OSAlgebra of S, f be ManySortedFunction of PTVars(X),the Sorts of U1 ex h be ManySortedFunction of ParsedTermsOSA(X),U1 st h is_homomorphism ParsedTermsOSA(X),U1 & h is order-sorted & h || PTVars(X) = f; :: NH stanbds for NatHom definition let S be locally_directed OrderSortedSign, X be non-empty ManySortedSet of S , s be Element of S; func NHReverse(s,X) -> Function of OSFreeGen(s,X),PTVars(s,X) means :: OSAFREE:def 29 for t be Symbol of DTConOSA(X) st (OSNat_Hom(ParsedTermsOSA(X),LCongruence(X)).s).( root-tree t) in OSFreeGen(s,X) holds it.((OSNat_Hom(ParsedTermsOSA(X), LCongruence(X)).s).(root-tree t)) = root-tree t; end; definition let S be locally_directed OrderSortedSign, X be non-empty ManySortedSet of S; func NHReverse(X) -> ManySortedFunction of OSFreeGen(X),PTVars(X) means :: OSAFREE:def 30 for s be Element of S holds it.s = NHReverse(s,X); end; theorem :: OSAFREE:38 for S be locally_directed OrderSortedSign, X be non-empty ManySortedSet of S holds OSFreeGen(X) is osfree; theorem :: OSAFREE:39 for S be locally_directed OrderSortedSign, X be non-empty ManySortedSet of S holds FreeOSA(X) is osfree; registration let S be locally_directed OrderSortedSign; cluster osfree strict for non-empty monotone OSAlgebra of S; end; begin :: PTMin ... minimality of PTCongruence on regular signatures :: minimal terms definition let S be locally_directed regular monotone OrderSortedSign, X be non-empty ManySortedSet of S; func PTMin X -> Function of TS(DTConOSA(X)), TS(DTConOSA(X)) means :: OSAFREE:def 31 ( for t being Symbol of DTConOSA(X) st t in Terminals DTConOSA(X) holds it.( root-tree t) = pi t ) & for nt being Symbol of DTConOSA(X), ts being FinSequence of TS(DTConOSA(X)) st nt ==> roots ts holds it.(nt-tree ts) = pi(@( X,nt),it * ts); end; theorem :: OSAFREE:40 for S be locally_directed regular monotone OrderSortedSign, X be non-empty ManySortedSet of S, t being Element of TS DTConOSA(X) holds (PTMin X).t in OSClass(PTCongruence(X),t) & LeastSort ((PTMin X).t) <= LeastSort t & ( for s being Element of S, x being set st x in X.s & t = root-tree [x,s] holds ( PTMin X).t = t ) & (for o being OperSymbol of S, ts being FinSequence of TS( DTConOSA(X)) st OSSym(o,X) ==> roots ts & t = OSSym(o,X)-tree ts holds LeastSorts ((PTMin X)*ts) <= the_arity_of o & OSSym(o,X) ==> roots ((PTMin X)* ts) & OSSym(LBound(o,LeastSorts ((PTMin X)*ts)),X) ==> roots ((PTMin X)*ts) & ( PTMin X).t = OSSym(LBound(o,LeastSorts ((PTMin X)*ts)),X)-tree ((PTMin X)*ts)); theorem :: OSAFREE:41 for S be locally_directed regular monotone OrderSortedSign, X be non-empty ManySortedSet of S, t,t1 being Element of TS DTConOSA(X) st t1 in OSClass(PTCongruence(X),t) holds (PTMin X).t1 = (PTMin X).t; theorem :: OSAFREE:42 for S be locally_directed regular monotone OrderSortedSign, X be non-empty ManySortedSet of S, t1,t2 be Element of TS DTConOSA(X) holds t2 in OSClass(PTCongruence(X),t1) iff (PTMin X).t2 = (PTMin X).t1; theorem :: OSAFREE:43 for S be locally_directed regular monotone OrderSortedSign, X be non-empty ManySortedSet of S, t1 be Element of TS DTConOSA(X) holds (PTMin X ).((PTMin X).t1) = (PTMin X).t1; theorem :: OSAFREE:44 for S be locally_directed regular monotone OrderSortedSign, X be non-empty ManySortedSet of S, R be monotone MSEquivalence-like (OrderSortedRelation of ParsedTermsOSA(X)), t be Element of TS DTConOSA(X) holds [t,(PTMin X).t] in R.(LeastSort t); theorem :: OSAFREE:45 for S be locally_directed regular monotone OrderSortedSign, X be non-empty ManySortedSet of S, R be monotone MSEquivalence-like OrderSortedRelation of ParsedTermsOSA(X) holds PTCongruence(X) c= R; :: minimality of PTCongruence theorem :: OSAFREE:46 for S be locally_directed regular monotone OrderSortedSign, X be non-empty ManySortedSet of S holds LCongruence(X) = PTCongruence(X); :: I would prefer attribute "minimal", but non-clusterable definition let S be locally_directed regular monotone OrderSortedSign, X be non-empty ManySortedSet of S; mode MinTerm of S,X -> Element of TS DTConOSA(X) means :: OSAFREE:def 32 (PTMin X).it = it; end; definition let S be locally_directed regular monotone OrderSortedSign, X be non-empty ManySortedSet of S; func MinTerms X -> Subset of TS DTConOSA(X) equals :: OSAFREE:def 33 rng (PTMin X); end; theorem :: OSAFREE:47 for S be locally_directed regular monotone OrderSortedSign, X be non-empty ManySortedSet of S, x being set holds x is MinTerm of S,X iff x in MinTerms X;