---

Step * of Lemma loop-class-memory-prior

∀[Info,B:Type]. ∀[X:EClass(B ⟶ B)]. ∀[init:Id ⟶ bag(B)].
  ∀es:EO+(Info). ∀e:E.
    ∀[v:B]
      uiff(v ∈ Prior(loop-class-memory(X;init))?init(e);((↑first(e)) ∧ v ↓∈ init loc(e))
      ∨ ((¬↑first(e)) ∧ v ∈ loop-class-memory(X;init)(pred(e))))
BY
{ ((UnivCD THENA Auto) THEN (Decide ⌜↑first(e)⌝⋅ THENA Auto) THEN Auto) }

1
1. Info : Type
2. B : Type
3. X : EClass(B ⟶ B)
4. init : Id ⟶ bag(B)
5. es : EO+(Info)@i'
6. e : E@i
7. v : B
8. ↑first(e)
9. v ∈ Prior(loop-class-memory(X;init))?init(e)
10. ↑first(e)
⊢ v ↓∈ init loc(e)

2
1. Info : Type
2. B : Type
3. X : EClass(B ⟶ B)
4. init : Id ⟶ bag(B)
5. es : EO+(Info)@i'
6. e : E@i
7. v : B
8. ↑first(e)
9. ((↑first(e)) ∧ v ↓∈ init loc(e)) ∨ ((¬↑first(e)) ∧ v ∈ loop-class-memory(X;init)(pred(e)))
⊢ v ∈ Prior(loop-class-memory(X;init))?init(e)

3
1. [Info] : Type
2. [B] : Type
3. [X] : EClass(B ⟶ B)
4. [init] : Id ⟶ bag(B)
5. es : EO+(Info)@i'
6. e : E@i
7. [v] : B
8. ¬↑first(e)
9. v ∈ Prior(loop-class-memory(X;init))?init(e)
10. ¬↑first(e)
⊢ v ∈ loop-class-memory(X;init)(pred(e))

4
1. Info : Type
2. B : Type
3. X : EClass(B ⟶ B)
4. init : Id ⟶ bag(B)
5. es : EO+(Info)@i'
6. e : E@i
7. v : B
8. ¬↑first(e)
9. ((↑first(e)) ∧ v ↓∈ init loc(e)) ∨ ((¬↑first(e)) ∧ v ∈ loop-class-memory(X;init)(pred(e)))
⊢ v ∈ Prior(loop-class-memory(X;init))?init(e)

---

Latex:

---

Latex:
\mforall{}[Info,B:Type].  \mforall{}[X:EClass(B  {}\mrightarrow{}  B)].  \mforall{}[init:Id  {}\mrightarrow{}  bag(B)].
    \mforall{}es:EO+(Info).  \mforall{}e:E.
        \mforall{}[v:B]
            uiff(v  \mmember{}  Prior(loop-class-memory(X;init))?init(e);((\muparrow{}first(e))  \mwedge{}  v  \mdownarrow{}\mmember{}  init  loc(e))
            \mvee{}  ((\mneg{}\muparrow{}first(e))  \mwedge{}  v  \mmember{}  loop-class-memory(X;init)(pred(e))))


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  (Decide  \mkleeneopen{}\muparrow{}first(e)\mkleeneclose{}\mcdot{}  THENA  Auto)  THEN  Auto)

---

Home Index