---

Step * 1 1 of Lemma Memory-classrel1

.....equality..... 
1. Info : Type
2. B : Type
3. A : Type
4. f : A ─→ B ─→ B
5. init : Id ─→ bag(B)
6. X : EClass(A)
7. es : EO+(Info)
8. e : E
9. v : B
⊢ v ∈ Memory-class(f;init;X)(e) ~ if first(e) then v ↓∈ init loc(e)
if 0 <z #(Accum-class(f;init;X) es pred(e)) then v ∈ Accum-class(f;init;X)(pred(e))
else v ∈ Memory-class(f;init;X)(pred(e))
fi 
BY
{ (RW (AddrC [1] (UnfoldC `Memory-class`)) 0
   THEN RepUR ``primed-class-opt classrel`` 0
   THEN RecUnfold `es-local-pred` 0
   THEN Reduce 0
   THEN RepeatFor 2 (AutoSplit)
   THEN Try ((Auto THEN Fold `eclass` 0 THEN Auto))
   THEN RW (AddrC [2] (UnfoldC `Memory-class`)) 0⋅
   THEN RepUR ``primed-class-opt classrel`` 0
   THEN RepeatFor 3 ((EqCD THEN Try (Trivial)))
   THEN MaAuto)⋅ }

---

Latex:

---

Latex:
.....equality..... 
1.  Info  :  Type
2.  B  :  Type
3.  A  :  Type
4.  f  :  A  {}\mrightarrow{}  B  {}\mrightarrow{}  B
5.  init  :  Id  {}\mrightarrow{}  bag(B)
6.  X  :  EClass(A)
7.  es  :  EO+(Info)
8.  e  :  E
9.  v  :  B
\mvdash{}  v  \mmember{}  Memory-class(f;init;X)(e)  \msim{}  if  first(e)  then  v  \mdownarrow{}\mmember{}  init  loc(e)
if  0  <z  \#(Accum-class(f;init;X)  es  pred(e))  then  v  \mmember{}  Accum-class(f;init;X)(pred(e))
else  v  \mmember{}  Memory-class(f;init;X)(pred(e))
fi 


By

---

Latex:
(RW  (AddrC  [1]  (UnfoldC  `Memory-class`))  0
  THEN  RepUR  ``primed-class-opt  classrel``  0
  THEN  RecUnfold  `es-local-pred`  0
  THEN  Reduce  0
  THEN  RepeatFor  2  (AutoSplit)
  THEN  Try  ((Auto  THEN  Fold  `eclass`  0  THEN  Auto))
  THEN  RW  (AddrC  [2]  (UnfoldC  `Memory-class`))  0\mcdot{}
  THEN  RepUR  ``primed-class-opt  classrel``  0
  THEN  RepeatFor  3  ((EqCD  THEN  Try  (Trivial)))
  THEN  MaAuto)\mcdot{}

---

Home Index