begin
theorem Th1:
definition
let I be
set ;
let A,
B be
ManySortedSet of
I;
let C be
ManySortedSubset of
A;
let F be
ManySortedFunction of
A,
B;
func F || C -> ManySortedFunction of
C,
B means :
Def1:
for
i being
set st
i in I holds
for
f being
Function of
(A . i),
(B . i) st
f = F . i holds
it . i = f | (C . i);
existence
ex b1 being ManySortedFunction of C,B st
for i being set st i in I holds
for f being Function of (A . i),(B . i) st f = F . i holds
b1 . i = f | (C . i)
uniqueness
for b1, b2 being ManySortedFunction of C,B st ( for i being set st i in I holds
for f being Function of (A . i),(B . i) st f = F . i holds
b1 . i = f | (C . i) ) & ( for i being set st i in I holds
for f being Function of (A . i),(B . i) st f = F . i holds
b2 . i = f | (C . i) ) holds
b1 = b2
end;
:: deftheorem Def1 defines || MSAFREE:def 1 :
for I being set
for A, B being ManySortedSet of I
for C being ManySortedSubset of A
for F being ManySortedFunction of A,B
for b6 being ManySortedFunction of C,B holds
( b6 = F || C iff for i being set st i in I holds
for f being Function of (A . i),(B . i) st f = F . i holds
b6 . i = f | (C . i) );
:: deftheorem Def2 defines coprod MSAFREE:def 2 :
for I being set
for X being ManySortedSet of I
for i being set st i in I holds
for b4 being set holds
( b4 = coprod (i,X) iff for x being set holds
( x in b4 iff ex a being set st
( a in X . i & x = [a,i] ) ) );
:: deftheorem Def3 defines coprod MSAFREE:def 3 :
for I being set
for X being ManySortedSet of I
for b3 being set holds
( b3 = coprod X iff ( dom b3 = I & ( for i being set st i in I holds
b3 . i = coprod (i,X) ) ) );
theorem
begin
:: deftheorem Def4 defines GeneratorSet MSAFREE:def 4 :
for S being non empty non void ManySortedSign
for U0 being MSAlgebra of S
for b3 being MSSubset of U0 holds
( b3 is GeneratorSet of U0 iff the Sorts of (GenMSAlg b3) = the Sorts of U0 );
theorem
:: deftheorem Def5 defines free MSAFREE:def 5 :
for S being non empty non void ManySortedSign
for U0 being MSAlgebra of S
for IT being GeneratorSet of U0 holds
( IT is free iff for U1 being non-empty MSAlgebra 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 || IT = f ) );
:: deftheorem Def6 defines free MSAFREE:def 6 :
for S being non empty non void ManySortedSign
for IT being MSAlgebra of S holds
( IT is free iff ex G being GeneratorSet of IT st G is free );
theorem Th4:
begin
definition
let S be non
empty non
void ManySortedSign ;
let X be
ManySortedSet of the
carrier of
S;
canceled;canceled;func REL 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 :
Def9:
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
b . x in coprod (
((the_arity_of o) . x),
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 b . x in coprod (((the_arity_of o) . x),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 b . x in coprod (((the_arity_of o) . x),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 b . x in coprod (((the_arity_of o) . x),X) ) ) ) ) ) ) ) ) holds
b1 = b2
end;
:: deftheorem MSAFREE:def 7 :
canceled;
:: deftheorem MSAFREE:def 8 :
canceled;
:: deftheorem Def9 defines REL MSAFREE:def 9 :
for S being non empty non void ManySortedSign
for X being ManySortedSet of the carrier 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 = REL 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 b . x in coprod (((the_arity_of o) . x),X) ) ) ) ) ) ) ) );
theorem Th5:
:: deftheorem defines DTConMSA MSAFREE:def 10 :
for S being non empty non void ManySortedSign
for X being ManySortedSet of the carrier of S holds DTConMSA X = DTConstrStr(# ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))),(REL X) #);
theorem Th6:
theorem Th7:
:: deftheorem defines Sym MSAFREE:def 11 :
for S being non empty non void ManySortedSign
for X being V16() ManySortedSet of the carrier of S
for o being OperSymbol of S holds Sym (o,X) = [o, the carrier of S];
:: deftheorem defines FreeSort MSAFREE:def 12 :
for S being non empty non void ManySortedSign
for X being V16() ManySortedSet of the carrier of S
for s being SortSymbol of S holds FreeSort (X,s) = { a where a is Element of TS (DTConMSA X) : ( ex x being set st
( x in X . s & a = root-tree [x,s] ) or ex o being OperSymbol of S st
( [o, the carrier of S] = a . {} & the_result_sort_of o = s ) ) } ;
:: deftheorem Def13 defines FreeSort MSAFREE:def 13 :
for S being non empty non void ManySortedSign
for X being V16() ManySortedSet of the carrier of S
for b3 being ManySortedSet of the carrier of S holds
( b3 = FreeSort X iff for s being SortSymbol of S holds b3 . s = FreeSort (X,s) );
theorem Th8:
theorem Th9:
theorem Th10:
theorem
canceled;
theorem Th12:
theorem Th13:
definition
let S be non
empty non
void ManySortedSign ;
let X be
V16()
ManySortedSet of the
carrier of
S;
let o be
OperSymbol of
S;
func DenOp (
o,
X)
-> Function of
((((FreeSort X) #) * the Arity of S) . o),
(((FreeSort X) * the ResultSort of S) . o) means :
Def14:
for
p being
FinSequence of
TS (DTConMSA X) st
Sym (
o,
X)
==> roots p holds
it . p = (Sym (o,X)) -tree p;
existence
ex b1 being Function of ((((FreeSort X) #) * the Arity of S) . o),(((FreeSort X) * the ResultSort of S) . o) st
for p being FinSequence of TS (DTConMSA X) st Sym (o,X) ==> roots p holds
b1 . p = (Sym (o,X)) -tree p
uniqueness
for b1, b2 being Function of ((((FreeSort X) #) * the Arity of S) . o),(((FreeSort X) * the ResultSort of S) . o) st ( for p being FinSequence of TS (DTConMSA X) st Sym (o,X) ==> roots p holds
b1 . p = (Sym (o,X)) -tree p ) & ( for p being FinSequence of TS (DTConMSA X) st Sym (o,X) ==> roots p holds
b2 . p = (Sym (o,X)) -tree p ) holds
b1 = b2
end;
:: deftheorem Def14 defines DenOp MSAFREE:def 14 :
for S being non empty non void ManySortedSign
for X being V16() ManySortedSet of the carrier of S
for o being OperSymbol of S
for b4 being Function of ((((FreeSort X) #) * the Arity of S) . o),(((FreeSort X) * the ResultSort of S) . o) holds
( b4 = DenOp (o,X) iff for p being FinSequence of TS (DTConMSA X) st Sym (o,X) ==> roots p holds
b4 . p = (Sym (o,X)) -tree p );
:: deftheorem Def15 defines FreeOper MSAFREE:def 15 :
for S being non empty non void ManySortedSign
for X being V16() ManySortedSet of the carrier of S
for b3 being ManySortedFunction of ((FreeSort X) #) * the Arity of S,(FreeSort X) * the ResultSort of S holds
( b3 = FreeOper X iff for o being OperSymbol of S holds b3 . o = DenOp (o,X) );
:: deftheorem defines FreeMSA MSAFREE:def 16 :
for S being non empty non void ManySortedSign
for X being V16() ManySortedSet of the carrier of S holds FreeMSA X = MSAlgebra(# (FreeSort X),(FreeOper X) #);
:: deftheorem Def17 defines FreeGen MSAFREE:def 17 :
for S being non empty non void ManySortedSign
for X being V16() ManySortedSet of the carrier of S
for s being SortSymbol of S
for b4 being Subset of ((FreeSort X) . s) holds
( b4 = FreeGen (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 Th14:
:: deftheorem Def18 defines FreeGen MSAFREE:def 18 :
for S being non empty non void ManySortedSign
for X being V16() ManySortedSet of the carrier of S
for b3 being GeneratorSet of FreeMSA X holds
( b3 = FreeGen X iff for s being SortSymbol of S holds b3 . s = FreeGen (s,X) );
theorem
theorem
definition
let S be non
empty non
void ManySortedSign ;
let X be
V16()
ManySortedSet of the
carrier of
S;
let s be
SortSymbol of
S;
func Reverse (
s,
X)
-> Function of
(FreeGen (s,X)),
(X . s) means :
Def19:
for
t being
Symbol of
(DTConMSA X) st
root-tree t in FreeGen (
s,
X) holds
it . (root-tree t) = t `1 ;
existence
ex b1 being Function of (FreeGen (s,X)),(X . s) st
for t being Symbol of (DTConMSA X) st root-tree t in FreeGen (s,X) holds
b1 . (root-tree t) = t `1
uniqueness
for b1, b2 being Function of (FreeGen (s,X)),(X . s) st ( for t being Symbol of (DTConMSA X) st root-tree t in FreeGen (s,X) holds
b1 . (root-tree t) = t `1 ) & ( for t being Symbol of (DTConMSA X) st root-tree t in FreeGen (s,X) holds
b2 . (root-tree t) = t `1 ) holds
b1 = b2
end;
:: deftheorem Def19 defines Reverse MSAFREE:def 19 :
for S being non empty non void ManySortedSign
for X being V16() ManySortedSet of the carrier of S
for s being SortSymbol of S
for b4 being Function of (FreeGen (s,X)),(X . s) holds
( b4 = Reverse (s,X) iff for t being Symbol of (DTConMSA X) st root-tree t in FreeGen (s,X) holds
b4 . (root-tree t) = t `1 );
:: deftheorem Def20 defines Reverse MSAFREE:def 20 :
for S being non empty non void ManySortedSign
for X being V16() ManySortedSet of the carrier of S
for b3 being ManySortedFunction of FreeGen X,X holds
( b3 = Reverse X iff for s being SortSymbol of S holds b3 . s = Reverse (s,X) );
:: deftheorem Def21 defines pi MSAFREE:def 21 :
for S being non empty non void ManySortedSign
for X, A being V16() ManySortedSet of the carrier of S
for F being ManySortedFunction of FreeGen X,A
for t being Symbol of (DTConMSA X) st t in Terminals (DTConMSA 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) );
:: deftheorem Def22 defines @ MSAFREE:def 22 :
for S being non empty non void ManySortedSign
for X being V16() ManySortedSet of the carrier of S
for t being Symbol of (DTConMSA 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 Def23 defines pi MSAFREE:def 23 :
for S being non empty non void ManySortedSign
for U0 being non-empty MSAlgebra of S
for o being OperSymbol of S
for p being FinSequence st p in Args (o,U0) holds
pi (o,U0,p) = (Den (o,U0)) . p;
theorem Th17:
theorem Th18:
theorem Th19:
theorem