let Al be QC-alphabet ; :: thesis: for Al2 being Al -expanding QC-alphabet
for p2 being Element of CQC-WFF Al2
for S being finite CQC_Substitution of Al
for S2 being finite CQC_Substitution of Al2
for p being Element of CQC-WFF Al st S = S2 & p = p2 holds
upVar (S,p) = upVar (S2,p2)
let Al2 be Al -expanding QC-alphabet ; :: thesis: for p2 being Element of CQC-WFF Al2
for S being finite CQC_Substitution of Al
for S2 being finite CQC_Substitution of Al2
for p being Element of CQC-WFF Al st S = S2 & p = p2 holds
upVar (S,p) = upVar (S2,p2)
let p2 be Element of CQC-WFF Al2; :: thesis: for S being finite CQC_Substitution of Al
for S2 being finite CQC_Substitution of Al2
for p being Element of CQC-WFF Al st S = S2 & p = p2 holds
upVar (S,p) = upVar (S2,p2)
let S be finite CQC_Substitution of Al; :: thesis: for S2 being finite CQC_Substitution of Al2
for p being Element of CQC-WFF Al st S = S2 & p = p2 holds
upVar (S,p) = upVar (S2,p2)
let S2 be finite CQC_Substitution of Al2; :: thesis: for p being Element of CQC-WFF Al st S = S2 & p = p2 holds
upVar (S,p) = upVar (S2,p2)
let p be Element of CQC-WFF Al; :: thesis: ( S = S2 & p = p2 implies upVar (S,p) = upVar (S2,p2) )
assume A1: ( S = S2 & p = p2 ) ; :: thesis: upVar (S,p) = upVar (S2,p2)
A2: Sub_Var S = Sub_Var S2
proof
for s being object st s in Sub_Var S holds
s in Sub_Var S2
proof
let s be object ; :: thesis: ( s in Sub_Var S implies s in Sub_Var S2 )
assume A3: s in Sub_Var S ; :: thesis: s in Sub_Var S2
s in { t where t is QC-symbol of Al : x. t in rng S } by A3, SUBSTUT1:def 10;
then consider s2 being QC-symbol of Al such that
A4: ( s = s2 & x. s2 in rng S ) ;
( s2 in QC-symbols Al & QC-symbols Al c= QC-symbols Al2 ) by Th2;
then consider s3 being QC-symbol of Al2 such that
A5: s3 = s2 ;
x. s2 = [4,s2] by QC_LANG3:def 2
.= x. s3 by A5, QC_LANG3:def 2 ;
then s3 in { t where t is QC-symbol of Al2 : x. t in rng S2 } by A1, A4;
hence s in Sub_Var S2 by A4, A5, SUBSTUT1:def 10; :: thesis: verum
end;
hence Sub_Var S c= Sub_Var S2 ; :: according to XBOOLE_0:def 10 :: thesis: Sub_Var S2 c= Sub_Var S
for s being object st s in Sub_Var S2 holds
s in Sub_Var S
proof
let s be object ; :: thesis: ( s in Sub_Var S2 implies s in Sub_Var S )
assume A6: s in Sub_Var S2 ; :: thesis: s in Sub_Var S
s in { t where t is QC-symbol of Al2 : x. t in rng S2 } by A6, SUBSTUT1:def 10;
then consider s2 being QC-symbol of Al2 such that
A7: ( s = s2 & x. s2 in rng S2 ) ;
A8: rng (@ S) c= bound_QC-variables Al by SUBSTUT1:39;
x. s2 in rng (@ S) by A1, A7, SUBSTUT1:def 2;
then x. s2 in bound_QC-variables Al by A8;
then [4,s2] in [:{4},(QC-symbols Al):] by QC_LANG3:def 2;
then s2 in QC-symbols Al by ZFMISC_1:87;
then consider s3 being QC-symbol of Al such that
A9: s3 = s2 ;
x. s2 = [4,s2] by QC_LANG3:def 2
.= x. s3 by A9, QC_LANG3:def 2 ;
then s3 in { t where t is QC-symbol of Al : x. t in rng S } by A1, A7;
hence s in Sub_Var S by A7, A9, SUBSTUT1:def 10; :: thesis: verum
end;
hence Sub_Var S2 c= Sub_Var S ; :: thesis: verum
end;
defpred S1[ Element of QC-WFF Al] means for q2 being Element of CQC-WFF Al2 st $1 = q2 holds
Bound_Vars $1 = Bound_Vars q2;
A10: S1[ VERUM Al]
proof
let q2 be Element of CQC-WFF Al2; :: thesis: ( VERUM Al = q2 implies Bound_Vars (VERUM Al) = Bound_Vars q2 )
assume A11: q2 = VERUM Al ; :: thesis: Bound_Vars (VERUM Al) = Bound_Vars q2
q2 = VERUM Al2 by A11;
hence Bound_Vars q2 = {} by SUBSTUT1:2
.= Bound_Vars (VERUM Al) by SUBSTUT1:2 ;
:: thesis: verum
end;
A12: for k being Nat
for P being QC-pred_symbol of k,Al
for l being CQC-variable_list of k,Al holds S1[P ! l]
proof
let k be Nat; :: thesis: for P being QC-pred_symbol of k,Al
for l being CQC-variable_list of k,Al holds S1[P ! l]
let P be QC-pred_symbol of k,Al; :: thesis: for l being CQC-variable_list of k,Al holds S1[P ! l]
let l be CQC-variable_list of k,Al; :: thesis: S1[P ! l]
set P2 = Al2 -Cast P;
set l2 = Al2 -Cast l;
let q2 be Element of CQC-WFF Al2; :: thesis: ( P ! l = q2 implies Bound_Vars (P ! l) = Bound_Vars q2 )
assume A13: P ! l = q2 ; :: thesis: Bound_Vars (P ! l) = Bound_Vars q2
A14: q2 = Al2 -Cast (P ! l) by A13
.= (Al2 -Cast P) ! (Al2 -Cast l) by Th8 ;
thus Bound_Vars (P ! l) = still_not-bound_in (P ! l) by SUBLEMMA:43
.= still_not-bound_in (Al2 -Cast (P ! l)) by Th12
.= still_not-bound_in ((Al2 -Cast P) ! (Al2 -Cast l)) by Th8
.= Bound_Vars q2 by A14, SUBLEMMA:43 ; :: thesis: verum
end;
A15: for r, s being Element of CQC-WFF Al st S1[r] & S1[s] holds
S1[r '&' s]
proof
let r, s be Element of CQC-WFF Al; :: thesis: ( S1[r] & S1[s] implies S1[r '&' s] )
assume A16: ( S1[r] & S1[s] ) ; :: thesis: S1[r '&' s]
set q = r '&' s;
set r2 = Al2 -Cast r;
set s2 = Al2 -Cast s;
let q2 be Element of CQC-WFF Al2; :: thesis: ( r '&' s = q2 implies Bound_Vars (r '&' s) = Bound_Vars q2 )
assume A17: r '&' s = q2 ; :: thesis: Bound_Vars (r '&' s) = Bound_Vars q2
A18: q2 = (Al2 -Cast r) '&' (Al2 -Cast s) by A17;
then ( r '&' s is conjunctive & q2 is conjunctive ) ;
then A19: ( the_left_argument_of (r '&' s) = r & the_right_argument_of (r '&' s) = s & the_left_argument_of q2 = Al2 -Cast r & the_right_argument_of q2 = Al2 -Cast s ) by A18, QC_LANG1:def 25, QC_LANG1:def 26;
A20: ( Bound_Vars r = Bound_Vars (Al2 -Cast r) & Bound_Vars s = Bound_Vars (Al2 -Cast s) ) by A16;
thus Bound_Vars (r '&' s) = (Bound_Vars r) \/ (Bound_Vars s) by A19, SUBSTUT1:5, QC_LANG1:def 20
.= Bound_Vars q2 by A18, A19, A20, SUBSTUT1:5, QC_LANG1:def 20 ; :: thesis: verum
end;
A21: for r being Element of CQC-WFF Al st S1[r] holds
S1[ 'not' r]
proof
let r be Element of CQC-WFF Al; :: thesis: ( S1[r] implies S1[ 'not' r] )
assume A22: S1[r] ; :: thesis: S1[ 'not' r]
set q = 'not' r;
set r2 = Al2 -Cast r;
let q2 be Element of CQC-WFF Al2; :: thesis: ( 'not' r = q2 implies Bound_Vars ('not' r) = Bound_Vars q2 )
assume A23: 'not' r = q2 ; :: thesis: Bound_Vars ('not' r) = Bound_Vars q2
A24: q2 = 'not' (Al2 -Cast r) by A23;
then ( 'not' r is negative & q2 is negative ) ;
then A25: ( the_argument_of ('not' r) = r & the_argument_of q2 = Al2 -Cast r ) by A24, QC_LANG1:def 24;
thus Bound_Vars ('not' r) = Bound_Vars r by A25, SUBSTUT1:4, QC_LANG1:def 19
.= Bound_Vars (Al2 -Cast r) by A22
.= Bound_Vars q2 by A24, A25, SUBSTUT1:4, QC_LANG1:def 19 ; :: thesis: verum
end;
A26: for x being bound_QC-variable of Al
for r being Element of CQC-WFF Al st S1[r] holds
S1[ All (x,r)]
proof
let x be bound_QC-variable of Al; :: thesis: for r being Element of CQC-WFF Al st S1[r] holds
S1[ All (x,r)]
let r be Element of CQC-WFF Al; :: thesis: ( S1[r] implies S1[ All (x,r)] )
assume A27: S1[r] ; :: thesis: S1[ All (x,r)]
set q = All (x,r);
set r2 = Al2 -Cast r;
set x2 = Al2 -Cast x;
let q2 be Element of CQC-WFF Al2; :: thesis: ( All (x,r) = q2 implies Bound_Vars (All (x,r)) = Bound_Vars q2 )
assume A28: All (x,r) = q2 ; :: thesis: Bound_Vars (All (x,r)) = Bound_Vars q2
A29: q2 = All ((Al2 -Cast x),(Al2 -Cast r)) by A28;
then ( All (x,r) is universal & q2 is universal ) ;
then A30: ( the_scope_of (All (x,r)) = r & bound_in (All (x,r)) = x & the_scope_of q2 = Al2 -Cast r & bound_in q2 = Al2 -Cast x ) by A29, QC_LANG1:def 27, QC_LANG1:def 28;
thus Bound_Vars (All (x,r)) = (Bound_Vars r) \/ {x} by A30, SUBSTUT1:6, QC_LANG1:def 21
.= (Bound_Vars (Al2 -Cast r)) \/ {(Al2 -Cast x)} by A27
.= Bound_Vars q2 by A29, A30, SUBSTUT1:6, QC_LANG1:def 21 ; :: thesis: verum
end;
A31: for r, s being Element of CQC-WFF Al
for x being bound_QC-variable of Al
for k being Nat
for l being CQC-variable_list of k,Al
for P being QC-pred_symbol of k,Al holds
( S1[ VERUM Al] & S1[P ! l] & ( S1[r] implies S1[ 'not' r] ) & ( S1[r] & S1[s] implies S1[r '&' s] ) & ( S1[r] implies S1[ All (x,r)] ) ) by A10, A12, A15, A21, A26;
A32: for q being Element of CQC-WFF Al holds S1[q] from CQC_LANG:sch 1(A31);
 A33: Dom_Bound_Vars p = Dom_Bound_Vars p2
proof
for s being object st s in Dom_Bound_Vars p holds
s in Dom_Bound_Vars p2
proof
let s be object ; :: thesis: ( s in Dom_Bound_Vars p implies s in Dom_Bound_Vars p2 )
assume A34: s in Dom_Bound_Vars p ; :: thesis: s in Dom_Bound_Vars p2
s in { b where b is QC-symbol of Al : x. b in Bound_Vars p } by A34, SUBSTUT1:def 9;
then consider s2 being QC-symbol of Al such that
A35: ( s = s2 & x. s2 in Bound_Vars p ) ;
x. s2 in Bound_Vars p2 by A1, A32, A35;
then x. s2 in bound_QC-variables Al2 ;
then [4,s2] in [:{4},(QC-symbols Al2):] by QC_LANG3:def 2;
then s2 in QC-symbols Al2 by ZFMISC_1:87;
then consider s3 being QC-symbol of Al2 such that
A36: s3 = s2 ;
x. s2 = [4,s2] by QC_LANG3:def 2
.= x. s3 by A36, QC_LANG3:def 2 ;
then x. s3 in Bound_Vars p2 by A1, A32, A35;
then s3 in { b where b is QC-symbol of Al2 : x. b in Bound_Vars p2 } ;
hence s in Dom_Bound_Vars p2 by A35, A36, SUBSTUT1:def 9; :: thesis: verum
end;
hence Dom_Bound_Vars p c= Dom_Bound_Vars p2 ; :: according to XBOOLE_0:def 10 :: thesis: Dom_Bound_Vars p2 c= Dom_Bound_Vars p
for s being object st s in Dom_Bound_Vars p2 holds
s in Dom_Bound_Vars p
proof
let s be object ; :: thesis: ( s in Dom_Bound_Vars p2 implies s in Dom_Bound_Vars p )
assume A37: s in Dom_Bound_Vars p2 ; :: thesis: s in Dom_Bound_Vars p
s in { b where b is QC-symbol of Al2 : x. b in Bound_Vars p2 } by A37, SUBSTUT1:def 9;
then consider s2 being QC-symbol of Al2 such that
A38: ( s = s2 & x. s2 in Bound_Vars p2 ) ;
x. s2 in Bound_Vars p by A1, A32, A38;
then x. s2 in bound_QC-variables Al ;
then [4,s2] in [:{4},(QC-symbols Al):] by QC_LANG3:def 2;
then s2 in QC-symbols Al by ZFMISC_1:87;
then consider s3 being QC-symbol of Al such that
A39: s3 = s2 ;
x. s2 = [4,s2] by QC_LANG3:def 2
.= x. s3 by A39, QC_LANG3:def 2 ;
then x. s3 in Bound_Vars p by A1, A32, A38;
then s3 in { b where b is QC-symbol of Al : x. b in Bound_Vars p } ;
hence s in Dom_Bound_Vars p by A38, A39, SUBSTUT1:def 9; :: thesis: verum
end;
hence Dom_Bound_Vars p2 c= Dom_Bound_Vars p ; :: thesis: verum
end;
A40: NSub (p,S) = NAT \ ((Dom_Bound_Vars p) \/ (Sub_Var S)) by SUBSTUT1:def 11
.= NSub (p2,S2) by A2, A33, SUBSTUT1:def 11 ;
thus upVar (S,p) = the Element of NSub (p,S) by SUBSTUT1:def 12
.= upVar (S2,p2) by A40, SUBSTUT1:def 12 ; :: thesis: verum