---

Step * 1 of Lemma bind-return-right


1. Info : Type
2. T : Type
3. X : EClass(T)
4. es : EO+(Info)
5. x : E
⊢ (X es x) = (X >x> return-class(x) es x) ∈ bag(T)
BY
{ (RenameVar `e' (-1)
   THEN RepUR ``bind-class`` 0
   THEN (Unfold `es-le-before` 0 THEN Fold `bag-append` 0)
   THEN (GenConcl ⌈before(e) = be ∈ bag({e':E| (e' <loc e)} )⌉⋅
         THENA (Auto THEN SubsumeC ⌈{e':E| (e' <loc e)}  List⌉⋅ THEN Auto)
         )
   THEN skip{(RepUR ``return-class`` 0
              THEN Fold `single-bag` 0
              THEN (InstLemma `bag-combine-append-left` [⌈{e':E| e' ≤loc e } ⌉;⌈T⌉]⋅ THENA Auto)
              THEN (RWO "-1" 0 THENA (Auto THEN Auto))
              THEN (RW (AddrC [2] (RevLemmaC `bag-empty-append`)) 0 THENA Auto)
              THEN EqCD
              THEN Auto)}) }

1
1. Info : Type
2. T : Type
3. X : EClass(T)
4. es : EO+(Info)
5. e : E
6. be : bag({e':E| (e' <loc e)} )@i
7. before(e) = be ∈ bag({e':E| (e' <loc e)} )@i
⊢ (X es e) = ∪e'∈be + [e].∪x∈X es e'.return-class(x) es.e' e ∈ bag(T)

---

Latex:



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


By

(RenameVar  `e'  (-1)
  THEN  RepUR  ``bind-class``  0
  THEN  (Unfold  `es-le-before`  0  THEN  Fold  `bag-append`  0)
  THEN  (GenConcl  \mkleeneopen{}before(e)  =  be\mkleeneclose{}\mcdot{}  THENA  (Auto  THEN  SubsumeC  \mkleeneopen{}\{e':E|  (e'  <loc  e)\}    List\mkleeneclose{}\mcdot{}  THEN  Auto))
  THEN  skip\{(RepUR  ``return-class``  0
                        THEN  Fold  `single-bag`  0
                        THEN  (InstLemma  `bag-combine-append-left`  [\mkleeneopen{}\{e':E|  e'  \mleq{}loc  e  \}  \mkleeneclose{};\mkleeneopen{}T\mkleeneclose{}]\mcdot{}  THENA  Auto)
                        THEN  (RWO  "-1"  0  THENA  (Auto  THEN  Auto))
                        THEN  (RW  (AddrC  [2]  (RevLemmaC  `bag-empty-append`))  0  THENA  Auto)
                        THEN  EqCD
                        THEN  Auto)\})

---

Home Index