begin
theorem Th1:
Lm1:
for k being Element of NAT
for P being QC-pred_symbol of k
for k, l being Element of NAT st P is QC-pred_symbol of k & P is QC-pred_symbol of l holds
k = l
theorem Th2:
theorem
theorem Th4:
theorem Th5:
theorem Th6:
theorem Th7:
theorem Th8:
theorem Th9:
for
p being
Element of
CQC-WFF for
x being
bound_QC-variable for
Sub being
CQC_Substitution holds
ExpandSub x,
p,
(RestrictSub x,(All x,p),Sub) = (@ (RestrictSub x,(All x,p),Sub)) +* (x | (S_Bound [(All x,p),Sub]))
theorem Th10:
theorem Th11:
theorem Th12:
begin
:: deftheorem SUBSTUT2:def 1 :
canceled;
:: deftheorem defines . SUBSTUT2:def 2 :
for p being Element of CQC-WFF
for x, y being bound_QC-variable holds p . x,y = CQC_Sub [p,(Sbst x,y)];
theorem
theorem
theorem Th15:
theorem Th16:
theorem
theorem Th18:
theorem Th19:
theorem
theorem Th21:
:: deftheorem defines CFQ SUBSTUT2:def 3 :
CFQ = QSub | CQC-Sub-WFF ;
definition
let p be
Element of
CQC-WFF ;
let x be
bound_QC-variable;
let Sub be
CQC_Substitution;
func QScope p,
x,
Sub -> CQC-WFF-like Element of
[:QC-Sub-WFF ,bound_QC-variables :] equals
[[p,(CFQ . [(All x,p),Sub])],x];
coherence
[[p,(CFQ . [(All x,p),Sub])],x] is CQC-WFF-like Element of [:QC-Sub-WFF ,bound_QC-variables :]
;
end;
:: deftheorem defines QScope SUBSTUT2:def 4 :
for p being Element of CQC-WFF
for x being bound_QC-variable
for Sub being CQC_Substitution holds QScope p,x,Sub = [[p,(CFQ . [(All x,p),Sub])],x];
:: deftheorem defines Qsc SUBSTUT2:def 5 :
for p being Element of CQC-WFF
for x being bound_QC-variable
for Sub being CQC_Substitution holds Qsc p,x,Sub = Sub;
theorem Th22:
theorem Th23:
theorem Th24:
theorem
theorem
begin
:: deftheorem Def6 defines PATH SUBSTUT2:def 6 :
for G, H being QC-formula st G is_subformula_of H holds
for b3 being FinSequence holds
( b3 is PATH of G,H iff ( 1 <= len b3 & b3 . 1 = G & b3 . (len b3) = H & ( for k being Element of NAT st 1 <= k & k < len b3 holds
ex G1, H1 being Element of QC-WFF st
( b3 . k = G1 & b3 . (k + 1) = H1 & G1 is_immediate_constituent_of H1 ) ) ) );
theorem
theorem Th28:
theorem Th29:
theorem
theorem
theorem
theorem Th33:
theorem