let i be Element of NAT ; :: thesis: for F1, F2 being QC-formula
for L being PATH of F1,F2 st F1 is_subformula_of F2 & 1 <= i & i <= len L holds
ex F3 being QC-formula st
( F3 = L . i & F3 is_subformula_of F2 )
let F1, F2 be QC-formula; :: thesis: for L being PATH of F1,F2 st F1 is_subformula_of F2 & 1 <= i & i <= len L holds
ex F3 being QC-formula st
( F3 = L . i & F3 is_subformula_of F2 )
let L be PATH of F1,F2; :: thesis: ( F1 is_subformula_of F2 & 1 <= i & i <= len L implies ex F3 being QC-formula st
( F3 = L . i & F3 is_subformula_of F2 ) )
set n = len L;
assume A1:
( F1 is_subformula_of F2 & 1 <= i & i <= len L )
; :: thesis: ex F3 being QC-formula st
( F3 = L . i & F3 is_subformula_of F2 )
then A2:
( 1 <= len L & L . 1 = F1 & L . (len L) = F2 & ( 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 F3 being QC-formula st
( F3 = L . ((len L) - $1) & F3 is_subformula_of F2 ) );
A3:
S1[ 0 ]
by 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 F3 being QC-formula st
( F3 = L . ((len L) - (k + 1)) & F3 is_subformula_of F2 )
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;
(
j1 + 1
= j &
j1 = (len L) - (k + 1) )
;
then consider G1,
H1 being
Element of
QC-WFF such that A11:
(
L . j1 = G1 &
L . j = H1 &
G1 is_immediate_constituent_of H1 )
by A1, A10, Def6;
reconsider F3 =
L . j1 as
QC-formula by A11;
take
F3
;
:: thesis: ( F3 = L . ((len L) - (k + 1)) & F3 is_subformula_of F2 )
consider F4 being
QC-formula such that A12:
(
F4 = L . j &
F4 is_subformula_of F2 )
by A5, A6, A7, XXREAL_0:2;
F3 is_proper_subformula_of F2
by A11, A12, QC_LANG2:83;
hence
(
F3 = L . ((len L) - (k + 1)) &
F3 is_subformula_of F2 )
by QC_LANG2:def 22;
:: thesis: verum
end;
A13:
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 A14:
(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 F3 being QC-formula st
( F3 = L . ((len L) - l) & F3 is_subformula_of F2 )
by A13, A14;
hence
ex F3 being QC-formula st
( F3 = L . i & F3 is_subformula_of F2 )
; :: thesis: verum