---

Step * 1 of Lemma bind-zero-right


1. Info : Type
2. T : Type
3. X : EClass(T)
4. Empty ∈ EClass(T)
5. es : EO+(Info)
6. x : E
⊢ (Empty es x) = (X >x> Empty es x) ∈ bag(T)
BY
{ (RenameVar `e' (-1)
   THEN RepUR ``bind-class es-empty-interface eclass-bag-val`` 0
   THEN (GenConcl ⌈≤loc(e) = B ∈ bag({e':E| e' ≤loc e } )⌉⋅ THENA (Auto THEN SubsumeC ⌈{e':E| e' ≤loc e }  List⌉⋅ THEN A\000Cuto))
   THEN (Assert {} = ∪e'∈B.{} ∈ bag(T) BY
               (RWW "bag-combine-empty-right" 0⋅ THEN Auto)⋅)
   THEN NthHypEq (-1)
   THEN RepeatFor 2 ((EqCD THEN Auto))) }

---

Latex:



1.  Info  :  Type
2.  T  :  Type
3.  X  :  EClass(T)
4.  Empty  \mmember{}  EClass(T)
5.  es  :  EO+(Info)
6.  x  :  E
\mvdash{}  (Empty  es  x)  =  (X  >x>  Empty  es  x)


By

(RenameVar  `e'  (-1)
  THEN  RepUR  ``bind-class  es-empty-interface  eclass-bag-val``  0
  THEN  (GenConcl  \mkleeneopen{}\mleq{}loc(e)  =  B\mkleeneclose{}\mcdot{}  THENA  (Auto  THEN  SubsumeC  \mkleeneopen{}\{e':E|  e'  \mleq{}loc  e  \}    List\mkleeneclose{}\mcdot{}  THEN  Auto))
  THEN  (Assert  \{\}  =  \mcup{}e'\mmember{}B.\{\}  BY
                          (RWW  "bag-combine-empty-right"  0\mcdot{}  THEN  Auto)\mcdot{})
  THEN  NthHypEq  (-1)
  THEN  RepeatFor  2  ((EqCD  THEN  Auto)))

---

Home Index