---

Step * 1 of Lemma filter-interface-predecessors-first-at


1. [Info] : Type
2. es : EO+(Info)@i'
3. [T] : Type
4. X : EClass(T)@i'
5. P : E(X) ─→ 𝔹@i
6. i : Id@i
7. ∀e:E(X). loc(e) = i ∈ Id supposing ↑P[e]
8. [R] : Id ─→ E(X) ─→ ℙ
9. ∀x1,x2:Id. ∀y:E(X).  (R[x1;y] ⇒ R[x2;y] ⇒ (x1 = x2 ∈ Id))
10. n : ℕ+@i
11. L : Id List@i
12. no_repeats(Id;L)
13. n ≤ ||L||
14. (∀x∈L.∃y:E(X). (R[x;y] ∧ (↑P[y])))@i
15. ∃e:{e:E(X)| ↑P[e]} . (||L|| ≤ ||filter(λe.P[e];≤(X)(e))||)
⊢ ∃e:E(X). ((↑P[e]) ∧ e is first@ i s.t.  q.||filter(λe.P[e];≤(X)(q))|| = n ∈ ℤ)
BY
{ Assert ⌈∃e:E. ((loc(e) = i ∈ Id) ∧ (||filter(λe.P[e];≤(X)(e))|| = n ∈ ℤ))⌉⋅ }

1
.....assertion..... 
1. [Info] : Type
2. es : EO+(Info)@i'
3. [T] : Type
4. X : EClass(T)@i'
5. P : E(X) ─→ 𝔹@i
6. i : Id@i
7. ∀e:E(X). loc(e) = i ∈ Id supposing ↑P[e]
8. [R] : Id ─→ E(X) ─→ ℙ
9. ∀x1,x2:Id. ∀y:E(X).  (R[x1;y] ⇒ R[x2;y] ⇒ (x1 = x2 ∈ Id))
10. n : ℕ+@i
11. L : Id List@i
12. no_repeats(Id;L)
13. n ≤ ||L||
14. (∀x∈L.∃y:E(X). (R[x;y] ∧ (↑P[y])))@i
15. ∃e:{e:E(X)| ↑P[e]} . (||L|| ≤ ||filter(λe.P[e];≤(X)(e))||)
⊢ ∃e:E. ((loc(e) = i ∈ Id) ∧ (||filter(λe.P[e];≤(X)(e))|| = n ∈ ℤ))

2
1. [Info] : Type
2. es : EO+(Info)@i'
3. [T] : Type
4. X : EClass(T)@i'
5. P : E(X) ─→ 𝔹@i
6. i : Id@i
7. ∀e:E(X). loc(e) = i ∈ Id supposing ↑P[e]
8. [R] : Id ─→ E(X) ─→ ℙ
9. ∀x1,x2:Id. ∀y:E(X).  (R[x1;y] ⇒ R[x2;y] ⇒ (x1 = x2 ∈ Id))
10. n : ℕ+@i
11. L : Id List@i
12. no_repeats(Id;L)
13. n ≤ ||L||
14. (∀x∈L.∃y:E(X). (R[x;y] ∧ (↑P[y])))@i
15. ∃e:{e:E(X)| ↑P[e]} . (||L|| ≤ ||filter(λe.P[e];≤(X)(e))||)
16. ∃e:E. ((loc(e) = i ∈ Id) ∧ (||filter(λe.P[e];≤(X)(e))|| = n ∈ ℤ))
⊢ ∃e:E(X). ((↑P[e]) ∧ e is first@ i s.t.  q.||filter(λe.P[e];≤(X)(q))|| = n ∈ ℤ)

---

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.  i  :  Id@i
7.  \mforall{}e:E(X).  loc(e)  =  i  supposing  \muparrow{}P[e]
8.  [R]  :  Id  {}\mrightarrow{}  E(X)  {}\mrightarrow{}  \mBbbP{}
9.  \mforall{}x1,x2:Id.  \mforall{}y:E(X).    (R[x1;y]  {}\mRightarrow{}  R[x2;y]  {}\mRightarrow{}  (x1  =  x2))
10.  n  :  \mBbbN{}\msupplus{}@i
11.  L  :  Id  List@i
12.  no\_repeats(Id;L)
13.  n  \mleq{}  ||L||
14.  (\mforall{}x\mmember{}L.\mexists{}y:E(X).  (R[x;y]  \mwedge{}  (\muparrow{}P[y])))@i
15.  \mexists{}e:\{e:E(X)|  \muparrow{}P[e]\}  .  (||L||  \mleq{}  ||filter(\mlambda{}e.P[e];\mleq{}(X)(e))||)
\mvdash{}  \mexists{}e:E(X).  ((\muparrow{}P[e])  \mwedge{}  e  is  first@  i  s.t.    q.||filter(\mlambda{}e.P[e];\mleq{}(X)(q))||  =  n)


By

---

Latex:
Assert  \mkleeneopen{}\mexists{}e:E.  ((loc(e)  =  i)  \mwedge{}  (||filter(\mlambda{}e.P[e];\mleq{}(X)(e))||  =  n))\mkleeneclose{}\mcdot{}

---

Home Index