---

Step * of Lemma return-loc-bag-class-program_wf

∀[Info,B:Type]. ∀[x:Id ⟶ bag(B)].
  return-loc-bag-class-program(x) ∈ LocalClass(return-loc-bag-class(x)) supposing valueall-type(B)
BY
{ (Auto
   THEN RepUR ``return-loc-bag-class-program hdf-return`` 0
   THEN MemTypeCD
   THEN Auto
   THEN Reduce 0
   THEN RepUR ``return-loc-bag-class class-ap`` 0
   THEN AutoSplit
   THEN RecUnfold `es-before` 0
   THEN AutoSplit
   THEN Reduce 0
   THEN Try (Complete ((RepUR ``hdf-run hdf-ap`` 0 THEN Auto)))
   THEN GenConclAtAddr [3;1;1;2]
   THEN (Assert ⌜0 < ||v||⌝⋅
         THENA ((RWO "map_append_sq" (-1) THENA Auto) THEN (RevHypSubst' (-1) 0 THENA Auto) THEN Reduce 0 THEN Auto')
         )
   THEN Thin (-2)
   THEN D (-2)
   THEN Reduce (-1)
   THEN Auto
   THEN Reduce 0
   THEN RepUR ``hdf-run hdf-ap`` 0
   THEN (RWO "iterate-hdf-halt" 0 THENA Auto)
   THEN RepUR ``hdf-halt`` 0
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[Info,B:Type].  \mforall{}[x:Id  {}\mrightarrow{}  bag(B)].
    return-loc-bag-class-program(x)  \mmember{}  LocalClass(return-loc-bag-class(x))  supposing  valueall-type(B)


By

---

Latex:
(Auto
  THEN  RepUR  ``return-loc-bag-class-program  hdf-return``  0
  THEN  MemTypeCD
  THEN  Auto
  THEN  Reduce  0
  THEN  RepUR  ``return-loc-bag-class  class-ap``  0
  THEN  AutoSplit
  THEN  RecUnfold  `es-before`  0
  THEN  AutoSplit
  THEN  Reduce  0
  THEN  Try  (Complete  ((RepUR  ``hdf-run  hdf-ap``  0  THEN  Auto)))
  THEN  GenConclAtAddr  [3;1;1;2]
  THEN  (Assert  \mkleeneopen{}0  <  ||v||\mkleeneclose{}\mcdot{}
              THENA  ((RWO  "map\_append\_sq"  (-1)  THENA  Auto)
                            THEN  (RevHypSubst'  (-1)  0  THENA  Auto)
                            THEN  Reduce  0
                            THEN  Auto')
              )
  THEN  Thin  (-2)
  THEN  D  (-2)
  THEN  Reduce  (-1)
  THEN  Auto
  THEN  Reduce  0
  THEN  RepUR  ``hdf-run  hdf-ap``  0
  THEN  (RWO  "iterate-hdf-halt"  0  THENA  Auto)
  THEN  RepUR  ``hdf-halt``  0
  THEN  Auto)

---

Home Index