---

Step * of Lemma filter-interface-predecessors-lower-bound2

∀[Info:Type]
  ∀es:EO+(Info)
    ∀[T:Type]
      ∀X:EClass(T). ∀P:E(X) ⟶ 𝔹.
        ∀[R:Id ⟶ E(X) ⟶ ℙ]
          ∀L:Id List
            ((∀x∈L.∃y:E(X). (R[x;y] ∧ (↑P[y])))
               ⇒ (∃e:{e:E(X)| ↑P[e]} . (||L|| ≤ ||filter(λe.P[e];≤(X)(e))||))) supposing 
               (0 < ||L|| and 
               no_repeats(Id;L)) 
          supposing ∀x1,x2:Id. ∀y:E(X).  (R[x1;y] ⇒ R[x2;y] ⇒ (x1 = x2 ∈ Id)) 
        supposing ∀e1,e2:E(X).  (loc(e1) = loc(e2) ∈ Id) supposing ((↑P[e2]) and (↑P[e1]))
BY
{ WithCumulativity((Auto
                    THEN (InstLemma `l_all_exists_injection` [⌜Id⌝;⌜E(X)⌝;⌜R⌝;⌜λ2e.↑P[e]⌝;⌜L⌝]⋅ THENA Auto)
                    THEN D -1
                    THEN UsingVars [`f'] (BLemma `filter-interface-predecessors-lower-bound3`)
                    THEN Auto)) }

1
1. Info : Type
2. es : EO+(Info)@i'
3. T : Type
4. X : EClass(T)@i'
5. P : E(X) ⟶ 𝔹@i
6. ∀e1,e2:E(X).  (loc(e1) = loc(e2) ∈ Id) supposing ((↑P[e2]) and (↑P[e1]))
7. R : Id ⟶ E(X) ⟶ ℙ
8. ∀x1,x2:Id. ∀y:E(X).  (R[x1;y] ⇒ R[x2;y] ⇒ (x1 = x2 ∈ Id))
9. L : Id List@i
10. no_repeats(Id;L)
11. 0 < ||L||
12. (∀x∈L.∃y:E(X). (R[x;y] ∧ (↑P[y])))@i
13. f : ℕ||L|| ⟶ {y:E(X)| ↑P[y]} 
14. Inj(ℕ||L||;{y:E(X)| ↑P[y]} ;f)
15. i : ℕ||L||@i
16. j : ℕ||L||@i
⊢ loc(f i) = loc(f j) ∈ Id

---

Latex:

---

Latex:
\mforall{}[Info:Type]
    \mforall{}es:EO+(Info)
        \mforall{}[T:Type]
            \mforall{}X:EClass(T).  \mforall{}P:E(X)  {}\mrightarrow{}  \mBbbB{}.
                \mforall{}[R:Id  {}\mrightarrow{}  E(X)  {}\mrightarrow{}  \mBbbP{}]
                    \mforall{}L:Id  List
                        ((\mforall{}x\mmember{}L.\mexists{}y:E(X).  (R[x;y]  \mwedge{}  (\muparrow{}P[y])))
                              {}\mRightarrow{}  (\mexists{}e:\{e:E(X)|  \muparrow{}P[e]\}  .  (||L||  \mleq{}  ||filter(\mlambda{}e.P[e];\mleq{}(X)(e))||)))  supposing 
                              (0  <  ||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{}e1,e2:E(X).    (loc(e1)  =  loc(e2))  supposing  ((\muparrow{}P[e2])  and  (\muparrow{}P[e1]))


By

---

Latex:
WithCumulativity((Auto
                                    THEN  (InstLemma  `l\_all\_exists\_injection`  [\mkleeneopen{}Id\mkleeneclose{};\mkleeneopen{}E(X)\mkleeneclose{};\mkleeneopen{}R\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}e.\muparrow{}P[e]\mkleeneclose{};\mkleeneopen{}L\mkleeneclose{}]\mcdot{}
                                                THENA  Auto
                                                )
                                    THEN  D  -1
                                    THEN  UsingVars  [`f']  (BLemma  `filter-interface-predecessors-lower-bound3`)
                                    THEN  Auto))

---

Home Index