← Back to branch summary

~ubuntu-branches/ubuntu/wily/acl2/wily

« back to all changes in this revision

Viewing changes to books/unicode/partition.lisp

  • Committer: Package Import Robot
  • Author(s): Camm Maguire
  • Date: 2015-01-16 10:35:45 UTC
  • mfrom: (3.3.26 sid)
  • Revision ID: package-import@ubuntu.com-20150116103545-prehe9thgo79o8w8
Tags: 7.0-1
New upstream release

Show diffs side-by-side

added added

removed removed

Lines of Context:
books/unicode/partition.lisp
74
74
                         0))
75
75
         :hints(("Goal" :induct (len x)))))
76
76
 
77
 
(local (defthm equal-of-take-and-list-fix
78
 
         (equal (equal (take n x) (list-fix x))
79
 
                (equal (nfix n) (len x)))
80
 
         :hints(("Goal" :in-theory (enable take-redefinition)))))
81
 
 
82
77
(local (defthm reassemble-lemma
83
78
         (implies (<= (nfix n) (len x))
84
79
                  (equal (append (take n x)