begin
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
Element of
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 Element of 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 Element of 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 Element of 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):] *)