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

for p, q being Element of CQC-WFF Al

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

( r = L . i & QuantNbr r <= n )

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

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

( r = L . i & QuantNbr r <= n )

let p, q be Element of CQC-WFF Al; :: 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 Al 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 Al st

( r = L . i & QuantNbr r <= n ) )

set m = len L;

assume that

A1: QuantNbr p <= n and

A2: q is_subformula_of p and

A3: 1 <= i and

A4: i <= len L ; :: thesis: ex r being Element of CQC-WFF Al st

( r = L . i & QuantNbr r <= n )

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

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

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

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

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

defpred S_{1}[ Nat] means ( $1 <= (len L) - 1 implies ex r being Element of CQC-WFF Al st

( r = L . ((len L) - $1) & QuantNbr r <= n ) );

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

S_{1}[k + 1]

then A25: S_{1}[ 0 ]
by A1;

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

then ex r being Element of CQC-WFF Al st

( r = L . ((len L) - l) & QuantNbr r <= n ) by A5;

hence ex r being Element of CQC-WFF Al st

( r = L . i & QuantNbr r <= n ) ; :: thesis: verum

for p, q being Element of CQC-WFF Al

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

( r = L . i & QuantNbr r <= n )

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

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

( r = L . i & QuantNbr r <= n )

let p, q be Element of CQC-WFF Al; :: 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 Al 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 Al st

( r = L . i & QuantNbr r <= n ) )

set m = len L;

assume that

A1: QuantNbr p <= n and

A2: q is_subformula_of p and

A3: 1 <= i and

A4: i <= len L ; :: thesis: ex r being Element of CQC-WFF Al st

( r = L . i & QuantNbr r <= n )

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

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

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

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

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

defpred S

( r = L . ((len L) - $1) & QuantNbr r <= n ) );

A6: for k being Nat st S

S

proof

L . (len L) = p
by A2, Def5;
let k be Nat; :: thesis: ( S_{1}[k] implies S_{1}[k + 1] )

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

assume A8: k + 1 <= (len L) - 1 ; :: thesis: ex r being Element of CQC-WFF Al st

( r = L . ((len L) - (k + 1)) & QuantNbr r <= n )

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

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

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

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

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

len L <= (len L) + k by NAT_1:11;

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

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

j1 + 1 = j ;

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

A12: L . j1 = G1 and

A13: ( L . j = H1 & G1 is_immediate_constituent_of H1 ) by A2, A10, A11, Def5;

reconsider r = G1 as Element of CQC-WFF Al by A2, A10, A11, A12, Th28;

k < k + 1 by NAT_1:13;

then consider q being Element of CQC-WFF Al such that

A14: q = L . j and

A15: QuantNbr q <= n by A7, A8, XXREAL_0:2;

( r = L . ((len L) - (k + 1)) & QuantNbr r <= n ) by A14, A13, A21, A18, A16, QC_LANG2:def 19; :: thesis: verum

end;assume A7: S

assume A8: k + 1 <= (len L) - 1 ; :: thesis: ex r being Element of CQC-WFF Al st

( r = L . ((len L) - (k + 1)) & QuantNbr r <= n )

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

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

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

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

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

len L <= (len L) + k by NAT_1:11;

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

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

j1 + 1 = j ;

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

A12: L . j1 = G1 and

A13: ( L . j = H1 & G1 is_immediate_constituent_of H1 ) by A2, A10, A11, Def5;

reconsider r = G1 as Element of CQC-WFF Al by A2, A10, A11, A12, Th28;

k < k + 1 by NAT_1:13;

then consider q being Element of CQC-WFF Al such that

A14: q = L . j and

A15: QuantNbr q <= n by A7, A8, XXREAL_0:2;

A16: now :: thesis: ( ex x being bound_QC-variable of Al st q = All (x,G1) implies ex r, r being Element of CQC-WFF Al st

( r = L . ((len L) - (k + 1)) & QuantNbr r <= n ) )

( r = L . ((len L) - (k + 1)) & QuantNbr r <= n ) )

given x being bound_QC-variable of Al such that A17:
q = All (x,G1)
; :: thesis: ex r, r being Element of CQC-WFF Al st

( r = L . ((len L) - (k + 1)) & QuantNbr r <= n )

take r = r; :: thesis: ex r being Element of CQC-WFF Al st

( r = L . ((len L) - (k + 1)) & QuantNbr r <= n )

(QuantNbr r) + 1 <= n by A15, A17, CQC_SIM1:18;

then QuantNbr r <= n by NAT_1:13;

hence ex r being Element of CQC-WFF Al st

( r = L . ((len L) - (k + 1)) & QuantNbr r <= n ) by A12; :: thesis: verum

end;( r = L . ((len L) - (k + 1)) & QuantNbr r <= n )

take r = r; :: thesis: ex r being Element of CQC-WFF Al st

( r = L . ((len L) - (k + 1)) & QuantNbr r <= n )

(QuantNbr r) + 1 <= n by A15, A17, CQC_SIM1:18;

then QuantNbr r <= n by NAT_1:13;

hence ex r being Element of CQC-WFF Al st

( r = L . ((len L) - (k + 1)) & QuantNbr r <= n ) by A12; :: thesis: verum

A18: now :: thesis: ( ex F being Element of QC-WFF Al st q = F '&' G1 implies ex r, r being Element of CQC-WFF Al st

( r = L . ((len L) - (k + 1)) & QuantNbr r <= n ) )

( r = L . ((len L) - (k + 1)) & QuantNbr r <= n ) )

given F being Element of QC-WFF Al such that A19:
q = F '&' G1
; :: thesis: ex r, r being Element of CQC-WFF Al st

( r = L . ((len L) - (k + 1)) & QuantNbr r <= n )

reconsider F = F as Element of CQC-WFF Al by A19, CQC_LANG:9;

take r = r; :: thesis: ex r being Element of CQC-WFF Al st

( r = L . ((len L) - (k + 1)) & QuantNbr r <= n )

n <= n + (QuantNbr F) by NAT_1:11;

then A20: n + (- (QuantNbr F)) <= (n + (QuantNbr F)) + (- (QuantNbr F)) by XREAL_1:6;

(QuantNbr r) + (QuantNbr F) <= n by A15, A19, CQC_SIM1:17;

then ((QuantNbr r) + (QuantNbr F)) + (- (QuantNbr F)) <= n + (- (QuantNbr F)) by XREAL_1:6;

hence ex r being Element of CQC-WFF Al st

( r = L . ((len L) - (k + 1)) & QuantNbr r <= n ) by A12, A20, XXREAL_0:2; :: thesis: verum

end;( r = L . ((len L) - (k + 1)) & QuantNbr r <= n )

reconsider F = F as Element of CQC-WFF Al by A19, CQC_LANG:9;

take r = r; :: thesis: ex r being Element of CQC-WFF Al st

( r = L . ((len L) - (k + 1)) & QuantNbr r <= n )

n <= n + (QuantNbr F) by NAT_1:11;

then A20: n + (- (QuantNbr F)) <= (n + (QuantNbr F)) + (- (QuantNbr F)) by XREAL_1:6;

(QuantNbr r) + (QuantNbr F) <= n by A15, A19, CQC_SIM1:17;

then ((QuantNbr r) + (QuantNbr F)) + (- (QuantNbr F)) <= n + (- (QuantNbr F)) by XREAL_1:6;

hence ex r being Element of CQC-WFF Al st

( r = L . ((len L) - (k + 1)) & QuantNbr r <= n ) by A12, A20, XXREAL_0:2; :: thesis: verum

A21: now :: thesis: ( ex F being Element of QC-WFF Al st q = G1 '&' F implies ex r, r being Element of CQC-WFF Al st

( r = L . ((len L) - (k + 1)) & QuantNbr r <= n ) )

( r = L . ((len L) - (k + 1)) & QuantNbr r <= n ) )

given F being Element of QC-WFF Al such that A22:
q = G1 '&' F
; :: thesis: ex r, r being Element of CQC-WFF Al st

( r = L . ((len L) - (k + 1)) & QuantNbr r <= n )

reconsider F = F as Element of CQC-WFF Al by A22, CQC_LANG:9;

take r = r; :: thesis: ex r being Element of CQC-WFF Al st

( r = L . ((len L) - (k + 1)) & QuantNbr r <= n )

n <= n + (QuantNbr F) by NAT_1:11;

then A23: n + (- (QuantNbr F)) <= (n + (QuantNbr F)) + (- (QuantNbr F)) by XREAL_1:6;

(QuantNbr r) + (QuantNbr F) <= n by A15, A22, CQC_SIM1:17;

then ((QuantNbr r) + (QuantNbr F)) + (- (QuantNbr F)) <= n + (- (QuantNbr F)) by XREAL_1:6;

hence ex r being Element of CQC-WFF Al st

( r = L . ((len L) - (k + 1)) & QuantNbr r <= n ) by A12, A23, XXREAL_0:2; :: thesis: verum

end;( r = L . ((len L) - (k + 1)) & QuantNbr r <= n )

reconsider F = F as Element of CQC-WFF Al by A22, CQC_LANG:9;

take r = r; :: thesis: ex r being Element of CQC-WFF Al st

( r = L . ((len L) - (k + 1)) & QuantNbr r <= n )

n <= n + (QuantNbr F) by NAT_1:11;

then A23: n + (- (QuantNbr F)) <= (n + (QuantNbr F)) + (- (QuantNbr F)) by XREAL_1:6;

(QuantNbr r) + (QuantNbr F) <= n by A15, A22, CQC_SIM1:17;

then ((QuantNbr r) + (QuantNbr F)) + (- (QuantNbr F)) <= n + (- (QuantNbr F)) by XREAL_1:6;

hence ex r being Element of CQC-WFF Al st

( r = L . ((len L) - (k + 1)) & QuantNbr r <= n ) by A12, A23, XXREAL_0:2; :: thesis: verum

now :: thesis: ( q = 'not' G1 implies ex r, r being Element of CQC-WFF Al st

( r = L . ((len L) - (k + 1)) & QuantNbr r <= n ) )

hence
ex r being Element of CQC-WFF Al st ( r = L . ((len L) - (k + 1)) & QuantNbr r <= n ) )

assume A24:
q = 'not' G1
; :: thesis: ex r, r being Element of CQC-WFF Al st

( r = L . ((len L) - (k + 1)) & QuantNbr r <= n )

take r = r; :: thesis: ex r being Element of CQC-WFF Al st

( r = L . ((len L) - (k + 1)) & QuantNbr r <= n )

QuantNbr r <= n by A15, A24, CQC_SIM1:16;

hence ex r being Element of CQC-WFF Al st

( r = L . ((len L) - (k + 1)) & QuantNbr r <= n ) by A12; :: thesis: verum

end;( r = L . ((len L) - (k + 1)) & QuantNbr r <= n )

take r = r; :: thesis: ex r being Element of CQC-WFF Al st

( r = L . ((len L) - (k + 1)) & QuantNbr r <= n )

QuantNbr r <= n by A15, A24, CQC_SIM1:16;

hence ex r being Element of CQC-WFF Al st

( r = L . ((len L) - (k + 1)) & QuantNbr r <= n ) by A12; :: thesis: verum

( r = L . ((len L) - (k + 1)) & QuantNbr r <= n ) by A14, A13, A21, A18, A16, QC_LANG2:def 19; :: thesis: verum

then A25: S

for k being Nat holds S

then ex r being Element of CQC-WFF Al st

( r = L . ((len L) - l) & QuantNbr r <= n ) by A5;

hence ex r being Element of CQC-WFF Al st

( r = L . i & QuantNbr r <= n ) ; :: thesis: verum