---

Step * 1 of Lemma primed-class-prior-val


1. Info : Type
2. T : Type
3. X : EClass(T)
4. Singlevalued(X)
5. es : EO+(Info)
6. e : E
⊢ (Prior(X) es e) = ((X)' es e) ∈ bag(T)
BY
{ (RepUR ``es-prior-val primed-class es-prior-interface local-pred-class`` 0 THEN RepUR ``in-eclass eclass-val`` 0)⋅ }

1
1. Info : Type
2. T : Type
3. X : EClass(T)
4. Singlevalued(X)
5. es : EO+(Info)
6. e : E
⊢ case last(λe'.0 <z #(X es e')) e of inl(e') => X es e' | inr(x) => {}
= if (#(case last(λe.(#(X es e) =z 1)) e of inl(e') => {e'} | inr(x) => {}) =z 1)
  then {only(X es only(case last(λe.(#(X es e) =z 1)) e of inl(e') => {e'} | inr(x) => {}))}
  else {}
  fi 
∈ bag(T)

---

Latex:

---

Latex:

1.  Info  :  Type
2.  T  :  Type
3.  X  :  EClass(T)
4.  Singlevalued(X)
5.  es  :  EO+(Info)
6.  e  :  E
\mvdash{}  (Prior(X)  es  e)  =  ((X)'  es  e)


By

---

Latex:
(RepUR  ``es-prior-val  primed-class  es-prior-interface  local-pred-class``  0
  THEN  RepUR  ``in-eclass  eclass-val``  0
  )\mcdot{}

---

Home Index