• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Community
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
    • Kestrel-books
      • Crypto-hdwallet
      • Apt
      • Error-checking
      • Fty-extensions
      • Isar
      • Kestrel-utilities
      • Set
      • C
        • Syntax-for-tools
          • Formalized-subset
          • Mapping-to-language-definition
          • Input-files
          • Compilation-database
          • Printer
          • Output-files
          • Abstract-syntax-operations
          • Implementation-environments
          • Abstract-syntax
          • Concrete-syntax
          • Disambiguation
            • Disambiguator
            • Unambiguity
              • Abstract-syntax-unambp
                • Exprs/decls/stmts-unambp
                • Filepath-transunit-map-unambp
                • Transunit-ensemble-unambp
                • Declor/absdeclor-unambp
                • Type-spec-list-unambp
                • Ext-declon-list-unambp
                • Fundef-option-unambp
                • Ext-declon-unambp
                • Expr/tyname-unambp
                • Declon/stmt-unambp
                • Code-ensemble-unambp
                • Fundef-unambp
                • Transunit-unambp
                • Typequal/attribspec-list-unambp
                • Typequal/attribspec-list-list-unambp
                • Typequal/attribspec-unambp
                • Struni-spec-unambp
                • Struct-declor-unambp
                • Struct-declor-list-unambp
                • Struct-declon-unambp
                • Struct-declon-list-unambp
                • Statassert-unambp
                • Spec/qual-unambp
                • Spec/qual-list-unambp
                • Param-declor-unambp
                • Param-declon-unambp
                • Param-declon-list-unambp
                • Member-designor-unambp
                • Initer-option-unambp
                • Init-declor-unambp
                • Init-declor-list-unambp
                • Genassoc-list-unambp
                • Expr-option-unambp
                • Enumer-list-unambp
                • Dirabsdeclor-unambp
                • Dirabsdeclor-option-unambp
                • Desiniter-list-unambp
                • Designor-list-unambp
                • Declor-option-unambp
                • Declon-list-unambp
                • Decl-spec-list-unambp
                • Const-expr-unambp
                • Const-expr-option-unambp
                • Block-item-unambp
                • Block-item-list-unambp
                • Attrib-spec-unambp
                • Attrib-spec-list-unambp
                • Attrib-list-unambp
                • Asm-output-unambp
                • Asm-output-list-unambp
                • Asm-input-list-unambp
                • Amb-expr/tyname-unambp
                • Amb-declor/absdeclor-unambp
                • Amb-declon/stmt-unambp
                • Align-spec-unambp
                • Absdeclor-option-unambp
                • Type-spec-unambp
                • Tyname-unambp
                • Stmt-unambp
                • Label-unambp
                • Initer-unambp
                • Genassoc-unambp
                • Expr-unambp
                • Expr-list-unambp
                • Enumer-unambp
                • Enum-spec-unambp
                • Dirdeclor-unambp
                • Desiniter-unambp
                • Designor-unambp
                • Declor-unambp
                • Declon-unambp
                • Decl-spec-unambp
                • Comp-stmt-unambp
                • Attrib-unambp
                • Asm-stmt-unambp
                • Asm-input-unambp
                • Absdeclor-unambp
              • Abstract-syntax-unambp-additional-theorems
              • Type-spec-list-unambp-of-sublists
              • Expr-unambp-of-operation-on-expr-unambp
          • Validation
          • Gcc-builtins
          • Preprocessing
          • Parsing
        • Atc
        • Transformation-tools
        • Language
        • Representation
        • Insertion-sort
        • Pack
      • Soft
      • Bv
      • Imp-language
      • Ethereum
      • Event-macros
      • Java
      • Riscv
      • Bitcoin
      • Zcash
      • Yul
      • ACL2-programming-language
      • Prime-fields
      • Json
      • Syntheto
      • File-io-light
      • Cryptography
      • Number-theory
      • Axe
      • Lists-light
      • Builtins
      • Solidity
      • Helpers
      • Htclient
      • Typed-lists-light
      • Arithmetic-light
    • X86isa
    • Axe
    • Execloader
  • Math
  • Testing-utilities

• Abstract-syntax-unambp

Ext-declon-list-unambp

Signature

(ext-declon-list-unambp ext-declon-list) → fty::result

Arguments

ext-declon-list — Guard (ext-declon-listp ext-declon-list).

Returns

fty::result — Type (booleanp fty::result).

Definitions and Theorems

Function: ext-declon-list-unambp

(defun ext-declon-list-unambp (ext-declon-list)
 (declare (xargs :guard (ext-declon-listp ext-declon-list)))
 (let ((__function__ 'ext-declon-list-unambp))
   (declare (ignorable __function__))
   (cond ((endp ext-declon-list) t)
         (t (and (ext-declon-unambp (car ext-declon-list))
                 (ext-declon-list-unambp (cdr ext-declon-list)))))))

Theorem: booleanp-of-ext-declon-list-unambp

(defthm booleanp-of-ext-declon-list-unambp
  (b* ((fty::result (ext-declon-list-unambp ext-declon-list)))
    (booleanp fty::result))
  :rule-classes :rewrite)

Theorem: ext-declon-list-unambp-of-ext-declon-list-fix-ext-declon-list

(defthm
      ext-declon-list-unambp-of-ext-declon-list-fix-ext-declon-list
 (equal
      (ext-declon-list-unambp (ext-declon-list-fix ext-declon-list))
      (ext-declon-list-unambp ext-declon-list)))

Theorem: ext-declon-list-unambp-ext-declon-list-equiv-congruence-on-ext-declon-list

(defthm
 ext-declon-list-unambp-ext-declon-list-equiv-congruence-on-ext-declon-list
 (implies
      (ext-declon-list-equiv ext-declon-list ext-declon-list-equiv)
      (equal (ext-declon-list-unambp ext-declon-list)
             (ext-declon-list-unambp ext-declon-list-equiv)))
 :rule-classes :congruence)