let i be Element of NAT ; for p being Element of CQC-WFF
for F1 being QC-formula
for L being PATH of F1,p st F1 is_subformula_of p & 1 <= i & i <= len L holds
L . i is Element of CQC-WFF
let p be Element of CQC-WFF ; for F1 being QC-formula
for L being PATH of F1,p st F1 is_subformula_of p & 1 <= i & i <= len L holds
L . i is Element of CQC-WFF
let F1 be QC-formula; for L being PATH of F1,p st F1 is_subformula_of p & 1 <= i & i <= len L holds
L . i is Element of CQC-WFF
let L be PATH of F1,p; ( F1 is_subformula_of p & 1 <= i & i <= len L implies L . i is Element of CQC-WFF )
set n = len L;
assume that
A1:
F1 is_subformula_of p
and
A2:
1 <= i
and
A3:
i <= len L
; L . i is Element of CQC-WFF
(len L) + 1 <= (len L) + i
by A2, XREAL_1:8;
then
((len L) + 1) + (- 1) <= ((len L) + i) + (- 1)
by XREAL_1:8;
then A4:
(len L) + (- i) <= (((len L) - 1) + i) + (- i)
by XREAL_1:8;
i + (- i) <= (len L) + (- i)
by A3, XREAL_1:8;
then reconsider l = (len L) - i as Element of NAT by INT_1:16;
defpred S1[ Element of NAT ] means ( $1 <= (len L) - 1 implies L . ((len L) - $1) is Element of CQC-WFF );
A5:
for k being Element of NAT st S1[k] holds
S1[k + 1]
proof
let k be
Element of
NAT ;
( S1[k] implies S1[k + 1] )
assume A6:
S1[
k]
;
S1[k + 1]
assume A7:
k + 1
<= (len L) - 1
;
L . ((len L) - (k + 1)) is Element of CQC-WFF
then
(k + 1) + 1
<= ((len L) - 1) + 1
by XREAL_1:8;
then A8:
(2 + k) + (- k) <= (len L) + (- k)
by XREAL_1:8;
then reconsider j =
(len L) - k as
Element of
NAT by INT_1:16;
k < k + 1
by NAT_1:13;
then reconsider q =
L . j as
Element of
CQC-WFF by A6, A7, XXREAL_0:2;
len L <= (len L) + k
by NAT_1:11;
then
(len L) + (- k) <= ((len L) + k) + (- k)
by XREAL_1:8;
then A9:
j - 1
< len L
by XREAL_1:148, XXREAL_0:2;
A10:
(1 + 1) + (- 1) <= j + (- 1)
by A8, XREAL_1:8;
then reconsider j1 =
j - 1 as
Element of
NAT by INT_1:16;
j1 + 1
= j
;
then consider G1,
H1 being
Element of
QC-WFF such that A11:
L . j1 = G1
and A12:
(
q = H1 &
G1 is_immediate_constituent_of H1 )
by A1, A10, A9, Def6;
A13:
( ex
F being
Element of
QC-WFF st
q = G1 '&' F implies
L . ((len L) - (k + 1)) is
Element of
CQC-WFF )
by A11, CQC_LANG:19;
A14:
( ex
x being
bound_QC-variable st
q = All (
x,
G1) implies
L . ((len L) - (k + 1)) is
Element of
CQC-WFF )
by A11, CQC_LANG:23;
A15:
( ex
F being
Element of
QC-WFF st
q = F '&' G1 implies
L . ((len L) - (k + 1)) is
Element of
CQC-WFF )
by A11, CQC_LANG:19;
(
q = 'not' G1 implies
L . ((len L) - (k + 1)) is
Element of
CQC-WFF )
by A11, CQC_LANG:18;
hence
L . ((len L) - (k + 1)) is
Element of
CQC-WFF
by A12, A13, A15, A14, QC_LANG2:def 20;
verum
end;
A16:
S1[ 0 ]
by A1, Def6;
for k being Element of NAT holds S1[k]
from NAT_1:sch 1(A16, A5);
then
L . ((len L) - l) is Element of CQC-WFF
by A4;
hence
L . i is Element of CQC-WFF
; verum