---

Step * 1 of Lemma eclass-state-classrel


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))
BY
{ (D 0
   THEN InstConcl [⌈b⌉;⌈b1⌉]⋅
   THEN Auto
   THEN (HypSubst (-5) (-3) THENA Auto)
   THEN Reduce (-3)
   THEN BagMemberD (-3)
   THEN Auto)⋅ }

---

Latex:

---

Latex:

1.  Info  :  Type
2.  A  :  Type
3.  B  :  Type
4.  init  :  Id  {}\mrightarrow{}  B
5.  f  :  Id  {}\mrightarrow{}  A  {}\mrightarrow{}  B  {}\mrightarrow{}  B
6.  X  :  EClass(A)
7.  es  :  EO+(Info)
8.  e  :  E
9.  v  :  B
10.  f1  :  B  {}\mrightarrow{}  bag(B)
11.  b  :  B
12.  b1  :  A
13.  b1  \mmember{}  X(e)
14.  f1  =  (\mlambda{}b@0.\{f  loc(e)  b1  b@0\})
15.  b  \mmember{}  Prior(eclass-state(init;f;X))?\mlambda{}l.\{init  l\}(e)
16.  v  \mdownarrow{}\mmember{}  f1  b
\mvdash{}  \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:
(D  0
  THEN  InstConcl  [\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}b1\mkleeneclose{}]\mcdot{}
  THEN  Auto
  THEN  (HypSubst  (-5)  (-3)  THENA  Auto)
  THEN  Reduce  (-3)
  THEN  BagMemberD  (-3)
  THEN  Auto)\mcdot{}

---

Home Index