---

Step * of Lemma loop-class-memory_wf

∀[Info,B:Type]. ∀[X:EClass(B ─→ B)]. ∀[init:Id ─→ bag(B)].  (loop-class-memory(X;init) ∈ EClass(B))
BY
{ (Auto
   THEN Unfold `eclass` 0
   THEN RepeatFor 2 ((BetterExt THEN Auto))
   THEN MoveToConcl (-1)
   THEN CausalInd'
   THEN RecUnfold `loop-class-memory` 0
   THEN RepUR ``primed-class-opt`` 0
   THEN GenConclAtAddr [2;1]) }

1
.....wf..... 
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. ∀e1:E. ((e1 < e) ⇒ (loop-class-memory(X;init) es e1 ∈ bag(B)))
⊢ last(λe'.0 <z #(eclass3(X;loop-class-memory(X;init)) es e')) e ∈ (∃e':{E
  ((e' <loc e)
  ∧ (↑((λe'.0 <z #(eclass3(X;loop-class-memory(X;init)) es e')) e'))
  ∧ (∀e'':E. ((e' <loc e'') ⇒ (e'' <loc e) ⇒ (¬↑((λe'.0 <z #(eclass3(X;loop-class-memory(X;init)) es e')) e'')))))})
  ∨ (¬(∃e':{E| ((e' <loc e) ∧ (↑((λe'.0 <z #(eclass3(X;loop-class-memory(X;init)) es e')) e')))}))

2
.....wf..... 
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. ∀e1:E. ((e1 < e) ⇒ (loop-class-memory(X;init) es e1 ∈ bag(B)))
⊢ (∃e':{E| ((e' <loc e)
           ∧ (↑((λe'.0 <z #(eclass3(X;loop-class-memory(X;init)) es e')) e'))
           ∧ (∀e'':E
                ((e' <loc e'')
                ⇒ (e'' <loc e)
                ⇒ (¬↑((λe'.0 <z #(eclass3(X;loop-class-memory(X;init)) es e')) e'')))))})
  ∨ (¬(∃e':{E| ((e' <loc e) ∧ (↑((λe'.0 <z #(eclass3(X;loop-class-memory(X;init)) es e')) 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. ∀e1:E. ((e1 < e) ⇒ (loop-class-memory(X;init) es e1 ∈ bag(B)))
8. v : (∃e':{E| ((e' <loc e)
                ∧ (↑((λe'.0 <z #(eclass3(X;loop-class-memory(X;init)) es e')) e'))
                ∧ (∀e'':E
                     ((e' <loc e'')
                     ⇒ (e'' <loc e)
                     ⇒ (¬↑((λe'.0 <z #(eclass3(X;loop-class-memory(X;init)) es e')) e'')))))})
∨ (¬(∃e':{E| ((e' <loc e) ∧ (↑((λe'.0 <z #(eclass3(X;loop-class-memory(X;init)) es e')) e')))}))@i
9. (last(λe'.0 <z #(eclass3(X;loop-class-memory(X;init)) es e')) e)
= v
∈ ((∃e':{E| ((e' <loc e)
            ∧ (↑((λe'.0 <z #(eclass3(X;loop-class-memory(X;init)) es e')) e'))
            ∧ (∀e'':E
                 ((e' <loc e'')
                 ⇒ (e'' <loc e)
                 ⇒ (¬↑((λe'.0 <z #(eclass3(X;loop-class-memory(X;init)) es e')) e'')))))})
  ∨ (¬(∃e':{E| ((e' <loc e) ∧ (↑((λe'.0 <z #(eclass3(X;loop-class-memory(X;init)) es e')) e')))})))@i
⊢ case v of inl(e') => eclass3(X;loop-class-memory(X;init)) es e' | inr(x) => init loc(e) ∈ bag(B)

---

Latex:

---

Latex:
\mforall{}[Info,B:Type].  \mforall{}[X:EClass(B  {}\mrightarrow{}  B)].  \mforall{}[init:Id  {}\mrightarrow{}  bag(B)].    (loop-class-memory(X;init)  \mmember{}  EClass(B))


By

---

Latex:
(Auto
  THEN  Unfold  `eclass`  0
  THEN  RepeatFor  2  ((BetterExt  THEN  Auto))
  THEN  MoveToConcl  (-1)
  THEN  CausalInd'
  THEN  RecUnfold  `loop-class-memory`  0
  THEN  RepUR  ``primed-class-opt``  0
  THEN  GenConclAtAddr  [2;1])

---

Home Index