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