let n be Element of NAT ; for X being Subset of CQC-WFF
for g, f being FinSequence of [:CQC-WFF ,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 ; for g, f being FinSequence of [:CQC-WFF ,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 ,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
A4:
n in Seg (len g)
by A1, A2, FINSEQ_1:3;
A5:
n in dom g
by A4, FINSEQ_1:def 3;
A6:
g . n = (f ^ g) . (n + (len f))
by A5, FINSEQ_1:def 7;
A7:
n + (len f) <= (len f) + (len g)
by A2, XREAL_1:8;
A8:
n + (len f) <= len (f ^ g)
by A7, FINSEQ_1:35;
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, A8, Th45, NAT_1:12;
CQC_THE1:def 4case A16:
((f ^ g) . (n + (len f))) `2 = 7
;
ex i, j being Element of NAT ex p, q being Element of CQC-WFF 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 )consider i,
j being
Element of
NAT ,
r,
t being
Element of
CQC-WFF such that A17:
1
<= i
and A18:
i < n
and A19:
1
<= j
and A20:
j < i
and A21:
(
r = (g . j) `1 &
t = (g . n) `1 &
(g . i) `1 = r => t )
by A3, A6, A16, Def4;
A22:
( 1
<= i + (len f) &
i + (len f) < n + (len f) )
by A17, A18, NAT_1:12, XREAL_1:8;
A23:
( 1
<= j + (len f) &
j + (len f) < i + (len f) )
by A19, A20, NAT_1:12, XREAL_1:8;
A24:
i <= len g
by A2, A18, XXREAL_0:2;
A25:
j <= len g
by A20, A24, XXREAL_0:2;
A26:
i in Seg (len g)
by A17, A24, FINSEQ_1:3;
A27:
j in Seg (len g)
by A19, A25, FINSEQ_1:3;
A28:
i in dom g
by A26, FINSEQ_1:def 3;
A29:
j in dom g
by A27, FINSEQ_1:def 3;
A30:
g . i = (f ^ g) . (i + (len f))
by A28, FINSEQ_1:def 7;
A31:
g . j = (f ^ g) . (j + (len f))
by A29, FINSEQ_1:def 7;
thus
ex
i,
j being
Element of
NAT ex
p,
q being
Element of
CQC-WFF 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 A6, A21, A22, A23, A30, A31;
verum end; case A32:
((f ^ g) . (n + (len f))) `2 = 8
;
ex i being Element of NAT ex p, q being Element of CQC-WFF ex x being bound_QC-variable 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) )consider i being
Element of
NAT ,
r,
t being
Element of
CQC-WFF ,
x being
bound_QC-variable such that A33:
1
<= i
and A34:
i < n
and A35:
(
(g . i) `1 = r => t & not
x in still_not-bound_in r &
(g . n) `1 = r => (All x,t) )
by A3, A6, A32, Def4;
A36:
( 1
<= (len f) + i &
(len f) + i < n + (len f) )
by A33, A34, NAT_1:12, XREAL_1:8;
A37:
i <= len g
by A2, A34, XXREAL_0:2;
A38:
i in Seg (len g)
by A33, A37, FINSEQ_1:3;
A39:
i in dom g
by A38, FINSEQ_1:def 3;
A40:
g . i = (f ^ g) . ((len f) + i)
by A39, FINSEQ_1:def 7;
thus
ex
i being
Element of
NAT ex
p,
q being
Element of
CQC-WFF ex
x being
bound_QC-variable 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 A6, A35, A36, A40;
verum end; case A41:
((f ^ g) . (n + (len f))) `2 = 9
;
ex i being Element of NAT ex x, y being bound_QC-variable ex s being QC-formula st
( 1 <= i & i < n + (len f) & s . x in CQC-WFF & s . y in CQC-WFF & not x in still_not-bound_in s & s . x = ((f ^ g) . i) `1 & s . y = ((f ^ g) . (n + (len f))) `1 )consider i being
Element of
NAT ,
x,
y being
bound_QC-variable,
s being
QC-formula such that A42:
1
<= i
and A43:
i < n
and A44:
(
s . x in CQC-WFF &
s . y in CQC-WFF & not
x in still_not-bound_in s &
s . x = (g . i) `1 &
(g . n) `1 = s . y )
by A3, A6, A41, Def4;
A45:
( 1
<= (len f) + i &
(len f) + i < n + (len f) )
by A42, A43, NAT_1:12, XREAL_1:8;
A46:
i <= len g
by A2, A43, XXREAL_0:2;
A47:
i in Seg (len g)
by A42, A46, FINSEQ_1:3;
A48:
i in dom g
by A47, FINSEQ_1:def 3;
A49:
g . i = (f ^ g) . ((len f) + i)
by A48, FINSEQ_1:def 7;
thus
ex
i being
Element of
NAT ex
x,
y being
bound_QC-variable ex
s being
QC-formula st
( 1
<= i &
i < n + (len f) &
s . x in CQC-WFF &
s . y in CQC-WFF & not
x in still_not-bound_in s &
s . x = ((f ^ g) . i) `1 &
s . y = ((f ^ g) . (n + (len f))) `1 )
by A6, A44, A45, A49;
verum end;