---

Step * of Lemma eclass-state-classrel

∀[Info,A,B:Type]. ∀[init:Id ─→ B]. ∀[f:Id ─→ A ─→ B ─→ B]. ∀[X:EClass(A)]. ∀[es:EO+(Info)]. ∀[e:E]. ∀[v:B].
  uiff(v ∈ eclass-state(init;f;X)(e);↓∃b:B
                                       ∃a:A
                                        (a ∈ X(e)
                                        ∧ b ∈ Prior(eclass-state(init;f;X))?λl.{init l}(e)
                                        ∧ (v = (f loc(e) a b) ∈ B)))
BY
{ WithCumulativity(((UnivCD THENA Auto)
                    THEN Unfold `eclass-state` 0
                    THEN (RWW "loop-classrel eclass1-classrel" 0 THENA Auto)
                    THEN Reduce 0
                    THEN Fold `eclass-state` 0
                    THEN Auto
                    THEN SqExRepD)) }

1
1. Info : Type
2. A : Type
3. B : Type
4. init : Id ─→ B
5. f : Id ─→ A ─→ B ─→ B
6. X : EClass(A)
7. es : EO+(Info)
8. e : E
9. v : B
10. f1 : B ─→ bag(B)
11. b : B
12. b1 : A
13. b1 ∈ X(e)
14. f1 = (λb@0.{f loc(e) b1 b@0}) ∈ (B ─→ bag(B))
15. b ∈ Prior(eclass-state(init;f;X))?λl.{init l}(e)
16. v ↓∈ f1 b
⊢ ↓∃b:B. ∃a:A. (a ∈ X(e) ∧ b ∈ Prior(eclass-state(init;f;X))?λl.{init l}(e) ∧ (v = (f loc(e) a b) ∈ B))

2
1. Info : Type
2. A : Type
3. B : Type
4. init : Id ─→ B
5. f : Id ─→ A ─→ B ─→ B
6. X : EClass(A)
7. es : EO+(Info)
8. e : E
9. v : B
10. b : B
11. a : A
12. a ∈ X(e)
13. b ∈ Prior(eclass-state(init;f;X))?λl.{init l}(e)
14. v = (f loc(e) a b) ∈ B
⊢ ↓∃f1:B ─→ bag(B)
    ∃b:B
     ((↓∃b:A. (b ∈ X(e) ∧ (f1 = (λb@0.{f loc(e) b b@0}) ∈ (B ─→ bag(B)))))
     ∧ b ∈ Prior(eclass-state(init;f;X))?λl.{init l}(e)
     ∧ v ↓∈ f1 b)

---

Latex:

---

Latex:
\mforall{}[Info,A,B:Type].  \mforall{}[init:Id  {}\mrightarrow{}  B].  \mforall{}[f:Id  {}\mrightarrow{}  A  {}\mrightarrow{}  B  {}\mrightarrow{}  B].  \mforall{}[X:EClass(A)].  \mforall{}[es:EO+(Info)].  \mforall{}[e:E].
\mforall{}[v:B].
    uiff(v  \mmember{}  eclass-state(init;f;X)(e);\mdownarrow{}\mexists{}b:B
                                                                              \mexists{}a:A
                                                                                (a  \mmember{}  X(e)
                                                                                \mwedge{}  b  \mmember{}  Prior(eclass-state(init;f;X))?\mlambda{}l.\{init  l\}(e)
                                                                                \mwedge{}  (v  =  (f  loc(e)  a  b))))


By

---

Latex:
WithCumulativity(((UnivCD  THENA  Auto)
                                    THEN  Unfold  `eclass-state`  0
                                    THEN  (RWW  "loop-classrel  eclass1-classrel"  0  THENA  Auto)
                                    THEN  Reduce  0
                                    THEN  Fold  `eclass-state`  0
                                    THEN  Auto
                                    THEN  SqExRepD))

---

Home Index