• Top
    • Documentation
    • Books
    • Boolean-reasoning
      • Ipasir
      • Aignet
      • Aig
      • Satlink
        • Sat-solver-options
        • Config-p
        • Logical-story
        • Dimacs
        • Gather-benchmarks
        • Cnf
          • Litp
          • Varp
            • Varp-reasoning
            • Env$
            • Eval-formula
            • Max-index-formula
            • Max-index-clause
            • Formula-indices
            • Clause-indices
          • 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
    • Varp

    Varp-reasoning

    Basic rules for reasoning about identifiers.