• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
    • Theories
    • Rule-classes
    • Proof-builder
      • Instructions
      • Proof-builder-commands
        • ACL2-pc::rewrite
        • ACL2-pc::apply-linear
        • ACL2-pc::sequence
        • Proof-builder-commands-short-list
        • ACL2-pc::=
        • ACL2-pc::s
        • ACL2-pc::exit
        • ACL2-pc::type-alist
        • ACL2-pc::in-theory
        • ACL2-pc::equiv
        • ACL2-pc::comm
        • ACL2-pc::casesplit
        • ACL2-pc::add-abbreviation
        • ACL2-pc::dv
        • ACL2-pc::hyps
        • ACL2-pc::prove-termination
        • ACL2-pc::prove-guard
        • ACL2-pc::x
        • ACL2-pc::pot-lst
        • ACL2-pc::fancy-use
        • ACL2-pc::dive
        • ACL2-pc::generalize
        • ACL2-pc::lisp
        • ACL2-pc::show-rewrites
        • ACL2-pc::claim
        • ACL2-pc::put
        • ACL2-pc::split
        • ACL2-pc::geneqv
        • ACL2-pc::prove
        • ACL2-pc::help
        • ACL2-pc::save
        • ACL2-pc::do-all
        • ACL2-pc::demote
        • ACL2-pc::wrap1
        • ACL2-pc::show-abbreviations
        • ACL2-pc::promote
        • ACL2-pc::retrieve
        • ACL2-pc::reduce
        • ACL2-pc::forwardchain
        • ACL2-pc::doc
        • ACL2-pc::bash
        • ACL2-pc::p-top
        • ACL2-pc::print
        • ACL2-pc::expand
        • ACL2-pc::bk
        • ACL2-pc::wrap
        • ACL2-pc::remove-abbreviations
        • ACL2-pc::reduce-by-induction
        • ACL2-pc::induct
        • ACL2-pc::unsave
        • ACL2-pc::undo
        • ACL2-pc::top
        • ACL2-pc::restore
        • ACL2-pc::replay
        • ACL2-pc::psog
        • ACL2-pc::p
        • ACL2-pc::nx
        • ACL2-pc::noise
        • ACL2-pc::contrapose
        • ACL2-pc::wrap-induct
        • ACL2-pc::pso!
        • ACL2-pc::pso
        • ACL2-pc::up
        • ACL2-pc::then
        • ACL2-pc::th
        • ACL2-pc::sl
        • ACL2-pc::show-type-prescriptions
        • ACL2-pc::bdd
        • ACL2-pc::repeat
        • ACL2-pc::pr
        • ACL2-pc::pl
        • ACL2-pc::finish
        • ACL2-pc::commands
        • ACL2-pc::change-goal
        • ACL2-pc::use
        • ACL2-pc::show-linears
        • ACL2-pc::s-prop
        • ACL2-pc::runes
        • ACL2-pc::protect
        • ACL2-pc::instantiate
        • ACL2-pc::insist-all-proved
        • ACL2-pc::fail
        • ACL2-pc::clause-processor
        • ACL2-pc::bookmark
        • ACL2-pc::retain
        • ACL2-pc::quiet!
        • ACL2-pc::pro
        • ACL2-pc::orelse
        • ACL2-pc::goals
        • ACL2-pc::drop
        • ACL2-pc::do-strict
        • ACL2-pc::print-all-concs
        • ACL2-pc::do-all-no-prompt
        • ACL2-pc::x-dumb
        • ACL2-pc::succeed
        • ACL2-pc::print-all-goals
        • ACL2-pc::pp
        • ACL2-pc::noise!
        • ACL2-pc::nil
        • ACL2-pc::negate
        • ACL2-pc::illegal
        • ACL2-pc::elim
        • ACL2-pc::sls
        • ACL2-pc::quiet
        • ACL2-pc::claim-simple
        • ACL2-pc::cg
        • ACL2-pc::pro-or-skip
        • ACL2-pc::ex
        • ACL2-pc::comment
        • ACL2-pc::ACL2-wrap
        • ACL2-pc::when-not-proved
        • ACL2-pc::skip
        • ACL2-pc::retain-or-skip
        • ACL2-pc::repeat-until-done
        • ACL2-pc::free
        • ACL2-pc::drop-or-skip
        • ACL2-pc::cg-or-skip
        • ACL2-pc::by
        • ACL2-pc::split-in-theory
        • ACL2-pc::st
        • ACL2-pc::sr
        • ACL2-pc::print-main
        • ACL2-pc::lemmas-used
        • ACL2-pc::cl-proc
        • ACL2-pc::al
        • ACL2-pc::run-instr-on-new-goals
        • ACL2-pc::run-instr-on-goal
        • ACL2-pc::repeat-rec
        • ACL2-pc::r
        • ACL2-pc::contradict
      • Proof-builder-commands-short-list
      • Dive-into-macros-table
      • Verify
      • Define-pc-macro
      • Macro-command
      • Define-pc-help
      • Toggle-pc-macro
      • Define-pc-meta
      • Retrieve
      • Unsave
      • Proof-checker
    • Recursion-and-induction
    • Hons-and-memoization
    • Events
    • Parallelism
    • History
    • Programming
    • Operational-semantics
    • Real
    • Start-here
    • Debugging
    • Miscellaneous
    • Output-controls
    • Macros
    • Interfacing-tools
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Proof-builder-commands

ACL2-pc::sl

(atomic macro) simplify with lemmas

Examples:
sl
(sl 3)

General Form:
(sl &optional backchain-limit)

Simplify, but with all function definitions disabled (see function-theory in the top-level ACL2 loop), except for a few basic functions (the ones in (theory 'minimal-theory)). The backchain-limit has a default of 0, but if it is supplied and not nil, then it should be a nonnegative integer; see ACL2-pc::s.

WARNING: This command completely ignores in-theory commands that are executed inside the interactive proof-builder.