environ
vocabularies HIDDEN, TARSKI, QC_LANG3, PBOOLE, MSUALG_1, CATALG_1, FINSEQ_1, XBOOLE_0, ZFMISC_1, ARYTM_3, CARD_1, NAT_1, NUMBERS, XXREAL_0, ZF_LANG1, ORDINAL1, TREES_A, ABIAN, CARD_3, MEMBER_1, FINSET_1, FUNCOP_1, FUNCT_1, TREES_4, TREES_2, MSATERM, RELAT_1, MCART_1, MSAFREE, ZF_MODEL, AOFA_000, FINSEQ_2, PARTFUN1, QC_LANG1, FUNCT_2, ORDINAL4, CAT_3, TREES_3, ABCMIZ_0, ABCMIZ_1, ABCMIZ_A, STRUCT_0, FACIRC_1, INSTALG1, MSUALG_2, COMPUT_1, BINTREE1, TREES_9, ARYTM_1, FUNCT_6, SUBSET_1, MARGREL1, SETLIM_2;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, XTUPLE_0, XFAMILY, SUBSET_1, DOMAIN_1, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, FACIRC_1, ENUMSET1, FUNCOP_1, XCMPLX_0, XXREAL_0, ORDINAL1, NAT_D, MCART_1, FINSET_1, CARD_1, NUMBERS, CARD_3, FINSEQ_1, FINSEQ_2, FINSEQ_4, FUNCT_6, TREES_1, TREES_2, TREES_3, TREES_4, TREES_9, PBOOLE, STRUCT_0, MSUALG_1, MSUALG_2, MSAFREE, EQUATION, MSATERM, INSTALG1, CATALG_1, MSAFREE3, AOFA_000, ABCMIZ_1;
definitions TARSKI, XBOOLE_0, RELAT_1, FUNCT_1, PBOOLE, ABCMIZ_1;
theorems TARSKI, XBOOLE_0, XBOOLE_1, TREES_1, XXREAL_0, XREAL_1, ZFMISC_1, FUNCT_1, FUNCT_2, FINSEQ_1, FINSEQ_2, ENUMSET1, FUNCT_6, INSTALG1, NAT_1, MCART_1, PBOOLE, RELAT_1, RELSET_1, CARD_1, CARD_5, ORDINAL1, MSUALG_2, TREES_3, TREES_4, FINSEQ_3, FUNCOP_1, MSAFREE, MSATERM, MSAFREE3, YELLOW11, PARTFUN1, WELLORD2, ABCMIZ_1, TREES_9, XTUPLE_0, XREGULAR;
schemes FUNCT_1, NAT_1, RECDEF_1, CLASSES1, FINSEQ_1;
registrations XBOOLE_0, SUBSET_1, XREAL_0, ORDINAL1, FUNCT_1, FINSET_1, STRUCT_0, PBOOLE, MSUALG_2, FINSEQ_1, NAT_1, CARD_1, TREES_3, TREES_2, FUNCOP_1, RELAT_1, INDEX_1, INSTALG1, MSAFREE3, WAYBEL26, FACIRC_1, ABCMIZ_1, MSATERM, RELSET_1, XTUPLE_0;
constructors HIDDEN, RELSET_1, DOMAIN_1, WELLORD2, TREES_9, EQUATION, NAT_D, FINSEQ_4, CATALG_1, FACIRC_1, ABCMIZ_1, PRE_POLY, XTUPLE_0, XFAMILY;
requirements HIDDEN, BOOLE, SUBSET, NUMERALS, ARITHM, REAL;
equalities TARSKI, SUBSET_1, FINSEQ_1, MSAFREE, MSAFREE3, MSUALG_1, ABCMIZ_1, ORDINAL1, CARD_1;
expansions TARSKI, XBOOLE_0, FUNCT_1, PBOOLE, ABCMIZ_1, ORDINAL1;
scheme
MinimalElement{
F1()
-> non
empty finite set ,
P1[
set ,
set ] } :
ex
x being
set st
(
x in F1() & ( for
y being
set st
y in F1() holds
not
P1[
y,
x] ) )
provided
A1:
for
x,
y being
set st
x in F1() &
y in F1() &
P1[
x,
y] holds
not
P1[
y,
x]
and A2:
for
x,
y,
z being
set st
x in F1() &
y in F1() &
z in F1() &
P1[
x,
y] &
P1[
y,
z] holds
P1[
x,
z]
scheme
FiniteC{
F1()
-> finite set ,
P1[
set ] } :
provided
A1:
for
A being
Subset of
F1() st ( for
B being
set st
B c< A holds
P1[
B] ) holds
P1[
A]
scheme
Numeration{
F1()
-> finite set ,
P1[
set ,
set ] } :
provided
A1:
for
x,
y being
set st
x in F1() &
y in F1() &
P1[
x,
y] holds
not
P1[
y,
x]
and A2:
for
x,
y,
z being
set st
x in F1() &
y in F1() &
z in F1() &
P1[
x,
y] &
P1[
y,
z] holds
P1[
x,
z]
set MC = MaxConstrSign ;
:: for t1,t2 being expression of C st t1 matches_with t2
:: holds t1,t2 are_weakly-unifiable;