---

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

∀[Info:Type]. ∀[es:EO+(Info)]. ∀[T:Type]. ∀[X:EClass(T)]. ∀[P:E(X) ─→ 𝔹]. ∀[Q:E(X) ─→ ℙ]. ∀[n:ℕ+]. ∀[e:E]. ∀[i:Id].
  ↑e ∈b X supposing e is first@ i s.t.  q.((↑q ∈b X) ∧ Q[q]) ∨ (||filter(λe.P[e];≤(X)(q))|| = n ∈ ℤ)
BY
{ (Auto
   THEN MoveToConcl (-1)
   THEN ((InstLemma `es-first-at-implies` [⌈es⌉;⌈i⌉;⌈λ2q.((↑q ∈b X) ∧ Q[q]) ∨ (||filter(λe.P[e];≤(X)(q))|| = n ∈ ℤ)⌉;
          ⌈λ2e.↑e ∈b X⌉;⌈e⌉]⋅
         THENM Trivial
         )
         THENA Auto
         )) }

1
1. Info : Type
2. es : EO+(Info)
3. T : Type
4. X : EClass(T)
5. P : E(X) ─→ 𝔹
6. Q : E(X) ─→ ℙ
7. n : ℕ+
8. e : E
9. i : Id
10. e1 : {e:E| loc(e) = i ∈ Id} @i
11. ((↑e1 ∈b X) ∧ Q[e1]) ∨ (||filter(λe.P[e];≤(X)(e1))|| = n ∈ ℤ)@i
12. ¬↑e1 ∈b X
⊢ ∃e':E. ((e' <loc e1) ∧ (((↑e' ∈b X) ∧ Q[e']) ∨ (||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{}[Q:E(X)  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[n:\mBbbN{}\msupplus{}].
\mforall{}[e:E].  \mforall{}[i:Id].
    \muparrow{}e  \mmember{}\msubb{}  X  supposing  e  is  first@  i  s.t.    q.((\muparrow{}q  \mmember{}\msubb{}  X)  \mwedge{}  Q[q])  \mvee{}  (||filter(\mlambda{}e.P[e];\mleq{}(X)(q))||  =  n)


By

---

Latex:
(Auto
  THEN  MoveToConcl  (-1)
  THEN  ((InstLemma  `es-first-at-implies`  [\mkleeneopen{}es\mkleeneclose{};\mkleeneopen{}i\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}q.((\muparrow{}q  \mmember{}\msubb{}  X)  \mwedge{}  Q[q])
                                                                                                      \mvee{}  (||filter(\mlambda{}e.P[e];\mleq{}(X)(q))||  =  n)\mkleeneclose{};
                \mkleeneopen{}\mlambda{}\msubtwo{}e.\muparrow{}e  \mmember{}\msubb{}  X\mkleeneclose{};\mkleeneopen{}e\mkleeneclose{}]\mcdot{}
              THENM  Trivial
              )
              THENA  Auto
              ))

---

Home Index