let Al be QC-alphabet ; :: thesis: for X being Subset of (CQC-WFF Al)

for p being Element of CQC-WFF Al st p in Cn X holds

ex Y being Subset of (CQC-WFF Al) st

( Y c= X & Y is finite & p in Cn Y )

let X be Subset of (CQC-WFF Al); :: thesis: for p being Element of CQC-WFF Al st p in Cn X holds

ex Y being Subset of (CQC-WFF Al) st

( Y c= X & Y is finite & p in Cn Y )

let p be Element of CQC-WFF Al; :: thesis: ( p in Cn X implies ex Y being Subset of (CQC-WFF Al) st

( Y c= X & Y is finite & p in Cn Y ) )

assume p in Cn X ; :: thesis: ex Y being Subset of (CQC-WFF Al) st

( Y c= X & Y is finite & p in Cn Y )

then consider f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] such that

A1: f is_a_proof_wrt X and

A2: Effect f = p by Th32;

A3: f <> {} by A1;

consider A being set such that

A4: A is finite and

A5: A c= CQC-WFF Al and

A6: rng f c= [:A,Proof_Step_Kinds:] by FINSEQ_1:def 4, FINSET_1:14;

reconsider Z = A as Subset of (CQC-WFF Al) by A5;

take Y = Z /\ X; :: thesis: ( Y c= X & Y is finite & p in Cn Y )

thus Y c= X by XBOOLE_1:17; :: thesis: ( Y is finite & p in Cn Y )

thus Y is finite by A4; :: thesis: p in Cn Y

for n being Nat st 1 <= n & n <= len f holds

f,n is_a_correct_step_wrt Y

then p in { q where q is Element of CQC-WFF Al : ex f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st

( f is_a_proof_wrt Y & Effect f = q ) } by A2;

hence p in Cn Y by Th31; :: thesis: verum

for p being Element of CQC-WFF Al st p in Cn X holds

ex Y being Subset of (CQC-WFF Al) st

( Y c= X & Y is finite & p in Cn Y )

let X be Subset of (CQC-WFF Al); :: thesis: for p being Element of CQC-WFF Al st p in Cn X holds

ex Y being Subset of (CQC-WFF Al) st

( Y c= X & Y is finite & p in Cn Y )

let p be Element of CQC-WFF Al; :: thesis: ( p in Cn X implies ex Y being Subset of (CQC-WFF Al) st

( Y c= X & Y is finite & p in Cn Y ) )

assume p in Cn X ; :: thesis: ex Y being Subset of (CQC-WFF Al) st

( Y c= X & Y is finite & p in Cn Y )

then consider f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] such that

A1: f is_a_proof_wrt X and

A2: Effect f = p by Th32;

A3: f <> {} by A1;

consider A being set such that

A4: A is finite and

A5: A c= CQC-WFF Al and

A6: rng f c= [:A,Proof_Step_Kinds:] by FINSEQ_1:def 4, FINSET_1:14;

reconsider Z = A as Subset of (CQC-WFF Al) by A5;

take Y = Z /\ X; :: thesis: ( Y c= X & Y is finite & p in Cn Y )

thus Y c= X by XBOOLE_1:17; :: thesis: ( Y is finite & p in Cn Y )

thus Y is finite by A4; :: thesis: p in Cn Y

for n being Nat st 1 <= n & n <= len f holds

f,n is_a_correct_step_wrt Y

proof

then
f is_a_proof_wrt Y
by A3;
let n be Nat; :: thesis: ( 1 <= n & n <= len f implies f,n is_a_correct_step_wrt Y )

assume A7: ( 1 <= n & n <= len f ) ; :: thesis: f,n is_a_correct_step_wrt Y

then A8: f,n is_a_correct_step_wrt X by A1;

not not (f . n) `2 = 0 & ... & not (f . n) `2 = 9 by A7, Th19;

end;assume A7: ( 1 <= n & n <= len f ) ; :: thesis: f,n is_a_correct_step_wrt Y

then A8: f,n is_a_correct_step_wrt X by A1;

not not (f . n) `2 = 0 & ... & not (f . n) `2 = 9 by A7, Th19;

per cases then
( (f . n) `2 = 0 or (f . n) `2 = 1 or (f . n) `2 = 2 or (f . n) `2 = 3 or (f . n) `2 = 4 or (f . n) `2 = 5 or (f . n) `2 = 6 or (f . n) `2 = 7 or (f . n) `2 = 8 or (f . n) `2 = 9 )
;

:: according to CQC_THE1:def 4end;

:: according to CQC_THE1:def 4

case
(f . n) `2 = 0
; :: thesis: (f . n) `1 in Y

then A9:
(f . n) `1 in X
by A8, Def4;

n in Seg (len f) by A7, FINSEQ_1:1;

then n in dom f by FINSEQ_1:def 3;

then f . n in rng f by FUNCT_1:def 3;

then (f . n) `1 in A by A6, MCART_1:10;

hence (f . n) `1 in Y by A9, XBOOLE_0:def 4; :: thesis: verum

end;n in Seg (len f) by A7, FINSEQ_1:1;

then n in dom f by FINSEQ_1:def 3;

then f . n in rng f by FUNCT_1:def 3;

then (f . n) `1 in A by A6, MCART_1:10;

hence (f . n) `1 in Y by A9, XBOOLE_0:def 4; :: thesis: verum

case
(f . n) `2 = 2
; :: thesis: ex p being Element of CQC-WFF Al st (f . n) `1 = (('not' p) => p) => p

hence
ex p being Element of CQC-WFF Al st (f . n) `1 = (('not' p) => p) => p
by A8, Def4; :: thesis: verum

end;case
(f . n) `2 = 3
; :: thesis: ex p, q being Element of CQC-WFF Al st (f . n) `1 = p => (('not' p) => q)

hence
ex p, q being Element of CQC-WFF Al st (f . n) `1 = p => (('not' p) => q)
by A8, Def4; :: thesis: verum

end;case
(f . n) `2 = 4
; :: thesis: ex p, q, r being Element of CQC-WFF Al st (f . n) `1 = (p => q) => (('not' (q '&' r)) => ('not' (p '&' r)))

hence
ex p, q, r being Element of CQC-WFF Al st (f . n) `1 = (p => q) => (('not' (q '&' r)) => ('not' (p '&' r)))
by A8, Def4; :: thesis: verum

end;case
(f . n) `2 = 5
; :: thesis: ex p, q being Element of CQC-WFF Al st (f . n) `1 = (p '&' q) => (q '&' p)

hence
ex p, q being Element of CQC-WFF Al st (f . n) `1 = (p '&' q) => (q '&' p)
by A8, Def4; :: thesis: verum

end;case
(f . n) `2 = 6
; :: thesis: ex p being Element of CQC-WFF Al ex x being bound_QC-variable of Al st (f . n) `1 = (All (x,p)) => p

hence
ex p being Element of CQC-WFF Al ex x being bound_QC-variable of Al st (f . n) `1 = (All (x,p)) => p
by A8, Def4; :: thesis: verum

end;case
(f . n) `2 = 7
; :: thesis: ex i, j being Nat ex p, q being Element of CQC-WFF Al st

( 1 <= i & i < n & 1 <= j & j < i & p = (f . j) `1 & q = (f . n) `1 & (f . i) `1 = p => q )

( 1 <= i & i < n & 1 <= j & j < i & p = (f . j) `1 & q = (f . n) `1 & (f . i) `1 = p => q )

hence
ex i, j being Nat ex p, q being Element of CQC-WFF Al st

( 1 <= i & i < n & 1 <= j & j < i & p = (f . j) `1 & q = (f . n) `1 & (f . i) `1 = p => q ) by A8, Def4; :: thesis: verum

end;( 1 <= i & i < n & 1 <= j & j < i & p = (f . j) `1 & q = (f . n) `1 & (f . i) `1 = p => q ) by A8, Def4; :: thesis: verum

case
(f . n) `2 = 8
; :: thesis: ex i being Nat ex p, q being Element of CQC-WFF Al ex x being bound_QC-variable of Al st

( 1 <= i & i < n & (f . i) `1 = p => q & not x in still_not-bound_in p & (f . n) `1 = p => (All (x,q)) )

( 1 <= i & i < n & (f . i) `1 = p => q & not x in still_not-bound_in p & (f . n) `1 = p => (All (x,q)) )

hence
ex i being Nat ex p, q being Element of CQC-WFF Al ex x being bound_QC-variable of Al st

( 1 <= i & i < n & (f . i) `1 = p => q & not x in still_not-bound_in p & (f . n) `1 = p => (All (x,q)) ) by A8, Def4; :: thesis: verum

end;( 1 <= i & i < n & (f . i) `1 = p => q & not x in still_not-bound_in p & (f . n) `1 = p => (All (x,q)) ) by A8, Def4; :: thesis: verum

case
(f . n) `2 = 9
; :: thesis: ex i being Nat ex x, y being bound_QC-variable of Al ex s being QC-formula of Al st

( 1 <= i & i < n & s . x in CQC-WFF Al & s . y in CQC-WFF Al & not x in still_not-bound_in s & s . x = (f . i) `1 & s . y = (f . n) `1 )

( 1 <= i & i < n & s . x in CQC-WFF Al & s . y in CQC-WFF Al & not x in still_not-bound_in s & s . x = (f . i) `1 & s . y = (f . n) `1 )

hence
ex i being Nat ex x, y being bound_QC-variable of Al ex s being QC-formula of Al st

( 1 <= i & i < n & s . x in CQC-WFF Al & s . y in CQC-WFF Al & not x in still_not-bound_in s & s . x = (f . i) `1 & s . y = (f . n) `1 ) by A8, Def4; :: thesis: verum

end;( 1 <= i & i < n & s . x in CQC-WFF Al & s . y in CQC-WFF Al & not x in still_not-bound_in s & s . x = (f . i) `1 & s . y = (f . n) `1 ) by A8, Def4; :: thesis: verum

then p in { q where q is Element of CQC-WFF Al : ex f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st

( f is_a_proof_wrt Y & Effect f = q ) } by A2;

hence p in Cn Y by Th31; :: thesis: verum