---

Step * 1 of Lemma filter-interface-predecessors-lower-bound-implies


1. [Info] : Type
2. es : EO+(Info)@i'
3. [T] : Type
4. X : EClass(T)@i'
5. P : E(X) ─→ 𝔹@i
6. n : ℕ@i
7. e : E@i
8. n ≤ ||filter(λe.P[e];≤(X)(e))||
⊢ ∃f:ℕn ─→ {e':E(X)| (↑P[e']) ∧ e' ≤loc e } . ∀i,j:ℕn.  (f i <loc f j) supposing i < j
BY
{ ((Assert ∃L:{x:{a:E(X)| loc(a) = loc(e) ∈ Id} | ↑(P x)}  List
            ((n ≤ ||L||) ∧ sorted-by(λx,y. (x <loc y);L) ∧ (∀i:ℕn. L[i] ≤loc e )) BY
          (...
           THEN (InstLemma `filter_type` [⌈{a:E(X)| loc(a) = loc(e) ∈ Id} ⌉;⌈λe.P[e]⌉;⌈≤(X)(e)⌉]⋅ THENA Auto)
           THEN All Reduce
           THEN With ⌈filter(λe.P[e];≤(X)(e))⌉ (D 0)⋅
           THEN Auto))
   THEN ExRepD
   ) }

1
1. [Info] : Type
2. es : EO+(Info)@i'
3. [T] : Type
4. X : EClass(T)@i'
5. P : E(X) ─→ 𝔹@i
6. n : ℕ@i
7. e : E@i
8. n ≤ ||filter(λe.P[e];≤(X)(e))||
9. sorted-by(λx,y. (x <loc y);filter(λe.P[e];≤(X)(e)))
10. filter(λe.P[e];≤(X)(e)) ∈ {x:{a:E(X)| loc(a) = loc(e) ∈ Id} | ↑P[x]}  List
11. n ≤ ||filter(λe.P[e];≤(X)(e))||
12. sorted-by(λx,y. (x <loc y);filter(λe.P[e];≤(X)(e)))
13. i : ℕn@i
⊢ filter(λe.P[e];≤(X)(e))[i] ≤loc e 

2
1. [Info] : Type
2. es : EO+(Info)@i'
3. [T] : Type
4. X : EClass(T)@i'
5. P : E(X) ─→ 𝔹@i
6. n : ℕ@i
7. e : E@i
8. n ≤ ||filter(λe.P[e];≤(X)(e))||
9. L : {x:{a:E(X)| loc(a) = loc(e) ∈ Id} | ↑(P x)}  List
10. n ≤ ||L||
11. sorted-by(λx,y. (x <loc y);L)
12. ∀i:ℕn. L[i] ≤loc e 
⊢ ∃f:ℕn ─→ {e':E(X)| (↑P[e']) ∧ e' ≤loc e } . ∀i,j:ℕn.  (f i <loc f j) supposing i < j

---

Latex:

---

Latex:

1.  [Info]  :  Type
2.  es  :  EO+(Info)@i'
3.  [T]  :  Type
4.  X  :  EClass(T)@i'
5.  P  :  E(X)  {}\mrightarrow{}  \mBbbB{}@i
6.  n  :  \mBbbN{}@i
7.  e  :  E@i
8.  n  \mleq{}  ||filter(\mlambda{}e.P[e];\mleq{}(X)(e))||
\mvdash{}  \mexists{}f:\mBbbN{}n  {}\mrightarrow{}  \{e':E(X)|  (\muparrow{}P[e'])  \mwedge{}  e'  \mleq{}loc  e  \}  .  \mforall{}i,j:\mBbbN{}n.    (f  i  <loc  f  j)  supposing  i  <  j


By

---

Latex:
((Assert  \mexists{}L:\{x:\{a:E(X)|  loc(a)  =  loc(e)\}  |  \muparrow{}(P  x)\}    List
                    ((n  \mleq{}  ||L||)  \mwedge{}  sorted-by(\mlambda{}x,y.  (x  <loc  y);L)  \mwedge{}  (\mforall{}i:\mBbbN{}n.  L[i]  \mleq{}loc  e  ))  BY
                ((Assert  sorted-by(\mlambda{}x,y.  (x  <loc  y);filter(\mlambda{}e.P[e];\mleq{}(X)(e)))  BY
                                (BLemma  `sorted-by-filter`
                                  THEN  Auto
                                  THEN  BLemma  `es-interface-predecessors-sorted-by-locl`
                                  THEN  Auto))
                  THEN  (InstLemma  `filter\_type`  [\mkleeneopen{}\{a:E(X)|  loc(a)  =  loc(e)\}  \mkleeneclose{};\mkleeneopen{}\mlambda{}e.P[e]\mkleeneclose{};\mkleeneopen{}\mleq{}(X)(e)\mkleeneclose{}]\mcdot{}
                              THENA  Auto
                              )
                  THEN  All  Reduce
                  THEN  With  \mkleeneopen{}filter(\mlambda{}e.P[e];\mleq{}(X)(e))\mkleeneclose{}  (D  0)\mcdot{}
                  THEN  Auto))
  THEN  ExRepD
  )

---

Home Index