---

Step * 1 1 of Lemma bind-return-right


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)
BY
{ (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 SubsumeC ⌈E⌉⋅ THEN Auto))
   THEN (RW (AddrC [2] (RevLemmaC `bag-empty-append`)) 0 THENA Auto)
   THEN EqCD
   THEN Auto) }

1
.....subterm..... T:t
1:n
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
8. ∀[ba,bb:bag({e':E| e' ≤loc e } )]. ∀[f:{e':E| e' ≤loc e }  ─→ bag(T)].
     (∪x∈ba + bb.f[x] = (∪x∈ba.f[x] + ∪x∈bb.f[x]) ∈ bag(T))
⊢ {} = ∪e'∈be.∪x∈X es e'.if first(e) then {x} else {} fi  ∈ bag(T)

2
.....subterm..... T:t
2:n
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
8. ∀[ba,bb:bag({e':E| e' ≤loc e } )]. ∀[f:{e':E| e' ≤loc e }  ─→ bag(T)].
     (∪x∈ba + bb.f[x] = (∪x∈ba.f[x] + ∪x∈bb.f[x]) ∈ bag(T))
⊢ (X es e) = ∪e'∈{e}.∪x∈X es e'.if first(e) then {x} else {} fi  ∈ bag(T)

---

Latex:



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@i
\mvdash{}  (X  es  e)  =  \mcup{}e'\mmember{}be  +  [e].\mcup{}x\mmember{}X  es  e'.return-class(x)  es.e'  e


By

(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  SubsumeC  \mkleeneopen{}E\mkleeneclose{}\mcdot{}  THEN  Auto))
  THEN  (RW  (AddrC  [2]  (RevLemmaC  `bag-empty-append`))  0  THENA  Auto)
  THEN  EqCD
  THEN  Auto)

---

Home Index