Step * 1 of Lemma l-last-is-last


1. Base
2. ∀l:Top List. (l-last(l) last(l))
3. is-exception(l-last(l))
⊢ l-last(l) ≤ last(l)
BY
(ExceptionSqequal (-1)
   THEN HypSubst' (-1) 0
   THEN (Assert exception(u; v) ≤ l-last(l) BY
               (HypSubst' (-1) THEN Auto))
   THEN Lemmaize [-1]
   THEN (UnivCD THENA Auto)) }

1
1. Base@i
2. Base@i
3. Base@i
4. exception(u; v) ≤ l-last(l)
⊢ exception(u; v) ≤ last(l)


Latex:


Latex:

1.  l  :  Base
2.  \mforall{}l:Top  List.  (l-last(l)  \msim{}  last(l))
3.  is-exception(l-last(l))
\mvdash{}  l-last(l)  \mleq{}  last(l)


By


Latex:
(ExceptionSqequal  (-1)
  THEN  HypSubst'  (-1)  0
  THEN  (Assert  exception(u;  v)  \mleq{}  l-last(l)  BY
                          (HypSubst'  (-1)  0  THEN  Auto))
  THEN  Lemmaize  [-1]
  THEN  (UnivCD  THENA  Auto))




Home Index