---

Step * 2 1 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∈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)
BY
{ (Fold `class-ap` 0
   THEN GenConclAtAddr [3;2]
   THEN RW (AddrC [2] (BasicSymbolicComputeC ``bag-combine bag-map es-loc``)) 0
   THEN Fold `class-ap` 0
   THEN (GenConclAtAddr [3;2] THEN GenConclAtAddr [3;1;3])
   THEN RepUR ``lifting-loc-2 lifting2-loc lifting-loc-gen-rev 
               lifting-gen-rev class-ap`` 0⋅
   THEN RepeatFor 3 ((RecUnfold `lifting-gen-list-rev` 0 THEN Reduce 0))
   THEN (GenApply 4 THENA Auto)
   THEN All Thin)⋅ }

1
1. B : Type
2. A : Type
3. v1 : bag(B)@i
4. v2 : bag(A)@i
5. z : A ─→ B ─→ B@i
⊢ ∪f@0∈bag-map(z;v2).bag-map(f@0;v1) = ∪x∈v2.∪x@0∈v1.{z x x@0} ∈ 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{}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))


By

---

Latex:
(Fold  `class-ap`  0
  THEN  GenConclAtAddr  [3;2]
  THEN  RW  (AddrC  [2]  (BasicSymbolicComputeC  ``bag-combine  bag-map  es-loc``))  0
  THEN  Fold  `class-ap`  0
  THEN  (GenConclAtAddr  [3;2]  THEN  GenConclAtAddr  [3;1;3])
  THEN  RepUR  ``lifting-loc-2  lifting2-loc  lifting-loc-gen-rev 
                          lifting-gen-rev  class-ap``  0\mcdot{}
  THEN  RepeatFor  3  ((RecUnfold  `lifting-gen-list-rev`  0  THEN  Reduce  0))
  THEN  (GenApply  4  THENA  Auto)
  THEN  All  Thin)\mcdot{}

---

Home Index