---

Step * 2 of Lemma Accum-loc-class-as-loop-class2


1. Info : Type
2. B : Type
3. A : Type
4. f : Id ─→ A ─→ B ─→ B
5. init : Id ─→ bag(B)
6. X : EClass(A)
7. es : EO+(Info)@i'
8. e : E@i
9. ∀e1:E. ((e1 < e) ⇒ ((loop-class2((f o X);init) es e1) = (Accum-loc-class(f;init;X) es e1) ∈ bag(B)))
⊢ ∪f@0∈λes,e. bag-map(f loc(e);X(e))(e).bag-map(f@0;Prior(Accum-loc-class(f;init;X))?init(e))
= Accum-loc-class(f;init;X)(e)
∈ bag(B)
BY
{ (Unfold `class-ap` 0
   THEN RW (AddrC [3] (UnfoldC `Accum-loc-class`)) 0⋅
   THEN RW (AddrC [3;1;1] UnfoldTopAbC) 0
   THEN RW (AddrC [3;1;1] RecUnfoldTopAbC) 0
   THEN Reduce 0
   THEN Fold `rec-combined-loc-class-opt-1` 0
   THEN Fold `Accum-loc-class` 0) }

1
1. Info : Type
2. B : Type
3. A : Type
4. f : Id ─→ A ─→ B ─→ B
5. init : Id ─→ bag(B)
6. X : EClass(A)
7. es : EO+(Info)@i'
8. e : E@i
9. ∀e1:E. ((e1 < e) ⇒ ((loop-class2((f o X);init) es e1) = (Accum-loc-class(f;init;X) es e1) ∈ bag(B)))
⊢ ∪f@0∈bag-map(f loc(e);X es e).bag-map(f@0;Prior(Accum-loc-class(f;init;X))?init es e)
= (lifting-loc-2(f) loc(e) (X es e) (Prior(Accum-loc-class(f;init;X))?init es e))
∈ bag(B)

---

Latex:

---

Latex:

1.  Info  :  Type
2.  B  :  Type
3.  A  :  Type
4.  f  :  Id  {}\mrightarrow{}  A  {}\mrightarrow{}  B  {}\mrightarrow{}  B
5.  init  :  Id  {}\mrightarrow{}  bag(B)
6.  X  :  EClass(A)
7.  es  :  EO+(Info)@i'
8.  e  :  E@i
9.  \mforall{}e1:E.  ((e1  <  e)  {}\mRightarrow{}  ((loop-class2((f  o  X);init)  es  e1)  =  (Accum-loc-class(f;init;X)  es  e1)))
\mvdash{}  \mcup{}f@0\mmember{}\mlambda{}es,e.  bag-map(f  loc(e);X(e))(e).bag-map(f@0;Prior(Accum-loc-class(f;init;X))?init(e))
=  Accum-loc-class(f;init;X)(e)


By

---

Latex:
(Unfold  `class-ap`  0
  THEN  RW  (AddrC  [3]  (UnfoldC  `Accum-loc-class`))  0\mcdot{}
  THEN  RW  (AddrC  [3;1;1]  UnfoldTopAbC)  0
  THEN  RW  (AddrC  [3;1;1]  RecUnfoldTopAbC)  0
  THEN  Reduce  0
  THEN  Fold  `rec-combined-loc-class-opt-1`  0
  THEN  Fold  `Accum-loc-class`  0)

---

Home Index