let Al be QC-alphabet ; :: thesis: for p being Element of CQC-WFF Al

for X being Subset of (CQC-WFF Al) st p is_formal_provable_from X holds

X |= p

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

X |= p

let X be Subset of (CQC-WFF Al); :: thesis: ( p is_formal_provable_from X implies X |= p )

assume p is_formal_provable_from X ; :: thesis: X |= p

then consider f being FinSequence of CQC-WFF Al such that

A1: rng (Ant f) c= X and

A2: Suc f = p and

A3: |- f ;

consider PR being FinSequence of [:(set_of_CQC-WFF-seq Al),Proof_Step_Kinds:] such that

A4: PR is a_proof and

A5: f = (PR . (len PR)) `1 by A3;

PR <> {} by A4;

then A6: 1 <= len PR by FINSEQ_1:20;

defpred S_{1}[ Nat] means ( $1 <= len PR implies for m being Nat st 1 <= m & m <= $1 holds

ex g being FinSequence of CQC-WFF Al st

( g = (PR . m) `1 & Ant g |= Suc g ) );

A7: for k being Nat st S_{1}[k] holds

S_{1}[k + 1]
_{1}[ 0 ]
;

for k being Nat holds S_{1}[k]
from NAT_1:sch 2(A67, A7);

then consider g being FinSequence of CQC-WFF Al such that

A68: g = (PR . (len PR)) `1 and

A69: Ant g |= Suc g by A6;

let A be non empty set ; :: according to CALCUL_1:def 12 :: thesis: for J being interpretation of Al,A

for v being Element of Valuations_in (Al,A) st J,v |= X holds

J,v |= p

let J be interpretation of Al,A; :: thesis: for v being Element of Valuations_in (Al,A) st J,v |= X holds

J,v |= p

let v be Element of Valuations_in (Al,A); :: thesis: ( J,v |= X implies J,v |= p )

assume J,v |= X ; :: thesis: J,v |= p

then for p being Element of CQC-WFF Al st p in rng (Ant f) holds

J,v |= p by A1;

then J,v |= rng (Ant f) ;

then J,v |= Ant g by A5, A68;

hence J,v |= p by A2, A5, A68, A69; :: thesis: verum

for X being Subset of (CQC-WFF Al) st p is_formal_provable_from X holds

X |= p

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

X |= p

let X be Subset of (CQC-WFF Al); :: thesis: ( p is_formal_provable_from X implies X |= p )

assume p is_formal_provable_from X ; :: thesis: X |= p

then consider f being FinSequence of CQC-WFF Al such that

A1: rng (Ant f) c= X and

A2: Suc f = p and

A3: |- f ;

consider PR being FinSequence of [:(set_of_CQC-WFF-seq Al),Proof_Step_Kinds:] such that

A4: PR is a_proof and

A5: f = (PR . (len PR)) `1 by A3;

PR <> {} by A4;

then A6: 1 <= len PR by FINSEQ_1:20;

defpred S

ex g being FinSequence of CQC-WFF Al st

( g = (PR . m) `1 & Ant g |= Suc g ) );

A7: for k being Nat st S

S

proof

A67:
S
let k be Nat; :: thesis: ( S_{1}[k] implies S_{1}[k + 1] )

assume A8: S_{1}[k]
; :: thesis: S_{1}[k + 1]

assume A9: k + 1 <= len PR ; :: thesis: for m being Nat st 1 <= m & m <= k + 1 holds

ex g being FinSequence of CQC-WFF Al st

( g = (PR . m) `1 & Ant g |= Suc g )

A10: k <= k + 1 by NAT_1:11;

let m be Nat; :: thesis: ( 1 <= m & m <= k + 1 implies ex g being FinSequence of CQC-WFF Al st

( g = (PR . m) `1 & Ant g |= Suc g ) )

assume that

A11: 1 <= m and

A12: m <= k + 1 ; :: thesis: ex g being FinSequence of CQC-WFF Al st

( g = (PR . m) `1 & Ant g |= Suc g )

A13: m <= len PR by A9, A12, XXREAL_0:2;

( g = (PR . m) `1 & Ant g |= Suc g ) ) by A8, A9, A11, A10, XXREAL_0:2;

hence ex g being FinSequence of CQC-WFF Al st

( g = (PR . m) `1 & Ant g |= Suc g ) by A12, A14, NAT_1:8; :: thesis: verum

end;assume A8: S

assume A9: k + 1 <= len PR ; :: thesis: for m being Nat st 1 <= m & m <= k + 1 holds

ex g being FinSequence of CQC-WFF Al st

( g = (PR . m) `1 & Ant g |= Suc g )

A10: k <= k + 1 by NAT_1:11;

let m be Nat; :: thesis: ( 1 <= m & m <= k + 1 implies ex g being FinSequence of CQC-WFF Al st

( g = (PR . m) `1 & Ant g |= Suc g ) )

assume that

A11: 1 <= m and

A12: m <= k + 1 ; :: thesis: ex g being FinSequence of CQC-WFF Al st

( g = (PR . m) `1 & Ant g |= Suc g )

A13: m <= len PR by A9, A12, XXREAL_0:2;

A14: now :: thesis: ( m = k + 1 implies ex g being object st

( g = (PR . m) `1 & ex g being FinSequence of CQC-WFF Al st

( g = (PR . m) `1 & Ant g |= Suc g ) ) )

( m <= k implies ex g being FinSequence of CQC-WFF Al st ( g = (PR . m) `1 & ex g being FinSequence of CQC-WFF Al st

( g = (PR . m) `1 & Ant g |= Suc g ) ) )

assume A15:
m = k + 1
; :: thesis: ex g being object st

( g = (PR . m) `1 & ex g being FinSequence of CQC-WFF Al st

( g = (PR . m) `1 & Ant g |= Suc g ) )

take g = (PR . m) `1 ; :: thesis: ( g = (PR . m) `1 & ex g being FinSequence of CQC-WFF Al st

( g = (PR . m) `1 & Ant g |= Suc g ) )

thus g = (PR . m) `1 ; :: thesis: ex g being FinSequence of CQC-WFF Al st

( g = (PR . m) `1 & Ant g |= Suc g )

reconsider g = (PR . m) `1 as FinSequence of CQC-WFF Al by A11, A13, Lm3;

A16: PR,m is_a_correct_step by A4, A11, A13;

( g = (PR . m) `1 & Ant g |= Suc g ) ; :: thesis: verum

end;( g = (PR . m) `1 & ex g being FinSequence of CQC-WFF Al st

( g = (PR . m) `1 & Ant g |= Suc g ) )

take g = (PR . m) `1 ; :: thesis: ( g = (PR . m) `1 & ex g being FinSequence of CQC-WFF Al st

( g = (PR . m) `1 & Ant g |= Suc g ) )

thus g = (PR . m) `1 ; :: thesis: ex g being FinSequence of CQC-WFF Al st

( g = (PR . m) `1 & Ant g |= Suc g )

reconsider g = (PR . m) `1 as FinSequence of CQC-WFF Al by A11, A13, Lm3;

A16: PR,m is_a_correct_step by A4, A11, A13;

now :: thesis: Ant g |= Suc g

hence
ex g being FinSequence of CQC-WFF Al st
not not (PR . m) `2 = 0 & ... & not (PR . m) `2 = 9
by A11, A13, Th31;

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

end;

suppose
(PR . m) `2 = 0
; :: thesis: Ant g |= Suc g

then
ex f being FinSequence of CQC-WFF Al st

( Suc f is_tail_of Ant f & (PR . m) `1 = f ) by A16, Def7;

hence Ant g |= Suc g by Th15; :: thesis: verum

end;( Suc f is_tail_of Ant f & (PR . m) `1 = f ) by A16, Def7;

hence Ant g |= Suc g by Th15; :: thesis: verum

suppose
(PR . m) `2 = 1
; :: thesis: Ant g |= Suc g

then
ex f being FinSequence of CQC-WFF Al st g = f ^ <*(VERUM Al)*>
by A16, Def7;

hence Ant g |= Suc g by Th30; :: thesis: verum

end;hence Ant g |= Suc g by Th30; :: thesis: verum

suppose
(PR . m) `2 = 2
; :: thesis: Ant g |= Suc g

then consider i being Nat, f, f1 being FinSequence of CQC-WFF Al such that

A17: 1 <= i and

A18: i < m and

A19: ( Ant f is_Subsequence_of Ant f1 & Suc f = Suc f1 & (PR . i) `1 = f & (PR . m) `1 = f1 ) by A16, Def7;

i <= k by A15, A18, NAT_1:13;

then ex h being FinSequence of CQC-WFF Al st

( h = (PR . i) `1 & Ant h |= Suc h ) by A8, A9, A10, A17, XXREAL_0:2;

hence Ant g |= Suc g by A19, Th16; :: thesis: verum

end;A17: 1 <= i and

A18: i < m and

A19: ( Ant f is_Subsequence_of Ant f1 & Suc f = Suc f1 & (PR . i) `1 = f & (PR . m) `1 = f1 ) by A16, Def7;

i <= k by A15, A18, NAT_1:13;

then ex h being FinSequence of CQC-WFF Al st

( h = (PR . i) `1 & Ant h |= Suc h ) by A8, A9, A10, A17, XXREAL_0:2;

hence Ant g |= Suc g by A19, Th16; :: thesis: verum

suppose
(PR . m) `2 = 3
; :: thesis: Ant g |= Suc g

then consider i, j being Nat, f, f1 being FinSequence of CQC-WFF Al such that

A20: 1 <= i and

A21: i < m and

A22: 1 <= j and

A23: j < i and

A24: ( len f > 1 & len f1 > 1 & Ant (Ant f) = Ant (Ant f1) & 'not' (Suc (Ant f)) = Suc (Ant f1) & Suc f = Suc f1 & f = (PR . j) `1 & f1 = (PR . i) `1 ) and

A25: (Ant (Ant f)) ^ <*(Suc f)*> = (PR . m) `1 by A16, Def7;

A26: ( Ant g = Ant (Ant f) & Suc g = Suc f ) by A25, Th5;

A27: i <= k by A15, A21, NAT_1:13;

then j <= k by A23, XXREAL_0:2;

then A28: ex h1 being FinSequence of CQC-WFF Al st

( h1 = (PR . j) `1 & Ant h1 |= Suc h1 ) by A8, A9, A10, A22, XXREAL_0:2;

ex h being FinSequence of CQC-WFF Al st

( h = (PR . i) `1 & Ant h |= Suc h ) by A8, A9, A10, A20, A27, XXREAL_0:2;

hence Ant g |= Suc g by A24, A28, A26, Th18; :: thesis: verum

end;A20: 1 <= i and

A21: i < m and

A22: 1 <= j and

A23: j < i and

A24: ( len f > 1 & len f1 > 1 & Ant (Ant f) = Ant (Ant f1) & 'not' (Suc (Ant f)) = Suc (Ant f1) & Suc f = Suc f1 & f = (PR . j) `1 & f1 = (PR . i) `1 ) and

A25: (Ant (Ant f)) ^ <*(Suc f)*> = (PR . m) `1 by A16, Def7;

A26: ( Ant g = Ant (Ant f) & Suc g = Suc f ) by A25, Th5;

A27: i <= k by A15, A21, NAT_1:13;

then j <= k by A23, XXREAL_0:2;

then A28: ex h1 being FinSequence of CQC-WFF Al st

( h1 = (PR . j) `1 & Ant h1 |= Suc h1 ) by A8, A9, A10, A22, XXREAL_0:2;

ex h being FinSequence of CQC-WFF Al st

( h = (PR . i) `1 & Ant h |= Suc h ) by A8, A9, A10, A20, A27, XXREAL_0:2;

hence Ant g |= Suc g by A24, A28, A26, Th18; :: thesis: verum

suppose
(PR . m) `2 = 4
; :: thesis: Ant g |= Suc g

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

A29: 1 <= i and

A30: i < m and

A31: 1 <= j and

A32: j < i and

A33: ( len f > 1 & Ant f = Ant f1 & Suc (Ant f) = 'not' p & 'not' (Suc f) = Suc f1 & f = (PR . j) `1 & f1 = (PR . i) `1 ) and

A34: (Ant (Ant f)) ^ <*p*> = (PR . m) `1 by A16, Def7;

A35: ( Ant g = Ant (Ant f) & Suc g = p ) by A34, Th5;

A36: i <= k by A15, A30, NAT_1:13;

then j <= k by A32, XXREAL_0:2;

then A37: ex h1 being FinSequence of CQC-WFF Al st

( h1 = (PR . j) `1 & Ant h1 |= Suc h1 ) by A8, A9, A10, A31, XXREAL_0:2;

ex h being FinSequence of CQC-WFF Al st

( h = (PR . i) `1 & Ant h |= Suc h ) by A8, A9, A10, A29, A36, XXREAL_0:2;

hence Ant g |= Suc g by A33, A37, A35, Th19; :: thesis: verum

end;A29: 1 <= i and

A30: i < m and

A31: 1 <= j and

A32: j < i and

A33: ( len f > 1 & Ant f = Ant f1 & Suc (Ant f) = 'not' p & 'not' (Suc f) = Suc f1 & f = (PR . j) `1 & f1 = (PR . i) `1 ) and

A34: (Ant (Ant f)) ^ <*p*> = (PR . m) `1 by A16, Def7;

A35: ( Ant g = Ant (Ant f) & Suc g = p ) by A34, Th5;

A36: i <= k by A15, A30, NAT_1:13;

then j <= k by A32, XXREAL_0:2;

then A37: ex h1 being FinSequence of CQC-WFF Al st

( h1 = (PR . j) `1 & Ant h1 |= Suc h1 ) by A8, A9, A10, A31, XXREAL_0:2;

ex h being FinSequence of CQC-WFF Al st

( h = (PR . i) `1 & Ant h |= Suc h ) by A8, A9, A10, A29, A36, XXREAL_0:2;

hence Ant g |= Suc g by A33, A37, A35, Th19; :: thesis: verum

suppose
(PR . m) `2 = 5
; :: thesis: Ant g |= Suc g

then consider i, j being Nat, f, f1 being FinSequence of CQC-WFF Al such that

A38: 1 <= i and

A39: i < m and

A40: 1 <= j and

A41: j < i and

A42: ( Ant f = Ant f1 & f = (PR . j) `1 & f1 = (PR . i) `1 ) and

A43: (Ant f) ^ <*((Suc f) '&' (Suc f1))*> = (PR . m) `1 by A16, Def7;

A44: ( Ant g = Ant f & Suc g = (Suc f) '&' (Suc f1) ) by A43, Th5;

A45: i <= k by A15, A39, NAT_1:13;

then j <= k by A41, XXREAL_0:2;

then A46: ex h1 being FinSequence of CQC-WFF Al st

( h1 = (PR . j) `1 & Ant h1 |= Suc h1 ) by A8, A9, A10, A40, XXREAL_0:2;

ex h being FinSequence of CQC-WFF Al st

( h = (PR . i) `1 & Ant h |= Suc h ) by A8, A9, A10, A38, A45, XXREAL_0:2;

hence Ant g |= Suc g by A42, A46, A44, Th20; :: thesis: verum

end;A38: 1 <= i and

A39: i < m and

A40: 1 <= j and

A41: j < i and

A42: ( Ant f = Ant f1 & f = (PR . j) `1 & f1 = (PR . i) `1 ) and

A43: (Ant f) ^ <*((Suc f) '&' (Suc f1))*> = (PR . m) `1 by A16, Def7;

A44: ( Ant g = Ant f & Suc g = (Suc f) '&' (Suc f1) ) by A43, Th5;

A45: i <= k by A15, A39, NAT_1:13;

then j <= k by A41, XXREAL_0:2;

then A46: ex h1 being FinSequence of CQC-WFF Al st

( h1 = (PR . j) `1 & Ant h1 |= Suc h1 ) by A8, A9, A10, A40, XXREAL_0:2;

ex h being FinSequence of CQC-WFF Al st

( h = (PR . i) `1 & Ant h |= Suc h ) by A8, A9, A10, A38, A45, XXREAL_0:2;

hence Ant g |= Suc g by A42, A46, A44, Th20; :: thesis: verum

suppose
(PR . m) `2 = 6
; :: thesis: Ant g |= Suc g

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

A47: 1 <= i and

A48: i < m and

A49: ( p '&' q = Suc f & f = (PR . i) `1 ) and

A50: (Ant f) ^ <*p*> = (PR . m) `1 by A16, Def7;

i <= k by A15, A48, NAT_1:13;

then A51: ex h being FinSequence of CQC-WFF Al st

( h = (PR . i) `1 & Ant h |= Suc h ) by A8, A9, A10, A47, XXREAL_0:2;

( Ant g = Ant f & Suc g = p ) by A50, Th5;

hence Ant g |= Suc g by A49, A51, Th21; :: thesis: verum

end;A47: 1 <= i and

A48: i < m and

A49: ( p '&' q = Suc f & f = (PR . i) `1 ) and

A50: (Ant f) ^ <*p*> = (PR . m) `1 by A16, Def7;

i <= k by A15, A48, NAT_1:13;

then A51: ex h being FinSequence of CQC-WFF Al st

( h = (PR . i) `1 & Ant h |= Suc h ) by A8, A9, A10, A47, XXREAL_0:2;

( Ant g = Ant f & Suc g = p ) by A50, Th5;

hence Ant g |= Suc g by A49, A51, Th21; :: thesis: verum

suppose
(PR . m) `2 = 7
; :: thesis: Ant g |= Suc g

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

A52: 1 <= i and

A53: i < m and

A54: ( p '&' q = Suc f & f = (PR . i) `1 ) and

A55: (Ant f) ^ <*q*> = (PR . m) `1 by A16, Def7;

i <= k by A15, A53, NAT_1:13;

then A56: ex h being FinSequence of CQC-WFF Al st

( h = (PR . i) `1 & Ant h |= Suc h ) by A8, A9, A10, A52, XXREAL_0:2;

( Ant g = Ant f & Suc g = q ) by A55, Th5;

hence Ant g |= Suc g by A54, A56, Th22; :: thesis: verum

end;A52: 1 <= i and

A53: i < m and

A54: ( p '&' q = Suc f & f = (PR . i) `1 ) and

A55: (Ant f) ^ <*q*> = (PR . m) `1 by A16, Def7;

i <= k by A15, A53, NAT_1:13;

then A56: ex h being FinSequence of CQC-WFF Al st

( h = (PR . i) `1 & Ant h |= Suc h ) by A8, A9, A10, A52, XXREAL_0:2;

( Ant g = Ant f & Suc g = q ) by A55, Th5;

hence Ant g |= Suc g by A54, A56, Th22; :: thesis: verum

suppose
(PR . m) `2 = 8
; :: thesis: Ant g |= Suc g

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

A57: 1 <= i and

A58: i < m and

A59: ( Suc f = All (x,p) & f = (PR . i) `1 ) and

A60: (Ant f) ^ <*(p . (x,y))*> = (PR . m) `1 by A16, Def7;

i <= k by A15, A58, NAT_1:13;

then A61: ex h being FinSequence of CQC-WFF Al st

( h = (PR . i) `1 & Ant h |= Suc h ) by A8, A9, A10, A57, XXREAL_0:2;

( Ant g = Ant f & Suc g = p . (x,y) ) by A60, Th5;

hence Ant g |= Suc g by A59, A61, Th25; :: thesis: verum

end;A57: 1 <= i and

A58: i < m and

A59: ( Suc f = All (x,p) & f = (PR . i) `1 ) and

A60: (Ant f) ^ <*(p . (x,y))*> = (PR . m) `1 by A16, Def7;

i <= k by A15, A58, NAT_1:13;

then A61: ex h being FinSequence of CQC-WFF Al st

( h = (PR . i) `1 & Ant h |= Suc h ) by A8, A9, A10, A57, XXREAL_0:2;

( Ant g = Ant f & Suc g = p . (x,y) ) by A60, Th5;

hence Ant g |= Suc g by A59, A61, Th25; :: thesis: verum

suppose
(PR . m) `2 = 9
; :: thesis: Ant g |= Suc g

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

A62: 1 <= i and

A63: i < m and

A64: ( Suc f = p . (x,y) & not y in still_not-bound_in (Ant f) & not y in still_not-bound_in (All (x,p)) & f = (PR . i) `1 ) and

A65: (Ant f) ^ <*(All (x,p))*> = (PR . m) `1 by A16, Def7;

i <= k by A15, A63, NAT_1:13;

then A66: ex h being FinSequence of CQC-WFF Al st

( h = (PR . i) `1 & Ant h |= Suc h ) by A8, A9, A10, A62, XXREAL_0:2;

( Ant g = Ant f & Suc g = All (x,p) ) by A65, Th5;

hence Ant g |= Suc g by A64, A66, Th29; :: thesis: verum

end;A62: 1 <= i and

A63: i < m and

A64: ( Suc f = p . (x,y) & not y in still_not-bound_in (Ant f) & not y in still_not-bound_in (All (x,p)) & f = (PR . i) `1 ) and

A65: (Ant f) ^ <*(All (x,p))*> = (PR . m) `1 by A16, Def7;

i <= k by A15, A63, NAT_1:13;

then A66: ex h being FinSequence of CQC-WFF Al st

( h = (PR . i) `1 & Ant h |= Suc h ) by A8, A9, A10, A62, XXREAL_0:2;

( Ant g = Ant f & Suc g = All (x,p) ) by A65, Th5;

hence Ant g |= Suc g by A64, A66, Th29; :: thesis: verum

( g = (PR . m) `1 & Ant g |= Suc g ) ; :: thesis: verum

( g = (PR . m) `1 & Ant g |= Suc g ) ) by A8, A9, A11, A10, XXREAL_0:2;

hence ex g being FinSequence of CQC-WFF Al st

( g = (PR . m) `1 & Ant g |= Suc g ) by A12, A14, NAT_1:8; :: thesis: verum

for k being Nat holds S

then consider g being FinSequence of CQC-WFF Al such that

A68: g = (PR . (len PR)) `1 and

A69: Ant g |= Suc g by A6;

let A be non empty set ; :: according to CALCUL_1:def 12 :: thesis: for J being interpretation of Al,A

for v being Element of Valuations_in (Al,A) st J,v |= X holds

J,v |= p

let J be interpretation of Al,A; :: thesis: for v being Element of Valuations_in (Al,A) st J,v |= X holds

J,v |= p

let v be Element of Valuations_in (Al,A); :: thesis: ( J,v |= X implies J,v |= p )

assume J,v |= X ; :: thesis: J,v |= p

then for p being Element of CQC-WFF Al st p in rng (Ant f) holds

J,v |= p by A1;

then J,v |= rng (Ant f) ;

then J,v |= Ant g by A5, A68;

hence J,v |= p by A2, A5, A68, A69; :: thesis: verum