---

Step * of Lemma Memory-loc-class-functional

∀[Info,A,S:Type]. ∀[init:Id ─→ bag(S)]. ∀[f:Id ─→ A ─→ S ─→ S]. ∀[X:EClass(A)]. ∀[es:EO+(Info)].
  (Memory-loc-class(f;init;X) is functional) supposing 
     (single-valued-classrel(es;X;A) and 
     (∀l:Id. single-valued-bag(init l;S)) and 
     (∀l:Id. (1 ≤ #(init l))))
BY
{ ((UnivCD THENA MaAuto)
   THEN Unfold `es-functional-class` 0
   THEN Auto
   THEN Try (BLemma `Memory-loc-class-single-val`)
   THEN Try (BLemma `Memory-loc-class-total`)
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[Info,A,S:Type].  \mforall{}[init:Id  {}\mrightarrow{}  bag(S)].  \mforall{}[f:Id  {}\mrightarrow{}  A  {}\mrightarrow{}  S  {}\mrightarrow{}  S].  \mforall{}[X:EClass(A)].  \mforall{}[es:EO+(Info)].
    (Memory-loc-class(f;init;X)  is  functional)  supposing 
          (single-valued-classrel(es;X;A)  and 
          (\mforall{}l:Id.  single-valued-bag(init  l;S))  and 
          (\mforall{}l:Id.  (1  \mleq{}  \#(init  l))))


By

---

Latex:
((UnivCD  THENA  MaAuto)
  THEN  Unfold  `es-functional-class`  0
  THEN  Auto
  THEN  Try  (BLemma  `Memory-loc-class-single-val`)
  THEN  Try  (BLemma  `Memory-loc-class-total`)
  THEN  Auto)

---

Home Index