• Top
    • Documentation
    • Books
    • Recursion-and-induction
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
      • Std/lists
        • Std/lists/abstract
        • Rev
        • Defsort
        • List-fix
        • Std/lists/nth
        • Hons-remove-duplicates
        • Std/lists/update-nth
        • Set-equiv
        • Duplicity
        • Prefixp
        • Std/lists/take
          • Take-of-take-split
            • Take-of-too-many
          • Std/lists/intersection$
          • Nats-equiv
          • Repeat
          • Index-of
          • All-equalp
          • Sublistp
          • Std/lists/nthcdr
          • Std/lists/append
          • Listpos
          • List-equiv
          • Final-cdr
          • Std/lists/remove
          • Subseq-list
          • Rcons
          • Std/lists/revappend
          • Std/lists/remove-duplicates-equal
          • Std/lists/last
          • Std/lists/reverse
          • Std/lists/resize-list
          • Flatten
          • Suffixp
          • Std/lists/set-difference
          • Std/lists/butlast
          • Std/lists/len
          • Std/lists/intersectp
          • Std/lists/true-listp
          • Intersectp-witness
          • Subsetp-witness
          • Std/lists/remove1-equal
          • Rest-n
          • First-n
          • Std/lists/union
          • Append-without-guard
          • Std/lists/subsetp
          • Std/lists/member
        • Std/alists
        • Obags
        • Std/util
        • Std/strings
        • Std/io
        • Std/osets
        • Std/system
        • Std/basic
        • Std/typed-lists
        • Std/bitsets
        • Std/testing
        • Std/typed-alists
        • Std/stobjs
        • Std-extensions
      • Proof-automation
      • Macro-libraries
      • ACL2
      • Interfacing-tools
      • Hardware-verification
      • Software-verification
      • Testing-utilities
      • Math
    • Std/lists/take

    Take-of-take-split

    Aggressive case splitting rule to reduce (take a (take b x)).

    Theorem: take-of-take-split

    (defthm take-of-take-split
            (equal (take a (take b x))
                   (if (<= (nfix a) (nfix b))
                       (take a x)
                       (append (take b x)
                               (repeat (- (nfix a) (nfix b)) nil)))))

    This rule may sometimes cause too much case splitting. If you disable it, nests of take can still be reduced when ACL2 can determine the relationship between a and b, using the following related rules:

    Theorem: take-of-take-same

    (defthm take-of-take-same
            (equal (take a (take a x)) (take a x)))

    Theorem: take-more-of-take-fewer

    (defthm
         take-more-of-take-fewer
         (implies (< (nfix b) (nfix a))
                  (equal (take a (take b x))
                         (append (take b x)
                                 (repeat (- (nfix a) (nfix b)) nil)))))

    Theorem: take-fewer-of-take-more

    (defthm take-fewer-of-take-more
            (implies (<= (nfix a) (nfix b))
                     (equal (take a (take b x)) (take a x))))