let Al be QC-alphabet ; :: thesis: for l being Nat

for X being Subset of (CQC-WFF Al)

for f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st f is_a_proof_wrt X & 1 <= l & l <= len f holds

(f . l) `1 in Cn X

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

for f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st f is_a_proof_wrt X & 1 <= l & l <= len f holds

(f . l) `1 in Cn X

let X be Subset of (CQC-WFF Al); :: thesis: for f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st f is_a_proof_wrt X & 1 <= l & l <= len f holds

(f . l) `1 in Cn X

let f be FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:]; :: thesis: ( f is_a_proof_wrt X & 1 <= l & l <= len f implies (f . l) `1 in Cn X )

assume that

A1: f is_a_proof_wrt X and

A2: ( 1 <= l & l <= len f ) ; :: thesis: (f . l) `1 in Cn X

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

(f . n) `1 in Cn X

for X being Subset of (CQC-WFF Al)

for f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st f is_a_proof_wrt X & 1 <= l & l <= len f holds

(f . l) `1 in Cn X

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

for f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st f is_a_proof_wrt X & 1 <= l & l <= len f holds

(f . l) `1 in Cn X

let X be Subset of (CQC-WFF Al); :: thesis: for f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st f is_a_proof_wrt X & 1 <= l & l <= len f holds

(f . l) `1 in Cn X

let f be FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:]; :: thesis: ( f is_a_proof_wrt X & 1 <= l & l <= len f implies (f . l) `1 in Cn X )

assume that

A1: f is_a_proof_wrt X and

A2: ( 1 <= l & l <= len f ) ; :: thesis: (f . l) `1 in Cn X

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

(f . n) `1 in Cn X

proof

hence
(f . l) `1 in Cn X
by A2; :: thesis: verum
defpred S_{1}[ Nat] means ( 1 <= $1 & $1 <= len f implies (f . $1) `1 in Cn X );

A3: for n being Nat st ( for k being Nat st k < n holds

S_{1}[k] ) holds

S_{1}[n]
_{1}[n]
from NAT_1:sch 4(A3);

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

(f . n) `1 in Cn X ; :: thesis: verum

end;A3: for n being Nat st ( for k being Nat st k < n holds

S

S

proof

for n being Nat holds S
let n be Nat; :: thesis: ( ( for k being Nat st k < n holds

S_{1}[k] ) implies S_{1}[n] )

assume A4: for k being Nat st k < n holds

S_{1}[k]
; :: thesis: S_{1}[n]

assume that

A5: 1 <= n and

A6: n <= len f ; :: thesis: (f . n) `1 in Cn X

A7: f,n is_a_correct_step_wrt X by A1, A5, A6;

end;S

assume A4: for k being Nat st k < n holds

S

assume that

A5: 1 <= n and

A6: n <= len f ; :: thesis: (f . n) `1 in Cn X

A7: f,n is_a_correct_step_wrt X by A1, A5, A6;

now :: thesis: (f . n) `1 in Cn X

hence
(f . n) `1 in Cn X
; :: thesis: verum
not not (f . n) `2 = 0 & ... & not (f . n) `2 = 9
by A5, A6, Th19;

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

end;

suppose
(f . n) `2 = 0
; :: thesis: (f . n) `1 in Cn X

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

X c= Cn X by Th13;

hence (f . n) `1 in Cn X by A8; :: thesis: verum

end;X c= Cn X by Th13;

hence (f . n) `1 in Cn X by A8; :: thesis: verum

suppose
(f . n) `2 = 2
; :: thesis: (f . n) `1 in Cn X

then
ex p being Element of CQC-WFF Al st (f . n) `1 = (('not' p) => p) => p
by A7, Def4;

hence (f . n) `1 in Cn X by Th3; :: thesis: verum

end;hence (f . n) `1 in Cn X by Th3; :: thesis: verum

suppose
(f . n) `2 = 3
; :: thesis: (f . n) `1 in Cn X

then
ex p, q being Element of CQC-WFF Al st (f . n) `1 = p => (('not' p) => q)
by A7, Def4;

hence (f . n) `1 in Cn X by Th4; :: thesis: verum

end;hence (f . n) `1 in Cn X by Th4; :: thesis: verum

suppose
(f . n) `2 = 4
; :: thesis: (f . n) `1 in Cn X

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

hence (f . n) `1 in Cn X by Th5; :: thesis: verum

end;hence (f . n) `1 in Cn X by Th5; :: thesis: verum

suppose
(f . n) `2 = 5
; :: thesis: (f . n) `1 in Cn X

then
ex p, q being Element of CQC-WFF Al st (f . n) `1 = (p '&' q) => (q '&' p)
by A7, Def4;

hence (f . n) `1 in Cn X by Th6; :: thesis: verum

end;hence (f . n) `1 in Cn X by Th6; :: thesis: verum

suppose
(f . n) `2 = 6
; :: thesis: (f . n) `1 in Cn X

then
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 A7, Def4;

hence (f . n) `1 in Cn X by Th8; :: thesis: verum

end;hence (f . n) `1 in Cn X by Th8; :: thesis: verum

suppose
(f . n) `2 = 7
; :: thesis: (f . n) `1 in Cn X

then consider i, j being Nat, p, q being Element of CQC-WFF Al such that

A9: 1 <= i and

A10: i < n and

A11: 1 <= j and

A12: j < i and

A13: ( p = (f . j) `1 & q = (f . n) `1 & (f . i) `1 = p => q ) by A7, Def4;

A14: j < n by A10, A12, XXREAL_0:2;

A15: i <= len f by A6, A10, XXREAL_0:2;

then j <= len f by A12, XXREAL_0:2;

then A16: (f . j) `1 in Cn X by A4, A11, A14;

(f . i) `1 in Cn X by A4, A9, A10, A15;

hence (f . n) `1 in Cn X by A13, A16, Th7; :: thesis: verum

end;A9: 1 <= i and

A10: i < n and

A11: 1 <= j and

A12: j < i and

A13: ( p = (f . j) `1 & q = (f . n) `1 & (f . i) `1 = p => q ) by A7, Def4;

A14: j < n by A10, A12, XXREAL_0:2;

A15: i <= len f by A6, A10, XXREAL_0:2;

then j <= len f by A12, XXREAL_0:2;

then A16: (f . j) `1 in Cn X by A4, A11, A14;

(f . i) `1 in Cn X by A4, A9, A10, A15;

hence (f . n) `1 in Cn X by A13, A16, Th7; :: thesis: verum

suppose
(f . n) `2 = 8
; :: thesis: (f . n) `1 in Cn X

then consider i being Nat, p, q being Element of CQC-WFF Al, x being bound_QC-variable of Al such that

A17: 1 <= i and

A18: i < n and

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

i <= len f by A6, A18, XXREAL_0:2;

hence (f . n) `1 in Cn X by A4, A17, A18, A19, Th9; :: thesis: verum

end;A17: 1 <= i and

A18: i < n and

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

i <= len f by A6, A18, XXREAL_0:2;

hence (f . n) `1 in Cn X by A4, A17, A18, A19, Th9; :: thesis: verum

suppose
(f . n) `2 = 9
; :: thesis: (f . n) `1 in Cn X

then consider i being Nat, x, y being bound_QC-variable of Al, s being QC-formula of Al such that

A20: 1 <= i and

A21: i < n and

A22: ( 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 & (f . n) `1 = s . y ) by A7, Def4;

i <= len f by A6, A21, XXREAL_0:2;

hence (f . n) `1 in Cn X by A4, A20, A21, A22, Th10; :: thesis: verum

end;A20: 1 <= i and

A21: i < n and

A22: ( 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 & (f . n) `1 = s . y ) by A7, Def4;

i <= len f by A6, A21, XXREAL_0:2;

hence (f . n) `1 in Cn X by A4, A20, A21, A22, Th10; :: thesis: verum

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

(f . n) `1 in Cn X ; :: thesis: verum