Step * of Lemma last_append2

[A,B:Top List].  last(A B) last(B) supposing 0 < ||B||
BY
(((InductionOnList THEN Reduce THEN UnivCD) THENA Auto) THEN Try (Trivial)) }

1
1. Top
2. Top List
3. ∀[B:Top List]. last(v B) last(B) supposing 0 < ||B||
4. Top List
5. 0 < ||B||
⊢ last([u (v B)]) last(B)


Latex:


Latex:
\mforall{}[A,B:Top  List].    last(A  @  B)  \msim{}  last(B)  supposing  0  <  ||B||


By


Latex:
(((InductionOnList  THEN  Reduce  0  THEN  UnivCD)  THENA  Auto)  THEN  Try  (Trivial))




Home Index