• Top
    • Documentation
    • Books
    • Recursion-and-induction
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
      • Gl
      • Esim
      • Vl2014
      • Sv
      • Vwsim
      • Fgl
      • Vl
        • Syntax
        • Loader
        • Warnings
        • Getting-started
        • Utilities
          • Name-database
          • Vl-gc
          • Symbol-list-names
          • Ints-from
          • Nats-from
          • Make-lookup-alist
          • Redundant-mergesort
          • Longest-common-prefix
          • Vl-remove-keys
          • Vl-plural-p
          • Vl-merge-contiguous-indices
          • Sum-nats
          • Vl-edition-p
          • Vl-maybe-integer-listp
          • Fast-memberp
          • Nat-listp
          • Max-nats
          • Longest-common-prefix-list
            • Character-list-listp
            • Vl-character-list-list-values-p
            • Remove-from-alist
            • Prefix-of-eachp
            • Vl-string-keys-p
            • Vl-maybe-nat-listp
            • Vl-string-list-values-p
            • String-list-listp
            • Vl-string-values-p
            • Explode-list
            • True-list-listp
            • Symbol-list-listp
            • All-have-len
            • Pos-listp
            • Min-nats
            • Debuggable-and
            • Vl-starname
            • Remove-equal-without-guard
            • String-fix
            • Anyp
            • Vl-maybe-string-list
            • Longer-than-p
            • Fast-alist-free-each-alist-val
            • Not*
            • Free-list-of-fast-alists
            • *nls*
          • Printer
          • Kit
          • Mlib
          • Transforms
        • X86isa
        • Svl
        • Rtl
      • Software-verification
      • Testing-utilities
      • Math
    • Utilities

    Longest-common-prefix-list

    (longest-common-prefix-list x) returns the longest list, p, such that p is a prefix of every list in x.

    Signature
    (longest-common-prefix-list x) → *

    See also longest-common-prefix.

    Definitions and Theorems

    Function: longest-common-prefix-list

    (defun
     longest-common-prefix-list (x)
     (declare (xargs :guard t))
     (let
      ((__function__ 'longest-common-prefix-list))
      (declare (ignorable __function__))
      (cond
       ((atom x) nil)
       ((atom (cdr x)) (list-fix (car x)))
       (t
        (longest-common-prefix (first x)
                               (longest-common-prefix-list (cdr x)))))))

    Theorem: true-listp-of-longest-common-prefix-list

    (defthm true-listp-of-longest-common-prefix-list
            (true-listp (longest-common-prefix-list x))
            :rule-classes :type-prescription)

    Theorem: string-listp-of-longest-common-prefix-list

    (defthm string-listp-of-longest-common-prefix-list
            (implies (string-list-listp x)
                     (string-listp (longest-common-prefix-list x))))

    Theorem: longest-common-prefix-list-of-list-fix

    (defthm longest-common-prefix-list-of-list-fix
            (equal (longest-common-prefix-list (list-fix x))
                   (longest-common-prefix-list x)))

    Theorem: prefix-of-eachp-of-longest-common-prefix-list

    (defthm prefix-of-eachp-of-longest-common-prefix-list
            (prefix-of-eachp (longest-common-prefix-list x)
                             x))