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