Step
*
of Lemma
has-value-l-last
∀[l:Base]. l ∈ Top × Top supposing (l-last(l))↓
BY
{ (Auto
THEN RepUR ``l-last l-last-default list_ind`` (-1)
THEN RW UnrollLoopsC (-1)
THEN Reduce (-1)
THEN RepeatFor 2 (HasValueD (-1))
THEN HVimplies2 (-2) [1]
THEN HVimplies2 (-3) [1]
THEN BotDiv) }
Latex:
Latex:
\mforall{}[l:Base]. l \mmember{} Top \mtimes{} Top supposing (l-last(l))\mdownarrow{}
By
Latex:
(Auto
THEN RepUR ``l-last l-last-default list\_ind`` (-1)
THEN RW UnrollLoopsC (-1)
THEN Reduce (-1)
THEN RepeatFor 2 (HasValueD (-1))
THEN HVimplies2 (-2) [1]
THEN HVimplies2 (-3) [1]
THEN BotDiv)
Home
Index