---

Step * of Lemma es-before-split-last

∀[es,e:Top].  (before(e) ~ if first(e) then [] else before(pred(e)) @ [pred(e)] fi )
BY
{ (Auto THEN RW (AddrC [1] RecUnfoldTopAbC) 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[es,e:Top].    (before(e)  \msim{}  if  first(e)  then  []  else  before(pred(e))  @  [pred(e)]  fi  )


By

---

Latex:
(Auto  THEN  RW  (AddrC  [1]  RecUnfoldTopAbC)  0  THEN  Auto)

---

Home Index