• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • 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
          • 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
            • 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
    • Pages Written Especially for the Tours

    A Trivial Proof

    A Trivial Proof