environ
vocabularies HIDDEN, FUNCT_1, CARD_3, RELAT_1, TARSKI, XBOOLE_0, LANG1, SUBSET_1, DTCONSTR, TREES_4, FINSEQ_1, TDGROUP, TREES_3, TREES_2, STRUCT_0, MSUALG_1, PBOOLE, MSAFREE, ZFMISC_1, MARGREL1, PROB_2, NAT_1, PARTFUN1, MCART_1, MSUALG_3, MSAFREE1;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NAT_1, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2, FINSEQ_2, STRUCT_0, XTUPLE_0, MCART_1, FINSEQ_1, MULTOP_1, PROB_2, CARD_3, TREES_2, TREES_3, TREES_4, LANG1, DTCONSTR, PBOOLE, MSUALG_1, MSAFREE, MSUALG_3;
definitions TARSKI, MSUALG_1, PBOOLE, PROB_2;
theorems MSAFREE, MSUALG_3, LANG1, FINSEQ_1, CARD_3, PBOOLE, FUNCT_1, FUNCT_2, DTCONSTR, TARSKI, ZFMISC_1, PROB_2, CARD_5, RELAT_1, DOMAIN_1, XBOOLE_0, XBOOLE_1, PARTFUN1, FINSEQ_2, XTUPLE_0;
schemes DTCONSTR, FUNCT_2, MULTOP_1, PBOOLE;
registrations XBOOLE_0, FUNCT_1, RELSET_1, FINSEQ_1, RELAT_1, TREES_3, STRUCT_0, DTCONSTR, MSUALG_1, MSUALG_3, MSAFREE, ORDINAL1, PBOOLE, XTUPLE_0;
constructors HIDDEN, MULTOP_1, PROB_2, MSUALG_3, MSAFREE, RELSET_1, CAT_3, FINSEQ_2, XTUPLE_0;
requirements HIDDEN, BOOLE, SUBSET;
equalities MSUALG_1;
expansions TARSKI, PBOOLE;
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(
object ,
object ,
object )
-> 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[
object ,
object ,
object ],
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] )