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