---

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

∀[Info:Type]
  ∀es:EO+(Info)
    ∀[T:Type]
      ∀X:EClass(T). ∀P:E(X) ⟶ 𝔹. ∀i:Id.
        ∀[R:Id ⟶ E(X) ⟶ ℙ]
          ∀n:ℕ+. ∀L:Id List.
            ((∀x∈L.∃y:E(X). (R[x;y] ∧ (↑P[y])))
               ⇒ (∃e:E(X). ((↑P[e]) ∧ e is first@ i s.t.  q.||filter(λe.P[e];≤(X)(q))|| = n ∈ ℤ))) supposing 
               ((n ≤ ||L||) and 
               no_repeats(Id;L)) 
          supposing ∀x1,x2:Id. ∀y:E(X).  (R[x1;y] ⇒ R[x2;y] ⇒ (x1 = x2 ∈ Id)) 
        supposing ∀e:E(X). loc(e) = i ∈ Id supposing ↑P[e]
BY
{ WithCumulativity((Auto
                    THEN (InstLemma `filter-interface-predecessors-lower-bound2` [⌜Info⌝;⌜es⌝;⌜T⌝;⌜X⌝;⌜P⌝;⌜R⌝;⌜L⌝]⋅
                          THENA (Auto THEN Try ((RWO "7" 0 THEN Complete (Auto))))
                          )
                    )) }

1
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 ∈ ℤ)

---

Latex:

---

Latex:
\mforall{}[Info:Type]
    \mforall{}es:EO+(Info)
        \mforall{}[T:Type]
            \mforall{}X:EClass(T).  \mforall{}P:E(X)  {}\mrightarrow{}  \mBbbB{}.  \mforall{}i:Id.
                \mforall{}[R:Id  {}\mrightarrow{}  E(X)  {}\mrightarrow{}  \mBbbP{}]
                    \mforall{}n:\mBbbN{}\msupplus{}.  \mforall{}L:Id  List.
                        ((\mforall{}x\mmember{}L.\mexists{}y:E(X).  (R[x;y]  \mwedge{}  (\muparrow{}P[y])))
                              {}\mRightarrow{}  (\mexists{}e:E(X)
                                        ((\muparrow{}P[e])  \mwedge{}  e  is  first@  i  s.t.    q.||filter(\mlambda{}e.P[e];\mleq{}(X)(q))||  =  n)))  supposing 
                              ((n  \mleq{}  ||L||)  and 
                              no\_repeats(Id;L)) 
                    supposing  \mforall{}x1,x2:Id.  \mforall{}y:E(X).    (R[x1;y]  {}\mRightarrow{}  R[x2;y]  {}\mRightarrow{}  (x1  =  x2)) 
                supposing  \mforall{}e:E(X).  loc(e)  =  i  supposing  \muparrow{}P[e]


By

---

Latex:
WithCumulativity((Auto
                                    THEN  (InstLemma  `filter-interface-predecessors-lower-bound2`  [\mkleeneopen{}Info\mkleeneclose{};\mkleeneopen{}es\mkleeneclose{};\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}X\mkleeneclose{};
                                                \mkleeneopen{}P\mkleeneclose{};\mkleeneopen{}R\mkleeneclose{};\mkleeneopen{}L\mkleeneclose{}]\mcdot{}
                                                THENA  (Auto  THEN  Try  ((RWO  "7"  0  THEN  Complete  (Auto))))
                                                )
                                    ))

---

Home Index