---

Step * of Lemma prior-classrel-p-local-pred

∀[T,Info:Type]. ∀[X:EClass(T)]. ∀[es:EO+(Info)]. ∀[e:E]. ∀[v:T].
  uiff(v ∈ Prior(X)(e);↓∃e':E. ((es-p-local-pred(es;λe'.(↓∃w:T. w ∈ X(e'))) e e') ∧ v ∈ X(e')))
BY
{ (InstLemma `prior-classrel` [] THEN RepeatFor 10 ((ParallelLast' THEN Try ((Reduce 0 THEN Complete (Auto)))))) }

1
1. T : Type
2. Info : Type
3. X : EClass(T)
4. es : EO+(Info)
5. e : E
6. v : T
7. v ∈ Prior(X)(e)
8. e' : E
9. v ∈ X(e')
10. (last(λe'.0 <z #(X es e')) e) = (inl e') ∈ (E + Top)
⊢ es-p-local-pred(es;λe'.(↓∃w:T. w ∈ X(e'))) e e'

2
1. T : Type
2. Info : Type
3. X : EClass(T)
4. es : EO+(Info)
5. e : E
6. v : T
7. e' : E
8. v ∈ X(e')
9. es-p-local-pred(es;λe'.(↓∃w:T. w ∈ X(e'))) e e'
⊢ (last(λe'.0 <z #(X es e')) e) = (inl e') ∈ (E + Top)

---

Latex:

---

Latex:
\mforall{}[T,Info:Type].  \mforall{}[X:EClass(T)].  \mforall{}[es:EO+(Info)].  \mforall{}[e:E].  \mforall{}[v:T].
    uiff(v  \mmember{}  Prior(X)(e);\mdownarrow{}\mexists{}e':E.  ((es-p-local-pred(es;\mlambda{}e'.(\mdownarrow{}\mexists{}w:T.  w  \mmember{}  X(e')))  e  e')  \mwedge{}  v  \mmember{}  X(e')))


By

---

Latex:
(InstLemma  `prior-classrel`  []
  THEN  RepeatFor  10  ((ParallelLast'  THEN  Try  ((Reduce  0  THEN  Complete  (Auto)))))
  )

---

Home Index