---

Step * of Lemma l-last-is-last

∀[l:Top]. (l-last(l) ~ last(l))
BY
{ TACTIC:(Auto
          THEN SqEqualBase
          THEN (Assert ∀l:Top List. (l-last(l) ~ last(l)) BY
                      (InductionOnList
                       THEN Try ((RWO "l-last-nil" 0 THENA Auto))
                       THEN Try ((RWO "l-last-cons" 0 THENA Auto))
                       THEN Try ((RWO "last_nil" 0 THENA Auto))
                       THEN Try ((RWO "last_cons2" 0 THENA Auto))
                       THEN Try (AutoSplit)
                       THEN Auto))
          THEN SqequalSqle
          THEN AssumeHasValue
          THEN Try (((FLemma `has-value-last-list` [-1] THENM RWO "2" 0) THEN Auto))
          THEN Try (((FLemma `has-value-l-last-list` [-1] THENM RWO "2" 0) THEN Auto))) }

1
1. l : Base
2. ∀l:Top List. (l-last(l) ~ last(l))
3. is-exception(l-last(l))
⊢ l-last(l) ≤ last(l)

2
1. l : Base
2. ∀l:Top List. (l-last(l) ~ last(l))
3. is-exception(last(l))
⊢ last(l) ≤ l-last(l)

---

Latex:

---

Latex:
\mforall{}[l:Top].  (l-last(l)  \msim{}  last(l))


By

---

Latex:
TACTIC:(Auto
                THEN  SqEqualBase
                THEN  (Assert  \mforall{}l:Top  List.  (l-last(l)  \msim{}  last(l))  BY
                                        (InductionOnList
                                          THEN  Try  ((RWO  "l-last-nil"  0  THENA  Auto))
                                          THEN  Try  ((RWO  "l-last-cons"  0  THENA  Auto))
                                          THEN  Try  ((RWO  "last\_nil"  0  THENA  Auto))
                                          THEN  Try  ((RWO  "last\_cons2"  0  THENA  Auto))
                                          THEN  Try  (AutoSplit)
                                          THEN  Auto))
                THEN  SqequalSqle
                THEN  AssumeHasValue
                THEN  Try  (((FLemma  `has-value-last-list`  [-1]  THENM  RWO  "2"  0)  THEN  Auto))
                THEN  Try  (((FLemma  `has-value-l-last-list`  [-1]  THENM  RWO  "2"  0)  THEN  Auto)))

---

Home Index