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


begin

definition
let A be QC-alphabet ;
func vSUB A ->  set  equals :: SUBSTUT1:def 1
 PFuncs ((bound_QC-variables A),(bound_QC-variables A));
coherence
 PFuncs ((bound_QC-variables A),(bound_QC-variables A)) is set ;
end;

:: deftheorem  defines vSUB SUBSTUT1:def_1_:_
 for A being QC-alphabet holds vSUB A = PFuncs ((bound_QC-variables A),(bound_QC-variables A));

registration
let A be QC-alphabet ;
cluster vSUB A ->  non empty ;
coherence
 not vSUB A is 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 ;
coherence
 vSUB A is 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
 Sub is PartFunc of (bound_QC-variables A),(bound_QC-variables A) by PARTFUN1:47;
end;

:: deftheorem  defines @ SUBSTUT1:def_2_:_
 for A being QC-alphabet
for Sub being CQC_Substitution of A holds @ Sub = Sub;

theorem Th1: :: SUBSTUT1:1
for A being QC-alphabet
for a being set
for Sub being CQC_Substitution of A st a in dom Sub holds
Sub . a in bound_QC-variables A
proofend;

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 &amp; ( for k being Element of NAT st 1 <= k &amp; k <= len l holds
( ( l . k in dom Sub implies it . k = Sub . (l . k) ) &amp; ( not l . k in dom Sub implies it . k = l . k ) ) ) );
existence
 ex b1 being FinSequence of QC-variables A st
( len b1 = len l &amp; ( for k being Element of NAT st 1 <= k &amp; k <= len l holds
( ( l . k in dom Sub implies b1 . k = Sub . (l . k) ) &amp; ( not l . k in dom Sub implies b1 . k = l . k ) ) ) )
proofend;
uniqueness
 for b1, b2 being FinSequence of QC-variables A st len b1 = len l &amp; ( for k being Element of NAT st 1 <= k &amp; k <= len l holds
( ( l . k in dom Sub implies b1 . k = Sub . (l . k) ) &amp; ( not l . k in dom Sub implies b1 . k = l . k ) ) ) &amp; len b2 = len l &amp; ( for k being Element of NAT st 1 <= k &amp; k <= len l holds
( ( l . k in dom Sub implies b2 . k = Sub . (l . k) ) &amp; ( not l . k in dom Sub implies b2 . k = l . k ) ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def3 defines CQC_Subst SUBSTUT1:def_3_:_
 for A being QC-alphabet
for l being FinSequence of QC-variables A
for Sub being CQC_Substitution of A
for b4 being FinSequence of QC-variables A holds
( b4 = CQC_Subst (l,Sub) iff ( len b4 = len l &amp; ( for k being Element of NAT st 1 <= k &amp; k <= len l holds
( ( l . k in dom Sub implies b4 . k = Sub . (l . k) ) &amp; ( not l . k in dom Sub implies b4 . k = l . k ) ) ) ) );

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;
coherence
 l is FinSequence of QC-variables A
proofend;
end;

:: deftheorem  defines @ SUBSTUT1:def_4_:_
 for A being QC-alphabet
for l being FinSequence of bound_QC-variables A holds @ l = l;

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);
coherence
 CQC_Subst ((@ l),Sub) is FinSequence of bound_QC-variables A
proofend;
end;

:: deftheorem  defines CQC_Subst SUBSTUT1:def_5_:_
 for A being QC-alphabet
for l being FinSequence of bound_QC-variables A
for Sub being CQC_Substitution of A holds CQC_Subst (l,Sub) = CQC_Subst ((@ l),Sub);

definition
let A be QC-alphabet ;
let Sub be CQC_Substitution of A;
let X be set ;
:: original:|
redefine funcSub | X ->  CQC_Substitution of A;
coherence
 Sub | X is CQC_Substitution of A
proofend;
end;

registration
let A be QC-alphabet ;
cluster Relation-like Function-like finite for Element of vSUB A;
existence
 ex b1 being CQC_Substitution of A st b1 is finite
proofend;
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 &amp; y is Element of dom Sub &amp; y <> x &amp; y <> Sub . y )  }  ;
coherence
 Sub |  {  y where y is bound_QC-variable of A : ( y in still_not-bound_in p &amp; y is Element of dom Sub &amp; y <> x &amp; y <> Sub . y )  }  is finite CQC_Substitution of A
proofend;
end;

:: deftheorem  defines RestrictSub SUBSTUT1:def_6_:_
 for A being QC-alphabet
for x being bound_QC-variable of A
for p being QC-formula of A
for Sub being CQC_Substitution of A holds RestrictSub (x,p,Sub) = Sub |  {  y where y is bound_QC-variable of A : ( y in still_not-bound_in p &amp; y is Element of dom Sub &amp; y <> x &amp; y <> Sub . y )  }  ;

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 Element of NAT : ( 1 <= k &amp; k <= len l1 &amp; l1 . k in bound_QC-variables A )  }  ;
coherence
  {  (l1 . k) where k is Element of NAT : ( 1 <= k &amp; k <= len l1 &amp; l1 . k in bound_QC-variables A )  }  is Subset of (bound_QC-variables A)
proofend;
end;

:: deftheorem  defines Bound_Vars SUBSTUT1:def_7_:_
 for A being QC-alphabet
for l1 being FinSequence of QC-variables A holds Bound_Vars l1 =  {  (l1 . k) where k is Element of NAT : ( 1 <= k &amp; k <= len l1 &amp; l1 . k in bound_QC-variables A )  }  ;

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 &amp; ( 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) ) &amp; ( p is atomic implies F . p = Bound_Vars (the_arguments_of p) ) &amp; ( p is negative &amp; d1 = F . (the_argument_of p) implies F . p = d1 ) &amp; ( p is conjunctive &amp; d1 = F . (the_left_argument_of p) &amp; d2 = F . (the_right_argument_of p) implies F . p = d1 \/ d2 ) &amp; ( p is universal &amp; d1 = F . (the_scope_of p) implies F . p = d1 \/ {(bound_in p)} ) ) ) );
correctness
existence
ex b1 being Subset of (bound_QC-variables A) ex F being Function of (QC-WFF A),(bool (bound_QC-variables A)) st
( b1 = F . p &amp; ( 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) ) &amp; ( p is atomic implies F . p = Bound_Vars (the_arguments_of p) ) &amp; ( p is negative &amp; d1 = F . (the_argument_of p) implies F . p = d1 ) &amp; ( p is conjunctive &amp; d1 = F . (the_left_argument_of p) &amp; d2 = F . (the_right_argument_of p) implies F . p = d1 \/ d2 ) &amp; ( p is universal &amp; d1 = F . (the_scope_of p) implies F . p = d1 \/ {(bound_in p)} ) ) ) );
uniqueness
for b1, b2 being Subset of (bound_QC-variables A) st ex F being Function of (QC-WFF A),(bool (bound_QC-variables A)) st
( b1 = F . p &amp; ( 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) ) &amp; ( p is atomic implies F . p = Bound_Vars (the_arguments_of p) ) &amp; ( p is negative &amp; d1 = F . (the_argument_of p) implies F . p = d1 ) &amp; ( p is conjunctive &amp; d1 = F . (the_left_argument_of p) &amp; d2 = F . (the_right_argument_of p) implies F . p = d1 \/ d2 ) &amp; ( p is universal &amp; d1 = F . (the_scope_of p) implies F . p = d1 \/ {(bound_in p)} ) ) ) ) &amp; ex F being Function of (QC-WFF A),(bool (bound_QC-variables A)) st
( b2 = F . p &amp; ( 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) ) &amp; ( p is atomic implies F . p = Bound_Vars (the_arguments_of p) ) &amp; ( p is negative &amp; d1 = F . (the_argument_of p) implies F . p = d1 ) &amp; ( p is conjunctive &amp; d1 = F . (the_left_argument_of p) &amp; d2 = F . (the_right_argument_of p) implies F . p = d1 \/ d2 ) &amp; ( p is universal &amp; d1 = F . (the_scope_of p) implies F . p = d1 \/ {(bound_in p)} ) ) ) ) holds
b1 = b2;
proofend;
end;

:: deftheorem Def8 defines Bound_Vars SUBSTUT1:def_8_:_
 for A being QC-alphabet
for p being QC-formula of A
for b3 being Subset of (bound_QC-variables A) holds
( b3 = Bound_Vars p iff ex F being Function of (QC-WFF A),(bool (bound_QC-variables A)) st
( b3 = F . p &amp; ( 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) ) &amp; ( p is atomic implies F . p = Bound_Vars (the_arguments_of p) ) &amp; ( p is negative &amp; d1 = F . (the_argument_of p) implies F . p = d1 ) &amp; ( p is conjunctive &amp; d1 = F . (the_left_argument_of p) &amp; d2 = F . (the_right_argument_of p) implies F . p = d1 \/ d2 ) &amp; ( p is universal &amp; d1 = F . (the_scope_of p) implies F . p = d1 \/ {(bound_in p)} ) ) ) ) );

Lm1:  for A being QC-alphabet
for p being QC-formula of A holds
( Bound_Vars (VERUM A) = {} (bound_QC-variables A) &amp; ( p is atomic implies Bound_Vars p = Bound_Vars (the_arguments_of p) ) &amp; ( p is negative implies Bound_Vars p = Bound_Vars (the_argument_of p) ) &amp; ( p is conjunctive implies Bound_Vars p = (Bound_Vars (the_left_argument_of p)) \/ (Bound_Vars (the_right_argument_of p)) ) &amp; ( p is universal implies Bound_Vars p = (Bound_Vars (the_scope_of p)) \/ {(bound_in p)} ) )
proofend;

theorem Th2: :: SUBSTUT1:2
for A being QC-alphabet holds Bound_Vars (VERUM A) = {}
proofend;

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 ;
coherence
 Bound_Vars p is finite
proofend;
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  }  ;
coherence
  {  s where s is QC-symbol of A : x. s in Bound_Vars p  }  is finite Subset of (QC-symbols A)
proofend;
end;

:: deftheorem  defines Dom_Bound_Vars SUBSTUT1:def_9_:_
 for A being QC-alphabet
for p being QC-formula of A holds Dom_Bound_Vars p =  {  s where s is QC-symbol of A : x. s in Bound_Vars p  }  ;

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  }  ;
coherence
  {  s where s is QC-symbol of A : x. s in rng finSub  }  is finite Subset of (QC-symbols A)
proofend;
end;

:: deftheorem  defines Sub_Var SUBSTUT1:def_10_:_
 for A being QC-alphabet
for finSub being finite CQC_Substitution of A holds Sub_Var finSub =  {  s where s is QC-symbol of A : x. s in rng finSub  }  ;

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

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));
coherence
 NAT \ ((Dom_Bound_Vars p) \/ (Sub_Var finSub)) is non empty Subset of (QC-symbols A)
proofend;
end;

:: deftheorem  defines NSub SUBSTUT1:def_11_:_
 for A being QC-alphabet
for p being QC-formula of A
for finSub being finite CQC_Substitution of A holds NSub (p,finSub) = NAT \ ((Dom_Bound_Vars p) \/ (Sub_Var finSub));

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);
coherence
 the Element of NSub (p,finSub) is QC-symbol of A ;
end;

:: deftheorem  defines upVar SUBSTUT1:def_12_:_
 for A being QC-alphabet
for finSub being finite CQC_Substitution of A
for p being QC-formula of A holds upVar (finSub,p) = the Element of NSub (p,finSub);

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]};
coherence
 ( ( x in rng finSub implies finSub \/ {[x,(x. (upVar (finSub,p)))]} is CQC_Substitution of A ) &amp; ( not x in rng finSub implies finSub \/ {[x,x]} is CQC_Substitution of A ) )
proofend;
consistency
 for b1 being CQC_Substitution of A holds verum ;
end;

:: deftheorem  defines ExpandSub SUBSTUT1:def_13_:_
 for A being QC-alphabet
for x being bound_QC-variable of A
for p being QC-formula of A
for finSub being finite CQC_Substitution of A st ex Sub being CQC_Substitution of A st finSub = RestrictSub (x,(All (x,p)),Sub) holds
( ( x in rng finSub implies ExpandSub (x,p,finSub) = finSub \/ {[x,(x. (upVar (finSub,p)))]} ) &amp; ( not x in rng finSub implies ExpandSub (x,p,finSub) = finSub \/ {[x,x]} ) );

definition
let A be QC-alphabet ;
let p be QC-formula of A;
let Sub be CQC_Substitution of A;
let b be set ;
predp,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))) ) &amp; ( not p is universal implies b = {} ) );
end;

:: deftheorem Def14 defines PQSub SUBSTUT1:def_14_:_
 for A being QC-alphabet
for p being QC-formula of A
for Sub being CQC_Substitution of A
for b being set holds
( p,Sub PQSub b iff ( ( p is universal implies b = ExpandSub ((bound_in p),(the_scope_of p),(RestrictSub ((bound_in p),p,Sub))) ) &amp; ( not p is universal implies b = {} ) ) );

definition
let A be QC-alphabet ;
func QSub A ->  Function means :: SUBSTUT1:def 15
 for a being set holds
( a in it iff ex p being QC-formula of A ex Sub being CQC_Substitution of A ex b being set st
( a = [[p,Sub],b] &amp; p,Sub PQSub b ) );
existence
 ex b1 being Function st
for a being set holds
( a in b1 iff ex p being QC-formula of A ex Sub being CQC_Substitution of A ex b being set st
( a = [[p,Sub],b] &amp; p,Sub PQSub b ) )
proofend;
uniqueness
 for b1, b2 being Function st ( for a being set holds
( a in b1 iff ex p being QC-formula of A ex Sub being CQC_Substitution of A ex b being set st
( a = [[p,Sub],b] &amp; p,Sub PQSub b ) ) ) &amp; ( for a being set holds
( a in b2 iff ex p being QC-formula of A ex Sub being CQC_Substitution of A ex b being set st
( a = [[p,Sub],b] &amp; p,Sub PQSub b ) ) ) holds
b1 = b2
proofend;
end;

:: deftheorem  defines QSub SUBSTUT1:def_15_:_
 for A being QC-alphabet
for b2 being Function holds
( b2 = QSub A iff for a being set holds
( a in b2 iff ex p being QC-formula of A ex Sub being CQC_Substitution of A ex b being set st
( a = [[p,Sub],b] &amp; p,Sub PQSub b ) ) );

begin

theorem Th7: :: SUBSTUT1:7
for A being QC-alphabet holds
( [:(QC-WFF A),(vSUB A):] is Subset of [:([:NAT,(QC-symbols A):] *),(vSUB A):] &amp; ( for k being Element of 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):] ) &amp; ( for e being Element of vSUB A holds [<*[0,0]*>,e] in [:(QC-WFF A),(vSUB A):] ) &amp; ( 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):] ) &amp; ( 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):] &amp; [q,e] in [:(QC-WFF A),(vSUB A):] holds
[((<*[2,0]*> ^ p) ^ q),e] in [:(QC-WFF A),(vSUB A):] ) &amp; ( 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):] ) )
proofend;

definition
let A be QC-alphabet ;
let IT be set ;
attrIT is A -Sub-closed  means :Def16: :: SUBSTUT1:def 16
( IT is Subset of [:([:NAT,(QC-symbols A):] *),(vSUB A):] &amp; ( for k being Element of 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 ) &amp; ( for e being Element of vSUB A holds [<*[0,0]*>,e] in IT ) &amp; ( 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 ) &amp; ( for p, q being FinSequence of [:NAT,(QC-symbols A):]
for e being Element of vSUB A st [p,e] in IT &amp; [q,e] in IT holds
[((<*[2,0]*> ^ p) ^ q),e] in IT ) &amp; ( 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_:_
 for A being QC-alphabet
for IT being set holds
( IT is A -Sub-closed iff ( IT is Subset of [:([:NAT,(QC-symbols A):] *),(vSUB A):] &amp; ( for k being Element of 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 ) &amp; ( for e being Element of vSUB A holds [<*[0,0]*>,e] in IT ) &amp; ( 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 ) &amp; ( for p, q being FinSequence of [:NAT,(QC-symbols A):]
for e being Element of vSUB A st [p,e] in IT &amp; [q,e] in IT holds
[((<*[2,0]*> ^ p) ^ q),e] in IT ) &amp; ( 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 ) ) );

registration
let A be QC-alphabet ;
cluster non empty A -Sub-closed for set ;
existence
 ex b1 being set st
( b1 is A -Sub-closed &amp; not b1 is empty )
proofend;
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):]
proofend;

Lm4:  for A being QC-alphabet
for k being Element of 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):]
proofend;

Lm5:  for A being QC-alphabet
for k being Element of 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):]
proofend;

definition
let A be QC-alphabet ;
func QC-Sub-WFF A ->  non empty set  means :Def17: :: SUBSTUT1:def 17
( it is A -Sub-closed &amp; ( for D being non empty set st D is A -Sub-closed holds
it c= D ) );
existence
 ex b1 being non empty set st
( b1 is A -Sub-closed &amp; ( for D being non empty set st D is A -Sub-closed holds
b1 c= D ) )
proofend;
uniqueness
 for b1, b2 being non empty set st b1 is A -Sub-closed &amp; ( for D being non empty set st D is A -Sub-closed holds
b1 c= D ) &amp; b2 is A -Sub-closed &amp; ( for D being non empty set st D is A -Sub-closed holds
b2 c= D ) holds
b1 = b2
proofend;
end;

:: deftheorem Def17 defines QC-Sub-WFF SUBSTUT1:def_17_:_
 for A being QC-alphabet
for b2 being non empty set holds
( b2 = QC-Sub-WFF A iff ( b2 is A -Sub-closed &amp; ( for D being non empty set st D is A -Sub-closed holds
b2 c= D ) ) );

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]
proofend;

registration
let A be QC-alphabet ;
cluster QC-Sub-WFF A ->  non empty A -Sub-closed ;
coherence
 QC-Sub-WFF A is A -Sub-closed 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];
coherence
 [(P ! l),e] is Element of QC-Sub-WFF A
proofend;
end;

:: deftheorem Def18 defines Sub_P SUBSTUT1:def_18_:_
 for A being QC-alphabet
for P being QC-pred_symbol of A
for l being FinSequence of QC-variables A
for e being Element of vSUB A st the_arity_of P = len l holds
Sub_P (P,l,e) = [(P ! l),e];

theorem Th9: :: SUBSTUT1:9
for A being QC-alphabet
for e being Element of vSUB A
for k being Element of 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]
proofend;

definition
let A be QC-alphabet ;
let S be Element of QC-Sub-WFF A;
attrS is A -Sub_VERUM  means :Def19: :: SUBSTUT1:def 19
 ex e being Element of vSUB A st S = [(VERUM A),e];
end;

:: deftheorem Def19 defines -Sub_VERUM SUBSTUT1:def_19_:_
 for A being QC-alphabet
for S being Element of QC-Sub-WFF A holds
( S is A -Sub_VERUM iff ex e being Element of vSUB A st S = [(VERUM A),e] );

definition
let A be QC-alphabet ;
let S be Element of QC-Sub-WFF A;
:: original:`1
redefine funcS `1  ->  Element of QC-WFF A;
coherence
 S `1 is Element of QC-WFF A
proofend;
:: original:`2
redefine funcS `2  ->  Element of vSUB A;
coherence
 S `2 is Element of vSUB A
proofend;
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)]
proofend;

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)];
coherence
 [('not' (S `1)),(S `2)] is Element of QC-Sub-WFF A
proofend;
end;

:: deftheorem  defines Sub_not SUBSTUT1:def_20_:_
 for A being QC-alphabet
for S being Element of QC-Sub-WFF A holds Sub_not S = [('not' (S `1)),(S `2)];

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

:: deftheorem Def21 defines Sub_&amp; SUBSTUT1:def_21_:_
 for A being QC-alphabet
for S, S9 being Element of QC-Sub-WFF A st S `2 = S9 `2 holds
Sub_&amp; (S,S9) = [((S `1) '&amp;' (S9 `1)),(S `2)];

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

definition
let A be QC-alphabet ;
let B be Element of [:(QC-Sub-WFF A),(bound_QC-variables A):];
attrB is quantifiable  means :Def22: :: 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 Def22 defines quantifiable SUBSTUT1:def_22_:_
 for A being QC-alphabet
for B being Element of [:(QC-Sub-WFF A),(bound_QC-variables A):] holds
( B is quantifiable iff ex e being Element of vSUB A st (B `1) `2 = (QSub A) . [(All ((B `2),((B `1) `1))),e] );

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
 ex b1 being Element of vSUB A st (B `1) `2 = (QSub A) . [(All ((B `2),((B `1) `1))),b1] by A1, Def22;
end;

:: deftheorem Def23 defines second_Q_comp SUBSTUT1:def_23_:_
 for A being QC-alphabet
for B being Element of [:(QC-Sub-WFF A),(bound_QC-variables A):] st B is quantifiable holds
for b3 being Element of vSUB A holds
( b3 is second_Q_comp of B iff (B `1) `2 = (QSub A) . [(All ((B `2),((B `1) `1))),b3] );

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];
coherence
 [(All ((B `2),((B `1) `1))),SQ] is Element of QC-Sub-WFF A
proofend;
end;

:: deftheorem Def24 defines Sub_All SUBSTUT1:def_24_:_
 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) = [(All ((B `2),((B `1) `1))),SQ];

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
 [S,x] is Element of [:(QC-Sub-WFF A),(bound_QC-variables A):]
proofend;
end;

scheme :: SUBSTUT1:sch 1
SubQCInd{ F1() ->  QC-alphabet , P1[ Element of QC-Sub-WFF F1()] } :
 for S being Element of QC-Sub-WFF F1() holds P1[S]
provided
A1: for k being Element of NAT
for P being QC-pred_symbol of k,F1()
for ll being QC-variable_list of k,F1()
for e being Element of vSUB F1() holds P1[ Sub_P (P,ll,e)] and
A2: for S being Element of QC-Sub-WFF F1() st S is F1() -Sub_VERUM holds
P1[S] and
A3: for S being Element of QC-Sub-WFF F1() st P1[S] holds
P1[ Sub_not S] and
A4: for S, S9 being Element of QC-Sub-WFF F1() st S `2 = S9 `2 &amp; P1[S] &amp; P1[S9] holds
P1[ Sub_&amp; (S,S9)] and
A5: for x being bound_QC-variable of F1()
for S being Element of QC-Sub-WFF F1()
for SQ being second_Q_comp of [S,x] st [S,x] is quantifiable &amp; P1[S] holds
P1[ Sub_All ([S,x],SQ)]
proofend;

definition
let A be QC-alphabet ;
let S be Element of QC-Sub-WFF A;
attrS is Sub_atomic  means :Def25: :: SUBSTUT1:def 25
 ex k being Element of 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 Def25 defines Sub_atomic SUBSTUT1:def_25_:_
 for A being QC-alphabet
for S being Element of QC-Sub-WFF A holds
( S is Sub_atomic iff ex k being Element of 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) );

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
proofend;

registration
let A be QC-alphabet ;
let k be Element of 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 ;
coherence
 Sub_P (P,ll,e) is Sub_atomic by Def25;
end;

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

:: deftheorem Def26 defines Sub_negative SUBSTUT1:def_26_:_
 for A being QC-alphabet
for S being Element of QC-Sub-WFF A holds
( S is Sub_negative iff ex S9 being Element of QC-Sub-WFF A st S = Sub_not S9 );

:: deftheorem Def27 defines Sub_conjunctive SUBSTUT1:def_27_:_
 for A being QC-alphabet
for S being Element of QC-Sub-WFF A holds
( S is Sub_conjunctive iff ex S1, S2 being Element of QC-Sub-WFF A st
( S = Sub_&amp; (S1,S2) &amp; S1 `2 = S2 `2 ) );

definition
let A be QC-alphabet ;
let S be Element of QC-Sub-WFF A;
attrS 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) &amp; B is quantifiable );
end;

:: deftheorem Def28 defines Sub_universal SUBSTUT1:def_28_:_
 for A being QC-alphabet
for S being Element of QC-Sub-WFF A holds
( S is Sub_universal iff 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) &amp; B is quantifiable ) );

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 )
proofend;

definition
let A be QC-alphabet ;
let S be Element of QC-Sub-WFF A;
assume B1: S is Sub_atomic ;
func Sub_the_arguments_of S ->  FinSequence of QC-variables A means :Def29: :: SUBSTUT1:def 29
 ex k being Element of 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 &amp; S = Sub_P (P,ll,e) );
existence
 ex b1 being FinSequence of QC-variables A ex k being Element of 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
( b1 = ll &amp; S = Sub_P (P,ll,e) )
proofend;
uniqueness
 for b1, b2 being FinSequence of QC-variables A st ex k being Element of 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
( b1 = ll &amp; S = Sub_P (P,ll,e) ) &amp; ex k being Element of 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
( b2 = ll &amp; S = Sub_P (P,ll,e) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def29 defines Sub_the_arguments_of SUBSTUT1:def_29_:_
 for A being QC-alphabet
for S being Element of QC-Sub-WFF A st S is Sub_atomic holds
for b3 being FinSequence of QC-variables A holds
( b3 = Sub_the_arguments_of S iff ex k being Element of 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
( b3 = ll &amp; S = Sub_P (P,ll,e) ) );

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;
existence
 ex b1 being Element of QC-Sub-WFF A st S = Sub_not b1 by A1, Def26;
uniqueness
 for b1, b2 being Element of QC-Sub-WFF A st S = Sub_not b1 &amp; S = Sub_not b2 holds
b1 = b2
proofend;
end;

:: deftheorem Def30 defines Sub_the_argument_of SUBSTUT1:def_30_:_
 for A being QC-alphabet
for S being Element of QC-Sub-WFF A st S is Sub_negative holds
for b3 being Element of QC-Sub-WFF A holds
( b3 = Sub_the_argument_of S iff S = Sub_not b3 );

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_&amp; (it,S9) &amp; it `2 = S9 `2 );
existence
 ex b1, S9 being Element of QC-Sub-WFF A st
( S = Sub_&amp; (b1,S9) &amp; b1 `2 = S9 `2 ) by A1, Def27;
uniqueness
 for b1, b2 being Element of QC-Sub-WFF A st ex S9 being Element of QC-Sub-WFF A st
( S = Sub_&amp; (b1,S9) &amp; b1 `2 = S9 `2 ) &amp; ex S9 being Element of QC-Sub-WFF A st
( S = Sub_&amp; (b2,S9) &amp; b2 `2 = S9 `2 ) holds
b1 = b2
proofend;
end;

:: deftheorem Def31 defines Sub_the_left_argument_of SUBSTUT1:def_31_:_
 for A being QC-alphabet
for S being Element of QC-Sub-WFF A st S is Sub_conjunctive holds
for b3 being Element of QC-Sub-WFF A holds
( b3 = Sub_the_left_argument_of S iff ex S9 being Element of QC-Sub-WFF A st
( S = Sub_&amp; (b3,S9) &amp; b3 `2 = S9 `2 ) );

definition
let A be QC-alphabet ;
let S be Element of QC-Sub-WFF A;
assume B1: 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_&amp; (S9,it) &amp; S9 `2 = it `2 );
existence
 ex b1, S9 being Element of QC-Sub-WFF A st
( S = Sub_&amp; (S9,b1) &amp; S9 `2 = b1 `2 )
proofend;
uniqueness
 for b1, b2 being Element of QC-Sub-WFF A st ex S9 being Element of QC-Sub-WFF A st
( S = Sub_&amp; (S9,b1) &amp; S9 `2 = b1 `2 ) &amp; ex S9 being Element of QC-Sub-WFF A st
( S = Sub_&amp; (S9,b2) &amp; S9 `2 = b2 `2 ) holds
b1 = b2
proofend;
end;

:: deftheorem Def32 defines Sub_the_right_argument_of SUBSTUT1:def_32_:_
 for A being QC-alphabet
for S being Element of QC-Sub-WFF A st S is Sub_conjunctive holds
for b3 being Element of QC-Sub-WFF A holds
( b3 = Sub_the_right_argument_of S iff ex S9 being Element of QC-Sub-WFF A st
( S = Sub_&amp; (S9,b3) &amp; S9 `2 = b3 `2 ) );

definition
let A be QC-alphabet ;
let S be Element of QC-Sub-WFF A;
assume B1: 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) &amp; B `2 = it &amp; B is quantifiable );
existence
 ex b1 being bound_QC-variable of A 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) &amp; B `2 = b1 &amp; B is quantifiable )
proofend;
uniqueness
 for b1, b2 being bound_QC-variable of A st 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) &amp; B `2 = b1 &amp; B is quantifiable ) &amp; 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) &amp; B `2 = b2 &amp; B is quantifiable ) holds
b1 = b2
proofend;
end;

:: deftheorem  defines Sub_the_bound_of SUBSTUT1:def_33_:_
 for A being QC-alphabet
for S being Element of QC-Sub-WFF A st S is Sub_universal holds
for b3 being bound_QC-variable of A holds
( b3 = Sub_the_bound_of S iff 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) &amp; B `2 = b3 &amp; B is quantifiable ) );

definition
let A be QC-alphabet ;
let A2 be Element of QC-Sub-WFF A;
assume B1: 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) &amp; B `1 = it &amp; B is quantifiable );
existence
 ex b1 being Element of QC-Sub-WFF A 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) &amp; B `1 = b1 &amp; B is quantifiable )
proofend;
uniqueness
 for b1, b2 being Element of QC-Sub-WFF A st 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) &amp; B `1 = b1 &amp; B is quantifiable ) &amp; 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) &amp; B `1 = b2 &amp; B is quantifiable ) holds
b1 = b2
proofend;
end;

:: deftheorem Def34 defines Sub_the_scope_of SUBSTUT1:def_34_:_
 for A being QC-alphabet
for A2 being Element of QC-Sub-WFF A st A2 is Sub_universal holds
for b3 being Element of QC-Sub-WFF A holds
( b3 = Sub_the_scope_of A2 iff 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) &amp; B `1 = b3 &amp; B is quantifiable ) );

registration
let A be QC-alphabet ;
let S be Element of QC-Sub-WFF A;
cluster Sub_not S ->  Sub_negative ;
coherence
 Sub_not S is Sub_negative
proofend;
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_&amp; (S1,S2) is Sub_conjunctive
proofend;

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
proofend;

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
proofend;

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 &amp; S19 `2 = S29 `2 &amp; Sub_&amp; (S1,S2) = Sub_&amp; (S19,S29) holds
( S1 = S19 &amp; S2 = S29 )
proofend;

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_&amp; (S1,S2)) = S1
proofend;

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_&amp; (S1,S2)) = S2
proofend;

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 &amp; B2 is quantifiable &amp; Sub_All (B1,SQ1) = Sub_All (B2,SQ2) holds
B1 = B2
proofend;

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
proofend;

scheme :: SUBSTUT1:sch 2
SubQCInd2{ F1() ->  QC-alphabet , P1[ Element of QC-Sub-WFF F1()] } :
 for S being Element of QC-Sub-WFF F1() holds P1[S]
provided
A1: for S being Element of QC-Sub-WFF F1() holds
( ( S is Sub_atomic implies P1[S] ) &amp; ( S is F1() -Sub_VERUM implies P1[S] ) &amp; ( S is Sub_negative &amp; P1[ Sub_the_argument_of S] implies P1[S] ) &amp; ( S is Sub_conjunctive &amp; P1[ Sub_the_left_argument_of S] &amp; P1[ Sub_the_right_argument_of S] implies P1[S] ) &amp; ( S is Sub_universal &amp; P1[ Sub_the_scope_of S] implies P1[S] ) )
proofend;

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))
proofend;

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)) &amp; len (@ ((Sub_the_right_argument_of S) `1)) < len (@ (S `1)) )
proofend;

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))
proofend;

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 ) &amp; ( S is Sub_atomic implies ex k being Element of NAT st (@ (S `1)) . 1 is QC-pred_symbol of k,A ) &amp; ( S is Sub_negative implies ((@ (S `1)) . 1) `1 = 1 ) &amp; ( S is Sub_conjunctive implies ((@ (S `1)) . 1) `1 = 2 ) &amp; ( S is Sub_universal implies ((@ (S `1)) . 1) `1 = 3 ) )
proofend;

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 &amp; ((@ (S `1)) . 1) `1 <> 1 &amp; ((@ (S `1)) . 1) `1 <> 2 &amp; ((@ (S `1)) . 1) `1 <> 3 )
proofend;

theorem Th27: :: SUBSTUT1:27
for A being QC-alphabet
for S being Element of QC-Sub-WFF A holds
( not ( S is Sub_atomic &amp; S is Sub_negative ) &amp; not ( S is Sub_atomic &amp; S is Sub_conjunctive ) &amp; not ( S is Sub_atomic &amp; S is Sub_universal ) &amp; not ( S is Sub_negative &amp; S is Sub_conjunctive ) &amp; not ( S is Sub_negative &amp; S is Sub_universal ) &amp; not ( S is Sub_conjunctive &amp; S is Sub_universal ) &amp; not ( S is A -Sub_VERUM &amp; S is Sub_atomic ) &amp; not ( S is A -Sub_VERUM &amp; S is Sub_negative ) &amp; not ( S is A -Sub_VERUM &amp; S is Sub_conjunctive ) &amp; not ( S is A -Sub_VERUM &amp; S is Sub_universal ) )
proofend;

scheme :: SUBSTUT1:sch 3
SubFuncEx{ F1() ->  QC-alphabet , F2() ->  non empty set , F3() ->  Element of F2(), F4( Element of QC-Sub-WFF F1()) ->  Element of F2(), F5( Element of F2()) ->  Element of F2(), F6( Element of F2(), Element of F2()) ->  Element of F2(), F7( set , Element of QC-Sub-WFF F1(), Element of F2()) ->  Element of F2() } :
 ex F being Function of (QC-Sub-WFF F1()),F2() st
for S being Element of QC-Sub-WFF F1()
for d1, d2 being Element of F2() holds
( ( S is F1() -Sub_VERUM implies F . S = F3() ) &amp; ( S is Sub_atomic implies F . S = F4(S) ) &amp; ( S is Sub_negative &amp; d1 = F . (Sub_the_argument_of S) implies F . S = F5(d1) ) &amp; ( S is Sub_conjunctive &amp; d1 = F . (Sub_the_left_argument_of S) &amp; d2 = F . (Sub_the_right_argument_of S) implies F . S = F6(d1,d2) ) &amp; ( S is Sub_universal &amp; d1 = F . (Sub_the_scope_of S) implies F . S = F7(F1(),S,d1) ) )
proofend;

scheme :: SUBSTUT1:sch 4
SubQCFuncUniq{ F1() ->  QC-alphabet , F2() ->  non empty set , F3() ->  Function of (QC-Sub-WFF F1()),F2(), F4() ->  Function of (QC-Sub-WFF F1()),F2(), F5() ->  Element of F2(), F6( set ) ->  Element of F2(), F7( set ) ->  Element of F2(), F8( set , set ) ->  Element of F2(), F9( set , set , set ) ->  Element of F2() } :
 F3() = F4()
provided
A1: for S being Element of QC-Sub-WFF F1()
for d1, d2 being Element of F2() holds
( ( S is F1() -Sub_VERUM implies F3() . S = F5() ) &amp; ( S is Sub_atomic implies F3() . S = F6(S) ) &amp; ( S is Sub_negative &amp; d1 = F3() . (Sub_the_argument_of S) implies F3() . S = F7(d1) ) &amp; ( S is Sub_conjunctive &amp; d1 = F3() . (Sub_the_left_argument_of S) &amp; d2 = F3() . (Sub_the_right_argument_of S) implies F3() . S = F8(d1,d2) ) &amp; ( S is Sub_universal &amp; d1 = F3() . (Sub_the_scope_of S) implies F3() . S = F9(F1(),S,d1) ) ) and
A2: for S being Element of QC-Sub-WFF F1()
for d1, d2 being Element of F2() holds
( ( S is F1() -Sub_VERUM implies F4() . S = F5() ) &amp; ( S is Sub_atomic implies F4() . S = F6(S) ) &amp; ( S is Sub_negative &amp; d1 = F4() . (Sub_the_argument_of S) implies F4() . S = F7(d1) ) &amp; ( S is Sub_conjunctive &amp; d1 = F4() . (Sub_the_left_argument_of S) &amp; d2 = F4() . (Sub_the_right_argument_of S) implies F4() . S = F8(d1,d2) ) &amp; ( S is Sub_universal &amp; d1 = F4() . (Sub_the_scope_of S) implies F4() . S = F9(F1(),S,d1) ) )
proofend;

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;
coherence
 S is Element of [:(QC-WFF A),(vSUB A):]
proofend;
end;

:: deftheorem  defines @ SUBSTUT1:def_35_:_
 for A being QC-alphabet
for S being Element of QC-Sub-WFF A holds @ S = S;

definition
let A be QC-alphabet ;
let Z be Element of [:(QC-WFF A),(vSUB A):];
:: original:`1
redefine funcZ `1  ->  Element of QC-WFF A;
coherence
 Z `1 is Element of QC-WFF A
proofend;
:: original:`2
redefine funcZ `2  ->  CQC_Substitution of A;
coherence
 Z `2 is CQC_Substitution of A
proofend;
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
 ( ( bound_in (Z `1) in rng (RestrictSub ((bound_in (Z `1)),(Z `1),(Z `2))) implies x. (upVar ((RestrictSub ((bound_in (Z `1)),(Z `1),(Z `2))),(the_scope_of (Z `1)))) is bound_QC-variable of A ) &amp; ( not bound_in (Z `1) in rng (RestrictSub ((bound_in (Z `1)),(Z `1),(Z `2))) implies bound_in (Z `1) is bound_QC-variable of A ) ) ;
consistency
 for b1 being bound_QC-variable of A holds verum ;
end;

:: deftheorem  defines S_Bound SUBSTUT1:def_36_:_
 for A being QC-alphabet
for Z being Element of [:(QC-WFF A),(vSUB A):] holds
( ( bound_in (Z `1) in rng (RestrictSub ((bound_in (Z `1)),(Z `1),(Z `2))) implies S_Bound Z = x. (upVar ((RestrictSub ((bound_in (Z `1)),(Z `1),(Z `2))),(the_scope_of (Z `1)))) ) &amp; ( not bound_in (Z `1) in rng (RestrictSub ((bound_in (Z `1)),(Z `1),(Z `2))) implies S_Bound Z = bound_in (Z `1) ) );

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);
coherence
 All ((S_Bound (@ S)),p) is Element of QC-WFF A ;
end;

:: deftheorem  defines Quant SUBSTUT1:def_37_:_
 for A being QC-alphabet
for S being Element of QC-Sub-WFF A
for p being QC-formula of A holds Quant (S,p) = All ((S_Bound (@ S)),p);

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 ) &amp; ( S is Sub_atomic implies F1 . S = (the_pred_symbol_of (S `1)) ! (CQC_Subst ((Sub_the_arguments_of S),(S `2))) ) &amp; ( S is Sub_negative implies F1 . S = 'not' (F1 . (Sub_the_argument_of S)) ) &amp; ( S is Sub_conjunctive implies F1 . S = (F1 . (Sub_the_left_argument_of S)) '&amp;' (F1 . (Sub_the_right_argument_of S)) ) &amp; ( S is Sub_universal implies F1 . S = Quant (S,(F1 . (Sub_the_scope_of S))) ) ) ) &amp; ( for S being Element of QC-Sub-WFF A holds
( ( S is A -Sub_VERUM implies F2 . S = VERUM A ) &amp; ( S is Sub_atomic implies F2 . S = (the_pred_symbol_of (S `1)) ! (CQC_Subst ((Sub_the_arguments_of S),(S `2))) ) &amp; ( S is Sub_negative implies F2 . S = 'not' (F2 . (Sub_the_argument_of S)) ) &amp; ( S is Sub_conjunctive implies F2 . S = (F2 . (Sub_the_left_argument_of S)) '&amp;' (F2 . (Sub_the_right_argument_of S)) ) &amp; ( S is Sub_universal implies F2 . S = Quant (S,(F2 . (Sub_the_scope_of S))) ) ) ) holds
F1 = F2
proofend;

begin

:: (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 &amp; ( for S9 being Element of QC-Sub-WFF A holds
( ( S9 is A -Sub_VERUM implies F . S9 = VERUM A ) &amp; ( S9 is Sub_atomic implies F . S9 = (the_pred_symbol_of (S9 `1)) ! (CQC_Subst ((Sub_the_arguments_of S9),(S9 `2))) ) &amp; ( S9 is Sub_negative implies F . S9 = 'not' (F . (Sub_the_argument_of S9)) ) &amp; ( S9 is Sub_conjunctive implies F . S9 = (F . (Sub_the_left_argument_of S9)) '&amp;' (F . (Sub_the_right_argument_of S9)) ) &amp; ( S9 is Sub_universal implies F . S9 = Quant (S9,(F . (Sub_the_scope_of S9))) ) ) ) );
existence
 ex b1 being Element of QC-WFF A ex F being Function of (QC-Sub-WFF A),(QC-WFF A) st
( b1 = F . S &amp; ( for S9 being Element of QC-Sub-WFF A holds
( ( S9 is A -Sub_VERUM implies F . S9 = VERUM A ) &amp; ( S9 is Sub_atomic implies F . S9 = (the_pred_symbol_of (S9 `1)) ! (CQC_Subst ((Sub_the_arguments_of S9),(S9 `2))) ) &amp; ( S9 is Sub_negative implies F . S9 = 'not' (F . (Sub_the_argument_of S9)) ) &amp; ( S9 is Sub_conjunctive implies F . S9 = (F . (Sub_the_left_argument_of S9)) '&amp;' (F . (Sub_the_right_argument_of S9)) ) &amp; ( S9 is Sub_universal implies F . S9 = Quant (S9,(F . (Sub_the_scope_of S9))) ) ) ) )
proofend;
uniqueness
 for b1, b2 being Element of QC-WFF A st ex F being Function of (QC-Sub-WFF A),(QC-WFF A) st
( b1 = F . S &amp; ( for S9 being Element of QC-Sub-WFF A holds
( ( S9 is A -Sub_VERUM implies F . S9 = VERUM A ) &amp; ( S9 is Sub_atomic implies F . S9 = (the_pred_symbol_of (S9 `1)) ! (CQC_Subst ((Sub_the_arguments_of S9),(S9 `2))) ) &amp; ( S9 is Sub_negative implies F . S9 = 'not' (F . (Sub_the_argument_of S9)) ) &amp; ( S9 is Sub_conjunctive implies F . S9 = (F . (Sub_the_left_argument_of S9)) '&amp;' (F . (Sub_the_right_argument_of S9)) ) &amp; ( S9 is Sub_universal implies F . S9 = Quant (S9,(F . (Sub_the_scope_of S9))) ) ) ) ) &amp; ex F being Function of (QC-Sub-WFF A),(QC-WFF A) st
( b2 = F . S &amp; ( for S9 being Element of QC-Sub-WFF A holds
( ( S9 is A -Sub_VERUM implies F . S9 = VERUM A ) &amp; ( S9 is Sub_atomic implies F . S9 = (the_pred_symbol_of (S9 `1)) ! (CQC_Subst ((Sub_the_arguments_of S9),(S9 `2))) ) &amp; ( S9 is Sub_negative implies F . S9 = 'not' (F . (Sub_the_argument_of S9)) ) &amp; ( S9 is Sub_conjunctive implies F . S9 = (F . (Sub_the_left_argument_of S9)) '&amp;' (F . (Sub_the_right_argument_of S9)) ) &amp; ( S9 is Sub_universal implies F . S9 = Quant (S9,(F . (Sub_the_scope_of S9))) ) ) ) ) holds
b1 = b2 by Lm6;
end;

:: deftheorem Def38 defines CQC_Sub SUBSTUT1:def_38_:_
 for A being QC-alphabet
for S being Element of QC-Sub-WFF A
for b3 being Element of QC-WFF A holds
( b3 = CQC_Sub S iff ex F being Function of (QC-Sub-WFF A),(QC-WFF A) st
( b3 = F . S &amp; ( for S9 being Element of QC-Sub-WFF A holds
( ( S9 is A -Sub_VERUM implies F . S9 = VERUM A ) &amp; ( S9 is Sub_atomic implies F . S9 = (the_pred_symbol_of (S9 `1)) ! (CQC_Subst ((Sub_the_arguments_of S9),(S9 `2))) ) &amp; ( S9 is Sub_negative implies F . S9 = 'not' (F . (Sub_the_argument_of S9)) ) &amp; ( S9 is Sub_conjunctive implies F . S9 = (F . (Sub_the_left_argument_of S9)) '&amp;' (F . (Sub_the_right_argument_of S9)) ) &amp; ( S9 is Sub_universal implies F . S9 = Quant (S9,(F . (Sub_the_scope_of S9))) ) ) ) ) );

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))
proofend;

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)
proofend;

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)) '&amp;' (CQC_Sub (Sub_the_right_argument_of S))
proofend;

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_&amp; (S1,S2)) = (CQC_Sub S1) '&amp;' (CQC_Sub S2)
proofend;

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)))
proofend;

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  }  ;
coherence
  {  S where S is Element of QC-Sub-WFF A : S `1 is Element of CQC-WFF A  }  is Subset of (QC-Sub-WFF A)
proofend;
end;

:: deftheorem  defines CQC-Sub-WFF SUBSTUT1:def_39_:_
 for A being QC-alphabet holds CQC-Sub-WFF A =  {  S where S is Element of QC-Sub-WFF A : S `1 is Element of CQC-WFF A  }  ;

registration
let A be QC-alphabet ;
cluster CQC-Sub-WFF A ->  non empty ;
coherence
 not CQC-Sub-WFF A is empty
proofend;
end;

theorem Th33: :: SUBSTUT1:33
for A being QC-alphabet
for S being Element of QC-Sub-WFF A st S is A -Sub_VERUM holds
CQC_Sub S is Element of CQC-WFF A
proofend;

Lm7:  for A being QC-alphabet
for k being Element of NAT
for P being QC-pred_symbol of k,A
for ll being CQC-variable_list of k,A holds the_pred_symbol_of (P ! ll) = P
proofend;

theorem Th34: :: SUBSTUT1:34
for A being QC-alphabet
for k being Element of NAT
for h being FinSequence holds
( h is CQC-variable_list of k,A iff ( h is FinSequence of bound_QC-variables A &amp; len h = k ) )
proofend;

theorem Th35: :: SUBSTUT1:35
for A being QC-alphabet
for k being Element of NAT
for P being QC-pred_symbol of k,A
for ll being CQC-variable_list of k,A
for e being Element of vSUB A holds CQC_Sub (Sub_P (P,ll,e)) is Element of CQC-WFF A
proofend;

theorem Th36: :: SUBSTUT1:36
for A being QC-alphabet
for S being Element of QC-Sub-WFF A st CQC_Sub S is Element of CQC-WFF A holds
CQC_Sub (Sub_not S) is Element of CQC-WFF A
proofend;

theorem Th37: :: SUBSTUT1:37
for A being QC-alphabet
for S1, S2 being Element of QC-Sub-WFF A st S1 `2 = S2 `2 &amp; CQC_Sub S1 is Element of CQC-WFF A &amp; CQC_Sub S2 is Element of CQC-WFF A holds
CQC_Sub (Sub_&amp; (S1,S2)) is Element of CQC-WFF A
proofend;

theorem Th38: :: SUBSTUT1:38
for A being QC-alphabet
for x being bound_QC-variable of A
for S being Element of QC-Sub-WFF A
for xSQ being second_Q_comp of [S,x] st CQC_Sub S is Element of CQC-WFF A &amp; [S,x] is quantifiable holds
CQC_Sub (Sub_All ([S,x],xSQ)) is Element of CQC-WFF A
proofend;

scheme :: SUBSTUT1:sch 5
SubCQCInd{ F1() ->  QC-alphabet , P1[ set ] } :
 for S being Element of CQC-Sub-WFF F1() holds P1[S]
provided
A1: for S, S9 being Element of CQC-Sub-WFF F1()
for x being bound_QC-variable of F1()
for SQ being second_Q_comp of [S,x]
for k being Element of NAT
for ll being CQC-variable_list of k,F1()
for P being QC-pred_symbol of k,F1()
for e being Element of vSUB F1() holds
( P1[ Sub_P (P,ll,e)] &amp; ( S is F1() -Sub_VERUM implies P1[S] ) &amp; ( P1[S] implies P1[ Sub_not S] ) &amp; ( S `2 = S9 `2 &amp; P1[S] &amp; P1[S9] implies P1[ Sub_&amp; (S,S9)] ) &amp; ( [S,x] is quantifiable &amp; P1[S] implies P1[ Sub_All ([S,x],SQ)] ) )
proofend;

definition
let A be QC-alphabet ;
let S be Element of CQC-Sub-WFF A;
:: original:CQC_Sub
redefine func CQC_Sub S ->  Element of CQC-WFF A;
coherence
 CQC_Sub S is Element of CQC-WFF A
proofend;
end;

theorem :: SUBSTUT1:39
for A being QC-alphabet
for Sub being CQC_Substitution of A holds rng (@ Sub) c= bound_QC-variables A ;