:: Substitution in First-Order Formulas -- Part II. {T}he Construction ofFirst-Order Formulas
:: by Patrick Braselmann and Peter Koepke
::
:: Received September 25, 2004
:: Copyright (c) 2004 Association of Mizar Users
theorem Th1: :: SUBSTUT2:1
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: :: SUBSTUT2:2
theorem :: SUBSTUT2:3
theorem Th4: :: SUBSTUT2:4
theorem Th5: :: SUBSTUT2:5
theorem Th6: :: SUBSTUT2:6
theorem Th7: :: SUBSTUT2:7
theorem Th8: :: SUBSTUT2:8
theorem Th9: :: SUBSTUT2:9
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: :: SUBSTUT2:10
theorem Th11: :: SUBSTUT2:11
theorem Th12: :: SUBSTUT2:12
:: deftheorem SUBSTUT2:def 1 :
canceled;
:: deftheorem defines . SUBSTUT2:def 2 :
theorem :: SUBSTUT2:13
theorem :: SUBSTUT2:14
theorem Th15: :: SUBSTUT2:15
theorem Th16: :: SUBSTUT2:16
theorem :: SUBSTUT2:17
theorem Th18: :: SUBSTUT2:18
theorem Th19: :: SUBSTUT2:19
theorem :: SUBSTUT2:20
theorem Th21: :: SUBSTUT2:21
:: 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 :: SUBSTUT2:def 4
[[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: :: SUBSTUT2:22
theorem Th23: :: SUBSTUT2:23
theorem Th24: :: SUBSTUT2:24
theorem :: SUBSTUT2:25
theorem :: SUBSTUT2:26
:: deftheorem Def6 defines PATH SUBSTUT2:def 6 :
theorem :: SUBSTUT2:27
theorem Th28: :: SUBSTUT2:28
theorem Th29: :: SUBSTUT2:29
theorem :: SUBSTUT2:30
theorem :: SUBSTUT2:31
theorem :: SUBSTUT2:32
theorem Th33: :: SUBSTUT2:33
theorem :: SUBSTUT2:34