---

Step * of Lemma es-prior-interface-vals-nil

∀[Info:Type]. ∀[es:EO+(Info)]. ∀[A:Type]. ∀[X:EClass(A)]. ∀[e:E].  uiff(X(<e) = [] ∈ (A List);¬↑e ∈b prior(X))
BY
{ (InstLemma `es-prior-interface-vals-property` []
   THEN (RepeatFor 5 (ParallelLast') THEN (Unhide THENA Auto))
   THEN MoveToConcl (-1)
   THEN AutoSplit
   THEN Auto) }

1
1. Info : Type
2. es : EO+(Info)
3. A : Type
4. X : EClass(A)
5. e : E
6. ↑e ∈b prior(X)
7. X(<e) = (X(<prior(X)(e)) @ [X(prior(X)(e))]) ∈ (A List)@i
8. X(<e) = [] ∈ (A List)
⊢ ¬True

2
1. Info : Type
2. es : EO+(Info)
3. A : Type
4. X : EClass(A)
5. e : E
6. ↑e ∈b prior(X)
⊢ prior(X)(e) ∈ E

---

Latex:

---

Latex:
\mforall{}[Info:Type].  \mforall{}[es:EO+(Info)].  \mforall{}[A:Type].  \mforall{}[X:EClass(A)].  \mforall{}[e:E].    uiff(X(<e)  =  [];\mneg{}\muparrow{}e  \mmember{}\msubb{}  prior(X))


By

---

Latex:
(InstLemma  `es-prior-interface-vals-property`  []
  THEN  (RepeatFor  5  (ParallelLast')  THEN  (Unhide  THENA  Auto))
  THEN  MoveToConcl  (-1)
  THEN  AutoSplit
  THEN  Auto)

---

Home Index