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 :
theorem
theorem
theorem Th15:
theorem Th16:
theorem
theorem Th18:
theorem Th19:
theorem
theorem Th21:
:: deftheorem defines CFQ SUBSTUT2:def 3 :
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 :
:: deftheorem defines Qsc SUBSTUT2:def 5 :
theorem Th22:
theorem Th23:
theorem Th24:
theorem
theorem
begin
:: deftheorem Def6 defines PATH SUBSTUT2:def 6 :
theorem
theorem Th28:
theorem Th29:
theorem
theorem
theorem
theorem Th33:
theorem