---

Step * of Lemma es-interface-state_wf

∀[Info,T,A:Type]. ∀[X:EClass(T)]. ∀[g:(T List) ⟶ bag(A)].  (es-interface-state(X; g) ∈ EClass(A))
BY
{ (Auto
   THEN Unfolds ``es-interface-state eclass`` 0
   THEN RepeatFor 3 ((MemCD THENA Auto))
   THEN MemCD
   THEN Try (Complete (Auto))) }

1
.....subterm..... T:t
3:n
1. Info : Type
2. T : Type
3. A : Type
4. X : EClass(T)
5. g : (T List) ⟶ bag(A)
6. es : EO+(Info)@i'
7. e : E@i
⊢ filter(λe.e ∈b X;≤loc(e)) ∈ E(X) List

---

Latex:

---

Latex:
\mforall{}[Info,T,A:Type].  \mforall{}[X:EClass(T)].  \mforall{}[g:(T  List)  {}\mrightarrow{}  bag(A)].    (es-interface-state(X;  g)  \mmember{}  EClass(A))


By

---

Latex:
(Auto
  THEN  Unfolds  ``es-interface-state  eclass``  0
  THEN  RepeatFor  3  ((MemCD  THENA  Auto))
  THEN  MemCD
  THEN  Try  (Complete  (Auto)))

---

Home Index