SUBSTUT1: Substitution in First-Order Formulas: Elementary Properties

:: Substitution in First-Order Formulas: Elementary Properties
:: by Patrick Braselmann and Peter Koepke
::
:: Received September 25, 2004
:: Copyright (c) 2004-2011 Association of Mizar Users

begin

definition

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

end;

:: deftheorem defines vSUB SUBSTUT1:def 1 :

registration

cluster vSUB -> non empty ;
coherence ;

end;

definition

mode CQC_Substitution is Element of vSUB ;

end;

registration

cluster vSUB -> functional ;
coherence ;

end;

definition

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

end;

:: deftheorem defines @ SUBSTUT1:def 2 :

theorem Th1: :: SUBSTUT1:1

for a being set
for Sub being CQC_Substitution st a in dom Sub holds
Sub . a in bound_QC-variables

proof end;

definition

let l be FinSequence of QC-variables ;
let Sub be CQC_Substitution;
func CQC_Subst (l,Sub) -> FinSequence of QC-variables means :Def3: :: SUBSTUT1:def 3
( len it = len l & ( for k being Element of NAT st 1 <= k & k <= len l holds
( ( l . k in dom Sub implies it . k = Sub . (l . k) ) & ( not l . k in dom Sub implies it . k = l . k ) ) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def3 defines CQC_Subst SUBSTUT1:def 3 :

definition

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

proof end;

end;

:: deftheorem defines @ SUBSTUT1:def 4 :

definition

let l be FinSequence of bound_QC-variables ;
let Sub be CQC_Substitution;
func CQC_Subst (l,Sub) -> FinSequence of bound_QC-variables equals :: SUBSTUT1:def 5
CQC_Subst ((@ l),Sub);
coherence

proof end;

end;

:: deftheorem defines CQC_Subst SUBSTUT1:def 5 :

definition

let Sub be CQC_Substitution;
let X be set ;
:: original: |
redefine func Sub | X -> CQC_Substitution;
coherence

proof end;

end;

registration

cluster Relation-like Function-like finite Element of vSUB ;
existence

proof end;

end;

definition

let x be bound_QC-variable;
let p be QC-formula;
let Sub be CQC_Substitution;
func RestrictSub (x,p,Sub) -> finite CQC_Substitution equals :: SUBSTUT1:def 6
Sub | { y where y is bound_QC-variable : ( y in still_not-bound_in p & y is Element of dom Sub & y <> x & y <> Sub . y ) } ;
coherence

proof end;

end;

:: deftheorem defines RestrictSub SUBSTUT1:def 6 :

definition

let l1 be FinSequence of QC-variables ;
func Bound_Vars l1 -> Subset of bound_QC-variables equals :: SUBSTUT1:def 7
{ (l1 . k) where k is Element of NAT : ( 1 <= k & k <= len l1 & l1 . k in bound_QC-variables ) } ;
coherence

proof end;

end;

:: deftheorem defines Bound_Vars SUBSTUT1:def 7 :

definition

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

proof end;

end;

:: 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)} ) )

proof end;

theorem :: SUBSTUT1:2

Bound_Vars VERUM = {} by Lm1;

theorem :: SUBSTUT1:3

for p being QC-formula st p is atomic holds
Bound_Vars p = Bound_Vars (the_arguments_of p) by Lm1;

theorem :: SUBSTUT1:4

for p being QC-formula st p is negative holds
Bound_Vars p = Bound_Vars (the_argument_of p) by Lm1;

theorem :: SUBSTUT1:5

for p being QC-formula st p is conjunctive holds
Bound_Vars p = (Bound_Vars (the_left_argument_of p)) \/ (Bound_Vars (the_right_argument_of p)) by Lm1;

theorem :: SUBSTUT1:6

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

registration

let p be QC-formula;
cluster Bound_Vars p -> finite ;
coherence

proof end;

end;

definition

let p be QC-formula;
func Dom_Bound_Vars p -> finite Subset of NAT equals :: SUBSTUT1:def 9
{ i where i is Element of NAT : x. i in Bound_Vars p } ;
coherence

proof end;

end;

:: deftheorem defines Dom_Bound_Vars SUBSTUT1:def 9 :

definition

let finSub be finite CQC_Substitution;
func Sub_Var finSub -> finite Subset of NAT equals :: SUBSTUT1:def 10
{ i where i is Element of NAT : x. i in rng finSub } ;
coherence

proof end;

end;

:: deftheorem defines Sub_Var SUBSTUT1:def 10 :

definition

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

proof end;

end;

:: deftheorem defines NSub SUBSTUT1:def 11 :

definition

let finSub be finite CQC_Substitution;
let p be QC-formula;
func upVar (finSub,p) -> Element of NAT equals :: SUBSTUT1:def 12
min (NSub (p,finSub));
coherence ;

end;

:: 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 :: SUBSTUT1:def 13
finSub \/ {[x,(x. (upVar (finSub,p)))]} if x in rng finSub
otherwise finSub \/ {[x,x]};
coherence

proof end;

consistency ;

end;

:: deftheorem defines ExpandSub SUBSTUT1:def 13 :

definition

let p be QC-formula;
let Sub be CQC_Substitution;
let b be set ;
pred p,Sub PQSub b means :Def14: :: SUBSTUT1:def 14
( ( p is universal implies b = ExpandSub ((bound_in p),(the_scope_of p),(RestrictSub ((bound_in p),p,Sub))) ) & ( not p is universal implies b = {} ) );

end;

:: deftheorem Def14 defines PQSub SUBSTUT1:def 14 :

definition

func QSub -> Function means :: SUBSTUT1:def 15
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

proof end;

uniqueness

proof end;

end;

:: deftheorem defines QSub SUBSTUT1:def 15 :

begin

theorem Th7: :: SUBSTUT1:7

( [: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:] ) )

proof end;

definition

let IT be set ;
attr IT is QC-Sub-closed means :Def16: :: SUBSTUT1:def 16
( 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 :

registration

cluster non empty QC-Sub-closed set ;
existence

proof end;

end;

Lm2: for x being bound_QC-variable
for p being FinSequence of [:NAT,NAT:] holds (<*[3,0]*> ^ <*x*>) ^ p is FinSequence of [:NAT,NAT:]

proof end;

Lm3: for k, l being Element of NAT
for e being Element of vSUB holds [<*[k,l]*>,e] in [:([:NAT,NAT:] *),vSUB:]

proof end;

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:]

proof end;

definition

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

proof end;

uniqueness

proof end;

end;

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

theorem Th8: :: SUBSTUT1:8

for S being Element of QC-Sub-WFF ex p being QC-formula ex e being Element of vSUB st S = [p,e]

proof end;

registration

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

end;

definition

let P be QC-pred_symbol;
let l be FinSequence of QC-variables ;
let e be Element of vSUB ;
assume A1: the_arity_of P = len l ;
func Sub_P (P,l,e) -> Element of QC-Sub-WFF equals :Def18: :: SUBSTUT1:def 18
[(P ! l),e];
coherence

proof end;

end;

:: deftheorem Def18 defines Sub_P SUBSTUT1:def 18 :

theorem Th9: :: SUBSTUT1:9

for e being Element of vSUB
for k being Element of NAT
for P being QC-pred_symbol of k
for ll being QC-variable_list of k holds Sub_P (P,ll,e) = [(P ! ll),e]

proof end;

definition

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

end;

:: deftheorem Def19 defines Sub_VERUM SUBSTUT1:def 19 :

definition

let S be Element of QC-Sub-WFF ;
:: original: `1
redefine func S `1 -> Element of QC-WFF ;
coherence

proof end;

:: original: `2
redefine func S `2 -> Element of vSUB ;
coherence

proof end;

end;

theorem Th10: :: SUBSTUT1:10

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

proof end;

definition

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

proof end;

end;

:: deftheorem defines Sub_not SUBSTUT1:def 20 :

definition

let S, S9 be Element of QC-Sub-WFF ;
assume A1: S `2 = S9 `2 ;
func Sub_& (S,S9) -> Element of QC-Sub-WFF equals :Def21: :: SUBSTUT1:def 21
[((S `1) '&' (S9 `1)),(S `2)];
coherence

proof end;

end;

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

definition

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

end;

definition

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

end;

:: deftheorem Def22 defines quantifiable SUBSTUT1:def 22 :

definition

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

end;

:: deftheorem Def23 defines second_Q_comp SUBSTUT1:def 23 :

definition

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

proof end;

end;

:: deftheorem Def24 defines Sub_All SUBSTUT1:def 24 :

definition

let S be Element of QC-Sub-WFF ;
let x be bound_QC-variable;
:: original: [
redefine func [S,x] -> Element of [:QC-Sub-WFF,bound_QC-variables:];
coherence

proof end;

end;

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

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

provided

A1: 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₁[ Sub_P (P,ll,e)] and
A2: for S being Element of QC-Sub-WFF st S is Sub_VERUM holds
P₁[S] and
A3: for S being Element of QC-Sub-WFF st P₁[S] holds
P₁[ Sub_not S] and
A4: for S, S9 being Element of QC-Sub-WFF st S `2 = S9 `2 & P₁[S] & P₁[S9] holds
P₁[ Sub_& (S,S9)] and
A5: for x being bound_QC-variable
for S being Element of QC-Sub-WFF
for SQ being second_Q_comp of [S,x] st [S,x] is quantifiable & P₁[S] holds
P₁[ Sub_All ([S,x],SQ)]

proof end;

definition

let S be Element of QC-Sub-WFF ;
attr S is Sub_atomic means :Def25: :: SUBSTUT1:def 25
ex k being Element of NAT ex P being QC-pred_symbol of k ex ll being QC-variable_list of k ex e being Element of vSUB st S = Sub_P (P,ll,e);

end;

:: deftheorem Def25 defines Sub_atomic SUBSTUT1:def 25 :

theorem Th11: :: SUBSTUT1:11

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

proof end;

registration

let k be Element of NAT ;
let P be QC-pred_symbol of k;
let ll be QC-variable_list of k;
let e be Element of vSUB ;
cluster Sub_P (P,ll,e) -> Sub_atomic ;
coherence by Def25;

end;

definition

let S be Element of QC-Sub-WFF ;
attr S is Sub_negative means :Def26: :: SUBSTUT1:def 26
ex S9 being Element of QC-Sub-WFF st S = Sub_not S9;
attr S is Sub_conjunctive means :Def27: :: SUBSTUT1:def 27
ex S1, S2 being Element of QC-Sub-WFF st
( S = Sub_& (S1,S2) & S1 `2 = S2 `2 );

end;

:: deftheorem Def26 defines Sub_negative SUBSTUT1:def 26 :

:: deftheorem Def27 defines Sub_conjunctive SUBSTUT1:def 27 :

definition

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

end;

:: deftheorem Def28 defines Sub_universal SUBSTUT1:def 28 :

theorem Th12: :: SUBSTUT1:12

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

proof end;

definition

let S be Element of QC-Sub-WFF ;
assume A1: S is Sub_atomic ;
func Sub_the_arguments_of S -> FinSequence of QC-variables means :Def29: :: SUBSTUT1:def 29
ex k being Element of NAT ex P being QC-pred_symbol of k ex ll being QC-variable_list of k ex e being Element of vSUB st
( it = ll & S = Sub_P (P,ll,e) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def29 defines Sub_the_arguments_of SUBSTUT1:def 29 :

definition

let S be Element of QC-Sub-WFF ;
assume A1: S is Sub_negative ;
func Sub_the_argument_of S -> Element of QC-Sub-WFF means :Def30: :: SUBSTUT1:def 30
S = Sub_not it;
existence by A1, Def26;
uniqueness

proof end;

end;

:: deftheorem Def30 defines Sub_the_argument_of SUBSTUT1:def 30 :

definition

let S be Element of QC-Sub-WFF ;
assume A1: S is Sub_conjunctive ;
func Sub_the_left_argument_of S -> Element of QC-Sub-WFF means :Def31: :: SUBSTUT1:def 31
ex S9 being Element of QC-Sub-WFF st
( S = Sub_& (it,S9) & it `2 = S9 `2 );
existence by A1, Def27;
uniqueness

proof end;

end;

:: deftheorem Def31 defines Sub_the_left_argument_of SUBSTUT1:def 31 :

definition

let S be Element of QC-Sub-WFF ;
assume A1: S is Sub_conjunctive ;
func Sub_the_right_argument_of S -> Element of QC-Sub-WFF means :Def32: :: SUBSTUT1:def 32
ex S9 being Element of QC-Sub-WFF st
( S = Sub_& (S9,it) & S9 `2 = it `2 );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def32 defines Sub_the_right_argument_of SUBSTUT1:def 32 :

definition

let A be set ;
assume A1: A is Sub_universal ;
func Sub_the_bound_of A -> bound_QC-variable means :: SUBSTUT1:def 33
ex B being Element of [:QC-Sub-WFF,bound_QC-variables:] ex SQ being second_Q_comp of B st
( A = Sub_All (B,SQ) & B `2 = it & B is quantifiable );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem defines Sub_the_bound_of SUBSTUT1:def 33 :

definition

let A be set ;
assume A1: A is Sub_universal ;
func Sub_the_scope_of A -> Element of QC-Sub-WFF means :Def34: :: SUBSTUT1:def 34
ex B being Element of [:QC-Sub-WFF,bound_QC-variables:] ex SQ being second_Q_comp of B st
( A = Sub_All (B,SQ) & B `1 = it & B is quantifiable );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def34 defines Sub_the_scope_of SUBSTUT1:def 34 :

registration

let S be Element of QC-Sub-WFF ;
cluster Sub_not S -> Sub_negative ;
coherence

proof end;

end;

theorem Th13: :: SUBSTUT1:13

for S1, S2 being Element of QC-Sub-WFF st S1 `2 = S2 `2 holds
Sub_& (S1,S2) is Sub_conjunctive

proof end;

theorem Th14: :: SUBSTUT1:14

for B being Element of [:QC-Sub-WFF,bound_QC-variables:]
for SQ being second_Q_comp of B st B is quantifiable holds
Sub_All (B,SQ) is Sub_universal

proof end;

theorem :: SUBSTUT1:15

for S, S9 being Element of QC-Sub-WFF st Sub_not S = Sub_not S9 holds
S = S9

proof end;

theorem :: SUBSTUT1:16

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

theorem :: SUBSTUT1:17

for S1, S2, S19, S29 being Element of QC-Sub-WFF st S1 `2 = S2 `2 & S19 `2 = S29 `2 & Sub_& (S1,S2) = Sub_& (S19,S29) holds
( S1 = S19 & S2 = S29 )

proof end;

theorem Th18: :: SUBSTUT1:18

for S1, S2 being Element of QC-Sub-WFF st S1 `2 = S2 `2 holds
Sub_the_left_argument_of (Sub_& (S1,S2)) = S1

proof end;

theorem Th19: :: SUBSTUT1:19

for S1, S2 being Element of QC-Sub-WFF st S1 `2 = S2 `2 holds
Sub_the_right_argument_of (Sub_& (S1,S2)) = S2

proof end;

theorem :: SUBSTUT1:20

for B1, B2 being Element of [:QC-Sub-WFF,bound_QC-variables:]
for SQ1 being second_Q_comp of B1
for SQ2 being second_Q_comp of B2 st B1 is quantifiable & B2 is quantifiable & Sub_All (B1,SQ1) = Sub_All (B2,SQ2) holds
B1 = B2

proof end;

theorem Th21: :: SUBSTUT1:21

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

proof end;

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

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

provided

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

proof end;

theorem Th22: :: SUBSTUT1:22

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

proof end;

theorem Th23: :: SUBSTUT1:23

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

proof end;

theorem Th24: :: SUBSTUT1:24

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

proof end;

theorem Th25: :: SUBSTUT1:25

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

proof end;

theorem Th26: :: SUBSTUT1:26

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

proof end;

theorem Th27: :: SUBSTUT1:27

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

proof end;

scheme :: SUBSTUT1:sch 3
SubFuncEx{ 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 F being Function of QC-Sub-WFF,F₁() st
for S being Element of QC-Sub-WFF
for d1, d2 being Element of F₁() holds
( ( S is Sub_VERUM implies F . S = F₂() ) & ( S is Sub_atomic implies F . S = F₃(S) ) & ( S is Sub_negative & d1 = F . (Sub_the_argument_of S) implies F . S = F₄(d1) ) & ( S is Sub_conjunctive & d1 = F . (Sub_the_left_argument_of S) & d2 = F . (Sub_the_right_argument_of S) implies F . S = F₅(d1,d2) ) & ( S is Sub_universal & d1 = F . (Sub_the_scope_of S) implies F . S = F₆(S,d1) ) )

proof end;

scheme :: SUBSTUT1:sch 4
SubQCFuncUniq{ 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

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

proof end;

definition

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

proof end;

end;

:: deftheorem defines @ SUBSTUT1:def 35 :

definition

let Z be Element of [:QC-WFF,vSUB:];
:: original: `1
redefine func Z `1 -> Element of QC-WFF ;
coherence

proof end;

:: original: `2
redefine func Z `2 -> CQC_Substitution;
coherence

proof end;

end;

definition

let Z be Element of [:QC-WFF,vSUB:];
func S_Bound Z -> bound_QC-variable equals :: SUBSTUT1:def 36
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 ;
consistency ;

end;

:: deftheorem defines S_Bound SUBSTUT1:def 36 :

definition

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

end;

:: 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

proof end;

begin

definition

let S be Element of QC-Sub-WFF ;
func CQC_Sub S -> Element of QC-WFF means :Def38: :: SUBSTUT1:def 38
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

proof end;

uniqueness by Lm5;

end;

:: deftheorem Def38 defines CQC_Sub SUBSTUT1:def 38 :

theorem Th28: :: SUBSTUT1:28

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

proof end;

theorem Th29: :: SUBSTUT1:29

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

proof end;

theorem Th30: :: SUBSTUT1:30

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

proof end;

theorem Th31: :: SUBSTUT1:31

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

proof end;

theorem Th32: :: SUBSTUT1:32

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

proof end;

definition

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

proof end;

end;

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

registration

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

proof end;

end;

theorem Th33: :: SUBSTUT1:33

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

proof end;

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

proof end;

theorem Th34: :: SUBSTUT1:34

for k being Element of NAT
for h being FinSequence holds
( h is CQC-variable_list of k iff ( h is FinSequence of bound_QC-variables & len h = k ) )

proof end;

theorem Th35: :: SUBSTUT1:35

for k being Element of NAT
for P being QC-pred_symbol of k
for ll being CQC-variable_list of k
for e being Element of vSUB holds CQC_Sub (Sub_P (P,ll,e)) is Element of CQC-WFF

proof end;

theorem Th36: :: SUBSTUT1:36

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

proof end;

theorem Th37: :: SUBSTUT1:37

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

proof end;

theorem Th38: :: SUBSTUT1:38

for x being bound_QC-variable
for S being Element of QC-Sub-WFF
for xSQ being second_Q_comp of [S,x] st CQC_Sub S is Element of CQC-WFF & [S,x] is quantifiable holds
CQC_Sub (Sub_All ([S,x],xSQ)) is Element of CQC-WFF

proof end;

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

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

provided

A1: for S, S9 being Element of CQC-Sub-WFF
for x being bound_QC-variable
for SQ being second_Q_comp of [S,x]
for k being Element of NAT
for ll being CQC-variable_list of k
for P being QC-pred_symbol of k
for e being Element of vSUB holds
( P₁[ Sub_P (P,ll,e)] & ( S is Sub_VERUM implies P₁[S] ) & ( P₁[S] implies P₁[ Sub_not S] ) & ( S `2 = S9 `2 & P₁[S] & P₁[S9] implies P₁[ Sub_& (S,S9)] ) & ( [S,x] is quantifiable & P₁[S] implies P₁[ Sub_All ([S,x],SQ)] ) )

proof end;

definition

let S be Element of CQC-Sub-WFF ;
:: original: CQC_Sub
redefine func CQC_Sub S -> Element of CQC-WFF ;
coherence

proof end;

end;