:: SUBSTUT2 semantic presentation

theorem Th1: :: SUBSTUT2:1

for b₁ being CQC_Substitution ex b₂ being Element of CQC-Sub-WFF st
( b₂ `1 = VERUM & b₂ `2 = b₁ )

proof end;

Lemma2: for b₁ being Nat
for b₂ being QC-pred_symbol of b₁
for b₃, b₄ being Nat st b₂ is QC-pred_symbol of b₃ & b₂ is QC-pred_symbol of b₄ holds
b₃ = b₄

proof end;

theorem Th2: :: SUBSTUT2:2

for b₁ being Nat
for b₂ being QC-pred_symbol of b₁
for b₃ being CQC-variable_list of b₁
for b₄ being CQC_Substitution ex b₅ being Element of CQC-Sub-WFF st
( b₅ `1 = b₂ ! b₃ & b₅ `2 = b₄ )

proof end;

theorem Th3: :: SUBSTUT2:3

for b₁ being Nat
for b₂ being QC-pred_symbol of b₁
for b₃, b₄ being Nat st b₂ is QC-pred_symbol of b₃ & b₂ is QC-pred_symbol of b₄ holds
b₃ = b₄ by Lemma2;

theorem Th4: :: SUBSTUT2:4

for b₁ being Element of CQC-WFF st ( for b₂ being CQC_Substitution ex b₃ being Element of CQC-Sub-WFF st
( b₃ `1 = b₁ & b₃ `2 = b₂ ) ) holds
for b₂ being CQC_Substitution ex b₃ being Element of CQC-Sub-WFF st
( b₃ `1 = 'not' b₁ & b₃ `2 = b₂ )

proof end;

theorem Th5: :: SUBSTUT2:5

for b₁, b₂ being Element of CQC-WFF st ( for b₃ being CQC_Substitution ex b₄ being Element of CQC-Sub-WFF st
( b₄ `1 = b₁ & b₄ `2 = b₃ ) ) & ( for b₃ being CQC_Substitution ex b₄ being Element of CQC-Sub-WFF st
( b₄ `1 = b₂ & b₄ `2 = b₃ ) ) holds
for b₃ being CQC_Substitution ex b₄ being Element of CQC-Sub-WFF st
( b₄ `1 = b₁ '&' b₂ & b₄ `2 = b₃ )

proof end;

definition

let c₁ be Element of CQC-WFF ;
let c₂ be CQC_Substitution;
redefine func [ as [c₁,c₂] -> Element of [:QC-WFF ,vSUB :];
coherence by ZFMISC_1:def 2;

end;

theorem Th6: :: SUBSTUT2:6

for b₁ being Element of CQC-WFF
for b₂ being bound_QC-variable
for b₃ being CQC_Substitution holds dom (RestrictSub b₂,(All b₂,b₁),b₃) misses {b₂}

proof end;

theorem Th7: :: SUBSTUT2:7

for b₁ being Element of CQC-WFF
for b₂ being bound_QC-variable
for b₃ being CQC_Substitution st b₂ in rng (RestrictSub b₂,(All b₂,b₁),b₃) holds
S_Bound [(All b₂,b₁),b₃] = x. (upVar (RestrictSub b₂,(All b₂,b₁),b₃),b₁)

proof end;

theorem Th8: :: SUBSTUT2:8

for b₁ being Element of CQC-WFF
for b₂ being bound_QC-variable
for b₃ being CQC_Substitution st not b₂ in rng (RestrictSub b₂,(All b₂,b₁),b₃) holds
S_Bound [(All b₂,b₁),b₃] = b₂

proof end;

theorem Th9: :: SUBSTUT2:9

for b₁ being Element of CQC-WFF
for b₂ being bound_QC-variable
for b₃ being CQC_Substitution holds ExpandSub b₂,b₁,(RestrictSub b₂,(All b₂,b₁),b₃) = (@ (RestrictSub b₂,(All b₂,b₁),b₃)) +* (b₂ | (S_Bound [(All b₂,b₁),b₃]))

proof end;

theorem Th10: :: SUBSTUT2:10

for b₁ being Element of CQC-WFF
for b₂ being bound_QC-variable
for b₃ being CQC_Substitution
for b₄ being Element of CQC-Sub-WFF st b₄ `2 = (@ (RestrictSub b₂,(All b₂,b₁),b₃)) +* (b₂ | (S_Bound [(All b₂,b₁),b₃])) & b₄ `1 = b₁ holds
( [b₄,b₂] is quantifiable & ex b₅ being Element of CQC-Sub-WFF st b₅ = [(All b₂,b₁),b₃] )

proof end;

theorem Th11: :: SUBSTUT2:11

for b₁ being Element of CQC-WFF
for b₂ being bound_QC-variable st ( for b₃ being CQC_Substitution ex b₄ being Element of CQC-Sub-WFF st
( b₄ `1 = b₁ & b₄ `2 = b₃ ) ) holds
for b₃ being CQC_Substitution ex b₄ being Element of CQC-Sub-WFF st
( b₄ `1 = All b₂,b₁ & b₄ `2 = b₃ )

proof end;

theorem Th12: :: SUBSTUT2:12

for b₁ being Element of CQC-WFF
for b₂ being CQC_Substitution ex b₃ being Element of CQC-Sub-WFF st
( b₃ `1 = b₁ & b₃ `2 = b₂ )

proof end;

definition

let c₁ be Element of CQC-WFF ;
let c₂ be CQC_Substitution;
redefine func [ as [c₁,c₂] -> Element of CQC-Sub-WFF ;
coherence

proof end;

end;

definition

let c₁, c₂ be bound_QC-variable;
func Sbst c₁,c₂ -> CQC_Substitution equals :: SUBSTUT2:def 1
a₁ .--> a₂;
coherence

proof end;

end;

:: deftheorem Def1 defines Sbst SUBSTUT2:def 1 :

definition

let c₁ be Element of CQC-WFF ;
let c₂, c₃ be bound_QC-variable;
func c₁ . c₂,c₃ -> Element of CQC-WFF equals :: SUBSTUT2:def 2
CQC_Sub [a₁,(Sbst a₂,a₃)];
coherence ;

end;

:: deftheorem Def2 defines . SUBSTUT2:def 2 :

scheme :: SUBSTUT2:sch 1
s1{ P₁[ set ] } :

for b₁ being Element of CQC-WFF holds P₁[b₁]

provided

E13: for b₁ being Element of CQC-WFF st QuantNbr b₁ = 0 holds
P₁[b₁] and
E14: for b₁ being Nat st ( for b₂ being Element of CQC-WFF st QuantNbr b₂ = b₁ holds
P₁[b₂] ) holds
for b₂ being Element of CQC-WFF st QuantNbr b₂ = b₁ + 1 holds
P₁[b₂]

proof end;

scheme :: SUBSTUT2:sch 2
s2{ P₁[ set ] } :

for b₁ being Element of CQC-WFF holds P₁[b₁]

provided

E13: for b₁ being Element of CQC-WFF st QuantNbr b₁ <= 0 holds
P₁[b₁] and
E14: for b₁ being Nat st ( for b₂ being Element of CQC-WFF st QuantNbr b₂ <= b₁ holds
P₁[b₂] ) holds
for b₂ being Element of CQC-WFF st QuantNbr b₂ <= b₁ + 1 holds
P₁[b₂]

proof end;

theorem Th13: :: SUBSTUT2:13

for b₁, b₂ being bound_QC-variable holds VERUM . b₁,b₂ = VERUM

proof end;

theorem Th14: :: SUBSTUT2:14

for b₁ being Nat
for b₂, b₃ being bound_QC-variable
for b₄ being QC-pred_symbol of b₁
for b₅ being CQC-variable_list of b₁ holds
( (b₄ ! b₅) . b₂,b₃ = b₄ ! (CQC_Subst b₅,(Sbst b₂,b₃)) & QuantNbr (b₄ ! b₅) = QuantNbr ((b₄ ! b₅) . b₂,b₃) )

proof end;

theorem Th15: :: SUBSTUT2:15

for b₁ being Nat
for b₂ being QC-pred_symbol of b₁
for b₃ being CQC-variable_list of b₁
for b₄ being CQC_Substitution holds QuantNbr (b₂ ! b₃) = QuantNbr (CQC_Sub [(b₂ ! b₃),b₄])

proof end;

definition

let c₁ be Element of QC-Sub-WFF ;
redefine func `2 as c₁ `2 -> CQC_Substitution;
coherence

proof end;

end;

theorem Th16: :: SUBSTUT2:16

for b₁ being Element of CQC-WFF
for b₂ being CQC_Substitution holds [('not' b₁),b₂] = Sub_not [b₁,b₂]

proof end;

theorem Th17: :: SUBSTUT2:17

for b₁ being Element of CQC-WFF
for b₂, b₃ being bound_QC-variable holds
( ('not' b₁) . b₂,b₃ = 'not' (b₁ . b₂,b₃) & ( QuantNbr b₁ = QuantNbr (b₁ . b₂,b₃) implies QuantNbr ('not' b₁) = QuantNbr (('not' b₁) . b₂,b₃) ) )

proof end;

theorem Th18: :: SUBSTUT2:18

for b₁ being Element of CQC-WFF st ( for b₂ being CQC_Substitution holds QuantNbr b₁ = QuantNbr (CQC_Sub [b₁,b₂]) ) holds
for b₂ being CQC_Substitution holds QuantNbr ('not' b₁) = QuantNbr (CQC_Sub [('not' b₁),b₂])

proof end;

theorem Th19: :: SUBSTUT2:19

for b₁, b₂ being Element of CQC-WFF
for b₃ being CQC_Substitution holds [(b₁ '&' b₂),b₃] = CQCSub_& [b₁,b₃],[b₂,b₃]

proof end;

theorem Th20: :: SUBSTUT2:20

for b₁, b₂ being Element of CQC-WFF
for b₃, b₄ being bound_QC-variable holds
( (b₁ '&' b₂) . b₃,b₄ = (b₁ . b₃,b₄) '&' (b₂ . b₃,b₄) & ( QuantNbr b₁ = QuantNbr (b₁ . b₃,b₄) & QuantNbr b₂ = QuantNbr (b₂ . b₃,b₄) implies QuantNbr (b₁ '&' b₂) = QuantNbr ((b₁ '&' b₂) . b₃,b₄) ) )

proof end;

theorem Th21: :: SUBSTUT2:21

for b₁, b₂ being Element of CQC-WFF st ( for b₃ being CQC_Substitution holds QuantNbr b₁ = QuantNbr (CQC_Sub [b₁,b₃]) ) & ( for b₃ being CQC_Substitution holds QuantNbr b₂ = QuantNbr (CQC_Sub [b₂,b₃]) ) holds
for b₃ being CQC_Substitution holds QuantNbr (b₁ '&' b₂) = QuantNbr (CQC_Sub [(b₁ '&' b₂),b₃])

proof end;

definition

func CFQ -> Function of CQC-Sub-WFF , vSUB equals :: SUBSTUT2:def 3
QSub | CQC-Sub-WFF ;
coherence

proof end;

end;

:: deftheorem Def3 defines CFQ SUBSTUT2:def 3 :

definition

let c₁ be Element of CQC-WFF ;
let c₂ be bound_QC-variable;
let c₃ be CQC_Substitution;
func QScope c₁,c₂,c₃ -> CQC-WFF-like Element of [:QC-Sub-WFF ,bound_QC-variables :] equals :: SUBSTUT2:def 4
[[a₁,(CFQ . [(All a₂,a₁),a₃])],a₂];
coherence ;

end;

:: deftheorem Def4 defines QScope SUBSTUT2:def 4 :

definition

let c₁ be Element of CQC-WFF ;
let c₂ be bound_QC-variable;
let c₃ be CQC_Substitution;
func Qsc c₁,c₂,c₃ -> second_Q_comp of QScope a₁,a₂,a₃ equals :: SUBSTUT2:def 5
a₃;
coherence

proof end;

end;

:: deftheorem Def5 defines Qsc SUBSTUT2:def 5 :

theorem Th22: :: SUBSTUT2:22

for b₁ being Element of CQC-WFF
for b₂ being bound_QC-variable
for b₃ being CQC_Substitution holds
( [(All b₂,b₁),b₃] = CQCSub_All (QScope b₁,b₂,b₃),(Qsc b₁,b₂,b₃) & QScope b₁,b₂,b₃ is quantifiable )

proof end;

theorem Th23: :: SUBSTUT2:23

for b₁ being Element of CQC-WFF
for b₂ being bound_QC-variable st ( for b₃ being CQC_Substitution holds QuantNbr b₁ = QuantNbr (CQC_Sub [b₁,b₃]) ) holds
for b₃ being CQC_Substitution holds QuantNbr (All b₂,b₁) = QuantNbr (CQC_Sub [(All b₂,b₁),b₃])

proof end;

theorem Th24: :: SUBSTUT2:24

for b₁ being CQC_Substitution holds QuantNbr VERUM = QuantNbr (CQC_Sub [VERUM ,b₁])

proof end;

theorem Th25: :: SUBSTUT2:25

for b₁ being Element of CQC-WFF
for b₂ being CQC_Substitution holds QuantNbr b₁ = QuantNbr (CQC_Sub [b₁,b₂])

proof end;

theorem Th26: :: SUBSTUT2:26

for b₁ being Element of CQC-WFF st b₁ is atomic holds
ex b₂ being Natex b₃ being QC-pred_symbol of b₂ex b₄ being CQC-variable_list of b₂ st b₁ = b₃ ! b₄

proof end;

scheme :: SUBSTUT2:sch 3
s3{ P₁[ set ] } :

for b₁ being Element of CQC-WFF st QuantNbr b₁ = 0 holds
P₁[b₁]

provided

E21: for b₁, b₂ being Element of CQC-WFF
for b₃ being bound_QC-variable
for b₄ being Nat
for b₅ being CQC-variable_list of b₄
for b₆ being QC-pred_symbol of b₄ holds
( P₁[ VERUM ] & P₁[b₆ ! b₅] & ( P₁[b₁] implies P₁[ 'not' b₁] ) & ( P₁[b₁] & P₁[b₂] implies P₁[b₁ '&' b₂] ) )

proof end;

definition

let c₁, c₂ be QC-formula;
assume E21: c₁ is_subformula_of c₂ ;
mode PATH of c₁,c₂ -> FinSequence means :Def6: :: SUBSTUT2:def 6
( 1 <= len a₃ & a₃ . 1 = a₁ & a₃ . (len a₃) = a₂ & ( for b₁ being Nat st 1 <= b₁ & b₁ < len a₃ holds
ex b₂, b₃ being Element of QC-WFF st
( a₃ . b₁ = b₂ & a₃ . (b₁ + 1) = b₃ & b₂ is_immediate_constituent_of b₃ ) ) );
existence

proof end;

end;

:: deftheorem Def6 defines PATH SUBSTUT2:def 6 :

theorem Th27: :: SUBSTUT2:27

for b₁ being Nat
for b₂, b₃ being QC-formula
for b₄ being PATH of b₂,b₃ st b₂ is_subformula_of b₃ & 1 <= b₁ & b₁ <= len b₄ holds
ex b₅ being QC-formula st
( b₅ = b₄ . b₁ & b₅ is_subformula_of b₃ )

proof end;

theorem Th28: :: SUBSTUT2:28

for b₁ being Nat
for b₂ being Element of CQC-WFF
for b₃ being QC-formula
for b₄ being PATH of b₃,b₂ st b₃ is_subformula_of b₂ & 1 <= b₁ & b₁ <= len b₄ holds
b₄ . b₁ is Element of CQC-WFF

proof end;

theorem Th29: :: SUBSTUT2:29

for b₁, b₂ being Nat
for b₃, b₄ being Element of CQC-WFF
for b₅ being PATH of b₃,b₄ st QuantNbr b₄ <= b₁ & b₃ is_subformula_of b₄ & 1 <= b₂ & b₂ <= len b₅ holds
ex b₆ being Element of CQC-WFF st
( b₆ = b₅ . b₂ & QuantNbr b₆ <= b₁ )

proof end;

theorem Th30: :: SUBSTUT2:30

for b₁ being Nat
for b₂, b₃ being Element of CQC-WFF st QuantNbr b₂ = b₁ & b₃ is_subformula_of b₂ holds
QuantNbr b₃ <= b₁

proof end;

theorem Th31: :: SUBSTUT2:31

for b₁ being Nat
for b₂ being Element of CQC-WFF st ( for b₃ being Element of CQC-WFF st b₃ is_subformula_of b₂ holds
QuantNbr b₃ = b₁ ) holds
b₁ = 0

proof end;

theorem Th32: :: SUBSTUT2:32

for b₁ being Element of CQC-WFF st ( for b₂ being Element of CQC-WFF st b₂ is_subformula_of b₁ holds
for b₃ being bound_QC-variable
for b₄ being Element of CQC-WFF holds b₂ <> All b₃,b₄ ) holds
QuantNbr b₁ = 0

proof end;

theorem Th33: :: SUBSTUT2:33

for b₁ being Element of CQC-WFF st ( for b₂ being Element of CQC-WFF st b₂ is_subformula_of b₁ holds
QuantNbr b₂ <> 1 ) holds
QuantNbr b₁ = 0

proof end;

theorem Th34: :: SUBSTUT2:34

for b₁ being Element of CQC-WFF st 1 <= QuantNbr b₁ holds
ex b₂ being Element of CQC-WFF st
( b₂ is_subformula_of b₁ & QuantNbr b₂ = 1 ) by Th33;