let Al be QC-alphabet ; :: thesis: for Al2 being Al -expanding QC-alphabet

for p being Element of CQC-WFF Al holds still_not-bound_in p = still_not-bound_in (Al2 -Cast p)

let Al2 be Al -expanding QC-alphabet ; :: thesis: for p being Element of CQC-WFF Al holds still_not-bound_in p = still_not-bound_in (Al2 -Cast p)

defpred S_{1}[ Element of CQC-WFF Al] means still_not-bound_in $1 = still_not-bound_in (Al2 -Cast $1);

A1: S_{1}[ VERUM Al]

for P being QC-pred_symbol of k,Al

for l being CQC-variable_list of k,Al holds S_{1}[P ! l]
_{1}[p] holds

S_{1}[ 'not' p]
_{1}[p] & S_{1}[q] holds

S_{1}[p '&' q]

for p being Element of CQC-WFF Al st S_{1}[p] holds

S_{1}[ All (x,p)]

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

( S_{1}[ VERUM Al] & S_{1}[P ! l] & ( S_{1}[p] implies S_{1}[ 'not' p] ) & ( S_{1}[p] & S_{1}[q] implies S_{1}[p '&' q] ) & ( S_{1}[p] implies S_{1}[ All (x,p)] ) )
by A1, A2, A8, A10;

for p being Element of CQC-WFF Al holds S_{1}[p]
from CQC_LANG:sch 1(A15);

hence for p being Element of CQC-WFF Al holds still_not-bound_in p = still_not-bound_in (Al2 -Cast p) ; :: thesis: verum

for p being Element of CQC-WFF Al holds still_not-bound_in p = still_not-bound_in (Al2 -Cast p)

let Al2 be Al -expanding QC-alphabet ; :: thesis: for p being Element of CQC-WFF Al holds still_not-bound_in p = still_not-bound_in (Al2 -Cast p)

defpred S

A1: S

proof

A2:
for k being Nat
thus still_not-bound_in (VERUM Al) =
{}
by QC_LANG3:3

.= still_not-bound_in (VERUM Al2) by QC_LANG3:3

.= still_not-bound_in (Al2 -Cast (VERUM Al)) ; :: thesis: verum

end;.= still_not-bound_in (VERUM Al2) by QC_LANG3:3

.= still_not-bound_in (Al2 -Cast (VERUM Al)) ; :: thesis: verum

for P being QC-pred_symbol of k,Al

for l being CQC-variable_list of k,Al holds S

proof

A8:
for p being Element of CQC-WFF Al st S
let k be Nat; :: thesis: for P being QC-pred_symbol of k,Al

for l being CQC-variable_list of k,Al holds S_{1}[P ! l]

let P be QC-pred_symbol of k,Al; :: thesis: for l being CQC-variable_list of k,Al holds S_{1}[P ! l]

let l be CQC-variable_list of k,Al; :: thesis: S_{1}[P ! l]

A3: still_not-bound_in l = still_not-bound_in (Al2 -Cast l)

.= still_not-bound_in ((Al2 -Cast P) ! (Al2 -Cast l)) by A3, QC_LANG3:5

.= still_not-bound_in (Al2 -Cast (P ! l)) by Th8 ; :: thesis: verum

end;for l being CQC-variable_list of k,Al holds S

let P be QC-pred_symbol of k,Al; :: thesis: for l being CQC-variable_list of k,Al holds S

let l be CQC-variable_list of k,Al; :: thesis: S

A3: still_not-bound_in l = still_not-bound_in (Al2 -Cast l)

proof

thus still_not-bound_in (P ! l) =
still_not-bound_in l
by QC_LANG3:5
for x being object st x in still_not-bound_in l holds

x in still_not-bound_in (Al2 -Cast l)

for x being object st x in still_not-bound_in (Al2 -Cast l) holds

x in still_not-bound_in l

end;x in still_not-bound_in (Al2 -Cast l)

proof

hence
still_not-bound_in l c= still_not-bound_in (Al2 -Cast l)
; :: according to XBOOLE_0:def 10 :: thesis: still_not-bound_in (Al2 -Cast l) c= still_not-bound_in l
let x be object ; :: thesis: ( x in still_not-bound_in l implies x in still_not-bound_in (Al2 -Cast l) )

assume A4: x in still_not-bound_in l ; :: thesis: x in still_not-bound_in (Al2 -Cast l)

consider n being Nat such that

A5: ( x = l . n & 1 <= n & n <= len l & l . n in bound_QC-variables Al ) by A4;

set y = l . n;

reconsider y = l . n as bound_QC-variable of Al by A5;

y = Al2 -Cast y ;

hence x in still_not-bound_in (Al2 -Cast l) by A5; :: thesis: verum

end;assume A4: x in still_not-bound_in l ; :: thesis: x in still_not-bound_in (Al2 -Cast l)

consider n being Nat such that

A5: ( x = l . n & 1 <= n & n <= len l & l . n in bound_QC-variables Al ) by A4;

set y = l . n;

reconsider y = l . n as bound_QC-variable of Al by A5;

y = Al2 -Cast y ;

hence x in still_not-bound_in (Al2 -Cast l) by A5; :: thesis: verum

for x being object st x in still_not-bound_in (Al2 -Cast l) holds

x in still_not-bound_in l

proof

hence
still_not-bound_in (Al2 -Cast l) c= still_not-bound_in l
; :: thesis: verum
let x be object ; :: thesis: ( x in still_not-bound_in (Al2 -Cast l) implies x in still_not-bound_in l )

assume A6: x in still_not-bound_in (Al2 -Cast l) ; :: thesis: x in still_not-bound_in l

consider n being Nat such that

A7: ( x = (Al2 -Cast l) . n & 1 <= n & n <= len (Al2 -Cast l) & (Al2 -Cast l) . n in bound_QC-variables Al2 ) by A6;

set y = (Al2 -Cast l) . n;

( rng l c= bound_QC-variables Al & dom l = Seg (len l) ) by FINSEQ_1:def 3;

then ( (Al2 -Cast l) . n = l . n & n in dom l & l is FinSequence of bound_QC-variables Al ) by A7, FINSEQ_1:1, FINSEQ_1:def 4;

then (Al2 -Cast l) . n in bound_QC-variables Al by FINSEQ_2:11;

hence x in still_not-bound_in l by A7; :: thesis: verum

end;assume A6: x in still_not-bound_in (Al2 -Cast l) ; :: thesis: x in still_not-bound_in l

consider n being Nat such that

A7: ( x = (Al2 -Cast l) . n & 1 <= n & n <= len (Al2 -Cast l) & (Al2 -Cast l) . n in bound_QC-variables Al2 ) by A6;

set y = (Al2 -Cast l) . n;

( rng l c= bound_QC-variables Al & dom l = Seg (len l) ) by FINSEQ_1:def 3;

then ( (Al2 -Cast l) . n = l . n & n in dom l & l is FinSequence of bound_QC-variables Al ) by A7, FINSEQ_1:1, FINSEQ_1:def 4;

then (Al2 -Cast l) . n in bound_QC-variables Al by FINSEQ_2:11;

hence x in still_not-bound_in l by A7; :: thesis: verum

.= still_not-bound_in ((Al2 -Cast P) ! (Al2 -Cast l)) by A3, QC_LANG3:5

.= still_not-bound_in (Al2 -Cast (P ! l)) by Th8 ; :: thesis: verum

S

proof

A10:
for p, q being Element of CQC-WFF Al st S
let p be Element of CQC-WFF Al; :: thesis: ( S_{1}[p] implies S_{1}[ 'not' p] )

assume A9: S_{1}[p]
; :: thesis: S_{1}[ 'not' p]

thus still_not-bound_in ('not' p) = still_not-bound_in p by QC_LANG3:7

.= still_not-bound_in ('not' (Al2 -Cast p)) by A9, QC_LANG3:7

.= still_not-bound_in (Al2 -Cast ('not' p)) ; :: thesis: verum

end;assume A9: S

thus still_not-bound_in ('not' p) = still_not-bound_in p by QC_LANG3:7

.= still_not-bound_in ('not' (Al2 -Cast p)) by A9, QC_LANG3:7

.= still_not-bound_in (Al2 -Cast ('not' p)) ; :: thesis: verum

S

proof

for x being bound_QC-variable of Al
let p, q be Element of CQC-WFF Al; :: thesis: ( S_{1}[p] & S_{1}[q] implies S_{1}[p '&' q] )

assume A11: ( S_{1}[p] & S_{1}[q] )
; :: thesis: S_{1}[p '&' q]

set p2 = Al2 -Cast p;

set q2 = Al2 -Cast q;

reconsider p2 = Al2 -Cast p, q2 = Al2 -Cast q as Element of CQC-WFF Al2 ;

( p '&' q is conjunctive & p2 '&' q2 is conjunctive ) ;

then A12: ( p = the_left_argument_of (p '&' q) & q = the_right_argument_of (p '&' q) & p2 = the_left_argument_of (p2 '&' q2) & q2 = the_right_argument_of (p2 '&' q2) ) by QC_LANG1:def 25, QC_LANG1:def 26;

hence still_not-bound_in (p '&' q) = (still_not-bound_in p) \/ (still_not-bound_in q) by QC_LANG1:def 20, QC_LANG3:9

.= still_not-bound_in (Al2 -Cast (p '&' q)) by A11, A12, QC_LANG1:def 20, QC_LANG3:9 ;

:: thesis: verum

end;assume A11: ( S

set p2 = Al2 -Cast p;

set q2 = Al2 -Cast q;

reconsider p2 = Al2 -Cast p, q2 = Al2 -Cast q as Element of CQC-WFF Al2 ;

( p '&' q is conjunctive & p2 '&' q2 is conjunctive ) ;

then A12: ( p = the_left_argument_of (p '&' q) & q = the_right_argument_of (p '&' q) & p2 = the_left_argument_of (p2 '&' q2) & q2 = the_right_argument_of (p2 '&' q2) ) by QC_LANG1:def 25, QC_LANG1:def 26;

hence still_not-bound_in (p '&' q) = (still_not-bound_in p) \/ (still_not-bound_in q) by QC_LANG1:def 20, QC_LANG3:9

.= still_not-bound_in (Al2 -Cast (p '&' q)) by A11, A12, QC_LANG1:def 20, QC_LANG3:9 ;

:: thesis: verum

for p being Element of CQC-WFF Al st S

S

proof

then A15:
for p, q being Element of CQC-WFF Al
let x be bound_QC-variable of Al; :: thesis: for p being Element of CQC-WFF Al st S_{1}[p] holds

S_{1}[ All (x,p)]

let p be Element of CQC-WFF Al; :: thesis: ( S_{1}[p] implies S_{1}[ All (x,p)] )

assume A13: S_{1}[p]
; :: thesis: S_{1}[ All (x,p)]

set x2 = Al2 -Cast x;

set p2 = Al2 -Cast p;

reconsider p2 = Al2 -Cast p as Element of CQC-WFF Al2 ;

reconsider x2 = Al2 -Cast x as bound_QC-variable of Al2 ;

( All (x,p) is universal & All (x2,p2) is universal ) ;

then A14: ( p = the_scope_of (All (x,p)) & x = bound_in (All (x,p)) & p2 = the_scope_of (All (x2,p2)) & x2 = bound_in (All (x2,p2)) ) by QC_LANG1:def 27, QC_LANG1:def 28;

then still_not-bound_in (All (x,p)) = (still_not-bound_in p) \ {x} by QC_LANG3:11, QC_LANG1:def 21

.= still_not-bound_in (Al2 -Cast (All (x,p))) by A13, A14, QC_LANG1:def 21, QC_LANG3:11 ;

hence S_{1}[ All (x,p)]
; :: thesis: verum

end;S

let p be Element of CQC-WFF Al; :: thesis: ( S

assume A13: S

set x2 = Al2 -Cast x;

set p2 = Al2 -Cast p;

reconsider p2 = Al2 -Cast p as Element of CQC-WFF Al2 ;

reconsider x2 = Al2 -Cast x as bound_QC-variable of Al2 ;

( All (x,p) is universal & All (x2,p2) is universal ) ;

then A14: ( p = the_scope_of (All (x,p)) & x = bound_in (All (x,p)) & p2 = the_scope_of (All (x2,p2)) & x2 = bound_in (All (x2,p2)) ) by QC_LANG1:def 27, QC_LANG1:def 28;

then still_not-bound_in (All (x,p)) = (still_not-bound_in p) \ {x} by QC_LANG3:11, QC_LANG1:def 21

.= still_not-bound_in (Al2 -Cast (All (x,p))) by A13, A14, QC_LANG1:def 21, QC_LANG3:11 ;

hence S

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

( S

for p being Element of CQC-WFF Al holds S

hence for p being Element of CQC-WFF Al holds still_not-bound_in p = still_not-bound_in (Al2 -Cast p) ; :: thesis: verum