Theorem a

• Type: A user defined theorem
• Validity: The proof is valid.
• Features: simp, localsimp,
• Comment:
• Used by: Noassoc, app, app-02, app-02-ant, app-03, app-04, app-05, app-06, app-07, app-08, app-09, append-size-less, c-01, c-02, c-05, c-09, constrrew, e-02, e-03, e-04, elim-first, eq, eq-01, eq-02, eq-03, eq-04, eq-05, first-01, first-02, first-app, firsteq, firsteq-01, firstoc, firstoc-rew, firstrest, if-in, in, in-01, in-06, in-07, in-08, in-09, in-10, in-11, in-12, in-13, in-14, in-15, in-16, in-17, in-append, in-append0-not-left, in-empty, in-last-rest, in-rec, inapp, inapp-01, inapp-02, inapp-03, inapp-04, inapp-05, inapp-06, inapp-07, inapp-08, inapp-09, inapp-10, inapp-11, inapp-12, inapp-13, inapp-14, inex, inex-01, inex-02, inex-03, ins, ins-01, isin, isin-01, k-Last-base, k-Last-rec, k-Two, last, last-01, lastdiv, lastdiv-rew, lastoc, lastoc-rew, lasttwo, len, len-01, len-03, len-04, len-06, len-last-rest, longest-common-prefix, neq, neq-01, neq-02, neq-03, neq-04, neq-05, neq-06, neq-07, neq-09, ni, one, one-01, onein, rest-01, rewlem, some-element, split-first, split-rest, two, unequal,
• Used by units in proved state: list-last, list-del, stream, string-less-new, stut-mon, path-reachable, olist-sort, olist-min-max, olist, mon-lim-filter-count, list-set, list-perm, streamseq-mon-lim, inf-app-list, infinite-append, assoclist, list-dup, list-setequal, list,
• Proof exists?: Yes

View the proof

Infos about the proof

• Proved?: Yes
• Interactions: 0
• Proof steps: 3
• Used lemmas: Cons, app-01, Nil,
• Used spec theorems:
  • Used simplifier rules:
    • list-data/f