• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Community
    • Proof-automation
    • ACL2
    • Macro-libraries
    • Interfacing-tools
    • Hardware-verification
      • Gl
      • Esim
      • Vl2014
      • Sv
        • Svex-stvs
          • Svtv-data
          • Defsvtv$
          • Svtv-run
          • Defsvtv-phasewise
          • Svtv
          • Svtv-spec
          • Defsvtv
          • Process.lisp
          • Svtv-doc
            • Svtv-to-xml
            • Stv-entry-to-xml
            • Stv-line-to-xml
            • Stv-entries-to-xml
            • Stv-lines-to-xml
            • 4vec-to-bitwise-chars
            • Stv-repeat-last-entry
            • Stv-repeat-last-entries
              • 4vec-to-hex-chars
              • 4vec-to-hex-char
              • Stv-name-to-xml
              • Stv-labels-to-xml
              • 4vec-to-xml-chars
            • Svtv-chase$
            • Svtv-versus-stv
            • Svtv-debug-fsm
            • Structure.lisp
            • Svtv-debug
            • Def-pipeline-thm
            • Expand.lisp
            • Def-cycle-thm
            • Svtv-utilities
            • Svtv-debug$
            • Defsvtv$-phasewise
          • Svex-decomposition-methodology
          • Sv-versus-esim
          • Svex-decomp
          • Svex-compose-dfs
          • Svex-compilation
          • Moddb
          • Svmods
          • Svstmt
          • Sv-tutorial
          • Expressions
          • Symbolic-test-vector
          • Vl-to-svex
        • Fgl
        • Vwsim
        • Vl
        • X86isa
        • Svl
        • Rtl
      • Software-verification
      • Math
      • Testing-utilities
    • Svtv-doc

    Stv-repeat-last-entries

    Signature
    (stv-repeat-last-entries lines nphases) → new-lines
    Arguments
    lines — Guard (true-list-listp lines).
    nphases — Guard (natp nphases).
    Returns
    new-lines — Type (true-list-listp new-lines).

    Definitions and Theorems

    Function: stv-repeat-last-entries

    (defun stv-repeat-last-entries (lines nphases)
      (declare (xargs :guard (and (true-list-listp lines)
                                  (natp nphases))))
      (let ((__function__ 'stv-repeat-last-entries))
        (declare (ignorable __function__))
        (if (atom lines)
            nil
          (cons (stv-repeat-last-entry (car lines)
                                       nphases)
                (stv-repeat-last-entries (cdr lines)
                                         nphases)))))

    Theorem: true-list-listp-of-stv-repeat-last-entries

    (defthm true-list-listp-of-stv-repeat-last-entries
      (b* ((new-lines (stv-repeat-last-entries lines nphases)))
        (true-list-listp new-lines))
      :rule-classes :rewrite)