let Al be QC-alphabet ; :: thesis: for i being Nat

for p being Element of CQC-WFF Al

for F1 being QC-formula of Al

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 Al

let i be Nat; :: thesis: for p being Element of CQC-WFF Al

for F1 being QC-formula of Al

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 Al

let p be Element of CQC-WFF Al; :: thesis: for F1 being QC-formula of Al

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 Al

let F1 be QC-formula of Al; :: 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 Al

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 Al )

set n = len L;

assume that

A1: F1 is_subformula_of p and

A2: 1 <= i and

A3: i <= len L ; :: thesis: L . i is Element of CQC-WFF Al

(len L) + 1 <= (len L) + i by A2, XREAL_1:6;

then ((len L) + 1) + (- 1) <= ((len L) + i) + (- 1) by XREAL_1:6;

then A4: (len L) + (- i) <= (((len L) - 1) + i) + (- i) by XREAL_1:6;

i + (- i) <= (len L) + (- i) by A3, XREAL_1:6;

then reconsider l = (len L) - i as Element of NAT by INT_1:3;

defpred S_{1}[ Nat] means ( $1 <= (len L) - 1 implies L . ((len L) - $1) is Element of CQC-WFF Al );

A5: for k being Nat st S_{1}[k] holds

S_{1}[k + 1]
_{1}[ 0 ]
by A1, Def5;

for k being Nat holds S_{1}[k]
from NAT_1:sch 2(A16, A5);

then L . ((len L) - l) is Element of CQC-WFF Al by A4;

hence L . i is Element of CQC-WFF Al ; :: thesis: verum

for p being Element of CQC-WFF Al

for F1 being QC-formula of Al

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 Al

let i be Nat; :: thesis: for p being Element of CQC-WFF Al

for F1 being QC-formula of Al

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 Al

let p be Element of CQC-WFF Al; :: thesis: for F1 being QC-formula of Al

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 Al

let F1 be QC-formula of Al; :: 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 Al

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 Al )

set n = len L;

assume that

A1: F1 is_subformula_of p and

A2: 1 <= i and

A3: i <= len L ; :: thesis: L . i is Element of CQC-WFF Al

(len L) + 1 <= (len L) + i by A2, XREAL_1:6;

then ((len L) + 1) + (- 1) <= ((len L) + i) + (- 1) by XREAL_1:6;

then A4: (len L) + (- i) <= (((len L) - 1) + i) + (- i) by XREAL_1:6;

i + (- i) <= (len L) + (- i) by A3, XREAL_1:6;

then reconsider l = (len L) - i as Element of NAT by INT_1:3;

defpred S

A5: for k being Nat st S

S

proof

A16:
S
let k be Nat; :: thesis: ( S_{1}[k] implies S_{1}[k + 1] )

assume A6: S_{1}[k]
; :: thesis: S_{1}[k + 1]

assume A7: k + 1 <= (len L) - 1 ; :: thesis: L . ((len L) - (k + 1)) is Element of CQC-WFF Al

then (k + 1) + 1 <= ((len L) - 1) + 1 by XREAL_1:6;

then A8: (2 + k) + (- k) <= (len L) + (- k) by XREAL_1:6;

then reconsider j = (len L) - k as Element of NAT by INT_1:3;

k < k + 1 by NAT_1:13;

then reconsider q = L . j as Element of CQC-WFF Al 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:6;

then A9: j - 1 < len L by XREAL_1:146, XXREAL_0:2;

A10: (1 + 1) + (- 1) <= j + (- 1) by A8, XREAL_1:6;

then reconsider j1 = j - 1 as Element of NAT by INT_1:3;

j1 + 1 = j ;

then consider G1, H1 being Element of QC-WFF Al such that

A11: L . j1 = G1 and

A12: ( q = H1 & G1 is_immediate_constituent_of H1 ) by A1, A10, A9, Def5;

A13: ( ex F being Element of QC-WFF Al st q = G1 '&' F implies L . ((len L) - (k + 1)) is Element of CQC-WFF Al ) by A11, CQC_LANG:9;

A14: ( ex x being bound_QC-variable of Al st q = All (x,G1) implies L . ((len L) - (k + 1)) is Element of CQC-WFF Al ) by A11, CQC_LANG:13;

A15: ( ex F being Element of QC-WFF Al st q = F '&' G1 implies L . ((len L) - (k + 1)) is Element of CQC-WFF Al ) by A11, CQC_LANG:9;

( q = 'not' G1 implies L . ((len L) - (k + 1)) is Element of CQC-WFF Al ) by A11, CQC_LANG:8;

hence L . ((len L) - (k + 1)) is Element of CQC-WFF Al by A12, A13, A15, A14, QC_LANG2:def 19; :: thesis: verum

end;assume A6: S

assume A7: k + 1 <= (len L) - 1 ; :: thesis: L . ((len L) - (k + 1)) is Element of CQC-WFF Al

then (k + 1) + 1 <= ((len L) - 1) + 1 by XREAL_1:6;

then A8: (2 + k) + (- k) <= (len L) + (- k) by XREAL_1:6;

then reconsider j = (len L) - k as Element of NAT by INT_1:3;

k < k + 1 by NAT_1:13;

then reconsider q = L . j as Element of CQC-WFF Al 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:6;

then A9: j - 1 < len L by XREAL_1:146, XXREAL_0:2;

A10: (1 + 1) + (- 1) <= j + (- 1) by A8, XREAL_1:6;

then reconsider j1 = j - 1 as Element of NAT by INT_1:3;

j1 + 1 = j ;

then consider G1, H1 being Element of QC-WFF Al such that

A11: L . j1 = G1 and

A12: ( q = H1 & G1 is_immediate_constituent_of H1 ) by A1, A10, A9, Def5;

A13: ( ex F being Element of QC-WFF Al st q = G1 '&' F implies L . ((len L) - (k + 1)) is Element of CQC-WFF Al ) by A11, CQC_LANG:9;

A14: ( ex x being bound_QC-variable of Al st q = All (x,G1) implies L . ((len L) - (k + 1)) is Element of CQC-WFF Al ) by A11, CQC_LANG:13;

A15: ( ex F being Element of QC-WFF Al st q = F '&' G1 implies L . ((len L) - (k + 1)) is Element of CQC-WFF Al ) by A11, CQC_LANG:9;

( q = 'not' G1 implies L . ((len L) - (k + 1)) is Element of CQC-WFF Al ) by A11, CQC_LANG:8;

hence L . ((len L) - (k + 1)) is Element of CQC-WFF Al by A12, A13, A15, A14, QC_LANG2:def 19; :: thesis: verum

for k being Nat holds S

then L . ((len L) - l) is Element of CQC-WFF Al by A4;

hence L . i is Element of CQC-WFF Al ; :: thesis: verum