---

Step * of Lemma Memory-classrel

∀[Info,B,A:Type]. ∀[f:A ─→ B ─→ B]. ∀[init:Id ─→ bag(B)].
  ∀X:EClass(A). ∀es:EO+(Info). ∀e:E.
    ∀[v:B]
      (v ∈ Memory-class(f;init;X)(e)
      ⇐⇒ ((↑first(e)) ∧ v ↓∈ init loc(e)) ∨ ((¬↑first(e)) ∧ iterated_classrel(es;B;A;f;init;X;pred(e);v)))
BY
{ ((UnivCD THENA (Auto THEN Unfold `label` 0 THEN Auto))
   THEN (Unhide THENA MaAuto)
   THEN Try ((AutoBoolCase ⌈first(e)⌉⋅
              THEN D 0
              THEN MaAuto
              THEN SqExRepD
              THEN SplitOrHyps
              THEN Auto
              THEN (D (-2) THEN Unhide THEN Auto)
              THEN SplitOrHyps
              THEN Auto))) }

1
1. Info : Type
2. B : Type
3. A : Type
4. f : A ─→ B ─→ B
5. init : Id ─→ bag(B)
6. X : EClass(A)@i'
7. es : EO+(Info)@i'
8. e : E@i
9. v : B
⊢ v ∈ Memory-class(f;init;X)(e)
⇐⇒ ((↑first(e)) ∧ v ↓∈ init loc(e)) ∨ ((¬↑first(e)) ∧ iterated_classrel(es;B;A;f;init;X;pred(e);v))

---

Latex:

---

Latex:
\mforall{}[Info,B,A:Type].  \mforall{}[f:A  {}\mrightarrow{}  B  {}\mrightarrow{}  B].  \mforall{}[init:Id  {}\mrightarrow{}  bag(B)].
    \mforall{}X:EClass(A).  \mforall{}es:EO+(Info).  \mforall{}e:E.
        \mforall{}[v:B]
            (v  \mmember{}  Memory-class(f;init;X)(e)
            \mLeftarrow{}{}\mRightarrow{}  ((\muparrow{}first(e))  \mwedge{}  v  \mdownarrow{}\mmember{}  init  loc(e))
                    \mvee{}  ((\mneg{}\muparrow{}first(e))  \mwedge{}  iterated\_classrel(es;B;A;f;init;X;pred(e);v)))


By

---

Latex:
((UnivCD  THENA  (Auto  THEN  Unfold  `label`  0  THEN  Auto))
  THEN  (Unhide  THENA  MaAuto)
  THEN  Try  ((AutoBoolCase  \mkleeneopen{}first(e)\mkleeneclose{}\mcdot{}
                        THEN  D  0
                        THEN  MaAuto
                        THEN  SqExRepD
                        THEN  SplitOrHyps
                        THEN  Auto
                        THEN  (D  (-2)  THEN  Unhide  THEN  Auto)
                        THEN  SplitOrHyps
                        THEN  Auto)))

---

Home Index