• Top
  • Documentation
  • Books
  • Boolean-reasoning
    • Ipasir
    • Aignet
    • Aig
    • Satlink
      • Sat-solver-options
        • Unsat-checking
        • Check-config
          • Pigeon-hole
            • No-two-in-hole-aux
            • No-others-in-hole
            • Not-both-in-hole
            • No-two-in-any-hole
            • Every-bird-in-hole
            • No-two-in-hole
            • Bird-in-some-hole
            • Bird-in-hole
          • Simple-sat
          • Assert-unsat
          • Assert-sat
      • Config-p
      • Logical-story
      • Dimacs
      • Gather-benchmarks
      • Cnf
      • Satlink-extra-hook
      • Sat
    • Truth
    • Ubdds
    • Bdd
    • Faig
    • Bed
    • 4v
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Pigeon-hole

No-two-in-hole-aux

Signature

(no-two-in-hole-aux tweety max-birds hole) → clauses

Arguments

tweety — Counts down from max birds.
    Guard (natp tweety).

max-birds — Fixed.
    Guard (natp max-birds).

hole — Fixed.
    Guard (natp hole).

Returns

clauses — No two birds share this one hole.
    Type (lit-list-listp clauses).

Definitions and Theorems

Function: no-two-in-hole-aux

(defun no-two-in-hole-aux (tweety max-birds hole)
  (declare (xargs :guard (and (natp tweety)
                              (natp max-birds)
                              (natp hole))))
  (let ((__function__ 'no-two-in-hole-aux))
    (declare (ignorable __function__))
    (b* (((when (zp tweety)) nil)
         (tweety (- tweety 1)))
      (append (no-others-in-hole tweety max-birds hole)
              (no-two-in-hole-aux tweety max-birds hole)))))

Theorem: lit-list-listp-of-no-two-in-hole-aux

(defthm lit-list-listp-of-no-two-in-hole-aux
  (b* ((clauses (no-two-in-hole-aux tweety max-birds hole)))
    (lit-list-listp clauses))
  :rule-classes :rewrite)