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