---

Step * of Lemma bind-return-left

∀[Info,T,S:Type]. ∀[x:T].  ∀f:T ─→ EClass(S). (return-class(x) >z> f[z] = f[x] ∈ EClass(S))
BY
{ ((Auto THEN (InstLemma `bind-class_wf` [⌈Info⌉;⌈T⌉;⌈S⌉]⋅ THENA Auto))
   THEN RepUR ``eclass`` 0⋅
   THEN Symmetry
   THEN Ext
   THEN Auto
   THEN Try (((Fold `eclass` 0 ⋅ THEN Auto) THEN BackThruSomeHyp THEN Auto))
   THEN RenameVar `es' (-1)⋅
   THEN Ext
   THEN Auto
   THEN Try (((Fold `eclass` 0 THEN Auto) ORELSE (GenConclAtAddrType ⌈EClass(S)⌉ [2;1]⋅ THEN Auto THEN BackThruSomeHyp))
             ⋅)
   THEN RenameVar `e' (-1)
   THEN RepUR ``bind-class`` 0) }

1
1. Info : Type
2. T : Type
3. S : Type
4. x : T
5. f : T ─→ EClass(S)@i'
6. ∀[X:EClass(T)]. ∀[Y:T ─→ EClass(S)].  (X >x> Y[x] ∈ EClass(S))
7. es : EO+(Info)
8. e : E
⊢ (f[x] es e) = ∪e'∈≤loc(e).∪z∈return-class(x) es e'.f[z] es.e' e ∈ bag(S)

---

Latex:


\mforall{}[Info,T,S:Type].  \mforall{}[x:T].    \mforall{}f:T  {}\mrightarrow{}  EClass(S).  (return-class(x)  >z>  f[z]  =  f[x])


By

((Auto  THEN  (InstLemma  `bind-class\_wf`  [\mkleeneopen{}Info\mkleeneclose{};\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}S\mkleeneclose{}]\mcdot{}  THENA  Auto))
  THEN  RepUR  ``eclass``  0\mcdot{}
  THEN  Symmetry
  THEN  Ext
  THEN  Auto
  THEN  Try  (((Fold  `eclass`  0  \mcdot{}  THEN  Auto)  THEN  BackThruSomeHyp  THEN  Auto))
  THEN  RenameVar  `es'  (-1)\mcdot{}
  THEN  Ext
  THEN  Auto
  THEN  Try  (((Fold  `eclass`  0  THEN  Auto)
                      ORELSE  (GenConclAtAddrType  \mkleeneopen{}EClass(S)\mkleeneclose{}  [2;1]\mcdot{}  THEN  Auto  THEN  BackThruSomeHyp)
                      )\mcdot{})
  THEN  RenameVar  `e'  (-1)
  THEN  RepUR  ``bind-class``  0)

---

Home Index