• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Debugging
  • Projects
  • 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
          • Logic-knowledge-taken-for-granted-propositional-calculus
          • Geneqv
          • Introduction-to-a-few-system-considerations
          • Refinement-failure
          • 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
          • Generalizing-key-checkpoints
          • Logic-knowledge-taken-for-granted-q1-answer
          • Practice-formulating-strong-rules-6
          • 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
        • Emacs
      • About-ACL2
    • Debugging
    • Miscellaneous
    • Output-controls
    • Macros
    • Interfacing-tools
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Introduction-to-the-theorem-prover

Logic-knowledge-taken-for-granted-base-case

A brief explanation of base cases

According to the sentence, the conjecture being proved is ``reversing the reverse of a true-listp yields the original list.'' The formula corresponding to this conjecture is:

(implies (true-listp z)
         (equal (rev (rev z)) z)).

We're also told that this is an inductive proof. Evidently we're doing an induction on the structure of the list z. Then the Base Case is the formula:

(implies (endp z)
         (implies (true-listp z)
                  (equal (rev (rev z)) z))).

Now use your browser's Back Button to return to the example proof in logic-knowledge-taken-for-granted.