---

Step * 2 of Lemma eclass-cond-classrel


1. Info : Type
2. B : Type
3. X : EClass(B ─→ B)
4. Y : EClass(B)
5. es : EO+(Info)
6. e : E
7. v : B
8. ↓if e ∈b X then ∃f:B ─→ B. ∃b:B. (f ∈ X(e) ∧ b ∈ Y(e) ∧ (v = (f b) ∈ B)) else v ∈ Y(e) fi 
⊢ v ∈ eclass-cond(X;Y)(e)
BY
{ ((SplitOnHypITE (-1) THENA Auto)
   THEN RepUR ``eclass-cond classrel class-ap`` 0
   THEN OldAutoSplit
   THEN Try (Fold `classrel` 0)
   THEN Try (Complete ((D (-3) THEN Unhide THEN Auto)))
   THEN BLemma `eclass3-classrel`
   THEN Auto) }

---

Latex:



1.  Info  :  Type
2.  B  :  Type
3.  X  :  EClass(B  {}\mrightarrow{}  B)
4.  Y  :  EClass(B)
5.  es  :  EO+(Info)
6.  e  :  E
7.  v  :  B
8.  \mdownarrow{}if  e  \mmember{}\msubb{}  X  then  \mexists{}f:B  {}\mrightarrow{}  B.  \mexists{}b:B.  (f  \mmember{}  X(e)  \mwedge{}  b  \mmember{}  Y(e)  \mwedge{}  (v  =  (f  b)))  else  v  \mmember{}  Y(e)  fi 
\mvdash{}  v  \mmember{}  eclass-cond(X;Y)(e)


By

((SplitOnHypITE  (-1)  THENA  Auto)
  THEN  RepUR  ``eclass-cond  classrel  class-ap``  0
  THEN  OldAutoSplit
  THEN  Try  (Fold  `classrel`  0)
  THEN  Try  (Complete  ((D  (-3)  THEN  Unhide  THEN  Auto)))
  THEN  BLemma  `eclass3-classrel`
  THEN  Auto)

---

Home Index