begin
:: deftheorem Def1 defines OSGeneratorSet OSAFREE:def 1 :
for S being OrderSortedSign
for U0 being OSAlgebra of S
for b3 being MSSubset of U0 holds
( b3 is OSGeneratorSet of U0 iff for O being OSSubset of U0 st O = OSCl b3 holds
the Sorts of (GenOSAlg O) = the Sorts of U0 );
theorem
:: deftheorem defines osfree OSAFREE:def 2 :
for S being OrderSortedSign
for U0 being monotone OSAlgebra of S
for IT being OSGeneratorSet of U0 holds
( IT is osfree iff for U1 being non-empty monotone OSAlgebra of S
for f being ManySortedFunction of IT, the Sorts of U1 ex h being ManySortedFunction of U0,U1 st
( h is_homomorphism U0,U1 & h is order-sorted & h || IT = f ) );
:: deftheorem defines osfree OSAFREE:def 3 :
for S being OrderSortedSign
for IT being monotone OSAlgebra of S holds
( IT is osfree iff ex G being OSGeneratorSet of IT st G is osfree );
begin
definition
let S be
OrderSortedSign;
let 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 :
Def4:
for
a being
Element of
[: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X)) for
b being
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 being
OperSymbol of
S st
[o, the carrier of S] = a holds
(
len b = len (the_arity_of o) & ( for
x being
set st
x in dom b holds
( (
b . x in [: the carrier' of S,{ the carrier of S}:] implies for
o1 being
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) ) ) ) ) ) ) ) );
existence
ex b1 being Relation of ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))),(([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) *) st
for a being Element of [: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))
for b being Element of ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) * holds
( [a,b] in b1 iff ( a in [: the carrier' of S,{ the carrier of S}:] & ( for o being OperSymbol of S st [o, the carrier of S] = a holds
( len b = len (the_arity_of o) & ( for x being set st x in dom b holds
( ( b . x in [: the carrier' of S,{ the carrier of S}:] implies for o1 being 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) ) ) ) ) ) ) ) )
uniqueness
for b1, b2 being Relation of ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))),(([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) *) st ( for a being Element of [: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))
for b being Element of ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) * holds
( [a,b] in b1 iff ( a in [: the carrier' of S,{ the carrier of S}:] & ( for o being OperSymbol of S st [o, the carrier of S] = a holds
( len b = len (the_arity_of o) & ( for x being set st x in dom b holds
( ( b . x in [: the carrier' of S,{ the carrier of S}:] implies for o1 being 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) ) ) ) ) ) ) ) ) ) & ( for a being Element of [: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))
for b being Element of ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) * holds
( [a,b] in b2 iff ( a in [: the carrier' of S,{ the carrier of S}:] & ( for o being OperSymbol of S st [o, the carrier of S] = a holds
( len b = len (the_arity_of o) & ( for x being set st x in dom b holds
( ( b . x in [: the carrier' of S,{ the carrier of S}:] implies for o1 being 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) ) ) ) ) ) ) ) ) ) holds
b1 = b2
end;
:: deftheorem Def4 defines OSREL OSAFREE:def 4 :
for S being OrderSortedSign
for X being ManySortedSet of S
for b3 being Relation of ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))),(([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) *) holds
( b3 = OSREL X iff for a being Element of [: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))
for b being Element of ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) * holds
( [a,b] in b3 iff ( a in [: the carrier' of S,{ the carrier of S}:] & ( for o being OperSymbol of S st [o, the carrier of S] = a holds
( len b = len (the_arity_of o) & ( for x being set st x in dom b holds
( ( b . x in [: the carrier' of S,{ the carrier of S}:] implies for o1 being 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) ) ) ) ) ) ) ) ) );
theorem Th2:
:: deftheorem defines DTConOSA OSAFREE:def 5 :
for S being OrderSortedSign
for X being ManySortedSet of S holds DTConOSA X = DTConstrStr(# ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))),(OSREL X) #);
theorem Th3:
theorem Th4:
:: deftheorem defines OSSym OSAFREE:def 6 :
for S being OrderSortedSign
for X being V16() ManySortedSet of S
for o being OperSymbol of S holds OSSym (o,X) = [o, the carrier of S];
:: deftheorem defines ParsedTerms OSAFREE:def 7 :
for S being OrderSortedSign
for X being V16() ManySortedSet of S
for s being Element of S holds ParsedTerms (X,s) = { a where a is Element of TS (DTConOSA X) : ( ex s1 being Element of S ex x being set st
( s1 <= s & x in X . s1 & a = root-tree [x,s1] ) or ex o being OperSymbol of S st
( [o, the carrier of S] = a . {} & the_result_sort_of o <= s ) ) } ;
:: deftheorem Def8 defines ParsedTerms OSAFREE:def 8 :
for S being OrderSortedSign
for X being V16() ManySortedSet of S
for b3 being OrderSortedSet of S holds
( b3 = ParsedTerms X iff for s being Element of S holds b3 . s = ParsedTerms (X,s) );
theorem Th5:
theorem Th6:
theorem Th7:
theorem Th8:
definition
let S be
OrderSortedSign;
let X be
V16()
ManySortedSet of
S;
let 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 :
Def9:
for
p being
FinSequence of
TS (DTConOSA X) st
OSSym (
o,
X)
==> roots p holds
it . p = (OSSym (o,X)) -tree p;
existence
ex b1 being Function of ((((ParsedTerms X) #) * the Arity of S) . o),(((ParsedTerms X) * the ResultSort of S) . o) st
for p being FinSequence of TS (DTConOSA X) st OSSym (o,X) ==> roots p holds
b1 . p = (OSSym (o,X)) -tree p
uniqueness
for b1, b2 being Function of ((((ParsedTerms X) #) * the Arity of S) . o),(((ParsedTerms X) * the ResultSort of S) . o) st ( for p being FinSequence of TS (DTConOSA X) st OSSym (o,X) ==> roots p holds
b1 . p = (OSSym (o,X)) -tree p ) & ( for p being FinSequence of TS (DTConOSA X) st OSSym (o,X) ==> roots p holds
b2 . p = (OSSym (o,X)) -tree p ) holds
b1 = b2
end;
:: deftheorem Def9 defines PTDenOp OSAFREE:def 9 :
for S being OrderSortedSign
for X being V16() ManySortedSet of S
for o being OperSymbol of S
for b4 being Function of ((((ParsedTerms X) #) * the Arity of S) . o),(((ParsedTerms X) * the ResultSort of S) . o) holds
( b4 = PTDenOp (o,X) iff for p being FinSequence of TS (DTConOSA X) st OSSym (o,X) ==> roots p holds
b4 . p = (OSSym (o,X)) -tree p );
:: deftheorem Def10 defines PTOper OSAFREE:def 10 :
for S being OrderSortedSign
for X being V16() ManySortedSet of S
for b3 being ManySortedFunction of ((ParsedTerms X) #) * the Arity of S,(ParsedTerms X) * the ResultSort of S holds
( b3 = PTOper X iff for o being OperSymbol of S holds b3 . o = PTDenOp (o,X) );
:: deftheorem defines ParsedTermsOSA OSAFREE:def 11 :
for S being OrderSortedSign
for X being V16() ManySortedSet of S holds ParsedTermsOSA X = MSAlgebra(# (ParsedTerms X),(PTOper X) #);
theorem Th9:
theorem Th10:
theorem Th11:
theorem Th12:
theorem Th13:
theorem Th14:
:: deftheorem Def12 defines LeastSort OSAFREE:def 12 :
for S being OrderSortedSign
for X being V16() ManySortedSet of S
for t being Element of TS (DTConOSA X)
for b4 being SortSymbol of S holds
( b4 = LeastSort t iff ( t in the Sorts of (ParsedTermsOSA X) . b4 & ( for s1 being Element of S st t in the Sorts of (ParsedTermsOSA X) . s1 holds
b4 <= s1 ) ) );
theorem Th15:
theorem Th16:
theorem
theorem Th18:
:: deftheorem OSAFREE:def 13 :
canceled;
:: deftheorem Def14 defines LeastSorts OSAFREE:def 14 :
for S being locally_directed OrderSortedSign
for X being V16() ManySortedSet of S
for x being FinSequence of TS (DTConOSA X)
for b4 being Element of the carrier of S * holds
( b4 = LeastSorts x iff ( dom b4 = dom x & ( for y being Nat st y in dom x holds
ex t being Element of TS (DTConOSA X) st
( t = x . y & b4 . y = LeastSort t ) ) ) );
theorem Th19:
:: deftheorem Def15 defines pi OSAFREE:def 15 :
for S being monotone regular locally_directed OrderSortedSign
for X being V16() ManySortedSet of S
for o being OperSymbol of S
for x being FinSequence of TS (DTConOSA X) st OSSym ((LBound (o,(LeastSorts x))),X) ==> roots x holds
pi (o,x) = (OSSym ((LBound (o,(LeastSorts x))),X)) -tree x;
:: deftheorem Def16 defines @ OSAFREE:def 16 :
for S being locally_directed OrderSortedSign
for X being V16() ManySortedSet of S
for t being Symbol of (DTConOSA X) st ex p being FinSequence st t ==> p holds
for b4 being OperSymbol of S holds
( b4 = @ (X,t) iff [b4, the carrier of S] = t );
:: deftheorem Def17 defines pi OSAFREE:def 17 :
for S being OrderSortedSign
for X being V16() ManySortedSet of S
for t being Symbol of (DTConOSA X) st t in Terminals (DTConOSA X) holds
pi t = root-tree t;
:: deftheorem Def18 defines LCongruence OSAFREE:def 18 :
for S being locally_directed OrderSortedSign
for X being V16() ManySortedSet of S
for b3 being monotone OSCongruence of ParsedTermsOSA X holds
( b3 = LCongruence X iff for R being monotone OSCongruence of ParsedTermsOSA X holds b3 c= R );
:: deftheorem defines FreeOSA OSAFREE:def 19 :
for S being locally_directed OrderSortedSign
for X being V16() ManySortedSet of S holds FreeOSA X = QuotOSAlg ((ParsedTermsOSA X),(LCongruence X));
:: deftheorem defines @ OSAFREE:def 20 :
for S being OrderSortedSign
for X being V16() ManySortedSet of S
for t being Symbol of (DTConOSA X) holds @ t = { [(root-tree t),s1] where s1 is Element of S : ex s being Element of S ex x being set st
( x in X . s & t = [x,s] & s <= s1 ) } ;
definition
let S be
OrderSortedSign;
let X be
V16()
ManySortedSet of
S;
let nt be
Symbol of
(DTConOSA X);
let 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
{ [((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 ) ) ) } ;
correctness
coherence
{ [((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 ) ) ) } is Subset of [:(TS (DTConOSA X)), the carrier of S:];
end;
:: deftheorem defines @ OSAFREE:def 21 :
for S being OrderSortedSign
for X being V16() ManySortedSet of S
for nt being Symbol of (DTConOSA X)
for x being FinSequence of bool [:(TS (DTConOSA X)), the carrier of S:] holds @ (nt,x) = { [((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 ) ) ) } ;
definition
let S be
locally_directed OrderSortedSign;
let X be
V16()
ManySortedSet of
S;
func PTClasses X -> Function of
(TS (DTConOSA X)),
(bool [:(TS (DTConOSA X)), the carrier of S:]) means :
Def22:
( ( 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) for
ts being
FinSequence of
TS (DTConOSA X) st
nt ==> roots ts holds
it . (nt -tree ts) = @ (
nt,
(it * ts)) ) );
existence
ex b1 being Function of (TS (DTConOSA X)),(bool [:(TS (DTConOSA X)), the carrier of S:]) st
( ( for t being Symbol of (DTConOSA X) st t in Terminals (DTConOSA X) holds
b1 . (root-tree t) = @ t ) & ( for nt being Symbol of (DTConOSA X)
for ts being FinSequence of TS (DTConOSA X) st nt ==> roots ts holds
b1 . (nt -tree ts) = @ (nt,(b1 * ts)) ) )
uniqueness
for b1, b2 being Function of (TS (DTConOSA X)),(bool [:(TS (DTConOSA X)), the carrier of S:]) st ( for t being Symbol of (DTConOSA X) st t in Terminals (DTConOSA X) holds
b1 . (root-tree t) = @ t ) & ( for nt being Symbol of (DTConOSA X)
for ts being FinSequence of TS (DTConOSA X) st nt ==> roots ts holds
b1 . (nt -tree ts) = @ (nt,(b1 * ts)) ) & ( for t being Symbol of (DTConOSA X) st t in Terminals (DTConOSA X) holds
b2 . (root-tree t) = @ t ) & ( for nt being Symbol of (DTConOSA X)
for ts being FinSequence of TS (DTConOSA X) st nt ==> roots ts holds
b2 . (nt -tree ts) = @ (nt,(b2 * ts)) ) holds
b1 = b2
end;
:: deftheorem Def22 defines PTClasses OSAFREE:def 22 :
for S being locally_directed OrderSortedSign
for X being V16() ManySortedSet of S
for b3 being Function of (TS (DTConOSA X)),(bool [:(TS (DTConOSA X)), the carrier of S:]) holds
( b3 = PTClasses X iff ( ( for t being Symbol of (DTConOSA X) st t in Terminals (DTConOSA X) holds
b3 . (root-tree t) = @ t ) & ( for nt being Symbol of (DTConOSA X)
for ts being FinSequence of TS (DTConOSA X) st nt ==> roots ts holds
b3 . (nt -tree ts) = @ (nt,(b3 * ts)) ) ) );
theorem Th20:
theorem Th21:
theorem Th22:
theorem Th23:
definition
let S be
locally_directed OrderSortedSign;
let X be
V16()
ManySortedSet of
S;
func PTCongruence X -> MSEquivalence-like OrderSortedRelation of
ParsedTermsOSA X means :
Def23:
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 } ;
existence
ex b1 being MSEquivalence-like OrderSortedRelation of ParsedTermsOSA X st
for i being set st i in the carrier of S holds
b1 . i = { [x,y] where x, y is Element of TS (DTConOSA X) : [x,i] in (PTClasses X) . y }
uniqueness
for b1, b2 being MSEquivalence-like OrderSortedRelation of ParsedTermsOSA X st ( for i being set st i in the carrier of S holds
b1 . i = { [x,y] where x, y is Element of TS (DTConOSA X) : [x,i] in (PTClasses X) . y } ) & ( for i being set st i in the carrier of S holds
b2 . i = { [x,y] where x, y is Element of TS (DTConOSA X) : [x,i] in (PTClasses X) . y } ) holds
b1 = b2
end;
:: deftheorem Def23 defines PTCongruence OSAFREE:def 23 :
for S being locally_directed OrderSortedSign
for X being V16() ManySortedSet of S
for b3 being MSEquivalence-like OrderSortedRelation of ParsedTermsOSA X holds
( b3 = PTCongruence X iff for i being set st i in the carrier of S holds
b3 . i = { [x,y] where x, y is Element of TS (DTConOSA X) : [x,i] in (PTClasses X) . y } );
theorem Th24:
theorem Th25:
theorem Th26:
theorem Th27:
for
S being
locally_directed OrderSortedSign for
X being
V16()
ManySortedSet of
S for
R being
ManySortedRelation of
(ParsedTermsOSA X) holds
(
R = PTCongruence X iff ( ( for
s1,
s2 being
Element of
S for
x being
set st
x in X . s1 holds
( (
s1 <= s2 implies
[(root-tree [x,s1]),(root-tree [x,s1])] in R . s2 ) & ( for
y being
set st (
[(root-tree [x,s1]),y] in R . s2 or
[y,(root-tree [x,s1])] in R . s2 ) holds
(
s1 <= s2 &
y = root-tree [x,s1] ) ) ) ) & ( for
o1,
o2 being
OperSymbol of
S for
x1 being
Element of
Args (
o1,
(ParsedTermsOSA X))
for
x2 being
Element of
Args (
o2,
(ParsedTermsOSA X))
for
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) ) ) ) ) ) ) )
theorem Th28:
:: deftheorem Def24 defines PTVars OSAFREE:def 24 :
for S being locally_directed OrderSortedSign
for X being V16() ManySortedSet of S
for s being Element of S
for b4 being Subset of ( the Sorts of (ParsedTermsOSA X) . s) holds
( b4 = PTVars (s,X) iff for x being set holds
( x in b4 iff ex a being set st
( a in X . s & x = root-tree [a,s] ) ) );
theorem Th29:
:: deftheorem Def25 defines PTVars OSAFREE:def 25 :
for S being locally_directed OrderSortedSign
for X being V16() ManySortedSet of S
for b3 being MSSubset of (ParsedTermsOSA X) holds
( b3 = PTVars X iff for s being Element of S holds b3 . s = PTVars (s,X) );
theorem
definition
let S be
locally_directed OrderSortedSign;
let X be
V16()
ManySortedSet of
S;
let s be
Element of
S;
func OSFreeGen (
s,
X)
-> Subset of
( the Sorts of (FreeOSA X) . s) means :
Def26:
for
x being
set holds
(
x in it iff ex
a being
set st
(
a in X . s &
x = ((OSNat_Hom ((ParsedTermsOSA X),(LCongruence X))) . s) . (root-tree [a,s]) ) );
existence
ex b1 being Subset of ( the Sorts of (FreeOSA X) . s) st
for x being set holds
( x in b1 iff ex a being set st
( a in X . s & x = ((OSNat_Hom ((ParsedTermsOSA X),(LCongruence X))) . s) . (root-tree [a,s]) ) )
uniqueness
for b1, b2 being Subset of ( the Sorts of (FreeOSA X) . s) st ( for x being set holds
( x in b1 iff ex a being set st
( a in X . s & x = ((OSNat_Hom ((ParsedTermsOSA X),(LCongruence X))) . s) . (root-tree [a,s]) ) ) ) & ( for x being set holds
( x in b2 iff ex a being set st
( a in X . s & x = ((OSNat_Hom ((ParsedTermsOSA X),(LCongruence X))) . s) . (root-tree [a,s]) ) ) ) holds
b1 = b2
end;
:: deftheorem Def26 defines OSFreeGen OSAFREE:def 26 :
for S being locally_directed OrderSortedSign
for X being V16() ManySortedSet of S
for s being Element of S
for b4 being Subset of ( the Sorts of (FreeOSA X) . s) holds
( b4 = OSFreeGen (s,X) iff for x being set holds
( x in b4 iff ex a being set st
( a in X . s & x = ((OSNat_Hom ((ParsedTermsOSA X),(LCongruence X))) . s) . (root-tree [a,s]) ) ) );
theorem Th31:
:: deftheorem Def27 defines OSFreeGen OSAFREE:def 27 :
for S being locally_directed OrderSortedSign
for X being V16() ManySortedSet of S
for b3 being OSGeneratorSet of FreeOSA X holds
( b3 = OSFreeGen X iff for s being Element of S holds b3 . s = OSFreeGen (s,X) );
theorem Th32:
:: deftheorem Def28 defines OSClass OSAFREE:def 28 :
for S being locally_directed OrderSortedSign
for X being V16() ManySortedSet of S
for R being OSCongruence of ParsedTermsOSA X
for t being Element of TS (DTConOSA X)
for b5 being Element of OSClass (R,(LeastSort t)) holds
( b5 = OSClass (R,t) iff for s being Element of S
for x being Element of the Sorts of (ParsedTermsOSA X) . s st t = x holds
b5 = OSClass (R,x) );
theorem Th33:
theorem Th34:
theorem Th35:
theorem Th36:
theorem Th37:
:: deftheorem Def29 defines pi OSAFREE:def 29 :
for S being locally_directed OrderSortedSign
for X being V16() ManySortedSet of S
for A being V16() ManySortedSet of the carrier of S
for F being ManySortedFunction of PTVars X,A
for t being Symbol of (DTConOSA X) st t in Terminals (DTConOSA X) holds
for b6 being Element of Union A holds
( b6 = pi (F,A,t) iff for f being Function st f = F . (t `2) holds
b6 = f . (root-tree t) );
theorem Th38:
definition
let S be
locally_directed OrderSortedSign;
let X be
V16()
ManySortedSet of
S;
let s be
Element of
S;
func NHReverse (
s,
X)
-> Function of
(OSFreeGen (s,X)),
(PTVars (s,X)) means
for
t being
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;
existence
ex b1 being Function of (OSFreeGen (s,X)),(PTVars (s,X)) st
for t being Symbol of (DTConOSA X) st ((OSNat_Hom ((ParsedTermsOSA X),(LCongruence X))) . s) . (root-tree t) in OSFreeGen (s,X) holds
b1 . (((OSNat_Hom ((ParsedTermsOSA X),(LCongruence X))) . s) . (root-tree t)) = root-tree t
uniqueness
for b1, b2 being Function of (OSFreeGen (s,X)),(PTVars (s,X)) st ( for t being Symbol of (DTConOSA X) st ((OSNat_Hom ((ParsedTermsOSA X),(LCongruence X))) . s) . (root-tree t) in OSFreeGen (s,X) holds
b1 . (((OSNat_Hom ((ParsedTermsOSA X),(LCongruence X))) . s) . (root-tree t)) = root-tree t ) & ( for t being Symbol of (DTConOSA X) st ((OSNat_Hom ((ParsedTermsOSA X),(LCongruence X))) . s) . (root-tree t) in OSFreeGen (s,X) holds
b2 . (((OSNat_Hom ((ParsedTermsOSA X),(LCongruence X))) . s) . (root-tree t)) = root-tree t ) holds
b1 = b2
end;
:: deftheorem defines NHReverse OSAFREE:def 30 :
for S being locally_directed OrderSortedSign
for X being V16() ManySortedSet of S
for s being Element of S
for b4 being Function of (OSFreeGen (s,X)),(PTVars (s,X)) holds
( b4 = NHReverse (s,X) iff for t being Symbol of (DTConOSA X) st ((OSNat_Hom ((ParsedTermsOSA X),(LCongruence X))) . s) . (root-tree t) in OSFreeGen (s,X) holds
b4 . (((OSNat_Hom ((ParsedTermsOSA X),(LCongruence X))) . s) . (root-tree t)) = root-tree t );
:: deftheorem defines NHReverse OSAFREE:def 31 :
for S being locally_directed OrderSortedSign
for X being V16() ManySortedSet of S
for b3 being ManySortedFunction of OSFreeGen X, PTVars X holds
( b3 = NHReverse X iff for s being Element of S holds b3 . s = NHReverse (s,X) );
theorem Th39:
theorem Th40:
begin
definition
let S be
monotone regular locally_directed OrderSortedSign;
let X be
V16()
ManySortedSet of
S;
func PTMin X -> Function of
(TS (DTConOSA X)),
(TS (DTConOSA X)) means :
Def32:
( ( 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) for
ts being
FinSequence of
TS (DTConOSA X) st
nt ==> roots ts holds
it . (nt -tree ts) = pi (
(@ (X,nt)),
(it * ts)) ) );
existence
ex b1 being Function of (TS (DTConOSA X)),(TS (DTConOSA X)) st
( ( for t being Symbol of (DTConOSA X) st t in Terminals (DTConOSA X) holds
b1 . (root-tree t) = pi t ) & ( for nt being Symbol of (DTConOSA X)
for ts being FinSequence of TS (DTConOSA X) st nt ==> roots ts holds
b1 . (nt -tree ts) = pi ((@ (X,nt)),(b1 * ts)) ) )
uniqueness
for b1, b2 being Function of (TS (DTConOSA X)),(TS (DTConOSA X)) st ( for t being Symbol of (DTConOSA X) st t in Terminals (DTConOSA X) holds
b1 . (root-tree t) = pi t ) & ( for nt being Symbol of (DTConOSA X)
for ts being FinSequence of TS (DTConOSA X) st nt ==> roots ts holds
b1 . (nt -tree ts) = pi ((@ (X,nt)),(b1 * ts)) ) & ( for t being Symbol of (DTConOSA X) st t in Terminals (DTConOSA X) holds
b2 . (root-tree t) = pi t ) & ( for nt being Symbol of (DTConOSA X)
for ts being FinSequence of TS (DTConOSA X) st nt ==> roots ts holds
b2 . (nt -tree ts) = pi ((@ (X,nt)),(b2 * ts)) ) holds
b1 = b2
end;
:: deftheorem Def32 defines PTMin OSAFREE:def 32 :
for S being monotone regular locally_directed OrderSortedSign
for X being V16() ManySortedSet of S
for b3 being Function of (TS (DTConOSA X)),(TS (DTConOSA X)) holds
( b3 = PTMin X iff ( ( for t being Symbol of (DTConOSA X) st t in Terminals (DTConOSA X) holds
b3 . (root-tree t) = pi t ) & ( for nt being Symbol of (DTConOSA X)
for ts being FinSequence of TS (DTConOSA X) st nt ==> roots ts holds
b3 . (nt -tree ts) = pi ((@ (X,nt)),(b3 * ts)) ) ) );
theorem Th41:
theorem Th42:
theorem Th43:
theorem Th44:
theorem Th45:
theorem Th46:
theorem
:: deftheorem Def33 defines MinTerm OSAFREE:def 33 :
for S being monotone regular locally_directed OrderSortedSign
for X being V16() ManySortedSet of S
for b3 being Element of TS (DTConOSA X) holds
( b3 is MinTerm of S,X iff (PTMin X) . b3 = b3 );
:: deftheorem defines MinTerms OSAFREE:def 34 :
for S being monotone regular locally_directed OrderSortedSign
for X being V16() ManySortedSet of S holds MinTerms X = rng (PTMin X);
theorem