---

Step * of Lemma ranked-eo-pred

∀[L,rk:Top]. ∀[e:Top × Top].  (pred(e) ~ if snd(e)=0  then e  else <fst(e), (snd(e)) - 1>)
BY
{ (Auto
   THEN D -1
   THEN Reduce 0
   THEN RecUnfold `es-pred` 0
   THEN RepUR ``es-base-pred ranked-eo mk-extended-eo mk-eo mk-eo-record es-dom let`` 0
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[L,rk:Top].  \mforall{}[e:Top  \mtimes{}  Top].    (pred(e)  \msim{}  if  snd(e)=0    then  e    else  <fst(e),  (snd(e))  -  1>)


By

---

Latex:
(Auto
  THEN  D  -1
  THEN  Reduce  0
  THEN  RecUnfold  `es-pred`  0
  THEN  RepUR  ``es-base-pred  ranked-eo  mk-extended-eo  mk-eo  mk-eo-record  es-dom  let``  0
  THEN  Auto)

---

Home Index