• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
      • Std/lists
        • Std/lists/abstract
          • Element-list-p
          • Element-list-equiv
          • Element-list-nonempty-p
          • Elementlist-projection
          • Element-equiv
          • Generic-eval-requirement
          • Element-list-fix
          • Elementlist-mapappend
          • Element-fix
          • Outelement-list-p
          • Outelement-p
          • Element-xformer
            • Element-listxformer
            • Element-p
            • Def-listp-rule
            • Def-projection-rule
            • Def-nonempty-listp-rule
            • Def-mapappend-rule
            • Def-listfix-rule
          • Rev
          • Defsort
          • List-fix
          • Std/lists/nth
          • Hons-remove-duplicates
          • Std/lists/update-nth
          • Set-equiv
          • Duplicity
          • Prefixp
          • Std/lists/take
          • Std/lists/intersection$
          • Nats-equiv
          • Repeat
          • Index-of
          • All-equalp
          • Sublistp
          • Std/lists/nthcdr
          • Listpos
          • List-equiv
          • Final-cdr
          • Std/lists/append
          • Std/lists/remove
          • Subseq-list
          • Rcons
          • Std/lists/revappend
          • Std/lists/remove-duplicates-equal
          • Std/lists/reverse
          • Std/lists/last
          • Std/lists/resize-list
          • Flatten
          • Suffixp
          • Std/lists/butlast
          • Std/lists/set-difference
          • 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
          • Std/lists/add-to-set
          • Append-without-guard
          • Std/lists/subsetp
          • Std/lists/member
        • Std/alists
        • Obags
        • Std/util
        • Std/strings
        • Std/io
        • Std/osets
        • Std/basic
        • Std/system
        • Std/typed-lists
        • Std/bitsets
        • Std/testing
        • Std/typed-alists
        • Std/stobjs
      • Proof-automation
      • Macro-libraries
      • ACL2
      • Interfacing-tools
      • Hardware-verification
      • Software-verification
      • Math
      • Testing-utilities
    • Std/lists/abstract

    Element-xformer

    Generic transform to be projected over a typed list.

    Definitions and Theorems

    Theorem: outelement-p-of-element-xformer

    (defthm outelement-p-of-element-xformer
  (implies (element-p x)
           (outelement-p (element-xformer x))))