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