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
([: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 :
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 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 :
:: 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 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 :
:: 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