let Al be QC-alphabet ; for n being Element of NAT
for X being Subset of (CQC-WFF Al)
for g, f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st 1 <= n & n <= len g & g,n is_a_correct_step_wrt X holds
f ^ g,n + (len f) is_a_correct_step_wrt X
let n be Element of NAT ; for X being Subset of (CQC-WFF Al)
for g, f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st 1 <= n & n <= len g & g,n is_a_correct_step_wrt X holds
f ^ g,n + (len f) is_a_correct_step_wrt X
let X be Subset of (CQC-WFF Al); for g, f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st 1 <= n & n <= len g & g,n is_a_correct_step_wrt X holds
f ^ g,n + (len f) is_a_correct_step_wrt X
let g, f be FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:]; ( 1 <= n & n <= len g & g,n is_a_correct_step_wrt X implies f ^ g,n + (len f) is_a_correct_step_wrt X )
assume that
A1:
1 <= n
and
A2:
n <= len g
and
A3:
g,n is_a_correct_step_wrt X
; f ^ g,n + (len f) is_a_correct_step_wrt X
n in Seg (len g)
by A1, A2, FINSEQ_1:1;
then
n in dom g
by FINSEQ_1:def 3;
then A4:
g . n = (f ^ g) . (n + (len f))
by FINSEQ_1:def 7;
n + (len f) <= (len f) + (len g)
by A2, XREAL_1:6;
then A5:
n + (len f) <= len (f ^ g)
by FINSEQ_1:22;
per cases
( ((f ^ g) . (n + (len f))) `2 = 0 or ((f ^ g) . (n + (len f))) `2 = 1 or ((f ^ g) . (n + (len f))) `2 = 2 or ((f ^ g) . (n + (len f))) `2 = 3 or ((f ^ g) . (n + (len f))) `2 = 4 or ((f ^ g) . (n + (len f))) `2 = 5 or ((f ^ g) . (n + (len f))) `2 = 6 or ((f ^ g) . (n + (len f))) `2 = 7 or ((f ^ g) . (n + (len f))) `2 = 8 or ((f ^ g) . (n + (len f))) `2 = 9 )
by A1, A5, Th23, NAT_1:12;
CQC_THE1:def 4case
((f ^ g) . (n + (len f))) `2 = 7
;
ex i, j being Element of NAT ex p, q being Element of CQC-WFF Al st
( 1 <= i & i < n + (len f) & 1 <= j & j < i & p = ((f ^ g) . j) `1 & q = ((f ^ g) . (n + (len f))) `1 & ((f ^ g) . i) `1 = p => q )then consider i,
j being
Element of
NAT ,
r,
t being
Element of
CQC-WFF Al such that A6:
1
<= i
and A7:
i < n
and A8:
1
<= j
and A9:
j < i
and A10:
(
r = (g . j) `1 &
t = (g . n) `1 &
(g . i) `1 = r => t )
by A3, A4, Def4;
A11:
( 1
<= i + (len f) &
i + (len f) < n + (len f) )
by A6, A7, NAT_1:12, XREAL_1:6;
A12:
( 1
<= j + (len f) &
j + (len f) < i + (len f) )
by A8, A9, NAT_1:12, XREAL_1:6;
A13:
i <= len g
by A2, A7, XXREAL_0:2;
then A14:
j <= len g
by A9, XXREAL_0:2;
A15:
i in Seg (len g)
by A6, A13, FINSEQ_1:1;
A16:
j in Seg (len g)
by A8, A14, FINSEQ_1:1;
A17:
i in dom g
by A15, FINSEQ_1:def 3;
A18:
j in dom g
by A16, FINSEQ_1:def 3;
A19:
g . i = (f ^ g) . (i + (len f))
by A17, FINSEQ_1:def 7;
g . j = (f ^ g) . (j + (len f))
by A18, FINSEQ_1:def 7;
hence
ex
i,
j being
Element of
NAT ex
p,
q being
Element of
CQC-WFF Al st
( 1
<= i &
i < n + (len f) & 1
<= j &
j < i &
p = ((f ^ g) . j) `1 &
q = ((f ^ g) . (n + (len f))) `1 &
((f ^ g) . i) `1 = p => q )
by A4, A10, A11, A12, A19;
verum end; case
((f ^ g) . (n + (len f))) `2 = 8
;
ex i being Element of NAT ex p, q being Element of CQC-WFF Al ex x being bound_QC-variable of Al st
( 1 <= i & i < n + (len f) & ((f ^ g) . i) `1 = p => q & not x in still_not-bound_in p & ((f ^ g) . (n + (len f))) `1 = p => (All (x,q)) )then consider i being
Element of
NAT ,
r,
t being
Element of
CQC-WFF Al,
x being
bound_QC-variable of
Al such that A20:
1
<= i
and A21:
i < n
and A22:
(
(g . i) `1 = r => t & not
x in still_not-bound_in r &
(g . n) `1 = r => (All (x,t)) )
by A3, A4, Def4;
A23:
( 1
<= (len f) + i &
(len f) + i < n + (len f) )
by A20, A21, NAT_1:12, XREAL_1:6;
i <= len g
by A2, A21, XXREAL_0:2;
then
i in Seg (len g)
by A20, FINSEQ_1:1;
then
i in dom g
by FINSEQ_1:def 3;
then
g . i = (f ^ g) . ((len f) + i)
by FINSEQ_1:def 7;
hence
ex
i being
Element of
NAT ex
p,
q being
Element of
CQC-WFF Al ex
x being
bound_QC-variable of
Al st
( 1
<= i &
i < n + (len f) &
((f ^ g) . i) `1 = p => q & not
x in still_not-bound_in p &
((f ^ g) . (n + (len f))) `1 = p => (All (x,q)) )
by A4, A22, A23;
verum end; case
((f ^ g) . (n + (len f))) `2 = 9
;
ex i being Element of NAT ex x, y being bound_QC-variable of Al ex s being QC-formula of Al st
( 1 <= i & i < n + (len f) & s . x in CQC-WFF Al & s . y in CQC-WFF Al & not x in still_not-bound_in s & s . x = ((f ^ g) . i) `1 & s . y = ((f ^ g) . (n + (len f))) `1 )then consider i being
Element of
NAT ,
x,
y being
bound_QC-variable of
Al,
s being
QC-formula of
Al such that A24:
1
<= i
and A25:
i < n
and A26:
(
s . x in CQC-WFF Al &
s . y in CQC-WFF Al & not
x in still_not-bound_in s &
s . x = (g . i) `1 &
(g . n) `1 = s . y )
by A3, A4, Def4;
A27:
( 1
<= (len f) + i &
(len f) + i < n + (len f) )
by A24, A25, NAT_1:12, XREAL_1:6;
i <= len g
by A2, A25, XXREAL_0:2;
then
i in Seg (len g)
by A24, FINSEQ_1:1;
then
i in dom g
by FINSEQ_1:def 3;
then
g . i = (f ^ g) . ((len f) + i)
by FINSEQ_1:def 7;
hence
ex
i being
Element of
NAT ex
x,
y being
bound_QC-variable of
Al ex
s being
QC-formula of
Al st
( 1
<= i &
i < n + (len f) &
s . x in CQC-WFF Al &
s . y in CQC-WFF Al & not
x in still_not-bound_in s &
s . x = ((f ^ g) . i) `1 &
s . y = ((f ^ g) . (n + (len f))) `1 )
by A4, A26, A27;
verum end;