• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Debugging
  • Projects
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
    • Theories
    • Rule-classes
    • Proof-builder
    • Hons-and-memoization
    • Events
    • History
    • Parallelism
    • Programming
    • Real
    • ACL2-tutorial
      • Introduction-to-the-theorem-prover
      • Pages Written Especially for the Tours
        • A Tiny Warning Sign
        • About the Prompt
        • ACL2 Symbols
        • Common Lisp
        • About Types
        • The Event Summary
        • An Example of ACL2 in Use
        • The Tours
        • Corroborating Models
        • The Proof of the Associativity of App
        • Guards in ACL2
        • Numbers in ACL2
        • About the Admission of Recursive Definitions
        • Free Variables in Top-Level Input
        • Common Lisp as a Modeling Language
        • ACL2 as an Interactive Theorem Prover (cont)
        • A Flying Tour of ACL2
        • Analyzing Common Lisp Models
        • A Walking Tour of ACL2
        • The Theorem that App is Associative
        • The End of the Walking Tour
        • Proving Theorems about Models
        • Functions for Manipulating these Objects
        • About the ACL2 Home Page
        • ACL2 Conses or Ordered Pairs
        • The Associativity of App
        • Models of Computer Hardware and Software
        • How To Find Out about ACL2 Functions (cont)
        • A Sketch of How the Rewriter Works
        • ACL2 System Architecture
        • Running Models
        • ACL2 is an Untyped Language
        • How To Find Out about ACL2 Functions
        • How Long Does It Take to Become an Effective User(Q)
        • The Admission of App
        • Guiding the ACL2 Theorem Prover
        • What Is ACL2(Q)
        • Conversion
        • An Example Common Lisp Function Definition
        • ACL2 Characters
        • You Must Think about the Use of a Formula as a Rule
        • The WARNING about the Trivial Consequence
        • Guessing the Type of a Newly Admitted Function
        • ACL2 Strings
        • What is a Mathematical Logic(Q)
        • Revisiting the Admission of App
        • What is a Mechanical Theorem Prover(Q)
        • About Models
        • What is Required of the User(Q)
        • Hey Wait! Is ACL2 Typed or Untyped(Q)
        • The Falling Body Model
        • Rewrite Rules are Generated from DEFTHM Events
        • A Typical State
        • The Time Taken to do the Associativity of App Proof
        • The Simplification of the Induction Conclusion (Step 1)
        • The Rules used in the Associativity of App Proof
        • Subsumption of Induction Candidates in App Example
        • Other Requirements
        • Models in Engineering
        • Symbolic Execution of Models
        • Suggested Inductions in the Associativity of App Example
        • Overview of the Proof of a Trivial Consequence
        • Evaluating App on Sample Input
        • The Induction Step in the App Example
        • Modeling in ACL2
        • The Simplification of the Induction Conclusion (Step 9)
        • The Induction Scheme Selected for the App Example
        • The First Application of the Associativity Rule
        • Overview of the Expansion of ENDP in the Induction Step
        • Flawed Induction Candidates in App Example
        • ACL2 as an Interactive Theorem Prover
        • Using the Associativity of App to Prove a Trivial Consequence
        • The Simplification of the Induction Conclusion (Step 8)
        • The Instantiation of the Induction Scheme
        • The Final Simplification in the Base Case (Step 0)
        • Overview of the Simplification of the Induction Step to T
        • Overview of the Simplification of the Induction Conclusion
        • On the Naming of Subgoals
        • Nontautological Subgoals
        • What is a Mechanical Theorem Prover(Q) (cont)
        • The Simplification of the Induction Conclusion (Step 12)
        • The Simplification of the Induction Conclusion (Step 10)
        • The End of the Flying Tour
        • The Base Case in the App Example
        • The Simplification of the Induction Conclusion (Step 11)
        • The Final Simplification in the Base Case (Step 3)
        • The Expansion of ENDP in the Induction Step (Step 1)
        • The Expansion of ENDP in the Induction Step (Step 0)
        • The End of the Proof of the Associativity of App
        • Overview of the Simplification of the Base Case to T
        • The Summary of the Proof of the Trivial Consequence
        • The Simplification of the Induction Conclusion (Step 7)
        • The Simplification of the Induction Conclusion (Step 6)
        • The Simplification of the Induction Conclusion (Step 5)
        • The Simplification of the Induction Conclusion (Step 4)
        • The Simplification of the Induction Conclusion (Step 2)
        • The Simplification of the Induction Conclusion (Step 0)
        • The Justification of the Induction Scheme
        • The Final Simplification in the Base Case (Step 1)
        • The Expansion of ENDP in the Induction Step (Step 2)
        • Popping out of an Inductive Proof
        • Overview of the Expansion of ENDP in the Base Case
        • The Simplification of the Induction Conclusion (Step 3)
        • The Q.E.D. Message
        • Overview of the Final Simplification in the Base Case
        • The Final Simplification in the Base Case (Step 2)
        • Perhaps
        • Name the Formula Above
        • Undocumented Topic
        • A Trivial Proof
      • Advanced-features
      • The-method
      • Interesting-applications
      • Tips
      • Alternative-introduction
      • Tidbits
      • Annotated-ACL2-scripts
      • Startup
      • ACL2-as-standalone-program
      • Talks
      • Nqthm-to-ACL2
      • ACL2-sedan
      • Emacs
    • Debugging
    • Miscellaneous
    • Prover-output
    • Built-in-theorems
    • Macros
    • Interfacing-tools
    • About-ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Testing-utilities
  • Math

• Pages Written Especially for the Tours

The Simplification of the Induction Conclusion (Step 6)

The Simplification of the Induction Conclusion (Step 6)

Subgoal *1/2' 
(IMPLIES (AND (CONSP A) 
              (EQUAL (APP (APP (CDR A) B) C) 
                     (APP (CDR A) (APP B C)))) 
         (EQUAL (IF T 
                    (CONS (CAR A) 
                          (APP (CDR (CONS (CAR A) (APP (CDR A) B))) 
                               C)) 
                    C) 
                (APP A (APP B C)))). 

Click on the link above to apply the Axiom (CDR (CONS x y)) = y.