environ
vocabularies HIDDEN, XBOOLE_0, FUNCT_1, RELAT_1, PBOOLE, SUBSET_1, CARD_3, REALSET1, TARSKI, ZFMISC_1, PARTFUN1, STRUCT_0, MSUALG_1, MSUALG_2, PRELAMB, MSUALG_3, FINSEQ_1, MARGREL1, LANG1, TDGROUP, DTCONSTR, TREES_3, TREES_4, NAT_1, TREES_2, MCART_1, UNIALG_2, QC_LANG1, GROUP_6, MSAFREE;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, XTUPLE_0, SUBSET_1, ORDINAL1, NAT_1, RELAT_1, RELSET_1, STRUCT_0, FUNCT_1, PARTFUN1, MCART_1, FUNCT_2, FINSEQ_1, PBOOLE, TREES_2, FINSEQ_2, CARD_3, LANG1, TREES_4, DTCONSTR, MSUALG_1, MSUALG_2, MSUALG_3;
definitions TARSKI, XBOOLE_0, PBOOLE, MSUALG_3;
theorems TARSKI, FUNCT_1, FUNCT_2, ZFMISC_1, PBOOLE, CARD_3, MSUALG_1, MSUALG_2, MSUALG_3, RELAT_1, LANG1, DTCONSTR, FINSEQ_1, TREES_4, TREES_1, DOMAIN_1, RELSET_1, XBOOLE_0, XBOOLE_1, FUNCOP_1, TREES_3, PARTFUN1, FINSEQ_3, FINSEQ_2, XTUPLE_0;
schemes CLASSES1, FUNCT_1, RELSET_1, DTCONSTR, XBOOLE_0;
registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, FUNCOP_1, FINSEQ_1, PBOOLE, TREES_2, TREES_3, STRUCT_0, DTCONSTR, MSUALG_1, MSUALG_3, FUNCT_2, PARTFUN1, RELSET_1, XTUPLE_0;
constructors HIDDEN, XXREAL_0, NAT_1, NAT_D, CARD_3, FINSEQOP, DTCONSTR, MSUALG_3, RELSET_1, PBOOLE, XTUPLE_0;
requirements HIDDEN, NUMERALS, BOOLE, SUBSET;
equalities TARSKI;
expansions TARSKI, XBOOLE_0, PBOOLE, MSUALG_3;
definition
let S be non
empty non
void ManySortedSign ;
let X be
ManySortedSet of the
carrier of
S;
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 :
Def7:
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 Def7 defines
REL MSAFREE:def 7 :
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) ) ) ) ) ) ) ) );
:: Preliminaries
::