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