---

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

.....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)
BY
{ (Symmetry
   THEN (Assert ⌈∪e'∈be.{} = {} ∈ bag(T)⌉ BY
               (RWO "bag-combine-empty-right" 0 THEN Auto))
   THEN Try ((NthHypEq  (-1) THEN RepeatFor 2 ((EqCD THEN Auto))))
   THEN ((Assert ⌈∪x∈X es e'.{} = {} ∈ bag(T)⌉ BY
                (RWO "bag-combine-empty-right" 0 THEN Auto))
         THEN Try ((NthHypEq  (-1) THEN RepeatFor 2 ((EqCD THEN Auto))))
         )⋅) }

1
.....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))
9. ∪e'∈be.{} = {} ∈ bag(T)
10. e' : {e':E| (e' <loc e)} @i
11. ∪x∈X es e'.{} = {} ∈ bag(T)
12. x : T@i
⊢ if first(e) then {x} else {} fi  = {} ∈ bag(T)

---

Latex:


.....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@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{}  \{\}  =  \mcup{}e'\mmember{}be.\mcup{}x\mmember{}X  es  e'.if  first(e)  then  \{x\}  else  \{\}  fi 


By

(Symmetry
  THEN  (Assert  \mkleeneopen{}\mcup{}e'\mmember{}be.\{\}  =  \{\}\mkleeneclose{}  BY
                          (RWO  "bag-combine-empty-right"  0  THEN  Auto))
  THEN  Try  ((NthHypEq    (-1)  THEN  RepeatFor  2  ((EqCD  THEN  Auto))))
  THEN  ((Assert  \mkleeneopen{}\mcup{}x\mmember{}X  es  e'.\{\}  =  \{\}\mkleeneclose{}  BY
                            (RWO  "bag-combine-empty-right"  0  THEN  Auto))
              THEN  Try  ((NthHypEq    (-1)  THEN  RepeatFor  2  ((EqCD  THEN  Auto))))
              )\mcdot{})

---

Home Index