begin
:: deftheorem defines vSUB SUBSTUT1:def 1 :
:: deftheorem defines @ SUBSTUT1:def 2 :
theorem Th1:
:: deftheorem Def3 defines CQC_Subst SUBSTUT1:def 3 :
:: deftheorem defines @ SUBSTUT1:def 4 :
:: deftheorem defines CQC_Subst SUBSTUT1:def 5 :
:: deftheorem defines RestrictSub SUBSTUT1:def 6 :
:: deftheorem defines Bound_Vars SUBSTUT1:def 7 :
:: deftheorem Def8 defines Bound_Vars SUBSTUT1:def 8 :
Lm1:
for p being QC-formula holds
( Bound_Vars VERUM = {} bound_QC-variables & ( p is atomic implies Bound_Vars p = Bound_Vars (the_arguments_of p) ) & ( p is negative implies Bound_Vars p = Bound_Vars (the_argument_of p) ) & ( p is conjunctive implies Bound_Vars p = (Bound_Vars (the_left_argument_of p)) \/ (Bound_Vars (the_right_argument_of p)) ) & ( p is universal implies Bound_Vars p = (Bound_Vars (the_scope_of p)) \/ {(bound_in p)} ) )
theorem
theorem
theorem
theorem
theorem
:: deftheorem defines Dom_Bound_Vars SUBSTUT1:def 9 :
:: deftheorem defines Sub_Var SUBSTUT1:def 10 :
:: deftheorem defines NSub SUBSTUT1:def 11 :
:: deftheorem defines upVar SUBSTUT1:def 12 :
definition
let x be
bound_QC-variable;
let p be
QC-formula;
let finSub be
finite CQC_Substitution;
assume A1:
ex
Sub being
CQC_Substitution st
finSub = RestrictSub x,
(All x,p),
Sub
;
func ExpandSub x,
p,
finSub -> CQC_Substitution equals
finSub \/ {[x,(x. (upVar finSub,p))]} if x in rng finSub otherwise finSub \/ {[x,x]};
coherence
( ( x in rng finSub implies finSub \/ {[x,(x. (upVar finSub,p))]} is CQC_Substitution ) & ( not x in rng finSub implies finSub \/ {[x,x]} is CQC_Substitution ) )
consistency
for b1 being CQC_Substitution holds verum
;
end;
:: deftheorem defines ExpandSub SUBSTUT1:def 13 :
for
x being
bound_QC-variable for
p being
QC-formula for
finSub being
finite CQC_Substitution st ex
Sub being
CQC_Substitution st
finSub = RestrictSub x,
(All x,p),
Sub holds
( (
x in rng finSub implies
ExpandSub x,
p,
finSub = finSub \/ {[x,(x. (upVar finSub,p))]} ) & ( not
x in rng finSub implies
ExpandSub x,
p,
finSub = finSub \/ {[x,x]} ) );
:: deftheorem Def14 defines PQSub SUBSTUT1:def 14 :
definition
func QSub -> Function means
for
a being
set holds
(
a in it iff ex
p being
QC-formula ex
Sub being
CQC_Substitution ex
b being
set st
(
a = [[p,Sub],b] &
p,
Sub PQSub b ) );
existence
ex b1 being Function st
for a being set holds
( a in b1 iff ex p being QC-formula ex Sub being CQC_Substitution ex b being set st
( a = [[p,Sub],b] & p,Sub PQSub b ) )
uniqueness
for b1, b2 being Function st ( for a being set holds
( a in b1 iff ex p being QC-formula ex Sub being CQC_Substitution ex b being set st
( a = [[p,Sub],b] & p,Sub PQSub b ) ) ) & ( for a being set holds
( a in b2 iff ex p being QC-formula ex Sub being CQC_Substitution ex b being set st
( a = [[p,Sub],b] & p,Sub PQSub b ) ) ) holds
b1 = b2
end;
:: deftheorem defines QSub SUBSTUT1:def 15 :
begin
theorem Th7:
(
[:QC-WFF ,vSUB :] is
Subset of
[:([:NAT ,NAT :] * ),vSUB :] & ( for
k being
Element of
NAT for
p being
QC-pred_symbol of
k for
ll being
QC-variable_list of
k for
e being
Element of
vSUB holds
[(<*p*> ^ ll),e] in [:QC-WFF ,vSUB :] ) & ( for
e being
Element of
vSUB holds
[<*[0 ,0 ]*>,e] in [:QC-WFF ,vSUB :] ) & ( for
p being
FinSequence of
[:NAT ,NAT :] for
e being
Element of
vSUB st
[p,e] in [:QC-WFF ,vSUB :] holds
[(<*[1,0 ]*> ^ p),e] in [:QC-WFF ,vSUB :] ) & ( for
p,
q being
FinSequence of
[:NAT ,NAT :] for
e being
Element of
vSUB st
[p,e] in [:QC-WFF ,vSUB :] &
[q,e] in [:QC-WFF ,vSUB :] holds
[((<*[2,0 ]*> ^ p) ^ q),e] in [:QC-WFF ,vSUB :] ) & ( for
x being
bound_QC-variable for
p being
FinSequence of
[:NAT ,NAT :] for
e being
Element of
vSUB st
[p,(QSub . [((<*[3,0 ]*> ^ <*x*>) ^ p),e])] in [:QC-WFF ,vSUB :] holds
[((<*[3,0 ]*> ^ <*x*>) ^ p),e] in [:QC-WFF ,vSUB :] ) )
definition
let IT be
set ;
attr IT is
QC-Sub-closed means :
Def16:
(
IT is
Subset of
[:([:NAT ,NAT :] * ),vSUB :] & ( for
k being
Element of
NAT for
p being
QC-pred_symbol of
k for
ll being
QC-variable_list of
k for
e being
Element of
vSUB holds
[(<*p*> ^ ll),e] in IT ) & ( for
e being
Element of
vSUB holds
[<*[0 ,0 ]*>,e] in IT ) & ( for
p being
FinSequence of
[:NAT ,NAT :] for
e being
Element of
vSUB st
[p,e] in IT holds
[(<*[1,0 ]*> ^ p),e] in IT ) & ( for
p,
q being
FinSequence of
[:NAT ,NAT :] for
e being
Element of
vSUB st
[p,e] in IT &
[q,e] in IT holds
[((<*[2,0 ]*> ^ p) ^ q),e] in IT ) & ( for
x being
bound_QC-variable for
p being
FinSequence of
[:NAT ,NAT :] for
e being
Element of
vSUB st
[p,(QSub . [((<*[3,0 ]*> ^ <*x*>) ^ p),e])] in IT holds
[((<*[3,0 ]*> ^ <*x*>) ^ p),e] in IT ) );
end;
:: deftheorem Def16 defines QC-Sub-closed SUBSTUT1:def 16 :
for
IT being
set holds
(
IT is
QC-Sub-closed iff (
IT is
Subset of
[:([:NAT ,NAT :] * ),vSUB :] & ( for
k being
Element of
NAT for
p being
QC-pred_symbol of
k for
ll being
QC-variable_list of
k for
e being
Element of
vSUB holds
[(<*p*> ^ ll),e] in IT ) & ( for
e being
Element of
vSUB holds
[<*[0 ,0 ]*>,e] in IT ) & ( for
p being
FinSequence of
[:NAT ,NAT :] for
e being
Element of
vSUB st
[p,e] in IT holds
[(<*[1,0 ]*> ^ p),e] in IT ) & ( for
p,
q being
FinSequence of
[:NAT ,NAT :] for
e being
Element of
vSUB st
[p,e] in IT &
[q,e] in IT holds
[((<*[2,0 ]*> ^ p) ^ q),e] in IT ) & ( for
x being
bound_QC-variable for
p being
FinSequence of
[:NAT ,NAT :] for
e being
Element of
vSUB st
[p,(QSub . [((<*[3,0 ]*> ^ <*x*>) ^ p),e])] in IT holds
[((<*[3,0 ]*> ^ <*x*>) ^ p),e] in IT ) ) );
Lm2:
for x being bound_QC-variable
for p being FinSequence of [:NAT ,NAT :] holds (<*[3,0 ]*> ^ <*x*>) ^ p is FinSequence of [:NAT ,NAT :]
Lm3:
for k, l being Element of NAT
for e being Element of vSUB holds [<*[k,l]*>,e] in [:([:NAT ,NAT :] * ),vSUB :]
Lm4:
for k being Element of NAT
for p being QC-pred_symbol of k
for ll being QC-variable_list of k
for e being Element of vSUB holds [(<*p*> ^ ll),e] in [:([:NAT ,NAT :] * ),vSUB :]
:: deftheorem Def17 defines QC-Sub-WFF SUBSTUT1:def 17 :
theorem Th8:
:: deftheorem Def18 defines Sub_P SUBSTUT1:def 18 :
theorem Th9:
:: deftheorem Def19 defines Sub_VERUM SUBSTUT1:def 19 :
theorem Th10:
:: deftheorem defines Sub_not SUBSTUT1:def 20 :
:: deftheorem Def21 defines Sub_& SUBSTUT1:def 21 :
:: deftheorem Def22 defines quantifiable SUBSTUT1:def 22 :
:: deftheorem Def23 defines second_Q_comp SUBSTUT1:def 23 :
:: deftheorem Def24 defines Sub_All SUBSTUT1:def 24 :
:: deftheorem Def25 defines Sub_atomic SUBSTUT1:def 25 :
theorem Th11:
:: deftheorem Def26 defines Sub_negative SUBSTUT1:def 26 :
:: deftheorem Def27 defines Sub_conjunctive SUBSTUT1:def 27 :
:: deftheorem Def28 defines Sub_universal SUBSTUT1:def 28 :
theorem Th12:
:: deftheorem Def29 defines Sub_the_arguments_of SUBSTUT1:def 29 :
:: deftheorem Def30 defines Sub_the_argument_of SUBSTUT1:def 30 :
:: deftheorem Def31 defines Sub_the_left_argument_of SUBSTUT1:def 31 :
:: deftheorem Def32 defines Sub_the_right_argument_of SUBSTUT1:def 32 :
:: deftheorem defines Sub_the_bound_of SUBSTUT1:def 33 :
:: deftheorem Def34 defines Sub_the_scope_of SUBSTUT1:def 34 :
theorem Th13:
theorem Th14:
theorem
theorem
theorem
theorem Th18:
theorem Th19:
theorem
theorem Th21:
theorem Th22:
theorem Th23:
theorem Th24:
theorem Th25:
theorem Th26:
theorem Th27:
scheme
SubQCFuncUniq{
F1()
-> non
empty set ,
F2()
-> Function of
QC-Sub-WFF ,
F1(),
F3()
-> Function of
QC-Sub-WFF ,
F1(),
F4()
-> Element of
F1(),
F5(
set )
-> Element of
F1(),
F6(
set )
-> Element of
F1(),
F7(
set ,
set )
-> Element of
F1(),
F8(
set ,
set )
-> Element of
F1() } :
provided
:: deftheorem defines @ SUBSTUT1:def 35 :
definition
let Z be
Element of
[:QC-WFF ,vSUB :];
func S_Bound Z -> bound_QC-variable equals
x. (upVar (RestrictSub (bound_in (Z `1 )),(Z `1 ),(Z `2 )),(the_scope_of (Z `1 ))) if bound_in (Z `1 ) in rng (RestrictSub (bound_in (Z `1 )),(Z `1 ),(Z `2 )) otherwise bound_in (Z `1 );
coherence
( ( bound_in (Z `1 ) in rng (RestrictSub (bound_in (Z `1 )),(Z `1 ),(Z `2 )) implies x. (upVar (RestrictSub (bound_in (Z `1 )),(Z `1 ),(Z `2 )),(the_scope_of (Z `1 ))) is bound_QC-variable ) & ( not bound_in (Z `1 ) in rng (RestrictSub (bound_in (Z `1 )),(Z `1 ),(Z `2 )) implies bound_in (Z `1 ) is bound_QC-variable ) )
;
consistency
for b1 being bound_QC-variable holds verum
;
end;
:: deftheorem defines S_Bound SUBSTUT1:def 36 :
:: deftheorem defines Quant SUBSTUT1:def 37 :
Lm5:
for F1, F2 being Function of QC-Sub-WFF ,QC-WFF st ( for S being Element of QC-Sub-WFF holds
( ( S is Sub_VERUM implies F1 . S = VERUM ) & ( S is Sub_atomic implies F1 . S = (the_pred_symbol_of (S `1 )) ! (CQC_Subst (Sub_the_arguments_of S),(S `2 )) ) & ( S is Sub_negative implies F1 . S = 'not' (F1 . (Sub_the_argument_of S)) ) & ( S is Sub_conjunctive implies F1 . S = (F1 . (Sub_the_left_argument_of S)) '&' (F1 . (Sub_the_right_argument_of S)) ) & ( S is Sub_universal implies F1 . S = Quant S,(F1 . (Sub_the_scope_of S)) ) ) ) & ( for S being Element of QC-Sub-WFF holds
( ( S is Sub_VERUM implies F2 . S = VERUM ) & ( S is Sub_atomic implies F2 . S = (the_pred_symbol_of (S `1 )) ! (CQC_Subst (Sub_the_arguments_of S),(S `2 )) ) & ( S is Sub_negative implies F2 . S = 'not' (F2 . (Sub_the_argument_of S)) ) & ( S is Sub_conjunctive implies F2 . S = (F2 . (Sub_the_left_argument_of S)) '&' (F2 . (Sub_the_right_argument_of S)) ) & ( S is Sub_universal implies F2 . S = Quant S,(F2 . (Sub_the_scope_of S)) ) ) ) holds
F1 = F2
begin
definition
let S be
Element of
QC-Sub-WFF ;
func CQC_Sub S -> Element of
QC-WFF means :
Def38:
ex
F being
Function of
QC-Sub-WFF ,
QC-WFF st
(
it = F . S & ( for
S9 being
Element of
QC-Sub-WFF holds
( (
S9 is
Sub_VERUM implies
F . S9 = VERUM ) & (
S9 is
Sub_atomic implies
F . S9 = (the_pred_symbol_of (S9 `1 )) ! (CQC_Subst (Sub_the_arguments_of S9),(S9 `2 )) ) & (
S9 is
Sub_negative implies
F . S9 = 'not' (F . (Sub_the_argument_of S9)) ) & (
S9 is
Sub_conjunctive implies
F . S9 = (F . (Sub_the_left_argument_of S9)) '&' (F . (Sub_the_right_argument_of S9)) ) & (
S9 is
Sub_universal implies
F . S9 = Quant S9,
(F . (Sub_the_scope_of S9)) ) ) ) );
existence
ex b1 being Element of QC-WFF ex F being Function of QC-Sub-WFF ,QC-WFF st
( b1 = F . S & ( for S9 being Element of QC-Sub-WFF holds
( ( S9 is Sub_VERUM implies F . S9 = VERUM ) & ( S9 is Sub_atomic implies F . S9 = (the_pred_symbol_of (S9 `1 )) ! (CQC_Subst (Sub_the_arguments_of S9),(S9 `2 )) ) & ( S9 is Sub_negative implies F . S9 = 'not' (F . (Sub_the_argument_of S9)) ) & ( S9 is Sub_conjunctive implies F . S9 = (F . (Sub_the_left_argument_of S9)) '&' (F . (Sub_the_right_argument_of S9)) ) & ( S9 is Sub_universal implies F . S9 = Quant S9,(F . (Sub_the_scope_of S9)) ) ) ) )
uniqueness
for b1, b2 being Element of QC-WFF st ex F being Function of QC-Sub-WFF ,QC-WFF st
( b1 = F . S & ( for S9 being Element of QC-Sub-WFF holds
( ( S9 is Sub_VERUM implies F . S9 = VERUM ) & ( S9 is Sub_atomic implies F . S9 = (the_pred_symbol_of (S9 `1 )) ! (CQC_Subst (Sub_the_arguments_of S9),(S9 `2 )) ) & ( S9 is Sub_negative implies F . S9 = 'not' (F . (Sub_the_argument_of S9)) ) & ( S9 is Sub_conjunctive implies F . S9 = (F . (Sub_the_left_argument_of S9)) '&' (F . (Sub_the_right_argument_of S9)) ) & ( S9 is Sub_universal implies F . S9 = Quant S9,(F . (Sub_the_scope_of S9)) ) ) ) ) & ex F being Function of QC-Sub-WFF ,QC-WFF st
( b2 = F . S & ( for S9 being Element of QC-Sub-WFF holds
( ( S9 is Sub_VERUM implies F . S9 = VERUM ) & ( S9 is Sub_atomic implies F . S9 = (the_pred_symbol_of (S9 `1 )) ! (CQC_Subst (Sub_the_arguments_of S9),(S9 `2 )) ) & ( S9 is Sub_negative implies F . S9 = 'not' (F . (Sub_the_argument_of S9)) ) & ( S9 is Sub_conjunctive implies F . S9 = (F . (Sub_the_left_argument_of S9)) '&' (F . (Sub_the_right_argument_of S9)) ) & ( S9 is Sub_universal implies F . S9 = Quant S9,(F . (Sub_the_scope_of S9)) ) ) ) ) holds
b1 = b2
by Lm5;
end;
:: deftheorem Def38 defines CQC_Sub SUBSTUT1:def 38 :
theorem Th28:
theorem Th29:
theorem Th30:
theorem Th31:
theorem Th32:
:: deftheorem defines CQC-Sub-WFF SUBSTUT1:def 39 :
theorem Th33:
Lm6:
for k being Element of NAT
for P being QC-pred_symbol of k
for ll being CQC-variable_list of k holds the_pred_symbol_of (P ! ll) = P
theorem Th34:
theorem Th35:
theorem Th36:
theorem Th37:
theorem Th38: