---

Step * 1 1 2 of Lemma bind-return-right

.....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)
BY
{ ((InstLemma `bag-combine-single-left` [⌈{e':E| e' = e ∈ E} ⌉;⌈T⌉]⋅ THENA Auto)
   THEN (RWO  "-1" 0 THENA (Auto THEN SubsumeC ⌈E⌉⋅ THEN Auto))
   THEN (RWO "eo-forward-first-trivial" 0 THENA Auto)
   THEN Reduce 0) }

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
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))
9. ∀[f:{e':E| e' = e ∈ E}  ─→ bag(T)]. ∀[a:{e':E| e' = e ∈ E} ].  (∪x∈{a}.f[x] ~ f[a])
10. x : Base
⊢ e = e ∈ E

2
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))
9. ∀[f:{e':E| e' = e ∈ E}  ─→ bag(T)]. ∀[a:{e':E| e' = e ∈ E} ].  (∪x∈{a}.f[x] ~ f[a])
⊢ (X es e) = ∪x∈X es e.{x} ∈ bag(T)

---

Latex:


.....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@i
8.  \mforall{}[ba,bb:bag(\{e':E|  e'  \mleq{}loc  e  \}  )].  \mforall{}[f:\{e':E|  e'  \mleq{}loc  e  \}    {}\mrightarrow{}  bag(T)].
          (\mcup{}x\mmember{}ba  +  bb.f[x]  =  (\mcup{}x\mmember{}ba.f[x]  +  \mcup{}x\mmember{}bb.f[x]))
\mvdash{}  (X  es  e)  =  \mcup{}e'\mmember{}\{e\}.\mcup{}x\mmember{}X  es  e'.if  first(e)  then  \{x\}  else  \{\}  fi 


By

((InstLemma  `bag-combine-single-left`  [\mkleeneopen{}\{e':E|  e'  =  e\}  \mkleeneclose{};\mkleeneopen{}T\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (RWO    "-1"  0  THENA  (Auto  THEN  SubsumeC  \mkleeneopen{}E\mkleeneclose{}\mcdot{}  THEN  Auto))
  THEN  (RWO  "eo-forward-first-trivial"  0  THENA  Auto)
  THEN  Reduce  0)

---

Home Index