---

Step * of Lemma State-comb-classrel-mem3

∀[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)) ∧ v ∈ State-comb(init;f;X)(pred(e))))
BY
{ (UnivCD THEN MaAuto) }

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
10. v ∈ Memory-class(f;init;X)(e)@i
⊢ ((↑first(e)) ∧ v ↓∈ init loc(e)) ∨ ((¬↑first(e)) ∧ v ∈ State-comb(init;f;X)(pred(e)))

2
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
10. ((↑first(e)) ∧ v ↓∈ init loc(e)) ∨ ((¬↑first(e)) ∧ v ∈ State-comb(init;f;X)(pred(e)))@i
⊢ v ∈ Memory-class(f;init;X)(e)

---

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{}  v  \mmember{}  State-comb(init;f;X)(pred(e))))


By

---

Latex:
(UnivCD  THEN  MaAuto)

---

Home Index