environ
vocabularies HIDDEN, NUMBERS, NAT_1, SUBSET_1, FUNCT_1, TARSKI, CARD_3, RELAT_1, XBOOLE_0, STRUCT_0, CATALG_1, PBOOLE, MSATERM, FACIRC_1, MSUALG_1, ZFMISC_1, ZF_MODEL, FUNCOP_1, CARD_1, FINSEQ_1, TREES_3, TREES_4, MARGREL1, MSAFREE, CLASSES1, SETFAM_1, FINSET_1, QC_LANG3, ARYTM_3, XXREAL_0, ORDINAL1, MCART_1, FINSEQ_2, ORDINAL4, PARTFUN1, ABCMIZ_0, FUNCT_2, FUNCT_4, ZF_LANG1, CAT_3, TREES_2, MSUALG_2, MEMBER_1, AOFA_000, CARD_5, ORDERS_2, YELLOW_1, ARYTM_0, LATTICE3, EQREL_1, LATTICES, YELLOW_0, ORDINAL2, WAYBEL_0, ASYMPT_0, LANG1, TDGROUP, DTCONSTR, BINOP_1, MATRIX_7, FUNCT_7, ABCMIZ_1, SETLIM_2;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, XTUPLE_0, XFAMILY, SUBSET_1, DOMAIN_1, SETFAM_1, RELAT_1, FUNCT_1, RELSET_1, BINOP_1, PARTFUN1, FACIRC_1, ENUMSET1, FUNCT_2, PARTIT_2, FUNCT_4, FUNCOP_1, XXREAL_0, ORDINAL1, XCMPLX_0, NAT_1, MCART_1, FINSET_1, CARD_1, NUMBERS, CARD_3, FINSEQ_1, FINSEQ_2, TREES_2, TREES_3, TREES_4, FUNCT_7, PBOOLE, MATRIX_7, XXREAL_2, STRUCT_0, LANG1, CLASSES1, ORDERS_2, LATTICE3, YELLOW_0, WAYBEL_0, YELLOW_1, YELLOW_7, DTCONSTR, MSUALG_1, MSUALG_2, MSAFREE, EQUATION, MSATERM, CATALG_1, MSAFREE3, AOFA_000, PRE_POLY;
definitions TARSKI, XBOOLE_0, RELAT_1, FUNCT_1, FINSEQ_2, LANG1, LATTICE3, PBOOLE, TREES_3, MSUALG_1, WAYBEL_0, XTUPLE_0;
theorems TARSKI, XBOOLE_0, XBOOLE_1, TREES_1, XXREAL_0, ZFMISC_1, FUNCT_1, FUNCT_2, FINSEQ_1, FINSEQ_2, SUBSET_1, ENUMSET1, FUNCT_4, PROB_2, LANG1, MATRIX_7, NAT_1, MCART_1, PBOOLE, FINSET_1, RELAT_1, RELSET_1, ORDINAL3, CARD_1, CARD_3, CARD_5, CLASSES1, ORDINAL1, SETFAM_1, MSUALG_2, TREES_4, FINSEQ_3, FUNCOP_1, MSAFREE, MSATERM, MSAFREE3, PARTFUN1, LATTICE3, YELLOW_0, WAYBEL_0, YELLOW_1, YELLOW_7, DTCONSTR, MSAFREE1, XXREAL_2, CARD_2, XTUPLE_0;
schemes XBOOLE_0, FUNCT_1, NAT_1, FRAENKEL, PBOOLE, MSATERM, DTCONSTR, CLASSES1, FUNCT_2;
registrations XBOOLE_0, SUBSET_1, XREAL_0, ORDINAL1, RELSET_1, FUNCT_1, FINSET_1, STRUCT_0, PBOOLE, MSUALG_1, MSUALG_2, FINSEQ_1, CARD_1, MSAFREE, FUNCOP_1, TREES_3, MSAFREE1, PARTFUN1, MSATERM, ORDERS_2, TREES_2, DTCONSTR, WAYBEL_0, YELLOW_1, LATTICE3, MEMBERED, RELAT_1, INDEX_1, INSTALG1, MSAFREE3, FACIRC_1, XXREAL_2, CLASSES1, FINSEQ_2, PARTIT_2, XTUPLE_0, NAT_1;
constructors HIDDEN, DOMAIN_1, MATRIX_7, MSAFREE1, FUNCT_7, EQUATION, YELLOW_1, CATALG_1, LATTICE3, WAYBEL_0, FACIRC_1, CLASSES1, MSAFREE3, XXREAL_2, RELSET_1, PRE_POLY, PARTIT_2, XTUPLE_0, XFAMILY;
requirements HIDDEN, BOOLE, SUBSET, NUMERALS, ARITHM, REAL;
equalities TARSKI, RELAT_1, FINSEQ_1, LANG1, LATTICE3, MSAFREE, MSAFREE3, CARD_3, MSUALG_1, ORDINAL1, CARD_1;
expansions TARSKI, FUNCT_1, LANG1, LATTICE3, PBOOLE, TREES_3;
definition
let A be
set ;
func varcl A -> set means :
Def1:
(
A c= it & ( for
x,
y being
set st
[x,y] in it holds
x c= it ) & ( for
B being
set st
A c= B & ( for
x,
y being
set st
[x,y] in B holds
x c= B ) holds
it c= B ) );
uniqueness
for b1, b2 being set st A c= b1 & ( for x, y being set st [x,y] in b1 holds
x c= b1 ) & ( for B being set st A c= B & ( for x, y being set st [x,y] in B holds
x c= B ) holds
b1 c= B ) & A c= b2 & ( for x, y being set st [x,y] in b2 holds
x c= b2 ) & ( for B being set st A c= B & ( for x, y being set st [x,y] in B holds
x c= B ) holds
b2 c= B ) holds
b1 = b2
existence
ex b1 being set st
( A c= b1 & ( for x, y being set st [x,y] in b1 holds
x c= b1 ) & ( for B being set st A c= B & ( for x, y being set st [x,y] in B holds
x c= B ) holds
b1 c= B ) )
projectivity
for b1, b2 being set st b2 c= b1 & ( for x, y being set st [x,y] in b1 holds
x c= b1 ) & ( for B being set st b2 c= B & ( for x, y being set st [x,y] in B holds
x c= B ) holds
b1 c= B ) holds
( b1 c= b1 & ( for x, y being set st [x,y] in b1 holds
x c= b1 ) & ( for B being set st b1 c= B & ( for x, y being set st [x,y] in B holds
x c= B ) holds
b1 c= B ) )
;
end;
deffunc H1( set , set ) -> set = { [(varcl A),j] where A is Subset of $2, j is Element of NAT : A is finite } ;
definition
existence
ex b1 being set ex V being ManySortedSet of NAT st
( b1 = Union V & V . 0 = { [{},i] where i is Element of NAT : verum } & ( for n being Nat holds V . (n + 1) = { [(varcl A),j] where A is Subset of (V . n), j is Element of NAT : A is finite } ) )
uniqueness
for b1, b2 being set st ex V being ManySortedSet of NAT st
( b1 = Union V & V . 0 = { [{},i] where i is Element of NAT : verum } & ( for n being Nat holds V . (n + 1) = { [(varcl A),j] where A is Subset of (V . n), j is Element of NAT : A is finite } ) ) & ex V being ManySortedSet of NAT st
( b2 = Union V & V . 0 = { [{},i] where i is Element of NAT : verum } & ( for n being Nat holds V . (n + 1) = { [(varcl A),j] where A is Subset of (V . n), j is Element of NAT : A is finite } ) ) holds
b1 = b2
end;
definition
let C be
ConstructorSignature;
A1:
the
carrier of
C = {a_Type,an_Adj,a_Term}
by Def9;
coherence
a_Type is SortSymbol of C
by A1, ENUMSET1:def 1;
coherence
an_Adj is SortSymbol of C
by A1, ENUMSET1:def 1;
coherence
a_Term is SortSymbol of C
by A1, ENUMSET1:def 1;
A2:
{*,non_op} c= the
carrier' of
C
by Def9;
A3:
* in {*,non_op}
by TARSKI:def 2;
A4:
non_op in {*,non_op}
by TARSKI:def 2;
coherence
non_op is OperSymbol of C
by A2, A4;
coherence
* is OperSymbol of C
by A2, A3;
end;
definition
let C be
initialized ConstructorSignature;
let f be
valuation of
C;
existence
ex b1 being term-transformation of C, MSVars C st
( ( for x being variable holds
( ( x in dom f implies b1 . (x -term C) = f . x ) & ( not x in dom f implies b1 . (x -term C) = x -term C ) ) ) & ( for c being constructor OperSymbol of C
for p, q being FinSequence of QuasiTerms C st len p = len (the_arity_of c) & q = b1 * p holds
b1 . (c -trm p) = c -trm q ) & ( for a being expression of C, an_Adj C holds b1 . ((non_op C) term a) = (non_op C) term (b1 . a) ) & ( for a being expression of C, an_Adj C
for t being expression of C, a_Type C holds b1 . ((ast C) term (a,t)) = (ast C) term ((b1 . a),(b1 . t)) ) )
correctness
uniqueness
for b1, b2 being term-transformation of C, MSVars C st ( for x being variable holds
( ( x in dom f implies b1 . (x -term C) = f . x ) & ( not x in dom f implies b1 . (x -term C) = x -term C ) ) ) & ( for c being constructor OperSymbol of C
for p, q being FinSequence of QuasiTerms C st len p = len (the_arity_of c) & q = b1 * p holds
b1 . (c -trm p) = c -trm q ) & ( for a being expression of C, an_Adj C holds b1 . ((non_op C) term a) = (non_op C) term (b1 . a) ) & ( for a being expression of C, an_Adj C
for t being expression of C, a_Type C holds b1 . ((ast C) term (a,t)) = (ast C) term ((b1 . a),(b1 . t)) ) & ( for x being variable holds
( ( x in dom f implies b2 . (x -term C) = f . x ) & ( not x in dom f implies b2 . (x -term C) = x -term C ) ) ) & ( for c being constructor OperSymbol of C
for p, q being FinSequence of QuasiTerms C st len p = len (the_arity_of c) & q = b2 * p holds
b2 . (c -trm p) = c -trm q ) & ( for a being expression of C, an_Adj C holds b2 . ((non_op C) term a) = (non_op C) term (b2 . a) ) & ( for a being expression of C, an_Adj C
for t being expression of C, a_Type C holds b2 . ((ast C) term (a,t)) = (ast C) term ((b2 . a),(b2 . t)) ) holds
b1 = b2;
end;
:: for C being ConstructorSignature holds the carrier of C = 3
:: by CONSTRSIGN,YELLOW11:1;