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 :
:: deftheorem Def2 defines coprod MSAFREE:def 2 :
:: deftheorem Def3 defines coprod MSAFREE:def 3 :
theorem
begin
:: deftheorem Def4 defines GeneratorSet MSAFREE:def 4 :
theorem
:: deftheorem Def5 defines free MSAFREE:def 5 :
:: deftheorem Def6 defines free MSAFREE:def 6 :
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 ,
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 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 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 , 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 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 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 , 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 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 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 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 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 :
theorem Th5:
:: deftheorem defines DTConMSA MSAFREE:def 10 :
theorem Th6:
theorem Th7:
:: deftheorem defines Sym MSAFREE:def 11 :
:: deftheorem defines FreeSort MSAFREE:def 12 :
:: deftheorem Def13 defines FreeSort MSAFREE:def 13 :
theorem Th8:
theorem Th9:
theorem Th10:
theorem
canceled;
theorem Th12:
theorem Th13:
definition
let S be non
empty non
void ManySortedSign ;
let X be
V5()
ManySortedSet of ;
let o be
OperSymbol of ;
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 :
:: deftheorem Def15 defines FreeOper MSAFREE:def 15 :
:: deftheorem defines FreeMSA MSAFREE:def 16 :
:: deftheorem Def17 defines FreeGen MSAFREE:def 17 :
theorem Th14:
:: deftheorem Def18 defines FreeGen MSAFREE:def 18 :
theorem
theorem
definition
let S be non
empty non
void ManySortedSign ;
let X be
V5()
ManySortedSet of ;
let s be
SortSymbol of ;
func Reverse s,
X -> Function of
FreeGen s,
X,
X . s means :
Def19:
for
t being
Symbol of 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 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 st root-tree t in FreeGen s,X holds
b1 . (root-tree t) = t `1 ) & ( for t being Symbol of 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 :
:: deftheorem Def20 defines Reverse MSAFREE:def 20 :
:: deftheorem Def21 defines pi MSAFREE:def 21 :
:: deftheorem Def22 defines @ MSAFREE:def 22 :
:: deftheorem Def23 defines pi MSAFREE:def 23 :
theorem Th17:
theorem Th18:
theorem Th19:
theorem