---

Step * 1 of Lemma Memory-class-es-sv


1. Info : Type
2. A : Type
3. init : Id ─→ bag(Top)
4. f : Top
5. X : EClass(A)
6. es : EO+(Info)
7. ∀l:Id. (#(init l) ≤ 1)
8. es-sv-class(es;X)
9. Memory-class(f;init;X) ∈ EClass(Top)
⊢ es-sv-class(es;Memory-class(f;init;X))
BY
{ (Unfold `Memory-class` 0
   THEN BLemma `primed-class-opt-es-sv`
   THEN Try (Complete (Auto))
   THEN Try (Complete (ProveEsSvClass))
   THEN Unfold `Accum-class` 0
   THEN (BLemma `rec-combined-class-opt-1_wf` THENA Try (Complete (Auto)))
   THEN RepUR ``lifting-2 lifting2 lifting-gen-rev`` 0
   THEN RepeatFor 3 ((RecUnfold `lifting-gen-list-rev` 0⋅ THEN Reduce 0))
   THEN Auto)⋅ }

---

Latex:

---

Latex:

1.  Info  :  Type
2.  A  :  Type
3.  init  :  Id  {}\mrightarrow{}  bag(Top)
4.  f  :  Top
5.  X  :  EClass(A)
6.  es  :  EO+(Info)
7.  \mforall{}l:Id.  (\#(init  l)  \mleq{}  1)
8.  es-sv-class(es;X)
9.  Memory-class(f;init;X)  \mmember{}  EClass(Top)
\mvdash{}  es-sv-class(es;Memory-class(f;init;X))


By

---

Latex:
(Unfold  `Memory-class`  0
  THEN  BLemma  `primed-class-opt-es-sv`
  THEN  Try  (Complete  (Auto))
  THEN  Try  (Complete  (ProveEsSvClass))
  THEN  Unfold  `Accum-class`  0
  THEN  (BLemma  `rec-combined-class-opt-1\_wf`  THENA  Try  (Complete  (Auto)))
  THEN  RepUR  ``lifting-2  lifting2  lifting-gen-rev``  0
  THEN  RepeatFor  3  ((RecUnfold  `lifting-gen-list-rev`  0\mcdot{}  THEN  Reduce  0))
  THEN  Auto)\mcdot{}

---

Home Index