---

Step * of Lemma first-at-filter-interface-predecessors1

∀[Info:Type]. ∀[es:EO+(Info)]. ∀[T:Type]. ∀[X:EClass(T)]. ∀[P:E(X) ⟶ 𝔹]. ∀[n:ℕ+]. ∀[e:E]. ∀[i:Id].
  {(↑e ∈b X) ∧ (↑P[e])} supposing e is first@ i s.t.  q.||filter(λe.P[e];≤(X)(q))|| = n ∈ ℤ
BY
{ ((RepeatFor 8 ((D 0 THENA Auto)) THEN (At ⌜Type⌝ (D 0)⋅ THENA Auto))
   THEN Unfold `guard` 0
   THEN MoveToConcl (-1)
   THEN ((InstLemma `es-first-at-implies` [⌜es⌝;⌜i⌝;⌜λ2q.||filter(λe.P[e];≤(X)(q))|| = n ∈ ℤ⌝;⌜λ2e.(↑e ∈b X) c∧ (↑P[e])⌝
          ;⌜e⌝]⋅
         THENM (Unfold `cand` (-1) THEN Fold `and` (-1) THEN Trivial)
         )
         THENA Auto
         )) }

1
1. Info : Type
2. es : EO+(Info)
3. T : Type
4. X : EClass(T)
5. P : E(X) ⟶ 𝔹
6. n : ℕ+
7. e : E
8. i : Id
9. e1 : {e:E| loc(e) = i ∈ Id} @i
10. ||filter(λe.P[e];≤(X)(e1))|| = n ∈ ℤ@i
11. ¬((↑e1 ∈b X) c∧ (↑P[e1]))
⊢ ∃e':E. ((e' <loc e1) ∧ (||filter(λe.P[e];≤(X)(e'))|| = n ∈ ℤ))

---

Latex:

---

Latex:
\mforall{}[Info:Type].  \mforall{}[es:EO+(Info)].  \mforall{}[T:Type].  \mforall{}[X:EClass(T)].  \mforall{}[P:E(X)  {}\mrightarrow{}  \mBbbB{}].  \mforall{}[n:\mBbbN{}\msupplus{}].  \mforall{}[e:E].  \mforall{}[i:Id].
    \{(\muparrow{}e  \mmember{}\msubb{}  X)  \mwedge{}  (\muparrow{}P[e])\}  supposing  e  is  first@  i  s.t.    q.||filter(\mlambda{}e.P[e];\mleq{}(X)(q))||  =  n


By

---

Latex:
((RepeatFor  8  ((D  0  THENA  Auto))  THEN  (At  \mkleeneopen{}Type\mkleeneclose{}  (D  0)\mcdot{}  THENA  Auto))
  THEN  Unfold  `guard`  0
  THEN  MoveToConcl  (-1)
  THEN  ((InstLemma  `es-first-at-implies`  [\mkleeneopen{}es\mkleeneclose{};\mkleeneopen{}i\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}q.||filter(\mlambda{}e.P[e];\mleq{}(X)(q))||  =  n\mkleeneclose{};
                \mkleeneopen{}\mlambda{}\msubtwo{}e.(\muparrow{}e  \mmember{}\msubb{}  X)  c\mwedge{}  (\muparrow{}P[e])\mkleeneclose{};\mkleeneopen{}e\mkleeneclose{}]\mcdot{}
              THENM  (Unfold  `cand`  (-1)  THEN  Fold  `and`  (-1)  THEN  Trivial)
              )
              THENA  Auto
              ))

---

Home Index