---

Step * 1 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. v ∈ eclass-cond(X;Y)(e)
⊢ ↓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 
BY
{ (RepUR ``eclass-cond classrel`` (-1)
   THEN OldAutoSplit
   THEN SplitOnHypITE (-2)
   THEN Auto
   THEN RepUR ``class-ap`` (-3)
   THEN Try (Fold `classrel` (-3)⋅)
   THEN Auto
   THEN Try (Complete ((D 0 THEN Auto)))
   THEN BLemma `eclass3-classrel`
   THEN Auto) }

---

Latex:

---

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.  v  \mmember{}  eclass-cond(X;Y)(e)
\mvdash{}  \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 


By

---

Latex:
(RepUR  ``eclass-cond  classrel``  (-1)
  THEN  OldAutoSplit
  THEN  SplitOnHypITE  (-2)
  THEN  Auto
  THEN  RepUR  ``class-ap``  (-3)
  THEN  Try  (Fold  `classrel`  (-3)\mcdot{})
  THEN  Auto
  THEN  Try  (Complete  ((D  0  THEN  Auto)))
  THEN  BLemma  `eclass3-classrel`
  THEN  Auto)

---

Home Index