environ
vocabularies HIDDEN, NUMBERS, XBOOLE_0, SUBSET_1, ZFMISC_1, TARSKI, XXREAL_0, MARGREL1, MCART_1, ARYTM_3, NAT_1, FINSEQ_1, RELAT_1, ORDINAL4, CARD_1, REALSET1, XBOOLEAN, BVFUNC_2, ZF_LANG, CLASSES2, FUNCT_1, FUNCOP_1, RCOMP_1, QC_LANG1, WELLORD1, RELAT_2, MEMBER_1;
notations HIDDEN, TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, XTUPLE_0, SUBSET_1, CARD_1, ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0, MCART_1, RELAT_1, FUNCT_1, RELSET_1, NAT_1, FUNCT_2, FUNCOP_1, FINSEQ_1, WELLORD1, WELLORD2, RELAT_2;
definitions TARSKI, XBOOLE_0, CARD_1;
theorems ZFMISC_1, SUBSET_1, TARSKI, FINSEQ_1, MCART_1, NAT_1, FUNCT_1, FUNCT_2, RELSET_1, XBOOLE_0, XBOOLE_1, FUNCOP_1, XXREAL_0, ORDINAL1, CARD_1, RELAT_1, WELLORD1, WELLORD2, RELAT_2, ORDERS_1;
schemes NAT_1, FUNCT_2, CLASSES1, XBOOLE_0;
registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, XREAL_0, FINSEQ_1, CARD_1, XTUPLE_0, NAT_1;
constructors HIDDEN, ENUMSET1, FUNCOP_1, XXREAL_0, XREAL_0, NAT_1, FINSEQ_1, RELSET_1, WELLORD1, WELLORD2, RELAT_2, XTUPLE_0, NUMBERS;
requirements HIDDEN, NUMERALS, REAL, SUBSET, BOOLE, ARITHM;
equalities FINSEQ_1;
expansions TARSKI, XBOOLE_0, FINSEQ_1;
Lm1:
for A being QC-alphabet holds
( [:{4},(QC-symbols A):] c= QC-variables A & [:{5},(QC-symbols A):] c= QC-variables A & [:{6},NAT:] c= QC-variables A )
definition
let A be
QC-alphabet ;
let D be
set ;
attr D is
A -closed means :
Def10:
(
D is
Subset of
([:NAT,(QC-symbols A):] *) & ( for
k being
Nat for
p being
QC-pred_symbol of
k,
A for
ll being
QC-variable_list of
k,
A holds
<*p*> ^ ll in D ) &
<*[0,0]*> in D & ( for
p being
FinSequence of
[:NAT,(QC-symbols A):] st
p in D holds
<*[1,0]*> ^ p in D ) & ( for
p,
q being
FinSequence of
[:NAT,(QC-symbols A):] st
p in D &
q in D holds
(<*[2,0]*> ^ p) ^ q in D ) & ( for
x being
bound_QC-variable of
A for
p being
FinSequence of
[:NAT,(QC-symbols A):] st
p in D holds
(<*[3,0]*> ^ <*x*>) ^ p in D ) );
end;
::
deftheorem Def10 defines
-closed QC_LANG1:def 10 :
for A being QC-alphabet
for D being set holds
( D is A -closed iff ( D is Subset of ([:NAT,(QC-symbols A):] *) & ( for k being Nat
for p being QC-pred_symbol of k,A
for ll being QC-variable_list of k,A holds <*p*> ^ ll in D ) & <*[0,0]*> in D & ( for p being FinSequence of [:NAT,(QC-symbols A):] st p in D holds
<*[1,0]*> ^ p in D ) & ( for p, q being FinSequence of [:NAT,(QC-symbols A):] st p in D & q in D holds
(<*[2,0]*> ^ p) ^ q in D ) & ( for x being bound_QC-variable of A
for p being FinSequence of [:NAT,(QC-symbols A):] st p in D holds
(<*[3,0]*> ^ <*x*>) ^ p in D ) ) );
Lm2:
for A being QC-alphabet
for k being Nat
for x being QC-symbol of A holds <*[k,x]*> is FinSequence of [:NAT,(QC-symbols A):]
Lm3:
for A being QC-alphabet
for k being Nat
for p being QC-pred_symbol of k,A
for ll being QC-variable_list of k,A holds <*p*> ^ ll is FinSequence of [:NAT,(QC-symbols A):]
Lm4:
for A being QC-alphabet
for x being bound_QC-variable of A
for p being FinSequence of [:NAT,(QC-symbols A):] holds (<*[3,0]*> ^ <*x*>) ^ p is FinSequence of [:NAT,(QC-symbols A):]
Lm5:
for A being QC-alphabet holds QC-WFF A is Subset of ([:NAT,(QC-symbols A):] *)