• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
    • Apt
    • Acre
    • Milawa
    • Smtlink
    • Aleobft
    • Abnf
    • Vwsim
    • Isar
    • Wp-gen
    • Dimacs-reader
    • Pfcs
      • Proof-support
      • Abstract-syntax
      • R1cs-subset
      • Semantics
      • Abstract-syntax-operations
      • Indexed-names
      • Well-formedness
        • Definition-list-wfp
        • Definition-wfp
        • Constraint-wfp
        • Constraint-list-wfp
        • System-wfp
      • Concrete-syntax
      • R1cs-bridge
      • Parser-interface
    • Legacy-defrstobj
    • Proof-checker-array
    • Soft
    • Farray
    • Rp-rewriter
    • Instant-runoff-voting
    • Imp-language
    • Sidekick
    • Leftist-trees
    • C
    • Java
    • Taspi
    • Bitcoin
    • Des
    • Ethereum
    • X86isa
    • Sha-2
    • Yul
    • Riscv
    • Zcash
    • Proof-checker-itp13
    • Regex
    • ACL2-programming-language
    • Json
    • Jfkr
    • Equational
    • Cryptography
    • Poseidon
    • Where-do-i-place-my-book
    • Bigmems
    • Builtins
    • Axe
    • Execloader
    • Solidity
    • Leo
    • Paco
    • Concurrent-programs
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Well-formedness

Constraint-list-wfp

Check if a list of constraints is well-formed, with respect to a list of relation definitions.

Signature

(constraint-list-wfp constrs defs) → yes/no

Arguments

constrs — Guard (constraint-listp constrs).

defs — Guard (definition-listp defs).

Returns

yes/no — Type (booleanp yes/no).

A list of constraints is well-formed iff all the constraints are well-formed.

Definitions and Theorems

Function: constraint-list-wfp

(defun constraint-list-wfp (constrs defs)
  (declare (xargs :guard (and (constraint-listp constrs)
                              (definition-listp defs))))
  (let ((__function__ 'constraint-list-wfp))
    (declare (ignorable __function__))
    (or (endp constrs)
        (and (constraint-wfp (car constrs) defs)
             (constraint-list-wfp (cdr constrs)
                                  defs)))))

Theorem: booleanp-of-constraint-list-wfp

(defthm booleanp-of-constraint-list-wfp
  (b* ((yes/no (constraint-list-wfp constrs defs)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: constraint-list-wfp-of-constraint-list-fix-constrs

(defthm constraint-list-wfp-of-constraint-list-fix-constrs
  (equal (constraint-list-wfp (constraint-list-fix constrs)
                              defs)
         (constraint-list-wfp constrs defs)))

Theorem: constraint-list-wfp-constraint-list-equiv-congruence-on-constrs

(defthm
    constraint-list-wfp-constraint-list-equiv-congruence-on-constrs
  (implies (constraint-list-equiv constrs constrs-equiv)
           (equal (constraint-list-wfp constrs defs)
                  (constraint-list-wfp constrs-equiv defs)))
  :rule-classes :congruence)

Theorem: constraint-list-wfp-of-definition-list-fix-defs

(defthm constraint-list-wfp-of-definition-list-fix-defs
  (equal (constraint-list-wfp constrs (definition-list-fix defs))
         (constraint-list-wfp constrs defs)))

Theorem: constraint-list-wfp-definition-list-equiv-congruence-on-defs

(defthm constraint-list-wfp-definition-list-equiv-congruence-on-defs
  (implies (definition-list-equiv defs defs-equiv)
           (equal (constraint-list-wfp constrs defs)
                  (constraint-list-wfp constrs defs-equiv)))
  :rule-classes :congruence)