:: SUBSTUT1 semantic presentation

definition

func vSUB -> set equals :: SUBSTUT1:def 1
PFuncs bound_QC-variables ,bound_QC-variables ;
coherence ;

end;

:: deftheorem Def1 defines vSUB SUBSTUT1:def 1 :

registration

cluster vSUB -> non empty ;
coherence ;

end;

definition

mode CQC_Substitution is Element of vSUB ;

end;

registration

cluster vSUB -> non empty functional ;
coherence ;

end;

definition

let c₁ be CQC_Substitution;
func @ c₁ -> PartFunc of bound_QC-variables , bound_QC-variables equals :: SUBSTUT1:def 2
a₁;
coherence by PARTFUN1:121;

end;

:: deftheorem Def2 defines @ SUBSTUT1:def 2 :

theorem Th1: :: SUBSTUT1:1

for b₁ being set
for b₂ being CQC_Substitution st b₁ in dom b₂ holds
b₂ . b₁ in bound_QC-variables

proof end;

definition

let c₁ be FinSequence of QC-variables ;
let c₂ be CQC_Substitution;
func CQC_Subst c₁,c₂ -> FinSequence of QC-variables means :Def3: :: SUBSTUT1:def 3
( len a₃ = len a₁ & ( for b₁ being Nat st 1 <= b₁ & b₁ <= len a₁ holds
( ( a₁ . b₁ in dom a₂ implies a₃ . b₁ = a₂ . (a₁ . b₁) ) & ( not a₁ . b₁ in dom a₂ implies a₃ . b₁ = a₁ . b₁ ) ) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def3 defines CQC_Subst SUBSTUT1:def 3 :

definition

let c₁ be FinSequence of bound_QC-variables ;
func @ c₁ -> FinSequence of QC-variables equals :: SUBSTUT1:def 4
a₁;
coherence

proof end;

end;

:: deftheorem Def4 defines @ SUBSTUT1:def 4 :

definition

let c₁ be FinSequence of bound_QC-variables ;
let c₂ be CQC_Substitution;
func CQC_Subst c₁,c₂ -> FinSequence of bound_QC-variables equals :: SUBSTUT1:def 5
CQC_Subst (@ a₁),a₂;
coherence

proof end;

end;

:: deftheorem Def5 defines CQC_Subst SUBSTUT1:def 5 :

definition

let c₁ be CQC_Substitution;
let c₂ be set ;
redefine func | as c₁ | c₂ -> CQC_Substitution;
coherence

proof end;

end;

registration

cluster finite Element of vSUB ;
existence

proof end;

end;

definition

let c₁ be bound_QC-variable;
let c₂ be QC-formula;
let c₃ be CQC_Substitution;
func RestrictSub c₁,c₂,c₃ -> finite CQC_Substitution equals :: SUBSTUT1:def 6
a₃ | { b₁ where B is bound_QC-variable : ( b₁ in still_not-bound_in a₂ & b₁ is Element of dom a₃ & b₁ <> a₁ & b₁ <> a₃ . b₁ ) } ;
coherence

proof end;

end;

:: deftheorem Def6 defines RestrictSub SUBSTUT1:def 6 :

definition

let c₁ be FinSequence of QC-variables ;
func Bound_Vars c₁ -> Subset of bound_QC-variables equals :: SUBSTUT1:def 7
{ (a₁ . b₁) where B is Nat : ( 1 <= b₁ & b₁ <= len a₁ & a₁ . b₁ in bound_QC-variables ) } ;
coherence

proof end;

end;

:: deftheorem Def7 defines Bound_Vars SUBSTUT1:def 7 :

definition

let c₁ be QC-formula;
func Bound_Vars c₁ -> Subset of bound_QC-variables means :Def8: :: SUBSTUT1:def 8
ex b₁ being Function of QC-WFF , bool bound_QC-variables st
( a₂ = b₁ . a₁ & ( for b₂ being Element of QC-WFF
for b₃, b₄ being Subset of bound_QC-variables holds
( ( b₂ = VERUM implies b₁ . b₂ = {} bound_QC-variables ) & ( b₂ is atomic implies b₁ . b₂ = Bound_Vars (the_arguments_of b₂) ) & ( b₂ is negative & b₃ = b₁ . (the_argument_of b₂) implies b₁ . b₂ = b₃ ) & ( b₂ is conjunctive & b₃ = b₁ . (the_left_argument_of b₂) & b₄ = b₁ . (the_right_argument_of b₂) implies b₁ . b₂ = b₃ \/ b₄ ) & ( b₂ is universal & b₃ = b₁ . (the_scope_of b₂) implies b₁ . b₂ = b₃ \/ {(bound_in b₂)} ) ) ) );
correctness

proof end;

end;

:: deftheorem Def8 defines Bound_Vars SUBSTUT1:def 8 :

Lemma4: for b₁ being QC-formula holds
( Bound_Vars VERUM = {} bound_QC-variables & ( b₁ is atomic implies Bound_Vars b₁ = Bound_Vars (the_arguments_of b₁) ) & ( b₁ is negative implies Bound_Vars b₁ = Bound_Vars (the_argument_of b₁) ) & ( b₁ is conjunctive implies Bound_Vars b₁ = (Bound_Vars (the_left_argument_of b₁)) \/ (Bound_Vars (the_right_argument_of b₁)) ) & ( b₁ is universal implies Bound_Vars b₁ = (Bound_Vars (the_scope_of b₁)) \/ {(bound_in b₁)} ) )

proof end;

theorem Th2: :: SUBSTUT1:2

Bound_Vars VERUM = {} by Lemma4;

theorem Th3: :: SUBSTUT1:3

for b₁ being QC-formula st b₁ is atomic holds
Bound_Vars b₁ = Bound_Vars (the_arguments_of b₁) by Lemma4;

theorem Th4: :: SUBSTUT1:4

for b₁ being QC-formula st b₁ is negative holds
Bound_Vars b₁ = Bound_Vars (the_argument_of b₁) by Lemma4;

theorem Th5: :: SUBSTUT1:5

for b₁ being QC-formula st b₁ is conjunctive holds
Bound_Vars b₁ = (Bound_Vars (the_left_argument_of b₁)) \/ (Bound_Vars (the_right_argument_of b₁)) by Lemma4;

theorem Th6: :: SUBSTUT1:6

for b₁ being QC-formula st b₁ is universal holds
Bound_Vars b₁ = (Bound_Vars (the_scope_of b₁)) \/ {(bound_in b₁)} by Lemma4;

registration

let c₁ be QC-formula;
cluster Bound_Vars a₁ -> finite ;
coherence

proof end;

end;

definition

let c₁ be QC-formula;
func Dom_Bound_Vars c₁ -> finite Subset of NAT equals :: SUBSTUT1:def 9
{ b₁ where B is Nat : x. b₁ in Bound_Vars a₁ } ;
coherence

proof end;

end;

:: deftheorem Def9 defines Dom_Bound_Vars SUBSTUT1:def 9 :

definition

let c₁ be finite CQC_Substitution;
func Sub_Var c₁ -> finite Subset of NAT equals :: SUBSTUT1:def 10
{ b₁ where B is Nat : x. b₁ in rng a₁ } ;
coherence

proof end;

end;

:: deftheorem Def10 defines Sub_Var SUBSTUT1:def 10 :

definition

let c₁ be QC-formula;
let c₂ be finite CQC_Substitution;
func NSub c₁,c₂ -> non empty Subset of NAT equals :: SUBSTUT1:def 11
NAT \ ((Dom_Bound_Vars a₁) \/ (Sub_Var a₂));
coherence

proof end;

end;

:: deftheorem Def11 defines NSub SUBSTUT1:def 11 :

definition

let c₁ be finite CQC_Substitution;
let c₂ be QC-formula;
func upVar c₁,c₂ -> Nat equals :: SUBSTUT1:def 12
min (NSub a₂,a₁);
coherence ;

end;

:: deftheorem Def12 defines upVar SUBSTUT1:def 12 :

definition

let c₁ be bound_QC-variable;
let c₂ be QC-formula;
let c₃ be finite CQC_Substitution;
assume E5: ex b₁ being CQC_Substitution st c₃ = RestrictSub c₁,(All c₁,c₂),b₁ ;
func ExpandSub c₁,c₂,c₃ -> CQC_Substitution equals :: SUBSTUT1:def 13
a₃ \/ {[a₁,(x. (upVar a₃,a₂))]} if a₁ in rng a₃
otherwise a₃ \/ {[a₁,a₁]};
coherence

proof end;

consistency ;

end;

:: deftheorem Def13 defines ExpandSub SUBSTUT1:def 13 :

definition

let c₁ be QC-formula;
let c₂ be CQC_Substitution;
let c₃ be set ;
pred c₁,c₂ PQSub c₃ means :Def14: :: SUBSTUT1:def 14
( ( a₁ is universal implies a₃ = ExpandSub (bound_in a₁),(the_scope_of a₁),(RestrictSub (bound_in a₁),a₁,a₂) ) & ( not a₁ is universal implies a₃ = {} ) );

end;

:: deftheorem Def14 defines PQSub SUBSTUT1:def 14 :

definition

func QSub -> Function means :: SUBSTUT1:def 15
for b₁ being set holds
( b₁ in a₁ iff ex b₂ being QC-formulaex b₃ being CQC_Substitutionex b₄ being set st
( b₁ = [[b₂,b₃],b₄] & b₂,b₃ PQSub b₄ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def15 defines QSub SUBSTUT1:def 15 :

theorem Th7: :: SUBSTUT1:7

( [:QC-WFF ,vSUB :] is Subset of [:([:NAT ,NAT :] * ),vSUB :] & ( for b₁ being Nat
for b₂ being QC-pred_symbol of b₁
for b₃ being QC-variable_list of b₁
for b₄ being Element of vSUB holds [(<*b₂*> ^ b₃),b₄] in [:QC-WFF ,vSUB :] ) & ( for b₁ being Element of vSUB holds [<*[0,0]*>,b₁] in [:QC-WFF ,vSUB :] ) & ( for b₁ being FinSequence of [:NAT ,NAT :]
for b₂ being Element of vSUB st [b₁,b₂] in [:QC-WFF ,vSUB :] holds
[(<*[1,0]*> ^ b₁),b₂] in [:QC-WFF ,vSUB :] ) & ( for b₁, b₂ being FinSequence of [:NAT ,NAT :]
for b₃ being Element of vSUB st [b₁,b₃] in [:QC-WFF ,vSUB :] & [b₂,b₃] in [:QC-WFF ,vSUB :] holds
[((<*[2,0]*> ^ b₁) ^ b₂),b₃] in [:QC-WFF ,vSUB :] ) & ( for b₁ being bound_QC-variable
for b₂ being FinSequence of [:NAT ,NAT :]
for b₃ being Element of vSUB st [b₂,(QSub . [((<*[3,0]*> ^ <*b₁*>) ^ b₂),b₃])] in [:QC-WFF ,vSUB :] holds
[((<*[3,0]*> ^ <*b₁*>) ^ b₂),b₃] in [:QC-WFF ,vSUB :] ) )

proof end;

definition

let c₁ be set ;
attr a₁ is QC-Sub-closed means :Def16: :: SUBSTUT1:def 16
( a₁ is Subset of [:([:NAT ,NAT :] * ),vSUB :] & ( for b₁ being Nat
for b₂ being QC-pred_symbol of b₁
for b₃ being QC-variable_list of b₁
for b₄ being Element of vSUB holds [(<*b₂*> ^ b₃),b₄] in a₁ ) & ( for b₁ being Element of vSUB holds [<*[0,0]*>,b₁] in a₁ ) & ( for b₁ being FinSequence of [:NAT ,NAT :]
for b₂ being Element of vSUB st [b₁,b₂] in a₁ holds
[(<*[1,0]*> ^ b₁),b₂] in a₁ ) & ( for b₁, b₂ being FinSequence of [:NAT ,NAT :]
for b₃ being Element of vSUB st [b₁,b₃] in a₁ & [b₂,b₃] in a₁ holds
[((<*[2,0]*> ^ b₁) ^ b₂),b₃] in a₁ ) & ( for b₁ being bound_QC-variable
for b₂ being FinSequence of [:NAT ,NAT :]
for b₃ being Element of vSUB st [b₂,(QSub . [((<*[3,0]*> ^ <*b₁*>) ^ b₂),b₃])] in a₁ holds
[((<*[3,0]*> ^ <*b₁*>) ^ b₂),b₃] in a₁ ) );

end;

:: deftheorem Def16 defines QC-Sub-closed SUBSTUT1:def 16 :

registration

cluster non empty QC-Sub-closed set ;
existence

proof end;

end;

Lemma8: for b₁ being bound_QC-variable
for b₂ being FinSequence of [:NAT ,NAT :] holds (<*[3,0]*> ^ <*b₁*>) ^ b₂ is FinSequence of [:NAT ,NAT :]

proof end;

Lemma9: for b₁, b₂ being Nat
for b₃ being Element of vSUB holds [<*[b₁,b₂]*>,b₃] in [:([:NAT ,NAT :] * ),vSUB :]

proof end;

Lemma10: for b₁ being Nat
for b₂ being QC-pred_symbol of b₁
for b₃ being QC-variable_list of b₁
for b₄ being Element of vSUB holds [(<*b₂*> ^ b₃),b₄] in [:([:NAT ,NAT :] * ),vSUB :]

proof end;

definition

func QC-Sub-WFF -> non empty set means :Def17: :: SUBSTUT1:def 17
( a₁ is QC-Sub-closed & ( for b₁ being non empty set st b₁ is QC-Sub-closed holds
a₁ c= b₁ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def17 defines QC-Sub-WFF SUBSTUT1:def 17 :

theorem Th8: :: SUBSTUT1:8

for b₁ being Element of QC-Sub-WFF ex b₂ being QC-formulaex b₃ being Element of vSUB st b₁ = [b₂,b₃]

proof end;

registration

cluster QC-Sub-WFF -> non empty QC-Sub-closed ;
coherence by Def17;

end;

definition

let c₁ be QC-pred_symbol;
let c₂ be FinSequence of QC-variables ;
let c₃ be Element of vSUB ;
assume E13: the_arity_of c₁ = len c₂ ;
func Sub_P c₁,c₂,c₃ -> Element of QC-Sub-WFF equals :Def18: :: SUBSTUT1:def 18
[(a₁ ! a₂),a₃];
coherence

proof end;

end;

:: deftheorem Def18 defines Sub_P SUBSTUT1:def 18 :

theorem Th9: :: SUBSTUT1:9

for b₁ being Element of vSUB
for b₂ being Nat
for b₃ being QC-pred_symbol of b₂
for b₄ being QC-variable_list of b₂ holds Sub_P b₃,b₄,b₁ = [(b₃ ! b₄),b₁]

proof end;

definition

let c₁ be Element of QC-Sub-WFF ;
attr a₁ is Sub_VERUM means :Def19: :: SUBSTUT1:def 19
ex b₁ being Element of vSUB st a₁ = [VERUM ,b₁];

end;

:: deftheorem Def19 defines Sub_VERUM SUBSTUT1:def 19 :

definition

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

proof end;

redefine func `2 as c₁ `2 -> Element of vSUB ;
coherence

proof end;

end;

theorem Th10: :: SUBSTUT1:10

for b₁ being Element of QC-Sub-WFF holds b₁ = [(b₁ `1 ),(b₁ `2 )]

proof end;

definition

let c₁ be Element of QC-Sub-WFF ;
func Sub_not c₁ -> Element of QC-Sub-WFF equals :: SUBSTUT1:def 20
[('not' (a₁ `1 )),(a₁ `2 )];
coherence

proof end;

end;

:: deftheorem Def20 defines Sub_not SUBSTUT1:def 20 :

definition

let c₁, c₂ be Element of QC-Sub-WFF ;
assume E17: c₁ `2 = c₂ `2 ;
func Sub_& c₁,c₂ -> Element of QC-Sub-WFF equals :Def21: :: SUBSTUT1:def 21
[((a₁ `1 ) '&' (a₂ `1 )),(a₁ `2 )];
coherence

proof end;

end;

:: deftheorem Def21 defines Sub_& SUBSTUT1:def 21 :

definition

let c₁ be Element of [:QC-Sub-WFF ,bound_QC-variables :];
redefine func `1 as c₁ `1 -> Element of QC-Sub-WFF ;
coherence by MCART_1:10;
redefine func `2 as c₁ `2 -> Element of bound_QC-variables ;
coherence by MCART_1:10;

end;

definition

let c₁ be Element of [:QC-Sub-WFF ,bound_QC-variables :];
attr a₁ is quantifiable means :Def22: :: SUBSTUT1:def 22
ex b₁ being Element of vSUB st (a₁ `1 ) `2 = QSub . [(All (a₁ `2 ),((a₁ `1 ) `1 )),b₁];

end;

:: deftheorem Def22 defines quantifiable SUBSTUT1:def 22 :

definition

let c₁ be Element of [:QC-Sub-WFF ,bound_QC-variables :];
assume E19: c₁ is quantifiable ;
mode second_Q_comp of c₁ -> Element of vSUB means :Def23: :: SUBSTUT1:def 23
(a₁ `1 ) `2 = QSub . [(All (a₁ `2 ),((a₁ `1 ) `1 )),a₂];
existence by E19, Def22;

end;

:: deftheorem Def23 defines second_Q_comp SUBSTUT1:def 23 :

definition

let c₁ be Element of [:QC-Sub-WFF ,bound_QC-variables :];
let c₂ be second_Q_comp of c₁;
assume E20: c₁ is quantifiable ;
func Sub_All c₁,c₂ -> Element of QC-Sub-WFF equals :Def24: :: SUBSTUT1:def 24
[(All (a₁ `2 ),((a₁ `1 ) `1 )),a₂];
coherence

proof end;

end;

:: deftheorem Def24 defines Sub_All SUBSTUT1:def 24 :

definition

let c₁ be Element of QC-Sub-WFF ;
let c₂ be bound_QC-variable;
redefine func [ as [c₁,c₂] -> Element of [:QC-Sub-WFF ,bound_QC-variables :];
coherence

proof end;

end;

scheme :: SUBSTUT1:sch 1
s1{ P₁[ Element of QC-Sub-WFF ] } :

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

provided

E21: for b₁ being Nat
for b₂ being QC-pred_symbol of b₁
for b₃ being QC-variable_list of b₁
for b₄ being Element of vSUB holds P₁[ Sub_P b₂,b₃,b₄] and
E22: for b₁ being Element of QC-Sub-WFF st b₁ is Sub_VERUM holds
P₁[b₁] and
E23: for b₁ being Element of QC-Sub-WFF st P₁[b₁] holds
P₁[ Sub_not b₁] and
E24: for b₁, b₂ being Element of QC-Sub-WFF st b₁ `2 = b₂ `2 & P₁[b₁] & P₁[b₂] holds
P₁[ Sub_& b₁,b₂] and
E25: for b₁ being bound_QC-variable
for b₂ being Element of QC-Sub-WFF
for b₃ being second_Q_comp of [b₂,b₁] st [b₂,b₁] is quantifiable & P₁[b₂] holds
P₁[ Sub_All [b₂,b₁],b₃]

proof end;

definition

let c₁ be Element of QC-Sub-WFF ;
attr a₁ is Sub_atomic means :Def25: :: SUBSTUT1:def 25
ex b₁ being Natex b₂ being QC-pred_symbol of b₁ex b₃ being QC-variable_list of b₁ex b₄ being Element of vSUB st a₁ = Sub_P b₂,b₃,b₄;

end;

:: deftheorem Def25 defines Sub_atomic SUBSTUT1:def 25 :

theorem Th11: :: SUBSTUT1:11

for b₁ being Element of QC-Sub-WFF st b₁ is Sub_atomic holds
b₁ `1 is atomic

proof end;

registration

let c₁ be Nat;
let c₂ be QC-pred_symbol of c₁;
let c₃ be QC-variable_list of c₁;
let c₄ be Element of vSUB ;
cluster Sub_P a₂,a₃,a₄ -> Sub_atomic ;
coherence by Def25;

end;

definition

let c₁ be Element of QC-Sub-WFF ;
attr a₁ is Sub_negative means :Def26: :: SUBSTUT1:def 26
ex b₁ being Element of QC-Sub-WFF st a₁ = Sub_not b₁;
attr a₁ is Sub_conjunctive means :Def27: :: SUBSTUT1:def 27
ex b₁, b₂ being Element of QC-Sub-WFF st
( a₁ = Sub_& b₁,b₂ & b₁ `2 = b₂ `2 );

end;

:: deftheorem Def26 defines Sub_negative SUBSTUT1:def 26 :

:: deftheorem Def27 defines Sub_conjunctive SUBSTUT1:def 27 :

definition

let c₁ be set ;
attr a₁ is Sub_universal means :Def28: :: SUBSTUT1:def 28
ex b₁ being Element of [:QC-Sub-WFF ,bound_QC-variables :]ex b₂ being second_Q_comp of b₁ st
( a₁ = Sub_All b₁,b₂ & b₁ is quantifiable );

end;

:: deftheorem Def28 defines Sub_universal SUBSTUT1:def 28 :

theorem Th12: :: SUBSTUT1:12

for b₁ being Element of QC-Sub-WFF holds
( b₁ is Sub_VERUM or b₁ is Sub_atomic or b₁ is Sub_negative or b₁ is Sub_conjunctive or b₁ is Sub_universal )

proof end;

definition

let c₁ be Element of QC-Sub-WFF ;
assume E27: c₁ is Sub_atomic ;
func Sub_the_arguments_of c₁ -> FinSequence of QC-variables means :Def29: :: SUBSTUT1:def 29
ex b₁ being Natex b₂ being QC-pred_symbol of b₁ex b₃ being QC-variable_list of b₁ex b₄ being Element of vSUB st
( a₂ = b₃ & a₁ = Sub_P b₂,b₃,b₄ );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def29 defines Sub_the_arguments_of SUBSTUT1:def 29 :

definition

let c₁ be Element of QC-Sub-WFF ;
assume E28: c₁ is Sub_negative ;
func Sub_the_argument_of c₁ -> Element of QC-Sub-WFF means :Def30: :: SUBSTUT1:def 30
a₁ = Sub_not a₂;
existence by E28, Def26;
uniqueness

proof end;

end;

:: deftheorem Def30 defines Sub_the_argument_of SUBSTUT1:def 30 :

definition

let c₁ be Element of QC-Sub-WFF ;
assume E29: c₁ is Sub_conjunctive ;
func Sub_the_left_argument_of c₁ -> Element of QC-Sub-WFF means :Def31: :: SUBSTUT1:def 31
ex b₁ being Element of QC-Sub-WFF st
( a₁ = Sub_& a₂,b₁ & a₂ `2 = b₁ `2 );
existence by E29, Def27;
uniqueness

proof end;

end;

:: deftheorem Def31 defines Sub_the_left_argument_of SUBSTUT1:def 31 :

definition

let c₁ be Element of QC-Sub-WFF ;
assume E30: c₁ is Sub_conjunctive ;
func Sub_the_right_argument_of c₁ -> Element of QC-Sub-WFF means :Def32: :: SUBSTUT1:def 32
ex b₁ being Element of QC-Sub-WFF st
( a₁ = Sub_& b₁,a₂ & b₁ `2 = a₂ `2 );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def32 defines Sub_the_right_argument_of SUBSTUT1:def 32 :

definition

let c₁ be set ;
assume E31: c₁ is Sub_universal ;
func Sub_the_bound_of c₁ -> bound_QC-variable means :: SUBSTUT1:def 33
ex b₁ being Element of [:QC-Sub-WFF ,bound_QC-variables :]ex b₂ being second_Q_comp of b₁ st
( a₁ = Sub_All b₁,b₂ & b₁ `2 = a₂ & b₁ is quantifiable );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def33 defines Sub_the_bound_of SUBSTUT1:def 33 :

definition

let c₁ be set ;
assume E31: c₁ is Sub_universal ;
func Sub_the_scope_of c₁ -> Element of QC-Sub-WFF means :Def34: :: SUBSTUT1:def 34
ex b₁ being Element of [:QC-Sub-WFF ,bound_QC-variables :]ex b₂ being second_Q_comp of b₁ st
( a₁ = Sub_All b₁,b₂ & b₁ `1 = a₂ & b₁ is quantifiable );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def34 defines Sub_the_scope_of SUBSTUT1:def 34 :

registration

let c₁ be Element of QC-Sub-WFF ;
cluster Sub_not a₁ -> Sub_negative ;
coherence

proof end;

end;

theorem Th13: :: SUBSTUT1:13

for b₁, b₂ being Element of QC-Sub-WFF st b₁ `2 = b₂ `2 holds
Sub_& b₁,b₂ is Sub_conjunctive

proof end;

theorem Th14: :: SUBSTUT1:14

for b₁ being Element of [:QC-Sub-WFF ,bound_QC-variables :]
for b₂ being second_Q_comp of b₁ st b₁ is quantifiable holds
Sub_All b₁,b₂ is Sub_universal

proof end;

theorem Th15: :: SUBSTUT1:15

for b₁, b₂ being Element of QC-Sub-WFF st Sub_not b₁ = Sub_not b₂ holds
b₁ = b₂

proof end;

theorem Th16: :: SUBSTUT1:16

for b₁ being Element of QC-Sub-WFF holds Sub_the_argument_of (Sub_not b₁) = b₁ by Def30;

theorem Th17: :: SUBSTUT1:17

for b₁, b₂, b₃, b₄ being Element of QC-Sub-WFF st b₁ `2 = b₂ `2 & b₃ `2 = b₄ `2 & Sub_& b₁,b₂ = Sub_& b₃,b₄ holds
( b₁ = b₃ & b₂ = b₄ )

proof end;

theorem Th18: :: SUBSTUT1:18

for b₁, b₂ being Element of QC-Sub-WFF st b₁ `2 = b₂ `2 holds
Sub_the_left_argument_of (Sub_& b₁,b₂) = b₁

proof end;

theorem Th19: :: SUBSTUT1:19

for b₁, b₂ being Element of QC-Sub-WFF st b₁ `2 = b₂ `2 holds
Sub_the_right_argument_of (Sub_& b₁,b₂) = b₂

proof end;

theorem Th20: :: SUBSTUT1:20

for b₁, b₂ being Element of [:QC-Sub-WFF ,bound_QC-variables :]
for b₃ being second_Q_comp of b₁
for b₄ being second_Q_comp of b₂ st b₁ is quantifiable & b₂ is quantifiable & Sub_All b₁,b₃ = Sub_All b₂,b₄ holds
b₁ = b₂

proof end;

theorem Th21: :: SUBSTUT1:21

for b₁ being Element of [:QC-Sub-WFF ,bound_QC-variables :]
for b₂ being second_Q_comp of b₁ st b₁ is quantifiable holds
Sub_the_scope_of (Sub_All b₁,b₂) = b₁ `1

proof end;

scheme :: SUBSTUT1:sch 2
s2{ P₁[ Element of QC-Sub-WFF ] } :

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

provided

E39: for b₁ being Element of QC-Sub-WFF holds
( ( b₁ is Sub_atomic implies P₁[b₁] ) & ( b₁ is Sub_VERUM implies P₁[b₁] ) & ( b₁ is Sub_negative & P₁[ Sub_the_argument_of b₁] implies P₁[b₁] ) & ( b₁ is Sub_conjunctive & P₁[ Sub_the_left_argument_of b₁] & P₁[ Sub_the_right_argument_of b₁] implies P₁[b₁] ) & ( b₁ is Sub_universal & P₁[ Sub_the_scope_of b₁] implies P₁[b₁] ) )

proof end;

theorem Th22: :: SUBSTUT1:22

for b₁ being Element of QC-Sub-WFF st b₁ is Sub_negative holds
len (@ ((Sub_the_argument_of b₁) `1 )) < len (@ (b₁ `1 ))

proof end;

theorem Th23: :: SUBSTUT1:23

for b₁ being Element of QC-Sub-WFF st b₁ is Sub_conjunctive holds
( len (@ ((Sub_the_left_argument_of b₁) `1 )) < len (@ (b₁ `1 )) & len (@ ((Sub_the_right_argument_of b₁) `1 )) < len (@ (b₁ `1 )) )

proof end;

theorem Th24: :: SUBSTUT1:24

for b₁ being Element of QC-Sub-WFF st b₁ is Sub_universal holds
len (@ ((Sub_the_scope_of b₁) `1 )) < len (@ (b₁ `1 ))

proof end;

theorem Th25: :: SUBSTUT1:25

for b₁ being Element of QC-Sub-WFF holds
( ( b₁ is Sub_VERUM implies ((@ (b₁ `1 )) . 1) `1 = 0 ) & ( b₁ is Sub_atomic implies ex b₂ being Nat st (@ (b₁ `1 )) . 1 is QC-pred_symbol of b₂ ) & ( b₁ is Sub_negative implies ((@ (b₁ `1 )) . 1) `1 = 1 ) & ( b₁ is Sub_conjunctive implies ((@ (b₁ `1 )) . 1) `1 = 2 ) & ( b₁ is Sub_universal implies ((@ (b₁ `1 )) . 1) `1 = 3 ) )

proof end;

theorem Th26: :: SUBSTUT1:26

for b₁ being Element of QC-Sub-WFF st b₁ is Sub_atomic holds
( ((@ (b₁ `1 )) . 1) `1 <> 0 & ((@ (b₁ `1 )) . 1) `1 <> 1 & ((@ (b₁ `1 )) . 1) `1 <> 2 & ((@ (b₁ `1 )) . 1) `1 <> 3 )

proof end;

theorem Th27: :: SUBSTUT1:27

for b₁ being Element of QC-Sub-WFF holds
( not ( b₁ is Sub_atomic & b₁ is Sub_negative ) & not ( b₁ is Sub_atomic & b₁ is Sub_conjunctive ) & not ( b₁ is Sub_atomic & b₁ is Sub_universal ) & not ( b₁ is Sub_negative & b₁ is Sub_conjunctive ) & not ( b₁ is Sub_negative & b₁ is Sub_universal ) & not ( b₁ is Sub_conjunctive & b₁ is Sub_universal ) & not ( b₁ is Sub_VERUM & b₁ is Sub_atomic ) & not ( b₁ is Sub_VERUM & b₁ is Sub_negative ) & not ( b₁ is Sub_VERUM & b₁ is Sub_conjunctive ) & not ( b₁ is Sub_VERUM & b₁ is Sub_universal ) )

proof end;

scheme :: SUBSTUT1:sch 3
s3{ F₁() -> non empty set , F₂() -> Element of F₁(), F₃( Element of QC-Sub-WFF ) -> Element of F₁(), F₄( Element of F₁()) -> Element of F₁(), F₅( Element of F₁(), Element of F₁()) -> Element of F₁(), F₆( Element of QC-Sub-WFF , Element of F₁()) -> Element of F₁() } :

ex b₁ being Function of QC-Sub-WFF ,F₁() st
for b₂ being Element of QC-Sub-WFF
for b₃, b₄ being Element of F₁() holds
( ( b₂ is Sub_VERUM implies b₁ . b₂ = F₂() ) & ( b₂ is Sub_atomic implies b₁ . b₂ = F₃(b₂) ) & ( b₂ is Sub_negative & b₃ = b₁ . (Sub_the_argument_of b₂) implies b₁ . b₂ = F₄(b₃) ) & ( b₂ is Sub_conjunctive & b₃ = b₁ . (Sub_the_left_argument_of b₂) & b₄ = b₁ . (Sub_the_right_argument_of b₂) implies b₁ . b₂ = F₅(b₃,b₄) ) & ( b₂ is Sub_universal & b₃ = b₁ . (Sub_the_scope_of b₂) implies b₁ . b₂ = F₆(b₂,b₃) ) )

proof end;

scheme :: SUBSTUT1:sch 4
s4{ F₁() -> non empty set , F₂() -> Function of QC-Sub-WFF ,F₁(), F₃() -> Function of QC-Sub-WFF ,F₁(), F₄() -> Element of F₁(), F₅( set ) -> Element of F₁(), F₆( set ) -> Element of F₁(), F₇( set , set ) -> Element of F₁(), F₈( set , set ) -> Element of F₁() } :

F₂() = F₃()

provided

E45: for b₁ being Element of QC-Sub-WFF
for b₂, b₃ being Element of F₁() holds
( ( b₁ is Sub_VERUM implies F₂() . b₁ = F₄() ) & ( b₁ is Sub_atomic implies F₂() . b₁ = F₅(b₁) ) & ( b₁ is Sub_negative & b₂ = F₂() . (Sub_the_argument_of b₁) implies F₂() . b₁ = F₆(b₂) ) & ( b₁ is Sub_conjunctive & b₂ = F₂() . (Sub_the_left_argument_of b₁) & b₃ = F₂() . (Sub_the_right_argument_of b₁) implies F₂() . b₁ = F₇(b₂,b₃) ) & ( b₁ is Sub_universal & b₂ = F₂() . (Sub_the_scope_of b₁) implies F₂() . b₁ = F₈(b₁,b₂) ) ) and
E46: for b₁ being Element of QC-Sub-WFF
for b₂, b₃ being Element of F₁() holds
( ( b₁ is Sub_VERUM implies F₃() . b₁ = F₄() ) & ( b₁ is Sub_atomic implies F₃() . b₁ = F₅(b₁) ) & ( b₁ is Sub_negative & b₂ = F₃() . (Sub_the_argument_of b₁) implies F₃() . b₁ = F₆(b₂) ) & ( b₁ is Sub_conjunctive & b₂ = F₃() . (Sub_the_left_argument_of b₁) & b₃ = F₃() . (Sub_the_right_argument_of b₁) implies F₃() . b₁ = F₇(b₂,b₃) ) & ( b₁ is Sub_universal & b₂ = F₃() . (Sub_the_scope_of b₁) implies F₃() . b₁ = F₈(b₁,b₂) ) )

proof end;

definition

let c₁ be Element of QC-Sub-WFF ;
func @ c₁ -> Element of [:QC-WFF ,vSUB :] equals :: SUBSTUT1:def 35
a₁;
coherence

proof end;

end;

:: deftheorem Def35 defines @ SUBSTUT1:def 35 :

definition

let c₁ be Element of [:QC-WFF ,vSUB :];
redefine func `1 as c₁ `1 -> Element of QC-WFF ;
coherence

proof end;

redefine func `2 as c₁ `2 -> CQC_Substitution;
coherence

proof end;

end;

definition

let c₁ be Element of [:QC-WFF ,vSUB :];
func S_Bound c₁ -> bound_QC-variable equals :: SUBSTUT1:def 36
x. (upVar (RestrictSub (bound_in (a₁ `1 )),(a₁ `1 ),(a₁ `2 )),(the_scope_of (a₁ `1 ))) if bound_in (a₁ `1 ) in rng (RestrictSub (bound_in (a₁ `1 )),(a₁ `1 ),(a₁ `2 ))
otherwise bound_in (a₁ `1 );
coherence ;
consistency ;

end;

:: deftheorem Def36 defines S_Bound SUBSTUT1:def 36 :

definition

let c₁ be Element of QC-Sub-WFF ;
let c₂ be QC-formula;
func Quant c₁,c₂ -> Element of QC-WFF equals :: SUBSTUT1:def 37
All (S_Bound (@ a₁)),a₂;
coherence ;

end;

:: deftheorem Def37 defines Quant SUBSTUT1:def 37 :

Lemma45: for b₁, b₂ being Function of QC-Sub-WFF , QC-WFF st ( for b₃ being Element of QC-Sub-WFF holds
( ( b₃ is Sub_VERUM implies b₁ . b₃ = VERUM ) & ( b₃ is Sub_atomic implies b₁ . b₃ = (the_pred_symbol_of (b₃ `1 )) ! (CQC_Subst (Sub_the_arguments_of b₃),(b₃ `2 )) ) & ( b₃ is Sub_negative implies b₁ . b₃ = 'not' (b₁ . (Sub_the_argument_of b₃)) ) & ( b₃ is Sub_conjunctive implies b₁ . b₃ = (b₁ . (Sub_the_left_argument_of b₃)) '&' (b₁ . (Sub_the_right_argument_of b₃)) ) & ( b₃ is Sub_universal implies b₁ . b₃ = Quant b₃,(b₁ . (Sub_the_scope_of b₃)) ) ) ) & ( for b₃ being Element of QC-Sub-WFF holds
( ( b₃ is Sub_VERUM implies b₂ . b₃ = VERUM ) & ( b₃ is Sub_atomic implies b₂ . b₃ = (the_pred_symbol_of (b₃ `1 )) ! (CQC_Subst (Sub_the_arguments_of b₃),(b₃ `2 )) ) & ( b₃ is Sub_negative implies b₂ . b₃ = 'not' (b₂ . (Sub_the_argument_of b₃)) ) & ( b₃ is Sub_conjunctive implies b₂ . b₃ = (b₂ . (Sub_the_left_argument_of b₃)) '&' (b₂ . (Sub_the_right_argument_of b₃)) ) & ( b₃ is Sub_universal implies b₂ . b₃ = Quant b₃,(b₂ . (Sub_the_scope_of b₃)) ) ) ) holds
b₁ = b₂

proof end;

definition

let c₁ be Element of QC-Sub-WFF ;
func CQC_Sub c₁ -> Element of QC-WFF means :Def38: :: SUBSTUT1:def 38
ex b₁ being Function of QC-Sub-WFF , QC-WFF st
( a₂ = b₁ . a₁ & ( for b₂ being Element of QC-Sub-WFF holds
( ( b₂ is Sub_VERUM implies b₁ . b₂ = VERUM ) & ( b₂ is Sub_atomic implies b₁ . b₂ = (the_pred_symbol_of (b₂ `1 )) ! (CQC_Subst (Sub_the_arguments_of b₂),(b₂ `2 )) ) & ( b₂ is Sub_negative implies b₁ . b₂ = 'not' (b₁ . (Sub_the_argument_of b₂)) ) & ( b₂ is Sub_conjunctive implies b₁ . b₂ = (b₁ . (Sub_the_left_argument_of b₂)) '&' (b₁ . (Sub_the_right_argument_of b₂)) ) & ( b₂ is Sub_universal implies b₁ . b₂ = Quant b₂,(b₁ . (Sub_the_scope_of b₂)) ) ) ) );
existence

proof end;

uniqueness by Lemma45;

end;

:: deftheorem Def38 defines CQC_Sub SUBSTUT1:def 38 :

theorem Th28: :: SUBSTUT1:28

for b₁ being Element of QC-Sub-WFF st b₁ is Sub_negative holds
CQC_Sub b₁ = 'not' (CQC_Sub (Sub_the_argument_of b₁))

proof end;

theorem Th29: :: SUBSTUT1:29

for b₁ being Element of QC-Sub-WFF holds CQC_Sub (Sub_not b₁) = 'not' (CQC_Sub b₁)

proof end;

theorem Th30: :: SUBSTUT1:30

for b₁ being Element of QC-Sub-WFF st b₁ is Sub_conjunctive holds
CQC_Sub b₁ = (CQC_Sub (Sub_the_left_argument_of b₁)) '&' (CQC_Sub (Sub_the_right_argument_of b₁))

proof end;

theorem Th31: :: SUBSTUT1:31

for b₁, b₂ being Element of QC-Sub-WFF st b₁ `2 = b₂ `2 holds
CQC_Sub (Sub_& b₁,b₂) = (CQC_Sub b₁) '&' (CQC_Sub b₂)

proof end;

theorem Th32: :: SUBSTUT1:32

for b₁ being Element of QC-Sub-WFF st b₁ is Sub_universal holds
CQC_Sub b₁ = Quant b₁,(CQC_Sub (Sub_the_scope_of b₁))

proof end;

definition

func CQC-Sub-WFF -> Subset of QC-Sub-WFF equals :: SUBSTUT1:def 39
{ b₁ where B is Element of QC-Sub-WFF : b₁ `1 is Element of CQC-WFF } ;
coherence

proof end;

end;

:: deftheorem Def39 defines CQC-Sub-WFF SUBSTUT1:def 39 :

registration

cluster CQC-Sub-WFF -> non empty ;
coherence

proof end;

end;

theorem Th33: :: SUBSTUT1:33

for b₁ being Element of QC-Sub-WFF st b₁ is Sub_VERUM holds
CQC_Sub b₁ is Element of CQC-WFF

proof end;

Lemma53: for b₁ being Nat
for b₂ being QC-pred_symbol of b₁
for b₃ being CQC-variable_list of b₁ holds the_pred_symbol_of (b₂ ! b₃) = b₂

proof end;

theorem Th34: :: SUBSTUT1:34

for b₁ being Nat
for b₂ being FinSequence holds
( b₂ is CQC-variable_list of b₁ iff ( b₂ is FinSequence of bound_QC-variables & len b₂ = b₁ ) )

proof end;

theorem Th35: :: SUBSTUT1:35

for b₁ being Nat
for b₂ being QC-pred_symbol of b₁
for b₃ being CQC-variable_list of b₁
for b₄ being Element of vSUB holds CQC_Sub (Sub_P b₂,b₃,b₄) is Element of CQC-WFF

proof end;

theorem Th36: :: SUBSTUT1:36

for b₁ being Element of QC-Sub-WFF st CQC_Sub b₁ is Element of CQC-WFF holds
CQC_Sub (Sub_not b₁) is Element of CQC-WFF

proof end;

theorem Th37: :: SUBSTUT1:37

for b₁, b₂ being Element of QC-Sub-WFF st b₁ `2 = b₂ `2 & CQC_Sub b₁ is Element of CQC-WFF & CQC_Sub b₂ is Element of CQC-WFF holds
CQC_Sub (Sub_& b₁,b₂) is Element of CQC-WFF

proof end;

theorem Th38: :: SUBSTUT1:38

for b₁ being bound_QC-variable
for b₂ being Element of QC-Sub-WFF
for b₃ being second_Q_comp of [b₂,b₁] st CQC_Sub b₂ is Element of CQC-WFF & [b₂,b₁] is quantifiable holds
CQC_Sub (Sub_All [b₂,b₁],b₃) is Element of CQC-WFF

proof end;

scheme :: SUBSTUT1:sch 5
s5{ P₁[ set ] } :

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

provided

E59: for b₁, b₂ being Element of CQC-Sub-WFF
for b₃ being bound_QC-variable
for b₄ being second_Q_comp of [b₁,b₃]
for b₅ being Nat
for b₆ being CQC-variable_list of b₅
for b₇ being QC-pred_symbol of b₅
for b₈ being Element of vSUB holds
( P₁[ Sub_P b₇,b₆,b₈] & ( b₁ is Sub_VERUM implies P₁[b₁] ) & ( P₁[b₁] implies P₁[ Sub_not b₁] ) & ( b₁ `2 = b₂ `2 & P₁[b₁] & P₁[b₂] implies P₁[ Sub_& b₁,b₂] ) & ( [b₁,b₃] is quantifiable & P₁[b₁] implies P₁[ Sub_All [b₁,b₃],b₄] ) )

proof end;

definition

let c₁ be Element of CQC-Sub-WFF ;
redefine func CQC_Sub as CQC_Sub c₁ -> Element of CQC-WFF ;
coherence

proof end;

end;