begin
Lm1:
for S being non empty ManySortedSign holds
( SingleAlg S is non-empty & SingleAlg S is disjoint_valued )
scheme
FreeSortUniq{
F1()
-> non
empty non
void ManySortedSign ,
F2()
-> V2()
ManySortedSet of the
carrier of
F1(),
F3()
-> V2()
ManySortedSet of the
carrier of
F1(),
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
F1()
for
ts being
Element of
Args (
o,
(FreeMSA F2()))
for
x being
Element 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
F1()
for
y being
set st
y in FreeGen (
s,
F2()) holds
(F6() . s) . y = F4(
y)
and A3:
for
o being
OperSymbol of
F1()
for
ts being
Element of
Args (
o,
(FreeMSA F2()))
for
x being
Element 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
F1()
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 the
carrier of
F1(),
F3()
-> non-empty MSAlgebra over
F1(),
P1[
set ,
set ,
set ],
F4()
-> ManySortedFunction of
(FreeMSA F2()),
F3(),
F5()
-> ManySortedFunction of
(FreeMSA F2()),
F3() } :
provided
A1:
F4()
is_homomorphism FreeMSA F2(),
F3()
and A2:
for
s being
SortSymbol of
F1()
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
F1()
for
x,
y being
set st
y in FreeGen (
s,
F2()) holds
(
(F5() . s) . y = x iff
P1[
s,
x,
y] )