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