begin
theorem Th1:
theorem Th2:
theorem
:: deftheorem Def1 defines Flatten MSAFREE1:def 1 :
theorem Th4:
:: deftheorem Def2 defines disjoint_valued MSAFREE1:def 2 :
:: deftheorem Def3 defines SingleAlg MSAFREE1:def 3 :
Lm1:
for S being non empty ManySortedSign holds
( SingleAlg S is non-empty & SingleAlg S is disjoint_valued )
theorem Th5:
scheme
FreeSortUniq{
F1()
-> non
empty non
void ManySortedSign ,
F2()
-> V2()
ManySortedSet of ,
F3()
-> V2()
ManySortedSet of ,
F4(
set )
-> Element of
Union F3(),
F5(
set ,
set ,
set )
-> Element of
Union F3(),
F6()
-> ManySortedFunction of
FreeSort F2(),
F3(),
F7()
-> ManySortedFunction of
FreeSort F2(),
F3() } :
provided
A1:
for
o being
OperSymbol of
for
ts being
Element of
Args o,
(FreeMSA F2()) for
x being
FinSequence of
Union F3() st
x = (Flatten F6()) * ts holds
(F6() . (the_result_sort_of o)) . ((Den o,(FreeMSA F2())) . ts) = F5(
o,
ts,
x)
and A2:
for
s being
SortSymbol of
for
y being
set st
y in FreeGen s,
F2() holds
(F6() . s) . y = F4(
y)
and A3:
for
o being
OperSymbol of
for
ts being
Element of
Args o,
(FreeMSA F2()) for
x being
FinSequence of
Union F3() st
x = (Flatten F7()) * ts holds
(F7() . (the_result_sort_of o)) . ((Den o,(FreeMSA F2())) . ts) = F5(
o,
ts,
x)
and A4:
for
s being
SortSymbol of
for
y being
set st
y in FreeGen s,
F2() holds
(F7() . s) . y = F4(
y)
scheme
ExtFreeGen{
F1()
-> non
empty non
void ManySortedSign ,
F2()
-> V2()
ManySortedSet of ,
F3()
-> non-empty MSAlgebra of
F1(),
P1[
set ,
set ,
set ],
F4()
-> ManySortedFunction of ,
(FreeMSA F2()),
F5()
-> ManySortedFunction of ,
(FreeMSA F2()) } :
provided
A1:
F4()
is_homomorphism FreeMSA F2(),
F3()
and A2:
for
s being
SortSymbol of
for
x,
y being
set st
y in FreeGen s,
F2() holds
(
(F4() . s) . y = x iff
P1[
s,
x,
y] )
and A3:
F5()
is_homomorphism FreeMSA F2(),
F3()
and A4:
for
s being
SortSymbol of
for
x,
y being
set st
y in FreeGen s,
F2() holds
(
(F5() . s) . y = x iff
P1[
s,
x,
y] )