---

Step * of Lemma last_member

∀[T:Type]. ∀L:T List. (last(L) ∈ L) supposing ¬↑null(L)
BY
{ (Unfolds ``l_member last`` 0
   THEN Auto
   THEN (Assert ||L|| > 0⋅
         THENL [(((RW assert_pushdownC (-1)) THENA Auto) THEN DVar `L' THEN All Reduce THEN Auto' THEN D -1 THEN Auto)
               ; (InstConcl [||L|| - 1]⋅ THEN Auto)]
   )) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}L:T  List.  (last(L)  \mmember{}  L)  supposing  \mneg{}\muparrow{}null(L)


By

---

Latex:
(Unfolds  ``l\_member  last``  0
  THEN  Auto
  THEN  (Assert  ||L||  >  0\mcdot{}
              THENL  [(((RW  assert\_pushdownC  (-1))  THENA  Auto)
                              THEN  DVar  `L'
                              THEN  All  Reduce
                              THEN  Auto'
                              THEN  D  -1
                              THEN  Auto)
                          ;  (InstConcl  [||L||  -  1]\mcdot{}  THEN  Auto)]
  ))

---

Home Index