---

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


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 ∈ ℤ))
BY
{ ((RWO "es-interface-predecessors-general-step" (-2)
   THENM (SplitOnHypITE -2  THENM (SplitOnHypITE -3  THENM Reduce (-4)))
   )
   THEN Auto
   )⋅ }

1
.....truecase..... 
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)(prior(X)(e1)) @ [e1])|| = n ∈ ℤ
11. ¬((↑e1 ∈b X) c∧ (↑P[e1]))
12. ↑e1 ∈b prior(X)
13. ↑e1 ∈b X
⊢ ∃e':E. ((e' <loc e1) ∧ (||filter(λe.P[e];≤(X)(e'))|| = n ∈ ℤ))

2
.....falsecase..... 
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)(prior(X)(e1)) @ [])|| = n ∈ ℤ
11. ¬((↑e1 ∈b X) c∧ (↑P[e1]))
12. ↑e1 ∈b prior(X)
13. ¬↑e1 ∈b X
⊢ ∃e':E. ((e' <loc e1) ∧ (||filter(λe.P[e];≤(X)(e'))|| = n ∈ ℤ))

3
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. ||if P[e1] then [e1] else [] fi || = n ∈ ℤ
11. ¬((↑e1 ∈b X) c∧ (↑P[e1]))
12. ¬↑e1 ∈b prior(X)
13. ↑e1 ∈b X
⊢ ∃e':E. ((e' <loc e1) ∧ (||filter(λe.P[e];≤(X)(e'))|| = n ∈ ℤ))

---

Latex:

---

Latex:

1.  Info  :  Type
2.  es  :  EO+(Info)
3.  T  :  Type
4.  X  :  EClass(T)
5.  P  :  E(X)  {}\mrightarrow{}  \mBbbB{}
6.  n  :  \mBbbN{}\msupplus{}
7.  e  :  E
8.  i  :  Id
9.  e1  :  \{e:E|  loc(e)  =  i\}  @i
10.  ||filter(\mlambda{}e.P[e];\mleq{}(X)(e1))||  =  n@i
11.  \mneg{}((\muparrow{}e1  \mmember{}\msubb{}  X)  c\mwedge{}  (\muparrow{}P[e1]))
\mvdash{}  \mexists{}e':E.  ((e'  <loc  e1)  \mwedge{}  (||filter(\mlambda{}e.P[e];\mleq{}(X)(e'))||  =  n))


By

---

Latex:
((RWO  "es-interface-predecessors-general-step"  (-2)
  THENM  (SplitOnHypITE  -2    THENM  (SplitOnHypITE  -3    THENM  Reduce  (-4)))
  )
  THEN  Auto
  )\mcdot{}

---

Home Index