let A be QC-alphabet ; for X being Subset of (CQC-WFF A)
for F, G being Element of CQC-WFF A st F is closed & X \/ {F} |- G holds
X |- F => G
let X be Subset of (CQC-WFF A); for F, G being Element of CQC-WFF A st F is closed & X \/ {F} |- G holds
X |- F => G
let F, G be Element of CQC-WFF A; ( F is closed & X \/ {F} |- G implies X |- F => G )
assume that
A1:
F is closed
and
A2:
X \/ {F} |- G
; X |- F => G
G in Cn (X \/ {F})
by A2;
then consider f being FinSequence of [:(CQC-WFF A),Proof_Step_Kinds:] such that
A3:
f is_a_proof_wrt X \/ {F}
and
A4:
Effect f = G
by CQC_THE1:36;
f <> {}
by A3;
then A5:
G = (f . (len f)) `1
by A4, CQC_THE1:def 6;
defpred S1[ Nat] means ( 1 <= $1 & $1 <= len f implies for H being Element of CQC-WFF A st H = (f . $1) `1 holds
X |- F => H );
A6:
for n being Nat st ( for k being Nat st k < n holds
S1[k] ) holds
S1[n]
proof
let n be
Nat;
( ( for k being Nat st k < n holds
S1[k] ) implies S1[n] )
assume A7:
for
k being
Nat st
k < n & 1
<= k &
k <= len f holds
for
H being
Element of
CQC-WFF A st
H = (f . k) `1 holds
X |- F => H
;
S1[n]
assume that A8:
1
<= n
and A9:
n <= len f
;
for H being Element of CQC-WFF A st H = (f . n) `1 holds
X |- F => H
A10:
f,
n is_a_correct_step_wrt X \/ {F}
by A3, A8, A9;
let H be
Element of
CQC-WFF A;
( H = (f . n) `1 implies X |- F => H )
assume A11:
H = (f . n) `1
;
X |- F => H
now X |- F => H
not not
(f . n) `2 = 0 & ... & not
(f . n) `2 = 9
by A8, A9, CQC_THE1:23;
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 )
;
suppose
(f . n) `2 = 7
;
X |- F => Hthen consider i,
j being
Nat,
p,
q being
Element of
CQC-WFF A such that A15:
1
<= i
and A16:
i < n
and A17:
1
<= j
and A18:
j < i
and A19:
p = (f . j) `1
and A20:
q = H
and A21:
(f . i) `1 = p => q
by A11, A10, CQC_THE1:def 4;
i <= len f
by A9, A16, XXREAL_0:2;
then A22:
X |- F => (p => q)
by A7, A15, A16, A21;
X |- (F => (p => q)) => ((F => p) => (F => q))
by CQC_THE1:59;
then A23:
X |- (F => p) => (F => q)
by A22, CQC_THE1:55;
j < n
by A16, A18, XXREAL_0:2;
then A24:
j <= len f
by A9, XXREAL_0:2;
j < n
by A16, A18, XXREAL_0:2;
then
X |- F => p
by A7, A17, A19, A24;
hence
X |- F => H
by A20, A23, CQC_THE1:55;
verum end; suppose
(f . n) `2 = 8
;
X |- F => Hthen consider i being
Nat,
p,
q being
Element of
CQC-WFF A,
x being
bound_QC-variable of
A such that A25:
1
<= i
and A26:
i < n
and A27:
(f . i) `1 = p => q
and A28:
not
x in still_not-bound_in p
and A29:
H = p => (All (x,q))
by A11, A10, CQC_THE1:def 4;
A30:
X |- (All (x,(p => q))) => (p => (All (x,q)))
by A28, Th74, CQC_THE1:59;
not
x in still_not-bound_in F
by A1, QC_LANG1:def 31;
then A31:
X |- (All (x,(F => (p => q)))) => (F => (All (x,(p => q))))
by Th74, CQC_THE1:59;
i <= len f
by A9, A26, XXREAL_0:2;
then
X |- All (
x,
(F => (p => q)))
by A7, A25, A26, A27, Th90;
then
X |- F => (All (x,(p => q)))
by A31, CQC_THE1:55;
hence
X |- F => H
by A29, A30, LUKASI_1:59;
verum end; suppose
(f . n) `2 = 9
;
X |- F => Hthen consider i being
Nat,
x,
y being
bound_QC-variable of
A,
s being
QC-formula of
A such that A32:
1
<= i
and A33:
i < n
and A34:
(
s . x in CQC-WFF A &
s . y in CQC-WFF A )
and A35:
not
x in still_not-bound_in s
and A36:
s . x = (f . i) `1
and A37:
H = s . y
by A11, A10, CQC_THE1:def 4;
reconsider s1 =
s . x,
s2 =
s . y as
Element of
CQC-WFF A by A34;
A38:
X |- (All (x,s1)) => s2
by A35, Th25, CQC_THE1:59;
not
x in still_not-bound_in F
by A1, QC_LANG1:def 31;
then A39:
X |- (All (x,(F => s1))) => (F => (All (x,s1)))
by Th74, CQC_THE1:59;
i <= len f
by A9, A33, XXREAL_0:2;
then
X |- All (
x,
(F => s1))
by A7, A32, A33, A36, Th90;
then
X |- F => (All (x,s1))
by A39, CQC_THE1:55;
hence
X |- F => H
by A37, A38, LUKASI_1:59;
verum end; end; end;
hence
X |- F => H
;
verum
end;
A40:
for n being Nat holds S1[n]
from NAT_1:sch 4(A6);
1 <= len f
by A3, CQC_THE1:25;
hence
X |- F => G
by A40, A5; verum