SUBSTUT1: Substitution in First-Order Formulas: Elementary Properties

end;

:: deftheorem defines vSUB SUBSTUT1:def 1 :

registration

let A be QC-alphabet ;

cluster vSUB A -> non empty ;

end;

definition

let A be QC-alphabet ;
mode CQC_Substitution of A is Element of vSUB A;

end;

registration

let A be QC-alphabet ;

cluster vSUB A -> functional ;

end;

definition

let A be QC-alphabet ;
let Sub be CQC_Substitution of A;

func @ Sub -> PartFunc of (bound_QC-variables A),(bound_QC-variables A) equals :: SUBSTUT1:def 2
Sub;

coherence by PARTFUN1:47;

end;

:: deftheorem defines @ SUBSTUT1:def 2 :

theorem Th1: :: SUBSTUT1:1

for A being QC-alphabet
for a being object
for Sub being CQC_Substitution of A st a in dom Sub holds
Sub . a in bound_QC-variables A

proof end;

definition

let A be QC-alphabet ;
let l be FinSequence of QC-variables A;
let Sub be CQC_Substitution of A;

func CQC_Subst (l,Sub) -> FinSequence of QC-variables A means :Def3: :: SUBSTUT1:def 3
( len it = len l & ( for k being 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 ) ) ) );

proof end;

proof end;

end;

:: deftheorem Def3 defines CQC_Subst SUBSTUT1:def 3 :

definition

let A be QC-alphabet ;
let l be FinSequence of bound_QC-variables A;

func @ l -> FinSequence of QC-variables A equals :: SUBSTUT1:def 4
l;

proof end;

end;

:: deftheorem defines @ SUBSTUT1:def 4 :

definition

let A be QC-alphabet ;
let l be FinSequence of bound_QC-variables A;
let Sub be CQC_Substitution of A;

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

proof end;

end;

:: deftheorem defines CQC_Subst SUBSTUT1:def 5 :

definition

let A be QC-alphabet ;
let Sub be CQC_Substitution of A;
let X be set ;
:: original: |
redefine func Sub | X -> CQC_Substitution of A;
coherence

proof end;

end;

registration

let A be QC-alphabet ;

cluster Relation-like Function-like finite for Element of vSUB A;

proof end;

end;

definition

let A be QC-alphabet ;
let x be bound_QC-variable of A;
let p be QC-formula of A;
let Sub be CQC_Substitution of A;

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

proof end;

end;

:: deftheorem defines RestrictSub SUBSTUT1:def 6 :

definition

let A be QC-alphabet ;
let l1 be FinSequence of QC-variables A;

func Bound_Vars l1 -> Subset of (bound_QC-variables A) equals :: SUBSTUT1:def 7
{ (l1 . k) where k is Nat : ( 1 <= k & k <= len l1 & l1 . k in bound_QC-variables A ) } ;

proof end;

end;

:: deftheorem defines Bound_Vars SUBSTUT1:def 7 :

definition

let A be QC-alphabet ;
let p be QC-formula of A;

func Bound_Vars p -> Subset of (bound_QC-variables A) means :Def8: :: SUBSTUT1:def 8
ex F being Function of (QC-WFF A),(bool (bound_QC-variables A)) st
( it = F . p & ( for p being Element of QC-WFF A
for d1, d2 being Subset of (bound_QC-variables A) holds
( ( p = VERUM A implies F . p = {} (bound_QC-variables A) ) & ( 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 A being QC-alphabet
for p being QC-formula of A holds
( Bound_Vars (VERUM A) = {} (bound_QC-variables A) & ( 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 Th2: :: SUBSTUT1:2

for A being QC-alphabet holds Bound_Vars (VERUM A) = {}

proof end;

theorem :: SUBSTUT1:3

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

theorem :: SUBSTUT1:4

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

theorem :: SUBSTUT1:5

for A being QC-alphabet
for p being QC-formula of A 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 A being QC-alphabet
for p being QC-formula of A st p is universal holds
Bound_Vars p = (Bound_Vars (the_scope_of p)) \/ {(bound_in p)} by Lm1;

registration

let A be QC-alphabet ;
let p be QC-formula of A;

cluster Bound_Vars p -> finite ;

proof end;

end;

definition

let A be QC-alphabet ;
let p be QC-formula of A;

func Dom_Bound_Vars p -> finite Subset of (QC-symbols A) equals :: SUBSTUT1:def 9
{ s where s is QC-symbol of A : x. s in Bound_Vars p } ;

proof end;

end;

:: deftheorem defines Dom_Bound_Vars SUBSTUT1:def 9 :

definition

let A be QC-alphabet ;
let finSub be finite CQC_Substitution of A;

func Sub_Var finSub -> finite Subset of (QC-symbols A) equals :: SUBSTUT1:def 10
{ s where s is QC-symbol of A : x. s in rng finSub } ;

proof end;

end;

:: deftheorem defines Sub_Var SUBSTUT1:def 10 :

Lm2: for X, Y being set st card X in card Y holds
Y \ X <> {}

proof end;

definition

let A be QC-alphabet ;
let p be QC-formula of A;
let finSub be finite CQC_Substitution of A;

func NSub (p,finSub) -> non empty Subset of (QC-symbols A) equals :: SUBSTUT1:def 11
NAT \ ((Dom_Bound_Vars p) \/ (Sub_Var finSub));

proof end;

end;

:: deftheorem defines NSub SUBSTUT1:def 11 :

definition

let A be QC-alphabet ;
let finSub be finite CQC_Substitution of A;
let p be QC-formula of A;

func upVar (finSub,p) -> QC-symbol of A equals :: SUBSTUT1:def 12
the Element of NSub (p,finSub);

end;

:: deftheorem defines upVar SUBSTUT1:def 12 :

definition

let A be QC-alphabet ;
let x be bound_QC-variable of A;
let p be QC-formula of A;
let finSub be finite CQC_Substitution of A;
assume A1: ex Sub being CQC_Substitution of A st finSub = RestrictSub (x,(All (x,p)),Sub) ;

func ExpandSub (x,p,finSub) -> CQC_Substitution of A equals :: SUBSTUT1:def 13
finSub \/ {[x,(x. (upVar (finSub,p)))]} if x in rng finSub
otherwise finSub \/ {[x,x]};

proof end;

consistency ;

end;

:: deftheorem defines ExpandSub SUBSTUT1:def 13 :

definition

let A be QC-alphabet ;
let p be QC-formula of A;
let Sub be CQC_Substitution of A;
let b be object ;

pred p,Sub PQSub b means :: 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 defines PQSub SUBSTUT1:def 14 :

definition

let A be QC-alphabet ;

func QSub A -> Function means :: SUBSTUT1:def 15
for a being object holds
( a in it iff ex p being QC-formula of A ex Sub being CQC_Substitution of A ex b being object st
( a = [[p,Sub],b] & p,Sub PQSub b ) );

proof end;

proof end;

end;

:: deftheorem defines QSub SUBSTUT1:def 15 :

theorem Th7: :: SUBSTUT1:7

for A being QC-alphabet holds
( [:(QC-WFF A),(vSUB A):] is Subset of [:([:NAT,(QC-symbols A):] *),(vSUB A):] & ( for k being Nat
for p being QC-pred_symbol of k,A
for ll being QC-variable_list of k,A
for e being Element of vSUB A holds [(<*p*> ^ ll),e] in [:(QC-WFF A),(vSUB A):] ) & ( for e being Element of vSUB A holds [<*[0,0]*>,e] in [:(QC-WFF A),(vSUB A):] ) & ( for p being FinSequence of [:NAT,(QC-symbols A):]
for e being Element of vSUB A st [p,e] in [:(QC-WFF A),(vSUB A):] holds
[(<*[1,0]*> ^ p),e] in [:(QC-WFF A),(vSUB A):] ) & ( for p, q being FinSequence of [:NAT,(QC-symbols A):]
for e being Element of vSUB A st [p,e] in [:(QC-WFF A),(vSUB A):] & [q,e] in [:(QC-WFF A),(vSUB A):] holds
[((<*[2,0]*> ^ p) ^ q),e] in [:(QC-WFF A),(vSUB A):] ) & ( for x being bound_QC-variable of A
for p being FinSequence of [:NAT,(QC-symbols A):]
for e being Element of vSUB A st [p,((QSub A) . [((<*[3,0]*> ^ <*x*>) ^ p),e])] in [:(QC-WFF A),(vSUB A):] holds
[((<*[3,0]*> ^ <*x*>) ^ p),e] in [:(QC-WFF A),(vSUB A):] ) )

proof end;

definition

let A be QC-alphabet ;
let IT be set ;

attr IT is A -Sub-closed means :Def16: :: SUBSTUT1:def 16
( IT is Subset of [:([:NAT,(QC-symbols A):] *),(vSUB A):] & ( for k being Nat
for p being QC-pred_symbol of k,A
for ll being QC-variable_list of k,A
for e being Element of vSUB A holds [(<*p*> ^ ll),e] in IT ) & ( for e being Element of vSUB A holds [<*[0,0]*>,e] in IT ) & ( for p being FinSequence of [:NAT,(QC-symbols A):]
for e being Element of vSUB A st [p,e] in IT holds
[(<*[1,0]*> ^ p),e] in IT ) & ( for p, q being FinSequence of [:NAT,(QC-symbols A):]
for e being Element of vSUB A st [p,e] in IT & [q,e] in IT holds
[((<*[2,0]*> ^ p) ^ q),e] in IT ) & ( for x being bound_QC-variable of A
for p being FinSequence of [:NAT,(QC-symbols A):]
for e being Element of vSUB A st [p,((QSub A) . [((<*[3,0]*> ^ <*x*>) ^ p),e])] in IT holds
[((<*[3,0]*> ^ <*x*>) ^ p),e] in IT ) );

end;

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

registration

let A be QC-alphabet ;

cluster non empty A -Sub-closed for set ;

proof end;

end;

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

proof end;

Lm4: for A being QC-alphabet
for k being Nat
for l being QC-symbol of A
for e being Element of vSUB A holds [<*[k,l]*>,e] in [:([:NAT,(QC-symbols A):] *),(vSUB A):]

proof end;

Lm5: for A being QC-alphabet
for k being Nat
for p being QC-pred_symbol of k,A
for ll being QC-variable_list of k,A
for e being Element of vSUB A holds [(<*p*> ^ ll),e] in [:([:NAT,(QC-symbols A):] *),(vSUB A):]

proof end;

definition

let A be QC-alphabet ;

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

proof end;

proof end;

end;

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

theorem Th8: :: SUBSTUT1:8

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

proof end;

registration

let A be QC-alphabet ;

cluster QC-Sub-WFF A -> non empty A -Sub-closed ;

coherence by Def17;

end;

definition

let A be QC-alphabet ;
let P be QC-pred_symbol of A;
let l be FinSequence of QC-variables A;
let e be Element of vSUB A;
assume A1: the_arity_of P = len l ;

func Sub_P (P,l,e) -> Element of QC-Sub-WFF A equals :Def18: :: SUBSTUT1:def 18
[(P ! l),e];

proof end;

end;

:: deftheorem Def18 defines Sub_P SUBSTUT1:def 18 :

theorem Th9: :: SUBSTUT1:9

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

proof end;

definition

let A be QC-alphabet ;
let S be Element of QC-Sub-WFF A;

attr S is A -Sub_VERUM means :: SUBSTUT1:def 19
ex e being Element of vSUB A st S = [(VERUM A),e];

end;

:: deftheorem defines -Sub_VERUM SUBSTUT1:def 19 :

definition

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

proof end;

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

proof end;

end;

theorem Th10: :: SUBSTUT1:10

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

proof end;

definition

let A be QC-alphabet ;
let S be Element of QC-Sub-WFF A;

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

proof end;

end;

:: deftheorem defines Sub_not SUBSTUT1:def 20 :

definition

let A be QC-alphabet ;
let S, S9 be Element of QC-Sub-WFF A;
assume A1: S `2 = S9 `2 ;

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

proof end;

end;

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

definition

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

end;

definition

let A be QC-alphabet ;
let B be Element of [:(QC-Sub-WFF A),(bound_QC-variables A):];

attr B is quantifiable means :: SUBSTUT1:def 22
ex e being Element of vSUB A st (B `1) `2 = (QSub A) . [(All ((B `2),((B `1) `1))),e];

end;

:: deftheorem defines quantifiable SUBSTUT1:def 22 :

definition

let A be QC-alphabet ;
let B be Element of [:(QC-Sub-WFF A),(bound_QC-variables A):];
assume A1: B is quantifiable ;

mode second_Q_comp of B -> Element of vSUB A means :Def23: :: SUBSTUT1:def 23
(B `1) `2 = (QSub A) . [(All ((B `2),((B `1) `1))),it];

existence by A1;

end;

:: deftheorem Def23 defines second_Q_comp SUBSTUT1:def 23 :

definition

let A be QC-alphabet ;
let B be Element of [:(QC-Sub-WFF A),(bound_QC-variables A):];
let SQ be second_Q_comp of B;
assume A1: B is quantifiable ;

func Sub_All (B,SQ) -> Element of QC-Sub-WFF A equals :Def24: :: SUBSTUT1:def 24
[(All ((B `2),((B `1) `1))),SQ];

proof end;

end;

:: deftheorem Def24 defines Sub_All SUBSTUT1:def 24 :

definition

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

proof end;

end;

scheme :: SUBSTUT1:sch 1
SubQCInd{ F₁() -> QC-alphabet , P₁[ Element of QC-Sub-WFF F₁()] } :

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

provided

A1: for k being Nat
for P being QC-pred_symbol of k,F₁()
for ll being QC-variable_list of k,F₁()
for e being Element of vSUB F₁() holds P₁[ Sub_P (P,ll,e)] and
A2: for S being Element of QC-Sub-WFF F₁() st S is F₁() -Sub_VERUM holds
P₁[S] and
A3: for S being Element of QC-Sub-WFF F₁() st P₁[S] holds
P₁[ Sub_not S] and
A4: for S, S9 being Element of QC-Sub-WFF F₁() st S `2 = S9 `2 & P₁[S] & P₁[S9] holds
P₁[ Sub_& (S,S9)] and
A5: for x being bound_QC-variable of F₁()
for S being Element of QC-Sub-WFF F₁()
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 A be QC-alphabet ;
let S be Element of QC-Sub-WFF A;

attr S is Sub_atomic means :: SUBSTUT1:def 25
ex k being Nat ex P being QC-pred_symbol of k,A ex ll being QC-variable_list of k,A ex e being Element of vSUB A st S = Sub_P (P,ll,e);

end;

:: deftheorem defines Sub_atomic SUBSTUT1:def 25 :

theorem Th11: :: SUBSTUT1:11

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

proof end;

registration

let A be QC-alphabet ;
let k be Nat;
let P be QC-pred_symbol of k,A;
let ll be QC-variable_list of k,A;
let e be Element of vSUB A;

cluster Sub_P (P,ll,e) -> Sub_atomic ;

end;

definition

let A be QC-alphabet ;
let S be Element of QC-Sub-WFF A;

attr S is Sub_negative means :Def26: :: SUBSTUT1:def 26
ex S9 being Element of QC-Sub-WFF A st S = Sub_not S9;

attr S is Sub_conjunctive means :Def27: :: SUBSTUT1:def 27
ex S1, S2 being Element of QC-Sub-WFF A 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 QC-alphabet ;
let S be Element of QC-Sub-WFF A;

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

end;

:: deftheorem Def28 defines Sub_universal SUBSTUT1:def 28 :

theorem Th12: :: SUBSTUT1:12

for A being QC-alphabet
for S being Element of QC-Sub-WFF A holds
( S is A -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 A be QC-alphabet ;
let S be Element of QC-Sub-WFF A;
assume A1: S is Sub_atomic ;

func Sub_the_arguments_of S -> FinSequence of QC-variables A means :Def29: :: SUBSTUT1:def 29
ex k being Nat ex P being QC-pred_symbol of k,A ex ll being QC-variable_list of k,A ex e being Element of vSUB A st
( it = ll & S = Sub_P (P,ll,e) );

proof end;

end;

:: deftheorem Def29 defines Sub_the_arguments_of SUBSTUT1:def 29 :

definition

let A be QC-alphabet ;
let S be Element of QC-Sub-WFF A;
assume A1: S is Sub_negative ;

func Sub_the_argument_of S -> Element of QC-Sub-WFF A means :Def30: :: SUBSTUT1:def 30
S = Sub_not it;

proof end;

end;

:: deftheorem Def30 defines Sub_the_argument_of SUBSTUT1:def 30 :

definition

let A be QC-alphabet ;
let S be Element of QC-Sub-WFF A;
assume A1: S is Sub_conjunctive ;

func Sub_the_left_argument_of S -> Element of QC-Sub-WFF A means :Def31: :: SUBSTUT1:def 31
ex S9 being Element of QC-Sub-WFF A st
( S = Sub_& (it,S9) & it `2 = S9 `2 );

proof end;

end;

:: deftheorem Def31 defines Sub_the_left_argument_of SUBSTUT1:def 31 :

definition

let A be QC-alphabet ;
let S be Element of QC-Sub-WFF A;
assume A1: S is Sub_conjunctive ;

func Sub_the_right_argument_of S -> Element of QC-Sub-WFF A means :Def32: :: SUBSTUT1:def 32
ex S9 being Element of QC-Sub-WFF A st
( S = Sub_& (S9,it) & S9 `2 = it `2 );

proof end;

end;

:: deftheorem Def32 defines Sub_the_right_argument_of SUBSTUT1:def 32 :

definition

let A be QC-alphabet ;
let S be Element of QC-Sub-WFF A;
assume A1: S is Sub_universal ;

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

proof end;

proof end;

end;

:: deftheorem defines Sub_the_bound_of SUBSTUT1:def 33 :

definition

let A be QC-alphabet ;
let A2 be Element of QC-Sub-WFF A;
assume A1: A2 is Sub_universal ;

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

proof end;

proof end;

end;

:: deftheorem Def34 defines Sub_the_scope_of SUBSTUT1:def 34 :

registration

let A be QC-alphabet ;
let S be Element of QC-Sub-WFF A;

cluster Sub_not S -> Sub_negative ;

end;

theorem Th13: :: SUBSTUT1:13

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

theorem Th14: :: SUBSTUT1:14

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

theorem :: SUBSTUT1:15

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

proof end;

theorem :: SUBSTUT1:16

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

theorem :: SUBSTUT1:17

for A being QC-alphabet
for S1, S2, S19, S29 being Element of QC-Sub-WFF A 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 A being QC-alphabet
for S1, S2 being Element of QC-Sub-WFF A st S1 `2 = S2 `2 holds
Sub_the_left_argument_of (Sub_& (S1,S2)) = S1

proof end;

theorem Th19: :: SUBSTUT1:19

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

proof end;

theorem :: SUBSTUT1:20

for A being QC-alphabet
for B1, B2 being Element of [:(QC-Sub-WFF A),(bound_QC-variables A):]
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 A being QC-alphabet
for B being Element of [:(QC-Sub-WFF A),(bound_QC-variables A):]
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{ F₁() -> QC-alphabet , P₁[ Element of QC-Sub-WFF F₁()] } :

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

provided

A1: for S being Element of QC-Sub-WFF F₁() holds
( ( S is Sub_atomic implies P₁[S] ) & ( S is F₁() -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 A being QC-alphabet
for S being Element of QC-Sub-WFF A st S is Sub_negative holds
len (@ ((Sub_the_argument_of S) `1)) < len (@ (S `1))

proof end;

theorem Th23: :: SUBSTUT1:23

for A being QC-alphabet
for S being Element of QC-Sub-WFF A 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 A being QC-alphabet
for S being Element of QC-Sub-WFF A st S is Sub_universal holds
len (@ ((Sub_the_scope_of S) `1)) < len (@ (S `1))

proof end;

theorem Th25: :: SUBSTUT1:25

for A being QC-alphabet
for S being Element of QC-Sub-WFF A holds
( ( S is A -Sub_VERUM implies ((@ (S `1)) . 1) `1 = 0 ) & ( S is Sub_atomic implies ex k being Nat st (@ (S `1)) . 1 is QC-pred_symbol of k,A ) & ( 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 A being QC-alphabet
for S being Element of QC-Sub-WFF A 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 A being QC-alphabet
for S being Element of QC-Sub-WFF A 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 A -Sub_VERUM & S is Sub_atomic ) & not ( S is A -Sub_VERUM & S is Sub_negative ) & not ( S is A -Sub_VERUM & S is Sub_conjunctive ) & not ( S is A -Sub_VERUM & S is Sub_universal ) )

proof end;

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

ex F being Function of (QC-Sub-WFF F₁()),F₂() st
for S being Element of QC-Sub-WFF F₁()
for d1, d2 being Element of F₂() holds
( ( S is F₁() -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₇(F₁(),S,d1) ) )

proof end;

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

F₃() = F₄()

provided

A1: for S being Element of QC-Sub-WFF F₁()
for d1, d2 being Element of F₂() holds
( ( S is F₁() -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₉(F₁(),S,d1) ) ) and
A2: for S being Element of QC-Sub-WFF F₁()
for d1, d2 being Element of F₂() holds
( ( S is F₁() -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₉(F₁(),S,d1) ) )

proof end;

definition

let A be QC-alphabet ;
let S be Element of QC-Sub-WFF A;

func @ S -> Element of [:(QC-WFF A),(vSUB A):] equals :: SUBSTUT1:def 35
S;

proof end;

end;

:: deftheorem defines @ SUBSTUT1:def 35 :

definition

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

proof end;

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

proof end;

end;

definition

let A be QC-alphabet ;
let Z be Element of [:(QC-WFF A),(vSUB A):];

func S_Bound Z -> bound_QC-variable of A 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 A be QC-alphabet ;
let S be Element of QC-Sub-WFF A;
let p be QC-formula of A;

func Quant (S,p) -> Element of QC-WFF A equals :: SUBSTUT1:def 37
All ((S_Bound (@ S)),p);

end;

:: deftheorem defines Quant SUBSTUT1:def 37 :

Lm6: for A being QC-alphabet
for F1, F2 being Function of (QC-Sub-WFF A),(QC-WFF A) st ( for S being Element of QC-Sub-WFF A holds
( ( S is A -Sub_VERUM implies F1 . S = VERUM A ) & ( 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 A holds
( ( S is A -Sub_VERUM implies F2 . S = VERUM A ) & ( 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;

:: (Ebb et al, Chapter III, Definition 8.1/8.2)

definition

let A be QC-alphabet ;
let S be Element of QC-Sub-WFF A;

func CQC_Sub S -> Element of QC-WFF A means :Def38: :: SUBSTUT1:def 38
ex F being Function of (QC-Sub-WFF A),(QC-WFF A) st
( it = F . S & ( for S9 being Element of QC-Sub-WFF A holds
( ( S9 is A -Sub_VERUM implies F . S9 = VERUM A ) & ( 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))) ) ) ) );

proof end;

uniqueness by Lm6;

end;

:: deftheorem Def38 defines CQC_Sub SUBSTUT1:def 38 :

theorem Th28: :: SUBSTUT1:28

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

proof end;

theorem Th29: :: SUBSTUT1:29

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

proof end;

theorem Th30: :: SUBSTUT1:30

for A being QC-alphabet
for S being Element of QC-Sub-WFF A 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 A being QC-alphabet
for S1, S2 being Element of QC-Sub-WFF A st S1 `2 = S2 `2 holds
CQC_Sub (Sub_& (S1,S2)) = (CQC_Sub S1) '&' (CQC_Sub S2)

proof end;

theorem Th32: :: SUBSTUT1:32

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

proof end;

definition

let A be QC-alphabet ;

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

proof end;

end;

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

registration

let A be QC-alphabet ;

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