• Top
    • Documentation
    • Books
    • Recursion-and-induction
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
      • Theories
      • Rule-classes
      • Proof-builder
      • Hons-and-memoization
      • Events
      • History
      • Parallelism
      • Programming
      • 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
            • 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
            • 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
        • Real
        • Debugging
        • Miscellaneous
        • Output-controls
        • Macros
        • Interfacing-tools
      • Interfacing-tools
      • Hardware-verification
      • Software-verification
      • Testing-utilities
      • Math
    • Introduction-to-the-theorem-prover

    Example-induction-scheme-binary-trees

    Induction on binary trees

    See logic-knowledge-taken-for-granted-inductive-proof for an explanation of what we mean by the induction suggested by a recursive function or a term.

    Classical Induction on Binary Trees: To prove (p x), for all x, by classical induction on binary tree structures, prove each of the following:

    Base Case: 
    (implies (atom x) (p x)) 
    
    Induction Step: 
    (implies (and (not (atom x)) 
                  (p (car x)) 
                  (p (cdr x))) 
             (p x)) 
    

    An argument analogous to that given in example-induction-scheme-on-lists should convince you that (p x) holds for every object.

    A function that suggests this induction is:

    (defun flatten (x)
      (if (atom x)
          (list x)
          (app (flatten (car x))
               (flatten (cdr x))))).