• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Community
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
    • Theories
    • Rule-classes
    • Proof-builder
    • Recursion-and-induction
    • Hons-and-memoization
    • Events
    • Parallelism
    • History
    • Programming
    • Operational-semantics
    • Real
    • Start-here
      • Gentle-introduction-to-ACL2-programming
      • ACL2-tutorial
        • Introduction-to-the-theorem-prover
          • Logic-knowledge-taken-for-granted
          • Logic-knowledge-taken-for-granted-inductive-proof
          • Introduction-to-rewrite-rules-part-1
          • Introduction-to-key-checkpoints
          • Introduction-to-rewrite-rules-part-2
          • Geneqv
          • Logic-knowledge-taken-for-granted-propositional-calculus
          • Refinement-failure
          • Introduction-to-a-few-system-considerations
          • Introduction-to-the-database
          • Programming-knowledge-taken-for-granted
          • Logic-knowledge-taken-for-granted-rewriting
          • Introductory-challenge-problem-4-answer
          • Introduction-to-programming-in-ACL2-for-those-who-know-lisp
          • Introduction-to-hints
          • Dealing-with-key-combinations-of-function-symbols
          • Architecture-of-the-prover
          • Further-information-on-rewriting
          • Frequently-asked-questions-by-newcomers
          • Specific-kinds-of-formulas-as-rewrite-rules
          • Strong-rewrite-rules
          • Practice-formulating-strong-rules-3
          • Practice-formulating-strong-rules-1
          • Practice-formulating-strong-rules-6
          • Generalizing-key-checkpoints
          • Logic-knowledge-taken-for-granted-q1-answer
          • Example-inductions
          • Logic-knowledge-taken-for-granted-q2-answer
          • Logic-knowledge-taken-for-granted-rewriting-repeatedly
          • Introductory-challenge-problem-4
          • Equivalent-formulas-different-rewrite-rules
          • Post-induction-key-checkpoints
          • Special-cases-for-rewrite-rules
          • Example-induction-scheme-with-accumulators
          • Practice-formulating-strong-rules-5
          • Practice-formulating-strong-rules
          • Practice-formulating-strong-rules-2
          • Introductory-challenges
          • Logic-knowledge-taken-for-granted-equals-for-equals
          • Logic-knowledge-taken-for-granted-evaluation
          • Example-induction-scheme-nat-recursion
          • Example-induction-scheme-down-by-2
          • Logic-knowledge-taken-for-granted-instance
          • Introductory-challenge-problem-3-answer
          • Example-induction-scheme-on-lists
          • Example-induction-scheme-upwards
          • Example-induction-scheme-with-multiple-induction-steps
          • Practice-formulating-strong-rules-4
          • Logic-knowledge-taken-for-granted-q3-answer
          • Example-induction-scheme-binary-trees
          • Introductory-challenge-problem-3
          • Introductory-challenge-problem-1
          • Logic-knowledge-taken-for-granted-base-case
          • Introductory-challenge-problem-1-answer
          • Example-induction-scheme-on-several-variables
          • Introductory-challenge-problem-2-answer
          • Introductory-challenge-problem-2
        • Pages Written Especially for the Tours
        • The-method
        • Advanced-features
        • Interesting-applications
        • Tips
        • Alternative-introduction
        • Tidbits
        • Annotated-ACL2-scripts
        • Startup
        • ACL2-as-standalone-program
        • ACL2-sedan
        • Talks
        • Nqthm-to-ACL2
        • Tours
        • Emacs
      • About-ACL2
        • Recursion-and-induction
        • Operational-semantics
        • Soundness
        • Release-notes
        • Workshops
        • ACL2-tutorial
          • Introduction-to-the-theorem-prover
            • Logic-knowledge-taken-for-granted
            • Logic-knowledge-taken-for-granted-inductive-proof
            • Introduction-to-rewrite-rules-part-1
            • Introduction-to-key-checkpoints
            • Introduction-to-rewrite-rules-part-2
            • Geneqv
            • Logic-knowledge-taken-for-granted-propositional-calculus
            • Refinement-failure
            • Introduction-to-a-few-system-considerations
            • Introduction-to-the-database
            • Programming-knowledge-taken-for-granted
            • Logic-knowledge-taken-for-granted-rewriting
            • Introductory-challenge-problem-4-answer
            • Introduction-to-programming-in-ACL2-for-those-who-know-lisp
            • Introduction-to-hints
            • Dealing-with-key-combinations-of-function-symbols
            • Architecture-of-the-prover
            • Further-information-on-rewriting
            • Frequently-asked-questions-by-newcomers
            • Specific-kinds-of-formulas-as-rewrite-rules
            • Strong-rewrite-rules
            • Practice-formulating-strong-rules-3
            • Practice-formulating-strong-rules-1
            • Practice-formulating-strong-rules-6
            • Generalizing-key-checkpoints
            • Logic-knowledge-taken-for-granted-q1-answer
            • Example-inductions
            • Logic-knowledge-taken-for-granted-q2-answer
            • Logic-knowledge-taken-for-granted-rewriting-repeatedly
            • Introductory-challenge-problem-4
            • Equivalent-formulas-different-rewrite-rules
            • Post-induction-key-checkpoints
            • Special-cases-for-rewrite-rules
            • Example-induction-scheme-with-accumulators
            • Practice-formulating-strong-rules-5
            • Practice-formulating-strong-rules
            • Practice-formulating-strong-rules-2
            • Introductory-challenges
            • Logic-knowledge-taken-for-granted-equals-for-equals
            • Logic-knowledge-taken-for-granted-evaluation
            • Example-induction-scheme-nat-recursion
            • Example-induction-scheme-down-by-2
            • Logic-knowledge-taken-for-granted-instance
            • Introductory-challenge-problem-3-answer
            • Example-induction-scheme-on-lists
            • Example-induction-scheme-upwards
            • Example-induction-scheme-with-multiple-induction-steps
            • Practice-formulating-strong-rules-4
            • Logic-knowledge-taken-for-granted-q3-answer
            • Example-induction-scheme-binary-trees
            • Introductory-challenge-problem-3
            • Introductory-challenge-problem-1
            • Logic-knowledge-taken-for-granted-base-case
            • Introductory-challenge-problem-1-answer
            • Example-induction-scheme-on-several-variables
            • Introductory-challenge-problem-2-answer
            • Introductory-challenge-problem-2
          • Pages Written Especially for the Tours
          • The-method
          • Advanced-features
          • Interesting-applications
          • Tips
          • Alternative-introduction
          • Tidbits
          • Annotated-ACL2-scripts
          • Startup
          • ACL2-as-standalone-program
          • ACL2-sedan
          • Talks
          • Nqthm-to-ACL2
          • Tours
          • Emacs
        • Version
        • How-to-contribute
        • Acknowledgments
        • Using-ACL2
        • Releases
        • Pre-built-binary-distributions
        • Common-lisp
        • Installation
        • Mailing-lists
        • Git-quick-start
        • Copyright
        • ACL2-help
    • Miscellaneous
    • Output-controls
    • Bdd
    • Macros
    • Installation
    • Mailing-lists
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Introduction-to-the-theorem-prover

Introductory-challenge-problem-2

Challenge problem 2 for the new user of ACL2

Start in a fresh ACL2, either by restarting your ACL2 image from scratch or executing :ubt! 1.

Use The Method to prove

(defthm subsetp-reflexive
  (subsetp x x))

When you've solved this problem, compare your answer to ours; see introductory-challenge-problem-2-answer.

Then, use your browser's Back Button to return to introductory-challenges.