---

Step * 2 of Lemma alle-at-iff


1. es : EO@i'
2. i : Id@i
3. [P] : {e:E| loc(e) = i ∈ Id}  ─→ ℙ
4. ∀e@i.P[e]@i
⊢ ∀e@i.P[pred(e)] ⇒ P[e] supposing ¬↑first(e)
BY
{ ((RepeatFor 3 ((ParallelOp (-1))))⋅ THEN Auto) }

---

Latex:



1.  es  :  EO@i'
2.  i  :  Id@i
3.  [P]  :  \{e:E|  loc(e)  =  i\}    {}\mrightarrow{}  \mBbbP{}
4.  \mforall{}e@i.P[e]@i
\mvdash{}  \mforall{}e@i.P[pred(e)]  {}\mRightarrow{}  P[e]  supposing  \mneg{}\muparrow{}first(e)


By

((RepeatFor  3  ((ParallelOp  (-1))))\mcdot{}  THEN  Auto)

---

Home Index