---

Step * of Lemma nth_tl-es-before

∀[es:EO]. ∀[e:E]. ∀[n:ℕ||before(e)||].  (nth_tl(n;before(e)) = filter(λa.before(e)[n] ≤loc a;before(e)) ∈ (E List))
BY
{ (Auto THEN RepeatFor 2 (MoveToConcl (-1)) THEN CausalInd' THEN Auto) }

1
1. es : EO
2. e : E@i
3. ∀e1:E
     ((e1 < e) ⇒ (∀n:ℕ||before(e1)||. (nth_tl(n;before(e1)) = filter(λa.before(e1)[n] ≤loc a;before(e1)) ∈ (E List))))
4. n : ℕ||before(e)||@i
⊢ nth_tl(n;before(e)) = filter(λa.before(e)[n] ≤loc a;before(e)) ∈ (E List)

---

Latex:


\mforall{}[es:EO].  \mforall{}[e:E].  \mforall{}[n:\mBbbN{}||before(e)||].
    (nth\_tl(n;before(e))  =  filter(\mlambda{}a.before(e)[n]  \mleq{}loc  a;before(e)))


By

(Auto  THEN  RepeatFor  2  (MoveToConcl  (-1))  THEN  CausalInd'  THEN  Auto)

---

Home Index