---

Step * of Lemma eo-forward-pred?

∀[Info:Type]. ∀[eo:EO+(Info)]. ∀[e:E].
  ∀e1:E. (es-pred?(eo.e;e1) = if es-eq(eo) e1 e then inr ⋅  else es-pred?(eo;e1) fi  ∈ (E?))
BY
{ ((UnivCD THENA Auto)
   THEN (Assert E ⊆r E BY
               (BLemma `eo-forward-E-subtype` THEN Auto))
   THEN RepUR ``es-pred?`` 0
   THEN (BoolCase ⌈first(e1)⌉⋅ THENA Auto)
   THEN Fold `es-eq-E` 0) }

1
1. Info : Type
2. eo : EO+(Info)
3. e : E
4. e1 : E@i
5. E ⊆r E
6. ↑first(e1)
⊢ (inr ⋅ ) = if e1 = e then inr ⋅  if first(e1) then inr ⋅  else inl pred(e1) fi  ∈ (E?)

2
1. Info : Type
2. eo : EO+(Info)
3. e : E
4. e1 : E@i
5. ¬↑first(e1)
6. E ⊆r E
⊢ (inl pred(e1)) = if e1 = e then inr ⋅  if first(e1) then inr ⋅  else inl pred(e1) fi  ∈ (E?)

---

Latex:


\mforall{}[Info:Type].  \mforall{}[eo:EO+(Info)].  \mforall{}[e:E].
    \mforall{}e1:E.  (es-pred?(eo.e;e1)  =  if  es-eq(eo)  e1  e  then  inr  \mcdot{}    else  es-pred?(eo;e1)  fi  )


By

((UnivCD  THENA  Auto)
  THEN  (Assert  E  \msubseteq{}r  E  BY
                          (BLemma  `eo-forward-E-subtype`  THEN  Auto))
  THEN  RepUR  ``es-pred?``  0
  THEN  (BoolCase  \mkleeneopen{}first(e1)\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  Fold  `es-eq-E`  0)

---

Home Index