:: 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
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 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
ex b1 being FinSequence of QC-variables A st
( len b1 = len l & ( for k being Element of NAT st 1 <= k & k <= len l holds
( ( l . k in dom Sub implies b1 . k = Sub . (l . k) ) & ( not l . k in dom Sub implies b1 . k = l . k ) ) ) )
proof end;
uniqueness
for b1, b2 being FinSequence of QC-variables A st len b1 = len l & ( for k being Element of NAT st 1 <= k & k <= len l holds
( ( l . k in dom Sub implies b1 . k = Sub . (l . k) ) & ( not l . k in dom Sub implies b1 . k = l . k ) ) ) & len b2 = len l & ( for k being Element of NAT st 1 <= k & k <= len l holds
( ( l . k in dom Sub implies b2 . k = Sub . (l . k) ) & ( not l . k in dom Sub implies b2 . k = l . k ) ) ) holds
b1 = b2
proof end;
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 & ( for k being Element of NAT st 1 <= k & k <= len l holds
( ( l . k in dom Sub implies b4 . k = Sub . (l . k) ) & ( 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
proof end;
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
proof end;
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 func Sub | X -> CQC_Substitution of A;
coherence
Sub | X is CQC_Substitution of A
proof end;
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
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 ) } ;
coherence
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 ) } is finite CQC_Substitution of A
proof end;
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 & y is Element of dom Sub & y <> x & 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 & k <= len l1 & l1 . k in bound_QC-variables A ) } ;
coherence
{ (l1 . k) where k is Element of NAT : ( 1 <= k & k <= len l1 & l1 . k in bound_QC-variables A ) } is Subset of (bound_QC-variables A)
proof end;
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 & k <= len l1 & 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 & ( 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
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 & ( 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)} ) ) ) )
;
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 & ( 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)} ) ) ) ) & ex F being Function of (QC-WFF A),(bool (bound_QC-variables A)) st
( b2 = 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)} ) ) ) ) holds
b1 = b2
;
proof end;
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 & ( 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)} ) ) ) ) );

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

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));
coherence
NAT \ ((Dom_Bound_Vars p) \/ (Sub_Var finSub)) is non empty Subset of (QC-symbols A)
proof end;
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 ) & ( not x in rng finSub implies finSub \/ {[x,x]} is CQC_Substitution of A ) )
proof end;
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)))]} ) & ( 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 ;
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 :
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))) ) & ( 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] & 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] & p,Sub PQSub b ) )
proof end;
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] & p,Sub PQSub b ) ) ) & ( 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] & p,Sub PQSub b ) ) ) holds
b1 = b2
proof end;
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] & 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):] & ( 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):] ) & ( 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 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 ) & ( 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 :
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):] & ( 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 ) & ( 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 ) ) );

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 & not b1 is empty )
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 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):]

proof end;

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

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 ) );
existence
ex b1 being non empty set st
( b1 is A -Sub-closed & ( for D being non empty set st D is A -Sub-closed holds
b1 c= D ) )
proof end;
uniqueness
for b1, b2 being non empty set st b1 is A -Sub-closed & ( for D being non empty set st D is A -Sub-closed holds
b1 c= D ) & b2 is A -Sub-closed & ( for D being non empty set st D is A -Sub-closed holds
b2 c= D ) holds
b1 = b2
proof end;
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 & ( 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]
proof end;

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
proof end;
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]
proof end;

definition
let A be QC-alphabet ;
let S be Element of QC-Sub-WFF A;
attr S 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 func S `1 -> Element of QC-WFF A;
coherence
S `1 is Element of QC-WFF A
proof end;
:: original: `2
redefine func S `2 -> Element of vSUB A;
coherence
S `2 is Element of vSUB A
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)];
coherence
[('not' (S `1)),(S `2)] is Element of QC-Sub-WFF A
proof end;
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_& (S,S9) -> Element of QC-Sub-WFF A equals :Def21: :: SUBSTUT1:def 21
[((S `1) '&' (S9 `1)),(S `2)];
coherence
[((S `1) '&' (S9 `1)),(S `2)] is Element of QC-Sub-WFF A
proof end;
end;

:: deftheorem Def21 defines Sub_& 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_& (S,S9) = [((S `1) '&' (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 func B `1 -> Element of QC-Sub-WFF A;
coherence
B `1 is Element of QC-Sub-WFF A
by MCART_1:10;
:: original: `2
redefine func B `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):];
attr B 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
proof end;
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):]
proof end;
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 & P1[S] & P1[S9] holds
P1[ Sub_& (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 & P1[S] holds
P1[ 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 :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
proof end;

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;
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 :
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_& (S1,S2) & S1 `2 = S2 `2 ) );

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 :
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) & 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 )
proof end;

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 & 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 & S = Sub_P (P,ll,e) )
proof end;
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 & S = Sub_P (P,ll,e) ) & 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 & S = Sub_P (P,ll,e) ) holds
b1 = b2
proof end;
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 & 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 & S = Sub_not b2 holds
b1 = b2
proof end;
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_& (it,S9) & it `2 = S9 `2 );
existence
ex b1, S9 being Element of QC-Sub-WFF A st
( S = Sub_& (b1,S9) & 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_& (b1,S9) & b1 `2 = S9 `2 ) & ex S9 being Element of QC-Sub-WFF A st
( S = Sub_& (b2,S9) & b2 `2 = S9 `2 ) holds
b1 = b2
proof end;
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_& (b3,S9) & 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_& (S9,it) & S9 `2 = it `2 );
existence
ex b1, S9 being Element of QC-Sub-WFF A st
( S = Sub_& (S9,b1) & S9 `2 = b1 `2 )
proof end;
uniqueness
for b1, b2 being Element of QC-Sub-WFF A st ex S9 being Element of QC-Sub-WFF A st
( S = Sub_& (S9,b1) & S9 `2 = b1 `2 ) & ex S9 being Element of QC-Sub-WFF A st
( S = Sub_& (S9,b2) & S9 `2 = b2 `2 ) holds
b1 = b2
proof end;
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_& (S9,b3) & 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) & B `2 = it & 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) & B `2 = b1 & B is quantifiable )
proof end;
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) & B `2 = b1 & B is quantifiable ) & 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 = b2 & B is quantifiable ) holds
b1 = b2
proof end;
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) & B `2 = b3 & 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) & B `1 = it & 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) & B `1 = b1 & B is quantifiable )
proof end;
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) & B `1 = b1 & B is quantifiable ) & 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 = b2 & B is quantifiable ) holds
b1 = b2
proof end;
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) & B `1 = b3 & 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
proof end;
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
proof end;

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
proof end;

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{ 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] ) & ( S is F1() -Sub_VERUM implies P1[S] ) & ( S is Sub_negative & P1[ Sub_the_argument_of S] implies P1[S] ) & ( S is Sub_conjunctive & P1[ Sub_the_left_argument_of S] & P1[ Sub_the_right_argument_of S] implies P1[S] ) & ( S is Sub_universal & P1[ Sub_the_scope_of S] implies P1[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 Element of 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{ 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() ) & ( S is Sub_atomic implies F . S = F4(S) ) & ( S is Sub_negative & d1 = F . (Sub_the_argument_of S) implies F . S = F5(d1) ) & ( S is Sub_conjunctive & d1 = F . (Sub_the_left_argument_of S) & d2 = F . (Sub_the_right_argument_of S) implies F . S = F6(d1,d2) ) & ( S is Sub_universal & d1 = F . (Sub_the_scope_of S) implies F . S = F7(F1(),S,d1) ) )
proof end;

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() ) & ( S is Sub_atomic implies F3() . S = F6(S) ) & ( S is Sub_negative & d1 = F3() . (Sub_the_argument_of S) implies F3() . S = F7(d1) ) & ( S is Sub_conjunctive & d1 = F3() . (Sub_the_left_argument_of S) & d2 = F3() . (Sub_the_right_argument_of S) implies F3() . S = F8(d1,d2) ) & ( S is Sub_universal & 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() ) & ( S is Sub_atomic implies F4() . S = F6(S) ) & ( S is Sub_negative & d1 = F4() . (Sub_the_argument_of S) implies F4() . S = F7(d1) ) & ( S is Sub_conjunctive & d1 = F4() . (Sub_the_left_argument_of S) & d2 = F4() . (Sub_the_right_argument_of S) implies F4() . S = F8(d1,d2) ) & ( S is Sub_universal & d1 = F4() . (Sub_the_scope_of S) implies F4() . S = F9(F1(),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;
coherence
S is Element of [:(QC-WFF A),(vSUB A):]
proof end;
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 func Z `1 -> Element of QC-WFF A;
coherence
Z `1 is Element of QC-WFF A
proof end;
:: original: `2
redefine func Z `2 -> CQC_Substitution of A;
coherence
Z `2 is CQC_Substitution of A
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
( ( 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 ) & ( 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)))) ) & ( 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 ) & ( 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;

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 & ( 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))) ) ) ) );
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 & ( 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
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 & ( 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))) ) ) ) ) & ex F being Function of (QC-Sub-WFF A),(QC-WFF A) st
( b2 = 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))) ) ) ) ) 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 & ( 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))) ) ) ) ) );

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 } ;
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)
proof end;
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
proof end;
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
proof end;

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

proof end;

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 & len h = k ) )
proof end;

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
proof end;

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
proof end;

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

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 & [S,x] is quantifiable holds
CQC_Sub (Sub_All ([S,x],xSQ)) is Element of CQC-WFF A
proof end;

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)] & ( S is F1() -Sub_VERUM implies P1[S] ) & ( P1[S] implies P1[ Sub_not S] ) & ( S `2 = S9 `2 & P1[S] & P1[S9] implies P1[ Sub_& (S,S9)] ) & ( [S,x] is quantifiable & P1[S] implies P1[ Sub_All ([S,x],SQ)] ) )
proof end;

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
proof end;
end;

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